Lemmas on ISTEP

1 files changed, 126 insertions, 194 deletions

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