(* *********************************************************************)
(*                                                                     *)
(*              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.     *)
(*                                                                     *)
(* *********************************************************************)

(** Correctness of instruction selection *)

Require Import FunInd.
Require Import Coqlib Maps.
Require Import AST Linking Errors Integers Values Memory Events Globalenvs Smallstep.
Require Import Switch Cminor Op CminorSel.
Require Import SelectOp SelectDiv SplitLong SelectLong Selection.
Require Import SelectOpproof SelectDivproof SplitLongproof SelectLongproof.

Local Open Scope cminorsel_scope.
Local Open Scope error_monad_scope.

(** * Relational specification of instruction selection *)

Definition match_fundef (cunit: Cminor.program) (f: Cminor.fundef) (tf: CminorSel.fundef) : Prop :=
  exists hf, helper_functions_declared cunit hf /\ sel_fundef (prog_defmap cunit) hf f = OK tf.

Definition match_prog (p: Cminor.program) (tp: CminorSel.program) :=
  match_program match_fundef eq p tp.

(** Processing of helper functions *)

Lemma record_globdefs_sound:
  forall dm id gd, (record_globdefs dm)!id = Some gd -> dm!id = Some gd.
Proof.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  intros.
(* Goal: @eq (option globdef) (@PTree.get globdef id dm) (@Some globdef gd) *)
  set (f := fun m id gd => if globdef_of_interest gd then PTree.set id gd m else m) in *.
(* Goal: @eq (option globdef) (@PTree.get globdef id dm) (@Some globdef gd) *)
  set (P := fun m m' => m'!id = Some gd -> m!id = Some gd).
(* Goal: @eq (option globdef) (@PTree.get globdef id dm) (@Some globdef gd) *)
  assert (X: P dm (PTree.fold f dm (PTree.empty _))).
(* Goal: forall (id : ident) (name : string) (sg : signature) (_ : @helper_declared Cminor.function unit prog id name sg), @helper_declared function unit tprog id name sg *)
(* Goal: forall (hf : helper_functions) (_ : @helper_functions_declared Cminor.function unit prog hf), @helper_functions_declared function unit tprog hf *)
  { apply PTree_Properties.fold_rec.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  - unfold P; intros. rewrite <- H0; auto.
  - red. rewrite ! PTree.gempty. auto.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  - unfold P; intros. rewrite PTree.gsspec. unfold f in H3.
(* Goal: @eq (option globdef) (if peq id k then @Some globdef v else @PTree.get globdef id m) (@Some globdef gd) *)
    destruct (globdef_of_interest v).
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
    + rewrite PTree.gsspec in H3. destruct (peq id k); auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
    + apply H2 in H3. destruct (peq id k). congruence. auto. }
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply X. auto.
Qed.

Lemma lookup_helper_correct_1:
  forall globs name sg id,
  lookup_helper globs name sg = OK id ->
  globs!id = Some (Gfun (External (EF_runtime name sg))).
Proof.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  intros.
  set (P := fun (m: PTree.t globdef) res => res = Some id -> m!id = Some(Gfun(External (EF_runtime name sg)))).
(* Goal: @eq (option globdef) (@PTree.get globdef id globs) (@Some (AST.globdef (AST.fundef Cminor.function) unit) (@Gfun (AST.fundef Cminor.function) unit (@External Cminor.function (EF_runtime name sg)))) *)
  assert (P globs (PTree.fold (lookup_helper_aux name sg) globs None)).
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  { apply PTree_Properties.fold_rec; red; intros.
  - rewrite <- H0. apply H1; auto.
  - discriminate.
  - assert (EITHER: k = id /\ v = Gfun (External (EF_runtime name sg))
                \/  a = Some id).
(* Goal: forall (id : ident) (name : string) (sg : signature) (_ : @helper_declared Cminor.function unit prog id name sg), @helper_declared function unit tprog id name sg *)
(* Goal: forall (hf : helper_functions) (_ : @helper_functions_declared Cminor.function unit prog hf), @helper_functions_declared function unit tprog hf *)
    { unfold lookup_helper_aux in H3. destruct v; auto. destruct f; auto. destruct e; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
      destruct (String.string_dec name name0); auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
      destruct (signature_eq sg sg0); auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
      inversion H3. left; split; auto. repeat f_equal; auto. }
(* Goal: @eq (option globdef) (@PTree.get globdef id (@PTree.set globdef k v m)) (@Some (AST.globdef (AST.fundef Cminor.function) unit) (@Gfun (AST.fundef Cminor.function) unit (@External Cminor.function (EF_runtime name sg)))) *)
    destruct EITHER as [[X Y] | X].
(* Goal: @eq (option globdef) (@PTree.get globdef id (@PTree.set globdef k v m)) (@Some (AST.globdef (AST.fundef Cminor.function) unit) (@Gfun (AST.fundef Cminor.function) unit (@External Cminor.function (EF_runtime name sg)))) *)
(* Goal: @eq (option globdef) (@PTree.get globdef id (@PTree.set globdef k v m)) (@Some (AST.globdef (AST.fundef Cminor.function) unit) (@Gfun (AST.fundef Cminor.function) unit (@External Cminor.function (EF_runtime name sg)))) *)
    subst k v. apply PTree.gss.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
    apply H2 in X. rewrite PTree.gso by congruence. auto.
  }
(* Goal: @eq (option globdef) (@PTree.get globdef id globs) (@Some (AST.globdef (AST.fundef Cminor.function) unit) (@Gfun (AST.fundef Cminor.function) unit (@External Cminor.function (EF_runtime name sg)))) *)
  red in H0. unfold lookup_helper in H.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  destruct (PTree.fold (lookup_helper_aux name sg) globs None); inv H. auto.
Qed.

Lemma lookup_helper_correct:
  forall p name sg id,
  lookup_helper (record_globdefs (prog_defmap p)) name sg = OK id ->
  helper_declared p id name sg.
Proof.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  intros. apply lookup_helper_correct_1 in H. apply record_globdefs_sound in H. auto.
Qed.

Lemma get_helpers_correct:
  forall p hf,
  get_helpers (prog_defmap p) = OK hf -> helper_functions_declared p hf.
Proof.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  intros. monadInv H. red; simpl. auto 20 using lookup_helper_correct.
Qed.

Theorem transf_program_match:
  forall p tp, sel_program p = OK tp -> match_prog p tp.
Proof.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  intros. monadInv H.
  eapply match_transform_partial_program_contextual. eexact EQ0.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  intros. exists x; split; auto. apply get_helpers_correct; auto.
Qed.

Lemma helper_functions_declared_linkorder:
  forall (p p': Cminor.program) hf,
  helper_functions_declared p hf -> linkorder p p' -> helper_functions_declared p' hf.
Proof.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  intros.
  assert (X: forall id name sg, helper_declared p id name sg -> helper_declared p' id name sg).
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  { unfold helper_declared; intros.
(* Goal: @eq (option (AST.globdef (AST.fundef Cminor.function) unit)) (@PTree.get (AST.globdef (AST.fundef Cminor.function) unit) id (@prog_defmap (AST.fundef Cminor.function) unit p')) (@Some (AST.globdef (AST.fundef Cminor.function) unit) (@Gfun (AST.fundef Cminor.function) unit (@External Cminor.function (EF_runtime name sg)))) *)
    destruct (prog_defmap_linkorder _ _ _ _ H0 H1) as (gd & P & Q).
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
    inv Q. inv H3. auto. }
(* Goal: @helper_functions_declared Cminor.function unit p' hf *)
  red in H. decompose [Logic.and] H; clear H. red; auto 20.
Qed.

(** * Correctness of the instruction selection functions for expressions *)

Section PRESERVATION.

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

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

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

Lemma function_ptr_translated:
  forall (b: block) (f: Cminor.fundef),
  Genv.find_funct_ptr ge b = Some f ->
  exists cu tf, Genv.find_funct_ptr tge b = Some tf /\ match_fundef cu f tf /\ linkorder cu prog.
Proof (Genv.find_funct_ptr_match TRANSF).

Lemma functions_translated:
  forall (v v': val) (f: Cminor.fundef),
  Genv.find_funct ge v = Some f ->
  Val.lessdef v v' ->
  exists cu tf, Genv.find_funct tge v' = Some tf /\ match_fundef cu f tf /\ linkorder cu prog.
Proof.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  intros. inv H0.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply Genv.find_funct_match; eauto.
(* Goal: @eq Cminor.fundef fd (@External Cminor.function (EF_external id0 sg)) *)
  discriminate.
Qed.

Lemma sig_function_translated:
  forall cu f tf, match_fundef cu f tf -> funsig tf = Cminor.funsig f.
Proof.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  intros. destruct H as (hf & P & Q). destruct f; monadInv Q; auto. monadInv EQ; auto.
Qed.

Lemma stackspace_function_translated:
  forall dm hf f tf, sel_function dm hf f = OK tf -> fn_stackspace tf = Cminor.fn_stackspace f.
Proof.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  intros. monadInv H. auto.
Qed.

Lemma helper_functions_preserved:
  forall hf, helper_functions_declared prog hf -> helper_functions_declared tprog hf.
Proof.
  assert (X: forall id name sg, helper_declared prog id name sg -> helper_declared tprog id name sg).
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  { unfold helper_declared; intros.
(* Goal: @eq (option (AST.globdef (AST.fundef function) unit)) (@PTree.get (AST.globdef (AST.fundef function) unit) id (@prog_defmap (AST.fundef function) unit tprog)) (@Some (AST.globdef (AST.fundef function) unit) (@Gfun (AST.fundef function) unit (@External function (EF_runtime name sg)))) *)
    generalize (match_program_defmap _ _ _ _ _ TRANSF id).
(* Goal: forall _ : @option_rel (AST.globdef Cminor.fundef unit) (AST.globdef fundef unit) (@match_globdef (AST.program Cminor.fundef unit) Cminor.fundef unit fundef unit (@Linker_prog Cminor.fundef unit (Linker_fundef Cminor.function) Linker_unit) match_fundef (@eq unit) prog) (@PTree.get (AST.globdef Cminor.fundef unit) id (@prog_defmap Cminor.fundef unit prog)) (@PTree.get (AST.globdef fundef unit) id (@prog_defmap fundef unit tprog)), @eq (option (AST.globdef (AST.fundef function) unit)) (@PTree.get (AST.globdef (AST.fundef function) unit) id (@prog_defmap (AST.fundef function) unit tprog)) (@Some (AST.globdef (AST.fundef function) unit) (@Gfun (AST.fundef function) unit (@External function (EF_runtime name sg)))) *)
    unfold Cminor.fundef; rewrite H; intros R; inv R. inv H2.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
    destruct H4 as (cu & A & B). monadInv B. auto. }
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  unfold helper_functions_declared; intros. decompose [Logic.and] H; clear H. auto 20.
Qed.

Section CMCONSTR.

Variable cunit: Cminor.program.
Variable hf: helper_functions.
Hypothesis LINK: linkorder cunit prog.
Hypothesis HF: helper_functions_declared cunit hf.

Let HF': helper_functions_declared tprog hf.
Proof.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply helper_functions_preserved. eapply helper_functions_declared_linkorder; eauto.
Qed.

Variable sp: val.
Variable e: env.
Variable m: mem.

Lemma eval_condexpr_of_expr:
  forall a le v b,
  eval_expr tge sp e m le a v ->
  Val.bool_of_val v b ->
  eval_condexpr tge sp e m le (condexpr_of_expr a) b.
Proof.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  intros until a. functional induction (condexpr_of_expr a); intros.
(* compare *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  inv H. econstructor; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  simpl in H6. inv H6. apply Val.bool_of_val_of_optbool. auto.
(* condition *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  inv H. econstructor; eauto. destruct va; eauto.
(* let *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  inv H. econstructor; eauto.
(* default *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor. constructor. eauto. constructor.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  simpl. inv H0. auto.
Qed.

Lemma eval_load:
  forall le a v chunk v',
  eval_expr tge sp e m le a v ->
  Mem.loadv chunk m v = Some v' ->
  eval_expr tge sp e m le (load chunk a) v'.
Proof.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  intros. generalize H0; destruct v; simpl; intro; try discriminate.
(* Goal: eval_expr tge sp e m le (load chunk a) v' *)
  unfold load.
(* Goal: step tge (State f (let (mode, args) := addressing chunk a1 in Sstore chunk mode args a2) k sp e m) E0 (State f Sskip k sp e m') *)
  generalize (eval_addressing _ _ _ _ _ chunk _ _ _ _ H (eq_refl _)).
(* Goal: forall _ : let (mode, args) := addressing chunk a in @ex (list val) (fun vl : list val => Logic.and (eval_exprlist tge sp e m le args vl) (@eq (option val) (@Op.eval_addressing fundef unit tge sp mode vl) (@Some val (Vptr b i)))), eval_expr tge sp e m le (let (mode, args) := addressing chunk a in Eload chunk mode args) v' *)
  destruct (addressing chunk a). intros [vl [EV EQ]].
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_Eload; eauto.
Qed.

Lemma eval_store:
  forall chunk a1 a2 v1 v2 f k m',
  eval_expr tge sp e m nil a1 v1 ->
  eval_expr tge sp e m nil a2 v2 ->
  Mem.storev chunk m v1 v2 = Some m' ->
  step tge (State f (store chunk a1 a2) k sp e m)
        E0 (State f Sskip k sp e m').
Proof.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  intros. generalize H1; destruct v1; simpl; intro; try discriminate.
(* Goal: step tge (State f (store chunk a1 a2) k sp e m) E0 (State f Sskip k sp e m') *)
  unfold store.
(* Goal: step tge (State f (let (mode, args) := addressing chunk a1 in Sstore chunk mode args a2) k sp e m) E0 (State f Sskip k sp e m') *)
  generalize (eval_addressing _ _ _ _ _ chunk _ _ _ _ H (eq_refl _)).
(* Goal: forall _ : @ex (list val) (fun vl : list val => Logic.and (eval_exprlist tge sp e m (@nil val) e0 vl) (@eq (option val) (@Op.eval_addressing fundef unit tge sp a vl) (@Some val (Vptr b i)))), step tge (State f (Sstore chunk a e0 a2) k sp e m) E0 (State f Sskip k sp e m') *)
  destruct (addressing chunk a1). intros [vl [EV EQ]].
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply step_store; eauto.
Qed.

(** Correctness of instruction selection for operators *)

Lemma eval_sel_unop:
  forall le op a1 v1 v,
  eval_expr tge sp e m le a1 v1 ->
  eval_unop op v1 = Some v ->
  exists v', eval_expr tge sp e m le (sel_unop op a1) v' /\ Val.lessdef v v'.
Proof.
(* Goal: forall (le : letenv) (op : binary_operation) (a1 a2 : expr) (v1 v2 v : val) (_ : eval_expr tge sp e m le a1 v1) (_ : eval_expr tge sp e m le a2 v2) (_ : @eq (option val) (eval_binop op v1 v2 m) (@Some val v)), @ex val (fun v' : val => Logic.and (eval_expr tge sp e m le (@sel_binop hf op a1 a2) v') (Val.lessdef v v')) *)
  destruct op; simpl; intros; FuncInv; try subst v.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_cast8unsigned; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_cast8signed; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_cast16unsigned; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_cast16signed; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_negint; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_notint; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_negf; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_absf; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_negfs; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_absfs; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_singleoffloat; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_floatofsingle; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_intoffloat; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_intuoffloat; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_floatofint; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_floatofintu; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_intofsingle; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_intuofsingle; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_singleofint; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_singleofintu; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_negl; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_notl; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_intoflong; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_longofint; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_longofintu; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_longoffloat; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_longuoffloat; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_floatoflong; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_floatoflongu; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_longofsingle; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_longuofsingle; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_singleoflong; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_singleoflongu; eauto.
Qed.

Lemma eval_sel_binop:
  forall le op a1 a2 v1 v2 v,
  eval_expr tge sp e m le a1 v1 ->
  eval_expr tge sp e m le a2 v2 ->
  eval_binop op v1 v2 m = Some v ->
  exists v', eval_expr tge sp e m le (sel_binop op a1 a2) v' /\ Val.lessdef v v'.
Proof.
(* Goal: forall (le : letenv) (op : binary_operation) (a1 a2 : expr) (v1 v2 v : val) (_ : eval_expr tge sp e m le a1 v1) (_ : eval_expr tge sp e m le a2 v2) (_ : @eq (option val) (eval_binop op v1 v2 m) (@Some val v)), @ex val (fun v' : val => Logic.and (eval_expr tge sp e m le (@sel_binop hf op a1 a2) v') (Val.lessdef v v')) *)
  destruct op; simpl; intros; FuncInv; try subst v.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_add; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_sub; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_mul; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_divs; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_divu; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_mods; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_modu; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_and; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_or; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_xor; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_shl; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_shr; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_shru; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_addf; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_subf; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_mulf; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_divf; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_addfs; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_subfs; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_mulfs; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_divfs; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_addl; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_subl; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_mull; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_divls; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_divlu; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_modls; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_modlu; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_andl; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_orl; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_xorl; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_shll; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_shrl; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_shrlu; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_comp; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_compu; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_compf; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_compfs; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exists v; split; auto. eapply eval_cmpl; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exists v; split; auto. eapply eval_cmplu; eauto.
Qed.

End CMCONSTR.

(** Recognition of calls to built-in functions *)

Lemma expr_is_addrof_ident_correct:
  forall e id,
  expr_is_addrof_ident e = Some id ->
  e = Cminor.Econst (Cminor.Oaddrsymbol id Ptrofs.zero).
Proof.
(* Goal: forall (e : Cminor.expr) (id : ident) (_ : @eq (option ident) (expr_is_addrof_ident e) (@Some ident id)), @eq Cminor.expr e (Econst (Oaddrsymbol id Ptrofs.zero)) *)
  intros e id. unfold expr_is_addrof_ident.
(* Goal: @eq Cminor.fundef fd (@External Cminor.function ef) *)
  destruct e; try congruence.
(* Goal: @eq Cminor.fundef fd (@External Cminor.function ef) *)
  destruct c; try congruence.
(* Goal: @eq Cminor.fundef fd (@External Cminor.function ef) *)
  predSpec Ptrofs.eq Ptrofs.eq_spec i0 Ptrofs.zero; congruence.
Qed.

Lemma classify_call_correct:
  forall unit sp e m a v fd,
  linkorder unit prog ->
  Cminor.eval_expr ge sp e m a v ->
  Genv.find_funct ge v = Some fd ->
  match classify_call (prog_defmap unit) a with
  | Call_default => True
  | Call_imm id => exists b, Genv.find_symbol ge id = Some b /\ v = Vptr b Ptrofs.zero
  | Call_builtin ef => fd = External ef
  end.
Proof.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  unfold classify_call; intros.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  destruct (expr_is_addrof_ident a) as [id|] eqn:EA; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit expr_is_addrof_ident_correct; eauto. intros EQ; subst a.
(* Goal: match match @PTree.get globdef id (@prog_defmap Cminor.fundef Datatypes.unit unit) with | Some (Gfun (Internal f0 as f) as g) => Call_imm id | Some (Gfun (External ef as f) as g) => if ef_inline ef then Call_builtin ef else Call_imm id | Some (Gvar v as g) => Call_imm id | None => Call_imm id end with | Call_default => True | Call_imm id => @ex block (fun b : block => Logic.and (@eq (option block) (@Genv.find_symbol Cminor.fundef Datatypes.unit ge id) (@Some block b)) (@eq val v (Vptr b Ptrofs.zero))) | Call_builtin ef => @eq Cminor.fundef fd (@External Cminor.function ef) end *)
  inv H0. inv H3. unfold Genv.symbol_address in *.
(* Goal: @eq Cminor.fundef fd (@External Cminor.function (EF_external id0 sg)) *)
  destruct (Genv.find_symbol ge id) as [b|] eqn:FS; try discriminate.
(* Goal: match match @PTree.get globdef id (@prog_defmap Cminor.fundef Datatypes.unit unit) with | Some (Gfun (Internal f0 as f) as g) => Call_imm id | Some (Gfun (External ef as f) as g) => if ef_inline ef then Call_builtin ef else Call_imm id | Some (Gvar v as g) => Call_imm id | None => Call_imm id end with | Call_default => True | Call_imm id => @ex block (fun b0 : block => Logic.and (@eq (option block) (@Genv.find_symbol Cminor.fundef Datatypes.unit ge id) (@Some block b0)) (@eq val (Vptr b Ptrofs.zero) (Vptr b0 Ptrofs.zero))) | Call_builtin ef => @eq Cminor.fundef fd (@External Cminor.function ef) end *)
  rewrite Genv.find_funct_find_funct_ptr in H1.
(* Goal: match match @PTree.get globdef id (@prog_defmap Cminor.fundef Datatypes.unit unit) with | Some (Gfun (Internal f0 as f) as g) => Call_imm id | Some (Gfun (External ef as f) as g) => if ef_inline ef then Call_builtin ef else Call_imm id | Some (Gvar v as g) => Call_imm id | None => Call_imm id end with | Call_default => True | Call_imm id => @ex block (fun b0 : block => Logic.and (@eq (option block) (@Genv.find_symbol Cminor.fundef Datatypes.unit ge id) (@Some block b0)) (@eq val (Vptr b Ptrofs.zero) (Vptr b0 Ptrofs.zero))) | Call_builtin ef => @eq Cminor.fundef fd (@External Cminor.function ef) end *)
  assert (DFL: exists b1, Genv.find_symbol ge id = Some b1 /\ Vptr b Ptrofs.zero = Vptr b1 Ptrofs.zero) by (exists b; auto).
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  unfold globdef; destruct (prog_defmap unit)!id as [[[f|ef] |gv] |] eqn:G; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  destruct (ef_inline ef) eqn:INLINE; auto.
(* Goal: @eq Cminor.fundef fd (@External Cminor.function ef) *)
  destruct (prog_defmap_linkorder _ _ _ _ H G) as (gd & P & Q).
(* Goal: @eq Cminor.fundef fd (@External Cminor.function ef) *)
  inv Q. inv H2.
- apply Genv.find_def_symbol in P. destruct P as (b' & X & Y). fold ge in X, Y.
  rewrite <- Genv.find_funct_ptr_iff in Y. congruence.
- simpl in INLINE. discriminate.
Qed.

(** Translation of [switch] statements *)

Inductive Rint: Z -> val -> Prop :=
  | Rint_intro: forall n, Rint (Int.unsigned n) (Vint n).

Inductive Rlong: Z -> val -> Prop :=
  | Rlong_intro: forall n, Rlong (Int64.unsigned n) (Vlong n).

Section SEL_SWITCH.

Variable make_cmp_eq: expr -> Z -> expr.
Variable make_cmp_ltu: expr -> Z -> expr.
Variable make_sub: expr -> Z -> expr.
Variable make_to_int: expr -> expr.
Variable modulus: Z.
Variable R: Z -> val -> Prop.

Hypothesis eval_make_cmp_eq: forall sp e m le a v i n,
  eval_expr tge sp e m le a v -> R i v -> 0 <= n < modulus ->
  eval_expr tge sp e m le (make_cmp_eq a n) (Val.of_bool (zeq i n)).
Hypothesis eval_make_cmp_ltu: forall sp e m le a v i n,
  eval_expr tge sp e m le a v -> R i v -> 0 <= n < modulus ->
  eval_expr tge sp e m le (make_cmp_ltu a n) (Val.of_bool (zlt i n)).
Hypothesis eval_make_sub: forall sp e m le a v i n,
  eval_expr tge sp e m le a v -> R i v -> 0 <= n < modulus ->
  exists v', eval_expr tge sp e m le (make_sub a n) v' /\ R ((i - n) mod modulus) v'.
Hypothesis eval_make_to_int: forall sp e m le a v i,
  eval_expr tge sp e m le a v -> R i v ->
  exists v', eval_expr tge sp e m le (make_to_int a) v' /\ Rint (i mod Int.modulus) v'.

Lemma sel_switch_correct_rec:
  forall sp e m varg i x,
  R i varg ->
  forall t arg le,
  wf_comptree modulus t ->
  nth_error le arg = Some varg ->
  comptree_match modulus i t = Some x ->
  eval_exitexpr tge sp e m le (sel_switch make_cmp_eq make_cmp_ltu make_sub make_to_int arg t) x.
Proof.
  intros until x; intros Ri. induction t; simpl; intros until le; intros WF ARG MATCH.
- (* base case *)
(* Goal: final_state (Returnstate (Vint r) Kstop m') r *)
  inv MATCH. constructor.
- (* eq test *)
  inv WF.
  assert (eval_expr tge sp e m le (make_cmp_eq (Eletvar arg) key) (Val.of_bool (zeq i key))).
(* Goal: forall (id : ident) (name : string) (sg : signature) (_ : @helper_declared Cminor.function unit prog id name sg), @helper_declared function unit tprog id name sg *)
(* Goal: forall (hf : helper_functions) (_ : @helper_functions_declared Cminor.function unit prog hf), @helper_functions_declared function unit tprog hf *)
  { eapply eval_make_cmp_eq; eauto. constructor; auto. }
  eapply eval_XEcondition with (va := zeq i key).
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_condexpr_of_expr; eauto. destruct (zeq i key); constructor; auto.
  destruct (zeq i key); simpl.
  + inv MATCH. constructor.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  + eapply IHt; eauto.
- (* lt test *)
  inv WF.
  assert (eval_expr tge sp e m le (make_cmp_ltu (Eletvar arg) key) (Val.of_bool (zlt i key))).
(* Goal: forall (id : ident) (name : string) (sg : signature) (_ : @helper_declared Cminor.function unit prog id name sg), @helper_declared function unit tprog id name sg *)
(* Goal: forall (hf : helper_functions) (_ : @helper_functions_declared Cminor.function unit prog hf), @helper_functions_declared function unit tprog hf *)
  { eapply eval_make_cmp_ltu; eauto. constructor; auto. }
  eapply eval_XEcondition with (va := zlt i key).
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_condexpr_of_expr; eauto. destruct (zlt i key); constructor; auto.
  destruct (zlt i key); simpl.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  + eapply IHt1; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  + eapply IHt2; eauto.
- (* jump table *)
  inv WF.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit (eval_make_sub sp e m le). eapply eval_Eletvar. eauto. eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  instantiate (1 := ofs). auto.
  intros (v' & A & B).
  set (i' := (i - ofs) mod modulus) in *.
  assert (eval_expr tge sp e m (v' :: le) (make_cmp_ltu (Eletvar O) sz) (Val.of_bool (zlt i' sz))).
(* Goal: forall (id : ident) (name : string) (sg : signature) (_ : @helper_declared Cminor.function unit prog id name sg), @helper_declared function unit tprog id name sg *)
(* Goal: forall (hf : helper_functions) (_ : @helper_functions_declared Cminor.function unit prog hf), @helper_functions_declared function unit tprog hf *)
  { eapply eval_make_cmp_ltu; eauto. constructor; auto. }
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor. eauto.
  eapply eval_XEcondition with (va := zlt i' sz).
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_condexpr_of_expr; eauto. destruct (zlt i' sz); constructor; auto.
  destruct (zlt i' sz); simpl.
  + exploit (eval_make_to_int sp e m (v' :: le) (Eletvar O)).
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
    constructor. simpl; eauto. eauto. intros (v'' & C & D). inv D.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
    econstructor; eauto. congruence.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  + eapply IHt; eauto.
Qed.

Lemma sel_switch_correct:
  forall dfl cases arg sp e m varg i t le,
  validate_switch modulus dfl cases t = true ->
  eval_expr tge sp e m le arg varg ->
  R i varg ->
  0 <= i < modulus ->
  eval_exitexpr tge sp e m le
     (XElet arg (sel_switch make_cmp_eq make_cmp_ltu make_sub make_to_int O t))
     (switch_target i dfl cases).
Proof.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  intros. exploit validate_switch_correct; eauto. omega. intros [A B].
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor. eauto. eapply sel_switch_correct_rec; eauto.
Qed.

End SEL_SWITCH.

Section SEL_SWITH_INT.

Variable cunit: Cminor.program.
Variable hf: helper_functions.
Hypothesis LINK: linkorder cunit prog.
Hypothesis HF: helper_functions_declared cunit hf.

Let HF': helper_functions_declared tprog hf.
Proof.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply helper_functions_preserved. eapply helper_functions_declared_linkorder; eauto.
Qed.
Lemma sel_switch_int_correct:
  forall dfl cases arg sp e m i t le,
  validate_switch Int.modulus dfl cases t = true ->
  eval_expr tge sp e m le arg (Vint i) ->
  eval_exitexpr tge sp e m le (XElet arg (sel_switch_int O t)) (switch_target (Int.unsigned i) dfl cases).
Proof.
  assert (INTCONST: forall n sp e m le,
            eval_expr tge sp e m le (Eop (Ointconst n) Enil) (Vint n)).
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  { intros. econstructor. constructor. auto. }
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  intros. eapply sel_switch_correct with (R := Rint); eauto.
- intros until n; intros EVAL R RANGE.
  exploit eval_comp. eexact EVAL. apply (INTCONST (Int.repr n)).
  instantiate (1 := Ceq). intros (vb & A & B).
  inv R. unfold Val.cmp in B. simpl in B. revert B.
  predSpec Int.eq Int.eq_spec n0 (Int.repr n); intros B; inv B.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  rewrite Int.unsigned_repr. unfold proj_sumbool; rewrite zeq_true; auto.
  unfold Int.max_unsigned; omega.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  unfold proj_sumbool; rewrite zeq_false; auto.
  red; intros; elim H1. rewrite <- (Int.repr_unsigned n0). congruence.
- intros until n; intros EVAL R RANGE.
  exploit eval_compu. eexact EVAL. apply (INTCONST (Int.repr n)).
  instantiate (1 := Clt). intros (vb & A & B).
  inv R. unfold Val.cmpu in B. simpl in B.
  unfold Int.ltu in B. rewrite Int.unsigned_repr in B.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  destruct (zlt (Int.unsigned n0) n); inv B; auto.
  unfold Int.max_unsigned; omega.
- intros until n; intros EVAL R RANGE.
  exploit eval_sub. eexact EVAL. apply (INTCONST (Int.repr n)). intros (vb & A & B).
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  inv R. simpl in B. inv B. econstructor; split; eauto.
  replace ((Int.unsigned n0 - n) mod Int.modulus)
     with (Int.unsigned (Int.sub n0 (Int.repr n))).
(* Goal: final_state (Returnstate (Vint r) Kstop m') r *)
  constructor.
  unfold Int.sub. rewrite Int.unsigned_repr_eq. f_equal. f_equal.
  apply Int.unsigned_repr. unfold Int.max_unsigned; omega.
- intros until i0; intros EVAL R. exists v; split; auto.
(* Goal: final_state (Returnstate (Vint r) Kstop m') r *)
  inv R. rewrite Zmod_small by (apply Int.unsigned_range). constructor.
- constructor.
- apply Int.unsigned_range.
Qed.

Lemma sel_switch_long_correct:
  forall dfl cases arg sp e m i t le,
  validate_switch Int64.modulus dfl cases t = true ->
  eval_expr tge sp e m le arg (Vlong i) ->
  eval_exitexpr tge sp e m le (XElet arg (sel_switch_long O t)) (switch_target (Int64.unsigned i) dfl cases).
Proof.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  intros. eapply sel_switch_correct with (R := Rlong); eauto.
- intros until n; intros EVAL R RANGE.
  eapply eval_cmpl. eexact EVAL. apply eval_longconst with (n := Int64.repr n).
  inv R. unfold Val.cmpl. simpl. f_equal; f_equal. unfold Int64.eq.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  rewrite Int64.unsigned_repr. destruct (zeq (Int64.unsigned n0) n); auto.
  unfold Int64.max_unsigned; omega.
- intros until n; intros EVAL R RANGE.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_cmplu; auto. eexact EVAL. apply eval_longconst with (n := Int64.repr n).
  inv R. unfold Val.cmplu. simpl. f_equal; f_equal. unfold Int64.ltu.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  rewrite Int64.unsigned_repr. destruct (zlt (Int64.unsigned n0) n); auto.
  unfold Int64.max_unsigned; omega.
- intros until n; intros EVAL R RANGE.
  exploit eval_subl; auto; try apply HF'. eexact EVAL. apply eval_longconst with (n := Int64.repr n).
  intros (vb & A & B).
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  inv R. simpl in B. inv B. econstructor; split; eauto.
  replace ((Int64.unsigned n0 - n) mod Int64.modulus)
     with (Int64.unsigned (Int64.sub n0 (Int64.repr n))).
(* Goal: final_state (Returnstate (Vint r) Kstop m') r *)
  constructor.
  unfold Int64.sub. rewrite Int64.unsigned_repr_eq. f_equal. f_equal.
  apply Int64.unsigned_repr. unfold Int64.max_unsigned; omega.
- intros until i0; intros EVAL R.
  exploit eval_lowlong. eexact EVAL. intros (vb & A & B).
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  inv R. simpl in B. inv B. econstructor; split; eauto.
  replace (Int64.unsigned n mod Int.modulus) with (Int.unsigned (Int64.loword n)).
(* Goal: final_state (Returnstate (Vint r) Kstop m') r *)
  constructor.
  unfold Int64.loword. apply Int.unsigned_repr_eq.
- constructor.
- apply Int64.unsigned_range.
Qed.

End SEL_SWITH_INT.

(** Compatibility of evaluation functions with the "less defined than" relation. *)

Ltac TrivialExists :=
  match goal with
  | [ |- exists v, Some ?x = Some v /\ _ ] => exists x; split; auto
  | _ => idtac
  end.

Lemma eval_unop_lessdef:
  forall op v1 v1' v,
  eval_unop op v1 = Some v -> Val.lessdef v1 v1' ->
  exists v', eval_unop op v1' = Some v' /\ Val.lessdef v v'.
Proof.
(* Goal: forall (op : unary_operation) (v1 v1' v : val) (_ : @eq (option val) (eval_unop op v1) (@Some val v)) (_ : Val.lessdef v1 v1'), @ex val (fun v' : val => Logic.and (@eq (option val) (eval_unop op v1') (@Some val v')) (Val.lessdef v v')) *)
  intros until v; intros EV LD. inv LD.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exists v; auto.
(* Goal: @ex val (fun v' : val => Logic.and (@eq (option val) (eval_unop op v1') (@Some val v')) (Val.lessdef v v')) *)
  destruct op; simpl in *; inv EV; TrivialExists.
Qed.

Lemma eval_binop_lessdef:
  forall op v1 v1' v2 v2' v m m',
  eval_binop op v1 v2 m = Some v ->
  Val.lessdef v1 v1' -> Val.lessdef v2 v2' -> Mem.extends m m' ->
  exists v', eval_binop op v1' v2' m' = Some v' /\ Val.lessdef v v'.
Proof.
  intros until m'; intros EV LD1 LD2 ME.
  assert (exists v', eval_binop op v1' v2' m = Some v' /\ Val.lessdef v v').
(* Goal: forall (id : ident) (name : string) (sg : signature) (_ : @helper_declared Cminor.function unit prog id name sg), @helper_declared function unit tprog id name sg *)
(* Goal: forall (hf : helper_functions) (_ : @helper_functions_declared Cminor.function unit prog hf), @helper_functions_declared function unit tprog hf *)
  { inv LD1. inv LD2. exists v; auto.
    destruct op; destruct v1'; simpl in *; inv EV; TrivialExists.
    destruct op; simpl in *; inv EV; TrivialExists. }
  assert (CMPU: forall c,
    eval_binop (Ocmpu c) v1 v2 m = Some v ->
    exists v' : val, eval_binop (Ocmpu c) v1' v2' m' = Some v' /\ Val.lessdef v v').
(* Goal: forall (id : ident) (name : string) (sg : signature) (_ : @helper_declared Cminor.function unit prog id name sg), @helper_declared function unit tprog id name sg *)
(* Goal: forall (hf : helper_functions) (_ : @helper_functions_declared Cminor.function unit prog hf), @helper_functions_declared function unit tprog hf *)
  { intros c A. simpl in *. inv A. econstructor; split. eauto.
    apply Val.of_optbool_lessdef.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
    intros. apply Val.cmpu_bool_lessdef with (Mem.valid_pointer m) v1 v2; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
    intros; eapply Mem.valid_pointer_extends; eauto. }
  assert (CMPLU: forall c,
    eval_binop (Ocmplu c) v1 v2 m = Some v ->
    exists v' : val, eval_binop (Ocmplu c) v1' v2' m' = Some v' /\ Val.lessdef v v').
(* Goal: forall (id : ident) (name : string) (sg : signature) (_ : @helper_declared Cminor.function unit prog id name sg), @helper_declared function unit tprog id name sg *)
(* Goal: forall (hf : helper_functions) (_ : @helper_functions_declared Cminor.function unit prog hf), @helper_functions_declared function unit tprog hf *)
  { intros c A. simpl in *. unfold Val.cmplu in *.
    destruct (Val.cmplu_bool (Mem.valid_pointer m) c v1 v2) as [b|] eqn:C; simpl in A; inv A.
    eapply Val.cmplu_bool_lessdef with (valid_ptr' := (Mem.valid_pointer m')) in C;
    eauto using Mem.valid_pointer_extends.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
    rewrite C. exists (Val.of_bool b); auto. }
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  destruct op; auto.
Qed.

(** * Semantic preservation for instruction selection. *)

(** Relationship between the local environments. *)

Definition env_lessdef (e1 e2: env) : Prop :=
  forall id v1, e1!id = Some v1 -> exists v2, e2!id = Some v2 /\ Val.lessdef v1 v2.

Lemma set_var_lessdef:
  forall e1 e2 id v1 v2,
  env_lessdef e1 e2 -> Val.lessdef v1 v2 ->
  env_lessdef (PTree.set id v1 e1) (PTree.set id v2 e2).
Proof.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  intros; red; intros. rewrite PTree.gsspec in *. destruct (peq id0 id).
(* Goal: @eq Cminor.fundef fd (@External Cminor.function ef) *)
  exists v2; split; congruence.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  auto.
Qed.

Lemma set_optvar_lessdef:
  forall e1 e2 optid v1 v2,
  env_lessdef e1 e2 -> Val.lessdef v1 v2 ->
  env_lessdef (set_optvar optid v1 e1) (set_optvar optid v2 e2).
Proof.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  unfold set_optvar; intros. destruct optid; auto. apply set_var_lessdef; auto.
Qed.

Lemma set_params_lessdef:
  forall il vl1 vl2,
  Val.lessdef_list vl1 vl2 ->
  env_lessdef (set_params vl1 il) (set_params vl2 il).
Proof.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  induction il; simpl; intros.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  red; intros. rewrite PTree.gempty in H0; congruence.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  inv H; apply set_var_lessdef; auto.
Qed.

Lemma set_locals_lessdef:
  forall e1 e2, env_lessdef e1 e2 ->
  forall il, env_lessdef (set_locals il e1) (set_locals il e2).
Proof.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  induction il; simpl. auto. apply set_var_lessdef; auto.
Qed.

(** Semantic preservation for expressions. *)

Section EXPRESSIONS.

Variable cunit: Cminor.program.
Variable hf: helper_functions.
Hypothesis LINK: linkorder cunit prog.
Hypothesis HF: helper_functions_declared cunit hf.

Lemma sel_expr_correct:
  forall sp e m a v,
  Cminor.eval_expr ge sp e m a v ->
  forall e' le m',
  env_lessdef e e' -> Mem.extends m m' ->
  exists v', eval_expr tge sp e' m' le (sel_expr a) v' /\ Val.lessdef v v'.
Proof.
  induction 1; intros; simpl.
  (* Evar *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit H0; eauto. intros [v' [A B]]. exists v'; split; auto. constructor; auto.
  (* Econst *)
(* Goal: final_state R r *)
  destruct cst; simpl in *; inv H.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exists (Vint i); split; auto. econstructor. constructor. auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exists (Vfloat f); split; auto. econstructor. constructor. auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exists (Vsingle f); split; auto. econstructor. constructor. auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exists (Vlong i); split; auto. apply eval_longconst.
  unfold Genv.symbol_address; rewrite <- symbols_preserved; fold (Genv.symbol_address tge i i0). apply eval_addrsymbol.
  apply eval_addrstack.
  (* Eunop *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit IHeval_expr; eauto. intros [v1' [A B]].
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit eval_unop_lessdef; eauto. intros [v' [C D]].
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit eval_sel_unop; eauto. intros [v'' [E F]].
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exists v''; split; eauto. eapply Val.lessdef_trans; eauto.
  (* Ebinop *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit IHeval_expr1; eauto. intros [v1' [A B]].
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit IHeval_expr2; eauto. intros [v2' [C D]].
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit eval_binop_lessdef; eauto. intros [v' [E F]].
  assert (G: exists v'', eval_expr tge sp e' m' le (sel_binop op (sel_expr a1) (sel_expr a2)) v'' /\ Val.lessdef v' v'')
  by (eapply eval_sel_binop; eauto).
  destruct G as [v'' [P Q]].
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exists v''; split; eauto. eapply Val.lessdef_trans; eauto.
  (* Eload *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit IHeval_expr; eauto. intros [vaddr' [A B]].
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit Mem.loadv_extends; eauto. intros [v' [C D]].
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exists v'; split; auto. eapply eval_load; eauto.
Qed.

Lemma sel_exprlist_correct:
  forall sp e m a v,
  Cminor.eval_exprlist ge sp e m a v ->
  forall e' le m',
  env_lessdef e e' -> Mem.extends m m' ->
  exists v', eval_exprlist tge sp e' m' le (sel_exprlist a) v' /\ Val.lessdef_list v v'.
Proof.
  induction 1; intros; simpl.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exists (@nil val); split; auto. constructor.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit sel_expr_correct; eauto. intros [v1' [A B]].
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit IHeval_exprlist; eauto. intros [vl' [C D]].
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exists (v1' :: vl'); split; auto. constructor; eauto.
Qed.

Lemma sel_builtin_arg_correct:
  forall sp e e' m m' a v c,
  env_lessdef e e' -> Mem.extends m m' ->
  Cminor.eval_expr ge sp e m a v ->
  exists v',
     CminorSel.eval_builtin_arg tge sp e' m' (sel_builtin_arg a c) v'
  /\ Val.lessdef v v'.
Proof.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  intros. unfold sel_builtin_arg.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit sel_expr_correct; eauto. intros (v1 & A & B).
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exists v1; split; auto.
  destruct (builtin_arg_ok (builtin_arg (sel_expr a)) c).
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply eval_builtin_arg; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  constructor; auto.
Qed.

Lemma sel_builtin_args_correct:
  forall sp e e' m m',
  env_lessdef e e' -> Mem.extends m m' ->
  forall al vl,
  Cminor.eval_exprlist ge sp e m al vl ->
  forall cl,
  exists vl',
     list_forall2 (CminorSel.eval_builtin_arg tge sp e' m')
                  (sel_builtin_args al cl)
                  vl'
  /\ Val.lessdef_list vl vl'.
Proof.
  induction 3; intros; simpl.
- exists (@nil val); split; constructor.
- exploit sel_builtin_arg_correct; eauto. intros (v1' & A & B).
  edestruct IHeval_exprlist as (vl' & C & D).
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exists (v1' :: vl'); split; auto. constructor; eauto.
Qed.

Lemma sel_builtin_res_correct:
  forall oid v e v' e',
  env_lessdef e e' -> Val.lessdef v v' ->
  env_lessdef (set_optvar oid v e) (set_builtin_res (sel_builtin_res oid) v' e').
Proof.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  intros. destruct oid; simpl; auto. apply set_var_lessdef; auto.
Qed.

End EXPRESSIONS.

(** Semantic preservation for functions and statements. *)

Inductive match_cont: Cminor.program -> helper_functions -> Cminor.cont -> CminorSel.cont -> Prop :=
  | match_cont_stop: forall cunit hf,
      match_cont cunit hf Cminor.Kstop Kstop
  | match_cont_seq: forall cunit hf s s' k k',
      sel_stmt (prog_defmap cunit) s = OK s' ->
      match_cont cunit hf k k' ->
      match_cont cunit hf (Cminor.Kseq s k) (Kseq s' k')
  | match_cont_block: forall cunit hf k k',
      match_cont cunit hf k k' ->
      match_cont cunit hf (Cminor.Kblock k) (Kblock k')
  | match_cont_call: forall cunit' hf' cunit hf id f sp e k f' e' k',
      linkorder cunit prog ->
      helper_functions_declared cunit hf ->
      sel_function (prog_defmap cunit) hf f = OK f' ->
      match_cont cunit hf k k' -> env_lessdef e e' ->
      match_cont cunit' hf' (Cminor.Kcall id f sp e k) (Kcall id f' sp e' k').

Definition match_call_cont (k: Cminor.cont) (k': CminorSel.cont) : Prop :=
  forall cunit hf, match_cont cunit hf k k'.

Inductive match_states: Cminor.state -> CminorSel.state -> Prop :=
  | match_state: forall cunit hf f f' s k s' k' sp e m e' m'
        (LINK: linkorder cunit prog)
        (HF: helper_functions_declared cunit hf)
        (TF: sel_function (prog_defmap cunit) hf f = OK f')
        (TS: sel_stmt (prog_defmap cunit) s = OK s')
        (MC: match_cont cunit hf k k')
        (LD: env_lessdef e e')
        (ME: Mem.extends m m'),
      match_states
        (Cminor.State f s k sp e m)
        (State f' s' k' sp e' m')
  | match_callstate: forall cunit f f' args args' k k' m m'
        (LINK: linkorder cunit prog)
        (TF: match_fundef cunit f f')
        (MC: match_call_cont k k')
        (LD: Val.lessdef_list args args')
        (ME: Mem.extends m m'),
      match_states
        (Cminor.Callstate f args k m)
        (Callstate f' args' k' m')
  | match_returnstate: forall v v' k k' m m'
        (MC: match_call_cont k k')
        (LD: Val.lessdef v v')
        (ME: Mem.extends m m'),
      match_states
        (Cminor.Returnstate v k m)
        (Returnstate v' k' m')
  | match_builtin_1: forall cunit hf ef args args' optid f sp e k m al f' e' k' m'
        (LINK: linkorder cunit prog)
        (HF: helper_functions_declared cunit hf)
        (TF: sel_function (prog_defmap cunit) hf f = OK f')
        (MC: match_cont cunit hf k k')
        (LDA: Val.lessdef_list args args')
        (LDE: env_lessdef e e')
        (ME: Mem.extends m m')
        (EA: list_forall2 (CminorSel.eval_builtin_arg tge sp e' m') al args'),
      match_states
        (Cminor.Callstate (External ef) args (Cminor.Kcall optid f sp e k) m)
        (State f' (Sbuiltin (sel_builtin_res optid) ef al) k' sp e' m')
  | match_builtin_2: forall cunit hf v v' optid f sp e k m f' e' m' k'
        (LINK: linkorder cunit prog)
        (HF: helper_functions_declared cunit hf)
        (TF: sel_function (prog_defmap cunit) hf f = OK f')
        (MC: match_cont cunit hf k k')
        (LDV: Val.lessdef v v')
        (LDE: env_lessdef e e')
        (ME: Mem.extends m m'),
      match_states
        (Cminor.Returnstate v (Cminor.Kcall optid f sp e k) m)
        (State f' Sskip k' sp (set_builtin_res (sel_builtin_res optid) v' e') m').

Remark call_cont_commut:
  forall cunit hf k k', match_cont cunit hf k k' -> match_call_cont (Cminor.call_cont k) (call_cont k').
Proof.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  induction 1; simpl; auto; red; intros.
- constructor.
- eapply match_cont_call with (hf := hf); eauto.
Qed.

Remark match_is_call_cont:
  forall cunit hf k k', match_cont cunit hf k k' -> Cminor.is_call_cont k -> match_call_cont k k'.
Proof.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  destruct 1; intros; try contradiction; red; intros.
- constructor.
- eapply match_cont_call with (hf := hf); eauto.
Qed.

Remark match_call_cont_cont:
  forall k k', match_call_cont k k' -> exists cunit hf, match_cont cunit hf k k'.
Proof.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  intros. simple refine (let cunit : Cminor.program := _ in _).
(* Goal: Cminor.program *)
(* Goal: @ex Cminor.program (fun cunit : Cminor.program => @ex helper_functions (fun hf : helper_functions => match_cont cunit hf k k')) *)
  econstructor. apply nil. apply nil. apply xH.
(* Goal: @ex Cminor.program (fun cunit : Cminor.program => @ex helper_functions (fun hf : helper_functions => match_cont cunit hf k k')) *)
  simple refine (let hf : helper_functions := _ in _).
(* Goal: ident *)
(* Goal: @ex Cminor.program (fun cunit : Cminor.program => @ex helper_functions (fun hf : helper_functions => match_cont cunit hf k k')) *)
  econstructor; apply xH.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exists cunit, hf; auto.
Qed.

Remark find_label_commut:
  forall cunit hf lbl s k s' k',
  match_cont cunit hf k k' ->
  sel_stmt (prog_defmap cunit) s = OK s' ->
  match Cminor.find_label lbl s k, find_label lbl s' k' with
  | None, None => True
  | Some(s1, k1), Some(s1', k1') => sel_stmt (prog_defmap cunit) s1 = OK s1' /\ match_cont cunit hf k1 k1'
  | _, _ => False
  end.
Proof.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  induction s; intros until k'; simpl; intros MC SE; try (monadInv SE); simpl; auto.
(* store *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  unfold store. destruct (addressing m (sel_expr e)); simpl; auto.
(* call *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  destruct (classify_call (prog_defmap cunit) e); simpl; auto.
(* tailcall *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  destruct (classify_call (prog_defmap cunit) e); simpl; auto.
(* seq *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto. eauto.
  destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)) as [[sx kx] | ];
  destruct (find_label lbl x (Kseq x0 k')) as [[sy ky] | ];
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  intuition. apply IHs2; auto.
(* ifthenelse *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit (IHs1 k); eauto.
  destruct (Cminor.find_label lbl s1 k) as [[sx kx] | ];
  destruct (find_label lbl x k') as [[sy ky] | ];
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  intuition. apply IHs2; auto.
(* loop *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply IHs. constructor; auto. simpl; rewrite EQ; auto. auto.
(* block *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply IHs. constructor; auto. auto.
(* switch *)
  destruct b.
  destruct (validate_switch Int64.modulus n l (compile_switch Int64.modulus n l)); inv SE.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  simpl; auto.
  destruct (validate_switch Int.modulus n l (compile_switch Int.modulus n l)); inv SE.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  simpl; auto.
(* return *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  destruct o; inv SE; simpl; auto.
(* label *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  destruct (ident_eq lbl l). auto. apply IHs; auto.
Qed.

Definition measure (s: Cminor.state) : nat :=
  match s with
  | Cminor.Callstate _ _ _ _ => 0%nat
  | Cminor.State _ _ _ _ _ _ => 1%nat
  | Cminor.Returnstate _ _ _ => 2%nat
  end.

Lemma sel_step_correct:
  forall S1 t S2, Cminor.step ge S1 t S2 ->
  forall T1, match_states S1 T1 ->
  (exists T2, step tge T1 t T2 /\ match_states S2 T2)
  \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 T1)%nat.
Proof.
  induction 1; intros T1 ME; inv ME; try (monadInv TS).
- (* skip seq *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  inv MC. left; econstructor; split. econstructor. econstructor; eauto.
- (* skip block *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  inv MC. left; econstructor; split. econstructor. econstructor; eauto.
- (* skip call *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit Mem.free_parallel_extends; eauto. intros [m2' [A B]].
  left; econstructor; split.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor. inv MC; simpl in H; simpl; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  erewrite stackspace_function_translated; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor; eauto. eapply match_is_call_cont; eauto.
- (* assign *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit sel_expr_correct; eauto. intros [v' [A B]].
  left; econstructor; split.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor; eauto. apply set_var_lessdef; auto.
- (* store *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit sel_expr_correct. eauto. eauto. eexact H. eauto. eauto. intros [vaddr' [A B]].
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit sel_expr_correct. eauto. eauto. eexact H0. eauto. eauto. intros [v' [C D]].
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit Mem.storev_extends; eauto. intros [m2' [P Q]].
  left; econstructor; split.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply eval_store; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor; eauto.
- (* Scall *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit classify_call_correct; eauto.
  destruct (classify_call (prog_defmap cunit) a) as [ | id | ef].
+ (* indirect *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit sel_expr_correct; eauto. intros [vf' [A B]].
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit sel_exprlist_correct; eauto. intros [vargs' [C D]].
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit functions_translated; eauto. intros (cunit' & fd' & U & V & W).
  left; econstructor; split.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor; eauto. econstructor; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply sig_function_translated; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply match_callstate with (cunit := cunit'); eauto.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  red; intros. eapply match_cont_call with (cunit := cunit) (hf := hf); eauto.
+ (* direct *)
  intros [b [U V]].
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit sel_exprlist_correct; eauto. intros [vargs' [C D]].
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit functions_translated; eauto. intros (cunit' & fd' & X & Y & Z).
  left; econstructor; split.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  subst vf. econstructor; eauto. rewrite symbols_preserved; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply sig_function_translated; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply match_callstate with (cunit := cunit'); eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  red; intros; eapply match_cont_call with (cunit := cunit) (hf := hf); eauto.
+ (* turned into Sbuiltin *)
  intros EQ. subst fd.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit sel_builtin_args_correct; eauto. intros [vargs' [C D]].
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  right; split. simpl. omega. split. auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor; eauto.
- (* Stailcall *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]].
  erewrite <- stackspace_function_translated in P by eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit sel_expr_correct; eauto. intros [vf' [A B]].
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit sel_exprlist_correct; eauto. intros [vargs' [C D]].
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit functions_translated; eauto. intros (cunit' & fd' & E & F & G).
  left; econstructor; split.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit classify_call_correct. eexact LINK. eauto. eauto.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  destruct (classify_call (prog_defmap cunit)) as [ | id | ef]; intros.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor; eauto. econstructor; eauto. eapply sig_function_translated; eauto.
  destruct H2 as [b [U V]]. subst vf. inv B.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor; eauto. econstructor; eauto. rewrite symbols_preserved; eauto. eapply sig_function_translated; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor; eauto. econstructor; eauto. eapply sig_function_translated; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply match_callstate with (cunit := cunit'); eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply call_cont_commut; eauto.
- (* Sbuiltin *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit sel_builtin_args_correct; eauto. intros [vargs' [P Q]].
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit external_call_mem_extends; eauto.
  intros [vres' [m2 [A [B [C D]]]]].
  left; econstructor; split.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor. eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor; eauto. apply sel_builtin_res_correct; auto.
- (* Seq *)
  left; econstructor; split.
(* Goal: final_state (Returnstate (Vint r) Kstop m') r *)
  constructor.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor; eauto. constructor; auto.
- (* Sifthenelse *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit sel_expr_correct; eauto. intros [v' [A B]].
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  assert (Val.bool_of_val v' b). inv B. auto. inv H0.
  left; exists (State f' (if b then x else x0) k' sp e' m'); split.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor; eauto. eapply eval_condexpr_of_expr; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor; eauto. destruct b; auto.
- (* Sloop *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  left; econstructor; split. constructor. econstructor; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  constructor; auto. simpl; rewrite EQ; auto.
- (* Sblock *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  left; econstructor; split. constructor. econstructor; eauto. constructor; auto.
- (* Sexit seq *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  inv MC. left; econstructor; split. constructor. econstructor; eauto.
- (* Sexit0 block *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  inv MC. left; econstructor; split. constructor. econstructor; eauto.
- (* SexitS block *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  inv MC. left; econstructor; split. constructor. econstructor; eauto.
- (* Sswitch *)
  inv H0; simpl in TS.
+ set (ct := compile_switch Int.modulus default cases) in *.
  destruct (validate_switch Int.modulus default cases ct) eqn:VALID; inv TS.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit sel_expr_correct; eauto. intros [v' [A B]]. inv B.
  left; econstructor; split.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor. eapply sel_switch_int_correct; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor; eauto.
+ set (ct := compile_switch Int64.modulus default cases) in *.
  destruct (validate_switch Int64.modulus default cases ct) eqn:VALID; inv TS.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit sel_expr_correct; eauto. intros [v' [A B]]. inv B.
  left; econstructor; split.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor. eapply sel_switch_long_correct; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor; eauto.
- (* Sreturn None *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]].
  erewrite <- stackspace_function_translated in P by eauto.
  left; econstructor; split.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor. simpl; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor; eauto. eapply call_cont_commut; eauto.
- (* Sreturn Some *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]].
  erewrite <- stackspace_function_translated in P by eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit sel_expr_correct; eauto. intros [v' [A B]].
  left; econstructor; split.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor; eauto. eapply call_cont_commut; eauto.
- (* Slabel *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  left; econstructor; split. constructor. econstructor; eauto.
- (* Sgoto *)
  assert (sel_stmt (prog_defmap cunit) (Cminor.fn_body f) = OK (fn_body f')).
(* Goal: forall (id : ident) (name : string) (sg : signature) (_ : @helper_declared Cminor.function unit prog id name sg), @helper_declared function unit tprog id name sg *)
(* Goal: forall (hf : helper_functions) (_ : @helper_functions_declared Cminor.function unit prog hf), @helper_functions_declared function unit tprog hf *)
  { monadInv TF; simpl; auto. }
  exploit (find_label_commut cunit hf lbl (Cminor.fn_body f) (Cminor.call_cont k)).
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
    eapply call_cont_commut; eauto. eauto.
  rewrite H.
  destruct (find_label lbl (fn_body f') (call_cont k'0))
  as [[s'' k'']|] eqn:?; intros; try contradiction.
  destruct H1.
  left; econstructor; split.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor; eauto.
- (* internal function *)
  destruct TF as (hf & HF & TF). specialize (MC cunit hf).
  monadInv TF. generalize EQ; intros TF; monadInv TF.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl.
  intros [m2' [A B]].
  left; econstructor; split.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor; simpl; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor; simpl; eauto. apply set_locals_lessdef. apply set_params_lessdef; auto.
- (* external call *)
  destruct TF as (hf & HF & TF).
  monadInv TF.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit external_call_mem_extends; eauto.
  intros [vres' [m2 [A [B [C D]]]]].
  left; econstructor; split.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor; eauto.
- (* external call turned into a Sbuiltin *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit external_call_mem_extends; eauto.
  intros [vres' [m2 [A [B [C D]]]]].
  left; econstructor; split.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor. eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor; eauto.
- (* return *)
(* Goal: final_state (Returnstate v' k' m') r *)
  apply match_call_cont_cont in MC. destruct MC as (cunit0 & hf0 & MC).
(* Goal: final_state (Returnstate v' k' m') r *)
  inv MC.
  left; econstructor; split.
(* Goal: Cminor.program *)
(* Goal: @ex Cminor.program (fun cunit : Cminor.program => @ex helper_functions (fun hf : helper_functions => match_cont cunit hf k k')) *)
  econstructor.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor; eauto. destruct optid; simpl; auto. apply set_var_lessdef; auto.
- (* return of an external call turned into a Sbuiltin *)
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  right; split. simpl; omega. split. auto. econstructor; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply sel_builtin_res_correct; auto.
Qed.

Lemma sel_initial_states:
  forall S, Cminor.initial_state prog S ->
  exists R, initial_state tprog R /\ match_states S R.
Proof.
  destruct 1.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  exploit function_ptr_translated; eauto. intros (cu & f' & A & B & C).
  econstructor; split.
(* Goal: Cminor.program *)
(* Goal: @ex Cminor.program (fun cunit : Cminor.program => @ex helper_functions (fun hf : helper_functions => match_cont cunit hf k k')) *)
  econstructor.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply (Genv.init_mem_match TRANSF); eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  rewrite (match_program_main TRANSF). fold tge. rewrite symbols_preserved. eauto.
  eexact A.
  rewrite <- H2. eapply sig_function_translated; eauto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  econstructor; eauto. red; intros; constructor. apply Mem.extends_refl.
Qed.

Lemma sel_final_states:
  forall S R r,
  match_states S R -> Cminor.final_state S r -> final_state R r.
Proof.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  intros. inv H0. inv H.
(* Goal: final_state (Returnstate v' k' m') r *)
  apply match_call_cont_cont in MC. destruct MC as (cunit0 & hf0 & MC).
(* Goal: final_state (Returnstate (Vint r) Kstop m') r *)
  inv MC. inv LD. constructor.
Qed.

Theorem transf_program_correct:
  forward_simulation (Cminor.semantics prog) (CminorSel.semantics tprog).
Proof.
(* Goal: forward_simulation (Cminor.semantics prog) (semantics tprog) *)
  apply forward_simulation_opt with (match_states := match_states) (measure := measure).
(* Goal: forall id : ident, @eq bool (Senv.public_symbol (symbolenv (semantics tprog)) id) (Senv.public_symbol (symbolenv (Cminor.semantics prog)) id) *)
(* Goal: forall (s1 : Smallstep.state (Cminor.semantics prog)) (_ : Smallstep.initial_state (Cminor.semantics prog) s1), @ex (Smallstep.state (semantics tprog)) (fun s2 : Smallstep.state (semantics tprog) => Logic.and (Smallstep.initial_state (semantics tprog) s2) (match_states s1 s2)) *)
(* Goal: forall (s1 : Smallstep.state (Cminor.semantics prog)) (s2 : Smallstep.state (semantics tprog)) (r : Int.int) (_ : match_states s1 s2) (_ : Smallstep.final_state (Cminor.semantics prog) s1 r), Smallstep.final_state (semantics tprog) s2 r *)
(* Goal: forall (s1 : Smallstep.state (Cminor.semantics prog)) (t : trace) (s1' : Smallstep.state (Cminor.semantics prog)) (_ : Smallstep.step (Cminor.semantics prog) (globalenv (Cminor.semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : match_states s1 s2), Logic.or (@ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (match_states s1' s2'))) (Logic.and (lt (measure s1') (measure s1)) (Logic.and (@eq trace t E0) (match_states s1' s2))) *)
  apply senv_preserved.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply sel_initial_states; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply sel_final_states; auto.
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  apply sel_step_correct; auto.
Qed.

End PRESERVATION.

(** ** Commutation with linking *)

Instance TransfSelectionLink : TransfLink match_prog.
Proof.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  red; intros. destruct (link_linkorder _ _ _ H) as [LO1 LO2].
(* Goal: env_lessdef e1 e2 *)
(* Goal: env_lessdef (@PTree.set val a Vundef (set_locals il e1)) (@PTree.set val a Vundef (set_locals il e2)) *)
  eapply link_match_program; eauto.
(* Goal: forall (S : Cminor.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Cminor.final_state S r), final_state R r *)
  intros. elim H3; intros hf1 [A1 B1]. elim H4; intros hf2 [A2 B2].
Local Transparent Linker_fundef.
  simpl in *. destruct f1, f2; simpl in *; monadInv B1; monadInv B2; simpl.
- discriminate.
- destruct e; inv H2. econstructor; eauto.
- destruct e; inv H2. econstructor; eauto.
- destruct (external_function_eq e e0); inv H2. econstructor; eauto.
Qed.
