Skip to content

Commit 3de07a6

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
fix(abi): type-check all 17 Idris2 proofs under 0.8.0 (#189)
## 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) - [x] 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](https://claude.ai/code/session_019tMcRS1Dm1nWjjYP4WvbJa)_ Co-authored-by: Claude <noreply@anthropic.com>
1 parent 165e353 commit 3de07a6

11 files changed

Lines changed: 267 additions & 95 deletions

‎Justfile‎

Lines changed: 33 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -394,28 +394,49 @@ lint: verify-no-believe-me typecheck
394394
# ═══════════════════════════════════════════════════════════════════════════════
395395

396396
# Type-check all Idris2 ABI files
397+
# NOTE: package type-checking uses `idris2 --typecheck <pkg>.ipkg` (the prior
398+
# `--check --package boj boj.ipkg` form is invalid — `--check` is for .idr
399+
# files and `--package` looks up an *installed* package, so it never ran).
397400
typecheck:
398-
@echo "Type-checking core ABI..."
399-
cd src/abi && idris2 --check --package boj boj.ipkg
401+
@echo "Type-checking core ABI (17 modules)..."
402+
cd src/abi && idris2 --typecheck boj.ipkg
400403
@echo "Type-checking cartridge ABIs..."
401-
cd cartridges/fleet-mcp/abi && idris2 --check fleet-mcp.ipkg
402-
cd cartridges/nesy-mcp/abi && idris2 --check nesy-mcp.ipkg
403-
cd cartridges/database-mcp/abi && idris2 --check database-mcp.ipkg
404-
cd cartridges/agent-mcp/abi && idris2 --check agent-mcp.ipkg
405-
cd cartridges/feedback-mcp/abi && idris2 --check feedback-mcp.ipkg
404+
cd cartridges/fleet-mcp/abi && idris2 --typecheck fleet-mcp.ipkg
405+
cd cartridges/nesy-mcp/abi && idris2 --typecheck nesy-mcp.ipkg
406+
cd cartridges/database-mcp/abi && idris2 --typecheck database-mcp.ipkg
407+
cd cartridges/agent-mcp/abi && idris2 --typecheck agent-mcp.ipkg
408+
cd cartridges/feedback-mcp/abi && idris2 --typecheck feedback-mcp.ipkg
406409
@echo "All ABI files type-check!"
407410

408-
# Verify zero believe_me in all Idris2 sources
411+
# Verify the trusted base: no unsound constructs beyond the sanctioned axioms.
412+
#
413+
# The estate trusted-base reduction policy (hyperpolymath/standards#203) sanctions
414+
# EXACTLY the 5 class-(J) axioms in src/abi/Boj/SafetyLemmas.idr — opaque Char/String
415+
# primitives, %unsafe-tagged and externally validated (see PROOF-NEEDS.md and
416+
# docs/proof-debt.md). Everything else must be a genuine constructive proof.
417+
# This recipe fails on any believe_me/assert_* outside that module, and also
418+
# fails if the audited axiom count drifts from 5 (keep the docs in sync).
409419
verify-no-believe-me:
410420
#!/usr/bin/env bash
411-
echo "Scanning for believe_me..."
412-
FOUND=$(grep -rn 'believe_me\|assert_total\|assert_smaller' --include='*.idr' src/ cartridges/ 2>/dev/null | grep -v -- '--.*believe_me' | grep -v '|||.*believe_me' | grep -v -- '--.*Admitted' | grep -v '|||.*Admitted' || true)
421+
set -euo pipefail
422+
AXIOM_FILE="src/abi/Boj/SafetyLemmas.idr"
423+
echo "Scanning for unsound constructs outside the sanctioned axiom module..."
424+
FOUND=$(grep -rn 'believe_me\|assert_total\|assert_smaller' --include='*.idr' src/ cartridges/ 2>/dev/null \
425+
| grep -v -- '--.*believe_me' | grep -v '|||.*believe_me' \
426+
| grep -v -- '--.*Admitted' | grep -v '|||.*Admitted' \
427+
| grep -v "^${AXIOM_FILE}:" || true)
413428
if [ -n "$FOUND" ]; then
414-
echo "CRITICAL: Found unsound constructs:"
429+
echo "CRITICAL: Found undocumented unsound constructs:"
415430
echo "$FOUND"
416431
exit 1
417432
fi
418-
echo "Zero believe_me — all proofs genuine!"
433+
AXIOM_COUNT=$(grep -c 'believe_me ()' "$AXIOM_FILE" 2>/dev/null || true)
434+
if [ "$AXIOM_COUNT" != "5" ]; then
435+
echo "CRITICAL: expected exactly 5 sanctioned class-(J) axioms in $AXIOM_FILE, found $AXIOM_COUNT."
436+
echo "If this change is intentional, update PROOF-NEEDS.md and docs/proof-debt.md to match."
437+
exit 1
438+
fi
439+
echo "OK: no undocumented unsound constructs; $AXIOM_COUNT sanctioned class-(J) axioms (all in SafetyLemmas.idr)."
419440
420441
# Full verification suite: type-check + zero believe_me + build + test
421442
verify: typecheck verify-no-believe-me build test

‎PROOF-NEEDS.md‎

Lines changed: 39 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -10,9 +10,45 @@
1010
> greps. Keep both in sync when the marker count in
1111
> `src/abi/Boj/SafetyLemmas.idr` changes.
1212
13-
## Current State (Updated 2026-05-18)
14-
15-
- **src/abi/Boj/**: 16 Idris2 ABI files
13+
## Build Verification (2026-06-03)
14+
15+
The full core ABI package now type-checks under the pinned toolchain
16+
(**Idris2 0.8.0**, Chez backend) — `cd src/abi && idris2 --typecheck boj.ipkg`
17+
builds all **17** modules clean. A re-verification on this date found six
18+
modules that the package build had never actually exercised (the `just
19+
typecheck` recipe used an invalid `--check --package boj boj.ipkg`
20+
invocation, and `CartridgeDispatch`/`APIContractCoverage` were absent from
21+
`boj.ipkg`). The fixes were purely in the proofs' construction — **theorem
22+
statements and the axiom budget are unchanged**:
23+
24+
- `CartridgeDispatch` — `with`-clause syntax (0.8.0 needs the full LHS or
25+
`_ |`); `dispatch` factored through a reducible helper so refused-
26+
completeness is provable; conjunction/`Uninhabited` lemmas replace the
27+
earlier `absurd` shortcuts.
28+
- `SafePromptInjection`, `SafeCORS` — `with`-abstraction rewrites the goal
29+
to `True = True`, so the residual obligations are `Refl`.
30+
- `SafeHTTP` — missing `Data.List.Elem`/`Data.Maybe` imports, `IsJust`→
31+
`isJust`, `all`→`allRec` (to match the `SafetyLemmas` lemmas), and
32+
explicit `{xs, ys}` binders (auto-generalised implicits are erased).
33+
- `SafeWebSocket` — `FrameSizeSafe` is now `FrameSizeSafeUpTo maxFrameSize`
34+
over a new bound-parameterised family. Baking the 16 MiB `maxFrameSize`
35+
literal directly into a constructor's `LTE` index forced it into a unary
36+
Nat and exhausted the elaborator; keeping the bound symbolic in the
37+
constructor (and applying it in a synonym) fixes this with no loss of
38+
strength.
39+
- `APIContractCoverage` — `representativeCatalogue` in a signature was being
40+
auto-bound as a fresh implicit (shadowing the global); fully qualified.
41+
- `SafetyLemmas` — added the constructive lemma `allTake` (used by the
42+
header/delimiter `take` proofs). No new axioms.
43+
44+
`just verify-no-believe-me` was also reconciled: it had enforced *zero*
45+
`believe_me`, which contradicts the sanctioned 5-axiom trusted base; it now
46+
permits exactly the 5 `%unsafe` class-(J) axioms in `SafetyLemmas.idr` and
47+
fails on anything else (or on axiom-count drift).
48+
49+
## Current State (Updated 2026-06-03)
50+
51+
- **src/abi/Boj/**: 17 Idris2 ABI files
1652
- **Dangerous patterns**: **5** `believe_me` invocations, **all** in
1753
`src/abi/Boj/SafetyLemmas.idr`, **all** classified `(J)` genuinely
1854
unavoidable (see audit table below). `logSafeBounded` (SafeAPIKey.idr)

‎src/abi/Boj/APIContractCoverage.idr‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -129,7 +129,7 @@ CartridgeHasProtocol c = NonEmpty (protocols c)
129129
||| non-empty concrete values.
130130
export
131131
repCatalogueProtocolCompliance :
132-
(c : Cartridge) -> Elem c representativeCatalogue -> CartridgeHasProtocol c
132+
(c : Cartridge) -> Elem c Boj.APIContractCoverage.representativeCatalogue -> CartridgeHasProtocol c
133133
repCatalogueProtocolCompliance _ Here = IsNonEmpty
134134
repCatalogueProtocolCompliance _ (There Here) = IsNonEmpty
135135
repCatalogueProtocolCompliance _ (There (There Here)) = IsNonEmpty
@@ -204,7 +204,7 @@ export bj3_proto_Fleet : ProtocolHasCartridge Fleet ; bj3_proto_Fleet = (f
204204
public export
205205
record BJ3Compliance where
206206
constructor MkBJ3Compliance
207-
protocolCompliance : (c : Cartridge) -> Elem c representativeCatalogue -> CartridgeHasProtocol c
207+
protocolCompliance : (c : Cartridge) -> Elem c Boj.APIContractCoverage.representativeCatalogue -> CartridgeHasProtocol c
208208
domainCoverage : (d : CapabilityDomain) ->
209209
Not (d = Dap) -> Not (d = Bsp) -> Not (d = CodeIntel) ->
210210
DomainHasReadyCartridge d

‎src/abi/Boj/CartridgeDispatch.idr‎

Lines changed: 90 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,45 @@ import Boj.Catalogue
3232

3333
%default total
3434

35+
-- ═══════════════════════════════════════════════════════════════════════════
36+
-- Boolean & Status Lemmas
37+
--
38+
-- `lookupCell` guards each cell with the conjunction
39+
-- `domain c == d && elem p (protocols c) && status c == Ready`.
40+
-- These lemmas let the dispatch invariants below extract each conjunct from a
41+
-- proof that the whole guard evaluated to True, without any axioms.
42+
-- ═══════════════════════════════════════════════════════════════════════════
43+
44+
||| From `a && b = True`, the left conjunct is True.
45+
andTrueLeft : (a : Bool) -> (b : Bool) -> (a && b) = True -> a = True
46+
andTrueLeft True _ _ = Refl
47+
andTrueLeft False _ prf = absurd prf
48+
49+
||| From `a && b = True`, the right conjunct is True.
50+
andTrueRight : (a : Bool) -> (b : Bool) -> (a && b) = True -> b = True
51+
andTrueRight True _ prf = prf
52+
andTrueRight False _ prf = absurd prf
53+
54+
||| Soundness of `==` against `Ready` for CartridgeStatus: the only status
55+
||| that compares equal to `Ready` is `Ready` itself.
56+
statusEqSoundReady : (s : CartridgeStatus) -> (s == Ready) = True -> s = Ready
57+
statusEqSoundReady Ready _ = Refl
58+
statusEqSoundReady Development prf = absurd prf
59+
statusEqSoundReady Deprecated prf = absurd prf
60+
statusEqSoundReady Faulty prf = absurd prf
61+
62+
-- Constructor disjointness for the `CartridgeStatus` lifecycle. `Ready` is a
63+
-- distinct constructor from every other state, so the corresponding equalities
64+
-- are uninhabited — proved by the absent `Refl` case, with no axioms.
65+
Uninhabited (Ready = Development) where
66+
uninhabited Refl impossible
67+
68+
Uninhabited (Ready = Deprecated) where
69+
uninhabited Refl impossible
70+
71+
Uninhabited (Ready = Faulty) where
72+
uninhabited Refl impossible
73+
3574
-- ═══════════════════════════════════════════════════════════════════════════
3675
-- Request and Dispatch Result Types
3776
-- ═══════════════════════════════════════════════════════════════════════════
@@ -66,12 +105,20 @@ data DispatchResult : DispatchRequest -> Type where
66105
-- Protocol Membership Lemmas
67106
-- ═══════════════════════════════════════════════════════════════════════════
68107

108+
||| Once the `foldl` accumulator of `elem` is True it stays True, regardless
109+
||| of the remaining list. `elem` is left-folded with `||`, so reducing
110+
||| `elem p (p :: ps)` exposes exactly this shape after `p == p` is known.
111+
orFoldlAccTrue : (q : ProtocolType -> Bool) -> (xs : List ProtocolType)
112+
-> foldl (\acc, e => acc || q e) True xs = True
113+
orFoldlAccTrue q [] = Refl
114+
orFoldlAccTrue q (y :: ys) = orFoldlAccTrue q ys
115+
69116
||| If a protocol is the head of the list, elem returns True.
70117
protocolElemHead : (p : ProtocolType) -> (ps : List ProtocolType)
71118
-> p `elem` (p :: ps) = True
72119
protocolElemHead p ps with (p == p) proof eq
73-
| True = Refl
74-
| False = absurd (elemSame p)
120+
protocolElemHead p ps | True = orFoldlAccTrue (p ==) ps
121+
protocolElemHead p ps | False = absurd (trans (sym eq) (elemSame p))
75122
where
76123
-- p == p = True for our Eq ProtocolType instance (all 9 cases reflexive)
77124
elemSame : (q : ProtocolType) -> q == q = True
@@ -112,10 +159,12 @@ protocolMatchInvariant :
112159
-> lookupCell p d cs = Just c
113160
-> p `elem` protocols c = True
114161
protocolMatchInvariant p d [] c eq = absurd eq
115-
protocolMatchInvariant p d (x :: xs) c eq with (domain x == d && elem p (protocols x) && status x == Ready)
116-
protocolMatchInvariant p d (x :: xs) x Refl | True with (elem p (protocols x)) proof ep
117-
protocolMatchInvariant p d (x :: xs) x Refl | True | True = Refl
118-
protocolMatchInvariant p d (x :: xs) x Refl | True | False = absurd ep
162+
protocolMatchInvariant p d (x :: xs) c eq with (domain x == d && elem p (protocols x) && status x == Ready) proof cond
163+
-- Guard held: `lookupCell` returned `Just x`, so `eq : Just x = Just c`
164+
-- forces `c = x`; the protocol conjunct is the left of the inner `&&`.
165+
protocolMatchInvariant p d (x :: xs) x Refl | True =
166+
andTrueLeft _ _ (andTrueRight _ _ cond)
167+
-- Guard failed: recurse on the tail with the same lookup proof.
119168
protocolMatchInvariant p d (x :: xs) c eq | False =
120169
protocolMatchInvariant p d xs c eq
121170

@@ -135,11 +184,11 @@ readinessGuard :
135184
-> status c = Ready
136185
readinessGuard p d [] c eq = absurd eq
137186
readinessGuard p d (x :: xs) c eq with (domain x == d && elem p (protocols x) && status x == Ready) proof cond
138-
readinessGuard p d (x :: xs) x Refl | True with (status x) proof st
139-
readinessGuard p d (x :: xs) x Refl | True | Ready = Refl
140-
readinessGuard p d (x :: xs) x Refl | True | Development = absurd cond
141-
readinessGuard p d (x :: xs) x Refl | True | Deprecated = absurd cond
142-
readinessGuard p d (x :: xs) x Refl | True | Faulty = absurd cond
187+
-- Guard held: `status x == Ready` is the right conjunct of the inner `&&`;
188+
-- `statusEqSoundReady` turns the boolean test into the propositional equality.
189+
readinessGuard p d (x :: xs) x Refl | True =
190+
statusEqSoundReady (status x) (andTrueRight _ _ (andTrueRight _ _ cond))
191+
-- Guard failed: recurse on the tail with the same lookup proof.
143192
readinessGuard p d (x :: xs) c eq | False =
144193
readinessGuard p d xs c eq
145194

@@ -172,15 +221,26 @@ lookupImpliesUnbreakable p d cs c eq =
172221
||| The type of the result guarantees (at compile time) that:
173222
||| - A Routed cartridge supports the requested protocol.
174223
||| - A Routed cartridge is in Ready status.
224+
||| Dispatch given the catalogue-lookup result *and* the proof that it is
225+
||| that result. Factoring this out of `dispatch` keeps the definition
226+
||| definitionally reducible on the lookup value — the refused-completeness
227+
||| theorem below relies on that, which a `with`-block definition would not
228+
||| provide.
229+
dispatchOn : (req : DispatchRequest) -> (cs : List Cartridge)
230+
-> (m : Maybe Cartridge)
231+
-> (lookupCell (reqProtocol req) (reqDomain req) cs = m)
232+
-> DispatchResult req
233+
dispatchOn req cs Nothing _ = Refused req
234+
dispatchOn req cs (Just c) prf =
235+
Routed c
236+
(lookupImpliesUnbreakable (reqProtocol req) (reqDomain req) cs c prf)
237+
req
238+
(protocolMatchInvariant (reqProtocol req) (reqDomain req) cs c prf)
239+
175240
export
176241
dispatch : (req : DispatchRequest) -> (cs : List Cartridge) -> DispatchResult req
177-
dispatch req cs with (lookupCell (reqProtocol req) (reqDomain req) cs) proof lk
178-
| Nothing = Refused req
179-
| Just c =
180-
Routed c
181-
(lookupImpliesUnbreakable (reqProtocol req) (reqDomain req) cs c lk)
182-
req
183-
(protocolMatchInvariant (reqProtocol req) (reqDomain req) cs c lk)
242+
dispatch req cs =
243+
dispatchOn req cs (lookupCell (reqProtocol req) (reqDomain req) cs) Refl
184244

185245
-- ═══════════════════════════════════════════════════════════════════════════
186246
-- Disjointness Theorem
@@ -231,8 +291,15 @@ refusedIfNoMatch :
231291
-> (cs : List Cartridge)
232292
-> lookupCell (reqProtocol req) (reqDomain req) cs = Nothing
233293
-> dispatch req cs = Refused req
234-
refusedIfNoMatch req cs noMatch with (dispatch req cs)
235-
| Refused _ = Refl
236-
| Routed c _ _ _ with (lookupCell (reqProtocol req) (reqDomain req) cs) proof lk
237-
| Nothing = absurd lk
238-
| Just _ = absurd noMatch
294+
refusedIfNoMatch req cs noMatch =
295+
lemma (lookupCell (reqProtocol req) (reqDomain req) cs) Refl noMatch
296+
where
297+
-- `dispatch req cs` is definitionally `dispatchOn req cs (lookupCell …) Refl`,
298+
-- so proving the goal for an arbitrary lookup result `m` (with its defining
299+
-- proof) and then instantiating at the real lookup value discharges it.
300+
lemma : (m : Maybe Cartridge)
301+
-> (prf : lookupCell (reqProtocol req) (reqDomain req) cs = m)
302+
-> m = Nothing
303+
-> dispatchOn req cs m prf = Refused req
304+
lemma Nothing _ _ = Refl
305+
lemma (Just c) _ eqN = absurd eqN

‎src/abi/Boj/SafeCORS.idr‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -141,8 +141,10 @@ decideCredentialSafe p with (p.allowCredentials) proof credPrf
141141
decideCredentialSafe p | True with (elem Boj.SafeCORS.wildcardOrigin p.allowedOrigins) proof elemPrf
142142
decideCredentialSafe p | True | False =
143143
Left (NoWildcard p {prf = falseImpliesNotTrue _ elemPrf})
144+
-- Both `with` scrutinees were rewritten to `True` in the goal, leaving the
145+
-- pair of reflexive obligations `(True = True, True = True)`.
144146
decideCredentialSafe p | True | True =
145-
Right (credPrf, elemPrf)
147+
Right (Refl, Refl)
146148

147149
export
148150
consOriginsValid : OriginValid o -> AllOriginsValid os -> AllOriginsValid (o :: os)
@@ -154,7 +156,7 @@ zeroMaxAgeReasonable = MkReasonableMaxAge 0 {prf = LTEZero}
154156

155157
export
156158
oneHourMaxAgeReasonable : ReasonableMaxAge 3600
157-
oneHourMaxAgeReasonable = MkReasonableMaxAge 3600 {prf = fromLteTrue 3600 86400 Refl}
159+
oneHourMaxAgeReasonable = MkReasonableMaxAge 3600 {prf = lteReflectsLTE 3600 86400 Refl}
158160

159161
--------------------------------------------------------------------------------
160162
-- Default Policies

0 commit comments

Comments
 (0)