From 99e735af1f7726da2903409758bee202cf47c6a4 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 17 May 2021 16:02:57 +0200 Subject: Lemmas on ISTEP --- scheduling/RTLtoBTLproof.v | 320 ++++++++++++++++++--------------------------- 1 file changed, 126 insertions(+), 194 deletions(-) (limited to 'scheduling/RTLtoBTLproof.v') diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 4d785c10..4d7508f1 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -260,9 +260,6 @@ Proof. intros (pc'1 & LNZ & REV). exists pc'1. split; auto. congruence. Qed. - -(*TODO Is this lemma too hard to read? *) - Lemma expand_iblock_istep_rec_correct sp ib rs0 m0 rs1 m1 ofin1: forall (ISTEP: iblock_istep tge sp rs0 m0 ib rs1 m1 ofin1) k ofin2 rs2 m2 @@ -277,9 +274,8 @@ Lemma expand_iblock_istep_rec_correct sp ib rs0 m0 rs1 m1 ofin1: Proof. induction 1; simpl. { (* BF *) - destruct k; - intros ? ? ? (HRS & HM & HOF); subst. - eapply exec_seq_stop. all: constructor. } + intros ? ? ? ? (HRS & HM & HOF); subst. + constructor. } (*destruct k; intros. try inv CONT.*) 1-4: (* Bnop, Bop, Bload, Bstore *) destruct k; intros; destruct CONT as [[HK [HRS [HM HO]]]|[rem [HR ISTEP]]]; @@ -302,38 +298,6 @@ Proof. destruct b; eapply IHISTEP; eauto. Qed. -(* TODO old version -Lemma expand_iblock_istep_rec_correct sp ib rs0 m0 rs1 m1 ofin: - forall (ISTEP: iblock_istep tge sp rs0 m0 ib rs1 m1 ofin) - k fin2 rs2 m2 - (CONT: match ofin with - | None => - exists rem, k = Some rem - /\ iblock_istep tge sp rs1 m1 rem rs2 m2 (Some fin2) - | Some fin => rs2=rs1 /\ m2=m1 /\ fin2=fin - end), - iblock_istep tge sp rs0 m0 (expand ib k) rs2 m2 (Some fin2). -Proof. - induction 1; simpl. - { (* BF *) - destruct k; - intros ? ? ? (HRS & HM & HOF); subst. - eapply exec_seq_stop. all: constructor. } - 1-4: (* Bnop, Bop, Bload, Bstore *) - destruct k; intros ? ? ? (rem & EQR & ISTEP); - inversion EQR; subst; clear EQR; - eapply exec_seq_continue; [ econstructor; eauto | assumption]. - - (* Bseq_stop *) - destruct k; intros; apply IHISTEP; eauto. - - (* Bseq_continue *) - destruct ofin; intros; apply IHISTEP1; - eexists; split; eauto. - - (* Bcond *) - destruct ofin; intros; - econstructor; eauto; - destruct b; eapply IHISTEP; auto. - Qed.*) - Lemma expand_iblock_istep_correct sp ib rs0 m0 rs1 m1 ofin: iblock_istep tge sp rs0 m0 ib rs1 m1 ofin -> iblock_istep tge sp rs0 m0 (expand ib None) rs1 m1 ofin. @@ -342,172 +306,140 @@ Proof. destruct ofin; simpl; auto. Qed. -(* TODO Which approach should we use here? *) -Lemma expand_iblock_istep_exact sp: - forall ib ofin rs0 m0 rs1 m1 - (ISTEP: iblock_istep tge sp rs0 m0 (expand ib None) rs1 m1 ofin), - iblock_istep tge sp rs0 m0 ib rs1 m1 ofin. -Proof. Admitted. (* - induction ib; intros; - try (inv ISTEP; econstructor; eauto; fail). - - - rewrite iblock_istep_run_equiv in *. - inv ISTEP. simpl. - - - - destruct (iblock_istep_run tge sp (Bseq ib1 ib2) rs0 m0) eqn:?. - * destruct o. symmetry. - inv Heqo. - destruct (iblock_istep_run tge sp ib1 rs0 m0) eqn:?; try discriminate. - destruct o, _fin0 eqn:?; simpl in *. - rewrite <- iblock_istep_run_equiv in *. - eapply expand_iblock_istep_rec_correct; eauto. - inv Heqo0. simpl; auto. - rewrite H1. - rewrite <- iblock_istep_run_equiv in *. - eapply expand_iblock_istep_rec_correct; eauto. - simpl; right; eexists; split. eauto. - apply expand_iblock_istep_correct; auto. - * simpl in *. - destruct (iblock_istep_run tge sp ib1 rs0 m0) eqn:?; try discriminate. - destruct o; simpl in *. - destruct _fin eqn:?; simpl in *; try discriminate. - inv Heqo. - - inv ISTEP. simpl; repeat autodestruct; intros. - + destruct o; simpl in *. symmetry. - rewrite <- iblock_istep_run_equiv in *. - eapply expand_iblock_istep_rec_correct; eauto. - inv EQ. simpl; auto. - + destruct o; simpl in *. - rewrite H0. - rewrite <- iblock_istep_run_equiv in *. - destruct (iblock_istep_run tge sp ib2 _rs _m) eqn:?. - * eapply IHib2. destruct o. - rewrite <- iblock_istep_run_equiv in Heqo. - eapply expand_iblock_istep_rec_correct; eauto. - * destruct o; simpl in *. symmetry. - rewrite <- iblock_istep_run_equiv in *. - eapply expand_iblock_istep_rec_correct; eauto. - inv EQ; right. eexists; split. eauto. - apply expand_iblock_istep_correct; auto. - * destruct H0. - 2: { - rewrite iblock_istep_run_equiv in *. inv ISTEP. - destruct _fin eqn:?, o eqn:?; simpl in *. - 2:{ inv Heqo0. destruct ib1 - rewrite iblock_istep_run_equiv in *. inv ISTEP. - - - destruct ib1 eqn:?; simpl in *. - + rewrite iblock_istep_run_equiv in *. - simpl in *. auto. - + repeat econstructor. - rewrite iblock_istep_run_equiv in ISTEP. - simpl in *. - rewrite <- iblock_istep_run_equiv in ISTEP. - apply IHib2; auto. - + rewrite iblock_istep_run_equiv in ISTEP. - simpl in *. - destruct (eval_operation _ _ _ _) eqn:?; try discriminate. - repeat econstructor. eauto. simpl in *. - rewrite <- iblock_istep_run_equiv in ISTEP. - apply IHib2; auto. - + rewrite iblock_istep_run_equiv in ISTEP. - simpl in *. - destruct trap eqn:?; try discriminate. - destruct (eval_addressing _ _ _ _) eqn:?; try discriminate. - destruct (Mem.loadv _ _ _) eqn:?; try discriminate. - repeat econstructor; eauto. simpl in *. - rewrite <- iblock_istep_run_equiv in ISTEP. - apply IHib2; auto. - + rewrite iblock_istep_run_equiv in ISTEP. - simpl in *. - destruct (eval_addressing _ _ _ _) eqn:?; try discriminate. - destruct (Mem.storev _ _ _) eqn:?; try discriminate. - repeat econstructor; eauto. simpl in *. - rewrite <- iblock_istep_run_equiv in ISTEP. - apply IHib2; auto. - + destruct ofin. - * econstructor; eauto. simpl in *. - eapply IHib1; eauto. - - - - - eapply IHib1. - rewrite iblock_istep_run_equiv in *; simpl in *. - inv ISTEP. - destruct (iblock_istep_run tge sp ib1 rs0 m0) eqn:EQib1. - destruct _fin, o. inv ISTEP. - rewrite iblock_istep_run_equiv in *. - - destruct ib1; simpl in *. - + eapply IHib1. inv ISTEP.*) +(* TODO useless? *) +Lemma expand_iblock_istep_run_Some_rec sp ib rs0 m0 rs1 m1 ofin1: + forall (ISTEP: iblock_istep_run tge sp ib rs0 m0 = + Some {| _rs := rs1; _m := m1; _fin := ofin1 |}) + k ofin2 rs2 m2 + (CONT: match ofin1 with + | None => + (k = None /\ rs2=rs1 /\ m2=m1 /\ ofin2 = None) + \/ (exists rem, k = Some rem + /\ iblock_istep_run tge sp rem rs1 m1 = + Some {| _rs := rs2; _m := m2; _fin := ofin2 |}) + | Some fin1 => rs2=rs1 /\ m2=m1 /\ ofin2=Some fin1 + end), + iblock_istep_run tge sp (expand ib k) rs0 m0 = + Some {| _rs := rs2; _m := m2; _fin := ofin2 |}. +Proof. + intros. destruct ofin1; + rewrite <- iblock_istep_run_equiv in *. + - destruct CONT as [HRS [HM HO]]; subst. + eapply expand_iblock_istep_rec_correct; eauto. + simpl; auto. + - eapply expand_iblock_istep_rec_correct; eauto. + simpl. destruct CONT as [HL | [rem [HR ISTEP']]]. + left; auto. rewrite <- iblock_istep_run_equiv in ISTEP'. + right; eexists; split; eauto. +Qed. + +Lemma expand_iblock_istep_run_None_rec sp ib: + forall rs0 m0 o k + (ISTEP: iblock_istep_run tge sp ib rs0 m0 = o) + (CONT: match o with + | Some (out rs1 m1 ofin) => + exists rem, + k = Some rem /\ ofin = None /\ + iblock_istep_run tge sp rem rs1 m1 = None + | _ => True + end), + iblock_istep_run tge sp (expand ib k) rs0 m0 = None. +Proof. + induction ib; simpl; + try discriminate. + - (* BF *) + intros; destruct o; try discriminate; simpl in *. + inv ISTEP. destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; inv HO. + - (* Bnop *) + intros; destruct o; inv ISTEP; destruct k; + destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; inv HO; trivial. + - (* Bop *) + intros; destruct o; + destruct (eval_operation _ _ _ _ _) eqn:EVAL; inv ISTEP; destruct k; + simpl; rewrite EVAL; auto; destruct CONT as [rem [HR [HO ISTEP]]]; + inv HR; inv HO; trivial. + - (* Bload *) + intros; destruct o; + destruct (trap) eqn:TRAP; + try destruct (eval_addressing _ _ _ _) eqn:EVAL; + try destruct (Mem.loadv _ _ _) eqn:MEM; inv ISTEP; destruct k; + simpl; try rewrite EVAL; try rewrite MEM; simpl; auto; + destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; inv HO; trivial. + - (* Bstore *) + intros; destruct o; + destruct (eval_addressing _ _ _ _) eqn:EVAL; + try destruct (Mem.storev _ _ _) eqn:MEM; inv ISTEP; destruct k; + simpl; try rewrite EVAL; try rewrite MEM; simpl; auto; + destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; inv HO; trivial. + - (* Bseq *) + intros. + eapply IHib1; eauto. + destruct (iblock_istep_run tge sp ib1 rs0 m0) eqn:EQib1; try auto. + destruct o0. eexists; split; eauto. simpl in *. + destruct _fin; inv ISTEP. + + destruct CONT as [rem [_ [CONTRA _]]]; inv CONTRA. + + split; auto. eapply IHib2; eauto. + - (* Bcond *) + intros; destruct (eval_condition _ _ _); trivial. + destruct b. + + eapply IHib1; eauto. + + eapply IHib2; eauto. +Qed. + +Lemma expand_preserves_iblock_istep_run_None sp ib: + forall rs m, iblock_istep_run tge sp ib rs m = None + -> iblock_istep_run tge sp (expand ib None) rs m = None. +Proof. + intros; eapply expand_iblock_istep_run_None_rec; eauto. + simpl; auto. +Qed. Lemma expand_preserves_iblock_istep_run sp ib: forall rs m, iblock_istep_run tge sp ib rs m = iblock_istep_run tge sp (expand ib None) rs m. -Proof. Admitted. (* +Proof. intros. - destruct (iblock_istep_run tge sp (expand ib None) rs m) eqn:ISTEP. - (*destruct (iblock_istep_run tge sp ib rs m) eqn:ISTEP.*) - - destruct o. + destruct (iblock_istep_run tge sp ib rs m) eqn:ISTEP. + - destruct o. symmetry. rewrite <- iblock_istep_run_equiv in *. - apply expand_iblock_istep_exact; auto. - - generalize dependent ib. - generalize dependent rs. - generalize dependent m. - induction ib; - try (intros; inv ISTEP; simpl; try autodestruct; fail). - + intros. inv ISTEP. simpl.*) - (* TODO Should we keep the None case in this lemma ? - destruct (iblock_istep_run tge sp ib1 rs m) eqn:EQib1; auto. - destruct o, _fin; simpl in *. - discriminate IHib1. - inv H0. - destruct IHib1. - rewrite <- iblock_istep_run_equiv in EQib1. - apply expand_iblock_istep_correct in EQib1. - discriminate IHib1. - apply EQib1 in IHib1. - inv EQib1. - 2: {, - destruct (iblock_istep_run tge sp (expand ib1 None) rs m) eqn:EQib1. - discriminate IHib1. - discriminate IHib1. - - - induction ib; try (simpl; auto; fail). - - intros. simpl. repeat autodestruct; intros. - + destruct o. symmetry. - rewrite <- iblock_istep_run_equiv in *. - simpl in EQ; rewrite EQ. - eapply expand_iblock_istep_rec_correct; eauto. - rewrite EQ; simpl; auto. - + destruct o. simpl in *. inv EQ. - rewrite <- iblock_istep_run_equiv in *. - 2: { intros. inv EQ. - - simpl.*) - -(* TODO -Lemma expand_matchiblock_rec_correct dupmap cfg ib pc isfst opc: - forall (MIB: match_iblock dupmap cfg isfst pc ib opc) - k fin2 - (CONT: match opc with - | None => + apply expand_iblock_istep_correct; auto. + - symmetry. + apply expand_preserves_iblock_istep_run_None; auto. +Qed. + +Lemma expand_matchiblock_rec_correct dupmap cfg ib pc isfst opc1: + forall (MIB: match_iblock dupmap cfg isfst pc ib opc1) + k opc2 + (CONT: match opc1 with + | Some pc' => exists rem, k = Some rem - /\ match_iblock dupmap cfg isfst pc rem (Some fin2) - | Some fin => fin2=fin + /\ match_iblock dupmap cfg false pc' rem opc2 + | None => opc2=opc1 end), - match_iblock dupmap cfg isfst pc (expand ib k) (Some fin2). -Proof. + match_iblock dupmap cfg isfst pc (expand ib k) opc2. +Proof. Admitted. + (* induction 1; simpl. - { destruct k. - intros; subst. econstructor. econstructor. - eapply exec_seq_stop. all: constructor. } + { admit. (* TODO we should add the seq_None constructor for this case ? *) } + + 1-4: (* Bnop, Bop, Bload, Bstore *) + destruct k; intros ? (rem & HR & MIB); inv HR; + repeat econstructor; eauto. + + { admit. (* What to do if a goto is the left child of a seq ? *) } + + - (* Bseq_continue *) + destruct opc; intros. + + destruct CONT as [rem [HR MIB]]; subst. + eapply IHMIB1. eexists; repeat split; eauto. + + inv CONT. eapply IHMIB1. eexists; repeat split; eauto. + - (* Bcond *) + destruct opc; intros. + + econstructor; eauto. + eapply IHMIB1; eauto. + autodestruct. intros EQ; inv EQ. - Qed.*) + Qed.*) (** * Match strong state property -- cgit