This is a note describing some ideas for building a VM using Nova/SuperNova (in future even with lookups/custom gates). Many of these ideas come from my prior experiments with Nova-zkMIPS and thinking about efficient zkVMs (thanks also to Adhyyan, afkbyte, Sampriti, Ye, YT and others for discussion and brainstorms on it), and were then made concrete in collaboration with the PSE zkWASM team (Carlos, Chiro, Oskarth, Violet, others?) at the Vietnam Residency.
The latter two are optional and subject to failure for various reasons, whereas the first one is an idea described vaguely in the original papers (so unlikely to have issues), and is also necessary to the success of a Nova-based zkVM vs. Halo2 or other proof systems.
Here are some explanations for how to parallelise proving with Nova.
For background, we first share a view of typical sequential IVC:
What IVC typically looks like, and how typical SNARK recursion based proving for IVC works
IVC is the repeated application of some step function (F) on some public state () with some extra/unknown witness input () at each step. In particular, IVC defines proofs at each step () that prove the execution of the first steps by themselves (in other words, proves that ).
In the usual instantiation of IVC, we use SNARKs to construct these incrementally: at each step shows that 1) and 2) verifies correctly. This strategy is described in more detail in other talks and blogs.
How Nova replaces the typical SNARK verifier for a Folding Scheme, and the function the folding scheme serves.
Opening the folding scheme black-box a bit more
Notice that in this view, the Nova machinery provides a black box with the ability to prove IVC sequentially. In specific, it assumes proofs are made in sequence, with a running instance being merged with at each step .
The rough idea for parallelizing Nova is by using a binary tree structure for computation instead. We will compute incremental proofs of single steps, double them in size, and continue until we've exhausted the entire trace.
More concretely, we use our folding scheme in the internal nodes to fold together proofs of half the computation trace, and additionally maintain some book-keeping and some checks of consistency for the values flowing through the computation.
Here's a closer look at the modded function F' in this case:
Read this diagram left side first, then right. The top part is about how the function F' proceeds and verifies. The bottom W (witness) notes how the prover computes the necessary values for the folding step at the level above the current one.
To get to SuperNova, we'll first define a VM-like notion of IVC: Non-uniform IVC. The only difference is that NIVC switches between the function being ran at each step (from some small set of hardcoded instructions).
selects which opcode to run at each step
Nova's folding scheme only works when merging two instances of the same circuit. SuperNova's key innovation is to provide an idea for folding many circuits in parallel for IVC, virtually allowing for many opcode-IVC, defined by the authors as Non-uniform IVC.
Out of the box, the simplest way to run NIVC with Nova is to just treat it as regular IVC, but with switch/case conditions: At each step, choose which opcode to run in the R1CS constraints. This yields a size circuit for each step (where = number of constraints for one opcode, = number of distinct opcodes).
SuperNova optimises by removing this switch/case conditional: instead, we maintain running instances in parallel, one for each opcode, and fold the current step's proof to the relevant opcode (with an added check that picked this opcode correctly). Here's a diagramatic explanation:
Notice that we've reduced the prover work done from to , a pretty significant asymptote.
Much like before, we'll make a binary tree structure, but now with many folding boxes (to contain the instances for each opcode).
Much like before, this binary tree structure takes time to compute, but with parallelisation of folding supported in a bottom-up order.
The key observation here is that Supernova works with any blocks of constraints, so the "opcodes" in SuperNova need not have anything to do with the real opcodes of the VM itself. While shifting around and adding opcodes does not impact the total number of constraints we have to prove for a computation trace, it can help us reduce the cost of folding at each step.
To verify a folding, Nova adds some number of constraints (for hashing, checking the commitment openings etc.). While we generally ignore these overhead constraints in asymptotics, let's focus on them for practicality: let's call the number of these constraints the recursion overhead/threshold (in practice, this number is 10000). The cost of running steps of SuperNova is . Notice that SuperNova allows us to shift around these recursion overhead constraints:
Note also that we assume above that .