Jagged PCS

Code: slop: crates/jagged/src/verifier.rs

The result of the zerocheck protocol is a point and claims on $p_1(z), \cdots, p_n(z)$ for all chips we want to prove. Note that $z$ is of size max_log_row_count, and $p_i$ are padded with zeroes beyond the "real" chip heights. We aggregate these claims into a single claim about the polynomial $P$ which is the sparse representation of the computation trace (i.e., the concatenation of all of the padded tables).

Now we want to connect this to the "main trace", i.e. the commitment of buffer of "real" data. This is the part that the Jagged Polynomial Commitment comes into play. We sample at random $z_{\text{col}}$ to combine these claims via the multilinear extension. and $Q$ as the dense representation (to which the prover committed), we need to prove that

$$P(z_{\text{row}}, z_{\text{col}}) = \sum_{i} Q(i) \cdot \text{eq}(z_{\text{row}}, \text{row}(i)) \cdot \text{eq}(z_{\text{col}}, \text{col}(i))$$

which is true since both are multilinear and equation holds over the boolean hypercube.

Consider the table heights $h_1, \cdots h_n$ and $t_i = \sum_{j=1}^{i-1} h_j$ be the prefix sum.

Denote $f(i)$ to be the multilinear extension of $\text{eq}(z_{\text{row}}, \text{row}(i)) \cdot \text{eq}(z_{\text{col}}, \text{col}(i))$. Then, what we have is essentially a sumcheck claim of $Q(i) \cdot f(i)$. Running the sumcheck procedure basically reduces to the verifier checking the evaluation claim of $Q$ and an evaluation claim of $f$. The former will be done using a PCS of $Q$, the dense representation. The latter is the harder part, and the verifier will compute this on their own.

First, note that

$$f(i) = \sum_{c \in [1, n]} \text{eq}(z_{\text{col}}, c) \cdot \hat{g}(z_{\text{row}}, i, t_c, t_{c+1})$$

where $\hat{g}$ is the multilinear extension of

$$g(a, b, c, d) = \begin{cases} 1 & a = b - c \text{ and } b \in [c, d) \\ 0 & \text{otherwise} \end{cases}$$

which can be seen by the fact that both sides are multilinear in $i$, and are equal over the hypercube. Therefore, computing $f$ is equivalent to computing $\hat{g}$ in $n$ points.

The Jagged Assist

Code: slop: crates/jagged/src/jagged_eval/sumcheck_eval.rs::jagged_evaluation

To make recursion costs better, the prover helps out. Basically, the prover will send the evaluation of $\hat{g}$ in $n$ points, and prove that the evaluations are correct. The verifier will just need to evaluate $\hat{g}$ once. Consider that the prover wants to show $h(x_i) = y_i$ for $1 \le i \le k$, where $h$ is multilinear. The verifier first selects $r$ randomly via Fiat-Shamir, then we show

$$\sum_{i} r^i \cdot h(x_i) = \sum_{i} r^i \cdot y_i$$

The RHS can be computed by the verifier directly. The LHS is

$$\sum_{i} r^i \cdot \sum_{b} \text{eq}(x_i, b) \cdot h(b) = \sum_{b} h(b) \sum_{i} \left( r^i \cdot \text{eq}(x_i, b) \right)$$

Now, if one runs a sumcheck protocol here over $b$, then the verifier needs to get

$$h(v) \cdot \sum_{i} \left( r^i \cdot \text{eq}(x_i, v) \right)$$

which means that the verifier can just compute a single $h(v)$ alongside with some $eq$.

Utilizing this, we can do

$$f(i) = \sum_{c \in [1, n]} \text{eq}(z_{\text{col}}, c) \cdot \hat{g}(z_{\text{row}}, i, t_c, t_{c+1})$$ $$= \sum_{c \in [1, n]}\text{eq}(z_{\text{col}}, c) \cdot \left( \sum_{u, v} \hat{g}(z_{\text{row}}, i, u, v) \cdot \text{eq}(u || v, t_c || t_{c+1}) \right)$$ $$= \sum_{u,v} \hat{g}(z_{\text{row}}, i, u, v) \cdot \left( \sum_{c \in [1, n]} \text{eq}(z_{\text{col}}, c) \cdot \text{eq}(u || v, t_c || t_{c+1}) \right)$$

and now with a sumcheck over $u, v$, we need one evaluation of $\hat{g}(z_{\text{row}}, i, u', v')$ as well as

$$\sum_{c \in [1, n]} \text{eq}(z_{\text{col}}, c) \cdot \text{eq}(u' || v', t_c || t_{c+1})$$

The Jagged Evaluation

Code: slop: crates/jagged/src/poly.rs, BranchingProgram::eval

This means the remaining task at hand for the verifier is to compute $\hat{g}$ at a single point.

Note that $z_{\text{row}}$ and the evaluation point for $f$, denoted $z_{\text{trace}}$ is fixed, so we can just define

$$h(u, v) = \hat{g}(z_{\text{row}}, z_{\text{trace}}, u, v)$$

and work with evaluation of a single $h$. We show how to compute $h$ based on a dynamic programming approach.

Since $\hat{g}$ is multilinear, one can write

$$h(u, v) = \sum_{a, b, c, d} \text{eq}(a, z_{\text{row}}) \cdot \text{eq}(b, z_{\text{trace}}) \cdot \text{eq}(c, u) \cdot \text{eq}(d, v) \cdot g(a, b, c, d)$$

If we can define some state over $a, b, c, d$ and its transition based on its bits one by one, we can compute this via dynamic programming. For example, consider that we can define some state $S_i$ over $a, b, c, d$'s first $i$ bits, and can transition it to $S_{i+1}$ based on their $i+1$th bit. Then, we can compute something like

$$H(S_{i, st}, u, v) = \sum_{a, b, c, d \in \{0, 1\}^i} \text{eq}(a, z_{\text{row}}) \cdot \text{eq}(b, z_{\text{trace}}) \cdot \text{eq}(c, u) \cdot \text{eq}(d, v) \cdot [(a, b, c, d) \in st]$$

where $\text{eq}$ polynomial just uses the first $i$ values. In this case, we can say

$$H(S_{i+1, st'}, u, v) = \sum_{st \rightarrow st' \text{ via } a', b', c', d'} H(S_{i, st}, u, v) \cdot \text{tr}(a', b', c', d')$$

where the transition coefficient is simply

$$\text{tr}(a',b',c',d') = \text{eq}(a' || b' || c' || d', z_{\text{row}}[i+1] || z_{\text{trace}}[i+1] || u[i+1] || v[i+1])$$

so now it just reduces to whether or not the state $a = b - c$, $b \in [c, d)$ can be represented in a such form. Basically we need to know $b = a + c$, and $b < d$ at the same time. Therefore, we keep the two boolean as states, while we traverse from LSB to MSB.

• the carry when adding $a + c$
• whether or not $b < d$ so far

as well as if the state is already failed, (i.e. $b = a + c$ is not true already). It is clear that this state can be managed by incrementing the four bits each step, as desired.