The purpose of a memory checking protocol is to allow a verifier to audit a large, untrusted memory transcript using only a small proof. The prover logs every read and write operation, generating a proof that guarantees both the correctness of the final memory state and the consistency of all operations. While most popular zkVMs use fairly standard methods for proving CPU instructions (with the notable exception of Jolt), the techniques for proving memory consistency play a critical role in determining proving speed. In this article, we provide a brief overview of the fundamental constructions and primitives used in memory checking protocols, and highlight which approaches are adopted by popular zkVMs.

Permutation argument

Many popular zkVMs nowadays use a permutation argument to prove the correctness of memory operations. We call a permutation argument an approach that allows proving the equality of two multisets, regardless of the order of the elements.

Based on ¹, the high-level idea is to reduce the claim of the correct memory transformation to the claim of the multisets equality. We start defining each memory cell as a tuple $(\mathsf{addr}, \mathsf{val}, \mathsf{cnt})$. Each of “Read” or “Write” operations (which basically are the simulated CPU instructions for the corresponding IS of the particular zkVM) is followed by incrementing of the corresponding counter, so the counter can be understood as a memory cell’s timestamp.

• Write$(\mathsf{addr}, \mathsf{val})$:
  (1) read the old value and its counter $\mathsf{cnt}$ at address $\mathsf{addr}$;
  (2) write the new value $\mathsf{val}$ with counter $\mathsf{cnt} + 1$ at address $\mathsf{addr}$.

• Read$(\mathsf{addr}) \rightarrow \mathsf{val}$:
  (1) read the value $\mathsf{val}$ and its counter $\mathsf{cnt}$ at address $\mathsf{addr}$;
  (2) write the same value $\mathsf{val}$ with counter $\mathsf{cnt} + 1$ at address $\mathsf{addr}$.

So, basically, each read operation is equal to the write operation, but with the same value. Next, let’s additionally define the following sets:

• $\mathsf{Writes}$ contains tuples that represent write operations: $(\mathsf{addr}, \mathsf{val}, \mathsf{cnt})$, where $\mathsf{val}$ is the value stored at the memory address $\mathsf{addr}$ with the specified counter $\mathsf{cnt}$;
• $\mathsf{Reads}$ contains tuples that represent read operations: $(\mathsf{addr}, \mathsf{val}, \mathsf{cnt})$, where $\mathsf{val}$ is the value read from the memory address $\mathsf{addr}$ with the specified counter $\mathsf{cnt}$;
• $\mathsf{Final}$ contains tuples such that $\mathsf{Writes} = \mathsf{Reads} \cup \mathsf{Final}$ if and only if all operations were executed correctly; otherwise, no such $\mathsf{Final}$ exists that satisfies this equality.

At the beginning, $\mathsf{Writes}$ is populated with the initial untrusted memory $\mathcal{M}$ state, where all counters are set to $0$, indicating that the values were first accessed during the initialization phase, while the $\mathsf{Reads}$ and $\mathsf{Final}$ are empty. Then, the prover executes the following functions any number of times:

Write$(\mathsf{addr}, \mathsf{val})$:

1. (old_val, cnt) := 𝑀[addr]
2. insert (addr, old_val, cnt) into Reads
3. 𝑀[addr] := (val, cnt+1)
4. insert (addr, val, cnt+1) into Writes

Read$(\mathsf{addr}) \rightarrow \mathsf{val}$:

1. (val, cnt) := 𝑀[addr]
2. insert (addr, val, cnt) into Reads
3. 𝑀[addr] := (val, cnt+1)
4. insert (addr, val, cnt+1) into Writes
5. return val

After all the read and write operations are done, one can notice that the $\mathsf{Final}$ multiset equals the final memory state. Then, the equality of multisets $\mathsf{Writes}=\mathsf{Reads} \cup \mathsf{Final}$ can be verified using a permutation argument.

Grand-products permutation argument (Jolt, RISC Zero)

The direct and most popular implementation of the permutation argument is ². It assumes proving that the products of elements shifted by a random challenge $\tau$ in both multisets are equal. While our multisets’ elements are tuples in $\hat{\mathbb{F}}^3$, we additionally require the existence of a deterministic isomorphism $\mathsf{f}: \hat{\mathbb{F}}^3 \rightarrow \mathbb{F}$. So, our final claim $\mathsf{Writes}$ and $\mathsf{Reads} \cup \mathsf{Final}$ can be verified via a grand-product protocol using a challenge $\tau \in \mathbb{F}$:

Sum-based permutation argument (Valida)

Using the LogUp ³ idea, the goal of the sum-based permutation argument is to reduce the number of multiplications in the circuit, replacing them with additions. This also allows the usage of sum-check as a proving backend directly. Same as before, while our multisets’ elements are tuples in $\hat{\mathbb{F}}^3$, we additionally require the existence of a deterministic isomorphism $\mathsf{f}: \hat{\mathbb{F}}^3 \rightarrow \mathbb{F}$. Then, we prove that, using challenge $\tau \in \mathbb{F}$, the following sums are equal:

Elliptic curve multi-set hashing (SP1)

Let’s assume the existence of a special function $\mathsf{Enc}\colon \mathbb{F}\rightarrow\mathbb{G}$. Commonly, it assumes a deterministic, curve-specific, and probabilistic algorithm that solves the quadratic equation to find the second coordinate under the hood. Then, following ⁴, we can use this encoding function to represent our multiset elements as elliptic curve points, checking that the additive equality holds using the group operation. Same as before, while our multisets’ elements are tuples in $\hat{\mathbb{F}}^3$, we additionally require the existence of a deterministic isomorphism $\mathsf{f}: \hat{\mathbb{F}}^3 \rightarrow \mathbb{F}$. So, we prove our final claim by proving the following equality:

The main benefit of such an approach is that we do not need the additional challenge $\tau$ for the permutation check – the security is leveraged on the complexity of the group operation and the deterministic nature of points.

Mapping tuples into one field element

As specified, all permutation argument protocols require the existence of a deterministic (independent of tuple elements) isomorphism $\mathsf{f}: \hat{\mathbb{F}}^3 \rightarrow \mathbb{F}$. This function can additionally be used to achieve blinding property for the tuple elements, but in terms of modern zkVMs, all these protocols are deployed inside the outer proving systems (Groth16 ⁵, PLONK ², etc.), which additionally brings a zero-knowledge property if needed. Thus, the main requirement for $\mathsf{f}$ is to be lightweight to compute inside the outer proving system circuit. Basically, there are two main popular approaches used by popular zkVMs:

• If the element in the multiset is represented through a list of scalars $a \in \hat{\mathbb{F}}^n$, we assume taking a linear combination of them with the vector $(1, \gamma, \gamma^2,\dots,\gamma^{n-1})$, where $\gamma \in \mathbb{F}$ is a random challenge:

  \(\mathsf{f}(a) = \sum_0^{n-1} a_i \gamma^i\) Usually, using such an approach, we assume $\hat{\mathbb{F}} = \mathbb{F}$.

• Lots of modern proving systems leverage the DEEP technique ⁶, which enables the usage of small fields for the constraints (usually, a $\sim 31$-bit field), achieving strong security properties by sampling challenges from the field extension (usually, a $4$-degree extension). Thus, while leveraging the assumption that $a,v,t$ are small enough (namely, $a,v,t \in \hat{\mathbb{F}}$), the bigger field namely, $\mathbb{F}$ such that

  \[3|\hat{\mathbb{F}}| \leq |\mathbb{F}|,\]

  the construction of $\mathsf{f}$ is obvious, (for example, from the implementation perspective it can be a bit concatenation).

Challenges

During the zk-VM proof generation, if the permutation prover requires additional challenges, we should commit to the entire memory trace to enable the use of the Fiat-Shamir heuristics. It means that we have to wait for the entire computation to finish before we can launch the memory proving process. One can note that the described permutation argument protocols may require two types of challenges:

• $\gamma$: a linear combination challenge, that allows us to map tuples into one field element;
• $\tau$: a permutation argument challenge that has a direct impact on the protocol’s security.

Thus, depending on the selected permutation argument protocol implementation and the function $\mathsf{f}$, the memory checking protocol may require one, two, or none challenges to be supplied.

Valida and Jolt

The Valida ⁷ and Jolt [^cryptoeprint:2023/1216], as the relatively new players in the zkVM industry, leverage the sum-based and grand-products permutation arguments accordingly, while the tuples mapping is implemented using a linear combination with an additional challenge. Obviously, this leads to the lack of performance compared to the RISC Zero of SP1.

Airbender

Airbender ⁸ leverages the following approach:

[…] We have to pre-commit to the pieces of the [memory] trace before starting ``full mode’’ proving of those individual pieces. Such pre-commitment is implemented via sending the columns that would be a part of the permutation argument into a separate subtree, so the prover usually does the following:

1. Generate full memory witness (not even full trace witness);
2. Commit to them in a chunked form;
3. Write them into the transcript and draw challenges;
4. Forget all the work above except challenges;
5. Start proving individual circuits using those external challenges for memory arguments;
6. In the recursive verification step – write down the same transcript using memory-related subtree commitments, and assert equality of the challenges from such a regenerated transcript and those external challenges used during proving.

This way, we do $\sim 5-10\%$ redundant work for pre-commit, but keep an excellent degree of parallelism for individual proofs over circuit chunks.

RISC Zero

On the other hand, RISC Zero does not care about the common challenges, delegating the proving of separate segments to the separate instances that evaluate their own challenges depending on their particular inputs [gafni2024highperformance]:

[…] In order to implement a zkVM with continuations, we need to choose between running one permutation argument per segment or running a single permutation argument that spans many segments. In other words, do we generate Fiat-Shamir randomness on a per-segment basis, or do we generate all the segments and then compute the Fiat-Shamir randomness? We opt for running one permutation argument per segment. This approach introduces a bit of overhead due to paging costs, but it saves us from a number of headaches in the context of horizontally scaling our proving infrastructure. Notably, this approach allows us to begin proving each segment as soon as it is constructed. On Bonsai, we begin proving segments before we finish running the executor, which reduces time-to-prove and increases system utilization.

SP1

Finally, the SP1 leverages an elliptic curve approach with small fields for tuples, which does not require sampling challenges, but the tradeoff is the complexity of elliptic group operations. This avoids some overhead with Merkle trees pre-building for memory segments, as in Airbender.