Require Import Coqlib Maps Lia.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import RTL Op Registers OptionMonad BTL.

Require Import Errors Linking RTLtoBTL.

Require Import Linking.

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);
  preserv_fnsig: fn_sig tf = RTL.fn_sig f;
  preserv_fnparams: fn_params tf = RTL.fn_params f;
  preserv_fnstacksize: fn_stacksize tf = RTL.fn_stacksize f
}.

Inductive match_fundef: RTL.fundef -> fundef -> Prop :=
  | match_Internal dupmap f tf: match_function dupmap f tf -> match_fundef (Internal f) (Internal tf)
  | match_External ef: match_fundef (External ef) (External ef).

Inductive match_stackframes: RTL.stackframe -> stackframe -> Prop :=
  | match_stackframe_intro 
      dupmap res f sp pc rs f' pc'
      (TRANSF: match_function dupmap f f')
      (DUPLIC: dupmap!pc' = Some pc)
      : match_stackframes (RTL.Stackframe res f sp pc rs) (Stackframe res f' sp pc' rs).

Lemma verify_function_correct dupmap f f' tt:
  verify_function dupmap f' f = OK tt ->
  fn_sig f' = RTL.fn_sig f ->
  fn_params f' = RTL.fn_params f ->
  fn_stacksize f' = RTL.fn_stacksize f ->
  match_function dupmap f f'.
Proof.
  unfold verify_function; intro VERIF. monadInv VERIF.
  constructor; eauto.
  - eapply verify_cfg_correct; eauto.
  - eapply verify_is_copy_correct; eauto.
Qed.

Lemma transf_function_correct f f':
  transf_function f = OK f' -> exists dupmap, match_function dupmap f f'.
Proof.
  unfold transf_function; unfold bind. repeat autodestruct.
  intros H _ _ X. inversion X; subst; clear X.
  eexists; eapply verify_function_correct; simpl; eauto.
Qed.

Lemma transf_fundef_correct f f':
  transf_fundef f = OK f' -> match_fundef f f'.
Proof.
  intros TRANSF; destruct f; simpl; monadInv TRANSF.
  + exploit transf_function_correct; eauto.
    intros (dupmap & MATCH_F).
    eapply match_Internal; eauto.
  + eapply match_External.
Qed.

Definition match_prog (p: RTL.program) (tp: program) :=
  match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.

Lemma transf_program_match:
  forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog.
Proof.
  intros. eapply match_transform_partial_program_contextual; eauto.
Qed.

Section BTL_SIMULATES_RTL.

Variable prog: RTL.program.
Variable tprog: program.

Hypothesis TRANSL: match_prog prog tprog.

Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Local Open Scope nat_scope.

(** * Match relation from a RTL state to a BTL state

The "option iblock" parameter represents the current BTL execution state.
Thus, each RTL single step is symbolized by a new BTL "option iblock"
starting at the equivalent PC.

The simulation diagram for match_states_intro is as follows:

<<

        RTL state       match_states_intro        BTL state
      [pcR0,rs0,m0] --------------------------- [pcB0,rs0,m0]
           |                                         |
           |                                         |
   RTL_RUN | *E0                                     | BTL_RUN
           |                                         |
           |                   MIB                   |
      [pcR1,rs1,m1] ------------------------------- [ib]

>>
*)

Inductive match_strong_state dupmap st st' f f' sp rs1 m1 rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst: Prop :=
  | match_strong_state_intro
      (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 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
  .

Inductive match_states: (option iblock) -> RTL.state -> state -> Prop :=
  | match_states_intro
      dupmap st st' f f' sp rs1 m1 rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst
      (MSTRONG: match_strong_state dupmap st st' f f' sp rs1 m1 rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst)
      (NGOTO: is_goto ib = false)
      : match_states (Some ib) (RTL.State st f sp pcR1 rs1 m1) (State st' f' sp pcB0 rs0 m0)
  | match_states_call
      st st' f f' args m
      (STACKS: list_forall2 match_stackframes st st')
      (TRANSF: match_fundef f f')
      : match_states None (RTL.Callstate st f args m) (Callstate st' f' args m)
  | match_states_return
      st st' v m
      (STACKS: list_forall2 match_stackframes st st')
      : match_states None (RTL.Returnstate st v m) (Returnstate st' v m)
  .

Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof.
  rewrite <- (Genv.find_symbol_match TRANSL). reflexivity.
Qed.

Lemma senv_preserved: Senv.equiv ge tge.
Proof.
  eapply (Genv.senv_match TRANSL).
Qed.

Lemma functions_translated (v: val) (f: RTL.fundef):
  Genv.find_funct ge v = Some f ->
  exists tf cunit, transf_fundef f = OK tf /\ Genv.find_funct tge v = Some tf /\ linkorder cunit prog.
Proof.
  intros. exploit (Genv.find_funct_match TRANSL); eauto.
  intros (cu & tf & A & B & C).
  repeat eexists; intuition eauto.
  + unfold incl; auto.
  + eapply linkorder_refl.
Qed.

Lemma function_ptr_translated v f:
  Genv.find_funct_ptr ge v = Some f ->
  exists tf,
  Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf.
Proof.
  intros.
  exploit (Genv.find_funct_ptr_transf_partial TRANSL); eauto.
Qed.

Lemma function_sig_translated f tf: transf_fundef f = OK tf -> funsig tf = RTL.funsig f.
Proof.
  intros H; apply transf_fundef_correct in H; destruct H; simpl; eauto.
  erewrite preserv_fnsig; eauto.
Qed.

Lemma transf_initial_states s1:
  RTL.initial_state prog s1 ->
  exists ib s2, initial_state tprog s2 /\ match_states ib s1 s2.
Proof.
  intros. inv H.
  exploit function_ptr_translated; eauto. intros (tf & FIND & TRANSF).
  eexists. eexists. split.
  - econstructor; eauto.
    + eapply (Genv.init_mem_transf_partial TRANSL); eauto.
    + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto.
      symmetry. eapply match_program_main. eauto.
    + erewrite function_sig_translated; eauto.
  - constructor; eauto.
    constructor.
    apply transf_fundef_correct; auto.
Qed.

Lemma transf_final_states ib s1 s2 r:
  match_states ib s1 s2 -> RTL.final_state s1 r -> final_state s2 r.
Proof.
  intros. inv H0. inv H. inv STACKS. constructor.
Qed.

Lemma find_function_preserved ri rs0 fd
  (FIND : RTL.find_function ge ri rs0 = Some fd)
  : exists fd', find_function tge ri rs0 = Some fd'
                /\ transf_fundef fd = OK fd'.
Proof.
  pose symbols_preserved as SYMPRES.
  destruct ri.
  + simpl in FIND; apply functions_translated in FIND.
    destruct FIND as (tf & cunit & TFUN & GFIND & LO).
    eexists; split. eauto. assumption.
  + simpl in FIND. destruct (Genv.find_symbol _ _) eqn:GFS; try discriminate.
    apply function_ptr_translated in FIND. destruct FIND as (tf & GFF & TF).
    eexists; split. simpl. rewrite symbols_preserved.
    rewrite GFS. eassumption. assumption.
Qed.

(** Representing an intermediate BTL state

We keep a measure of code that remains to be executed with the omeasure
type defined below. Intuitively, each RTL step corresponds to either
   - a single BTL step if we are on the last instruction of the block
   - no BTL step (as we use a "big step" semantics) but a change in
     the measure which represents the new intermediate state of the BTL code
 *)
Fixpoint measure ib: nat :=
  match ib with
  | Bseq ib1 ib2
  | Bcond _ _ ib1 ib2 _ => measure ib1 + measure ib2
  | ib => 1
  end.

Definition omeasure (oib: option iblock): nat :=
 match oib with
 | None => 0
 | Some ib => measure ib
 end.

Remark measure_pos: forall ib,
  measure ib > 0.
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 expand_entry_isnt_goto dupmap f pc ib:
  match_iblock dupmap (RTL.fn_code f) true pc (expand (entry ib) None) None ->
  is_goto (expand (entry ib) None) = false.
Proof.
  destruct (is_goto (expand (entry ib) None))eqn:EQG.
  - destruct (expand (entry ib) None);
    try destruct fi; try discriminate; trivial.
    intros; inv H; inv H4.
  - destruct (expand (entry ib) None);
    try destruct fi; try discriminate; trivial.
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 expand_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 =>
             (k = None /\ rs2=rs1 /\ m2=m1 /\ ofin2 = None)
             \/ (exists rem, k = Some rem
                /\ iblock_istep tge sp rs1 m1 rem rs2 m2 ofin2)
         | Some fin1 => rs2=rs1 /\ m2=m1 /\ ofin2=Some fin1
         end),
  iblock_istep tge sp rs0 m0 (expand ib k) rs2 m2 ofin2.
Proof.
  induction 1; simpl.
  { (* BF *)
    intros ? ? ? ? (HRS & HM & HOF); subst.
    constructor. }
    (*destruct k; intros. try inv CONT.*)
  1-4: (* Bnop, Bop, Bload, Bstore *)
    destruct k; intros; destruct CONT as [[HK [HRS [HM HO]]]|[rem [HR ISTEP]]];
    subst; try (inv HK; fail); try (inv HR; fail); try (econstructor; eauto; fail);
    inversion HR; subst; clear HR;
    eapply exec_seq_continue; [ econstructor; eauto | assumption].
  - (* Bseq_stop *)
    destruct k; intros; apply IHISTEP; eauto.
  - (* Bseq_continue *)
    destruct ofin; intros.
    + destruct CONT as [HRS [HM HOF]]; subst.
      eapply IHISTEP1; right. eexists; repeat split; eauto.
    + destruct CONT as [[HK [HRS [HM HO]]]|[rem [HR ISTEP]]]; subst.
      * eapply IHISTEP1; right. eexists; repeat split; eauto.
        eapply IHISTEP2; left; simpl; auto.
      * eapply IHISTEP1; right. eexists; repeat split; eauto.
  - (* Bcond *)
    destruct ofin; intros;
    econstructor; eauto;
    destruct b; eapply IHISTEP; eauto.
Qed.

Lemma expand_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 (expand ib None) rs1 m1 ofin.
Proof.
  intros; eapply expand_iblock_istep_rec_correct; eauto.
  destruct ofin; simpl; auto.
Qed.

(* TODO useless? *)
Lemma expand_iblock_istep_run_Some_rec sp ib rs0 m0 rs1 m1 ofin1:
  forall (ISTEP: iblock_istep_run tge sp ib rs0 m0 =
  Some {| _rs := rs1; _m := m1; _fin := ofin1 |})
  k ofin2 rs2 m2
  (CONT: match ofin1 with
         | None =>
             (k = None /\ rs2=rs1 /\ m2=m1 /\ ofin2 = None)
             \/ (exists rem, k = Some rem
                /\ iblock_istep_run tge sp rem rs1 m1 =
                Some {| _rs := rs2; _m := m2; _fin := ofin2 |})
         | Some fin1 => rs2=rs1 /\ m2=m1 /\ ofin2=Some fin1
         end),
  iblock_istep_run tge sp (expand ib k) rs0 m0 =
  Some {| _rs := rs2; _m := m2; _fin := ofin2 |}.
Proof.
  intros. destruct ofin1;
  rewrite <- iblock_istep_run_equiv in *.
  - destruct CONT as [HRS [HM HO]]; subst.
    eapply expand_iblock_istep_rec_correct; eauto.
    simpl; auto.
  - eapply expand_iblock_istep_rec_correct; eauto.
    simpl. destruct CONT as [HL | [rem [HR ISTEP']]].
    left; auto. rewrite <- iblock_istep_run_equiv in ISTEP'.
    right; eexists; split; eauto.
Qed.

Lemma expand_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) =>
             exists rem,
             k = Some rem /\ ofin = None /\
             iblock_istep_run tge sp rem rs1 m1 = None
         | _ => True
     end),
  iblock_istep_run tge sp (expand ib k) rs0 m0 = None.
Proof.
  induction ib; simpl;
  try discriminate.
  - (* BF *)
    intros; destruct o; try discriminate; simpl in *.
    inv ISTEP. destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; inv HO.
  - (* Bnop *)
    intros; destruct o; inv ISTEP; destruct k;
    destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; inv HO; trivial.
  - (* Bop *)
    intros; destruct o;
    destruct (eval_operation _ _ _ _ _) eqn:EVAL; inv ISTEP; destruct k;
    simpl; rewrite EVAL; auto; destruct CONT as [rem [HR [HO ISTEP]]];
    inv HR; inv HO; trivial.
  - (* Bload *)
    intros; destruct o;
    destruct (trap) eqn:TRAP;
    try destruct (eval_addressing _ _ _ _) eqn:EVAL;
    try destruct (Mem.loadv _ _ _) eqn:MEM; inv ISTEP; destruct k;
    simpl; try rewrite EVAL; try rewrite MEM; simpl; auto;
    destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; inv HO; trivial.
  - (* Bstore *)
    intros; destruct o;
    destruct (eval_addressing _ _ _ _) eqn:EVAL;
    try destruct (Mem.storev _ _ _) eqn:MEM; inv ISTEP; destruct k;
    simpl; try rewrite EVAL; try rewrite MEM; simpl; auto;
    destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; inv HO; trivial.
  - (* Bseq *)
    intros.
    eapply IHib1; eauto.
    destruct (iblock_istep_run tge sp ib1 rs0 m0) eqn:EQib1; try auto.
    destruct o0. eexists; split; eauto. simpl in *.
    destruct _fin; inv ISTEP.
    + destruct CONT as [rem [_ [CONTRA _]]]; inv CONTRA.
    + split; auto. eapply IHib2; eauto.
  - (* Bcond *)
    intros; destruct (eval_condition _ _ _); trivial.
    destruct b.
    + eapply IHib1; eauto.
    + eapply IHib2; eauto.
Qed.

Lemma expand_preserves_iblock_istep_run_None sp ib:
  forall rs m, iblock_istep_run tge sp ib rs m = None
  -> iblock_istep_run tge sp (expand ib None) rs m = None.
Proof.
  intros; eapply expand_iblock_istep_run_None_rec; eauto.
  simpl; auto.
Qed.

Lemma expand_preserves_iblock_istep_run sp ib:
  forall rs m, iblock_istep_run tge sp ib rs m =
  iblock_istep_run tge sp (expand ib 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 expand_iblock_istep_correct; auto.
  - symmetry.
    apply expand_preserves_iblock_istep_run_None; auto.
Qed.

Lemma expand_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' =>
             k = None /\ opc2 = opc1 \/
             (exists rem, k = Some rem
             /\ match_iblock dupmap cfg false pc' rem opc2)
         | None => opc2=opc1
         end),
  match_iblock dupmap cfg isfst pc (expand ib k) opc2.
Proof.
  induction 1; simpl.
  { (* BF *)
    intros; inv CONT; econstructor; eauto. }
  1-4: (* Bnop *)
    destruct k; intros; destruct CONT as [[HK HO] | [rem [HR MIB]]];
    try inv HK; try inv HO; try inv HR; repeat econstructor; eauto.
  { (* Bgoto *)
    intros; inv CONT; apply mib_exit; auto. }
  { (* Bseq *)
    intros. eapply IHMIB1. right. eexists; split; eauto. }
  { (* Bcond *)
    intros. inv H0;
    econstructor; eauto; try econstructor.
    destruct opc0; econstructor. }
Qed.

Lemma expand_matchiblock_correct dupmap cfg ib pc isfst opc:
  match_iblock dupmap cfg isfst pc ib opc ->
  match_iblock dupmap cfg isfst pc (expand ib None) opc.
Proof.
  intros.
  eapply expand_matchiblock_rec_correct; eauto.
  destruct opc; simpl; auto.
Qed.

(** * Match strong state property

Used when executing non-atomic instructions such as Bseq/Bcond(ib1,ib2).
Two possible executions:

<<

 **ib2 is a Bgoto (left side):**

      RTL state                MSS1             BTL state
     [pcR1,rs1,m1] -------------------------- [ib1,pcB0,rs0,m0]
           |                                         |
           |                                         |
           |                                         | BTL_STEP
           |                                         |
           |                                         |
  RTL_STEP | *E0                       [ib2,pc=(Bgoto succ),rs2,m2]
           |                          /              |
           |             MSS2        /               |
           |       _________________/                | BTL_GOTO
           |      /                                  |
           |     /   GOAL: match_states              |
    [pcR2,rs2,m2] ------------------------ [ib?,pc=succ,rs2,m2]


 **ib2 is any other instruction (right side):**

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))
  (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)).
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; apply expand_matchiblock_correct in MI.
      econstructor; eauto. apply expand_correct; trivial.
      econstructor. apply expand_preserves_iblock_istep_run.
      eapply expand_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
  (STEP : RTL.step ge (RTL.State st f sp pcR1 rs m) t s1')
  (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.
  inversion MSTRONG; subst. inv MIB.
  - (* mib_BF *)
    inv H0;
    inversion STEP; subst; try_simplify_someHyps; intros.
    + (* Breturn *)
      eexists; left; eexists; split.
      * econstructor; eauto. econstructor.
        eexists; eexists; split.
        eapply iblock_istep_run_equiv in BTL_RUN.
        eapply BTL_RUN. econstructor; eauto.
        erewrite preserv_fnstacksize; eauto.
      * econstructor; eauto.
    + (* Bcall *)
      rename H10 into FIND.
      eapply find_function_preserved in FIND.
      destruct FIND as (fd' & FF & TRANSFUN).
      eexists; left; eexists; split.
      * econstructor; eauto. econstructor.
        eexists; eexists; split.
        eapply iblock_istep_run_equiv in BTL_RUN.
        eapply BTL_RUN. econstructor; eauto.
        eapply function_sig_translated; eauto.
      * repeat (econstructor; eauto).
        eapply transf_fundef_correct; eauto.
    + (* Btailcall *)
      rename H9 into FIND.
      eapply find_function_preserved in FIND.
      destruct FIND as (fd' & FF & TRANSFUN).
      eexists; left; eexists; split.
      * econstructor; eauto. econstructor.
        eexists; eexists; split.
        eapply iblock_istep_run_equiv in BTL_RUN.
        eapply BTL_RUN. econstructor; eauto.
        eapply function_sig_translated; eauto.
        erewrite preserv_fnstacksize; eauto.
      * repeat (econstructor; eauto).
        eapply transf_fundef_correct; eauto.
    + (* Bbuiltin *)
      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 expand_matchiblock_correct in MI.
        { econstructor; eauto. apply expand_correct; trivial.  
          apply star_refl. apply expand_preserves_iblock_istep_run. }
        eapply expand_entry_isnt_goto; eauto.
    + (* 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 expand_matchiblock_correct in MI.
        { econstructor; eauto. apply expand_correct; trivial.  
          apply star_refl. apply expand_preserves_iblock_istep_run. }
        eapply expand_entry_isnt_goto; 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.
    + (* Bnop *)
      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.
    + (* Bop *)
      eapply match_strong_state_simu.
      1,2: do 2 (econstructor; 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.
    + (* Bload *)
      eapply match_strong_state_simu.
      1,2: do 2 (econstructor; 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.
    + (* Bstore *)
      eapply match_strong_state_simu.
      1,2: do 2 (econstructor; 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.
  - (* mib_cond *)
    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; 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

Two possible executions:

<<

 **Last instruction (left side):**

    RTL state         match_states          BTL state
       s1 ------------------------------------ s2
       |                                       |
  STEP |       Classical lockstep simu         | 
       |                                       | 
       s1' ----------------------------------- s2' 


 **Middle instruction (right side):**

    RTL state         match_states [oib]    BTL state
       s1 ------------------------------------ s2
       |                               _______/
  STEP | *E0       ___________________/         
       |          / match_states [oib']         
       s1' ______/
   Where omeasure oib' < omeasure oib

>>
*)

Theorem opt_simu s1 t s1' oib s2:
 RTL.step ge s1 t s1' ->
 match_states oib s1 s2 ->
 exists (oib' : option iblock),
     (exists s2', step tge s2 t s2' /\ match_states oib' s1' s2')
  \/ (omeasure oib' < omeasure oib /\ t=E0 /\ match_states oib' s1' s2) 
 .
Proof.
  inversion 2; subst; clear H0.
  - (* State *)
    exploit opt_simu_intro; eauto.
  - (* Callstate *)
    inv H.
    + (* Internal function *)
      inv TRANSF.
      rename H0 into TRANSF.
      eapply dupmap_entrypoint in TRANSF as ENTRY.
      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.
      * eapply exec_function_internal.
        erewrite preserv_fnstacksize; eauto.
      * apply expand_matchiblock_correct in MI.
        econstructor. econstructor; eauto.
        apply expand_correct; trivial.
        3: eapply expand_entry_isnt_goto; eauto.
        all: erewrite preserv_fnparams; eauto.
        constructor.
        apply expand_preserves_iblock_istep_run.
    + (* External function *)
      inv TRANSF.
      eexists; left; eexists; split.
      * eapply exec_function_external.
        eapply external_call_symbols_preserved.
        eapply senv_preserved. eauto.
      * econstructor; eauto.
  - (* Returnstate *)
    inv H. inv STACKS. inv H1.
    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 expand_matchiblock_correct in MI.
      econstructor. econstructor; eauto.
      apply expand_correct; trivial.
      constructor. apply expand_preserves_iblock_istep_run.
      eapply expand_entry_isnt_goto; eauto.
Qed.

Local Hint Resolve plus_one star_refl: core.

Theorem transf_program_correct:
  forward_simulation (RTL.semantics prog) (BTL.semantics tprog).
Proof.
  eapply (Forward_simulation (L1:=RTL.semantics prog) (L2:=semantics tprog) (ltof _ omeasure) match_states).
  constructor 1; simpl.
  - apply well_founded_ltof.
  - eapply transf_initial_states.
  - eapply transf_final_states.
  - intros s1 t s1' STEP i s2 MATCH. exploit opt_simu; eauto. clear MATCH STEP.
    destruct 1 as (oib' & [ (s2' & STEP & MATCH) | (MEASURE & TRACE & MATCH) ]).
    + repeat eexists; eauto.
    + subst. repeat eexists; eauto.
  - eapply senv_preserved.
Qed.

End BTL_SIMULATES_RTL.