saymrwulf/fips205-slhdsa-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/fips205-slhdsa-verified.git synced 2026-09-03 19:53:49 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
fips205-slhdsa-verified/verification/Proofs/ForsInnerSpec.lean
mrwulf e3f68b2473 phase 2: FIFTH CERTIFICATE — FORS pk-from-sig (Algorithm 17), inner + outer loops 
Two theorems, split into two files (METHOD-4 discipline — each proof a clean
unit). NB: an early single-file/bare-rfl attempt appeared to "OOM at the clamp",
but that memory pressure was a SYMPTOM of the runaway whnf diagnosed below, not
a real memory need — the fixed proofs compile in seconds at the default caps.

fips205.fors_inner_loop_eq (Proofs/ForsInnerSpec.lean): the extracted inner
Merkle auth-path loop for ONE FORS tree (fors_pk_from_sig_free_loop0_loop0)
equals the explicit auth-path fold — at level j set tree height j+1, test bit j
of THIS tree's leaf index indices[i], hash the current node with auth.tree[j] in
the bit order (even: node||auth[j]; odd: auth[j]||node), halving the tree index.
Structurally the XMSS auth-path loop, but the bit source is indices[i]>>j and the
loop returns the (adrs,node) pair. Cone: kernel-3 + verify_mono.oracle.h.

fips205.fors_outer_loop_eq (Proofs/ForsOuterSpec.lean): the extracted outer
per-tree loop (fors_pk_from_sig_free_loop0) equals the explicit K-tree fold — for
each tree i, compute the leaf with F at tree index (i<<a)+indices[i], run the
inner Merkle loop over the A levels, write the result to root[i]. Consumes the
inner loop as an opaque sub-call. Cone: kernel-3 + verify_mono.oracle.{f,h}
(F per leaf; H transitively through the inner loop).

Fidelity review at authorship (three-way, both loops): extracted bodies (gen
Funs.lean 893-933 inner, 954-985 outer) == Rust verify_mono.rs
fors_pk_from_sig_free (verbatim from upstream fors.rs, hash calls -> oracle) ==
FIPS 205 Algorithm 17, incl. the even/odd sibling order and the (i<<a)+indices[i]
leaf index.

Proof: the branched-Merkle recipe (XMSS) for the inner loop (by_cases on the
index bit, pair-bind matcher made concrete via bind_congr+rintro then full simp);
the HT straight-line recipe for the outer loop, adapted (bind_congr-peeled step
lemma + bind_congr x16 induction, both threading the inner-loop sub-call opaquely). loop_unfold_bind / u32_succ
/ fwd_succ / hnext reused verbatim from ChainSpec.

check.sh: PROOFS += ForsInnerSpec, ForsOuterSpec; CERTS += the two fors certs;
audit imports both; check.sh settings unchanged (400s/4096MB). ForsOuterSpec
compiles in 4.4s / 2.4GB after the fix below. check.sh green over ALL SIX
certificates with the axiom audit. README status -> FIVE certificates.

DIAGNOSIS NOTE (honesty): ForsOuterSpec's fors_outer_step first closed with a
bare `rfl`, which whnf'd the whole 16-bind body INCLUDING the inner-loop `loop`
term and hit a DETERMINISTIC 4M-heartbeat timeout (never actually passed — an
earlier "green" reading was a misread wrapper exit code; the real error was
hidden by check.sh piping per-file output to /dev/null). Fix: peel the 16 binds
with bind_congr so the closing rfl only sees the small loop-tail, and close the
post-pair-rintro tail with a full simp (the pair `let` won't iota via simp only).
This is the HtSpec straight-line recipe adapted for a body that nests a loop.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-23 23:57:27 +02:00

218 lines
9.8 KiB
Text
Raw Permalink Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

/- Proofs/ForsInnerSpec.lean — FORS inner Merkle authentication-path loop
(Algorithm 17, one FORS tree).
THEOREM fors_inner_loop_eq: the extracted inner loop
(fors_pk_from_sig_free_loop0_loop0) equals the explicit auth-path fold for
one FORS tree — at level j set the tree height to j+1, test bit j of the
tree's leaf index indices[i], and hash the current node with auth.tree[j]
in the bit-dictated order (even: node ∥ auth[j]; odd: auth[j] ∥ node),
halving the tree index. Structurally the XMSS auth-path loop (XmssSpec),
but the bit source is indices[i] >> j and the loop returns the (adrs, node)
pair. Cone: kernel three + verify_mono.oracle.h.
Split from the outer per-tree loop (ForsOuterSpec) so each file stays under
the memory ceiling (METHOD-4 file split). Reuses u32_succ / fwd_succ /
hnext / loop_unfold_bind from ChainSpec.
-/
import Proofs.ChainSpec
open Aeneas Aeneas.Std Result ControlFlow
open fips205
set_option maxHeartbeats 4000000
namespace fips205
/-- Inner loop body on a non-empty range, resolved to the successor w. -/
theorem hbody_fi {A K N : Std.Usize} (pk_seed : Slice Std.U8) (indices : Array Std.U32 K)
(i : Std.U32) (auth : types.Auth A N) (start stop w : Std.U32)
(adrs : types.Adrs) (node : Array Std.U8 N)
(hd : decide (start.val < stop.val) = true) (hwok : start + 1#u32 = ok w) :
verify_mono.fors_pk_from_sig_free_loop0_loop0.body pk_seed indices i auth
{ start := start, «end» := stop } adrs node
= (do
let adrs1 ← helpers.Adrs.set_tree_height adrs w
let i2 ← lift (UScalar.cast .Usize i)
let i3 ← Array.index_usize indices i2
let i4 ← i3 >>> start
let i5 ← lift (i4 &&& 1#u32)
if i5 = 0#u32
then
let (i6, adrs2) ← helpers.Adrs.get_tree_index adrs1
let tmp ← i6 / 2#u32
let adrs3 ← helpers.Adrs.set_tree_index adrs2 tmp
let s0 ← lift (Array.to_slice node)
let i7 ← lift (UScalar.cast .Usize start)
let a ← Array.index_usize auth.tree i7
let s1 ← lift (Array.to_slice a)
let node1 ← verify_mono.oracle.h N pk_seed adrs3 s0 s1
ok (cont (({ start := w, «end» := stop } : core.ops.range.Range Std.U32), adrs3, node1))
else
let (i6, adrs2) ← helpers.Adrs.get_tree_index adrs1
let i7 ← i6 - 1#u32
let tmp ← i7 / 2#u32
let adrs3 ← helpers.Adrs.set_tree_index adrs2 tmp
let i8 ← lift (UScalar.cast .Usize start)
let a ← Array.index_usize auth.tree i8
let s0 ← lift (Array.to_slice a)
let s1 ← lift (Array.to_slice node)
let node1 ← verify_mono.oracle.h N pk_seed adrs3 s0 s1
ok (cont (({ start := w, «end» := stop } : core.ops.range.Range Std.U32), adrs3, node1))) := by
unfold verify_mono.fors_pk_from_sig_free_loop0_loop0.body
rw [hnext hd hwok]
simp [hwok]
/-- The inner Merkle-path fold for one FORS tree. -/
noncomputable def forsInnerFold {A K N : Std.Usize} (pk_seed : Slice Std.U8)
(indices : Array Std.U32 K) (i : Std.U32) (auth : types.Auth A N) :
types.Adrs → Array Std.U8 N → Std.U32 → Nat → Result (types.Adrs × Array Std.U8 N)
| adrs, node, _, 0 => ok (adrs, node)
| adrs, node, lvl, (s+1) => do
let w ← lvl + 1#u32
let adrs1 ← helpers.Adrs.set_tree_height adrs w
let i2 ← lift (UScalar.cast .Usize i)
let i3 ← Array.index_usize indices i2
let i4 ← i3 >>> lvl
let i5 ← lift (i4 &&& 1#u32)
if i5 = 0#u32
then
let (i6, adrs2) ← helpers.Adrs.get_tree_index adrs1
let tmp ← i6 / 2#u32
let adrs3 ← helpers.Adrs.set_tree_index adrs2 tmp
let s0 ← lift (Array.to_slice node)
let i7 ← lift (UScalar.cast .Usize lvl)
let a ← Array.index_usize auth.tree i7
let s1 ← lift (Array.to_slice a)
let node1 ← verify_mono.oracle.h N pk_seed adrs3 s0 s1
forsInnerFold pk_seed indices i auth adrs3 node1 w s
else
let (i6, adrs2) ← helpers.Adrs.get_tree_index adrs1
let i7 ← i6 - 1#u32
let tmp ← i7 / 2#u32
let adrs3 ← helpers.Adrs.set_tree_index adrs2 tmp
let i8 ← lift (UScalar.cast .Usize lvl)
let a ← Array.index_usize auth.tree i8
let s0 ← lift (Array.to_slice a)
let s1 ← lift (Array.to_slice node)
let node1 ← verify_mono.oracle.h N pk_seed adrs3 s0 s1
forsInnerFold pk_seed indices i auth adrs3 node1 w s
/-- One inner loop step = one fold step (both branches). -/
theorem fors_inner_step {A K N : Std.Usize} (pk_seed : Slice Std.U8) (indices : Array Std.U32 K)
(i : Std.U32) (auth : types.Auth A N) (start stop : Std.U32)
(adrs : types.Adrs) (node : Array Std.U8 N)
(hlt : start.val < stop.val) (hb : start.val + 1 < 2 ^ 32) :
verify_mono.fors_pk_from_sig_free_loop0_loop0 { start := start, «end» := stop }
pk_seed adrs indices i node auth
= (do
let w ← start + 1#u32
let adrs1 ← helpers.Adrs.set_tree_height adrs w
let i2 ← lift (UScalar.cast .Usize i)
let i3 ← Array.index_usize indices i2
let i4 ← i3 >>> start
let i5 ← lift (i4 &&& 1#u32)
if i5 = 0#u32
then
let (i6, adrs2) ← helpers.Adrs.get_tree_index adrs1
let tmp ← i6 / 2#u32
let adrs3 ← helpers.Adrs.set_tree_index adrs2 tmp
let s0 ← lift (Array.to_slice node)
let i7 ← lift (UScalar.cast .Usize start)
let a ← Array.index_usize auth.tree i7
let s1 ← lift (Array.to_slice a)
let node1 ← verify_mono.oracle.h N pk_seed adrs3 s0 s1
verify_mono.fors_pk_from_sig_free_loop0_loop0 { start := w, «end» := stop }
pk_seed adrs3 indices i node1 auth
else
let (i6, adrs2) ← helpers.Adrs.get_tree_index adrs1
let i7 ← i6 - 1#u32
let tmp ← i7 / 2#u32
let adrs3 ← helpers.Adrs.set_tree_index adrs2 tmp
let i8 ← lift (UScalar.cast .Usize start)
let a ← Array.index_usize auth.tree i8
let s0 ← lift (Array.to_slice a)
let s1 ← lift (Array.to_slice node)
let node1 ← verify_mono.oracle.h N pk_seed adrs3 s0 s1
verify_mono.fors_pk_from_sig_free_loop0_loop0 { start := w, «end» := stop }
pk_seed adrs3 indices i node1 auth) := by
obtain ⟨w, hwok, _⟩ := u32_succ hb
have hd : decide (start.val < stop.val) = true := by simp [hlt]
conv_lhs => rw [verify_mono.fors_pk_from_sig_free_loop0_loop0, loop_unfold_bind]
dsimp only
rw [hbody_fi pk_seed indices i auth start stop w adrs node 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]
apply bind_congr; intro adrs1
apply bind_congr; intro i2
apply bind_congr; intro i3
apply bind_congr; intro i4
apply bind_congr; intro i5
by_cases hc : i5 = 0#u32
· rw [if_pos hc, if_pos hc]
simp only [bind_assoc, bind_ok]
apply bind_congr; rintro ⟨i6, adrs2⟩
simp [bind_assoc, bind_ok, verify_mono.fors_pk_from_sig_free_loop0_loop0]
· rw [if_neg hc, if_neg hc]
simp only [bind_assoc, bind_ok]
apply bind_congr; rintro ⟨i6, adrs2⟩
simp [bind_assoc, bind_ok, verify_mono.fors_pk_from_sig_free_loop0_loop0]
/-- **Algorithm 17 inner fidelity.** The extracted inner Merkle loop over
[start, start+s) equals the explicit auth-path fold for one FORS tree. -/
theorem fors_inner_loop_eq {A K N : Std.Usize} (pk_seed : Slice Std.U8) (indices : Array Std.U32 K)
(i : Std.U32) (auth : types.Auth A N) (s : Nat) :
∀ (start : Std.U32) (adrs : types.Adrs) (node : Array Std.U8 N),
start.val + s < 2 ^ 32 →
∀ (stop : Std.U32), stop.val = start.val + s →
verify_mono.fors_pk_from_sig_free_loop0_loop0 { start := start, «end» := stop }
pk_seed adrs indices i node auth
= forsInnerFold pk_seed indices i auth adrs node start s := by
induction s with
| zero =>
intro start adrs node _ stop hstop
have hse : start = stop := by apply Std.UScalar.eq_of_val_eq; omega
subst hse
unfold verify_mono.fors_pk_from_sig_free_loop0_loop0 forsInnerFold
rw [loop.eq_1]
unfold verify_mono.fors_pk_from_sig_free_loop0_loop0.body core.iter.range.IteratorRange.next
simp [core.cmp.impls.PartialOrdU32.lt]
| succ k ih =>
intro start adrs node 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 [fors_inner_step pk_seed indices i auth start stop adrs node hlt hb1]
unfold forsInnerFold
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 i2
apply bind_congr; intro i3
apply bind_congr; intro i4
apply bind_congr; intro i5
by_cases hc : i5 = 0#u32
· rw [if_pos hc, if_pos hc]
apply bind_congr; rintro ⟨i6, adrs2⟩
apply bind_congr; intro tmp
apply bind_congr; intro adrs3
apply bind_congr; intro s0
apply bind_congr; intro i7
apply bind_congr; intro a
apply bind_congr; intro s1
apply bind_congr; intro node1
exact ih w adrs3 node1 hbound stop hstop'
· rw [if_neg hc, if_neg hc]
apply bind_congr; rintro ⟨i6, adrs2⟩
apply bind_congr; intro i7
apply bind_congr; intro tmp
apply bind_congr; intro adrs3
apply bind_congr; intro i8
apply bind_congr; intro a
apply bind_congr; intro s0
apply bind_congr; intro s1
apply bind_congr; intro node1
exact ih w adrs3 node1 hbound stop hstop'
end fips205
Reference in a new issue View git blame Copy permalink