Wizard: build your own P-IOP protocol in 15 min!

Transcription by ESO. Translation by — to you the tech we developed to develop the proof system of Linear. Linear actually uses many different proof systems for many different use cases. It is a complex system. What I'm going to present to you is the main one that we use for proving the execution, so concretely proving EVM execution.

So, I shall present myself. I'm Alexandre. I've been working in this space for seven years now, and been focused on cryptography for five years now. I've been working on INEA since the beginning, even doing research on roll-up even before that. So, yeah, just to talk a little bit about myself.

Okay, so I'd like to involve the audience a little bit. Who knows what a ZK-EVM is? All right, so that's a good half, a good third. So a ZK-EVM layer is a layer two solution which is whose purpose is to help Ethereum scalability. The idea is, instead of sending transactions on the Ethereum mainnet, you send them to a third party, Linear.

Linear runs an Ethereum virtual machine, will process the transaction. It will be processed separately from the mainnet. So the contracts that are deployed on mainnet are not the same, necessarily the same as the ones that are deployed on linear. The states are separated. But we can bridge between the two.

I'm not going to describe much more how we bridge between Ethereum and linear. But what is important to remember here is that we basically bundle the execution of many transactions and submit one proof at the end. We give you one number, every finalization finalizes on average 65,000 transactions at once. And since we are using snark proof systems, meaning they have a very short verifier time which is mostly independent from how many transactions are executed, that's how we get scalability. Verifying the final proof which is a Planck proof takes a few milliseconds but it's for 65,000 transactions.

So that's why it's much cheaper and that's how ZK EVMs can achieve much lower gas price. All right. So maybe a few words on ZKP and SNARK. ZKP is, I mean, usually we say ZKP but most of the time what we use in production are ZKPs, I mean, usually we say ZKP, but most of the time what we use in production are ZK argument of knowledge. And in order for a protocol to be a ZK argument of knowledge, it needs three properties.

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 the proof. Meaning, for instance, if you want to know that you proved the square root of some number, it should work for every number and not just one number. And the most important one is argument is knowledge soundness, or essentially computational knowledge soundness.

It is how you say that you know, that you prove that you know what you're proving you know. And so, as I mentioned earlier, we are building a ZKVM, but really the ZK is not about zero knowledge or hiding things it's really about proving that we know valid execution traces. We'll explain more on that later but especially we need more properties. We want the verification to be succinct, to be small and we want also the protocol to be non-interactive. It should be a single proof, a single message, and from that we should be capable of verifying a proof.

Okay, so let's apply all that to the EVM. The Ethereum virtual machine is a state machine on which we can execute and a transaction in GVM is like an instruction from the user of that virtual machine. It is specialized for running smart contracts. It has a lot and a lot of features that interact in a complex way between each other. 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 Ketchak hash function that every smart contract uses all the time, like it's free. It's really not free to prove. And so if we want to solve that problem, so of course we need to deal with the inherent complexity of the EVM, but we also need a proof system that is flexible enough to solve all the problems that we need to solve to execute the EVM. Concretely, in order to prove the EVM, we have traces of execution that are instantiated by polynomials. We call them colon in our framework.

And it could be summed up as a collection of errors that communicate with each other by sub-argument. And there are many different sub-arguments that are possible to use. We can have lookups. We can have projection queries. We also support variants of lookups that we call conditional lookups or fractional lookups, we can have projection queries, we also support variants of lookups that we call conditional lookups or fractional lookups.

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 linear zarythmetization. Okay, so in order to do that, we designed the wizard framework, which is the main gateway between describing the constraints to represent EVM and actually proving things. It has a very neat particularity in that in the wizard framework, you write protocols in an ideal model and you don't have to worry about how you're going to commit to things or which arguments you're going to use. You just say what you want and then you have a list of techniques like a menu which you apply to that protocol statement and it will create for you 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 complex protocols. Like if you take, for example, the GROSS-16 proof system, 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 NILP, and then it continues, and at the end you have a concrete 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 growth 16, and there is a growth 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 the whole protocol. In the case of linear, 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 add their own type of constraints, the framework will allow that without changing the core of it. All right. allow that without changing the core of it. Alright, so as I mentioned earlier, the proof system, 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... If it existed in reality, we would not need cryptography. So that does not mean that 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 multi-round fashion.

I mentioned at the beginning that we need non-interactivity, but the protocol sort this out using the Fiat-Shamir trick. It puts some limitation. It means that the verifier can only send random challenges to the prover, but that's a common limitation that every protocol has nowadays. It's very uncommon to be in a contrary situation. And so essentially, the prover can use the oracle by sending a big, large message to it, and the oracle will just remember and notify the verifier that, hey, the prover did this part of the work.

You can ask questions. So the verifier can ask questions, and the oracle responds to the question without needing to do any computation. It's like a godlike entity, and it is always honest. So you don't have to worry about him lying. So as I mentioned the prover, the verifier and the oracle can send messages to each other and here comes the first primitive of the framework which is what we call colons.

So colons can be of any sort. We have what we call committed column. Committed column means it is sent to the oracle. And basically being sent to the oracle means that the prover cannot change its mind about what was sent to the oracle. You can only send something once to the oracle.

Otherwise, you're cheating. And the protocol will always ensure that. But on top of that we have what we call pre-computed columns. So pre-computed columns, they can be of two types. They can be sent to the verifier or sent to the oracle and 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, for instance, the Planck circuit description, which is instantiated by several polynomials. We are going to see how we can implement Planck in 10 minutes. So I'm just putting myself forward a little bit.

You need those columns as part of the proving keys, and they describe the plumb 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 variants of column type. The columns also have a predefined size.

It can be one. It can be one, it has a power of two, it's due to a limitation, a current limitation in the framework, and they have a round assignment. And the round number is essentially describing at which round of interaction the column is associated by the prover. That's for the main part. And then, as I said, for some columns that are sent to the oracle, or for some groups of columns that are sent to the oracle, the verifier can ask questions about these columns to the oracle.

So that's what we call queries. It's a common term used in academia. If you know about FRI, they do random position opening queries, so that's what they mean when they mean query. In polynomial IOP protocol, there would be univariate openings. In our framework, query stands for at the same time constraints.

It 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 served as a constraint. And here we describe it as a query. And we also have open questions that are like polynomial opening, position opening, and so these expect a response from the oracle that is other than yes or no.

So we support many, many different types of queries. It can be lookups, it can be univariate evaluation, it can be inner product between several columns. So essentially, most of the folklore is there. And we implemented it because we needed it for the concrete implementation of vortex and linear arithmetization. All right.

So as I said, once you have a protocol description, 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 a concrete protocol that is secure in the standard model. So here is the base description that allows us to go from without IOP to polynomial IOP at the end. But in practice, this would not be sufficient. We would also need a polynomial commitment to turn this into a concrete protocol. So this part of the code does not describe how we do the polynomial commitment, but how we go to this point.

Okay, so now let's get onto a practical example. So here is the Planck constraints description. So we have a set of columns. Qs are describing a Planck circuit. Xa, Xb, XC are describing the witness.

And so usually we add another column on the right that is for the public inputs and that we are going to use. On top of that, Planck has some copy constraints which can be instantiated by a permutation argument, which I'm going to show you how to do. Okay, so let's implement Plonk. So as I mentioned, we need to define our protocol, then we can compile it, and after we can run it, so running the prover and verifying it. We can also automatically recurse it, but we are 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. Most of the prover stack of linear is using Gnark, and the linear prover is also implemented in Go, as it is also relying on Gnark's implementation.

So the defined function has this simple 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, columns, or so on. And we can also specify checks to be done by the verifier. So let's go into that. OK.

So here are the verifier. So let's go into there. Okay, so here are the columns description. So you can recognize the column that we saw at the beginning. So the queues column are for the circuit description.

They should be the same no matter what we try to prove. So they go into pre-computed. The XXBXC are commitment, they have to be sent to the oracle and PI for the public input is inserted as a proof object because it has to be revealed to the prover. It's a bit counterintuitive that we call that proof but proof means a message sent to the pro community. It's part of the proof.

Even if it's a nonsense from an academia perspective. And also a number of public inputs. Because the PI is, colon is larger than the actual number of public inputs, because every colon should have the same size. And also the value of the queue should be known beforehand, of course, because that's the circuit description. Okay.

So now we can declare the queries. So on your right you have a global constraint, which is an arithmetic expression that has to vanish on all the rows of every column that it's touching. We can recognize the equation of the Planck gate constraints at the beginning. And we have a fixed permutation, which is instantiated by some forced permutation that has the concatenation of XA, XB, XC invariant. And that's how Planck proves the copy constraints.

Then finally, 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 padded on the right with zeros. Okay. So now once we have that, we can compile that into an actual protocol. So here I added the part that converts the PIOP into a concrete protocol because I added the vortex.

compile, vortex being the polynomial commitment that we use. And now we just have to run it. So the only thing we need to specify is how concretely we are going to assign our columns. Because this is the only thing that is unknown at this stage, after reading the protocol description. So, yeah.

We just provide it and we assign it. It's four lines of code. And so, yeah. Now, so we have some things that allow us to write Plunk constraints manually. But I don't know if you have tried writing Plunk circuit by hand, but this is really difficult.

And it turns out that Gnark offers a very nice front-end to write circuits. So let's just write a wrapper of what we just wrote using Gnark so that we can use a Gnark circuit description. So 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 Fibonacci as a use case. So my circuit, you have two values, U0, U1 as input, and you want to have the 50th number of the Fibonacci sequence generated by U0 and U1. U0 and U1 being public parameters. So on your right, you have the circuit writing in NARC, so 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 wizard.prove, and it's going to generate a proof for you using vertex-threaded polynomial commitment, and you can verify that in one line. All right.

I have six seconds for the polynomial commitment, and you can verify that in one line. All right. I have six seconds for the future improvement, so we want to add more queries, and we think we can also remove the necessity to specify runs in the protocol as it should be inferred automatically. All right. That's it.

You can check out the code here. Amazing, Alexandre. You can check out the code here. Yeah. Amazing.

Thanks so much for the great introduction of Wizard. So a 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. And you can also vote. So if you have a question that you really want it to be answered, vote for them. So let's start with the top one.

Does WSIR support lookup tables? And can it be used to implement lookup tables based on CKVMs? Absolutely. So the way you would do it is, for instance, say, so what you can do, first of all, if you want to do a range check, so that's a big use case for lookup table, you already have a range query. So you just take one column and you say, I have this query that just enforces the whole column to be within bound, and that's all you do.

A second way, if you want to do more complicated range checks, like XOR, for instance, then you would have to specify three columns for your XOR. One column for the left side, the right side, and one for the result. And in this column, you put all the possibilities. So maybe say for 8 bits to 8 bits, you would have 2 to the 16th possibility. So you write down all of that in your table.

And then you create a lookup constraint between this table and a triplet of columns for which you want to enforce XOR constraint. And you can also add a conditional lookups. You can have a fourth column that contains zeros or one and that activates the XOR 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 row corresponds to each kind of gate?

So when you generate a global constraint this is essentially what is your custom gate then it's going to apply over everything but the wizard framework is more abstract than this. Essentially, there is a general technique to do it, which is to say that you add a selectors column that says which constraint is going to apply for each, and you have some product of your constraints custom gate expression multiplied by an indicative that asks 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 gate. Actually, that's what they do all the time 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? So there is a separate way you can do recursion. So we do it inside of the Wizard at the same time and outside. The first way, we have a compilation step that is called self-recursion that usually goes just after vertex.

The text of vertex proof and re-arithmetize it. And we can do proofs of that again, and we repeat, and we can shrink the proof. That's because vertex, as a single polynomial commitment, has a square root, very fair time. But applying log-login application of self-recursion, you get constant size proof. Great.

And the last question that we have in the queue, at least for now, is that it's great that you can define an ideal protocol programmatically, and it seems that that does make it easy. Does that make it easy or possible to support automated formal verification or UC proofs of security? I'm not too sure what it would entail exactly to formally verify. So we could formally verify 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 to do it. I don't know and I can't tell you how to make it easy but it would be a great use case I agree it would be great maybe after that conversation