new lemma definition, some preparations in existing proofs

1 files changed, 65 insertions, 52 deletions

diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index eb4734b8..d9fec468 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -102,9 +102,8 @@ The simulation diagram for match_states_intro is as follows:
 >>
 *)
 
-Inductive match_strong_state: (option iblock) -> RTL.state -> state -> Prop :=
+Inductive match_strong_state dupmap st st' f f' sp rs m rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst: 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')
       (ATpc0: (fn_code f')!pcB0 = Some ib0)
@@ -113,13 +112,13 @@ Inductive match_strong_state: (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)
+      : match_strong_state dupmap st st' f f' sp rs m rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst
   .
 
 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))
+      dupmap st st' f f' sp rs m rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst
+      (MSTRONG: match_strong_state dupmap st st' f f' sp rs m rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst)
       (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
@@ -133,23 +132,6 @@ Inductive match_states: (option iblock) -> RTL.state -> state -> Prop :=
       : 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.
   rewrite <- (Genv.find_symbol_match TRANSL). reflexivity.
@@ -252,6 +234,15 @@ Proof.
   induction ib; simpl; auto; lia.
 Qed.
 
+Lemma entry_isnt_goto dupmap f pc ib:
+  match_iblock dupmap (RTL.fn_code f) true pc (entry ib) None ->
+  is_goto (entry ib) = false.
+Proof.
+  intros.
+  destruct (entry ib); trivial.
+  destruct fi; trivial. inv H. inv H4.
+Qed.
+
 Lemma list_nth_z_rev_dupmap:
   forall dupmap ln ln' (pc pc': node) val,
   list_nth_z ln val = Some pc ->
@@ -269,17 +260,29 @@ Proof.
       intros (pc'1 & LNZ & REV). exists pc'1. split; auto. congruence.
 Qed.
 
+Lemma match_strong_state_simu
+  dupmap st st' f f' sp rs m rs0 m0 rs1 m1 pcB0 pcR0 pcR1 pcR2 isfst ib1 ib2 ib0 t
+  (STEP : RTL.step ge (RTL.State st f sp pcR1 rs m) t (RTL.State st f sp pcR2 rs1 m1))
+  (MSS1 : match_strong_state dupmap st st' f f' sp rs m rs0 m0 pcB0 pcR0 pcR1 ib1 ib0 isfst)
+  (MSS2 : match_strong_state dupmap st st' f f' sp rs1 m1 rs0 m0 pcB0 pcR0 pcR2 ib2 ib0 false)
+  (*(MES  : measure ib2 < measure ib1)*)
+  : exists (oib' : option iblock),
+      (exists s2', step tge (State st' f' sp pcB0 rs0 m0) E0 s2'
+          /\ match_states oib' (RTL.State st f sp pcR2 rs1 m1) s2')
+      \/ (omeasure oib' < S (measure ib2) /\ t=E0
+          /\ match_states oib' (RTL.State st f sp pcR2 rs1 m1) (State st' f' sp pcB0 rs0 m0)).
+Proof. Admitted.
+
 Lemma opt_simu_intro
-  sp f f' st st' pcR1 pcB0 ib rs m rs0 m0 t s1'
+  dupmap st st' f f' sp rs m rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst s1' t
   (STEP : RTL.step ge (RTL.State st f sp pcR1 rs m) t s1')
-  (MSTRONG : match_strong_state (Some ib) (RTL.State st f sp pcR1 rs m)
-              (State st' f' sp pcB0 rs0 m0))
+  (MSTRONG : match_strong_state dupmap st st' f f' sp rs m rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst)
   (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 MSTRONG. inv MIB.
+  inversion MSTRONG; subst. inv MIB.
   - (* mib_BF *)
     inv H0;
     inversion STEP; subst; try_simplify_someHyps; intros.
@@ -351,45 +354,54 @@ Proof.
         inv H4; try_simplify_someHyps.
   - (* mib_exit *)
     discriminate.
-  - (* mib_seq *) admit.
-    (* inv H.
+  - (* mib_seq *)
+    inversion H; subst.
     + (* Bnop *)
-      inversion STEP; subst; try_simplify_someHyps.
-      exists (Some b2); right; repeat (split; auto).
-      econstructor; eauto. inv IS_EXPD; auto; discriminate.
+      inversion STEP; subst; try_simplify_someHyps; intros.
+      eapply match_strong_state_simu.
+      1,2: do 2 (econstructor; eauto).
+      econstructor; eauto. (* TODO factorize *)
+      inv IS_EXPD; eauto. simpl in *; discriminate.
       eapply star_right; eauto.
     + (* Bop *)
-      inversion STEP; subst; try_simplify_someHyps.
-      exists (Some b2); right; repeat (split; auto).
-      econstructor; eauto. inv IS_EXPD; auto; discriminate.
+      inversion STEP; subst; try_simplify_someHyps; intros.
+      eapply match_strong_state_simu.
+      1,2: do 2 (econstructor; eauto).
+      econstructor; eauto. (* TODO factorize *)
+      inv IS_EXPD; eauto. simpl in *; discriminate.
       eapply star_right; eauto.
-      erewrite eval_operation_preserved in H10.
-      erewrite H10 in BTL_RUN; simpl in BTL_RUN; auto.
+      erewrite eval_operation_preserved in H11.
+      erewrite H11 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 IS_EXPD; auto; discriminate.
+      inversion STEP; subst; try_simplify_someHyps; intros.
+      eapply match_strong_state_simu.
+      1,2: do 2 (econstructor; eauto).
+      econstructor; eauto. (* TODO factorize *)
+      inv IS_EXPD; eauto. simpl in *; discriminate.
       eapply star_right; eauto.
-      erewrite eval_addressing_preserved in H10.
-      erewrite H10, H11 in BTL_RUN; simpl in BTL_RUN; auto.
+      erewrite eval_addressing_preserved in H11.
+      erewrite H11, H12 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 IS_EXPD; auto; discriminate.
+      inversion STEP; subst; try_simplify_someHyps; intros.
+      eapply match_strong_state_simu.
+      1,2: do 2 (econstructor; eauto).
+      econstructor; eauto. (* TODO factorize *)
+      inv IS_EXPD; eauto. simpl in *; discriminate.
       eapply star_right; eauto.
-      erewrite eval_addressing_preserved in H10.
-      erewrite H10, H11 in BTL_RUN; simpl in BTL_RUN; auto.
+      erewrite eval_addressing_preserved in H11.
+      erewrite H11, H12 in BTL_RUN; simpl in BTL_RUN; auto.
       intros; rewrite <- symbols_preserved; trivial.
     + (* Absurd case *)
-      inv IS_EXPD. inv H4. inv H.
+      inv IS_EXPD; try inv H5; discriminate.
     + (* Absurd Bcond (Bcond are not allowed in the left part of a Bseq *)
-              inv IS_EXPD; discriminate.*)
+      inv IS_EXPD; discriminate.
   - (* mib_cond *) admit. (*
-    inversion STEP; subst; try_simplify_someHyps.
+    inversion STEP; subst; try_simplify_someHyps; intros.
     intros; rewrite H12 in BTL_RUN. destruct b.
     * (* Ifso *)
+      eapply match_strong_state_simu.
       exists (Some bso); right; repeat (split; eauto).
       simpl; assert (measure bnot > 0) by apply measure_pos; lia.
       inv H2; econstructor; eauto.
@@ -455,8 +467,9 @@ Proof.
       eexists; left; eexists; split.
       * eapply exec_function_internal.
         erewrite preserv_fnstacksize; eauto.
-      * econstructor; eauto.
+      * econstructor. econstructor; eauto.
         eapply code_expand; eauto.
+        3: eapply entry_isnt_goto; eauto.
         all: erewrite preserv_fnparams; eauto.
         constructor.
     + (* External function *)
@@ -473,9 +486,9 @@ Proof.
     apply DMC in DUPLIC as [ib [FNC MI]]; clear DMC.
     eexists; left; eexists; split.
     + eapply exec_return.
-    + econstructor; eauto.
+    + econstructor. econstructor; eauto.
       eapply code_expand; eauto.
-      constructor.
+      constructor. eapply entry_isnt_goto; eauto.
 Qed.
 
 Local Hint Resolve plus_one star_refl: core.