Executable additive NTT algorithms

Generic function-backed and array-backed additive NTT implementations over a finite field, with an explicitly supplied binary-subfield algebra and independent basis vectors. The function-backed transform mirrors the abstract stages; the array-backed transform caches subspace-polynomial constants and twiddle tables.

CompPoly.Fields.Binary.AdditiveNTT.Correctness relates these implementations to the abstract algorithm and its evaluation specification. Concrete tower instances and the compatibility entry point remain in CompPoly.Fields.Binary.AdditiveNTT.Impl.

The coefficient tiling, twiddle factors, and descending butterfly stages follow the Lin–Chung–Han additive NTT presentation in [DP24], Algorithm 2. The array-backed path caches quantities used by these same stages.

References

• Diamond, B. E. and Posen, J., Polylogarithmic proofs for multilinears over binary towers

def AdditiveNTT.Array.toFinVec {α : Type u_1} (n : ℕ) (arr : Array α) (h : arr.size = n) : Fin n → α

Read an array of length n as a function on Fin n.

def AdditiveNTT.arrayToFinFunction {α : Type u_1} [Zero α] (n : ℕ) (arr : Array α) : Fin n → α

Converts an array to a Fin n function, using 0 for missing entries.

theorem AdditiveNTT.List.prod_finRange_eq_finset_prod {M : Type u_1} [CommMonoid M] {n : ℕ} (f : Fin n → M) : (List.map f (List.finRange n)).prod = ∏ i : Fin n, f i

The product of a function over the list of finite indices equals its finite product.

def AdditiveNTT.bitsToU {r : ℕ} [NeZero r] {L : Type} [Field L] {𝔽q : Type} [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) {ℓ R_rate : ℕ} (i : Fin r) (k : Fin (2 ^ ↑i)) : ↥(U 𝔽q β i)

Map the numeric mask k to the sum of the first i basis vectors selected by its bits, as an element of their linear span.

def AdditiveNTT.getUElements {r : ℕ} {L : Type} [Field L] (β : Fin r → L) {ℓ R_rate : ℕ} (i : Fin r) : List L

Computes the elements of the subspace: U_i = span({β_0, ..., β_{i-1}}).

def AdditiveNTT.evalWAt {r : ℕ} {L : Type} [Field L] (β : Fin r → L) {ℓ R_rate : ℕ} (i : Fin r) (x : L) : L

Evaluates the subspace vanishing polynomial W_i(x) = ∏_{u ∈ U_i} (x - u).

def AdditiveNTT.evalNormalizedWAt {r : ℕ} {L : Type} [Field L] (β : Fin r → L) {ℓ R_rate : ℕ} (i : Fin r) (x : L) : L

Evaluates the normalized subspace vanishing polynomial Ŵ_i(x) = W_i(x) / W_i(β_i).

def AdditiveNTT.computableTwiddleFactor {r : ℕ} {L : Type} [Field L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin ℓ) (u : Fin (2 ^ (ℓ + R_rate - ↑i - 1))) : L

Compute the stage-i twiddle factor by summing normalized subspace-polynomial evaluations selected by the bits of u.

def AdditiveNTT.computableNTTStage {r : ℕ} {L : Type} [Field L] {𝔽q : Type} [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) [Fact (LinearIndependent 𝔽q β)] (i : Fin ℓ) (b : Fin (2 ^ (ℓ + R_rate)) → L) : Fin (2 ^ (ℓ + R_rate)) → L

Perform stage i on the coefficient buffer b, pairing entries whose indices differ in bit i and applying the corresponding twiddle factor.

def AdditiveNTT.computableAdditiveNTT {r : ℕ} {L : Type} [Field L] {𝔽q : Type} [Field 𝔽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) : Fin (2 ^ (ℓ + R_rate)) → L

Transform 2 ^ ℓ novel-basis coefficients into 2 ^ (ℓ + R_rate) values by first tiling the coefficients and then applying stages ℓ - 1 down to 0. The basis has length r, and ℓ + R_rate < r bounds the evaluation domain.

def AdditiveNTT.tileCoeffsArray {L : Type} {ℓ : ℕ} (R_rate : ℕ) (a : Fin (2 ^ ℓ) → L) : Array L

Array-backed coefficient tiling for the fast additive NTT path.

@[irreducible]

def AdditiveNTT.evalWAtCachedConstantsLoop {L : Type} [Field L] (constants : Array L) (j : ℕ) (acc : L) : L

Starting from acc, iterate acc ↦ acc * (acc + constants[k]) for indices k from j to constants.size - 1. Return acc unchanged when constants.size ≤ j.

For j ≤ constants.size, if the initial accumulator is W_j(x) and the remaining constants are W_k(β_k), the result is W_{constants.size}(x).

def AdditiveNTT.evalWAtCachedConstants {L : Type} [Field L] (constants : Array L) (x : L) : L

Evaluate a subspace polynomial using cached constants W_k(β_k).

Starting from W_0(x) = x, each cached constant advances the recurrence W_{k+1}(x) = W_k(x) * (W_k(x) + W_k(β_k)).

@[irreducible]

def AdditiveNTT.subspacePolynomialConstantsArrayLoop {r : ℕ} {L : Type} [Field L] (β : Fin r → L) {ℓ R_rate : ℕ} (i : Fin r) (k : ℕ) (constants : Array L) : Array L

Extend the supplied constants array, starting at index k and stopping before i. Each step evaluates the polynomial recurrence encoded by the current array at β_k and appends the result. Return the array unchanged when i ≤ k.

If the supplied array has length k and entry j is W_j(β_j) for every j < k, each appended entry has the same interpretation at its index.

def AdditiveNTT.subspacePolynomialConstantsArray {r : ℕ} {L : Type} [Field L] (β : Fin r → L) {ℓ R_rate : ℕ} (i : Fin r) : Array L

Precompute the constants W_k(β_k) needed by the recursive subspace polynomial evaluator up to stage i.

def AdditiveNTT.computableNormalizedWValuesArray {r : ℕ} {L : Type} [Field L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin ℓ) : Array L

Precompute normalized vanishing evaluations used by one stage's twiddle factors.

def AdditiveNTT.computableTwiddleTableArray {r : ℕ} {L : Type} [Field L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin ℓ) : Array L

Precompute all twiddle factors for one additive NTT stage.

The table entry for u is the subset sum of the cached normalized values selected by the set bits of u.

def AdditiveNTT.computableNTTStageArray {L : Type} [Field L] {ℓ R_rate : ℕ} (i : Fin ℓ) (twiddles b : Array L) : Array L

Array update for one additive NTT stage.

The twiddles array is intended to store the values of computableTwiddleFactor for this stage, indexed by u. Missing entries in either input array are read as zero.

def AdditiveNTT.computableAdditiveNTTFastStages {r : ℕ} {L : Type} [Field L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) : StateM (Array L) Unit

Fast additive NTT stage driver over an Array L state.

The state is expected to contain the initialized output buffer. Each stage updates that buffer using the array transition from computableNTTStageArray.

def AdditiveNTT.computableAdditiveNTTFastAction {r : ℕ} {L : Type} [Field L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (a : Fin (2 ^ ℓ) → L) : StateM (Array L) (Array L)

Fast additive NTT array producer as a state action.

def AdditiveNTT.computableAdditiveNTTFast {r : ℕ} {L : Type} [Field L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (a : Fin (2 ^ ℓ) → L) : Array L

Fast additive NTT array producer.