diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml
index 82098ef96..c38a23411 100644
--- a/.github/workflows/rust.yml
+++ b/.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
diff --git a/CoqOfRust/blacklist.txt b/CoqOfRust/blacklist.txt
index b0737bdab..a48700014 100644
--- a/CoqOfRust/blacklist.txt
+++ b/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
diff --git a/CoqOfRust/core/links/array.v b/CoqOfRust/core/links/array.v
new file mode 100644
index 000000000..bacf9844d
--- /dev/null
+++ b/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.
diff --git a/CoqOfRust/core/links/bool.v b/CoqOfRust/core/links/bool.v
new file mode 100644
index 000000000..9dd256bda
--- /dev/null
+++ b/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.
diff --git a/CoqOfRust/core/links/option.v b/CoqOfRust/core/links/option.v
new file mode 100644
index 000000000..3e9c5b2a9
--- /dev/null
+++ b/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.
diff --git a/CoqOfRust/core/simulations/result.v b/CoqOfRust/core/links/result.v
similarity index 82%
rename from CoqOfRust/core/simulations/result.v
rename to CoqOfRust/core/links/result.v
index e0505baa1..5cc49360b 100644
--- a/CoqOfRust/core/simulations/result.v
+++ b/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) := {
diff --git a/CoqOfRust/core/simulations/bool.v b/CoqOfRust/core/simulations/bool.v
index 67bfb402b..200feba74 100644
--- a/CoqOfRust/core/simulations/bool.v
+++ 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
diff --git a/CoqOfRust/core/simulations/option.v b/CoqOfRust/core/simulations/option.v
index f52f6644e..123753d72 100644
--- a/CoqOfRust/core/simulations/option.v
+++ b/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.
diff --git a/CoqOfRust/revm/links/dependencies.v b/CoqOfRust/revm/links/dependencies.v
new file mode 100644
index 000000000..fbcf48c70
--- /dev/null
+++ b/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.
diff --git a/CoqOfRust/revm/links/interpreter/interpreter.v b/CoqOfRust/revm/links/interpreter/interpreter.v
new file mode 100644
index 000000000..d6d1726fe
--- /dev/null
+++ b/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.
diff --git a/CoqOfRust/revm/links/interpreter/interpreter/contract.v b/CoqOfRust/revm/links/interpreter/interpreter/contract.v
new file mode 100644
index 000000000..284d144d2
--- /dev/null
+++ b/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.
diff --git a/CoqOfRust/revm/links/interpreter/interpreter/function_stack.v b/CoqOfRust/revm/links/interpreter/interpreter/function_stack.v
new file mode 100644
index 000000000..398d0a914
--- /dev/null
+++ b/CoqOfRust/revm/links/interpreter/interpreter/function_stack.v
@@ -0,0 +1,65 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import CoqOfRust.core.links.array.
+
+(*
+  /// Function return frame.
+  /// Needed information for returning from a function.
+  #[derive(Debug, Default, Clone, Copy, PartialEq, Eq, Hash)]
+  #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
+  pub struct FunctionReturnFrame {
+      /// The index of the code container that this frame is executing.
+      pub idx: usize,
+      /// The program counter where frame execution should continue.
+      pub pc: usize,
+  }
+*)
+
+Module FunctionReturnFrame.
+  Record t : Set := {
+    idx : Z;
+    pc : Z;
+  }.
+
+  Global Instance IsToTy : ToTy t := {
+    Φ := Ty.path "revm_interpreter::interpreter::function_return_frame::FunctionReturnFrame";
+  }.
+
+  Global Instance IsToValue : ToValue t := {
+    φ x :=
+      Value.StructRecord "revm_interpreter::interpreter::function_return_frame::FunctionReturnFrame" [
+        ("idx", φ x.(idx));
+        ("pc", φ x.(pc))
+      ];
+  }.
+End FunctionReturnFrame.
+
+(*
+  /// Function Stack
+  #[derive(Debug, Default)]
+  #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
+  pub struct FunctionStack {
+      pub return_stack: Vec<FunctionReturnFrame>,
+      pub current_code_idx: usize,
+  }
+*)
+
+(* TODO: Vectors? *)
+Module FunctionStack.
+  Record t : Set := {
+    return_stack : list FunctionReturnFrame.t;
+    current_code_idx : Z;
+  }.
+
+  Global Instance IsToTy : ToTy t := {
+    Φ := Ty.path "revm_interpreter::interpreter::function_stack::FunctionStack";
+  }.
+
+  Global Instance IsToValue : ToValue t := {
+    φ x :=
+      Value.StructRecord "revm_interpreter::interpreter::function_stack::FunctionStack" [
+        ("return_stack", φ x.(return_stack));
+        ("current_code_idx", φ x.(current_code_idx))
+      ];
+  }.
+End FunctionStack.
diff --git a/CoqOfRust/revm/interpreter/links/gas.v b/CoqOfRust/revm/links/interpreter/interpreter/gas.v
similarity index 96%
rename from CoqOfRust/revm/interpreter/links/gas.v
rename to CoqOfRust/revm/links/interpreter/interpreter/gas.v
index 18cd9d4bc..d0ebcee13 100644
--- a/CoqOfRust/revm/interpreter/links/gas.v
+++ b/CoqOfRust/revm/links/interpreter/interpreter/gas.v
@@ -1,19 +1,25 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
 Require core.links.clone.
-Require Import revm.interpreter.gas.
+Require Import revm.translations.interpreter.gas.
 
 Import Run.
 
-Module Gas.
-  (* pub struct Gas {
+(*
+  /// Represents the state of gas during execution.
+  #[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Hash)]
+  #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
+  pub struct Gas {
       /// The initial gas limit. This is constant throughout execution.
       limit: u64,
       /// The remaining gas.
       remaining: u64,
       /// Refunded gas. This is used only at the end of execution.
       refunded: i64,
-  } *)
+  }
+*)
+
+Module Gas.
   Record t : Set := {
     limit : Z;
     remaining : Z;
@@ -33,6 +39,7 @@ Module Gas.
       ];
   }.
 
+  
   Module SubPointer.
     Definition get_limit : SubPointer.Runner.t t Z := {|
       SubPointer.Runner.index :=
diff --git a/CoqOfRust/revm/links/interpreter/interpreter/instruction_result.v b/CoqOfRust/revm/links/interpreter/interpreter/instruction_result.v
new file mode 100644
index 000000000..60732ec68
--- /dev/null
+++ b/CoqOfRust/revm/links/interpreter/interpreter/instruction_result.v
@@ -0,0 +1,145 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+
+(*
+  #[repr(u8)]
+  #[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Hash)]
+  #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
+  pub enum InstructionResult {
+      // success codes
+      #[default]
+      Continue = 0x00,
+      Stop,
+      Return,
+      SelfDestruct,
+      ReturnContract,
+
+      // revert codes
+      Revert = 0x10, // revert opcode
+      CallTooDeep,
+      OutOfFunds,
+
+      // Actions
+      CallOrCreate = 0x20,
+
+      // error codes
+      OutOfGas = 0x50,
+      MemoryOOG,
+      MemoryLimitOOG,
+      PrecompileOOG,
+      InvalidOperandOOG,
+      OpcodeNotFound,
+      CallNotAllowedInsideStatic,
+      StateChangeDuringStaticCall,
+      InvalidFEOpcode,
+      InvalidJump,
+      NotActivated,
+      StackUnderflow,
+      StackOverflow,
+      OutOfOffset,
+      CreateCollision,
+      OverflowPayment,
+      PrecompileError,
+      NonceOverflow,
+      /// Create init code size exceeds limit (runtime).
+      CreateContractSizeLimit,
+      /// Error on created contract that begins with EF
+      CreateContractStartingWithEF,
+      /// EIP-3860: Limit and meter initcode. Initcode size limit exceeded.
+      CreateInitCodeSizeLimit,
+      /// Fatal external error. Returned by database.
+      FatalExternalError,
+      /// RETURNCONTRACT called in not init eof code.
+      ReturnContractInNotInitEOF,
+      /// Legacy contract is calling opcode that is enabled only in EOF.
+      EOFOpcodeDisabledInLegacy,
+      /// EOF function stack overflow
+      EOFFunctionStackOverflow,
+  }
+*)
+
+Module InstructionResult.
+  Inductive t : Set :=
+  (* success codes *)
+  | Continue
+  | Stop
+  | Return
+  | SelfDestruct
+  | ReturnContract
+  (* revert codes *)
+  | Revert
+  | CallTooDeep
+  | OutOfFunds
+  (* Actions *)
+  | CallOrCreate
+  (* error codes *)
+  | OutOfGas
+  | MemoryOOG
+  | MemoryLimitOOG
+  | PrecompileOOG
+  | InvalidOperandOOG
+  | OpcodeNotFound
+  | CallNotAllowedInsideStatic
+  | StateChangeDuringStaticCall
+  | InvalidFEOpcode
+  | InvalidJump
+  | NotActivated
+  | StackUnderflow
+  | StackOverflow
+  | OutOfOffset
+  | CreateCollision
+  | OverflowPayment
+  | PrecompileError
+  | NonceOverflow
+  | CreateContractSizeLimit
+  | CreateContractStartingWithEF
+  | CreateInitCodeSizeLimit
+  | FatalExternalError
+  | ReturnContractInNotInitEOF
+  | EOFOpcodeDisabledInLegacy
+  | EOFFunctionStackOverflow.
+
+  Global Instance IsToTy : ToTy t := {
+    Φ := Ty.path "revm_interpreter::instruction_result::InstructionResult";
+  }.
+
+  Global Instance IsToValue : ToValue t := {
+    φ x :=
+      match x with
+      | Continue => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::Continue" []
+      | Stop => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::Stop" []
+      | Return => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::Return" []
+      | SelfDestruct => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::SelfDestruct" []
+      | ReturnContract => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::ReturnContract" []
+      | Revert => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::Revert" []
+      | CallTooDeep => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CallTooDeep" []
+      | OutOfFunds => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::OutOfFunds" []
+      | CallOrCreate => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CallOrCreate" []
+      | OutOfGas => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::OutOfGas" []
+      | MemoryOOG => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::MemoryOOG" []
+      | MemoryLimitOOG => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::MemoryLimitOOG" []
+      | PrecompileOOG => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::PrecompileOOG" []
+      | InvalidOperandOOG => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::InvalidOperandOOG" []
+      | OpcodeNotFound => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::OpcodeNotFound" []
+      | CallNotAllowedInsideStatic => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CallNotAllowedInsideStatic" []
+      | StateChangeDuringStaticCall => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::StateChangeDuringStaticCall" []
+      | InvalidFEOpcode => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::InvalidFEOpcode" []
+      | InvalidJump => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::InvalidJump" []
+      | NotActivated => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::NotActivated" []
+      | StackUnderflow => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::StackUnderflow" []
+      | StackOverflow => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::StackOverflow" []
+      | OutOfOffset => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::OutOfOffset" []
+      | CreateCollision => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CreateCollision" []
+      | OverflowPayment => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::OverflowPayment" []
+      | PrecompileError => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::PrecompileError" []
+      | NonceOverflow => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::NonceOverflow" []
+      | CreateContractSizeLimit => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CreateContractSizeLimit" []
+      | CreateContractStartingWithEF => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CreateContractStartingWithEF" []
+      | CreateInitCodeSizeLimit => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CreateInitCodeSizeLimit" []
+      | FatalExternalError => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::FatalExternalError" []
+      | ReturnContractInNotInitEOF => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::ReturnContractInNotInitEOF" []
+      | EOFOpcodeDisabledInLegacy => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::EOFOpcodeDisabledInLegacy" []
+      | EOFFunctionStackOverflow => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::EOFFunctionStackOverflow" []
+      end;
+  }.
+End InstructionResult.
diff --git a/CoqOfRust/revm/links/interpreter/interpreter/shared_memory.v b/CoqOfRust/revm/links/interpreter/interpreter/shared_memory.v
new file mode 100644
index 000000000..77140c79d
--- /dev/null
+++ b/CoqOfRust/revm/links/interpreter/interpreter/shared_memory.v
@@ -0,0 +1,48 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import CoqOfRust.core.links.option.
+Require Import CoqOfRust.core.links.array.
+
+(*
+  /// A sequential memory shared between calls, which uses
+  /// a `Vec` for internal representation.
+  /// A [SharedMemory] instance should always be obtained using
+  /// the `new` static method to ensure memory safety.
+  #[derive(Clone, PartialEq, Eq, Hash)]
+  #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
+  pub struct SharedMemory {
+      /// The underlying buffer.
+      buffer: Vec<u8>,
+      /// Memory checkpoints for each depth.
+      /// Invariant: these are always in bounds of `data`.
+      checkpoints: Vec<usize>,
+      /// Invariant: equals `self.checkpoints.last()`
+      last_checkpoint: usize,
+      /// Memory limit. See [`CfgEnv`](revm_primitives::CfgEnv).
+      #[cfg(feature = "memory_limit")]
+      memory_limit: u64,
+  }
+*)
+
+Module SharedMemory.
+  Record t : Set := {
+    buffer : list Z;
+    checkpoints : list Z;
+    last_checkpoint : Z;
+    memory_limit : option Z;
+  }.
+
+  Global Instance IsToTy : ToTy t := {
+    Φ := Ty.path "revm_interpreter::interpreter::shared_memory::SharedMemory";
+  }.
+
+  Global Instance IsToValue : ToValue t := {
+    φ x :=
+      Value.StructRecord "revm_interpreter::interpreter::shared_memory::SharedMemory" [
+        ("buffer", φ x.(buffer));
+        ("checkpoints", φ x.(checkpoints));
+        ("last_checkpoint", φ x.(last_checkpoint));
+        ("memory_limit", φ x.(memory_limit))
+      ];
+  }.
+End SharedMemory.
diff --git a/CoqOfRust/revm/links/interpreter/interpreter/stack.v b/CoqOfRust/revm/links/interpreter/interpreter/stack.v
new file mode 100644
index 000000000..7725d9a97
--- /dev/null
+++ b/CoqOfRust/revm/links/interpreter/interpreter/stack.v
@@ -0,0 +1,28 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import CoqOfRust.core.links.array.
+Require Import CoqOfRust.revm.links.dependencies.
+
+(*
+  /// EVM stack with [STACK_LIMIT] capacity of words.
+  #[derive(Debug, PartialEq, Eq, Hash)]
+  #[cfg_attr(feature = "serde", derive(serde::Serialize))]
+  pub struct Stack {
+      /// The underlying data of the stack.
+      data: Vec<U256>,
+  }
+*)
+
+Module Stack.
+  Inductive t : Set :=
+  | data : list U256 -> t.
+
+  Global Instance IsToTy : ToTy t := {
+    Φ := Ty.path "revm_interpreter::interpreter::stack::Stack";
+  }.
+
+  Global Instance IsToValue : ToValue t := {
+    φ '(data x) := 
+      Value.StructRecord "revm_interpreter::interpreter::stack::Stack" [("data", φ x)]
+  }.
+End Stack.
diff --git a/CoqOfRust/revm/links/interpreter/interpreter_action.v b/CoqOfRust/revm/links/interpreter/interpreter_action.v
new file mode 100644
index 000000000..4234a8bcd
--- /dev/null
+++ b/CoqOfRust/revm/links/interpreter/interpreter_action.v
@@ -0,0 +1,87 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import CoqOfRust.revm.links.dependencies.
+Require Import CoqOfRust.revm.links.interpreter.interpreter_action.call_inputs.
+Require Import CoqOfRust.revm.links.interpreter.interpreter_action.create_inputs.
+Require Import CoqOfRust.revm.links.interpreter.interpreter_action.eof_create_inputs.
+Require Import CoqOfRust.revm.links.interpreter.interpreter.instruction_result.
+Require Import CoqOfRust.revm.links.interpreter.interpreter.gas.
+
+(*
+  /// The result of an interpreter operation.
+  #[derive(Clone, Debug, PartialEq, Eq)]
+  #[cfg_attr(feature = "serde", derive(::serde::Serialize, ::serde::Deserialize))]
+  pub struct InterpreterResult {
+      /// The result of the instruction execution.
+      pub result: InstructionResult,
+      /// The output of the instruction execution.
+      pub output: Bytes,
+      /// The gas usage information.
+      pub gas: Gas,
+  }
+*)
+
+Module InterpreterResult.
+  Record t : Set := {
+    result : InstructionResult.t;
+    output : Bytes.t;
+    gas : Gas.t;
+  }.
+
+  Global Instance IsToTy : ToTy t := {
+    Φ := Ty.path "revm_interpreter::interpreter::InterpreterResult";
+  }.
+
+  Global Instance IsToValue : ToValue t := {
+    φ x :=
+      Value.StructRecord "revm_interpreter::interpreter::InterpreterResult" [
+        ("result", φ x.(result));
+        ("output", φ x.(output));
+        ("gas", φ x.(gas))
+      ];
+  }.
+End InterpreterResult.
+
+(*
+  #[derive(Clone, Debug, Default, PartialEq, Eq)]
+  #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
+  pub enum InterpreterAction {
+      /// CALL, CALLCODE, DELEGATECALL, STATICCALL
+      /// or EOF EXT instuction called.
+      Call { inputs: Box<CallInputs> },
+      /// CREATE or CREATE2 instruction called.
+      Create { inputs: Box<CreateInputs> },
+      /// EOF CREATE instruction called.
+      EOFCreate { inputs: Box<EOFCreateInput> },
+      /// Interpreter finished execution.
+      Return { result: InterpreterResult },
+      /// No action
+      #[default]
+      None,
+  }
+*)
+
+(* TODO: Box? *)
+Module InterpreterAction.
+  Inductive t : Set :=
+  | Call : CallInputs.t -> t
+  | Create : CreateInputs.t -> t
+  | EOFCreate : EOFCreateInput.t -> t
+  | Return : InterpreterResult.t -> t
+  | None.
+
+  Global Instance IsToTy : ToTy t := {
+    Φ := Ty.path "revm_interpreter::interpreter_action::InterpreterAction";
+  }.
+
+  Global Instance IsToValue : ToValue t := {
+    φ x :=
+      match x with
+      | Call x => Value.StructRecord "revm_interpreter::interpreter_action::InterpreterAction::Call" [("inputs", φ x)]
+      | Create x => Value.StructRecord "revm_interpreter::interpreter_action::InterpreterAction::Create" [("inputs", φ x)]
+      | EOFCreate x => Value.StructRecord "revm_interpreter::interpreter_action::InterpreterAction::EOFCreate" [("inputs", φ x)]
+      | Return x => Value.StructRecord "revm_interpreter::interpreter_action::InterpreterAction::Return" [("result", φ x)]
+      | None => Value.StructRecord "revm_interpreter::interpreter_action::InterpreterAction::None" []
+      end;
+  }.
+End InterpreterAction.
diff --git a/CoqOfRust/revm/links/interpreter/interpreter_action/call_inputs.v b/CoqOfRust/revm/links/interpreter/interpreter_action/call_inputs.v
new file mode 100644
index 000000000..3b4bc8101
--- /dev/null
+++ b/CoqOfRust/revm/links/interpreter/interpreter_action/call_inputs.v
@@ -0,0 +1,153 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import CoqOfRust.core.links.bool.
+Require Import CoqOfRust.revm.links.dependencies.
+
+(*
+  /// Call value.
+  #[derive(Clone, Debug, PartialEq, Eq, Hash)]
+  #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
+  pub enum CallValue {
+      /// Concrete value, transferred from caller to callee at the end of the transaction.
+      Transfer(U256),
+      /// Apparent value, that is **not** actually transferred.
+      ///
+      /// Set when in a `DELEGATECALL` call type, and used by the `CALLVALUE` opcode.
+      Apparent(U256),
+  }
+*)
+
+Module CallValue.
+  Inductive t : Set :=
+  | Transfer : Z -> t
+  | Apparent : Z -> t.
+
+  Global Instance IsToTy : ToTy t := {
+    Φ := Ty.path "revm_interpreter::interpreter_action::call_inputs::CallValue";
+  }.
+
+  Global Instance IsToValue : ToValue t := {
+    φ x :=
+      match x with
+      | Transfer x => Value.StructTuple "revm_interpreter::interpreter_action::call_inputs::CallValue::Transfer" [φ x]
+      | Apparent x => Value.StructTuple "revm_interpreter::interpreter_action::call_inputs::CallValue::Approval" [φ x]
+      end;
+  }.
+End CallValue.
+
+(*
+  /// Call scheme.
+  #[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
+  #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
+  pub enum CallScheme {
+      /// `CALL`.
+      Call,
+      /// `CALLCODE`
+      CallCode,
+      /// `DELEGATECALL`
+      DelegateCall,
+      /// `STATICCALL`
+      StaticCall,
+  }
+*)
+
+Module CallScheme.
+  Inductive t : Set :=
+  | Call
+  | CallCode
+  | DelegateCall
+  | StaticCall.
+
+  Global Instance IsToTy : ToTy t := {
+    Φ := Ty.path "revm_interpreter::interpreter_action::call_inputs::CallScheme";
+  }.
+
+  Global Instance IsToValue : ToValue t := {
+    φ x :=
+      match x with
+      | Call => Value.StructTuple "revm_interpreter::interpreter_action::call_inputs::CallScheme::Call" []
+      | CallCode => Value.StructTuple "revm_interpreter::interpreter_action::call_inputs::CallScheme::CallCode" []
+      | DelegateCall => Value.StructTuple "revm_interpreter::interpreter_action::call_inputs::CallScheme::DelegateCall" []
+      | StaticCall => Value.StructTuple "revm_interpreter::interpreter_action::call_inputs::CallScheme::StaticCall" []
+      end;
+  }.
+End CallScheme.
+
+
+(*
+  /// Inputs for a call.
+  #[derive(Clone, Debug, PartialEq, Eq, Hash)]
+  #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
+  pub struct CallInputs {
+      /// The call data of the call.
+      pub input: Bytes,
+      /// The return memory offset where the output of the call is written.
+      ///
+      /// In EOF, this range is invalid as EOF calls do not write output to memory.
+      pub return_memory_offset: Range<usize>,
+      /// The gas limit of the call.
+      pub gas_limit: u64,
+      /// The account address of bytecode that is going to be executed.
+      ///
+      /// Previously `context.code_address`.
+      pub bytecode_address: Address,
+      /// Target address, this account storage is going to be modified.
+      ///
+      /// Previously `context.address`.
+      pub target_address: Address,
+      /// This caller is invoking the call.
+      ///
+      /// Previously `context.caller`.
+      pub caller: Address,
+      /// Call value.
+      ///
+      /// NOTE: This value may not necessarily be transferred from caller to callee, see [`CallValue`].
+      ///
+      /// Previously `transfer.value` or `context.apparent_value`.
+      pub value: CallValue,
+      /// The call scheme.
+      ///
+      /// Previously `context.scheme`.
+      pub scheme: CallScheme,
+      /// Whether the call is a static call, or is initiated inside a static call.
+      pub is_static: bool,
+      /// Whether the call is initiated from EOF bytecode.
+      pub is_eof: bool,
+  }
+*)
+
+(* TODO: Ranges? *)
+Module CallInputs.
+  Record t : Set := {
+    input : Bytes.t;
+    return_memory_offset : (Z * Z);
+    gas_limit : Z;
+    bytecode_address : Address.t;
+    target_address : Address.t;
+    caller : Address.t;
+    value : CallValue.t;
+    scheme : CallScheme.t;
+    is_static : bool;
+    is_eof : bool;
+  }.
+
+  Global Instance IsToTy : ToTy t := {
+    Φ := Ty.path "revm_interpreter::interpreter::call_inputs::CallInputs";
+  }.
+
+  Global Instance IsToValue : ToValue t := {
+    φ x :=
+      Value.StructRecord "revm_interpreter::interpreter::call_inputs::CallInputs" [
+        ("input", φ x.(input));
+        ("return_memory_offset", φ x.(return_memory_offset));
+        ("gas_limit", φ x.(gas_limit));
+        ("bytecode_address", φ x.(bytecode_address));
+        ("target_address", φ x.(target_address));
+        ("caller", φ x.(caller));
+        ("value", φ x.(value));
+        ("scheme", φ x.(scheme));
+        ("is_static", φ x.(is_static));
+        ("is_eof", φ x.(is_eof))
+      ];
+  }.
+End CallInputs.
diff --git a/CoqOfRust/revm/links/interpreter/interpreter_action/create_inputs.v b/CoqOfRust/revm/links/interpreter/interpreter_action/create_inputs.v
new file mode 100644
index 000000000..2589647e6
--- /dev/null
+++ b/CoqOfRust/revm/links/interpreter/interpreter_action/create_inputs.v
@@ -0,0 +1,47 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import CoqOfRust.revm.links.dependencies.
+Require Import CoqOfRust.revm.links.primitives.env.
+
+(*
+  /// Inputs for a create call.
+  #[derive(Clone, Debug, PartialEq, Eq, Hash)]
+  #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
+  pub struct CreateInputs {
+      /// Caller address of the EVM.
+      pub caller: Address,
+      /// The create scheme.
+      pub scheme: CreateScheme,
+      /// The value to transfer.
+      pub value: U256,
+      /// The init code of the contract.
+      pub init_code: Bytes,
+      /// The gas limit of the call.
+      pub gas_limit: u64,
+  }
+*)
+
+Module CreateInputs.
+  Record t : Set := {
+    caller : Address.t;
+    scheme : CreateScheme.t;
+    value : U256;
+    init_code : Bytes.t;
+    gas_limit : Z;
+  }.
+
+  Global Instance IsToTy : ToTy t := {
+    Φ := Ty.path "revm_interpreter::interpreter::create_inputs::CreateInputs";
+  }.
+
+  Global Instance IsToValue : ToValue t := {
+    φ x :=
+      Value.StructRecord "revm_interpreter::interpreter::create_inputs::CreateInputs" [
+        ("caller", φ x.(caller));
+        ("scheme", φ x.(scheme));
+        ("value", φ x.(value));
+        ("init_code", φ x.(init_code));
+        ("gas_limit", φ x.(gas_limit))
+      ];
+  }.
+End CreateInputs.
diff --git a/CoqOfRust/revm/links/interpreter/interpreter_action/eof_create_inputs.v b/CoqOfRust/revm/links/interpreter/interpreter_action/eof_create_inputs.v
new file mode 100644
index 000000000..7512bb822
--- /dev/null
+++ b/CoqOfRust/revm/links/interpreter/interpreter_action/eof_create_inputs.v
@@ -0,0 +1,52 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import CoqOfRust.revm.links.dependencies.
+Require Import CoqOfRust.revm.links.primitives.bytecode.eof.
+
+(*
+  /// Inputs for EOF create call.
+  #[derive(Debug, Default, Clone, PartialEq, Eq)]
+  #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
+  pub struct EOFCreateInput {
+      /// Caller of Eof Craate
+      pub caller: Address,
+      /// New contract address.
+      pub created_address: Address,
+      /// Values of ether transfered
+      pub value: U256,
+      /// Init eof code that is going to be executed.
+      pub eof_init_code: Eof,
+      /// Gas limit for the create call.
+      pub gas_limit: u64,
+      /// Return memory range. If EOF creation Reverts it can return the
+      /// the memory range.
+      pub return_memory_range: Range<usize>,
+  }
+*)
+
+Module EOFCreateInput.
+  Record t : Set := {
+    caller : Address.t;
+    created_address : Address.t;
+    value : U256;
+    eof_init_code : Eof.t;
+    gas_limit : Z;
+    return_memory_range : (Z * Z);
+  }.
+
+  Global Instance IsToTy : ToTy t := {
+    Φ := Ty.path "revm_interpreter::interpreter::eof_create_input::EOFCreateInput";
+  }.
+
+  Global Instance IsToValue : ToValue t := {
+    φ x :=
+      Value.StructRecord "revm_interpreter::interpreter::eof_create_input::EOFCreateInput" [
+        ("caller", φ x.(caller));
+        ("created_address", φ x.(created_address));
+        ("value", φ x.(value));
+        ("eof_init_code", φ x.(eof_init_code));
+        ("gas_limit", φ x.(gas_limit));
+        ("return_memory_range", φ x.(return_memory_range))
+      ];
+  }.
+End EOFCreateInput.
diff --git a/CoqOfRust/revm/links/primitives/bytecode.v b/CoqOfRust/revm/links/primitives/bytecode.v
new file mode 100644
index 000000000..44c7335fe
--- /dev/null
+++ b/CoqOfRust/revm/links/primitives/bytecode.v
@@ -0,0 +1,27 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+
+(*
+    /// State of the [`Bytecode`] analysis.
+    #[derive(Clone, Debug, PartialEq, Eq, Hash)]
+    #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
+    pub enum Bytecode {
+        /// No analysis has been performed.
+        LegacyRaw(Bytes),
+        /// The bytecode has been analyzed for valid jump destinations.
+        LegacyAnalyzed(LegacyAnalyzedBytecode),
+        /// Ethereum Object Format
+        Eof(Eof),
+    }
+*)
+
+Module Bytecode.
+  Parameter t : Set.
+
+  Global Instance IsToTy : ToTy t := {
+    Φ := Ty.path "revm_primitives::bytecode::Bytecode";
+  }.
+
+  Global Instance IsToValue : ToValue t.
+  Admitted.
+End Bytecode.
diff --git a/CoqOfRust/revm/links/primitives/bytecode/eof.v b/CoqOfRust/revm/links/primitives/bytecode/eof.v
new file mode 100644
index 000000000..19c363752
--- /dev/null
+++ b/CoqOfRust/revm/links/primitives/bytecode/eof.v
@@ -0,0 +1,43 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import CoqOfRust.revm.links.dependencies.
+Require Import CoqOfRust.revm.links.primitives.bytecode.eof.header.
+Require Import CoqOfRust.revm.links.primitives.bytecode.eof.body.
+
+(*
+  /// EOF - Ethereum Object Format.
+  ///
+  /// It consist of a header, body and raw original bytes Specified in EIP.
+  /// Most of body contain Bytes so it references to the raw bytes.
+  ///
+  /// If there is a need to create new EOF from scratch, it is recommended to use `EofBody` and
+  /// use `encode` function to create full [`Eof`] object.
+  #[derive(Clone, Debug, PartialEq, Eq, Hash)]
+  #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
+  pub struct Eof {
+      pub header: EofHeader,
+      pub body: EofBody,
+      pub raw: Bytes,
+  }
+*)
+
+Module Eof.
+  Record t : Set := {
+    header : EofHeader.t;
+    body : EofBody.t;
+    raw : Bytes.t;
+  }.
+
+  Global Instance IsToTy : ToTy t := {
+    Φ := Ty.path "revm_primitives::bytecode::eof::Eof";
+  }.
+
+  Global Instance IsToValue : ToValue t := {
+    φ x :=
+      Value.StructRecord "revm_primitives::bytecode::eof::Eof" [
+        ("header", φ x.(header));
+        ("body", φ x.(body));
+        ("raw", φ x.(raw))
+      ];
+  }.
+End Eof.
diff --git a/CoqOfRust/revm/links/primitives/bytecode/eof/body.v b/CoqOfRust/revm/links/primitives/bytecode/eof/body.v
new file mode 100644
index 000000000..b54ddc0a1
--- /dev/null
+++ b/CoqOfRust/revm/links/primitives/bytecode/eof/body.v
@@ -0,0 +1,46 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import CoqOfRust.core.links.bool.
+Require Import CoqOfRust.core.links.array.
+Require Import CoqOfRust.revm.links.dependencies.
+Require Import CoqOfRust.revm.links.primitives.bytecode.eof.type_section.
+
+(*
+  /// EOF Body, contains types, code, container and data sections.
+  ///
+  /// Can be used to create new EOF object.
+  #[derive(Clone, Debug, Default, PartialEq, Eq, Hash)]
+  #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
+  pub struct EofBody {
+      pub types_section: Vec<TypesSection>,
+      pub code_section: Vec<Bytes>,
+      pub container_section: Vec<Bytes>,
+      pub data_section: Bytes,
+      pub is_data_filled: bool,
+  }
+*)
+
+Module EofBody.
+  Record t : Set := {
+    types_section : list TypesSection.t;
+    code_section : list Bytes.t;
+    container_section : list Bytes.t;
+    data_section : Bytes.t;
+    is_data_filled : bool;
+  }.
+
+  Global Instance IsToTy : ToTy t := {
+    Φ := Ty.path "revm_primitives::bytecode::eof::body::EofBody";
+  }.
+
+  Global Instance IsToValue : ToValue t := {
+    φ x :=
+      Value.StructRecord "revm_primitives::bytecode::eof::body::EofBody" [
+        ("types_section", φ x.(types_section));
+        ("code_section", φ x.(code_section));
+        ("container_section", φ x.(container_section));
+        ("data_section", φ x.(data_section));
+        ("is_data_filled", φ x.(is_data_filled))
+      ];
+  }.
+End EofBody.
diff --git a/CoqOfRust/revm/links/primitives/bytecode/eof/header.v b/CoqOfRust/revm/links/primitives/bytecode/eof/header.v
new file mode 100644
index 000000000..a4a4b386b
--- /dev/null
+++ b/CoqOfRust/revm/links/primitives/bytecode/eof/header.v
@@ -0,0 +1,53 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import CoqOfRust.core.links.array.
+
+(*
+  /// EOF Header containing
+  #[derive(Clone, Debug, Default, PartialEq, Eq, Hash)]
+  #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
+  pub struct EofHeader {
+      /// Size of EOF types section.
+      /// types section includes num of input and outputs and max stack size.
+      pub types_size: u16,
+      /// Sizes of EOF code section.
+      /// Code size can't be zero.
+      pub code_sizes: Vec<u16>,
+      /// EOF Container size.
+      /// Container size can be zero.
+      pub container_sizes: Vec<u16>,
+      /// EOF data size.
+      pub data_size: u16,
+      /// sum code sizes
+      pub sum_code_sizes: usize,
+      /// sum container sizes
+      pub sum_container_sizes: usize,
+  }
+*)
+
+Module EofHeader.
+  Record t : Set := {
+    types_size : Z;
+    code_sizes : list Z;
+    container_sizes : list Z;
+    data_size : Z;
+    sum_code_sizes : Z;
+    sum_container_sizes : Z;
+  }.
+
+  Global Instance IsToTy : ToTy t := {
+    Φ := Ty.path "revm_primitives::bytecode::eof::header::EofHeader";
+  }.
+
+  Global Instance IsToValue : ToValue t := {
+    φ x :=
+      Value.StructRecord "revm_primitives::bytecode::eof::header::EofHeader" [
+        ("types_size", φ x.(types_size));
+        ("code_sizes", φ x.(code_sizes));
+        ("container_sizes", φ x.(container_sizes));
+        ("data_size", φ x.(data_size));
+        ("sum_code_sizes", φ x.(sum_code_sizes));
+        ("sum_container_sizes", φ x.(sum_container_sizes))
+      ];
+  }.
+End EofHeader.
diff --git a/CoqOfRust/revm/links/primitives/bytecode/eof/type_section.v b/CoqOfRust/revm/links/primitives/bytecode/eof/type_section.v
new file mode 100644
index 000000000..77468e67a
--- /dev/null
+++ b/CoqOfRust/revm/links/primitives/bytecode/eof/type_section.v
@@ -0,0 +1,41 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+
+
+(*
+  /// Types section that contains stack information for matching code section.
+  #[derive(Debug, Clone, Default, Hash, PartialEq, Eq, Copy)]
+  #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
+  pub struct TypesSection {
+      /// inputs - 1 byte - `0x00-0x7F`
+      /// number of stack elements the code section consumes
+      pub inputs: u8,
+      /// outputs - 1 byte - `0x00-0x80`
+      /// number of stack elements the code section returns or 0x80 for non-returning functions
+      pub outputs: u8,
+      /// max_stack_height - 2 bytes - `0x0000-0x03FF`
+      /// maximum number of elements ever placed onto the stack by the code section
+      pub max_stack_size: u16,
+  }
+*)
+
+Module TypesSection.
+  Record t : Set := {
+    inputs : Z;
+    outputs : Z;
+    max_stack_size : Z;
+  }.
+
+  Global Instance IsToTy : ToTy t := {
+    Φ := Ty.path "revm_primitives::bytecode::eof::types_section::TypesSection";
+  }.
+
+  Global Instance IsToValue : ToValue t := {
+    φ x :=
+      Value.StructRecord "revm_primitives::bytecode::eof::types_section::TypesSection" [
+        ("inputs", φ x.(inputs));
+        ("outputs", φ x.(outputs));
+        ("max_stack_size", φ x.(max_stack_size))
+      ];
+  }.
+End TypesSection.
diff --git a/CoqOfRust/revm/links/primitives/env.v b/CoqOfRust/revm/links/primitives/env.v
new file mode 100644
index 000000000..0dd9cdd7e
--- /dev/null
+++ b/CoqOfRust/revm/links/primitives/env.v
@@ -0,0 +1,35 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+
+(*
+  /// Create scheme.
+  #[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)]
+  #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
+  pub enum CreateScheme {
+      /// Legacy create scheme of `CREATE`.
+      Create,
+      /// Create scheme of `CREATE2`.
+      Create2 {
+          /// Salt.
+          salt: U256,
+      },
+  }
+*)
+
+Module CreateScheme.
+  Inductive t : Set :=
+  | Create
+  | Create2 : Z -> t.
+
+  Global Instance IsToTy : ToTy t := {
+    Φ := Ty.path "revm_primitives::env::CreateScheme";
+  }.
+
+  Global Instance IsToValue : ToValue t := {
+    φ x :=
+      match x with
+      | Create => Value.StructTuple "revm_primitives::env::CreateScheme::Create" []
+      | Create2 x => Value.StructTuple "revm_primitives::env::CreateScheme::Create2" [φ x]
+      end;
+  }.
+End CreateScheme.
diff --git a/CoqOfRust/revm/simulations/interpreter/instructions/macros.v b/CoqOfRust/revm/simulations/interpreter/instructions/macros.v
new file mode 100644
index 000000000..17f456d3c
--- /dev/null
+++ b/CoqOfRust/revm/simulations/interpreter/instructions/macros.v
@@ -0,0 +1,39 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import CoqOfRust.simulations.M.
+Import simulations.M.Notations.
+Require Import CoqOfRust.revm.links.interpreter.interpreter.
+Require Import CoqOfRust.revm.links.interpreter.interpreter.gas.
+Require Import CoqOfRust.revm.links.interpreter.interpreter.instruction_result.
+Require Import CoqOfRust.revm.simulations.interpreter.interpreter.
+Require Import CoqOfRust.revm.simulations.interpreter.interpreter.gas.
+
+
+(*
+  /// Records a `gas` cost and fails the instruction if it would exceed the available gas.
+  #[macro_export]
+  macro_rules! gas {
+      ($interp:expr, $gas:expr) => {
+          $crate::gas!($interp, $gas, ())
+      };
+      ($interp:expr, $gas:expr, $ret:expr) => {
+          if !$interp.gas.record_cost($gas) {
+              $interp.instruction_result = $crate::InstructionResult::OutOfGas;
+              return $ret;
+          }
+      };
+  }
+*)
+
+Definition gas_macro (gas : Z) :
+    MS? Interpreter.t string unit :=
+  letS? interp := readS? in
+  letS? success := liftS? Interpreter.Lens.gas (Gas.record_cost gas) in
+  if negb success
+  then
+    letS? _ := writeS? (interp <|
+      Interpreter.instruction_result := InstructionResult.OutOfGas
+    |>) in
+    returnS? tt
+  else
+    returnS? tt.
diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter.v b/CoqOfRust/revm/simulations/interpreter/interpreter.v
new file mode 100644
index 000000000..51162db2a
--- /dev/null
+++ b/CoqOfRust/revm/simulations/interpreter/interpreter.v
@@ -0,0 +1,22 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import CoqOfRust.simulations.M.
+Import simulations.M.Notations.
+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.
+Require Import CoqOfRust.revm.links.interpreter.interpreter.
+
+Module Interpreter.
+  Module Lens.
+    Definition gas : Lens.t Interpreter.t Gas.t := {|
+      Lens.read interp := Interpreter.gas interp;
+      Lens.write interp gas := interp <| Interpreter.gas := gas |>
+    |}.
+  End Lens.
+End Interpreter.
diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter/gas.v b/CoqOfRust/revm/simulations/interpreter/interpreter/gas.v
new file mode 100644
index 000000000..ecc55e371
--- /dev/null
+++ b/CoqOfRust/revm/simulations/interpreter/interpreter/gas.v
@@ -0,0 +1,35 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import CoqOfRust.simulations.M.
+Import simulations.M.Notations.
+Require Import CoqOfRust.revm.links.interpreter.interpreter.gas.
+
+Module Gas.
+  (*
+    /// Records an explicit cost.
+    ///
+    /// Returns `false` if the gas limit is exceeded.
+    #[inline]
+    #[must_use = "prefer using `gas!` instead to return an out-of-gas error on failure"]
+    pub fn record_cost(&mut self, cost: u64) -> bool {
+        let (remaining, overflow) = self.remaining.overflowing_sub(cost);
+        let success = !overflow;
+        if success {
+            self.remaining = remaining;
+        }
+        success
+    }
+  *)
+  Definition record_cost
+      (cost : Z) :
+      MS? Gas.t string bool :=
+    letS? 'gas := readS? in
+    let remaining_sub_cost := gas.(Gas.remaining) - cost in
+    let success := remaining_sub_cost >=? 0 in
+    letS? _ :=
+      if success 
+      then writeS? (gas <| Gas.remaining := remaining_sub_cost |>)
+      else returnS? tt
+    in
+    returnS? success.
+End Gas.
diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter/stack.v b/CoqOfRust/revm/simulations/interpreter/interpreter/stack.v
new file mode 100644
index 000000000..2192044d4
--- /dev/null
+++ b/CoqOfRust/revm/simulations/interpreter/interpreter/stack.v
@@ -0,0 +1,118 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import CoqOfRust.simulations.M.
+Import simulations.M.Notations.
+Require Import CoqOfRust.core.links.array.
+Require Import CoqOfRust.revm.links.dependencies.
+Require Import CoqOfRust.revm.links.interpreter.interpreter.instruction_result.
+Require Import CoqOfRust.revm.links.interpreter.interpreter.stack.
+
+Module Stack.
+  (*
+    /// Returns the length of the stack in words.
+    #[inline]
+    pub fn len(&self) -> usize {
+        self.data.len()
+    }
+  *)
+  Definition len '(Stack.data stack) : Z :=
+    Z.of_nat (List.length stack).
+
+  (*
+    /// Removes the topmost element from the stack and returns it, or `StackUnderflow` if it is
+    /// empty.
+    #[inline]
+    pub fn pop(&mut self) -> Result<U256, InstructionResult> {
+        self.data.pop().ok_or(InstructionResult::StackUnderflow)
+    }
+  *)
+  Definition pop :
+      MS? Stack.t string (U256 + InstructionResult.t) :=
+    letS? '(Stack.data stack) := readS? in
+    match stack with
+    | [] => returnS? (inr InstructionResult.StackUnderflow)
+    | x :: xs => 
+      letS? _ := writeS? (Stack.data xs) in
+      returnS? (inl x)
+    end.
+
+  (*
+    /// Removes the topmost element from the stack and returns it.
+    ///
+    /// # Safety
+    ///
+    /// The caller is responsible for checking the length of the stack.
+    #[inline]
+    pub unsafe fn pop_unsafe(&mut self) -> U256 {
+        self.data.pop().unwrap_unchecked()
+    }
+  *)
+  Definition pop_unsafe :
+      MS? Stack.t string U256 :=
+    letS? result := pop in
+    match result with
+    | inl x => returnS? x
+    | inr _ => panicS? "Stack underflow"
+    end.
+
+  (*
+      /// Peeks the top of the stack.
+      ///
+      /// # Safety
+      ///
+      /// The caller is responsible for checking the length of the stack.
+      #[inline]
+      pub unsafe fn top_unsafe(&mut self) -> &mut U256 {
+          let len = self.data.len();
+          self.data.get_unchecked_mut(len - 1)
+      }
+  *)
+  Definition top_unsafe :
+      MS? Stack.t string U256 :=
+    letS? '(Stack.data stack) := readS? in
+    match stack with
+    | [] => panicS? "Stack underflow"
+    | x :: _ => returnS? x
+    end.
+
+  (*
+      /// Pop the topmost value, returning the value and the new topmost value.
+      ///
+      /// # Safety
+      ///
+      /// The caller is responsible for checking the length of the stack.
+      #[inline]
+      pub unsafe fn pop_top_unsafe(&mut self) -> (U256, &mut U256) {
+          let pop = self.pop_unsafe();
+          let top = self.top_unsafe();
+          (pop, top)
+      }
+  *)
+  Definition pop_top_unsafe :
+      MS? Stack.t string (U256 * U256) :=
+    letS? pop := pop_unsafe in
+    letS? top := top_unsafe in
+    returnS? (pop, top).
+  
+  (*
+    /// Pops 2 values from the stack and returns them, in addition to the new topmost value.
+    ///
+    /// # Safety
+    ///
+    /// The caller is responsible for checking the length of the stack.
+    #[inline]
+    pub unsafe fn pop2_top_unsafe(&mut self) -> (U256, U256, &mut U256) {
+        let pop1 = self.pop_unsafe();
+        let pop2 = self.pop_unsafe();
+        let top = self.top_unsafe();
+
+        (pop1, pop2, top)
+    }
+  *)
+  Definition pop2_top_unsafe :
+      MS? Stack.t string (U256 * U256 * U256) :=
+    letS? pop1 := pop_unsafe in
+    letS? pop2 := pop_unsafe in
+    letS? top := top_unsafe in
+    returnS? (pop1, pop2, top).
+End Stack.
diff --git a/CoqOfRust/revm/interpreter/function_stack.v b/CoqOfRust/revm/translations/interpreter/function_stack.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/function_stack.v
rename to CoqOfRust/revm/translations/interpreter/function_stack.v
diff --git a/CoqOfRust/revm/interpreter/gas.v b/CoqOfRust/revm/translations/interpreter/gas.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/gas.v
rename to CoqOfRust/revm/translations/interpreter/gas.v
diff --git a/CoqOfRust/revm/interpreter/gas/calc.v b/CoqOfRust/revm/translations/interpreter/gas/calc.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/gas/calc.v
rename to CoqOfRust/revm/translations/interpreter/gas/calc.v
diff --git a/CoqOfRust/revm/interpreter/gas/constants.v b/CoqOfRust/revm/translations/interpreter/gas/constants.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/gas/constants.v
rename to CoqOfRust/revm/translations/interpreter/gas/constants.v
diff --git a/CoqOfRust/revm/interpreter/host.v b/CoqOfRust/revm/translations/interpreter/host.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/host.v
rename to CoqOfRust/revm/translations/interpreter/host.v
diff --git a/CoqOfRust/revm/interpreter/host/dummy.v b/CoqOfRust/revm/translations/interpreter/host/dummy.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/host/dummy.v
rename to CoqOfRust/revm/translations/interpreter/host/dummy.v
diff --git a/CoqOfRust/revm/interpreter/instruction_result.v b/CoqOfRust/revm/translations/interpreter/instruction_result.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/instruction_result.v
rename to CoqOfRust/revm/translations/interpreter/instruction_result.v
diff --git a/CoqOfRust/revm/interpreter/instructions/arithmetic.v b/CoqOfRust/revm/translations/interpreter/instructions/arithmetic.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/instructions/arithmetic.v
rename to CoqOfRust/revm/translations/interpreter/instructions/arithmetic.v
diff --git a/CoqOfRust/revm/interpreter/instructions/bitwise.v b/CoqOfRust/revm/translations/interpreter/instructions/bitwise.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/instructions/bitwise.v
rename to CoqOfRust/revm/translations/interpreter/instructions/bitwise.v
diff --git a/CoqOfRust/revm/interpreter/instructions/contract.v b/CoqOfRust/revm/translations/interpreter/instructions/contract.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/instructions/contract.v
rename to CoqOfRust/revm/translations/interpreter/instructions/contract.v
diff --git a/CoqOfRust/revm/interpreter/instructions/contract/call_helpers.v b/CoqOfRust/revm/translations/interpreter/instructions/contract/call_helpers.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/instructions/contract/call_helpers.v
rename to CoqOfRust/revm/translations/interpreter/instructions/contract/call_helpers.v
diff --git a/CoqOfRust/revm/interpreter/instructions/control.v b/CoqOfRust/revm/translations/interpreter/instructions/control.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/instructions/control.v
rename to CoqOfRust/revm/translations/interpreter/instructions/control.v
diff --git a/CoqOfRust/revm/interpreter/instructions/data.v b/CoqOfRust/revm/translations/interpreter/instructions/data.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/instructions/data.v
rename to CoqOfRust/revm/translations/interpreter/instructions/data.v
diff --git a/CoqOfRust/revm/interpreter/instructions/host.v b/CoqOfRust/revm/translations/interpreter/instructions/host.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/instructions/host.v
rename to CoqOfRust/revm/translations/interpreter/instructions/host.v
diff --git a/CoqOfRust/revm/interpreter/instructions/host_env.v b/CoqOfRust/revm/translations/interpreter/instructions/host_env.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/instructions/host_env.v
rename to CoqOfRust/revm/translations/interpreter/instructions/host_env.v
diff --git a/CoqOfRust/revm/interpreter/instructions/i256.v b/CoqOfRust/revm/translations/interpreter/instructions/i256.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/instructions/i256.v
rename to CoqOfRust/revm/translations/interpreter/instructions/i256.v
diff --git a/CoqOfRust/revm/interpreter/instructions/memory.v b/CoqOfRust/revm/translations/interpreter/instructions/memory.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/instructions/memory.v
rename to CoqOfRust/revm/translations/interpreter/instructions/memory.v
diff --git a/CoqOfRust/revm/interpreter/instructions/stack.v b/CoqOfRust/revm/translations/interpreter/instructions/stack.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/instructions/stack.v
rename to CoqOfRust/revm/translations/interpreter/instructions/stack.v
diff --git a/CoqOfRust/revm/interpreter/instructions/system.v b/CoqOfRust/revm/translations/interpreter/instructions/system.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/instructions/system.v
rename to CoqOfRust/revm/translations/interpreter/instructions/system.v
diff --git a/CoqOfRust/revm/interpreter/instructions/utility.v b/CoqOfRust/revm/translations/interpreter/instructions/utility.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/instructions/utility.v
rename to CoqOfRust/revm/translations/interpreter/instructions/utility.v
diff --git a/CoqOfRust/revm/interpreter/interpreter.v b/CoqOfRust/revm/translations/interpreter/interpreter.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/interpreter.v
rename to CoqOfRust/revm/translations/interpreter/interpreter.v
diff --git a/CoqOfRust/revm/interpreter/interpreter/analysis.v b/CoqOfRust/revm/translations/interpreter/interpreter/analysis.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/interpreter/analysis.v
rename to CoqOfRust/revm/translations/interpreter/interpreter/analysis.v
diff --git a/CoqOfRust/revm/interpreter/interpreter/contract.v b/CoqOfRust/revm/translations/interpreter/interpreter/contract.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/interpreter/contract.v
rename to CoqOfRust/revm/translations/interpreter/interpreter/contract.v
diff --git a/CoqOfRust/revm/interpreter/interpreter/shared_memory.v b/CoqOfRust/revm/translations/interpreter/interpreter/shared_memory.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/interpreter/shared_memory.v
rename to CoqOfRust/revm/translations/interpreter/interpreter/shared_memory.v
diff --git a/CoqOfRust/revm/interpreter/interpreter/stack.v b/CoqOfRust/revm/translations/interpreter/interpreter/stack.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/interpreter/stack.v
rename to CoqOfRust/revm/translations/interpreter/interpreter/stack.v
diff --git a/CoqOfRust/revm/interpreter/interpreter_action.v b/CoqOfRust/revm/translations/interpreter/interpreter_action.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/interpreter_action.v
rename to CoqOfRust/revm/translations/interpreter/interpreter_action.v
diff --git a/CoqOfRust/revm/interpreter/interpreter_action/call_inputs.v b/CoqOfRust/revm/translations/interpreter/interpreter_action/call_inputs.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/interpreter_action/call_inputs.v
rename to CoqOfRust/revm/translations/interpreter/interpreter_action/call_inputs.v
diff --git a/CoqOfRust/revm/interpreter/interpreter_action/call_outcome.v b/CoqOfRust/revm/translations/interpreter/interpreter_action/call_outcome.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/interpreter_action/call_outcome.v
rename to CoqOfRust/revm/translations/interpreter/interpreter_action/call_outcome.v
diff --git a/CoqOfRust/revm/interpreter/interpreter_action/create_inputs.v b/CoqOfRust/revm/translations/interpreter/interpreter_action/create_inputs.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/interpreter_action/create_inputs.v
rename to CoqOfRust/revm/translations/interpreter/interpreter_action/create_inputs.v
diff --git a/CoqOfRust/revm/interpreter/interpreter_action/create_outcome.v b/CoqOfRust/revm/translations/interpreter/interpreter_action/create_outcome.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/interpreter_action/create_outcome.v
rename to CoqOfRust/revm/translations/interpreter/interpreter_action/create_outcome.v
diff --git a/CoqOfRust/revm/interpreter/interpreter_action/eof_create_inputs.v b/CoqOfRust/revm/translations/interpreter/interpreter_action/eof_create_inputs.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/interpreter_action/eof_create_inputs.v
rename to CoqOfRust/revm/translations/interpreter/interpreter_action/eof_create_inputs.v
diff --git a/CoqOfRust/revm/interpreter/interpreter_action/eof_create_outcome.v b/CoqOfRust/revm/translations/interpreter/interpreter_action/eof_create_outcome.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/interpreter_action/eof_create_outcome.v
rename to CoqOfRust/revm/translations/interpreter/interpreter_action/eof_create_outcome.v
diff --git a/CoqOfRust/revm/interpreter/opcode.v b/CoqOfRust/revm/translations/interpreter/opcode.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/opcode.v
rename to CoqOfRust/revm/translations/interpreter/opcode.v
diff --git a/CoqOfRust/revm/interpreter/opcode/eof_printer.v b/CoqOfRust/revm/translations/interpreter/opcode/eof_printer.v
similarity index 100%
rename from CoqOfRust/revm/interpreter/opcode/eof_printer.v
rename to CoqOfRust/revm/translations/interpreter/opcode/eof_printer.v
diff --git a/CoqOfRust/revm/precompile/blake2.v b/CoqOfRust/revm/translations/precompile/blake2.v
similarity index 100%
rename from CoqOfRust/revm/precompile/blake2.v
rename to CoqOfRust/revm/translations/precompile/blake2.v
diff --git a/CoqOfRust/revm/precompile/bn128.v b/CoqOfRust/revm/translations/precompile/bn128.v
similarity index 100%
rename from CoqOfRust/revm/precompile/bn128.v
rename to CoqOfRust/revm/translations/precompile/bn128.v
diff --git a/CoqOfRust/revm/precompile/hash.v b/CoqOfRust/revm/translations/precompile/hash.v
similarity index 100%
rename from CoqOfRust/revm/precompile/hash.v
rename to CoqOfRust/revm/translations/precompile/hash.v
diff --git a/CoqOfRust/revm/precompile/identity.v b/CoqOfRust/revm/translations/precompile/identity.v
similarity index 100%
rename from CoqOfRust/revm/precompile/identity.v
rename to CoqOfRust/revm/translations/precompile/identity.v
diff --git a/CoqOfRust/revm/precompile/kzg_point_evaluation.v b/CoqOfRust/revm/translations/precompile/kzg_point_evaluation.v
similarity index 100%
rename from CoqOfRust/revm/precompile/kzg_point_evaluation.v
rename to CoqOfRust/revm/translations/precompile/kzg_point_evaluation.v
diff --git a/CoqOfRust/revm/precompile/lib.v b/CoqOfRust/revm/translations/precompile/lib.v
similarity index 100%
rename from CoqOfRust/revm/precompile/lib.v
rename to CoqOfRust/revm/translations/precompile/lib.v
diff --git a/CoqOfRust/revm/precompile/modexp.v b/CoqOfRust/revm/translations/precompile/modexp.v
similarity index 100%
rename from CoqOfRust/revm/precompile/modexp.v
rename to CoqOfRust/revm/translations/precompile/modexp.v
diff --git a/CoqOfRust/revm/precompile/secp256k1.v b/CoqOfRust/revm/translations/precompile/secp256k1.v
similarity index 100%
rename from CoqOfRust/revm/precompile/secp256k1.v
rename to CoqOfRust/revm/translations/precompile/secp256k1.v
diff --git a/CoqOfRust/revm/precompile/utilities.v b/CoqOfRust/revm/translations/precompile/utilities.v
similarity index 100%
rename from CoqOfRust/revm/precompile/utilities.v
rename to CoqOfRust/revm/translations/precompile/utilities.v
diff --git a/CoqOfRust/revm/primitives/bytecode.v b/CoqOfRust/revm/translations/primitives/bytecode.v
similarity index 100%
rename from CoqOfRust/revm/primitives/bytecode.v
rename to CoqOfRust/revm/translations/primitives/bytecode.v
diff --git a/CoqOfRust/revm/primitives/bytecode/eof.v b/CoqOfRust/revm/translations/primitives/bytecode/eof.v
similarity index 100%
rename from CoqOfRust/revm/primitives/bytecode/eof.v
rename to CoqOfRust/revm/translations/primitives/bytecode/eof.v
diff --git a/CoqOfRust/revm/primitives/bytecode/eof/body.v b/CoqOfRust/revm/translations/primitives/bytecode/eof/body.v
similarity index 100%
rename from CoqOfRust/revm/primitives/bytecode/eof/body.v
rename to CoqOfRust/revm/translations/primitives/bytecode/eof/body.v
diff --git a/CoqOfRust/revm/primitives/bytecode/eof/decode_helpers.v b/CoqOfRust/revm/translations/primitives/bytecode/eof/decode_helpers.v
similarity index 100%
rename from CoqOfRust/revm/primitives/bytecode/eof/decode_helpers.v
rename to CoqOfRust/revm/translations/primitives/bytecode/eof/decode_helpers.v
diff --git a/CoqOfRust/revm/primitives/bytecode/eof/header.v b/CoqOfRust/revm/translations/primitives/bytecode/eof/header.v
similarity index 100%
rename from CoqOfRust/revm/primitives/bytecode/eof/header.v
rename to CoqOfRust/revm/translations/primitives/bytecode/eof/header.v
diff --git a/CoqOfRust/revm/primitives/bytecode/eof/types_section.v b/CoqOfRust/revm/translations/primitives/bytecode/eof/types_section.v
similarity index 100%
rename from CoqOfRust/revm/primitives/bytecode/eof/types_section.v
rename to CoqOfRust/revm/translations/primitives/bytecode/eof/types_section.v
diff --git a/CoqOfRust/revm/primitives/bytecode/legacy.v b/CoqOfRust/revm/translations/primitives/bytecode/legacy.v
similarity index 100%
rename from CoqOfRust/revm/primitives/bytecode/legacy.v
rename to CoqOfRust/revm/translations/primitives/bytecode/legacy.v
diff --git a/CoqOfRust/revm/primitives/bytecode/legacy/jump_map.v b/CoqOfRust/revm/translations/primitives/bytecode/legacy/jump_map.v
similarity index 100%
rename from CoqOfRust/revm/primitives/bytecode/legacy/jump_map.v
rename to CoqOfRust/revm/translations/primitives/bytecode/legacy/jump_map.v
diff --git a/CoqOfRust/revm/primitives/constants.v b/CoqOfRust/revm/translations/primitives/constants.v
similarity index 100%
rename from CoqOfRust/revm/primitives/constants.v
rename to CoqOfRust/revm/translations/primitives/constants.v
diff --git a/CoqOfRust/revm/primitives/db.v b/CoqOfRust/revm/translations/primitives/db.v
similarity index 100%
rename from CoqOfRust/revm/primitives/db.v
rename to CoqOfRust/revm/translations/primitives/db.v
diff --git a/CoqOfRust/revm/primitives/db/components.v b/CoqOfRust/revm/translations/primitives/db/components.v
similarity index 100%
rename from CoqOfRust/revm/primitives/db/components.v
rename to CoqOfRust/revm/translations/primitives/db/components.v
diff --git a/CoqOfRust/revm/primitives/db/components/block_hash.v b/CoqOfRust/revm/translations/primitives/db/components/block_hash.v
similarity index 100%
rename from CoqOfRust/revm/primitives/db/components/block_hash.v
rename to CoqOfRust/revm/translations/primitives/db/components/block_hash.v
diff --git a/CoqOfRust/revm/primitives/db/components/state.v b/CoqOfRust/revm/translations/primitives/db/components/state.v
similarity index 100%
rename from CoqOfRust/revm/primitives/db/components/state.v
rename to CoqOfRust/revm/translations/primitives/db/components/state.v
diff --git a/CoqOfRust/revm/primitives/env.v b/CoqOfRust/revm/translations/primitives/env.v
similarity index 100%
rename from CoqOfRust/revm/primitives/env.v
rename to CoqOfRust/revm/translations/primitives/env.v
diff --git a/CoqOfRust/revm/primitives/env/handler_cfg.v b/CoqOfRust/revm/translations/primitives/env/handler_cfg.v
similarity index 100%
rename from CoqOfRust/revm/primitives/env/handler_cfg.v
rename to CoqOfRust/revm/translations/primitives/env/handler_cfg.v
diff --git a/CoqOfRust/revm/primitives/kzg/env_settings.v b/CoqOfRust/revm/translations/primitives/kzg/env_settings.v
similarity index 100%
rename from CoqOfRust/revm/primitives/kzg/env_settings.v
rename to CoqOfRust/revm/translations/primitives/kzg/env_settings.v
diff --git a/CoqOfRust/revm/primitives/kzg/trusted_setup_points.v b/CoqOfRust/revm/translations/primitives/kzg/trusted_setup_points.v
similarity index 100%
rename from CoqOfRust/revm/primitives/kzg/trusted_setup_points.v
rename to CoqOfRust/revm/translations/primitives/kzg/trusted_setup_points.v
diff --git a/CoqOfRust/revm/primitives/precompile.v b/CoqOfRust/revm/translations/primitives/precompile.v
similarity index 100%
rename from CoqOfRust/revm/primitives/precompile.v
rename to CoqOfRust/revm/translations/primitives/precompile.v
diff --git a/CoqOfRust/revm/primitives/result.v b/CoqOfRust/revm/translations/primitives/result.v
similarity index 100%
rename from CoqOfRust/revm/primitives/result.v
rename to CoqOfRust/revm/translations/primitives/result.v
diff --git a/CoqOfRust/revm/primitives/specification.v b/CoqOfRust/revm/translations/primitives/specification.v
similarity index 100%
rename from CoqOfRust/revm/primitives/specification.v
rename to CoqOfRust/revm/translations/primitives/specification.v
diff --git a/CoqOfRust/revm/primitives/state.v b/CoqOfRust/revm/translations/primitives/state.v
similarity index 100%
rename from CoqOfRust/revm/primitives/state.v
rename to CoqOfRust/revm/translations/primitives/state.v
diff --git a/CoqOfRust/revm/primitives/utilities.v b/CoqOfRust/revm/translations/primitives/utilities.v
similarity index 100%
rename from CoqOfRust/revm/primitives/utilities.v
rename to CoqOfRust/revm/translations/primitives/utilities.v
diff --git a/CoqOfRust/revm/revm/builder.v b/CoqOfRust/revm/translations/revm/builder.v
similarity index 100%
rename from CoqOfRust/revm/revm/builder.v
rename to CoqOfRust/revm/translations/revm/builder.v
diff --git a/CoqOfRust/revm/revm/context.v b/CoqOfRust/revm/translations/revm/context.v
similarity index 100%
rename from CoqOfRust/revm/revm/context.v
rename to CoqOfRust/revm/translations/revm/context.v
diff --git a/CoqOfRust/revm/revm/context/context_precompiles.v b/CoqOfRust/revm/translations/revm/context/context_precompiles.v
similarity index 100%
rename from CoqOfRust/revm/revm/context/context_precompiles.v
rename to CoqOfRust/revm/translations/revm/context/context_precompiles.v
diff --git a/CoqOfRust/revm/revm/context/evm_context.v b/CoqOfRust/revm/translations/revm/context/evm_context.v
similarity index 100%
rename from CoqOfRust/revm/revm/context/evm_context.v
rename to CoqOfRust/revm/translations/revm/context/evm_context.v
diff --git a/CoqOfRust/revm/revm/context/inner_evm_context.v b/CoqOfRust/revm/translations/revm/context/inner_evm_context.v
similarity index 100%
rename from CoqOfRust/revm/revm/context/inner_evm_context.v
rename to CoqOfRust/revm/translations/revm/context/inner_evm_context.v
diff --git a/CoqOfRust/revm/revm/db/emptydb.v b/CoqOfRust/revm/translations/revm/db/emptydb.v
similarity index 100%
rename from CoqOfRust/revm/revm/db/emptydb.v
rename to CoqOfRust/revm/translations/revm/db/emptydb.v
diff --git a/CoqOfRust/revm/revm/db/in_memory_db.v b/CoqOfRust/revm/translations/revm/db/in_memory_db.v
similarity index 100%
rename from CoqOfRust/revm/revm/db/in_memory_db.v
rename to CoqOfRust/revm/translations/revm/db/in_memory_db.v
diff --git a/CoqOfRust/revm/revm/db/states/account_status.v b/CoqOfRust/revm/translations/revm/db/states/account_status.v
similarity index 100%
rename from CoqOfRust/revm/revm/db/states/account_status.v
rename to CoqOfRust/revm/translations/revm/db/states/account_status.v
diff --git a/CoqOfRust/revm/revm/db/states/bundle_account.v b/CoqOfRust/revm/translations/revm/db/states/bundle_account.v
similarity index 100%
rename from CoqOfRust/revm/revm/db/states/bundle_account.v
rename to CoqOfRust/revm/translations/revm/db/states/bundle_account.v
diff --git a/CoqOfRust/revm/revm/db/states/bundle_state.v b/CoqOfRust/revm/translations/revm/db/states/bundle_state.v
similarity index 100%
rename from CoqOfRust/revm/revm/db/states/bundle_state.v
rename to CoqOfRust/revm/translations/revm/db/states/bundle_state.v
diff --git a/CoqOfRust/revm/revm/db/states/cache.v b/CoqOfRust/revm/translations/revm/db/states/cache.v
similarity index 100%
rename from CoqOfRust/revm/revm/db/states/cache.v
rename to CoqOfRust/revm/translations/revm/db/states/cache.v
diff --git a/CoqOfRust/revm/revm/db/states/cache_account.v b/CoqOfRust/revm/translations/revm/db/states/cache_account.v
similarity index 100%
rename from CoqOfRust/revm/revm/db/states/cache_account.v
rename to CoqOfRust/revm/translations/revm/db/states/cache_account.v
diff --git a/CoqOfRust/revm/revm/db/states/changes.v b/CoqOfRust/revm/translations/revm/db/states/changes.v
similarity index 100%
rename from CoqOfRust/revm/revm/db/states/changes.v
rename to CoqOfRust/revm/translations/revm/db/states/changes.v
diff --git a/CoqOfRust/revm/revm/db/states/plain_account.v b/CoqOfRust/revm/translations/revm/db/states/plain_account.v
similarity index 100%
rename from CoqOfRust/revm/revm/db/states/plain_account.v
rename to CoqOfRust/revm/translations/revm/db/states/plain_account.v
diff --git a/CoqOfRust/revm/revm/db/states/reverts.v b/CoqOfRust/revm/translations/revm/db/states/reverts.v
similarity index 100%
rename from CoqOfRust/revm/revm/db/states/reverts.v
rename to CoqOfRust/revm/translations/revm/db/states/reverts.v
diff --git a/CoqOfRust/revm/revm/db/states/state.v b/CoqOfRust/revm/translations/revm/db/states/state.v
similarity index 100%
rename from CoqOfRust/revm/revm/db/states/state.v
rename to CoqOfRust/revm/translations/revm/db/states/state.v
diff --git a/CoqOfRust/revm/revm/db/states/state_builder.v b/CoqOfRust/revm/translations/revm/db/states/state_builder.v
similarity index 100%
rename from CoqOfRust/revm/revm/db/states/state_builder.v
rename to CoqOfRust/revm/translations/revm/db/states/state_builder.v
diff --git a/CoqOfRust/revm/revm/db/states/transition_account.v b/CoqOfRust/revm/translations/revm/db/states/transition_account.v
similarity index 100%
rename from CoqOfRust/revm/revm/db/states/transition_account.v
rename to CoqOfRust/revm/translations/revm/db/states/transition_account.v
diff --git a/CoqOfRust/revm/revm/db/states/transition_state.v b/CoqOfRust/revm/translations/revm/db/states/transition_state.v
similarity index 100%
rename from CoqOfRust/revm/revm/db/states/transition_state.v
rename to CoqOfRust/revm/translations/revm/db/states/transition_state.v
diff --git a/CoqOfRust/revm/revm/evm.v b/CoqOfRust/revm/translations/revm/evm.v
similarity index 100%
rename from CoqOfRust/revm/revm/evm.v
rename to CoqOfRust/revm/translations/revm/evm.v
diff --git a/CoqOfRust/revm/revm/frame.v b/CoqOfRust/revm/translations/revm/frame.v
similarity index 100%
rename from CoqOfRust/revm/revm/frame.v
rename to CoqOfRust/revm/translations/revm/frame.v
diff --git a/CoqOfRust/revm/revm/handler.v b/CoqOfRust/revm/translations/revm/handler.v
similarity index 100%
rename from CoqOfRust/revm/revm/handler.v
rename to CoqOfRust/revm/translations/revm/handler.v
diff --git a/CoqOfRust/revm/revm/handler/handle_types/execution.v b/CoqOfRust/revm/translations/revm/handler/handle_types/execution.v
similarity index 100%
rename from CoqOfRust/revm/revm/handler/handle_types/execution.v
rename to CoqOfRust/revm/translations/revm/handler/handle_types/execution.v
diff --git a/CoqOfRust/revm/revm/handler/handle_types/post_execution.v b/CoqOfRust/revm/translations/revm/handler/handle_types/post_execution.v
similarity index 100%
rename from CoqOfRust/revm/revm/handler/handle_types/post_execution.v
rename to CoqOfRust/revm/translations/revm/handler/handle_types/post_execution.v
diff --git a/CoqOfRust/revm/revm/handler/handle_types/pre_execution.v b/CoqOfRust/revm/translations/revm/handler/handle_types/pre_execution.v
similarity index 100%
rename from CoqOfRust/revm/revm/handler/handle_types/pre_execution.v
rename to CoqOfRust/revm/translations/revm/handler/handle_types/pre_execution.v
diff --git a/CoqOfRust/revm/revm/handler/handle_types/validation.v b/CoqOfRust/revm/translations/revm/handler/handle_types/validation.v
similarity index 100%
rename from CoqOfRust/revm/revm/handler/handle_types/validation.v
rename to CoqOfRust/revm/translations/revm/handler/handle_types/validation.v
diff --git a/CoqOfRust/revm/revm/handler/mainnet/execution.v b/CoqOfRust/revm/translations/revm/handler/mainnet/execution.v
similarity index 100%
rename from CoqOfRust/revm/revm/handler/mainnet/execution.v
rename to CoqOfRust/revm/translations/revm/handler/mainnet/execution.v
diff --git a/CoqOfRust/revm/revm/handler/mainnet/post_execution.v b/CoqOfRust/revm/translations/revm/handler/mainnet/post_execution.v
similarity index 100%
rename from CoqOfRust/revm/revm/handler/mainnet/post_execution.v
rename to CoqOfRust/revm/translations/revm/handler/mainnet/post_execution.v
diff --git a/CoqOfRust/revm/revm/handler/mainnet/pre_execution.v b/CoqOfRust/revm/translations/revm/handler/mainnet/pre_execution.v
similarity index 100%
rename from CoqOfRust/revm/revm/handler/mainnet/pre_execution.v
rename to CoqOfRust/revm/translations/revm/handler/mainnet/pre_execution.v
diff --git a/CoqOfRust/revm/revm/handler/mainnet/validation.v b/CoqOfRust/revm/translations/revm/handler/mainnet/validation.v
similarity index 100%
rename from CoqOfRust/revm/revm/handler/mainnet/validation.v
rename to CoqOfRust/revm/translations/revm/handler/mainnet/validation.v
diff --git a/CoqOfRust/revm/revm/handler/register.v b/CoqOfRust/revm/translations/revm/handler/register.v
similarity index 100%
rename from CoqOfRust/revm/revm/handler/register.v
rename to CoqOfRust/revm/translations/revm/handler/register.v
diff --git a/CoqOfRust/revm/revm/inspector.v b/CoqOfRust/revm/translations/revm/inspector.v
similarity index 100%
rename from CoqOfRust/revm/revm/inspector.v
rename to CoqOfRust/revm/translations/revm/inspector.v
diff --git a/CoqOfRust/revm/revm/inspector/customprinter.v b/CoqOfRust/revm/translations/revm/inspector/customprinter.v
similarity index 100%
rename from CoqOfRust/revm/revm/inspector/customprinter.v
rename to CoqOfRust/revm/translations/revm/inspector/customprinter.v
diff --git a/CoqOfRust/revm/revm/inspector/gas.v b/CoqOfRust/revm/translations/revm/inspector/gas.v
similarity index 100%
rename from CoqOfRust/revm/revm/inspector/gas.v
rename to CoqOfRust/revm/translations/revm/inspector/gas.v
diff --git a/CoqOfRust/revm/revm/inspector/handler_register.v b/CoqOfRust/revm/translations/revm/inspector/handler_register.v
similarity index 100%
rename from CoqOfRust/revm/revm/inspector/handler_register.v
rename to CoqOfRust/revm/translations/revm/inspector/handler_register.v
diff --git a/CoqOfRust/revm/revm/inspector/noop.v b/CoqOfRust/revm/translations/revm/inspector/noop.v
similarity index 100%
rename from CoqOfRust/revm/revm/inspector/noop.v
rename to CoqOfRust/revm/translations/revm/inspector/noop.v
diff --git a/CoqOfRust/revm/revm/journaled_state.v b/CoqOfRust/revm/translations/revm/journaled_state.v
similarity index 100%
rename from CoqOfRust/revm/revm/journaled_state.v
rename to CoqOfRust/revm/translations/revm/journaled_state.v
diff --git a/CoqOfRust/simulations/M.v b/CoqOfRust/simulations/M.v
index 70ff3f857..139af6cf1 100644
--- a/CoqOfRust/simulations/M.v
+++ b/CoqOfRust/simulations/M.v
@@ -1,5 +1,13 @@
 Require Import CoqOfRust.CoqOfRust.
 
+Module Lens.
+  Record t {Big_A A : Set} : Set := {
+    read : Big_A -> A;
+    write : Big_A -> A -> Big_A
+  }.
+  Arguments t : clear implicits.
+End Lens.
+
 (** ** Monads that are useful for the definition of simulations. *)
 
 Module Error.
@@ -41,6 +49,14 @@ Module StateError.
   Definition lift_from_error {State Error A : Set} (value : Error.t Error A) : t State Error A :=
     fun state =>
     (value, state).
+
+  Definition lift_lens {Big_State State Error A : Set}
+      (lens : Lens.t Big_State State)
+      (value : t State Error A) :
+      t Big_State Error A :=
+    fun big_state =>
+      let (value, state) := value (lens.(Lens.read) big_state) in
+      (value, lens.(Lens.write) big_state state).
 End StateError.
 
 Module Notations.
@@ -75,4 +91,6 @@ Module Notations.
   Notation "panicS?" := StateError.panic.
 
   Notation "return?toS?" := StateError.lift_from_error.
+
+  Notation "liftS?" := StateError.lift_lens.
 End Notations.