Helper lemmas for ntt_outerLoop_computes_ref_ntt

theorem n_lt_64_of_pow2_nat (m n : ℕ) (hm : m = 2 ^ n) (hm_dvd : m ∣ mod64.toNat - 1) : n < 64

ℕ-variant: if m = 2^n and m ∣ mod64.toNat - 1, then n < 64.

theorem rootsInner_preserves_bound {n : ℕ} (wm : UInt32) (halfLen k i : ℕ) (v : Vector UInt32 n) (hv : (v.all fun (x : UInt32) => decide (x < mod32)) = true) : ((rootsInner wm halfLen k i v).all fun (x : UInt32) => decide (x < mod32)) = true

rootsInner preserves boundedness of the underlying vector.

theorem outer_preserves_bound (n : ℕ) (v : Vector UInt32 n) (hn : 0 < n) (len : UInt64) (f : ℕ) (hv : (v.all fun (x : UInt32) => decide (x < mod32)) = true) : ((ensureRoots.outer n v len hn f).all fun (x : UInt32) => decide (x < mod32)) = true

ensureRoots.outer preserves boundedness.

theorem ensure_roots_bound {m : UInt64} : ((ensureRoots m.toNat).all fun (x : UInt32) => decide (x < mod32)) = true

All entries of ensureRoots m are strictly below mod32.

theorem ensure_roots_bound_nat (m : ℕ) (hm : m < 2 ^ 64) : ((ensureRoots m).all fun (x : UInt32) => decide (x < mod32)) = true

ℕ-variant of ensure_roots_bound: all entries of ensureRoots m are < mod32.

theorem outerLoop_returns_gt {m : ℕ} (inverse : Bool) (roots a : Vector UInt32 m) (len : UInt64) (fuel : ℕ) (h : len.toNat * 2 > m) : nttInplace.outerLoop inverse roots a len fuel = a

theorem go_computes_log2 (m : UInt64) (n : ℕ) (hm : m.toNat = 2 ^ n) (hn : n < 64) : (nttInplace.go 64 m.toNat 0).toNat = n

theorem go_parity_even_nat (m n : ℕ) (hm : m = 2 ^ n) (hn : n < 64) (hne : Even n) : nttInplace.go 64 m 0 &&& 1 = 0

ℕ-variant: if m = 2^n and n is even, then nttInplace.go 64 m 0 &&& 1 = 0.

theorem go_parity_odd_nat (m n : ℕ) (hm : m = 2 ^ n) (hn : n < 64) (hno : Odd n) : nttInplace.go 64 m 0 &&& 1 ≠ 0

ℕ-variant: if m = 2^n and n is odd, then nttInplace.go 64 m 0 &&& 1 ≠ 0.

def bitRev : ℕ → ℕ → ℕ

bitRev w x reverses the lowest w bits of x.

Equations

• bitRev 0 x✝ = 0
• bitRev w.succ x✝ = 2 ^ w * (x✝ % 2) + bitRev w (x✝ / 2)

@[simp]

theorem bitRev_zero_width (x : ℕ) : bitRev 0 x = 0

@[simp]

theorem bitRev_succ (w x : ℕ) : bitRev (w + 1) x = 2 ^ w * (x % 2) + bitRev w (x / 2)

theorem bitRev_lt (w x : ℕ) : bitRev w x < 2 ^ w

theorem bitRev_index_lt (n q : ℕ) (hq : q ≤ n) (j : Fin (2 ^ q)) (b : ℕ) : 2 ^ (n - q) * ↑j + bitRev (n - q) b < 2 ^ n

noncomputable def ntt_sub_input {m : ℕ} (n q : ℕ) (hq : q ≤ n) (hm_eq : m = 2 ^ n) (v : Vector UInt32 m) (b : ℕ) : Fin (2 ^ q) → ZMod mod32.toNat

Equations

• ntt_sub_input n q hq hm_eq v b j = ↑(toMont v[Fin.cast ⋯ ⟨2 ^ (n - q) * ↑j + bitRev (n - q) b, ⋯⟩]).toNat

def outerLoop_inv {m : ℕ} (n q : ℕ) (hq : q ≤ n) (hm_eq : m = 2 ^ n) (v a : Vector UInt32 m) : Prop

Equations

• One or more equations did not get rendered due to their size.

theorem inv_at_n_implies_ref_ntt {m : ℕ} (n : ℕ) (hm_eq : m = 2 ^ n) (v a : Vector UInt32 m) (hinv : outerLoop_inv n n ⋯ hm_eq v a) : have ω := ↑primRoot.toNat ^ ((mod64.toNat - 1) / m); ∀ (k : Fin m), ↑a[↑k].toNat = ref_ntt n ω (fun (j : Fin (2 ^ n)) => ↑(toMont v[Fin.cast ⋯ j]).toNat) (Fin.cast hm_eq k)

@[simp]

theorem radix4Middle_zero_blocks {n : ℕ} (inverse : Bool) (roots : Vector UInt32 n) (s len b : ℕ) (a : Vector UInt32 n) : radix4Middle inverse roots s len 0 b a = a

When the block count is 0 (which happens when len is large enough relative to m or when len = 0), radix4Middle does nothing.

theorem outerLoop_len_not_gt_nat {m : ℕ} (n q : ℕ) (hm_eq : m = 2 ^ n) (hq2 : q + 2 ≤ n) (len : UInt64) (hlen : len.toNat = 2 ^ (q + 1)) : ¬len.toNat * 2 > m

Nat version of outerLoop_len_not_gt.

theorem vector_map_to_mont_bound {m : ℕ} (v : Vector UInt32 m) (hv : (v.all fun (x : UInt32) => decide (x < mod32)) = true) : ((Vector.map toMont v).all fun (x : UInt32) => decide (x < mod32)) = true

Helper: the toMont mapping preserves the overall bound.

theorem outerLoop_noop_pow2 {m : ℕ} (inverse : Bool) (roots a : Vector UInt32 m) (len : UInt64) (fuel n : ℕ) (hm_eq : m = 2 ^ n) (h : (∃ (k : ℕ), len.toNat = 2 ^ k ∧ n < k ∧ k < 64) ∨ len.toNat = 0) : nttInplace.outerLoop inverse roots a len fuel = a

bitRev radix-4 decomposition

theorem bitRev_four_mul_add_one (w b : ℕ) : bitRev (w + 2) (4 * b + 1) = 2 ^ (w + 1) + bitRev w b

ntt_sub_input stride-4 relations

theorem fin_4mul_lt (q : ℕ) (j : Fin (2 ^ q)) : 4 * ↑j < 2 ^ (q + 2)

theorem fin_4mul1_lt (q : ℕ) (j : Fin (2 ^ q)) : 4 * ↑j + 1 < 2 ^ (q + 2)

theorem fin_4mul2_lt (q : ℕ) (j : Fin (2 ^ q)) : 4 * ↑j + 2 < 2 ^ (q + 2)

theorem fin_4mul3_lt (q : ℕ) (j : Fin (2 ^ q)) : 4 * ↑j + 3 < 2 ^ (q + 2)

theorem pow2q_lt_q2 (q j2 : ℕ) (hj2 : j2 < 2 ^ q) : j2 < 2 ^ (q + 2)

theorem pow2q_add_q_lt_q2 (q j2 : ℕ) (hj2 : j2 < 2 ^ q) : j2 + 2 ^ q < 2 ^ (q + 2)

theorem pow2q_add_q1_lt_q2 (q j2 : ℕ) (hj2 : j2 < 2 ^ q) : j2 + 2 ^ (q + 1) < 2 ^ (q + 2)

theorem pow2q_add_q_q1_lt_q2 (q j2 : ℕ) (hj2 : j2 < 2 ^ q) : j2 + 2 ^ q + 2 ^ (q + 1) < 2 ^ (q + 2)

theorem ntt_sub_input_block_0 {m : ℕ} (n q : ℕ) (hq2 : q + 2 ≤ n) (hm_eq : m = 2 ^ n) (v : Vector UInt32 m) (b : ℕ) (hb : b < 2 ^ (n - q - 2)) (j : Fin (2 ^ q)) : ntt_sub_input n q ⋯ hm_eq v (4 * b) j = ntt_sub_input n (q + 2) hq2 hm_eq v b ⟨4 * ↑j, ⋯⟩

theorem ntt_sub_input_block_1 {m : ℕ} (n q : ℕ) (hq2 : q + 2 ≤ n) (hm_eq : m = 2 ^ n) (v : Vector UInt32 m) (b : ℕ) (j : Fin (2 ^ q)) : ntt_sub_input n q ⋯ hm_eq v (4 * b + 1) j = ntt_sub_input n (q + 2) hq2 hm_eq v b ⟨4 * ↑j + 2, ⋯⟩

theorem ntt_sub_input_block_2 {m : ℕ} (n q : ℕ) (hq2 : q + 2 ≤ n) (hm_eq : m = 2 ^ n) (v : Vector UInt32 m) (b : ℕ) (j : Fin (2 ^ q)) : ntt_sub_input n q ⋯ hm_eq v (4 * b + 2) j = ntt_sub_input n (q + 2) hq2 hm_eq v b ⟨4 * ↑j + 1, ⋯⟩

theorem ntt_sub_input_block_3 {m : ℕ} (n q : ℕ) (hq2 : q + 2 ≤ n) (hm_eq : m = 2 ^ n) (v : Vector UInt32 m) (b : ℕ) (hb : b < 2 ^ (n - q - 2)) (j : Fin (2 ^ q)) : ntt_sub_input n q ⋯ hm_eq v (4 * b + 3) j = ntt_sub_input n (q + 2) hq2 hm_eq v b ⟨4 * ↑j + 3, ⋯⟩

ref_ntt radix-4 unfolding

theorem ref_ntt_radix4_q0 {R : Type u_1} [CommRing R] (q : ℕ) (ω : R) (f : Fin (2 ^ (q + 2)) → R) (j2 : ℕ) (hj2 : j2 < 2 ^ q) : ref_ntt (q + 2) ω f ⟨j2, ⋯⟩ = ref_ntt q (ω ^ 4) (fun (j : Fin (2 ^ q)) => f ⟨4 * ↑j, ⋯⟩) ⟨j2, hj2⟩ + (ω ^ 2) ^ j2 * ref_ntt q (ω ^ 4) (fun (j : Fin (2 ^ q)) => f ⟨4 * ↑j + 2, ⋯⟩) ⟨j2, hj2⟩ + ω ^ j2 * (ref_ntt q (ω ^ 4) (fun (j : Fin (2 ^ q)) => f ⟨4 * ↑j + 1, ⋯⟩) ⟨j2, hj2⟩ + (ω ^ 2) ^ j2 * ref_ntt q (ω ^ 4) (fun (j : Fin (2 ^ q)) => f ⟨4 * ↑j + 3, ⋯⟩) ⟨j2, hj2⟩)

theorem ref_ntt_radix4_q1 {R : Type u_1} [CommRing R] (q : ℕ) (ω : R) (f : Fin (2 ^ (q + 2)) → R) (j2 : ℕ) (hj2 : j2 < 2 ^ q) : ref_ntt (q + 2) ω f ⟨j2 + 2 ^ q, ⋯⟩ = ref_ntt q (ω ^ 4) (fun (j : Fin (2 ^ q)) => f ⟨4 * ↑j, ⋯⟩) ⟨j2, hj2⟩ - (ω ^ 2) ^ j2 * ref_ntt q (ω ^ 4) (fun (j : Fin (2 ^ q)) => f ⟨4 * ↑j + 2, ⋯⟩) ⟨j2, hj2⟩ + ω ^ (j2 + 2 ^ q) * (ref_ntt q (ω ^ 4) (fun (j : Fin (2 ^ q)) => f ⟨4 * ↑j + 1, ⋯⟩) ⟨j2, hj2⟩ - (ω ^ 2) ^ j2 * ref_ntt q (ω ^ 4) (fun (j : Fin (2 ^ q)) => f ⟨4 * ↑j + 3, ⋯⟩) ⟨j2, hj2⟩)

theorem ref_ntt_radix4_q2 {R : Type u_1} [CommRing R] (q : ℕ) (ω : R) (f : Fin (2 ^ (q + 2)) → R) (j2 : ℕ) (hj2 : j2 < 2 ^ q) : ref_ntt (q + 2) ω f ⟨j2 + 2 ^ (q + 1), ⋯⟩ = ref_ntt q (ω ^ 4) (fun (j : Fin (2 ^ q)) => f ⟨4 * ↑j, ⋯⟩) ⟨j2, hj2⟩ + (ω ^ 2) ^ j2 * ref_ntt q (ω ^ 4) (fun (j : Fin (2 ^ q)) => f ⟨4 * ↑j + 2, ⋯⟩) ⟨j2, hj2⟩ - ω ^ j2 * (ref_ntt q (ω ^ 4) (fun (j : Fin (2 ^ q)) => f ⟨4 * ↑j + 1, ⋯⟩) ⟨j2, hj2⟩ + (ω ^ 2) ^ j2 * ref_ntt q (ω ^ 4) (fun (j : Fin (2 ^ q)) => f ⟨4 * ↑j + 3, ⋯⟩) ⟨j2, hj2⟩)

Quadrant 2: position j2 + 2^(q+1).

theorem ref_ntt_radix4_q3 {R : Type u_1} [CommRing R] (q : ℕ) (ω : R) (f : Fin (2 ^ (q + 2)) → R) (j2 : ℕ) (hj2 : j2 < 2 ^ q) : ref_ntt (q + 2) ω f ⟨j2 + 2 ^ q + 2 ^ (q + 1), ⋯⟩ = ref_ntt q (ω ^ 4) (fun (j : Fin (2 ^ q)) => f ⟨4 * ↑j, ⋯⟩) ⟨j2, hj2⟩ - (ω ^ 2) ^ j2 * ref_ntt q (ω ^ 4) (fun (j : Fin (2 ^ q)) => f ⟨4 * ↑j + 2, ⋯⟩) ⟨j2, hj2⟩ - ω ^ (j2 + 2 ^ q) * (ref_ntt q (ω ^ 4) (fun (j : Fin (2 ^ q)) => f ⟨4 * ↑j + 1, ⋯⟩) ⟨j2, hj2⟩ - (ω ^ 2) ^ j2 * ref_ntt q (ω ^ 4) (fun (j : Fin (2 ^ q)) => f ⟨4 * ↑j + 3, ⋯⟩) ⟨j2, hj2⟩)

theorem ntt_block_pos_arith_nat {m : ℕ} (n q : ℕ) (hq2 : q + 2 ≤ n) (hm_eq : m = 2 ^ n) (hn64 : n < 64) (len : UInt64) (hlen : len.toNat = 2 ^ (q + 1)) (b' j2' : ℕ) (hb' : b' < 2 ^ (n - q - 2)) (hj2' : j2' < 2 ^ q) : have s := len >>> 1; have i2' := (b' * 2 * len.toNat).toUInt64; i2'.toNat = b' * 2 ^ (q + 2) ∧ (i2' + j2'.toUInt64).toNat = b' * 2 ^ (q + 2) + j2' ∧ (i2' + j2'.toUInt64 + s).toNat = b' * 2 ^ (q + 2) + j2' + 2 ^ q ∧ (i2' + len + j2'.toUInt64).toNat = b' * 2 ^ (q + 2) + j2' + 2 ^ (q + 1) ∧ (i2' + len + j2'.toUInt64 + s).toNat = b' * 2 ^ (q + 2) + j2' + 2 ^ (q + 1) + 2 ^ q ∧ (i2' + j2'.toUInt64).toNat < m ∧ (i2' + j2'.toUInt64 + s).toNat < m ∧ (i2' + len + j2'.toUInt64).toNat < m ∧ (i2' + len + j2'.toUInt64 + s).toNat < m

Position arithmetic for block b', with ℕ size bound m.

theorem radix4Middle_comp {N : ℕ} (inverse : Bool) (roots : Vector UInt32 N) (s len k1 k2 b_start : ℕ) (a : Vector UInt32 N) : radix4Middle inverse roots s len (k1 + k2) b_start a = radix4Middle inverse roots s len k2 (b_start + k1) (radix4Middle inverse roots s len k1 b_start a)

theorem radix4_block_ne_pos (q b j2 j2nat : ℕ) (hj2 : j2 < 2 ^ q) (hj2_lt : j2nat < 2 ^ q) (hj2_ne : j2 ≠ j2nat) (posval : ℕ) (hpos : posval = b * 2 ^ (q + 2) + j2nat ∨ posval = b * 2 ^ (q + 2) + j2nat + 2 ^ q ∨ posval = b * 2 ^ (q + 2) + j2nat + 2 ^ (q + 1) ∨ posval = b * 2 ^ (q + 2) + j2nat + 2 ^ (q + 1) + 2 ^ q) : b * 2 ^ (q + 2) + j2 ≠ posval ∧ b * 2 ^ (q + 2) + j2 + 2 ^ q ≠ posval ∧ b * 2 ^ (q + 2) + j2 + 2 ^ (q + 1) ≠ posval ∧ b * 2 ^ (q + 2) + j2 + 2 ^ (q + 1) + 2 ^ q ≠ posval

Butterfly at j2 ≠ j2nat does not touch any of the four block positions for j2nat. Isolated so omega runs in minimal context (avoids slow hypothesis scanning).