iblock_istep rec and correct lemmas

1 files changed, 83 insertions, 0 deletions

diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index 93f83450..cebf867b 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -260,6 +260,88 @@ Proof.
       intros (pc'1 & LNZ & REV). exists pc'1. split; auto. congruence.
 Qed.
 
+(*
+
+TODO Version avec ofin2 quelconque
+
+(*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
+  (CONT: match ofin1 with
+         | None =>
+             exists rem, k = Some rem /\ ofin2=Some fin2
+             /\ iblock_istep tge sp rs1 m1 rem rs2 m2 (Some fin2)
+         | Some fin1 => rs2=rs1 /\ m2=m1 /\ ofin2=Some fin1
+         end),
+  iblock_istep tge sp rs0 m0 (expand ib k) rs2 m2 ofin2.
+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 & EQO & 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.
+    destruct CONT as [HRS [HM HOF]]; subst.
+    2: destruct CONT as [rem [HRS [HM HOF]]]; subst.
+    all: eapply IHISTEP1; eexists; repeat split; eauto.
+  - (* Bcond *)
+    destruct ofin; intros;
+    econstructor; eauto;
+    destruct b; eapply IHISTEP; eauto.
+   Qed.*)
+ *)
+
+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 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).
+Proof.
+  intros; eapply expand_iblock_istep_rec_correct; eauto; 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.
+
 (** * Match strong state property
 
 Used when executing non-atomic instructions such as Bseq/Bcond(ib1,ib2).
@@ -291,6 +373,7 @@ See explanations of opt_simu below.
 
 >>
 *)
+
 Lemma match_strong_state_simu
   dupmap st st' f f' sp rs2 m2 rs1 m1 rs0 m0 pcB0 pcR0 pcR1 pcR2 isfst ib1 ib2 ib0 n
   (STEP : RTL.step ge (RTL.State st f sp pcR1 rs1 m1) E0 (RTL.State st f sp pcR2 rs2 m2))