ZK7: Miden VM: a STARK-friendly VM for blockchains - Bobbin Threadbare – Polygon

Transcript

[Music] and on this stage we're going to hear about mayden vm a stark friendly vm for blockchains with bob and threadbear welcome to the stage thank you anna [Applause] hi everyone well so my talk today my talk here today is about might and vm and unlike i think a lot of previous talks i i don't think i have a single formula in my slides so it will be a little bit different um but basically um so i want to talk about modern vm in the context of blockchains and

zero uh zero knowledge virtual machines so the first thing to talk about is what exactly is a zero knowledge virtual machine and here is like basically a very simple diagram of a regular virtual machine i would say where a virtual machine we can define just the state machine or you know it takes some initial state applies programs to it and get some final state in there now a difference with a zk virtual machine is that you get some extra blocks here so the first block is that and then you also get a proof and this proof can be used by anyone to verify that the programs were executed correctly and you actually do get uh initial uh you know final state from the initial state uh without you actually having to execute any of the programs the other thing that you do get is

something called the witness or you know secret inputs that you can provide into this virtual machine and the verifier whoever wants to verify the correct execution of this program does not actually need to know this witness and you know you can provide different things in this witness for example in a context of blockchain transactions it could be signatures that go into witness so we just need to know that signatures existed and they were correct but we don't actually need to see those signatures and frequently because we have access to this uh kind of private or secret witness secret inputs we can also transform some of the other inputs so for example instead of providing the full initial state and the final state we can provide just the commitments to the initial state and the final state and we can do the same thing with the programs instead of providing the

actual programs we can provide commitments to the program so basically uh those all go into this witness and then uh in theory verified to verify you know the correct execution just needs to know the you know what was the commitment to the initial state or those commitments to the final state and what were their commitments to the programs executed and they can verify that you know things was actually executed correctly uh without knowing anything that was involved in this execution or anything kind of like any specific details so one of the questions why do we need zkvms uh what is the point and well one of the points is that not mentioned on the slide is that for example if you want to have smart contracts that execute in context of

zero knowledge you may want to have uh zero virtual machines because they allow you to have like arbitrary computations uh but another very important point is that uh kind of this is of use you don't need to be like in other cases to be to make use of zero knowledge properties and you know all this awesome technology you need to be um you know either a cryptographer or somebody who spent a lot of time studying this and understanding this but in the context of zkvms like if you have a vm that can take a program that can be written in a semi familiar language to what people are used to then you don't actually need to have any deep understanding of zkp's or cryptography and so forth so that's a big plus then you know this kind of this universality where if your zkvm is

turing complete then what you can do is you can support arbitrary computations on this vm so you don't need to come up with anything else this vm supports any kind of computations and it supports also heterogeneous computation so it could be many different programs that you execute and each program can be different the other thing for the lack of a better word is i guess simplicity but maybe there is a better word to uh to use but basically what it says is that you can you need to design the constraint system only once and once you design it it doesn't change it can be audited it can be verified and the the hard part of figuring out all the circuits needs to be done only once and then everything else is just programs that are written against the circuit the circuit doesn't change and the last uh well maybe not the last

but another important benefit is that you get recursion basically for free because if your vm is powerful enough to support arbitrary computations you can write a program that verifies execution of the vm and then it can verify its own execution or verify the proof of its own execution and you can get infinite recursion this way all right what are the drawbacks so like these are all the nice properties are there any reasons why you may not want to do zkvms and yes there are uh some reasons and a few like a couple i highlight here so the first one is not all proving systems can support zkvm so for example i think it would be very difficult to express the kvm in a kind of r1cs circuit because of you know you need to have the upper bound to the circuit so it might be difficult but in

other kind of frameworks it may not be that difficult so for example for starks it's not really an issue you can it's actually a very simple way for like it's it's a very efficient way for a start to uh to support the kind of virtual machine because you have the state transitions that you know are uniform and you apply one the same transitions to many kind of like uh can you know you have this trace and you apply the same transition to the entire trace and the other thing is the drawback is potentially performance so you can think if you have a computation you can handcraft the circuit that would be more efficient and there is an overhead of the virtual machine that you have to support and for simple computation that actually matters a lot so like if you have something simple you don't want to

have like an overhead of an entire virtual machine running it may be more efficient to do a handcrafted circuit and even for complex computations it might make sense to do something more handcrafted but there is a solution to this or at least something that alleviates this a little bit is that um you can have some specialized circuits within the vm and you'll see some examples of that when i go in into my vm and how we handle some of the specialized computations in there all right um so if we want to build a zkvm the network question is what type of zk vm do we want to build and which architecture do we want to support and there are a few options that we have so one option is just goes with something mainstream some instructions that is already exists out there so an example

could be webassembly or risk five or something like that and it's a perfectly valid choice the other one if we care about blockchains for example we may want to do something that is evm equivalent so basically support you know proves execution of an evm because that's a you know the most popular virtual machine right now in the blockchain space and then the other option is do something like completely new a new architecture a new instruction set and you know presumably you would do it to make it dk optimized so there are a few properties that we care about and you know some of the properties that i think are important are first like how much tooling expertise is there um so if you go with something mainstream where you you know have a web assembly for example you compile things to

webassembly you can there are tons of tools available out there and there are a lot of people who already know how to code and see or say plus plus and rust and so forth that can be compiled to webassembly so there is a lot of tools and expertise and if you go with like evm equivalence you also get some people there is you know quite a few people who understand a solidity and can code in it and you know understand evm and so forth so uh you know it's not as many as in you know with c or c plus and rust but there is still a big big number of those people and then obviously if you build something specialized you will there is nobody who knows what you and you've done before so people need to learn and the tools need to be built

the other aspect that you may or may not care about is you whether you want your kind of vm to be blockchain focused and again that comes in you know there are specific things that we care about in blockchains more for example verifying signatures could be done like in a single instruction for example in a couple instructions you don't want to spend a lot of effort in the vm on that but and they may not be important in general context so if you go with a mainstream like web assembly you don't get this blockchain focus for example but in the other two options you do or yeah and then the last question is performance so if you choose something from the mainstream you may be performant because um um you know there are different options like let's say risk five could be fairly performant if you choose the 32-bit

architecture and you know you choose a specific uh you know extension of risk five but let's say web assembly may be a bit less performant and if you go with evm equivalents that's probably not gonna be performed because evm has made a lot of design choices which are not very conductive to zero knowledge proofs and then if you're doing your own thing then obviously you can design it to be as performant as possible within a given context all right um so let's talk a little bit about different vm design considerations or zkvm design consideration so if we decided to build up to build our own architecture so what do we need to think about so the first one is you know what type of machine we want to do like do we want to have stock machine register machine there is also this memory memory approach

and it's a you know non-trivial decision because for example things that are expensive in regular cpus are not as expensive in zk context so memory access is relatively cheap so you might memory memory machine actually makes a lot of sense um the other one is like how do we want to handle flow control and there are again different options you know typical like hardware domain mark architecture uh there is also this merciless laptex industry that we actually use in mdml i'll touch on this a little bit later um then how do you provide inputs into the into the vm how the program is supplied to the vm and um you know you can do it as a public input like what i showed on the very first slide or you can provide a commitment and then the question is how do like what is

efficient because sometimes public inputs are less efficient sometimes you can provide just a single hash and then you need to like unhash it using non-deterministic inputs within the vm so there is um uh there are different options there um the next is like how do you handle function posts do you allow like you know self-modifying code and dynamic function calls so do you like restrict things memory model is another important one because you know doing write once memory is very cheap within the zkvm but if you want to be potentially a bit more developer friendly and support right and read write memory that's a bit more expensive so there's a trade-off there uh sorry and i guess uh the other things like you know what data types you want to support

this all of these vms for or zkvms work in uh in finite field so do like you expose just the field elements or do you build something on top of that do you have structs do you have uh like regular integers supported and things like that and then the question like depending on which proving system you choose what field do you work and then there are traders associated with that as well so some proving systems are constrained you can only if you work in a given proven system your field has to be 256 bits or something close to that in other cases like starks for example you are not as constrained by field so it makes sense to go to a smaller field and in that the case you get a big performance benefit where you know if you go with 64 bits for example your all

your field elements fit into 64 bit cpu registers and that's already very efficient all right so now there's a kind of overall consideration so let's talk a little bit about might and vm specifically and uh i'll first outline goals that we have from in vm and then can kind of go through through a few design choices that we made from might and vm so first minor vm is turing complete start based ethereum compatible virtual machine so what i mean by this well turing complete i guess is probably known to everyone stark based is that means that we're using starks as underlying proving system and that gives us the flexibility of choosing a small field for example um it is what i mean by ethereum compatible is that we're not trying to be like evm compatible uh i think that is too

difficult and uh you know that you need to optimize like the the performance uh kind of issue is fairly significant so what we're trying to do is build like some different architecture but we want to be compatible with ethereum at the solidity level so the idea is that you'll be able to compile solidity smart contracts into might and vm and then virtual machine we talked about already what it is so there are a few goals that we had in mind when designing mind and vm so the first one we wanted to be safe and safe vm so basically make it as simple as possible uh you know to prevent unsafe behavior or like uh support like prevent unsafe behavior and then support uh as much as possible like ease of formal verification so we

explicitly prohibited some things within the vm to make this task simpler we do want to support some advanced functionality so like the way we want to deviate from evm for example is like you know you want we want to add additional features that evm does not support yet some examples are account obstructions if you care about let's say post quantum cryptography we may be able to support some post quantum like signatures and things like that we want to make sure that the vm is powerful enough to support multiple languages so being able to compile from solidity is important but also other languages like let's say move that was developed at um facebook's novi or sway that is being developed at a few labs and things like that so we want people to be able to choose which languages you use to write against the vm

and then this is more of a future goal is we do want to have privacy in the future and we want to build at least put some foundations in place where you will be able to at least not to hinder them in the future by kind of implementing programs that allow you to have privacy preserving smart contracts right um let's talk about the kind of the how the vm was designed and what is what we do we have inside so we have a this is a stack machine mining vm is a stock machine so we have a push down stack and each element on the stock is a single element in the 64-bit field and basically um you know you can also because of the field choice that we've made you can actually interpret each element as just a single 32-bit element so there are instructions in the vm that

allow you to interpret this as a regular 32-bit uh value and that makes it very convenient you can view this vm as a simple uh 32-bit machine we have memory so this is read-write memory and the memory is what we call word addressable where you have four field elements uh within uh that are at a given address so you can read and write in batches of four field elements if you want to translate this into you know 32-bit numbers so then it becomes like 128 bits per read and write we also have this advice provider this is the mechanism that is used to provide non-deterministic inputs into the vm so like i talked about this witness in in initially so you can for example provide

signatures or other things non-deterministically through this advice provider and then we also have this co-processors this is basically the mechanism that we use to offload some computations to uh like some common computations that would be potentially too expensive to simulate using a stack but we want to do them more efficiently and this is kind of like what i alluded to when i said that some computations may not be like you don't want to do them in general way but you want to uh you know have specialized circuits for those computations so let me give you a few examples of those um computations so here's like a few core processors that we have right now for example we have a dedicated uh set of co-processors that does 16-bit bit range checks and those are used within the vm

you can actually do up you know four range checks per cycle we use rescue hash function as the core hash function within the vm so you can do a bunch of things kind of we have this hash processor that allows you to compute two to one hashes or linear hashes and we actually have instructions that allow you to compute the full miracle branch in a single vm instruction in basically a single vm cycle which comes in handy if you want to do like recursive start proof verification where you need to verify a bunch of miracle paths the bitwise operators like and or and xor are expensive very expensive to do like on the stack so we have a specialized circuit that handles those and so basically it's still from a standpoint of the vm it looks like a single

vm operation but there is actually a separate circuit circuit that computes those and then we another have like an exponentiation that is a small one to handle like raising to a power of two and then in the future we might add others because you know if you want to support elliptic curves you might want to have some other additional uh coprocessors and do like you know operations over elliptic curves more efficiently all right this is kind of a diagram of the execution tray so like because this is start based vm one of the important things is like what is the uh kind of the stack trace and the way to think about this is that you have uh like each row represents a state of the machine at the given cycle and then as you know you can implement this like as different columns and then

each row is like a state of uh avm at the given cycle of that vm so we have a like logically speaking i don't know if i have a pointer here maybe not oh i do um so we have different like segments on different columns responsible for doing different things so like we have a decoder that decodes the instructions we have the stock uh columns that handle like operations on the stock uh we have this like a set of columns that handle range checks and like a bunch of other coprocessors handled here and like if you look at this for example this is just the selectors that turn on and off a given co-processor for a given type of instruction all right the other thing that is interesting is

how we handle programs so the user-facing interface to the vm is this modern assembly language which is a fairly simple one it's basically you know you push elements into the stack you perform operations and so forth you have uh fairly simple instructions uh but we actually have a kind of assembler that translates this into a pro what we call a program master mercalized object syntax tree and then it's actually this syntax tree that gets fed into the vm to execute the program so let me talk a little bit about this program as so what is the merkilized object syntax stream and this is basically if you think about it as a it's a tree that represents a sub programs that kind of get aggregated up to the root and every well let me actually describe this so there are some key properties to this merciless objects

industry so the first one is that um you know all programs can be reduced to a single hash and this is the root of the mast then every internal node is actually a subprogram that represents you know the programs that get aggregated up to the root and we can they'll control flow with via this internal nodes and then leaves of the mast are actually linear sequences of instructions that have no control flow in them and just to give an example of how this works so let's say this is our assembly code we have some sequence of instructions then we have an if else statement within the via within the assembly code and then you know there are two branches and then at the end we execute another linear sequence of instructions you know mast for this would look something like this we basically have the four sorry

we basically have the four uh kind of linear sequences of instructions at the leaf nodes and a split block a split node here basically indicates that you either execute a left or right branch depending on you know what is the top of the start look right now and then a join block basically says it's a sequential execution you first execute the left node and then you execute the right node so this is basically if you start at the root and do a kind of depth first traversal of this tree you execute the entire program that's that's the idea and then i guess the question is why do we bother with must why didn't we go with you know one neumann architecture or something like that and there are a couple of reasons so first reason is um kind of alludes to again this uh how do you supply a

program to to the vm and as i mentioned sometimes you do it as a hush and then you unhash it within the vm kind of like provide the actual program deterministically and then you start executing uh with this approach you actually need to unharsher hash only the branches that got executed so the stuff that you don't execute you never actually have to unhash a hash within the vm so that means that if for example you have a smart contract that has a bunch of functions and a given transaction only executes one function you only need to ever unhash like in that transaction that one function that gets executed the other benefit is safety because of the structure you actually always deterministically know what it's getting called so you don't call a function by providing an address in memory you call a function by providing a hush of that

function and then you know the hush fixes the code completely and you know all all call targets are always known statically and uh the last one is like it's interesting because you can actually think about this merkle tree where you can reveal different leaves selectively so you can hide like keep most of the tree private but reveal some leaves in the tree and that means that for example you can have public pre and post conditions where it was a private program so whoever needs to verify the program they don't know what the middle of the program does but they know that for example that they have run the program in the beginning and at the end that verifies that no new assets were created or destroyed while the program was executing um yeah so and then um almost done here but uh just to talk a

little bit about like the performance because this is important and this is why we try to build something that is more zk optimized so in our case the target reform and this is still work in progress so this is what we are targeting um this uh like on if we want to run my vm on a single cpu core you get about 25 kilohertz so you will get about 25 kilohertz and this is not a lot uh this is fairly slow but this does include both the execution and the proof generation uh and uh the nice thing about generation obviously is that it's massively paralyzable so if you throw it on 16 or 64 of course you can get you know not quite linear improvement in performance but pretty close and then if you you know you go to gpus and fpgas and so forth you can actually

get to much higher levels of performance here and then on the verifier side um you know the proof sizes are you know with any transparency with any transparent system unfairly large so you get 6200 kilobytes depending on parameters that you use uh verification time goes extremely fast it doesn't really matter how much uh how long the computation is itself but uh you can verify pretty much any proof within three to five milliseconds if you think about like the cost of verifying for example in the ethereum context it is a bit expensive because the proofs are large and it costs you know a fair bit of gas to put uh to put large proofs on chains so you know for those who know ethereum like three to five million gas that's what we would roughly cost to verify start proof

all right um and to wrap up basically where we are with my vm we released the uh first product first prototype in november we're very actively working on the next version which is going to be released next month and that will support like read write memory 32-bit operations natively and procedures and a bunch of other things and then you know by august it's going to be kind of more or less feature complete and we will be building a roll-up around it you know as part of the polygon modem so that's that's it thank you [Music] all right there's a question over here are you aiming for and is it at all

conceivable to have my vm formally verified and the verification the verification circuit off or it's not a circuit right it's a program also yes i mean that would be my ideal scenario like we would want to i mean once we have all the constraints written out and once it stabilizes a little bit more because we are optimizing and changing a lot of things yeah formally verifying those constraints would be the ideal outcome and then actually somehow figuring out whether the translations of those constraints into the code was done properly is also a very big problem so that's something we still need to solve as well yeah thank you so i was wondering basically in case you're supporting loops in the how how

the structure will look in the mast because like if you need to keep extending the execution of a loop like due to more iterations like at the end you should arrive to like a maximum heat of the tree that you're supporting or something like this so how do you approach this yeah so within the master actually didn't show this but the way you handle loops is that a loop is actually a single node that like you don't unroll the iteration of the loop so the way it would work on the vm is that you execute let's say a sequence of linear instructions like let's say the loop is the simplest loop has contains a linear sequence of instructions so you execute this linear sequence of instructions in the vm and you verify whether this iteration of the loop matches the the hash of the node for the body of the

loop and then once you verify that it matches you know that at least one iteration of the loop was executed you check if the top of the stack is one for example and then you enter in the next iteration of the loop and again you have to execute it in the end and once you get then you again check whether the hash is correct so basically it's one node for the entire loop oh a question all the way back there right making me run um could you talk a little bit about um how the stack is implemented in the trace like um what are the values that you actually write down yep yep definitely so the way we implement the stack is with we allocate 16 columns for the kind of top of the

stock so basically at any point in time like instruction can access 16 elements of the stock and then for the things that fall kind of out of this 16 elements we have um kind of like this what we call an overflow table which is implemented using this multiset checks basically it's kind of like a you know i guess very similar to to the way you would handle it in plonk i guess or long cashier's mutinization where you have this table that records the stuff that gets kind of removed from the stock at one cycle and then if uh if you drop something from the stock you also take like remove the item from the table and put it back at the end of the 16 columns we call those things virtual tables actually i should have highlighted it when i was talking about this diagram we

have a bunch of those virtual tables that tie different parts of the execution trace together so from a stack itself for example the way you would look up into the processor table is that you would do this kind of multiset check against like an inputs and outputs based on kind of like the same thing that the plonk does uh hi uh i was wondering i'm here yeah um so you mentioned earlier that you had like almost 1 000 of commitments that you generate like for your trace and since you are using stock proofs i believe that it this will be fry commitments do you have any like id on how to batch them batch verify batch

open this kind of commitments since like stock proofs is not on office like so are you talking about like recursive proof aggregation or something else uh i know what kind of yeah so i mean you can so like once you have the vm itself you can build a stark verifier uh in the in the assembly language of the vm and then you can uh you know compute a bunch of proofs and then just aggregate them recursively and you actually get infinite recursion so you can do it in a tree-like fashion whichever way you would like so that you know if i'm understanding your question correctly that should not be a problem once you have the kind of written the recursive proof verification within the within the vm okay thanks do we have any other oh there's another

one there actually i think was there one from the live stream oh oh just i have to run i feel like next one's gonna be all the way over there all right yeah so i was wondering basically in regards of the memory alignment uh if you are doing always rates of uh 128 bits it was if i remember correctly since solidity supports structures and i guess that you also will want to keep like providing support for all of those things which is the approach that you take are you padding the memory for not needing to do like an align reads is the capability of doing that is a task of the developer to figure out how

to like create everything yep so that's a very good question so the way we're handling it that's something that i didn't touch upon in this talk that we have like a standard library that allows you to write custom procedures so there will be like a like ethereum built-ins as a part as a namespace within the library that will say well execute an m load which interprets the memory as a you know byte addressable array so and it will be less efficient than trying to read because you will need to like read multiple potentially elements from multiple addresses and then like shift them and things like that so it will be more expensive to do that but it will provide you with ethereum compatibility in that way yeah it would be much cheaper to do access this way but if you need to do it another way to be

compatible that you know you'll pay a little bit extra for it any others here okay okay yeah all right livestream question a question about um what's what's your current memory model and what's the advantages slash disadvantages between your design and cairo's read-only model yeah so um basically the way to think about so like the most efficient memory you can implement in zkvm is something that what cairo does where you have write one's memory uh it's actually just very few constraints that you need to impose this approach actually is a bit more

complicated because you need to support read write memory and so you need to use a few more columns and like the number of constraints is probably like four times more i you know it's like think about it four or five x more complicated than uh cairo system but at the same time you do get the benefit of read write memory and one of the reasons why we do this um you know ability to read in four elements rather than just a single element is because reading four elements actually amortizes the cost across you know you actually you know maybe like when i did the calculations our approach is maybe like two you know x or two and a half x less efficient than kairos uh for the common use case uh and the reason again if you need why we do this reading in batches

of forest in many cases like the hashes like rescue hashes feed in four elements so if you read the rescue hashes or process merkle trees which i expect to be a you know a very important use case to support in the blockchain context is something that you know makes sense for you to do this common optimize for the common use case yeah but if we if we did it naively where you would allow to reading a single element at the time i think it would come out to be like five or six x and less efficient than uh cairo approach okay cool all right so i think that wraps up this talk thank you so much bobbin for this fantastic talk thank you [Music] [Applause]