From 3cfe2c8c52a323ceb85f32a23e8ea2729d273c7c Mon Sep 17 00:00:00 2001
From: Antoine James <mushow@proton.me>
Date: Fri, 6 Dec 2024 10:17:27 +0100
Subject: [PATCH 1/7] feat: Add TypeSafetyChecker Module

---
 .../proofs/move_bytecode_verifier/type_safety.v        | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v b/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
index 930bc2f29..c165cf9bb 100644
--- a/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
+++ b/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
@@ -10,6 +10,16 @@ Require Import move_sui.simulations.move_vm_types.values.values_impl.
 
 Import simulations.M.Notations.
 
+Module TypeSafetyChecker.
+  Module Valid.
+    Record t (x : TypeSafetyChecker.t) : Prop := {
+      stack : AbstractStack.Valid.t x.(TypeSafetyChecker.stack);
+    }.
+  End Valid.
+
+
+End TypeSafetyChecker.
+
 Module IsValueOfType.
   Definition t (value : Value.t) (typ : SignatureToken.t) : Prop :=
     match value, typ with

From 61dea5018f898169494577470ca1bd4ba007ab75 Mon Sep 17 00:00:00 2001
From: Antoine James <mushow@proton.me>
Date: Fri, 6 Dec 2024 10:23:45 +0100
Subject: [PATCH 2/7] feat: Add verify_instr_is_valid Lemma

---
 .../move_sui/proofs/move_bytecode_verifier/type_safety.v  | 8 ++++++++
 1 file changed, 8 insertions(+)

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 c165cf9bb..2367b24a6 100644
--- a/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
+++ b/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
@@ -436,3 +436,11 @@ Proof.
     admit.
   }
 Admitted.
+
+Lemma verify_instr_is_valid (instruction : Bytecode.t) (pc : Z) (type_safety_checker : TypeSafetyChecker.t)
+  (H_type_safety_checker : TypeSafetyChecker.Valid.t type_safety_checker) :
+  match verify_instr instruction pc type_safety_checker with
+  | Panic.Value (Result.Ok _, type_safety_checker') => TypeSafetyChecker.Valid.t type_safety_checker'
+  | _ => True
+  end.
+Proof.

From bdeb574430da968cacf643d4c44ac6b6bfc82518 Mon Sep 17 00:00:00 2001
From: Antoine James <mushow@proton.me>
Date: Fri, 6 Dec 2024 10:55:13 +0100
Subject: [PATCH 3/7] feat: Re-order Bytecode instructions

---
 .../simulations/move_binary_format/file_format.v   | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/CoqOfRust/move_sui/simulations/move_binary_format/file_format.v b/CoqOfRust/move_sui/simulations/move_binary_format/file_format.v
index 9d304e52d..d71aefd56 100644
--- a/CoqOfRust/move_sui/simulations/move_binary_format/file_format.v
+++ b/CoqOfRust/move_sui/simulations/move_binary_format/file_format.v
@@ -844,11 +844,17 @@ Module Bytecode.
   | BrFalse (_ : Z)
   | Branch (_ : Z)
   | LdU8 (_ : Z)
+  | LdU16 (_ : Z)
+  | LdU32 (_ : Z)
   | LdU64 (_ : Z)
   | LdU128 (_ : Z)
+  | LdU256 (_ : Z)
   | CastU8
+  | CastU16
+  | CastU32
   | CastU64
   | CastU128
+  | CastU256
   | LdConst (_ : ConstantPoolIndex.t)
   | LdTrue
   | LdFalse
@@ -908,13 +914,7 @@ Module Bytecode.
   | VecPushBack (_ : SignatureIndex.t)
   | VecPopBack (_ : SignatureIndex.t)
   | VecUnpack (_ : SignatureIndex.t) (_ : Z)
-  | VecSwap (_ : SignatureIndex.t)
-  | LdU16 (_ : Z)
-  | LdU32 (_ : Z)
-  | LdU256 (_ : Z)
-  | CastU16
-  | CastU32
-  | CastU256.
+  | VecSwap (_ : SignatureIndex.t).
 
   Definition is_unconditional_branch (self : t) : bool :=
     match self with

From 8af60e5b2ef32e1d601a2569778d612fd8b1d01c Mon Sep 17 00:00:00 2001
From: Antoine James <mushow@proton.me>
Date: Fri, 6 Dec 2024 10:58:49 +0100
Subject: [PATCH 4/7] feat: Add all instruction cases - admit. for now

---
 .../move_bytecode_verifier/type_safety.v      | 234 ++++++++++++++++++
 1 file changed, 234 insertions(+)

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 2367b24a6..e28503dd5 100644
--- a/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
+++ b/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
@@ -444,3 +444,237 @@ Lemma verify_instr_is_valid (instruction : Bytecode.t) (pc : Z) (type_safety_che
   | _ => True
   end.
 Proof.
+  destruct instruction eqn:H_instruction; cbn.
+  { guard_instruction Bytecode.Pop.
+    admit.
+  }
+  { guard_instruction Bytecode.Ret.
+    admit.
+  }
+  { guard_instruction (Bytecode.BrTrue z).
+    admit.
+  }
+  { guard_instruction (Bytecode.BrFalse z).
+    admit.
+  }
+  { guard_instruction (Bytecode.Branch z).
+    admit.
+  }
+  { guard_instruction (Bytecode.LdU8 z).
+    admit.
+  }
+  {
+    guard_instruction (Bytecode.LdU16 z).
+    admit.
+  }
+  { guard_instruction (Bytecode.LdU32 z).
+    admit.
+  }
+  { guard_instruction (Bytecode.LdU64 z).
+    admit.
+  }
+  { guard_instruction (Bytecode.LdU128 z).
+    admit.
+  }
+  { guard_instruction (Bytecode.LdU256 z).
+    admit.
+  }
+  { guard_instruction Bytecode.CastU8.
+    admit.
+  }
+  { guard_instruction Bytecode.CastU16.
+    admit.
+  }
+  { guard_instruction Bytecode.CastU32.
+    admit.
+  }
+  { guard_instruction Bytecode.CastU64.
+    admit.
+  }
+  { guard_instruction Bytecode.CastU128.
+    admit.
+  }
+  { guard_instruction Bytecode.CastU256.
+    admit.
+  }
+  { guard_instruction (Bytecode.LdConst t).
+    admit.
+  }
+  { guard_instruction Bytecode.LdTrue.
+    admit.
+  }
+  { guard_instruction Bytecode.LdFalse.
+    admit.
+  }
+  { guard_instruction (Bytecode.CopyLoc z).
+    admit.
+  }
+  { guard_instruction (Bytecode.MoveLoc z).
+    admit.
+  }
+  { guard_instruction (Bytecode.StLoc z).
+    admit.
+  }
+  { guard_instruction (Bytecode.Call t).
+    admit.
+  }
+  { guard_instruction (Bytecode.CallGeneric t).
+    admit.
+  }
+  { guard_instruction (Bytecode.Pack t).
+    admit.
+  }
+  { guard_instruction (Bytecode.PackGeneric t).
+    admit.
+  }
+  { guard_instruction (Bytecode.Unpack t).
+    admit.
+  }
+  { guard_instruction (Bytecode.UnpackGeneric t).
+    admit.
+  }
+  { guard_instruction Bytecode.ReadRef.
+    admit.
+  }
+  { guard_instruction Bytecode.WriteRef.
+    admit.
+  }
+  { guard_instruction Bytecode.FreezeRef.
+    admit.
+  }
+  { guard_instruction (Bytecode.MutBorrowLoc z).
+    admit.
+  }
+  { guard_instruction (Bytecode.ImmBorrowLoc z).
+    admit.
+  }
+  { guard_instruction (Bytecode.MutBorrowField t).
+    admit.
+  }
+  { guard_instruction (Bytecode.MutBorrowFieldGeneric t).
+    admit.
+  }
+  { guard_instruction (Bytecode.ImmBorrowField t).
+    admit.
+  }
+  { guard_instruction (Bytecode.ImmBorrowFieldGeneric t).
+    admit.
+  }
+  { guard_instruction (Bytecode.MutBorrowGlobalDeprecated t).
+    admit.
+  }
+  { guard_instruction (Bytecode.MutBorrowGlobalGenericDeprecated t).
+    admit.
+  }
+  { guard_instruction (Bytecode.ImmBorrowGlobalDeprecated t).
+    admit.
+  }
+  { guard_instruction (Bytecode.ImmBorrowGlobalGenericDeprecated t).
+    admit.
+  }
+  { guard_instruction Bytecode.Add.
+    admit.
+  }
+  { guard_instruction Bytecode.Sub.
+    admit.
+  }
+  { guard_instruction Bytecode.Mul.
+    admit.
+  }
+  { guard_instruction Bytecode.Mod.
+    admit.
+  }
+  { guard_instruction Bytecode.Div.
+    admit.
+  }
+  { guard_instruction Bytecode.BitOr.
+    admit.
+  }
+  { guard_instruction Bytecode.BitAnd.
+    admit.
+  }
+  { guard_instruction Bytecode.Xor.
+    admit.
+  }
+  { guard_instruction Bytecode.Or.
+    admit.
+  }
+  { guard_instruction Bytecode.And.
+    admit.
+  }
+  { guard_instruction Bytecode.Not.
+    admit.
+  }
+  { guard_instruction Bytecode.Eq.
+    admit.
+  }
+  { guard_instruction Bytecode.Neq.
+    admit.
+  }
+  { guard_instruction Bytecode.Lt.
+    admit.
+  }
+  { guard_instruction Bytecode.Gt.
+    admit.
+  }
+  { guard_instruction Bytecode.Le.
+    admit.
+  }
+  { guard_instruction Bytecode.Ge.
+    admit.
+  }
+  { guard_instruction Bytecode.Abort.
+    admit.
+  }
+  { guard_instruction Bytecode.Nop.
+    admit.
+  }
+  { guard_instruction (Bytecode.ExistsDeprecated t).
+    admit.
+  }
+  { guard_instruction (Bytecode.ExistsGenericDeprecated t).
+    admit.
+  }
+  { guard_instruction (Bytecode.MoveFromDeprecated t).
+    admit.
+  }
+  { guard_instruction (Bytecode.MoveFromGenericDeprecated t).
+    admit.
+  }
+  { guard_instruction (Bytecode.MoveToDeprecated t).
+    admit.
+  }
+  { guard_instruction (Bytecode.MoveToGenericDeprecated t).
+    admit.
+  }
+  { guard_instruction Bytecode.Shl.
+    admit.
+  }
+  { guard_instruction Bytecode.Shr.
+    admit.
+  }
+  { guard_instruction (Bytecode.VecPack t z).
+    admit.
+  }
+  { guard_instruction (Bytecode.VecLen t).
+    admit.
+  }
+  { guard_instruction (Bytecode.VecImmBorrow t).
+    admit.
+  }
+  { guard_instruction (Bytecode.VecMutBorrow t).
+    admit.
+  }
+  { guard_instruction (Bytecode.VecPushBack t).
+    admit.
+  }
+  { guard_instruction (Bytecode.VecPopBack t).
+    admit.
+  }
+  { guard_instruction (Bytecode.VecUnpack t z).
+    admit.
+  }
+  { guard_instruction (Bytecode.VecSwap t).
+    admit.
+  }
+Admitted.
\ No newline at end of file

From 134d69c1614aee501c012a52830f867755f3292a Mon Sep 17 00:00:00 2001
From: Antoine James <mushow@proton.me>
Date: Fri, 6 Dec 2024 12:11:52 +0100
Subject: [PATCH 5/7] draft: Start with LdUX

---
 .../proofs/move_bytecode_verifier/type_safety.v       | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 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 e28503dd5..5c8c0bb91 100644
--- a/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
+++ b/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
@@ -16,8 +16,6 @@ Module TypeSafetyChecker.
       stack : AbstractStack.Valid.t x.(TypeSafetyChecker.stack);
     }.
   End Valid.
-
-
 End TypeSafetyChecker.
 
 Module IsValueOfType.
@@ -460,8 +458,15 @@ Proof.
   { guard_instruction (Bytecode.Branch z).
     admit.
   }
+  (*
+  Lemma push_n_is_valid {A : Set} `{Eq.Trait A}
+      (item : A) (n : Z) (stack : AbstractStack.t A)
+      (H_n : Integer.Valid.t IntegerKind.U64 n)
+      (H_stack : AbstractStack.Valid.t stack) :
+  *)
   { guard_instruction (Bytecode.LdU8 z).
-    admit.
+    unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push.
+    pose proof (AbstractStack.push_n_is_valid (SignatureToken.U8) z type_safety_checker.(TypeSafetyChecker.stack) _ H_type_safety_checker).
   }
   {
     guard_instruction (Bytecode.LdU16 z).

From f357e84d9f4be13544c37030be7e9cabe7e1c91a Mon Sep 17 00:00:00 2001
From: Antoine James <mushow@proton.me>
Date: Fri, 6 Dec 2024 13:55:15 +0100
Subject: [PATCH 6/7] draft: Move further in LdU8

---
 .../move_sui/proofs/move_bytecode_verifier/type_safety.v   | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

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 5c8c0bb91..9cfaa75ec 100644
--- a/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
+++ b/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
@@ -466,7 +466,11 @@ Proof.
   *)
   { guard_instruction (Bytecode.LdU8 z).
     unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push.
-    pose proof (AbstractStack.push_n_is_valid (SignatureToken.U8) z type_safety_checker.(TypeSafetyChecker.stack) _ H_type_safety_checker).
+    pose proof (AbstractStack.push_n_is_valid SignatureToken.U8 z).
+    unfold state
+    {  }
+    
+    admit.
   }
   {
     guard_instruction (Bytecode.LdU16 z).
@@ -485,6 +489,7 @@ Proof.
     admit.
   }
   { guard_instruction Bytecode.CastU8.
+
     admit.
   }
   { guard_instruction Bytecode.CastU16.

From 9e338df7768292dcf0bd2e7bdc769599b7661f61 Mon Sep 17 00:00:00 2001
From: Antoine James <mushow@proton.me>
Date: Fri, 6 Dec 2024 14:13:03 +0100
Subject: [PATCH 7/7] feat: clean up code and write LdU8, LdU16, LdU32, LdU64,
 LdU128, LdU256 proofs

---
 .../move_bytecode_verifier/type_safety.v      | 98 ++++++++++++-------
 1 file changed, 61 insertions(+), 37 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 9cfaa75ec..32e3f090c 100644
--- a/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
+++ b/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
@@ -65,9 +65,14 @@ Ltac guard_instruction expected_instruction :=
   end.
 
 Ltac unfold_state_monad :=
-  unfold StatePanicResult.bind, StatePanic.bind, StatePanic.bind,
-    "return!toS!", "liftS!", "readS!";
-  cbn.
+  repeat (
+    unfold StatePanicResult.bind, StatePanic.bind, StatePanic.bind,
+      "return!toS!", 
+      "liftS!", 
+      "readS!", 
+      "return!toS!?";
+    cbn
+  ).
 
 Ltac destruct_abstract_push :=
   unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push;
@@ -172,6 +177,12 @@ Proof.
     rewrite H_push.
     hauto l: on.
   }
+  { guard_instruction (Bytecode.LdU16 z).
+    admit.
+  }
+  { guard_instruction (Bytecode.LdU32 z).
+    admit.
+  }
   { guard_instruction (Bytecode.LdU64 z).
     destruct_abstract_push.
     lib.step; cbn; [|exact I].
@@ -188,6 +199,9 @@ Proof.
     rewrite H_push.
     hauto l: on.
   }
+  { guard_instruction (Bytecode.LdU256 z).
+    admit.
+  }
   { guard_instruction Bytecode.CastU8.
     destruct_abstract_pop H_interpreter.
     lib.step; cbn; [exact I|].
@@ -199,6 +213,12 @@ Proof.
       sauto lq: on
     ).
   }
+  { guard_instruction Bytecode.CastU16.
+    admit.
+  }
+  { guard_instruction Bytecode.CastU32.
+    admit.
+  }
   { guard_instruction Bytecode.CastU64.
     destruct_abstract_pop H_interpreter.
     lib.step; cbn; [exact I|].
@@ -221,6 +241,9 @@ Proof.
       sauto lq: on
     ).
   }
+  { guard_instruction Bytecode.CastU256.
+    admit.
+  }
   { guard_instruction (Bytecode.LdConst t).
     admit.
   }
@@ -415,24 +438,6 @@ Proof.
   { guard_instruction (Bytecode.VecSwap t).
     admit.
   }
-  { guard_instruction (Bytecode.LdU16 z).
-    admit.
-  }
-  { guard_instruction (Bytecode.LdU32 z).
-    admit.
-  }
-  { guard_instruction (Bytecode.LdU256 z).
-    admit.
-  }
-  { guard_instruction Bytecode.CastU16.
-    admit.
-  }
-  { guard_instruction Bytecode.CastU32.
-    admit.
-  }
-  { guard_instruction Bytecode.CastU256.
-    admit.
-  }
 Admitted.
 
 Lemma verify_instr_is_valid (instruction : Bytecode.t) (pc : Z) (type_safety_checker : TypeSafetyChecker.t)
@@ -458,35 +463,54 @@ Proof.
   { guard_instruction (Bytecode.Branch z).
     admit.
   }
-  (*
-  Lemma push_n_is_valid {A : Set} `{Eq.Trait A}
-      (item : A) (n : Z) (stack : AbstractStack.t A)
-      (H_n : Integer.Valid.t IntegerKind.U64 n)
-      (H_stack : AbstractStack.Valid.t stack) :
-  *)
   { guard_instruction (Bytecode.LdU8 z).
     unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push.
-    pose proof (AbstractStack.push_n_is_valid SignatureToken.U8 z).
-    unfold state
-    {  }
-    
-    admit.
+    with_strategy opaque [AbstractStack.push] unfold_state_monad.
+    pose proof (AbstractStack.push_is_valid SignatureToken.U8 type_safety_checker.(TypeSafetyChecker.stack)).
+    destruct AbstractStack.push as [[result stack']|]; cbn; [|trivial].
+    destruct result; cbn; [|trivial].
+    sauto q: on.
   }
   {
     guard_instruction (Bytecode.LdU16 z).
-    admit.
+    unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push.
+    with_strategy opaque [AbstractStack.push] unfold_state_monad.
+    pose proof (AbstractStack.push_is_valid SignatureToken.U16 type_safety_checker.(TypeSafetyChecker.stack)).
+    destruct AbstractStack.push as [[result stack']|]; cbn; [|trivial].
+    destruct result; cbn; [|trivial].
+    sauto q: on.
   }
   { guard_instruction (Bytecode.LdU32 z).
-    admit.
+    unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push.
+    with_strategy opaque [AbstractStack.push] unfold_state_monad.
+    pose proof (AbstractStack.push_is_valid SignatureToken.U32 type_safety_checker.(TypeSafetyChecker.stack)).
+    destruct AbstractStack.push as [[result stack']|]; cbn; [|trivial].
+    destruct result; cbn; [|trivial].
+    sauto q: on.
   }
   { guard_instruction (Bytecode.LdU64 z).
-    admit.
+    unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push.
+    with_strategy opaque [AbstractStack.push] unfold_state_monad.
+    pose proof (AbstractStack.push_is_valid SignatureToken.U64 type_safety_checker.(TypeSafetyChecker.stack)).
+    destruct AbstractStack.push as [[result stack']|]; cbn; [|trivial].
+    destruct result; cbn; [|trivial].
+    sauto q: on.
   }
   { guard_instruction (Bytecode.LdU128 z).
-    admit.
+    unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push.
+    with_strategy opaque [AbstractStack.push] unfold_state_monad.
+    pose proof (AbstractStack.push_is_valid SignatureToken.U128 type_safety_checker.(TypeSafetyChecker.stack)).
+    destruct AbstractStack.push as [[result stack']|]; cbn; [|trivial].
+    destruct result; cbn; [|trivial].
+    sauto q: on.
   }
   { guard_instruction (Bytecode.LdU256 z).
-    admit.
+    unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push.
+    with_strategy opaque [AbstractStack.push] unfold_state_monad.
+    pose proof (AbstractStack.push_is_valid SignatureToken.U256 type_safety_checker.(TypeSafetyChecker.stack)).
+    destruct AbstractStack.push as [[result stack']|]; cbn; [|trivial].
+    destruct result; cbn; [|trivial].
+    sauto q: on.
   }
   { guard_instruction Bytecode.CastU8.