Simulations for the REVM arithmetic

.github/workflows/rust.yml

@@ -86,28 +86,28 @@ jobs:
             cargo coq-of-rust
             touch src/lib.rs
             cargo coq-of-rust
-            rsync -av src/ ../../../../CoqOfRust/revm/interpreter/ --include='*/' --include='*.v' --exclude='*'
+            rsync -av src/ ../../../../CoqOfRust/revm/translations/interpreter/ --include='*/' --include='*.v' --exclude='*'
             cd ..
             # precompile
             cd precompile
             cargo coq-of-rust
             touch src/lib.rs
             cargo coq-of-rust
-            rsync -av src/ ../../../../CoqOfRust/revm/precompile/ --include='*/' --include='*.v' --exclude='*'
+            rsync -av src/ ../../../../CoqOfRust/revm/translations/precompile/ --include='*/' --include='*.v' --exclude='*'
             cd ..
             # primitives
             cd primitives
             cargo coq-of-rust
             touch src/lib.rs
             cargo coq-of-rust
-            rsync -av src/ ../../../../CoqOfRust/revm/primitives/ --include='*/' --include='*.v' --exclude='*'
+            rsync -av src/ ../../../../CoqOfRust/revm/translations/primitives/ --include='*/' --include='*.v' --exclude='*'
             cd ..
             # revm
             cd revm
             cargo coq-of-rust
             touch src/lib.rs
             cargo coq-of-rust
-            rsync -av src/ ../../../../CoqOfRust/revm/revm/ --include='*/' --include='*.v' --exclude='*'
+            rsync -av src/ ../../../../CoqOfRust/revm/translations/revm/ --include='*/' --include='*.v' --exclude='*'
             cd ..
             cd ../../..
           endGroup

CoqOfRust/blacklist.txt

@@ -2,9 +2,9 @@ examples/default/examples/ink_contracts/proofs/erc20.v
 examples/default/examples/ink_contracts/proofs/lib.v
 examples/default/examples/ink_contracts/simulations/erc20.v
 examples/default/examples/ink_contracts/simulations/erc721.v
-revm/precompile/utilities.v
+revm/translations/precompile/utilities.v
 # This file works but is taking a very long time (ten minutes)
-revm/interpreter/opcode.v
+revm/translations/interpreter/opcode.v
 examples/default/examples/ink_contracts/proofs/erc721.v
 move/
 core/any.v

CoqOfRust/core/links/array.v

@@ -0,0 +1,12 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import links.M.
+
+Module Array.
+  Global Instance IsToTy (A : Set) (_ : ToTy A) : ToTy (list A) := {
+    Φ := Ty.apply (Ty.path "array") [Φ A];
+  }.
+
+  Global Instance IsToValue (A : Set) (_ : ToValue A) : ToValue (list A) := {
+    φ x := Value.Array (List.map φ x);
+  }.
+End Array.

CoqOfRust/core/links/bool.v

@@ -0,0 +1,13 @@
+Require Import Coq.Strings.String.
+Require Import links.M.
+Require Import CoqOfRust.lib.lib.
+
+Module Bool.
+  Global Instance IsToTy : ToTy bool := {
+    Φ := Ty.path "bool";
+  }.
+
+  Global Instance IsToValue : ToValue bool := {
+    φ := Value.Bool;
+  }.
+End Bool.

CoqOfRust/core/links/option.v

@@ -0,0 +1,16 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import links.M.
+
+Module Option.
+  Global Instance IsToTy (A : Set) (_ : ToTy A) : ToTy (option A) := {
+    Φ := Ty.apply (Ty.path "core::option::Option") [Φ A];
+  }.
+
+  Global Instance IsToValue (A : Set) (_ : ToValue A) : ToValue (option A) := {
+    φ x :=
+      match x with
+      | None => Value.StructTuple "core::option::Option::None" []
+      | Some x => Value.StructTuple "core::option::Option::Some" [φ x]
+      end;
+  }.
+End Option.

CoqOfRust/core/simulations/result.v → CoqOfRust/core/links/result.v

@@ -1,7 +1,5 @@
 Require Import CoqOfRust.CoqOfRust.
-Require Import simulations.M.
-Require CoqOfRust.core.simulations.default.
-Import simulations.M.Notations.
+Require Import links.M.
 
 Module Result.
   Global Instance IsToTy (A B : Set) (_ : ToTy A) (_ : ToTy B) : ToTy (A + B) := {

CoqOfRust/core/simulations/bool.v

@@ -1,17 +1,8 @@
 Require Import Coq.Strings.String.
 Require Import CoqOfRust.simulations.M.
-Require Import CoqOfRust.lib.lib.
 Import simulations.M.Notations.
 
 Module Bool.
-  Global Instance IsToTy : ToTy bool := {
-    Φ := Ty.path "bool";
-  }.
-
-  Global Instance IsToValue : ToValue bool := {
-    φ := Value.Bool;
-  }.
-
   Definition and {State Error} (x y : MS? State Error bool) : MS? State Error bool :=
     letS? a := x in
     if negb a

CoqOfRust/core/simulations/option.v

@@ -3,20 +3,6 @@ Require Import simulations.M.
 Require CoqOfRust.core.simulations.default.
 Import simulations.M.Notations.
 
-Module Option.
-  Global Instance IsToTy (A : Set) (_ : ToTy A) : ToTy (option A) := {
-    Φ := Ty.apply (Ty.path "core::option::Option") [Φ A];
-  }.
-
-  Global Instance IsToValue (A : Set) (_ : ToValue A) : ToValue (option A) := {
-    φ x :=
-      match x with
-      | None => Value.StructTuple "core::option::Option::None" []
-      | Some x => Value.StructTuple "core::option::Option::Some" [φ x]
-      end;
-  }.
-End Option.
-
 Module Impl_Option_T.
   Definition Self (T : Set) : Set :=
     option T.

CoqOfRust/revm/links/dependencies.v

@@ -0,0 +1,45 @@
+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.

CoqOfRust/revm/links/interpreter/interpreter.v

@@ -0,0 +1,97 @@
+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.

CoqOfRust/revm/links/interpreter/interpreter/contract.v

@@ -0,0 +1,53 @@
+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.