Instruction execution

One distinguishing feature of Jolt among zkVM architectures is how it handles instruction execution, i.e. proving the correct input/output behavior of every RISC-V instruction in the trace. This is primarily achieved through the Shout lookup argument.

Large Lookup Tables and Prefix-Suffix Sumcheck

The Shout instance for instruction execution must query a massive lookup table -- effectively of size $2^{64}$, since the lookup query is constructed from two 32-bit operands. This $K>>T$ parameter regime is discussed in the Twist and Shout paper (Section 7), which proposes the use of sparse-dense sumcheck. However, upon implementation it became clear that sparse-dense sumcheck did not generalize well to the full RISC-V instruction set.

Instead, Jolt introduces a new algorithm: prefix-suffix sumcheck, described in the appendix of Proving CPU Executions in Small Space. Like the sparse-dense algorithm, it requires some structure in the lookup table:

• The lookup table must have an MLE that is efficiently evaluable by the verifier. The JoltLookupTable trait encapsulates this MLE.
• The lookup index can be split into a prefix and suffix, such that MLEs can be evaluated independently on the two parts and then recombined to obtain the desired lookup entry.
• Every prefix/suffix MLE is efficiently evaluable (constant time) on Boolean inputs

The prefix-suffix sumcheck algorithm can be conceptualized as a careful application of the distributive law to reduce the number of multiplications required for a sumcheck that would otherwise be intractably large.

To unpack this, consider the read-checking sumcheck for Shout, as presented in the paper.

$$\widetilde{\text{rv}}(r_{\text{cycle}})=\sum _{k=(k_1,\dots ,k_d)\in {\left(\{0,1{\}}^{\log (K)/d}\right)}^d,j\in \{0,1{\}}^{\log (T)}}\widetilde{\text{eq}}(r_{\text{cycle}},j)\cdot \left(\prod _{i=1}^d{\widetilde{\text{ra}}}_i(k_i,j)\right)\cdot \widetilde{\text{Val}}(k)$$

Naively, this would require $\Theta (dKT)$ multiplications, which is far too large given $d=8$ and $K=2^{64}$. But suppose $\widetilde{\text{Val}}$ has prefix-suffix structure. The key intuition of prefix-suffix structure is captured by the following equation:

$$\widetilde{\text{Val}}(k_{\text{prefix}},k_{\text{suffix}})=\sum _{(\text{prefix},\text{suffix})\in \text{decompose}(\text{Val})}\widetilde{\text{prefix}}(k_{\text{prefix}})\cdot \widetilde{\text{suffix}}(k_{\text{suffix}})$$

You can think of $k_{\text{prefix}}$ and $k_{\text{suffix}}$ as the high-order and low-order "bits" of $k$, respectively, obtained by splitting $k$ at some partition index. The PrefixSuffixDecomposition trait specifies which prefix/suffix MLEs to evaluate and how to combine them.

We will split $k$ four times at four different indices, and these will induce the four phases of the prefix-suffix sumcheck. Each of the four phases encompasses 16 rounds of sumcheck (i.e. 16 of the address variables $k$), so together they comprise the first $\log K=64$ rounds of the read-checking sumcheck.

Given our prefix-suffix decomposition of $\widetilde{\text{Val}}$, we can rewrite our read-checking sumcheck as follows:

$$\widetilde{\text{rv}}(r_{\text{cycle}})=\sum _{k_{\text{prefix}}\in \{0,1{\}}^{16},k_{\text{suffix}}\in \{0,1{\}}^{48},j\in \{0,1{\}}^{\log (T)}}\widetilde{\text{eq}}(r_{\text{cycle}},j)\cdot \widetilde{\text{ra}}(k_{\text{prefix}},k_{\text{suffix}},j)\cdot \sum _{(\text{prefix},\text{suffix})}\widetilde{\text{prefix}}(k_{\text{prefix}})\cdot \widetilde{\text{suffix}}(k_{\text{suffix}})$$

Note that we have replaced ${\prod }_{i=1}^d{\widetilde{\text{ra}}}_i(k_i,j)$ with just $\widetilde{\text{ra}}$. Since ${\prod }_{i=1}^d{\widetilde{\text{ra}}}_i(k_i,j)$ is degree 1 in each $k$ variable, we will treat it as a single multilinear polynomial while we're binding those variables (the first $\log K$ rounds). The equation as written above depicts the first phase, where $k_{\text{prefix}}$ is the first 16 variables of $k$, and $k_{\text{suffix}}$ is the last 48 variables of $k$.

Rearranging the terms in the sum, we have:

$$\widetilde{\text{rv}}(r_{\text{cycle}})=\sum _{k_{\text{prefix}}\in \{0,1{\}}^{16}}\sum _{(\text{prefix},\text{suffix})}\widetilde{\text{prefix}}(k_{\text{prefix}})\cdot \left(\sum _{k_{\text{suffix}}\in \{0,1{\}}^{48},j\in \{0,1{\}}^{\log T}}\widetilde{\text{ra}}(k_{\text{prefix}},k_{\text{suffix}},j)\cdot \widetilde{\text{eq}}(r_{\text{cycle}},j)\cdot \widetilde{\text{suffix}}(k_{\text{suffix}})\right)$$

Note that the summand is degree 2 in $k_{\text{prefix}}$, the variables being bound in the first phase:

1. $k_{\text{prefix}}$ appears in $\widetilde{\text{prefix}}(k_{\text{prefix}})$
2. $k_{\text{prefix}}$ also appears in appears in the paranthesized expression in $\widetilde{\text{ra}}(k_{\text{prefix}},k_{\text{suffix}},j)$

Written in this way, it becomes clear that we can treat the first 16 rounds as a mini-sumcheck over just the 16 $k_{\text{prefix}}$ variables, and with just multilinear terms. If we can efficiently compute the $2^{16}$ coefficients of each mulitlinear term, the rest of this mini-sumcheck is efficient. Each evaluation of $\widetilde{\text{prefix}}(k_{\text{prefix}})$ can be computed in constant time, so that leaves the parenthesized term:

$$\left(\sum _{k_{\text{suffix}}\in \{0,1{\}}^{48},j\in \{0,1{\}}^{\log T}}\widetilde{\text{ra}}(k_{\text{prefix}},k_{\text{suffix}},j)\cdot \widetilde{\text{eq}}(r_{\text{cycle}},j)\cdot \widetilde{\text{suffix}}(k_{\text{suffix}})\right)$$

This can be computed in $\Theta (T)$: since $\widetilde{\text{ra}}$ is one-hot, we can do a single iteration over $j\in \{0,1{\}}^{\log T}$ and only compute the terms of the sum where $\widetilde{\text{ra}}(k_{\text{prefix}},k_{\text{suffix}},j)=1$. We compute a table of $\widetilde{\text{eq}}(r_{\text{cycle}},j)$ evaluation a priori, and $\widetilde{\text{suffix}}(k_{\text{suffix}})$ can be evaluated in constant time on Boolean inputs.

After the first phase, the high-order 16 variables of $k$ will have been bound. We will need to use a new sumcheck expression for the next phase:

$$\widetilde{\text{rv}}(r_{\text{cycle}})=\sum _{k_{\text{prefix}}\in \{0,1{\}}^{16}}\sum _{(\text{prefix},\text{suffix})}\widetilde{\text{prefix}}(r^{(1)},k_{\text{prefix}})\cdot \left(\sum _{k_{\text{suffix}}\in \{0,1{\}}^{32},j\in \{0,1{\}}^{\log T}}\widetilde{\text{ra}}(r^{(1)},k_{\text{prefix}},k_{\text{suffix}},j)\cdot \widetilde{\text{eq}}(r_{\text{cycle}},j)\cdot \widetilde{\text{suffix}}(k_{\text{suffix}})\right)$$

Now $r^{(1)}\in {\mathbb{F}}^{16}$ are random values that the first 16 variables were bound to, and $k_{\text{prefix}}$ are the next 16 variables of $k$. Meanwhile, $k_{\text{suffix}}$ now represents the last 32 variables of $k$.

This complicates things slightly, but the algorithm follows the same blueprint as in phase 1. This is a sumcheck over the 16 $k_{\text{prefix}}$ variables, and there are two multilinear terms. We can still compute each evaluation of $\widetilde{\text{prefix}}(r^{(1)},k_{\text{prefix}})$ in constant time, and we can still compute the parenthesized term in $\Theta (T)$ time (observe that there is exactly one non-zero coefficient of $\widetilde{\text{ra}}(r^{(1)},k_{\text{prefix}},k_{\text{suffix}},j)$ per cycle $j$).

After the first $\log K$ rounds of sumcheck, we are left with:

$$\sum _{j\in \{0,1{\}}^{\log (T)}}\widetilde{\text{eq}}(r_{\text{cycle}},j)\cdot \widetilde{\text{ra}}(r_{\text{address}},j)\cdot \widetilde{\text{Val}}(r_{\text{address}})$$

which we prove using the standard linear-time sumcheck algorithm. Note that $\widetilde{\text{ra}}(r_{\text{address}},j)$ here is a virtual polynomial.

Prefix and Suffix Implementations

Jolt modularizes prefix/suffix decomposition using two traits:

• SparseDensePrefix (under prefixes/)
• SparseDenseSuffix (under suffixes/)

Each prefix/suffix used in a lookup table implements these traits.

Multiplexing Between Instructions

An execution trace contains many different RISC-V instructions. Note that there is a many-to-one relationship between instructions and lookup tables -- multiple instructions may share a lookup table (e.g., XOR and XORI). To manage this, Jolt uses the InstructionLookupTable trait, whose lookup_table method returns an instruction's associated lookup table, if it has one (some instructions do not require a lookup).

Boolean lookup table flags indicate which table is active on a given cycle. At most one flag is set per cycle. These flags allow us to "multiplex" between all of the lookup tables:

$$\sum _{\ell }{\widetilde{\text{flag}}}_{\ell }(j)\cdot {\widetilde{\text{Val}}}_{\ell }(k)$$

where the sum is over all lookup tables $\ell$.

Only one table's flag $\textsf{flag}}_{\ell}(j)$ is 1 at any given cycle $j$, so only that table's ${\widetilde{\text{Val}}}_{\ell }(k)$ contributes to the sum.

This term becomes a drop-in replacement for $\widetilde{\text{Val}}$ as it appears in the Shout read-checking sumcheck:

$$\widetilde{\text{rv}}(r_{\text{cycle}})=\sum _{k=(k_1,\dots ,k_d)\in {\left(\{0,1{\}}^{\log (K)/d}\right)}^d,j\in \{0,1{\}}^{\log (T)}}\widetilde{\text{eq}}(r_{\text{cycle}},j)\cdot \left(\prod _{i=1}^d{\widetilde{\text{ra}}}_i(k_i,j)\right)\cdot \left(\sum _{\ell }{\widetilde{\text{flag}}}_{\ell }(j)\cdot {\widetilde{\text{Val}}}_{\ell }(k)\right)$$

Note that each ${\widetilde{\text{Val}}}_{\ell }$ here has prefix-suffix structure.

raf Evaluation

The $\widetilde{\text{raf}}$-evaluation sumcheck in Jolt deviates from the description in the Twist/Shout paper. This is mostly an artifact of the prefix-suffix sumcheck, which imposes some required structure on the lookup index (i.e. the "address" variables $k$).

Case 1: Interleaved operands

Consider, for example, the lookup table for XOR x y. Intuitively, the lookup index must be crafted from the bits of x and y. A first attempt might be to simply concatenate the bits of x and y, i.e.:

$$(k_1,k_2,\dots ,k_{64})=(x_1,x_2,\dots ,x_{32},y_1,y_2,\dots ,y_{32})$$

Unfortunately, there is no apparent way for this formulation to satisfy prefix-suffix structure. Instead we will interleave the bits of x and y, i.e.

$$(k_1,k_2,\dots ,k_{64})=(x_1,y_1,x_2,y_2,\dots ,x_{32},y_{32})$$

With this formulation, the prefix-suffix structure is easily apparent. Suppose the prefix-suffix split index is 16, so:

$$\begin{gathered} k_{\text{prefix}}=(x_1,y_1,x_2,y_2,\dots ,x_8,y_8) \\ {k}_{\text{suffix}}=(x_9,y_9,x_{10},y_{10},\dots ,x_{32},y_{32}) \end{gathered}$$

Then XOR x y has the following prefix-suffix decomposition:

$$\begin{gathered} {\widetilde{\text{Val}}}_{\text{XOR}}(k_{\text{prefix}},k_{\text{suffix}})={\widetilde{\text{prefix}}}_{\text{XOR}}(k_{\text{prefix}})+{\widetilde{\text{suffix}}}_{\text{XOR}}(k_{\text{suffix}}) \\ {\widetilde{\text{prefix}}}_{\text{XOR}}(k_{\text{prefix}})=2^{31}\cdot \left(x_1+y_1-2x_1{y}_1\right)+2^{31}\cdot \left(x_2+y_2-2x_2{y}_2\right)+\cdots +2^{24}\cdot \left(x_8+y_8-2x_8{y}_8\right) \\ {\widetilde{\text{suffix}}}_{\text{XOR}}(k_{\text{prefix}})=2^{23}\cdot \left(x_9+y_9-2x_9{y}_9\right)+2^{22}\cdot \left(x_{10}+y_{10}-2x_{10}{y}_{10}\right)+\cdots +2^0\cdot \left(x_{32}+y_{32}-2x_{32}{y}_{32}\right) \end{gathered}$$

By inspection, ${\widetilde{\text{prefix}}}_{\text{XOR}}(k_{\text{prefix}})$ effectively computes the 8-bit XOR of the high-order bits of x and y, while ${\widetilde{\text{suffix}}}_{\text{XOR}}$ computes the 24-bit XOR of the low-order bits of x and y. Then the full result XOR x y is obtained by concatenating (adding) the two results.

Now that we've confirmed that we have something with prefix-suffix structure, we can write down the $\widetilde{\text{raf}}$-evaluation sumcheck expression. Instead of a single $\widetilde{\text{raf}}$ polynomial, here we have two lookup operands x and y, which are called LeftLookupOperand and RightLookupOperand in code. These are the values that appear in Jolt's R1CS constraints. The point of the $\widetilde{\text{raf}}$-evaluation sumcheck is to relate these (non-one-hot) polynomials to their one-hot counterparts. In the context of instruction execution Shout, this means the $\widetilde{\text{ra}}$ polynomial.

Since we have two $\widetilde{\text{raf}}$-like polynomials, we have two sumcheck instances:

$$\begin{gathered} \widetilde{\text{LeftLookupOperand}}(r)=\sum _{k,j}\widetilde{\text{eq}}(r,j)\cdot \widetilde{\text{ra}}(k,j)\cdot \sum _{\ell =0}^{\log (K)/2-1}{2}^{\ell }\cdot k_{2\ell } \\ \widetilde{\text{RightLookupOperand}}(r)=\sum _{k,j}\widetilde{\text{eq}}(r,j)\cdot \widetilde{\text{ra}}(k,j)\cdot \sum _{\ell =0}^{\log (K)/2-1}{2}^{\ell }\cdot k_{2\ell +1} \end{gathered}$$

This captures the interleaving behavior we described above: LeftLookupOperand is the concatenation of the "odd bits" of $k$, while RightLookupOperand is the concatenation of the "even bits" of $k$.

Case 2: Single operand

Many RISC-V instructions are similar to XOR, in that interleaving the operand bits lends itself to prefix-suffix structure. However, there are some instructions where this is not the case. The execution of some arithmetic instructions, for example, are handled by computing the corresponding operation in the field, and applying a range-check lookup to the result to truncate potential overflow bits.

In this case, the lookup index corresponds to the (single) value y being range-checked, so we do not interleave its bits with another operand. Instead, we just have:

$$(k_1,k_2,\dots ,k_{64})=(0,0,\dots ,0,y_1{y}_2,\dots ,y_{32})$$

In this case, we have the following sumchecks:

$$\begin{gathered} \widetilde{\text{LeftLookupOperand}}(r)=0 \\ \widetilde{\text{RightLookupOperand}}(r)=\sum _{k,j}\widetilde{\text{eq}}(r,j)\cdot \widetilde{\text{ra}}(k,j)\cdot \sum _{\ell =0}^{\log (K)-1}{2}^{\ell }\cdot k_{\ell } \end{gathered}$$

LeftLookupOperand is 0 and RightLookupOperand will be the concatenation of all the bits of $k$.

In order to handle Cases 1 and 2 simultaneously, we can use the same "multiplexing" technique as in the read-checking sumcheck. We use a flag polynomial to indicate which case we're in:

$$\widetilde{\text{InterleaveOperands}}(j)=1-\widetilde{\text{AddOperands}}(j)-\widetilde{\text{SubtractOperands}}(j)-\widetilde{\text{MultiplyOperands}}(j)$$

where $\widetilde{\text{AddOperands}}$, $\widetilde{\text{SubtractOperands}}$, and $\widetilde{\text{MultiplyOperands}}$ are circuit flags.

Prefix-suffix structure

These sumchecks have similar structure to the read-checking sumcheck. A side-by-side comparison of the read-checking sumcheck with the sumchecks for Case 1:

$$\begin{gathered} \widetilde{\text{rv}}(r)=\sum _{k,j}\widetilde{\text{eq}}(r,j)\cdot \widetilde{\text{ra}}(k,j)\cdot \widetilde{\text{Val}}(k) \\ \widetilde{\text{LeftLookupOperand}}(r)=\sum _{k,j}\widetilde{\text{eq}}(r,j)\cdot \widetilde{\text{ra}}(k,j)\cdot \sum _{\ell =0}^{\log (K)/2-1}{2}^{\ell }\cdot k_{2\ell } \\ \widetilde{\text{RightLookupOperand}}(r)=\sum _{k,j}\widetilde{\text{eq}}(r,j)\cdot \widetilde{\text{ra}}(k,j)\cdot \sum _{\ell =0}^{\log (K)/2-1}{2}^{\ell }\cdot k_{2\ell +1} \end{gathered}$$

As it turns out, ${\sum }_{\ell =0}^{\log (K)/2-1}{2}^{\ell }\cdot k_{2\ell }$ and ${\sum }_{\ell =0}^{\log (K)/2-1}{2}^{\ell }\cdot k_{2\ell +1}$ have prefix-suffix structure, so we can also use the prefix-suffix algorithm for these sumchecks. Due to their similarities, we batch the read-checking and these $\widetilde{\text{raf}}$-evaluation sumchecks together in a bespoke fashion.

Other sumchecks

ra virtualization

The lookup tables used for instruction execution are of size $K=2^{64}$, so we set $d=8$ as our decomposition parameter such that $K^{1/d}=2^8$.

Similar to the RAM Twist instance, we opt to virtualize the $\widetilde{\text{ra}}$ polynomial. In other words, Jolt simply carries out the read checking and $\widetilde{\text{raf}}$ evaluation sumchecks as if $d=1$.

At the conclusion of these sumchecks, we are left with claims about the virtual $\widetilde{\text{ra}}$ polynomial. Since the polynomial is uncommitted, Jolt invokes a separate sumcheck that expresses an evaluation $\widetilde{\text{ra}}$ in terms of the constituent ${\widetilde{\text{ra}}}_i$ polynomials. The ${\widetilde{\text{ra}}}_i$ polynomials are, by definition, a tensor decomposition of $\widetilde{\text{ra}}$, so the "$\widetilde{\text{ra}}$ virtualization" sumcheck is the following:

$$\widetilde{\text{ra}}(r,r^{\prime })=\sum _{j\in \{0,1{\}}^{\log (T)}}\widetilde{\text{eq}}(r^{\prime },j)\cdot \left(\prod _{i=1}^d{\widetilde{\text{ra}}}_i(r_i,j)\right)$$

Since the degree of this sumcheck is $d+1=9$, using the standard linear-time sumcheck prover algorithm would make this sumcheck relatively slow. However, we employ optimizations specific to high-degree sumchecks, adapting techniques from the Karatsuba and Toom-Cook multiplication algorithms.

One-hot checks

Jolt enforces that the ${\widetilde{\text{ra}}}_i$ polynomials used for instruction execution are one-hot, using a Booleanity and Hamming weight sumcheck as described in the paper. These implementations follow the Twist and Shout paper closely, with no notable deviations.