Nebula: Proving Machine Executions via Folding Schemes

A zero-knowledge virtual machine (zkVM) is a versatile, developer-friendly primitive that proves the correct execution of programs on a fixed machine architecture. A major bottleneck for these protocols is the prover's space complexity, which grows linearly with the number of program steps and makes it impractical to produce proofs for longrunning computations. To overcome this, we propose generating these proofs incrementally, using folding schemes. However, realizing this requires new tools in the folding setting: (1) an efficient read-write memory argument for proving the correctness of memory operations; and (2) a method to eliminate the overheads incurred by unused machine instructions when incrementally proving a program execution step. We address these with new techniques. First, we introduce commitment-carrying IVC, where a proof carries an incremental commitment to the prover's non-deterministic advice provided at different steps. Second, we show how this unlocks efficient read-write memory arguments (which implies indexed lookups arguments), with a cost profile identical to that of memory arguments in the context of non-recursive arguments. Third, we provide a new universal “switchboard” circuit construction that combines circuits of different instructions such that one can “turn off” uninvoked circuit elements and constraints, offering a new way to achieve pay-per-use prover costs. We design an IVC scheme, which we refer to as Nebula, that incorporates these techniques. We implement a prototype of a Nebula-based zkVM for the Ethereum Virtual Machine (EVM). We find that our techniques qualitatively provide a $30 \times$ smaller constraint system to represent the EVM over standard memory-checking techniques, and lead to over $260 \times$ faster proof generation for the standard ERC-20 token transfer transaction when compared to our baseline Nova (CRYPTO'22) with existing arithmetization methods.