Powdr, a modular stack for zkVMs | Christian Reitwiessner (October 2023)

new project we started earlier this year and it's a modular stack for zkm or zero knowledge virtual machines and I want to start explaining what that actually means what is a zero knowledge virtual machine or yeah more more particular what is your knowledge and the answer is uh we're not so interested in that so uh you can actually already forget this Z knowledge part again um instead we're interested in verifying computation so the the the goal is uh to have a computation that is run on somebody's computer and as we all know somebody's computer is not trustworthy so we want to so and that somebody computes a result and we want to check that a certain program run on a certain input computes a certain result and of course an easy way to do this is to just run the computation again and see if the result is the same but then I mean what have we gained with that nothing we could have run the computational sets to begin with so and um yeah there's a very cool result from the '90s that says uh there is a certain way to encode the execution of a program so that uh it it's enough to to read five bits in that encoding to verify whether uh the computation was correct or not and we're not exactly doing that but uh we're kind of making this theoretic result uh practical and of course we're not the only ones who do this there's a gig IND behind that uh that has developed over the past years and especially uh so this has all started with circuits and the main feature of a circuit is that it has a fixed length which means that you can only compute a a fixed computation a computation of a certain size and over the past months maybe small years uh small number of years uh virtual machines have become more and more popular in that area and the main difference here is that a bu machine can run a program with a kind of dynamic length so you can yeah run a program that is quite short or a program that is very large um and this all works in the same framework um yeah and is so and maybe a bit more specific um AVM in this sense is something that has an actual yeah a a fixed program stored somewhere and that it has dynamic memory uh and a program counter that points at instructions in the program jumps and so on so the the execution is much more Dynamic than in a in a fixed Sur okay um yeah I already said that uh there there was a lot of development on these knowled machines in uh the recent time and um if you look at them that most of them are very specific to a certain execution environment to a certain virtual machines certain architecture and uh most of them also did a kind of an implementation from scratch so everything is made in a very custom way uh buil from from very small Primitives and um yeah this has advantages and disadvantages so the advantage of uh building such a thing in a custom way from the ground up uh is probably performance so I think this is the reason why people do it but um the disadvantages are of course uh yeah I mean if you want to get an audit for such a machine then the Auditors have to learn Single part every every uh single custom implementation you did um there's also much more Cod to read then uh if you at some point uh find out that some architectural decision you you made in the very beginning uh was maybe not the best then it could be very difficult to change this decision later on and in generally yeah it's a lot of work to to build such a Zer virtual machine and it is often also Pro specific so when I when I use the term prover yeah maybe I'll explain it on the next slide so and yeah the Cod build is is very hard to use because it's specific to your system um okay I'll explain Pro for so um yeah I would like to make an analogy and I would like to say that uh the current knowledge virtual machines am I actually standing in front of the screen um the currently programs are so programs for Zer knowledge V machines or Z knowledge verion machines themselves are written in a uh in a very lowlevel language that is machine specific and um you can think of this as uh writing a computer game in the in the 80s so you write most of the parts in assembly because it needed to be fast uh and you also wrote the computer game for a specific computer in mind so for a specific architecture and if you want to Port over the game to a new architecture you essentially have to rewrite the whole thing and uh this is of course not how it works nowadays you use high level languages that just compile to a different architecture uh by flipping a switch and you're also not concerned with uh with lowle routines so of course if you want you can write stuff using lowlevel uh mechanisms but that will only be the yeah the very very small highly performance critical sections of your code most of the other code is is very high level and it it just works so um yeah harder wants to be something like LM for zerge vir machines where you can use highle languages and swap out and back ends as um yes we also uh we also want the system to be very modular so you cannot only swap out fr the backends but also some some machines you use in the middle um to to just try out different uh yeah different ways to do things if there's a new theoretical result uh in that are you can directly switch to it and see if it works if it improves your system and so powder is a programming language or maybe two programming languages depending on how you look at it and this means you write your whole ckvm in this language and there's a system that understands the language and you can analyze it so you can run optimizations on it you can check I don't know this this part is it actually redundant can I remove it or can I group some things together and this is if you if you hand wrve your system this is not possible even if you uh I don't know do things in a in a in a modification of rust uh there's no analysis step that would do that for you and uh you can also do a um run analysis on your system whether it's actually doing what you want it to do so you can have correctness proofs of your system because it is encoded in uh in a in a a special language and yeah the the idea is that it's easy to build easy to test and easy to a so this is a an architectural diagram and uh here I explain what Prov means [Music] um powder has or supports different front ends and the list is of course not exhaustive here um we currently support um rust and with assembly as front ends C++ if you compile it to risk 5 also works and uh evm is something you want to tackle in the future so directly direct evm code as a front for powder of course you can write an evm interpreter in r and have that run on run evm code but um this is another layer and um powder has essentially two stages the assembly so powder ASM and the pill stage powder pill uh pill is St for polinomial identity language and this is a yeah this is a language uh origin originally uh defined by the polygon Herm team and we kind of started with the language and extended it uh yeah to um and so and yeah what what does is it takes code written in for example uh RIS five assembly turns this into powder assembly and then turns the powder assembly into powder pill and P is just a series of equations over pols essentially this is this is what it is and um at every stage if you want you can extract the data or also input new data so you can you can take rust and and uh pull it through powder all the way to the to the back grer but you can also take assembly so handwritten powder assembly and injected here you can also mix and match you can have rust code with order assembly and you can also yeah say hey compile this rest code to pill I don't want to go all the way to proof I just want to have the pill code and then I want to run some analysis on the on the P code for example or you can also take yeah P code and combine that with with rust and system like that yeah and uh so this is the point where we where we have our boundary where we stop so we do not intend to build aelves approver is so we stop at the at the point where we have the polinomial equations and where we have uh kind of a solution for the computation so uh one of the main features of powder is that it runs an automatic witness generation so if you have if you have a a program and an input and you run the program and the input it generates an execution trace it generates intermediate values and so on and this is uh P will do that for you automatically and uh so this is where we start we have the trace we have the values intermediate values and the polinomial equations and those are then handed over to aover um we currently support Halo 2 hear and Nova in an experimental way uh but the idea is that we're totally Pro agnostics so whatever whatever has this kind of form where you have polinomial equations uh yeah whenever this is the case then we would like to support theover and yeah the approver does the actual yeah gener um okay um then now I want to talk about a little bit about our risk FL example fronted so um initially we only Built This risk five frontend as a a proof of concept A validation that it is actually possible to build such a system with powder so we can build a system that compiles rust code into polinomial equations uh but it's yeah it's working so nicely that we're continuing to improve it and make it faster and more efficient and but the cool thing about this so even the initial version the initial I don't know unoptimized version it only needs 300 lines of powder code so you define the whole with five arure in only 300 lines of this PO Co lines in the PO language and it will automatically do winess clation for you and it works for any uh no rest and as I said in the beginning we also want to have different FMS so not just not just rust through risk five into powder but also also R through lvm into powder or directly evm into powder and the cool thing about that is uh so there there's for example this this Vala architecture which is a uh specific LM that does not have registers instead everything is done with direct memory operations because in ckvm memory operations are very cheap and um if you do that you can actually directly compare compiling R wire risk 5 through powder and compiling Rask wire valer through powder and see which of them is more efficient or which of them is yeah more efficient in which way and maybe there's also a way to combine these these two uh systems or to to yeah pick the the good parts from one of them and better system that okay um so so here we have an example we have rust code on the left hand side and um as you can see it uses a an external crate so this is just the um unmodified tiny catchup crate and it uh Imports some symbols from there runs a uh ketchup uh hash on the on on inut and then checks that the output is a certain value so that the hash uh has a certain value and um so poter will compile the whole thing for you and uh turn this into r five assembly which looks like that and this is of course just a very initial part um and then we have a yeah very very minimal transform from from risk five assembly into harder assembly so this is the harder Assembly Language we won't continue the example here but I want to talk to you about a little bit more about what you can do with poer assembly and um so the the interesting thing about poer assembly is that it it's a it's a language without features so it's an assembly language that does not have any registers it does not have any instructions at least in the beginning it is so because you can Define registers and Define instructions and by that way Define your own assembly architecture using the language itself So the instructions are defined in the language itself and then they are used in the language and um can see that here for example reg PC defines a PC register and it has a special annotation that tells you know this is this is APC because it's important for um how to how to go to the next line so PC has to be incremented to get to the next line and then we have uh for registers XY Z and a and x y and z are special they are assignment registers uh I won't get what that actually means and then we see we have inser jump so this defines a jump instruction and the jump instruction takes a label and uh here we have the instruction body and the instruction body consists of pill constraints so it has polinomial equations and uh what what does jump do it takes a label and sets the PC at the next step to that label so this means you jump to that label so program execution jumps to that label and uh so this this Prime here after PC means uh it's the PC in the next stro so this this Prime can be used on all the the all the symbols here and yeah here means it sets the you see on the next row to L and we have an assertion instruction here it asserts that X and Y are equal and if you write that as an equation uh we could yeah x - y = 0 we can also write x = y and then we have an add instruction and that one is special because it it delegates its operation to an external machine that is that is imported here so we have an arithmetics machine uh which is defined here and import into the main machine VI and then uh we Define a function so you can have every machine can have different functions and the functions are defined in terms of a sequence of instructions uh it starts with a label start and then it adds two and one and assigns that into the register a and then we assert that a has the value three uh we jump again to the St so this is a program that is valid so uh there's a there's a way to assign values to the variables that do not violate any constraint so this works and uh yeah the the arithmetic machine is a different machine in the way that it's not really a virtual machine in the sense that it doesn't have a PC it doesn't have instructions but instead is uh it has it is defined in terms of polinomial equations directly so you can also do that uh so you're kind of reaching from the assembly stage down into the pill and uh yeah so [Music] while VM machines have functions uh these block machines or these uh constraint machines have operations but it's kind of similar and uh yeah you have you you you don't Define registers but inste you define columns and uh here is a an equation that just says yeah in every in every row uh Z needs to equal X+ y okay now going down to the lowest level the Pol constraint level so um yeah um this is kind of similar to the arithmetic machine we we saw before but instead it the difference is that it's selfcontain now and um I'm sure how much I should go detail here so uh this whole system in the end is compiled down into polinomial equations as I said and the idea is that you have kind of a a very big table with rows and columns and if you have a have a equation like this first * y - 1 equals z this has to be satisfied on every single Row in this table and the the the system is valid if there's a way to fill the columns set all equations satisfied on all rows and there's essentially in pill there's essentially two different types of columns fixed columns and witness columns the is that fixed columns are defined together with the program and do not cannot depend on the input and you can Define them like that here so first is a fixed column um and here the the parameter I is the number of the row so for fixed columns you have direct access to to the row index and it just says if the row index is zero then the value in that uh cell is one otherwise it's zero and so you see for the the First Column has a one in the first row and then zeros in all other rows and then we have two witness columns X and Y which are which are not defined in terms of a function because they are defined in terms of these polinomial equations and uh let's just quickly go through them so these equations both have to be zero and on the left hand side there's a there's a product so they are zero so the equation is zero if the left side of the product is zero or the right side of the product is zero which means if first is zero then the the right factor is is unconstrained because it is already zero right so there's no additional constraint on X and Y but the first is is one so which is only in the first row then these parts here have to be zero which means X and Y have to be one so this is a way to initialize the the cell or yeah initialize these these columns and so the only way to satisfy this is to put ones in the first row here and then uh the lower part here Let's ignore this this this left thing uh the lower part says X Prime - y = 0 which essentially means X on the next row is equal to Y so X next row is equal to Y on the current row and this this just copies over y's from the row before to X in the next row and then the the last part here that is actually this the the fential series definition that y on the next row equals x + y on the current row and that's how you how you fill up the so that determines the rest of the of the cells in this table okay I want you to make a quick demo so this is essentially the the example we saw on the slide and uh now when I run on that so I just do Caro run minus r is you want to run in release mode because past rust means or actually I can just that and then we see the options so this yeah it's just the the different ways you start with it you can start with pill you can start with rust you can start with risk five assembly uh and so on and you want to start with rust and we so this is the directory that contains a a rust crate so it just compiles the rust crate and uh we we output in that directory and I ran it before so this directory is not empty which means override and let's see if that works yeah so it it compiles uh this stuff into risk assembly the PO assembly the pill optimizes the pill and now we have the main part where it diffuses the witnesses so where runs the the actual program and so it says it detected a loop this means that the at the end of the execution just have an infin Loop that just goes back and forth between two instructions and we detect that and can can speed up the uh the generation here um yeah so it is done it wrote the it wrote a binary file containing all the values for the fixed columns and it also wrote a binary file uh containing all the values for the witness columns now let's see what did it actually what did it actually generate um so we can maybe start with so this is the risk five assembly file of the cat check um yes this should be the main um it's it's a lot of code because it's the whole the whole crate and we run um we run some analysis on that and actually remove UN code um yeah I can't find the main function now but it won't be won't be too useful anyway so you see that's a lot of assembly uh assembly files also a lot of data so the these are lookup tables here um and we also have to import some stuff that is part of the of the uh rust compiler or rust runtime and uh then this is the powder assembly file that is generated so uh you see here the registers PC then some assignment registers and then the the 12 so the the 32 registers of the risk 5 architecture so this is actually quite bad for z kvms um because as I said memory access is cheap so we wouldn't need that many registers um and then here's the the definition of the architecture what are the the instructions we have jump load label branches um comparisons Clary operations um some assertions division yeah you can actually see here 275 lines so uh below here the actual program starts with instructions so the definition of the architecture is 27 lines yeah I cheated a bit because we have some external um machines so for arithmetic and binary operations but they are not and here we have the PO assembly code and then this gets down gets compiled down to to pill code you can see here and you might recognize a lot of this because yeah the the instruction definitions they have pill code in their bodies and this gets directly translated um but what is very different is the the actual program so the the sequence of instructions in the program that doesn't exist anymore that instead gets translated into a gigantic table um or a set of tables here which is actually this is and a lot of lots of zeros and ones um and we have essentially we have one column per instruction and it has zeros and ones saying whether or not the instructions used on that line or not and uh we run an Optimizer on that get this code here and yeah this is the demo I would say something else um the the output like the commits and constant those are things that we would take and get give to the approver is that correct yes yes yes actually yeah um I mean you can also there's there's options to also directly run the appr from here but uh I don't want to do that here now so okay I I don't know that much about um the technology behind this but outside of this demo is there anything that people already use about powder or or have built with powder or is this like really just what you just showed us and now people are starting to use it how can I conceive of use cases for this so maybe yeah uh maybe this was kind of implicit but I mean the the prime use case for this is of course verifying blockchains so uh you you just encode the whole history of a blockchain into a single computational single proof and you verify and your syn right need to verify or also um verifying one blockchain and another so so Layer Two blockchains verified in the layer one blockchain um but you were probably asking about specific applications so um we are currently expl exploring uh Partnerships so we don't have uh so I mean this is of course not a production right this is uh just uh um uh in the research stage now in the Prototype stage uh yeah and we're exp um how big is the witness actually okay so you have this one part extion of the that you showed like how big is the witness for that one for example I mean you mean the wi here yeah 5 wow but this I mean this is I mean that that's the proof will be much smaller right so this is just what we give to the pro and then it will create Pro output right and the cool thing is that in some proof systems you can get a proof that totals like a four curve points have four curve points that is entire proof for any if you turn into SAR then there's a way to do a KOB basically right [Music] it's is time 32 Byes and yeah the the cool thing about this technology is that I mean so the input is of course also part of the proof and the input here is not the program it's just the input of the program but of course you can always hash the input and just have the hash actual input and then oh yeah I know some input so that this program runs more of a a general question again um like what's your motivation for working on this is it is this for making blockchains faster more scalable more decentralized I mean maybe all of the above um but like what's the like what what inroads are you trying to make into what problems space I mean in in the blockchain space the motivation is of course to scale blockchains right to uh um yeah be able to move stuff into Layer Two and be able to uh verify things faster so um we actually reduces the need for decentralization right because you need fewer people to actually check stuff um I don't know yeah but I mean and the more General uh motivation is just I don't know I really find this technology to be very exciting and I want to be easier to use easier easier to use that technology and bring it into mainstream because uh I don't I don't like trusting other people to execute stuff correctly I want to verify it I want to verify that's what I find just and I mean I don't know of course blockchain the the main main use case here because of the the interest and the kind of uh yeah trust assumptions but you could I can totally see uh having I don't know a a computation that does hydrodynamic simulation and then verifies that some or a a aerodynamic simulation verifies that a airplane doesn't break down and then condense it into a proof and then you can verify oh yeah they ran the simulation correctly and works or a I don't know um how do you say English yeah do some analysis on a on a building that it doesn't down all right to then thank you very [Applause] much