diff --git a/CoqOfPython/ethereum/paris/vm/instructions/simulations/arithmetic.v b/CoqOfPython/ethereum/paris/vm/instructions/simulations/arithmetic.v
index ad6e132..609994f 100644
--- a/CoqOfPython/ethereum/paris/vm/instructions/simulations/arithmetic.v
+++ b/CoqOfPython/ethereum/paris/vm/instructions/simulations/arithmetic.v
@@ -31,7 +31,7 @@ Definition add : MS? Evm.t Exception.t unit :=
   letS? y := StateError.lift_lens Evm.Lens.stack pop in
 
   (* GAS *)
-  letS? _ := charge_gas GAS_VERY_LOW in
+  (* letS? _ := charge_gas GAS_VERY_LOW in *)
 
   (* OPERATION *)
   let result := U256.wrapping_add x y in
@@ -43,3 +43,40 @@ Definition add : MS? Evm.t Exception.t unit :=
     (inl tt, Uint.__add__ pc (Uint.Make 1))) in
 
   returnS? tt.
+
+Axiom environment : __init__.Environment.t.
+Axiom message : __init__.Message.t Evm.t.
+
+Definition empty_evm : Evm.t :=
+  Evm.Make message {|
+    Evm.Rest.pc := Uint.Make 0;
+    Evm.Rest.stack := [];
+    Evm.Rest.memory := [];
+    Evm.Rest.code := __init__.Bytes.Make [];
+    Evm.Rest.gas_left := Uint.Make 0;
+    Evm.Rest.env := environment;
+    Evm.Rest.valid_jump_destinations := [];
+    Evm.Rest.logs := [];
+    Evm.Rest.refund_counter := 0;
+    Evm.Rest.running := true;
+    Evm.Rest.output := __init__.Bytes.Make [];
+    Evm.Rest.accounts_to_delete := [];
+    Evm.Rest.touched_accounts := [];
+    Evm.Rest.return_data := __init__.Bytes.Make [];
+    Evm.Rest.error := None;
+    Evm.Rest.accessed_addresses := [];
+    Evm.Rest.accessed_storage_keys := [];
+  |}.
+
+Definition evm_with_gas : Evm.t :=
+  Evm.Lens.gas_left.(Lens.write) empty_evm GAS_VERY_LOW.
+
+Definition evm_with_stack : Evm.t :=
+  Evm.Lens.stack.(Lens.write) evm_with_gas [
+    U256.of_Z 12;
+    U256.of_Z 23
+  ].
+
+(* The term does not fully evaluate as the `charge_gas` function is still an axiom, so we have to
+   comment its call in the code above. *)
+Compute (add evm_with_stack).
diff --git a/CoqOfPython/ethereum/paris/vm/simulations/__init__.v b/CoqOfPython/ethereum/paris/vm/simulations/__init__.v
index 5fb9a63..16baafb 100644
--- a/CoqOfPython/ethereum/paris/vm/simulations/__init__.v
+++ b/CoqOfPython/ethereum/paris/vm/simulations/__init__.v
@@ -105,5 +105,15 @@ Module Evm.
       Lens.read '(Make _ rest) := rest.(Rest.memory);
       Lens.write '(Make message rest) memory := Make message rest<|Rest.memory := memory|>;
     |}.
+
+    Definition code : Lens.t t Bytes.t := {|
+      Lens.read '(Make _ rest) := rest.(Rest.code);
+      Lens.write '(Make message rest) code := Make message rest<|Rest.code := code|>;
+    |}.
+
+    Definition gas_left : Lens.t t Uint.t := {|
+      Lens.read '(Make _ rest) := rest.(Rest.gas_left);
+      Lens.write '(Make message rest) gas_left := Make message rest<|Rest.gas_left := gas_left|>;
+    |}.
   End Lens.
 End Evm.