3 Proof Systems
3.1 Simple Oracle Reductions
We start by introducing a number of simple oracle reductions.
3.1.1 Polynomial Equality Testing
Context: two univariate polynomials \(P, Q \in \mathbb {F}[X]\) of degree at most \(d\), available as polynomial evaluation oracles
Input relation: \(P = Q\) as polynomials
Protocol type: a single message of type \(\mathbb {F}\) from the verifier to the prover.
Honest prover: does nothing
Honest verifier: checks that \(P(r) = Q(r)\)
Output relation: \(P(r) = Q(r)\)
Extractor: trivial since there is no witness
Completenes: trivial
Round-by-round state function: corresponds precisely to input and output relation
Round-by-round error: \(d / \lvert \mathbb {F} \rvert \)
Round-by-round knowledge soundness: follows from Schwartz-Zippel
To summarize, we have the following judgment:
where \(\mathsf{St}(i) = \begin{cases} \end{cases} P \stackrel{?}{=} Q \text{ if } i = 0 \\ P(r) \stackrel{?}{=} Q(r) \text{ if } i = 1 \end{cases}\)
3.1.2 Batching Polynomial Evaluation Claims
Context: \(n\)-tuple of values \(v = (v_1, \ldots , v_n) \in \mathbb {F}^n\)
Protocol type: one message of type \(\mathbb {F}^k\) from the verifier to the prover, and another message of type \(\mathbb {F}\) from the prover to the verifier
Auxiliary function: a polynomial map \(E : \mathbb {F}^k \to \mathbb {F}^n\)
Honest prover: given \(r \gets \mathbb {F}^k\) from the verifier’s message, computes \(\langle E(r), v\rangle := E(r)_1 \cdot v_1 + \cdots + E(r)_n \cdot v_n\) and sends it to the verifier
Honest verifier: checks that the received value \(v'\) is equal to \(\langle E(r), v\rangle \)
Extractor: trivial since there is no witness
Security: depends on the degree & non-degeneracy of the polynomial map \(E\)
3.2 The Sum-Check Protocol
In this section, we describe the sum-check protocol [ 1 ] in a modular manner, as a running example for our approach to specifying and proving properties of oracle reductions (based on a program logic approach).
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\).
The sum-check protocol is complete.
We now proceed to break down this protocol into individual message, 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:
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\).
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.
The verifier samples and sends a random challenge \(r \gets \mathbb {F}\).
The verifier checks that \(s(0) + s(1) = d\). The predicate on the resulting output context is that \(p(r) = s(r)\).
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 \{ 0, 1\} ^{n - i - 1}} P(r_1, \ldots , r_{i - 1}, X, x)\).
The scalar \(d\) is instantiated as \(c\) 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:
The initial state funtion is the same as the predicate on the initial context, namely that \(p(0) + p(1) = d\).
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.
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)\).
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.