From 788406cac443d2d33345c0b9db86577c6b39011e Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 24 Nov 2020 17:04:26 +0100 Subject: Main part of postpasssch proof now completed --- aarch64/PostpassScheduling.v | 423 +------------------------------------------ 1 file changed, 9 insertions(+), 414 deletions(-) (limited to 'aarch64/PostpassScheduling.v') diff --git a/aarch64/PostpassScheduling.v b/aarch64/PostpassScheduling.v index fa7e2776..74c2438e 100644 --- a/aarch64/PostpassScheduling.v +++ b/aarch64/PostpassScheduling.v @@ -17,9 +17,8 @@ Require Import Coqlib Errors AST Integers. Require Import Asmblock Axioms Memory Globalenvs. -Require Import Asmblockdeps Asmblockgenproof0 Asmblockprops. +Require Import Asmblockdeps Asmblockprops. Require Import IterList. -(*Require Peephole.*) Local Open Scope error_monad_scope. @@ -33,188 +32,6 @@ Section verify_schedule. Variable lk: aarch64_linker. -(* -(** * Concat all bundles into one big basic block *) - -(* Lemmas necessary for defining concat_all *) -Lemma app_nonil {A: Type} (l l': list A) : l <> nil -> l ++ l' <> nil. -Proof. - intros. destruct l; simpl. - - contradiction. - - discriminate. -Qed. - -Lemma app_nonil2 {A: Type} : forall (l l': list A), l' <> nil -> l ++ l' <> nil. -Proof. - destruct l. - - intros. simpl; auto. - - intros. rewrite <- app_comm_cons. discriminate. -Qed. - -Definition check_size bb := - if zlt Ptrofs.max_unsigned (size bb) - then Error (msg "PostpassSchedulingproof.check_size") - else OK tt. - -Program Definition concat2 (bb bb': bblock) : res bblock := - do ch <- check_size bb; - do ch' <- check_size bb'; - match (exit bb) with - | None => - match (header bb') with - | nil => - match (exit bb') with - | Some (PExpand (Pbuiltin _ _ _)) => Error (msg "PostpassSchedulingproof.concat2: builtin not alone") - | _ => OK {| header := header bb; body := body bb ++ body bb'; exit := exit bb' |} - end - | _ => Error (msg "PostpassSchedulingproof.concat2") - end - | _ => Error (msg "PostpassSchedulingproof.concat2") - end. -Next Obligation. - apply wf_bblock_refl. constructor. - - destruct bb' as [hd' bdy' ex' WF']. destruct bb as [hd bdy ex WF]. simpl in *. - apply wf_bblock_refl in WF'. apply wf_bblock_refl in WF. - inversion_clear WF'. inversion_clear WF. clear H1 H3. - inversion H2; inversion H0. - + left. apply app_nonil. auto. - + right. auto. - + left. apply app_nonil2. auto. - + right. auto. - - unfold builtin_alone. intros. rewrite H0 in H. - assert (Some (PExpand (Pbuiltin ef args res)) <> Some (PExpand (Pbuiltin ef args res))). - apply (H ef args res). contradict H1. auto. -Defined. - -Lemma concat2_zlt_size: - forall a b bb, - concat2 a b = OK bb -> - size a <= Ptrofs.max_unsigned - /\ size b <= Ptrofs.max_unsigned. -Proof. - intros. monadInv H. - split. - - unfold check_size in EQ. destruct (zlt Ptrofs.max_unsigned (size a)); monadInv EQ. omega. - - unfold check_size in EQ1. destruct (zlt Ptrofs.max_unsigned (size b)); monadInv EQ1. omega. -Qed. - -Lemma concat2_noexit: - forall a b bb, - concat2 a b = OK bb -> - exit a = None. -Proof. - intros. destruct a as [hd bdy ex WF]; simpl in *. - destruct ex as [e|]; simpl in *; auto. - unfold concat2 in H. simpl in H. monadInv H. -Qed. - -Lemma concat2_decomp: - forall a b bb, - concat2 a b = OK bb -> - body bb = body a ++ body b - /\ exit bb = exit b. -Proof. - intros. exploit concat2_noexit; eauto. intros. - destruct a as [hda bda exa WFa]; destruct b as [hdb bdb exb WFb]; destruct bb as [hd bd ex WF]; simpl in *. - subst exa. - unfold concat2 in H; simpl in H. - destruct hdb. - - destruct exb. - + destruct c. - * destruct i; monadInv H; split; auto. - * monadInv H. split; auto. - + monadInv H. split; auto. - - monadInv H. -Qed. - -Lemma concat2_size: - forall a b bb, concat2 a b = OK bb -> size bb = size a + size b. -Proof. - intros. unfold concat2 in H. - destruct a as [hda bda exa WFa]; destruct b as [hdb bdb exb WFb]; destruct bb as [hd bdy ex WF]; simpl in *. - destruct exa; monadInv H. destruct hdb; try (monadInv EQ2). destruct exb; try (monadInv EQ2). - - destruct c. - + destruct i; monadInv EQ2; - unfold size; simpl; rewrite app_length; rewrite Nat.add_0_r; rewrite <- Nat2Z.inj_add; rewrite Nat.add_assoc; reflexivity. - + monadInv EQ2. unfold size; simpl. rewrite app_length. rewrite Nat.add_0_r. rewrite <- Nat2Z.inj_add. rewrite Nat.add_assoc. reflexivity. - - unfold size; simpl. rewrite app_length. repeat (rewrite Nat.add_0_r). rewrite <- Nat2Z.inj_add. reflexivity. -Qed. - -Lemma concat2_header: - forall bb bb' tbb, - concat2 bb bb' = OK tbb -> header bb = header tbb. -Proof. - intros. destruct bb as [hd bdy ex COR]; destruct bb' as [hd' bdy' ex' COR']; destruct tbb as [thd tbdy tex tCOR]; simpl in *. - unfold concat2 in H. simpl in H. monadInv H. - destruct ex; try discriminate. destruct hd'; try discriminate. destruct ex'. - - destruct c. - + destruct i; try discriminate; congruence. - + congruence. - - congruence. -Qed. - -Lemma concat2_no_header_in_middle: - forall bb bb' tbb, - concat2 bb bb' = OK tbb -> - header bb' = nil. -Proof. - intros. destruct bb as [hd bdy ex COR]; destruct bb' as [hd' bdy' ex' COR']; destruct tbb as [thd tbdy tex tCOR]; simpl in *. - unfold concat2 in H. simpl in H. monadInv H. - destruct ex; try discriminate. destruct hd'; try discriminate. reflexivity. -Qed. - - - -Fixpoint concat_all (lbb: list bblock) : res bblock := - match lbb with - | nil => Error (msg "PostpassSchedulingproof.concatenate: empty list") - | bb::nil => OK bb - | bb::lbb => - do bb' <- concat_all lbb; - concat2 bb bb' - end. - -Lemma concat_all_size : - forall lbb a bb bb', - concat_all (a :: lbb) = OK bb -> - concat_all lbb = OK bb' -> - size bb = size a + size bb'. -Proof. - intros. unfold concat_all in H. fold concat_all in H. - destruct lbb; try discriminate. - monadInv H. rewrite H0 in EQ. inv EQ. - apply concat2_size. assumption. -Qed. - -Lemma concat_all_header: - forall lbb bb tbb, - concat_all (bb::lbb) = OK tbb -> header bb = header tbb. -Proof. - destruct lbb. - - intros. simpl in H. congruence. - - intros. simpl in H. destruct lbb. - + inv H. eapply concat2_header; eassumption. - + monadInv H. eapply concat2_header; eassumption. -Qed. - -Lemma concat_all_no_header_in_middle: - forall lbb tbb, - concat_all lbb = OK tbb -> - Forall (fun b => header b = nil) (tail lbb). -Proof. - induction lbb; intros; try constructor. - simpl. simpl in H. destruct lbb. - - constructor. - - monadInv H. simpl tl in IHlbb. constructor. - + apply concat2_no_header_in_middle in EQ0. apply concat_all_header in EQ. congruence. - + apply IHlbb in EQ. assumption. -Qed. - -Inductive is_concat : bblock -> list bblock -> Prop := - | mk_is_concat: forall tbb lbb, concat_all lbb = OK tbb -> is_concat tbb lbb. -*) -(** * Remainder of the verified scheduler *) - Definition verify_schedule (bb bb' : bblock) : res unit := match bblock_simub bb bb' with | true => OK tt @@ -230,105 +47,6 @@ Proof. apply Z.eqb_eq. assumption. Qed. -(* Lemma verify_schedule_no_header: - forall bb bb', - verify_schedule (no_header bb) bb' = verify_schedule bb bb'. -Proof. - intros. unfold verify_schedule. unfold bblock_simub. unfold pure_bblock_simu_test, bblock_simu_test. rewrite trans_block_noheader_inv. - reflexivity. -Qed. *) - - -(*Lemma stick_header_verify_schedule:*) - (*forall hd bb' hbb' bb,*) - (*stick_header hd bb' = hbb' ->*) - (*verify_schedule bb bb' = verify_schedule bb hbb'.*) -(*Proof.*) - (*intros. unfold verify_schedule. unfold bblock_simub, pure_bblock_simu_test, bblock_simu_test.*) - (*rewrite <- H. rewrite trans_block_header_inv. reflexivity.*) -(*Qed.*) - -(*Lemma check_size_stick_header:*) - (*forall bb hd,*) - (*check_size bb = check_size (stick_header hd bb).*) -(*Proof.*) - (*intros. unfold check_size. rewrite stick_header_size. reflexivity.*) -(*Qed.*) - -(*Lemma stick_header_concat2:*) - (*forall bb bb' hd tbb,*) - (*concat2 bb bb' = OK tbb ->*) - (*concat2 (stick_header hd bb) bb' = OK (stick_header hd tbb).*) -(*Proof.*) - (*intros. monadInv H. erewrite check_size_stick_header in EQ.*) - (*unfold concat2. rewrite EQ. rewrite EQ1. simpl.*) - (*destruct bb as [hdr bdy ex COR]; destruct bb' as [hdr' bdy' ex' COR']; simpl in *.*) - (*destruct ex; try discriminate. destruct hdr'; try discriminate. destruct ex'.*) - (*- destruct c.*) - (*+ destruct i; try discriminate; inv EQ2; unfold stick_header; simpl; reflexivity.*) - (*+ inv EQ2. unfold stick_header; simpl. reflexivity.*) - (*- inv EQ2. unfold stick_header; simpl. reflexivity.*) -(*Qed.*) - -(*Lemma stick_header_concat_all:*) - (*forall bb c tbb hd,*) - (*concat_all (bb :: c) = OK tbb ->*) - (*concat_all (stick_header hd bb :: c) = OK (stick_header hd tbb).*) -(*Proof.*) - (*intros. simpl in *. destruct c; try congruence.*) - (*monadInv H. rewrite EQ. simpl.*) - (*apply stick_header_concat2. assumption.*) -(*Qed.*) - -(*Lemma stick_header_code_no_header:*) - (*forall bb c,*) - (*stick_header_code (header bb) (no_header bb :: c) = OK (bb :: c).*) -(*Proof.*) - (*intros. unfold stick_header_code. simpl. rewrite stick_header_no_header. reflexivity.*) -(*Qed.*) - -(*Lemma hd_tl_size:*) - (*forall lbb bb, hd_error lbb = Some bb -> size_blocks lbb = size bb + size_blocks (tl lbb).*) -(*Proof.*) - (*destruct lbb.*) - (*- intros. simpl in H. discriminate.*) - (*- intros. simpl in H. inv H. simpl. reflexivity.*) -(*Qed.*) - -(*Lemma stick_header_code_size:*) - (*forall h lbb lbb', stick_header_code h lbb = OK lbb' -> size_blocks lbb = size_blocks lbb'.*) -(*Proof.*) - (*intros. unfold stick_header_code in H. destruct (hd_error lbb) eqn:HD; try discriminate.*) - (*inv H. simpl. rewrite stick_header_size. erewrite hd_tl_size; eauto.*) -(*Qed.*) - -(*Lemma stick_header_code_no_header_in_middle:*) - (*forall c h lbb,*) - (*stick_header_code h c = OK lbb ->*) - (*Forall (fun b => header b = nil) (tl c) ->*) - (*Forall (fun b => header b = nil) (tl lbb).*) -(*Proof.*) - (*destruct c; intros.*) - (*- unfold stick_header_code in H. simpl in H. discriminate.*) - (*- unfold stick_header_code in H. simpl in H. inv H. simpl in H0.*) - (*simpl. assumption.*) -(*Qed.*) - -(*Lemma stick_header_code_concat_all:*) - (*forall hd lbb hlbb tbb,*) - (*stick_header_code hd lbb = OK hlbb ->*) - (*concat_all lbb = OK tbb ->*) - (*exists htbb,*) - (*concat_all hlbb = OK htbb*) - (*/\ stick_header hd tbb = htbb.*) -(*Proof.*) - (*intros. exists (stick_header hd tbb). split; auto.*) - (*destruct lbb.*) - (*- unfold stick_header_code in H. simpl in H. discriminate.*) - (*- unfold stick_header_code in H. simpl in H. inv H.*) - (*apply stick_header_concat_all. assumption.*) -(*Qed.*) - Program Definition make_bblock_from_basics lb := match lb with | nil => Error (msg "PostpassScheduling.make_bblock_from_basics") @@ -341,79 +59,22 @@ Program Definition schedule_to_bblock (lb: list basic) (oc: option control) : re | Some c => OK {| header := nil; body := lb; exit := Some c |} end. Next Obligation. - unfold Is_true, AB.non_empty_bblockb. - unfold AB.non_empty_exit. rewrite orb_true_r. reflexivity. + unfold Is_true, non_empty_bblockb. + unfold non_empty_exit. rewrite orb_true_r. reflexivity. Qed. Definition do_schedule (bb: bblock) : res bblock := if (Z.eqb (size bb) 1) then OK (bb) - else match (schedule bb) with (lb, oc) => schedule_to_bblock lb oc end. (* TODO Something here *) - -(* TODO to remove ? *) -(*Definition verify_par_bblock (bb: bblock) : res unit :=*) - (*if (bblock_para_check bb) then OK tt else Error (msg "PostpassScheduling.verify_par_bblock").*) -(*Fixpoint verify_par (lbb: list bblock) :=*) - (*match lbb with*) - (*| nil => OK tt*) - (*| bb :: lbb => do res <- verify_par_bblock bb; verify_par lbb*) - (*end.*) + else match (schedule bb) with (lb, oc) => schedule_to_bblock lb oc end. Definition verified_schedule (bb : bblock) : res bblock := let nhbb := no_header bb in - (* TODO remove? let bb'' := Peephole.optimize_bblock bb' in *) do nhbb' <- do_schedule nhbb; - (*do tbb <- concat_all lbb;*) let bb' := stick_header (header bb) nhbb' in do sizecheck <- verify_size bb bb'; - do schedcheck <- verify_schedule bb bb'; (* TODO Keep this one *) + do schedcheck <- verify_schedule bb bb'; OK (bb'). -(* Definition verified_schedule_nob (bb : bblock) : res (list bblock) := - let nhbb := no_header bb in - do bb' <- do_schedule nhbb; - do sizecheck <- verify_size nhbb bb'; - do schedcheck <- verify_schedule nhbb bb'; - do res <- stick_header_code (header bb) bb'; - OK res. *) - -(*Lemma verified_schedule_nob_size:*) - (*forall bb lbb, verified_schedule_nob bb = OK lbb -> size bb = size_blocks lbb.*) -(*Proof.*) - (*intros. monadInv H. erewrite <- stick_header_code_size; eauto.*) - (*apply verify_size_size.*) - (*destruct x1; try discriminate. assumption.*) -(*Qed.*) - -(*Lemma verified_schedule_nob_no_header_in_middle:*) - (*forall lbb bb,*) - (*verified_schedule_nob bb = OK lbb ->*) - (*Forall (fun b => header b = nil) (tail lbb).*) -(*Proof.*) - (*intros. monadInv H. eapply stick_header_code_no_header_in_middle; eauto.*) - (*eapply concat_all_no_header_in_middle. eassumption.*) -(*Qed.*) - -(*Lemma verified_schedule_nob_header:*) - (*forall bb tbb lbb,*) - (*verified_schedule_nob bb = OK (tbb :: lbb) ->*) - (*header bb = header tbb*) - (*/\ Forall (fun b => header b = nil) lbb.*) -(*Proof.*) - (*intros. split.*) - (*- monadInv H. unfold stick_header_code in EQ3. destruct (hd_error _); try discriminate. inv EQ3.*) - (*simpl. reflexivity.*) - (*- apply verified_schedule_nob_no_header_in_middle in H. assumption.*) -(*Qed.*) - - -(* Definition verified_schedule (bb : bblock) : res (list bblock) := - verified_schedule_nob bb. *) -(* TODO Remove? - match exit bb with - | Some (PExpand (Pbuiltin ef args res)) => OK (bb::nil) (* Special case for ensuring the lemma verified_schedule_builtin_idem *) - | _ => verified_schedule_nob bb - end.*) - Lemma verified_schedule_size: forall bb bb', verified_schedule bb = OK bb' -> size bb = size bb'. Proof. @@ -439,83 +100,17 @@ Proof. rewrite ESIZE. reflexivity. Qed. -(*Lemma verified_schedule_no_header_in_middle:*) - (*forall lbb bb,*) - (*verified_schedule bb = OK lbb ->*) - (*Forall (fun b => header b = nil) (tail lbb).*) -(*Proof.*) - (*intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i.*) - (*all: try (eapply verified_schedule_nob_no_header_in_middle; eauto; fail).*) - (*inv H. simpl. auto.*) -(*Qed.*) - -(*Lemma verified_schedule_header:*) - (*forall bb tbb lbb,*) - (*verified_schedule bb = OK (tbb :: lbb) ->*) - (*header bb = header tbb*) - (*/\ Forall (fun b => header b = nil) lbb.*) -(*Proof.*) - (*intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i.*) - (*all: try (eapply verified_schedule_nob_header; eauto; fail).*) - (*inv H. split; simpl; auto.*) -(*Qed.*) - - -(*Lemma verified_schedule_nob_correct:*) - (*forall ge f bb lbb,*) - (*verified_schedule_nob bb = OK lbb ->*) - (*exists tbb,*) - (*is_concat tbb lbb*) - (*/\ bblock_simu ge f bb tbb.*) -(*Proof.*) - (*intros. monadInv H.*) - (*exploit stick_header_code_concat_all; eauto.*) - (*intros (tbb & CONC & STH).*) - (*exists tbb. split; auto. constructor; auto.*) - (*rewrite verify_schedule_no_header in EQ2. erewrite stick_header_verify_schedule in EQ2; eauto.*) - (*eapply bblock_simub_correct; eauto. unfold verify_schedule in EQ2.*) - (*destruct (bblock_simub _ _); auto; try discriminate.*) -(*Qed.*) - Theorem verified_schedule_correct: forall ge f bb bb', verified_schedule bb = OK bb' -> bblock_simu lk ge f bb bb'. Proof. -(* intros. - assert (size bb = size bb'). { apply verified_schedule_size. auto. } - unfold verified_schedule in H. monadInv H. + intros. + monadInv H. eapply bblock_simub_correct. - unfold do_schedule in EQ. unfold verify_schedule in EQ0. - - destruct (bblock_simub _ _) in *; try discriminate. - destruct schedule. - simpl. unfold bblock_simub. - - eapply bblock_simub_correct. - destruct (bblock_simub); try discriminate. - - destruct schedule. - unfold bblock_simu, exec_bblock. destruct (exit bb). destruct c. destruct i. - - - intros rs m rs' m' t (rs1 & m1 & EBDY & EXT). - - eexists; eexists; split. - simpl. unfold exec_body. - - all: try (eapply verified_schedule_nob_correct; eauto; fail). - inv H. eexists; eexists; split; simpl; auto. constructor; auto. simpl; auto. constructor; auto. -Qed. *) -Admitted. -(*Lemma verified_schedule_builtin_idem:*) - (*forall bb ef args res lbb,*) - (*exit bb = Some (PExpand (Pbuiltin ef args res)) ->*) - (*verified_schedule bb = OK lbb ->*) - (*lbb = bb :: nil.*) -(*Proof.*) - (*intros. unfold verified_schedule in H0. rewrite H in H0. inv H0. reflexivity.*) -(*Qed.*) + destruct (bblock_simub _ _) in *; try discriminate; auto. +Qed. End verify_schedule. -- cgit