TLDR
zkVMs (and especially RISC-V VMs) have received tremendous attention since last year: the vast majority of the ethproofs zk-EVM projects have adopted this approach. Vitalik is even considering swapping the EVM for RISC-V in the future. This is motivated by their versatility and their simplicity while offering reasonable performances. This works by running the code of the EVM in a RISC-V zk-VM and this contrasts with our techniques: writing the EVM in the form of constraints.
We estimate that our approach will yield one order of magnitude better performances in the long run (and therefore reduced prover costs, and better latency). And, we also acknowledge that we need to progressively take to a more versatile approach than hand-writing our constraints as it can only help us to be more Ethereum-aligned, and we outline our ideas to get the best of both world.
Intro
RISC-V is a recent (and already quite mature) flexible and minimal instruction set architecture (ISA). It was developed in 2013 as an open-source alternative to x86 and ARM and is seeing increasing adoption by specialised hardware manufacturers, and is well-supported as a compilation target. This architecture has been chosen by 2 projects, RISC-0 and SP1, as a target to build zk-VMs. By doing so, they have successfully managed to build the first zk-EVM by running the code of the EVM in their zk-VM to generate a proof of execution of an Ethereum mainnet block, thus generating the very first Type-1 zk-EVMs proof. Since then, their performances have considerably improved, and it takes only a few cents to prove a block.
-
Since then, the community’s focus has shifted from direct arithmetization (previously adopted by the major zk-EVM L2s: Linea, Scrolls and Polygon) toward the zk-VMs approach.
-
Today, 21 ZK projects are targeting to compete in the Ethproof.org competition (including Linea)
Linea is one of the only non-zk-VM project
This has led Vitalik to make a radical proposal: replacing the EVM with a RISC-V interpreter.
This hype toward RISC-V is to be nuanced as other projects (PowdrLabs, OpenVM and others …) are working on ISA agnostic solutions, and they can be applied to emulate the EVM. But still, RISC-V is largely predominant as a technical choice.
Despite this shift of attention, we believe that Linea’s approach to building zk-EVM has many benefits that the zk-VM approach cannot offer, and we need to show it better to the community.
Linea uses direct arithmetization
Arithmetizing a system means converting it into maths. More practically, an arithmetization is a very large non-linear system of constraints whose set of solutions maps to a valid trace of execution in the initial system. This is a crucial step for the proof generation, because the prover can only reason about the existence and the validity of a solution, and not directly about the initial system.
Linea uses a direct arithmetization method of the EVM. Concretely, every component of the EVM is abstracted into a manually written circuit. And this can be used to prove the execution of Ethereum blocks of transactions. The arithmetization targets a large field with more than 160 bits and this is the case for historic reasons.
Pros
-
Best performances possible as the approach gives total control for optimising and does not have the overheads of emulating the EVM on an intermediate-level VM. The current arithmetization state is over 10x better than that of state of the Arts RISC-V zk-VMs and this can only improve as we optimise the circuits.
-
Despite not having a tangible result to show it. Working out constraints directly and not having to go through a compiler suite has a reduced bug surface.
-
Worth noting that some key zkVMs are Rust based and all use reth code base / similar compiler toolchain. Direct arithmetization + multiprover has some value for diversity / bug resistance.
Cons
-
It is a complex system and requires a solid expertise in both the EVM and the niche area of zk-Circuit design to maintain it. And typically, implementing an EIP or a protocol upgrade is a multi-week (sometimes months) effort.
-
Although the arithmetization exhibits some common patterns of structure. It contains a lot of manual optimisations and small variations, which seriously complicates the audits and the FV (formal verification) effort. As a nuance, this is something that is continuously addressed by the arithmetization team to get to a more uniform and generalizable approach.
-
The corset arithmetization does not cover all of Linea’s proving statement. As for the ISA approaches, the precompiles are manually written in a lower-level language but that’s not all. For instance, the public-inputs, the extraction of the bridge-logs, the compression proof, the state-access (and more…) are manually added on-top to derive a fully-functional provable relation for Linea.
But we have many ideas to make this effort come out on top and solve the Cons without sacrificing the pros and also getting the pros of the zk-VM approach. Also, Linea targets Type-1 compatibility with Ethereum (currently Type 2).
One idea we are contemplating is that we are generalizing the work that has been done for the EVM to a more standard source language. For example, we would be writing code in a higher-level language and compile it into constraints directly. The resulting solution will give us a higher-level of developer experience while retaining the efficiency of handwritten constraints. As a bonus, it would also simplify the work on FV. Some POCs have already been done, and we believe they have to potential to eventually completely replace our handwritten constraints.
RISC-V-based arithmetization
Currently, a lot of hype goes to RISC-V type 1 zk-EVM. They work by implementing a RISC-V zkVM. The structure is similar to that of Linea, but instead of arithmetizing the EVM directly, they arithmetize the RISC-V ISA, resulting in a zk-VM. This zk-VM is, in turn, used to run and prove the execution of the code of the EVM, compiled from source to RISC-V using a custom compilation pipeline. This emulated version of the EVM can then, in turn, be used to prove the execution of blocks of transactions.
Most of these arithmetizations rely on a small field.
Sources:
Pros
-
Since a RISC-V VM has much less instructions and complexity (gas, exceptions, …) than the EVM, writing an arithmetization for it is comparatively simple. This is without accounting for the precompiles, as both zkVM and zkEVM approaches need to have specific support baked-in the VM to support them.
-
The simplicity of the VM allows for quick wins in the development of a formally verified zk-EVM. Namely, formally verifying the determinism and soundness of a RISC-V circuit is less complicated compared to a direct arithmetization of the EVM. RISC-0 reported having “almost-complete” proof of determinism for their circuit. This does not cover all of what needs to be done, this point is detailed in the Cons.
-
Since many teams concurrently work on it, there are many opportunities to cross-pollinate (meaning they can reuse each other’s work, but the overall progress is steady as a result). This also comes from the fact that most projects use Rust.
-
The RISC-V ecosystem is mature and is well-supported by many languages. There is a caveat still; they compile from a subset of Rust and some other languages only currently. This makes it a natural choice for building a zk-VM.
-
This solution is much better to follow the evolution of the EVM. To reflect a change, it suffices to implement it in the source code and recompile it. It is a bit more complicated than that due to the practical limitations of the current RISC-V VMs. But this remains infinitely simpler than updating a direct arithmetization. Developers can also do it without strong ZK expertise.
-
Cherry on the cake: this allows reusing the tech for other use-cases than zk-EVM.
Cons
-
As a side effect of being minimalistic, RISC-V is not very efficient. Many elementary operations require multiple cycles. For instance, there is no ADDCARRY instruction and doing addition with carry – a trivial task on most ISAs – requires quirking with the generated assembly. Allegedly, this results in 2x-3x overheads compared to better-suited ISAs. This is even worse compared to a direct arithmetization.
-
From a formal verification standpoint, although we have seen considerable progress in formally verifying RISC5 circuits, we are still missing the “EVM source to RISC-V assembly”. Researchers estimates that it would be complete by EOY, but we think this timeline is too optimistic (more like several years). Still, the FV effort for RISC is considerable and even if it takes more time for them to get there.
-
Not all the features of RISC-V have been incorporated in the circuit, and they have patched some aspects of the RISC-V spec around memory management. Meaning that we cannot just take code and compile and prove it off-the-shelf either. This also weakens the narrative on “being integrated with mature tooling” as it requires maintaining a forked versions of the compilers of the source code. So, it is unlikely that we see 50 different languages being supported. There are also a security risk associated with potential bugs in the compilers.
Linea’s Prover relies on Vortex
Regarding the proof system. There is less convergence, but STARKs are the most popular solutions and have been adopted by StarkWare, ZkSync, SP1, RISC-0.
Other proof systems, such as Vortex, Plonky3 and Binius, position themselves in the family of STARK proof systems, and they have better theoretical performances. Although it is quite hard to compare proof systems (only RISC-0 and SP1 are running on ethproofs.org) as they are often optimised for varying hardware support, they offer the best performance. At the expense of worse verifier time.
A version of Vortex with the Koala Bear field has been released recently (not integrated in the stack yet), and benchmarks show that it can outcompete Plonky3 by 3x apple-to-apple for the commitment part (which is the part that matters).
The benchmark: Benchmarking Plonky3 vs. Vortex - HackMD
These benchmarks also allow us to estimate a performance boost anywhere between 30x to 300x in theory. This alone would bring Vortex’s prover up on track toward achieving real-time proving.
But in addition to Vortex, Linea Prover stack integrates a plurality of components:
- Arcane: a cryptographic compiler
- Wizard: a generic framework allowing unparallel flexibility for proof system design
- GKR: used as a side-car for several tasks. Mainly batch-proving hashes.
These have been developed and shaped by the problem we had been solving and each tool of the stack is optimal for the role it plays. This is by far the most sophisticated proof system in production.
Vision on the proposal of Vitalik
We understand the rationale behind this proposal as,
-
Emulating the EVM via RISC-V adds overheads, so we might as well directly run contracts over RISC-V to get better EVM perfs. Potentially amounting to a massive speed-up for simple operations. This would help the release of real-time provers.
-
Adoption of RISC-V is ossifying in the ZK community, and thus, it would accelerate and improve the enshrining of ZK protocols as part of Ethereum.
-
Simplifying the Ethereum Protocol to allow steadier additions of new execution layers features.
-
RISC-V is the most promising solution for FV, as there has been recent progress shared publicly.
But we believe the proposal does not address the following points
-
It reminds us of the eWASM effort, which was abandoned 5 years ago. Among other things, the concerns were static analysis, cost-metering, bug-surface and insufficient speed increase of the EVM. We do not see how the current proposal differs from that.
-
Regardless of the VM efficiency itself. A significant part of the EVM runtime for the prover are cryptographic operations. These are implemented using custom precompiles (e.g., compiled outside the RISC-V runtime environment). That means that there is an intrinsic bottleneck to how much we can increase performance by swapping the EVM for a more efficient one. We think the potential gain for the provers is around 2x or 5x. Still, it would help, but the benefits would be far from the 100x targeted.
-
We appreciate the perspective of cleaning the executing layer of the complexity and the quirks of the EVM but the migration of the old contract will still has a lot of unsized and undefined parts. For instance, about calling a contract from EVM context to RISC-V context. Because, of these “undefined yet” parts of the plan, we think the ideas need to mature a bit more before we can estimate if it will add or remove complexity in the end.
Whatever happens, Linea will remain aligned with Ethereum and we will pivot our tech toward RISC-V if the proposal gets adopted. In term of impact, we believe this is acceptable as (1) writing an arithmetization with RISC-V can be done without changing the prover and the tools used to write the aritmetization (2) the RISC-V architecture is simpler and more stable so it won’t take so much time implement it: we think less than a year. Especially if the high-level language is functional at this stage (3) the proposal will take years before being specified, implemented and deployed. So we have the time to pivot.
