phase 2 WIP: chain (Alg 5) spec — fold defined, base case proven

drafts/ChainSpec.lean (NOT in Proofs/, NOT in check.sh — carries a
sorry, so nothing is claimed proven; H1/H2 hold):

- chainFoldN: the mathematical s-fold of the opaque hash F, threading
  the hash-address (i, i+1, …, i+s-1) and index exactly as the extracted
  loop body does. Equational spec (chain_free_loop = chainFoldN) — chosen
  over a WP triple so it needs no assumption that the opaque oracle.f
  succeeds (both sides fail together if it does).
- chain_free_loop_eq: induction on the step count via loop.eq_1.
  BASE CASE PROVEN (empty range start..start reduces to ok tmp,
  PartialOrdU32.lt start start = false). Step case is the one open
  front: align the loop's monadic forward_checked with the fold's
  start+1 (u32 add-spec from the no-overflow bound) and fold the loop
  continuation back for the IH — the dalek loop-spec pattern, tractable.

De-plumbing (prior commit bde63f5) means this cone will carry only the
kernel three + oracle.f once closed. First real certificate incoming.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

verification/drafts/ChainSpec.lean

@@ -0,0 +1,67 @@
+/- drafts/ChainSpec.lean — WIP: Algorithm 5 (chain) fidelity.
+
+   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.
+-/
+import SlhVerify.Funs
+open Aeneas Aeneas.Std Result ControlFlow
+open fips205
+
+set_option maxHeartbeats 2000000
+
+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. -/
+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
+  | adrs, tmp, start, (k+1) => 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
+      chainFoldN pk_seed adrs1 tmp1 start1 k
+
+/-- The loop over the range [start, start+s) equals the s-step fold. -/
+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 →
+      ∀ (stop : Std.U32), stop.val = start.val + s →
+      verify_mono.chain_free_loop { start := start, «end» := stop } pk_seed adrs tmp
+        = chainFoldN pk_seed adrs tmp start s := by
+  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
+    subst hse
+    unfold verify_mono.chain_free_loop chainFoldN
+    rw [loop.eq_1]
+    unfold verify_mono.chain_free_loop.body core.iter.range.IteratorRange.next
+    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.
+    sorry
+
+end fips205