Visualizing Lasso: A fast new lookup argument for SNARKs

Transcript

in this presentation I'll be going over Owasso a new lookup argument authored by srinath seti Justin thaler and Riyad Wabi which enables efficient lookups over huge lookup tables leveraging techniques introduced in Spartan as well as multi-linear some check alright so I'm going to give an overview of lasso in a visual map like format so first to start this is the high level overview of this presentation we're going to start with the motivation or setup of how we arrive at the particular statement that lasso approves and then we'll dig into the details of lasso itself as you can see from this picture waso is a pretty thin wrapper around surge which is a generalization of spark the

sparse polynomial commitment scheme introduced in the Spartan paper and within surge there are roughly three phases there's the commitment phase there's what we've been calling the primary sum check and then there's memory checking and we'll get into what each of those mean later but going back to the motivation here conceptually what we want to prove is this statement looking up indices M of table T gives you a in linear algebra form that looks something like this so you have a lookup table T which in this picture contains these entries 8 6 7 5 309

and you're going to perform some lookups into that table as specified by this binary Matrix M each row of this Matrix corresponds to one lookup into this table the first row of this Matrix has a one in column three so it's performing a lookup into the third entry of t and we can see that the first or rather zeroth entry of the lookup results Vector a contains a five similarly the second row of M has a one at index two so it's looking up the second entry of t and a has the element seven in in its first index in practice T is potentially very big you can think of it being roughly 2 to

the 128 in size and then of course M has to have n columns to match the size of t the number of rows of M corresponds to the number of lookups which we'll be referring to with the variable s throughout and that's also the size of the vector a so assuming T is huge m is going to be much wider than it is tall and with this sort of linear algebra equation in mind the correctness of a can be checked using the sumcheck protocol which can be formulated like this we have the multi-linear extensions of m t and a and we're going to be summing over all the entries of the table so if R is in the Boolean hypercube of

Dimension log s then the left hand side and the right hand side should be equal to one another conceptually if R is all zeros and ones it would correspond to a particular lookup or a particular row of M so for one particular term in the summation M twiddle would be equal to either 0 or 1 depending on if that particular lookup is looking at the corresponding entry of the table T if it is then this m twiddle would be one and that gets multiplied by the appropriate table entry so this is a valid expression that can be proven using the some check protocol but the problem of course is that m is huge m is way too big to commit or to evaluate the mle of efficiently

so we want to reformulate the sum check or this expression on the left hand side into something that's more tractable specifically we're going to reformulate it as a summation over a smaller Boolean hypercube which is depicted here so the high level idea is that we're going to be summing over the lookups instead of the table entries recall that the number of lookups is way smaller than the number of table entries so we're changing the summation from Y and 0 1 to the login to J and 0 1 to the log s and again the left hand side is formulated to be equal to the right hand side when R is in the Boolean hypercube this EQ twiddle term that you see here

is basically a selector so it's 1 if R is equal to the particular lookup index given by J and 0 otherwise so now that we're summing over lookups we're changing t total of Y to this expression now we have the table capital T and we're indexing into it using this function NZ of J so if we're looking at the jth lookup NZ is mapping that to the table index being read by the jth lookup pictorially that looks something like this so previously we had this Matrix M determining our lookup indices where the entry being looked at was specified by whether there's a one in the

corresponding column of a for that row so now we're just basically converting the rows into a single value since the first row has a one in column three we put a 3 in the zeroth entry of NZ so here we're just writing NZ as a vector instead of a function and Row 2 of M has a one in column two so we're putting a 2 in the first index of NZ and so on and so forth conceptually M was this very sparse Matrix before with lots of zeros and we're effectively densifying it into this NZ Vector this is going to allow us to do some check much more efficiently so now we still have the problem that t

might be really big but assuming T has what the lasso paper calls spark only structure which we're not going to formally Define here but basically that just means that t can be decomposed into smaller subtables so with this decomposition we can rewrite this statement as this so we're replacing the big table t with this function G applied to reads into these subtables T1 through TC we're also splitting NZ into quote unquote chunks of indices and Z1 through nzc so what does this decomposition look like in practice so before the decomposition

we had something that looks like this so here we're looking at three and bitwise and operations on various operands so these correspond to these entries of NZ basically the operands are being concatenated together to get the corresponding and Z entry and those NZ entries are being used to index into the big table T where the table entry contains the output of the bitwise and on the corresponding operands so for example this second and operation is operating over all zeros and all ones and the output of that should be all zeros which is what's in fact in the

table T here and recall that at this table in practice would be really big so something like two than 128 entries so we can arrive at the same result with a few extra steps by decomposing which is depicted here the high level observation is that the result of the bitwise and can be computed from smaller bitwise ands basically splitting up the operands so here we have the same bitwise and operations the first one has the operands zero one zero one zero one and zero zero one one zero one but we can break the left and right operand into two bits each so the first two bits of the left

operand are zero one and the first two bits of the right operand are zero zero so that's why we have this right here and in total we're going to be breaking it into three chunks so one two three now each chunk will get its own and Z Vector which again is just concatenating these now smaller operands and the entries of NZ are used to index into these now smaller subtables T1 through TC just like the big table these subtables contain the outputs of bitwise and now over 2-bit operands so the table entry corresponding to the index 0 1 0 0

contains 0 0. and of course the subtables are now going to be much smaller than the big table t and finally once we have the values read from the subtables we can recombine them into the result that would be read from the big table so in this case the combination is basically just concatenating together the result spread from the subtables into a single value and as you can see the values we end up with are the same that were found from the big table t going back to the equation the G function is just the function that does the combining of the subtable lookups at this point we've already introduced what

nzi and TI are going to look like but a few housekeeping items will need to commit to these subtable indices so to do that we'll need them in mle form that's pretty straightforward we're just going to Define these dim sub I polynomials to be equal to the multi-linear extension of those NZ sub I's so that's going to have this domain and range so F Well I guess to f just subbing in DMI for nzi we get this expression one remaining thing is that everything in the summand needs to be a polynomial for some check to work at this point we still have these TI's which are not polynomials they're subtables which can be thought of as

vectors or arrays so we're going to need to change those into polynomials somehow what we're going to do is basically Define these EI polynomials which combine the TI and demise together effectively so it's just the multi-linear extension of all the subtable values read for the relevant subtable lookup indices so that's this expression here and that takes us to the final expression that we want which is this and this is what we're going to end up proving in lasso so now that we're done with the background we can get into lasso itself so just to recap the high level statement that we're looking to prove is

that looking up indices M of table T gives you a well as I was going to do that in four steps so first it's going to send a surge commitment to the verifier and we'll see in a bit what that commitment consists of step two the verifier is going to pick some Randomness R consisting of log S field elements and this of course could be Fiat Shamir step 3 the verifier is going to obtain the value a total of R by making one evaluation query to a twiddle which is committed to outside of lasso for example in jolt and finally The Proven verifier are going to apply the surge protocol to prove that this equation that we arrived at earlier in fact holds and it's

important to caveat here that it's assumed at this point that e i is in fact equal to the subtable values read and we'll be using memory checking techniques to prove that this is in fact the case so you'll see that these dotted lines are connecting things to parts of surge so Step One is the search commitment we're going to need to commit to these polynomials at the outset and this can be done using any multilinear polynomial commitment scheme in particular a dense multi-linear PCS as opposed to a sparse one for example in the lasso implementation as in Spartan it uses hyrax as the PCS but you could Sub in something else yielding different

performance characteristics or other properties so the first set of polynomials is the E sub I polynomials again these are basically encoding the values read from the subtables we're also going to need the Demi polynomials those are the chunked lookup indices as we saw before and finally we'll need these counter polynomials read counts and final counts those are going to be used in memory checking and we'll introduce them then so once the prover has sent over these committed polynomials to the verifier we can move on to the primary sum check so the proven verifier we're going to apply its some check protocol to the summation we saw earlier we're not going to get into the details

of the subtract protocol here but it's basically going to reduce this check into these checks so the EI polynomials evaluated at some random Point RZ chosen by the verifier over the course of some check is equal to these VI values provided by the prover at the end of some check and this is for I from 1 to C in other words for all the Eis the verifier is going to obtain EI of RZ by making one evaluation query to each EI which if you follow the dotted line was committed to back in the commitment phase so at this point there's still no guarantee that like we said EI actually

encodes the subtable values so we need to somehow prove slash verify that the Eis are in fact consistent with the TI's and dimis to do that we're going to apply memory checking this takes us to the third step of surge so just for definitions and setup this is how we're going to depict a memory basically it's a vector or an array of tuples so the memory is indexed by these addresses these red a values and each memory cell is going to contain a memory value and a counter which keeps track of how many times that particular memory cell has been accessed note that in this specific subtable that we've

depicted the addresses are going to equal the values for all the memory cells this table is used for range checks but in general the values are not necessarily equal to the addresses so to take a sequence of lookups and represent them as memory access patterns we're going to think of this as occurring in four phases we'll have an initialization phase a sequence of reads and writes and end up at the final memory state in the initialization phase the memory values are all initialized to the corresponding subtable entries in other words each V is equal to T sub I of a all the counters are set to zero upon

initialization because none of the memory cells have been accessed yet this initialization step can be represented by this set I consisting of tuples each Tuple containing an address value encounter this set I is of size M which is the same as the size of the memory now each lookup into the memory is going to be represented by a paired read and write operation so the address corresponds to this dim Supply polynomial of J the read operation is just going to add this Tuple dim I of j v t to the read set and there's going to be a corresponding element added to the right set which is the same Tuple except incrementing the

counter by one note that the read and write sets are going to be the same size namely s which is the number of lookups at the end of all the lookups or all of the reads and writes we're going to end up at this final memory State note that the addresses and values are the same as upon initialization it's just the counters that have been changed so the final counter value is basically the number of times that memory cell has been accessed so in this picture the zeroth cell has been accessed twice the first cell once the second cell five times Etc and again the set f is going to have size M corresponding to the size of memory now with these init read write and final sets in mind the memory checking and

variant that we want to hold is the following I Union W equals R Union f so init Union write equals read Union final intuitively every memory Tuple though is red must have been written at some point the init tuples you can think of as basically a special case of right and the final tuples are a special case of read in order to efficiently check this invariant we're going to use some fingerprinting techniques which you can think of as hash functions basically it would be really inefficient to check every element of each one of these multi-sets to make sure that they're equal instead we would much rather check the equality of for example two field

elements so in order to get there first we're going to take the read Solomon fingerprint of each Tuple so we have this lowercase H sub gamma mapping the address value counter to a single field element like so but what we really want is to go from the entire multi-set of tuples to a single field element so that's this Capital H hash function so for each Tuple in the set we're going to apply the read Solomon fingerprint function to it and then subtract Tau and then multiply everything together so as you can see that gives a single field element for the multi-set so now this invariant holds if and only if up to some security parameter

this equation holds so the multi-set hash of I times the hash of w equals the hash of R times the hash of f and since each multi-set hash is basically a huge product over things it can be written as a binary tree Circuit of multiplication Gates where the leaves are the read Solomon Fingerprints of each Tuple this allows us to prove the value of each multi-set hash using the grand product argument from thaler 13. the grand product argument is just an optimized version of the gkr protocol for binary trees of multiplication Gates at the end of the grand product argument the verifier is going to need to

evaluate the mle of the leaves at a random point and that particular mle is going to differ based on which set it's for so for the read mle you're going to have one leaf per lookup so the addresses are going to be the dim Sab eye polynomials evaluated at some index k the values are going to be given by E sub I and this is where the read countered polynomial that we introduced earlier is going to be used so this polynomial was committed to in the commitment phase and will be used by the verifier to evaluate this read mle the right mle is identical except the counters are going to be one more than the ones in the read mle

and then for init and final the number of leaves is instead the size of the memory so in this address term here we're basically converting this bit vector k into its corresponding field element representation the value is going to be the subtable Moe evaluated at k and for init the counters are all zero for final we're going to use the final counters polynomial that we committed to in the commitment phase so that concludes memory checking we've shown that the Eis TI's and dim eyes are consistent with each other so that means that this statement that we proved in the primary subtract suffices to show that looking up indices

M of table T in fact gives you the vector a and that's it that's lasso we hope you found this explanation helpful there's a working implementation of lasso on GitHub which you can find Linked In the description alongside the lasso paper and a16z crypto blog posts about lasso and its companion work jolt