# Spartan SumCheck-Trick

This post will describe the basic strategy of the [Spartan](https://eprint.iacr.org/2019/550.pdf) proof system for $\text{R1CS}$ constraints and pin-point a key trick which may be useful in other contexts.

R1CS
===
The Language $$\mathcal{L}_{\text{R1CS}} := \{(\mathbb{F}, A, B, C, x, m, n) | \exists w \text{ s.t. } (Az)\circ (Bz) = Cz, z = (x,1,w) \}$$
is $\text{NP}$-complete - i.e. it has enough structure to express arbitrary computations (proof sketch: take a circuit-sat instance and construct a collection of quadratic polynomials over $\mathbb{F}_2$ which are simulatenously satisfiable iff the circuit-sat instance is satisfiable). Here
* $\mathbb{F}$ is a field (Think scalar field of an elliptic curve $E/\mathbb{F}_p$)
* $A,B,C$ are $m\times m$ matrices with values in $\mathbb{F}$ with at most $n$ non-zero entries.
($A,B,C$ being square is for convenience)
* $x$ is a $\mathbb{F}$-vector of dimension $< m$ representing public I/O.

Spartan is a proof system for $\mathcal{L}_{\text{R1CS}}$. Impressively,
> "Spartan offers the first transparent zkSNARK that achieves sub-linear verification costs for arbitrary NP statements." - [Spartan](https://eprint.iacr.org/2019/550.pdf)

(N.B: zkSnark = Zero Knowledge Non-Interactive Argument of Knowledge,
Transparent = No trusted setup.)

Spartan Proof System
===
Recall the **Sum-Check Protocol** allows a Prover to convince a Verifier of the value of
$$ \sum_{x_1\in \{0,1\}}\cdots \sum_{x_\mu\in \{0,1\}}P(x_1, \cdots, x_{\mu}). $$
for a polynomial $P$. (With a little work, this protocol can be used to show that $\text{IP} = \text{PSPACE}$, demonstrating its power).

We will only give a very brief sketch of the protocol here, and a succint summary can be found [here](https://people.cs.georgetown.edu/jthaler/sumcheck.pdf). The basic idea is to proceed in $\mu$ rounds. In each round $1\leq i\leq \mu$, the verifier specifies a random field element $r_i$, and has the prover send the univariate polynomial in $X_i$ having fixed the first $i - 1$ variables as $r_1, \cdots, r_{i - 1}$ and summing over the remaining variables. The verifier then does a quick check each round to make sure that the answer is consistent with the answer of the previous round.

To briefly discuss the costs: For each of the $\mu$ rounds, the prover sends the verifier a polynomial of degree $d_i := \text{deg}_{x_i}(P)$, which entails $d_i + 1$ field elements. The verifier needs to make 3 evaluations of this polynomial (at $0$, $1$, and a random point $r$), and at the end of the protocol query $P$ at a single point. If $T$ is the time it takes to query $P$ at a point, then the verifier complexity is $O(d\mu + T)$, where $d = \text{max}_i d_i$. The prover complexity is $O(2^\mu T)$, which accounts for both computing the sum over the hypercube and constructing the polynomials to send to the verifier (to derive this latter cost, use the fact that in each subsequent round, the number of terms in the polynomial that the prover must sent halves.)

Spartan will try to convert the satisfiability of an $\text{R1CS}$ instance into a claim whose proof is amenable to the sum-check protocol.

The first step is to *view matrices as multilinear polynomials*. Let $s = \log m$, and view $A,B,C$ as functions $A,B,C: \{0,1\}^{s}\times \{0,1\}^{s}\rightarrow \mathbb{F}$ mapping a pair of indices $(r,c)$ to matrix entry at that position. Let $\tilde{A}, \tilde{B}, \tilde{C}: \{0,1\}^s\times \{0,1\}^s \rightarrow \mathbb{F}$ be their respective multilinear extensions. For $Z = (x, 1, w)$, define $Z: \{0,1\}^s \rightarrow \mathbb{F}$ and let $\tilde{Z}$ be its multilinear extension. Finally, define
$$\tilde{F}(r) := (\sum_{c\in \{0,1\}^s}\tilde{A}(r,c)\tilde{Z}(c))*(\sum_{c\in \{0,1\}^s}\tilde{B}(r,c)\tilde{Z}(c)) - (\sum_{c\in \{0,1\}^s}\tilde{C}(r,c)\tilde{Z}(c)) $$
Then $Z$ satsfies the $\text{R1CS}$ instance iff $\tilde{F}(r) = 0$ for all $r\in \{0,1\}^s$ - the equality $\tilde{F}(r) = 0$ for fixed $r$ implies that $Z$ satsifies the constraint imposed by the $r$th row of the matrices $A,B,C$.

At this point, we may be tempted to just use the sum-check protocol to show that $\sum_{r\in \{0,1\}^s}\tilde{F}(r) = 0$. Unfortunately, this is not enough to conclude that $\tilde{F}(r) = 0$ for all $r$, because their may be some non-trivial cancellation in the sum.

This is where the *Spartan Trick* comes in.

**Spartan Trick:** For any $P\in \mathbb{F}[x_1, \cdots, x_s]$,
$$P(x) = 0 \space \forall x\in \{0,1\}^s \Longleftrightarrow \sum_{r\in \{0,1\}^s}P(r)\prod_{i = 1}^{s}(x_i r_i + (1 - x_i)(1 - r_i)) = 0 \space \forall x\in \{0,1\}^s.$$
(The proof of the trick is straightfoward, it just uses the fact that $\prod_{i = 1}^{s}(x_ir_i + (1 - x_i)(1 - r_i)) = 1$ iff $x_i = r_i$ $\forall i$ and is equal to $0$ otherwise.)

The key point is that the polynomial in the RHS is a sum over the boolean hypercube of a multilinear polynomial in the $r_i$, so for a given $x\in \{0,1\}^s$, the sum-check protocol can be used to show that this sum is zero. But by the *Schwartz-Zippel* lemma, it is enough to show that the RHS is zero for a randomly chosen $x\in \{0,1\}^s$ (Indeed, the expression on the RHS is just some multilinear polynomial in the $x_i$).

Thus, taking $P = \tilde{F}$, the *Spartan Trick* (together with Schwartz-Zippel) reduces the satisfiability of the original $\text{R1CS}$ instance to showing that, after picking a random $x\in \{0,1\}^s$, the sum of
$$\mathcal{F}(r_1, \cdots, r_s) := \tilde{F}(r_1, \cdots r_s)\prod_{i = 1}^{s}(x_ir_i + (1 - x_i)(1 - r_i))$$
over the boolean hypercube is equal to $0$, which is exactly what the sum-check protocol was designed for. The costs can be determined by the discussion of the costs of the sum-check protocol in general, and noting that the polynomial $\mathcal{F}$ has degree $3$ and is $s$-variate.