proof(SafeCapability): DISCHARGE 5 anchor OWEDs via Refl (file fully clear) (proven#90)

[hyperpolymath]

Seventh "overly cautious OWED" discharge of today's proven#90 Phase 3 campaign — clears the full file.

What it does

All 5 SafeCapability OWEDs in src/Proven/SafeCapability/Proofs.idr discharge by Refl:

public export
makeNonDelegatableSetsFalse :
  (cap : Capability) -> (makeNonDelegatable cap).capDelegatable = False
makeNonDelegatableSetsFalse _ = Refl

public export
setExpirySetsJust :
  (t : Nat) -> (cap : Capability) -> (setExpiry t cap).capExpiry = Just t
setExpirySetsJust _ _ = Refl

public export
emptyStoreNoCapabilities : (emptyStore).capabilities = []
emptyStoreNoCapabilities = Refl

public export
emptyStoreNoRevoked : (emptyStore).revoked = []
emptyStoreNoRevoked = Refl

public export
adminHierarchyDef : adminHierarchy = MkHierarchy Admin [Read, Write, Execute, Delete]
adminHierarchyDef = Refl

Why it works

All 5 underlying definitions are public export with concrete bodies:

• makeNonDelegatable cap = { capDelegatable := False } cap (L171-172)
• setExpiry time cap = { capExpiry := Just time } cap (L176-177)
• emptyStore = MkCapabilityStore [] [] (L188-189)
• adminHierarchy = MkHierarchy Admin [Read, Write, Execute, Delete] (L258-259)

Idris2 unfolds public export definitions at the type level, so the record-update projection ({ field := value } _) and the named-constructor projection both reduce directly for Refl.

Pattern (now 7 PRs deep)

The OWED comments cited "public export body opacity" as the blocker — that diagnosis is inverted. public export ENABLES type-level unfolding (it's private and export-only that block it). The 5 OWEDs were thus mis-classified as needing case-splits when they only needed Refl.

Combined session count: 6 PRs filed, 5 merged (Idris 2 CI accepting Refl cleanly across SafeUrl, SafeRegex, SafeEmail, SafeCron, SafeGit). This makes the eighth.

Refs #90

[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: 331 issues detected

Severity	Count
🔴 Critical	130
🟠 High	31
🟡 Medium	170

⚠️ 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": "missing_timeout_minutes",
    "file": "architecture-enforcement.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in architecture-enforcement.yml",
    "type": "missing_timeout_minutes",
    "file": "architecture-enforcement.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "missing_timeout_minutes",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_batch.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_batch.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_pr.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_pr.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_timeout_minutes",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence