leanVM-02: Memory Models and Lookup Arguments
leanVM Workshop 2025 · 3 Oct 2025 · 1:28:01
A workshop from lean week in Cambridge, UK, held on 3 October 2025 and hosted by the Ethereum Foundation. leanVM is a minimal zkVM designed for post-quantum signature aggregation and recursive proving. This session covers memory models and lookup arguments.
Speakers
Topics
From leanVM Workshop 2025, hosted by Ethereum Foundation.
Transcript
This is okay. You can take my can. >> Yes. So I think that after the presentation of Emil that went quite quite deep into the details of the we are trying to organize today into three main tracks uh in order to discuss various challenges that we face with the VM we try to be focused on the VM and we will discuss other topics during the other days of the first quantum workshop. Um so As summarized by we are working on like
the postquantum signature to replace BS in the consensus of Ethereum for the future. Um for that like we have decided to go to the path of minimum cryptographic. In the beginning we have tried to just um implement and the the program that we need to prove and try to improve that with existing ZKVM on the market like uh OpenVPN SP1 and a bunch of others. For now we think that they are kind of too slow and and complex orders of magnitude too slow compared to what we want and to what we have currently with the VM.
Um about this point we have seen recently the numbers of the current VM to speed up speed up and speed up again but this is always to reconsider especially with some VM like a jolt that is designed for simplicity or stuff like that. Uh this is always important to benchmark this stuff and so we are trying to also maintain kind of comparison with existing ZKVM when possible to be that current zkm are not are not slow or are too slow. Um we have also the possibility to write our full program into a custom circuit uh for in for
performance improvements but we think that right now with the recussion because you will have to handle like recussion and rewrite this inside the circuit and so this this is simply too complex to handle. That's why we went to the minimal cryptographic CKVM to simplify this custom circuit without adding too much overhead. We have also in mind this point about like folding or accumulation techniques with the recent work that we have seen especially with neo and warp. Neo is like a kind of latis based folding stuff and warp is cont but on the the ash ash world. Uh so we are keeping in touch
with all the authors of these papers. Uh soon we will kind of hopefully push like a small explanation on each research with because a lot to like this funding techniques and he did amazing amazing job about this. So we are trying to explain the pros and cons of each uh possible pass and explain why we could use possibly this folding technique because when you want to aggregate some stuff this is kind of like folding could be a natural things for this. Unfortunately for now we have no real implementation neither
neo nor war. So we cannot really compare the numbers that we have with aluminium for example with this kind of techniques to see if they worth more investigation. But we keep a lot of discussion with all of these guys also Don like this and so just explained by me we have this lean VM we mark VM that is purpose build this is not general purpose as just explained we have like a small compiler you cannot prove with this VM for example blocks but it should be really performant for like signature regation
So basically today we will try to have three tracks to discuss three main topics that we have but of course we can deviate and talk about other topics in the meantime. This is not the problem. So our first topic will be the check. Why? Because we have designed this minimal CKDM to be multilinear oriented. This means that we are not dealing with unared polomials anymore like this is the case for example with f like this but we are dealing with multiar polomials. So this is a complete say new world compared to un settings and the same check is kind of in the middle of
everything there both on the p side of things because we need to have like a zero check with the table of constraints and PCS in wheel also because at each round we have like some check to reduce the problem. So subject is very important. Uh we have a lot of optimization to be done on the sound check. Uh right now what we have is kind of simple check without that many optimization on the P. we have already like the univers that is implemented. But what we want is to have like a general check. So one
implementation to rule them all let's say with all the optimizations and so the check that could be efficient on the POP on the PCS and yet with a lot of optimization because this is one of the bottleneck right now. If we can reduce the cost of the sun chain, this will reduce the cost of the PP and this will also reduce the cost of the PCF. So this is kind of very important. Main what we will discuss mainly is about the possible optimization strategy that we could have with sun check.
Mainly the thing to remind uh is that we have two kind of operation with some check. Some implementation some work can be done in the base field. This is very cheap and this is at the beginning of the subject because we can do operation and multiplication between small fields. But after that for security reason the verifier should send randomness that should be in the extension field and from this point we are operating between extension field elements and so the multiplication are much more costly. For that we can discuss two strategies but we could have more obviously like very recent strategies by and paper from this year
where this kind of premp computes some coefficients uh in the base field before even inter iterating with the verifier and so this conserve a lot of this premputee work offline before interacting with the verifier and so reducing the cost of like followup operation with extension field then I I will share like some discussion starter like notes but we can have like a bunch of open question like is this kind of optimization the best choice for our PCS our POP why um also in all of these strategy you always have this idea
that you will apply the optimization the optimized strategy for the first round and then switch to the basic check what is the optimal number of round is it like four, five, seven more. Um and we have also this other strategy that is maybe more common and designed by so in this strategy you combine the first few rounds into one big step like to do like a big round at the beginning with a small film and then you switch for the rest of the computation to the classical sun check but you have this
benefit of having skipped couple of rounds five um we have seen that on the PI this impacts a lot the performance decreasing that by a huge this is also the case in other protocols that have implemented districts for example P news or others um on the PCS we have uh seen that this impacts a lot of the code external to the subject. Why? Because in this in this world like you see the your polomial in a complete different way with different dimension of the algorith and so it impact like the
prover the the generation of the queries the verifier that should interpolate differently. So it impact a lot of the code. Uh so again how would we manage this complexity? For example, we could have maybe like the p with this optimization and the PCS with the others or maybe something. We could have another strategy that could be complimentary to these two. For example, using CD and packing techniques inside the subject. How to rearrange things inside the subject to be able to do compressed operations at each round.
and then reduce the time. And the goal will be as we plan to integrate wheel into 3, we will need a sun check. And so if this is possible, the plan will be to have like very nice sun for small techniques, small field techniques into 3. So that could be used as a primitive for everyone. Uh yeah. So that will be like one of this discussion. The second discussion will be this afternoon about like the memory model of the VM and the lookup techniques as mentioned by Emil VM use a read memory model and so how do we efficiently prove that
all the memory reads are consistent and valid we have different possible strategies we have the classical run product where you have like kind of running product that prove your permutation Um the limitation what are the limitation for example where you have like multiplicities or stuff or like you have to run this product this is also limitation so that is widely used in all of the zkm almost all of the zkm right now use log so this transform this product into a sum we will see that this afternoon um to handle like multiplicities But like we have also a version of log
with GKR that was tried by many players but some of them like just abandon this and just switch back to to log. And we have this very new strategy that was implemented also by inside the VM that is local star in by and so this use like kind of specialized technique for index look up in order to reduce the amount of commitment we have to do.
And so yeah, we will kind of discuss this what could be a good strategy uh is maybe local a good one why lo is particularly useful and all of this. And finally we will have a third track about like the VM compiler all of the problems that were discussed by Emil with a for loop that is just either unroll restructure as a recursive function if this is too large to be unrolled. Um all of the memory stuff, the dynamic allocation, the MO, all of this stuff can be with the two pass stuff can be
discussed. How we could do better? How can we verify the compiler? Um how we can make it secure? Do we need like formal verification? We need the outsource of strategy. How can we optimize also like the the model cost? Meaning that how we can check all all of the compilation stuff in order to reduce the number of operations that then need to be done inside the VM. This is also an interesting step and maybe a final question with or without the compiler.
Why I I am saying this because we have seen like a bunch of new modern VM such as like KM open VM and the new one like the recussion project by where for now like you don't have this compiler, you just have like an friendly API to build circuits and so you don't have to deal with DSL and you can just like build your circuits uh thanks to like friendly API is it possible in our case is it too complex? Uh yeah, I was particularly thinking about this because our
Our project need to be laser focused on one case and so maybe we could avoid the use of the compiler by doing some clever trick uh to play with circuit builder API. This was also an idea shared a couple of day ago by from Karot in the conclusion of their paper they mentioned that they plan not to use um a compiler and DSL but to play with the different errors and through the different airs also with the logo. And uh an interesting point about this is a powder strategy with auto pre-ompile.
This is kind of the same stuff. They optimize the way that you generate the hair and the pre-ompile using compiler techniques under the hood. So yeah, on that there was also a project at PSC called uh to do uh the same kind of API but for two circuits. Okay. Okay. Okay. Okay. Very nice. So, can I ask this?
>> Do do we know to which uh devices are we optimizing this column for? Because is this for GPUs for CPUs? Like what? >> Raspberry Pi. >> True. Not true. The verifier is on a Raspberry Pi the proverb. >> Yeah. What we plan to do maybe better explain than me but validators can run on Raspberry P but a few of them will opt in to be aggregators like 10% of them for example and they particularly should run on a highend CPU laptop such as this one or a
better one. kind of >> we're hoping that the network will do well with just CPUs, but in practice what I expect will happen is that um someone will come in with one GPU and that will be sufficient to prove the whole network. >> But just the story is so much better if we only rely on CPUs. >> What's better about it? just the barrier to entry to become a navigator is is much lower.
>> Seems like it's low already if you just need one GPU. >> That is true, but it's actually one GPU kind of per subnet or because there's there's you need one GPU and a very good internet connection to to connect to all of the subnets. So the way that we do aggregation is that we have parallel subnets um where there's like partial aggregation and then there's a second round a second stage where you aggregate the aggregates.
>> Oh this is like a vision for scaling. >> So this is what we have today with DS. Um so today processes 2.7,000 transactions per second and the only way that we can get to that kind of scale is by parallelizing and we would do the post. >> Okay. So yeah if you agree like we can start with some check uh maybe checking a bit like the the subject and discussing idea. I have put like some notes as a discussion starter but yeah I don't want me to talk only like interactive discussion I have not all of the ideas
so I'm sure that you can review other stuff maybe what I can do is that I can present you briefly like the same check as a reminder then I can show you in how we are doing the same check and how we try to implement for example the univarious kit that is one of the techniques we discussed and so that we can discuss optimization. >> Tom, can you blow up the text a bit, please? >> Sorry. >> Can you blow up the text a bit, please? >> You only have one.
>> Yeah. Oh, but look. >> Oh, >> I think I am. >> Yeah, >> that's perfect. It's good. It's good. >> That's good. >> Yeah. Yeah. So, the same check is like kind of all over the place. We'll try to not focus that much on like wheel because we have other discussion in the coming day we but let us focus on on the
subject that is used both on the p and on we let us forget about we for a moment just on the subject so the prover the prover should accept like the sum of some multi So should about like the sun there or the hue and the goal like of the verifier it to check do some very light check at each round and in an efficient way because as you can see there like a n check will require like two to the power l computation due to this. So this is not feasible and this is not
something that we want. So we what we want is thanks to the trick of the same check is to reduce the verifier work just one simple evaluation at the end and some light check in the middle at each run. And so the goal is just to reduce the verifier word work but it can become kind of easy for the for the prover who has to do all of the e work. Yeah this is like multivaried but isn't multilinear. in our case like it is a multilar >> yeah we focus on multilinear settings so yeah let let us say that the pol the polomial g is like a product
there and we have like kind of this things that is very important to to remind like the small v vs vs vs vs vs vs vs vs vs vs vs vs vs vs vs vs vs vs vs vs large uh large field computation. Why? Because we can we have like at the very beginning like small values from the base field that is square there for example. So this is very small because our field can can be contained to one U32 and so you can easily play with it do operation uh quite cheaply multiplication and stuff. But then for security reason just after the first round like the verifier should um a challenge in the extension field
and this extension field is much larger because it's FP to the power K where we use for example an extension field of order four or five for security and so this create kind of significant performance gap between like different type of operation and between the first round and the other round so in most of the papers from Bad and Hal they they have distinct way of treating operation. They have this SS to distinguish like small base field per base field operation. SF to distinguish base field per extensive operation. That's this one is very fast. This one is fast and the large one
LL so large operation multiply by large operation and it's very slow. If you want to put numbers on that like if the degrees is K, SS is like O one, SL is K and LL is K square. >> This is roughly guess. So like when K is four, it's like 1 16 >> and so yeah this is what just I just mentioned from like the work the round two and onwards is dominated by slow L multiplication and so the key optimization almost all of the tricks they say that differently in different way but the key optimization is to rearrange the computation to minimize this LL operation by doing more work at
first and so be able to work in this cheaper detail. So let us work first in the universe skip because this is the one that we know the most. So this is a technique to skip a bunch of round from the the first one. So the motivation is quite simple. Can we do more work in the basic to reduce the number of extension operation we need to do later? The solution for that is to reorganize the do.
So by reorganizing this doain we can restructure and replace the K variable with a single variable that so at the beginning like you have this multi very big multiar polar that you see. So you really interpret simply this big like g pol that is g as a function of x0 x l minus one and you reinterpret that as a function of big x and then x k x lus one. So as you can see a lot of
variables there just disappear and are replaced by the big x here and with x is in this multiplicative of group D. That is the way we can skip K round. And so K here can be a constant that is fixed in the code. For example, you can skip three round, five round, seven round. And so the prover should compute a single unar poling over the remaining L minus K variables. This is what we just mentioned there.
And here vx is a uni and it can be defined in a manageable number of of evaluation and the prover does send this polomial to the verifier. In the classical sitting like the vx that is unarant is of order two but there if we skip k it can be like higher order but we have use function in3 to interpolate this and so we can play with this and so if I if I show you with code maybe So
basically what I have here is that I we have in this subject module where inside this file you have all of the computation of the subject containing both the univarial setting and the nonunarial setting and so you can run one by one in this In the other field uh in the other file this one we have like the computation of this specific skipping technique. At the beginning we have as enter like two matrices that are like the f matrices and the weight matrices because if you just recall at the beginning of this file we just said that uh what we
want is a product of uh two polomials. And so In our case the two polinomials are represented by f and way. So in the first um in in in the first place what you do is that you rearrange your matrix to view your polomial differently. So if you recall correctly like you like you you view your polomial completely differently by replacing the first variables of the multilinear settings into one variable. This is what we do there. And after that, we just apply an LTE that is doing the
computation for you. And at the end, we just compute the results that we we expected and we just return the result to the reorganized f and y matrices. Then why why does it impact all of the code? And I This is the important stuff to learn is that if we check the optimization technique there for example like all of these are randomness challenges sent by the verifier
and in the classical settings like you have like air0 that is during the first round then you have air1 then you have air2 and etc etc. But for example if we want to and so then the when you have like the construction in the on the prover side and on the verifier side the verifier can can run by run and check for example this randomness and then this randomness and then this randomness. But when we are in the univar settings if for example we chose to to skip two rounds let us this to one then this will be replaced by uh let us say a and then directly two. So
for these two skipped run like the prover the verifier will just issue run one single randomness and so then when the verifier will want to to extract L0 and then L1 it will not be possible because we will just one. >> So >> yeah, >> the R1 to R IUS one in the equation there kind of like instance all sent in the same round by the verifier. >> Yeah. Yeah. Just one. If for example if you if you have like um in in the classical setting you have a run by step at each round you reduce the polomial.
So you replace uh the the previous x variable by the randomness sent by the verifier during the previous round. So during the first round you issue one randomness. During the second round one another but if you skip n terms you don't issue n randomness. You issue one for all of the skip run. And so then it induce a bunch of reorganization all over the code because when you do like run by run stuff inside the verifier for example at the first run the verifier we want to extract this one and at the second this one then you have kind of out of bound
stuff because you will have just one for the two sch. So this induced like a a world reorganization of how both the prover and the verifier sees the polomials and so change at least for the PCS all over the code. But for the PIP I guess can talk better than me about this but you have just the same check and no not this notion of like constraints for the for the verifier and the prover. So that this is much simpler to handle this case because you have just the same check and the verifier of the sun check and so you can just deal
with the sun check but in the PCS side of things you deal with some check randomness all over the place in in all of the code >> yeah how much of the total time is spent on some checks like do we know that >> uh I don't remember but a lot like a lot because we have decoupled that in different rounds but >> I don't know maybe >> okay >> yeah more than 25% is >> that's on wheel not on >> yeah yeah just on the whole system apart from FFT and
the tree in everything is check so yeah >> and do of security by having this batching this very >> in this case I think that can answer better but no >> I I think very slightly so so I mean like so so the the bit security comes from the degree of the polomial I think so when you do the univariate skip you do lose a couple of bits of security but it's not it's like five or something >> it's not a big number >> I think There's one thing I want to add um because the so as to mention there are two as I understand two two different
optimization skip and the background >> and one thing I want to add is that the so the back thing is led by Justin I think >> it's aation and those have been designed for some check with a product of premium. But in the POP when you want to use some check to prove validity of air constraints, you will end up with an arithmetic circuit inside your check. You can always forance if you want to prove poss and you can always develop it to get a
sum of product. But if you do it will have a very very big like hundreds of terms due to the poson constraints that that are developed. So you to to get efficiency you need to keep it as an arithmetic circuit like factorized way and if it's an arithmetic circuit I don't know how to apply the bag optimizations and that's why I only know how to apply the unarant skip on this is pretty straightforward but applying the other tricks where we de compos after compressing the de composite
And so it's for me it's I don't know honestly how to do it. Maybe it's posible but I don't know >> that that's why I think that the bag optimization was designed I think purpose bit for spartan and jol because they mentioned a lot of spartan in the paper the thing is that on the pcs side of thing as you can see in the documentation of this function the goal that we have when we enter this in various keep optimization is to run the subject over the sum of product of two function fx and W XB so two much linear function this is what we are represented by the two argument of the function right there. So my point is that maybe
we should apply different optimization for the two maybe as you just mentioned like the universe keep is perfect for the POP but is not perfect for the PCS and then maybe the optimization is better for the PCS. The only thing that I know is that due to the way they end we cannot combine the optimization. For example, you cannot use like unk plus back in you have to choose.
I think that lambda cast worked a bit on that. So maybe they have things to have. I think that also you raised a point recently Emil that maybe could be discussed with Angus is that I think that you apply the universe keep in a different way that we do due to the choose of the yeah the set D as I just mentioned there you got like this notion of a multiplicative subgroup D in which like you you view your polomial differently in such a way that in the real setting if you apply due to the LDE things that we are doing and the fact that we use a
multiplicative subgroup if you apply the same check with K equal one. So virtually you you would end up with same number of like randomness. So technically this is the same as not doing any any skip but in our case like the result is a bit different from the classical subject. And I think that in your case you end up with the same result as if you do the classical instead of because you have to choose D or size. If K is the number of runs that you skip, the size of D must be to the power of K.
>> And the prover will have to perform a bunch of FFT on. And so in this right? >> Yeah. F. >> Yes, exactly. And you would say taked a multiplicative subgroup. So FFT is fast. Perfect. And this is like the natural idea. But I would argue that what another is to take for D the set zero 1 2 3 until the power of K minus one. The cons is that the FFT is not free but in practice FFT on a small set you do it with complexity it's if K
equals 5 it's anyway but the advantage is that when you take K equals one you end up on the classical check and so it's like personally I think it's a better generalization of the sun because for instance you have one implementation and if you want to do normal subject you simply use K equivalent and so it simplifies but the drawback is that the the FFT are not like it's not FFT friendly but if it's if K is smart in practice is the case I would say it's broken makes sense yeah I think I picked them all sub just because it makes like the
math easy basically but it's yeah you can pick any subgroup with the right size it just Yeah. Okay. And I I wanted also to discuss like uh I I think that you guys worked on the bag implementation a bit. >> Yeah. >> Like maybe you have some words to add. You think this is like half time to implement it. It is okay. It is performance. Okay.
>> No, it's it's going well. We we had like some some things to make it compatible with uh the one used in 23 because we were like um choosing the variables in in a different mdms. So I think in one case you started with XN and we were starting with X0 or >> the other way around. I think that in in the case of the POP since you are using air maybe the univer keep offers like some advantages because you are like combining a lot of polomials and they are not uh the product of uh multinas but uh a bit more complex besides I think you can save a little bit on the
proof by just not sending all the zeros because essentially if you're using the zero check you know so that all the terms will be zero. So you can like uh have the the verifier fill by himself all all the zeros. Now for the PCS maybe it makes sense because there you have already the product of two multilinears and maybe with bagat you can go a bit faster. Of course I don't know perhaps span has some advantages.
Uh I've been thinking a bit about um Spartan and and the multi-air you can transform from one to the other. Um the advantage is that in Spartan you don't need to sample u random challenges to combine the constraints and if it has like a very nice shape then um evaluating like the the matrices at random points might be rather easy. Um and besides I think you can handle sparity bit better than than in the case of air but We are still looking a bit at it. So
>> if I am correct I just rec this with with a small example. If I am correct about like the bag implementation like you have for example two polomials P1 and P2 that are multi-linear and then you have this uh this sum in the classical setting like due to the air that is the first randomness issue by the verifier like you have the product of two polomials that are large. So this is a LL computation and so you decompose using like like that with some coefficient a that you can premp compute offline before applying that to the end and so you just compute your a offline
everything is in small field so this is like a cheap operation that let's say so you comput all your coefficients and then you just do online this computation after that so this just end up with SL SL instead of everything large >> if I remember correct. >> Yeah. Yeah. >> Just like that. >> Okay. So yeah. Okay. So two kind of implementation but as you are think like both are related to the same thing with doing as much work as we can with the base field and then later with the extension field. I I think like one thing that makes this a bit like no not
this but generally these optimizations a bit harder in this case is that I think when we look at the two morning linear so if you go to so in word two linears and even the very first case one of the morning lineers lies in the base field which is great but the other one still lies in the extension field and so I think they're like sort of I think a lot of these methods like do very well when you have like all yours in the base field but when one of them sits in the extension field all of a sudden you sort of pick up more overhead just Because naturally like univers anything beneficial if everything's in the extension field the bag depth is isn't either.
>> Yes. Yeah. What you just mentioned is yeah very true for wheel because like as you can just see here we have like the two polomials that are represented by matrix. One is in is in the base field but the other one is the extension field. So it makes all of the operation even more complex to optimize. Could it be possible to I'm sorry. Could it be possible to um find a polomial with coefficients in the base field representing the polomial with coefficients in bigger field?
>> What am I representing here? Since you you're talking about the case in which one polomial was easy and the other one had like bigger coefficients like I don't know maybe mapping the complicated pol simple one >> then taking up on that I don't know but if you do that will your like the new polomial be larger and end up with almost the same cost to the fact that it is larger. I don't know code but um you know since field elements can be represented as couples
>> of base elements >> I don't know >> playing with sparsity maybe if if you know that it's multilinear then >> I don't know good idea Okay. Um I know also that you have played a bit like with the ND because like right now in in we like we we fall from like the classical and so this is very difficult to apply packing inside the the sun. Uh I I don't know like where exactly you plan to
adding in there but I guess in the in the compression function um actually um we could almost everywhere every time in where you have a vector containing extension elements you could have instead a vector containing packet extension elements. So you locally you transpose it to speed up to speed up with simpification and for instance the weights. So initially the are the base so packing is free because it's free and the weights are in
the extension field >> but instead what you can do is you take weight in the pack extension field. So the representation is slightly different locally it's it's like it chang but anyway and but to make it work because currently we start by folding the last variables like x x1 x2 it start by folding on xn but xn um it's uh which means that currently to fold you you take every um um extension field elements at an even location. You you and you fold with the elements at the
odd location and so by by pairs of two and you you you multiply them and you but the issue is that um when it's packet uh you cannot do this because locally you have you have modified it in a packet way. So what you should do is that um if you fold starting by the X1 by the left folding is simply taking the first half and multiply and add with the right part and this is piping friendly and uh in the end I think every time in the code where there is like a vector of extension field we could replace it with
a vector of packet extension field and almost except at the end when it's smaller than the packing width you need to split it in a normal way but at least in the beginning when it's expensive you can have packing almost everywhere I >> how does the packing works >> um so yeah so so roughly um when we're saying packing here we just mean that if you have like a single field element but you want to do like a bunch of additions. It's easier as opposed to having like one U32 to pack in your SIMD operations. Um, so you want to add like eight field elements, you can sort of pack ah
>> eight U32s into like a 256 bit thing and then do that. Um, and then the issue with extension fields is that like if you want to do like if you want to multiply two extension field elements, it doesn't really make sense to sort of pack extension field elements into individual SIMD uh registers. So let's say you have an extension of degree 8 then in theory you could pack an your your whole extension field into one of these mm26 vectors and then and then addition would be great but multiplication would be a complete nightmare because you simply doesn't really work well when you want to mix everything. So what we tried to do in in 43 was basically um thinking about like an out you can think about like packed field elements as sort of like an an
algebra over the field um just because if you can imagine you have like a cd pack vector you can still multiply that by like a single field element and everything goes well and so you can imagine then doing like trying to do like an algebra over the extension field where now uh each of your elements of your algebra is basically a sim packed field element and and you You can think of this as like eight extension field elements sort of squashed together where you where you've joined everything which has of like the same coefficient and then this now has sort of fast then now multiplication is nice because like you can do if you have like 80 80 cent elements and another 80 cent fill elements you want to multiply them you can do all the multiplications and all the addition sim and so that's faster the cost is that
it's prohibitively annoying and expensive to transfer in and out of this form because you sort of have to do these like transposes >> and in our case in I think we can keep 100% of them in this form. Yeah. Yeah. Never come back to the normal form. >> Yeah. Yeah. That's ideal. Yeah. So if you can stick everything in extension in this packed form and leave it there forever it's ideal but otherwise >> Yeah. Is that making sense? Or I can write things down. >> Maybe can we just an example of >> operation that will be like This is for I think a problem is this is okay for you to
a problem with that is maybe more special GPU program uh when you want to do operation you want to have all the R together all the G together all the uh uh B together even though the individual pixel is LGB but for Cindy it's better to have all the red etc. in column channels and basically that's what we're doing uh while packing uh extension fields. >> Yeah. Yeah, that's exactly right. Yeah. Sorry. Should I write things down or does everyone have >> Yeah.
>> Okay. So, so what's the what's the base thing? So, let's take a field. Uh so, you can pick pick some field and then we just I'm just going to look at like an extension of degree two. So, like I don't know F joint gamma where gamma squ is seven or something. If that's not I mean let's assume this works. Um so what what does modulation of the field look like? Well that's easy right? You know sort of you know x * y and then you just have basically have to reduce mod f. And the question is well what happens if you want to do so what if we want to do a lotations.
So up here right you can sort of think about each of these internally in our computer is going to sit as a U32 and this will be another 32 I'm saying uk but like it's a 32-bit integer integer and this also be a 32-bit integer. So basically if you want to do a single multiplication you just use scala code scal but the question is if you want to do a lot of these it makes sense to do this to do sim operations because it means in a single cycle as opposed to doing like one ad, you could essentially do like eight ads or in a in ax or four in neon or 12 16 in ax 12. And so the way if you want to do like um if you want to do lots of moles is you sort of imagine you
pack you get sort of like a vector x which is going to be a packed. So this is like like sort of packs I copies of X I field elements. And now you can do sort of Xar time Y bar * Y. Am I this way too small? Sorry. Okay.
Yeah. Sorry. So I can I can also try bigger. So what are we trying to do? So the point is that if you want to do like let's say a so I here um this be one off by one errors. Um so so so now we can use some the point is that we get to do sort of um eight moles uh sorry for cost of of basically basically one. So on ax2 basically we can do eight miles on the cost of one and if you look at like throughput numbers it is literally
like an eight times improvement. I think it's actually even a bit better than that for weird reasons. But um but like you basically just you get like a eight times speed up because you just can do all all all your operations at once. Um and so the question is how do you what do you do when we want to do sort of uh how would you do extension field multiplication like this? And so so what does extension field multiplication look like? So now an element so in in this f a joint gamma what do elements look like? Elements now look like a + b gamma right and the way that multiplication works if we do a + b gamma time c + d gamma. So we just give us
we'll get and here here we just go gamma and we're saying gamma squ= 7 to pick a number. So then this multiplication is going to equal a c + 7 bd plus uh a d uh plus bc. >> Okay. So this is this is how like a single extension field multiplication works. And the question is well how can we get the same speed up that we got for the base field operations for the extension field operations. And so the the nice case is if you're just doing things if you're only doing additions then actually everything then additions work quite nicely because you like
addition sort of just you know the A and the C are together the B and the D together you don't have to do anything cross stuff but when you don't want to do multiplications all of a sudden you have this sort of annoying issue which is that if like if A and B are packed into the same vector um SIMD doesn't work well with doing multiplication sort of across lanes it wants everything to in the lane. And so the ide gamma is basically what we're going to do is we're going to think about the algebra where now our elements look like a vector plus b vector gamma where here a vector b vector are exactly these packed field elements I talked about
earlier. And so now we can do basically so now you should think of this this is like this this kind of contains this is like eight uh f gamma elements packed together. Um okay, does that sort of make sense? >> Yeah. >> Okay. And so now so this is this is nice for doing the operations but the annoying thing is getting things into and out of this form because if you imagine how how these things look like in in your computer if you have sort of eight like f gather elements.
So what does this look like? Well this looks going to look like a b a1 b1 right? So generally like this will be stored in this sort of format. Whereas Now if you want to look at our our packed field gamma, this now is going to be stored in a1 dot b1. And so you could think about this thing is this is exactly like um we have an array of of field elements of length two of length eight.
Whereas this thing is more naturally thought of as an array of field elements of length eight of length two. So like the difference here is literally like this is it's literally just a transpose. So what it means is when you want to convert into and out of this pack field format you have to like go through and do these individual transposes which is painful. Um but basically what it means is that if you want to work with pack field extensions wherever possible you want to put everything into pack form do as much as you can and then convert out whereas the sort of opposite case is if you're just doing with operations the
like if one of if this is a one obviously all of a sudden the transpose is free because you're not doing anything and so when you're just working with the base field you can convert in and out of pack form very smoothly I think that's where Pompy 3 works best but then when you get to extension field just by nature of having this transpose causes sort of problems and slows you down. >> Yeah. Just want to add some parallel to other engineering disciplines. >> Yeah. >> So um I mentioned this is used in video games and graphics programming. Uh I'll take an example of uh pixel. So let's say you have four pixel. You can store them as RGB V R G B R GB very GB. But uh this is similar to storing
them now in R r g b and now you can use cd gp programming etc to do acceleration and uh this is called um data oriented design which is uh focusing on data layout for acceleration and this This is also called uh you can also look for SOA for strct uh of uh arrays and this is stored in arrays of strct.
So each point is array or strip and now you change it to str and this is how um when you do any video encoder uh you get all those cd acceleration over multiple pixels because if you store it like that it's just too slow you I may have maybe like two question for like both of you. Um with the experiment, do you know what is
recommended in term of number of rounds that we should keep and number of rounds that we should apply the bucket optimization? Is there like a tradeoff? Is there some simple rules or is it just with experimentation that we can find the better tradeoff. I seen I think that being used for using seven skip something like that. Do you know if more is the best or >> I I would just recommend putting as a parameter of trying out I think this precise number for the univer thing is going to depend on on sort of your exact use case.
Do you know inively it should be number of runs skipped should be the logarithm of the extension approximately I think in news they skip like something seven because I use extension two to the power seven but in our case I think currently like it's three and but if you use four it would not change a lot if you I would sayively that as long as you use more than the logarithm or the extension degree it will not impact a lot performance but it will improve increase sorry proof size because you have to transmit a longer
>> yeah I think of the increased proof size is the bigger drawback in some sense of like um because I think somehow like every time you do an extra round I think somehow like each extra round you add should still give you a small performance boost but it's less and less of a performance boost and every time you add a round you increase the size. So you can consider like the really stupid thing where you just skip all the rounds of univer skip >> and from the proven this is ideal. This is like really fast. And then the verifier gets given a like degree to the 20 polinomial and told to evaluate >> which makes it very um yeah but I think in principle you can like you can skip all the as many rounds as you want but it yeah the proof size
is sort of the thing that that cost >> I get this is the same >> no for for the other optimization um I think proposes a quotient of logarithms >> okay >> based on the number of factors that you have >> and also So that there's a factor called kappa which is measures >> how much you take to perform an um multiplication versus how much it takes to perform an SS multiplication. So it takes the quotient throws that hea into this uh California and ends up with an L0 that's between three and four in most cases when they combine that optimization with the uh polomials with EQ as a factor.
>> Yeah. >> Uh it's it's usually shorter. >> You end up with one round less. >> Okay. >> Because the comparison is now between the LL and the SL. >> Okay. Yeah. >> So few >> so for the univer that this is already implemented here. um like what are the I mean I know it's broken that's what I was about to get to but like aside from the fact that it's broken like what else um is there still to do like okay like for example the type field elements for the extension field >> and what else
>> I get then we need to design like a single one and integrate that into three >> that would be my next question like uh I guess that the best that we could do is to have like a single one at least a sing single implementation that should be used both for wheel and for the POP so that when we do for example one optimization it has a benefits for both and then we multiply the benefits um my question is that how do you see that in two I imagine as a separate trades I imagine also that it has maintenance work >> yeah of course >> I mean I think so there's I think
currently two issues with the univer skip in word which one of which is it's broken it doesn't work >> and the second like I think somehow equally important one is it doesn't speed up compared to >> B I think that the subject the subject implementation the subject alone is okay >> I think that the problem is not in the subject the problem is as I just mentioned before that it modifies everything in the view and so I try to spend a bit of time toward this but not that much because I I felt that it complexifies everything >> and so I had in my mind that maybe for the PC this wasn't the best solution as well. So yeah, but yeah, in PL3 like probably we would have
like a general like some check that would fit with zero check of the the P with our case for the PCS maybe with some backing optimization maybe with the back optimization maybe with the universally yeah I haven't thought about this super in detail but I think something that I think would make sense. So I think both bagget and the univer skip it. Honestly, I think almost all of the optimizations for subject subject I've seen are all focused around the early rounds, right?
Like the fact that you do something different and then at some point it turns into sort of a generic sum check. >> But it does seem like probably the most sensible thing to do is like have the generic sum check in and then because because I think the initial couple of rounds are also going to depend massively on what does it look what are your input polinomials look like. So, so zero check is like you know oh my my input polom is always zero so I can do some sort of tricks in the first few rounds like like most of the and similarly for were right for for your input polomial you know it's going to be a product of two things and so there might be like tricks you can do just because you know it's going to be a product of two things in the first few
rounds before it has to be converted to like a generic >> so in3 you see more like the generic implementation and then we handle all of the optimization on our side on different this is what you you mentioned or >> I I would say that like the generic one seems like the thing that can get more easily added earlier because the because I mean the question is like you know we don't want to necessarily have like you know the universe if you've got two if you have two polinomials the universe if you have three pol at some point I think it's handy for people to like take what we have and then write you know write what their first round is going to look like and then they can hand it off the sort of I think that if we had all of the optimization from this require like a
lot of experience from the user be able to choose like the correct number of round to keep the correct optimization. >> Yeah, >> a lot of things like that should be handled by the users. >> Sorry, just question. I got a bit lost. So you said that the university is not getting messed up, right? currently currently >> we we need to in because when I think it back I think that we may have a problem in the way that the prover see the polomials and so we are doing much more work than we require in the university because Angus we can discuss that separately because
>> I think that when we when we commit initially like in the leaves of of the mer tree we should change the the the way we see the polomial due to the universe keep. So maybe we need less leaves. >> Yeah. >> And so right now maybe the broken things is that we have too many leaves plus the universe keep and so maybe the prover sees the the polar much bigger than it is. So I'm not sure about the fact that it doesn't speed up. Let us unbroken and then we'll be able to >> Yeah. I think there's been a bunch of things where I've looked and we're like there's probably places can be sped up, but we should try and
>> we should try have it running before we try and speed it up because >> we don't want to I think I think we've actually doing the opposite right now of like doing things that make it slightly slower and trying to make it more simple to try and fix it. >> Yeah. The problem is that we thought that this was okay but it was wrong because in the test we use like a constant polomial with a constant coefficient everywhere. So I thought for a couple of weeks that it was okay and then I I don't know why I just sent you a random pol just to be sure and then I answered. >> So yeah, yeah, I think there's also reasons to expect to get less of a benefit here from the universe compared to cases where your initial thing is entirely in
the base field just because sort of half of the polomial is still in the extension field. So you're getting some benefit but it's sort of it's not as clear. this is like a product. My suspicion is also that yeah I think stepping back to what I mentioned before is that probably somehow yeah that the initial round probably the way to get this fast is to try and like work out how to make initial round optimized and just look in the specific case of like what are the pol that are coming in and then and then have the later rounds handled by the subject. I get that also your optimization the fact that to to to be able to use tracking then we need to be organized like the folding way >> so I guess this requ
of history >> yes indeed modify >> so I think that this will have like another parameter in the history to be able to say to the GST either you want to do the DST in one order or in another so that we are able to >> I I think I know what you mean but I probably at some point >> in fact this will require more or less like a boo >> to tell to the GF if you want to go to one order or to the other >> so that we can fold in the specific order that is of interest for us in order to be able to apply the packing. I think you're saying that like the the FF the way FFK works doesn't super nicely
work with pack extension fields >> because beforeation we were using the small batch DFT for3 but simply the twers were slightly modified to do the FFT on the evaluations. >> Oh yes yes so first and then to be able to use this pattern optimization I had to modify the DFT because um currently the DFT. Okay. Instead of for instance beginning for the butterfly in the large butterflies the small butterflies I think now what
they did is like small too large maybe it's related to like the distillation in frequency dist something like that >> is the point that like you don't like butterflies that are within packings are a nightmare so you want to like avoid doing those but but uh I made it work with packing It worked fast. It's as fast as the previous DFT, but even faster because in the previous DFT at the end of the butterflies and so on, there there was um a bit um like when you transpose with the bits which is quite expensive because it's not nice with memory locality. And uh with this new representation,
this removes this index fling at the cost at a small cost but in the end the game which is that before applying the FFT previously we have to take our evaluations and to duplicate it to this is like the rate of the element. If you want rate of half, you simply double the evolations. Then you apply the FFT on the whole thing. And now what we do is that um uh instead of doing this, I just repeat locally every value. So instead of this IVP like this and and so this is a bit more costly but
the fact that we guide we have got the bit it's more interesting this new >> yeah that makes sense >> yeah so that is a point that we should discuss to integrate that but one last point I think that could be interesting in the context of check is about like the way that we discussed before. So yeah, just to remind everyone like in order to integrate our test into like promis3, we need to have an agreement on the fam. So right now if you look at that is in we have like a pro state inside the pro state. So we have a bunch of stuff but we have this proof data that is a back of field elements. So we can represent
this as like a big vector and each time the prover does something just uh inject some stuff into like the pia vector. For example, if you look at uh when the in the subject so at each round when the prover wants to send the univariate polomials that he have to compute to the verifier it just send the variation of them for the verifier to be able to reconstru like the given polinomial. So that is just here add extension character
and so basically what it does is just just add some elements to this to this vector. like say x1, x2, x3 and so on and then this is passed to the verifier and then the verifier is able to extract like the required thing. So for example if we spoke about like the three evaluation of the polomials that are this three evaluation then as the vector is passed to the verifier then the verifier will be able to catch this one and return the ver the the polomial.
So that is just kind of a streaming fashion to um to send information from the prover to the verifier. So the prover can push information the and the verifier pull this information in the same order. It has the benefit of not having like a pro structure because in in PL3 this is done a bit differently because you have kind of the same stuff inside the states of the tam just to generate randomness. So that it it is absorbed by the mean 23. All of this is hash together and then you can extract some randomness. But in our case this is used
both for this purpose of extracting new randomness but also for the purpose of exchanging information between the prover and the verifier. Whereas I think that in history what you just do is at the end you have like a big prover and inside this truck uh you store all of the information and you pass this structure to to the verifier and then the verifier just catch information by information inside this. >> Yeah, I think that the benefit of this is that first we don't have the structure. So yeah >> and then >> I think the claim be at least from the
tree side the structure is makes it a little bit easier to construct the proof and like separate things out as opposed to just having a giant vector >> where yeah doing that >> doing this way has the benefits of clear view clear mental model when you code everything >> you can even debug easier like to check the different field of the structure have a mental model of what is passed between the rather than here you just have like a big vector of elements and you don't know anything but it has the benefit that we as we catch the elements in the same order we cannot make any mistake as I say any security flows or anything because
if you have like um if you have like one one element inside I I will call it XM it's malicious then the the verifier is not able to con because the wrong information. >> So yeah, but yeah, but I think that that's truly the case because that like as long I guess in three as long as you're like the main trick is whenever you add to prove a data you also you also have to add to challenger, right? Like you also have to like update the challenger. >> That's sort of the key and I think that that >> I think that what is difficult there as we just discussed during the break is that if you want to make it generic there we just care about like post and stuff. So you can just store f element there. But if you want to make generic
and be able to use that with sketching >> then you cannot put f there because it does not correspond to anything compatible with sketch. >> Yeah. And so you have to put UA there or something generic and then having kind of serialization trait that is able to serialize data when it enters like the true data and deserialize data when it goes out out of the out of this data to to be able to be reconstructed. So I guess this has also this blowback.
>> Yeah. But yeah, I think this is something that we should uh discuss and have an agreement on because I think that this will block the integration of the check inside the history because we use the >> Yeah. Yeah. I think probably I mean I mean we can do do offline here. Um but we can I think um uh we should just stare at what we do in pocket 3 for like what does fry proof look like? I think we have a struct called fried proof and you could easily have another strct here called like word proof which is like what that what what that section of proof looks and the I mean so the advantage of having something like that it just means that when you go for a proof that has a bunch of different
features you can like sort of just send hey this is a proof of the fry bit this is a proof of the word bit um >> I guess this will also require like some modification on your hand because I think that in the VM >> you use the same And it's it's very everywhere. So I guess it's very useful to simply when the program wants to send just I have send information and it's done and because I believe um it it drastically reduces the risk of not not um hashing like not updating the state before
sending information and believe that most of the in practice critical bugs comes from this flow. >> Yeah, that makes sense. >> Yeah. >> Um in practice at least in our code base there's been quite a few. >> Yes. >> Yeah. >> Yes. >> So yeah, you say that we should modify our this is not a problem. I we should just adapt and open an issue and someone has to invent that. But >> yeah, I'm just trying to think of how hard it will be to retrofit. I think that no I think I I do like the idea of like having the challenge. So and I think the key thing that this struck does is has has the challenger as part of the strct so that it just sort of automatically whenever you add things to
the strct. >> Yeah. >> When you when you say that you had for example one scalar or one field element this function. So this just had some elements inside the data >> and also the challenger inest this. I guess the question is that is it valuable to have the details of the fried proof will somebody need at some point to easily access I don't know the the second mer if it's not the case we I I would say a long vector of feed elements is enough for proof but if someone needs to access the details of the proof indeed it's not very
convenient with this system >> I I think this also comes back to I that kind of Thomas made about what happens when you someone says, "Oh, I want to use catch not." Um, so I mean maybe one if you want to uh if you want to switch to a slightly different I think a decent thing to look at is what does the Poppy 3 uh fried proof strct of like what is now fried proof because I think this is like the sort of this is the equivalent of the work of of what what's in it currently. Yeah. So we go to 23 and then I think that we should be able to retrofit this to like roughly do what you guys you want. But my suspicion is that we might go both ways of update our thing to do what you want then also maybe update your thing to sort of
match. But like roughly but basically like you could imagine that like there could easily be a function that takes these four things and just turns it into the vector that you have. It's just basically just saying we're just all we do is separate se separate out like the commitments the query proves the final product and the witness and then the other advantages here is that like this allows us to sort of you know you if you put in what uh like binding function you use right you'll get different commitments and so this just already works as like catcher emphasis item um but I think that like this sort of structure should also work fine for work I think and then you should you should be able to like like You should there should be it should be possible to write
a function that takes this strct and outputs just like maybe two vectors because I guess you have some field the elements and some non field elements but that should be doable for work as well I think but then I also agree that like you could easily add into this like a challenger and then update it. So when you add things automatically. >> Yeah. >> If you think about this, this will also make us closer to the integration because we could remove the folder inside. Right. >> I think I think you have you have a word proof >> once we have a word proof we can remove the folder in we and just just call it personally. It makes the de the
development easier with this approach because you don't have to customize the the structure the proof the proof I guess for instance have to do this you need >> on fry obviously the proof is pretty simple but when it's quite complicated like the full proof system of a VM there will be a tons of fields in the struct and it's clear like we can do it but honestly it's a good question. I I don't know how the the when you have like a complicated >> yeah what does the truth look like? Is
it a big rust structure or is it like a continuous vector of >> it's a big strct? >> It's a big strct. Okay. >> Yeah. My suspicion is it's a big strct because doing a gigantic vector of like bytes is sort of nightmarish to like >> what do you do with that? You deserialize it instruct and then verify it. >> Yeah. Yeah. >> But this is not exact not exactly what we do because we derialize when we need we don't deserialize at the beginning make the strike. >> I mean so we can like like fry proof support serialization. So so we can always send this to you as a set of bytes if that's what we want. The question is what why would you is that like if that's going to be easier for
your proof system that's saying like you can you can get this as a set of bytes >> you want to custom step >> uh no I think the serization is it just turns I mean so no I think serialization just turns the elements into bytes and then the commitment into bytes in just sort of the obvious way. So like like this isn't like you can write this as you can get this entry as a vector of bytes. It just is going to be a horrifying bytes. Why do you need a selection of files? >> Because in terms of security, >> you cannot make mistake on if you use a script where the challenger and the vector is at the same place.
>> For now, we don't use by because we we are just using coded. >> Okay. >> And so we just push field element by field element. No. But if we do if we want to do general settings and include that into block history and be compatible with ketchup then we need to find a common format of sterilization derilization when we push that >> I think where you could make a mistake with the theatir if you just have a sequence of bytes is if you didn't sequence your bites in just the right way that corresponds with the order of interactions and the interactive protocol. Yeah. And so and it's quite easy to make mistakes if you and it's
likely that they have been that I think six months there was a critical vulnerability because the ordering was not maybe I think it was the a tree was not committed to something like this. Sure. And so you can make mistakes and mistakes are impossible. >> No. So but my saying is but the I think the the key design feature that's making those mistakes impossible is is having the challenger in the f in the proof structure. Okay. >> It's it's not having the proof structure only be only be a vector of >> so you would suggest to have a structure with different fields and at the same time the challenger.
>> Exactly. >> So I'm saying I'm saying we should update fried food to have the challenger and the fried fruit and have whenever you want to add something to it like Yeah. >> Okay. I see. >> Um, >> yeah, the mutable reference to reference to >> Yeah. Yeah. >> You have a mistakes and you have the regularity of of the proof. >> Yeah. Yeah. I think Yeah. So, we have to look at how easy that is to do. I expect one of the hard thing here is that like these get built at different parts of the protocol, but but I think that should be doable. But I think that that's the that's the thing that I think makes sense and reduces mistakes. I think the STR thing is also going to reduce it's just going to save you years of coding time just because like if you
just only use vectors it's going to be it's just going to be complicated but actually I I like to develop this uh this abstraction of I send the feed elements I receive elements I sample events it's only this and it makes it's quite simple and because otherwise I would have to vector add then challenger observe And so again a line every time any special >> so this is kind of yeah this when you have a you don't really know where it's come like for example if you in your case when you have like the vector if you do get and you don't receive the proper vector then debugging is actually
the way I debug I I print to find the moment the The key is to find at which point punch the code of the verifier diverges. So you simply print the internal state of H and you can find the line at which disagree and it's obvious. Yes. And it's okay. Not that easy. >> Okay. So yeah, I think that we can go for lunch.
>> Yeah, lunch is next door. a thump he's made. I don't have a