Wizard: build your own P-IOP protocol in 15 min! by Alexandre Belling | Devcon SEA

[Music] PA please um uh so hello everybody uh so today I'm going to present to you uh the tech we developed to uh develop the proof system of linear linear actually use many many different proof systems for many different use cases it's it is a complex system what I'm going to present to you is uh the one the main one that we use for proving the execution so concretely proving evm execution so uh I should present myself I'm alexand uh I've been working in this space for seven years now uh and been focused on cryptography for five years now uh I've been working on Linea since the beginning even and doing research and roll up even before that uh so yeah just to talk a little bit about myself okay so uh uh I'd like to involve the audience a little bit who knows uh What uh zvk evm is right so that's a good half a good third um so a zvm layer is uh a layer two solution uh which is whose purpose is to help ethereum scalability the idea is instead of sending transactions on the ethereum main net you send them to a certain party linear linear runs uh an ethereum virtual machine will process the transaction it will be processed separately from the main net so the contracts that are deployed on Main net are not the same necessarily the same as the on that are deployed on linear the state are separated uh but we can bridge between the two I'm not going to describe much more how we bridge between ethereum and iner uh but what is uh important to uh remember here is that we basically bundle the execution of many transaction and submit one proof at the end we give you one number uh every finalization finalizes on average 65,000 transaction at once uh and since uh we are using snack proof systems meaning they have a very short very time which is mostly independent from how many transactions are executed that's how we get scalability verifying the final proof which is a PL proof TX uh a few milliseconds but it's for 65,000 transaction so that's why it's much cheaper and that's how uh the kvms can achieve a much lower gas price all right uh so maybe a few word uh on um on zkp and snar zkps uh I mean usually we say zkp but most of the time what we use in production are ZK argument of knowledge uh and in order to for a protocol to be uh Z key argument of knowledge it needs three property you need zero knowledge zero knowledge means that the proof does not reveal more than what it should reveal you need to have completeness meaning that if you want to prove something that is true you should always be capable of generating proof meaning for instance if you want to know that you prove the square root of some number it should work for every number and not just your favor just one number and the most important one is uh argument is knowledge sness or essentially computational knowledge sness it is how you say that you know that you prove that you know uh what you're proving you know um and so as I mentioned earlier uh we are building a ZK VM but really the ZK is not it's not about zero knowledge or hiding things it's really about proving that we know valid execution traces we explain more on that later uh but especially we need more properties we want the verification to be suent to be small and we want uh also the verification the protocol to be non interactive it should be a single proof a single message and from that we should be capable of verifying uh approve okay so let's apply all that to uh the evm uh the etherum virtual machine is a state machine uh you on which we can execute code uh and a transaction in zvm is like an instruction from the user uh of that virtual machine uh it has a lot it is specialized for running smart contract it has a lot and a lot of features and that interact in a complex way between each other and uh and not every computation that are easy to do on the evm are necessarily easy to prove so for instance I'm thinking about the Kash function that very smart contract uses all the time like it's free it's really not free to prove um and and so if we want to solve that problem uh so of course we need to deal with the inent complexity of the evm but we so need a proof system that is flexible enough to solve all the problem that we need to solve to execute the evm concretely um in order to prove the evm we have traces of execution that are instantiated by polinomial we call them colon in our framework uh and it could be summed up as a collection of airs that communicate with each other by sub argument and there are many different sub argument that are possible to use we can have lookups we can have projection queries uh we also support variance of lookups that we call conditional lookup or fractional lookups um and so in order to make this work we need a proof system that is really flexible and can deal with all the polymorphism that is inherent to proving uh linear arithmetization okay so in order to do that we designed uh the with framework which is is uh the main uh um the main gateway between describing the constraints to represent evm and actually proving things uh it has a very neat particularity is that in the wiard framework you work you um write protocols in an ideal model and you don't have to worry about how you're going to commit to things or how which argument you're going to you just say what you want and then you have a list of technique like a menu uh which you apply to that uh protocol statement and it will create for you uh a proof system as complicated as you need it to be and so that's perfect for us it turns out that this is how in Academia they describe uh complex protocol like if you take for example uh the grow 16 uh proof system uh if you had a look at the paper before you would see that they say okay so this is the constraint system at the beginning then we do something that is called qap and then we do something that is called NP and then uh in continuous and at the end you have a conrete proof system which is a gross 16 proof system but that does not translate into the implementation people just take the final protocol at the end that you apply after every step of compilation of grow 16 and and there is a grow 16 implementation so what we do is that we actually Implement every possible step so that this step can be reused for other proof systems and we don't have to really mentally work out with the work the whole protocol in the case of Lina it would just be impossible and on top of that we made it in such a way that if anybody wants to add their own compilers or do their own tweak or are their own type of constraints uh the framework will allow that without changing the core of it all right so as I mentioned earlier the proof system uh the protocol that you are going to construct you have to describe it in an ideal model and this ideal model involves what we call the wizard Oracle the wizard Oracle is from the point of view of the protocol designer a trusted third party it knows everything it remembers everything it does computation for free it is always honest it's like something you really uh if we if it existed in reality we would not need cryptography uh so that does not mean that uh what we build will not be secure it just means that the Oracle will concretely be instantiated by something else in the future as we compile the protocol so the protocol can also be described in a multiun fashion I mentioned at the beginning that we need non interactivity but the protocols s this out using the fat Shamir uh the fet Shamir trick uh it put some limitation it means that the verifier can only send random challenges to the prover but that's a common limitation that every protocol have nowaday it's very uncommon to be in a contrary situation and so essentially the prover can use the Oracle by sending big large message to it and the Oracle will just remember and notify the verifier that hey uh the pr did is part of the work you can ask question and so the verifier can ask questions and the Oracle respond to the question without needing to do any computation it's like a god-like entity uh and it is always honest so you don't have to worry about him lying so uh as I mentioned the prover the verifier and the orle can send messages to each other uh and here comes the first primitive of the framework which is what we call uh colons so colons can be of any sort we have what we call commitment committed colon committed colon means means it is sent to the Oracle uh and basically being sent to the Oracle means uh that the prover cannot change its mind about what was sent to the orle you can only send something once to the orle otherwise you're cheating uh and the protocol will always ensure that uh but on top of that we have what we call pre-computed colon so precomputed colons are they can be of two types they can be sent to the verifier or sent to the and uh they are known beforehand so that's something that is part of the protocol description actually they always have the same values you can think of for instance the plun uh circuit description which is instantiated by several polinomial we're going to see how we can Implement plun in 10 minute uh so I'm just uh pting myself forward a little bit uh you need uh those colons to uh as part of the proving keys and they describe the plum circuits and on top of that you can send proofs and proofs means a message that is sent directly to the verifier and there are other types actually we have eight types of different variant of colon type so col also have a predefined size can be one it has b a power of two it's due to a limitation uh aurent limitation in the framework uh and they have a r assignment and the r uh number is essentially describing at which round of interaction the colon is sated by the prover so that's for the main part um and then as I said uh so for some colon that are sent to the Oracle or for some groups of colons that are sent to the Oracle the verifier can ask questions about these colons to the Oracle so that's what we call queries it's the common term used in Academia uh if you know about fries they do uh random position opening query so that's what they mean when they mean query in polinomial IOP protocol that would be univariate openings in our framework we query stands for at the same time constraints so that would be questions that have a yes or no answer like is this value the square of this other value the answer can always be yes or no most of the time it is sough as a constraint uh and here we describe it as a query and and so we and we also have open questions that are like polinomial opening position opening uh and so these have uh expect a response for from the orle that is other than yes or no um so we support many many different types of query it can be lcaps it can be uh it can be univarate evaluation it can be uh inner product between several colons so essentially uh most of the folklore is there and because and we implemented it because we needed it for the concrete implementation of Vortex and linear arithmetization all right uh so as I said once you have a protocol description uh the only thing you need to do is to describe how you want to go from this description in an Ideal World with ideal Oracle into concrete protocol that is secure in the standard model uh so here is the base uh description that allow us to go from uh without IOP to polinomial IOP at the end uh but in practice this would not be sufficient we would also need a polinomial commitment to turn this into a concrete protocol uh so in this part of the code does not describe how we do the pomal commitment but how we go to this point um okay okay so now let's get onto a practical example uh so here is uh the plun uh constraints um description so we have a set of colums Q's are describing a PL circuit x a XB XC are describing the witness uh and also usually we add another colon on the right that is for the public inputs and that we are going to use on top of that plun has some copy constraints uh which are can be instantiated by um a permutation argument which I'm going to show you how to do okay so let's Implement plun uh so as I mentioned we need to Define our protocol then we can compile it and after we can run run it so running the prover and verifying it we can also recurse automatically recurse it but we're not going to cover that today all right okay so first of all defining the protocol this is done by specifying a function so the whole framework is in go uh most of the prover stack of linear is using KN and the linear prover is also implemented Ino as it is also relying on GAR implementation so uh the defined function uh has this simple uh signature and the Builder is an object that is going to store everything we said to declare an entity in the protocol so either queries colums or so on and we can also specify checks to be done by the verifier so let's go into there okay so here are the colon uh description uh so you can recognize uh the plun uh colon that we saw at the beginning uh so the cu's colon are for the circuit description they should be the same no matter what we try to prove so they go into precomputed uh the XX bxc are a commitment have to be sent to the Oracle and Pi the public input is inserted as a proof object because it has to be revealed to the prover so it's a bit cont inuitive that we call that proof but proof means a message sent to the pr it is part of the proof even if it's a nonsense from an Academia perspective and also a number of public inputs uh because the pi is po colon is larger than the actual number of public input is because every colon should have the same size so and that's the value of the CU should be known beforehand of course because of the circuit description okay so now we can declare the queries uh so on your right you have the a global constraint which is an arithmetic expression that has to vanish uh on the all the rows of every colon that is touching we can recognize the equation of the pl gate constraint at the beginning and we have a fixed permut which is instantiated by some forc permutation that has the concatenation of XA xbxc uh invariant and that's how PL proves uh the copy constraints uh then finally uh we need to add a verifier check this is to ensure that the pi that is sent to the verifier is well formed and that it should be paded on the right with zeros okay uh so now once we have that we can compile that into an actual protocol so here I added the part that convert uh the piop into uh a concrete protocol because I added the vortex. compile Vortex being the prial commitment that we use and now uh we just have to run it uh so the only thing we need to specify is how concretely uh we are going to assign uh our colons because this is the only thing that is unknown at this stage after reading the protocol description uh so yeah we just provide it and we assign it it's for lines of code uh and so yeah now so we have some things that allow us to write PL constraints manually uh but write I don't know if you have tried writing a PL Circuit by hand but it is really difficult uh and it turns out that garx offers a very nice front end to WR circuit so let's just write a wrapper of what we just root uh using Gar so that we can use a gar circuit description so I I did the implementation it was a bit longer than 100 lines but it was essentially a few automated stuff okay so let's do a circuit so let's use uh Fibonacci as a use case uh so my circuit you have two values U U1 as input and you want to have the 50th number number of the Fibonacci sequence generated by U and U1 U and U1 being public parameters uh so on your right you have uh the circuit writing in KN you can see that it's fairly easy and much simpler than writing a circuit by hand and then we just have to run it and that's it you just create your proof function that is explaining how to assign the colon you run with. proof and is going to generate a proof for you using vertex of the polinomial commitment and you can verify that in one line all right I have six seconds for the uh future Improvement so we want to add more queries and we think we can also remove the necessity for runs in to specify runs in the protocol as it should be inferred automatically right that's it you can check out the code here yeah amazing alexand thanks so much for for the great introduction of wizard so uh reminder that if you scan the QR code you will attend the session and you can ask questions and you can also claim an nft so and you can also vote so if you have a question that you really want it to be answered uh vote for them so let's start with the top one uh does wizard support local tables and can it be used to implement uh local tables based on ckvm uh absolutely so uh the way you would do it is for instance say um so what you can do first of all if you want to do range checks so that's a big use case for lookup table you already have a range query so you just take one colon and you say I have this query that just enforce the whole colon to be within Bond and that's all you do uh a second way if you want to do more complicated R checks likeor for instance then you would have to specify three colons for your exor one colon for the left side the hand the right side and one for the result and in this colon you put all the possible uh all the possib ities uh so maybe say for 8 Bits to 8 Bits you would have a Col you would have two to the 16 possibility so you write down all of that in your table and then you create a lookup constraints between this table and a tri plate of color for which you want to enforce exor uh uh constraint and you can also add a conditional lookups you can have a force colon that say that contains zeros or one and that activate the the exort constraints or not great thanks for the answer the next question is can you create different custom Gates and at which instance do you decide which roow corresponds to each kind of gate um so when you generate a global constraint this is essentially what is your custom gate uh then it's going to apply over everything um but the wiard framework is more abstract than this uh essentially there is a general technique to do it uh which which is to say that you add a selectors colon that says which constraint is going to apply uh for each and you have a some product of your constraint custom Gates expression multiplied by uh an indicative that ask whether this constraint is active here or not and you would merge everything into a single Global constraint in the end so yes you could Implement custom gaug actually that's uh what they do all the time uh when they specify the evm great the next question is about recursion so is recursion something that would be implemented in Wizard or would it be separately like a commitment uh so there is separate where you can do a recursion uh so we do it inside of the wiard at at the same time and outside uh so the first way we have a compilation steps that is called self recur that usually goes just after Vortex that text a Vortex proof and rear matize it and we can do proofs of that again and we repeat and we can shrink the proof that's because vertex uh as a single polinomial commitment has a square root verifier time but applying log login application of self retion you get constant size proof great and the last question that we have in the queue at least for now is uh that it's great that you can define an ideal protocol programmatically and it seems that that does make it easy would would does that make it easy or possible to support automated formal verif ification or you see proofs of security um so I'm not too sure what it would entail exactly to formally verify so we could formally verify uh like the standard set of compilers that we have I think this is at least a necessity but then there is a protocol description it should be formally verified this I don't know how how to do it I don't know and I can't tell you how to make it easy but that would be a great use case I agree yeah it will be great maybe after have the conversation