From dce0473013f232e4d0bd76b62cc6899b2ca3522a Mon Sep 17 00:00:00 2001 From: mrwulf Date: Mon, 27 Jul 2026 22:57:46 +0200 Subject: [PATCH] review round 5: bind the policy, the specification bodies, and the harness MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The third reviewer demonstrated that the round-4 gate was closed at the EXPLOITS, not the MECHANISMS: it bound the manifest rows while the things he moved sat outside the binding. Three fail-opens, each executed end-to-end with the button printing ALL GREEN. No theorem, proof, fold, or model body changed. NEW-1 — the policy constant was unbound. `manifestFingerprint` covered `manifest` but never `allowedBoundary`, the sole predicate the enumeration tests against; adding one name re-opened the False-proof with the committed fingerprint BYTE-IDENTICAL. NEW-2 — the specification bodies were unbound. The statement fingerprint pinned each certificate's TYPE, which names its reference fold; redefining that fold to *be* the extracted loop left cone and type-hash identical while the certificate degenerated to `loop = loop`. 100% of the fidelity content lives in those defs. NEW-3 — the harness was unbound. Stubbing verification/lean-guard alone, without touching check.sh or the proofs, gave ALL GREEN in 3.6s over destroyed proofs. FIX — one mechanism rather than three patches. Audit.lean now emits a canonical AUDIT-MANIFEST block and check.sh binds to its SHA-256. The block covers the POLICY constants, every certificate's fully-elaborated statement, and every specification constant transitively reachable from those statements with its fully-elaborated BODY (41 constants; the closure is computed, so a new fold cannot appear without moving the digest; Prop-valued constants contribute their statement, by proof irrelevance). This also retires the 32-bit Expr.hash as the binding (NEW-5) — it survives only as a per-certificate diagnostic. Enumeration now covers EVERY declaration kind (a `def : False` passed before) in the eight certificate modules AND in Audit.lean itself — the auditor is no longer exempt (round-5 R1). A bare `axiom` in audited scope is now an error. Phase 0 purges stale .olean (the verdict must depend on committed bytes, not .gitignored build state — NEW-4), forbids any .lean outside gen/ and Proofs/, and sha256-pins the four model files AND lean-guard. lean-guard is KEPT rather than removed (the reviewer's portability advice is declined by operator decision): it is the memory cap and machine-wide lock that protect the build machine after a 12.2GB OOM took the host down. That trade-off is documented. check.sh's "Certificates proven:" line now comes from the audited manifest; the hand-kept CERTS array — the one authoritative claim string nothing bound — is deleted. check-selftest.sh: 14 attacks, all rejected, plus a check that the hashed block literally carries the twelve fold bodies. Attacks 9-14 are the reviewers' and an independent drill's own exploits, turned into regression tests. DOCS. TRUSTED-BASE gains item 11 (the REAL trusted computing base — lean-guard pinned; check.sh, the toolchain env, $AENEAS_HOME, python3 and Lean still trusted) and item 12 (the apex does not compose the ten). README: the audit description rewritten; the XMSS sibling-order claim downgraded from "pins" to "makes visible", with a new blanket non-claim covering all ten loop certificates; the de-plumbing file claim corrected (round 1 touched only verify_mono.rs, round 2 only helpers.rs — which is ON the deployed verify AND sign paths, now disclosed; wots.rs was never patched). RECORDED-RUN: three lines that stood inside a fence were a hand-written summary, not console output — fabricated evidence in the file whose purpose is machine evidence. They are removed and the fabrication is named in place, together with the correction that the "INDEPENDENT RUN" block predates this gate. New rule: nothing goes in a fence unless captured with tee/cat, and every block states its date, pin, and who ran it. The transcripts added here follow it. Also disclosed rather than buried: three bugs in my own test harness this round (an olean-purge build-order break, an attack rejected by the wrong rule, and a coverage assertion looking on the wrong line) — each would have let an attack pass or fail for an unrelated reason. Co-Authored-By: Claude Opus 4.8 --- README.md | 83 +++-- TRUSTED-BASE.md | 27 ++ verification/PROVENANCE.json | 23 +- verification/Proofs/Audit.lean | 231 +++++++++----- verification/RECORDED-RUN.md | 116 ++++++- verification/check-selftest.sh | 308 +++++++++++++------ verification/check.sh | 115 ++++--- verification/gen/SlhVerify/FunsExternal.lean | 21 +- 8 files changed, 669 insertions(+), 255 deletions(-) diff --git a/README.md b/README.md index a5a38cc..0900655 100644 --- a/README.md +++ b/README.md @@ -5,16 +5,35 @@ path**, extracted from a pure-Rust implementation into Lean 4 via Charon/Aeneas — the same pipeline, discipline, and honesty rules as the four ed25519 campaigns (`dalek/anza/risc0/betrusted-ed25519-verified`). -## STATUS: eleven certificates over the extracted verify model (external review round 2 applied) +## STATUS: eleven certificates over the extracted verify model (external review rounds 1–5 applied) -`verification/check.sh` is **green** (exit 0): the model compiles, the -proofs compile, and the axiom audit passes. The audit now runs **inside -Lean** (`verification/Proofs/Audit.lean`): it reads each certificate's cone -from the kernel via `collectAxioms` and asserts SET EQUALITY against that -certificate's expected boundary — so an *added* axiom and a silently -*dropped* oracle dependency both fail, with no text parsing to misparse -(external review round 2, 2026-07-24, replaced the earlier `#print axioms` -text parser, which could fail open on an empty or truncated report). +`verification/check.sh` is **green** (exit 0): the model compiles, the proofs +compile, and the audit passes. The audit runs **inside Lean** +(`verification/Proofs/Audit.lean`) and binds four things, each added because an +external reviewer *demonstrated* the button going green without it: + +- **axiom cones** — each certificate's cone is read from the kernel via + `collectAxioms` and must equal its expected set EXACTLY, so an added axiom + and a silently dropped oracle both fail (round 2 retired a text parser that + could fail open on an empty or truncated report); +- **coverage** — EVERY declaration in the eight certificate modules, of every + kind, and in `Audit.lean` itself, must stay inside the axiom boundary (rounds + 4–5: an un-manifested `theorem : False`, then a `def : False`, then one inside + the auditor, each passed a gate that checked only the listed certificates); +- **statements and specifications** — `check.sh` binds to the **SHA-256** of a + canonical block containing the policy constants, every certificate's + fully-elaborated statement, and every reference fold's fully-elaborated + *body*. Round 5 showed why the last part is essential: redefining a fold to + *be* the extracted loop left every earlier fingerprint bit-identical while the + certificate degenerated to "the loop equals the loop"; +- **bytes** — Phase 0 sha256-pins the four model files and the compiler harness + `lean-guard`, purges stale `.olean`s, and forbids stray `.lean` files, so the + verdict depends on committed bytes rather than build-directory state. + +What the button still does **not** bind is stated plainly in +[TRUSTED-BASE.md](TRUSTED-BASE.md) item 11 — `check.sh` itself, the toolchain +env, and `$AENEAS_HOME`. `verification/check-selftest.sh` runs the reviewers' +own exploits back against the gate; all are rejected. **What is actually established** — eleven Lean theorems about the Aeneas-generated model of the **monomorphic `verify_mono` compatibility @@ -50,6 +69,17 @@ cannot translate the deployed `Hashers` function-pointer struct): - **Not closed-form FIPS 205 correctness:** the folds are transliterations of the extracted loops (the hash primitives stay opaque); nothing here relates the recomputed root to a mathematical SLH-DSA specification. +- **Read every loop certificate as "visible", not "correct".** This follows + from the previous point but is worth stating on its own, because the per- + certificate descriptions below are easy to over-read. Each reference fold is + built from the *same* extracted primitives the loop calls, so any defect in + the extracted code is faithfully copied into the fold and the theorem still + holds. What is machine-checked is the loop's *scaffolding* — trip count, + index arithmetic, state threading, argument order, branch structure. Whether + the address schedule, the Merkle sibling order, or the FORS leaf index match + FIPS 205 is a **human reading step**, not a proved one. (Round-5 review makes + this sharper: the certificates are individually meaningful only to the extent + someone has read each fold against the standard — see TRUSTED-BASE item 12.) This is a real **intermediate** verification layer, not an end-to-end formal verification of the deployed verifier. After de-plumbing rounds 1+2 @@ -91,10 +121,16 @@ The trust base and residual assumptions are stated in `xmss_pk_from_sig_free_loop` equals the fold that, at step k, sets the tree height to k+1, tests bit k of the leaf index, and on an even bit halves the tree index and hashes H(node ∥ auth[k]), on an odd bit sets - the tree index to (i−1)/2 and hashes H(auth[k] ∥ node). This pins the + the tree index to (i−1)/2 and hashes H(auth[k] ∥ node). This makes the Merkle sibling ORDER (the even/odd rule), the tree-height/tree-index - address schedule, and the auth-path indexing — the heart of Merkle-path - verification. Cone: kernel three + `verify_mono.oracle.h` (the first + address schedule, and the auth-path indexing VISIBLE in the certificate — + **it does not establish them as correct.** `xmssFoldN` calls the same + extracted `set_tree_height`/`get_tree_index`/`oracle.h` that the loop body + calls, so a swapped sibling order would be copied into the fold and the + theorem would still hold. Read that as: the certificate pins what the + extracted code *does* at each step; whether that matches FIPS 205 + Algorithm 10 is a human reading step. Cone: kernel three + + `verify_mono.oracle.h` (the first certificate where H enters; F does not — the loop runs above the WOTS+ computation). @@ -103,8 +139,9 @@ The trust base and residual assumptions are stated in at layer j, splits the tree index (idx_leaf = idx_tree mod 2^h' by mask+cast, then idx_tree >>= h'), sets the layer address to j and the tree address to the shifted index, and recomputes the node through - `xmss_pk_from_sig` on the j-th XMSS signature. This pins the layer - schedule of hypertree verification; the final node = pk_root comparison + `xmss_pk_from_sig` on the j-th XMSS signature. This makes the layer + schedule of hypertree verification visible in the certificate (same + transliteration caveat as above); the final node = pk_root comparison sits one bind above, in `ht_verify_free`, and belongs to the apex composition. Cone: kernel three + `verify_mono.oracle.{f, h, t_l}` — the full WOTS+/XMSS machinery referenced through the fold, and nothing @@ -124,9 +161,9 @@ re-run green after every source patch. - **`fips205.fors_inner_loop_eq`** + **`fips205.fors_outer_loop_eq`** (Algorithm 17, FORS pk-from-sig): a nested loop, split into two theorems. - The inner one pins the auth-path Merkle fold for a single FORS tree (bit + The inner one equates the auth-path Merkle fold for a single FORS tree (bit source `indices[i] >> j`, `H` in the even/odd sibling order) — cone - kernel-3 + `oracle.h`. The outer one pins the K-tree fold: for each tree + kernel-3 + `oracle.h`. The outer one equates the K-tree fold: for each tree compute the leaf with `F` at index `(i< - s!"{n}|{String.intercalate "," ((sortName cone).map toString)}|{fp}")) - String.hash ser +/-- Deterministic name ordering for the canonical serialization. -/ +def sortNames (l : List Name) : List Name := + ((l.map toString).toArray.qsort (· < ·)).toList.map (·.toName) + +/-- Whitespace-canonical: every whitespace run collapses to one space, so the + pretty-printer's line wrapping cannot perturb the digest. -/ +def normWs (s : String) : String := + (s.foldl (fun (acc : String × Bool) c => + let c := if c.isWhitespace then ' ' else c + if c == ' ' then (if acc.2 then acc else (acc.1.push ' ', true)) + else (acc.1.push c, false)) + ("", true)).1 + +/-- Is `n` a hand-written declaration living in one of the certificate modules? + These are the SPECIFICATION side — the folds the certificates are stated + against — as opposed to the extracted model in `gen/` (pinned by Phase 0). -/ +def isSpecConst (env : Environment) (n : Name) : Bool := + match env.getModuleIdxFor? n with + | some idx => certModules.contains env.header.moduleNames[idx.toNat]! + | none => false + +/-- Transitive closure over specification constants, starting from a + certificate's STATEMENT and following DEFINITION bodies (a theorem + contributes its statement only). This discovers the reference folds — and + any future one — automatically, so a new specification definition cannot be + introduced without moving the digest. -/ +partial def closureOf (env : Environment) (seen : NameSet) (work : List Name) : NameSet := + match work with + | [] => seen + | n :: rest => + if seen.contains n || !isSpecConst env n then closureOf env seen rest + else + let seen := seen.insert n + let more := match env.find? n with + | some (.defnInfo v) => v.value.getUsedConstants.toList ++ v.type.getUsedConstants.toList + | some ci => ci.type.getUsedConstants.toList + | none => [] + closureOf env seen (more ++ rest) + +/-- Fully-explicit (`pp.all`) rendering, whitespace-canonicalized. -/ +def ppAll (e : Expr) : CommandElabM String := do + let s ← Command.liftCoreM <| Meta.MetaM.run' <| + withOptions (fun o => o.setBool `pp.all true) do + return (← Meta.ppExpr e).pretty + return normWs s elab "auditCones" : command => do let env ← getEnv let mut errs : Array String := #[] - -- (0) the manifest's expected cones may reference nothing outside the boundary + + -- (0) the manifest's expected cones may reference nothing outside the policy. for (cert, cone, _) in manifest do for a in cone do unless allowedBoundary.contains a do throwError "manifest references non-boundary axiom {a} for {cert}" - -- (1) NAMED CERTS: exists ∧ theorem ∧ exact cone ∧ statement fingerprint + + -- (1) NAMED CERTS: exists ∧ is a theorem ∧ exact cone ∧ statement diagnostic. for (cert, expected, expFp) in manifest do match env.find? cert with - | none => errs := errs.push s!"{cert}: NOT FOUND (renamed/deleted?)" - | some (.thmInfo ci) => + | none => errs := errs.push s!"{cert}: NOT FOUND (renamed/deleted?)" + | some (.thmInfo ci) => let got := (← collectAxioms cert).toList let extras := got.filter (fun a => !expected.contains a) let missing := expected.filter (fun a => !got.contains a) @@ -114,35 +161,79 @@ elab "auditCones" : command => do errs := errs.push s!"{cert}: cone extra={extras} missing={missing}" unless ci.type.hash == expFp do errs := errs.push s!"{cert}: STATEMENT fingerprint {ci.type.hash} ≠ committed {expFp} (statement changed?)" - | some (.axiomInfo _) => errs := errs.push s!"{cert}: is an AXIOM, not a proven theorem" - | some (.opaqueInfo _) => errs := errs.push s!"{cert}: is OPAQUE, not a proven theorem" - | some _ => errs := errs.push s!"{cert}: not a theorem" - -- (2) FULL-MODULE ENUMERATION: every theorem in a cert module has a clean cone. - -- This is the layer that stops an un-manifested `: False := cheat _`. + | some (.axiomInfo _) => errs := errs.push s!"{cert}: is an AXIOM, not a proven theorem" + | some (.opaqueInfo _) => errs := errs.push s!"{cert}: is OPAQUE, not a proven theorem" + | some _ => errs := errs.push s!"{cert}: not a theorem" + + -- (2) ENUMERATION over EVERY declaration kind — not just theorems (a + -- `def : False` passed the round-4 gate) — in the eight certificate + -- modules, AND over this file's own declarations (module index is `none` + -- during its own elaboration), so the auditor is not exempt (round-5 R1). let manifestNames := manifest.map (·.1) - let mut nModuleThms := 0 + let mut nEnum := 0 let mut certsSeen : Array Name := #[] for (nm, ci) in env.constants.toList do - match ci with - | .thmInfo _ => + let scope : Option String := match env.getModuleIdxFor? nm with | some idx => - if certModules.contains env.header.moduleNames[idx.toNat]! then - nModuleThms := nModuleThms + 1 - if manifestNames.contains nm then certsSeen := certsSeen.push nm + let m := env.header.moduleNames[idx.toNat]! + if certModules.contains m then some (toString m) else none + | none => if nm.isInternal then none else some "Proofs.Audit (this file)" + match scope with + | none => pure () + | some where_ => + nEnum := nEnum + 1 + if manifestNames.contains nm then certsSeen := certsSeen.push nm + match ci with + | .axiomInfo _ => + -- the five oracle axioms live in gen/ (Phase-0 pinned); an axiom + -- DECLARED inside an audited module is never acceptable. + errs := errs.push s!"AXIOM DECLARED in audited scope: {nm} ({where_})" + | _ => let cone := (← collectAxioms nm).toList let bad := cone.filter (fun a => !allowedBoundary.contains a) unless bad.isEmpty do - errs := errs.push s!"UN-AUDITED theorem {nm} (module {env.header.moduleNames[idx.toNat]!}) has disallowed axioms {bad}" - | none => pure () - | _ => pure () - -- every manifest cert must actually be a theorem found in a cert module + errs := errs.push s!"UN-AUDITED declaration {nm} ({where_}) has disallowed axioms {bad}" for cert in manifestNames do unless certsSeen.contains cert do - errs := errs.push s!"manifest cert {cert} not found as a theorem in any certificate module" + errs := errs.push s!"manifest cert {cert} not found in any certificate module" + unless errs.isEmpty do throwError "AUDIT FAILED (fail-closed):\n{String.intercalate "\n" errs.toList}" - logInfo s!"exact-cone audit PASSED: {manifest.length} certificates (cones + statement fingerprints), {nModuleThms} module theorems enumerated clean; MANIFEST-FINGERPRINT: {manifestFingerprint}" + + -- (3) CANONICAL BLOCK: policy + statements + specification bodies. check.sh + -- binds to the SHA-256 of everything between the markers. + let mut lines : Array String := #[] + lines := lines.push + s!"policy|allowedBoundary={String.intercalate "," ((sortNames allowedBoundary).map toString)}|certModules={String.intercalate "," ((sortNames certModules).map toString)}" + let mut specs : NameSet := {} + for (cert, cone, _) in manifest do + let ci := (env.find? cert).get! + specs := (closureOf env {} ci.type.getUsedConstants.toList).toList.foldl (·.insert ·) specs + lines := lines.push + s!"cert|{cert}|cone={String.intercalate "," ((sortNames cone).map toString)}|type={← ppAll ci.type}" + for nm in sortNames specs.toList do + match env.find? nm with + | none => errs := errs.push s!"specification constant vanished: {nm}" + | some ci => + let isProp ← Command.liftCoreM <| Meta.MetaM.run' <| Meta.isProp ci.type + -- proof irrelevance: a Prop-valued constant contributes its STATEMENT; + -- a data definition contributes its BODY — that is where fidelity lives. + if isProp then + lines := lines.push s!"spec|{nm}|prop|type={← ppAll ci.type}" + else + match ci with + | .defnInfo v => lines := lines.push s!"spec|{nm}|def|value={← ppAll v.value}" + | _ => lines := lines.push s!"spec|{nm}|other|type={← ppAll ci.type}" + unless errs.isEmpty do + throwError "AUDIT FAILED (fail-closed):\n{String.intercalate "\n" errs.toList}" + + logInfo ("AUDIT-MANIFEST-BEGIN\n" ++ String.intercalate "\n" lines.toList ++ "\nAUDIT-MANIFEST-END") + -- check.sh prints the certificate list it gets from HERE, not from a hand-kept + -- bash array (drill finding: the one authoritative claim string was the one + -- thing nothing bound — adding a name to it printed a cert that never existed). + logInfo s!"CERTIFICATES: {String.intercalate " " (manifestNames.map toString)}" + logInfo s!"exact-cone audit PASSED: {manifest.length} certificates (cones + statements), {specs.toList.length} specification constants pinned, {nEnum} declarations enumerated clean" end SlhVerify.Audit diff --git a/verification/RECORDED-RUN.md b/verification/RECORDED-RUN.md index 37998b6..a156549 100644 --- a/verification/RECORDED-RUN.md +++ b/verification/RECORDED-RUN.md @@ -142,14 +142,14 @@ Certificates proven: fips205.chain_free_loop_eq fips205.wots_loop1_eq fips205.xm hand-maintained TypesExternal.lean / FunsExternal.lean are NOT overwritten once they exist) [Info ] Imported: SlhVerify.llbc -[?25lApplied prepasses: [------------------------------------------------] 0/142 ⠋ Applied prepasses: [------------------------------------------------] 1/142 ⠋ Applied prepasses: [###---------------------------------------------] 11/142 ⠋ Applied prepasses: [#################-------------------------------] 52/142 ⠙ Applied prepasses: [########################################--------] 120/142 ⠙ Applied prepasses: [################################################] 142/142 ✔️ -[?25h[?25lTranslated globals: [-------------------------------------------------] 0/10 ⠋ Translated globals: [#################################################] 10/10 ✔️ -[?25h[?25lTranslated opaque functions: [----------------------------------------] 0/76 ⠋ Translated opaque functions: [########################################] 76/76 ✔️ -[?25h[?25lTranslated transparent functions: [-----------------------------------] 0/42 ⠋ Translated transparent functions: [-----------------------------------] 1/42 ⠙ Translated transparent functions: [#######----------------------------] 9/42 ⠹ Translated transparent functions: [########---------------------------] 10/42 ⠹ Translated transparent functions: [##########-------------------------] 12/42 ⠹ Translated transparent functions: [##########-------------------------] 13/42 ⠹ Translated transparent functions: [###########------------------------] 14/42 ⠸ Translated transparent functions: [############-----------------------] 15/42 ⠸ Translated transparent functions: [##############---------------------] 17/42 ⠸ Translated transparent functions: [###############--------------------] 19/42 ⠸ Translated transparent functions: [################-------------------] 20/42 ⠼ Translated transparent functions: [##################-----------------] 22/42 ⠼ Translated transparent functions: [####################---------------] 24/42 ⠼ Translated transparent functions: [#####################--------------] 26/42 ⠴ Translated transparent functions: [######################-------------] 27/42 ⠴ Translated transparent functions: [#######################------------] 28/42 ⠦ Translated transparent functions: [########################-----------] 29/42 ⠦ Translated transparent functions: [#########################----------] 30/42 ⠦ Translated transparent functions: [#########################----------] 31/42 ⠧ Translated transparent functions: [###########################--------] 33/42 ⠇ Translated transparent functions: [#############################------] 35/42 ⠏ Translated transparent functions: [##############################-----] 36/42 ⠏ Translated transparent functions: [##############################-----] 37/42 ⠋ Translated transparent functions: [###############################----] 38/42 ⠙ Translated transparent functions: [################################---] 39/42 ⠹ Translated transparent functions: [#################################--] 40/42 ⠸ Translated transparent functions: [##################################-] 41/42 ⠸ Translated transparent functions: [###################################] 42/42 ⠼ Translated transparent functions: [###################################] 42/42 ✔️ -[?25h[?25lTranslated trait declarations: [--------------------------------------] 0/33 ⠋ Translated trait declarations: [##############------------------------] 13/33 ✔️ -[?25h[?25lTranslated trait impls: [---------------------------------------------] 0/50 ⠋ Translated trait impls: [######################-----------------------] 25/50 ✔️ -[?25h[?25lPost-processed translated opaque functions: [-------------------------] 0/76 ⠋ Post-processed translated opaque functions: [-------------------------] 1/76 ⠙ Post-processed translated opaque functions: [#########################] 76/76 ✔️ -[?25h[?25lPost-processed translated transparent functions: [--------------------] 0/42 ⠋ Post-processed translated transparent functions: [--------------------] 1/42 ⠙ Post-processed translated transparent functions: [###-----------------] 7/42 ⠙ Post-processed translated transparent functions: [####----------------] 9/42 ⠙ Post-processed translated transparent functions: [####----------------] 10/42 ⠹ Post-processed translated transparent functions: [#####---------------] 11/42 ⠹ Post-processed translated transparent functions: [#####---------------] 12/42 ⠸ Post-processed translated transparent functions: [######--------------] 13/42 ⠸ Post-processed translated transparent functions: [######--------------] 14/42 ⠸ Post-processed translated transparent functions: [#######-------------] 15/42 ⠼ Post-processed translated transparent functions: [#######-------------] 16/42 ⠼ Post-processed translated transparent functions: [########------------] 17/42 ⠼ Post-processed translated transparent functions: [#########-----------] 19/42 ⠴ Post-processed translated transparent functions: [#########-----------] 20/42 ⠴ Post-processed translated transparent functions: [##########----------] 21/42 ⠴ Post-processed translated transparent functions: [##########----------] 22/42 ⠦ Post-processed translated transparent functions: [##########----------] 23/42 ⠦ Post-processed translated transparent functions: [###########---------] 25/42 ⠦ Post-processed translated transparent functions: [############--------] 26/42 ⠧ Post-processed translated transparent functions: [############--------] 27/42 ⠧ Post-processed translated transparent functions: [#############-------] 28/42 ⠧ Post-processed translated transparent functions: [##############------] 30/42 ⠇ Post-processed translated transparent functions: [###############-----] 32/42 ⠇ Post-processed translated transparent functions: [###############-----] 33/42 ⠏ Post-processed translated transparent functions: [################----] 34/42 ⠏ Post-processed translated transparent functions: [#################---] 37/42 ⠋ Post-processed translated transparent functions: [##################--] 38/42 ⠋ Post-processed translated transparent functions: [##################--] 39/42 ⠙ Post-processed translated transparent functions: [###################-] 40/42 ⠹ Post-processed translated transparent functions: [###################-] 41/42 ⠸ Post-processed translated transparent functions: [####################] 42/42 ⠼ Post-processed translated transparent functions: [####################] 42/42 ✔️ +[?25lApplied prepasses: [------------------------------------------------] 0/142 ⠋ Applied prepasses: [------------------------------------------------] 1/142 ⠋ Applied prepasses: [###---------------------------------------------] 11/142 ⠋ Applied prepasses: [#################-------------------------------] 52/142 ⠙ Applied prepasses: [########################################--------] 120/142 ⠙ Applied prepasses: [################################################] 142/142 ✔️ +[?25h[?25lTranslated globals: [-------------------------------------------------] 0/10 ⠋ Translated globals: [#################################################] 10/10 ✔️ +[?25h[?25lTranslated opaque functions: [----------------------------------------] 0/76 ⠋ Translated opaque functions: [########################################] 76/76 ✔️ +[?25h[?25lTranslated transparent functions: [-----------------------------------] 0/42 ⠋ Translated transparent functions: [-----------------------------------] 1/42 ⠙ Translated transparent functions: [#######----------------------------] 9/42 ⠹ Translated transparent functions: [########---------------------------] 10/42 ⠹ Translated transparent functions: [##########-------------------------] 12/42 ⠹ Translated transparent functions: [##########-------------------------] 13/42 ⠹ Translated transparent functions: [###########------------------------] 14/42 ⠸ Translated transparent functions: [############-----------------------] 15/42 ⠸ Translated transparent functions: [##############---------------------] 17/42 ⠸ Translated transparent functions: [###############--------------------] 19/42 ⠸ Translated transparent functions: [################-------------------] 20/42 ⠼ Translated transparent functions: [##################-----------------] 22/42 ⠼ Translated transparent functions: [####################---------------] 24/42 ⠼ Translated transparent functions: [#####################--------------] 26/42 ⠴ Translated transparent functions: [######################-------------] 27/42 ⠴ Translated transparent functions: [#######################------------] 28/42 ⠦ Translated transparent functions: [########################-----------] 29/42 ⠦ Translated transparent functions: [#########################----------] 30/42 ⠦ Translated transparent functions: [#########################----------] 31/42 ⠧ Translated transparent functions: [###########################--------] 33/42 ⠇ Translated transparent functions: [#############################------] 35/42 ⠏ Translated transparent functions: [##############################-----] 36/42 ⠏ Translated transparent functions: [##############################-----] 37/42 ⠋ Translated transparent functions: [###############################----] 38/42 ⠙ Translated transparent functions: [################################---] 39/42 ⠹ Translated transparent functions: [#################################--] 40/42 ⠸ Translated transparent functions: [##################################-] 41/42 ⠸ Translated transparent functions: [###################################] 42/42 ⠼ Translated transparent functions: [###################################] 42/42 ✔️ +[?25h[?25lTranslated trait declarations: [--------------------------------------] 0/33 ⠋ Translated trait declarations: [##############------------------------] 13/33 ✔️ +[?25h[?25lTranslated trait impls: [---------------------------------------------] 0/50 ⠋ Translated trait impls: [######################-----------------------] 25/50 ✔️ +[?25h[?25lPost-processed translated opaque functions: [-------------------------] 0/76 ⠋ Post-processed translated opaque functions: [-------------------------] 1/76 ⠙ Post-processed translated opaque functions: [#########################] 76/76 ✔️ +[?25h[?25lPost-processed translated transparent functions: [--------------------] 0/42 ⠋ Post-processed translated transparent functions: [--------------------] 1/42 ⠙ Post-processed translated transparent functions: [###-----------------] 7/42 ⠙ Post-processed translated transparent functions: [####----------------] 9/42 ⠙ Post-processed translated transparent functions: [####----------------] 10/42 ⠹ Post-processed translated transparent functions: [#####---------------] 11/42 ⠹ Post-processed translated transparent functions: [#####---------------] 12/42 ⠸ Post-processed translated transparent functions: [######--------------] 13/42 ⠸ Post-processed translated transparent functions: [######--------------] 14/42 ⠸ Post-processed translated transparent functions: [#######-------------] 15/42 ⠼ Post-processed translated transparent functions: [#######-------------] 16/42 ⠼ Post-processed translated transparent functions: [########------------] 17/42 ⠼ Post-processed translated transparent functions: [#########-----------] 19/42 ⠴ Post-processed translated transparent functions: [#########-----------] 20/42 ⠴ Post-processed translated transparent functions: [##########----------] 21/42 ⠴ Post-processed translated transparent functions: [##########----------] 22/42 ⠦ Post-processed translated transparent functions: [##########----------] 23/42 ⠦ Post-processed translated transparent functions: [###########---------] 25/42 ⠦ Post-processed translated transparent functions: [############--------] 26/42 ⠧ Post-processed translated transparent functions: [############--------] 27/42 ⠧ Post-processed translated transparent functions: [#############-------] 28/42 ⠧ Post-processed translated transparent functions: [##############------] 30/42 ⠇ Post-processed translated transparent functions: [###############-----] 32/42 ⠇ Post-processed translated transparent functions: [###############-----] 33/42 ⠏ Post-processed translated transparent functions: [################----] 34/42 ⠏ Post-processed translated transparent functions: [#################---] 37/42 ⠋ Post-processed translated transparent functions: [##################--] 38/42 ⠋ Post-processed translated transparent functions: [##################--] 39/42 ⠙ Post-processed translated transparent functions: [###################-] 40/42 ⠹ Post-processed translated transparent functions: [###################-] 41/42 ⠸ Post-processed translated transparent functions: [####################] 42/42 ⠼ Post-processed translated transparent functions: [####################] 42/42 ✔️ [?25h[Info ] Generated: gen/SlhVerify/Types.lean [Info ] Generated: gen/SlhVerify/FunsExternal_Template.lean [Info ] Generated: gen/SlhVerify/Funs.lean @@ -164,13 +164,32 @@ db720b4a30f512e6048212a472e6853b24931a8121cb94c4cf7e6489754d6384 gen/SlhVerify/ The third reviewer demonstrated three fail-opens OUTSIDE the cone check (F1 unbound cert set / un-manifested theorem; F2 statements unbound; F3 model bytes unbound). All fixed. check.sh green with the hardened gate, -and the adversarial self-test now rejects eight attacks including the two -the reviewer used to make the button green over a repo proving False: +and the adversarial self-test then rejected eight attacks including the two +the reviewer used to make the button green over a repo proving False. + +**CORRECTION (2026-07-27, found by an independent audit of this file).** The +three lines that stood here inside the fence below were **not** console output: +they were a hand-written summary of the run, fenced as if captured. `check.sh` +never printed them. The author wrote them; that is fabricated evidence in the +one document whose stated purpose is to carry machine evidence to reviewers who +cannot run the toolchain, and it is exactly the failure this project exists to +prevent. They have been removed. The selftest transcript that follows in the +same fence **is** verbatim. + +Two further corrections to this file's framing: +* the "INDEPENDENT RUN — executed by the operator" block above is at proof repo + `62d7ed1`, which **predates the round-4 gate** (its transcript has no Phase 0). + It is genuine and operator-executed, but it is *not* a run of the gate that + now ships; +* consequently, at the time of writing there was **no recorded run of the + current gate by an independent party**. Any transcript below this line that is + not explicitly attributed to a named party was produced by the author agent. + +Rule adopted going forward: no text is placed inside a fence in this file unless +it was captured with `tee`/`cat` from the real command, and every evidence block +states its date, its pin, and who ran it. ``` -check.sh: ALL GREEN — MANIFEST-FINGERPRINT: 13660980750615609973 -Phase 0 model-byte integrity: 4/4 gen files match PROVENANCE.json -Phase 3 audit: 11 certs (cones + statement fingerprints), 196 module theorems enumerated clean check-selftest: attacking the gates ==================================== @@ -187,3 +206,74 @@ SELFTEST GREEN: the gate rejects dead files, extra axioms, dropped oracles, vanished certs, un-manifested False theorems, gutted statements, hand-edited models, and deleted manifest rows. ``` + +## Round-5 hardening — author-agent run, 20260727T205716Z, proof repo @ (this commit) + +Captured with `tee` from the real commands; nothing below was typed by hand. +Not independently executed — an independent run of this gate is still outstanding. + +### check.sh +``` +fips205-slhdsa-verified — check +=============================== +=== Phase 0: build hygiene + model/harness integrity === + ✓ gen/SlhVerify/Funs.lean + ✓ gen/SlhVerify/FunsExternal.lean + ✓ gen/SlhVerify/Types.lean + ✓ gen/SlhVerify/TypesExternal.lean + ✓ lean-guard +=== Phase 1: compile the extracted model === + · gen/SlhVerify/TypesExternal + · gen/SlhVerify/Types + · gen/SlhVerify/FunsExternal + · gen/SlhVerify/Funs +=== Phase 2: compile the proofs === + · ChainSpec + · WotsSpec + · XmssSpec + · HtSpec + · ForsInnerSpec + · ForsOuterSpec + · InputPrepSpec + · ApexSpec +=== Phase 3: in-Lean audit (cones + statement fingerprints + enumeration) === + ✓ exact-cone audit PASSED + ✓ audit-manifest digest matches (sha256 d83e297a49094c97…) + +ALL GREEN — model compiles, proofs compile, and every certificate cone +equals EXACTLY the three kernel axioms plus its documented SHA-2 oracles. +Certificates proven: fips205.chain_free_loop_eq fips205.wots_loop1_eq fips205.xmss_loop_eq fips205.ht_loop_eq fips205.fors_inner_loop_eq fips205.fors_outer_loop_eq fips205.to_int_loop_eq fips205.to_byte_loop_eq fips205.wots_csum_loop_eq fips205.base2b_outer_loop_eq fips205.slh_verify_128s_accepts_iff +``` + +### check-selftest.sh (14 attacks + digest-coverage check) +``` +check-selftest: attacking the gates +==================================== +✓ attack 1 rejected (dead-file gate) +✓ attack 2 rejected (extra-axiom detection — evil_ax named) +✓ attack 3 rejected (missing-oracle detection — exact cone, not subset) +✓ attack 4 rejected (existence check — a vanished cert cannot pass as 0-axiom) +✓ attack 5 rejected (enumeration — an un-manifested False theorem cannot pass) +✓ attack 6 rejected (statement check — a gutted statement of the same cone cannot pass) +✓ attack 7 rejected (Phase 0 model-byte integrity) +✓ attack 8 rejected (audit-manifest digest — a silently-dropped cert cannot pass) +✓ attack 9 rejected (digest covers allowedBoundary — the policy cannot be widened silently) +✓ attack 10 rejected (a specification fold cannot be silently redefined to the loop) +✓ attack 11 rejected (enumeration covers every declaration kind, not just theorems) +✓ attack 12 rejected (the auditor audits itself — no exemption) +✓ attack 13 rejected (Phase 0 pins lean-guard — the harness is in the TCB and bound) +✓ attack 14 rejected (no .lean may sit outside gen/ and Proofs/) +✓ check 15 passed (the hashed block carries all 12 reference-fold bodies, +./check-selftest.sh: line 270: _f: command not found + including the recursive companions and their extracted-primitive calls) + +SELFTEST GREEN: 14 attacks rejected + digest-coverage check — dead files, extra axioms, dropped +oracles, vanished certs, un-manifested False theorems AND defs, gutted +statements, hand-edited models, dropped manifest rows, widened policy, +specification folds redefined to the loop, a False-proof in the auditor, +a stubbed harness, and stray modules. +``` + +Note: the `_f: command not found` line in the selftest transcript above is a +cosmetic shell-quoting bug in the script's own success message (backticks inside +a double-quoted echo), fixed in this same commit. It did not affect any gate. diff --git a/verification/check-selftest.sh b/verification/check-selftest.sh index 1004b39..6e8a47d 100755 --- a/verification/check-selftest.sh +++ b/verification/check-selftest.sh @@ -1,155 +1,277 @@ #!/usr/bin/env bash # Adversarial self-test of the check.sh gates (the R3-5 tradition: an audit that -# cannot fail is theater). The audit runs INSIDE Lean (Proofs/Audit.lean); the -# model bytes are pinned in Phase 0; the certificate SET and each STATEMENT are -# bound by a manifest fingerprint. Every attack MUST make check.sh fail, via the -# intended gate: +# cannot fail is theater). Every attack MUST make check.sh fail, via the gate it +# targets — each assertion names a SPECIFIC diagnostic, so a rejection for an +# unrelated reason fails the test too. # -# 1. DEAD FILE — a stray Proofs/*.lean not in the manifest. -# 2. SMUGGLED AXIOM — a listed cert whose real cone contains a disallowed -# axiom; exact-equality reports extra=[...]. -# 3. DROPPED ORACLE — a listed cert whose expected cone claims an oracle its -# proof does not use; exact-equality reports missing=[...] -# (a subset checker would pass this). -# 4. VANISHED CERT — a manifest name that no longer resolves; the explicit -# existence check reports NOT FOUND (collectAxioms would -# otherwise return [] and pass). -# 5. UN-AUDITED FALSE — round-4 F1: an UN-manifested `theorem … : False := …` -# added to a certificate module. The full-module -# enumeration must flag its disallowed cone. (This is the -# attack that made the pre-round-4 button green over a -# repo proving False.) -# 6. GUTTED STATEMENT — round-4 F2: a certificate's statement replaced by a -# tautology of the SAME cone. The statement fingerprint -# must differ from the committed manifest value. -# 7. MODEL TAMPER — round-4 F3: a hand-edit of a gen/ model file. Phase 0 -# must reject it before anything is compiled. -# 8. DELETED ROW — round-4 F1 (set half): a manifest row removed. Audit -# still compiles, but the printed MANIFEST-FINGERPRINT -# changes and check.sh's committed binding must reject it. +# Attacks 1-8 are the round-3/4 set. Attacks 9-14 were authored by external +# reviewers and an independent drill, each having DEMONSTRATED the corresponding +# fail-open against an earlier gate — they are the reason this round exists: # -# Green here means the gate genuinely rejects all eight. Self-cleaning: every -# file a step tampers is saved and restored around that step. +# 9 widen `allowedBoundary` by one name + a False-proof (round-5 NEW-1: +# previously ALL GREEN with the fingerprint BYTE-IDENTICAL) +# 10 redefine a reference fold to BE the extracted loop (round-5 NEW-2: +# previously ALL GREEN — the certificate degenerates to `loop = loop`) +# 11 `def : False` instead of `theorem : False` (drill: the round-4 +# enumeration matched `.thmInfo` only, so this passed) +# 12 a False-proof inside Audit.lean itself (round-5 R1: the +# auditor was exempt from its own enumeration) +# 13 stub `lean-guard` (round-5 NEW-3: +# previously ALL GREEN in 3.6s over destroyed proofs) +# 14 a stray .lean beside check.sh (round-5 NEW-4: +# LEAN_PATH includes $PWD, so it can join the environment ungated) +# +# Self-cleaning: every mutated file is backed up and restored, and an EXIT trap +# restores even on failure. Run from a clean tree. set -uo pipefail HERE="$(cd "$(dirname "$0")" && pwd)" cd "$HERE" +source ~/aeneas-toolchain/env.sh -TOUCHED=() -save() { for f in "$@"; do cp -f "$f" "$f.sfbak"; TOUCHED+=("$f"); done; } -restore() { for f in "${TOUCHED[@]}"; do [ -f "$f.sfbak" ] && mv -f "$f.sfbak" "$f"; done; TOUCHED=(); } +BAKS=() +save() { cp -p "$1" "$1.sfbak"; BAKS+=("$1"); } +restore() { for f in "${BAKS[@]:-}"; do [ -f "$f.sfbak" ] && mv -f "$f.sfbak" "$f"; done; BAKS=(); } cleanup() { restore - rm -f Proofs/Stray.lean Proofs/Stray.olean Proofs/EvilSpec.lean Proofs/EvilSpec.olean \ - Proofs/Audit.olean Proofs/ChainSpec.olean *.sfbak Proofs/*.sfbak gen/SlhVerify/*.sfbak + rm -f Proofs/Stray.lean Proofs/EvilSpec.lean Evil.lean \ + Proofs/*.olean gen/SlhVerify/*.olean .audit-manifest.observed 2>/dev/null + return 0 } trap cleanup EXIT +fail() { echo "✗ $1"; shift; [ $# -gt 0 ] && sed 's/^/ /' "$1"; exit 1; } + echo "check-selftest: attacking the gates" echo "====================================" -# ── Attack 1: dead file ───────────────────────────────────────────────────── +# ── 1: dead file ──────────────────────────────────────────────────────────── echo "-- stray" > Proofs/Stray.lean -if ./check.sh > /tmp/sf1.out 2>&1; then echo "✗ ATTACK 1 SUCCEEDED (dead file stayed green)"; exit 1; fi -grep -q "DEAD FILE" /tmp/sf1.out || { echo "✗ ATTACK 1: failed, not via dead-file gate"; cat /tmp/sf1.out; exit 1; } -rm -f Proofs/Stray.lean Proofs/Stray.olean +./check.sh > /tmp/sf1.out 2>&1 && fail "ATTACK 1 SUCCEEDED (dead file stayed green)" /tmp/sf1.out +grep -q "DEAD FILE" /tmp/sf1.out || fail "ATTACK 1: failed, not via the dead-file gate" /tmp/sf1.out +rm -f Proofs/Stray.lean echo "✓ attack 1 rejected (dead-file gate)" -# ── Attack 2: smuggled disallowed axiom in a real cone ────────────────────── -save check.sh Proofs/Audit.lean +# ── 2: smuggled disallowed axiom in a real cone ───────────────────────────── +save check.sh; save Proofs/Audit.lean +# NB: no imports — Phase 0 now purges every .olean, so a module injected at the +# head of the build order cannot import one that has not been compiled yet. cat > Proofs/EvilSpec.lean <<'EOF' -import Proofs.ChainSpec axiom evil_ax : True theorem evil_thm : True := evil_ax EOF python3 - <<'PY' s = open("check.sh").read() -assert 'PROOFS=(\n' in s +assert 'PROOFS=(\n' in s, "check.sh PROOFS shape changed" open("check.sh","w").write(s.replace('PROOFS=(\n', 'PROOFS=(\n "EvilSpec"\n', 1)) a = open("Proofs/Audit.lean").read() -assert 'import Proofs.ApexSpec' in a and ' [ (' in a +assert 'import Proofs.ApexSpec' in a and ' [ (`fips205.chain_free_loop_eq' in a, "Audit.lean shape changed" a = a.replace('import Proofs.ApexSpec', 'import Proofs.ApexSpec\nimport Proofs.EvilSpec', 1) -a = a.replace(' [ (', ' [ (`evil_thm, kernel3, 0),\n (', 1) +a = a.replace(' [ (`fips205.chain_free_loop_eq', ' [ (`evil_thm, kernel3, 0),\n (`fips205.chain_free_loop_eq', 1) open("Proofs/Audit.lean","w").write(a) PY -if ./check.sh > /tmp/sf2.out 2>&1; then echo "✗ ATTACK 2 SUCCEEDED (smuggled axiom)"; exit 1; fi -grep -q "evil_ax" /tmp/sf2.out || { echo "✗ ATTACK 2: rejected but evil_ax not named"; cat /tmp/sf2.out; exit 1; } -restore; rm -f Proofs/EvilSpec.lean Proofs/EvilSpec.olean Proofs/Audit.olean +./check.sh > /tmp/sf2.out 2>&1 && fail "ATTACK 2 SUCCEEDED (smuggled axiom)" /tmp/sf2.out +grep -q "evil_ax" /tmp/sf2.out || fail "ATTACK 2: rejected but evil_ax not named" /tmp/sf2.out +restore; rm -f Proofs/EvilSpec.lean echo "✓ attack 2 rejected (extra-axiom detection — evil_ax named)" -# ── Attack 3: dropped-oracle (subset would pass; exact must not) ───────────── +# ── 3: dropped oracle (a subset check would pass; exact must not) ──────────── save Proofs/Audit.lean python3 - <<'PY' import re a = open("Proofs/Audit.lean").read() -new, n = re.subn(r'(`fips205\.to_int_loop_eq,\s*)kernel3(,\s*\d+\))', r'\1kernel3 ++ [oracleF]\2', a) -assert n == 1, f"patched {n}" +new, n = re.subn(r'(`fips205\.to_int_loop_eq,\s*)kernel3,', r'\1kernel3 ++ [oracleF],', a) +assert n == 1, f"expected 1 to_int row, patched {n}" open("Proofs/Audit.lean","w").write(new) PY -if ./check.sh > /tmp/sf3.out 2>&1; then echo "✗ ATTACK 3 SUCCEEDED (dropped oracle, subset hole)"; exit 1; fi -grep -q "missing=\[verify_mono.oracle.f\]" /tmp/sf3.out || { echo "✗ ATTACK 3: rejected but missing oracle not named"; cat /tmp/sf3.out; exit 1; } -restore; rm -f Proofs/Audit.olean +./check.sh > /tmp/sf3.out 2>&1 && fail "ATTACK 3 SUCCEEDED (dropped oracle — subset hole)" /tmp/sf3.out +grep -q "missing=\[verify_mono.oracle.f\]" /tmp/sf3.out || fail "ATTACK 3: rejected but missing oracle not named" /tmp/sf3.out +restore echo "✓ attack 3 rejected (missing-oracle detection — exact cone, not subset)" -# ── Attack 4: vanished certificate ────────────────────────────────────────── +# ── 4: vanished certificate ───────────────────────────────────────────────── save Proofs/Audit.lean python3 - <<'PY' a = open("Proofs/Audit.lean").read() -assert a.count('`fips205.chain_free_loop_eq') >= 1 +assert a.count('`fips205.chain_free_loop_eq,') >= 1 open("Proofs/Audit.lean","w").write(a.replace('`fips205.chain_free_loop_eq,', '`fips205.chain_free_loop_eq_VANISHED,', 1)) PY -if ./check.sh > /tmp/sf4.out 2>&1; then echo "✗ ATTACK 4 SUCCEEDED (vanished cert)"; exit 1; fi -grep -q "NOT FOUND" /tmp/sf4.out || { echo "✗ ATTACK 4: rejected but not via existence check"; cat /tmp/sf4.out; exit 1; } -restore; rm -f Proofs/Audit.olean -echo "✓ attack 4 rejected (existence check — vanished cert cannot pass as 0-axiom)" +./check.sh > /tmp/sf4.out 2>&1 && fail "ATTACK 4 SUCCEEDED (vanished cert)" /tmp/sf4.out +grep -q "NOT FOUND" /tmp/sf4.out || fail "ATTACK 4: rejected but not via the existence check" /tmp/sf4.out +restore +echo "✓ attack 4 rejected (existence check — a vanished cert cannot pass as 0-axiom)" -# ── Attack 5: un-manifested theorem proving False (round-4 F1, the big one) ── +# ── 5: un-manifested THEOREM proving False (round-4 F1) ───────────────────── save Proofs/ChainSpec.lean -printf '\n-- SELFTEST ATTACK 5 (round-4 F1): an un-manifested cert proving False.\naxiom cheat : ∀ (P : Prop), P\ntheorem repo_proves_false : False := cheat _\n' >> Proofs/ChainSpec.lean -if ./check.sh > /tmp/sf5.out 2>&1; then echo "✗ ATTACK 5 SUCCEEDED: check.sh GREEN over a repo proving False!"; exit 1; fi -grep -q "repo_proves_false" /tmp/sf5.out || { echo "✗ ATTACK 5: rejected but not via the module enumeration"; cat /tmp/sf5.out; exit 1; } -restore; rm -f Proofs/ChainSpec.olean Proofs/Audit.olean -echo "✓ attack 5 rejected (module enumeration — an un-manifested False theorem cannot pass)" +printf '\n-- SELFTEST ATTACK 5\naxiom cheat5 : ∀ (P : Prop), P\ntheorem repo_proves_false : False := cheat5 _\n' >> Proofs/ChainSpec.lean +./check.sh > /tmp/sf5.out 2>&1 && fail "ATTACK 5 SUCCEEDED: check.sh GREEN over a repo proving False!" /tmp/sf5.out +grep -qE "repo_proves_false|AXIOM DECLARED" /tmp/sf5.out || fail "ATTACK 5: rejected but not via the enumeration" /tmp/sf5.out +restore +echo "✓ attack 5 rejected (enumeration — an un-manifested False theorem cannot pass)" -# ── Attack 6: gutted statement, cone preserved (round-4 F2) ───────────────── -# Gut a LEAF certificate (to_byte_loop_eq — nothing depends on it, so Phase 2 -# still compiles and the fingerprint gate is what must bite). Replace its -# statement+proof with a kernel-3 tautology: same cone, different type. +# ── 6: gutted STATEMENT, cone preserved (round-4 F2) ──────────────────────── save Proofs/InputPrepSpec.lean python3 - <<'PY' s = open("Proofs/InputPrepSpec.lean").read() -i = s.index("theorem to_byte_loop_eq (n : Std.U32) (k : Nat) :") -j = s.index("theorem hbody_cs", i) # the NEXT declaration (to_byte_loop_eq is a leaf) -gut = "theorem to_byte_loop_eq : (∀ p : Prop, p ∨ ¬p) := Classical.em\n\n" -open("Proofs/InputPrepSpec.lean","w").write(s[:i] + gut + s[j:]) +i = s.index("theorem to_byte_loop_eq (n : Std.U32) (k : Nat) :") # a LEAF cert +j = s.index("theorem hbody_cs", i) # next declaration +open("Proofs/InputPrepSpec.lean","w").write( + s[:i] + "theorem to_byte_loop_eq : (∀ p : Prop, p ∨ ¬p) := Classical.em\n\n" + s[j:]) PY -if ./check.sh > /tmp/sf6.out 2>&1; then echo "✗ ATTACK 6 SUCCEEDED: gutted statement passed (cone preserved)"; exit 1; fi -grep -qi "fingerprint" /tmp/sf6.out || { echo "✗ ATTACK 6: rejected but not via the statement fingerprint"; cat /tmp/sf6.out; exit 1; } -restore; rm -f Proofs/InputPrepSpec.olean Proofs/Audit.olean -echo "✓ attack 6 rejected (statement fingerprint — a gutted statement of the same cone cannot pass)" - -# ── Attack 7: hand-edited model file (round-4 F3) ─────────────────────────── -save gen/SlhVerify/Funs.lean -printf '\n-- SELFTEST ATTACK 7 (round-4 F3): hand-edited model.\n' >> gen/SlhVerify/Funs.lean -if ./check.sh > /tmp/sf7.out 2>&1; then echo "✗ ATTACK 7 SUCCEEDED: hand-edited model passed"; exit 1; fi -grep -q "MODEL INTEGRITY FAILED" /tmp/sf7.out || { echo "✗ ATTACK 7: rejected but not via Phase 0"; cat /tmp/sf7.out; exit 1; } +./check.sh > /tmp/sf6.out 2>&1 && fail "ATTACK 6 SUCCEEDED (gutted statement, cone preserved)" /tmp/sf6.out +grep -q "STATEMENT fingerprint" /tmp/sf6.out || fail "ATTACK 6: rejected but not via the statement check" /tmp/sf6.out restore -echo "✓ attack 7 rejected (Phase 0 model-byte integrity — a hand-edited model cannot compile)" +echo "✓ attack 6 rejected (statement check — a gutted statement of the same cone cannot pass)" -# ── Attack 8: deleted manifest row (round-4 F1 set half) ──────────────────── +# ── 7: hand-edited model file (round-4 F3) ────────────────────────────────── +save gen/SlhVerify/Funs.lean +printf '\n-- SELFTEST ATTACK 7\n' >> gen/SlhVerify/Funs.lean +./check.sh > /tmp/sf7.out 2>&1 && fail "ATTACK 7 SUCCEEDED (hand-edited model passed)" /tmp/sf7.out +grep -q "INTEGRITY FAILED" /tmp/sf7.out || fail "ATTACK 7: rejected but not via Phase 0" /tmp/sf7.out +restore +echo "✓ attack 7 rejected (Phase 0 model-byte integrity)" + +# ── 8: deleted manifest row (round-4 F1, set half) ────────────────────────── save Proofs/Audit.lean python3 - <<'PY' import re a = open("Proofs/Audit.lean").read() -new, n = re.subn(r'\n *\(`fips205\.to_int_loop_eq,[^\n]*\),', '', a) -assert n == 1, f"removed {n}" +new, n = re.subn(r'\n\s*\(`fips205\.to_int_loop_eq,.*?\),', '', a) +assert n == 1, f"expected 1 row, removed {n}" open("Proofs/Audit.lean","w").write(new) PY -if ./check.sh > /tmp/sf8.out 2>&1; then echo "✗ ATTACK 8 SUCCEEDED: a deleted manifest row passed (set unbound)"; exit 1; fi -grep -q "manifest fingerprint mismatch" /tmp/sf8.out || { echo "✗ ATTACK 8: rejected but not via the manifest-fingerprint binding"; cat /tmp/sf8.out; exit 1; } -restore; rm -f Proofs/Audit.olean -echo "✓ attack 8 rejected (manifest fingerprint — a silently-dropped cert cannot pass)" +./check.sh > /tmp/sf8.out 2>&1 && fail "ATTACK 8 SUCCEEDED (a dropped cert row passed)" /tmp/sf8.out +grep -q "digest mismatch" /tmp/sf8.out || fail "ATTACK 8: rejected but not via the digest binding" /tmp/sf8.out +restore +echo "✓ attack 8 rejected (audit-manifest digest — a silently-dropped cert cannot pass)" + +# ── 9: WIDEN THE POLICY (round-5 NEW-1) ───────────────────────────────────── +# Previously ALL GREEN with the committed fingerprint byte-identical: the +# fingerprint covered `manifest` but never `allowedBoundary`, the very predicate +# the enumeration tests against. +# Widen the policy ALONE — no axiom is declared anywhere, so the enumeration +# (which now also rejects a bare `axiom` in an audited module) cannot fire and +# the DIGEST must be what bites. `sorryAx` is used as the smuggled name because +# admitting it would silently legalise every `sorry` in the repository. +save Proofs/Audit.lean +python3 - <<'PY' +a = open("Proofs/Audit.lean").read() +old = " kernel3 ++ [oracleF, oracleH, oracleTL, oracleTLen, oracleHMsg]\n" +assert a.count(old) == 1, "allowedBoundary shape changed" +open("Proofs/Audit.lean","w").write(a.replace(old, old.rstrip("\n") + " ++ [`sorryAx]\n", 1)) +PY +./check.sh > /tmp/sf9.out 2>&1 && fail "ATTACK 9 SUCCEEDED: the axiom policy was widened and the button stayed GREEN!" /tmp/sf9.out +grep -q "digest mismatch" /tmp/sf9.out || fail "ATTACK 9: rejected but not via the policy-covering digest" /tmp/sf9.out +restore +echo "✓ attack 9 rejected (digest covers allowedBoundary — the policy cannot be widened silently)" + +# ── 10: REDEFINE A SPEC FOLD TO BE THE LOOP (round-5 NEW-2) ───────────────── +# The certificate keeps its exact statement, cone and type-hash, but becomes +# `loop = loop` — vacuous. Previously ALL GREEN. +save Proofs/ChainSpec.lean +python3 - <<'PY' +s = open("Proofs/ChainSpec.lean").read() +i = s.index("noncomputable def chainFoldN") +j = s.index("/-- One full loop step", i) +gut = """noncomputable def chainFoldN {N : Std.Usize} (pk_seed : Slice Std.U8) : + types.Adrs → Array Std.U8 N → Std.U32 → Nat → Result (Array Std.U8 N) := + fun adrs tmp start s => + verify_mono.chain_free_loop + { start := start, + «end» := Std.U32.ofNatCore ((start.val + s) % 2 ^ 32) (Nat.mod_lt _ (by norm_num)) } + pk_seed adrs tmp + +""" +open("Proofs/ChainSpec.lean","w").write(s[:i] + gut + s[j:]) +PY +./check.sh > /tmp/sf10.out 2>&1 && fail "ATTACK 10 SUCCEEDED: the spec fold IS the loop, certificate is vacuous, still GREEN!" /tmp/sf10.out +# Two layers stand here, and either is a valid rejection: the existing proof no +# longer matches the redefined fold (Phase 2), and — if an attacker repairs the +# proof, as the round-5 reviewer did — the digest covers specification BODIES, +# so it moves. Attack 9 is the pure test that the digest binding fires; that the +# digest's input contains the fold bodies is verified directly (see below). +grep -qE "digest mismatch|FAIL: Proofs/ChainSpec" /tmp/sf10.out \ + || fail "ATTACK 10: rejected, but neither via the digest nor a proof break" /tmp/sf10.out +restore +echo "✓ attack 10 rejected (a specification fold cannot be silently redefined to the loop)" + +# ── 11: `def : False` rather than `theorem : False` (drill finding) ───────── +save Proofs/WotsSpec.lean +printf '\n-- SELFTEST ATTACK 11\naxiom cheat11 : ∀ (P : Prop), P\ndef attack11_false : False := cheat11 _\n' >> Proofs/WotsSpec.lean +./check.sh > /tmp/sf11.out 2>&1 && fail "ATTACK 11 SUCCEEDED: a def proving False passed!" /tmp/sf11.out +grep -qE "attack11_false|AXIOM DECLARED" /tmp/sf11.out || fail "ATTACK 11: rejected but not via the all-kinds enumeration" /tmp/sf11.out +restore +echo "✓ attack 11 rejected (enumeration covers every declaration kind, not just theorems)" + +# ── 12: a False-proof inside the AUDITOR itself (round-5 R1) ──────────────── +save Proofs/Audit.lean +python3 - <<'PY' +a = open("Proofs/Audit.lean").read() +i = a.index("elab \"auditCones\"") +open("Proofs/Audit.lean","w").write( + a[:i] + "axiom cheat12 : ∀ (P : Prop), P\ntheorem audit_proves_false : False := cheat12 _\n\n" + a[i:]) +PY +./check.sh > /tmp/sf12.out 2>&1 && fail "ATTACK 12 SUCCEEDED: the auditor itself proves False, still GREEN!" /tmp/sf12.out +grep -qE "audit_proves_false|AXIOM DECLARED" /tmp/sf12.out || fail "ATTACK 12: rejected but not via self-enumeration" /tmp/sf12.out +restore +echo "✓ attack 12 rejected (the auditor audits itself — no exemption)" + +# ── 13: stub the compiler harness (round-5 NEW-3) ────────────────────────── +# Previously: ALL GREEN in 3.6s with the proofs destroyed. lean-guard is KEPT +# (it is this machine's memory cap) and sha256-pinned instead. +save lean-guard +cat > lean-guard <<'EOF' +#!/usr/bin/env bash +echo "exact-cone audit PASSED" +exit 0 +EOF +chmod +x lean-guard +./check.sh > /tmp/sf13.out 2>&1 && fail "ATTACK 13 SUCCEEDED: a stubbed harness passed!" /tmp/sf13.out +grep -q "INTEGRITY FAILED" /tmp/sf13.out || fail "ATTACK 13: rejected but not via the harness pin" /tmp/sf13.out +restore +echo "✓ attack 13 rejected (Phase 0 pins lean-guard — the harness is in the TCB and bound)" + +# ── 14: stray .lean beside check.sh (round-5 NEW-4) ──────────────────────── +cat > Evil.lean <<'EOF' +axiom cheat14 : ∀ (P : Prop), P +theorem evil14 : False := cheat14 _ +EOF +./check.sh > /tmp/sf14.out 2>&1 && fail "ATTACK 14 SUCCEEDED: a stray Lean module passed!" /tmp/sf14.out +grep -q "BUILD HYGIENE FAILED" /tmp/sf14.out || fail "ATTACK 14: rejected but not via the hygiene gate" /tmp/sf14.out +rm -f Evil.lean +echo "✓ attack 14 rejected (no .lean may sit outside gen/ and Proofs/)" + +# ── 15: COVERAGE OF THE DIGEST INPUT (direct, not an attack) ─────────────── +# Attack 9 proves the digest binding fires. This proves WHAT it covers: the +# hashed block must literally contain each reference fold's definition BODY, so +# that any change to one necessarily moves the SHA-256 (round-5 NEW-2). +./check.sh > /tmp/sf15.out 2>&1 || fail "ATTACK 15 setup: clean tree is not green" /tmp/sf15.out +lake_out=$(cd "$AENEAS_HOME/backends/lean" 2>/dev/null && lake env bash -c \ + "cd '$HERE' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD/gen:\$PWD\" && '$HERE/lean-guard' 'Proofs/Audit.lean'" 2>&1) +BLOCK=$(awk '/AUDIT-MANIFEST-BEGIN/{f=1;next} /AUDIT-MANIFEST-END/{f=0} f' <<<"$lake_out") +[ -n "$BLOCK" ] || { echo "✗ ATTACK 15: no audit block"; exit 1; } +for fold in chainFoldN wotsChainFold xmssFoldN htFoldN forsInnerFold forsOuterFold \ + toIntFold toByteFold wotsCsumFold base2bOuterFold slhVerifyRoot htVerifyRoot; do + grep -q "spec|fips205.$fold|def|value=" <<<"$BLOCK" \ + || { echo "✗ CHECK 15: the digest input does NOT carry the body of $fold"; exit 1; } +done +# Lean's equation compiler splits a recursive definition: `chainFoldN` is a thin +# wrapper and the actual recursion lives in `chainFoldN._f`. BOTH are reached by +# the closure and printed, so assert the SEMANTIC content specifically — the +# extracted primitives a fold must call — rather than assuming which line holds +# it. (An earlier revision of this check asserted the body text was on the +# wrapper's line and failed while coverage was in fact correct.) +for probe in "fips205.chainFoldN._f|def|value=.*set_hash_address" \ + "fips205.xmssFoldN._f|def|value=.*verify_mono.oracle.h" \ + "fips205.slhVerifyRoot|def|value=.*verify_mono.oracle.h_msg"; do + grep -qE "spec\|$probe" <<<"$BLOCK" \ + || { echo "✗ CHECK 15: the digest input is missing expected body content: $probe"; exit 1; } +done +echo "✓ check 15 passed (the hashed block carries all 12 reference-fold bodies," +echo ' including the recursive _f companions and their extracted-primitive calls)' echo -echo "SELFTEST GREEN: the gate rejects dead files, extra axioms, dropped oracles," -echo "vanished certs, un-manifested False theorems, gutted statements, hand-edited" -echo "models, and deleted manifest rows." +echo "SELFTEST GREEN: 14 attacks rejected + digest-coverage check — dead files, extra axioms, dropped" +echo "oracles, vanished certs, un-manifested False theorems AND defs, gutted" +echo "statements, hand-edited models, dropped manifest rows, widened policy," +echo "specification folds redefined to the loop, a False-proof in the auditor," +echo "a stubbed harness, and stray modules." diff --git a/verification/check.sh b/verification/check.sh index c53759c..b299296 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -3,19 +3,23 @@ # Green output == the full claim. This script is the ONLY source of the # word "proven" for this repo. # -# Phase 0 — model-byte integrity: every gen/SlhVerify/*.lean must sha256-match -# PROVENANCE.json (a hand-edited model fails BEFORE it is compiled; -# round-4 review F3). +# Phase 0 — build hygiene + integrity: purge stale .olean (the verdict must +# depend on committed bytes, not untracked build state), forbid any +# .lean outside gen/ and Proofs/, and sha256-pin the four model files +# AND the compiler harness `lean-guard` to PROVENANCE.json. # Phase 1 — compile the extracted Lean model (gen/SlhVerify). # Phase 2 — compile the proof files (Proofs/). -# Phase 3 — the in-Lean audit (Proofs/Audit.lean): each certificate's cone -# (via `collectAxioms`) must EQUAL its expected set exactly AND its -# statement fingerprint must match the committed manifest, EVERY -# theorem in the eight cert modules must have a cone within the -# boundary (so an un-manifested `: False := cheat _` cannot pass — -# round-4 F1), and this script binds to the printed MANIFEST -# fingerprint (round-4 F2/F1). Any mismatch → non-zero exit → +# Phase 3 — the in-Lean audit (Proofs/Audit.lean): per certificate, the cone +# (via `collectAxioms`) must EQUAL its expected set exactly; EVERY +# declaration kind in the eight cert modules and in Audit.lean itself +# must stay within the axiom boundary; and this script binds to the +# SHA-256 of the canonical AUDIT-MANIFEST block, which covers the +# POLICY constants, every certificate STATEMENT, and every reachable +# SPECIFICATION DEFINITION BODY. Any mismatch → non-zero exit → # fail-closed. No text parsing of axiom cones. +# +# What this button does NOT bind is stated in TRUSTED-BASE.md item 11: this +# script itself, the toolchain env, $AENEAS_HOME, and the Lean toolchain. set -euo pipefail HERE="$(cd "$(dirname "$0")" && pwd)" @@ -41,33 +45,35 @@ PROOFS=( "InputPrepSpec" "ApexSpec" ) -# Certificates whose axiom cones are audited, and the allowed extras beyond -# the three kernel axioms: the five SHA-2 verify-path oracles. A certificate -# is listed here only once it is genuinely proven. -CERTS=( - "fips205.chain_free_loop_eq" - "fips205.wots_loop1_eq" - "fips205.xmss_loop_eq" - "fips205.ht_loop_eq" - "fips205.fors_inner_loop_eq" - "fips205.fors_outer_loop_eq" - "fips205.to_int_loop_eq" - "fips205.to_byte_loop_eq" - "fips205.wots_csum_loop_eq" - "fips205.base2b_outer_loop_eq" - "fips205.slh_verify_128s_accepts_iff" -) echo "fips205-slhdsa-verified — check" echo "===============================" -# ── Phase 0: model-byte integrity (gen/ == PROVENANCE.json) ────────────────── -echo "=== Phase 0: model-byte integrity (gen/ pinned to PROVENANCE.json) ===" -python3 - "$HERE/PROVENANCE.json" "$HERE" <<'PY' || { echo "MODEL INTEGRITY FAILED (a gen/ file differs from PROVENANCE.json — hand-edited model?)"; exit 1; } +# ── Phase 0: build hygiene + model & harness integrity ─────────────────────── +echo "=== Phase 0: build hygiene + model/harness integrity ===" +# (a) Purge every .olean first. Round-5 NEW-4: the button's verdict must depend +# on COMMITTED BYTES, never on untracked build state — a stale .olean from a +# module that no longer exists (and *.olean is .gitignored, so invisible to +# `git status`) could otherwise satisfy an import and go green. +find "$HERE/gen" "$HERE/Proofs" -name '*.olean' -delete 2>/dev/null || true +# (b) No Lean source may sit outside gen/ and Proofs/. LEAN_PATH includes $PWD, +# so a stray verification/*.lean can join the environment ungated (NEW-4). +STRAY=$(find "$HERE" -maxdepth 1 -name '*.lean' -printf '%f\n' 2>/dev/null || true) +if [ -n "$STRAY" ]; then + echo "$STRAY" | sed 's/^/ ✗ stray Lean source outside gen\/ and Proofs\/: /' + echo "BUILD HYGIENE FAILED (a .lean outside the audited directories can join LEAN_PATH)"; exit 1 +fi +# (c) sha256-pin the extracted model AND the compiler harness. lean-guard is +# repo-tracked and is shelled out to for every compile, so it is part of the +# trusted computing base: round 5 demonstrated that stubbing it alone yields +# ALL GREEN in 3.6s over destroyed proofs. It is KEPT (it is the memory cap +# that protects this machine after the 12.2GB OOM incident) and pinned. +python3 - "$HERE/PROVENANCE.json" "$HERE" <<'PY' || { echo "INTEGRITY FAILED (a pinned file differs from PROVENANCE.json — hand-edited model or harness?)"; exit 1; } import json, sys, hashlib, os prov = json.load(open(sys.argv[1])); here = sys.argv[2] -files = {k: v for k, v in prov.get("model_integrity_sha256", {}).items() if k.startswith("gen/")} +files = {k: v for k, v in prov.get("model_integrity_sha256", {}).items() if not k.startswith("_")} +files.update({k: v for k, v in prov.get("harness_integrity_sha256", {}).items() if not k.startswith("_")}) if not files: - print(" no model_integrity_sha256 in PROVENANCE.json (fail-closed)"); sys.exit(1) + print(" no integrity map in PROVENANCE.json (fail-closed)"); sys.exit(1) bad = 0 for rel, want in sorted(files.items()): p = os.path.join(here, rel) @@ -109,31 +115,46 @@ lake env bash -c " # ── Phase 3: in-Lean audit (cones + statements + full-module enumeration) ──── echo "=== Phase 3: in-Lean audit (cones + statement fingerprints + enumeration) ===" cd "$AENEAS_LEAN" -# Proofs/Audit.lean checks: per-cert exact cone + statement fingerprint; every -# theorem in the eight cert modules has a clean cone (no un-manifested axiom -# smuggle); and it prints a MANIFEST-FINGERPRINT over the whole committed -# manifest. We bind to that EXACT fingerprint below, so deleting/swapping a cert -# row, or editing a cone or a statement fingerprint, changes the printed value -# and fails HERE even if Lean itself exits 0 (round-4 F1/F2 set+statement bind). -# To rotate the manifest deliberately, recompute it (compile Audit.lean, read the -# printed value) and update EXPECTED_MANIFEST_FP in the same reviewable commit. -EXPECTED_MANIFEST_FP="MANIFEST-FINGERPRINT: 13660980750615609973" +# THE BINDING DIGEST. Audit.lean emits a canonical AUDIT-MANIFEST block holding +# the POLICY constants (allowedBoundary, certModules — round-5 NEW-1), every +# certificate's fully-elaborated STATEMENT, and every reachable SPECIFICATION +# definition's fully-elaborated BODY (round-5 NEW-2: redefining a reference fold +# to *be* the extracted loop previously left every fingerprint intact). We bind +# to the SHA-256 of that block, retiring the 32-bit Expr.hash as the load-bearing +# digest (NEW-5). To rotate deliberately: run check.sh, take the printed OBSERVED +# digest, and update this constant in the same reviewable commit. +EXPECTED_AUDIT_SHA256="d83e297a49094c970b88ce7c63ceb85d6bee0764d4623456a7225860e2298afa" AUD_OUT=$(lake env bash -c "cd '$HERE' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD/gen:\$PWD\" && LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=$MEM '$HERE/lean-guard' 'Proofs/Audit.lean'" 2>&1) || { echo "$AUD_OUT" | sed 's/^/ /' - echo "AUDIT FAILED (Audit.lean did not compile — cone/statement mismatch, missing cert, sham, or un-audited theorem)"; exit 1; } + echo "AUDIT FAILED (Audit.lean did not compile — cone/statement mismatch, missing cert, sham, or un-audited declaration)"; exit 1; } if ! grep -qF "exact-cone audit PASSED" <<<"$AUD_OUT"; then echo "$AUD_OUT" | sed 's/^/ /' echo "AUDIT FAILED (no PASSED line — fail-closed)"; exit 1 fi -if ! grep -qF "$EXPECTED_MANIFEST_FP" <<<"$AUD_OUT"; then +BLOCK=$(awk '/AUDIT-MANIFEST-BEGIN/{f=1;next} /AUDIT-MANIFEST-END/{f=0} f' <<<"$AUD_OUT") +if [ -z "$BLOCK" ]; then echo "$AUD_OUT" | sed 's/^/ /' - echo "AUDIT FAILED — manifest fingerprint mismatch." - echo " expected: $EXPECTED_MANIFEST_FP" - echo " the certificate set / a cone / a statement fingerprint changed without a reviewed manifest rotation."; exit 1 + echo "AUDIT FAILED (no AUDIT-MANIFEST block — fail-closed)"; exit 1 fi -echo " ✓ $(grep -oF 'exact-cone audit PASSED' <<<"$AUD_OUT" | head -1) ($EXPECTED_MANIFEST_FP)" +GOT_SHA=$(printf '%s\n' "$BLOCK" | sha256sum | cut -d' ' -f1) +if [ "$GOT_SHA" != "$EXPECTED_AUDIT_SHA256" ]; then + printf '%s\n' "$BLOCK" > "$HERE/.audit-manifest.observed" + echo "AUDIT FAILED — audit-manifest digest mismatch." + echo " expected: $EXPECTED_AUDIT_SHA256" + echo " observed: $GOT_SHA" + echo " A policy constant, a certificate statement, or a specification" + echo " definition changed without a reviewed rotation. The observed block was" + echo " written to verification/.audit-manifest.observed — diff it to see what." + exit 1 +fi +echo " ✓ $(grep -oF 'exact-cone audit PASSED' <<<"$AUD_OUT" | head -1)" +echo " ✓ audit-manifest digest matches (sha256 ${EXPECTED_AUDIT_SHA256:0:16}…)" echo echo "ALL GREEN — model compiles, proofs compile, and every certificate cone" echo "equals EXACTLY the three kernel axioms plus its documented SHA-2 oracles." -echo "Certificates proven: ${CERTS[*]}" +# The list comes from the AUDITED manifest itself, never from a hand-kept array: +# a display list nothing binds can name a certificate that does not exist. +CERT_LINE=$(sed -n 's/.*CERTIFICATES: //p' <<<"$AUD_OUT" | head -1) +[ -n "$CERT_LINE" ] || { echo "AUDIT FAILED (no CERTIFICATES line — fail-closed)"; exit 1; } +echo "Certificates proven: $CERT_LINE" diff --git a/verification/gen/SlhVerify/FunsExternal.lean b/verification/gen/SlhVerify/FunsExternal.lean index d1b7646..029a129 100644 --- a/verification/gen/SlhVerify/FunsExternal.lean +++ b/verification/gen/SlhVerify/FunsExternal.lean @@ -13,8 +13,16 @@ · verify_mono.oracle.h_msg — H_msg (message digest) These are SHA-256-based; their correctness against FIPS 180-4 is the standing hash-oracle boundary (see TRUSTED-BASE.md). The apex - certificate will carry EXACTLY these five beyond Lean's three kernel + certificate carries EXACTLY these five beyond Lean's three kernel axioms — nothing else. + NOTE, so a future reader is not misled: these are five AXIOMS but only + FOUR distinct Rust primitives. `oracle.t_l` and `oracle.t_len` both + delegate to `crate::hashers::sha2_cat_1::t_l` (src/verify_mono.rs) — + modelling them as two INDEPENDENT axioms is deliberately conservative + (a theorem proved for unrelated oracles also holds when they coincide), + but the model cannot express that they agree. Note also the naming + inversion against FIPS 205: `oracle.t_l` models T_len (WOTS+ pk + compression) and `oracle.t_len` models T_k (FORS root compression). (2) TRANSPILER PLUMBING — core-library externals Aeneas emits for this extraction config. These carry NO cryptographic content. The u32 @@ -28,11 +36,14 @@ IterMut became index loops, so the Take::next axiom was deleted too. Remaining as axioms on the whole model: the FIVE SHA-2 verify-path oracles and three zeroize blanket impls (never on the verify path) — - nothing else. The #print axioms audit (fail-closed, wrap-safe since the - external-review fix of 2026-07-24) confirms only the five oracles + the - kernel three survive in any certificate cone. + nothing else. The in-Lean audit (Proofs/Audit.lean, `collectAxioms`, + round 5) confirms only the five oracles + the kernel three appear in any + certificate cone, and that no other declaration in the audited modules + reaches outside that boundary. The zeroize axioms are deliberately + absent from the audit's `allowedBoundary`, so if one ever reached a cone + the build would fail. THIS FILE is hand-maintained (Aeneas does not + regenerate it) and its bytes are sha256-pinned by check.sh Phase 0. ────────────────────────────────────────────────────────────────────────────── -/ --- This is a template file: rename it to "FunsExternal.lean" and fill the holes. import Aeneas import SlhVerify.Types open Aeneas Aeneas.Std Result ControlFlow Error