I'd like to thank Nicolas Mohnblatt for brainstorming, discussing and reviewing this article, and for his many shared insights, and to Srinath Setty for providing the inspiration for this work and 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.

Folding CCS relations in HyperNova

In part 1, we managed to verify the validity of a CCS relation using the sum-check. The goal was to get ourselves familiar with the mechanics of the protocol. In particular, we saw that two sum-checks are run for such a CCS relation, and how the two sum-checks relate.

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

The goal of this post is to go beyond a single CCS instance to a folding of many as is done in the HyperNova paper. One of the main insights of folding in HyperNova is that we can accumulate or delay the computation of the inner sum-checks.

Linearised Committed CCS (LCCCS)

Recall that 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 that $(s,\times ,\omega )\in {\mathcal{R}}_{CCS}(s,\; \backslash times,\; \backslash omega)\; \backslash in\; \backslash mathcal\{R\}\_\{CCS\}$ if and only if for all $x\in \{0,1{\}}^{\log m}x\; \backslash in\; \backslash \{0,1\backslash \}^\{\backslash log\; m\}$

where $\tilde{z}(y)=\widetilde{(\omega ,\times ,1)}(y)\backslash widetilde\{z\}(y)=\backslash widetilde\{(\backslash omega,\; \backslash times,\; 1)\}(y)$

In HyperNova, CCS relations are modified for folding:

• A Linearised CCS relation ${\mathcal{R}}_{LCCS}\backslash mathcal\{R\}\_\{LCCS\}$ contains only inner linear sum-checks. Concretely,

$\begin{array}{c}{\displaystyle (s,(u,x,r,\{v_1,\mathrm{.}\mathrm{.}\mathrm{.},v_t\}),\tilde{w})\in {\mathcal{R}}_{LCCS}⟺v_i=\sum _{y\in \{0,1\}}\widetilde{M_i}(r,y)\cdot \tilde{z}(y)}\end{array}\backslash begin\{aligned\}\; (s,\; (u,\; x,\; r,\; \backslash \{v\_1,...,v\_t\backslash \}),\; \backslash widetilde\{w\})\; \backslash in\; \backslash mathcal\{R\}\_\{LCCS\}\; \backslash iff\; v\_i\; =\; \backslash sum\_\{y\; \backslash in\; \backslash \{\; 0,1\backslash \}\}\; \backslash widetilde\{M\_i\}(r,\; y)\; \backslash cdot\; \backslash widetilde\{z\}(y)\; \backslash end\{aligned\}$.

One can think of an LCCS instance as an object that encapsulates the inner sum-checks that are left after computing the outer sum-check of a CCS instance.

• A Committed CCS relation $(C,s,\times ,\omega )\in {\mathcal{R}}_{CCCS}(C,\; s,\; \backslash times,\; \backslash omega)\; \backslash in\; \backslash mathcal\{R\}\_\{CCCS\}$ is a CCS instance where a commitment to the witness $\omega \backslash omega$ is also presented in the instance.
• A Linearised Committed CCS instance $(C,s,(u,x,r,\{v_1,\mathrm{.}\mathrm{.}\mathrm{.},v_t\}),\tilde{w})\in {\mathcal{R}}_{LCCCS}(C,\; s,\; (u,\; x,\; r,\; \backslash \{v\_1,...,v\_t\backslash \}),\; \backslash widetilde\{w\})\; \backslash in\; \backslash mathcal\{R\}\_\{LCCCS\}$ is a linearised instance with a commitment to the witness $\omega \backslash omega$ of the instance.

Multi-folding for CCS construction

Folding in HyperNova takes an accumulated relation $R_1\in {\mathcal{R}}_{LCCCS}R\_1\; \backslash in\; \backslash mathcal\{R\}\_\{LCCCS\}$ and a new, incoming relation $R_2\in {\mathcal{R}}_{CCCS}R\_2\; \backslash in\; \backslash mathcal\{R\}\_\{CCCS\}$, and returns a new accumulated relation $R_3\in {\mathcal{R}}_{LCCCS}R\_3\; \backslash in\; \backslash mathcal\{R\}\_\{LCCCS\}$.

More precisely, a folding step will require us to prove the sums in:

• $R_1\in {\mathcal{R}}_{LCCCS}R\_1\; \backslash in\; \backslash mathcal\{R\}\_\{LCCCS\}$: $v_i={\sum }_{y\in \{0,1\}}\widetilde{M_i}(r,y)\cdot \tilde{z}(y)v\_i\; =\; \backslash sum\_\{y\; \backslash in\; \backslash \{\; 0,1\backslash \}\}\; \backslash widetilde\{M\_i\}(r,\; y)\; \backslash cdot\; \backslash widetilde\{z\}(y)$
• $R_2\in {\mathcal{R}}_{CCCS}R\_2\; \backslash in\; \backslash mathcal\{R\}\_\{CCCS\}$: ${\sum }_{i=1}^q{c}_i\cdot ({\prod }_{j\in S_i}({\sum }_{y\in \{0,1{\}}^{\log m}}{\tilde{M}}_j(x,y)\cdot \tilde{z}(y)))=0\backslash sum\_\{i=1\}^q\; c\_i\; \backslash cdot\; (\backslash prod\_\{j\backslash in\; S\_i\}\; (\backslash sum\_\{y\backslash in\; \backslash \{0,1\backslash \}^\{\backslash log\; m\}\}\; \backslash widetilde\{M\}\_j(x,y)\; \backslash cdot\; \backslash widetilde\{z\}(y)))\; =\; 0$

while delaying some of the sum-checks for later steps, which are encoded in $R_3\in {\mathcal{R}}_{LCCCS}R\_3\; \backslash in\; \backslash mathcal\{R\}\_\{LCCCS\}$.

Folding Fibonacci

To illustrate the workings of folding in HyperNova, we'll perform two iterations of our Fibonacci example:

// i-th iteration
fibonacci(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)
}

Recall that a Fibonacci iteration arithmetises in CCS as follows:

Multi-folding refers to the property that instances of different structures can be folded together. However, the structure $s_{i}s\_i$ for each instance in our fibonacci example will be the same. That is, $s=s_1=s_2=([{\tilde{M}}_1,{\tilde{M}}_2,{\tilde{M}}_3],[S_1,S_2],[c_1,c_2])s\; =\; s\_1\; =\; s\_2\; =\; ([\backslash widetilde\{M\}\_1,\; \backslash widetilde\{M\}\_2,\; \backslash widetilde\{M\}\_3],\; [S\_1,\; S\_2],\; [c\_1,\; c\_2])$, where $S_1=\{1,2\}S\_1\; =\; \backslash \{1,\; 2\backslash \}$, $S_2=\{3\}S\_2\; =\; \backslash \{\; 3\; \backslash \}$, $c_1=1c\_1\; =\; 1$, $c_2=-1c\_2\; =\; -1$.

# Necessary boilerplate from our last post
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)

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]
])

Recall also that 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)$.

And that to apply the sum-check, the CCS relation

$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

# 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]])

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]])

Iteration 1 (base case)

As we did in our previous post, we provide 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$ to the Fibonacci step function, which outputs $x=1,y=6,t=6x\; =\; 1,\; y=6,\; t=6$.

The ingredients for our first iterations are:

• Accumulated relation $R_1=\mathrm{\perp }\in {\mathcal{R}}_{LCCCS}R\_1\; =\; \backslash bot\; \backslash in\; \backslash mathcal\{R\}\_\{LCCCS\}$
• Incoming relation $R_2=(s,C_2,{\times }_2)\in {\mathcal{R}}_{CCCS}R\_2\; =\; (s,\; C\_2,\; \backslash times\_2)\; \backslash in\; \backslash mathcal\{R\}\_\{CCCS\}$
• Accumulated instance ${\tilde{z}}_1=\mathrm{\perp }\backslash widetilde\{z\}\_1\; =\; \backslash bot$
• Incoming instance ${\tilde{z}}_2=\widetilde{({\omega }_2,{\times }_2,1)}\backslash widetilde\{z\}\_2\; =\; \backslash widetilde\{(\backslash omega\_2,\; \backslash times\_2,\; 1)\}$, where ${\omega }_2=()\backslash omega\_2\; =\; ()$ and ${\times }_2=(0,1,1,2,3,6,6)\backslash times\_2\; =\; (0,1,1,2,3,6,6)$.

public_x2 = [0,1,1,2,3,6,6]
private_w2 = []
z2 = vector(k, private_w2 + public_x2 + [1])
z2

(0, 1, 1, 2, 3, 6, 6, 1)

Checking $R_1\in {\mathcal{R}}_{LCCCS}R\_1\; \backslash in\; \backslash mathcal\{R\}\_\{LCCCS\}$

In this first iteration or base case, our accumulated instance $R_{1}R\_1$ is empty, so there is no sum-check to run.

Checking for $R_2\in {\mathcal{R}}_{CCCS}R\_2\; \backslash in\; \backslash mathcal\{R\}\_\{CCCS\}$

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$, where

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

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

As we did in the previous post, we compute the multilinear extension of $G((X_1,X_2))G((X\_1,X\_2))$, $h((X_1,X_2))={\sum }_{x_1,x_2\in \{0,1\}}\widetilde{eq}((X_1,X_2),(x_1,x_2))\cdot G((x_1,x_2))h((X\_1,X\_2))\; =\; \backslash sum\_\{x\_1,x\_2\; \backslash in\; \backslash \{0,1\backslash \}\}\; \backslash widetilde\{eq\}((X\_1,X\_2),(x\_1,x\_2))\; \backslash cdot\; G((x\_1,\; x\_2))$.

Checking that $hh$ is the zero polynomial implies with high probability that for all $x\in \{0,1{\}}^{2}x\; \backslash in\; \backslash \{\; 0,1\backslash \}^2$, $G(x)=0G(x)\; =\; 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

To check that $h=0h\; =\; 0$, we can apply the Swartz-Zippel lemma and evaluate $hh$ at a random point $\beta :=({\beta }_1,{\beta }_2)\backslash beta\; :=\; (\backslash beta\_1,\; \backslash beta\_2)$.

Thus, the verifier samples a random challenge $\beta :=({\beta }_1,{\beta }_2)\backslash beta\; :=\; (\backslash beta\_1,\; \backslash beta\_2)$.

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

(beta1, beta2)

(91, 30)

The prover computes $h(({\beta }_1,{\beta }_2))h((\backslash beta\_1,\backslash beta\_2))$ and sends it to the verifier. The goal of the verifier is to check that $h(({\beta }_1,{\beta }_2))h((\backslash beta\_1,\backslash beta\_2))$ is indeed this sum:

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

Equivalently, it is checking that ${\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$ where

$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

39*x11^3*x22^3 + 17*x11^3*x22^2 - 5*x11^2*x22^3 - 4*x11^3*x22 + 5*x11^2*x22^2 - 39*x11*x22^3 + 6*x11^3 + 41*x11^2*x22 + 6*x11*x22^2 - 38*x11^2 + 41*x11*x22 + 32*x11

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

-37*x11^3 - 35*x11^2 - 29*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

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

95

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 (final)

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)$

The prover sends the verifier 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

13*x22^3 + 7*x22^2 - 27*x22 - 28

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

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

70

There is no more need for recursion, since the verifier may now evaluate $Q(r_1,r_2)=Q_2(r_2)Q(r\_1,\; r\_2)\; =\; Q\_2(r\_2)$.

However, to compute $Q_2(r_2)Q\_2(r\_2)$ the verifier must know the value of the sums

To assist the verifier in this computation, the prover computes $v_i={\sum }_{y\in \{0,1{\}}^3}\widetilde{M_i}((r_1,r_2),y)\cdot {\tilde{z}}_2(y)v\_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\}\_2(y)$ and sends them to the verifier.

def v_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]])

v1 = v_generator(M1, z2)
v2 = v_generator(M2, z2)
v3 = v_generator(M3, z2)

(v1,v2,v3)

(37, -48, -8)

Accumulating sum-checks into $R_3\in {\mathcal{R}}_{LCCCS}R\_3\; \backslash in\; \backslash mathcal\{R\}\_\{LCCCS\}$

Instead of engaging in a sum-check now, they construct $R_3\in {\mathcal{R}}_{LCCCS}R\_3\; \backslash in\; \backslash mathcal\{R\}\_\{LCCCS\}$, which serves as an accumulation of these inner sum-checks:

$R_3=(s,C_3,(u_3,{\times }_3,(r_1,r_2),\{v_1,v_2,v_3\}))R\_3\; =\; (s,\; C\_3,\; (u\_3,\; \backslash times\_3,\; (r\_1,\; r\_2),\; \backslash \{v\_1,v\_2,v\_3\backslash \}))$

where $C_3=C_{2}C\_3\; =\; C\_2$, $u_3=1u\_3\; =\; 1$, ${\times }_3={\times }_2\backslash times\_3\; =\; \backslash times\_2$.

So, by checking $R_{3}R\_3$ in a future step, the verifier will verify that $v_1,v_2,v_{3}v\_1,\; v\_2,\; v\_3$ were computed correctly, thus avoiding running any inner sum-check at this step. Folding for the win!

u3 = 1
public_x3 = public_x2

Iteration 2 (iterative case)

• Accumulated relation $R_1^{\mathrm{\prime }}=R_3=(s,C_3,(u_3,{\times }_3,(r_1,r_2),\{v_1,v_2,v_3\}))\in {\mathcal{R}}_{LCCCS}R\text{'}\_1\; =\; R\_3\; =\; (s,\; C\_3,\; (u\_3,\; \backslash times\_3,\; (r\_1,\; r\_2),\; \backslash \{v\_1,v\_2,v\_3\backslash \}))\; \backslash in\; \backslash mathcal\{R\}\_\{LCCCS\}$
• Incoming relation $R_2^{\mathrm{\prime }}=(s,C_2^{\mathrm{\prime }},{\times }_2^{\mathrm{\prime }})\in {\mathcal{R}}_{CCCS}R\text{'}\_2\; =\; (s,\; C\text{'}\_2,\; \backslash times\text{'}\_2)\; \backslash in\; \backslash mathcal\{R\}\_\{CCCS\}$
• Accumulated instance ${\tilde{z}}_1^{\mathrm{\prime }}=\widetilde{({\omega }_3,{\times }_3,u_3)}\backslash widetilde\{z\}\text{'}\_1\; =\; \backslash widetilde\{(\backslash omega\_3,\; \backslash times\_3,\; u\_3)\}$
• Incoming instance ${\tilde{z}}_2^{\mathrm{\prime }}=\widetilde{({\omega }_2^{\mathrm{\prime }},{\times }_2^{\mathrm{\prime }},1)}\backslash widetilde\{z\}\text{'}\_2\; =\; \backslash widetilde\{(\backslash omega\text{'}\_2,\; \backslash times\text{'}\_2,\; 1)\}$ where ${\omega }_2^{\mathrm{\prime }}=()\backslash omega\text{'}\_2\; =\; ()$ and ${\times }_2^{\mathrm{\prime }}=(1,1,2,3,6,18,36)\backslash times\text{'}\_2\; =\; (1,1,2,3,6,18,36)$.

public_xx1 = public_x3
zz1 = vector(k, public_xx1 + [] + [1])
zz1

(0, 1, 1, 2, 3, 6, 6, 1)

public_xx2 = [1,1,2,3,6,18,36]
zz2 = vector(k, public_xx2 + [] + [1])
zz2

(1, 1, 2, 3, 6, 18, 36, 1)

Checking $R_1^{\mathrm{\prime }}\in {\mathcal{R}}_{LCCCS}R\text{'}\_1\; \backslash in\; \backslash mathcal\{R\}\_\{LCCCS\}$

The verifier wants to check that $v_i=H_i^{\mathrm{\prime }}((r_1,r_2))v\_i\; =\; H\text{'}\_i((r\_1,\; r\_2))$, where $H_i^{\mathrm{\prime }}(x)={\sum }_{y\in \{0,1{\}}^3}\widetilde{M_i}(x,y)\cdot {\tilde{z}}_1^{\mathrm{\prime }}(y)H\text{'}\_i(x)\; =\; \backslash sum\_\{y\; \backslash in\; \backslash \{0,\; 1\; \backslash \}^3\}\; \backslash widetilde\{M\_i\}(x,\; y)\; \backslash cdot\; \backslash widetilde\{z\}\text{'}\_1(y)$, as the prover claims.

By lemma 6 of the HyperNova paper, since $H_{i}H\_i$ is a multilinear polynomial in two variables,

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

So the prover is tasked to convince the verifier that

$v_i=H_i((r_1,r_2))={\sum }_{x_1\in \{0,1\}}{\sum }_{x_2\in \{0,1\}}{L}_i((x_1,x_2))v\_i\; =\; H\_i((r\_1,\; r\_2))\; =\; \backslash sum\_\{x\_1\; \backslash in\; \backslash \{0,\; 1\; \backslash \}\}\; \backslash sum\_\{x\_2\; \backslash in\; \backslash \{0,\; 1\; \backslash \}\}\; L\_i((x\_1,\; x\_2))$

where $L_i((X_1,X_2))=\widetilde{eq}((r_1,r_2),(X_1,X_2))\cdot H_i((X_1,X_2))L\_i((X\_1,\; X\_2))\; =\; \backslash widetilde\{eq\}((r\_1,\; r\_2),\; (X\_1,\; X\_2))\; \backslash cdot\; H\_i((X\_1,\; X\_2))$

def H_generator(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]])

H1 = H_generator(M1, zz1)
H2 = H_generator(M2, zz1)
H3 = H_generator(M3, zz1)

(H1, H2, H3)

(-3*x11*x22 + 2*x11 + 1,
 -7*x11*x22 + x11 + 5*x22 + 1,
 -11*x11*x22 + 5*x11 + 5*x22 + 1)

L1 = eqx(x1 = r1, x2= r2) * H1
L2 = eqx(x1 = r1, x2= r2) * H2
L3 = eqx(x1 = r1, x2= r2) * H3

(L1, L2, L3)

(-33*x11^2*x22^2 - 43*x11^2*x22 + 10*x11*x22^2 - 24*x11^2 - 28*x11*x22 + 32*x11 - 37*x22 + 22,
 24*x11^2*x22^2 - 6*x11^2*x22 + 11*x11*x22^2 - 12*x11^2 - 38*x11*x22 + 17*x22^2 + 10*x11 - 28*x22 + 22,
 -20*x11^2*x22^2 - 15*x11^2*x22 - 43*x11*x22^2 + 41*x11^2 + 29*x11*x22 + 17*x22^2 - 3*x11 - 28*x22 + 22)

# Sanity check
H1(x11= r1, x22=r2) == sum([ sum([ L1(x11=x1, x22=x2) for x2 in [0,1]])for x1 in [0,1]])

True

Batching sum-checks in $R_1^{\mathrm{\prime }}\in {\mathcal{R}}_{LCCCS}R\text{'}\_1\; \backslash in\; \backslash mathcal\{R\}\_\{LCCCS\}$

Instead of engaging in three separate sum-checks, the verifier samples a random element $\gamma \in \mathbb{F}\backslash gamma\; \backslash in\; \backslash mathbb\{F\}$, and the three sums ${\sum }_{x_1\in \{0,1\}}{\sum }_{x_2\in \{0,1\}}{L}_i((x_1,x_2))\backslash sum\_\{x\_1\; \backslash in\; \backslash \{0,\; 1\; \backslash \}\}\; \backslash sum\_\{x\_2\; \backslash in\; \backslash \{0,\; 1\; \backslash \}\}\; L\_i((x\_1,\; x\_2))$ for $i\in \{1,2,3\}i\; \backslash in\; \backslash \{1,2,3\backslash \}$ are simultaneously checked together by using a random linear combination of $L_{i}L\_i$, $g_1(x)={\sum }_{j\in \{1,2,3\}}{\gamma }^j\cdot L_j(x)g\_1(x)\; =\; \backslash sum\_\{j\; \backslash in\; \backslash \{1,2,3\backslash \}\}\; \backslash gamma^j\; \backslash cdot\; L\_j(x)$

Checking that

${\sum }_{j\in \{1,2,3\}}{\gamma }^j\cdot v_j={\sum }_{x_1\in \{0,1\}}{\sum }_{x_2\in \{0,1\}}{g}_1((x_1,x_2))\backslash sum\_\{j\; \backslash in\; \backslash \{1,2,3\backslash \}\}\; \backslash gamma^j\; \backslash cdot\; v\_j\; =\; \backslash sum\_\{x\_1\; \backslash in\; \backslash \{0,\; 1\; \backslash \}\}\; \backslash sum\_\{x\_2\; \backslash in\; \backslash \{0,\; 1\; \backslash \}\}\; g\_1((x\_1,\; x\_2))$

implies with high probability that

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

for each $i\in \{1,2,3\}i\; \backslash in\; \backslash \{1,2,3\backslash \}$.

gamma = k.random_element()
gamma

23

g1 = gamma * L1 + gamma^2 * L2 + gamma^3 * L3
g1

-12*x11^2*x22^2 - 20*x11^2*x22 - 12*x11*x22^2 - 24*x11^2 + 9*x11*x22 - 5*x22^2 + 27*x11 - 11*x22 + 48

sum([ 
    sum([ g1(x11=x1, x22=x2) for x2 in [0,1]])
for x1 in [0,1]]) == gamma * v1 + gamma^2 * v2 + gamma^3 * v3

True

The prover thus sends the sum ${\sum }_{j\in \{1,2,3\}}{\gamma }^j\cdot v_j\backslash sum\_\{j\; \backslash in\; \backslash \{1,2,3\backslash \}\}\; \backslash gamma^j\; \backslash cdot\; v\_j$ to the verifier.

Note that the verifier is delaying these checks for now. They will later be further batched with other sum-checks from $R_2^{\mathrm{\prime }}R\text{'}\_2$.

Checking $R_2^{\mathrm{\prime }}\in {\mathcal{R}}_{CCCS}R\text{'}\_2\; \backslash in\; \backslash mathcal\{R\}\_\{CCCS\}$

As we did for $R_{2}R\_2$, the verifier aims to check that $0=G^{\mathrm{\prime }}(X),X\in \{0,1{\}}^{2}0\; =\; G\text{'}(X),\; X\; \backslash in\; \backslash \{\; 0,1\backslash \}^2$, where

${\tilde{z}}_2^{\mathrm{\prime }}=\widetilde{({\omega }_2^{\mathrm{\prime }},{\times }_2^{\mathrm{\prime }},1)}\backslash widetilde\{z\}\text{'}\_2\; =\; \backslash widetilde\{(\backslash omega\text{'}\_2,\; \backslash times\text{'}\_2,\; 1)\}$ where ${\omega }_2^{\mathrm{\prime }}=()\backslash omega\text{'}\_2\; =\; ()$ and ${\times }_2^{\mathrm{\prime }}=(1,1,2,3,6,18,36)\backslash times\text{'}\_2\; =\; (1,1,2,3,6,18,36)$

This is equivalent to checking that ${\sum }_{x_1\in \{0,1\}}{\sum }_{x_2\in \{0,1\}}{Q}^{\mathrm{\prime }}(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\text{'}(x\_1,\; x\_2)\; =\; 0$ where

$Q^{\mathrm{\prime }}(X_1,X_2):=G^{\mathrm{\prime }}((X_1,X_2))\cdot \widetilde{eq}(({\beta }_1^{\mathrm{\prime }},{\beta }_2^{\mathrm{\prime }}),(X_1,X_2))Q\text{'}(X\_1,\; X\_2)\; :=\; G\text{'}((X\_1,\; X\_2))\; \backslash cdot\; \backslash widetilde\{eq\}((\backslash beta\text{'}\_1,\; \backslash beta\text{'}\_2),\; (X\_1,\; X\_2))$, since

${\sum }_{x_1\in \{0,1\}}{\sum }_{x_2\in \{0,1\}}{G}^{\mathrm{\prime }}((x_1,x_2))\cdot \widetilde{eq}((X_1,X_2),(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\text{'}((x\_1,\; x\_2))\; \backslash cdot\; \backslash widetilde\{eq\}((X\_1,\; X\_2),\; (x\_1,\; x\_2))$ is a multilinear polynomial, thus uniquely determined, so it is equal to zero. Thus we apply the Schwartz-Zippel lemma by randomly evaluate it to $({\beta }_1^{\mathrm{\prime }},{\beta }_2^{\mathrm{\prime }})(\backslash beta\text{'}\_1,\; \backslash beta\text{'}\_2)$.

GG = Mi_z_prod(M1, zz2) * Mi_z_prod(M2, zz2) - Mi_z_prod(M3, zz2)
GG

19*x11^2*x22^2 + 9*x11^2*x22 - x11*x22^2 + 8*x11^2 - 27*x11*x22 - 8*x11

The verifier samples a random challenge ${\beta }^{\mathrm{\prime }}:=({\beta }_1^{\mathrm{\prime }},{\beta }_2^{\mathrm{\prime }})\backslash beta\text{'}\; :=\; (\backslash beta\text{'}\_1,\; \backslash beta\text{'}\_2)$.

beta11 = k.random_element()
beta22 = k.random_element()

(beta11, beta22)

(26, 39)

QQ = GG * eqx(x1=beta11,x2=beta22)
QQ

-26*x11^3*x22^3 + 36*x11^3*x22^2 - x11^2*x22^3 + 36*x11^3*x22 - 43*x11^2*x22^2 + 6*x11*x22^3 + 50*x11^3 + 21*x11^2*x22 + 20*x11*x22^2 - 25*x11^2 - 49*x11*x22 - 25*x11

Batching sum-checks in $R_1^{\mathrm{\prime }}\in {\mathcal{R}}_{LCCCS}R\text{'}\_1\; \backslash in\; \backslash mathcal\{R\}\_\{LCCCS\}$ and $R_2^{\mathrm{\prime }}\in {\mathcal{R}}_{CCCS}R\text{'}\_2\; \backslash in\; \backslash mathcal\{R\}\_\{CCCS\}$

We now batch:

• The remaining batched check on $R_1^{\mathrm{\prime }}R\text{'}\_1$, $g_1(x)={\sum }_{j\in \{1,2,3\}}{\gamma }^j\cdot L_j(x)g\_1(x)\; =\; \backslash sum\_\{j\; \backslash in\; \backslash \{1,2,3\backslash \}\}\; \backslash gamma^j\; \backslash cdot\; L\_j(x)$
• The new check $G^{\mathrm{\prime }}(x)=0G\text{'}(x)\; =\; 0$

Using a random linear combination $g(x)=g_1(x)+{\gamma }^4{Q}^{\mathrm{\prime }}(x)g(x)\; =\; g\_1(x)\; +\; \backslash gamma^4\; Q\text{'}(x)$.

As expected, proving the new sum:

${\sum }_{j\in \{1,2,3\}}{\gamma }^j\cdot v_j+{\gamma }^4\cdot 0={\sum }_{x_1\in \{0,1\}}{\sum }_{x_2\in \{0,1\}}g((x_1,x_2))\backslash sum\_\{j\; \backslash in\; \backslash \{1,2,3\backslash \}\}\; \backslash gamma^j\; \backslash cdot\; v\_j\; +\; \backslash gamma^4\; \backslash cdot\; 0\; =\; \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))$

will in turn prove with high probability the batched checks.

g = g1 + gamma^4 * QQ
g

-28*x11^3*x22^3 + 31*x11^3*x22^2 + 30*x11^2*x22^3 + 31*x11^3*x22 - 35*x11^2*x22^2 + 22*x11*x22^3 + 15*x11^3 - 44*x11^2*x22 - 6*x11*x22^2 + 19*x11^2 - 36*x11*x22 - 5*x22^2 - 31*x11 - 11*x22 + 48

$v={\sum }_{j\in \{1,2,3\}}{\gamma }^j\cdot v_j+{\gamma }^4\cdot 0v\; =\; \backslash sum\_\{j\; \backslash in\; \backslash \{1,2,3\backslash \}\}\; \backslash gamma^j\; \backslash cdot\; v\_j\; +\; \backslash gamma^4\; \backslash cdot\; 0$

v = (gamma^1 * v1 + gamma^2 * v2 + gamma^3 * v3) + gamma^4 * 0
v

30

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

True

Round 1

Prover sends $s_1^{\mathrm{\prime }}s\text{'}\_1$ claiming to be $g_1^{\mathrm{\prime }}g\text{'}\_1$

$g_1^{\mathrm{\prime }}(X_1):={\sum }_{x_2\in \{0,1\}}g(X_1,x_2)g\text{'}\_1(X\_1)\; :=\; \backslash sum\_\{x\_2\; \backslash in\; \backslash \{0,1\backslash \}\}\; g(X\_1,\; x\_2)$

gg1 = sum([ g(x22=x2) for x2 in [0,1]])
ss1 = gg1

ss1

-37*x11^3 - 11*x11^2 + 19*x11 - 21

The verifier first checks that $s_1^{\mathrm{\prime }}(0)+s_1^{\mathrm{\prime }}(1)s\text{'}\_1(0)\; +\; s\text{'}\_1(1)$ matches the expected result, i.e. $s_1^{\mathrm{\prime }}(0)+s_1^{\mathrm{\prime }}(1)=vs\text{'}\_1(0)\; +\; s\text{'}\_1(1)\; =\; v$

ss1(x11=0) + ss1(x11=1) == v

True

The verifier checks $s_1^{\mathrm{\prime }}=g_1^{\mathrm{\prime }}s\text{'}\_1\; =\; g\text{'}\_1$ by checking that $g_1^{\mathrm{\prime }}g\text{'}\_1$ and $s_1^{\mathrm{\prime }}s\text{'}\_1$ agree at a random point $r_1^{\mathrm{\prime }}r\text{'}\_1$ (Schwartz-Zippel lemma)

rr1 = k.random_element()
rr1

64

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

Round 2 (final)

The new claim is that $s_1^{\mathrm{\prime }}(r_1^{\mathrm{\prime }}):={\sum }_{x_2\in \{0,1\}}g(r_1^{\mathrm{\prime }},x_2)s\text{'}\_1(r\text{'}\_1)\; :=\; \backslash sum\_\{x\_2\; \backslash in\; \backslash \{0,1\backslash \}\}\; g(r\text{'}\_1,\; x\_2)$

The prover sends the verifier a univariate $s_2^{\mathrm{\prime }}(X_2)s\text{'}\_2(X\_2)$ which he claims to be equal to $g_2^{\mathrm{\prime }}(X_2):=g(r_1^{\mathrm{\prime }},X_2)g\text{'}\_2(X\_2)\; :=\; g(r\text{'}\_1,\; X\_2)$.

gg2 = g(x11=rr1)
ss2 = gg2

ss2

-x22^3 - 22*x22^2 - 28*x22 - 36

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

ss2(x22=0) + ss2(x22=1) == ss1(x11=rr1)

True

The verifier sends a random challenge $r_2^{\mathrm{\prime }}r\text{'}\_2$ to check that $s_2^{\mathrm{\prime }}(r_2^{\mathrm{\prime }})=g_2^{\mathrm{\prime }}(r_2^{\mathrm{\prime }})s\text{'}\_2(r\text{'}\_2)\; =\; g\text{'}\_2(r\text{'}\_2)$.

rr2 = k.random_element()
rr2

67

There is no more need for recursion, since the verifier may now evaluate $g(r_1^{\mathrm{\prime }},r_2^{\mathrm{\prime }})=g_2^{\mathrm{\prime }}(r_2^{\mathrm{\prime }})g(r\text{'}\_1,\; r\text{'}\_2)\; =\; g\text{'}\_2(r\text{'}\_2)$.

However, to compute $g_2^{\mathrm{\prime }}(r_2^{\mathrm{\prime }})g\text{'}\_2(r\text{'}\_2)$ the verifier must know the value of the sums

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

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

for $i\in \{1,2,3\}i\; \backslash in\; \backslash \{1,2,3\backslash \}$, since

To assist the verifier, the prover sends ${\sigma }_i\backslash sigma\_i$ and ${\theta }_i\backslash theta\_i$.

def v_generator(Mi, zi):
    return sum([
        sum([
            sum([
                Mi_linear(Mi)(x11=rr1, x22= rr2, 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]])

sigma1 = v_generator(M1, zz1)
sigma2 = v_generator(M2, zz1)
sigma3 = v_generator(M3, zz1)

theta1 = v_generator(M1, zz2)
theta2 = v_generator(M2, zz2)
theta3 = v_generator(M3, zz2)

(sigma1, sigma2, sigma3), (theta1, theta2, theta3)

((-9, -23, 49), (-18, 45, 3))

g(x11=rr1, x22=rr2) == (gamma * sigma1 + gamma^2 * sigma2 + gamma^3 * sigma3) * eqx(x1=r1, x2=r2, x11=rr1, x22=rr2) + gamma^4 * (theta1 * theta2 - theta3) * eqx(x1=beta11, x2=beta22, x11=rr1, x22=rr2)

True

To avoid doing many sum-checks, the verifier samples a random challenge $\rho \backslash rho$ and reduces the task to checking

${\sigma }_i+\rho \cdot {\theta }_i={\sum }_{y\in \{0,1{\}}^3}\widetilde{M_i}((r_1^{\mathrm{\prime }},r_2^{\mathrm{\prime }}),y)\cdot ({\tilde{z}}_1^{\mathrm{\prime }}(y)+\rho \cdot {\tilde{z}}_2^{\mathrm{\prime }}(y))\backslash sigma\_i\; +\; \backslash rho\; \backslash cdot\; \backslash theta\_i\; =\; \backslash sum\_\{y\; \backslash in\; \backslash \{0,1\backslash \}^3\}\; \backslash widetilde\{M\_i\}((r\text{'}\_1,\; r\text{'}\_2),\; y)\; \backslash cdot\; (\backslash widetilde\{z\}\text{'}\_1(y)\; +\; \backslash rho\; \backslash cdot\; \backslash widetilde\{z\}\text{'}\_2(y))$

rho = k.random_element()
rho

45

Accumulating sum-checks into $R_3^{\mathrm{\prime }}\in {\mathcal{R}}_{LCCCS}R\text{'}\_3\; \backslash in\; \backslash mathcal\{R\}\_\{LCCCS\}$

Instead of engaging in a sum-check now, we construct $R_3^{\mathrm{\prime }}\in {\mathcal{R}}_{LCCCS}R\text{'}\_3\; \backslash in\; \backslash mathcal\{R\}\_\{LCCCS\}$, which serves as an accumulation of all the remaining inner sum-checks:

$R_3^{\mathrm{\prime }}=(s,C_3^{\mathrm{\prime }},(u_3^{\mathrm{\prime }},{\times }_3^{\mathrm{\prime }},(r_1^{\mathrm{\prime }},r_2^{\mathrm{\prime }}),\{v_1^{\mathrm{\prime }},v_2^{\mathrm{\prime }},v_3^{\mathrm{\prime }}\}))R\text{'}\_3\; =\; (s,\; C\text{'}\_3,\; (u\text{'}\_3,\; \backslash times\text{'}\_3,\; (r\text{'}\_1,\; r\text{'}\_2),\; \backslash \{v\text{'}\_1,v\text{'}\_2,v\text{'}\_3\backslash \}))$

where

• $C_3^{\mathrm{\prime }}=C^{\mathrm{\prime }}1+\rho \cdot C_{2}C\text{'}\_3\; =\; C\text{'}1\; +\; \backslash rho\; \backslash cdot\; C\_2$
• $u_3^{\mathrm{\prime }}=1+\rho \cdot 1u\text{'}\_3\; =\; 1\; +\; \backslash rho\; \backslash cdot\; 1$
• ${\times }_3^{\mathrm{\prime }}={\times }_1^{\mathrm{\prime }}+\rho \cdot {\times }^{\mathrm{\prime }}2\backslash times\text{'}\_3\; =\; \backslash times\text{'}\_1\; +\; \backslash rho\; \backslash cdot\; \backslash times\text{'}2$
• $v_i^{\mathrm{\prime }}={\sigma }_i+\rho \cdot {\theta }_{i}v\text{'}\_i\; =\; \backslash sigma\_i\; +\; \backslash rho\; \backslash cdot\; \backslash theta\_i$

Checking the $R_3^{\mathrm{\prime }}R\text{'}\_3$ relation is equivalent to checking

$v_i^{\mathrm{\prime }}={\sum }_{y\in \{0,1{\}}^3}\widetilde{M_i}((r_1^{\mathrm{\prime }},r_2^{\mathrm{\prime }}),y)\cdot ({\tilde{z}}_1^{\mathrm{\prime }}(y)+\rho \cdot {\tilde{z}}_2^{\mathrm{\prime }}(y))v\text{'}\_i\; =\; \backslash sum\_\{y\; \backslash in\; \backslash \{0,1\backslash \}^3\}\; \backslash widetilde\{M\_i\}((r\text{'}\_1,\; r\text{'}\_2),\; y)\; \backslash cdot\; (\backslash widetilde\{z\}\text{'}\_1(y)\; +\; \backslash rho\; \backslash cdot\; \backslash widetilde\{z\}\text{'}\_2(y))$

for all $i\in \{1,2,3\}i\; \backslash in\; \backslash \{1,2,3\backslash \}$.

u3 = 1 + rho
public_xx3 = public_xx1 + rho * public_xx2
vv1 = sigma1 + rho * theta1
vv2 = sigma2 + rho * theta2
vv3 = sigma3 + rho * theta3

Verifying the folded instance

We are left with a linearised CCCS relation $R_3^{\mathrm{\prime }}R\text{'}\_3$. Since our goal was only to compute two iterations, we can finally compute the sum-check on this instance. Had we wanted to run more iterations, we would accumulate these sum-checks further.

$v_i^{\mathrm{\prime }}={\sum }_{y\in \{0,1{\}}^3}\widetilde{M_i}((r_1^{\mathrm{\prime }},r_2^{\mathrm{\prime }}),y)\cdot ({\tilde{z}}_1^{\mathrm{\prime }}(y)+\rho \cdot {\tilde{z}}_2^{\mathrm{\prime }}(y))v\text{'}\_i\; =\; \backslash sum\_\{y\; \backslash in\; \backslash \{0,1\backslash \}^3\}\; \backslash widetilde\{M\_i\}((r\text{'}\_1,\; r\text{'}\_2),\; y)\; \backslash cdot\; (\backslash widetilde\{z\}\text{'}\_1(y)\; +\; \backslash rho\; \backslash cdot\; \backslash widetilde\{z\}\text{'}\_2(y))$

where $v_i^{\mathrm{\prime }}={\sigma }_i+\rho \cdot {\theta }_{i}v\text{'}\_i\; =\; \backslash sigma\_i\; +\; \backslash rho\; \backslash cdot\; \backslash theta\_i$

Note that checking $v_i^{\mathrm{\prime }}v\text{'}\_i$ implies checking both ${\sigma }_i\backslash sigma\_i$ and ${\theta }_i\backslash theta\_i$ with high probability.

By batching all $v_i^{\mathrm{\prime }}v\text{'}\_i$ with a random linear combination, checking

implies with high probability that

$v_i^{\mathrm{\prime }}={\sum }_{y\in \{0,1{\}}^3}\widetilde{M_i}((r_1^{\mathrm{\prime }},r_2^{\mathrm{\prime }}),y)\cdot ({\tilde{z}}_1^{\mathrm{\prime }}(y)+\rho \cdot {\tilde{z}}_2^{\mathrm{\prime }}(y))v\text{'}\_i\; =\; \backslash sum\_\{y\; \backslash in\; \backslash \{0,1\backslash \}^3\}\; \backslash widetilde\{M\_i\}((r\text{'}\_1,\; r\text{'}\_2),\; y)\; \backslash cdot\; (\backslash widetilde\{z\}\text{'}\_1(y)\; +\; \backslash rho\; \backslash cdot\; \backslash widetilde\{z\}\text{'}\_2(y))$

which in turn implies that ${\sigma }_i\backslash sigma\_i$ and ${\theta }_i\backslash theta\_i$ for $i\in \{1,2,3\}i\; \backslash in\; \backslash \{1,2,3\backslash \}$ are computed correctly as the prover previously claimed.

Batching sum-checks from $R_3^{\mathrm{\prime }}\in {\mathcal{R}}_{LCCCS}R\text{'}\_3\; \backslash in\; \backslash mathcal\{R\}\_\{LCCCS\}$

The verifier samples $\alpha \in \mathbb{F}\backslash alpha\; \backslash in\; \backslash mathbb\{F\}$ randomly to check

alpha = k.random_element()
alpha

81

vv = sum([
        sum([
            sum([
                Mi_linear(M1)(x11=rr1, x22= rr2, y11=y1,y22=y2,y33=y3) * (z_linear(zz1)(y11=y1,y22=y2,y33=y3) + rho * z_linear(zz2)(y11=y1,y22=y2,y33=y3)) +
                alpha * Mi_linear(M2)(x11=rr1, x22= rr2, y11=y1,y22=y2,y33=y3) * (z_linear(zz1)(y11=y1,y22=y2,y33=y3) + rho * z_linear(zz2)(y11=y1,y22=y2,y33=y3)) +
                alpha^2 * Mi_linear(M3)(x11=rr1, x22= rr2, y11=y1,y22=y2,y33=y3) * (z_linear(zz1)(y11=y1,y22=y2,y33=y3) + rho * z_linear(zz2)(y11=y1,y22=y2,y33=y3))
            for y3 in [0,1]])
        for y2 in [0,1]])
    for y1 in [0,1]])

vv

17

Round 1

Prover sends $q_{1}q\_1$ claiming to be equal to $v_{11}^{\mathrm{\prime }}v\text{'}\_\{11\}$

vv11 = sum([
        sum([
            Mi_linear(M1)(x11=rr1, x22= rr2, y22=y2,y33=y3) * (z_linear(zz1)(y22=y2,y33=y3) + rho * z_linear(zz2)(y22=y2,y33=y3)) +
                alpha * Mi_linear(M2)(x11=rr1, x22= rr2, y22=y2,y33=y3) * (z_linear(zz1)(y22=y2,y33=y3) + rho * z_linear(zz2)(y22=y2,y33=y3)) +
                alpha^2 * Mi_linear(M3)(x11=rr1, x22= rr2, y22=y2,y33=y3) * (z_linear(zz1)(y22=y2,y33=y3) + rho * z_linear(zz2)(y22=y2,y33=y3))
        for y3 in [0,1]])
    for y2 in [0,1]])
q1 = vv11

q1

32*y11^2 - 28*y11 - 44

Verifier checks that $q_1(0)+q_1(1)=v^{\mathrm{\prime }}q\_1(0)\; +\; q\_1(1)\; =\; v\text{'}$

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

True

Verifier computes a random element $r_1^{\mathrm{\prime }\mathrm{\prime }}r\text{'}\text{'}\_1$ to check that $q_{1}q\_1$ is actually $v^{\mathrm{\prime }}v\text{'}$

rrr1 = k.random_element()
rrr1

77

Round 2

Prover sends $q_{2}q\_2$ claiming to be equal to $v_{12}^{\mathrm{\prime }}v\text{'}\_\{12\}$

vv12 = sum([
        Mi_linear(M1)(x11=rr1, x22= rr2, y11=rrr1,y33=y3) * (z_linear(zz1)(y11=rrr1,y33=y3) + rho * z_linear(zz2)(y11=rrr1,y33=y3)) + 
        alpha * Mi_linear(M2)(x11=rr1, x22= rr2, y11=rrr1,y33=y3) * (z_linear(zz1)(y11=rrr1,y33=y3) + rho * z_linear(zz2)(y11=rrr1,y33=y3)) +
        alpha^2 * Mi_linear(M3)(x11=rr1, x22= rr2, y11=rrr1,y33=y3) * (z_linear(zz1)(y11=rrr1,y33=y3) + rho * z_linear(zz2)(y11=rrr1,y33=y3))
    for y3 in [0,1]])
q2 = vv12

q2

-3*y22^2 + 36*y22 + 46

Verifier checks that $q_2(0)+q_2(1)=q_1(r_1^{\mathrm{\prime }\mathrm{\prime }})q\_2(0)\; +\; q\_2(1)\; =\; q\_1(r\text{'}\text{'}\_1)$

# Verifier checks 
q2(y22=0) + q2(y22=1) == q1(y11=rrr1)

True

Verifier computes a random element $r_2^{\mathrm{\prime }\mathrm{\prime }}r\text{'}\text{'}\_2$ to check that $q_{2}q\_2$ is actually $v_{12}^{\mathrm{\prime }}v\text{'}\_\{12\}$

rrr2 = k.random_element()
rrr2

5

Round 3

$$v_{13}^{\mathrm{\prime }}=\widetilde{M_1}((r_1^{\mathrm{\prime }},r_2^{\mathrm{\prime }}),(r_1^{\mathrm{\prime }\mathrm{\prime }},r_2^{\mathrm{\prime }\mathrm{\prime }},y_3))\cdot ({\tilde{z}}_1^{\mathrm{\prime }}((r_1^{\mathrm{\prime }\mathrm{\prime }},r_2^{\mathrm{\prime }\mathrm{\prime }},y_3))+\rho \cdot {\tilde{z}}_2^{\mathrm{\prime }}((r_1^{\mathrm{\prime }\mathrm{\prime }},r_2^{\mathrm{\prime }\mathrm{\prime }},y_3)))v\text{'}\_\{13\}\; =\; \backslash widetilde\{M\_1\}((r\text{'}\_1,\; r\text{'}\_2),\; (r\text{'}\text{'}\_1,\; r\text{'}\text{'}\_2,\; y\_3))\; \backslash cdot\; (\backslash widetilde\{z\}\text{'}\_1((r\text{'}\text{'}\_1,\; r\text{'}\text{'}\_2,\; y\_3))\; +\; \backslash rho\; \backslash cdot\; \backslash widetilde\{z\}\text{'}\_2((r\text{'}\text{'}\_1,\; r\text{'}\text{'}\_2,\; y\_3)))$$

Prover sends $q_{3}q\_3$ claiming to be equal to $v_{13}^{\mathrm{\prime }}v\text{'}\_\{13\}$

vv13 = Mi_linear(M1)(x11=rr1, x22= rr2, y11=rrr1,y22=rrr2) * (z_linear(zz1)(y11=rrr1,y22=rrr2) + rho * z_linear(zz2)(y11=rrr1,y22=rrr2)) + alpha * Mi_linear(M2)(x11=rr1, x22= rr2, y11=rrr1,y22=rrr2) * (z_linear(zz1)(y11=rrr1,y22=rrr2) + rho * z_linear(zz2)(y11=rrr1,y22=rrr2)) + alpha^2 * Mi_linear(M3)(x11=rr1, x22= rr2, y11=rrr1,y22=rrr2) * (z_linear(zz1)(y11=rrr1,y22=rrr2) + rho * z_linear(zz2)(y11=rrr1,y22=rrr2))
q3 = vv13

q3

2*y33^2 + 29*y33 + 31

Verifier checks that $q_3(0)+q_3(1)=q_2(r_2^{\mathrm{\prime }\mathrm{\prime }})q\_3(0)\; +\; q\_3(1)\; =\; q\_2(r\text{'}\text{'}\_2)$

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

True

Verifier computes a random element $r_3^{\mathrm{\prime }\mathrm{\prime }}r\text{'}\text{'}\_3$ to check that $q_{3}q\_3$ is actually $v_{13}^{\mathrm{\prime }}v\text{'}\_\{13\}$

rrr3 = k.random_element()
rrr3

30

The verifier can compute now on his own

and check that $q(r_3^{\mathrm{\prime }\mathrm{\prime }})q(r\text{'}\text{'}\_3)$ is indeed that random linear combination.

c1 = Mi_linear(M1)(x11=rr1, x22= rr2, y11=rrr1,y22=rrr2, y33=rrr3) * (z_linear(zz1)(y11=rrr1,y22=rrr2, y33=rrr3) + rho * z_linear(zz2)(y11=rrr1,y22=rrr2, y33=rrr3)) + alpha * Mi_linear(M2)(x11=rr1, x22= rr2, y11=rrr1,y22=rrr2, y33=rrr3) * (z_linear(zz1)(y11=rrr1,y22=rrr2, y33=rrr3) + rho * z_linear(zz2)(y11=rrr1,y22=rrr2, y33=rrr3)) + alpha^2 * Mi_linear(M3)(x11=rr1, x22= rr2, y11=rrr1,y22=rrr2, y33=rrr3) * (z_linear(zz1)(y11=rrr1,y22=rrr2, y33=rrr3) + rho * z_linear(zz2)(y11=rrr1,y22=rrr2, y33=rrr3))

c1 == q3(y33=rrr3)

True

The Domino Effect

For reference:

• $Q^{\mathrm{\prime }}(X_1,X_2):=G^{\mathrm{\prime }}((X_1,X_2))\cdot \widetilde{eq}(({\beta }_1^{\mathrm{\prime }},{\beta }_2^{\mathrm{\prime }}),(X_1,X_2))Q\text{'}(X\_1,\; X\_2)\; :=\; G\text{'}((X\_1,\; X\_2))\; \backslash cdot\; \backslash widetilde\{eq\}((\backslash beta\text{'}\_1,\; \backslash beta\text{'}\_2),\; (X\_1,\; X\_2))$
• $L_i((X_1,X_2))=\widetilde{eq}((r_1,r_2),(X_1,X_2))\cdot H_i((X_1,X_2))L\_i((X\_1,\; X\_2))\; =\; \backslash widetilde\{eq\}((r\_1,\; r\_2),\; (X\_1,\; X\_2))\; \backslash cdot\; H\_i((X\_1,\; X\_2))$
• $H_i((X_1,X_2)):={\sum }_{y\in \{0,1{\}}^3}{\tilde{M}}_i((X_1,X_2),y)\cdot {\tilde{z}}_1^{\mathrm{\prime }}(y)H\_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\}\text{'}\_1(y)$
• ${\sigma }_i=H_i((r_1^{\mathrm{\prime }},r_2^{\mathrm{\prime }}))={\sum }_{y\in \{0,1{\}}^3}\widetilde{M_i}((r_1^{\mathrm{\prime }},r_2^{\mathrm{\prime }}),y)\cdot {\tilde{z}}_1^{\mathrm{\prime }}(y)\backslash sigma\_i\; =\; H\_i((r\text{'}\_1,\; r\text{'}\_2))\; =\; \backslash sum\_\{y\; \backslash in\; \backslash \{0,\; 1\; \backslash \}^3\}\; \backslash widetilde\{M\_i\}((r\text{'}\_1,\; r\text{'}\_2),\; y)\; \backslash cdot\; \backslash widetilde\{z\}\text{'}\_1(y)$
• ${\theta }_i=L_i((r_1^{\mathrm{\prime }},r_2^{\mathrm{\prime }}))={\sum }_{y\in \{0,1{\}}^3}\widetilde{M_i}((r_1^{\mathrm{\prime }},r_2^{\mathrm{\prime }}),y)\cdot {\tilde{z}}_2^{\mathrm{\prime }}(y)\backslash theta\_i\; =\; L\_i((r\text{'}\_1,\; r\text{'}\_2))\; =\; \backslash sum\_\{y\; \backslash in\; \backslash \{0,\; 1\; \backslash \}^3\}\; \backslash widetilde\{M\_i\}((r\text{'}\_1,\; r\text{'}\_2),\; y)\; \backslash cdot\; \backslash widetilde\{z\}\text{'}\_2(y)$
• $g_1((X_1,X_2))={\sum }_{j\in \{1,2,3\}}{\gamma }^j\cdot L_j((X_1,X_2))g\_1((X\_1,\; X\_2))\; =\; \backslash sum\_\{j\; \backslash in\; \backslash \{1,2,3\backslash \}\}\; \backslash gamma^j\; \backslash cdot\; L\_j((X\_1,\; X\_2))$
• $g((X_1,X_2))=g_1((X_1,X_2))+{\gamma }^4{Q}^{\mathrm{\prime }}((X_1,X_2))g((X\_1,\; X\_2))\; =\; g\_1((X\_1,\; X\_2))\; +\; \backslash gamma^4\; Q\text{'}((X\_1,\; X\_2))$

The verifier has now checked that $v_1^{\mathrm{\prime }},v_2^{\mathrm{\prime }},v_3^{\mathrm{\prime }}v\text{'}\_1,\; v\text{'}\_2,\; v\text{'}\_3$ from $R_3^{\mathrm{\prime }}R\text{'}\_3$ are the values that the prover claimed by checking their random linear combination. This in turn implies that ${\sigma }_1,{\sigma }_2,{\sigma }_3\backslash sigma\_1,\; \backslash sigma\_2,\; \backslash sigma\_3$ and ${\theta }_1,{\theta }_2,{\theta }_3\backslash theta\_1,\; \backslash theta\_2,\; \backslash theta\_3$ are indeed the values that the prover's claimed. Thus, the verifier is assured about the validity of the sum-checks from $R_1^{\mathrm{\prime }}\in {\mathcal{R}}_{LCCCS}R\text{'}\_1\; \backslash in\; \backslash mathcal\{R\}\_\{LCCCS\}$ and $R_2^{\mathrm{\prime }}\in {\mathcal{R}}_{CCCS}R\text{'}\_2\; \backslash in\; \backslash mathcal\{R\}\_\{CCCS\}$

In other words, by checking that

${\sum }_{j\in \{1,2,3\}}{\gamma }^j\cdot v_j+{\gamma }^4\cdot 0={\sum }_{x_1\in \{0,1\}}{\sum }_{x_2\in \{0,1\}}g((x_1,x_2))\backslash sum\_\{j\; \backslash in\; \backslash \{1,2,3\backslash \}\}\; \backslash gamma^j\; \backslash cdot\; v\_j\; +\; \backslash gamma^4\; \backslash cdot\; 0\; =\; \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))$, for $g(x)=g_1(x)+{\gamma }^4{Q}^{\mathrm{\prime }}(x)g(x)\; =\; g\_1(x)\; +\; \backslash gamma^4\; Q\text{'}(x)$,

the verifier is thus implicitely verifying all claims of $R_1^{\mathrm{\prime }}\in {\mathcal{R}}_{LCCCS}R\text{'}\_1\; \backslash in\; \backslash mathcal\{R\}\_\{LCCCS\}$ and $R_2^{\mathrm{\prime }}\in {\mathcal{R}}_{CCCS}R\text{'}\_2\; \backslash in\; \backslash mathcal\{R\}\_\{CCCS\}$, which are encoded in $g_{1}g\_1$ and $Q^{\mathrm{\prime }}(x)Q\text{'}(x)$, respectively. We can apply recursively this logic, since $R_3=R_1^{\mathrm{\prime }}R\_3\; =\; R\text{'}\_1$, which checks $R_2\in {\mathcal{R}}_{CCCS}R\_2\; \backslash in\; \backslash mathcal\{R\}\_\{CCCS\}$ and $R_1\in {\mathcal{R}}_{LCCCS}R\_1\; \backslash in\; \backslash mathcal\{R\}\_\{LCCCS\}$.

More precisely, checking

implies with high probability that

$v_i^{\mathrm{\prime }}={\sum }_{y\in \{0,1{\}}^3}\widetilde{M_i}((r_1^{\mathrm{\prime }},r_2^{\mathrm{\prime }}),y)\cdot ({\tilde{z}}_1^{\mathrm{\prime }}(y)+\rho \cdot {\tilde{z}}_2^{\mathrm{\prime }}(y))v\text{'}\_i\; =\; \backslash sum\_\{y\; \backslash in\; \backslash \{0,1\backslash \}^3\}\; \backslash widetilde\{M\_i\}((r\text{'}\_1,\; r\text{'}\_2),\; y)\; \backslash cdot\; (\backslash widetilde\{z\}\text{'}\_1(y)\; +\; \backslash rho\; \backslash cdot\; \backslash widetilde\{z\}\text{'}\_2(y))$

which implies with high probability that

• ${\sigma }_i={\sum }_{y\in \{0,1{\}}^3}\widetilde{M_i}((r_1^{\mathrm{\prime }},r_2^{\mathrm{\prime }}),y)\cdot {\tilde{z}}_1^{\mathrm{\prime }}(y)\backslash sigma\_i\; =\; \backslash sum\_\{y\; \backslash in\; \backslash \{0,\; 1\; \backslash \}^3\}\; \backslash widetilde\{M\_i\}((r\text{'}\_1,\; r\text{'}\_2),\; y)\; \backslash cdot\; \backslash widetilde\{z\}\text{'}\_1(y)$
• ${\theta }_i={\sum }_{y\in \{0,1{\}}^3}\widetilde{M_i}((r_1^{\mathrm{\prime }},r_2^{\mathrm{\prime }}),y)\cdot {\tilde{z}}_2^{\mathrm{\prime }}(y)\backslash theta\_i\; =\; \backslash sum\_\{y\; \backslash in\; \backslash \{0,\; 1\; \backslash \}^3\}\; \backslash widetilde\{M\_i\}((r\text{'}\_1,\; r\text{'}\_2),\; y)\; \backslash cdot\; \backslash widetilde\{z\}\text{'}\_2(y)$

which allows the verifier to verify that

which he previously assumed to be true, from the values ${\sigma }_i\backslash sigma\_i$ and ${\theta }_i\backslash theta\_i$ given by the prover.

This implies that

${\sum }_{j\in \{1,2,3\}}{\gamma }^j\cdot v_j+{\gamma }^4\cdot 0={\sum }_{x_1\in \{0,1\}}{\sum }_{x_2\in \{0,1\}}g((x_1,x_2))=g_1(x)+{\gamma }^4{Q}^{\mathrm{\prime }}(x)\backslash sum\_\{j\; \backslash in\; \backslash \{1,2,3\backslash \}\}\; \backslash gamma^j\; \backslash cdot\; v\_j\; +\; \backslash gamma^4\; \backslash cdot\; 0\; =\; \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))\; =\; g\_1(x)\; +\; \backslash gamma^4\; Q\text{'}(x)$

which implies with high probability that

and

Summary

We made it, again! We have managed to fold two iterations of our Fibonacci example and then verify the folding protocol by sum-checking the final linearised CCCS relation $R_3^{\mathrm{\prime }}R\text{'}\_3$.

At each iteration, the incoming relation $R_2^{(k)}\in {\mathcal{R}}_{CCCS}R^\{(k)\}\_2\; \backslash in\; \backslash mathcal\{R\}\_\{CCCS\}$ generates random values $r^{(k)}\in \mathbb{F}r^\{(k)\}\; \backslash in\; \backslash mathbb\{F\}$ that are propagated to the next accumulated relation $R_1^{(k+1)}\in {\mathcal{R}}_{LCCCS}R^\{(k+1)\}\_1\; \backslash in\; \backslash mathcal\{R\}\_\{LCCCS\}$. This serves as the glue that makes the domino effect possible.

We batched many of the sum-checks into a single sum-check using a random linear combination of the sums, thus avoiding unnecessary computation when needed.

There was a lot of work and wit put into SuperSpartan and HyperNova. I hope this post contributes to spread the understanding of such inspiring work.

Thanks for reading!