VADCOPs: Leveraging STARKs for Tailored Proof Generation | Devcon SEA

[Music] hello hello well ER hello everyone I'm eor MIP and his yeah felici Barcelo we are from polygon labs and today we are pleased to explain a little bit a concept or better say I will say a set of Concepts that we have been working on during these months which we co as vops okay which stands for variable degree composite proofs we will see that this set of Concepts will allow any prover specifically an prover to prove any kind computation in a way that H he can tailor the computation uh as it wants okay let's start anyways with the basics uh let's say that you are posed with a problem of er proving any a specific computation okay and you normally see a computation in two different views one view is the evolution of this computation along the time okay for example let's say that you your your computation is composed of of four variables you study the evolution of the state of these variables along the time okay and then the and you record this state evolution ions okay and this is what we normally refer to in execution trace this will be very relevant in order to prove it correctness and then on the other side you have what we refer to as a transition function which is basically a set of rules that these computations has to be for example you can enforce that the computation on the variable a has to start at one B has to start at seven okay you can also pose restrictions on the very same state for example you can say that a plus b is equal to 2D along all the states you can also say for example restrictions along ER continuous H stage for example that c has to be also has to be always equal to to a of the previous state okay and so on and so forth basically H linguistically speaking is a set of rules that the developer think of H in order to compute a computation okay then we have the process of witness computation which is basically trying to find a set of values that satisfy such rules and finally and because uh commutations can be described in in very very different manners we have to find a way a language H to describe it in a in a common way okay and this is normally referred to as lization basically finding the correct set of constraints that describes the transation function of the computation okay okay now if we go a little bit beyond of this basic problem let's say that we are posed with a problem of trying to artize thing like an evm okay this is far from being something trivial because in the evm you have a lot of components you have on the storage you have a memory you have arithmetic operation you have memory operation you have a lot of things and you have to try to arzee them all you have to find the right set of of constraints okay and the a if solution of this problem is okay let's try to do it okay let's try to find a set of constraints that enforces not only arithmetic operations but also memory operations but also H input data management and so on and so forth okay and then we soon realized that trying to do it as a whole is a very very complex problem okay azing all these things are far from something trivial okay so we needed to find something else we need to find a new tool in order to do that and the tool the thing that unlocked the me on the of the evm was the concept of of a b okay which basically allows you to break down the armatization in different components okay so it's very natural that if your computation or your component has Artic operations you have a dedicated set of constraints only ensuring the correctness of the of the Artic operations okay the same happens with the memory with the storage and so on and so forth okay then you have all the components in individ ually being proven and then you need something to prove the relationships between these components okay and this is the V okay with the V you basically if you are for example in the main component and you want to perform antic operation you basically assume and you have and you're giving some inputs you basically assume that the you basically assume this inputs and you throw them you throw this data to the B okay with the expectation that at some point the correct component if you have done so for sure will take these inputs it will compute the output and we check will give you a proof that this computation have been done correctly okay so from one side you have components throwing things to the bus this is what we normally refer to as assuming a computation from the other side you have other components taking things from the B okay taking things things from the bus and trying to prove them this one normally we refer to as proving something to prove assume versus proof okay this is very abstract so let's see let's see an example let's see the different ways that we have come up in order to manage the b or to throw things to the bus for example you can use the bus to try to prove a permutation between those two two components because for example you want to ensure that the memory operations that you are doing in the main component are exactly the same as the ones that you are proving in the memory component you can have lookups for example because you maybe are doing the same arithmetic operations many times and you want to prove it so you will find it many repetition of these operation in one site but you want only to prove it once and there are a lot of more variety of of ways to throw things to the bus for example you have range checks you have connections you have whatever you need basically okay but anyways with this we were able to ER divide the imization in many components but animation was more or less easy I would say and then you basically generate a proof of all these things not only of the components but also of the correctness of of the B let's say okay and you generate this proof and what you normally will expect is that you have a lot of traces all of them filled with meaningful values and then you prove it and then basically you're proving the state transition of the evbm which is the original objective but then then after after trying it with very inputs coming from different kind of transtions we realized that the reality was completely different okay the reality was that we had some components that were totally meaningful were totally filled of important values but then there were other components that were not even filled for example U because because the size of the stres has to be the same because we are generating a proof of a whole trace the arithmetic tic component was was not even used uh the in the average okay and for example if you go to the extreme case that you are designing a specializ for component for special cases or special operations for example when you want to prove the corness of a pting then we realized that this component was totally ER Unos okay so we needed some way of fixing this problem and the way to fix it was the introduction of bath cops okay now uh things will be completely different okay we are we will not be again trying to generate a proof of the whole thing at once and now the idea is that you could adapt the armatization to the size that you would like to to have for example if you expect that for the ous case you are not using thetic too much but you still need it you could design a ration that is lower in size okay the same happens with other different components and then the idea is instead of generating a proof of everything we generate a proof of all the components individually and for sure we also need that this proof takes into account the relationships between all these components because the relation zims are still there okay so from one side agregation from the other side consistency okay so let's let's go through an example let's say that we have the main component and the Artic component different sizes perly for our needs and we want to prove the relationship between these two okay so what we normally do is we compute what we call an accili Trace beyond the original trace the main and the arithmetic okay then when we do an assume ER we accumulate this value along these actuality tray and the same holds for the Artic okay and at the end we end up with a with a value that we normally refer to as an aoup value and Beyond proving the correctness of each component we will need to prove that the resulting value is the same in both sides okay achieving the fact that they are related correctly okay for example if you are if you are with the problem of proving a lookup and you're using for example the loog up protocol okay H we what we do is we are going to be accumulating the fraction sum of all these of of the both sides of theity Trace okay and at the end for sure you will have constraints ensuring that this accumulation H is done correctly and this we this still will be proven in the let's say the basic proof and then you will need to proof outside the individual ones that the two values that you end up with are completely are basically the same okay achieving the lookup H check okay if we will a little bit on the details of this aggregation and this and these constraints and these proofs okay this this is the in this diagram you you see what is normally a circuit for agregation aggregating two independent proofs okay so the logic of this circuit is basically a copy of the verifier logic okay and you give it it expects input for example po inputs dation type the proof and so on and what you expect the the verification of these two circuits is successful and then generate a proof of this statement okay this is a traditional independently proven aration circuit okay but now we are going to energe this logic only to deal with the dependence that this proof uh have underneath okay we are going to be giving it the Air Group values the accumulated Air Group value until this point then the circuit instead instead of just saying if the proof is Val or not they will also generate their a values their resulting sums that doesn't matter if you lookup peration and so on the resulting sums and then we are going to the S itself is going to aggregate the Ed grou values and it going to be and then it going to speed out as an output not only the proof but these a group values okay and then at the end of the at the end of the aggregation the the last the last agre circuit will ensure that that the sum or the aration function that doesn't matter if it's a some or not matches okay as in the previous example okay one one of the the things that we need to solve is the scalability uh I was explaining before scalability can be uh you can see this in in two ways one is the high scalability I produce different um different uh machines specializ it that means that I can solve the problem with with a specific machines okay um but but it's only one type of theability okay it in this scality I can use the different the number of the different the machines but the problem is that I need to to add something this is the this is the part of the horizontal scalability the other is related to the vertical scalability that means if we analyze the different type of the the state matchine that we have there are the typical single machine that means that only one one instance okay for example the Rome that would has the the the correct uh instructions that can be executed another another are the in uh the machines that are SL independently that have independencies no have no constraints between the different SL that can I do I can divide this in horizontal I can put this in in in in any place not have a problem because not have relations uh between these machines I I prove the different binary operations okay but each proof is independent of the other okay but there are another that have some relations between this or for example the memory or the main because the trace one row depends of the the previous row okay something what can you do uh we put some relation between the end of the first the end of one stage uh of one instance one segment to the other okay and we need to link this in a correct way we use whereb who make this okay we we use the same concept that ector explains before when you start a segment you assume an an an initial state that you put in the in the in the in the bass and when you finish you prove that this assuming this initial State you finish with this state and you put this inside the bass okay with this you you you can add any uh instances any segments of the the the main of the memory that you want okay the only is the this relation okay this have an uh thing that we need okay but we R this start with one one state and finish with with this but we need to to to broke this this relation because really the initial state of the program cannot be the the final Pro state of the program for these reasons there are a global constraints uh that defines this relation using the bus but in a point of view of the global constraints that means that you define with a global constraints what is the the initial state for example what is the PC now the boot address or what is the the values of the register that you want okay and after you define how needs to be finished this program in correct way okay and this put inside the bass this a very and very useful uh instrument because there are another problem when you use um cycle machines in a security problem that you can repeat the cycle times and you qu if I close close this cycle that means but I can add two different cycles and this is not a correct execution of the program how you put this in the in the global constraint you only have produce one time the cyle because not have any things in the bus to start a new a new to allow to start a new cycle right okay uh as a sumary uh the continuations uh is something that assumes an an an initial State okay and and pro the next it's important that this this continuations is different the other continuations that use a big uh numb so use one for uh for all the machines this is individual for each machines that means that I design a machine I cut that have relation ship between the rows I don't have problem to cut only do be use this this this um this continuations the initial and final uh State I have full control about this that means I can execute for example two Mains with different program because I can put in the in the in the the global constraints the beginning and the end of the different of the different uh Vines I have fully control of this in initial State and fin the other thing is is we have an an an idea to produce an an AAL what is what is AAL when when when we think in the trace we think in the rows okay but when we thinking in the state of the instance really don't have dimensions of rows because no change is the the the state at initial or the state at the end no need to to fill on row with this Val because we not spend a lot of for put this and this means that that we need the air Val the air Val is something that is only is common is inside the the the the H instance for for example what is the beginning PC or what is the NPC what is the segment ID something like that okay and it's very cheaper because not is something that applies to all the rows okay uh okay uh how how these constraints really this a Val you have an relation to directly the specific row of the constraint for example I say the PC say must match this air value related to the beginning PC the first valer that is in the trace of the PC that this is the relation who fix the vales or who constrain the vales that have these air vales okay um this give to us an a tool to Define to Define uh a trace that we want not not the limitations when we can put put good good and put the different the different things to the B using the same performance bus not using anything is a like way to to to do this this um continuations okay and and the same way that we use in the main you can use for the memory okay and you don't pay any cost for the other machines for the contion because you don't need okay or Ms yeah well as you have seen uh there were many Concepts that we try to fit in with within a 20-minute presentation we are using all of these H to build the you can check out the repository and see that all of this is not only Theory but it has been implemented in practice just check it and try to understand it and well epic phrase at the end and yeah thank you very much thank you so much both for the great presentation so um reminder to the public that if you scan this code uh you can U visit the session in mcut and that allows you to ask questions vote for questions and also collect an nft about the session so yes uh I think right now we only have one one vote so let's start with that one if you were a time traveler would you prefer better architecture for evm to make it more CK friendly and yeah maybe you can expand that and me precise what what if so yeah yeah yeah I mean if you see the history the the the the the people that designed the evbm at the beginning they reject or at least didn't expect the world to be that g friendly at the future and I'm sure that they will have designed some things differently at the at the at the moment that they design the evbn they will know the impact of these things on the on the use cases of GK in general okay just keep in mind that when the when ethereum came out there were not even papers that make snark or GK in General ER pable and let's say practical okay so yes for sure I will make it more J friendly but I will say that no one else at that time was able to predict that that impact of GK in general I think it's important to say that that all the things that we have a lot of improvement that we breaken some some that we have related we make the BM and we found and we alert we have a lesson learn it about about this is important because we we see what what we need for make more big things that's the luxury of hindsight hindsight right the next one thank you for the one who asked what are the implications of beam chain if 3.0 that was discussed yesterday I don't know if you if if you saw it or heard it as it relates to CK yes so I mean related to our talk it's clear that at least we are using all that we have described to build a zbm and it was clear from Justin Justin talk that gkbm will be used in many many many places in 3.0 in particular in the consensus part so I mean I will not say implications of the V chain to GK but the other way around the implications of the evolution of GK to the V Cham itself great please Round of Applause thanks so much