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.


Require Import CUAST Footprint Blockset LDSimDefs_local LDSim_local.
Require Import InteractionSemantics IS_local val_casted InjRels
        MemOpFP Op_fp Cminor_op_footprint Cminor_local CminorSel_local
        selectop_proof selectdiv_proof splitlong_proof selectlong_proof
        selection.

Local Notation empfp:=FP.emp.
Local Notation footprint:=FP.t.

Local Open Scope cminorsel_scope.
Local Open Scope error_monad_scope.

Relational specification of instruction selection

Definition match_fundef (scu: cminor_comp_unit) (f: Cminor.fundef) (tf: CminorSel.fundef) : Prop :=
  exists hf, helper_functions_declared scu hf /\ sel_fundef (comp_unit_defmap scu) hf f = OK tf.

Definition match_cu (scu: cminor_comp_unit) (tcu: cminorsel_comp_unit) :=
  match_comp_unit_gen (match_fundef scu) eq scu tcu.

Lemma record_globdefs_sound:
  forall dm id gd, (record_globdefs dm)!id = Some gd -> dm!id = Some gd.

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

Lemma lookup_helper_correct:
  forall cu name sg id,
  lookup_helper (record_globdefs (comp_unit_defmap cu)) name sg = OK id ->
  helper_declared cu id name sg.


Lemma get_helpers_correct:
  forall cu hf,
  get_helpers (comp_unit_defmap cu) = OK hf -> helper_functions_declared cu hf.

Theorem transf_program_match:
  forall scu tcu, transf_program scu = OK tcu -> match_cu scu tcu.

Correctness of the instruction selection functions for expressions

Section PRESERVATION.

Variable scu: cminor_comp_unit.
Variable tcu: cminorsel_comp_unit.
Variable sge: Cminor.genv.
Variable tge: CminorSel.genv.
Hypothesis SGEINIT: globalenv_generic scu sge.
Hypothesis TGEINIT: globalenv_generic tcu tge.
Hypothesis S_EQ: sge.(Genv.genv_next) = tge.(Genv.genv_next).

Hypothesis TRANSF: match_cu scu tcu.

Lemma ge_match: ge_match_strict sge tge.

Lemma genv_match: Genv.match_genvs (match_globdef (fun f tf => match_fundef scu f tf) eq) sge tge.

Lemma symbols_preserved:
  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol sge s.

Lemma senv_preserved:
  Senv.equiv sge tge.

Lemma function_ptr_translated:
  forall (b: block) (f: Cminor.fundef),
  Genv.find_funct_ptr sge b = Some f ->
  exists tf,
  Genv.find_funct_ptr tge b = Some tf /\ match_fundef scu f tf.

Lemma functions_translated:
  forall v v' f,
    Genv.find_funct sge v = Some f ->
    Val.lessdef v v' ->
    exists tf, Genv.find_funct tge v' = Some tf /\ match_fundef scu f tf.

Lemma sig_function_translated:
  forall f tf, match_fundef scu f tf -> funsig tf = Cminor.funsig f.

Lemma stackspace_function_translated:
  forall dm hf f tf, sel_function dm hf f = OK tf -> fn_stackspace tf = Cminor.fn_stackspace f.

Lemma helper_functions_preserved:
  forall hf, helper_functions_declared scu hf -> helper_functions_declared tcu hf.

Section CMCONSTR.
Variable hf: helper_functions.
Hypothesis HF: helper_functions_declared scu hf.
Let HF': helper_functions_declared tcu hf.

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

Lemma eval_condexpr_of_expr_fp:
  forall a le v fp b,
    eval_expr tge sp e m le a v ->
    eval_expr_fp tge sp e m le a fp ->
    Val.bool_of_val v b ->
    eval_condexpr tge sp e m le (condexpr_of_expr a) b /\
    eval_condexpr_fp tge sp e m le (condexpr_of_expr a) fp.

Lemma eval_load_fp:
  forall le a v fp chunk v',
  eval_expr tge sp e m le a v ->
  eval_expr_fp tge sp e m le a fp ->
  Mem.loadv chunk m v = Some v' ->
  eval_expr tge sp e m le (load chunk a) v' /\
  eval_expr_fp tge sp e m le (load chunk a) (FP.union (loadv_fp chunk v) fp).

Lemma eval_store_fp:
  forall chunk a1 a2 v1 v2 fp1 fp2 f k m',
  eval_expr tge sp e m nil a1 v1 ->
  eval_expr_fp tge sp e m nil a1 fp1 ->
  eval_expr tge sp e m nil a2 v2 ->
  eval_expr_fp tge sp e m nil a2 fp2 ->
  Mem.storev chunk m v1 v2 = Some m' ->
  step tge (Core_State f (store chunk a1 a2) k sp e) m
       (FP.union (FP.union fp1 fp2) (storev_fp chunk v1)) (Core_State f Sskip k sp e) m'.

Ltac uopexploit H1 H2:=
  let v := fresh in
  let A := fresh in
  let B := fresh in
  exploit H1; try exacteval H2; eauto; intros [v [A B]]; evalge A.

Lemma eval_sel_unop_fp:
  forall le op a1 v1 fp v,
  eval_expr tge sp e m le a1 v1 ->
  eval_expr_fp tge sp e m le a1 fp ->
  eval_unop op v1 = Some v ->
  (exists v', eval_expr tge sp e m le (sel_unop op a1) v' /\ Val.lessdef v v') /\
  (exists fp', eval_expr_fp tge sp e m le (sel_unop op a1) fp' /\ FP.subset fp' fp).

Let tprog := mkprogram (cu_defs tcu) (cu_public tcu) 1%positive.


Ltac bexploit1 T1 H1 H2 :=
  (exploit T1; [exact H1|exact H2|]) || (exploit T1; [exact H1|exact H2| |]).
Ltac bexploit2 T1 H1 H2 :=
  ((exploit (T1 tprog); subst tprog; [exacteval H1|exacteval H2|])
  || (exploit (T1 tprog); subst tprog; [exacteval H1|exacteval H2| | ])
  || (exploit (T1 tprog); subst tprog; [|exacteval H1|exacteval H2| ])
  || (exploit (T1 tprog); subst tprog; [|exacteval H1|exacteval H2| | ])).
Ltac bexploit T1 T2:=
  match goal with
  | [ H1: (eval_expr _ _ _ _ _ ?a1 _),
          H2: (eval_expr _ _ _ _ _ ?a2 _)
      |- context[(_ ?a1 ?a2)] ]
    => (((bexploit2 T1 H1 H2); eauto; intros [?v [?A ?B]]; evalge A)
       || ((bexploit1 T1 H1 H2); eauto; intros [?v [?A ?B]]));
      split; [eauto| try eapply T2; eauto];
      try (exploit T2; [exact H1|eauto|exact H2|eauto|eauto|]; simpl; TrivFP; fail)
  end.

Lemma eval_sel_binop_fp:
  forall le op a1 a2 v1 v2 fp1 fp2 v fp,
    eval_expr tge sp e m le a1 v1 ->
    eval_expr_fp tge sp e m le a1 fp1 ->
    eval_expr tge sp e m le a2 v2 ->
    eval_expr_fp tge sp e m le a2 fp2 ->
    eval_binop op v1 v2 m = Some v ->
    eval_binop_fp op v1 v2 m = Some fp ->
    (exists v', eval_expr tge sp e m le (sel_binop op a1 a2) v' /\ Val.lessdef v v') /\
    (exists fp', eval_expr_fp tge sp e m le (sel_binop op a1 a2) fp' /\ FP.subset fp' (FP.union (FP.union fp1 fp2) fp)).

End CMCONSTR.

Lemma expr_is_addrof_ident_correct:
  forall e id,
  expr_is_addrof_ident e = Some id ->
  e = Cminor.Econst (Cminor.Oaddrsymbol id Ptrofs.zero).

Lemma classify_call_correct:
  forall sp e m a v fd,
  Cminor.eval_expr sge sp e m a v ->
  Genv.find_funct sge v = Some fd ->
  match classify_call (comp_unit_defmap scu) a with
  | Call_default => True
  | Call_imm id => exists b, Genv.find_symbol sge id = Some b /\ v = Vptr b Ptrofs.zero
  | Call_builtin ef => fd = External ef
  end.

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 no_ptr: forall z v b i, R z v -> v <> Vptr b i.

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_eq_fp: forall sp e m le a v fp i n,
  eval_expr tge sp e m le a v ->
  eval_expr_fp tge sp e m le a fp ->
  R i v -> 0 <= n < modulus ->
  exists fp', eval_expr_fp tge sp e m le (make_cmp_eq a n) fp' /\ FP.subset fp' fp.
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_cmp_ltu_fp: forall sp e m le a v fp i n,
  eval_expr tge sp e m le a v ->
  eval_expr_fp tge sp e m le a fp ->
  R i v -> 0 <= n < modulus ->
  exists fp', eval_expr_fp tge sp e m le (make_cmp_ltu a n) fp' /\ FP.subset fp' fp.
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_sub_fp: forall sp e m le a v fp i n,
  eval_expr tge sp e m le a v ->
  eval_expr_fp tge sp e m le a fp ->
  R i v -> 0 <= n < modulus ->
  exists fp', eval_expr_fp tge sp e m le (make_sub a n) fp' /\ FP.subset fp' fp.
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'.
Hypothesis eval_make_to_int_fp: forall sp e m le a v fp i,
  eval_expr tge sp e m le a v ->
  eval_expr_fp tge sp e m le a fp ->
  R i v ->
  exists fp', eval_expr_fp tge sp e m le (make_to_int a) fp' /\ FP.subset fp' fp.

Ltac exactcond A := eapply eval_condexpr_preserved; try exact A; try gegen; eauto with gegen.

Lemma sel_switch_correct_rec_fp:
  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 /\
  eval_exitexpr_fp tge sp e m le (sel_switch make_cmp_eq make_cmp_ltu make_sub make_to_int arg t) empfp.

Lemma sel_switch_correct_fp:
  forall dfl cases arg sp e m varg fp i t le,
  validate_switch modulus dfl cases t = true ->
  eval_expr tge sp e m le arg varg ->
  eval_expr_fp tge sp e m le arg fp ->
  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) /\
  eval_exitexpr_fp tge sp e m le
     (XElet arg (sel_switch make_cmp_eq make_cmp_ltu make_sub make_to_int O t)) fp .

End SEL_SWITCH.

Lemma sel_switch_int_correct_fp:
  forall dfl cases arg sp e m i fp t le,
  validate_switch Int.modulus dfl cases t = true ->
  eval_expr tge sp e m le arg (Vint i) ->
  eval_expr_fp tge sp e m le arg fp ->
  eval_exitexpr tge sp e m le (XElet arg (sel_switch_int O t)) (switch_target (Int.unsigned i) dfl cases) /\
  eval_exitexpr_fp tge sp e m le (XElet arg (sel_switch_int O t)) fp.

Lemma sel_switch_long_correct_fp:
  forall dfl cases arg sp e m i fp t le,
  validate_switch Int64.modulus dfl cases t = true ->
  eval_expr tge sp e m le arg (Vlong i) ->
  eval_expr_fp tge sp e m le arg fp ->
  eval_exitexpr tge sp e m le (XElet arg (sel_switch_long O t)) (switch_target (Int64.unsigned i) dfl cases) /\
  eval_exitexpr_fp tge sp e m le (XElet arg (sel_switch_long O t)) fp.


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'.

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'.

Lemma eval_binop_lessdef_fp:
  forall op v1 v1' v2 v2' v fp m m',
    eval_binop op v1 v2 m = Some v ->
    eval_binop_fp op v1 v2 m = Some fp ->
    Val.lessdef v1 v1' -> Val.lessdef v2 v2' -> Mem.extends m m' ->
    exists fp', eval_binop_fp op v1' v2' m' = Some fp' /\ FP.subset fp' fp.

Semantic preservation for instruction selection.

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

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

Lemma set_params_lessdef:
  forall il vl1 vl2,
  Val.lessdef_list vl1 vl2 ->
  env_lessdef (set_params vl1 il) (set_params vl2 il).

Lemma set_locals_lessdef:
  forall e1 e2, env_lessdef e1 e2 ->
  forall il, env_lessdef (set_locals il e1) (set_locals il e2).


Section EXPRESSIONS.
Variable hf: helper_functions.
Hypothesis HF: helper_functions_declared scu hf.

Ltac TrivEval := do 2 eexists; split;[repeat econstructor; eauto|split;[eauto|split;[repeat econstructor; eauto|TrivFP]]].
Lemma sel_expr_correct_fp:
  forall sp e m a fp,
    Cminor_local.eval_expr_fp sge sp e m a fp ->
    forall v, Cminor.eval_expr sge sp e m a v ->
    forall e' le m',
      env_lessdef e e' -> Mem.extends m m' ->
      exists v' fp',
        eval_expr tge sp e' m' le (sel_expr a) v' /\ Val.lessdef v v' /\
        eval_expr_fp tge sp e' m' le (sel_expr a) fp' /\ FP.subset fp' fp.

Lemma sel_exprlist_correct_fp:
  forall sp e m a fp,
    Cminor_local.eval_exprlist_fp sge sp e m a fp ->
    forall v, Cminor.eval_exprlist sge sp e m a v ->
    forall e' le m',
      env_lessdef e e' -> Mem.extends m m' ->
      exists v' fp', eval_exprlist tge sp e' m' le (sel_exprlist a) v' /\ Val.lessdef_list v v' /\
                eval_exprlist_fp tge sp e' m' le (sel_exprlist a) fp' /\ FP.subset fp' fp.

Lemma sel_builtin_arg_correct_fp:
  forall sp e e' m m' a v fp c,
    env_lessdef e e' -> Mem.extends m m' ->
    Cminor.eval_expr sge sp e m a v ->
    Cminor_local.eval_expr_fp sge sp e m a fp ->
  exists v' fp',
    CminorSel.eval_builtin_arg tge sp e' m' (sel_builtin_arg a c) v' /\ Val.lessdef v v' /\
    CminorSel_local.eval_builtin_arg_fp tge sp e' m' (sel_builtin_arg a c) fp' /\ FP.subset fp' fp.

Lemma sel_builtin_args_correct_fp:
  forall sp e e' m m',
    env_lessdef e e' -> Mem.extends m m' ->
    forall al fp,
      Cminor_local.eval_exprlist_fp sge sp e m al fp ->
      forall vl, Cminor.eval_exprlist sge sp e m al vl ->
            forall cl, exists vl' fpl',
                list_forall2 (CminorSel.eval_builtin_arg tge sp e' m')
                             (sel_builtin_args al cl) vl'
                /\ Val.lessdef_list vl vl'
                /\ list_forall2 (CminorSel_local.eval_builtin_arg_fp tge sp e' m')
                               (sel_builtin_args al cl) fpl'
                /\ FP.subset (fold_right (fun fph fpt => FP.union fph fpt) empfp fpl') fp.

End EXPRESSIONS.


Inductive match_cont: helper_functions -> Cminor.cont -> CminorSel.cont -> Prop :=
  | match_cont_stop: forall hf,
      match_cont hf Cminor.Kstop Kstop
  | match_cont_seq: forall hf s s' k k',
      sel_stmt (comp_unit_defmap scu) s = OK s' ->
      match_cont hf k k' ->
      match_cont hf (Cminor.Kseq s k) (Kseq s' k')
  | match_cont_block: forall hf k k',
      match_cont hf k k' ->
      match_cont hf (Cminor.Kblock k) (Kblock k')
  | match_cont_call: forall hf hf' id f sp e k f' e' k',
      helper_functions_declared scu hf ->
      sel_function (comp_unit_defmap scu) hf f = OK f' ->
      match_cont hf k k' -> env_lessdef e e' ->
      match_cont 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 hf, match_cont hf k k'.

Definition union_fp_list (fpl: list FP.t) : FP.t :=
  (fold_right (fun fph fpt => FP.union fph fpt) empfp fpl).

Inductive match_state: FP.t -> FP.t ->
                       Cminor_local.core * mem -> CminorSel_local.core * mem -> Prop :=
| match_state_intro:
    forall fp fp' hf f f' s k s' k' sp e m e' m'
      (HF: helper_functions_declared scu hf)
      (TF: sel_function (comp_unit_defmap scu) hf f = OK f')
      (TS: sel_stmt (comp_unit_defmap scu) s = OK s')
      (MC: match_cont hf k k')
      (LD: env_lessdef e e')
      (ME: Mem.extends m m')
      (FPMATCH: FP.subset fp' fp),
      match_state fp fp'
                  (Cminor_local.Core_State f s k sp e, m)
                  (Core_State f' s' k' sp e', m')
| match_callstate:
    forall fp fp' f f' args args' k k' m m'
      (TF: match_fundef scu f f')
      (MC: match_call_cont k k')
      (LD: Val.lessdef_list args args')
      (ME: Mem.extends m m')
      (FPMATCH: FP.subset fp' fp),
      match_state fp fp'
                  (Cminor_local.Core_Callstate f args k, m)
                  (Core_Callstate f' args' k', m')
| match_returnstate:
    forall fp fp' v v' k k' m m'
      (MC: match_call_cont k k')
      (LD: Val.lessdef v v')
      (ME: Mem.extends m m')
      (FPMATCH: FP.subset fp' fp),
      match_state fp fp'
                  (Cminor_local.Core_Returnstate v k, m)
                  (Core_Returnstate v' k', m')

| match_builtin_1:
    forall fp fp' fpl hf ef args args' optid f sp e k m al f' e' k' m'
      (TF: sel_function (comp_unit_defmap scu) hf f = OK f')
      (MC: match_cont 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')
      (INLINE: ef_inline ef = true)
      (EAFP: list_forall2 (CminorSel_local.eval_builtin_arg_fp tge sp e' m') al fpl)
      (FPMATCH: FP.subset (FP.union fp' (union_fp_list fpl)) fp),
      match_state fp fp'
                  (Cminor_local.Core_Callstate (External ef) args (Cminor.Kcall optid f sp e k), m)
                  (Core_State f' (Sbuiltin (sel_builtin_res optid) ef al) k' sp e', m').

Definition MS b n mu fp fp' cm cm': Prop :=
  match_state fp fp' cm cm' /\
  let (c, m) := cm in
  let (c', m') := cm' in
  (forall b, Bset.belongsto (Injections.SharedSrc mu) b -> Mem.valid_block m b) /\
  (forall b, Bset.belongsto (Injections.SharedTgt mu) b -> Mem.valid_block m' b) /\
  (proper_mu sge tge inject_id mu) /\
  (MemClosures_local.unmapped_closed mu m m') /\
  match c with
  | Cminor_local.Core_State _ _ _ _ _ => n = 1%nat /\ b = true
  | Cminor_local.Core_Callstate _ _ _ => n = 0%nat
  | Cminor_local.Core_Returnstate _ _ => n = 2%nat
  end.

Ltac invMS :=
  match goal with
  | H: MS _ _ _ _ _ ?cm1 ?cm2 |- _ =>
    destruct cm1 as [sc Hm]; destruct cm2 as [tc Lm];
    unfold MS in H; simpl in H;
    destruct H as [MS [SVALID [TVALID [AGMU [RCPRESV INDEX]]]]]
  | H: MS _ _ _ _ _ ?cm1 ?cm2 |- _ =>
    unfold MS in H; simpl in H;
    destruct H as [MS [SVALID [TVALID [AGMU [RCPRESV INDEX]]]]]
  end.


Remark call_cont_commut:
  forall hf k k', match_cont hf k k' -> match_call_cont (Cminor.call_cont k) (call_cont k').

Remark match_is_call_cont:
  forall hf k k', match_cont hf k k' -> Cminor.is_call_cont k -> match_call_cont k k'.

Remark match_call_cont_cont:
  forall k k', match_call_cont k k' -> exists hf, match_cont hf k k'.

Remark find_label_commut:
  forall hf lbl s k s' k',
  match_cont hf k k' ->
  sel_stmt (comp_unit_defmap scu) 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 (comp_unit_defmap scu) s1 = OK s1' /\ match_cont hf k1 k1'
  | _, _ => False
  end.


Ltac Ex_index :=
  match goal with
  | |- context[Cminor_local.Core_State] => exists 1%nat
  | |- context[Cminor_local.Core_Callstate] => exists 0%nat
  | |- context[Cminor_local.Core_Returnstate] => exists 2%nat
  end.

Ltac resolvfp:=
  match goal with
  | |- context[FP.union _ empfp] => rewrite FP.fp_union_emp; resolvfp
  | |- context[FP.union empfp _] => rewrite FP.emp_union_fp; resolvfp
  | H: Some _ = Some _ |- _ => inv H; resolvfp
  | H: FP.subset ?fp1' ?fp1 |- Injections.FPMatch' ?mu (FP.union ?fp1 _) (FP.union ?fp1' _) =>
    eapply Injections.fp_match_union'; resolvfp
  | H: FP.subset ?fp1' ?fp1 |- FP.subset (FP.union ?fp1' _) (FP.union ?fp1 _) =>
    eapply FP.subset_parallel_union; resolvfp
  | H: FP.subset ?fp1' ?fp1 |- FP.subset (FP.union (FP.union ?fp1' _) _) (FP.union (FP.union ?fp1 _) _)=>
    eapply FP.subset_parallel_union; resolvfp
  | H: FP.subset ?fp ?fp' |- FP.subset ?fp (FP.union ?fp1 ?fp') =>
    rewrite FP.union_comm_eq; resolvfp
  | H: FP.subset ?fp ?fp' |- FP.subset ?fp (FP.union ?fp' _) =>
    apply FP.subset_union_subset; auto
  | |- Injections.FPMatch' _ _ empfp => apply Injections.fp_match_emp'
  | H: FP.subset ?fp1 ?fp2 |- Injections.FPMatch' _ ?fp2 ?fp1 =>
    apply Injections.fp_match_subset_T' with fp2; try exact H; resolvfp
  | H: FP.subset ?fp2 ?fp1 |- Injections.FPMatch' _ (FP.union ?fp1 _) ?fp2 =>
    apply Injections.fp_match_union_S'; resolvfp
  | |- FP.subset ?fp ?fp => apply FP.subset_refl
  | H: proper_mu _ _ _ _ |- Injections.FPMatch' _ ?fp ?fp => inv H; eapply fp_match_id; eauto
  | _ => idtac
  end.

Ltac eresolvfp:= resolvfp; eauto.

Ltac resvalid:=
  match goal with
  | H: (forall x, Bset.belongsto ?S x -> Mem.valid_block ?m1 x), H': Mem.free ?m1 _ _ _ = Some ?m2
    |- (forall x, Bset.belongsto ?S x -> Mem.valid_block ?m2 x)
    => let X := fresh in
      intros ? X; apply H in X; eapply Mem.valid_block_free_1; eauto
  | H: (forall x, Bset.belongsto ?S x -> Mem.valid_block ?m1 x), H': Mem.alloc ?m1 _ _ = (?m2,_)
    |- (forall x, Bset.belongsto ?S x -> Mem.valid_block ?m2 x)
    => let X := fresh in
      intros ? X; apply H in X; eapply Mem.valid_block_alloc; eauto
  | H: (forall x, Bset.belongsto ?S x -> Mem.valid_block ?m1 x), H': Mem.store _ ?m1 _ _ _ = Some ?m2
    |- (forall x, Bset.belongsto ?S x -> Mem.valid_block ?m2 x)
    => let X := fresh in
      intros ? X; apply H in X; eapply Mem.store_valid_block_1; eauto
  | H1: Mem.store _ ?m1 _ _ _ = Some ?m2,
        H2: Mem.store _ ?m1' _ _ _ = Some ?m2',
            H3: proper_mu _ _ _ _
    |- MemClosures_local.unmapped_closed _ ?m2 ?m2'
    => inv H3; eapply MemClosures_local.store_val_inject_unmapped_closed_preserved;
      try (rewrite Z.add_0_r); try eassumption;
      try (compute; eauto; fail); try omega
  | H1: Mem.free ?m1 _ _ _ = Some ?m2,
        H2: Mem.free ?m1' _ _ _ = Some ?m2',
            H3: proper_mu _ _ _ _
    |- MemClosures_local.unmapped_closed _ ?m2 ?m2'
    => inv H3; eapply MemClosures_local.free_inject_unmapped_closed_preserved; eauto;
      try (rewrite Z.add_0_r); try eassumption;
      try (compute; eauto; fail); try omega
  | H1: Mem.alloc ?m1 _ _ = (?m2, _),
        H2: Mem.alloc ?m1' _ _ = (?m2', _),
            H3: proper_mu _ _ _ _
    |- MemClosures_local.unmapped_closed _ ?m2 ?m2'
    => inv H3; eapply MemClosures_local.unchanged_on_unmapped_closed_preserved; eauto;
      try (eapply Mem.alloc_unchanged_on; eauto; fail)
  | _ => idtac
  end.

Ltac Right := right; Ex_index; do 3 eexists; split; [apply plus_one|resolvfp].
Ltac FP:= match goal with |- ?P /\ _ => assert P; [eresolvfp| try (split;[auto; fail|])] end.
Ltac Left := left; Ex_index; split; [auto|eresolvfp].
Ltac splitMS :=
  split;
  [econstructor; eresolvfp |split;
   [try resvalid; auto |split; [try resvalid; auto
                         |split; [auto| split; try resvalid; eauto]]]].

Theorem TRANSF_local_ldsim:
  @local_ldsim Cminor_IS CminorSel_IS sge tge sge tge.

End PRESERVATION.

Theorem transf_local_ldsim:
  forall scu tcu,
    selection.transf_program scu = OK tcu ->
    forall sge sG tge tG,
      init_genv_local Cminor_IS scu sge sG ->
      init_genv_local CminorSel_IS tcu tge tG ->
      Genv.genv_next sge = Genv.genv_next tge ->
      local_ldsim sG tG sge tge.