Lambda VM: continuations

Every zkVM runs into the same wall sooner or later. A STARK prover holds the entire execution in memory at once, and for anything the size of an Ethereum block that is more memory than a reasonable machine has. This post is about how zkVMs get around that wall, and about the two ways we tried in Lambda VM.

If you read our first post, you know the theme: keep it simple. This problem is a good test of it, because the standard solution adds a fair amount of machinery, and we wanted to see how little of it we could get away with.

Why the prover needs everything at once

The problem looks like this. The executor runs the program and writes down every step. That log becomes a set of tables, one per kind of operation, and the prover has to commit to every table before it can prove anything about them: each table gets stretched out (the low-degree extension) and hashed into a Merkle tree, and the root of that tree is what goes into the proof.

The catch is that the tables are not independent. The multiplication table has to agree with the CPU table about which multiplications happened, the memory tables have to agree with every load and store, and so on. We check all of that with one lookup argument that spans every table, and that argument needs a random challenge from the verifier. The challenge can only be drawn after every table has been committed, and the reason is soundness. If the prover knew the challenge before committing, it could pick table contents that pass the check for that particular challenge, and the verifier would never know. Committing first pins the tables down, so the challenge tests something the prover can no longer change. So until the last table is committed, nothing can be dropped.

The prover's peak memory, then, is roughly the sum of every table, stretched and hashed, all alive at the same moment. That grows linearly with the number of cycles: a program that runs twice as long needs twice the RAM, and an Ethereum block runs for a very long time.

What everyone else does

The standard answer has a name that RISC Zero gave it back in 2023: continuations. You stop the execution every so often, prove the chunk you just ran, write down enough state for the next chunk to pick up where you left off, and at the end you use recursion to stitch the chunk proofs into one. Memory is almost all of that state, so the interesting differences between zkVMs are in how memory crosses the boundary and where the cut is made.

RISC Zero

RISC Zero splits a run into segments and carries the memory image across them as a Merkle tree; its root, program counter included, is the image ID. Between segments the zkVM "essentially hibernates, saving all working memory to the host", and the segment proofs are later folded into one with two recursion programs, lift and join.

OpenVM

OpenVM does the textbook version, and does it on purpose: its whitepaper wants each segment proof "self-contained, so that segment proving can be parallelized with minimal communication between provers". Memory is a Merkle trie, each segment's proof exposes the root before and after as public values, and the aggregation tree checks that one segment's final root is the next one's initial root.

SP1

SP1 calls its segments shards and skips the Merkle roots. Inside a shard, a memory-local table records, for every address it touched, the value it found first and the value it left behind. Those records, plus the program's initial and final memory, are turned into digests and added into one running sum across shards, and the recursion circuit checks that the sum comes out to zero: if it balances, every value read somewhere was written somewhere.

ZisK

ZisK's whitepaper goes after the hidden cost of the standard scheme: padding every table in every segment to a fixed height. So it "decouples segmentation from execution": each chip slices its own trace into fixed-height pieces, and only the last piece of each chip needs padding. State that has to survive a cut rides on a continuation bus, and one global equation, enforced at the root of the aggregation tree, closes everything.

All four split the work and lean on recursion to put it back together. The consistency checks that make the whole thing sound live in the aggregation layer, not in any single proof. They differ in what crosses the cut (a Merkle root of memory for RISC Zero and OpenVM, a running sum for SP1 and ZisK) and in where the cut goes. But in every case, proving a long program means proving many pieces and then proving that you verified them.

What we wanted

We did not want to go down that road if we could help it. Our first post made the case for a small verifier and a proof system with few moving parts, and a design where proving a long program requires a tree of recursive verifiers, each checking the pieces below it, pulls in the other direction. We also did not want recursion to be mandatory just to get a proof out. Recursion is on our roadmap for other reasons, mainly proofs small enough to verify on Ethereum, but it should be something you add, not something you need.

The question we gave ourselves was narrower: can we bound the prover's memory and still end up with a single proof that the ordinary verifier checks, with no cross-segment logic anywhere?

3MI Labs wrote up two answers in a short section of the spec, and they share one premise. Let the prover build tables the way it always does, and when memory gets tight, do some proving work early so the tables can be thrown away. The two ideas differ in what "some proving work" means and in how much of it has to be redone later. We ended up building both.

Epochs

The first idea starts from an observation about the trace. Take any stretch of cycles: almost every constraint on it can be checked by looking at that stretch alone. An addition is correct or it isn't, a branch goes where it should or it doesn't, and none of that depends on what happened a million cycles earlier. The one thing that reaches outside the stretch is memory, because a load late in the run may read what a store wrote much earlier.

So cut the run into epochs of a fixed number of cycles and prove each one as if it were a complete program, with its own commitments, its own challenge and its own FRI. Once an epoch is proven, everything about it can be dropped except one small table, which we call local-to-global. It has one row per memory cell the epoch touched, and each row says what the cell held when this epoch first saw it, which earlier epoch had written that value, and what the cell held when the epoch was done.

Those tables are what links the epochs. A second, global lookup argument checks that every "this is what I found" claim is matched by exactly one "this is what I left" claim from an earlier epoch, that every cell's chain starts at the program's initial memory, which the verifier knows from the ELF so the prover cannot invent it, and that it ends at the final memory. If an epoch had read a value nobody wrote, the chain would have a gap and the global argument would fail. Inside an epoch the usual memory checking does its job; local-to-global only provides the seams at the edges. Nothing is ever re-executed.

Making this sound took more care than the description suggests. Two examples. The chain has to be ordered: a row must point at a strictly earlier epoch, or a dishonest prover can make a row cancel itself out and slip a forged value into an epoch while every bus still balances. And the selector that tells real rows from padding has to gate every interaction the table takes part in, not just the cross-epoch ones. If it only gated the chain, a prover could flag a real row as padding: that epoch's write would silently drop out of the chain, an older value could be claimed as the cell's final one, and the epoch's own proof would still pass, because its local memory checks never look at that flag.

What epochs cost is structural. Every epoch carries its own copy of the fixed tables, the ones that describe the instruction set and the bit lookups, plus its own padding and its own FRI. So the proof grows with the number of epochs, and so does the work to verify it. That last part matters more than it looks, because verification work is exactly what recursion ends up paying for.

Prove-and-retire

The second idea goes the other way. Instead of splitting the proof into pieces that then have to be reconciled, keep exactly one proof, with one challenge over all the tables, the way the monolithic prover does it. Just refuse to hold everything at once, and re-run the program as many times as it takes.

It works in passes. In the first pass the prover walks the execution and builds tables chunk by chunk; as soon as a chunk is full it is stretched, hashed and committed, and then thrown away. What survives the pass is a list of Merkle roots, plus the few tables that cannot be chunked, the fixed ones and the accumulators behind the hash and signature accelerators. With all the roots in hand, the prover draws the single challenge that ties the tables together, exactly as before. Then it walks the execution again: each table is rebuilt, the lookup argument and the constraint checks are computed for it, it gets its FRI and its openings, and it is dropped again. What crosses from one pass to the next is small: roots, challenges and not much else. The one subtlety is that some tables feed others (every memory timestamp check lands a row in the comparison table, for instance), so a chunk has to settle what it owes the rest before it is retired. Getting that wrong is how a proof of a small test program verifies and a proof of a real block does not.

The proof that comes out is the monolithic proof. Not an equivalent one: the same commitments, checked by the same verifier, and no change to the protocol anywhere. The cost is that trace building and the first round of commitments happen twice, and re-running a program is a real cost when the program is a block. We are paying with compute for the right not to retain.

There is a second variant for when the proof is going to be verified inside another proof. Instead of finishing each table with its own FRI, the prover stops one step short, folds all of those intermediate polynomials into a handful of combined ones, and runs FRI on those. That means far fewer hashes for a verifier to check, which is what a recursive verifier spends most of its time on. It is a new proof format with its own verifier, and we treat it as more experimental than the first variant: its soundness still has to be reviewed by someone who did not write it.

Where we are

Epochs are implemented, and they are what Lambda VM runs today when a program is too long for a single proof. Prove-and-retire is still an experiment, in a branch, and we want to be honest about that. But it has been doing a lot better than we expected, and the reason is not complicated. Re-running a program is cheap next to proving it: the executor is fast, and rebuilding a table from the trace is a small part of what the prover then does with that table. What was expensive all along was holding every stretched, hashed table in memory at the same time. Epochs avoid recomputing anything, but they pay a fixed cost per epoch, in tables and in FRI, and that cost lands in the proof and on the verifier. Prove-and-retire pays once, in compute, and hands back the same proof the monolithic prover would have produced.