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] 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.