(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*          Sylvain Boulmé  Grenoble-INP, VERIMAG                      *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** Correctness proof for the branch tunneling optimization. *)

Require Import Coqlib Maps Errors.
Require Import AST Linking.
Require Import Values Memory Events Globalenvs Smallstep.
Require Import Op Locations LTL.
Require Import LTLTunneling.

Local Open Scope nat.


(** * Properties of the branch_target, when the verifier succeeds *)

Definition check_included_spec (c:code) (td:UF) (ok: option bblock) :=
   ok <> None -> forall pc, c!pc = None -> td!pc = None.

Lemma check_included_correct (td: UF) (c: code): 
  check_included_spec c td (check_included td c).
Proof. 
  apply PTree_Properties.fold_rec with (P := check_included_spec c).
- (* extensionality *)
  unfold check_included_spec. intros m m' a EQ IND X pc. rewrite <- EQ; auto.
- (* base case *)
  intros _ pc.  rewrite PTree.gempty; try congruence.
- (* inductive case *)
  unfold check_included_spec.
  intros m [|] pc bb NEW ATPC IND; simpl; try congruence.
  intros H pc0. rewrite PTree.gsspec; destruct (peq _ _); subst; simpl; try congruence.
  intros; eapply IND; try congruence.
Qed.

Inductive target_bounds (target: node -> node) (bound: node -> nat) (pc: node): (option bblock) -> Prop :=
 | TB_default (TB: target pc = pc) ob
     : target_bounds target bound pc ob
 | TB_branch s bb
     (EQ: target pc = target s)
     (DECREASE: bound s < bound pc)
     : target_bounds target bound pc (Some (Lbranch s::bb))
 | TB_cond cond args s1 s2 info bb
     (EQ1: target pc = target s1)
     (EQ2: target pc = target s2)
     (DEC1: bound s1 < bound pc)
     (DEC2: bound s2 < bound pc)
     : target_bounds target bound pc (Some (Lcond cond args s1 s2 info::bb))
 .
Local Hint Resolve TB_default: core.

Lemma target_None (td:UF) (pc: node): td!pc = None -> td pc = pc.
Proof.
  unfold target, get. intros H; rewrite H; auto.
Qed.
Local Hint Resolve target_None Z.abs_nonneg: core.

Lemma get_nonneg td pc t d: get td pc = (t, d) -> (0 <= d)%Z.
Proof.
  unfold get. destruct (td!_) as [(t0&d0)|]; intros H; inversion H; subst; simpl; lia || auto.
Qed.
Local Hint Resolve get_nonneg: core.

Definition bound (td: UF) (pc: node) := Z.to_nat (snd (get td pc)).

Lemma check_bblock_correct (td:UF) (pc:node) (bb: bblock):
  check_bblock td pc bb = OK tt -> 
  target_bounds (target td) (bound td) pc (Some bb).
Proof.
  unfold check_bblock, bound.
  destruct (td!pc) as [(tpc&dpc)|] eqn:Hpc; auto.
  assert (Tpc: td pc = tpc). { unfold target, get; rewrite Hpc; simpl; auto. }
  assert (Dpc: snd (get td pc) = Z.abs dpc). { unfold get; rewrite Hpc; simpl; auto. }
  destruct bb as [|[ ] bb]; simpl; try congruence.
  + destruct (get td s) as (ts, ds) eqn:Hs.
    repeat (destruct (peq _ _) || destruct (zlt _ _)); simpl; try congruence.
    intros; apply TB_branch.
    * rewrite Tpc. unfold target; rewrite Hs; simpl; auto.
    * rewrite Dpc, Hs; simpl. apply Z2Nat.inj_lt; eauto.
  + destruct (get td s1) as (ts1, ds1) eqn:Hs1.
    destruct (get td s2) as (ts2, ds2) eqn:Hs2.
    repeat (destruct (peq _ _) || destruct (zlt _ _)); simpl; try congruence.
    intros; apply TB_cond.
    * rewrite Tpc. unfold target; rewrite Hs1; simpl; auto.
    * rewrite Tpc. unfold target; rewrite Hs2; simpl; auto.
    * rewrite Dpc, Hs1; simpl. apply Z2Nat.inj_lt; eauto.
    * rewrite Dpc, Hs2; simpl. apply Z2Nat.inj_lt; eauto.
Qed.

Definition check_code_spec (td:UF) (c:code) (ok: res unit) :=
   ok = OK tt -> forall pc bb, c!pc = Some bb -> target_bounds (target td) (bound td) pc (Some bb).

Lemma check_code_correct (td:UF) c:
   check_code_spec td c (check_code td c).
Proof.
  apply PTree_Properties.fold_rec with (P := check_code_spec td).
- (* extensionality *)
  unfold check_code_spec. intros m m' a EQ IND X pc bb; subst. rewrite  <- ! EQ; eauto.
- (* base case *)
  intros _ pc.  rewrite PTree.gempty; try congruence.
- (* inductive case *)
  unfold check_code_spec.
  intros m [[]|] pc bb NEW ATPC IND; simpl; try congruence.
  intros H pc0 bb0. rewrite PTree.gsspec; destruct (peq _ _); subst; simpl; auto.
  intros X; inversion X; subst.
  apply check_bblock_correct; auto.
Qed.

Theorem branch_target_bounds:
  forall f tf pc, 
  tunnel_function f = OK tf ->
  target_bounds (branch_target f) (bound (branch_target f)) pc (f.(fn_code)!pc).
Proof.
  unfold tunnel_function; intros f f' pc.
  destruct (check_included _ _) eqn:H1; try congruence.
  destruct (check_code _ _) as [[]|] eqn:H2; simpl; try congruence.
  intros _.
  destruct ((fn_code f)!pc) eqn:X.
  - exploit check_code_correct; eauto.
  - exploit check_included_correct; eauto.
    congruence.
Qed.

Lemma tunnel_function_unfold:
  forall f tf pc,
  tunnel_function f = OK tf -> 
  (fn_code tf)!pc = option_map (tunnel_block (branch_target f)) (fn_code f)!pc.
Proof.
  unfold tunnel_function; intros f f' pc.
  destruct (check_included _ _) eqn:H1; try congruence.
  destruct (check_code _ _) as [[]|] eqn:H2; simpl; try congruence.
  intros X; inversion X; clear X; subst.
  simpl. rewrite PTree.gmap1. auto.
Qed.

Lemma tunnel_fundef_Internal:
  forall f tf, tunnel_fundef (Internal f) = OK tf
  -> exists tf', tunnel_function f = OK tf' /\ tf = Internal tf'.
Proof.
  intros f tf; simpl.
  destruct (tunnel_function f) eqn:X; simpl; try congruence.
  intros EQ; inversion EQ.
  eexists; split; eauto.
Qed.

Lemma tunnel_fundef_External:
  forall tf ef, tunnel_fundef (External ef) = OK tf
  -> tf = External ef.
Proof.
  intros tf ef; simpl. intros H; inversion H; auto.
Qed.

(** * Preservation of semantics *)

Definition match_prog (p tp: program) :=
  match_program (fun _ f tf => tunnel_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 PRESERVATION.

Variables prog tprog: program.
Hypothesis TRANSL: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Lemma functions_translated:
  forall (v: val) (f: fundef),
  Genv.find_funct ge v = Some f ->
  exists tf, tunnel_fundef f = OK tf /\ Genv.find_funct tge v = Some tf.
Proof.
  intros. exploit (Genv.find_funct_match TRANSL); eauto.
  intros (cu & tf & A & B & C).
  repeat eexists; intuition eauto.
Qed.

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

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 sig_preserved:
  forall f tf, tunnel_fundef f = OK tf -> funsig tf = funsig f.
Proof.
  intros. destruct f.
  - simpl in H. monadInv H. unfold tunnel_function in EQ. 
    destruct (check_included _ _); try congruence.
    monadInv EQ. simpl; auto.
  - simpl in H. monadInv H. reflexivity.
Qed.

Lemma fn_stacksize_preserved:
  forall f tf, tunnel_function f = OK tf -> fn_stacksize tf = fn_stacksize f.
Proof.
  intros f tf; unfold tunnel_function.
  destruct (check_included _ _); try congruence.
  destruct (check_code _ _); simpl; try congruence.
  intros H; inversion H; simpl; auto.
Qed.

Lemma fn_entrypoint_preserved:
  forall f tf, tunnel_function f = OK tf -> fn_entrypoint tf = branch_target f (fn_entrypoint f).
Proof.
  intros f tf; unfold tunnel_function.
  destruct (check_included _ _); try congruence.
  destruct (check_code _ _); simpl; try congruence.
  intros H; inversion H; simpl; auto.
Qed.


(** The proof of semantic preservation is a simulation argument
  based on diagrams of the following form:
<<
           st1 --------------- st2
            |                   |
           t|                  ?|t
            |                   |
            v                   v
           st1'--------------- st2'
>>
  The [match_states] predicate, defined below, captures the precondition
  between states [st1] and [st2], as well as the postcondition between
  [st1'] and [st2'].  One transition in the source code (left) can correspond
  to zero or one transition in the transformed code (right).  The
  "zero transition" case occurs when executing a [Lnop] instruction
  in the source code that has been removed by tunneling.

  In the definition of [match_states], what changes between the original and
  transformed codes is mainly the control-flow
  (in particular, the current program point [pc]), but also some values
  and memory states, since some [Vundef] values can become more defined
  as a consequence of eliminating useless [Lcond] instructions. *)

Definition locmap_lessdef (ls1 ls2: locset) : Prop :=
  forall l, Val.lessdef (ls1 l) (ls2 l).

Inductive match_stackframes: stackframe -> stackframe -> Prop :=
  | match_stackframes_intro:
      forall f tf sp ls0 bb tls0,
      locmap_lessdef ls0 tls0 ->
      tunnel_function f = OK tf ->
      match_stackframes
         (Stackframe f sp ls0 bb)
         (Stackframe tf sp tls0 (tunnel_block (branch_target f) bb)).

Inductive match_states: state -> state -> Prop :=
  | match_states_intro:
      forall s f tf sp pc ls m ts tls tm
        (STK: list_forall2 match_stackframes s ts)
        (LS: locmap_lessdef ls tls)
        (MEM: Mem.extends m tm)
        (TF: tunnel_function f = OK tf),
      match_states (State s f sp pc ls m)
                   (State ts tf sp (branch_target f pc) tls tm)
  | match_states_block:
      forall s f tf sp bb ls m ts tls tm
        (STK: list_forall2 match_stackframes s ts)
        (LS: locmap_lessdef ls tls)
        (MEM: Mem.extends m tm)
        (TF: tunnel_function f = OK tf),
      match_states (Block s f sp bb ls m)
                   (Block ts tf sp (tunnel_block (branch_target f) bb) tls tm)
  | match_states_interm:
      forall s f tf sp pc i bb ls m ts tls tm
        (STK: list_forall2 match_stackframes s ts)
        (LS: locmap_lessdef ls tls)
        (MEM: Mem.extends m tm)
        (IBRANCH: tunnel_instr (branch_target f) i = Lbranch pc)
        (TF: tunnel_function f = OK tf),
      match_states (Block s f sp (i :: bb) ls m)
                   (State ts tf sp pc tls tm)
  | match_states_call:
      forall s f tf ls m ts tls tm
        (STK: list_forall2 match_stackframes s ts)
        (LS: locmap_lessdef ls tls)
        (MEM: Mem.extends m tm)
        (TF: tunnel_fundef f = OK tf),
      match_states (Callstate s f ls m)
                   (Callstate ts tf tls tm)
  | match_states_return:
      forall s ls m ts tls tm
        (STK: list_forall2 match_stackframes s ts)
        (LS: locmap_lessdef ls tls)
        (MEM: Mem.extends m tm),
      match_states (Returnstate s ls m)
                   (Returnstate ts tls tm).

(** Properties of [locmap_lessdef] *)

Lemma reglist_lessdef:
  forall rl ls1 ls2,
  locmap_lessdef ls1 ls2 -> Val.lessdef_list (reglist ls1 rl) (reglist ls2 rl).
Proof.
  induction rl; simpl; intros; auto.
Qed.

Lemma locmap_set_lessdef:
  forall ls1 ls2 v1 v2 l,
  locmap_lessdef ls1 ls2 -> Val.lessdef v1 v2 -> locmap_lessdef (Locmap.set l v1 ls1) (Locmap.set l v2 ls2).
Proof.
  intros; red; intros l'. unfold Locmap.set. destruct (Loc.eq l l').
- destruct l; auto using Val.load_result_lessdef.
- destruct (Loc.diff_dec l l'); auto.
Qed.

Lemma locmap_set_undef_lessdef:
  forall ls1 ls2 l,
  locmap_lessdef ls1 ls2 -> locmap_lessdef (Locmap.set l Vundef ls1) ls2.
Proof.
  intros; red; intros l'. unfold Locmap.set. destruct (Loc.eq l l').
- destruct l; auto. destruct ty; auto. 
- destruct (Loc.diff_dec l l'); auto.
Qed.

Lemma locmap_undef_regs_lessdef:
  forall rl ls1 ls2,
  locmap_lessdef ls1 ls2 -> locmap_lessdef (undef_regs rl ls1) (undef_regs rl ls2).
Proof.
  induction rl as [ | r rl]; intros; simpl. auto. apply locmap_set_lessdef; auto. 
Qed.

Lemma locmap_undef_regs_lessdef_1:
  forall rl ls1 ls2,
  locmap_lessdef ls1 ls2 -> locmap_lessdef (undef_regs rl ls1) ls2.
Proof.
  induction rl as [ | r rl]; intros; simpl. auto. apply locmap_set_undef_lessdef; auto. 
Qed.

Lemma locmap_getpair_lessdef:
  forall p ls1 ls2,
  locmap_lessdef ls1 ls2 -> Val.lessdef (Locmap.getpair p ls1) (Locmap.getpair p ls2).
Proof.
  intros; destruct p; simpl; auto using Val.longofwords_lessdef.
Qed.

Lemma locmap_getpairs_lessdef:
  forall pl ls1 ls2,
  locmap_lessdef ls1 ls2 ->
  Val.lessdef_list (map (fun p => Locmap.getpair p ls1) pl) (map (fun p => Locmap.getpair p ls2) pl).
Proof.
  intros. induction pl; simpl; auto using locmap_getpair_lessdef.
Qed.

Lemma locmap_setpair_lessdef:
  forall p ls1 ls2 v1 v2,
  locmap_lessdef ls1 ls2 -> Val.lessdef v1 v2 -> locmap_lessdef (Locmap.setpair p v1 ls1) (Locmap.setpair p v2 ls2).
Proof.
  intros; destruct p; simpl; auto using locmap_set_lessdef, Val.loword_lessdef, Val.hiword_lessdef.
Qed.

Lemma locmap_setres_lessdef:
  forall res ls1 ls2 v1 v2,
  locmap_lessdef ls1 ls2 -> Val.lessdef v1 v2 -> locmap_lessdef (Locmap.setres res v1 ls1) (Locmap.setres res v2 ls2).
Proof.
  induction res; intros; simpl; auto using locmap_set_lessdef, Val.loword_lessdef, Val.hiword_lessdef.
Qed.

Lemma locmap_undef_caller_save_regs_lessdef:
  forall ls1 ls2,
  locmap_lessdef ls1 ls2 -> locmap_lessdef (undef_caller_save_regs ls1) (undef_caller_save_regs ls2).
Proof.
  intros; red; intros. unfold undef_caller_save_regs. 
  destruct l.
- destruct (Conventions1.is_callee_save r); auto.
- destruct sl; auto.
Qed.

Lemma find_function_translated:
  forall ros ls tls fd,
  locmap_lessdef ls tls ->
  find_function ge ros ls = Some fd ->
  exists tfd, tunnel_fundef fd = OK tfd /\ find_function tge ros tls = Some tfd.
Proof.
  intros. destruct ros; simpl in *.
- assert (E: tls (R m) = ls (R m)).
  { exploit Genv.find_funct_inv; eauto. intros (b & EQ). 
    generalize (H (R m)). rewrite EQ. intros LD; inv LD. auto. }
  rewrite E. exploit functions_translated; eauto.
- rewrite symbols_preserved. destruct (Genv.find_symbol ge i); inv H0. 
  exploit function_ptr_translated; eauto.
  intros (tf & X1 & X2). exists tf; intuition.
Qed.

Lemma call_regs_lessdef:
  forall ls1 ls2, locmap_lessdef ls1 ls2 -> locmap_lessdef (call_regs ls1) (call_regs ls2).
Proof.
  intros; red; intros. destruct l as [r | [] ofs ty]; simpl; auto.
Qed.

Lemma return_regs_lessdef:
  forall caller1 callee1 caller2 callee2,
  locmap_lessdef caller1 caller2 ->
  locmap_lessdef callee1 callee2 ->
  locmap_lessdef (return_regs caller1 callee1) (return_regs caller2 callee2).
Proof.
  intros; red; intros. destruct l; simpl.
- destruct (Conventions1.is_callee_save r); auto.
- destruct sl; auto.
Qed. 

(** To preserve non-terminating behaviours, we show that the transformed
  code cannot take an infinity of "zero transition" cases.
  We use the following [measure] function over source states,
  which decreases strictly in the "zero transition" case. *)

Definition measure (st: state) : nat :=
  match st with
  | State s f sp pc ls m => (bound (branch_target f) pc) * 2
  | Block s f sp (Lbranch pc :: _) ls m => (bound (branch_target f) pc) * 2 + 1
  | Block s f sp (Lcond _ _ pc1 pc2 _ :: _) ls m => (max (bound (branch_target f) pc1) (bound (branch_target f) pc2)) * 2 + 1
  | Block s f sp bb ls m => 0
  | Callstate s f ls m => 0
  | Returnstate s ls m => 0
  end.

Lemma match_parent_locset:
  forall s ts,
  list_forall2 match_stackframes s ts ->
  locmap_lessdef (parent_locset s) (parent_locset ts).
Proof.
  induction 1; simpl.
- red; auto.
- inv H; auto.
Qed.

Lemma tunnel_step_correct:
  forall st1 t st2, step ge st1 t st2 ->
  forall st1' (MS: match_states st1 st1'),
  (exists st2', step tge st1' t st2' /\ match_states st2 st2')
  \/ (measure st2 < measure st1 /\ t = E0 /\ match_states st2 st1')%nat.
Proof.
  induction 1; intros; try inv MS; try (simpl in IBRANCH; inv IBRANCH).

- (* entering a block *)
  exploit (branch_target_bounds f tf pc); eauto.
  rewrite H. intros X; inversion X.
  + (* TB_default *) 
    rewrite TB; left. econstructor; split.
    * econstructor. simpl. erewrite tunnel_function_unfold, H ; simpl; eauto.
    * econstructor; eauto.
  + (* FT_branch *)
    simpl; right.
    rewrite EQ; repeat (econstructor; lia || eauto).
  + (* FT_cond *)
    simpl; right.
    repeat (econstructor; lia || eauto); simpl.
    destruct (peq _ _); try congruence.
- (* Lop *)
  exploit eval_operation_lessdef. apply reglist_lessdef; eauto. eauto. eauto. 
  intros (tv & EV & LD).
  left; simpl; econstructor; split.
  eapply exec_Lop with (v := tv); eauto.
  rewrite <- EV. apply eval_operation_preserved. exact symbols_preserved.
  econstructor; eauto using locmap_set_lessdef, locmap_undef_regs_lessdef.
- (* Lload *)
  exploit eval_addressing_lessdef. apply reglist_lessdef; eauto. eauto. 
  intros (ta & EV & LD).
  exploit Mem.loadv_extends. eauto. eauto. eexact LD. 
  intros (tv & LOAD & LD').
  left; simpl; econstructor; split.
  eapply exec_Lload with (a := ta).
  rewrite <- EV. apply eval_addressing_preserved. exact symbols_preserved.
  eauto. eauto.
  econstructor; eauto using locmap_set_lessdef, locmap_undef_regs_lessdef.
- (* Lload notrap1 *)
  exploit eval_addressing_lessdef_none. apply reglist_lessdef; eauto. eassumption.
  left; simpl; econstructor; split.
  eapply exec_Lload_notrap1.
  rewrite <- H0.
  apply eval_addressing_preserved. exact symbols_preserved. eauto.
  econstructor; eauto using locmap_set_lessdef, locmap_undef_regs_lessdef.
- (* Lload notrap2 *)
  exploit eval_addressing_lessdef. apply reglist_lessdef; eauto. eauto. 
  intros (ta & EV & LD).
  destruct (Mem.loadv chunk tm ta) eqn:Htload.
  {
  left; simpl; econstructor; split.
  eapply exec_Lload.
  rewrite <- EV. apply eval_addressing_preserved. exact symbols_preserved.
  exact Htload. eauto.
  econstructor; eauto using locmap_set_lessdef, locmap_undef_regs_lessdef.
  }
  {
  left; simpl; econstructor; split.
  eapply exec_Lload_notrap2.
  rewrite <- EV. apply eval_addressing_preserved. exact symbols_preserved.
  exact Htload. eauto.
  econstructor; eauto using locmap_set_lessdef, locmap_undef_regs_lessdef.
  }
- (* Lgetstack *)
  left; simpl; econstructor; split.
  econstructor; eauto.
  econstructor; eauto using locmap_set_lessdef, locmap_undef_regs_lessdef.
- (* Lsetstack *)
  left; simpl; econstructor; split.
  econstructor; eauto.
  econstructor; eauto using locmap_set_lessdef, locmap_undef_regs_lessdef.
- (* Lstore *)
  exploit eval_addressing_lessdef. apply reglist_lessdef; eauto. eauto. 
  intros (ta & EV & LD).
  exploit Mem.storev_extends. eauto. eauto. eexact LD. apply LS.  
  intros (tm' & STORE & MEM').
  left; simpl; econstructor; split.
  eapply exec_Lstore with (a := ta).
  rewrite <- EV. apply eval_addressing_preserved. exact symbols_preserved.
  eauto. eauto.
  econstructor; eauto using locmap_undef_regs_lessdef.
- (* Lcall *)
  left; simpl.
  exploit find_function_translated; eauto.
  intros (tfd & Htfd & FIND).
  econstructor; split.
  + eapply exec_Lcall; eauto.
    erewrite sig_preserved; eauto.
  + econstructor; eauto.
    constructor; auto.
    constructor; auto.
- (* Ltailcall *)
  exploit find_function_translated. 2: eauto.
  { eauto using return_regs_lessdef, match_parent_locset. }
  intros (tfd & Htfd & FIND).
  exploit Mem.free_parallel_extends. eauto. eauto. intros (tm' & FREE & MEM').
  left; simpl; econstructor; split.
  + eapply exec_Ltailcall; eauto.
    * eapply sig_preserved; eauto.
    * erewrite fn_stacksize_preserved; eauto.
  + econstructor; eauto using return_regs_lessdef, match_parent_locset.
- (* Lbuiltin *)
  exploit eval_builtin_args_lessdef. eexact LS. eauto. eauto. intros (tvargs & EVA & LDA).
  exploit external_call_mem_extends; eauto. intros (tvres & tm' & A & B & C & D).
  left; simpl; econstructor; split.
  eapply exec_Lbuiltin; eauto.
  eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. 
  eapply external_call_symbols_preserved. apply senv_preserved. eauto.
  econstructor; eauto using locmap_setres_lessdef, locmap_undef_regs_lessdef.
- (* Lbranch (preserved) *)
  left; simpl; econstructor; split.
  eapply exec_Lbranch; eauto.
  fold (branch_target f pc). econstructor; eauto.
- (* Lbranch (eliminated) *)
  right; split. simpl. lia. split. auto. constructor; auto.
- (* Lcond (preserved) *)
  simpl; left; destruct (peq _ _) eqn: EQ.
  + econstructor; split.
    eapply exec_Lbranch. 
    destruct b.
    * constructor; eauto using locmap_undef_regs_lessdef_1.
    * rewrite e. constructor; eauto using locmap_undef_regs_lessdef_1.
  + econstructor; split.
    eapply exec_Lcond; eauto. eapply eval_condition_lessdef; eauto using reglist_lessdef.
    destruct b; econstructor; eauto using locmap_undef_regs_lessdef.
- (* Lcond (eliminated) *)
  destruct (peq _ _) eqn: EQ; try inv H1.
  right; split; simpl. 
  + destruct b.
    generalize (Nat.le_max_l (bound (branch_target f) pc1) (bound (branch_target f) pc2)); lia.
    generalize (Nat.le_max_r (bound (branch_target f) pc1) (bound (branch_target f) pc2)); lia.
  + destruct b.
    -- repeat (constructor; auto).
    -- rewrite e; repeat (constructor; auto).
- (* Ljumptable *)
  assert (tls (R arg) = Vint n).
  { generalize (LS (R arg)); rewrite H; intros LD; inv LD; auto. }
  left; simpl; econstructor; split.
  eapply exec_Ljumptable.
  eauto. rewrite list_nth_z_map, H0; simpl; eauto. eauto.
  econstructor; eauto using locmap_undef_regs_lessdef.
- (* Lreturn *)
  exploit Mem.free_parallel_extends. eauto. eauto. intros (tm' & FREE & MEM'). 
  left; simpl; econstructor; split.
  + eapply exec_Lreturn; eauto.
    erewrite fn_stacksize_preserved; eauto.
  + constructor; eauto using return_regs_lessdef, match_parent_locset.
- (* internal function *)
  exploit tunnel_fundef_Internal; eauto.
  intros (tf' & TF' & ITF). subst.
  exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl.
  intros (tm' & ALLOC & MEM').
  left; simpl.
  econstructor; split.
  + eapply exec_function_internal; eauto.
    erewrite fn_stacksize_preserved; eauto.
  + simpl.
    erewrite (fn_entrypoint_preserved f tf'); auto.
    econstructor; eauto using locmap_undef_regs_lessdef, call_regs_lessdef.
- (* external function *)
  exploit external_call_mem_extends; eauto using locmap_getpairs_lessdef.
  intros (tvres & tm' & A & B & C & D).
  left; simpl; econstructor; split.
  + erewrite (tunnel_fundef_External tf ef); eauto.
    eapply exec_function_external; eauto.
    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
  + simpl. econstructor; eauto using locmap_setpair_lessdef, locmap_undef_caller_save_regs_lessdef.
- (* return *)
  inv STK. inv H1.
  left; econstructor; split.
  eapply exec_return; eauto.
  constructor; auto.
Qed.

Lemma transf_initial_states:
  forall st1, initial_state prog st1 ->
  exists st2, initial_state tprog st2 /\ match_states st1 st2.
Proof.
  intros. inversion H.
  exploit function_ptr_translated; eauto.
  intros (tf & Htf & Hf).
  exists (Callstate nil tf (Locmap.init Vundef) m0); split.
  econstructor; eauto.
  apply (Genv.init_mem_transf_partial TRANSL); auto.
  rewrite (match_program_main TRANSL).
  rewrite symbols_preserved. eauto.
  rewrite <- H3. apply sig_preserved. auto.
  constructor. constructor. red; simpl; auto. apply Mem.extends_refl. auto.
Qed.

Lemma transf_final_states:
  forall st1 st2 r,
  match_states st1 st2 -> final_state st1 r -> final_state st2 r.
Proof.
  intros. inv H0. inv H. inv STK.
  set (p := map_rpair R (Conventions1.loc_result signature_main)) in *.
  generalize (locmap_getpair_lessdef p _ _ LS). rewrite H1; intros LD; inv LD.
  econstructor; eauto.
Qed.

Theorem transf_program_correct:
  forward_simulation (LTL.semantics prog) (LTL.semantics tprog).
Proof.
  eapply forward_simulation_opt.
  apply senv_preserved.
  eexact transf_initial_states.
  eexact transf_final_states.
  eexact tunnel_step_correct.
Qed.

End PRESERVATION.