From 246553dadbf6a089bd92bcdea645cff95e26f3ed Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Sun, 6 Dec 2020 22:15:54 +0100 Subject: Asmgen proof completely proved with ldp/stp --- aarch64/PostpassSchedulingproof.v | 43 +++++++++++++++++++-------------------- 1 file changed, 21 insertions(+), 22 deletions(-) (limited to 'aarch64/PostpassSchedulingproof.v') diff --git a/aarch64/PostpassSchedulingproof.v b/aarch64/PostpassSchedulingproof.v index 140b3aa2..48840602 100644 --- a/aarch64/PostpassSchedulingproof.v +++ b/aarch64/PostpassSchedulingproof.v @@ -99,28 +99,27 @@ Lemma transf_find_bblock: verified_schedule bb = OK tbb /\ find_bblock (Ptrofs.unsigned ofs) (fn_blocks tf) = Some tbb. Proof. -Admitted. - (*intros.*) - (*monadInv H0. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x))); try (inv EQ0; fail). inv EQ0.*) - (*monadInv EQ. simpl in *.*) - (*generalize (Ptrofs.unsigned ofs) H x EQ0; clear ofs H x g EQ0.*) - (*induction (fn_blocks f).*) - (*- intros. simpl in *. discriminate.*) - (*- intros. simpl in *.*) - (*monadInv EQ0. simpl.*) - (*destruct (zlt z 0); try discriminate.*) - (*destruct (zeq z 0).*) - (*+ inv H. eauto.*) - (*+ monadInv EQ0.*) - (*exploit IHb; eauto.*) - (*intros (tbb & SCH & FIND).*) - (*eexists; split; eauto.*) - (*inv FIND.*) - (*unfold verify_size in EQ0.*) - (*destruct (size a =? size (stick_header (header a) x)) eqn:EQSIZE; try discriminate.*) - (*rewrite Z.eqb_eq in EQSIZE; rewrite EQSIZE.*) - (*reflexivity.*) -(*Qed.*) + intros. + monadInv H0. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x))); try (inv EQ0; fail). inv EQ0. + monadInv EQ. simpl in *. + generalize (Ptrofs.unsigned ofs) H x EQ0; clear ofs H x g EQ0. + induction (fn_blocks f). + - intros. simpl in *. discriminate. + - intros. simpl in *. + monadInv EQ0. simpl. + destruct (zlt z 0); try discriminate. + destruct (zeq z 0). + + inv H. eauto. + + monadInv EQ0. + exploit IHb; eauto. + intros (tbb & SCH & FIND). + eexists; split; eauto. + inv FIND. + unfold verify_size in EQ0. + destruct (size a =? size (stick_header (header a) x)) eqn:EQSIZE; try discriminate. + rewrite Z.eqb_eq in EQSIZE; rewrite EQSIZE. + reflexivity. +Qed. Lemma stick_header_neutral: forall a, a = (stick_header (header a) (no_header a)). -- cgit