Ethereum Specs in Lean 4

Transcript

We will talk about writing Ethereum in Lean, but I think that this is a very good session for us to talk about like the FV part of everything without we mentioned in the previous session. We had like this I will I will talk about a few slides, but then we had like this discussion during like the break about different components of the of the roadmap with FV inside and I think that this can be a very good session to talk about this. So, I just have a very few slides. So, what a spec is is for because recently we have seen like Lean 4 emerging like as a super cool speaking language especially at the age of AI.

And so, of course this is a definition of of a program and I I took this like this quote of Vitalik in 2020 and why Python Python was chosen as a speaking language because the functions are written in Python to strike a balance between formal formality and ease of reading. And this is very cool because right now these are the main properties that Lean 4 can can offer to us. So, in the history of Ethereum we had this different sort of speaking. So, we had the yellow paper and then the content to spec and the execution spec and then maybe Lean will be like the new speaking language.

So, right now in the content to spec what we have is like specs as markdown files with Python blocks and markdown comments and then we transform that into Python and we are able to generate test vectors that can be consumed by all of the clients. But, the test vector can just operate over discrete points in times while in Lean you have these benefits of being able via theorems to to check that your code is formally verified. But, we have like of course this chain of trust where like you have what you mean then you should transform what you mean into a spec and then you have the clients consuming the test vectors from your spec in different languages, and then the machine code that is what

validators run. So, Lean 4 as a specking language is nice because you can have this you can have both functions that can be executable and where you can run arbitrary logic inside, but you have also theorems that run through the kernel to check that everything is correct for every input. And so, you are able, for example, to do theorems on very basic stuff like if you take, for example, SSZ or any serialization stuff, you can check that you serialize and you deserialize, and watch just the decoding undoes the encoding for everything and for all of the inputs. So, that is a way to do like a round trip not testing, but formal verification thing. You can also, for

example check a stuff with a Merkle trees that two different values within the giving the same roots is a collision. This is something that we check for, example, for SSZ. Um we have the cryptography spec repo that has been initiated by the cryptography team at the EF, where we already have like BLS, KZG, and XMSS component available with test vectors that the client can consume and a little bit more than 400 theorems to to to prove everything. We already have some toolings for formal verification. So, we have like Arc Leap, e-theorum, the fast confirmation rule, EVM SM, and EVM UL and the cryptography spec.

Um and now the main strength of all of this is that AI can generate all of this Lean proof and specification very easily. Before, it was like a very hard job to write Lean because writing Lean by hand is super complex and not very human-friendly, but the AI exceptionally like exceptionally good at this. Uh but we have some trade-off. The trade-offs are that we have a lot of pros because of course like you can check every input thanks to the theorem and the typing system of Lean.

Uh, so both the spec, the code, and the proof can be written in the same repo. This is what what we what we are doing right now. Uh, every function has a precise meaning. AI can be very helpful to write proof and check them. Uh, and the client can also reuse the spec code with much better insurance. But, on the other side, fewer people are reading Lean than Python, for example. This is a much more complex language to to to start with. Um, someone need to check the statement. This is what we we are doing in spec, but of course like you cannot just write code everything. You have to check as a human the statement to check that everything is correct.

Uh, and the proof are in general much longer than the spec. And we had like some slowing down when compared to very fancy um implementation because sometime for some operations like uh Lean's Lean 4 is slow to compile and sometimes slower to execute than the very fancy Rust, for example. >> Removing elliptic curves will fix most of this. >> Yeah. [laughter] And yeah, but for example, the other day I was experimenting with some SHA-256 when compared to the Yeah.

Yeah. And we have to trust Lean. We have different like we have a possible approach in the time to for Lean as a speaking language. So, first this is the stage that we are right now on on on the left where like the Lean side sits be beside the Python. So, we have both the Python spec and the Lean spec and we just check via test vectors that they they are in agreement. then we can have like Lean owning like some math module and stuff like this well Lean is particularly friendly to and Python owning the rest of the spec and then we can have maybe in the future Lean completely replacing the spec.

So, now since this is a workshop, I think this is a good time to have a discussion. I imagine some questions that we can talk about, but I I think that so yeah, just to read the question and then I I will I will say what I have in mind as well. So, I I wanted to know if Lean would have code some attacks or some stuff that you you guys have have in mind uh when compared to what we have right now. What's is the approach for you if first like Lean should replace Python as a spec and what is the approach for this in the time?

Who writes the theorem statement and who checks them? Uh will the EIP authors and client developers read Lean and maybe uh provide some Lean proof as part of the EIPs as well? Uh and if we can like fully trust the Lean kernel compiler and and everything. And um what module should we prioritize? And at the end like should we start a more general like is lib efforts um for general or formal verification of Ethereum like we have math lib or arc lib, should we also have eth lib?

>> Yes. Yes. >> I think everyone >> Okay. Perfect then. >> [snorts] >> And uh like I raised like another points uh from the discussion that we had during the break is how should Lean 4 be integrated into the PQ fault in the sense that this is not very clear from the from the the board there that is a bit messy, but like we had Sphinx, we have uh Lean VM for the aggregation.

We need to make sure that this is secure. We have couple of months to couple of years, but not that many. And so, we need to FV Sphinx and we need to FV Lean VM as well. In the post that you did where you described George and and Kev as the different paths that we have for FV Sphinx, you described different approach. One of them is for example to write Lean 4 and then to write assembly of everything and then prove the assembly is correct, but this is likely not the approach we will take for example for Lean VM because Lean VM should be Rust code that is readable by the user that is

um yeah, something that we can check that a lot of people can read. So, this is likely not the approach. On the other side, we have another approach that is with Anise where so, you take some Rust code and things to Anise and Agda that are external framework, you just like extract your Rust code to Lean and then you check that this correspond to the spec. But, I am not exactly and this is of course right now this includes only a part of of Rust, but not the entire Rust and so, this is a bit messy where you need to have some patches and stuff like this. So, maybe a good first question would be how should we approach this in a reasonable way?

Yes George. >> Uh just wondering why did you do this distinction where like in the Sphinx case uh you didn't value human readability, but then in the Lean VM case, you're like, "Ah, we need to be rust so that we can like why is >> I I I think this is Yeah, just because I forgot, I think. But, we can we can have the same. >> But, there is actually a point. >> But, may Yeah, but maybe a bit less because right now if we check, for example, for some consensus or execution clients, we sometimes have BLS or hash functions just written as

assembly code with EV fuzzing. So, maybe since Sphinx is a smaller part and a more cryptography friendly part, we can maybe afford the full assembly with FV strict. But, since lean VM is huge with like the risk five probably inside and so the the core, the compiler, the primitives, the field arithmetics and stuff, maybe less, but I'm not sure. >> No, no, I I heavily agree. So, I think there is So, so I think there is a kind of very specific point we can make, which is that Sphinx is an established standard,

right? You can open SSL HTSA and there's an established standard and everything. It's much more tightly scoped. It's, you know, one set of algorithms that does something very specific with properties that we understand. You know, we understand what it means for a signature scheme to be secure. And even if, you know, we tweak it via sec.gov and so on, like it still is meant to conform to the standard. Essentially, it's just a refinement of it, right? So, the requirement to look at the implementation and check that it does the right thing is much better captured by the high-level spec and the properties that we expect from the spec. Whereas for lean VM, I mean, you could easily have, you know, a fully verified, you know, thing in assembly and it is just a you commit to the wrong guest program and it all goes wrong, right?

So, the the scope of things that are not captured by properties of the underlying cryptography and things like this and Lean VM is much much bigger and that's where you need much closer inspection of what you're doing to check that what you're doing is the correct thing even if your cryptography is is all validated. Um so I think that's an important bit but I do think that this also means that within Lean VM we can have components where we say we have a spec, we have the assembly and you know, if we're not looking at the assembly it's kind of okay. So like if you give me the Lean VM verifier and it's just pure assembly uh like I can I can very easily live with this because I know exactly what I want my verifier to do and it is very very small scope of

things. Whereas if you tell me I just have assembly that says you know, what gets committed to you know, the starts of a Lean VM you know, proof then I kind of want to have a look at this and check that it's committing to the right data. Um and and that's a bit trickier. >> Okay. Okay. So I think I think based on what we just said basically these small mathy modules can be done like straight up in assembly whereas these more complicated things like Lean VM and clients need to be done in a more modular

uh way I guess where some of the sub modules can be done assembly but the overall glue thing needs to be more >> Yes, yes. So so that's also >> modular. >> idea behind if you look at Lean of VM one idea behind this is that then we can do even if we wanted to have verified Rust or something or verified assembly then we would have Lean of VM which is end-to-end Lean VM in Lean and everything that we want to show about the glue and be able to manually inspect about the glue is all there in Lean and then if you want to do then you inline some assembly some FFI but then you have per function correctness properties for the stuff that you're not carefully inspecting manually because it's hard to inspect and you have far more visible and inspectable glue logic in, you know,

high-level theorems that you care about. And that seems to me like the kind of nice approach. Whether you do it in Rust or D or anything else. >> So, is that the approach? >> So, we have Sphinx, ASM, Lean 4. We have XMSS, ASM, Lean 4. And we have Lean VM, Rust, Anise with Axe, Lean 4. >> What's the Lean 4 part? >> Lean 4 is a language. >> Oh, no, I mean what are the errors in >> Uh I mean like we have Lean Sphinx implementation. We have Lean Sphinx as a like as a spec and >> The assembly comes from Lean 4, so the errors are the wrong way.

Yeah. Yeah, yeah, yeah, yeah. Um and and same so same for Lean VM, you could generate Rust from a Lean spec if you wanted. >> But wouldn't we expect people to just read the spec? If you want readability or like why do we need people to be able to read the Rust or >> Uh so there's the there are some components which the spec is less obvious than the cryptography components which have very simple which have hard to implement right properties, but which are otherwise quite simple to understand. >> Okay. >> Um and and there you want a bit more visibility to have higher likelihood of catching that uh we've forgotten about something in the spec.

>> But it feels like you are still adding like layers of complexity uh you know, like the Rust plus the I actually don't know what those are. >> Anise. Anise. >> Uh when you could also sort of like make a conscious effort to have like readable specs and and >> that's what I want. I mean, if I if I can like delete Rust, I'm very happy. >> Yeah, okay. >> That's what That's what I'm working on, right? It's a It's a question of when are you shipping, you know, it's the same as you could if Lean is fast enough, we could just run Lean in production.

>> Yeah, yeah. >> And you have a verified compiler for Lean. It's just that right now Lean is not yet fast It's just about fast enough actually on some things, and we don't get to have a verified compiler for Lean. Maybe in a year we have both. Okay. But then, that's a discussion to have next year. Um >> Okay, so so my point there is that is that we have those things and XMSS papers or spec like this. We have that in Lean 4 for both, and then we just back and forth with the assembly to go to have like a faster and faster and faster implementation that is formally verified. So, that is the approach that we take for the two massive module, and for Lean VM, so we have the Rust code that is now in the Lean VM repo.

We have a spec in Lean, and then we have someone extracting the the Rust to Lean thanks to Anisse, and we prove equivalence with the spec. Is is that the the plan? >> I would opt to generate Rust from a Lean spec. >> But if you So, you go like this. You You have an arrow in this direction as well? >> Yeah, that's what two of our interns did over there. They wrote the [snorts] spec in our Lean, and then they have a Rust implementation of that spec, and it's generated by an agent, and it's constrained to extract back and verify against the open spec.

>> Yeah, I see. >> And remarkably, when you generate Rust, it can only is only valid if it's >> And you back and forth to make it faster and faster and faster? >> Yes. >> Can I Can I try that? Why don't you use the C right >> Uh the C back end of Lean is is not verified, and I trust the Rust compiler more than the C one. >> Wait, just one clarification like um Is that correct that if you went to if you were to ditch Lean VM and just use circuits, then you would get rid of the Rust layer because you wouldn't need it, and it would be closer to sort of these things no?

>> I think >> But you you have to implement the circuit in something. >> Yeah, and I think >> will do it in Rust? Yeah, you could do it in clean and >> Right. >> I I Yeah, but I think that's the even with a circuit, you still need a circuit, you still need the PIOP, you still need the PCS, you still need the bus. This is too complex to >> Okay, okay. >> Yeah, this works, but maybe this is a bit too complex because then no one will be able to read that, so I don't know. >> I have a comment here. >> Can I try something like I feel like this is quite simple because as we said, they are we have very Oh, yeah, yeah, sorry.

>> So, the the top the top two lines are quite simple because they have very simple like mathematical theorem structure. The the third line is more complicated, but I think the way I see it, maybe it's wrong, I don't know. Alex, how you see it is like sort of like having a big Lean VM box like this, which maybe is Rust, and then inside you have like some modules, which is like I don't know, like the finite field stuff, the the sum check thingy, the the like PCS.

Yeah yeah good. Like a bunch of modules, which also on their own have very simple mathematical structure, like the top two boxes, so there you can do ASM kind of stuff. And then you have a bunch of glue in the middle that connects these boxes. And you know, like these boxes are sort of easy to do, sort of, but then the question is how do you connect the boxes? And either you do it with Rust plus Anys, or you do some more weirder thing, but like the the amount of glue you have and how you you prove

it is what I'm it's not clear to me. You know what I mean? >> I mean a lot of this glue does not worry me that much. The glue that worries me is the choosing what I commit to at the start and, you know, passing the execution trace and doing that kind of stuff, checking that the lookup tables are well-formed. Um that that's the glue where, you know, that worries me a bit more. They're like, you know, checking that like Fiat-Shamir well implemented and it like Fiat-Shamir correctly compiles uh you know, my IP with the PCS into the SNARK.

I'm fine with this. We can all do end-to-end. This is not a big issue. Like the so the glue you would write in Lean, right? You wouldn't write in in my mind you wouldn't write like I mean, you you can have it implemented for you in Rust, but then the glue theorems are all in Lean based off of the Lean modules that you get from Rust or from which you generate Rust or you know, doesn't matter. Um that's not a big uh that's not a big problem. >> That I like the approach and we talked about this with with Justin recently. Uh this would allow as well to do auto research challenges on each of the small parts. So, we can have, for example, PCS auto challenge. So, you just the rules are simple. You just have a a polynomial. You should commit it and

open it as fast as possible. And you can find any techniques with a good specification in Lean. Same same for the sum check. The sum check is a very well-known uh algorithm. You can just specify it in Lean and find any possible tricks to make it super fast. >> I I just yeah, I I agree. >> But but I I think so you to your point about the glue as well. The point is also that like how the glue is implemented is a question of software engineering practices. So, if you fix, you know, in advance what are the types and the interfaces and the data structures, then you can iterate on each module and it won't break things as long as you respect some interface invariant, right? So, this is what I'm writing like I have a

Ethereum gas program spec in kind of pure functional Lean. And here like I've, you know, I've written like, you know, pseudo Lean markdown files for every there's like 20 modules. They all have like the types and data structures that are internal or specified to the interface between each of them is specified. And so, I can work on each module completely in parallel and invariants are preserved and nothing breaks, right? And then then it's much easier because, you know, the glue you can kind of abstract away because you can verify it independently. >> Oh, okay. So, I think >> This is the point. >> Okay, so just to draw some connections here, you know, like the various modules will talk to each other and stuff.

And I think what you're saying is that you're saying that if the interactions between the modules are modeled in a very nice and elegant way, and then the glue is essentially minimized in the sense that >> Well, it is then the the glue is an invariant holds regardless of how you change individual modules, which gives you much better guarantees that you can, for example, auto research every module independently as long as whatever comes out of it satisfies some interface invariant. So, if you auto research the IOP, you just need to make sure that then what comes out of it is still of the right type and the right kind of data form to go into Fiat-Shamir, right? And as long as that's respected, you can do whatever you want to do with the IOP, it doesn't matter.

>> And so, what does it mean exactly for us like, Kev, maybe what is your your point of view about this? How should we approach that? You have worked on so recently on on Clean to make the circuits so that's basically here inside Lean VM. So, we have Clean where we can fit the circuits. Say, and so, what's is your opinion about all this because Derek has worked on this for Plonky 3 to extract the Plonky 3 code that is in Rust and make it checkable with a Lean 4 proof.

But this is quite a heavy job and with some like sometimes some patches that you have to do and stuff. So I don't know Kev, maybe if you have like an opinion on how we should approach this. >> Um so I guess Lean VM is more than just a circuit cuz Clean >> Yeah, yeah. It's just for the circuit part. >> Yeah, yeah. >> Um I do think it makes sense to use Clean to write the circuits and write theorems about the circuits to make sure they're correct. Um that's sort of one of the reasons we've switched to VMs cuz circuits were hard to write.

Um so in my opinion I think writing it in Clean and extracting it to Rust makes the the most sense. Um >> And and for the rest of the VM, we just go to this? >> Uh I think this is the best tool we have today. Um just using [clears throat] Anias to extract Lean VM to from Rust to Lean and then proving things about it. But this is I've only ever thought about the verifier. I mean the prover is important, but it seems kind of harder to um prove a lot of things about. Like cuz for the prover we want completeness, right? Um under some amount of memory guarantees.

Like you want to make sure that given any witness the you never go over let's say 32 GB. I'm not completely sure how to prove things like this. Um Like cuz the says Lean VM there, so I just assumed that it's prover and verifier. >> Yeah, this is more or less everything. I I don't know what you guys think, but I I I would go for everything, yeah. And how how many lines maybe do you expect it because I think like I am trying to imagine that, but I think this is like hundreds of thousands of lines of everything before the proof of specs, both.

>> I mean, lines of proof doesn't really matter. >> Yeah, yeah. >> I think uh the Anes pathway is reasonably reliable. Um in the case of like the cryptography where we care about and what we'll have in Lean VM, um we there are logistical things kind of in in this extraction process. We'll probably have to patch, kind of massage the Rust um a bit. So, there's a question, like Alex was saying, we could start with the spec and um and we can probably get performance by auto researching within the subset of

Rust that Anes already fully supports. They are continuously expanding the tool and they care about um these things, and so it might be the case that uh we we don't have some of these issues extracting in the short term. I I think certainly um there there may be we may be able to approach a verification from um two different levels of abstraction, um kind of the module plus glue level, where we can prove uh we have these high-level Arclight specs, and we maybe we can prove um the coherence of everything kind of at a higher level. Um we may uh um there there there may be aspects of

of Lean VM that we um from the extraction standpoint, we kind of axiomatize them, but then we um have a separate verification effort where we where we show that the summaries are axioms that we assume over this a module maybe about Fiat Shamir, you know, one of these boxes here, um show that it holds, especially if especially if we're using um like um these optimized backends for for rust that Anias doesn't really support so like SimD backends and things like that. I I think we can reasonably for for these kind of smaller more focused modules, I think it will be very reasonable for us to verify the the like machine code directly

>> [clears throat] >> and just and kind of decompile it logically. So I I picture kind of a fusion of these will I think we will want the Anias extraction especially for the high level kind of architecture of things and then we will likely have to assume things about different modules but then we can check those assumptions. We can actually prove those assumptions hold kind of in the way that Alex was saying of of essentially from a logical standpoint establishing interfaces of these modules and kind of how they talk to each other. Um >> once it comes, you can probably have a

general case of of this assembly implementation in kind of one shot pretty widely and in a day or two. >> For what? >> I I just I think that our ability to formally verify assembly will will grow rapidly and and so it like the XMSS verifier that was done in an afternoon and some of these other projects have taken a little bit more time, but um but I think it's just a question of figuring [clears throat] out the right kind of setup and I we should be able to do this quickly. I don't think this will bog us down at all.

>> Yeah. Right. Yeah, I guess I'm saying that there are things that we currently today put in assembly because we need it to be performance critical and it does seem to make sense to make sure that formal verification make sure that these things are correct, but just because we can put something in assembly >> no, no, because there's also a point that like if we can generate verified assembly in an afternoon, it is both faster and easier to formally verify than a bunch of Rust doesn't extract. >> It doesn't extract as in >> So, if you give me like a Plonky2 verifier right now, it does not extract via any sort of hacks, so you cannot verify it. Whereas if you generate a RISC-V assembly verifier that you can

verify, then that's verified and the Rust one is not. >> You mean like a >> I mean it cannot extract the full Rust. This is just a small part of the Rust. >> So, like what you can what you can generate in assembly, you can both generate and formally verify with less effort than the Rust. >> And this is the SNARK verifier, right? >> Yeah. >> Mhm. >> Or or you know, XMSS things you know, for these for these like small things which are like a couple of hundred lines or something at most, then like generating the RISC-V assembly is generally faster, easier, and has less TCB than Rust.

>> Okay, I see. >> So, it's it's a kind of no you know, a no-brainer as some would say. >> But but why is that the case? Why is it that Rust can verify No, it's just good Plonky's 3 wasn't written or whatever is used now wasn't written to extract via an ears. I mean, I can verify another very I can generate another verify in Rust and constrain it to extract via an ears. Uh I don't care about the difference.

Yeah, it's so easy to generate. >> It's a point. >> takes an afternoon. Why would you, >> [snorts] >> you know? >> I think the point was just about Rust itself because Anis just supports a subset of Rust and so if you have unsafe Rust or traits in Rust, sometimes it just doesn't extract well and so you have to do some patches to remember to >> if it if it takes an afternoon to verify the assembly produced by Rust or an afternoon to like generate some fresh assembly, I I don't care which one we do. It doesn't matter. Whichever one is faster.

>> And how do you manage the the assembly that you have inside Rust function? Because you know, inside Rust function, for example, if I have a function A, I can inside >> So this depends on whether you pass it as an intrinsic or as an inline. So if you pass it as an intrinsic, the Rust compiler can still optimize it and then you lose you add some trust. If you pass it inline, then the Rust compiler won't touch it. >> Yeah, so if I have a function A, inside inside I have ASM macro and I have a bunch of ASM lines. To extract that to Lean, you still have to go to Anis or you can >> I would generate the assembly from Lean and then pass that to the Rust.

Right. >> Yeah. >> So so I think there's a lot of stuff here which is based on oh, we have this code and we need to figure out how to get it to lean. I think that at the point now where generating code is very, very easy, whatever we can generate code from lean makes our life easier and we pass it back to us if we need to. Because then we remove the chance that we have some rust that we want to pass back to lean and it just doesn't work. Right? If we just start from lean, we'll get stuff that at least always works with respect to verification. >> That's why I was asking you the other day at your workshop about recursion that fast the question if we should go module by module or as a whole because I think that if we are sure that a prover

system should always have a sum check, should always have a finite field, should always have a PCS and everything, then it is probably easier to go piece by piece for the auto research because you are able to easily optimize one piece with less constraint to the auto research. While if we are unsure about this, this probably a best approach to go to some to that full and like ask the auto research to just optimize the whole prover as a as a whole.

>> Yeah, I mean so well so the auto research is a bit different because the auto research you have you know, a market of sorts and you could imagine that, you know, people who are participating will focus on one module at a time. Right? Um I mean this is kind of what you see in the current auto research things. If you look at snark dot fast, at some point a lot of people were submitting things on like the NTT kernel and then they switched to optimizing something else based on, you know, someone does a good submission to optimize something. People do the micro optimizations on top of that. Someone finds like another kind of big path. So, you could split it up into modules. You could have everything at once and allow for kind of co-optimization of some kind. Um I don't think it it matters too much and

then yes, if you have invariant interfaces between the modules, then you can optimize every module independently and it won't break things. So, that's uh it did Yeah, that's fine. >> So, you There may be complications if you have modules which work over shared state. So, you've got some shared memory and you know, model model B is essentially operating over the output of model A. Um you know, the if you optimize exclusively for a single module, you may get it to be very efficient, but the subsequent memory layout that your

downstream models now have modules have to consume >> But this depends on where you can fix that in the interface. Right. If you know what the if you know what the receiving module would perform best on, you can obviously transmit that to the higher level module. But but yes, but I do think there are cases where co-design will will help, right? >> Yeah, maybe like the the global optimum is very different from like a local optimum. >> Yes, I think that's entirely possible. But that's the point of having an end-to-end correctness statement for the whole thing where you can spec out intermediate statements for each module, but still say if you want to tweak these as long as the end-to-end one stands, it's it's fine. Benedict.

>> I'm sorry. I just one more point. I I feel like that um also links back to the point around this glue logic. In many cases, it seems to be that the separation um in terms of the the kind of the environment. So, specifically the memory uh becomes more and more challenging as the size of the program grows because you've got memory many different modules all accessing and modifying the same state. So, being able to kind of chain um you know, these incremental transformations across your you know, your your proof essentially um, becomes a lot more challenging. Um, >> But this is also a question of, um,

engineering design decisions. You can you can make every module purely functional and then it's not that much of an issue, right? And that's that's I think is you just need kind of feedback from performance engineers on what would be best. >> A lot of the code that we do see is kind of imperative and >> Yeah, yeah. But but that's that doesn't have to be fixed. I mean, it can stay that way. It can change and we just need people with engineering expertise to advise on this. >> So, I guess about the separate splitting up the the auto research challenge in particular in modules, I think it there's one source of complexity that is if you like if you have have the entire thing and your submission is the entire thing, then it needs to contain a soundness proof. That's I think we all agree on that. But if you split it

up in modules that you can submit individually, then what is the security notion for each module? Then you need to define that and you need to convince you need to essentially, while designing the auto research challenge, you need to provide a security proof that says these different security notions compose into soundness. Right? So, it's designing the challenge is much more tricky. Right, right. You But you need to define for every module you need to define what is the security notion and then you need to give a lean proof that says if I have anything that satisfies this notion and

anything that satisfies this notion, then it composes generically into into a sound thing. And I think designing these notions so that the auto research challenge gives you in total a meaningful thing is not so trivial. >> Yeah, so so I think with the example of sum check, one issue would be you can always say like my sum check spec is sound, but there's a question of what is the sum check actually checking? And George has this for example, right? So, I think Kwong is not here, but I remember talking to him a while back and he was saying that, you know, with Jolteon, part of the complexity was they had 20 sum checks or something, and keeping track of what every sum check is meant to do is hard, even if every sum check is sound kind of in isolation.

Um and that's the kind of where the glue logic comes in. Um which if you have an end-to-end theorem that has to be preserved is still fine, right? So, it's just that if you ship a per module challenge, you still have to ship that within some kind of end-to-end ZKVM framework, and with a global theorem that has to hold no matter what, even if you're only working on one module at a time. Um >> Um I have a question about this ASM thing still. So, do we have concrete numbers for how long it takes to, let's say, I already have the spec written to prove that um let's say some examples of ASM are correct outside of this like just basically hashing a bunch of times?

Like, do we have numbers for, let's say, something like SSZ, something that's a bit more uh complicated? >> It depends a bit on the complexity of the program. So, something like is, you know, a verifier which is a single sort of program that doesn't do weird stuff is going to be not too bad. Something which has like some concurrency, something which has uh a lot of jumps is going to be harder. I don't think we have full numbers. I don't think there is a kind of strict rule of thumb uh to to follow. Or we definitely don't have enough data to give like a strict rule of thumb. >> Okay. Uh but do we have numbers on like outside of uh strings? Like, do do we have like other examples of ASM that we've uh formally verified just to have like >> so we have the original iteration of EVM

ASM, and that took, you know, a long time. Yeah. Uh take into account that we were doing it for the first time, and you know, there was a bit of figuring out what to do, but it it, you know, for that size of execution gas program, it obviously took, you know, an order of more than an order of magnitude more than uh than, you know, otus.go verifier. >> Right. And do we have uh numbers for x86 I mean probably not but x86 and arm because I think for these ones we've been doing risk five. >> Yes. For x86 and arm it would well okay given again a single threaded very simple program I don't think it would be that different like there are more instructions but the complexity is pretty not that bad and like the reasoning about the program won't change

that much. Um so I don't I wouldn't say it would be like drastically different but I would say that there are probably within x86 and arm is also the kinds of programs that we would want verified at that level large ones who are going to be more complex because it's going to be things like client code which is more complex. >> Right. >> So it's less about I mean the ISO will probably make a difference but I think it's less about the ISO itself and more about the complexity of the program and whatever concurrency jumps and this kind of stuff. >> Right. >> Yeah I think this would be interesting numbers to have it probably be more convincing cuz I did try and I feel like maybe it's a skill issue on my end cuz my SSD thing was like running for two days.

>> the thing is with these projects I think a lot of it is in terms of how you set it up right that that's why I think it in many ways just kind of like generating fresh assembly is just that much easier than taking something that comes out of a compiler because the setup cost is just kind of easy you start from scratch with like a spec and your kind of workflow set up and you're not trying to integrate anything else. Um and I I think that that kind of methodology is going to be important. I mean same with EVM ASM right like a lot of the issues that we ran into were essentially setup issues more than anything like at the point where you're just generating assembly the cost is number of tokens and agent time right which is not which is kind of a fake

cost. Um >> But then what's the delta between the thing the agent has generated versus like the thing that's gone through the compiler it's gone through many optimization passes like why is that why is the thing the agent generated different from the thing the compiler generates like >> What do you mean by different? You mean different in terms of like setting it up? >> Like I expect that the compiler is going to generate something very optimized that I guess is going to be harder to prove than something the agent is going to generate. Is this also going to be very optimized or like what's the delta here? Um >> Uh I mean the the the delta is kind of Well, again, it depends on the program complexity and then the delta is in, you know, how much harder is it to verify

some already optimized set of instructions compared to how much harder is it to do translation validation over an unoptimized set of instructions that you then later optimize. And that is I don't know, kind of empirical. >> It also depends on the thing where you want the source code to be, if you want to maintain source in Rust or something like that, um so you can start depending and then plug it into things. And then how how often you need to compile it. >> Yeah, with potentially a different version of the compiler. >> So, uh on the performance side, you can do more optimization if you are directly in assembly, but uh to have uh to get get from most of the

uh benefits, you need to have bigger functions because uh one of the constraint of compilers uh is that they have this calling convention thing in between function. They need to save registers and restore registers. And if you have a global uh state transition function, they can say, "Well, let's forget about registers uh saving uh etc. I know from the spec which one uh are actually matter." And so, you can uh skip a lot of overhead uh this way. Um now, the thing is with agents, the smaller uh you give them uh as a thing to optimize, the better they are at it

uh because uh they have uh the context um issue as well. So, I'm a bit torn into like giving them small function, like you said, and giving them uh bigger functions uh to optimize. I think the bigger is the better, and then you can have uh some kind of um common API a C-like uh API uh that any client can then use uh to call it. >> Right.

>> Yeah, so uh I had a hash tree root um function, and I basically just wrote it in Rust. I generated the assembly, and we just started from there. So, it wasn't the agent generating it. Uh there was Lean specs already written uh by you and Justin Traglia uh that I asked it to prove equivalence with. No, I just I couldn't get it to do the first uh equivalence proof after like 2 3 days, so I just gave up.

>> But but so you gave it some assembly to prove instead of generating assembly. >> Yeah, exactly. >> So, I I would try asking it to generate assembly. >> Mhm. >> Yeah, I have a question. So, the assembly there's more than one language, right? There's like uh x86 uh arm RISC-V. So, is the plan to have proofs for each uh pair basically or because you could you could also consider having some intermediate language uh to compile to like could even be like WebAssembly or something like this. >> So, one thing we did consider was actually just using RISC-V and then having a fully verified interpreter from RISC-V to x86 and arm on the basis that essentially the ZK-VMs have already demonstrated that they're able to like

emulate RISC-V um at kind of near native speed. That would be one option. Uh we we haven't tested is it better to try to do this or is it better to just write X86 or arm assembly directly. Um we need to just kind of find this out empirically. >> Mhm. Cool. Thanks. >> Yeah, [clears throat] I'm a bit less certain about the writing a program in RISC-V and then having a RISC-V interpreter uh run this RISC-V if the functions are too small. I think probably >> I don't know. Like it would be doable. I don't know if it's better.

>> Right. Right. >> There is also like this possibility of doing like another auto-research time to transform like the the RISC-V in the arm interpreter. >> Um >> Yep. Yeah. I mean as long I mean, you know, from a verification perspective, as long as you can show that, you know, just the the the state of the execution versus RISC-V and whatever I see you then target with interpreter is is consistently the same, you know, that's that's the property you're after and you could auto-research over this. Um But but then also once you auto-research over this, your interpreter's going to become a compiler, um which which is doable. So I know I, you know, from talking to the Fractus guys who just compiled a team, I remember them saying that they looked at the

emulators from RISC and so on and they felt extremely confident that they would be able to produce something faster with a lowering in MLIR from RISC-V to X86. And we already have a RISC-V MLIR dialect which is formally verified against the cell spec. Um there's interest including from someone at Intel who's working on the X86 specs at is formally verified against an X86 spec. So that could be a target. >> Uh just one point in terms of um auto-research. Uh so far we've been primarily focused on optimizing algorithms and constructions, but I wonder if we could maybe take a step back and focus the auto-research on um the actual frameworks that we used to

do formal verification. So, a lot of the um the the F V, you know, the risk five interpreters, etc., the separation logic, maybe even some semantics for um different uh assembly um or or or RISC-V could potentially be um you know, the target of auto research. We could look at metrics such as um performance to try and get um you know, F V as quick as possible, but also to try and identify um you know, potential for bugs, whether that's in the semantic definitions or you know, other places. Um but it seems like maybe we can use the same sort of auto research effort, uh but focus it on kind of tooling and frameworks as opposed to

necessarily exclusively um you know, the actual uh algorithms and constructions. >> Um I I I I think the risk with with that is that like when you change semantic definitions, the nice thing with auto research is that whatever you auto research, you still have a notion of it's correct. But if you start going into like libraries and tooling and start changing definitions for what like a oracle is, what a reduction is, what a SNARK is, like how do you know that the AI doesn't start reward hacking and and whatnot?

>> Well, I you should have some >> I mean, in an ideal situation, you'd have a way to check. So, um like a differential oracle, let's say you're running on you're running on um you know, an ARM chip or an X86 chip, uh you know, you write some instruction sequence and you assert that uh you know, the kind of the output that you execute on the on the CPU itself, on the host, is equivalent to >> But this assumes correctness of your CPU. >> Yes. Yes, it does. >> know, they have bugs, so >> True.

Um it's just an idea, uh but >> Yeah. >> it's >> I think auto researching the spec is difficult because if you're not changing the spec as part of the order research it's unclear what you're doing and then maybe making the spec like a bit faster to execute. >> Not not necessarily the spec, but more so just framework. So, I mean you've got some risk five interpreter in um you know, in in lean or you have some separation logic, whatever it is. Um and ultimately uh you want to make it faster. Um but you want to preserve semantics. I mean the preserve the semantic definition stuff, maybe that's you know, separate conversation, but just generally speaking it seems reasonable that we should be able to

um apply auto research to optimize tooling um while still preserving correctness. If we can do it for for you know, cryptographic algorithms, why can't we do it for uh an interpreter in lean? >> Yeah, can try. I mean I can see potential for like auto researching decision procedures or tactics or something that you know, work over some data set. >> Mhm. >> It will probably overfit, you know, potentially badly, but uh but yeah, could be done.

As long as you can specify some invariants. Right. Um [clears throat] I am a bit worried about like this one. I don't know like we have talked about this for 1 hour now, but I think this this one can be really messy and since we are like especially right now since we are pushing much more like AI generated code in Lean VM with the risk

five branch, uh I think that we should take this one seriously quickly. >> I completely agree with what you said. I think the only way that two first things might go sour is if this sort of technique doesn't give us the performance we wanted like Yeah, I don't know what performance we want like compared to what Emil has done and what ASML in four things is going to give us, but that's another thing that you know, in a few months we might be like oh we need to get a tool.

Yeah, yeah, yeah, yeah. Just that I don't know right now >> Yeah. I I On my side I am pretty confident especially like given the fact that with Benedict we were able to to to do the XMSS back almost completely and with human review in lean in couple of So

I know we can do it. I know this this is small modules. But this one Yes, but the performance I think that with EVM ISM this was kind of there is Yeah. Yep. No okay. I have maybe slightly tangential question on just Lean VM development generally. So, we can of course use any us kind of out of the box as the raw tool. Um there's a sister tool which is hacks which is what I've been using for Plonky 3 which is essentially these days it's essentially

um a wrapper and some small tweaks to any us. Um the point being that it's easier to integrate with rust code uh and and you can inline specs uh through comments and there's a kind of a syntax uh that hacks uses. Um I wonder what the appetite is for inlining um in kind of inlining specs uh with that method in lean lean VM directly. >> You mean like on the top of the rest what you describe at the last minute on the top of the right function you just write some photo spec and this is automatically read by the >> It generates a lemma that and it it

generates a proof obligation that you you then need to discharge on the lean side. It it what it does is it couples the like um There will be times in in the functions where you where you're maybe writing a function you say, "Oh, I need this parameter to not exceed this bound or whatever." And you can write that directly and then you can formally prove it um on the lean side. >> that on all of the function and all of the object. For example, I have a structure >> Just wherever you want it. >> Okay, okay. But the the the ideal situation is to have that everywhere, right?

>> I think you just kind of do it anywhere. I don't actually know the limits. Yeah, it's it's sort of an optional thing anywhere you want to. If you the the ideal I think situation from that perspective is is if you're developing the code and you think to yourself, "I need this property about this function, but I can't constrain it natively in the types or something like that, then you can annotate with any spec you want, but it's it's completely optional everywhere. >> And there is a I guess a specific framework to do that. >> Yeah, they have a kind of a spec language that you put into the comments. Yeah.

>> Very good. We haven't do that, but >> I think I think that um if if we're looking I mean if we're developing this with the intent of formally verifying it, um I I think it's if there's appetite for I think I think that we should. Um I think it's a it could be a really strong verification pipeline. >> Yeah, but yeah, because personally the more we have AI generated code, the more I am scared about what I push. Yeah.

Okay. >> I think Haxl will be more friendly to the software developer, and Yices I think is is more of a slightly more academic, um and slightly more just kind of purely formal verification. I think Haxl they do a good job of integrating it with the software development life life cycle. >> Okay. And like if we go to this, like where can we find this one? Like I know that Nick has worked on on on Lean VM specified in Lean 4. So, I guess that we are we are re- reusing like Arclib and like Compcert, I guess.

Yeah. >> Just the whole kind of Arclib ecosystem. We have lot Yeah. >> [cough] >> And is there like a is there a specific repo that encapsulate all of this? Is there like a Lean 4 Lean specific repo? Lean VM. >> Leaner VM. >> Okay. Okay. >> It's like >> This is where you are working on. >> Yes. Yes. Yeah. >> And this is for this is not for the risk five stuff. This is for the Purely yeah. Oh yeah, that's right.

>> [clears throat] >> For risk five it's like should be just plug and play basically. Yeah, like you should just be able to plug it in and it will work. >> You have verified all of these modules? Like the fiat shamir, the sound check. >> Yeah, so right now we just have We we have a interactive IOP. It's been formally verified. But the actual BCS transform is not not not yet, but >> Okay. Okay. >> Yeah, yeah, I'll be giving a talk about this in like two hours or something. Yeah.

>> One question I have is on this x86 and arm. Uh As far as I know the risk five specs are pretty basically gold standard. Uh for the x86 and arm specs are they maintained? Are they like good? >> x86 we have they are we're still kind of investigating that. There are two strong choices, but they are maintained. And I think yeah. >> one spec >> [clears throat] >> have a set of x

semantics but but yeah, and it's the same for arm. And there's an automatic translation for ASL which is arm's spec language. And then the other thing for x86 is the guy who worked on x on the arm specs and ASL at arm for many many years is now Intel and he's working on a new fancy set of x 86 >> Okay.

>> [snorts] >> Okay. >> And so the feature mirror should be there in archive? Yeah. It is not there It is not there yet? And it's a D S F S Yeah. Okay.

Then uh yeah. I guess that we will need to talk more in the upcoming weeks. Yeah, that's perfect. >> I I think that with with Lean VM we can probably start um and I I looked and noticed there is some kind of formal work, but we can probably start even now just getting a good framework in for verification for this pipeline kind of through hacks and and or um and kind of figuring out where the pain points are going to be with our specs, how are they getting married in and of course with Nick's work.

>> And that is very cool like it's a work by by Kev like the clean stuff is very cool. We should we should have it. >> Uh just a preface. I just like one prompted the AI's I haven't checked that PR yet. Just Just a [laughter] give a disclaimer. I need >> Um I have a question with the hacks and near stuff. Like from what I understand because a lot of the optimizations in Lean VM are very much like concurrency, threading, SIMD based which we don't have formalization for in Lean 4. Am I correct? So like we we going to We that, right? Otherwise if we don't have it then the VM is just not performing worth less.

>> especially like in the newest version that in the vibe coded version, let us say, of LLVM in the risk five exploration branch, you have like SIMD and even assembly everywhere like so. >> Yeah, so that that has to be so for like anything if we want to like have some measure of equivalence between my rust code and Merlin full spec, this needs to be thought about. Like yeah. >> [laughter] >> Excellent.

The other is obviously we do the assembly route. And then the other which was suggested by Buzz, who I guess will be here later today or tomorrow, was he has some experience where he will basically have some Jasmine. Jasmine is essentially typed assembly with a verified compiler. And he just basically puts that on the leaves of the rust code that he's done verifying at the high level in hacks. Uh and so he he he basically puts in some Jasmine code to some rust verified code for like SIMD backends. And and that, you know, seems to work. Um so it's it's doable. I don't think we have maybe like we haven't seen like what is the best way to do it, but it is doable.

>> Yeah. >> I mean, I'm not an expert with with like SIMD and like the concurrency stuff. But yeah, but from what I understand, like SIMD is not the same necessarily as is not the same as concurrency like we were talking about earlier. >> I mean, maybe do we care about like race conditions and um >> So, uh Intel used to have something online that explains SIMD and it's actually it looks like a formal spec. Like it it has inputs. It it says in a big Indian what's the input and what's the output with XOR, shifts, roll, etc.

So, each SIMD instruction is very simple for Intel and it's also the same on ARM. And I think you can just write code in an overnight with proper tests. The issue is mapping. If you do a high-level spec in LIN 4 and you say use SIMD, it's just it has to pack the data in a very specific manner to use it. And then you need to generate the actual code from this. But the formalization of SIMD, I don't think it's hard. It's a packing around.

>> Okay. And but this doesn't Um >> Yeah, but this the C compiler when you use SIMD is It does nothing. Like it's it's a intrinsics that you call. And so So, what what what's happened is that um the Uh They they have a mapping where they see an intrinsics and then they have a specific instruction to generate directly the SIMD code. But you don't really need to care about

that. You can just check in the header x86.h and then you have a couple of headers for each AVX2, AVX512, etc. And you can see inside that it's um Uh So, so the compiler even doesn't go into that. You see that it's a SIMD SIMD and it's intercept the call and replace it into a specific AST node. >> I miss This is just not This is just a SIMD. We don't have anything equivalent for say like atomic read, atomic writes, compare and swap, like these kind of instructions.

>> Yeah, so those are the hardest, but um uh for Lean VM, I guess they're needed, but if for example, if you do the state transition function for the uh you don't need it. Like it's not used. You cannot even The only thing you can parallelize is uh currently the cryptography if you have multiple blocks and you do you want to do batch parallel verification. >> Okay. But Lean VM does use those self-instructions, right? I see.

Yeah, okay. Um >> Uh on for on the parallelism side, uh you can probably formally verify the components and then launch uh at a higher level multiple threads. I would have to look into uh how it's done today uh to to give you more info. >> Yeah, I mean if there's a risk with concurrency that like it often you when you formally verify the code of one thread, it's like correct and is fine, but as soon as you have interactions and other threads and whatnot, then like everything starts blowing up. And that's like that's where the difficulty is. It was never the >> But uh that's uh if your functions uh work on shared memory, but uh in in the case of Lean VM, uh you can't

parallelize easily the tree construction because the tree uh every single function inside the tree is pure and it's only at the seam uh to talk like Claude at you have those uh merging. >> Right. Okay. Yeah. >> Um yeah, I was going to say maybe a quick summary is that like if you're maybe like doing engineering currently today uh and you have assembly that you want to ensure is correct, then the way that I guess people are advising is to write your spec in Lean 4 and prove that is equivalent the small assembly that you have. And if you written it in Rust, then Anias hacks is the way forward at

least for now. And it has different like trust is has a different TCP, but at least compared to what we're doing today with like unit tests like this is at least better. Um >> I mean, it's particularly better checking the logic of a protocol. >> Right. >> Which unit tests are not very good at checking. >> Right. And for circuits, clean is sort of the approach. >> Just write it in clean and then you can extract to Rust. >> And and so clean has the plonky two back in NCR now actually. >> Right. Right. >> We're not using plonky.

>> It'd be nice to have some more data there. Just like sort of like what you say the packet >> Yeah, so I have a draft blog I've been meaning to publish on the website which has the like here's the stack and you know, use that. >> [laughter] >> Cool. >> Yeah. >> All right. >> Thank you. >> Thank you. >> Then lunch? >> On the concurrency side just because maybe it's useful like in our prover at least like there are some obvious concurrency parts that happens.

For example, you might want to start proving before you finish generating the whole trace. So there there are multiple scenarios where you want to move forward faces and start to running more things in parallel. So that's something you have more serial parts of the code that keep advancing on its own and more parallels that starts at the side. Uh >> Any comments?

>> Yeah. >> [applause] >> Thank you.