Spartan

These are notes on just a small part of Spartan: Efficient and general-purpose zkSNARKs without trusted setup (opens new window).

Spartan offers the first zkSNARKs without a trusted setup for NP, where verifying a proof incurs sub-linear costs—without requiring uniformity in the NP statement’s structure.

The core insight is that the sum-check protocol, when applied to a suitably constructed low-degree polynomial, yields a powerful—but highly inefficient—interactive proof protocol. However, the inefficiency can be tamed with new techniques.

Sum-check protocol

Suppose there is a function $f(x_1, ..., x_n)$, and a prover wants to prove that

$H = \sum_{(x_1, ..., x_n) \in \{0, 1\}^n} f(x_1, ..., x_n)$

for some value $H$. The sum-check protocol enables proving such a statement.

When we want to prove, for example, that the vector $v$ has the sum of its coefficients equal to $H$, we observe $v$ as a function. Let’s say $v$ has $8$ coefficients:

$v = \begin{pmatrix} v_0 \\ v_1 \\ v_2 \\ v_3 \\ v_4 \\ v_5 \\ v_6 \\ v_7 \end{pmatrix}$

We see $v$ as a function $f$ of $3$ variables ($2^3 = 8$):

$v = \begin{pmatrix} f(0, 0, 0) \\ f(0, 0, 1) \\ f(0, 1, 0) \\ f(0, 1, 1) \\ f(1, 0, 0) \\ f(1, 0, 1) \\ f(1, 1, 0) \\ f(1, 1, 1) \end{pmatrix}$

By using the sum-check protocol, we can prove $v_0 + v_1 + ... + v_7 = H$.

In fact, many times it’s needed to prove that each coefficient is equal to zero:

$v_0 = 0$

$...$

$v_7 = 0$

This can be achieved by a zero-check protocol, which is an extension of the sum-check protocol.

So, how does Spartan use the sum-check protocol?

Encoding of R1CS instances as low-degree polynomials

Theorem 4.1 from the paper roughly says that for any R1CS instance, there exists a degree-3 $log(m)$-variate polynomial $G$ such that $\sum_{x \in \{0, 1\}^{log(m)}} G(x) = 0$ if and only if there exists a witness $w$ such that $Sat_{R1CS}(x, w) = 1$ (the witness $w$ satisfies the constraint system).

Let’s say we have the following constraint system:

$A z \circ B z - C z = 0$

$\begin{pmatrix} & & & \\ & & & \\ & & & \\ & & & \end{pmatrix} \begin{pmatrix} \\ \\ \\ \end{pmatrix} \circ \begin{pmatrix} & & & \\ & & & \\ & & & \\ & & & \end{pmatrix} \begin{pmatrix} \\ \\ \\ \end{pmatrix} - \begin{pmatrix} & & & \\ & & & \\ & & & \\ & & & \end{pmatrix} \begin{pmatrix} \\ \\ \\ \end{pmatrix} = 0$

How do we transform this system into an equation $\sum_{x \in \{0, 1\}^{log(m)}} G(x) = 0$?

We can view matrices $A, B, C \in \mathbb{F}^{m \times m}$ as functions with the following signature: $\{0, 1\}^s \times \{0, 1\}^s \rightarrow \mathbb{F}$ where $s = log(m)$.

We view $A, B, C$ as vectors of $2s$ coefficients (functions on the hyperboolean cube of dimension $2s$). The first $s$ coordinates denote the row, the second $s$ coordinates denote the column:

$A[0][0] = \tilde A(0, ..., 0, 0, ..., 0)$

$A[0][1] = \tilde A(0, ..., 0, 0, ..., 1)$

$A[0][m] = \tilde A(0, ..., 0, 1, ..., 1)$

$...$

$\tilde A$, $\tilde B$, $\tilde C$ are MLEs of $A, B, C$.

Let’s write $z = (io, 1, w)$, where $io$ is the input and $w$ is the witness. We view $z$ as a function on the hyperboolean cube of dimension $s$, and we take its MLE: $\tilde z$.

Let’s have the following function for $x \in \{0, 1\}^s$:

$f(x) = \sum_{y \in \{0, 1\}^s} \tilde A(x, y) \tilde z(y) \cdot \sum_{y \in \{0, 1\}^s} \tilde B(x, y) \tilde z(y) - \sum_{y \in \{0, 1\}^s} \tilde C(x, y) \tilde z(y)$

Using the sum-check protocol, we can now prove:

$\sum_{x \in \{0, 1\}^s} f(x) = 0$

But this is not what we need. However, our R1CS can be rewritten as:

$f(x) = 0 \; \text{for} \; \text{each} \; x \in \{0, 1\}^s$

And this can be proven by the zero-check protocol, which means running the sum-check protocol for the following polynomial:

$g(t) = \sum_{x \in \{0, 1\}^s} f(x) \cdot eq(t, x)$

where

$eq(t, x) = \Pi_{i=1}^s (t_i x_i + (1-t_i)(1 - x_i))$

In the sum-check protocol, the prover does most of the work, and the verifier is left to compute one evaluation of the function at a random point:

$e_x = g(r_x)$

where $e_x$ is computed by the prover and $r_x$ is a random point from $\mathbb{F}^s$.

So, the verifier needs to efficiently compute $g(r_x)$. The paper proposes the prover to compute:

$v_A = \sum_{y \in \{0, 1\}^s} \tilde A(r_x, y) \tilde z(y)$

$v_B = \sum_{y \in \{0, 1\}^s} \tilde B(r_x, y) \tilde z(y)$

$v_C = \sum_{y \in \{0, 1\}^s} \tilde C(r_x, y) \tilde z(y)$

The verifier then needs to check:

$e_x = (v_A v_B - v_C) \cdot eq(\tau, r_x)$

However, the prover needs to prove that $v_A, v_B, v_C$ have been computed correctly, and for this, the sum-checks can be used again (three sum-checks or, better, a random linear combination of three sum-checks). The claims to be checked are:

$v_A = \tilde A(r_x, r_y) z(r_y)$

$v_B = \tilde B(r_x, r_y) z(r_y)$

$v_C = \tilde C(r_x, r_y) z(r_y)$