[hyperpolymath]

Summary

Closes #95 — the two SafeAPIKey `Proofs.idr` Refl proofs that were broken under Idris2 0.8.0 (a DIFFERENT bug class from #92's shadowing) now both type-check.

Root causes

Both proofs failed because Idris2 0.8.0 does not reduce string FFI primitives at type-check time.

`emptyKeyRejected : mkAPIKey "" = Nothing`

Pre-fix `mkAPIKey` definition:
```idris
mkAPIKey s with (choose (length s >= MinKeyLength))
mkAPIKey s | Left prf = Just (MkAPIKey s ...)
mkAPIKey s | Right _ = Nothing
```

For `mkAPIKey ""`, the type-checker needed `length ""` to reduce to a concrete `Nat`, then `0 >= 16` to `False`, then `choose False` to `Right Oh`. The `prim__strLength`/`>=` FFI chain doesn't reduce.

`fullMaskFormat : (key : APIKey) -> isPrefixOf "[REDACTED:" (fullMask key) = True`

`fullMask key` is `"[REDACTED:" ++ show (length key.raw) ++ " chars]"`. `isPrefixOf` goes via `unpack` + list-prefix-by — over a universally-quantified `key`, these don't reduce.

Fixes

`emptyKeyRejected` — fast-path equation

Added an explicit `mkAPIKey "" = Nothing` equation BEFORE the `with`-block in `SafeAPIKey.idr`:

```idris
mkAPIKey "" = Nothing
mkAPIKey s with (choose (length s >= MinKeyLength))
...
```

Identical runtime behaviour (empty rejected either way), proof discharges by `Refl` directly via the first equation match.

`fullMaskFormat` -> `fullMaskStructure` — reshape

Replaced with the structurally-true variant:

```idris
fullMaskStructure : (key : APIKey) ->
fullMask key = "[REDACTED:" ++ show (length key.raw) ++ " chars]"
fullMaskStructure _ = Refl
```

Same safety guarantee, mechanically: the masked output is a fixed-prefix template containing only the redacted length count, no key material. A consumer that needs `isPrefixOf` form can derive it locally from `fullMaskStructure` + a small list-prefix lemma without hitting the FFI wall.

CI gap closed

`Proven.SafeAPIKey.Proofs` added to `proven.ipkg` modules list — was excluded by #94 (sibling-audit) pending the present fix.

Acceptance criteria

• `emptyKeyRejected` type-checks (via `mkAPIKey` fast-path)
• `fullMaskFormat` type-checks (reshaped as `fullMaskStructure`)
• `Proven.SafeAPIKey.Proofs` added to `proven.ipkg`
• CI `Idris 2 CI` green (will verify on push)

Test plan

• `idris2 --check src/Proven/SafeAPIKey/Proofs.idr` clean (Idris2 0.8.0, zero `believe_me` / `assert_total` / `postulate`)
• CI build green

Refs

• Closes proof(SafeAPIKey): emptyKeyRejected + fullMaskFormat fail to reduce (Idris2 0.8.0) #95
• Refs proof(SafeCORS): 4 broken Refl proofs need qualified-projection fix #92 (sibling-audit surfaced this — DIFFERENT bug class from proof(SafeCORS): 4 broken Refl proofs need qualified-projection fix #92's shadowing)
• Refs proof(SafeCORS): qualify defaultPolicy to fix 4 broken Refl proofs (#92) #94 (which excluded `SafeAPIKey.Proofs` from ipkg pending the present fix)

🤖 Generated with Claude Code

[sonarqubecloud]

Quality Gate passed

Issues
0 New issues
0 Accepted issues

Measures
0 Security Hotspots
0.0% Coverage on New Code
0.0% Duplication on New Code

See analysis details on SonarQube Cloud

[github-actions]

🔍 Hypatia Security Scan

Findings: 383 issues detected

Severity	Count
🔴 Critical	177
🟠 High	38
🟡 Medium	168

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in architecture-enforcement.yml",
    "type": "unknown",
    "file": "architecture-enforcement.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in architecture-enforcement.yml",
    "type": "unknown",
    "file": "architecture-enforcement.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "unknown",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "unknown",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "unknown",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_batch.yml",
    "type": "unknown",
    "file": "cflite_batch.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_pr.yml",
    "type": "unknown",
    "file": "cflite_pr.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "unknown",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "unknown",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence