Additive NTT Algorithm (Algorithm 2, LCH14) #
This file defines the FRI-Binius ([DP24]) variant of the Additive NTT algorithm originally introduced in [LCH14]. This variant adopts concrete optimizations and a different proof strategy, making it highly suitable for the FRI-Binius proof system, while still fully complying with the original algorithm in [LCH14] through a different interpretation.
Main Definitions #
sDomain: The intermediate evaluation domainS⁽ⁱ⁾for the roundiin the Additive NTT algorithmqMap: The quotient mapq⁽ⁱ⁾(X)that relates successive domainsintermediateNormVpoly: Thei-th order subspace vanishing polynomialsŴₖ⁽ⁱ⁾over domainS⁽ⁱ⁾intermediateNovelBasisX: The intermediate novel basisXⱼ⁽ⁱ⁾for the roundiin the Additive NTT algorithmintermediateEvaluationPoly: The intermediate evaluation polynomialP⁽ⁱ⁾(X)for the roundiin the Additive NTT algorithmadditiveNTT: The main implementation of the Additive NTT encoding algorithm.NTTStage: The main implementation of each NTT stage in the Additive NTT encoding algorithm.additiveNTT_correctness: Main correctness statement of the encoding algorithm.additiveNTTInvariant: Describes the invariant for each loop in the algorithm, which states whether the result of an encoding round is correctNTTStage_correctness: Main correctness statement of each NTT stage in the encoding algorithm, this proves that if the previous round satisfies the invariant, then the current round also
References #
- [Diamond, B.E. and Posen, J., Polylogarithmic proofs for multilinears over binary towers][DP24]
- [Lin, S., Chung, W., and Han, Y.S., Novel polynomial basis and its application to reed-solomon erasure codes][LCH14]
- [Von zur Gathen, J. and Gerhard, J., Arithmetic and factorization of polynomial over F2 (extended abstract)][GGJ96]
TODOs #
- Define computable additive NTT and transfer correctness proof to it
1. Intermediate Structures: Domains, Maps, and Bases #
This section defines the intermediate evaluation domains, quotient maps, and the structure of the subspace vanishing polynomials and their bases. These are the core algebraic objects underlying the Additive NTT algorithm.
The intermediate evaluation domain S⁽ⁱ⁾, defined as the image of the full evaluation space
under the normalized subspace vanishing polynomial Ŵᵢ(X).
∀ i ∈ {0, ..., r-1}, we define Uᵢ:= <β₀, ..., βᵢ₋₁>_{𝔽q}, note that Uᵣ is not used.
∀ i ∈ {0, ..., r-1}, S⁽ⁱ⁾ is the image of the subspace U_{ℓ+R}
under the 𝔽q-linear map x ↦ Ŵᵢ(x).
Equations
Instances For
The quotient map q⁽ⁱ⁾(X) that relates successive domains.
q⁽ⁱ⁾(X) := (Wᵢ(βᵢ)^q / Wᵢ₊₁(βᵢ₊₁)) * ∏_{c ∈ 𝔽q} (X - c). Usable range is ∀ i ∈ {0, ..., r-2}
Equations
Instances For
Lemma 4.2. The quotient maps compose with the Ŵ polynomials.
q⁽ⁱ⁾ ∘ Ŵᵢ = Ŵᵢ₊₁, ∀ i ∈ {0, ..., r-2}.
The evaluation of the quotient map q⁽ⁱ⁾(X) is an 𝔽q-linear map.
Usable range is ∀ i ∈ {0, ..., r-2}.
Theorem 4.3. The quotient map q⁽ⁱ⁾ maps the domain S⁽ⁱ⁾ to S⁽ⁱ⁺¹⁾.
Usable range is ∀ i ∈ {0, ..., r-2}.
Prove the equality between the recursive definition
of qCompositionChain and the Fin.foldl form.
Corollary 4.4. For each i ∈ {0, ..., r-1}, we have Ŵᵢ = q⁽ⁱ⁻¹⁾ ∘ ... ∘ q⁽⁰⁾
(with the convention that for i = 0, this is just X).
The vectors y_j^{(i)} = Ŵᵢ(β_j) for j ∈ {i, ..., ℓ+R-1}.
Equations
Instances For
The vectors sDomainBasisVectors are indeed elements of the subspace sDomain,
∀ i ∈ {0, ..., r-1}.
S⁽ⁱ⁾ is the image over Wᵢ(X) of the the subspace spanned by {βᵢ, ..., β_{ℓ+R-1}}.
Usable range is ∀ i ∈ {0, ..., ℓ+R-1}.
Corollary 4.5. The set {Ŵᵢ(βᵢ), ..., Ŵᵢ(β_{ℓ+R-1})} is an 𝔽q-basis for S⁽ⁱ⁾.
Equations
Instances For
Equations
Domain-Index Bijections #
Bijections between elements in S^(i) and Fin (2^(ℓ + R_rate - i)) for use in
Binary Basefold protocol implementations.
Equations
Instances For
Convert an element of S^(i) to its index in Fin (2^(ℓ + R_rate - i)).
This uses the basis representation of elements in the domain.
This requires 𝔽q = 𝔽₂ for the bijection to work.
Equations
Instances For
Convert an index in Fin (2 ^ (ℓ + R_rate - i)) to an element of S^(i).
This is the inverse of sDomainToFin.
Equations
Instances For
The bijection between S^(i) and Fin (2^(ℓ + R_rate - i)).
This requires 𝔽q = 𝔽₂ for the bijection to work properly.
Equations
Instances For
2. Intermediate Novel Polynomial Bases Xⱼ⁽ⁱ⁾ and evaluation polynomials P⁽ⁱ⁾ #
∀ i ∈ {0, ..., ℓ}, The i-th order subspace vanishing polynomials Ŵₖ⁽ⁱ⁾,
Ŵₖ⁽ⁱ⁾ := q⁽ⁱ⁺ᵏ⁻¹⁾ ∘ ⋯ ∘ q⁽ⁱ⁾ for k ∈ {1, ..., ℓ - i -1}, and X for k = 0.
-- k ∈ {0, ..., ℓ-i-1}. Note that when i = ℓ, k ∈ Fin 0 does not exists.
Equations
Instances For
Iterated quotient map W_k⁽ⁱ⁾: Maps a point from S⁽ⁱ⁾ to S⁽ⁱ⁺ᵏ⁾ by evaluating
the intermediate norm vanishing polynomial at that point. This one mainly proves that
the intermediateNormVpoly works with points in the restricted sDomains,
instead of the whole field L.
Equations
Instances For
The evaluation of qMap on an element from sDomain i belongs to sDomain (i+1). This is a key property that qMap maps between successive domains.
When k = 1, iteratedQuotientMap reduces to evaluating qMap directly. This shows that iteratedQuotientMap with k = 1 is equivalent to the single-step quotient map.
Lifts a point y from a higher-indexed domain sDomain j to the canonical
base point of its fiber in a lower-indexed domain sDomain i,
by retaining all coeffs for the corresponding basis elements
Equations
Instances For
Applying the forward map to a lifted point returns the original point.
∀ i ∈ {0, ..., ℓ}, The i-th order novel polynomial basis Xⱼ⁽ⁱ⁾.
Xⱼ⁽ⁱ⁾ := Π_{k=0}^{ℓ-i-1} (Ŵₖ⁽ⁱ⁾)^{jₖ}, ∀ j ∈ {0, ..., 2^(ℓ-i)-1}
Equations
Instances For
X₂ⱼ⁽ⁱ⁾ = Xⱼ⁽ⁱ⁺¹⁾(q⁽ⁱ⁾(X)) ∀ j ∈ {0, ..., 2^(ℓ-i)-1}, ∀ i ∈ {0, ..., ℓ-1}
X₂ⱼ₊₁⁽ⁱ⁾ = X * (Xⱼ⁽ⁱ⁺¹⁾(q⁽ⁱ⁾(X))) ∀ j ∈ {0, ..., 2^(ℓ-i)-1}, ∀ i ∈ {0, ..., ℓ-1}
∀ i ∈ {0, ..., ℓ}, The i-th order evaluation polynomial
P⁽ⁱ⁾(X) := ∑_{j=0}^{2^(ℓ-i)-1} coeffsⱼ ⋅ Xⱼ⁽ⁱ⁾(X) over the domain S⁽ⁱ⁾.
where the polynomial P⁽⁰⁾(X) over the domain S⁽⁰⁾ is exactly the original
polynomial P(X) we need to evaluate,
and coeffs is the list of 2^(ℓ-i) coefficients of the polynomial.
Equations
Instances For
The even and odd refinements of P⁽ⁱ⁾(X) which are polynomials in the (i+1)-th basis.
P₀⁽ⁱ⁺¹⁾(Y) = ∑_{j=0}^{2^{ℓ-i-1}-1} a_{2j} ⋅ Xⱼ⁽ⁱ⁺¹⁾(Y)
P₁⁽ⁱ⁺¹⁾(Y) = ∑_{j=0}^{2^{ℓ-i-1}-1} a_{2j+1} ⋅ Xⱼ⁽ⁱ⁺¹⁾(Y)
Equations
Instances For
Key Polynomial Identity (Equation 39). This identity is the foundation for the
butterfly operation in the Additive NTT. It relates a polynomial in the i-th basis to
its even and odd parts expressed in the (i+1)-th basis via the quotient map q⁽ⁱ⁾.
∀ i ∈ {0, ..., ℓ-1}, P⁽ⁱ⁾(X) = P₀⁽ⁱ⁺¹⁾(q⁽ⁱ⁾(X)) + X ⋅ P₁⁽ⁱ⁺¹⁾(q⁽ⁱ⁾(X))
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.
Constructs an evaluation point ω in the domain S⁽ⁱ⁾ from a Nat.getBit representation.
This uses the 𝔽q-basis of S⁽ⁱ⁾ from sDomain_basis.
ω_{u,b,i} = b⋅Ŵᵢ(βᵢ) + ∑_{k=0}^{|u|-1} uₖ ⋅ Ŵᵢ(β_{i+1+k})
where (u,b) is a Nat.getBit string of length ℓ + R - i.
Computes the twiddle factor t for a given stage i and high-order bits u.
t := Σ_{k=0}^{ℓ+R-i-1} u_k ⋅ Ŵᵢ(β_{i+k}).
This corresponds to the x₀ term in the recursive butterfly identity.
Equations
Instances For
A single stage of the Additive NTT for a given i.
It takes the buffer b from the previous stage and applies the butterfly operations.
This function implements one step of the for i from ℓ-1 down to 0 loop.
Equations
Instances For
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}).
Equations
Instances For
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.
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.
The main loop invariant for the additiveNTT algorithm: the evaluation buffer b
at the end of stage i (i ∈ {0, ..., ℓ}, i=ℓ means the initial tiled buffer)
holds the value P⁽ⁱ⁾(ω_{u, b, v}) for all Nat.getBit mask index
(u||b||v) ∈ {0, ..., 2^(ℓ+R_rate)-1}, where the points ω_{u, b, v} 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
uis a bitstring of lengthℓ + R_rate - i - 1,bis a single Nat.getBit (the LSB of the high bits),vis a bitstring of lengthi(the LSBs), holds the valueP⁽ⁱ⁾(ω_{u, b, i}), where:P⁽ⁱ⁾is the intermediate polynomial at roundi(in the novel basis),ω_{u, b, i}is the evaluation point in the subspaceS⁽ⁱ⁾constructed as a linear combination of the basis elements ofS⁽ⁱ⁾:- the Nat.getBit
bis the coefficient forŴᵢ(βᵢ)(the LSB), - the LSB of
uis the coefficient forŴᵢ(β_{i+1}), ..., the MSB ofuis the coefficient forŴᵢ(β_{ℓ+R_rate-1}).
- the Nat.getBit
- The value is replicated
2^itimes for eachv(i.e., the lastibits 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(theiLSBs), - 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})
Equations
Instances For
The correctness theorem for the NTTStage function. This is the inductive step
in the main proof. It asserts that if the invariant holds for i+1, then after
applying NTTStage i, the invariant holds for i ∈ {0, ..., ℓ-1}.
Main Correctness Theorem for Additive NTT
If b is the output of additiveNTT on input a, then for all j, b j
is the evaluation of the polynomial P (from the novel basis coefficients a)
at the evaluation point ω_{0, j} in the domain S⁰.