Lessons from integrating LogUp-GKR in the Miden VM by Philippe Laferriere | Devcon SEA

[Music] hello um so I'm Phillip uh work on the mining VM and um yeah today we're going to talk about our lessons from integrating uh log up gkr and the M VM uh it's going to be fairly high level so I wrote a little hackmd book at bit.ly log up-gk R where a lot of the details that we don't cover here are in that book so for context log up gkr is a uh technique proposed by Shahar and olrick around this time last year in their paper improving logarithmic derivative lookups using gkr so in this talk we're going to first look at what log up is first of all and then uh how log up is typically proved with Starks and then we'll look at how you do it with gkr which is the main the main purpose of the talk then our takeaway is from doing so so really quickly log up is a protocol to prove the equality of two multi sets uh multiset is a set where repetition is allowed so they're super super useful in Virtual machines uh they allow you to have practically unlimited stack def um do large number of range checks so making sure that a given value in your Trace is within some bounds and uh they allow communication between different parts of the trace so for example in your main processor you could have an exor and prove that exor somewhere else in your trace the multi set check is what you would use to connect the two parts of the trace so for example this is a uh depiction of the uh M VM Trace so a 2d grid of number effectively and in this context a multi set check would check that the multi set represented by the green squares is equal to the multi set represented by the blue ones so they're they're basically multi sets on values in your Trace multi set checks um so we'll jump straight into the equation unfortunately we don't have time to talk about why that makes sense uh it's in the book but we'll take some time and and analyze it together so uh log up is there's four sets of variables of interest um the a AIG J and B J uh are the elements in your multi set A and B correspond uh respectively and then uh the m a and the MB are the corresponding multiplicities of those elements so for example if you want an element to appear five times in your multiset but it's only once in your Trace you could set that M to be five and it's going to be the exact same effect so a multiset uh element is the the expression is really its multiplicity over Alpha a random value minus AIG the the element AIG so we have these two uh these two terms per or actually K of them per row where the I for the row goes from 1 to n minus one the big take away from this is log up is one big sum of fractions that's the one main thing to get from this slide and we're going to have to prove this so how do we do it with Starks um so that's our equation at the bottom and we'll just use an example so we have a main trace of two columns A and B and each column contains our one of the two multi sets so column A contains multi set a and column B contains multi set B and we can visually inspect that the two multisets are equal they're just a permutation of one to the next so the algorithm to actually do that to implement the log up is to add an extra column that we'll call P and we say it's a running sum column uh so how is it built it starts at zero and then following our equation if we look at the first element it's off by one compared to the trace but we all the multiplicities are one and so we have one over Alpha minus A1 which is the element in the multi set a minus 1 over Alpha minus A2 the element in B and that again is just from our equation uh then for the next row we initialize it with the the contents of the previous row and that means we're basically running an accumulator and uh and then add the new elements so 1 minus Alpha minus A2 is added from the multi set a and we remove one 1 over alpha- A3 from from B uh same thing over again we we initialize with the previous contents add in the new elements and since this is the last row uh it's going to all the terms cancel out and it's equal to zero so the boundary constraints on on this col armor that it must start at zero and end at zero if your multi if your columns if your multi sets are actually equal but we also have to check that each row is is built correctly and that's what we do in a transition constraint so we're going to zoom in on that uh so we have P here um and uh the the transition constraint is basically what we just did in the previous slide so pi+ 1 so the next row is equal to pi plus the new terms so when a is equal to one uh yeah only two terms this is not quite right because um the constraints must be polinomial and fractions are not you can't have a fraction in your polinomial so what we need to do is simply multiply out the PO the the denominators and so when K is equal to one with only two terms uh per row uh we get this expression which is a degree 3 polinomial because we're multiplying three variables together uh but that was when K was equal to one uh when K is equal to two uh we're going to have four terms in that row so we're going to be multiplying five elements here so degree five so as K increases so the more terms you have in your multi set per Row the larger the degree the trick is in Starks you typically have a bound on your uh on your transition constraints on the degree of your transition constraints and so how we deal with this is we simply make a new column if if only we can only have let's say two elements here we'll create a new column again a running sum with whatever elements are left over that we were not able to do with the previous column and so on and so forth it could go up to hundreds so again the takeaway of when we prove log up with Starks is that we need a collection of running some columns main takeaway let's see how we do it with the gkr uh gkr uh for context is a protocol that uh proves the correct evaluation of a layered circuit uh so here we have a layered circuit and yeah so effectively the prover evaluates the circuit and then uses gkr to convince the verifier that this was done correctly uh with log up we have a specific circuit that encodes the log up relationship so we're going to spend some time thinking about how that circuit looks like how it's designed really uh if you recall log up is a sum of fractions and so uh over your entire Trace so this is depicted by the the the sum of fraction at the bottom here and to get the the next layer we're going to merge uh pairs of uh of these terms by common denominator just like what you did in high school so on and so forth until we get just one uh one fraction and really we're going to stop at two but for for intuition we'll say that we we get just one uh one fraction um so that's not really a circuit but it's a simple translation to get a circuit uh basically every note in your circuit is going to have two numbers corresponding to the numerator and the denominator and then to merge two nodes together we we apply the the the which we Define as the sum over those pairs is really the sum of fractions so the denominator here if we look at uh ad D plus CB that's the denominator that we got from those two fractions and then BD is the sorry that was the numerator and BD is the denominator so then what do we do with uh G on this circuit there's actually slight modification to the gkr protocol but we're we're not going to have time to go through this again that's all in the book uh so at a high level theover evaluates this circuit uh and then sends the output layer to the verifier so only two fractions that represent the exact same uh exact same sum that was in the input layer but really at on with two fractions so the verifier can easily check uh that this is equal to zero and we'll also check the denominators are nonzero to make sure that they're proper fractions and and then prover and verifier are going to run gkr to convince the verifier that uh the the circuit was properly evaluated and that translates to that the output layer really comes from the input layer it's basically the same sum but represented in a different set of fractions we're not done yet because we've we know that the output layer is equivalent to the input layer we don't know yet that the input layer was properly populated from elements of your Trace uh to do that we're going to have to do this in Starks and we're going to have to add two columns to our Trace we will not go into how we do that unfortunately because it's like very cool and like quite quite clever honestly uh but the the the long story short is that we need we really only need two columns in uh in our in our trees so if we take a step back um when we were proving log up with uh with Starks we ended up needing a collection of running some columns again that can go up to 100 or more with gkr we needed only two columns but with the overhead of gkr on top of that so then the big question that we asked before starting is which is best and like anything in VMS there's no simple answer uh it depends on a variety of parameters uh so we just went on and and did it and so uh there are takeaways from uh from doing this many many many different parameters influence which technique is best in what circumstance depending on what you care about um we're going to focus on three uh hash function speed the degree of star constraints and the size of the bus so hash function speed uh when in Starks you have to choose your hash function uh and by by slow or fast we really mean on for the prover on on the PR's machine how fast is it to to Hash two numbers or whatever or how however many so the reason why the hash function speed matters in choosing one or the other is that if you recall from log up we were adding a bunch of columns and each columns adds hashing work to the prover and so if that hashing work is expensive because you have a slow hash function it's going to going to cost a lot to add these columns uh so the green check marks means favorable to gkr to to log up gkr and the reason is uh log up in Starks needed a bunch of columns in gkr we only need needed two and so if we go from hundreds to two that's a lot less work for the prover of course there's overhead from gkr but from if we hone in on that parameter it's very good degree of star constraints uh same idea so uh if you recall from earlier the degree bound on your star constraints is what made us is what made us create new columns because we were not able to pack more uh we were not able to pack a bunch of uh fractions in a single column so the lower the degree the more columns you'll need and then the same intuition comes back uh the lower the degree the more columns the more columns the more the more work for the prover uh and so removing all these columns when switching to gkr is favorable to gkr again if your degre is high you're removing fewer columns and so maybe the gain is not as good the last parameter is this size of the bus uh by size of the bus we really mean how many fractions per row are you adding that K from the previous uh uh K from the previous uh equation so here if you have a very large bus so meaning you're adding a bunch of fractions per row you're going to need a lot more columns same intuition so a large size uh a large bus is going to mean a lot of columns when you're proving in in stars and a lot less a lot of Prov work that you're removing when you're switching to gkr so this is our mental model rough meal model for uh when when to use log up gkr and when not to use it so in the case of MVM we the rollup uses a slow hash function uh so that was that was good that was quite favorable but the Mind VM uses quite high high degree of start constraints we use nine uh three is uh is quite popular five is also used so we're we're pretty up up there so not very good for log up gkr also our bus was kind of small we only had a few extra columns for log up so basically we by optimizing gkr and gkr is based on some check and there were a lot of optimizations there to get it down to get log of gkr down to be equivalent in prover time to uh Starks only but it's as soon as we went back to a fast hash function we used Blake 3 uh log up gkr was still slower and uh it seemed like maybe it's it would maybe even never reach uh like parody because our bus is small and our degree is High um we were not the only ones to implement this starkware also did that and um Andrew Milson was uh very nice and shared with us uh the numbers that they got so they they have uh the their in their experiments they used Blake 2 as a hash function so quite fast but they have degree three constraints so very nice for log of gkr and a very large bus like hundreds of columns and they were able to get a 15% Improvement uh and they will say that they're still not done optimizing so they think they can get that even higher but it just goes to show that even though they have a they use a hash hash function that's fast they were able to make log of gkr worth it again this is all pro time the one thing that this slide doesn't talk about is uh proof size and verifier time maybe the the big the big drawback uh for log up gkr I'd say is proof size so these extra columns that we're adding and all the nodes that the the the circuit nodes for log up gkr are um are all in the in the extension field so example but uh in the M VM we use uh goldilock so roughly 64-bit field extension field is uh where we do any any kind of Randomness is done in the extension field and that's roughly 128 bits so every number is is larger and proofs kind of at very large uh for traces that are that we can expect in in the rollup we were getting maybe 200 kilobyte size uh proofs just for gkr and typically we're able to get it maybe at 80 or 100 kilobytes uh so it really blew up our our proof sizes up and we're actually trying to to decrease them so that uh so ultimately our our current um takeaway is that we're not going to use it for the first version of of the M VM but we're also looking into uh making some pretty drastic changes in the future and uh yeah this is the m map we're going to use uh when we when we do that and whether or not we want to use log of gkr But ultimately it was a a great experience and uh like a very clever idea by Shahar and O so again like most of the de details uh we didn't talk about if you go to that link uh most of them are there I I try and make it approachable uh feel free to ask questions on the hackmd directly uh send me a DM on Twitter or just message me uh whichever I'm happy to to have more conversations about this and yeah uh hopefully youn you learned something thank you thank you phip it was an insightful talk so again I just remind you that there is a q code if you want to ask questions um but we have actually a few so maybe why if we start with the first one do we uh in practice mix JK and stock for different use cases other than look up I guess yeah that's a really good question uh and something that we start to think about more uh currently log up is the only one that I'm aware of that is being used or even tried um but uh it is on our we are going to think about more ways uh that we can do this because now we we have a clear use case and or rather a clear example of how it can work and uh yeah but so far I I don't think so so there Reas is like just implementation wise you need to try it to see how it works so implementation wise absolutely even just understanding like the glue from from gkr to Starks was non-trivial to understand at least for me because you're going from a multi-linear world to a uh univariant world uh and there's some but I'm pretty sure that some of the insights there can be reused for other purposes that makes sense um yeah why if we take the second question is log up more gkr friendly than other lookup arguments yeah another good question uh I do not know any other uses of there might be but I do not know uh other lookup Arguments for uh that use gkr so uh I I don't know and you were using like log UPS before introducing JKR so we it was stock friendly I guess right so we use actually we use log up only when we need multiplicities because uh as we saw it makes the degree log up makes the degree go uh go up pretty quickly because of these denominators you have to multiply out I mean a constraint degree sorry uh for most of our lookup arguments in Starks we use good old multi set checks we I call them like vanilla multi set checks they're based on they're not sums of fractions they're really uh it's not a running sum column it's a running product and it's slightly different your degree is slightly better so unless you need to uncode multiplicities explicitly uh we don't use log up but I don't know how to do that other one with JR okay cool cool we have more questions so what's hash function function you are using right so the M VM does does not you can use whichever one you want with the m VM uh we use the M VM in the M rollup and for that we use uh hash function RPO which is uh ZK friendly hash function and we actually I think we're going to switch soon to RPX so is it also it's like an improvement as I understand she's also stock friendly also yeah okay um then next question is how fast slow is gkr verifier in stocks uh yeah good question um I it I think it's comparable to uh from what I recall I was focusing Less on GK fa fire so I'd have to go back uh it was not drastically faster or slower it was you were getting roughly the same maybe a bit slower okay and does it change like in terms of the size of the lookup you're proven or yes but in the numbers that we that we care about so maybe traces of 2 to the 16 or we typically around that uh you didn't see many differences between uh it was relatively constant okay cool cool uh if we can just scroll down to see more questions and yeah miden law yeah good one it's a good one and maybe last question any plans for Hardware acceleration for the mid V yeah uh so we have uh GPU support that is maybe even in our main branch yet or at least soon to be uh but we have active GPU work being done uh more longterm we're also looking at uh using ZK specific chips but that are not on the market yet but it's already a okay yeah yeah great okay cool cool well well if we give a round of applause of for our speaker Philip thank you very much