Correctness proofs for the NTT-based binary convolution pipeline.

theorem ntt_outerLoop_computes_ref_ntt {m : ℕ} (n : ℕ) (hm_eq : m = 2 ^ n) (h_dvd : 2 ^ n ∣ mod64.toNat - 1) (v : Vector UInt32 m) (hv_bound : (v.all fun (x : UInt32) => decide (x < mod32)) = true) (roots : Vector UInt32 m) (hroots : ntt_roots_correct m roots) (hroots_bnd : (roots.all fun (x : UInt32) => decide (x < mod32)) = true) (a_in : Vector UInt32 m) (ha_in : a_in = have a1 := bitRevLoop (m - 1) 0 (Vector.map toMont v) 0; if (nttInplace.go 64 m 0 &&& 1 != 0) = true then radix2Pass (m / 2) 0 a1 else a1) (start : UInt64) (hstart : start = if (nttInplace.go 64 m 0 &&& 1 != 0) = true then 4 else 2) : have ω := ↑primRoot.toNat ^ ((mod64.toNat - 1) / m); ∀ (k : Fin m), ↑(nttInplace.outerLoop false roots a_in start 64)[↑k].toNat = ref_ntt n ω (fun (j : Fin (2 ^ n)) => ↑(toMont v[Fin.cast ⋯ j]).toNat) (Fin.cast hm_eq k)

theorem ntt_inplace_forward_eq_ref_ntt {m : ℕ} (n : ℕ) (hm_eq : m = 2 ^ n) (h_dvd : 2 ^ n ∣ mod64.toNat - 1) (v : Vector UInt32 m) (hv_bound : (v.all fun (x : UInt32) => decide (x < mod32)) = true) (roots : Vector UInt32 m) (hroots : ntt_roots_correct m roots) (hroots_bnd : (roots.all fun (x : UInt32) => decide (x < mod32)) = true) : have ω := ↑primRoot.toNat ^ ((mod64.toNat - 1) / m); ∀ (k : Fin m), ↑(nttInplace v false roots)[↑k].toNat = ref_ntt n ω (fun (j : Fin (2 ^ n)) => ↑(toMont v[Fin.cast ⋯ j]).toNat) (Fin.cast hm_eq k)

theorem ntt_computes_dft_of_montv {m : ℕ} (v : Vector UInt32 m) (hm_pow2 : m.isPowerOfTwo) (hm_dvd : m ∣ mod64.toNat - 1) (hv_bound : (v.all fun (x : UInt32) => decide (x < mod32)) = true) (roots : Vector UInt32 m) (hroots : ntt_roots_correct m roots) (hroots_bnd : (roots.all fun (x : UInt32) => decide (x < mod32)) = true) : have ω := ↑primRoot.toNat ^ ((mod64.toNat - 1) / m); have result := nttInplace v false roots; ∀ (k : Fin result.size), ↑result[k].toNat = ∑ j : Fin m, ↑(toMont v[↑j]).toNat * ω ^ (↑j * ↑k)

The core FFT correctness lemma: nttInplace v false roots computes the DFT of the Montgomery-encoded input v.map toMont. That is, for each output index k, result[k] = Σ_j (toMont (v[j])) · ω^(j·k) in ZMod mod32.toNat.

theorem ntt_inplace_forward_from_roots {m : ℕ} (v : Vector UInt32 m) (hm_pow2 : m.isPowerOfTwo) (hm_dvd : m ∣ mod64.toNat - 1) (hv_bound : (v.all fun (x : UInt32) => decide (x < mod32)) = true) (roots : Vector UInt32 m) (hroots : ntt_roots_correct m roots) (hroots_bnd : (roots.all fun (x : UInt32) => decide (x < mod32)) = true) : have ω := ↑primRoot.toNat ^ ((mod64.toNat - 1) / m); have result := nttInplace v false roots; ∀ (k : Fin result.size), ↑result[k].toNat = ↑montR1.toNat * ∑ j : Fin m, ↑v[↑j].toNat * ω ^ (↑j * ↑k)

theorem ntt_inplace_forward_spec {m : ℕ} (v : Vector UInt32 m) (hm_pow2 : m.isPowerOfTwo) (hm_dvd : m ∣ mod64.toNat - 1) (hv_bound : (v.all fun (x : UInt32) => decide (x < mod32)) = true) : have ω := ↑primRoot.toNat ^ ((mod64.toNat - 1) / m); have result := nttInplace v false (ensureRoots m); ∀ (k : Fin result.size), ↑result[k].toNat = ↑montR1.toNat * ∑ j : Fin m, ↑v[↑j].toNat * ω ^ (↑j * ↑k)

theorem ntt_outerLoop_inv_computes_ref_ntt {m : ℕ} (n : ℕ) (hm_eq : m = 2 ^ n) (h_dvd : 2 ^ n ∣ mod64.toNat - 1) (v : Vector UInt32 m) (hv_bound : (v.all fun (x : UInt32) => decide (x < mod32)) = true) (roots : Vector UInt32 m) (hroots : ntt_roots_correct m roots) (hroots_bnd : (roots.all fun (x : UInt32) => decide (x < mod32)) = true) (a_in : Vector UInt32 m) (ha_in : a_in = have a1 := bitRevLoop (m - 1) 0 v 0; if (nttInplace.go 64 m 0 &&& 1 != 0) = true then radix2Pass (m / 2) 0 a1 else a1) (start : UInt64) (hstart : start = if (nttInplace.go 64 m 0 &&& 1 != 0) = true then 4 else 2) : have ω := ↑primRoot.toNat ^ ((mod64.toNat - 1) / m); ∀ (k : Fin m), ↑(nttInplace.outerLoop true roots a_in start 64)[↑k].toNat = ref_ntt n ω⁻¹ (fun (j : Fin (2 ^ n)) => ↑v[Fin.cast ⋯ j].toNat) (Fin.cast hm_eq k)

theorem ntt_inplace_inverse_correct {m : ℕ} (v : Vector UInt32 m) (hm_pow2 : m.isPowerOfTwo) (hm_dvd : m ∣ mod64.toNat - 1) (hv_bound : (v.all fun (x : UInt32) => decide (x < mod32)) = true) : have ω := ↑primRoot.toNat ^ ((mod64.toNat - 1) / m); have result := nttInplace v true (ensureRoots m); ∀ (k : Fin result.size), ↑result[k].toNat = (↑montR1.toNat)⁻¹ * (↑m)⁻¹ * ∑ j : Fin m, ↑v[↑j].toNat * ω⁻¹ ^ (↑j * ↑k)

── Top-level ─────────────────────────────────────────────────────────────────

Proof of circular_convolution_gf2_correct

Proof outline:

1. The guard m < 2 * n is vacuous when 2 * n fits in UInt64 (from next_pow2_ge).
2. The NTT pipeline computes result[k] = the k-th value of the integer-valued LINEAR convolution of the 0/1 embeddings of a and b (Montgomery factors cancel: forward NTT maps input to Montgomery domain, inverse NTT maps back out).
3. Folding: result[i] + result[i+n] = the integer-valued CIRCULAR convolution at index i (valid because fa, fb have support in [0,n) and m ≥ 2n prevents aliasing).
4. Bit-0 of the folded sum equals the GF(2) circular convolution bit.

def int_circ_conv {n : ℕ} (a b : BitVec n) (i : Fin n) : ℕ

Integer-valued circular convolution: count (mod 2 will give GF(2) result).

Equations

• int_circ_conv a b i = ∑ j : Fin n, (if a.getLsb j = true then 1 else 0) * if b.getLsb (i - j) = true then 1 else 0

def int_lin_conv {n : ℕ} (a b : BitVec n) (k : ℕ) : ℕ

The integer-valued linear convolution of the 0/1 embeddings at index k.

Equations

• int_lin_conv a b k = ∑ j : Fin n, if h : ↑j ≤ k ∧ k - ↑j < n then (if a.getLsb j = true then 1 else 0) * if b.getLsb ⟨k - ↑j, ⋯⟩ = true then 1 else 0 else 0

theorem lin_conv_fold_eq_circ_conv {n : ℕ} (a b : BitVec n) (i : Fin n) : int_lin_conv a b ↑i + int_lin_conv a b (↑i + n) = int_circ_conv a b i

def vec_circ_conv {m : ℕ} (fa fb : Vector UInt32 m) (k : Fin m) : ℕ

Integer circular convolution of two UInt32 vectors. (fa ⊛_m fb)[k] = Σ_j fa[j] * fb[(k - j) mod m] This is what the NTT pipeline computes internally (modulo mod32).

Equations

• vec_circ_conv fa fb k = ∑ j : Fin m, (fa.get j).toNat * (fb.get ⟨(↑k + m - ↑j) % m, ⋯⟩).toNat

theorem vec_circ_conv_zero_padded {n m : ℕ} (a b : BitVec n) (hm : 2 * n ≤ m) (k : Fin m) (fa fb : Vector UInt32 m) (hfa : ∀ (i : Fin m), (fa.get i).toNat = if h : ↑i < n then if a.getLsb ⟨↑i, h⟩ = true then 1 else 0 else 0) (hfb : ∀ (i : Fin m), (fb.get i).toNat = if h : ↑i < n then if b.getLsb ⟨↑i, h⟩ = true then 1 else 0 else 0) : vec_circ_conv fa fb k = int_lin_conv a b ↑k

theorem omega_is_prim_root {m : ℕ} (hm_pow2 : m.isPowerOfTwo) (hm_dvd : m ∣ mod64.toNat - 1) : IsPrimitiveRoot (↑primRoot.toNat ^ ((mod64.toNat - 1) / m)) m

ω = primRoot ^ ((p-1)/m) is a primitive m-th root of unity in ZMod p.

Apply IsPrimitiveRoot.pow_of_dvd to the primitive (p-1)-th root primRoot (prim_root_PRIM_ROOT) with divisor d = (p-1)/m; it yields a primitive ((p-1)/d)-th root, leaving three side goals: the order (p-1)/d = m, that d ≠ 0, and that d ∣ (p-1).

theorem m_gt_one_of_pow2_dvd {m : ℕ} (hm_dvd : m ∣ mod64.toNat - 1) (hm_ne : m ≠ 1) : 1 < m

theorem ntt_orthogonality (m : ℕ) (ω : ZMod mod32.toNat) (hω : IsPrimitiveRoot ω m) (c : ℕ) : ∑ j : Fin m, ω ^ (↑j * c) = if c % m = 0 then ↑m else 0

theorem mont_mul_zmod (a b : UInt32) (ha : a.toNat < mod32.toNat) (hb : b.toNat < mod32.toNat) : (montMul a b).toNat = (↑a.toNat * ↑b.toNat * (↑montR1.toNat)⁻¹).val

theorem prod_bound {m : ℕ} (FA FB : Vector UInt32 m) (hFA : (FA.all fun (x : UInt32) => decide (x < mod32)) = true) (hFB : (FB.all fun (x : UInt32) => decide (x < mod32)) = true) : ((Vector.map (fun (xy : UInt32 × UInt32) => montMul xy.1 xy.2) (FA.zip FB)).all fun (x : UInt32) => decide (x < mod32)) = true

theorem m_ne_zero_zmod (m : ℕ) (hm : 1 < m) (hm_dvd : m ∣ mod32.toNat - 1) : ↑m ≠ 0

theorem dft_convolution_theorem (m : ℕ) (hm : 1 < m) (ω : ZMod mod32.toNat) (hω : IsPrimitiveRoot ω m) (hm_dvd : m ∣ mod32.toNat - 1) (f g : Fin m → ZMod mod32.toNat) (k : Fin m) : (↑m)⁻¹ * ∑ j : Fin m, ((∑ i : Fin m, f i * ω ^ (↑i * ↑j)) * ∑ l : Fin m, g l * ω ^ (↑l * ↑j)) * ω⁻¹ ^ (↑j * ↑k) = ∑ i : Fin m, f i * g ⟨(↑k + m - ↑i) % m, ⋯⟩

theorem ntt_pipeline_computes_circ_conv {m : ℕ} (fa fb : Vector UInt32 m) (k : Fin m) (hm_pow2 : m.isPowerOfTwo) (hm_dvd : m ∣ mod64.toNat - 1) (hfa_bound : (fa.all fun (x : UInt32) => decide (x < mod32)) = true) (hfb_bound : (fb.all fun (x : UInt32) => decide (x < mod32)) = true) : have FA := nttInplace fa false (ensureRoots m); have FB := nttInplace fb false (ensureRoots m); have prod := Vector.map (fun (xy : UInt32 × UInt32) => montMul xy.1 xy.2) (FA.zip FB); have result := nttInplace prod true (ensureRoots m); result[k].toNat = vec_circ_conv fa fb k % mod32.toNat

theorem vec_circ_conv_lt_mod {n m : ℕ} (hm : 2 * n ≤ m) (hn : n < mod32.toNat) (fa fb : Vector UInt32 m) (k : Fin m) (hfa : ∀ (i : Fin m), (fa.get i).toNat ≤ 1 ∧ (n ≤ ↑i → (fa.get i).toNat = 0)) (hfb : ∀ (i : Fin m), (fb.get i).toNat ≤ 1) : vec_circ_conv fa fb k < mod32.toNat

theorem ntt_pipeline_eq_lin_conv {n : ℕ} (a b : BitVec n) (hn_mod : n < mod32.toNat) (hm_dvd : (2 * n).nextPowerOfTwo ∣ mod64.toNat - 1) : let m := (2 * n).nextPowerOfTwo; have roots := ensureRoots m; have fa := Vector.ofFn fun (i : Fin m) => if h : ↑i < n then if a.getLsb ⟨↑i, h⟩ = true then 1 else 0 else 0; have fb := Vector.ofFn fun (i : Fin m) => if h : ↑i < n then if b.getLsb ⟨↑i, h⟩ = true then 1 else 0 else 0; have FA := nttInplace fa false roots; have FB := nttInplace fb false roots; have result := nttInplace (Vector.map (fun (xy : UInt32 × UInt32) => montMul xy.1 xy.2) (FA.zip FB)) true roots; ∀ (k : Fin m), result[k].toNat = int_lin_conv a b ↑k

The NTT pipeline result at index k equals the integer linear convolution at k. Key insight: forward NTT converts inputs to Montgomery domain (× R); inverse NTT converts back (× R⁻¹), so the net Montgomery factor is 1 and results are plain integers. Also uses the NTT convolution theorem: pointwise product in frequency domain = circular convolution in time domain (= linear convolution here, due to zero-padding).

theorem bool_sum_eq_int_parity {n : ℕ} (a b : BitVec n) (i : Fin n) : ∑ j : Fin n, a[j] * b[i - j] = (int_circ_conv a b i % 2 == 1)

theorem uint32_sum_bit0 (u v : UInt32) : (u + v &&& 1 == 1) = ((u.toNat + v.toNat) % 2 == 1)

theorem circular_convolution_gf2_correct' {n : ℕ} (a b : BitVec n) (hn_mod : n < mod32.toNat) (hm_dvd : (2 * n).nextPowerOfTwo ∣ mod64.toNat - 1) : circularConvolutionGf2 a b = a.circConvolutionBruteforce b

Correctness theorem for NTT-based implementation.

theorem pow2_divides_MOD_sub_one (n : ℕ) (hn : n < 2 ^ 29) : (2 * n).nextPowerOfTwo ∣ mod64.toNat - 1