fix(idris): rebuild logSafeBounded proof for Idris2 0.8.0 (SafeAPIKey baseline rot)

[hyperpolymath]

Summary

Restores Boj.SafeAPIKey to a green Idris2 0.8.0 build. The pre-existing logSafeBounded proof on main does not type-check; this PR rebuilds it against the current stdlib + elaborator behaviour. No new axioms. The 5-class-(J) framing established in #108 is preserved.

Discovered while verifying #108 (item 11). Was originally stacked on #108; rebased onto main after #108 merged at 2026-05-20T08:13Z.

Three independent defects, each fixed

1. Removed the redundant local plusLteMonotone helper. It wrapped lteTransitive (plusLteMonotoneRight _ lmn) (plusLteMonotoneLeft _ lpq):

   • lteTransitive is no longer in stdlib — Idris2 0.8.0 uses Control.Relation.transitive, but that's ambiguous in this import context.
   • plusLteMonotoneRight / plusLteMonotoneLeft have signature (p, q, r : Nat) -> LTE q r -> LTE (q+p) (r+p) in this stdlib — the wrapper passed wildcards expecting a different shape.

   The stdlib already ships Data.Nat.plusLteMonotone : LTE m n -> LTE p q -> LTE (m + p) (n + q) — exactly what the wrapper was trying to be. Use it directly.

2. Lifted both branches out of the with-block. Inside logSafeBounded s with (length s <= 8) proof cond, Idris2 0.8.0 does not reduce length "***" (or length "...") at type level — the goal is exposed as LTE (integerToNat (prim__cast_IntInteger (prim__strLength (if True then ... else ...)))) 11 with the if-arm unreduced. Outside the with-block, the same lemmas type-check via Refl-equivalent computation. Extracted logSafeBoundedShort / logSafeBoundedLong as private helpers; the with-block now just dispatches.

3. Right-associated the long-path proof. (++) is right-associative in Idris (a ++ b ++ c = a ++ (b ++ c)), but the original composed (p1 ++ "...") ++ p3 (left-associative) — its conclusion didn't match the with-block's False-branch goal. New proof: step23 (length "..." + length (substr ...) ≤ 3 + 4) then step123 (length (substr 0 4 s) + length (...) ≤ 4 + 7).

Plus two bound-name typos in toLogSafeShortEq / toLogSafeLongEq where the outer _ discarded the prf argument that the inner branch then referenced.

Test plan

Per-module idris2 --check on every safety module — all 12 green:

Boj.SafetyLemmas        green
Boj.SafeAPIKey          green  (this PR)
Boj.Safety              green
Boj.APIContractCoverage green
Boj.CartridgeDispatch   green
Boj.Catalogue           green
Boj.CredentialIsolation green
Boj.Federation          green
Boj.SafeCORS            green
Boj.SafeHTTP            green
Boj.SafePromptInjection green
Boj.SafeWebSocket       green

idris2 --build src/abi/boj.ipkg does not complete in 9 min on my dev box (gets SIGTERMed) — same note as #108. Per-module --check is the verification surface.

Why this matters

PROOF-NEEDS.md's 2026-05-18 audit claims SafeAPIKey carries constructive proofs that close BJ2-partial. Pre-this-PR the proof did not compile. The audit was, like the SafetyLemmas axiom count noted in #108, evidently a desk-read of the source rather than a build. With this PR merged, the audited safety surface is buildable from scratch.

Refs epic #87 Tier C (companion to #108 / #109).

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 31 issues detected

Severity	Count
🔴 Critical	19
🟠 High	5
🟡 Medium	7

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Stale AI session file -- delete",
    "type": "stale",
    "file": "GEMINI.md",
    "action": "delete",
    "rule_module": "root_hygiene",
    "severity": "medium"
  },
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Python file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/.github/scripts/validate-eclexiaiser.py",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/sanctify-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/academic-workflow-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/fireflag-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/ephapax-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/bofig-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

[github-actions]

🔍 Hypatia Security Scan

Findings: 31 issues detected

Severity	Count
🔴 Critical	19
🟠 High	5
🟡 Medium	7

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Stale AI session file -- delete",
    "type": "stale",
    "file": "GEMINI.md",
    "action": "delete",
    "rule_module": "root_hygiene",
    "severity": "medium"
  },
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Python file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/.github/scripts/validate-eclexiaiser.py",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/sanctify-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/academic-workflow-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/fireflag-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/ephapax-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/bofig-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence