ZK10: powdr: a modular stack for zkVMs - Christian Reitwiessner (powdr labs)

Transcript

[Music] yeah let's just get started powder is a uh new project well this is bright a new project we started earlier this year and um the idea is that you can use powder to build zero knowledge virtual machines um okay I probably don't have to talk too much about what is z knowledge virtual machine is to this audience but just one thing uh the ZK part in the ZK VM is not too important for us uh we are more focused on uh yeah the verifiable computation aspect so we want

to have ckvm that generate proofs for execution of a program that are faster to verify than rerunning the execution in the first place and uh there are two distinctions uh ZK circuits and ZK VM and uh yeah CK circuits are fixed size the the computation you can do is is fixed and in contrast svm is uh something I mean in the end it's probably also a circuit uh but it's something that executes a dynamic program so a program that has a program counter has jumps branches uh memory and so on everything you would expect from a virtual machine um and yeah with with a ckvm you

can generate proofs for anything that uh that runs inside the programs and any any program um over the past couple of months there were many new ZK VMS created um I won't read out all of them uh but uh one thing we noticed is that they usually focus on a specific virtual machine so the input so they always tailored towards a specific virtual machine and usually they are even custom made and um especially this this customade part

uh it has one advantage and that is uh probably performance but um I don't know if you if you have looked at uh some custom build Z kvms they are usually quite difficult to audit because it's it's low code written in yeah some obscure language uh once you made the design decision it's very difficult to change that and uh in total it's lots of effort to to build it in the first place to maintain it later on and uh they are often uh very specific to the proof system that is used of course that again comes with performance benefits uh but uh if there's an a new proof system if a

new proof system comes around then it's difficult to change it over to that new system and uh of course anything you did in a custom ckvm is hard to you reuse in a different ckvm so uh if I may make that analogy currently we are at a stage where uh computer game programming was in the uh 1980s so the games are written for a specific machine usually in an assembly language that is also specific to that machine and when you want to Port over that game to a different uh type of computer then you usually have to rewrite the whole game or at least yeah large parts of the assembly that uh

that the game's written in and uh yeah powder wants to change that uh powder wants to be a llvm for ZK VM so A system that allows you to freely change change the front end freely change the back end you can write z kvms in highle languages uh like rust here and uh it has various layers of abstraction that allows you to run optimizations um and Analysis so yeah powder is a compiler stack that allows you to Define Z KVM so you

actually a virtual machine in the powder source code in the powder language you define the architect you define the instructions um it allows you to abstract away all the low-level stuff the lowle constraints the Prov complexity you can build your machines in a very modular way and you can run automated analysis on the powder source code like optimizations you can you can check for non-determinism you can do formal verification to check whether the implementation is correct cor and the the goal is uh for parter to make it easy to build test and audits their knowledge virtual machines so this is an overview of the

architecture of powder um on the left you see uh there are various input languages you could lose you you could use and on the right uh we currently support Halo 2 East dark and Supernova as backends and in the middle you see that there are kind of two layers the the powder assembly layer layer and the powder pill layer uh powder assembly is an assembly like language where you define your VM architecture in we will we will see an example later and um this gets compiled down to powder pill which is uh very similar or an extension to polygon hermis pill and

uh the the system allows you always to so the of course when you write stuff in pill it is probably much more optimized but the system allows you reach to to reach down to the level further to the level further down at any point so you can always use a more uh efficient implementation directly written and pill if you want and uh powder uh takes care of uh yeah automated witness generation for you it runs optimization stages and so on you just need to select the back end and uh it will do the rest of the job um so let's start with an example this is the the lowest level of powder powder

pill uh you might have seen that before because as I said it's very similar to polygon hermis pill uh we extended it in uh several ways for example we allow fixed columns to be uh directly specified in the language so you have this uh uh fixed column first which is one on the first row and and zero otherwise um and then you have two other columns X and Y which are witness columns and this so this is this this table View and uh powder with so you don't have to I mean yeah of course you don't have to write down these numbers but the the thing is that powder when when you run powder on this code it will automatically fill out

the table for you and for the First Column this is uh this is obvious you just uh evaluate the code here but for X and Y it actually looks at these constraints further down and will solve them for you automatically and we can take a quick look at the actual constraints so this uh example implements the Fibonacci series in the column y or X depending how you look at it and um the the first constraint here first * y - 1al 0 this needs to be uh equal to zero on all on every single row so uh and when we take a look at the first row we see that first is one in

that row so in order for this expression to be zero Yus 1 needs to be zero so y needs to be one so this is this is also how the automated Sol works so uh it can set y to to one and the same for X on the first row and uh for all the other rows these two upper constraints uh they are zero already just because first is zero so uh first is zero and then the the uh right Factor uh you can just ignore it and then uh if you take a look at the the two constraints at the bottom let's just ignore this uh one minus first Prime for now uh then the first

constraint says uh y Prime minus sorry x primeus y equal Z so this Prime symbol u means that you're refer refering not to the current row so but to the next row so what it says if we ignore the first part it says that X on the next row equals y on the current row so this is just just copies over the value from one row to the next so from y to X and if you look at the table this is also what happens right so the the value of x is always the same as the value of y in the previous row and uh the second constraint that is actually what what defines the Fibonacci series uh again if we if we ignore the first part it says y

on the next row equals x + y on the current row and this is uh just the definition of the Fibonacci series cool so this is how you define the the lowlevel constraints in the powder language and um let's now go up one level this is already powder assembly it defines a virtual machine so we also we already had a machine Fibonacci uh on this slide but the difference is that this is a a constraint machine it's not a program it's just a list of constraints that need to be true on all every single row and uh here we have a virtu machine which is which has uh a program counter

so um in powder when you start out with a to define a virtual machine it's completely empty it has no predefined instructions no predefined registers um you have to yeah uh declare or Define all of them explicitly so we started with a a register that is called PC and we have an annotation that says this is the program counter and then we have a general purpose register a and another register X which is an assignment register this is the the little arrow there um it's the distinction is not important for now and then we Define an instruction that is called assert zero and it takes an argument in X and then inside the instruction we have

constraints in the same language we've just seen so these are just the normal so this is just pill code and it says x equals z so whenever the assert zero instruction is active then X has to be zero and uh we also have a jump instruction which takes a an argument a label and uh here again we have uh PC Prime equals label so whenever the jump instruction is active then the PC on the next row is set to that label so that's the defition of a jump and that's how you uh go on defining your machine and then uh with this function keyword you can start writing the actual assembly

code for the machine uh this is a very simple machine it starts with assigning zero to the register a and then it asserts that um yeah this example doesn't make sense it should say assert z a of course and not assert z0 you've already noticed that and that's it uh so it always succeeds uh there's nothing to do but it's a nice uh tiny example and then so what about more complicated things what if you want to uh compute a hash for example I mean we could write down the hash in assembly code and just I mean we have we have jumps and stuff right so we

can just jump to a procedure that computes the hash but that would need that would mean that uh all the rows so it takes a lot of rows and they are all accounted for in this in this main machine instead you can define a specific instruction that computes the hash and um and you delegate it to a submachine so uh this in the second line we say here machine VM or and then hasher H which means that the that this machine has a reference to a submachine which is a hasher machine and the the hash instruction links to the hash operation in the hasher machine and then we Define the hasher machine and this is again a

constraint machine and we use uh pill constraints to define the hash and then uh so this is an abstraction depending on the back end it will turn it will be turned into a lookup or a recursive proof or whatever so uh whenever use the hash instruction in the main machine it will just take a single Row in the main machine and then do a lookup to the Submachine or a included proof or whatever you use so the idea is if you want uh very optimized operations that are expensive and run often you would Implement them

them in a specialized uh Submachine and the rest you would Implement in assembly um or even in a higher level language the the overall compilation process uh works that we we just look at all the virtual machines uh uh determine the links the connections and so on then we run an Optimizer so in in certain cases you can combine multiple uh instructions into a single Row for example um then we reduce all the virtual machines into constraint machines so this all this assembly code is translated into pill code and in the end everything is a

constraint machine so there know is registers and uh then we use yeah link mechanisms to to do the links using either lookup arguments or recursive proofs or whatever new mechanism will be developed in the future and then we also have another optimization stage on the low-level constraints um and now we can go even one level higher so this is yeah I don't know it's not the the core of powder but just as an example to validate the concept we implemented uh risk five front end for powder and uh this allows you to translate arbitrary no STD rust code here on the left to risk five in the

middle so this is a risk five assembly and then to uh powder assembly um yeah we we're not working on uh risk 5 binary code here but inste on assembly because it allows us to do some more optimizations and then the um the translation from risk 5 assembly to Powter assembly is more or less a local transformation so you see the the addition op code at the beginning um is translated into yeah just a plus plus uh and a a call to the rep function which wraps the value again into 32 bits uh

and the the store instructions are split into two instructions uh where we first assign the address and then execute the store um that's probably not a good idea but uh served as a proof of concept we will improve that later on um yeah and um so overall we managed to implement the the whole risk 532 architecture in just 300 lines of powder assembly codee and uh you can the rust code you saw on the left you just run powder on that uh po will automatically so it it translates that translates that down into lowlevel pill code and then will automatically synthesize witness

generation and the constraints and so on and uh it just works out of the box so it works with any rust no CD code and uh the cool thing is is we can now so we want to implement also valida for example as a different uh front end it's it is a it is an llvm backend so we can compare uh whether so compare compiling rust code through valida and then through powder with rust code through our risk five front end and then to powder um and um yeah we also have evm front in in preparation

um yeah and that's the the idea that you have uh one system where you can swap out frontends and backends and see what difference it makes um plans for the future uh our automated witness generation is quite slow which is expected because it has to solve constraints we want to allow uh external witness generators so that you can just run a program that provides the witnesses this has the advantage that has to be tailored towards your code so whenever you have to change when whenever you change your code you also have to change your witness generator um we want to support aggregation so um taking chunks of the VM execution

and uh generating proofs for that we want to further extend the polinomial language the polinomial constraint language we want to add add a proper type system for example and uh yeah add more backends and then uh we want to work towards a standard Library so that when you want to use a hash function a standard hash function you don't have to rewrite it yourself but instead you can use one from the standard library or you can also yeah I mean the idea idea is that one person writes it once and then we share the code um yeah the everything is open source uh you can find it on GitHub we have a website at p.org uh please try out the examples read the

documentation um yeah contact us if you have have any questions and yeah thanks for listening to my [Applause] talk do we have any questions for Christian oh oh I'll get you next okay um so a lot of this looks a lot similar like languages that are just for building circuits um so I I'm curious how where where you see the main differentiators to something like circum or vampire which does not care about building

VMS I mean the the main difference to circum is that we can build VMS with that so there's the whole Assembly Language on top of it that that that circum does not have um and vampire I think it also has a fixed instruction set doesn't it so I think that is that is one aspect for of powder that is is really cool that you can just really Define your own instruction set you say oh yeah I want to have a specified instruction just for this very weird multiplication operation or uh whatever you you you want to have so I mean the example I showed compiling from rust that of course uses a fixed instruction set but that is not the the I don't know the the main use case for

powder the main use case for powder is that you define your own instruction set okay thank you um just to add to that real quickly I think that vampire lives at like has a different purpose I think it is U trying to represent polinomial systems in an like proof system agnostic way so I I it might just live somewhere else in the stock yeah we're doing the same so um we're also compiling down to polinomial systems and our proof system agnostic yes but I think vampire then is this uh well anyway okay um are you or have you considered using

something like air script for defining the constraints um I mean escript is also is more in the Assembly Language area right and and not in the polinomial constraint air script is as far as I understand a tool to Define constraints for um stars it should be uh kind of compatible but uh where we don't want to mix languages too much so so instead you invent your own I mean we just took one that already existed and extended it right so okay fair enough thanks um do you have a plan to add llvm

IR as a front end I mean the thing is what what are you talking about when you say l VM I mean you have to specify an instruction set right and uh but it's already um like it's uh the intermediate representation that when you compile from C from R from with song or um many over languages um they compil down to lvm so you have addition subtractions and everything so you can generate proofs from this so the I think the only reason that makes llvm a little bit less suitable is that it has an unlimited number of of registers

um but actually we're trying to uh have an alternative implementation of risk five that does not use registers but instead uses a just a dedicated memory machine for the register so that could also work for L lvm that's true yeah awesome I have I have a question um I should probably start asking mine first so I don't constantly get the last question but um so you mentioned kind of the uh a use case for this is that you know you can Define your own VMS and you know there's the trade-off that you kind of trade off against this performance right so this is being the CEO of Alo we obviously have a very opinionated stack with regards to Leo what it compiles to

and the proof system it's very inflexible but the reason we did that was for performance reasons we found that for many circuits if you tried to increase like offer support for multiple backends that you would end up with much bigger circuits in many cases by having a compiler that was trying it basically remove optimization opportunities do you have any concrete comparison points or benchmarks between some kind of maybe very specific could even be circum or you know any any I guess like uh opinionated uh you know VM or opinionated language and compiler compared to like the circus that you guys could generate out of powder I guess just to kind of quantify what the performance trade-off could be I mean so it depends on what you mean by by

performance so we stop at the at the appr level right so Pro performance is is is not uh well but the circuit the size of the circuit yeah how many gates that's what I mean yeah the number of columns I mean the thing is it all depends on how you how you use powder right I mean if you it's a language right and uh we and as I said the risk five was just an example so I would not uh want to have any benchmarks on that so uh yeah it's hard to answer a question here got it okay cool yeah I just the only reason I ask it because I think for the people like me in the room who are obviously very focus on implementing something and it needs to be very performant at the for the end client who's generating proofs it would

be it would be interesting to see like how an architecture like this you know maybe uh is worse or better even I think depending on how a compiler is architected I mean this is the whole point of compilers right you can get like maybe optimizations that individual uh wouldn't have if they were writing circum I mean the thing is uh I did mention that in the talk but we have uh so what you can also do if even if you if you start from rust so if you do the the rust wire risk 5 pipeline uh we have a way where you can you declare a function in rust without a function body and then you say this is implemented with a low-level pill code machine so you can take all the the critical stuff like hash functions tic curve operations whatever and Implement

them at a very low level very much optimized and then the kind of the the business code of your of your machine you can read rest very cool uh let's give Christian oh wait we have another question in the back yeah this might be a stupid question so I apologize where do you think adoption is going to come for you and what sort of infrastructure Partners outside of the obvious do you think might find a lot of value in picking up powder and starting to play around with it I mean I I can't predict the future but I would assume that the first people to try out powder are researchers who want to try yeah to find some some

trade-offs and want to try out some stuff and then I hope at some point uh I mean it is probably difficult to convince uh existing ZK existing project that already have a zkm like uh your uh to switch our stack but uh I mean we will see so there's always new ckvm popping up I guess amazing um thank you all very much let's give Christian another hand thanks