Cinder: A simple-but-not-so-efficient dense-to-sparse MLE compiler

tl;dr: Spartan is a versatile zkSNARK framework that requires a sparse MLE PCS to be instantiated. This blog post explains a simple (and likely well-known) compiler to get such a PCS given a weaker dense PCS as input.

Preliminaries

We assume familiarity with the Spartan protocol and its mathematical preliminaries:

• MLEs
• sumchecks
• Lagrange polynomials for interpolating MLEs
• dense MLE PCSs
• sparse MLE PCSs

Notation

• We use $[s) \bydef \{0,1,\ldots,s-1\}$.
• We typically denote the boolean hypercube of size $2^s$ as $\binS$.
• $\SC.\prove(F, T, s, d)\rightarrow (\pi,e; \r)$ is an algorithm that reduces $\sum_{\b \in \binS} F(\b) = T$ on an $s$-variate polynomial of max degree $d$ to:
  1. verifying a sumcheck proof $\pi$
  2. verifiying the $F(\r) = e$ opening for some random $\r\in \F^s$ (picked after $F$ is fixed)
• We use $a\fsget S$ to denote sampling from a set $S$ in a deterministic manner using the Fiat-Shamir transcript $\FS$ derived so far
• We use $\mathcal{A}^\FSo$ to indicate that an algorithm $\mathcal{A}$ has oracle access to the Fiat-Shamir transcript $\FS$ and can read and append to it.

Cinder explanation

The Spartan paper explained Spark, a compiler that takes any dense MLE PCS for size-$n$ MLEs and turns it into a sparse one for size $m^2$ MLEs with only $n \approx m$ non-zero entries.

This section explains Cinder, a much simpler (but a bit more expensive) compiler than Spark¹.

Recall that $m=2^s$ and that we have a size-$m^2$ MLE $\tilde{V}$ of a sparse R1CS square matrix, say, $V=(V_{i,j})_{i,j\in[m)}$ with $n\approx m$ non-zero entries: \begin{align} \tilde{V}(\X,\Y) = \sum_{\i\in\binS,\j\in\binS} V_{i,j}\cdot\eq_i(\X)\eq_j(\Y) \end{align}

Our goal is to come up with an MLE PCS so we can efficiently and provably open $\tilde{V}$ at the random $(\r_x,\r_y)$ point picked by the verifier: \begin{align} \label{eq:r1cs-matrix-sumcheck} \tilde{V}(\r_x,\r_y) = \sum_{\i\in\binS,\j\in\binS} A_{i,j}\cdot\eq_i(\r_x)\eq_j(\r_y) \end{align}

Our approach: Take Spark and implement the most naive variant of it you can imagine!

I’d bet at least three sangrias that this Cinder approach was probably described in some paper or even in Spartan itself. A similar idea, but around a permutation MLE $\sigma$, is described in the HyperPLONK paper² (see Section 3.6 on “Another permutation PIOP”). Hopefully, someone more knowledgeable than me will confirm and I will add more context after!

For each R1CS matrix $V$, the universal setup will commit to three dense MLEs representing the $n$ non-zero entries $V_{i,j}$ in the matrix and their locations $i,j$.

Denote the set of $n$ non-zero entries in a matrix $V$ by: \begin{align} %N_V \bydef \left(i_k,j_k,V_{i_k,j_k}\right)_{k\in[n)} \end{align}

Then, we can define three MLEs $\row,\col,\val : \F^{\log{n}} \rightarrow \F$ that represent this set as: \begin{align} \label{eq:rows-cols-vals} \forall k\in[n), \begin{cases} \term{\row(\k)} &= i_k \wedge {}\\
\term{\col(\k)} &= j_k \wedge {}\\
\term{\val(\k)} &= A_{i_k,j_k} \end{cases} %\row(\X) \bydef \sum_{\b\in\binS} \end{align} (These can be interpolated as usual.)

Now assume a function that converts a row or column index $i\in[m)$ (or $j\in[m)$) to its $s$-bit binary representation:

As a result, we can rewrite the R1CS matrix sumcheck from Eq. \ref{eq:r1cs-matrix-sumcheck} as: \begin{align} \label{eq:r1cs-sparse-sumcheck} \tilde{V}(\r_x,\r_y) &= \sum_{\i,\j\in\binS} V_{i,j}\cdot\eq_i(\r_x)\cdot\eq_j(\r_y)\\
&= \sum_{\i,\j\in\binS} V_{i,j}\cdot\eq_{\r_x}(\i)\cdot\eq_{\r_y}(\j)\\
&= \sum_{V_{i,j}\ne 0} V_{i,j}\cdot\eq_{\r_x}(\i)\cdot\eq_{\r_y}(\j)\\
\label{eq:r1cs-dense-sumcheck} &= \sum_{k\in[n)} \val(\k)\cdot\eq_{\r_x}(\bits(\row(\k)))\cdot\eq_{\r_y}(\bits(\col(\k)))\\
%&\bydef \sum_{k\in[n)} \val(\k)\cdot\eqr{V}(\k,\r_x)\eqc{V}(\k,\r_y)\\
\end{align}

Unfortunately, the term inside the sum above from Eq. \ref{eq:r1cs-dense-sumcheck} is not a polynomial. This is because $\bits$’s domain is $[m)$ and we cannot evaluate it on arbitrary field elements in $\F$.

My understanding so far is that Spark is an efficient protocol for “linearizing” the $\eq_{\r_x}(\bits(\row(\r_k)))$ expression into an MLE that agrees with it over hypercube (and its $\col$ counterpart).

So far, we are re-stating Spark.

What we do differently: for the row indices, we will have one MLE per each bit of a row index. We will have the same for the column indices. In total, there will now be $2s+1$ MLEs produced by the universal setup: \begin{align} \label{eq:bit-rows-cols-vals} \forall k\in[n), \begin{cases} \term{\row_{t}(\k)} &= \term{\bit_t(i_k)}, \forall t \in [s) \wedge {}\\
\term{\col_{t}(\k)} &= \bit_t(j_k) , \forall t \in [s) \wedge {}\\
\val(\k) &= A_{i_k,j_k} \end{cases} \end{align} where $\term{\bit_t(b)}$ denotes the $t$th bit in $b$’s binary expansion: \begin{align} \row(\k) =\sum_{t\in[s)} 2^t \cdot \row_{t}(\k) \end{align} (i.e., the $t$th element in $\bits(b)$).

Now, we can rewrite the sumcheck from Eq. \ref{eq:r1cs-dense-sumcheck} as: \begin{align} \tilde{V}(\r_x,\r_y) &= \sum_{k\in[n)} \val(\k)\cdot\eq_{\r_x}(\bits(\row(\k)))\cdot\eq_{\r_y}(\bits(\col(\k)))\\
\label{eq:E} &= \sum_{k\in[n)} \val(\k)\cdot \underbrace{ \eq_{\r_x}(\row_{0}(\k),\ldots,\row_{s-1}(\k)) }_{\term{E_x(\k)}} \cdot \underbrace{\eq_{\r_y}(\col_{0}(\k),\ldots,\col_{s-1}(\k))}_{\term{E_y(\k)}}\\
\label{eq:dense-sum} &\bydef \sum_{k\in[n)} \val(\k) \cdot E_x(\k) \cdot E_y(\k) \end{align}

As a result, at the end of the sumcheck, the verifier has the random point $\r_k\randget\F^{\log{n}}$ and evaluation claims $\val(\r_k),E_x(\r_k)$ and $E_y(\r_k)$.

Then, the verifier can be given a batched evaluation proof for $\left((\row_{t}(\r_k),\col_t(\r_k))_{t\in[s)}, \val(\r_k)\right)$. The $\row_t(\r_k)$ and $\col_t(\r_k)$ evaluations can be used to reconstruct the $E_x(\r_k)$ and $E_y(\r_k)$ evaluations, as per Eq. \ref{eq:E}.

Therefore, the verifier will have everything it needs to validate the $\tilde{V}(\r_x,\r_y)$ evaluation.

There are a few challenges:

1. The sumcheck will be over a degree-$\log{m}$ multivariate polynomial of $\log{n}$ variables (see below)
   • The sumcheck proof will be $\log{n}\log{m}$-sized $\Rightarrow$ we need to compress it!
2. While we can batch the evaluation proof for $\left((\row_{t}(\r_k),\col_t(\r_k))_{t\in[s)}, \val(\r_k)\right)$, we still need to include the actual $2s + 1$ evaluations to allow the verifier to check the sumcheck?

Inefficiencies

Consider the $E_x(\Z)$ polynomial defined above (and, similarly, $E_y(\Z)$): \begin{align} E_x(\Z)\bydef E_x(Z_0,\ldots,Z_{\log{n}-1}) \bydef \eq_{\r_x}(\row_{0}(\Z),\ldots,\row_{s-1}(\Z)) \end{align} Note that it will have $\log{n}$ variables, with degree $\log{m}\bydef s$ in each variable.

This will result in an $O(s n)=O(n\log{m})$-time sumcheck proving time. And, if done naively, in an $O(s\log{n})=O(\log{n}\log{m})$ communication and verifier time?

It may also be tricky to implement this sumcheck efficiently because of the degree-$\log{m}$ $E_x(\Z)$ polynomials.

The other problem will be that computing the batched evaluation proof will involve combining together $2s+1$ MLEs of size $n$ each $\rightarrow O(n \log{m})$ work.

So, asymptotically, this will not perform as well as Spartan with Spark.

The key question is: how well will this perform for sufficiently-large-but-not-too-large circuits (e.g., $n \le 2^{23}$ R1CS non-zero entries)

Cinder algorithms

$\mathsf{Cinder}_{\mathcal{D}}.\mathsf{Setup}(n, m) \Rightarrow (\mathsf{ck},\mathsf{ok})$

• $(\ck_\dense, \ok_\dense) \gets \dense.\setup(n)$
• $s\gets \log{m}$
• $\term{\ck}\gets (\ck_\dense, s, n)$
• $\term{\ok}\gets (\ok_\dense, s, n)$

$\mathsf{Cinder}_{\mathcal{D}}.\mathsf{Commit}(\mathsf{ck}, \tilde{V}) \Rightarrow (c, \aux)$

Commit to the row, column and value MLEs, as defined in Eq. \ref{eq:bit-rows-cols-vals}.

• $(\ck_\dense, s, \cdot)\parse \ck$
• $c_{\row,t} \gets \dense.\commit(\ck_\dense,\row_t),\forall t\in[s)$
• $c_{\col,t} \gets \dense.\commit(\ck_\dense,\col_t),\forall t\in [s)$
• $c_\val \gets \dense.\commit(\ck_\dense,\val)$
• $\term{c}\gets ((c_{\row,t},c_{\col,t})_{t\in[s)},c_\val)$
• $\term{\aux}\gets \left((\row_t(\Z),\col_t(\Z))_{t\in[s)}, \val(\Z)\right)$

$\mathsf{Cinder}_{\mathcal{D}}.\mathsf{Open}^{\mathcal{FS}(\cdot)}(\mathsf{ck}, \mathsf{aux}, c, \tilde{V}, (\r_x, \r_y)) \Rightarrow (v, \pi)$

As per Eq. \ref{eq:E}, let:

• $E_x(\Z)\bydef \eq_{\r_x}(\row_{0}(\Z),\ldots,\row_{s-1}(\Z))$
• $E_y(\Z)\bydef \eq_{\r_y}(\col_{0}(\Z),\ldots,\col_{s-1}(\Z))$

Do the sumcheck:

• add $c$ to the $\FS$ transcript
• $(\cdot, s, n)\parse \ck$
• $\term{v}\gets\tilde{V}(\r_x,\r_y)$
• $(e_\Sigma, \pi_\Sigma; \r_k) \gets \SC.\prove^\FSo(\val \cdot E_x \cdot E_y, v, \log{n}, s)$

Open the dense polynomials at the sumcheck challenge point:

• $(\ck_\dense, \cdot, \cdot)\parse \ck$
• $((\rho_t, \gamma_t)_{t\in [s)}) \fsget \F^{2s}$
• $P(\Z) \gets \val(\Z) + \sum_{t\in[s)} \rho_t \cdot \row_t(\Z) + \gamma_t \cdot \col_t(\Z)$
• $c_P \gets c_\val + \sum_{t\in[s)} \rho_t \cdot c_{\row,t} + \gamma_t \cdot c_{\col,t}$
  • Note: Assuming homomorphic dense MLE PCS commitments
• $(\cdot, \pi_P) \gets \dense.\open^\FSo(\ck_\dense, c_P, P, \r_k)$

Let:

• $v_\val \gets \val(\r_k)$
• $v_{\row,t}\gets \row_t(\r_k),\forall t\in[s)$
• $v_{\col,t}\gets \col_t(\r_k),\forall t\in[s)$
  • (Recall that the sumcheck challenge evaluation is for $e_\Sigma\equals\val(\r_k)\cdot E_x(\r_k) \cdot E_y(\r_k)$

The proof will be:

• $\term{\pi} \gets \left(\left((v_{\row,t},v_{\col,t})_{t\in[s)},v_\val\right), \pi_P,e_\Sigma,\pi_\Sigma\right)$

Proof size

• sumcheck evaluation claim $e_\sum$
  • 32 bytes
• sumcheck proof $\pi_\sum$ for $e_\sum$
  • e.g., without compression, for $n=2^{23},m = 2^{20}$, $\left((\log{m}+1)\log{n} + 1\right)\times \F = (21\times 23 + 1)\times 32 = 484 \times 32 =$ 15,488 bytes $=$ 15.125 KiB
• dense MLE PCS opening proof $\pi_P$
• row, column and value polynomial evaluations
  • e.g., for $s=20$, $(2\cdot 20 + 1)\times \F = 1312$ bytes

$\mathsf{Cinder}_{\mathcal{D}}.\mathsf{Verify}^{\mathcal{FS}(\cdot)}(\mathsf{ok}, c, v, (\r_x, \r_y); \pi) \Rightarrow \{0,1\}$

Verify sumcheck proof, reducing the claim that $v$ is the sum from Eq. \ref{eq:dense-sum} (i.e., $v = \tilde{V}(\r_x,\r_y)$) to a claim that $e_\Sigma\equals\val(\r_k) \cdot E_x(\r_k)\cdot E_y(\r_k)$:

• $(\cdot, s, \cdot)\parse \ok$
• add $c$ to the $\FS$ transcript
• $\left(\cdot, \cdot,e_\Sigma,\pi_\Sigma\right)\parse \pi$
• $(b; \r_k) \gets \SC.\verify^\FSo(v, e_\Sigma, s; \pi_\Sigma)$
• assert $b\equals 1$

Reduce checking the $e_\Sigma$ evaluation claim to verifying dense MLE PCS openings:

• $\left(\left((v_{\row,t},v_{\col,t})_{t\in[s)},v_\val\right), \cdot,\cdot,\cdot\right)\parse \pi$
• assert $e_\Sigma\equals v_\val \cdot \eq_{\r_x}(v_{\row,0},\ldots,v_{\row,s-1}) \cdot \eq_{\r_y}(v_{\col,0},\ldots,v_{\col,s-1})$
  • (i.e., check that $e_\Sigma\equals\val(\r_k)\cdot E_x(\r_k) \cdot E_y(\r_k)$

Verify said dense MLE openings:

• $((c_{\row,t},c_{\col,t})_{t\in[s)},c_\val)\parse c$
• $((\rho_t, \gamma_t)_{t\in [s)}) \fsget \F^{2s}$
• $c_P \gets c_\val + \sum_{t\in[s)} \rho_t \cdot c_{\row,t} + \gamma_t \cdot c_{\col,t}$
  • Note: Assuming homomorphic dense MLE PCS commitments
• $v_P \gets v_\val + \sum_{t\in[s)} \rho_t \cdot v_{\row,t} + \gamma_t \cdot v_{\col,t}$
• $(\ok_\dense,\cdot,\cdot)\parse\ok$
• $\left(\cdot, \pi_P,\cdot,\cdot\right)\parse \pi$
• assert $\dense.\verify^\FSo(\ok_\dense, c_P, v_P, \r_k;\pi_P)$

Succeed:

• return 1

Verifier time

1. Verify a sumcheck over a degree-$\log{m}$ polynomial with $\log{n}$ variables.
2. Verify $e_\sum$ given row, column and val. poly. evaluations (involves evaluating $\eq_{\r_x},\eq_{\r_y}$ polynomials over $\log{m}$ variables.)
3. Fiat-Shamir hashing for the $\rho_t,\gamma_t$ linear combination
4. Derive dense MLE PCS commitment for random linear combination poylnomial $P(\Z)$
   • e.g., $(2\log{m})$-sized $\Gr_1$ MSM assuming PST commitments
5. Derive random linear combination for $P(\r_k)$
   • i.e., $2\log{m} \times \F$ multiplications
6. Verify dense MLE PCS opening on $P(\Z)$

Acknowledgements

Thanks to Weijie Wang for explaining Spark¹. We arrived at Cinder by simply asking: “What’s the simplest thing we could do instead? (Without sparks!)” Thanks to Albert Garretta for listening to an explanation of Cinder and helping us reason through it. Thanks to Ron Rothblum and Justin Thaler for their feedback on the write-up.

References

For cited works, see below 👇👇