From 2267e04d105ed1ea311512a2145224ac33005c7c Mon Sep 17 00:00:00 2001 From: mrwulf Date: Thu, 23 Jul 2026 17:14:21 +0200 Subject: [PATCH] =?UTF-8?q?phase=202:=20FOURTH=20CERTIFICATE=20=E2=80=94?= =?UTF-8?q?=20hypertree=20layer=20walk=20(Algorithm=2012)=20+=20de-plumbin?= =?UTF-8?q?g?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit fips205.ht_loop_eq (Proofs/HtSpec.lean): the extracted ht_verify_free_loop equals the explicit d-layer fold — at layer j: idx_leaf = idx_tree masked to h' bits (mask+cast), idx_tree >>= h', layer address j, tree address to the shifted index, node recomputed through xmss_pk_from_sig on the j-th XMSS signature. Pins the hypertree layer schedule; the final node == pk_root comparison sits one bind above in ht_verify_free (apex material). Exact cone: [propext, Classical.choice, Quot.sound, verify_mono.oracle.f, verify_mono.oracle.h, verify_mono.oracle.t_l] — kernel-3 plus exactly the three hash primitives the referenced WOTS+/XMSS machinery touches. THE LAYER'S OBSTRUCTION (one per layer, on pattern) was not the proof but the CONE: the first extraction of this loop carried Result-conversion plumbing (try_from/is_err/unwrap; transitively a Take iterator and the &u32 Sub instance) — all axioms, rightly rejected by the Phase-3 audit. Fixed at SOURCE level (fips205-source 6f6a9d6, 8 sites, semantics identical for every FIPS 205 parameter set, differential test re-run green), then re-extracted: the loop body is now straight-line and the proof is the plain chain/wots recipe (no branches; base case via loop.eq_1; step lemma closes by rfl; induction = bind_congr ×12). Also in this commit: - gen/ regenerated from the patched snapshot (loop bodies of the three prior certificates byte-identical modulo source line comments; all three proofs recompiled unchanged and re-audited green). - Dead-stub deletion (axiom-shadowing hygiene rule): the five obsoleted plumbing axioms + vestigial take.default removed from FunsExternal, the orphaned TryFromIntError type axiom removed from TypesExternal. The model's external surface is now: 5 SHA-2 oracles (the boundary), the Take iterator machinery used only by helpers::to_int (apex round's de-plumbing item), 3 zeroize blanket impls (never on the verify path), and the discharged-real u32 Step defs. - check.sh: PROOFS += HtSpec, CERTS += fips205.ht_loop_eq, audit import (self-test structure anchors untouched). README: four certificates + the de-plumbing record. Fidelity review at authorship (three-way): extracted body == Rust ht_verify_free (verbatim from upstream hypertree.rs, calls -> *_free) == FIPS 205 Algorithm 12, incl. mask-then-shift order and layer-then-tree address order. Co-Authored-By: Claude Fable 5 --- README.md | 27 ++- verification/Proofs/HtSpec.lean | 165 +++++++++++++ verification/check.sh | 4 +- verification/gen/SlhVerify/Funs.lean | 226 +++++++----------- verification/gen/SlhVerify/FunsExternal.lean | 78 +----- verification/gen/SlhVerify/Types.lean | 1 - verification/gen/SlhVerify/TypesExternal.lean | 6 - 7 files changed, 287 insertions(+), 220 deletions(-) create mode 100644 verification/Proofs/HtSpec.lean diff --git a/README.md b/README.md index 34e514c..95a8a44 100644 --- a/README.md +++ b/README.md @@ -5,10 +5,10 @@ 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: THREE CERTIFICATES PROVEN — chain (5) + WOTS+ loop (8) + XMSS path (10) +## STATUS: FOUR CERTIFICATES PROVEN — chain (5), WOTS+ loop (8), XMSS path (10), hypertree (12) `verification/check.sh` is **green** (exit 0): the model compiles, the -proofs compile, and the axiom audit passes. **Three certificates proven so +proofs compile, and the axiom audit passes. **Four certificates proven so far, bottom-up:** - **`fips205.chain_free_loop_eq`** (Algorithm 5, WOTS+ chaining): the @@ -43,13 +43,30 @@ far, bottom-up:** 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); fidelity pinned by a differential test in the snapshot -(valid / corrupted / wrong-message). +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 semantics-identical for every FIPS 205 parameter set, and the +obsoleted transpiler axioms deleted from the external files); fidelity +pinned by a differential test in the snapshot (valid / corrupted / +wrong-message), re-run green after every source patch. -The remaining layers (hypertree, FORS, the WOTS+/XMSS input-prep plumbing, +The remaining layers (FORS, the input-prep/digest-split composition, apex) are not yet proven — the pyramid rises one certificate at a time, each audited to the same boundary. diff --git a/verification/Proofs/HtSpec.lean b/verification/Proofs/HtSpec.lean new file mode 100644 index 0000000..e8bba63 --- /dev/null +++ b/verification/Proofs/HtSpec.lean @@ -0,0 +1,165 @@ +/- Proofs/HtSpec.lean — hypertree verification (Algorithm 12), the layer walk. + + THEOREM ht_loop_eq: the extracted hypertree loop (ht_verify_free_loop) + equals the explicit d-layer fold that, at layer j, splits the tree index + (idx_leaf = idx_tree mod 2^h' via 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 FIPS 205 hypertree verification: the + mask-then-shift index split, the layer/tree-address order, the signature + indexing, and the node threading. The final node = pk_root comparison + lives one bind above, in ht_verify_free — the apex composition's job. + + HISTORY: the first extraction of this loop carried Result-conversion + plumbing (try_from / is_err / unwrap and, transitively through the + xmss/wots defs, a Take iterator and a &u32 Sub instance) — all AXIOMS, + which the Phase-3 audit rightly rejected. The fips205-source de-plumbing + patch (8 sites, semantics identical for every FIPS 205 parameter set, + re-validated by the in-snapshot differential test) replaced them with + real-definition constructs; after re-extraction the loop body is + straight-line and this proof is the plain chain/wots recipe on a u32 + range — u32_succ / fwd_succ / hnext / loop_unfold_bind reused VERBATIM + from ChainSpec, no branches, no side conditions beyond the range bound. +-/ +import Proofs.ChainSpec +open Aeneas Aeneas.Std Result ControlFlow +open fips205 + +set_option maxHeartbeats 4000000 + +namespace fips205 + +/-- The loop body on a non-empty range, as a clean do-block (iterator + resolved to the successor w). -/ +theorem hbody_ht {D HP LEN N : Std.Usize} (a : Array (types.XmssSig HP LEN N) D) + (pk_seed : Slice Std.U8) (hp32 : Std.U32) + (start stop w : Std.U32) (idx_tree : Std.U64) (adrs : types.Adrs) + (node : Array Std.U8 N) + (hd : decide (start.val < stop.val) = true) (hwok : start + 1#u32 = ok w) : + verify_mono.ht_verify_free_loop.body a pk_seed hp32 + { start := start, «end» := stop } idx_tree adrs node + = (do + let i ← 1#u64 <<< hp32 + let i1 ← i - 1#u64 + let i2 ← lift (idx_tree &&& i1) + let idx_leaf ← lift (UScalar.cast .U32 i2) + let idx_tree1 ← idx_tree >>> hp32 + let adrs1 ← helpers.Adrs.set_layer_address adrs start + let adrs2 ← helpers.Adrs.set_tree_address adrs1 idx_tree1 + let i3 ← lift (UScalar.cast .Usize start) + let xs ← Array.index_usize a i3 + let sig_tmp ← types.XmssSig.Insts.CoreCloneClone.clone xs + let s0 ← lift (Array.to_slice node) + let node1 ← verify_mono.xmss_pk_from_sig_free idx_leaf sig_tmp s0 pk_seed adrs2 + ok (cont (({ start := w, «end» := stop } : core.ops.range.Range Std.U32), + idx_tree1, adrs2, node1))) := by + unfold verify_mono.ht_verify_free_loop.body + rw [hnext hd hwok] + simp + +/-- The mathematical hypertree fold: at layer j split the index, set the + layer/tree addresses, recompute the node through xmss_pk_from_sig on + signature j. All fallible scalar ops stay monadic, mirroring the + extracted code exactly. -/ +noncomputable def htFoldN {D HP LEN N : Std.Usize} + (a : Array (types.XmssSig HP LEN N) D) (pk_seed : Slice Std.U8) + (hp32 : Std.U32) : + Std.U64 → types.Adrs → Array Std.U8 N → Std.U32 → Nat → + Result (Array Std.U8 N) + | _, _, node, _, 0 => ok node + | idx_tree, adrs, node, j, (s+1) => do + let i ← 1#u64 <<< hp32 + let i1 ← i - 1#u64 + let i2 ← lift (idx_tree &&& i1) + let idx_leaf ← lift (UScalar.cast .U32 i2) + let idx_tree1 ← idx_tree >>> hp32 + let adrs1 ← helpers.Adrs.set_layer_address adrs j + let adrs2 ← helpers.Adrs.set_tree_address adrs1 idx_tree1 + let i3 ← lift (UScalar.cast .Usize j) + let xs ← Array.index_usize a i3 + let sig_tmp ← types.XmssSig.Insts.CoreCloneClone.clone xs + let s0 ← lift (Array.to_slice node) + let node1 ← verify_mono.xmss_pk_from_sig_free idx_leaf sig_tmp s0 pk_seed adrs2 + let w ← j + 1#u32 + htFoldN a pk_seed hp32 idx_tree1 adrs2 node1 w s + +/-- One full loop step on a non-empty range = one fold step, tail as the + continuation loop. -/ +theorem ht_loop_step {D HP LEN N : Std.Usize} (a : Array (types.XmssSig HP LEN N) D) + (pk_seed : Slice Std.U8) (hp32 : Std.U32) + (start stop : Std.U32) (idx_tree : Std.U64) (adrs : types.Adrs) + (node : Array Std.U8 N) + (hlt : start.val < stop.val) (hb : start.val + 1 < 2 ^ 32) : + verify_mono.ht_verify_free_loop { start := start, «end» := stop } + a pk_seed idx_tree hp32 adrs node + = (do + let i ← 1#u64 <<< hp32 + let i1 ← i - 1#u64 + let i2 ← lift (idx_tree &&& i1) + let idx_leaf ← lift (UScalar.cast .U32 i2) + let idx_tree1 ← idx_tree >>> hp32 + let adrs1 ← helpers.Adrs.set_layer_address adrs start + let adrs2 ← helpers.Adrs.set_tree_address adrs1 idx_tree1 + let i3 ← lift (UScalar.cast .Usize start) + let xs ← Array.index_usize a i3 + let sig_tmp ← types.XmssSig.Insts.CoreCloneClone.clone xs + let s0 ← lift (Array.to_slice node) + let node1 ← verify_mono.xmss_pk_from_sig_free idx_leaf sig_tmp s0 pk_seed adrs2 + let w ← start + 1#u32 + verify_mono.ht_verify_free_loop { start := w, «end» := stop } + a pk_seed idx_tree1 hp32 adrs2 node1) := by + obtain ⟨w, hwok, _⟩ := u32_succ hb + have hd : decide (start.val < stop.val) = true := by simp [hlt] + conv_lhs => rw [verify_mono.ht_verify_free_loop, loop_unfold_bind] + dsimp only + rw [hbody_ht a pk_seed hp32 start stop w idx_tree adrs node hd hwok] + simp only [bind_assoc, bind_ok] + conv_rhs => rw [show (start + 1#u32) = ok w from hwok] + simp only [bind_tc_ok, bind_ok] + rfl + +/-- **Algorithm 12 fidelity.** The extracted hypertree loop over + [start, start+s) equals the explicit layer fold. -/ +theorem ht_loop_eq {D HP LEN N : Std.Usize} (a : Array (types.XmssSig HP LEN N) D) + (pk_seed : Slice Std.U8) (hp32 : Std.U32) (s : Nat) : + ∀ (start : Std.U32) (idx_tree : Std.U64) (adrs : types.Adrs) (node : Array Std.U8 N), + start.val + s < 2 ^ 32 → + ∀ (stop : Std.U32), stop.val = start.val + s → + verify_mono.ht_verify_free_loop { start := start, «end» := stop } + a pk_seed idx_tree hp32 adrs node + = htFoldN a pk_seed hp32 idx_tree adrs node start s := by + induction s with + | zero => + intro start idx_tree adrs node _ stop hstop + have hse : start = stop := by apply Std.UScalar.eq_of_val_eq; omega + subst hse + unfold verify_mono.ht_verify_free_loop htFoldN + rw [loop.eq_1] + unfold verify_mono.ht_verify_free_loop.body core.iter.range.IteratorRange.next + simp [core.cmp.impls.PartialOrdU32.lt] + | succ k ih => + intro start idx_tree adrs node hb stop hstop + have hlt : start.val < stop.val := by omega + have hb1 : start.val + 1 < 2 ^ 32 := by omega + obtain ⟨w, hwok, hwv⟩ := u32_succ hb1 + rw [ht_loop_step a pk_seed hp32 start stop idx_tree adrs node hlt hb1] + unfold htFoldN + rw [hwok] + simp only [bind_tc_ok, bind_ok] + have hbound : w.val + k < 2 ^ 32 := by omega + have hstop' : stop.val = w.val + k := by omega + apply bind_congr; intro i + apply bind_congr; intro i1 + apply bind_congr; intro i2 + apply bind_congr; intro idx_leaf + apply bind_congr; intro idx_tree1 + apply bind_congr; intro adrs1 + apply bind_congr; intro adrs2 + apply bind_congr; intro i3 + apply bind_congr; intro xs + apply bind_congr; intro sig_tmp + apply bind_congr; intro s0 + apply bind_congr; intro node1 + exact ih w idx_tree1 adrs2 node1 hbound stop hstop' + +end fips205 diff --git a/verification/check.sh b/verification/check.sh index 6903a9f..7d3abe7 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -27,6 +27,7 @@ PROOFS=( "ChainSpec" "WotsSpec" "XmssSpec" + "HtSpec" ) # Certificates whose axiom cones are audited, and the allowed extras beyond # the three kernel axioms: the five SHA-2 verify-path oracles. A certificate @@ -35,6 +36,7 @@ CERTS=( "fips205.chain_free_loop_eq" "fips205.wots_loop1_eq" "fips205.xmss_loop_eq" + "fips205.ht_loop_eq" ) ORACLES="verify_mono.oracle.f, verify_mono.oracle.h, verify_mono.oracle.t_l, verify_mono.oracle.t_len, verify_mono.oracle.h_msg" ALLOWED="[propext, Classical.choice, Quot.sound, ${ORACLES}]" @@ -71,7 +73,7 @@ echo "=== Phase 3: axiom audit (cone ⊆ kernel-3 + 5 oracles) ===" cd "$AENEAS_LEAN" AUD="$HERE/Proofs/.audit.lean" { echo "import Proofs.ChainSpec"; echo "import Proofs.WotsSpec" - echo "import Proofs.XmssSpec" + echo "import Proofs.XmssSpec"; echo "import Proofs.HtSpec" for c in "${CERTS[@]}"; do echo "#print axioms $c"; done } > "$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) diff --git a/verification/gen/SlhVerify/Funs.lean b/verification/gen/SlhVerify/Funs.lean index d9c5668..ce866ae 100644 --- a/verification/gen/SlhVerify/Funs.lean +++ b/verification/gen/SlhVerify/Funs.lean @@ -31,16 +31,6 @@ def U32.Insts.CoreIterRangeStep : core.iter.range.Step Std.U32 := { backward_checked := U32.Insts.CoreIterRangeStep.backward_checked } -/-- Trait implementation: [core::num::error::{impl core::fmt::Debug for core::num::error::TryFromIntError}] - Source: '/rustc/library/core/src/num/error.rs', lines 9:9-9:14 - Name pattern: [core::fmt::Debug] -/ -@[reducible, rust_trait_impl - "core::fmt::Debug"] -def core.num.error.TryFromIntError.Insts.CoreFmtDebug : core.fmt.Debug - core.num.error.TryFromIntError := { - fmt := core.num.error.TryFromIntError.Insts.CoreFmtDebug.fmt -} - /-- Trait implementation: [zeroize::{impl zeroize::Zeroize for Z}] Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/zeroize-1.9.0/src/lib.rs', lines 270:0-272:23 Name pattern: [zeroize::Zeroize<@Z>] -/ @@ -633,40 +623,39 @@ def verify_mono.chain_free verify_mono.chain_free_loop { start := i, «end» := i1 } pk_seed adrs1 cap_x /-- [fips205::verify_mono::wots_pk_from_sig_free]: loop body 0: - Source: 'src/verify_mono.rs', lines 118:4-120:5 -/ + Source: 'src/verify_mono.rs', lines 122:4-124:5 -/ @[rust_loop_body] def verify_mono.wots_pk_from_sig_free_loop0.body - (iter : core.iter.adapters.take.Take (core.slice.iter.Iter Std.U32)) - (csum : Std.U32) : - Result (ControlFlow ((core.iter.adapters.take.Take (core.slice.iter.Iter - Std.U32)) × Std.U32) Std.U32) + {LEN : Std.Usize} (msg : Array Std.U32 LEN) + (iter : core.ops.range.Range Std.Usize) (csum : Std.U32) : + Result (ControlFlow ((core.ops.range.Range Std.Usize) × Std.U32) Std.U32) := do let (o, iter1) ← - core.iter.adapters.take.Take.Insts.CoreIterTraitsIteratorIterator.next - (core.iter.traits.iterator.IteratorSliceIter Std.U32) iter + core.iter.range.IteratorRange.next core.iter.range.StepUsize iter match o with | none => ok (done csum) - | some item => - let i ← W - 1#u32 - let i1 ← U32.Insts.CoreOpsArithSubShared0U32U32.sub i item - let csum1 ← csum + i1 + | some i => + let i1 ← W - 1#u32 + let i2 ← Array.index_usize msg i + let i3 ← i1 - i2 + let csum1 ← csum + i3 ok (cont (iter1, csum1)) /-- [fips205::verify_mono::wots_pk_from_sig_free]: loop 0: - Source: 'src/verify_mono.rs', lines 118:4-120:5 -/ + Source: 'src/verify_mono.rs', lines 122:4-124:5 -/ @[rust_loop] def verify_mono.wots_pk_from_sig_free_loop0 - (iter : core.iter.adapters.take.Take (core.slice.iter.Iter Std.U32)) - (csum : Std.U32) : + {LEN : Std.Usize} (iter : core.ops.range.Range Std.Usize) (csum : Std.U32) + (msg : Array Std.U32 LEN) : Result Std.U32 := do loop - (fun (iter1, csum1) => verify_mono.wots_pk_from_sig_free_loop0.body iter1 - csum1) + (fun (iter1, csum1) => verify_mono.wots_pk_from_sig_free_loop0.body msg + iter1 csum1) (iter, csum) /-- [fips205::verify_mono::wots_pk_from_sig_free]: loop body 1: - Source: 'src/verify_mono.rs', lines 131:4-140:5 -/ + Source: 'src/verify_mono.rs', lines 135:4-144:5 -/ @[rust_loop_body] def verify_mono.wots_pk_from_sig_free_loop1.body {LEN : Std.Usize} {N : Std.Usize} (sig : types.WotsSig LEN N) @@ -692,7 +681,7 @@ def verify_mono.wots_pk_from_sig_free_loop1.body ok (cont (iter1, adrs1, a2)) /-- [fips205::verify_mono::wots_pk_from_sig_free]: loop 1: - Source: 'src/verify_mono.rs', lines 131:4-140:5 -/ + Source: 'src/verify_mono.rs', lines 135:4-144:5 -/ @[rust_loop] def verify_mono.wots_pk_from_sig_free_loop1 {LEN : Std.Usize} {N : Std.Usize} (iter : core.ops.range.Range Std.Usize) @@ -706,16 +695,13 @@ def verify_mono.wots_pk_from_sig_free_loop1 (iter, adrs, tmp) /-- [fips205::verify_mono::wots_pk_from_sig_free]: - Source: 'src/verify_mono.rs', lines 107:0-147:1 -/ + Source: 'src/verify_mono.rs', lines 107:0-151:1 -/ def verify_mono.wots_pk_from_sig_free {LEN : Std.Usize} {N : Std.Usize} (sig : types.WotsSig LEN N) (m : Slice Std.U8) (pk_seed : Slice Std.U8) (adrs : types.Adrs) : Result (types.WotsPk N) := do - let r ← U32.Insts.CoreConvertTryFromUsizeTryFromIntError.try_from N - let n32 ← - core.result.Result.unwrap core.num.error.TryFromIntError.Insts.CoreFmtDebug - r + let n32 ← lift (UScalar.cast .U32 N) let adrs1 ← types.Adrs.Insts.CoreCloneClone.clone adrs let a := Array.repeat N 0#u8 let tmp := Array.repeat LEN a @@ -728,38 +714,37 @@ def verify_mono.wots_pk_from_sig_free { start := 0#usize, «end» := i1 } let s1 ← helpers.base_2b m LGW i s let msg1 := index_mut_back s1 - let s2 ← lift (Array.to_slice msg1) - let i2 ← core.slice.Slice.iter s2 - let iter ← core.slice.iter.IteratorSliceIter.take i2 i1 - let csum ← verify_mono.wots_pk_from_sig_free_loop0 iter 0#u32 - let i3 ← LEN2 * LGW - let i4 ← lift (i3 &&& 7#u32) - let i5 ← 8#u32 - i4 - let i6 ← lift (i5 &&& 7#u32) - let csum1 ← csum <<< i6 - let i7 ← i3 + 7#u32 - let i8 ← i7 / 8#u32 - let a1 ← helpers.to_byte csum1 i8 - let s3 ← lift (Array.to_slice a1) - let (s4, index_mut_back1) ← + let csum ← + verify_mono.wots_pk_from_sig_free_loop0 { start := 0#usize, «end» := i1 } + 0#u32 msg1 + let i2 ← LEN2 * LGW + let i3 ← lift (i2 &&& 7#u32) + let i4 ← 8#u32 - i3 + let i5 ← lift (i4 &&& 7#u32) + let csum1 ← csum <<< i5 + let i6 ← i2 + 7#u32 + let i7 ← i6 / 8#u32 + let a1 ← helpers.to_byte csum1 i7 + let s2 ← lift (Array.to_slice a1) + let (s3, index_mut_back1) ← core.array.Array.index_mut (core.ops.index.IndexMutSlice (core.slice.index.SliceIndexRangeFromUsizeSlice Std.U32)) msg1 { start := i1 } - let s5 ← helpers.base_2b s3 LGW LEN2 s4 - let msg2 := index_mut_back1 s5 + let s4 ← helpers.base_2b s2 LGW LEN2 s3 + let msg2 := index_mut_back1 s4 let (adrs2, tmp1) ← verify_mono.wots_pk_from_sig_free_loop1 { start := 0#usize, «end» := LEN } sig pk_seed adrs1 tmp msg2 let wotspk_adrs ← types.Adrs.Insts.CoreCloneClone.clone adrs2 let wotspk_adrs1 ← helpers.Adrs.set_type_and_clear wotspk_adrs types.WOTS_PK - let i9 ← helpers.Adrs.get_key_pair_address adrs2 - let wotspk_adrs2 ← helpers.Adrs.set_key_pair_address wotspk_adrs1 i9 + let i8 ← helpers.Adrs.get_key_pair_address adrs2 + let wotspk_adrs2 ← helpers.Adrs.set_key_pair_address wotspk_adrs1 i8 let pk ← verify_mono.oracle.t_l pk_seed wotspk_adrs2 tmp1 ok pk /-- [fips205::verify_mono::xmss_pk_from_sig_free]: loop body 0: - Source: 'src/verify_mono.rs', lines 169:4-181:5 -/ + Source: 'src/verify_mono.rs', lines 173:4-185:5 -/ @[rust_loop_body] def verify_mono.xmss_pk_from_sig_free_loop.body {HP : Std.Usize} {N : Std.Usize} (idx : Std.U32) (pk_seed : Slice Std.U8) @@ -801,7 +786,7 @@ def verify_mono.xmss_pk_from_sig_free_loop.body ok (cont (iter1, adrs3, node_1)) /-- [fips205::verify_mono::xmss_pk_from_sig_free]: loop 0: - Source: 'src/verify_mono.rs', lines 169:4-181:5 -/ + Source: 'src/verify_mono.rs', lines 173:4-185:5 -/ @[rust_loop] def verify_mono.xmss_pk_from_sig_free_loop {HP : Std.Usize} {N : Std.Usize} (iter : core.ops.range.Range Std.U32) @@ -815,17 +800,14 @@ def verify_mono.xmss_pk_from_sig_free_loop (iter, adrs, node_0) /-- [fips205::verify_mono::xmss_pk_from_sig_free]: - Source: 'src/verify_mono.rs', lines 152:0-184:1 -/ + Source: 'src/verify_mono.rs', lines 156:0-188:1 -/ def verify_mono.xmss_pk_from_sig_free {HP : Std.Usize} {LEN : Std.Usize} {N : Std.Usize} (idx : Std.U32) (sig_xmss : types.XmssSig HP LEN N) (m : Slice Std.U8) (pk_seed : Slice Std.U8) (adrs : types.Adrs) : Result (Array Std.U8 N) := do - let r ← U32.Insts.CoreConvertTryFromUsizeTryFromIntError.try_from HP - let hp32 ← - core.result.Result.unwrap core.num.error.TryFromIntError.Insts.CoreFmtDebug - r + let hp32 ← lift (UScalar.cast .U32 HP) let adrs1 ← types.Adrs.Insts.CoreCloneClone.clone adrs let adrs2 ← helpers.Adrs.set_type_and_clear adrs1 types.WOTS_HASH let adrs3 ← helpers.Adrs.set_key_pair_address adrs2 idx @@ -838,90 +820,75 @@ def verify_mono.xmss_pk_from_sig_free idx pk_seed adrs5 auth wp /-- [fips205::verify_mono::ht_verify_free]: loop body 0: - Source: 'src/verify_mono.rs', lines 202:4-219:1 -/ + Source: 'src/verify_mono.rs', lines 206:4-220:5 -/ @[rust_loop_body] def verify_mono.ht_verify_free_loop.body {D : Std.Usize} {HP : Std.Usize} {LEN : Std.Usize} {N : Std.Usize} (a : Array (types.XmssSig HP LEN N) D) (pk_seed : Slice Std.U8) - (pk_root : Array Std.U8 N) (hp32 : Std.U32) - (iter : core.ops.range.Range Std.U32) (idx_tree : Std.U64) + (hp32 : Std.U32) (iter : core.ops.range.Range Std.U32) (idx_tree : Std.U64) (adrs : types.Adrs) (node : Array Std.U8 N) : Result (ControlFlow ((core.ops.range.Range Std.U32) × Std.U64 × types.Adrs - × (Array Std.U8 N)) Bool) + × (Array Std.U8 N)) (Array Std.U8 N)) := do let (o, iter1) ← core.iter.range.IteratorRange.next U32.Insts.CoreIterRangeStep iter match o with - | none => - let b ← - core.array.equality.PartialEqArray.eq core.cmp.PartialEqU8 node pk_root - ok (done b) + | none => ok (done node) | some j => let i ← 1#u64 <<< hp32 let i1 ← i - 1#u64 let i2 ← lift (idx_tree &&& i1) - let idx_leaf ← U32.Insts.CoreConvertTryFromU64TryFromIntError.try_from i2 - let b ← core.result.Result.is_err idx_leaf - if b - then ok (done false) - else - let idx_leaf1 ← - core.result.Result.unwrap - core.num.error.TryFromIntError.Insts.CoreFmtDebug idx_leaf - let idx_tree1 ← idx_tree >>> hp32 - let adrs1 ← helpers.Adrs.set_layer_address adrs j - let adrs2 ← helpers.Adrs.set_tree_address adrs1 idx_tree1 - let i3 ← lift (UScalar.cast .Usize j) - let xs ← Array.index_usize a i3 - let sig_tmp ← types.XmssSig.Insts.CoreCloneClone.clone xs - let s ← lift (Array.to_slice node) - let node1 ← - verify_mono.xmss_pk_from_sig_free idx_leaf1 sig_tmp s pk_seed adrs2 - ok (cont (iter1, idx_tree1, adrs2, node1)) + let idx_leaf ← lift (UScalar.cast .U32 i2) + let idx_tree1 ← idx_tree >>> hp32 + let adrs1 ← helpers.Adrs.set_layer_address adrs j + let adrs2 ← helpers.Adrs.set_tree_address adrs1 idx_tree1 + let i3 ← lift (UScalar.cast .Usize j) + let xs ← Array.index_usize a i3 + let sig_tmp ← types.XmssSig.Insts.CoreCloneClone.clone xs + let s ← lift (Array.to_slice node) + let node1 ← + verify_mono.xmss_pk_from_sig_free idx_leaf sig_tmp s pk_seed adrs2 + ok (cont (iter1, idx_tree1, adrs2, node1)) /-- [fips205::verify_mono::ht_verify_free]: loop 0: - Source: 'src/verify_mono.rs', lines 202:4-219:1 -/ + Source: 'src/verify_mono.rs', lines 206:4-220:5 -/ @[rust_loop] def verify_mono.ht_verify_free_loop {D : Std.Usize} {HP : Std.Usize} {LEN : Std.Usize} {N : Std.Usize} (iter : core.ops.range.Range Std.U32) (a : Array (types.XmssSig HP LEN N) D) - (pk_seed : Slice Std.U8) (pk_root : Array Std.U8 N) (idx_tree : Std.U64) - (hp32 : Std.U32) (adrs : types.Adrs) (node : Array Std.U8 N) : - Result Bool + (pk_seed : Slice Std.U8) (idx_tree : Std.U64) (hp32 : Std.U32) + (adrs : types.Adrs) (node : Array Std.U8 N) : + Result (Array Std.U8 N) := do loop (fun (iter1, idx_tree1, adrs1, node1) => - verify_mono.ht_verify_free_loop.body a pk_seed pk_root hp32 iter1 - idx_tree1 adrs1 node1) + verify_mono.ht_verify_free_loop.body a pk_seed hp32 iter1 idx_tree1 adrs1 + node1) (iter, idx_tree, adrs, node) /-- [fips205::verify_mono::ht_verify_free]: - Source: 'src/verify_mono.rs', lines 189:0-219:1 -/ + Source: 'src/verify_mono.rs', lines 193:0-223:1 -/ def verify_mono.ht_verify_free {D : Std.Usize} {HP : Std.Usize} {LEN : Std.Usize} {N : Std.Usize} (m : Slice Std.U8) (sig_ht : types.HtSig D HP LEN N) (pk_seed : Slice Std.U8) (idx_tree : Std.U64) (idx_leaf : Std.U32) (pk_root : Array Std.U8 N) : Result Bool := do - let r ← U32.Insts.CoreConvertTryFromUsizeTryFromIntError.try_from D - let d32 ← - core.result.Result.unwrap core.num.error.TryFromIntError.Insts.CoreFmtDebug - r - let r1 ← U32.Insts.CoreConvertTryFromUsizeTryFromIntError.try_from HP - let hp32 ← - core.result.Result.unwrap core.num.error.TryFromIntError.Insts.CoreFmtDebug - r1 + let d32 ← lift (UScalar.cast .U32 D) + let hp32 ← lift (UScalar.cast .U32 HP) let adrs ← types.Adrs.Insts.CoreDefaultDefault.default let adrs1 ← helpers.Adrs.set_tree_address adrs idx_tree let xs ← Array.index_usize sig_ht.xmss_sigs 0#usize let sig_tmp ← types.XmssSig.Insts.CoreCloneClone.clone xs let node ← verify_mono.xmss_pk_from_sig_free idx_leaf sig_tmp m pk_seed adrs1 - verify_mono.ht_verify_free_loop { start := 1#u32, «end» := d32 } - sig_ht.xmss_sigs pk_seed pk_root idx_tree hp32 adrs1 node + let node1 ← + verify_mono.ht_verify_free_loop { start := 1#u32, «end» := d32 } + sig_ht.xmss_sigs pk_seed idx_tree hp32 adrs1 node + core.array.equality.PartialEqArray.eq core.cmp.PartialEqU8 node1 pk_root /-- [fips205::verify_mono::fors_pk_from_sig_free]: loop body 1: - Source: 'src/verify_mono.rs', lines 244:8-256:9 -/ + Source: 'src/verify_mono.rs', lines 248:8-260:9 -/ @[rust_loop_body] def verify_mono.fors_pk_from_sig_free_loop0_loop0.body {A : Std.Usize} {K : Std.Usize} {N : Std.Usize} (pk_seed : Slice Std.U8) @@ -966,7 +933,7 @@ def verify_mono.fors_pk_from_sig_free_loop0_loop0.body ok (cont (iter1, adrs3, node_1)) /-- [fips205::verify_mono::fors_pk_from_sig_free]: loop 1: - Source: 'src/verify_mono.rs', lines 244:8-256:9 -/ + Source: 'src/verify_mono.rs', lines 248:8-260:9 -/ @[rust_loop] def verify_mono.fors_pk_from_sig_free_loop0_loop0 {A : Std.Usize} {K : Std.Usize} {N : Std.Usize} @@ -982,7 +949,7 @@ def verify_mono.fors_pk_from_sig_free_loop0_loop0 (iter, adrs, node_0) /-- [fips205::verify_mono::fors_pk_from_sig_free]: loop body 0: - Source: 'src/verify_mono.rs', lines 234:4-259:5 -/ + Source: 'src/verify_mono.rs', lines 238:4-263:5 -/ @[rust_loop_body] def verify_mono.fors_pk_from_sig_free_loop0.body {A : Std.Usize} {K : Std.Usize} {N : Std.Usize} @@ -1018,7 +985,7 @@ def verify_mono.fors_pk_from_sig_free_loop0.body ok (cont (iter1, adrs3, a1)) /-- [fips205::verify_mono::fors_pk_from_sig_free]: loop 0: - Source: 'src/verify_mono.rs', lines 234:4-259:5 -/ + Source: 'src/verify_mono.rs', lines 238:4-263:5 -/ @[rust_loop] def verify_mono.fors_pk_from_sig_free_loop0 {A : Std.Usize} {K : Std.Usize} {N : Std.Usize} @@ -1033,21 +1000,15 @@ def verify_mono.fors_pk_from_sig_free_loop0 (iter, adrs, root) /-- [fips205::verify_mono::fors_pk_from_sig_free]: - Source: 'src/verify_mono.rs', lines 224:0-266:1 -/ + Source: 'src/verify_mono.rs', lines 228:0-270:1 -/ def verify_mono.fors_pk_from_sig_free {A : Std.Usize} {K : Std.Usize} {N : Std.Usize} (sig_fors : types.ForsSig A K N) (md : Slice Std.U8) (pk_seed : Slice Std.U8) (adrs : types.Adrs) : Result (types.ForsPk N) := do - let r ← U32.Insts.CoreConvertTryFromUsizeTryFromIntError.try_from A - let a32 ← - core.result.Result.unwrap core.num.error.TryFromIntError.Insts.CoreFmtDebug - r - let r1 ← U32.Insts.CoreConvertTryFromUsizeTryFromIntError.try_from K - let k32 ← - core.result.Result.unwrap core.num.error.TryFromIntError.Insts.CoreFmtDebug - r1 + let a32 ← lift (UScalar.cast .U32 A) + let k32 ← lift (UScalar.cast .U32 K) let adrs1 ← types.Adrs.Insts.CoreCloneClone.clone adrs let indices := Array.repeat K 0#u32 let (s, to_slice_mut_back) ← lift (Array.to_slice_mut indices) @@ -1067,7 +1028,7 @@ def verify_mono.fors_pk_from_sig_free ok { key := pk } /-- [fips205::verify_mono::slh_verify_internal_free]: - Source: 'src/verify_mono.rs', lines 272:0-329:1 -/ + Source: 'src/verify_mono.rs', lines 276:0-332:1 -/ def verify_mono.slh_verify_internal_free {A : Std.Usize} {D : Std.Usize} (H : Std.Usize) {HP : Std.Usize} {K : Std.Usize} {LEN : Std.Usize} (M : Std.Usize) {N : Std.Usize} @@ -1075,14 +1036,8 @@ def verify_mono.slh_verify_internal_free (pk : types.SlhPublicKey N) : Result Bool := do - let r ← U32.Insts.CoreConvertTryFromUsizeTryFromIntError.try_from D - let d32 ← - core.result.Result.unwrap core.num.error.TryFromIntError.Insts.CoreFmtDebug - r - let r1 ← U32.Insts.CoreConvertTryFromUsizeTryFromIntError.try_from H - let h32 ← - core.result.Result.unwrap core.num.error.TryFromIntError.Insts.CoreFmtDebug - r1 + let d32 ← lift (UScalar.cast .U32 D) + let h32 ← lift (UScalar.cast .U32 H) let adrs ← types.Adrs.Insts.CoreDefaultDefault.default let s ← lift (Array.to_slice sig.randomness) let s1 ← lift (Array.to_slice pk.pk_seed) @@ -1132,25 +1087,16 @@ def verify_mono.slh_verify_internal_free let idx_leaf ← lift (i22 &&& i24) let adrs1 ← helpers.Adrs.set_tree_address adrs idx_tree let adrs2 ← helpers.Adrs.set_type_and_clear adrs1 types.FORS_TREE - let idx_leaf_u32 ← - U32.Insts.CoreConvertTryFromU64TryFromIntError.try_from idx_leaf - let b ← core.result.Result.is_err idx_leaf_u32 - if b - then ok false - else - let idx_leaf_u321 ← - core.result.Result.unwrap - core.num.error.TryFromIntError.Insts.CoreFmtDebug idx_leaf_u32 - let adrs3 ← helpers.Adrs.set_key_pair_address adrs2 idx_leaf_u321 - let s3 ← lift (Array.to_slice pk.pk_seed) - let pk_fors ← verify_mono.fors_pk_from_sig_free sig.fors_sig md s3 adrs3 - let s4 ← lift (Array.to_slice pk_fors.key) - let s5 ← lift (Array.to_slice pk.pk_seed) - verify_mono.ht_verify_free s4 sig.ht_sig s5 idx_tree idx_leaf_u321 - pk.pk_root + let idx_leaf_u32 ← lift (UScalar.cast .U32 idx_leaf) + let adrs3 ← helpers.Adrs.set_key_pair_address adrs2 idx_leaf_u32 + let s3 ← lift (Array.to_slice pk.pk_seed) + let pk_fors ← verify_mono.fors_pk_from_sig_free sig.fors_sig md s3 adrs3 + let s4 ← lift (Array.to_slice pk_fors.key) + let s5 ← lift (Array.to_slice pk.pk_seed) + verify_mono.ht_verify_free s4 sig.ht_sig s5 idx_tree idx_leaf_u32 pk.pk_root /-- [fips205::verify_mono::slh_verify_128s]: - Source: 'src/verify_mono.rs', lines 338:0-342:1 -/ + Source: 'src/verify_mono.rs', lines 341:0-345:1 -/ def verify_mono.slh_verify_128s (mprime : Slice Std.U8) (sig : types.SlhDsaSig 12#usize 7#usize 9#usize 14#usize 35#usize 16#usize) diff --git a/verification/gen/SlhVerify/FunsExternal.lean b/verification/gen/SlhVerify/FunsExternal.lean index 122d691..46d98a1 100644 --- a/verification/gen/SlhVerify/FunsExternal.lean +++ b/verification/gen/SlhVerify/FunsExternal.lean @@ -17,14 +17,17 @@ axioms — nothing else. (2) TRANSPILER PLUMBING — core-library externals Aeneas emits for this - extraction config (u32::try_from, Result::is_err, the iterator Step / - Take machinery driving `for` ranges, the zeroize blanket impls, the - TryFromIntError Debug impl). These carry NO cryptographic content. - They are adopted here as axioms so the model type-checks at phase 1 - (no certificates exist yet, so H4's cone requirement is vacuous). The - proof phase will discharge each from Aeneas.Std / real definitions and - the #print axioms audit will then confirm only class (1) survives in - any certificate cone. Tracked as the phase-2 de-plumbing item. + extraction config. These carry NO cryptographic content. The u32 + range Step machinery is DISCHARGED below with real definitions + (2026-07-22). The try_from / is_err / &u32-Sub / wots-Take / + Debug-fmt axioms were ELIMINATED at source level by the + fips205-source de-plumbing patch (8 sites, semantics identical, + differential-test-validated) and their declarations deleted here + (dead-stub rule, 2026-07-23). Remaining as axioms: the Take + iterator machinery used by helpers::to_int (slh_verify_internal's + digest split — the apex round's de-plumbing item) and the zeroize + blanket impls (never on the verify path). The #print axioms audit + confirms only class (1) survives in any certificate cone. ────────────────────────────────────────────────────────────────────────────── -/ -- This is a template file: rename it to "FunsExternal.lean" and fill the holes. import Aeneas @@ -41,36 +44,6 @@ set_option maxHeartbeats 1000000 set_option maxRecDepth 2048 open fips205 -/-- [core::convert::num::ptr_try_from_impls::{impl core::convert::TryFrom for u32}::try_from]: - Source: '/rustc/library/core/src/convert/num.rs', lines 300:12-300:64 - Name pattern: [core::convert::num::ptr_try_from_impls::{core::convert::TryFrom}::try_from] - Visibility: public -/ -@[rust_fun - "core::convert::num::ptr_try_from_impls::{core::convert::TryFrom}::try_from"] -axiom U32.Insts.CoreConvertTryFromUsizeTryFromIntError.try_from - : - Std.Usize → Result (core.result.Result Std.U32 - core.num.error.TryFromIntError) - -/-- [core::convert::num::{impl core::convert::TryFrom for u32}::try_from]: - Source: '/rustc/library/core/src/convert/num.rs', lines 300:12-300:64 - Name pattern: [core::convert::num::{core::convert::TryFrom}::try_from] - Visibility: public -/ -@[rust_fun - "core::convert::num::{core::convert::TryFrom}::try_from"] -axiom U32.Insts.CoreConvertTryFromU64TryFromIntError.try_from - : - Std.U64 → Result (core.result.Result Std.U32 - core.num.error.TryFromIntError) - -/-- [core::ops::arith::{impl core::ops::arith::Sub<&'_0 u32, u32> for u32}::sub]: - Source: '/rustc/library/core/src/internal_macros.rs', lines 38:12-38:68 - Name pattern: [core::ops::arith::{core::ops::arith::Sub}::sub] - Visibility: public -/ -@[rust_fun "core::ops::arith::{core::ops::arith::Sub}::sub"] -axiom U32.Insts.CoreOpsArithSubShared0U32U32.sub - : Std.U32 → Std.U32 → Result Std.U32 - /-- [core::iter::adapters::take::{impl core::iter::traits::iterator::Iterator for core::iter::adapters::take::Take}::next]: Source: '/rustc/library/core/src/iter/adapters/take.rs', lines 36:4-36:55 Name pattern: [core::iter::adapters::take::{core::iter::traits::iterator::Iterator, @Clause0_Item>}::next] @@ -130,35 +103,6 @@ def U32.Insts.CoreIterRangeStep.steps_between let steps := Std.Usize.ofNatCore (end_.val - start.val) (by scalar_tac) ok (steps, some steps) -/-- [core::iter::traits::iterator::Iterator::take]: - Source: '/rustc/library/core/src/iter/traits/iterator.rs', lines 1447:4-1449:20 - Name pattern: [core::iter::traits::iterator::Iterator::take] - Visibility: public -/ -@[rust_fun "core::iter::traits::iterator::Iterator::take"] -axiom core.iter.traits.iterator.Iterator.take.default - {Self : Type} {Clause0_Item : Type} (IteratorInst : - core.iter.traits.iterator.Iterator Self Clause0_Item) : - Self → Std.Usize → Result (core.iter.adapters.take.Take Self) - -/-- [core::num::error::{impl core::fmt::Debug for core::num::error::TryFromIntError}::fmt]: - Source: '/rustc/library/core/src/num/error.rs', lines 9:9-9:14 - Name pattern: [core::num::error::{core::fmt::Debug}::fmt] - Visibility: public -/ -@[rust_fun - "core::num::error::{core::fmt::Debug}::fmt"] -axiom core.num.error.TryFromIntError.Insts.CoreFmtDebug.fmt - : - core.num.error.TryFromIntError → core.fmt.Formatter → Result - ((core.result.Result Unit core.fmt.Error) × core.fmt.Formatter) - -/-- [core::result::{core::result::Result}::is_err]: - Source: '/rustc/library/core/src/result.rs', lines 646:4-646:38 - Name pattern: [core::result::{core::result::Result<@T, @E>}::is_err] - Visibility: public -/ -@[rust_fun "core::result::{core::result::Result<@T, @E>}::is_err"] -axiom core.result.Result.is_err - {T : Type} {E : Type} : core.result.Result T E → Result Bool - /-- [zeroize::{impl zeroize::Zeroize for Z}::zeroize]: Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/zeroize-1.9.0/src/lib.rs', lines 274:4-274:25 Name pattern: [zeroize::{zeroize::Zeroize<@Z>}::zeroize] diff --git a/verification/gen/SlhVerify/Types.lean b/verification/gen/SlhVerify/Types.lean index 62c72c6..bea3447 100644 --- a/verification/gen/SlhVerify/Types.lean +++ b/verification/gen/SlhVerify/Types.lean @@ -1,7 +1,6 @@ -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS -- [fips205]: type definitions import Aeneas -import SlhVerify.TypesExternal open Aeneas Aeneas.Std Result ControlFlow Error set_option linter.dupNamespace false set_option linter.hashCommand false diff --git a/verification/gen/SlhVerify/TypesExternal.lean b/verification/gen/SlhVerify/TypesExternal.lean index 6829973..585cab4 100644 --- a/verification/gen/SlhVerify/TypesExternal.lean +++ b/verification/gen/SlhVerify/TypesExternal.lean @@ -14,10 +14,4 @@ set_option maxHeartbeats 1000000 /- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/ set_option maxRecDepth 2048 -/-- [core::num::error::TryFromIntError] - Source: '/rustc/library/core/src/num/error.rs', lines 10:0-10:26 - Name pattern: [core::num::error::TryFromIntError] - Visibility: public -/ -@[rust_type "core::num::error::TryFromIntError"] -axiom core.num.error.TryFromIntError : Type