From 26a04fbdedc968a5a486e3f38f1643758b2773a3 Mon Sep 17 00:00:00 2001 From: Antoine James Date: Fri, 6 Dec 2024 14:56:41 +0100 Subject: [PATCH] draft: Start working on CastU8 proof --- .../move_sui/proofs/move_bytecode_verifier/type_safety.v | 7 +++++-- 1 file changed, 5 insertions(+), 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 index 32e3f090c..09b1a18d0 100644 --- 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.