zkVM Proof Aggregation: From Zero to Hero

Transcript

Hello. Hello. Should we start? Okay. Thank you. So, hello everyone. We are and Roger. We are research engineers at this which is a well I will say a kind of a newly released GKVM basically a zero knowledge virtual machine and today we're here because we would like to try to explain a little bit how we did proof recussion in the context of of a GKBM okay in the concept of GKVM proof recussion aggregation are I will say quite distinct from an standard context so the idea Uh the main idea of this presentation is not only to

introduce the concept uh basically the from zero part of the title but we all we would like to emphasize the main differences or the main ideas that we have been uh cooking in the proagration in our zikavia. Okay. So let's start very very quickly quickly uh from the basics. What is VM? A a ZKVM I'd like to define is as a I will say a virtual machine or a piece of software that allows you to prove that some program some program has been computed given an input to a program h properly okay basically erh let's

imagine that you have a program written in a high level high level language like in rust okay and then with a zkm you can generate a proof that h for a given input for a given an instance of the problem. Uh let's say the output of this problem is correct. Okay. And then this this proof well in fact you can build a lot of applications on top of this proof. One one deal application is that you can send it to mobile phone and you can try and you can verify h this proof very quickly. Okay. So that the mobile phone doesn't have to reexecute the computation uh from the beginning to the end. The the mobile phone only has to verify such proof. Okay.

Okay. Uh in order to do that, I'd like to describe it in a very high level detail like in a three-step process. Okay. The first one is the one that I like to call the compilation step in which basically you have to translate the program description in the high level language to a description that the machine that you are working on understands. Okay. So this is the traditional compilation that they have in programming languages. So for example you have a Ras program the traditional way of expressing or doing this trans transpilation is by h compile it down to r 5 codes. Okay. So basically you translate the program to risk 5. The second stage is what we call the

arithmetization in which once you have a program that the machine understands you have to again translate it to something that the proving system understands because the main objective is to generate a proof. Okay. So basically atization you translate it to something that is amenable for a proving system. And finally uh we have the proving stage in which h the idea is that you are trying to find a satisfying witness or a satisfying execution uh that basically passes all the immaturization uh of your particular problem.

Okay. So uh so there are problems like the previous one which are very easy to understand are very easy to arithmeticize but then in order to be akm you have to to you have to arithmeticize let's say a full complete language okay so in the case of GKBMS the most example is ris 5 okay as you can see in this diagram 5 is composed of many components it has a lot of instructions it has memory It has registers, it has an assembly and so on. Okay. And the main idea so so that you can build a Zika VM is that you have to be able to arimeize all these components.

Okay. There are many many ways of doing that and there have been many attempts uh during the past in order to do that as quick and as easy as possible. One idea will be okay let's try toize all this problem h all together. Okay, so you have to come up with a se set of constraints that basically do all the things but this is very complicated and a second idea which is I will say that an awesome idea is to do it in a peaceways manner. Okay, in the sense that h you divide very naturally the limitization in all the components h as you will do in the ris five in the r five problem.

Okay. So for example, you have your processor, you have your memory, you have the program, you have one component dealing with arithmetic operations, what is known as the LU and so on. Okay. And then through something that we used to call the bus, okay, which basically is a channel of communications between all the components like in a regular CPU, you prove that for example, if you're in the processor and you want to perform a computation that you know how to arenize, you basically assume this computation in the processor and then in the specialized component that knows how to perform or knows how to prove this uh operation uh will prove that operation.

Okay. So from one side we assume that operations are correct and from the other side we prove that operations have been done correctly. Okay. This is from the arithmetization perspective. From the proving perspective you have yet another problem. Okay. The traditional way of doing that is by computing a monolithic proof or what is known a monolyic proof which basically is okay we have all this limitation. We have the boost. We have all the components. Let's basically compute a full proof of all at once.

Okay. Erh well there are many issues regarding this approach. One is h the proving time is I would say quite huge if the program if the program that you are trying toize is uh very large. Okay. Another problem is that because you are going for a monolithic approach a lot of of these components are underused. Okay. because not all the programs uh use the use the same components in the same frequency. Okay. So this is an example of a typical program that is use that is using let's say in a in a regular manner all the components and at the end the main issue is that you will end up proving or you are will end up using

computation for some components that in fact are not being used during the proof but you still have to pay for it. A second better approach that is the approach that we are using in the in the VM in the VM is what we call a vat variable degree composite proof in which instead of trying to generate a full proof of all the things all at once you generate a proof for all the components h individually. Okay. So you have a proof of the coordinates for your main processor. You have a proof of the coordinates for your binary and so on and so forth for the rest of components.

Okay. So at the end what you end up with is a let's say with a cluster of a group of groups all together that that are proving that all the components are doing the things correctly. Okay. The problem with that is that you will need if you do not if you do don't do something else you will end up needing as much verifiers as the number of components that you have. Okay. So here the missing piece is that uh we are using proof aggregation or proof recursion in order to reduce the problem of having let's say multiple proofs to a single proof.

Okay. Okay, so that the verifier basically verifies the single proof in order to uh be sure that all the rest of the proofs are correct. Okay, so what is pro aggression? H basically the main idea is that uh you have your let's say your instance of problem one or you have your your one of the components in the top you have another component in the bottom you generate a proof of all these two components and then you arithmeticize not the problem itself but the verifier of the of the proving system that you choose. You send the two proofs to this let's say to this verifier prover and then you generate a single proof

attesting that the previous two proofs are valid proofs. Okay, you can do this with two proofs or multiple proofs. But there is still one issue that we need to tackle and is the dependency between all the components because remember that all these components are communicating through the bus and so we have to ensure h that the assumptions and the proof parts of this of this bus uh are rendered correctly. Okay. So one of the ideas or the way that we do that is by computing what we call an ailary trace. Okay. in which in some sense we commit to the parts of the trace that are performing a particular

operation. Okay. So let's say that the main processor is per is assuming some arithmetic operations in some part of the traces and then the arithmetic is proving such operations. What we what we do basically is computing let's say a single representative okay what we call the accumulated value of of these assumptions from one side and of the let's say the proof parts on the other side and finally what we do in a future step is ensuring h that the two accumulated values in two sides are precisely the same. Okay, ensuring that the assumptions in one part and the proofs in another pattern have been the same. Okay, and you are not trying to lie. you are not trying uh to introduce

newly operations and so on. Okay, this can be repeated for all the components, right? Because the for example the main compressor communicates through the bus through many other components. Okay, so at the end you have the the accumulated value of the main of the main processor. You have the accumulated value for all the components and you prove that all the sums are the are equal to the main sum. Okay. And finally, one single example that I'd like to highlight or one way that we do that is via the gransum argument. Okay, in which we use basically uh let's say that we h use a verifier challenge a verifier message in

order to to ensure that the accumulation of all these values have been done correctly. So now that we have introduced the problem we I will explain how we can uh properly reduce aggregate all those proofs so we can just get a single one. So the first thing that we need to understand is that how we can reduce uh those proofs into one. So what we can do is we can write the verifier as an arithmetic circuit which then will allow to generate a new set of constraints. So now you can generate a new proof of the existing one. This will allow us to like to create circuits that are verifying more than one proof. So then uh we will we will get end up getting a single one.

If we were on a monolytic approach, this would be very straightforward because you have one proof and it's an independent one. So the verifier uh using Fir interactive protocol can generate all the randomness that the prover needs. So it can automatically verify the proof. However, we are in a as Zector explained we are in in a bad cop approach and in this approach all these proofs are connected uh with uh with the global constraints and in order to ensure its correctness there's a global challenge that all that's a randomness that all the different proofs need to share in order to verify the corre the correctness of the global constraint. Therefore this uh this uh randomness that I will explain later on

how we can calculate it. It cannot be obtained just for a single proof but you need information from all the different ones. And then what uh in order to verify a batco proof in this first stage, the first thing that you need to do is you need to provide to the verifier this extra information this global challenge so that uh they can verify this initial proof and then later on we will verify that this global challenge that was a free input and that it was not verified initially it actually is correct and and matches the the global contribution.

So additionally like h in this first stage which we call the normalization stage uh we do three three things. We verify the proof then uh and then we prepare for each instance the contribution to this randomness and also as explained each instance will either assume or prove some part of the global constraint. So we will prepare those inputs so that later on we can aggregate it together. Then uh we reach the aggregation part which is where where the fun begins. Basically here there's an example uh of a regression of 2 to1 but you could uh do a regression n to one if you want.

Basically what's happening here you have uh two uh different proofs that has been uh normalized and and prepared and now you want to get together. So you create a new circuit which is called the agrator circuit which instead of verifying a single proof it verifies two proofs together. or more if you want also it this aggregator circuit does uh two very important things. The first one is it starts uh recalculating the the randomness the the global randomness. So you have two instances and you get uh those partial contributions to the randomness and you aggregate it together. I will explain the next slide how there's two different ways of doing that and also it also accumulates the

partial contributions to the global constraint. So at the end we can verify that it matches. And so this process is is repeat is done recursively until you get uh one uh single proof. So there's one important thing to notice here. Here you have like two normalized circuits that are that are processed by an aggregator circuit. But if you think about it on your on the second iteration you will need to to aggregate two aggregator circuits into a new one. So it's very important that the normalized circuit and the aggregator circuit generate the same type of proof. So you can blend them together and you can aggregate them instinctively.

So now there's a very important question. Okay, you have like n proofs and you want to merge, you want to reduce it, but which or do you there's is there any specific order that you need to follow? This basically depends on how you define uh the the global challenge which is the randomness that all the instances share. And there's two different approaches you can take. The first one and probably the mo the more naive one is a hashbased. So basically you could uh define a tree uh so in which all the leaves are the the contributions to the randomness of each instance and then the prompifier agrees on the order of the tree and when the

verifier performs the aggregation then it just it needs to follow that order that was previously accorded with the prover because otherwise if you change uh two leaves of the of the tree uh the global route the the global chat the route will be different and then uh and the things will not match. This is an issue because you are forced to follow that order and additionally if if you want to go to a very performant approach it has the issue that you it requires login steps because you will need to compute the lower level of the tree then the the next one and this way until up until top. This means that even though you have like thousands of of machines,

if you have like for example sex 64 instances, you will need to do six steps. There's no way you can speed this process up. And that's the limitation for example for ZKVMs that right now we're trying to go uh proving Ethereum in real time. There's however another approach that we can take and it's based on elitic curves and it's basically we can take advantage of the very uh amazing property that elliptic curves provide that addition is commutative which mi which means that basically you can you have all the initial contributions and if you're able to map these contributions to a point of the curve you can add those points and then you can you can get a resulting point

and you can map it back to to your field or field extension so that then the verifier uh will just will be able to aggregate in any order and still uh reach the same result. This has the downside if you want to say that you need to find a specific curve which uh for your setting but it's much more powerful because you break the dependency of the ordering. So you can aggregate in any order. You can also it's way easier to distribute the computation because you can just uh you have different servers that aggregate independently their proofs first come first serve or the way they want and at the end the they will always reach the

same uh rand final randomness because uh addition is commutative. So now we have uh reduced all the we have we have uh aggregated all the proofs together and we have one uh fi we need to generate one final proof. Why? Because first we we need to check that with the global challenge that was originally provided as a free input. It's actually correct. So basically while you were doing the aggregation you were checking that you were reconstructing this challenge. So now you check that it matched the one that was initially provided. And the second thing is you need to verify those global

constraints because you had like partial you you had partial parts of that constraint and now you need to verify that when you added everything together h the result was zero. So everything that was assumed was proofed. So basically this is like an overview of what what I was explaining. We have here like uh several instances. We go through the the normalization stage which we generate a first proof that verifies this initial one and prepares the inputs for aggregation. Then we have an aggregation stage which in for example in this case you can see a 3:1 aggregation.

And then finally we generate this final proof that uh verifies uh the global constraints and the global challenge. Here there's one thing that you can have like maybe the first proof is too big. you may need a compressor uh stage in which you reduce the the first proof by generating a new app proof of the first one. That's just for compressing but usually this will not be the case. And well uh everything so far that we've explained was mostly from an abstract point of view. We've been applying this in ZISK which is a ZKM that we've been developing for the last year at the beginning in Polygon and now was an independent project and then Jordi will explain in a couple hours in the retro stage but here you can see

some properties and here's some numbers for for example for us this at this we're using Starks and uh Fry and here you can see that for some numbers about a single recussion uh step how long how long it takes or how much memory does it use or the proof size. And that's all. Uh here you can see uh our repository as we are fully open source and if you have any questions feel free to ask.

[Applause] [Music]