RAM

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

Dynamic parameters

In Twist, the parameter $K$ determines the size of the memory. For RAM, unlike registers, $K$ is not known a priori and depends on the memory usage of the guest program. Consequently, the parameter $d$, dictating how the memory address space is partitioned into chunks, must also be dynamically tuned. This ensures that no committed polynomial exceeds a maximum size defined by $T\times K^{1/d}$.

Jolt is currently configured so that $K^{1/d}=2^8$.

Address remapping

We treat each 4-byte-aligned word in the guest memory as one "cell" for the purposes of memory checking. Our RISC-V emulator is configured to use 0x80000000 as the DRAM start address -- the stack and heap occupy addresses above the start address, while Jolt reserves some memory below the start address for program inputs and outputs.

For the purposes of the memory checking argument, we remap the memory address to a witness index:

#![allow(unused)]
fn main() {
(address - memory_layout.input_start) / 4 + 1
}

where input_start is the left-most address depicted in the diagram above. The division by four reflects the fact that we treat guest memory as "word-addressable" for the purposes of memory-checking. Any load or store instructions that access less than a full word (e.g. LB, SH) are expanded into virtual sequences that use the LW or SW instead.

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, RAM-specific deviations are described below.

Single operation 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 RV32IM instruction set, only a single memory operation -- either a read or a write (or neither) -- is performed per cycle. Thus, a single polynomial (merging $\widetilde{\text{ra}}$ and $\widetilde{\text{wa}}$) suffices, simplifying and optimizing the algorithm. This polynomial is referred to as $\widetilde{\text{ra}}$ for the rest of this document.

No-op cycles

Many instructions do not access memory, so we represent them using a row of zeros in the $\widetilde{\text{ra}}$ polynomial rather than the one-hot encoding of the accessed address. Having more zeros in $\widetilde{\text{ra}}$ makes it cheaper to commit to and speeds up some of the other Twist sumchecks. This modification necessitates adjustments to the Hamming weight sumcheck, which would otherwise enforce that the Hamming weight for each "row" in $\widetilde{\text{ra}}$ is 1.

We introduce an additional Hamming Booleanity sumcheck:

$$0=\sum _{j\in \{0,1{\}}^{\log (T)}}\widetilde{\text{eq}}(r^{\prime },j)\cdot \left(\widetilde{\text{hw}}(j{)}^2-\widetilde{\text{hw}}(j)\right)$$

where $\widetilde{\text{hw}}$ is the Hamming weight polynomial, which can be virtualized using the original Hamming weight sumcheck expression:

$$\widetilde{\text{hw}}(r_{\text{cycle}})=\sum _{k=(k_1,\dots ,k_d)\in {\left(\{0,1{\}}^{\log (K)/d}\right)}^d}\widetilde{\text{ra}}(k,r_{\text{cycle}})$$

For simplicity, these equations are presented for the $d=1$ case, but as described above, $d$ for RAM is dynamic and can be greater than one.

ra virtualization

In Twist as described in the paper, a higher $d$ parameter would translate to higher sumcheck degree for the read checking, write checking, and $\widetilde{\text{raf}}$ evaluation sumchecks. Moreover, $d>1$ is fundamentally incompatible with the local prover algorithm for the read/write checking sumchecks.

To leverage the local algorithm while still supporting $d>1$, Jolt simply carries out the read checking, write checking, and $\widetilde{\text{raf}}$ evaluation sumchecks as if $d=1$, i.e. with a single (virtual) $\widetilde{\text{ra}}$ polynomial.

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 "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)$$

Output Check

Jolt ensures correctness of guest program outputs via the output check sumcheck. Guest I/O operations, including outputs, inputs, and termination or panic bits, occur within a designated memory region. At execution completion, outputs and relevant status bits are written into this region.

Verifying that the claimed outputs and status bits are correct amounts to checking that the following polynomials agree at the indices corresponding to the program I/O memory region:

Note that val_io is only contains information known by the verifier. To check that these two polynomials are equal, we use the following sumcheck:

$$0=\sum _{k\in \{0,1{\}}^{\log K}}\widetilde{\text{eq}}(r_{\text{address}},k)\cdot \widetilde{\text{io-range}}(k)\cdot \left({\widetilde{\text{Val}}}_{\text{final}}(k)-{\widetilde{\text{Val}}}_{\text{io}}(k)\right)$$

where $\widetilde{\text{io-range}}$ is a "masking" polynomial, equal to 1 at all the indices corresponding to the program I/O region and 0 elsewhere. The MLE for a masking polynomial that isolates the range $[\text{start},\text{end})$ can be written as follows:

$${\widetilde{\text{mask}}}_{\text{start, end}}(r)=\widetilde{\text{LT}}(r,\text{end})-\widetilde{\text{LT}}(r,\text{start})$$

It is implemented in code as RangeMaskPolynomial.

This output check sumcheck generates a claim about the final memory state polynomial (${\widetilde{\text{Val}}}_{\text{final}}$), which, being virtual, is proven using the ${\widetilde{\text{Val}}}_{\text{final}}$ evaluation sumcheck:

$${\widetilde{\text{Val}}}_{\text{final}}(r)-{\widetilde{\text{Val}}}_{\text{init}}(r)=\sum _{j\in \{0,1{\}}^{\log (T)}}\widetilde{\text{Inc}}(j)\cdot \widetilde{\text{ra}}(r,j)$$

Intuitively, the delta between the final and initial state of some memory cell is the sum of all increments to that cell.

You may have noticed in the above expression that $\widetilde{\text{Inc}}(j)$ if a polynomial only over cyclce variables, while the book describes $\widetilde{\text{Inc}}:{\mathbb{F}}^{\log K}\times {\mathbb{F}}^{\log T}\to \mathbb{F}$. This change is explained in wv virtualization.

Both the ${\widetilde{\text{Val}}}_{\text{final}}$ and $\widetilde{\text{Val}}$ evaluation sumchecks use the virtual $\widetilde{\text{ra}}$ polynomial, with claims subsequently proven via ra virtualization sumcheck.