From 015f467954f86051022a91cb0c4c6df1f74c44bf Mon Sep 17 00:00:00 2001 From: mrwulf Date: Fri, 24 Jul 2026 08:55:34 +0200 Subject: [PATCH] =?UTF-8?q?phase=202:=20INPUT-PREP=20layer=20=E2=80=94=20t?= =?UTF-8?q?o=5Fint,=20to=5Fbyte,=20WOTS+=20checksum=20(3=20kernel-3=20cert?= =?UTF-8?q?s)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Three straight-line range-loop fidelity theorems (Proofs/InputPrepSpec.lean), each #print axioms = EXACTLY [propext, Classical.choice, Quot.sound] — pure byte/bit arithmetic, NO hash oracle enters (the cleanest cones in the campaign): - fips205.to_int_loop_eq (Algorithm 2, toInt): the extracted big-endian byte->u64 loop = the fold total <- (total<<8) + x[i]. - fips205.to_byte_loop_eq (Algorithm 3, toByte): the extracted u32->byte loop = the fold writing s[n-1-i] and shifting total right by 8. - fips205.wots_csum_loop_eq: the WOTS+ checksum loop = the fold csum <- csum + (W-1-msg[i]). All three are the straight-line recipe (hbody -> step lemma closed by rfl -> induction with bind_congr per bind). to_int + checksum use the usize range helpers (WotsSpec), to_byte the u32 range (ChainSpec); loop_unfold_bind reused. Also in this commit — DE-PLUMBING ROUND 2 landed (source bea1051, separate commit in fips205-source): to_int's iter().take() and base_2b's iter_mut() became index loops, so both extract to real definitions. Consequently: - gen/ regenerated (to_int_loop / base_2b_loop0 now clean StepUsize range loops with Slice.index_usize / Slice.update; the six prior certificates recompiled UNCHANGED and re-audited green against the new gen). - The core::iter::adapters::take::Take::next AXIOM — the LAST non-oracle, non-zeroize plumbing axiom on the verify path — is now unreferenced and was DELETED from FunsExternal (dead-stub hygiene rule). The model's external surface is now EXACTLY: the 5 SHA-2 oracles + 3 zeroize blanket impls (never on the verify path) + the discharged-real u32 Step defs. Nothing else. Fidelity review at authorship (three-way): extracted loop bodies (gen Funs.lean) == Rust helpers.rs to_int/to_byte + verify_mono checksum (verbatim FIPS 205 Alg 2/3) == the folds above. check.sh: PROOFS += InputPrepSpec; CERTS += the 3 certs; audit imports it. Green over ALL NINE certificates at default caps (400s/4096MB). Co-Authored-By: Claude Fable 5 --- verification/Proofs/InputPrepSpec.lean | 284 +++++++++++++++++++ verification/check.sh | 6 +- verification/gen/SlhVerify/Funs.lean | 120 ++++---- verification/gen/SlhVerify/FunsExternal.lean | 14 +- 4 files changed, 349 insertions(+), 75 deletions(-) create mode 100644 verification/Proofs/InputPrepSpec.lean diff --git a/verification/Proofs/InputPrepSpec.lean b/verification/Proofs/InputPrepSpec.lean new file mode 100644 index 0000000..fa0ffbd --- /dev/null +++ b/verification/Proofs/InputPrepSpec.lean @@ -0,0 +1,284 @@ +/- Proofs/InputPrepSpec.lean — input-preparation loop fidelity (FIPS 205 + helpers: to_int, to_byte, and the WOTS+ checksum loop). + + Three straight-line range-loop fidelity theorems, all KERNEL-3 CLEAN (pure + byte/bit arithmetic — no hash oracle enters these). They pin the message- + and index-preparation steps that feed the verify path: + + - to_int_loop_eq (Algorithm 2, toInt): the extracted big-endian byte→u64 + accumulation loop equals the explicit fold total ← (total≪8) + x[i]. + - to_byte_loop_eq (Algorithm 3, toByte): the extracted u32→byte loop equals + the explicit fold writing s[n−1−i] and shifting total right by 8. + - wots_csum_loop_eq: the WOTS+ checksum accumulation csum ← csum + (W−1−msg[i]). + + All three are the HtSpec straight-line recipe (no branches): hbody → + step lemma (rfl close) → induction (bind_congr per bind, exact ih). to_int + and the checksum use the usize range (usize_succ/fwd_succ_usize/hnext_usize + from WotsSpec); to_byte uses the u32 range (u32_succ/fwd_succ/hnext from + ChainSpec). loop_unfold_bind reused throughout. + + These are the last non-apex layer: after de-plumbing round 2 (to_int/base_2b + index loops) the model carries NO plumbing axioms on the verify path. +-/ +import Proofs.WotsSpec -- transitively imports ChainSpec (u32 range helpers too) +open Aeneas Aeneas.Std Result ControlFlow +open fips205 + +set_option maxHeartbeats 4000000 + +namespace fips205 + +/- ── to_int (Algorithm 2): big-endian n-byte → u64 ─────────────────────────── -/ + +theorem hbody_ti (x : Slice Std.U8) (start stop w : Std.Usize) (total : Std.U64) + (hd : decide (start.val < stop.val) = true) (hwok : start + 1#usize = ok w) : + helpers.to_int_loop.body x { start := start, «end» := stop } total + = (do + let i1 ← total <<< 8#i32 + let i2 ← Slice.index_usize x start + let i3 ← lift (core.convert.num.FromU64U8.from i2) + let total1 ← i1 + i3 + ok (cont (({ start := w, «end» := stop } : core.ops.range.Range Std.Usize), total1))) := by + unfold helpers.to_int_loop.body + rw [hnext_usize hd hwok] + simp + +noncomputable def toIntFold (x : Slice Std.U8) : + Std.U64 → Std.Usize → Nat → Result Std.U64 + | total, _, 0 => ok total + | total, i, (s+1) => do + let i1 ← total <<< 8#i32 + let i2 ← Slice.index_usize x i + let i3 ← lift (core.convert.num.FromU64U8.from i2) + let total1 ← i1 + i3 + let i' ← i + 1#usize + toIntFold x total1 i' s + +theorem to_int_step (x : Slice Std.U8) (start stop : Std.Usize) (total : Std.U64) + (hlt : start.val < stop.val) (hb : start.val + 1 < 2 ^ System.Platform.numBits) : + helpers.to_int_loop { start := start, «end» := stop } x total + = (do + let i1 ← total <<< 8#i32 + let i2 ← Slice.index_usize x start + let i3 ← lift (core.convert.num.FromU64U8.from i2) + let total1 ← i1 + i3 + let i' ← start + 1#usize + helpers.to_int_loop { start := i', «end» := stop } x total1) := by + obtain ⟨w, hwok, _⟩ := usize_succ hb + have hd : decide (start.val < stop.val) = true := by simp [hlt] + conv_lhs => rw [helpers.to_int_loop, loop_unfold_bind] + dsimp only + rw [hbody_ti x start stop w total hd hwok] + simp only [bind_assoc, bind_ok] + conv_rhs => rw [show (start + 1#usize) = ok w from hwok] + simp only [bind_tc_ok, bind_ok] + rfl + +/-- **Algorithm 2 (toInt) fidelity.** -/ +theorem to_int_loop_eq (x : Slice Std.U8) (s : Nat) : + ∀ (start : Std.Usize) (total : Std.U64), + start.val + s < 2 ^ System.Platform.numBits → + ∀ (stop : Std.Usize), stop.val = start.val + s → + helpers.to_int_loop { start := start, «end» := stop } x total + = toIntFold x total start s := by + induction s with + | zero => + intro start total _ stop hstop + have hse : start = stop := by apply Std.UScalar.eq_of_val_eq; omega + subst hse + unfold helpers.to_int_loop toIntFold + rw [loop.eq_1] + unfold helpers.to_int_loop.body core.iter.range.IteratorRange.next + simp [core.iter.range.StepUsize, core.cmp.impls.PartialOrdUsize.lt] + | succ k ih => + intro start total hb stop hstop + have hlt : start.val < stop.val := by omega + have hb1 : start.val + 1 < 2 ^ System.Platform.numBits := by scalar_tac + obtain ⟨w, hwok, hwv⟩ := usize_succ hb1 + rw [to_int_step x start stop total hlt hb1] + unfold toIntFold + rw [hwok] + simp only [bind_tc_ok, bind_ok] + have hbound : w.val + k < 2 ^ System.Platform.numBits := by scalar_tac + have hstop' : stop.val = w.val + k := by omega + apply bind_congr; intro i1 + apply bind_congr; intro i2 + apply bind_congr; intro i3 + apply bind_congr; intro total1 + exact ih w total1 hbound stop hstop' + +/- ── to_byte (Algorithm 3): u32 → n big-endian bytes ───────────────────────── -/ + +theorem hbody_tb (n : Std.U32) (start stop w : Std.U32) + (s : Array Std.U8 2#usize) (total : Std.U32) + (hd : decide (start.val < stop.val) = true) (hwok : start + 1#u32 = ok w) : + helpers.to_byte_loop.body n { start := start, «end» := stop } s total + = (do + let a ← lift (core.num.U32.to_le_bytes total) + let i1 ← Array.index_usize a 0#usize + let i2 ← n - 1#u32 + let i3 ← i2 - start + let i4 ← lift (UScalar.cast .Usize i3) + let a1 ← Array.update s i4 i1 + let total1 ← total >>> 8#i32 + ok (cont (({ start := w, «end» := stop } : core.ops.range.Range Std.U32), a1, total1))) := by + unfold helpers.to_byte_loop.body + rw [hnext hd hwok] + simp + +noncomputable def toByteFold (n : Std.U32) : + Array Std.U8 2#usize → Std.U32 → Std.U32 → Nat → Result (Array Std.U8 2#usize) + | s, _, _, 0 => ok s + | s, total, i, (k+1) => do + let a ← lift (core.num.U32.to_le_bytes total) + let i1 ← Array.index_usize a 0#usize + let i2 ← n - 1#u32 + let i3 ← i2 - i + let i4 ← lift (UScalar.cast .Usize i3) + let a1 ← Array.update s i4 i1 + let total1 ← total >>> 8#i32 + let i' ← i + 1#u32 + toByteFold n a1 total1 i' k + +theorem to_byte_step (n : Std.U32) (start stop : Std.U32) + (s : Array Std.U8 2#usize) (total : Std.U32) + (hlt : start.val < stop.val) (hb : start.val + 1 < 2 ^ 32) : + helpers.to_byte_loop { start := start, «end» := stop } n s total + = (do + let a ← lift (core.num.U32.to_le_bytes total) + let i1 ← Array.index_usize a 0#usize + let i2 ← n - 1#u32 + let i3 ← i2 - start + let i4 ← lift (UScalar.cast .Usize i3) + let a1 ← Array.update s i4 i1 + let total1 ← total >>> 8#i32 + let i' ← start + 1#u32 + helpers.to_byte_loop { start := i', «end» := stop } n a1 total1) := by + obtain ⟨w, hwok, _⟩ := u32_succ hb + have hd : decide (start.val < stop.val) = true := by simp [hlt] + conv_lhs => rw [helpers.to_byte_loop, loop_unfold_bind] + dsimp only + rw [hbody_tb n start stop w s total 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 3 (toByte) fidelity.** -/ +theorem to_byte_loop_eq (n : Std.U32) (k : Nat) : + ∀ (start : Std.U32) (s : Array Std.U8 2#usize) (total : Std.U32), + start.val + k < 2 ^ 32 → + ∀ (stop : Std.U32), stop.val = start.val + k → + helpers.to_byte_loop { start := start, «end» := stop } n s total + = toByteFold n s total start k := by + induction k with + | zero => + intro start s total _ stop hstop + have hse : start = stop := by apply Std.UScalar.eq_of_val_eq; omega + subst hse + unfold helpers.to_byte_loop toByteFold + rw [loop.eq_1] + unfold helpers.to_byte_loop.body core.iter.range.IteratorRange.next + simp [core.cmp.impls.PartialOrdU32.lt] + | succ k ih => + intro start s total 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 [to_byte_step n start stop s total hlt hb1] + unfold toByteFold + 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 a + apply bind_congr; intro i1 + apply bind_congr; intro i2 + apply bind_congr; intro i3 + apply bind_congr; intro i4 + apply bind_congr; intro a1 + apply bind_congr; intro total1 + exact ih w a1 total1 hbound stop hstop' + +/- ── WOTS+ checksum accumulation ───────────────────────────────────────────── -/ + +theorem hbody_cs {LEN : Std.Usize} (msg : Array Std.U32 LEN) + (start stop w : Std.Usize) (csum : Std.U32) + (hd : decide (start.val < stop.val) = true) (hwok : start + 1#usize = ok w) : + verify_mono.wots_pk_from_sig_free_loop0.body msg { start := start, «end» := stop } csum + = (do + let i1 ← W - 1#u32 + let i2 ← Array.index_usize msg start + let i3 ← i1 - i2 + let csum1 ← csum + i3 + ok (cont (({ start := w, «end» := stop } : core.ops.range.Range Std.Usize), csum1))) := by + unfold verify_mono.wots_pk_from_sig_free_loop0.body + rw [hnext_usize hd hwok] + simp + +noncomputable def wotsCsumFold {LEN : Std.Usize} (msg : Array Std.U32 LEN) : + Std.U32 → Std.Usize → Nat → Result Std.U32 + | csum, _, 0 => ok csum + | csum, i, (s+1) => do + let i1 ← W - 1#u32 + let i2 ← Array.index_usize msg i + let i3 ← i1 - i2 + let csum1 ← csum + i3 + let i' ← i + 1#usize + wotsCsumFold msg csum1 i' s + +theorem wots_csum_step {LEN : Std.Usize} (msg : Array Std.U32 LEN) + (start stop : Std.Usize) (csum : Std.U32) + (hlt : start.val < stop.val) (hb : start.val + 1 < 2 ^ System.Platform.numBits) : + verify_mono.wots_pk_from_sig_free_loop0 { start := start, «end» := stop } csum msg + = (do + let i1 ← W - 1#u32 + let i2 ← Array.index_usize msg start + let i3 ← i1 - i2 + let csum1 ← csum + i3 + let i' ← start + 1#usize + verify_mono.wots_pk_from_sig_free_loop0 { start := i', «end» := stop } csum1 msg) := by + obtain ⟨w, hwok, _⟩ := usize_succ hb + have hd : decide (start.val < stop.val) = true := by simp [hlt] + conv_lhs => rw [verify_mono.wots_pk_from_sig_free_loop0, loop_unfold_bind] + dsimp only + rw [hbody_cs msg start stop w csum hd hwok] + simp only [bind_assoc, bind_ok] + conv_rhs => rw [show (start + 1#usize) = ok w from hwok] + simp only [bind_tc_ok, bind_ok] + rfl + +/-- **WOTS+ checksum-loop fidelity.** -/ +theorem wots_csum_loop_eq {LEN : Std.Usize} (msg : Array Std.U32 LEN) (s : Nat) : + ∀ (start : Std.Usize) (csum : Std.U32), + start.val + s < 2 ^ System.Platform.numBits → + ∀ (stop : Std.Usize), stop.val = start.val + s → + verify_mono.wots_pk_from_sig_free_loop0 { start := start, «end» := stop } csum msg + = wotsCsumFold msg csum start s := by + induction s with + | zero => + intro start csum _ stop hstop + have hse : start = stop := by apply Std.UScalar.eq_of_val_eq; omega + subst hse + unfold verify_mono.wots_pk_from_sig_free_loop0 wotsCsumFold + rw [loop.eq_1] + unfold verify_mono.wots_pk_from_sig_free_loop0.body core.iter.range.IteratorRange.next + simp [core.iter.range.StepUsize, core.cmp.impls.PartialOrdUsize.lt] + | succ k ih => + intro start csum hb stop hstop + have hlt : start.val < stop.val := by omega + have hb1 : start.val + 1 < 2 ^ System.Platform.numBits := by scalar_tac + obtain ⟨w, hwok, hwv⟩ := usize_succ hb1 + rw [wots_csum_step msg start stop csum hlt hb1] + unfold wotsCsumFold + rw [hwok] + simp only [bind_tc_ok, bind_ok] + have hbound : w.val + k < 2 ^ System.Platform.numBits := by scalar_tac + have hstop' : stop.val = w.val + k := by omega + apply bind_congr; intro i1 + apply bind_congr; intro i2 + apply bind_congr; intro i3 + apply bind_congr; intro csum1 + exact ih w csum1 hbound stop hstop' + +end fips205 diff --git a/verification/check.sh b/verification/check.sh index e408cff..6853e1a 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -30,6 +30,7 @@ PROOFS=( "HtSpec" "ForsInnerSpec" "ForsOuterSpec" + "InputPrepSpec" ) # Certificates whose axiom cones are audited, and the allowed extras beyond # the three kernel axioms: the five SHA-2 verify-path oracles. A certificate @@ -41,6 +42,9 @@ CERTS=( "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" ) 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}]" @@ -78,7 +82,7 @@ cd "$AENEAS_LEAN" AUD="$HERE/Proofs/.audit.lean" { echo "import Proofs.ChainSpec"; echo "import Proofs.WotsSpec" echo "import Proofs.XmssSpec"; echo "import Proofs.HtSpec" - echo "import Proofs.ForsInnerSpec"; echo "import Proofs.ForsOuterSpec" + echo "import Proofs.ForsInnerSpec"; echo "import Proofs.ForsOuterSpec"; echo "import Proofs.InputPrepSpec" 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 ce866ae..ff9b68d 100644 --- a/verification/gen/SlhVerify/Funs.lean +++ b/verification/gen/SlhVerify/Funs.lean @@ -59,48 +59,45 @@ def Array.Insts.ZeroizeZeroize {Z : Type} (N : Std.Usize) (ZeroizeInst : } /-- [fips205::helpers::to_int]: loop body 0: - Source: 'src/helpers.rs', lines 17:4-23:5 -/ + Source: 'src/helpers.rs', lines 20:4-26:5 -/ @[rust_loop_body] def helpers.to_int_loop.body - (iter : core.iter.adapters.take.Take (core.slice.iter.Iter Std.U8)) - (total : Std.U64) : - Result (ControlFlow ((core.iter.adapters.take.Take (core.slice.iter.Iter - Std.U8)) × Std.U64) Std.U64) + (x : Slice Std.U8) (iter : core.ops.range.Range Std.Usize) (total : Std.U64) + : + Result (ControlFlow ((core.ops.range.Range Std.Usize) × Std.U64) Std.U64) := do let (o, iter1) ← - core.iter.adapters.take.Take.Insts.CoreIterTraitsIteratorIterator.next - (core.iter.traits.iterator.IteratorSliceIter Std.U8) iter + core.iter.range.IteratorRange.next core.iter.range.StepUsize iter match o with | none => ok (done total) - | some item => - let i ← total <<< 8#i32 - let i1 ← lift (core.convert.num.FromU64U8.from item) - let total1 ← i + i1 + | some i => + let i1 ← total <<< 8#i32 + let i2 ← Slice.index_usize x i + let i3 ← lift (core.convert.num.FromU64U8.from i2) + let total1 ← i1 + i3 ok (cont (iter1, total1)) /-- [fips205::helpers::to_int]: loop 0: - Source: 'src/helpers.rs', lines 17:4-23:5 -/ + Source: 'src/helpers.rs', lines 20:4-26:5 -/ @[rust_loop] def helpers.to_int_loop - (iter : core.iter.adapters.take.Take (core.slice.iter.Iter Std.U8)) - (total : Std.U64) : + (iter : core.ops.range.Range Std.Usize) (x : Slice Std.U8) (total : Std.U64) + : Result Std.U64 := do loop - (fun (iter1, total1) => helpers.to_int_loop.body iter1 total1) + (fun (iter1, total1) => helpers.to_int_loop.body x iter1 total1) (iter, total) /-- [fips205::helpers::to_int]: - Source: 'src/helpers.rs', lines 9:0-27:1 -/ + Source: 'src/helpers.rs', lines 9:0-30:1 -/ def helpers.to_int (x : Slice Std.U8) (n : Std.U32) : Result Std.U64 := do let left_val := Slice.len x let right_val ← lift (UScalar.cast .Usize n) massert (left_val = right_val) massert (n <= 8#u32) - let i ← core.slice.Slice.iter x - let i1 ← lift (UScalar.cast .Usize n) - let iter ← core.slice.iter.IteratorSliceIter.take i i1 - helpers.to_int_loop iter 0#u64 + let i ← lift (UScalar.cast .Usize n) + helpers.to_int_loop { start := 0#usize, «end» := i } x 0#u64 /-- [fips205::LEN2] Source: 'src/lib.rs', lines 74:0-74:20 -/ @@ -111,7 +108,7 @@ def helpers.to_int (x : Slice Std.U8) (n : Std.U32) : Result Std.U64 := do @[global_simps, irreducible] def LGW : Std.U32 := 4#u32 /-- [fips205::helpers::to_byte]: loop body 0: - Source: 'src/helpers.rs', lines 44:4-53:5 -/ + Source: 'src/helpers.rs', lines 47:4-56:5 -/ @[rust_loop_body] def helpers.to_byte_loop.body (n : Std.U32) (iter : core.ops.range.Range Std.U32) @@ -134,7 +131,7 @@ def helpers.to_byte_loop.body ok (cont (iter1, a1, total1)) /-- [fips205::helpers::to_byte]: loop 0: - Source: 'src/helpers.rs', lines 44:4-53:5 -/ + Source: 'src/helpers.rs', lines 47:4-56:5 -/ @[rust_loop] def helpers.to_byte_loop (iter : core.ops.range.Range Std.U32) (n : Std.U32) @@ -146,7 +143,7 @@ def helpers.to_byte_loop (iter, s, total) /-- [fips205::helpers::to_byte]: - Source: 'src/helpers.rs', lines 35:0-57:1 -/ + Source: 'src/helpers.rs', lines 38:0-60:1 -/ def helpers.to_byte (x : Std.U32) (n : Std.U32) : Result (Array Std.U8 2#usize) := do let s := Array.repeat 2#usize 0#u8 @@ -160,7 +157,7 @@ def helpers.to_byte helpers.to_byte_loop { start := 0#u32, «end» := n } n s x /-- [fips205::helpers::base_2b]: loop body 1: - Source: 'src/helpers.rs', lines 83:8-95:9 -/ + Source: 'src/helpers.rs', lines 90:8-102:9 -/ @[rust_loop_body] def helpers.base_2b_loop0_loop0.body (x : Slice Std.U8) (b : Std.U32) (inn : Std.Usize) (bits : Std.U32) @@ -180,7 +177,7 @@ def helpers.base_2b_loop0_loop0.body else ok (done (inn, bits, total)) /-- [fips205::helpers::base_2b]: loop 1: - Source: 'src/helpers.rs', lines 83:8-95:9 -/ + Source: 'src/helpers.rs', lines 90:8-102:9 -/ @[rust_loop] def helpers.base_2b_loop0_loop0 (x : Slice Std.U8) (b : Std.U32) (inn : Std.Usize) (bits : Std.U32) @@ -193,48 +190,46 @@ def helpers.base_2b_loop0_loop0 (inn, bits, total) /-- [fips205::helpers::base_2b]: loop body 0: - Source: 'src/helpers.rs', lines 80:4-104:5 -/ + Source: 'src/helpers.rs', lines 87:4-111:5 -/ @[rust_loop_body] def helpers.base_2b_loop0.body - (x : Slice Std.U8) (b : Std.U32) (iter : core.slice.iter.IterMut Std.U32) - (back : core.slice.iter.IterMut Std.U32 → core.slice.iter.IterMut Std.U32) - (inn : Std.Usize) (bits : Std.U32) (total : Std.U32) : - Result (ControlFlow ((core.slice.iter.IterMut Std.U32) × - (core.slice.iter.IterMut Std.U32 → core.slice.iter.IterMut Std.U32) × - Std.Usize × Std.U32 × Std.U32) (core.slice.iter.IterMut Std.U32)) + (x : Slice Std.U8) (b : Std.U32) (iter : core.ops.range.Range Std.Usize) + (baseb : Slice Std.U32) (inn : Std.Usize) (bits : Std.U32) (total : Std.U32) + : + Result (ControlFlow ((core.ops.range.Range Std.Usize) × (Slice Std.U32) × + Std.Usize × Std.U32 × Std.U32) (Slice Std.U32)) := do - let (o, iter1, next_back) ← core.slice.iter.IteratorIterMut.next iter + let (o, iter1) ← + core.iter.range.IteratorRange.next core.iter.range.StepUsize iter match o with - | none => ok (done (let im := next_back iter1 none - back im)) - | some _ => + | none => ok (done baseb) + | some out => let (inn1, bits1, total1) ← helpers.base_2b_loop0_loop0 x b inn bits total let bits2 ← bits1 - b let i ← total1 >>> bits2 let i1 ← 32#u32 - b let i2 ← core.num.U32.MAX >>> i1 - let item ← lift (i &&& i2) - ok (cont (iter1, fun im => let im1 := next_back im (some item) - back im1, inn1, bits2, total1)) + let i3 ← lift (i &&& i2) + let s ← Slice.update baseb out i3 + ok (cont (iter1, s, inn1, bits2, total1)) /-- [fips205::helpers::base_2b]: loop 0: - Source: 'src/helpers.rs', lines 80:4-104:5 -/ + Source: 'src/helpers.rs', lines 87:4-111:5 -/ @[rust_loop] def helpers.base_2b_loop0 - (iter : core.slice.iter.IterMut Std.U32) - (back : core.slice.iter.IterMut Std.U32 → core.slice.iter.IterMut Std.U32) - (x : Slice Std.U8) (b : Std.U32) (inn : Std.Usize) (bits : Std.U32) - (total : Std.U32) : - Result (core.slice.iter.IterMut Std.U32) + (iter : core.ops.range.Range Std.Usize) (x : Slice Std.U8) (b : Std.U32) + (baseb : Slice Std.U32) (inn : Std.Usize) (bits : Std.U32) (total : Std.U32) + : + Result (Slice Std.U32) := do loop - (fun (iter1, back1, inn1, bits1, total1) => helpers.base_2b_loop0.body x b - iter1 back1 inn1 bits1 total1) - (iter, back, inn, bits, total) + (fun (iter1, baseb1, inn1, bits1, total1) => helpers.base_2b_loop0.body x b + iter1 baseb1 inn1 bits1 total1) + (iter, baseb, inn, bits, total) /-- [fips205::helpers::base_2b]: - Source: 'src/helpers.rs', lines 65:0-107:1 -/ + Source: 'src/helpers.rs', lines 68:0-114:1 -/ def helpers.base_2b (x : Slice Std.U8) (b : Std.U32) (out_len : Std.U32) (baseb : Slice Std.U32) : @@ -250,40 +245,39 @@ def helpers.base_2b let left_val ← lift (UScalar.cast .Usize out_len) let right_val := Slice.len baseb massert (left_val = right_val) - let (iter, iter_mut_back) ← core.slice.Slice.iter_mut baseb - let back ← - helpers.base_2b_loop0 iter (fun im => im) x b 0#usize 0#u32 0#u32 - ok (iter_mut_back back) + let i5 ← lift (UScalar.cast .Usize out_len) + helpers.base_2b_loop0 { start := 0#usize, «end» := i5 } x b baseb 0#usize + 0#u32 0#u32 /-- [fips205::helpers::{fips205::types::Adrs}::set_layer_address]: - Source: 'src/helpers.rs', lines 200:4-200:86 -/ + Source: 'src/helpers.rs', lines 207:4-207:86 -/ def helpers.Adrs.set_layer_address (self : types.Adrs) (la : Std.U32) : Result types.Adrs := do let a ← lift (core.num.U32.to_be_bytes la) ok { self with f0 := a } /-- [fips205::helpers::{fips205::types::Adrs}::get_key_pair_address]: - Source: 'src/helpers.rs', lines 202:4-202:84 -/ + Source: 'src/helpers.rs', lines 209:4-209:84 -/ def helpers.Adrs.get_key_pair_address (self : types.Adrs) : Result Std.U32 := do ok (core.num.U32.from_be_bytes self.f5) /-- [fips205::helpers::{fips205::types::Adrs}::set_key_pair_address]: - Source: 'src/helpers.rs', lines 204:4-204:100 -/ + Source: 'src/helpers.rs', lines 211:4-211:100 -/ def helpers.Adrs.set_key_pair_address (self : types.Adrs) (kp_addr : Std.U32) : Result types.Adrs := do let a ← lift (core.num.U32.to_be_bytes kp_addr) ok { self with f5 := a } /-- [fips205::helpers::{fips205::types::Adrs}::set_chain_address]: - Source: 'src/helpers.rs', lines 206:4-206:85 -/ + Source: 'src/helpers.rs', lines 213:4-213:85 -/ def helpers.Adrs.set_chain_address (self : types.Adrs) (i : Std.U32) : Result types.Adrs := do let a ← lift (core.num.U32.to_be_bytes i) ok { self with f6 := a } /-- [fips205::helpers::{fips205::types::Adrs}::set_type_and_clear]: - Source: 'src/helpers.rs', lines 208:4-213:5 -/ + Source: 'src/helpers.rs', lines 215:4-220:5 -/ def helpers.Adrs.set_type_and_clear (self : types.Adrs) (type_t : Std.U32) : Result types.Adrs := do let a ← lift (core.num.U32.to_be_bytes type_t) @@ -293,7 +287,7 @@ def helpers.Adrs.set_type_and_clear ok { self with f4 := a, f5 := a1, f6 := a2, f7 := a3 } /-- [fips205::helpers::{fips205::types::Adrs}::set_tree_address]: - Source: 'src/helpers.rs', lines 215:4-219:5 -/ + Source: 'src/helpers.rs', lines 222:4-226:5 -/ def helpers.Adrs.set_tree_address (self : types.Adrs) (t : Std.U64) : Result types.Adrs := do let bytes ← lift (core.num.U64.to_be_bytes t) @@ -314,28 +308,28 @@ def helpers.Adrs.set_tree_address ok { self with f2 := a, f3 := a1 } /-- [fips205::helpers::{fips205::types::Adrs}::set_hash_address]: - Source: 'src/helpers.rs', lines 221:4-221:89 -/ + Source: 'src/helpers.rs', lines 228:4-228:89 -/ def helpers.Adrs.set_hash_address (self : types.Adrs) (addr : Std.U32) : Result types.Adrs := do let a ← lift (core.num.U32.to_be_bytes addr) ok { self with f7 := a } /-- [fips205::helpers::{fips205::types::Adrs}::set_tree_height]: - Source: 'src/helpers.rs', lines 223:4-223:82 -/ + Source: 'src/helpers.rs', lines 230:4-230:82 -/ def helpers.Adrs.set_tree_height (self : types.Adrs) (z : Std.U32) : Result types.Adrs := do let a ← lift (core.num.U32.to_be_bytes z) ok { self with f6 := a } /-- [fips205::helpers::{fips205::types::Adrs}::get_tree_index]: - Source: 'src/helpers.rs', lines 225:4-225:82 -/ + Source: 'src/helpers.rs', lines 232:4-232:82 -/ def helpers.Adrs.get_tree_index (self : types.Adrs) : Result (Std.U32 × types.Adrs) := do let i ← lift (core.num.U32.from_be_bytes self.f7) ok (i, self) /-- [fips205::helpers::{fips205::types::Adrs}::set_tree_index]: - Source: 'src/helpers.rs', lines 227:4-227:81 -/ + Source: 'src/helpers.rs', lines 234:4-234:81 -/ def helpers.Adrs.set_tree_index (self : types.Adrs) (i : Std.U32) : Result types.Adrs := do let a ← lift (core.num.U32.to_be_bytes i) diff --git a/verification/gen/SlhVerify/FunsExternal.lean b/verification/gen/SlhVerify/FunsExternal.lean index 46d98a1..526d8fd 100644 --- a/verification/gen/SlhVerify/FunsExternal.lean +++ b/verification/gen/SlhVerify/FunsExternal.lean @@ -44,17 +44,9 @@ set_option maxHeartbeats 1000000 set_option maxRecDepth 2048 open fips205 -/-- [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] - Visibility: public -/ -@[rust_fun - "core::iter::adapters::take::{core::iter::traits::iterator::Iterator, @Clause0_Item>}::next"] -axiom core.iter.adapters.take.Take.Insts.CoreIterTraitsIteratorIterator.next - {I : Type} {Clause0_Item : Type} (traitsiteratorIteratorInst : - core.iter.traits.iterator.Iterator I Clause0_Item) : - core.iter.adapters.take.Take I → Result ((Option Clause0_Item) × - (core.iter.adapters.take.Take I)) +-- (the core::iter::adapters::take::Take::next axiom was here; DELETED +-- 2026-07-24 after de-plumbing round 2 removed the last Take iterator on the +-- verify path — to_int/base_2b now index-loop. dead-stub hygiene rule.) /-- [core::iter::range::{impl core::iter::range::Step for u32}::backward_checked]: Source: '/rustc/library/core/src/iter/range.rs', lines 290:16-290:74