Ethereum Execution Client in LEAN

Stream: general

[Elton Govada]

Yes, this is probably a very ambitious effort, but if I really wanted to build one, how would you recommend I start?

[Elton Govada]

The up to date Ethereum Execution Layer Specification (EELS) is written and implemented using python but the model uses OOP. I guess my first question is how would I model a LEAN implementation using functional programming?

[Elton Govada]

Lastly, the main motivation is to use the theorem proving capabilities of LEAN alongside the implementation so it could be formally verified.

[Kim Morrison]

What experience do you have with Lean so far?

[Elton Govada]

Mostly theoretical. I've read through chapter 7 (Inductive Types) in the Theorem Proving book and through about chapter 5 (Monads) in the Functional Programming book. I did more hands on with Coq prior to learning Lean, and that was because I found the Software Foundations in Coq a lot easier to learn and follow initially.

[Elton Govada]

I guess my question is more about how I'd start designing and building using FP concepts than it is the theorem proving part atm? Hope that helps :)

[Bolton Bailey]

At the end of the day, even though Lean is a functional languages and Python is object-oriented, many of the same concepts will carry over. There is the additional benefit that blockchain has a philosophy of "immutability" that synergizes nicely with functional code. I don't necessarily see a reason why you couldn't go class-by-class method-by-method through the python code translating to Lean. My only doubt is with the chain itself - I don't know how the spec manages the data type for representing the whole blockchain, but you probably don't want to go around making copies of it with small modifications.

[Bolton Bailey]

I have been thinking more about this in light of the recent interest of the EF in Lean. Off chance, but has anyone on here looked into this since January?

[Elton Govada]

Hey Bolton! Just came from your YT video. Funny enough, soon after posting my interest on the topic, I got a job working in the crypto space, so the project was kinda in the back burner ever since. But I'd love to revisit this topic and try your approach.

One suggestion is if we used the EVM spec as opposed to an implementation, we'd be able to translate the code without all the client code. I think what you were looking for during your live was this: https://github.com/ethereum/execution-specs/tree/master/src/ethereum/cancun

[Bolton Bailey]

Cool! I'll share my thoughts in a minute when I get situated.

[Bolton Bailey]

For anyone who is wondering, here is the recording Elton is referencing is here.

It seems like an implementation of the EVM in Lean could be helpful for this competition, so I'm interested in making one that I can then show to the Ethereum Foundation for them to either use directly or modify for their purposes. There are a variety of ways you could think about making this but the way that seems like it has the highest potential to be extremely easy is to port an existing implementation. I mostly felt the best about this rust implementation linked from the EF website.

[Bolton Bailey]

For some reason Rust has seemed to me to be linguistically similar to Lean, so I like this target. GitHub Copilot was doing a very good job translating Rust to Lean types. It makes me wonder if there are any good LLM based code porting tools that could maybe do this all at once (so if anyone reading this has a suggestion there, LMK).

[Bolton Bailey]

Any other good tool for porting Rust to Lean would be good too. Along these lines I have heard about Aeneas, but unfortunately it looks like there are several Rust language features it still does not support.

[Henrik Böving]

For some reason Rust has seemed to me to be linguistically similar to Lean

that's because we often just copy rust unless there is a good reason not to

[Bolton Bailey]

I see, that's awesome. That makes a lot of sense, not just on the level of having nice implementations to crib from, but also on the level of making it easier for the Rust community to align with Lean.

[Bolton Bailey]

I am reminded of this toot.

[Bolton Bailey]

Anyway, I may want to look into autotranslation a bit more, but @Elton Govada I will try to post whatever I have in GitHub in a day or two.

[Elton Govada]

Bolton Bailey said:

For some reason Rust has seemed to me to be linguistically similar to Lean, so I like this target. GitHub Copilot was doing a very good job translating Rust to Lean types. It makes me wonder if there are any good LLM based code porting tools that could maybe do this all at once (so if anyone reading this has a suggestion there, LMK).

Don't know about code porting tools, but at least for alternative coding LLMS, I'd look into maybe StarCoder2. I had heard some good things about it but haven't looked into it myself yet, but it's trained on like 600 languages so should be promising.

[Bolton Bailey]

Ooh, I see this is available on ollama, which I already have installed, this looks promising.

[Elton Govada]

Bolton Bailey said:

Ooh, I see this is available on ollama, which I already have installed, this looks promising.

sweet, hope it works for ya. Also, what are your thoughts on the pyspec I linked above? Personally, I think the pyspec implementation looks a lot easier to read and decipher over the rust implementation. It might be better to start from there. I'm taking a look at it right now.

[Bolton Bailey]

Yes, I looked around at python options, since I'm more familiar with Python than rust. I think I sort of concluded that it would be too hard to know what all the types were/find where they were defined - I think I was looking at py-evm and saw that some types were defined in a different repository. This execution specs repo looks like it could be good though.

[Matej Penciak]

Automatically generating the code seems like a really interesting strategy. My original route (back in January when I messaged @Elton Govada ) was following the yellow paper and trying to implement everything as I went along. I didn't get much further than the basic arithmetic types, but if there's interest in getting this project off the ground I'd be happy to lend a hand

[Bolton Bailey]

Yeah, if this LLM approach turns out to totally fail I guess the yellowpaper is a good fallback.

Here is my recording of my second work session on this project

I attempted starcoder but it refused to stop generating code, so I switched to llama3 - I later added a token generation limit probably this could be switched back.
The repo is up here, anyone feel free to PR to it if you think you have a good idea.