From f7fc5e129199392f24d535f0929c86c9ed710c7c Mon Sep 17 00:00:00 2001
From: Guillaume Claret <dev@clarus.me>
Date: Thu, 19 Dec 2024 19:28:16 +0100
Subject: [PATCH 1/4] sui: set the undefined instruction as TODO in the
 interpreter

---
 .../move_bytecode_verifier/type_safety.v      | 233 ++++++---
 .../simulations/move_vm_runtime/interpreter.v | 450 ++++++++++--------
 .../move_vm_types/values/values_impl.v        |  14 +-
 3 files changed, 447 insertions(+), 250 deletions(-)

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 1216e0fbe..4cee962b3 100644
--- a/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
+++ b/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
@@ -34,27 +34,32 @@ Module IsValueOfType.
     | _, _ => False
     end.
 
-  Lemma value_of_bool (value : Value.t) (H_value : IsValueOfType.t value SignatureToken.Bool) :
+  Lemma value_of_bool (value : Value.t) (ty : SignatureToken.t)
+    (H_value : t value ty)
+    (* This is the form in which is appears in the proofs *)
+    (H_ty : ty = SignatureToken.Bool) :
     exists b, value = ValueImpl.Bool b.
   Proof.
-    destruct value; cbn; try contradiction.
+    destruct ty; cbn in *; try easy; clear H_ty.
+    destruct value; cbn in *; try easy.
     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.
+    exists (integer_value : IntegerValue.t),
+    value = IntegerValue.to_value_impl integer_value.
   Proof.
-    now destruct value, ty; cbn in *.
+    destruct value, ty; cbn in *; try easy;
+      (
+        (now eexists (IntegerValue.U8 _)) ||
+        (now eexists (IntegerValue.U16 _)) ||
+        (now eexists (IntegerValue.U32 _)) ||
+        (now eexists (IntegerValue.U64 _)) ||
+        (now eexists (IntegerValue.U128 _)) ||
+        (now eexists (IntegerValue.U256 _))
+      ).
   Qed.
 End IsValueOfType.
 
@@ -144,13 +149,54 @@ Ltac destruct_abstract_push :=
     destruct_post H_check_push
   end.
 
+Ltac destruct_initial_if :=
+  step; cbn; try exact I;
+  repeat match goal with
+  | H : _ && _ = true |- _ =>
+    destruct (andb_prop _ _ H);
+    clear H
+  end;
+  repeat rewrite Bool.negb_false_iff in *;
+  (* We put the equalities to a constant in a different form *)
+  repeat match goal with
+  | H_Eq : _, H : SignatureToken.t_beq ?x ?y = true |- _ =>
+    match y with
+    | SignatureToken.Bool => assert (x = y) by now apply H_Eq
+    end;
+    clear H
+  end;
+  (* For all the equalities on variables we duplicate *)
+  repeat match goal with
+  | H_Eq : _, H_ty_eq : SignatureToken.t_beq ?x1 ?x2 = true |- _ =>
+    assert (SignatureToken.is_integer x2 = true) by (
+      now replace x2 with x1 by now apply H_Eq
+    );
+    clear H_ty_eq
+  end;
+  (* We apply our known lemma for values of specific types *)
+  repeat (
+    match goal with
+    | H_value : _, H_ty : _ |- _ =>
+      destruct_post (IsValueOfType.value_of_bool _ _ H_value H_ty);
+      clear H_ty
+    end ||
+    match goal with
+    | H_value : _, H_ty : _ |- _ =>
+      destruct_post (IsValueOfType.value_of_integer _ _ H_value H_ty);
+      clear H_ty
+    end
+  );
+  cbn; trivial.
+
 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) :
+    (H_interpreter : IsInterpreterContextOfType.t locals interpreter type_safety_checker)
+    (* This lemma is not true for [Bytecode.Ret] *)
+    (H_not_Ret : instruction <> Bytecode.Ret) :
   let state := {|
     State.pc := pc;
     State.locals := locals;
@@ -191,27 +237,15 @@ Proof.
     repeat (step; cbn; try easy).
   }
   { guard_instruction Bytecode.Ret.
-    admit.
+    congruence.
   }
   { guard_instruction (Bytecode.BrTrue z).
     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 * by hauto lq: on; clear H_beq.
-    match goal with
-    | H : _ |- _ => destruct_post (IsValueOfType.value_of_bool _ H)
-    end; cbn.
-    hauto l: on.
+    destruct_initial_if.
   }
   { guard_instruction (Bytecode.BrFalse z).
     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 * by hauto lq: on; clear H_beq.
-    match goal with
-    | H : _ |- _ => destruct_post (IsValueOfType.value_of_bool _ H)
-    end; cbn.
-    hauto l: on.
+    destruct_initial_if.
   }
   { guard_instruction (Bytecode.Branch z).
     apply H_interpreter.
@@ -381,59 +415,112 @@ Proof.
   { guard_instruction Bytecode.Add.
     destruct_abstract_pop.
     destruct_abstract_pop.
-    step; cbn; [|exact I].
+    destruct_initial_if.
     destruct_abstract_push.
-    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;
+    destruct_all IntegerValue.t; cbn in *; try easy; (
       unfold IntegerValue.add_checked; cbn;
       repeat (step; cbn; try easy);
       sauto lq: on
     ).
   }
   { guard_instruction Bytecode.Sub.
-    admit.
+    destruct_abstract_pop.
+    destruct_abstract_pop.
+    destruct_initial_if.
+    destruct_abstract_push.
+    destruct_all IntegerValue.t; cbn in *; try easy; (
+      unfold IntegerValue.sub_checked; cbn;
+      repeat (step; cbn; try easy);
+      sauto lq: on
+    ).
   }
   { guard_instruction Bytecode.Mul.
-    admit.
+    destruct_abstract_pop.
+    destruct_abstract_pop.
+    destruct_initial_if.
+    destruct_abstract_push.
+    destruct_all IntegerValue.t; cbn in *; try easy; (
+      unfold IntegerValue.mul_checked; cbn;
+      repeat (step; cbn; try easy);
+      sauto lq: on
+    ).
   }
   { guard_instruction Bytecode.Mod.
-    admit.
+    destruct_abstract_pop.
+    destruct_abstract_pop.
+    destruct_initial_if.
+    destruct_abstract_push.
+    destruct_all IntegerValue.t; cbn in *; try easy; (
+      unfold IntegerValue.rem_checked; cbn;
+      repeat (step; cbn; try easy);
+      sauto lq: on
+    ).
   }
   { guard_instruction Bytecode.Div.
-    admit.
+    destruct_abstract_pop.
+    destruct_abstract_pop.
+    destruct_initial_if.
+    destruct_abstract_push.
+    destruct_all IntegerValue.t; cbn in *; try easy; (
+      unfold IntegerValue.div_checked; cbn;
+      repeat (step; cbn; try easy);
+      sauto lq: on
+    ).
   }
   { guard_instruction Bytecode.BitOr.
-    admit.
+    destruct_abstract_pop.
+    destruct_abstract_pop.
+    destruct_initial_if.
+    destruct_abstract_push.
+    destruct_all IntegerValue.t; cbn in *; try easy; (
+      unfold IntegerValue.bit_or; cbn;
+      repeat (step; cbn; try easy);
+      sauto lq: on
+    ).
   }
   { guard_instruction Bytecode.BitAnd.
-    admit.
+    destruct_abstract_pop.
+    destruct_abstract_pop.
+    destruct_initial_if.
+    destruct_abstract_push.
+    destruct_all IntegerValue.t; cbn in *; try easy; (
+      unfold IntegerValue.bit_and; cbn;
+      repeat (step; cbn; try easy);
+      sauto lq: on
+    ).
   }
   { guard_instruction Bytecode.Xor.
-    admit.
+    destruct_abstract_pop.
+    destruct_abstract_pop.
+    destruct_initial_if.
+    destruct_abstract_push.
+    destruct_all IntegerValue.t; cbn in *; try easy; (
+      unfold IntegerValue.bit_xor; cbn;
+      repeat (step; cbn; try easy);
+      sauto lq: on
+    ).
   }
   { guard_instruction Bytecode.Or.
-    admit.
+    destruct_abstract_pop.
+    destruct_abstract_pop.
+    destruct_initial_if.
+    destruct_abstract_push.
+    step; cbn; try easy.
+    hauto l: on.
   }
   { guard_instruction Bytecode.And.
-    admit.
+    destruct_abstract_pop.
+    destruct_abstract_pop.
+    destruct_initial_if.
+    destruct_abstract_push.
+    step; cbn; try easy.
+    hauto l: on.
   }
   { guard_instruction Bytecode.Not.
-    admit.
+    destruct_abstract_pop.
+    destruct_initial_if.
+    destruct_abstract_push.
+    hauto l: on.
   }
   { guard_instruction Bytecode.Eq.
     admit.
@@ -442,22 +529,46 @@ Proof.
     admit.
   }
   { guard_instruction Bytecode.Lt.
-    admit.
+    destruct_abstract_pop.
+    destruct_abstract_pop.
+    destruct_initial_if.
+    destruct_abstract_push.
+    destruct_all IntegerValue.t; cbn in *; try easy;
+      repeat (step; cbn; try easy);
+      sauto lq: on.
   }
   { guard_instruction Bytecode.Gt.
-    admit.
+    destruct_abstract_pop.
+    destruct_abstract_pop.
+    destruct_initial_if.
+    destruct_abstract_push.
+    destruct_all IntegerValue.t; cbn in *; try easy;
+      repeat (step; cbn; try easy);
+      sauto lq: on.
   }
   { guard_instruction Bytecode.Le.
-    admit.
+    destruct_abstract_pop.
+    destruct_abstract_pop.
+    destruct_initial_if.
+    destruct_abstract_push.
+    destruct_all IntegerValue.t; cbn in *; try easy;
+      repeat (step; cbn; try easy);
+      sauto lq: on.
   }
   { guard_instruction Bytecode.Ge.
-    admit.
+    destruct_abstract_pop.
+    destruct_abstract_pop.
+    destruct_initial_if.
+    destruct_abstract_push.
+    destruct_all IntegerValue.t; cbn in *; try easy;
+      repeat (step; cbn; try easy);
+      sauto lq: on.
   }
   { guard_instruction Bytecode.Abort.
     admit.
   }
   { guard_instruction Bytecode.Nop.
-    admit.
+    assumption.
   }
   { guard_instruction (Bytecode.ExistsDeprecated t).
     admit.
diff --git a/CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v b/CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v
index 09e76200f..97e54e161 100644
--- a/CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v
+++ b/CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v
@@ -384,6 +384,24 @@ Module Impl_Interpreter.
       | IntegerValue.U256 x => return? $ ValueImpl.U256 x
       end
     ).
+
+  (*
+  /// Perform a binary operation for boolean values.
+  fn binop_bool<F, T>(&mut self, f: F) -> PartialVMResult<()>
+  where
+      Value: VMValueCast<T>,
+      F: FnOnce(T, T) -> PartialVMResult<bool>,
+  {
+      self.binop(|lhs, rhs| Ok(Value::bool(f(lhs, rhs)?)))
+  }
+  *)
+  Definition binop_bool {T : Set} `{VMValueCast.Trait Value.t T}
+    (f : T -> T -> PartialVMResult.t bool) :
+    MS! Interpreter.t (PartialVMResult.t unit) :=
+    binop (fun lhs rhs =>
+      let? result := f lhs rhs in
+      return? $ ValueImpl.Bool result
+    ).
 End Impl_Interpreter.
 
 (* 
@@ -403,187 +421,6 @@ Module Frame.
   }.
 End Frame.
 
-(* 
-    fn execute_instruction(
-        pc: &mut u16,
-        locals: &mut Locals,
-        ty_args: &[Type],
-        function: &Arc<Function>,
-        resolver: &Resolver,
-        interpreter: &mut Interpreter,
-        gas_meter: &mut impl GasMeter,
-        instruction: &Bytecode,
-    ) -> PartialVMResult<InstrRet> {
-        use SimpleInstruction as S;
-
-        match instruction {
-            Bytecode::Shl => {
-                gas_meter.charge_simple_instr(S::Shl)?;
-                let rhs = interpreter.operand_stack.pop_as::<u8>()?;
-                let lhs = interpreter.operand_stack.pop_as::<IntegerValue>()?;
-                interpreter
-                    .operand_stack
-                    .push(lhs.shl_checked(rhs)?.into_value())?;
-            }
-            Bytecode::Shr => {
-                gas_meter.charge_simple_instr(S::Shr)?;
-                let rhs = interpreter.operand_stack.pop_as::<u8>()?;
-                let lhs = interpreter.operand_stack.pop_as::<IntegerValue>()?;
-                interpreter
-                    .operand_stack
-                    .push(lhs.shr_checked(rhs)?.into_value())?;
-            }
-            Bytecode::Or => {
-                gas_meter.charge_simple_instr(S::Or)?;
-                interpreter.binop_bool(|l, r| Ok(l || r))?
-            }
-            Bytecode::And => {
-                gas_meter.charge_simple_instr(S::And)?;
-                interpreter.binop_bool(|l, r| Ok(l && r))?
-            }
-            Bytecode::Lt => {
-                gas_meter.charge_simple_instr(S::Lt)?;
-                interpreter.binop_bool(IntegerValue::lt)?
-            }
-            Bytecode::Gt => {
-                gas_meter.charge_simple_instr(S::Gt)?;
-                interpreter.binop_bool(IntegerValue::gt)?
-            }
-            Bytecode::Le => {
-                gas_meter.charge_simple_instr(S::Le)?;
-                interpreter.binop_bool(IntegerValue::le)?
-            }
-            Bytecode::Ge => {
-                gas_meter.charge_simple_instr(S::Ge)?;
-                interpreter.binop_bool(IntegerValue::ge)?
-            }
-            Bytecode::Abort => {
-                gas_meter.charge_simple_instr(S::Abort)?;
-                let error_code = interpreter.operand_stack.pop_as::<u64>()?;
-                let error = PartialVMError::new(StatusCode::ABORTED)
-                    .with_sub_status(error_code)
-                    .with_message(format!("{} at offset {}", function.pretty_string(), *pc,));
-                return Err(error);
-            }
-            Bytecode::Eq => {
-                let lhs = interpreter.operand_stack.pop()?;
-                let rhs = interpreter.operand_stack.pop()?;
-                gas_meter.charge_eq(&lhs, &rhs)?;
-                interpreter
-                    .operand_stack
-                    .push(Value::bool(lhs.equals(&rhs)?))?;
-            }
-            Bytecode::Neq => {
-                let lhs = interpreter.operand_stack.pop()?;
-                let rhs = interpreter.operand_stack.pop()?;
-                gas_meter.charge_neq(&lhs, &rhs)?;
-                interpreter
-                    .operand_stack
-                    .push(Value::bool(!lhs.equals(&rhs)?))?;
-            }
-            Bytecode::MutBorrowGlobalDeprecated(_)
-            | Bytecode::ImmBorrowGlobalDeprecated(_)
-            | Bytecode::MutBorrowGlobalGenericDeprecated(_)
-            | Bytecode::ImmBorrowGlobalGenericDeprecated(_)
-            | Bytecode::ExistsDeprecated(_)
-            | Bytecode::ExistsGenericDeprecated(_)
-            | Bytecode::MoveFromDeprecated(_)
-            | Bytecode::MoveFromGenericDeprecated(_)
-            | Bytecode::MoveToDeprecated(_)
-            | Bytecode::MoveToGenericDeprecated(_) => {
-                unreachable!("Global bytecodes deprecated")
-            }
-            Bytecode::FreezeRef => {
-                gas_meter.charge_simple_instr(S::FreezeRef)?;
-                // FreezeRef should just be a null op as we don't distinguish between mut
-                // and immut ref at runtime.
-            }
-            Bytecode::Not => {
-                gas_meter.charge_simple_instr(S::Not)?;
-                let value = !interpreter.operand_stack.pop_as::<bool>()?;
-                interpreter.operand_stack.push(Value::bool(value))?;
-            }
-            Bytecode::Nop => {
-                gas_meter.charge_simple_instr(S::Nop)?;
-            }
-            Bytecode::VecPack(si, num) => {
-                let ty = resolver.instantiate_single_type(*si, ty_args)?; //*)
-                Self::check_depth_of_type(resolver, &ty)?;
-                gas_meter.charge_vec_pack(
-                    make_ty!(&ty),
-                    interpreter.operand_stack.last_n(*num as usize)?, //*)
-                )?;
-                let elements = interpreter.operand_stack.popn(*num as u16)?; //*)
-                let value = Vector::pack(&ty, elements)?;
-                interpreter.operand_stack.push(value)?;
-            }
-            Bytecode::VecLen(si) => {
-                let vec_ref = interpreter.operand_stack.pop_as::<VectorRef>()?;
-                let ty = &resolver.instantiate_single_type(*si, ty_args)?; //*)
-                gas_meter.charge_vec_len(TypeWithLoader {
-                    ty,
-                    loader: resolver.loader(),
-                })?;
-                let value = vec_ref.len(ty)?;
-                interpreter.operand_stack.push(value)?;
-            }
-            Bytecode::VecImmBorrow(si) => {
-                let idx = interpreter.operand_stack.pop_as::<u64>()? as usize;
-                let vec_ref = interpreter.operand_stack.pop_as::<VectorRef>()?;
-                let ty = resolver.instantiate_single_type(*si, ty_args)?; //*)
-                let res = vec_ref.borrow_elem(idx, &ty);
-                gas_meter.charge_vec_borrow(false, make_ty!(&ty), res.is_ok())?;
-                interpreter.operand_stack.push(res?)?;
-            }
-            Bytecode::VecMutBorrow(si) => {
-                let idx = interpreter.operand_stack.pop_as::<u64>()? as usize;
-                let vec_ref = interpreter.operand_stack.pop_as::<VectorRef>()?;
-                let ty = &resolver.instantiate_single_type(*si, ty_args)?; //*)
-                let res = vec_ref.borrow_elem(idx, ty);
-                gas_meter.charge_vec_borrow(true, make_ty!(ty), res.is_ok())?;
-                interpreter.operand_stack.push(res?)?;
-            }
-            Bytecode::VecPushBack(si) => {
-                let elem = interpreter.operand_stack.pop()?;
-                let vec_ref = interpreter.operand_stack.pop_as::<VectorRef>()?;
-                let ty = &resolver.instantiate_single_type(*si, ty_args)?; //*)
-                gas_meter.charge_vec_push_back(make_ty!(ty), &elem)?;
-                vec_ref.push_back(elem, ty, interpreter.runtime_limits_config().vector_len_max)?;
-            }
-            Bytecode::VecPopBack(si) => {
-                let vec_ref = interpreter.operand_stack.pop_as::<VectorRef>()?;
-                let ty = &resolver.instantiate_single_type(*si, ty_args)?; //*)
-                let res = vec_ref.pop(ty);
-                gas_meter.charge_vec_pop_back(make_ty!(ty), res.as_ref().ok())?;
-                interpreter.operand_stack.push(res?)?;
-            }
-            Bytecode::VecUnpack(si, num) => {
-                let vec_val = interpreter.operand_stack.pop_as::<Vector>()?;
-                let ty = &resolver.instantiate_single_type(*si, ty_args)?; //*)
-                gas_meter.charge_vec_unpack(
-                    make_ty!(ty),
-                    NumArgs::new(*num), //*)
-                    vec_val.elem_views(),
-                )?;
-                let elements = vec_val.unpack(ty, *num)?;
-                for value in elements {
-                    interpreter.operand_stack.push(value)?;
-                }
-            }
-            Bytecode::VecSwap(si) => {
-                let idx2 = interpreter.operand_stack.pop_as::<u64>()? as usize;
-                let idx1 = interpreter.operand_stack.pop_as::<u64>()? as usize;
-                let vec_ref = interpreter.operand_stack.pop_as::<VectorRef>()?;
-                let ty = &resolver.instantiate_single_type(*si, ty_args)?; //*)
-                gas_meter.charge_vec_swap(make_ty!(ty))?;
-                vec_ref.swap(idx1, idx2, ty)?;
-            }
-        }
-
-        Ok(InstrRet::Ok)
-    }
-*)
-
 (* NOTE: State designed for `execute_instruction` *)
 Module State.
   Record t : Set := {
@@ -610,6 +447,8 @@ Module State.
   End Lens.
 End State.
 
+Axiom execute_instruction_TODO : MS! State.t (PartialVMResult.t InstrRet.t).
+
 (* NOTE: this function is of `impl Frame` (but doesn't involve `Frame` item?) *)
 Definition execute_instruction
   (ty_args : list _Type.t)
@@ -768,7 +607,7 @@ Definition execute_instruction
   }
   *)
   (* NOTE: paused from investigation *)
-  | Bytecode.LdConst idx => returnS! $ Result.Ok InstrRet.Ok
+  | Bytecode.LdConst idx => execute_instruction_TODO
     (* let constant := Resolver.Impl_Resolver.constant_at resolver idx in
     (* TODO: 
       - resolve mutual dependency issue 
@@ -898,7 +737,7 @@ Definition execute_instruction
   }
   *)
   (* NOTE: paused from investigation: mutual dependency issue for `borrow_loc` *)
-  | Bytecode.MutBorrowLoc idx => returnS! $ Result.Ok InstrRet.Ok
+  | Bytecode.MutBorrowLoc idx | Bytecode.ImmBorrowLoc idx=> execute_instruction_TODO
 
   (*
   Bytecode::ImmBorrowField(fh_idx) | Bytecode::MutBorrowField(fh_idx) => {
@@ -916,7 +755,7 @@ Definition execute_instruction
   }
   *)
   (* NOTE: paused for mutual dependency issue *)
-  | Bytecode.ImmBorrowField fh_idx => 
+  | Bytecode.ImmBorrowField fh_idx | Bytecode.MutBorrowField fh_idx =>
     letS!? reference := liftS! State.Lens.interpreter (
       (* NOTE: Notice that since we identify the instance by the `ValueImpl`
       item, here we have to apply the `StructRef` instance indirectly *)
@@ -945,7 +784,8 @@ Definition execute_instruction
   }
   *)
   (* NOTE: paused for mutual dependency issue *)
-  | Bytecode.ImmBorrowFieldGeneric fi_idx => returnS! $ Result.Ok InstrRet.Ok
+  | Bytecode.ImmBorrowFieldGeneric fi_idx | Bytecode.MutBorrowFieldGeneric fi_idx =>
+    execute_instruction_TODO
 
   (* 
   Bytecode::Pack(sd_idx) => {
@@ -1276,6 +1116,242 @@ Definition execute_instruction
     letS!? _ := liftS! State.Lens.interpreter (
       Impl_Interpreter.binop_int IntegerValue.bit_xor) in
     returnS! $ Result.Ok InstrRet.Ok
-
-  | _ => returnS! $ Result.Ok InstrRet.Ok
+  (*
+  Bytecode::Shl => {
+    gas_meter.charge_simple_instr(S::Shl)?;
+    let rhs = interpreter.operand_stack.pop_as::<u8>()?;
+    let lhs = interpreter.operand_stack.pop_as::<IntegerValue>()?;
+    interpreter
+        .operand_stack
+        .push(lhs.shl_checked(rhs)?.into_value())?;
+  }
+  *)
+  | Bytecode.Shl =>
+    execute_instruction_TODO
+  (*
+  Bytecode::Shr => {
+      gas_meter.charge_simple_instr(S::Shr)?;
+      let rhs = interpreter.operand_stack.pop_as::<u8>()?;
+      let lhs = interpreter.operand_stack.pop_as::<IntegerValue>()?;
+      interpreter
+          .operand_stack
+          .push(lhs.shr_checked(rhs)?.into_value())?;
+  }
+  *)
+  | Bytecode.Shr =>
+    execute_instruction_TODO
+  (*
+  Bytecode::Or => {
+      gas_meter.charge_simple_instr(S::Or)?;
+      interpreter.binop_bool(|l, r| Ok(l || r))?
+  }
+  *)
+  | Bytecode.Or =>
+    letS!? _ := liftS! State.Lens.interpreter (
+      Impl_Interpreter.binop_bool (fun l r => Result.Ok (l || r))) in
+    returnS! $ Result.Ok InstrRet.Ok
+  (*
+  Bytecode::And => {
+      gas_meter.charge_simple_instr(S::And)?;
+      interpreter.binop_bool(|l, r| Ok(l && r))?
+  }
+  *)
+  | Bytecode.And =>
+    letS!? _ := liftS! State.Lens.interpreter (
+      Impl_Interpreter.binop_bool (fun l r => Result.Ok (l && r))) in
+    returnS! $ Result.Ok InstrRet.Ok
+  (*
+  Bytecode::Lt => {
+      gas_meter.charge_simple_instr(S::Lt)?;
+      interpreter.binop_bool(IntegerValue::lt)?
+  }
+  *)
+  | Bytecode.Lt =>
+    letS!? _ := liftS! State.Lens.interpreter (
+      Impl_Interpreter.binop_bool IntegerValue.lt) in
+    returnS! $ Result.Ok InstrRet.Ok
+  (*
+  Bytecode::Gt => {
+      gas_meter.charge_simple_instr(S::Gt)?;
+      interpreter.binop_bool(IntegerValue::gt)?
+  }
+  *)
+  | Bytecode.Gt =>
+    letS!? _ := liftS! State.Lens.interpreter (
+      Impl_Interpreter.binop_bool IntegerValue.gt) in
+    returnS! $ Result.Ok InstrRet.Ok
+  (*
+  Bytecode::Le => {
+      gas_meter.charge_simple_instr(S::Le)?;
+      interpreter.binop_bool(IntegerValue::le)?
+  }
+  *)
+  | Bytecode.Le =>
+    letS!? _ := liftS! State.Lens.interpreter (
+      Impl_Interpreter.binop_bool IntegerValue.le) in
+    returnS! $ Result.Ok InstrRet.Ok
+  (*
+  Bytecode::Ge => {
+      gas_meter.charge_simple_instr(S::Ge)?;
+      interpreter.binop_bool(IntegerValue::ge)?
+  }
+  *)
+  | Bytecode.Ge =>
+    letS!? _ := liftS! State.Lens.interpreter (
+      Impl_Interpreter.binop_bool IntegerValue.ge) in
+    returnS! $ Result.Ok InstrRet.Ok
+  (* Bytecode::Abort => {
+      gas_meter.charge_simple_instr(S::Abort)?;
+      let error_code = interpreter.operand_stack.pop_as::<u64>()?;
+      let error = PartialVMError::new(StatusCode::ABORTED)
+          .with_sub_status(error_code)
+          .with_message(format!("{} at offset {}", function.pretty_string(), *pc,));
+      return Err(error);
+  } *)
+  | Bytecode.Abort =>
+    execute_instruction_TODO
+  (* Bytecode::Eq => {
+      let lhs = interpreter.operand_stack.pop()?;
+      let rhs = interpreter.operand_stack.pop()?;
+      gas_meter.charge_eq(&lhs, &rhs)?;
+      interpreter
+          .operand_stack
+          .push(Value::bool(lhs.equals(&rhs)?))?;
+  } *)
+  | Bytecode.Eq => execute_instruction_TODO
+  (* Bytecode::Neq => {
+      let lhs = interpreter.operand_stack.pop()?;
+      let rhs = interpreter.operand_stack.pop()?;
+      gas_meter.charge_neq(&lhs, &rhs)?;
+      interpreter
+          .operand_stack
+          .push(Value::bool(!lhs.equals(&rhs)?))?;
+  } *)
+  | Bytecode.Neq => execute_instruction_TODO
+  (* Bytecode::MutBorrowGlobalDeprecated(_)
+  | Bytecode::ImmBorrowGlobalDeprecated(_)
+  | Bytecode::MutBorrowGlobalGenericDeprecated(_)
+  | Bytecode::ImmBorrowGlobalGenericDeprecated(_)
+  | Bytecode::ExistsDeprecated(_)
+  | Bytecode::ExistsGenericDeprecated(_)
+  | Bytecode::MoveFromDeprecated(_)
+  | Bytecode::MoveFromGenericDeprecated(_)
+  | Bytecode::MoveToDeprecated(_)
+  | Bytecode::MoveToGenericDeprecated(_) => {
+      unreachable!("Global bytecodes deprecated")
+  } *)
+  | Bytecode.MutBorrowGlobalDeprecated _
+  | Bytecode.ImmBorrowGlobalDeprecated _
+  | Bytecode.MutBorrowGlobalGenericDeprecated _
+  | Bytecode.ImmBorrowGlobalGenericDeprecated _
+  | Bytecode.ExistsDeprecated _
+  | Bytecode.ExistsGenericDeprecated _
+  | Bytecode.MoveFromDeprecated _
+  | Bytecode.MoveFromGenericDeprecated _
+  | Bytecode.MoveToDeprecated _
+  | Bytecode.MoveToGenericDeprecated _ => 
+    panicS! "Global bytecodes deprecated"
+  (* Bytecode::FreezeRef => {
+      gas_meter.charge_simple_instr(S::FreezeRef)?;
+      // FreezeRef should just be a null op as we don't distinguish between mut
+      // and immut ref at runtime.
+  } *)
+  | Bytecode.FreezeRef => 
+    returnS! $ Result.Ok InstrRet.Ok
+  (* Bytecode::Not => {
+      gas_meter.charge_simple_instr(S::Not)?;
+      let value = !interpreter.operand_stack.pop_as::<bool>()?;
+      interpreter.operand_stack.push(Value::bool(value))?;
+  } *)
+  | Bytecode.Not => 
+    letS!? value := liftS! State.Lens.interpreter (
+      liftS! Interpreter.Lens.operand_stack $ Stack.Impl_Stack.pop_as bool) in
+    let value := negb value in
+    letS!? _ := liftS! State.Lens.interpreter (
+      liftS! Interpreter.Lens.operand_stack $ Stack.Impl_Stack.push $ ValueImpl.Bool value) in
+    returnS! $ Result.Ok InstrRet.Ok
+  (* Bytecode::Nop => {
+      gas_meter.charge_simple_instr(S::Nop)?;
+  } *)
+   | Bytecode.Nop => returnS! $ Result.Ok InstrRet.Ok
+  (* Bytecode::VecPack(si, num) => {
+      let ty = resolver.instantiate_single_type(*si, ty_args)?; //*)
+      Self::check_depth_of_type(resolver, &ty)?;
+      gas_meter.charge_vec_pack(
+          make_ty!(&ty),
+          interpreter.operand_stack.last_n(*num as usize)?, //*)
+      )?;
+      let elements = interpreter.operand_stack.popn(*num as u16)?; //*)
+      let value = Vector::pack(&ty, elements)?;
+      interpreter.operand_stack.push(value)?;
+  } *)
+  | Bytecode.VecPack _ _ => execute_instruction_TODO
+  (* Bytecode::VecLen(si) => {
+      let vec_ref = interpreter.operand_stack.pop_as::<VectorRef>()?;
+      let ty = &resolver.instantiate_single_type(*si, ty_args)?; //*)
+      gas_meter.charge_vec_len(TypeWithLoader {
+          ty,
+          loader: resolver.loader(),
+      })?;
+      let value = vec_ref.len(ty)?;
+      interpreter.operand_stack.push(value)?;
+  } *)
+  | Bytecode.VecLen _ => execute_instruction_TODO
+  (* Bytecode::VecImmBorrow(si) => {
+      let idx = interpreter.operand_stack.pop_as::<u64>()? as usize;
+      let vec_ref = interpreter.operand_stack.pop_as::<VectorRef>()?;
+      let ty = resolver.instantiate_single_type(*si, ty_args)?; //*)
+      let res = vec_ref.borrow_elem(idx, &ty);
+      gas_meter.charge_vec_borrow(false, make_ty!(&ty), res.is_ok())?;
+      interpreter.operand_stack.push(res?)?;
+  } *)
+  | Bytecode.VecImmBorrow _ => execute_instruction_TODO
+  (* Bytecode::VecMutBorrow(si) => {
+      let idx = interpreter.operand_stack.pop_as::<u64>()? as usize;
+      let vec_ref = interpreter.operand_stack.pop_as::<VectorRef>()?;
+      let ty = &resolver.instantiate_single_type(*si, ty_args)?; //*)
+      let res = vec_ref.borrow_elem(idx, ty);
+      gas_meter.charge_vec_borrow(true, make_ty!(ty), res.is_ok())?;
+      interpreter.operand_stack.push(res?)?;
+  } *)
+  | Bytecode.VecMutBorrow _ => execute_instruction_TODO
+  (* Bytecode::VecPushBack(si) => {
+      let elem = interpreter.operand_stack.pop()?;
+      let vec_ref = interpreter.operand_stack.pop_as::<VectorRef>()?;
+      let ty = &resolver.instantiate_single_type(*si, ty_args)?; //*)
+      gas_meter.charge_vec_push_back(make_ty!(ty), &elem)?;
+      vec_ref.push_back(elem, ty, interpreter.runtime_limits_config().vector_len_max)?;
+  } *)
+  | Bytecode.VecPushBack _ => execute_instruction_TODO
+  (* Bytecode::VecPopBack(si) => {
+      let vec_ref = interpreter.operand_stack.pop_as::<VectorRef>()?;
+      let ty = &resolver.instantiate_single_type(*si, ty_args)?; //*)
+      let res = vec_ref.pop(ty);
+      gas_meter.charge_vec_pop_back(make_ty!(ty), res.as_ref().ok())?;
+      interpreter.operand_stack.push(res?)?;
+  } *)
+  | Bytecode.VecPopBack _ => execute_instruction_TODO
+  (* Bytecode::VecUnpack(si, num) => {
+      let vec_val = interpreter.operand_stack.pop_as::<Vector>()?;
+      let ty = &resolver.instantiate_single_type(*si, ty_args)?; //*)
+      gas_meter.charge_vec_unpack(
+          make_ty!(ty),
+          NumArgs::new(*num), //*)
+          vec_val.elem_views(),
+      )?;
+      let elements = vec_val.unpack(ty, *num)?;
+      for value in elements {
+          interpreter.operand_stack.push(value)?;
+      }
+  } *)
+  | Bytecode.VecUnpack _ _ => execute_instruction_TODO
+  (* Bytecode::VecSwap(si) => {
+      let idx2 = interpreter.operand_stack.pop_as::<u64>()? as usize;
+      let idx1 = interpreter.operand_stack.pop_as::<u64>()? as usize;
+      let vec_ref = interpreter.operand_stack.pop_as::<VectorRef>()?;
+      let ty = &resolver.instantiate_single_type(*si, ty_args)?; //*)
+      gas_meter.charge_vec_swap(make_ty!(ty))?;
+      vec_ref.swap(idx1, idx2, ty)?;
+  } *)
+  | Bytecode.VecSwap _ => execute_instruction_TODO
   end.
diff --git a/CoqOfRust/move_sui/simulations/move_vm_types/values/values_impl.v b/CoqOfRust/move_sui/simulations/move_vm_types/values/values_impl.v
index a507a93fc..2cde27cc3 100644
--- a/CoqOfRust/move_sui/simulations/move_vm_types/values/values_impl.v
+++ b/CoqOfRust/move_sui/simulations/move_vm_types/values/values_impl.v
@@ -978,7 +978,6 @@ Module Impl_Locals.
 End Impl_Locals.
 
 Module IntegerValue.
-
   Inductive t : Type :=
   | U8 : Z -> t
   | U16 : Z -> t
@@ -988,6 +987,17 @@ Module IntegerValue.
   | U256 : Z -> t
   .
 
+  (** This function is not in the original Rust code but is convenient for the proofs. *)
+  Definition to_value_impl (self : t) : ValueImpl.t :=
+    match self with
+    | U8 x => ValueImpl.U8 x
+    | U16 x => ValueImpl.U16 x
+    | U32 x => ValueImpl.U32 x
+    | U64 x => ValueImpl.U64 x
+    | U128 x => ValueImpl.U128 x
+    | U256 x => ValueImpl.U256 x
+    end.
+
   Definition checked_add (a : IntegerValue.t) (b : IntegerValue.t) : option IntegerValue.t :=
     match a, b with
     | IntegerValue.U8 l, IntegerValue.U8 r =>
@@ -1103,7 +1113,7 @@ Module IntegerValue.
       else Some (IntegerValue.U256 (l / r))
     | _, _ => None
     end.
-  
+
   Definition checked_rem (a : IntegerValue.t) (b : IntegerValue.t) : option IntegerValue.t :=
   match a, b with
   | IntegerValue.U8 l, IntegerValue.U8 r =>

From c88abe9b44ab529f6c2d3ce901fd417e371111fe Mon Sep 17 00:00:00 2001
From: Guillaume Claret <dev@clarus.me>
Date: Thu, 19 Dec 2024 22:28:40 +0100
Subject: [PATCH 2/4] sui: verify Bytecode.LdConst

---
 CoqOfRust/lib/proofs/lib.v                    |  13 ++
 .../proofs/move_binary_format/file_format.v   | 122 ++++++++++--------
 .../move_bytecode_verifier/type_safety.v      |  69 +++++-----
 .../proofs/move_vm_types/values/values_impl.v |  22 ++++
 .../simulations/move_vm_runtime/interpreter.v |  26 ++--
 .../move_vm_types/values/values_impl.v        |  19 ++-
 6 files changed, 160 insertions(+), 111 deletions(-)
 create mode 100644 CoqOfRust/move_sui/proofs/move_vm_types/values/values_impl.v

diff --git a/CoqOfRust/lib/proofs/lib.v b/CoqOfRust/lib/proofs/lib.v
index 4e53506cb..82bb5adf0 100644
--- a/CoqOfRust/lib/proofs/lib.v
+++ b/CoqOfRust/lib/proofs/lib.v
@@ -99,3 +99,16 @@ Module BinOp.
     Qed.
   End Error.
 End BinOp.
+
+Module List.
+  Lemma Forall_nth_error {A : Set} (P : A -> Prop) (l : list A) (n : nat)
+      (H_l : List.Forall P l) :
+    match List.nth_error l n with
+    | Some x => P x
+    | None => True
+    end.
+  Proof.
+    generalize dependent n.
+    induction H_l; intros; destruct n; cbn; sfirstorder.
+  Qed.
+End List.
diff --git a/CoqOfRust/move_sui/proofs/move_binary_format/file_format.v b/CoqOfRust/move_sui/proofs/move_binary_format/file_format.v
index 3131db4d2..42c8f3f42 100644
--- a/CoqOfRust/move_sui/proofs/move_binary_format/file_format.v
+++ b/CoqOfRust/move_sui/proofs/move_binary_format/file_format.v
@@ -1,9 +1,10 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.simulations.M.
-
+Require Import CoqOfRust.lib.proofs.lib.
 Require Import move_sui.simulations.move_binary_format.file_format.
 Require Import move_sui.simulations.move_binary_format.file_format_index.
-Require Import CoqOfRust.lib.proofs.lib.
+Require Import move_sui.simulations.move_vm_types.values.values_impl.
+Require Import move_sui.proofs.move_vm_types.values.values_impl.
 
 Module SignatureToken.
   Lemma t_beq_is_valid (x y : SignatureToken.t) :
@@ -13,95 +14,85 @@ Module SignatureToken.
 End SignatureToken.
 
 Module CompiledModule.
-  (*
-  Definition field_handle_at (self : t) (idx : FieldHandleIndex.t) : M! FieldHandle.t :=
-    let idx := idx.(FieldHandleIndex.a0) in
-    Option.expect
-      (List.nth_error self.(field_handles) (Z.to_nat idx))
-      "field_handle_at index error".
-      *)
-
-
   Lemma field_handle_at_is_valid (self : CompiledModule.t) (idx : FieldHandleIndex.t) :
-  match CompiledModule.field_handle_at self idx with
-  | Panic.Value _ => True
-  | Panic.Panic _ => True
-  end.
+    match CompiledModule.field_handle_at self idx with
+    | Panic.Value _ => True
+    | Panic.Panic _ => True
+    end.
   Proof.
   Admitted.
 
   Lemma struct_instantiation_at_is_valid (self : CompiledModule.t) (idx : StructDefInstantiationIndex.t) : 
-  match CompiledModule.struct_instantiation_at self idx with
-  | Panic.Value _ => True
-  | Panic.Panic _ => True
-  end.
+    match CompiledModule.struct_instantiation_at self idx with
+    | Panic.Value _ => True
+    | Panic.Panic _ => True
+    end.
   Proof.
   Admitted.
 
   Lemma struct_def_at_is_valid (self : CompiledModule.t) (idx : StructDefinitionIndex.t) :
-  match CompiledModule.struct_def_at self idx with
-  | Panic.Value _ => True
-  | Panic.Panic _ => True
-  end.
+    match CompiledModule.struct_def_at self idx with
+    | Panic.Value _ => True
+    | Panic.Panic _ => True
+    end.
   Proof.
   Admitted.
 
   Lemma struct_handle_at_is_valid (self : CompiledModule.t) (idx : StructHandleIndex.t) :
-  match CompiledModule.struct_handle_at self idx with
-  | Panic.Value _ => True
-  | Panic.Panic _ => True
-  end.
+    match CompiledModule.struct_handle_at self idx with
+    | Panic.Value _ => True
+    | Panic.Panic _ => True
+    end.
   Proof.
   Admitted.
 
   Lemma signature_at_is_valid (self : CompiledModule.t) (idx : SignatureIndex.t) :
-  match CompiledModule.signature_at self idx with
-  | Panic.Value _ => True
-  | Panic.Panic _ => True
-  end.
+    match CompiledModule.signature_at self idx with
+    | Panic.Value _ => True
+    | Panic.Panic _ => True
+    end.
   Proof.
   Admitted.
 
   Lemma constant_at_is_valid (self : CompiledModule.t) (idx : ConstantPoolIndex.t) :
-  match CompiledModule.constant_at self idx with
-  | Panic.Value _ => True
-  | Panic.Panic _ => True
-  end.
+    match CompiledModule.constant_at self idx with
+    | Panic.Value _ => True
+    | Panic.Panic _ => True
+    end.
   Proof.
   Admitted.
 
   Lemma function_handle_at_is_valid (self : CompiledModule.t) (idx : FunctionHandleIndex.t) :
-  match CompiledModule.function_handle_at self idx with
-  | Panic.Value _ => True
-  | Panic.Panic _ => True
-  end.
+    match CompiledModule.function_handle_at self idx with
+    | Panic.Value _ => True
+    | Panic.Panic _ => True
+    end.
   Proof.
   Admitted.
 
   Lemma field_instantiation_at_is_valid (self : CompiledModule.t) (idx : FieldInstantiationIndex.t) :
-  match CompiledModule.field_instantiation_at self idx with
-  | Panic.Value _ => True
-  | Panic.Panic _ => True
-  end.
+    match CompiledModule.field_instantiation_at self idx with
+    | Panic.Value _ => True
+    | Panic.Panic _ => True
+    end.
   Proof.
   Admitted.
 
   Lemma function_instantiation_at_is_valid (self : CompiledModule.t) (idx : FunctionInstantiationIndex.t) :
-  match CompiledModule.function_instantiation_at self idx with
-  | Panic.Value _ => True
-  | Panic.Panic _ => True
-  end.
+    match CompiledModule.function_instantiation_at self idx with
+    | Panic.Value _ => True
+    | Panic.Panic _ => True
+    end.
   Proof.
   Admitted.
 
   Lemma abilities_is_valid (self : CompiledModule.t) (ty : SignatureToken.t) (constraints : list AbilitySet.t) :
-  match CompiledModule.abilities self ty constraints with
-  | Panic.Value _ => True
-  | Panic.Panic _ => True
-  end.
+    match CompiledModule.abilities self ty constraints with
+    | Panic.Value _ => True
+    | Panic.Panic _ => True
+    end.
   Proof.
   Admitted.
-
 End CompiledModule.
 
 Module Bytecode.
@@ -187,4 +178,29 @@ Module Bytecode.
       | Bytecode.VecSwap _ => True
       end.
   End Valid.
-End Bytecode.
\ No newline at end of file
+End Bytecode.
+
+Module Constant.
+  Module Valid.
+    Definition t (x : Constant.t) : Prop :=
+      match Impl_Value.deserialize_constant x with
+      | None => False
+      | Some value => IsValueOfType.t value x.(Constant.type_)
+      end.
+  End Valid.
+End Constant.
+
+Module ConstantPool.
+  Module Valid.
+    Definition t (x : ConstantPool.t) : Prop :=
+      List.Forall Constant.Valid.t x.
+  End Valid.
+End ConstantPool.
+
+Module CompiledModule.
+  Module Valid.
+    Record t (x : CompiledModule.t) : Prop := {
+      constant_pool : ConstantPool.Valid.t x.(CompiledModule.constant_pool);
+    }.
+  End Valid.
+End CompiledModule.
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 4cee962b3..eacc50650 100644
--- a/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
+++ b/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
@@ -1,41 +1,29 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.simulations.M.
 Require Import CoqOfRust.lib.proofs.lib.
-Require Import move_sui.proofs.move_abstract_stack.lib.
-Require Import move_sui.proofs.move_binary_format.file_format.
 Require Import move_sui.simulations.move_abstract_stack.lib.
 Require Import move_sui.simulations.move_binary_format.file_format.
 Require Import move_sui.simulations.move_bytecode_verifier.type_safety.
 Require Import move_sui.simulations.move_vm_runtime.interpreter.
 Require Import move_sui.simulations.move_vm_types.values.values_impl.
+Require Import move_sui.proofs.move_abstract_stack.lib.
+Require Import move_sui.proofs.move_binary_format.file_format.
+Require Import move_sui.proofs.move_vm_types.values.values_impl.
 
 Import simulations.M.Notations.
 
 Module TypeSafetyChecker.
   Module Valid.
     Record t (x : TypeSafetyChecker.t) : Prop := {
+      module : CompiledModule.Valid.t x.(TypeSafetyChecker.module);
       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
-    | ValueImpl.U8 _, SignatureToken.U8 => True
-    | ValueImpl.U16 _, SignatureToken.U16 => True
-    | ValueImpl.U32 _, SignatureToken.U32 => True
-    | ValueImpl.U64 _, SignatureToken.U64 => True
-    | ValueImpl.U128 _, SignatureToken.U128 => True
-    | ValueImpl.U256 _, SignatureToken.U256 => True
-    | ValueImpl.Bool _, SignatureToken.Bool => True
-    | ValueImpl.Address _, SignatureToken.Address => True
-    (* TODO: other cases *)
-    | _, _ => False
-    end.
-
   Lemma value_of_bool (value : Value.t) (ty : SignatureToken.t)
-    (H_value : t value ty)
+    (H_value : IsValueOfType.t value ty)
     (* This is the form in which is appears in the proofs *)
     (H_ty : ty = SignatureToken.Bool) :
     exists b, value = ValueImpl.Bool b.
@@ -46,7 +34,7 @@ Module IsValueOfType.
   Qed.
 
   Lemma value_of_integer (value : Value.t) (ty : SignatureToken.t)
-      (H_value : t value ty)
+      (H_value : IsValueOfType.t value ty)
       (H_ty : SignatureToken.is_integer ty = true) :
     exists (integer_value : IntegerValue.t),
     value = IntegerValue.to_value_impl integer_value.
@@ -195,6 +183,10 @@ Lemma progress
     (type_safety_checker : TypeSafetyChecker.t)
     (H_type_safety_checker : TypeSafetyChecker.Valid.t type_safety_checker)
     (H_interpreter : IsInterpreterContextOfType.t locals interpreter type_safety_checker)
+    (H_resolver :
+      resolver.(loader.Resolver.binary).(loader.BinaryType.compiled) =
+      type_safety_checker.(TypeSafetyChecker.module)
+    )
     (* This lemma is not true for [Bytecode.Ret] *)
     (H_not_Ret : instruction <> Bytecode.Ret) :
   let state := {|
@@ -230,7 +222,8 @@ Proof.
   pose proof file_format.SignatureToken.ImplEq.I_is_valid as H_Eq.
   destruct interpreter as [[stack]].
   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 H_type_safety_checker as [H_module H_stack_ty]; cbn in *.
+  destruct H_module as [H_constant_pool].
   destruct instruction eqn:H_instruction_eq; cbn in *.
   { guard_instruction Bytecode.Pop.
     destruct_abstract_pop.
@@ -329,7 +322,21 @@ Proof.
       sauto lq: on rew: off.
   }
   { guard_instruction (Bytecode.LdConst t).
-    admit.
+    unfold_state_monad.
+    unfold CompiledModule.constant_at.
+    match goal with
+    | |- context[List.nth_error ?l ?i] =>
+      epose proof (List.Forall_nth_error _ l i H_constant_pool)
+    end.
+    destruct List.nth_error as [constant|] eqn:H_nth_error; cbn; try easy.
+    destruct_abstract_push.
+    unfold loader.Resolver.Impl_Resolver.constant_at.
+    rewrite H_resolver.
+    unfold CompiledModule.constant_at; rewrite H_nth_error; cbn.
+    unfold Constant.Valid.t in *.
+    destruct Impl_Value.deserialize_constant as [value|]; cbn; [|easy].
+    step; cbn; try easy.
+    hauto l: on.
   }
   { guard_instruction Bytecode.LdTrue.
     destruct_abstract_push.
@@ -344,8 +351,9 @@ Proof.
   { guard_instruction (Bytecode.CopyLoc z).
     unfold_state_monad.
     do 3 (step; cbn; try easy).
-    unfold TypeSafetyChecker.Impl_TypeSafetyChecker.local_at; cbn.
+    unfold TypeSafetyChecker.Impl_TypeSafetyChecker.local_at in *; cbn in *.
     destruct_abstract_push.
+    unfold Impl_Locals.copy_loc.
     admit.
   }
   { guard_instruction (Bytecode.MoveLoc z).
@@ -628,10 +636,10 @@ Lemma verify_instr_is_valid (instruction : Bytecode.t) (pc : Z) (type_safety_che
   | _ => True
   end.
 Proof.
+  destruct H_type_safety_checker as [H_module H_stack].
   destruct instruction eqn:H_instruction; cbn in *.
   { guard_instruction Bytecode.Pop.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
@@ -643,7 +651,6 @@ Proof.
   }
   { guard_instruction (Bytecode.BrTrue z).
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
@@ -652,7 +659,6 @@ Proof.
   }
   { guard_instruction (Bytecode.BrFalse z).
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
@@ -660,7 +666,7 @@ Proof.
     sauto.
   }
   { guard_instruction (Bytecode.Branch z).
-    apply H_type_safety_checker.
+    hauto l: on.
   }
   { guard_instruction (Bytecode.LdU8 z).
     unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push.
@@ -713,7 +719,6 @@ Proof.
   }
   { guard_instruction Bytecode.CastU8.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack). 
     destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
@@ -730,7 +735,6 @@ Proof.
   }
   { guard_instruction Bytecode.CastU16.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
@@ -747,7 +751,6 @@ Proof.
   }
   { guard_instruction Bytecode.CastU32.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
@@ -764,7 +767,6 @@ Proof.
   }
   { guard_instruction Bytecode.CastU64.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
@@ -781,7 +783,6 @@ Proof.
   }
   { guard_instruction Bytecode.CastU128.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
@@ -798,7 +799,6 @@ Proof.
   }
   { guard_instruction Bytecode.CastU256.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
@@ -919,7 +919,6 @@ Proof.
   }
   { guard_instruction Bytecode.FreezeRef.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
@@ -964,7 +963,6 @@ Proof.
   }
   { guard_instruction Bytecode.Add.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
@@ -1006,7 +1004,6 @@ Proof.
   }
   { guard_instruction Bytecode.Mul.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
@@ -1344,7 +1341,7 @@ Proof.
     hauto l: on.
   }
   { guard_instruction Bytecode.Nop.
-    apply H_type_safety_checker.
+    hauto l: on.
   }
   { guard_instruction (Bytecode.ExistsDeprecated t).
     admit.
@@ -1366,7 +1363,6 @@ Proof.
   }
   { guard_instruction Bytecode.Shl.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
@@ -1387,7 +1383,6 @@ Proof.
   }
   { guard_instruction Bytecode.Shr.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
diff --git a/CoqOfRust/move_sui/proofs/move_vm_types/values/values_impl.v b/CoqOfRust/move_sui/proofs/move_vm_types/values/values_impl.v
new file mode 100644
index 000000000..255827522
--- /dev/null
+++ b/CoqOfRust/move_sui/proofs/move_vm_types/values/values_impl.v
@@ -0,0 +1,22 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.simulations.M.
+Require Import CoqOfRust.lib.proofs.lib.
+
+Require Import move_sui.simulations.move_binary_format.file_format.
+Require Import move_sui.simulations.move_vm_types.values.values_impl.
+
+Module IsValueOfType.
+  Definition t (value : Value.t) (typ : SignatureToken.t) : Prop :=
+    match value, typ with
+    | ValueImpl.U8 _, SignatureToken.U8 => True
+    | ValueImpl.U16 _, SignatureToken.U16 => True
+    | ValueImpl.U32 _, SignatureToken.U32 => True
+    | ValueImpl.U64 _, SignatureToken.U64 => True
+    | ValueImpl.U128 _, SignatureToken.U128 => True
+    | ValueImpl.U256 _, SignatureToken.U256 => True
+    | ValueImpl.Bool _, SignatureToken.Bool => True
+    | ValueImpl.Address _, SignatureToken.Address => True
+    (* TODO: other cases *)
+    | _, _ => False
+    end.
+End IsValueOfType.
diff --git a/CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v b/CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v
index 97e54e161..7a7584b98 100644
--- a/CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v
+++ b/CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v
@@ -606,21 +606,17 @@ Definition execute_instruction
       interpreter.operand_stack.push(val)?
   }
   *)
-  (* NOTE: paused from investigation *)
-  | Bytecode.LdConst idx => execute_instruction_TODO
-    (* let constant := Resolver.Impl_Resolver.constant_at resolver idx in
-    (* TODO: 
-      - resolve mutual dependency issue 
-      - figure out the logic to load a constant *)
-    let val := Value.Impl_Value.deserialize_constant constant in
-    let val := match val with
-    | Some v => v
-    | None => PartialVMError.new StatusCode.VERIFIER_INVARIANT_VIOLATION
-    end in
-    letS!? _ := liftS! State.Lens.interpreter (
-      liftS! Interpreter.Lens.lens_self_stack $ Stack.Impl_Stack.push val) in 
-    returnS! $ Result.Ok InstrRet.Ok *)
-
+  | Bytecode.LdConst idx =>
+    letS! constant := return!toS! $ Resolver.Impl_Resolver.constant_at resolver idx in
+    match Impl_Value.deserialize_constant constant with
+    | None =>
+      returnS! $ Result.Err $
+        PartialVMError.new StatusCode.VERIFIER_INVARIANT_VIOLATION
+    | Some val =>
+      letS!? _ := liftS! State.Lens.interpreter (
+        liftS! Interpreter.Lens.operand_stack $ Stack.Impl_Stack.push val) in
+      returnS! $ Result.Ok InstrRet.Ok
+    end
   (* 
   Bytecode::LdTrue => {
       gas_meter.charge_simple_instr(S::LdTrue)?;
diff --git a/CoqOfRust/move_sui/simulations/move_vm_types/values/values_impl.v b/CoqOfRust/move_sui/simulations/move_vm_types/values/values_impl.v
index 2cde27cc3..00c6f6fad 100644
--- a/CoqOfRust/move_sui/simulations/move_vm_types/values/values_impl.v
+++ b/CoqOfRust/move_sui/simulations/move_vm_types/values/values_impl.v
@@ -11,7 +11,7 @@ Module PartialVMError := errors.PartialVMError.
 Require CoqOfRust.move_sui.simulations.move_core_types.vm_status.
 Module StatusCode := vm_status.StatusCode.
 
-Require CoqOfRust.move_sui.simulations.move_binary_format.file_format.
+Require Import CoqOfRust.move_sui.simulations.move_binary_format.file_format.
 
 (* TODO(progress): 
   - Implement `Reference`:
@@ -21,11 +21,6 @@ Require CoqOfRust.move_sui.simulations.move_binary_format.file_format.
     - read_ref
 *)
 
-(* NOTE(STUB): Only implement if necessary *)
-Module Constant.
-  Parameter t : Set.
-End Constant.
-
 Module AccountAddress.
   Parameter t : Set.
 End AccountAddress.
@@ -492,6 +487,18 @@ Module Value.
   Definition coerce_Locals_Container (self : t) : Value.t. Admitted.
 End Value.
 
+Module Impl_Value.
+  (*
+  pub fn deserialize_constant(constant: &Constant) -> Option<Value> {
+      let layout = Self::constant_sig_token_to_layout(&constant.type_)?;
+      Value::simple_deserialize(&constant.data, &layout)
+  }
+  *)
+  (** We keep this function as axiom for now, as its definition would be quite complex and the
+      details are not required for the verification of the type-checker. *)
+  Parameter deserialize_constant : Constant.t -> option Value.t.
+End Impl_Value.
+
 (*
 impl ContainerRef {
     fn read_ref(self) -> PartialVMResult<Value> {

From 574116ab555913f955e516f6d47b61b11b374874 Mon Sep 17 00:00:00 2001
From: Guillaume Claret <dev@clarus.me>
Date: Tue, 24 Dec 2024 11:23:52 +0100
Subject: [PATCH 3/4] sui: more proofs for the type-checker

---
 CoqOfRust/lib/proofs/lib.v                    |  12 +
 .../proofs/move_binary_format/file_format.v   |  50 +-
 .../move_bytecode_verifier/type_safety.v      | 190 +++--
 .../proofs/move_vm_types/values/values_impl.v |   3 +-
 .../move_bytecode_verifier/type_safety.v      |  82 +-
 .../simulations/move_vm_runtime/interpreter.v |   2 +-
 .../move_vm_types/values/values_impl.v        | 761 ++++++++++--------
 CoqOfRust/simulations/M.v                     |  12 +
 8 files changed, 663 insertions(+), 449 deletions(-)

diff --git a/CoqOfRust/lib/proofs/lib.v b/CoqOfRust/lib/proofs/lib.v
index 82bb5adf0..262a92f74 100644
--- a/CoqOfRust/lib/proofs/lib.v
+++ b/CoqOfRust/lib/proofs/lib.v
@@ -111,4 +111,16 @@ Module List.
     generalize dependent n.
     induction H_l; intros; destruct n; cbn; sfirstorder.
   Qed.
+
+  Lemma Forall2_nth_error {A B : Set} (P : A -> B -> Prop) (l1 : list A) (l2 : list B) (n : nat)
+      (H_l : List.Forall2 P l1 l2) :
+    match List.nth_error l1 n, List.nth_error l2 n with
+    | Some x1, Some x2 => P x1 x2
+    | Some _, None | None, Some _ => False
+    | _, _ => True
+    end.
+  Proof.
+    generalize dependent n.
+    induction H_l; intros; destruct n; cbn; sfirstorder.
+  Qed.
 End List.
diff --git a/CoqOfRust/move_sui/proofs/move_binary_format/file_format.v b/CoqOfRust/move_sui/proofs/move_binary_format/file_format.v
index 42c8f3f42..84ec9ca76 100644
--- a/CoqOfRust/move_sui/proofs/move_binary_format/file_format.v
+++ b/CoqOfRust/move_sui/proofs/move_binary_format/file_format.v
@@ -13,7 +13,30 @@ Module SignatureToken.
   Admitted.
 End SignatureToken.
 
+Module Constant.
+  Module Valid.
+    Definition t (x : Constant.t) : Prop :=
+      match Impl_Value.deserialize_constant x with
+      | None => False
+      | Some value => IsValueOfType.t value x.(Constant.type_)
+      end.
+  End Valid.
+End Constant.
+
+Module ConstantPool.
+  Module Valid.
+    Definition t (x : ConstantPool.t) : Prop :=
+      List.Forall Constant.Valid.t x.
+  End Valid.
+End ConstantPool.
+
 Module CompiledModule.
+  Module Valid.
+    Record t (x : CompiledModule.t) : Prop := {
+      constant_pool : ConstantPool.Valid.t x.(CompiledModule.constant_pool);
+    }.
+  End Valid.
+
   Lemma field_handle_at_is_valid (self : CompiledModule.t) (idx : FieldHandleIndex.t) :
     match CompiledModule.field_handle_at self idx with
     | Panic.Value _ => True
@@ -119,7 +142,7 @@ Module Bytecode.
       | Bytecode.LdConst _ => True
       | Bytecode.LdTrue => True
       | Bytecode.LdFalse => True
-      | Bytecode.CopyLoc _ => True
+      | Bytecode.CopyLoc z => Integer.Valid.t IntegerKind.U8 z
       | Bytecode.MoveLoc _ => True
       | Bytecode.StLoc _ => True
       | Bytecode.Call _ => True
@@ -179,28 +202,3 @@ Module Bytecode.
       end.
   End Valid.
 End Bytecode.
-
-Module Constant.
-  Module Valid.
-    Definition t (x : Constant.t) : Prop :=
-      match Impl_Value.deserialize_constant x with
-      | None => False
-      | Some value => IsValueOfType.t value x.(Constant.type_)
-      end.
-  End Valid.
-End Constant.
-
-Module ConstantPool.
-  Module Valid.
-    Definition t (x : ConstantPool.t) : Prop :=
-      List.Forall Constant.Valid.t x.
-  End Valid.
-End ConstantPool.
-
-Module CompiledModule.
-  Module Valid.
-    Record t (x : CompiledModule.t) : Prop := {
-      constant_pool : ConstantPool.Valid.t x.(CompiledModule.constant_pool);
-    }.
-  End Valid.
-End CompiledModule.
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 eacc50650..eab526d12 100644
--- a/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
+++ b/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
@@ -69,21 +69,47 @@ Module IsStackValueOfType.
   Qed.
 End IsStackValueOfType.
 
-(** Here we show that all the stack operations on values follow the stack operations on types *)
-Module Stack.
-  (* TODO *)
-End Stack.
+Module IsLocalsOfType.
+  Record t (locals : values_impl.Locals.t) (locals_ty : type_safety.Locals.t) : Prop := {
+    param_count : locals_ty.(type_safety.Locals.param_count) = 0;
+    parameters : locals_ty.(type_safety.Locals.parameters) = {| Signature.a0 := [] |};
+    locals :
+      List.Forall2 IsValueOfType.t
+        locals
+        locals_ty.(type_safety.Locals.locals).(Signature.a0);
+  }.
+
+  Lemma local_at_eq locals locals_ty index
+      (H : t locals locals_ty)
+      (H_index : Integer.Valid.t IntegerKind.U8 index) :
+    Impl_Locals.local_at locals_ty {| file_format_index.LocalIndex.a0 := index |} =
+    Panic.List.nth
+      locals_ty.(type_safety.Locals.locals).(Signature.a0)
+      (Z.to_nat index).
+  Proof.
+    unfold Impl_Locals.local_at.
+    destruct H as [H_param_count ? ?].
+    rewrite H_param_count.
+    step; cbn in *.
+    { lia. }
+    { f_equal; lia. }
+  Qed.
+End IsLocalsOfType.
 
 Module IsInterpreterContextOfType.
-  (** For now we do not use the [locals] but they should be eventually *)
-  Definition t
+  Record t
       (locals : Locals.t) (interpreter : Interpreter.t)
       (type_safety_checker : TypeSafetyChecker.t) :
-      Prop :=
-    IsStackValueOfType.t
-      interpreter.(Interpreter.operand_stack)
-      type_safety_checker.(TypeSafetyChecker.stack).
-  Arguments t /.
+      Prop := {
+    locals :
+      IsLocalsOfType.t
+        locals
+        type_safety_checker.(TypeSafetyChecker.locals);
+    stack :
+      IsStackValueOfType.t
+        interpreter.(Interpreter.operand_stack)
+        type_safety_checker.(TypeSafetyChecker.stack);
+  }.
 End IsInterpreterContextOfType.
 
 (* To know in which case we are *)
@@ -181,6 +207,7 @@ Lemma progress
     (instruction : Bytecode.t)
     (pc : Z) (locals : Locals.t) (interpreter : Interpreter.t)
     (type_safety_checker : TypeSafetyChecker.t)
+    (H_instruction : Bytecode.Valid.t instruction)
     (H_type_safety_checker : TypeSafetyChecker.Valid.t type_safety_checker)
     (H_interpreter : IsInterpreterContextOfType.t locals interpreter type_safety_checker)
     (H_resolver :
@@ -215,7 +242,7 @@ Lemma progress
     | StatusCode.ARITHMETIC_ERROR => True
     | _ => False
     end
-  | _, _ => True
+  | Panic.Panic _, _ | Panic.Value (Result.Err _, _), _ => True
   end.
 Proof.
   Opaque AbstractStack.flatten.
@@ -224,6 +251,7 @@ Proof.
   destruct type_safety_checker as [module function_context locals_ty stack_ty]; cbn in *.
   destruct H_type_safety_checker as [H_module H_stack_ty]; cbn in *.
   destruct H_module as [H_constant_pool].
+  destruct H_interpreter as [H_locals_typing H_stack_typing].
   destruct instruction eqn:H_instruction_eq; cbn in *.
   { guard_instruction Bytecode.Pop.
     destruct_abstract_pop.
@@ -235,43 +263,45 @@ Proof.
   { guard_instruction (Bytecode.BrTrue z).
     destruct_abstract_pop.
     destruct_initial_if.
+    now constructor.
   }
   { guard_instruction (Bytecode.BrFalse z).
     destruct_abstract_pop.
     destruct_initial_if.
+    now constructor.
   }
   { guard_instruction (Bytecode.Branch z).
-    apply H_interpreter.
+    easy.
   }
   { guard_instruction (Bytecode.LdU8 z).
     destruct_abstract_push.
     step; cbn; [|easy].
-    sauto lq: on.
+    sauto q: on.
   }
   { guard_instruction (Bytecode.LdU16 z).
     destruct_abstract_push.
     step; cbn; [|easy].
-    sauto lq: on.
+    sauto q: on.
   }
   { guard_instruction (Bytecode.LdU32 z).
     destruct_abstract_push.
     step; cbn; [|easy].
-    sauto lq: on.
+    sauto q: on.
   }
   { guard_instruction (Bytecode.LdU64 z).
     destruct_abstract_push.
     step; cbn; [|easy].
-    sauto lq: on.
+    sauto q: on.
   }
   { guard_instruction (Bytecode.LdU128 z).
     destruct_abstract_push.
     step; cbn; [|easy].
-    sauto lq: on.
+    sauto q: on.
   }
   { guard_instruction (Bytecode.LdU256 z).
     destruct_abstract_push.
     step; cbn; [|easy].
-    sauto lq: on.
+    sauto q: on.
   }
   { guard_instruction Bytecode.CastU8.
     destruct_abstract_pop.
@@ -279,7 +309,8 @@ Proof.
     destruct_abstract_push.
     step; cbn; (try easy); (try now destruct operand_ty);
       repeat (step; cbn; try easy);
-      sauto lq: on rew: off.
+      constructor; cbn;
+      sauto lq: on.
   }
   { guard_instruction Bytecode.CastU16.
     destruct_abstract_pop.
@@ -287,7 +318,8 @@ Proof.
     destruct_abstract_push.
     step; cbn; (try easy); (try now destruct operand_ty);
       repeat (step; cbn; try easy);
-      sauto lq: on rew: off.
+      constructor; cbn;
+      sauto lq: on.
   }
   { guard_instruction Bytecode.CastU32.
     destruct_abstract_pop.
@@ -295,7 +327,8 @@ Proof.
     destruct_abstract_push.
     step; cbn; (try easy); (try now destruct operand_ty);
       repeat (step; cbn; try easy);
-      sauto lq: on rew: off.
+      constructor; cbn;
+      sauto lq: on.
   }
   { guard_instruction Bytecode.CastU64.
     destruct_abstract_pop.
@@ -303,7 +336,8 @@ Proof.
     destruct_abstract_push.
     step; cbn; (try easy); (try now destruct operand_ty);
       repeat (step; cbn; try easy);
-      sauto lq: on rew: off.
+      constructor; cbn;
+      sauto lq: on.
   }
   { guard_instruction Bytecode.CastU128.
     destruct_abstract_pop.
@@ -311,7 +345,8 @@ Proof.
     destruct_abstract_push.
     step; cbn; (try easy); (try now destruct operand_ty);
       repeat (step; cbn; try easy);
-      sauto lq: on rew: off.
+      constructor; cbn;
+      sauto lq: on.
   }
   { guard_instruction Bytecode.CastU256.
     destruct_abstract_pop.
@@ -319,7 +354,8 @@ Proof.
     destruct_abstract_push.
     step; cbn; (try easy); (try now destruct operand_ty);
       repeat (step; cbn; try easy);
-      sauto lq: on rew: off.
+      constructor; cbn;
+      sauto lq: on.
   }
   { guard_instruction (Bytecode.LdConst t).
     unfold_state_monad.
@@ -336,25 +372,58 @@ Proof.
     unfold Constant.Valid.t in *.
     destruct Impl_Value.deserialize_constant as [value|]; cbn; [|easy].
     step; cbn; try easy.
-    hauto l: on.
+    sauto q: on.
   }
   { guard_instruction Bytecode.LdTrue.
     destruct_abstract_push.
     step; cbn; [|exact I].
-    sauto lq: on.
+    sauto q: on.
   }
   { guard_instruction Bytecode.LdFalse.
     destruct_abstract_push.
     step; cbn; [|exact I].
-    sauto lq: on.
+    sauto q: on.
   }
   { guard_instruction (Bytecode.CopyLoc z).
     unfold_state_monad.
-    do 3 (step; cbn; try easy).
-    unfold TypeSafetyChecker.Impl_TypeSafetyChecker.local_at in *; cbn in *.
+    unfold TypeSafetyChecker.Impl_TypeSafetyChecker.local_at; cbn.
+    match goal with
+    | |- context[Impl_Locals.local_at ?locals_ty ?index] =>
+      let H_eq := fresh "H_eq" in
+      pose proof (IsLocalsOfType.local_at_eq
+        locals
+        locals_ty
+        index.(file_format_index.LocalIndex.a0)
+        H_locals_typing
+      ) as H_eq;
+      cbn in H_eq;
+      rewrite H_eq by assumption;
+      clear H_eq
+    end.
+    do 4 (step; cbn; try easy).
     destruct_abstract_push.
     unfold Impl_Locals.copy_loc.
-    admit.
+    unfold Panic.List.nth in *.
+    destruct H_locals_typing as [? ? H_locals].
+    destruct locals_ty as [? ? [locals_ty]]; cbn in *.
+    pose proof List.Forall2_nth_error _ locals locals_ty (Z.to_nat z) H_locals as H_nth_error.
+    unfold Value.t in H_nth_error.
+    destruct (List.nth_error locals) as [local|] eqn:H_nth_error_eq; cbn.
+    { destruct local eqn:H_local_eq; cbn.
+      { admit. }
+      all: try (
+        step; cbn; try easy;
+        constructor; cbn; [hauto l: on|];
+        match goal with
+        | H : _ = _ |- _ => rewrite H
+        end;
+        constructor; try assumption;
+        destruct (List.nth_error locals_ty); try easy;
+        hauto lq: on
+      ).
+      { admit. }
+    }
+    { now destruct (List.nth_error locals_ty). }
   }
   { guard_instruction (Bytecode.MoveLoc z).
     unfold TypeSafetyChecker.Impl_TypeSafetyChecker.local_at; cbn.
@@ -428,6 +497,8 @@ Proof.
     destruct_all IntegerValue.t; cbn in *; try easy; (
       unfold IntegerValue.add_checked; cbn;
       repeat (step; cbn; try easy);
+      constructor; cbn;
+      try assumption;
       sauto lq: on
     ).
   }
@@ -439,6 +510,8 @@ Proof.
     destruct_all IntegerValue.t; cbn in *; try easy; (
       unfold IntegerValue.sub_checked; cbn;
       repeat (step; cbn; try easy);
+      constructor; cbn;
+      try assumption;
       sauto lq: on
     ).
   }
@@ -450,6 +523,8 @@ Proof.
     destruct_all IntegerValue.t; cbn in *; try easy; (
       unfold IntegerValue.mul_checked; cbn;
       repeat (step; cbn; try easy);
+      constructor; cbn;
+      try assumption;
       sauto lq: on
     ).
   }
@@ -461,6 +536,8 @@ Proof.
     destruct_all IntegerValue.t; cbn in *; try easy; (
       unfold IntegerValue.rem_checked; cbn;
       repeat (step; cbn; try easy);
+      constructor; cbn;
+      try assumption;
       sauto lq: on
     ).
   }
@@ -472,6 +549,8 @@ Proof.
     destruct_all IntegerValue.t; cbn in *; try easy; (
       unfold IntegerValue.div_checked; cbn;
       repeat (step; cbn; try easy);
+      constructor; cbn;
+      try assumption;
       sauto lq: on
     ).
   }
@@ -483,6 +562,8 @@ Proof.
     destruct_all IntegerValue.t; cbn in *; try easy; (
       unfold IntegerValue.bit_or; cbn;
       repeat (step; cbn; try easy);
+      constructor; cbn;
+      try assumption;
       sauto lq: on
     ).
   }
@@ -494,6 +575,8 @@ Proof.
     destruct_all IntegerValue.t; cbn in *; try easy; (
       unfold IntegerValue.bit_and; cbn;
       repeat (step; cbn; try easy);
+      constructor; cbn;
+      try assumption;
       sauto lq: on
     ).
   }
@@ -505,6 +588,8 @@ Proof.
     destruct_all IntegerValue.t; cbn in *; try easy; (
       unfold IntegerValue.bit_xor; cbn;
       repeat (step; cbn; try easy);
+      constructor; cbn;
+      try assumption;
       sauto lq: on
     ).
   }
@@ -514,7 +599,7 @@ Proof.
     destruct_initial_if.
     destruct_abstract_push.
     step; cbn; try easy.
-    hauto l: on.
+    constructor; cbn; sauto lq: on.
   }
   { guard_instruction Bytecode.And.
     destruct_abstract_pop.
@@ -522,13 +607,14 @@ Proof.
     destruct_initial_if.
     destruct_abstract_push.
     step; cbn; try easy.
-    hauto l: on.
+    constructor; cbn; sauto lq: on.
   }
   { guard_instruction Bytecode.Not.
     destruct_abstract_pop.
     destruct_initial_if.
     destruct_abstract_push.
-    hauto l: on.
+    step; cbn; try easy.
+    constructor; cbn; sauto lq: on.
   }
   { guard_instruction Bytecode.Eq.
     admit.
@@ -543,6 +629,7 @@ Proof.
     destruct_abstract_push.
     destruct_all IntegerValue.t; cbn in *; try easy;
       repeat (step; cbn; try easy);
+      constructor; cbn;
       sauto lq: on.
   }
   { guard_instruction Bytecode.Gt.
@@ -552,6 +639,7 @@ Proof.
     destruct_abstract_push.
     destruct_all IntegerValue.t; cbn in *; try easy;
       repeat (step; cbn; try easy);
+      constructor; cbn;
       sauto lq: on.
   }
   { guard_instruction Bytecode.Le.
@@ -561,6 +649,7 @@ Proof.
     destruct_abstract_push.
     destruct_all IntegerValue.t; cbn in *; try easy;
       repeat (step; cbn; try easy);
+      constructor; cbn;
       sauto lq: on.
   }
   { guard_instruction Bytecode.Ge.
@@ -570,13 +659,14 @@ Proof.
     destruct_abstract_push.
     destruct_all IntegerValue.t; cbn in *; try easy;
       repeat (step; cbn; try easy);
+      constructor; cbn;
       sauto lq: on.
   }
   { guard_instruction Bytecode.Abort.
     admit.
   }
   { guard_instruction Bytecode.Nop.
-    assumption.
+    now constructor; cbn.
   }
   { guard_instruction (Bytecode.ExistsDeprecated t).
     admit.
@@ -838,8 +928,8 @@ Proof.
     do 3 (step; cbn; trivial).
     unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push.
     with_strategy opaque [AbstractStack.push] unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
-    pose proof (AbstractStack.push_is_valid
+    admit.
+    (* pose proof (AbstractStack.push_is_valid
       (TypeSafetyChecker.Impl_TypeSafetyChecker.local_at type_safety_checker {| file_format_index.LocalIndex.a0 := z |})
       type_safety_checker.(TypeSafetyChecker.stack)
       H_stack
@@ -849,11 +939,11 @@ Proof.
     step; cbn; trivial.
     destruct u.
     constructor; cbn.
-    apply H.
+    apply H. *)
   }
   { guard_instruction (Bytecode.MoveLoc z).
-    destruct H_type_safety_checker as [H_stack].
-    unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push.
+    admit.
+    (* unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push.
     with_strategy opaque [AbstractStack.push] unfold_state_monad.
     pose proof (AbstractStack.push_is_valid
       (TypeSafetyChecker.Impl_TypeSafetyChecker.local_at type_safety_checker {| file_format_index.LocalIndex.a0 := z |})
@@ -865,11 +955,10 @@ Proof.
     step; cbn; trivial.
     destruct u.
     constructor; cbn.
-    apply H.
+    apply H. *)
   }
   { guard_instruction (Bytecode.StLoc z).
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
@@ -892,7 +981,6 @@ Proof.
   { guard_instruction (Bytecode.Unpack t).
     unfold_state_monad.
     destruct CompiledModule.struct_def_at; cbn; trivial.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     unfold set; cbn.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
@@ -983,7 +1071,6 @@ Proof.
   }
   { guard_instruction Bytecode.Sub.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
@@ -1024,7 +1111,6 @@ Proof.
   }
   { guard_instruction Bytecode.Mod.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
@@ -1045,7 +1131,6 @@ Proof.
   }
   { guard_instruction Bytecode.Div.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
@@ -1066,7 +1151,6 @@ Proof.
   }
   { guard_instruction Bytecode.BitOr.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
@@ -1087,7 +1171,6 @@ Proof.
   }
   { guard_instruction Bytecode.BitAnd.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
@@ -1108,7 +1191,6 @@ Proof.
   }
   { guard_instruction Bytecode.Xor.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
@@ -1129,7 +1211,6 @@ Proof.
   }
   { guard_instruction Bytecode.Or.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
@@ -1150,7 +1231,6 @@ Proof.
   }
   { guard_instruction Bytecode.And.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
@@ -1171,7 +1251,6 @@ Proof.
   }
   { guard_instruction Bytecode.Not.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
@@ -1189,7 +1268,6 @@ Proof.
   }
   { guard_instruction Bytecode.Eq.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand1 stack']|]; cbn; [|trivial].
@@ -1214,7 +1292,6 @@ Proof.
   }
   { guard_instruction Bytecode.Neq.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand1 stack']|]; cbn; [|trivial].
@@ -1239,7 +1316,6 @@ Proof.
   }
   { guard_instruction Bytecode.Lt.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand1 stack']|]; cbn; [|trivial].
@@ -1262,7 +1338,6 @@ Proof.
   }
   { guard_instruction Bytecode.Gt.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand1 stack']|]; cbn; [|trivial].
@@ -1285,7 +1360,6 @@ Proof.
   }
   { guard_instruction Bytecode.Le.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand1 stack']|]; cbn; [|trivial].
@@ -1308,7 +1382,6 @@ Proof.
   }
   { guard_instruction Bytecode.Ge.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand1 stack']|]; cbn; [|trivial].
@@ -1331,7 +1404,6 @@ Proof.
   }
   { guard_instruction Bytecode.Abort.
     unfold_state_monad.
-    destruct H_type_safety_checker as [H_stack].
     destruct type_safety_checker; cbn in *.
     pose proof (AbstractStack.pop_is_valid stack H_stack).
     destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
diff --git a/CoqOfRust/move_sui/proofs/move_vm_types/values/values_impl.v b/CoqOfRust/move_sui/proofs/move_vm_types/values/values_impl.v
index 255827522..9d928abcb 100644
--- a/CoqOfRust/move_sui/proofs/move_vm_types/values/values_impl.v
+++ b/CoqOfRust/move_sui/proofs/move_vm_types/values/values_impl.v
@@ -6,8 +6,9 @@ Require Import move_sui.simulations.move_binary_format.file_format.
 Require Import move_sui.simulations.move_vm_types.values.values_impl.
 
 Module IsValueOfType.
-  Definition t (value : Value.t) (typ : SignatureToken.t) : Prop :=
+  Definition t (value : ValueImpl.t) (typ : SignatureToken.t) : Prop :=
     match value, typ with
+    | ValueImpl.Invalid, _ => False
     | ValueImpl.U8 _, SignatureToken.U8 => True
     | ValueImpl.U16 _, SignatureToken.U16 => True
     | ValueImpl.U32 _, SignatureToken.U32 => True
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 4e5003332..33804814c 100644
--- a/CoqOfRust/move_sui/simulations/move_bytecode_verifier/type_safety.v
+++ b/CoqOfRust/move_sui/simulations/move_bytecode_verifier/type_safety.v
@@ -42,39 +42,37 @@ Module Locals.
     parameters : Signature.t;
     locals : Signature.t;
   }.
-
-  Module Impl_Locals.
-    Definition Self : Set := 
-      move_sui.simulations.move_bytecode_verifier.type_safety.Locals.t.
-
-    Definition new (parameters locals : Signature.t) : Self :=
-      {|
-        Locals.param_count := Signature.len parameters;
-        Locals.parameters := parameters;
-        Locals.locals := locals;
-      |}.
-
-    (* 
-    fn local_at(&self, i: LocalIndex) -> &SignatureToken {
-        let idx = i as usize;
-        if idx < self.param_count {
-            &self.parameters.0[idx]
-        } else {
-            &self.locals.0[idx - self.param_count]
-        }
-    }
-    *)
-    Definition local_at (self : t) (i : LocalIndex.t) : SignatureToken.t :=
-      let idx := i.(LocalIndex.a0) in 
-      if idx <? self.(param_count)
-      then List.nth (Z.to_nat idx) self.(parameters).(Signature.a0) 
-        SignatureToken.Bool (* This should never arrive at *)
-      else List.nth (Z.to_nat $ idx - self.(param_count)) self.(locals).(Signature.a0) 
-        SignatureToken.Bool. (* This should never arrive at *)
-
-  End Impl_Locals.
 End Locals.
 
+Module Impl_Locals.
+  Definition Self : Set :=
+    Locals.t.
+
+  Definition new (parameters locals : Signature.t) : Self :=
+    {|
+      Locals.param_count := Signature.len parameters;
+      Locals.parameters := parameters;
+      Locals.locals := locals;
+    |}.
+
+  (* 
+  fn local_at(&self, i: LocalIndex) -> &SignatureToken {
+      let idx = i as usize;
+      if idx < self.param_count {
+          &self.parameters.0[idx]
+      } else {
+          &self.locals.0[idx - self.param_count]
+      }
+  }
+  *)
+  Definition local_at (self : Self) (i : LocalIndex.t) : M! SignatureToken.t :=
+    let idx := i.(LocalIndex.a0) in
+    if idx <? self.(Locals.param_count) then
+      Panic.List.nth self.(Locals.parameters).(Signature.a0) (Z.to_nat idx)
+    else
+      Panic.List.nth self.(Locals.locals).(Signature.a0) (Z.to_nat $ idx - self.(Locals.param_count)).
+End Impl_Locals.
+
 Definition TYPE_NODE_COST : Z := 30.
 
 Module TypeSafetyChecker.
@@ -95,7 +93,7 @@ Module TypeSafetyChecker.
       move_sui.simulations.move_bytecode_verifier.type_safety.TypeSafetyChecker.t.
 
     Definition new (module : CompiledModule.t) (function_context : FunctionContext.t) : Self :=
-      let locals := Locals.Impl_Locals.new 
+      let locals := Impl_Locals.new 
       (* NOTE: We directly access the corresponded fields here for conveniency *)
       function_context.(FunctionContext.parameters)
       function_context.(FunctionContext.locals) in
@@ -106,8 +104,8 @@ Module TypeSafetyChecker.
         TypeSafetyChecker.stack := AbstractStack.new;
       |}.
 
-    Definition local_at (self : Self) (i : LocalIndex.t) : SignatureToken.t :=
-      Locals.Impl_Locals.local_at self.(locals) i.
+    Definition local_at (self : Self) (i : LocalIndex.t) : M! SignatureToken.t :=
+      Impl_Locals.local_at self.(locals) i.
 
     Definition abilities (self : Self) (t : SignatureToken.t) :
         M! (PartialVMResult.t AbilitySet.t) :=
@@ -428,7 +426,8 @@ fn borrow_loc(
 Definition borrow_loc (offset : CodeOffset.t) (mut_ : bool) (idx : LocalIndex.t)
   : MS! TypeSafetyChecker.t (PartialVMResult.t unit) :=
   letS! verifier := readS! in
-  let loc_signature := TypeSafetyChecker.Impl_TypeSafetyChecker.local_at verifier idx in
+  letS! loc_signature :=
+    return!toS! $ TypeSafetyChecker.Impl_TypeSafetyChecker.local_at verifier idx in
   if SignatureToken.is_reference loc_signature
   then returnS! $ Result.Err $ 
     TypeSafetyChecker.Impl_TypeSafetyChecker.error 
@@ -1039,9 +1038,10 @@ Definition verify_instr
     | Bytecode.StLoc idx => 
         letS! operand :=
           liftS! TypeSafetyChecker.lens_self_stack AbstractStack.pop in
+        letS! operand_at := return!toS! $ TypeSafetyChecker.Impl_TypeSafetyChecker
+          .local_at verifier (LocalIndex.Build_t idx) in
         letS! operand := return!toS! $ safe_unwrap_err operand in
-        if negb $ SignatureToken.t_beq operand $ TypeSafetyChecker.Impl_TypeSafetyChecker
-          .local_at verifier (LocalIndex.Build_t idx)
+        if negb $ SignatureToken.t_beq operand operand_at
         then returnS! $ Result.Err $ TypeSafetyChecker.Impl_TypeSafetyChecker
           .error verifier StatusCode.STLOC_TYPE_MISMATCH_ERROR offset
         else returnS! $ Result.Ok tt
@@ -1248,8 +1248,10 @@ Definition verify_instr
     }
     *)
     | Bytecode.CopyLoc idx => 
-        let local_signature := TypeSafetyChecker.Impl_TypeSafetyChecker
-          .local_at verifier $ LocalIndex.Build_t idx in
+        letS! local_signature :=
+          return!toS! $
+            TypeSafetyChecker.Impl_TypeSafetyChecker.local_at verifier $
+              LocalIndex.Build_t idx in
         letS! abilities := return!toS! $
           CompiledModule.abilities
             verifier.(TypeSafetyChecker.module) local_signature 
@@ -1270,7 +1272,7 @@ Definition verify_instr
           }
     *)
     | Bytecode.MoveLoc idx => 
-      let local_signature := TypeSafetyChecker.Impl_TypeSafetyChecker
+      letS! local_signature := return!toS! $ TypeSafetyChecker.Impl_TypeSafetyChecker
         .local_at verifier $ LocalIndex.Build_t idx in
       TypeSafetyChecker.Impl_TypeSafetyChecker.push local_signature
 
diff --git a/CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v b/CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v
index 7a7584b98..203824c5d 100644
--- a/CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v
+++ b/CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v
@@ -885,7 +885,7 @@ Definition execute_instruction
   | Bytecode.ReadRef => 
     letS!? reference := liftS! State.Lens.interpreter (
       liftS! Interpreter.Lens.operand_stack $ Stack.Impl_Stack.pop_as Reference.t) in
-    letS!? value := returnS! $ Impl_ReferenceImpl.read_ref reference in
+    letS!? value := return!toS! $ Impl_ReferenceImpl.read_ref reference in
     letS!? _ := liftS! State.Lens.interpreter (
       liftS! Interpreter.Lens.operand_stack $ Stack.Impl_Stack.push value) in
     returnS! $ Result.Ok InstrRet.Ok
diff --git a/CoqOfRust/move_sui/simulations/move_vm_types/values/values_impl.v b/CoqOfRust/move_sui/simulations/move_vm_types/values/values_impl.v
index 00c6f6fad..c0f37ccf5 100644
--- a/CoqOfRust/move_sui/simulations/move_vm_types/values/values_impl.v
+++ b/CoqOfRust/move_sui/simulations/move_vm_types/values/values_impl.v
@@ -56,59 +56,22 @@ enum Container {
     VecU256(Rc<RefCell<Vec<u256::U256>>>),
 }
 *)
-Module Container.
-
-  Inductive t : Set :=
-  (* TODO: Resolve mutual dependency issue below *)
-  (*| Locals : list ValueImpl.t -> t*)
-  (* | Vec : list ValueImpl.t -> t *)
-  (* | Struct : list ValueImpl.t -> t *)
-  | VecU8 : list Z -> t
-  | VecU64 : list Z -> t
-  | VecU128 : list Z -> t
-  | VecBool : list bool -> t
-  | VecAddress : list AccountAddress.t -> t
-  | VecU16 : list Z -> t
-  | VecU32 : list Z -> t
-  | VecU256 : list Z -> t
+Module ContainerSkeleton.
+  Inductive t {ValueImpl : Set} : Set :=
+  | Locals (locals : list ValueImpl)
+  | Vec (vec : list ValueImpl)
+  | Struct (fields : list ValueImpl)
+  | VecU8 (vec : list Z)
+  | VecU64 (vec : list Z)
+  | VecU128 (vec : list Z)
+  | VecBool (vec : list bool)
+  | VecAddress (vec : list AccountAddress.t)
+  | VecU16 (vec : list Z)
+  | VecU32 (vec : list Z)
+  | VecU256 (vec : list Z)
   .
-
-  (*
-  fn copy_value(&self) -> PartialVMResult<Self> {
-        let copy_rc_ref_vec_val = |r: &Rc<RefCell<Vec<ValueImpl>>>| {
-            Ok(Rc::new(RefCell::new(
-                r.borrow()
-                    .iter()
-                    .map(|v| v.copy_value())
-                    .collect::<PartialVMResult<_>>()?,
-            )))
-        };
-
-        Ok(match self {
-            Self::Vec(r) => Self::Vec(copy_rc_ref_vec_val(r)?),
-            Self::Struct(r) => Self::Struct(copy_rc_ref_vec_val(r)?),
-
-            Self::VecU8(r) => Self::VecU8(Rc::new(RefCell::new(r.borrow().clone()))),
-            Self::VecU16(r) => Self::VecU16(Rc::new(RefCell::new(r.borrow().clone()))),
-            Self::VecU32(r) => Self::VecU32(Rc::new(RefCell::new(r.borrow().clone()))),
-            Self::VecU64(r) => Self::VecU64(Rc::new(RefCell::new(r.borrow().clone()))),
-            Self::VecU128(r) => Self::VecU128(Rc::new(RefCell::new(r.borrow().clone()))),
-            Self::VecU256(r) => Self::VecU256(Rc::new(RefCell::new(r.borrow().clone()))),
-            Self::VecBool(r) => Self::VecBool(Rc::new(RefCell::new(r.borrow().clone()))),
-            Self::VecAddress(r) => Self::VecAddress(Rc::new(RefCell::new(r.borrow().clone()))),
-
-            Self::Locals(_) => {
-                return Err(
-                    PartialVMError::new(StatusCode::UNKNOWN_INVARIANT_VIOLATION_ERROR)
-                        .with_message("cannot copy a Locals container".to_string()),
-                )
-            }
-        })
-    }*)
-  Definition copy_value (self : t) : PartialVMResult.t t := 
-    Result.Ok self.
-
-End Container.
+  Arguments t : clear implicits.
+End ContainerSkeleton.
 
 (* 
 /// A ContainerRef is a direct reference to a container, which could live either in the frame
@@ -123,50 +86,21 @@ enum ContainerRef {
     },
 }
 *)
-Module ContainerRef.
-  Module __Global.
-    Record t : Set := {
+Module ContainerRefSkeleton.
+  Module Global_.
+    Record t {ValueImpl : Set} : Set := {
       status : GlobalDataStatus.t;
-      container: Container.t;
+      container: ContainerSkeleton.t ValueImpl;
     }.
-  End __Global.
+    Arguments t : clear implicits.
+  End Global_.
 
-  Inductive t : Set :=
-  | Local : Container.t -> t
-  | _Global : __Global.t -> t
+  Inductive t {ValueImpl : Set} : Set :=
+  | Local : ContainerSkeleton.t ValueImpl -> t
+  | Global_ : Global_.t ValueImpl -> t
   .
-
-  (*
-  fn container(&self) -> &Container {
-        match self {
-            Self::Local(container) | Self::Global { container, .. } => container,
-        }
-    }
-  *)
-  Definition container (self : t) : Container.t :=
-    match self with
-    | Local container => container
-    | _Global g => g.(__Global.container)
-    end.
-
-  (* NOTE: This function is ignored
-  fn copy_by_ref(&self) -> Self {
-      match self {
-          Self::Vec(r) => Self::Vec(Rc::clone(r)),
-          Self::Struct(r) => Self::Struct(Rc::clone(r)),
-          Self::VecU8(r) => Self::VecU8(Rc::clone(r)),
-          Self::VecU16(r) => Self::VecU16(Rc::clone(r)),
-          Self::VecU32(r) => Self::VecU32(Rc::clone(r)),
-          Self::VecU64(r) => Self::VecU64(Rc::clone(r)),
-          Self::VecU128(r) => Self::VecU128(Rc::clone(r)),
-          Self::VecU256(r) => Self::VecU256(Rc::clone(r)),
-          Self::VecBool(r) => Self::VecBool(Rc::clone(r)),
-          Self::VecAddress(r) => Self::VecAddress(Rc::clone(r)),
-          Self::Locals(r) => Self::Locals(Rc::clone(r)),
-      }
-  }
-  *)
-End ContainerRef.
+  Arguments t : clear implicits.
+End ContainerRefSkeleton.
 
 (* 
 /// A Move reference pointing to an element in a container.
@@ -176,38 +110,13 @@ struct IndexedRef {
     container_ref: ContainerRef,
 }
 *)
-Module IndexedRef.
-  Record t : Set := {
+Module IndexedRefSkeleton.
+  Record t {ValueImpl : Set} : Set := {
     idx : Z;
-    container_ref : ContainerRef.t;
+    container_ref : ContainerRefSkeleton.t ValueImpl;
   }.
-End IndexedRef.
-
-(* 
-/// An umbrella enum for references. It is used to hide the internals of the public type
-/// Reference.
-#[derive(Debug)]
-enum ReferenceImpl {
-    IndexedRef(IndexedRef),
-    ContainerRef(ContainerRef),
-}
-*)
-
-Module ReferenceImpl.
-  Inductive t : Set :=
-  | IndexedRef : IndexedRef.t -> t
-  | ContainerRef : ContainerRef.t -> t
-  .
-End ReferenceImpl.
-
-(* 
-/// A generic Move reference that offers two functionalities: read_ref & write_ref.
-#[derive(Debug)]
-pub struct Reference(ReferenceImpl);
-*)
-Module Reference.
-  Definition t := ReferenceImpl.t.
-End Reference.
+  Arguments t : clear implicits.
+End IndexedRefSkeleton.
 
 (* 
 enum ValueImpl {
@@ -239,12 +148,231 @@ Module ValueImpl.
   | U256 : Z -> t
   | Bool : bool -> t
   | Address : AccountAddress.t -> t
-  | Container : Container.t -> t
-  | ContainerRef : ContainerRef.t -> t
-  | IndexedRef : IndexedRef.t -> t
+  | Container : ContainerSkeleton.t t -> t
+  | ContainerRef : ContainerRefSkeleton.t t -> t
+  | IndexedRef : IndexedRefSkeleton.t t -> t
   .
 End ValueImpl.
 
+Module Container.
+  Definition t : Set := ContainerSkeleton.t ValueImpl.t.
+End Container.
+
+Module ContainerRef.
+  Definition t : Set := ContainerRefSkeleton.t ValueImpl.t.
+End ContainerRef.
+
+Module IndexedRef.
+  Definition t : Set := IndexedRefSkeleton.t ValueImpl.t.
+End IndexedRef.
+
+(* 
+/// An umbrella enum for references. It is used to hide the internals of the public type
+/// Reference.
+#[derive(Debug)]
+enum ReferenceImpl {
+    IndexedRef(IndexedRef),
+    ContainerRef(ContainerRef),
+}
+*)
+Module ReferenceImpl.
+  Inductive t : Set :=
+  | IndexedRef : IndexedRef.t -> t
+  | ContainerRef : ContainerRef.t -> t
+  .
+End ReferenceImpl.
+
+(* 
+/// A generic Move reference that offers two functionalities: read_ref & write_ref.
+#[derive(Debug)]
+pub struct Reference(ReferenceImpl);
+*)
+Module Reference.
+  Definition t := ReferenceImpl.t.
+End Reference.
+
+Module Impl_ContainerRef.
+  Definition Self : Set := ContainerRef.t.
+
+  (*
+  fn copy_value(&self) -> Self {
+        match self {
+            Self::Local(container) => Self::Local(container.copy_by_ref()),
+            Self::Global { status, container } => Self::Global {
+                status: Rc::clone(status),
+                container: container.copy_by_ref(),
+            },
+        }
+    }
+  *)
+  (* If we unroll the definition this is the identity function (ignoring the pointers) *)
+  Definition copy_value (self : Self) : Self :=
+    self.
+
+  (*
+  fn container(&self) -> &Container {
+      match self {
+          Self::Local(container) | Self::Global { container, .. } => container,
+      }
+  }
+  *)
+  Definition container (self : Self) : Container.t :=
+    match self with
+    | ContainerRefSkeleton.Local container
+    | ContainerRefSkeleton.Global_ {| ContainerRefSkeleton.Global_.container := container |} =>
+      container
+    end.
+End Impl_ContainerRef.
+
+Module Impl_IndexedRef.
+  Definition Self : Set := IndexedRef.t.
+
+  (*
+  fn copy_value(&self) -> Self {
+        Self {
+            idx: self.idx,
+            container_ref: self.container_ref.copy_value(),
+        }
+    }
+  *)
+  (* If we unroll the definition this is the identity function (ignoring the pointers) *)
+  Definition copy_value (self : Self) : Self :=
+    self.
+End Impl_IndexedRef.
+
+Module Impl_ValueImpl.
+  Definition Self : Set := ValueImpl.t.
+
+  (*
+  fn copy_value(&self) -> PartialVMResult<Self> {
+        use ValueImpl::*;
+
+        Ok(match self {
+            Invalid => Invalid,
+
+            U8(x) => U8( *x),
+            U16(x) => U16( *x),
+            U32(x) => U32( *x),
+            U64(x) => U64( *x),
+            U128(x) => U128( *x),
+            U256(x) => U256( *x),
+            Bool(x) => Bool( *x),
+            Address(x) => Address( *x),
+
+            ContainerRef(r) => ContainerRef(r.copy_value()),
+            IndexedRef(r) => IndexedRef(r.copy_value()),
+
+            // When cloning a container, we need to make sure we make a deep
+            // copy of the data instead of a shallow copy of the Rc.
+            Container(c) => Container(c.copy_value()?),
+        })
+    }
+  *)
+  Reserved Notation "'Container_copy_value".
+
+  Fixpoint copy_value (self : Self) : PartialVMResult.t Self :=
+    (* impl Container { *)
+    (*
+    fn copy_value(&self) -> PartialVMResult<Self> {
+        let copy_rc_ref_vec_val = |r: &Rc<RefCell<Vec<ValueImpl>>>| {
+            Ok(Rc::new(RefCell::new(
+                r.borrow()
+                    .iter()
+                    .map(|v| v.copy_value())
+                    .collect::<PartialVMResult<_>>()?,
+            )))
+        };
+
+        Ok(match self {
+            Self::Vec(r) => Self::Vec(copy_rc_ref_vec_val(r)?),
+            Self::Struct(r) => Self::Struct(copy_rc_ref_vec_val(r)?),
+
+            Self::VecU8(r) => Self::VecU8(Rc::new(RefCell::new(r.borrow().clone()))),
+            Self::VecU16(r) => Self::VecU16(Rc::new(RefCell::new(r.borrow().clone()))),
+            Self::VecU32(r) => Self::VecU32(Rc::new(RefCell::new(r.borrow().clone()))),
+            Self::VecU64(r) => Self::VecU64(Rc::new(RefCell::new(r.borrow().clone()))),
+            Self::VecU128(r) => Self::VecU128(Rc::new(RefCell::new(r.borrow().clone()))),
+            Self::VecU256(r) => Self::VecU256(Rc::new(RefCell::new(r.borrow().clone()))),
+            Self::VecBool(r) => Self::VecBool(Rc::new(RefCell::new(r.borrow().clone()))),
+            Self::VecAddress(r) => Self::VecAddress(Rc::new(RefCell::new(r.borrow().clone()))),
+
+            Self::Locals(_) => {
+                return Err(
+                    PartialVMError::new(StatusCode::UNKNOWN_INVARIANT_VIOLATION_ERROR)
+                        .with_message("cannot copy a Locals container".to_string()),
+                )
+            }
+        })
+    }
+    *)
+    (* let Container_copy_value (self : Container.t) : PartialVMResult.t Container.t :=
+      match self with
+      | ContainerSkeleton.Vec vec =>
+        let? vec := Result.map copy_value vec in
+        Result.Ok $ ContainerSkeleton.Vec vec
+      | ContainerSkeleton.Struct f =>
+        let? f := Result.map copy_value f in
+        Result.Ok $ ContainerSkeleton.Struct f
+      | ContainerSkeleton.VecU8 v => Result.Ok $ ContainerSkeleton.VecU8 v
+      | ContainerSkeleton.VecU64 v => Result.Ok $ ContainerSkeleton.VecU64 v
+      | ContainerSkeleton.VecU128 v => Result.Ok $ ContainerSkeleton.VecU128 v
+      | ContainerSkeleton.VecBool v => Result.Ok $ ContainerSkeleton.VecBool v
+      | ContainerSkeleton.VecAddress v => Result.Ok $ ContainerSkeleton.VecAddress v
+      | ContainerSkeleton.VecU16 v => Result.Ok $ ContainerSkeleton.VecU16 v
+      | ContainerSkeleton.VecU32 v => Result.Ok $ ContainerSkeleton.VecU32 v
+      | ContainerSkeleton.VecU256 v => Result.Ok $ ContainerSkeleton.VecU256 v
+      | ContainerSkeleton.Locals _ =>
+        Result.Err $ PartialVMError.new StatusCode.UNKNOWN_INVARIANT_VIOLATION_ERROR
+      end in *)
+    match self with
+    | ValueImpl.Invalid => Result.Ok ValueImpl.Invalid
+    | ValueImpl.U8 x => Result.Ok $ ValueImpl.U8 x
+    | ValueImpl.U16 x => Result.Ok $ ValueImpl.U16 x
+    | ValueImpl.U32 x => Result.Ok $ ValueImpl.U32 x
+    | ValueImpl.U64 x => Result.Ok $ ValueImpl.U64 x
+    | ValueImpl.U128 x => Result.Ok $ ValueImpl.U128 x
+    | ValueImpl.U256 x => Result.Ok $ ValueImpl.U256 x
+    | ValueImpl.Bool x => Result.Ok $ ValueImpl.Bool x
+    | ValueImpl.Address x => Result.Ok $ ValueImpl.Address x
+    | ValueImpl.ContainerRef r =>
+      Result.Ok $ ValueImpl.ContainerRef (Impl_ContainerRef.copy_value r)
+    | ValueImpl.IndexedRef r =>
+      Result.Ok $ ValueImpl.IndexedRef (Impl_IndexedRef.copy_value r)
+    | ValueImpl.Container c =>
+      let? copy_value := 'Container_copy_value c in
+      Result.Ok $ ValueImpl.Container copy_value
+    end
+
+    where "'Container_copy_value" := (fun (self : Container.t) =>
+      match self with
+      | ContainerSkeleton.Vec vec =>
+        let? vec := Result.map copy_value vec in
+        Result.Ok $ ContainerSkeleton.Vec vec
+      | ContainerSkeleton.Struct f =>
+        let? f := Result.map copy_value f in
+        Result.Ok $ ContainerSkeleton.Struct f
+      | ContainerSkeleton.VecU8 v => Result.Ok $ ContainerSkeleton.VecU8 v
+      | ContainerSkeleton.VecU64 v => Result.Ok $ ContainerSkeleton.VecU64 v
+      | ContainerSkeleton.VecU128 v => Result.Ok $ ContainerSkeleton.VecU128 v
+      | ContainerSkeleton.VecBool v => Result.Ok $ ContainerSkeleton.VecBool v
+      | ContainerSkeleton.VecAddress v => Result.Ok $ ContainerSkeleton.VecAddress v
+      | ContainerSkeleton.VecU16 v => Result.Ok $ ContainerSkeleton.VecU16 v
+      | ContainerSkeleton.VecU32 v => Result.Ok $ ContainerSkeleton.VecU32 v
+      | ContainerSkeleton.VecU256 v => Result.Ok $ ContainerSkeleton.VecU256 v
+      | ContainerSkeleton.Locals _ =>
+        Result.Err $ PartialVMError.new StatusCode.UNKNOWN_INVARIANT_VIOLATION_ERROR
+      end
+    ).
+
+  Definition Container_copy_value := 'Container_copy_value.
+End Impl_ValueImpl.
+
+Module Impl_Container.
+  Definition Self : Set := Container.t.
+
+  Definition copy_value : Self -> PartialVMResult.t Self := Impl_ValueImpl.Container_copy_value.
+End Impl_Container.
+
 (* 
 pub trait VMValueCast<T> {
   fn cast(self) -> PartialVMResult<T>;
@@ -260,6 +388,7 @@ End VMValueCast.
 (* pub struct Value(ValueImpl); *)
 Module Value.
   Definition t : Set := ValueImpl.t.
+  Arguments t /.
 
   (* 
   NOTE: We just roughly implement it as a collection of functions since it's also performance-wise nice. 
@@ -499,107 +628,132 @@ Module Impl_Value.
   Parameter deserialize_constant : Constant.t -> option Value.t.
 End Impl_Value.
 
-(*
-impl ContainerRef {
-    fn read_ref(self) -> PartialVMResult<Value> {
-        Ok(Value(ValueImpl::Container(self.container().copy_value()?)))
-    }
-}
-*)
-
-(*
-impl ContainerRef {
-    fn write_ref(self, v: Value) -> PartialVMResult<()> {
-        match v.0 {
-            ValueImpl::Container(c) => {
-                macro_rules! assign {
-                    ($r1: expr, $tc: ident) => {{
-                        let r = match c {
-                            Container::$tc(v) => v,
-                            _ => {
-                                return Err(PartialVMError::new(
-                                    StatusCode::UNKNOWN_INVARIANT_VIOLATION_ERROR,
-                                )
-                                .with_message(
-                                    "failed to write_ref: container type mismatch".to_string(),
-                                ))
-                            }
-                        };
-                        *$r1.borrow_mut() = take_unique_ownership(r)?;
-                    }};
-                }
-
-                match self.container() {
-                    Container::Struct(r) => assign!(r, Struct),
-                    Container::Vec(r) => assign!(r, Vec),
-                    Container::VecU8(r) => assign!(r, VecU8),
-                    Container::VecU16(r) => assign!(r, VecU16),
-                    Container::VecU32(r) => assign!(r, VecU32),
-                    Container::VecU64(r) => assign!(r, VecU64),
-                    Container::VecU128(r) => assign!(r, VecU128),
-                    Container::VecU256(r) => assign!(r, VecU256),
-                    Container::VecBool(r) => assign!(r, VecBool),
-                    Container::VecAddress(r) => assign!(r, VecAddress),
-                    Container::Locals(_) => {
-                        return Err(PartialVMError::new(
-                            StatusCode::UNKNOWN_INVARIANT_VIOLATION_ERROR,
-                        )
-                        .with_message("cannot overwrite Container::Locals".to_string()))
-                    }
-                }
-                self.mark_dirty();
-            }
-            _ => {
-                return Err(
-                    PartialVMError::new(StatusCode::UNKNOWN_INVARIANT_VIOLATION_ERROR)
-                        .with_message(format!(
-                            "cannot write value {:?} to container ref {:?}",
-                            v, self
-                        )),
-                )
-            }
-        }
-        Ok(())
-    }
-}
-*)
-
-Module Impl_ContainerRef.
+Module Impl_ContainerRef'.
   Definition Self := ContainerRef.t.
 
+  (*
+  fn read_ref(self) -> PartialVMResult<Value> {
+      Ok(Value(ValueImpl::Container(self.container().copy_value()?)))
+  }
+  *)
   Definition read_ref (self : Self) : PartialVMResult.t Value.t :=
-    let? copy_value := Container.copy_value (ContainerRef.container self) in
+    let? copy_value := Impl_Container.copy_value (Impl_ContainerRef.container self) in
     Result.Ok $ ValueImpl.Container copy_value.
 
+  (*
+  fn write_ref(self, v: Value) -> PartialVMResult<()> {
+    match v.0 {
+        ValueImpl::Container(c) => {
+            macro_rules! assign {
+                ($r1: expr, $tc: ident) => {{
+                    let r = match c {
+                        Container::$tc(v) => v,
+                        _ => {
+                            return Err(PartialVMError::new(
+                                StatusCode::UNKNOWN_INVARIANT_VIOLATION_ERROR,
+                            )
+                            .with_message(
+                              "failed to write_ref: container type mismatch".to_string(),
+                              ))
+                          }
+                      };
+                      *$r1.borrow_mut() = take_unique_ownership(r)?;
+                  }};
+              }
+
+              match self.container() {
+                  Container::Struct(r) => assign!(r, Struct),
+                  Container::Vec(r) => assign!(r, Vec),
+                  Container::VecU8(r) => assign!(r, VecU8),
+                  Container::VecU16(r) => assign!(r, VecU16),
+                  Container::VecU32(r) => assign!(r, VecU32),
+                  Container::VecU64(r) => assign!(r, VecU64),
+                  Container::VecU128(r) => assign!(r, VecU128),
+                  Container::VecU256(r) => assign!(r, VecU256),
+                  Container::VecBool(r) => assign!(r, VecBool),
+                  Container::VecAddress(r) => assign!(r, VecAddress),
+                  Container::Locals(_) => {
+                      return Err(PartialVMError::new(
+                          StatusCode::UNKNOWN_INVARIANT_VIOLATION_ERROR,
+                      )
+                      .with_message("cannot overwrite Container::Locals".to_string()))
+                  }
+              }
+              self.mark_dirty();
+          }
+          _ => {
+              return Err(
+                  PartialVMError::new(StatusCode::UNKNOWN_INVARIANT_VIOLATION_ERROR)
+                      .with_message(format!(
+                          "cannot write value {:?} to container ref {:?}",
+                          v, self
+                      )),
+              )
+          }
+      }
+      Ok(())
+  }
+  *)
   Definition write_ref (self : Self) (v : Value.t) : PartialVMResult.t unit. Admitted.
+End Impl_ContainerRef'.
 
-End Impl_ContainerRef.
+Module Impl_IndexedRef'.
+  Definition Self := IndexedRef.t.
 
-(*
-impl IndexedRef {
-    fn read_ref(self) -> PartialVMResult<Value> {
-        use Container::*;
-
-        let res = match self.container_ref.container() {
-            Locals(r) | Vec(r) | Struct(r) => r.borrow()[self.idx].copy_value()?,
-            VecU8(r) => ValueImpl::U8(r.borrow()[self.idx]),
-            VecU16(r) => ValueImpl::U16(r.borrow()[self.idx]),
-            VecU32(r) => ValueImpl::U32(r.borrow()[self.idx]),
-            VecU64(r) => ValueImpl::U64(r.borrow()[self.idx]),
-            VecU128(r) => ValueImpl::U128(r.borrow()[self.idx]),
-            VecU256(r) => ValueImpl::U256(r.borrow()[self.idx]),
-            VecBool(r) => ValueImpl::Bool(r.borrow()[self.idx]),
-            VecAddress(r) => ValueImpl::Address(r.borrow()[self.idx]),
-        };
+  (*
+  fn read_ref(self) -> PartialVMResult<Value> {
+      use Container::*;
+
+      let res = match self.container_ref.container() {
+          Locals(r) | Vec(r) | Struct(r) => r.borrow()[self.idx].copy_value()?,
+          VecU8(r) => ValueImpl::U8(r.borrow()[self.idx]),
+          VecU16(r) => ValueImpl::U16(r.borrow()[self.idx]),
+          VecU32(r) => ValueImpl::U32(r.borrow()[self.idx]),
+          VecU64(r) => ValueImpl::U64(r.borrow()[self.idx]),
+          VecU128(r) => ValueImpl::U128(r.borrow()[self.idx]),
+          VecU256(r) => ValueImpl::U256(r.borrow()[self.idx]),
+          VecBool(r) => ValueImpl::Bool(r.borrow()[self.idx]),
+          VecAddress(r) => ValueImpl::Address(r.borrow()[self.idx]),
+      };
 
-        Ok(Value(res))
-    }
-}
-*)
+      Ok(Value(res))
+  }
+  *)
+  Definition read_ref (self : Self) : M! (PartialVMResult.t Value.t) :=
+    match Impl_ContainerRef.container self.(IndexedRefSkeleton.container_ref) with
+    | ContainerSkeleton.Locals r
+    | ContainerSkeleton.Vec r
+    | ContainerSkeleton.Struct r =>
+      let! v := Panic.List.nth r (Z.to_nat self.(IndexedRefSkeleton.idx)) in
+      return! $ Impl_ValueImpl.copy_value v
+    | ContainerSkeleton.VecU8 r =>
+      let! v := Panic.List.nth r (Z.to_nat self.(IndexedRefSkeleton.idx)) in
+      return!? $ ValueImpl.U8 v
+    | ContainerSkeleton.VecU16 r =>
+      let! v := Panic.List.nth r (Z.to_nat self.(IndexedRefSkeleton.idx)) in
+      return!? $ ValueImpl.U16 v
+    | ContainerSkeleton.VecU32 r =>
+      let! v := Panic.List.nth r (Z.to_nat self.(IndexedRefSkeleton.idx)) in
+      return!? $ ValueImpl.U32 v
+    | ContainerSkeleton.VecU64 r =>
+      let! v := Panic.List.nth r (Z.to_nat self.(IndexedRefSkeleton.idx)) in
+      return!? $ ValueImpl.U64 v
+    | ContainerSkeleton.VecU128 r =>
+      let! v := Panic.List.nth r (Z.to_nat self.(IndexedRefSkeleton.idx)) in
+      return!? $ ValueImpl.U128 v
+    | ContainerSkeleton.VecU256 r =>
+      let! v := Panic.List.nth r (Z.to_nat self.(IndexedRefSkeleton.idx)) in
+      return!? $ ValueImpl.U256 v
+    | ContainerSkeleton.VecBool r =>
+      let! v := Panic.List.nth r (Z.to_nat self.(IndexedRefSkeleton.idx)) in
+      return!? $ ValueImpl.Bool v
+    | ContainerSkeleton.VecAddress r =>
+      let! v := Panic.List.nth r (Z.to_nat self.(IndexedRefSkeleton.idx)) in
+      return!? $ ValueImpl.Address v
+    end.
 
-(*
-impl IndexedRef {
-    fn write_ref(self, x: Value) -> PartialVMResult<()> {
+  (*
+  fn write_ref(self, x: Value) -> PartialVMResult<()> {
         match &x.0 {
             ValueImpl::IndexedRef(_)
             | ValueImpl::ContainerRef(_)
@@ -608,109 +762,80 @@ impl IndexedRef {
                 return Err(
                     PartialVMError::new(StatusCode::UNKNOWN_INVARIANT_VIOLATION_ERROR)
                         .with_message(format!(
-                            "cannot write value {:?} to indexed ref {:?}",
-                            x, self
-                        )),
-                )
-            }
-            _ => (),
-        }
-
-        match (self.container_ref.container(), &x.0) {
-            (Container::Locals(r), _) | (Container::Vec(r), _) | (Container::Struct(r), _) => {
-                let mut v = r.borrow_mut();
-                v[self.idx] = x.0;
-            }
-            (Container::VecU8(r), ValueImpl::U8(x)) => r.borrow_mut()[self.idx] = *x,
-            (Container::VecU16(r), ValueImpl::U16(x)) => r.borrow_mut()[self.idx] = *x,
-            (Container::VecU32(r), ValueImpl::U32(x)) => r.borrow_mut()[self.idx] = *x,
-            (Container::VecU64(r), ValueImpl::U64(x)) => r.borrow_mut()[self.idx] = *x,
-            (Container::VecU128(r), ValueImpl::U128(x)) => r.borrow_mut()[self.idx] = *x,
-            (Container::VecU256(r), ValueImpl::U256(x)) => r.borrow_mut()[self.idx] = *x,
-            (Container::VecBool(r), ValueImpl::Bool(x)) => r.borrow_mut()[self.idx] = *x,
-            (Container::VecAddress(r), ValueImpl::Address(x)) => r.borrow_mut()[self.idx] = *x,
-
-            (Container::VecU8(_), _)
-            | (Container::VecU16(_), _)
-            | (Container::VecU32(_), _)
-            | (Container::VecU64(_), _)
-            | (Container::VecU128(_), _)
-            | (Container::VecU256(_), _)
-            | (Container::VecBool(_), _)
-            | (Container::VecAddress(_), _) => {
-                return Err(
-                    PartialVMError::new(StatusCode::INTERNAL_TYPE_ERROR).with_message(format!(
-                        "cannot write value {:?} to indexed ref {:?}",
-                        x, self
-                    )),
-                )
-            }
-        }
-        self.container_ref.mark_dirty();
-        Ok(())
-    }
-}
-*)
-
-Module Impl_IndexedRef.
-  Definition Self := IndexedRef.t.
-
-  Definition default_address : AccountAddress.t. Admitted.
-
-  Definition read_ref (self : Self) : PartialVMResult.t Value.t :=
-    let idx := Z.to_nat self.(IndexedRef.idx) in
-    let container := ContainerRef.container self.(IndexedRef.container_ref) in
-    match container with
-    | Container.VecBool r => Result.Ok $ ValueImpl.Bool (List.nth idx r false)
-    | Container.VecAddress r => Result.Ok $ ValueImpl.Address (List.nth idx r default_address)
-    | _ => match container with
-           | Container.VecU8 r => Result.Ok $ ValueImpl.U8 (List.nth idx r 0)
-           | Container.VecU16 r => Result.Ok $ ValueImpl.U16 (List.nth idx r 0)
-           | Container.VecU32 r => Result.Ok $ ValueImpl.U32 (List.nth idx r 0)
-           | Container.VecU64 r => Result.Ok $ ValueImpl.U64 (List.nth idx r 0)
-           | Container.VecU128 r => Result.Ok $ ValueImpl.U128 (List.nth idx r 0)
-           | Container.VecU256 r => Result.Ok $ ValueImpl.U256 (List.nth idx r 0)
-           | _ => Result.Err $ PartialVMError.new StatusCode.UNKNOWN_INVARIANT_VIOLATION_ERROR
-           end
-    end.
+                          "cannot write value {:?} to indexed ref {:?}",
+                          x, self
+                      )),
+              )
+          }
+          _ => (),
+      }
 
+      match (self.container_ref.container(), &x.0) {
+          (Container::Locals(r), _) | (Container::Vec(r), _) | (Container::Struct(r), _) => {
+              let mut v = r.borrow_mut();
+              v[self.idx] = x.0;
+          }
+          (Container::VecU8(r), ValueImpl::U8(x)) => r.borrow_mut()[self.idx] = *x,
+          (Container::VecU16(r), ValueImpl::U16(x)) => r.borrow_mut()[self.idx] = *x,
+          (Container::VecU32(r), ValueImpl::U32(x)) => r.borrow_mut()[self.idx] = *x,
+          (Container::VecU64(r), ValueImpl::U64(x)) => r.borrow_mut()[self.idx] = *x,
+          (Container::VecU128(r), ValueImpl::U128(x)) => r.borrow_mut()[self.idx] = *x,
+          (Container::VecU256(r), ValueImpl::U256(x)) => r.borrow_mut()[self.idx] = *x,
+          (Container::VecBool(r), ValueImpl::Bool(x)) => r.borrow_mut()[self.idx] = *x,
+          (Container::VecAddress(r), ValueImpl::Address(x)) => r.borrow_mut()[self.idx] = *x,
+
+          (Container::VecU8(_), _)
+          | (Container::VecU16(_), _)
+          | (Container::VecU32(_), _)
+          | (Container::VecU64(_), _)
+          | (Container::VecU128(_), _)
+          | (Container::VecU256(_), _)
+          | (Container::VecBool(_), _)
+          | (Container::VecAddress(_), _) => {
+              return Err(
+                  PartialVMError::new(StatusCode::INTERNAL_TYPE_ERROR).with_message(format!(
+                      "cannot write value {:?} to indexed ref {:?}",
+                      x, self
+                  )),
+              )
+          }
+      }
+      self.container_ref.mark_dirty();
+      Ok(())
+  }
+  *)
   Definition write_ref (self : Self) (x : Value.t) : PartialVMResult.t unit. Admitted.
-
-End Impl_IndexedRef.
-
-(*
-impl ReferenceImpl {
-    fn read_ref(self) -> PartialVMResult<Value> {
-        match self {
-            Self::ContainerRef(r) => r.read_ref(),
-            Self::IndexedRef(r) => r.read_ref(),
-        }
-    }
-}
-
-impl ReferenceImpl {
-    fn write_ref(self, x: Value) -> PartialVMResult<()> {
-        match self {
-            Self::ContainerRef(r) => r.write_ref(x),
-            Self::IndexedRef(r) => r.write_ref(x),
-        }
-    }
-}
-*)
+End Impl_IndexedRef'.
 
 Module Impl_ReferenceImpl.
   Definition Self := ReferenceImpl.t.
 
-  Definition read_ref (self : Self) : PartialVMResult.t Value.t :=
+  (*
+  fn read_ref(self) -> PartialVMResult<Value> {
+      match self {
+          Self::ContainerRef(r) => r.read_ref(),
+          Self::IndexedRef(r) => r.read_ref(),
+      }
+  }
+  *)
+  Definition read_ref (self : Self) : M! (PartialVMResult.t Value.t) :=
     match self with
-    | ReferenceImpl.ContainerRef r => Impl_ContainerRef.read_ref r
-    | ReferenceImpl.IndexedRef r => Impl_IndexedRef.read_ref r
+    | ReferenceImpl.ContainerRef r => return! $ Impl_ContainerRef'.read_ref r
+    | ReferenceImpl.IndexedRef r => Impl_IndexedRef'.read_ref r
     end.
 
+  (*
+  fn write_ref(self, x: Value) -> PartialVMResult<()> {
+      match self {
+          Self::ContainerRef(r) => r.write_ref(x),
+          Self::IndexedRef(r) => r.write_ref(x),
+      }
+  }
+  *)
   Definition write_ref (self : Self) (x : Value.t) : PartialVMResult.t unit :=
     match self with
-    | ReferenceImpl.ContainerRef r => Impl_ContainerRef.write_ref r x
-    | ReferenceImpl.IndexedRef r => Impl_IndexedRef.write_ref r x
+    | ReferenceImpl.ContainerRef r => Impl_ContainerRef'.write_ref r x
+    | ReferenceImpl.IndexedRef r => Impl_IndexedRef'.write_ref r x
     end.
 End Impl_ReferenceImpl.
 
@@ -786,8 +911,6 @@ End Locals.
 Module Impl_Locals.
   Definition Self := move_sui.simulations.move_vm_types.values.values_impl.Locals.t.
 
-  Definition default_valueimpl := ValueImpl.Invalid.
-
   (* 
   pub fn copy_loc(&self, idx: usize) -> PartialVMResult<Value> {
       let v = self.0.borrow();
@@ -806,18 +929,12 @@ Module Impl_Locals.
   }
   *)
   Definition copy_loc (self : Self) (idx : Z) : PartialVMResult.t Value.t :=
-    (* idx is out of range, which is the 3rd case for the match clause *)
-    if Z.of_nat $ List.length self <=? idx
-    then Result.Err $ PartialVMError.new
-      StatusCode.VERIFIER_INVARIANT_VIOLATION
-    else
-    (* Now we deal with the former 2 cases *)
-      let v := List.nth (Z.to_nat idx) self default_valueimpl in
-      match v with
-      | ValueImpl.Invalid => Result.Err $ PartialVMError.new
-        StatusCode.UNKNOWN_INVARIANT_VIOLATION_ERROR
-      | _ => Result.Ok $ v
-      end.
+    match List.nth_error self (Z.to_nat idx) with
+    | Some ValueImpl.Invalid =>
+      Result.Err $ PartialVMError.new StatusCode.UNKNOWN_INVARIANT_VIOLATION_ERROR
+    | Some v => Impl_ValueImpl.copy_value v
+    | None => Result.Err $ PartialVMError.new StatusCode.VERIFIER_INVARIANT_VIOLATION
+    end.
 
   (* 
   fn swap_loc(&mut self, idx: usize, x: Value, violation_check: bool) -> PartialVMResult<Value> {
diff --git a/CoqOfRust/simulations/M.v b/CoqOfRust/simulations/M.v
index c54bc5340..6239e07e2 100644
--- a/CoqOfRust/simulations/M.v
+++ b/CoqOfRust/simulations/M.v
@@ -21,6 +21,9 @@ Module Result.
   Definition fold_left {A B Error : Set} (init : A) (l : list B) (f : A -> B -> t A Error) :
       t A Error :=
     List.fold_left (fun acc x => bind acc (fun acc => f acc x)) l (return_ init).
+
+  Definition map {A B Error : Set} (f : A -> t B Error) (l : list A) : t (list B) Error :=
+    fold_left [] l (fun acc x => bind (f x) (fun y => return_ (y :: acc))).
 End Result.
 
 Module ResultNotations.
@@ -49,6 +52,7 @@ Module Panic.
 
   Definition return_ {A : Set} (value : A) : t A :=
     Value value.
+  Arguments return_ /.
 
   Definition panic {A Error : Set} (error : Error) : t A :=
     Panic (existS Error error).
@@ -66,6 +70,14 @@ Module Panic.
     List.fold_right
       (fun x acc => bind acc (fun acc => bind (f x) (fun x => return_ (x :: acc))))
       (return_ []) l.
+
+  Module List.
+    Definition nth {A : Set} (l : list A) (n : nat) : t A :=
+      match List.nth_error l n with
+      | Some value => return_ value
+      | None => panic "List.nth: index out of bounds"
+      end.
+  End List.
 End Panic.
 
 Module PanicNotations.

From 5008004f59dc0bf94cec4c9773b50f9cd7ea0bea Mon Sep 17 00:00:00 2001
From: Guillaume Claret <dev@clarus.me>
Date: Mon, 30 Dec 2024 11:02:36 +0100
Subject: [PATCH 4/4] move-sui: add more proofs

---
 .../proofs/move_binary_format/file_format.v   |  14 +-
 .../move_bytecode_verifier/type_safety.v      |  72 +--
 .../proofs/move_vm_runtime/interpreter.v      |  19 +-
 .../proofs/move_vm_types/values/values_impl.v |  58 +-
 .../move_vm_types/values/values_impl.v        |  32 +-
 CoqOfRust/what_we_do.md                       | 531 ++++++++++++++++++
 6 files changed, 651 insertions(+), 75 deletions(-)
 create mode 100644 CoqOfRust/what_we_do.md

diff --git a/CoqOfRust/move_sui/proofs/move_binary_format/file_format.v b/CoqOfRust/move_sui/proofs/move_binary_format/file_format.v
index 84ec9ca76..84a8a6e06 100644
--- a/CoqOfRust/move_sui/proofs/move_binary_format/file_format.v
+++ b/CoqOfRust/move_sui/proofs/move_binary_format/file_format.v
@@ -18,7 +18,7 @@ Module Constant.
     Definition t (x : Constant.t) : Prop :=
       match Impl_Value.deserialize_constant x with
       | None => False
-      | Some value => IsValueOfType.t value x.(Constant.type_)
+      | Some value => IsValueImplOfType.t value x.(Constant.type_)
       end.
   End Valid.
 End Constant.
@@ -127,12 +127,12 @@ Module Bytecode.
       | Bytecode.BrTrue _ => True
       | Bytecode.BrFalse _ => True
       | Bytecode.Branch _ => True
-      | Bytecode.LdU8 _ => True
-      | Bytecode.LdU16 _ => True
-      | Bytecode.LdU32 _ => True
-      | Bytecode.LdU64 _ => True
-      | Bytecode.LdU128 _ => True
-      | Bytecode.LdU256 _ => True
+      | Bytecode.LdU8 z => Integer.Valid.t IntegerKind.U8 z
+      | Bytecode.LdU16 z => Integer.Valid.t IntegerKind.U16 z
+      | Bytecode.LdU32 z => Integer.Valid.t IntegerKind.U32 z
+      | Bytecode.LdU64 z => Integer.Valid.t IntegerKind.U64 z
+      | Bytecode.LdU128 z => Integer.Valid.t IntegerKind.U128 z
+      | Bytecode.LdU256 z => 0 <= z < 2^256
       | Bytecode.CastU8 => True
       | Bytecode.CastU16 => True
       | Bytecode.CastU32 => True
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 eab526d12..e8fb22fec 100644
--- a/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
+++ b/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
@@ -21,9 +21,9 @@ Module TypeSafetyChecker.
   End Valid.
 End TypeSafetyChecker.
 
-Module IsValueOfType.
+Module IsValueImplOfType.
   Lemma value_of_bool (value : Value.t) (ty : SignatureToken.t)
-    (H_value : IsValueOfType.t value ty)
+    (H_value : IsValueImplOfType.t value ty)
     (* This is the form in which is appears in the proofs *)
     (H_ty : ty = SignatureToken.Bool) :
     exists b, value = ValueImpl.Bool b.
@@ -34,7 +34,7 @@ Module IsValueOfType.
   Qed.
 
   Lemma value_of_integer (value : Value.t) (ty : SignatureToken.t)
-      (H_value : IsValueOfType.t value ty)
+      (H_value : IsValueImplOfType.t value ty)
       (H_ty : SignatureToken.is_integer ty = true) :
     exists (integer_value : IntegerValue.t),
     value = IntegerValue.to_value_impl integer_value.
@@ -49,21 +49,21 @@ Module IsValueOfType.
         (now eexists (IntegerValue.U256 _))
       ).
   Qed.
-End IsValueOfType.
+End IsValueImplOfType.
 
 Module IsStackValueOfType.
   Definition t (stack : Stack.t) (abstract_stack : AbstractStack.t SignatureToken.t) : Prop :=
-    List.Forall2 IsValueOfType.t
+    List.Forall2 IsValueImplOfType.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) ->
+    List.Forall2 IsValueImplOfType.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).
+      IsValueImplOfType.t value operand_ty /\
+      List.Forall2 IsValueImplOfType.t stack' (AbstractStack.flatten stack_ty).
   Proof.
     sauto lq: on.
   Qed.
@@ -74,7 +74,7 @@ Module IsLocalsOfType.
     param_count : locals_ty.(type_safety.Locals.param_count) = 0;
     parameters : locals_ty.(type_safety.Locals.parameters) = {| Signature.a0 := [] |};
     locals :
-      List.Forall2 IsValueOfType.t
+      List.Forall2 IsValueImplOfType.t
         locals
         locals_ty.(type_safety.Locals.locals).(Signature.a0);
   }.
@@ -147,9 +147,9 @@ Ltac destruct_abstract_pop :=
     destruct_post H_check_pop
   end;
   match goal with
-  | H_interpreter : _ |- _ =>
-    destruct_post (IsStackValueOfType.pop _ _ _ H_interpreter);
-    clear H_interpreter
+  | H_of_type : _ |- _ =>
+    destruct_post (IsStackValueOfType.pop _ _ _ H_of_type);
+    clear H_of_type
   end.
 
 Ltac destruct_abstract_push :=
@@ -191,12 +191,12 @@ Ltac destruct_initial_if :=
   repeat (
     match goal with
     | H_value : _, H_ty : _ |- _ =>
-      destruct_post (IsValueOfType.value_of_bool _ _ H_value H_ty);
+      destruct_post (IsValueImplOfType.value_of_bool _ _ H_value H_ty);
       clear H_ty
     end ||
     match goal with
     | H_value : _, H_ty : _ |- _ =>
-      destruct_post (IsValueOfType.value_of_integer _ _ H_value H_ty);
+      destruct_post (IsValueImplOfType.value_of_integer _ _ H_value H_ty);
       clear H_ty
     end
   );
@@ -209,7 +209,7 @@ Lemma progress
     (type_safety_checker : TypeSafetyChecker.t)
     (H_instruction : Bytecode.Valid.t instruction)
     (H_type_safety_checker : TypeSafetyChecker.Valid.t type_safety_checker)
-    (H_interpreter : IsInterpreterContextOfType.t locals interpreter type_safety_checker)
+    (H_of_type : IsInterpreterContextOfType.t locals interpreter type_safety_checker)
     (H_resolver :
       resolver.(loader.Resolver.binary).(loader.BinaryType.compiled) =
       type_safety_checker.(TypeSafetyChecker.module)
@@ -251,7 +251,7 @@ Proof.
   destruct type_safety_checker as [module function_context locals_ty stack_ty]; cbn in *.
   destruct H_type_safety_checker as [H_module H_stack_ty]; cbn in *.
   destruct H_module as [H_constant_pool].
-  destruct H_interpreter as [H_locals_typing H_stack_typing].
+  destruct H_of_type as [H_locals_typing H_stack_typing].
   destruct instruction eqn:H_instruction_eq; cbn in *.
   { guard_instruction Bytecode.Pop.
     destruct_abstract_pop.
@@ -276,32 +276,38 @@ Proof.
   { guard_instruction (Bytecode.LdU8 z).
     destruct_abstract_push.
     step; cbn; [|easy].
-    sauto q: on.
+    constructor; cbn; try assumption.
+    sauto lq: on.
   }
   { guard_instruction (Bytecode.LdU16 z).
     destruct_abstract_push.
     step; cbn; [|easy].
-    sauto q: on.
+    constructor; cbn; try assumption.
+    sauto lq: on.
   }
   { guard_instruction (Bytecode.LdU32 z).
     destruct_abstract_push.
     step; cbn; [|easy].
-    sauto q: on.
+    constructor; cbn; try assumption.
+    sauto lq: on.
   }
   { guard_instruction (Bytecode.LdU64 z).
     destruct_abstract_push.
     step; cbn; [|easy].
-    sauto q: on.
+    constructor; cbn; try assumption.
+    sauto lq: on.
   }
   { guard_instruction (Bytecode.LdU128 z).
     destruct_abstract_push.
     step; cbn; [|easy].
-    sauto q: on.
+    constructor; cbn; try assumption.
+    sauto lq: on.
   }
   { guard_instruction (Bytecode.LdU256 z).
     destruct_abstract_push.
     step; cbn; [|easy].
-    sauto q: on.
+    constructor; cbn; try assumption.
+    sauto lq: on.
   }
   { guard_instruction Bytecode.CastU8.
     destruct_abstract_pop.
@@ -309,7 +315,7 @@ Proof.
     destruct_abstract_push.
     step; cbn; (try easy); (try now destruct operand_ty);
       repeat (step; cbn; try easy);
-      constructor; cbn;
+      constructor; cbn; try assumption;
       sauto lq: on.
   }
   { guard_instruction Bytecode.CastU16.
@@ -409,18 +415,14 @@ Proof.
     pose proof List.Forall2_nth_error _ locals locals_ty (Z.to_nat z) H_locals as H_nth_error.
     unfold Value.t in H_nth_error.
     destruct (List.nth_error locals) as [local|] eqn:H_nth_error_eq; cbn.
-    { destruct local eqn:H_local_eq; cbn.
-      { admit. }
-      all: try (
-        step; cbn; try easy;
-        constructor; cbn; [hauto l: on|];
-        match goal with
-        | H : _ = _ |- _ => rewrite H
-        end;
-        constructor; try assumption;
-        destruct (List.nth_error locals_ty); try easy;
-        hauto lq: on
-      ).
+    { match goal with
+      | |- context[if ?is_local_expr then _ else _] =>
+        set (is_local := is_local_expr)
+      end.
+      destruct is_local eqn:H_is_invalid_eq; cbn.
+      { destruct local eqn:H_local_eq; try easy.
+        now destruct List.nth_error in H_nth_error.
+      }
       { admit. }
     }
     { now destruct (List.nth_error locals_ty). }
diff --git a/CoqOfRust/move_sui/proofs/move_vm_runtime/interpreter.v b/CoqOfRust/move_sui/proofs/move_vm_runtime/interpreter.v
index dc353a14e..ef35511fd 100644
--- a/CoqOfRust/move_sui/proofs/move_vm_runtime/interpreter.v
+++ b/CoqOfRust/move_sui/proofs/move_vm_runtime/interpreter.v
@@ -1,5 +1,18 @@
 Require Import CoqOfRust.CoqOfRust.
+Require Import move_sui.simulations.move_vm_runtime.interpreter.
 
-Module Impl_Interpreter.
-  
-End Impl_Interpreter.
+Module Stack.
+  Module Valid.
+    Record t (x : Stack.t) : Prop := {
+      valid : True;
+    }.
+  End Valid.
+End Stack.
+
+Module Interpreter.
+  Module Valid.
+    Record t (x : Interpreter.t) : Prop := {
+      operand_stack : Stack.Valid.t x.(Interpreter.operand_stack);
+    }.
+  End Valid.
+End Interpreter.
diff --git a/CoqOfRust/move_sui/proofs/move_vm_types/values/values_impl.v b/CoqOfRust/move_sui/proofs/move_vm_types/values/values_impl.v
index 9d928abcb..d7ed790f9 100644
--- a/CoqOfRust/move_sui/proofs/move_vm_types/values/values_impl.v
+++ b/CoqOfRust/move_sui/proofs/move_vm_types/values/values_impl.v
@@ -5,19 +5,61 @@ Require Import CoqOfRust.lib.proofs.lib.
 Require Import move_sui.simulations.move_binary_format.file_format.
 Require Import move_sui.simulations.move_vm_types.values.values_impl.
 
-Module IsValueOfType.
+Import simulations.M.Notations.
+
+Module ContainerSkeleton.
+  Module IsWithoutLocals.
+    Inductive t {ValueImpl : Set} (P : ValueImpl -> Prop) : ContainerSkeleton.t ValueImpl -> Prop :=
+    | Vec vec : List.Forall P vec -> t P (ContainerSkeleton.Vec vec)
+    | Struct f : List.Forall P f -> t P (ContainerSkeleton.Struct f)
+    | VecU8 vec : t P (ContainerSkeleton.VecU8 vec)
+    | VecU64 vec : t P (ContainerSkeleton.VecU64 vec)
+    | VecU128 vec : t P (ContainerSkeleton.VecU128 vec)
+    | VecBool vec : t P (ContainerSkeleton.VecBool vec)
+    | VecAddress vec : t P (ContainerSkeleton.VecAddress vec)
+    | VecU16 vec : t P (ContainerSkeleton.VecU16 vec)
+    | VecU32 vec : t P (ContainerSkeleton.VecU32 vec)
+    | VecU256 vec : t P (ContainerSkeleton.VecU256 vec).
+  End IsWithoutLocals.
+End ContainerSkeleton.
+
+Module ValueImpl.
+  Module IsWithoutLocals.
+    Inductive t : ValueImpl.t -> Prop :=
+    | Invalid : t ValueImpl.Invalid
+    | U8 z : t (ValueImpl.U8 z)
+    | U16 z : t (ValueImpl.U16 z)
+    | U32 z : t (ValueImpl.U32 z)
+    | U64 z : t (ValueImpl.U64 z)
+    | U128 z : t (ValueImpl.U128 z)
+    | U256 z : t (ValueImpl.U256 z)
+    | Bool b : t (ValueImpl.Bool b)
+    | Address a : t (ValueImpl.Address a)
+    | ContainerRef r : t (ValueImpl.ContainerRef r)
+    | IndexedRef r : t (ValueImpl.IndexedRef r)
+    | Container c : ContainerSkeleton.IsWithoutLocals.t t c -> t (ValueImpl.Container c).
+  End IsWithoutLocals.
+End ValueImpl.
+
+Module IsValueImplOfType.
   Definition t (value : ValueImpl.t) (typ : SignatureToken.t) : Prop :=
     match value, typ with
     | ValueImpl.Invalid, _ => False
-    | ValueImpl.U8 _, SignatureToken.U8 => True
-    | ValueImpl.U16 _, SignatureToken.U16 => True
-    | ValueImpl.U32 _, SignatureToken.U32 => True
-    | ValueImpl.U64 _, SignatureToken.U64 => True
-    | ValueImpl.U128 _, SignatureToken.U128 => True
-    | ValueImpl.U256 _, SignatureToken.U256 => True
+    | ValueImpl.U8 z, SignatureToken.U8 => True
+    | ValueImpl.U16 z, SignatureToken.U16 => True
+    | ValueImpl.U32 z, SignatureToken.U32 => True
+    | ValueImpl.U64 z, SignatureToken.U64 => True
+    | ValueImpl.U128 z, SignatureToken.U128 => True
+    | ValueImpl.U256 z, SignatureToken.U256 => True
     | ValueImpl.Bool _, SignatureToken.Bool => True
     | ValueImpl.Address _, SignatureToken.Address => True
     (* TODO: other cases *)
     | _, _ => False
     end.
-End IsValueOfType.
+
+  Lemma invalid_has_no_type typ :
+    ~ IsValueImplOfType.t ValueImpl.Invalid typ.
+  Proof.
+    now destruct typ.
+  Qed.
+End IsValueImplOfType.
diff --git a/CoqOfRust/move_sui/simulations/move_vm_types/values/values_impl.v b/CoqOfRust/move_sui/simulations/move_vm_types/values/values_impl.v
index c0f37ccf5..193f3fe3d 100644
--- a/CoqOfRust/move_sui/simulations/move_vm_types/values/values_impl.v
+++ b/CoqOfRust/move_sui/simulations/move_vm_types/values/values_impl.v
@@ -305,25 +305,6 @@ Module Impl_ValueImpl.
         })
     }
     *)
-    (* let Container_copy_value (self : Container.t) : PartialVMResult.t Container.t :=
-      match self with
-      | ContainerSkeleton.Vec vec =>
-        let? vec := Result.map copy_value vec in
-        Result.Ok $ ContainerSkeleton.Vec vec
-      | ContainerSkeleton.Struct f =>
-        let? f := Result.map copy_value f in
-        Result.Ok $ ContainerSkeleton.Struct f
-      | ContainerSkeleton.VecU8 v => Result.Ok $ ContainerSkeleton.VecU8 v
-      | ContainerSkeleton.VecU64 v => Result.Ok $ ContainerSkeleton.VecU64 v
-      | ContainerSkeleton.VecU128 v => Result.Ok $ ContainerSkeleton.VecU128 v
-      | ContainerSkeleton.VecBool v => Result.Ok $ ContainerSkeleton.VecBool v
-      | ContainerSkeleton.VecAddress v => Result.Ok $ ContainerSkeleton.VecAddress v
-      | ContainerSkeleton.VecU16 v => Result.Ok $ ContainerSkeleton.VecU16 v
-      | ContainerSkeleton.VecU32 v => Result.Ok $ ContainerSkeleton.VecU32 v
-      | ContainerSkeleton.VecU256 v => Result.Ok $ ContainerSkeleton.VecU256 v
-      | ContainerSkeleton.Locals _ =>
-        Result.Err $ PartialVMError.new StatusCode.UNKNOWN_INVARIANT_VIOLATION_ERROR
-      end in *)
     match self with
     | ValueImpl.Invalid => Result.Ok ValueImpl.Invalid
     | ValueImpl.U8 x => Result.Ok $ ValueImpl.U8 x
@@ -930,9 +911,16 @@ Module Impl_Locals.
   *)
   Definition copy_loc (self : Self) (idx : Z) : PartialVMResult.t Value.t :=
     match List.nth_error self (Z.to_nat idx) with
-    | Some ValueImpl.Invalid =>
-      Result.Err $ PartialVMError.new StatusCode.UNKNOWN_INVARIANT_VIOLATION_ERROR
-    | Some v => Impl_ValueImpl.copy_value v
+    | Some value =>
+      let is_invalid :=
+        match value with
+        | ValueImpl.Invalid => true
+        | _ => false
+        end in
+      if is_invalid then
+        Result.Err $ PartialVMError.new StatusCode.UNKNOWN_INVARIANT_VIOLATION_ERROR
+      else
+        Impl_ValueImpl.copy_value value
     | None => Result.Err $ PartialVMError.new StatusCode.VERIFIER_INVARIANT_VIOLATION
     end.
 
diff --git a/CoqOfRust/what_we_do.md b/CoqOfRust/what_we_do.md
new file mode 100644
index 000000000..c1e2b7d21
--- /dev/null
+++ b/CoqOfRust/what_we_do.md
@@ -0,0 +1,531 @@
+# What We Do
+
+In this file we document how we specify and formally verify programs, following our flow. The idea is to later help LLM agents to do the same.
+
+## Task: Unblocking the `progress` lemma for the cast cases, by adding an additional hypothesis
+
+We are in the file move_sui/proofs/move_bytecode_verifier/type_safety.v The lemma `progress` is about verifying the type-checker of the Sui language, showing that for each instruction if we start from a state of a certain type, the new state generated by the interpreter is of the type generated by the type-checker. For error cases, if the type-checker succeeds then the interpreter also, except in a few cases which are explicitly mentioned: if there is a stack overflow or an arithmetic overflow. Indeed, these errors cannot be anticipated by the type-checker. The lemma is stated as follows (by reading its definition):
+
+```coq
+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_instruction : Bytecode.Valid.t instruction)
+    (H_type_safety_checker : TypeSafetyChecker.Valid.t type_safety_checker)
+    (H_interpreter : IsInterpreterContextOfType.t locals interpreter type_safety_checker)
+    (H_resolver :
+      resolver.(loader.Resolver.binary).(loader.BinaryType.compiled) =
+      type_safety_checker.(TypeSafetyChecker.module)
+    )
+    (* This lemma is not true for [Bytecode.Ret] *)
+    (H_not_Ret : instruction <> Bytecode.Ret) :
+  let state := {|
+    State.pc := pc;
+    State.locals := locals;
+    State.interpreter := interpreter;
+  |} in
+  match
+    verify_instr instruction pc type_safety_checker,
+    execute_instruction ty_args function resolver instruction state
+  with
+  | Panic.Value (Result.Ok _, type_safety_checker'),
+    Panic.Value (Result.Ok _, state') =>
+    let '{|
+      State.pc := _;
+      State.locals := locals';
+      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
+  | Panic.Panic _, _ | Panic.Value (Result.Err _, _), _ => True
+  end.
+```
+
+We have to show:
+
+```
+List.Forall2 IsValueImplOfType.t (ValueImpl.U8 z :: x0) (AbstractStack.flatten t)
+```
+
+On the left we have a stack of values, on the right a stack of types. On the left there is one element followed by the rest of the stack (`::`) and on the right any stack. We need both to be on the same form to reason with `List.Forall2`.
+
+We rewrite `t` with something more precise using a hypothesis in the context:
+
+```
+H_post3: AbstractStack.flatten t = SignatureToken.U8 :: AbstractStack.flatten stack_ty0
+```
+
+To avoid having to name this hypothesis with a generated name, we do:
+
+```
+match goal with
+| H : _ = _ |- _ =>
+  rewrite H; clear H
+end.
+```
+
+We get the goal:
+
+```
+List.Forall2 IsValueImplOfType.t (ValueImpl.U8 z :: x0) (SignatureToken.U8 :: AbstractStack.flatten stack_ty0)
+```
+
+By applying the `constructor` tactic we get to sub goals for each part of the list:
+
+```
+IsValueImplOfType.t (ValueImpl.U8 z) SignatureToken.U8
+```
+and
+```
+List.Forall2 IsValueImplOfType.t x0 (AbstractStack.flatten stack_ty0)
+```
+
+We enter in the first one with a curly brace. Tactic `best` does not work. We unfold the definition of the predicate with:
+
+```
+unfold IsValueImplOfType.t.
+```
+
+It says:
+
+```
+Integer.Valid.t IntegerKind.U8 z
+```
+
+meaning we need to show that `z` is in the bounds of a U8 integer. We do not think this is expected, as checking that a value has a certain type should not require checking the integer bounds. It should be enough to say that we have:
+
+```
+IsValueImplOfType.t (ValueImpl.U8 z) SignatureToken.U8
+```
+
+given that we have a value starting by `ValueImpl.U8`. We go to our definition of `IsValueImplOfType.t` that we find by `Locate IsValueImplOfType.t`:
+
+```
+Module IsValueImplOfType.
+  Definition t (value : ValueImpl.t) (typ : SignatureToken.t) : Prop :=
+    match value, typ with
+    | ValueImpl.Invalid, _ => False
+    | ValueImpl.U8 z, SignatureToken.U8 => Integer.Valid.t IntegerKind.U8 z
+    | ValueImpl.U16 z, SignatureToken.U16 => Integer.Valid.t IntegerKind.U16 z
+    | ValueImpl.U32 z, SignatureToken.U32 => Integer.Valid.t IntegerKind.U32 z
+    | ValueImpl.U64 z, SignatureToken.U64 => Integer.Valid.t IntegerKind.U64 z
+    | ValueImpl.U128 z, SignatureToken.U128 => Integer.Valid.t IntegerKind.U128 z
+    | ValueImpl.U256 z, SignatureToken.U256 => 0 <= z < 2^256
+    | ValueImpl.Bool _, SignatureToken.Bool => True
+    | ValueImpl.Address _, SignatureToken.Address => True
+    (* TODO: other cases *)
+    | _, _ => False
+    end.
+End IsValueImplOfType.
+```
+
+We remove the bounds on integers:
+
+```
+Module IsValueImplOfType.
+  Definition t (value : ValueImpl.t) (typ : SignatureToken.t) : Prop :=
+    match value, typ with
+    | ValueImpl.Invalid, _ => False
+    | ValueImpl.U8 z, SignatureToken.U8 => True
+    | ValueImpl.U16 z, SignatureToken.U16 => True
+    | ValueImpl.U32 z, SignatureToken.U32 => True
+    | ValueImpl.U64 z, SignatureToken.U64 => True
+    | ValueImpl.U128 z, SignatureToken.U128 => True
+    | ValueImpl.U256 z, SignatureToken.U256 => True
+    | ValueImpl.Bool _, SignatureToken.Bool => True
+    | ValueImpl.Address _, SignatureToken.Address => True
+    (* TODO: other cases *)
+    | _, _ => False
+    end.
+End IsValueImplOfType.
+```
+
+We check that it compiles. We re-compile the project with `make` as this is a dependency of the file we are working on.
+
+Now a previous case is failing:
+
+```
+hauto l: on.
+```
+
+with:
+
+```
+Error: hauto failed
+```
+
+As this is a tactic generated by `best`, we try to use `best` again. It works! We continue and arrive at our current goal. Out of curiosity, we try `best` again. It works! The idea is that since we made weaker the definition of what we want to prove, maybe we can now solve it automatically.
+
+We have six cases which are solved by `best`:
+
+```
+{ best. }
+{ best. }
+{ best. }
+{ best. }
+{ best. }
+{ best. }
+```
+
+We replace it by `; best` after the block of previous tactics:
+
+```
+step; cbn; (try easy); (try now destruct operand_ty);
+  repeat (step; cbn; try easy);
+  constructor; cbn; try assumption;
+  best.
+```
+
+It works! By running `make` again we get that we can replace the `best` by `
+
+So now we have done the `Bytecode.CastU8` case.
+
+## Continuing with the next instructions
+
+There are a lot of other cast instructions, such as `Bytecode.CastU16`. Before checking if what we have done for `Bytecode.CastU8` works for the other cases, we re-compile the project with `make`. It works, including proofs for the other casts that were already there and correct! We wonder why we had the bug then.
+
+We commit and go to the next `admit` in the proof.
+
+## Next admit: the CopyLoc instruction
+
+The next `admit` is for the instruction `Bytecode.CopyLoc`. The goal is:
+
+```
+False
+```
+
+This means that either we made something wrong, or that we must show a contradiction in the hypothesis.
+
+Something we can do is as follows: understanding how we arrived into such a `False` branch. Going back to the previous tactic, we see:
+
+```
+destruct local eqn:H_local_eq; cbn.
+```
+
+This is because in the goal we have:
+
+```
+match local with
+| ValueImpl.Invalid => Result.Err (PartialVMError.new StatusCode.UNKNOWN_INVARIANT_VIOLATION_ERROR)
+| _ => Impl_ValueImpl.copy_value local
+end
+```
+
+An issue with this `match` is that it hides more cases than it seems. When we destruct `local`, we get one case per constructor of the `ValueImpl.t` type, instead of just two.
+
+Here the code we are verifying is written by us as it is a simulation of the original one. Let us change it !
+
+We first need to find this `match` in the code. The code that is pretty-printed in the goal is not necessarily written as it is in the source. We still try a text search on the pattern:
+
+```
+| ValueImpl.Invalid =>
+```
+
+The results are not convincing. We try instead to search for:
+
+```
+UNKNOWN_INVARIANT_VIOLATION_ERROR
+```
+
+Too many results! Instead we think about how we came there. The first computations are about typing. If we go to the definition of the type-checker for the `CopyLoc` instruction we look for the function `verify_instr` and do not see anything convincing. We look at the interpreter instead:
+
+```
+let local := Impl_Locals.copy_loc state.(State.locals) idx in
+```
+
+In `copy_loc` we have:
+
+```
+Definition copy_loc (self : Self) (idx : Z) : PartialVMResult.t Value.t :=
+  match List.nth_error self (Z.to_nat idx) with
+  | Some ValueImpl.Invalid =>
+    Result.Err $ PartialVMError.new StatusCode.UNKNOWN_INVARIANT_VIOLATION_ERROR
+  | Some v => Impl_ValueImpl.copy_value v
+  | None => Result.Err $ PartialVMError.new StatusCode.VERIFIER_INVARIANT_VIOLATION
+  end.
+```
+
+This is what we are looking for! Let us rewrite it with less cases, using an equality check with an `if`:
+
+```
+Definition copy_loc (self : Self) (idx : Z) : PartialVMResult.t Value.t :=
+  match List.nth_error self (Z.to_nat idx) with
+  | Some value =>
+    let is_invalid :=
+      match value with
+      | ValueImpl.Invalid => true
+      | _ => false
+      end in
+    if is_invalid then
+      Result.Err $ PartialVMError.new StatusCode.UNKNOWN_INVARIANT_VIOLATION_ERROR
+    else
+      Impl_ValueImpl.copy_value value
+  | None => Result.Err $ PartialVMError.new StatusCode.VERIFIER_INVARIANT_VIOLATION
+  end.
+```
+
+This seems silly but now we will be able to destruct on a boolean instead of on the `ValueImpl.t` type. We re-compile the project with `make`.
+
+Going back to our previous point in the proof, just before the destruct of `local`, we replace it by:
+
+```
+match goal with
+| |- context[if ?is_local_expr then _ else _] =>
+  set (is_local := is_local_expr)
+end.
+destruct is_local; cbn.
+```
+
+We name the boolean condition with a `set` tactic to be explicit, and destruct it. We now have two sub goals instead of many similar one for the `_` pattern!
+
+The first sub goal is still `False`. Something special in the hypothesis that we see is:
+
+```
+H_nth_error:
+  match List.nth_error locals_ty (Z.to_nat z) with
+  | Some x2 => IsValueImplOfType.t local x2
+  | None => False
+  end
+```
+
+Can it be true? In some sense, if `local` is the invalid value, it cannot have a type. So both the case `Some` and `None` are impossible. Is it really what we want that an invalid value has no type? Let us assume that as this sounds reasonable. If this is not actually the case, we will be stuck in the proof later, if the interpreter can produce invalid values.
+
+Let us prove a lemma about that, to say that an invalid value cannot have a type. We put it just after the definition of `IsValueImplOfType.t`:
+
+```
+Lemma invalid_has_no_type typ :
+  ~ IsValueImplOfType.t ValueImpl.Invalid typ.
+```
+
+Note that we use `typ` as a direct parameter for the `Lemma` instead of a `forall` quantifier. This is our convention, to make the code shorter.
+
+We go into this lemma. The proof we be by case, for each possible `typ`. We start with:
+
+```
+destruct typ; cbn; try easy.
+```
+
+It works! We simplify with `now destruct typ` which is the equivalent of `destruct typ; easy`. We re-compile the project with `make`. We are back to our goal.
+
+We forgot to add that in the `False` case the condition `is_invalid` is true. We add it with:
+
+```
+destruct is_invalid eqn:H_is_invalid_eq; cbn.
+```
+
+We always name the equality hypothesis that was as a convention. Now we destruct the `local` variable again, generating many sub goals, but with a simpler resolution:
+
+```
+destruct local eqn:H_local_eq.
+```
+
+No `cbn` as there is nothing to reduce in the goal. We need to eliminate easily the cases where `local` is not invalid. We do:
+
+```
+destruct local eqn:H_local_eq; try easy.
+```
+
+Now we have:
+
+```
+match List.nth_error locals_ty (Z.to_nat z) with
+| Some x2 => IsValueImplOfType.t ValueImpl.Invalid x2
+| None => False
+end
+```
+
+We reason by cases on the `nth_error`:
+
+```
+destruct List.nth_error in H_nth_error; try easy.
+```
+
+We reaslize that all the cases succeed! This means we do not need the lemma we proved about invalid values not having a type. We still keep the lemma as it is still an important property to state explicitly.
+
+We replace the destruct by:
+
+```
+now destruct List.nth_error in H_nth_error.
+```
+
+Solved! We go to the next goal. It starts with:
+
+```
+match Impl_ValueImpl.copy_value local with
+```
+
+We go to the definition of `copy_value`: it is a complex mutually recursive definition! Maybe we can define a lemma about it. We go to the definition of `copy_value`:
+
+```
+Fixpoint copy_value (self : Self) : PartialVMResult.t Self :=
+  match self with
+  | ValueImpl.Invalid => Result.Ok ValueImpl.Invalid
+  | ValueImpl.U8 x => Result.Ok $ ValueImpl.U8 x
+  | ValueImpl.U16 x => Result.Ok $ ValueImpl.U16 x
+  | ValueImpl.U32 x => Result.Ok $ ValueImpl.U32 x
+  | ValueImpl.U64 x => Result.Ok $ ValueImpl.U64 x
+  | ValueImpl.U128 x => Result.Ok $ ValueImpl.U128 x
+  | ValueImpl.U256 x => Result.Ok $ ValueImpl.U256 x
+  | ValueImpl.Bool x => Result.Ok $ ValueImpl.Bool x
+  | ValueImpl.Address x => Result.Ok $ ValueImpl.Address x
+  | ValueImpl.ContainerRef r =>
+    Result.Ok $ ValueImpl.ContainerRef (Impl_ContainerRef.copy_value r)
+  | ValueImpl.IndexedRef r =>
+    Result.Ok $ ValueImpl.IndexedRef (Impl_IndexedRef.copy_value r)
+  | ValueImpl.Container c =>
+    let? copy_value := 'Container_copy_value c in
+    Result.Ok $ ValueImpl.Container copy_value
+  end
+
+  where "'Container_copy_value" := (fun (self : Container.t) =>
+    match self with
+    | ContainerSkeleton.Vec vec =>
+      let? vec := Result.map copy_value vec in
+      Result.Ok $ ContainerSkeleton.Vec vec
+    | ContainerSkeleton.Struct f =>
+      let? f := Result.map copy_value f in
+      Result.Ok $ ContainerSkeleton.Struct f
+    | ContainerSkeleton.VecU8 v => Result.Ok $ ContainerSkeleton.VecU8 v
+    | ContainerSkeleton.VecU64 v => Result.Ok $ ContainerSkeleton.VecU64 v
+    | ContainerSkeleton.VecU128 v => Result.Ok $ ContainerSkeleton.VecU128 v
+    | ContainerSkeleton.VecBool v => Result.Ok $ ContainerSkeleton.VecBool v
+    | ContainerSkeleton.VecAddress v => Result.Ok $ ContainerSkeleton.VecAddress v
+    | ContainerSkeleton.VecU16 v => Result.Ok $ ContainerSkeleton.VecU16 v
+    | ContainerSkeleton.VecU32 v => Result.Ok $ ContainerSkeleton.VecU32 v
+    | ContainerSkeleton.VecU256 v => Result.Ok $ ContainerSkeleton.VecU256 v
+    | ContainerSkeleton.Locals _ =>
+      Result.Err $ PartialVMError.new StatusCode.UNKNOWN_INVARIANT_VIOLATION_ERROR
+    end
+  ).
+```
+
+Which property can we prove about this function? We see that this is very often the identity function, except for the `Locals` case. Is that the case that we cannot have a container of locals? We go to the Rust code to investigate a bit. We name the Rocq files as in Rust. We search for the `Container` text and Ctrl-click to its definition:
+
+```
+/// A container is a collection of values. It is used to represent data structures like a
+/// Move vector or struct.
+///
+/// There is one general container that can be used to store an array of any values, same
+/// type or not, and a few specialized flavors to offer compact memory layout for small
+/// primitive types.
+///
+/// Except when not owned by the VM stack, a container always lives inside an Rc<RefCell<>>,
+/// making it possible to be shared by references.
+````
+
+We do not see anything in the comments about the `Locals` case. We look instead in the function making an error for locals, namely `copy_value`. We do not see any interesting comments either. So maybe this is because locals cannot contain other locals. Let us add this property!
+
+The locals are the set of local variables for the current function. There are disjoint from the values on the stack. So we need a predicate specifically for them. We add it is a `ValueImpl` module in a proof file with the same name as where `ValueImpl` is defined. The name of the file is move_sui/proofs/move_vm_types/values/values_impl.v We make a definition in a module:
+
+```
+Module ValueImpl.
+  Module IsWithoutLocals.
+    
+  End IsWithoutLocals.
+End ValueImpl.
+```
+
+to be namespaced. The definition of `ValueImpl.t` is a complex mutually recursive definition. We get inspiration from the definition of the `copy_value` function, as this is the one we will specify anyways. We start by its definition and add a resulting property for each of the branches:
+
+```
+Reserved Notation "'Container_t".
+
+Fixpoint t (self : ValueImpl.t) : Prop :=
+  match self with
+  | ValueImpl.Invalid => True
+  | ValueImpl.U8 _ => True
+  | ValueImpl.U16 _ => True
+  | ValueImpl.U32 _ => True
+  | ValueImpl.U64 _ => True
+  | ValueImpl.U128 _ => True
+  | ValueImpl.U256 _ => True
+  | ValueImpl.Bool _ => True
+  | ValueImpl.Address _ => True
+  | ValueImpl.ContainerRef r => ContainerRef.IsWithoutLocals.t r
+  | ValueImpl.IndexedRef r => IndexedRef.IsWithoutLocals.t r
+  | ValueImpl.Container c => 'Container_t c
+  end
+
+  where "'Container_t" := (fun (self : Container.t) =>
+    match self with
+    | ContainerSkeleton.Vec vec => List.Forall t vec
+    | ContainerSkeleton.Struct f => List.Forall t f
+    | ContainerSkeleton.VecU8 _ => True
+    | ContainerSkeleton.VecU64 _ => True
+    | ContainerSkeleton.VecU128 _ => True
+    | ContainerSkeleton.VecBool _ => True
+    | ContainerSkeleton.VecAddress _ => True
+    | ContainerSkeleton.VecU16 _ => True
+    | ContainerSkeleton.VecU32 _ => True
+    | ContainerSkeleton.VecU256 _ => True
+    | ContainerSkeleton.Locals _ => False
+    end
+  ).
+```
+
+It does not work!
+
+```
+Error: Recursive definition of t is ill-formed.
+In environment
+t : ValueImpl.t -> Prop
+self : ValueImpl.t
+c : ContainerSkeleton.t ValueImpl.t
+self0 := c : Container.t
+f : list ValueImpl.t
+Recursive call to t has not enough arguments.
+```
+
+This might be due to the `List.Forall` that is an inductive rather than a function. By commenting the corresponding cases it works! We need to design a new definition, using an inductive instead.
+
+Our direct attempt at using an Inductive results in an error "impossible: strictly positive occurrence of t".
+
+Instead, the solution that works is to follow the inductives defining the type. We get the following definition:
+
+```
+Module ContainerSkeleton.
+  Module IsWithoutLocals.
+    Inductive t {ValueImpl : Set} (P : ValueImpl -> Prop) : ContainerSkeleton.t ValueImpl -> Prop :=
+    | Vec vec : List.Forall P vec -> t P (ContainerSkeleton.Vec vec)
+    | Struct f : List.Forall P f -> t P (ContainerSkeleton.Struct f)
+    | VecU8 vec : t P (ContainerSkeleton.VecU8 vec)
+    | VecU64 vec : t P (ContainerSkeleton.VecU64 vec)
+    | VecU128 vec : t P (ContainerSkeleton.VecU128 vec)
+    | VecBool vec : t P (ContainerSkeleton.VecBool vec)
+    | VecAddress vec : t P (ContainerSkeleton.VecAddress vec)
+    | VecU16 vec : t P (ContainerSkeleton.VecU16 vec)
+    | VecU32 vec : t P (ContainerSkeleton.VecU32 vec)
+    | VecU256 vec : t P (ContainerSkeleton.VecU256 vec).
+  End IsWithoutLocals.
+End ContainerSkeleton.
+
+Module ValueImpl.
+  Module IsWithoutLocals.
+    Inductive t : ValueImpl.t -> Prop :=
+    | Invalid : t ValueImpl.Invalid
+    | U8 z : t (ValueImpl.U8 z)
+    | U16 z : t (ValueImpl.U16 z)
+    | U32 z : t (ValueImpl.U32 z)
+    | U64 z : t (ValueImpl.U64 z)
+    | U128 z : t (ValueImpl.U128 z)
+    | U256 z : t (ValueImpl.U256 z)
+    | Bool b : t (ValueImpl.Bool b)
+    | Address a : t (ValueImpl.Address a)
+    | ContainerRef r : t (ValueImpl.ContainerRef r)
+    | IndexedRef r : t (ValueImpl.IndexedRef r)
+    | Container c : ContainerSkeleton.IsWithoutLocals.t t c -> t (ValueImpl.Container c).
+  End IsWithoutLocals.
+End ValueImpl.
+```
+
+which type-checks. We will now show that it implies that the function `copy_value` succeeds. We state this lemma where this function is defined, namely in: