new strong_state predicate and lemma

1 files changed, 72 insertions, 38 deletions

diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index 1fa13242..eb4734b8 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -102,8 +102,8 @@ The simulation diagram for match_states_intro is as follows:
 >>
 *)
 
-Inductive match_states: (option iblock) -> RTL.state -> state -> Prop :=
-  | match_states_intro (* TODO: LES DETAILS SONT SANS DOUTE A REVOIR !!! *)
+Inductive match_strong_state: (option iblock) -> RTL.state -> state -> Prop :=
+  | match_strong_state_intro
       ib dupmap st f sp rs m st' f' pcB0 pcR0 pcR1 rs0 m0 isfst ib0
       (STACKS: list_forall2 match_stackframes st st')
       (TRANSF: match_function dupmap f f')
@@ -113,6 +113,14 @@ Inductive match_states: (option iblock) -> RTL.state -> state -> Prop :=
       (IS_EXPD: is_expand 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 ib0.(entry) rs0 m0 = iblock_istep_run tge sp ib rs m)
+      : match_strong_state (Some ib) (RTL.State st f sp pcR1 rs m) (State st' f' sp pcB0 rs0 m0)
+  .
+
+Inductive match_states: (option iblock) -> RTL.state -> state -> Prop :=
+  | match_states_intro (* TODO: LES DETAILS SONT SANS DOUTE A REVOIR !!! *)
+      ib st f sp rs m st' f' pcB0 pcR1 rs0 m0
+      (MSTRONG: match_strong_state (Some ib) (RTL.State st f sp pcR1 rs m) (State st' f' sp pcB0 rs0 m0))
+      (NGOTO: is_goto ib = false)
       : match_states (Some ib) (RTL.State st f sp pcR1 rs m) (State st' f' sp pcB0 rs0 m0)
   | match_states_call
       st st' f f' args m
@@ -123,7 +131,24 @@ Inductive match_states: (option iblock) -> RTL.state -> state -> Prop :=
       st st' v m
       (STACKS: list_forall2 match_stackframes st st')
       : match_states None (RTL.Returnstate st v m) (Returnstate st' v m)
-   .
+  .
+
+Lemma match_strong_state_equiv sp st st' ib f f' rs m rs0 m0 pcB0 pcR1:
+  match_strong_state (Some ib) (RTL.State st f sp pcR1 rs m) (State st' f' sp pcB0 rs0 m0) ->
+  match is_goto ib with
+  | true =>
+      exists ib' succ,
+        iblock_istep tge sp rs0 m0 (entry ib') rs m (Some (Bgoto succ))
+  | false => match_states (Some ib) (RTL.State st f sp pcR1 rs m) (State st' f' sp pcB0 rs0 m0)
+  end.
+Proof.
+  destruct (is_goto ib) eqn:EQ.
+  - intros. destruct ib; try destruct fi; try discriminate.
+    inv H. simpl in BTL_RUN.
+    rewrite <- iblock_istep_run_equiv in BTL_RUN.
+    repeat eexists; eauto.
+  - intros. econstructor; eauto.
+Qed.
 
 Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s.
 Proof.
@@ -227,24 +252,34 @@ Proof.
   induction ib; simpl; auto; lia.
 Qed.
 
+Lemma list_nth_z_rev_dupmap:
+  forall dupmap ln ln' (pc pc': node) val,
+  list_nth_z ln val = Some pc ->
+  list_forall2 (fun n' n => dupmap!n' = Some n) ln' ln ->
+  exists (pc': node),
+     list_nth_z ln' val = Some pc'
+  /\ dupmap!pc' = Some pc.
+Proof.
+  induction ln; intros until val; intros LNZ LFA.
+  - inv LNZ.
+  - inv LNZ. destruct (zeq val 0) eqn:ZEQ.
+    + inv H0. destruct ln'; inv LFA.
+      simpl. exists p. split; auto.
+    + inv LFA. simpl. rewrite ZEQ. exploit IHln. 2: eapply H0. all: eauto.
+      intros (pc'1 & LNZ & REV). exists pc'1. split; auto. congruence.
+Qed.
+
 Lemma opt_simu_intro
-  sp f f' st st' dupmap isfst pcR0 pcR1 pcB0 ib ib0 rs m rs0 m0 t s1'
+  sp f f' st st' pcR1 pcB0 ib 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)
-  (IS_EXPD : is_expand 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)
+  (MSTRONG : match_strong_state (Some ib) (RTL.State st f sp pcR1 rs m)
+              (State st' f' sp pcB0 rs0 m0))
+  (NGOTO : is_goto ib = false)
   : 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.
+  inv MSTRONG. inv MIB.
   - (* mib_BF *)
     inv H0;
     inversion STEP; subst; try_simplify_someHyps; intros.
@@ -293,32 +328,31 @@ Proof.
         pose symbols_preserved as SYMPRES.
         eapply eval_builtin_args_preserved; eauto.
         eapply external_call_symbols_preserved; eauto. eapply senv_preserved.
-      * econstructor; eauto. eapply code_expand; eauto.
-        apply star_refl.
+      * econstructor; eauto.
+        { econstructor; eauto. eapply code_expand; eauto.  
+          apply star_refl. }
+        inversion MI; subst; try_simplify_someHyps.
+        inv H3; try_simplify_someHyps.
     + (* Bjumptable *)
-      admit.
-      (* eexists; left; eexists; split.
+      exploit list_nth_z_rev_dupmap; eauto.
+      intros (pc'0 & LNZ & DM).
+      eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC.
+      remember DM as ODUPLIC; clear HeqODUPLIC.
+      apply DMC in DM as [ib [FNC MI]]; clear DMC.
+      eexists; left; eexists; split.
       * econstructor; eauto. econstructor.
         eexists; eexists; split.
         eapply iblock_istep_run_equiv in BTL_RUN.
         eapply BTL_RUN. econstructor; eauto.
-        exploit (list_nth_z_dupmap dupmap ln' ln); eauto.
-       * econstructor; eauto.*)
+      * econstructor; eauto.
+        { econstructor; eauto. eapply code_expand; eauto.  
+          apply star_refl. }
+        inversion MI; subst; try_simplify_someHyps.
+        inv H4; try_simplify_someHyps.
   - (* mib_exit *)
-    (* exists None; right; repeat (split; auto).
-      inversion STEP; subst; try_simplify_someHyps.
-      eexists; left. eexists; split.
-      econstructor; eauto. econstructor.
-      eexists; eexists; split.
-      eapply iblock_istep_run_equiv in BTL_RUN.
-      eapply BTL_RUN. econstructor. econstructor; eauto.
-      inv BTL_RUN.
-    + eapply exec_iblock; eauto.
-      econstructor; repeat eexists.
-      inv STEP.
-       eapply exec_Bgoto.*) admit.
-  - (* mib_seq *)
-    inv H.
+    discriminate.
+  - (* mib_seq *) admit.
+    (* inv H.
     + (* Bnop *)
       inversion STEP; subst; try_simplify_someHyps.
       exists (Some b2); right; repeat (split; auto).
@@ -351,8 +385,8 @@ Proof.
     + (* Absurd case *)
       inv IS_EXPD. inv H4. inv H.
     + (* Absurd Bcond (Bcond are not allowed in the left part of a Bseq *)
-      inv IS_EXPD; discriminate.
-  - (* mib_cond *)
+              inv IS_EXPD; discriminate.*)
+  - (* mib_cond *) admit. (*
     inversion STEP; subst; try_simplify_someHyps.
     intros; rewrite H12 in BTL_RUN. destruct b.
     * (* Ifso *)
@@ -366,7 +400,7 @@ Proof.
       simpl; assert (measure bso > 0) by apply measure_pos; lia.
       inv H2; econstructor; eauto.
       1,3: inv IS_EXPD; auto; discriminate.
-      all: eapply star_right; eauto.
+                             all: eapply star_right; eauto.*)
 Admitted.
 
 (** * Main RTL to BTL simulation theorem