[proofs/b] Cartridge proofs (domains): coverage + single source of truth

[hyperpolymath]

Tracking issue for cartridge proof obligations in general (scope b).

Current state (verified 2026-06-05)

• boj-server-cartridges: 99 .idr under cartridges/domains/; ~2 believe_me/postulate sites to audit.
• boj-server (embedded cartridges/): 104/125 cartridges have abi/*.idr; 21 have none.
• Two proof homes exist — boj-server/cartridges/*/abi/ and boj-server-cartridges/cartridges/domains/ — risk of divergence.

What remains

1. Single source of truth. Decide which repo is canonical for cartridge ABI proofs and reconcile/dedupe the two trees (or define the sync direction).
2. Coverage. Enumerate the 21 embedded cartridges with no abi/ — each gets a compiling ABI proof or a documented exemption (mirror the TS-exemption-table style).
3. Drift gate. abi-drift covers a subset (~66/110 per the prior audit) — bring every cartridge onto the allowlist or exempt it explicitly.
4. Constructive completeness. Audit the ~2 believe_me/postulate sites in the domain proofs; discharge or justify.
5. Fix the false-positive ABI gate (lsp-dap-bsp.yml, shared with scope a/e): grep *.idr only.

Done when

• Every cartridge has a compiling ABI proof or a documented exemption.
• One canonical proof tree; drift gate covers all cartridges; gate has no doc false-positives.

Proving track.

---

Filed via Claude Code · https://claude.ai/code/session_019tMcRS1Dm1nWjjYP4WvbJa

[hyperpolymath]

Evidence: domain proofs are broken AND diverged from boj-server (2026-06-05 real idris2 --check sweep)

Ran idris2 --check (0.8.0) on every proof in both repos via parallel agents. For this repo's cartridges/domains/: 81/99 pass, 18 FAIL. Crucially, the boj-server copies of several of these pass — so the two trees have diverged: boj-server holds the fixed proofs, this repo holds stale broken ones. That is the concrete case for this issue's "single source of truth" item.

The 18 failures (grouped by error)

• Module-name mismatch (module ABI.X but file at abi-root → wants module X): code-quality/sanctify-mcp/Sanctify.idr, development/fireflag-mcp/Fireflag.idr, research/bofig-mcp/Bofig.idr
• public without export: infrastructure/hesiod-mcp/Hesiod.idr, research/academic-workflow-mcp/AcademicWorkflow.idr
• reserved word (total/data) as record field: config/conflow-mcp/Conflow/Protocol.idr, container/k8s-mcp/K8sMcp/SafeK8s.idr, repository-management/reposystem-mcp/Reposystem/Protocol.idr, security/panic-attack-mcp/PanicAttack/Protocol.idr, formal-verification/ephapax-mcp/Ephapax.idr
• Undefined name NonEmpty (missing import): ci-cd/hypatia-mcp/Hypatia/Protocol.idr, community/civic-connect-mcp/CivicConnect/Protocol.idr, container/stapeln-mcp/Stapeln/Protocol.idr
• Undefined name LTE/lteTransitive: ci-cd/hypatia-mcp (also), legal/pmpl-mcp/PmplMcp/SafeProvenance.idr
• duplicate constructor Connect: database/postgresql-mcp/PostgresqlMcp/SafeDatabase.idr
• Refl can't close length = 8: database/verisimdb-mcp/VeriSimDB/Protocol.idr
• parse error (named arg in ctor position): communications/burble-admin-mcp/BurbleAdmin/Protocol.idr
• Expected a type declaration: communications/matrix-mcp/MatrixMcp/SafeComms.idr

No axioms (believe_me/postulate/etc.) in any .idr — README boilerplate only.

Recommendation

boj-server's cartridges/*/abi/ is the canonical, compiling tree (108/108 pass under 0.8.0). Reconcile by syncing the fixed proofs boj-server → here (or porting the 18 fixes), then wire this repo into the same idris2 --check gate. Until then this repo's domain proofs are not authoritative.

Real-check evidence; cross-cutting batch still verifying.

---

Generated by Claude Code

[hyperpolymath]

PR #40 — proof-compilation reconciled + gate added.

The compilation half of this issue is resolved. Verified with real idris2 --check (0.8.0): the 18 domain proofs that had drifted out of compilation now type-check, by syncing each from its compiling boj-server twin. Repo-wide the new gate reports 113/113 proofs pass, 0 axioms.

Against the original checklist:

• (4) Constructive completeness — tree is now axiom-free; scripts/check-trusted-base.sh enforces zero believe_me/assert/idris_crash/sorry in CI.
• (3) Drift gate — new .github/workflows/proofs.yml type-checks every cartridge ABI (not a subset) on each proof-touching PR. This was the actual hole: nothing ran idris2 in this repo before, so drift was invisible.
• [~] (1) Single source of truth — direction is now decided and applied: a non-compiling proof can't be the source of truth, so boj-server's compiling tree is canonical and the 21 diverged cartridges are reconciled to it. What remains is the physical dedup — one tree vendored/generated into the other instead of two hand-maintained copies. Recommendation: make this repo the canonical home (it is the cartridge home), with boj-server consuming a pinned snapshot, both sides gated by this same proofs.yml.
• (2) Coverage — enumerate boj-server's embedded cartridges that have no abi/ (a boj-server-side task; every abi/ in this repo now compiles).
• (5) lsp-dap-bsp false positive — fixed in boj-server #205 (grep --include='*.idr').

Leaving open for the dedup decision (1) and the embedded-coverage enumeration (2).

---

Generated by Claude Code