[hyperpolymath]

Summary

• Replace bodyless 0 misconfiguredNoHeaders OWED declaration in src/Proven/SafeCORS/Proofs.idr with a genuine proof via a small validatePolicyNonNil bridge lemma.
• Zero believe_me, zero postulate, zero assert_total. Both new top-level functions are public export for downstream reuse.

Why this works (refuting the OWED note)

The prior OWED comment claimed Idris2 0.8.0 could not reduce the validatePolicy / generateHeaders guard chain past the leading ++ conjunct. In fact:

• rewriteing by isUnsafeConfiguration policy = True collapses the inner if to its True arm.
• [WildcardWithCredentials] ++ tail then unfolds to WildcardWithCredentials :: tail.
• isNil (_ :: _) reduces by Refl.
• The opaque emptyMethods right operand of ++ never needs to be inspected, because isNil matches the spine constructor of the whole list, not its content.

Scope discipline

This PR does NOT touch the four pre-existing broken Refl proofs in the same file (defaultPolicyDeniesAll, defaultPolicyIsSafe, defaultPolicyNoErrors, defaultPolicyNoHeaders). They fail for a different reason — Idris2 0.8.0 does not reduce record-field projection on MkCORSPolicy ... unless the value name is qualified. Independent tech debt; will file as separate follow-up issue.

Test plan

• Local: idris2 --build cors-check.ipkg (private isolated package) reports exactly the 4 pre-existing Refl errors and zero new errors at misconfiguredNoHeaders or validatePolicyNonNil.
• No believe_me / postulate / assert_total introduced.
• CI: Proven.SafeCORS.Proofs is not in proven.ipkg (see follow-up issue) so this PR does not change CI surface; the discharge stands on its own type signature.

Refs hyperpolymath/standards#124
Refs hyperpolymath/standards#158

Co-Authored-By: Claude Opus 4.7 (1M context) noreply@anthropic.com

🤖 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: 385 issues detected

Severity	Count
🔴 Critical	177
🟠 High	36
🟡 Medium	172

⚠️ 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