I'd like to thank Nicolas Mohnblatt for brainstorming, discussing and reviewing this article, and for his many shared insights. I'm also thankful to Srinath Setty, Jamie Gabbay and Apriori for their generous feedback. This article wouldn't have been possible without them. All mistakes are my own.

This article was originally written on a SageMath Jupyter notebook, which can be found here.

Introduction

The sum-check protocol is like one of those magic tricks that, despite having been exposed to how it works, it still makes your mind do some acrobatics every time you see it applied.

Any polynomial equation can be transformed into an instance of the sum-check, making this amazing algorithm surprisingly applicable.

Since the sum-check lies at the core of the HyperNova's folding techniques, we will dive first into its details on a simpler case: the checking of a Customisable Constraint System (CCS) instance using the SuperSpartan’s polynomial IOP as described in their paper.

Transforming any check into a sumcheck

The goal of the sum-check is to check that an untrusted prover has computed the following equation correctly, where $f\in K[X_1,\mathrm{.}\mathrm{.}\mathrm{.},X_l]f\; \backslash in\; K[X\_1,...,X\_l]$ is a multivariate polynomial (not necessarily multilinear):

After $ll$ rounds, the protocol allows the verifier to check $f(r_1,\mathrm{.}\mathrm{.}\mathrm{.},r_l)=cf(r\_1,...,r\_l)\; =\; c$, for some random $r_i\in \mathbb{F}r\_i\; \backslash in\; \backslash mathbb\{F\}$, which with high probability implies the original equation, due to the Schwartz-Zippel lemma.

Say we have a polynomial $ff$ encoding a vector of evaluations $v=[v_1,\mathrm{.}\mathrm{.}\mathrm{.},v_n]v\; =\; [v\_1,...,\; v\_\{n\}]$ such that for all $x_{i}x\_i$ in some subdomain $HH$, $f(x_i)=v_{i}f(x\_i)\; =\; v\_i$. In our setting, a prover wants to convince a verifier that this is the case (i.e. $\mathrm{\forall }{x}_i\in H\mathrm{.}f(x_i)=v_i\backslash forall\; x\_i\; \backslash in\; H.\; f(x\_i)\; =\; v\_i$). If every $v_i=0v\_i\; =\; 0$, this is known as a zero-check.

Note that we can always transform the check $f(x_i)=v_{i}f(x\_i)\; =\; v\_i$ into a zero-check since $f(x_i)-v_i=0f(x\_i)\; -\; v\_i\; =\; 0$.

For example, in vanilla Plonk, $ff$ is a univariate polynomial that encodes an execution trace and $HH$ is a subset of the roots of unity of some prime field (e.g. $H:=\{{\omega }^1,{\omega }^2,{\omega }^3,{\omega }^4,{\omega }^5,{\omega }^6,{\omega }^7,{\omega }^8\}H\; :=\; \backslash \{\backslash omega^1,\backslash omega^2,\backslash omega^3,\backslash omega^4,\backslash omega^5,\backslash omega^6,\backslash omega^7,\backslash omega^8\backslash \}$).

In HyperPlonk (a variant of Plonk that transforms the zero-checks in the protocol into sumchecks), $HH$ becomes a boolean hypercube $\{0,1{\}}^l\backslash \{0,1\backslash \}^l$ (i.e. all the $ll$ combinations of zeroes and ones), and $ff$ a multivariate polynomial of some degree $dd$ such that $\mathrm{\forall }x\in \{0,1{\}}^l\mathrm{.}f(x)=0\backslash forall\; x\; \backslash in\; \backslash \{0,1\backslash \}^l.\; f(x)\; =\; 0$. For example, if $ll$ is set to 3, then $H:=\{0,1{\}}^3=\{(0,0,0),(0,0,1),(0,1,0),(0,1,1),(1,0,0),(1,0,1),(1,1,0),(1,1,1)\}H\; :=\; \backslash \{0,1\backslash \}^3\; =\; \backslash \{(0,0,0),\; (0,0,1),\; (0,1,0),\; (0,1,1),\; (1,0,0),\; (1,0,1),\; (1,1,0),\; (1,1,1)\backslash \}$

To apply the sum-check protocol, we need a statement of the form ${\sum }_{x\in \{0,1{\}}^l}f(x)=0\backslash sum\_\{x\backslash in\; \backslash \{0,1\backslash \}^l\}\; f(x)\; =\; 0$.

It is clear that if $\mathrm{\forall }x\in \{0,1{\}}^l\mathrm{.}f(x)=0\backslash forall\; x\backslash in\; \backslash \{0,1\backslash \}^l.\; f(x)\; =\; 0$ then ${\sum }_{x\in \{0,1{\}}^l}f(x)=0\backslash sum\_\{x\backslash in\; \backslash \{0,1\backslash \}^l\}\; f(x)\; =\; 0$, but the converse doesn't necessarily hold. For example, $f((0,0,1))=-1f((0,0,1))\; =\; -1$, $f((0,1,0))=1f((0,1,0))\; =\; 1$ and $f(x)=0f(x)\; =\; 0$ otherwise makes ${\sum }_{x\in \{0,1{\}}^l}f(x)=0\backslash sum\_\{x\backslash in\; \backslash \{0,1\backslash \}^l\}\; f(x)\; =\; 0$ but $f(x)\mathrm{\ne }0f(x)\; \backslash neq\; 0$ for some $x\in \{0,1{\}}^{l}x\backslash in\; \backslash \{0,1\backslash \}^l$.

To overcome this, we define a different multilinear polynomial:

That is

$\widetilde{eq}(X_1,X_2):={\prod }_{j=1}^l((1-X_{1_j})(1-X_{2_j})+X_{1_j}{X}_{2_j})\backslash widetilde\{eq\}(X\_1,\; X\_2)\; :=\; \backslash prod\_\{j=1\}^l\; ((1-X\_\{1\_j\})(1-X\_\{2\_j\})\; +\; X\_\{1\_j\}\; X\_\{2\_j\})$.

We use a tilde ~ over a function $gg$ to emphasise that $\tilde{g}\backslash widetilde\{g\}$ is a multilinear polynomial.

k = GF(101)

R = PolynomialRing(k, 10, "x1, x2, y1, y2, y3, x11, x22, y11, y22, y33")
x1, x2, y1, y2, y3, x11, x22, y11, y22, y33 = R.gens()

eqx = ((1 - x1)*(1 - x11) + x1*x11) * ((1 - x2)*(1 - x22) + x2*x22)
eqy = ((1 - y1)*(1 - y11) + y1*y11) * ((1 - y2)*(1 - y22) + y2*y22) * ((1 - y3)*(1 - y33) + y3*y33)

eqx(x1=1, x2=1, x11=1, x22=0)

0

The new polynomial $\widetilde{eq}\backslash widetilde\{eq\}$ together with the sum-check protocol will allow us to compute the desired zero-check, $\mathrm{\forall }x\in H\mathrm{.}f(x)=0\backslash forall\; x\; \backslash in\; H.\; f\; (x)\; =\; 0$, as follows:

We define a new polynomial

Note that $XX$ is a variable while $xx$ is not. $hh$ is known as a multilinear extension of $ff$ in the boolean hypercube, since $\mathrm{\forall }X\in \{0,1{\}}^l\mathrm{.}h(X)=f(X)\backslash forall\; X\backslash in\; \backslash \{0,1\backslash \}^l.\; h(X)\; =\; f(X)$. That is, $ff$ is defined over $\{0,1{\}}^l\backslash \{0,1\backslash \}^l$ while $hh$ is defined over ${\mathbb{F}}^l\backslash mathbb\{F\}^l$.

For example, if $X=(1,0,1)X\; =\; (1,0,1)$, then $h((1,0,1))={\sum }_{x\in \{0,1{\}}^l}f(x)\cdot \widetilde{eq}(x,(1,0,1))=f((1,0,1))h((1,0,1))\; =\; \backslash sum\_\{x\; \backslash in\; \backslash \{0,1\backslash \}^l\}\; f(x)\; \backslash cdot\; \backslash widetilde\{eq\}(x,\; (1,0,1))\; =\; f((1,0,1))$.

Since $\mathrm{\forall }x\in \{0,1{\}}^l\mathrm{.}f(x)=0\backslash forall\; x\backslash in\; \backslash \{0,1\backslash \}^l.\; f(x)\; =\; 0$, and $\mathrm{\forall }X\in \{0,1{\}}^l\mathrm{.}h(X)=f(X)\backslash forall\; X\backslash in\; \backslash \{0,1\backslash \}^l.\; h(X)=f(X)$, then $\mathrm{\forall }X\in \{0,1{\}}^l\mathrm{.}h(X)=0\backslash forall\; X\backslash in\; \backslash \{0,1\backslash \}^l.\; h(X)\; =\; 0$.

The main difference between $ff$ and $hh$ is that $ff$ is a multivariate polynomial of (potentially high) degree $dd$, whereas $hh$ is a multilinear polynomial.

We know that a univariate polynomial $gg$ of $k>1k>1$ coefficients in uniquely determined by $kk$ evaluations, and it is of degree $k-1k-1$. Similarly, a multilinear polynomial $hh$ of $kk$ variables is uniquely determined by $2^{k}2^k$ evaluations.

In this case, $h(Y):={\sum }_{x\in \{0,1{\}}^l}f(x)\cdot \widetilde{eq}(x,Y)h(Y)\; :=\; \backslash sum\_\{x\; \backslash in\; \backslash \{0,1\backslash \}^l\}\; f(x)\; \backslash cdot\; \backslash widetilde\{eq\}(x,\; Y)$ has $2^{l}2^l$ coefficients (most of them zero) and so it is uniquely determined by $2^{l}2^l$ evaluations. Since $\mathrm{\forall }\{0,1{\}}^l\mathrm{.}h(Y)=f(Y)=0\backslash forall\; \backslash \{0,1\backslash \}^l.\; h(Y)\; =\; f(Y)\; =\; 0$, then $hh$ is zero at $2^{l}2^l$ points and must necessarily be the zero polynomial, $h=0h\; =\; 0$.

The verifier has reduced his task to checking that $hh$ is indeed the zero polynomial, which is a simpler problem.

By the Schwartz-Zippel lemma, we can verify that $hh$ is the zero polynomial with high probability by evaluating $hh$ at a random point $r\in {\mathbb{F}}^{l}r\; \backslash in\; \backslash mathbb\{F\}^l$.

That is, $h(r):={\sum }_{x\in \{0,1{\}}^l}f(x)\cdot \widetilde{eq}(x,r)h(r)\; :=\; \backslash sum\_\{x\; \backslash in\; \backslash \{0,1\backslash \}^l\}\; f(x)\; \backslash cdot\; \backslash widetilde\{eq\}(x,\; r)$ must be equal to zero. Here is where we apply the sum-check protocol.

So if $h(r)=0h(r)\; =\; 0$, this implies with high probability that $h=0h\; =\; 0$, which implies that $\mathrm{\forall }Y\in \{0,1{\}}^l\mathrm{.}h(Y)=0\backslash forall\; Y\; \backslash in\; \backslash \{0,1\backslash \}^l.\; h(Y)\; =\; 0$, which implies that $\mathrm{\forall }x\in \{0,1{\}}^l\mathrm{.}f(x)=0\backslash forall\; x\backslash in\; \backslash \{0,1\backslash \}^l.\; f(x)\; =\; 0$, thus proving the original statement with high probability (w.h.p.). In short,

$h(r)=0h=0⟹\mathrm{\forall }Y\in \{0,1{\}}^l\mathrm{.}h(Y)=0⟹\mathrm{\forall }x\in \{0,1{\}}^l\mathrm{.}f(x)=0h(r)\; =\; 0\; \backslash overset\{w.h.p\}\{\backslash Longrightarrow\}\; h\; =\; 0\; \backslash Longrightarrow\; \backslash forall\; Y\; \backslash in\; \backslash \{0,1\backslash \}^l\; .\; h(Y)\; =\; 0\; \backslash Longrightarrow\; \backslash forall\; x\backslash in\; \backslash \{0,1\backslash \}^l.\; f(x)\; =\; 0$.

Example: A Fibonacci relation

The following recurrence relation is tailored to help us illustrate the workings sum-check protocol for CCS relations as is used in HyperNova. This example reflects the SuperSpartan’s polynomial IOP for CCS protocol described in the CCS paper.

// i-th iteration
fibonnaci(x_2, x_1, y_2, y_1) {
    x = x_1 + x_2 // Fibonacci
    y = y_1 * y_2 // Multiplicative Fibonacci
    t = x * y     // Fibonacci x (Multiplicative Fibonacci)
    (x, y, t)
}

In the second part of this post, we will prove the result of iterating $nn$ times over $ff$, starting with some initial values, by applying the folding techniques in HyperNova.

For now, we focus on proving a single iteration, in particular, that which results from the initial values $x_2=0,x_1=1,y_2=2,y_1=3x\_2\; =\; 0,\; x\_1\; =\; 1,\; y\_2=2,\; y\_1=3$ that outputs $x=1,y=6,t=6x\; =\; 1,\; y=6,\; t=6$.

So we first need to arithmetise this statement.

A CCS primer

Customisable Constraint System (CCS) relations are a generalisation of R1CS relations.

In particular, a relation $\mathcal{R}\backslash mathcal\{R\}$ in CCS is composed by:

• a structure $s:=([M_1,\mathrm{.}\mathrm{.}\mathrm{.},M_t],[S_1,\mathrm{.}\mathrm{.}\mathrm{.},S_q],[c_1,\mathrm{.}\mathrm{.}\mathrm{.},c_q])s\; :=\; ([M\_1,\; ...,\; M\_t],\; [S\_1,...,S\_q],\; [c\_1,\; ...,\; c\_q])$, plus some other bound parameters such as the number of rows $mm$ and columns $nn$ of the matrices $M_{i}M\_i$.
• an instance, which consists of public inputs $\times \in {\mathbb{F}}^l\backslash times\; \backslash in\; \backslash mathbb\{F\}^l$ and private inputs $\omega \in {\mathbb{F}}^m\backslash omega\; \backslash in\; \backslash mathbb\{F\}^m$.

that satisfies:

$\begin{array}{c}{\displaystyle \sum _{i=0}^{q-1}{c}_i\cdot {\circ }_{j\in S_i}{M}_j\cdot z=\vec{0}}\end{array}\backslash begin\{aligned\}\; \backslash sum\_\{i=0\}^\{q-1\}\; c\_i\; \backslash cdot\; \backslash circ\_\{j\; \backslash in\; S\_i\}\; M\_j\; \backslash cdot\; z\; =\; \backslash vec\{0\}\; \backslash end\{aligned\}$

where:

• $z:=(\omega ,x,1)\in {\mathbb{F}}^{n}z\; :=\; (\backslash omega,\; x,\; 1)\; \backslash in\; \backslash mathbb\{F\}^n$.
• $x\in {\mathbb{F}}^{l}x\; \backslash in\; \backslash mathbb\{F\}^\{l\}$ are the public inputs.
• $\omega \in {\mathbb{F}}^{m-l-1}\backslash omega\; \backslash in\; \backslash mathbb\{F\}^\{m\; -\; l\; -\; 1\}$ are the private inputs.
• $M_j\cdot zM\_j\; \backslash cdot\; z$ denotes matrix-vector multiplication,
• $\circ \backslash circ$ denotes the Hadamard product between vectors
• $\vec{0}\backslash vec\; 0$ is an $mm$-sized vector with entries equal to the the additive identity $0\in \mathbb{F}0\; \backslash in\; \backslash mathbb\{F\}$.

Expanded, a CCS equation looks like:

$\begin{array}{c}{\displaystyle c_0\cdot \stackrel{j_i\in S_0}{\overbrace{(M_{j_0}\cdot z\circ \mathrm{.}\mathrm{.}\mathrm{.}\circ M_{j_{\mathrm{\mid }{S}_0\mathrm{\mid }-1}}\cdot z)}}+\mathrm{.}\mathrm{.}\mathrm{.}+c_{q-1}\cdot \stackrel{j_i\in S_{q-1}}{\overbrace{(M_{j_0}\cdot z\circ \mathrm{.}\mathrm{.}\mathrm{.}\circ M_{j_{\mathrm{\mid }{S}_{q-1}\mathrm{\mid }-1}}\cdot z)}}=\vec{0}}\end{array}\backslash begin\{aligned\}\; c\_0\; \backslash cdot\; \backslash overbrace\{(M\_\{j\_\{0\}\}\; \backslash cdot\; z\; \backslash circ\; ...\; \backslash circ\; M\_\{j\_\{|\{S\_\{0\}\}|-1\}\}\; \backslash cdot\; z)\}^\{j\_i\; \backslash in\; S\_0\}\; +\; ...\; +\; c\_\{q-1\}\; \backslash cdot\; \backslash overbrace\{(M\_\{j\_\{0\}\}\; \backslash cdot\; z\; \backslash circ\; ...\; \backslash circ\; M\_\{j\_\{|\{S\_\{q-1\}\}|-1\}\}\; \backslash cdot\; z)\}^\{j\_i\; \backslash in\; S\_\{q-1\}\}\; =\; \backslash vec\{0\}\; \backslash end\{aligned\}$.

In our case, $m=4m\; =\; 4$ and $n=8n\; =\; 8$ are the rows and columns of the $t=3t=3$ matrices $M_1,M_2,M_{3}M\_1,\; M\_2,\; M\_3$. $\{M_1,M_2\}\backslash \{M\_1,\; M\_2\backslash \}$ are multiplied and added to $\{M_3\}\backslash \{M\_3\backslash \}$, so $S_1=\{1,2\},S_2=\{3\}S\_1\; =\; \backslash \{1,\; 2\backslash \},\; S\_2\; =\; \backslash \{3\backslash \}$. Since there are two addends $S_{1}S\_1$ and $S_{2}S\_2$, $q=2q\; =2$.

A Fibonacci CCS relation

The Fibonacci combined recurrence relation of our example can easily be represented as a CCS relation:

$c_1\cdot (M_1\cdot z\circ M_2\cdot z)+c_2\cdot (M_3\cdot z)=\vec{0}c\_1\; \backslash cdot\; (M\_1\; \backslash cdot\; z\; \backslash circ\; M\_2\; \backslash cdot\; z)\; +\; c\_2\; \backslash cdot\; (M\_3\; \backslash cdot\; z)\; =\; \backslash vec\{0\}$

We have a particular interest in having our rows and columns of size $2^{m}2^m$ for some $mm$, since the sum-check protocol runs over the boolean hypercube. In this case, $m=4=2^{2}m\; =\; 4\; =\; 2^2$ is the number of constraints (i.e. rows) and $n=8=2^{3}n\; =\; 8\; =\; 2^3$ is the number of witnesses (i.e. columns) as well as the size of the vector $zz$.

Note that we have added a dummy row is $[0,\mathrm{.}\mathrm{.}\mathrm{.},0][0\; ,...,\; 0]$ for $M_1,M_2,M_{3}M\_1,\; M\_2,\; M\_3$ (it could be any other vector as long as the CCS relation holds trivially).

M1 = Matrix(k, [
    [1,1,0,0,0,0,0,0],
    [0,0,0,0,1,0,0,0],
    [0,0,1,0,0,0,0,0],
    [0,0,0,0,0,0,0,0]
])

M2 = Matrix(k, [
    [0,0,0,0,0,0,0,1],
    [0,0,0,1,0,0,0,0],
    [0,0,0,0,0,1,0,0],
    [0,0,0,0,0,0,0,0]
])

M3 = Matrix(k, [
    [0,0,1,0,0,0,0,0],
    [0,0,0,0,0,1,0,0],
    [0,0,0,0,0,0,1,0],
    [0,0,0,0,0,0,0,0]
])

# First iteration
x = [0,1,1,2,3,6,6]
w = []
z1 = vector(k, x + w + [1])

# CCS relation check
1 * (M1*z1.column()).elementwise_product(M2*z1.column())-(M3*z1.column()) == vector([0,0,0,0]).column()

m = M1.nrows()
n = M1.ncols()

(m, n)

Transforming CCS relation into a sum-check

We want to turn this matrix-vector problem statement into a sum over the boolean hypercube.

We begin by creating multilinear extensions $\widetilde{M_i}\backslash widetilde\{M\_i\}$ of $M_{i}M\_i$ and $\tilde{z}\backslash widetilde\{z\}$ of $zz$ such that the multilinear polynomial

is a multilinear extension of our matrix-vector product $M_i\cdot zM\_i\; \backslash cdot\; z$.

Since $m=2^{2}m=2^2$ and $n=8=2^{3}n=8\; =\; 2^3$, then $\log m=2\backslash log\; m\; =\; 2$, $\log n=3\backslash log\; n\; =\; 3$, and

.

Note that a matrix $MM$ can be seen as a function $M:\{0,1{\}}^{\log m}\times \{0,1{\}}^{\log n}\to \mathbb{F}M\; :\; \backslash \{0,1\backslash \}^\{\backslash log\; m\}\; \backslash times\; \backslash \{0,1\backslash \}^\{\backslash log\; n\}\; \backslash to\; \backslash mathbb\{F\}$, since for each row $m_{i}m\_i$ and column $n_{j}n\_j$ we can derive the element $M(m_i,n_j)M(m\_i,\; n\_j)$ from the matrix $MM$. As in the HyperNova paper, we will denote $s=\log ms\; =\; \backslash log\; m$ and $s^{\mathrm{\prime }}=\log ns\text{'}\; =\; \backslash log\; n$.

The multilinear extensions $\widetilde{M_i}\backslash widetilde\{M\_i\}$ of $M_{i}M\_i$ and $\tilde{z}\backslash widetilde\{z\}$ of $zz$ are defined as

$\tilde{z}(Y):={\sum }_{y\in \{0,1{\}}^{s^{\mathrm{\prime }}}}z(y)\cdot \widetilde{eq}(y,Y)\backslash widetilde\{z\}(Y)\; :=\; \backslash sum\_\{y\; \backslash in\; \backslash \{0,\; 1\; \backslash \}^\{s\text{'}\}\}\; z(y)\; \backslash cdot\; \backslash widetilde\{eq\}(y,\; Y)$.

Setting $s=\log m=\log 4=2,s^{\mathrm{\prime }}=\log n=\log 8=3s=\; \backslash log\; m\; =\; \backslash log\; 4\; =\; 2,\; s\text{'}=\; \backslash log\; n\; =\; \backslash log\; 8\; =\; 3$ as in our example:

$$\tilde{z}((Y_1,Y_2,Y_3)):=\sum _{y_1\in \{0,1\}}\sum _{y_2\in \{0,1\}}\sum _{y_3\in \{0,1\}}z((y_1,y_2,y_3))\cdot \widetilde{eq}((y_1,y_2,y_3),(Y_1,Y_2,Y_3))\backslash widetilde\{z\}((Y\_1,\; Y\_2,\; Y\_3))\; :=\; \backslash sum\_\{y\_1\; \backslash in\; \backslash \{0,\; 1\; \backslash \}\}\backslash sum\_\{y\_2\; \backslash in\; \backslash \{0,\; 1\; \backslash \}\}\backslash sum\_\{y\_3\; \backslash in\; \backslash \{0,\; 1\; \backslash \}\}\; z((y\_1,\; y\_2,\; y\_3))\; \backslash cdot\; \backslash widetilde\{eq\}((y\_1,\; y\_2,\; y\_3),\; (Y\_1,\; Y\_2,\; Y\_3))$$

# From-binary-to-decimal polynomials
row = x1 + 2*x2
col = y1 + 2*y2 + 4*y3

def Mi_linear(Mi):
    return sum([
            sum([
                sum([
                    sum([
                        sum([
                            Mi[Integer(row(x1=x1, x2=x2))][Integer(col(y1=y1,y2=y2,y3=y3))] * eqx(x1=x1,x2=x2,x11=x11,x22=x22) * eqy(y1=y1, y11=y11, y2=y2, y22=y22, y3=y3, y33=y33)
                        for y3 in [0,1]])
                    for y2 in [0,1]])
                for y1 in [0,1]])
            for x2 in [0,1]])
         for x1 in [0,1]])

def z_linear(zi):
    return sum([
                sum([
                    sum([
                        zi[Integer(col(y1=y1,y2=y2,y3=y3))]* eqy(y1=y1, y11=y11, y2=y2, y22=y22, y3=y3, y33=y33)
                    for y3 in [0,1]])
                for y2 in [0,1]])
            for y1 in [0,1]])

Thus the multilinear extension $f_{i}f\_i$ of our matrix-vector product $M\cdot zM\; \backslash cdot\; z$ is

$f_i((X_1,X_2))={\sum }_{y\in \{0,1{\}}^3}\widetilde{M_i}((X_1,X_2),y)\cdot \tilde{z}(y)f\_i((X\_1,\; X\_2))\; =\; \backslash sum\_\{y\; \backslash in\; \backslash \{0,\; 1\; \backslash \}^3\}\; \backslash widetilde\{M\_i\}((X\_1,\; X\_2),\; y)\; \backslash cdot\; \backslash widetilde\{z\}(y)$

def Mi_z_prod(Mi, zi):
        return sum([
                sum([
                    sum([
                        Mi_linear(Mi)(y11=y1,y22=y2,y33=y3) * z_linear(zi)(y11=y1,y22=y2,y33=y3)
                    for y3 in [0,1]])
                for y2 in [0,1]])
            for y1 in [0,1]])

The CCS relation we want to check,

$1\cdot (M_1\cdot z\circ M_2\cdot z)+(-1)\cdot (M_3\cdot z)=\vec{0}1\; \backslash cdot\; (M\_1\; \backslash cdot\; z\; \backslash circ\; M\_2\; \backslash cdot\; z)\; +\; (-1)\; \backslash cdot\; (M\_3\; \backslash cdot\; z)\; =\; \backslash vec\{0\}$

is thus turned into a polynomial equation

G = Mi_z_prod(M1, z1) * Mi_z_prod(M2, z1) - Mi_z_prod(M3, z1)
G

21*x11^2*x22^2 - 17*x11^2*x22 - 15*x11*x22^2 + 2*x11^2 + 11*x11*x22 - 2*x11

The prover wants to prove that $G((x_1,x_2))=0G((x\_1,\; x\_2))\; =\; 0$ for all $x_1,x_2\in \{0,1\}x\_1,\; x\_2\; \backslash in\; \backslash \{0,1\backslash \}$ using the sum-check.

That is $G((0,0))=G((0,1))=G((1,0))=G((1,1))=0G((0,0))=\; G((0,1))=\; G((1,0))=\; G((1,1))=0$.

As expected, we extend the multivariate polynomial $G:\{0,1\}\times \{0,1\}\to \mathbb{F}G\; :\; \backslash \{0,1\backslash \}\; \backslash times\; \backslash \{0,1\backslash \}\; \backslash to\; \backslash mathbb\{F\}$ of degree $22$ into a multilinear polynomial

As we did earlier, now $h(X)h(X)$ is a multilinear extension that encodes the $44$ evaluations ($\{(0,0),(0,1),(1,0),(1,1)\}\backslash \{(0,0),\; (0,1),\; (1,0),\; (1,1)\; \backslash \}$) of $GG$ into its coefficients, so it is uniquely determined by $44$ evaluations (i.e. a polynomial of $nn$ coefficients is of degree $n-1n\; -\; 1$, thus uniquely defined by $nn$ evaluations).

Since $\mathrm{\forall }{x}_1,x_2\in \{0,1\}\mathrm{.}h((x_1,x_2))=G((x_1,x_2))=0\backslash forall\; x\_1,\; x\_2\; \backslash in\; \backslash \{0,1\backslash \}.\; h((x\_1,\; x\_2))\; =\; G((x\_1,\; x\_2))\; =\; 0$, then $hh$ must necessarily be the zero polynomial $h=0h\; =\; 0$.

h = sum([
        sum([
            G(x11=x11, x22=x22) * eqx(x11=x11, x22=x22)
            for x22 in [0,1]])
     for x11 in [0,1]])

h

0

Note that there would be no harm in doing such transformation if $GG$ were already multilinear. If a polynomial $G\in \mathbb{F}[x_1,\mathrm{.}\mathrm{.}\mathrm{.},x_s]G\; \backslash in\; \backslash mathbb\{F\}[x\_1,...,\; x\_s]$ is multilinear, then $G(X)={\sum }_{x\in \{0,1{\}}^s}G(x)\cdot \widetilde{eq}(x,X)G(X)\; =\; \backslash sum\_\{x\backslash in\; \backslash \{0,1\backslash \}^s\}\; G(x)\; \backslash cdot\; \backslash widetilde\{eq\}(x,\; X)$ You can check lemma 6 of HyperNova for a proof.

By the Schwartz-Zippel lemma, we can evaluate

$h((X_1,X_2))={\sum }_{x_1\in \{0,1\}}{\sum }_{x_2\in \{0,1\}}G((x_1,x_2))\cdot \widetilde{eq}((X_1,X_2),(x_1,x_2))=0h((X\_1,\; X\_2))\; =\; \backslash sum\_\{x\_1\; \backslash in\; \backslash \{0,1\backslash \}\}\backslash sum\_\{x\_2\; \backslash in\; \backslash \{0,1\backslash \}\}\; G((x\_1,\; x\_2))\; \backslash cdot\; \backslash widetilde\{eq\}((X\_1,\; X\_2),\; (x\_1,\; x\_2))\; =\; 0$

at a random point $\beta :=({\beta }_1,{\beta }_2)\in {\mathbb{F}}^2\backslash beta\; :=\; (\backslash beta\_1,\; \backslash beta\_2)\; \backslash in\; \backslash mathbb\{F\}^2$ to prove that $hh$ is indeed the zero polynomial.

That is, if

then $h(X_1,X_2)=0h(X\_1,\; X\_2)\; =\; 0$ with high probability.

beta1 = k.random_element()
beta2 = k.random_element()

(beta1, beta2)

(57, 23)

Note that $\widetilde{eq}(({\beta }_1,{\beta }_2),(x_1,x_2))=((1-{\beta }_1)(1-x_1)+{\beta }_1{x}_1)\cdot ((1-{\beta }_2)(1-x_2)+{\beta }_2{x}_2)\backslash widetilde\{eq\}((\backslash beta\_1,\; \backslash beta\_2),\; (x\_1,\; x\_2))\; =\; ((1-\backslash beta\_1)(1-x\_1)\; +\; \backslash beta\_1\; x\_1)\; \backslash cdot\; ((1-\backslash beta\_2)(1-x\_2)\; +\; \backslash beta\_2\; x\_2)$ may not be zero if ${\beta }_1,{\beta }_2\mathrm{\notin }\{0,1\}\backslash beta\_1,\; \backslash beta\_2\; \backslash notin\; \backslash \{0,1\backslash \}$.

Let $Q(X_1,X_2):=G((X_1,X_2))\cdot \widetilde{eq}(({\beta }_1,{\beta }_2),(X_1,X_2))Q(X\_1,\; X\_2)\; :=\; G((X\_1,\; X\_2))\; \backslash cdot\; \backslash widetilde\{eq\}((\backslash beta\_1,\; \backslash beta\_2),\; (X\_1,\; X\_2))$.

Q = G * eqx(x1=beta1,x2=beta2)
Q

28*x11^3*x22^3 + 22*x11^3*x22^2 - 16*x11^2*x22^3 + 13*x11^3*x22 + 34*x11^2*x22^2 + 26*x11*x22^3 - 23*x11^3 + 29*x11^2*x22 - 43*x11*x22^2 - 38*x11^2 + 8*x11*x22 - 40*x11

To help us refer to the different sum-checks conceptually, we give them different names:

• Outer sum-check: $0=G(x)0\; =\; G(x)$ for all $x\in \{0,1{\}}^{2}x\; \backslash in\; \backslash \{0,1\backslash \}^2$.
• Inner sum-check: $T_j={\sum }_{y\in \{0,1{\}}^3}{\tilde{M}}_j(r,y)\cdot \tilde{z}(y)T\_j\; =\; \backslash sum\_\{y\backslash in\; \backslash \{0,1\backslash \}^\{3\}\}\; \backslash widetilde\{M\}\_j(r,y)\; \backslash cdot\; \backslash widetilde\{z\}(y)$

Outer sum-check

The prover engages with the verifier in the following sum-check:

${\sum }_{x_1\in \{0,1\}}{\sum }_{x_2\in \{0,1\}}Q(x_1,x_2)=0\backslash sum\_\{x\_1\; \backslash in\; \backslash \{0,1\backslash \}\}\backslash sum\_\{x\_2\; \backslash in\; \backslash \{0,1\backslash \}\}\; Q(x\_1,\; x\_2)\; =\; 0$

which implies that $G((x_1,x_2))=0G((x\_1,\; x\_2))\; =\; 0$ for all $x_1,x_2\in \{0,1\}x\_1,\; x\_2\; \backslash in\; \backslash \{0,1\backslash \}$.

sum([ 
    sum([ Q(x11=x1, x22=x2) for x2 in [0,1]])
for x1 in [0,1]]) == 0

True

Round 1

The prover $PP$ sends the verifier $VV$ a univariate polynomial $s_1(X_1)s\_1(X\_1)$ claiming to be equal to $Q_1(X_1):={\sum }_{x_2\in \{0,1\}}Q(X_1,x_2)Q\_1(X\_1)\; :=\; \backslash sum\_\{x\_2\; \backslash in\; \backslash \{0,1\backslash \}\}\; Q(X\_1,\; x\_2)$. That is, we keep the first variable unbound while summing up the values over the boolean hypercube.

Q1 = sum([ Q(x22=x2) for x2 in [0,1]])
s1 = Q1

s1

17*x11^3 - 29*x11^2 + 12*x11

The verifier first checks that $s_1(0)+s_1(1)s\_1(0)\; +\; s\_1(1)$ matches the expected result, i.e. $s_1(0)+s_1(1)=0s\_1(0)\; +\; s\_1(1)\; =\; 0$.

s1(x11=0) + s1(x11=1) == 0

True

Then the verifier checks $s_1=Q_{1}s\_1\; =\; Q\_1$ by checking that $Q_{1}Q\_1$ and $s_{1}s\_1$ agree at a random point $r_{1}r\_1$ (Schwartz-Zippel lemma).

r1 = k.random_element()
r1

84

The verifier can compute directly $s_1(r_1)s\_1(r\_1)$ but doesn't know what $Q_{1}Q\_1$ is, so the check $s_1=Q_{1}s\_1\; =\; Q\_1$ must be done recursively.

Round 2

The new claim is that $s_1(r_1):={\sum }_{x_2\in \{0,1\}}Q(r_1,x_2)s\_1(r\_1)\; :=\; \backslash sum\_\{x\_2\; \backslash in\; \backslash \{0,1\backslash \}\}\; Q(r\_1,\; x\_2)$, so $PP$ sends $VV$ a univariate $s_2(X_2)s\_2(X\_2)$ which he claims to be equal to $Q_2(X_2):=Q(r_1,X_2)Q\_2(X\_2)\; :=\; Q(r\_1,\; X\_2)$.

Q2 = Q(x11=r1)
s2 = Q2

s2

-18*x22^3 + 37*x22^2 + 27*x22 - 20

The verifier first checks that $s_1(r_1)s\_1(r\_1)$ is indeed $s_2(0)+s_2(1)s\_2(0)\; +\; s\_2(1)$

s2(x22=0) + s2(x22=1) == s1(x11=r1)

True

Then the verifier sends a random challenge $r_{2}r\_2$ to check that $s_2(r_2)=Q_2(r_2)s\_2(r\_2)\; =\; Q\_2(r\_2)$.

r2 = k.random_element()
r2

31

There is no more need for recursion, since the verifier can now evaluate

However, the verifier doesn't want to compute the inner sums

${\sum }_{y\in \{0,1{\}}^3}\widetilde{M_i}((r_1,r_2),y)\cdot \tilde{z}(y)\backslash sum\_\{y\; \backslash in\; \backslash \{0,\; 1\; \backslash \}^3\}\; \backslash widetilde\{M\_i\}((r\_1,\; r\_2),\; y)\; \backslash cdot\; \backslash widetilde\{z\}(y)$

for $i\in \{1,2,3\}i\; \backslash in\; \backslash \{1,2,3\backslash \}$ by himself, so he engages in further sum-checks with the prover.

Batching inner sum-checks

The prover is asked to compute the inner sum-checks

and to send $T_{i}T\_i$ to the verifier for $i\in \{1,2,3\}i\; \backslash in\; \backslash \{1,2,3\backslash \}$ to sum-check it.

def Ti_generator(Mi, zi):
    return sum([
        sum([
            sum([
                Mi_linear(Mi)(x11=r1, x22= r2, y11=y1,y22=y2,y33=y3) * z_linear(zi)(y11=y1,y22=y2,y33=y3)
            for y3 in [0,1]])
        for y2 in [0,1]])
    for y1 in [0,1]])

T1 = Ti_generator(M1, z1)
T2 = Ti_generator(M2, z1)
T3 = Ti_generator(M3, z1)
T1, T2, T3

(33, -10, 10)

However, instead of engaging in separate sum-checks $T_i={\sum }_{y\in \{0,1{\}}^3}\widetilde{M_i}((r_1,r_2),y)\cdot \tilde{z}(y)T\_i\; =\; \backslash sum\_\{y\; \backslash in\; \backslash \{0,\; 1\; \backslash \}^3\}\; \backslash widetilde\{M\_i\}((r\_1,\; r\_2),\; y)\; \backslash cdot\; \backslash widetilde\{z\}(y)$ for each $i\in \{1,2,3\}i\; \backslash in\; \backslash \{1,2,3\backslash \}$, the prover will batch them using a random element $\alpha \backslash alpha$ generated by the verifier.

Which proves with high probability that all $T_1,T_2,T_{3}T\_1,\; T\_2,\; T\_3$ are correctly computed from ${\sum }_{y\in \{0,1{\}}^3}\widetilde{M_i}((r_1,r_2),y)\cdot \tilde{z}(y)\backslash sum\_\{y\; \backslash in\; \backslash \{0,\; 1\; \backslash \}^3\}\; \backslash widetilde\{M\_i\}((r\_1,\; r\_2),\; y)\; \backslash cdot\; \backslash widetilde\{z\}(y)$.

alpha = k.random_element()
alpha

78

T = T1 + alpha * T2 + alpha^2 * T3
T

-2

Round 1

The prover $PP$ sends the verifier $VV$ a univariate polynomial $q_1(Y_1)q\_1(Y\_1)$ to be equal to

That is, we keep the first variable unbound while summing up the values over the boolean hypercube.

f1 = sum([
        sum([
            Mi_linear(M1)(x11=r1, x22= r2, y22=y2,y33=y3) * z_linear(z1)(y22=y2,y33=y3) + 
            alpha * Mi_linear(M2)(x11=r1, x22= r2, y22=y2,y33=y3) * z_linear(z1)(y22=y2,y33=y3) +
            alpha^2 * Mi_linear(M3)(x11=r1, x22= r2, y22=y2,y33=y3) * z_linear(z1)(y22=y2,y33=y3)
        for y3 in [0,1]])
    for y2 in [0,1]])
q1 = f1

q1

-2*y11^2 + 16*y11 - 8

The verifier first checks that $q_1(0)+q_1(1)q\_1(0)\; +\; q\_1(1)$ matches the expected result, i.e. $q_1(0)+q_1(1)=Tq\_1(0)\; +\; q\_1(1)\; =\; T$.

q1(y11=0) + q1(y11=1) == T

True

Then the verifier checks $q_1=f_{1}q\_1\; =\; f\_1$ by checking that $f_{1}f\_1$ and $q_{1}q\_1$ agree at a random point $r_1^{\mathrm{\prime }}r\text{'}\_1$ (Schwartz-Zippel lemma).

r11 = k.random_element()
r11

23

The verifier can compute directly $q_1(r_1^{\mathrm{\prime }})q\_1(r\text{'}\_1)$ but doesn't know what $f_{1}f\_1$ is, so the check $q_1=f_{1}q\_1\; =\; f\_1$ must be done recursively.

Round 2

The new claim is that

so $PP$ sends $VV$ a univariate $q_2(Y_2)q\_2(Y\_2)$ claimed to be equal to

f2 = sum([
        Mi_linear(M1)(x11=r1, x22= r2, y11=r11, y33=y3) * z_linear(z1)(y11=r11,y33=y3) + 
        alpha * Mi_linear(M2)(x11=r1, x22= r2, y11=r11,y33=y3) * z_linear(z1)(y11=r11,y33=y3) +
        alpha^2 * Mi_linear(M3)(x11=r1, x22= r2, y11=r11,y33=y3) * z_linear(z1)(y11=r11,y33=y3)
    for y3 in [0,1]])
q2 = f2

q2

27*y22^2 + 9*y22 + 37

The verifier first checks that $q_1(r_1^{\mathrm{\prime }})q\_1(r\text{'}\_1)$ is indeed $q_2(0)+q_2(1)q\_2(0)\; +\; q\_2(1)$

q2(y22=0) + q2(y22=1) == q1(y11=r11)

True

Then sends a random challenge $r_2^{\mathrm{\prime }}r\text{'}\_2$ to check that $q_2(r_2^{\mathrm{\prime }})=f_2(r_2^{\mathrm{\prime }})q\_2(r\text{'}\_2)\; =\; f\_2(r\text{'}\_2)$.

r22 = k.random_element()
r22

96

Round 3

Finally, the prover claims that

so $PP$ sends $VV$ a univariate $q_3(Y_2)q\_3(Y\_2)$ claimed to be equal to

f3 = Mi_linear(M1)(x11=r1, x22= r2, y11=r11, y22=r22) * z_linear(z1)(y11=r11,y22=r22) + alpha * Mi_linear(M2)(x11=r1, x22= r2, y11=r11,y22=r22) * z_linear(z1)(y11=r11,y22=r22) + alpha^2 * Mi_linear(M3)(x11=r1, x22= r2, y11=r11,y22=r22) * z_linear(z1)(y11=r11,y22=r22)

q3 = f3

q3

-45*y33^2 - 33*y33 + 19

The verifier first checks that $q_2(r_2^{\mathrm{\prime }})q\_2(r\text{'}\_2)$ is indeed $q_3(0)+q_3(1)q\_3(0)\; +\; q\_3(1)$

q3(y33=0) + q3(y33=1) == q2(y22=r22)

True

Then, using a random value $r_3^{\mathrm{\prime }}r\text{'}\_3$, he can compute on his own $f_3(r_3^{\mathrm{\prime }})f\_3(r\text{'}\_3)$ and check that $q_3(r_3^{\mathrm{\prime }})q\_3(r\text{'}\_3)$ is indeed equal to $f_3(r_3^{\mathrm{\prime }})f\_3(r\text{'}\_3)$, thus $q_3=f_{3}q\_3\; =\; f\_3$.

r33 = k.random_element()
r33

84

That is, that $f_3(r_3^{\mathrm{\prime }})=\widetilde{M_i}((r_1,r_2),(r_1^{\mathrm{\prime }},r_2^{\mathrm{\prime }},r_3^{\mathrm{\prime }}))\cdot \tilde{z}((r_1^{\mathrm{\prime }},r_2^{\mathrm{\prime }},r_3^{\mathrm{\prime }}))f\_3(r\text{'}\_3)\; =\; \backslash widetilde\{M\_i\}((r\_1,\; r\_2),\; (r\text{'}\_1,\; r\text{'}\_2,\; r\text{'}\_3))\; \backslash cdot\; \backslash widetilde\{z\}((r\text{'}\_1,\; r\text{'}\_2,\; r\text{'}\_3))$, which the verifier can easily compute.

c1 = Mi_linear(M1)(x11=r1, x22= r2, y11=r11, y22=r22,y33=r33) * z_linear(z1)(y11=r11,y22=r22,y33=r33) + alpha * Mi_linear(M2)(x11=r1, x22= r2, y11=r11,y22=r22,y33=r33) * z_linear(z1)(y11=r11,y22=r22,y33=r33) + alpha^2 * Mi_linear(M3)(x11=r1, x22= r2, y11=r11,y22=r22,y33=r33) * z_linear(z1)(y11=r11,y22=r22,y33=r33)

c1 == q3(y33=r33)

True

Thus, the verifier has checked that

so he can trust that all $T_1,T_2,T_{3}T\_1,\; T\_2,\; T\_3$ derive from ${\sum }_{y\in \{0,1{\}}^3}\widetilde{M_i}((r_1,r_2),y)\cdot \tilde{z}(y)\backslash sum\_\{y\; \backslash in\; \backslash \{0,\; 1\; \backslash \}^3\}\; \backslash widetilde\{M\_i\}((r\_1,\; r\_2),\; y)\; \backslash cdot\; \backslash widetilde\{z\}(y)$, and use them in the remaining step of the outer sum-check.

Final check

We were left in the outer sum-check with the verifier wanting to compute

However, he needed help from the prover to compute

$T_i:={\sum }_{y\in \{0,1{\}}^3}\widetilde{M_i}((r_1,r_2),y)\cdot \tilde{z}(y)T\_i\; :=\; \backslash sum\_\{y\; \backslash in\; \backslash \{0,\; 1\; \backslash \}^3\}\; \backslash widetilde\{M\_i\}((r\_1,\; r\_2),\; y)\; \backslash cdot\; \backslash widetilde\{z\}(y)$

After batching the inner sum-checks into a single grand inner sum-check, the verifier has now proof of $T_1,T_{2}T\_1,\; T\_2$ and $T_{3}T\_3$, so can easily compute

Q(x11=r1, x22=r2) == (T1 * T2 - T3) * eqx(x11=r1, x22=r2, x1=beta1, x2=beta2)

True

Which proves the original claim that the CCS relation for the Fibonacci example $1\cdot (M_1\cdot z\circ M_2\cdot z)+(-1)\cdot (M_3\cdot z)=\vec{0}1\; \backslash cdot\; (M\_1\; \backslash cdot\; z\; \backslash circ\; M\_2\; \backslash cdot\; z)\; +\; (-1)\; \backslash cdot\; (M\_3\; \backslash cdot\; z)\; =\; \backslash vec\{0\}$ holds.

That is,

There are two ways in which a verifier may evaluate these multi-linear extension of CCS matrices:

1. if matrices are structured the verifier evaluates them in logarithmic time
2. if matrices are unstructured, the prover can prove evaluations of MLE of sparse matrices in linear time using memory checking techniques (see Spark compiler in the Spartan paper).

Conclusion

We made it! To recap, we have shown in this article how:

1. Any polynomial equation can be transformed into a (bunch of) sum-checks, by leveraging the properties of multilinear polynomials and the Schwartz-Zippel lemma.

2. A CCS relation can be transformed into a sum of a multilinear polynomial over the boolean hypercube and proved using the sum-check protocol.

During the outer sum-check ${\sum }_{x_1\in \{0,1\}}{\sum }_{x_2\in \{0,1\}}Q(x_1,x_2)=0\backslash sum\_\{x\_1\; \backslash in\; \backslash \{0,1\backslash \}\}\backslash sum\_\{x\_2\; \backslash in\; \backslash \{0,1\backslash \}\}\; Q(x\_1,\; x\_2)\; =\; 0$ the verifier was eventually be confronted to compute $Q(r)Q(r)$ for some $r\in {\mathbb{F}}^{2}r\; \backslash in\; \backslash mathbb\{F\}^\{2\}$.

Since $Q(r)=G(r)\cdot \widetilde{eq}(({\beta }_1,{\beta }_2),r)Q(r)\; =\; G(r)\; \backslash cdot\; \backslash widetilde\{eq\}((\backslash beta\_1,\; \backslash beta\_2),\; r)$ the verifier had to compute ${\sum }_{y\in \{0,1{\}}^3}{\tilde{M}}_j(r,y)\cdot \tilde{z}(y)\backslash sum\_\{y\backslash in\; \backslash \{0,1\backslash \}^\{3\}\}\; \backslash widetilde\{M\}\_j(r,y)\; \backslash cdot\; \backslash widetilde\{z\}(y)$ for $j\in \{1,2,3\}j\; \backslash in\; \backslash \{1,2,3\backslash \}$. Thus he asked for help to the prover, and engaged in a batched inner sum-check.

The main idea of HyperNova will be to fold or delay the computation of any inner sum-check. This will be explored in the next article.

Thanks for reading!