feat: add proofs for Abort

formal-land · Dec 17, 2024 · 0177d28 · 0177d28
1 parent a7e5857
commit 0177d28
Showing 1 changed file with 9 additions and 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
@@ -1027,7 +1027,15 @@ Proof.
     admit.
   }
   { guard_instruction Bytecode.Abort.
-    admit.
+    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].
+    destruct operand; cbn; trivial.
+    step; cbn; trivial.
+    unfold set; cbn.
+    hauto l: on.
   }
   { guard_instruction Bytecode.Nop.
     apply H_type_safety_checker.