Notes on (Super)spartan

I think that the superspartan paper doesn't lack maths, but a bit of motivation and intuition. Hence, I will sometimes handwave the maths in the benefit of prose. Note that superspartan is a generalization of spartan. The intuition that we lay out also works for spartan.

Superspartan is a polynomial IOP for CCS, described in the same paper. Let's quickly review here the notational definition from the CCS paper, for reading practicality.

A CCS structure $\mathcal{S}$ consists of:

• Size bounds $m, n, N, l, t, q, d \in N$ where $n \gt N$
• A sequence of matrices $M_0, \dots, M_{t-1} \in F^{m \times n}$
• A sequence of $q$ multisets [$S_0, \dots, S_{q-1}$] where an element in each multiset is from the domain ${0, \dots, t-1}$ and the cardinality of each multiset is at most $d$
• A sequence of $q$ constants [$c_0, \dots, c_{q-1}$], where each constant is from $F$.

Superspartan leverages the sumcheck protocol. Sumcheck is an interactive protocol between a prover $P$ and a verifier $V$. $P$ uses sumcheck to convince $V$ that a claimed sum $H$ is equal to the summation of a polynomial over an hypercube of size $k$. That is, $P$ wants to convince $V$ that for a given multivariate polynomial $g(x_0, \dots, x_k)$:

where $\{0, 1\}^{k}$ is the hypercube of size $k$. Sumcheck requires $k$ communication rounds and a final oracle query of $V$ to evaluate $g(x_0, ..., x_k)$ at a random point $r \in F^{k}$.

An intuitive explanation for superspartan

Turning the CCS into MLEs

Let $z = (1, x, w)$, where $w$ is a purported satisfying witness for a CCS structure-instance tuple $(\mathcal{S}, x)$. In the context of superspartan, a prover $P$ wants to convince a verifier $V$ that a $z$ vector is a satisfying assignment to a CCS structure $\mathcal{S}$.

In the preprocessing phase, turn CCS matrices $M_0, \dots, M_{t-1}$ into a set of multilinear extensions (MLEs) in $log(m) + log(n)$ variables: $\widetilde{M}_{0}(x, y), \dots, \widetilde{M}_{t-1}(x, y)$. Do the same for the $z$ vector, to obtain $\widetilde{Z}(y)$, an MLE in $log(n)$ variables.

Using the definition of an MLE, observe that for, say $M_0$, turning it into an MLE means that we will get $\widetilde{M}_0(x, y) = M_0[x][y]$. MLEs re-interpret matrices as functions in $log(m) + log(n)$ variables. Similarly, for the vector $z$, $\widetilde{Z}(y) = z[y]$. This is (roughly) the preprocessing step for superspartan: MLEs are used to turn the original CCS into a set of low-degree polynomials.

Next, using those low-degree polynomials, $P$ will use the sumcheck protocol to convince $V$ that the CCS instance-structure tuple $(x, \mathcal{S})$ is satisfied by $z$.

Prove the knowledge of a satisfying assignment, with sumcheck

Once the MLE pre-processing is done, the idea is to prove that $z$ satisfies $(\mathcal{S}, x)$ with sumcheck. To do this, $P$ and $V$ will perform two invocations of the sumcheck protocol. The first invocation consists into $P$ showing that when turned into an MLE, say $g(x_0, \dots, x_k)$ where $k = log(n) + log(m)$, the CCS is satisfied by $z$.

However, $V$ will need to evaluate $g(x_0, \dots, x_k)$ at a random point to conclude this first sumcheck invocation (the final oracle query mentioned above). Hence, the second sumcheck invocation will consists into $P$ convincing $V$ that the evaluation of $g(x_0, \dots, x_k)$ at the first sumcheck invocation's random point $r_a$ is correct.

Superspartan, commented

I'm commenting here the pseudocode laid out in figure 2 (p.15). I'm not a fiat-shamir expert, so I omitted what should be hashed to obtain random challenges.

1. $P$ sends $V$ the MLE of $w$, noted $\widetilde{W}$
2. $V$ sends a random challenge $\tau$ to $P$. $P$ uses fiat shamir to obtain $\tau$ non-interactively
3. Apply the sum check protocol over the CCS-turned-MLE $g(x_0, \dots, x_k)$ polynomial. Observe that the sum in equation $(15)$ is basically the sum used for checking that a CCS is satisfied by a witness $w$, in equation $(2)$. Hence, this first sum check is used to prove that the sum of $g(x_0, \dots, x_k)$, done over the hypercube of size $log(m)$, is 0. Observe that $\widetilde{eq}(\tau, a)$ enforces this sum to be done a specific row of the CCS; i.e. a row "selected" by the verifier using a random challenge. At the end of this first sumcheck, $V$ still has to ensure that the final evaluation $g(r_a)$ is correct, for $r_a \in F^{log (m)}$.
4. $V$ sends a random challenge $\gamma$ to $P$. Using fiat-shamir, $P$ obtains it non-interactively
5. $P$ sends claimed sums over the hypercube of size $log(n)$ for $\widetilde{M}(r_a, y) \cdot \widetilde{Z}(y)$. To check those claimed sum, $V$ and $P$ run the sum check protocol to compute the sum over the hypercube of size $log(n)$ of a random linear combination of $\gamma^{i} \cdot \widetilde{M}_(r_a, y) \cdot \widetilde{Z}(y)$. The random linear combination is useful to avoid running as many sumcheck invocations as they are matrices and instead run a single one

When all of the above is done, $V$ performs the three following checks:

1. The claimed sums for $\widetilde{M}(r_a, y) \cdot \widetilde{Z}(y)$ are correct. Simply take their random linear combination and compare the result to the second sumcheck proof.
2. The final evaluation $\gamma^{i} \cdot \widetilde{M}_(r_a, r_y) \cdot \widetilde{Z}(r_y)$ is correct. $V$ has access to those MLEs as oracles, the check is straightforward.
3. Using the above sums for $\widetilde{M}(r_a, y) \cdot \widetilde{Z}(y)$, compute the evaluation $g(r_a)$ and assert that it is equal to the claimed evaluation in the first sumcheck invocation.