Minimal zkVM - Cairo M Design

Transcript

Sorry for the few minutes late I was out of battery. Uh so during this session we are supposed to with Robin to talk about minimal ZKN design. So we are going to do this actually two stage. uh I will first talk about uh I would say the the way the the things that you can do when you want to design I would say these days generally speaking like if I want to I mean because I built a ZV like months ago two months ago say so this is fresh ideas that when we want in 2025 you know to start building basic from

scratch and then from this presentation we will go to minimum term that may may go may talk about at the end of the of the slot at the second half of the slot. We will see anyway at the beginning it says that when you really want to do only few operation maybe you have some design decision that you can make that makes the whole things more efficient. So I'm not here to to brag about this current design.

But this might be also a bad marketing decision because has nothing to do with so don't think about game if you know it anyway. So I think that uh so nowadays there is because I was talking with some people day before and there is a misunderstanding of the fact that if you actually build a play you don't need to commit to the whole exection phase. This is not something that I think it's done. So basically if you go from the execution up to the proving you have normally an initial I would say trace generation which would be a log of all the states of the the

virtual machine that you are actually exhibiting plus a log of all the memory memory access I would say that you so this is sort of too small in terms of number of column but very long in terms of the size of the execution table. So this is sort of a first name generation and then from this initial table you do a I would say if you talk about data set you do group by at some point of this big traces to split it in terms of operation that have been done by the by the main trace and this is sort of the second I would say witness generation or the post processing of the witness of

the initial weakness that you have and this This is the table that you actually about to to commit. Uh if it's not clear, you can tell me. But anyway, the idea is that you don't you don't build a whole trace in the pro. What you need to think about is you will have several tables that are communicating with each other with a system that you can think about as a as a messaging system like whatever you can push and pull messages from it. The actual way it's done is using local look.

Yes. In your mind, what is the advantage of doing this with multiple tables compared to maybe older designs like the old where you have like the classical way of doing things. So the the thing is that if you if you keep the whole execution trace is one single table of course you have the size of your table that is directly related to the size of the execution. So if you want to execute for 1 million cycle or 10 million cycle or 1 billion cycle then you need to materialize all this table. But if you actually reshape it sort of move back several small tables you have all of

these tables. If you have 10 of for example and the execution is sort of evenly split into the 10 of you have 10 10 tables but with the size divided by 10 so that you can sort of fit 10 10x more operation with the same final log size and of course the size influence the size of the proof. I mean the number of influence the size of the proof but still so it helps you first get smaller traces and that height more easily constraint that applies to different because you don't need to manage a global state. So the idea is that as soon as you able to split the main logic into several independent I would say circuits these

independent circuits do the operation that they need to do on their own parts and they remain consistent with each other by sending messages at some point meaning that for example I have consumed a state of the VM with PC or something and I'm adding to the queue another state that needs to be consumed by someone else but you don't need to sort of to materialize effectively how the host are organized with each other. So it's more like for example if you say you have a two addition and multiplication and you're only doing one of the two each row in your table for example for addition you

enforce that the output is equal to the sum of the input and it will consume a state of the uh of the VM and it will push another state and this other state might be consumed by another addition might be consumed by a notification you know So it helps keeping everything very local in terms of constraint declaration and the the the lookup arguments are used to maintain the global consistency of all this local constraint so that you actually prove an initial trace. But it's more like you are instead of keeping the the view of the big trace you are splitting it in independent choice and sort of building a graph of

dependencies in all these chains. Thanks to the global argument which means that for example uh yes for register update you don't only like it's always like it's always any operation that you do is always consuming a previous state. So consuming a message that has been emitted by someone else before and adding eventually something else to the to the cube that will need to be consumed by someone else at the very end. And at the very very end of course you need to find zero meaning that the stack of messages or say a stack of state or stack of whatever has been pushed by someone else

has been consumed by someone else. Yes. Is it true to say that the advantage is that the constraints are local to the table? table are more appropriate constraints. You don't need constraint that will apply to all the roads and and I think that you gain in this sense at the expense of having to pay maybe for the communication between the different tables. I mean it simplifies the constraints in the sense that instead of having to describe the hold all the possibilities in each row.

>> Yeah. >> Like if you come from the usual design, they have tons of flags because you need to make sure that if the flags one or two or three is set, then this constraint need to apply and this is sort of replaced by independent very I mean my belief very independent piece of logic that constrain one circuit. So the circuit is sort of the flatten of course it's a I would say the color of the table is one is a circuit and then this circuit just is related to others by pushing to the with the argument some part of the value that it uses. So to make sure that they are related to values that have

been used somewhere else. For example, if you if you if you can go to memory, but if you want to do a memory that you do to pull values from memory and then write the values for memory. So from the point of view of the logical the values are here you just want to constrain the value like for example addition but because it's not an independent second but it's normally not part of a global execution these values that you use needs to be related to the values that are used of course by the component and especially in this case by the fact that this is memory segment one single memory segment probably for the whole memory segment

let's say one single memory segment for the So as soon as you use the value you need to it's really like messaging you need to think about it as messaging. Yes. >> Yeah. So on the the point that you were mentioning you will always be this messaging anyway even if you were committing to like the extinction trace uh of your program. uh it's just that if you remove the competitive exection trade which naturally speaking is going to be one of the largest people that you will have uh then you end up having a trade off of more look more but small amounts yes and I think but you will always have naturally this kind of

prediction looks anyway to ensure like global consistency because your pairs are going to be enforcing only constraints one thing although that I think Worth mentioning is why more recent designs can afford possibly remove completely the notion of committing to the execution trace is because all the designs were CPUcentric and your CPU is in a sense literally executing like execution trace and this is why it is quite burden. This is where approaches that open allow different approaches and are in a sense probably more when lean towards more of a messaging stack and then you can

push and pull whatever you want. on this tag and that gives you a global consistency. Thanks. You have more anyway. Uh and then from this point then you can really decide to add one or two or three or 10 tables regarding depending on the need that you have. uh I think that uh I did you can have registers of course you don't need to have registers actually in the sense that at the very end the only thing that's required is that the whole the whole queue is empty at the very end this is the only so you could have one single proof system that make co different kind of logics and of state transition

function at the very very end you just need to make sure that all that has been emitted has been used by someone else. I think that this is really the most important things to have in mind. And so if you think about it like that, you can see if you think about it like that. So you have one big table that you're going to reshape doing group by logic and then for each logic they're constraint is a circle. So each table is one single circle and once you have group by you just from the point of view you start with a group by tables. This is the weakness of the program and these tables are all related to the initial

big data frame because you have so which means that you start from a single table and then you split in several small table that represent the actual logic that you want to prove. >> Yes. What's the criteria that you use to create a new table? That mean at which point you say okay this logic is sufficient enough for me to create a new dedicated table for this. So I so this is I think the the how I see things now is that if you if you if you are from the prover point of view the constraint that you can

describe from with saying that you can describe additive or mic at the very end. This is the very limited field that you can use when you build the circuit and then from this you can expose them directly and proceed with flow. So you will have likeification or you can if you need to store memory the opposite operation subsection and division and then the flow. This is I think the bar that expos directly what the constraints actually if you were to write directly with with the library the comparation plus if you want to have

a line some sort of filter and plus if you don't have one in the table uh of course some sort of memory memory that needs to leave somewhere close to related to this to this minimality. Uh that being said uh I think that of course depending on what you want to prove if you know that you are going to prove most of the time that given computation instead of keeping only additionification you can add a code that will gather what should be otherwise a friend of your of

your initial say of your initial computation if this makes sense. It's just like If if you expose this in for example then you write a function that do addition addition addition multiplication multiplication addition again this is going to be five you can describe it as a sequence of five minus but okay if I use this frame in terms of compression frame again and again I'm better maybe just do it as a as a component itself and get and get a function that will just go and directly fill this air with same of course plus cycles plus eventually operation in the sense that if you if

you do several one component of course you can reduce the values more and you can in one single conraint have several several but not usually speaking number if you define your define your addition and not three four five I think to complement this um whenever you want to prove something you can start with a single error that's going to be fairly complex like with a bunch of registers super wide but it can represent the whole computation. The problem with this approach is naturally on every row, every step of the execution, you're going to have a bunch of waste because as you want to represent for example all the operations

that you can support, only one is being executed for example or very tiny subset and so you end up with like a massive waste on the total area of air. And the question of when do you want to offload a part of the computation to air processor is basically I think looking at the overall surface area of of combine if you manage to reduce this usually I mean always depend on like some of the resistance you're using and the different parameters that you're having but usually reducing the overall air area is going to allow you to gain in performance even though there tricks like naturally if you want to optimize speed only you would rather have super wide air traces fairly small intense the

otherise on the other hand would rather have extremely narrow traces fairly long when you have regression involved then becomes a bit more tricky and you have a more complicated trade-off. But yes, I would say surface area on your edge is basically the reason how you design >> and so for example if we look at what is your simple I would say in terms of yes in terms of of How can I do that?

So in the end the minimal I think everyone has agreed that this that the minimal VM that is still actually a VM with random number of needs to maintain at least two registers the program to point to the you want to execute and consequently the same as this you were doing this if you have read memory at some point I think it's also required to have I mean there might be but you need to have a time stamp that says when this instruction was Otherwise you cannot guarantee that the right is followed by the read and not the read and then the right are making a good value. Um so that you need also of course to get this previous time stamp for each value that

you use anyway and uh yeah so basically this is how you locally enforce the global transition by each component actually removing I would say from the messaging the previous register state that is actually using and adding the next step that needs to be consumed by someone else. You don't not need to know what will PC + 1 be as an instruction but you might force at least someone to consume this and it's the same for I mean in my design here the the program is so for the you just keep consuming considering the fact that all the required values have been edited by the the the segment from the memory comm

the memory you remove the previous value for each address and you add the value that this component is supposed to is supposed to enforce and then and maybe here is where I understood well saying that it's possible to do something different I have not figured myself yet you need of course to check that you in this design at least that you are writing in the future and you are actually removing what it has been done in the past uh if I mistake You were saying yesterday that it's possible to remove this shape for for this kind of operation.

I think it was. >> Yeah. When it's you don't need any time step because I never change so you don't care. But even if it's right even if it's right and if everyone has followed yesterday and somehow followed but I did not understand everything. Normally it should be posed to remove this handshake. Uh but maybe I want to small vote.

>> Yeah, I mean in general with any um it really reduces to a matching problem. >> Um and just deal with that sort of way. Um but range checks are something that are like if they're not too expensive, you can put those in but I think I think there's a lot of work around these techn and the thing that might be also I think is if I'm not mistaken what you say if I I could remove the the because here all the time they are guessing witness

generation so they are not part of the spec when it receive the initial witness you add a time stamp each operation and then you can make sure that there is sort of a past and a future where where normally if you're just doing local there is no past and your future you're just enforcing local as well and and enforcing that someone else is taking up where you are actually in the state. Uh I think that maybe if you want but you say that you don't have jobs that's also maybe the >> those are sort of independent concerns.

Um you can Even laron of those issues. Just to give you some high level context though on sort of a range check like that power checking in this situation. Um so when you're doing rewrites um we found when we were trying to get rid of the range checks um that actually you kind of need a unique identifier for every single one of the matches. So when you start doing multiplicity stuff so when when you start sort of like getting roots with multiplicity um which you know are just the way we represent them in polomials things get kind of uh well I want to say disgusting but difficult um because you

have to basically because it all redesum I can go will find you one. Um, but if you have unique identifiers for everything, you can basically reduce it to like the same way open. The way I I kind of in intuitively think about it is that like um you can't really get rid of check unless you do do like a global check at the end of stuff. So I always put these things like a similar level of power in a sense.

>> I feel this is if you have a fixed sort of control flow and that you can exactly know from the very beginning how much time you are going to jump in which location and so on and so forth so that when you jump you exactly know the next time it will be used and this is deterministic from the very beginning but if you want to have a sort of a general purpose mechanism that allows more flexibility then you need to have this >> yeah so like the moment that you allow for determinism you know like just to be clear I mean determinism in the context of there's a unique transcript for every statement data pair I don't mean determinism in the context of the rap where we're doing

interactions between the prover and the verifier you actually end up getting way way more powerful properties in in in a variety of different context one of which is as you said very correctly um this kind of stuff so you can um you know the more structure you impose on it, you can sort of reprocess the way and and really get rid of the race checks. But you know what motiv is that what you can present later this morning or this afternoon for the question it's the same because you say that you are the all the indices are deterministic and so you don't you even master process you don't need to to do

this kind ofation because you absolutely know from the very beginning which indices will be used by which of the hand and when. So any kind of friendship model >> uh on the branch checks one thing that we were doing with Petra one idea that we had is so range checks um typically you'll break them into smaller uh you know ranges like do an 8 bit range check and then sort of do a couple of those to do a 32bit range check. Most of uh you can do a sort of caching type of thing where if you know that some memory cell is going to get read you know in close

sequence to itself most of your like the range check on the actual reads can just be say 8 bit range check. So it only you know allows you to read something that was read within the last say 256 cycles and then you have a separate table that sort of loads things from cache. So if you you know basically most of your reads can just do an 8 bit range check and then if you need to access something that hasn't been accessed in a while you sort of have this separate table that's just going to do a read and a write and so you get you some have a small reading memory that is buffered at some point depending on that you're going to use that when you need only to read values you read

values from this small buffers relation and then If it's too hard, you need to to pull it from the global level. >> Yeah, I think that's right. I mean reads and writes, it's basically just that like when you do an actual write, it needs to have a time stamp that's within a very small range. >> Yes. But for this for this item difference what we what we do I mean what actually is but we are just implementing a clock and component which is just not the itself but the full witness generation part where it actually just figures out to there is

deltas in the time that are too big to be handled by the uncheckable. It just keeps adding rs that are that have never been done by the VM itself but that dates in the clock. >> Okay. And I think that's some flavor is where is that size? Yeah. This is because you have a built-in range checking it of course depending on the maximum size that you want to cover. And so when you do the generation which is this group byation you you figures out that you figure that there are deltas that are too big. So you can just add this kind of constraint

in the in the table and they makes absolutely no difference in terms of logic. Just keep increasing the clock to see the moment where it will be close enough for the next actual usage in the the logic. Uh yes, this is this is like to say here I think the memory the memory design is maybe the most interesting things actually how to interact with the memory memory what do you do with the memory because the instructions themselves are really dependent on I think the problem that you want to do apart from maybe additionification and I think also that the combination of the of the most

description is something that is interesting to do. That's why I was most in favor of the autocompile autoi things of uh of what is doing uh maybe as one thing I'd like to say is that when you design so of course the the native minimal world is the element I mean of the every color will of course get one single element of course but from the VM point of view and from the memory management point of view you don't need to say that the memory world is only one element and you can actually naturally design your your your memory to handle

a lazy even a lazy number of elements which becomes quite element if you want to do native types with several elements like for example if you are working a small field that you want to do 32 or 64, you need two of them or four of them for example. And actually you can design your your so as to to to navigate I would say this uh this variable size number of feed element per quite easily.

Um so if I'm talking about that here because the thing that is interesting to notice that when you do a lookup argument, you actually are training zeros that have no impact on the value that you're actually pushing to the I would say the commitment. So it's the same to push memory a z and four value and you can you can add an infinite number of string zero it would be the exact same because at the very end how the login is computed this will you get the challenges and the the weighted the weighted value of the tpples that you provide with all the random challenges.

So all zeros in the tles are actually discarding the the value of the lookups. But if you put all these values at the end of course of your topple, it mean that the topple with training zero, you will get the exact same value as a topple with no training zero, which helps you uh navigate easily. For example, between a U16 and a U32 or a U64 if it fits if it fits. So it's a free testing I would say of different size differently size U type If I understand so if I understand correctly when I read like the paper if you want for example to transform a U32

into a U64 you just have the trading zero yes I mean so you don't the thing is that because the value that you push to the Q of Z stack stack of value that needs to be used at some point won't be affected by any number of z if you are at some point use for example your proving an operation of value 32. So the component of course has materialized two field element per input and it does the computation but if then you want later on to use these values at the same address as a 64 because the 64 is just adding you can directly read the memory

value at the same address that you computed as 32 but you read it as a new 64 Is it possible to go in the other direction removing the training mirror? >> Sorry the thing that there is no real need to either add them or remove from a component of if you complement and then the output of the computation actually fits in a U32. It means that the two last are zero which means that this later on you can just read in the component it will match >> because what you want at the very end is just to make sure that all match.

Yes. So you can have a viable number of per address which can be quite interesting both for set. So you can have with only one or two but with much more if you want and for the more flexibility to to actually play play with this. Yes, I think this is so anyway the main takeaway to me now this. So the main take away is really when you design when you design the minimation that exist at the prover library

which say yes just maybe I have a question on the plus and minus that you is it similar somewhat to the M3 stuff that you have done with streaming stuff Yeah, I mean I I consider this type of architecture to be an optimization, but I think the idea has popped up a couple different times, but as long as I can like um one way I one mental or just formal model I have for these types of systems and etc that I think is useful and underexplored is modeling them as colored petriants which is like a well known

type of problem computer science and I think that would help us to be able to like formally model systems and statements within the language of petriets to formally analyze like correctness and soundness and capture noneterminism. So um yeah okay yeah was I mean I free yesterday from from Ben actually but it's probably when we talk about this is probably really really I mean if it's not the same it's really similar uh to be fair the the only so from my my

perspective the idea might come from somewhere I don't know but because I mainly designed all this based on the observation of what is doing for the work and discussion with engineers I don't know where they can when they but maybe I don't know but that's why also at the very end the real users need to think that you're pushing that it's a login or whatever kind of argument really does not make any difference it makes a difference in the cost analysis because then it's how the look is actually matter it doesn't make any difference the design in the design decision of the component

uh anyway So what I wanted to say as a conclusion I think of the minimal VM thing I was yeah so so as I mean my is influenced by what what you have been doing for three years now what about so I've been wrong saying that fbased KVM was probably more efficient than risk five or whatever instruction already existing for general purpose computation. It would be possible to save on cycles and be at the very end more efficient. Uh now when I think about this

so I think that you either want to do general purpose computation and most of the software that we know is actually written with a bite system in mind. Everything is a bite. So in this context I would put my memory to be from the very beginning constrained to be a bite memory with each being a bite and then you don't need to range check again and again all the values because by design all the values are by for example but then you need to remove completely the idea of a feed element from your memory or you really want to be at the field element level because you know what you are doing and it's

something very specific and especially for example if you are doing a verifier because the verifier is actually natively it's one of these program that are natively few based I mean I get up and then I'm not sure if it really makes sense to do a VM like a full VM with a full execution flow that can execute random things because you know that you're about to execute maybe true verification and the proof verification very failure is determined problem it's not any random problem exactly know how it would be, what would be the control flow, how many steps he would do and then at some point to come up with a I would say no VM design there is not even a VM and very close to what actually

we talk either now or maybe or this afternoon but anyway so I think that the idea is that if you are thinking about field element operation or operation between field element Then you probably can just set up the circuits that you want to do directly as tables that fit your own computation and this can be done either with a circuit build or with a compiler writing a TSL directly to I feel that most of the company have actually for you look at the start marketplace is definitely not written by I mean it's been generated so that's why it's a bit

difficult to to learn is reading scope for example because it's machine there is a lot of things that you need to remove organize to meology so I think that yeah you get sort of DSL or language or whatever but this is not a VM then anymore not so much or you can use this for defining compile or ash function maybe it's a bit easier to work with but maybe not so much and if it's general purpose computation I think it is better to pick to pick an existing instruction set and not to go there so much about defining instruction and control flow and language and compiler and so on and so

forth. Uh yes I think this is the and I think it's a surprise that actually if you go to proof you see that most of the people are actually improving bugs are just using everyone at the end is using still and I think only is still using custom circuits for the this big which is so yeah I think it's just I mean I spent 2.5 years building software and I think it was yeah that's my view about VM CKVM and

the minimal minimal you say >> yeah I don't know if I should probably say >> we have 15 minutes maybe we have one You mentioned for example >> I don't know if you

Um, yeah, I mean Petra Petra was a custom ISA. One thing that I think does make it different is it was designed to use write once memory non-deterministic read only memory but kind of like for functional programs and that does make like a bunch of things nice. So you noted that you can get rid of clocks if you don't have rewrite memory. Um but also there's like the tricks like the prover allocations are nondeterministic which I think I saw in in your design. Um and I think this like covers uh in a bunch of programs that are like you express a lot of programs as as functional programs. Now the main

downside that we found is that when you basically need to do continuations and pass from your local frame to the next frame. You could end up copying a bunch of like data like local data data between these frames and then sort of if we're redundantly put it into memory. Um that's uh I don't know. I mean I think there's that that is a cost. It depends. There's trade-offs. If you can handle memory interaction properly, you can get around it.

You have to And but yeah, I think that the I mean the cost of maintaining a maintaining a compiler of tool chain or something or whatever to actually target this compared to the simplicity of just using maybe using 20 30 50% of performance but then being able to focus on places where you probably can get a 5x or 10x if you do a good acceleration or GPU or whatever then for sure. Uh, one one other idea that we didn't pursue that I thought was like was thinking about a lot um, argument

guys recommended building an archonization for the zinc VM. So zinc is a uh, a virtual machine that comes from the literature and uh, like ML like languages compile to it. It's an interpreted it's an interpreted sort of small language. So, the language has a um target if you run there's two compilation nodes one will compile the native one will compile to a zinc like interpreted VM and it's a pretty small thing um I think that would be pretty cool because then you would basically get the ability to write programs and uh compile it to zinc and thenize that um

there's probably some more like exploration of of these sort of like mineral interpreted things that already show up. entire

mix of for yeah because we doing together performance of the kind of jokes kind Yes, but at the very end I think or do software that are compiled with

and then generate the sheet that you want to use and focus on for them. So I think it makes sense. I was in love with ZK for this specific table so that it creates a consistent uh proof for this operation or I said I want network need to be able to pull any people want to pull and I want

and this is my so for the only one things or few things that are clear that won't change then directly that you want to build this given interaction uh because there is a the same thing and then just play with this fill the table as you want and there is no more concept of the end but then this is what say the mic

wants to say something.