Additive NTT Algorithm

Core Additive NTT data flow: evaluation points, twiddle factors, stage/update definitions, coefficient tiling, and the stage invariant.

2. The Additive NTT Algorithm and Correctness

This section describes the construction of the evaluation points, the tiling of coefficients, the main loop invariant, and the final correctness theorem for the Additive NTT algorithm.

noncomputable def AdditiveNTT.evaluationPointω {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i ≤ ℓ) (x : Fin (2 ^ (ℓ + R_rate - ↑i))) : L

Constructs an evaluation point in sDomain i from its Nat.getBit representation.

The index is loose (i : Fin r); h_i records that it is an Additive-NTT level.

noncomputable def AdditiveNTT.twiddleFactor {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i < ℓ) (u : Fin (2 ^ (ℓ + R_rate - ↑i - 1))) : L

The twiddle factor at a strict NTT stage i.

It is the evaluation point with the stage bit set to zero, i.e. the x₀ term of the butterfly identity.

theorem AdditiveNTT.evaluationPointω_eq_twiddleFactor_of_div_2 {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i < ℓ) (x : Fin (2 ^ (ℓ + R_rate - ↑i))) : evaluationPointω 𝔽q β h_ℓ_add_R_rate i ⋯ x = twiddleFactor 𝔽q β h_ℓ_add_R_rate i h_i ⟨↑x / 2, ⋯⟩ + ↑(↑x % 2) * Polynomial.eval (β ⟨↑i, ⋯⟩) (normalizedW 𝔽q β ⟨↑i, ⋯⟩)

theorem AdditiveNTT.eval_point_ω_eq_next_twiddleFactor_comp_qmap {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 r) (h_i : ↑i < ℓ) (x : Fin (2 ^ (ℓ + R_rate - (↑i + 1)))) : evaluationPointω 𝔽q β h_ℓ_add_R_rate ⟨↑i + 1, ⋯⟩ ⋯ x = Polynomial.eval (twiddleFactor 𝔽q β h_ℓ_add_R_rate i h_i ⟨↑x, ⋯⟩) (qMap 𝔽q β ⟨↑i, ⋯⟩ ⋯)

def AdditiveNTT.tileCoeffs {L : Type u} {ℓ R_rate : ℕ} (a : Fin (2 ^ ℓ) → L) : Fin (2 ^ (ℓ + R_rate)) → L

The 2^R_rate-fold tiling of coefficients a into the initial buffer b. b(v) = aⱼ, where j are the ℓ LSBs of v.

noncomputable def AdditiveNTT.NTTStage {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i < ℓ) (b : Fin (2 ^ (ℓ + R_rate)) → L) : Fin (2 ^ (ℓ + R_rate)) → L

A single Additive-NTT stage.

i : Fin r is a loose index, while h_i : i < ℓ restricts it to a stage of the for i from ℓ - 1 down to 0 loop.

noncomputable def AdditiveNTT.additiveNTT {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (a : Fin (2 ^ ℓ) → L) : Fin (2 ^ (ℓ + R_rate)) → L

The Additive NTT Algorithm (Algorithm 2)

Computes the Additive NTT on a given set of coefficients from the novel basis.

• a: The initial coefficient array (a₀, ..., a_{2^ℓ-1}).

def AdditiveNTT.coeffsBySuffix {r : ℕ} {L : Type u} {ℓ R_rate : ℕ} (a : Fin (2 ^ ℓ) → L) (i : Fin r) (h_i : ↑i ≤ ℓ) (v : Fin (2 ^ ↑i)) : Fin (2 ^ (ℓ - ↑i)) → L

The coefficients of the level-i polynomial selected by the low-bit suffix v.

The loose index i : Fin r is constrained by h_i : i ≤ ℓ; at i = ℓ this is the initially tiled buffer.

theorem AdditiveNTT.base_coeffsBySuffix {r : ℕ} [NeZero r] {L : Type u} {ℓ R_rate : ℕ} (a : Fin (2 ^ ℓ) → L) : coeffsBySuffix a 0 ⋯ 0 = a

theorem AdditiveNTT.evenRefinement_eq_novel_poly_of_0_leading_suffix {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i < ℓ) (v : Fin (2 ^ ↑i)) (original_coeffs : Fin (2 ^ ℓ) → L) : have h_v := ⋯; evenRefinement 𝔽q β h_ℓ_add_R_rate i h_i (coeffsBySuffix original_coeffs i ⋯ v) = intermediateEvaluationPoly 𝔽q β h_ℓ_add_R_rate ⟨↑i + 1, ⋯⟩ ⋯ (coeffsBySuffix original_coeffs ⟨↑i + 1, ⋯⟩ ⋯ ⟨↑v, h_v⟩)

P₀, ₍ᵥ₎⁽ⁱ⁺¹⁾(X) = P₍₀ᵥ₎⁽ⁱ⁺¹⁾(X), where v consists of exactly i bits Note that the even refinement P₀, ₍ᵥ₎⁽ⁱ⁺¹⁾(X) is constructed from the view of stage i, while the novel polynomial P₍₀ᵥ₎⁽ⁱ⁺¹⁾(X) is constructed from the view of stage i+1.

theorem AdditiveNTT.oddRefinement_eq_novel_poly_of_1_leading_suffix {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i < ℓ) (v : Fin (2 ^ ↑i)) (original_coeffs : Fin (2 ^ ℓ) → L) : have h_v := ⋯; oddRefinement 𝔽q β h_ℓ_add_R_rate i h_i (coeffsBySuffix original_coeffs i ⋯ v) = intermediateEvaluationPoly 𝔽q β h_ℓ_add_R_rate ⟨↑i + 1, ⋯⟩ ⋯ (coeffsBySuffix original_coeffs ⟨↑i + 1, ⋯⟩ ⋯ ⟨↑v ||| 1 <<< ↑i, h_v⟩)

P₁, ₍ᵥ₎⁽ⁱ⁺¹⁾(X) = P₍₁ᵥ₎⁽ⁱ⁺¹⁾(X), where v consists of exactly i bits Note that the odd refinement P₁,₍ᵥ₎⁽ⁱ⁺¹⁾(X) is constructed from the view of stage i, while the novel polynomial P₍₁ᵥ₎⁽ⁱ⁺¹⁾(X) is constructed from the view of stage i+1.

def AdditiveNTT.additiveNTTInvariant {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (evaluation_buffer : Fin (2 ^ (ℓ + R_rate)) → L) (original_coeffs : Fin (2 ^ ℓ) → L) (i : Fin r) (h_i : ↑i ≤ ℓ) : Prop

The main loop invariant for the additiveNTT algorithm: the evaluation buffer b at the end of level i (i ∈ {0, ..., ℓ}, i=ℓ means the initial tiled buffer) holds the value P⁽ⁱ⁾(ω_{u, b, i}) for all Nat.getBit mask index (u||b||v) ∈ {0, ..., 2^(ℓ+R_rate)-1}, where the points ω_{u, b, i} are in the domain S⁽ⁱ⁾.

Main statement: After round i ∈ {ℓ-1, ℓ-2, ..., 0}: the buffer b at index j (which can be decomposed as j = (u || b || v) in little-endian order, where

• u is a bitstring of length ℓ + R_rate - i - 1,
• b is a single Nat.getBit (the LSB of the high bits),
• v is a bitstring of length i (the LSBs), holds the value P⁽ⁱ⁾(ω_{u, b, i}), where:
  • P⁽ⁱ⁾ is the intermediate polynomial at round i (in the novel basis),
  • ω_{u, b, i} is the evaluation point in the subspace S⁽ⁱ⁾ constructed as a linear combination of the basis elements of S⁽ⁱ⁾:
    • the Nat.getBit b is the coefficient for Ŵᵢ(βᵢ) (the LSB),
    • the LSB of u is the coefficient for Ŵᵢ(β_{i+1}), ..., the MSB of u is the coefficient for Ŵᵢ(β_{ℓ+R_rate-1}).
  • The value is replicated 2^i times for each v (i.e., the last i bits do not affect the value).

More precisely, for all j : Fin (2^(ℓ + R_rate)), let u_b_v := j.val (as a natural number),

• let v := u_b_v % 2^i (the i LSBs),
• let u_b := u_b_v / 2^i (the high bits),
• let b := u_b % 2 (the LSB of the high bits),
• let u := u_b / 2 (the remaining high bits), then: b j = P⁽ⁱ⁾(ω_{u, b, i})