ZK10: Lasso: An Engineering Heavy Overview - Michael Zhu & Sam Ragsdale

Transcript

foreign [Music] Ragsdale from a16z talking about the lasso and Engineering heavy overview so I'll hand you straight over and enjoy [Applause] hello I'm Sam Ragsdale an investment engineer with a16z crypto and I'm Michael Zoo a research engineer we will be talking about lasso and jolt so these are two closely related research papers

lasso was written by srinos seti Justin thaler and Riad Wabi it provides a faster lookup argument prover than the existing constructions it's capable of proving lookups into massive tables think on the order of 200 or 2 to the 128 entries and you pay costs roughly proportional to the number of lookups rather than the table size jolt is a closely related work which Builds on top of lasso it was written by erasu Arun srinath seti and Justin thaler provides a new paradigm for building ZK VMS it applies lasso to an entire instruction set think risk five wasm or the evm um it has a faster approver with more accessible devex and easier auditability in terms of an agenda first we're going

to do a little bit of background on what our lookups a lot of people here probably know but we'll set the stage briefly then we will give a high level overview of the lineage of spark surge lasso and jolt then we'll do a brief detour into multilinear extensions Zach did a pretty good one earlier but we'll do that again so that everybody can follow along and finally we'll spend the majority of the time at building a full single instruction jolt VM to show what that developer experience looks like so first background what are lookups um so this is a 4-bit bitwise or operation bitwise operations are ones where you take integers you represent

them as bit vectors and then you operate over each pair of bits sequentially so these are quite simple on Silicon CPUs are designed to do this at the speed of light but unfortunately they represent a lot of complexity uh within snarks and that is because we have to take our integers our field elements represent them as binary field Elements which can be 64 bits or even 256 bits decompose them operate over each of those and then recompose them and this is very expensive so what can we do instead there is an a strategy known as a lookup where we pre-compute all permutations of the operands in this case we have two two-bit operands for a total of four

bits of operands creating a table of size two to the four we can pre-compute that then we can commit to it and we can create simple arguments or symbol operations within a snark where we look up to make sure that an operation lives within this table unfortunately for large VMS with 64-bit operands this table grows to size 2 to the 128 rows which is uh impractical to pre-compute much less to commit to or create evaluation proofs over um so what can we do instead uh in practice what we usually do is a a chunking operation so these are 32-bit operations or 32-bit operands we

represent them as bit vectors and rather than split them out into individual bits we're going to split them into eight four bit chunks this creates eight bit operands and then we only need an 8-bit lookup table or a size 2 to the eight rows so then we can look them up individually of course this still has some overhead but it's much less terrible than splitting it out into single bits or doing the opposite so this brings us to an interesting argument so most lookup arguments have prover costs roughly proportional to the table size we like to analogize this to building a library building all the bookshelves filling it with books and

then getting on a ladder and pulling two books out of that library and then burning it to the ground and this is hugely wasteful as you can imagine so it begs the question if there's a better way so this brings us to the high level ideas behind lasso and jolt in 2020 srinath City released a paper called Spartan which introduced a sparse multilinear polynomial commitment scheme known as spark a sparse multi-linear polynomial commitment scheme is one where you pay costs or you only pay for entries which are non-zero um in the context this applied it in the context of r1cs circuit set which if you've ever done that you'll know that

those matrices have a lot of zeros in them and so it's very wasteful to commit to uh all of those uh indices lasso instead has this commitment scheme called surge which applies a similar idea but rather than to r1cs circuits at we'll apply it to sparse lookups where the sparsity is that we have this whole table and we only use a subset of the rows within that table which lasso is a thin wrapper on top of so this all brings us to lasso the high level idea behind lasso is rather than use it as or use lookups as a a niche tool of VM design we can look up all operands in a VM we can do this

regardless of their complexity so if you're doing the bitwise operations or you're doing the multiply add divide they all have exactly the same complexity you can create these two to the 128 size row tables freely and lasso will do all the heavy lifting for you so this chart here we show two 64-bit operands doing bitwise and and we show that we can prove roughly a million operations or two to the 20 in around 17 seconds um so there's two high-level ideas that we want you to take away from this one is that lasso is very fast and jolt VMS built on top of lasso will be very fast hopefully in the future um so here we we compare in the most

Apples to Apples way we can against Halo 2 both the IPA and kzg back ends we show that around a million instructions we are 10 to 40 times faster the second important takeaway is that lasso is simple and the jolt VMS built on top of lasso are simple they're highly modular and highly comprehensible and we'll try to spend the rest of today proving that to you all right so for some quick math backgrounds so we'll also and jolt heavily leveraged techniques based on multi-linear extension polynomials so for those of you who may be more familiar with their univariate counterparts we're going to give a brief overview and comparison of the two

so let's say we have some data that we'd like to encode as a polynomial so here we have these field elements eight six seven five three zero nine and what we can do is use a univariate LaGrange interpolation so basically these elements get mapped to these points where the x coordinates correspond to their indices within the vector and then we just interpolate a polynomial on top so this Q polynomial we have q of 0 equals eight Q of one equals six and so on and we can also evaluate this polynomial outside of the domain 0 to 6. so at an arbitrary field element say 123.

moving to multi-linear extension polynomials we have a similar situation so the indices of the vector still correspond to the domain of the polynomial but now instead of just a single field element the domain is multivariate so what we're going to do is encode each index as it's as basically a bit Vector of field elements so where before we had Q of 0 equals eight we now have q of zero zero zero equals eight before we had Q of one equals six now we have q of 0 0 1 equals six Etc and once again we can evaluate outside of the the Boolean hypercube at arbitrary field elements

and we can obtain this multi-linear extension polynomial using the multivariate version of LaGrange interpolation pictorially that looks something like this so on the left we still have our univariate extension polynomial on the right we have the domain for the multi-linear extension which is this Boolean hypercube which in this case is just a Boolean Cube instead of the x-axis as the domain so the multi-linear extension polynomial is just going to map points on this Cube to elements in this Vector like so cool so this brings us to the Boolean hypercube which we wish we could stand

up here and tell you that this is the Boolean hypercube and if you stare deep into it you'll find the evaluations you seek but unfortunately this is the reality this is the Boolean hypercube it's just sequential integer indexes represented as bit vectors instead and if you want to represent a value in the range 0 to the 2B minus 1 you have to represent it in B binary bits we do this so that we can use multivariate polynomials instead for use in the sumcheck protocol um so now we're going to do a little detour and talk about in depth what the multi-linear extension of the EQ instruction would look like the EQ instruction is one which takes two integer uh values returns zero if

they're unequal and one if they're equal because we're using multivariate polynomials or multi-linear extensions we are going to have all of the inputs be bits or binary rather than full integers so if we wanted to represent two bits or represent zero one two three we'd need two bits per operand so this is the definition of the multilinear extension of a given operation um the multi-linear extension of an operation says it is equal to that operation over the full domain on which that operation is defined so in our case it's all X and Y operands that are length two bit vectors

I'm going to go ahead and tell you what the multilinear extension of this of this operation is the Q operation and it's here in practice this can be found for for all uh all instructions so we'll expand this for b equals two for two bits and on your own time you can plug in all values of zero one two three as bit vectors and you'll find that the multi-linear extension or EQ twiddle matches the EQ operation but the cool thing about EQ twiddle or the multi-linear extension of EQ is that it's defined on a domain larger than that of the original operation so we can put in all length two vectors of field elements for each operand and we get

another field element which gives us this distance Amplified encoding that we need for some check so that's all the background we need now we can do the fun part so we'll talk a little bit about the developer experience of jolt so lasso is out we release that in mid August that is at a16z lasso on GitHub jolt is what we're still working on jolt allows you to do multiple instructions within the same proofs so the lasso code base will allow you to do a lot of a single instruction that's not particularly useful for building a VM you need to be able to do multiple so jolt will do the glue here it's still in progress It's on this Branch it's highly

unstable but we'll give you a preview of it today we think uh in a month or so when this is out it'll look fairly similar um so if you were to build a jolt VM on your own or build a lasso implementation on your own you'd spend many many late nights with these two papers and the 60 pages of math in them you'd probably eventually binary search down to this figure five which is around page 40 of lasso which describes surges polynomial IOP the good news is that if you build on top of us all you need to learn is this green box and what all those symbols mean and then you can build a full jolt VM

um so there's two rust traits that you'll have to implement in order to implement a jolt VM the first is the jolt instruction trait the first two functions here correspond to this function G the collation function the third corresponds to these T sub I which are the the subtables and each of them for each subtable you have to define a lasso subtable trait and then finally there is this two indices function which corresponds to this indexing down here for each of the subtables we have this lasso subtable trait for which you have to define the materialize function which is simply the evaluation over the Boolean hypercube

um and the second is this evaluate multi-linear extension function which is that EQ twiddle we talked about earlier there's also an example for uh and twiddle here this is exists for all subtables within jolt to give a bit more detail we're going to build a one instruction VM for the 8-Bit EQ instruction this is not particularly useful but it'll give you the mental models you need to build out all jolt VMS also we're doing 8-bit EQ instructions here um just because it's easier to represent it on slides if we did 64-bit operands nobody would be able to follow along but it has exactly the same complexity from a from a developer standpoint

so again we'll take our EQ of integer operands we'll convert it into bit vectors so this is three and three all of those bits individually are equal so we'll return a one now we can do the same for eight and four those bits are not all equal so we'll get a zero um so the high level mental model to come back to here is a lookup table a lookup table is an evaluation over the operation over the entire domain on which it's defined in our case that's all bit vectors of length 16 or two 8-bit operands which means that this lookup table is of size 2 to the 16.

we'll call this parameter n which is the big table size the the issue that we mentioned earlier is that on 64-bit operands this table ends up being size 2 to the 128 which is entirely impractically large so we'll need to do something else what we can do is we can split this 8-bit EQ instruction into a series of two-bit instructions because bitwise operations of course are independent so we can copy in two bits at a time into a two-bit EQ Prime operation so rather than doing EQ over 8-bit integers this does it over two bit integers

and then note here that uh if any of these EQ Prime subtables return zero it'll multiply through the rest and the full big table evaluation will also be zero signifying that it's unequal and now we have a much oh uh one other parameter to Define here is C this is the subtable dimensionality in our case it's four because we use four EQ Prime two bit subtables this creates a much smaller table size our subtable size is now of over four bed operands all permutations of that would be of size 2 to the four which allows us to Define this additional parameter M which is our subtable size

it's of size n to the one over C or in our very specific example 2 to the four so that background gives us everything we need to understand the entirety of the green box I promised we'd explain first n is the big table size this is 2 to the 16 for 16 bits worth of operands then we have this parameter K is the number of unique subtable types you need to define a big table instruction in our case we only need that EQ Prime subtable the two bit subtable which makes k equal one which makes Alpha equal to C uh now the or we can now Define c as

well which is the number of subtables number of EQ Prime subtables we used which if you remember was four uh this allows us to Define m m is the subtable size and it's n to the one over C in our case 2 to the 4. and finally we can Define the collation function G this is how you combine subtables into a big table evaluation and for us we can just do the product of all the subtables if any of those subtables is unequal then the entire bigtable evaluation is also unequal also returns zero all right so returning to those two rust rates that Sam introduced earlier we're going to implement them for the equals instruction

so starting with the jolt instruction trait we have four methods to implement first combine lookups is basically this G polynomial combining these subtable values that we just saw so in the case of equals that's just taking a product over all the subtable values which is this one-liner in Rust nice and easy the G poly degree function Returns the polynomial degree of G which in our case is just taking the product over C variables so this polynomial degree is C the subtables function is just returning the different types of subtables used so

as we saw just now for the equals instruction it always uses that EQ Prime subtable so we just we just return a length one vector containing that but as Sam was alluding to earlier in general instructions may use multiple different types of subtables in which case that would be reflected in the implementation of this function finally we have these the two indices function which is just converting the instruction operands the 8-Bit instruction operands into the four bit indices which we're going to use to index into the subtables so moving on to the lasso subtable trait

we just saw that the equals instruction only uses the equals subtable so for the equal subtable the materialize function uh is just Computing the entries of the table row by row um and it's going to do that by iterating from 0 to M the subtable size and at each step it's going to split that iterator into two two-bit operands and just compute equals over those operands writing down the result and another way to frame it is we're just evaluating the EQ mle over the entire small Boolean hypercube of size m and the evaluate mle method

well we already saw the mle for equals which was this and so this function is just implementing that in Rust and this is going to allow us to evaluate the mle on a vector of arbitrary field elements not necessarily within the Boolean hypercube and that's it so we've implemented the equals instruction and the equals subtable both pretty concise and to sort of put it all together if we wanted to implement an entire jolt VM well first we would have to implement the individual instructions and subtables but once we have that we just use a couple of macros to define the

instruction set as well as the set of subtables needed for those instructions we would set the constants C and M which together would determine the VM word size as well as the size of the subtables and once we have our VM to prove a sequence of instructions all we have to do is pass in a vector of these instruction structs to the prove function so we hope we convinced you in the past 10 to 15 minutes that building a jolt VM is fairly simple and highly comprehensible you'll notice that we didn't talk about arithmetization high degree constraints circuits none of that stuff all that stuff is dealt with for you you have to Define some multi-linear extensions a little bit of indexing and

some table collation stuff but they're all fairly understandable functions um additionally one of the cool properties we get here is once we build out these subtables and the corresponding instructions that use them there's a lot of high-level VMS that can use the same implementations there so you can imagine the the evm version and the wasm version of the jolt VM sharing the same underlying instructions this creates a shared auditing service and many devs can sort of learn the same toolkit rather than sharding attention across very many different very complicated code bases so that's it um if you have any questions feel free to reach out to us directly on x.com I'm at samrags underscore he's at Moodle Zoup

alternatively feel free to reach out to us directly via GitHub this is open source and it will always be open source going forward we have an issues tab with a great range of issues from basic stuff down to arithmetization stuff to assembly level optimizations in addition we're going to eventually have applications built on top of jolt and there's a lot of interesting work that can be done there so if you want to contribute or you want to build on top feel free to reach out or or contribute directly that's it thank you very much so we've got some time for quite if there are any

oh yeah okay quite a few yep um we're at the front here sorry I'm making a tell you what don't worry Emma I'm here there you go hey uh so one question is uh from user yeah developer point of view and developer is it we deployed and deployed in some ckvms and some of them don't support easy pairing free compilers so we cannot do certain one are you supporting pre-compilers uh so today so one jolt is not built yet um we're in the process of building it um I the the evm particularly is difficult

to implement given the 256-bit registers we think we do have a strategy for it we do have a plan to include in jolt the concept of gadgets which rather than just looking up everything you'll be able to sort of route to a specific circuit like an optimized pre-compile circuit so today we don't we have a plan on sort of the very long term roadmap for doing so thank you thank you for the great talk um you gave an example of how to combine the model linear extensions of the subtables for the quality operation do you have an example can you give an

example of a more difficult operation to yeah help grow the intuition of how to combine these subtable mles the the short answer is a lot of them are simple um but there's complicated ones yeah there's so all the bitwise ones are simple for example those basically require one subtable um things like uh shift and less than greater than those get a bit more complicated to give the the point of the jolt paper is to prove that you can do an entire instruction set in this uh in this structure I think less than is a good example this is available on lasso in the lasso repo today you can check it

out but the less than instruction for example you have to decompose and you have both an EQ subtable and a less than subtable and the idea is the EQ subtable continuously tracks whether the previous high order bits had already decided whether it was less than and you multiply that like uh more and more by the the less than table to check if the high order bits have decided or not already whether less than uh is true or not and for like a an example that isn't equals that's um different we have the and Emily here so uh combining the different and Emily's and this generalizes to you all

the bitwise operations you would basically just be taking a weighted sum over the chunks to sort of concatenate them together cool yeah I think I've seen that in the variable thank you um for the example of uh less than or greater than um I wanted to ask if you could expand on that um because my current understanding you would consult the is less than table and then the way that you broke down say a 64-bit arithmetization or 64 bits into a bunch of 8-bit three Tuple 8-bit tables you would then have to check each of

these three 8-bit tables in parallel and if any one of them failed you had an is less than or could you expand on that a little more yeah so let me let me try to do less than live it's a fairly complicated table but you can imagine let's take uh integers that two integers that you're comparing um let's say that the subtables are you have C equals four which means that you have uh uh four subtables of each type um the the mle would first check the subtable of less than for the high order bits um you can imagine that being inconclusive only in the case that all of them are equal like all the high order bits are equal and then you have to go to the next set so you would take uh the the evaluation would be the less

than the less than subtable of the high order bits plus the less than subtable of the next lowest order bits next highest order bits times the EQ subtable of the highest order bits and then sequentially for the remaining few okay that would make sense thank you yeah so my understanding of lasso is that it's you know the look of argument right and then drolt connects that with r1cs and as well as a memory lookup argument to prove that solution of VM so with this API also cover the rncs part and as well as a memory argument uh RSU one of the co-authors on the jolt paper is working on the r1cs bit of jolt

sort of in parallel with uh our repository on GitHub you're right though that we do need a separate r1cs that's custom per jolt yeah um we're in the process of figuring out sort of what that spec looks like generically but it's the r1cs is fairly simple it covers sort of like making sure that register updates happen correctly and that we are decomposing the indexes correctly some of you guys may not have registers and so I'm just trying to understand whether this is just for lasso where it's like like draw in general you can you know also optimize for example like customize you know as operand stack where like registers no registers versus you know different memories per uh per instruction um yeah we think all of that is handled

by the r1cs okay thanks lovely I think that's all we have time for today so um thank you very much Michael and Sam [Applause]