Grand Product Argument

The grand product argument handles claims about the product of a polynomial's values over the boolean hypercube. These claims take the form

where $T$ is $\ell$-variate and $a$ is a value known to the verifier. The argument reduces these grand product claims to evaluation claims on $T$.

Binius implements the grand product argument using a idea from Thaler [Tha13], which is based on the [GKR15] protocol. GKR is a very useful general technique for verifying the output of highly structured, low-depth arithmetic circuits. In this case, we want to verify the output of a circuit that is a binary tree of multiplication gates, as a means of checking the product of all the circuit's inputs. The GKR protocol requires no additional commitments, making it remarkably efficient for the prover while remaining succinct for the verifier. Under the hood, the GKR protocol progresses layer by layer through the circuit, invoking the sumcheck protocol once per layer.

Background

We have already seen how the sumcheck can transform claims about the sum over the cube of some multivariate polynomial to a claim about the evaluation of that multivariate polynomial. The GKR protocol is a special way of exploiting the sumcheck in a "layered" fashion. That is, we set up a sort of layered circuit or tree. Each layer of that tree is defined elementwise as a sum over the layer below it. Thus to go from one layer to the one beneath it, we need to run a sumcheck, to "peel off" that layer. We end up running as many sumchecks as there are layers in the entire tree.

This technique is very powerful, since many computations of interest can be expressed as layered circuits or trees. As it turns out, multiplication is one of them—and gives us one of our simplest (and most important) applications of GKR.

The Setup

Let's again write $T(X_0, \ldots , X_{\ell - 1})$ for our $\ell$-variate multilinear of interest (itself perhaps virtual). Again, the public data is $a$; our claim is that $\prod_{v \in \mathcal{B}_\ell} T(v) \stackrel{?}= a$.

The idea is very simple: both the prover and verifier will imagine a height-$\ell$, perfectly balanced binary tree. In the leaves, we will inscribe the values $T_\ell(v) \coloneqq T(v)$ for $v \in \mathcal{B}_\ell$ varying (i.e., the leaf layer will be just $T$ itself). For each internal layer $k \in \{0, \ldots , \ell - 1\}$, we will have exactly $2^k$ node values to fill in; we will call these $T_k(v)$, where here $v \in \mathcal{B}_k$ varies. In fact, for each $v \in \mathcal{B}_k$, we will recursively write in the node value $T_k(v) \coloneqq T_{k + 1}(v \mathbin{\Vert} 0) \cdot T_{k + 1}(v \mathbin{\Vert} 1)$. In other words, each internal node will be the product of its two children.

Following this idea to its root (pardon the pun), we see easily that the root of this tree will be $\prod_{v \in \mathcal{B}_\ell} T(v)$, or $a$ itself if the prover is honest. Technically, we should have $T_0() \stackrel{?}= a$ ($T_0$ is a "$0$-variate multilinear", or in other words a constant).

Unwinding GKR Layers

Now this hasn't gotten us much so far. The key point, though, is that the verifier can use the sumcheck to reduce a claim about one layer to a claim about the layer below it. The master claim that the verifier wants to check is a claim about the very top, 0^th layer (namely, that $T_0() \stackrel{?}= a$). If the verifier has the ability to repeatedly unwind claims like this, then it may proceed straight down to the leaf layer, at which point it will arrive upon an evaluation claim about $T$ itself, which is what we wanted.

The fact that saves us is that the relationship between each layer and the one below it is algebraic. Thus, for each $k \in \{0, \ldots , \ell - 1\}$, since, for each $v \in \mathcal{B}_k$, $T_k(v) = T_{k + 1}(v \mathbin{\Vert} 0) \cdot T_{k + 1}(v \mathbin{\Vert} 1)$ holds by fiat, $T_k$'s multilinear extension $T_k(X_0, \ldots , X_{k - 1})$ equals:

Each evaluation claim of the form $T_k(r_k) \stackrel{?}= a_k$, say, thus amounts to a sum claim on the $k$-variate, degree-3 multivariate polynomial:

This is exactly the kind of thing we can sumcheck; upon doing so, the verifier will reduce the initial claim $T_k(r_k) \stackrel{?}= a_k$ to a further claim of the form

for some point $r'_k = (r'_{k, 0}, \ldots , r'_{k, k - 1}) \in \mathcal{T}_\tau^k$ sampled during the sumcheck. The verifier may evaluate $\widetilde{\texttt{eq}}(r'_k, r_k)$ itself. As for the others, up to nondeterministically receiving claimed evaluations $s_0 = T_{k + 1}(r'_{k, 0}, \ldots , r'_{k, k - 1}, 0)$ and $s_1 = T_{k + 1}(r'_{k, 0}, \ldots , r'_{k, k - 1}, 1)$ from the prover, the verifier can sample a further random challenge $r'_{k, k} \gets \mathcal{T}_\tau$, and output the reduced evaluation claim $T_{k + 1}(r'_{k, 0}, \ldots , r'_{k, k}) \stackrel{?}= a_{k + 1} \coloneqq (1 - r'_k) \cdot s_0 + r'_k \cdot s_1$.

Thus we've gotten what we wanted: our new evaluation claim is that $T_{k + 1}(r_{k + 1}) \stackrel{?}= a_{k + 1}$. Here, the parties mutually set $r_{k + 1} \coloneqq (r'_{k, 0}, \ldots , r'_{k, k})$ and $a_{k + 1} \coloneqq (1 - r'_k) \cdot s_0 + r'_k \cdot s_1$, just as the verifier did above.

The End

By proceeding this way throughout $\ell$ rounds, the verifier may thus reduce its initial claim $a \stackrel{?}= T_0() = \prod_{v \in \mathcal{B}_\ell} T(v)$ to the evaluation claim $a_\ell \stackrel{?}= T_\ell(r_\ell) = T(r_\ell)$. Since $T$ is virtual, we agreed already that the verifier will have a way of evaluating it.

Evaluating a virtual polynomial can be complicated, though: a fact which brings us to our next page, evalcheck.