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

Justfile

@@ -394,28 +394,49 @@ lint: verify-no-believe-me typecheck
 # ═══════════════════════════════════════════════════════════════════════════════
 
 # Type-check all Idris2 ABI files
+# NOTE: package type-checking uses `idris2 --typecheck <pkg>.ipkg` (the prior
+# `--check --package boj boj.ipkg` form is invalid — `--check` is for .idr
+# files and `--package` looks up an *installed* package, so it never ran).
 typecheck:
-    @echo "Type-checking core ABI..."
-    cd src/abi && idris2 --check --package boj boj.ipkg
+    @echo "Type-checking core ABI (17 modules)..."
+    cd src/abi && idris2 --typecheck boj.ipkg
     @echo "Type-checking cartridge ABIs..."
-    cd cartridges/fleet-mcp/abi && idris2 --check fleet-mcp.ipkg
-    cd cartridges/nesy-mcp/abi && idris2 --check nesy-mcp.ipkg
-    cd cartridges/database-mcp/abi && idris2 --check database-mcp.ipkg
-    cd cartridges/agent-mcp/abi && idris2 --check agent-mcp.ipkg
-    cd cartridges/feedback-mcp/abi && idris2 --check feedback-mcp.ipkg
+    cd cartridges/fleet-mcp/abi && idris2 --typecheck fleet-mcp.ipkg
+    cd cartridges/nesy-mcp/abi && idris2 --typecheck nesy-mcp.ipkg
+    cd cartridges/database-mcp/abi && idris2 --typecheck database-mcp.ipkg
+    cd cartridges/agent-mcp/abi && idris2 --typecheck agent-mcp.ipkg
+    cd cartridges/feedback-mcp/abi && idris2 --typecheck feedback-mcp.ipkg
     @echo "All ABI files type-check!"
 
-# Verify zero believe_me in all Idris2 sources
+# Verify the trusted base: no unsound constructs beyond the sanctioned axioms.
+#
+# The estate trusted-base reduction policy (hyperpolymath/standards#203) sanctions
+# EXACTLY the 5 class-(J) axioms in src/abi/Boj/SafetyLemmas.idr — opaque Char/String
+# primitives, %unsafe-tagged and externally validated (see PROOF-NEEDS.md and
+# docs/proof-debt.md). Everything else must be a genuine constructive proof.
+# This recipe fails on any believe_me/assert_* outside that module, and also
+# fails if the audited axiom count drifts from 5 (keep the docs in sync).
 verify-no-believe-me:
     #!/usr/bin/env bash
-    echo "Scanning for believe_me..."
-    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)
+    set -euo pipefail
+    AXIOM_FILE="src/abi/Boj/SafetyLemmas.idr"
+    echo "Scanning for unsound constructs outside the sanctioned axiom module..."
+    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' \
+        | grep -v "^${AXIOM_FILE}:" || true)
     if [ -n "$FOUND" ]; then
-        echo "CRITICAL: Found unsound constructs:"
+        echo "CRITICAL: Found undocumented unsound constructs:"
         echo "$FOUND"
         exit 1
     fi
-    echo "Zero believe_me — all proofs genuine!"
+    AXIOM_COUNT=$(grep -c 'believe_me ()' "$AXIOM_FILE" 2>/dev/null || true)
+    if [ "$AXIOM_COUNT" != "5" ]; then
+        echo "CRITICAL: expected exactly 5 sanctioned class-(J) axioms in $AXIOM_FILE, found $AXIOM_COUNT."
+        echo "If this change is intentional, update PROOF-NEEDS.md and docs/proof-debt.md to match."
+        exit 1
+    fi
+    echo "OK: no undocumented unsound constructs; $AXIOM_COUNT sanctioned class-(J) axioms (all in SafetyLemmas.idr)."
 
 # Full verification suite: type-check + zero believe_me + build + test
 verify: typecheck verify-no-believe-me build test

PROOF-NEEDS.md

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

src/abi/Boj/APIContractCoverage.idr

@@ -129,7 +129,7 @@ CartridgeHasProtocol c = NonEmpty (protocols c)
 ||| non-empty concrete values.
 export
 repCatalogueProtocolCompliance :
-  (c : Cartridge) -> Elem c representativeCatalogue -> CartridgeHasProtocol c
+  (c : Cartridge) -> Elem c Boj.APIContractCoverage.representativeCatalogue -> CartridgeHasProtocol c
 repCatalogueProtocolCompliance _ Here                                                              = IsNonEmpty
 repCatalogueProtocolCompliance _ (There Here)                                                      = IsNonEmpty
 repCatalogueProtocolCompliance _ (There (There Here))                                              = IsNonEmpty
@@ -204,7 +204,7 @@ export bj3_proto_Fleet   : ProtocolHasCartridge Fleet   ; bj3_proto_Fleet   = (f
 public export
 record BJ3Compliance where
   constructor MkBJ3Compliance
-  protocolCompliance : (c : Cartridge) -> Elem c representativeCatalogue -> CartridgeHasProtocol c
+  protocolCompliance : (c : Cartridge) -> Elem c Boj.APIContractCoverage.representativeCatalogue -> CartridgeHasProtocol c
   domainCoverage     : (d : CapabilityDomain) ->
                        Not (d = Dap) -> Not (d = Bsp) -> Not (d = CodeIntel) ->
                        DomainHasReadyCartridge d

src/abi/Boj/CartridgeDispatch.idr

@@ -32,6 +32,45 @@ import Boj.Catalogue
 
 %default total
 
+-- ═══════════════════════════════════════════════════════════════════════════
+-- Boolean & Status Lemmas
+--
+-- `lookupCell` guards each cell with the conjunction
+--   `domain c == d && elem p (protocols c) && status c == Ready`.
+-- These lemmas let the dispatch invariants below extract each conjunct from a
+-- proof that the whole guard evaluated to True, without any axioms.
+-- ═══════════════════════════════════════════════════════════════════════════
+
+||| From `a && b = True`, the left conjunct is True.
+andTrueLeft : (a : Bool) -> (b : Bool) -> (a && b) = True -> a = True
+andTrueLeft True  _ _   = Refl
+andTrueLeft False _ prf = absurd prf
+
+||| From `a && b = True`, the right conjunct is True.
+andTrueRight : (a : Bool) -> (b : Bool) -> (a && b) = True -> b = True
+andTrueRight True  _ prf = prf
+andTrueRight False _ prf = absurd prf
+
+||| Soundness of `==` against `Ready` for CartridgeStatus: the only status
+||| that compares equal to `Ready` is `Ready` itself.
+statusEqSoundReady : (s : CartridgeStatus) -> (s == Ready) = True -> s = Ready
+statusEqSoundReady Ready       _   = Refl
+statusEqSoundReady Development prf = absurd prf
+statusEqSoundReady Deprecated  prf = absurd prf
+statusEqSoundReady Faulty      prf = absurd prf
+
+-- Constructor disjointness for the `CartridgeStatus` lifecycle. `Ready` is a
+-- distinct constructor from every other state, so the corresponding equalities
+-- are uninhabited — proved by the absent `Refl` case, with no axioms.
+Uninhabited (Ready = Development) where
+  uninhabited Refl impossible
+
+Uninhabited (Ready = Deprecated) where
+  uninhabited Refl impossible
+
+Uninhabited (Ready = Faulty) where
+  uninhabited Refl impossible
+
 -- ═══════════════════════════════════════════════════════════════════════════
 -- Request and Dispatch Result Types
 -- ═══════════════════════════════════════════════════════════════════════════
@@ -66,12 +105,20 @@ data DispatchResult : DispatchRequest -> Type where
 -- Protocol Membership Lemmas
 -- ═══════════════════════════════════════════════════════════════════════════
 
+||| Once the `foldl` accumulator of `elem` is True it stays True, regardless
+||| of the remaining list. `elem` is left-folded with `||`, so reducing
+||| `elem p (p :: ps)` exposes exactly this shape after `p == p` is known.
+orFoldlAccTrue : (q : ProtocolType -> Bool) -> (xs : List ProtocolType)
+              -> foldl (\acc, e => acc || q e) True xs = True
+orFoldlAccTrue q []        = Refl
+orFoldlAccTrue q (y :: ys) = orFoldlAccTrue q ys
+
 ||| If a protocol is the head of the list, elem returns True.
 protocolElemHead : (p : ProtocolType) -> (ps : List ProtocolType)
                 -> p `elem` (p :: ps) = True
 protocolElemHead p ps with (p == p) proof eq
-  | True  = Refl
-  | False = absurd (elemSame p)
+  protocolElemHead p ps | True  = orFoldlAccTrue (p ==) ps
+  protocolElemHead p ps | False = absurd (trans (sym eq) (elemSame p))
   where
     -- p == p = True for our Eq ProtocolType instance (all 9 cases reflexive)
     elemSame : (q : ProtocolType) -> q == q = True
@@ -112,10 +159,12 @@ protocolMatchInvariant :
   -> lookupCell p d cs = Just c
   -> p `elem` protocols c = True
 protocolMatchInvariant p d [] c eq = absurd eq
-protocolMatchInvariant p d (x :: xs) c eq with (domain x == d && elem p (protocols x) && status x == Ready)
-  protocolMatchInvariant p d (x :: xs) x Refl | True with (elem p (protocols x)) proof ep
-    protocolMatchInvariant p d (x :: xs) x Refl | True | True = Refl
-    protocolMatchInvariant p d (x :: xs) x Refl | True | False = absurd ep
+protocolMatchInvariant p d (x :: xs) c eq with (domain x == d && elem p (protocols x) && status x == Ready) proof cond
+  -- Guard held: `lookupCell` returned `Just x`, so `eq : Just x = Just c`
+  -- forces `c = x`; the protocol conjunct is the left of the inner `&&`.
+  protocolMatchInvariant p d (x :: xs) x Refl | True =
+    andTrueLeft _ _ (andTrueRight _ _ cond)
+  -- Guard failed: recurse on the tail with the same lookup proof.
   protocolMatchInvariant p d (x :: xs) c eq | False =
     protocolMatchInvariant p d xs c eq
 
@@ -135,11 +184,11 @@ readinessGuard :
   -> status c = Ready
 readinessGuard p d [] c eq = absurd eq
 readinessGuard p d (x :: xs) c eq with (domain x == d && elem p (protocols x) && status x == Ready) proof cond
-  readinessGuard p d (x :: xs) x Refl | True with (status x) proof st
-    readinessGuard p d (x :: xs) x Refl | True | Ready      = Refl
-    readinessGuard p d (x :: xs) x Refl | True | Development = absurd cond
-    readinessGuard p d (x :: xs) x Refl | True | Deprecated  = absurd cond
-    readinessGuard p d (x :: xs) x Refl | True | Faulty      = absurd cond
+  -- Guard held: `status x == Ready` is the right conjunct of the inner `&&`;
+  -- `statusEqSoundReady` turns the boolean test into the propositional equality.
+  readinessGuard p d (x :: xs) x Refl | True =
+    statusEqSoundReady (status x) (andTrueRight _ _ (andTrueRight _ _ cond))
+  -- Guard failed: recurse on the tail with the same lookup proof.
   readinessGuard p d (x :: xs) c eq | False =
     readinessGuard p d xs c eq
 
@@ -172,15 +221,26 @@ lookupImpliesUnbreakable p d cs c eq =
 ||| The type of the result guarantees (at compile time) that:
 |||   - A Routed cartridge supports the requested protocol.
 |||   - A Routed cartridge is in Ready status.
+||| Dispatch given the catalogue-lookup result *and* the proof that it is
+||| that result. Factoring this out of `dispatch` keeps the definition
+||| definitionally reducible on the lookup value — the refused-completeness
+||| theorem below relies on that, which a `with`-block definition would not
+||| provide.
+dispatchOn : (req : DispatchRequest) -> (cs : List Cartridge)
+          -> (m : Maybe Cartridge)
+          -> (lookupCell (reqProtocol req) (reqDomain req) cs = m)
+          -> DispatchResult req
+dispatchOn req cs Nothing  _   = Refused req
+dispatchOn req cs (Just c) prf =
+    Routed c
+      (lookupImpliesUnbreakable (reqProtocol req) (reqDomain req) cs c prf)
+      req
+      (protocolMatchInvariant (reqProtocol req) (reqDomain req) cs c prf)
+
 export
 dispatch : (req : DispatchRequest) -> (cs : List Cartridge) -> DispatchResult req
-dispatch req cs with (lookupCell (reqProtocol req) (reqDomain req) cs) proof lk
-  | Nothing = Refused req
-  | Just c  =
-      Routed c
-        (lookupImpliesUnbreakable (reqProtocol req) (reqDomain req) cs c lk)
-        req
-        (protocolMatchInvariant (reqProtocol req) (reqDomain req) cs c lk)
+dispatch req cs =
+  dispatchOn req cs (lookupCell (reqProtocol req) (reqDomain req) cs) Refl
 
 -- ═══════════════════════════════════════════════════════════════════════════
 -- Disjointness Theorem
@@ -231,8 +291,15 @@ refusedIfNoMatch :
   -> (cs  : List Cartridge)
   -> lookupCell (reqProtocol req) (reqDomain req) cs = Nothing
   -> dispatch req cs = Refused req
-refusedIfNoMatch req cs noMatch with (dispatch req cs)
-  | Refused _ = Refl
-  | Routed c _ _ _ with (lookupCell (reqProtocol req) (reqDomain req) cs) proof lk
-    | Nothing = absurd lk
-    | Just _  = absurd noMatch
+refusedIfNoMatch req cs noMatch =
+    lemma (lookupCell (reqProtocol req) (reqDomain req) cs) Refl noMatch
+  where
+    -- `dispatch req cs` is definitionally `dispatchOn req cs (lookupCell …) Refl`,
+    -- so proving the goal for an arbitrary lookup result `m` (with its defining
+    -- proof) and then instantiating at the real lookup value discharges it.
+    lemma : (m : Maybe Cartridge)
+         -> (prf : lookupCell (reqProtocol req) (reqDomain req) cs = m)
+         -> m = Nothing
+         -> dispatchOn req cs m prf = Refused req
+    lemma Nothing  _ _   = Refl
+    lemma (Just c) _ eqN = absurd eqN

src/abi/Boj/SafeCORS.idr

@@ -141,8 +141,10 @@ decideCredentialSafe p with (p.allowCredentials) proof credPrf
   decideCredentialSafe p | True with (elem Boj.SafeCORS.wildcardOrigin p.allowedOrigins) proof elemPrf
     decideCredentialSafe p | True | False =
       Left (NoWildcard p {prf = falseImpliesNotTrue _ elemPrf})
+    -- Both `with` scrutinees were rewritten to `True` in the goal, leaving the
+    -- pair of reflexive obligations `(True = True, True = True)`.
     decideCredentialSafe p | True | True =
-      Right (credPrf, elemPrf)
+      Right (Refl, Refl)
 
 export
 consOriginsValid : OriginValid o -> AllOriginsValid os -> AllOriginsValid (o :: os)
@@ -154,7 +156,7 @@ zeroMaxAgeReasonable = MkReasonableMaxAge 0 {prf = LTEZero}
 
 export
 oneHourMaxAgeReasonable : ReasonableMaxAge 3600
-oneHourMaxAgeReasonable = MkReasonableMaxAge 3600 {prf = fromLteTrue 3600 86400 Refl}
+oneHourMaxAgeReasonable = MkReasonableMaxAge 3600 {prf = lteReflectsLTE 3600 86400 Refl}
 
 --------------------------------------------------------------------------------
 -- Default Policies