docs: honest framing of remaining ABI axioms (epic #87 Tier C item 11) (#108)

## Summary

- Module docstring on `src/abi/Boj/SafetyLemmas.idr` claimed "Three
axiomatic `believe_me` primitives" while five live in the file.
Corrected to enumerate all five and tag each to its underlying `prim__*`
primitive.
- `appendLengthSum` and `substrLengthBound` declarations used `(x y :
T)` multi-binder syntax which **Idris2 0.8.0 rejects** at parse time
("Expected a type declaration" at the colon). Adding the comma — `(x, y
: T)` — restores parsability. Types and proof terms are unchanged.
- New `== Formal verification` section in `README.adoc` summarising
posture so external readers don't have to dig through `PROOF-NEEDS.md`:
all P1/P2 obligations closed; the 5 remaining axioms are *principled
assumptions over Idris2 primitives*, not unproven debt.

## Why this is a docs PR, not a discharge campaign

The 2026-05-18 audit in `PROOF-NEEDS.md` already classified every
remaining `believe_me` as class (J) — *genuinely unavoidable* in Idris2
0.8.0 because `Char` / `String` are opaque primitives with no
in-language induction principle. The reduction path is external
backend-assurance (Chez/BEAM extraction), not constructive proof. Item
11 was therefore already done as research — just not surfaced honestly.
This PR closes the documentation gap.

`d2622566 proof(abi): reduce believe_me from 31 to 4` is where the "4
axioms canonical" framing originated; `4f729e7e` and `0de09a47` later
added `appendLengthSum` and `substrLengthBound`. Honest current count:
5.

## Out of scope (deliberately)

- `src/abi/Boj/SafeAPIKey.idr` has **independent baseline rot**:
`plusLteMonotone` not found (likely stdlib rename — "did you mean
transitive?") + a constraint-solver failure on `logSafeBounded`.
Pre-existing, **not** introduced here. Worth a separate fix-up PR.
- `idris2 --build src/abi/boj.ipkg` does not complete in 9 min on my dev
box (gets SIGTERMed). Per-module `idris2 --check` is fast and was used
for verification.
- No CI workflow exercises the `src/abi/boj.ipkg` build today
(`.github/workflows/` only mentions idris2 in `abi-drift.yml` which uses
a different tool). Wiring an idris2 build into CI is a separate concern.

## Test plan

- [x] `idris2 --check src/abi/Boj/SafetyLemmas.idr` — green with my
changes; previously red on `origin/main` due to the multi-binder parse
error.
- [x] `idris2 --check src/abi/Boj/Safety.idr` — green (downstream
consumer of `charEqSound`).
- [ ] CI Hypatia neurosymbolic analysis + dogfood gate (will run on PR
open).
- [ ] Reviewer sanity-check on PROOF-NEEDS.md vs the new README posture.

## Related branches / overlap to resolve

`fix/proof-needs-reconcile-believe-me` exists on remote (single commit
`3d6b881c` dated 2026-05-18, title says "reconcile believe_me audit — 5
justified axioms, not zero/4") but its diff does **not** touch
`PROOF-NEEDS.md`, `SafetyLemmas.idr`, or `README.adoc` — looks
abandoned. Worth a quick owner confirmation that this PR isn't
displacing intentional work.

Refs epic #87 Tier C item 11. Item 12 (cross-cartridge composition
proof) is a separate draft PR (ADR-0014 RFC).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

README.adoc

@@ -107,6 +107,27 @@ Run the coherence tests:
 node --test mcp-bridge/tests/
 ----
 
+== Formal verification
+
+BoJ's ABI safety layer is written in Idris2 with the proof obligations
+audited in `PROOF-NEEDS.md`. Headline posture (as of 2026-05-18 audit):
+
+* *All P1/P2 obligations closed.* `SafePromptInjection`, `SafeCORS`,
+  `SafeAPIKey`, `SafeWebSocket`, `SafeHTTP`, `Federation`, `Catalogue`,
+  `CartridgeDispatch` (BJ1), `CredentialIsolation` (BJ2),
+  `APIContractCoverage` (BJ3) — all carry constructive proofs.
+* *Five remaining `believe_me` invocations*, all isolated in
+  `src/abi/Boj/SafetyLemmas.idr`, all class (J) — *principled
+  assumptions*, not unproven debt. They axiomatise the soundness of
+  Idris2 0.8.0's opaque `Char`/`String` primitives (`prim__eqChar`,
+  `prim__strToCharList`, `prim__strAppend`, `prim__strSubstr`) which
+  have no in-language induction principle. The only reduction path is
+  external backend-assurance evidence (Chez/BEAM extraction or
+  property-test harness), not constructive in-language proof.
+* *No unproven obligations remain in the audited surface.* The full
+  per-site rationale and the in-progress cross-cartridge composition
+  question are tracked in `PROOF-NEEDS.md` and `docs/decisions/`.
+
 == License
 
 PMPL-1.0-or-later

src/abi/Boj/SafetyLemmas.idr

@@ -6,12 +6,20 @@
 ||| proofs in SafeHTTP, SafeCORS, SafeWebSocket, SafePromptInjection,
 ||| SafeAPIKey, and Safety modules.
 |||
-||| Three axiomatic believe_me primitives are declared here:
-|||   charEqSound  — soundness of prim__eqChar (c1 == c2 = True → c1 = c2)
-|||   charEqSym    — symmetry of prim__eqChar (x == y = y == x)
-|||   unpackLength — prim__strToCharList preserves length
+||| Five axiomatic believe_me primitives are declared here. Each is
+||| class (J) — genuinely unavoidable in Idris2 0.8.0 because `Char`
+||| and `String` are opaque primitive types whose operations are
+||| foreign functions with no constructors and no in-language induction
+||| principle. They are documented as principled assumptions, not
+||| unproven debt; see PROOF-NEEDS.md for the per-site audit.
 |||
-||| All other proofs are constructive.
+|||   charEqSound       — soundness of prim__eqChar (c1 == c2 = True → c1 = c2)
+|||   charEqSym         — symmetry of prim__eqChar (x == y = y == x)
+|||   unpackLength      — prim__strToCharList preserves length
+|||   appendLengthSum   — prim__strAppend: length (s ++ t) = length s + length t
+|||   substrLengthBound — prim__strSubstr: result no longer than the requested count
+|||
+||| All other proofs in this module are constructive.
 module Boj.SafetyLemmas
 
 import Data.List
@@ -215,12 +223,12 @@ unpackLength _ = believe_me ()
 ||| Idris2 type level. Established by semantics of all supported backends.
 %unsafe
 export
-appendLengthSum : (s t : String) -> length (s ++ t) = length s + length t
+appendLengthSum : (s, t : String) -> length (s ++ t) = length s + length t
 appendLengthSum _ _ = believe_me ()
 
 ||| Substring of a string has length at most the requested count.
 ||| Axiomatic: prim__strSubstr semantics — result is never longer than `len`.
 %unsafe
 export
-substrLengthBound : (s : String) -> (start len : Nat) -> LTE (length (substr start len s)) len
+substrLengthBound : (s : String) -> (start, len : Nat) -> LTE (length (substr start len s)) len
 substrLengthBound _ _ _ = believe_me ()