finish proof

1 files changed, 45 insertions, 39 deletions

diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index d9fec468..7d039f11 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -116,7 +116,7 @@ Inductive match_strong_state dupmap st st' f f' sp rs m rs0 m0 pcB0 pcR0 pcR1 ib
   .
 
 Inductive match_states: (option iblock) -> RTL.state -> state -> Prop :=
-  | match_states_intro (* TODO: LES DETAILS SONT SANS DOUTE A REVOIR !!! *)
+  | match_states_intro
       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)
@@ -261,17 +261,36 @@ Proof.
 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))
+  dupmap st st' f f' sp rs m rs0 m0 rs1 m1 pcB0 pcR0 pcR1 pcR2 isfst ib1 ib2 ib0 n
+  (STEP : RTL.step ge (RTL.State st f sp pcR1 rs m) E0 (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)*)
+  (MES  : measure ib2 < n)
   : 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
+          \/ (omeasure oib' < n /\ E0=E0
           /\ match_states oib' (RTL.State st f sp pcR2 rs1 m1) (State st' f' sp pcB0 rs0 m0)).
-Proof. Admitted.
+Proof.
+  destruct (is_goto ib2) eqn:GT.
+  destruct ib2; try destruct fi; try discriminate.
+  - (* Bgoto *)
+    inv MSS2. inversion MIB; subst; try inv H3.
+    remember H0 as ODUPLIC; clear HeqODUPLIC.
+    eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC.
+    apply DMC in H0 as [ib [FNC MI]]; clear DMC.
+    eexists; left; eexists; split.
+    + repeat econstructor; eauto.
+      apply iblock_istep_run_equiv in BTL_RUN; eauto.
+    + econstructor. econstructor; eauto.
+      eapply code_expand; eauto.
+      econstructor.
+      eapply entry_isnt_goto; eauto.
+  - (* Others *)
+    exists (Some ib2); right; split.
+    simpl; auto.
+    split; auto. econstructor; eauto.
+Qed.
 
 Lemma opt_simu_intro
   dupmap st st' f f' sp rs m rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst s1' t
@@ -355,65 +374,52 @@ Proof.
   - (* mib_exit *)
     discriminate.
   - (* mib_seq *)
-    inversion H; subst.
+    inversion H; subst;
+    try (inv IS_EXPD; try inv H5; discriminate; fail);
+    inversion STEP; subst; try_simplify_someHyps; intros.
     + (* Bnop *)
-      inversion STEP; subst; try_simplify_someHyps; intros.
       eapply match_strong_state_simu.
       1,2: do 2 (econstructor; eauto).
-      econstructor; eauto. (* TODO factorize *)
+      econstructor; eauto.
       inv IS_EXPD; eauto. simpl in *; discriminate.
-      eapply star_right; eauto.
+      eapply star_right; eauto. lia.
     + (* Bop *)
-      inversion STEP; subst; try_simplify_someHyps; intros.
       eapply match_strong_state_simu.
       1,2: do 2 (econstructor; eauto).
-      econstructor; eauto. (* TODO factorize *)
+      econstructor; eauto.
       inv IS_EXPD; eauto. simpl in *; discriminate.
       eapply star_right; eauto.
       erewrite eval_operation_preserved in H11.
       erewrite H11 in BTL_RUN; simpl in BTL_RUN; auto.
-      intros; rewrite <- symbols_preserved; trivial.
+      intros; rewrite <- symbols_preserved; trivial. lia.
     + (* Bload *)
-      inversion STEP; subst; try_simplify_someHyps; intros.
       eapply match_strong_state_simu.
       1,2: do 2 (econstructor; eauto).
-      econstructor; eauto. (* TODO factorize *)
+      econstructor; eauto.
       inv IS_EXPD; eauto. simpl in *; discriminate.
       eapply star_right; eauto.
       erewrite eval_addressing_preserved in H11.
       erewrite H11, H12 in BTL_RUN; simpl in BTL_RUN; auto.
-      intros; rewrite <- symbols_preserved; trivial.
+      intros; rewrite <- symbols_preserved; trivial. lia.
     + (* Bstore *)
-      inversion STEP; subst; try_simplify_someHyps; intros.
       eapply match_strong_state_simu.
       1,2: do 2 (econstructor; eauto).
-      econstructor; eauto. (* TODO factorize *)
+      econstructor; eauto.
       inv IS_EXPD; eauto. simpl in *; discriminate.
       eapply star_right; eauto.
       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; try inv H5; discriminate.
-    + (* Absurd Bcond (Bcond are not allowed in the left part of a Bseq *)
-      inv IS_EXPD; discriminate.
-  - (* mib_cond *) admit. (*
+      intros; rewrite <- symbols_preserved; trivial. lia.
+  - (* mib_cond *)
     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.
-      1,3: inv IS_EXPD; auto; discriminate.
-      all: eapply star_right; eauto.
-    * (* Ifnot *)
-      exists (Some bnot); right; repeat (split; eauto).
-      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.*)
-Admitted.
+    intros; rewrite H12 in BTL_RUN. destruct b;
+    eapply match_strong_state_simu; eauto.
+    1,3: inv H2; econstructor; eauto.
+    1,3,5,7: inv IS_EXPD; auto; discriminate.
+    1-4: eapply star_right; eauto.
+    assert (measure bnot > 0) by apply measure_pos; lia.
+    assert (measure bso > 0) by apply measure_pos; lia.
+Qed.
 
 (** * Main RTL to BTL simulation theorem