ZK8: The power of multiset checks in STARK-based VMs - grjte - Polygon Miden

Transcript

foreign next up I want to introduce gershta from polygon Maiden who's going to be talking about the power of multi-set checks in stark-based VMS so welcome gersta thank you is this for yeah great so um what does this mean I'm going to talk about some optimization tools that you can use inside of a stark based VM to essentially do a variety of things more efficiently and in particular I'll start with sort of a general overview of those tools but then we can look at some things that we do in mind and VM using

them to allow a practically unlimited stack depth performing large numbers of range checks efficiently and single cycle Merkle path verification so we can start out by talking about what multisex set checks are they're based on multi-set equality which is um the idea given two sets they're multi-set equal if uh they contain the same elements including duplicates but possibly in a different order so one is a term mutation of the other I'm sure this is review for most people here um and how do we go about actually doing the multi-set equality check so we'll have an interactive protocol where first our approver commits to two sets you can consider it to be a vector of field elements a one through a n and another Vector of field elements B and then we

will get a random value beta from our verifier and then we'll perform a grand product check just like the heart of Planck from the Aztec team and the way we do this is by offsetting each element from a with our random value beta and multiplying them all together and then we do the same thing with everything from set B and if these two things are equal then with high probability we have multi-set equality so how do we do this in starts the first thing we'll do is put it into an execution Trace when we're looking at a stark we're going to start with an execution trace and a set of constraints that we apply to that execution Trace before we perform the rest of our arithmetic station so now we've got our two um sets and again we want the Pervert to commit and then we will get values from

the verifier and do our grand product check but we need to build another execution Trace to do that grand product check and so we can't do this exactly with a regular error we need what's called a randomized error where we'll commit to this main main Trace which is you know our execution trace and constraints We've Got A and B our permutations of each other then we get random values from the verifier and then we build a new auxiliary I'm calling it the auxiliary trace and it's another execution Trace with some constraints on it and this is where we do that grand product check so we can do this with a running product column where we say it starts at one and at each cycle we'll multiply in the value from a shifted by our random value we will divide out the

value from B shifted Again by the random value and you can see that if we're multiplying in and dividing out the same things we should end up with one at the end and so this is what the constraints look like that we need on our running product column we just need to have two boundary constraints at the beginning and the end and then this the laser is what I was going for then we have our transition constraint here where P are running product column at the next row is equal to P at the current row times the value from a divided by the value from B and from now on I'm going to show this main Trace that we can put two first in black and the auxiliary Trace that we do in the second half after getting the randomness will always be in purple

so now the next thing that we would like to be able to do is do a multi-set check between two subsets instead of having all of a is a permutation of all of B we actually only care about say you know four values and all these dashes are just values we don't care about we'd like to skip them so how can we do that we can do that by using selectors to identify the values we do care about and the ones we don't and we'll just add two selector columns and set it to one when we want to include the value in our running product and zero when we don't and now we'll compute some intermediate values so instead of including a plus Alpha into our running product we'll use a selector to choose when we include it and when we don't want to include it

we'll just use one and our running product doesn't change and this is now what that transition constraint looks like same as before but now we've got our intermediate value instead of just a straight up value of a and there's one more thing that would be really useful to be able to do before we can actually look at these optimization tools I promised and that is let's suppose that we have a tuple of three elements instead of just a single element in our set a same thing in our set B uh we'd like to still be able to do checks over this and to do that we need to compress these these rows these sets of values into a single value and once again we'll use random values from the verifier so once again our approver commits to a we get some random values and now we will just do a linear

combination and shift this again by a random value so we'll compress everything and later on I'll refer to this as compressing the row into value for the rest of the talk and now this is the first tool this is sort of a mental model that you can think about for how we can do things efficiently the goal here is let's say it's cycle T I have a b and c in my main trace and I know that I want to use them later but maybe not for thousands of Cycles um I don't want to have to keep them in my main trace the entire time in between because I don't need them in between so what can I do to use them here and then use them again down here and make sure in between that I actually am staying consistent maintaining consistency so the idea here is to build a virtual

table and by virtual I mean it does not go in the execution trace this is just in our minds here and in our implementation and I'll just add a b and c as a row to the virtual table and later when I want them I'll remove them from the virtual table and now I can construct this running product column to actually keep us honest and make sure that everything is consistent here I'll compress this row into a single value and when I insert to the multi to the virtual table I'll multiply it into our running product column and when I remove it from the virtual table I'll divide it out of the running product column and so what you should be able to see now is that when we are actually consistent there and here our multi-set check proves this and these are the constraints once again

we'll use some selectors to make sure that we actually construct these values correctly our value for insertion our value for removal and then this is the running product transition constraint for that and I'm not showing the boundary constraints of any of these it's because it's the same we're still saying it's going to be one at the beginning and one at the end this is the other main tool that we use to enable a lot of our constructions we call it a communication bus the idea here is you've got two different segments of the trace and you want consistency between them so you can think of it as there's sort of one segment of the trace that maybe is doing your main computation maybe it's your Sac or your processor and you'd like to offload things that will be expensive here into some sort of specialized uh

component in the trace that can do them much more efficiently so an example might be if I want to do a bitwise operation I could have a specialized bitwise component I'm just going to call these the requester and the provider and the idea is here I do an operation on a and b and I get the result C and the prover sets this result non-deterministically and then sends this request to the bus and then the provider actually proves that the computation of a you know a operation b equals c so the requester is going to divide out the value from the bus and the provider is going to multiply the value into the bus and once again we'll see that everything holds and this is what the actual constraints on that bus look like at this point we've again got um a selector to say yes we want to send

this request now we've got a select over here saying okay we've computed it and we want to set it back and then we select and you may notice there's a little bit of an error here this should be um r0 from the next row rather than R2 but we're going to select the values that we send based on um The Columns there so uh and and here again is our running product transition constraint it should look very familiar at this point we've got our bus value in the next row equals the bus value in the current row times the value from the provider divided by the value from the requester and now we have everything we need to actually look at the constructions that I mentioned at the beginning so virtual table communication bus are the main things that we're going to use and in my

item we can look at how we have practically unlimited stack depth using just a virtual table uh so here is a stack execution Trace some stuff happens early on and I did not mention this earlier but these are clock Cycles we're starting at cycle zero and going to cycle n and most of you hopefully grabs that from the execution Trace uh so let's say at some point we have the state of the stack is is like this this is the top of the sack s0 and then S7 and now we want to actually push another value on so normally we got to push a value the stack is full we're gonna have a problem um and the Stack's going to overflow instead what we'd like to do is say okay we'll just take this value 20 when it falls off the end of the stack and we'll

put it into a virtual table so we'll just create a new row that has 20 in it let's give it an address so we can keep track of it later so we'll use this clock cycle for the address and let's point back to the last row in the virtual table in this case it's the first row that we're adding so we don't have a previous row so that's fine so then we compress this into a row into a single value and we'll multiply our running product column with that to keep it in there uh we'll push again and now we've got 12 is going to fall off so we'll add to our virtual table so now we have two rows in our virtual table and we'll multiply that compressed value in and so you can see that the the product of the elements in here in the column is

exactly the set of rows that are in our virtual table and finally we will drop and so now the stack shifts back to the left and we would like to put our 12 back onto the end of the sack here so we'll remove this Row from the virtual table we end up with something that's just a single row now and when we remove it we divide it out so this is exactly the same virtual table that I showed earlier but now you can see how it's used to enable stackdep that is essentially unlimited um one really interesting thing that we get from this so far we've been looking at all of our running product columns they start at one and they end at one but actually that doesn't have to be the case what we could do instead is we could consider pre-loading this table at

the beginning of execution and then so we sort of create our table and we set the values at the first row of our running product column to contain the values representing the resonance table and so as long as we have the correct boundary constraint we can have something else in this table when we start and we could analogously do the same thing at the end we could end without actually emptying that table back off and um they don't have to be the same either so we don't have to end with our zero times R1 so to summarize the sac overflow table we've enabled practically unlimited stacked up with just this virtual table construction um we don't need to start and end it with one we can pre-load values and we can have values at the end and those starting and ending states do not need

to be equal the next construction I will bring in a communication bus for this one so this is a range Checker it is more complicated than the last one because we are adding the bus and the virtual table together so let's start by thinking about how you would go about doing range checks um so an 8-bit range check we'll start at we'll have some set of values these are the values that we're range checking and we will have some set of constraints over this sort of range Checker construction and I won't describe all of them but one thing that will require is that we start at zero we end at 255 and at each line at each row we either increase by one or stay the same um so now to do to provide range checks the bus this only shows providing the checks

it does not show somebody requesting the checks there's nothing being divided out so this is really just one half of a transition constraint to provide checks to the bus we're just going to multiply in V shifted by our random value um there's sort of a problem with this because if we want to request we actually now need to request every single value that's in here even if the requesting component doesn't actually care about having a range check for that value another limitation is that now this we can only provide as many values as the length of the trace as many range checks as the length of the trace so we'd like to do a bit better and the first thing that we can do to do better is to add send selector columns to Define flags and we'll let these flags tell us how many range checks we're

actually going to send to the bus so when we have two zeros we'll say that's you know this flag and we'll send zero range checks to the bus or we could send if we have two ones we'll send four range checks to the bus so now we have a lot more control if there's a value that nobody actually cares about range checking nobody's sending requests for it we just set zeros in here and um they don't have to be sent to the bus and this lets us do up to four and rain checks because we now have a way of sending four values instead of just um one value at a time this is what the transition constraints look like for this again this is just sending the values this is not the requester side of the constraint you can see here when our F3 flag is set here to send four values

we send V offset by Alpha four times so now things to start to get even more dizzying as we try to provide 16-bit range checks because 8-bit range checks really aren't good enough and so the last uh the last construction kind of lets us down so this is the big picture of what we really want we really would like to have somebody that can um request six team at range checks anytime they want they send them to the bus so you can consider maybe this is the stack and we send over four range checks um to the bus and here we need to have some 16-bit range Checker that provides range checks so what's going on here is this 8-bit section is exactly the same as what we just looked at I've added one

new column and this column is zero when we're doing the construction we just looked at with eight bits and it's set to one when we're in this new 16-bit section so we're only going to provide range checks from this 16-bit portion um so from the sax protective we request them over here we provide 16-bit range checks and now what is going on here well what's going on is that we're using the 8-Bit range Checker to range check differences between the values in the 16-bit range Checker uh the reason that we're doing that if we considered just extending the 8-Bit construction that we had we'd have to go all the way from zero to sixty five five three five stepping up by one or by zero each time and it's just not practical it's super long there are a lot of

values we'd really like to be able to skip so this is how we can skip them in here we're going to put just the values that we actually care about and then we'll use a virtual table to um we'll calculate the difference as an intermediate value and we'll just range check the difference using the 8-Bit range Checker so this virtual table is being used for internal consistency on our range Checker um there is one caveat here which is that our 8-bit range Checker can only range check up to 255. so if imagine say the stack wants to know wants a range check for four and it wants a range check for 500 we can't actually do that without filling in a value in between so we can have a gap of at most 255 here which is what's going on here this is what the virtual table actually

looks like we've got sort of up here this is adding two values to the virtual table so the 8-Bit range Checker can add zero one two or four values as we discussed before using these selector columns um and then the 16 bit can only remove one at a time because it's just removing this difference right here so we build up this virtual table that looks like this we add two zeros we add a one we and um and here's our running product column and then down here we start removing rows from our virtual table so we divide these values out again and so we should start at one we should end at one just as we looked at before and we've maintained internal consistency there so now this is the full picture of our range Checker uh we've got our requester sending values over here we're providing

zero one two or four sixteen bit range check values and here the 8-Bit range Checker is sending zero one two or four values to the virtual table and the 16 bit section is removing them one at a time and if this holds then we know that our range Checker is internally consistent if this holds then we know that all the values that we're range checking are in fact being proven um here in our range checker so the key points we combined this virtual table and communication bus these two tools for a more powerful construction um we can now send different numbers of requests and responses to the bus at each cycle by using Flags um from selector columns we can also use different constraints from different

components to do the same thing and we've enabled large numbers of arbitrary range 16-bit range checks efficiently so over 3n arbitrary range attacks for long choices and even with short traces where we have sort of fewer than n unique values we can do up to three n total values because of those columns that we had this is the final construction that I want to show you our hash chiplet using um a communicate a communication bus so we can with it do single cycle Merkel path verification and a few other things the first thing that you might want to do if you have a specialized hasher uh it's just a single permutation so we use rescue Prime as our native hash function and all we'd like to do let's say we

have the stack here which starts out with some initial state of 12 elements that's the size of the rescue Prime State and then we'd just like to get a permutation and so the next row in the sack is just going to be some is is going to be the result of a single permutation of rescue Prime so what we'll do is we'll send our input to the bus and then we'll also excuse me we'll request this input to the bus so we're dividing it we'll request this output from the bus as well and over here in the hasher we're going to do the same thing we will multiply them by the input and then here we will actually do this permutation we have the constraints that enforce that it happens correctly and then we'll send the output so the key here is that we're no longer sending

just one value from each side we now need to distinguish between an input and an output um talking about Merkel path verification let's say that we want to prove that D is a leaf in the tree with root G so we need to do a couple of hashes here and the key point is that the input now looks different than what it looked like before and we're also sending a different output so before we were sending the entire State now we're descending the middle which is the root node and so we kind of need to distinguish between the different hash operations that we're doing when we send these things to the bus we also need to distinguish between sending the input here and the output eight rows later versus setting the input here and sending the output you know some arbitrary number of rows later which is

going to let us have arbitrary depth um so that's sort of the summary summary of what we can do with our has shiplet we will Define mutually exclusive flags for each of them to find unique value computations and then perform everything else the way that we did before so we have some constraint that looks essentially like this we include when the flag is true we include that value and that gives us all of these benefits in the house shiplet doing a lot of different operations differentiating between the different types of values and all of the operations being performed in a single cycle on the stack and that is everything I don't know if there's time for questions but thank you all right [Applause] okay so I think there is some time for

questions all right we have one over here we actually have a few minutes if there are more um first of all thank you this was very very impressive talk um also this will be a new question but in the first part um where you have yeah you don't have to go back but like the communication bus where you were explaining this is this um all happening like uh there was a everything happens at the execution cycle of the stack so you also need to just include empty um I I'm trying to remember what was happening on the right side of the communication bus but uh so if you can

help me in there I think it's worth pulling up the picture yeah right uh yeah you so you had this specific proofer on the right side yeah does this need to happen at the same cycle frequency or no that's part of what's really cool is it doesn't have to so I can request that I can request something at you know let's say this is cycle four or whatever and I can actually calculate it way down here and send it back as long as it as long as it gets sent from both sides then our bus column is going to fulfill its constraints so they absolutely do not need to happen at the same cycle thanks for the talk uh how do you in the stock overflow table ensure that it is

not possible to pop something from the stock before you push it how do you achieve that kind of consistency yeah um it's a good question so we have a lot of constraints on address and the previous and what we're allowed to put into S7 here not a lot of constraints but we have a few constraints and we have a couple of we have three additional registers that we use to help maintain the consistency here and I just didn't have time to dive into it in person to talk but if you go to docs.io we describe it all in detail there and um you can get the answer cool anyone else all right well thank you so much gersta for the talk thank you