Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL

1 files changed, 301 insertions, 258 deletions

diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index 5a5b3a86..f561ee7a 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -6,6 +6,229 @@ Require Import Errors Linking RTLtoBTL.
 
 Require Import Linking.
 
+(** * Normalization of BTL iblock for simulation of RTL
+
+Below [normRTL] normalizes the representation of BTL blocks, 
+in order to represent as sequences of RTL instructions.
+
+This eases the 
+
+*)
+
+Definition is_RTLatom (ib: iblock): bool :=
+ match ib with
+ | Bseq _ _ | Bcond _ _ _ _ _ | Bnop None => false 
+ | _ => true
+ end.
+
+Definition is_RTLbasic (ib: iblock): bool :=
+ match ib with
+ | Bseq _ _ | Bcond _ _ _ _ _ | Bnop None | BF _ _ => false 
+ | _ => true
+ end.
+
+(** The strict [is_normRTL] property specifying the ouput of [normRTL] below *)
+Inductive is_normRTL: iblock -> Prop :=
+  | norm_Bseq ib1 ib2:
+     is_RTLbasic ib1 = true ->
+     is_normRTL ib2 ->
+     is_normRTL (Bseq ib1 ib2)
+  | norm_Bcond cond args ib1 ib2 i:
+     is_normRTL ib1 ->
+     is_normRTL ib2 ->
+     is_normRTL (Bcond cond args ib1 ib2 i)
+  | norm_others ib:
+     is_RTLatom ib = true ->
+     is_normRTL ib
+     .
+Local Hint Constructors is_normRTL: core.
+
+(** Weaker version allowing for trailing [Bnop None]. *)
+Inductive is_wnormRTL: iblock -> Prop :=
+  | wnorm_Bseq ib1 ib2:
+     is_RTLbasic ib1 = true ->
+     (ib2 <> Bnop None -> is_wnormRTL ib2) -> 
+     is_wnormRTL (Bseq ib1 ib2)
+  | wnorm_Bcond cond args ib1 ib2 iinfo:
+     (ib1 <> Bnop None -> is_wnormRTL ib1) ->
+     (ib2 <> Bnop None -> is_wnormRTL ib2) ->
+     is_wnormRTL (Bcond cond args ib1 ib2 iinfo)
+  | wnorm_others ib:
+     is_RTLatom ib = true ->
+     is_wnormRTL ib
+     .
+Local Hint Constructors is_wnormRTL: core.
+
+(* NB: [k] is a "continuation" (e.g. semantically [normRTLrec ib k] is like [Bseq ib k]) *)
+Fixpoint normRTLrec (ib: iblock) (k: iblock): iblock :=
+  match ib with
+  | Bseq ib1 ib2 => normRTLrec ib1 (normRTLrec ib2 k)
+  | Bcond cond args ib1 ib2 iinfo => 
+     Bcond cond args (normRTLrec ib1 k) (normRTLrec ib2 k) iinfo
+  | BF fin iinfo => BF fin iinfo
+  | Bnop None => k
+  | ib => Bseq ib k
+  end.
+
+Definition normRTL ib := normRTLrec ib (Bnop None).
+
+Lemma normRTLrec_wcorrect ib: forall k,
+  (k <> (Bnop None) -> is_wnormRTL k) ->
+  (normRTLrec ib k) <> Bnop None ->
+  is_wnormRTL (normRTLrec ib k).
+Proof.
+  induction ib; simpl; intros; repeat autodestruct; auto.
+Qed.
+
+Lemma normRTL_wcorrect ib: 
+ (normRTL ib) <> Bnop None ->
+ is_wnormRTL (normRTL ib).
+Proof.
+ intros; eapply normRTLrec_wcorrect; eauto.
+Qed.
+
+Lemma is_join_opt_None {A} (opc1 opc2: option A): 
+  is_join_opt opc1 opc2 None -> opc1 = None /\ opc2 = None.
+Proof.
+  intros X. inv X; auto.
+Qed.
+
+Lemma match_iblock_None_not_Bnop dupmap cfg isfst pc ib: 
+  match_iblock dupmap cfg isfst pc ib None -> ib <> Bnop None.
+Proof.
+  intros X; inv X; try congruence.
+Qed.
+Local Hint Resolve match_iblock_None_not_Bnop: core.
+
+Lemma is_wnormRTL_normRTL dupmap cfg ib:
+  is_wnormRTL ib ->
+  forall isfst pc
+  (MIB: match_iblock dupmap cfg isfst pc ib None),
+  is_normRTL ib.
+Proof.
+  induction 1; simpl; intros; auto; try (inv MIB); eauto.
+  (* Bcond *)
+  destruct (is_join_opt_None opc1 opc2); subst; eauto.
+  econstructor; eauto.
+Qed.
+
+Local Hint Constructors iblock_istep: core.
+Lemma normRTLrec_iblock_istep_correct tge sp ib rs0 m0 rs1 m1 ofin1:
+  forall (ISTEP: iblock_istep tge sp rs0 m0 ib rs1 m1 ofin1)
+  k ofin2 rs2 m2
+  (CONT: match ofin1 with
+         | None => iblock_istep tge sp rs1 m1 k rs2 m2 ofin2
+         | Some fin1 => rs2=rs1 /\ m2=m1 /\ ofin2=Some fin1
+         end),
+  iblock_istep tge sp rs0 m0 (normRTLrec ib k) rs2 m2 ofin2.
+Proof.
+  induction 1; simpl; intuition subst; eauto.
+  { (* Bnop *) autodestruct; eauto. }
+  1-3: (* Bop, Bload, Bstore *)
+     intros; repeat econstructor; eauto.
+  (* Bcond *)
+  destruct ofin; intuition subst;
+  destruct b; eapply IHISTEP; eauto.
+Qed.
+
+Lemma normRTL_iblock_istep_correct tge sp ib rs0 m0 rs1 m1 ofin:
+  iblock_istep tge sp rs0 m0 ib rs1 m1 ofin ->
+  iblock_istep tge sp rs0 m0 (normRTL ib) rs1 m1 ofin.
+Proof.
+  intros; eapply normRTLrec_iblock_istep_correct; eauto.
+  destruct ofin; simpl; auto.
+Qed.
+
+Lemma normRTLrec_iblock_istep_run_None tge sp ib:
+  forall rs0 m0 k
+  (CONT: match iblock_istep_run tge sp ib rs0 m0 with
+         | Some (out rs1 m1 ofin) =>
+             ofin = None /\
+             iblock_istep_run tge sp k rs1 m1 = None
+         | _ => True
+     end),
+  iblock_istep_run tge sp (normRTLrec ib k) rs0 m0 = None.
+Proof.
+  induction ib; simpl; intros; subst; intuition (try discriminate).
+  - (* Bnop *)
+    intros. autodestruct; auto.
+  - (* Bop *)
+    intros; repeat autodestruct; simpl; intuition congruence.
+  - (* Bload *)
+    intros; repeat autodestruct; simpl; intuition congruence.
+  - (* Bstore *)
+    intros; repeat autodestruct; simpl; intuition congruence.
+  - (* Bseq *)
+    intros.
+    eapply IHib1; eauto.
+    autodestruct; simpl in *; destruct o; simpl in *; intuition eauto.
+    + destruct _fin; intuition eauto.
+    + destruct _fin; intuition congruence || eauto.
+  - (* Bcond *)
+    intros; repeat autodestruct; simpl; intuition congruence || eauto.
+Qed.
+
+Lemma normRTL_preserves_iblock_istep_run_None tge sp ib:
+  forall rs m, iblock_istep_run tge sp ib rs m = None
+  -> iblock_istep_run tge sp (normRTL ib) rs m = None.
+Proof.
+  intros; eapply normRTLrec_iblock_istep_run_None; eauto.
+  rewrite H; simpl; auto.
+Qed.
+
+Lemma normRTL_preserves_iblock_istep_run tge sp ib:
+  forall rs m, iblock_istep_run tge sp ib rs m =
+  iblock_istep_run tge sp (normRTL ib) rs m.
+Proof.
+  intros.
+  destruct (iblock_istep_run tge sp ib rs m) eqn:ISTEP.
+  - destruct o. symmetry.
+    rewrite <- iblock_istep_run_equiv in *.
+    apply normRTL_iblock_istep_correct; auto.
+  - symmetry.
+    apply normRTL_preserves_iblock_istep_run_None; auto.
+Qed.
+
+Local Hint Constructors match_iblock: core.
+Lemma normRTLrec_matchiblock_correct dupmap cfg ib pc isfst:
+  forall opc1
+  (MIB: match_iblock dupmap cfg isfst pc ib opc1) k opc2
+  (CONT: match opc1 with
+         | Some pc' =>
+             match_iblock dupmap cfg false pc' k opc2
+         | None => opc2=opc1
+         end),
+  match_iblock dupmap cfg isfst pc (normRTLrec ib k) opc2.
+Proof.
+  induction 1; simpl; intros; subst; eauto.
+  (* Bcond *)
+  intros. inv H0;
+  econstructor; eauto; try econstructor.
+  destruct opc0; econstructor.
+Qed.
+
+Lemma normRTL_matchiblock_correct dupmap cfg ib pc isfst opc:
+  match_iblock dupmap cfg isfst pc ib opc ->
+  match_iblock dupmap cfg isfst pc (normRTL ib) opc.
+Proof.
+  intros.
+  eapply normRTLrec_matchiblock_correct; eauto.
+  destruct opc; simpl; auto.
+Qed.
+
+Lemma is_normRTL_correct dupmap cfg ib pc
+  (MI : match_iblock dupmap cfg true pc ib None):
+  is_normRTL (normRTL ib).
+Proof.
+  exploit normRTL_matchiblock_correct; eauto.
+  intros MI2.
+  eapply is_wnormRTL_normRTL; eauto.
+  apply normRTL_wcorrect; try congruence.
+  inv MI2; discriminate.
+Qed.
+
+(** * Matching relation on functions *)
+
 Record match_function dupmap (f:RTL.function) (tf: BTL.function): Prop := {
   dupmap_correct: match_cfg dupmap (fn_code tf) (RTL.fn_code f);
   dupmap_entrypoint: dupmap!(fn_entrypoint tf) = Some (RTL.fn_entrypoint f);
@@ -106,7 +329,7 @@ Inductive match_strong_state dupmap st st' f f' sp rs1 m1 rs0 m0 pcB0 pcR0 pcR1
       (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)
+      (IS_EXPD: is_normRTL ib)
       (RTL_RUN: star RTL.step ge (RTL.State st f sp pcR0 rs0 m0) E0 (RTL.State st f sp pcR1 rs1 m1))
       (BTL_RUN: iblock_istep_run tge sp ib0.(entry) rs0 m0 = iblock_istep_run tge sp ib rs1 m1)
       : match_strong_state dupmap st st' f f' sp rs1 m1 rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst
@@ -231,43 +454,30 @@ Proof.
   induction ib; simpl; auto; lia.
 Qed.
 
-(* TODO gourdinl remove useless lemma? *)
-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 H5.
-Qed.
-
-Lemma normRTL_entry_isnt_goto dupmap f pc ib:
-  match_iblock dupmap (RTL.fn_code f) true pc (normRTL (entry ib) (Bnop None)) None ->
-  is_goto (normRTL (entry ib) (Bnop None)) = false.
-Proof.
-  destruct (is_goto (normRTL (entry ib) (Bnop None))) eqn:EQG;
-  destruct (normRTL (entry ib) (Bnop None));
-  try destruct fi; try discriminate; trivial.
-  intros; inv H; inv H5.
-Qed.
-
-Lemma normRTL_entry_isnt_bnop dupmap f pc ib:
-  match_iblock dupmap (RTL.fn_code f) true pc (normRTL (entry ib) (Bnop None)) None ->
-  normRTL (entry ib) (Bnop None) <> Bnop None.
+Lemma match_iblock_true_isnt_goto dupmap cfg pc ib opc:
+  match_iblock dupmap cfg true pc ib opc ->
+  is_goto ib = false.
 Proof.
-  destruct (normRTL (entry ib) (Bnop None)) eqn:EQG;
-  try destruct fi; try discriminate; trivial.
-  intros; inv H; inv H5.
+  intros MIB; inversion MIB as [d1 d2 d3 d4 d5 H H0| | | | | | | |]; subst; simpl; try congruence.
+  inv H0; congruence.
 Qed.
 
-Lemma is_expand_normRTL_entry dupmap f ib pc
-  (MI : match_iblock dupmap (RTL.fn_code f) true pc (normRTL (entry ib) (Bnop None)) None):
-  is_expand (normRTL (entry ib) (Bnop None)).
+Local Hint Resolve match_iblock_true_isnt_goto normRTL_preserves_iblock_istep_run star_refl star_right: core.
+Local Hint Constructors match_strong_state RTL.step: core.
+
+(** At entry in a block: we init [match_states] on [normRTL] to normalize the block *)
+Lemma match_states_entry dupmap st f sp pc ib rs m st' f' pc'
+  (STACKS : list_forall2 match_stackframes st st')
+  (TRANSF : match_function dupmap f f')
+  (FN : (fn_code f') ! pc' = Some ib)
+  (MI : match_iblock dupmap (RTL.fn_code f) true pc (entry ib) None)
+  (DUP : dupmap ! pc' = Some pc):
+  match_states (Some (normRTL (entry ib))) (RTL.State st f sp pc rs m) (State st' f' sp pc' rs m).
 Proof.
-  eapply is_wexpand_expand; eauto.
-  apply normRTL_correct; try congruence.
-  eapply normRTL_entry_isnt_bnop; eauto.
+  exploit is_normRTL_correct; eauto.
+  econstructor; eauto; apply normRTL_matchiblock_correct in MI; eauto.
 Qed.
+Local Hint Resolve match_states_entry: core.
 
 Lemma list_nth_z_rev_dupmap:
   forall dupmap ln ln' (pc pc': node) val,
@@ -286,141 +496,6 @@ Proof.
       intros (pc'1 & LNZ & REV). exists pc'1. split; auto. congruence.
 Qed.
 
-Local Hint Constructors iblock_istep: core.
-Lemma normRTL_iblock_istep_rec_correct sp ib rs0 m0 rs1 m1 ofin1:
-  forall (ISTEP: iblock_istep tge sp rs0 m0 ib rs1 m1 ofin1)
-  k ofin2 rs2 m2
-  (CONT: match ofin1 with
-         | None => iblock_istep tge sp rs1 m1 k rs2 m2 ofin2
-         | Some fin1 => rs2=rs1 /\ m2=m1 /\ ofin2=Some fin1
-         end),
-  iblock_istep tge sp rs0 m0 (normRTL ib k) rs2 m2 ofin2.
-Proof.
-  induction 1; simpl; intros; intuition subst; eauto.
-  { (* Bnop *)
-    autodestruct; intros OI; inv OI; destruct (Bnop_dec k); subst;
-    try (inv CONT; constructor; fail); repeat econstructor; eauto. }
-  1-3: (* Bop, Bload, Bstore *)
-    intros; destruct (Bnop_dec k); subst; repeat econstructor; eauto;
-    inv CONT; econstructor; eauto.
-  - (* Bcond *)
-    destruct ofin; intros;
-    econstructor; eauto;
-    destruct b; eapply IHISTEP; eauto.
-Qed.
-
-Lemma normRTL_iblock_istep_correct sp ib rs0 m0 rs1 m1 ofin:
-  iblock_istep tge sp rs0 m0 ib rs1 m1 ofin ->
-  iblock_istep tge sp rs0 m0 (normRTL ib (Bnop None)) rs1 m1 ofin.
-Proof.
-  intros; eapply normRTL_iblock_istep_rec_correct; eauto.
-  destruct ofin; simpl; auto.
-Qed.
-
-Lemma normRTL_iblock_istep_run_None_rec sp ib:
-  forall rs0 m0 o k
-  (ISTEP: iblock_istep_run tge sp ib rs0 m0 = o)
-  (CONT: match o with
-         | Some (out rs1 m1 ofin) =>
-             ofin = None /\
-             iblock_istep_run tge sp k rs1 m1 = None
-         | _ => True
-     end),
-  iblock_istep_run tge sp (normRTL ib k) rs0 m0 = None.
-Proof.
-  induction ib; simpl;
-  try discriminate.
-  - (* BF *)
-    intros; destruct o; try discriminate; simpl in *.
-    inv ISTEP. destruct CONT as [HO ISTEP]; inv HO.
-  - (* Bnop *)
-    intros; destruct o; inv ISTEP; destruct oiinfo, CONT; auto.
-    destruct (Bnop_dec k); subst; repeat econstructor; eauto.
-  - (* Bop *)
-    intros; destruct o; destruct (Bnop_dec k);
-    destruct (eval_operation _ _ _ _ _) eqn:EVAL; inv ISTEP;
-    simpl; rewrite EVAL; auto; destruct CONT as [HO ISTEP];
-    trivial.
-  - (* Bload *)
-    intros; destruct o; destruct (Bnop_dec k);
-    destruct (trap) eqn:TRAP;
-    try destruct (eval_addressing _ _ _ _) eqn:EVAL;
-    try destruct (Mem.loadv _ _ _) eqn:MEM; inv ISTEP;
-    simpl; try rewrite EVAL; try rewrite MEM; simpl; auto;
-    destruct CONT as [HO ISTEP]; trivial.
-  - (* Bstore *)
-    intros; destruct o; destruct (Bnop_dec k);
-    destruct (eval_addressing _ _ _ _) eqn:EVAL;
-    try destruct (Mem.storev _ _ _) eqn:MEM; inv ISTEP;
-    simpl; try rewrite EVAL; try rewrite MEM; simpl; auto;
-    destruct CONT as [HO ISTEP]; inv HO; trivial.
-  - (* Bseq *)
-    intros.
-    eapply IHib1; eauto.
-    destruct (iblock_istep_run tge sp ib1 rs0 m0) eqn:EQib1; try auto.
-    destruct o0; simpl in *. destruct _fin; inv ISTEP.
-    + destruct CONT as [CONTRA _]; inv CONTRA.
-    + split; auto. eapply IHib2; eauto.
-  - (* Bcond *)
-    intros; destruct (eval_condition _ _ _); trivial.
-    destruct b.
-    + eapply IHib1; eauto.
-    + eapply IHib2; eauto.
-Qed.
-
-Lemma normRTL_preserves_iblock_istep_run_None sp ib:
-  forall rs m, iblock_istep_run tge sp ib rs m = None
-  -> iblock_istep_run tge sp (normRTL ib (Bnop None)) rs m = None.
-Proof.
-  intros; eapply normRTL_iblock_istep_run_None_rec; eauto.
-  simpl; auto.
-Qed.
-
-Lemma normRTL_preserves_iblock_istep_run sp ib:
-  forall rs m, iblock_istep_run tge sp ib rs m =
-  iblock_istep_run tge sp (normRTL ib (Bnop None)) rs m.
-Proof.
-  intros.
-  destruct (iblock_istep_run tge sp ib rs m) eqn:ISTEP.
-  - destruct o. symmetry.
-    rewrite <- iblock_istep_run_equiv in *.
-    apply normRTL_iblock_istep_correct; auto.
-  - symmetry.
-    apply normRTL_preserves_iblock_istep_run_None; auto.
-Qed.
-
-Local Hint Constructors match_iblock: core.
-Lemma normRTL_matchiblock_rec_correct dupmap cfg ib pc isfst:
-  forall opc1
-  (MIB: match_iblock dupmap cfg isfst pc ib opc1) k opc2
-  (CONT: match opc1 with
-         | Some pc' =>
-             match_iblock dupmap cfg false pc' k opc2
-         | None => opc2=opc1
-         end),
-  match_iblock dupmap cfg isfst pc (normRTL ib k) opc2.
-Proof.
-  induction 1; simpl; intros; eauto.
-  { (* BF *)
-    inv CONT; econstructor; eauto. }
-  1-4: (* Bnop, Bop, Bload, Bstore *)
-    destruct (Bnop_dec k); subst; eauto; inv CONT; econstructor; eauto.
-  { (* Bgoto *)
-    intros; inv CONT; apply mib_exit; auto. }
-  { (* Bcond *)
-    intros. inv H0;
-    econstructor; eauto; try econstructor.
-    destruct opc0; econstructor. }
-Qed.
-
-Lemma normRTL_matchiblock_correct dupmap cfg ib pc isfst opc:
-  match_iblock dupmap cfg isfst pc ib opc ->
-  match_iblock dupmap cfg isfst pc (normRTL ib (Bnop None)) opc.
-Proof.
-  intros.
-  eapply normRTL_matchiblock_rec_correct; eauto.
-  destruct opc; simpl; auto.
-Qed.
 
 (** * Match strong state property
 
@@ -455,17 +530,20 @@ See explanations of opt_simu below.
 *)
 
 Lemma match_strong_state_simu
-  dupmap st st' f f' sp rs2 m2 rs1 m1 rs0 m0 pcB0 pcR0 pcR1 pcR2 isfst ib1 ib2 ib0 n
-  (STEP : RTL.step ge (RTL.State st f sp pcR1 rs1 m1) E0 (RTL.State st f sp pcR2 rs2 m2))
+  dupmap st st' f f' sp rs2 m2 rs1 m1 rs0 m0 pcB0 pcR0 pcR1 pcR2 isfst ib1 ib2 ib0 n t s1'
+  (EQt: t=E0)
+  (EQs1': s1'=(RTL.State st f sp pcR2 rs2 m2))
+  (STEP : RTL.step ge (RTL.State st f sp pcR1 rs1 m1) t s1')
   (MSS1 : match_strong_state dupmap st st' f f' sp rs1 m1 rs0 m0 pcB0 pcR0 pcR1 ib1 ib0 isfst)
   (MSS2 : match_strong_state dupmap st st' f f' sp rs2 m2 rs0 m0 pcB0 pcR0 pcR2 ib2 ib0 false)
   (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 rs2 m2) s2')
-          \/ (omeasure oib' < n /\ E0=E0
-          /\ match_states oib' (RTL.State st f sp pcR2 rs2 m2) (State st' f' sp pcB0 rs0 m0)).
+      (exists s2', step tge (State st' f' sp pcB0 rs0 m0) t s2'
+          /\ match_states oib' s1' s2')
+          \/ (omeasure oib' < n /\ t=E0
+          /\ match_states oib' s1' (State st' f' sp pcB0 rs0 m0)).
 Proof.
+  subst.
   destruct (is_goto ib2) eqn:GT.
   destruct ib2; try destruct fi; try discriminate.
   - (* Bgoto *)
@@ -473,13 +551,9 @@ Proof.
     remember H2 as ODUPLIC; clear HeqODUPLIC.
     eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC.
     apply DMC in H2 as [ib [FNC MI]]; clear DMC.
-    eexists; left; eexists; split.
-    + repeat econstructor; eauto.
-      apply iblock_istep_run_equiv in BTL_RUN; eauto.
-    + econstructor; apply normRTL_matchiblock_correct in MI.
-      econstructor; eauto. eapply is_expand_normRTL_entry; eauto.
-      econstructor. apply normRTL_preserves_iblock_istep_run.
-      eapply normRTL_entry_isnt_goto; eauto.
+    eexists; left; eexists; split; eauto.
+    repeat econstructor; eauto.
+    apply iblock_istep_run_equiv in BTL_RUN; eauto.
   - (* Others *)
     exists (Some ib2); right; split.
     simpl; auto.
@@ -495,7 +569,7 @@ Lemma opt_simu_intro
      (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.
-  inversion MSTRONG; subst. inv MIB.
+  inv MSTRONG; subst. inv MIB.
   - (* mib_BF *)
     inv H0;
     inversion STEP; subst; try_simplify_someHyps; intros.
@@ -536,81 +610,60 @@ Proof.
       eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC.
       remember H1 as ODUPLIC; clear HeqODUPLIC.
       apply DMC in H1 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.
-        pose symbols_preserved as SYMPRES.
-        eapply eval_builtin_args_preserved; eauto.
-        eapply external_call_symbols_preserved; eauto. eapply senv_preserved.
-      * econstructor; eauto; apply normRTL_matchiblock_correct in MI.
-        { econstructor; eauto. eapply is_expand_normRTL_entry; eauto.
-          apply star_refl. apply normRTL_preserves_iblock_istep_run. }
-        eapply normRTL_entry_isnt_goto; eauto.
+      exists (Some (normRTL (entry ib))); left; eexists; split; eauto.
+      econstructor; eauto. econstructor.
+      eexists; eexists; split.
+      eapply iblock_istep_run_equiv in BTL_RUN.
+      eapply BTL_RUN. econstructor; eauto.
+      pose symbols_preserved as SYMPRES.
+      eapply eval_builtin_args_preserved; eauto.
+      eapply external_call_symbols_preserved; eauto. eapply senv_preserved.
     + (* Bjumptable *)
       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.
-      * econstructor; eauto; apply normRTL_matchiblock_correct in MI.
-        { econstructor; eauto. eapply is_expand_normRTL_entry; eauto.
-          apply star_refl. apply normRTL_preserves_iblock_istep_run. }
-        eapply normRTL_entry_isnt_goto; eauto.
+      exists (Some (normRTL (entry ib))); left; eexists; split; eauto.
+      econstructor; eauto. econstructor.
+      eexists; eexists; split.
+      eapply iblock_istep_run_equiv in BTL_RUN.
+      eapply BTL_RUN. econstructor; eauto.
   - (* mib_exit *)
     discriminate.
   - (* mib_seq *)
-    inversion H; subst;
-    try (inv IS_EXPD; try inv H5; discriminate; fail);
-    inversion STEP; subst; try_simplify_someHyps; intros.
+    inv IS_EXPD; try discriminate.
+    inv H; simpl in *; try congruence;
+    inv STEP; try_simplify_someHyps; eauto.
     + (* Bnop is_rtl *)
-      eapply match_strong_state_simu.
-      1,2: do 2 (econstructor; eauto).
-      econstructor; eauto.
-      inv IS_EXPD; eauto. simpl in *; discriminate.
-      eapply star_right; eauto. lia.
+      intros; eapply match_strong_state_simu; eauto.
     + (* Bop *)
-      eapply match_strong_state_simu.
-      1,2: do 2 (econstructor; eauto).
+      intros; eapply match_strong_state_simu; eauto.
       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. lia.
+      erewrite eval_operation_preserved in H12.
+      erewrite H12 in BTL_RUN; simpl in BTL_RUN; auto.
+      intros; rewrite <- symbols_preserved; trivial.
     + (* Bload *)
-      eapply match_strong_state_simu.
-      1,2: do 2 (econstructor; eauto).
+      intros; eapply match_strong_state_simu; eauto.
       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. lia.
+      erewrite eval_addressing_preserved in H12.
+      erewrite H12, H13 in BTL_RUN; simpl in BTL_RUN; auto.
+      intros; rewrite <- symbols_preserved; trivial.
     + (* Bstore *)
-      eapply match_strong_state_simu.
-      1,2: do 2 (econstructor; eauto).
+      intros; eapply match_strong_state_simu; eauto.
       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. lia.
+      erewrite eval_addressing_preserved in H12.
+      erewrite H12, H13 in BTL_RUN; simpl in BTL_RUN; auto.
+      intros; rewrite <- symbols_preserved; trivial.
   - (* mib_cond *)
+    inv IS_EXPD; try discriminate.
     inversion STEP; subst; try_simplify_someHyps; intros.
-    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; try 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.
+    destruct (is_join_opt_None opc1 opc2); eauto. subst.
+    eapply match_strong_state_simu with (ib1:=Bcond c lr bso bnot iinfo) (ib2:=(if b then bso else bnot)); eauto.
+    + intros; rewrite H14 in BTL_RUN; destruct b; econstructor; eauto.
+    + assert (measure (if b then bnot else bso) > 0) by apply measure_pos; destruct b; simpl; lia.
+  Unshelve.
+    all: eauto.
 Qed.
 
 (** * Main RTL to BTL simulation theorem
@@ -624,9 +677,9 @@ Two possible executions:
     RTL state         match_states          BTL state
        s1 ------------------------------------ s2
        |                                       |
-  STEP |       Classical lockstep simu         | 
-       |                                       | 
-       s1' ----------------------------------- s2' 
+  STEP |       Classical lockstep simu         |
+       |                                       |
+       s1' ----------------------------------- s2'
 
 
  **Middle instruction (right side):**
@@ -634,8 +687,8 @@ Two possible executions:
     RTL state         match_states [oib]    BTL state
        s1 ------------------------------------ s2
        |                               _______/
-  STEP | *E0       ___________________/         
-       |          / match_states [oib']         
+  STEP | *E0       ___________________/
+       |          / match_states [oib']
        s1' ______/
    Where omeasure oib' < omeasure oib
 
@@ -662,15 +715,10 @@ Proof.
       eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC.
       apply DMC in ENTRY as DMC'.
       destruct DMC' as [ib [CENTRY MI]]; clear DMC.
-      eexists; left; eexists; split.
+      exists (Some (normRTL (entry ib))); left; eexists; split.
       * eapply exec_function_internal.
         erewrite preserv_fnstacksize; eauto.
-      * apply normRTL_matchiblock_correct in MI.
-        econstructor. econstructor; eauto.
-        eapply is_expand_normRTL_entry; eauto.
-        3: eapply normRTL_entry_isnt_goto; eauto.
-        all: erewrite preserv_fnparams; eauto.
-        constructor. apply normRTL_preserves_iblock_istep_run.
+      * erewrite preserv_fnparams; eauto.
     + (* External function *)
       inv TRANSF.
       eexists; left; eexists; split.
@@ -683,13 +731,8 @@ Proof.
     eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC.
     remember DUPLIC as ODUPLIC; clear HeqODUPLIC.
     apply DMC in DUPLIC as [ib [FNC MI]]; clear DMC.
-    eexists; left; eexists; split.
-    + eapply exec_return.
-    + apply normRTL_matchiblock_correct in MI.
-      econstructor. econstructor; eauto.
-      eapply is_expand_normRTL_entry; eauto.
-      econstructor. apply normRTL_preserves_iblock_istep_run.
-      eapply normRTL_entry_isnt_goto; eauto.
+    eexists; left; eexists; split; eauto.
+    eapply exec_return.
 Qed.
 
 Local Hint Resolve plus_one star_refl: core.