From ce2d38832c4b97b14ca541518d24b6e6a3cf3a97 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Thu, 23 Jul 2026 09:01:06 +0200 Subject: [PATCH] post-flip drill over phase-2 window: all claims held; one doc upgrade MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Re-verified from primary sources: - THE DEEP CHECK: the three discharged u32 Step defs vs the PINNED rustc's own library/core/src/iter/range.rs (nightly-2026-06-01, u32 = narrower arm on 64-bit): forward/backward = try_from-then- checked_{add,sub} (try_from succeeds iff n < 2^32), steps_between = (0, None) iff start > end else saturated diff twice. Branch-for- branch identical to the defs in FunsExternal.lean. - commit scopes: bde63f5 = exactly the 3 axiom->def swaps; d6e4d93 = only the new draft file. - fresh audits: the u32 Step INSTANCE and each of the three defs are axiom-clean ([propext(, Classical.choice, Quot.sound)]); check.sh green fresh; draft compiles with exactly ONE sorry (line 65, succ branch); base case genuinely closed. - the 'dalek u32 Step axioms are vestigial' claim: confirmed — every IteratorRange.next call site in dalek's gen uses StepUsize. - remote heads match local everywhere. Drill catch (documentation, not error): the loop increments the index BEFORE each oracle call (forward_checked inside next, .panic on overflow), the fold AFTER (add's overflow error) — equal only under the theorem's start.val + s < 2^32 precondition, which is exactly why that precondition exists. Now documented on chainFoldN so the step-case prover discharges both increments from the bound and nobody weakens it. Co-Authored-By: Claude Fable 5 --- verification/drafts/ChainSpec.lean | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/verification/drafts/ChainSpec.lean b/verification/drafts/ChainSpec.lean index 8b2bd0b..9d627fa 100644 --- a/verification/drafts/ChainSpec.lean +++ b/verification/drafts/ChainSpec.lean @@ -19,7 +19,18 @@ 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. -/ + iterator's `forward_checked`). Recursion on the step count. + + 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. -/ 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