intermediate lemma for opt_simu intro case

1 files changed, 21 insertions, 10 deletions

diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index 7d58de5a..f5ea9fdc 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -243,6 +243,24 @@ 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),
+      omeasure oib < omeasure (Some ib) /\
+      t = E0 /\ match_states oib s1' (State st' f' sp pcB0 rs0 m0).
+Admitted.
+
 Theorem opt_simu s1 t s1' oib s2:
  RTL.step ge s1 t s1' ->
  match_states oib s1 s2 ->
@@ -253,15 +271,8 @@ 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.
+    intros (oib' & SIMU); exists oib'; right; assumption.
   - (* Callstate *)
     inv H.
     + (* Internal function *)
@@ -295,7 +306,7 @@ Proof.
     + econstructor; eauto.
       eapply code_right_assoc; eauto.
       constructor.
-Admitted.
+Qed.
 
 Local Hint Resolve plus_one star_refl: core.