GKR Claims
Claim definition
"Claims" in GKR are statements which the prover has yet to show correctness for. As described earlier, the first step in proving the correctness of a GKR circuit (after sending over all circuit inputs, both public and committed) is to take the circuit's (public) output layer and send over all of its evaluations to the verifier.
For example, let's say that we have a circuit whose output layer contains 4 elements, i.e. whose representative MLE can be described by . Additionally, let's say that these evaluations are , such that
These four equalities above are actually the first claims whose validity the prover wishes to demonstrate to the verifier. The verifier doesn't know what the true values of are, of course, but would be able to check each of these relationships with the prover's help via sumcheck. This would be rather expensive, however, as the number of claims is exactly equal to the number of circuit outputs/evaluations within the circuit's output layer. Instead, the verifier can sample some randomness and have the prover prove the following:
Note that the above follows precisely from the definition of a multilinear extension (MLE), and it can indeed be viewed exactly as the evaluation of at the random points . The protocol takes a slight soundness hit here, as a cheating prover might get away with an incorrect circuit output (say, , but ), but the probability of such an occurrence is , as non-identical MLEs only intersect at exactly one point via the Schwartz-Zippel lemma.
In general, claims take the following form:
In other words, the prover wishes to convince the verifier that the evaluation of the MLE representing the 'th layer at the challenge is .
Claim Propagation
For another example of claim propagation/reduction, see this section. Note that the below example uses a structured GKR relationship while the other example uses a canonic GKR relationship.
Recall the general sumcheck relationship for a function ; the prover claims that the following relationship is true for :
Assuming that are bound to during the sumcheck process, the final verifier check within sumcheck is the following, where the RHS must be an "oracle query", i.e. the verifier must know that the evaluation of on is correct:
How does this oracle query actually get evaluated in GKR? The answer is claims and sumcheck over claims for a previous layer. Specifically, let's consider the following relationship (see structured GKR section for more information about the polynomial and this kind of layerwise relationship):
This is the polynomial relationship between layer and layer of a circuit where the 'th layer's values are exactly those of the 'th layer's values squared. For example, if the evaluations of are then we expect the evaluations of to be .
The prover starts with a claim
for , and wishes to prove it to the verifier. It does so by running sumcheck on the RHS of the above equation, i.e.
Let be bound to during the rounds of sumcheck. Additionally, let be the univariate polynomial the prover sends in the 'th round of sumcheck. The oracle query check is then
The verifier is able to compute on its own in time, but unless is an MLE within an input layer of the GKR circuit, they will not be able to determine the value of . Instead, the prover sends over a new claimed value , and the verifier checks that
The only thing left to check is whether . Notice, however, that this now a new claim on an MLE residing in layer , and that we started with a claim on layer . In other words, we've reduced the validity of a claim on layer to that of a claim on layer , which is the core idea behind GKR: start with claims on circuit output layers, and reduce those using sumcheck to claims on earlier layers of the circuit. Eventually all remaining claims will be those on circuit input layers, which can be directly checked via either a direct verifier MLE evaluation for public input layers, or a PCS evaluation proof for committed input layers.
Claim Aggregation
In the above example, we reduced a single claim on layer to claim(s) on MLEs residing in previous layers. What happens when there are multiple claims on the same layer, e.g.
One method would be to simply run sumcheck times, once for each of the above claims, and reduce to separate claims on MLEs residing in previous layers. This strategy, however, leads to an exponential number of claims in the depth of the circuit, which is undesirable.
Instead, Remainder implements two primary modes of claim aggregation, i.e. methods for using a single sumcheck to prove the validity of many claims on the same MLE.
RLC (Random Linear Combination) Claim Aggregation
Additional reading: See XZZ+19, page 10 ("Combining two claims: random linear combination").
The idea behind RLC claim aggregation is precisely what it sounds like: the prover shows that a random linear combination of the claimed values indeed equals the corresponding random linear combination of the summations on the RHS of e.g. the third equation in the above section. The implementation of RLC claim aggregation within Remainder works for structured layers and gate layers, but not for matrix multiplication layers or input layers (as explained below).
We defer to the corresponding pages for more detailed explanations of the layerwise relationships, but review their form factors here and show how RLC claim aggregation can be done for each here.
Structured Layers
We start with structured layers, and use the same example relationship from above:
For simplicity, we aggregate two claims rather than claims, but the methodology generalizes in a straightforward fashion. Our aggregated claim is constructed as follows:
Similarly, we take an RLC of the summations and create a new summation to sumcheck over (we let and for concision):
For structured layers, in other words, the prover and verifier simply take a random linear combination of the claims and perform sumcheck over a polynomial which is identical to the original layerwise relationship polynomial but with the term replaced with an RLC of terms in the same manner as the RLC of the original claims.
Gate Layers
A similar idea applies to gate layers. We use mul gate as the example layerwise relationship here:
Again, we aggregate just two claims for simplicity, although the idea generalizes very naturally to claims:
The polynomial relationship to run sumcheck over is constructed using a similar idea as that of structured layers:
Rather than taking a linear combination of the polynomials, we instead take a linear combination of the polynomials.
Costs
The prover costs for RLC claim aggregation are as follows -- assume that we are working with a structured layer (the analysis is similar for gate layers) and that the degree of every sumcheck variable is (in the above example for a structured layer, ). Additionally, assume that we have claims over a layer with variables.
- As shown above, RLC claim aggregation for structured layers simply involves "factoring out" the term between each of the 's and the 's. Rather than multiplying the structured polynomial relationship by a single , we multiply by an RLC of terms.
- For each additional term, the prover incurs an additional evaluations worth of work (across a single sumcheck round). Evaluating can be done in time by the prover for variables, and thus the total cost (for claims) is
- across all rounds of sumcheck. The total prover runtime is thus .
The proof size is identical to that of the single-claim sumcheck case, since the degree of the sumcheck messages do not change.
Finally, the verifier cost is slightly increased. Specifically, during intermediate rounds of sumcheck the verifier does not do any additional work (compared to the single-claim sumcheck case), but during the oracle query the verifier must evaluate separate instances of at fixed points. This takes the verifier additional time.
Matrix Multiplication Layers (counterexample)
Prerequisite: matrix multiplication layers page.
For matrix multiplication layers: consider , and consider the sumcheck relationship .
In matrix multiplication layers, the claim is always of the form , and the prover proceeds by first binding and before showing that . In the RLC claim aggregation case, we have claims Where and (otherwise they would be claims from the same "source" layer and would therefore be identical). The verifier samples random challenge . In this case, our sumcheck relationship is the following: Because and , there is no way to factor the above expression's RHS to combine terms in any way, and thus RLC claim aggregation is equivalent to not aggregating claims at all and simply running two separate sumchecks on
Input Layers (counterexample)
For input layers: RLC claim aggregation combines claims into a single claimed statement For public inputs, the verifier must evaluate each of and on their own, and thus nothing is gained by the combination.
For committed inputs, a polynomial commitment scheme may allow for cheaper evaluation proofs in the above form (vs. two separate evaluation proofs; one for each claim), but this is generally not the case.
Interpolative Claim Aggregation
Additional reading: See Tha13, page 15 ("reducing to verification of a single point"), for another description of the protocol, and Mod24, page 15 (Section 3.4, "Claim aggregation"), for a thorough description + optimization.
Interpolative claim aggreation works by having the prover and verifier both compute an interpolating polynomial , such that for the claims described earlier, i.e.
we have that
Note that the degree of is , as there are points for each of the coordinates which must be interpolated.
The prover then sends over the polynomial , i.e. the restriction of to points in generated by . Note that the degree of is , as is multilinear in each of its variables, and each of those variables is degree at most in the input variable for .
The verifier samples and sends it to the prover. The prover and verifier both compute , and the prover proves the single claim
where was sent by the prover and the verifier evaluates it at on its own.
Costs
The prover cost for interpolative claim aggregation is as follows:
- Given claims with variables each, is a -degree function in each of its components, and since is multilinear in each of its variables, is a univariate polynomial with degree . The prover must send evaluations to the verifier, although the first have already been sent implicitly in the form of the claims.
- The prover thus must evaluate at points. Each evaluation requires the prover to evaluate in time, and then in time. The prover's total runtime is thus .
The proof size for interpolative claim aggregation is as follows:
- As reasoned earlier in the prover cost section, the prover sends over evaluations of . The proof size is thus field elements.
The verifier runtime for interpolative claim aggregation is as follows:
- The verifier receives evaluations of from the prover and evaluates it at a random point . This takes time. Additionally, the verifier evaluates , which takes time as well. The verifier's total runtime is thus .
Optimizations
Remainder has a few built-in optimizations for interpolative claim aggregation which substantially lower the prover costs for claims with "structure" within their evaluation points. For more details, see Mod24, page 15 (Claim Aggregation section).