Minimal zkVM for Lean Ethereum

Transcript

Sorry. Some of the windows That's the best week.

I need to slide. Okay.

So here I'm going to present to you um the basic idea of this minual machine that that we are training to build in order to aggregate those XMSS signatures. So first as explained the goal is to be able to aggregate XMs signatures and second to be able to aggregate those already aggregated signatures. So to have recursion in them and to do so um there there are a lot of good ideas that we can take from KO and here the thesis will be to limit as much as possible the use of pre-ompiles in order to keep it

as simple as possible. to give you brief overview of the of a current potential idea of how such a VM could be implemented. Um here here is a proposal where you have one read only memory as in kro two registers frame pointer and program counter the difference with ko is that you don't have the AP the allocation pointer register and I will explain later how to do it like how to make it work without this register without this register and so you have uh one memory which is committed you can see as like a big chunk of field elements in the the base

field and you have a B by code and each cycle you execute one instruction that will um read and like fetch some elements in memory assert some equality like add and M constraints between the elements in memory and you can also have GS and the reference as I will explain next. There are four basic instructions like it's it has be it has been designed to be as simple as possible here. So as explained you can add and multiply elements in memory but the index memory that you access are

relative to FP. So FP is the frame pointer. It points to the start of the current stack or the current frame in memory that that you are located at and you can also multiply obviously feed elements. There is this reference op code that allows you to as its name suggests the reference some kind of pointer and this would be useful to access um elements in memory that are not in the current frame. We'll see later what why it's necessary. And finally, a conditional jump, which basically let you jump at a different

location in the bite code based on some condition. And when you jump, you can update the you can update or not the frame point because the two operations we are trying to verify firsts aggregation and second region heavily relies on hashes. We will naturally need some pre-ompiles and obviously two posiles over like the posutation over 16 and respectively over 24 ft elements and there are also two more preo compiles that have been um found useful when implementing the we recussion

algorithm. But this is like just a detail more importantly can focus on those that basic basically let you perform possilinear world. Everything is a multilinear polomial. The field has explained is collab and the extension degree can if you accept the conjecture up to capacity you can get close to 128 bits

of security with uh with some grinding some grinding sorry and an extension degree of five. it works and um so the PCS is weird and you you replace like everything uh every almost all the um machinery in the in the uh in the IOP is based on some checks. So for instance to prove errors you don't use the question the traditional questioning technique you use a some check like a zero check to prove the validity of your air tables and using this check based approach approach you

also um avoid to commit to the to the quotient polinomial so you can gain a bit in term of commitment so with some check you can prove validity of those different tables Basically there is one table for execution like this is where most like every cycle um in the execution of the VM corresponds to one row of this air table and then you have some tables for the pre-ompiles and then you have your memory here not everything is committed the memory is committed except for the public memory which is the part on which prover and verifier agree It's the part

of memory which is useful to pass like the arguments to the program you are trying to verify. For instance, in our case the um message and the public keys of the uh sign of the XMSS signatures and you prove the consistency using two thing. First a look up for instance in the execution table. We have a closer look later but some columns are in yellow are not committed thanks to log star which is a recent index lookup

which allows you to only for instance here this indexes column are index that will point to memory. For instance, if the index is four here, it means that the um fifth element in memory should be stored at the corresponding value here. But traditionally what you would do is that you commit to the index, you commit to the table which is being accessed and you also commit to the resulting data.

But with star you can skip this commitment and those column those columns become virtual column when it comes to the lookup from the execution table into the memory. You will not gain a lot. Actually in our case there are approximately three times more indexes that that there are cells in the memory. And if you do the math, if you compare the commitment cost, the commitment cost to log up versus log star, it's similar because in log star you you avoid committing to the data, you avoid committing to the

accumulation, but you have to commit to the push forward of the ability. So the the cost here is similar to leg, but the the the great advantages app clear when it comes to the B code because in this virtual in this ZK virtual machine each instruction it's the same in zero is encoded you can think between 15 to 20 flags and operants each in each each instruction is encoded for instance there is a flag is this instruction and is there's a flag if it's a zero or one etc etc and So at each cycle you need you need

to fetch those flags and you get you can interpret this operation of fet fetching the corresponding flags and and offsets and etc from an index lookup with the PC column program counter into the bite code and this operation can be performed extremely efficiently. Thanks to log star because you avoid committing to those 15 or 20 columns representing your flags. They are they become virtual columns and in the end you also have some product GK sync to prove the overall

consistency between the pre-ompile call because each time you each time you call compile you need to ensure that it appears indeed in the 16 table. Here as explained thanks to lookup star do not commit to the data which is in accessed by an index lookup. So in this part you do not gain a lot versus the classical lo but here in this part when it comes to the by code you gain a lot and in the end the execution table is mostly composed

of virtual columns. You only commit in the execution table to PCFP and three indexes column. So you only commit to five small field elements per cycle in the execution table. You need to commit to other stuff memory etc. But if we only consider the execution table, it's very lightweight in term of commitment. And quickly to give you an idea how we can use those four basic op codes to do interesting and useful stuff.

Here is an example of how to implement some kind of functions with this very primitive ISO. Imagine you are here. So this is your current frame or stack memory and you want to call a function my function with input Y. You must know in advance the memory footprint of the function and you also know obviously the location in the P code of the function. Then what you do is that instead of relying on the AP allocation pointer register, you will receive as a hint the

location of a new frame in memory which the pro the prover that runs that is trying to to generate a proof has access to knows which part of the memory is still free to use. So the prover can allocate memory knowing how much memory is is required and the prover will hint by inserting at here the location of this allocated memory and then the program will jump to the correct to the location like there

is at the same time a jump in the B code jump to the function and you will update the FP register with this hinted value. So in the B code jump to your function and in the memory your FP jump to this new value of FP and the key idea is that because the prover has the liberty to put the chain of memory wherever he wants. The key idea is that because we are in a read only memory, there is no risk of overwriting previous memory with this chunk. So the prover has no choice to allocate an like

a free space of memory to put it to to place this new allocated frame. The server cannot cheat because it would obviously not work at all if we were using write. In the end, you execute the B code of this function. And one important thing is that using the D reference instruction that the DF that allows you to write stuff.

Basically the DF allows you when you are still before jumping you are still in this frame you are able to write the value of the input of your function in the newly allocated frame. You can also write the value of the current frame pointer here and you can also write the value of the current program counter in this new frame. Then you jump and at the end of the execution of this function, you will be able to jump back to your previous context using those value PCNFP that have been stored at the beginning

of the newly allocated frame. And this mechanism allows you to have functions even though you don't have the IP register. And using this you can have loops because you can transform your loops in your function your loops into recursive functions and basically you can you can do whatever you want like it's sufficiently general to write complex and one last thing I wanted to point out is that recently found a way to use the derence Because as you can see here

the memory will be accessed with some value some index and this will not work if the index is bigger than the memory size. And using this fact you can have a check that some value is smaller than the size of your memory. And if you know that X is smaller than the size of the memory and you know that let's say 10 minus X is also smaller than the size of memory you know that X is smaller than 11 and basically and in three cycles this is an and this is not an intended consequence but you can it's funny but you can use the D instruction to perform

efficient range checks in only cycles of the virtual machine. And to conclude, the main things that remain to be done is to fully implement the recursion program. Only we has been implemented for now to implement properly the SMSs program with the appropriate encoding. But this is one of the important of this workshop.

And finally, to improve performance, even if performance has been improved over the last couple of the last weeks, we still need something like a 5x to be to to have like a good performance and there are still quite a bunch of known optimizations that are not implemented yet. So, we should be able to at least close to the performance targets. [Applause] that performance is single threaded or using

>> it's yes it's multi threaded but it's it's on a CPU everything here is the performance is on the CPU on on this Um so according to the figuring that you presented yesterday there would be um maybe about a 12% improvement in the efficiency of the consistency check between the memory table and the execution table where we use log up instead of logup star for that. So, so is that accurate and if so, um what is the reason for using logup star for

that? >> The reason that indeed maybe log up to be slightly more efficient when it comes to the log up the lookup sorry yes for this lookup execution to memory log up would likely mean would be slightly more efficient. The reason is to use a size just simplicity to have only one look of argument I would say because if log star is much more efficient for the other parts why not use log star everywhere but I believe if there if the number of indexes is three times the size of your table and the extension degree is four

log star is almost as efficient as if the extension is five log star is slightly like 12% less efficient. >> Thank you. >> Thank you. Uh thanks a lot for this. So I have a couple questions about uh so my understanding is that you designed the op codes uh from from the ground up. Um so I have a couple of questions a little bit about the uh the op codes chosen. So the first question I have is um what is this the minimal set of op codes you need for touring complet or full expressivity of your language. And secondly, um, so I noticed you have dref and jump uh in there as fundamental op

codes, which to me strike me more as in a sense helper functions for navigating memory. >> Yes. >> Um, so I was just wondering um especially given that the the lean ISA is fundamentally motivated by your need to verify a very specific structure, right? So the Merkel tree with with all the paths. I was just wondering if it would just make your life a lot easier if you enforced a specific structure for your memory, for example, a binary tree, so that you get rid of some of these um and you don't have to worry about the kind of overflows and all of that really nasty stuff. Um, and therefore sort of like still keep the expressivity by

keeping for example addition and probably you also like latently have equality as another offer I presume. you can do equality by addition would be zero. >> Okay. Sure. Yeah. Um and so and so in a sense if if you really just only need that for completeness and the things that you particularly care about have to do with the uh very specific binary tree structure. Maybe things are just much easier if your memory is indexed like that as well. >> Actually what you're suggesting for instance if we only keep it's anistic but It would be totally doable I guess to implement the XMSS eleation with a

custom doable. The hard part I believe is for the recursion because you have to do recussion. You could also imagine to have recursive like thection being done with a complete circuit but the idea is that I believe it's simpler to use a minimal. >> I agree with you. I agree with you. I guess what I'm saying is that instead of giving full control to your compiler or to your ISA to reach any part of memory which I don't personally that scares me um you just have one index sort of lookup function which basically would say something like look at this part of the tree instead of having drefs and

jumps and then just run through with your custom ISA so with your ad and um and whatever else you need that's very cheap and one or two constraints to do in the transition. Um, and every time you need access to memory, um, you just run that op code. And what it does is it just does a sort of in a sense a Merkel lookup into your memory trace in which you've enforced that you just have very specific places you can put things. And you can even just adapt this to still be general, but have like the XMSS structure that you need as fitting in very nicely. I don't know. I'm just smit instead of a continuous memory to have a more granular memory adapted to the to our problem

>> sort of I mean I I still want to keep generality but what I'm saying is so so your memory basically is like a big block and you can go anywhere >> right and that gives you a massive amount of freedom and it sort of reminds me of what most compiler languages look like what I'm saying is um in a sense instead of your memory just being from zero to k um like in every bit it's a field element with certain number of bits. Instead of that, you just index it differently. So the way that you index it would be something that um is very cheap for you to sort of instantiate in an op code >> um so that for example when you're doing your signatures and you need to make sure that all the different parts work out. So basically abstract away the

refs, drefs and jumps because that can that I mean >> you get generalization, right? But my argument is that you can probably that by uh making more structure there just to make your life easier honestly. Um >> this is exactly the kind of conversation that we want to have >> during the workshop. This is great. >> Um >> it's interesting. It's interesting >> and this relates to the work that you wrote about right. Yeah. For the novm and all that stuff. Yeah. Um >> for sure. Let's have this conversation.

>> Um we have two more questions. Oh, three more questions. Four more questions. Okay, let's be very quick. >> Cheers. >> Uh, thank you for the talk. I want to ask if is it possible to use this lin VM for other applications for instance for recussion and like ZKVMs for like writing verifiers. >> I guess everything has I see. Thank you.

Hi. Um, so for the uh I understand we want to formally verify the recussion program and signification program and the signature program. But will we also formally verify the ISA itself? >> Yes. >> Alex said yes. So the answer is yes. >> Thank you. Uh if I understand correctly uh when we write a program in this language it's then compiles into like circuit or something and you mentioned as an example that if you supply wrong parameters into DF the program should fail so that uh when you compile it means that you provide some additional

sanitizing checks for the inputs I wonder in general when you compile a program uh into the circuit which kind of guarantees It can provide which kind of standardizing checks uh it gives to the uh proven verifier. You mean when you compile from the high score?

>> No, no. From from the up codes uh you obtain uh immediately like uh how formulated it a circuit or like an layer whatever. uh but it it doesn't accept any input that thing you said like some some inputs would fail because they are out of memory or something and I wonder is like a general set of uh there are some conraints that the execution tables that will say if it's an I want this to

be the result of this addition if it's a I want this to be and you have and if it's a jump with condition to like I want to change and you have a bunch of con that ensure that the intuition in the sound at the level of the But actually your idea about the d it works because there is an index look up from the execution table to the lookup that would fail if you try to index with something bigger than the

memo. Last question. your mic. >> Um yes. So um currently >> thank you. Um currently do you have estimates on how how much of the time does the lookup the lockup star argument take and did you look at alternative say recent memory arguments like twist and child? Um currently currently logist is a significant portion even though yesterday I there was some interesting idea I I think this this should be this should be reduced in the coming days

still is a significant portion about twist I didn't answer but my understanding is that those memory arguments require to commit to a bunch of ones and zero which is perfectly suited when you have elliptic curve commitments or binary fields commitments because it's quite cheap but if in our case you commit your ones and zero interpreted as qual field elements I guess you will have some big overhead >> um yeah but I think it can be adapted um we we can talk later >> okay

Perfect. Thank you so much,