Bytecode

At each cycle of the RISC-V virtual machine, the current instruction (as indicated by the program counter) is "fetched" from the bytecode and decoded. In Jolt, this is proven by treating the bytecode as a lookup table, and fetches as lookups. To prove the correctness of these lookups, we use the Shout lookup argument.

One distinguishing feature of the bytecode Shout instance is that we have multiple instances of the read-checking and $\widetilde{\text{raf}}$-evaluation sumchecks. Intuitively, the bytecode serves as the "ground truth" of what's being executed, so one would expect many virtual polynomial claims to eventually lead back to the bytecode. And this holds in practice –– in the Jolt sumcheck DAG diagram, we see that there are three colors of edges (corresponding to stages 1, 2, and 3,) pointing to the bytecode read-checking node, and two colors of edges (corresponding to stages 1 and 3) pointing to the bytecode $\widetilde{\text{raf}}$-evaluation node.

Each stage has its a unique opening point, so having in-edges of different colors implies that multiple instances of that sumcheck must be run in parallel to prove the different claims.

Read-checking

Another distinguishing feature of the bytecode Shout instance is that we treat each entry of lookup table as containing a tuple of values, rather than a single value. Intuitively, this is because each instruction in the bytecode encodes multiple pieces of information: opcode, operands, etc.

The figure below loosely depicts the relationship between bytecode and $\widetilde{\text{Val}}$ polynomial.

We start from some ELF file, compiled from the guest program. For each instruction in the ELF (raw bytes), we decode/preprocess the instruction into a structured format containing the individual witness values used in Jolt:

• The instruction operands rs1, rs2, rd, imm
• Circuit and lookup table flags
• The instruction address

Then, we compute a Reed-Solomon fingerprint of some subset of the values in the tuple, depending on what $\widetilde{\text{rv}}$ claims are being proven. These fingerprints serve as the coefficients of the $\widetilde{\text{Val}}$ polynomial for that read-checking instance.

The figure above depicts the $\widetilde{\text{Val}}$ polynomial we would use to prove the read-checking instance for the Stage 2 claims, labeled as "ra/wa claims" in the DAG diagram. As explained below, the $\widetilde{\text{ra}}$ and $\widetilde{\text{wa}}$ polynomials correspond to the registers (rs1, rs2, rd) in the bytecode. Each coefficient in $\widetilde{\text{Val}}$ is $\text{rd}+\gamma \cdot \text{rs1}+{\gamma }^2\cdot \text{rs2}$, for the registers of one particular instruction.

We can write the read-checking sumcheck expression for the Stage 2 claims as the following:

$${\widetilde{\text{rv}}}_{\text{rd}}(r)+\gamma \cdot {\widetilde{\text{rv}}}_{\text{rs1}}(r)+{\gamma }^2\cdot {\widetilde{\text{rv}}}_{\text{rs2}}(r)=\sum _{k,j}\widetilde{\text{eq}}(r,j)\cdot \widetilde{\text{ra}}(k,j)\cdot \left({\widetilde{\text{Val}}}_{\text{rd}}(k)+\gamma \cdot {\widetilde{\text{Val}}}_{\text{rs1}}(k)+{\gamma }^2\cdot {\widetilde{\text{Val}}}_{\text{rs2}}(k)\right)$$

where we treat

$$\widetilde{\text{Val}}(k)={\widetilde{\text{Val}}}_{\text{rd}}(k)+\gamma \cdot {\widetilde{\text{Val}}}_{\text{rs1}}(k)+{\gamma }^2\cdot {\widetilde{\text{Val}}}_{\text{rs2}}(k)$$

as a single multilinear polynomial.

Observe that this sumcheck satisfies our needs for the Stage 2 claims: ${\widetilde{\text{rv}}}_{\text{rd}}(r)$, ${\widetilde{\text{rv}}}_{\text{rs1}}(r)$, ${\widetilde{\text{rv}}}_{\text{rs2}}(r)$ are the claims output by the registers read/write-checking sumcheck, and we can simply compute Reed-Solomon fingerprint of these claims to obtain the left-hand side (i.e. input claim) of sumcheck expression above.

Registers

Technically, the explanation above glosses over some details for the sake of exposition. To be precise, the claims output by registers read/write-checking are actually:

$$\begin{gathered} {\widetilde{\text{wa}}}_{\text{rd}}(r_{\text{address}},r_{\text{cycle}}) \\ {\widetilde{\text{ra}}}_{\text{rs1}}(r_{\text{address}},r_{\text{cycle}}) \\ {\widetilde{\text{ra}}}_{\text{rs2}}(r_{\text{address}},r_{\text{cycle}}) \end{gathered}$$

where $r_{\text{address}}\in {\mathbb{F}}^{\log (\text{\# registers})}$.

So we define:

$$\widetilde{\text{Val}}(k)=\widetilde{\text{rd}}(k,r_{\text{address}})+\gamma \cdot \widetilde{\text{rs1}}(k,r_{\text{address}})+{\gamma }^2\cdot \widetilde{\text{rs2}}(k,r_{\text{address}})$$

where $\forall k\in \{0,1{\}}^{\log (\text{bytecode size})},k^{\prime }\in \{0,1{\}}^{\log (\text{\# registers})}$:

• $\widetilde{\text{rd}}(k,k^{\prime })=1$ if the $k$-th instruction in the bytecode has $rd=k^{\prime }$
• $\widetilde{\text{rd}}(k,k^{\prime })=0$ otherwise

and similarly for $\widetilde{\text{rs1}}$ and $\widetilde{\text{rs2}}$.

Equivalently,

$$\widetilde{\text{Val}}(k)=\widetilde{\text{eq}}(\text{rd}[k],r_{\text{address}})+\gamma \cdot \widetilde{\text{eq}}(\text{rs1}[k],r_{\text{address}})+{\gamma }^2\cdot \widetilde{\text{eq}}(\text{rs2}[k],r_{\text{address}})$$

where $\text{rd}[k]$ (respectively, $\text{rs1}[k]$ and $\text{rs2}[k]$) is the bitvector denoting the rd (respectively, rs1 and rs2) for the $k$-th instruction in the bytecode.

Instruction address

Each instruction in the bytecode has two associated "addresses":

• its index in the expanded bytecode. "Expanded" bytecode refers to the preprocessed bytecode, after instructions are expanded to their virtual sequences
• its memory address as given by ELF. All the instructions in a virtual sequence are assigned the address of the "real" instruction they were expanded from.

The former is used for the $\widetilde{\text{raf}}$-evaluation sumcheck, described below. The latter is used to enforce program counter updates in the [R1CS constraints] (./r1cs_constraints.md), and is treated as a part of the tuple of values in the preprocessed bytecode.

The "outer" and shift sumchecks in Spartan output claims about the virtual UnexpandedPC polynomial, which corresponds to the latter. These claims are proven using bytecode read-checking.

Flags

There are two types of Boolean flags used in Jolt:

• Circuit flags, used in R1CS constraints
• Lookup table flags, used in the instruction execution Shout

The associated flags for a given instruction in the bytecode can be computed a priori (i.e. in preprocessing), so any claims about these flags arising output by Spartan or instruction execution Shout are also proven using bytecode read-checking.

raf-evaluation

There are two $\widetilde{\text{raf}}$-evaluation instances for bytecode, corresponding to $\widetilde{\text{raf}}$ claims arising from stages 1 and 3.

The $\widetilde{\text{raf}}$ polynomial, in the context of bytecode, is the program counter (PC). The two sumchecks that output claims about the PC are the "outer" and "shift" sumchecks used to prove Jolt's R1CS constraints.

One-hot checks

Jolt enforces that the ${\widetilde{\text{ra}}}_i$ polynomials used for bytecode Shout 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.