ZK11: Natively Compatible Super-Efficient Lookup Arguments - Matteo Campanelli

Transcript

[Music] hello folks um hopefully if I play my cards right I'll finish early and hopefully if I play my cards right I'm not going to confuse you except in one slide so this is join work with a few other people that F jaran man Jun and hopefully we're going to get the only print soon we're we're going to get the only print soon so the topic of this talk is new constructions for lookup arguments so I hope some of you have seen lookup arguments before but just as a refresher there are specific type of narc for a very specific type of

relation and the relation looks sort of like this we have a table that's supposed to be even arbitrarily large depending on the application and then we have a commitment at the table actually the verifier can hold it so it's done a PR process in time once and for and forever and then sometimes I want to prove that a certain set of values is in the table this is actually a multi set here it says a set but I mean there could be repeated uh instances inside F all right and that's my proof P lookup so I give two commitments one is a pre-processing time one is a proving time and that's what we get now lookup arguments are pretty useful because for several

application to to some extent they obstruct something that's close to batch membership proof so if you have a set of users think of uh permission lists or block lists and you want to prove that s subset of the users is in that list or not you can use look up arguments but also they're really interesting usually because they get as faster snarks how do they get us faster snarks well this is what lookups outside n Fields so computer science are good for so you just look up the resultant of my operation instead of actually computing so instead of representing something with constraints for example we can just pregenerate our table of operations and

then we're good to go so that's what they're good for uh one example okay so one example in that sense is take the exort table here for the case of for bit just this our T from the slide before yeah okay so two this dat we often want in lookups are some form of efficiency that they call Super efficiency here I'll talk about it and the point of this tall compatibility all right I'll introduce both of them so super efficiency is very simple to understand we do not want the prover to work linearly in the big table so at proven time I want the prover to work yes linearly in F but I don't want it to

run linearly in t that's the thing so I want it to be complete independent now it's sort of counterintuitive I'm proving I'm going to prove a statement about the T can I even do this yes you can the important thing is that okay this is I'll tell this in a second the important thing is that you preprocess you need to pre you need to work in that n at some point so you need to preprocess stuff store it and use that auxiliary information later so of course when do you care about this well for example when f is substantially smaller than n which depends on the application of course all right so if that makes sense so not it's not trivial to obtain super efficiency it's not trivial that

you need it either all the time but it's not not all constructions have it so here's a list of constructions which do have super efficiency in the sense CQ CQ plus which is just an improvement on CQ lasso which achieves that type of efficiency only on tables with a specific structure uh so they I don't have the technical definition fresh in my mind now but basically you can decompose the algebraic representation of those tables in an nice way call plus Balo and fluk and so other deployed proof systems also don't don't have it but still useful okay so that's the first deser item the second dis item I'm going to call it

compatibility and that's to do with how we use lookup arguments with other proof systems okay so you may remember earlier I mentioned these two applications right so let's use I'm going to use the faster nark application as an example but everything I'm going to say here also holdes for the setting so we want to achieve faster snarks for some computation okay that's our computation it does a bunch of amazing things and then if we want to use lookups we can sort of split into two blobs the first blob that I call the general purpose blob so it can be arithmetization or 1cs arithmetic circuits and such and the second blob the lookup blob which is going to be lookup is so as examples of the two the

the first the top part is going to be represented by R1 CS of some type and the second part is going to be maybe a bunch of exor or whatever yeah okay once you do that what you need to do to prove the computation in a fast way so you have the best of you want the Best of Both Worlds use your general purpose Nars for the first part is your lookups argument for the other one are we done not quite there is that bleeding wound over there which is the shared State between these two things so it's a computation it's doing something and you're going to have wires of course they're not independent you need to interface them you cannot use these as two black boxes and never make them talk so M but they need to be able to talk

and there's a bunch of ways to implement this and some ways are nice so they're going to link to each other nicely some ways are going to be less nice less intuitive I mean you can still do that but it's it's going to be more costly so let's look let's open the box of compatibility what do we mean here in actual proof systems right what we mean is that the two proof systems need to have some you can call it Comm and proove compatibility of source so both of the proof systems are going to use polinomial commitments right this is we saw that in the last talk we we know them as a basic building block is NS they need to be compatible so what do you mean let's think how do we use polinomial commitments in snarks so in snarks some snarks often the first thing

you do you take an encoding of the witness and you commit to it okay this encoding is a polinomial and then in lookups what you do you do something similar the first thing you do you commit to an encoding of your F the thing you're looking up into all right so there are different types of encodings and different types of commitments right so on the top you can see the lren coding with LR interpolation for Univar polinomial but then a bunch of proof systems use the hyper Cube as represented below this leads to different encodings different polinomial different polom commitments which are going to be the two handles over there you want them hopefully to be the same type so you can make them talk

efficiently so this is what I mean by ntic compatibility it's not a technical definition but if the committed polinomial are of the same type and over the same field all right so let's see examples of compatibility and incompatibility in this proess so for example plun works pretty well with a bunch of those for examples and if you read the hyper plun paper it's nicely modularly structured so there is hyper plun which is the proof system for R1 CS proper and then hyper plun plus which is hyper plon which is able to talk with an additional module module which is the multi sorry that was a

[Music] mistake which is a variant of plup for multivariat so for that's one case in which you need to modify the lookup argument to make it talk and then of course trivial examples of incompatibility take the bottom left and take the top right over there okay so if that Mak sense uh you could ask fine can I can't I use the two modules there anyway so what happens if they're incompatible are we doomed of course not they're not you can do something you can apply a snark on top of the shared wound and and do everything but this is less simple this is the point of of this whole thing you are free to do that but then you get way

more complex in your system it's less efficient you need to modify apis interfaces and maybe security properties too you need to be cautious and of course maybe you're losing efficiency so we want to save in those two Dimensions all right so what are we trying to do here we're trying to look a look up arguments with both of these this there and so for example why do we care because if you take why do we care about proof systems such as hyper plun that are multivaried based they have linear complexity for example and if you care about hyper plun you may want to use it so now the proof system that's using the

hyper plone paper is this modified plup I mentioned which is not super efficient there're so the only super efficient lookup I'm familiar with please come to me if you know others that um that is multivar based is for example the the lasso look up but lasso is superficial super efficient only for specific type of tables so what we want to construct is a proof system that's super efficient for any type of table and is natively compatible with this yeah and so once you have this you can you know plug it into proof systems like the one before hyper plun Spartan and

just do but there are others cool so what are the constructions I want to talk about so the first construction is a direct construction it's called me you hopefully get the reference and it's a direct construction whose techniques are based on CQ and it's modular so you can plug it in you can plug in any multilinear polinomial commitment Kingdom and it's going to work as your handle interface so the second construction is actually a compiler so the first question you could ask yourself when you so my life from before so you want these two handles to be compatible fine we have these other lookup arguments that are univariate and nice can't you just transform all these cool systems into another Well actually

there are a bunch of simple techniques to do that some of them have different tradeoffs and the general compiler we propose is one of these systems and I'm going to show you more about the compiler but what does the compiler do it takes in input a super efficient lookup argument with Vari polinomial commitment as interface takes a multivari polinomial commitment with very simple property needs to be on the same field and it gives you a super efficient lookup argument with multivaried polom commitment so blackbox okay and there are no fireworks there you're going to see how it works you're going to nod and say okay that makes sense hopefully uh and yeah you can instantiate that with whatever you want so right so you can instantiate

that on your favorite lookup systems with univ futures um I'm not going to talk so much about the efficiency of this second construction but in general is sort of as efficient as mysic but it since it works blackbox it does more stuff it doesn't look very well at what you're doing so if you probably you're going to be better off using the first one in many cases yeah okay so some numbers um if you care look at the rest of the table but I will focus just on the last two uh rows so the last row is our work and then you can see lasto FR structure tables we're going to talk about lastone structure tables later more but so what

would I want to take from this the fact that the prover does linear linear job in group operation and field operations and you can have a rough idea that I have concrete constants here for our proof systems I don't know the concrete constants for ler I don't know if they're easy to extrapolate either so if you want numbers for example say you doing a lookup of around 1,000 your proof is around few kilobytes how much does it grow if you increase that doesn't grow much so those logarithms so act is they tend to do logarithms sure so some technical intuitions I'm going to give a very very superficial perspective on the first construction and they're sort of most of

the techniques of Music are techniques of CQ I'm just going to mention The Usual Suspects so the S Check LMA from Aurora the lookup LMA and cach quotient if you've never seen this I'm not hoping it's going to make sense to you now but if you've seen it you're just going to recognize it the cash qution techniques from CQ so how do you use these guys I mean one also this a usual suspect you would expect you put them with the Su protocol now CQ as it is you cannot quite transform it directly but if you look C CQ as um HP or polinomial you can sort of see this transformation sort of EAS and we care

that's that's mysic basically instead I want to talk about thec compiler which I have some hopes of bringing so to get in touch with all right so what's the compiler trying to do the compiler is trying to get univ polinomial commitment sorry a lookup argument with the type of interface and a multivaried polinomial commitment and give me that so I want to achieve a proof system where the interface of my verifier is Su and coding of this F over here of that form so me is referring to the multivar case nice so that's the interface of my verifier the verifier holds this just got it from the from the approver in brackets I just mean the commitment to

that uh also have some other shapes to to make the relation clear so those are the same those are the same fine so what's the first thing that the prover can do the prover can use the building block over there so I can use a lookup argument for Univar polinomial sure so the prover can send the proof for Univar lookup but with respect to what polinomial so I need to send a polinomial first so it sends another commitment to F to it's a vector is he then Calles it with lrange interpolation as a Univar Pol nomial it send it it's sort of done the job is done except so yes that's the

same so what's left is this very simple property that we need to show we must show that those two commitments refer to the same Vector okay so what do these commitments look like they are brackets so they commit to these two polinomial respectively yeah so hyper Cube on top and L the bottom what do we do we do um we're going to do a S Check of search so we're the we just sample random Point Sigma and then I'm going to use some I take a random evaluation in the point of the univ polinomial and now I'm going to link it

to something else so you can see that if you open the box of f univariate if you look at the second row that's what it looks like and so B it's basic basically a linear a linear combination of the type so it's the FI points and the Lambda Grange pooms in Sigma that's it so I have a commitment to F that's the the top row a commitment in the multivariate thing I just need if I have a commitment to the second thing to the Lambda in Sigma I'm done so let's have it peits to it with a multivar thing and then it needs to show show it has the right shape that's all that's

left and we do now this is the moment that all intuition all intuitions are sort of going to be compressed here it proves that it's actually of the right shape you can see it here roughly we're using the H is this is uh this is a multilinear encoding of um of my domain for the univ polinomial uh this is run then you can see challenges over here here and so on and so forth so we're just checking that linear the linear product over there and the right for and this is the compiler this is it so run the sound check on that and you're done I shouldn't have done

[Music] it but this it okay so what should you bring home about whether this stuff is useful or not is useful all the time well so remember the first I don't know if I have a picture here I do I think so let's talk about SAR architecture I I will submit to you that this is useful if you want a simple architecture but other architectures are possible so earlier I show you this diagram right so if you're comfortable for whatever reason doing this this is useful to you maybe you should use this but there are probably more performance proof systems out there they have a different architecture so this is one thing you could do

so take an actual architecture bring everything into lookups don't do the risk the the R1 CS versus something else or general versus lookups just bring everything to the lookup spectrum and that's what you get and maybe that's better but it's a more complex system maybe so so that's the first caveat second caveat types of tables were this useful so I said that um you may remember this slide and you can notice that the second row here is for unstructured tables for lasso what happens to lasso for structur tables so structur tables lass is pretty efficient and in practice it is I don't know how they perform but I expect for many tables of death form lasso uh proving

time could be better so probably uh mic is better for unstructured tables which means plausibly for example variant structure tables are permission lists I was mentioning before so arbitrary sets of sort um this is just a miscellaneous point about how do you think of M mic so think of it as a modular version of CQ that you can instantiate with various multilinear polom commitments so also remember the compiler I showed you is one among a spectrum of others other compilers are possible and they have different caveats different srs's different trade-offs so this is not the only way to do this

wrapping up up so two constructions for super efficient lookups compatible with multivariate proof systems we saw two Concrete Construction and the compiler what's next so one thing you could ask can you put zero knowledge here yes one possibility is probably extending some Zer knowledge techniques for CQ from the from this recent paper pkc uh then we're working on implementation and first first but not last but not first but first ePrint thank [Applause] you thank you Mato any

questions don't be shy y uh wait one second for the mic got to get the sound on the video so these are revenge on M question I guess right uh what sort of pre-processing do you need to do cuz I saw some pre-processing in the table right so there's this um I forget what it looks like exactly but you just pre-compute all possible here's one kdg for all possible points that you care about this is one of the things you do in the pre-processing so F katovich and such for example that's one of the fundamental steps but it depends on the proof system thank you thank you very much mato