Verify EVM execution in the pessimistic proof

Transcript

Okay. So, as I mentioned at the very beginning, uh this is kind of a long talk, but we already missed four minutes. So, I will try to go a little bit fast in order to finish the full presentation. H my name is Carlos Natana. I work at Polygon. I'm the protocol team lead. And today my presentation is about how to prefy EBM execution inside the pessimistic proof. In order to do that the presentation is divided into three different stages. The first one is kind of an introduction of what is basically the pessimistic proof. The second one is the uh new design that we implement in order to prefy an EBM transaction. And the third one is the next steps. uh most probably I will not have time to read those slides but are

just two slides and basically the next step is uh some uh improvement features that uh we want to add into the pessimistic proof in order to improve it. So uh first of all some introduction some key components correct concepts on the pessimistic proofs and the first of all is why we need the pessimistic proof. We need the pessimistic proof because we have a single uh smart contract on layer one which is called bridge lex y act layer lex y bridge whatsoever and basically this bridge has all the liquidity across all the chains that are connected to the act layer and what we want is that uh single layer to chain cannot spend the assets of other

chains. So it means that the chains must not trust other chains and how we do that quite simple. It's kind of a ledger. So in the pessimistic group we track all the token balances that are in a chain and this basically means that those token balances could not be negative, could not be um lower than zero. So it basically means that a chain cannot spend what it doesn't have. So we're going to check more in details how this works. Basically in the pessimistic proof there are two key actions. One action is the bridge and the second important action is the imported bridge.

A bridge basically means that some tokens are leaving the chain and then an imported bridge it means that some tokens are entering the chain. So it's quite a straightforward that you cannot do a bridge before an important bridge happens because you will not have on the ledger that I mentioned before those tokens over there. And how we track this kind of ledger as usually in the zon ecosystem we are using a Merkel tree. This tree we call it local valance tree and this local balance tree is basically a ledger. So it tracks all the tokens balances that the chain has. And as I mentioned, every time that there is a bridge, uh there is

some substraction on tokens on this ledger. And every time that there is an imported bridge, there are there is some addition inside this local balance tree. Besides this Merkel tree structure, we have more Merkel trees and those Merkel trees are basically the local exit tree and the nullifier tree. The nullifier tree is quite a is quite a straightforward and is basically is to avoid double spending. Every time that there is an imported bridge we are al we are going to mark it as that it has been claimed it has been spent in order to avoid double spending and the local exit tree it basically it tracks all the breaches that has been done in a chain later on this local

exist tree will be shared with other layer tools so other layers tools can claim the breaches that has been done on on your chain but it's not enough with the local exit tree. That's why we have the local the global exit tree. The global exit route. And basically the global exit tree what it does is it gathers all the local exit trees. It's basically it's a merkel tree. So it's a root. It gathers all the local exit trees and it kind of aggregates them. It joins all of them together. And then we have another merkel tree which is the layer one info tree which gather all the historic of global exit global exit trees. It means

that with a single 32 bytes value the layer 1 info tree the root of that Merkel tree uh with those 32 values a chain can access all the bridges that has been done in all the chains on the act layer and very convenient when you want to share bridges among layer two to layer two layer one to layer two or whatever. Okay, let's see the design of the pessimistic proof the the second version that we did while bike ago and at the very end the pessimistic proof it's a zero knowledge circuit so it's it's a program basically that has some constraints and you can think about uh the pessimistic proof and an EVM state transition proof so you have some

initial state you have some transactions and when you apply those transactions in the initial state you have a final final state on the AVM you have an initial patricia Merkel tree some transactions you apply to them and you have a final state of the matricia Merkel tree. So here it happens exactly the same. You have a initial state which is defined by the trees that I show before and those three result the local exit tree the local balance tree and the nullifier tree and then you apply some transactions. Those transactions in the context of the pessimistic are basically the bridges and the imported bridges I explained before. And then you will get a new state of the pessimistic.

Okay let's see what the circuit uh does. Well, I would say this is quite straightforward, but then on on the circuit uh there are three different stages. We apply the brides, we apply the imported bridges and then we verify ICDS tool. This will be very important in the upcoming version. When we apply the breaches, what we are doing is to move forward on the pessimistic state transition. And every time that we apply a bridges as I mentioned before we are adding one leaf to the local exit tree. And also at the same time h as I mentioned before every time that we apply a bridge it means that we are subtracting some value from

the local balance tree. And here for this is just an example that on the old pessimistic uh on the old local balance tree we have 10 ether then we subtract one ether which is quite a straightforward example of a bridge of one ether. And then the second stage is that we apply imported bridges. Those imported bridges affects as I mentioned before on the local banks tree and the nullifier tree. So first of all uh we need to modify the balance of that given token. For example, in this example is 66 pole. We are subtracting uh we are adding uh that balance into the local manry and on the nullifier route we are basically set it kind of as claim it.

And let's go for the third one. uh in a layer two if you have an initial state and you want to go to the final state who can basically propose the transaction as that availability in order to move from the initial to the final state. So this is basically the sequencer and here it kind of happens the same who is able to move forward on the state transition on the pessimistic proof and we have some kind somehow this is a a sequencer. So basically it's a sequel is basically an address that the chain can define on layer one and and basically this address uh the signature of this address will be checked on the circuit and of course it needs to match

with the one that has been set on layer one. That's why we have defined uh super simple approach which is consensus type and address. Consensus type means that in the circuit we will do an easy recover and in order to forward some forward those values into the circuit we just uh hash it and then we make what we call the action hash. This is on layer one. Exactly the same thing we will be do on the circuit. And this is basically a public input of the pessimistic proof and they need to match otherwise the proof will not be correct.

Okay. So what happens what happened with such an approach? Uh this approach is not enough modular. What does it means is that imagine that a chain does not want to use an easy recover and IDCA signature in order to move forward on the pessimistic transition. Imagine that a chain uh wants to add another signature scheme or a multis or whatsoever. It means that inside the pessimistic proof we will need to add some kind of new code with a new consensus type in order to allow that chain to work. It means that basically the chain cannot choose whatever the chain wants in order to move from the initial state to the final state. And this is problematic because basically

the chain depends on us. No. we provide in in this case an ECDCA and maybe we will add another concentr the chain needs to choose between one of them that's not enough modular and does not give freedom to the chains so the version three tries to um tries to give some sovereignty to the chains and and basically the version three what tries to do is to it introduce a new concept which is a generic acting And basically what we do is we verify a zero knowledge proof again inside a zero knowledge proof and basically this gives full freedom uh to the chains we are

using basically SP1 and it also the new design also has backwards compatibility with version two we'll see in the following slides and this is the version three I would say um summary overview of the circuit as you can notice the public input are exactly the same but we only have one addition here which is uh dealing with consensus type equal to one and instead of doing here we are doing SDCA here we can do I don't know multisc another uh signature scheme here we are verifying as your knowledge proof and by verifying as knowledge proof we are saying that the chain can verify whatever zero knowledge proof that the chain wants so

totally freedom to the chain and how we can achieve We introduce a new consensus type and we are hashing now two fields the action be key and the action params and basically the smart contract builds the new action hash which is the key of the consensus type action key and action params here the nomenclatur is very similar to the one that is using sp1 because as I mentioned we are using sp1 uh verifier and the good thing about that is that inside we will see later on but inside the Ike chain params are the public's inputs that the chain wants to verify on its general knowledge proof and the

pessimistic proof is fully agnostic to those parameters. So it means that the the pessimistic proof does not care about what the chain is going to be verified. And we will see later on as well the action bey basically defines the circuit that the the chain wants to verify. Okay. And this is kind of uh the code uh inside the pessimistic circuit as I mentioned if B was compatible. So if consensus type equals to zero, this code is exactly the same as the version two.

But if consensus type is equal to one, what we are doing is to building the input for this zero knowledge proof and those are the public inputs which is the SHA of the public's input of theistic concordated with the act params and then we are verifying a zero knowledge proof and basically if we use one library in Ras which is SP1.y H we need to provide the public input and the action BK. The action BK defines the circuit. This is very important. What is inside as I mentioned before what is inside the action params the pessimistic proof does not care at all. We will see later on.

And then the circuit of course uh builds the action hash and the hash is a public input of the pessimistic role. So we need to match with the one that the smart contract uh has built. Okay, let's get now we saw how we change the pessimistic proof and now um we cannot just only verify an ECDS signature but we can also verify a zero knowledge proof. Okay, let's get inside that zero knowledge proof. As I mentioned before in the pessimistic secret we are doing SP1.verify verify and one of the parameters is the action B key and the action B key as I mentioned before it defines the program that the chain needs to verify and this program we call it action params and

let's see how it looks like when we want to verify an EBM state transition this is the circuit of the action programs and the publics are built by the pessimistic are the ones that I show you before so it's the public of the PP plus action params and what this action program does it has two different stages. The first stage is to verify an EBM state transition. And I would say that the chain can verify the this state transition as the chain wants. We will see how. And also we have the bridge constraints. The bridge constraints are very important because uh the bridge constraints assures that all the bridges and important bridges that happen on your chain matches with the ones that

the chain is providing to the pessimistic. they need to match. Okay. So what happens the actions that happens in your chain matches the one that the actions that you provide to the pessimistic proof. So let's see one example how to verify this EVM state transition on the action program and uh I would say that the code is not uh super complex but basically and this is the action program and in the action program now inside the action program now we provide all the necessary public inputs in order to verify the ZVM state transition. This is not the pessimistic proof is the the circuit inside the pessimistic proof.

Uh here of course we need to rebuild the public's inputs in order to match the public's inputs that the pessimistic proof have computed and basically inside the action program what we do is verifying another zero knowledge proof and this zero knowledge proof basically verifies an EVM state transition and those are the bridge constraints. uh in order uh the bridge constraints basically are divided in three different uh main points. The first one is to prove that all global exits that we insert on layer two needs to exist on layer one. And in order to do that we just do a hash chain of global exit

roots. Um and basically this hash chain is stored on the smart contract at a specific smart contract at a specific storage slot. So with just two storage proof we can read the initial of the hashing and the final of the hashing. If we have the initial value and the final value the the prover must to provide all the intermediate value in order to reveal that hing and then we can get kind of an array of local exit roots and that array of local exit roots we can prove it again the layer one info3. Also the second point is the new local exit uh the new local exit route. If we take the new state route at a given smart contract at a given stretch slot, we can use anes proof in order to read that specific structure which is the new local and this new needs to match with

the one that is defined on the pessimistic route. And then we do exactly the same with the imported brides and the imported brides work exactly the same as the global exit route. uh we just do a hash chain with two storage proofs and the most um I would say important here is this assert here and this assert here. Those asserts as I mentioned before is asserting that what happens on the pessimistic proof is exactly the same as what happens on a layer two. If you kind of delete those assairs, uh a chain can do whatever they want on the state transition on the ABM state transition and kind of cheat the pessimistic proof. So those asserts are very important

and this is how the proof schema looks like uh in the final I would say flow. As I mentioned before, we use opisin in order to verify this ZVM is the transition. In the opioxin at the very first stage they create um a proofs that basically validates some block range from from block one to block 10 and so on. Also the opisin stack creates another uh proof that basically aggregates all block range. Does this aggregated proof is verified in inside the action proof and then the action proof is verified inside the pessimistic proof and then the pessimistic proof is verified on

layer one. It's an kind of an inception of zero knowledge proofs and okay let's see the next steps as I mentioned before this is the act program and imagine that a chain does not want to verify its EVM state transition using uh opinion stack but instead they want to verify with a totally different consensus. The thing is that we can kind of reuse almost all the action program and instead of verifying a zero knowledge proof here, we can just verify a proof of work. We can verify a proof of stake or whatever consensus do we want.

It means that basically reusing the same circuit and changing some line of code, we can h give more freedom, more sovereign to the layer to change. And then uh also uh as I mentioned before we are using SP1 on the pessimistic proof in order to and and SP1 is the proving system that we are using. Uh so the chain I would say must use SP1 in order to verify its acting program and we want also in the future to add more proving system. So the chain is not just only fully freedom to choose state transition but also it can choose the proving system that they use. So we

can for example we are using now uh SP1 we can also use the we can use drix zero or whatever other proving system uh I did quite fast sorry for that uh but I think I'm in time. I'm in time. We don't have time. Well, we don't have time for questions, but if you have any questions, I will be out. So, please uh feel free to reach me and ask me whatever question you have. Thank you very much. [Applause]