In this post we will take a high level look at zkVMs. I wrote this blogpost mainly to have some context for when building out the Erigion executable proof sourcing project. It looks at how zkVMs are built and some that exists already, it mainly focuses on zkVMs targeting EVM execution proofs.
I'm not the first to write about this, obviously, you can read more at these places:
(I'm reusing the example from the blogpost of Vitalik throughout this section)
From a high level, things are built up by Algebraic circuits which you can think of as logic gates. You perform some computation, you have that encoded as gates, then you can verify the logic gates.
More precisely, you have some equation that you want to prove that you have the answer for.
def qeval(x):
y = x**3
return x + y + 5(I'm reusing the example from the blogpost of Vitalik throughout this section)
This code by itself is too complex to prove so we need to do some adjustments to make it provable. The first step in doing that is converting it into a flattened form (also called algebraic circuit).
The flattened form can only do some operators like assignments or simple math operators ($a + b$, $a - b$, $a \cdot b$, $\frac{a}{b}$) which is why we can't do $x^3$ in one step.
sym_1 = x * x
y = sym_1 * x
sym_2 = y + x
~out = sym_2 + 5This flattened form can then be converted into R1CS. This is just a way to describe the constraint in the form of $(A \cdot w) \circ (B \cdot w) = (C \cdot w)$ which we will now look at.
We will mainly discuss this at a high level, if you want the full details see this section from the original post of Vitalik.
Each logic gate will have a constraint and they will always be in a triplet form (which is also why we needed to do $x^3$ in two operations above). This means we can describe it as group of three vectors ($a$, $b$ and $c$) which would encapsulate the outputs and the inputs. There would also need to be a solution ($w$) to this constraint which when applied would make the results on both sides be equal. The witness vector contains all the variables from the flattened computation and is used to provide the intermediate values of the computation steps.
The constraints are created like this:
A[0] = [0,1,0,0,0,0] selects x
B[0] = [0,1,0,0,0,0] selects x
C[0] = [0,0,0,1,0,0] selects sym_1
A[1] = [0,0,0,1,0,0] selects sym_1
B[1] = [0,1,0,0,0,0] selects x
C[1] = [0,0,0,0,1,0] selects y
A[2] = [0,1,0,0,1,0] selects x + y
B[2] = [1,0,0,0,0,0] selects ~one
C[2] = [0,0,0,0,0,1] selects sym_2
A[3] = [5,0,0,0,0,1] selects (5 * ~one) + sym_2 = 5 + sym_2
B[3] = [1,0,0,0,0,0] selects ~one
C[3] = [0,0,1,0,0,0] selects ~out
We can compute the solution vector (also called witness vector) with the following computation
def compute_witness(x):
# Step 1: sym_1 = x * x
sym_1 = x * x
# Step 2: y = sym_1 * x (this gives us x^3)
y = sym_1 * x
# Step 3: sym_2 = y + x (this gives us x^3 + x)
sym_2 = y + x
# Step 4: out = sym_2 + 5 (this gives us x^3 + x + 5)
out = sym_2 + 5
# Construct witness vector: [~one, x, ~out, sym_1, y, sym_2]
witness = [1, x, out, sym_1, y, sym_2]
return witness
compute_witness(3) # [1, 3, 35, 9, 27, 30]
We can verify the computation by doing the following
def verify_constraints(witness, A, B, C):
print("Verifying R1CS constraints...")
for i, (a_row, b_row, c_row) in enumerate(zip(A, B, C)):
# Compute dot products
left = sum(a * w for a, w in zip(a_row, witness))
right = sum(b * w for b, w in zip(b_row, witness))
expected = sum(c * w for c, w in zip(c_row, witness))
result = left * right
if result != expected:
return False
return True
We can think of the R1CS as a way to describe zkVMs, but without the zk part. To make it zk, we would convert this R1CS specification into a polynomial (or cryptographic proving system). The two most common ones are STARKs and SNARKs, different zkVMs use different proving systems depending on what tradeoffs they chose (proof size, trusted setup, verification time, etc).
We won't go into the details of encoding it as QAP in this blogpost, but some good resources to read more for this can be found here:
The high level idea would be to create a trace of the program execution and then have a circuit which verifies that computation.
The tricky part is how to handle memory access which is commonly solved by doing Merkle proofs of the memory. What about loops? You can't have them in a arithmetic circuit. One way is to just unroll the program execution. There is also research into using recursion. This is some of many challenges with writing a program that uses zk proofs.
Alright, so it's not all that easy to create proofs for this, but how do we get program execution in the first place? From the previous section you might recall that we only have access to some primitive math operators, luckily enough these operators are simple enough to give us access to NAND gates which are universal computation units.
Some resources to read more about this step can be found here:
Most current zkVMs don't really give privacy benefits, but do give verification speed benefits. zk-SNARKs can verify any code complexity in O(1) time which is why they are appealing.
There are many variants of zkVMs, Vitalik also wrote up a good blogpost on this The different types of ZK-EVMs. zkVMs are generally easier to build and more flexible than building zkEVMs. The big challenge is having the EVM compatibility.
Some resources to read more about this can be found here:
By proving the execution trace we will have full EVM compatibility. This means you don't have to recompile the contract with some custom compiler and that things should generally just work as on mainnet.
This is something that Scroll has done and is also done by Linea. You can see the high level compilation approach matches that of the EVM as well.
Another approach, usually done to optimize the performance is to use a custom VM, but at the cost of more complexity. You will need to recompile your contracts and things are likely to not fully match how things work on mainnet all the time.
There are a few variants of this for instance earlier versions of Polygon Hermez and ZkSync. Note that ZkSync uses a custom fork of the Solidity compiler to generate the zkEVM bytecode.
There has lately also been a lot of progress in general-purpose zkVMs which target other ISA than the EVM. Most of them target RISC-V, but there are also MIPS variants. These has gathered a lot more attention in recent time.
One of the main advantages of this is that it allows faster proving, but the con in the context of the EVM is that no EVM program will be natively supported and has to be recompiled for the target ISA. However, you can always compile the EVM implementation into the target ISA and run the proofs that way.
Some examples of general purpose zkVMs are:
Utilizing general-purpose zkVMs for EVM execution traces is also something I'm looking into with Erigion executable proof sourcing as a way to optimize the proving time of EVM executions by not having to also prove the EVM implementation.
It's also worth mentioning that most of these provers support running on the GPU. RISC ZERO reported a significant improvements (10x+) improvement with GPU optimizations.
Certain operations like cryptography are slow to execute in the raw zkVM ISA. Many therefore add what are called precompiles or accelerated circuits. These are extensions to the underlying ISA to allow certain operations to be performed faster.
For instance, what ISA is being used and how memory modelling is done has an impact on the performance. Parallelized proving by breaking up the program into segments.
Vitalik made a post Long-term L1 execution layer proposal: replace the EVM with RISC-V where he advocated that moving to RISC-V could be beneficial for ZK provers.
Here are some posts that provides more nuance to the discussion
If you liked this post, you might also like: