Registers

Jolt proves the correctness of register updates using the Twist memory checking algorithm, specifically utilizing the "local" prover algorithm.

In this Twist instance, $K=64$ because we have 32 RISC-V registers and 32 virtual registers. This is small enough that we can use $d=1$.

Virtual register layout

The 32 virtual registers (registers 32--63) are partitioned into three regions:

Reserved registers (32--39) are persistent: they retain their values across instructions and are never handed out by the allocator. The two reservation registers are used by the LR/SC virtual sequences to track atomic reservations. The six CSR registers store M-mode control/status state for trap handling.

Instruction registers (40--46) are a pool of 7 temporary registers used by allocate() within virtual sequences (e.g., for division, SC). They are released back to the pool when the virtual sequence completes.

Inline registers (47--63) are used by allocate_for_inline() for inline sequences. All inline registers must be zeroed at the end of the inline sequence to ensure clean state.

Deviations from the Twist algorithm as described in the paper

Our implementation of the Twist prover algorithm differs from the description given in the Twist and Shout paper in a couple of ways. One such deviation is wv virtualization. Other, register-specific deviations are described below.

Two reads, one write per cycle

The Twist algorithm as described in the paper assumes one read and one write per cycle, with corresponding polynomials $\widetilde{\text{ra}}$ (read address) and $\widetilde{\text{wa}}$ (write address). However, in the context of the RV64IMAC instruction set, a single instruction (specifically, an R-type instruction) can read from two source registers (rs1 and rs2) and write to a destination register (rd).

Thus, we have two $\widetilde{\text{ra}}$ polynomials corresponding to rs1 and rs2, plus a $\widetilde{\text{wa}}$) polynomial corresponding to rd. Similarly, there are two $\widetilde{\text{rv}}$ polynomials and one $\widetilde{\text{wv}}$ polynomial.

As a result, we have two read-checking sumcheck instances and one write-checking sumcheck instance. In practice, all three are batched into a single sumcheck instance.

Why we don't need one-hot checks

Normally in Twist and Shout, polynomials like $\widetilde{\text{ra}}$ and $\widetilde{\text{wa}}$ need to be checked for one-hotness using the Booleanity and Hamming weight sumchecks.

In the context of registers, we do not need to perform these one-hot checks for ${\widetilde{\text{ra}}}_{\text{rs1}}$, ${\widetilde{\text{ra}}}_{\text{rs2}}$, and ${\widetilde{\text{wa}}}_{\text{rd}}$.

Observe that the registers are hardcoded in the program bytecode. Thus we can virtualize ${\widetilde{\text{ra}}}_{\text{rs1}}$, ${\widetilde{\text{ra}}}_{\text{rs2}}$, and ${\widetilde{\text{wa}}}_{\text{rd}}$ using the bytecode read-checking sumcheck. Since the bytecode is known by the verifier and assumed to be "well-formed", the soundness of the read-checking sumcheck effectively ensures the one-hotness of ${\widetilde{\text{ra}}}_{\text{rs1}}$, ${\widetilde{\text{ra}}}_{\text{rs2}}$, and ${\widetilde{\text{wa}}}_{\text{rd}}$.

A (simplified) sumcheck expression to illustrate how this virtualization works:

$${\widetilde{\text{ra}}}_{\text{rs1}}(r_{\text{register}},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{rd}}(k,r_{\text{register}})$$

where $\widetilde{\text{rd}}(k_{\text{bytecode}},k_{\text{register}})=1$ if the instruction at index $k_{\text{bytecode}}$ in the bytecode has $\text{rs1}=k_{\text{register}}$.