Lasso + Jolt: An engineering overview

Transcript

So next up, we've got Michael Zhu and Sam Ragsdale from A16Z talking about the Lasso an engineering heavy overview. So I'll hand you straight over and enjoy. Thank you. HELLO. I'M SAM RAGSDALE, AN INVESTMENT engineer with A16Z crypto. And I'm Michael Zhu, a research engineer. We will be talking about Lasso and Jolt. So these are two closely related research papers. Lasso was written by Srinath Setty, Justin Thaler, and Riyadh Wahby. 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 what are 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 Arasu Arun, Srinath Setty, and Justin Thaler. Provides a new paradigm for building ZK VMs. It applies Lasso to an entire instruction set. Think RISC-V, WASM, or the EVM. It has a faster prover with more accessible dev x and easier auditability.

In terms of an agenda, first we're going to do a little bit of background on what are 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? So this is a four-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 within SNARKs. And that's 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 precompute 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 precompute that, then we can commit to it, and we can create simple arguments or simple 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 two to the 128 rows, which is impractical to precompute, much less to commit to or create evaluation proofs over. So what can we do instead? In practice, what we usually do is 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 eight-bit lookup table or size two 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 Setty released a paper called Spartan, which introduced a sparse multilinear polynomial commitment scheme known as Spark. A sparse multilinear polynomial commitment scheme is one where you pay costs or you only pay for entries which are non-zero. In the context this applied 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 all of those indices.

Lasso instead has this commitment scheme called Surge, which applies a similar idea, but rather than to R1CS circuit set, 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 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. 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. So here we we compare in the most apples-to-apples way we can against Halo 2, both the IPA and KZG backends. 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 background, so Lasso and Jolt heavily leverage techniques based on multilinear 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 8675309. And what we can do is use 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 8, Q of 1 equals 6, 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 multilinear 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 what we're going to do is encode each index as it as basically a bit vector of field elements. So where before we had Q of 0 equals 8, we now have Q of 000 equals 8. Before we had Q of 1 equals 6, now we have Q of 001 equals 6, etc. And once again, we can evaluate outside of the the Boolean hypercube at arbitrary field elements. And we can obtain this multilinear 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 multilinear 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 multilinear 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 sum check protocol. So now we're going to do a little detour and talk about in-depth what the multilinear extension of the EQ instruction would look like.

Um, the EQ instruction is one which takes two integer uh values, returns zero if they're unequal, and one if they're equal. Um, because we're using multivariate polynomials or multilinear extensions, um, we are going to have all of the inputs be uh bits or or binary, um, rather than full integers. So, if we wanted to represent two bits or represent uh 0 1 2 3, we'd need two bits per operand. So, this is the definition of the multilinear uh extension of a given operation.

Um, the multilinear 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 uh 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 uh of this operation is, the EQ operation, and it's here. Um, 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 0 1 2 3 as bit vectors, and you'll find that the multilinear extension or EQ twiddle

matches the EQ operation. But, the cool thing about EQ twiddle or the multilinear extension of EQ is that it's defined on a domain larger than that of the original operation. So, we can put in all uh 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 sum check. Um, so that's all the background we need. Now, we can do the fun part. Um, so, we'll talk a little bit about the developer experience of Jolt. So, Lasso is out. We released that um in mid uh August. That is um at a16z/lasso on GitHub.

Um, Jolt is what we're still working on. Jolt allows you to do uh 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. Um, 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 uh describes Surge's polynomial IOP. Um, the good news is that if you build on top of us, all you need to learn is this green box and what all of those symbols mean, and then you can build a full Jolt VM. Um, so, there's two Rust traits that uh you'll have to implement in order to implement a Jolt VM. The first is the Jolt instruction trait. Um, the first two functions here correspond to this uh function G, the collation function. The third corresponds to these T sub I, which are the sub tables.

Um, and each of them for for each sub table, you have to define a Lasso sub table trait. And then finally, there is this two indices function, which corresponds to this indexing down here. For each of the sub tables, we have this Lasso sub table trait, um, 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 multilinear 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 sub tables within Jolt.

Um, 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. Uh 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. Um, so again, we'll take our EQ um 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. Um, 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 um two to the 16. We'll call this parameter N, which is the big table size.

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

And then, note here that uh if any of these EQ prime sub tables return zero, um, 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 sub table dimensionality. In our case, it's four because we use four EQ prime 2-bit sub tables. Uh this creates a much smaller table size. Our sub table size is now of over 4-bit operands. All permutations of that would be of size two to the four, which allows us to define this additional parameter M, which is our sub table size. It's of size N to the one over C,

or in our very specific example, two to the four. Um, 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. Um, this is two to the 16 for 16 bits worth of operands. Um, then we have this parameter K. Uh K is the number of unique sub table types you need to define a big table instruction. In our case, we only need that EQ prime sub table, the 2-bit sub table, which makes K equal one, which makes alpha equal to C.

Uh now the or or we can now define C as well, which is the number of sub tables, the number of EQ prime sub tables we used, which, if you remember, was four. Uh this allows us to define M. M is the sub table size, and it's N to the one over C, in our case, two to the four. And finally, we can define the collation function G. This is how you combine sub tables into a big table evaluation. And for us, we can just do the product of all of the sub tables. If any of those sub tables is unequal, then the entire big table evaluation is also unequal, also returns zero.

All right. So, returning to those two Rust traits 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 the sub table values that we just saw. Uh so, in the case of equals, that's just taking a product over all the sub table 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 uh polynomial degree is C.

The sub tables function is just returning the uh different types of sub tables used. Uh so, as we saw just now, uh for the equals instruction, it only uses that EQ prime sub table. So, we just we just return a length one vector containing that. Uh but, as Sam was alluding to earlier, in general, instructions may use uh multiple different types of sub tables, in which case that would be reflected in the implementation of this function. Finally, we have these uh 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 sub tables. So, moving on to the Lasso sub table trait, uh we just saw that the equals instruction only uses uh the equals sub table. So, for the equals sub table, 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 zero to M the subtable size.

Uh 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 uh 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. Um and this is going to allow us to evaluate the MLE uh on a vector of arbitrary field elements, not necessarily within the Boolean hypercube.

And that's it. So we've implemented the equals instruction uh and the equals subtable, both pretty concise. And to sort of put it all together, uh if we wanted to implement an entire Jolt VM, well, first we would have to implement the individual instructions and subtables. Uh but once we have that, we just uh 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 uh 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. Uh so we hope we convinced you in the past 10 to 15 minutes that building a Jolt VM um is fairly simple and highly comprehensible. Um 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. Um you have to define some multilinear extensions, a little bit of indexing, and some table collation stuff, but they're all uh fairly understandable uh 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 uh underlying instructions. This creates a shared auditing service and uh many devs can sort of learn the same toolkit rather than sharding attention across very many different very complicated codebases. 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_, he's at moodlezoop. Um alternatively, feel free to reach out to us directly um via

GitHub. This is open source and it will always be open source going forward. Um we have an issues tab with a great range of issues from basic stuff down to arithmetization stuff um to assembly level optimizations. Um 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 questions now if there are any.

Oh, yeah. Okay, quite a few. Yeah. Um one at the front here. Sorry, I'm making a Tell you what, don't worry, Emma. I'm here. Here you go. Uh hi. Uh so one question is uh from um user Yeah, developer point of view and developer is it we deploy deployed in some uh CK VMs and some of them don't support easy pairing precompilers. So we cannot do certain Are you supporting precompilers?

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. Um we we think we do have a strategy for it. We do have a plan to include in Jolt um the concept of gadgets, which rather than just looking up everything, you'll be able to uh sort of route to a specific circuit like an optimized precompiler 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 uh multilinear extensions of the subtables for the equality operation. Do you have an example Can you give an example of a more difficult uh operation to yeah, help grow the intuition of how to combine these subtable MLEs? The the the short answer is a lot of them are simple, um but there's complicated ones.

Yeah, there's 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. Um to give uh the the point of the Jolt paper is to prove that you can do an entire instruction set in this uh in this structure. Um I think less than's a good example. This is available on Lasso in the Lasso repo today. You can check it out. Um but the less than instruction, for example, you have to decompose and you have both an EQ subtable and a less than subtable.

Um and the idea is the EQ subtable continuously tracks whether the previous high-order bits had already decided whether it was less than. Um and you multiply that like uh more and more by the the less than table to check if the higher-order bits have decided or not already whether less than uh is is true or not. And for like uh an an example that isn't equals that's um different, we have the and MLE here. So uh combining the different and MLEs and this generalizes to all of the bitwise operations. Um 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 repo. 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 uh in my current understanding, you would consult the is less than table and then the way that you broke down say a 64-bit arithmetiza- uh 64 bits into a bunch of eight-bit uh three-tuple eight-bit tables, you would then have to check each of these three eight-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 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. Um 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 Jolt connects that with R1CS and as well as uh a memory look up argument to prove that's using a VM. So would this API also cover the R1CS part and as well as a memory argument? Uh R C U, one of the co-authors on the Jolt paper is working on the R1CS bit uh of of Jolt sort of in parallel with uh our our repository on GitHub.

You're right though that we do need a separate R1CS that's custom per Jolt VM. 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 VMs may not have registers and so I'm just trying to understand whether this is just for Lasso or is like like Jolt in general you can, you know, also optimize. For example, I customize I have operand stack or like registers, no registers versus, you know, different memories per per per instruction.

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.