From 195eafcc160f074c8a0644365c67cc651acb5574 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Sat, 4 Jul 2026 15:30:18 +0200 Subject: [PATCH] NAF campaign stages 1-2: LE load walks + the digit loop's arithmetic core MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - `Proofs/DsmNafLoadSpec.lean` (generated) — the byte-to-word LE load of `non_adjacent_form`: four 8-peel inner walks (t |= bytes[8k+bi] << 8bi) and the outer 4-peel filling x_u64[0..3]; x_u64[4] stays 0 (the pad word the cross-word window reads at positions >= 251). - `Proofs/DsmNafMath.lean` — the pure arithmetic of the w=5 digit loop: `nafSum`/`nafSum_set`; window-read lemmas `naf_window_single` / `naf_window_cross` (cross-word disjoint-OR read sees (V >> pos) mod 32); invariant steps `naf_even_step` / `naf_odd_step` (Nat.mod_mul telescope: digit + promoted carry reconstruct the consumed bits EXACTLY, in ZZ); carry-kill `naf_carry_even` / `naf_carry_odd` (V < 2^253 forces the carry dead before bit 256); `naf_exit` (nafSum naf 256 = V exactly). The digit-loop walk (stage 3) composes these next; its invariant is nafSum naf 256 + carry*2^pos = V mod 2^pos with digits at k >= pos all zero and carry = 1 -> pos <= 254. CERTS += naf_load_spec, naf_window_cross, naf_exit (axiom-clean). Co-Authored-By: Claude Fable 5 --- verification/Proofs/DsmNafLoadSpec.lean | 1473 +++++++++++++++++++++++ verification/Proofs/DsmNafMath.lean | 239 ++++ verification/check.sh | 19 + 3 files changed, 1731 insertions(+) create mode 100644 verification/Proofs/DsmNafLoadSpec.lean create mode 100644 verification/Proofs/DsmNafMath.lean diff --git a/verification/Proofs/DsmNafLoadSpec.lean b/verification/Proofs/DsmNafLoadSpec.lean new file mode 100644 index 0000000..620b7e5 --- /dev/null +++ b/verification/Proofs/DsmNafLoadSpec.lean @@ -0,0 +1,1473 @@ +/- ────────────────────────────────────────────────────────────────────────────── + Proofs/DsmNafLoadSpec.lean — NAF campaign, stage 1: the little-endian + byte→word load of `non_adjacent_form` (scalar.rs: read_le_u64_into + refactored to the nested index loop for extraction). + + Four inner walks (one per word: t |= bytes[8k+bi] << 8bi, bi = 0..7) and + the outer 4-peel filling x_u64[0..3]; x_u64[4] stays 0 — the pad word the + digit loop's cross-word window reads at positions ≥ 251. + + GENERATED by dsm_naf_load_gen.py — proven fbw idioms: or-accumulation via + Nat.two_pow_add_eq_or_of_lt with the explicit calc bridge (default simp + literalizes 2^8; simp only keeps pow form), hypothesis-side index + evaluation, minimal-context value haves. + ────────────────────────────────────────────────────────────────────────────── -/ +import Proofs.DsmTableSpec +open Aeneas Aeneas.Std Result ControlFlow +open curve25519_dalek + +set_option maxHeartbeats 8000000 +set_option linter.unusedSimpArgs false +set_option maxRecDepth 8000 + +namespace CurveFieldProofs + +open Aeneas.Std.WP + +/-- Inner LE-load loop for word 0: t accumulates bytes 0..7 + little-endian. The scalar struct passes through unchanged. -/ +theorem naf_word_loop_spec_0 (self : scalar.Scalar) + (b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31 : Std.U8) + (hb : (↑self.bytes : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31]) : + scalar.Scalar.non_adjacent_form_loop0_loop0 self 0#usize 0#u64 0#usize + ⦃ p => p.1 = self ∧ p.2.val = b0.val + b1.val * 2^8 + b2.val * 2^16 + b3.val * 2^24 + b4.val * 2^32 + b5.val * 2^40 + b6.val * 2^48 + b7.val * 2^56 ⦄ := by + have hsz64 : (U64.size : ℕ) = 2^64 := by scalar_tac + have hbb0 : b0.val < 2^8 := by scalar_tac + have hbb1 : b1.val < 2^8 := by scalar_tac + have hbb2 : b2.val < 2^8 := by scalar_tac + have hbb3 : b3.val < 2^8 := by scalar_tac + have hbb4 : b4.val < 2^8 := by scalar_tac + have hbb5 : b5.val < 2^8 := by scalar_tac + have hbb6 : b6.val < 2^8 := by scalar_tac + have hbb7 : b7.val < 2^8 := by scalar_tac + unfold scalar.Scalar.non_adjacent_form_loop0_loop0 + -- bi = 0: byte 0 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (0#usize < 8#usize) by scalar_tac)] + step as ⟨i0, hi0⟩ + have hi0v : i0 = 0#usize := by clear * - hi0; scalar_tac + rw [hi0v] + step as ⟨i10, hi10⟩ + have hi10v : i10 = 0#usize := by clear * - hi10; scalar_tac + rw [hi10v] + step as ⟨x0, hx0⟩ + simp [hb] at hx0 + step with UScalar.cast.step_spec as ⟨c0, hc0⟩ + have hc0v : c0.val = b0.val := by + rw [hc0, UScalar.cast_val_eq, hx0] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s0, hsh0⟩ + have hsv0 : s0.val = 0 := by clear * - hsh0; scalar_tac + step as ⟨t0, ht0⟩ + have ht0v : t0.val = b0.val * 2^0 := by + rw [ht0] + simp [hsv0, hc0v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y0, hy0⟩ + have hy0v : y0.val = b0.val := by + simp [hy0, UScalar.val_or, ht0v] + step as ⟨bi0, hbi0⟩ + have hbi0v : bi0 = 1#usize := by clear * - hbi0; scalar_tac + rw [hbi0v] + try simp only [spec_ok] + -- bi = 1: byte 1 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (1#usize < 8#usize) by scalar_tac)] + step as ⟨i1, hi1⟩ + have hi1v : i1 = 0#usize := by clear * - hi1; scalar_tac + rw [hi1v] + step as ⟨i11, hi11⟩ + have hi11v : i11 = 1#usize := by clear * - hi11; scalar_tac + rw [hi11v] + step as ⟨x1, hx1⟩ + simp [hb] at hx1 + step with UScalar.cast.step_spec as ⟨c1, hc1⟩ + have hc1v : c1.val = b1.val := by + rw [hc1, UScalar.cast_val_eq, hx1] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s1, hsh1⟩ + have hsv1 : s1.val = 8 := by clear * - hsh1; scalar_tac + step as ⟨t1, ht1⟩ + have ht1v : t1.val = b1.val * 2^8 := by + rw [ht1] + simp [hsv1, hc1v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y1, hy1⟩ + have hy1v : y1.val = b0.val + b1.val * 2^8 := by + have hult : y0.val < 2^8 := by rw [hy0v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y0.val) (i := 8) hult b1.val + have hadd : y0.val ||| b1.val * 2^8 = y0.val + b1.val * 2^8 := by + calc y0.val ||| b1.val * 2^8 + = y0.val ||| 2^8 * b1.val := by rw [Nat.mul_comm] + _ = 2^8 * b1.val ||| y0.val := Nat.lor_comm _ _ + _ = 2^8 * b1.val + y0.val := hor.symm + _ = y0.val + b1.val * 2^8 := by ring + simp only [hy1, UScalar.val_or, ht1v] + rw [hadd, hy0v] + try ring + step as ⟨bi1, hbi1⟩ + have hbi1v : bi1 = 2#usize := by clear * - hbi1; scalar_tac + rw [hbi1v] + try simp only [spec_ok] + -- bi = 2: byte 2 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (2#usize < 8#usize) by scalar_tac)] + step as ⟨i2, hi2⟩ + have hi2v : i2 = 0#usize := by clear * - hi2; scalar_tac + rw [hi2v] + step as ⟨i12, hi12⟩ + have hi12v : i12 = 2#usize := by clear * - hi12; scalar_tac + rw [hi12v] + step as ⟨x2, hx2⟩ + simp [hb] at hx2 + step with UScalar.cast.step_spec as ⟨c2, hc2⟩ + have hc2v : c2.val = b2.val := by + rw [hc2, UScalar.cast_val_eq, hx2] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s2, hsh2⟩ + have hsv2 : s2.val = 16 := by clear * - hsh2; scalar_tac + step as ⟨t2, ht2⟩ + have ht2v : t2.val = b2.val * 2^16 := by + rw [ht2] + simp [hsv2, hc2v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y2, hy2⟩ + have hy2v : y2.val = b0.val + b1.val * 2^8 + b2.val * 2^16 := by + have hult : y1.val < 2^16 := by rw [hy1v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y1.val) (i := 16) hult b2.val + have hadd : y1.val ||| b2.val * 2^16 = y1.val + b2.val * 2^16 := by + calc y1.val ||| b2.val * 2^16 + = y1.val ||| 2^16 * b2.val := by rw [Nat.mul_comm] + _ = 2^16 * b2.val ||| y1.val := Nat.lor_comm _ _ + _ = 2^16 * b2.val + y1.val := hor.symm + _ = y1.val + b2.val * 2^16 := by ring + simp only [hy2, UScalar.val_or, ht2v] + rw [hadd, hy1v] + try ring + step as ⟨bi2, hbi2⟩ + have hbi2v : bi2 = 3#usize := by clear * - hbi2; scalar_tac + rw [hbi2v] + try simp only [spec_ok] + -- bi = 3: byte 3 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (3#usize < 8#usize) by scalar_tac)] + step as ⟨i3, hi3⟩ + have hi3v : i3 = 0#usize := by clear * - hi3; scalar_tac + rw [hi3v] + step as ⟨i13, hi13⟩ + have hi13v : i13 = 3#usize := by clear * - hi13; scalar_tac + rw [hi13v] + step as ⟨x3, hx3⟩ + simp [hb] at hx3 + step with UScalar.cast.step_spec as ⟨c3, hc3⟩ + have hc3v : c3.val = b3.val := by + rw [hc3, UScalar.cast_val_eq, hx3] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s3, hsh3⟩ + have hsv3 : s3.val = 24 := by clear * - hsh3; scalar_tac + step as ⟨t3, ht3⟩ + have ht3v : t3.val = b3.val * 2^24 := by + rw [ht3] + simp [hsv3, hc3v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y3, hy3⟩ + have hy3v : y3.val = b0.val + b1.val * 2^8 + b2.val * 2^16 + b3.val * 2^24 := by + have hult : y2.val < 2^24 := by rw [hy2v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y2.val) (i := 24) hult b3.val + have hadd : y2.val ||| b3.val * 2^24 = y2.val + b3.val * 2^24 := by + calc y2.val ||| b3.val * 2^24 + = y2.val ||| 2^24 * b3.val := by rw [Nat.mul_comm] + _ = 2^24 * b3.val ||| y2.val := Nat.lor_comm _ _ + _ = 2^24 * b3.val + y2.val := hor.symm + _ = y2.val + b3.val * 2^24 := by ring + simp only [hy3, UScalar.val_or, ht3v] + rw [hadd, hy2v] + try ring + step as ⟨bi3, hbi3⟩ + have hbi3v : bi3 = 4#usize := by clear * - hbi3; scalar_tac + rw [hbi3v] + try simp only [spec_ok] + -- bi = 4: byte 4 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (4#usize < 8#usize) by scalar_tac)] + step as ⟨i4, hi4⟩ + have hi4v : i4 = 0#usize := by clear * - hi4; scalar_tac + rw [hi4v] + step as ⟨i14, hi14⟩ + have hi14v : i14 = 4#usize := by clear * - hi14; scalar_tac + rw [hi14v] + step as ⟨x4, hx4⟩ + simp [hb] at hx4 + step with UScalar.cast.step_spec as ⟨c4, hc4⟩ + have hc4v : c4.val = b4.val := by + rw [hc4, UScalar.cast_val_eq, hx4] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s4, hsh4⟩ + have hsv4 : s4.val = 32 := by clear * - hsh4; scalar_tac + step as ⟨t4, ht4⟩ + have ht4v : t4.val = b4.val * 2^32 := by + rw [ht4] + simp [hsv4, hc4v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y4, hy4⟩ + have hy4v : y4.val = b0.val + b1.val * 2^8 + b2.val * 2^16 + b3.val * 2^24 + b4.val * 2^32 := by + have hult : y3.val < 2^32 := by rw [hy3v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y3.val) (i := 32) hult b4.val + have hadd : y3.val ||| b4.val * 2^32 = y3.val + b4.val * 2^32 := by + calc y3.val ||| b4.val * 2^32 + = y3.val ||| 2^32 * b4.val := by rw [Nat.mul_comm] + _ = 2^32 * b4.val ||| y3.val := Nat.lor_comm _ _ + _ = 2^32 * b4.val + y3.val := hor.symm + _ = y3.val + b4.val * 2^32 := by ring + simp only [hy4, UScalar.val_or, ht4v] + rw [hadd, hy3v] + try ring + step as ⟨bi4, hbi4⟩ + have hbi4v : bi4 = 5#usize := by clear * - hbi4; scalar_tac + rw [hbi4v] + try simp only [spec_ok] + -- bi = 5: byte 5 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (5#usize < 8#usize) by scalar_tac)] + step as ⟨i5, hi5⟩ + have hi5v : i5 = 0#usize := by clear * - hi5; scalar_tac + rw [hi5v] + step as ⟨i15, hi15⟩ + have hi15v : i15 = 5#usize := by clear * - hi15; scalar_tac + rw [hi15v] + step as ⟨x5, hx5⟩ + simp [hb] at hx5 + step with UScalar.cast.step_spec as ⟨c5, hc5⟩ + have hc5v : c5.val = b5.val := by + rw [hc5, UScalar.cast_val_eq, hx5] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s5, hsh5⟩ + have hsv5 : s5.val = 40 := by clear * - hsh5; scalar_tac + step as ⟨t5, ht5⟩ + have ht5v : t5.val = b5.val * 2^40 := by + rw [ht5] + simp [hsv5, hc5v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y5, hy5⟩ + have hy5v : y5.val = b0.val + b1.val * 2^8 + b2.val * 2^16 + b3.val * 2^24 + b4.val * 2^32 + b5.val * 2^40 := by + have hult : y4.val < 2^40 := by rw [hy4v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y4.val) (i := 40) hult b5.val + have hadd : y4.val ||| b5.val * 2^40 = y4.val + b5.val * 2^40 := by + calc y4.val ||| b5.val * 2^40 + = y4.val ||| 2^40 * b5.val := by rw [Nat.mul_comm] + _ = 2^40 * b5.val ||| y4.val := Nat.lor_comm _ _ + _ = 2^40 * b5.val + y4.val := hor.symm + _ = y4.val + b5.val * 2^40 := by ring + simp only [hy5, UScalar.val_or, ht5v] + rw [hadd, hy4v] + try ring + step as ⟨bi5, hbi5⟩ + have hbi5v : bi5 = 6#usize := by clear * - hbi5; scalar_tac + rw [hbi5v] + try simp only [spec_ok] + -- bi = 6: byte 6 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (6#usize < 8#usize) by scalar_tac)] + step as ⟨i6, hi6⟩ + have hi6v : i6 = 0#usize := by clear * - hi6; scalar_tac + rw [hi6v] + step as ⟨i16, hi16⟩ + have hi16v : i16 = 6#usize := by clear * - hi16; scalar_tac + rw [hi16v] + step as ⟨x6, hx6⟩ + simp [hb] at hx6 + step with UScalar.cast.step_spec as ⟨c6, hc6⟩ + have hc6v : c6.val = b6.val := by + rw [hc6, UScalar.cast_val_eq, hx6] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s6, hsh6⟩ + have hsv6 : s6.val = 48 := by clear * - hsh6; scalar_tac + step as ⟨t6, ht6⟩ + have ht6v : t6.val = b6.val * 2^48 := by + rw [ht6] + simp [hsv6, hc6v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y6, hy6⟩ + have hy6v : y6.val = b0.val + b1.val * 2^8 + b2.val * 2^16 + b3.val * 2^24 + b4.val * 2^32 + b5.val * 2^40 + b6.val * 2^48 := by + have hult : y5.val < 2^48 := by rw [hy5v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y5.val) (i := 48) hult b6.val + have hadd : y5.val ||| b6.val * 2^48 = y5.val + b6.val * 2^48 := by + calc y5.val ||| b6.val * 2^48 + = y5.val ||| 2^48 * b6.val := by rw [Nat.mul_comm] + _ = 2^48 * b6.val ||| y5.val := Nat.lor_comm _ _ + _ = 2^48 * b6.val + y5.val := hor.symm + _ = y5.val + b6.val * 2^48 := by ring + simp only [hy6, UScalar.val_or, ht6v] + rw [hadd, hy5v] + try ring + step as ⟨bi6, hbi6⟩ + have hbi6v : bi6 = 7#usize := by clear * - hbi6; scalar_tac + rw [hbi6v] + try simp only [spec_ok] + -- bi = 7: byte 7 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (7#usize < 8#usize) by scalar_tac)] + step as ⟨i7, hi7⟩ + have hi7v : i7 = 0#usize := by clear * - hi7; scalar_tac + rw [hi7v] + step as ⟨i17, hi17⟩ + have hi17v : i17 = 7#usize := by clear * - hi17; scalar_tac + rw [hi17v] + step as ⟨x7, hx7⟩ + simp [hb] at hx7 + step with UScalar.cast.step_spec as ⟨c7, hc7⟩ + have hc7v : c7.val = b7.val := by + rw [hc7, UScalar.cast_val_eq, hx7] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s7, hsh7⟩ + have hsv7 : s7.val = 56 := by clear * - hsh7; scalar_tac + step as ⟨t7, ht7⟩ + have ht7v : t7.val = b7.val * 2^56 := by + rw [ht7] + simp [hsv7, hc7v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y7, hy7⟩ + have hy7v : y7.val = b0.val + b1.val * 2^8 + b2.val * 2^16 + b3.val * 2^24 + b4.val * 2^32 + b5.val * 2^40 + b6.val * 2^48 + b7.val * 2^56 := by + have hult : y6.val < 2^56 := by rw [hy6v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y6.val) (i := 56) hult b7.val + have hadd : y6.val ||| b7.val * 2^56 = y6.val + b7.val * 2^56 := by + calc y6.val ||| b7.val * 2^56 + = y6.val ||| 2^56 * b7.val := by rw [Nat.mul_comm] + _ = 2^56 * b7.val ||| y6.val := Nat.lor_comm _ _ + _ = 2^56 * b7.val + y6.val := hor.symm + _ = y6.val + b7.val * 2^56 := by ring + simp only [hy7, UScalar.val_or, ht7v] + rw [hadd, hy6v] + try ring + step as ⟨bi7, hbi7⟩ + have hbi7v : bi7 = 8#usize := by clear * - hbi7; scalar_tac + rw [hbi7v] + try simp only [spec_ok] + -- exit: bi = 8, done (self, t) + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_neg (show ¬ (8#usize < 8#usize) by scalar_tac)] + try simp only [spec_ok] + exact ⟨True.intro, hy7v⟩ + +/-- Inner LE-load loop for word 1: t accumulates bytes 8..15 + little-endian. The scalar struct passes through unchanged. -/ +theorem naf_word_loop_spec_1 (self : scalar.Scalar) + (b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31 : Std.U8) + (hb : (↑self.bytes : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31]) : + scalar.Scalar.non_adjacent_form_loop0_loop0 self 1#usize 0#u64 0#usize + ⦃ p => p.1 = self ∧ p.2.val = b8.val + b9.val * 2^8 + b10.val * 2^16 + b11.val * 2^24 + b12.val * 2^32 + b13.val * 2^40 + b14.val * 2^48 + b15.val * 2^56 ⦄ := by + have hsz64 : (U64.size : ℕ) = 2^64 := by scalar_tac + have hbb8 : b8.val < 2^8 := by scalar_tac + have hbb9 : b9.val < 2^8 := by scalar_tac + have hbb10 : b10.val < 2^8 := by scalar_tac + have hbb11 : b11.val < 2^8 := by scalar_tac + have hbb12 : b12.val < 2^8 := by scalar_tac + have hbb13 : b13.val < 2^8 := by scalar_tac + have hbb14 : b14.val < 2^8 := by scalar_tac + have hbb15 : b15.val < 2^8 := by scalar_tac + unfold scalar.Scalar.non_adjacent_form_loop0_loop0 + -- bi = 0: byte 8 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (0#usize < 8#usize) by scalar_tac)] + step as ⟨i0, hi0⟩ + have hi0v : i0 = 8#usize := by clear * - hi0; scalar_tac + rw [hi0v] + step as ⟨i10, hi10⟩ + have hi10v : i10 = 8#usize := by clear * - hi10; scalar_tac + rw [hi10v] + step as ⟨x0, hx0⟩ + simp [hb] at hx0 + step with UScalar.cast.step_spec as ⟨c0, hc0⟩ + have hc0v : c0.val = b8.val := by + rw [hc0, UScalar.cast_val_eq, hx0] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s0, hsh0⟩ + have hsv0 : s0.val = 0 := by clear * - hsh0; scalar_tac + step as ⟨t0, ht0⟩ + have ht0v : t0.val = b8.val * 2^0 := by + rw [ht0] + simp [hsv0, hc0v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y0, hy0⟩ + have hy0v : y0.val = b8.val := by + simp [hy0, UScalar.val_or, ht0v] + step as ⟨bi0, hbi0⟩ + have hbi0v : bi0 = 1#usize := by clear * - hbi0; scalar_tac + rw [hbi0v] + try simp only [spec_ok] + -- bi = 1: byte 9 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (1#usize < 8#usize) by scalar_tac)] + step as ⟨i1, hi1⟩ + have hi1v : i1 = 8#usize := by clear * - hi1; scalar_tac + rw [hi1v] + step as ⟨i11, hi11⟩ + have hi11v : i11 = 9#usize := by clear * - hi11; scalar_tac + rw [hi11v] + step as ⟨x1, hx1⟩ + simp [hb] at hx1 + step with UScalar.cast.step_spec as ⟨c1, hc1⟩ + have hc1v : c1.val = b9.val := by + rw [hc1, UScalar.cast_val_eq, hx1] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s1, hsh1⟩ + have hsv1 : s1.val = 8 := by clear * - hsh1; scalar_tac + step as ⟨t1, ht1⟩ + have ht1v : t1.val = b9.val * 2^8 := by + rw [ht1] + simp [hsv1, hc1v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y1, hy1⟩ + have hy1v : y1.val = b8.val + b9.val * 2^8 := by + have hult : y0.val < 2^8 := by rw [hy0v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y0.val) (i := 8) hult b9.val + have hadd : y0.val ||| b9.val * 2^8 = y0.val + b9.val * 2^8 := by + calc y0.val ||| b9.val * 2^8 + = y0.val ||| 2^8 * b9.val := by rw [Nat.mul_comm] + _ = 2^8 * b9.val ||| y0.val := Nat.lor_comm _ _ + _ = 2^8 * b9.val + y0.val := hor.symm + _ = y0.val + b9.val * 2^8 := by ring + simp only [hy1, UScalar.val_or, ht1v] + rw [hadd, hy0v] + try ring + step as ⟨bi1, hbi1⟩ + have hbi1v : bi1 = 2#usize := by clear * - hbi1; scalar_tac + rw [hbi1v] + try simp only [spec_ok] + -- bi = 2: byte 10 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (2#usize < 8#usize) by scalar_tac)] + step as ⟨i2, hi2⟩ + have hi2v : i2 = 8#usize := by clear * - hi2; scalar_tac + rw [hi2v] + step as ⟨i12, hi12⟩ + have hi12v : i12 = 10#usize := by clear * - hi12; scalar_tac + rw [hi12v] + step as ⟨x2, hx2⟩ + simp [hb] at hx2 + step with UScalar.cast.step_spec as ⟨c2, hc2⟩ + have hc2v : c2.val = b10.val := by + rw [hc2, UScalar.cast_val_eq, hx2] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s2, hsh2⟩ + have hsv2 : s2.val = 16 := by clear * - hsh2; scalar_tac + step as ⟨t2, ht2⟩ + have ht2v : t2.val = b10.val * 2^16 := by + rw [ht2] + simp [hsv2, hc2v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y2, hy2⟩ + have hy2v : y2.val = b8.val + b9.val * 2^8 + b10.val * 2^16 := by + have hult : y1.val < 2^16 := by rw [hy1v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y1.val) (i := 16) hult b10.val + have hadd : y1.val ||| b10.val * 2^16 = y1.val + b10.val * 2^16 := by + calc y1.val ||| b10.val * 2^16 + = y1.val ||| 2^16 * b10.val := by rw [Nat.mul_comm] + _ = 2^16 * b10.val ||| y1.val := Nat.lor_comm _ _ + _ = 2^16 * b10.val + y1.val := hor.symm + _ = y1.val + b10.val * 2^16 := by ring + simp only [hy2, UScalar.val_or, ht2v] + rw [hadd, hy1v] + try ring + step as ⟨bi2, hbi2⟩ + have hbi2v : bi2 = 3#usize := by clear * - hbi2; scalar_tac + rw [hbi2v] + try simp only [spec_ok] + -- bi = 3: byte 11 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (3#usize < 8#usize) by scalar_tac)] + step as ⟨i3, hi3⟩ + have hi3v : i3 = 8#usize := by clear * - hi3; scalar_tac + rw [hi3v] + step as ⟨i13, hi13⟩ + have hi13v : i13 = 11#usize := by clear * - hi13; scalar_tac + rw [hi13v] + step as ⟨x3, hx3⟩ + simp [hb] at hx3 + step with UScalar.cast.step_spec as ⟨c3, hc3⟩ + have hc3v : c3.val = b11.val := by + rw [hc3, UScalar.cast_val_eq, hx3] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s3, hsh3⟩ + have hsv3 : s3.val = 24 := by clear * - hsh3; scalar_tac + step as ⟨t3, ht3⟩ + have ht3v : t3.val = b11.val * 2^24 := by + rw [ht3] + simp [hsv3, hc3v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y3, hy3⟩ + have hy3v : y3.val = b8.val + b9.val * 2^8 + b10.val * 2^16 + b11.val * 2^24 := by + have hult : y2.val < 2^24 := by rw [hy2v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y2.val) (i := 24) hult b11.val + have hadd : y2.val ||| b11.val * 2^24 = y2.val + b11.val * 2^24 := by + calc y2.val ||| b11.val * 2^24 + = y2.val ||| 2^24 * b11.val := by rw [Nat.mul_comm] + _ = 2^24 * b11.val ||| y2.val := Nat.lor_comm _ _ + _ = 2^24 * b11.val + y2.val := hor.symm + _ = y2.val + b11.val * 2^24 := by ring + simp only [hy3, UScalar.val_or, ht3v] + rw [hadd, hy2v] + try ring + step as ⟨bi3, hbi3⟩ + have hbi3v : bi3 = 4#usize := by clear * - hbi3; scalar_tac + rw [hbi3v] + try simp only [spec_ok] + -- bi = 4: byte 12 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (4#usize < 8#usize) by scalar_tac)] + step as ⟨i4, hi4⟩ + have hi4v : i4 = 8#usize := by clear * - hi4; scalar_tac + rw [hi4v] + step as ⟨i14, hi14⟩ + have hi14v : i14 = 12#usize := by clear * - hi14; scalar_tac + rw [hi14v] + step as ⟨x4, hx4⟩ + simp [hb] at hx4 + step with UScalar.cast.step_spec as ⟨c4, hc4⟩ + have hc4v : c4.val = b12.val := by + rw [hc4, UScalar.cast_val_eq, hx4] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s4, hsh4⟩ + have hsv4 : s4.val = 32 := by clear * - hsh4; scalar_tac + step as ⟨t4, ht4⟩ + have ht4v : t4.val = b12.val * 2^32 := by + rw [ht4] + simp [hsv4, hc4v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y4, hy4⟩ + have hy4v : y4.val = b8.val + b9.val * 2^8 + b10.val * 2^16 + b11.val * 2^24 + b12.val * 2^32 := by + have hult : y3.val < 2^32 := by rw [hy3v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y3.val) (i := 32) hult b12.val + have hadd : y3.val ||| b12.val * 2^32 = y3.val + b12.val * 2^32 := by + calc y3.val ||| b12.val * 2^32 + = y3.val ||| 2^32 * b12.val := by rw [Nat.mul_comm] + _ = 2^32 * b12.val ||| y3.val := Nat.lor_comm _ _ + _ = 2^32 * b12.val + y3.val := hor.symm + _ = y3.val + b12.val * 2^32 := by ring + simp only [hy4, UScalar.val_or, ht4v] + rw [hadd, hy3v] + try ring + step as ⟨bi4, hbi4⟩ + have hbi4v : bi4 = 5#usize := by clear * - hbi4; scalar_tac + rw [hbi4v] + try simp only [spec_ok] + -- bi = 5: byte 13 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (5#usize < 8#usize) by scalar_tac)] + step as ⟨i5, hi5⟩ + have hi5v : i5 = 8#usize := by clear * - hi5; scalar_tac + rw [hi5v] + step as ⟨i15, hi15⟩ + have hi15v : i15 = 13#usize := by clear * - hi15; scalar_tac + rw [hi15v] + step as ⟨x5, hx5⟩ + simp [hb] at hx5 + step with UScalar.cast.step_spec as ⟨c5, hc5⟩ + have hc5v : c5.val = b13.val := by + rw [hc5, UScalar.cast_val_eq, hx5] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s5, hsh5⟩ + have hsv5 : s5.val = 40 := by clear * - hsh5; scalar_tac + step as ⟨t5, ht5⟩ + have ht5v : t5.val = b13.val * 2^40 := by + rw [ht5] + simp [hsv5, hc5v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y5, hy5⟩ + have hy5v : y5.val = b8.val + b9.val * 2^8 + b10.val * 2^16 + b11.val * 2^24 + b12.val * 2^32 + b13.val * 2^40 := by + have hult : y4.val < 2^40 := by rw [hy4v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y4.val) (i := 40) hult b13.val + have hadd : y4.val ||| b13.val * 2^40 = y4.val + b13.val * 2^40 := by + calc y4.val ||| b13.val * 2^40 + = y4.val ||| 2^40 * b13.val := by rw [Nat.mul_comm] + _ = 2^40 * b13.val ||| y4.val := Nat.lor_comm _ _ + _ = 2^40 * b13.val + y4.val := hor.symm + _ = y4.val + b13.val * 2^40 := by ring + simp only [hy5, UScalar.val_or, ht5v] + rw [hadd, hy4v] + try ring + step as ⟨bi5, hbi5⟩ + have hbi5v : bi5 = 6#usize := by clear * - hbi5; scalar_tac + rw [hbi5v] + try simp only [spec_ok] + -- bi = 6: byte 14 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (6#usize < 8#usize) by scalar_tac)] + step as ⟨i6, hi6⟩ + have hi6v : i6 = 8#usize := by clear * - hi6; scalar_tac + rw [hi6v] + step as ⟨i16, hi16⟩ + have hi16v : i16 = 14#usize := by clear * - hi16; scalar_tac + rw [hi16v] + step as ⟨x6, hx6⟩ + simp [hb] at hx6 + step with UScalar.cast.step_spec as ⟨c6, hc6⟩ + have hc6v : c6.val = b14.val := by + rw [hc6, UScalar.cast_val_eq, hx6] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s6, hsh6⟩ + have hsv6 : s6.val = 48 := by clear * - hsh6; scalar_tac + step as ⟨t6, ht6⟩ + have ht6v : t6.val = b14.val * 2^48 := by + rw [ht6] + simp [hsv6, hc6v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y6, hy6⟩ + have hy6v : y6.val = b8.val + b9.val * 2^8 + b10.val * 2^16 + b11.val * 2^24 + b12.val * 2^32 + b13.val * 2^40 + b14.val * 2^48 := by + have hult : y5.val < 2^48 := by rw [hy5v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y5.val) (i := 48) hult b14.val + have hadd : y5.val ||| b14.val * 2^48 = y5.val + b14.val * 2^48 := by + calc y5.val ||| b14.val * 2^48 + = y5.val ||| 2^48 * b14.val := by rw [Nat.mul_comm] + _ = 2^48 * b14.val ||| y5.val := Nat.lor_comm _ _ + _ = 2^48 * b14.val + y5.val := hor.symm + _ = y5.val + b14.val * 2^48 := by ring + simp only [hy6, UScalar.val_or, ht6v] + rw [hadd, hy5v] + try ring + step as ⟨bi6, hbi6⟩ + have hbi6v : bi6 = 7#usize := by clear * - hbi6; scalar_tac + rw [hbi6v] + try simp only [spec_ok] + -- bi = 7: byte 15 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (7#usize < 8#usize) by scalar_tac)] + step as ⟨i7, hi7⟩ + have hi7v : i7 = 8#usize := by clear * - hi7; scalar_tac + rw [hi7v] + step as ⟨i17, hi17⟩ + have hi17v : i17 = 15#usize := by clear * - hi17; scalar_tac + rw [hi17v] + step as ⟨x7, hx7⟩ + simp [hb] at hx7 + step with UScalar.cast.step_spec as ⟨c7, hc7⟩ + have hc7v : c7.val = b15.val := by + rw [hc7, UScalar.cast_val_eq, hx7] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s7, hsh7⟩ + have hsv7 : s7.val = 56 := by clear * - hsh7; scalar_tac + step as ⟨t7, ht7⟩ + have ht7v : t7.val = b15.val * 2^56 := by + rw [ht7] + simp [hsv7, hc7v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y7, hy7⟩ + have hy7v : y7.val = b8.val + b9.val * 2^8 + b10.val * 2^16 + b11.val * 2^24 + b12.val * 2^32 + b13.val * 2^40 + b14.val * 2^48 + b15.val * 2^56 := by + have hult : y6.val < 2^56 := by rw [hy6v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y6.val) (i := 56) hult b15.val + have hadd : y6.val ||| b15.val * 2^56 = y6.val + b15.val * 2^56 := by + calc y6.val ||| b15.val * 2^56 + = y6.val ||| 2^56 * b15.val := by rw [Nat.mul_comm] + _ = 2^56 * b15.val ||| y6.val := Nat.lor_comm _ _ + _ = 2^56 * b15.val + y6.val := hor.symm + _ = y6.val + b15.val * 2^56 := by ring + simp only [hy7, UScalar.val_or, ht7v] + rw [hadd, hy6v] + try ring + step as ⟨bi7, hbi7⟩ + have hbi7v : bi7 = 8#usize := by clear * - hbi7; scalar_tac + rw [hbi7v] + try simp only [spec_ok] + -- exit: bi = 8, done (self, t) + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_neg (show ¬ (8#usize < 8#usize) by scalar_tac)] + try simp only [spec_ok] + exact ⟨True.intro, hy7v⟩ + +/-- Inner LE-load loop for word 2: t accumulates bytes 16..23 + little-endian. The scalar struct passes through unchanged. -/ +theorem naf_word_loop_spec_2 (self : scalar.Scalar) + (b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31 : Std.U8) + (hb : (↑self.bytes : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31]) : + scalar.Scalar.non_adjacent_form_loop0_loop0 self 2#usize 0#u64 0#usize + ⦃ p => p.1 = self ∧ p.2.val = b16.val + b17.val * 2^8 + b18.val * 2^16 + b19.val * 2^24 + b20.val * 2^32 + b21.val * 2^40 + b22.val * 2^48 + b23.val * 2^56 ⦄ := by + have hsz64 : (U64.size : ℕ) = 2^64 := by scalar_tac + have hbb16 : b16.val < 2^8 := by scalar_tac + have hbb17 : b17.val < 2^8 := by scalar_tac + have hbb18 : b18.val < 2^8 := by scalar_tac + have hbb19 : b19.val < 2^8 := by scalar_tac + have hbb20 : b20.val < 2^8 := by scalar_tac + have hbb21 : b21.val < 2^8 := by scalar_tac + have hbb22 : b22.val < 2^8 := by scalar_tac + have hbb23 : b23.val < 2^8 := by scalar_tac + unfold scalar.Scalar.non_adjacent_form_loop0_loop0 + -- bi = 0: byte 16 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (0#usize < 8#usize) by scalar_tac)] + step as ⟨i0, hi0⟩ + have hi0v : i0 = 16#usize := by clear * - hi0; scalar_tac + rw [hi0v] + step as ⟨i10, hi10⟩ + have hi10v : i10 = 16#usize := by clear * - hi10; scalar_tac + rw [hi10v] + step as ⟨x0, hx0⟩ + simp [hb] at hx0 + step with UScalar.cast.step_spec as ⟨c0, hc0⟩ + have hc0v : c0.val = b16.val := by + rw [hc0, UScalar.cast_val_eq, hx0] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s0, hsh0⟩ + have hsv0 : s0.val = 0 := by clear * - hsh0; scalar_tac + step as ⟨t0, ht0⟩ + have ht0v : t0.val = b16.val * 2^0 := by + rw [ht0] + simp [hsv0, hc0v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y0, hy0⟩ + have hy0v : y0.val = b16.val := by + simp [hy0, UScalar.val_or, ht0v] + step as ⟨bi0, hbi0⟩ + have hbi0v : bi0 = 1#usize := by clear * - hbi0; scalar_tac + rw [hbi0v] + try simp only [spec_ok] + -- bi = 1: byte 17 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (1#usize < 8#usize) by scalar_tac)] + step as ⟨i1, hi1⟩ + have hi1v : i1 = 16#usize := by clear * - hi1; scalar_tac + rw [hi1v] + step as ⟨i11, hi11⟩ + have hi11v : i11 = 17#usize := by clear * - hi11; scalar_tac + rw [hi11v] + step as ⟨x1, hx1⟩ + simp [hb] at hx1 + step with UScalar.cast.step_spec as ⟨c1, hc1⟩ + have hc1v : c1.val = b17.val := by + rw [hc1, UScalar.cast_val_eq, hx1] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s1, hsh1⟩ + have hsv1 : s1.val = 8 := by clear * - hsh1; scalar_tac + step as ⟨t1, ht1⟩ + have ht1v : t1.val = b17.val * 2^8 := by + rw [ht1] + simp [hsv1, hc1v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y1, hy1⟩ + have hy1v : y1.val = b16.val + b17.val * 2^8 := by + have hult : y0.val < 2^8 := by rw [hy0v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y0.val) (i := 8) hult b17.val + have hadd : y0.val ||| b17.val * 2^8 = y0.val + b17.val * 2^8 := by + calc y0.val ||| b17.val * 2^8 + = y0.val ||| 2^8 * b17.val := by rw [Nat.mul_comm] + _ = 2^8 * b17.val ||| y0.val := Nat.lor_comm _ _ + _ = 2^8 * b17.val + y0.val := hor.symm + _ = y0.val + b17.val * 2^8 := by ring + simp only [hy1, UScalar.val_or, ht1v] + rw [hadd, hy0v] + try ring + step as ⟨bi1, hbi1⟩ + have hbi1v : bi1 = 2#usize := by clear * - hbi1; scalar_tac + rw [hbi1v] + try simp only [spec_ok] + -- bi = 2: byte 18 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (2#usize < 8#usize) by scalar_tac)] + step as ⟨i2, hi2⟩ + have hi2v : i2 = 16#usize := by clear * - hi2; scalar_tac + rw [hi2v] + step as ⟨i12, hi12⟩ + have hi12v : i12 = 18#usize := by clear * - hi12; scalar_tac + rw [hi12v] + step as ⟨x2, hx2⟩ + simp [hb] at hx2 + step with UScalar.cast.step_spec as ⟨c2, hc2⟩ + have hc2v : c2.val = b18.val := by + rw [hc2, UScalar.cast_val_eq, hx2] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s2, hsh2⟩ + have hsv2 : s2.val = 16 := by clear * - hsh2; scalar_tac + step as ⟨t2, ht2⟩ + have ht2v : t2.val = b18.val * 2^16 := by + rw [ht2] + simp [hsv2, hc2v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y2, hy2⟩ + have hy2v : y2.val = b16.val + b17.val * 2^8 + b18.val * 2^16 := by + have hult : y1.val < 2^16 := by rw [hy1v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y1.val) (i := 16) hult b18.val + have hadd : y1.val ||| b18.val * 2^16 = y1.val + b18.val * 2^16 := by + calc y1.val ||| b18.val * 2^16 + = y1.val ||| 2^16 * b18.val := by rw [Nat.mul_comm] + _ = 2^16 * b18.val ||| y1.val := Nat.lor_comm _ _ + _ = 2^16 * b18.val + y1.val := hor.symm + _ = y1.val + b18.val * 2^16 := by ring + simp only [hy2, UScalar.val_or, ht2v] + rw [hadd, hy1v] + try ring + step as ⟨bi2, hbi2⟩ + have hbi2v : bi2 = 3#usize := by clear * - hbi2; scalar_tac + rw [hbi2v] + try simp only [spec_ok] + -- bi = 3: byte 19 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (3#usize < 8#usize) by scalar_tac)] + step as ⟨i3, hi3⟩ + have hi3v : i3 = 16#usize := by clear * - hi3; scalar_tac + rw [hi3v] + step as ⟨i13, hi13⟩ + have hi13v : i13 = 19#usize := by clear * - hi13; scalar_tac + rw [hi13v] + step as ⟨x3, hx3⟩ + simp [hb] at hx3 + step with UScalar.cast.step_spec as ⟨c3, hc3⟩ + have hc3v : c3.val = b19.val := by + rw [hc3, UScalar.cast_val_eq, hx3] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s3, hsh3⟩ + have hsv3 : s3.val = 24 := by clear * - hsh3; scalar_tac + step as ⟨t3, ht3⟩ + have ht3v : t3.val = b19.val * 2^24 := by + rw [ht3] + simp [hsv3, hc3v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y3, hy3⟩ + have hy3v : y3.val = b16.val + b17.val * 2^8 + b18.val * 2^16 + b19.val * 2^24 := by + have hult : y2.val < 2^24 := by rw [hy2v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y2.val) (i := 24) hult b19.val + have hadd : y2.val ||| b19.val * 2^24 = y2.val + b19.val * 2^24 := by + calc y2.val ||| b19.val * 2^24 + = y2.val ||| 2^24 * b19.val := by rw [Nat.mul_comm] + _ = 2^24 * b19.val ||| y2.val := Nat.lor_comm _ _ + _ = 2^24 * b19.val + y2.val := hor.symm + _ = y2.val + b19.val * 2^24 := by ring + simp only [hy3, UScalar.val_or, ht3v] + rw [hadd, hy2v] + try ring + step as ⟨bi3, hbi3⟩ + have hbi3v : bi3 = 4#usize := by clear * - hbi3; scalar_tac + rw [hbi3v] + try simp only [spec_ok] + -- bi = 4: byte 20 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (4#usize < 8#usize) by scalar_tac)] + step as ⟨i4, hi4⟩ + have hi4v : i4 = 16#usize := by clear * - hi4; scalar_tac + rw [hi4v] + step as ⟨i14, hi14⟩ + have hi14v : i14 = 20#usize := by clear * - hi14; scalar_tac + rw [hi14v] + step as ⟨x4, hx4⟩ + simp [hb] at hx4 + step with UScalar.cast.step_spec as ⟨c4, hc4⟩ + have hc4v : c4.val = b20.val := by + rw [hc4, UScalar.cast_val_eq, hx4] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s4, hsh4⟩ + have hsv4 : s4.val = 32 := by clear * - hsh4; scalar_tac + step as ⟨t4, ht4⟩ + have ht4v : t4.val = b20.val * 2^32 := by + rw [ht4] + simp [hsv4, hc4v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y4, hy4⟩ + have hy4v : y4.val = b16.val + b17.val * 2^8 + b18.val * 2^16 + b19.val * 2^24 + b20.val * 2^32 := by + have hult : y3.val < 2^32 := by rw [hy3v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y3.val) (i := 32) hult b20.val + have hadd : y3.val ||| b20.val * 2^32 = y3.val + b20.val * 2^32 := by + calc y3.val ||| b20.val * 2^32 + = y3.val ||| 2^32 * b20.val := by rw [Nat.mul_comm] + _ = 2^32 * b20.val ||| y3.val := Nat.lor_comm _ _ + _ = 2^32 * b20.val + y3.val := hor.symm + _ = y3.val + b20.val * 2^32 := by ring + simp only [hy4, UScalar.val_or, ht4v] + rw [hadd, hy3v] + try ring + step as ⟨bi4, hbi4⟩ + have hbi4v : bi4 = 5#usize := by clear * - hbi4; scalar_tac + rw [hbi4v] + try simp only [spec_ok] + -- bi = 5: byte 21 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (5#usize < 8#usize) by scalar_tac)] + step as ⟨i5, hi5⟩ + have hi5v : i5 = 16#usize := by clear * - hi5; scalar_tac + rw [hi5v] + step as ⟨i15, hi15⟩ + have hi15v : i15 = 21#usize := by clear * - hi15; scalar_tac + rw [hi15v] + step as ⟨x5, hx5⟩ + simp [hb] at hx5 + step with UScalar.cast.step_spec as ⟨c5, hc5⟩ + have hc5v : c5.val = b21.val := by + rw [hc5, UScalar.cast_val_eq, hx5] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s5, hsh5⟩ + have hsv5 : s5.val = 40 := by clear * - hsh5; scalar_tac + step as ⟨t5, ht5⟩ + have ht5v : t5.val = b21.val * 2^40 := by + rw [ht5] + simp [hsv5, hc5v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y5, hy5⟩ + have hy5v : y5.val = b16.val + b17.val * 2^8 + b18.val * 2^16 + b19.val * 2^24 + b20.val * 2^32 + b21.val * 2^40 := by + have hult : y4.val < 2^40 := by rw [hy4v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y4.val) (i := 40) hult b21.val + have hadd : y4.val ||| b21.val * 2^40 = y4.val + b21.val * 2^40 := by + calc y4.val ||| b21.val * 2^40 + = y4.val ||| 2^40 * b21.val := by rw [Nat.mul_comm] + _ = 2^40 * b21.val ||| y4.val := Nat.lor_comm _ _ + _ = 2^40 * b21.val + y4.val := hor.symm + _ = y4.val + b21.val * 2^40 := by ring + simp only [hy5, UScalar.val_or, ht5v] + rw [hadd, hy4v] + try ring + step as ⟨bi5, hbi5⟩ + have hbi5v : bi5 = 6#usize := by clear * - hbi5; scalar_tac + rw [hbi5v] + try simp only [spec_ok] + -- bi = 6: byte 22 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (6#usize < 8#usize) by scalar_tac)] + step as ⟨i6, hi6⟩ + have hi6v : i6 = 16#usize := by clear * - hi6; scalar_tac + rw [hi6v] + step as ⟨i16, hi16⟩ + have hi16v : i16 = 22#usize := by clear * - hi16; scalar_tac + rw [hi16v] + step as ⟨x6, hx6⟩ + simp [hb] at hx6 + step with UScalar.cast.step_spec as ⟨c6, hc6⟩ + have hc6v : c6.val = b22.val := by + rw [hc6, UScalar.cast_val_eq, hx6] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s6, hsh6⟩ + have hsv6 : s6.val = 48 := by clear * - hsh6; scalar_tac + step as ⟨t6, ht6⟩ + have ht6v : t6.val = b22.val * 2^48 := by + rw [ht6] + simp [hsv6, hc6v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y6, hy6⟩ + have hy6v : y6.val = b16.val + b17.val * 2^8 + b18.val * 2^16 + b19.val * 2^24 + b20.val * 2^32 + b21.val * 2^40 + b22.val * 2^48 := by + have hult : y5.val < 2^48 := by rw [hy5v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y5.val) (i := 48) hult b22.val + have hadd : y5.val ||| b22.val * 2^48 = y5.val + b22.val * 2^48 := by + calc y5.val ||| b22.val * 2^48 + = y5.val ||| 2^48 * b22.val := by rw [Nat.mul_comm] + _ = 2^48 * b22.val ||| y5.val := Nat.lor_comm _ _ + _ = 2^48 * b22.val + y5.val := hor.symm + _ = y5.val + b22.val * 2^48 := by ring + simp only [hy6, UScalar.val_or, ht6v] + rw [hadd, hy5v] + try ring + step as ⟨bi6, hbi6⟩ + have hbi6v : bi6 = 7#usize := by clear * - hbi6; scalar_tac + rw [hbi6v] + try simp only [spec_ok] + -- bi = 7: byte 23 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (7#usize < 8#usize) by scalar_tac)] + step as ⟨i7, hi7⟩ + have hi7v : i7 = 16#usize := by clear * - hi7; scalar_tac + rw [hi7v] + step as ⟨i17, hi17⟩ + have hi17v : i17 = 23#usize := by clear * - hi17; scalar_tac + rw [hi17v] + step as ⟨x7, hx7⟩ + simp [hb] at hx7 + step with UScalar.cast.step_spec as ⟨c7, hc7⟩ + have hc7v : c7.val = b23.val := by + rw [hc7, UScalar.cast_val_eq, hx7] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s7, hsh7⟩ + have hsv7 : s7.val = 56 := by clear * - hsh7; scalar_tac + step as ⟨t7, ht7⟩ + have ht7v : t7.val = b23.val * 2^56 := by + rw [ht7] + simp [hsv7, hc7v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y7, hy7⟩ + have hy7v : y7.val = b16.val + b17.val * 2^8 + b18.val * 2^16 + b19.val * 2^24 + b20.val * 2^32 + b21.val * 2^40 + b22.val * 2^48 + b23.val * 2^56 := by + have hult : y6.val < 2^56 := by rw [hy6v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y6.val) (i := 56) hult b23.val + have hadd : y6.val ||| b23.val * 2^56 = y6.val + b23.val * 2^56 := by + calc y6.val ||| b23.val * 2^56 + = y6.val ||| 2^56 * b23.val := by rw [Nat.mul_comm] + _ = 2^56 * b23.val ||| y6.val := Nat.lor_comm _ _ + _ = 2^56 * b23.val + y6.val := hor.symm + _ = y6.val + b23.val * 2^56 := by ring + simp only [hy7, UScalar.val_or, ht7v] + rw [hadd, hy6v] + try ring + step as ⟨bi7, hbi7⟩ + have hbi7v : bi7 = 8#usize := by clear * - hbi7; scalar_tac + rw [hbi7v] + try simp only [spec_ok] + -- exit: bi = 8, done (self, t) + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_neg (show ¬ (8#usize < 8#usize) by scalar_tac)] + try simp only [spec_ok] + exact ⟨True.intro, hy7v⟩ + +/-- Inner LE-load loop for word 3: t accumulates bytes 24..31 + little-endian. The scalar struct passes through unchanged. -/ +theorem naf_word_loop_spec_3 (self : scalar.Scalar) + (b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31 : Std.U8) + (hb : (↑self.bytes : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31]) : + scalar.Scalar.non_adjacent_form_loop0_loop0 self 3#usize 0#u64 0#usize + ⦃ p => p.1 = self ∧ p.2.val = b24.val + b25.val * 2^8 + b26.val * 2^16 + b27.val * 2^24 + b28.val * 2^32 + b29.val * 2^40 + b30.val * 2^48 + b31.val * 2^56 ⦄ := by + have hsz64 : (U64.size : ℕ) = 2^64 := by scalar_tac + have hbb24 : b24.val < 2^8 := by scalar_tac + have hbb25 : b25.val < 2^8 := by scalar_tac + have hbb26 : b26.val < 2^8 := by scalar_tac + have hbb27 : b27.val < 2^8 := by scalar_tac + have hbb28 : b28.val < 2^8 := by scalar_tac + have hbb29 : b29.val < 2^8 := by scalar_tac + have hbb30 : b30.val < 2^8 := by scalar_tac + have hbb31 : b31.val < 2^8 := by scalar_tac + unfold scalar.Scalar.non_adjacent_form_loop0_loop0 + -- bi = 0: byte 24 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (0#usize < 8#usize) by scalar_tac)] + step as ⟨i0, hi0⟩ + have hi0v : i0 = 24#usize := by clear * - hi0; scalar_tac + rw [hi0v] + step as ⟨i10, hi10⟩ + have hi10v : i10 = 24#usize := by clear * - hi10; scalar_tac + rw [hi10v] + step as ⟨x0, hx0⟩ + simp [hb] at hx0 + step with UScalar.cast.step_spec as ⟨c0, hc0⟩ + have hc0v : c0.val = b24.val := by + rw [hc0, UScalar.cast_val_eq, hx0] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s0, hsh0⟩ + have hsv0 : s0.val = 0 := by clear * - hsh0; scalar_tac + step as ⟨t0, ht0⟩ + have ht0v : t0.val = b24.val * 2^0 := by + rw [ht0] + simp [hsv0, hc0v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y0, hy0⟩ + have hy0v : y0.val = b24.val := by + simp [hy0, UScalar.val_or, ht0v] + step as ⟨bi0, hbi0⟩ + have hbi0v : bi0 = 1#usize := by clear * - hbi0; scalar_tac + rw [hbi0v] + try simp only [spec_ok] + -- bi = 1: byte 25 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (1#usize < 8#usize) by scalar_tac)] + step as ⟨i1, hi1⟩ + have hi1v : i1 = 24#usize := by clear * - hi1; scalar_tac + rw [hi1v] + step as ⟨i11, hi11⟩ + have hi11v : i11 = 25#usize := by clear * - hi11; scalar_tac + rw [hi11v] + step as ⟨x1, hx1⟩ + simp [hb] at hx1 + step with UScalar.cast.step_spec as ⟨c1, hc1⟩ + have hc1v : c1.val = b25.val := by + rw [hc1, UScalar.cast_val_eq, hx1] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s1, hsh1⟩ + have hsv1 : s1.val = 8 := by clear * - hsh1; scalar_tac + step as ⟨t1, ht1⟩ + have ht1v : t1.val = b25.val * 2^8 := by + rw [ht1] + simp [hsv1, hc1v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y1, hy1⟩ + have hy1v : y1.val = b24.val + b25.val * 2^8 := by + have hult : y0.val < 2^8 := by rw [hy0v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y0.val) (i := 8) hult b25.val + have hadd : y0.val ||| b25.val * 2^8 = y0.val + b25.val * 2^8 := by + calc y0.val ||| b25.val * 2^8 + = y0.val ||| 2^8 * b25.val := by rw [Nat.mul_comm] + _ = 2^8 * b25.val ||| y0.val := Nat.lor_comm _ _ + _ = 2^8 * b25.val + y0.val := hor.symm + _ = y0.val + b25.val * 2^8 := by ring + simp only [hy1, UScalar.val_or, ht1v] + rw [hadd, hy0v] + try ring + step as ⟨bi1, hbi1⟩ + have hbi1v : bi1 = 2#usize := by clear * - hbi1; scalar_tac + rw [hbi1v] + try simp only [spec_ok] + -- bi = 2: byte 26 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (2#usize < 8#usize) by scalar_tac)] + step as ⟨i2, hi2⟩ + have hi2v : i2 = 24#usize := by clear * - hi2; scalar_tac + rw [hi2v] + step as ⟨i12, hi12⟩ + have hi12v : i12 = 26#usize := by clear * - hi12; scalar_tac + rw [hi12v] + step as ⟨x2, hx2⟩ + simp [hb] at hx2 + step with UScalar.cast.step_spec as ⟨c2, hc2⟩ + have hc2v : c2.val = b26.val := by + rw [hc2, UScalar.cast_val_eq, hx2] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s2, hsh2⟩ + have hsv2 : s2.val = 16 := by clear * - hsh2; scalar_tac + step as ⟨t2, ht2⟩ + have ht2v : t2.val = b26.val * 2^16 := by + rw [ht2] + simp [hsv2, hc2v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y2, hy2⟩ + have hy2v : y2.val = b24.val + b25.val * 2^8 + b26.val * 2^16 := by + have hult : y1.val < 2^16 := by rw [hy1v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y1.val) (i := 16) hult b26.val + have hadd : y1.val ||| b26.val * 2^16 = y1.val + b26.val * 2^16 := by + calc y1.val ||| b26.val * 2^16 + = y1.val ||| 2^16 * b26.val := by rw [Nat.mul_comm] + _ = 2^16 * b26.val ||| y1.val := Nat.lor_comm _ _ + _ = 2^16 * b26.val + y1.val := hor.symm + _ = y1.val + b26.val * 2^16 := by ring + simp only [hy2, UScalar.val_or, ht2v] + rw [hadd, hy1v] + try ring + step as ⟨bi2, hbi2⟩ + have hbi2v : bi2 = 3#usize := by clear * - hbi2; scalar_tac + rw [hbi2v] + try simp only [spec_ok] + -- bi = 3: byte 27 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (3#usize < 8#usize) by scalar_tac)] + step as ⟨i3, hi3⟩ + have hi3v : i3 = 24#usize := by clear * - hi3; scalar_tac + rw [hi3v] + step as ⟨i13, hi13⟩ + have hi13v : i13 = 27#usize := by clear * - hi13; scalar_tac + rw [hi13v] + step as ⟨x3, hx3⟩ + simp [hb] at hx3 + step with UScalar.cast.step_spec as ⟨c3, hc3⟩ + have hc3v : c3.val = b27.val := by + rw [hc3, UScalar.cast_val_eq, hx3] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s3, hsh3⟩ + have hsv3 : s3.val = 24 := by clear * - hsh3; scalar_tac + step as ⟨t3, ht3⟩ + have ht3v : t3.val = b27.val * 2^24 := by + rw [ht3] + simp [hsv3, hc3v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y3, hy3⟩ + have hy3v : y3.val = b24.val + b25.val * 2^8 + b26.val * 2^16 + b27.val * 2^24 := by + have hult : y2.val < 2^24 := by rw [hy2v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y2.val) (i := 24) hult b27.val + have hadd : y2.val ||| b27.val * 2^24 = y2.val + b27.val * 2^24 := by + calc y2.val ||| b27.val * 2^24 + = y2.val ||| 2^24 * b27.val := by rw [Nat.mul_comm] + _ = 2^24 * b27.val ||| y2.val := Nat.lor_comm _ _ + _ = 2^24 * b27.val + y2.val := hor.symm + _ = y2.val + b27.val * 2^24 := by ring + simp only [hy3, UScalar.val_or, ht3v] + rw [hadd, hy2v] + try ring + step as ⟨bi3, hbi3⟩ + have hbi3v : bi3 = 4#usize := by clear * - hbi3; scalar_tac + rw [hbi3v] + try simp only [spec_ok] + -- bi = 4: byte 28 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (4#usize < 8#usize) by scalar_tac)] + step as ⟨i4, hi4⟩ + have hi4v : i4 = 24#usize := by clear * - hi4; scalar_tac + rw [hi4v] + step as ⟨i14, hi14⟩ + have hi14v : i14 = 28#usize := by clear * - hi14; scalar_tac + rw [hi14v] + step as ⟨x4, hx4⟩ + simp [hb] at hx4 + step with UScalar.cast.step_spec as ⟨c4, hc4⟩ + have hc4v : c4.val = b28.val := by + rw [hc4, UScalar.cast_val_eq, hx4] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s4, hsh4⟩ + have hsv4 : s4.val = 32 := by clear * - hsh4; scalar_tac + step as ⟨t4, ht4⟩ + have ht4v : t4.val = b28.val * 2^32 := by + rw [ht4] + simp [hsv4, hc4v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y4, hy4⟩ + have hy4v : y4.val = b24.val + b25.val * 2^8 + b26.val * 2^16 + b27.val * 2^24 + b28.val * 2^32 := by + have hult : y3.val < 2^32 := by rw [hy3v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y3.val) (i := 32) hult b28.val + have hadd : y3.val ||| b28.val * 2^32 = y3.val + b28.val * 2^32 := by + calc y3.val ||| b28.val * 2^32 + = y3.val ||| 2^32 * b28.val := by rw [Nat.mul_comm] + _ = 2^32 * b28.val ||| y3.val := Nat.lor_comm _ _ + _ = 2^32 * b28.val + y3.val := hor.symm + _ = y3.val + b28.val * 2^32 := by ring + simp only [hy4, UScalar.val_or, ht4v] + rw [hadd, hy3v] + try ring + step as ⟨bi4, hbi4⟩ + have hbi4v : bi4 = 5#usize := by clear * - hbi4; scalar_tac + rw [hbi4v] + try simp only [spec_ok] + -- bi = 5: byte 29 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (5#usize < 8#usize) by scalar_tac)] + step as ⟨i5, hi5⟩ + have hi5v : i5 = 24#usize := by clear * - hi5; scalar_tac + rw [hi5v] + step as ⟨i15, hi15⟩ + have hi15v : i15 = 29#usize := by clear * - hi15; scalar_tac + rw [hi15v] + step as ⟨x5, hx5⟩ + simp [hb] at hx5 + step with UScalar.cast.step_spec as ⟨c5, hc5⟩ + have hc5v : c5.val = b29.val := by + rw [hc5, UScalar.cast_val_eq, hx5] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s5, hsh5⟩ + have hsv5 : s5.val = 40 := by clear * - hsh5; scalar_tac + step as ⟨t5, ht5⟩ + have ht5v : t5.val = b29.val * 2^40 := by + rw [ht5] + simp [hsv5, hc5v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y5, hy5⟩ + have hy5v : y5.val = b24.val + b25.val * 2^8 + b26.val * 2^16 + b27.val * 2^24 + b28.val * 2^32 + b29.val * 2^40 := by + have hult : y4.val < 2^40 := by rw [hy4v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y4.val) (i := 40) hult b29.val + have hadd : y4.val ||| b29.val * 2^40 = y4.val + b29.val * 2^40 := by + calc y4.val ||| b29.val * 2^40 + = y4.val ||| 2^40 * b29.val := by rw [Nat.mul_comm] + _ = 2^40 * b29.val ||| y4.val := Nat.lor_comm _ _ + _ = 2^40 * b29.val + y4.val := hor.symm + _ = y4.val + b29.val * 2^40 := by ring + simp only [hy5, UScalar.val_or, ht5v] + rw [hadd, hy4v] + try ring + step as ⟨bi5, hbi5⟩ + have hbi5v : bi5 = 6#usize := by clear * - hbi5; scalar_tac + rw [hbi5v] + try simp only [spec_ok] + -- bi = 6: byte 30 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (6#usize < 8#usize) by scalar_tac)] + step as ⟨i6, hi6⟩ + have hi6v : i6 = 24#usize := by clear * - hi6; scalar_tac + rw [hi6v] + step as ⟨i16, hi16⟩ + have hi16v : i16 = 30#usize := by clear * - hi16; scalar_tac + rw [hi16v] + step as ⟨x6, hx6⟩ + simp [hb] at hx6 + step with UScalar.cast.step_spec as ⟨c6, hc6⟩ + have hc6v : c6.val = b30.val := by + rw [hc6, UScalar.cast_val_eq, hx6] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s6, hsh6⟩ + have hsv6 : s6.val = 48 := by clear * - hsh6; scalar_tac + step as ⟨t6, ht6⟩ + have ht6v : t6.val = b30.val * 2^48 := by + rw [ht6] + simp [hsv6, hc6v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y6, hy6⟩ + have hy6v : y6.val = b24.val + b25.val * 2^8 + b26.val * 2^16 + b27.val * 2^24 + b28.val * 2^32 + b29.val * 2^40 + b30.val * 2^48 := by + have hult : y5.val < 2^48 := by rw [hy5v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y5.val) (i := 48) hult b30.val + have hadd : y5.val ||| b30.val * 2^48 = y5.val + b30.val * 2^48 := by + calc y5.val ||| b30.val * 2^48 + = y5.val ||| 2^48 * b30.val := by rw [Nat.mul_comm] + _ = 2^48 * b30.val ||| y5.val := Nat.lor_comm _ _ + _ = 2^48 * b30.val + y5.val := hor.symm + _ = y5.val + b30.val * 2^48 := by ring + simp only [hy6, UScalar.val_or, ht6v] + rw [hadd, hy5v] + try ring + step as ⟨bi6, hbi6⟩ + have hbi6v : bi6 = 7#usize := by clear * - hbi6; scalar_tac + rw [hbi6v] + try simp only [spec_ok] + -- bi = 7: byte 31 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_pos (show (7#usize < 8#usize) by scalar_tac)] + step as ⟨i7, hi7⟩ + have hi7v : i7 = 24#usize := by clear * - hi7; scalar_tac + rw [hi7v] + step as ⟨i17, hi17⟩ + have hi17v : i17 = 31#usize := by clear * - hi17; scalar_tac + rw [hi17v] + step as ⟨x7, hx7⟩ + simp [hb] at hx7 + step with UScalar.cast.step_spec as ⟨c7, hc7⟩ + have hc7v : c7.val = b31.val := by + rw [hc7, UScalar.cast_val_eq, hx7] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + step as ⟨s7, hsh7⟩ + have hsv7 : s7.val = 56 := by clear * - hsh7; scalar_tac + step as ⟨t7, ht7⟩ + have ht7v : t7.val = b31.val * 2^56 := by + rw [ht7] + simp [hsv7, hc7v, Nat.shiftLeft_eq, hsz64] + omega + step as ⟨y7, hy7⟩ + have hy7v : y7.val = b24.val + b25.val * 2^8 + b26.val * 2^16 + b27.val * 2^24 + b28.val * 2^32 + b29.val * 2^40 + b30.val * 2^48 + b31.val * 2^56 := by + have hult : y6.val < 2^56 := by rw [hy6v]; omega + have hor := Nat.two_pow_add_eq_or_of_lt (b := y6.val) (i := 56) hult b31.val + have hadd : y6.val ||| b31.val * 2^56 = y6.val + b31.val * 2^56 := by + calc y6.val ||| b31.val * 2^56 + = y6.val ||| 2^56 * b31.val := by rw [Nat.mul_comm] + _ = 2^56 * b31.val ||| y6.val := Nat.lor_comm _ _ + _ = 2^56 * b31.val + y6.val := hor.symm + _ = y6.val + b31.val * 2^56 := by ring + simp only [hy7, UScalar.val_or, ht7v] + rw [hadd, hy6v] + try ring + step as ⟨bi7, hbi7⟩ + have hbi7v : bi7 = 8#usize := by clear * - hbi7; scalar_tac + rw [hbi7v] + try simp only [spec_ok] + -- exit: bi = 8, done (self, t) + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0_loop0.body] + rw [if_neg (show ¬ (8#usize < 8#usize) by scalar_tac)] + try simp only [spec_ok] + exact ⟨True.intro, hy7v⟩ + +/-- Outer LE-load loop: fills x_u64[0..3] with the four little-endian + words of the 32 scalar bytes; x_u64[4] stays 0 (the carry pad). -/ +theorem naf_load_spec (self : scalar.Scalar) + (x_u64 : Std.Array Std.U64 5#usize) + (b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31 : Std.U8) + (hb : (↑self.bytes : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31]) + (hx : (↑x_u64 : List Std.U64) = [0#u64, 0#u64, 0#u64, 0#u64, 0#u64]) : + scalar.Scalar.non_adjacent_form_loop0 self x_u64 0#usize + ⦃ ws => ∃ v0 v1 v2 v3 : U64, + (↑ws : List Std.U64) = [v0, v1, v2, v3, 0#u64] ∧ + v0.val = b0.val + b1.val * 2^8 + b2.val * 2^16 + b3.val * 2^24 + b4.val * 2^32 + b5.val * 2^40 + b6.val * 2^48 + b7.val * 2^56 ∧ + v1.val = b8.val + b9.val * 2^8 + b10.val * 2^16 + b11.val * 2^24 + b12.val * 2^32 + b13.val * 2^40 + b14.val * 2^48 + b15.val * 2^56 ∧ + v2.val = b16.val + b17.val * 2^8 + b18.val * 2^16 + b19.val * 2^24 + b20.val * 2^32 + b21.val * 2^40 + b22.val * 2^48 + b23.val * 2^56 ∧ + v3.val = b24.val + b25.val * 2^8 + b26.val * 2^16 + b27.val * 2^24 + b28.val * 2^32 + b29.val * 2^40 + b30.val * 2^48 + b31.val * 2^56 ⦄ := by + unfold scalar.Scalar.non_adjacent_form_loop0 + -- k = 0: word 0 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0.body] + rw [if_pos (show (0#usize < 4#usize) by scalar_tac)] + step with (naf_word_loop_spec_0 self b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31 hb) as ⟨s0, t0, hs0, ht0⟩ + rw [hs0] + step as ⟨a0, ha0⟩ + have hl0 : (↑a0 : List Std.U64) = [t0, 0#u64, 0#u64, 0#u64, 0#u64] := by + simp only [ha0, Array.set_val_eq, hx] + rfl + step as ⟨k0, hk0⟩ + have hk0v : k0 = 1#usize := by clear * - hk0; scalar_tac + rw [hk0v] + try simp only [spec_ok] + -- k = 1: word 1 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0.body] + rw [if_pos (show (1#usize < 4#usize) by scalar_tac)] + step with (naf_word_loop_spec_1 self b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31 hb) as ⟨s1, t1, hs1, ht1⟩ + rw [hs1] + step as ⟨a1, ha1⟩ + have hl1 : (↑a1 : List Std.U64) = [t0, t1, 0#u64, 0#u64, 0#u64] := by + simp only [ha1, Array.set_val_eq, hl0] + rfl + step as ⟨k1, hk1⟩ + have hk1v : k1 = 2#usize := by clear * - hk1; scalar_tac + rw [hk1v] + try simp only [spec_ok] + -- k = 2: word 2 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0.body] + rw [if_pos (show (2#usize < 4#usize) by scalar_tac)] + step with (naf_word_loop_spec_2 self b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31 hb) as ⟨s2, t2, hs2, ht2⟩ + rw [hs2] + step as ⟨a2, ha2⟩ + have hl2 : (↑a2 : List Std.U64) = [t0, t1, t2, 0#u64, 0#u64] := by + simp only [ha2, Array.set_val_eq, hl1] + rfl + step as ⟨k2, hk2⟩ + have hk2v : k2 = 3#usize := by clear * - hk2; scalar_tac + rw [hk2v] + try simp only [spec_ok] + -- k = 3: word 3 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0.body] + rw [if_pos (show (3#usize < 4#usize) by scalar_tac)] + step with (naf_word_loop_spec_3 self b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31 hb) as ⟨s3, t3, hs3, ht3⟩ + rw [hs3] + step as ⟨a3, ha3⟩ + have hl3 : (↑a3 : List Std.U64) = [t0, t1, t2, t3, 0#u64] := by + simp only [ha3, Array.set_val_eq, hl2] + rfl + step as ⟨k3, hk3⟩ + have hk3v : k3 = 4#usize := by clear * - hk3; scalar_tac + rw [hk3v] + try simp only [spec_ok] + -- exit: k = 4, done x_u64 + apply loop_step + simp only [scalar.Scalar.non_adjacent_form_loop0.body] + rw [if_neg (show ¬ (4#usize < 4#usize) by scalar_tac)] + try simp only [spec_ok] + exact ⟨t0, t1, t2, t3, hl3, ht0, ht1, ht2, ht3⟩ + +end CurveFieldProofs diff --git a/verification/Proofs/DsmNafMath.lean b/verification/Proofs/DsmNafMath.lean new file mode 100644 index 0000000..e3f04ac --- /dev/null +++ b/verification/Proofs/DsmNafMath.lean @@ -0,0 +1,239 @@ +/- ────────────────────────────────────────────────────────────────────────────── + Proofs/DsmNafMath.lean — NAF campaign, stage 2: the pure arithmetic core + of the w=5 NAF digit loop (no extraction dependence beyond `nafDigit`). + + The digit loop's state is (naf, pos, carry) with the exact ℤ invariant + nafSum naf 256 + carry·2^pos = V mod 2^pos + (digits at k ≥ pos all zero, carry ≤ 1, and carry = 1 → pos ≤ 254 given + V < 2^253 — the component that kills the carry at exit). + + Step theorems the monadic walk plugs in: + · `nafSum_set` — writing a fresh digit adds d·2^pos to the sum. + · `div_pow_shift` / `mod32_absorb` / `naf_window_single` / `naf_window_cross` + — the 64-bit buffer read at bit position p+b sees (V >> (p+b)) mod 32 + (single word when b + 5 ≤ 64; cross-word via disjoint-OR otherwise). + · `naf_even_step` — even window ⇒ pos+1, carry preserved (the parity + of V >> pos matches carry, so both sides absorb carry·2^(pos+1)). + · `naf_odd_step` — odd window ⇒ digit (window − 32·carry'), pos+5: + the digit plus the new carry reconstruct the 5 consumed bits + (Nat.mod_mul telescoping). + · `naf_carry_even` / `naf_carry_odd` — carry = 1 → pos ≤ 254 propagation + from V < 2^253. + · `naf_exit` — pos ≥ 256 kills the carry: nafSum = V exactly. + ────────────────────────────────────────────────────────────────────────────── -/ +import Proofs.DsmLoopSpec +open Aeneas Aeneas.Std +open curve25519_dalek + +set_option maxHeartbeats 4000000 +set_option linter.unusedSimpArgs false +set_option maxRecDepth 8000 + +namespace CurveFieldProofs + +/-! ### The signed digit sum -/ + +/-- Σ_{k> b plus the rest shifted down. -/ +theorem div_pow_shift (lo w rest p b : ℕ) (hlo : lo < 2^p) (hb : b ≤ 64) : + (lo + 2^p * (w + 2^64 * rest)) / 2^(p+b) = w / 2^b + 2^(64-b) * rest := by + have hp : (0:ℕ) < 2^p := Nat.two_pow_pos p + have hbp : (0:ℕ) < 2^b := Nat.two_pow_pos b + rw [pow_add, ← Nat.div_div_eq_div_mul] + have h1 : (lo + 2^p * (w + 2^64 * rest)) / 2^p = w + 2^64 * rest := by + rw [Nat.add_mul_div_left _ _ hp, Nat.div_eq_of_lt hlo, Nat.zero_add] + rw [h1] + have h2 : (2:ℕ)^64 = 2^b * 2^(64-b) := by + rw [← pow_add]; congr 1; omega + rw [h2, Nat.mul_assoc, Nat.add_mul_div_left _ _ hbp] + +/-- Multiples of 2^m (m ≥ 5) vanish mod 32. -/ +theorem mod32_absorb (x y m : ℕ) (hm : 5 ≤ m) : + (x + 2^m * y) % 32 = x % 32 := by + have h : (2:ℕ)^m = 32 * 2^(m-5) := by + rw [show (32:ℕ) = 2^5 by norm_num, ← pow_add]; congr 1; omega + rw [h, Nat.mul_assoc, Nat.add_mul_mod_self_left] + +/-- Single-word window read: when the 5-bit window at bit b fits inside + word w (b + 5 ≤ 64), (w >> b) mod 32 is the value's window at p+b. -/ +theorem naf_window_single (V lo w rest p b : ℕ) + (hV : V = lo + 2^p * (w + 2^64 * rest)) (hlo : lo < 2^p) (hb : b + 5 ≤ 64) : + (w / 2^b) % 32 = (V / 2^(p+b)) % 32 := by + rw [hV, div_pow_shift lo w rest p b hlo (by omega)] + exact (mod32_absorb _ _ _ (by omega)).symm + +/-- Cross-word window read: when the window at bit b straddles into the next + word w' (b ≥ 60), the extracted read (w >> b) ||| ((w' << (64−b)) mod 2^64) + still sees the value's window at p+b, mod 32. -/ +theorem naf_window_cross (V lo w w' rest p b : ℕ) + (hV : V = lo + 2^p * (w + 2^64 * (w' + 2^64 * rest))) + (hlo : lo < 2^p) (hw : w < 2^64) (hb : b < 64) : + ((w / 2^b) ||| (w' <<< (64 - b)) % 2^64) % 32 = (V / 2^(p+b)) % 32 := by + have hp64 : (2:ℕ)^(64-b) * 2^b = 2^64 := by + rw [← pow_add]; congr 1; omega + have hp128 : (2:ℕ)^(64-b) * 2^64 = 2^(128-b) := by + rw [← pow_add]; congr 1; omega + -- the truncated shift: (w' << (64−b)) mod 2^64 = 2^(64−b)·(w' mod 2^b) + have hsh : (w' <<< (64 - b)) % 2^64 = 2^(64-b) * (w' % 2^b) := by + rw [Nat.shiftLeft_eq, Nat.mul_comm w' _, ← hp64, Nat.mul_mod_mul_left] + -- the OR is disjoint: w >> b < 2^(64−b) + have hdl : w / 2^b < 2^(64-b) := by + rw [Nat.div_lt_iff_lt_mul (Nat.two_pow_pos b)] + calc w < 2^64 := hw + _ = 2^(64-b) * 2^b := hp64.symm + have hor := Nat.two_pow_add_eq_or_of_lt (b := w / 2^b) (i := 64-b) hdl (w' % 2^b) + rw [hsh, Nat.lor_comm, ← hor] + -- the value side + rw [hV, div_pow_shift lo w _ p b hlo (by omega)] + -- both sides are (w/2^b + 2^(64−b)·(w' mod 2^b)) mod 32 after absorbing + -- the 2^64-multiples: w' = w' mod 2^b + 2^b·(w'/2^b) + have hw' : w' = w' % 2^b + 2^b * (w' / 2^b) := (Nat.mod_add_div _ _).symm + have e1 : w / 2^b + 2^(64-b) * (w' + 2^64 * rest) + = (2^(64-b) * (w' % 2^b) + w / 2^b) + + 2^64 * (w' / 2^b + 2^(64-b) * rest) := by + conv_lhs => rw [hw'] + rw [Nat.mul_add, Nat.mul_add, Nat.mul_add, ← Nat.mul_assoc, hp64, + ← Nat.mul_assoc, hp128] + have hp128' : (2:ℕ)^(128-b) = 2^64 * 2^(64-b) := by + rw [← pow_add]; congr 1; omega + rw [hp128'] + ring + rw [e1] + have := mod32_absorb (2^(64-b) * (w' % 2^b) + w / 2^b) + (w' / 2^b + 2^(64-b) * rest) 64 (by omega) + rw [this] + +/-! ### Invariant step theorems -/ + +/-- Even window: digit 0, position advances by 1, carry preserved. + The parity of V >> pos equals the carry, so the invariant extends. -/ +theorem naf_even_step (V pos : ℕ) (carry : ℕ) (S : ℤ) + (hc : carry ≤ 1) + (hinv : S + carry * 2^pos = ((V % 2^pos : ℕ) : ℤ)) + (heven : (carry + (V / 2^pos) % 32) % 2 = 0) : + S + carry * 2^(pos+1) = ((V % 2^(pos+1) : ℕ) : ℤ) := by + have hmm : V % 2^(pos+1) = V % 2^pos + 2^pos * ((V / 2^pos) % 2) := by + rw [pow_succ, Nat.mod_mul] + have hpar : (V / 2^pos) % 2 = carry := by omega + rw [hmm, hpar] + push_cast at hinv ⊢ + linear_combination hinv + +/-- Odd window: digit window − 32·carry', position advances by 5. + The digit plus the promoted carry reconstruct the 5 consumed bits. -/ +theorem naf_odd_step (V pos : ℕ) (carry carry' : ℕ) (S d : ℤ) + (hinv : S + carry * 2^pos = ((V % 2^pos : ℕ) : ℤ)) + (hd : d = (carry : ℤ) + ((V / 2^pos) % 32 : ℕ) - 32 * carry') : + (S + d * 2^pos) + carry' * 2^(pos+5) = ((V % 2^(pos+5) : ℕ) : ℤ) := by + have hmm : V % 2^(pos+5) = V % 2^pos + 2^pos * ((V / 2^pos) % 32) := by + have h : (2:ℕ)^(pos+5) = 2^pos * 32 := by rw [pow_add]; norm_num + rw [h, Nat.mod_mul] + rw [hmm, hd] + push_cast at hinv ⊢ + linear_combination hinv + +/-- Carry propagation, even step: with V < 2^253, an even step that keeps + carry = 1 must be reading a set bit, so pos ≤ 252 and pos+1 ≤ 254. -/ +theorem naf_carry_even (V pos : ℕ) (carry : ℕ) (hV : V < 2^253) + (hc : carry ≤ 1) + (heven : (carry + (V / 2^pos) % 32) % 2 = 0) : + carry = 1 → pos + 1 ≤ 254 := by + intro h1 + subst h1 + have h3 : 1 ≤ (V / 2^pos) % 32 := by + generalize (V / 2^pos) % 32 = r at heven ⊢ + omega + have hge : 1 ≤ V / 2^pos := le_trans h3 (Nat.mod_le _ _) + have hle : 2^pos ≤ V := by + have h5 := (Nat.le_div_iff_mul_le (Nat.two_pow_pos pos)).mp hge + simpa using h5 + have hpb : pos ≤ 252 := by + by_contra h + have h253 : (2:ℕ)^253 ≤ 2^pos := Nat.pow_le_pow_right (by norm_num) (by omega) + exact absurd (lt_of_le_of_lt (le_trans h253 hle) hV) (lt_irrefl _) + omega + +/-- Carry propagation, odd step: producing carry' = 1 needs window ≥ 16, so + V >> pos ≥ 15, forcing pos ≤ 249 (V < 2^253) and pos+5 ≤ 254. -/ +theorem naf_carry_odd (V pos : ℕ) (carry carry' : ℕ) (hV : V < 2^253) + (hc : carry ≤ 1) + (hcw : (carry + (V / 2^pos) % 32 < 16 ∧ carry' = 0) ∨ + (16 ≤ carry + (V / 2^pos) % 32 ∧ carry' = 1)) : + carry' = 1 → pos + 5 ≤ 254 := by + intro h1 + rcases hcw with ⟨-, h0⟩ | ⟨hge, -⟩ + · omega + · have h15 : 15 ≤ (V / 2^pos) % 32 := by + generalize (V / 2^pos) % 32 = r at hge ⊢ + omega + have hge15 : 15 ≤ V / 2^pos := le_trans h15 (Nat.mod_le _ _) + have hmul : 15 * 2^pos ≤ V := + (Nat.le_div_iff_mul_le (Nat.two_pow_pos pos)).mp hge15 + have hpb : pos ≤ 249 := by + by_contra h + have h250 : (2:ℕ)^250 ≤ 2^pos := Nat.pow_le_pow_right (by norm_num) (by omega) + have hbig : (2:ℕ)^253 < 15 * 2^250 := by norm_num + have hmono : 15 * 2^250 ≤ 15 * 2^pos := Nat.mul_le_mul_left 15 h250 + exact absurd (lt_of_le_of_lt (le_trans hmono hmul) hV) (not_lt.mpr hbig.le) + omega + +/-- Exit: at pos ≥ 256 the carry must be dead (carry = 1 forces pos ≤ 254), + and V mod 2^pos = V, so the digit sum equals V exactly. -/ +theorem naf_exit (V pos : ℕ) (carry : ℕ) (S : ℤ) (hV : V < 2^253) + (hpos : 256 ≤ pos) (hc : carry ≤ 1) (hcp : carry = 1 → pos ≤ 254) + (hinv : S + carry * 2^pos = ((V % 2^pos : ℕ) : ℤ)) : S = V := by + have hc0 : carry = 0 := by + by_contra h + have h1 : carry = 1 := by omega + have := hcp h1 + omega + subst hc0 + have hmod : V % 2^pos = V := by + apply Nat.mod_eq_of_lt + calc V < 2^253 := hV + _ ≤ 2^pos := Nat.pow_le_pow_right (by norm_num) (by omega) + rw [hmod] at hinv + push_cast at hinv + linarith + +end CurveFieldProofs diff --git a/verification/check.sh b/verification/check.sh index b8e1b35..87e25a0 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -52,16 +52,35 @@ PROOFS=( EdAddAffNiels EdConvert EdMain + DsmTableSpec + DsmStepSpec + DsmLoopSpec + DsmNafLoadSpec + DsmNafMath ) # Fully-qualified certificate names; each must be axiom-clean. CERTS=( CurveFieldProofs.fieldImplementation CurveFieldProofs.edwardsImplementation + CurveFieldProofs.naf_table_spec + CurveFieldProofs.naf_select_spec + CurveFieldProofs.proj_double_law + CurveFieldProofs.compl_as_projective_law + CurveFieldProofs.dsm_step_p_law + CurveFieldProofs.dsm_step_b_law + CurveFieldProofs.dsm_loop_spec + CurveFieldProofs.naf_load_spec + CurveFieldProofs.naf_exit ) # Imports needed so every certificate in CERTS is in scope for the audit. AUDIT_IMPORTS=( Proofs.FieldMain Proofs.EdMain + Proofs.DsmTableSpec + Proofs.DsmStepSpec + Proofs.DsmLoopSpec + Proofs.DsmNafLoadSpec + Proofs.DsmNafMath ) # ── Phase 0: resource + integrity guards ────────────────────────────────────