We like to have numbers to measure our progress while coding.
Here is the list of EVM instructions from the Rust Revm implementation that we have successfully translated to a typed version in Rocq: https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/revm/revm_interpreter/instructions/links/progress_on_links.md
Here is the list of EVM instructions from the Rust Revm implementation that we have successfully translated to a typed version in Rocq: https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/revm/revm_interpreter/instructions/links/progress_on_links.md
Comments
The "coq-of-rust" translator gives us a first representation of the code in Rocq, but then we need to show that a typing of the translated code exists, which can require a bit of work.
We are not yet there, but hopefully, it will be the case in some months!