Module SimplLocalsDummyproof


Semantic preservation for the SimplLocals pass.

Require Import FSets.
Require FSetAVL.
Require Import Coqlib.
Require Import Errors.
Require Import Ordered.
Require Import AST.
Require Import Maps.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Globalenvs.
Require Import Events.
Require Import Smallstep.
Require Import Ctypes.
Require Import Cop.
Require Import Clight.
Require Import SimplLocalsDummy.

Require Import Values_symbolictype.
Require Import Values_symbolic.
Require Import Normalise.
Require Import NormaliseSpec.
Require Import Memory.
Require Import Equivalences.
Require Import ClightEquivalences.

Section PRESERVATION.

Variable prog: program.
Variable tprog: program.
Hypothesis TRANSF: transf_program prog = OK tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Lemma symbols_preserved:
  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof.
  exact (Genv.find_symbol_transf_partial _ _ TRANSF).
Qed.

Lemma varinfo_preserved:
  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
Proof.
  exact (Genv.find_var_info_transf_partial _ _ TRANSF).
Qed.

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

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

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

Matching between environments before and after
 
Record match_envs (e: env) (le: temp_env) (m: mem) (lo hi: block)
       (tle: temp_env) : Prop :=
  mk_match_envs {
      me_temps:
        forall id v,
          le!id = Some v ->
          (exists tv, tle!id = Some tv /\ same_eval v tv);
      me_inj:
        forall id1 b1 ty1 id2 b2 ty2,
          e!id1 = Some(b1, ty1) -> e!id2 = Some(b2, ty2) ->
          id1 <> id2 -> b1 <> b2;
      me_range:
        forall id b ty, e!id = Some(b, ty) -> Ple lo b /\ Plt b hi;
      me_incr:
        Ple lo hi;
      me_bounds:
        forall id b ty,
          e ! id = Some (b,ty) ->
          Mem.bounds_of_block m b = (0, sizeof ty)
    }.

Invariance by change of memory and injection

Lemma match_envs_invariant:
  forall e le m lo hi tle m',
  match_envs e le m lo hi tle ->
  (forall b, Ple lo b /\ Plt b hi -> Mem.bounds_of_block m b = Mem.bounds_of_block m' b) ->
  match_envs e le m' lo hi tle.
Proof.
  intros until m'; intros ME SB.
  destruct ME; constructor; eauto.
  intros; auto. rewrite <- SB. eauto.
  eapply me_range0. eauto.
Qed.

Invariance by external call

Lemma match_envs_extcall:
  forall e le m lo hi tle tm m',
  match_envs e le m lo hi tle ->
  Mem.unchanged_on (fun b _ => Ple lo b /\ Plt b hi) m m' ->
  Ple hi (Mem.nextblock m) -> Ple hi (Mem.nextblock tm) ->
  (forall b, Mem.bounds_of_block m b = Mem.bounds_of_block m' b) ->
  match_envs e le m' lo hi tle.
Proof.
  intros. eapply match_envs_invariant; eauto.
Qed.

Correctness of make_cast

Lemma make_cast_correct:
  forall e le m a v1 tto v2,
  eval_expr tge e le m a v1 ->
  sem_cast_expr v1 (typeof a) tto = Some v2 ->
  eval_expr tge e le m (make_cast a tto) v2.
Proof.
  intros.
  econstructor; eauto.
Qed.

Preservation by assignment to a temporary

Lemma match_envs_set_temp:
  forall e le m lo hi tle id v tv,
  match_envs e le m lo hi tle ->
  same_eval v tv ->
  match_envs e (PTree.set id v le) m lo hi (PTree.set id tv tle).
Proof.
  intros.
  destruct H. constructor; eauto; intros.
  rewrite PTree.gsspec in *. destruct (peq id0 id).
  inv H. exists tv; split; auto.
  eapply me_temps0; eauto.
Qed.

Lemma match_envs_set_opttemp:
  forall e le m lo hi tle optid v tv,
  match_envs e le m lo hi tle ->
  same_eval v tv ->
  match_envs e (set_opttemp optid v le) m lo hi (set_opttemp optid tv tle).
Proof.
  intros. unfold set_opttemp. destruct optid; simpl in *.
  eapply match_envs_set_temp; eauto.
  auto.
Qed.

Extensionality with respect to temporaries

Lemma match_envs_temps_exten:
  forall e le m lo hi tle tle',
  match_envs e le m lo hi tle ->
  (forall id, tle'!id = tle!id) ->
  match_envs e le m lo hi tle'.
Proof.
  intros. destruct H. constructor; auto; intros.
  rewrite H0. eauto.
Qed.

Invariance by assignment to an irrelevant temporary

Lemma match_envs_change_temp:
  forall e le m lo hi tle id v,
  match_envs e le m lo hi tle ->
  le!id = None ->
  match_envs e le m lo hi (PTree.set id v tle).
Proof.
  intros. destruct H. constructor; auto; intros.
  rewrite PTree.gso. eauto. congruence.
Qed.

Allocation and initialization of parameters

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

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

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

Lemma alloc_variables_bounds:
  forall e m vars e' m',
    alloc_variables e m vars e' m' ->
    (forall id b ty, e!id = Some (b, ty) -> Mem.valid_block m b) ->
    (forall id ty b, e!id = Some (b,ty) -> Mem.bounds_of_block m b = (0, sizeof ty)) ->
    forall id ty b,
      e'!id = Some (b,ty) ->
      Mem.bounds_of_block m' b = (0, sizeof ty).
Proof.
  induction 1; simpl; intros.
  - eapply H0; eauto.
  - Alloc.trim IHalloc_variables.
    {
      intros id1 b0 ty1; rewrite PTree.gsspec.
      destruct (peq id1 id); subst.
      intro A; inv A.
      eapply Mem.valid_new_block; eauto.
      intro.
      apply H1 in H4.
      eapply Mem.valid_block_alloc; eauto.
    }
    Alloc.trim IHalloc_variables.
    {
      intros id1 ty1 b0; rewrite PTree.gsspec.
      destruct (peq id1 id); subst.
      intro A; inv A.
      eapply Mem.bounds_of_block_alloc; eauto.
      intro.
      destruct (peq b1 b0). subst.
      apply Mem.fresh_block_alloc in H.
      apply H1 in H4. congruence.
      erewrite <- Mem.bounds_of_block_alloc_other; eauto.
    }
    eapply IHalloc_variables; eauto.
Qed.

Lemma match_alloc_variables:
  forall e m vars e' m'
         (AV: alloc_variables e m vars e' m')
         tm
         (lnr: list_norepet (var_names vars))
         (MINJ: mem_equiv m tm),
  exists tm',
      alloc_variables e tm vars e' tm'
  /\ mem_equiv m' tm'
  /\ (forall id ty, In (id, ty) vars ->
      exists b,
        e'!id = Some(b, ty))
  /\ (forall id, ~In id (var_names vars) -> e'!id = e!id).
Proof.
  induction 1; intros.
  -
    exists tm; simpl.
    repeat (split; auto). constructor.
    tauto.
  -
    simpl in lnr. inv lnr. simpl.
    destruct (alloc_mem_equiv _ _ _ _ _ H _ MINJ) as [tm' [A B]].
    exploit IHAV; eauto.
    intros [tm'0 [C [D [E F]]]].
    exists tm'0.
    repeat (split; eauto).
    + econstructor; eauto.
    + intros. destruct (ident_eq id0 id).
      *
        subst id0.
        assert (ty0 = ty).
        destruct H0. congruence. elim H2. unfold var_names. change id with (fst (id, ty0)). apply in_map; auto.
        subst ty0.
        exploit F; eauto.
        intros X. rewrite X.
        rewrite PTree.gss; eexists; eauto.
      *
        exploit (E id0 ty0). destruct H0. congruence. auto. auto.
    + intros. exploit (F id0). tauto. intros X. rewrite X; apply PTree.gso; intuition.
Qed.

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


Lemma alloc_variables_bound:
  forall e m vars e' m',
  alloc_variables e m vars e' m' ->
  forall b,
    Plt b (Mem.nextblock m) ->
    Mem.bounds_of_block m b = Mem.bounds_of_block m' b.
Proof.
  induction 1; intros.
  auto.
  rewrite <- IHalloc_variables; auto.
  destruct (peq b b1); subst.
  apply Mem.alloc_result in H. subst; xomega.
  eapply Mem.bounds_of_block_alloc_other in H; eauto.
  rewrite (Mem.nextblock_alloc _ _ _ _ _ H).
  xomega.
Qed.




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

 

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

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

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

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

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

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

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

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


Lemma vars_and_temps_properties:
  forall params vars temps,
  list_norepet (var_names params ++ var_names vars) ->
  list_disjoint (var_names params) (var_names temps) ->
  list_norepet (var_names params)
  /\ list_norepet (var_names (params ++ vars))
  /\ list_disjoint (var_names params) (var_names temps).
Proof.
  intros. rewrite list_norepet_app in H. destruct H as [A [B C]].
  split. auto.
  split. unfold var_names. rewrite map_app. apply list_norepet_append; assumption.
  auto.
Qed.

Lemma alloc_variables_preserves_bounds:
  forall e m vars e' m'
         (A: alloc_variables e m vars e' m')
         tm te te' tm'
         (TA: alloc_variables te tm vars te' tm')
         (sb: forall b : block, Mem.bounds_of_block m b = Mem.bounds_of_block tm b)
         (nb: Mem.nextblock m = Mem.nextblock tm),
   forall b : block, Mem.bounds_of_block m' b = Mem.bounds_of_block tm' b.
Proof.
  induction 1; simpl; intros; auto.
  inv TA. auto.
  inv TA.
  generalize (Mem.alloc_result _ _ _ _ _ H7).
  generalize (Mem.alloc_result _ _ _ _ _ H).
  intros; subst.
  rewrite nb in *.
  eapply IHA in H8; eauto.
  intros. destruct (peq b0 (Mem.nextblock tm)); subst; auto.
  + rewrite (Mem.bounds_of_block_alloc _ _ _ _ _ H).
    rewrite (Mem.bounds_of_block_alloc _ _ _ _ _ H7). auto.
  + rewrite <- (Mem.bounds_of_block_alloc_other _ _ _ _ _ H); auto.
    rewrite <- (Mem.bounds_of_block_alloc_other _ _ _ _ _ H7); auto.
  + apply Mem.nextblock_alloc in H7.
    apply Mem.nextblock_alloc in H. congruence.
Qed.

Theorem match_envs_alloc_variables:
  forall m vars e m' temps tm
         (AV: alloc_variables empty_env m vars e m')
         (lnr: list_norepet (var_names vars))
         (MINK: mem_equiv m tm),
  exists tm',
    alloc_variables empty_env tm vars e tm'
      /\ match_envs e (create_undef_temps temps) m'
                    (Mem.nextblock m) (Mem.nextblock m')
                    (create_undef_temps temps)
      /\ mem_equiv m' tm'.
Proof.
  intros.
  exploit (match_alloc_variables); eauto.
  intros [tm' [A [B [C D]]]].
  (exists tm').
  split. auto. split; auto.
  constructor; intros; eauto.
  - eexists; split; try reflexivity; auto.
  -
    eapply alloc_variables_injective. eexact AV.
    rewrite PTree.gempty. congruence.
    intros. rewrite PTree.gempty in H2. congruence.
    eauto. eauto. auto.
  -
    exploit alloc_variables_range. eexact AV. eauto.
    rewrite PTree.gempty. intuition congruence.
  - eapply alloc_variables_nextblock; eauto.
  - eapply alloc_variables_bounds in H; eauto.
    intros id0 b0 ty0. rewrite PTree.gempty. congruence.
    intros id0 ty0 b0. rewrite PTree.gempty. congruence.
Qed.

Lemma assign_loc_inject:
  forall ty m addr addr' v m' tm v',
    assign_loc ty m addr v m' ->
    same_eval addr addr' ->
    same_eval v v' ->
    mem_equiv m tm ->
    exists tm',
      assign_loc ty tm addr' v' tm'
      /\ mem_equiv m' tm'.
Proof.
  intros t m addr addr' v m' tm v' AL SE1 SE2 ME.
  inv AL.
  - eapply storev_mem_equiv in H0; eauto.
    destruct H0 as [m2' [ST B]].
    eapply storev_val_equiv in ST; eauto.
    destruct ST as [m2'0 [ST C]].
    exists m2'0; split; eauto.
    econstructor; eauto.
    unfold Mem.storev.
    rewrite <- (same_eval_eqm _ _ _ _ SE1).
    auto. etransitivity; eauto.
  -
    eapply mem_equiv_loadbytes in H3; eauto.
    eapply storebytes_mem_equiv in H4; eauto.
    destruct H3 as [v'0 [A B]].
    destruct H4 as [m0 [C D]].
    eapply (storebytes_val_equiv) in C; eauto.
    destruct C as [m1 [E F]].
    exists m1; split; auto.
    eapply assign_loc_copy with (ofs':=ofs') (ofs:=ofs); eauto.
    rewrite <- H5.
    rewrite (same_eval_eqm _ _ _ _ SE2); eauto.
    apply mem_equiv_norm; symmetry; eauto.
    rewrite <- H6.
    rewrite (same_eval_eqm _ _ _ _ SE1); auto.
    apply mem_equiv_norm; symmetry; eauto.
    rewrite D; rewrite F; reflexivity.
Qed.

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

Lemma assign_loc_nextblock:
  forall ty m addr v m',
  assign_loc ty m addr v m' -> Mem.nextblock m' = Mem.nextblock m.
Proof.
  induction 1.
  unfold Mem.storev in H0; revert H0; destr_cond_match; try discriminate.
  eapply Mem.nextblock_store; eauto.
  eapply Mem.nextblock_storebytes; eauto.
Qed.

Lemma assign_loc_bounds:
  forall ty m addr v m' b,
    assign_loc ty m addr v m' ->
    Mem.bounds_of_block m b = Mem.bounds_of_block m' b.
Proof.
  intros ty m addr v m' b AL; inv AL.
  - unfold Mem.storev in H0; revert H0; destr_cond_match; try discriminate.
    intros; eapply Mem.bounds_of_block_store; eauto.
  - eapply Mem.bounds_of_block_storebytes; eauto.
Qed.


Inductive casted_list : list expr_sym -> list type -> Prop :=
  casted_list_nil: casted_list nil nil
| casted_list_cons:
    forall el tl e t e',
      sem_cast_expr e t t = Some e' ->
      same_eval e e' ->
      casted_list el tl ->
      casted_list (e::el) (t::tl).

Lemma assign_loc_equiv:
  forall ty m e1 e2 m' e2',
    assign_loc ty m e1 e2 m' ->
    same_eval e2 e2' ->
    exists m2',
      assign_loc ty m e1 e2' m2' /\
      mem_equiv m' m2'.
Proof.
  intros ty m e1 e2 m' e2' AL SE; inv AL.
  - eapply storev_val_equiv in H0; eauto.
    destruct H0 as [m2' [A B]].
    eexists; split; eauto.
    eapply assign_loc_value; eauto.
  - erewrite same_eval_eqm in H5; eauto.
    eexists; split.
    eapply (assign_loc_copy ty m e1 b ofs b' ofs' bytes m'); eauto.
    reflexivity.
Qed.


Lemma bpt_set_se:
  forall bl params t1 t2 tle',
    temp_env_equiv t1 t2 ->
    bind_parameter_temps params bl t1 = Some tle' ->
    exists tle'0,
      bind_parameter_temps params bl t2 = Some tle'0 /\
      temp_env_equiv tle' tle'0.
Proof.
  induction bl; destruct params; simpl; intros; try destruct p; try inv H0.
  - eexists; split; auto.
  - eapply IHbl; eauto.
    intro.
    rewrite ! PTree.gsspec.
    destruct (peq i0 i); subst; auto.
    reflexivity.
    apply H.
Qed.


Lemma set_se:
  forall t id b v,
    same_eval b v ->
    temp_env_equiv (PTree.set id b t) (PTree.set id v t).
Proof.
  intros t id b v SE i.
  rewrite ! PTree.gsspec.
  destruct (peq i id); subst; auto.
  destr_cond_match; auto; reflexivity.
Qed.
 

Lemma temp_env_equiv_refl:
  forall t,
    temp_env_equiv t t.
Proof.
  red; intros.
  destr_cond_match; auto; reflexivity.
Qed.




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

Lemma norm_ptr_in_bound:
  forall m b ofs,
    NormaliseSpec.in_bound (Int.unsigned ofs) (Mem.bounds_of_block m b) ->
    Mem.mem_norm m (Eval (Eptr b ofs)) Ptr = Vptr b ofs.
Proof.
  intros; unfold Mem.mem_norm.
    destruct (Mem.concrete_mem m).
    rewrite (Normalise.normalise_ptr_ptr _ _ _ H0 b ofs); auto.
Qed.


Lemma norm_ptr_zero:
  forall m b,
    Mem.mem_norm m (Eval (Eptr b Int.zero)) Ptr = Vptr b Int.zero \/
    Mem.mem_norm m (Eval (Eptr b Int.zero)) Ptr = Vundef.
Proof.
  intros.
  destruct (in_bound_dec (Mem.bounds_of_block m b) 0).
  left; apply norm_ptr_in_bound. auto.
  destruct (normalise_ptr_type (Mem.bounds_of_block m) (Mem.nat_mask m) (Eval (Eptr b Int.zero))); auto.
  destruct H0 as [b0 [ofs A]].
  apply Mem.norm_ptr_same_eval in A; intuition congruence.
Qed.


Lemma bind_parameters_load:
  forall e chunk b ofs,
  (forall id b' ty, e!id = Some(b', ty) -> b <> b') ->
  forall m params args m',
  bind_parameters e m params args m' ->
  Mem.load chunk m' b ofs = Mem.load chunk m b ofs.
Proof.
  induction 2.
  auto.
  rewrite IHbind_parameters.
  assert (b <> b0) by eauto.
  inv H1.
  unfold Mem.storev in H5; revert H5; destr_cond_match; try discriminate.
  intro. eapply Mem.load_store_other; eauto.
  destruct (norm_ptr_zero m b0); try congruence.
  rewrite Heqv in H1; inv H1.
  auto.
  eapply Mem.load_storebytes_other; eauto.
  destruct (norm_ptr_zero m b0); try congruence.
  rewrite H11 in H1; inv H1.
  auto.
Qed.


Lemma bind_parameters_bound:
  forall e b,
  (forall id b' ty, e!id = Some(b', ty) -> b <> b') ->
  forall m params args m',
  bind_parameters e m params args m' ->
  Mem.bounds_of_block m' b = Mem.bounds_of_block m b.
Proof.
  induction 2.
  auto.
  rewrite IHbind_parameters.
  assert (b <> b0) by eauto.
  symmetry; eapply assign_loc_bounds; eauto.
Qed.



Freeing of local variables

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

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

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

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

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



Lemma free_contents:
  forall m b lo hi m',
    Mem.free m b lo hi = Some m' ->
    Mem.mem_contents m = Mem.mem_contents m'.
Proof.
  intros m b lo hi m' F.
  Transparent Mem.free.
  unfold Mem.free in F.
  revert F; destr_cond_match; try discriminate.
  intro A; inv A. simpl; auto.
Qed.


Theorem match_envs_free_blocks:
  forall e m m' tm,
    mem_equiv m tm ->
    Mem.free_list m (blocks_of_env e) = Some m' ->
    exists tm',
      Mem.free_list tm (blocks_of_env e) = Some tm'
      /\ mem_equiv m' tm'.
Proof.
  intros.
  eapply free_list_mem_equiv; eauto.
Qed.


Matching global environments

Inductive match_globalenvs (bound: block): Prop :=
  | mk_match_globalenvs
      (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> Plt b bound)
      (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> Plt b bound)
      (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> Plt b bound).

Evaluation of expressions

Section EVAL_EXPR.

Variables e : env.
Variables le tle: temp_env.
Variables m tm: mem.
Variables lo hi : block.
Hypothesis MATCH: match_envs e le m lo hi tle.
Hypothesis MEMINJ: mem_equiv m tm.
Hypothesis GLOB: exists bound, match_globalenvs bound.

Lemma deref_loc_se:
  forall ty addr v addr',
    deref_loc ty m addr v ->
    same_eval addr addr' ->
    exists tv,
      deref_loc ty tm addr' tv
      /\ same_eval v tv.
Proof.
  intros ty addr v addr' DL SE; inv DL.
  - destruct (loadv_mem_equiv _ _ _ _ _ MEMINJ H0) as [v' [A B]].
    clear H0.
    exists v'; split; try reflexivity; eauto.
    econstructor; eauto.
    unfold Mem.loadv.
    rewrite <- (same_eval_eqm _ _ _ _ SE). auto.
  - eexists; split; eauto.
    eapply deref_loc_reference; auto.
  - eexists; split; eauto.
    eapply deref_loc_copy; auto.
Qed.

Lemma eval_simpl_expr:
  forall a v,
  eval_expr ge e le m a v ->
  exists tv, eval_expr tge e tle tm a tv /\ same_eval v tv

with eval_simpl_lvalue:
  forall a addr,
  eval_lvalue ge e le m a addr ->
  exists addr',
    eval_lvalue tge e tle tm a addr' /\
    same_eval addr addr'.

Proof.
  destruct 1; simpl; intros.
  - eexists; split; eauto; repeat (constructor; simpl; auto).
  - eexists; split; eauto; repeat (constructor; simpl; auto).
  - eexists; split; eauto; repeat (constructor; simpl; auto).
  - eexists; split; eauto; repeat (constructor; simpl; auto).
  - exploit me_temps; eauto. intros [tv [A B]].
    exists tv; split; auto. constructor; auto.
  - exploit eval_simpl_lvalue; eauto.
    intros [addr' [A B]].
    (exists addr'); split; auto. constructor; auto.
  -
    exploit eval_simpl_expr; eauto. intros [tv1 [A B]].
    generalize (sem_unary_operation_expr_se op (typeof a) _ _ B). intro C.
    eexists; split; eauto. econstructor; eauto.
    subst; auto.
  -
    exploit eval_simpl_expr. eexact H. intros [tv1 [A B]].
    exploit eval_simpl_expr. eexact H0. intros [tv2 [C D]].
    generalize (sem_binary_operation_expr_se
                m op (typeof a1) (typeof a2) _ _ _ _ B D).
    rewrite H1. destr_cond_match; try tauto. intro E.
    eexists; split; eauto. econstructor; eauto.
  -
    exploit eval_simpl_expr; eauto. intros [tv1 [A B]].
    generalize (sem_cast_expr_se (typeof a) ty _ _ B). rewrite H0.
    destr_cond_match; try tauto; intro E.
    eexists ; split; eauto. econstructor. eauto. eauto.
  -
  exploit eval_simpl_lvalue; eauto. intros [addr' [A B]].
  exploit deref_loc_se; eauto. intros [tv [C D]].
  eexists tv; split; eauto. econstructor. eexact A. eauto.

-
  destruct 1; simpl; intros.
  +
    eexists; split; eauto.
    econstructor; eauto. reflexivity.
  +
    eexists; split; eauto.
    rewrite <- symbols_preserved in H0.
    eapply eval_Evar_global; eauto.
    reflexivity.
  +
    exploit eval_simpl_expr; eauto. intros [tv [A B]].
    eexists; split.
    econstructor; simpl; eauto. auto.
  +
    exploit eval_simpl_expr; eauto. intros [tv [A B]].
    eexists; split.
    econstructor; eauto. apply binop_same_eval; auto. reflexivity.
  +
    exploit eval_simpl_expr; eauto. intros [tv [A B]].
    eexists; split.
    eapply eval_Efield_union; eauto. auto.
Qed.

Lemma eval_simpl_exprlist:
  forall al tyl vl,
  eval_exprlist ge e le m al tyl vl ->
  exists tvl,
    eval_exprlist tge e tle tm al tyl tvl
    /\ list_forall2 same_eval vl tvl.
Proof.
  induction 1; simpl; intros.
  econstructor; split. constructor. constructor.
  exploit eval_simpl_expr; eauto. intros [tv1 [A B]].
  generalize (sem_cast_expr_se (typeof a) ty _ _ B); rewrite H0.
  destr_cond_match; try tauto; intro C.
  destruct IHeval_exprlist as [tvl [E F]].
  exists (e0 :: tvl); split. econstructor; eauto.
  econstructor; eauto.
Qed.

End EVAL_EXPR.

Matching continuations

Inductive match_cont : cont -> cont -> mem -> block -> block -> Prop :=
  | match_Kstop: forall m bound tbound hi,
      match_globalenvs hi -> Ple hi bound -> Ple hi tbound ->
      match_cont Kstop Kstop m bound tbound
  | match_Kseq: forall s k tk m bound tbound,
      match_cont k tk m bound tbound ->
      match_cont (Kseq s k) (Kseq s tk) m bound tbound
  | match_Kloop1: forall s1 s2 k tk m bound tbound,
      match_cont k tk m bound tbound ->
      match_cont (Kloop1 s1 s2 k) (Kloop1 s1 s2 tk) m bound tbound
  | match_Kloop2: forall s1 s2 k tk m bound tbound,
      match_cont k tk m bound tbound ->
      match_cont (Kloop2 s1 s2 k) (Kloop2 s1 s2 tk) m bound tbound
  | match_Kswitch: forall k tk m bound tbound,
      match_cont k tk m bound tbound ->
      match_cont (Kswitch k) (Kswitch tk) m bound tbound
  | match_Kcall: forall optid fn e le k tfn tle tk m hi thi lo bound tbound,
      transf_function fn = OK tfn ->
      match_envs e le m lo hi tle ->
      match_cont k tk m lo lo ->
      Ple hi bound -> Ple thi tbound ->
      match_cont (Kcall optid fn e le k)
                 (Kcall optid tfn e tle tk) m bound tbound.

Invariance property by change of memory and injection

Lemma match_cont_invariant:
  forall m' k tk m bound tbound,
  match_cont k tk m bound tbound ->
  (forall b, Plt b bound -> Mem.bounds_of_block m b = Mem.bounds_of_block m' b) ->
  match_cont k tk m' bound tbound.
Proof.
  induction 1; simpl; intros ME; econstructor; eauto.
  eapply match_envs_invariant; eauto.
  intros. eapply ME; eauto. xomega.
  eapply IHmatch_cont; eauto.
  intros; eapply ME; eauto. inv H0; xomega.
Qed.

Invariance by assignment to location "above"

Lemma match_cont_assign_loc:
  forall k tk m bound tbound ty addr loc ofs v m',
  match_cont k tk m bound tbound ->
  assign_loc ty m addr v m' ->
  Mem.mem_norm m addr Ptr = Vptr loc ofs ->
  Ple bound loc ->
  match_cont k tk m' bound tbound.
Proof.
  intros. eapply match_cont_invariant; eauto.
  intros; eapply assign_loc_bounds; eauto.
Qed.

Invariance by external calls


Invariance by change of bounds

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

match_cont and call continuations.

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

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

match_cont and freeing of environment blocks

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

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

Lemma match_cont_free_env:
  forall e le m lo hi tle tm k tk m' tm',
  match_envs e le m lo hi tle ->
  match_cont k tk m lo lo ->
  Ple hi (Mem.nextblock m) ->
  Mem.free_list m (blocks_of_env e) = Some m' ->
  Mem.free_list tm (blocks_of_env e) = Some tm' ->
  mem_equiv m tm ->
  match_cont k tk m' (Mem.nextblock m') (Mem.nextblock tm').
Proof.
  intros. apply match_cont_incr_bounds with lo lo.
  eapply match_cont_invariant; eauto.
  intros.
  symmetry. eapply Mem.bounds_freelist; eauto.
  intro A. apply in_map_iff in A.
  destruct A as [[[b' lo'] hi'] [A B]]. simpl in *. subst.
  unfold blocks_of_env in B.
  apply in_map_iff in B.
  destruct B as [[b' [l h]] [B C]]. simpl in *.
  inv B.
  apply PTree.elements_complete in C.
  eapply me_range in C; eauto. destruct C; xomega.
  rewrite (free_list_nextblock _ _ _ H2). inv H; xomega.
  rewrite (free_list_nextblock _ _ _ H3). inv H. eapply Ple_trans; eauto.
  inv H4. rewrite <- mem_nextblock_eq; auto.
Qed.

Matching of global environments

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

Hint Resolve match_cont_globalenv: compat.

Lemma match_cont_find_funct:
  forall k tk m tm bound tbound vf fd tvf,
    match_cont k tk m bound tbound ->
    Genv.find_funct m ge vf = Some fd ->
    same_eval vf tvf ->
    mem_equiv m tm ->
  exists tfd, Genv.find_funct tm tge tvf = Some tfd /\ transf_fundef fd = OK tfd.
Proof.
  intros. exploit match_cont_globalenv; eauto. intros [bound1 MG]. destruct MG.
  unfold Genv.find_funct in *.
  revert H0; destr_cond_match; try discriminate.
  destr_cond_match; try discriminate.
  intro. subst.
  setoid_rewrite <- (same_eval_eqm tm _ _ _ H1).
  rewrite <- (mem_equiv_norm _ _ _ _ H2).
  setoid_rewrite Heqv. rewrite pred_dec_true; auto.
  apply function_ptr_translated; auto.
Qed.

Relating execution states

Fixpoint type_list_of_typelist (tl: typelist) : list type :=
  match tl with
      Tnil => nil
    | Tcons a b => a::(type_list_of_typelist b)
  end.

Inductive match_states: state -> state -> Prop :=
  | match_regular_states:
      forall f s k e le m tf tk tle tm lo hi
             (TRF: transf_function f = OK tf)
             (MENV: match_envs e le m lo hi tle)
             (MCONT: match_cont k tk m lo lo)
             (MINJ: mem_equiv m tm)
             (BOUND: Ple hi (Mem.nextblock m)),
        match_states (State f s k e le m)
                     (State tf s tk e tle tm)
  | match_call_state:
      forall fd vargs k m tfd tvargs tk tm targs tres cconv
             (TRFD: transf_fundef fd = OK tfd)
             (MCONT: match_cont k tk m (Mem.nextblock m) (Mem.nextblock tm))
             (MINJ: mem_equiv m tm)
             (AINJ: casted_list vargs (type_list_of_typelist targs))
             (SE: list_forall2 same_eval vargs tvargs)
             (FUNTY: type_of_fundef fd = Tfunction targs tres cconv),
        match_states (Callstate fd vargs k m)
                     (Callstate tfd tvargs tk tm)
  | match_return_state:
      forall v k m tv tk tm
        (MCONT: match_cont k tk m (Mem.nextblock m) (Mem.nextblock tm))
        (MINJ: mem_equiv m tm)
        (RINJ: same_eval v tv),
      match_states (Returnstate v k m)
                   (Returnstate tv tk tm).

The simulation diagrams

Section FIND_LABEL.

Variable m: mem.
Variables bound tbound: block.
Variable lbl: ident.

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

with simpl_find_label_ls:
  forall ls k tk,
  match_cont k tk m bound tbound ->
  match find_label_ls lbl ls k with
  | None =>
      find_label_ls lbl ls tk = None
  | Some(s', k') =>
    exists tk',
      find_label_ls lbl ls tk = Some(s', tk')
      /\ match_cont k' tk' m bound tbound
  end.

Proof.
  induction s; simpl; intros until tk; intros MC; auto.
  -
    exploit (IHs1 (Kseq s2 k) (Kseq s2 tk)); eauto with compat.
    constructor; eauto with compat.
    destruct (find_label lbl s1 (Kseq s2 k)) as [[s' k']|].
    intros [tk' [P Q]]. exists tk'. simpl. rewrite P. auto.
    intros E. simpl. rewrite E. eapply IHs2; eauto with compat.
  -
    exploit (IHs1 k tk); eauto with compat.
    destruct (find_label lbl s1 k) as [[s' k']|].
    intros [tk' [P Q]]. exists tk'. simpl. rewrite P. auto.
    intros E. simpl. rewrite E. eapply IHs2; eauto with compat.
  -
    exploit (IHs1 (Kloop1 s1 s2 k) (Kloop1 s1 s2 tk)); eauto with compat.
    constructor; eauto with compat.
    destruct (find_label lbl s1 (Kloop1 s1 s2 k)) as [[s' k']|].
    intros [tk' [P Q]]. exists tk'. simpl. rewrite P. auto.
    intros E. simpl. rewrite E. eapply IHs2; eauto with compat.
    econstructor; eauto with compat.
  -
    eapply simpl_find_label_ls; eauto with compat. constructor; auto.
  -
    destruct (ident_eq lbl l).
    + (exists tk; auto).
    + eapply IHs; eauto.
  -
    induction ls; simpl; intros; auto.
    exploit (simpl_find_label s (Kseq (seq_of_labeled_statement ls) k)).
    constructor; eauto.
    destruct (find_label lbl s (Kseq (seq_of_labeled_statement ls) k)) as [[s' k']|].
    intros [tk' [P Q]]. rewrite P.
    eexists; split; eauto.
    intros E. simpl; rewrite E. eapply IHls; eauto with compat.
Qed.


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

End FIND_LABEL.

Lemma free_list_bounds_after:
  forall bl m m',
    Mem.free_list m bl = Some m' ->
    forall b lo0 hi0,
      Mem.bounds_of_block m' b = (lo0, hi0) ->
      hi0 - lo0 <> 0 ->
      Mem.bounds_of_block m b = (lo0, hi0).
Proof.
  induction bl; simpl; intros; auto.
  - inv H; auto.
  - destruct a as [[b' lo] hi].
    destruct (Mem.free m b' lo hi) eqn:?; try discriminate.
    eapply IHbl in H; eauto.
    destruct (Mem.free_bounds _ _ _ _ _ b Heqo); auto.
    congruence.
    rewrite H in H2; inv H2; omega.
Qed.



Lemma bpt_se:
  forall vargs tvargs,
    list_forall2 same_eval vargs tvargs ->
    forall te pars e m0 m1,
      bind_parameters e m0 pars vargs m1 ->
      exists ee,
        bind_parameter_temps pars tvargs te = Some ee.
Proof.
  induction 1; simpl; intros; eauto.
  inv H; simpl. eexists; eauto.
  inv H1. eapply IHlist_forall2 in H9; eauto.
Qed.

Lemma bpt_se':
  forall vargs tyargs,
    casted_list vargs tyargs ->
    forall te pars e m0 m1,
      bind_parameters e m0 pars vargs m1 ->
      exists ee,
        bind_parameter_temps pars vargs te = Some ee.
Proof.
  induction 1; simpl; intros; eauto.
  inv H; simpl. eexists; eauto.
  inv H2.
  eapply IHcasted_list in H10; eauto.
Qed.


Lemma bpt_se'':
  forall vargs tvargs,
    list_forall2 same_eval vargs tvargs ->
    forall pars te te' ee,
      temp_env_equiv te te' ->
      bind_parameter_temps pars vargs te = Some ee ->
      exists ee',
        bind_parameter_temps pars tvargs te' = Some ee' /\
        temp_env_equiv ee ee'.
Proof.
  induction 1; simpl; intros.
  - destruct pars; simpl in *; try intuition congruence; try destruct p; inv H0.
    eexists; split; eauto. inv H0. auto.
    destruct p; inv H0.
  - destruct pars; simpl in *; try intuition congruence; try destruct p; inv H0.
    destruct p.
    eapply IHlist_forall2 in H2; eauto.
    intro; intros.
    rewrite ! PTree.gsspec.
    destruct (peq i0 i); simpl; auto.
    apply H1.
Qed.

Lemma unop_ext_se:
  forall s0 n v1,
    0 < n ->
   same_eval
     (Eunop
        (match s0 with
         | Signed => OpSignext
         | Unsigned => OpZeroext
         end n) Tint v1)
     (Eunop
        (match s0 with
         | Signed => OpSignext
         | Unsigned => OpZeroext
         end n) Tint
        (Eunop
           (match s0 with
            | Signed => OpSignext
            | Unsigned => OpZeroext
            end n) Tint v1)).
Proof.
  intros; constructor.
  - simpl.
    destruct (has_typ Tint (tcheck_expr v1)) eqn:?; simpl; auto.
    destruct s0; simpl; auto.
  - intros.
    destruct s0; unfold_eval;
    inv_expr_type (eSexpr alloc em eb eu Tint v1).
    rewrite Int.sign_ext_widen; auto; try omega.
    rewrite Int.zero_ext_widen; auto; try omega.
Qed.

Lemma boolval_idem_se:
  forall v1,
    same_eval (Eunop OpBoolval Tint v1)
              (Eunop OpBoolval Tint (Eunop OpBoolval Tint v1)).
Proof.
  intros; constructor; simpl; auto.
  - destruct (has_typ Tint (tcheck_expr v1)); simpl; auto.
  - intros; unfold_eval.
    inv_expr_type (eSexpr alloc em eb eu Tint v1).
    destruct (Int.eq i Int.zero); simpl.
    rewrite Int.eq_true; simpl; auto.
    rewrite Int.eq_false; simpl; auto.
    apply Int.one_not_zero.
Qed.

Lemma notbool_boolval_se:
  forall e,
    same_eval (Eunop OpNotbool Tint e)
              (Eunop OpBoolval Tint (Eunop OpNotbool Tint e)).
Proof.
  intros; constructor; simpl; auto.
  - destruct (has_typ Tint (tcheck_expr e)); simpl; auto.
  - intros; unfold_eval.
    inv_expr_type (eSexpr alloc em eb eu Tint e).
    destruct (Int.eq i Int.zero); simpl; auto.
Qed.

Lemma sem_cast_expr_idem:
  forall v1 ta ty v2,
    sem_cast_expr v1 ta ty = Some v2 ->
    exists v2',
      sem_cast_expr v2 ty ty = Some v2' /\
      same_eval v2 v2'.
Proof.
  intros.
  unfold sem_cast_expr in H.
  destruct ta eqn:?; destruct ty eqn:?;
           simpl in *;
    inv H;
    unfold sem_cast_expr;simpl;
    try (eexists; split; eauto; reflexivity).
  destruct i; simpl in *; inv H1.
  destruct f; simpl; inv H1.
  destruct i0; simpl in *; inv H1; eexists; split; eauto;
  try apply unop_ext_se; try omega.
  reflexivity.
  apply boolval_idem_se.
  destruct f; simpl; inv H1; eexists; split; eauto; reflexivity.
  destruct i; simpl in *; inv H1; eexists; split; eauto;
  try apply unop_ext_se; try omega.
  reflexivity.
  apply notbool_boolval_se.
  destruct f; simpl; inv H1; eexists; split; eauto; reflexivity.
  destruct i; simpl in *; inv H1; eexists; split; eauto;
  try destruct f; inv H0;
  try apply unop_ext_se; try omega;
  try reflexivity;
  try apply notbool_boolval_se.
  destruct f0; destruct f; simpl; inv H1; eexists; split; eauto; reflexivity.
  destruct i; simpl in *; inv H1; eexists; split; eauto;
  try apply unop_ext_se; try omega.
  reflexivity.
  apply notbool_boolval_se.
  destruct f; simpl; inv H1; eexists; split; eauto; reflexivity.
  destruct i; simpl in *; inv H1; eexists; split; eauto;
  try apply unop_ext_se; try omega.
  reflexivity.
  apply notbool_boolval_se.
  destruct f; simpl; inv H1; eexists; split; eauto; reflexivity.
  destruct i; simpl in *; inv H1; eexists; split; eauto;
  try apply unop_ext_se; try omega.
  reflexivity.
  apply notbool_boolval_se.
  destruct f; simpl; inv H1; eexists; split; eauto; reflexivity.
  destruct i0; simpl in *; inv H1; eexists; split; eauto;
  try apply unop_ext_se; try omega.
  destruct f0; simpl; inv H1; eexists; split; eauto; reflexivity.
  destruct (ident_eq i0 i0); destruct (fieldlist_eq f0 f0); simpl; try congruence.
  eexists; split; eauto; reflexivity.
  destruct i0; simpl in *; inv H1; eexists; split; eauto;
  try apply unop_ext_se; try omega.
  destruct f0; simpl; inv H1; eexists; split; eauto; reflexivity.
  destruct (ident_eq i0 i0); destruct (fieldlist_eq f0 f0); simpl; try congruence.
  eexists; split; eauto; reflexivity.
  destruct i0; simpl in *; inv H1; eexists; split; eauto;
  try apply unop_ext_se; try omega.
  reflexivity.
  apply notbool_boolval_se.
  destruct f; simpl; inv H1; eexists; split; eauto; reflexivity.
Qed.

Lemma eval_exprlist_casted_list:
  forall ge e le m al tyargs vargs,
    eval_exprlist ge e le m al tyargs vargs ->
    casted_list vargs (type_list_of_typelist tyargs).
Proof.
  induction 1; simpl; auto.
  constructor.
  apply sem_cast_expr_idem in H0.
  destruct H0 as [v2' [A B]].
  econstructor; eauto.
Qed.


Lemma params_type_list:
  forall f,
    (type_list_of_typelist (type_of_params (fn_params f))) =
    map snd (fn_params f).
Proof.
  intro. generalize (fn_params f).
  induction l; simpl; intros; eauto.
  destruct a; simpl; eauto.
  congruence.
Qed.





Lemma temp_env_equiv_sym:
  forall t1 t2,
    temp_env_equiv t1 t2 ->
    temp_env_equiv t2 t1.
Proof.
  intros t1 t2 A; red; intro i; specialize (A i);
  repeat destr_cond_match; try symmetry; auto.
Qed.

Lemma temp_env_equiv_trans:
  forall t1 t2 t3,
    temp_env_equiv t1 t2 ->
    temp_env_equiv t2 t3 ->
    temp_env_equiv t1 t3.
Proof.
  intros t1 t2 t3 A B; red; intro i;
  specialize (A i); specialize (B i);
  repeat destr_cond_match; destruct (t2!i) eqn:?; simpl in *; auto;
  etransitivity; eauto; try tauto.
Qed.

Instance temp_env_equiv_equi : RelationClasses.Equivalence temp_env_equiv :=
  RelationClasses.Build_Equivalence _ _
                                     (temp_env_equiv_refl)
                                     (temp_env_equiv_sym)
                                     (temp_env_equiv_trans).

Theorem store_params_correct:
  forall e m params args m',
    bind_parameters e m params args m' ->
    casted_list args (map snd params) ->
    forall f k le lo hi ,
    forall s tm tle1 targs,
      list_norepet (var_names params) ->
      list_forall2 same_eval args targs ->
      match_envs e le m lo hi tle1 ->
      mem_equiv m tm ->
      (forall id, In id (var_names params) -> le!id = None) ->
      forall tle ,
        bind_parameter_temps params args tle1 = Some tle ->
          exists tm',
            star step2 tge (State f (store_params params s) k e tle tm)
                 E0 (State f s k e tle tm')
            /\ mem_equiv m' tm'
            /\ match_envs e le m' lo hi tle
            /\ Mem.nextblock tm' = Mem.nextblock tm
            /\ (forall b, Mem.bounds_of_block tm' b = Mem.bounds_of_block tm b).
Proof.
  induction 1; simpl; intro CL; intros until targs; intros NOREPET SE MENV ME LE tle BPT .
  -
    inv SE. inv BPT. exists tm.
    split. apply star_refl. repeat (split; auto).
  -
    inv CL. inv SE.
    inv NOREPET.
    exploit assign_loc_inject; eauto. reflexivity.
    intros [tm1 [A B]].
    destruct (assign_loc_equiv _ _ _ _ _ _ A (same_eval_trans _ _ _ (same_eval_sym _ _ H4) H7)) as [tm2 [C D]].
    assert (mem_equiv m1 tm2) by (etransitivity; eauto).
    clear B.
    generalize BPT.
    intro.
    edestruct (IHbind_parameters) as [tm' [U [X [Y [Z Z0]]]]]; eauto.
    +
      apply match_envs_change_temp.
      eapply match_envs_invariant; eauto.
      intros. eapply assign_loc_bounds; eauto.
      apply LE; auto.
    +
      
      exists tm'.
      split.
      * eapply star_trans; eauto; try traceEq.
        eapply star_left. econstructor; eauto.
        eapply star_left. econstructor; eauto.
        eapply eval_Evar_local; eauto.
        econstructor; eauto.
        erewrite bind_parameter_temps_inv; eauto.
        apply PTree.gss.
        eapply star_left. econstructor.
        apply star_refl.
        reflexivity. reflexivity.
        traceEq.
      * rewrite (assign_loc_nextblock _ _ _ _ _ C) in Z.
        split; auto.
        repeat (split; auto; [idtac]).
        intros; rewrite Z0.
        symmetry; eapply assign_loc_bounds; eauto.
Qed.

Inductive match_cont_eq : cont -> cont -> Prop :=
| match_cont_eq_stop: match_cont_eq Kstop Kstop
| match_cont_eq_seq:
    forall s k k',
      match_cont_eq k k' ->
      match_cont_eq (Kseq s k) (Kseq s k')
| match_cont_eq_loop1:
    forall s t k k',
      match_cont_eq k k' ->
      match_cont_eq (Kloop1 s t k) (Kloop1 s t k')
| match_cont_eq_loop2:
    forall s t k k',
      match_cont_eq k k' ->
      match_cont_eq (Kloop2 s t k) (Kloop2 s t k')
| match_cont_eq_switch:
    forall k k',
      match_cont_eq k k' ->
      match_cont_eq (Kswitch k) (Kswitch k')
| match_cont_eq_call:
    forall k k' te te' oi f e,
      temp_env_equiv te te' ->
      match_cont_eq k k' ->
      match_cont_eq (Kcall oi f e te k) (Kcall oi f e te' k').

Inductive match_states_eq : state -> state -> Prop :=
| match_states_eq_state:
    forall f s k k' e te te' m m',
      temp_env_equiv te te' ->
      mem_equiv m m' ->
      match_cont_eq k k' ->
      match_states_eq (State f s k e te m) (State f s k' e te' m')
| match_states_eq_call:
    forall f el el' k k' m m',
      list_forall2 same_eval el el' ->
      mem_equiv m m' ->
      match_cont_eq k k' ->
      match_states_eq (Callstate f el k m) (Callstate f el' k' m')
| match_states_eq_ret:
    forall e e' k k' m m',
      match_cont_eq k k' ->
      mem_equiv m m' ->
      same_eval e e' ->
      match_states_eq (Returnstate e k m) (Returnstate e' k' m').



Lemma mem_temp_equiv_expr_lvalue:
  forall ge e le le' m m',
    mem_equiv m m' ->
    temp_env_equiv le le' ->
    (forall a v,
       Clight.eval_expr ge e le m a v ->
       exists v',
         Clight.eval_expr ge e le' m' a v' /\
         same_eval v v')
    /\(forall a v,
         Clight.eval_lvalue ge e le m a v ->
         exists v',
           Clight.eval_lvalue ge e le' m' a v' /\
           same_eval v v').
Proof.
  intros ge0 e le le' m m' ME TEE.
  apply eval_expr_lvalue_ind; intros.
  - eexists; split; eauto. econstructor; simpl; eauto. reflexivity.
  - eexists; split; eauto. econstructor; simpl; eauto. reflexivity.
  - eexists; split; eauto. econstructor; simpl; eauto. reflexivity.
  - eexists; split; eauto. econstructor; simpl; eauto. reflexivity.
  - specialize (TEE id); rewrite H in TEE.
    destruct (le'!id) eqn:?; try tauto.
    eexists; split; eauto. econstructor; simpl; eauto.
  - destruct H0 as [v' [A B]].
    eexists; split; eauto. econstructor; simpl; eauto.
  - destruct H0 as [v' [A B]].
    eexists; split; eauto. econstructor; simpl; eauto.
    subst.
    apply sem_unary_operation_expr_se; auto.
  - destruct H0 as [v' [A B]].
    destruct H2 as [v'' [C D]].
    generalize (sem_binary_operation_expr_se m op (typeof a1) (typeof a2) _ _ _ _ B D).
    rewrite H3.
    destr_cond_match; try tauto.
    intro; eexists; split; eauto. econstructor; simpl; eauto.
  - destruct H0 as [v' [A B]].
    generalize (sem_cast_expr_se (typeof a) ty _ _ B).
    rewrite H1. destr_cond_match; try tauto.
    eexists; split; eauto. econstructor; simpl; eauto.
  - destruct H0 as [v' [A B]].
    eapply deref_loc_se in H1; eauto.
    destruct H1 as [tv [C D]].
    eexists; split; eauto. econstructor; simpl; eauto.
  - eexists; split; eauto. econstructor; simpl; eauto. reflexivity.
  - eexists; split; eauto. eapply eval_Evar_global; eauto. reflexivity.
  - destruct H0 as [v' [A B]].
    eexists; split; eauto.
    econstructor. eauto.
  - destruct H0 as [v' [A B]].
    eexists; split; eauto.
    econstructor; eauto.
    apply binop_same_eval; auto. reflexivity.
  - destruct H0 as [v' [A B]].
    eexists; split; eauto.
    econstructor; eauto.
Qed.


Lemma mem_temp_equiv_expr:
  forall ge e le le' m m',
    mem_equiv m m' ->
    temp_env_equiv le le' ->
    forall a v,
      Clight.eval_expr ge e le m a v ->
      exists v',
        Clight.eval_expr ge e le' m' a v' /\
        same_eval v v'.
Proof.
  intros ge0 e le le' m m' ME TEE.
  apply (proj1 (mem_temp_equiv_expr_lvalue ge0 e _ _ _ _ ME TEE)).
Qed.
    
Lemma mem_temp_equiv_lvalue:
  forall ge e le le' m m',
    mem_equiv m m' ->
    temp_env_equiv le le' ->
    forall a v,
      Clight.eval_lvalue ge e le m a v ->
      exists v',
        Clight.eval_lvalue ge e le' m' a v' /\
        same_eval v v'.
Proof.
  intros ge0 e le le' m m' ME TEE.
  apply (proj2 (mem_temp_equiv_expr_lvalue ge0 e _ _ _ _ ME TEE)).
Qed.

   


Lemma mem_temp_equiv_exprlist:
  forall ge e le m al tl vl le' m',
    mem_equiv m m' ->
    temp_env_equiv le le' ->
    eval_exprlist ge e le m al tl vl ->
    exists vl',
      eval_exprlist ge e le' m' al tl vl' /\
      list_forall2 same_eval vl vl'.
Proof.
  intros ge0 e le m al tl vl le' m' ME TEE EEL.
  eapply temp_equiv_clight_eval_exprlist in EEL; eauto.
  destruct EEL as [vl' [EEL B]].
  eapply mem_equiv_clight_eval_exprlist in EEL; eauto.
  destruct EEL as [vl2' [EEL C]].
  eexists; split; eauto.
  rewrite B. rewrite C. reflexivity.
Qed.

Lemma mem_equiv_same_eval_norm:
  forall m m' e1 e2 r,
    mem_equiv m m' ->
    same_eval e1 e2 ->
    Mem.mem_norm m e1 r = Mem.mem_norm m' e2 r.
Proof.
  intros m m' e1 e2 r ME SE.
  rewrite (mem_equiv_norm _ _ _ _ ME).
  rewrite (same_eval_eqm _ _ _ _ SE); auto.
Qed.

Ltac simpeq :=
  repeat match goal with
             H: eval_lvalue ?tge ?e ?le ?m ?a1 ?vptr,
                ME: mem_equiv ?m ?m',
                    TE: temp_env_equiv ?le ?le' |- _ =>
             let vptr' := fresh "vptr" in
             let se := fresh "SE" in
             apply (mem_temp_equiv_lvalue tge e le le' m m' ME TE) in H;
               destruct H as [vptr' [H se]]
           | H: Mem.mem_norm ?m ?e ?r = _,
                ME: mem_equiv ?m ?m',
                    SE: same_eval ?e ?e' |- _ =>
             rewrite (mem_equiv_same_eval_norm m m' e e' r ME SE) in H
           | H: eval_expr ?tge ?e ?le ?m ?a1 ?v,
                ME: mem_equiv ?m ?m',
                    TE: temp_env_equiv ?le ?le' |- _ =>
             let v' := fresh "v" in
             let se := fresh "SE" in
             apply (mem_temp_equiv_expr tge e le le' m m' ME TE) in H;
               destruct H as [v' [H se]]
           | H: eval_exprlist ?tge ?e ?le ?m ?al ?tl ?vl,
                ME: mem_equiv ?m ?m',
                    TE: temp_env_equiv ?le ?le' |- _ =>
             let vl' := fresh "vl" in
             let se := fresh "SE" in
             apply (mem_temp_equiv_exprlist tge e le m al tl vl _ _ ME TE) in H;
               destruct H as [vl' [H se]]
           | H: sem_cast_expr ?v2 ?ty ?ty' = Some ?v,
                SE: same_eval ?v2 ?v3 |- _ =>
             let v := fresh "v" in
             let se := fresh "SE" in
             let sce := fresh "SCE" in
             generalize (sem_cast_expr_se ty ty' _ _ SE);
               rewrite H;
               destruct (sem_cast_expr v3 ty ty') as [v|] eqn:SCE; try tauto;
               intro se
           | H: assign_loc ?ty ?m ?addr ?v ?m2,
                ME: mem_equiv ?m ?m',
                    SE1: same_eval ?addr ?addr',
                         SE2: same_eval ?v ?v' |- _ =>
             let m2 := fresh "m" in
             let me := fresh "ME" in
             let al := fresh "AL" in
             destruct (assign_loc_inject _ _ _ _ _ _ _ _ H SE1 SE2 ME) as [m2 [al me]];
               clear H
           | H: Genv.find_funct ?m ?ge ?v = _,
                ME: mem_equiv ?m ?m',
                    SE: same_eval ?v ?v' |- _ =>
             rewrite (genv_find_funct_equiv ge _ _ _ _ ME SE) in H
           | H: match_cont_eq (Kseq ?s ?k) ?k' |- _ => inv H
           | H: match_cont_eq (Kloop1 ?s ?t ?k) ?k' |- _ => inv H
           | H: match_cont_eq (Kloop2 ?s ?t ?k) ?k' |- _ => inv H
           | H: match_cont_eq (Kswitch ?k) ?k' |- _ => inv H
           | H: match_cont_eq (Kcall ?oi ?f ?e ?te ?k) ?k' |- _ => inv H
           | H: Mem.free_list ?m ?bl = Some ?m',
                ME: mem_equiv ?m ?m2 |- _ =>
             let m2 := fresh "m2" in
             let me := fresh "ME" in
             apply (free_list_mem_equiv _ _ _ _ ME) in H;
               destruct H as [m2 [H me]]
         end.

Lemma match_cont_eq_call_cont:
  forall k k',
    match_cont_eq k k' ->
    match_cont_eq (call_cont k) (call_cont k').
Proof.
  induction 1; simpl; intros; try constructor; auto.
Qed.

Lemma is_call_cont_match_eq:
  forall k k',
    match_cont_eq k k' ->
    is_call_cont k ->
    is_call_cont k'.
Proof.
  induction 1; simpl; intros; auto.
Qed.


Lemma find_label_cont:
  forall lbl s k tk,
  match_cont_eq k tk ->
  match find_label lbl s k with
    | None =>
      find_label lbl s tk = None
    | Some(s', k') =>
      exists tk',
        find_label lbl s tk = Some(s', tk')
        /\ match_cont_eq k' tk'
  end

with find_label_ls_cont:
  forall lbl ls k tk,
  match_cont_eq k tk ->
  match find_label_ls lbl ls k with
  | None =>
      find_label_ls lbl ls tk = None
  | Some(s', k') =>
    exists tk',
      find_label_ls lbl ls tk = Some(s', tk')
      /\ match_cont_eq k' tk'
  end.

Proof.
  - induction s; simpl; intros until tk; intros MC; auto.
    + assert (match_cont_eq (Kseq s2 k) (Kseq s2 tk)) by (constructor; auto).
      destruct (find_label lbl s1 (Kseq s2 k)) eqn:?.
      generalize (IHs1 _ _ H).
      * destruct p.
         rewrite Heqo.
         intros [tk' [A B]].
         rewrite A. eexists; split; eauto.
      * generalize (IHs1 _ _ H).
        rewrite Heqo.
        intro A.
        rewrite A.
        apply IHs2. auto.
    + destruct (find_label lbl s1 k) eqn:?.
      generalize (IHs1 _ _ MC).
      * destruct p.
        rewrite Heqo.
        intros [tk' [A B]].
        rewrite A. eexists; split; eauto.
      *generalize (IHs1 _ _ MC).
       rewrite Heqo.
       intro A.
       rewrite A.
       apply IHs2. auto.
    + assert (match_cont_eq (Kloop1 s1 s2 k) (Kloop1 s1 s2 tk)) by (constructor; auto).
      destruct (find_label lbl s1 (Kloop1 s1 s2 k)) eqn:?.
      generalize (IHs1 _ _ H).
      * destruct p.
        rewrite Heqo.
        intros [tk' [A B]].
        rewrite A. eexists; split; eauto.
      * generalize (IHs1 _ _ H).
        rewrite Heqo.
        intro A.
        rewrite A.
        apply IHs2. constructor; auto.
    + apply find_label_ls_cont.
      constructor; auto.
    + destruct (ident_eq lbl l); subst; auto.
      eexists; split; eauto.
      apply IHs. auto.
  - induction ls; simpl in *. auto. intros.
    exploit (find_label_cont lbl s (Kseq (seq_of_labeled_statement ls) k)); eauto.
    econstructor; eauto.
    destruct (find_label lbl s (Kseq (seq_of_labeled_statement ls) k)) eqn:?; eauto.
    destruct p.
    intros [tk' [A B]].
    rewrite A. eexists; split; eauto.
    intro A; rewrite A.
    apply IHls. auto.
    
Qed.

Lemma find_label_call_cont:
  forall lbl f k k'0 s' k',
    find_label lbl (fn_body f) (call_cont k) = Some (s', k') ->
    match_cont_eq k k'0 ->
    exists k2,
      find_label lbl (fn_body f) (call_cont k'0) = Some (s', k2) /\
      match_cont_eq k' k2.
Proof.
  intros lbl f k k'0 s' k' FL MCE.
  generalize (find_label_cont lbl (fn_body f) (call_cont k) (call_cont k'0)).
  rewrite FL.
  intros [tk' [A B]].
  apply match_cont_eq_call_cont; auto.
  rewrite A.
  repeat eexists; eauto.
Qed.

Lemma bpt_mem_equiv_temp_equiv:
  forall params el te tte,
    bind_parameter_temps params el te = Some tte ->
    forall el' te',
      list_forall2 same_eval el el' ->
      temp_env_equiv te te' ->
      exists tte',
        bind_parameter_temps params el' te' = Some tte' /\
        temp_env_equiv tte tte'.
Proof.
  induction params; simpl; intros; auto.
  - destruct el; simpl in *; try discriminate.
    inv H.
    inv H0.
    eexists; split; auto.
  - destruct a.
    destruct el; try discriminate.
    inv H0.
    eapply IHparams in H; eauto.
    apply temp_env_equiv_set; auto.
Qed.

Lemma step_equiv_builtin:
  forall ef e le te' f m m' m'0 optid vres vargs vl tyargs t k k' al,
    eval_exprlist tge e te' m'0 al tyargs vl ->
    list_forall2 same_eval vargs vl ->
    external_call ef tge vargs m t vres m' ->
    temp_env_equiv le te' ->
    mem_equiv m m'0 ->
    match_cont_eq k k' ->
   exists S2' : state,
     step2 tge (State f (Sbuiltin optid ef tyargs al) k' e te' m'0) t S2' /\
     match_states_eq (State f Sskip k e (set_opttemp optid vres le) m') S2'.
Proof.
  intros.
  eapply external_call_se in H1; eauto.
  destruct H1 as [vres' [m2' [A [B C]]]].
  destruct ef; intros; simpl in *;
  try (eexists; split; eauto; [econstructor; eauto| constructor; auto; destruct optid; auto;
                                                    apply temp_env_equiv_set; auto]).
Qed.


Lemma step_equiv_external:
  forall ef m m' m'0 vres vargs el' cconv tres targs t k k' ,
    external_call ef tge vargs m t vres m' ->
    list_forall2 same_eval vargs el' ->
    mem_equiv m m'0 ->
    match_cont_eq k k' ->
   exists S2' : state,
     step2 tge (Callstate (External ef targs tres cconv) el' k' m'0) t S2' /\
     match_states_eq (Returnstate vres k m') S2'.
Proof.
  intros.
  eapply external_call_se in H1; eauto.
  destruct H1 as [vres' [m2' [A [B C]]]].
  destruct ef; intros; simpl in *;
  try (eexists; split; eauto; [econstructor; eauto| constructor; auto; destruct optid; auto;
                                                    apply temp_env_equiv_set; auto]).
Qed.

Lemma step_equiv:
  forall S1 t S2,
    step2 tge S1 t S2 ->
    forall S1' (MS: match_states_eq S1 S1'),
    exists S2',
      step2 tge S1' t S2' /\ match_states_eq S2 S2'.
Proof.
  induction 1; simpl; intros; inv MS; simpeq;
  try (eexists; split; [econstructor; simpl; eauto | constructor; auto;
                                                     ((constructor; auto) ||
                                                                          (apply match_cont_eq_call_cont; auto))]; fail).
  - eexists; split.
    econstructor; simpl; eauto.
    constructor; auto.
    apply temp_env_equiv_set; auto.
  - eapply step_equiv_builtin; eauto.
  - eexists; split.
    econstructor; simpl; eauto.
    instantiate (1:=b).
    rewrite <- H0; symmetry.
    eapply mem_equiv_same_eval_norm; eauto.
    apply bool_expr_se; auto.
    constructor; auto.
  - eexists; split; eauto.
    apply step_break_loop1; auto.
    constructor; auto.
  - eexists; split; eauto.
    econstructor; eauto.
    eapply is_call_cont_match_eq; eauto.
    constructor; auto. reflexivity.
  - eexists; split; eauto.
    econstructor; eauto.
    unfold sem_switch_arg in *.
    destruct (classify_switch (typeof a)) eqn:?; simpl in *;
      try rewrite <- (mem_equiv_same_eval_norm _ _ _ _ _ H9 SE); eauto.
    constructor; auto.
    constructor; auto.
  - eexists; split; eauto.
    apply step_continue_switch; auto.
    constructor; auto.
  - eapply find_label_call_cont in H; eauto.
    destruct H as [k2 [FL MCE]]. eexists; split; eauto.
    econstructor; eauto.
    constructor; auto.
  - inv H.
    apply bpt_mem_equiv_temp_equiv with (el':=el') (te':= create_undef_temps (fn_temps f)) in H4; auto.
    destruct H4 as [tte' [BPT TEE]].
    apply match_envs_alloc_variables with (temps:= fn_temps f) (tm:=m') in H3; auto.
    destruct H3 as [tm' [AV [MENV ME]]].
    eexists; split; eauto.
    econstructor.
    econstructor; eauto.
    constructor; auto.
    revert H0. apply Alloc.permutation_norepet.
    unfold var_names.
    apply Permutation.Permutation_map.
    apply VarSortType.Permuted_sort.
    reflexivity.
  - eapply step_equiv_external; eauto.
  - eexists; split; eauto.
    econstructor; simpl; eauto.
    constructor; auto.
    destruct optid; simpl; auto.
    apply temp_env_equiv_set; auto.
Qed.

Lemma star_step_equiv:
  forall S1 t S2,
    star step2 tge S1 t S2 ->
    forall S1' (MS: match_states_eq S1 S1'),
    exists S2',
      star step2 tge S1' t S2' /\ match_states_eq S2 S2'.
Proof.
  induction 1; simpl; intros.
  - (exists S1'; split; auto).
    apply star_refl.
  - eapply step_equiv in H; eauto.
    destruct H as [s2' [A B]].
    apply IHstar in B.
    destruct B as [S2' [AA BB]].
    eexists; split; eauto.
    eapply star_left; eauto.
Qed.


Lemma match_cont_eq_refl:
  forall k,
    match_cont_eq k k.
Proof.
  induction k; simpl; intros; try constructor; auto.
  reflexivity.
Qed.

Lemma match_envs_temp_equiv:
  forall e le m lo hi tle tle',
    match_envs e le m lo hi tle ->
    temp_env_equiv tle tle' ->
    match_envs e le m lo hi tle'.
Proof.
  destruct 1; intros; constructor; auto.
  intros.
  apply me_temps0 in H0; eauto.
  destruct H0 as [tv [A B]].
  specialize (H id); rewrite A in H; destruct (tle'!id) eqn:?; try tauto.
  eexists; split; eauto.
  rewrite B; auto.
Qed.

Lemma match_cont_eq_match_cont:
  forall k tk m lo hi,
    match_cont k tk m lo hi ->
    forall k'
           (MCE: match_cont_eq tk k'),
      match_cont k k' m lo hi.
Proof.
  induction 1; simpl; intros; inv MCE; try constructor; auto.
  eapply match_Kstop; eauto.
  eapply match_Kcall; eauto.
  eapply match_envs_temp_equiv; eauto.
Qed.

Lemma menv_ec:
  forall ef vargs m t vres m' le e lo hi tle
         (EC: external_call ef ge vargs m t vres m')
         (MENV : match_envs e le m lo hi tle),
   match_envs e le m' lo hi tle.
Proof.
  destruct ef; simpl; intros.
  - eapply external_call_not_taken_into_account; eauto.
  - eapply external_call_not_taken_into_account; eauto.
  - inv EC; inv MENV; constructor; auto.
  - inv EC; inv MENV; constructor; auto.
    intros; erewrite <- me_bounds0; eauto.
    inv H; auto.
    symmetry;eapply Mem.bounds_of_block_store; eauto.
  - inv EC; inv MENV; constructor; auto.
  - inv EC; inv MENV; constructor; auto.
    intros; erewrite <- me_bounds0; eauto.
    inv H0; auto.
    symmetry;eapply Mem.bounds_of_block_store; eauto.
  - inv EC; inv MENV; constructor; auto.
    intros; erewrite <- me_bounds0; eauto.
    symmetry; erewrite Mem.bounds_of_block_storebytes; eauto.
  - eapply inline_assembly_not_taken_into_account; eauto.
Qed.


Lemma mcont_ec:
  forall ef vargs m t vres m' k k' lo hi
         (EC: external_call ef ge vargs m t vres m')
         (MENV : match_cont k k' m lo hi),
    match_cont k k' m' lo hi.
Proof.
  intros.
  eapply match_cont_invariant; eauto.
  destruct ef; simpl; intros; try inv EC; auto.
  - eapply external_call_not_taken_into_account; eauto.
  - eapply external_call_not_taken_into_account; eauto.
  - inv H0; auto.
    eapply Mem.bounds_of_block_store; eauto.
  - inv H1; auto.
    eapply Mem.bounds_of_block_store; eauto.
  - erewrite Mem.bounds_of_block_storebytes; eauto.
  - eapply inline_assembly_not_taken_into_account; eauto.
Qed.


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

-


  exploit eval_simpl_lvalue; eauto with compat. intros [tb [E F]].
  exploit eval_simpl_expr; eauto with compat. intros [tv2 [A B]].
  generalize (sem_cast_expr_se (typeof a2) (typeof a1) _ _ B).
  rewrite H1; destr_cond_match; try tauto; intro C.
  exploit assign_loc_inject; eauto. intros [tm' [X Y]].
  econstructor; split.
  apply plus_one. econstructor. eexact E. eexact A. eexact Heqo.
  eexact X.
  econstructor; eauto with compat.
  eapply match_envs_invariant; eauto.
  { intros.
    eapply assign_loc_bounds; eauto. }
  eapply match_cont_invariant; eauto.
  { intros.
    eapply assign_loc_bounds; eauto. }
  erewrite assign_loc_nextblock; eauto.

-
  exploit eval_simpl_expr; eauto with compat. intros [tv [A B]].
  econstructor; split.
  apply plus_one. econstructor. eauto.
  econstructor; eauto with compat.
  eapply match_envs_set_temp; eauto.

-
  exploit eval_simpl_expr; eauto with compat. intros [tvf [A B]].
  exploit eval_simpl_exprlist; eauto with compat. intros [tvargs [C D]].
  exploit match_cont_find_funct; eauto. intros [tfd [P Q]].
  econstructor; split.
  + apply plus_one. eapply step_call with (fd := tfd); eauto.
    erewrite type_of_fundef_preserved; eauto.
  + econstructor; eauto.
    econstructor; eauto.
    inv MINJ; rewrite <- mem_nextblock_eq; eauto.
    eapply eval_exprlist_casted_list; eauto.
-
  exploit eval_simpl_exprlist; eauto with compat. intros [tvargs [C D]].
  exploit external_call_se; eauto.
  intros [vres' [m2' [A [B E]]]].
  eexists; split.
  apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto.
  exact symbols_preserved. exact varinfo_preserved.
  econstructor; eauto.
  eapply match_envs_set_opttemp; eauto.
  eapply menv_ec; eauto.
  eapply mcont_ec; eauto.
  eapply Ple_trans; eauto. eapply external_call_nextblock; eauto.
-
  econstructor; split. apply plus_one. econstructor.
  econstructor; eauto with compat. econstructor; eauto with compat.

-
  inv MCONT. econstructor; split. apply plus_one. econstructor. econstructor; eauto.

-
  inv MCONT. econstructor; split. apply plus_one. econstructor. econstructor; eauto.
 
-
  inv MCONT. econstructor; split. apply plus_one. econstructor. econstructor; eauto.

-
  exploit eval_simpl_expr; eauto with compat. intros [tv [A B]].
  econstructor; split.
  apply plus_one. apply step_ifthenelse with (v1 := tv) (b := b). auto.
  rewrite <- H0.
  symmetry; erewrite mem_equiv_norm; eauto.
  apply same_eval_eqm.
  apply bool_expr_se; auto.
  destruct b; econstructor; eauto with compat.

-
  econstructor; split. apply plus_one. econstructor. econstructor; eauto with compat. econstructor; eauto with compat.

-
  inv MCONT. econstructor; split.
  apply plus_one. econstructor. auto.
  econstructor; eauto with compat. econstructor; eauto with compat.

-
  inv MCONT. econstructor; split. apply plus_one. eapply step_break_loop1.
  econstructor; eauto.

-
  inv MCONT. econstructor; split. apply plus_one. eapply step_skip_loop2.
  econstructor; eauto with compat.

-
  inv MCONT. econstructor; split. apply plus_one. eapply step_break_loop2.
  econstructor; eauto.

-
  exploit match_envs_free_blocks; eauto. intros [tm' [P R]].
  econstructor; split. apply plus_one. econstructor; eauto.
  econstructor; eauto.
  intros. eapply match_cont_call_cont. eapply match_cont_free_env; eauto.
  reflexivity.
-
  exploit eval_simpl_expr; eauto with compat. intros [tv [A B]].
  generalize (sem_cast_expr_se (typeof a) (fn_return f) _ _ B); rewrite H0;
  destr_cond_match; try tauto; intro C.
  exploit match_envs_free_blocks; eauto. intros [tm' [P Q]].
  econstructor; split. apply plus_one. econstructor; eauto.
  monadInv TRF; simpl. eauto.
  econstructor; eauto.
  intros. eapply match_cont_call_cont. eapply match_cont_free_env; eauto.

-
  exploit match_envs_free_blocks; eauto. intros [tm' [P Q]].
  econstructor; split. apply plus_one. econstructor; eauto.
  eapply match_cont_is_call_cont; eauto.
  monadInv TRF; auto.
  econstructor; eauto.
  intros. eapply match_cont_free_env; eauto.
  reflexivity.
  
-
  exploit eval_simpl_expr; eauto with compat. intros [tv [A B]].
  econstructor; split. apply plus_one. econstructor; eauto.
  instantiate (1 := n).
  unfold sem_switch_arg in *;
  destruct (classify_switch (typeof a)); try discriminate;
  inv H0; auto; revert H2; destr_cond_match; try discriminate; intro C; inv C;
  erewrite <- mem_equiv_norm; eauto;
  erewrite <- same_eval_eqm; eauto.
  rewrite Heqv0; auto.
  rewrite Heqv0; auto.
  econstructor; eauto.
  econstructor; eauto.

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

-
  inv MCONT. econstructor; split.
  apply plus_one. eapply step_continue_switch.
  econstructor; eauto with compat.

-
  econstructor; split. apply plus_one. econstructor. econstructor; eauto.

-
  generalize TRF; intros TRF'. monadInv TRF'.
  exploit (simpl_find_label m lo lo lbl (fn_body f) (call_cont k)
                            (call_cont tk)).
    eauto. eapply match_cont_call_cont. eauto.
  rewrite H. intros [tk' [A B]].
  econstructor; split.
  apply plus_one. econstructor; eauto. simpl. rewrite find_label_store_params. eexact A.
  econstructor; eauto.

-
  monadInv TRFD. inv H.
  generalize EQ; intro EQ'; monadInv EQ'.
  assert (list_norepet (var_names (fn_params f ++ fn_vars f))).
  { unfold var_names. rewrite map_app. auto. }
  exploit match_envs_alloc_variables; eauto.
  {
    revert H. apply Alloc.permutation_norepet.
    unfold var_names.
    apply Permutation.Permutation_map.
    apply VarSortType.Permuted_sort.
  }
  
  intros [tm' [A [B C]]].
  destruct (bpt_se' _ _ AINJ (create_undef_temps (fn_temps f)) _ _ _ _ H2) as [te' Hte'].
  destruct (bpt_se'' _ _ SE _ _ _ _ (temp_env_equiv_refl _) Hte') as [te'' [Hte'' D]].

  exploit store_params_correct.
  + eauto.
  + unfold type_of_function in FUNTY. inv FUNTY.
    rewrite params_type_list in AINJ. auto.
  + eapply list_norepet_append_left; eauto.
  + eauto.
  + eexact B.
  + eexact C.
  + intros. destruct (create_undef_temps (fn_temps f))!id as [v|] eqn:?; auto.
    exploit create_undef_temps_inv; eauto. intros [P Q]. elim (l id id); auto.
    eauto.
  + eauto.
  + intros [tm1 [P [Q [R [S T]]]]].
    eapply (star_step_equiv) in P; eauto.
    destruct P as [S2' [SS MSE]].
    generalize (vars_and_temps_properties (fn_params f) (fn_vars f) (fn_temps f)).
    intros [X [Y Z]]. auto. auto.
    eexists; split; simpl; eauto.
    * eapply plus_left. econstructor.
      econstructor; simpl.
      exact Y. exact X. exact Z. eexact A.
      eauto.
      simpl. eexact SS.
      reflexivity.
    * inv MSE. econstructor; eauto.
      eapply match_envs_temp_equiv; eauto.
      eapply match_cont_invariant with (m:=m); eauto.
      inv MINJ. rewrite <- mem_nextblock_eq in MCONT; auto.
      eapply match_cont_eq_match_cont; eauto.
      intros.
      transitivity (Mem.bounds_of_block m0 b).
      eapply alloc_variables_bound; eauto.
      symmetry. eapply bind_parameters_bound; eauto. intros.
      exploit alloc_variables_range. eexact H1. eauto.
      unfold empty_env. rewrite PTree.gempty. intros [?|?]. congruence.
      red; intros; subst b'. xomega.
      rewrite <- H11. auto.
      rewrite (bind_parameters_nextblock _ _ _ _ _ H2). xomega.
    * constructor; auto. reflexivity. apply match_cont_eq_refl.
-
  monadInv TRFD. inv FUNTY.
  exploit external_call_se; eauto.
  intros [vres' [m2' [A [B C]]]].
  econstructor; split.
  apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto.
  exact symbols_preserved. exact varinfo_preserved.
  econstructor; eauto.
  intros. apply match_cont_incr_bounds with (Mem.nextblock m) (Mem.nextblock tm).
  eapply mcont_ec; eauto.
  eapply external_call_nextblock; eauto.
  eapply external_call_nextblock; eauto.
  
-
  inv MCONT.
  econstructor; split.
  apply plus_one. econstructor.
  econstructor; eauto with compat.
  eapply match_envs_set_opttemp; eauto.
Qed.

Lemma initial_states_simulation:
  forall S, initial_state prog S ->
  exists R, initial_state tprog R /\ match_states S R.
Proof.
  intros. inv H.
  exploit function_ptr_translated; eauto. intros [tf [A B]].
  econstructor; split.
  econstructor.
  eapply Genv.init_mem_transf_partial; eauto.
  rewrite (transform_partial_program_main _ _ TRANSF).
  instantiate (1 := b). rewrite <- H1. apply symbols_preserved.
  eauto.
  rewrite <- H3; apply type_of_fundef_preserved; auto.
  econstructor; eauto.
  econstructor. instantiate (1 := Mem.nextblock m0).
  constructor; intros.
  eapply Genv.find_symbol_not_fresh; eauto.
  eapply Genv.find_funct_ptr_not_fresh; eauto.
  eapply Genv.find_var_info_not_fresh; eauto.
  xomega. xomega.
  reflexivity.
  simpl. constructor.
  constructor.
Qed.

Lemma final_states_simulation:
  forall S R r,
  match_states S R -> final_state S r -> final_state R r.
Proof.
  intros. inv H0. inv H.
  inv MCONT.
  econstructor.
  erewrite <- mem_equiv_norm; eauto.
  erewrite <- same_eval_eqm; eauto.
Qed.

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

End PRESERVATION.