Etheorem: Lean 4 Consensus-Spec Proofs

Transcript

[music] for being here. Excited to hear about Ethereum. Uh go for it. Hi everyone, I'm Ivan. This is Raj. Uh and we're presenting our work on Ethereum. Uh the whole project is about uh formalification of consensus layer. So we have uh almost complete uh [snorts] uh fully faithful to the model to the original spec uh lean model. Uh [snorts] uh our goal is like basically make it uh back compatible to like a line. Uh and we have like proofs from very basic variance to like very high level things.

Um so like uh basically from uh original Python uh spec we uh we make executable model um and we also verify it with a field test vectors but that's not enough. We must verify that every impossible situation uh like absolutely every input is done exactly the same way as in the original spec. And based on that we um um um make different kinds of proof like different level of complexity um uh like it's from like basic uh things like lack of integral overflows to like very high level facts that like in

fossil u u main property is met if uh a builder emits transaction without like been some V mission. Uh and uh if allations are met then yeah they will lose their bit and um it will uh by ep finalize uh on the empty uh like it should uh like apart from the proofs uh we still updating because the spec is alive uh we are repeating to uh every new release uh so it's currently the latest uh beta form uh and keeping it like that still a lot of effort And it's still ongoing effort

to make it actually back compatible. Uh like the possible situation that don't cover uh we still need to made it completely faithful to the original script which is uh surprisingly big item. um uh like uh uh other big results like uh proven wise um I did make a proof for uh milk branch completeness uh which is like used in several places in the spec u lots of environments including like balances arithmetic uh time arithmetic like stuff um

stuff stuff uh and like yeah the biggest item we still been in process of measuring that st it's like five request I think we are on number three or something like that [laughter] uh but um uh that's what I mentioned the fossil proof uh uh the basic claim is very simple to state uh and the main statement is super short but uh uh prerequisites like proof machinery and uh other things they took like lots of code uh lots I don't remember exact details but tens of thousands lines uh uh we still be integrating that uh and like we just went to the so I won't be detailing the protocol itself I think

we all know how it's supposed to work um but I said like u essential claim is super simple it's like one line uh proving that is like [clears throat] tens of thousands of codes of code Uh and it's like proven from uh simple result over one block one node uh to uh uh like to finality by end of epoch uh um it cannot falize unless we have uh three fives of doing the other way for some reason. uh and if they honest they should not do that. Uh with some assumptions

conditions uh it means that uh if transactions emitted and if somehow it finalizes u on the full on the empty somebody [snorts] will get slashed. It's like completely proved u uh all inputs are mapped to uh outcomes and uh with some things still being left in uh as hypothesis to be honest. Uh so it's not completely uh covering a few of the prequisites. Um there is still some ongoing work to be done to be honest there. But uh uh those things are lawful. Um uh mean uh honest clients do follow those rules. Uh we just need to

prove that uh like uh part of proof machinery uh we need to do um a proof for a safety for finality to prove the finality uh thingy. Um and uh I shake shaking the projector. [laughter] Um yep uh shuffle proof. Uh it was also uh pretty fun. Uh like essentially just proving that um uh shuffle is also always a various permutation of the data set and that uh committition honestly. Uh there are no

repetitions. Uh nobody skips essentially. Uh that um uh basically covers uh our main uh proof results and uh just like highlights of what is planned as uh [snorts] uh next items uh which uh we are planning to work on. Uh we do plan to make uh like almost complete uh client. Uh we are currently hiking li2p. Uh we're planning to add some database and um some things in the model needs optimization uh initization but um we plan to try to make it full client that can follow crypto devet and um uh

actually be verified end to end um uh we can use like as I mentioned uh our model and proofs to verify um other clients especially Ras based uh uh especially really easy to do because uh like yeah we can use NES to translate Ras code into lin um and um this lighthouse is already being used hopefully we'll expand uh prove the implementation using my fal theorem and um [snorts] uh like yeah uh we can do vector generation uh it's one of the things

we're uh trying to to [snorts] uh we do want more proofs. Uh we still not uh close to 100% proof coverage uh like for example miracle branch hence can be used to prove part of lighthouse sorry uh uh light lensing protocol uh and we are not too close to that. We need to finish model on that part and do improve machinery. uh and uh uh repeating u like following the last spec changes uh is ongoing efforts we are trying to do some kind of tooling [snorts] uh to both foration and also to have moreic

results uh because uh it's currently uh tools process we basically use AI to make updates with human control in the loop but um uh tooling would be nice uh which cars for Python for technical reasons. Um uh and that covers my part. Uh I will give it over to Raj to uh talk about uh CZ proof. >> Thanks. Uh hi uh I'm Raj. So I basically uh worked on the layer underneath the consensus objects uh which is Seline. Uh basically Siseline is a our uh Ethereum SSG library. So uh like so basically like uh my main

contribution was to uh extending the uh three serialization result to more of the type the like the consensus specifications. So like uh which mean like know like the uh round trip which like you guys already know about this uh like decoding and encoding uh returns the original value and like the two value with the same encoding must be equal and uh uh also the like encoding like stays uh with their uh schema bound and also like the mostly the results uh quantify over supported values and like rather than just the uh examples. So like uh yep. So round trip and

injectivity like retain and uh encoding size condition for that. So uh so next one uh this is the like basically uh most uh kind of uh difficult case for us like which is a mix field containers. So like where like and also the collections like where every element have the variable size and where the work and coding length carries the uh table of four offsets and so also like we found a bug in uh while doing the uh work. So like for a variable size uh like the old formula was for uh like old bound was like uh six bound uh six bytes. So like uh which calculate the

payload but uh uh emitted the offset table and like the here the outer list like uh allows the uh three elements uh also like the for the like the inner element we have the only uh two bytes. So uh the old bound is uh six byt now like one let's take now uh one by two by and elements. So like that give us three playload by but plus the 12 offset bite. So which is uh totally in 15 in the total. So basically the valid encoding like exceeds the old bound. So uh we worked on that and found that like the uh valid encoding must be uh and the

correct bound must be like the uh 18 uh bytes. So like it was the bound like like no like it was the bound that was the wrong but not that the like proof attempt like so we have to like uh go to expose like what's uh goes wrong there. So like uh once the generary cases were like proved so I wanted the results to be usable and uh for the real consensus specifications. So like the theorem takes a schema predates called uh uh basic support and uh so like I uh because they're like manually uh assembling that proofs to

uh beacon state is not a practical interface. So I added a decision procedure uh the leans kernel check to like get the close schemas. So like the fu module applies round trip and injectivities. So to the beacon state uh beacon board state uh beacon block and uh sign beacon block and for the like minimal and the main net uh presets and the uh also the uh the encoding size remain like the explicit in the two to the uh 32 bytes. So uh so like it's basically a kernel

uh decide not a native decide. So the h the condition in the encoded uh with the size strictly like below the 2 to the 30 power by. So while we are working on that so the specification move uh so a client confirmance like uh uh like we in investigation we found that the glo uh state could round trip through prison while there Merkel uh route. So our pre pin use the classic switches uh but uh yeah so like for the matching the bite like did know like that mean that like matching the three rules so like I added a progressive list and like the

progressive bit list and the some progressive containers uh like uh so that we in line from with them and also like uh uh then worked on the glo migration like also So uh gloss and he's basically used the progressive container but our fu stay with the classic one. So writing down the exact guarantee uh expose another type of uh bug like where serialization injectivity says that if a encoder produce the same uh byes for two values like so the four like those values like the uh may may be equal but

say nothing about the buffer uh the decoder will use. So uh basically in a u 64 encoding uh uh which needs the eight bytes and but the user facing rapper uh discard the one bite from them. So like uh uh so uh extra and extra bite was accepted and also got ignored at the same time. So that did not contradict with the injectivity but the encoder was never produced that uh long buffer for uh our decoder to like consume that bite. So, so like my trailing bike fix is like still open and like full conductivity like is kind of need to prove more and yeah like the next we are going to

uh prove the canonical decoding and extend the like our current like codec results to the progressive glows and his shapes and like regenerates the glow uh corpus. So with the uh uh moving generator like we are working on and like yeah and like uh so like uh my basically like take away from the fellowship is kind of the main this theorem and also the implementations and specification pin which have we have to like agree and that's so thanks.

Yeah. So I want to thank Leo uh Mario Ivan Mo and all the uh Ethereum Foundation team and all my fellows. Yeah. >> Yep. >> Awesome. Thank you guys. And do we have any questions thoughts? Yeah. >> Uh yeah. So I think I'm joining a bit late so maybe missing the first part of the presentation but uh I'm aware of the other um um lean repository called eip and they are also having the ssz um um proofs about the konacity and etc. So uh do you know what's the difference

between uh the work that you did and what is sleep can provide? Uh well uh basically uh we are much more complete uh if it's short uh it was like a journal effort u from uh EF guys to uh do another attempt for for verify some kind of stuff they did not go for u like making it a complete model with proof like we did like it's not the same level of effort. Uh it's also a good attempt. Um uh I would not go over like pros and cons. Uh I did not compile it

by by uh but uh uh um y so just talk I'm I'm Leo from not in the AFP. So I we just talked like a few days ago with people. So they are going to focus on the cryptography. So we are we build the protocol using other cryptography primitives uh kind of we are kind of uh uh agnostics of the cryptography implementation. So uh now we are using mostly kind of forign libraries for the cryptography and then we are going to replace them with the leaves cryptography in lin 4 and then

but they are not going to build the whole consensus. The consensus is going to be a theorem and if leaf is going to be like below like at the cryptography level and more like primitives ethereum consensus and execution primitives. Yeah. Yes. So I think in uh like the now there is like we will build the first SSC link for library in May and they have another one and yeah I uh the yeah that's that's going to be decided or something. Yeah. Yeah. Not not yet determined. Yeah.

[music] >> [music]