phase 2: FIRST CERTIFICATE — chain (Algorithm 5) proven, button green

verification/check.sh is green (exit 0): 3 phases — model compiles,
proofs compile, axiom audit passes.

fips205.chain_free_loop_eq (Proofs/ChainSpec.lean): the extracted
chain_free loop = the explicit s-fold hash chain, hash address i..i+s-1.
Machine-checked, for the deployed monomorphic SHA2-128s verify path, that
there is no off-by-one loop bound, no wrong address field, no wrong
threading. #print axioms cone = EXACTLY [propext, Classical.choice,
Quot.sound, verify_mono.oracle.f] — kernel three + the one hash oracle,
zero transpiler plumbing (the u32 Step machinery was discharged earlier
with real defs). check.sh Phase 3 enforces cone subset of kernel-3 + the
five SHA-2 oracles, failing the build otherwise.

Proof structure (all lemmas axiom-clean, no sorry): u32_succ + fwd_succ
(the monadic u32 increment, checked against pinned rustc semantics);
loop_unfold_bind (one turn of the Aeneas loop fixpoint, closed by cases
because a hand-written match compiles to a non-defeq matcher);
hnext + hbody (iterator step and loop body as clean equations);
chain_step (one loop step = one fold step); chain_free_loop_eq
(induction, IH threaded under the opaque binds with bind_congr).

Both prior sorries closed. Certificate lives in Proofs/ (not drafts/);
the WIP draft is retired. check.sh committed as -F stdin per the
no-backticks-in-commit-messages rule.

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

README.md

@@ -5,26 +5,33 @@ path**, extracted from a pure-Rust implementation into Lean 4 via
 Charon/Aeneas — the same pipeline, discipline, and honesty rules as the
 four ed25519 campaigns (`dalek/anza/risc0/betrusted-ed25519-verified`).
 
-## STATUS: MODEL EXTRACTED & TYPE-CHECKS — NOTHING PROVEN YET
+## STATUS: FIRST CERTIFICATE PROVEN — Algorithm 5 (chain)
 
-There are still **zero certificates** in this repository. What phase 1
+`verification/check.sh` is **green** (exit 0): the model compiles, the
-established (2026-07-22):
+proofs compile, and the axiom audit passes. **One certificate proven so
+far:**
 
-- the Aeneas-compat patch landed in the snapshot (an additive monomorphic
+- **`fips205.chain_free_loop_eq`** (Algorithm 5, WOTS+ chaining): the
-  SHA2-128s verify module reached through a named hash-oracle boundary);
+  extracted `chain_free` loop equals the explicit s-fold hash chain, with
-- **charon and aeneas both exit 0** on the full verify cone — the gate-0
+  the hash address set to i, i+1, …, i+s−1 in turn. This rules out —
-  fn-pointer blocker is gone;
+  machine-checked, for the deployed monomorphic SHA2-128s verify path — an
-- the extracted Lean model (`verification/gen/SlhVerify`, 62 defs, apex
+  off-by-one loop bound, a wrong address field, and wrong threading. Its
-  `verify_mono.slh_verify_128s`) **type-checks under lean-guard**
+  `#print axioms` cone is **exactly** `[propext, Classical.choice,
-  (`verification/check.sh` Phase 1 is green);
+  Quot.sound, verify_mono.oracle.f]` — the three kernel axioms plus the one
-- fidelity of the monomorphic path is pinned by a differential test in the
+  hash oracle it touches, and nothing else (no transpiler plumbing; the u32
-  snapshot that agrees with the deployed verifier on valid / corrupted /
+  range machinery was discharged with real definitions). check.sh Phase 3
-  wrong-message signatures.
+  fails the build if any certificate cone contains anything outside the
+  kernel three + the five documented SHA-2 oracles.
 
-A green Phase-1 compile proves the model is **well-formed**, NOT that the
+Foundations behind this (2026-07-22/23): the Aeneas-compat patch (additive
-verifier is correct. No operation theorem has been stated or proven. Every
+monomorphic verify module through a named oracle boundary; charon + aeneas
-claim under "What will be claimed" remains a *plan* (H5: an honest gap
+exit 0); the u32 range-loop de-plumbing (faithful `Step` defs vs pinned
-outranks a hollow certificate).
+rustc, axiom-clean); fidelity pinned by a differential test in the snapshot
+(valid / corrupted / wrong-message).
+
+The remaining layers (WOTS+ pk, XMSS path, hypertree, FORS, apex) are not
+yet proven — the pyramid rises one certificate at a time, each audited to
+the same boundary.
 
 ## Subject
 

verification/Proofs/ChainSpec.lean

@@ -0,0 +1,160 @@
+/- Proofs/ChainSpec.lean — Algorithm 5 (chain / WOTS+ chaining) fidelity.
+
+   THEOREM chain_free_loop_eq: the extracted `chain_free` loop equals the
+   explicit s-fold application of the hash F, with the hash-address set to
+   i, i+1, …, i+s−1 in turn. This rules out — machine-checked, for the
+   deployed monomorphic SHA2-128s verify path — an off-by-one loop bound, a
+   wrong address field, and wrong threading. F stays opaque
+   (verify_mono.oracle.f), so the certificate cone is the three kernel axioms
+   + oracle.f, and nothing else (audited by check.sh Phase 3).
+
+   The proof: an induction on the step count. `chain_step` is one loop step =
+   one fold step, proven by unfolding the Aeneas `loop` fixpoint one turn
+   (loop_unfold_bind), reducing the range iterator to a clean equation
+   (fips205_hnext) and the loop body to a clean do-block (fips205_hbody), and
+   aligning the monadic u32 index increment (u32_succ / fwd_succ) with the
+   fold's. The succ case threads the IH under the opaque binds with
+   bind_congr.
+-/
+import SlhVerify.Funs
+open Aeneas Aeneas.Std Result ControlFlow
+open fips205
+
+set_option maxHeartbeats 4000000
+
+namespace fips205
+
+/-- The successful u32 increment as a clean equation (no overflow). -/
+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
+
+/-- The range iterator's forward step, when start+1 succeeds. -/
+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 Aeneas `loop` fixpoint, unfolded one turn into a bind. The `casesOn`
+    continuation matches loop's own reduction, so it closes by cases+rfl
+    (a hand-written `match` would compile to a different, non-defeq matcher). -/
+theorem loop_unfold_bind {α β : Type} (body : α → Result (ControlFlow α β)) (x : α) :
+    loop body x = body x >>= (fun r => ControlFlow.casesOn r (fun c => loop body c) (fun d => ok d)) := by
+  conv_lhs => rw [loop.eq_1]
+  cases body x with
+  | ok cf => cases cf <;> rfl
+  | fail e => rfl
+  | div => rfl
+
+/-- The range iterator step on a non-empty range, as a clean equation. -/
+theorem hnext {start stop w : Std.U32}
+    (hd : decide (start.val < stop.val) = true) (hwok : start + 1#u32 = ok w) :
+    core.iter.range.IteratorRange.next U32.Insts.CoreIterRangeStep
+        { start := start, «end» := stop }
+      = ok (some start, { start := w, «end» := stop }) := by
+  unfold core.iter.range.IteratorRange.next
+  simp only [core.cmp.impls.PartialOrdU32.lt, hd, decide_true, if_true,
+    bind_tc_ok, bind_ok, core.clone.impls.CloneU32.clone, fwd_succ hwok]
+
+/-- The loop body on a non-empty range reduces to a clean do-block. -/
+theorem hbody {N : Std.Usize} (pk_seed : Slice Std.U8) (start stop w : Std.U32)
+    (adrs : types.Adrs) (tmp : Array Std.U8 N)
+    (hd : decide (start.val < stop.val) = true) (hwok : start + 1#u32 = ok w) :
+    verify_mono.chain_free_loop.body pk_seed { start := start, «end» := stop } 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
+          ok (cont (({ start := w, «end» := stop } : core.ops.range.Range Std.U32), adrs1, tmp1))) := by
+  unfold verify_mono.chain_free_loop.body
+  rw [hnext hd hwok]
+  simp
+
+/-- The mathematical chaining fold: at each step set the hash address to the
+    current index, hash, advance the index (monadically, matching the u32
+    range iterator). Recursion on the step count. Agreement with the extracted
+    loop holds under `start.val + s < 2^32`, which makes every 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
+  | 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
+
+/-- One full loop step on a non-empty range = one fold step, tail as the
+    continuation loop. -/
+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_unfold_bind]
+  dsimp only
+  rw [hbody pk_seed start stop w adrs tmp 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 5 fidelity.** The extracted chain loop over [start, start+s)
+    equals the explicit s-fold hash-chain. -/
+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
+    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
+    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 [chain_step pk_seed start stop adrs tmp hlt hb1]
+    unfold chainFoldN
+    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 adrs1
+    apply bind_congr; intro s
+    apply bind_congr; intro tmp1
+    exact ih w adrs1 tmp1 hbound stop hstop'
+
+end fips205

verification/check.sh

@@ -1,44 +1,94 @@
 #!/usr/bin/env bash
 # The one-button claim for this repository (rigor invariant R3).
+# Green output == the full claim. This script is the ONLY source of the
+# word "proven" for this repo.
 #
-# PHASE 1 (current): compiles the extracted Lean model (gen/SlhVerify) under
+#   Phase 1 — compile the extracted Lean model (gen/SlhVerify).
-# lean-guard. Green here means the monomorphic SHA2-128s verify cone
+#   Phase 2 — compile the proof files (Proofs/).
-# translated and TYPE-CHECKS — it does NOT yet mean anything is proven. There
+#   Phase 3 — axiom audit: every certificate's #print axioms cone must be a
-# are zero certificates; the proof layers come next. This script grows a
+#             subset of {propext, Classical.choice, Quot.sound} plus the five
-# Phase-2 (proofs) and Phase-3 (axiom audit) section as the pyramid rises,
+#             SHA-2 hash oracles (the documented boundary) — nothing else.
-# exactly like the ed25519 check.sh.
 set -euo pipefail
 
 HERE="$(cd "$(dirname "$0")" && pwd)"
 source ~/aeneas-toolchain/env.sh
 AENEAS_LEAN="$AENEAS_HOME/backends/lean"
-TIMEOUT="${LEAN_TIMEOUT:-300}"
+TIMEOUT="${LEAN_TIMEOUT:-400}"
-CORES="${LEAN_MAX_CORES:-4}"
+MEM="${LEAN_MEM_MB:-4096}"
 
-# Import order (each depends on the previous).
 GEN_MODULES=(
   "SlhVerify/TypesExternal"
   "SlhVerify/Types"
   "SlhVerify/FunsExternal"
   "SlhVerify/Funs"
 )
+# Proof files, in dependency order.
+PROOFS=(
+  "ChainSpec"
+)
+# Certificates whose axiom cones are audited, and the allowed extras beyond
+# the three kernel axioms: the five SHA-2 verify-path oracles. A certificate
+# is listed here only once it is genuinely proven.
+CERTS=(
+  "fips205.chain_free_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}]"
 
-echo "fips205-slhdsa-verified — check (PHASE 1: model compile only)"
+echo "fips205-slhdsa-verified — check"
-echo "============================================================"
+echo "==============================="
-echo "NOTE: 0 certificates. A green compile proves the extracted model is"
-echo "well-formed; it does NOT prove the verifier correct. See README.md."
-echo
 
-LOG=$(mktemp /tmp/fips205-check-XXXX.log)
+# ── Phase 1: model ──────────────────────────────────────────────────────────
+echo "=== Phase 1: compile the extracted model ==="
 cd "$AENEAS_LEAN"
 lake env bash -c "
   set -euo pipefail
-  cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
+  cd '$HERE' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD/gen:\$PWD\"
-  compile() {
+  compile() { echo \"  · \$1\"; LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=$MEM '$HERE/lean-guard' \"\${1}.lean\" >/dev/null || { echo \"FAIL: \$1\"; exit 1; }; }
-    echo \"  · \$1\"
+  for m in ${GEN_MODULES[*]}; do compile \"gen/\$m\"; done
-    LEAN_TIMEOUT=$TIMEOUT LEAN_MAX_CORES=$CORES '$HERE/lean-guard' \"\${1}.lean\" 2>&1 | tee -a '$LOG' || { echo \"FAIL: \$1\"; exit 1; }
-  }
-  for m in ${GEN_MODULES[*]}; do compile \"\$m\"; done
 "
+
+# ── Phase 2: proofs ─────────────────────────────────────────────────────────
+echo "=== Phase 2: compile the proofs ==="
+cd "$AENEAS_LEAN"
+lake env bash -c "
+  set -euo pipefail
+  cd '$HERE' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD/gen:\$PWD\"
+  compile() { echo \"  · \$1\"; LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=$MEM '$HERE/lean-guard' \"Proofs/\${1}.lean\" >/dev/null || { echo \"FAIL: Proofs/\$1\"; exit 1; }; }
+  for m in ${PROOFS[*]}; do compile \"\$m\"; done
+  # no dead proof files: everything under Proofs/ must be in the manifest
+  for f in Proofs/*.lean; do b=\$(basename \"\$f\" .lean)
+    case \" ${PROOFS[*]} \" in *\" \$b \"*) ;; *) echo \"DEAD FILE: Proofs/\$b.lean not in manifest\"; exit 1 ;; esac
+  done
+"
+
+# ── Phase 3: axiom audit ────────────────────────────────────────────────────
+echo "=== Phase 3: axiom audit (cone ⊆ kernel-3 + 5 oracles) ==="
+cd "$AENEAS_LEAN"
+AUD="$HERE/Proofs/.audit.lean"
+{ echo "import Proofs.ChainSpec"
+  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)
+rm -f "$AUD"
+fail=0
+for c in "${CERTS[@]}"; do
+  line=$(echo "$OUT" | grep -F "'$c' depends on axioms:" || true)
+  if [ -z "$line" ]; then echo "  ✗ $c — no axiom report"; fail=1; continue; fi
+  cone=$(echo "$line" | sed "s/.*depends on axioms: //")
+  # every axiom in the cone must be in ALLOWED
+  bad=$(echo "$cone" | tr -d '[]' | tr ',' '\n' | sed 's/^ *//;s/ *$//' | while read -r ax; do
+    [ -z "$ax" ] && continue
+    case " propext Classical.choice Quot.sound verify_mono.oracle.f verify_mono.oracle.h verify_mono.oracle.t_l verify_mono.oracle.t_len verify_mono.oracle.h_msg " in
+      *" $ax "*) ;; *) echo "$ax" ;;
+    esac
+  done)
+  if [ -n "$bad" ]; then echo "  ✗ $c — DISALLOWED axioms: $bad"; fail=1
+  else echo "  ✓ $c  cone ⊆ allowed"; fi
+done
+[ "$fail" = 0 ] || { echo "AXIOM AUDIT FAILED"; exit 1; }
+
 echo
-echo "PHASE 1 GREEN: gen/SlhVerify model type-checks. Proofs are the next layer."
+echo "ALL GREEN — model compiles, proofs compile, every certificate cone is"
+echo "the three kernel axioms plus (at most) the SHA-2 hash oracles."
+echo "Certificates proven: ${CERTS[*]}"

verification/drafts/ChainSpec.lean

@@ -1,131 +0,0 @@
-/- 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 — 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.
-
-   RECORD NOTE: commit a2d8e5f's message body lost one backticked fragment
-   to shell command-substitution (it reads "the let-pair  so"); the intended
-   text was: the let-pair (o,iter1) := (some start, {start:=w,end:=stop}).
-   This header is the authoritative technical record.
--/
-import SlhVerify.Funs
-open Aeneas Aeneas.Std Result ControlFlow
-open fips205
-
-set_option maxHeartbeats 4000000
-
-namespace fips205
-
-/-- 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
-
-/-- 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
-  | 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
-
-/-- 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 →
-      ∀ (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
-    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
-    have hlt : start.val < stop.val := by omega
-    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