ZK12: Lessons from integrating LogUp-GKR in the Miden VM - Bobbin Threadbare & Philippe Laferrière

Transcript

This is we for the past 8 9 months on and off we've been working on integrating Logu GKR. Uh and yeah, we learned a lot of things that were not clear to us from the start. So the goal of this presentation is to try and convey this knowledge. Um So it was a little bit tricky to make it fit in 1 hour not knowing very much of the background that people would have on the different topics. So how we tried to design the presentation is assume almost nothing and try to get to the end. Uh so we'll start with more of the basics and so that's why like if you have any questions anything feel free to ask. Um and if we don't finish honestly it doesn't matter. Uh well we can just like

go straight to the conclusions towards the end. Uh we'll try and make it uh yeah like so that people like the goal is to convey these lessons and uh I wrote this book on Hack and D. Uh the link is here it's going to be uh probably like recorded so I don't know it's probably hard to type in but uh if you just like look at my @plaffair the like everything that's in the in presentation or almost everything is in this book. So yeah, so this presentation is more as a okay let's let's just talk it out and any small detail it's all in there. Uh and yeah, feel free to reach out to either of of the mining team and we'll be happy to help out. So that's uh so Bob will start with uh you know,

talking about the multi-set tracks. Yeah, and um basically uh most of the work here was done actually by Phil and Al over there. Myself participated very little bit. Um and the overall structure that we're going to go through this presentation will also have like some code to show you guys of how we've implemented it. There is like a uh two versions of uh kind of like a dummy VMs that we've put together that show like when to use log up G car when not to use it and like in which settings it's applicable. So, there will be like a coding portion to it.

Although, you will not have to do any coding. We'll just show you the code and you know, walk you through it. Um All right. So, um let's get started. Um a lot of what I will cover in this initial section is probably looking at the audience, I think probably super familiar to everyone. So, like not sure and you'll see a lot of new stuff and we'll get further down, but I'll cover it anyway for the recording and maybe for a few people who are not familiar with it. Uh but the first thing we want to start with is you know, the multi-set checks and like why do use them and like you know, we use them in my VM. They're used in you know, other projects as well very extensively. I would say multi-set checks is probably uh one of the biggest if not if not the biggest like

innovations in the stark protocol since the original stark because they allow you to do things that you were not able to do previously with like a you know, basic stark protocol. And this is basically allows you to express non-local constraints. Without multi-set checks constraints in starks are fairly local. They're usually involving adjacent rows or you know, maybe a small set of adjacent rows or sometimes you can jump, but you in very regular offsets. With multi-set checks it kind of allows you to um kind of enforce constraints that like take some things from like this part of the trace against this part of the trace and you know, give you a lot of flexibility. A lot of things that we do um in VM specifically in kind of stark

based VMs would not be possible or would not be nearly as efficient without multi-set checks. So, in my VM we use multi-set checks um for a few things. There is like a few things listed here. Uh we use it for for more than that, but you know, we have like a stark based machine. Uh my VM is a stark machine. So, like you want to have stark which is you know has very uh kind of like you can put a lot of elements on it so practically unlimited depth this is what we use multi-set checks for we can kind of emulate it using a lookup table um uh you want to do range checks this is like a you know almost a table stakes for any kind of useful VM where you need to check and make sure

like some values are within a given range 16-bit 16-bit range checks is usually what we kind of care about and then we can build other things from these and again you want to do a ton of those um and then we have some more esoteric instructions in my VM that allow you to do like say Merkle path verification as a single instruction so like from the main processor standpoint there is one instruction and then the multi-set check you have a separate we call them chiplets or sometimes they're called co-processors where you can offload the verification of a Merkle path to a separate co-processor and it just does it from the kind of standpoint of the main VM it's just a single instruction but there is a whole other machine running that allows you to do it separately All right

So we'll start with multi-set checks and then we'll build up to lookup and then we'll from lookup we'll go to lookup ZK-R so I'll do the easy part which is just the multi-set checks and then Phil will handle the more complicated stuff uh so multi-set checks again probably super familiar to everyone here but we have um you know we want to make sure two sets of values or I mean our case usually field elements are equivalent and in in this case we say what matters is that if the the two sets contain the same set of elements it doesn't matter in which order so if if they contain the same set of elements they're considered to be equal uh if one set is missing one element they're obviously not equal order doesn't matter repetitions do matter so

like if you have you know two threes in one case and only one three in the other case that that those are not equal sets And the core idea here is that we will represent kind of this set of as polynomial. So we basically, you know, as roots you take the values that you want to have in a multiset check, you set it as a root of polynomial. Um and then you want to check if the polynomials are equal and the way we do it is evaluated random points. So you basically take them at random point. Um you compare if the evaluations of the two polynomials at random point are equal and that's how you figure it out.

Um The in Miden VM, like this is a little bit of an eye chart and not going to go into this, but this is like the layout of the trace of Miden VM. And you can see like there are different parts to it. Like there is, for example, the main processor is here, there is a decoder here. Um and then there is like a bunch of chiplets and a range checker on the right side. Uh and there's like a some system trace here. Uh and you may want to have some things that you put in into like, let's say, one of the sets and they can come from different parts of the trace. For example, uh an example of this could be, although this is not a correct example for this, but let's say you want to do a range check.

So you'll do a bunch of range checks. Like you say, "Okay, I'm going to range check a bunch of values here." And then let's say you want to have the other part. And again, range check is probably not the best example, but you can uh you can say, "Well, we'll the left hand side of the multiset check is going to be these green boxes. They can be contributed from any part of the trace and the right hand side is going to be these blue boxes and then they also can be contributed from any from another part of the trace. And we want to make sure these sets are equal." Um so kind of this is a more general form of describing it because every row can contribute multiple values to a multiset check, so to say. Um there is a constraint on how many rows

per value um or how many values per row you can contribute. And this constraint is usually run into the degree bound. So like the more things you want to at least in this setting when we use multiplications, you run into the constraint where um you know, you can put you can add a lot of like you can add some values to them to the set that you want to multi set check against. But let's say if you put eight, your your degree of your constraint may need to be eight unless you introduce additional columns to kind of like reduce the degrees and things like that.

But here you do this multiplications to add more values from the same row. And you know, if you have K elements in the row that you want to add, your degree could go up to eight or up to K unless you reduce this. One of the benefits of Logup GKR is that this actually is no longer the case. You can add more things per row and you don't have the same degree constraint. And then the way we express it in StarkEx is by using this running product column. So let's say we have these two sets and A and B and this is a simplified view where like the column is entirely represent you know, one column has the A values and the other column has the B

values. And what we want to do is we want to have this running product column where you know, whenever we want to whenever we have something on the left hand side of the multi set check, it gets multiplied into the column and whenever whenever we want to have something in the B side of the multi set check, we divide it out of the over that column. And so you know, this column progresses you know, it starts at one because there is nothing that we compare against and then as we go row by row, we either multiply or divide the multiply values in or divide values out of that running product column and if the sets are equal like by the virtue of this kind of the formulas that you can see here on the right hand side, you should end up with one at the end.

This is a very kind of standard way of doing this. There are other variations on this where for example, you can start not with one but with some other value, and then you run through the same product kind of kind of computation running protocol, and then, you know, you may kind of initialize your set in the one way, or you may end up with not one, and this is useful in other ways, like you can basically say inputs and outputs of this table you can kind of uh pre or uh prime them, or um you know, use some outputs out of them to say, okay, like it didn't actually was equal, but I can tell you exactly which parts were not equal, and that's useful in other ways.

Um yeah. So, there is one problem with this, though, is that uh as soon as we introduce randomness, um like our trace usually base field elements, so randomness and you know, adds a little bit of What did it find? Uh um complexity here. So, what we need to do is that we actually have an auxiliary trace, as what we call, uh and which is actually an extension of the field, and this really matters only if you're in a small field, which most dark nowadays tend to be in a smaller field. If you're in a large field, extension like you still have auxiliary trace, but it's it could be in a in a same field, but let's say 64 32-bit uh base field, uh you actually need a

larger value for randomness. 64 bits is not not enough for randomness. Uh 32 32 bits is not also enough. So, you usually want to be at like 128 bits, or maybe even higher for um for a good level of security. And so, the flow is usually the prover commits to the values that they want to multi-set check in the main trace. Um then the verifier um sends the randomness. Usually, this is done via Fiat-Shamir um uh kind of transformation practice, where we don't we go from interactive to non-interactive protocol, but you basically get this random value alpha.

This random value alpha then um um you know, is kind of used to compute this auxiliary column, which is gets added to the auxiliary trace, and um you know, we get our multiset checks. Um Now, and then yeah, we need to impose the boundary conditions on this auxiliary column, like if uh if we want one to start with one and end with one, if we want the sets to be completely equal, or again, as I mentioned, you can actually initialize or like put different boundary conditions on it. Now, the other useful thing would be like is to be able to specify multiplicities for values.

This is um a good example of this is a range check. Sometimes um you know, the same value may get checked many, many times, and instead of like repeating it many, many times in the trace, you may want to say, "Okay, I've seen this value like five times. I don't need to repeat it. I don't need it to occupy five separate cells. I want it to be um uh kind of like still very efficient expressive wrong time. So, basically, what we get is like we would want to say, "Okay, this is the value that I'm going to put in the um in the set to multiset check against, but I also want to specify how many times it needs to go into that set."

So, you would say, "Okay, some values go zero times, some values go one time, some values go five and 100 and and so on and so forth." So, this is very useful again when you have a well, let's say a relatively short trace, but like every row can contribute multiple range checks uh as an example, and um instead of like growing the length of the trace, you can just say, "Okay, this value was range checked like 100 times." And you don't need to like add extra 100 rows to your trace for that. Um so, this would be very uh cool thing to have, and here you can see like this is a general form expression of how to do it. The problem, of course, here is that these are no longer um um

the constraints no are no longer polynomials. Like if in the in this general form, like if you try to apply this multiplicity this way, um you don't get like the same polynomial constraints. Um so, you kind of like are um you know, in a in a difficult spot. You can actually do multiplicities like in a very early version of my VM, we did like limited version of multiplicities where you could specify like a limited set of multiplicities, so it would be like, "Okay, I'm going to add either 0, 1, 2, 4, or like 8." And this would be your only multiplicity choices. And in this case, you can actually write constraints where you can say, "Okay, this value is going to be repeated four times, or this value is going to be repeated two times."

Um the constraints are not as nice, uh but it is doable, uh but there is actually like uh much nicer construction, and this is lookup, and here is where I'll hand it off to Phil. Yes. How in if you go to slides, you'll But how come you have multiplicity value of zero? How can you know that A3 is going to be multiplicity zero? How do you uh like how do you know ahead of time? Or I usually don't necessarily know ahead of time. So, like in the example of a range check, like the way you would do a range check is that um like and let's say it's a 16-bit range check. You would write all the values like the simplest way is you would initialize all the values from 0 to 2 to the 16 uh minus 1.

And um you would basically fill in those values like wh- whatever things you would didn't use, like uh the prover would later go in like say, "Okay, this value was never range checked, so I'll put zero in against it." So, it's not something that you would know ahead of time. It's kind of like after the program is done, you kind of usually fill in those columns. So, what you keep kind of a running uh count of how many times a given range check was used, and then at the end of trace generation, you would go and fill in the multiplicity column based on that. Yeah.

Um Um, we actually do uh like um in my N VM, instead of like listing all range checks like all possible range check values uh by like from zero to 2 to the 16 because we want traces to be usually sometimes smaller than 2 to the 16. We don't want to list all possible values if they're not used. So, we actually skip some uh values like we usually go in like powers of three, I think where we would start with like zero and then if like let's say the value between zero and eight was never checked, we'll like insert it like a value eight and so on and so forth. So, your trace could be as small as 250 or yeah, 256 rows I think we can like the smallest trace my N VM can have because, you know, uh the values of the range checks that were

never used are never actually added to the trace. We kind of do the skipping thing. All right. Now, I'll uh and we'll go to Logup, which is a much more exciting way to do a multiset check. Yeah. Right. So, where we left off is a is how do we how do we introduce multiplicities and actually able to prove them uh properly. Uh so, we'll start we'll start by doing it in the STARK context, which is a very similar construction to the running product column.

And then and what this leads to is okay, we're going to want to prove this with GKR instead of a STARK. Uh so, we'll start first with the STARK. Um Right. So, as a reminder, uh now I'll I'll just go into the derivation of Logup uh to just get an intuition for where it comes from. Where this equation we're going to transform this equation. So, we start with our multiset check uh equation that has these powers that we're trying to get rid of.

Um So, first we apply the log to both sides. Um you know, this is field elements and log is typically over the real numbers. Paper goes into the formal treatment of this, but for now we're just going to use this as an intuition. So, we apply log on both sides. We apply the log rule where multiplications in the inputs are transformed into addition. And also, this is how we got rid of our exponent. We apply the log rule of x to the y becomes y times log of x.

So, here our m a and our m b are now multiplying the log. And then the final step is to derive the both sides. So, we apply d d x um a bit of an abuse of a notation here. We're doing it over alpha and alpha was our random value. It was just to keep the slides similar. Really, this is a polynomial over x and we're doing the derivative over x. So, really substitute alpha with x in your mind. So, really we're deriving x. So, when you apply, you know, you move it in the sum and all that, this is ultimately the equation for log a.

So, you know, two things to remember is this is exactly equivalent to this will check the same thing as the the the the version that was doing a product. Um and our we succeeded at no longer having exponents. Like that's the that's the whole reason why we did this. Um So, here this is exactly the same uh equation as this slide except that I just moved everything on the left-hand side by subtracting both sides the the left subtracting the right-hand side to get everything on the left-hand side.

Um and so, we're going to do a running sum column. It's very similar. Instead of products, we get sums. Uh so, we're going to just going to do a very similar thing. So, our running sum column is going to start with zero. At every row we add in we add in we add the the set A and we remove we add all elements from the set A and remove all elements from the set B. So, in this case, you know, set A has at row one has A1 and so we do one over alpha minus A1 and then we remove what's in set B and so one over alpha minus A2.

And then we do this at every row where we take the previous value of the P column. So, it's a running sum. So, you take whatever was there before, you add in the new stuff and you you add in the new A's and you remove the new B's. And at the end, if your multi set check is indeed if the two multi sets are indeed equal, you're going to get a zero at the very end. And as Bobbin mentioned, you can actually make it not zero, but for the purpose of this presentation, it's just going to be zero. We want equality of multi sets.

Um So, if we look at the constraints for for this for this running sum column we have P at I plus one, so the running sum at the next row needs to be equal to the previous row. So, whatever was there plus add in all the A's and remove all the B's. This is not a polynomial yet because we have, you know, this these fractions. But by multiplying out the denominators um you know, we get a polynomial. So, the Don't worry too much about exactly the equations here. Like there's it's a lot of to take in at once.

The only take home message is we're able to make actual constraints that have a field element as a multiplicity. So, we're able to use multiplicities freely using log up. Um Yeah so now we're going to go into uh how to do this with GKR, which is uh well, what Logup GKR is. Um and why we're all here. There's one issue to that we're going to look at right now that's going to be super important later, and Bob and I already alluded to it, is the degree of the constraints. Uh those are going to be a problem or something to deal with, and maybe even something that motivates the

use of Logup GKR. So, if you look here, we have degree three or more uh because uh our constraints are over all the uh the current all the variables in the current row and the next row, so all the columns in the current row and the next row, and so here we have P at I uh AI0 and BI0. Actually, AIBs AI0 and BI0 are in general polynomials of columns, so they could be they could have their own degree, they could be degree five and degree six.

But, the minimum is their degree one where they're exactly one column. So, the minimum degree of this expression is three. Uh and it goes up as you don't uh if if you don't uh if you don't commit to everything basically and you do polynomials uh of columns, then this degree goes up. And VMs typically have a limit on the degree of constraints. In VM in mine currently, they're at nine, so it's pretty high. Uh s- many VMs use three, and so you're basically not allowed to do any uh use any polynomials of columns, you need to use directly the the columns. So, if you need these expression, you need to commit to new columns.

Uh yeah, you need to create new columns just to make that work effectively, and that's extra work for the prover. So, then yeah, so let's go into Logup GKR. We'll we'll come back to this point. Uh so, GKR for Logup. So, GKR is a an old older protocol and it was adapted to make it work for Logup. We're not going to discuss the original version. We'll just talk about the modified uh GKR, but it's in spirit they're the same. So, GKR is a protocol to prove the correct evaluation of a layered circuit.

So, we have a circuit here. We'll go into the details of what's in there, but just in general, you have a circuit and you want the prover to evaluate it and the verifier to succinctly be able to check that the verifier indeed uh that the prover indeed did this correctly. Uh this is all that GKR does. All that it does. So, we're going to have We're going to design a a circuit for Logup. And it's going to encode effectively this equation, which is that's the Logup equation we we've seen.

Uh we're going to design a circuit that computes this. Um So, in the first row, we're going to encode uh the entire sum. So, really here A over B and C over D, the this is the flattened version of uh what you see on the the double sum you see on the bottom. So, it is for every row, there is K elements, you flatten them all out, and the the the the input layer of that circuit is going to contain all of these fractions.

And then what we do is when we go up a layer, so for with every new layer, we reduce the number of fractions by half by combining uh just how we do it in high school math, uh combining fractions. Um with a common denominator. And we do this until we have one fraction. Actually, for technical reasons, we'll have we'll we'll stop at two, but conceptually you can we'll go all the way to a single fraction that is equal to like at every every layer sums if you were to sum the fractions, they all sum to zero in our in our case.

Uh in general, it's some number, but really we'll just talk about zero. So, what does that look like in a in a circuit? We'll have one node per fraction, and each node is going to contain two numbers, the numerator and the denominator. And a sum is going to be defined as a sum over these pairs is going to be defined as just what you'd do with fractions. So, AD + CB for the numerator, and then BD for the denominator.

And uh Yeah, they in the paper they call it the uh projective representation. Whatever. It's like it's pairs, and you think of them as as a fractions. Uh right. So, then I guess just conceptually we have everything for log of GKR is in that instead of doing this running sum product running sum column, uh we're going to the provers instead is going to build the circuit, use GKR to prove that it was done correctly, and then we will have proven our log up relation.

But now we'll dig a bit more cuz there's actually a lot that goes into it. Um I will not go into all the details of GKR. I think it'd be pointless. There's already, you know, a bunch of information here. We'll just go into what you sort of need to know for this presentation. Feel free to ask questions. Um Yeah. Uh It's uh it's a little tricky to go into enough detail, but not too much. So, we'll just I'll go into the basics. So, what is sumcheck? I won't go into all the details.

All that's really important for this presentation is uh first it's multivariate and so G is over, you know, M well, in this case M uh variables. And what you prove with a sumcheck is this G it's a polynomial it's defined over F F being your field F to the M uh M field elements, but you evaluate G over the Boolean hypercube or really all all bit uh combinations of M bits. So, 0000, 0001 all the way to 1111.

You evaluate G at all these points, you sum them up and the sumcheck sumcheck is a protocol to prove this value that this value is computed correctly. Two things that are important is obviously there's polynomials and therefore you have, you know, evaluations at random points. Uh in the case of uh sumcheck we're going to be sampling M random points during the course of the protocol and the verifier at the very end needs to evaluate G only once and at this one random point.

Uh this will and I'll come back to this, but uh this is like the crux of sumcheck. Uh the second concept of 2 of 2 uh that's necessary is effectively how do we do interpolation in the multivariate context? Uh you know, Lagrange interpolation in the univariate context most people are familiar with. Uh I didn't assume that everyone had done it in the multivariate context. So, we'll just go a bit more quickly into uh what that looks like.

But, it's exact you can think of it exactly as the same as you have Well, I we'll get to it. So, first you have the equal function and it's over M X's and M R's. And uh yeah, so it's X I R I plus 1 minus X I 1 minus R I. What is this? Uh it effectively outputs when you put values of when you put bits in, it'll evaluate to zero if they're the bits are not equal, and it'll evaluate to one when the the bits are equal. You can actually plug the values in and check for yourself.

Uh but that's how it's designed. But again, ECH is a polynomial. It is not just defined over the Boolean hypercube, uh but it's really designed to be uh to have this effect. Um I guess one thing to note is that the degree in X in all X I's and in all R I's is one. Uh if you stare at it for long enough, you'll notice that uh this is the case. You never have X I squared or whatever.

Um So, the multilinear extension or you know, Lagrange interpolation in the multivariate case is if you have your F function which is defined over bits, you know, Boolean hypercube, uh the domain is only bits, and you want to fit a polynomial. Um this is the equation. It's maybe a bit scary, but honestly, it's it's quite intuitive. We sum over all the possible bit patterns. We check if it's equal. When it's equal, it we output one. If it's not equal, we output zero.

And times F at that bit value. And so, you can see that if R is one of the bit values, let's say all zeros, ECH will evaluate it like the equal function's going to evaluate to to to one only for zero. In all the other bit values, it's going to output zero. So, it we're going to zero out all the other values. So, we can see that F tilde or the multilinear extension does indeed interpolate F. And uh the degree is one because it is a it's in R. And we as we talked before, the F function is multilinear.

So, yeah, by by uh I guess function composition uh not even composition. Uh the multilinear uh uh the the F tilde is also degree one in all the variables. Okay. So, two things, sumcheck and multilinear extension. Uh we're now going to come back to GKR. We're going to be building a some functions over the Boolean hypercube, and then we're going to be taking the linear the multilinear extension, and then we're going to be doing sumcheck.

So, this is why we did all this before. Um So, if we recall So, maybe if I go back just to give context, this was our circuit, and we're just going to zoom in on P1Q1, so the the middle layer. Um So, we have the middle layer here. Um We're going to build two functions over the Boolean hypercube. Um PI P is going to be all the numerators, and Q is going to be all the denominators.

So, and you can think of it as you know, it's the it's the bit decomposition of the index. So, P at the bit decomposition of one, for example, so 1 0 uh is therefore the the second one, EH plus DF, the second numerator. Uh Uh, P at 0 0 is AD plus CB and yeah, so uh, P really looks at encodes all the numerators and Q encodes all the denominators.

Uh, and we do that for every layer. So, if you remember just by circuit construction, we can then define every layer is defined in terms of the of its previous one. Uh, I mean just to really make that point clear. Uh, you know, here we had fractions. They're every every new layer is is taken from the fractions from the previous one and you merge them into a new one into this new layer.

Uh, so now all all that we've done so far is uh, we define the P and the Q functions. So, we're going to now just going to apply what we did from before, but just in that new language. So, P at I, so at layer uh, let's say one, it's is P at two. And then uh, I think I have, yeah. And it is ba- basically at the in the next layer, it's the numerator times the denominator plus the numerator times the denominator like left, right.

Um, this is a bit hard to say. Uh, if X is your bit, if X is in red here at layer one, so 00, 01, 10, and 11, uh, you can see that the children the the children start with if I'm a child of 00, my most significant bits are going to be 0 0. If my If my parent is 0 1, uh my most significant bits are going to be 0 1.

So, this kind of explained why if X is basically whatever is in the input layer, uh sorry, not the input layer, the the the layer above, you can see that on the next layer we see we reuse that X uh like here. We We reuse that X because of that fact, and we either do zero for the left or one for the right. Uh and so, I guess it's a little bit much to take in, but it's just rewriting exactly what we had before, but in this new language, and reusing this circuit structure where your parents have your the same bits.

Uh yeah. So, now we have functions over the extension to make polynomials out of them. We're just going to fit a polynomial over P and over Q. So, all I'm doing here, I probably could have wrote written this more simply, but all this is is the multilinear uh function for P. So, we sum over all possible X's, we pass into X, and then we pass in the definition of P.

And same for Q. I realize that it's a lot on one slide, but really there's not that much. If all that you get from this slide is we're building polynomials out of these functions, that's that's all there is. Um Yes. Yes. Like Like uh like when when you when we go to these extensions, like uh like the if your function is well-defined only on the Boolean hypercube, Ah, good question. So, the question was uh when we we said that the EQ function was only over the Boolean hypercube so how how is this well defined when we're in other field elements are not zero or one.

So the EQ function and maybe I was not as clear earlier is actually defined here let's go back to the definition. Yeah. It is defined over not just the Boolean hypercube like if you look at the equation on the right this holds like this holds over all field elements. When you put in zeros and ones you get these properties but it is actually defined everywhere. For all X's and all R's.

So the Exactly it's going to be a big number. Yeah. Yeah so this is yeah exactly thank you for that's I should have made this more clear. The EQ function is a is a polynomial that has these properties over the Boolean hypercube but really it's a polynomial. So if we go back to what we had big expression honestly I should have written it a bit simpler just cuz it's a lot to take in and actually there's not that much we have a like two sum check instances

here. What was sum check? It was summing over Boolean hypercube of some polynomial and this is exactly what we have. We sum over all Boolean hypercubes of X and we have the polynomial over X. And you know X hat in this sum check is is considered to be fixed. So the only variable when you're thinking in sum check terms is over X and X hat is fixed. Um What I'm trying to What I'm trying to get out with this slide is uh we we did all of this so that GKR can use sum checks.

Uh in the next slide um And please ask ask questions. I'm happy to spend Yeah. Yeah, it's basically what you're saying. Like those two polynomials which are expressed as sums over the hypercube, basically are Yeah, they're they're setting up this sum check where we can do a sum check for each layer in order to get from your large expression down to lower reduce. Exactly. Yes, that's precisely And that was like what I was trying to get with exactly this side. So, no, no, man, it's perfect. So, um Okay, so what he said. So, we have two sum checks. There's a standard trick uh when you have like two instances, you can just take a random

linear combination uh and just solve one problem of uh the combined like the the the batched or the combined problem. So, here on the left we have PI at X plus lambda QI at X. So, that lambda is a random uh is random, so we're looking at a random linear combination. And then uh when you actually work it out with the sums and all that, you get this on the right. You get the X function times the P plus lambda the Q.

Uh this is like copy-paste of P plus lambda and then copy-paste of Q. So, this is our sum check problem that we run at every layer. I will not go into the details of exactly how we do this reduction, but the I mean, as exactly as uh as was said is the whole point is And again, more details in the in the hackMD, but like for the purposes of this talk, we have a sumcheck that is going to reduce to another layer to the other to the claim for the next layer, which we're going to use sumcheck again to reduce to us another sumcheck problem all the way down to the input input layer.

Uh Right. So, also just to try and give an intuition is we're never able to complete the sumcheck at every layer. It is never done because uh if you remember from sumcheck, the verifier has to evaluate G, which is like whatever's inside that sum uh at that random point. But G in this case is a bunch of of circuit nodes, and the verifier doesn't have the circuit nodes.

So, what we do is the prover sends in the values as claims is like I'll I'll fill in whatever you don't have, and then in the next layer we'll prove it recursively. So, the intuition is this uh and so by reducing to we mean prover sends whatever values are needed for the for the untrusted values that the verifier needs to complete this round sumcheck, but then we're left with okay, well, these values I don't trust. We're able to combine them into this what's at the bottom of the slide, PI + 1 at this row it's just some new random variable.

Uh yeah, random value. And and then we're able to do this recursively until the end. So, the only mental model to have uh if you've worked with GKR, this makes sense. If you didn't, probably not so much. Like it requires a bit more thinking. Uh at least I did. So, maybe the only thing to to to really try and to fill is if if we if we go over all all that we've talked about is we have this layer.

We We Or rather, every layer we we fill in these two polynomials, P and Q, for every layer. And then the verifier says, "Okay, here's evaluate these at a random value. We're going to do this with sumcheck. At the end, I'm not going to be able to complete the sumcheck, so you'll send me some values so I can do that. But I don't trust those. So I'll reduce this for a statement, and it's all nice. I reduce it to a statement for the next layer. So by to prove this these values, I can we're we're it it is exactly the same as proving the next layer. All the way down to the input layer.

Uh that's the the intuition to have of how this process works. Uh right, so Okay, so I guess that's what I just said. So I'm going to first send but maybe we can also just do it a bit slowly. So we have our our our circuit. How do we prove log up in GKR? That's sort of the the the last slide about this. Um the prover sends the top layer. And as we said, we have two fractions left. So it's P0 at zero and at one, and Q0 or rather Q for that layer at zero and at

one. The verifier checks that if you interpret these as fractions, does it sum to what we said, you know, as Think of it as zero. It can be something else, but think of it as zero. So is your output layer correct? Uh and obviously check that the denominators are not zero before you do that. Uh if the verifier agrees, like, "Okay, perfect. Your output layer is good. Now let I'm going to need you to prove that it's effectively related to all the way down to the input layer. That this is not just some random those some random numbers you sent me.

So then we sample uh at like an evaluation point for Q and P and Q. This is Okay, prove this to me. At every layer we're going to run some check uh at this random point, which is um Yeah, it's this polynomial check of I'm going to sample at a random point. If it's good uh if if it checks out, we're happy. Um and then for the final layer in this slide we're going to assume that the verifier has the final layer.

We're going to correct that in the next slides, but we're just going to say, "Okay, I've reduced it to this final layer. I will then evaluate the final layer, make sure that it all checks out, and if it does uh yeah, we're done." So um any questions up to now? There's been a few, but uh I can Okay so So what we have until now is we were able to prove everything all the way up to the input layer.

And the input layer could almost be a talk in itself in and of itself because there's actually a lot that goes in there. It was by far the hardest to understand for me. Um I'll I have a question. Like Yes. How do the verifier knows the the biggest layer below the root? Yeah. Good question. Uh this is this is the topic of this section. Yeah. Uh and so gluing log of G cactus stalks, like that's like a big challenge.

So what we'll go into is really understanding what needs to be done, and we'll give some details. We won't give them all. Happy to dive wherever is needed. Um Can you also have a look at the minutes left. Okay. So, okay, so that's why All right. I'll I'll do this in about 5 minutes. We have a few things to run at the end. Um I'll skip this slide then. Uh Okay. So, as an example, we'll just remind ourselves, we've talked about this earlier, of how the What What is the input layer?

Right? It is uh as a simplification, elements from our trace. Uh Bob and talked about it. I talked about it for a bit. So, on the left-hand side here, we have our trace. And as a simplification, we'll say that the first The entire first column is all the the MA values. The F2 is all the A the multiset A. And then same for F3 and F4, but for for B. So, you'll have the multiplicity for B, and then the B multiset. And when you lay out the log-up equation at the bottom, you have um uh yeah, I mean, we we've been over this.

Uh this is all stuff we've talked about. And again, that's just a reminder, this is how they're laid out. The big challenge for the input layer, uh given that there's not so much time left, uh we'll just go more with the intuition of the work that needs to be done, is the very like there needs to be a protocol to prove that these values actually come from the trace without ever showing the trace, because in a STARK, the trace is never sent to the verifier. So, how like how do you do that? Uh The There's going to be a boundary between the GKR and STARKs, and that boundary is going to be the multilinear So, if you take each where F is the the column, so we have M columns in this case.

Uh GKR is going to reduce to a statement about the multilinear extension, or you you know, fitting the FI columns at this random point. It's going to be able to prove all the way up to that. And then the stark is going to take it from there and it's going to say, okay, this is what's left to be proven from this entire circuit evaluation. This is my job now to prove in starks. Uh one thing to notice is that starks don't speak the multivariate language. We typically speak in univariate or rather we speak in univariate language. So this multivariate multilinear extension is not a thing in starks. So we need to to do this somehow.

Uh Honestly, I won't even go into that. Like just to give a final intuition is we're going to have we're basically going to be going to be proving this with two columns. We're going to have one column that is the evaluation of EC that we've talked about. And then another column that uh puts everything together. Like I don't I'd like to spend more time here. Uh I think we can maybe run run some of the go to the conclusions. I think the conclusions of when is GKR good maybe more interesting than the specifics of this.

Uh happy to go into it though if there are questions. The picture will be a little bit inside the J. Uh No so EC we're summing over all X's. EC is taking that row equal and then but then you pass in the X. So like over the over bits when row is equal to 01 or sorry bits. Uh Does that make sense or I did not explain how to construct the sum so I So if FJ takes one variable and X is a vector.

Mhm. So and then row X is No, sorry. Row is a vector as well. Uh I yeah, row row is uh is as wide as X's, but in field elements instead of it. Honestly, I I apologize. I just that that was not properly explained. Uh, yeah, that's a All right, so that that's like when is it worth it? Uh, that was not that's the part that was very much not clear to us and it is uh now. Um, so if we try and like take a step back from everything we did, we're comparing when we're proving log up either in STARKs or in GKR.

In STARKs, we often have to add a bunch of like when our expression gets very big, as we talked about, we need to add helper columns. Um, and maybe it would help to just go back to the slide and we'll just talk from there. Uh, the big issue Yeah, so this slide at the bottom. The big issue with the proving it in STARKs is you probably have to add a bunch of columns for these intermediary expressions that would blow up your degree to a very high if you didn't.

So then all these columns in the STARK protocol, they're all being hashed. Uh, so you can think of when I'm when I'm proving log up with STARKs, I have a bunch of extra columns that are forced for the log up only. And the question is, is it worth it to remove this work? So we're going to get rid of all these columns and then add the overhead of all this the the protocol we talked about for GKR has a cost. So which cost is smallest is the question we have to ask. And there's a like three parameters we'll focus on is how how fast is your hash function? So if hashing these columns is extremely expensive, then getting rid of a bunch

of columns to hash is going to be good. If your ha if your hash function is extremely fast, then it's all you know, if it's if you think of it as free, then you don't care to add a bunch of columns. That That's one consideration. A second consideration, which goes down to how many columns you have, is how how many fractions like how big is that K here? How many fractions do you have in your bus? Uh or in in your multiset check. If every row can add a thousand elements, you're going to need, you know, way more columns uh to just to fit these these intermediary values that like many many many many columns. That's going to be a lot of work for the prover. If you can

get rid of all that work and put it in GKR instead, um might be good. So, like just another consideration is how how many things are you putting in that bus? And then um Uh the final one, well, I think we want to talk about the extension field. We might skip that. Uh The degree is the last one. Yeah, yeah, yeah. Right, right. So, the degree is the last one. So, uh well, I guess it was the second one. So, uh we've alluded to that already. So, if the the degree of your constraints is low, you need way more helper columns.

The higher you go, the the less columns. So, it's always in this in this question of how many columns am I adding and how expensive is that versus the overhead that I get with GKR. Uh only benchmarks can tell you that at the end of the day. There it's many many many many variables. Uh so, that's what we're going to do. So, I'm not going to show code cuz I don't think we have time. I will only run um So, we're going to vary which hash function. We're going to use a slow hash function and a fast hash function.

And then we're going to be increasing the size of the bus. So, we're going to look at slow hash function uh and then add more things to that bus so that the we need to increase the number of columns by a lot. Um and we'll look at it, okay, what happens when we prove that in STARKs and what happens when we prove that in GKR. So, on the left-hand side, is that big enough? Uh well, honestly, it I I can just read it out. So, this is on the left-hand side is going to be proving with STARKs, on the right-hand side is going to be proving with log-up GKR.

So, uh this has 16 the the 16 fractions per row. So, the K here would be uh 16. And uh so, we've proved it in 4 seconds, like 4.4 seconds. Uh if we do the same thing with log-up GKR, um again, this is using a slow hash function. So, we expect log-up GKR to be good at some point. Uh 4.5 seconds. So, at 16 elements per in that bus, they're roughly equal.

Um if we go to uh 32, so now we're we're adding even more things in that bus, so we're adding even more helper columns, so the slow hash function is starting to be expensive. Uh 6.5 seconds if we do the same thing um with log-up GKR, hopefully, log-up GKR is better in that case. Uh and 5.9, 6.5. Yeah, so it's you know, 500 ms, 600 ms faster. And these are not proper benchmarks. Uh we should, you know, use proper tooling.

This is just for just to show. Um Okay, so what we've seen right here is that at 16 the size of the bus 16, roughly equal. If you add in more, GKR started to be useful. Uh and you know, real numbers I think in uh in my and VM we have about uh 60, 70 uh the fractions in our bus, so where it's definitely worth it using RPO using this slow slow hash function. We're going to do the same thing with a fast hash function, so Blake 3.

Um So, Blake 3 will do 16. And the punchline is that Blake 3 will never log of GKR will never be better when we use Blake 3. Uh unfortunately. So, Blake 3 uh we did it with 16. Right, so we have uh 500 milliseconds, so 0.5 seconds versus 1 second.

Uh and if we go all the way to the bigger one, which is 168 uh sorry, 68. If we put 168 things per row in our bus, so you know, many, many, many, many helper columns, uh we have 4.5 seconds in the Blake in the RPO case. Uh sorry, in the log up case, no GKR. And in the uh log up GKR case, uh six So, 6 seconds versus 4.5. So, log up GKR is still slower.

Okay, couple things about that. So, slow hash function was better with a sizable bus. Fast hash function, at least this current implementation, uh log up GKR is never faster. Um Al has worked on a bunch of awesome optimizations. That is not what I'm running right now. We get closer, but it's still not quite there yet. Um So, our big So, for the Miden roll-up specifically, we're going to use a slow hash function.

So, it would be preferable to use log up GKR. Um but maybe we don't want to do it for the entire VM because people might want to use it and use a fast hash function in which case log up GKR would slow them down. Uh So, yeah. I guess like the big big takeaway from from all of this is log up GKR is not always good. Um and the the the the main framework that we have is the cost of all these helper columns versus the overhead that GKR gives you.

Um And uh I'll leave it at that. Yeah, I think like the takeaway is that now currently the limitation of Miden VM where we have relatively like You want to talk over the in the mic? Yeah. Um we have like relatively uh few bosses. Like we don't have a ton of boss columns uh and we have high degree. Um I think where we ended up is like using RPO, we kind of break even in terms of log up GKR and uh non-log up GKR approach. If we use Blake 3 as a hash function, we are like twice as slow, I think. I think that's what we've seen.

Now, uh we do think there are a few ways we can improve. Like one of the ways like it's if we went to a lower degree uh kind of a situation of Miden VM where right now our degree bound is nine and if we were to go to degree uh three, that would like automatically mean that we need more intermediate columns and in that case um like for in a RPO context, like there is it's no brainer. We should be using log up GKR. There is uh no reason not to use it. And then Blake if in a Blake context, it's I still I still think it's an open question. I think I'll you try to get it close. Uh I don't know if it will break even or will be slightly better. We are not quite there yet to say for sure, but even with Blake, we might be able to get

to a point where it's kind of like a parity, but it is still an open question whether we will get there. But yeah, that's kind of the main thing. There I think there are a few other things to consider about Logup GKR because one of the things that was not obviously obvious to me like in the Logup context in the beginning like you can actually place boundary constraints against the starting value and the ending value of the of these columns or the running sum columns. In Logup GKR you cannot do that. You kind of can have like this single value for the entire sum, but you do not you're not able to do like bound boundary against the beginning and the end. And in some context it doesn't matter, but in some context it does matter where you like if you want to link

through those things externally it may create a little bit of challenges. So like I think overall like Logup GKR work is super cool and like we learned a ton. Whether we'll use it immediately in my VM is probably you know we still need to figure out if we if there is usability kind of like immediately usefulness to this, but I think in the long run there is clearly something that we will use as we kind of reduce the degree and do other things. So like it's been a very interesting like learning experience I would say. Yes. In the demo you discussed only the proving time. I noticed that there's also was verification time and proof size.

These are the last two examples it was clear wins for the Starks rather than the GKR. You didn't notice it for the first example. So does it ever win in verification time and proof size? Yeah, that's a good question. Al, do you have a better intuition as that as to verification So the question was we've only focused about proving time. Um what about verification time and proof size? I think verification time should still be even competitive for Logup GKR because you are not doing a a of hashes, right? And you are doing more algebraic like the verifier basically just evaluates polynomials for for the subject that we're So, it's very hard to beat that in a sense compared to hashing the leaves.

Like if you have like very wide traces, it means that you have to have to hash like more of the actual trees. So, from that point only maybe, but the proof size is probably worse. Probably worse. And I think most of your hashes you don't really do for all of the columns. Most of your hashes will be Yeah, I see. Sorry to interrupt, but we're running quite a lot over. We have a break Yeah, yeah, yeah. So, maybe continue the discussion outside. There's a nice little hangout there. Yeah, I'd be happy to like step outside and talk through those things. All right. Thank you very much. Thank you for joining.