From a2d8e5f4d50a08aeb444cbc92b9b9b4c1d0d2c91 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Thu, 23 Jul 2026 09:38:54 +0200 Subject: [PATCH] =?UTF-8?q?phase=202=20WIP:=20chain=20proof=20=E2=80=94=20?= =?UTF-8?q?both=20increment=20lemmas=20PROVEN,=20one=20plumbing=20sorry?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Real progress on the first certificate (chain / Algorithm 5). Two mathematically-substantive lemmas now PROVEN and axiom-clean ([propext, Classical.choice, Quot.sound]): - u32_succ: the successful u32 index increment (start+1 = ok w, no overflow from the theorem's bound) — via UScalar.add_equiv case split. - fwd_succ: the range iterator's forward_checked start 1 = ok (some w), bridging checked_add/Option.ofResult/ofNatCore to the plain add. - match_ok_bind: the loop.eq_1 outer match = Result bind (rfl). chain_free_loop_eq BASE CASE proven (empty range). Two sorries remain, both PURE LEAN PLUMBING, no math left: - chain_step (one loop step = one fold step): reduction fully mechanised except exposing the let-pair so rw[match_ok_bind] can see the bind; next tactic documented in-file (full simp to reduce the let-pair, then match_ok_bind + bind_assoc; fallback = the WP loop.spec_decr_nat/spec_mono dalek pattern). - the succ case, which is chain_step + ih once chain_step lands. Still in drafts/ (sorries ⇒ never Proofs/ or check.sh); zero certificates claimed. Probes ran under lean-guard per S1. Co-Authored-By: Claude Fable 5 --- verification/drafts/ChainSpec.lean | 118 ++++++++++++++++++++--------- 1 file changed, 83 insertions(+), 35 deletions(-) diff --git a/verification/drafts/ChainSpec.lean b/verification/drafts/ChainSpec.lean index 9d627fa..631a1b6 100644 --- a/verification/drafts/ChainSpec.lean +++ b/verification/drafts/ChainSpec.lean @@ -2,35 +2,72 @@ Goal: the extracted `chain_free` loop equals the explicit s-fold application of the (opaque) hash F, with hash-address set to - i, i+1, …, i+s−1 in turn. Proving this rules out off-by-one loop - bounds, a wrong address field, and wrong threading — the exact bug - class the SLH-DSA verify path is exposed to. F stays opaque - (verify_mono.oracle.f), so the certificate cone is the three kernel - axioms + oracle.f only. + i, i+1, …, i+s−1 in turn — ruling out off-by-one loop bounds, a wrong + address field, and wrong threading. F stays opaque (oracle.f), so a + finished certificate cone here is the three kernel axioms + oracle.f. + + STATUS (2026-07-23): the two mathematically-substantive increment + lemmas are PROVEN and axiom-clean: + · u32_succ — the successful u32 index increment (start+1 = ok w). + · fwd_succ — the range iterator's `forward_checked start 1` = some w. + The one open front is `chain_step` (one loop step = one fold step): the + reduction is fully mechanised EXCEPT the final let-pair exposure. After + `simp only [… fwd_succ hwok]` the loop-body scrutinee is + `let (o,iter1) := (some start, {start:=w,end:=stop}); match o with …` + which neither `simp only` nor `dsimp` iota/zeta-reduces, so + `rw [match_ok_bind]` cannot see the underlying `bind` yet. NEXT TACTIC: + force the let-pair with full `simp` (it did reduce it in probing), + producing `match (do binds; ok (cont y)) with …`, THEN + `rw [match_ok_bind]; simp only [bind_assoc, bind_ok, hwok]; rfl`. The + fallback is the WP formulation (`loop.spec_decr_nat` + `spec_mono`, the + dalek loop-spec pattern), which sidesteps the raw match/bind plumbing. + Nothing here is claimed proven: this file carries sorries and lives in + drafts/, never in Proofs/ or check.sh. -/ import SlhVerify.Funs open Aeneas Aeneas.Std Result ControlFlow open fips205 -set_option maxHeartbeats 2000000 +set_option maxHeartbeats 4000000 namespace fips205 -/-- The mathematical chaining fold, threading the address exactly as the - extracted body does: at each step set the hash address to the current - index, hash, advance the index (monadically, matching the u32 range - iterator's `forward_checked`). Recursion on the step count. +/-- The successful u32 increment as a clean equation (no overflow). PROVEN. -/ +theorem u32_succ {start : Std.U32} (hb : start.val + 1 < 2 ^ 32) : + ∃ w : Std.U32, start + 1#u32 = ok w ∧ w.val = start.val + 1 := by + have he := Std.UScalar.add_equiv start (1#u32) + cases hc : start + 1#u32 with + | ok w => + refine ⟨w, rfl, ?_⟩ + rw [hc] at he + have : (1#u32 : Std.U32).val = 1 := by rfl + omega + | fail e => + exfalso; rw [hc] at he; simp [Std.UScalar.inBounds] at he + have : (1#u32 : Std.U32).val = 1 := by rfl + omega + | div => rw [hc] at he; simp at he - EFFECT-ORDER NOTE (audited 2026-07-23): the extracted loop increments the - index FIRST (inside `IteratorRange.next`, via `forward_checked`, failing - with `.panic` on overflow BEFORE any oracle call), while this fold hashes - first and increments AFTER (failing with the add's overflow error). The - two therefore agree only where neither increment can fail — which is - exactly what the theorem's precondition `start.val + s < 2^32` provides - (it makes every intermediate index < 2^32, so `forward_checked` always - yields `some` and `start + 1#u32` always succeeds). The step-case proof - must discharge BOTH monadic increments from that bound; do not weaken the - precondition. -/ +/-- The range iterator's forward step, when start+1 succeeds. PROVEN. -/ +theorem fwd_succ {start w : Std.U32} (hw : start + 1#u32 = ok w) : + U32.Insts.CoreIterRangeStep.forward_checked start 1#usize = ok (some w) := by + unfold U32.Insts.CoreIterRangeStep.forward_checked + have h1 : (1#usize : Std.Usize).val < 2 ^ 32 := by decide + simp only [h1, dif_pos] + have hone : Std.U32.ofNatCore (1#usize : Std.Usize).val h1 = (1#u32 : Std.U32) := by + apply Std.UScalar.eq_of_val_eq; rfl + rw [hone] + unfold Std.U32.checked_add core.num.checked_add_UScalar Option.ofResult + rw [hw] + +/-- The outer match of `loop.eq_1` IS the Result bind (definitional). PROVEN. -/ +theorem match_ok_bind {α β : Type} (m : Result α) (f : α → Result β) : + (match m with | ok r => f r | fail e => fail e | div => div) = m >>= f := rfl + +/-- The mathematical chaining fold, threading the address exactly as the + extracted body does. See the EFFECT-ORDER NOTE: agreement holds precisely + under `start.val + s < 2^32`, which makes every intermediate increment + succeed. -/ 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) | _, tmp, _, 0 => ok tmp @@ -41,7 +78,28 @@ noncomputable def chainFoldN {N : Std.Usize} (pk_seed : Slice Std.U8) : let start1 ← start + 1#u32 chainFoldN pk_seed adrs1 tmp1 start1 k -/-- The loop over the range [start, start+s) equals the s-step fold. -/ +/-- One full loop step on a non-empty range = one fold step, tail as the + continuation loop. OPEN (see file header — let-pair exposure). -/ +theorem chain_step {N : Std.Usize} (pk_seed : Slice Std.U8) (start stop : Std.U32) + (adrs : types.Adrs) (tmp : Array Std.U8 N) + (hlt : start.val < stop.val) (hb : start.val + 1 < 2 ^ 32) : + verify_mono.chain_free_loop { start := start, «end» := stop } pk_seed adrs tmp + = (do + let adrs1 ← helpers.Adrs.set_hash_address adrs start + let s ← lift (Array.to_slice tmp) + let tmp1 ← verify_mono.oracle.f N pk_seed adrs1 s + let start1 ← start + 1#u32 + verify_mono.chain_free_loop { start := start1, «end» := stop } pk_seed adrs1 tmp1) := by + obtain ⟨w, hwok, _⟩ := u32_succ hb + have hd : decide (start.val < stop.val) = true := by simp [hlt] + conv_lhs => rw [verify_mono.chain_free_loop, loop.eq_1] + unfold verify_mono.chain_free_loop.body core.iter.range.IteratorRange.next + simp only [core.cmp.impls.PartialOrdU32.lt, hd, if_true, bind_tc_ok, bind_ok, + core.clone.impls.CloneU32.clone, fwd_succ hwok] + sorry + +/-- The loop over [start, start+s) equals the s-step fold. Base case PROVEN; + succ case reduces to `chain_step` + the IH once `chain_step` closes. -/ theorem chain_free_loop_eq {N : Std.Usize} (pk_seed : Slice Std.U8) (s : Nat) : ∀ (start : Std.U32) (adrs : types.Adrs) (tmp : Array Std.U8 N), start.val + s < 2 ^ 32 → @@ -51,9 +109,7 @@ theorem chain_free_loop_eq {N : Std.Usize} (pk_seed : Slice Std.U8) (s : Nat) : induction s with | zero => intro start adrs tmp _ stop hstop - -- empty range: start.val = stop.val, so start = stop and lt is false - have hse : start = stop := by - apply Std.UScalar.eq_of_val_eq; omega + have hse : start = stop := by apply Std.UScalar.eq_of_val_eq; omega subst hse unfold verify_mono.chain_free_loop chainFoldN rw [loop.eq_1] @@ -61,18 +117,10 @@ theorem chain_free_loop_eq {N : Std.Usize} (pk_seed : Slice Std.U8) (s : Nat) : simp [core.cmp.impls.PartialOrdU32.lt] | succ k ih => intro start adrs tmp hb stop hstop - -- non-empty: lt start stop is true, so the iterator yields `some start` - -- and steps to start+1; one loop step then aligns with one fold step and - -- the IH closes the tail. have hlt : start.val < stop.val := by omega - unfold verify_mono.chain_free_loop chainFoldN - rw [loop.eq_1] - unfold verify_mono.chain_free_loop.body core.iter.range.IteratorRange.next - -- OPEN FRONT (the crux): align the loop's monadic `forward_checked start 1` - -- (a `Result U32`) with the fold's `start1 ← start + 1#u32`, then fold the - -- continuation `loop body (…)` back into `chain_free_loop` and apply `ih` - -- at start+1 / stop / k. Needs the U32 add-spec (no overflow from `hb`) and - -- ControlFlow bind-normalisation. Tractable (dalek loop-spec pattern), WIP. + have hb1 : start.val + 1 < 2 ^ 32 := by omega + rw [chain_step pk_seed start stop adrs tmp hlt hb1] + -- push the fold's step through, then apply ih at (w, stop, k) sorry end fips205