feat: Add verify_instr_is_valid Lemma

formal-land · Dec 6, 2024 · 599e698 · 599e698
1 parent 03a7941
commit 599e698
Showing 1 changed file with 8 additions and 0 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
@@ -81,3 +81,11 @@ Proof.
     admit.
   }
 Admitted.
+
+Lemma verify_instr_is_valid (instruction : Bytecode.t) (pc : Z) (type_safety_checker : TypeSafetyChecker.t)
+  (H_type_safety_checker : TypeSafetyChecker.Valid.t type_safety_checker) :
+  match verify_instr instruction pc type_safety_checker with
+  | Panic.Value (Result.Ok _, type_safety_checker') => TypeSafetyChecker.Valid.t type_safety_checker'
+  | _ => True
+  end.
+Proof.