[proofs/a] boj-server core: enforce + minimise the trusted base

[hyperpolymath]

Tracking issue for the core server proof obligations (scope a of the proving sort-out).

Current state (verified 2026-06-05)

• 17 .idr under src/abi/Boj/.
• Trusted base = exactly 5 axioms, all believe_me () in src/abi/Boj/SafetyLemmas.idr (lines 67, 76, 241, 251, 261): charEqSound, charEqSym, unpackLength, appendLengthSum, substrLengthBound.
• Zero real postulate / assert_total / sorry / idris_crash in core .idr (the lone grep hit is a doc comment). check-trusted-base.sh enforces this.
• SafeHTTP.idr is fully constructive.

What remains

1. Enforce compilation in CI. Confirm proofs.yml actually idris2 --checks the modules (not just structural checks) and fails on a proof error. It is currently blind to ffi/** — the Zig layer the proofs are about — so a breaking FFI change can't trip a proof. Wire proof obligations to ffi/**.
2. Minimise the trusted base. Audit the 5 axioms: which can be discharged constructively (esp. the Length/append/substr arithmetic lemmas)? This is the near-term face of the obleeny plan (scope d).
3. Stop committing proof binaries. src/abi/build/ttc/**/*.ttc and *.ttm are checked into git — gitignore them; CI recompiles, never trusts a committed artifact.
4. Fix the broken proof gate (shared with scope b/e): lsp-dap-bsp.yml's "ABI Specification Check" greps believe_me|assert_total|sorry over the whole abi/ dir and matches README.adoc documentation — a false positive on every run. Scope the grep to *.idr.

Done when

• Core proofs compile in CI on every src/abi/** and ffi/** change.
• Trusted base documented with a per-axiom "can this be discharged?" verdict.
• No compiled proof artifacts in git.

Proving track — active in the proving+maker thread.

---

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

[hyperpolymath]

Unmerged proof groundwork found (2026-06-05 checkpoint)

The branch claude/cartridge-abi-proofs holds proof-CI work that is not on main (its remote was pruned during reconciliation; re-pushed for preservation). It directly advances this issue — review, rebase onto current main, and land it as the first move of the proving phase rather than redoing it.

What it contains (3 commits not on main):

• c4e1e2d — type-check all cartridge ABIs under Idris2 0.8.0 (fixes across 17 .idr: fireflag, hesiod, hypatia, k8s, local-coord ×3, matrix, ml, model-router, panic-attack, pmpl, postgresql, reposystem, sanctify, stapeln, verisimdb).
• c67e6f5 — gate every Idris2 ABI in CI + add scripts/check-trusted-base.sh.
• 86cb115 — add timeout-minutes + shellcheck-clean the sweep; adds scripts/typecheck-proofs.sh (idris2 --checks every cartridge ABI).

Why it matters here: this is most of "enforce compilation in CI" (item 1 of this issue) and the cartridge-side of scope b (hyperpolymath/boj-server-cartridges#36). Note check-trusted-base.sh already exists on main and proofs.yml has some gating — so this branch needs a rebase + reconcile (not a blind merge) to avoid duplicating what landed since.

Caveat: the Foundry already ships tools/foundry/proof/check.sh (typechecks the design proof) and stages/harness.sh (idris2 --check per cartridge) in boj-server-cartridges. Reconcile the two proof-CI approaches so there's one canonical gate, not two.

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

---

Generated by Claude Code

[hyperpolymath]

Verified: core + all boj-server cartridge ABIs type-check (2026-06-05 real sweep)

Real idris2 --check (0.8.0) via parallel agents:

• Core src/abi/Boj/ — 17/17 pass. Trusted base = exactly 5 believe_me (SafetyLemmas.idr:67,76,241,251,261); zero other axioms anywhere in core. ✅
• cartridges/*/abi/ — 108/108 pass, zero leaf axioms (the believe_me grep hits that broke lsp-dap-bsp.yml are all README prose — fixed in fix(ci): make the LSP/DAP/BSP gate real + policy-compliant #205).

So this repo's proofs compile cleanly under the pinned toolchain — the cartridge-abi-proofs branch's 0.8.0 fixes are effectively already on main. The remaining work for this issue is the enforcement/minimisation items (wire proofs.yml to ffi/**, drop committed .ttc, shrink the 5 axioms), not broken proofs.

(For contrast: the boj-server-cartridges domains tree has 18 broken proofs — see hyperpolymath/boj-server-cartridges#36. boj-server is the canonical tree.)

---

Generated by Claude Code