some advance

1 files changed, 191 insertions, 24 deletions

diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index cebf867b..4d785c10 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -260,17 +260,17 @@ Proof.
       intros (pc'1 & LNZ & REV). exists pc'1. split; auto. congruence.
 Qed.
 
-(*
 
-TODO Version avec ofin2 quelconque
+(*TODO Is this lemma too hard to read? *)
 
-(*Lemma expand_iblock_istep_rec_correct sp ib rs0 m0 rs1 m1 ofin1:
+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 fin2 rs2 m2
+  k ofin2 rs2 m2
   (CONT: match ofin1 with
          | None =>
-             exists rem, k = Some rem /\ ofin2=Some fin2
-             /\ iblock_istep tge sp rs1 m1 rem rs2 m2 (Some fin2)
+             (k = None /\ rs2=rs1 /\ m2=m1 /\ ofin2 = None)
+             \/ (exists rem, k = Some rem
+                /\ iblock_istep tge sp rs1 m1 rem rs2 m2 ofin2)
          | Some fin1 => rs2=rs1 /\ m2=m1 /\ ofin2=Some fin1
          end),
   iblock_istep tge sp rs0 m0 (expand ib k) rs2 m2 ofin2.
@@ -278,26 +278,31 @@ Proof.
   induction 1; simpl.
   { (* BF *)
     destruct k;
-    intros ? ? ? ? (HRS & HM & HOF); subst.
+    intros ? ? ? (HRS & HM & HOF); subst.
     eapply exec_seq_stop. all: constructor. }
+    (*destruct k; intros. try inv CONT.*)
   1-4: (* Bnop, Bop, Bload, Bstore *)
-    destruct k; intros ? ? ? ? (rem & EQR & EQO & ISTEP);
-    inversion EQR; subst; clear EQR;
+    destruct k; intros; destruct CONT as [[HK [HRS [HM HO]]]|[rem [HR ISTEP]]];
+    subst; try (inv HK; fail); try (inv HR; fail); try (econstructor; eauto; fail);
+    inversion HR; subst; clear HR;
     eapply exec_seq_continue; [ econstructor; eauto | assumption].
   - (* Bseq_stop *)
     destruct k; intros; apply IHISTEP; eauto.
   - (* Bseq_continue *)
     destruct ofin; intros.
-    destruct CONT as [HRS [HM HOF]]; subst.
-    2: destruct CONT as [rem [HRS [HM HOF]]]; subst.
-    all: eapply IHISTEP1; eexists; repeat split; eauto.
+    + destruct CONT as [HRS [HM HOF]]; subst.
+      eapply IHISTEP1; right. eexists; repeat split; eauto.
+    + destruct CONT as [[HK [HRS [HM HO]]]|[rem [HR ISTEP]]]; subst.
+      * eapply IHISTEP1; right. eexists; repeat split; eauto.
+        eapply IHISTEP2; left; simpl; auto.
+      * eapply IHISTEP1; right. eexists; repeat split; eauto.
   - (* Bcond *)
     destruct ofin; intros;
     econstructor; eauto;
     destruct b; eapply IHISTEP; eauto.
-   Qed.*)
- *)
+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
@@ -327,20 +332,182 @@ Proof.
     destruct ofin; intros;
     econstructor; eauto;
     destruct b; eapply IHISTEP; auto.
-Qed.
+   Qed.*)
 
-Lemma expand_iblock_istep_correct sp ib rs0 m0 rs1 m1 fin:
-  iblock_istep tge sp rs0 m0 ib rs1 m1 (Some fin) ->
-  iblock_istep tge sp rs0 m0 (expand ib None) rs1 m1 (Some fin).
+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.
 Proof.
-  intros; eapply expand_iblock_istep_rec_correct; eauto; simpl; auto.
+  intros; eapply expand_iblock_istep_rec_correct; eauto.
+  destruct ofin; simpl; auto.
 Qed.
 
-(* TODO *)
-Lemma expand_iblock_istep_exact sp rs0 m0 rs1 m1:
-  forall ib fin (ISTEP: iblock_istep tge sp rs0 m0 (expand ib None) rs1 m1 (Some fin)),
-  iblock_istep tge sp rs0 m0 ib rs1 m1 (Some fin).
-Admitted.
+(* 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.*)
+
+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. (*
+  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.
+    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 =>
+             exists rem, k = Some rem
+             /\ match_iblock dupmap cfg isfst pc rem (Some fin2)
+         | Some fin => fin2=fin
+         end),
+  match_iblock dupmap cfg isfst pc (expand ib k) (Some fin2).
+Proof.
+  induction 1; simpl.
+  { destruct k.
+    intros; subst. econstructor. econstructor.
+    eapply exec_seq_stop. all: constructor. }
+
+   Qed.*)
 
 (** * Match strong state property