ZK14 - Nondeterministic Autoprecompiles - Georg Wiese (Powdr Labs)

Transcript

Nice. Good afternoon. Yeah, I want to give an update on some of the new ideas that we have for auto pre-ompiles. So, let's jump right in. What is an auto pre-ompile? It's a ZKVM pre-ompile. So, it's something that makes ZKVMs faster. Um, but it's not written by us or by an AI or anyone. Um, it's automatically generated from a specific guest program. So you can think about you have a ZKVM, you have some guest program that you care about. Um you give that to us and we give you a faster ZKVM for this specific program.

So let's dive into how this is done concretely and then I can talk some of uh can talk about some of the new ideas. So for the purpose of this talk you can think of a ZKVM as just some collection of ZK circuits. So for example, you could have a risk 5 ZKVM that has a circuit for each of the risk five instructions. You could also have fewer circuits. Um an extreme example of this being Jolt that has just one circuit. Uh doesn't really matter. And then you have the guest program which is a a list of assembly instructions.

And so the first thing that we do to the program is we segment it into basic blocks which means that we only look at consecutive instructions where only the last instruction can be a branching instruction. And then the goal is to make a new circuit that can prove execution of the entire basic block in one go as opposed to proving instruction by instruction which is what a ZKVM would normally do. And we start out by doing the most obvious thing. We just copy paste together a bunch of circuits that the ZKVM would have used if it would have proven this basic block. And we wire it up correctly and we have a new monolithic circuit that can prove

execution of the entire basic block. But of course that would be useless if we wouldn't then optimize it and get a smaller circuit to do the same work. So let's dive deeper into how these optimizations work. Actually no uh this is a summary slide. Uh so right now what we see um is that for a typical basic block that we get from compiling Rust to Risk 5, we see about a 3 to 4x improvement in efficiency in that optimization step. Um that's like kind of the average case.

And then in some cases we see a higher efficiency. um for example like more than 10x on catchup. >> Yeah, exactly. It's risk 5 compiled to I think openvm in this case and then applying this optimization. So let's look into more detail. Um here I'm just presenting like a single instruction. So forget about basic blocks. Um this is um to keep this really simple. And this instruction is incrementing one register. So think about a Rust program that has some kind of loop and you have a loop counter that you need to increment each iteration of a loop which is stored in register 29.

And so we want to prove that increment. So typical CKVM would commit to a bunch of data to prove a correct execution of this instruction. For example, the current program counter, the current time step, then the instruction data, which is basically encoding stuff about the instruction like what are the source and destination registers, what are the immediate values, stuff like this. Then there's uh two operants and a result which are both machine words. And in this example, there would be 32-bit machine words represented as four feed elements, each of them encoding one bite of the 32-bit word.

And last but not least, there's some auxiliary data needed to for the memory argument to prove that all the register accesses have been done correctly. And already today, we can remove most of this um because we're building a circuit for this very specific instruction. So we already know the program counter. So we don't have to commit to it at runtime. We can just hardcode it in the circuit. Similarly, we can remove the instruction data because it's implied by the program counter. For example, in this case, we know that the register being accessed is register 29.

We can also remove uh the immediate the second operand in this case because it's an immediate value. And uh we can also remove most of the memory argument auxiliary data because in general an addition instruction would have the infrastructure to access up to three registers. But in this example there's only one register being accessed. So we can remove 2/3 basically. So that's the state today. We get like a smaller circuit. And let's have a look at like an even more concrete example.

and uh check the case where the loop counter is 42. So we want to increment register 29 which stores 42 we get 43. So we would commit to the operant and to the results. Um and in this case 42 and 43 are relatively small numbers. So the three first byes of the representation will be zero. But now imagine this loop never runs more than 255 times and it will always be zero. Of course, that's not something we might be able to prove, but we can still observe that this is the case typically.

So the optimiz uh the observation here is that even in the very optimized case we still have uh situations where many of the trade cells that the prover still commits to are either equal to each other or equal to a constant. In this case they're equal to a constant but even if the loop counter was very big the chance that the most significant bite changes when you increment by one is pretty low. Like it won't be the case for most inputs. So the idea here is let's build a pre-ompile for the typical case um kind of losing completeness. So we get a circuit that only has a satisfiable witness in the typical case but is smaller smaller to prove and the

prover needs to have some kind of fallback um to the situ like for situations where it doesn't where it doesn't apply. So in this case if the loop counter becomes too large uh the prover needs to fall back to something else this could be another auto pre-ompile or it could just be falling back to the circuits that the ZKVM already has because already today prover is not forced to use an auto pre-ompile. It can kind of nondeterministically choose the circuits that it uses to prove um the statement. So yeah, that's why we call an optimistic pre-ompile.

Um, it's built in three steps. We first uh run the program on a bunch of representative inputs to collect data. Um, like I mentioned, we check for trade cells that are usually equal to each other or usually equal to a constant. Then when we're building the circuit, we over constrain it. So we whatever observation we made in the first step, we add that as a constraint. Um and that basically enforces that observation and the circuit will not have a satisfying witness if the observation like if the condition doesn't hold and then we just pass this to the

existing optimizer which would just do the right thing. So for example, if it sees a circuit where two variables are constrained to be equal, we just allocate a single variable and get a smaller circuit. We implemented this on OpenVM. It's a prototype. Um, but we tested this on a program that verifies Ethereum blocks. Um, looking only at the part that's not accelerated because OpenVMs comes with pre-ompiles for something like Ketchup, but it also still needs to prove a lot of risk five stuff. So, we're only looking at that part.

Um and then we're kind of assuming that we can accelerate all the basic blocks and by doing that we get this first number this 3.3x without optimistic pre-ompiles and with optimistic pre-ompiles this number goes up to 4.8x. So we can reduce the amount of data that the prover has to commit to by this factor. And so compared to the current state is like a 1.5x increase in efficiency. So that wraps up optimistic pre-ompiles.

I want to briefly talk about a very related idea which is branch prediction. So consider this uh example. So here um the program does a division but it also does some error handling and checks whether the divisor is zero and then if not it carries on the division but probably most people are not going to attempt to divide something by zero. So the typical case will be that there will be two basic blocks that are executed one after the other. The first one checks whether the divisor is zero and then does a conditional jump which would typically jump to the second block

which carries out the division and does the function return. Um but the same principle applies as in for optimistic pre-ompiles. We can just build a pre-ompile for the typical case. So in this case we would b uh build a pre-ompile for the super block which would just prove both basic blocks in one go. And so the way we build the circuit is basically returning the conditional jumper to an assertion. There's it won't be able there will not be a satisfying witness if the condition doesn't hold.

So the circuit would still check that the divisor is non zero. But if it is if it happens to be zero then the provers won't be able to use the circuit and has to fall back to something else. And the motivation for branch prediction is kind of this chart. So here we looked at the relationship between the number of cycles that were proven in one auto pre-ompile and the effectiveness which is this number that I was presenting before. And right now we see that many basic blocks have about 10 instructions in them and we get a 3.3x effectiveness.

Um, and we're hoping that with branch prediction, we can bring this number up, kind of move to the right side of the chart. I also included the number of the far right here, which of course is not realistic. Um, but I thought it's kind of interesting because at this point we're kind of approaching having a single circuit to prove the entire computation. So, um, branch prediction can get us in that direction. So that's it. To summarize, I presented two ideas, optimistic pre-ompiles and branch prediction. Both of them were expecting to give us very significant reduction in trace cells. And the

unifying theme here is that what we're doing here is exploiting the non-determinism of ZKVMs to be able to optimize for typical situations. >> Okay, great. We'll move on to questions if that's okay. Um does this kind of technique mean that you can um transfer other um kinds of optimizations from conventional processes like caching for example? So um if you're doing a memory access um you don't you you probably know that it's within um a small subset of the memory. So you can be optimistic about that as well >> that it's like you know like caching

pages of memory. >> Well um it wouldn't necessarily have to work in the same way as a cash in a processor because you you can just basically guess that the memory location is um one of a small number of possibilities and then that's your optimistic recompile. So you don't need to actually keep track of the same cache information the processor will be doing but you get the similar effect. >> Yeah, I think we've seen something like this that for example some of the things that it can observe is that it will know more for example the the most significant limb of the memory address which I think is what you're referring to. What we've also seen is that as part of a memory argument, you need to commit

to like a previous time stamp with the difference to the current time stamp, which is often a constant because if you're accessing something in a loop, >> yeah, >> it's always like a difference in time stamp will always be the same. >> So that's something we've seen in practice. >> We've got two more. We'll uh we'll take both these questions if you want to go ahead and then we'll come to you to buy afterwards. Yeah, I just wanted to say that basically if you have a predictable memory pattern, memory access pattern um you can or at least like optimistically like predictable memory access pattern um using sparity based arguments you can you can sort of turn it into a single

vectorzed access in a sense. So so this is one way of doing this. >> Great. Okay, we'll take this final question and then we'll move on. And we should have Maddie here ready for next time. >> Yeah. So the question is have you considered loop unrolling? I guess it's kind of related to branch prediction but that means if you have like a loop uh maybe you do 256 uh iterations of that loop as a pre-ompile and then you can reuse that. >> Yeah, I would say that loop unrolling is a special case of branch prediction. So I think it just captured by this.

>> Yeah, that makes sense. Thanks. Thanks for the many questions. >> Thank you very much.