phase 2 WIP: chain proof — both increment lemmas PROVEN, one plumbing sorry

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 <noreply@anthropic.com>

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