doc: add generated revm verif files

docs/revm-python-spec/import_revm.py

@@ -0,0 +1,121 @@
+"""
+Import the Revm files.
+"""
+
+import os
+
+# rm -Rf output folders
+for folder in ["revm", "revm-coq", "spec", "spec-coq"]:
+    os.system(f"rm -Rf revm-verif/{folder}")
+
+crates_folder = "../../../../Rust/revm/crates"
+spec_folder = "../../../../Ethereum/execution-specs/src/ethereum"
+rust_coq_folder = "../../../../Rust/coq-of-rust/CoqOfRust/revm"
+spec_coq_folder = "../../../../Ethereum/coq-of-python/CoqOfPython/ethereum"
+
+# For each Revm file, recursively import the file to the current directory.
+for root, dirs, files in os.walk(crates_folder):
+    for file in files:
+        if file.endswith(".rs"):
+            file_path = os.path.join(root, file)
+            # Get the `root` path relative to `crates_folder`.
+            root_path = os.path.relpath(root, crates_folder)
+            new_file_path = os.path.join("revm-verif/revm", root_path, file[:-3] + ".md")
+            print(file_path)
+            print(new_file_path)
+            print()
+            with open(file_path, "r") as f:
+                # Create the directory if needed
+                os.makedirs(os.path.dirname(new_file_path), exist_ok=True)
+                with open(new_file_path, "w") as new_f:
+                    new_f.write(
+                        f"""# 🦀 {file}
+
+[🐙 GitHub source](https://github.com/bluealloy/revm/tree/99e177d6bedf3823a717d3017b3cfeb98ed2aeac/crates/{root_path}/{file})
+
+```rust
+""" +
+                        f.read() +
+                        "```\n"
+                    )
+
+# For each Python spec file, recursively import the file to the current directory.
+for root, dirs, files in os.walk(spec_folder):
+    for file in files:
+        if file.endswith(".py"):
+            file_path = os.path.join(root, file)
+            # Get the `root` path relative to `crates_folder`.
+            root_path = os.path.relpath(root, spec_folder)
+            new_file_path = os.path.join("revm-verif/spec", root_path, file[:-3] + ".md")
+            print(file_path)
+            print(new_file_path)
+            print()
+            with open(file_path, "r") as f:
+                # Create the directory if needed
+                os.makedirs(os.path.dirname(new_file_path), exist_ok=True)
+                with open(new_file_path, "w") as new_f:
+                    new_f.write(
+                        f"""# 🐍 {file}
+
+[🐙 GitHub source](https://github.com/ethereum/execution-specs/blob/c5415056a4a7066906f67c203ec5364a9de8e017/src/ethereum/{root_path}/{file})
+
+```python
+""" +
+                        f.read() +
+                        "```\n"
+                    )
+
+for root, dirs, files in os.walk(rust_coq_folder):
+    for file in files:
+        if file.endswith(".v"):
+            file_path = os.path.join(root, file)
+            # Get the `root` path relative to `crates_folder`.
+            root_path = os.path.relpath(root, rust_coq_folder)
+            new_file_path = os.path.join("revm-verif/revm-coq", root_path, file[:-2] + ".md")
+            print(file_path)
+            print(new_file_path)
+            print()
+            with open(file_path, "r") as f:
+                # Create the directory if needed
+                os.makedirs(os.path.dirname(new_file_path), exist_ok=True)
+                with open(new_file_path, "w") as new_f:
+                    new_f.write(
+                        f"""# 🐓 {file}
+
+[🐙 GitHub source](https://github.com/formal-land/coq-of-rust/tree/main/CoqOfRust/revm/{root_path}/{file})
+
+```coq
+""" +
+                        f.read() +
+                        "```\n"
+                    )
+
+for root, dirs, files in os.walk(spec_coq_folder):
+    for file in files:
+        if file.endswith(".v"):
+            file_path = os.path.join(root, file)
+            # Get the `root` path relative to `crates_folder`.
+            root_path = os.path.relpath(root, spec_coq_folder)
+            new_file_path = \
+                os.path.join(
+                    "revm-verif/spec-coq",
+                    root_path,
+                    file[:-2] + ".md"
+                )
+            print(file_path)
+            print(new_file_path)
+            print()
+            with open(file_path, "r") as f:
+                # Create the directory if needed
+                os.makedirs(os.path.dirname(new_file_path), exist_ok=True)
+                with open(new_file_path, "w") as new_f:
+                    new_f.write(
+                        f"""# 🐓 {file}
+
+[🐙 GitHub source](https://github.com/formal-land/coq-of-python/tree/main/CoqOfPython/ethereum/{root_path}/{file})
+
+```coq
+""" +
+                        f.read() +
+                        "```\n"
+                    )

docs/revm-python-spec/revm-verif/revm-coq/links/dependencies.md

@@ -0,0 +1,51 @@
+# 🐓 dependencies.v
+
+[🐙 GitHub source](https://github.com/formal-land/coq-of-rust/tree/main/CoqOfRust/revm/links/dependencies.v)
+
+```coq
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+
+(*
+  /// Wrapper type around [`bytes::Bytes`] to support "0x" prefixed hex strings.
+  #[derive(Clone, Default, Hash, PartialEq, Eq, PartialOrd, Ord)]
+  #[repr(transparent)]
+  pub struct Bytes(pub bytes::Bytes);
+*)
+
+Module Bytes.
+  Parameter t : Set.
+
+  Global Instance IsToTy : ToTy t := {
+    Φ := Ty.path "bytes::bytes::Bytes";
+  }.
+
+  Global Instance IsToValue : ToValue t.
+  Admitted.
+End Bytes.
+
+Module Address.
+  Parameter t : Set.
+
+  Global Instance IsToTy : ToTy t := {
+    Φ := Ty.path "alloy_primitives::bits::address::Address";
+  }.
+
+  Global Instance IsToValue : ToValue t.
+  Admitted.
+End Address.
+
+Module FixedBytes.
+  Parameter t : Set.
+
+  Global Instance IsToTy : ToTy t := {
+    Φ := Ty.path "alloy_primitives::bits::fixed::FixedBytes";
+  }.
+
+  Global Instance IsToValue : ToValue t.
+  Admitted.
+End FixedBytes.
+
+Definition B256 := FixedBytes.t.
+Definition U256 := FixedBytes.t.
+```

docs/revm-python-spec/revm-verif/revm-coq/links/interpreter/interpreter.md

@@ -0,0 +1,103 @@
+# 🐓 interpreter.v
+
+[🐙 GitHub source](https://github.com/formal-land/coq-of-rust/tree/main/CoqOfRust/revm/links/interpreter/interpreter.v)
+
+```coq
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import CoqOfRust.revm.links.dependencies.
+Require Import CoqOfRust.revm.links.interpreter.interpreter.instruction_result.
+Require Import CoqOfRust.revm.links.interpreter.interpreter.gas.
+Require Import CoqOfRust.revm.links.interpreter.interpreter.contract.
+Require Import CoqOfRust.revm.links.interpreter.interpreter.shared_memory.
+Require Import CoqOfRust.revm.links.interpreter.interpreter.stack.
+Require Import CoqOfRust.revm.links.interpreter.interpreter.function_stack.
+Require Import CoqOfRust.revm.links.interpreter.interpreter_action.
+
+(*
+    /// EVM bytecode interpreter.
+    #[derive(Debug)]
+    pub struct Interpreter {
+        /// The current instruction pointer.
+        pub instruction_pointer: *const u8,
+        /// The gas state.
+        pub gas: Gas,
+        /// Contract information and invoking data
+        pub contract: Contract,
+        /// The execution control flag. If this is not set to `Continue`, the interpreter will stop
+        /// execution.
+        pub instruction_result: InstructionResult,
+        /// Currently run Bytecode that instruction result will point to.
+        /// Bytecode is owned by the contract.
+        pub bytecode: Bytes,
+        /// Whether we are Interpreting the Ethereum Object Format (EOF) bytecode.
+        /// This is local field that is set from `contract.is_eof()`.
+        pub is_eof: bool,
+        /// Is init flag for eof create
+        pub is_eof_init: bool,
+        /// Shared memory.
+        ///
+        /// Note: This field is only set while running the interpreter loop.
+        /// Otherwise it is taken and replaced with empty shared memory.
+        pub shared_memory: SharedMemory,
+        /// Stack.
+        pub stack: Stack,
+        /// EOF function stack.
+        pub function_stack: FunctionStack,
+        /// The return data buffer for internal calls.
+        /// It has multi usage:
+        ///
+        /// * It contains the output bytes of call sub call.
+        /// * When this interpreter finishes execution it contains the output bytes of this contract.
+        pub return_data_buffer: Bytes,
+        /// Whether the interpreter is in "staticcall" mode, meaning no state changes can happen.
+        pub is_static: bool,
+        /// Actions that the EVM should do.
+        ///
+        /// Set inside CALL or CREATE instructions and RETURN or REVERT instructions. Additionally those instructions will set
+        /// InstructionResult to CallOrCreate/Return/Revert so we know the reason.
+        pub next_action: InterpreterAction,
+    }
+*)
+
+Module Interpreter.
+  Record t : Set := {
+    instruction_pointer : Z;
+    gas : Gas.t;
+    contract : Contract.t;
+    instruction_result : InstructionResult.t;
+    Bytecode : Bytes.t;
+    IsEof : bool;
+    IsEofInit : bool;
+    SharedMemory : SharedMemory.t;
+    stack : Stack.t;
+    function_stack : FunctionStack.t;
+    return_data_buffer : Bytes.t;
+    is_static : bool;
+    next_action : InterpreterAction.t;
+  }.
+
+  Global Instance IsToTy : ToTy t := {
+    Φ := Ty.path "revm_interpreter::interpreter::Interpreter";
+  }.
+
+  Global Instance IsToValue : ToValue t := {
+    φ x :=
+      Value.StructRecord "revm_interpreter::interpreter::Interpreter" [
+        ("instruction_pointer", φ x.(instruction_pointer));
+        ("gas", φ x.(gas));
+        ("contract", φ x.(contract));
+        ("instruction_result", φ x.(instruction_result));
+        ("Bytecode", φ x.(Bytecode));
+        ("IsEof", φ x.(IsEof));
+        ("IsEofInit", φ x.(IsEofInit));
+        ("SharedMemory", φ x.(SharedMemory));
+        ("stack", φ x.(stack));
+        ("function_stack", φ x.(function_stack));
+        ("return_data_buffer", φ x.(return_data_buffer));
+        ("is_static", φ x.(is_static));
+        ("next_action", φ x.(next_action))
+      ];
+  }.
+End Interpreter.
+```

docs/revm-python-spec/revm-verif/revm-coq/links/interpreter/interpreter/contract.md

@@ -0,0 +1,59 @@
+# 🐓 contract.v
+
+[🐙 GitHub source](https://github.com/formal-land/coq-of-rust/tree/main/CoqOfRust/revm/links/interpreter/interpreter/contract.v)
+
+```coq
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import CoqOfRust.core.links.option.
+Require Import CoqOfRust.revm.links.dependencies.
+Require Import CoqOfRust.revm.links.primitives.bytecode.
+
+(*
+  /// EVM contract information.
+  #[derive(Clone, Debug, Default)]
+  #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
+  pub struct Contract {
+      /// Contracts data
+      pub input: Bytes,
+      /// Bytecode contains contract code, size of original code, analysis with gas block and jump table.
+      /// Note that current code is extended with push padding and STOP at end.
+      pub bytecode: Bytecode,
+      /// Bytecode hash for legacy. For EOF this would be None.
+      pub hash: Option<B256>,
+      /// Target address of the account. Storage of this address is going to be modified.
+      pub target_address: Address,
+      /// Caller of the EVM.
+      pub caller: Address,
+      /// Value send to contract from transaction or from CALL opcodes.
+      pub call_value: U256,
+  }
+*)
+
+Module Contract.
+  Record t : Set := {
+    input : Bytes.t;
+    bytecode : Bytecode.t;
+    hash : option B256;
+    target_address : Address.t;
+    caller : Address.t;
+    call_value : Z;
+  }.
+
+  Global Instance IsToTy : ToTy t := {
+    Φ := Ty.path "revm_interpreter::interpreter::contract::Contract";
+  }.
+
+  Global Instance IsToValue : ToValue t := {
+    φ x :=
+      Value.StructRecord "revm_interpreter::interpreter::contract::Contract" [
+        ("input", φ x.(input));
+        ("bytecode", φ x.(bytecode));
+        ("hash", φ x.(hash));
+        ("target_address", φ x.(target_address));
+        ("caller", φ x.(caller));
+        ("call_value", φ x.(call_value))
+      ];
+  }.
+End Contract.
+```