fix(abi): type-check all 17 Idris2 proofs under 0.8.0

[hyperpolymath]

Summary

Against the pinned toolchain (Idris2 0.8.0, Chez backend), 6 of the 17 core ABI proof modules did not type-check — yet all were marked "✅ Complete". They rotted undetected because the build never exercised them:

• just typecheck used an invalid invocation (idris2 --check --package boj boj.ipkg → "Can't find package boj"); the correct form is --typecheck boj.ipkg.
• CartridgeDispatch and APIContractCoverage were absent from boj.ipkg, so the package build skipped them entirely.

After this PR, cd src/abi && idris2 --typecheck boj.ipkg builds all 17 modules clean. Theorem statements and the axiom budget are unchanged — the fixes are in the proofs' construction.

Proof fixes (all constructive, zero new axioms)

Module	Root cause	Fix
CartridgeDispatch	bare-pipe with syntax 0.8.0 rejects; refusedIfNoMatch needed a reducible dispatch; absurd lacked Uninhabited instances	full-LHS with; dispatch via reducible dispatchOn helper; conjunction + statusEqSoundReady + 3 Uninhabited lemmas
SafePromptInjection	with-abstraction rewrites goal to True = True	Right Refl
SafeCORS	same with issue; undefined fromLteTrue	(Refl, Refl); fromLteTrue → lteReflectsLTE
SafeHTTP	missing Data.List.Elem/Data.Maybe; IsJust→isJust; all→allRec; erased implicits; let x : a = b mis-parse	imports, name fixes, explicit {xs,ys}, parenthesised annotations
SafeWebSocket	elaborator OOM — 16 MiB maxFrameSize baked into a constructor LTE index forced a unary Nat	bound-parameterised FrameSizeSafeUpTo; FrameSizeSafe/ControlFrameSizeSafe become synonyms
APIContractCoverage	representativeCatalogue auto-bound as a fresh implicit (shadowed the global)	fully qualified
SafetyLemmas	allTake referenced but undefined	added the constructive lemma (no new axiom)

Plumbing & docs

• boj.ipkg: added Boj.CartridgeDispatch + Boj.APIContractCoverage.
• Justfile: typecheck now uses --typecheck; verify-no-believe-me reconciled to the sanctioned 5-axiom trusted base (it previously enforced zero, contradicting PROOF-NEEDS.md), and fails on any other believe_me or on axiom-count drift.
• PROOF-NEEDS.md / verification/proofs/README.adoc: build-verification notes.

Trusted base unchanged

believe_me count = 5, all in SafetyLemmas.idr, all %unsafe class-(J) axioms (opaque Char/String primitives). No assert_total / assert_smaller / new %unsafe anywhere.

Roadmap (this branch, follow-up commits)

• Core boj ABI package green under 0.8.0
• Cartridge ABIs — common components (fleet/nesy/database/agent/feedback + shared protocol/safety patterns)
• Remaining cartridge-specific proofs (~100 .idr files)

Draft until the cartridge ABIs are also green.

https://claude.ai/code/session_019tMcRS1Dm1nWjjYP4WvbJa

---

Generated by Claude Code

[github-actions]

🏁 path-claims bench

Commit 36d8de2

Numbers

path-claims bench  (node v22.22.3)

  scenario                                              iters       ms        ns/op          ops/s
  --------------------------------------------------------------------------------------------------------------
  register: 10 active claims, 3 new paths               50000 iters    198 ms      3.98 µs/op    251.4k ops/s
  register: 100 active claims, 3 new paths              20000 iters    332 ms     16.61 µs/op     60.2k ops/s
  register: 1000 active claims, 3 new paths              5000 iters   1004 ms    200.96 µs/op      5.0k ops/s
  register: 100 active claims, 20 new paths              5000 iters    387 ms     77.45 µs/op     12.9k ops/s

  pathsOverlap: deep diverge at segment 4             1000000 iters    164 ms     164.5 ns/op     6.08M ops/s
  pathsOverlap: short prefix match                    1000000 iters    140 ms     140.8 ns/op     7.10M ops/s

  refresh (existing claim)                             100000 iters     10 ms     108.6 ns/op     9.20M ops/s
  list (100 active claims)                              50000 iters    317 ms      6.36 µs/op    157.3k ops/s

  (Bench numbers depend on host; use deltas across commits, not absolute values.)

Host-dependent — compare deltas across commits, not absolute values.

[github-actions]

🔍 Hypatia Security Scan

Findings: 255 issues detected

Severity	Count
🔴 Critical	15
🟠 High	130
🟡 Medium	110

⚠️ 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": "Action    if: always()\n        uses: actions/upload-artifact@ea165 needs attention",
    "type": "unpinned_action",
    "file": "e2e.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "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 abi-drift.yml",
    "type": "missing_timeout_minutes",
    "file": "abi-drift.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 container-publish.yml",
    "type": "missing_timeout_minutes",
    "file": "container-publish.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"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.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"
  },
  {
    "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