Additive NTT Correctness #
The stage-wise correctness argument and the final correctness theorem for the Additive NTT.
Running a state fold made only of state updates gives the same final state as the corresponding pure fold.
theorem
AdditiveNTT.bitsToU_bijective
{r : ℕ}
[NeZero r]
{L : Type}
[Field L]
[Fintype L]
[DecidableEq L]
{𝔽q : Type}
[Field 𝔽q]
[Fintype 𝔽q]
[hFq_card : Fact (Fintype.card 𝔽q = 2)]
[Algebra 𝔽q L]
(β : Fin r → L)
[hβ_lin_indep : Fact (LinearIndependent 𝔽q β)]
{ℓ R_rate : ℕ}
(i : Fin r)
:
Function.Bijective (bitsToU β i)
The bitsToU mapping is a bijection: showing that iterating bits corresponds
exactly to the linear span.
theorem
AdditiveNTT.evalWAt_eq_W
{r : ℕ}
[NeZero r]
{L : Type}
[Field L]
[Fintype L]
[DecidableEq L]
{𝔽q : Type}
[Field 𝔽q]
[Fintype 𝔽q]
[hFq_card : Fact (Fintype.card 𝔽q = 2)]
[Algebra 𝔽q L]
(β : Fin r → L)
[hβ_lin_indep : Fact (LinearIndependent 𝔽q β)]
{ℓ R_rate : ℕ}
(i : Fin r)
(x : L)
:
Prove that evalWAt equals the standard definition of W_i(x).
theorem
AdditiveNTT.evalNormalizedWAt_eq_normalizedW
{r : ℕ}
[NeZero r]
{L : Type}
[Field L]
[Fintype L]
[DecidableEq L]
{𝔽q : Type}
[Field 𝔽q]
[Fintype 𝔽q]
[hFq_card : Fact (Fintype.card 𝔽q = 2)]
[Algebra 𝔽q L]
(β : Fin r → L)
[hβ_lin_indep : Fact (LinearIndependent 𝔽q β)]
{ℓ R_rate : ℕ}
(i : Fin r)
(x : L)
:
Prove that evalNormalizedWAt equals the standard definition of Ŵ_i(x).
theorem
AdditiveNTT.computableTwiddleFactor_eq_twiddleFactor
{r : ℕ}
[NeZero r]
{L : Type}
[Field L]
[Fintype L]
[DecidableEq L]
{𝔽q : Type}
[Field 𝔽q]
[Fintype 𝔽q]
[hFq_card : Fact (Fintype.card 𝔽q = 2)]
[Algebra 𝔽q L]
(β : Fin r → L)
[hβ_lin_indep : Fact (LinearIndependent 𝔽q β)]
{ℓ R_rate : ℕ}
(h_ℓ_add_R_rate : ℓ + R_rate < r)
(i : Fin ℓ)
:
Prove that computableTwiddleFactor equals the standard definition of twiddleFactor.
theorem
AdditiveNTT.computableNTTStage_eq_NTTStage
{r : ℕ}
[NeZero r]
{L : Type}
[Field L]
[Fintype L]
[DecidableEq L]
{𝔽q : Type}
[Field 𝔽q]
[Fintype 𝔽q]
[hFq_card : Fact (Fintype.card 𝔽q = 2)]
[Algebra 𝔽q L]
(β : Fin r → L)
[hβ_lin_indep : Fact (LinearIndependent 𝔽q β)]
{ℓ R_rate : ℕ}
(h_ℓ_add_R_rate : ℓ + R_rate < r)
(i : Fin ℓ)
:
Prove that computableNTTStage equals the standard definition of NTTStage.
theorem
AdditiveNTT.W_eval_succ_eq_mul_add
{r : ℕ}
[NeZero r]
{L : Type}
[Field L]
[Fintype L]
[DecidableEq L]
{𝔽q : Type}
[Field 𝔽q]
[Fintype 𝔽q]
[hFq_card : Fact (Fintype.card 𝔽q = 2)]
[h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))]
[Algebra 𝔽q L]
(β : Fin r → L)
[hβ_lin_indep : Fact (LinearIndependent 𝔽q β)]
(i : Fin r)
(h_i_add_1 : ↑i + 1 < r)
(x : L)
:
Polynomial.eval x (W 𝔽q β (i + 1)) = Polynomial.eval x (W 𝔽q β i) * (Polynomial.eval x (W 𝔽q β i) + Polynomial.eval (β i) (W 𝔽q β i))
In the binary-field setting, the subspace vanishing polynomials satisfy the
runtime recurrence used by evalWAtCachedConstants.
theorem
AdditiveNTT.evalWAtCachedConstantsLoop_eq_W_of_correct
{r : ℕ}
[NeZero r]
{L : Type}
[Field L]
[Fintype L]
[DecidableEq L]
{𝔽q : Type}
[Field 𝔽q]
[Fintype 𝔽q]
[hFq_card : Fact (Fintype.card 𝔽q = 2)]
[h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))]
[Algebra 𝔽q L]
(β : Fin r → L)
[hβ_lin_indep : Fact (LinearIndependent 𝔽q β)]
(constants : Array L)
(i : Fin r)
(j : ℕ)
(x acc : L)
(hsize : constants.size = ↑i)
(hj_le : j ≤ ↑i)
(hj_lt_r : j < r)
(hacc : acc = Polynomial.eval x (W 𝔽q β ⟨j, hj_lt_r⟩))
(hcorrect : ∀ (k : ℕ), j ≤ k → ∀ (hki : k < ↑i), constants.getD k 0 = Polynomial.eval (β ⟨k, ⋯⟩) (W 𝔽q β ⟨k, ⋯⟩))
:
The cached evaluator computes W_i(x) when the cache stores exactly
W_k(β_k) for k < i. This is stated for the internal loop so later proofs can
resume from a partially consumed cache.
theorem
AdditiveNTT.evalWAtCachedConstants_eq_W_of_correct
{r : ℕ}
[NeZero r]
{L : Type}
[Field L]
[Fintype L]
[DecidableEq L]
{𝔽q : Type}
[Field 𝔽q]
[Fintype 𝔽q]
[hFq_card : Fact (Fintype.card 𝔽q = 2)]
[h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))]
[Algebra 𝔽q L]
(β : Fin r → L)
[hβ_lin_indep : Fact (LinearIndependent 𝔽q β)]
(constants : Array L)
(i : Fin r)
(x : L)
(hsize : constants.size = ↑i)
(hcorrect : ∀ (k : ℕ) (hki : k < ↑i), constants.getD k 0 = Polynomial.eval (β ⟨k, ⋯⟩) (W 𝔽q β ⟨k, ⋯⟩))
:
The cached evaluator computes W_i(x) from a complete cache for stage i.
theorem
AdditiveNTT.subspacePolynomialConstantsArrayLoop_spec
{r : ℕ}
[NeZero r]
{L : Type}
[Field L]
[Fintype L]
[DecidableEq L]
{𝔽q : Type}
[Field 𝔽q]
[Fintype 𝔽q]
[hFq_card : Fact (Fintype.card 𝔽q = 2)]
[h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))]
[Algebra 𝔽q L]
(β : Fin r → L)
[hβ_lin_indep : Fact (LinearIndependent 𝔽q β)]
{ℓ R_rate : ℕ}
(i : Fin r)
(k : ℕ)
(constants : Array L)
(hsize : constants.size = k)
(hk_le : k ≤ ↑i)
(hcorrect : ∀ (m : ℕ) (hmk : m < k), constants.getD m 0 = Polynomial.eval (β ⟨m, ⋯⟩) (W 𝔽q β ⟨m, ⋯⟩))
:
The constants-array builder preserves the invariant that entry k stores
W_k(β_k), and finishes with one entry for every k < i.
theorem
AdditiveNTT.subspacePolynomialConstantsArray_getD
{r : ℕ}
[NeZero r]
{L : Type}
[Field L]
[Fintype L]
[DecidableEq L]
{𝔽q : Type}
[Field 𝔽q]
[Fintype 𝔽q]
[hFq_card : Fact (Fintype.card 𝔽q = 2)]
[h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))]
[Algebra 𝔽q L]
(β : Fin r → L)
[hβ_lin_indep : Fact (LinearIndependent 𝔽q β)]
{ℓ R_rate : ℕ}
(i : Fin r)
(m : ℕ)
(hm : m < ↑i)
:
theorem
AdditiveNTT.evalWAtCachedConstants_subspacePolynomialConstantsArray_eq_W
{r : ℕ}
[NeZero r]
{L : Type}
[Field L]
[Fintype L]
[DecidableEq L]
{𝔽q : Type}
[Field 𝔽q]
[Fintype 𝔽q]
[hFq_card : Fact (Fintype.card 𝔽q = 2)]
[h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))]
[Algebra 𝔽q L]
(β : Fin r → L)
[hβ_lin_indep : Fact (LinearIndependent 𝔽q β)]
{ℓ R_rate : ℕ}
(i : Fin r)
(x : L)
:
theorem
AdditiveNTT.computableNormalizedWValuesArray_getD
{r : ℕ}
[NeZero r]
{L : Type}
[Field L]
[Fintype L]
[DecidableEq L]
{𝔽q : Type}
[Field 𝔽q]
[Fintype 𝔽q]
[hFq_card : Fact (Fintype.card 𝔽q = 2)]
[h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))]
[Algebra 𝔽q L]
(β : Fin r → L)
[hβ_lin_indep : Fact (LinearIndependent 𝔽q β)]
{ℓ R_rate : ℕ}
(h_ℓ_add_R_rate : ℓ + R_rate < r)
(i : Fin ℓ)
(k : Fin (ℓ + R_rate - ↑i - 1))
:
(computableNormalizedWValuesArray β h_ℓ_add_R_rate i).getD (↑k) 0 = Polynomial.eval (β ⟨↑i + 1 + ↑k, ⋯⟩) (normalizedW 𝔽q β ⟨↑i, ⋯⟩)
theorem
AdditiveNTT.computableTwiddleTableArray_getD
{r : ℕ}
[NeZero r]
{L : Type}
[Field L]
[Fintype L]
[DecidableEq L]
{𝔽q : Type}
[Field 𝔽q]
[Fintype 𝔽q]
[hFq_card : Fact (Fintype.card 𝔽q = 2)]
[h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))]
[Algebra 𝔽q L]
(β : Fin r → L)
[hβ_lin_indep : Fact (LinearIndependent 𝔽q β)]
{ℓ R_rate : ℕ}
(h_ℓ_add_R_rate : ℓ + R_rate < r)
(i : Fin ℓ)
(u : Fin (2 ^ (ℓ + R_rate - ↑i - 1)))
:
(computableTwiddleTableArray β h_ℓ_add_R_rate i).getD (↑u) 0 = twiddleFactor 𝔽q β h_ℓ_add_R_rate ⟨↑i, ⋯⟩ u
theorem
AdditiveNTT.computableNTTStageArray_eq_computableNTTStage
{r : ℕ}
[NeZero r]
{L : Type}
[Field L]
[Fintype L]
[DecidableEq L]
{𝔽q : Type}
[Field 𝔽q]
[Fintype 𝔽q]
[hFq_card : Fact (Fintype.card 𝔽q = 2)]
[h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))]
[Algebra 𝔽q L]
(β : Fin r → L)
[hβ_lin_indep : Fact (LinearIndependent 𝔽q β)]
{ℓ R_rate : ℕ}
(h_ℓ_add_R_rate : ℓ + R_rate < r)
(i : Fin ℓ)
(b : Array L)
:
arrayToFinFunction (2 ^ (ℓ + R_rate)) (computableNTTStageArray i (computableTwiddleTableArray β h_ℓ_add_R_rate i) b) = computableNTTStage β h_ℓ_add_R_rate ⟨↑i, ⋯⟩ (arrayToFinFunction (2 ^ (ℓ + R_rate)) b)
theorem
AdditiveNTT.computableAdditiveNTT_eq_additiveNTT
{r : ℕ}
[NeZero r]
{L : Type}
[Field L]
[Fintype L]
[DecidableEq L]
{𝔽q : Type}
[Field 𝔽q]
[Fintype 𝔽q]
[hFq_card : Fact (Fintype.card 𝔽q = 2)]
[Algebra 𝔽q L]
(β : Fin r → L)
[hβ_lin_indep : Fact (LinearIndependent 𝔽q β)]
{ℓ R_rate : ℕ}
(h_ℓ_add_R_rate : ℓ + R_rate < r)
(a : Fin (2 ^ ℓ) → L)
:
The proof-oriented computable additive NTT agrees with the abstract additive NTT specification.
theorem
AdditiveNTT.computableAdditiveNTTFastAction_run_eq_fold
{r : ℕ}
{L : Type}
[Field L]
(β : Fin r → L)
{ℓ R_rate : ℕ}
(h_ℓ_add_R_rate : ℓ + R_rate < r)
(a : Fin (2 ^ ℓ) → L)
:
(StateT.run (computableAdditiveNTTFastAction β h_ℓ_add_R_rate a) #[]).1 = Fin.foldl ℓ
(fun (current : Array L) (i : Fin ℓ) =>
have stage := ⟨ℓ - 1 - ↑i, ⋯⟩;
have twiddles := computableTwiddleTableArray β h_ℓ_add_R_rate stage;
computableNTTStageArray stage twiddles current)
(tileCoeffsArray R_rate a)
theorem
AdditiveNTT.computableAdditiveNTTFast_eq_computableAdditiveNTT
{r : ℕ}
[NeZero r]
{L : Type}
[Field L]
[Fintype L]
[DecidableEq L]
{𝔽q : Type}
[Field 𝔽q]
[Fintype 𝔽q]
[hFq_card : Fact (Fintype.card 𝔽q = 2)]
[h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))]
[Algebra 𝔽q L]
(β : Fin r → L)
[hβ_lin_indep : Fact (LinearIndependent 𝔽q β)]
{ℓ R_rate : ℕ}
(h_ℓ_add_R_rate : ℓ + R_rate < r)
(a : Fin (2 ^ ℓ) → L)
:
arrayToFinFunction (2 ^ (ℓ + R_rate)) (computableAdditiveNTTFast β h_ℓ_add_R_rate a) = computableAdditiveNTT β h_ℓ_add_R_rate a
The fast additive NTT array implementation is extensionally equal to the
proof-oriented computable implementation after converting its output array to a
Fin-indexed function.
This is the preferred proof boundary for the fast path: once this theorem is
proved, correctness against the abstract additive NTT specification follows from
computableAdditiveNTT_eq_additiveNTT.
theorem
AdditiveNTT.computableAdditiveNTTFast_eq_additiveNTT
{r : ℕ}
[NeZero r]
{L : Type}
[Field L]
[Fintype L]
[DecidableEq L]
{𝔽q : Type}
[Field 𝔽q]
[Fintype 𝔽q]
[hFq_card : Fact (Fintype.card 𝔽q = 2)]
[h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))]
[Algebra 𝔽q L]
(β : Fin r → L)
[hβ_lin_indep : Fact (LinearIndependent 𝔽q β)]
{ℓ R_rate : ℕ}
(h_ℓ_add_R_rate : ℓ + R_rate < r)
(a : Fin (2 ^ ℓ) → L)
:
arrayToFinFunction (2 ^ (ℓ + R_rate)) (computableAdditiveNTTFast β h_ℓ_add_R_rate a) = additiveNTT 𝔽q β h_ℓ_add_R_rate a
The fast additive NTT array implementation is correct against the abstract
additive NTT specification after converting its output array to a Fin-indexed
function.
theorem
AdditiveNTT.initial_tiled_coeffs_correctness
{r : ℕ}
[NeZero r]
{L : Type u}
[Field L]
[Fintype L]
[DecidableEq L]
(𝔽q : Type u)
[Field 𝔽q]
[Fintype 𝔽q]
[h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))]
[Algebra 𝔽q L]
(β : Fin r → L)
[hβ_lin_indep : Fact (LinearIndependent 𝔽q β)]
[h_β₀_eq_1 : Fact (β 0 = 1)]
{ℓ R_rate : ℕ}
(h_ℓ_add_R_rate : ℓ + R_rate < r)
(h_ℓ : ℓ ≤ r)
(a : Fin (2 ^ ℓ) → L)
:
have b := tileCoeffs a;
additiveNTTInvariant 𝔽q β h_ℓ_add_R_rate b a ⟨ℓ, ⋯⟩
theorem
AdditiveNTT.NTTStage_correctness
{r : ℕ}
[NeZero r]
{L : Type u}
[Field L]
[Fintype L]
[DecidableEq L]
(𝔽q : Type u)
[Field 𝔽q]
[Fintype 𝔽q]
[h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))]
[Algebra 𝔽q L]
(β : Fin r → L)
[hβ_lin_indep : Fact (LinearIndependent 𝔽q β)]
{ℓ R_rate : ℕ}
(h_ℓ_add_R_rate : ℓ + R_rate < r)
(i : Fin ℓ)
(input_buffer : Fin (2 ^ (ℓ + R_rate)) → L)
(original_coeffs : Fin (2 ^ ℓ) → L)
:
additiveNTTInvariant 𝔽q β h_ℓ_add_R_rate input_buffer original_coeffs ⟨↑i + 1, ⋯⟩ →
additiveNTTInvariant 𝔽q β h_ℓ_add_R_rate (NTTStage 𝔽q β h_ℓ_add_R_rate ⟨↑i, ⋯⟩ input_buffer) original_coeffs ⟨↑i, ⋯⟩
theorem
AdditiveNTT.foldl_NTTStage_inductive_aux
{r : ℕ}
[NeZero r]
{L : Type u}
[Field L]
[Fintype L]
[DecidableEq L]
(𝔽q : Type u)
[Field 𝔽q]
[Fintype 𝔽q]
[h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))]
[Algebra 𝔽q L]
(β : Fin r → L)
[hβ_lin_indep : Fact (LinearIndependent 𝔽q β)]
[h_β₀_eq_1 : Fact (β 0 = 1)]
{ℓ R_rate : ℕ}
(h_ℓ_add_R_rate : ℓ + R_rate < r)
(h_ℓ : ℓ ≤ r)
(k : Fin (ℓ + 1))
(original_coeffs : Fin (2 ^ ℓ) → L)
:
theorem
AdditiveNTT.additiveNTT_correctness
{r : ℕ}
[NeZero r]
{L : Type u}
[Field L]
[Fintype L]
[DecidableEq L]
(𝔽q : Type u)
[Field 𝔽q]
[Fintype 𝔽q]
[h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))]
[Algebra 𝔽q L]
(β : Fin r → L)
[hβ_lin_indep : Fact (LinearIndependent 𝔽q β)]
[h_β₀_eq_1 : Fact (β 0 = 1)]
{ℓ R_rate : ℕ}
(h_ℓ_add_R_rate : ℓ + R_rate < r)
(h_ℓ : ℓ ≤ r)
(original_coeffs : Fin (2 ^ ℓ) → L)
(output_buffer : Fin (2 ^ (ℓ + R_rate)) → L)
(h_alg : output_buffer = additiveNTT 𝔽q β h_ℓ_add_R_rate original_coeffs)
:
have P := polynomialFromNovelCoeffs 𝔽q β ℓ h_ℓ original_coeffs;
∀ (j : Fin (2 ^ (ℓ + R_rate))), output_buffer j = Polynomial.eval (evaluationPointω 𝔽q β h_ℓ_add_R_rate ⟨0, ⋯⟩ j) P