Additive NTT Implementation

Concrete implementation of the Additive NTT algorithm.

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

Converts an Array to a Fin function of a specific size 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

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)

Define the mapping explicitly from the index k to the Submodule U.

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

Computes the twiddle factor used in the butterfly operation. Corresponds to AdditiveNTT.twiddleFactor.

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

Performs one stage of the Additive NTT. This corresponds to NTTStage in the abstract definition: b is the array of coefficients. i is the stage index (0 to r-1).

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

The main computable Additive NTT function. a is the input array of coefficients. r is the number of stages (dimension of the domain). The input array size must be at least 2^r.

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

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)).

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

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

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 stores the values of computableTwiddleFactor for this stage, indexed by u.

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.

instance AdditiveNTT.instNeZeroHPowNatOfNat_compPoly (k : ℕ) : NeZero (2 ^ k)

def AdditiveNTT.computableBasisExplicit (k : ℕ) (i : Fin (2 ^ k)) : ConcreteBinaryTower.ConcreteBTField k

Computable basis for ConcreteBTField k over ConcreteBTField 0. This is the explicit product of Z's.

theorem AdditiveNTT.hβ_lin_indep_concrete (k : ℕ) : LinearIndependent (ConcreteBinaryTower.ConcreteBTField 0) (computableBasisExplicit k)

@[reducible, inline]

abbrev AdditiveNTT.BTF₃ : Type

instance AdditiveNTT.instNeZeroHPowOfNat_compPoly : NeZero (2 ^ 3)

@[implicit_reducible]

instance AdditiveNTT.instFieldBTF₃ : Field BTF₃

@[implicit_reducible]

instance AdditiveNTT.instDecidableEqBTF₃ : DecidableEq BTF₃

@[implicit_reducible]

instance AdditiveNTT.instFintypeBTF₃ : Fintype BTF₃

def AdditiveNTT.testNTTBTF₃ : Fin (2 ^ (2 + 2)) → BTF₃

Test of the computable additive NTT over BTF₃ (an 8-bit binary tower field BTF₃). Input polynomial: p(x) = x (novel coefficients [7, 1, 0, 0]) of size 2^ℓ in BTF₃

• ℓ = 2
• R_rate = 2: Repetition rate, evaluating at S₀ of size 2^(ℓ + R_rate) = 16 points
• r = 2^3 = 8: Dimension of the basis for BTF₃ over GF(2) Output: A function Fin 16 → BTF₃ giving the evaluations of p(x) = x at 16 points in the evaluation domain S₀ defined by the spanning basis elements {β₀, ..., β_{ℓ + 𝓡 - 1}} of BTF₃ over GF(2).