From 122ac5c135f83fbef201fc9f465855a3569ee7a9 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 27 May 2026 09:16:12 +0100 Subject: [PATCH] docs(proof-debt): add canonical AXIOM: annotations to SafetyLemmas.idr MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Apply the estate Trusted-Base Reduction Policy (standards#203) inline annotation convention to the 5 class-(J) believe_me sites in src/abi/Boj/SafetyLemmas.idr. Each previously had a prose "Axiomatic:" doc-comment which is informative but not picked up by the canonical scripts/check-trusted-base.sh grep (standards#211) — that script recognises TRUSTED: / AXIOM: / OWED: keywords. Updates: - 5 doc-comments on charEqSound / charEqSym / unpackLength / appendLengthSum / substrLengthBound get an AXIOM: header line citing docs/proof-debt.md §(c) and the per-primitive docs/backend-assurance/ file. boj-server now satisfies BOTH halves of the check (inline + docs/proof-debt.md enumeration), making it the fully canonical reference implementation cited in standards#203 §"Precedent". - Module-header summary updated from "Five axiomatic believe_me" to "Five AXIOM-tagged believe_me primitives ... disposition-§(c) NECESSARY-AXIOM" so it matches the policy vocabulary. - PROOF-NEEDS.md gets a header note cross-linking docs/proof-debt.md (strategic-goals doc ↔ schema-conformant per-repo index) per the standards#213 seed pattern. Marker inventory unchanged: 5 markers, all §(c) NECESSARY AXIOM, all externally validated via docs/backend-assurance/. docs/proof-debt.md (landed in PR#161) already enumerates them and remains the source of truth. Refs: hyperpolymath/standards#203, hyperpolymath/standards#211, hyperpolymath/boj-server#161 Co-Authored-By: Claude Opus 4.7 (1M context) --- PROOF-NEEDS.md | 10 ++++++++++ src/abi/Boj/SafetyLemmas.idr | 38 +++++++++++++++++++++++++----------- 2 files changed, 37 insertions(+), 11 deletions(-) diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index aa4eea6e..9fcf26d1 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -1,5 +1,15 @@ # PROOF-NEEDS.md — boj-server +> **See also**: [`docs/proof-debt.md`](docs/proof-debt.md) is the +> schema-conformant per-repo index under the estate +> [Trusted-Base Reduction Policy](https://github.com/hyperpolymath/standards/blob/main/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc) +> (standards#203, enforcement standards#211). PROOF-NEEDS.md is the +> *strategic-goals* narrative — full audit table, classification +> rationale, and external-validation pointers. `docs/proof-debt.md` is +> the *machine-checked* index that `scripts/check-trusted-base.sh` +> 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 diff --git a/src/abi/Boj/SafetyLemmas.idr b/src/abi/Boj/SafetyLemmas.idr index fbe15d21..29fc7ef4 100644 --- a/src/abi/Boj/SafetyLemmas.idr +++ b/src/abi/Boj/SafetyLemmas.idr @@ -6,12 +6,15 @@ ||| proofs in SafeHTTP, SafeCORS, SafeWebSocket, SafePromptInjection, ||| SafeAPIKey, and Safety modules. ||| -||| 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 +||| Five AXIOM-tagged believe_me primitives are declared here (per the +||| estate trusted-base reduction policy — hyperpolymath/standards#203). +||| 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. +||| principle. They are documented as principled disposition-§(c) +||| NECESSARY-AXIOM assumptions, not unproven debt; see +||| `docs/proof-debt.md` (schema-conformant index) and `PROOF-NEEDS.md` +||| (audit narrative) for the per-site disposition. ||| ||| charEqSound — soundness of prim__eqChar (c1 == c2 = True → c1 = c2) ||| charEqSym — symmetry of prim__eqChar (x == y = y == x) @@ -54,14 +57,19 @@ notTrueNotTrue : not True = True -> Void notTrueNotTrue Refl impossible ||| Primitive char equality soundness: c1 == c2 = True implies c1 = c2. -||| Axiomatic: correctness of Idris2's prim__eqChar backend primitive. +||| AXIOM: charEqSound; class-(J) — correctness of Idris2's prim__eqChar +||| backend primitive. `Char` is an opaque primitive; no in-language +||| induction principle exists in Idris2 0.8.0. See docs/proof-debt.md §(c) +||| and docs/backend-assurance/prim__eqChar.md for external validation. %unsafe export charEqSound : (c1, c2 : Char) -> c1 == c2 = True -> c1 = c2 charEqSound _ _ _ = believe_me () ||| Helper: symmetry of Char equality. -||| Axiomatic: symmetry of prim__eqChar on the BEAM/Chez backend. +||| AXIOM: charEqSym; class-(J) — symmetry of prim__eqChar on the BEAM/Chez +||| backend. Same root cause as charEqSound. See docs/proof-debt.md §(c) +||| and docs/backend-assurance/prim__eqChar.md. %unsafe export charEqSym : (x, y : Char) -> (x == y) = (y == x) @@ -212,22 +220,30 @@ allNeqImpliesNotElem {target} {xs = x :: xs'} prf with (x == target) proof xEq -------------------------------------------------------------------------------- ||| `unpack s` has the same length as `s`. -||| Axiomatic: prim__strToCharList preserves length (backend primitive guarantee). +||| AXIOM: unpackLength; class-(J) — prim__strToCharList preserves length +||| (backend primitive guarantee). `String` is opaque with no induction +||| principle. See docs/proof-debt.md §(c) and +||| docs/backend-assurance/prim__strToCharList.md for external validation. %unsafe export unpackLength : (s : String) -> length (unpack s) = length s unpackLength _ = believe_me () ||| String concatenation length equals the sum of both argument lengths. -||| Axiomatic: prim__strAppend is a backend primitive not reducible at the -||| Idris2 type level. Established by semantics of all supported backends. +||| AXIOM: appendLengthSum; class-(J) — prim__strAppend is a backend +||| primitive not reducible at the Idris2 type level. Established by +||| semantics of all supported backends. See docs/proof-debt.md §(c) and +||| docs/backend-assurance/prim__strAppend.md for external validation. %unsafe export 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`. +||| AXIOM: substrLengthBound; class-(J) — prim__strSubstr semantics: result +||| is never longer than `len`. Backend primitive guarantee with no in- +||| language proof. See docs/proof-debt.md §(c) and +||| docs/backend-assurance/prim__strSubstr.md for external validation. %unsafe export substrLengthBound : (s : String) -> (start, len : Nat) -> LTE (length (substr start len s)) len