Leo Alt of powdr labs @ ZK Hack Meetup in Berlin, 24 Apr 2025

Transcript

[Music] All right. Hi everyone, my name is Leo. Um, I work on powder which is primarily an SDK for ZKVMs. And with that we've built powder VM which is a risk 5 based zikkVM but there's a lot more interesting thing interesting things happening in in the powder SDKs. So the the front end is flexible that you can plug in different instructions architectures risk 5 was different

things. You can also plug in different backends. Um right now there's like hello 2, plunky 3 um and two and but the main thing I'm going to talk about today is one of the compiler techniques we have in the middle of the whole workflow which is automatic automatic synthesis of pre-ompiles. And this happens um basically before going to the to the ZK proof. So this is a technical talk. So it would be great if everyone is already deeply familiar with internals of ZKVMs. Yes. Give me five seconds.

Um yeah. So this we first wrote about this technique in um in a blog post. If you want to read more in text forum um it's there. But this I think was published last year. I actually don't remember. So there's probably more information like more updated information in this talk even though you'll find more information in general in the blog post. So the main topic here is pre-ompiles or co-processors or acceleration circuits or whichever name people give to it. So in ZKVMs it's really important to have this idea of pre-ompiles which is circuits that you build by hand to

replace computation that's expensive when you come from software. So if you have a Rust program that uses tiny catch library, it's a software library that computes catch that's going to use a lot of CPU cycles, a lot of risk 5 or was them whatever cycles to compute catch. And um if you want and that's going to dominate the the cost of your proof. So if you want to make that faster, you'd write a manual circuit that computes Ketchup with hopefully fewer resources than the CPU like your VM would take um to compute catchup in the software form which consists of a bunch of generic instructions.

And if you take Ethereum for example, there's a lot of um different things you want to accelerate to make it even possible to prove um like Ethereum blocks for example in reasonable time and these would be for example catchda SHA and BN254 operations because these would be very very expensive if you compute them just in software and you let the VM take care of them. So this is for example what um the beginning of the software catch up um permutation looks like in risk 5. So there's a lot of generic instructions there's like adds ends exor shifts the whole thing is going to be dominated by

exor and shifts and this is only the beginning. There's actually almost 700 instructions to compute ketchup. So it's a lot of code to do this this computation. So you see there's a label up there and this whole block is going to end in a branching instruction and this is what we call a basic block. So you have a linear path all the way to the end and at the end you can also just continue from there but you have like somewhere where you want to stop and when you have a pre-ompile what you want to do is basically replace this whole thing here by one instruction.

And what this one instruction is going to do is all of that not in the same way, not using the same amount of resources, but the results going to be the same. So if before that block your memory had a certain content and after that block you want address 12 to have the resulting catch, this should do exactly the same thing. And what this instruction is going to do is it's going to use this newly constructed chip or circuit air whatever you want to call it that knows how to how to compute catch without using any of the exor and add instructions that are generic um to the VM. So this is quite efficient since for example these are very arbitrary numbers

taking into account different um current risk 5 ZKVMs. We're trading about 700 instructions which is the amount of instructions we have sequentially to to compute catch times 150 cells. This is like the amount of data you need at the same time. So for example registers, memory locations and so on. Um which we call this is the width of the CPU. um chip or the sum of instruction circuits depending if it's a node super architecture. So you're trading that by a large chip. Now we have a thousand columns or more in this new air. Uh but we have very few rows and we can basically compress all this generic computation into this amount of of

specific computation and this will give us a lot of benefits improve time and recussion and so on later on. So in the wild you usually see 5x 10x or more depending on the case speed up improving time for zkms and this makes pre-ompilers essential for complex programs in zkVMs because the KVMs they can be very expensive if you're just doing generic computation but for computationally heavy things like ketchups and so on. So Ethereum blocks would be very complicated to prove if we didn't have these pre-ompiles nowadays.

This is what the plunky 3 catch specific circuit looks like. This is only a part of it. There's hundred hundreds of lines more of code. Um it's a lot of code. It's not super easy to read. Um and yeah, it was handwritten. So couple humans probably wrote that. And the reason why I show the plunky 3 catch is because it's used by a lot of different Zik VM. So a lot of different ZKVMs nowadays use Splunky 3 and they either use that circuit directly or an adaptation of that circuit. So this includes for example SP1, powder VM, um, OpenVM and probably others. And yeah, that's why I showed the catch one. But what if we end up

with the workflow which is common that you have a complex gas program, it's not catch, it's something else. It's a it's another hash function. is MPT something else and you profile it in Zik VM and you notice someone else something else dominating the cost of the proof and now you want to optimize that and then you do it again and then do that again and then other companies do the same thing and then in the end we end up with tens hundreds of thousands of of these handwritten massive circuits that are very complicated to read um and very complicated to write. So the main consequences here is that we're going to end up with a crazy amount of engineering effort that's not scalable.

Everyone is doing a specific thing that sure other people can use it, but if the use case is different then you're going to have to write a different pre-ompile for that use case. And the second thing is they're going to be full of bugs. Enter auto pre-ompiles. So why should engineers be doing this by hand if we can do it automatically? Well, the obvious answer is that you can't until this. So, auto pre-ompiles is um an optimizer, an optimization feature that we wrote that basically does that and it's fully automated. There's no human inputs. It's agnostic to the ISA.

It only needs very little information about the ISA. Um doesn't matter if it's risk five, WASM, whatever. It only needs to know what branching instructions are and the encoding of the program needs to be a normal binary encoding. Not that it can't be do otherwise. It's just the easiest to integrate and the performance is already comparable to manually written pre-ompiles. Um, so there's this expectation that manually written things will always be faster than the compiler can generate. But with time we've seen that this is not always the case. At some point you can't fool the compiler anymore. You can't be better than the compiler.

And the expectation is that you can reach that at some point. Um on the security side, we're hoping that by having this one central way of automatically generating the circuits that once this is audited, formally verified and so on, this security basically scales to all the circuits that it that it creates and you don't have to individually audit a thousand pre-ompiles that people have written all over the world. And the last thing which is maybe one of the most important ones, it makes it more suitable for form verification. You can compile these automatic circuits in a certain specific way that if you write a tool chain once that leads to having

some form verification results, you can reuse it the same like it basically scales to all the pre-ompiles that you create other than instead of just writing them by hand and then trying to verify um one by one. And in the first implementation we did for powdervm, we saw three 3x reduction in witness cells. And witness cells usually translates um directly to proof time. What it doesn't translate necessarily into is when you do recursion, which is often the case if you have big proofs, you have this proof time for a lot of different what called segments or chunks and then you have this recursion tree that compresses like a hundred different segments into a single proof. And we couldn't run this

experiment end to end on Per VM because we didn't have recursion. So we started integrating with VMs that do. And this also shows that this type of optimizations they are actually applicable to any similar ZKVM not only to powder VM as an optimization module. So you can take just that module and integrated into different ZKVMs and still get very good results. So this was an experiment we ran with OpenVM. So basically using OpenVM's front end ISA then going to powder for optimizations then going back to OpenVM for for proofs. And what we see here is that in this experiment we had 25,000 catch runs. The software version there's no

acceleration. It's just that massive block of code I showed earlier leads to 49 segments. And a segment is basically when you have enough instructions that you're proving, usually about like a million instructions, that you're not going to be able to make a proof anymore or it's going to be it's going to take too long. It's going to take too much RAM. So you stop at that point. You say, "Okay, this is enough for one proof and you start again from scratch after that." And then in the end, you end up with a bunch of these each proof um proving basically one million or so instructions.

And in the software version we end up with 49 segments and in the manual pre-ompile four segments and the auto pre-ompile version using this module end up with nine with nine segments and yeah the proof time itself is arbitrary doesn't really matter the number is so these are the things we care about. The first thing is what is the improvement um versus a software version because that's the the reference right. So the manual pre-ompile version is able to accelerate this example by 11 times and this includes these like initial proofs as well as the whole recursion tree to compress all these proofs into a single proof. The automatic one is almost 3.5 times. So this actually matches quite

well and is actually better than this because it's a bigger number um and includes recursion which is actually one of the bottlenecks of this um of this approach. And the other number we're interested is when you take the manual pre-ompiler as a reference because that's the fastest we have right now. And if you see here, it's almost only 3x um worse than the auto premp than the manual one, which I think is really good results already because um that's the fastest way we have to represent catchock in zkms right now except maybe for bin um in the risk five

ones. So yeah, this is um so it's actually kind of in the middle. see like it's almost the same factory versus software and the manual one. So this is actually really really encouraging results um because of the the benefits you get like it's 3x lower but you don't have to write a single line of code. You potentially get better security um guarantees for verification and so on. Um, so for some cases, you might still be interested in writing a manual one to get the extra 3x on it. But if you think that you can get 3 2x or I mean this is going to improve of course, but even if you have a 2x um overhead by m by using the automatic version, that's already

very powerful versus having to manually write a bunch of pre-ompiles. Um, okay, how does it actually work? So what's happening behind this feature? So the basic idea is actually pretty simple. So in the ZVM each instruction is going to lead to a different set of constraints. It will depend on the architecture if it's a monolithic CPU or no CPU. But we can use the monolithic one for now which is you have a CPU. CPU has a bunch of registers and these registers are used um to compute the result of different instructions adds shifts um exors and so on.

Um so every time you call instruction you add a row to a table that represents the entire CPU with all the registers and so on. So every row is one unit of time and all the constraints that ensure that these instructions are computed correctly they have to be active in every row. So what we do now we collect all the circuits from all the instructions that in this massive block from ketchup. We put all of them together in a massive circuit, super wide circuit that is as wide as a combination of all the instructions that we that we started with. Then the very first step, it's a very small step, but

it triggers a whole bunch of other stuff is inline an instruction arguments. So if you think about an exor, you have exor of a b equals c, and it's a generic way to apply exor and that's what the VM needs. But if you're accelerating a single instruction in that block, you actually know what the arguments are. Um in this case would be the indices of the registers. So you'd say exor of the specific registers five and six need to go to the register seven for example which in risk five they're numbered from 0 to 31. So when you know this you know the source location of a lot of the computation you can inline these things in the circuits and then this inlining propagates a lot of different optimizations that we can make and yeah

after doing this you just optimize the whole thing and you get good numbers. Um so this is just a quick visualization of what it works of of what it looks like. So you can think about one row as all the data you need for one instruction. So you're going to have some instruction flags and some instruction arguments that tell you where you are and what you're doing. The instruction columns which um represent the actual computation being verified in that instruction and then what we call bus interaction columns which is how you communicate with memory with some of the registers and different machinery you have underneath. Um yeah, so the first step what I mentioned before, you take all these rows that would be needed with all these columns for that block that I

showed earlier and you just put them next to each other. So this is now one super wide circuit that does catch up and each row of this is going to do what that entire block of assembly was doing at the beginning. But yeah, as the comment says, at this point we're committing to the same amount of data as a software version. There's no improvements here versus softer. We just took this and we did this. But now we can start optimizing things. The first thing is you see that here we have the yellow um data which is the instruction flags. But now we know what they are. They're written in the block. So they just go away. So we know what they are including immediates at compile time. So we just remove them and

they don't have to be here. The next thing is we can start um optimizing the blue and green parts because a lot of data is local. So we don't have to keep going to memory and back which instructions generically need to do. So now we can say okay I'm writing to a location and then I'm immediately reading from it again. I don't need this write and read. They can just merge these two things. Um, and this same thing then if you end up seeing that something is a constant, you can propagate that constant and start simplifying or even solving for a lot of constraints. Um, I don't know if you can read this, but this is an example of a really small block coming from Risk 5 program coming from Rust. So, this actually does nothing.

Um, but it's a good example because it's small because Ketchac would take us two days to go through. Um yeah so you don't have to read this it's just a sequence of instructions and the good but what I wanted to show here is that when you look at the program the arguments of the instruction are constants it doesn't mean that it's all constant computation these constants are like the ids of the registers memory addresses and these kind of things but this is what has to be generic because when you call an ad all these things inside that circuit are generic but here they're not I'm computing an ad for these parameters for these arguments.

And if we turn this this block into like this text form, this is what it's doing. Um, it's updating the stack pointer in risk 5, putting,24 in register 10. Then it's putting this R10 in this address here, R2 + 12, which we don't know what it is because R2 is symbolic at the beginning. This should be X2. But then we read this. We just set this address to X10 R10. We load this address again and then we update the PC at the end with something we have to jump. But if we actually look at one thing at a time, so we have R10 equals 1204. This can be inlined. We don't need

R10 for this. And when we have this store, it's like, okay, we can't get rid of it because maybe it's going to be used later on, but we can remember at least that address R2 + 12 has 124. Then we see that R10= R2 + 12. This can be inlined as well. And the reason for this is that this is a linear expression, and it doesn't cost more if you inline them. It gets more expensive if if they're not linear. But this can be removed. Then we're loading from address R2 + 12, which is literally what we just wrote. So this load can actually completely go away and we know it's 124. Now we have R10 equals R0 + 2. R0 is actually always zero in the risk 5

spec because of hardware. Um so we know this is actually two. We can align it, remove it completely. And in the end, even this expression actually simplifies to a constant. And we know that even the condition can be removed. Everything can be removed. we know exactly where the PC is going to go. So, this is an example that is so simple that we actually don't have to go to the circus to solve it. You could solve it in the assembly level because the compiler just did a really bad job here. Um, which is not unusual with LVM. But that's kind of like just to show more or less the optimizations you're looking for. It's just that usually it wouldn't be that simple in the assembly level, but on the circuit level, you can actually propagate a lot

of this knowledge. So this is actually what the circuit is going to look like later on. You're going to have a lot of buzz interactions doing rain checks, memory accesses, and so on. And a lot of insane constraints. And so these are like a list of of depos optimizations we're already doing. So inline and instruction arguments removing redundant memory reads and writes and because now the data is local to the block so I don't have to all the time for every instruction go to memory come from memory which is very common in risk 5 because of the stack model uses in RAM um and especially in risk 5 this is we actually get an upper bound for the

amount of reads and writes for registers that a pre-ompile is going to do. is going to be maximum 64 32 reads and 32 writes maximum because there are 32 registers and you only have to keep the first read and the last right everything in between can be completely inlined. Um and when we remove memory accesses usually the memory arguments are built in a way that need a time stamp and you have to range constraint the time stamp um difference from the previous one to keep it increasing. So now we can remove a lot of constraints. You can remove rain checks, you can remove a bunch of other things. Um the same thing with redundant buzz interactions on the PC because before this every instruction

has to commit to knowing what the PC is, what the PC update has to be and what instruction has to be and like the the Rome contained in the program. Now we don't need any of that anymore because we know a compile time what the PC um update is for each instruction. Um and in general this is kind of like a black box but probably the most import most important part of all simplifying complex constraints. So we start in lining things and in the end you end up with weird looking quadratic cubic whatever highderee constraints that they're not organized in a way that's like a equals this b equals this and so on that's kind of like easy to solve in a diagonal way. Um, so they can be complicated to solve, but you can

actually partially solve for a lot of variables. Um, and this basically allows you to remove a lot of different columns, which is actually likely the the main um the main bottleneck of these circuits just like having lots lots of columns. Actually, we ran an experiment. If you remove all the constraints, we have a massive pre-ompile, an automated one for catchup which has thousands of columns, thousands of constraints. If you remove all the constraints, give it zero constraints and just keep the columns, the the proving cost is still 90% of the original. So the important thing here is really to remove data, remove columns.

And the constraints are actually not super important to remove themselves. But optimizing the constraints allows us to remove columns which is just data within the the constraints. So for this we have a custom solver that takes these constraints and tries to solve for variables. And Chris and Gorg here are the ones working with it. So if you have questions about the server, you should ask them, not me. Um yeah so these are and then these are this is what we see in this small example. So when we first in take all the chips and put them together in the single chip, this is what we see. It has 200 something columns, 200 something

constraints and 100 bus interactions. And after all those optimizations from before, this is the numbers we get. So it's about like a four 5x reduction on the size. And if we go back to the catch um example, this is the numbers we get. So the initial chip has 20,000 columns which is an insane number of columns for a chip. So for reference the manually written catch has about 2.5,000 columns 3k I think it's about between two and I think 2.4 2.6,000 columns.

Um and yeah so 20k is you would have 10x worst performance basically but with all the optimizations together memory constraints columns and so on we managed to reduce it to less than 5k which puts us within um a 2 3x ratio from the manually written one and this this really translates to proof time both the basic proof time and the the recussion one this a lot more to recursion and this is basically almost like actually this is last now but the last time I ran these numbers it was it was very close like the numbers we see in practice like the

two 3.2 two slower than ketchup was very close to um to how many extra columns this circuit has. So it it translates very closely and some more exciting optimizations coming that will hopefully um get us a lot closer to manual one. There's more um compile time constraint solving um coming soon. more memory redundant redundant memory detection for the stack which in risk five is a lot and heap heap is I don't know how much you can actually optimize there but stack should be

um should be considerable um propagating linear expressions up to degree bound so this is like a a niche thing but if you have a lot of constraints that are like linear or quadratic usually in the proof systems that these ZKVMs use they accept up to cubic constraints for example. So if you're not using cubic constraints you're kind of missing out because you could inline some of these expressions to end up with cubic constraints and remove columns in in the process. Um, and air stacking is an even more complicated optimization which is useful for when you have a lot of pre-ompiles because then recursion gets really expensive.

And if you have a lot of pre-ompiles that are very wide, but they don't use as many columns, as many rows, sorry, that would occupy a whole segment. You can actually take these two different pre-ompiles and merge them. Just put them on top of each other because now they have the same width and more rows. as long as they fit. This is more efficient and it just got rid of a bunch of columns. Um, so but this is probably the most complicated one. Um, and the goal is to get the automatic catchback pre-ompile to be faster than the handwritten one. That's it. Thank you.

Can you train AI to be good at this? Probably not. Then my next question is like where is the where is like the where does this start to fail? Is it because of obviously training data or because you actually need to instruct this whole algorithm of reduction? Um for some of it AI could do but where AI is not going to succeed for a long time is simplifying the constraints. It's just really bad at math and this is yeah it's it's not going to be good at it. You're not going to ensure any kind of I mean yeah if I guess like with AI you would have to have form verification as a requirement in a way like you have to be you have to prove that the generated

chip does the same thing as the original one right sure so I think that requirement becomes a lot stronger in the AI case instead of like heruristics and math solvers um sorry behind you was first yeah out of all the optimizations that you have on your Are there some that are simply not possible on the LLDM compiler before even getting here? uh I mean the circuits basically because this doesn't exist there right so the when you get from I don't know m store in LVM when you get the assembly it's just like literally an instruction right but when

you get to a circuit it's going to be implemented as a sequence of constraints or like a set of constraints that have nothing to do with LVM and this is what actually is expensive in the end so you can do high level optimizations which which will have an impact but some of them just won't exist until you get to this point. Yeah. Is there a limit? Yeah, that's a good question. So, um there's one idea that you could actually turn the whole program into pre-ompiles. You take every single block in the whole program and then your final

program is just pre-ompiles. And it's a pretty theoretical idea at this point. I actually did it I actually tried it on on an EVM like on Wrath basically. Um and you end up with like almost 5,000 pre-ompiles and I didn't even try to make a proof for it because um yeah recursion will just get destroyed. I think for that you would need a very strong um air stacking at least, but also like I literally did for all of them, but that's that's also very clearly not a good technique because you want them to be at least somewhat expensive because if they're cheap enough, it's not useful

to optimize them. You can just spend the instructions and it's fine. Yes, there must be like a one thing we also do is just like some profiling guided optimization. So you just profile it first with some sample inputs to see what the hot paths are and this kind of things to see which basic blocks to optimize because if a block is never used, you only you could be paying for a lot more columns even though you use like once or twice. It's not worth it. Sorry. Okay, cool.

Uh if I remember right, the catch circuit in which I guess was like the handwritten reference basically it decomposes the entire state. So it's like 1600 state columns. Is that also what you end up with? No, I think that's specifically for catchup. I think that's why we can actually be more efficient at some point because we're not doing the bit de composition which is which ends up being pretty wasteful, right? It's it makes it easier to write the circuit. Yeah. So what gem's referring to so in the in the handwritten circuit that I showed here it basically implements catchak by bit de composing the whole state. So

each column is a bit which is pretty wasteful in terms of data. It makes it easier to write the circuit and the constraints become simpler but as far as number of columns go it's pretty wasteful. And in our case, we end up with the higher level instructions because um like if a catch does a shift in risk 5, then it's going to use a shift chip and the shift chip will probably not bit decompose it. Um it's probably going to use lookups. Is a bad example, right? Yeah. Yeah. Yeah. But like exor xor for example in the in this case I mean in the automatic in this case it's going to

use the bits and then it's going to use yeah one bit one one column for each bit whereas in our case going to be turned into lookups into byte byte range x and the lookup for the exor result. So the exor should be more efficient than in the handwritten one. But yeah, that's more like a coincidence. But I guess like this would be a common effect like when you write the manually written circuits, you can optimize for readability somewhat or for the full optimization of the of the handwritten circuit which then might make it even less readable. Um so I think that's also a good point. Sorry, I'll question.

Yeah question do you want to do the auto compiler also instru instruction set independent it is is independent so this is risk five because that's the ISA of the provers we ran with powder VM and openVM but it is actually fully agnostic it only relies on um I mean it's already actually implemented on the powder implementation of risk 5 which is not risk five it's just a an approximation And same for OpenVM. It's implemented for the OpenVM internal ISA which is like somewhat risk 5 but it's already the internal ones. So it doesn't have to be risk 5. And the only thing that it relies on is knowing

what branching instructions are which could also be automatic automatically detected but at this point it's just easier to know them because we know. Yeah. Yeah. H sorry. No. Yeah. Yeah. So when we do actually these core processors in hardware, we sometimes reuse resources. So for example, if two core processors next to each other both need multiplier, you may actually just end up with one multiplier in hardware, but then two of them virtually share it. Yeah. For optimization, can your optimization share resources so that you kind of end up with 1.5 crocessors?

Yeah. It appear like two core processors from the function perspective. Yeah, you could. There's nothing that prevents it. um at a at the first implementation, it depends on what the original chips are doing in the first place. So, and one example is um again exor. Yeah. So, if you have two different pre-ompiles that use Exor, they will both end up using the same lookup chip. I see. So, that's already shared. But some other chips they have some inline chip that they like for example I think the like there's like a less than small air that gets inlined every time it's used. So this would be different copies but just because of the way the original chip for the instruction was written. But if the

original chip uses like a common one uh via called the bus then it will end up shared as well in the final pre-ompile. Um but if it's in line it's going to be in line as well but it's also something that could be further optimized later on. So that's that's very intuitive for arithmetics. How about memories? Can you like share buses maybe like or have a notion scratch pad to be shared? Yeah. So the memory is the same memory as before. So the only thing we do with memory is remove all the redundant accesses but the accesses that remain they still use the same memory as before. Yeah.

Thank you.