diff --git a/CoqOfPython/CoqOfPython.v b/CoqOfPython/CoqOfPython.v
index af03df8..f63fd2d 100644
--- a/CoqOfPython/CoqOfPython.v
+++ b/CoqOfPython/CoqOfPython.v
@@ -146,6 +146,12 @@ Module Object.
       internal := Some data;
       fields := [];
     |}.
+
+  Definition empty {Value : Set} : t Value :=
+    {|
+      internal := None;
+      fields := [];
+    |}.
 End Object.
 
 Module Pointer.
@@ -187,10 +193,7 @@ End Locals.
 (** ** Constants *)
 Module Constant.
   Definition None_ : Value.t :=
-    Value.Make "builtins" "NoneType" (Pointer.Imm {|
-      Object.internal := None;
-      Object.fields := [];
-    |}).
+    Value.Make "builtins" "NoneType" (Pointer.Imm Object.empty).
 
   Definition ellipsis : Value.t :=
     Value.Make "builtins" "ellipsis" (Pointer.Imm (Object.wrapper Data.Ellipsis)).
@@ -411,7 +414,8 @@ Module M.
 
   Parameter delete : Value.t -> M.
 
-  Parameter return_ : Value.t -> M.
+  Definition return_ (value : Value.t) : M :=
+    LowM.Pure (inr (Exception.Return value)).
 
   Parameter pass : M.
 
@@ -423,6 +427,14 @@ Module M.
 
   Parameter assert : Value.t -> M.
 
+  Definition catch_return (m : M) : M :=
+    let- v := m in
+    match v with
+    | inl v => pure v
+    | inr (Exception.Return v) => pure v
+    | inr e => LowM.Pure (inr e)
+    end.
+
   Parameter if_then_else : Value.t -> M -> M -> M.
 
   Parameter for_ : Value.t -> Value.t -> M -> M -> M.
diff --git a/CoqOfPython/builtins.v b/CoqOfPython/builtins.v
index e2a293e..2fe0184 100644
--- a/CoqOfPython/builtins.v
+++ b/CoqOfPython/builtins.v
@@ -2,6 +2,8 @@ Require Import CoqOfPython.CoqOfPython.
 
 Definition globals : Globals.t := "builtins".
 
+Definition locals_stack : list Locals.t := [].
+
 Definition type : Value.t :=
   make_klass {|
     Klass.bases := [];
@@ -26,5 +28,14 @@ Definition str : Value.t :=
   |}.
 Axiom str_in_globals : IsInGlobals "builtins" "str" str.
 
-Parameter len : Value.t -> Value.t -> M.
+Definition len : Value.t -> Value.t -> M :=
+  fun (args kwargs : Value.t) =>
+    let- locals_stack := M.create_locals locals_stack args kwargs [ "value" ] in
+    let* value := M.get_name globals locals_stack "value" in
+    let '(Value.Make _ _ pointer) := value in
+    let- object := M.read pointer in
+    match object.(Object.internal) with
+    | Some (Data.List list) => M.pure (Constant.int (Z.of_nat (List.length list)))
+    | _ => M.impossible
+    end.
 Axiom len_in_globals : IsInGlobals globals "len" (make_function len).
diff --git a/CoqOfPython/ethereum/paris/vm/simulations/proofs/exceptions.v b/CoqOfPython/ethereum/paris/vm/simulations/proofs/exceptions.v
new file mode 100644
index 0000000..8c8691b
--- /dev/null
+++ b/CoqOfPython/ethereum/paris/vm/simulations/proofs/exceptions.v
@@ -0,0 +1,35 @@
+Require Import CoqOfPython.CoqOfPython.
+Require Import simulations.proofs.CoqOfPython.
+Require Import simulations.proofs.heap.
+
+Require Import ethereum.paris.vm.simulations.exceptions.
+
+Import Run.
+
+Module ExceptionalHalt.
+  Definition to_value (exn : ExceptionalHalt.t) : Value.t :=
+    match exn with
+    | ExceptionalHalt.StackUnderflowError =>
+      Value.Make "exceptions" "StackUnderflowError" (Pointer.Imm Object.empty)
+    | ExceptionalHalt.StackOverflowError =>
+      Value.Make "exceptions" "StackOverflowError" (Pointer.Imm Object.empty)
+    | ExceptionalHalt.OutOfGasError =>
+      Value.Make "exceptions" "OutOfGasError" (Pointer.Imm Object.empty)
+    | ExceptionalHalt.InvalidOpcode code =>
+      Value.Make "exceptions" "InvalidOpcode" (Pointer.Imm (Object.wrapper (Data.Integer code)))
+    | ExceptionalHalt.InvalidJumpDestError =>
+      Value.Make "exceptions" "InvalidJumpDestError" (Pointer.Imm Object.empty)
+    | ExceptionalHalt.StackDepthLimitError =>
+      Value.Make "exceptions" "StackDepthLimitError" (Pointer.Imm Object.empty)
+    | ExceptionalHalt.WriteInStaticContext =>
+      Value.Make "exceptions" "WriteInStaticContext" (Pointer.Imm Object.empty)
+    | ExceptionalHalt.OutOfBoundsRead =>
+      Value.Make "exceptions" "OutOfBoundsRead" (Pointer.Imm Object.empty)
+    | ExceptionalHalt.InvalidParameter =>
+      Value.Make "exceptions" "InvalidParameter" (Pointer.Imm Object.empty)
+    | ExceptionalHalt.InvalidContractPrefix =>
+      Value.Make "exceptions" "InvalidContractPrefix" (Pointer.Imm Object.empty)
+    | ExceptionalHalt.AddressCollision =>
+      Value.Make "exceptions" "AddressCollision" (Pointer.Imm Object.empty)
+    end.
+End ExceptionalHalt.
diff --git a/CoqOfPython/ethereum/paris/vm/simulations/proofs/stack.v b/CoqOfPython/ethereum/paris/vm/simulations/proofs/stack.v
index fd7de01..32072b4 100644
--- a/CoqOfPython/ethereum/paris/vm/simulations/proofs/stack.v
+++ b/CoqOfPython/ethereum/paris/vm/simulations/proofs/stack.v
@@ -1,12 +1,14 @@
 Require Import CoqOfPython.CoqOfPython.
-Require Import proofs.CoqOfPython.
-Require Import simulations.CoqOfPython.
-Require Import proofs.heap.
+Require Import simulations.proofs.CoqOfPython.
+Require Import simulations.proofs.heap.
 
 Require ethereum.paris.vm.simulations.stack.
 Require ethereum.paris.vm.stack.
+Require CoqOfPython.builtins.
 
 Require ethereum.paris.vm.simulations.proofs.__init__.
+Require simulations.proofs.builtins.
+
 Module Evm := __init__.Evm.
 
 Import Run.
@@ -28,39 +30,155 @@ Module PopLocals.
     ].
 End PopLocals.
 
-Lemma run_pop (stack : Stack.t) (heap : Heap.t) :
-  let evm := Heap.to_evm heap in
-  let '(result, evm') := StateError.lift_lens Evm.Lens.stack simulations.stack.pop evm in
-  let result :=
-    match result with
-    | inl s' => inl Constant.None_
-    | inr exn => inr (Exception.Raise (Some Constant.None_))
-    end in
-  exists fresh_stack heap',
+(** Test function to experiment with the simulations. We might remove it later. *)
+Definition get_length : Value.t -> Value.t -> M :=
+  let globals := "ethereum.paris.vm.stack" in
+  let locals_stack := [] in
+
+  fun (args kwargs : Value.t) =>
+    let- locals_stack := M.create_locals locals_stack args kwargs [ "evm" ] in
+    M.catch_return ltac:(M.monadic (
+    let _ := Constant.str "
+    Returns the length of the stack.
+ 
+    Parameters
+    ----------
+    evm :
+        EVM stack.
+ 
+    Returns
+    -------
+    length : `int`
+        Length of the stack.
+ 
+    " in
+    let _ := M.return_ (|
+      M.call (|
+        M.get_name (| globals, locals_stack, "len" |),
+        make_list [
+          M.get_name (| globals, locals_stack, "evm" |)
+        ],
+        make_dict []
+      |)
+    |) in
+    M.pure Constant.None_)).
+ 
+(** Run for the function [get_length]. *)
+Definition run_get_length (stack : Stack.t) (heap : Heap.t) :
   {{ stack, heap |
-    stack.pop (make_list [Evm.stack_to_value]) (make_dict []) ⇓
-    result
-  | stack ++ fresh_stack, heap' }} /\
-  evm' = Heap.to_evm heap'.
+    stack.get_length (make_list [Evm.stack_to_value]) (make_dict []) ⇓
+    (fun (n : Z) => inl (Constant.int n))
+  |
+    fun stack' => stack' = stack,
+    fun heap' => heap' = heap
+  }}.
 Proof.
+  cbn.
+  apply Run.CallPrimitiveStateAllocImm.
+  cbn.
+  eapply Run.CallPrimitiveGetInGlobals. {
+    apply builtins_is_imported.
+    apply builtins.len_in_globals.
+  }
+  cbn.
+  eapply Run.CallClosure. {
+    eapply builtins.run_len.
+    { pose proof (H := IsRead.Heap stack heap Address.stack).
+      now apply H.
+    }
+    { reflexivity. }
+  }
   intros.
-  destruct StateError.lift_lens as [result evm'] eqn:?.
-  unfold stack.pop, simulations.stack.pop in *.
-  cbn in *.
-  repeat eexists.
-  { eapply Run.CallPrimitiveStateAllocMutable. {
-      now apply (IsAlloc.Stack PopLocals.to_object (PopLocals.init evm)).
+  cbn.
+  now eapply Run.Pure.
+Defined.
+
+(** Very simple version of the function [get_length], that actually only return the length of the
+    stack. *)
+Definition simple_get_length (heap : Heap.t) : Z :=
+  Z.of_nat (List.length heap.(Heap.stack)).
+
+(** We can show that it only returns the length of the stack by reflexivity! *)
+Lemma simple_get_length_eq stack heap :
+  simple_get_length heap =
+  let '(l, _, _) := evaluate (run_get_length stack heap) in
+  l.
+Proof.
+  reflexivity.
+Qed.
+
+(** Test module for demo purposes that could be removed later. *)
+Module TestGetLength.
+  (** Dummy value used for the compute below. *)
+  Definition dummy_heap : Heap.t := {|
+    Heap.evm := {|
+      Heap.Evm.pc := Uint.Make 12;
+      Heap.Evm.gas_left := Uint.Make 23;
+    |};
+    Heap.stack := [
+      U256.of_Z 42;
+      U256.of_Z 43;
+      U256.of_Z 44
+    ];
+  |}.
+
+  Definition current_length : Z :=
+    let '(l, _, _) := evaluate (run_get_length [] dummy_heap) in
+    l.
+
+  (* Should return 3 *)
+  (* Compute current_length. *)
+End TestGetLength.
+
+(** Run of the [pop] function. *)
+Definition run_pop (stack : Stack.t) (heap : Heap.t) :
+  {{ stack, heap |
+    stack.pop (make_list [Evm.stack_to_value]) (make_dict []) ⇓
+    (fun (result : unit + builtins.Exception.t) =>
+      match result with
+      | inl tt => inl Constant.None_
+      | inr exn => inr (Exception.Raise (Some (builtins.Exception.to_value exn)))
+      end)
+  |
+    fun stack' => exists fresh_stack, stack' = stack ++ fresh_stack,
+    fun heap' => True
+  }}.
+Proof.
+  cbn.
+  apply Run.CallPrimitiveStateAllocImm.
+  cbn.
+  eapply Run.CallPrimitiveGetInGlobals. {
+    apply builtins_is_imported.
+    apply builtins.len_in_globals.
+  }
+  cbn.
+  eapply Run.CallClosure. {
+    eapply builtins.run_len.
+    { pose proof (H := IsRead.Heap stack heap Address.stack).
+      now apply H.
     }
-    cbn.
-    eapply Run.CallPrimitiveStateRead. {
-      apply IsRead.Stack.
-      now erewrite Stack.read_length_eq.
+    { reflexivity. }
+  }
+  intros.
+  cbn.
+  replace (Compare.eq (Constant.int value_inter) (Constant.int 0))
+    with (M.pure (Constant.bool (value_inter =? 0)))
+    by admit.
+  cbn.
+  match goal with
+  | |- context [ M.if_then_else (Constant.bool ?cond) ] =>
+    replace (M.if_then_else (Constant.bool cond))
+      with (fun (success error : M) => if cond then success else error)
+      by admit
+  end.
+  destruct (_ =? _); cbn.
+  { admit. }
+  { eapply Run.CallPrimitiveStateRead. {
+      pose proof (H2 := IsRead.Heap stack_inter heap_inter Address.stack).
+      now apply H2.
     }
     cbn.
-    eapply Run.CallPrimitiveGetInGlobals. {
-      apply builtins_is_imported.
-      admit.
-    }
+    (* TODO: implement method calls *)
     admit.
   }
 Admitted.
diff --git a/CoqOfPython/ethereum/simulations/proofs/exceptions.v b/CoqOfPython/ethereum/simulations/proofs/exceptions.v
new file mode 100644
index 0000000..63ed17a
--- /dev/null
+++ b/CoqOfPython/ethereum/simulations/proofs/exceptions.v
@@ -0,0 +1,16 @@
+Require Import CoqOfPython.CoqOfPython.
+Require Import simulations.proofs.CoqOfPython.
+Require Import simulations.proofs.heap.
+
+Require ethereum.paris.vm.simulations.proofs.exceptions.
+Require ethereum.simulations.exceptions.
+
+Import Run.
+
+Module EthereumException.
+  Definition to_value (exn : exceptions.EthereumException.t) : Value.t :=
+    match exn with
+    | exceptions.EthereumException.ExceptionalHalt exn =>
+      Value.Make "exceptions" "ExceptionalHalt" (Pointer.Imm Object.empty)
+    end.
+End EthereumException.
diff --git a/CoqOfPython/simulations/proofs/CoqOfPython.v b/CoqOfPython/simulations/proofs/CoqOfPython.v
index 2ffab45..e5a856b 100644
--- a/CoqOfPython/simulations/proofs/CoqOfPython.v
+++ b/CoqOfPython/simulations/proofs/CoqOfPython.v
@@ -64,7 +64,7 @@ Module IsAlloc.
     Pointer.Mutable.t Value.t ->
     Object.t Value.t ->
     Stack.t -> Heap ->
-    Prop :=
+    Set :=
   | Stack {A : Set} to_object (value : A) object :
     let index := List.length stack in
     object = to_object value ->
@@ -92,7 +92,7 @@ Module IsRead.
     (stack : Stack.t) (heap : Heap) :
     Pointer.Mutable.t Value.t ->
     Object.t Value.t ->
-    Prop :=
+    Set :=
   | Stack {A : Set} index to_object (value : A) :
     Stack.read stack index = Some (existS A value) ->
     t
@@ -107,13 +107,27 @@ Module IsRead.
       (to_object value).
 End IsRead.
 
+Module PointerRead.
+  (** A generalization of [IsRead.t] to take into account immediate values. Useful for some
+      lemma. *)
+  Definition t `{Heap.Trait}
+      (stack : Stack.t) (heap : Heap)
+      (pointer : Pointer.t Value.t)
+      (object : Object.t Value.t) :
+      Set :=
+    match pointer with
+    | Pointer.Imm object' => object' = object
+    | Pointer.Mutable mutable => IsRead.t stack heap mutable object
+    end.
+End PointerRead.
+
 Module IsWrite.
   Inductive t `{Heap.Trait}
     (stack : Stack.t) (heap : Heap) :
     Pointer.Mutable.t Value.t ->
     Object.t Value.t ->
     Stack.t -> Heap ->
-    Prop :=
+    Set :=
   | Stack {A : Set} index to_object (update : A) update_object :
     let stack' := Stack.write stack index update in
     update_object = to_object update ->
@@ -133,36 +147,63 @@ Module IsWrite.
 End IsWrite.
 
 Module Run.
-  Reserved Notation "{{ stack , heap | e ⇓ result | stack' , heap' }}".
-
-  Inductive t `{Heap.Trait} {A : Set}
-      (* Be aware of the order of parameters: the result and final heap are at
-         the beginning. This is due to the way polymorphic types for inductive
-         work in Coq, and the fact that the result is always the same as we are
-         in continuation passing style. *)
-      {result : A} {stack' : Stack.t} {heap' : Heap} :
-      LowM.t A -> Stack.t -> Heap -> Prop :=
-  | Pure :
-    {{ stack', heap' |
-      LowM.Pure result ⇓
-      result
-    | stack', heap' }}
-  | CallPrimitiveStateAllocImmediate
-      (stack : Stack.t) (heap : Heap) (object : Object.t Value.t)
-      (k : Pointer.t Value.t -> LowM.t A) :
+  Reserved Notation "{{ stack , heap | e ⇓ to_value | P_stack , P_heap }}".
+
+  (** A execution trace of a monadic expression, where we do name resolution and explicit an
+      allocation strategy. We do not talk about the result, we only say that it exists. Thus we can
+      infer the result when building the trace rather than stating it beforehand. The [evaluate]
+      function defined after can compute this result from a trace. We will make our specifications
+      and proofs about the output of the [evaluate] function.
+
+      Even if we do not compute the result, we still constraint it with the [to_value] function,
+      saying that it should be in the image of this function, and with the [P_stack] and [P_heap]
+      predicates, saying that the stack and heap should respect some properties. This is mainly
+      useful for the [CallClosure] case, in order to avoid exploring impossible branches or
+      branches corresponding to ill-typed Python expressions at the return of a function call.
+
+      The [P_stack] and [P_heap] predicates should be very simple. The attempt here is not to
+      verify the code, only to build an execution trace. It should mainly contain information about
+      the size of the stack and the presence of some values in the heap, just enough to be able to
+      build the trace.
+  *)
+  Inductive t `{Heap.Trait} {A B : Set}
+      (stack : Stack.t) (heap : Heap)
+      (to_value : A -> B) (P_stack : Stack.t -> Prop) (P_heap : Heap -> Prop) :
+      LowM.t B -> Set :=
+  (** Final case of an execution. We check that [to_value], [P_stack], and [P_heap] are true. *)
+  | Pure
+    (* We can have some choices for the expression of [result]. One can use [rewrite] in order to
+       simplify the [result] expression and provide something that will simplify the proofs later.
+    *)
+    (result : A)
+    (result' : B) :
+    result' = to_value result ->
+    P_stack stack ->
+    P_heap heap ->
+    {{ stack, heap |
+      LowM.Pure result' ⇓
+      to_value
+    | P_stack, P_heap }}
+  (** Allocation as an immediate value for that values that will not be modified. If the code is
+      written in a purely functional way, we should only do immediate allocations. This removes the
+      need to manipulate pointers in the proofs later. *)
+  | CallPrimitiveStateAllocImm
+      (object : Object.t Value.t)
+      (k : Pointer.t Value.t -> LowM.t B) :
     {{ stack, heap |
       k (Pointer.Imm object) ⇓
-      result
-    | stack', heap' }} ->
+      to_value
+    | P_stack, P_heap }} ->
     {{ stack, heap |
       LowM.CallPrimitive (Primitive.StateAlloc object) k ⇓
-      result
-    | stack', heap' }}
+      to_value
+    | P_stack, P_heap }}
+  (** Allocation either on the stack or the heap. *)
   | CallPrimitiveStateAllocMutable
       (mutable : Pointer.Mutable.t Value.t)
       (object : Object.t Value.t)
-      (stack stack_inter : Stack.t) (heap heap_inter : Heap)
-      (k : Pointer.t Value.t -> LowM.t A) :
+      (stack_inter : Stack.t) (heap_inter : Heap)
+      (k : Pointer.t Value.t -> LowM.t B) :
     IsAlloc.t
       stack heap
       mutable
@@ -170,75 +211,170 @@ Module Run.
       stack_inter heap_inter ->
     {{ stack_inter, heap_inter |
       k (Pointer.Mutable mutable) ⇓
-      result
-    | stack', heap' }} ->
+      to_value
+    | P_stack, P_heap }} ->
     {{ stack, heap |
       LowM.CallPrimitive (Primitive.StateAlloc object) k ⇓
-      result
-    | stack', heap' }}
+      to_value
+    | P_stack, P_heap }}
+  (** Read of a pointer in the stack or the heap. *)
   | CallPrimitiveStateRead
       (mutable : Pointer.Mutable.t Value.t)
       (object : Object.t Value.t)
-      (stack : Stack.t) (heap : Heap)
-      (k : Object.t Value.t -> LowM.t A) :
+      (k : Object.t Value.t -> LowM.t B) :
     IsRead.t stack heap mutable object ->
     {{ stack, heap |
       k object ⇓
-      result
-    | stack', heap' }} ->
+      to_value
+    | P_stack, P_heap }} ->
     {{ stack, heap |
       LowM.CallPrimitive (Primitive.StateRead mutable) k ⇓
-      result
-    | stack', heap' }}
+      to_value
+    | P_stack, P_heap }}
+  (** Read to a pointer in the stack or the heap. *)
   | CallPrimitiveStateWrite
       (mutable : Pointer.Mutable.t Value.t)
       (update : Object.t Value.t)
-      (stack stack_inter : Stack.t) (heap heap_inter : Heap)
-      (k : unit -> LowM.t A) :
-    IsWrite.t stack heap mutable update stack' heap' ->
+      (stack_inter : Stack.t) (heap_inter : Heap)
+      (k : unit -> LowM.t B) :
+    IsWrite.t stack heap mutable update stack_inter heap_inter ->
     {{ stack_inter, heap_inter |
       k tt ⇓
-      result
-    | stack', heap' }} ->
+      to_value
+    | P_stack, P_heap }} ->
     {{ stack, heap |
       LowM.CallPrimitive (Primitive.StateWrite mutable update) k ⇓
-      result
-    | stack', heap' }}
+      to_value
+    | P_stack, P_heap }}
+  (** Name resolution for top-level names. *)
   | CallPrimitiveGetInGlobals
       (globals : Globals.t)
       (name : string)
       (value : Value.t)
-      (stack : Stack.t) (heap : Heap)
-      (k : Value.t -> LowM.t A) :
+      (k : Value.t -> LowM.t B) :
     IsInGlobals globals name value ->
     {{ stack, heap |
       k value ⇓
-      result
-    | stack', heap' }} ->
+      to_value
+    | P_stack, P_heap }} ->
     {{ stack, heap |
       LowM.CallPrimitive (Primitive.GetInGlobals globals name) k ⇓
-      result
-    | stack', heap' }}
-  | CallClosure
-      (stack stack_inter : Stack.t) (heap heap_inter : Heap)
+      to_value
+    | P_stack, P_heap }}
+  (** Call of a closure. We abstract away the detail of the call. We use closures as an explicit
+      abstraction barrier to split our traces. *)
+  | CallClosure {C : Set}
       (f : Value.t -> Value.t -> M)
       (args kwargs : Value.t)
-      (value : Value.t + Exception.t)
-      (k : Value.t + Exception.t -> LowM.t A) :
+      (to_value_inter : C -> Value.t + Exception.t)
+      (P_stack_inter : Stack.t -> Prop) (P_heap_inter : Heap -> Prop)
+      (k : Value.t + Exception.t -> LowM.t B) :
     let closure := Data.Closure f in
     {{ stack, heap |
       f args kwargs ⇓
-      value
-    | stack_inter, heap_inter }} ->
-    {{ stack_inter, heap_inter |
-      k value ⇓
-      result
-    | stack', heap' }} ->
+      to_value_inter
+    | P_stack_inter, P_heap_inter }} ->
+    (* We quantify over every possible values as we cannot compute the result of the closure here.
+       We only know that it exists and respect some constraints in this inductive definition. *)
+    (forall value_inter stack_inter heap_inter,
+      P_stack_inter stack_inter ->
+      P_heap_inter heap_inter ->
+      {{ stack_inter, heap_inter |
+        k (to_value_inter value_inter) ⇓
+        to_value
+      | P_stack, P_heap }}
+    ) ->
     {{ stack, heap |
       LowM.CallClosure closure args kwargs k ⇓
-      result
-    | stack', heap' }}
+      to_value
+    | P_stack, P_heap }}
 
-  where "{{ stack , heap | e ⇓ result | stack' , heap' }}" :=
-    (t (result := result) (stack' := stack') (heap' := heap') e stack heap).
+  where "{{ stack , heap | e ⇓ to_value | P_stack , P_heap }}" :=
+    (t stack heap to_value P_stack P_heap e).
 End Run.
+
+Import Run.
+
+(** Get the value computed from the trace of a monadic expression. We will do our proofs on the
+    output of this function, as it gives a purely functional interpretation of the translated
+    monadic expressions.
+
+    Do be able to do the induction in this definition, we also return a proof for [P_stack]
+    and [P_heap].
+*)
+Fixpoint evaluate `{Heap.Trait} {A B : Set}
+    {stack : Stack.t} {heap : Heap} {e : LowM.t B}
+    {to_value : A -> B} {P_stack : Stack.t -> Prop} {P_heap : Heap -> Prop}
+    (run : {{ stack, heap | e ⇓ to_value | P_stack, P_heap }}) :
+  A *
+  { stack : Stack.t | P_stack stack } *
+  { heap : Heap | P_heap heap }.
+Proof.
+  (* We use very explicit tactics in order to make sure that we build the definition we want. *)
+  destruct run.
+  { repeat split.
+    { exact result. }
+    { try eexists.
+      match goal with
+      | H : P_stack _ |- _ => exact H
+      end.
+    }
+    { try eexists.
+      match goal with
+      | H : P_heap _ |- _ => exact H
+      end.
+    }
+  }
+  { eapply evaluate.
+    exact run.
+  }
+  { eapply evaluate.
+    exact run.
+  }
+  { eapply evaluate.
+    exact run.
+  }
+  { eapply evaluate.
+    exact run.
+  }
+  { eapply evaluate.
+    exact run.
+  }
+  { destruct (evaluate _ _ _ _ _ _ _ _ _ _ _ run) as
+      [[value_inter [stack_inter H_stack_inter]] [heap_inter H_heap_inter]].
+    eapply evaluate.
+    match goal with
+    | H : forall _ _ _, _ |- _ => apply (H value_inter)
+    end.
+    { exact H_stack_inter. }
+    { exact H_heap_inter. }
+  }
+Defined.
+
+(** Trace of the read at a memory location, wether it is an immediate or allocated value. *)
+Definition run_read `{Heap.Trait} {A : Set}
+    (stack : Stack.t) (heap : Heap)
+    (pointer : Pointer.t Value.t)
+    (object : Object.t Value.t)
+    (to_value : A -> Value.t + Exception.t)
+    (k : Object.t Value.t -> M)
+    (P_stack : Stack.t -> Prop) (P_heap : Heap -> Prop)
+    (H_pointer : PointerRead.t stack heap pointer object) :
+  {{ stack, heap |
+    k object ⇓
+    to_value
+  | P_stack, P_heap }} ->
+  {{ stack, heap |
+    LowM.bind (M.read pointer) k ⇓
+    to_value
+  | P_stack, P_heap }}.
+Proof.
+  intros.
+  destruct pointer; cbn in *.
+  { congruence. }
+  { eapply Run.CallPrimitiveStateRead. {
+      apply H_pointer.
+    }
+    trivial.
+  }
+Defined.
diff --git a/CoqOfPython/simulations/proofs/builtins.v b/CoqOfPython/simulations/proofs/builtins.v
new file mode 100644
index 0000000..6696fbd
--- /dev/null
+++ b/CoqOfPython/simulations/proofs/builtins.v
@@ -0,0 +1,48 @@
+Require Import CoqOfPython.CoqOfPython.
+Require Import simulations.proofs.CoqOfPython.
+Require Import simulations.proofs.heap.
+
+Require CoqOfPython.builtins.
+Require ethereum.simulations.proofs.exceptions.
+
+Import Run.
+
+Module ArithmeticError.
+  Definition to_value (exn : builtins.ArithmeticError.t) : Value.t :=
+    match exn with
+    | builtins.ArithmeticError.OverflowError =>
+      Value.Make "builtins" "OverflowError" (Pointer.Imm Object.empty)
+    end.
+End ArithmeticError.
+
+Module Exception.
+  Definition to_value (exn : builtins.Exception.t) : Value.t :=
+    match exn with
+    | builtins.Exception.ArithmeticError exn => ArithmeticError.to_value exn
+    | builtins.Exception.EthereumException exn => exceptions.EthereumException.to_value exn
+    end.
+End Exception.
+
+(** Run of the primitive [len] function. *)
+Definition run_len {A : Set} (stack : Stack.t) (heap : Heap.t)
+  pointer object (l : list A) (to_value : A -> Value.t)
+  (H_pointer : PointerRead.t stack heap pointer object)
+  (H_object : object = Object.wrapper (Data.List (List.map to_value l))) :
+  {{ stack, heap |
+    builtins.len (make_list [Value.Make "builtins" "list" pointer]) (make_dict []) ⇓
+    (fun (n : Z) => inl (Constant.int n))
+  |
+    fun stack' => stack' = stack,
+    fun heap' => heap' = heap
+  }}.
+Proof.
+  intros.
+  cbn.
+  apply Run.CallPrimitiveStateAllocImm.
+  cbn.
+  eapply run_read. {
+    apply H_pointer.
+  }
+  rewrite H_object; cbn.
+  now eapply Run.Pure; try rewrite List.map_length.
+Defined.