diff --git a/README.md b/README.md index 95a8a44..e35ee96 100644 --- a/README.md +++ b/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<> 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 diff --git a/verification/Proofs/ForsOuterSpec.lean b/verification/Proofs/ForsOuterSpec.lean new file mode 100644 index 0000000..d52cdcd --- /dev/null +++ b/verification/Proofs/ForsOuterSpec.lean @@ -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 diff --git a/verification/check.sh b/verification/check.sh index 7d3abe7..e408cff 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -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)