The Sumcheck
The sumcheck protocol is perhaps our single most important building block. We will find occasion to use it constantly throughout the blueprint ahead. This protocol is originally due to Lund, Fortnow, Karloff, and Nisan [LFKN92].
To explain the sumcheck, we fix a multivariate polynomial, say (generally not multilinear). The sumcheck is devoted to a task that might seem odd at first: learning the sum of the respective values that takes over the boolean cube . Mathematically, this looks like checking the claim
Indeed, is an -variate polynomial. Thus, for any tuple in , and even in , we can get a value . The sumcheck is about the particular values takes on a subset of its domain: namely, on inputs which happen to have boolean components. In particular, we want to learn the sum of all of those.
Of course, the verifier can always learn this sum by hand—by doing on the order of work. Our goal will be to achieve this task succinctly for the verifier—using an amount of work just polynomial in .
Why?
What's the point of such an odd task? In fact, it's one of the "magic" aspects of multilinear SNARKs that many disparate tasks can ultimately be reformulated as problems of precisely this form—i.e., of learning the sum of some polynomial's values over the cube. We'll defer the full explanation on this, but one of the most canonical examples is the zerocheck protocol. In that protocol, we have a totally different task: checking that some multivariate polynomial is identically zero on the cube . By using multilinear extensions, some tricks, and bit of randomness, we wind up being able to reduce that check to a sumcheck. That protocol is one of the most instructive basic examples to work through.
The PIOP Model
You might have noticed a subtle thing: the sumcheck protocol lets us check a claim about a polynomial . Which polynomial? This polynomial can't be one which the verifier has cleartext access to, since takes memory on the order of even to represent explicitly. On the other hand, we want the complexity for the verifier to be polylogarithmic: namely, polynomial in .
Thus, we need a way for to be "fixed" and well-defined, but without the verifier actually having explicit access to it. It turns out that we have the perfect way to do this: working in the PIOP model. Thus, the sumcheck is best conceptualized as a protocol which takes place in the PIOP model. Here, the polynomial in question is well-defined and fixed, in the sense that the prover has already committed the requisite data to the oracle. On the other hand, the verifier doesn't have to touch or see it in full.
The verifier's task will be to check whether the sum claim holds—or, more precisely, to reduce this claim to an evaluation claim on . This evaluation claim can be dealt with by means of queries to the oracle.
The Protocol
Here, we sketch the sumcheck protocol in full. As above, we have a fixed multivariate polynomial , and a claimed sum . The protocol is interactive, and proceeds over rounds.
- For each round index ,
- The prover computes the round polynomial and sends to the verifier (say, by sending its evaluations on sufficiently many points).
- The verifier checks whether .
- The verifier samples a random challenge and sends it to the prover. Moreover, the verifier updates its running sum claim:
- At the very end, the verifier outputs the reduced evaluation claim .
The security claim is that, up to a soundness error of a most , the correctness of the initial sum claim reduces to the correctness of that final evaluation. Thus, it suffices for the verifier to just check whether the final evaluation holds, which is much easier for it to do.
Sketch of Security Proof
As of the beginning of each given round , the running sum claim
will either be true or not true. Let's assume that it isn't true. Moreover, the prover's round polynomial either will or won't equal the "prescribed" univariate polynomial
Let's suppose that the running sum claim isn't true. If the prover sends the right , then the verifier will reject immediately: indeed, in this case,
will hold, so the verifier will reject its check above. The first inequality above is our hypothesis whereby the running sum claim is false. The second equality comes from the definition of . The third equality comes from our hypothesis .
Thus, we can safely pay attention to the case in which ; i.e., these univariate polynomials are not the same. And yet by basic univariate Schwartz–Zippel, we see that in this case will hold with high probability over the verifier's choice of . Assuming that this inequality does hold (i.e., that the verifier doesn't get extremely unlucky), we obtain:
In other words, the "wrongness" of the prover's round- sum claim has propagated to the next round .
If the prover's initial round claim is wrong, then, carrying this argument through all rounds, we conclude that that wrongness will propagate with high probability into the final inequality , which is what we need to show.