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}|}. \]

An adaptive prover extends the basic prover type with the ability to choose the input statement adaptively based on oracle access. This models stronger adversaries that can choose their statements after seeing some oracle responses.

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

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

A reduction satisfies completeness with error \(\epsilon \geq 0\) and with respect to input relation \(R_{\text{in}}\) and output relation \(R_{\text{out}}\), if for all valid statement-witness pair \((x_{\text{in}}, w_{\text{in}})\) for \(R_{\text{in}}\), the execution between the honest prover and the honest verifier will result in a tuple \(((x_{\text{out}}^P, w_{\text{out}}), x_{\text{out}}^V)\) such that:

• \(R_{\text{out}}(x_{\text{out}}^V, w_{\text{out}}) = \text{True}\) (the output statement-witness pair is valid), and

• \(x_{\text{out}}^P = x_{\text{out}}^V\) (the output statements are the same from both prover and verifier)

except with probability \(\epsilon \).

In an (oracle) reduction, its (oracle) context consists of a statement type, a witness type, and (in the oracle case) an indexed list of oracle statement types.

Currently, we do not abstract out / bundle the context as a separate structure, but rather specifies the types explicitly. This may change in the future.

A context lens combines a statement lens and a witness lens for adapting complete reduction contexts.

A context lens preserves completeness if it maintains relation satisfaction under projection and lifting.

A context lens preserves knowledge soundness if it maintains witness extractability.

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

Given a collection of prover messages and an input statement, the function \(\mathsf{deriveTranscriptFS}\) reconstructs the full protocol transcript up to round \(k\):

This is computed inductively:

• For challenge rounds: Query the Fiat-Shamir oracle with the statement and messages up to that point

• For message rounds: Use the corresponding message from the prover

The result is a complete transcript that includes both prover messages and verifier challenges.

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

For a protocol specification \(\mathsf{pSpec}\) and input statement type \(\mathsf{StmtIn}\), the Fiat-Shamir challenge oracle interface for the \(i\)-th challenge is defined as follows:

• Query type: \(\mathsf{StmtIn}\times \mathsf{pSpec}.\mathsf{MessagesUpTo}\; i.\mathsf{val}.\mathsf{castSucc}\)

• Response type: \(\mathsf{pSpec}.\mathsf{Challenge}\; i\)

• Oracle behavior: Returns the challenge (which is determined by the random oracle)

The query consists of the input statement and all prover messages sent up to (but not including) round \(i\).

The Fiat-Shamir oracle specification for a protocol \(\mathsf{pSpec}\) with input statement type \(\mathsf{StmtIn}\) is:

where for each challenge index \(i\), the oracle domain is \(\mathsf{StmtIn}\times \mathsf{pSpec}.\mathsf{MessagesUpTo}\; i.\mathsf{val}.\mathsf{castSucc}\) and the range is \(\mathsf{pSpec}.\mathsf{Challenge}\; i\).

This specification defines a family of oracles, one for each challenge round, that deterministically computes challenges based on the statement and messages up to that round.

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.

To actually run oracle computations, we need a way to handle (or implement) the oracle queries. An oracle implementation consists a mapping from oracle queries to values in another monad. Depending on the monad, this may allow for various interpretations of the oracle queries.

A reduction satisfies (straightline) knowledge soundness with error \(\epsilon \geq 0\) and with respect to input relation \(R_{\text{in}}\) and output relation \(R_{\text{out}}\) if:

• there exists a straightline extractor \(E\), such that

• for all input statement \(x_{\text{in}}\), witness \(w_{\text{in}}\), and (malicious) prover,

• if the execution with the honest verifier results in a pair \((x_{\text{out}}, w_{\text{out}})\),

• and the extractor produces some \(w'_{\text{in}}\),

then the probability that \((x_{\text{in}}, w'_{\text{in}})\) is not valid for \(R_{\text{in}}\) and yet \((x_{\text{out}}, w_{\text{out}})\) is valid for \(R_{\text{out}}\) is at most \(\epsilon \).

A (straightline) extractor for knowledge soundness is a deterministic algorithm that takes in the output public context after executing the oracle reduction, the side information (i.e. log of oracle queries from the malicious prover) observed during execution, and outputs the witness for the input context.

Note that since we assume the context is append-only, and we append only the public (or oracle) messages obtained during protocol execution, it follows that the witness stays the same throughout the execution.

A knowledge state function for a verifier, with respect to input relation \(R_{\text{in}}\), output relation \(R_{\text{out}}\), and intermediate witness types, extends the basic state function to track witness validity throughout the protocol execution. This is used to define round-by-round knowledge soundness.

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

Using the simulation framework, we can add logging and caching behaviors to oracle queries:

• Logging records all queries made during a computation

• Caching remembers query responses and reuses them for repeated queries

These are implemented as special cases of simulation oracles.

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

A round-by-round extractor is monotone if its success probability on a given query log is the same as the success probability on any extension of that query log.

An extractor is monotone if its success probability on a given query log is the same as the success probability on any extension of that query log. This property ensures that the extractor’s performance does not degrade when given more information.

An oracle computation represents a program that can make oracle queries. It can:

• Return a pure value without making any queries (via pure)

• Make an oracle query and continue with the response (via queryBind)

• Signal failure (via failure)

The formal implementation uses a free monad on the inductive type of oracle queries wrapped in an option monad transformer (i.e. OptionT(FreeMonad(OracleQuery spec))).

For oracle reductions, we additionally need lenses for oracle statements that can simulate oracle access between contexts.

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

An oracle interface for an underlying data type \(\mathsf{D}\) consists of the following:

• A type \(\mathsf{Q}\) for queries to the oracle,

• A type \(\mathsf{R}\) for responses from the oracle,

• A function \(\mathsf{oracle} : \mathsf{D} \to \mathsf{Q} \to \mathsf{R}\) that specifies the oracle’s behavior given the underlying data and a query.

An oracle prover is a prover whose input statement includes the underlying data for oracle statements, and whose output includes oracle statements. Formally, it is a prover with input statement type \(\mathsf{StmtIn}\times (\forall i : \iota _{\mathsf{si}}, \mathsf{OStmtIn}(i))\) and output statement type \(\mathsf{StmtOut}\times (\forall i : \iota _{\mathsf{so}}, \mathsf{OStmtOut}(i))\), where:

• \(\mathsf{OStmtIn}: \iota _{\mathsf{si}} \to \mathsf{Type}\) are the input oracle statement types

• \(\mathsf{OStmtOut}: \iota _{\mathsf{so}} \to \mathsf{Type}\) are the output oracle statement types

An interactive oracle reduction for protocol specification \(\mathsf{pSpec}: \mathsf{ProtocolSpec}(n)\) with oracle interfaces for all prover messages, and oracle specification \(\mathsf{oSpec}\), consists of:

• An oracle prover \(\mathcal{P} : \mathsf{OracleProver}(\mathsf{pSpec}, \mathsf{oSpec}, \mathsf{StmtIn}, \mathsf{WitIn}, \mathsf{StmtOut}, \mathsf{WitOut}, \mathsf{OStmtIn}, \mathsf{OStmtOut})\)

• An oracle verifier \(\mathcal{V} : \mathsf{OracleVerifier}(\mathsf{pSpec}, \mathsf{oSpec}, \mathsf{StmtIn}, \mathsf{StmtOut}, \mathsf{OStmtIn}, \mathsf{OStmtOut})\)

where:

• \(\mathsf{OStmtIn}: \iota _{\mathsf{si}} \to \mathsf{Type}\) are the input oracle statement types with oracle interfaces

• \(\mathsf{OStmtOut}: \iota _{\mathsf{so}} \to \mathsf{Type}\) are the output oracle statement types

The oracle reduction allows the verifier to access prover messages and oracle statements only through specified oracle interfaces, enabling more flexible and composable protocol designs.

Sequential composition extends naturally to oracle reductions by composing the oracle provers and oracle verifiers.

Completeness of an oracle reduction is the same as for non-oracle reductions, but applied to the converted reduction where oracle statements are handled through their interfaces.

The execution of an interactive oracle reduction is similar to a standard reduction but includes logging of oracle queries:

Returns the same outputs as a standard reduction, plus logs of all oracle queries made by both the prover and verifier.

An oracle specification describes a collection of available oracles, each with its own input and output types. Formally, it’s given by an indexed family where each oracle is specified by:

• A domain type (what inputs it accepts)

• A range type (what outputs it can produce)

The indexing allows for potentially infinite collections of oracles, and the specification itself is agnostic to how the oracles actually behave - it just describes their interfaces.

An oracle verifier \(\mathcal{V}\) consists of the following components:

• Verification Logic: A function

  \[ \mathsf{verify} : \mathsf{StmtIn}\to \mathsf{pSpec}.\mathsf{Challenges}\to \mathsf{OracleComp}(\mathsf{oSpec}\mathrel {++_\mathsf {o}} ([\mathsf{OStmtIn}]_\mathsf {o} \mathrel {++_\mathsf {o}} [\mathsf{pSpec}.\mathsf{Message}]_\mathsf {o}), \mathsf{StmtOut}) \]

  that takes the input statement and verifier challenges, and performs oracle queries to the shared oracle, input oracle statements, and prover messages to produce an output statement.

• Output Oracle Embedding: An injective function

  \[ \mathsf{embed} : \iota _{\mathsf{so}} \hookrightarrow \iota _{\mathsf{si}} \oplus \mathsf{pSpec}.\mathsf{MessageIdx} \]

  that specifies how each output oracle statement is derived from either an input oracle statement or a prover message.

• Type Compatibility: A proof term

  \[ \mathsf{hEq} : \forall i : \iota _{\mathsf{so}}, \mathsf{OStmtOut}(i) = \begin{cases} \end{cases} \mathsf{OStmtIn}(j) & \text{if } \mathsf{embed}(i) = \mathsf{inl}(j) \\ \mathsf{pSpec}.\mathsf{Message}(k) & \text{if } \mathsf{embed}(i) = \mathsf{inr}(k) \end{cases} \]

  ensuring that output oracle statement types match their sources.

This design ensures that output oracle statements are always a subset of the available input oracle statements and prover messages.

Knowledge soundness of an oracle verifier is defined by converting it to a standard verifier and applying the standard knowledge soundness definition.

Round-by-round knowledge soundness of an oracle verifier is defined by converting it to a standard verifier and applying the standard round-by-round knowledge soundness definition.

Round-by-round soundness of an oracle verifier is defined by converting it to a standard verifier and applying the standard round-by-round soundness definition.

The execution of an oracle verifier is defined as:

This simulates the oracle access to input oracle statements and prover messages, then executes the verification logic.

Soundness of an oracle verifier is defined by converting it to a standard verifier and applying the standard soundness definition.

An oracle verifier can be converted to a standard verifier through a natural simulation process. The key insight is that while an oracle verifier only has oracle access to certain data (input oracle statements and prover messages), a standard verifier can be given the actual underlying data directly.

The conversion works as follows: when the oracle verifier needs to make an oracle query to some data, the converted verifier can respond to this query immediately using the actual underlying data it possesses. This is accomplished through the OracleInterface type class, which specifies for each data type how to respond to queries given the underlying data.

Specifically, given an oracle verifier \(\mathcal{V}_{\text{oracle}}\):

• The converted verifier \(\mathcal{V}_{\text{oracle}}.\mathsf{toVerifier}\) takes as input both the statement and the actual underlying data for all oracle statements

• When \(\mathcal{V}_{\text{oracle}}\) attempts to query an oracle statement or prover message, the converted verifier uses the corresponding OracleInterface instance to compute the response from the actual data

• The output oracle statements are constructed according to the embedding specification, selecting the appropriate subset of input oracle statements and prover messages

A reduction satisfies perfect completeness if it satisfies completeness with error \(0\). This means that the probability of the reduction outputting a valid statement-witness pair is exactly 1 (instead of at least \(1 - 0\)).

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 145 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\)

We can view oracle computations as probabilistic programs by considering what happens when oracles respond uniformly at random. This gives rise to a probability distribution over possible outputs (including the possibility of failure). The semantics maps each oracle query to a uniform distribution over its possible responses.

A protocol specification for an \(n\)-message (oracle) reduction, is an element of the following type:

In other words, for each step \(i\) of interaction, the protocol specification describes the direction of the message sent in that step, i.e., whether it is from the prover or from the verifier. It also describes the type of that message.

In the oracle setting, we also expect an oracle interface for each message from the prover to the verifier.

Given two protocol specifications \(\mathsf{pSpec}_1 : \mathsf{ProtocolSpec}\ m\) and \(\mathsf{pSpec}_2 : \mathsf{ProtocolSpec}\ n\), their sequential composition is:

Given a protocol spec \(\mathsf{pSpec}: \mathsf{ProtocolSpec}\ n\), we define:

• \(\mathsf{pSpec}.\mathsf{Dir}\ i := (\mathsf{pSpec}\ i).\mathsf{fst}\) extracts the direction of the \(i\)-th message.

• \(\mathsf{pSpec}.\mathsf{Type}\ i := (\mathsf{pSpec}\ i).\mathsf{snd}\) extracts the type of the \(i\)-th message.

• \(\mathsf{pSpec}.\mathsf{MessageIdx}:= \{ i : \mathsf{Fin}\ n \mathbin {/\! /}\mathsf{pSpec}.\mathsf{Dir}\ i = \mathsf{P \! \! \rightarrow \! \! V}\} \) is the subtype of indices corresponding to prover messages.

• \(\mathsf{pSpec}.\mathsf{ChallengeIdx}:= \{ i : \mathsf{Fin}\ n \mathbin {/\! /}\mathsf{pSpec}.\mathsf{Dir}\ i = \mathsf{V \! \! \rightarrow \! \! P}\} \) is the subtype of indices corresponding to verifier challenges.

• \(\mathsf{pSpec}.\mathsf{Message}\ i := (i : \mathsf{pSpec}.\mathsf{MessageIdx}) \to \mathsf{pSpec}.\mathsf{Type}\ i.\mathsf{val}\) is an indexed family of message types in the protocol.

• \(\mathsf{pSpec}.\mathsf{Challenge}\ i := (i : \mathsf{pSpec}.\mathsf{ChallengeIdx}) \to \mathsf{pSpec}.\mathsf{Type}\ i.\mathsf{val}\) is an indexed family of challenge types in the protocol.

Given a family of protocol specifications \(\mathsf{pSpec}: \forall i : \mathsf{Fin}(m+1), \mathsf{ProtocolSpec}\ (n\ i)\), their composition is:

A prover \(\mathcal{P}\) in a reduction consists of the following components:

• Prover State: A family of types \(\mathsf{PrvState} : \mathsf{Fin}(n+1) \to \mathsf{Type}\) representing the prover’s internal state at each round of the protocol.

• Input Processing: A function

  \[ \mathsf{input} : \mathsf{StmtIn}\to \mathsf{WitIn}\to \mathsf{PrvState}(0) \]

  that initializes the prover’s state from the input statement and witness.

• Message Sending: For each message index \(i : \mathsf{pSpec}.\mathsf{MessageIdx}\), a function

  \[ \mathsf{sendMessage}_i : \mathsf{PrvState}(i.\mathsf{val}.\mathsf{castSucc}) \to \mathsf{OracleComp}(\mathsf{oSpec}, \mathsf{pSpec}.\mathsf{Message}(i) \times \mathsf{PrvState}(i.\mathsf{val}.\mathsf{succ})) \]

  that generates the message and updates the prover’s state.

• Challenge Processing: For each challenge index \(i : \mathsf{pSpec}.\mathsf{ChallengeIdx}\), a function

  \[ \mathsf{receiveChallenge}_i : \mathsf{PrvState}(i.\mathsf{val}.\mathsf{castSucc}) \to \mathsf{pSpec}.\mathsf{Challenge}(i) \to \mathsf{PrvState}(i.\mathsf{val}.\mathsf{succ}) \]

  that updates the prover’s state upon receiving a challenge.

• Output Generation: A function

  \[ \mathsf{output} : \mathsf{PrvState}(\mathsf{Fin}.\mathsf{last}(n)) \to \mathsf{StmtOut}\times \mathsf{WitOut} \]

  that produces the final output statement and witness from the prover’s final state.

Given provers \(P_1 : \mathsf{Prover}\ \mathsf{pSpec}_1\ \mathsf{oSpec}\ \mathsf{StmtIn}_1\ \mathsf{WitIn}_1\ \mathsf{StmtOut}_1\ \mathsf{WitOut}_1\) and \(P_2 : \mathsf{Prover}\ \mathsf{pSpec}_2\ \mathsf{oSpec}\ \mathsf{StmtOut}_1\ \mathsf{WitOut}_1\ \mathsf{StmtOut}_2\ \mathsf{WitOut}_2\), their sequential composition is:

The composed prover works by:

• Running \(P_1\) on the input context to produce an intermediate context

• Using this intermediate context as input to \(P_2\)

• Outputting the final context from \(P_2\)

Given an interactive prover \(P\) for protocol \(\mathsf{pSpec}\), the Fiat-Shamir transformation produces a non-interactive prover:

The transformed prover:

• Has state type that combines the statement with the original prover’s state at round 0, and uses the final state type for subsequent rounds

• On input, stores both the statement and initializes the original prover’s state

• Sends a single message containing all of the original prover’s messages, computed via \(\mathsf{runToRoundFS}\)

• Never receives challenges (since it’s non-interactive)

• Outputs using the original prover’s output function

Given a prover \(P\) for the inner context and a context lens, the lifted prover works by:

• Projecting the outer input to the inner context

• Running the inner prover

• Lifting the output back to the outer context

The modified round processing function for Fiat-Shamir maintains the prover messages (but not challenges) and the input statement throughout execution:

For each round \(j\):

• If \(j\) is a challenge round: Query the Fiat-Shamir oracle with the statement and messages so far, then update the prover state with the received challenge

• If \(j\) is a message round: Generate the message using the prover’s \(\mathsf{sendMessage}\) function and append it to the message history

The key difference from standard execution is that challenges are derived via oracle queries rather than received from an interactive verifier.

The complete execution of a prover is defined as:

Returns the output statement, output witness, and complete transcript.

The execution of a prover up to round \(i : \mathsf{Fin}(n+1)\) is defined inductively:

where \(\mathsf{processRound}\) handles individual rounds by either:

• Verifier Challenge (\(\mathsf{pSpec}.\mathsf{getDir}(j) = \mathsf{V\_ to\_ P}\)): Query for a challenge and update prover state

• Prover Message (\(\mathsf{pSpec}.\mathsf{getDir}(j) = \mathsf{P\_ to\_ V}\)): Generate message via \(\mathsf{sendMessage}\) and update state

Returns the transcript up to round \(i\) and the prover’s state after round \(i\).

The Fiat-Shamir prover execution up to round \(i\) is defined as:

This executes the prover inductively using \(\mathsf{processRoundFS}\), starting from the initial state and accumulating messages and the statement. Returns the messages up to round \(i\), the input statement, and the prover’s final state.

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:

A random oracle is implemented as a caching oracle that uses lazy sampling:

• On first query: generates a uniform random response and caches it

• On repeated queries: returns the cached response

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.

A round-by-round extractor with index \(m\) is given:

• the input statement \(x_{\text{in}}\),

• a partial transcript of length \(m\),

• the prover’s query log

and returns a witness to the statement.

Note that the RBR extractor does not need to take in the output statement or witness.

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}))\)

An interactive reduction for protocol specification \(\mathsf{pSpec}: \mathsf{ProtocolSpec}(n)\) and oracle specification \(\mathsf{oSpec}\) consists of:

• A prover \(\mathcal{P} : \mathsf{Prover}(\mathsf{pSpec}, \mathsf{oSpec}, \mathsf{StmtIn}, \mathsf{WitIn}, \mathsf{StmtOut}, \mathsf{WitOut})\)

• A verifier \(\mathcal{V} : \mathsf{Verifier}(\mathsf{pSpec}, \mathsf{oSpec}, \mathsf{StmtIn}, \mathsf{StmtOut})\)

The reduction establishes a relationship between input relations on \((\mathsf{StmtIn}, \mathsf{WitIn})\) and output relations on \((\mathsf{StmtOut}, \mathsf{WitOut})\) through the interactive protocol defined by \(\mathsf{pSpec}\).

Sequential composition of reductions combines the corresponding provers and verifiers:

Given an interactive reduction \(R\) for protocol \(\mathsf{pSpec}\), the Fiat-Shamir transformation produces a non-interactive reduction:

This transformation simply applies the Fiat-Shamir transformation to both the prover and verifier components of the reduction.

The execution of an interactive reduction consists of running the prover followed by the verifier:

Returns both the prover’s output (statement and witness) and the verifier’s output statement, along with the complete transcript.

A rewinding extractor consists of:

• An extractor state type

• Simulation oracles for challenges and oracle queries for the prover

• A function that runs the extractor with the prover’s oracle interface, allowing for calling the prover multiple times

This allows the extractor to rewind the prover to earlier states and try different challenges.

A protocol with verifier \(\mathcal{V}\) satisfies round-by-round knowledge soundness with respect to input relation \(R_{\text{in}}\), output relation \(R_{\text{out}}\), and error function \(\epsilon : \text{ChallengeIdx} \to \mathbb {R}_{\geq 0}\) if:

• there exists a knowledge state function for the verifier and the languages of the input/output relations,

• there exists a round-by-round extractor,

• for all initial statements,

• for all initial witnesses,

• for all provers,

• for all challenge rounds \(i\),

the probability that:

• the extracted witness does not satisfy the input relation

• the state function is false for the partial transcript output by the prover

• the state function is true for the partial transcript appended by next challenge (chosen randomly)

is at most \(\epsilon (i)\).

A protocol with verifier \(\mathcal{V}\) satisfies round-by-round soundness with respect to input language \(L_{\text{in}}\), output language \(L_{\text{out}}\), and error function \(\epsilon : \text{ChallengeIdx} \to \mathbb {R}_{\geq 0}\) if:

• there exists a state function for the verifier and the input/output languages, such that

• for all initial statements \(x_{\text{in}} \notin L_{\text{in}}\),

• for all initial witnesses,

• for all provers,

• for all challenge rounds \(i\),

the probability that:

• the state function is false for the partial transcript output by the prover

• the state function is true for the partial transcript appended by next challenge (chosen randomly)

is at most \(\epsilon (i)\).

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})\)

We can simulate complex oracles using simpler ones by providing a translation mechanism. A simulation oracle specifies how to implement queries in one specification using computations in another specification, possibly maintaining additional state information during the simulation.

A simulator consists of:

• Oracle simulation capabilities for the shared oracles

• A prover simulation function that takes an input statement and produces a transcript

The simulator should have programming access to the shared oracles and be able to generate transcripts that are indistinguishable from real protocol executions.

A reduction satisfies soundness with error \(\epsilon \geq 0\) and with respect to input language \(L_{\text{in}} \subseteq \text{Statement}_{\text{in}}\) and output language \(L_{\text{out}} \subseteq \text{Statement}_{\text{out}}\) if:

• for all (malicious) provers with arbitrary types for witness types,

• for all arbitrary input witness,

• for all input statement \(x_{\text{in}} \notin L_{\text{in}}\),

the execution between the prover and the honest verifier will result in an output statement \(x_{\text{out}} \in L_{\text{out}}\) with probability at most \(\epsilon \).

State-restoration knowledge soundness extends state-restoration soundness with the requirement that there exists a straightline extractor that can recover valid witnesses from any state-restoration prover that convinces the verifier.

Note: This definition is currently under development in the Lean formalization.

A state-restoration prover is a modified prover that has query access to challenge oracles that can return the \(i\)-th challenge, for all \(i\), given the input statement and the transcript up to that point.

It takes in the input statement and witness, and outputs a full transcript of interaction, along with the output statement and witness.

This models adversaries in the state-restoration setting where challenges can be queried programmably.

State-restoration soundness is a security notion where the adversarial prover has access to challenge oracles that can return the \(i\)-th challenge for any round \(i\), given the input statement and the transcript up to that point. This models stronger adversaries in the programmable random oracle model or when challenges can be computed deterministically.

A verifier satisfies state-restoration soundness if for all input statements not in the language, for all witnesses, and for all state-restoration provers, the probability that the verifier outputs a statement in the output language is bounded by the soundness error.

Note: This definition is currently under development in the Lean formalization.

A (deterministic) state function for a verifier, with respect to input language \(L_{\text{in}}\) and output language \(L_{\text{out}}\), consists of a function that maps partial transcripts to boolean values, satisfying:

• For all input statements not in the language, the state function is false for the empty transcript

• If the state function is false for a partial transcript, and the next message is from the prover to the verifier, then the state function is also false for the new partial transcript regardless of the message

• If the state function is false for a full transcript, the verifier will not output a statement in the output language

A statement lens between outer context types \((\mathsf{StmtIn}_{\mathsf{outer}}, \mathsf{StmtOut}_{\mathsf{outer}})\) and inner context types \((\mathsf{StmtIn}_{\mathsf{inner}}, \mathsf{StmtOut}_{\mathsf{inner}})\) consists of:

• \(\mathsf{projStmt}: \mathsf{StmtIn}_{\mathsf{outer}} \to \mathsf{StmtIn}_{\mathsf{inner}}\) (projection to inner context)

• \(\mathsf{liftStmt}: \mathsf{StmtIn}_{\mathsf{outer}} \times \mathsf{StmtOut}_{\mathsf{inner}} \to \mathsf{StmtOut}_{\mathsf{outer}}\) (lifting back to outer context)

For round-by-round soundness, we need a slightly relaxed soundness condition.

A statement lens preserves soundness if it maps invalid statements to invalid statements.

A straightline, deterministic, non-oracle-querying extractor takes in:

• the output witness \(w_{\text{out}}\),

• the initial statement \(x_{\text{in}}\),

• the IOR transcript \(\tau \),

• the query logs from the prover and verifier

and returns a corresponding initial witness \(w_{\text{in}}\).

Note that the extractor does not need to take in the output statement, since it can be derived via re-running the verifier on the initial statement, the transcript, and the verifier’s query log.

This form of extractor suffices for proving knowledge soundness of most hash-based IOPs.

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

Given protocol specification \(\mathsf{pSpec}: \mathsf{ProtocolSpec}\ n\), we define:

• A transcript up to round \(k : \mathsf{Fin}\ (n + 1)\) is an element of type

  \[ \mathsf{Transcript}\ k\ \mathsf{pSpec}:= (i : \mathsf{Fin}\ k) \to \mathsf{pSpec}.\mathsf{Type}\ (\uparrow i : \mathsf{Fin}\ n) \]

  where \(\uparrow i : \mathsf{Fin}\ n\) denotes casting \(i : \mathsf{Fin}\ k\) to \(\mathsf{Fin}\ n\) (valid since \(k \leq n + 1\)).

• A full transcript is \(\mathsf{FullTranscript}\ \mathsf{pSpec}:= (i : \mathsf{Fin}\ n) \to \mathsf{pSpec}.\mathsf{Type}\ i\).

• The type of all messages from prover to verifier is

  \[ \mathsf{pSpec}.\mathsf{Messages}:= \prod _{i : \mathsf{pSpec}.\mathsf{MessageIdx}} \mathsf{pSpec}.\mathsf{Message}\ i \]

• The type of all challenges from verifier to prover is

  \[ \mathsf{pSpec}.\mathsf{Challenges}:= \prod _{i : \mathsf{pSpec}.\mathsf{ChallengeIdx}} \mathsf{pSpec}.\mathsf{Challenge}\ i \]

Given full transcripts \(T_1 : \mathsf{FullTranscript}\ \mathsf{pSpec}_1\) and \(T_2 : \mathsf{FullTranscript}\ \mathsf{pSpec}_2\), their sequential composition is:

A verifier \(\mathcal{V}\) in a reduction is specified by a single function:

This function takes the input statement and the complete transcript of the protocol interaction, and performs an oracle computation (potentially querying the shared oracle \(\mathsf{oSpec}\)) to produce an output statement.

The verifier is assumed to be public-coin, meaning it only sends uniformly random challenges and uses no other randomness beyond what is provided by the shared oracle.

Given verifiers \(V_1 : \mathsf{Verifier}\ \mathsf{pSpec}_1\ \mathsf{oSpec}\ \mathsf{StmtIn}_1\ \mathsf{StmtOut}_1\) and \(V_2 : \mathsf{Verifier}\ \mathsf{pSpec}_2\ \mathsf{oSpec}\ \mathsf{StmtOut}_1\ \mathsf{StmtOut}_2\), their sequential composition is:

The composed verifier first runs \(V_1\) on the first part of the transcript, then runs \(V_2\) on the second part using the intermediate statement from \(V_1\).

Given an interactive verifier \(V\) for protocol \(\mathsf{pSpec}\), the Fiat-Shamir transformation produces a non-interactive verifier:

The transformed verifier:

• Takes the input statement and a proof consisting of all prover messages

• Derives the full transcript using \(\mathsf{deriveTranscriptFS}\)

• Runs the original verifier’s verification logic on the reconstructed transcript

The execution of a verifier is simply the application of its verification function:

This takes the input statement and full transcript, and returns the output statement via an oracle computation.

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

A witness lens between outer witness types \((\mathsf{WitIn}_{\mathsf{outer}}, \mathsf{WitOut}_{\mathsf{outer}})\) and inner witness types \((\mathsf{WitIn}_{\mathsf{inner}}, \mathsf{WitOut}_{\mathsf{inner}})\) consists of:

• \(\mathsf{projWit}: \mathsf{WitIn}_{\mathsf{outer}} \to \mathsf{WitIn}_{\mathsf{inner}}\) (projection to inner context)

• \(\mathsf{liftWit}: \mathsf{WitIn}_{\mathsf{outer}} \times \mathsf{WitOut}_{\mathsf{inner}} \to \mathsf{WitOut}_{\mathsf{outer}}\) (lifting back to outer context)

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

If reductions \(R_1\) and \(R_2\) satisfy completeness with compatible relations and respective errors \(\epsilon _1\) and \(\epsilon _2\), then their sequential composition \(R_1.\mathsf{append}\ R_2\) satisfies completeness with error \(\epsilon _1 + \epsilon _2\).

Let \(R\) be an interactive reduction with completeness error \(\epsilon \) with respect to input relation \(R_{\text{in}}\) and output relation \(R_{\text{out}}\). Then the Fiat-Shamir transformed reduction \(R.\mathsf{fiatShamir}\) also satisfies completeness with error \(\epsilon \) with respect to the same relations.

Formally: \(R.\mathsf{completeness} \; R_{\text{in}} \; R_{\text{out}} \; \epsilon \to (R.\mathsf{fiatShamir}).\mathsf{completeness} \; R_{\text{in}} \; R_{\text{out}} \; \epsilon \)

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)\),

If verifiers \(V_1\) and \(V_2\) satisfy knowledge soundness with respective errors \(\epsilon _1\) and \(\epsilon _2\), then their sequential composition satisfies knowledge soundness with error \(\epsilon _1 + \epsilon _2\).

Knowledge soundness with knowledge error \(\epsilon {\lt} 1\) implies soundness with the same soundness error \(\epsilon \), and for the corresponding input and output languages.

If a reduction satisfies completeness and the context lens is completeness-preserving, then the lifted reduction also satisfies completeness.

If a verifier satisfies knowledge soundness and the context lens is knowledge soundness-preserving, then the lifted verifier also satisfies knowledge soundness.

If a verifier satisfies round-by-round knowledge soundness and the context lens is knowledge soundness-preserving, then the lifted verifier also satisfies round-by-round knowledge soundness.

If a verifier satisfies round-by-round soundness and the statement lens is RBR soundness-preserving, then the lifted verifier also satisfies round-by-round soundness.

If a verifier satisfies soundness and the statement lens is soundness-preserving, then the lifted verifier also satisfies soundness.

If reductions \(R_1\) and \(R_2\) satisfy perfect completeness with compatible relations, then their sequential composition also satisfies perfect completeness.

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} \]

If verifiers \(V_1\) and \(V_2\) satisfy round-by-round knowledge soundness, then their sequential composition also satisfies round-by-round knowledge soundness.

Round-by-round knowledge soundness with error function \(\epsilon \) implies knowledge soundness with error \(\sum _i \epsilon (i)\), where the sum is over all challenge rounds \(i\).

Round-by-round knowledge soundness with error function \(\epsilon \) implies round-by-round soundness with the same error function \(\epsilon \).

If verifiers \(V_1\) and \(V_2\) satisfy round-by-round soundness, then their sequential composition also satisfies round-by-round soundness.

Round-by-round soundness with error function \(\epsilon \) implies soundness with error \(\sum _i \epsilon (i)\), where the sum is over all challenge rounds \(i\).

If verifiers \(V_1\) and \(V_2\) satisfy soundness with respective errors \(\epsilon _1\) and \(\epsilon _2\), then their sequential composition satisfies soundness with error \(\epsilon _1 + \epsilon _2\).

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.