feat: add proof for Bytecode.MoveLoc

formal-land · Dec 19, 2024 · 03777d5 · 03777d5
1 parent 2cdf5fd
commit 03777d5
Showing 1 changed file with 18 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
@@ -713,7 +713,24 @@ Proof.
     apply H.
   }
   { guard_instruction (Bytecode.MoveLoc z).
-    admit.
+    destruct H_type_safety_checker as [H_stack].
+    pose proof (TypeSafetyChecker.Impl_TypeSafetyChecker.push
+      (TypeSafetyChecker.Impl_TypeSafetyChecker.local_at type_safety_checker {| file_format_index.LocalIndex.a0 := z |})
+      type_safety_checker
+    ).
+    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 |})
+      type_safety_checker.(TypeSafetyChecker.stack)
+      H_stack
+    ).
+    do 2 (step; cbn; trivial).
+    unfold safe_unwrap_err.
+    step; cbn; trivial.
+    destruct u.
+    constructor; cbn.
+    apply H0.
   }
   { guard_instruction (Bytecode.StLoc z).
     unfold_state_monad.