zkStudyClub - Lasso/Jolt (Justin Thaler, Georgetown University/a16z)
24 Aug 2023 · 1:38:35
Prover commitments are the bottleneck Lasso targets: the talk presents an indexed lookup argument that commits to fewer, smaller field elements and handles huge structured tables by decomposing each lookup into smaller ones. Jolt then assigns one lookup to each VM step, alongside offline memory checking and R1CS constraints; its three prover-cost components were analytically estimated to be roughly equal. The case remains provisional because Jolt was not fully built, zero knowledge was deferred, and the preferred read-write memory and less-than designs were still unsettled.
Speakers
Topics
Transcript
hello everyone welcome back to another session of ZK Study Club today very excited to be doing a deep dive in some new work called lasso and jolt by uh Justin Baylor and this is Joint work with a few other co-authors which I'm not going to go all the way through them all but you can read them here but Justin is here today and he's going to be presenting this uh for all of us at CK Study Club welcome Justin thanks for having me um yeah so I I want to tell you a little bit about um two new works called lasso and jolt um so there are three and a half hours of of talks from a seminar at a 16z um available on uh on these Works um and so my goal here is to have a
completely self-contained talk uh you know obviously I'm not assuming anyone has watched three and a half hours of videos you know prior to this uh but at the same time to make the talk like complementary to those three and a half hours um and uh yeah this is I sort of view this as uh an opportunity to um kind of update the presentation um in light of a lot of the feedback we've gotten since we released the the papers a couple weeks ago um and also just to dive deeper into the weeds uh since I think the the audience here today is a little bit more technical um I did just throw this presentation together like in the last two hours so um I really welcome questions all along the way I think uh it'll both be kind of
more fun and you know it's not like this is a carefully considered uh presentation anyway uh so please just jump in um about anything at any time um okay so uh let me start by um just telling you you know what what my plan is today and I welcome you know diversions or tangents um so I'll tell you first what is a lookup argument um because lasso is essentially a new lookup argument um then I'll tell you what last one jolt are um then I'll give details of lasso uh details with Jolt um jolt is essentially um like a system that builds on lasso so lasso is like a like a key technical component to jolt uh but it's not it is not the only way to build on lasso so
I'll describe at the end uh sorry how I think you know last I should be viewed as a tool um that exists you know independently of something like Joel's can be used in other ways um and sort of speculate on how else lasso uh might find applications in the future and as we'll see like uh there's there's a lot of of lasso that's really not specific to lasso it's uh the you know know kind of key new techniques or you know insights in lasso actually can be applied to other lookup arguments as well um and I'm actually quite optimistic that um you know the we might see a future where um you know the there are all sorts of lookup arguments being used depending on
certain parameters settings and things like that but all of them are kind of uh building on the same key insights that I'll tell you about today um okay so look up arguments what are they uh so I actually uh want to introduce two variants of lookup arguments um the the first one is the one that people normally study or normally refer to when they say a lookup argument okay and uh so but I'm going to call this an unindexed lookup argument so in in this setting um the prover has kind of already committed to a vector a let's say of length m okay and the lookup arguments lets them prove approve that every entry of a resides somewhere in a predetermined table t okay so that is for every entry of the
committed Vector a there is some index uh bi such that that entry of a equals the bi entry of t okay um so this is actually equivalent to like a Set uh like a subset relationship so you can think of t as a set and the lookup argument lets the prover prove that you know every element of a is in the set um so it's like kind of a like a batched step membership proof um so that that's an unindexed lookup argument if you read any paper before lasso that says look up argument that's probably what the paper means um sort of lasso naturally gives and and jolt is going to need something that I
call an index lookup argument um we're here uh the vector B of indices is pre-committed um and the prover's claim actually refers to those indices right so that is uh an index lookup argument lets the proof approve that for every entry a i of a AI equals the bi entry of the table okay um and in this case I'll call a like the vector I've looked up values and B the vector of indices okay and here um you know just as I said like another way of describing on index lookup arguments is like you know subset uh relationship or you know set membership queries um an index lookup argument is really
the same as like a read-only memory right so like um you know doing uh you know saying that AI equals T of bi is the same as saying that if you read cell bi of the memory specified by the table the result the value stored there is AI okay and at the end of this presentation I'll give like yet other ways to view index lookup arguments um I think thinking of lookup arguments as lookups is very useful I think other ways of viewing them which are completely equivalent are also useful and actually it's good to actually kind of um uh formerly State and clarify all all of the views okay anyone ask any questions
at this point I don't have a question so in the index case do you have like the indices pre-computed so both primary if I don't know them before starting the protocol or it could be the case that the Brewer commits uh the first step let's say of the argument so this sentences yeah great great question so uh the verifier does not know a Orbee they're committed the verifier does know the table um but how the verifier like knows the table um is going to you know some of the tables we want to think about are enormous and um you know uh so big you can never write down every entry in them uh but the verifier still knows it because
um it has a succinct implicit description or something like that um so no one you know um yeah I'll I'll say more about that later um so the important Point here is um the verifier does know the table um somehow uh again I'll say more later but does not know the entries of A and B they are committed by the proverb um now you can either think of you know the commitments to A and B as like part of the problem statement um so this is just like an accounting question like you know uh when I State the commitment costs for the approver in our index lookup arguments I'm going to just assume that um the entries of A and B are already committed just so I don't have to like charge uh the prover to commit to them
um I'm thinking of them as like kind of pre-committed or you know part of the problem statement uh yeah but you could also just think of um the very first step of the lookup argument is the proofer commits to A and B and then then proves that you know what what's listed on this slide did that make sense cool yeah um another funny question whenever you talk about index Loop lookup argument generally what we do in as you say previous papers is that we take a random linear combination of uh the index together with everything what's the advantage besides the round complexity here of uh not going through that approach yeah great I I plan to say more about this later too um but uh let me let me address it now
um I I noticed that as well um because if you do that then you can avoid the extra range checks so okay great so firstly there are no range checks here okay if um if bi is out of range meaning bigger than the table size n um the previous claim is just false and there's just no way for you know soundness guarantees um you know the proofer is going to fail uh in the lookup argument um and then uh yeah so there are generic Transformations which I think you're asking about from on indexed lookup arguments to look up ones right where like um yeah you said you sort of take a random linear combination of
um the indices and the table entries and you know that's like a new table and um you apply to the end of Click of argument to that new table and you know it's uh yeah there's another transformation which we actually you know describe not that I think there's anything new to it at all in an appendix of the lasso eprints where rather than a random linear combination um you just pack deterministically the indices and values together um that obviously requires the field to be big enough that you can sort of pack those two values together without any sort of you know overflow issues um that was what I was referring to in regards to look at the extra range checks okay great uh so even in that case um well whatever and and last one on job we don't use either those Transformations
like um we just sort of directly give an index lookup argument here is why um I think um using those Transformations can be problematic and um this is this is a subject that's worth thinking through carefully uh this is like sort of my initial impression and I'll say more about this later um lasso is really really heavily going to get mileage out of two properties of these lookup tables um one is uh that if the values in the table are small uh the prover is going to be like really fast uh much faster than if the values were like random field elements and so a random linear combination of indices and and values would
uh lose that property and then um the the packing thing um you know wouldn't lose the property would make the table entries bigger but not like it's you know crazy big um but uh we're gonna deal with um really big tables that are structure have a certain kind of structure and uh that's sort of packing together indices and values into the table um for some tables uh might not preserve that structure I think um for some tables it will and for other tables that won't I think to build jolt uh it would not we would have a problem for uh some something some tables we need to deal with so uh my sense right now is it's uh really crucial that we directly give an
index argument without invoking one of these Transformations um but again uh I I think it's a really important topic to Think Through you know not just me for like 15 minutes or something um and I I think a lot of the uh ideas or techniques uh we're we're putting forward um can and will benefit other lookup arguments as well and can actually you know potentially improve jolt if you can address the issues I just raised about the transformations yeah I mean it definitely seems well motivated to me cool other questions okay um great so uh lasso is like a new
family of index lookup arguments high level the prover is about an order magnitude faster than prior Works um and and this is the the bottleneck for the prover in in Prior Works um tends to be the commitment costs um so basically there's always some kind of polynomial commitment scheme that gets used um and uh lasso sort of you know by about an order magnitude reduces the prover time um to deal with the polynomial commitment scheme um and so uh this is the benefits are coming in from two aspects um the prover in lasso is committing to fewer field elements than prior works but also smaller field elements than prior works and actually uh most of the order
magnitude um it's really can be a little bit more than an order of magnitude is coming from the the second thing that the third elements are all small um rather than you know so you maybe get a factor two or three fewer field elements but a factor of you know six or to ten from all of them being small um by small I don't mean that the field is small um although I think this property could help you work over smaller Fields uh potentially in some contexts um what I mean is even if the field is Big all of the committed field elements are in like zero one up to two to the 20 or something and that that um uh speeds up to the commitment schemes depending on which commitment scheme you're using um um I I had a question about this
um so the paper doesn't mention zero knowledge um if you're doing this in zero knowledge would you have to randomize those commitments uh yeah or would that mean that they're no longer small yeah great question um so yeah the paperwork you know we we're putting off the dealing with ZK till later um I completely understand yeah we did we did two in the first uh Halo paper right yeah it should be fine to just basically have a handful of of blinding factors um so um you know in addition to committing to um you know a whole bunch of small field elements the prover also commits to a
pretty small number of random field elements um and I do not think that that should you know uh bottleneck the prover um and uh yeah that sounds plausible the devil is in the detail but yeah yeah and then you know the sort of generic like um uh you know which uh might feel like a bit of a cop-out but is you know you can always compose with a ZK snark at the end as long as the verifier you know fast enough you turn into a circuit or something yeah um other questions um another new property of this lookup argument
um which you know I think is more of a uh just a nice thing I don't think it's completely crucial um is uh for many many lookup tables um in particular everything we need in jolt um I'll tell you shortly what jolt is um no no honest party has to commit to the table and pre-processing so like in in Prior lookup arguments the verifier sort of learns the table really by being handed a commitment to the table um that has to be computed by an honest party all of the tables arising like in jolt um just have this nice structure to it that um the the verifier can sort of process the table on its own with like 50 field operations or something
um 100 200 and you know even for ridiculously big tables um and uh you know finally um lasso sort of naturally supports gigantic tables as long as they have some structure to it um so uh I'll say much more about this soon I mean people are already doing things like this but um you know in general um if the table has and think of n as like 128. um that you know you can the designer uh can choose some setting of a parameter C and basically the there are two there are two kinds of prover costs um there's sort of a cost that depends only on the size of the table but not on the number of lookups and a cost that depends only on the number of lookups not on the size of the table and the bigger C is the
smaller you make like the table only cost but the bigger you make the uh per lookup cost um and so for table size 228 maybe you want to set C to be like six or something and you'll kind of equalize these two costs um you know if you're doing you know say a few million lookups into a table of this size um I yeah um this question might fit better later on when you get into detail um I was wondering how that was different from doing C separate lookups and then um sort of combining the results to get the um the thing that you're looking up in the the larger virtual table yeah um I mean yeah so let me let me handle that
later uh the short version is it's it's not different um up to some details that might be really important um okay so yeah but conceptually it is it is not different okay yeah so it's just concrete optimizations on that yeah uh yeah you could think of it that way um you know there's some of these issues with uh that that you know I um discussed thanks to your earlier question um about um you know we we naturally are invoking an index lookup arguments um or become really important uh when you're uh looking to combine the results of the small table lookups into uh the big table lookup okay okay so that's lasso you know in a
in a slide uh what jolt is it's like a new a new technique for Designing um ZK VMS um so these are snarks that sort of let the prover prove it correctly ran a program um expressed in like the Assembly Language of a specific sort of processor instruction set architecture or something um you know step by step on some witness um high level uh you know we think the prover is just faster than prior approaches to zkvm design uh jolt is not fully built yet so um what we're doing here is uh just sort of a careful analytic and Counting uh basically we're confirming that um the non-cryptographic you know the non-commitment costs for the approvers should not be a bottleneck and then we're very very carefully
counting analytically what is the cryptographic uh the commitment cost for the approver and comparing it to you know prior ZK VMS um and and soon hopefully Joe will be built in we will be not just doing that kind of um accounting and comparison um high level what's going on here is that um each primitive operation for the VM will be executed as just one lookup into a giant table uh that table being the entire evaluation table for that instruction so if the instruction operates on like 264-bit inputs that's a table of size like 228.
um now I think this is like a a new way of um thinking about primitive instruction evaluations but again people are already doing very similar things um as uh Dara's question um sort of got at you know what uh our people already decomposing big tables into small ones and combining the results so the answer is yes we did this in the orchard circuit um for the range checks okay yeah um okay yeah so I will get to um how I think um the precise way we go about things is a little bit different but conceptually totally the same uh you know you're just uh uh executing the instruction by doing you know C lookups into smaller tables and combining the results I mean that
that's it okay um all right so let me give a little more detail about lasso um and then I'll say more about Joel so this probably I don't know 15 minutes about lasso and then then on to onto Joel maybe 20 minutes um okay so a little bit more specifics about the cost of lasso uh before I just said kind of order uh you know number of lookups plus table size to the one over c um so more precisely uh the lasso prover to do um M lookups into a table of size n and these are index lookups uh commits to you know three three C field elements per lookup and then there's this fixed cost of um something like c times n to the one
over C for a lot of tables you actually don't get that c in front of the end of the one over C but it doesn't really matter that much um and uh the all of these field elements are small um say concretely in the set zero up to I don't know uh two to the 20 to the 22 or you know it depends on how many lookups you're doing and um you know what c is and things like that um and this is assuming all of the table elements are small uh just because you just cannot avoid like by definition of a lookup argument the prover does have to commit to the results of the lookups right so if the result of the lookups are huge you know two to the 200 or something that is just now avoiding committing to those
um and the importance of small field elements um in you know uh if you've looked at the paper this is sort of emphasized heavily but uh is um MSM based uh so uh multiscalar multiplication based commitment schemes are just much much faster uh when when committing the small field elements than to than to random ones and in particular um you can basically commit to each of these uh sort of 3C field elements per per lookup uh with just one group operation uh per field element um so that means if it's an additive group like one group Edition um you know so that's that's much faster just to be clear than like a scalar multiplication uh say 400 times faster typically or something like that okay now um C equals one is like a
special case so C equals one I I call it basic lasso we didn't use that terminology in the paper but I'm sort of using it in presentations um where you you don't pay for this this three out in front um of the of the per lookup cost um and uh the the previous commitment cost is only uh M plus N Field elements in this case um and even amongst those n plus n uh many of them are zeros okay so at most 2m sorry most two per lookup are non-zero and in in many cases it's sort of you know determined you know um based on just um how many distinct um array you know like table elements are accessed um uh as few as uh Eminem
might be odd non-zero um so this is important because committing to zeros is like free in a sense like it's it's no it's not no group operation at all okay um so yeah hopefully this makes sense now let me just take a step back um and uh explain where these costs are coming from and like kind of how they compare to um other lookup arguments and naive approaches um so it's it's not so difficult um and kind of like the the natural lookup arguments you would come up with I think with a little bit of thought um what they would naturally wind up having approver do is commit to um a a vector um of of size n that's the table size uh
which at most M non-zeros and so think of these as like um access counts people call them multiplicities um so for each cellular table how many times was it read okay now this is it's actually possible with msms to commit to such a vector like as fast as you could hope uh which is basically um exactly sort of the lasso like cost of their M Small field elements um you think sort of just ignore all the zeros um because they don't like change the value of the MSM um so where you run into a problem is that like at the end of you know the lookup argument um the verifier is going to have to evaluate uh the committed you know polynomial that we're interpreting this length n Vector that's very sparse as like the coefficients of a polynomial or something the verify is going to have to
evaluate that committed polynomial at a point and the evaluation proof um is going to wind up paying costs that grow with n the tables the length of this Vector um that sort of the evaluation proofs don't seem to benefit as far as we know uh from sparsity of the committed Vector um and so that's that's the problem like everyone's grappling with um and to be clear like there are some polynomial commitment schemes where the cryptographic work of the prover and Computing the evaluation proof is sub linear and n but it's still square root n um so if the table size 2 is 28 it's still like just doesn't work okay so you know the line of work uh there's a there's a great line of work starting with caulk and you know uh most recently culminating in CQ
[Music] um that deals with this issue um by pushing all of the processing of uh that depends on N to pre-processing right so you pay like you know it's something like n log n group you know scale them applications or whatever in pre-processing I think it's also specific to kzg Commitment so you need an SRS of size n um and the nice thing after that is uh you know after that pre-processing your costs are completely independent of n so you don't even get this like end of the one over C term um but uh I think with them uh with CQ it's like you know seven random field elements committed per lookup whereas lasso you know you do have this end of the one over C term but it's like
um you know if C is six or something it's like you know roughly 18 or something small field elements per lookup which is much faster than seven random field elements um and so what what lasso does for these big tables is just deal with this issue of you know the sparse Vector of length n um uh and in just a completely different way um so what lasso has the prover do for these you know giant decomposable tables is the the approver will like never commit to like a length end Vector at all instead what the proverb will commit to is um the much shorter Vector that sort of just lists like which entries of the giant length n Vector are non-zero okay and then when the um that's the commitment to um you know this
um uh like the these polynomials of access counts um is just like you know apply a dense polynomial commitment scheme you know like a normal one um to uh like the vector that just lists the non the non-zero access counts um and then when the verifier says hey I need to evaluate that committed polynomial at a point the prover just proves that it correctly ran an algorithm that sort of takes the evaluation point and takes like the non-zeros that were already committed and computes the evaluation given those two inputs okay so the evaluation proof is just like I prove I ran this evaluation algorithm correctly on this you know um particular representation of the source
polynomial that's lasso okay um any questions cool okay um and then in terms of verifier costs so um you wind up with um logarithmically many um and actually it turns out just to be logging on the number of lookups and like even for these big tables and uh you know that have huge size n uh logarithmically many um field operations and if you're applying fiatry me or hash evaluations coming from um the some check protocol um plus one evaluation of uh like you know the the committed polynomials so
you can you know the approver commits to several polynomials and you can batch all the evaluation proofs into into one um so that's like one evaluation proof for my polynomial size like you know n to the one over c um yeah and uh you know I think these costs are are low enough that um basically you know uh you should ignore them I mean some people might disagree with this but um uh they should be low enough that uh you can do something like snark composition uh this is a little bit dependent on like exactly what polynomial criminal scheme you want to use you know I think ideally you would um use one that uh has like a you know the fastest proofer you can come up with and the the evaluation proofs might be
somewhat bigger uh and you just want the evaluation proofs to be sort of small enough that um it doesn't become a bottleneck to do the composition um and yeah happy to talk more about this uh but that's just my general view is uh you know kind of a natural way to design snarks is get the proof as fast as possible and the verifier costs like just low enough that you can bash the process down further through through composition okay yeah I was just I was just thinking it might be useful for some applications if um you could prove things about the the number of accesses to um an element so so for example if that's just zero or one then you're proving that the input Vector is a
permutation of a subset of the table and that that could be a directly useful thing to prove yeah that's interesting um I mean the lookup argument um under the hood does use uh you know a permutation check anyway yeah um you know the the main stuff the prover commits to um okay in the in the sequels one case where there's no you know decomposing victim on the small table the prover is just committing to access counts um there is this nuisance that um like let's say a cell is accessed um you know five times so the prover is
going to commit to the numbers um like zero one two three four and you know it should be possible to like only commit to four and we like don't know how to do that yet um and there's some follow-up work I'm going to mention which is uh I believe going online tomorrow uh by others um that does achieve exactly that um by you know building on the sort of the key ideas I'm about to describe to you um using logarithmic derivatives but it's sort of naturally an unindex lookup argument and I don't think these transformations to index lookup arguments would play nicely enough to build jolt out of it but if you if you could um and I could usually be wrong about that I'd love to be wrong um I'd say you should um
potentially just swap out the C equals one lasso with the logarithmic derivatives one uh but keep using the um you know how we do the decompositions of the big tables into small tables more engineering to be done yeah yes um yeah uh cool thanks for the the questions uh any anything else now okay yeah feel free and continue no questions in the chat I'll read them if they come up okay thanks okay so let me say a little bit more about how these decompositions are being done although um I think I'm not going to go into great detail so maybe I've
already said this let me just yeah I think I basically already said this so yeah uh you know we're um we actually give two variants of lasso for big tables okay one um applies to more General class of tables um but is more expensive in the sense that um about a third of the committed field elements are random instead of small and we don't actually know like any example of a of a table where you need the generality of that one so let's just ignore it for from now on um so yeah the kind of structure used by the more efficient variants is what we call decomposability this basically means conceptually you know what we've already discussed uh one look up into the big table can be answered by doing say C lookups into one or more tables of
size you know n to the one over C where n is the big table size and we'll see examples of this where uh yeah I will cover examples of decompositions in a bit um where this this decomposition thing is very natural um I have a question here like all the proof size depend on the amount of different tables you're using so amount of tables they are using for the compose the big one so our proof size not really um verifier time the verifier is going to have to evaluate um the multi-linear extension polynomial of each little table at a random point and so um you know more small tables increases that time but it's it's just field work
um it's I don't think it should be a bottleneck compared to others you know the cryptographic operations the verifier is ultimately going to have to do right thanks um yeah the proof size grows a little bit because well it depends how much you're like batching things the the prover commits to you know certain polynomials for each small table um but uh you know there are ways to commit to you know many polynomials by kind of gluing them together into one and you know you can batch the evaluation proofs together and things like that so yeah um there are there are these costs that grow with the number of subtables but I don't think it's it's bad uh for anyone really I don't think it really matters that much
um other questions okay um in jolt I think there's a total of something like um 45 different subtables roughly if that's if that's helpful um okay so yeah yeah I'm just I'm just thinking about um how expensive the the verify a circuit is if you need to do recursive yeah well okay so you don't have to recurse on that part of the verifier um right the parts of the verifier we would run a recursor on are like uh if you don't like you know the log size uh some check proofs you know that's field work and hashes um but you know fry is you know like cubicle
um and so I think the big thing is like if you want to use like a fast proof or polynomial commitment schemer the evaluation proofs are bigger than you want to post on chain or something I think that's really what you'd want to recurse on um and you everything else I think is cheap enough you probably wouldn't mind uh not recursing on it um yeah okay yeah so I guess the the way we um take the results of the small table lookups and turn them into the results of the big table lookup is is with the subject protocol so we use the Centric protocol like in many different places in both lasso and jolt um and that basically makes the combining like free
for the prover there's just like no more commitment costs um and uh this is sort of where you know if you have like uh if the results of the small table lookup is like an index and a an actual value sort of packed together uh you want you want up into issues like so if the way you're gonna you know like glue the you know small table indices into a big table index matches the way you want to glue the values together uh you kind of have no problem and that actually is the case for like some tables in jolt but for others it's not right like the way you want to glue indices together these are like the indices are like a limb decomposition of the big table index so you want to take a weighted sum of the like you know limbs to get the the big
thing um but we often need to glue you know small table um like values together not through weighted sums and that's that's why that's like my main sticking point I think right now um in terms of trying to use on indexed lookup arguments that are not naturally indexed um to give you know something that we you know uh that would let us build jolt from it cool okay um let's see uh okay so let's let me now just say like what are the key ideas in in lasso um that and uh you know in this lasso is arguably like completely implicit already in um a
result in Spartan um so uh mainly we're just making observations that clarify benefits of um these techniques that I guess you know exactly this extent of the benefits weren't previously clear okay so like all known lookup arguments and you know a lot of snarks that are not look up arguments um use something called a grand product argument and this is just a way to multiply together a bunch of committed values um and uh if you um use a snark that like under the hood is using univariate polynomials um as far as I know like the the only Grand product arguments um uh firstly that what they kind of two issues what one is uh the main one is the prover minds of
committing to partial products um and there are some other issues that I I think um you can attribute like like pluck up as a has a cost that uh grows with the maximum of the number of lookups in the table size and uh I think you can kind of attribute where that maximum is coming from to to using kind of univari polynomials under the hood I'm not 100 sure that uh so that's another um nuisance um and uh this is not necessary um so there are look up our uh sorry Grand product arguments based on the subject protocol that just don't have any more commitment costs for the approver so um I gave one in 2013. it was just uh this interactive proof called the gkr protocol sort of
optimized for a circuit that's just like a binary tree of multiplication Gates um now the the proof size there is like log squared um and the in the number of things you're multiplying uh which again is like better than fry which a lot of people are using today already uh but if that is too much for you um study and Lee um gave a nice way to sort of reduce that verifier cost from log Square down to something very close to log with like a small increase in in improver commitment costs um yeah so uh very high level and you know I'm not planning going into more detail than this but you can um basically take some existing lookup arguments and just swap out the grand
product argument um to use you know either this um gkr based one or the you know um the variant from um seti and Lee um and like maybe the key observation is like the only reason the prover in the current lookup arguments is committing the random field elements is because these partial products um involve Randomness um yeah so you just get rid of it yeah did I get the right link for the paper t13 uh let me sorry uh let me just check time optimal interactive fifths per second that's it that's it yeah okay um exactly um and you know I mean if you if you you
know don't care about like the very precise optimizations you know you're happy with like a heavier hammer and extra log factors or something uh you could have invoked prior Works uh that still have this qualitative aspect that uh there's no commitments happening in the grand product argument um yeah but the 2013 paper sort of made sure that the provers uh you know field work is itself linear in the number of things being multiplied um okay yeah and I mentioned like there's there's a nice upcoming work um I think I think it's I'm mentioning it because I think it should be online tomorrow I didn't check with the authors if it was okay so I hope it's okay um uh you know uh kind of applying
similar sorts of insights to the logarithmic derivatives um and to get I think an actually a better unindexed lookup argument than like basic lasso uh but on this uh I don't currently see how to slot it into like something like jolt that needs to look up argument to be awesome if if you know if I'm wrong about that um okay so yeah I guess as a higher level takeaway uh you know these techniques have been around right so like you know um it's possible the community is just not quite fully internalized uh like the power of the soundtrack protocol which is underlying all of this um to minimize commitment costs for the approver um yeah okay so uh if you want to see details of how basic lasso Works um I
did cover that in my second a16z talk um so I won't focus on that here I also don't really think it's that important um uh and then um I I'm gonna say more at the end of this presentation about how I you know suggest thinking about lasso as a hammer so I'm not sort of done you know explaining you know lasso in some in some ways um yeah just as a heads up I'll I'll say more about this I'm not totally done with okay any questions before jolt uh can you just go back to that last slide so I can um notice that's opinion okay thanks okay
um okay yeah so let's talk about Joel so uh yeah jolt is a yeah sorry a quick question um Can the the t13 can you like do it with uh a multiplication gate with fan in like d instead of two and then maybe get the log squared in a bigger base than two yeah yeah great question so um you can you can um there's a trade-off there where I don't believe would it uh I should think about that more hmm if you have fewer layers
So within each layer so I I'll probably think offline how to optimize that it's a great question um you know the gkr protocol goes layer by layer through a circuit okay so if you um uh make the circuit uh you know um shorter uh but the fan in more uh there are fewer layers but the cost within each layer goes up um and the cost will actually grow up within each layer um the field elements will go up linearly with the degree with the fan in um the rounds actually should not really increase per layer um so I think what's happening my here's my guess my guess is the number of field
elements in the proof will actually go above log squared but the rounds will go way down um and for composition um those rounds turn into hashes which is the bottleneck so that um could be a Ben a good way to do things potentially if you're looking into composition um if you just care about proof size um I'm not sure if it'll help I guess as it won't just because it'll make the number of field elements uh potentially go up but yeah there again the number of layers going down that's actually good for proof size but you know within each layer the number of field elements is going up that's bad for proof size I have to have to think about it more yeah I was mainly thinking of the number of hashes in recursive composition yeah that would uh it would definitely help
with that um and then another thing you could help you could help with is within each layer rather than working over the Boolean hypercube you know zero one to the log you know um layer size um you could work over like zero one two three four and that would have the number of rounds it would increase the number field elements sent in each round but that's just more field Ops for the verify or not hashes um so that's another um toggle you could turn um if you're looking to minimize you know hashes for composition reasons yeah okay thanks yeah thanks for the question other questions cool okay yeah so um just a quick
um sort of recap of ZK VMS I guess um so the setting here is you say the proverb is claiming to have run a computer program for some number of steps and deliberately I'm choosing and the same as you know the same letter that I use to denote number of lookups before um because there's going to be one lookup per step of the computation here um and uh so let for zkvm you know the program should be expressed in the Assembly Language of a virtual machine um popular virtual machines today for ZK VMS uh you know there's a Cairo virtual machine there's risk five uh there's the ethereum virtual machine um and there there are others as well maiden and so forth um and the way people deal with these today is they'll basically turn the
computer program into uh uh really the virtual machine I guess into into a circuit like kind of a universal circuit um or constraint system and basically what the what the constraint system will do is make sure that you know the prover sort of at each step of the computation like kind of correctly figures out like what instruction needs to be executed at this step uh what what primitive instruction and then that the prover correctly executes that instruction so that's sort of what's happening over and over again there's some kind of Master Loop that's you know sort of getting unrolled for T steps or m-steps where n is some predetermined bound uh and it's just repeatedly like figure out what instruction to execute and what data execute the instruction okay
um and what what uh jolt does is it uses lasso to handle the second thing execute the instruction with just like one lookup into the entire evaluation table of that instruction um and as I said before you know that means if there's like two 64-bit inputs to that instruction this table is size 2 to 128 um and things get a little bit annoying when you have you know 50 different primitive instructions and then so they each have their own evaluation table and you have to deal with those things uh but here here's like jolt in a in a picture I'll try to summarize uh this is just you know I copy pasted from the paper I try to summarize how I'm thinking about things so um I'd say there are three aspects to Z an easy KVM really um I sort of mentioned two of them
already uh which is like you know at each step of the computer program uh you sort of have to figure out which instructions should be executed next on which inputs um you have to correctly execute that instruction and then the last thing is you know um that first part or and also like uh where you sort of store the output those involve reads and writes um to either like random access memory and or to like the registers of the CPU so like Risk five I think it's 32 or 64 registers Cairo I think there are three registers um so there's really three components here okay there's um uh uh there's the lookup argument we're gonna use
um to make sure that each instruction is executed correctly okay there's um what I call offline memory checking and offline memory checking argument to make sure that like all reads and rights are done correctly right so anytime the machine like does a read into uh the you know CPUs random access memory or you know like write something to a register or whatever you sort of think there would be two separate memories like the 64 registers or whatever and uh you know uh whatever however big random access memory is uh we need um a memory checking argument to make sure the provers you know returning the right value for every read you know the the value most recently written to that register or memory cell okay and then is that is that argument
not also implementable using lookups great question um so lookups are for read-only memories um and and here we need read write and um actually to um make the argument secure um you have to do things a little differently a little more extensively with read write um so there is a a section like an appendix in the jolt paper where I try to like brain dump it probably didn't do a great job um now in the con let me just I'll briefly tell you the offline memory checking procedure that um for read write memory that we're planning on using in in jolt but there are there are
others so um what what lasso does um or basically so is uh it's sort of any any read uh to the read-only memory um gets paired with a account so the prover also returns account which if the prover is honest it's just an access count how many times was the cell accessed and um anytime there's uh you know a read on the proof of return you know says hey here's the value you know um that lives in the cell you asked to read and here's the counts you know that live you know that was associated with that cell the verifier will immediately write back to the same cell the the return value and the same count but incremented by one which ensures that like you know if the approver was honest
like the count continues to be just an access count um now uh the yeah and then what you know you wind up showing like hey if the prover like you know you sort of have a read set and a right set um you know the read set is like all of the re the values and counts returned by the reads the right side is the values and counts written and you showed the permutations of each other if and only if the proverb is honest okay so you just do a permutation check um so it by only incrementing the count by one like that's a really nice simple update to the count uh that does not prevent a cheating prover from doing something like um answering a read at time you know I with some value that will be written to the same cell sometime in the future
okay so it can kind of reorder and an adversary can successfully like reorder the values um you know uh return a value that will only be written in the future and then in the future return of value that was written in the past um so to prevent that uh you have to change the count update procedure and what we do we take something out of um a paper called spice that um replaces plus one with a certain Max operation so the there's a kind of a global Max uh that like the circuit is is sort of tracking at all times and and the the accounts for each you know after each read operation gets updated to the max of the return counts and that Global count plus
one and that prevents this sort of like going back in time attack uh this might have been without this paper um proving the correct execution of concurrent Services yeah um so we use um yeah that spice like count update procedure that's what we plan to use and how we did all our calculations and uh but to make this Max operation like less painful uh what do we do we use lasso um inside it um there are other um approaches um and it's not 100 clear to me that actually um the spice thing like is the best but you know it's certainly you know among them um one nice thing about both you know basic lasso which is
really in spark and about spice um is there's no like grouping or resorting of the operations um you know it's just like the prover is sort of on the Fly you know committing to these values and counts and it doesn't have to like sort by memory cell and some of the other techniques do have these sort of uh the provery like groups by memory cell and stuff you know um go ahead sorry yeah before you were talking about the different ways in which you can look at the lookup protocol and you told us about the indexed way and the anestheticate way and now you're introducing these remember the checking and so um the first question is how do you see how do you do you see memory checking with
respect to the index at the perspective that you gave us earlier I think there is a difference yeah so um memory checking for a read-only memory is completely equivalent to indexed lookup arguments um but if it's a read write memory it's uh you know that's a harder problem so that's sort of like indexed lookups into a table that you can you know overwrite cells of okay and and so okay another quick question in Spartan that was already the offline memory checking idea but that was already taking this linear combination of the value synthesis for the read and write tapes so you're not doing that anymore okay so so Spartan what's happening in in Spartan's memory
checking stuff uh it sort of applies it specifically to get a sparse polynomial commitment scheme okay and um so so two things so I it is just doing like um okay so so sparse polynomial evaluation this algorithm I mentioned earlier where the evaluation proof or the prover proves it correctly ran a certain algorithm um to evaluate the committed polynomial at the requested Point all that algorithm does is it is it literally like initializes these small tables of size n of the one over C and then for each like non-zero coefficient of the sparse polynomial that's been committed it does one lookup into each of the small tables and multiplies the results together to get the result of
the bigtable lookup um and those tables um are filled with random field elements uh no matter what right like that's just the tables themselves in this context are filled with you know these these Big Field elements so um all Spartan is doing is it's applying um lasso um is literally like lasso is what Spartan or spark that's supposed to spark spark costs as far as polynomial commitment scheme um uh but um spark is a very specific application to a very specific like algorithm and and you know lookup table um and so all we're doing in lasso is sort of pointing out that the situation is more General and it applies Beyond
sparse polynomial commitment schemes and then when you do apply it Beyond Sports polynomial commitment schemes the small tables can have very very small entries instead of like random field elements um was that helpful that answer the question um yes but I want to know more so I'll let you talk I'll leave you today I think okay okay you got it yeah I have a question um so that there's a a thing that is intermediate and expressiveness between um um I look up in a read-only memory and uh sort of memory checking which is looking up uh in a dynamically witness table
um and it so if you use a hello like look up argument then um it just naturally supports that there are some details but um that this it doesn't become significantly more complicated um does that also apply to lasso um just just consider basic lasso for this yeah so um okay I might need to know a little bit more about what I guess what you mean by you know dynamically witness table but it um in so in spark the sports polynomial come in scheme the relevant tables are not known ahead of time um they are dynamically determined they're determined by the point at which the verifier wants to evaluate the
committed sparse polynomial uh but once you determine that evaluation point it's like the tables are determined and so they've read only like from that point so they're sort of dynamic read only yeah I think that is I think that is the same thing okay okay so yes you you know you could use Dynamic tables uh yes yeah that's the as the basic tables uh and and then obviously not directly for the generalized lasso uh yeah yeah but they you the big table is constructed from the dynamic table exactly exactly that's right interesting cool uh yeah so okay so I guess back to
the picture yeah so you know the the VM sort of at each step figures out like what instruction needs to be executed and what inputs executes the instruction and you know saves the results somewhere right and uh you know somewhere in there is like you know getting the input saving the results um there there might be like reads reads from memory so um yeah we use like the lasso lookup argument to make sure each instruction gets correct uh executed correctly once the inputs to the instructions are determined we use offline memory checking to make sure like any reads and rights to registers or memory cells are dealt with appropriately and then the r1cs is sort of capturing I mean anything else but um what those things tend to be is
um how you determine um like what inputs uh and what instruction is getting applied to those inputs at each step so like for example um when we um sort of save things into memory or register um we to the extent possible want it packed all into one field element because the cost of the memory checking procedure like grow with the number of field elements we're sort of reading um but uh then to easily sort of figure out like what instruction to execute on which inputs um we then need to kind of unpack um like an OP code into its individual bits or you know things like that um and so the r1cs is capturing
constraints like you know make sure the unpacking is done correctly and also it captures like within the lookup arguments we need to make sure like when we decompose an index into the bigtable into limbs we need to make sure like those limbs are really a decomposition of the big there's no range checks but of the big table index so the r1cs is just capturing all those constraints okay now in terms of the prover costs um sort of uh surprisingly to me uh at this stage um all three are about equal um so uh that does me I think that's a little bit bad because it means if you did want to continue to improve things further like you have to sort of move all three
um I'm surprised by this uh I think um uh what's really going on or it's just a little more annoying to do like offline memory checking is a little more expensive than I would like like sort of unpacking of field elements um into constituent pieces that we need is like more expensive than I would like um and so I you know I would have thought that this you know uh you know the step this this look up into a giant table would be the bottleneck and I guess we've Tinder made it efficient enough that it's it's not it's about you know uh equal to the other two costs um so uh so so does that depend on the kind of program um because some programs might do more
lookups than others yeah it does so there's this interesting thing where um I think there are you know 45 50 primitive instructions in Risk five um now um some of them do no lookups um most of them do uh okay so some of them you only have to do a lookup into like a you know table of size um like two to the 65. um most of them it's size 228 and then um one a couple uh are even kind of 2x more expensive than that um and uh we really only have to pay um for the instructions that are
actually executed essentially there there's some details there um but uh yeah um so so some programs will be cheaper than others uh just based on what instructions get executed and then another another caveat um sort of in the reverse Direction uh uh here I'm saying like some things are sort of um more efficient than what we kind of accounted for in the paper is uh some instructions uh we sort of have to turn into multiple invocations of another instruction but this is just like to do division we have the proof or provide like the quotient and remainder kind of situation yeah um was it that that answered your question roughly yes yeah yeah so it will be interesting to
to compare the the um instruction costs uh in this approach with the the native instruction costs yeah yeah and there's this funny thing where like each like real lookup into like a subtable is sort of cost the same um it doesn't really matter like um what is in the subtable because all the subtables are small and stuff like that uh so that we're the only place where you get like you know sort of program dependence stuff is just because different instructions involve different number of subtable lookups anywhere from zero to twelve actually is the biggest 12 if we're setting C to be six which um yeah anyway we plan to set C to B6 for 64-bit uh data types
um yeah okay I was gonna ask what the um sort of useful range of C was okay that's interesting yeah so I think for 32-bit data types probably want to set C to be about three and that's just because your tables will a size like 2 to 64 and you divide that by three and now it's like pretty close to the 20 and like MSM is a size 2 to 20 no problem and if you square the table size you double see roughly so because it's you know table size to the one over C so yeah kind of cool okay other questions um I have another one um and it's going to be really stupid so if I have we worry so much about the in
the tables the size of the elements in our in our lookup but at the end of the day we're going to have to do a sound check of the same side as the look as the tables they were having to look into right at least a number of elements you're doing some check all these elements could be randomized because you know some check so like at least from the second round I will have all random elements what am I missing here yeah the the key point and this is exactly the power of some check is uh the prover is not cryptographically committing to those elements it's just field work oh right right yeah
um now I will say um if you do really want to work over like a small field uh you know an extension fit of a small base field uh you sort of raise an important issue um which is if you're naive about if you sort of take the linear time subject approvers today um from the second round onward all arithmetic is happening over the extension field if your random elements are chosen from the extension field um so I have some work in progress that can improve over that um and so when you want to work over these small Fields um the field work can become a bottleneck um when you work over big fields I I think they're you know you it just won't be on
just um yeah the you know the small field the stuff over small Fields um you know it's like uh you know risk zeros working over baby bear now so like for each committed field element um you can actually pack like eight committed field elements into one you know they're using a you know hashing based stuff right so the small field is saving you cryptographic costs right because rather than you know um if you use a 251-bit field um you know you can only you know if your hash function takes two 256 bit inputs you can only hash like you know two field elements at a time but if when you pack elements like that then you need to do at least an inner product in order to show that the the packing has been done correctly I don't think the packing is being done
um algebraically it's just uh your hash well it is if you like recurse so yeah if you without recursion you just do the packing and the verifier itself does the unpacking and it doesn't have to be algebraic in nature if you recurse then you have to express the verifier as a uh circuit and now the verifier does have to be algebraic um so that anyway maybe I shouldn't have gone into this because the discussion gets complicated uh but the yeah uh maybe I'll just take a step back and say um uh yeah the sum check you're right you're right that the sun check prover needs to compute over random field elements you know from round two onward but it's only field work um I think you do want to pay attention to that field work if the field is really small um if not it really should
not be a bottleneck um and even in that case I think there's uh or I know that there's some interesting stuff you can do um that hopefully continues to ensure that the field work is not a bottleneck for the proverb okay thank you you mentioned the baby bird feel that I just look looked up it's just under 31 bits yeah yeah exactly so yeah up to issues with uh you know um do you have to pack and unpack in an algebraic way uh you can pack like eight field elements into 256 bits cool okay so uh yeah so I sort of I've told you what jolt is now
um and you know just some brief context you know we sort of we're pitching jolt I mean I we think it is a realization of Barry White Hat's kind of look up Singularity Vision uh because most of like the serious work happening um in the is it happening in the lookup argument even though the approver costs actually are sort of split evenly between sort of three components of the system um and the hope is that you know this is sort of a uh you know you wanna let's say you um what you know it turns the the auditing procedure into the following like uh make sure that your lookup argument is correct your offline memory checking procedure is correct um and uh
yeah that's uh I guess that's that's a a big piece of it and then once all that's correct um uh if you want to like change your primitive instruction set um for your VM um all the developer has to do is like specify like the subtables and how to combine the results of the subtable lookups um thereafter on so this feels uh I think like a qualitatively different way of building zkvms um it it feels like it cuts out like the need to like hand design a optimized circuit like any time you change the Primitive instruction set and things like that um you know as I've already you know acknowledged it is pretty similar to things people are already doing um so I think what the the key
differences here um are coming from the the lookup arguments um so firstly it's just much lower commitment costs for the prover so you can just kind of use it more freely um yeah less expense um it's naturally indexed so I sort of you know highlighted this uh struggle to take on the next lookup arguments and you can turn them into index but does it preserve the properties we're really exploiting in in lasso and joltitz I uh not clear to me that that it does I think it might not I think it doesn't actually um and then like since our collation technique turning the small table results into bigtable results um uses some check it sort of comes at no additional cost for the approver um and it's not clear to me that like non-subject-based techniques can can
achieve that and you sort of put all these together and I think that's what's unlocking our ability to sort of do you know um all of the risk five instructions as you know just look UPS into these decomposable tables um again I think it's uh I hope it's a good thing that we're doing things closely related to what people are already doing and maybe just pushing them a little further and with optimizations um you know kind of the the closer it is to the way people are doing things I hope the easier it is to you know for people to start using it um if um if people wind up thinking it's it's worthwhile uh yeah and uh so let me see how much okay so I have like 15 minutes or so
I've been thinking about how I've used so this kind of uh multiple tables combining the results in existing circuits um and so how complicated can the combining operation be yeah um I'd say the the main amount uh annoying ones are like uh less than and you know bit shifts are surprisingly annoying um but um you know complicated is like complicated in terms of like writing down the summations um in terms of performance for the
prover um you know it's uh it's all just a handful of additions and multiplications handful meaning you know like uh SQL six probably uh a total of like you know five editions and five multiplications is the worse you're gonna get something like that uh is that right the shifts actually this year do you mean for uh all of the combination functions that are used in the end risks there yeah then uh your honors five yeah so I think the the yeah uh that's the short version is uh think of it as each is like um something like uh some in order of like five editions and five multiplications um in the yeah
yeah because I I'm thinking of the most complicated um ways I've used this and probably that one would be since I'm here where you're you're adding um you're doing um elliptic curve operations to to combine the um table lookup so I'm not I'm not sure whether something's that complicated is useful to consider as an instance of the same approach or so are you are you thinking about like what if you did the combining without some check but with some other technique is is that what you're thinking of or are you thinking uh yeah I'm asking what the limitations are of doing it using some check
um on the complexity of combining functions oh I see um okay so the some check you know it's it's all field work for the prover and the verifier of course there's you know per round there's going to be hashes after you feature near it um and the there's going to be one round um for each subtable lookup I think and so you know that's the hashes are for the verifier are just determined by the number of subtable lookups um and then the number of field elements sent per round is just determined by
the degree of the combining function um right okay so it's it's like a custom constraint um effectively right water pump yes but but without any commitment costs yeah right okay and then the degree of that determines the cost okay yes that makes a lot of sense yeah um and all of our combining functions though are um naturally sort of uh multilinear in the subtable results so um the degree in each variable is just well maybe one or is it one it might just be might be two uh anyway
so there the the degree it seems that like you know just degree one or two suffices um for the combining functions oh interesting so in each variable uh yeah so do you count the total degree in the same way as you count them for a punk um custom constraint so that's that's the maximum degree of any tan yeah so um yeah some check it's the number of field elements sent in round I is the degree of the you know combining function in variable I or you know subtable result I um oh right okay thanks yeah cool um and Alex your question uh how much time do I have
left um so I think well technically 13 minutes left um but I mean if you want to go a little bit longer that's fine but I just want to be respectful of your time most especially uh but it's up to you I we can go a little bit longer you know say 10-15 minutes if people are interested and you are interested but it's up to you okay so sounds good I think I can get through um everything I I want to say anyway and um about 15 minutes we'll I guess we'll see um just trying to think reorder it um yeah okay so I'll follow your lead don't worry about it don't worry about the time whenever you're you're I can key you when it's 11 30 in case you have other stuff but yeah I would say just yeah I I have no no uh hard stops so um
okay yeah so I thought we would my plan for the rest is let's see some example decompositions um and then I was just gonna talk about um lasso uh kind of as a tool independent of jolt and how else it might be used um okay so yeah we'll start with bitwise end which is the example we sort of give it's the simplest cleanest example you know like in the intros to the papers um so maybe you've seen it but um yeah it's worth covering so uh yeah the fact that the evaluation table bitwise end is decomposable uh is essentially equivalent to the fact that to compute the bitwise end of like two 64-bit inputs you can break each of those inputs up into say chunks of eight bits each you can bit wise end you know each
each chunk and just like concatenate the results okay so that means um you know you you you just like do a Lindy con and 8-bit limit decomposition of of each uh each of the two 64-bit inputs um you know you each of them turns into a look up into the smaller table that only takes two 8-bit instead of two 64-bit inputs and then concatenating the results is just like a weighted sum okay so I have a question um so if you were doing this just using um an existing lookup argument um then the decomposition would be um we've come for free with the bitwise
under table lookup because um your your x i and y I would be constrained to eight bits in the table um is that also the case for lasso yeah so you're asking like do you have to do like a range check a separate range check yeah yeah you do not need to do any range checks here okay cool um yeah and then um if you so the verifier at the end of um lasso has to evaluate the multi-linear extension of each subtable there's only one subtable here it's like the sort of you know two eight the eight bit n subtable um at a random point and so here is that multi-linear extension so it's just you
know it takes 16 variables as input and it computes this weighted sum of the variables each variable has you know total degree two sorry each determine the sun is total group two so that's why um no one has to commit to even the subtable um the verifier can just you know evaluate um the MultiLing extension of the subtable uh in like 25 field operations or whatever um do you get a cost benefit from the fact that the subtables are all the same in this case yeah for the verifier yeah so if there were more subtables each one of those would have like a different extension polynomial that the verifier would have to evaluate at the same random Point um but different polynomial and I don't think I don't think there's
any but it's just one evaluation for each one for each one yeah okay and it's all field work yeah um okay so that that is and okay so here's risk five Edition um I sort of copied this out of a Twitter thread like right before the talk so I hope this isn't too bad so uh basically yeah if you um uh yeah you take 264-bit data types X and Y you want to add them together um if the result is bigger than you know 2 to 64 minus one I guess there's like an overflow bit that I believe risk five prescribes you to just ignore like throw away the Overflow bit so essentially you know what we have to do is identify that overflow bit okay so what we're going to do is uh what jolt does is it will do
the addition in the field okay so now we just have one field element which might be bigger than you know 2 to 64 minus one um in which case we have a problem we have to sort of you know subtract off uh that overflow bit times 2 to 64. so we need to use lookups to figure out what is the Overflow bid so all this amounts to is doing a limb decomposition of that field element um so you do sort of it's you know net yeah yeah is it approver commits to the lens um we now we do do it over like a range check in this the lookup is like basically a range check on the limbs um we add a constraint to the ancillary r1cs that make sure it really is a limb decomposition of you know X Plus y um and then there's just one more lookup
uh where we take the highest order limb and do a look up to just sort of pull out the the high order bit um and actually another way you could have done it is you could have had the proofer sort of commit to that high order bit separately um and then uh you know uh have to hire a limb just you know range check it to be you know like uh you might not impossible you can even avoid it but um anyway there are other ways you could you could figure out that high order bit that actually might be a little bit more efficient but it's not going to be a big big difference okay questions about this one okay and then again this lookup table ultimately all the lookups are just into like um they're just for range checks and those are also like mle structure
tables multi-inter extension structures so no one's committing to the the subtables okay final one on less than um so this is actually like the most expensive um table for us uh in jolt um and here uh yeah again you just like you know uh take the two inputs X and Y if you want to know is X less than y um and again you just sort of do a limb decomposition of them so that is you you chunk each into like eight eight limbs say and now now I've written this expression here um for uh what the what the answer is um so yeah uh you know if like if you take the high order chunk and you know uh you just compare the high order chunks and and the comparison goes a certain
way you know what the answer is right like if I think if you want to know if x is less than y and in in fact the high order chunk of X is greater than the higher chunk of Y you already know the answer is zero or something so like you don't even have to continue on to the remaining chunks um but if the higher chunks are are the same [Music] you know okay I think if it okay so if the higher the higher response like might make a decision right if like if the higher chunk is strictly greater than y or strictly less than y you already know what the answer is uh you have a problem if they're the same then you have to move on to the next chunk and figure out do they make a decision in the ordering you know if they're the
same you have to move on to the next chunk and that's what this sum here is capturing right so we go like you know each term of the chunk of the sum is capturing like which chunk are we looking at now you know let's see if if that chunk made a decision um you know uh by evaluating less than like just on that chunk um and uh you know if uh if not we move on to the other ones and only pay attention to the other ones if like all the higher order chunks were equal you know that's conceptually I know there's too much to follow online but maybe you can look at the expression offline uh but that's what's going on is you're just uh solving less than sort of by breaking into chunks and looking at the chunks from the highest order to the
lowest order ones um there's a different way of doing it which is to subtract the inputs and then compare the results to zero that's a that's a great Point um you have to be very careful of overflow it's more complicated than I've said it there yeah no that yeah that is a great place I think you you end up doing two range checks so so live snark um had a comparison function that worked this way um yeah you now that you bring it up I remember this um I'll I'll Think through um it's possible that because the number of times in this this output is quite
large isn't it because it's so I am I reading it correctly the there's a parano round um the uh to the left of the two CI minus one and to the right of the Eek um there is so I think you can um uh you know so so there are eight terms of the sum um and although the the ith term involves um a product of High minus right so you've got a quadratic yeah quadratic yeah but you don't actually pay the quadratic because there's so much overlap between the terms uh like you can compute the sum with like an arithmetic Circuit of size only about uh 10 rather than
8 square root over 2 just because just because these products are you know there's only one term that's different in each as you advance I oh I see yeah so this might actually be reasonably cheap already so but um yeah the I mean the thing is all of the cost is really in the subtable lookups and uh evaluating this expression is just field work for the prover um so it almost doesn't matter um for anyway that that's an engineering optimization yeah yeah and it's great my guess is since the what matters is the number of subtable lookups my my initial guess is there will be range checks coming into you know the um subtraction approach that will wind up equalizing
the cost um but I definitely should think that through it might is it is a uh I don't think it's like bottlenecks the proof of performance anyway but it is a nuisance to have an instruction here that um does a look up into um you know like two subtables two different subtables per chunk instead of just one I think it's like the only instruction that does that so that's just like an engineering nuisance and if we can avoid that that's nice yeah so if I ever remember correctly you reduce um a comparison on K bits to basically two range checks on K bets um
that makes sense and I think that I think you're going to give the exact same cost so I'll take that out while the the tables yeah so you can do because um your range fact tables um just have one input and they're not binary tables so I think it does end up cheaper oh that is that's a good point if this is a much smaller table Yeah okay um all right yeah maybe that will um get rid of this annoying factor of two um actually so thank you um I'll follow up and let you know that would be uh be great um okay so those were the examples I
guess I wanted to cover I uh you know so this involves like this a quality subtable and it's less than subtable and like two 8-bit inputs and I just wrote out like you know what their MultiLing extensions are and again it it's like uh not many field operations to evaluate them at a random point so no one has to commit to those subtables in uh yeah okay so the last thing I wanted to discuss was like lasso uh like how um I think you should think of it as a tool um which is at least if you want to avoid anybody committing to the subtables um which you know it's not the end of the world too have someone commit to them um since they're all small but um it's I think it's nice to not have to have that
um then um I think intuitively what these techniques support is doing Simple operations on the bit representations of field elements but without having the prover like commit to individual bits but rather mainly committing to uh like these limb decompositions um the reason this is uh you know sort of simple functions on the bits um that are are sort of captured by um lasso is because these multi-linear extension polynomials of these subtables are quickly evaluatable like roughly when um they're simple functions of the bits of the indices um yeah so uh one thing to clarify here
is uh lookups you know sort of in my view are like all about economies of scale and it probably there are some exceptions with like C C I'll actually say a little bit more about that in a second but um if you're just doing like three lookups into some table uh you know at least with lasso there's like some cost that depends on the table size that you're not gonna amortize effectively over that few lookups so you really want to be doing a lot of lookups before it makes any sense uh with something like CQ you have this nice property where uh you sort of deal with the table once in pre-processing and then you can sort of do you know like three lookups to the table in this snark and three lookups to the table and the other and another snark and you you know you're never
having to pay that you know cost that depending on the table size again after the pre-processing phase so that is maybe the main exception um but yeah so um I think in general if you are repeatedly doing simple operations on the bit representation to field elements that's kind of when you wouldn't want to use lasso and it's it is more General than that if you're willing to have an honest party commit to some some things in uh in pre-processing um okay so um yeah I just uh I you know I I promise at the start that I would discuss a couple other ways to view lookup arguments um and I you know my favorite way of viewing them now is as snarks for
um I call data parallel computation it's probably easiest to just say repeated function evaluation uh but here if you think of the lookup table as jolt does as just storing the entire evaluation table of some function then what what a lookup argument does is let the prover like commit to a bunch of claims inputs and claimed outputs of the function and prove that the outputs are correct okay so literally it's just like a rephrasing of a lookup argument is just a snark for repeated function evaluation okay um and then you know in settings where um you really want like you know A2 to depend on F of A1 or something you'd have like an ancillary r1cs to like
confirm that A2 indeed is like derived from r1cs in the right way from A1 in the right way or whatever um and so from this perspective lookup arguments are just like really efficient snarks for computations with repeated structure um and uh you know with lasso because there's a cost that grows like table size to the one over c um you want you wind up in the situation that people don't normally think about uh I think um in most people's heads when they think about snarks for repeated function evaluation so normally you think well if your function's on n Bits then maybe you're going to evaluate it like you know uh poly in many times or something and like that's like many repeated evaluations of of the function here uh
but for that you know end of the one over C cost and lasso to you know be not ridiculous you really need number of evaluations here to be like kind of weekly exponential in the size of the input to f right um okay so that you know um two to the size of that input that's that's n and so you need that to the one over C where C is like six or three or would have you um to be a reasonable cost for the prover to pay um and so yeah that means like you know um you really need the the number of evaluations of f to be you know uh at least like two to the input size to the one over C you know to the 1 6 or something
um however with like virtual machine execution that's exactly the setting you're in because these primitive instructions only operate on like 64-bit inputs or 128-bit inputs but you run the machine for a billion steps a trillion steps you know um and and it really is reasonable to you basically should think of the input side to f as like logarithmic in like the real input size and um the number of valuations of f as you know exponential in that which is now only polynomial and like the real input size um yeah so you know uh you could just call look up arguments like very effective snarks for repeated uh function evaluation um and so I think lasso will be useful whenever you have repeated function evaluation and I'm
just going to mention like I think uh this slide is horrible I threw it together like right before the talk um I think there are other ways to identify repeated structure in computations um other than going through like virtual machine abstractions um just as As One Direction which I'm I'm working on um with uh my intern from the summer you know and another student uh sriram um there's there's actually an approach from the hardware Community called bit slicing which is trying to take advantage of the fact that uh real computers have like you know 64-bit data types and sort of uh you know operating on all 64 bits is like the same cost as operating on one bit um so what this means is like you know
for a function um that sort of naturally captured by a Boolean circuit and I think like AES and Shaw or uh should qualify and that's sort of the point of the project is to kind of make sure this um what you could do is to evaluate on many different inputs like you would for you know several education paths if that's the hash function you used um you would take the first bit of each of those inputs and you know say they're 64 of them and pack them into one field element the second bit of each of those six of each of those say 64 inputs and pack it into another field element and then you take the the Boolean circuit for one copy of F and replace each like two-bit end with like you know an end on 264-bit inputs
and now each output gate rather than Computing one bit of one output is computing like one bit of all 64 outputs and then of course you'd have to do like the sort of unpacking and repacking to uh get your your bits all together um so this is just another way to sort of get you know leverage data parallelism um and you know that lasso was like very well tailored for um the advantage is that the cryptographic engineers are already used to doing this um it's because it is already the the best way to optimize cryptographic algorithms on conventional architectures yeah yeah um so uh and and you know to me
um like the I I continue to be like surprised uh um others seem to not be by the extent to which the parallels uh go between like kind of how people design real hardware and how we can design snarks and like you can't push them too far uh like you know a lookup argument is not literally just doing a read in the memory literally but um yeah this uh this seems like uh another example um where you know for slightly different reasons uh designing a snark might make sense to use the same exact technique that you know um people are using today and uh outside of snarks um okay so I think I'll stop here uh but yeah in general
um I think these lookup arguments are just a a toll for any computations with repeated structure it does not have to be uh virtual machine abstraction so jolt I hope is just sort of the first application of these uh these things yeah thanks for uh all your uh uh attention to this talk yeah thanks for having me yeah thanks thanks very much Justin um I have a quick maybe question and then maybe others have questions but I think like one way to think about this is like you're taking advantage of kind of the structured nature of these bitwise computations specifically to construct a table and the question that I I'm actually this is producious question he asked uh he asked me earlier about when we were discussing this work is if you have to go to bitwise representation anyway to do the table
lookup is there like is there actual Savings in real world terms so I guess that that would maybe be a question for you to like how would you answer that so the question is um we're comparing savings relative to just having an approver commit to the bit decompositions that's right yes it's a big savings uh it's at least an order of magnitude and it's because if you're using MSN based commitments anyway and I think there are Savings in other contexts too but pippenger's algorithm conceptually lets you commit to let's say a 22-bit field element meaning Big Field but the element is between 0 and 2 to 22 or something with one group operation which is the same exact cost uh that it would take to commit to like a single bit
um does that make sense so like yeah yeah um so it really makes sense to try to pack to the extent possible at least like 20 to 30 bits into each field element um and when you do that you commit to fewer field elements like at the same cost per field element and then there are ancillary costs depending on like your setting or snark that also will go down um because you're committing to fewer field elements so short version is yeah I see like a like a 20 to 30 x speed up from uh doing it this way cool uh does anyone else have any questions I know a couple people dropped it at the half hour mark but anyone else uh anyone else in the group have questions for
Justin um yeah I wanted to understand a bit better this idea of rain checks and these uh packing ideas so the idea is that at the end of the day you're in the big commitment to all of your values and then you check the range on those and then you group them together in order to um perform algebraic operations over larger like um sequences of bits I don't understand how this is this packing and rain checks ideas work together so what I I think the way to think of it is we um we never decompose the elements to be range checked uh into into smaller data types than Limbs and the
the relevant limbs are between like 16 bits and that's however big you're willing to do uh like kind of an NSM like you go up to maybe 30 odd bits um and yeah so to confirm that like some some field element is between like zero and 228 uh maybe you decompose it into either I say 32-bit limbs if you're willing to do size 2 to 32 msms um so what is that that's for them or something so four limbs um and you range check each each limb uh make sure it's between 0 and 2 to 32 with an unindexed lookup argument into the table that just stores you know the field element zero up to 232-1 um and that's your that's your range
check um and you're just you're never gonna decompose the limbs any further into like their bits or anything like that um at the end of the day all I do with that with the limps maybe I'm doing like um if I'm doing operations on each of the lanes at the end of the day then the lookup itself will be checking the range wouldn't it why am I doing a rain check so um you in in general it just gets a little confusing but like in most applications of lasso we don't need to do any range checks okay like the lookup itself intrinsically uh checks internet yeah does a Range check right there there are some contexts where we literally just want to do a range check and there's no other relevant lookups or
something and um and then we will just do an actual range check with lasso um but um yeah I mean you know they're they're different applications of lookup arguments sometimes you do want to do operations on the limbs um other times um you know you don't really care about the limbs I mean like with with less than right like um uh we we break things into limbs just so that the size of the subtables is like small uh we don't actually care about the limbs we only care about the result of the less than operation right and like that's just like one bit so um you know when the less than operation like we do um again you know that dire might have
us doing it a better way but right now we're doing like a look up into you know um like a an equality table and a less than table on on each you know limb um and uh we collate the results to get our you know our final result of the whole less than and we just don't do anything with the limbs ever um is that is that helpful like so we're we we're only going into limbs to keep the subtables small yeah yeah it makes more sense you know thank you I I understand better yeah thanks for the question awesome well hey Justin thank you for being super generous with your time this is an awesome talk we this is I think actually one of the best the most most
participation I've seen in one of these in a while so thank you very much for uh for joining us uh today uh really hoping to have you back at some point you know I know you've got some other follow-up work uh and you mentioned some interesting future directions which we didn't get to touch on but especially interested to see as you guys Implement I think you mentioned there's some work to implement jolt is that right uh ongoing yeah we're hoping maybe I shouldn't say this out loud we're hoping in just like a couple months um to have some working version of jolt um which which should be good for benchmarking so um we'll see we'll see how things actually go yeah really really would be really cool to see you know kind of the concrete you know improvements that this could bring and but in General on a
theory from a theoretical level seems like a lot of really really great uh improvements here so thank you very much for sharing that with all of us in this group and thank you everybody for uh attending this week's Study Club thanks for having me again thanks for the great questions