draft: Start working on CastU8 proof

formal-land · Dec 6, 2024 · 91b9a3e · 91b9a3e
1 parent 9e338df
commit 91b9a3e
Showing 1 changed file with 5 additions and 2 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
@@ -1,5 +1,6 @@
 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.
@@ -513,8 +514,10 @@ Proof.
     sauto q: on.
   }
   { guard_instruction Bytecode.CastU8.
-
-    admit.
+    unfold_state_monad.
+    destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
+    destruct operand; cbn; [|trivial].
+    step; cbn. trivial.
   }
   { guard_instruction Bytecode.CastU16.
     admit.