The road less travelled: 4 years of direct arithmetization of the EVM

Transcript

Okay. Good morning. Hello, I should say. My name is Olivier. I'm with Linera and ConsenSys. Um, and I'll be telling you about, um, yeah, the sort of 4 years that we spent on directly arithmeticizing the EVM, but also the future of Linera. Uh, which is going to be on risk-5. Um, is this a clicker? All right, so a quick quick recap.

Um, Linera is one of the original, uh, ZK EVM projects. It is a type two ZK EVM. Um, uh, it is, uh, uh, essentially unique, I believe, in that space, um, in being a ZK EVM rather than being a risk-5 ZK EVM. One of its defining features is that the lattice behind Linera is, uh, sorry, the cryptography behind Linera is lattice-based, it runs on CPUs, and it provides 128 bits of security. And for everything precompiled and other, uh, portions of the arithmetization, we'll we rely on Gnoark circuits.

Um, I'll also give a quick recap of the sort of history. As I said, we started relatively early on in late 2021 as an R&D project within ConsenSys. Um, we left R&D and became a product in early 2023, and by summer of that year, we had launched our mainnet, uh, running, uh, the London EVM, but at that point not being fully proven. And we bridged that gap in 2025, early 2025, when we, uh, were able to deploy the 100% proven uh, upgrade to the um, mainnet.

And that also started our sprint toward catching up because at that point we were still running the London EVM and we targeted the Osaka release which happened in December. And we hit that date releasing simultaneously on Osaka, sorry, on mainnet and on Linea mainnet that network upgrade. That brings us to 2026, so the current point in time. We had to perform a couple of extra non-trivial upgrades to the network, one of which was was including EIP 7702.

The other one, both of which I'll come back to, the other one being sort of modifying the underlying base field of the arithmetization. But most importantly for that talk, it gave us time to reassess and to sort of recalibrate. And we decided internally earlier that year that we would be doing a radical pivot from the direct arithmetization of the Ethereum Virtual Machine pivoting towards arithmetizing RISC-V as has become the industry standard. So, let me walk through what it took to building the ZK VM, also the rationals behind building a ZK EVM rather than a ZK VM.

Initially the idea was that arithmetizing the EVM directly would have plenty of benefits. There would be no extra compilation or transpilation step. You would be proving directly the execution of native unadulterated EVM bytecode just as it is as it is deployed on any Ethereum compatible chain. You would also gain a certain amount of control over trace sizes, complexity of the constraints, number of cells required to deal with any one up code. Um obviously you would have to deal with uh what comes with arithmetizing the EVM.

That is to say an incredible amount of complexity. You have to deal with all kinds of state, semi-permanent or not, like machine state gas gas mechanics, etc. The crude state, all sorts of things around warmth and self-destruct sets and but also the EVM state itself, so accounts, storage slots. And then all the nastiness that comes from the complex opcode semantics of the EVM and rollbacks and exceptional haltings and deployments and various transaction types and system transactions etc.

So miraculously, I would say to some extent, this project succeeded. It amounted in an enormous amount of complexity. Our specification takes more than 1,000 pages at this point and it's final. And yeah, so it was in some sense it was a six succession of miracles. The fact the fact that we even got to the fully proven London EVM, which took towering 3 years, was in some sense a miracle. The fact that we got to the Osaka upgrade in time was all itself a kind of a minor miracle and that was driven mainly by partner requests that needed support for various

opcodes and transaction types. Um I should also mention that another sort of minor miracle that we were able to pull off and which I'll come back to later was what I alluded to earlier, the switch of the underlying field of the arithmetization. So that was also a long time in the works and it was not at all obvious that this would work. It was done mainly for performance reasons, even though for various reasons like the uh of so-called legacy constraints that are not field agnostic.

Um these gains in performance were somehow somewhat offset by the sort of um deluge of new columns and constraints to sort of reinterpret old constraints. And this was a massive effort which um uh occupied essentially, I want to say like 15 to 20 people full-time for a few years. But at this point we've sort of uh reached a uh tipping point as I said we've had time to reflect.

And uh our goals were met. And uh it's time to sort of um reassess whether that direction is viable in the long term. So uh I'll be telling you some of the lessons that we learned from arithmetizing the EVM well, carrying out this project over the span of 4 years. And what we hope to uh bring to this new direction we're going into which is uh the risk 5 path. So, I'll be talking about several topics. Uh I don't know to what extent I'll probably cover everything I imagine. I have 20 minutes, it should be fine.

Um but uh here are a few of the sort of highlights that uh I want to address. There's what I already mentioned, the sort of presence of uh or the coexistence of legacy constraints and sort of higher-level constraints that emerge later on. Um also with respect to formal verification, the sort of um intertwined nature of these legacy constraints being a blocker. Um I want to re- to go back over this idea that um having handwritten constraints and having constraints that directly arithmetize EVM the EVM itself would give you tight control over traces and cell cell count.

I'll also mention a few of the optimizations that we thought were optimizations that we did at the time that ended up having ripple effects that were unforeseen at that point. And which yeah, which I'll come back to. And then another important thing I'll mention is how that sort of was also a problem towards parallelization, which is one of our current goals. And obviously the difficulty of managing hard forks, which I've already alluded to but So, legacy constraints were the original language in which we wrote our ZK-EVM.

Initially, they were relatively primitive. We had opinion made opinionated choices about the underlying field that would support our arithmetization. And in particular, it was a very large field and the sort of native unit in which we could express constraints related to the EVM was like having basically having field elements contain up to uint128s. Those choices were reflected directly in the constraints themselves. And we had no common abstraction for the sort of splitting of EVM words, which are typically well, which are natively uint256s.

So, a lot of complexity and a sort of um variety of dealing with with the splitting emerged and we had to on top of the EVM test suite itself write thousands upon thousands of tests, a great number of which were which were related to the splitting alone. And this was one of the sort of hindsight that we the insights we got relatively early on and that um motivated us to develop a higher level language, which was that it would be it's in some sense necessary to hide the implementation details between behind layers of abstractions, especially when writing such a complex

system as a ZK-VM. Um another point is that uh this sort of um uh lack of abstraction um was a hindrance, a real hindrance towards uh formal verification. And in particular, our constraints are not differentiating between constraints that are sort of dictating the shape and the overall um scaffolding of modules and constraints that are there to really catch the semantics or the intent of modules.

And this resulted in basically a very complicated uh system of constraints for any formal verification system to attempt to verify. We made attempts at it and uh we found that basically the the modules written in the sort of new language and a higher abstraction level language were well, uh they were relatively straightforward if not straightforward uh to to prove formal verification to perform formal verification on and prove determinacy, but everything that we had done and which uh actually contained most of the complexity of the system so everything we'd done by hand uh was basically a no-go with respect to formal verification.

Even such a module such as the one responsible for carrying out the uh jump destination analysis in bytecode proved too difficult for a pilot project that we did with uh Veridise and they tried. Um yes, I may skip that slide, uh but another thing that we found is that okay, while uh it is very nice to have granular control over how we perform opcode operations and most of the opcodes fit into the sort of mold of occupying a very limited scope of rows in any trace we found that there were some outliers and these outliers typically related to halting instructions or calls concentrated an immense amount of complexity.

Uh some of the worst offenders are like calls to precompiles that trigger various success or revert scenarios. And this was a complexity that was just that was concentrated in the biggest module in the most uh sort of central module, which we uh have not tried to convert to uh ZK ASM at that point. All right. On a different note, um uh we did initially several choices that seemed like smart choices, optimization choices.

For instance, in how we uh structured memory. The EVM memory is a um EVM word indexed byte array. Um de facto, it is much smaller because you have memory expansion cost, so you can't really access memory beyond, let's say, 4 billion bytes. Uh and since we had this sort of um uh uh basic uh our sort of basic type was the were these uint128s. And those were the objects we were manipulating on the stack, for instance, uh of the EVM. We thought it would be uh a good idea, or I thought it would be a good idea, to sort of um structure the memory accordingly. And rather than

having a an array of bytes, having an having an array of these uint128s, which in the end prove is equivalent, but it introduced all kinds of um difficult uh constraints around how to sort of um perform surgery on words when you want to do uh copies and and writes into memory. So, one of those hindsights that we gained from that is that the I mean, dealing with everything uniformly, um and not having these uh all kinds of edge edge cases that appear from these optimizations, while being maybe less optimal in the short term actually pays off in simplicity and maintainability down road

down the road. Uh similarly and I'll skip quickly over this one but I already mentioned call instructions were an absolute nightmare. They were very difficult because of this inherent complexity and the way in which they can fail ahead of execution and they can fail during execution and they can be reverted uh and all of these things interacting non-trivially one with one another with one another. Um an optimization which we thought was one at the time which we uh sort of um uh which crystallized very early was that we would have distinction between calling externally on the accounts and smart contracts.

Um the problem with that is that this uh uh was in line for instance with the way Besu uh deals with um uh these calls where when the target account is empty code it performs a different sort of um call than if it has non-empty code. That was very nice but it clashed immediately or it it had a negative effects when it uh came to merging the EIP-7702 constraints into the system. And it actually added a lot of complexity to that to that upgrade.

So uniformity not only is a sort of a simpler but it's also more easy to upgrade. Something we uh that wasn't uh much of an issue initially was getting I mean it it was known that we would have to strive for very high performance. But it wasn't clear initially that parallelization of the tracing would be one of the ways in which we would achieve this. Internally in the constraint system we have all kinds of data structure struct structures that are very that are tailor-made to be able to accommodate for the words.

And the way this is implemented in constraints requires the availability of an of global information, so-called information that only becomes present or becomes known at a future point in time. So, these present knowledge of future events sort of mechanisms we have implemented all over the place. And that was in some sense one of the biggest sins we did with respect to wanting to parallelize stuff. Because you cannot delegate the tracing of a certain chunk of the trace unless you have knowledge of those future events, which require tracing the entirety of the trace.

So, this is really a peculiarity of implement or arithmetizing the EVM because of its rollback mechanism in particular. Yes and I guess what we learned from that is that if we if we want to target performance, we must target something that is immediately amenable to parallelization. And that has as little as possible non-local information needed to carry out this parallelization.

Um another sort of bright idea that we had or that I had, I should say, was that we should merge somehow the Ethereum state with the accrued state of the execution. Um this in some sense was a sort of a a measure to reduce the size of the traces, and on that front it worked. Um but it introduced problems with connecting to other components, in particular to our state management system or service Shamay, but also the underlying execution client base that you're using that we're using.

And moreover, if we look into the future and um the Glamsterdam update, this directly clashes with the the block access lists uh uh EIP where a certain order in which you want to perform certain checks before you actually do any state accesses is enforced. And the order that they chose does not correspond to the one that we chose in many cases. So, this in some sense implementation detail became a choice that had we gone to Amsterdam, we would have had a lot of difficulty sort of um uh changing.

Yes, and I already mentioned, I mean, EVM hard forks are going to be difficult if you're doing a ZK EVM. Uh we saw this very recently with the EIP 7702 stuff. But, we dodged, to be honest, a big bullet early on, uh which is EOF V1. And I say this not as a critique of this set of EIPs, but just from the pure arithmetization point of view, uh this would have been quite difficult for us to handle because of all the sort of opcode semantic changes that it introduced and the new way of sort of dealing with deployments etc.

and the pre-analysis of bytecode that you're going to deploy. All right. So, the sort of main uh insight that all of this points to is that it's easier to choose a static target if you're going to arithmetize it. RISC-V being one of these static targets. All right. So, now that I've sort of um critiqued our past, I've sung its praises, but also critiqued it quite harshly. What is the future for Linar?

Well, uh as I said, we weighed the pros and cons of the direct arithmetization approach of the EVM. The conclusion is that we are going to be transitioning to RISC-V, as already mentioned. Uh for the reasons that I said, stability and simplicity, essentially. We don't have to deal with the continuous evolution of the EVM. RISC-V is a very simple and stable platform. Furthermore, uh we have the tools and we are developing uh more tools to integrate from the get-go with formal verification.

There will be no more legacy constraints that we have to somehow port to different arithmetizations. Everything will be done in a high-level programming language um that incorporates these abstractions and deals with the constraint generation in the background. And obviously, our goal is to both contribute and benefit from the formal verification efforts that the ecosystem is undertaking on the RISC-V front. And I think that's it. Thank you very much.

Do you have some questions, maybe? Yeah, one question. One one question. Hey Olivier. Um so, it seems like the um the underlying theme here is decisions that were made early on that you know, it's often the case in a big project that it's that you you know, make choices early on that that you come back to want to change, right? But the challenge, it seems anyway, the challenge is that that the undoing those design decisions was very difficult and that it sort of left you in a difficult position. Is that fair?

Yes. It is fair and so we we as as you know, we could have chosen alternative paths. We could have gone with ZK simplifying the entire existing stack and continuing on the ZK EVM path. But ditching everything that is legacy and at some point even ditching ZK assembly since we don't need the sort of reinterpretation of legacy constraints. That is definitely one option that we could have gone down. Along but it several reasons why we didn't choose it. First of all, it doesn't solve the hardfork problem, not really.

It requires maintaining a client that runs in parallel of Besu. Also, it still puts us at odds with the sort of general direction of the ecosystem in particular the direction set by the foundation. Okay, thank you so much. Give a great applause.