ZK Whiteboard Sessions - Module Six: Lookup Tables for Performance Optimisation

Transcript

foreign [Music] welcome to another episode of the ZK whiteboard series I'm Brendan I work at polygon and I'm here with Mary Maller Mary's leading snark researcher responsible for works like Sonic Marlin caulk stockpack and she's currently at the ethereum foundation welcome Mary thank you for the introduction so today I'm going to be talking about lookup arguments which are a key technique in the snark world to try and make provers faster we like that

um so with a lookup argument you would have some value w which is Secret you're trying to keep it hidden but equally you do want some kind of constraint on W what you want that it's included in some kind of set so and this set would be public so for example it might be zero three four seven trying to come up with a set that doesn't have any particular structure here um so a lookup argument would allow you to prove that W is inside this public set but it wouldn't reveal any of them any

other information about W cool so so where where might we use a lookup argument so a classic place where we use them all the time is actually in our snout constraint systems because often it is quicker to check that W is in some pre-computed list then to check all of the constraints on W that would lead to W being in that pre-computed list lookup arguments are also very very related to lots of other Concepts in the literature so there's a lot of over overlap with set membership proofs there's a lot of overlap with accumulators with Vector commitments no doubt there's some that have forgotten

but in the context of sort of trying to make snark circuits faster typically we would call them look up arguments cool so my plan for today is first to just run through an example of how you would represent a range proof and a constraint system and this is just to sort of try and get you familiar with how we would how we would actually like program these things I guess after that I'm going to be talking more about what to look up proof is what is the motivation behind them that sort of thing then I'm going to move on to talking about Vector commitments and how we might represent them in the standard

basis how you might represent them in the lower Branch basis these are very relevant to look up arguments um then I'm going to talk through the Halo 2 lookup argument and I'll be finished by presenting some of our new work which is in the cold color cup argument sounds great okay so for a range proof again we have a witness w and we're trying to prove that is in the set zero one I'm not going to write it all out

zero through let's say eight which is equal to 2 to the three and again W is private we don't want to reveal w this is a simplified example typically when you would be proving these range proofs eight would be something more like 64. but for this example I'm writing out on the board so I'm trying to keep it simple range proofs like this appear all of the time in snack circuits they're absolutely everywhere um and the reason is because we're working over a prime field piece and this means you get something called overflow errors

which can be really bad for cryptocurrency oh yes that can be bad so what I sort of mean by this is that if you have you have inverses basically so if you have the number four then it is certainly the case that P minus 4 exists so what you would do if a range proof is you would say that W is not in fact equal to P minus four because it's out of range so but not to delay with the point if if we weren't checking this then there are situations where I could mint like P minus four coins which would be pretty good you know two to the 256

minus four coins that's a lot of coins I I can retire on that one of the classic ways in which we would try and show that W is within this range would be through doing a binary decomposition so we would say that there exists values B zero B1 B2 all included in zero and one such that W is equal to

b0 plus 2 times B1 Plus 4 times B2 so we're we're sort of splitting it into bits where the bis are bits and and we can express anything in this range in that form that's where exactly that yes um these B values they're also private though because revealing v0 B1 B2 reveals W directly so you also have to keep those hidden and this means you get some amount of witness blow up because before where you had a witness of size one one element you now have a witness of size four

and this obviously blows up more with larger ranges okay cool we also need some additional constraints here because I've said that be zero and B1 B2 they're in zero and one but you do have to check that so the way that you would check that is you would check that 0 is equal to b0 times B zero minus B zero the only way you can satisfy this equation is if b0 is zero or one and you do the same for each of your other bits so guaranteed to be bits this guarantees

them to be bits but as you can see this is also blowing up a number of constraints in our circuit because we now have one additional modification constraint per bit and actually if you're in systems um Universal snacks where additional costs are no longer free there's also some addition constraints going on here so what does this look like in terms of like an r1cs Matrix um if we were to put this in terms of an r1cs Matrix which is a constraint system which is used a lot in the snap Cloud I think more recently A lot of people have been moving to the plant aramatization scheme but for this example I'm going to

explain it in terms of violence yes um sorry so r1cs really works in terms of matrices it's like a vector and Matrix type of argument so you have one Matrix Times by vector sorry one metrics multiplied by your witness vector Times by

another Matrix multiplied by your same witness vector so if I could keep my witness Vector the same let me separate this minus third vector Times by your witness Vector so your witness the vector appears three times and you're trying to show that this is all equal to the zero vector and you want it to be the case that we

can find a matrix here here and here that represents the constraint systems over on that side so how do we actually do this well our first constraint we don't have any multiplication Gates here so we're going to look straight to this Matrix and we see here that we have W equal to b0 plus 2b2 plus 4b2 plus 2b1 so this can also be seen as out 0 equals minus W plus so in order to represent that constraint

I'm going to have 1 times w Plus sorry minus 1 times B 0 minus 2 times B1 minus 4 times B2 and I want that to equal 0. there is nothing happening with the multiplication Stone constraints so up here we just have zero zero zero zero and zero zero zero zero our next constraint we have to actually enforce the binary constraint on b0 and this is a multiplication constraint so we're going to be working up here and really what we need to do is we just need to select out the b0 from each of

these matrices so that would just be zero one zero zero here and the same here zero one zero zero and then we need to minus it off so sorry one zero zero and the blossom Matrix the other binary constraints are all of the same so we do the same thing zero zero one zero zero zero one zero zero zero one zero zero zero one zero zero zero one and zero zero zero one and there you have it this would be an

r1ca where of trying to represent that W is between 0 and 8. cool yeah because we so we're enforcing the the W is can be decomposed into these uh bis and then that the bis are all bits and that's cool oh awesome thanks Mary okay so as you can see here we have that the witness has been like a bit blown up because of how we're having to represent these binary constraints such that the snap can read it I'm just going to now try and explain that in a more visual way and provide a schematic and wrap what's up here first foreign

you have some computation that you're trying to prove so I'm going to call this computation as a function s f is going to take as input a public value X is it okay if I erase up here do you think yeah it's also going to take as input a private value w the computation will output

y and then what your snap approver would be doing is it would be saying I know w such that f of x w equals y and really what you'd often like this to be in like real life I would say is like maybe a c program or a rust program like an actual computation however we do actually need this to be something that the verif that the approver can read we need to be able to snarkify it

and this means that we have to arithmetize our function and the arithmetization process is where a lot of the prover costs come in for snacks because we can't just use a lot of the operations that will that we have access to like an arrest program like there's no less than or greater than operator or any of these like anything except for additional multiplication right I yes there's lots of things that you don't have access to you also if you wanted to have an if Loop you would have to iterate both possibilities are in Europe Loop really and sort of say it's one of these two it's hard to jump around in

the program execution Trace there's there's lots of places where in order to arithmetize you have to do things in a different way so in doing so much like we saw in our binary constraint example you're going to blow up the size of your Witness so I'm going to write a bigger W in order to in order to represent this again private value and so this is what we saw earlier where we have we had we started with w and we ended up with a bunch of bits yes you might be there

only a bit it's only zero one it doesn't actually take that much storage in the snack bar that isn't true your bits cost the same as any other element in the field so it really does hurt and then we're going to have our function which I'm now going to call bigger um it's again going to take in a public value and actually the public value is the one thing which doesn't change much this because the verifying is this and we still want to know that the

output of this function which should be the same function just represented in a different way is equal to y nope sorry I know picked up you such that f of x Big W is equal to y and yes these two statements here should be equivalent if you've done your arithmetizing correctly so what does this do to like prover time or uh kind of things that we care about in practice it explains the proof of

time like not just a little bit either we're talking orders of magnitude proving this it was um the witnesses often like many many more times the size of this witness okay so so if we're doing a bunch of range checks then we might be in a tough spot because uh like from from an efficiency perspective uh I mean it's not undoable it's not like this can't be done because it is done it's just it is an area where the quicker we can get this the better we can get this arithmetization process the fast stress mark is going to be it's one of like the the key places to tackle um it doesn't however affect drift size

really and it doesn't affect verify time this is purely for the proof of time cool so hopefully there's a better way for handling range checks and so like something that that maybe will have like a smaller blow-up factor for our arithmetized circuit yes there are definitely better ways and one of the sort of really promising ways which has come out is to use lookup arguments no surprises there I'm sure um shall we rub this out so Mary what's uh what's the lookup

argument so before I sort of said that we want to prove that we have a private w which is included in some set zero through eight this set is public so what we can do is we can pre-commit to it we can set up a table with all of the values between 0 and 8. 8 so we generate a table and in the table we have zero one two three four five

six seven a very even table and and we can do this because we know that no matter what w is what we'll always have to check that it's between zero and eight and and so this is not something that depends on the witness it's something that we can kind of bake into our circuit yeah I think it is something which would on the circuit like if you're using these lookup tables I'm giving them in the specific case of range checks because they're one of the cases that come up all of the time but really what you'd probably want to be looking at is more what kind of operations in your specific circuit come up all the time like if you were trying to prove a hash

function then one of the things that you might want to store in your table is the possible outputs of the S boxes yeah yeah yeah I I just meant that like it's something that we can pre-compute once and sort of like bake into our constraints that we wrote and and then yeah okay cool yes no you absolutely can do that so yes then we've got our table I'm going to call this is equal to T and we just want to find a way of proving that w is included in t and hopefully with fewer constraints

then uh and hopefully and hopefully in a way which is more efficient than doing the full binary constraint uh binary decomposition cool okay so we have a table that we need to pre-commit to so the next thing I'm going to be talking about is different ways in which we might commit to this table mind if I come over here uh yeah so if we're sort of thinking in

polynomial notation which is something which certainly the zero knowledgeable World in general I'd say is moving towards more and more and more we would say that we have a polynomial f of x and we might want to commit to a set of values in a table a0 A1 let's just say A2 keep life easy by having them as being the coefficients of the polynomial a0 plus A1 X plus A2 x squared I would say that this basis is very good

for some settings but actually often in the settings that we're working in it's not necessarily the best way and the reason is because it's just a little bit more complicated to open right so if for example you wanted to open A1 the easiest way to do this would be to provide another polynomial say G zero of x and G1 of x and then you would want to prove

that f of x minus A1 of x is equal to g0 of x Plus G1 of x times pi x squared and that g zero of x has maximum degree zero so this would give you that A1 is indeed

the coefficient relating to X for f of x because this term cannot have an X to the power of one term but as you can see it's like it's quite convoluted like we've got degree checks we have multiple polynomials there's a sort of quite a few steps to doing this and there is an alternative basis called the LaGrange basis where you don't have to do this that's good I should actually keep this but but do you keep going would you like the f of x or yeah but

just yeah effects of your skin guy so a way that you can do this instead is you can say that f of x is equal to a zero l0 of x Plus A1 L1 of x thank you Plus A2 L2 of x where l0 L1 L2

r the LaGrange polynomials are the LaGrange polynomials over the set V is equal to Omega zero Omega one Omega 2.

I know these look like W's I will avoid using W's um for this section of the talk because they look so much like W's they're actually omegas they have nothing to do with the witness they're completely public they're usually roots of unity actually what's uh take me back to uh to abstract algebra what's a root of unity root of unity so this is a set of size not a power of two which is not helpful it would always be a set of size of Power of Two um but a root of unity would be a value such that w i to the power of n is equal to one

Ida whichever field you're working over and so we call that an nth root of unity that would be an out through to Unity okay I can't make this a power of two but pretend okay cool um probably you might want me to explain what a LaGrange polynomial is yeah that'd be great okay let me see this I think erase that actually I might need to erase both to make space um I'll try and rewrite rewrite out some of the the fact that we have that set B Because B is going to be important

sneak over here again there is equal to the set we'll make a zero Omega one Omega 2. and we have that l0 of x is the unique polynomial there's only one of them fully moon nickel Nick Polly

um such that l0 of Omega zero is equal to one L zero of Omega 1 is equal to zero and l0 of Omega 2 is equal to zero and so the the others are kind of defined similarly where uh you know if the indexes match it's one and if they don't it's zero yes yes and these polynes are named compute you have l0 of x

is equal to the product between equals zero and two I not equal to zero so actually a equals one to two but for the others I'm going to write it like that sure um of x minus Omega I or divided by the product I equals zero to two a not equal to zero of Omega 0 minus Omega I think

so yeah you can see here if you were to insert Omega 0 you would get one because it provides exactly if you were to insert Omega one then you have omega 1 minus Omega 1 in your product so that would go to zero one thing also worth mentioning is that when these are roots of unity these uh polynomials are very quick to compute because we have fast Fourier transforms but I'm not going to go into any more detail other than saying their existence here okay cool so how does the LaGrange basis sort of

save us when we have to open uh our Vector commitments well again we've got our public survey which I've conveniently dropped out if you want to be able to open S at A1 you would just need to prove that F of Omega 1 is equal to A1 it seems very convenient it is very convenient um and yeah this check is very easy to do in particular one way that you would do it when you're using kcg polynomial commitments is you would prove that f of x

minus A1 is equal to x minus Omega one times some equations not Vanishing quotient polynomial Q of x cool so yes when we're committing to tables this is how we would do it so we just uh so right now we have a table with three elements and we uh instantiate a polynomial of this form yes cool and then when we want to open depending

on our polynomial commitment scheme it can look a little bit different you've got pairings specifically if you were doing highlight two you wouldn't you wouldn't do it exactly like this yeah yeah cool uh so I would say keep this up here but okay I'll keep that one as well okay so I'm now going to talk about how this kind of polynomial would actually kind of be used in the Halo 2 lookup argument the um actually the idea to use lookup arguments wasn't originally halated it was originally a Planck idea the pluck-up argument and this is like a

really really good paper really sort of revolutionized how people do things but Halo 2 is quite a lot simpler so for the sake of a whiteboard session I thought it would be a better one to explain so again you have a table of values such as the one above but you also have another polynomial also over a LaGrange basis which is your polynomial committing to your Witness so this one's called f of x I'm going to call this a of x this may not be at all consistent with how the Halo 2 people are doing it in

terms of their notation so sorry about that an a of X is going to be equal to let's say be zero l0 of X so these uh bis are they like elements from our witness or like things that we're trying to look up uh these are elements from our Witness and actually a lot of the time they're going to be not values in your table because you're not interested in doing a lookup argument for this value and the way they handle that is via selector polynomials which I'm also not going to cover so for Simplicity just assume that every

witness element in your um in your computation is something which you want to be equal to either a0 or A1 or A2 okay so one of the sort of first problems that you're going to come across here is that these values be zero be one B two I should say visual if you want P2 it will want to be included an a0 A1 A2 these are not necessarily going to be in the most convenient order

like uh like b0 could be A2 and B1 could be a zero and exactly that okay I might even use a red pen for the first time I like Scott uh um put that idea out there like maybe you have this kind of structure it sure would be nice if they were because that would be the same polynomial yeah you might even have um repeats actually that's a that's a good point so you might have that both um both be zero and B2 are equal to A2 and this is an additional challenge

which you have to work with Okay so the very first thing that Halo do um to is actually going to do is it's going to permute these values such that they're in a more convenient order okay so we would want to have some alternative polynomial let's call it a dash of x which is equal to what do we want probably won't be one first which is equal to B1 l0 of x Plus B zero L1 X

plus B2 L2 of x but the proofer might not give you the correct value of a prime of X you you sort of really need to enforce that this that a prime is genuinely a permutation you don't care what permutation but you care that it's a permutation so the very very first thing they do is just a permutation argument foreign just to say

a prime of x is equal to um some permutation of a of x ah I probably need to make a bit of space again we'll keep the a prime of x would you like to keep this yeah for now okay um

so we got a prime of X we've already proven that it's a permutation of a of x and for now for the purpose of this session we're just treating a permutation argument as a black box yeah and now we have a much much nicer structure oh we have that um we have that b0 is now mapping to A1 B1 is mapping to A2 and B2 is mapping to A2 probably made life a bit difficult for

myself by not having b0 starting at a0 actually so I'm actually going to just change this and make life easy sure pretend pretend I wrote it out the the easy way first time one quick note I will add is the way they get around the thing whereas they're like I've made it difficult this stuff these area doesn't map to a0 the

way they get to the brand that is they actually permute f of x as well so they permute f of x to be in a convenient order as well as AFX to be in a convenient order okay okay and now our problem becomes much simpler or you simply have to prove two things we prove that either foreign of Omega 0 the Eva constraint isn't relevant yet that will come we prove that a prime of Omega 0 is equal to F of Omega zero

that's just like our starting point okay we then prove that um either a one prime of Omega 1 is equal to a prime a prime of Omega zero or a prime of Omega 1.

is equal to f of Omega 1. and we can see like the Omega 0 is picking out this value and this value to start and so we're just iterating through yes yeah and we will do this with Omega 2 as well okay I'm not going to write that out again for every value you prove that is either equal to the last value in a prime or it's equal to the value relating to f of x okay and because we've permuted uh a prime and you know theoretically F if we needed to we know that we're basically like picking out all of the yeah um

the one sort of way in which this is really nice is that you're just working with permutation arguments everything is fairly simple and usually what they're going to do is they're going to make it so that the size of the table corresponds very conveniently with the size of the witness um but if you do have it the case that you have like a very very large table you're always going to have it the case that this lookup argument is linear in the size of the table because you have to do the permutation argument and so yeah so it's like when we use lookups we sort of have to strategically pick a table size that is kind of optimal like we might use like you know

16 a table size of 16 or some uh smaller value so that we don't have to like pay the full cost of yeah cool so I've sort of explained how the Halo 2 argument is working from like a very very high level um with colqui we're trying to do something very different in the sense we're still trying to do a lookup argument of course but we're trying to beat that sort of linear time restriction we wanted it to be sub-linear in the size of the table which it's nice if we if we have bigger tables right we have very big tables but yeah but it becomes pretty nice Okay

um yeah we can drop this off and actually I'm also going to rub off f of x because I want f of x to have a few more um terms in order to be a bigger polynomial okay I might need to write a little bit smaller for it a bit um so let's say that f of x is equal to uh a0 l0 how many do you reckon I should go up so uh you know we could obviously just use like a an eye index let's do that okay is equal to the sum of I equals

zero to minus 1 of a i l i of x 4. bigger it's still not like big big in cryptography terms it's still like you know I would I would say that probably we can go up to two to the 28th which is still quite a bit bigger than it's like basically reasonable with um the Halo 2 style arguments or uh or pluck upward uh yes it is it works for like a lot of use cases yeah

um so this is now going to be our table and kind of I the key trick in calc I would say is that we still want to be working over sets of routes of unity and for sure f is divine we find over V which equals Omega I for I equals zero to n minus one but our idea is that when we have our polynomial a of x I think the notation we use in the paper is Phi so I'm going to do that here Pi of x

um is equal to the sum of bi we're still going to have it over a LaGrange basis versus LaGrange basis this is the give me a letter I guess W or all right T um W is going to be over same UI I equals 0 to not n minus one so what is Mu M minus one mu is a different set of roots of unity okay

W is going to be much smaller than V okay in this case so then we can have PSI of X is equal to be zero times a different set of roots of unity that we were using l am I going to use M doesn't really imply LaGrange I'll use Lambda Lambda I of x and we still want to prove that every bi is equal to AJ for some J but the thing here is that we're not going to have perfectly that Lambda I and Li are the same set and equally V and W are going

to be different sets so just from my understanding is the Lambda are those LaGrange polynomials over the set of muse or okay okay um so really what we're doing here is we're getting a different trade-off we are going to have costs which are going to depend on this m so the size of our commitment but they're not going to depend on the size of that table cool so and because m is more much more of an n in some cases yeah okay if you have a case where m is much larger larger than n then actually currently we have quadratic costs so you really would not want cheesecake there but if m is small then it works quite nicely okay nice um

okay so now we want to relate five x to f of x but our problem is that the roots of unity are different so what we're going to do instead is we're going to have some polynomial U of x which is going to select out the roots of unity from f of x which I like of interest to us right so I U of X is going to equal the sum of some omega i j I'll call it in order to indicate that it's not going to sum over all of the omegas only the ones that are interesting um

and so by by interesting is that just the set that actually we're matching on yes okay that's just to set that we're matching on and then what we want to do is we want to um prove that the Omega ijs Our Roots of unity and we also want to prove that for every mujay we have that f of U

of mu J is going to be equal to Phi of mujane and so we we have to prove this because there's no way in the circuit like without another lookup table that we could uh like guarantee that these values that we're providing are actually like part of the set of omegas exactly that yes but proving that the value is like a root of unity is kind of like very doable because of what a root of unity is right like remember that we have that Omega IJ to the n is equal to one

this is a very checkable relation you can check this in log n time to be precise and log and time just by using the square and multiply algorithm inside your constraint system and that's exactly what we do cool um so I I probably could go into more detail but equally I think I I won't I will just sort of finish by saying that

the overall complexity we get in terms of private time here is on the order M squared plus m log n we're very keen to get rid of this m Square term we sort of intuitively think that it should be possible but we've not figured out how to do it so this is sort of something which I would say like if you have an idea is what it's worth exploring cool and so right now I I think that uh my understanding is the scheme uh depends on some like on using pairings for like some linearity tricks yes is there like can you imagine a way where you wouldn't uh you could remove the

record the pairing requirement or is that it would be very challenging actually um just because like the way that we're making this check fast is by using the Casey Jake scheme we sort of say we've got this pre-computed kcg commitment which shows that F opens at this point to that point and then we just like prove knowledge of our kcg opening yeah if you wanted to do the same in a discrete logarithm setting you end up working with a proving system which has random oracles all over the place yeah and these are much harder to integrate in a sort of pretty way into your proving system yeah so again I don't think it's like impossible but there are

additional challenges that you would face cool so is there anything that's kind of on the road map for either caulk or or lookup tables that um that you're working on or is this sort of where I would say that we are sort of exploring can we get rid of the M squared but we've not solved it so I don't want to get your hopes up there uh cool well so I guess we to recap we looked at um certain things that are expensive and very common in circuits and and uh like range checks and how we might use techniques like look up arguments to make them less expensive and then we looked at the Halo 2 lookup argument and

then caulk um yeah this was really great uh thanks to Mary thanks to the ZK hack team and to everyone for watching thank you [Music]