path: root/backend/RTLTunnelingproof.v

(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*          Sylvain Boulmé  Grenoble-INP, VERIMAG                      *)
(*          Pierre Goutagny ENS-Lyon, 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 for RTL. *)
(* This is a port of Tunnelingproof.v, the same optimisation for LTL. *)

Require Import Coqlib Maps Errors.
Require Import AST Linking.
Require Import Values Memory Registers Events Globalenvs Smallstep.
Require Import Op Locations RTL.
Require Import RTLTunneling.
Require Import Conventions1.

Local Open Scope nat.

Definition check_included_spec (c:code) (td:UF) (ok: option instruction) :=
  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); unfold check_included_spec.
  - intros m m' oi EQ IND N pc. rewrite <- EQ. apply IND. apply N.
  - intros N pc. rewrite PTree.gempty. auto.
  - intros m oi pc v N S IND. destruct oi.
    + intros. rewrite PTree.gsspec. destruct (peq _ _); try congruence. apply IND. congruence. apply H0.
    + contradiction.
Qed.

Inductive target_bounds (target: node -> node) (bound: node -> nat) (pc: node) : option instruction -> Prop :=
  | TB_default (TB: target pc = pc) oi:
      target_bounds target bound pc oi
  | TB_nop s
      (EQ: target pc = target s)
      (DEC: bound s < bound pc):
      target_bounds target bound pc (Some (Inop s))
  | TB_cond cond args ifso ifnot info
      (EQSO: target pc = target ifso)
      (EQNOT: target pc = target ifnot)
      (DECSO: bound ifso < bound pc)
      (DECNOT: bound ifnot < bound pc):
      target_bounds target bound pc (Some (Icond cond args ifso ifnot info))
.
Local Hint Resolve TB_default: core.

Lemma target_None (td: UF) (pc: node): td!pc = None -> td pc = pc.
Proof.
  unfold target, get. intro EQ. rewrite EQ. 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!pc as [(tpc,dpc)|]; intro H; inv H; lia.
Qed.
Local Hint Resolve get_nonneg: core.

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


(* TODO: à réécrire proprement *)
Lemma check_instr_correct (td: UF) (pc: node) (i: instruction):
  check_instr td pc i = OK tt ->
  target_bounds (target td) (bound td) pc (Some i).
Proof.
  unfold check_instr. destruct (td!pc) as [(tpc,dpc)|] eqn:EQ.
  assert (DPC: snd (get td pc) = Z.abs dpc). { unfold get. rewrite EQ. auto. }
  - destruct i; try congruence.
    + destruct (get td n) as (ts,ds) eqn:EQs.
      destruct (peq _ _); try congruence.
      destruct (zlt _ _); try congruence. intros _.
      apply TB_nop. replace (td pc) with tpc.
      unfold target. rewrite EQs. auto.
      unfold target. unfold get. rewrite EQ. auto.
      unfold bound. rewrite DPC. rewrite EQs; simpl. apply Z2Nat.inj_lt; try lia. apply get_nonneg with td n ts. apply EQs.
    + destruct (get td n) as (tso,dso) eqn:EQSO.
      destruct (get td n0) as (tnot,dnot) eqn:EQNOT.
      intro H.
      repeat ((destruct (peq _ _) in H || destruct (zlt _ _) in H); try congruence).
      apply TB_cond; subst.
      * unfold target. replace (fst (get td pc)) with tnot. rewrite EQSO. auto.
        unfold get. rewrite EQ. auto.
      * unfold target. replace (fst (get td pc)) with tnot. rewrite EQNOT. auto.
        unfold get. rewrite EQ. auto.
      * unfold bound. rewrite DPC. apply Z2Nat.inj_lt; try lia. apply get_nonneg with td n tnot. rewrite EQSO. auto. rewrite EQSO. auto.
      * unfold bound. rewrite DPC. apply Z2Nat.inj_lt; try lia. apply get_nonneg with td n0 tnot. rewrite EQNOT; auto. rewrite EQNOT; auto.
  - intros _. apply TB_default. unfold target. unfold get. rewrite EQ. auto.
Qed.

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

Lemma check_code_correct (td:UF) c:
   check_code_spec td c (check_code td c).
Proof.
  unfold check_code. apply PTree_Properties.fold_rec; unfold check_code_spec.
  - intros. rewrite <- H in H2. apply H0; auto.
  - intros. rewrite PTree.gempty in H0. congruence.
  - intros m [[]|e] pc i N S IND; simpl; try congruence.
    intros H pc0 i0. rewrite PTree.gsspec. destruct (peq _ _).
    subst. intro. inv H0. apply check_instr_correct. apply H.
    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.
  intros. unfold tunnel_function in H.
  destruct (check_included _ _) eqn:EQinc; try congruence.
  monadInv H. rename EQ into EQcode.
  destruct (_ ! _) eqn:EQ.
  - exploit check_code_correct. destruct x. apply EQcode. apply EQ. auto.
  - exploit check_included_correct.
    rewrite EQinc. congruence.
    apply EQ.
    intro. apply TB_default. apply target_None. apply H.
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). apply H.
  intros (cu & tf & A & B & C).
  eexists. 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_match TRANSL).
  - apply H.
  - intros (cu & tf & A & B & C). exists tf. split. apply A. apply B.
Qed.

Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof.
  apply (Genv.find_symbol_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 _ _) in EQ; try congruence.
    monadInv EQ. auto.
  - monadInv H. auto.
Qed.

Lemma senv_preserved:
  Senv.equiv ge tge.
Proof.
  eapply (Genv.senv_match TRANSL). (* Il y a déjà une preuve de cette propriété très exactement, je ne vais pas réinventer la roue ici *)
Qed.

Inductive match_stackframes: stackframe -> stackframe -> Prop :=
  | match_stackframes_intro:
      forall res f tf sp pc rs trs
      (TF: tunnel_function f = OK tf)
      (RS: Registers.regs_lessdef rs trs),
      match_stackframes
        (Stackframe res f sp pc rs)
        (Stackframe res tf sp (branch_target f pc) trs).

Inductive match_states: state -> state -> Prop :=
  | match_states_intro:
      forall s ts f tf sp pc rs trs m tm
      (STK: list_forall2 match_stackframes s ts)
      (TF: tunnel_function f = OK tf)
      (RS: Registers.regs_lessdef rs trs)
      (MEM: Mem.extends m tm),
      match_states
        (State s f sp pc rs m)
        (State ts tf sp (branch_target f pc) trs tm)
  | match_states_call:
      forall s ts f tf a ta m tm
      (STK: list_forall2 match_stackframes s ts)
      (TF: tunnel_fundef f = OK tf)
      (ARGS: list_forall2 Val.lessdef a ta)
      (MEM: Mem.extends m tm),
      match_states
        (Callstate s f a m)
        (Callstate ts tf ta tm)
  | match_states_return:
      forall s ts v tv m tm
      (STK: list_forall2 match_stackframes s ts)
      (VAL: Val.lessdef v tv)
      (MEM: Mem.extends m tm),
      match_states
        (Returnstate s v m)
        (Returnstate ts tv tm).

Definition measure (st: state): nat :=
  match st with
  | State s f sp pc rs m => bound (branch_target f) pc
  | Callstate s f v m => 0
  | Returnstate s v m => 0
  end.


Lemma transf_initial_states:
  forall s1: state, initial_state prog s1 ->
  exists s2: state, initial_state tprog s2 /\ match_states s1 s2.
Proof.
  intros. inversion H as [b f m0 ge0 MEM SYM PTR SIG CALL].
  exploit function_ptr_translated.
  - apply PTR.
  - intros (tf & TPTR & TUN).
    exists (Callstate nil tf nil m0). split.
    + apply initial_state_intro with b.
      * apply (Genv.init_mem_match TRANSL). apply MEM.
      * rewrite (match_program_main TRANSL).
        rewrite symbols_preserved. apply SYM.
      * apply TPTR.
      * rewrite <- SIG. apply sig_preserved. apply TUN.
    + apply match_states_call.
      * apply list_forall2_nil.
      * apply TUN.
      * apply list_forall2_nil.
      * apply Mem.extends_refl.
Qed.

Lemma transf_final_states:
  forall (s1 : state)
  (s2 : state) (r : Integers.Int.int),
  match_states s1 s2 ->
  final_state s1 r ->
  final_state s2 r.
Proof.
  intros. inv H0. inv H. inv VAL. inversion STK. apply final_state_intro.
Qed.

Lemma tunnel_function_unfold:
  forall f tf pc,
  tunnel_function f = OK tf ->
  (fn_code tf) ! pc =
  option_map (tunnel_instr (branch_target f)) (fn_code f) ! pc.
Proof.
  intros f tf pc.
  unfold tunnel_function.
  destruct (check_included _ _) eqn:EQinc; try congruence.
  destruct (check_code _ _) eqn:EQcode; simpl; try congruence.
  intro. inv H. simpl. rewrite PTree.gmap1. reflexivity.
Qed.

Lemma reglist_lessdef:
  forall (rs trs: Registers.Regmap.t val) (args: list Registers.reg),
  regs_lessdef rs trs -> Val.lessdef_list (rs##args) (trs##args).
Proof.
  intros. induction args; simpl; constructor.
  apply H. apply IHargs.
Qed.

Lemma instruction_type_preserved:
  forall (f tf:function) (pc:node) (i ti:instruction)
  (TF: tunnel_function f = OK tf)
  (FATPC: (fn_code f) ! pc = Some i)
  (NOTINOP: forall s, i <> Inop s)
  (NOTICOND: forall cond args ifso ifnot info, i <> Icond cond args ifso ifnot info)
  (TI: ti = tunnel_instr (branch_target f) i),
  (fn_code tf) ! (branch_target f pc) = Some ti.
Proof.
  intros.
  assert ((fn_code tf) ! pc = Some (tunnel_instr (branch_target f) i)) as TFATPC.
  rewrite (tunnel_function_unfold f tf pc); eauto.
  rewrite FATPC; eauto.
  exploit branch_target_bounds; eauto.
  intro TB. inversion TB as [BT|s|cond args ifso ifnot info]; try (rewrite FATPC in H; congruence).
Qed.

Lemma find_function_translated:
  forall ros rs trs fd,
  regs_lessdef rs trs ->
  find_function ge ros rs = Some fd ->
  exists tfd, tunnel_fundef fd = OK tfd /\ find_function tge ros trs = Some tfd.
Proof.
  intros. destruct ros; simpl in *.
  - (* reg *)
    assert (E: trs # r = rs # r).
    { exploit Genv.find_funct_inv. apply H0. intros (b & EQ).
      generalize (H r) . rewrite EQ. intro LD. inv LD. auto. }
    rewrite E. exploit functions_translated; eauto.
  - (* ident *)
    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 list_forall2_lessdef_rs:
  forall rs trs args,
  regs_lessdef rs trs ->
  list_forall2 Val.lessdef rs ## args trs ## args.
Proof.
  intros rs trs args LD.
  exploit (reglist_lessdef rs trs args). apply LD.
  induction args; simpl; intros H; try constructor; inv H.
  apply H3. apply IHargs. apply H5.
Qed.

Lemma fn_stacksize_preserved:
  forall f tf
  (TF: tunnel_function f = OK tf),
  fn_stacksize f = fn_stacksize tf.
Proof.
  intros f tf. unfold tunnel_function.
  destruct (check_included _ _); try congruence.
  intro H. monadInv H. simpl. reflexivity.
Qed.

Lemma regs_setres_lessdef:
  forall res vres tvres rs trs,
  regs_lessdef rs trs -> Val.lessdef vres tvres ->
  regs_lessdef (regmap_setres res vres rs) (regmap_setres res tvres trs).
Proof.
  induction res; intros; simpl; try auto using set_reg_lessdef.
Qed.

Lemma regmap_optget_lessdef:
  forall or rs trs,
  regs_lessdef rs trs -> Val.lessdef (regmap_optget or Vundef rs) (regmap_optget or Vundef trs).
Proof.
  intros or rs trs RS.
  induction or; simpl; auto using set_reg_lessdef.
Qed.

Lemma tunnel_fundef_Internal:
  forall (f: function) (tf: fundef)
  (TF: tunnel_fundef (Internal f) = OK tf),
  exists (tf': function), tf = (Internal tf') /\ tunnel_function f = OK tf'.
Proof.
  intros f tf.
  unfold tunnel_fundef. simpl. intro H. monadInv H. exists x.
  split. reflexivity. apply EQ.
Qed.

Lemma tunnel_fundef_External:
  forall (ef: external_function) (tf: fundef)
  (TF: tunnel_fundef (External ef) = OK tf),
  tf = (External ef).
Proof.
  intros f tf.
  unfold tunnel_fundef. simpl. intro H. monadInv H. reflexivity.
Qed.


Lemma fn_entrypoint_preserved:
  forall f tf
  (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.
  intro TF. monadInv TF. simpl. reflexivity.
Qed.

Lemma init_regs_lessdef:
  forall f tf args targs
  (ARGS: list_forall2 Val.lessdef args targs)
  (TF: tunnel_function f = OK tf),
  regs_lessdef (init_regs args (fn_params f)) (init_regs targs (fn_params tf)).
Proof.
  assert (regs_lessdef (Regmap.init Vundef) (Regmap.init Vundef)) as Hundef.
  { unfold Regmap.init. unfold regs_lessdef. intro. unfold Regmap.get. rewrite PTree.gempty. apply Val.lessdef_undef. }

  intros f tf args targs ARGS.

  unfold tunnel_function. destruct (check_included _ _) eqn:EQinc; try congruence.
  intro TF. monadInv TF. simpl. 
  (* 
  induction ARGS.
  - induction (fn_params f) eqn:EQP; apply Hundef.
  - induction (fn_params f) eqn:EQP.
    * simpl. apply Hundef.
    * simpl. apply set_reg_lessdef. apply H. 
    *)
    
  generalize (fn_params f) as l. induction ARGS; induction l; try (simpl; apply Hundef).
    simpl. apply set_reg_lessdef; try assumption. apply IHARGS.
Qed.

Lemma lessdef_forall2_list:
  forall args ta,
  list_forall2 Val.lessdef args ta -> Val.lessdef_list args ta.
Proof.
  intros args ta H. induction H. apply Val.lessdef_list_nil. apply Val.lessdef_list_cons. apply H. apply IHlist_forall2.
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.
  intros st1 t st2 H. induction H; intros; try (inv MS).
  - (* Inop *)
    exploit branch_target_bounds. apply TF.
    rewrite H. intro. inv H0.
    + (* TB_default *)
      rewrite TB. left. eexists. split.
      * apply exec_Inop. rewrite (tunnel_function_unfold f tf pc). rewrite H. simpl. eauto. apply TF.
      * constructor; try assumption.
    + (* TB_nop *)
      simpl. right. repeat split. apply DEC.
      rewrite EQ. apply match_states_intro; assumption.
  - (* Iop *)
    exploit eval_operation_lessdef; try eassumption.
    apply reglist_lessdef. apply RS.
    intros (tv & EVAL & LD).
    left; eexists; split.
    + eapply exec_Iop with (v:=tv).
      apply instruction_type_preserved with (Iop op args res pc'); (simpl; auto)||congruence.
      rewrite <- EVAL. apply eval_operation_preserved. apply symbols_preserved.
    + apply match_states_intro; eauto. apply set_reg_lessdef. apply LD. apply RS.
  - (* Iload *)
    inv H0.
    + exploit eval_addressing_lessdef; try eassumption.
      apply reglist_lessdef. apply RS.
      intros (ta & EVAL' & LD).
      exploit Mem.loadv_extends; try eassumption.
      intros (tv & LOAD' & LD').
      left. eexists. split.
      * eapply exec_Iload.
        -- exploit instruction_type_preserved; (simpl; eauto)||congruence.
        -- try (eapply has_loaded_normal; eauto; rewrite <- EVAL'; apply eval_addressing_preserved; apply symbols_preserved).
      * apply match_states_intro; try assumption. apply set_reg_lessdef. apply LD'. apply RS.
    + destruct (eval_addressing) eqn:EVAL in LOAD.
      * specialize (LOAD v).
        exploit eval_addressing_lessdef; try eassumption.
        apply reglist_lessdef; apply RS.
        intros (ta & ADDR & LD).
        (* TODO: on peut sans doute factoriser ça *)
        destruct (Mem.loadv chunk tm ta) eqn:Htload.
        -- left; eexists; split.
           eapply exec_Iload.
           ++ exploit instruction_type_preserved; (simpl; eauto)||congruence.
           ++ try (eapply has_loaded_normal; eauto; rewrite <- ADDR; apply eval_addressing_preserved; apply symbols_preserved).
           ++ apply match_states_intro; try assumption. apply set_reg_lessdef; eauto.
        -- left; eexists; split.
           eapply exec_Iload.
           ++ exploit instruction_type_preserved; (simpl; eauto)||congruence.
           ++ eapply has_loaded_default; eauto.
              rewrite eval_addressing_preserved with (ge1:=ge).
              intros a EVAL'; rewrite ADDR in EVAL'; inv EVAL'. auto.
              apply symbols_preserved.
           ++ apply match_states_intro; try assumption. apply set_reg_lessdef; eauto.
      * exploit eval_addressing_lessdef_none; try eassumption.
        apply reglist_lessdef; apply RS.
        left. eexists. split.
        -- eapply exec_Iload.
           ++ exploit instruction_type_preserved; (simpl; eauto)||congruence.
           ++ eapply has_loaded_default; eauto.
              rewrite eval_addressing_preserved with (ge1:=ge).
              intros a EVAL'; rewrite H0 in EVAL'; inv EVAL'.
              apply symbols_preserved.
        -- apply match_states_intro; try assumption. apply set_reg_lessdef. apply Val.lessdef_undef. apply RS.
  - (* Lstore *)
    exploit eval_addressing_lessdef; try eassumption.
    apply reglist_lessdef; apply RS.
    intros (ta & EVAL & LD).
    exploit Mem.storev_extends; try eassumption. apply RS.
    intros (tm' & STORE & MEM').
    left. eexists. split.
    + eapply exec_Istore.
      * exploit instruction_type_preserved; (simpl; eauto)||congruence.
      * rewrite <- EVAL. apply eval_addressing_preserved. apply symbols_preserved.
      * rewrite STORE. reflexivity.
    + apply match_states_intro; try eassumption.
  - (* Icall *)
    left.
    exploit find_function_translated; try eassumption.
    intros (tfd & TFD & FIND).
    eexists. split.
    + eapply exec_Icall.
      * exploit instruction_type_preserved; (simpl; eauto)||congruence.
      * apply FIND.
      * apply sig_preserved. apply TFD.
    + apply match_states_call; try assumption.
      * apply list_forall2_cons; try assumption. apply match_stackframes_intro; try assumption.
      * apply list_forall2_lessdef_rs. apply RS.
  - (* Itailcall *)
    exploit find_function_translated; try eassumption.
    intros (tfd & TFD & FIND).
    exploit Mem.free_parallel_extends; try eassumption.
    intros (tm' & FREE & MEM').
    left. eexists. split.
    + eapply exec_Itailcall.
      * exploit instruction_type_preserved; (simpl; eauto)||congruence.
      * apply FIND.
      * apply sig_preserved. apply TFD.
      * erewrite <- fn_stacksize_preserved; try eassumption.
    + apply match_states_call; try assumption.
      apply list_forall2_lessdef_rs. apply RS.
  - (* Ibuiltin *)
    exploit eval_builtin_args_lessdef; try eassumption. apply RS.
    intros (vl2 & EVAL & LD).
    exploit external_call_mem_extends; try eassumption.
    intros (tvres & tm' & EXT & LDRES & MEM' & UNCHGD).
    left. eexists. split.
    + eapply exec_Ibuiltin.
      * exploit instruction_type_preserved; (simpl; eauto)||congruence.
      * eapply eval_builtin_args_preserved. eapply symbols_preserved. eapply EVAL.
      * eapply external_call_symbols_preserved. eapply senv_preserved. eapply EXT.
    + apply match_states_intro; try assumption. apply regs_setres_lessdef; try assumption.
  - (* Icond *)
    simpl. exploit branch_target_bounds. apply TF. rewrite H. intro. inv H1.
    + (* TB_default *)
      rewrite TB.
      destruct (fn_code tf)!pc as [[]|] eqn:EQ;
      assert (tunnel_function f = OK tf) as TF'; auto;
      unfold tunnel_function in TF; destruct (check_included _ _) in TF; monadInv TF;
      simpl in EQ; rewrite PTree.gmap1 in EQ; rewrite H in EQ; simpl in EQ; destruct (peq _ _) eqn: EQpeq in EQ; try congruence.
      * left. eexists. split. 
        -- eapply exec_Inop. simpl. rewrite PTree.gmap1. rewrite H. simpl. rewrite EQpeq. reflexivity.
        -- destruct b. apply match_states_intro; eauto. rewrite e. apply match_states_intro; eauto.
      * left. eexists. split.
        -- eapply exec_Icond; auto. simpl. rewrite PTree.gmap1. rewrite H. simpl. rewrite EQpeq. reflexivity. eapply eval_condition_lessdef; try eassumption. apply reglist_lessdef. apply RS.
        -- destruct b; apply match_states_intro; auto.
    + (* TB_cond *) right; repeat split; destruct b; try assumption.
      * rewrite EQSO. apply match_states_intro; try assumption.
      * rewrite EQNOT. apply match_states_intro; try assumption.
  - (* Ijumptable *)
    left. eexists. split.
    + eapply exec_Ijumptable.
      * exploit instruction_type_preserved; (simpl; eauto)||congruence.
      * generalize (RS arg). rewrite H0. intro. inv H2. reflexivity.
      * rewrite list_nth_z_map. rewrite H1. simpl. reflexivity.
    + apply match_states_intro; try eassumption.
  - (* Ireturn *)
    exploit Mem.free_parallel_extends; try eassumption.
    intros (tm' & FREE & MEM').
    left. eexists. split.
    + eapply exec_Ireturn.
      * exploit instruction_type_preserved; (simpl; eauto)||congruence.
      * erewrite <- fn_stacksize_preserved. eapply FREE. eapply TF.
    + apply match_states_return; try eassumption.
      apply regmap_optget_lessdef. apply RS.
  - (* internal function *)
    exploit tunnel_fundef_Internal; try eassumption.
    intros (tf' & EQ & TF'). subst.
    exploit Mem.alloc_extends; try eassumption. reflexivity. reflexivity.
    intros (m2' & ALLOC & EXT).
    left. eexists. split.
    + eapply exec_function_internal.
      rewrite <- (fn_stacksize_preserved f tf'). eapply ALLOC. eapply TF'.
    + rewrite (fn_entrypoint_preserved f tf'); try eassumption. apply match_states_intro; try eassumption.
      apply init_regs_lessdef. apply ARGS. apply TF'.
  - (* external function *)
    exploit external_call_mem_extends. eapply H. eapply MEM.  eapply lessdef_forall2_list. eapply ARGS.
    intros (tvres & tm' & EXTCALL & LD & EXT & MEMUNCHGD).
    left. eexists. split.
    + erewrite (tunnel_fundef_External ef tf); try eassumption.
      eapply exec_function_external. eapply external_call_symbols_preserved. eapply senv_preserved. eapply EXTCALL.
    + eapply match_states_return; try assumption.
  - (* return *)
    inv STK. inv H1.
    left. eexists. split.
    + eapply exec_return.
    + eapply match_states_intro; try assumption.
      apply set_reg_lessdef; try assumption.
Qed.


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

End PRESERVATION.