1 files changed, 71 insertions, 10 deletions
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index 7c9fb456..efc22eb6 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -245,6 +245,75 @@ Definition omeasure (oib: option iblock): nat :=
  | Some ib => measure ib
  end.
 
+Lemma opt_simu_intro
+  sp f f' st st' dupmap isfst pcR0 pcR1 pcB0 ib ib0 rs m rs0 m0 t s1'
+  (STEP : RTL.step ge (RTL.State st f sp pcR1 rs m) t s1')
+  (STACKS : list_forall2 match_stackframes st st')
+  (TRANSF : match_function dupmap f f')
+  (ATpc0 : (fn_code f') ! pcB0 = Some ib0)
+  (DUPLIC : dupmap ! pcB0 = Some pcR0)
+  (MIB : match_iblock dupmap (RTL.fn_code f) isfst pcR1 ib None)
+  (RIGHTA : is_right_assoc ib)
+  (RTL_RUN : star RTL.step ge (RTL.State st f sp pcR0 rs0 m0) E0
+              (RTL.State st f sp pcR1 rs m))
+  (BTL_RUN : iblock_istep_run tge sp (entry ib0) rs0 m0 =
+            iblock_istep_run tge sp ib rs m)
+  : exists (oib' : option iblock),
+     (exists s2', step tge (State st' f' sp pcB0 rs0 m0) t s2' /\ match_states oib' s1' s2')
+  \/ (omeasure oib' < omeasure (Some ib) /\ t=E0 /\ match_states oib' s1' (State st' f' sp pcB0 rs0 m0)).
+Proof.
+  inv MIB.
+  - (* mib_BF *)
+    admit.
+  - (* mib_exit *)
+    (*
+      simpl in *.
+      eapply iblock_istep_run_equiv in BTL_RUN.
+      inv BTL_RUN.
+    eexists; left. eexists; split.
+    + eapply exec_iblock; eauto.
+      econstructor; repeat eexists.
+      inv STEP.
+       eapply exec_Bgoto.*) admit.
+  - (* mib_seq *)
+    inv H.
+    + (* Bnop *)
+      inversion STEP; subst; try_simplify_someHyps. (* TODO maybe move that for each subcase *)
+      exists (Some b2); right; repeat (split; auto).
+      econstructor; eauto. inv RIGHTA; auto; discriminate.
+      eapply star_right; eauto.
+    + (* Bop *)
+      inversion STEP; subst; try_simplify_someHyps.
+      exists (Some b2); right; repeat (split; auto).
+      econstructor; eauto. inv RIGHTA; auto; discriminate.
+      eapply star_right; eauto.
+      erewrite eval_operation_preserved in H10.
+      erewrite H10 in BTL_RUN; simpl in BTL_RUN; auto.
+      intros; rewrite <- symbols_preserved; trivial.
+    + (* Bload *)
+      inversion STEP; subst; try_simplify_someHyps.
+      exists (Some (b2)); right; repeat (split; auto).
+      econstructor; eauto. inv RIGHTA; auto; discriminate.
+      eapply star_right; eauto.
+      erewrite eval_addressing_preserved in H10.
+      erewrite H10, H11 in BTL_RUN; simpl in BTL_RUN; auto.
+      intros; rewrite <- symbols_preserved; trivial.
+    + (* Bstore *)
+      inversion STEP; subst; try_simplify_someHyps.
+      exists (Some b2); right; repeat (split; auto).
+      econstructor; eauto. inv RIGHTA; auto; discriminate.
+      eapply star_right; eauto.
+      erewrite eval_addressing_preserved in H10.
+      erewrite H10, H11 in BTL_RUN; simpl in BTL_RUN; auto.
+      intros; rewrite <- symbols_preserved; trivial.
+    + (* Absurd case *)
+      inv RIGHTA. inv H4. inv H.
+    + (* Bcond *)
+      admit.
+  - (* mib_cond *)
+    admit.
+Admitted.
+
 Theorem opt_simu s1 t s1' oib s2:
  RTL.step ge s1 t s1' ->
  match_states oib s1 s2 ->
@@ -255,15 +324,7 @@ Theorem opt_simu s1 t s1' oib s2:
 Proof.
   inversion 2; subst; clear H0.
   - (* State *)
-    inv H.
-
-    1: { (* Inop *)
-      eexists; right; split.
-      2: split; trivial.
-      2: {
-        econstructor; eauto.
-        all: admit. } admit. }
-    all: admit. 
+    exploit opt_simu_intro; eauto.
   - (* Callstate *)
     inv H.
     + (* Internal function *)
@@ -297,7 +358,7 @@ Proof.
     + econstructor; eauto.
       eapply code_right_assoc; eauto.
       constructor.
-Admitted.
+Qed.
 
 Local Hint Resolve plus_one star_refl: core.