[hyperpolymath]

Summary

Discharges 4 default-policy Refl proofs in src/Proven/SafeCORS/Proofs.idr that previously failed to type-check under Idris2 0.8.0:

• defaultPolicyDeniesAll
• defaultPolicyIsSafe
• defaultPolicyNoErrors
• defaultPolicyNoHeaders

Root cause (per #92)

Idris2 0.8.0 implicitly binds a bare lowercase identifier in a type
signature as a fresh implicit variable when no upper-case rule fires
first, even when a top-level name with the same identifier exists in
scope. The elaborator emits a shadowing the associated global definitions warning. The Refl on the RHS then cannot reduce
because the type-level defaultPolicy is the opaque implicit, not
the concrete record value.

Fix

Option 1 from the issue body — qualify every defaultPolicy
occurrence in the 4 signatures to Proven.SafeCORS.defaultPolicy.
Mechanical, minimal, no believe_me / assert_total / postulate.
A NOTE comment in the file captures the trap so a future reader
doesn't strip the qualifier on a "tidy-up" pass.

CI gap closed

Proven.SafeCORS.Proofs was not in proven.ipkg, so the Idris 2 CI workflow never type-checked it — exactly how the bug landed
silently in the first place. PR adds it to the modules list.

Sibling audit (per #92 acceptance)

File	Status	Notes
Proven.SafeArgs.Proofs	✓ clean	already in ipkg; CI catches it
Proven.SafeAPIKey.Proofs	✗ 2 failures of a different class	filed as follow-up — emptyKeyRejected needs with-block reduction, fullMaskFormat needs String ++ FFI reduction. Neither is the qualified-projection bug.

SafeAPIKey.Proofs is not added to ipkg in this PR (would regress
CI). Once the follow-up lands, fold it in.

Acceptance criteria

• All four defaultPolicy* Refl proofs type-check
• Proven.SafeCORS.Proofs added to proven.ipkg
• Sibling audit completed for SafeAPIKey.Proofs + SafeArgs.Proofs
• CI green on idris2-ci.yml (will verify on push)

Test plan

• CI Idris 2 CI workflow green
• idris2 --build proven.ipkg builds clean locally (verified with IDRIS2_PREFIX workaround)
• Spot-check: idris2 --check src/Proven/SafeCORS/Proofs.idr reports no errors

Closes #92 (partial — SafeAPIKey portion intentionally deferred per audit above)
Refs metadatastician/standards#124

🤖 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