Lightning Talk: Autoprecompiles: Compiler-Based Acceleration for zkVMs by Leo Alt, powdr

Transcript

Sounds good. >> Yeah, thanks Will. >> Leo from Powder talking about auto pre-ompiles, compiler based acceleration for ZKVMs. >> Thanks Will for the intro and for the great work on it proofs and this event. Um ZKVM pre-ompiles [snorts] are fundamental for the performance of ZKVMs. However, they are quite difficult to um write, read, audit, proof correctness off and scale. Um, it's not sustainable to handw write these massively complex circuits every time you want to accelerate a gas program.

Um, this is not a Thanks, Alex. It's not a sustainable uh design for ZKVMs. So, wouldn't it be great if some form of gas acceleration happened automatically? Um this is already happening. Auto pre-ompiles are automatically synthesized um circuits. This is not some futuristic out of reach um research we're speculating on. This is something we have code for that works right now and already improves a few major ZVMs. This is obviously a very deep complex topic. This is a short talk. So feel free to reach out with questions or find me later if you have deeper technical questions.

These circuits aka pre-ompiles they are generated from the program's basic blocks using old and new techniques such as profile gut optimization hot path analysis something we call hot witness analysis we don't really call it that but for the purpose of this slide I call this this and we're also working on new/ old techniques like branch prediction analysis these kind of things that has been common in the hardware world and seems to apply quite well to zms as After these circuits are generated by a very simple process, they are extremely heavily optimized by lots of optimizers we have in the powder code base such as static analysis, um compile time

constraint solving, loaded grip level substitution and lots of other super interesting techniques. As the name suggests, this is of course fully automated. It is ISA agnostic. We currently work mostly on risk 5, but it is ISA agnostic and it already has comparable performance to handwritten pre-ompiles as you're about to see and the security also scales a lot better than handwritten pre-ompiles. Other pre-mpiles are fully integrated into OpenVM, one of the main ZKVMs out there. Um, already doing real-time proofs on Ethereum. This is a bench a reference benchmark we run often to test the current state of our of the powder auto pre-ompiles. This benchmark does catch or 10,000 iterations of catchack.

And we have three settings here. The pure software version which just uses the tiny catchak rust library. It's just doing catchak in rust. No pre-ompiles involved. And it takes about 800 something seconds to prove it on a certain CPU. Um if we use the handwritten pre-ompile that comes with OpenVM, we get a 10x acceleration which is obviously very very good. Um but if you use auto pre-ompiles, we actually get even more acceleration, 11 times faster than the software version. And so 1.2 times faster than the handwritten pre-ompile. Actually, if we use this for Ethereum, we're not necessarily interested in replacing the pre-ompiles that are already there because they are very performant. So we want to use the current software version

plus handwritten pre-ompiles that are already there proving Ethereum and this is um the proof time for some run and you can see that as we add new or more auto pre-ompiles, it gets faster and faster. So currently with OpenGVM plus 100 auto pre-ompiles, we got 1.37 times faster end to end proofs including recursion. Um it's important to mention recursion here because in the current way that a lot of ZKVMs and provers are written, there is quite a big penalty for having a lot of circuits or a lot of pre-ompiles in the ZKVM for a certain guest. Um because the verifier is linear in the amount of columns. It goes into details but the more auto pre-ompiles you have the more penalty you're paying

off in the recussion layer. So it it ends up being u being a lot slower but we already get this acceleration even including recursion. So as more provers maybe move into multilinear settings uh this will get uh faster and faster with this. We have uh integrated power NVM on it proofs as of last week. Um which is great to compare to the state-of-the-art ZKVMs um and be be part of this this race and test our own optimizations with time. What's also interesting is what's after this? What can we improve on now? So as I mentioned just now, recursion has a pretty big penalty on this. But let's say recursion is solved. Not a problem

anymore. What can we do? How many auto pre-ompiles can we use? Well, if we use even more 500 or 1,000 auto pre-ompiles and we consider only what NGM calls app proofs. So, this is before recursion starts, we actually got almost 2x um faster proofs already. Um, so if we can actually do even more, so if we could accelerate all the 13,000 plus risk 5 basic blocks that the RET um client has, usually 80% of the trade cells that are in risk 5 right now would simply vanish.

So you can maybe see where I'm going with this. Um, this is some analysis that we do often in our benchmarks, which is what's the effectiveness of an auto pre-ompile. So each risk 5 basic block becomes an auto pre-ompile and not all of them are used because of of current restrictions on approvers. But we we know what the effectiveness of an auto pre-ompile is. Meaning how many like fewer trace cells do we use if we use that the approver has to commit to if we use an auto pre-ompile instead of a risk 5 basic block. So after our new optimizers integration or testing the last two weeks, we actually seen almost seven times average exploration per basic block in the RAF benchmark.

This is also a pretty fun stat. In some basic blocks in the RAF benchmark, we actually see up to 20 22 21 22 times improvements when you take a risk 5 basic block and transform it into um into a circuit. And interestingly the EVM interpreter code implementing the op codes later uh less than and greater than for the EVM are actually among such basic blocks that are accelerated almost 21 times when you make a circuit for it. Of course a lot of people ask um how are we going to secure all of this? You can possibly pay enough people to audit and verify this manually as the whole thing is automatic. We also want to do automatic formal verification. So we

have two projects going on. One is our own uh lane four rewrite of the optimizer. We want to have uh fully um pro like correct by construction prover where which you can prove in lane 4 and then a verified checker as well that can check when auto pre-ompiles are um generated. We also have a project with the foundation serora to use SMT based approaches to prove that every single generated auto pre-ompile is semantically equivalent to the risk 5 basic block that it came from. This of course um also propagates to different ZKVMs and S31 HyperCube has an initial integration with auto pre-ompiles that already shows almost uh twice as fast proofs.

Um to finalize I wanted to note that auto pre-ompiles are not just a potential replacement for the pre-ompiles we have now in Ethereum. They're also not just a tool to accelerate Ethereum. um they can be used for any guest to accelerate any basic block that we're not even aware that they could or should be accelerated. Um auto break compilers are bridging the gap between ZKVMs and ZK circuits. They are basically removing the ZKVM overhead and bringing ZK bringing the performance of ZK circuits to ZKVMs while keeping the best UX and effects that we already have from ZKVMS. Thank you.

>> [applause] >> All right, thanks Le. We've got a couple questions here. I I think perhaps you answered the first one. Uh I'll restate it just in case. Can you give a brief overview of how you plan to formally verify your optimization passes? What spec do you do you compare against? Yeah. So the most realistic for now, let me go back to this is so every auto pre-ompile generated from a risk 5 basic block from the instructions in that basic block and the circuits that verify those instructions. So the first idea here is to take the optimized circuit after all the optimizations and prove that the behavior is semantically equivalent to the risk 5 basic block where it came from. So as long as the original ZKVM is formally verified, we

keep the same level of security with auto pre-ompiles as well. We don't reduce levels of security of the ZKVM itself. Um the other approach the more long-term approach which is we are writing the optimizer in the whole process in lane 4 as well so that we can have proof of correctness of the whole algorithm of the whole codebase um and not just prove auto pre-ompiles as they come out. Hope that makes sense. >> Great. Uh last question. Uh how did you go about defining defining a basic block or is it dynamic?

>> Um a basic block is pretty easy to identify. If you look at risk 5 assembly code or most assembly code, you'll have branching instructions, jump instructions, a basic block is basically a a nonbranching sequence of instructions that ends in a branching instruction. So this is is pretty um is pretty identifiable from from compiler generated code. Awesome. >> Thanks very much, Leah. >> Thank you. [applause]