SimplLocalsproof.v

(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  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.     *)
(*                                                                     *)
(* *********************************************************************)

(** Semantic preservation for the SimplLocals pass. *)

Require Import FSets.
Require Import Coqlib Errors Ordered Maps Integers Floats.
Require Import AST Linking.
Require Import Values Memory Globalenvs Events Smallstep.
Require Import Ctypes Cop Clight SimplLocals.

Module VSF := FSetFacts.Facts(VSet).
Module VSP := FSetProperties.Properties(VSet).

Definition match_prog (p tp: program) : Prop :=
    match_program (fun ctx f tf => transf_fundef f = OK tf) eq p tp
 /\ prog_types tp = prog_types p.

Lemma match_transf_program:
  forall p tp, transf_program p = OK tp -> match_prog p tp.
Proof.
  unfold transf_program; intros. monadInv H. 
  split; auto. apply match_transform_partial_program. rewrite EQ. destruct x; auto.
Qed.

Section PRESERVATION.

Variable prog: program.
Variable tprog: program.
Hypothesis TRANSF: match_prog prog tprog.
Let ge := globalenv prog.
Let tge := globalenv tprog.

Lemma comp_env_preserved:
  genv_cenv tge = genv_cenv ge.
Proof.
  unfold tge, ge. destruct prog, tprog; simpl. destruct TRANSF as [_ EQ]. simpl in EQ. congruence.
Qed.

Lemma symbols_preserved:
  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof (Genv.find_symbol_match (proj1 TRANSF)).

Lemma senv_preserved:
  Senv.equiv ge tge.
Proof (Genv.senv_match (proj1 TRANSF)).

Lemma functions_translated:
  forall (v: val) (f: fundef),
  Genv.find_funct ge v = Some f ->
  exists tf, Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.
Proof (Genv.find_funct_transf_partial (proj1 TRANSF)).

Lemma function_ptr_translated:
  forall (b: block) (f: fundef),
  Genv.find_funct_ptr ge b = Some f ->
  exists tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
Proof (Genv.find_funct_ptr_transf_partial (proj1 TRANSF)).

Lemma type_of_fundef_preserved:
  forall fd tfd,
  transf_fundef fd = OK tfd -> type_of_fundef tfd = type_of_fundef fd.
Proof.
  intros. destruct fd; monadInv H; auto.
  monadInv EQ. simpl; unfold type_of_function; simpl. auto.
Qed.

(** Matching between environments before and after *)

Inductive match_var (f: meminj) (cenv: compilenv) (e: env) (m: mem) (te: env) (tle: temp_env) (id: ident) : Prop :=
  | match_var_lifted: forall b ty chunk v tv
      (ENV: e!id = Some(b, ty))
      (TENV: te!id = None)
      (LIFTED: VSet.mem id cenv = true)
      (MAPPED: f b = None)
      (MODE: access_mode ty = By_value chunk)
      (LOAD: Mem.load chunk m b 0 = Some v)
      (TLENV: tle!(id) = Some tv)
      (VINJ: Val.inject f v tv),
      match_var f cenv e m te tle id
  | match_var_not_lifted: forall b ty b'
      (ENV: e!id = Some(b, ty))
      (TENV: te!id = Some(b', ty))
      (LIFTED: VSet.mem id cenv = false)
      (MAPPED: f b = Some(b', 0)),
      match_var f cenv e m te tle id
  | match_var_not_local: forall
      (ENV: e!id = None)
      (TENV: te!id = None)
      (LIFTED: VSet.mem id cenv = false),
      match_var f cenv e m te tle id.

Record match_envs (f: meminj) (cenv: compilenv)
                  (e: env) (le: temp_env) (m: mem) (lo hi: block)
                  (te: env) (tle: temp_env) (tlo thi: block) : Prop :=
  mk_match_envs {
    me_vars:
      forall id, match_var f cenv e m te tle id;
    me_temps:
      forall id v,
      le!id = Some v ->
      (exists tv, tle!id = Some tv /\ Val.inject f v tv)
      /\ (VSet.mem id cenv = true -> v = Vundef);
    me_inj:
      forall id1 b1 ty1 id2 b2 ty2, e!id1 = Some(b1, ty1) -> e!id2 = Some(b2, ty2) -> id1 <> id2 -> b1 <> b2;
    me_range:
      forall id b ty, e!id = Some(b, ty) -> Ple lo b /\ Plt b hi;
    me_trange:
      forall id b ty, te!id = Some(b, ty) -> Ple tlo b /\ Plt b thi;
    me_mapped:
      forall id b' ty,
      te!id = Some(b', ty) -> exists b, f b = Some(b', 0) /\ e!id = Some(b, ty);
    me_flat:
      forall id b' ty b delta,
      te!id = Some(b', ty) -> f b = Some(b', delta) -> e!id = Some(b, ty) /\ delta = 0;
    me_incr:
      Ple lo hi;
    me_tincr:
      Ple tlo thi
  }.

(** Invariance by change of memory and injection *)

Lemma match_envs_invariant:
  forall f cenv e le m lo hi te tle tlo thi f' m',
  match_envs f cenv e le m lo hi te tle tlo thi ->
  (forall b chunk v,
    f b = None -> Ple lo b /\ Plt b hi -> Mem.load chunk m b 0 = Some v -> Mem.load chunk m' b 0 = Some v) ->
  inject_incr f f' ->
  (forall b, Ple lo b /\ Plt b hi -> f' b = f b) ->
  (forall b b' delta, f' b = Some(b', delta) -> Ple tlo b' /\ Plt b' thi -> f' b = f b) ->
  match_envs f' cenv e le m' lo hi te tle tlo thi.
Proof.
  intros until m'; intros ME LD INCR INV1 INV2.
  destruct ME; constructor; eauto.
(* vars *)
  intros. generalize (me_vars0 id); intros MV; inv MV.
  eapply match_var_lifted; eauto.
  rewrite <- MAPPED; eauto.
  eapply match_var_not_lifted; eauto.
  eapply match_var_not_local; eauto.
(* temps *)
  intros. exploit me_temps0; eauto. intros [[v' [A B]] C]. split; auto. exists v'; eauto.
(* mapped *)
  intros. exploit me_mapped0; eauto. intros [b [A B]]. exists b; split; auto.
(* flat *)
  intros. eapply me_flat0; eauto. rewrite <- H0. symmetry. eapply INV2; eauto.
Qed.

(** Invariance by external call *)

Lemma match_envs_extcall:
  forall f cenv e le m lo hi te tle tlo thi tm f' m',
  match_envs f cenv e le m lo hi te tle tlo thi ->
  Mem.unchanged_on (loc_unmapped f) m m' ->
  inject_incr f f' ->
  inject_separated f f' m tm ->
  Ple hi (Mem.nextblock m) -> Ple thi (Mem.nextblock tm) ->
  match_envs f' cenv e le m' lo hi te tle tlo thi.
Proof.
  intros. eapply match_envs_invariant; eauto.
  intros. eapply Mem.load_unchanged_on; eauto.
  red in H2. intros. destruct (f b) as [[b' delta]|] eqn:?.
  eapply H1; eauto.
  destruct (f' b) as [[b' delta]|] eqn:?; auto.
  exploit H2; eauto. unfold Mem.valid_block. intros [A B].
  extlia.
  intros. destruct (f b) as [[b'' delta']|] eqn:?. eauto.
  exploit H2; eauto. unfold Mem.valid_block. intros [A B].
  extlia.
Qed.

(** Properties of values resulting from a cast *)

Lemma val_casted_load_result:
  forall v ty chunk,
  val_casted v ty -> access_mode ty = By_value chunk ->
  Val.load_result chunk v = v.
Proof.
  intros. inversion H; clear H; subst v ty; simpl in H0.
- destruct sz.
  destruct si; inversion H0; clear H0; subst chunk; simpl in *; congruence.
  destruct si; inversion H0; clear H0; subst chunk; simpl in *; congruence.
  clear H1. inv H0. auto.
  inversion H0; clear H0; subst chunk. simpl in *.
  destruct (Int.eq n Int.zero); subst n; reflexivity.
- inv H0; auto.
- inv H0; auto.
- inv H0; auto.
- inv H0. unfold Mptr, Val.load_result; destruct Archi.ptr64; auto. 
- inv H0. unfold Mptr, Val.load_result; rewrite H1; auto.
- inv H0. unfold Val.load_result; rewrite H1; auto.
- inv H0. unfold Mptr, Val.load_result; rewrite H1; auto.
- inv H0. unfold Val.load_result; rewrite H1; auto.
- discriminate.
- discriminate.
- discriminate.
Qed.

Lemma val_casted_inject:
  forall f v v' ty,
  Val.inject f v v' -> val_casted v ty -> val_casted v' ty.
Proof.
  intros. inv H; auto.
  inv H0; constructor; auto.
  inv H0; constructor.
Qed.

Lemma forall2_val_casted_inject:
  forall f vl vl', Val.inject_list f vl vl' ->
  forall tyl, list_forall2 val_casted vl tyl -> list_forall2 val_casted vl' tyl.
Proof.
  induction 1; intros tyl F; inv F; constructor; eauto. eapply val_casted_inject; eauto.
Qed.

Inductive val_casted_list: list val -> typelist -> Prop :=
  | vcl_nil:
      val_casted_list nil Tnil
  | vcl_cons: forall v1 vl ty1 tyl,
      val_casted v1 ty1 -> val_casted_list vl tyl ->
      val_casted_list (v1 :: vl) (Tcons  ty1 tyl).

Lemma val_casted_list_params:
  forall params vl,
  val_casted_list vl (type_of_params params) ->
  list_forall2 val_casted vl (map snd params).
Proof.
  induction params; simpl; intros.
  inv H. constructor.
  destruct a as [id ty]. inv H. constructor; auto.
Qed.

(** Correctness of [make_cast] *)

Lemma make_cast_correct:
  forall e le m a v1 tto v2,
  eval_expr tge e le m a v1 ->
  sem_cast v1 (typeof a) tto m = Some v2 ->
  eval_expr tge e le m (make_cast a tto) v2.
Proof.
  intros.
  assert (DFL: eval_expr tge e le m (Ecast a tto) v2).
    econstructor; eauto.
  unfold sem_cast, make_cast in *.
  destruct (classify_cast (typeof a) tto); auto.
  destruct v1; destruct Archi.ptr64; inv H0; auto.
  destruct sz2; auto. destruct v1; inv H0; auto.
  destruct v1; inv H0; auto.
  destruct v1; inv H0; auto.
  destruct v1; inv H0; auto.
  destruct v1; try discriminate.
  destruct (ident_eq id1 id2); inv H0; auto.
  destruct v1; try discriminate.
  destruct (ident_eq id1 id2); inv H0; auto.
  inv H0; auto.
Qed.

(** Debug annotations. *)

Lemma cast_typeconv:
  forall v ty m,
  val_casted v ty ->
  sem_cast v ty (typeconv ty) m = Some v.
Proof.
  induction 1; simpl.
- unfold sem_cast, classify_cast; destruct sz, Archi.ptr64; auto.
- auto.
- auto.
- unfold sem_cast, classify_cast; destruct Archi.ptr64; auto.
- auto.
- unfold sem_cast; simpl; rewrite H; auto.
- unfold sem_cast; simpl; rewrite H; auto.
- unfold sem_cast; simpl; rewrite H; auto.
- unfold sem_cast; simpl; rewrite H; auto.
- unfold sem_cast; simpl. rewrite dec_eq_true; auto.
- unfold sem_cast. simpl. rewrite dec_eq_true; auto.
- auto.
Qed.

Lemma step_Sdebug_temp:
  forall f id ty k e le m v,
  le!id = Some v ->
  val_casted v ty ->
  step2 tge (State f (Sdebug_temp id ty) k e le m)
         E0 (State f Sskip k e le m).
Proof.
  intros. unfold Sdebug_temp. eapply step_builtin with (optid := None).
  econstructor. constructor. eauto. simpl. eapply cast_typeconv; eauto. constructor.
  simpl. constructor.
Qed.

Lemma step_Sdebug_var:
  forall f id ty k e le m b,
  e!id = Some(b, ty) ->
  step2 tge (State f (Sdebug_var id ty) k e le m)
         E0 (State f Sskip k e le m).
Proof.
  intros. unfold Sdebug_var. eapply step_builtin with (optid := None).
  econstructor. constructor. constructor. eauto.
  simpl. reflexivity. constructor.
  simpl. constructor.
Qed.

Lemma step_Sset_debug:
  forall f id ty a k e le m v v',
  eval_expr tge e le m a v ->
  sem_cast v (typeof a) ty m = Some v' ->
  plus step2 tge (State f (Sset_debug id ty a) k e le m)
              E0 (State f Sskip k e (PTree.set id v' le) m).
Proof.
  intros; unfold Sset_debug.
  assert (forall k, step2 tge (State f (Sset id (make_cast a ty)) k e le m)
                           E0 (State f Sskip k e (PTree.set id v' le) m)).
  { intros. apply step_set. eapply make_cast_correct; eauto. }
  destruct (Compopts.debug tt).
- eapply plus_left. constructor.
  eapply star_left. apply H1.
  eapply star_left. constructor.
  apply star_one. apply step_Sdebug_temp with (v := v').
  apply PTree.gss. eapply cast_val_is_casted; eauto.
  reflexivity. reflexivity. reflexivity.
- apply plus_one. apply H1.
Qed.

Lemma step_add_debug_vars:
  forall f s e le m vars k,
  (forall id ty, In (id, ty) vars -> exists b, e!id = Some (b, ty)) ->
  star step2 tge (State f (add_debug_vars vars s) k e le m)
              E0 (State f s k e le m).
Proof.
  unfold add_debug_vars. destruct (Compopts.debug tt).
- induction vars; simpl; intros.
  + apply star_refl.
  + destruct a as [id ty].
    exploit H; eauto. intros (b & TE).
    simpl. eapply star_left. constructor.
    eapply star_left. eapply step_Sdebug_var; eauto.
    eapply star_left. constructor.
    apply IHvars; eauto.
    reflexivity. reflexivity. reflexivity.
- intros. apply star_refl.
Qed.

Remark bind_parameter_temps_inv:
  forall id params args le le',
  bind_parameter_temps params args le = Some le' ->
  ~In id (var_names params) ->
  le'!id = le!id.
Proof.
  induction params; simpl; intros.
  destruct args; inv H. auto.
  destruct a as [id1 ty1]. destruct args; try discriminate.
  transitivity ((PTree.set id1 v le)!id).
  eapply IHparams; eauto. apply PTree.gso. intuition.
Qed.

Lemma step_add_debug_params:
  forall f s k e le m params vl le1,
  list_norepet (var_names params) ->
  list_forall2 val_casted vl (map snd params) ->
  bind_parameter_temps params vl le1 = Some le ->
  star step2 tge (State f (add_debug_params params s) k e le m)
              E0 (State f s k e le m).
Proof.
  unfold add_debug_params. destruct (Compopts.debug tt).
- induction params as [ | [id ty] params ]; simpl; intros until le1; intros NR CAST BIND; inv CAST; inv NR.
  + apply star_refl.
  + assert (le!id = Some a1). { erewrite bind_parameter_temps_inv by eauto. apply PTree.gss. }
    eapply star_left. constructor.
    eapply star_left. eapply step_Sdebug_temp; eauto.
    eapply star_left. constructor.
    eapply IHparams; eauto.
    reflexivity. reflexivity. reflexivity.
- intros; apply star_refl.
Qed.

(** Preservation by assignment to lifted variable. *)

Lemma match_envs_assign_lifted:
  forall f cenv e le m lo hi te tle tlo thi b ty v m' id tv,
  match_envs f cenv e le m lo hi te tle tlo thi ->
  e!id = Some(b, ty) ->
  val_casted v ty ->
  Val.inject f v tv ->
  assign_loc ge ty m b Ptrofs.zero Full v m' ->
  VSet.mem id cenv = true ->
  match_envs f cenv e le m' lo hi te (PTree.set id tv tle) tlo thi.
Proof.
  intros. destruct H. generalize (me_vars0 id); intros MV; inv MV; try congruence.
  rewrite ENV in H0; inv H0. inv H3; try congruence.
  unfold Mem.storev in H0. rewrite Ptrofs.unsigned_zero in H0.
  constructor; eauto; intros.
(* vars *)
  destruct (peq id0 id). subst id0.
  eapply match_var_lifted with (v := v); eauto.
  exploit Mem.load_store_same; eauto. erewrite val_casted_load_result; eauto.
  apply PTree.gss.
  generalize (me_vars0 id0); intros MV; inv MV.
  eapply match_var_lifted; eauto.
  rewrite <- LOAD0. eapply Mem.load_store_other; eauto.
  rewrite PTree.gso; auto.
  eapply match_var_not_lifted; eauto.
  eapply match_var_not_local; eauto.
(* temps *)
  exploit me_temps0; eauto. intros [[tv1 [A B]] C]. split; auto.
  rewrite PTree.gsspec. destruct (peq id0 id).
  subst id0. exists tv; split; auto. rewrite C; auto.
  exists tv1; auto.
Qed.

(** Preservation by assignment to a temporary *)

Lemma match_envs_set_temp:
  forall f cenv e le m lo hi te tle tlo thi id v tv x,
  match_envs f cenv e le m lo hi te tle tlo thi ->
  Val.inject f v tv ->
  check_temp cenv id = OK x ->
  match_envs f cenv e (PTree.set id v le) m lo hi te (PTree.set id tv tle) tlo thi.
Proof.
  intros. unfold check_temp in H1.
  destruct (VSet.mem id cenv) eqn:?; monadInv H1.
  destruct H. constructor; eauto; intros.
(* vars *)
  generalize (me_vars0 id0); intros MV; inv MV.
  eapply match_var_lifted; eauto. rewrite PTree.gso. eauto. congruence.
  eapply match_var_not_lifted; eauto.
  eapply match_var_not_local; eauto.
(* temps *)
  rewrite PTree.gsspec in *. destruct (peq id0 id).
  inv H. split. exists tv; auto. intros; congruence.
  eapply me_temps0; eauto.
Qed.

Lemma match_envs_set_opttemp:
  forall f cenv e le m lo hi te tle tlo thi optid v tv x,
  match_envs f cenv e le m lo hi te tle tlo thi ->
  Val.inject f v tv ->
  check_opttemp cenv optid = OK x ->
  match_envs f cenv e (set_opttemp optid v le) m lo hi te (set_opttemp optid tv tle) tlo thi.
Proof.
  intros. unfold set_opttemp. destruct optid; simpl in H1.
  eapply match_envs_set_temp; eauto.
  auto.
Qed.

(** Extensionality with respect to temporaries *)

Lemma match_envs_temps_exten:
  forall f cenv e le m lo hi te tle tlo thi tle',
  match_envs f cenv e le m lo hi te tle tlo thi ->
  (forall id, tle'!id = tle!id) ->
  match_envs f cenv e le m lo hi te tle' tlo thi.
Proof.
  intros. destruct H. constructor; auto; intros.
  (* vars *)
  generalize (me_vars0 id); intros MV; inv MV.
  eapply match_var_lifted; eauto. rewrite H0; auto.
  eapply match_var_not_lifted; eauto.
  eapply match_var_not_local; eauto.
  (* temps *)
  rewrite H0. eauto.
Qed.

(** Invariance by assignment to an irrelevant temporary *)

Lemma match_envs_change_temp:
  forall f cenv e le m lo hi te tle tlo thi id v,
  match_envs f cenv e le m lo hi te tle tlo thi ->
  le!id = None -> VSet.mem id cenv = false ->
  match_envs f cenv e le m lo hi te (PTree.set id v tle) tlo thi.
Proof.
  intros. destruct H. constructor; auto; intros.
  (* vars *)
  generalize (me_vars0 id0); intros MV; inv MV.
  eapply match_var_lifted; eauto. rewrite PTree.gso; auto. congruence.
  eapply match_var_not_lifted; eauto.
  eapply match_var_not_local; eauto.
  (* temps *)
  rewrite PTree.gso. eauto. congruence.
Qed.

(** Properties of [cenv_for]. *)

Definition cenv_for_gen (atk: VSet.t) (vars: list (ident * type)) : compilenv :=
  List.fold_right (add_local_variable atk) VSet.empty vars.

Remark add_local_variable_charact:
  forall id ty atk cenv id1,
  VSet.In id1 (add_local_variable atk (id, ty) cenv) <->
  VSet.In id1 cenv \/ exists chunk, access_mode ty = By_value chunk /\ id = id1 /\ VSet.mem id atk = false.
Proof.
  intros. unfold add_local_variable. split; intros.
  destruct (access_mode ty) eqn:?; auto.
  destruct (VSet.mem id atk) eqn:?; auto.
  rewrite VSF.add_iff in H. destruct H; auto. right; exists m; auto.
  destruct H as [A | [chunk [A [B C]]]].
  destruct (access_mode ty); auto. destruct (VSet.mem id atk); auto. rewrite VSF.add_iff; auto.
  rewrite A. rewrite <- B. rewrite C. apply VSet.add_1; auto.
Qed.

Lemma cenv_for_gen_domain:
 forall atk id vars, VSet.In id (cenv_for_gen atk vars) -> In id (var_names vars).
Proof.
  induction vars; simpl; intros.
  rewrite VSF.empty_iff in H. auto.
  destruct a as [id1 ty1]. rewrite add_local_variable_charact in H.
  destruct H as [A | [chunk [A [B C]]]]; auto.
Qed.

Lemma cenv_for_gen_by_value:
  forall atk id ty vars,
  In (id, ty) vars ->
  list_norepet (var_names vars) ->
  VSet.In id (cenv_for_gen atk vars) ->
  exists chunk, access_mode ty = By_value chunk.
Proof.
  induction vars; simpl; intros.
  contradiction.
  destruct a as [id1 ty1]. simpl in H0. inv H0.
  rewrite add_local_variable_charact in H1.
  destruct H; destruct H1 as [A | [chunk [A [B C]]]].
  inv H. elim H4. eapply cenv_for_gen_domain; eauto.
  inv H. exists chunk; auto.
  eauto.
  subst id1. elim H4. change id with (fst (id, ty)). apply in_map; auto.
Qed.

Lemma cenv_for_gen_compat:
  forall atk id vars,
  VSet.In id (cenv_for_gen atk vars) -> VSet.mem id atk = false.
Proof.
  induction vars; simpl; intros.
  rewrite VSF.empty_iff in H. contradiction.
  destruct a as [id1 ty1]. rewrite add_local_variable_charact in H.
  destruct H as [A | [chunk [A [B C]]]].
  auto.
  congruence.
Qed.

(** Compatibility between a compilation environment and an address-taken set. *)

Definition compat_cenv (atk: VSet.t) (cenv: compilenv) : Prop :=
  forall id, VSet.In id atk -> VSet.In id cenv -> False.

Lemma compat_cenv_for:
  forall f, compat_cenv (addr_taken_stmt f.(fn_body)) (cenv_for f).
Proof.
  intros; red; intros.
  assert (VSet.mem id (addr_taken_stmt (fn_body f)) = false).
    eapply cenv_for_gen_compat. eexact H0.
  rewrite VSF.mem_iff in H. congruence.
Qed.

Lemma compat_cenv_union_l:
  forall atk1 atk2 cenv,
  compat_cenv (VSet.union atk1 atk2) cenv -> compat_cenv atk1 cenv.
Proof.
  intros; red; intros. eapply H; eauto. apply VSet.union_2; auto.
Qed.

Lemma compat_cenv_union_r:
  forall atk1 atk2 cenv,
  compat_cenv (VSet.union atk1 atk2) cenv -> compat_cenv atk2 cenv.
Proof.
  intros; red; intros. eapply H; eauto. apply VSet.union_3; auto.
Qed.

Lemma compat_cenv_empty:
  forall cenv, compat_cenv VSet.empty cenv.
Proof.
  intros; red; intros. eapply VSet.empty_1; eauto.
Qed.

Hint Resolve compat_cenv_union_l compat_cenv_union_r compat_cenv_empty: compat.

(** Allocation and initialization of parameters *)

Lemma alloc_variables_nextblock:
  forall ge e m vars e' m',
  alloc_variables ge e m vars e' m' -> Ple (Mem.nextblock m) (Mem.nextblock m').
Proof.
  induction 1.
  apply Ple_refl.
  eapply Ple_trans; eauto. exploit Mem.nextblock_alloc; eauto. intros EQ; rewrite EQ. apply Ple_succ.
Qed.

Lemma alloc_variables_range:
  forall ge id b ty e m vars e' m',
  alloc_variables ge e m vars e' m' ->
  e'!id = Some(b, ty) -> e!id = Some(b, ty) \/ Ple (Mem.nextblock m) b /\ Plt b (Mem.nextblock m').
Proof.
  induction 1; intros.
  auto.
  exploit IHalloc_variables; eauto. rewrite PTree.gsspec. intros [A|A].
  destruct (peq id id0). inv A.
  right. exploit Mem.alloc_result; eauto. exploit Mem.nextblock_alloc; eauto.
  generalize (alloc_variables_nextblock _ _ _ _ _ _ H0). intros A B C.
  subst b. split. apply Ple_refl. eapply Pos.lt_le_trans; eauto. rewrite B. apply Plt_succ.
  auto.
  right. exploit Mem.nextblock_alloc; eauto. intros B. rewrite B in A. extlia.
Qed.

Lemma alloc_variables_injective:
  forall ge id1 b1 ty1 id2 b2 ty2 e m vars e' m',
  alloc_variables ge e m vars e' m' ->
  (e!id1 = Some(b1, ty1) -> e!id2 = Some(b2, ty2) -> id1 <> id2 -> b1 <> b2) ->
  (forall id b ty, e!id = Some(b, ty) -> Plt b (Mem.nextblock m)) ->
  (e'!id1 = Some(b1, ty1) -> e'!id2 = Some(b2, ty2) -> id1 <> id2 -> b1 <> b2).
Proof.
  induction 1; intros.
  eauto.
  eapply IHalloc_variables; eauto.
  repeat rewrite PTree.gsspec; intros.
  destruct (peq id1 id); destruct (peq id2 id).
  congruence.
  inv H6. exploit Mem.alloc_result; eauto. exploit H2; eauto. unfold block; extlia.
  inv H7. exploit Mem.alloc_result; eauto. exploit H2; eauto. unfold block; extlia.
  eauto.
  intros. rewrite PTree.gsspec in H6. destruct (peq id0 id). inv H6.
  exploit Mem.alloc_result; eauto. exploit Mem.nextblock_alloc; eauto. unfold block; extlia.
  exploit H2; eauto. exploit Mem.nextblock_alloc; eauto. unfold block; extlia.
Qed.

Lemma match_alloc_variables:
  forall cenv e m vars e' m',
  alloc_variables ge e m vars e' m' ->
  forall j tm te,
  list_norepet (var_names vars) ->
  Mem.inject j m tm ->
  exists j', exists te', exists tm',
      alloc_variables tge te tm (remove_lifted cenv vars) te' tm'
  /\ Mem.inject j' m' tm'
  /\ inject_incr j j'
  /\ (forall b, Mem.valid_block m b -> j' b = j b)
  /\ (forall b b' delta, j' b = Some(b', delta) -> Mem.valid_block tm b' -> j' b = j b)
  /\ (forall b b' delta, j' b = Some(b', delta) -> ~Mem.valid_block tm b' ->
         exists id, exists ty, e'!id = Some(b, ty) /\ te'!id = Some(b', ty) /\ delta = 0)
  /\ (forall id ty, In (id, ty) vars ->
      exists b,
          e'!id = Some(b, ty)
       /\ if VSet.mem id cenv
          then te'!id = te!id /\ j' b = None
          else exists tb, te'!id = Some(tb, ty) /\ j' b = Some(tb, 0))
  /\ (forall id, ~In id (var_names vars) -> e'!id = e!id /\ te'!id = te!id).
Proof.
  induction 1; intros.
  (* base case *)
  exists j; exists te; exists tm. simpl.
  split. constructor.
  split. auto. split. auto. split. auto.  split. auto.
  split. intros. elim H2. eapply Mem.mi_mappedblocks; eauto.
  split. tauto. auto.

  (* inductive case *)
  simpl in H1. inv H1. simpl.
  destruct (VSet.mem id cenv) eqn:?. simpl.
  (* variable is lifted out of memory *)
  exploit Mem.alloc_left_unmapped_inject; eauto.
  intros [j1 [A [B [C D]]]].
  exploit IHalloc_variables; eauto. instantiate (1 := te).
  intros [j' [te' [tm' [J [K [L [M [N [Q [O P]]]]]]]]]].
  exists j'; exists te'; exists tm'.
  split. auto.
  split. auto.
  split. eapply inject_incr_trans; eauto.
  split. intros. transitivity (j1 b). apply M. eapply Mem.valid_block_alloc; eauto.
    apply D. apply Mem.valid_not_valid_diff with m; auto. eapply Mem.fresh_block_alloc; eauto.
  split. intros. transitivity (j1 b). eapply N; eauto.
    destruct (eq_block b b1); auto. subst.
    assert (j' b1 = j1 b1). apply M. eapply Mem.valid_new_block; eauto.
    congruence.
  split. exact Q.
  split. intros. destruct (ident_eq id0 id).
    (* same var *)
    subst id0.
    assert (ty0 = ty).
      destruct H1. congruence. elim H5. unfold var_names. change id with (fst (id, ty0)). apply in_map; auto.
    subst ty0.
    exploit P; eauto. intros [X Y]. rewrite Heqb. rewrite X. rewrite Y.
    exists b1. split. apply PTree.gss.
    split. auto.
    rewrite M. auto. eapply Mem.valid_new_block; eauto.
    (* other vars *)
    eapply O; eauto. destruct H1. congruence. auto.
  intros. exploit (P id0). tauto. intros [X Y]. rewrite X; rewrite Y.
    split; auto. apply PTree.gso. intuition.

  (* variable is not lifted out of memory *)
  exploit Mem.alloc_parallel_inject.
    eauto. eauto. apply Z.le_refl. apply Z.le_refl.
  intros [j1 [tm1 [tb1 [A [B [C [D E]]]]]]].
  exploit IHalloc_variables; eauto. instantiate (1 := PTree.set id (tb1, ty) te).
  intros [j' [te' [tm' [J [K [L [M [N [Q [O P]]]]]]]]]].
  exists j'; exists te'; exists tm'.
  split. simpl. econstructor; eauto. rewrite comp_env_preserved; auto.
  split. auto.
  split. eapply inject_incr_trans; eauto.
  split. intros. transitivity (j1 b). apply M. eapply Mem.valid_block_alloc; eauto.
    apply E. apply Mem.valid_not_valid_diff with m; auto. eapply Mem.fresh_block_alloc; eauto.
  split. intros. transitivity (j1 b). eapply N; eauto. eapply Mem.valid_block_alloc; eauto.
    destruct (eq_block b b1); auto. subst.
    assert (j' b1 = j1 b1). apply M. eapply Mem.valid_new_block; eauto.
    rewrite H4 in H1. rewrite D in H1. inv H1. eelim Mem.fresh_block_alloc; eauto.
  split. intros. destruct (eq_block b' tb1).
    subst b'. rewrite (N _ _ _ H1) in H1.
    destruct (eq_block b b1). subst b. rewrite D in H1; inv H1.
    exploit (P id); auto. intros [X Y]. exists id; exists ty.
    rewrite X; rewrite Y. repeat rewrite PTree.gss. auto.
    rewrite E in H1; auto. elim H3. eapply Mem.mi_mappedblocks; eauto.
    eapply Mem.valid_new_block; eauto.
    eapply Q; eauto. unfold Mem.valid_block in *.
    exploit Mem.nextblock_alloc. eexact A. exploit Mem.alloc_result. eexact A.
    unfold block; extlia.
  split. intros. destruct (ident_eq id0 id).
    (* same var *)
    subst id0.
    assert (ty0 = ty).
      destruct H1. congruence. elim H5. unfold var_names. change id with (fst (id, ty0)). apply in_map; auto.
    subst ty0.
    exploit P; eauto. intros [X Y]. rewrite Heqb. rewrite X. rewrite Y.
    exists b1. split. apply PTree.gss.
    exists tb1; split.
    apply PTree.gss.
    rewrite M. auto. eapply Mem.valid_new_block; eauto.
    (* other vars *)
    exploit (O id0 ty0). destruct H1. congruence. auto.
    rewrite PTree.gso; auto.
  intros. exploit (P id0). tauto. intros [X Y]. rewrite X; rewrite Y.
    split; apply PTree.gso; intuition.
Qed.

Lemma alloc_variables_load:
  forall e m vars e' m',
  alloc_variables ge e m vars e' m' ->
  forall chunk b ofs v,
  Mem.load chunk m b ofs = Some v ->
  Mem.load chunk m' b ofs = Some v.
Proof.
  induction 1; intros.
  auto.
  apply IHalloc_variables. eapply Mem.load_alloc_other; eauto.
Qed.

Lemma sizeof_by_value:
  forall ty chunk,
  access_mode ty = By_value chunk -> size_chunk chunk <= sizeof ge ty.
Proof.
  unfold access_mode; intros.
  assert (size_chunk chunk = sizeof ge ty).
  {
    destruct ty; try destruct i; try destruct s; try destruct f; inv H; auto;
    unfold Mptr; simpl; destruct Archi.ptr64; auto.
  }
  lia.
Qed.

Definition env_initial_value (e: env) (m: mem) :=
  forall id b ty chunk,
  e!id = Some(b, ty) -> access_mode ty = By_value chunk -> Mem.load chunk m b 0 = Some Vundef.

Lemma alloc_variables_initial_value:
  forall e m vars e' m',
  alloc_variables ge e m vars e' m' ->
  env_initial_value e m ->
  env_initial_value e' m'.
Proof.
  induction 1; intros.
  auto.
  apply IHalloc_variables. red; intros. rewrite PTree.gsspec in H2.
  destruct (peq id0 id). inv H2.
  eapply Mem.load_alloc_same'; eauto.
  lia. rewrite Z.add_0_l. eapply sizeof_by_value; eauto.
  apply Z.divide_0_r.
  eapply Mem.load_alloc_other; eauto.
Qed.

Lemma create_undef_temps_charact:
  forall id ty vars, In (id, ty) vars -> (create_undef_temps vars)!id = Some Vundef.
Proof.
  induction vars; simpl; intros.
  contradiction.
  destruct H. subst a. apply PTree.gss.
  destruct a as [id1 ty1]. rewrite PTree.gsspec. destruct (peq id id1); auto.
Qed.

Lemma create_undef_temps_inv:
  forall vars id v, (create_undef_temps vars)!id = Some v -> v = Vundef /\ In id (var_names vars).
Proof.
  induction vars; simpl; intros.
  rewrite PTree.gempty in H; congruence.
  destruct a as [id1 ty1]. rewrite PTree.gsspec in H. destruct (peq id id1).
  inv H. auto.
  exploit IHvars; eauto. tauto.
Qed.

Lemma create_undef_temps_exten:
  forall id l1 l2,
  (In id (var_names l1) <-> In id (var_names l2)) ->
  (create_undef_temps l1)!id = (create_undef_temps l2)!id.
Proof.
  assert (forall id l1 l2,
          (In id (var_names l1) -> In id (var_names l2)) ->
          (create_undef_temps l1)!id = None \/ (create_undef_temps l1)!id = (create_undef_temps l2)!id).
    intros. destruct ((create_undef_temps l1)!id) as [v1|] eqn:?; auto.
    exploit create_undef_temps_inv; eauto. intros [A B]. subst v1.
    exploit list_in_map_inv. unfold var_names in H. apply H. eexact B.
    intros [[id1 ty1] [P Q]]. simpl in P; subst id1.
    right; symmetry; eapply create_undef_temps_charact; eauto.
  intros.
  exploit (H id l1 l2). tauto.
  exploit (H id l2 l1). tauto.
  intuition congruence.
Qed.

Remark var_names_app:
  forall vars1 vars2, var_names (vars1 ++ vars2) = var_names vars1 ++ var_names vars2.
Proof.
  intros. apply map_app.
Qed.

Remark filter_app:
  forall (A: Type) (f: A -> bool) l1 l2,
  List.filter f (l1 ++ l2) = List.filter f l1 ++ List.filter f l2.
Proof.
  induction l1; simpl; intros.
  auto.
  destruct (f a). simpl. decEq; auto. auto.
Qed.

Remark filter_charact:
  forall (A: Type) (f: A -> bool) x l,
  In x (List.filter f l) <-> In x l /\ f x = true.
Proof.
  induction l; simpl. tauto.
  destruct (f a) eqn:?.
  simpl. rewrite IHl. intuition congruence.
  intuition congruence.
Qed.

Remark filter_norepet:
  forall (A: Type) (f: A -> bool) l,
  list_norepet l -> list_norepet (List.filter f l).
Proof.
  induction 1; simpl. constructor.
  destruct (f hd); auto. constructor; auto. rewrite filter_charact. tauto.
Qed.

Remark filter_map:
  forall (A B: Type) (f: A -> B) (pa: A -> bool) (pb: B -> bool),
  (forall a, pb (f a) = pa a) ->
  forall l, List.map f (List.filter pa l) = List.filter pb (List.map f l).
Proof.
  induction l; simpl.
  auto.
  rewrite H. destruct (pa a); simpl; congruence.
Qed.

Lemma create_undef_temps_lifted:
  forall id f,
  ~ In id (var_names (fn_params f)) ->
  (create_undef_temps (add_lifted (cenv_for f) (fn_vars f) (fn_temps f))) ! id =
  (create_undef_temps (add_lifted (cenv_for f) (fn_params f ++ fn_vars f) (fn_temps f))) ! id.
Proof.
  intros. apply create_undef_temps_exten.
  unfold add_lifted. rewrite filter_app.
  unfold var_names in *.
  repeat rewrite map_app. repeat rewrite in_app. intuition.
  exploit list_in_map_inv; eauto. intros [[id1 ty1] [P Q]]. simpl in P. subst id.
  rewrite filter_charact in Q. destruct Q.
  elim H. change id1 with (fst (id1, ty1)). apply List.in_map. auto.
Qed.

Lemma vars_and_temps_properties:
  forall cenv params vars temps,
  list_norepet (var_names params ++ var_names vars) ->
  list_disjoint (var_names params) (var_names temps) ->
  list_norepet (var_names params)
  /\ list_norepet (var_names (remove_lifted cenv (params ++ vars)))
  /\ list_disjoint (var_names params) (var_names (add_lifted cenv vars temps)).
Proof.
  intros. rewrite list_norepet_app in H. destruct H as [A [B C]].
  split. auto.
  split. unfold remove_lifted. unfold var_names. erewrite filter_map.
  instantiate (1 := fun a => negb (VSet.mem a cenv)). 2: auto.
  apply filter_norepet. rewrite map_app. apply list_norepet_append; assumption.
  unfold add_lifted. rewrite var_names_app.
  unfold var_names at 2. erewrite filter_map.
  instantiate (1 := fun a => VSet.mem a cenv). 2: auto.
  change (map fst vars) with (var_names vars).
  red; intros.
  rewrite in_app in H1. destruct H1.
  rewrite filter_charact in H1. destruct H1. apply C; auto.
  apply H0; auto.
Qed.

Theorem match_envs_alloc_variables:
  forall cenv m vars e m' temps j tm,
  alloc_variables ge empty_env m vars e m' ->
  list_norepet (var_names vars) ->
  Mem.inject j m tm ->
  (forall id ty, In (id, ty) vars -> VSet.mem id cenv = true ->
                     exists chunk, access_mode ty = By_value chunk) ->
  (forall id, VSet.mem id cenv = true -> In id (var_names vars)) ->
  exists j', exists te, exists tm',
     alloc_variables tge empty_env tm (remove_lifted cenv vars) te tm'
  /\ match_envs j' cenv e (create_undef_temps temps) m' (Mem.nextblock m) (Mem.nextblock m')
                        te (create_undef_temps (add_lifted cenv vars temps)) (Mem.nextblock tm) (Mem.nextblock tm')
  /\ Mem.inject j' m' tm'
  /\ inject_incr j j'
  /\ (forall b, Mem.valid_block m b -> j' b = j b)
  /\ (forall b b' delta, j' b = Some(b', delta) -> Mem.valid_block tm b' -> j' b = j b)
  /\ (forall id ty, In (id, ty) vars -> VSet.mem id cenv = false -> exists b, te!id = Some(b, ty)).
Proof.
  intros.
  exploit (match_alloc_variables cenv); eauto. instantiate (1 := empty_env).
  intros [j' [te [tm' [A [B [C [D [E [K [F G]]]]]]]]]].
  exists j'; exists te; exists tm'.
  split. auto. split; auto.
  constructor; intros.
  (* vars *)
  destruct (In_dec ident_eq id (var_names vars)).
  unfold var_names in i. exploit list_in_map_inv; eauto.
  intros [[id' ty] [EQ IN]]; simpl in EQ; subst id'.
  exploit F; eauto. intros [b [P R]].
  destruct (VSet.mem id cenv) eqn:?.
  (* local var, lifted *)
  destruct R as [U V]. exploit H2; eauto. intros [chunk X].
  eapply match_var_lifted with (v := Vundef) (tv := Vundef); eauto.
  rewrite U; apply PTree.gempty.
  eapply alloc_variables_initial_value; eauto.
  red. unfold empty_env; intros. rewrite PTree.gempty in H4; congruence.
  apply create_undef_temps_charact with ty.
  unfold add_lifted. apply in_or_app. left.
  rewrite filter_In. auto.
  (* local var, not lifted *)
  destruct R as [tb [U V]].
  eapply match_var_not_lifted; eauto.
  (* non-local var *)
  exploit G; eauto. unfold empty_env. rewrite PTree.gempty. intros [U V].
  eapply match_var_not_local; eauto.
  destruct (VSet.mem id cenv) eqn:?; auto.
  elim n; eauto.

  (* temps *)
  exploit create_undef_temps_inv; eauto. intros [P Q]. subst v.
  unfold var_names in Q. exploit list_in_map_inv; eauto.
  intros [[id1 ty] [EQ IN]]; simpl in EQ; subst id1.
  split; auto. exists Vundef; split; auto.
  apply create_undef_temps_charact with ty. unfold add_lifted.
  apply in_or_app; auto.

  (* injective *)
  eapply alloc_variables_injective. eexact H.
  rewrite PTree.gempty. congruence.
  intros. rewrite PTree.gempty in H7. congruence.
  eauto. eauto. auto.

  (* range *)
  exploit alloc_variables_range. eexact H. eauto.
  rewrite PTree.gempty. intuition congruence.

  (* trange *)
  exploit alloc_variables_range. eexact A. eauto.
  rewrite PTree.gempty. intuition congruence.

  (* mapped *)
  destruct (In_dec ident_eq id (var_names vars)).
  unfold var_names in i. exploit list_in_map_inv; eauto.
  intros [[id' ty'] [EQ IN]]; simpl in EQ; subst id'.
  exploit F; eauto. intros [b [P Q]].
  destruct (VSet.mem id cenv).
  rewrite PTree.gempty in Q. destruct Q; congruence.
  destruct Q as [tb [U V]]. exists b; split; congruence.
  exploit G; eauto. rewrite PTree.gempty. intuition congruence.

  (* flat *)
  exploit alloc_variables_range. eexact A. eauto.
  rewrite PTree.gempty. intros [P|P]. congruence.
  exploit K; eauto. unfold Mem.valid_block. extlia.
  intros [id0 [ty0 [U [V W]]]]. split; auto.
  destruct (ident_eq id id0). congruence.
  assert (b' <> b').
  eapply alloc_variables_injective with (e' := te) (id1 := id) (id2 := id0); eauto.
  rewrite PTree.gempty; congruence.
  intros until ty1; rewrite PTree.gempty; congruence.
  congruence.

  (* incr *)
  eapply alloc_variables_nextblock; eauto.
  eapply alloc_variables_nextblock; eauto.

  (* other properties *)
  intuition auto. edestruct F as (b & X & Y); eauto. rewrite H5 in Y.
  destruct Y as (tb & U & V). exists tb; auto.
Qed.

Lemma assign_loc_inject:
  forall f ty m loc ofs bf v m' tm loc' ofs' v',
  assign_loc ge ty m loc ofs bf v m' ->
  Val.inject f (Vptr loc ofs) (Vptr loc' ofs') ->
  Val.inject f v v' ->
  Mem.inject f m tm ->
  exists tm',
     assign_loc tge ty tm loc' ofs' bf v' tm'
  /\ Mem.inject f m' tm'
  /\ (forall b chunk v,
      f b = None -> Mem.load chunk m b 0 = Some v -> Mem.load chunk m' b 0 = Some v).
Proof.
  intros. inv H.
- (* by value *)
  exploit Mem.storev_mapped_inject; eauto. intros [tm' [A B]].
  exists tm'; split. eapply assign_loc_value; eauto.
  split. auto.
  intros. rewrite <- H5. eapply Mem.load_store_other; eauto.
  left. inv H0. congruence.
- (* by copy *)
  inv H0. inv H1.
  rename b' into bsrc. rename ofs'0 into osrc.
  rename loc into bdst. rename ofs into odst.
  rename loc' into bdst'. rename b2 into bsrc'.
  rewrite <- comp_env_preserved in *.
  destruct (zeq (sizeof tge ty) 0).
+ (* special case size = 0 *)
  assert (bytes = nil).
  { exploit (Mem.loadbytes_empty m bsrc (Ptrofs.unsigned osrc) (sizeof tge ty)).
    lia. congruence. }
  subst.
  destruct (Mem.range_perm_storebytes tm bdst' (Ptrofs.unsigned (Ptrofs.add odst (Ptrofs.repr delta))) nil)
  as [tm' SB].
  simpl. red; intros; extlia.
  exists tm'.
  split. eapply assign_loc_copy; eauto.
  intros; extlia.
  intros; extlia.
  rewrite e; right; lia.
  apply Mem.loadbytes_empty. lia.
  split. eapply Mem.storebytes_empty_inject; eauto.
  intros. rewrite <- H0. eapply Mem.load_storebytes_other; eauto.
  left. congruence.
+ (* general case size > 0 *)
  exploit Mem.loadbytes_length; eauto. intros LEN.
  assert (SZPOS: sizeof tge ty > 0).
  { generalize (sizeof_pos tge ty); lia. }
  assert (RPSRC: Mem.range_perm m bsrc (Ptrofs.unsigned osrc) (Ptrofs.unsigned osrc + sizeof tge ty) Cur Nonempty).
    eapply Mem.range_perm_implies. eapply Mem.loadbytes_range_perm; eauto. auto with mem.
  assert (RPDST: Mem.range_perm m bdst (Ptrofs.unsigned odst) (Ptrofs.unsigned odst + sizeof tge ty) Cur Nonempty).
    replace (sizeof tge ty) with (Z.of_nat (List.length bytes)).
    eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem.
    rewrite LEN. apply Z2Nat.id. lia.
  assert (PSRC: Mem.perm m bsrc (Ptrofs.unsigned osrc) Cur Nonempty).
    apply RPSRC. lia.
  assert (PDST: Mem.perm m bdst (Ptrofs.unsigned odst) Cur Nonempty).
    apply RPDST. lia.
  exploit Mem.address_inject.  eauto. eexact PSRC. eauto. intros EQ1.
  exploit Mem.address_inject.  eauto. eexact PDST. eauto. intros EQ2.
  exploit Mem.loadbytes_inject; eauto. intros [bytes2 [A B]].
  exploit Mem.storebytes_mapped_inject; eauto. intros [tm' [C D]].
  exists tm'.
  split. eapply assign_loc_copy; try rewrite EQ1; try rewrite EQ2; eauto.
  intros; eapply Mem.aligned_area_inject with (m := m); eauto.
  apply alignof_blockcopy_1248.
  apply sizeof_alignof_blockcopy_compat.
  intros; eapply Mem.aligned_area_inject with (m := m); eauto.
  apply alignof_blockcopy_1248.
  apply sizeof_alignof_blockcopy_compat.
  eapply Mem.disjoint_or_equal_inject with (m := m); eauto.
  apply Mem.range_perm_max with Cur; auto.
  apply Mem.range_perm_max with Cur; auto.
  split. auto.
  intros. rewrite <- H0. eapply Mem.load_storebytes_other; eauto.
  left. congruence.
- (* bitfield *)
  inv H3.
  exploit Mem.loadv_inject; eauto. intros (vc' & LD' & INJ). inv INJ.
  exploit Mem.storev_mapped_inject; eauto. intros [tm' [A B]].
  inv H1.
  exists tm'; split. eapply assign_loc_bitfield; eauto. econstructor; eauto.
  split. auto.
  intros. rewrite <- H3. eapply Mem.load_store_other; eauto.
  left. inv H0. congruence.
Qed.

Lemma assign_loc_nextblock:
  forall ge ty m b ofs bf v m',
  assign_loc ge ty m b ofs bf v m' -> Mem.nextblock m' = Mem.nextblock m.
Proof.
  induction 1.
  simpl in H0. eapply Mem.nextblock_store; eauto.
  eapply Mem.nextblock_storebytes; eauto.
  inv H. eapply Mem.nextblock_store; eauto.
Qed.

Theorem store_params_correct:
  forall j f k cenv le lo hi te tlo thi e m params args m',
  bind_parameters ge e m params args m' ->
  forall s tm tle1 tle2 targs,
  list_norepet (var_names params) ->
  list_forall2 val_casted args (map snd params) ->
  Val.inject_list j args targs ->
  match_envs j cenv e le m lo hi te tle1 tlo thi ->
  Mem.inject j m tm ->
  (forall id, ~In id (var_names params) -> tle2!id = tle1!id) ->
  (forall id, In id (var_names params) -> le!id = None) ->
  exists tle, exists tm',
  star step2 tge (State f (store_params cenv params s) k te tle tm)
              E0 (State f s k te tle tm')
  /\ bind_parameter_temps params targs tle2 = Some tle
  /\ Mem.inject j m' tm'
  /\ match_envs j cenv e le m' lo hi te tle tlo thi
  /\ Mem.nextblock tm' = Mem.nextblock tm.
Proof.
Local Opaque Conventions1.parameter_needs_normalization.
  induction 1; simpl; intros until targs; intros NOREPET CASTED VINJ MENV MINJ TLE LE.
- (* base case *)
  inv VINJ. exists tle2; exists tm; split. apply star_refl. split. auto. split. auto.
  split. apply match_envs_temps_exten with tle1; auto. auto.
- (* inductive case *)
  inv NOREPET. inv CASTED. inv VINJ.
  exploit me_vars; eauto. instantiate (1 := id); intros MV.
  destruct (VSet.mem id cenv) eqn:LIFTED.
+ (* lifted to temp *)
  exploit (IHbind_parameters s tm (PTree.set id v' tle1) (PTree.set id v' tle2)).
    eauto. eauto. eauto.
    eapply match_envs_assign_lifted; eauto.
    inv MV; try congruence. rewrite ENV in H; inv H.
    inv H0; try congruence.
    unfold Mem.storev in H2. eapply Mem.store_unmapped_inject; eauto.
    intros. repeat rewrite PTree.gsspec. destruct (peq id0 id). auto.
    apply TLE. intuition.
    eauto.
  intros (tle & tm' & U & V & X & Y & Z).
  exists tle, tm'; split; [|auto].
  destruct (Conventions1.parameter_needs_normalization (rettype_of_type ty)); [|assumption].
  assert (A: tle!id = Some v').
  { erewrite bind_parameter_temps_inv by eauto. apply PTree.gss. }
  eapply star_left. constructor.
  eapply star_left. econstructor. eapply make_cast_correct.
    constructor; eauto. apply cast_val_casted; auto. eapply val_casted_inject; eauto.
  rewrite PTree.gsident by auto.
  eapply star_left. constructor. eassumption.
  traceEq. traceEq. traceEq.
+ (* still in memory *)
  inv MV; try congruence. rewrite ENV in H; inv H.
  exploit assign_loc_inject; eauto.
  intros [tm1 [A [B C]]].
  exploit IHbind_parameters. eauto. eauto. eauto.
  instantiate (1 := PTree.set id v' tle1).
  apply match_envs_change_temp.
  eapply match_envs_invariant; eauto.
  apply LE; auto. auto.
  eauto.
  instantiate (1 := PTree.set id v' tle2).
  intros. repeat rewrite PTree.gsspec. destruct (peq id0 id). auto.
  apply TLE. intuition.
  intros. apply LE. auto.
  instantiate (1 := s).
  intros [tle [tm' [U [V [X [Y Z]]]]]].
  exists tle; exists tm'; split.
  eapply star_trans.
  eapply star_left. econstructor.
  eapply star_left. econstructor.
    eapply eval_Evar_local. eauto.
    eapply eval_Etempvar. erewrite bind_parameter_temps_inv; eauto.
    apply PTree.gss.
    simpl. instantiate (1 := v'). apply cast_val_casted.
    eapply val_casted_inject with (v := v1); eauto.
    simpl. eexact A.
  apply star_one. constructor.
  reflexivity. reflexivity.
  eexact U.
  traceEq.
  rewrite (assign_loc_nextblock _ _ _ _ _ _ _ _ A) in Z. auto.
Qed.

Lemma bind_parameters_nextblock:
  forall ge e m params args m',
  bind_parameters ge e m params args m' -> Mem.nextblock m' = Mem.nextblock m.
Proof.
  induction 1.
  auto.
  rewrite IHbind_parameters. eapply assign_loc_nextblock; eauto.
Qed.

Lemma bind_parameters_load:
  forall ge e chunk b ofs,
  (forall id b' ty, e!id = Some(b', ty) -> b <> b') ->
  forall m params args m',
  bind_parameters ge e m params args m' ->
  Mem.load chunk m' b ofs = Mem.load chunk m b ofs.
Proof.
  induction 2.
  auto.
  rewrite IHbind_parameters.
  assert (b <> b0) by eauto.
  inv H1.
  simpl in H5. eapply Mem.load_store_other; eauto.
  eapply Mem.load_storebytes_other; eauto.
Qed.

(** Freeing of local variables *)

Lemma free_blocks_of_env_perm_1:
  forall ce m e m' id b ty ofs k p,
  Mem.free_list m (blocks_of_env ce e) = Some m' ->
  e!id = Some(b, ty) ->
  Mem.perm m' b ofs k p ->
  0 <= ofs < sizeof ce ty ->
  False.
Proof.
  intros. exploit Mem.perm_free_list; eauto. intros [A B].
  apply B with 0 (sizeof ce ty); auto.
  unfold blocks_of_env. change (b, 0, sizeof ce ty) with (block_of_binding ce (id, (b, ty))).
  apply in_map. apply PTree.elements_correct. auto.
Qed.

Lemma free_list_perm':
  forall b lo hi l m m',
  Mem.free_list m l = Some m' ->
  In (b, lo, hi) l ->
  Mem.range_perm m b lo hi Cur Freeable.
Proof.
  induction l; simpl; intros.
  contradiction.
  destruct a as [[b1 lo1] hi1].
  destruct (Mem.free m b1 lo1 hi1) as [m1|] eqn:?; try discriminate.
  destruct H0. inv H0. eapply Mem.free_range_perm; eauto.
  red; intros. eapply Mem.perm_free_3; eauto. eapply IHl; eauto.
Qed.

Lemma free_blocks_of_env_perm_2:
  forall ce m e m' id b ty,
  Mem.free_list m (blocks_of_env ce e) = Some m' ->
  e!id = Some(b, ty) ->
  Mem.range_perm m b 0 (sizeof ce ty) Cur Freeable.
Proof.
  intros. eapply free_list_perm'; eauto.
  unfold blocks_of_env. change (b, 0, sizeof ce ty) with (block_of_binding ce (id, (b, ty))).
  apply in_map. apply PTree.elements_correct. auto.
Qed.

Fixpoint freelist_no_overlap (l: list (block * Z * Z)) : Prop :=
  match l with
  | nil => True
  | (b, lo, hi) :: l' =>
      freelist_no_overlap l' /\
      (forall b' lo' hi', In (b', lo', hi') l' ->
       b' <> b \/ hi' <= lo \/ hi <= lo')
  end.

Lemma can_free_list:
  forall l m,
  (forall b lo hi, In (b, lo, hi) l -> Mem.range_perm m b lo hi Cur Freeable) ->
  freelist_no_overlap l ->
  exists m', Mem.free_list m l = Some m'.
Proof.
  induction l; simpl; intros.
- exists m; auto.
- destruct a as [[b lo] hi]. destruct H0.
  destruct (Mem.range_perm_free m b lo hi) as [m1 A]; auto.
  rewrite A. apply IHl; auto.
  intros. red; intros. eapply Mem.perm_free_1; eauto.
  exploit H1; eauto. intros [B|B]. auto. right; lia.
  eapply H; eauto.
Qed.

Lemma blocks_of_env_no_overlap:
  forall (ge: genv) j cenv e le m lo hi te tle tlo thi tm,
  match_envs j cenv e le m lo hi te tle tlo thi ->
  Mem.inject j m tm ->
  (forall id b ty,
   e!id = Some(b, ty) -> Mem.range_perm m b 0 (sizeof ge ty) Cur Freeable) ->
  forall l,
  list_norepet (List.map fst l) ->
  (forall id bty, In (id, bty) l -> te!id = Some bty) ->
  freelist_no_overlap (List.map (block_of_binding ge) l).
Proof.
  intros until tm; intros ME MINJ PERMS. induction l; simpl; intros.
- auto.
- destruct a as [id [b ty]]. simpl in *. inv H. split.
  + apply IHl; auto.
  + intros. exploit list_in_map_inv; eauto. intros [[id' [b'' ty']] [A B]].
    simpl in A. inv A. rename b'' into b'.
    assert (TE: te!id = Some(b, ty)) by eauto.
    assert (TE': te!id' = Some(b', ty')) by eauto.
    exploit me_mapped. eauto. eexact TE. intros [b0 [INJ E]].
    exploit me_mapped. eauto. eexact TE'. intros [b0' [INJ' E']].
    destruct (zle (sizeof ge0 ty) 0); auto.
    destruct (zle (sizeof ge0 ty') 0); auto.
    assert (b0 <> b0').
    { eapply me_inj; eauto. red; intros; subst; elim H3.
      change id' with (fst (id', (b', ty'))). apply List.in_map; auto. }
    assert (Mem.perm m b0 0 Max Nonempty).
    { apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable.
      eapply PERMS; eauto. lia. auto with mem. }
    assert (Mem.perm m b0' 0 Max Nonempty).
    { apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable.
      eapply PERMS; eauto. lia. auto with mem. }
    exploit Mem.mi_no_overlap; eauto. intros [A|A]. auto. extlia.
Qed.

Lemma free_list_right_inject:
  forall j m1 l m2 m2',
  Mem.inject j m1 m2 ->
  Mem.free_list m2 l = Some m2' ->
  (forall b1 b2 delta lo hi ofs k p,
     j b1 = Some(b2, delta) -> In (b2, lo, hi) l ->
     Mem.perm m1 b1 ofs k p -> lo <= ofs + delta < hi -> False) ->
  Mem.inject j m1 m2'.
Proof.
  induction l; simpl; intros.
  congruence.
  destruct a as [[b lo] hi]. destruct (Mem.free m2 b lo hi) as [m21|] eqn:?; try discriminate.
  eapply IHl with (m2 := m21); eauto.
  eapply Mem.free_right_inject; eauto.
Qed.

Lemma blocks_of_env_translated:
  forall e, blocks_of_env tge e = blocks_of_env ge e.
Proof.
  intros. unfold blocks_of_env, block_of_binding.
  rewrite comp_env_preserved; auto.
Qed.

Theorem match_envs_free_blocks:
  forall j cenv e le m lo hi te tle tlo thi m' tm,
  match_envs j cenv e le m lo hi te tle tlo thi ->
  Mem.inject j m tm ->
  Mem.free_list m (blocks_of_env ge e) = Some m' ->
  exists tm',
     Mem.free_list tm (blocks_of_env tge te) = Some tm'
  /\ Mem.inject j m' tm'.
Proof.
  intros.
Local Opaque ge tge.
  assert (X: exists tm', Mem.free_list tm (blocks_of_env tge te) = Some tm').
  {
    rewrite blocks_of_env_translated. apply can_free_list.
  - (* permissions *)
    intros. unfold blocks_of_env in H2.
    exploit list_in_map_inv; eauto. intros [[id [b' ty]] [EQ IN]].
    unfold block_of_binding in EQ; inv EQ.
    exploit me_mapped; eauto. eapply PTree.elements_complete; eauto.
    intros [b [A B]].
    change 0 with (0 + 0). replace (sizeof ge ty) with (sizeof ge ty + 0) by lia.
    eapply Mem.range_perm_inject; eauto.
    eapply free_blocks_of_env_perm_2; eauto.
  - (* no overlap *)
    unfold blocks_of_env; eapply blocks_of_env_no_overlap; eauto.
    intros. eapply free_blocks_of_env_perm_2; eauto.
    apply PTree.elements_keys_norepet.
    intros. apply PTree.elements_complete; auto.
  }
  destruct X as [tm' FREE].
  exists tm'; split; auto.
  eapply free_list_right_inject; eauto.
  eapply Mem.free_list_left_inject; eauto.
  intros. unfold blocks_of_env in H3. exploit list_in_map_inv; eauto.
  intros [[id [b' ty]] [EQ IN]]. unfold block_of_binding in EQ. inv EQ.
  exploit me_flat; eauto. apply PTree.elements_complete; eauto.
  intros [P Q]. subst delta. eapply free_blocks_of_env_perm_1 with (m := m); eauto.
  rewrite <- comp_env_preserved. lia.
Qed.

(** Matching global environments *)

Inductive match_globalenvs (f: meminj) (bound: block): Prop :=
  | mk_match_globalenvs
      (DOMAIN: forall b, Plt b bound -> f b = Some(b, 0))
      (IMAGE: forall b1 b2 delta, f b1 = Some(b2, delta) -> Plt b2 bound -> b1 = b2)
      (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> Plt b bound)
      (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> Plt b bound)
      (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> Plt b bound).

Lemma match_globalenvs_preserves_globals:
  forall f,
  (exists bound, match_globalenvs f bound) ->
  meminj_preserves_globals ge f.
Proof.
  intros. destruct H as [bound MG]. inv MG.
  split; intros. eauto. split; intros. eauto. symmetry. eapply IMAGE; eauto.
Qed.

(** Evaluation of expressions *)

Section EVAL_EXPR.

Variables e te: env.
Variables le tle: temp_env.
Variables m tm: mem.
Variable f: meminj.
Variable cenv: compilenv.
Variables lo hi tlo thi: block.
Hypothesis MATCH: match_envs f cenv e le m lo hi te tle tlo thi.
Hypothesis MEMINJ: Mem.inject f m tm.
Hypothesis GLOB: exists bound, match_globalenvs f bound.

Lemma typeof_simpl_expr:
  forall a, typeof (simpl_expr cenv a) = typeof a.
Proof.
  destruct a; simpl; auto. destruct (VSet.mem i cenv); auto.
Qed.

Lemma deref_loc_inject:
  forall ty loc ofs bf v loc' ofs',
  deref_loc ty m loc ofs bf v ->
  Val.inject f (Vptr loc ofs) (Vptr loc' ofs') ->
  exists tv, deref_loc ty tm loc' ofs' bf tv /\ Val.inject f v tv.
Proof.
  intros. inv H.
- (* by value *)
  exploit Mem.loadv_inject; eauto. intros [tv [A B]].
  exists tv; split; auto. eapply deref_loc_value; eauto.
- (* by reference *)
  exists (Vptr loc' ofs'); split; auto. eapply deref_loc_reference; eauto.
- (* by copy *)
  exists (Vptr loc' ofs'); split; auto. eapply deref_loc_copy; eauto.
- (* bitfield *)
  inv H1.   exploit Mem.loadv_inject; eauto. intros [tc [A B]]. inv B. 
  econstructor; split. eapply deref_loc_bitfield. econstructor; eauto. constructor.
Qed.

Lemma eval_simpl_expr:
  forall a v,
  eval_expr ge e le m a v ->
  compat_cenv (addr_taken_expr a) cenv ->
  exists tv, eval_expr tge te tle tm (simpl_expr cenv a) tv /\ Val.inject f v tv

with eval_simpl_lvalue:
  forall a b ofs bf,
  eval_lvalue ge e le m a b ofs bf ->
  compat_cenv (addr_taken_expr a) cenv ->
  match a with Evar id ty => VSet.mem id cenv = false | _ => True end ->
  exists b', exists ofs', eval_lvalue tge te tle tm (simpl_expr cenv a) b' ofs' bf /\ Val.inject f (Vptr b ofs) (Vptr b' ofs').

Proof.
  destruct 1; simpl; intros.
(* const *)
  exists (Vint i); split; auto. constructor.
  exists (Vfloat f0); split; auto. constructor.
  exists (Vsingle f0); split; auto. constructor.
  exists (Vlong i); split; auto. constructor.
(* tempvar *)
  exploit me_temps; eauto. intros [[tv [A B]] C].
  exists tv; split; auto. constructor; auto.
(* addrof *)
  exploit eval_simpl_lvalue; eauto.
  destruct a; auto with compat.
  destruct a; auto. destruct (VSet.mem i cenv) eqn:?; auto.
  elim (H0 i). apply VSet.singleton_2. auto. apply VSet.mem_2. auto.
  intros [b' [ofs' [A B]]].
  exists (Vptr b' ofs'); split; auto. constructor; auto.
(* unop *)
  exploit eval_simpl_expr; eauto. intros [tv1 [A B]].
  exploit sem_unary_operation_inject; eauto. intros [tv [C D]].
  exists tv; split; auto. econstructor; eauto. rewrite typeof_simpl_expr; auto.
(* binop *)
  exploit eval_simpl_expr. eexact H. eauto with compat. intros [tv1 [A B]].
  exploit eval_simpl_expr. eexact H0. eauto with compat. intros [tv2 [C D]].
  exploit sem_binary_operation_inject; eauto. intros [tv [E F]].
  exists tv; split; auto. econstructor; eauto.
  repeat rewrite typeof_simpl_expr; rewrite comp_env_preserved; auto.
(* cast *)
  exploit eval_simpl_expr; eauto. intros [tv1 [A B]].
  exploit sem_cast_inject; eauto. intros [tv2 [C D]].
  exists tv2; split; auto. econstructor. eauto. rewrite typeof_simpl_expr; auto.
(* sizeof *)
  econstructor; split. constructor. rewrite comp_env_preserved; auto.
(* alignof *)
  econstructor; split. constructor. rewrite comp_env_preserved; auto.
(* rval *)
  assert (EITHER: (exists id, exists ty, a = Evar id ty /\ VSet.mem id cenv = true)
               \/ (match a with Evar id _ => VSet.mem id cenv = false | _ => True end)).
    destruct a; auto. destruct (VSet.mem i cenv) eqn:?; auto. left; exists i; exists t; auto.
  destruct EITHER as [ [id [ty [EQ OPT]]] | NONOPT ].
  (* a variable pulled out of memory *)
  subst a. simpl. rewrite OPT.
  exploit me_vars; eauto. instantiate (1 := id). intros MV.
  inv H; inv MV; try congruence.
  rewrite ENV in H7; inv H7.
  inv H0; try congruence.
  assert (chunk0 = chunk). simpl in H. congruence. subst chunk0.
  assert (v0 = v). unfold Mem.loadv in H2. rewrite Ptrofs.unsigned_zero in H2. congruence. subst v0.
  exists tv; split; auto. constructor; auto.
  simpl in H; congruence.
  simpl in H; congruence.
  (* any other l-value *)
  exploit eval_simpl_lvalue; eauto. intros [loc' [ofs' [A B]]].
  exploit deref_loc_inject; eauto. intros [tv [C D]].
  exists tv; split; auto. econstructor. eexact A. rewrite typeof_simpl_expr; auto.

(* lvalues *)
  destruct 1; simpl; intros.
(* local var *)
  rewrite H1.
  exploit me_vars; eauto. instantiate (1 := id). intros MV. inv MV; try congruence.
  rewrite ENV in H; inv H.
  exists b'; exists Ptrofs.zero; split.
  apply eval_Evar_local; auto.
  econstructor; eauto.
(* global var *)
  rewrite H2.
  exploit me_vars; eauto. instantiate (1 := id). intros MV. inv MV; try congruence.
  exists l; exists Ptrofs.zero; split.
  apply eval_Evar_global. auto. rewrite <- H0. apply symbols_preserved.
  destruct GLOB as [bound GLOB1]. inv GLOB1.
  econstructor; eauto.
(* deref *)
  exploit eval_simpl_expr; eauto. intros [tv [A B]].
  inversion B. subst.
  econstructor; econstructor; split; eauto. econstructor; eauto.
(* field struct *)
  rewrite <- comp_env_preserved in *.
  exploit eval_simpl_expr; eauto. intros [tv [A B]].
  inversion B. subst.
  econstructor; econstructor; split.
  eapply eval_Efield_struct; eauto. rewrite typeof_simpl_expr; eauto.
  econstructor; eauto. repeat rewrite Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut.
(* field union *)
  rewrite <- comp_env_preserved in *.
  exploit eval_simpl_expr; eauto. intros [tv [A B]].
  inversion B. subst.
  econstructor; econstructor; split.
  eapply eval_Efield_union; eauto. rewrite typeof_simpl_expr; eauto.
  econstructor; eauto. repeat rewrite Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut.
Qed.

Lemma eval_simpl_exprlist:
  forall al tyl vl,
  eval_exprlist ge e le m al tyl vl ->
  compat_cenv (addr_taken_exprlist al) cenv ->
  val_casted_list vl tyl /\
  exists tvl,
     eval_exprlist tge te tle tm (simpl_exprlist cenv al) tyl tvl
  /\ Val.inject_list f vl tvl.
Proof.
  induction 1; simpl; intros.
  split. constructor. econstructor; split. constructor. auto.
  exploit eval_simpl_expr; eauto with compat. intros [tv1 [A B]].
  exploit sem_cast_inject; eauto. intros [tv2 [C D]].
  exploit IHeval_exprlist; eauto with compat. intros [E [tvl [F G]]].
  split. constructor; auto. eapply cast_val_is_casted; eauto.
  exists (tv2 :: tvl); split. econstructor; eauto.
  rewrite typeof_simpl_expr; auto.
  econstructor; eauto.
Qed.

End EVAL_EXPR.

(** Matching continuations *)

Inductive match_cont (f: meminj): compilenv -> cont -> cont -> mem -> block -> block -> Prop :=
  | match_Kstop: forall cenv m bound tbound hi,
      match_globalenvs f hi -> Ple hi bound -> Ple hi tbound ->
      match_cont f cenv Kstop Kstop m bound tbound
  | match_Kseq: forall cenv s k ts tk m bound tbound,
      simpl_stmt cenv s = OK ts ->
      match_cont f cenv k tk m bound tbound ->
      compat_cenv (addr_taken_stmt s) cenv ->
      match_cont f cenv (Kseq s k) (Kseq ts tk) m bound tbound
  | match_Kloop1: forall cenv s1 s2 k ts1 ts2 tk m bound tbound,
      simpl_stmt cenv s1 = OK ts1 ->
      simpl_stmt cenv s2 = OK ts2 ->
      match_cont f cenv k tk m bound tbound ->
      compat_cenv (VSet.union (addr_taken_stmt s1) (addr_taken_stmt s2)) cenv ->
      match_cont f cenv (Kloop1 s1 s2 k) (Kloop1 ts1 ts2 tk) m bound tbound
  | match_Kloop2: forall cenv s1 s2 k ts1 ts2 tk m bound tbound,
      simpl_stmt cenv s1 = OK ts1 ->
      simpl_stmt cenv s2 = OK ts2 ->
      match_cont f cenv k tk m bound tbound ->
      compat_cenv (VSet.union (addr_taken_stmt s1) (addr_taken_stmt s2)) cenv ->
      match_cont f cenv (Kloop2 s1 s2 k) (Kloop2 ts1 ts2 tk) m bound tbound
  | match_Kswitch: forall cenv k tk m bound tbound,
      match_cont f cenv k tk m bound tbound ->
      match_cont f cenv (Kswitch k) (Kswitch tk) m bound tbound
  | match_Kcall: forall cenv optid fn e le k tfn te tle tk m hi thi lo tlo bound tbound x,
      transf_function fn = OK tfn ->
      match_envs f (cenv_for fn) e le m lo hi te tle tlo thi ->
      match_cont f (cenv_for fn) k tk m lo tlo ->
      check_opttemp (cenv_for fn) optid = OK x ->
      Ple hi bound -> Ple thi tbound ->
      match_cont f cenv (Kcall optid fn e le k)
                        (Kcall optid tfn te tle tk) m bound tbound.

(** Invariance property by change of memory and injection *)

Lemma match_cont_invariant:
  forall f' m' f cenv k tk m bound tbound,
  match_cont f cenv k tk m bound tbound ->
  (forall b chunk v,
    f b = None -> Plt b bound -> Mem.load chunk m b 0 = Some v -> Mem.load chunk m' b 0 = Some v) ->
  inject_incr f f' ->
  (forall b, Plt b bound -> f' b = f b) ->
  (forall b b' delta, f' b = Some(b', delta) -> Plt b' tbound -> f' b = f b) ->
  match_cont f' cenv k tk m' bound tbound.
Proof.
  induction 1; intros LOAD INCR INJ1 INJ2; econstructor; eauto.
(* globalenvs *)
  inv H. constructor; intros; eauto.
  assert (f b1 = Some (b2, delta)). rewrite <- H; symmetry; eapply INJ2; eauto. extlia.
  eapply IMAGE; eauto.
(* call *)
  eapply match_envs_invariant; eauto.
  intros. apply LOAD; auto. extlia.
  intros. apply INJ1; auto; extlia.
  intros. eapply INJ2; eauto; extlia.
  eapply IHmatch_cont; eauto.
  intros; apply LOAD; auto. inv H0; extlia.
  intros; apply INJ1. inv H0; extlia.
  intros; eapply INJ2; eauto. inv H0; extlia.
Qed.

(** Invariance by assignment to location "above" *)

Lemma match_cont_assign_loc:
  forall f cenv k tk m bound tbound ty loc ofs bf v m',
  match_cont f cenv k tk m bound tbound ->
  assign_loc ge ty m loc ofs bf v m' ->
  Ple bound loc ->
  match_cont f cenv k tk m' bound tbound.
Proof.
  intros. eapply match_cont_invariant; eauto.
  intros. rewrite <- H4. inv H0.
- (* scalar *)
  simpl in H6. eapply Mem.load_store_other; eauto. left. unfold block; extlia.
- (* block copy *)
  eapply Mem.load_storebytes_other; eauto. left. unfold block; extlia.
- (* bitfield *)
  inv H5. eapply Mem.load_store_other; eauto. left. unfold block; extlia.
Qed.

(** Invariance by external calls *)

Lemma match_cont_extcall:
  forall f cenv k tk m bound tbound tm f' m',
  match_cont f cenv k tk m bound tbound ->
  Mem.unchanged_on (loc_unmapped f) m m' ->
  inject_incr f f' ->
  inject_separated f f' m tm ->
  Ple bound (Mem.nextblock m) -> Ple tbound (Mem.nextblock tm) ->
  match_cont f' cenv k tk m' bound tbound.
Proof.
  intros. eapply match_cont_invariant; eauto.
  intros. eapply Mem.load_unchanged_on; eauto.
  red in H2. intros. destruct (f b) as [[b' delta] | ] eqn:?. auto.
  destruct (f' b) as [[b' delta] | ] eqn:?; auto.
  exploit H2; eauto. unfold Mem.valid_block. intros [A B]. extlia.
  red in H2. intros. destruct (f b) as [[b'' delta''] | ] eqn:?. auto.
  exploit H2; eauto. unfold Mem.valid_block. intros [A B]. extlia.
Qed.

(** Invariance by change of bounds *)

Lemma match_cont_incr_bounds:
  forall f cenv k tk m bound tbound,
  match_cont f cenv k tk m bound tbound ->
  forall bound' tbound',
  Ple bound bound' -> Ple tbound tbound' ->
  match_cont f cenv k tk m bound' tbound'.
Proof.
  induction 1; intros; econstructor; eauto; extlia.
Qed.

(** [match_cont] and call continuations. *)

Lemma match_cont_change_cenv:
  forall f cenv k tk m bound tbound cenv',
  match_cont f cenv k tk m bound tbound ->
  is_call_cont k ->
  match_cont f cenv' k tk m bound tbound.
Proof.
  intros. inv H; simpl in H0; try contradiction; econstructor; eauto.
Qed.

Lemma match_cont_is_call_cont:
  forall f cenv k tk m bound tbound,
  match_cont f cenv k tk m bound tbound ->
  is_call_cont k ->
  is_call_cont tk.
Proof.
  intros. inv H; auto.
Qed.

Lemma match_cont_call_cont:
  forall f cenv k tk m bound tbound,
  match_cont f cenv k tk m bound tbound ->
  forall cenv',
  match_cont f cenv' (call_cont k) (call_cont tk) m bound tbound.
Proof.
  induction 1; simpl; auto; intros; econstructor; eauto.
Qed.

(** [match_cont] and freeing of environment blocks *)

Remark free_list_nextblock:
  forall l m m',
  Mem.free_list m l = Some m' -> Mem.nextblock m' = Mem.nextblock m.
Proof.
  induction l; simpl; intros.
  congruence.
  destruct a. destruct p. destruct (Mem.free m b z0 z) as [m1|] eqn:?; try discriminate.
  transitivity (Mem.nextblock m1). eauto. eapply Mem.nextblock_free; eauto.
Qed.

Remark free_list_load:
  forall chunk b' l m m',
  Mem.free_list m l = Some m' ->
  (forall b lo hi, In (b, lo, hi) l -> Plt b' b) ->
  Mem.load chunk m' b' 0 = Mem.load chunk m b' 0.
Proof.
  induction l; simpl; intros.
  inv H; auto.
  destruct a. destruct p. destruct (Mem.free m b z0 z) as [m1|] eqn:?; try discriminate.
  transitivity (Mem.load chunk m1 b' 0). eauto.
  eapply Mem.load_free. eauto. left. assert (Plt b' b) by eauto. unfold block; extlia.
Qed.

Lemma match_cont_free_env:
  forall f cenv e le m lo hi te tle tm tlo thi k tk m' tm',
  match_envs f cenv e le m lo hi te tle tlo thi ->
  match_cont f cenv k tk m lo tlo ->
  Ple hi (Mem.nextblock m) ->
  Ple thi (Mem.nextblock tm) ->
  Mem.free_list m (blocks_of_env ge e) = Some m' ->
  Mem.free_list tm (blocks_of_env tge te) = Some tm' ->
  match_cont f cenv k tk m' (Mem.nextblock m') (Mem.nextblock tm').
Proof.
  intros. apply match_cont_incr_bounds with lo tlo.
  eapply match_cont_invariant; eauto.
  intros. rewrite <- H7. eapply free_list_load; eauto.
  unfold blocks_of_env; intros. exploit list_in_map_inv; eauto.
  intros [[id [b1 ty]] [P Q]]. simpl in P. inv P.
  exploit me_range; eauto. eapply PTree.elements_complete; eauto. extlia.
  rewrite (free_list_nextblock _ _ _ H3). inv H; extlia.
  rewrite (free_list_nextblock _ _ _ H4). inv H; extlia.
Qed.

(** Matching of global environments *)

Lemma match_cont_globalenv:
  forall f cenv k tk m bound tbound,
  match_cont f cenv k tk m bound tbound ->
  exists bound, match_globalenvs f bound.
Proof.
  induction 1; auto. exists hi; auto.
Qed.

Hint Resolve match_cont_globalenv: compat.

Lemma match_cont_find_funct:
  forall f cenv k tk m bound tbound vf fd tvf,
  match_cont f cenv k tk m bound tbound ->
  Genv.find_funct ge vf = Some fd ->
  Val.inject f vf tvf ->
  exists tfd, Genv.find_funct tge tvf = Some tfd /\ transf_fundef fd = OK tfd.
Proof.
  intros. exploit match_cont_globalenv; eauto. intros [bound1 MG]. destruct MG.
  inv H1; simpl in H0; try discriminate. destruct (Ptrofs.eq_dec ofs1 Ptrofs.zero); try discriminate.
  subst ofs1.
  assert (f b1 = Some(b1, 0)).
    apply DOMAIN. eapply FUNCTIONS; eauto.
  rewrite H1 in H2; inv H2.
  rewrite Ptrofs.add_zero. simpl. rewrite dec_eq_true. apply function_ptr_translated; auto.
Qed.

(** Relating execution states *)

Inductive match_states: state -> state -> Prop :=
  | match_regular_states:
      forall f s k e le m tf ts tk te tle tm j lo hi tlo thi
        (TRF: transf_function f = OK tf)
        (TRS: simpl_stmt (cenv_for f) s = OK ts)
        (MENV: match_envs j (cenv_for f) e le m lo hi te tle tlo thi)
        (MCONT: match_cont j (cenv_for f) k tk m lo tlo)
        (MINJ: Mem.inject j m tm)
        (COMPAT: compat_cenv (addr_taken_stmt s) (cenv_for f))
        (BOUND: Ple hi (Mem.nextblock m))
        (TBOUND: Ple thi (Mem.nextblock tm)),
      match_states (State f s k e le m)
                   (State tf ts tk te tle tm)
  | match_call_state:
      forall fd vargs k m tfd tvargs tk tm j targs tres cconv
        (TRFD: transf_fundef fd = OK tfd)
        (MCONT: forall cenv, match_cont j cenv k tk m (Mem.nextblock m) (Mem.nextblock tm))
        (MINJ: Mem.inject j m tm)
        (AINJ: Val.inject_list j vargs tvargs)
        (FUNTY: type_of_fundef fd = Tfunction targs tres cconv)
        (ANORM: val_casted_list vargs targs),
      match_states (Callstate fd vargs k m)
                   (Callstate tfd tvargs tk tm)
  | match_return_state:
      forall v k m tv tk tm j
        (MCONT: forall cenv, match_cont j cenv k tk m (Mem.nextblock m) (Mem.nextblock tm))
        (MINJ: Mem.inject j m tm)
        (RINJ: Val.inject j v tv),
      match_states (Returnstate v k m)
                   (Returnstate tv tk tm).

(** The simulation diagrams *)

Remark is_liftable_var_charact:
  forall cenv a,
  match is_liftable_var cenv a with
  | Some id => exists ty, a = Evar id ty /\ VSet.mem id cenv = true
  | None => match a with Evar id ty => VSet.mem id cenv = false | _ => True end
  end.
Proof.
  intros. destruct a; simpl; auto.
  destruct (VSet.mem i cenv) eqn:?.
  exists t; auto.
  auto.
Qed.

Remark simpl_select_switch:
  forall cenv n ls tls,
  simpl_lblstmt cenv ls = OK tls ->
  simpl_lblstmt cenv (select_switch n ls) = OK (select_switch n tls).
Proof.
  intros cenv n.
  assert (DFL:
    forall ls tls,
    simpl_lblstmt cenv ls = OK tls ->
    simpl_lblstmt cenv (select_switch_default ls) = OK (select_switch_default tls)).
  {
    induction ls; simpl; intros; monadInv H.
    auto.
    simpl. destruct o. eauto. simpl; rewrite EQ, EQ1. auto.
  }
  assert (CASE:
    forall ls tls,
    simpl_lblstmt cenv ls = OK tls ->
    match select_switch_case n ls with
    | None => select_switch_case n tls = None
    | Some ls' =>
        exists tls', select_switch_case n tls = Some tls' /\ simpl_lblstmt cenv ls' = OK tls'
    end).
  {
    induction ls; simpl; intros; monadInv H; simpl.
    auto.
    destruct o.
    destruct (zeq z n).
    econstructor; split; eauto. simpl; rewrite EQ, EQ1; auto.
    apply IHls. auto.
    apply IHls. auto.
  }
  intros; unfold select_switch.
  specialize (CASE _ _ H). destruct (select_switch_case n ls) as [ls'|].
  destruct CASE as [tls' [P Q]]. rewrite P, Q. auto.
  rewrite CASE. apply DFL; auto.
Qed.

Remark simpl_seq_of_labeled_statement:
  forall cenv ls tls,
  simpl_lblstmt cenv ls = OK tls ->
  simpl_stmt cenv (seq_of_labeled_statement ls) = OK (seq_of_labeled_statement tls).
Proof.
  induction ls; simpl; intros; monadInv H; simpl.
  auto.
  rewrite EQ; simpl. erewrite IHls; eauto. simpl. auto.
Qed.

Remark compat_cenv_select_switch:
  forall cenv n ls,
  compat_cenv (addr_taken_lblstmt ls) cenv ->
  compat_cenv (addr_taken_lblstmt (select_switch n ls)) cenv.
Proof.
  intros cenv n.
  assert (DFL: forall ls,
    compat_cenv (addr_taken_lblstmt ls) cenv ->
    compat_cenv (addr_taken_lblstmt (select_switch_default ls)) cenv).
  {
    induction ls; simpl; intros.
    eauto with compat.
    destruct o; simpl; eauto with compat.
  }
  assert (CASE: forall ls ls',
    compat_cenv (addr_taken_lblstmt ls) cenv ->
    select_switch_case n ls = Some ls' ->
    compat_cenv (addr_taken_lblstmt ls') cenv).
  {
    induction ls; simpl; intros.
    discriminate.
    destruct o. destruct (zeq z n). inv H0. auto. eauto with compat.
    eauto with compat.
  }
  intros. specialize (CASE ls). unfold select_switch.
  destruct (select_switch_case n ls) as [ls'|]; eauto.
Qed.

Remark addr_taken_seq_of_labeled_statement:
  forall ls, addr_taken_stmt (seq_of_labeled_statement ls) = addr_taken_lblstmt ls.
Proof.
  induction ls; simpl; congruence.
Qed.

Section FIND_LABEL.

Variable f: meminj.
Variable cenv: compilenv.
Variable m: mem.
Variables bound tbound: block.
Variable lbl: ident.

Lemma simpl_find_label:
  forall s k ts tk,
  simpl_stmt cenv s = OK ts ->
  match_cont f cenv k tk m bound tbound ->
  compat_cenv (addr_taken_stmt s) cenv ->
  match find_label lbl s k with
  | None =>
      find_label lbl ts tk = None
  | Some(s', k') =>
      exists ts', exists tk',
         find_label lbl ts tk = Some(ts', tk')
      /\ compat_cenv (addr_taken_stmt s') cenv
      /\ simpl_stmt cenv s' = OK ts'
      /\ match_cont f cenv k' tk' m bound tbound
  end

with simpl_find_label_ls:
  forall ls k tls tk,
  simpl_lblstmt cenv ls = OK tls ->
  match_cont f cenv k tk m bound tbound ->
  compat_cenv (addr_taken_lblstmt ls) cenv ->
  match find_label_ls lbl ls k with
  | None =>
      find_label_ls lbl tls tk = None
  | Some(s', k') =>
      exists ts', exists tk',
         find_label_ls lbl tls tk = Some(ts', tk')
      /\ compat_cenv (addr_taken_stmt s') cenv
      /\ simpl_stmt cenv s' = OK ts'
      /\ match_cont f cenv k' tk' m bound tbound
  end.

Proof.
  induction s; simpl; intros until tk; intros TS MC COMPAT; auto.
  (* skip *)
  monadInv TS; auto.
  (* var *)
  destruct (is_liftable_var cenv e); monadInv TS; auto.
  unfold Sset_debug. destruct (Compopts.debug tt); auto.
  (* set *)
  monadInv TS; auto.
  (* call *)
  monadInv TS; auto.
  (* builtin *)
  monadInv TS; auto.
  (* seq *)
  monadInv TS.
  exploit (IHs1 (Kseq s2 k) x (Kseq x0 tk)); eauto with compat.
    constructor; eauto with compat.
  destruct (find_label lbl s1 (Kseq s2 k)) as [[s' k']|].
  intros [ts' [tk' [P [Q [R S]]]]]. exists ts'; exists tk'. simpl. rewrite P. auto.
  intros E. simpl. rewrite E. eapply IHs2; eauto with compat.
  (* ifthenelse *)
  monadInv TS.
  exploit (IHs1 k x tk); eauto with compat.
  destruct (find_label lbl s1 k) as [[s' k']|].
  intros [ts' [tk' [P [Q [R S]]]]]. exists ts'; exists tk'. simpl. rewrite P. auto.
  intros E. simpl. rewrite E. eapply IHs2; eauto with compat.
  (* loop *)
  monadInv TS.
  exploit (IHs1 (Kloop1 s1 s2 k) x (Kloop1 x x0 tk)); eauto with compat.
    constructor; eauto with compat.
  destruct (find_label lbl s1 (Kloop1 s1 s2 k)) as [[s' k']|].
  intros [ts' [tk' [P [Q [R S]]]]]. exists ts'; exists tk'. simpl; rewrite P. auto.
  intros E. simpl; rewrite E. eapply IHs2; eauto with compat. econstructor; eauto with compat.
  (* break *)
  monadInv TS; auto.
  (* continue *)
  monadInv TS; auto.
  (* return *)
  monadInv TS; auto.
  (* switch *)
  monadInv TS. simpl.
  eapply simpl_find_label_ls; eauto with compat. constructor; auto.
  (* label *)
  monadInv TS. simpl.
  destruct (ident_eq lbl l).
  exists x; exists tk; auto.
  eapply IHs; eauto.
  (* goto *)
  monadInv TS; auto.

  induction ls; simpl; intros.
  (* nil *)
  monadInv H. auto.
  (* cons *)
  monadInv H.
  exploit (simpl_find_label s (Kseq (seq_of_labeled_statement ls) k)).
    eauto. constructor. eapply simpl_seq_of_labeled_statement; eauto. eauto.
    rewrite addr_taken_seq_of_labeled_statement. eauto with compat.
    eauto with compat.
  destruct (find_label lbl s (Kseq (seq_of_labeled_statement ls) k)) as [[s' k']|].
  intros [ts' [tk' [P [Q [R S]]]]]. exists ts'; exists tk'; split. simpl; rewrite P. auto. auto.
  intros E. simpl; rewrite E. eapply IHls; eauto with compat.
Qed.

Lemma find_label_store_params:
  forall s k params, find_label lbl (store_params cenv params s) k = find_label lbl s k.
Proof.
  induction params; simpl. auto.
  destruct a as [id ty]. destruct (VSet.mem id cenv); [destruct Conventions1.parameter_needs_normalization|]; auto.
Qed.

Lemma find_label_add_debug_vars:
  forall s k vars, find_label lbl (add_debug_vars vars s) k = find_label lbl s k.
Proof.
  unfold add_debug_vars. destruct (Compopts.debug tt); auto.
  induction vars; simpl; auto. destruct a as [id ty]; simpl. auto.
Qed.

Lemma find_label_add_debug_params:
  forall s k vars, find_label lbl (add_debug_params vars s) k = find_label lbl s k.
Proof.
  unfold add_debug_params. destruct (Compopts.debug tt); auto.
  induction vars; simpl; auto. destruct a as [id ty]; simpl. auto.
Qed.

End FIND_LABEL.


Lemma step_simulation:
  forall S1 t S2, step1 ge S1 t S2 ->
  forall S1' (MS: match_states S1 S1'), exists S2', plus step2 tge S1' t S2' /\ match_states S2 S2'.
Proof.
  induction 1; simpl; intros; inv MS; simpl in *; try (monadInv TRS).

(* assign *)
  generalize (is_liftable_var_charact (cenv_for f) a1); destruct (is_liftable_var (cenv_for f) a1) as [id|]; monadInv TRS.
  (* liftable *)
  intros [ty [P Q]]; subst a1; simpl in *.
  exploit eval_simpl_expr; eauto with compat. intros [tv2 [A B]].
  exploit sem_cast_inject; eauto. intros [tv [C D]].
  exploit me_vars; eauto. instantiate (1 := id). intros MV.
  inv H.
  (* local variable *)
  econstructor; split.
  eapply step_Sset_debug. eauto. rewrite typeof_simpl_expr. eauto.
  econstructor; eauto with compat.
  eapply match_envs_assign_lifted; eauto. eapply cast_val_is_casted; eauto.
  eapply match_cont_assign_loc; eauto. exploit me_range; eauto. extlia.
  inv MV; try congruence. inv H2; try congruence. unfold Mem.storev in H3.
  eapply Mem.store_unmapped_inject; eauto. congruence.
  erewrite assign_loc_nextblock; eauto.
  (* global variable *)
  inv MV; congruence.
  (* not liftable *)
  intros P.
  exploit eval_simpl_lvalue; eauto with compat. intros [tb [tofs [E F]]].
  exploit eval_simpl_expr; eauto with compat. intros [tv2 [A B]].
  exploit sem_cast_inject; eauto. intros [tv [C D]].
  exploit assign_loc_inject; eauto. intros [tm' [X [Y Z]]].
  econstructor; split.
  apply plus_one. econstructor. eexact E. eexact A. repeat rewrite typeof_simpl_expr. eexact C.
  rewrite typeof_simpl_expr; auto. eexact X.
  econstructor; eauto with compat.
  eapply match_envs_invariant; eauto.
  eapply match_cont_invariant; eauto.
  erewrite assign_loc_nextblock; eauto.
  erewrite assign_loc_nextblock; eauto.

(* set temporary *)
  exploit eval_simpl_expr; eauto with compat. intros [tv [A B]].
  econstructor; split.
  apply plus_one. econstructor. eauto.
  econstructor; eauto with compat.
  eapply match_envs_set_temp; eauto.

(* call *)
  exploit eval_simpl_expr; eauto with compat. intros [tvf [A B]].
  exploit eval_simpl_exprlist; eauto with compat. intros [CASTED [tvargs [C D]]].
  exploit match_cont_find_funct; eauto. intros [tfd [P Q]].
  econstructor; split.
  apply plus_one. eapply step_call with (fd := tfd).
  rewrite typeof_simpl_expr. eauto.
  eauto. eauto. eauto.
  erewrite type_of_fundef_preserved; eauto.
  econstructor; eauto.
  intros. econstructor; eauto.

(* builtin *)
  exploit eval_simpl_exprlist; eauto with compat. intros [CASTED [tvargs [C D]]].
  exploit external_call_mem_inject; eauto. apply match_globalenvs_preserves_globals; eauto with compat.
  intros [j' [tvres [tm' [P [Q [R [S [T [U V]]]]]]]]].
  econstructor; split.
  apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
  econstructor; eauto with compat.
  eapply match_envs_set_opttemp; eauto.
  eapply match_envs_extcall; eauto.
  eapply match_cont_extcall; eauto.
  inv MENV; extlia. inv MENV; extlia.
  eapply Ple_trans; eauto. eapply external_call_nextblock; eauto.
  eapply Ple_trans; eauto. eapply external_call_nextblock; eauto.

(* sequence *)
  econstructor; split. apply plus_one. econstructor.
  econstructor; eauto with compat. econstructor; eauto with compat.

(* skip sequence *)
  inv MCONT. econstructor; split. apply plus_one. econstructor. econstructor; eauto.

(* continue sequence *)
  inv MCONT. econstructor; split. apply plus_one. econstructor. econstructor; eauto.

(* break sequence *)
  inv MCONT. econstructor; split. apply plus_one. econstructor. econstructor; eauto.

(* ifthenelse *)
  exploit eval_simpl_expr; eauto with compat. intros [tv [A B]].
  econstructor; split.
  apply plus_one. apply step_ifthenelse with (v1 := tv) (b := b). auto.
  rewrite typeof_simpl_expr. eapply bool_val_inject; eauto.
  destruct b; econstructor; eauto with compat.

(* loop *)
  econstructor; split. apply plus_one. econstructor. econstructor; eauto with compat. econstructor; eauto with compat.

(* skip-or-continue loop *)
  inv MCONT. econstructor; split.
  apply plus_one. econstructor. destruct H; subst x; simpl in *; intuition congruence.
  econstructor; eauto with compat. econstructor; eauto with compat.

(* break loop1 *)
  inv MCONT. econstructor; split. apply plus_one. eapply step_break_loop1.
  econstructor; eauto.

(* skip loop2 *)
  inv MCONT. econstructor; split. apply plus_one. eapply step_skip_loop2.
  econstructor; eauto with compat. simpl; rewrite H2; rewrite H4; auto.

(* break loop2 *)
  inv MCONT. econstructor; split. apply plus_one. eapply step_break_loop2.
  econstructor; eauto.

(* return none *)
  exploit match_envs_free_blocks; eauto. intros [tm' [P Q]].
  econstructor; split. apply plus_one. econstructor; eauto.
  econstructor; eauto.
  intros. eapply match_cont_call_cont. eapply match_cont_free_env; eauto.

(* return some *)
  exploit eval_simpl_expr; eauto with compat. intros [tv [A B]].
  exploit sem_cast_inject; eauto. intros [tv' [C D]].
  exploit match_envs_free_blocks; eauto. intros [tm' [P Q]].
  econstructor; split. apply plus_one. econstructor; eauto.
  rewrite typeof_simpl_expr. monadInv TRF; simpl. eauto.
  econstructor; eauto.
  intros. eapply match_cont_call_cont. eapply match_cont_free_env; eauto.

(* skip call *)
  exploit match_envs_free_blocks; eauto. intros [tm' [P Q]].
  econstructor; split. apply plus_one. econstructor; eauto.
  eapply match_cont_is_call_cont; eauto.
  monadInv TRF; auto.
  econstructor; eauto.
  intros. apply match_cont_change_cenv with (cenv_for f); auto. eapply match_cont_free_env; eauto.

(* switch *)
  exploit eval_simpl_expr; eauto with compat. intros [tv [A B]].
  econstructor; split. apply plus_one. econstructor; eauto.
  rewrite typeof_simpl_expr. instantiate (1 := n).
  unfold sem_switch_arg in *;
  destruct (classify_switch (typeof a)); try discriminate;
  inv B; inv H0; auto.
  econstructor; eauto.
  erewrite simpl_seq_of_labeled_statement. reflexivity.
  eapply simpl_select_switch; eauto.
  econstructor; eauto. rewrite addr_taken_seq_of_labeled_statement.
  apply compat_cenv_select_switch. eauto with compat.

(* skip-break switch *)
  inv MCONT. econstructor; split.
  apply plus_one. eapply step_skip_break_switch. destruct H; subst x; simpl in *; intuition congruence.
  econstructor; eauto with compat.

(* continue switch *)
  inv MCONT. econstructor; split.
  apply plus_one. eapply step_continue_switch.
  econstructor; eauto with compat.

(* label *)
  econstructor; split. apply plus_one. econstructor. econstructor; eauto.

(* goto *)
  generalize TRF; intros TRF'. monadInv TRF'.
  exploit (simpl_find_label j (cenv_for f) m lo tlo lbl (fn_body f) (call_cont k) x (call_cont tk)).
    eauto. eapply match_cont_call_cont. eauto.
    apply compat_cenv_for.
  rewrite H. intros [ts' [tk' [A [B [C D]]]]].
  econstructor; split.
  apply plus_one. econstructor; eauto. simpl.
  rewrite find_label_add_debug_params. rewrite find_label_store_params. rewrite find_label_add_debug_vars. eexact A.
  econstructor; eauto.

(* internal function *)
  monadInv TRFD. inv H.
  generalize EQ; intro EQ'; monadInv EQ'.
  assert (list_norepet (var_names (fn_params f ++ fn_vars f))).
    unfold var_names. rewrite map_app. auto.
  exploit match_envs_alloc_variables; eauto.
    instantiate (1 := cenv_for_gen (addr_taken_stmt f.(fn_body)) (fn_params f ++ fn_vars f)).
    intros. eapply cenv_for_gen_by_value; eauto. rewrite VSF.mem_iff. eexact H4.
    intros. eapply cenv_for_gen_domain. rewrite VSF.mem_iff. eexact H3.
  intros [j' [te [tm0 [A [B [C [D [E [F G]]]]]]]]].
  assert (K: list_forall2 val_casted vargs (map snd (fn_params f))).
  { apply val_casted_list_params. unfold type_of_function in FUNTY. congruence. }
  exploit store_params_correct.
    eauto.
    eapply list_norepet_append_left; eauto.
    eexact K.
    apply val_inject_list_incr with j'; eauto.
    eexact B. eexact C.
    intros. apply (create_undef_temps_lifted id f). auto.
    intros. destruct (create_undef_temps (fn_temps f))!id as [v|] eqn:?; auto.
    exploit create_undef_temps_inv; eauto. intros [P Q]. elim (l id id); auto.
  intros [tel [tm1 [P [Q [R [S T]]]]]].
  change (cenv_for_gen (addr_taken_stmt (fn_body f)) (fn_params f ++ fn_vars f))
    with (cenv_for f) in *.
  generalize (vars_and_temps_properties (cenv_for f) (fn_params f) (fn_vars f) (fn_temps f)).
  intros [X [Y Z]]. auto. auto.
  econstructor; split.
  eapply plus_left. econstructor.
  econstructor. exact Y. exact X. exact Z. simpl. eexact A. simpl. eexact Q.
  simpl. eapply star_trans. eapply step_add_debug_params. auto. eapply forall2_val_casted_inject; eauto. eexact Q.
  eapply star_trans. eexact P. eapply step_add_debug_vars.
  unfold remove_lifted; intros. rewrite List.filter_In in H3. destruct H3.
  apply negb_true_iff in H4. eauto.
  reflexivity. reflexivity. traceEq.
  econstructor; eauto.
  eapply match_cont_invariant; eauto.
  intros. transitivity (Mem.load chunk m0 b 0).
  eapply bind_parameters_load; eauto. intros.
  exploit alloc_variables_range. eexact H1. eauto.
  unfold empty_env. rewrite PTree.gempty. intros [?|?]. congruence.
  red; intros; subst b'. extlia.
  eapply alloc_variables_load; eauto.
  apply compat_cenv_for.
  rewrite (bind_parameters_nextblock _ _ _ _ _ _ H2). extlia.
  rewrite T; extlia.

(* external function *)
  monadInv TRFD. inv FUNTY.
  exploit external_call_mem_inject; eauto. apply match_globalenvs_preserves_globals.
  eapply match_cont_globalenv. eexact (MCONT VSet.empty).
  intros [j' [tvres [tm' [P [Q [R [S [T [U V]]]]]]]]].
  econstructor; split.
  apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
  econstructor; eauto.
  intros. apply match_cont_incr_bounds with (Mem.nextblock m) (Mem.nextblock tm).
  eapply match_cont_extcall; eauto. extlia. extlia.
  eapply external_call_nextblock; eauto.
  eapply external_call_nextblock; eauto.

(* return *)
  specialize (MCONT (cenv_for f)). inv MCONT.
  econstructor; split.
  apply plus_one. econstructor.
  econstructor; eauto with compat.
  eapply match_envs_set_opttemp; eauto.
Qed.

Lemma initial_states_simulation:
  forall S, initial_state prog S ->
  exists R, initial_state tprog R /\ match_states S R.
Proof.
  intros. inv H.
  exploit function_ptr_translated; eauto. intros [tf [A B]].
  econstructor; split.
  econstructor.
  eapply (Genv.init_mem_transf_partial (proj1 TRANSF)). eauto.
  replace (prog_main tprog) with (prog_main prog). 
  instantiate (1 := b). rewrite <- H1. apply symbols_preserved.
  generalize (match_program_main (proj1 TRANSF)). simpl; auto.
  eauto.
  rewrite <- H3; apply type_of_fundef_preserved; auto.
  econstructor; eauto.
  intros. instantiate (1 := Mem.flat_inj (Mem.nextblock m0)).
  econstructor. instantiate (1 := Mem.nextblock m0).
  constructor; intros.
  unfold Mem.flat_inj. apply pred_dec_true; auto.
  unfold Mem.flat_inj in H. destruct (plt b1 (Mem.nextblock m0)); inv H. auto.
  eapply Genv.find_symbol_not_fresh; eauto.
  eapply Genv.find_funct_ptr_not_fresh; eauto.
  eapply Genv.find_var_info_not_fresh; eauto.
  extlia. extlia.
  eapply Genv.initmem_inject; eauto.
  constructor.
Qed.

Lemma final_states_simulation:
  forall S R r,
  match_states S R -> final_state S r -> final_state R r.
Proof.
  intros. inv H0. inv H.
  specialize (MCONT VSet.empty). inv MCONT.
  inv RINJ. constructor.
Qed.

Theorem transf_program_correct:
  forward_simulation (semantics1 prog) (semantics2 tprog).
Proof.
  eapply forward_simulation_plus.
  apply senv_preserved.
  eexact initial_states_simulation.
  eexact final_states_simulation.
  eexact step_simulation.
Qed.

End PRESERVATION.

(** ** Commutation with linking *)

Global Instance TransfSimplLocalsLink : TransfLink match_prog.
Proof.
  red; intros. eapply Ctypes.link_match_program; eauto. 
- intros.
Local Transparent Linker_fundef.
  simpl in *; unfold link_fundef in *.
  destruct f1; monadInv H3; destruct f2; monadInv H4; try discriminate.
  destruct e; inv H2. exists (Internal x); split; auto. simpl; rewrite EQ; auto.
  destruct e; inv H2. exists (Internal x); split; auto. simpl; rewrite EQ; auto.
  destruct (external_function_eq e e0 && typelist_eq t t1 &&
            type_eq t0 t2 && calling_convention_eq c c0); inv H2.
  econstructor; split; eauto. 
Qed.