From cfd50bbe64f75fe72a8ea26a2d51daad68ad25c8 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Thu, 23 Jul 2026 11:34:59 +0200 Subject: [PATCH] =?UTF-8?q?phase=202:=20FIRST=20CERTIFICATE=20=E2=80=94=20?= =?UTF-8?q?chain=20(Algorithm=205)=20proven,=20button=20green?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- README.md | 41 +++++--- verification/Proofs/ChainSpec.lean | 160 +++++++++++++++++++++++++++++ verification/check.sh | 94 +++++++++++++---- verification/drafts/ChainSpec.lean | 131 ----------------------- 4 files changed, 256 insertions(+), 170 deletions(-) create mode 100644 verification/Proofs/ChainSpec.lean delete mode 100644 verification/drafts/ChainSpec.lean diff --git a/README.md b/README.md index b503411..818dca6 100644 --- a/README.md +++ b/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 -established (2026-07-22): +`verification/check.sh` is **green** (exit 0): the model compiles, the +proofs compile, and the axiom audit passes. **One certificate proven so +far:** -- the Aeneas-compat patch landed in the snapshot (an additive monomorphic - SHA2-128s verify module reached through a named hash-oracle boundary); -- **charon and aeneas both exit 0** on the full verify cone — the gate-0 - fn-pointer blocker is gone; -- the extracted Lean model (`verification/gen/SlhVerify`, 62 defs, apex - `verify_mono.slh_verify_128s`) **type-checks under lean-guard** - (`verification/check.sh` Phase 1 is green); -- fidelity of the monomorphic path is pinned by a differential test in the - snapshot that agrees with the deployed verifier on valid / corrupted / - wrong-message signatures. +- **`fips205.chain_free_loop_eq`** (Algorithm 5, WOTS+ chaining): the + extracted `chain_free` loop equals the explicit s-fold hash chain, 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. Its + `#print axioms` cone is **exactly** `[propext, Classical.choice, + Quot.sound, verify_mono.oracle.f]` — the three kernel axioms plus the one + hash oracle it touches, and nothing else (no transpiler plumbing; the u32 + range machinery was discharged with real definitions). check.sh Phase 3 + 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 -verifier is correct. No operation theorem has been stated or proven. Every -claim under "What will be claimed" remains a *plan* (H5: an honest gap -outranks a hollow certificate). +Foundations behind this (2026-07-22/23): the Aeneas-compat patch (additive +monomorphic verify module through a named oracle boundary; charon + aeneas +exit 0); the u32 range-loop de-plumbing (faithful `Step` defs vs pinned +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 diff --git a/verification/Proofs/ChainSpec.lean b/verification/Proofs/ChainSpec.lean new file mode 100644 index 0000000..612b571 --- /dev/null +++ b/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 diff --git a/verification/check.sh b/verification/check.sh index f70ca60..e6f6c3c 100755 --- a/verification/check.sh +++ b/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 -# lean-guard. Green here means the monomorphic SHA2-128s verify cone -# translated and TYPE-CHECKS — it does NOT yet mean anything is proven. There -# are zero certificates; the proof layers come next. This script grows a -# Phase-2 (proofs) and Phase-3 (axiom audit) section as the pyramid rises, -# exactly like the ed25519 check.sh. +# Phase 1 — compile the extracted Lean model (gen/SlhVerify). +# Phase 2 — compile the proof files (Proofs/). +# Phase 3 — axiom audit: every certificate's #print axioms cone must be a +# subset of {propext, Classical.choice, Quot.sound} plus the five +# SHA-2 hash oracles (the documented boundary) — nothing else. set -euo pipefail HERE="$(cd "$(dirname "$0")" && pwd)" source ~/aeneas-toolchain/env.sh AENEAS_LEAN="$AENEAS_HOME/backends/lean" -TIMEOUT="${LEAN_TIMEOUT:-300}" -CORES="${LEAN_MAX_CORES:-4}" +TIMEOUT="${LEAN_TIMEOUT:-400}" +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 "============================================================" -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 +echo "fips205-slhdsa-verified — check" +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\" - compile() { - echo \" · \$1\" - 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 + cd '$HERE' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD/gen:\$PWD\" + compile() { echo \" · \$1\"; LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=$MEM '$HERE/lean-guard' \"\${1}.lean\" >/dev/null || { echo \"FAIL: \$1\"; exit 1; }; } + for m in ${GEN_MODULES[*]}; do compile \"gen/\$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[*]}" diff --git a/verification/drafts/ChainSpec.lean b/verification/drafts/ChainSpec.lean deleted file mode 100644 index 5494c1e..0000000 --- a/verification/drafts/ChainSpec.lean +++ /dev/null @@ -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