# Proving EVM Bytecode Execution in the zk-EVM | Devcon Bogotá

- Channel: [Devcon](https://streameth.org/devcon)
- Date: 2023-10-07
- Duration: 24:37
- Watch: https://streameth.org/watch/yt-W2f_GLEtobo
- YouTube: https://www.youtube.com/watch?v=W2f_GLEtobo

## Description

Visit the https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on Swarm, IPFS and more.
https://archive.devcon.org/archive/watch/6/proving-evm-bytecode-execution-in-the-zk-evm/

Rollups are the go-to solution to scaling Ethereum and at the heart of the Ethereum roadmap. Programmable rollups and zk-evms have gathered a lot of attention and research interest. Provers in particular, which produce cryptographic proofs of evm execution, pose challenging problems both theoretically and practically. In this talk we will present our arithmetization and proving scheme, and demo the zk-evm under development at ConsenSys, providing an EVM bytecode compatible end to end solution.

Speaker(s): Olivier Bégassat, Franklin Delehelle
Skill level: Advanced
Track: Layer 2s
Keywords: zk-evm

Follow us: https://twitter.com/efdevcon, https://twitter.com/ethereum
Learn more about devcon: https://www.devcon.org/
Learn more about ethereum: https://ethereum.org/ 

Devcon is the Ethereum conference for developers, researchers, thinkers, and makers. 
Devcon 6 was held in Bogotá, Colombia on Oct 11 - 14, 2022.
Devcon is organized and presented by the Ethereum Foundation, with the support of our sponsors. To find out more, please visit https://ethereum.foundation/

## Transcript

Okay. Morning, everybody. Um I'm Aurelian, uh security and protocol dev at Optimism. Uh and this morning, I'm happy to introduce you to Oh, hang on. We have Franklin and Olivier from ConsenSys, who will be speaking to you about proving EVM bytecode execution in the ZK-EVM. Okay. Take it away, guys. Hello. Hello, everybody. Thank you for coming. Um so, yeah, we are both from the ZK- Sorry, from ConsenSys R&D. We've been working on a ZK-EVM pretty much for about a year. And in this talk, we want to talk to you about um its arithmeti- arithmetization, how we implemented it. And we'll have an announcement at the end. All right. Uh so, first of all, why ZK rollups? Um the screen is not working for me. Um well, in terms of scaling Ethereum, one of the bottlenecks that is addressed by a ZK rollup is that of the state. So, in order to validate the state transition, which is um you need to basically execute uh the transactions within a block. And the state is a big object, and this uh validation is a resource-intensive operation. So, the promise of a ZK rollup is to basically alleviate that workload from most of the nodes in the network. So, um when you have a ZK rollup, you have basically this powerful node, which is an operator, which provides proofs of state transitions. And uh these proofs typically verify the following: the validity of the transactions in the batch, uh the fact that the internal logic of the rollup is respected. Roll ups are usually application specific. And the fact that they induce uh the proposed state transition. And here and throughout, when we talk about proof, we talk about proofs of computational integrity, which in practice uh implemented as zero knowledge proofs. So, a ZK-EVM is a particular kind of a ZK roll up. Um the big distinction or the the thing that makes it a ZK-EVM is the logic part. The logic that is being executed or improved in the proof is the execution of the Ethereum Virtual Machine. It also means that the transactions uh that roll in pretty much obey the same format as standard L1 ins- uh instru- um transactions, sorry. Okay. So, um how does that work in concrete or semi-concrete terms? Well, you have your L2, which has a state, and um a bunch of transactions roll in. And they induce a or uh executing them induces a tran- transition of state. And the ZK-EVM basically plugs itself at this point. It extracts the required data from the previous state. It takes into account the transactions and basically the diff uh of the new state. And it does its magic and it produces uh traces, which it passes on to a prover, and the prover then produces a proof, which ends up on mainnet. And in this way, you bundle uh all of these L2 transactions into a single L1 transaction. So, um why would one want to build a ZK-EVM? There's two parts in this. There's the ZK and the EVM part. So, the EVM part um basically the advantages or the interesting parts is that it allows you to reuse or to use all the existing tooling which has been developed for L1. You can basically write in a ZK-EVM, write and deploy smart contracts on the on L2 just as though you were doing it on the L1. Furthermore, you can redeploy already deployed bytecode onto L2. And the ZK part in the ZKEVM, well, it gives you um the basically the scalability boost. And also finality, uh faster finality just because of the fact that there's a proof associated to it. So, that makes it interesting as well. Okay, when we set out on this project, uh we had a few goals. So, we wanted to be able to in our ZKEVM prove the execution of unadulterated native bytecode and respect the logic which is specified in the Ethereum yellow paper. We wanted uh full coverage of all the opcodes. Uh where we allowed ourselves to deviate is in terms of the representation of the state. And so, for instance, we will not be using Keccak. We are building a type 2 ZKEVM in the sense of the classification put forward by Vitalik. So, this project um um I'm sure you're aware presents a lot of challenges. Um there's a lot of complexity that comes from the EVM itself, uh which is composed of many parts which are tightly coupled and uh have complex interactions. There's a lot of intricacies that are really specificities of the EVM. Uh you have um families of opcodes that have slight um variations in their execution. Uh it's slightly non-uniformity. There's a completely different kind of challenge which is that of of auditability. So, Franklin will touch upon that um in his portion of the talk. And uh the main challenge which challenge which everybody faces today is that of performance. Uh efficient proving schemes um yes, and this is something we will communicate on uh at a further point. Today is really about the arithmetization. Okay, so here's basically the basic setup um of how it's going to work. Um you will have a modified Ethereum node and execution client which receives transactions sent by users or by dapps. We plug ourselves into this execution client and extract some data which we use to fill some traces. I'll be talking about traces later. And these preliminary traces are fed into this tool which we call Corset which does many things. Among them it is responsible for producing the constraint system. And it also expands and computes the remaining parts of the trace. All of this constraints and expanded traces are then fed into our inner proof system. The inner proof system we use is not compatible with Ethereum per se. So we have to feed it into a verifier which is a circuit over BN254. This is where we plug into with Gnark. And Gnark then produces the outer proof which is then posted on mainnet. Okay, let's talk about a bit about the arithmetization. So first of all, on Monday we published an updated and expanded version of the spec which is now a pretty hefty document. And its contents are basically the arithmetization oops of the EVM. So when we talk about arithmetization in this talk at least we mean to basically construct or write down a system of polynomial equations the simultaneous satisfaction of which perfectly encapsulates or captures a particular computation performed on particular set of inputs. For us the computations of interest are valid executions of the Ethereum virtual machine given a set of transactions and initial state. Okay, so since the EVM is a beast of complexity, it's a big thing. We basically need or it's it pays off to try to decouple as many of these components as we can to work in a modular fashion to sort of um concentrate the complexity in different places. So, this is the general architecture we have. We have the central piece, which we call the hub, which is basically our stack and our call stack. And then we have plenty of smaller modules that are tasked with doing specific kinds of operation, such as arithmetic or binary operations or storage. And I don't know if you can see it, but uh there's also the memory part. Okay, it doesn't work. The memory, which is this MMU and MMIO modules. Okay. And when you run uh the ZK VM, what do you get? Uh you get these traces that I was telling you about, which are these large matrices which contain data represented as field elements. There's one such trace per module. And each trace obeys its own internal constraint system. So, on the previous slide, uh you had these arrows which pointed uh from one module to another, and this is basically um connections uh period cup connections, which allow us to transport data from one place to another. The other kinds of constraints are basically the internal constraints. So, for instance, when you update the program counter, you expect something particular to happen. But you also have another kind of constraint, which is uh sort of global constraints, global consistency constraints, which range over the entirety of the block rather than two or three consecutive rows. And that, for instance, may express properties such as that well, when you re-enter an execution context and you load something from RAM, you get what you last put there. So, let's zoom in a bit on this central piece, the hub, which is our as I said, our stack and our call stack. It gets its instruction from the ROM. And what it does when it's once it has an instruction is to basically dispatch this instruction where it makes sense. Once it has an instruction that it loads from ROM, it first does some preliminary decomposition of that instruction. It extracts some parameters, which are hard-coded. And it decides on certain things, such as how to interact with the stack, how much data to excavate from the stack and where to put it in the in the trace, the layout basically of the data. It also raises uh some module flags, etc. And uh the next step is then uh to dispatch the instruction. But before we can go there, we actually have to deal with potential exceptions. And the the hub also deals with the exceptions. It's basically some of them it can detect, others it imports from other modules. And if an opcode makes it past this hurdle, uh then you have the instruction dispatching per se, which um kicks in, and you have these flags, these activation bits that light up, and you have some stamps that are updated because you need to keep track of temporality. Yeah, at this point these activation flags, well well, they tell you what will be active. So, for instance, in when you do a create, you will be touching RAM, so you'll be touching those two modules, uh MMU and MMIO. You will also be touching ROM because you'll be deploying initialization code, and you will touch gas and memory expansion. And same thing for create two, but since there's a larger hash involved for the initialization code, you tap into some hash modules. Okay, so let's talk about about the next big piece, which is RAM. So, RAM is probably the most complex piece in our arithmetization. By the way, all the figures that I put here are available in the document. Um and some of the Well, one reason why it is so complex is that it has all these um data uh stores with with which it can interact. Um and the different instructions uh which interact with RAM actually have uh different sources and targets. So, there there's already some first complexity. The next source of complexity comes from the fact that operations which are atomic from the point of view of the EVM, such as returns or creates, have to be broken down into smaller elementary operations in the ZK-EVM. And so, the first task is task is basically do a lot of off offset computation and deciding when some padding has to be done, this sort of stuff. And once all of this has been decided, well, you can start writing instructions. And this is still just writing them without executing anything. You just have this sort of workflow that tells you in this case I need to do this and that, some XRAM slide chunk or something. And once you're at this point, you are at the phase where you can actually start doing something. So, this is the the work of the MMIO, which is the the actual RAM in a in a sense. This is the the component that touches data and that actually does um the sort of byte decompositions, recombinations, slicing, dicing, surgeries, etc. And then you have these consistency checks that I told you earlier about, which is basically finishing the the memory part. Basically, what you've written last is what you should retrieve next time. So, I'll stop here for the arithmetization. I'll hand it off to Frankland. So, thank you for the this very extensive description of what is a constraint system on the arithmetization. And now, I'm going to talk to you about this comeback. Thank you. I'm going to talk to you about how to go from this well, let's say, conceptual data to how we actually implement the whole thing. There is a lot of challenges when we want to go from the specification to the implementation. And the most be with the biggest one is that there are three moving parts. On the one on we have the actual specification, 250 pages. Then we have the implementation of the specification. And then finally, we have the proof system of the verification of the of the traces. So, all of these stuff is developed by different people working on different teams. We still need to maintain 100% conformity between all of these pieces. So, of course, if the prover is proving something else than what the spec is describing, which is itself something else than what is actually implemented, nothing will work. And finally, it's hard to hold it three diverging code bases or three diverging sources of data. So, what kind of solution did we find? We developed a formalized single source of truth, which is then exported to multiple targets. So, what happened is that we have in some format that I will show you in a in a few seconds, a description of all of these constraint system. And from this single source of data, we are able to produce first uh Go library defining the constraints on the data that will be in the that will then be used by the prover to to actually prove stuff. Then we have another Go library that is used by the ZK-VM implementation to ensure conformity with the specification. And finally, we can generate LaTeX data for integration within the final specification document on the 215 pages of of PDF. So, here is how it looks. So, you can see that this is a very clearly uh Lisp-inspired languages with a lot of parentheses or other kind of stuff. And this is a very simplified example of what you could find, for example, in all of the MMU. So, what do we have in this? First, we have the column definition. Those are like the columns of the matrices that Olivier showed you a few minutes ago. And you can see that they are they can either be normal, like the one at the top, or they can be uh we have a very rough typing system type system that is used for some optimization. And finally, for the pure pure uh ease of implementation and ease of use, we have some kind of very simple arrays, that kind of stuff. So, yeah. Afterward, uh you have helper functions, which are functions that can be well defined like any other Lisp function to uh act on this data. And for instance, here, you have two functions. The first one is checking that two arrays of length eight are actually element-wise equal one to the other. And the other one is computing the we're checking that an array of eight elements is actually a byte decomposition of a given value. So, those do these do not really exist per se, but they are just like smaller syntactic sugar for the ease of implementation. And finally, we have the the meat of the the meat of the data, which is the constraints themselves. So, here we have an example of two three constraints. So, the first one is doing a body composition of some data. The other one is checking the memory is aligned and so on and so on. And from this, we will run it through courses that um Olivier evoked a few minutes ago. And Corset will do quite a few things. And among other, it will for instance generate a lot of go code for the prover that code you can see here. And you can imagine how writing this by hand would be a living nightmare. Or we can also generate LaTeX. So, here you have for instance a a piece of piece of LaTeX code on the PDF renderings that is ready to be incorporated in the spec. So, this whole stuff that we call Corset is really a cornerstone in our work workflow on the our implementation of the ZK-EVM. Now, I will talk to you about some results that we have reached from our from the specification to the implementation to the actual results. So, the first thing we want to benchmark our implementation against is the EVM test suite, of course. The EVM test suite is a golden standard for Ethereum clients, including but not not restricted to the EVM itself. So, we have tested our current implementation of the ZK-EVM, which is well advanced but not yet finished. So, for now, you see here the list of modules that are ready. So, we have the hub, the MMU, the ROM, the ALU, the binary, and some comparator functions. And on over 17,000 tests, we run our EVM on these, and 16,000 are success. So, it means that it runs and the traces are validated. Zero are failing, so it means that we do not have any problem handling this this this test. And finally, we have 1,303, which are hitting functions that are not implemented in the in the EVM in the ZK EVM, namely in this case, the precompiled contracts and the self-destruct operation. So, for now, we have a 92.6% success rate on the EVM test suite, which is we believe a good start. Another way to test and to benchmark our implementation is of course to work on real data, right? So, we have a quite a few real-world examples, but the most striking one we have is I believe the successful execution validation of proof of exemptions using the Uniswap contract and the successful execution and validation of random mainnet block. So, what we do is that we run our Ethereum client on the mainnet and we generate traces for some blocks there and there and then we validate all of the constraints. So, I will show you a little bit how this work. We are going to check the verifications of the constraint of the on the traces we generated for this block 0x35b7e90, blah blah blah. This block was created yesterday in the afternoon. So, let us start and while it is working, I will show you a little bit of what is in this block. So, here is the data on Etherscan of this block. Uh as you can see, it is like 23 hours old. We have quite a lot of different transaction in it. So, we have a basic transfer transaction. We have a some wrapped stuff. We have some multi-call. We have failing transaction. We have successful transaction. We have Uniswap. We have Tether. So, it's quite a nice example. It's not a very big block. It has only 52 transactions if I remember correctly and it's only using 2 million gas on the half, but it it is still quite quite inclusive in what it what it provides. If we take a quick look at the traces that we generate for this block. So, here you have a decomposition of all of the data that we generate for this block. So, on the very big red stuff at the top of the screen, you can see that in the end we generate let's say 13 13 and a half million of cells, so which is like the actual content of the traces. You can see that the biggest one are the binary with 2.5 million of cells. Then you have the ROM Well, sorry, the ROM first with 5 millions, then the binary with 2 million and a half, the hub, which is also before the binary, sorry, with 3 millions. And all of that is culminating into 13 million of cells that have to be proved and checked and then cryptographically checked. So, here we can see that Cosette is actually doing a very naive check of all of this because it will basically just run all of the numeric numeric constraints that we define on all of the lines and rows of the matrix one by one, which is obviously very suboptimal, absolutely not cryptographic, but it's either debugging tool that I show you for to to prove you that our stuff is still working. And as you can see, the validation is successful and the block 0x 35B is actually validated with all our constraints and our EVM will be able to give all of this data to the prover and the prover will be able to generate the proof and put it on the main chain. Now, going back to the to the presentation. So, sorry, I can't play because no Wi-Fi, so you will have the development version. So, in conclusion, the complexity of the EVM implementation has been partially solved with modules, well, completely solved with modules. The intricacies of the EVM Maybe Olivier, you want to say something about this? Um yeah, so in terms of basically finalizing the arithmetization, we have two big two big chunks that are still left to be done. Um but um we are quite confident that we'll be done um basically for the testnet. Regarding the auditability, we are we have we don't have yet an audit or formal verification of what we have done, but who thanks to our single source of truth mechanism, we have laid the groundwork to actually be able to work on that on prove in a single strike all of the success all of the the three components with a a single single audit. And finally, regarding performances, we are now connected to the prover system and there will be more more information regarding that soon on the in a in a coming paper. So, thank you for your attention. We will be launching a testnet soon. So, if you want to join, please just scan this stuff or just go to the to the URL. And if you have any questions, then we will be happy to take them. Can you just give a high-level overview of of the differences between your implementation and the current other uh ZK EVMs such as uh from Scroll and and Polygon, etc.? I don't know exactly the inner workings of Hermes and Scroll. Um I I know that we share some design principles with both. Um I know that our prover will be different. Um our arithmetization is also going to be very different. And um I think this probably represents actually a strength overall, not for us in particular, but for the ZK EVM ecosystem as a whole. Keeping in line with this multi-ZK EVM prover future that Vitalik has been talking about. Um But um in terms of concrete details, um I'm I'm not quite aware. Oh, regarding concrete details, uh the big difference with Scroll is uh let's say the arithmetization method that they are they are the both of us are using different methods and we will see which one will sustain the test of time. On regarding the difference with Polygon Hermes, the main difference is that Polygon, contrary to us, doesn't directly works on EVM bytecode, but they first translate the EVM byte code into another byte code that is running not on the EVM but on ad-hoc register machine, which is then proved. So, there is a supplementary step that neither Scroll nor we do do have. What are the opcodes that have been the most difficult to implement in the zkEVM? Um you may be surprised, but call data load has been horrible. You would expect if you do if you can do a M load, you can do a call data load, but in the way that we arithmetize things, it's actually quite difficult because of the provenance of the data and the fact that there's some padding involved. Um but in terms of the real complexity, the real complexity is actually for anything that involves writing a whole lot of data with padding potentially. So, anything such as code copy, x code copy, I don't know. Um Yeah, basically these kinds of opcodes have been the most complex. And if you look at the arithmetization about MMIO, there's literally pages upon pages of I'm defining in we're defining nibble nibble seven and bit eight and they have to interact in some complex way. Um memory has been the the worst.