Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Revm: Links: Add them for the revm_precompile crate #658

Open
11 tasks
clarus opened this issue Feb 14, 2025 · 0 comments
Open
11 tasks

Revm: Links: Add them for the revm_precompile crate #658

clarus opened this issue Feb 14, 2025 · 0 comments
Assignees
Labels

Comments

@clarus
Copy link
Collaborator

clarus commented Feb 14, 2025

Add the links for the revm_precompile crate that is translated in https://github.com/formal-land/coq-of-rust/tree/main/CoqOfRust/revm/revm_precompile

The source crate is in https://github.com/bluealloy/revm/tree/543b4bb8167e5cd9bf5f6421b1af2b867468e8a0/crates/precompile/src

The links should be in a folder CoqOfRust/revm/revm_precompile/links with the same names as the files of the crate. These should contain both the analogous for the types, the traits if any, and the functions/constants.

An example of link file that is complete is https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/revm/revm_interpreter/links/gas.v There is no documentation apart from this example file and the blog posts https://formal.land/blog/2025/01/30/links-for-rust-in-rocq and https://formal.land/blog/2025/02/05/links-for-rust-in-rocq-2 that are slightly outdated.

In a parallel task, I am adding automation to generate the link types in Python, as they are generally very verbose to write but rather simple.

Here is the list of files, excluding the sub-folder for bls12_381 that we can ignore for now:

  • revm/revm_precompile/blake2
  • revm/revm_precompile/bls12_381.v
  • revm/revm_precompile/bn128
  • revm/revm_precompile/hash
  • revm/revm_precompile/identity.v
  • revm/revm_precompile/interface.v
  • revm/revm_precompile/kzg_point_evaluation.v
  • revm/revm_precompile/lib.v
  • revm/revm_precompile/modexp.v
  • revm/revm_precompile/secp256k1.v
  • revm/revm_precompile/utilities.v
@clarus clarus added the Revm label Feb 14, 2025
@romefeller romefeller self-assigned this Feb 16, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

2 participants