mirror of
https://github.com/saymrwulf/fips205-slhdsa-verified.git
synced 2026-09-03 19:53:49 +00:00
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>
This commit is contained in:
parent
2267e04d10
commit
e3f68b2473
4 changed files with 433 additions and 6 deletions
23
README.md
23
README.md
|
|
@ -5,11 +5,11 @@ 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: FOUR CERTIFICATES PROVEN — chain (5), WOTS+ loop (8), XMSS path (10), hypertree (12)
|
||||
## STATUS: FIVE LAYERS PROVEN — chain (5), WOTS+ loop (8), XMSS (10), hypertree (12), FORS (17)
|
||||
|
||||
`verification/check.sh` is **green** (exit 0): the model compiles, the
|
||||
proofs compile, and the axiom audit passes. **Four certificates proven so
|
||||
far, bottom-up:**
|
||||
proofs compile, and the axiom audit passes. **Six theorems across five
|
||||
verify-path layers, proven bottom-up:**
|
||||
|
||||
- **`fips205.chain_free_loop_eq`** (Algorithm 5, WOTS+ chaining): the
|
||||
extracted `chain_free` loop equals the explicit s-fold hash chain, with
|
||||
|
|
@ -66,9 +66,20 @@ obsoleted transpiler axioms deleted from the external files); fidelity
|
|||
pinned by a differential test in the snapshot (valid / corrupted /
|
||||
wrong-message), re-run green after every source patch.
|
||||
|
||||
The remaining layers (FORS, the input-prep/digest-split composition,
|
||||
apex) are not yet proven — the pyramid rises one certificate at a time,
|
||||
each audited to the same boundary.
|
||||
- **`fips205.fors_inner_loop_eq`** + **`fips205.fors_outer_loop_eq`**
|
||||
(Algorithm 17, FORS pk-from-sig): a nested loop, split into two theorems.
|
||||
The inner one pins the auth-path Merkle fold for a single FORS tree (bit
|
||||
source `indices[i] >> j`, `H` in the even/odd sibling order) — cone
|
||||
kernel-3 + `oracle.h`. The outer one pins the K-tree fold: for each tree
|
||||
compute the leaf with `F` at index `(i<<a)+indices[i]`, run the inner
|
||||
Merkle loop, write `root[i]` — cone kernel-3 + `oracle.{f, h}`. Split into
|
||||
two files under the memory discipline; the outer step lemma closes by
|
||||
peeling its 16-bind body with `bind_congr` (a bare `rfl` there whnf-times-
|
||||
out over the nested inner `loop`).
|
||||
|
||||
The remaining layers (the input-prep/digest-split composition and the apex)
|
||||
are not yet proven — the pyramid rises one certificate at a time, each
|
||||
audited to the same boundary.
|
||||
|
||||
## Subject
|
||||
|
||||
|
|
|
|||
218
verification/Proofs/ForsInnerSpec.lean
Normal file
218
verification/Proofs/ForsInnerSpec.lean
Normal file
|
|
@ -0,0 +1,218 @@
|
|||
/- 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
|
||||
193
verification/Proofs/ForsOuterSpec.lean
Normal file
193
verification/Proofs/ForsOuterSpec.lean
Normal file
|
|
@ -0,0 +1,193 @@
|
|||
/- Proofs/ForsOuterSpec.lean — FORS outer per-tree loop (Algorithm 17).
|
||||
|
||||
THEOREM fors_outer_loop_eq: the extracted outer 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, and write the result to root[i].
|
||||
Straight-line body (like HtSpec) that consumes the inner loop
|
||||
(fors_pk_from_sig_free_loop0_loop0) as an opaque sub-call — its own
|
||||
fidelity is fors_inner_loop_eq in ForsInnerSpec. Cone: kernel three +
|
||||
verify_mono.oracle.{f, h} (F for each leaf; H reached transitively through
|
||||
the referenced inner loop).
|
||||
|
||||
Split from the inner loop (ForsInnerSpec) 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
|
||||
|
||||
/-- Outer loop body on a non-empty range, resolved to the successor w. -/
|
||||
theorem hbody_fo {A K N : Std.Usize} (sig_fors : types.ForsSig A K N) (pk_seed : Slice Std.U8)
|
||||
(a32 : Std.U32) (indices : Array Std.U32 K) (start stop w : Std.U32)
|
||||
(adrs : types.Adrs) (root : Array (Array Std.U8 N) K)
|
||||
(hd : decide (start.val < stop.val) = true) (hwok : start + 1#u32 = ok w) :
|
||||
verify_mono.fors_pk_from_sig_free_loop0.body sig_fors pk_seed a32 indices
|
||||
{ start := start, «end» := stop } adrs root
|
||||
= (do
|
||||
let i1 ← lift (UScalar.cast .Usize start)
|
||||
let sk ← Array.index_usize sig_fors.private_key_value i1
|
||||
let adrs1 ← helpers.Adrs.set_tree_height adrs 0#u32
|
||||
let i2 ← start <<< a32
|
||||
let i3 ← lift (UScalar.cast .Usize start)
|
||||
let i4 ← Array.index_usize indices i3
|
||||
let i5 ← i2 + i4
|
||||
let adrs2 ← helpers.Adrs.set_tree_index adrs1 i5
|
||||
let s ← lift (Array.to_slice sk)
|
||||
let node_0 ← verify_mono.oracle.f N pk_seed adrs2 s
|
||||
let i6 ← lift (UScalar.cast .Usize start)
|
||||
let a ← Array.index_usize sig_fors.auth i6
|
||||
let auth ← types.Auth.Insts.CoreCloneClone.clone a
|
||||
let (adrs3, node_01) ←
|
||||
verify_mono.fors_pk_from_sig_free_loop0_loop0
|
||||
{ start := 0#u32, «end» := a32 } pk_seed adrs2 indices start node_0 auth
|
||||
let i7 ← lift (UScalar.cast .Usize start)
|
||||
let a1 ← Array.update root i7 node_01
|
||||
ok (cont (({ start := w, «end» := stop } : core.ops.range.Range Std.U32), adrs3, a1))) := by
|
||||
unfold verify_mono.fors_pk_from_sig_free_loop0.body
|
||||
rw [hnext hd hwok]
|
||||
simp
|
||||
|
||||
/-- The outer per-tree fold: at tree i, F-leaf then the inner Merkle loop,
|
||||
writing root[i]. The inner loop is consumed as an opaque sub-call. -/
|
||||
noncomputable def forsOuterFold {A K N : Std.Usize} (sig_fors : types.ForsSig A K N)
|
||||
(pk_seed : Slice Std.U8) (a32 : Std.U32) (indices : Array Std.U32 K) :
|
||||
types.Adrs → Array (Array Std.U8 N) K → Std.U32 → Nat →
|
||||
Result (types.Adrs × Array (Array Std.U8 N) K)
|
||||
| adrs, root, _, 0 => ok (adrs, root)
|
||||
| adrs, root, i, (s+1) => do
|
||||
let i1 ← lift (UScalar.cast .Usize i)
|
||||
let sk ← Array.index_usize sig_fors.private_key_value i1
|
||||
let adrs1 ← helpers.Adrs.set_tree_height adrs 0#u32
|
||||
let i2 ← i <<< a32
|
||||
let i3 ← lift (UScalar.cast .Usize i)
|
||||
let i4 ← Array.index_usize indices i3
|
||||
let i5 ← i2 + i4
|
||||
let adrs2 ← helpers.Adrs.set_tree_index adrs1 i5
|
||||
let s0 ← lift (Array.to_slice sk)
|
||||
let node_0 ← verify_mono.oracle.f N pk_seed adrs2 s0
|
||||
let i6 ← lift (UScalar.cast .Usize i)
|
||||
let a ← Array.index_usize sig_fors.auth i6
|
||||
let auth ← types.Auth.Insts.CoreCloneClone.clone a
|
||||
let (adrs3, node_01) ←
|
||||
verify_mono.fors_pk_from_sig_free_loop0_loop0
|
||||
{ start := 0#u32, «end» := a32 } pk_seed adrs2 indices i node_0 auth
|
||||
let i7 ← lift (UScalar.cast .Usize i)
|
||||
let a1 ← Array.update root i7 node_01
|
||||
let w ← i + 1#u32
|
||||
forsOuterFold sig_fors pk_seed a32 indices adrs3 a1 w s
|
||||
|
||||
/-- One outer loop step = one fold step (straight-line body). -/
|
||||
theorem fors_outer_step {A K N : Std.Usize} (sig_fors : types.ForsSig A K N) (pk_seed : Slice Std.U8)
|
||||
(a32 : Std.U32) (indices : Array Std.U32 K) (start stop : Std.U32)
|
||||
(adrs : types.Adrs) (root : Array (Array Std.U8 N) K)
|
||||
(hlt : start.val < stop.val) (hb : start.val + 1 < 2 ^ 32) :
|
||||
verify_mono.fors_pk_from_sig_free_loop0 { start := start, «end» := stop }
|
||||
sig_fors pk_seed a32 adrs indices root
|
||||
= (do
|
||||
let i1 ← lift (UScalar.cast .Usize start)
|
||||
let sk ← Array.index_usize sig_fors.private_key_value i1
|
||||
let adrs1 ← helpers.Adrs.set_tree_height adrs 0#u32
|
||||
let i2 ← start <<< a32
|
||||
let i3 ← lift (UScalar.cast .Usize start)
|
||||
let i4 ← Array.index_usize indices i3
|
||||
let i5 ← i2 + i4
|
||||
let adrs2 ← helpers.Adrs.set_tree_index adrs1 i5
|
||||
let s ← lift (Array.to_slice sk)
|
||||
let node_0 ← verify_mono.oracle.f N pk_seed adrs2 s
|
||||
let i6 ← lift (UScalar.cast .Usize start)
|
||||
let a ← Array.index_usize sig_fors.auth i6
|
||||
let auth ← types.Auth.Insts.CoreCloneClone.clone a
|
||||
let (adrs3, node_01) ←
|
||||
verify_mono.fors_pk_from_sig_free_loop0_loop0
|
||||
{ start := 0#u32, «end» := a32 } pk_seed adrs2 indices start node_0 auth
|
||||
let i7 ← lift (UScalar.cast .Usize start)
|
||||
let a1 ← Array.update root i7 node_01
|
||||
let w ← start + 1#u32
|
||||
verify_mono.fors_pk_from_sig_free_loop0 { start := w, «end» := stop }
|
||||
sig_fors pk_seed a32 adrs3 indices a1) := 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, loop_unfold_bind]
|
||||
dsimp only
|
||||
rw [hbody_fo sig_fors pk_seed a32 indices start stop w adrs root 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]
|
||||
-- Peel all 16 binds with bind_congr so the closing `rfl` only whnf's the
|
||||
-- small loop-tail, not the whole body threading the inner `loop` term
|
||||
-- (a bare `rfl` here blows the 4M-heartbeat whnf budget — the HtSpec body had
|
||||
-- no nested loop, so its rfl was cheap; the FORS outer body does).
|
||||
apply bind_congr; intro i1
|
||||
apply bind_congr; intro sk
|
||||
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
|
||||
apply bind_congr; intro adrs2
|
||||
apply bind_congr; intro s0
|
||||
apply bind_congr; intro node_0
|
||||
apply bind_congr; intro i6
|
||||
apply bind_congr; intro a
|
||||
apply bind_congr; intro auth
|
||||
apply bind_congr; rintro ⟨adrs3, node_01⟩
|
||||
-- the pair `let` blocks further bind_congr (won't iota via simp only); the
|
||||
-- remaining tail (i7, a1, loop recursion) is small, so a full simp closes it
|
||||
-- cheaply — no whnf over the body, so no heartbeat blowup
|
||||
simp [bind_assoc, bind_ok, verify_mono.fors_pk_from_sig_free_loop0]
|
||||
|
||||
/-- **Algorithm 17 outer fidelity.** The extracted per-tree loop over
|
||||
[start, start+s) equals the explicit K-tree fold. -/
|
||||
theorem fors_outer_loop_eq {A K N : Std.Usize} (sig_fors : types.ForsSig A K N)
|
||||
(pk_seed : Slice Std.U8) (a32 : Std.U32) (indices : Array Std.U32 K) (s : Nat) :
|
||||
∀ (start : Std.U32) (adrs : types.Adrs) (root : Array (Array Std.U8 N) K),
|
||||
start.val + s < 2 ^ 32 →
|
||||
∀ (stop : Std.U32), stop.val = start.val + s →
|
||||
verify_mono.fors_pk_from_sig_free_loop0 { start := start, «end» := stop }
|
||||
sig_fors pk_seed a32 adrs indices root
|
||||
= forsOuterFold sig_fors pk_seed a32 indices adrs root start s := by
|
||||
induction s with
|
||||
| zero =>
|
||||
intro start adrs root _ 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 forsOuterFold
|
||||
rw [loop.eq_1]
|
||||
unfold verify_mono.fors_pk_from_sig_free_loop0.body core.iter.range.IteratorRange.next
|
||||
simp [core.cmp.impls.PartialOrdU32.lt]
|
||||
| succ k ih =>
|
||||
intro start adrs root 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_outer_step sig_fors pk_seed a32 indices start stop adrs root hlt hb1]
|
||||
unfold forsOuterFold
|
||||
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 i1
|
||||
apply bind_congr; intro sk
|
||||
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
|
||||
apply bind_congr; intro adrs2
|
||||
apply bind_congr; intro s0
|
||||
apply bind_congr; intro node_0
|
||||
apply bind_congr; intro i6
|
||||
apply bind_congr; intro a
|
||||
apply bind_congr; intro auth
|
||||
apply bind_congr; rintro ⟨adrs3, node_01⟩
|
||||
apply bind_congr; intro i7
|
||||
apply bind_congr; intro a1
|
||||
exact ih w adrs3 a1 hbound stop hstop'
|
||||
|
||||
end fips205
|
||||
|
|
@ -28,6 +28,8 @@ PROOFS=(
|
|||
"WotsSpec"
|
||||
"XmssSpec"
|
||||
"HtSpec"
|
||||
"ForsInnerSpec"
|
||||
"ForsOuterSpec"
|
||||
)
|
||||
# Certificates whose axiom cones are audited, and the allowed extras beyond
|
||||
# the three kernel axioms: the five SHA-2 verify-path oracles. A certificate
|
||||
|
|
@ -37,6 +39,8 @@ CERTS=(
|
|||
"fips205.wots_loop1_eq"
|
||||
"fips205.xmss_loop_eq"
|
||||
"fips205.ht_loop_eq"
|
||||
"fips205.fors_inner_loop_eq"
|
||||
"fips205.fors_outer_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}]"
|
||||
|
|
@ -74,6 +78,7 @@ cd "$AENEAS_LEAN"
|
|||
AUD="$HERE/Proofs/.audit.lean"
|
||||
{ echo "import Proofs.ChainSpec"; echo "import Proofs.WotsSpec"
|
||||
echo "import Proofs.XmssSpec"; echo "import Proofs.HtSpec"
|
||||
echo "import Proofs.ForsInnerSpec"; echo "import Proofs.ForsOuterSpec"
|
||||
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)
|
||||
|
|
|
|||
Loading…
Reference in a new issue