NOTE: Draft of post for zkresear.ch as one of the deliverables for the residency. Want to post this on Thursday ~2m. /Oskar
This work was done at ZK Spring Residency in Vietnam. It is a joint work by Carlos (PSE), Chiro (Orochi Network), Nalin (0xPARC), Oskar (independent), and Violet (Delv). Special thanks to to Nalin for shaping the design and explaining Nova to us, Srinath Setty (Microsoft) for the Nova paper/code, and 0xPARC/PSE for hosting the Spring Residency.
This post introduces our ideas for a Nova-based VM, some initial benchmarks and future steps.
This is the latest version as of 2023-04-06 1pm Vietnam time.
The live version can be found here.
We propose a ZKVM based on Nova/SuperNova. Nova allows us execute repetitive blocks of code more efficiently using Incrementally Verifiable Computation (IVC) and a so called folding scheme. SuperNova generalizes this to work on different blocks of code using Non-uniform IVC (NIVC). This fits well with the instruction set in a VM. Both Nova and Supernova allows us to parallelize significant parts of the computation and also doesn't require FFTs. Taken together, this suggests there should be significantly faster proving time, and lower memory usage.
By mapping Intermediate Representation (IR) and its opcodes to individual IVC steps, we can prove execution of small blocks of repetitive code more efficiently. This leverages existing compiler infrastructure and hot-path optimizations. We propose a design that deals with VM state updates using vector commitments. Each computation step can be folded up in a binary tree that is amendable to be parallelization. The final fold ensures the integrity of the entire computation, and is wrapped up in a SNARK at the very end to achieve succinctness.
This work can be applied to both to proving ZK-WASM and ZK-LLVM execution and we sketch out what this looks like, as well as give an example of a toy VM.
The proposed architecture is especially interesting for unbounded computation execution proving (unlike the EVM with gas) due to not having the same limits around roots of unity and memory consumption, such as in Halo2.
This section gives relevant background for the reader that isn't specific to our ZKVM design.
This section gives relevant background on the notion of IVCs.
Incrementally Verifiable Computation (IVC) is the repeated application of some step function \(F\) on some public state \(z_i\) with some extra witness input \(W_i\) at each step. IVC defines proofs \(\pi_i\) at each step that proves the execution of the first \(i\) steps. That is, \(\pi_i\) proves that \(F^i(z_0) = z_i\).
Normally, SNARKs are used to construct \(\pi_i\) incrementally [xx].
This section gives relevant background from the Nova paper.
Nova uses IVC but replaces the SNARK verifier with a Folding Scheme. By doing this, the recursion overhead is significantly reduced, up to an order of magintude or more.
With Nova, the prover at each step only has to do O(C)
MSM (Multi Scalar Multiplications). We can compare this with Halo, where the work done at each step is O(C)
FFT and O(C)
EXP (Exponentiations in a cryptographic group). C is the size of the circuit.
In practice, the recursion overhead is on the order of ~10 000 constraints. This means that if we have more constraints than that for a given function, it is worthwhile to fold it.
See section below on how paralleization of Nova can be achieved.
This section gives relevant background from the SuperNova paper.
Supernova generalizes Nova by allowing for Non-Uniform IVC. This means that we can have different functions being run at each step.
Naively, NIVC can be achieved with Nova where you bundle together functions and have a switch function. However, this means the circuit for each step is \(O(C \cdot L)\), where C is the number of constraints for a function, and L is the number of distinct functions.
With SuperNova, we maintain L running instances in parallel, one for each function, and fold the current steps's proofs to the relevant function.
In this section we give an overview of the approach taken.
A VM is made up of a set of instructions executed sequentially together with some state (memory/stack). Each opcode in this VM corresponds to a step in the IVC. We use SuperNova to more efficiently leverage different opcodes. We also parallelize the proving of each step. Memory state changes is dealt with as public input and output to each step change, and is done with vector commitments (other designs are also possible).
With SuperNova we have multiple different functions run at each step. THis maps very nicely to opcodes in a VM.
In the context of a VM with N instructions, the prover work is reduced from \(O(N \cdot C \cdot L)\) to \(O(N \cdot (C + L))\), which is quite significant. For any reasonable \(C>>L\), it also means we don't have to be too concerned with the number of opcodes.
For example, EVM is on the order of ~100 opcodes WASM is on the order of ~400 opcodes. We can safely assume \(C\) is much larger than that, so the prover time becomes \(O(N \cdot C)\) where C is the average number of constraints per opcode.
In this section we show how Nova can be parallelized.
To parallelize Nova, we construct a binary tree of computations, where each node executes one step. At the root of the tree, we get claim that all computations have been executed correcly in the correct order.
Since the required computation at each node can be done without knowledge of the other nodes state, we can parallelize this.
In the above illustration we see how computation is folded upwards. More generally, \(F'(L,R)\) represents a claim that steps L through R have been executed correctly. This claim is a commitment.
As a base case, we have \(F(L,L)\), where \(F(Z_{L-1}) = Z_L\), as per the original Nova paper. \(Z_i\) represents the public input and output.
In the above diagam, we have two types of nodes, base layer nodes and internal/intermediate nodes.
Base layer nodes only prove the execution trace. Each of them proves a state change dependant on the F instance we apply.
Internal nodes also prove a correct step change. But in addition, they prove the correct chaining of the previous output being equal to the actual input. They also take care of proving the correct folding performed in downstream instances.
We can see this in more detail below:
Here we can see the two different cases that we can have in Nova. We have a base layer, which requires us to provide witness for as well as represent the entire execution trace (\(F\) boxes above).
Above, we see the intermediate levels (which keeps going until the top). These prove a correct execution of \(F\) and take care of the public input/output consistency of the folds as well as doing the NIFS.Verify
step.
To understand how folding works in Nova in more detail, let's look at the required checks and how it works in each case.
We can see above the distinction between the things we have to check for base nodes and internal nodes, respectively. Green indicates that it is a check we perform and red that we don't perform it. We include both checks we do and don't do to make the recursion easier to write and reason about.
For base nodes, we just prove that if we apply F
to the input we get the expected output. That is, we prove that given a set of public inputs we get a set of public outputs that is pushed forward to the next F
instance.
To do so, we create an F'
instance which verifies a dummy-initialized and agreed-upon (between the prover and the verifier) folding instance (the NIFS.Verify()
step).
We aren't actually verifying any previous folds here. We are just combining the initial dummy fold with our F'
instance.
Finally, we need to ensure public input-output consistency. This step is not needed as we're on the base layer and there's no initial inputs/outputs on what we need to agree with for our F'
instance validation.
At the end of this, we simply:
Note that we include the dummy checks too as we want all the \(F'\) instances to be of the same shape.
In the case of intermediate nodes, the story is completely different.
In this case, we have both inputs for an F and pair of Relaxed R1CS instances which claim to satisfy a pair of previously folded \(F'\) instances which are one computational step apart.
As seen in the above figure, the purpose of the intermediate nodes is to:
F(left.out) = F(right.in)
To summarize, we parallelize Nova by using a binary tree structure for computation. We compute incremental proofs of a single step, and then fold "upwards". That is, step 1-2
and step 3-4
turns into proving transition from step [1-2]
to step [3-4]
.
At the very top of the tree, we guarantee the integrity of the computation and that all state transitions happened correctly.
See Nova (PSE fork) for an experimental implementation of parallel Nova.
Also see appendix for a sketch of a distributed prover architecture.
In the previous section we described how an F' would verify a folding step on each new step in our proof. However this sketch misses a key detail: because the base field is not equal to the elliptic curve field the constraints to do this naively would be quite expensive. To get around this we run two chains of folded proofs together and use an elliptic curve cycle where the verification of the elliptic curve operations of one curve are cheap to verify in the base field of the other and vice versa. This adds to the recursive overhead of at least the size of the F' circuit and proving time for an extra fold to each step of the sequential prover.
We use this curve cycling in practice for the sequential case by initalizing two relaxed and two normal R1CS instances. The algorithm for moving forward one step in the proof is as follows:
At the end you will have a Nova proof of the folding validity of the other curve's Nova sequence and this curve's circuit invoked \(n\) times, for each curve. They must be proven and verified together to be valid as each curve's Nova instance check's the other curve's Nova instance.
Direct application of the system for constructing Nova by curve cycling from the previous proof to the parallel case will fail. This is because the F' for the sequential case is designed to only accumulate 1 relaxed R1CS with 1 normal R1CS. In the parallel case each node in our tree has both a relaxed R1CS instance claiming the validity of node proofs below via folding and a new R1CS claiming the next invokation of F'. In order to reduce these four claims to one we implemented a naive proof of concept which folds 2 relaxed and 2 normal R1CS instances to one relaxed instance, and an F' which verifies this quad fold. Our naive implementation reuses as much of Microsoft's Nova's lib as possible as so is implemented as 3 foldings of 2 instances. This is likely much less efficient than implementing this as a new higher degree folding protocol.
We give a diagram of this where we create a new \(u\) which is an R1CS claim that the left and right nodes of a tree fold to a new relaxed R1CS claim \(N\):
When we speak about SuperNova parallelization, things can get quite complicated.
The main thing to consider is that SuperNova is designed to support VM execution trace proving. That means that for each set of opcodes, we need to support each one of them in each fold (we don't know which opcode will be digested on each fold). Rephrasing, we don't know which will be the next folded opcode on the next \(F'\) instance.
Now, each fold will contain as many \(F'\) instances as opcodes we have avaliable.
It is already well known how to support multiple opcodes within Nova-style folds. The unknown is mostly how to guarantee memory, execution-order and stack consistency across folds in SuperNova. Especially in the parallel case.
We sketch a design proposal for that, which solves the issues at a pretty affordable cost within R1CS (could be improved using a Plonkish-style arithmetization). See the section below.
The idea is to commit to the memory state of the VM before and after the \(F'\) execution. So that we can open all the positions we want and prove inside of the R1CS that they're equivalent to our witness values which with we will operate then.
One challenge with a VM is that you need to make sure your memory is consistent.
With vector commitments we have the following operations:
Remember that a vector commitment commits to a vector \(a_0,…,a_{n−1}\) and lets you prove that you committed to \(a_i\) for some \(i\). We can reproduce this using the Kate commitment scheme: Let \(p(X)\) be the polynomial that for all \(i\) evaluates as \(p(i)=a_i\).
This completely matches the behaviour we need where we will commit to all the Memory positions for example, and we need to prove inside of the circuit that we are providing the witnesses that satisfy the openings at particular places of the memory.
As per KZG commitments We know there is such a polynomial, and we can for example compute it using Lagrange interpolation:
\[
\sum_{n=0}^{n=i_{max}}Mem_i \prod_{n=0}^{n=i_{max}} {X-j\over n-j}
\]
As an example, let's look at the MUL opcode. Let's assume we have commitments to all the Memory and Stack positions such that:
\[ C_M = \sum_{i=Mem(0)}^{i=Mem(MAX)}Mem_i \prod_{j=0\\j \neq i}^{j=MaxMemPos} {X-j\over i-j} \\ C_S = \sum_{i=Stack(0)}^{i=Stack(MAX)}Stack_i \prod_{j=0\\j \neq i}^{j=MaxStackPos} {X-j\over i-j} \]
Therefore:
\[ \mathbb{Opcode}_{MUL} \gets a \times b = c \]
We first fetch \(a\), \(b\) and \(c\) from memory. To do so, we prove the correct openings of them against \(C_M\). Note that \(c\) is obtained from the commitment of the memory at the end of the step (\(C_{M+1}\))
\[ Fetch(Mem(idx_a)) \gets \mathbb O(C_M, idx_a) = a\\ Fetch(Mem(idx_b)) \gets \mathbb O(C_M, idx_b) = b\\ Set(Mem(idx_{c+1})) \gets \mathbb E(C_{M+1}, c_{+1}, idx_{c+1})\\ \]
We now check the Stack consistency by checking that \(a\), \(b\) and \(c\) are at the correct positions in the Stack at the end.
\[ Set(Stack(a)) \gets \mathbb E(C_{S+1}, a, idx_{a+1})\\ Set(Stack(b)) \gets \mathbb E(C_{S+1}, b, idx_{b+1})\\ Set(Stack(c_{+1})) \gets \mathbb E(C_{S+1}, c_{+1}, idx_{c+1})\\ \]
Now we apply a constraint in R1CS which checks the correctness of the MUL execution.
\[ R1CS(a \times b = c_{+1}) \]
Note that we have just proven the correctness of the memory handling for one Opcode. This has 2 important considerations:
Public Inputs
of the current fold are the Public Outputs
of the previous one. In that way, at the very top of the aggregation/folding tree we are sure all the memory is consistent.See appendix for more details on how to handle memory.
With the above architecture, a lot of the problems that we expect to see are essentially compiler problems. This means we can leverage existing techniques, such as hot-path optimization etc to our benefit. This is a well known problem, and there's a lot of literature and tools around this that can be leveraged.
In this document, we focus on a toy VM, but the general architecture can be used in any general-purpose VM, and this was indeed one of the motivations behind the Nova and SuperNova paper.
Notice that unlike in the ZKEVM, there's no concept of Gas
for ZKWASM or any VM in general.
That means that proving systems like Halo2 or Groth16 can have a hard time expressing VM execution traces due to the fact that they're limited by the amount of roots of unity they have on their underlying curves.
While recursion could be a solution for this, but then there are chalenges on how to properly partition the execution trace. There are also limitations that plonkish-style proving systems have when there are a lot of columns or rows, which is that aggregation is slow.
A simple toy VM which includes ADD and MUL instructions, together with memory and program counter can be constructed. This gives intuition for the general approach and also touches relevant aspects (dealing with memory and overhead for it, multiple opcodes, execution trace).
See section below for a WASM-based execution trace that includes this.
zk-WASM is interesting because WASM is more general-purpose than e.g. EVM. This opens the door for a lot of developers to do private and verifiable computation.
For example, a user may want to prove the WASM execution of having access to some website in the browser, or prove that their sqlite db contains some entry.
We can modify Emscripten to prove correct execution of the intermediate representation. In the appendix we illustrate how we can extract the execution trace from WASMthe WebAssembly runtime.
Similarly to WASM, LLVM uses a modular architecture and it is possible to add new backends and optimizations to LLVM. Using the suggested architecture essentially turns the problem into a compiler optimization problem.
Note that because of how SuperNova works, we can add extra opcodes without significant overhead.
RISC-V is an open standard instruction set architecture based on established RISC principles. Unlike most other ISA designs, RISC-V is provided under open source licenses that do not require fees to use.
There are some advantages of zk-RISC-V to be a good candidate for zkVM.
Nova assumes DLOG hardness and RO (Random Oracle).
While privacy has not been a focus of this architecture, we can naively and trivially re-introduce it by performing a zk-SNARK for each folding step. However, this is likely to be very inefficent. We can also replace the Spartan compression proof with one that is ZK. This has the downside that the prover of the IVC cannot be shared.
To enable zero-knowledge privacy more efficiently requires further research.
The following section includes some preliminary benchmarks
See current list of benchmarks here. This document also contains some pointers for how to write performant circuits.
This section sketches how a distributed Nova prover might look like and what kind of performance we can expect.
The following can be simulated in a server with N threads. Alternatively, it can be done in a distributed fashion, either in a controlled data center environment, or in a permissionless environment. As we move from a single server to a data center to a permissionless network we can expect more participants/total parallelization capacity, at the cost of higher latency and complexity.
In cases where we don't have \(2^n\) steps, we can either pad the tree, or we can "skip" the computation and compute it at two levels above (this is due to elliptic curve cycles).
A base level computation involves three folds - aggregated, primary and secondary circuit.
The three folds of the par case are folding the left running instance with the left new instance, that for the right and then folding the result of those two folds.
This merges two nodes where each node has a running instance and new instance.
At the very top of the tree a CompressedSNARK is generated, either by the coordinator or the first available worker.
If we have N execution steps and N workers, we can roughly expect the following overhead:
L
If \(L\) is high, we lose a lot of the benefits of parallelization. Also note that for the sequential case, a lot of MSM operations can be performed in a multi-threaded environment (powerful server).
To reduce load on coordinator we can also send this to predefined worker, assuming equal load. For example, worker 2 could send its result to worker 1, etc. This assumes that (i) workers are reliable (ii) each worker finishes in about the same time.
Also note that we change field for each level in the tree, which may incur extra overhead.
To prove arbitrary computation we need to extract the execution trace and prove that every step of the computation is correct.
See here for extracting the execution trace of the WebAssembly runtime.
See proposal on how to deal with memory trace using KZG commitments, verkle trees and vector commitments.
Non-exhaustive list of thing that should be added to this spec:
NIFS.Verify
in backgroundCopyright and related rights waived via CC0.
Here's a list of some of the benchmarks we've been taking to better understand how Nova performs vs other proof systems.
NOTE: Disclaimer - these benchmarks are preliminary and should be taken with a grain of salt. Some shortcuts were taken as these were done and we want to check the correctness of these calculations before being 100% confident in them.
Recursively hashing of SHA256 \(k\) times. That is, computations of the form \(h(h(h(h(h(x)))))\).
This also show how doing many recursives hashes in a single fold in Nova improves performance. That is, turning expression above into:
\[h(h(h(x))) \text{(d times)}\rightarrow h(h(h(x))) \text{(d times)} \rightarrow \dots\]
With the same number of recursive hashes, just batching more in a single fold.
Rationale: Similar to https://github.com/celer-network/zk-benchmark but doing hashing recursively to take advantage of Nova+IVC.
Code: https://github.com/privacy-scaling-explorations/nova-bench
Framework | Arithmetization | Algorithm | Curve | Other |
---|---|---|---|---|
Circom (snarkjs) | R1CS | Groth16 | Pasta | |
Nova (seq) | Relaxed R1CS | Nova | Pasta | |
Nova (par) | Relaxed R1CS | Nova | Pasta | parallel PoC |
Halo2 | Plonkish | KZG | BN254 |
Hardware: Macbook Pro M1 Max (2021), 64GB memory.
k | Circom | Nova (total) d=1 | Nova (step sum) d=1 | Halo 2 (KZG) |
---|---|---|---|---|
1 | 0.3s | 0.2s | 0.1s | 0.8s |
10 | 7.3s | 2.4s | 1.2s | 0.8s |
100 | 62s | 24s | 12.5s | 1.6s |
1000 | - | 240s | 125s | 25s |
Hardware: Server with 72 cores and ~350GB RAM.
k | Nova d=1 | Nova d=10 | Nova d=100 | Nova d=100 par | Halo 2 (KZG) |
---|---|---|---|---|---|
100 | 19s | 3.6s | - | - | 2.5s |
1000 | 190s | 36s | 26.5s | 28.5s | 41.6s |
10000 | 1900s | 360s | 265s | 226s | 389.1s |
100000 | 19000s | ? |
This is not completely an apples-to-apples comparison, as: (i) Circom implements the recursive hashing "in-circuit", and (ii) Halo2 uses a different aritmeitization and lookup tables with a highly optimized implementation. However, it shows how a standard operation behaves when called recursively and expressed in a (somewhat) idiomatic fashion.
Step sum is the sum of all the individual folds, i.e. it doesn't account for the witness generation etc that is done when calling create_recursive_circuit
in Nova Scotia. The witness generation overhead is quite high, especially when running it in WASM (MBP M1 limitation). The step sum is the more representative metric. For Nova, we also don't count the SNARK verification part (currently done with Spartan using IPA-PC, not a huge overhead).
The d
parameter is how many recursive hashes we do inside each fold. For the Nova examples we use step sum.
Circom (Groth16) and Nova are run with the Pasta (Pallas/Vesta) curves and use (Relaxed) R1CS arithmetization. Halo2 (KZG) is using BN254 and Plonkish arithmetization.
Hardware: Server with 72 cores and ~350GB RAM
k | Nova (seq) d=1 | Halo 2 (KZG) | Nova (par PoC) |
---|---|---|---|
100 | 1.6GB | 3.7GB | 9GB |
1000 | 1.6GB | 32GB | 244GB |
10000 | 1.6GB | 245GB | OOM |
100000 | 1.6GB | ? | ? |
For Circom, at k=100 the number of constraints is 3m, and we need 23 powers of tau or structured reference string (SRS), 2^23. This is a 9GB file and it increases linearly, quickly becomes infeasible.
For Halo2, which is Plonkish, the situation is a bit better. The SRS of Halo2 is 2^18 for k=100, 2^22 for k=1000, and 2^25 for k=10000. Because the arithmetization is more efficient, Halo2 needs a shorter SRS than Circom.
Nova, assuming it is run natively or with Circom C++ witness generator, has constant memory overhead. Note that we use Nova Scotia and Circom for writing the circuits. With d=1 we have ~30k constraints, d=10 300k constraints, etc.
In the current parallel PoC of Nova there's a bug in the code that leads to linearly increasing memory. This isn't intrinsic to Nova though, and more of a software bug.
Based on the above we draw the following conclusions:
NOTE: We also did a benchmark for Bitcoin blocks, but this is comparing against an old prototype of Halo so is less relevant. See here.
While above benchmarks gives us some insight, it'd be useful to do further benchmarks to better understand how Nova behaves. These are not in order of priority.
Nova is quite new, and working on this for the last few weeks we've identified a lot of things that can be improved in Nova and the Nova-related ecosystem. Here's a Nova wishlist and next steps.
For people who want to participate in the effort we have the main repo here.
We also welcome people to join the Nova track at the Zuzalu ZK Hackathon Apr 16-23.
Thank you for your attention and we welcome comments in this thread and on our Github repo.
Copyright and related rights waived via CC0.