# fips205-slhdsa-verified Machine-checked verification campaign for the **SLH-DSA (FIPS 205) verify 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) `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). **What is actually established** — eleven Lean theorems about the Aeneas-generated model of the **monomorphic `verify_mono` compatibility verify path** (an additive, `#![allow(dead_code)]` re-expression of the deployed generic verifier, using named hash oracles because Charon/Aeneas cannot translate the deployed `Hashers` function-pointer struct): - **Ten loop-fidelity theorems** (chain 5, WOTS+ 8, XMSS 10, hypertree 12, FORS-inner/outer 17, and the input-prep helpers to_int/to_byte/checksum/ base_2b-outer, Alg 2/3/4). Each equates one *generated* Aeneas loop with an explicit hand-written recursive fold — a local control-flow correspondence, not an Algorithm-level mathematical specification. - **The apex, `fips205.slh_verify_128s_accepts_iff`** — the extracted `verify_mono::slh_verify_128s` returns `ok true` **iff** the recomputed hypertree root byte-equals `pk.pk_root`. This is an *acceptance characterization*: there is no acceptance path other than root equality over the extracted recomputation. Its `#print axioms` cone is exactly `[propext, Classical.choice, Quot.sound]` + the five SHA-2 oracles. **What is NOT (yet) established — do not overclaim:** - **The apex proof does not compose the ten loop theorems.** It is a *structural factorization* of the extracted verifier around its final equality check; it references none of the ten (it would remain provable if one were deleted). The ten are independent local-fidelity lemmas, not links in the apex's proof chain. - **Not "every loop":** `base_2b`'s inner accumulation loop (`helpers.base_2b_loop0_loop0`) is threaded *opaquely* and has no certificate — and it determines the FORS indices / WOTS digits, so a defect there could change the recomputed root while all eleven theorems still hold. - **Not the deployed public verifier:** the proved subject is the private `verify_mono` facade; the bridge to upstream's generic `pk.verify()` is the finite in-snapshot **differential test**, not a machine-checked refinement. - **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. This is a real **intermediate** verification layer, not an end-to-end formal verification of the deployed verifier. After de-plumbing rounds 1+2 the model carries no plumbing axioms on the verify path — its external surface is exactly the five SHA-2 oracles (plus off-path zeroize impls). The trust base and residual assumptions are stated in [TRUSTED-BASE.md](TRUSTED-BASE.md). - **`fips205.chain_free_loop_eq`** (Algorithm 5, WOTS+ chaining): the extracted `chain_free` loop equals the explicit s-fold hash chain, with the hash address set to i, i+1, …, i+s−1 in turn. This rules out — machine-checked, for the monomorphic SHA2-128s `verify_mono` path — an off-by-one loop bound, a wrong address field, and wrong threading. Its `#print axioms` cone is **exactly** `[propext, Classical.choice, Quot.sound, verify_mono.oracle.f]` — the three kernel axioms plus the one hash oracle it touches, and nothing else (no transpiler plumbing; the u32 range machinery was discharged with real definitions). check.sh Phase 3 (the in-Lean exact-cone audit) fails the build if any certificate's cone differs from its expected set — an extra axiom or a dropped oracle both break it. - **`fips205.wots_loop1_eq`** (Algorithm 8, WOTS+ pk recomputation — the chain loop): the extracted `wots_pk_from_sig_free_loop1` equals the fold that, at each index i in [0, LEN), sets the chain address to i and runs `chain_free` on sig[i] starting at digit msg[i] for W−1−msg[i] steps, writing tmp[i]. This is the layer above chain: it consumes `chain_free` and pins that the LEN chains run with the right start indices, step counts, and slots. Cone: kernel three + `verify_mono.oracle.f`. - **`fips205.xmss_loop_eq`** (Algorithm 10, XMSS pk-from-sig — the authentication-path Merkle loop): the extracted `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 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 certificate where H enters; F does not — the loop runs above the WOTS+ computation). - **`fips205.ht_loop_eq`** (Algorithm 12, hypertree verification — the layer walk): the extracted `ht_verify_free_loop` equals the fold that, 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 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 else. Foundations behind this (2026-07-22/23): the Aeneas-compat patch (additive monomorphic verify module through a named oracle boundary; charon + aeneas exit 0); the u32 range-loop de-plumbing (faithful `Step` defs vs pinned rustc, axiom-clean); the 8-site source de-plumbing (snapshot commit `6f6a9d6`: `try_from`/`is_err`/`unwrap` on pre-masked values → plain casts, the WOTS+ checksum `iter().take()` + `&u32` Sub → an index loop — each site a local rewrite whose equivalence is argued in the commit and checked, for SHA2-128s, by the differential test; the obsoleted transpiler axioms were deleted from the external files); fidelity pinned by that differential test in the snapshot (valid / corrupted / wrong-message), 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 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 compute the leaf with `F` at index `(i< slh_verify_internal -> fors_pk_from_sig -> ht_verify -> xmss_pk_from_sig -> wots_pk_from_sig -> chain ``` Key generation and signing are out of scope (trusted base), exactly as ed25519 signing was. The five verify-path hash oracles (`h_msg, f, h, t_l, t_len` — SHA-2 instantiations; `prf`/`prf_msg` are sign-side only and never enter the cone) are opaque external models with written justifications. They are the *only* things beyond Lean's three kernel axioms that any certificate cone contains: each cone is exactly the kernel three plus the specific oracles that certificate's computation reaches (e.g. `chain` reaches `F`, so `oracle.f` is inside its cone; the input-prep helpers reach no hash, so their cones are kernel-3 alone). That the cones contain *nothing else* — no transpiler plumbing, no hidden axiom — is what the audit enforces (honesty invariant H4); their semantics are the standing SHA-2 oracle boundary documented in [TRUSTED-BASE.md](TRUSTED-BASE.md). ## Gate-0 record (2026-07-22) Per TARGETS.md ("re-verify before use"), the subject was probed before this repository was created: - **Charon**: clean (`charon cargo --preset=aeneas`, roots at the verify cone, `sha2/sha3/zeroize/rand_core` opaque, features `slh_dsa_sha2_128s`) — LLBC produced, exit 0. - **Aeneas**: translated the entire const-generic verify cone to Lean definitions (`wots.chain` … `slh.slh_verify_internal` all generated), with exactly **one obstruction class** (3 unique errors): the `crate::hashers::Hashers` struct of plain **function pointers** cannot be translated. - **Phase 1 — DONE (2026-07-22)**: the Aeneas-compat patch landed in `fips205-source` (snapshot `2d89ee3`): an additive monomorphic SHA2-128s verify module (`src/verify_mono.rs`) whose hash suite is reached through named free functions in `verify_mono::oracle` (marked opaque at the Charon boundary) — the `sha512_*`-shim pattern. Two further compat refinements: the message-digest input M' passes as a single `&[u8]` (nested `&[&[u8]]` is untranslatable), and one `let-else` became the `is_err`/`unwrap` idiom. `verification/extract.sh` now re-derives the model from the mono root; charon + aeneas both exit 0, and `verification/check.sh` compiles the result. At this compat-patch commit the only change to pre-existing code was two lines wiring the new module; the generic paths and all twelve parameter sets stayed untouched. (The later de-plumbing commits — rounds 1 and 2 — then made further local edits to `helpers.rs`/`wots.rs`, each documented and differential-tested; see the snapshot history at head `797b4ef`.) ## What is claimed (the button is green) Each certificate is a statement about the **extracted** functions (H3), compiled by `verification/check.sh` with the in-Lean exact-cone audit (H1): chain semantics, WOTS+ pk recomputation, XMSS path recomputation, hypertree acceptance, FORS pk recomputation, the input-prep helpers, and the apex — `verify_mono::slh_verify_128s` accepts iff the recomputed hypertree root equals the pinned public-key root. The precise scope and non-claims are in the STATUS section above. **The allowed axiom set, stated precisely:** unlike the ed25519 field and scalar layers (whose cones are exactly `[propext, Classical.choice, Quot.sound]`), the hash oracles permeate *every* SLH-DSA layer — `chain` already calls `F`. Each certificate's cone is therefore the three kernel axioms **plus exactly the named oracles its computation reaches** (and nothing else). The transpiler-plumbing axioms that once sat in `FunsExternal.lean` were discharged (de-plumbing rounds 1+2) before any certificate shipped; the audit fails the button if anything outside a certificate's expected boundary — plumbing, an extra oracle, or a dropped one — appears in its cone. ## Discipline Every Lean compile in this repository runs under `verification/lean-guard` (memory-capped, machine-wide serialized). Extraction is reproducible: the full pin set (source commit, Charon/Aeneas commits + toolchain channel, Lean and OCaml versions) is in [verification/PROVENANCE.json](verification/PROVENANCE.json); `verification/extract.sh` refuses to run against a wrong-commit or dirty source tree, and re-running it reproduces the aeneas-generated model byte-identically (verified 2026-07-24). The axiom audit runs inside Lean ([verification/Proofs/Audit.lean](verification/Proofs/Audit.lean)): exact per-certificate cone equality, fail-closed, adversarially exercised by `verification/check-selftest.sh`. What cannot be proven is named in [TRUSTED-BASE.md](TRUSTED-BASE.md), not hidden (H5).