3 Proof Systems

3.1 Simple Oracle Reductions

We start by introducing a number of simple oracle reductions that serve as fundamental building blocks for more complex proof systems. These components can be composed together to construct larger protocols.

3.1.1 Trivial Reduction

The simplest possible oracle reduction is one that performs no computation at all. Both the prover and verifier simply pass their inputs through unchanged. While seemingly trivial, this reduction serves as an important identity element for composition and provides a base case for lifting and lens operations.

The oracle version of DoNothing handles oracle statements by passing them through unchanged as well. The prover receives both non-oracle and oracle statements as input, and outputs them in the same form to the verifier.

3.1.2 Sending the Witness

A fundamental building block in many proof systems is the ability for the prover to transmit witness information to the verifier. The SendWitness reduction provides this functionality in both direct and oracle settings.

In the oracle setting, we consider two variants:

3.1.3 Oracle Equality Testing

One of the most fundamental oracle reductions is testing whether two oracles of the same type are equal. This is achieved through random sampling from the query space.

The key security property of RandomQuery depends on the notion of oracle distance:

We mention two special cases of RandomQuery that are useful for specific applications.

Polynomial Equality Testing

A common application of oracle reductions is testing equality between polynomial oracles. This is a specific instance of the RandomQuery reduction applied to polynomial evaluation oracles.

The state function for this reduction corresponds precisely to the input and output relations, transitioning from checking polynomial equality to checking evaluation equality at the sampled point.

Batching Polynomial Evaluation Claims

Another important building block is the ability to batch multiple polynomial evaluation claims into a single check using random linear combinations.

TODO: express this as a lifted version of \(\mathsf{RandomQuery}\) over a virtual polynomial whose variables are the random linear combination coefficients.

3.1.4 Sending a Claim

The SendClaim reduction enables a prover to transmit a claim (oracle statement) to the verifier, who then verifies a relationship between the original and transmitted claims.

3.1.5 Claim Reduction

A fundamental building block for constructing complex proof systems is the ability to locally reduce one type of claim to another. The ReduceClaim reduction provides this functionality through mappings between statement and witness types.

3.1.6 Claim Verification

Another essential building block is the ability to verify that a given predicate holds for a statement without requiring additional witness information.

3.2 The Sum-Check Protocol

This section documents our formalization of the sum-check protocol. We first describe the sum-check protocol as it is typically described in the literature, and then present a modular description that maximally relies on our general oracle reduction framework.

3.2.1 Standard Description

Protocol Parameters

The sum-check protocol is parameterized by the following:

• \(R\): the underlying ring (for soundness, required to be finite and an integral domain)

• \(n \in \mathbb {N}\): the number of variables (and the number of rounds for the protocol)

• \(d \in \mathbb {N}\): the individual degree bound for the polynomial

• \(\mathcal{D}: \{ 0, 1, \ldots , m-1\} \hookrightarrow R\): the set of \(m\) evaluation points for each variable, represented as an injection. The image of \(\mathcal{D}\) as a finite subset of \(R\) is written as \(\text{Image}(\mathcal{D})\).

• \(\mathcal{O}\): the set of underlying oracles (e.g., random oracles) that may be needed for other reductions. However, the sum-check protocol itself does not use any oracles.

Input and Output Statements

For the standard description of the sum-check protocol, we specify the complete input and output data:

Input Statement.

The claimed sum \(T \in R\).

Input Oracle Statement.

The polynomial \(P \in R[X_0, X_1, \ldots , X_{n-1}]_{\leq d}\) of \(n\) variables with bounded individual degrees \(d\).

Input Witness.

None (the unit type).

Input Relation.

The sum-check relation:

Output Statement.

The claimed evaluation \(e \in R\) and the challenge vector \((r_0, r_1, \ldots , r_{n-1}) \in R^n\).

Output Oracle Statement.

The same polynomial \(P \in R[X_0, X_1, \ldots , X_{n-1}]_{\leq d}\).

Output Witness.

None (the unit type).

Output Relation.

The evaluation relation:

Protocol Description

The sum-check protocol proceeds in \(n\) rounds of interaction between the prover and verifier. The protocol reduces the claim that a multivariate polynomial \(P\) sums to a target value \(T\) over the domain \((\text{Image}(\mathcal{D}))^n\) to the claim that \(P\) evaluates to a specific value \(e\) at a random point \((r_0, r_1, \ldots , r_{n-1})\).

In each round, the prover sends a univariate polynomial of bounded degree, and the verifier responds with a random challenge. The verifier performs consistency checks by querying the polynomial oracle at specific evaluation points. After \(n\) rounds, the protocol terminates with an output statement asserting that \(P(r_0, r_1, \ldots , r_{n-1}) = e\), where the challenges \((r_0, r_1, \ldots , r_{n-1})\) are the random values chosen by the verifier during the protocol execution.

The protocol is described as an oracle reduction, where the polynomial \(P\) is accessed only through evaluation queries rather than being explicitly represented.

Security Properties

We prove the following security properties for the sum-check protocol:

Implementation Notes

Our formalization includes several important implementation considerations:

Oracle Reduction Level.

This description of the sum-check protocol stays at the oracle reduction level, describing the protocol before being compiled with concrete cryptographic primitives such as polynomial commitment schemes for \(P\). The oracle model allows us to focus on the logical structure and security properties of the protocol without being concerned with the specifics of how polynomial evaluations are implemented or verified.

Abstract Protocol Description.

The protocol description above does not consider implementation details and optimizations that would be necessary in practice. For instance, we do not address computational efficiency, concrete polynomial representations, or specific algorithms for polynomial evaluation. This abstraction allows us to establish the fundamental security properties that any concrete implementation must preserve.

Degree Constraints.

To represent sum-check as a series of Interactive Oracle Reductions (IORs), we implicitly constrain the degree of the polynomials via using subtypes such as \(R[X]_{\leq d}\) and appropriate multivariate polynomial degree bounds. This is necessary because the oracle verifier only gets oracle access to evaluating the polynomials, but does not see the polynomials in the clear.

Polynomial Commitments.

When this protocol is compiled to an interactive proof (rather than an oracle reduction), the corresponding polynomial commitment schemes will enforce that the declared degree bounds hold, by letting the (non-oracle) verifier perform explicit degree checks.

Formalization Alignment.

TODO: Align the sum-check protocol formalization in Lean to use \(n\) variables and \(n\) rounds (as in this standard description) rather than \(n+1\) variables and \(n+1\) rounds. This should be achievable by refactoring the current implementation to better match the standard presentation.

Future Extensions

Several generalizations are considered for future work:

• Variable Degree Bounds: Generalize to \(d : \{ 0, 1, \ldots , n+1\} \to \mathbb {N}\) and \(\mathcal{D} : \{ 0, 1, \ldots , n+1\} \to (\{ 0, 1, \ldots , m-1\} \hookrightarrow R)\), allowing different degree bounds and summation domains for each variable.

• Restricted Challenge Domains: Generalize the challenges to come from suitable subsets of \(R\) (e.g., subtractive sets), rather than the entire domain. This modification is used in lattice-based protocols.

• Module-based Sum-check: Extend to sum-check over modules instead of just rings. This would require extending multivariate polynomial evaluation to modules, defining something like \(\text{evalModule} : (R^n \to M) \to R[X_0, \ldots , X_{n-1}] \to M\) where \(M\) is an \(R\)-module.

The sum-check protocol, as described in the original paper and many expositions thereafter, is a protocol to reduce the claim that

where \(P\) is an \(n\)-variate polynomial of certain individual degree bounds, and \(c\) is some field element, to the claim that

for some claimed value \(v\) (derived from the protocol transcript), where \(r\) is a vector of random challenges from the verifier sent during the protocol.

In our language, the initial context of the sum-check protocol is the pair \((P, c)\), where \(P\) is an oracle input and \(c\) is public. The protocol proceeds in \(n\) rounds of interaction, where in each round \(i\) the prover sends a univariate polynomial \(s_i\) of bounded degree and the verifier sends a challenge \(r_i \gets \mathbb {F}\). The honest prover would compute

and the honest verifier would check that \(s_i(0) + s_i(1) = s_{i - 1}(r_{i - 1})\), with the convention that \(s_0(r_0) = c\).

3.2.2 Modular Description

Round-by-Round Analysis

Our modular approach breaks down the sum-check protocol into individual rounds, each of which can be analyzed as a two-message Interactive Oracle Reduction. This decomposition allows us to prove security properties compositionally and provides a more granular understanding of the protocol’s structure.

Round-Specific Statements.

For the \(i\)-th round, where \(i \in \{ 0, 1, \ldots , n\} \), the statement contains:

• \(\text{target} \in R\): the target value for sum-check at this round

• \(\text{challenges} \in R^i\): the list of challenges sent from the verifier to the prover in previous rounds

The oracle statement remains the same polynomial \(P \in R[X_0, X_1, \ldots , X_{n-1}]_{\leq d}\).

Round-Specific Relations.

The sum-check relation for the \(i\)-th round checks that:

Note that when \(i = n\), this becomes the output statement of the sum-check protocol, checking that \(P(\text{challenges}) = \text{target}\).

Individual Round Protocol

For \(i = 0, 1, \ldots , n-1\), the \(i\)-th round of the sum-check protocol consists of the following:

Step 1: Prover’s Message.

The prover sends a univariate polynomial \(p_i \in R[X]_{\leq d}\) of degree at most \(d\). If the prover is honest, then:

Here, \(P(\text{challenges}_0, \ldots , \text{challenges}_{i-1}, X, x)\) is the polynomial \(P\) evaluated at the concatenation of:

• the prior challenges \(\text{challenges}_0, \ldots , \text{challenges}_{i-1}\)

• the \(i\)-th variable as the new indeterminate \(X\)

• the remaining values \(x \in (\text{Image}(\mathcal{D}))^{n-i}\)

In the oracle protocol, this polynomial \(p_i\) is turned into an oracle for which the verifier can query evaluations at arbitrary points.

Step 2: Verifier’s Challenge.

The verifier sends the \(i\)-th challenge \(r_i\) sampled uniformly at random from \(R\).

Step 3: Verifier’s Check.

The (oracle) verifier performs queries for the evaluations of \(p_i\) at all points in \(\text{Image}(\mathcal{D})\), and checks that:

If the check fails, the verifier outputs \(\texttt{failure}\). Otherwise, it outputs a statement for the next round as follows:

• \(\text{target}\) is updated to \(p_i(r_i)\)

• \(\text{challenges}\) is updated to the concatenation of the previous challenges and \(r_i\)

Single Round Security Analysis

Virtual Protocol Decomposition

We now proceed to break down this protocol into individual messages, and then specify the predicates that should hold before and after each message is exchanged.

First, it is clear that we can consider each round in isolation. In fact, each round can be seen as an instantiation of the following simpler "virtual" protocol:

The reason why this simpler protocol is related to a sum-check round is that we can emulate the simpler protocol using variables in the context at the time:

• The univariate polynomial \(p\) is instantiated as \(\sum _{x \in (\text{Image}(\mathcal{D}))^{n - i - 1}} P(r_0, \ldots , r_{i - 1}, X, x)\).

• The scalar \(d\) is instantiated as \(T\) if \(i = 0\), and as \(s_{i - 1}(r_{i - 1})\) otherwise.

It is "clear" that the simpler protocol is perfectly complete. It is sound (and since there is no witness, also knowledge sound) since by the Schwartz-Zippel Lemma, the probability that \(p \ne s\) and yet \(p(r) = s(r)\) for a random challenge \(r\) is at most the degree of \(p\) over the size of the field.

Note that there is no witness, so knowledge soundness follows trivially from soundness.

Moreover, we can define the following state function for the simpler protocol

Seen in this light, it should be clear that the simpler protocol satisfies round-by-round soundness.

In fact, we can break down this simpler protocol even more: consider the two sub-protocols that each consists of a single message. Then the intermediate state function is the same as the predicate on the intermediate context, and is given in a "strongest post-condition" style where it incorporates the verifier’s check along with the initial predicate. We can also view the final state function as a form of "canonical" post-condition, that is implied by the previous predicate except with small probability.

3.3 The Spartan Protocol

3.3.1 Preliminaries

The Spartan protocol is designed to prove the satisfiability of Rank-1 Constraint System (R1CS). An R1CS instance is defined by a set of matrices \((A, B, C)\) over a field \(\mathbb {F}\) (more generally the definition makes sense over any semiring \(\mathsf{R}\)), and it is satisfied by a public input \(x\) and a private witness \(w\) if the combined vector \(z = (x, w)\) satisfies the relation:

where \(\circ \) denotes the Hadamard (entry-wise) product. Our formalization follows the definition in ArkLib/ProofSystem/ConstraintSystem/R1CS.lean.

3.3.2 Description in Paper

Figure 3.1 is the description of the Spartan protocol from the original paper  [ 10 ] . Note that in this section, we only formalize the Polynomial IOP (PIOP) aspect of Spartan. In the PIOP model, the prover does not commit to polynomials using a Polynomial Commitment Scheme (PCS). Instead, the verifier is given oracle access to the polynomials. Therefore, steps involving ‘PCS.Setup‘, ‘PCS.Commit‘, and ‘PCS.Eval‘ are replaced by simple oracle interactions.

After stripping away the polynomial commitment scheme, the protocol has the following structure:

Setup:

This step is part of the polynomial commitment scheme and is not part of the PIOP we formalize.

Interaction:

The interaction is between a prover \(\mathcal{P}\) with witness \(w\) and a verifier \(\mathcal{V}\) with public inputs \((\mathbb {F}, A, B, C, \text{io}, m, n)\).

1. \(\mathcal{P}\): Sends oracle access to the multilinear extension of the witness, \(\tilde{w}\), to \(\mathcal{V}\). In the original paper, this is a commitment \((C,S) \leftarrow \text{PC.Commit}(\text{pp}, \tilde{w})\).

2. \(\mathcal{V}\): Samples a random challenge \(\tau \in \mathbb {F}^{\log m}\) and sends it to \(\mathcal{P}\).

3. Let \(T_1 = 0\), \(\mu _1 = \log m\), \(\ell _1 = 3\). These are parameters for the first sum-check protocol.

4. \(\mathcal{V}\): Samples a random challenge \(r_x \in \mathbb {F}^{\mu _1}\).

5. Sum-check#1. A sum-check protocol is executed. The verifier receives the claimed evaluation \(e_x\). The prover of the sum-check has oracle access to a polynomial \(G_{io, \tau }\), and the verifier has oracle access to \(r_x\). The parameters for this sub-protocol are \((\mu _1, \ell _1, T_1)\).

6. \(\mathcal{P}\): Computes evaluations \(v_A = \tilde{A}(r_x)\), \(v_B = \tilde{B}(r_x)\), \(v_C = \tilde{C}(r_x)\) and sends them to \(\mathcal{V}\). \(\tilde{A}, \tilde{B}, \tilde{C}\) are multilinear extensions of the matrices \(A, B, C\).

7. \(\mathcal{V}\): Aborts if \(e_x \neq (v_A \cdot v_B - v_C) \cdot \tilde{\text{eq}}(r_x, \tau )\). This is the verifier’s check for the first sum-check.

8. \(\mathcal{V}\): Samples random challenges \(r_A, r_B, r_C \in \mathbb {F}\) and sends them to \(\mathcal{P}\).

9. Let \(T_2 = r_A \cdot v_A + r_B \cdot v_B + r_C \cdot v_C\), \(\mu _2 = \log n\), \(\ell _2 = 2\). These are parameters for the second sum-check protocol. Note: The image states \(\mu _2 = \log m\), which is likely a typo and should be \(\log n\).

10. \(\mathcal{V}\): Samples a random challenge \(r_y \in \mathbb {F}^{\mu _2}\).

11. Sum-check#2. Another sum-check protocol is executed. The verifier receives the claimed evaluation \(e_y\).

12. \(\mathcal{P}\): Computes \(v \leftarrow \tilde{w}(r_y[1..])\) and sends \(v\) to \(\mathcal{V}\).

13. This step involves a polynomial commitment evaluation proof. In our PIOP formalization, this check is not needed as the verifier has direct oracle access to \(\tilde{w}\).

14. \(\mathcal{V}\): This step is part of the evaluation proof check, so it is omitted.

15. \(\mathcal{V}\): Computes \(v_Z \leftarrow (1 - r_y[0]) \cdot \tilde{w}(r_y[1..]) + r_y[0] \cdot \widetilde{(\text{io}, 1)}(r_y[1..])\). This reconstructs the evaluation of the combined input-witness vector polynomial \(\tilde{z}\).

16. \(\mathcal{V}\): Queries oracles for \(\tilde{A}, \tilde{B}, \tilde{C}\) at \((r_x, r_y)\) to get \(v_1, v_2, v_3\).

17. \(\mathcal{V}\): Aborts if \(e_y \neq (r_A \cdot v_1 + r_B \cdot v_2 + r_C \cdot v_3) \cdot v_Z\). This is the final check.

18. \(\mathcal{V}\): Outputs 1.

3.3.3 Formalization using IOR Composition

3.4 Stir

3.4.1 Tools for Reed Solomon codes

Random linear combination as a proximity generator

Univariate Function Quotienting

In the following, we start by defining the quotient of a univariate function.

Next we define the polynomial quotient operator, which quotients a polynomial relative to its output on evaluation points. The polynomial quotient is a polynomial of lower degree.

The following lemma, implicit in prior works, shows that if the function is “quotiented by the wrong value”, then its quotient is far from low-degree.

Out of domain sampling

Folding univariate functions

STIR relies on \(k\)-wise folding of functions and polynomials - this is similar to prior works, although presented in a slightly different form. As shown below, folding a function preserves proximity from the Reed-Solomon code with high probability. The folding operator is based on the following fact, decomposing univariate polynomials into bivariate ones.

Below, we define folding of a polynomial followed by folding of a function.

The following lemma shows that the distance of a function is preserved under folding. If a functions \(f\) has distance \(\delta \) to a Reed-Solomon code then, with high probability over the choice of folding randomness, its folding also has a distance of \(\delta \) to the “\(k\)-wise folded” Reed-Solomon code.

Combine functions of varying degrees

We show a new method for combining functions of varying degrees with minimal proximity require- ments using geometric sums. We begin by recalling a fact about geometric sums.

Below it is shown that combining multiple polynomials of varying degrees can be done as long as the proximity error is bounded by \((\min {\{ 1-{\mathsf{B}}^*(\rho ),1-\rho -1/|\mathcal{L}|\} })\).

3.4.2 Stir Main theorems

3.5 Whir

3.5.1 Tools for Reed Solomon codes

Mutual Correlated Agreement as a Proximity Generator

Mutual correlated agreement preserves list decoding

Folding univariate functions

Block relative distance

Note that \(\Delta _{r}(\mathcal{C}, 0, 0, f, g) = \Delta (f, g)\) for any \(\mathcal{C}\). We define the block list decoding of a codeword.

Folding preserves list decoding

3.6 The Spartan Protocol

3.7 The Ligero Polynomial Commitment Scheme