From ad69926edbee2832242d0b991a654cbda66ff367 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 21 Mar 2019 07:10:14 +0100 Subject: simplification of the proof --- mppa_k1c/PostpassScheduling.v | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'mppa_k1c/PostpassScheduling.v') diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v index b5d55ad3..8cc74eda 100644 --- a/mppa_k1c/PostpassScheduling.v +++ b/mppa_k1c/PostpassScheduling.v @@ -351,8 +351,9 @@ Definition verified_schedule_nob (bb : bblock) : res (list bblock) := do tbb <- concat_all lbb; do sizecheck <- verify_size bb lbb; do schedcheck <- verify_schedule bb' tbb; - do parcheck <- verify_par lbb; - stick_header_code (header bb) lbb. + do res <- stick_header_code (header bb) lbb; + do parcheck <- verify_par res; + OK res. Lemma verified_schedule_nob_size: forall bb lbb, verified_schedule_nob bb = OK lbb -> size bb = size_blocks lbb. @@ -378,7 +379,7 @@ Lemma verified_schedule_nob_header: /\ Forall (fun b => header b = nil) lbb. Proof. intros. split. - - monadInv H. unfold stick_header_code in EQ4. destruct (hd_error _); try discriminate. inv EQ4. + - monadInv H. unfold stick_header_code in EQ2. destruct (hd_error _); try discriminate. inv EQ2. simpl. reflexivity. - apply verified_schedule_nob_no_header_in_middle in H. assumption. Qed. -- cgit