Quickstart

Hi there! Welcome to the official Remainder documentation/tutorial. For the code reference, see this site. Note that Remainder is specifically a GKR/Hyrax prover and that this tutorial assumes familiarity with basic concepts in zero-knowledge and interactive proofs. For a gentler introduction to the basics behind verifiable computation, interactive proofs, and zero-knowledge, see Chapter 1 of Justin Thaler's wonderful manuscript.

The documentation is split into four primary parts:

• The first is an intuitive introduction to the "GKR" interactive proof scheme for layered circuits. The name "GKR" refers to Goldwasser, Kalai, and Rothblum, the co-authors of the paper which first introduced the notion of proving the correctness of layered circuits' outputs with respect to their inputs via sumcheck. If you are not familiar with GKR concepts, we strongly recommend you read this section before engaging with either of the next two sections or even the quickstart below.
• The second follows from the first and dives a tad deeper into the specific methodology of layerwise relationships, prover claims, etc. and explains the various concepts behind GKR in a loosely mathematical fashion.
• The third is a guide to Remainder's frontend where we explain how the theoretical concepts described in earlier sections can be used in practice. It contains a lot of examples with runnable Rust code, and it can be studied independently or in conjunction with the second section.
• The final is an introduction to the Hyrax interactive proof protocol, a "wrapper" around the GKR protocol which offers computational zero-knowledge using blinded Pedersen Commitments.

In addition, we provide a concise "how-to" quickstart here. This quickstart covers the basics of using Remainder as a GKR proof system library, including the following:

• Circuit description generation
• Appending inputs to a circuit description
• Proving and verifying

Creating a Layered (GKR) Circuit

See frontend/examples/tutorial.rs for code reference. To run the test yourself, navigate to the Remainder_CE root directory and run the following command:

cargo run --package frontend --example tutorial

To define a layered circuit, we must describe the circuit's inputs, intermediate layers and relationships between them, and output layers. We'll first take a look at the build_circuit() function. The first line is

#![allow(unused)]
fn main() {
let mut builder = CircuitBuilder::<Fr>::new();
}

This creates a new CircuitBuilder instance with native field Fr (BN254's scalar field). The CircuitBuilder is where all circuit components (nodes) will be aggregated and compiled into a full layered circuit.

The next line is

#![allow(unused)]
fn main() {
let lhs_rhs_input_layer =
    builder.add_input_layer("LHS RHS input layer", LayerVisibility::Committed);
let expected_output_input_layer =
    builder.add_input_layer("Expected output", LayerVisibility::Public);
}

This adds two input layers to the circuit (see the Input Layer page for more details). Note that an input layer is one which gets all claims on it bundled together and is treated as a single polynomial (multilinear extension) when the prover decides how to divide the circuit inputs to commit to each one.

In this example we separate the input data into two separate input layers because we want some of them to be committed instead of publicly known. This means that the verifier should only be able to see polynomial commitments to the MLEs on such input layers (see Committed Inputs). Depending on the proving backend used (plain GKR vs. Hyrax), committed layers can act as private layers in the sense that the verfier learns nothing about their contents when verifying a proof (more on that later on).

We then have the following:

#![allow(unused)]
fn main() {
let lhs = builder.add_input_shred("LHS", 2, &lhs_rhs_input_layer);
let rhs = builder.add_input_shred("RHS", 2, &lhs_rhs_input_layer);
let expected_output = builder.add_input_shred("Expected output", 2, &lhs_rhs_input_layer);
}

We add three input "shred"s to the circuit, the first two being subsets of the data in the "LHS RHS input layer", and the last one being (the entire) "Expected output" layer. Each "shred" has 2 variables (i.e. has $2^2=4$ evaluations, and is identified with a unique string, e.g. "RHS"). The difference between an input layer and an input "shred" is that the latter refers to a specific subset of the input layer's data which should be treated as a contiguous chunk to be used as input to a later layer within the circuit.

We begin adding layers to the circuit:

#![allow(unused)]
fn main() {
let multiplication_sector = builder.add_sector(lhs * rhs);
}

Notice that even though lhs and rhs are input "shred"s from the same input layer, because we added them as separate "shred"s earlier, we can now use them as separate inputs to be element-wise multiplied against one another. In general, input layers are treated as a single entity by the verifier, while input shreds are treated as subsets of input layers which the prover can use as inputs to other layers within the circuit.

This first layer is a "sector", which is the Remainder way of referring to structured layerwise relationships. This simply means that with evaluations $[a,b,c,d]$ in lhs and $[e,f,g,h]$ in rhs, the resulting layer should hold the element-wise product of the evaluations in lhs and those in rhs, i.e. $[ae,bf,cg,dh]$.

We add another layer to the circuit:

#![allow(unused)]
fn main() {
let subtraction_sector = builder.add_sector(multiplication_sector - expected_output);

builder.set_output(&subtraction_sector);
}

This layer is another element-wise operator, but where we element-wise subtract all of the values rather than multiply them. Here, we are semantically subtracting the expected_output from the earlier layer we created which was the element-wise product of the values in lhs and rhs (see this section for more details). The resulting layer should be zero if the two are element-wise equal, and we thus call builder.set_output() on the resulting layer, which tells the circuit builder that this layer's values should be publicly revealed to the verifier (and that no future layer depends on the values).

Finally, we create the layered circuit from its components:

#![allow(unused)]
fn main() {
builder.build().expect("Failed to build circuit")
}

This creates a Circuit<Fr> struct which contains the layered circuit description (see GKRCircuitDescription), the mapping between nodes and layers (see CircuitEvalMap), and the state for circuit inputs which have been partially populated already.

Populating Circuit Inputs

First, we instantiate the circuit description which we created above (see the function main()):

#![allow(unused)]
fn main() {
let base_circuit = build_circuit();
let mut prover_circuit = base_circuit.clone();
let verifier_circuit = base_circuit.clone();
}

Note that we additionally create prover and verifier "versions" of the circuit. The reason for this is that the prover will want to attach input data to the circuit, whereas the verifier will want to receive those inputs from the proof itself and will not independently attach inputs to the circuit this time around. We additionally note that in general, rather than generating the circuit description once and then cloning for the prover and verifier, we will usually generate the circuit description and serialize it, then distribute the description to both the proving and verifying party. The above emulates this but in code.

The next step to proving the correctness of the output of a GKR circuit is to provide the circuit with all of its inputs (including hints for "verification" rather than "computation" circuits, e.g. the binary decomposition of a value; note that Remainder currently does not have features which assist with computing such "hint" values and these will have to be manually computed outside of the main prove() function). In the case of our example circuit, we have the following:

#![allow(unused)]
fn main() {
let lhs_data = vec![1, 2, 3, 4].into();
let rhs_data = vec![5, 6, 7, 8].into();
let expected_output_data = vec![5, 12, 21, 32].into();
}

The vec!s above define the integer values belonging to the input "shreds" which we declared earlier in our circuit description definition (recall that "shreds" are already assigned to input layers). Additionally, since we declared earlier that e.g. let lhs = builder.add_input_shred("LHS", 2, &input_layer);, where the 2 represents the number of variables as the argument of the multilinear extension representing that input "shred", we have $2^2$ values within each input "shred", i.e. 4 evaluations for each of the above.

We ask the circuit to set the above data using our string tags for the input "shred"s (note that we need an exact string match here).

#![allow(unused)]
fn main() {
prover_circuit.set_input("LHS", lhs_data);
prover_circuit.set_input("RHS", rhs_data);
prover_circuit.set_input("Expected output", expected_output_data);
}

Generating a GKR proof

We next "finalize" the circuit for proving, i.e. check that all declared input "shred"s have data associated to them, combine their data with respect to their declared input layer sources, and set up parameters for polynomial commitments to input layers, e.g. Ligero PCS.

#![allow(unused)]
fn main() {
let provable_circuit = prover_circuit
    .gen_provable_circuit()
    .expect("Failed to generate provable circuit");
}

Finally, we run the prover using the "runtime-optimized" configuration:

#![allow(unused)]
fn main() {
let (proof_config, proof_as_transcript) =
    prove_circuit_with_runtime_optimized_config::<Fr, PoseidonSponge<Fr>>(&provable_circuit);
}

This function returns a ProofConfig and a TranscriptReader<Fr, PoseidonSponge<Fr>>. The former tells the verifier which configuration it should run in to verify the proof, and the latter is a transcript representing the full GKR proof (see Proof/Transcript section for more details).

Verifying the GKR proof

To verify the proof, we first take the circuit description and prepare it for verification:

#![allow(unused)]
fn main() {
let verifiable_circuit = verifier_circuit
    .gen_verifiable_circuit()
    .expect("Failed to generate verifiable circuit");
}

Finally, we verify:

#![allow(unused)]
fn main() {
verify_circuit_with_proof_config::<Fr, PoseidonSponge<Fr>>(
    &verifiable_circuit,
    &proof_config,
    proof_as_transcript,
);
}

This function uses the provided proof_config and executes the GKR verifier against the verifiable_circuit, i.e. the verifier-ready circuit description. The function crashes if the proof does not verify for any reason, although in this case it should pass.

Congratulations! You have just:

• Created your first layered circuit description,
• Attached data to the circuit input layers,
• Proven the correctness of the circuit outputs against the inputs, and
• Verified the resulting GKR proof!

GKR Background

This section describes the basics of GKR, including necessary notation, mathematical concepts, and arithmetization, as well as a high-level description of how proving and verification works in theory.

Notation Glossary

Note that each of these definitions will be described in further detail in the sections to come, but are aggregated here for convenience.

High-level Description

GKR is an interactive protocol which was first introduced by Goldwasser, Kalai, and Rothblum [2008]. It proves the statement that $C(y)=0$, where $C$ is a layered arithmetic circuit, and $y$ is the input to the circuit.

At a high-level, it works by reducing the validity of the output of the circuit (typically denoted as layer $0$, ${\mathcal{L}}_0(x)=0$, for a circuit with depth $d+1$), to the previous layer of computation in the circuit, ${\mathcal{L}}_1.$ Eventually, these statements reduce to a claim an evaluation of the input as a polynomial. If the input $y$ is encoded as the coefficients of a polynomial $f$, we are left to prove that $f(x)=c$.

The later sections unpack these reductions, showing how we can reduce the claim that $C(y)=0$ to a polynomial evaluation at a random point.

Why GKR?

GKR has several key advantages when compared with other proof systems:

• Not having to cryptographically commit to the entire "circuit trace":
  • In general, proof systems which use e.g. PlonK-ish or R1CS/GR1CS arithmetization require a polynomial commitment to all circuit values.
  • The size of this commitment often determines the memory/runtime/proof size/verification time of such systems, as the PCS (rather than the IOP) tends to be the bottleneck re: the aforementioned metrics.
  • GKR, on the other hand, does not require a commitment to any "intermediate" values within the circuit, i.e. those which can be computed using addition/multiplication from other values present within the circuit.
  • For certain layered circuits (e.g. neural network circuits, where the intermediate activation values "flow" through the model and can be fully computed from the weights and model input), this substantially reduces the number of circuit values which require cryptographic operations (e.g. circuit-friendly hash function, MSM, FFT), reducing the bottleneck which the PCS step normally imposes.
• Natively multilinear IOP which depends almost wholly on sumcheck and other linear, embarrassingly parallel operations -- sumcheck is an extremely fast, field-only primitive which is extremely parallelizable and lends itself to various small field + extension field optimizations, resulting in an extremely fast prover.
• Easy lookup integration with both LogUp and Lasso. The former, in particular, is expressible via a very lovely structured circuit, and is time-optimal within GKR with respect to the number of lookups (linear # of field operations in number of witnesses to be looked up + lookup table size).

Interactive Protocol

In the following sections, we start with some necessary background, such as Multilinear Extensions and the Sumcheck Interactive Protocol. We then move on to use these two primitives in order to build out the GKR protocol, which involves encoding layer-wise relationships within the circuit $C$ as sumcheck statements.

Finally, we move on to some protocols used within the Remainder codebase, such as claim aggregation, and detail the differences between what we call "canonic" GKR and "structured" GKR, both of which are implemented in Remainder.

Statement Encoding

The GKR protocol specifically works with statements of the form $C(y)=0$, where $C$ is a layered arithmetic circuit. Define a singular value, $0$, to be the output layer, ${\mathcal{L}}_0$, and the input values $y_i$ to make up the input layer, ${\mathcal{L}}_d$.

For any layer, the following invariant holds: if a value is in ${\mathcal{L}}_i$, then it must be the result of a binary operation involving values in layers $j,k$ such that $j>i,k>i$. It is possible that $j=k$, but not necessary.

These binary operations are usually referred to as "gates." In the following tutorial we will be focusing on two gates: $\mathrm{add}$ gates, which are represented by the following function:

$$\mathrm{add}(z,x,y):\{0,1{\}}^{s_i+s_j+s_k}\mapsto \{0,1\}=\{\begin{array}{ll}1,& \text{if }{\mathrm{val}}_j(x)+{\mathrm{val}}_k(y)={\mathrm{val}}_i(z)\\ 0,& \text{otherwise}\end{array}$$ and $\mathrm{mul}$ gates: $$\mathrm{mul}(z,x,y):\{0,1{\}}^{s_i+s_j+s_k}\mapsto \{0,1\}=\{\begin{array}{ll}1,& \text{if }{\mathrm{val}}_j(x)\cdot {\mathrm{val}}_k(y)={\mathrm{val}}_i(z)\\ 0,& \text{otherwise}\end{array}$$

In other words, if we think of a physical representation of $C$, the binary gates represent the "wires" of the circuit. They show how the values from wires belonging in previous layers of the circuit can be used to compute a value in a future layer (from input to output). In fact, for every value with label $z$ in layer $i\ne 0:\exists x,y$ such that $\mathrm{add}(z,x,y)=1$ or $\mathrm{mul}(z,x,y)=1$ for $x,y$ as labels for values in layers $j,k>i$.

Example

Let's look at the following layered arithmetic circuit with depth $d$ = 3:

In this case, $\mathrm{add}(4,0,1)=1$ and $\mathrm{mul}(4,0,1)=0$, but $\mathrm{mul}(7,4,1)=1$. Notice how the circuit naturally falls in "layers" based on the dependencies of values.

Multilinear Extensions (MLEs)

Let $f(x_1,x_2,\dots ,x_n)$ be a function $\in {\mathbb{F}}^n\mapsto \mathbb{F}$. Its multilinear extension $\tilde{f}(x_1,\dots ,x_n)$ is defined such that $\tilde{f}$ is linear in each $x_j\in \mathbb{F}$, and where $\tilde{f}(x)=f(x)\forall x\in \{0,1{\}}^n$.

Equality MLE

In order to explicitly formulate $\tilde{f}$ in terms of $f$, let us define the following indicator function:

$$\mathrm{eq}(x;z):\{0,1{\}}^{2n}\mapsto \{0,1\}=\{\begin{array}{ll}1,& \text{if }x=z\\ 0,& \text{otherwise}.\end{array}$$

Fortunately, $\mathrm{eq}(x;z):\{0,1{\}}^{2n}\to \{0,1\}$ has an explicit formula which is linear in each of $x_i$, or the bits of $x$. Intuitively, if $x=z$, then each of its bits must be equal. In boolean logic, this is the same thing as saying $(x_i=z_i=0)$ OR $(x_i=z_i=1)$ for all of the bits $i$ (which is an AND over all of the bits $i$).

When our inputs $x_i,z_i\in \{0,1\}$ this statement can be expressed as the following product: $$\prod _{i=1}^n(1-x_i)(1-z_i)+x_i{z}_i.$$ Taking the multilinear extension of $\mathrm{eq}$ simply means allowing for non-binary inputs $x_i,z_i\in \mathbb{F}$, because the polynomial is already linear in each variable. Since for all binary $x_i,z_i\in \{0,1\}$ we have that $\mathrm{eq}(x;z)=\widetilde{\mathrm{eq}}(x;z)$, the above definition of $\widetilde{\mathrm{eq}}(x;z)$ is an actual multilinear extension of $\mathrm{eq}$.

Construction from $\widetilde{\mathrm{eq}}$

We now have a polynomial extension of $\mathrm{eq}(x,z)$ which happens to be (by construction) linear in the $x$ variables (again, denote this function $\widetilde{\text{eq}}$). We can now define the multilinear extension of any function, as hoped for above:

$$\tilde{f}(x_1,\dots ,x_n)=\sum _{z_1,...,z_n\in \{0,1{\}}^n}\widetilde{\mathrm{eq}}(x;z)\cdot f(z_1,\dots ,z_n)$$

where $z_i$ are the bits of $z$.

Why is the above a valid multilinear extension of $f$? The idea here is that when evaluating $\tilde{f}$ on any $x_1,...,x_n\in \{0,1{\}}^n$, we have $\widetilde{\mathrm{eq}}(x;z)=0$ for all $z\ne x$ (since both $z$ and $x$ are binary, $\widetilde{\mathrm{eq}}(x;z)=\mathrm{eq}(x;z)$ behaves exactly like the boolean equality function), and thus all the terms in the above summation over $z_1,...,z_n\in \{0,1{\}}^n$ are zero except for the term where $z=x$, where we have $\widetilde{\mathrm{eq}}(x;z)=1$, and the value of that term is exactly $f(z_1,...,z_n)=f(x_1,...,x_n)$.

Another nice property of multilinear extensions which can be proven is that they are uniquely defined. I.e., ${\sum }_{z_i\in \{0,1\}}\widetilde{\mathrm{eq}}(x;z)\cdot f(z_1,\dots ,z_n)$ is the only multilinear function in $n$ variables which extends $f$.

Example

Let $f(x_1,x_2,x_3)=2x_1^2{x}_3+4x_2{x}_3^3+3x_1{x}_2^2{x}_3+5x_1+6x_2+3.$ Let us first build a table of evaluations of $f$ for $x_i\in \{0,1\}:$

We also build a table for $\widetilde{\mathrm{eq}}(x;z)$ for $x_i\in \{0,1\}$ in terms of $z$:

Then, using the formula for $\tilde{f}(x_1,\dots ,x_n)={\sum }_{z_i\in \{0,1\}}\widetilde{\mathrm{eq}}(x;z)\cdot f(z_1,\dots ,z_n)$, we get the explicit formula:

$$\begin{gathered} \tilde{f}(x_1,\dots ,x_n)=3(1-x_1)(1-x_2)(1-x_3)+3(1-x_1)(1-x_2)(x_3) \\ +9(1-x_1)(x_2)(1-x_3)+13(1-x_1)(x_2)(x_3)+8(x_1)(1-x_2)(1-x_3) \\ +10(x_1)(1-x_2)(x_3)+14(x_1)(x_2)(1-x_3)+23(x_1)(x_2)(x_3) \end{gathered}$$.

From here you can verify that $\tilde{f}(x)=f(x)$ when $x\in \{0,1{\}}^n$, and that $\tilde{f}(x)$ is linear in each of the $x$ variables.

Sumcheck

(Most of the content of this section is from Section 4.1 in Proofs, Args, and ZK by Justin Thaler, which has more detailed explanations of the below.)

This section will first cover the background behind the sumcheck protocol, and then provide an introduction as to why this may be useful in verifying the computation of layerwise arithmetic circuits.

The sumcheck protocol is an interactive protocol which verifies claims of the form: $$H\stackrel{?}{=}\sum _{x_i\in \{0,1\}}f(x_1,\dots ,x_n).$$ In this statement, $f$ is not necessarily multilinear, and $H\in \mathbb{F}$.

In other words, the prover, $\mathcal{P}$, claims that the sum of the evaluations of a function $f:{\mathbb{F}}^n\to \mathbb{F}$ over the boolean hypercube of dimension $n$ is $H.$ Naively, the verifier $\mathcal{V}$ can verify this statement by evaluating this sum themselves in $O(2^n)$ time assuming oracle access to $f$ (being able to query evaluations of $f$ in $O(1)$ time), with perfect completeness (true claims are always identified by the verifier) and perfect soundness (false claims are always identified by the verifier).

Sumcheck relaxes the perfect soundness to provide a probabilistic protocol which verifies the claim in $O(n\cdot d)$ time with a soundness error of $\le \frac{n\cdot d}{|\mathbb{F}|}$ where $d$ is the maximum degree of any variable $x_1,\dots ,x_n$.

The Interactive Protocol

We start with a straw-man interactive protocol which still achieves perfect completeness and soundness in verifier time $O(2^n)$ and prover time $O(2^n).$ Then, we build on this version of the protocol and introduce randomness to achieve $O(n\cdot d)$ verifier time, with a soundness error of $\le \frac{n\cdot d}{|\mathbb{F}|}.$

A non-probabilistic protocol

Note that the sum we are trying to verify can be rewritten as such: $$H\stackrel{?}{=}\sum _{x_1\in \{0,1\}}\sum _{x_2\in \{0,1\}}\sum _{x_3\in \{0,1\}}\cdots \sum _{x_n\in \{0,1\}}f(x_1,\dots ,x_n).$$ Let's say $\mathcal{P}$ sends $\mathcal{V}$ the following univariate: $$f_1(X)\stackrel{?}{=}\sum _{x_2\in \{0,1\}}\sum _{x_3\in \{0,1\}}\cdots \sum _{x_n\in \{0,1\}}f(X,x_2,\dots ,x_n).$$ One way for $\mathcal{P}$ to communicate $g(X)$ to $\mathcal{V}$ the univariate $g(X)$ is to send $d+1=\mathrm{degree}(g)+1$ evaluations of $g(X)$. While $\mathcal{P}$ can alternatively send coefficients, we focus on this method of defining a univariate and assume $\mathcal{P}$ sends the evaluations $g(0),g(1),\dots ,g(d)$ to $\mathcal{V}$.

$\mathcal{V}$ can verify whether $H$ is correct in relation to $f_1(X)$ by checking whether $H=f_1(0)+f_1(1).$ In other words, we have reduced the validity of claim that $H$ is the sum of the evaluations of $f$ over the $n$-dimensional boolean hypercube to the claim that $f_1(X)$ is the univariate polynomial over a smaller sum.

Now the verifier has evaluations $f_1(0),f_1(1)$ to verify. We can similarly reduce this to claims over even smaller summations. Namely, now the prover sends over the following univariates: $$f_{2,j}(X)\stackrel{?}{=}\sum _{x_3\in \{0,1\}}\sum _{x_4\in \{0,1\}}\cdots \sum _{x_n\in \{0,1\}}f(j,X,x_2,\dots ,x_n),\forall j\in [0,1].$$

$\mathcal{P}$ and $\mathcal{V}$ keep engaging in such reductions until $\mathcal{V}$ is left to verify $2^n$ evaluations of $f$: this is exactly the evaluations of $f$ over the boolean hypercube, assuming that $\mathcal{V}$ has oracle access to $f$ (it can query evaluations of $f$ in $O(1)$ time).

We have transformed the naive solution, where $\mathcal{V}$ just evaluates the summation on their own, into an interactive protocol. In the next section we will go over how to slightly modify this by adding randomness to significantly reduce the costs incurred by $\mathcal{P}$ and $\mathcal{V}$.

Schwartz-Zippel Lemma

As a brief interlude, let us go over the Schwartz-Zippel Lemma, which we can use to modify the straw-man protocol. It states that if $f(x)$ is a nonzero polynomial with degree $d$, then the probability that $f(r)=0$ for some random value $r$ sampled from a set $S$ is upper-bounded by $\frac{d}{|S|}$.

This is can be seen because by the Fundamental Theorem of Alegbra, $f(x)$ has at most $d$ roots. We take the probability that we randomly sampled one of those roots out of a set of size $|S|$.

In the case of sumcheck, we consider the polynomial to be over a field $\mathbb{F}$, and our randomly sampled element to be uniformly sampled from $\mathbb{F}$.

Introducing randomness

Our main blow-up with the straw-man interactive protocol came from the exponentially growing number of claims $\mathcal{V}$ had to verify, ending up with $2^n$ evaluations of $f$ at the end. Instead, if we found a way for the reduction from $f_i(X)$ to claims on $f_{i+1}(X)$ (or the reduction from the claim of $H$ to claims on $f_1(X)$) to be a one-to-one reduction in terms of number of claims, rather than one claim reduced to two claims, $\mathcal{V}$ would only have to verify $n$ claims, and $\mathcal{P}$ would only have to send over $n$ univariate polynomials.

Let us keep the first step the same, where $\mathcal{P}$ first sends the following univariate polynomial: $$f_1(X)\stackrel{?}{=}\sum _{x_2\in \{0,1\}}\sum _{x_3\in \{0,1\}}\cdots \sum _{x_n\in \{0,1\}}f(X,x_2,\dots ,x_n).$$

Now, $\mathcal{V}$ checks whether $H=g(0)+g(1).$ Instead of $\mathcal{P}$ sending both $f_{2,0}(X)$ and $f_{2,1}(X)$, $\mathcal{V}$ uniformly samples a random challenge $r_1$ from $\mathbb{F}$ and sends this to $\mathcal{P}.$ $\mathcal{P}$ sends a single univariate: $$f_2(X)\stackrel{?}{=}\sum _{x_3\in \{0,1\}}\sum _{x_4\in \{0,1\}}\cdots \sum _{x_n\in \{0,1\}}f(r_1,X,x_3,\dots ,x_n).$$ $\mathcal{V}$ checks whether $f_1(r_1)=f_2(0)+f_2(1).$ This process is repeated iteratively, until finally in the last round, where $\mathcal{P}$ sends $\mathcal{V}$ the following:

$$f_n(X)\stackrel{?}{=}f(r_1,\dots ,r_{n-1},X).$$

Assuming the verifier has oracle access to $f$, the verifier can check whether $f_n(r_n)=f(r_1,\dots ,r_n)$. The difference between this protocol and the naive protocol above is that at each step, instead of individually verifying $f_i(0)$ and $f_i(1)$, $\mathcal{V}$ sends $\mathcal{P}$ a "challenge" $r_i$ in which $\mathcal{P}$ responds to by sending over the appropriate univariate polynomial. Therefore we have achieved a one-to-one claim reduction, and the verifier having to only verify one equation per round.

Soundness Intuition

We provide brief intuition for the soundness bound from the above protocol. At any step $i$, the prover can cheat by sending a different univariate polynomial $h_i(X)$ instead of the expected $f_i(X)$ such that $h_i(r_i)=f_i(r_i)$, but $h_i(X)\ne f_i(X)$. This allows them to, ultimately, prove a different original statement: that the sum ${\sum }_{x\in \{0,1{\}}^n}f(x)=H^{\prime }\ne H$. Because $\mathcal{V}$ sends $r_i$ to $\mathcal{P}$, we can be confident that $\mathcal{P}$ does not adversarially choose $r_i$ to be one of the roots of $h_i(X)-f_i(X)$. Then, by the Schwartz-Zippel lemma, the probability that $r_i$ happened to be one of the "zeros" of $h_i(X)-f_i(X)=\frac{d_i}{|\mathbb{F}|}$ where $d_i$ is the degree of $h_i(X)-f_i(X).$

Example

We do a short example of the sumcheck protocol in the integers. Let $f(x)=3x_1{x}_2^2+4x_3{x}_2+5x_1^3{x}_3+2.$ $\mathcal{P}$ rightfully claims that ${\sum }_{x_1\in \{0,1\}}{\sum }_{x_2\in \{0,1\}}{\sum }_{x_1\in \{0,1\}}f(x_1,x_2,x_3)=H=40.$ In order to verify this claim, $\mathcal{P}$ and $\mathcal{V}$ engage in a sumcheck protocol.

$\mathcal{P}$ sends $\mathcal{V}$ the univariate: $$f_1(X)=\sum _{x_2\in \{0,1\}}\sum _{x_3\in \{0,1\}}(3X{x}_2^2+4x_3{x}_2+5X^3{x}_3+2)=10X^3+6X+12.$$ $\mathcal{V}$ verifies that $(f_1(0)=12)+(f_1(1)=28)=40=H.$ Then, $\mathcal{V}$ samples the challenge $r_1=5$ and now $\mathcal{P}$ computes: $$f_2(X)=\sum _{x_3\in \{0,1\}}(3(5)X^2+4X{x}_3+5(5{)}^3{x}_3+2)=30X^2+4X+629.$$

$\mathcal{V}$ checks that $(f_2(0)=629)+(f_2(1)=663)=1292=f_1(5).$ Next, $\mathcal{V}$ samples another challenge $r_2=7$ and sends it to $\mathcal{P}$ who then computes and sends $f_3(X)=653X+737.$ Finally, $\mathcal{V}$ samples another random challenge $r_3=3$ and checks whether $f_3(3)=f(5,7,3).$ Indeed, $f_3=2696=f(5,7,3).$

Why Sumcheck?

In the previous section, we introduced the notion of a multilinear extension of a polynomial $f$, which is defined as $$\tilde{f}(x_1,\dots ,x_n)=\sum _{z_i\in \{0,1\}}\widetilde{\mathrm{eq}}(x;z)\cdot f(z_1,\dots ,z_n).$$ Notice that naturally, a multilinear extension is defined by taking the sum over a boolean hypercube, which is what sumcheck proves claims over.

In the next section, we will go over how we can encode layers of circuits as multilinear extensions, and prove statements about the output of these layers using sumcheck.

Encoding Layers in GKR

At this point, we have all the puzzle pieces needed to describe the GKR protocol -- layered arithmetic circuits, multilinear extensions, and sumcheck. This section talks about how we can tie all of these concepts together to verify claims on the output of an arithmetic circuit.

Grounding Example

We start with an example layered arithmetic circuit. Throughout this tutorial, we will provide this concrete example while simultaneously providing the generic steps of GKR.

Note some differences from the way this circuit is labeled as opposed to the example in the statement encoding section. Over here, we let the output be a nonzero value for the sake of the example (we explain how to transform any circuit with nonzero output to a circuit with zero output in a future section). Additionally, note that the gate labels start from $0$ in each layer, as opposed to the labels being unique throughout the entire circuit in the previous example. Because our gates ${\mathrm{add}}_{i,j,k}$ and ${\mathrm{mul}}_{i,j,k}$ are unique per triplet of layers $(i,j,k)$, we can start from $0$ in labeling the gates at the start of each layer.

In this example, $\mathcal{P}$ claims that the output of the following circuit is $45.$ Note that beyond the values in the input, and the actual structure of the circuit (what we refer to as the circuit description), $\mathcal{V}$ does not need any more information to verify the output of the circuit by computation:

This is because every node in every layer ${\mathcal{L}}_i$ with $i<d$ can be computed as the result of gates applied to nodes in previous layers.

At a high level, for the rest of this section we focus on encoding layers in two ways: as an MLE of its own, and using its relationship to other layers (via gates). We can equate these two encodings because they are of the same thing (the values in a single layer). With that, we have an equation we can perform a sumcheck over.

Encoding Layer Nodes as an MLE

We start by encoding the input layer in our example, and then show how this extends to the general case. More concretely, we want an MLE ${\tilde{V}}_j(x)$ such that ${\tilde{V}}_j(x)={\mathrm{val}}_j(x).$ Although it might not be immediately evident, because we eventually want to invoke the sumcheck protocol, it is useful to consider the inputs $x$ as bit-strings rather than integral values.

Example

Therefore, for example, we want ${\tilde{V}}_3(0,1)=3$ because ${\mathrm{val}}_3(1)=3$ and the bit-string $01$ represents $1$. Another way of restating our problem statement of encoding the input layer as some MLE ${\tilde{V}}_3(x_1,x_2)$ is to say "when $x=z$, output ${\mathrm{val}}_3(z).$

Here we can leverage the power of the $\widetilde{\mathrm{eq}}$ MLE: $${\tilde{V}}_3(x_1,x_2)=\sum _{b_1,b_2}\widetilde{\mathrm{eq}}(x_1,x_2;b_1,b_2)\cdot V_3(b_1,b_2),$$ or in other words: $${\tilde{V}}_3(x_1,x_2)=5(1-x_1)(1-x_2)+3(1-x_1)x_2+2x_1(1-x_2)+5x_1{x}_2.$$ You can independently verify that at each of the node input label values, $\tilde{V}(x)$ outputs the correct value.

General

Note that we conveniently defined the node labels to start from $0$ and naturally enumerate the nodes in each layer in our definition of ${\tilde{V}}_3(x_1,x_2)$ above. This allows us to generally extend the function $f(x)={\mathrm{val}}_i(x)$ which represents the nodes of layer $i$ into the following MLE: $${\tilde{V}}_i(x)=\sum _{z\in \{0,1{\}}^{s_i}}\widetilde{\mathrm{eq}}(x;z){\mathrm{val}}_i(z)$$ where $s_i$ is the $\log$ number of nodes in layer $i$.

Encoding Layers using their Relationship to other Layers

Another note we made when presenting the above diagram was that the only information that $\mathcal{V}$ needs to know immediately is the values of the input itself and the structure of the circuit. This is because the values of the future layers are determined by nodes in previous layers and the gates that connect them. Let's formalize this statement below.

Example

In the running example, let's fill in the layer ${\mathcal{L}}_2:$

We were able to fill this in because: $$\begin{array}{rlr}{\mathrm{val}}_2(0)& =& {\mathrm{val}}_3(1)+{\mathrm{val}}_3(2)\\ {\mathrm{val}}_2(1)& =& {\mathrm{val}}_3(0)\cdot {\mathrm{val}}_3(2)\\ {\mathrm{val}}_2(2)& =& {\mathrm{val}}_3(1)\cdot {\mathrm{val}}_3(3)\end{array}$$

So, while one way to write the MLE representing ${\mathcal{L}}_2$, as explained in the previous section, is $${\tilde{V}}_2(x_1,x_2)=5(1-x_1)(1-x_2)+10(1-x_1)x_2+15x_1(1-x_2),$$ we can also represent it by its relationship to the nodes in ${\mathcal{L}}_3:$ $$\begin{array}{rlr}{\tilde{V}}_2(x_1,x_2)& =& \widetilde{\mathrm{eq}}(x_1,x_2;0,0)({\tilde{V}}_3(0,1)+{\tilde{V}}_3(1,0))\\ & +& \widetilde{\mathrm{eq}}(x_1,x_2;0,1)({\tilde{V}}_3(0,0)\cdot {\tilde{V}}_3(1,0))\\ & +& \widetilde{\mathrm{eq}}(x_1,x_2;1,0)({\tilde{V}}_3(0,1)\cdot {\tilde{V}}_3(1,1))\end{array}$$ Note that in this definition, we still are linear in the variables $x_1,x_2.$

General

Now we go over how to write ${\tilde{V}}_i(x_1,x_2)$ in terms of ${\tilde{V}}_j(z)$ for $j>i.$ Recall the definition of ${\mathrm{add}}_{i,j,k}(z,x,y)$ and ${\mathrm{mul}}_{i,j,k}(z,x,y)$. For example, in the case of ${\mathcal{L}}_2$: $$\begin{gathered} {\mathrm{add}}_{2,3,3}((0,0),(0,1),(1,0))=1 \\ {\mathrm{mul}}_{2,3,3}((0,1),(0,0),(1,0))=1 \\ {\mathrm{mul}}_{2,3,3}((1,0),(0,1),(1,1))=1. \end{gathered}$$

If we use the indicator functions $\mathrm{add}$ and $\mathrm{mul}$ to translate the example above: $$\begin{gathered} {\tilde{V}}_i(x)=\sum _{z\in \{0,1{\}}^{s_i}}\sum _{x^{\prime }\in \{0,1{\}}^{s_j}}\sum _{y^{\prime }\in \{0,1{\}}^{s_k}}(\widetilde{\mathrm{eq}}(x;z){\mathrm{add}}_{i,j,k}(z,x^{\prime },y^{\prime })[{\mathrm{val}}_j(x^{\prime })+{\mathrm{val}}_k(y^{\prime })] \\ +\widetilde{\mathrm{eq}}(x;z){\mathrm{mul}}_{i,j,k}(z,x^{\prime },y^{\prime })[{\mathrm{val}}_j(x^{\prime })\cdot {\mathrm{val}}_k(y^{\prime })\left]\right) \end{gathered}$$ where $s_i,s_j,s_k$ are the number of bits needed to represent the node labels of that respective layer. We know that ${\mathrm{val}}_j(x^{\prime })$ and ${\mathrm{val}}_k(y^{\prime })$ can be computed using MLEs for ${\mathcal{L}}_j$ and ${\mathcal{L}}_k$, so we can rewrite the above as: $$\begin{gathered} {\tilde{V}}_i(x)=\sum _{z\in \{0,1{\}}^{s_i}}\sum _{x^{\prime }\in \{0,1{\}}^{s_j}}\sum _{y^{\prime }\in \{0,1{\}}^{s_k}}(\widetilde{\mathrm{eq}}(x;z){\mathrm{add}}_{i,j,k}(z,x^{\prime },y^{\prime })[{\tilde{V}}_j(x^{\prime })+{\tilde{V}}_k(y^{\prime })] \\ +\widetilde{\mathrm{eq}}(x;z){\mathrm{mul}}_{i,j,k}(z,x^{\prime },y^{\prime })[{\tilde{V}}_j(x^{\prime })\cdot {\tilde{V}}_k(y^{\prime })\left]\right). \end{gathered}$$ More detail and examples on transforming these indicator gate functions into MLEs are described in the section on canonic GKR.

Using the Equivalence between Layer Encodings

Now we have enough information to show how we can reduce claims on one layer to claims on the output of an MLE encoding a source layer (closer to the circuit input layer) for that layer.

Example

We start with the MLE encoding the output. $\mathcal{P}$ claims that the output of the circuit is $45$, i.e., ${\tilde{V}}_0=45$. Then, at any random point $\mathcal{V}$ challenges $\mathcal{P}$ with, say $g$, because ${\tilde{V}}_0$ is a constant function, an honest $\mathcal{P}$ claims that ${\tilde{V}}_0(g)=45$.

Another way, as expressed above to write ${\tilde{V}}_0(g)$ is as:

$$\begin{gathered} 45\stackrel{?}{=}{\tilde{V}}_0(g)=\sum _{z\in \{0,1{\}}^{s_0}}\sum _{x^{\prime }\in \{0,1{\}}^{s_j}}\sum _{y^{\prime }\in \{0,1{\}}^{s_k}}(\widetilde{\mathrm{eq}}(g;z){\mathrm{add}}_{0,1,1}(z,x^{\prime },y^{\prime })[{\tilde{V}}_1(x^{\prime })+{\tilde{V}}_1(y^{\prime })] \\ +\widetilde{\mathrm{eq}}(g;z){\mathrm{mul}}_{0,1,1}(z,x^{\prime },y^{\prime })[{\tilde{V}}_1(x^{\prime })\cdot {\tilde{V}}_1(y^{\prime })\left]\right). \end{gathered}$$

Note that while we expicitly write $z$ to maintain consistency between earlier examples, in this case, because there is only one output, there are no $z$ variables. Therefore, ${\mathrm{add}}_{0,1,1}(z,x,y)$ and ${\mathrm{mul}}_{0,1,1}(z,x,y)$ are constant functions, and their extensions are equal to their value in their first position: ${\mathrm{add}}_{0,1,1}(0,x,y)$ and ${\mathrm{mul}}_{0,1,1}(0,x,y)$.

$\mathcal{P}$ and $\mathcal{V}$ engage in a sumcheck protocol to verify this claim of the sum of a polynomial over the boolean hypercube. Recall that sumcheck requires binding the variables that the sum is over (in this case, $z,x^{\prime },y^{\prime }$), one by one, with random challenges.

If we follow the sumcheck protocol as is, at the end, $x$ is bound to $u$ and $y$ is bound to $v$. Let's say the prover's final univariate is $f_{s_j+s_k}(X)$ and the verifier's final challenge is $v_k.$ Then, we end with the final claim:

$$f_{s_k+s_k}(v_k)\stackrel{?}{=}{\mathrm{add}}_{0,1,1}(0,u,v)[{\tilde{V}}_1(u)+{\tilde{V}}_1(v)]+{\mathrm{mul}}_{0,1,1}(0,u,v)[{\tilde{V}}_1(u)\cdot {\tilde{V}}_1(v)].$$

$\mathcal{V}$ knows the structure of the circuit, so they can compute ${\mathrm{add}}_{0,1,1}(p,u,v),{\mathrm{mul}}_{0,1,1}(p,u,v)$ on their own. Additionally, $\widetilde{\mathrm{eq}}$ is publically computable, so $\mathcal{V}$ computes that on their own as well. Normally, sumcheck would require $\mathcal{V}$ make a query to an "oracle" to verify the claimed values $V_1(u)\stackrel{?}{=}{c}_1$ and ${\tilde{V}}_1(v)\stackrel{?}{=}{h}_2$.

However, instead we say that $\mathcal{P}$ "reduces" the claim that ${\tilde{V}}_0(g)\stackrel{?}{=}45$ to two claims on ${\tilde{V}}_1:V_1(u)\stackrel{?}{=}{c}_1;{\tilde{V}}_1(v)\stackrel{?}{=}{c}_2.$

Similarly, ${\tilde{V}}_1$ has a relationship to MLEs in later layers, so the sumcheck on ${\tilde{V}}_1$ will reduce to claims on these MLEs, eventually propagating to claims on the input layer.

For another example of claim reduction for structured GKR, see this section.

General

In general, GKR works very similarly to the example above. We cover the case where $\mathcal{V}$ expects the output of the circuit to be $0$. $\mathcal{P}$ receives a challenge from $\mathcal{V},g$ and claims that the MLE representing ${\mathcal{L}}_0$ still evaluates to $0$ over that random point. I.e., $\mathcal{P}$ claims that ${\tilde{V}}_0(g)=0.$ Using the encoding of ${\tilde{V}}_0$ using later layers, $\mathcal{P}$ reduces its claim on the output of the circuit to evaluations of MLEs representing future layers.

Note that there is an exponential blow-up of claims when reducing claims on one layer to the next. We describe a protocol to aggregate claims (and therefore achieve a one-to-one reduction) in the claims section.

Circuit Description

Throughout this section, we refer to $\mathcal{V}$ using the description of the circuit in order to evaluate the gates or to understand the layerwise relationships on their own. The circuit description is something agreed upon beforehand with $\mathcal{P}$ and $\mathcal{V}$ and visible to both parties -- it is the "shape" of the circuit, which includes how many nodes each layer contains, the number of layers, and which gates connect nodes from layer to layer.

Therefore, the circuit description of our example circuit is this:

Note: Transforming a Circuit to have Zero Output

In Remainder, $\mathcal{V}$ expects circuits to have output $0$. This is because certain types of circuits (such as those resulting from LogUp) require the output to specifically be $0$, and $\mathcal{V}$ needs to specifically verify this fact.

If a circuit does not have output $0$, one way to transform this is to add the negative of the expected output to the input. The last layer of the circuit can be the sum of this expected output, and the actual output of the circuit. This results in a circuit with the output layer evaluating to $0$. We show this transformation applied to our example above:

GKR Theory Overview

Read the introduction and ready to dive into some deeper GKR theory concepts? Let's go!

Structured ("Sector") GKR

Source: Tha13, section 5 ("Time-Optimal Protocols for Circuit Evaluation").

Review: Equality MLE

We begin by briefly recalling the $\widetilde{\mathrm{eq}}$ MLE (see this section for more details). We first consider the binary string equality function $\mathrm{eq}:\{0,1{\}}^{2n}\mapsto \{0,1\}$, where

$$\mathrm{eq}(X_1,...,X_n;Y_1,...,Y_n)=\{\begin{array}{ll}1& \text{if ∀i:Xi=Yi}\\ 0& \text{otherwise}\end{array}$$

This function is $1$ if and only if $X$ and $Y$ are equal as binary strings, and $0$ otherwise. We can extend this to a multilinear extension via the following -- consider $\widetilde{\mathrm{eq}}:{\mathbb{F}}^{2n}\mapsto \mathbb{F}$, where

$$\widetilde{\mathrm{eq}}(X_1,...,X_n;Y_1,...,Y_n)=\prod _{i=1}^n(1-X_i)(1-Y_i)+X_i{Y}_i$$

Structured Layerwise Relationship

See Tha13, page 25 ("Theorem 1") for a more rigorous treatment. Note that Remainder does not implement Theorem 1 in its entirety, and that many circuits which do fulfill the criteria of Theorem 1 are currently not expressible within Remainder's circuit frontend.

Structured layerwise relationships can loosely be thought of as data relationships where the bits of the index of the "destination" value in the $i$'th layer are a (optionally subset) permutation of the bits of the index of the "source" value in the $j$'th layer for $j>i$. As a concrete example, we consider a layerwise relationship where the destination layer is half the size, and its values are the element-wise products of the two halves of the source layer's values: Let ${\tilde{V}}_i(Z_1,Z_2)$ represent the MLE of the destination layer, and let ${\tilde{V}}_j(Z_1,Z_2,Z_3)$ represent the MLE of the source layer.

Let the evaluations of ${\tilde{V}}_j$ over the hypercube be $[a,b,c,d,e,f,g,h]$. Then we wish to create a layerwise relationship such that the evaluations of ${\tilde{V}}_i$ over the hypercube are $[ae,bf,cg,dh]$. We can actually write this as a simple rule in terms of the (integer) indices of $V_i$ as follows:

$$V_i(z)=V_j(z)\cdot V_j(4+z)$$

If we allow for our arguments to be the binary decomposition of $z$ rather than $z$ itself, we might have the following relationship:

$$V_i(z_1,z_2)=V_j(0,z_1,z_2)\cdot V_j(1,z_1,z_2)$$

where $0z_1{z}_2$ is the binary representation of $z$ and $1z_1{z}_2$ is the binary representation of $4+z$. This is in fact very close to the exact form-factor of the polynomial layerwise relationship which we should create between the layers -- we now consider the somewhat un-intuitive relationship

$$V_i(Z_1,Z_2)=\sum _{b_1,b_2\in \{0,1{\}}^2}\mathrm{eq}(Z_1,Z_2;b_1,b_2)\cdot V_j(0,b_1,b_2)\cdot V_j(1,b_1,b_2)$$

One way to read the above relationship is the following: for any (binary decomposition) $Z_1,Z_2$, the value of the $i$'th layer at the index represented by $Z_1,Z_2$ should be $V_j(0,Z_1,Z_2)\cdot V_j(1,Z_1,Z_2)$. We are summing over all possible values of the hypercube above, $b_1,b_2\in \{0,1{\}}^2$, and for each value we check whether the current iterated hypercube value $b_1,b_2$ "equals" the argument $Z_1,Z_2$ value. If so, we contribute $V_j(0,b_1,b_2)\cdot V_j(1,b_1,b_2)$ to the sum and if not, we contribute zero to the sum.

In this way we see for $Z_1,Z_2\in \{0,1\}$ that all of the summed values will be zero except for when $b_1,b_2$ are exactly identical to $Z_1,Z_2$, and thus only the correct value $V_j(0,b_1,b_2)\cdot V_j(1,b_1,b_2)$ will contribute to the sum (and thus the value of $V_i(Z_1,Z_2)$).

As described, the above relationship looks extremely inefficient in some sense -- why bother summing over all the hypercube values when we already know that all of them will be zero because $\mathrm{eq}$ will evaluate to zero at all values except one?

The answer is that it's not enough to only consider $V_i(Z_1,Z_2)$ for binary $Z_1,Z_2$, as our claims will be of the form ${\tilde{V}}_i(g_1,g_2)=c$, where $g_1,g_2,c\in \mathbb{F}$, and ${\tilde{V}}_i$ is the multilinear extension of $V_i$ (see claims section for more information on prover claims). Another way to see this is that the above relationship is able to be shown for each $Z_1,Z_2\in \{0,1\}$, but we want to make sure that the relationship holds for all $Z_1,Z_2\in \{0,1\}$. Rather than checking each index individually, it's much more efficient to check a "random combination" of all values simultaneously by evaluating ${\tilde{V}}_i$ at a random point $g_1,g_2$. We thus have, instead, that

$${\tilde{V}}_i(Z_1,Z_2)=\sum _{b_1,b_2\in \{0,1{\}}^2}\widetilde{\mathrm{eq}}(Z_1,Z_2;b_1,b_2)\cdot {\tilde{V}}_j(0,b_1,b_2)\cdot {\tilde{V}}_j(1,b_1,b_2)$$

Since ${\tilde{V}}_i$ is identical to $V_i$ (and similarly for $\widetilde{\mathrm{eq}}$ and ${\tilde{V}}_j$) everywhere on the hypercube, the above relationship should still hold for all binary $Z_1,Z_2$. Moreover, the above relationship is now one which we can directly apply sumcheck to, since we have a summation over the hypercube!

But wait, you might say. This still seems wasteful -- why are we bothering with this summation and $\widetilde{\mathrm{eq}}$ polynomial? Why can't we just have something like

$${\tilde{V}}_i(Z_1,Z_2)={\tilde{V}}_j(0,Z_1,Z_2)\cdot {\tilde{V}}_j(1,Z_1,Z_2)$$

Unfortunately the above relationship cannot work, as $Z_1,Z_2$ are linear on the LHS and quadratic on the RHS. The purpose of the summation and $\widetilde{\mathrm{eq}}$ polynomial is to "linearize" the RHS and quite literally turn any high degree polynomial (such as ${\tilde{V}}_j(0,Z_1,Z_2)\cdot {\tilde{V}}_j(1,Z_1,Z_2)$) into its unique multilinear extension (recall the definition of multilinear extension).

We see that the general pattern of creating a "structured" layerwise relationship is as follows:

• First, write the relationship in terms of the binary indices of values between each layer. In our case, $V_i(z_1,z_2)=V_j(0,z_1,z_2)\cdot V_j(1,z_1,z_2)$.
• Next, replace $z_i$ on the LHS of the equation with formal variable $Z_i\in \mathbb{F}$, and allow the LHS to be a multilinear extension. We now have ${\tilde{V}}_i(Z_1,Z_2)$ on the LHS.
• Next, replace $z_i$ on the RHS of the equation with boolean $b_i$ values and add an $\widetilde{\mathrm{eq}}$ predicate between $Z_i,b_i$, and add a summation over all $b_i$ values. Additionally, extend all $V_j$ to their multilinear extensions ${\tilde{V}}_j$ (this is importantly only for sumcheck):