ZK10: Optimizing recursive STARK verification in Polygon Miden VM - Bobbin Threadbare

Transcript

[Music] all right everyone welcome we have Bob and threadbear from polygon Maiden hello everyone uh very happy to be here um my talk is not going to be nearly as exciting for one my slides are not that colorful and but more importantly I also don't have a T-shirt cannon so um it's going to be just some boring stuff anyways but um my presentation today is really about like how do we optimize recursive proof verification within mid VM and some of the things we learned and kind of uh uh how we've approached the the the problem overall

so kind of as a road map for this um talk first I'm going to talk about different approaches to recursion and here I'm going to focus mostly on Stark be recursion but um it applies to many other uh schemes as well uh I'm going to talk about like the requirements that we have uh specifically for the m rollup and uh how we think about different parts of the verifier costs and then talk about some of the optimizations that we did within mid VM and finally present some results and conclusions so let's talk about uh kind of recursion and why do we need it so usually uh we may have like an N number of programs these programs uh could be chunks of one big program or it could be completely independent programs in the context of starks where a lot of the systems use this virtual machines or Star based

virtual machines we execute those virtual machines and generate proof for each of the programs independently but frequently we want to roll up this um individual proofs into one single proof uh for various reasons uh it's useful in context of blockchains it's useful in other contexts as well uh but basically what we can do and this is like in the first approach where we have a specialized circuit that does the aggregation so recursive proof aggregation is done by some specialized circuit that um you know or it could be a number of different circuits that takes two or more proofs combines them together and outputs a single proof uh and this is kind of what I call the special circuit approach there's another approach to do this and um I call it the single circuit approach where we also start out with end programs we generate end proofs and then um we use the same

VM to aggregate the proofs so basically the same VM gets executed it has the same VM logic uh and we can do this because a VM itself is you know if it's powerful enough for example if it's it's your incomplete VM then you can write a program that verifies uh its own proof of its own execution basically so you use the same logic you don't have a specialized circuit that's basically the same thing um and uh you know there are different pros and cons of why we want to do go one way or the other so if we compare a specialized uh um circuit versus kind of same circuit or using the same VM to do both the leaf programs as well as uh the aggregated uh aggregation you know uh what are the things we want to look at so first is flexibility with

a specialized circuit approach it is very focused on what we want to do we want to do requestive proof aggregation so uh your flexibility somewhat limited with the same circuit you have the full power of the VM you can execute whatever you want um you are very flexible basically any program can be executed together with the proof verification in that uh in that uh circuit or that VM kind of run uh design complexity I would say that if you uh have multiple circuits your job is somewhat easier because you have very well- defined problems and you have a specialized circuit that is you know doing one task and it's easy to optimize for that specific task if you're building a single VM that needs to be efficient in multiple different contexts there are some sometimes conflicting goals and it is difficult to kind of come up with a

ideal design um I would say on the other hand like once you have the design auditing it um is somewhat simpler because you have just a one VM that you need to check and make sure the constraints are correct while in the specialized circuit context um you have multiple circuits that you need to uh AIT and sometimes you know interaction between those circuits may not be trivial so it's a bit more complexity there uh but what one of the primary reasons why you want to do specialized circuit is performance If You're Building A specialized circuit that is um you know it all purpose is to do recursive Pro aggregation it obviously will be more efficient than whatever you can come up with in a generalized setting and I put it depends because it really depends on the instructions that that you're using uh whether a same circuit you know is

really horrible or acceptable or you know could get close to the performance level of the specialized circuit and um the distinction here is that if you don't control the instruction set if you use something that is given to you it's very difficult to make it efficient uh for recursive proof verification so like if you are taking you know let's say um evm like doing recursive proofs in evm would be extremely complicated or would cost a lot but if you're taking um something evm that where you control the design where you control the um kind of the instructions set then you can introduce specific things uh this is what we've done with mid VM just to foreshadow a little bit um and then you can make proof verification uh a bit more efficient and and uh again you

won't get all the way up to the same level of performance as you can get with a specialized circuit but you can get pretty close all right so let me cover a few of the requirements that we have specifically for the miden rollup so um in mid rollup we go with a single VM approach where uh the same VM is used to execute programs and also to uh aggregate the proofs and the reason why we need this is that uh at different levels of aggregation we execute non-trivial amount of logic that is not just uh proof aggregation itself we for example at um at a block level we also need to verify in the future consensus for example logic and things like that so we want to have other things executing not just proof aggregation the other reason for this is um we want to

make it flexible so we want to provide Primitives within the VM that may uh let people create uh efficient um verification of proofs that are not just for Mid VM but for other maybe VMS or maybe proving systems so if you have a primitive for example is a fry verify uh fry verification is efficient you can use it not just for Mid VM but you can use it for from multiple other VMS if you would like that anything that uses fry for example as a polinomial commitment scheme um as far as the requirements go we are currently targeting and I'm listing this so you can some of the numbers that I show later uh kind of make more sense but we're targeting 100 bit security level which means in the context of starks and this if you don't know Starks that these numbers may not mean a lot to you but

you know we use a 8X blow up we use 27 queries and 16 bits of grinding that's kind of like our uh um proving setup and this is like all the numbers that follow will kind of Target this level of security with this parameters um and then the way we think about the leaf programs in the context of the mid rollup the leaf programs should be relatively small and by relatively small small I mean they should take between two to the 12 between and 2 to the 22 Cycles to execute now programs can go outside of this but like we think this is the sweet spot for us to like have efficient recursion in now if your program is bigger it still will work fine it just will be a bit more expensive to verify recursively now in terms of like our concrete targets what we want to get to

is do a 2 to1 recursive proof in 1 to two seconds using consumer hardware and by consumer Hardware I means something like a mid-range maybe mid to highend range laptop I don't mean like a low power smartphone at this point we'll probably get to a uh Smartphones at some point as well but for now we're targeting kind of this laptop type of environment and we want to do this recursive proofs in 1 to two seconds and then if we go to something more customized we want to do 16 to1 recursive proofs in 1 to two seconds and here um you know 16 to1 proof can be done as a tree of smaller like 2 to1 proof so it could be done as a 1 16 to1 proof it doesn't really matter uh that much and by customize Hardware I don't mean something that will require an ASCO

fpg I requ I just mean like you may need to choose a power processor pair it up with like a GPU or two uh but you can build it with off the shelf components uh it's just customized in the way that you've put it together it may not be available kind of like something to buy over the Shelf immediately or something like that um to put this uh kind of uh goals and context let me tell you a little bit more of what M DM is capable of doing right now so M VM if you want to execute a program that takes two to the 17 Cycles um right now let's say on the MacBook um M M1 um and if we use a fast hash function which is like Blake three we can do a proof in about 1 second uh if we use like something more power than

M2 marks we can do a proof in you know slightly faster and then if we go to something like which is not consumer grade but which is like a cloud grab it on instance with 64 course we can do it in uh half a second um now if we want to do recursion we can't use Blake three as a hash function we need to use something that is arithmetization friendly so in our instance we use rescue Prime optimized and you can see that there is a performance degradation because this is a obviously slower H har function so we need uh it takes longer time to generate proofs um so on an M1 it takes about 6 seconds uh on the M2 Max it takes uh about 3 seconds and the main difference is that it's GPU accelerated and uh M2 Max has twice the number of

GPU cores so we can run it faster uh and then surprisingly actually that M2 Max was like just 12 CPU cores and some and GPU run uh this proves almost as fast as a 64 core graviton so it's a very interesting uh tidbit of information now we're not done with optimizing uh I believe there is like we're working on a number of different optimizations where we plan to get this to you know on an M1 Pro reive proof done in about two seconds on a Max in one uh Second and you know gravit on it will be in one second as well and the way we're going to get there is like reducing number of Trace columns we have some ideas of how to do that replacing a hash function with a slightly more efficient One X hases that based on Rescue Prime that we're considering and

using V instruction in some settings so like there is enough room left in the optimizing this where we can get to these numbers I believe um so basically right now uh what this boils down to is to achieve our kind of Target of getting to two recursion 2 to1 recursion in two to the 17 Cycles we need to be able to do uh a single recursive verification and two to the 16 cycles and the question is can this be done in mid VM so can we get there um and this brings us to talking about the different parts of the verifier cost but actually before I talk about verifier cost themselves I need to explain a little bit about the architecture of miden VM so this is like uh an ey chart where uh this is like the layout of the miden VM uh trace and this is a Star

based system so you generate a trace uh I'm not going to go over this all of this uh but there there are a couple of important parts first there is the main processor the main processor you can think of it executes uh it adds a single row to the trace for every instruction that you EX and these are simple instructions like addition multiplication you know division whatnot uh so you get one uh one row per that instruction but sometimes you want to accelerate some common computations and for that we have like this uh segment of the trace which we call chiplets and these chiplets do something you know uh very specialized computations they may take multiple rows per instruction and the important thing to note is that they run concurrently with the main processor so you can have uh something happening in the chiplets and something happening

in main processor and then you know they can be doing two things at the same time uh in the context of recursive proof verification for Starks one of the important order the main chiplet that we use is the hashing chiplet which computes hashes and this uh chiplet requires um you know eight rows per permutation of the hash function uh now with that in mind we can break down the cost of the verifier in two big buckets the first one is hashing this is in a stark proof one of the main costs so like hashing verifying moral pass primarily but there is other things that we use hushing for and the second bucket is everything else and the reason I broke them out in this way is because hashing is done on this hasher chiplet uh and everything else is done on the main processor so if we can get uh both

of them kind of using uh less than 26 rows we can we're successful um with hashing like let's examine hashing first so how many hashes do we need to generate uh to verify specific proof so here's a table of programs of various sizes and this is again using the parameter set that we used before so let's say if our program is 2 to the 12 Cycles we need about 3.6 ,000 hashes to uh verified and this is most of this go for fry verification but there are other hashes as well uh and then if the program size grows to 2 to the 22 we need about 7.2 th000 hashes uh and they translate linearly into the number of rows in the hasher chiplet so you just multiply by eight and you would get you know somewhere between 30 and you know 60,000 hashes that you need uh

rows that you need to verify uh proofs of this size and the nice thing is that you know this actually falls within the Target that we have set out for itself so we are under 2 to the 16 so from the hashing stand point we're good we we can achieve our Target we're actually not going to uh go beyond the the limit that we set for ourselves um let's talk about the other costs like everything else that we need to do and this is happening a lot of this is happening on the main processor there's uh obviously um offloading to the hasher as well but this is like uh things that need to happen not necessarily in the in the order in that which they happen and also I'm skipping some of the uh things here but you need to verify constraint and um or trace and

constraint commitments we need to load the out of the main frame we need to evaluate air constraints over the out of the main frame uh we need to generate some Randomness um or PUD random PUD Randomness for composition of different uh polinomial uh we need to compute this polinomial so dip composition polinomial and there are few others uh and then we need to run fry verification so at the high level these are the steps again not necessarily in the order it happens and also I'm skipping a few simple things here but these are the main uh costs that we're incurring and actually I'm going to skip over to like how we do optimizations if we think about which are the main bottlenecks here is these are the these three evaluating air constraints Computing the dip or verifying the DI comp composition polinomial was computed correctly and

also fry verification so let's go through some of this and I'll explain how we've optimized some of this in a context of M VM so let's start with fry verification and fry for those who uh kind of I'm not going to explain the full fry protocol but basically you take a polinomial you kind of fold it uh into smaller polinomial and then you end up with a remainder and then you check the degree of the remainder at the end so this is this picture is meant to illustrate that um and the verifier needs to do a few things the verifier needs to for each um kind of layer it needs to verify that the folding was done correctly and here the question is what is the optimal folding factor that you want for recursive proof um and the second one is that we need to verify the degree of the

remainder and here is like what is the optimal remainder degree that we want to verify and how we can accelerate this so uh let's start with the remainder for the remainder the usual approach that you do outside of the kind of zero knowledge based VM is you interpolate the remainder using an NTT algorithm uh you get the polinomial coefficient form and then it's trivial to check that you know what is the degree of that polinomial this is pretty expensive to do like running entities in mid and VM is fairly expensive a lot of stock manipulation and so forth so what we do is uh for optimizing we actually don't do the entity inside the uh VM We Run The Entity outside of the VM then we provide the result of interpolation to the VM non-deterministically uh and then we use this neat trick of of uh bicentric

evaluation that we can verify that um what we provided nistic is actually an interpolation of the of the input of the polinomial and this actually very efficient in the context of mid VN for example you can verify the degree you know a polinomial of less of degree less than 8 in about 3K Cycles uh and in our context a polinomial of degree less than um 8 is basically 64 evaluations because we're in a ax blow up so if you have 64 uh evaluations you only need 3K Cycles to verify the degree of that um the next thing to optimize is the folding procedure uh or verification of the folding procedure so the challenge is there is that lots of arithmetic operations in the extension field um and there is a kind of tension

between uh if you choose a higher folding Factor uh your Expressions become more complicated so you don't need to do more math and uh there is uh but you also can do fewer uh folding layers so you know you need to figure out what's the optimal there and overall we tried to do do this it's very expensive in our kind of first implementation it took 10 10,000 cycles for a single folding which is you know you need to do some number of the foldings depending on the size of the program sometimes five sometimes seven and this results basically in just the folding part will put us over the budget uh of what we want to achieve so the way we optimize this first um we introduce new instruction because we control the instruction set fully so there is an instruction to uh do a multiplication

and extension field uh second we introduce another instruction which is actually much more powerful even than the first instruction it does the entire fry folding um by by a factor of four in a single cycle so previously this would have taken like 100 cycles and now we can do it in a single cycle it's like an instruction that takes like 16 inputs and produce 16 outputs uh and we can do it because like the stock is 16 elements uh wide or what the part that you can access is 16 elements wide so this has helped us a lot um and in the end we get to something that we also can do a single folding in about 3K Cycles which is you know again very efficient so like if now if you have to do you know seven layers of holding you only need 7 * 3

21,000 cycles and we're kind of good in in within our budget um let's talk about the next thing the Deep uh verifying the Deep composition so I'm just going to show this expression this was the original expression that we uh kind of an original protocol that we used for um you know Computing the Deep composition I'm not going to go over the uh parts of this expression because uh this is just to illustrate how complex it was but the idea is what the challenge is again we have lots of computation that we need to do uh they're both an extension in the base field uh and you know there are many variables to keep track of there is a lot of random values to generate um so also very expensive in m and VM uh optimizations that we applied uh I would break them into two buckets first there

is kind of protocol improvements that have happened since we implemented the first protocol so for example removing the conjugate check we don't need like there's a part of that expression that does this conjugate check this is no longer needed or you know nobody's doing this anymore and the second one is removing degree adjustments so those also no longer needed uh third one reducing the number of random values that we use to combine um you know combine the polinomial together so that by itself simplified that pre the expression that I showed on the previous page quite a bit uh and then we also introduced two new instructions that help us Computing this random linear combination of this polinomial and you know um those two instructions also each cut out like between 30 and 40 Cycles so whatever was happening in 20 or 40 Cycles can now be done in a single

cycle um and this helped us a lot but before I show the results of like all of this let me um talk about the evolution of constraints this is the last thing that we uh tried to optimize and actually this is still in progress so the challeng is there is that for one we need to write this evaluation Logic for constraints in miden assembly uh this is both challenging and also difficult to maintain and one of the reasons why it's difficult to maintain is because we're still evolving the constraints we're still modifying things and U you know optimizing here and there reducing the number of Trace columns and modifying the constraints in M assembly uh like writing them in the first place is difficult but keeping up with all the changes is even more difficult so this is just a not a viable solution so our

approach to this is to write constraints in air script and then use a back end of airpt like M assembly based back end for air script to kind of output the optimized mid uh assembly code for evaluating constraints and this is still in progress um we're still working on this uh but just to give like a overall overview of the air script is that it's you know a language that um can be compiled to ir and then the can output different different backends so like you can uh in the middle there there is mid assembly backend which could be used to Output evaluation Logic for constraints uh for whatever is described in a script and the idea here is this is you know the source code is readable auditable Al also much more maintainable we can apply some optimizations at the IR level and then some very back and specific

optimizations that for example miden uh know how miden VM Works to like output the optimal evaluation code for a given algebraic expression um so to share a few results so first this is kind of like if we wanted to execute the a program of 2 or verify execution of a program of 26 Cycles this is how many cycles it would take on the main processor and in the hasher to do so uh you can see that fry verification at the bottom there is by far the most expensive one it requires 2.6 K hashes uh and it requires almost 20,000 um Cycles in the main uh in the main processor the next one is this deep polinomial composition doesn't require any hashes but requires 8,000 Cycles on the uh main processor and then you can

see the other things the constraint evaluation is um still TBD uh and there is some things that we can still optimize for example generating random coefficients um and kind of query indexes I think can be improved quite a bit from what we have there but overall we can see there is like around 5,000 hashes and if you multiply it by eight we're within 40,000 rows roughly for this type of program and you know about 37,000 uh Cycles on the main tray so both both of this are within range and uh basically we started with original question can we do a single proof verification in two to the 16 cycles of mid and VM and the answer is that yeah we can do this if the number of cycles that we need for evaluating constraints and there is a typ of here should say evaluating not evaluation not evaluation

but if we can do evaluation of constraints in less than 30k Cycles then we are within our Target and from what I kind of know about the mid constraint and like thinking through again this is not fully implemented yet but uh looking at our constraint system uh understanding how we can implement it in mind assembly I think this is totally doable so we should be able to get into our Target of doing recursive proof verification within 2016 cycles and um yeah that's actually my talk happy to take any [Applause] questions does anyone have any questions

thank you bobin after so many years again I used to work with bobin by the way at Facebook for the Libra project and then he went to polygon of course um so I have a question about the folding on the on the fry protocol right uh if you go back to that slide you mentioned that um you having this uh new instruction like the Fry 2 F4 and you use the folding factor of four is this the optimal uh So within M VM it is optimal so we try to play around so like if you do folding Factor two for example it um there are too many layers and um you know the cost increases folding factor of four like you could go to folding factor eight but in our context it doesn't fit on a stock so we can't uh do a single instruction

for this so our stock is like the access part is only 16 elements and if we wanted to folding by a factor of eight we would need more than 16 elements as inputs uh so um in the context of miden VM it is uh optimal to do it fold by four I would say when we do it outside of miden VM we actually do fold by eight this is more optimal outside of the uh VM and I would actually say there is um um we don't do this right now but you can have a kind of like custom folding schedule where you fold by different factors at different layers and that could give you another 30% Improvement based on like what we uh kind of experimented with we don't have this implemented but it it like if you have like Dynamic folding factors you can get

a bit more improvement from out of that thank you totally makes sense okay we have another question over here yeah I was going to ask about your choice of 16 uh elements in the you said you have 16 elements in the stack that you can access and I was going to ask if you could explain that decision and then also the alternative between using a stack based architecture for miden VM versus other architectures yeah so um the choice of 16 like it's it's a good question because it's hard to tell what is optimal um we've and it goes back to let me go so like you know this main processor basically this is where the 16 uh accessible registers leave so to say

um we chose this because first first of all you want to have as few of them as possible because you want to minimize number of columns so the tension is between trying to have as few as possible but at the same time provide enough of the flexibility where you can execute more complex instructions so in our case 16 kind of worked out well because we have instructions that require you to have you know more than just a few more than just eight or let's say um we have some instructions that require 12 elements on the stock some instructions require in this case all 16 elements on the stock and so forth so um for our purposes uh 16 kind of worked out well we could go in add more but that will add kind of more columns to the trace and increase the cost of the

entire system reducing it will mean would mean that we need to give up some instructions and this instructions are fairly efficient so we don't want to do that now the question is you know what is the benefit between stock based versus other architectures I think we will have a talk about this later today and he will explain this in much more detail but uh I think uh there are a few few pros and cons so stock based architecture allows you to have some of the more complex instructions so like uh you know you don't need to specify the offsets for the operant so like in a register based or uh other architectures usually have two operant that you read and then uh perform some operation you write the result because you need to specify where the operants come from and where they go and things like that in

the stock Bas architecture like you work with things that are at the top of the stock already so you can uh kind of have more flexibility in how you design the instructions and instruction said you can have this instructions that take 16 elements and do something with them uh and you don't need to specify 16 offsets they're all kind of on the stock already the downside of the stock uh architecture is that you do have a bunch of stock manipulation instructions that you have to do uh to arrange the elements correctly on the stock and they can take up quite a bit of Cycles so it could be like twice as more expensive to run the uh stock Bas architecture versus something else in some cases but it is very context dependent any other questions

um what's the field size for your Stark so we use um what is called the gold Delux field so 64 bits the 2 to the 64 minus 2 to the 32 + 1 and uh for the challenge you use elements from that field so the for for the challenge because we're in the 100 bit security level Target we can use um degree 2 extension of the field so we're basically in a 128bit field uh for the challenges thank you we still have a couple more minutes if anyone has any other questions okay all right thank you so much bobin thank you [Applause] everyone