I like the idea of exploring changes in the EVM to make it more provable.
As for the performances, I understand implicitly the proposal as splitting the EVM in two parts. The first part is a kernel controlling the “sensitive” operations (e.g. handling the state accesses, creating the execution contexts for every calls and subcalls, doing the reverts etc…) and the second part is a free RISC5 interpreter that can be used by the contracts. I am confident it would allow massive saving for use-cases like Fibonacci, doing heavy integer arithmetic and almost no kernel calls. But for actual workload, most of the gas spending is done by doing cryptography operations and storage access. I am also concerned that switching a lot between kernel and user mode may have a non-negligible cost. So, even in a world where every contract has migrated to the RISC5 version of the EVM, the prover runtime savings I see would be well under the objective of 50x.
For similar reasons, I wouldn’t suggest moving to more ZK-friendly ISAs because they would not address the above problem and would also come with the issues of young developer ecosystems. If the target of 100x is important, it would have to be combined with an effective way to optimize the precompiles and the kernel operations and this will require more aggressive solutions. Direct arithmetization, combined with in-depth proof-system engineering (for the precompiles), is a more promising way to get there. This is the path we have been taking at Linea and unlike many, we have no plan to switch to a pure RISC-V approach.
And even then, all the benefits would be negated if the retro-compatibility entails maintaining the old EVM beside the RISC5 one. If the actual driver and primary goal of the proposal is to move away from the current EVM while maintaining ZK-friendliness, then it is understandable. But then, I also have concerns/questions with the proposed approaches.
- Side-by-side environments: I worry about these temporary solutions that end up lasting forever and adding a lot complexity to the overall system.
- Transpiling on the fly the legacy bytecode. This will require figuring out a transpilation algorithm that guarantees that the contracts always behave in the same way after transpilation. It’s not very clear to me how this would work; would it just expand the “EVM” handling of every opcode into RISC5 code?
- Multiple execution environments: If we want this to unfold in a way that does not worsen the Eth fragmentation and maintain prover-friendliness, it means we will have to work out a standard way to allow contracts to call each other through different execution environments. For the provers, this corresponds to emulating multiple VMs. I can see how this could make developing on Ethereum more attractive but it also means that the prover complexity will increase even more.
To conclude, I stress that formal verification of zk-EVMs is years away from being L1-ready. I fully appreciate all the steady progress that is being and has been made in the RISC5 ecosystem toward formally verifying the arithmetization of RISC5. However, I think the speed of the progress (vs direct arithmetization) is mainly due to the simplicity of the RISC5 VM, and I’d add that the FV analysis of a RISC5 approach also needs to cover FV-ing the compiler suites. This part is a completely different beast. Taking this into account, contrary to the current popular belief, I don’t think direct arithmetization is that much worse off than RISC5 for FV.
Multiprovers and L2 fallback mechanisms are currently the only short-to-medium-term solution to have fully production-ready ZK systems on-chain.