mib lemma

1 files changed, 29 insertions, 26 deletions

diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index 4d7508f1..faf0b76c 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -407,39 +407,42 @@ Proof.
     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
+Lemma expand_matchiblock_rec_correct dupmap cfg ib pc isfst:
+  forall opc1
+  (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 false pc' rem opc2
+             k = None /\ opc2 = opc1 \/
+             (exists rem, k = Some rem
+             /\ match_iblock dupmap cfg false pc' rem opc2)
          | None => opc2=opc1
          end),
   match_iblock dupmap cfg isfst pc (expand ib k) opc2.
-Proof. Admitted.
-  (*
+Proof.
   induction 1; simpl.
-  { 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.
+  { (* BF *)
+    intros; inv CONT; econstructor; eauto. }
+  1-4: (* Bnop *)
+    destruct k; intros; destruct CONT as [[HK HO] | [rem [HR MIB]]];
+    try inv HK; try inv HO; try inv HR; repeat econstructor; eauto.
+  { (* Bgoto *)
+    intros; inv CONT; apply mib_exit; auto. }
+  { (* Bseq *)
+    intros. eapply IHMIB1. right. eexists; split; eauto. }
+  { (* Bcond *)
+    intros. inv H0;
+    econstructor; eauto; try econstructor.
+    destruct opc0; econstructor. }
+Qed.
 
-          Qed.*)
+Lemma expand_matchiblock_correct dupmap cfg ib pc isfst opc:
+  match_iblock dupmap cfg isfst pc ib opc ->
+  match_iblock dupmap cfg isfst pc (expand ib None) opc.
+Proof.
+  intros.
+  eapply expand_matchiblock_rec_correct; eauto.
+  destruct opc; simpl; auto.
+Qed.
 
 (** * Match strong state property