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 930bc2f29..32e3f090c 100644
--- a/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
+++ b/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
@@ -10,6 +10,14 @@ Require Import move_sui.simulations.move_vm_types.values.values_impl.
 
 Import simulations.M.Notations.
 
+Module TypeSafetyChecker.
+  Module Valid.
+    Record t (x : TypeSafetyChecker.t) : Prop := {
+      stack : AbstractStack.Valid.t x.(TypeSafetyChecker.stack);
+    }.
+  End Valid.
+End TypeSafetyChecker.
+
 Module IsValueOfType.
   Definition t (value : Value.t) (typ : SignatureToken.t) : Prop :=
     match value, typ with
@@ -57,9 +65,14 @@ Ltac guard_instruction expected_instruction :=
   end.
 
 Ltac unfold_state_monad :=
-  unfold StatePanicResult.bind, StatePanic.bind, StatePanic.bind,
-    "return!toS!", "liftS!", "readS!";
-  cbn.
+  repeat (
+    unfold StatePanicResult.bind, StatePanic.bind, StatePanic.bind,
+      "return!toS!", 
+      "liftS!", 
+      "readS!", 
+      "return!toS!?";
+    cbn
+  ).
 
 Ltac destruct_abstract_push :=
   unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push;
@@ -164,6 +177,12 @@ Proof.
     rewrite H_push.
     hauto l: on.
   }
+  { guard_instruction (Bytecode.LdU16 z).
+    admit.
+  }
+  { guard_instruction (Bytecode.LdU32 z).
+    admit.
+  }
   { guard_instruction (Bytecode.LdU64 z).
     destruct_abstract_push.
     lib.step; cbn; [|exact I].
@@ -180,6 +199,9 @@ Proof.
     rewrite H_push.
     hauto l: on.
   }
+  { guard_instruction (Bytecode.LdU256 z).
+    admit.
+  }
   { guard_instruction Bytecode.CastU8.
     destruct_abstract_pop H_interpreter.
     lib.step; cbn; [exact I|].
@@ -191,6 +213,12 @@ Proof.
       sauto lq: on
     ).
   }
+  { guard_instruction Bytecode.CastU16.
+    admit.
+  }
+  { guard_instruction Bytecode.CastU32.
+    admit.
+  }
   { guard_instruction Bytecode.CastU64.
     destruct_abstract_pop H_interpreter.
     lib.step; cbn; [exact I|].
@@ -213,6 +241,9 @@ Proof.
       sauto lq: on
     ).
   }
+  { guard_instruction Bytecode.CastU256.
+    admit.
+  }
   { guard_instruction (Bytecode.LdConst t).
     admit.
   }
@@ -407,13 +438,82 @@ Proof.
   { guard_instruction (Bytecode.VecSwap t).
     admit.
   }
-  { guard_instruction (Bytecode.LdU16 z).
+Admitted.
+
+Lemma verify_instr_is_valid (instruction : Bytecode.t) (pc : Z) (type_safety_checker : TypeSafetyChecker.t)
+  (H_type_safety_checker : TypeSafetyChecker.Valid.t type_safety_checker) :
+  match verify_instr instruction pc type_safety_checker with
+  | Panic.Value (Result.Ok _, type_safety_checker') => TypeSafetyChecker.Valid.t type_safety_checker'
+  | _ => True
+  end.
+Proof.
+  destruct instruction eqn:H_instruction; cbn.
+  { guard_instruction Bytecode.Pop.
     admit.
   }
-  { guard_instruction (Bytecode.LdU32 z).
+  { guard_instruction Bytecode.Ret.
+    admit.
+  }
+  { guard_instruction (Bytecode.BrTrue z).
     admit.
   }
+  { guard_instruction (Bytecode.BrFalse z).
+    admit.
+  }
+  { guard_instruction (Bytecode.Branch z).
+    admit.
+  }
+  { guard_instruction (Bytecode.LdU8 z).
+    unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push.
+    with_strategy opaque [AbstractStack.push] unfold_state_monad.
+    pose proof (AbstractStack.push_is_valid SignatureToken.U8 type_safety_checker.(TypeSafetyChecker.stack)).
+    destruct AbstractStack.push as [[result stack']|]; cbn; [|trivial].
+    destruct result; cbn; [|trivial].
+    sauto q: on.
+  }
+  {
+    guard_instruction (Bytecode.LdU16 z).
+    unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push.
+    with_strategy opaque [AbstractStack.push] unfold_state_monad.
+    pose proof (AbstractStack.push_is_valid SignatureToken.U16 type_safety_checker.(TypeSafetyChecker.stack)).
+    destruct AbstractStack.push as [[result stack']|]; cbn; [|trivial].
+    destruct result; cbn; [|trivial].
+    sauto q: on.
+  }
+  { guard_instruction (Bytecode.LdU32 z).
+    unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push.
+    with_strategy opaque [AbstractStack.push] unfold_state_monad.
+    pose proof (AbstractStack.push_is_valid SignatureToken.U32 type_safety_checker.(TypeSafetyChecker.stack)).
+    destruct AbstractStack.push as [[result stack']|]; cbn; [|trivial].
+    destruct result; cbn; [|trivial].
+    sauto q: on.
+  }
+  { guard_instruction (Bytecode.LdU64 z).
+    unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push.
+    with_strategy opaque [AbstractStack.push] unfold_state_monad.
+    pose proof (AbstractStack.push_is_valid SignatureToken.U64 type_safety_checker.(TypeSafetyChecker.stack)).
+    destruct AbstractStack.push as [[result stack']|]; cbn; [|trivial].
+    destruct result; cbn; [|trivial].
+    sauto q: on.
+  }
+  { guard_instruction (Bytecode.LdU128 z).
+    unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push.
+    with_strategy opaque [AbstractStack.push] unfold_state_monad.
+    pose proof (AbstractStack.push_is_valid SignatureToken.U128 type_safety_checker.(TypeSafetyChecker.stack)).
+    destruct AbstractStack.push as [[result stack']|]; cbn; [|trivial].
+    destruct result; cbn; [|trivial].
+    sauto q: on.
+  }
   { guard_instruction (Bytecode.LdU256 z).
+    unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push.
+    with_strategy opaque [AbstractStack.push] unfold_state_monad.
+    pose proof (AbstractStack.push_is_valid SignatureToken.U256 type_safety_checker.(TypeSafetyChecker.stack)).
+    destruct AbstractStack.push as [[result stack']|]; cbn; [|trivial].
+    destruct result; cbn; [|trivial].
+    sauto q: on.
+  }
+  { guard_instruction Bytecode.CastU8.
+
     admit.
   }
   { guard_instruction Bytecode.CastU16.
@@ -422,7 +522,193 @@ Proof.
   { guard_instruction Bytecode.CastU32.
     admit.
   }
+  { guard_instruction Bytecode.CastU64.
+    admit.
+  }
+  { guard_instruction Bytecode.CastU128.
+    admit.
+  }
   { guard_instruction Bytecode.CastU256.
     admit.
   }
-Admitted.
+  { guard_instruction (Bytecode.LdConst t).
+    admit.
+  }
+  { guard_instruction Bytecode.LdTrue.
+    admit.
+  }
+  { guard_instruction Bytecode.LdFalse.
+    admit.
+  }
+  { guard_instruction (Bytecode.CopyLoc z).
+    admit.
+  }
+  { guard_instruction (Bytecode.MoveLoc z).
+    admit.
+  }
+  { guard_instruction (Bytecode.StLoc z).
+    admit.
+  }
+  { guard_instruction (Bytecode.Call t).
+    admit.
+  }
+  { guard_instruction (Bytecode.CallGeneric t).
+    admit.
+  }
+  { guard_instruction (Bytecode.Pack t).
+    admit.
+  }
+  { guard_instruction (Bytecode.PackGeneric t).
+    admit.
+  }
+  { guard_instruction (Bytecode.Unpack t).
+    admit.
+  }
+  { guard_instruction (Bytecode.UnpackGeneric t).
+    admit.
+  }
+  { guard_instruction Bytecode.ReadRef.
+    admit.
+  }
+  { guard_instruction Bytecode.WriteRef.
+    admit.
+  }
+  { guard_instruction Bytecode.FreezeRef.
+    admit.
+  }
+  { guard_instruction (Bytecode.MutBorrowLoc z).
+    admit.
+  }
+  { guard_instruction (Bytecode.ImmBorrowLoc z).
+    admit.
+  }
+  { guard_instruction (Bytecode.MutBorrowField t).
+    admit.
+  }
+  { guard_instruction (Bytecode.MutBorrowFieldGeneric t).
+    admit.
+  }
+  { guard_instruction (Bytecode.ImmBorrowField t).
+    admit.
+  }
+  { guard_instruction (Bytecode.ImmBorrowFieldGeneric t).
+    admit.
+  }
+  { guard_instruction (Bytecode.MutBorrowGlobalDeprecated t).
+    admit.
+  }
+  { guard_instruction (Bytecode.MutBorrowGlobalGenericDeprecated t).
+    admit.
+  }
+  { guard_instruction (Bytecode.ImmBorrowGlobalDeprecated t).
+    admit.
+  }
+  { guard_instruction (Bytecode.ImmBorrowGlobalGenericDeprecated t).
+    admit.
+  }
+  { guard_instruction Bytecode.Add.
+    admit.
+  }
+  { guard_instruction Bytecode.Sub.
+    admit.
+  }
+  { guard_instruction Bytecode.Mul.
+    admit.
+  }
+  { guard_instruction Bytecode.Mod.
+    admit.
+  }
+  { guard_instruction Bytecode.Div.
+    admit.
+  }
+  { guard_instruction Bytecode.BitOr.
+    admit.
+  }
+  { guard_instruction Bytecode.BitAnd.
+    admit.
+  }
+  { guard_instruction Bytecode.Xor.
+    admit.
+  }
+  { guard_instruction Bytecode.Or.
+    admit.
+  }
+  { guard_instruction Bytecode.And.
+    admit.
+  }
+  { guard_instruction Bytecode.Not.
+    admit.
+  }
+  { guard_instruction Bytecode.Eq.
+    admit.
+  }
+  { guard_instruction Bytecode.Neq.
+    admit.
+  }
+  { guard_instruction Bytecode.Lt.
+    admit.
+  }
+  { guard_instruction Bytecode.Gt.
+    admit.
+  }
+  { guard_instruction Bytecode.Le.
+    admit.
+  }
+  { guard_instruction Bytecode.Ge.
+    admit.
+  }
+  { guard_instruction Bytecode.Abort.
+    admit.
+  }
+  { guard_instruction Bytecode.Nop.
+    admit.
+  }
+  { guard_instruction (Bytecode.ExistsDeprecated t).
+    admit.
+  }
+  { guard_instruction (Bytecode.ExistsGenericDeprecated t).
+    admit.
+  }
+  { guard_instruction (Bytecode.MoveFromDeprecated t).
+    admit.
+  }
+  { guard_instruction (Bytecode.MoveFromGenericDeprecated t).
+    admit.
+  }
+  { guard_instruction (Bytecode.MoveToDeprecated t).
+    admit.
+  }
+  { guard_instruction (Bytecode.MoveToGenericDeprecated t).
+    admit.
+  }
+  { guard_instruction Bytecode.Shl.
+    admit.
+  }
+  { guard_instruction Bytecode.Shr.
+    admit.
+  }
+  { guard_instruction (Bytecode.VecPack t z).
+    admit.
+  }
+  { guard_instruction (Bytecode.VecLen t).
+    admit.
+  }
+  { guard_instruction (Bytecode.VecImmBorrow t).
+    admit.
+  }
+  { guard_instruction (Bytecode.VecMutBorrow t).
+    admit.
+  }
+  { guard_instruction (Bytecode.VecPushBack t).
+    admit.
+  }
+  { guard_instruction (Bytecode.VecPopBack t).
+    admit.
+  }
+  { guard_instruction (Bytecode.VecUnpack t z).
+    admit.
+  }
+  { guard_instruction (Bytecode.VecSwap t).
+    admit.
+  }
+Admitted.
\ No newline at end of file
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 9d304e52d..d71aefd56 100644
--- a/CoqOfRust/move_sui/simulations/move_binary_format/file_format.v
+++ b/CoqOfRust/move_sui/simulations/move_binary_format/file_format.v
@@ -844,11 +844,17 @@ Module Bytecode.
   | BrFalse (_ : Z)
   | Branch (_ : Z)
   | LdU8 (_ : Z)
+  | LdU16 (_ : Z)
+  | LdU32 (_ : Z)
   | LdU64 (_ : Z)
   | LdU128 (_ : Z)
+  | LdU256 (_ : Z)
   | CastU8
+  | CastU16
+  | CastU32
   | CastU64
   | CastU128
+  | CastU256
   | LdConst (_ : ConstantPoolIndex.t)
   | LdTrue
   | LdFalse
@@ -908,13 +914,7 @@ Module Bytecode.
   | VecPushBack (_ : SignatureIndex.t)
   | VecPopBack (_ : SignatureIndex.t)
   | VecUnpack (_ : SignatureIndex.t) (_ : Z)
-  | VecSwap (_ : SignatureIndex.t)
-  | LdU16 (_ : Z)
-  | LdU32 (_ : Z)
-  | LdU256 (_ : Z)
-  | CastU16
-  | CastU32
-  | CastU256.
+  | VecSwap (_ : SignatureIndex.t).
 
   Definition is_unconditional_branch (self : t) : bool :=
     match self with