diff --git a/CoqOfRust/RecordUpdate.v b/CoqOfRust/RecordUpdate.v
index 6dca6f571..58526e6c4 100644
--- a/CoqOfRust/RecordUpdate.v
+++ b/CoqOfRust/RecordUpdate.v
@@ -72,6 +72,8 @@ Class Setter{R E: Type}(getter: R -> E): Type :=
   set : E -> R -> R.
 
 Arguments set {R E} (getter) {Setter} (fieldUpdater) (r).
+(* Reduce when calling the [cbn] tactic *)
+Arguments set /.
 
 Global Hint Extern 1 (@Setter ?R ?E ?getter) =>
   exact_setter R getter : typeclass_instances.
diff --git a/CoqOfRust/core/simulations/eq.v b/CoqOfRust/core/simulations/eq.v
index 95a3233b5..c034ecd6c 100644
--- a/CoqOfRust/core/simulations/eq.v
+++ b/CoqOfRust/core/simulations/eq.v
@@ -2,6 +2,14 @@ Module Eq.
   Class Trait (Self : Set) : Set := {
     eqb: Self -> Self -> bool
   }.
+
+  Module Valid.
+  (** An equality [equal] is valid when it decides the standard equality [=]. *)
+  Definition t {Self : Set} `{Trait Self} (domain : Self -> Prop) : Prop :=
+    forall x y,
+    domain x -> domain y ->
+    (x = y) <-> (eqb x y = true).
+  End Valid.
 End Eq.
 
 Module Notations.
diff --git a/CoqOfRust/move_sui/proofs/move_abstract_stack/lib.v b/CoqOfRust/move_sui/proofs/move_abstract_stack/lib.v
index c9f7b8f1d..9abb51146 100644
--- a/CoqOfRust/move_sui/proofs/move_abstract_stack/lib.v
+++ b/CoqOfRust/move_sui/proofs/move_abstract_stack/lib.v
@@ -18,6 +18,9 @@ Module AbstractStack.
 
     Definition get_length {A : Set} (stack : list (Z * A)) : Z :=
       List.fold_right (fun '(n, _) acc => n + acc)%Z 0 stack.
+
+    Definition flatten {A : Set} (stack : list (Z * A)) : list A :=
+      List.flat_map (fun '(n, v) => List.repeat v (Z.to_nat n)) stack.
   End Stack.
 
   (** The length as computed by summing all the repetition numbers *)
@@ -35,7 +38,7 @@ Module AbstractStack.
 
   (** A version of the stack where we unfold the types that are with a repeat counter *)
   Definition flatten {A : Set} (abstract_stack : AbstractStack.t A) : list A :=
-    List.flat_map (fun '(n, v) => List.repeat v (Z.to_nat n)) abstract_stack.(AbstractStack.values).
+    Stack.flatten abstract_stack.(AbstractStack.values).
 
   Lemma push_n_is_valid {A : Set} `{Eq.Trait A}
       (item : A) (n : Z) (stack : AbstractStack.t A)
@@ -67,9 +70,9 @@ Module AbstractStack.
       destruct H.(Eq.eqb); cbn.
       { constructor; cbn.
         { inversion_clear H_values; constructor; lia. }
-        { split; [hauto lq: on|].
-          (* FIX *)
-          admit.
+        { (* We admit there are no overflows here *)
+          replace ((count + n) mod _) with (count + n)%Z by admit.
+          lia.
         }
       }
       { constructor; cbn.
@@ -82,6 +85,59 @@ Module AbstractStack.
     }
   Admitted.
 
+  Lemma flatten_push_n {A : Set} `{Eq.Trait A} (item : A) (n : Z) (stack : AbstractStack.t A)
+      (H_Eq : Eq.Valid.t (fun _ => True))
+      (H_n : Integer.Valid.t IntegerKind.U64 n)
+      (H_stack : AbstractStack.Valid.t stack) :
+    match AbstractStack.push_n item n stack with
+    | Panic.Value (Result.Ok tt, stack') =>
+      flatten stack' = List.repeat item (Z.to_nat n) ++ flatten stack
+    | _ => True
+    end.
+  Proof.
+    unfold AbstractStack.push_n; cbn.
+    destruct (n =? 0) eqn:?; cbn.
+    { destruct stack as [values len]; cbn.
+      { replace n with 0 by lia. reflexivity. }
+    }
+    { step; cbn; [|exact I].
+      rename Heqo into H_checked_add_stack.
+      rename z into new_len.
+      destruct stack as [values len]; cbn in *.
+      unfold_state_monad.
+      destruct values as [|[count last_item] values]; cbn; [reflexivity|].
+      step; cbn; [|reflexivity].
+      rewrite List.app_assoc; f_equal.
+      (* We admit there are no overflows here *)
+      replace ((count + n) mod _) with (count + n)%Z by admit.
+      replace last_item with item by now apply H_Eq.
+      rewrite <- List.repeat_app.
+      f_equal.
+      rewrite <- Z2Nat.inj_add; [lia | lia |].
+      destruct H_stack as [H_stack ?]; cbn in *.
+      inversion_clear H_stack.
+      lia.
+    }
+  Admitted.
+
+  Lemma check_push_n {A : Set} `{Eq.Trait A} (item : A) (n : Z) (stack : AbstractStack.t A)
+      (H_Eq : Eq.Valid.t (fun _ => True))
+      (H_n : Integer.Valid.t IntegerKind.U64 n)
+      (H_stack : AbstractStack.Valid.t stack) :
+    match AbstractStack.push_n item n stack with
+    | Panic.Value (Result.Ok tt, stack') =>
+      AbstractStack.Valid.t stack' /\
+      flatten stack' = List.repeat item (Z.to_nat n) ++ flatten stack
+      | Panic.Value (Result.Err _, stack') =>
+      stack' = stack
+    | _ => True
+    end.
+  Proof.
+    pose proof (push_n_is_valid item n stack H_n H_stack).
+    pose proof (flatten_push_n item n stack H_Eq H_n H_stack).
+    hauto l: on.
+  Qed.
+
   Lemma push_is_valid {A : Set} `{Eq.Trait A}
       (item : A) (stack : AbstractStack.t A)
       (H_stack : AbstractStack.Valid.t stack) :
@@ -96,6 +152,37 @@ Module AbstractStack.
     apply push_n_is_valid; lia.
   Qed.
 
+  Lemma flatten_push {A : Set} `{Eq.Trait A} (item : A) (stack : AbstractStack.t A)
+      (H_Eq : Eq.Valid.t (fun _ => True))
+      (H_stack : AbstractStack.Valid.t stack) :
+    match AbstractStack.push item stack with
+    | Panic.Value (Result.Ok tt, stack') =>
+      flatten stack' = item :: flatten stack
+    | _ => True
+    end.
+  Proof.
+    unfold AbstractStack.push.
+    pose proof (flatten_push_n item 1 stack) as H_push_n.
+    apply H_push_n; lia.
+  Qed.
+
+  Lemma check_push {A : Set} `{Eq.Trait A} (item : A) (stack : AbstractStack.t A)
+      (H_Eq : Eq.Valid.t (fun _ => True))
+      (H_stack : AbstractStack.Valid.t stack) :
+    match AbstractStack.push item stack with
+    | Panic.Value (Result.Ok tt, stack') =>
+      AbstractStack.Valid.t stack' /\
+      flatten stack' = item :: flatten stack
+    | Panic.Value (Result.Err _, stack') =>
+      stack' = stack
+    | _ => True
+    end.
+  Proof.
+    pose proof (push_is_valid item stack H_stack) as H_push_is_valid.
+    pose proof (flatten_push item stack H_Eq H_stack) as H_flatten_push.
+    hauto l: on.
+  Qed.
+
   Lemma pop_eq_n_is_valid {A : Set} `{Eq.Trait A}
       (n : Z) (stack : AbstractStack.t A)
       (H_n : Integer.Valid.t IntegerKind.U64 n)
@@ -120,21 +207,20 @@ Module AbstractStack.
         { step; cbn in *.
           { constructor; cbn.
             { sauto lq: on rew: off. }
-            { split; destruct H_stack as [H_values H_len]; cbn in *.
-              { lia. }
-              { destruct H_len. hauto l: on. } 
-            }
+            { destruct H_stack; cbn in *; split; lia. }
           }
           { constructor; cbn; inversion_clear H_stack as [H_values H_len].
             { inversion_clear H_values.
-              constructor; [lia | assumption]. }
+              constructor; lia.
+            }
             { split.
               { destruct H_len as [H_len_valid H_len_eq].
                 unfold get_length in *; cbn in *.
                 rewrite H_len_eq.
                 unfold Stack.get_length; cbn; lia. }
               { inversion_clear H_values; cbn in *.
-                inversion_clear H_len. lia. }
+                inversion_clear H_len. lia.
+              }
             }
           }
         }
@@ -142,6 +228,35 @@ Module AbstractStack.
     }
   Qed.
 
+  Lemma flatten_pop_eq_n {A : Set} `{Eq.Trait A} (n : Z) (stack : AbstractStack.t A) 
+      (H_n : n >= 0) :
+    match AbstractStack.pop_eq_n n stack with
+    | Panic.Value (Result.Ok item, stack') =>
+      flatten stack = List.repeat item (Z.to_nat n) ++ flatten stack'
+    | _ => True
+    end.
+  Proof.
+    unfold AbstractStack.pop_eq_n.
+    step; cbn.
+    { trivial. }
+    { destruct stack as [values len]; cbn.
+      destruct values as [|[count last_item] values]; cbn.
+      { trivial. }
+      { destruct (count <? n) eqn:H_count_is_negative; cbn.
+        { trivial. }
+        { destruct (count =? n) eqn:H_count_eq_n; cbn.
+          { replace count with n by lia. reflexivity. }
+          { rewrite List.app_assoc.
+            f_equal.
+            rewrite <- List.repeat_app.
+            f_equal.
+            rewrite <- Z2Nat.inj_add; lia.
+          }
+        }
+      }
+    }
+  Qed.
+
   Lemma pop_is_valid {A : Set} `{Eq.Trait A}
       (stack : AbstractStack.t A)
       (H_stack : AbstractStack.Valid.t stack) :
@@ -156,6 +271,35 @@ Module AbstractStack.
     apply pop_eq_n_is_valid; lia.
   Qed.
 
+  Lemma flatten_pop {A : Set} `{Eq.Trait A} (stack : AbstractStack.t A) :
+    match AbstractStack.pop stack with
+    | Panic.Value (Result.Ok item, stack') =>
+      flatten stack = item :: flatten stack'
+    | _ => True
+    end.
+  Proof.
+    unfold AbstractStack.pop.
+    pose proof (flatten_pop_eq_n 1 stack) as H_pop_eq_n.
+    apply H_pop_eq_n; lia.
+  Qed.
+
+  Lemma check_pop {A : Set} `{Eq.Trait A}
+      (stack : AbstractStack.t A)
+      (H_stack : AbstractStack.Valid.t stack) :
+    match AbstractStack.pop stack with
+    | Panic.Value (Result.Ok item, stack') =>
+      AbstractStack.Valid.t stack' /\
+      flatten stack = item :: flatten stack'
+    | Panic.Value (Result.Err _, stack') =>
+      stack' = stack
+    | _ => True
+    end.
+  Proof.
+    pose proof (pop_is_valid stack H_stack) as H_pop_is_valid.
+    pose proof (flatten_pop stack) as H_flatten_pop.
+    hauto l: on.
+  Qed.
+
   Lemma pop_any_n_helper_is_valid {A : Set}
     (values : list (Z * A)) (rem : Z)
     (H_values : AbstractStack.Stack.Valid.t values)
@@ -181,6 +325,49 @@ Module AbstractStack.
     }
   Qed.
 
+  Lemma flatten_pop_any_n_helper {A : Set} (values : list (Z * A)) (rem : Z)
+      (H_values : AbstractStack.Stack.Valid.t values)
+      (H_rem : rem >= 0) :
+    match AbstractStack.pop_any_n_helper values rem with
+    | Panic.Value values' =>
+      exists items,
+      List.length items = Z.to_nat rem /\
+      Stack.flatten values = items ++ Stack.flatten values'
+    | Panic.Panic _ => True
+    end.
+  Proof.
+    revert rem H_rem.
+    induction values as [|[count last] values]; cbn; intros.
+    { step; cbn; [exact I|].
+      exists []; cbn; split; lia.
+    }
+    { step; cbn.
+      { step; cbn.
+        { assert (H_rem_count : rem - count >= 0) by lia.
+          inversion_clear H_values as [|? ? H_count H_values'].
+          pose proof (IHvalues H_values' (rem - count) H_rem_count) as IHvalues'.
+          destruct  AbstractStack.pop_any_n_helper as [values'|]; cbn; [|exact I].
+          destruct IHvalues' as [items [H_items_len H_items_eq]].
+          exists (List.repeat last (Z.to_nat count) ++ items); split.
+          { rewrite List.app_length, List.repeat_length, H_items_len.
+            rewrite Z2Nat.inj_sub; lia.
+          }
+          { rewrite <- List.app_assoc; f_equal.
+            now rewrite <- H_items_eq.
+          }
+        }
+        { exists (List.repeat last (Z.to_nat rem)); split.
+          { rewrite List.repeat_length; lia. }
+          { rewrite List.app_assoc; f_equal.
+            rewrite <- List.repeat_app; f_equal.
+            rewrite <- Z2Nat.inj_add; lia.
+          }
+        }
+      }
+      { exists []; cbn; split; lia. }
+    }
+  Qed.
+
   Lemma get_length_pop_any_n_helper {A : Set}
     (values : list (Z * A)) (rem : Z)
     (H_values : AbstractStack.Stack.Valid.t values)
@@ -250,84 +437,8 @@ Module AbstractStack.
     }
   Qed.
 
-  Lemma flatten_push_n {A : Set} `{Eq.Trait A} (item : A) (n : Z) (stack : AbstractStack.t A) 
-      (H_n : n >= 0) :
-    match AbstractStack.push_n item n stack with
-    | Panic.Value (Result.Ok tt, stack') =>
-      flatten stack' = List.repeat item (Z.to_nat n) ++ flatten stack
-    | _ => True
-    end.
-  Proof.
-    unfold AbstractStack.push_n; cbn.
-    destruct (n =? 0) eqn:?; cbn.
-    { destruct stack as [values len]; cbn.
-      { replace n with 0 by lia. reflexivity. }
-    }
-    { step.
-      rename Heqo into H_checked_add_stack.
-      rename z into new_len. cbn.
-      destruct stack as [values len].
-      { cbn. (* Still complex to dive in with lots of monad *)
-        admit.
-      }
-      { cbn; trivial. } 
-    }
-  Admitted.
-
-  Lemma flatten_push {A : Set} `{Eq.Trait A} (item : A) (stack : AbstractStack.t A) :
-    match AbstractStack.push item stack with
-    | Panic.Value (Result.Ok tt, stack') =>
-      flatten stack' = item :: flatten stack
-    | _ => True
-    end.
-  Proof.
-    unfold AbstractStack.push.
-    pose proof (flatten_push_n item 1 stack) as H_push_n.
-    apply H_push_n; lia.
-  Qed.
-
-  Lemma flatten_pop_eq_n {A : Set} `{Eq.Trait A} (n : Z) (stack : AbstractStack.t A) 
-      (H_n : n >= 0) :
-    match AbstractStack.pop_eq_n n stack with
-    | Panic.Value (Result.Ok item, stack') =>
-      flatten stack = List.repeat item (Z.to_nat n) ++ flatten stack'
-    | _ => True
-    end.
-  Proof.
-    unfold AbstractStack.pop_eq_n.
-    step; cbn.
-    { trivial. }
-    { destruct stack as [values len]; cbn.
-      destruct values as [|[count last_item] values]; cbn.
-      { trivial. }
-      { destruct (count <? n) eqn:H_count_is_negative; cbn.
-        { trivial. }
-        { destruct (count =? n) eqn:H_count_eq_n; cbn.
-          { replace count with n by lia. reflexivity. }
-          { rewrite List.app_assoc.
-            f_equal.
-            rewrite <- List.repeat_app.
-            f_equal.
-            rewrite <- Z2Nat.inj_add; lia.
-          }
-        }
-      }
-    }
-  Qed.
-
-  Lemma flatten_pop {A : Set} `{Eq.Trait A} (stack : AbstractStack.t A) :
-    match AbstractStack.pop stack with
-    | Panic.Value (Result.Ok item, stack') =>
-      flatten stack = item :: flatten stack'
-    | _ => True
-    end.
-  Proof.
-    unfold AbstractStack.pop.
-    pose proof (flatten_pop_eq_n 1 stack) as H_pop_eq_n.
-    apply H_pop_eq_n; lia.
-  Qed.
-
   Lemma flatten_pop_any_n {A : Set} `{Eq.Trait A} (n : Z) (stack : AbstractStack.t A)
+      (H_stack : AbstractStack.Valid.t stack)
       (H_n : n >= 0) :
     match AbstractStack.pop_any_n n stack with
     | Panic.Value (Result.Ok tt, stack') =>
@@ -337,5 +448,11 @@ Module AbstractStack.
     | _ => True
     end.
   Proof.
-  Admitted.
+    unfold AbstractStack.pop_any_n.
+    step; cbn; [exact I|].
+    pose proof (flatten_pop_any_n_helper stack.(AbstractStack.values) n)
+      as H_pop_any_n_helper.
+    destruct AbstractStack.pop_any_n_helper; cbn; [|exact I].
+    sauto lq: on rew: off.
+  Qed.
 End AbstractStack.
diff --git a/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v b/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
index 9c6711cf7..2ae40661f 100644
--- a/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
+++ b/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
@@ -33,14 +33,47 @@ Module IsValueOfType.
     (* TODO: other cases *)
     | _, _ => False
     end.
+
+  Lemma value_of_bool (value : Value.t) (H_value : IsValueOfType.t value SignatureToken.Bool) :
+    exists b, value = ValueImpl.Bool b.
+  Proof.
+    destruct value; cbn; try contradiction.
+    now eexists.
+  Qed.
+
+  Lemma value_of_integer (value : Value.t) (ty : SignatureToken.t)
+      (H_value : t value ty)
+      (H_ty : SignatureToken.is_integer ty = true) :
+    match value with
+    | ValueImpl.U8 _
+    | ValueImpl.U16 _
+    | ValueImpl.U32 _
+    | ValueImpl.U64 _
+    | ValueImpl.U128 _
+    | ValueImpl.U256 _ => True
+    | _ => False
+    end.
+  Proof.
+    now destruct value, ty; cbn in *.
+  Qed.
 End IsValueOfType.
 
 Module IsStackValueOfType.
   Definition t (stack : Stack.t) (abstract_stack : AbstractStack.t SignatureToken.t) : Prop :=
-    List.Forall2
-      IsValueOfType.t
+    List.Forall2 IsValueOfType.t
       stack.(Stack.value)
       (AbstractStack.flatten abstract_stack).
+  Arguments t /.
+
+  Lemma pop stack operand_ty stack_ty :
+    List.Forall2 IsValueOfType.t stack (operand_ty :: AbstractStack.flatten stack_ty) ->
+    exists value stack',
+      stack = value :: stack' /\
+      IsValueOfType.t value operand_ty /\
+      List.Forall2 IsValueOfType.t stack' (AbstractStack.flatten stack_ty).
+  Proof.
+    sauto lq: on.
+  Qed.
 End IsStackValueOfType.
 
 (** Here we show that all the stack operations on values follow the stack operations on types *)
@@ -57,6 +90,7 @@ Module IsInterpreterContextOfType.
     IsStackValueOfType.t
       interpreter.(Interpreter.operand_stack)
       type_safety_checker.(TypeSafetyChecker.stack).
+  Arguments t /.
 End IsInterpreterContextOfType.
 
 (* To know in which case we are *)
@@ -65,46 +99,57 @@ Ltac guard_instruction expected_instruction :=
   | _ : _ = expected_instruction |- _ => idtac
   end.
 
-Ltac unfold_state_monad :=
-  repeat (
-    unfold StatePanicResult.bind, StatePanic.bind, StatePanic.bind,
-      "return!toS!", 
-      "liftS!", 
-      "readS!", 
-      "return!toS!?";
-    cbn
-  ).
+Ltac destruct_post H :=
+  match type of H with
+  | ?H1 /\ ?H2 =>
+    let H1' := fresh "H_post" in
+    let H2' := fresh "H_post" in
+    destruct H as [H1' H2'];
+    destruct_post H1';
+    destruct_post H2'
+  | _ = _ =>
+    rewrite H in *;
+    clear H
+  | exists _, _ =>
+    let H' := fresh "H_post" in
+    destruct H as [? H'];
+    destruct_post H'
+  | _ => idtac
+  end.
+
+Ltac destruct_abstract_pop :=
+  unfold_state_monad;
+  match goal with
+  | H_stack : _ |- context[AbstractStack.pop ?stack] =>
+    let H_check_pop := fresh "H_check_pop" in
+    pose proof (AbstractStack.check_pop stack H_stack) as H_check_pop;
+    destruct (AbstractStack.pop stack) as [[[?operand_ty |] ?stack_ty] |];
+      cbn; [|exact I | exact I];
+    destruct_post H_check_pop
+  end;
+  match goal with
+  | H_interpreter : _ |- _ =>
+    destruct_post (IsStackValueOfType.pop _ _ _ H_interpreter);
+    clear H_interpreter
+  end.
 
 Ltac destruct_abstract_push :=
   unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push;
   with_strategy opaque [AbstractStack.push] unfold_state_monad;
   match goal with
-  | |- context[AbstractStack.push ?item ?stack] =>
-    pose proof (
-      AbstractStack.flatten_push item stack
-    ) as H_push
-  end;
-  destruct AbstractStack.push as [[[[]|] ?stack_ty]|]; cbn; [|exact I | exact I].
-
-Ltac destruct_abstract_pop H_interpreter :=
-  unfold_state_monad;
-    let H_pop := fresh "H_pop" in
-    match goal with
-    | |- context[AbstractStack.pop ?stack] =>
-      pose proof (
-        AbstractStack.flatten_pop stack
-      ) as H_pop
-    end;
-    destruct AbstractStack.pop as [[[?operand_ty |] ?stack_ty] |];
-      cbn; [|exact I | exact I];
-    rewrite H_pop in H_interpreter; cbn in H_interpreter;
-    clear H_pop.
+  | H_Eq : _, H_stack : _ |- context[AbstractStack.push ?operand_ty ?stack] =>
+    let H_check_push := fresh "H_check_push" in
+    pose proof (AbstractStack.check_push operand_ty stack H_Eq H_stack) as H_check_push;
+    destruct AbstractStack.push as [[[[]|] ?]|]; cbn; try exact I;
+    destruct_post H_check_push
+  end.
 
 Lemma progress
     (ty_args : list _Type.t) (function : loader.Function.t) (resolver : loader.Resolver.t)
     (instruction : Bytecode.t)
     (pc : Z) (locals : Locals.t) (interpreter : Interpreter.t)
     (type_safety_checker : TypeSafetyChecker.t)
+    (H_type_safety_checker : TypeSafetyChecker.Valid.t type_safety_checker)
     (H_interpreter : IsInterpreterContextOfType.t locals interpreter type_safety_checker) :
   let state := {|
     State.pc := pc;
@@ -123,191 +168,154 @@ Lemma progress
       State.interpreter := interpreter';
     |} := state' in
     IsInterpreterContextOfType.t locals' interpreter' type_safety_checker'
+  (* If the type-checker succeeds, then the interpreter cannot return an error *)
+  | Panic.Value (Result.Ok _, _), Panic.Panic _ => False
+  | Panic.Value (Result.Ok _, _), Panic.Value (Result.Err error, _) =>
+    let '{| PartialVMError.major_status := major_status |} := error in
+    match major_status with
+    | StatusCode.EXECUTION_STACK_OVERFLOW
+    | StatusCode.ARITHMETIC_ERROR => True
+    | _ => False
+    end
   | _, _ => True
   end.
 Proof.
   Opaque AbstractStack.flatten.
+  pose proof file_format.SignatureToken.ImplEq.I_is_valid as H_Eq.
   destruct interpreter as [[stack]].
-  destruct instruction eqn:H_instruction_eq; cbn in *;
-    unfold IsInterpreterContextOfType.t, IsStackValueOfType.t in H_interpreter.
+  destruct type_safety_checker as [module function_context locals_ty stack_ty]; cbn in *.
+  destruct H_type_safety_checker as [H_stack_ty]; cbn in *.
+  destruct instruction eqn:H_instruction_eq; cbn in *.
   { guard_instruction Bytecode.Pop.
-    destruct_abstract_pop H_interpreter.
-    admit.
+    destruct_abstract_pop.
+    repeat (step; cbn; try easy).
   }
   { guard_instruction Bytecode.Ret.
     admit.
   }
   { guard_instruction (Bytecode.BrTrue z).
-    destruct_abstract_pop H_interpreter.
+    destruct_abstract_pop.
     pose proof SignatureToken.t_beq_is_valid operand_ty SignatureToken.Bool as H_beq.
     destruct SignatureToken.t_beq; cbn; [|exact I].
-    replace operand_ty with SignatureToken.Bool in H_interpreter by sfirstorder; clear H_beq.
-    unfold Stack.Impl_Stack.pop_as, Stack.Impl_Stack.pop; cbn.
-    unfold_state_monad.
-    cbn in *.
-    inversion_clear H_interpreter as [|operand ? stack' ? H_operand_bool H_stack']; cbn.
-    assert (exists b, operand = ValueImpl.Bool b) as [b H_operand_eq]. {
-      destruct operand; cbn; try contradiction; sfirstorder.
-    }
-    rewrite H_operand_eq; clear H_operand_eq; cbn.
-    apply H_stack'.
+    replace operand_ty with SignatureToken.Bool in * by hauto lq: on; clear H_beq.
+    match goal with
+    | H : _ |- _ => destruct_post (IsValueOfType.value_of_bool _ H)
+    end; cbn.
+    hauto l: on.
   }
   { guard_instruction (Bytecode.BrFalse z).
-    destruct_abstract_pop H_interpreter.
+    destruct_abstract_pop.
     pose proof SignatureToken.t_beq_is_valid operand_ty SignatureToken.Bool as H_beq.
     destruct SignatureToken.t_beq; cbn; [|exact I].
-    replace operand_ty with SignatureToken.Bool in H_interpreter by sfirstorder; clear H_beq.
-    unfold Stack.Impl_Stack.pop_as, Stack.Impl_Stack.pop; cbn.
-    unfold_state_monad.
-    cbn in *.
-    inversion_clear H_interpreter as [|operand ? stack' ? H_operand_bool H_stack']; cbn.
-    assert (exists b, operand = ValueImpl.Bool b) as [b H_operand_eq]. {
-      destruct operand; cbn; try contradiction; sfirstorder.
-    }
-    rewrite H_operand_eq; clear H_operand_eq; cbn.
-    apply H_stack'.
+    replace operand_ty with SignatureToken.Bool in * by hauto lq: on; clear H_beq.
+    match goal with
+    | H : _ |- _ => destruct_post (IsValueOfType.value_of_bool _ H)
+    end; cbn.
+    hauto l: on.
   }
   { guard_instruction (Bytecode.Branch z).
     apply H_interpreter.
   }
   { guard_instruction (Bytecode.LdU8 z).
     destruct_abstract_push.
-    lib.step; cbn; [|exact I].
-    unfold IsInterpreterContextOfType.t; cbn.
-    unfold IsStackValueOfType.t; cbn.
-    rewrite H_push.
-    hauto l: on.
+    step; cbn; [|easy].
+    sauto lq: on.
   }
   { guard_instruction (Bytecode.LdU16 z).
     destruct_abstract_push.
-    lib.step; cbn; [|exact I].
-    unfold IsInterpreterContextOfType.t; cbn.
-    unfold IsStackValueOfType.t; cbn.
-    rewrite H_push.
-    hauto l: on.
+    step; cbn; [|easy].
+    sauto lq: on.
   }
   { guard_instruction (Bytecode.LdU32 z).
     destruct_abstract_push.
-    lib.step; cbn; [|exact I].
-    unfold IsInterpreterContextOfType.t; cbn.
-    unfold IsStackValueOfType.t; cbn.
-    rewrite H_push.
-    hauto l: on.
+    step; cbn; [|easy].
+    sauto lq: on.
   }
   { guard_instruction (Bytecode.LdU64 z).
     destruct_abstract_push.
-    lib.step; cbn; [|exact I].
-    unfold IsInterpreterContextOfType.t; cbn.
-    unfold IsStackValueOfType.t; cbn.
-    rewrite H_push.
-    hauto l: on.
+    step; cbn; [|easy].
+    sauto lq: on.
   }
   { guard_instruction (Bytecode.LdU128 z).
     destruct_abstract_push.
-    lib.step; cbn; [|exact I].
-    unfold IsInterpreterContextOfType.t; cbn.
-    unfold IsStackValueOfType.t; cbn.
-    rewrite H_push.
-    hauto l: on.
+    step; cbn; [|easy].
+    sauto lq: on.
   }
   { guard_instruction (Bytecode.LdU256 z).
     destruct_abstract_push.
-    lib.step; cbn; [|exact I].
-    unfold IsInterpreterContextOfType.t; cbn.
-    unfold IsStackValueOfType.t; cbn.
-    rewrite H_push.
-    hauto l: on.
+    step; cbn; [|easy].
+    sauto lq: on.
   }
   { guard_instruction Bytecode.CastU8.
-    destruct_abstract_pop H_interpreter.
-    lib.step; cbn; [exact I|].
+    destruct_abstract_pop.
+    step; cbn; [exact I|].
     destruct_abstract_push.
-    destruct stack as [|operand stack]; cbn; [exact I|].
-    destruct operand; cbn; try exact I; (
-      repeat (lib.step; cbn; [|exact I]);
-      unfold IsInterpreterContextOfType.t, IsStackValueOfType.t; cbn;
-      sauto lq: on
-    ).
+    step; cbn; (try easy); (try now destruct operand_ty);
+      repeat (step; cbn; try easy);
+      sauto lq: on rew: off.
   }
   { guard_instruction Bytecode.CastU16.
-    destruct_abstract_pop H_interpreter.
-    lib.step; cbn; [exact I|].
+    destruct_abstract_pop.
+    step; cbn; [exact I|].
     destruct_abstract_push.
-    destruct stack as [|operand stack]; cbn; [exact I|].
-    destruct operand; cbn; try exact I; (
-      repeat (lib.step; cbn; [|exact I]);
-      unfold IsInterpreterContextOfType.t, IsStackValueOfType.t; cbn;
-      sauto lq: on
-    ).
+    step; cbn; (try easy); (try now destruct operand_ty);
+      repeat (step; cbn; try easy);
+      sauto lq: on rew: off.
   }
   { guard_instruction Bytecode.CastU32.
-    destruct_abstract_pop H_interpreter.
-    lib.step; cbn; [exact I|].
+    destruct_abstract_pop.
+    step; cbn; [exact I|].
     destruct_abstract_push.
-    destruct stack as [|operand stack]; cbn; [exact I|].
-    destruct operand; cbn; try exact I; (
-      repeat (lib.step; cbn; [|exact I]);
-      unfold IsInterpreterContextOfType.t, IsStackValueOfType.t; cbn;
-      sauto lq: on
-    ).
+    step; cbn; (try easy); (try now destruct operand_ty);
+      repeat (step; cbn; try easy);
+      sauto lq: on rew: off.
   }
   { guard_instruction Bytecode.CastU64.
-    destruct_abstract_pop H_interpreter.
-    lib.step; cbn; [exact I|].
+    destruct_abstract_pop.
+    step; cbn; [exact I|].
     destruct_abstract_push.
-    destruct stack as [|operand stack]; cbn; [exact I|].
-    destruct operand; cbn; try exact I; (
-      repeat (lib.step; cbn; [|exact I]);
-      unfold IsInterpreterContextOfType.t, IsStackValueOfType.t; cbn;
-      sauto lq: on
-    ).
+    step; cbn; (try easy); (try now destruct operand_ty);
+      repeat (step; cbn; try easy);
+      sauto lq: on rew: off.
   }
   { guard_instruction Bytecode.CastU128.
-    destruct_abstract_pop H_interpreter.
-    lib.step; cbn; [exact I|].
+    destruct_abstract_pop.
+    step; cbn; [exact I|].
     destruct_abstract_push.
-    destruct stack as [|operand stack]; cbn; [exact I|].
-    destruct operand; cbn; try exact I; (
-      repeat (lib.step; cbn; [|exact I]);
-      unfold IsInterpreterContextOfType.t, IsStackValueOfType.t; cbn;
-      sauto lq: on
-    ).
+    step; cbn; (try easy); (try now destruct operand_ty);
+      repeat (step; cbn; try easy);
+      sauto lq: on rew: off.
   }
   { guard_instruction Bytecode.CastU256.
-    destruct_abstract_pop H_interpreter.
-    lib.step; cbn; [exact I|].
+    destruct_abstract_pop.
+    step; cbn; [exact I|].
     destruct_abstract_push.
-    destruct stack as [|operand stack]; cbn; [exact I|].
-    destruct operand; cbn; try exact I; (
-      repeat (lib.step; cbn; [|exact I]);
-      unfold IsInterpreterContextOfType.t, IsStackValueOfType.t; cbn;
-      (* U256 too big? sauto lq: on *)
-      admit
-    ).
+    step; cbn; (try easy); (try now destruct operand_ty);
+      repeat (step; cbn; try easy);
+      sauto lq: on rew: off.
   }
   { guard_instruction (Bytecode.LdConst t).
     admit.
   }
   { guard_instruction Bytecode.LdTrue.
     destruct_abstract_push.
-    lib.step; cbn; [|exact I].
-    unfold IsInterpreterContextOfType.t; cbn.
-    unfold IsStackValueOfType.t; cbn.
-    rewrite H_push.
-    hauto l: on.
+    step; cbn; [|exact I].
+    sauto lq: on.
   }
   { guard_instruction Bytecode.LdFalse.
     destruct_abstract_push.
-    lib.step; cbn; [|exact I].
-    unfold IsInterpreterContextOfType.t; cbn.
-    unfold IsStackValueOfType.t; cbn.
-    rewrite H_push.
-    hauto l: on.
+    step; cbn; [|exact I].
+    sauto lq: on.
   }
   { guard_instruction (Bytecode.CopyLoc z).
+    unfold_state_monad.
+    do 3 (step; cbn; try easy).
+    unfold TypeSafetyChecker.Impl_TypeSafetyChecker.local_at; cbn.
+    destruct_abstract_push.
     admit.
   }
   { guard_instruction (Bytecode.MoveLoc z).
+    unfold TypeSafetyChecker.Impl_TypeSafetyChecker.local_at; cbn.
     admit.
   }
   { guard_instruction (Bytecode.StLoc z).
@@ -371,11 +379,31 @@ Proof.
     admit.
   }
   { guard_instruction Bytecode.Add.
-    do 2 destruct_abstract_pop H_interpreter.
-    lib.step; cbn; [|exact I].
+    destruct_abstract_pop.
+    destruct_abstract_pop.
+    step; cbn; [|exact I].
     destruct_abstract_push.
-    destruct stack as [|operand1 stack]; cbn; [exact I|].
-    admit.
+    match goal with
+    | H : _ && _ = true |- _ => destruct (andb_prop _ _ H); clear H
+    end.
+    match goal with
+    | H : SignatureToken.t_beq ?x1 ?x2 = true |- _ =>
+      assert (SignatureToken.is_integer x2 = true); [
+        now replace x2 with x1 by now apply H_Eq
+      |];
+      clear H
+    end.
+    repeat match goal with
+    | H_value : _, H_ty : _ |- _ =>
+      pose proof (IsValueOfType.value_of_integer _ _ H_value H_ty);
+      clear H_ty
+    end.
+    step; cbn in *; try easy; (
+      step; cbn in *; try easy;
+      unfold IntegerValue.add_checked; cbn;
+      repeat (step; cbn; try easy);
+      sauto lq: on
+    ).
   }
   { guard_instruction Bytecode.Sub.
     admit.
@@ -940,4 +968,4 @@ Proof.
   { guard_instruction (Bytecode.VecSwap t).
     admit.
   }
-Admitted.
\ No newline at end of file
+Admitted.
diff --git a/CoqOfRust/move_sui/simulations/move_binary_format/file_format.v b/CoqOfRust/move_sui/simulations/move_binary_format/file_format.v
index d71aefd56..e97dff80b 100644
--- a/CoqOfRust/move_sui/simulations/move_binary_format/file_format.v
+++ b/CoqOfRust/move_sui/simulations/move_binary_format/file_format.v
@@ -522,6 +522,10 @@ Module SignatureToken.
 
   Module ImplEq.
     Global Instance I : Eq.Trait SignatureToken.t := { eqb := t_beq }.
+
+    Lemma I_is_valid : Eq.Valid.t (fun _ => True).
+    Proof.
+    Admitted.
   End ImplEq.
   (* 
   impl SignatureToken {
diff --git a/CoqOfRust/move_sui/simulations/move_bytecode_verifier/type_safety.v b/CoqOfRust/move_sui/simulations/move_bytecode_verifier/type_safety.v
index c733b7b3c..4e5003332 100644
--- a/CoqOfRust/move_sui/simulations/move_bytecode_verifier/type_safety.v
+++ b/CoqOfRust/move_sui/simulations/move_bytecode_verifier/type_safety.v
@@ -2090,7 +2090,7 @@ Definition verify_instr
         verifier.push(meter, ST::U256)?;
     }
     *)
-    | Bytecode.CastU16 => 
+    | Bytecode.CastU16 =>
       letS! operand :=
         liftS! TypeSafetyChecker.lens_self_stack AbstractStack.pop in
       letS! operand := return!toS! $ safe_unwrap_err operand in
@@ -2098,7 +2098,7 @@ Definition verify_instr
       then returnS! $ Result.Err $ TypeSafetyChecker.Impl_TypeSafetyChecker
         .error verifier StatusCode.INTEGER_OP_TYPE_MISMATCH_ERROR offset
       else TypeSafetyChecker.Impl_TypeSafetyChecker.push SignatureToken.U16
-    | Bytecode.CastU32 => 
+    | Bytecode.CastU32 =>
       letS! operand :=
         liftS! TypeSafetyChecker.lens_self_stack AbstractStack.pop in
       letS! operand := return!toS! $ safe_unwrap_err operand in
@@ -2106,14 +2106,14 @@ Definition verify_instr
       then returnS! $ Result.Err $ TypeSafetyChecker.Impl_TypeSafetyChecker
         .error verifier StatusCode.INTEGER_OP_TYPE_MISMATCH_ERROR offset
       else TypeSafetyChecker.Impl_TypeSafetyChecker.push SignatureToken.U32
-    | Bytecode.CastU256 => 
+    | Bytecode.CastU256 =>
       letS! operand :=
         liftS! TypeSafetyChecker.lens_self_stack AbstractStack.pop in
       letS! operand := return!toS! $ safe_unwrap_err operand in
       if negb $ SignatureToken.is_integer operand
       then returnS! $ Result.Err $ TypeSafetyChecker.Impl_TypeSafetyChecker
         .error verifier StatusCode.INTEGER_OP_TYPE_MISMATCH_ERROR offset
-      else TypeSafetyChecker.Impl_TypeSafetyChecker.push SignatureToken.U64
+      else TypeSafetyChecker.Impl_TypeSafetyChecker.push SignatureToken.U256
     end.
 
 (* 
diff --git a/CoqOfRust/simulations/M.v b/CoqOfRust/simulations/M.v
index c36a57d07..c54bc5340 100644
--- a/CoqOfRust/simulations/M.v
+++ b/CoqOfRust/simulations/M.v
@@ -416,4 +416,17 @@ Module Notations.
   Include LensNotations.
 
   Notation "f $ x" := (f x) (at level 60, right associativity, only parsing).
+
+  (** Convenient as the state monads hide the state variable which can be needed for reduction *)
+  Ltac unfold_state_monad :=
+    repeat (
+      unfold StatePanicResult.bind, StatePanic.bind, StatePanic.bind,
+        "returnS!",
+        "return!toS!", 
+        "liftS!", 
+        "liftS!of?",
+        "readS!", 
+        "return!toS!?";
+      cbn
+    ).
 End Notations.