Dependencies

The DoNothing reduction satisfies perfect completeness for any input relation.

The SendWitness reduction satisfies perfect completeness.

The SendSingleWitness oracle reduction satisfies perfect completeness.

The RandomQuery oracle reduction satisfies perfect completeness: if two oracles are equal, they will agree on any random query.

If the oracle type has distance bound \(d\), then the RandomQuery oracle reduction satisfies round-by-round knowledge soundness with error probability \(\frac{d}{|\mathsf{Query}|}\).

The polynomial equality testing reduction satisfies perfect completeness: if \(P = Q\) as polynomials, then \(P(r) = Q(r)\) for any field element \(r\).

The polynomial equality testing reduction satisfies round-by-round knowledge soundness with error probability \(\frac{d}{|\mathbb {F}|}\), where \(d\) is the maximum degree bound. This follows from the Schwartz-Zippel lemma: distinct polynomials of degree at most \(d\) can agree on at most \(d\) points.

The batching polynomial evaluation reduction satisfies perfect completeness.

The SendClaim oracle reduction satisfies perfect completeness when the input relation matches the oracle computation requirement.

The ReduceClaim reduction satisfies perfect completeness when the relation condition holds.

The CheckClaim reduction satisfies perfect completeness.

The CheckClaim oracle reduction satisfies perfect completeness.

Let \(\mathcal{C}:= \mathrm{RS}[\mathbb {F}, \mathcal{L}, m]\) be a Reed Solomon code with rate \(\rho \). The function \(\mathsf{Gen}(\mathsf{par}\ell ; \alpha ) = (1, \alpha , \ldots , \alpha ^{\mathsf{par}\ell - 1})\) is a proximity generator for \(\mathcal{C}\) with mutual correlated agreement with proximity bound \({\mathsf{B}}^\star (\mathcal{C}, \mathsf{par}\ell ) := \frac{1 + \rho }{2}\) and error \(\mathsf{err}^\star (\mathcal{C}, \mathsf{par}\ell , \delta ) = \frac{(\mathsf{par}\ell - 1) \cdot 2^m}{\rho \cdot |\mathbb {F}|}\).

The function \(\mathsf{Gen}(\mathsf{par}\ell ; \alpha ) := (1, \alpha , \ldots , \alpha ^{\mathsf{par}\ell - 1})\) is a proximity generator with mutual correlated agreement for every smooth Reed Solomon code \(\mathcal{C}:= \mathrm{RS}[\mathbb {F}, \mathcal{L}, m]\) (with rate \(\rho := 2^m / |\mathcal{L}|\)). We give two conjectures, for the parameters of the proximity bound \({\mathsf{B}}^\star \) and the error \(\mathsf{err}^\star \):

1. Up to the Johnson bound: \({\mathsf{B}}^\star (\mathcal{C}, \mathsf{par}\ell ) := \sqrt{\rho },\) and

   \[ \mathsf{err}(\mathcal{C}, \mathsf{par}\ell , \delta ) := \frac{(\mathsf{par}\ell - 1) \cdot 2^m}{|\mathbb {F}| \cdot \left( 2 \cdot \min \left\{ 1 - \sqrt{\rho } - \delta , \frac{\sqrt{\rho }}{20} \right\} \right)^7}. \]

2. Up to capacity: \({\mathsf{B}}^\star (\mathcal{C}, \mathsf{par}\ell ) := \rho \), and there exist constants \(c_1, c_2, c_3 \in \mathbb {N}\) such that for every \(\eta {\gt} 0\) and \(0 {\lt} \delta {\lt} 1 - \rho - \eta \):

   \[ \mathsf{err}^\star (\mathcal{C}, \mathsf{par}\ell , \delta ) := \frac{(\mathsf{par}\ell - 1)^{c_2} \cdot \delta ^{c_2}}{\eta ^{c_1} \cdot \rho ^{c_1 + c_2} \cdot |\mathbb {F}|}. \]

Consider an \(n\)-tuple of values \(v = (v_1, \ldots , v_n) \in \mathbb {F}^n\) and a polynomial map \(E : \mathbb {F}^k \to \mathbb {F}^n\). The batching reduction is defined as:

• Protocol specification: Two messages:

  1. Verifier sends random \(r \in \mathbb {F}^k\) to prover

  2. Prover sends \(\langle E(r), v \rangle := \sum _{i=1}^n E(r)_i \cdot v_i\) to verifier

• Honest prover: Computes the inner product \(\langle E(r), v \rangle \) and sends it

• Honest verifier: Verifies that the received value equals the expected inner product

• Extractor: Trivial since there is no witness to extract

A binary tower field \(\mathcal{T}_{\iota }\) for \(\iota \in \mathbb {N}\) is defined inductively as the \(\iota \)-th field in the sequence of quadratic extensions over the ground field \(\mathbb {F}_2\).

• \(\mathcal{T}_{0} := \mathbb {F}_{2}\)

• \(\forall \iota {\gt} 0\), \(\mathcal{T}_{\iota } := \mathcal{T}_{\iota -1}[X_{\iota -1}] / (X_{\iota -1}^{2}+X_{\iota -2} \cdot X_{\iota -1}+1)\), where we conventionally set \(X_{-1} := 1\).

Let \(\mathcal{L}\subseteq \mathbb {F}\) be a smooth evaluation domain and \(k \in \mathbb {N}\) be a folding parameter. For \(z \in \mathcal{L}^{2^k}\), define \(\mathrm{Block}(\mathcal{L}, i, k, z) := \{ x \in \mathcal{L}, y \in \mathcal{L}^{2^i} : y^{2^{k-i}} = z \} \).

Let \(\mathcal{C}:= \mathrm{RS}[\mathbb {F}, \mathcal{L}, m]\) be a smooth Reed Solomon code and let \(f, g : \mathcal{L}^{2^i} \to \mathbb {F}\). We define the \((i,k)\)-wise block relative distance as

The oracle version handles predicates that require oracle access:

• Oracle predicate: \(\mathsf{pred} : \mathsf{StmtIn}\to \mathsf{OracleComp}[\mathsf{OStmtIn}]_{\mathcal{O}} \mathsf{Prop}\)

• Never-fails condition: \(\mathsf{pred}(\mathsf{stmt})\) never fails for any statement

• Oracle computation: Verifier executes oracle computation to check predicate

• Input relation: Defined via oracle simulation of the predicate

The CheckClaim reduction is a zero-round protocol that verifies predicates:

• Protocol specification: \(\mathsf{pSpec}:= []\) (no messages exchanged)

• Predicate: \(\mathsf{pred} : \mathsf{StmtIn}\to \mathsf{Prop}\) (decidable)

• Prover: Simply stores and outputs the input statement with unit witness

• Verifier: Checks \(\mathsf{pred}(\mathsf{stmt})\) and outputs statement if successful

• Input relation: \(R_{\mathsf{in}}(\mathsf{stmt}, ()) := \mathsf{pred}(\mathsf{stmt})\)

• Output relation: \(R_{\mathsf{out}}(\mathsf{stmt}, ()) := \mathsf{True}\) (trivial after verification)

Given target degree \(d^*\in \mathbb {N}\), shifting parameter \(r\in \mathbb {F}\), functions \(f_0,\ldots ,f_{m-1}:\mathcal{L}\rightarrow \mathbb {F}\), and degrees \(0\leq d_0,\ldots ,d_{m-1}\leq {d}^*\), we define \(\mathsf{Combine}(d^*,r,(f_0,d_0),\ldots ,(f_{m-1},d_{m-1})):\mathcal{L}\rightarrow \mathbb {F}\) as follows:

Above, \(r_i:=r^{i-1+\sum _{j{\lt}i}(d^*-d_j)}\).

Building upon the abstract definition of binary tower fields, we define a concrete, computable representation of binary tower fields. This construction, which underpins our formalization, represents each element of the field \(\mathcal{T}_\iota \) as a bit vector of length \(2^\iota \) corresponding to the coefficients of the multilinear \(\mathbb {F}_2\)-basis.

The arithmetic operations on these bit-vector representations are defined as follows:

• Addition: The sum of two elements is defined as the bitwise XOR of their corresponding bit-vector representations.

• Multiplication (in \(\mathcal{T}_\iota \)): The product of two elements within the same field \(\mathcal{T}_\iota \) is defined via a recursive Karatsuba-based algorithm  [ 10 ] . The complexity of this operation is \(\Theta (2^{\log _2(3) \cdot \iota })\).

• Cross-Level Multiplication: The product of an element \(\alpha \in \mathcal{T}_{\iota +\kappa }\) by a scalar \(b \in \mathcal{T}_\iota \) is defined by representing \(\alpha \) via its \(2^\kappa \) coefficients \((a_u)_{u \in \{ 0,1\} ^\kappa }\) in the \(\mathcal{T}_\iota \)-basis and performing the multiplication component-wise on those coefficients in the subfield \(\mathcal{T}_\iota \). The total complexity is \(2^\kappa \cdot \Theta (2^{\log _2(3) \cdot \iota })\).

Given target degree \(d^*\in \mathbb {N}\), shifting parameter \(r\in \mathbb {F}\), function \(f:\mathcal{L}\rightarrow \mathbb {F}\), and degree \(0\leq d\leq d^*\), we define \(\mathsf{DegCor}(d^*,r,f,d)\) as follows.

(Observe that \(\mathsf{DegCor}(d^*,r,f,d)=\mathsf{Combine}(d^*,r,(f,d))\).)

The DoNothing reduction is a zero-round protocol with the following components:

• Protocol specification: \(\mathsf{pSpec}:= []\) (empty protocol, no messages exchanged)

• Prover: Simply stores the input statement and witness, and outputs them unchanged

• Verifier: Takes the input statement and outputs it directly

• Input relation: Any relation \(R_{\mathsf{in}} : \mathsf{StmtIn}\to \mathsf{WitIn}\to \mathsf{Prop}\)

• Output relation: The same relation \(R_{\mathsf{out}} := R_{\mathsf{in}}\)

Let \(\mathsf{extract}:\mathcal{L}^{2^{k+1}}\rightarrow \mathcal{L}^{2^k}\) be a function. There exists \(x \in \mathcal{L}\), such that \(y = x^{2^{k+1}}\in \mathcal{L}^{2^{k+1}}\). Then \(\mathsf{extract}\) returns \(z = \sqrt{y} = x^{2^k}\in \mathcal{L}^{2^k}\) such that \(y = z^2\).

Let \(f:\mathcal{L}\rightarrow \mathbb {F}\) be a function, \(k\in \mathbb {N}\) a folding parameter and \(\alpha \in \mathbb {F}\). For every \(x\in {\mathcal{L}}^k\), let \(\hat{p}_x\in \mathbb {F}^{{\lt}k}[X]\) be the polynomial where \(\hat{p}_x(y)=f(y)\) for every \(y\in {\mathcal{L}}\) such that \(y^k=x\). We define \(\mathsf{Fold}(f,k,\alpha ):\mathcal{L}\rightarrow \mathbb {F}\) as follows.

In order to compute \(\mathsf{Fold}(f,k,\alpha )(x)\) it suffices to interpolate the \(k\) values \(\{ f(y):y\in \mathcal{L}\text{ s.t. }y^k=x\} \) into the polynomial \(\hat{p}_x\) and evaluate this polynomial at \(\alpha \).

For \(k \leq m\) and \(\vec{\alpha } = (\alpha _0, \ldots , \alpha _{k-1}) \in \mathbb {F}^k\) we define \(\mathrm{Fold}(f, \vec{\alpha }) : \mathcal{L}^{2^k} \to \mathbb {F}\) to equal \(\mathrm{Fold}(f, \vec{\alpha }) := f_k\) where \(f_k\) is defined recursively as follows: \(f_0 := f\), and \(f_i := \mathrm{Fold_f}(f_{i-1}, \alpha _i)\).

For a set \(S \subseteq \mathbb {F}^{\mathcal{L}}\) we denote \(\mathrm{Fold_{S}}(S, \vec{\alpha }) := \{ \mathrm{Fold_{S}}(f, \vec{\alpha }) \mid f \in S\} \).

Let \(f : \mathcal{L}^{2^k} \to \mathbb {F}\) be a function, and \(\alpha \in \mathbb {F}\). We define \(\mathrm{Fold_f}(f, {\alpha }) : \mathcal{L}^{(2^{k+1})} \to \mathbb {F}\) as follows:

In order to compute \(\mathrm{Fold_f}(f, \alpha )(y)\) it suffices to query \(f\) at \(x\) and \(-x\), by retrieving \(x=\mathsf{extract}(y)\).

Let \(\mathcal{C}\) be a linear code. We say that \(\mathsf{Gen}\) be a proximity generator with mutual correlated agreement with proximity bounds \({\mathsf{B}}^\star \) and \(\mathsf{err}^\star \), if for \(f_0,\ldots ,f_{\mathsf{par}\ell -1}:\mathcal{L}\rightarrow \mathbb {F}\) and \(\delta \in (0,1-{\mathsf{B}}^\star (\mathcal{C},\mathsf{par}\ell ))\) the following holds.

For a smooth Reed Solomon code \(\mathrm{RS}:= \mathrm{RS}[\mathbb {F}, \mathcal{L}, m]\), proximity parameter \(\delta \in [0,1]\), and \(f : \mathcal{L}^{2^i} \to \mathbb {F}\), we let

denote the list of codewords in \(\mathcal{C}\) within relative block distance at most \(\delta \) from \(f\).

For \(S \subseteq \mathbb {F}^{\mathcal{L}}\), we let \(\Delta _{r}(\mathcal{C}, i, k, f, S) := \min _{g \in S} \Delta _{r}(\mathcal{C}, i, k, f, g)\).

For any tower field \(\mathcal{T}_\iota \), we define its canonical bases as follows:

• \(\mathbb {F}_2\)-Basis of \(\mathcal{T}_\iota \): The set of multilinear monomials in the variables \(\{ X_0, \dots , X_{\iota -1}\} \) forms a basis for \(\mathcal{T}_\iota \) as a \(2^\iota \)-dimensional vector space over \(\mathbb {F}_2\). An element is typically stored as a \(2^\iota \)-bit string corresponding to this basis.

• \(\mathcal{T}_\iota \)-Basis of \(\mathcal{T}_{\iota +\kappa }\): For any \(\kappa \ge 0\), the set of multilinear monomials in the variables \(\{ X_\iota , \dots , X_{\iota +\kappa -1}\} \) forms a basis for \(\mathcal{T}_{\iota +\kappa }\) as a \(2^\kappa \)-dimensional vector space over the subfield \(\mathcal{T}_\iota \).

For oracles \(\mathsf{a}, \mathsf{b}\) of the same type, we define their distance as:

We say an oracle type has distance bound \(d\) if for any two distinct oracles \(\mathsf{a} \neq \mathsf{b}\), we have \(\mathsf{distance}(\mathsf{a}, \mathsf{b}) \geq |\mathsf{Query}| - d\).

Given a polynomial \(\hat{f}\in \mathbb {F}^{{\lt}d}[X]\), a folding parameter \(k\in \mathbb {N}\) and \(r\in \mathbb {F}\), we define a polynomial \(\mathsf{PolyFold}(\hat{f},k,r)\in \mathbb {F}^{d/k}[X]\) as follows. Let \(\hat{Q}[X,Y]\) be the bivariate polynomial derived from \(\hat{f}\) using Fact 147 with \(\hat{q}(X):=X^k\). Then \(\mathsf{PolyFold}(\hat{f},k,r)(X):=\hat{Q}(X,r)\).

Let \(\hat{f}\in \mathbb {F}^{{\lt}d}[X]\) be a polynomial and \(S\subseteq \mathbb {F}\) be a set, let \(\hat{V}_S\in \mathbb {F}^{{\lt}|S|+1}[X]\) be the unique non-zero polynomial with \(\hat{V}_S(x)=0\) for every \(x\in S\). The polynomial quotient \(\mathsf{PolyQuotient}(\hat{f},S)\in \mathbb {F}^{{\lt}d-|S|}[X]\) is defined as follows:

where \(\hat{Ans}\in \mathbb {F}^{{\lt}|S|}[X]\) is the unique non-zero polynomial with \(\hat{Ans}(x)=\hat{f}(x)\) for every \(x \in S\).

Consider two univariate polynomials \(P, Q \in \mathbb {F}[X]\) of degree at most \(d\), available as polynomial evaluation oracles. The polynomial equality testing reduction is defined as:

• Input relation: \(P = Q\) as polynomials

• Protocol specification: Single challenge of type \(\mathbb {F}\) from verifier to prover

• Honest prover: Receives the random field element \(r\) but performs no computation

• Honest verifier: Checks that \(P(r) = Q(r)\) by querying both polynomial oracles

• Output relation: \(P(r) = Q(r)\) for the sampled point \(r\)

Let \(\mathcal{C}\subseteq \mathbb {F}^{\mathcal{L}}\) be a linear code. We say that \(\mathsf{Gen}\) is a proximity generator for \(\mathcal{C}\) with proximity bounds \({\mathsf{B}}\) and \(\mathsf{err}\) if the following implication holds for \(f_0,\ldots ,f_{\mathsf{par}\ell -1} : \mathcal{L}\rightarrow \mathbb {F}\) and \(\delta \in (0,1-{\mathsf{B}}(\rho ,\mathsf{par}\ell ))\). If

Let \(f:\mathcal{L}\to \mathbb {F}\) be a function, \(S\subseteq \mathbb {F}\) be a set, and \(\mathsf{Ans},\mathsf{Fill}: S\rightarrow \mathbb {F}\) be functions. Let \(\hat{\mathsf{Ans}}\in \mathbb {F}^{{\lt}|S|}[X]\) be the (unique) polynomial with \(\hat{\mathsf{Ans}}(x)=\mathsf{Ans}(x)\) for every \(x\in S\), and let \(\hat{V}_S\in \mathbb {F}^{{\lt}|S|+1}[X]\) be the unique non-zero polynomial with \(\hat{V}_S(x)=0\) for every \(x\in S\). The quotient function \(\mathsf{Quotient}\bigl(f,S,\mathsf{Ans},\mathsf{Fill}\bigr): \mathcal{L}\to \mathbb {F}\) is defined as follows:

The RandomQuery reduction tests equality between two oracles by random querying:

• Input: Two oracles \(\mathsf{a}, \mathsf{b}\) of the same type with oracle interface

• Protocol specification: \(\mathsf{pSpec}:= [(\mathsf{V \! \! \rightarrow \! \! P}, \mathsf{Query})]\) (single challenge from verifier)

• Input relation: \(R_{\mathsf{in}}((), (\mathsf{a}, \mathsf{b}), ()) := (\mathsf{a} = \mathsf{b})\)

• Verifier: Samples random query \(q\) and sends it to prover

• Prover: Receives query \(q\), performs no computation

• Output relation: \(R_{\mathsf{out}}((q, (\mathsf{a}, \mathsf{b})), ()) := (\mathsf{oracle}(\mathsf{a}, q) = \mathsf{oracle}(\mathsf{b}, q))\)

A variant of RandomQuery where the second oracle is replaced with an explicit response:

• Input: Single oracle \(\mathsf{a}\) and target response \(r\)

• Output relation: \(R_{\mathsf{out}}(((q, r), \mathsf{a}), ()) := (\mathsf{oracle}(\mathsf{a}, q) = r)\)

This variant is useful when one wants to verify a specific query-response pair rather than oracle equality.

The oracle version additionally handles oracle statements through an embedding:

• Oracle statement mapping: Embedding \(\mathsf{embedIdx} : \iota _{\mathsf{out}} \hookrightarrow \iota _{\mathsf{in}}\)

• Type compatibility: \(\mathsf{OStmtIn}(\mathsf{embedIdx}(i)) = \mathsf{OStmtOut}(i)\) for all \(i\)

• Oracle embedding: Maps output oracle indices to corresponding input oracle indices

The ReduceClaim reduction is a zero-round protocol that transforms claims via explicit mappings:

• Protocol specification: \(\mathsf{pSpec}:= []\) (no messages exchanged)

• Statement mapping: \(\mathsf{mapStmt} : \mathsf{StmtIn}\to \mathsf{StmtOut}\)

• Witness mapping: \(\mathsf{mapWit} : \mathsf{WitIn}\to \mathsf{WitOut}\)

• Prover: Applies both mappings to input statement and witness

• Verifier: Applies statement mapping to input statement

• Input relation: \(R_{\mathsf{in}} : \mathsf{StmtIn}\to \mathsf{WitIn}\to \mathsf{Prop}\)

• Output relation: \(R_{\mathsf{out}} : \mathsf{StmtOut}\to \mathsf{WitOut}\to \mathsf{Prop}\)

• Relation condition: \(R_{\mathsf{in}}(\mathsf{stmt}, \mathsf{wit}) \iff R_{\mathsf{out}}(\mathsf{mapStmt}(\mathsf{stmt}), \mathsf{mapWit}(\mathsf{wit}))\)

The SendClaim reduction is a one-round protocol for claim transmission:

• Protocol specification: \(\mathsf{pSpec}:= [(\mathsf{P \! \! \rightarrow \! \! V}, \mathsf{OStmtIn})]\) (single oracle message)

• Input: Statement and single oracle statement (via \(\mathsf{Unique}\) index type)

• Prover: Sends the input oracle statement as protocol message

• Verifier: Executes oracle computation \(\mathsf{relComp} : \mathsf{StmtIn}\to \mathsf{OracleComp}[\mathsf{OStmtIn}]_{\mathcal{O}} \mathsf{Unit}\)

• Output oracle statements: Sum type \(\mathsf{OStmtIn}\oplus \mathsf{OStmtIn}\) containing both original and transmitted claims

• Output relation: \(R_{\mathsf{out}}((), \mathsf{oracles}) := \mathsf{oracles}(\mathsf{inl}) = \mathsf{oracles}(\mathsf{inr})\)

A specialized variant for a single witness with oracle interface:

• Witness type: \(\mathsf{WitIn}: \mathsf{Type}\) with oracle interface

• Protocol specification: \(\mathsf{pSpec}:= [(\mathsf{P \! \! \rightarrow \! \! V}, \mathsf{WitIn})]\)

• Conversion: Implicitly converts to indexed family \(\mathsf{WitIn}: \mathsf{Fin}(1) \to \mathsf{Type}\)

The oracle version handles witnesses that are indexed families of types with oracle interfaces:

• Witness type: \(\mathsf{WitIn}: \iota _w \to \mathsf{Type}\) where each \(\mathsf{WitIn}(i)\) has an oracle interface

• Protocol specification: \(\mathsf{pSpec}:= [(\mathsf{P \! \! \rightarrow \! \! V}, \forall i, \mathsf{WitIn}(i))]\)

• Output oracle statements: Combination of input oracle statements and the transmitted witness

The SendWitness reduction is a one-round protocol where the prover sends the complete witness to the verifier:

• Protocol specification: \(\mathsf{pSpec}:= [(\mathsf{P \! \! \rightarrow \! \! V}, \mathsf{WitIn})]\) (single message from prover to verifier)

• Prover: Sends the witness \(\mathbb {w}\) as its single message

• Verifier: Receives the witness and combines it with the input statement to form the output

• Input relation: \(R_{\mathsf{in}} : \mathsf{StmtIn}\to \mathsf{WitIn}\to \mathsf{Prop}\)

• Output relation: \(R_{\mathsf{out}} : (\mathsf{StmtIn}\times \mathsf{WitIn}) \to \mathsf{Unit}\to \mathsf{Prop}\) defined by \(((\mathsf{stmt}, \mathsf{wit}), ()) \mapsto R_{\mathsf{in}}(\mathsf{stmt}, \mathsf{wit})\)

The \(i\)-th round of sum-check consists of:

1. Input: A statement containing target value and prior challenges, along with an oracle for the multivariate polynomial

2. Prover’s message: A univariate polynomial \(p_i \in R[X]_{\leq d}\)

3. Verifier’s challenge: A random element \(r_i \gets R\)

4. Output: An updated statement with new target \(p_i(r_i)\) and extended challenges

1. In this protocol, the context is a pair \((p, d)\), where \(p\) is now a univariate polynomial of bounded degree. The predicate / relation is that \(p(0) + p(1) = d\).

2. The prover first sends a univariate polynomial \(s\) of the same bounded degree as \(p\). In the honest case, it would just send \(p\) itself.

3. The verifier samples and sends a random challenge \(r \gets R\).

4. The verifier checks that \(s(0) + s(1) = d\). The predicate on the resulting output context is that \(p(r) = s(r)\).

The state function for the virtual sum-check round protocol is given by:

1. The initial state function is the same as the predicate on the initial context, namely that \(p(0) + p(1) = d\).

2. The state function after the prover sends \(s\) is the predicate that \(p(0) + p(1) = d\) and \(s(0) + s(1) = d\). Essentially, we add in the verifier’s check.

3. The state function for the output context (after the verifier sends \(r\)) is the predicate that \(s(0) + s(1) = d\) and \(p(r) = s(r)\).

Let \(\mathbb {F}\) be a field, \(r\in \mathbb {F}\) be a field element, \(a\in \mathbb {N}\) be a natural number. Then

Given a polynomial \(\hat{q}\in \mathbb {F}[X]\):

• For every univariate polynomial \(\hat{f}\in \mathbb {F}[X]\), there exists a unique bivariate polynomial \(\hat{Q}\in \mathbb {F}[X,Y]\) with:

  \[ \mathsf{deg}_X(\hat{Q}) := \left\lfloor \frac{\mathsf{deg}(\hat{f})}{\mathsf{deg}(\hat{q})} \right\rfloor ,\quad \mathsf{deg}_Y(\hat{Q}) {\lt} \mathsf{deg}(\hat{q}) \]

  such that \(\hat{f}(Z)=\hat{Q}(\hat{q}(Z),Z)\). Moreover, \(\hat{Q}\) can be computed efficiently given \(\hat{f}\) and \(\hat{q}\). Observe that if \(\mathsf{deg}(\hat{f}){\lt}t\cdot \mathsf{deg}(\hat{q})\) then \(\mathsf{deg}(\hat{Q}){\lt}t\).

• For every \(\hat{Q}[X,Y]\) with \(\mathsf{deg}_X(\hat{Q}){\lt}t\) and \(\mathsf{deg}_Y(\hat{Q}){\lt}\mathsf{deg}(\hat{q})\), the polynomial \(\hat{f}(Z)=\hat{Q}(\hat{q}(Z),Z)\) has degree \(\mathsf{deg}(\hat{f}){\lt}t\cdot \mathsf{deg}(\hat{q})\).

Let \(\mathcal{C}\subseteq \mathbb {F}^{\mathcal{L}}\) be a linear code with minimum distance \(\delta _{\mathcal{C}}\), and let \(\mathsf{Gen}\) be a proximity generator for \(\mathcal{C}\) with mutual correlated agreement with proximity bound \({\mathsf{B}}^\star \) and error \(\mathsf{err}^\star \). Then, for every \(f_0, \ldots , f_{\mathsf{par}\ell -1} : \mathcal{L}\to \mathbb {F}\) and \(\delta \in (0, \min \{ \delta _{\mathcal{C}}, 1 - {\mathsf{B}}^\star (\mathcal{C}, \mathsf{par}\ell )\} )\):

For any \(\mathcal{C}:= \mathrm{RS}[\mathbb {F}, \mathcal{L}, m]\), \(k \in \mathbb {N}\), and \(f, g : \mathcal{L}^{2^i} \to \mathbb {F}\), we have that \(\Delta (f, g) \leq \Delta _{r}(\mathcal{C}, i, k, f, g)\). Consequently, \(\Lambda _{r}(\mathcal{C}, i, k, f, \delta ) \subseteq \Lambda (\mathcal{C}, f, \delta )\) for \(\delta \in [0,1]\).

Let \(d^*\) be a target degree, \(f_0,\ldots ,f_{m-1}:\mathcal{L}\rightarrow \mathbb {F}\) be functions, \(0\leq d_0,\ldots ,d_{m-1}\leq d^*\) be degrees, \(\delta \in \min {\{ 1-{\mathsf{B}}^*(\rho ),1-\rho -1/|\mathcal{L}|\} }\) be a distance parameter, where \(\rho =d^*/|\mathcal{L}|\). If

then there exists \(S\subseteq \mathcal{L}\) with \(|S|\geq (1-\delta )\cdot |\mathcal{L}|\), and

Note that this implies \(\Delta (f_i,\mathrm{RS}[\mathbb {F},\mathcal{L},d_i]){\lt}\delta \) for every \(i\). Above, \({\mathsf{B}}^*\) and \({\mathsf{err}}^*\) are the proximity bound and error (respectively) described in the proximity gap theorem.

Let \(f : \mathcal{L}\rightarrow \mathbb {F}\) be a function, \(m \in \mathbb {N}\) be a number of variables, \(s \in \mathbb {N}\) be a repetition parameter, and let \(\delta \in [0,1]\) be a distance parameter. For every \(\vec{r_0}, \dots , \vec{r_{s-1}} \in \mathbb {F}^m\), the following are equivalent statements.

• There exist distinct \(u, u' \in \Lambda (\mathrm{RS}[\mathbb {F}, \mathcal{L}, m], f, \delta )\) such that, for every \(i \in [0,s-1]\), \(\hat{u}(\vec{r_i}) = \hat{u}'(\vec{r_i})\).

• There exists \(\sigma _0, \dots , \sigma _{s-1} \in \mathbb {F}\) such that

  \[ \left| \Lambda (\mathrm{CRS}[\mathbb {F}, \mathcal{L}, m, ((Z \cdot \mathrm{eq}(\vec{r_0}, \cdot ), \sigma _0), \dots , (Z \cdot \mathrm{eq}(\vec{r_{s-1}}, \cdot ), \sigma _{s-1}))], f, \delta ) \right| {\gt} 1. \]

Let \(f : \mathcal{L}\to \mathbb {F}\) be a function, \(\vec{\alpha } \in \mathbb {F}^k\) folding randomness and let \(g := \mathrm{Fold}(f, \vec{\alpha })\). If \(f \in \mathrm{RS}[\mathbb {F}, \mathcal{L}, m]\) and \(k \leq m\), then \(g \in \mathrm{RS}[\mathbb {F}, \mathcal{L}^{2^k}, m - k]\), and further the multilinear extension of \(g\) is given by \(\hat{g}(X_k, \ldots , X_{m-1}) := \hat{f}(\vec{\alpha }, X_k, \ldots , X_{m-1})\) where \(\hat{f}\) is the multilinear extension of \(f\).

For every function \(f:\mathcal{L}\rightarrow \mathbb {F}\), degree parameter \(d\in \mathbb {N}\), folding parameter \(k\in \mathbb {N}\), distance parameter \(\delta \in (0,\min \{ {\Delta (\mathsf{Fold}[f,k,r^{\mathsf{fold}}],\mathrm{RS}[\mathbb {F},{\mathcal{L}}^k, d/k]),1-{\mathsf{B}}^*(\rho )}\} )\), letting \(\rho :=\frac{d}{|\mathcal{L}|}\),

Above, \({\mathsf{B}}^*\) and \({\mathsf{err}}^*\) are the proximity bound and error (respectively) described in Section ??.

Let \(\mathcal{C}:= \mathrm{RS}[\mathbb {F}, \mathcal{L}, m]\) be a Reed Solomon code, and \(k \leq m\) be a parameter. Denote \(\mathcal{C}' := \mathrm{RS}[\mathbb {F}, \mathcal{L}^{2}, m - 1]\). Then for every \(f : \mathcal{L}\to \mathbb {F}\) and \(\delta \in (0, 1 - {\mathsf{B}}^\star (\mathcal{C}', 2))\),

For every \(\alpha \in \mathbb {F}\), \(\mathrm{Fold_S}(\Lambda _{r}(\mathcal{C}, 0, k, f, \delta ), \alpha ) \subseteq \Lambda _{r}(\mathcal{C}', 1, k, \mathrm{Fold}(f, \alpha ), \delta )\).

Let \(\mathcal{C}\) be a linear code with minimum distance \(\delta _{\mathcal{C}}\) and let \(\mathsf{Gen}\) be a proximity generator for \(\mathcal{C}\) with proximity bound \({\mathsf{B}}\) and error \(\mathsf{err}\). Then \(\mathsf{Gen}\) has mutual correlated agreement with proximity bound \({\mathsf{B}}^\star (\mathcal{C}, \mathsf{par}\ell ) = \min \{ 1 - \delta _{\mathcal{C}}/2, \mathsf{B}(\mathcal{C}, \mathsf{par}\ell )\} \) and error \(\mathsf{err}^\star (\mathcal{C}, \mathsf{par}\ell , \delta ) := \mathsf{err}(\mathcal{C}, \mathsf{par}\ell , \delta )\).

Let \(f : \mathcal{L}\rightarrow \mathbb {F}\) be a function, \(m \in \mathbb {N}\) be a number of variables, \(s \in \mathbb {N}\) be a repetition parameter, and \(\delta \in [0,1]\) be a distance parameter. If \(\mathrm{RS}[\mathbb {F}, \mathcal{L}, m]\) is \((\delta , \ell )\)-list decodable then

Let \(f:\mathcal{L}\rightarrow \mathbb {F}\) be a function, \(d\in \mathbb {N}\) be a degree parameter, \(s\in \mathbb {N}\) be a repetition parameter, and \(\delta \in [0,1]\) be a distance parameter. If \(\mathrm{RS}[\mathbb {F},\mathcal{L},d]\) be \((d,l)\)-list decodable then

Let \(f:\mathcal{L}\rightarrow \mathbb {F}\) be a function, \(d\in \mathbb {N}\) be the degree parameter, \(\delta \in (0,1)\) be a distance parameter, \(S\subseteq \mathbb {F}\) be a set with \(|S|{\lt}d\), and \(\mathsf{Ans},\mathsf{Fill}:S\rightarrow \mathbb {F}\) are functions. Suppose that for every \(u\in \mathsf{List}(f,d,\delta )\) there exists \(x\in S\) with \(\hat{u}(x)\neq \mathsf{Ans}(x)\). Then

where \(T:=\{ x\in \mathcal{L}\cap S: \hat{\mathsf{Ans}}(x)\neq f(x)\} \).

Consider \((\mathbb {F},M,d,k_0,\ldots ,k_M,\mathcal{L}_0,\ldots ,\mathcal{L}_M,t_0,\ldots ,t_M)\) and for every \(i\in \{ 0,\ldots ,M\} \), let \(d_i:=\frac{d}{\prod _{j{\lt}i}k^j}\) and \(\rho _i:=d_i/|\mathcal{L}_i|\). For every \(f\notin \mathrm{RS}[\mathbb {F},\mathcal{L}_0,d_0]\) and every \(\delta _0,\ldots ,\delta _M\) where

• \(\delta _0\in (0,\Delta (f,\mathrm{RS}[\mathbb {F},\mathcal{L}_0,d_0])]\cap (0,1-{\mathsf{B}}^*(\rho _0))\)

• for every \(0{\lt}i\leq M\): \(\delta _i\in (0,\min {\{ 1-\rho _i-\frac{1}{|\mathcal{L}_i|},1-{\mathsf{B}^*(\rho _i)}\} })\), and

• for every \(0{\lt}i\leq M\): \(\mathrm{RS}[\mathbb {F},\mathcal{L}_i,d_i]\) is \((\delta _i,l_i)\)-list decodable,

There exists an IOPP with above parameters, that has round-by-round soundness error \((\epsilon ^{\mathsf{fold}},\epsilon ^{\mathsf{out}}_1,\epsilon ^{\mathsf{shift}}_1,\ldots ,\epsilon ^{\mathsf{out}}_M,\epsilon ^{\mathsf{shift}}_M,\epsilon ^{\mathsf{fin}})\) where:

• \(\epsilon ^{\mathsf{fold}}\leq \mathsf{err}^*(d_0/k_0,\rho _0,\delta _0,k_0)\).

• \(\epsilon ^{\mathsf{out}}_i\leq \frac{l^2_i}{2}\cdot {\big(\frac{d_i}{|\mathbb {F}|-|\mathcal{L}_i|}\big)}^s\)

• \(\epsilon ^{\mathsf{shift}}_i\leq {(1-\delta _{i-1})}^{t_{i-1}}+\mathsf{err}^*(d_i,\rho _i,\delta _i,t_{i-1}+s)+\mathsf{err}^*(d_i/k_i,\rho _i,\delta _i,k_i)\).

• \(\epsilon ^{\mathsf{fin}}\leq {(1-\delta _M)}^{t_M}\).

Above, \({\mathsf{B}}^*\) and \({\mathsf{err}}^*\) are the proximity bound and error (respectively) described in Section ??.

Consider \((\mathbb {F}, M, (k_i, m_i, \mathcal{L}_i, t_i)_{0 \leq i \leq M}, \widehat{w}_0, \sigma _0, m, d^\star , d)\) with the following ingrediants and conditions,

• a constrained Reed Solomon code \(\mathrm{CRS}[\mathbb {F}, \mathcal{L}_0, m_0, \widehat{w}_0, \sigma _0]\);

• an iteration count \(M \in \mathbb {N}\);

• folding parameters \(k_0, \ldots , k_{M}\) such that \(\sum _{i=0}^{M} k_i \leq m\);

• evaluation domains \(\mathcal{L}_0, \ldots , \mathcal{L}_{M} \subseteq \mathbb {F}\) where \(\mathcal{L}_i\) is a smooth coset of \(\mathbb {F}^*\) with order \(|\mathcal{L}_i| \geq 2^{m_i}\);

• repetition parameters \(t_0, \ldots , t_M\) with \(t_i \leq |\mathcal{L}_i|\);

• define \(m_0 := m\) and \(m_i := m - \sum _{j {\lt} i} k_j\);

• define \(d^\star := 1 + \deg _{\mathbb {Z}}(\widehat{w}_0) + \max _{i \in [m_0]} \deg _{X_i}(\widehat{w}_0)\) and \(d := \max \{ d^\star , 3\} \).

For every \(f \notin \mathrm{CRS}[\mathbb {F}, \mathcal{L}_0, m_0, \widehat{w}_0, \sigma _0]\) and every \(\delta _0, \dots , \delta _{M}\) and \((\mathsf{par}\ell _{i,s})_{0 \leq i \leq M}^{0 \leq s \leq k_i}\) where

• \(\delta _0 \in (0, \Delta (f, \mathrm{CRS}[\mathbb {F}, \mathcal{L}_0, m_0, \widehat{w}_0, \sigma _0]))\);

• the function \(\mathsf{Gen}(\mathsf{par}\ell ; \alpha ) = (1, \alpha , \dots , \alpha ^{\mathsf{par}\ell -1})\) is a proximity generator with mutual correlated agreement for the codes \((\mathcal{C}_{\mathrm{RS}}^{(i,s)})_{0 \leq i \leq M}^{0 \leq s \leq k_i}\) where \(\mathcal{C}_{\mathrm{RS}}^{(i,s)} := \mathrm{RS}[\mathbb {F}, \mathcal{L}_i^{(2^s)}, m_i - s]\) with bound \({\mathsf{B}}^\star \) and error \(\mathsf{err}^\star \);

• for every \(0 \leq i \le M\), \(\delta _i \in (0, 1 - {\mathsf{B}}^\star (\mathcal{C}_{\mathrm{RS}}^{(i,s)}, 2))\);

• for every \(0 \leq i \le M\), \(\mathcal{C}_{\mathrm{RS}}^{(i,s)}\) is \((\ell _{i,s}, \delta _i)\)-list decodable.

Then there exists an IOPP for \(\mathrm{CRS}[\mathbb {F}, \mathcal{L}_0, m_0, \widehat{w}_0, \sigma _0]\) with above parameters, with round-by-round soundness error

where:

• \(\varepsilon _{0,s}^{\mathrm{fold}} \leq \dfrac {d^* \cdot \ell _{0,s-1}}{|\mathbb {F}|} + \mathrm{err}^*(\mathcal{C}_{\mathrm{RS}}^{(0,s)}, 2, \delta _0)\);

• \(\varepsilon _i^{\mathrm{out}} \leq \dfrac {2^{m_i} \cdot \ell _{i,0}^2}{2 \cdot |\mathbb {F}|}\);

• \(\varepsilon _i^{\mathrm{shift}} \leq (1 - \delta _{i-1})^{t_i - 1} + \dfrac {\ell _{i,0} \cdot (t_i - 1 + 1)}{|\mathbb {F}|}\);

• \(\varepsilon _{i,s}^{\mathrm{fold}} \leq \dfrac {d \cdot \ell _{i,s-1}}{|\mathbb {F}|} + \mathrm{err}^*(\mathcal{C}_{\mathrm{RS}}^{(i,s)}, 2, \delta _i)\);

• \(\varepsilon ^{\mathrm{fin}} \leq (1 - \delta _{M-1})^{t_M - 1}\).

The defining polynomial \(X_{\iota -1}^{2}+X_{\iota -2} \cdot X_{\iota -1}+1\) of \(\mathcal{T}_{\iota }\) is irreducible over \(\mathcal{T}_{\iota -1}\) for all \(\iota {\gt} 0\).

We prove that the binary tower fields are finite fields:

• The ground field \(\mathcal{T}_{0} := \mathbb {F}_2\) is a field. For all \(\iota {\gt} 0\), \(\mathcal{T}_{\iota }\) is the quotient ring of \(\mathcal{T}_{\iota -1}[X_{\iota -1}]\) by the irreducible polynomial \(X_{\iota -1}^{2}+X_{\iota -2} \cdot X_{\iota -1}+1\), therefore \(\mathcal{T}_{\iota }\) is a field extension of \(\mathcal{T}_{\iota -1}\).

• For all \(\iota \in \mathbb {N}\), the cardinality of \(\mathcal{T}_{\iota }\) is \(2^{2^{\iota }}\).

• For all \(\iota \in \mathbb {N}\), the characteristic of \(\mathcal{T}_{\iota }\) is 2.

Let \(\mathcal{C}= \mathrm{RS}[\mathbb {F}, \mathcal{L}, m]\) be a smooth Reed Solomon code and \(k \leq m\). For \(0 \leq i \leq k\) let \(\mathcal{C}^{(i)} := \mathrm{RS}[\mathbb {F}, \mathcal{L}^{2^i}, m - i]\). Let \(\mathsf{Gen}(\mathsf{par}\ell ; \alpha ) = (1, \alpha , \ldots , \alpha ^{\mathsf{par}\ell - 1})\) be a proximity generator with mutual correlated agreement for the codes \(\mathcal{C}^{(0)}, \ldots , \mathcal{C}^{(k-1)}\) with proximity bound \({\mathsf{B}}^\star \) and error \(\mathsf{err}^\star \). Then for every \(f : \mathcal{L}\to \mathbb {F}\) and \(\delta \in \left(0, 1 - \max _{i \in [0,(k-1)]} \{ {\mathsf{B}}^\star (\mathcal{C}^{(i)}, 2) \} \right)\),

Let \(\mathcal{C}:= \mathrm{RS}[\mathbb {F},\mathcal{L},d]\) be a Reed Solomon code with rate \(\rho :=\frac{d}{|\mathcal{L}|}\) and let \(B^*(\rho ):=\sqrt{\rho }\). For every \(\delta \in (0,1 - B^*(\rho ))\) and functions \(f_0,\ldots ,f_{m-1} : \mathcal{L}\to \mathbb {F}\), if

then there exists a subset \(S \subseteq \mathcal{L}\) with \(|S| \ge (1 - \delta )\cdot |L|\), and for every \(i \in [m]\), there exists \(u \in \mathrm{RS}[\mathbb {F},\mathcal{L},d]\) such that \(f_i(S) = u(S)\).

Above, \(\mathsf{err}^*(d,\rho ,\delta ,m)\) is defined as follows:

• if \(\delta \in \left(0,\frac{1-\rho }{2}\right]\) then

  \[ \mathsf{err}^*(d,\rho ,\delta ,m)=\frac{(m-1)\cdot d}{\rho \cdot |\mathbb {F}|} \]

• if \(\delta \in \Bigl(\frac{1-\rho }{2}, 1-\sqrt{\rho }\Bigr)\) then

  \[ \mathsf{err}^*(d,\rho ,\delta ,m)=\frac{(m-1)\cdot {d}^2}{|\mathbb {F}|\cdot {\Bigl(2\cdot \min \{ 1-\sqrt{\rho }-\delta ,\frac{\sqrt{\rho }}{20}\} \Bigr)}^7} \]

Let \(\mathcal{C}= \mathrm{RS}[\mathbb {F},\mathcal{L},m]\) be a Reed Solomon code with rate \(\rho = 2^m/|\mathcal{L}|\). \(\mathsf{Gen}(\alpha ,\mathsf{par}\ell )=\{ 1,\alpha ,\ldots ,\alpha ^{\mathsf{par}\ell -1}\} \) is a proximity generator for \(\mathcal{C}\) with proximity bounds \({\mathsf{B}}(\rho ,\mathsf{par}\ell )=\sqrt{\rho }\) and \(\mathsf{err}(C,\mathsf{par}\ell ,\delta )\) defined below.

• if \(\delta \in \left(0,\frac{1-\rho }{2}\right]\) then

  \[ \mathsf{err}(\mathcal{C},\mathsf{par}\ell ,\delta )=\frac{(m-1)\cdot d}{\rho \cdot |\mathbb {F}|} \]

• if \(\delta \in \Bigl(\frac{1-\rho }{2}, 1-\sqrt{\rho }\Bigr)\) then

  \[ \mathsf{err}(\mathcal{C},\mathsf{par}\ell ,\delta )=\frac{(m-1)\cdot {d}^2}{|\mathbb {F}|\cdot {\Bigl(2\cdot \min \{ 1-\sqrt{\rho }-\delta ,\frac{\sqrt{\rho }}{20}\} \Bigr)}^7} \]

Consider the following ingrediants:

• A security parameter \(\lambda \in \mathbb {N}\).

• A Reed-Solomon code \(\mathrm{RS}[\mathbb {F},\mathcal{L},d]\) with \(\rho :=\frac{d}{|\mathcal{L}|}\) where \(d\) is a power of \(2\), and \(\mathcal{L}\) is a smooth domain.

• A proximity parameter \(\delta \in (0,1-1.05\cdot \sqrt{\rho })\).

• A folding parameter \(k\in \mathbb {N}\) that is power of \(2\) with \(k\geq 4\).

If \(|\mathbb {F}|=\Omega (\frac{\lambda \cdot 2^\lambda \cdot d^2\cdot {|\mathcal{L}|}^2}{\log (1/\rho )})\), there is a public-coin IOPP for \(\mathrm{RS}[\mathbb {F},\mathcal{L},d]\) with the following parameters:

• Round-by-round soundness error \(2^{-\lambda }\).

• Round complexity: \(M:=O(\log _k{d})\).

• Proof length: \(|\mathcal{L}|+O_k(\log {d})\).

• Query complexity to the input: \(\frac{\lambda }{-\log {(1-\delta )}}\).

• Query complexity to the proof strings: \(O_k(\log {d}+\lambda \cdot \log {\Big(\frac{\log {d}}{\log {1/\rho }}\Big)})\).

The sum-check protocol satisfies knowledge soundness. The soundness error is bounded by \(n \cdot d / |R|\), where \(n\) is the number of rounds, \(d\) is the degree bound, and \(|R|\) is the size of the field.

The sum-check protocol satisfies perfect completeness. That is, for any valid input statement and oracle statement satisfying the input relation, the protocol accepts with probability 1.

The sum-check protocol satisfies round-by-round knowledge soundness. Each individual round can be analyzed independently, and the soundness error in each round is bounded by \(d / |R|\).

The sum-check protocol satisfies round-by-round knowledge soundness with respect to an appropriate state function (to be specified). Each round maintains the security properties compositionally, allowing for modular security analysis.

Each individual round of the sum-check protocol is perfectly complete.

Each individual round of the sum-check protocol is sound with error probability at most \(d / |R|\), where \(d\) is the degree bound and \(|R|\) is the size of the field.

The virtual sum-check round protocol is knowledge sound.

The virtual sum-check round protocol is round-by-round sound.

The virtual sum-check round protocol is sound.