Table of Contents
R1CS encoding
R1CS instance \(x=(\mathbb{F},A,B,C,io,m,n)\)
let \(Z=(io,1,w)\), then we have for example
\(\underbrace{\begin{bmatrix}0&1&1&0\\0&0&1&0\\…&…&…&..\\…&…&…&..\end{bmatrix}}_{A}\begin{pmatrix}w_1\\1\\w_2\\w_3\end{pmatrix}\circ \underbrace{\begin{bmatrix}0&1&0&0\\0&0&1&0\\…&…&…&..\\…&…&…&..\end{bmatrix}}_{B}\begin{pmatrix}w_1\\1\\w_2\\w_3\end{pmatrix}\)
\(=\underbrace{\begin{bmatrix}1&0&0&0\\0&0&0&1\\…&…&…&..\\…&…&…&..\end{bmatrix}}_{C}\begin{pmatrix}w_1\\1\\w_2\\w_3\end{pmatrix}\)
This express the constraints:
$$(1+w_2) \cdot 1=w_1$$
$$w_2 \cdot w_2=w_3$$
In order to use the sum-check protocol, we need to encode R1CS in a different way, as sum-check is about binary representations, therefore, it ends up something like this:
\(F_{io}(x)=\left(\sum\limits_{y\in\{0,1\}^s}A(x,y)\cdot Z(y)\right)\cdot \left(\sum\limits_{y\in\{0,1\}^s}B(x,y)\cdot Z(y)\right)\)
$$-\left(\sum\limits_{y\in\{0,1\}^s}C(x,y)\cdot Z(y)\right)$$
view \(x\) as the row number and \(y\) as the column, let me write the above equation in another way:
\(\underbrace{\begin{bmatrix}\widetilde{A}([00],[00])&\widetilde{A}([00],[01])&\widetilde{A}([00],[10])&\widetilde{A}([00],[11])\\\widetilde{A}([01],[00])&\widetilde{A}([01],[01])&\widetilde{A}([01],[10])&\widetilde{A}([01],[11])\\…&…&…&..\\…&…&…&..\end{bmatrix}}_{A}\begin{pmatrix}z([00])\\z([01])\\z([10])\\z([11])\end{pmatrix}\)
\(\circ \underbrace{\begin{bmatrix}\widetilde{B}([00],[00])&\widetilde{B}([00],[01])&\widetilde{B}([00],[10])&\widetilde{B}([00],[11])\\\widetilde{B}([01],[00])&\widetilde{B}([01],[01])&\widetilde{B}([01],[10])&\widetilde{B}([01],[11])\\…&…&…&..\\…&…&…&..\end{bmatrix}}_{B}\begin{pmatrix}z([00])\\z([01])\\z([10])\\z([11])\end{pmatrix}\)
\(=\underbrace{\begin{bmatrix}\widetilde{B}([00],[00])&\widetilde{B}([00],[01])&\widetilde{B}([00],[10])&\widetilde{B}([00],[11])\\\widetilde{B}([01],[00])&\widetilde{B}([01],[01])&\widetilde{B}([01],[10])&\widetilde{B}([01],[11])\\…&…&…&..\\…&…&…&..\end{bmatrix}}_{C}\begin{pmatrix}z([00])\\z([01])\\z([10])\\z([11])\end{pmatrix}\)
\(=\begin{pmatrix}\left(\sum\limits_{y\in\{0,1\}^2}A([00],y)z(y)\right)\cdot\left(\sum\limits_{y\in\{0,1\}^2}B([00],y)z(y)\right)-\left(\sum\limits_{y\in\{0,1\}^2}C([00],y)z(y)\right) \\\left(\sum\limits_{y\in\{0,1\}^2}A([01],y)z(y)\right)\cdot\left(\sum\limits_{y\in\{0,1\}^2}B([01],y)z(y)\right)-\left(\sum\limits_{y\in\{0,1\}^2}C([01],y)z(y)\right)\\z([10])\\z([11])\end{pmatrix}\)
\(=\begin{pmatrix}\widetilde{F}_{io}([00])\\\widetilde{F}_{io}([01])\\\widetilde{F}_{io}([10])\\\widetilde{F}_{io}([11])\end{pmatrix}\)
Now come to Lemma 4.1 in Spartan paper, the conclusion is straight forward.
Til now we can talk about sum-check protocol with variate \(y\in \{0,1\}^s\), we would like one more layer of sum-check, namely, make \(x\) also into variate.
let
\(\mathcal{G}_{io,\tau}(x)=\widetilde{F}_{io}(x)\cdot \widetilde{eq}(\tau,x)\)
\(\mathcal{Q}_{io}(\tau)=\sum\limits_{x\in \{0,1\}^s}\mathcal{G}_{io,\tau}(x)=\sum\limits_{x\in \{0,1\}^s}\widetilde{F}_{io}(x)\cdot \widetilde{eq}(\tau,x)\)
Now our goal is to check if \(\mathcal{Q}_{io}(\tau)=0\), this claim can be reduced to \(e_x\stackrel{?}{=}\mathcal{G}_{io,\tau}(r_x)\) where \(r_x\in \mathbb{F}^s\) (recall the last step of a sum-check protocol is an evaluation of a function in a random point.)
from the equation
\(\widetilde{F}_{io}(x)=\left(\sum\limits_{y\in\{0,1\}^s}\widetilde{A}(x,y)\cdot Z(y)\right)\cdot \left(\sum\limits_{y\in\{0,1\}^s}\widetilde{B}(x,y)\cdot Z(y)\right)\)
$$-\left(\sum\limits_{y\in\{0,1\}^s}\widetilde{C}(x,y)\cdot Z(y)\right)$$
The prover can then make three separate claims to \(\mathcal{V}\) :
$$\bar{A}(r_x)=v_A,\bar{B}(r_x)=v_B,\bar{C}(r_x)=v_C$$
(why the tilde becomes bar? because the values here is the product of matrix and witness, name \(\bar{A}(r_x)=\sum\limits_{y\in\{0,1\}^s}\widetilde{A}(x,y)\cdot Z(y)\))
Then \(\mathcal{V}\) can evaluate
$$\mathcal{G}_{io,\tau}(r_x)=(v_A\cdot v_B – v_C)\cdot \tilde{eq}(r_x,\tau)$$
Then \( \mathcal{V}\) needs to use three sum-check protocol to check \(v_A,v_B,v_C\) are correct.
There is a way to combine three checks into one. Namely, \(\mathcal{V}\) samples \(r_A,r_B,r_C\) computes
$$c=r_A\cdot v_A+r_B\cdot v_B+r_C\cdot v_C$$
and checks with the prover
$$r_A\cdot \bar{A}(r_x)+r_B\cdot \bar{B}(r_x)+r_C\cdot \bar{C}(r_x)\stackrel{?}{=}c$$
which means, the combined sum-check is for
\(L(r_x)= \sum\limits_{y\in\{0,1\}^s}\left(r_A\widetilde{A}(x,y)+ r_B \cdot\widetilde{B}(x,y)+ r_C \cdot\widetilde{C}(x,y)\right)\cdot \widetilde{Z}(y)\)
\(= \sum\limits_{y\in\{0,1\}^s}M_{r_x}(y)\)