From 03777d5b231e547602ddddfbff7ac6baf604c3fc Mon Sep 17 00:00:00 2001 From: Antoine James Date: Thu, 19 Dec 2024 11:31:23 +0100 Subject: [PATCH] feat: add proof for Bytecode.MoveLoc --- .../move_bytecode_verifier/type_safety.v | 19 ++++++++++++++++++- 1 file changed, 18 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 6f1cdd1ac..744d669de 100644 --- 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.