diff --git a/Justfile b/Justfile index fe7780ea..c135586e 100644 --- a/Justfile +++ b/Justfile @@ -394,28 +394,49 @@ lint: verify-no-believe-me typecheck # ═══════════════════════════════════════════════════════════════════════════════ # Type-check all Idris2 ABI files +# NOTE: package type-checking uses `idris2 --typecheck .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 diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index 9fcf26d1..804470de 100644 --- a/PROOF-NEEDS.md +++ b/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) diff --git a/src/abi/Boj/APIContractCoverage.idr b/src/abi/Boj/APIContractCoverage.idr index 5999f24c..495d783e 100644 --- a/src/abi/Boj/APIContractCoverage.idr +++ b/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 diff --git a/src/abi/Boj/CartridgeDispatch.idr b/src/abi/Boj/CartridgeDispatch.idr index 8dcb989a..f363593d 100644 --- a/src/abi/Boj/CartridgeDispatch.idr +++ b/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 diff --git a/src/abi/Boj/SafeCORS.idr b/src/abi/Boj/SafeCORS.idr index a1f440c3..99b5503d 100644 --- a/src/abi/Boj/SafeCORS.idr +++ b/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 diff --git a/src/abi/Boj/SafeHTTP.idr b/src/abi/Boj/SafeHTTP.idr index eaf5c31c..6c39915b 100644 --- a/src/abi/Boj/SafeHTTP.idr +++ b/src/abi/Boj/SafeHTTP.idr @@ -16,6 +16,8 @@ module Boj.SafeHTTP import Data.List +import Data.List.Elem +import Data.Maybe import Data.Nat import Data.String import Boj.SafetyLemmas @@ -57,7 +59,7 @@ parseMethod _ = Nothing public export data ValidMethod : String -> Type where MkValidMethod : (s : String) -> - {auto prf : IsJust (parseMethod s) = True} -> + {auto prf : isJust (parseMethod s) = True} -> ValidMethod s -------------------------------------------------------------------------------- @@ -75,14 +77,14 @@ isHeaderUnsafe c = c == '\r' || c == '\n' || c == '\0' public export data HeaderCharsafe : List Char -> Type where MkHeaderCharsafe : (cs : List Char) -> - {auto prf : all (\c => not (isHeaderUnsafe c)) cs = True} -> + {auto prf : allRec (\c => not (isHeaderUnsafe c)) cs = True} -> HeaderCharsafe cs ||| Predicate: a header value (as String) contains no CRLF injection characters. public export data HeaderSafe : String -> Type where MkHeaderSafe : (s : String) -> - {auto prf : all (\c => not (isHeaderUnsafe c)) (unpack s) = True} -> + {auto prf : allRec (\c => not (isHeaderUnsafe c)) (unpack s) = True} -> HeaderSafe s ||| Theorem: the empty string is header-safe. @@ -97,29 +99,29 @@ nilIsHeaderCharsafe = MkHeaderCharsafe [] ||| Theorem: header char safety implies no carriage returns in the list. ||| Proof: '\r' makes isHeaderUnsafe True, so not (isHeaderUnsafe '\r') = False. -||| But all (\c => not (isHeaderUnsafe c)) cs = True means every char passes. +||| But allRec (\c => not (isHeaderUnsafe c)) cs = True means every char passes. ||| Therefore '\r' cannot be an element. export headerCharsafeNoCR : HeaderCharsafe cs -> Not (Elem '\r' cs) headerCharsafeNoCR (MkHeaderCharsafe cs {prf}) elemPrf = - let charFails : not (isHeaderUnsafe '\r') = True - charFails = allTrueElem {p = \c => not (isHeaderUnsafe c)} prf elemPrf + let charFails : (not (isHeaderUnsafe '\r') = True) + charFails = allTrueElem prf elemPrf in absurd charFails ||| Theorem: header char safety implies no line feeds in the list. export headerCharsafeNoLF : HeaderCharsafe cs -> Not (Elem '\n' cs) headerCharsafeNoLF (MkHeaderCharsafe cs {prf}) elemPrf = - let charFails : not (isHeaderUnsafe '\n') = True - charFails = allTrueElem {p = \c => not (isHeaderUnsafe c)} prf elemPrf + let charFails : (not (isHeaderUnsafe '\n') = True) + charFails = allTrueElem prf elemPrf in absurd charFails ||| Theorem: header char safety implies no null bytes in the list. export headerCharsafeNoNull : HeaderCharsafe cs -> Not (Elem '\0' cs) headerCharsafeNoNull (MkHeaderCharsafe cs {prf}) elemPrf = - let charFails : not (isHeaderUnsafe '\0') = True - charFails = allTrueElem {p = \c => not (isHeaderUnsafe c)} prf elemPrf + let charFails : (not (isHeaderUnsafe '\0') = True) + charFails = allTrueElem prf elemPrf in absurd charFails ||| Theorem: concatenating two header-char-safe lists produces a safe list. @@ -138,15 +140,15 @@ takeHeaderCharsafe (MkHeaderCharsafe cs {prf}) n = ||| Theorem: header char safety is preserved under splitting left. export -splitLeftHeaderCharsafe : HeaderCharsafe (xs ++ ys) -> HeaderCharsafe xs -splitLeftHeaderCharsafe (MkHeaderCharsafe _ {prf}) = - MkHeaderCharsafe xs {prf = allAppendLeft prf} +splitLeftHeaderCharsafe : {xs, ys : List Char} -> HeaderCharsafe (xs ++ ys) -> HeaderCharsafe xs +splitLeftHeaderCharsafe {xs} {ys} (MkHeaderCharsafe _ {prf}) = + MkHeaderCharsafe xs {prf = allAppendLeft {xs} {ys} prf} ||| Theorem: header char safety is preserved under splitting right. export -splitRightHeaderCharsafe : HeaderCharsafe (xs ++ ys) -> HeaderCharsafe ys -splitRightHeaderCharsafe (MkHeaderCharsafe _ {prf}) = - MkHeaderCharsafe ys {prf = allAppendRight prf} +splitRightHeaderCharsafe : {xs, ys : List Char} -> HeaderCharsafe (xs ++ ys) -> HeaderCharsafe ys +splitRightHeaderCharsafe {xs} {ys} (MkHeaderCharsafe _ {prf}) = + MkHeaderCharsafe ys {prf = allAppendRight {xs} {ys} prf} -------------------------------------------------------------------------------- -- Status Code Safety @@ -182,12 +184,14 @@ classifyStatus code = ||| Theorem: status code 200 is valid. export status200Valid : ValidStatus 200 -status200Valid = MkValidStatus 200 +status200Valid = MkValidStatus 200 {lower = lteReflectsLTE 100 200 Refl} + {upper = lteReflectsLTE 200 599 Refl} ||| Theorem: status code 404 is valid. export status404Valid : ValidStatus 404 -status404Valid = MkValidStatus 404 +status404Valid = MkValidStatus 404 {lower = lteReflectsLTE 100 404 Refl} + {upper = lteReflectsLTE 404 599 Refl} -------------------------------------------------------------------------------- -- Host Header Safety (works on List Char for provability) @@ -204,7 +208,7 @@ public export data HostCharsafe : List Char -> Type where MkHostCharsafe : (cs : List Char) -> {auto nonEmpty : NonEmpty cs} -> - {auto prf : all isHostChar cs = True} -> + {auto prf : allRec Boj.SafeHTTP.isHostChar cs = True} -> HostCharsafe cs ||| Predicate: a host value (as String) contains only valid hostname characters. @@ -212,17 +216,17 @@ public export data HostSafe : String -> Type where MkHostSafe : (s : String) -> {auto nonEmpty : NonEmpty (unpack s)} -> - {auto prf : all isHostChar (unpack s) = True} -> + {auto prf : allRec Boj.SafeHTTP.isHostChar (unpack s) = True} -> HostSafe s ||| Theorem: host char safety implies no spaces. ||| Proof: ' ' is not alphanumeric, not '-', '.', ':', '[', or ']', -||| so isHostChar ' ' = False. But all isHostChar cs = True +||| so isHostChar ' ' = False. But allRec Boj.SafeHTTP.isHostChar cs = True ||| means every char passes. Therefore ' ' cannot be in cs. export hostCharsafeNoSpace : HostCharsafe cs -> Not (Elem ' ' cs) hostCharsafeNoSpace (MkHostCharsafe cs {prf}) elemPrf = - let charFails : isHostChar ' ' = True + let charFails : (isHostChar ' ' = True) charFails = allTrueElem prf elemPrf in absurd charFails @@ -230,7 +234,7 @@ hostCharsafeNoSpace (MkHostCharsafe cs {prf}) elemPrf = export hostCharsafeNoNewline : HostCharsafe cs -> Not (Elem '\n' cs) hostCharsafeNoNewline (MkHostCharsafe cs {prf}) elemPrf = - let charFails : isHostChar '\n' = True + let charFails : (isHostChar '\n' = True) charFails = allTrueElem prf elemPrf in absurd charFails @@ -238,7 +242,7 @@ hostCharsafeNoNewline (MkHostCharsafe cs {prf}) elemPrf = export hostCharsafeNoCR : HostCharsafe cs -> Not (Elem '\r' cs) hostCharsafeNoCR (MkHostCharsafe cs {prf}) elemPrf = - let charFails : isHostChar '\r' = True + let charFails : (isHostChar '\r' = True) charFails = allTrueElem prf elemPrf in absurd charFails @@ -269,7 +273,7 @@ parseSafeContentType s = public export data ValidContentType : String -> Type where MkValidContentType : (s : String) -> - {auto prf : IsJust (parseSafeContentType s) = True} -> + {auto prf : isJust (parseSafeContentType s) = True} -> ValidContentType s -------------------------------------------------------------------------------- diff --git a/src/abi/Boj/SafePromptInjection.idr b/src/abi/Boj/SafePromptInjection.idr index 509a90c2..f02c3f12 100644 --- a/src/abi/Boj/SafePromptInjection.idr +++ b/src/abi/Boj/SafePromptInjection.idr @@ -49,7 +49,9 @@ decidePromptSafe : (s : String) -> (containsInjectionPattern s = True) decidePromptSafe s with (containsInjectionPattern s) proof prf decidePromptSafe s | False = Left (MkPromptSafe s {prf = prf}) - decidePromptSafe s | True = Right prf + -- `with` rewrote `containsInjectionPattern s` to `True` in the goal, so the + -- residual obligation is `True = True`. + decidePromptSafe s | True = Right Refl -------------------------------------------------------------------------------- -- Role Boundary Safety @@ -81,7 +83,8 @@ decideRoleBoundarySafe : (s : String) -> (isRoleBoundary s = True) decideRoleBoundarySafe s with (isRoleBoundary s) proof prf decideRoleBoundarySafe s | False = Left (MkRoleBoundarySafe s {prf = prf}) - decideRoleBoundarySafe s | True = Right prf + -- `with` rewrote `isRoleBoundary s` to `True` in the goal. + decideRoleBoundarySafe s | True = Right Refl -------------------------------------------------------------------------------- -- Delimiter Escape Safety diff --git a/src/abi/Boj/SafeWebSocket.idr b/src/abi/Boj/SafeWebSocket.idr index 6c84d4b3..2e397e36 100644 --- a/src/abi/Boj/SafeWebSocket.idr +++ b/src/abi/Boj/SafeWebSocket.idr @@ -121,34 +121,49 @@ public export maxControlFrameSize : Nat maxControlFrameSize = 125 +||| A frame whose payload length `n` is bounded by an arbitrary `bound`. +||| +||| The bound is a *parameter*, deliberately not a baked-in literal: keeping it +||| symbolic in the constructor's `LTE n bound` index stops the elaborator from +||| forcing the 16 MiB `maxFrameSize` into unary form at data-declaration time +||| (which exhausts memory in Idris2 0.8.0). The concrete data- and control-frame +||| predicates are recovered as nullary type synonyms below — `maxFrameSize` then +||| appears only in an *application* position, which the elaborator handles lazily. public export -data FrameSizeSafe : Nat -> Type where - MkFrameSizeSafe : (n : Nat) -> - {auto prf : LTE n Boj.SafeWebSocket.maxFrameSize} -> - FrameSizeSafe n +data FrameSizeSafeUpTo : (bound : Nat) -> Nat -> Type where + MkSizeSafe : (n : Nat) -> + {auto prf : LTE n bound} -> + FrameSizeSafeUpTo bound n +||| A data frame is size-safe when its length is within `maxFrameSize`. public export -data ControlFrameSizeSafe : Nat -> Type where - MkControlFrameSizeSafe : (n : Nat) -> - {auto prf : LTE n Boj.SafeWebSocket.maxControlFrameSize} -> - ControlFrameSizeSafe n +FrameSizeSafe : Nat -> Type +FrameSizeSafe = FrameSizeSafeUpTo Boj.SafeWebSocket.maxFrameSize + +||| A control frame is size-safe when its length is within `maxControlFrameSize`. +public export +ControlFrameSizeSafe : Nat -> Type +ControlFrameSizeSafe = FrameSizeSafeUpTo Boj.SafeWebSocket.maxControlFrameSize -export -controlImpliesFrameSafe : ControlFrameSizeSafe n -> FrameSizeSafe n ||| maxControlFrameSize (125) ≤ maxFrameSize (16 777 216). maxControlLeqMaxFrame : LTE Boj.SafeWebSocket.maxControlFrameSize Boj.SafeWebSocket.maxFrameSize -maxControlLeqMaxFrame = fromLteTrue 125 16777216 Refl +maxControlLeqMaxFrame = lteReflectsLTE 125 16777216 Refl -controlImpliesFrameSafe (MkControlFrameSizeSafe n {prf}) = - MkFrameSizeSafe n {prf = transitive prf maxControlLeqMaxFrame} +||| Control-frame size-safety implies data-frame size-safety: a payload within +||| the 125-byte control limit is a fortiori within the data-frame limit. Proved +||| by transitivity of `LTE` (bound weakening), not by re-checking the literal. +export +controlImpliesFrameSafe : ControlFrameSizeSafe n -> FrameSizeSafe n +controlImpliesFrameSafe (MkSizeSafe n {prf}) = + MkSizeSafe n {prf = transitive prf maxControlLeqMaxFrame} export emptyFrameSafe : FrameSizeSafe 0 -emptyFrameSafe = MkFrameSizeSafe 0 {prf = LTEZero} +emptyFrameSafe = MkSizeSafe 0 {prf = LTEZero} export emptyControlFrameSafe : ControlFrameSizeSafe 0 -emptyControlFrameSafe = MkControlFrameSizeSafe 0 {prf = LTEZero} +emptyControlFrameSafe = MkSizeSafe 0 {prf = LTEZero} -------------------------------------------------------------------------------- -- Origin Validation @@ -221,17 +236,17 @@ parseRoundtrips MessageTooBig = Refl parseRoundtrips InternalError = Refl ||| Every RFC 6455 close code lies in the range [1000, 1011]. -||| Proofs constructed via fromLteTrue on the closed-form values. +||| Proofs constructed via lteReflectsLTE on the closed-form values. export closeCodeInRange : (c : WSCloseCode) -> (LTE 1000 (closeCodeToNat c), LTE (closeCodeToNat c) 1011) -closeCodeInRange NormalClosure = (fromLteTrue 1000 1000 Refl, fromLteTrue 1000 1011 Refl) -closeCodeInRange GoingAway = (fromLteTrue 1000 1001 Refl, fromLteTrue 1001 1011 Refl) -closeCodeInRange ProtocolError = (fromLteTrue 1000 1002 Refl, fromLteTrue 1002 1011 Refl) -closeCodeInRange UnsupportedData = (fromLteTrue 1000 1003 Refl, fromLteTrue 1003 1011 Refl) -closeCodeInRange InvalidPayload = (fromLteTrue 1000 1007 Refl, fromLteTrue 1007 1011 Refl) -closeCodeInRange PolicyViolation = (fromLteTrue 1000 1008 Refl, fromLteTrue 1008 1011 Refl) -closeCodeInRange MessageTooBig = (fromLteTrue 1000 1009 Refl, fromLteTrue 1009 1011 Refl) -closeCodeInRange InternalError = (fromLteTrue 1000 1011 Refl, fromLteTrue 1011 1011 Refl) +closeCodeInRange NormalClosure = (lteReflectsLTE 1000 1000 Refl, lteReflectsLTE 1000 1011 Refl) +closeCodeInRange GoingAway = (lteReflectsLTE 1000 1001 Refl, lteReflectsLTE 1001 1011 Refl) +closeCodeInRange ProtocolError = (lteReflectsLTE 1000 1002 Refl, lteReflectsLTE 1002 1011 Refl) +closeCodeInRange UnsupportedData = (lteReflectsLTE 1000 1003 Refl, lteReflectsLTE 1003 1011 Refl) +closeCodeInRange InvalidPayload = (lteReflectsLTE 1000 1007 Refl, lteReflectsLTE 1007 1011 Refl) +closeCodeInRange PolicyViolation = (lteReflectsLTE 1000 1008 Refl, lteReflectsLTE 1008 1011 Refl) +closeCodeInRange MessageTooBig = (lteReflectsLTE 1000 1009 Refl, lteReflectsLTE 1009 1011 Refl) +closeCodeInRange InternalError = (lteReflectsLTE 1000 1011 Refl, lteReflectsLTE 1011 1011 Refl) -------------------------------------------------------------------------------- -- Message Ordering @@ -247,12 +262,12 @@ data InOrder : WSSequence -> WSSequence -> Type where MkInOrder : {auto prf : LT a.seqNum b.seqNum} -> InOrder a b export -inOrderTrans : InOrder a b -> InOrder b c -> InOrder a c +inOrderTrans : {a, b, c : WSSequence} -> InOrder a b -> InOrder b c -> InOrder a c inOrderTrans (MkInOrder {prf = ab}) (MkInOrder {prf = bc}) = MkInOrder {prf = transitive (lteSuccRight ab) bc} export -inOrderIrreflexive : Not (InOrder a a) +inOrderIrreflexive : {a : WSSequence} -> Not (InOrder a a) inOrderIrreflexive (MkInOrder {prf}) = absurd (succNotLTEpred a.seqNum prf) where succNotLTEpred : (n : Nat) -> LTE (S n) n -> Void diff --git a/src/abi/Boj/SafetyLemmas.idr b/src/abi/Boj/SafetyLemmas.idr index 29fc7ef4..c20b0dcd 100644 --- a/src/abi/Boj/SafetyLemmas.idr +++ b/src/abi/Boj/SafetyLemmas.idr @@ -118,6 +118,17 @@ allAppendBoth {p} {xs = x :: xs'} pX pY with (p x) proof eq allAppendBoth {p} {xs = x :: xs'} pX pY | True = allAppendBoth {xs = xs'} pX pY allAppendBoth {p} {xs = x :: xs'} pX pY | False = absurd pX +||| `allRec p` is preserved by `take`: a prefix of a list all of whose +||| elements satisfy `p` also has all elements satisfying `p`. +export +allTake : {p : a -> Bool} -> {n : Nat} -> {xs : List a} -> + allRec p xs = True -> allRec p (take n xs) = True +allTake {n = Z} _ = Refl +allTake {n = S k} {xs = []} _ = Refl +allTake {n = S k} {xs = x :: xs'} prf with (p x) proof eq + allTake {n = S k} {xs = x :: xs'} prf | True = allTake {n = k} {xs = xs'} prf + allTake {n = S k} {xs = x :: xs'} prf | False = absurd prf + ||| If `allRec p xs` holds, then for any predicate q that is implied by p, ||| `allRec q xs` holds. export diff --git a/src/abi/boj.ipkg b/src/abi/boj.ipkg index 3b54a77d..0a719485 100644 --- a/src/abi/boj.ipkg +++ b/src/abi/boj.ipkg @@ -26,6 +26,8 @@ modules = Boj.Protocol , Boj.SafeAPIKey , Boj.CredentialIsolation , Boj.SafeWebSocket + , Boj.CartridgeDispatch + , Boj.APIContractCoverage depends = base , contrib diff --git a/verification/proofs/README.adoc b/verification/proofs/README.adoc index 07e82bfb..b724bbb0 100644 --- a/verification/proofs/README.adoc +++ b/verification/proofs/README.adoc @@ -6,6 +6,17 @@ Formally verified properties of the BoJ server ABI layer. All proofs are written in Idris2 and live in `src/abi/Boj/`. +[NOTE] +==== +*Build status (2026-06-03):* the full package type-checks under the pinned +toolchain — `cd src/abi && idris2 --typecheck boj.ipkg` builds all 17 modules +clean on Idris2 0.8.0 (Chez backend), the only `believe_me` being the 5 +sanctioned class-(J) axioms in `SafetyLemmas.idr`. `CartridgeDispatch` and +`APIContractCoverage` are now listed in `boj.ipkg` (previously omitted, so the +package build never checked them). See `PROOF-NEEDS.md` -> _Build Verification_ +for the per-module reconciliation. +==== + == Proof Inventory [cols="2,3,1,1"]