(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** Elimination of unneeded computations over RTL: correctness proof. *)

Require Import FunInd.
Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
Require Import AST Linking.
Require Import Values Memory Globalenvs Events Smallstep.
Require Import Registers Op RTL.
Require Import ValueDomain ValueAnalysis NeedDomain NeedOp Deadcode.

Definition match_prog (prog tprog: RTL.program) :=
  match_program (fun cu f tf => transf_fundef (romem_for cu) f = OK tf) eq prog tprog.

Lemma transf_program_match:
  forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog.
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. eapply match_transform_partial_program_contextual; eauto.
Qed.

(** * Relating the memory states *)

(** The [magree] predicate is a variant of [Mem.extends] where we
  allow the contents of the two memory states to differ arbitrarily
  on some locations.  The predicate [P] is true on the locations whose
  contents must be in the [lessdef] relation. *)

Definition locset := block -> Z -> Prop.

(* Goal: forall (chunk : memory_chunk) (addr v : val) (_ : @eq (option val) (Mem.loadv chunk m addr) (@Some val v)), @ex val (fun v' : val => @eq (option val) (Mem.loadv chunk m' addr) (@Some val v')) *)
(* Goal: forall (a : builtin_arg positive) (v : val) (_ : @eval_builtin_arg positive (@Genv.to_senv fundef unit ge) (fun r : positive => Regmap.get val r e) (Vptr sp Ptrofs.zero) m a v), @ex val (fun v' : val => @eval_builtin_arg positive (@Genv.to_senv fundef unit tge) (fun r : positive => Regmap.get val r e') (Vptr sp Ptrofs.zero) m' a v') *)
Record magree (m1 m2: mem) (P: locset) : Prop := mk_magree {
  ma_perm:
    forall b ofs k p,
    Mem.perm m1 b ofs k p -> Mem.perm m2 b ofs k p;
  ma_perm_inv:
    forall b ofs k p,
    Mem.perm m2 b ofs k p -> Mem.perm m1 b ofs k p \/ ~Mem.perm m1 b ofs Max Nonempty;
  ma_memval:
    forall b ofs,
    Mem.perm m1 b ofs Cur Readable ->
    P b ofs ->
    memval_lessdef (ZMap.get ofs (PMap.get b (Mem.mem_contents m1)))
                   (ZMap.get ofs (PMap.get b (Mem.mem_contents m2)));
  ma_nextblock:
    Mem.nextblock m2 = Mem.nextblock m1
}.

Lemma magree_monotone:
  forall m1 m2 (P Q: locset),
  magree m1 m2 P ->
  (forall b ofs, Q b ofs -> P b ofs) ->
  magree m1 m2 Q.
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. destruct H. constructor; auto.
Qed.

Lemma mextends_agree:
  forall m1 m2 P, Mem.extends m1 m2 -> magree m1 m2 P.
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. destruct H. destruct mext_inj. constructor; intros.
- replace ofs with (ofs + 0) by omega. eapply mi_perm; eauto. auto.
- eauto.
- exploit mi_memval; eauto. unfold inject_id; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  rewrite Z.add_0_r. auto.
- auto.
Qed.

Lemma magree_extends:
  forall m1 m2 (P: locset),
  (forall b ofs, P b ofs) ->
  magree m1 m2 P -> Mem.extends m1 m2.
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. destruct H0. constructor; auto. constructor; unfold inject_id; intros.
- inv H0. rewrite Z.add_0_r. eauto.
- inv H0. apply Z.divide_0_r.
- inv H0. rewrite Z.add_0_r. eapply ma_memval0; eauto.
Qed.

Lemma magree_loadbytes:
  forall m1 m2 P b ofs n bytes,
  magree m1 m2 P ->
  Mem.loadbytes m1 b ofs n = Some bytes ->
  (forall i, ofs <= i < ofs + n -> P b i) ->
  exists bytes', Mem.loadbytes m2 b ofs n = Some bytes' /\ list_forall2 memval_lessdef bytes bytes'.
Proof.
  assert (GETN: forall c1 c2 n ofs,
    (forall i, ofs <= i < ofs + Z.of_nat n -> memval_lessdef (ZMap.get i c1) (ZMap.get i c2)) ->
    list_forall2 memval_lessdef (Mem.getN n ofs c1) (Mem.getN n ofs c2)).
(* Goal: forall (chunk : memory_chunk) (addr v : val) (_ : @eq (option val) (Mem.loadv chunk m addr) (@Some val v)), @ex val (fun v' : val => @eq (option val) (Mem.loadv chunk m' addr) (@Some val v')) *)
(* Goal: forall (a : builtin_arg positive) (v : val) (_ : @eval_builtin_arg positive (@Genv.to_senv fundef unit ge) (fun r : positive => Regmap.get val r e) (Vptr sp Ptrofs.zero) m a v), @ex val (fun v' : val => @eval_builtin_arg positive (@Genv.to_senv fundef unit tge) (fun r : positive => Regmap.get val r e') (Vptr sp Ptrofs.zero) m' a v') *)
  {
    induction n; intros; simpl.
(* Goal: final_state (Returnstate (@nil stackframe) (Vint r) tm) r *)
    constructor.
(* Goal: final_state (Returnstate (@nil stackframe) (Vint r) tm) r *)
    rewrite Nat2Z.inj_succ in H. constructor.
    apply H. omega.
(* Goal: Logic.and (Z.le ofs ofs0) (Z.lt ofs0 (Z.add ofs (Z.of_nat (@Datatypes.length memval bytes1)))) *)
(* Goal: P b ofs0 *)
    apply IHn. intros; apply H; omega.
  }
Local Transparent Mem.loadbytes.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  unfold Mem.loadbytes; intros. destruct H.
(* Goal: final_state st2 r *)
  destruct (Mem.range_perm_dec m1 b ofs (ofs + n) Cur Readable); inv H0.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  rewrite pred_dec_true. econstructor; split; eauto.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  apply GETN. intros. rewrite nat_of_Z_max in H.
(* Goal: Logic.and (Z.le ofs ofs0) (Z.lt ofs0 (Z.add ofs (Z.of_nat (@Datatypes.length memval bytes1)))) *)
(* Goal: P b ofs0 *)
  assert (ofs <= i < ofs + n) by xomega.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  apply ma_memval0; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  red; intros; eauto.
Qed.

Lemma magree_load:
  forall m1 m2 P chunk b ofs v,
  magree m1 m2 P ->
  Mem.load chunk m1 b ofs = Some v ->
  (forall i, ofs <= i < ofs + size_chunk chunk -> P b i) ->
  exists v', Mem.load chunk m2 b ofs = Some v' /\ Val.lessdef v v'.
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. exploit Mem.load_valid_access; eauto. intros [A B].
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit Mem.load_loadbytes; eauto. intros [bytes [C D]].
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit magree_loadbytes; eauto. intros [bytes' [E F]].
(* Goal: @ex val (fun v' : val => Logic.and (@eq (option val) (Mem.load chunk m2 b ofs) (@Some val v')) (Val.lessdef v v')) *)
  exists (decode_val chunk bytes'); split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  apply Mem.loadbytes_load; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  apply val_inject_id. subst v. apply decode_val_inject; auto.
Qed.

Lemma magree_storebytes_parallel:
  forall m1 m2 (P Q: locset) b ofs bytes1 m1' bytes2,
  magree m1 m2 P ->
  Mem.storebytes m1 b ofs bytes1 = Some m1' ->
  (forall b' i, Q b' i ->
                b' <> b \/ i < ofs \/ ofs + Z.of_nat (length bytes1) <= i ->
                P b' i) ->
  list_forall2 memval_lessdef bytes1 bytes2 ->
  exists m2', Mem.storebytes m2 b ofs bytes2 = Some m2' /\ magree m1' m2' Q.
Proof.
  assert (SETN: forall (access: Z -> Prop) bytes1 bytes2,
    list_forall2 memval_lessdef bytes1 bytes2 ->
    forall p c1 c2,
    (forall i, access i -> i < p \/ p + Z.of_nat (length bytes1) <= i -> memval_lessdef (ZMap.get i c1) (ZMap.get i c2)) ->
    forall q, access q ->
    memval_lessdef (ZMap.get q (Mem.setN bytes1 p c1))
                   (ZMap.get q (Mem.setN bytes2 p c2))).
(* Goal: forall (chunk : memory_chunk) (addr v : val) (_ : @eq (option val) (Mem.loadv chunk m addr) (@Some val v)), @ex val (fun v' : val => @eq (option val) (Mem.loadv chunk m' addr) (@Some val v')) *)
(* Goal: forall (a : builtin_arg positive) (v : val) (_ : @eval_builtin_arg positive (@Genv.to_senv fundef unit ge) (fun r : positive => Regmap.get val r e) (Vptr sp Ptrofs.zero) m a v), @ex val (fun v' : val => @eval_builtin_arg positive (@Genv.to_senv fundef unit tge) (fun r : positive => Regmap.get val r e') (Vptr sp Ptrofs.zero) m' a v') *)
  {
(* Goal: forall (access : forall _ : Z, Prop) (bytes1 bytes2 : list memval) (_ : @list_forall2 memval memval memval_lessdef bytes1 bytes2) (p : Z) (c1 c2 : ZMap.t memval) (_ : forall (i : Z) (_ : access i) (_ : Logic.or (Z.lt i p) (Z.le (Z.add p (Z.of_nat (@Datatypes.length memval bytes1))) i)), memval_lessdef (@ZMap.get memval i c1) (@ZMap.get memval i c2)) (q : Z) (_ : access q), memval_lessdef (@ZMap.get memval q (Mem.setN bytes1 p c1)) (@ZMap.get memval q (Mem.setN bytes2 p c2)) *)
    induction 1; intros; simpl.
  - apply H; auto. simpl. omega.
  - simpl length in H1; rewrite Nat2Z.inj_succ in H1.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
    apply IHlist_forall2; auto.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
    intros. rewrite ! ZMap.gsspec. destruct (ZIndexed.eq i p). auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
    apply H1; auto. unfold ZIndexed.t in *; omega.
  }
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros.
(* Goal: @ex Mem.mem (fun m2' : Mem.mem => Logic.and (@eq (option Mem.mem) (Mem.storebytes m2 b ofs bytes2) (@Some Mem.mem m2')) (magree m1' m2' Q)) *)
  destruct (Mem.range_perm_storebytes m2 b ofs bytes2) as [m2' ST2].
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  { erewrite <- list_forall2_length by eauto. red; intros.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
    eapply ma_perm; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
    eapply Mem.storebytes_range_perm; eauto. }
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exists m2'; split; auto.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  constructor; intros.
- eapply Mem.perm_storebytes_1; eauto. eapply ma_perm; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply Mem.perm_storebytes_2; eauto.
- exploit ma_perm_inv; eauto using Mem.perm_storebytes_2.
(* Goal: forall _ : Logic.or (Mem.perm m1 b0 ofs0 k p) (not (Mem.perm m1 b0 ofs0 Max Nonempty)), Logic.or (Mem.perm m1' b0 ofs0 k p) (not (Mem.perm m1' b0 ofs0 Max Nonempty)) *)
  intuition eauto using Mem.perm_storebytes_1, Mem.perm_storebytes_2.
- rewrite (Mem.storebytes_mem_contents _ _ _ _ _ H0).
(* Goal: memval_lessdef (@ZMap.get memval ofs0 (@PMap.get (ZMap.t memval) b0 (@PMap.set (ZMap.t memval) b (Mem.setN bytes1 ofs (@PMap.get (ZMap.t memval) b (Mem.mem_contents m1))) (Mem.mem_contents m1)))) (@ZMap.get memval ofs0 (@PMap.get (ZMap.t memval) b0 (Mem.mem_contents m2'))) *)
  rewrite (Mem.storebytes_mem_contents _ _ _ _ _ ST2).
(* Goal: memval_lessdef (@ZMap.get memval ofs0 (@PMap.get (ZMap.t memval) b0 (@PMap.set (ZMap.t memval) b (Mem.setN bytes1 ofs (@PMap.get (ZMap.t memval) b (Mem.mem_contents m1))) (Mem.mem_contents m1)))) (@ZMap.get memval ofs0 (@PMap.get (ZMap.t memval) b0 (@PMap.set (ZMap.t memval) b (Mem.setN bytes2 ofs (@PMap.get (ZMap.t memval) b (Mem.mem_contents m2))) (Mem.mem_contents m2)))) *)
  rewrite ! PMap.gsspec. destruct (peq b0 b).
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
+ subst b0. apply SETN with (access := fun ofs => Mem.perm m1' b ofs Cur Readable /\ Q b ofs); auto.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. destruct H5. eapply ma_memval; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply Mem.perm_storebytes_2; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
+ eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto.
- rewrite (Mem.nextblock_storebytes _ _ _ _ _ H0).
(* Goal: @eq block (Mem.nextblock m2') (Mem.nextblock m1) *)
  rewrite (Mem.nextblock_storebytes _ _ _ _ _ ST2).
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply ma_nextblock; eauto.
Qed.

Lemma magree_store_parallel:
  forall m1 m2 (P Q: locset) chunk b ofs v1 m1' v2,
  magree m1 m2 P ->
  Mem.store chunk m1 b ofs v1 = Some m1' ->
  vagree v1 v2 (store_argument chunk) ->
  (forall b' i, Q b' i ->
                b' <> b \/ i < ofs \/ ofs + size_chunk chunk <= i ->
                P b' i) ->
  exists m2', Mem.store chunk m2 b ofs v2 = Some m2' /\ magree m1' m2' Q.
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit Mem.store_valid_access_3; eauto. intros [A B].
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit Mem.store_storebytes; eauto. intros SB1.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit magree_storebytes_parallel. eauto. eauto.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  instantiate (1 := Q). intros. rewrite encode_val_length in H4.
  rewrite <- size_chunk_conv in H4. apply H2; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply store_argument_sound; eauto.
  intros [m2' [SB2 AG]].
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exists m2'; split; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  apply Mem.storebytes_store; auto.
Qed.

Lemma magree_storebytes_left:
  forall m1 m2 P b ofs bytes1 m1',
  magree m1 m2 P ->
  Mem.storebytes m1 b ofs bytes1 = Some m1' ->
  (forall i, ofs <= i < ofs + Z.of_nat (length bytes1) -> ~(P b i)) ->
  magree m1' m2 P.
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. constructor; intros.
- eapply ma_perm; eauto. eapply Mem.perm_storebytes_2; eauto.
- exploit ma_perm_inv; eauto.
(* Goal: forall _ : Logic.or (Mem.perm m1 b0 ofs0 k p) (not (Mem.perm m1 b0 ofs0 Max Nonempty)), Logic.or (Mem.perm m1' b0 ofs0 k p) (not (Mem.perm m1' b0 ofs0 Max Nonempty)) *)
  intuition eauto using Mem.perm_storebytes_1, Mem.perm_storebytes_2.
- rewrite (Mem.storebytes_mem_contents _ _ _ _ _ H0).
(* Goal: memval_lessdef (@ZMap.get memval ofs0 (if peq b0 b then Mem.setN bytes1 ofs (@PMap.get (ZMap.t memval) b (Mem.mem_contents m1)) else @PMap.get (ZMap.t memval) b0 (Mem.mem_contents m1))) (@ZMap.get memval ofs0 (@PMap.get (ZMap.t memval) b0 (Mem.mem_contents m2))) *)
  rewrite PMap.gsspec. destruct (peq b0 b).
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
+ subst b0. rewrite Mem.setN_outside. eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  destruct (zlt ofs0 ofs); auto. destruct (zle (ofs + Z.of_nat (length bytes1)) ofs0); try omega.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  elim (H1 ofs0). omega. auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
+ eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto.
- rewrite (Mem.nextblock_storebytes _ _ _ _ _ H0).
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply ma_nextblock; eauto.
Qed.

Lemma magree_store_left:
  forall m1 m2 P chunk b ofs v1 m1',
  magree m1 m2 P ->
  Mem.store chunk m1 b ofs v1 = Some m1' ->
  (forall i, ofs <= i < ofs + size_chunk chunk -> ~(P b i)) ->
  magree m1' m2 P.
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. eapply magree_storebytes_left; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply Mem.store_storebytes; eauto.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. rewrite encode_val_length in H2.
  rewrite <- size_chunk_conv in H2. apply H1; auto.
Qed.

Lemma magree_free:
  forall m1 m2 (P Q: locset) b lo hi m1',
  magree m1 m2 P ->
  Mem.free m1 b lo hi = Some m1' ->
  (forall b' i, Q b' i ->
                b' <> b \/ ~(lo <= i < hi) ->
                P b' i) ->
  exists m2', Mem.free m2 b lo hi = Some m2' /\ magree m1' m2' Q.
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros.
  destruct (Mem.range_perm_free m2 b lo hi) as [m2' FREE].
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  red; intros. eapply ma_perm; eauto. eapply Mem.free_range_perm; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exists m2'; split; auto.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  constructor; intros.
- (* permissions *)
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  assert (Mem.perm m2 b0 ofs k p). { eapply ma_perm; eauto. eapply Mem.perm_free_3; eauto. }
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit Mem.perm_free_inv; eauto. intros [[A B] | A]; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  subst b0. eelim Mem.perm_free_2. eexact H0. eauto. eauto.
- (* inverse permissions *)
  exploit ma_perm_inv; eauto using Mem.perm_free_3. intros [A|A].
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply Mem.perm_free_inv in A; eauto. destruct A as [[A B] | A]; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  subst b0; right; eapply Mem.perm_free_2; eauto.
  right; intuition eauto using Mem.perm_free_3.
- (* contents *)
  rewrite (Mem.free_result _ _ _ _ _ H0).
  rewrite (Mem.free_result _ _ _ _ _ FREE).
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  simpl. eapply ma_memval; eauto. eapply Mem.perm_free_3; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  apply H1; auto. destruct (eq_block b0 b); auto.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  subst b0. right. red; intros. eelim Mem.perm_free_2. eexact H0. eauto. eauto.
- (* nextblock *)
  rewrite (Mem.free_result _ _ _ _ _ H0).
  rewrite (Mem.free_result _ _ _ _ _ FREE).
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  simpl. eapply ma_nextblock; eauto.
Qed.

Lemma magree_valid_access:
  forall m1 m2 (P: locset) chunk b ofs p,
  magree m1 m2 P ->
  Mem.valid_access m1 chunk b ofs p ->
  Mem.valid_access m2 chunk b ofs p.
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. destruct H0; split; auto.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  red; intros. eapply ma_perm; eauto.
Qed.

(** * Properties of the need environment *)

Lemma add_need_all_eagree:
  forall e e' r ne,
  eagree e e' (add_need_all r ne) -> eagree e e' ne.
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros; red; intros. generalize (H r0). unfold add_need_all.
(* Goal: forall _ : vagree (Regmap.get val r0 e) (Regmap.get val r0 e') (NE.get r0 (NE.set r (nlub nv (NE.get r ne)) ne)), vagree (Regmap.get val r0 e) (Regmap.get val r0 e') (NE.get r0 ne) *)
  rewrite NE.gsspec. destruct (peq r0 r); auto with na.
Qed.

Lemma add_need_all_lessdef:
  forall e e' r ne,
  eagree e e' (add_need_all r ne) -> Val.lessdef e#r e'#r.
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. generalize (H r); unfold add_need_all.
(* Goal: forall _ : vagree (Regmap.get val r e) (Regmap.get val r e') (NE.get r (NE.set r (nlub nv (NE.get r ne)) ne)), vagree (Regmap.get val r e) (Regmap.get val r e') nv *)
  rewrite NE.gsspec, peq_true. auto with na.
Qed.

Lemma add_need_eagree:
  forall e e' r nv ne,
  eagree e e' (add_need r nv ne) -> eagree e e' ne.
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros; red; intros. generalize (H r0); unfold add_need.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  rewrite NE.gsspec. destruct (peq r0 r); auto.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  subst r0. intros. eapply nge_agree; eauto. apply nge_lub_r.
Qed.

Lemma add_need_vagree:
  forall e e' r nv ne,
  eagree e e' (add_need r nv ne) -> vagree e#r e'#r nv.
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. generalize (H r); unfold add_need.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  rewrite NE.gsspec, peq_true. intros. eapply nge_agree; eauto. apply nge_lub_l.
Qed.

Lemma add_needs_all_eagree:
  forall rl e e' ne,
  eagree e e' (add_needs_all rl ne) -> eagree e e' ne.
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  induction rl; simpl; intros.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  apply IHrl. eapply add_need_all_eagree; eauto.
Qed.

Lemma add_needs_all_lessdef:
  forall rl e e' ne,
  eagree e e' (add_needs_all rl ne) -> Val.lessdef_list e##rl e'##rl.
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  induction rl; simpl; intros.
(* Goal: final_state (Returnstate (@nil stackframe) (Vint r) tm) r *)
  constructor.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  constructor. eapply add_need_all_lessdef; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply IHrl. eapply add_need_all_eagree; eauto.
Qed.

Lemma add_needs_eagree:
  forall rl nvl e e' ne,
  eagree e e' (add_needs rl nvl ne) -> eagree e e' ne.
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  induction rl; simpl; intros.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  destruct nvl. apply add_needs_all_eagree with (a :: rl); auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply IHrl. eapply add_need_eagree; eauto.
Qed.

Lemma add_needs_vagree:
  forall rl nvl e e' ne,
  eagree e e' (add_needs rl nvl ne) -> vagree_list e##rl e'##rl nvl.
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  induction rl; simpl; intros.
(* Goal: final_state (Returnstate (@nil stackframe) (Vint r) tm) r *)
  constructor.
  destruct nvl.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  apply vagree_lessdef_list. eapply add_needs_all_lessdef with (rl := a :: rl); eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  constructor. eapply add_need_vagree; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply IHrl. eapply add_need_eagree; eauto.
Qed.

Lemma add_ros_need_eagree:
  forall e e' ros ne, eagree e e' (add_ros_need_all ros ne) -> eagree e e' ne.
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. destruct ros; simpl in *. eapply add_need_all_eagree; eauto. auto.
Qed.

Hint Resolve add_need_all_eagree add_need_all_lessdef
             add_need_eagree add_need_vagree
             add_needs_all_eagree add_needs_all_lessdef
             add_needs_eagree add_needs_vagree
             add_ros_need_eagree: na.

Lemma eagree_init_regs:
  forall rl vl1 vl2 ne,
  Val.lessdef_list vl1 vl2 ->
  eagree (init_regs vl1 rl) (init_regs vl2 rl) ne.
Proof.
(* Goal: Logic.or (Z.lt q p) (Z.le (Z.add p (Z.of_nat (@Datatypes.length memval (@nil memval)))) q) *)
  induction rl; intros until ne; intros LD; simpl.
- red; auto with na.
- inv LD.
  + red; auto with na.
  + apply eagree_update; auto with na.
Qed.

(** * Basic properties of the translation *)

Section PRESERVATION.

Variable prog: program.
Variable tprog: program.
Hypothesis TRANSF: match_prog prog 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 (Genv.find_symbol_match TRANSF).

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

Lemma functions_translated:
  forall (v: val) (f: RTL.fundef),
  Genv.find_funct ge v = Some f ->
  exists cu tf,
  Genv.find_funct tge v = Some tf /\ transf_fundef (romem_for cu) f = OK tf /\ linkorder cu prog.
Proof (Genv.find_funct_match TRANSF).

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

Lemma sig_function_translated:
  forall rm f tf,
  transf_fundef rm f = OK tf ->
  funsig tf = funsig f.
Proof.
(* Goal: forall (rm : romem) (f tf : fundef) (_ : @eq (res fundef) (transf_fundef rm f) (@OK fundef tf)), @eq signature (funsig tf) (funsig f) *)
  intros; destruct f; monadInv H.
(* Goal: @eq signature (funsig (@Internal function x)) (funsig (@Internal function f)) *)
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  unfold transf_function in EQ.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  destruct (analyze (ValueAnalysis.analyze rm f) f); inv EQ; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  auto.
Qed.

Lemma stacksize_translated:
  forall rm f tf,
  transf_function rm f = OK tf -> tf.(fn_stacksize) = f.(fn_stacksize).
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  unfold transf_function; intros. destruct (analyze (ValueAnalysis.analyze rm f) f); inv H; auto.
Qed.

Definition vanalyze (cu: program) (f: function) :=
  ValueAnalysis.analyze (romem_for cu) f.

Lemma transf_function_at:
  forall cu f tf an pc instr,
  transf_function (romem_for cu) f = OK tf ->
  analyze (vanalyze cu f) f = Some an ->
  f.(fn_code)!pc = Some instr ->
  tf.(fn_code)!pc = Some(transf_instr (vanalyze cu f) an pc instr).
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. unfold transf_function in H. unfold vanalyze in H0. rewrite H0 in H. inv H; simpl.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  rewrite PTree.gmap. rewrite H1; auto.
Qed.

Lemma is_dead_sound_1:
  forall nv, is_dead nv = true -> nv = Nothing.
Proof.
(* Goal: forall (nv : nval) (_ : @eq bool (is_dead nv) true), @eq nval nv Nothing *)
  destruct nv; simpl; congruence.
Qed.

Lemma is_dead_sound_2:
  forall nv, is_dead nv = false -> nv <> Nothing.
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros; red; intros. subst nv; discriminate.
Qed.

Hint Resolve is_dead_sound_1 is_dead_sound_2: na.

Lemma is_int_zero_sound:
  forall nv, is_int_zero nv = true -> nv = I Int.zero.
Proof.
(* Goal: forall (nv : nval) (_ : @eq bool (is_int_zero nv) true), @eq nval nv (I Int.zero) *)
  unfold is_int_zero; destruct nv; try discriminate.
(* Goal: forall _ : @eq bool (Int.eq m Int.zero) true, @eq nval (I m) (I Int.zero) *)
  predSpec Int.eq Int.eq_spec m Int.zero; congruence.
Qed.

Lemma find_function_translated:
  forall ros rs fd trs ne,
  find_function ge ros rs = Some fd ->
  eagree rs trs (add_ros_need_all ros ne) ->
  exists cu tfd,
     find_function tge ros trs = Some tfd
  /\ transf_fundef (romem_for cu) fd = OK tfd
  /\ linkorder cu prog.
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. destruct ros as [r|id]; simpl in *.
- assert (LD: Val.lessdef rs#r trs#r) by eauto with na. inv LD.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  apply functions_translated; auto.
  rewrite <- H2 in H; discriminate.
- rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try discriminate.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  apply function_ptr_translated; auto.
Qed.

(** * Semantic invariant *)

Inductive match_stackframes: stackframe -> stackframe -> Prop :=
  | match_stackframes_intro:
      forall res f sp pc e tf te cu an
        (LINK: linkorder cu prog)
        (FUN: transf_function (romem_for cu) f = OK tf)
        (ANL: analyze (vanalyze cu f) f = Some an)
        (RES: forall v tv,
              Val.lessdef v tv ->
              eagree (e#res <- v) (te#res<- tv)
                     (fst (transfer f (vanalyze cu f) pc an!!pc))),
      match_stackframes (Stackframe res f (Vptr sp Ptrofs.zero) pc e)
                        (Stackframe res tf (Vptr sp Ptrofs.zero) pc te).

Inductive match_states: state -> state -> Prop :=
  | match_regular_states:
      forall s f sp pc e m ts tf te tm cu an
        (STACKS: list_forall2 match_stackframes s ts)
        (LINK: linkorder cu prog)
        (FUN: transf_function (romem_for cu) f = OK tf)
        (ANL: analyze (vanalyze cu f) f = Some an)
        (ENV: eagree e te (fst (transfer f (vanalyze cu f) pc an!!pc)))
        (MEM: magree m tm (nlive ge sp (snd (transfer f (vanalyze cu f) pc an!!pc)))),
      match_states (State s f (Vptr sp Ptrofs.zero) pc e m)
                   (State ts tf (Vptr sp Ptrofs.zero) pc te tm)
  | match_call_states:
      forall s f args m ts tf targs tm cu
        (STACKS: list_forall2 match_stackframes s ts)
        (LINK: linkorder cu prog)
        (FUN: transf_fundef (romem_for cu) f = OK tf)
        (ARGS: Val.lessdef_list args targs)
        (MEM: Mem.extends m tm),
      match_states (Callstate s f args m)
                   (Callstate ts tf targs tm)
  | match_return_states:
      forall s v m ts tv tm
        (STACKS: list_forall2 match_stackframes s ts)
        (RES: Val.lessdef v tv)
        (MEM: Mem.extends m tm),
      match_states (Returnstate s v m)
                   (Returnstate ts tv tm).

(** [match_states] and CFG successors *)

Lemma analyze_successors:
  forall cu f an pc instr pc',
  analyze (vanalyze cu f) f = Some an ->
  f.(fn_code)!pc = Some instr ->
  In pc' (successors_instr instr) ->
  NA.ge an!!pc (transfer f (vanalyze cu f) pc' an!!pc').
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. eapply DS.fixpoint_solution; eauto.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. unfold transfer; rewrite H2. destruct a. apply DS.L.eq_refl.
Qed.

Lemma match_succ_states:
  forall s f sp pc e m ts tf te tm an pc' cu instr ne nm
    (LINK: linkorder cu prog)
    (STACKS: list_forall2 match_stackframes s ts)
    (FUN: transf_function (romem_for cu) f = OK tf)
    (ANL: analyze (vanalyze cu f) f = Some an)
    (INSTR: f.(fn_code)!pc = Some instr)
    (SUCC: In pc' (successors_instr instr))
    (ANPC: an!!pc = (ne, nm))
    (ENV: eagree e te ne)
    (MEM: magree m tm (nlive ge sp nm)),
  match_states (State s f (Vptr sp Ptrofs.zero) pc' e m)
               (State ts tf (Vptr sp Ptrofs.zero) pc' te tm).
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. exploit analyze_successors; eauto. rewrite ANPC; simpl. intros [A B].
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  econstructor; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply eagree_ge; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply magree_monotone; eauto.
Qed.

(** Builtin arguments and results *)

Lemma eagree_set_res:
  forall e1 e2 v1 v2 res ne,
  Val.lessdef v1 v2 ->
  eagree e1 e2 (kill_builtin_res res ne) ->
  eagree (regmap_setres res v1 e1) (regmap_setres res v2 e2) ne.
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. destruct res; simpl in *; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  apply eagree_update; eauto. apply vagree_lessdef; auto.
Qed.

Lemma transfer_builtin_arg_sound:
  forall bc e e' sp m m' a v,
  eval_builtin_arg ge (fun r => e#r) (Vptr sp Ptrofs.zero) m a v ->
  forall nv ne1 nm1 ne2 nm2,
  transfer_builtin_arg nv (ne1, nm1) a = (ne2, nm2) ->
  eagree e e' ne2 ->
  magree m m' (nlive ge sp nm2) ->
  genv_match bc ge ->
  bc sp = BCstack ->
  exists v',
     eval_builtin_arg ge (fun r => e'#r) (Vptr sp Ptrofs.zero) m' a  v'
  /\ vagree v v' nv
  /\ eagree e e' ne1
  /\ magree m m' (nlive ge sp nm1).
Proof.
  induction 1; simpl; intros until nm2; intros TR EA MA GM SPM; inv TR.
- exists e'#x; intuition auto. constructor. eauto 2 with na. eauto 2 with na.
- exists (Vint n); intuition auto. constructor. apply vagree_same.
- exists (Vlong n); intuition auto. constructor. apply vagree_same.
- exists (Vfloat n); intuition auto. constructor. apply vagree_same.
- exists (Vsingle n); intuition auto. constructor. apply vagree_same.
- simpl in H. exploit magree_load; eauto.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. eapply nlive_add; eauto with va. rewrite Ptrofs.add_zero_l in H0; auto.
  intros (v' & A & B).
(* Goal: Mem.extends m1 m2 *)
  exists v'; intuition auto. constructor; auto. apply vagree_lessdef; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply magree_monotone; eauto. intros; eapply incl_nmem_add; eauto.
- exists (Vptr sp (Ptrofs.add Ptrofs.zero ofs)); intuition auto with na. constructor.
- unfold Senv.symbol_address in H; simpl in H.
  destruct (Genv.find_symbol ge id) as [b|] eqn:FS; simpl in H; try discriminate.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit magree_load; eauto.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. eapply nlive_add; eauto. constructor. apply GM; auto.
  intros (v' & A & B).
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exists v'; intuition auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  constructor. simpl. unfold Senv.symbol_address; simpl; rewrite FS; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  apply vagree_lessdef; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply magree_monotone; eauto. intros; eapply incl_nmem_add; eauto.
- exists (Senv.symbol_address ge id ofs); intuition auto with na. constructor.
- destruct (transfer_builtin_arg All (ne1, nm1) hi) as [ne' nm'] eqn:TR.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit IHeval_builtin_arg2; eauto. intros (vlo' & A & B & C & D).
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit IHeval_builtin_arg1; eauto. intros (vhi' & P & Q & R & S).
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exists (Val.longofwords vhi' vlo'); intuition auto.
(* Goal: Mem.extends m1 m2 *)
  constructor; auto.
  apply vagree_lessdef.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  apply Val.longofwords_lessdef; apply lessdef_vagree; auto.
- destruct (transfer_builtin_arg All (ne1, nm1) a1) as [ne' nm'] eqn:TR.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit IHeval_builtin_arg2; eauto. intros (v2' & A & B & C & D).
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit IHeval_builtin_arg1; eauto. intros (v1' & P & Q & R & S).
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  econstructor; intuition auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  econstructor; eauto.
  destruct Archi.ptr64; auto using Val.add_lessdef, Val.addl_lessdef, vagree_lessdef, lessdef_vagree.
Qed.

Lemma transfer_builtin_args_sound:
  forall e sp m e' m' bc al vl,
  eval_builtin_args ge (fun r => e#r) (Vptr sp Ptrofs.zero) m al vl ->
  forall ne1 nm1 ne2 nm2,
  transfer_builtin_args (ne1, nm1) al = (ne2, nm2) ->
  eagree e e' ne2 ->
  magree m m' (nlive ge sp nm2) ->
  genv_match bc ge ->
  bc sp = BCstack ->
  exists vl',
     eval_builtin_args ge (fun r => e'#r) (Vptr sp Ptrofs.zero) m' al vl'
  /\ Val.lessdef_list vl vl'
  /\ eagree e e' ne1
  /\ magree m m' (nlive ge sp nm1).
Proof.
Local Opaque transfer_builtin_arg.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  induction 1; simpl; intros.
- inv H. exists (@nil val); intuition auto. constructor.
- destruct (transfer_builtin_arg All (ne1, nm1) a1) as [ne' nm'] eqn:TR.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit IHlist_forall2; eauto. intros (vs' & A1 & B1 & C1 & D1).
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit transfer_builtin_arg_sound; eauto. intros (v1' & A2 & B2 & C2 & D2).
(* Goal: Mem.extends m1 m2 *)
  exists (v1' :: vs'); intuition auto. constructor; auto.
Qed.

Lemma can_eval_builtin_arg:
  forall sp e m e' m' P,
  magree m m' P ->
  forall a v,
  eval_builtin_arg ge (fun r => e#r) (Vptr sp Ptrofs.zero) m a v ->
  exists v', eval_builtin_arg tge (fun r => e'#r) (Vptr sp Ptrofs.zero) m' a v'.
Proof.
(* Goal: forall (sp : block) (e : Regmap.t val) (m : Mem.mem) (e' : Regmap.t val) (m' : Mem.mem) (P : locset) (_ : magree m m' P) (a : builtin_arg positive) (v : val) (_ : @eval_builtin_arg positive (@Genv.to_senv fundef unit ge) (fun r : positive => Regmap.get val r e) (Vptr sp Ptrofs.zero) m a v), @ex val (fun v' : val => @eval_builtin_arg positive (@Genv.to_senv fundef unit tge) (fun r : positive => Regmap.get val r e') (Vptr sp Ptrofs.zero) m' a v') *)
  intros until P; intros MA.
  assert (LD: forall chunk addr v,
              Mem.loadv chunk m addr = Some v ->
              exists v', Mem.loadv chunk m' addr = Some v').
(* Goal: forall (chunk : memory_chunk) (addr v : val) (_ : @eq (option val) (Mem.loadv chunk m addr) (@Some val v)), @ex val (fun v' : val => @eq (option val) (Mem.loadv chunk m' addr) (@Some val v')) *)
(* Goal: forall (a : builtin_arg positive) (v : val) (_ : @eval_builtin_arg positive (@Genv.to_senv fundef unit ge) (fun r : positive => Regmap.get val r e) (Vptr sp Ptrofs.zero) m a v), @ex val (fun v' : val => @eval_builtin_arg positive (@Genv.to_senv fundef unit tge) (fun r : positive => Regmap.get val r e') (Vptr sp Ptrofs.zero) m' a v') *)
  {
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
    intros. destruct addr; simpl in H; try discriminate.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
    eapply Mem.valid_access_load. eapply magree_valid_access; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
    eapply Mem.load_valid_access; eauto. }
(* Goal: forall (a : builtin_arg positive) (v : val) (_ : @eval_builtin_arg positive (@Genv.to_senv fundef unit ge) (fun r : positive => Regmap.get val r e) (Vptr sp Ptrofs.zero) m a v), @ex val (fun v' : val => @eval_builtin_arg positive (@Genv.to_senv fundef unit tge) (fun r : positive => Regmap.get val r e') (Vptr sp Ptrofs.zero) m' a v') *)
  induction 1; try (econstructor; now constructor).
(* Goal: Mem.extends m1 m2 *)
- exploit LD; eauto. intros (v' & A). exists v'; constructor; auto.
- exploit LD; eauto. intros (v' & A). exists v'; constructor.
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit prog)) (@Some block b) *)
(* Goal: @eq ident (@prog_main fundef unit prog) (@prog_main fundef unit tprog) *)
(* Goal: @eq signature (funsig tf) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) tf (@nil val) m0) *)
  unfold Senv.symbol_address, Senv.find_symbol. rewrite symbols_preserved. assumption.
- destruct IHeval_builtin_arg1 as (v1' & A1).
(* Goal: @ex val (fun v' : val => @eval_builtin_arg positive (@Genv.to_senv fundef unit tge) (fun r : positive => Regmap.get val r e') (Vptr sp Ptrofs.zero) m' (@BA_addptr positive a1 a2) v') *)
  destruct IHeval_builtin_arg2 as (v2' & A2).
(* Goal: Mem.extends m1 m2 *)
  exists (Val.longofwords v1' v2'); constructor; auto.
- destruct IHeval_builtin_arg1 as (v1' & A1).
(* Goal: @ex val (fun v' : val => @eval_builtin_arg positive (@Genv.to_senv fundef unit tge) (fun r : positive => Regmap.get val r e') (Vptr sp Ptrofs.zero) m' (@BA_addptr positive a1 a2) v') *)
  destruct IHeval_builtin_arg2 as (v2' & A2).
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  econstructor; econstructor; eauto.
Qed.

Lemma can_eval_builtin_args:
  forall sp e m e' m' P,
  magree m m' P ->
  forall al vl,
  eval_builtin_args ge (fun r => e#r) (Vptr sp Ptrofs.zero) m al vl ->
  exists vl', eval_builtin_args tge (fun r => e'#r) (Vptr sp Ptrofs.zero) m' al vl'.
Proof.
  induction 2.
- exists (@nil val); constructor.
- exploit can_eval_builtin_arg; eauto. intros (v' & A).
  destruct IHlist_forall2 as (vl' & B).
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exists (v' :: vl'); constructor; eauto.
Qed.

(** Properties of volatile memory accesses *)

Lemma transf_volatile_store:
  forall v1 v2 v1' v2' m tm chunk sp nm t v m',
  volatile_store_sem chunk ge (v1::v2::nil) m t v m' ->
  Val.lessdef v1 v1' ->
  vagree v2 v2' (store_argument chunk) ->
  magree m tm (nlive ge sp nm) ->
  v = Vundef /\
  exists tm', volatile_store_sem chunk ge (v1'::v2'::nil) tm t Vundef tm'
           /\ magree m' tm' (nlive ge sp nm).
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. inv H. split; auto.
(* Goal: final_state st2 r *)
  inv H0. inv H9.
- (* volatile *)
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exists tm; split; auto. econstructor. econstructor; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply eventval_match_lessdef; eauto. apply store_argument_load_result; auto.
- (* not volatile *)
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit magree_store_parallel. eauto. eauto. eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  instantiate (1 := nlive ge sp nm). auto.
  intros (tm' & P & Q).
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exists tm'; split. econstructor. econstructor; eauto. auto.
Qed.

Lemma eagree_set_undef:
  forall e1 e2 ne r, eagree e1 e2 ne -> eagree (e1#r <- Vundef) e2 ne.
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros; red; intros. rewrite PMap.gsspec. destruct (peq r0 r); auto with na.
Qed.

(** * The simulation diagram *)

Theorem step_simulation:
  forall S1 t S2, step ge S1 t S2 ->
  forall S1', match_states S1 S1' -> sound_state prog S1 ->
  exists S2', step tge S1' t S2' /\ match_states S2 S2'.
Proof.

Ltac TransfInstr :=
  match goal with
  | [INSTR: (fn_code _)!_ = Some _,
     FUN: transf_function _ _ = OK _,
     ANL: analyze _ _ = Some _ |- _ ] =>
       generalize (transf_function_at _ _ _ _ _ _ FUN ANL INSTR);
       let TI := fresh "TI" in
       intro TI; unfold transf_instr in TI
  end.

Ltac UseTransfer :=
  match goal with
  | [INSTR: (fn_code _)!?pc = Some _,
     ANL: analyze _ _ = Some ?an |- _ ] =>
       destruct (an!!pc) as [ne nm] eqn:ANPC;
       unfold transfer in *;
       rewrite INSTR in *;
       simpl in *
  end.

  induction 1; intros S1' MS SS; inv MS.

- (* nop *)
  TransfInstr; UseTransfer.
  econstructor; split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply exec_Inop; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply match_succ_states; eauto. simpl; auto.

- (* op *)
  TransfInstr; UseTransfer.
  destruct (is_dead (nreg ne res)) eqn:DEAD;
  [idtac|destruct (is_int_zero (nreg ne res)) eqn:INTZERO;
  [idtac|destruct (operation_is_redundant op (nreg ne res)) eqn:REDUNDANT]].
+ (* dead instruction, turned into a nop *)
  econstructor; split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply exec_Inop; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply match_succ_states; eauto. simpl; auto.
(* Goal: forall _ : vagree (Regmap.get val r e) (Regmap.get val r e') All, Val.lessdef (Regmap.get val r e) (Regmap.get val r e') *)
  apply eagree_update_dead; auto with na.
+ (* instruction with needs = [I Int.zero], turned into a load immediate of zero. *)
  econstructor; split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply exec_Iop with (v := Vint Int.zero); eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply match_succ_states; eauto. simpl; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  apply eagree_update; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  rewrite is_int_zero_sound by auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  destruct v; simpl; auto. apply iagree_zero.
+ (* redundant operation *)
  destruct args.
  * (* kept as is because no arguments -- should never happen *)
  simpl in *.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit needs_of_operation_sound. eapply ma_perm; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eauto. instantiate (1 := nreg ne res). eauto with na. eauto with na. intros [tv [A B]].
  econstructor; split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply exec_Iop with (v := tv); eauto.
  rewrite <- A. apply eval_operation_preserved. exact symbols_preserved.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply match_succ_states; eauto. simpl; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  apply eagree_update; auto.
  * (* turned into a move *)
  unfold fst in ENV. unfold snd in MEM. simpl in H0.
  assert (VA: vagree v te#r (nreg ne res)).
(* Goal: forall (chunk : memory_chunk) (addr v : val) (_ : @eq (option val) (Mem.loadv chunk m addr) (@Some val v)), @ex val (fun v' : val => @eq (option val) (Mem.loadv chunk m' addr) (@Some val v')) *)
(* Goal: forall (a : builtin_arg positive) (v : val) (_ : @eval_builtin_arg positive (@Genv.to_senv fundef unit ge) (fun r : positive => Regmap.get val r e) (Vptr sp Ptrofs.zero) m a v), @ex val (fun v' : val => @eval_builtin_arg positive (@Genv.to_senv fundef unit tge) (fun r : positive => Regmap.get val r e') (Vptr sp Ptrofs.zero) m' a v') *)
  { eapply operation_is_redundant_sound with (arg1' := te#r) (args' := te##args).
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
    eauto. eauto. exploit add_needs_vagree; eauto. }
  econstructor; split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply exec_Iop; eauto. simpl; reflexivity.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply match_succ_states; eauto. simpl; auto.
  eapply eagree_update; eauto 2 with na.
+ (* preserved operation *)
  simpl in *.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit needs_of_operation_sound. eapply ma_perm; eauto. eauto. eauto 2 with na. eauto with na.
  intros [tv [A B]].
  econstructor; split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply exec_Iop with (v := tv); eauto.
  rewrite <- A. apply eval_operation_preserved. exact symbols_preserved.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply match_succ_states; eauto. simpl; auto.
  apply eagree_update; eauto 2 with na.

- (* load *)
  TransfInstr; UseTransfer.
  destruct (is_dead (nreg ne dst)) eqn:DEAD;
  [idtac|destruct (is_int_zero (nreg ne dst)) eqn:INTZERO];
  simpl in *.
+ (* dead instruction, turned into a nop *)
  econstructor; split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply exec_Inop; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply match_succ_states; eauto. simpl; auto.
(* Goal: forall _ : vagree (Regmap.get val r e) (Regmap.get val r e') All, Val.lessdef (Regmap.get val r e) (Regmap.get val r e') *)
  apply eagree_update_dead; auto with na.
+ (* instruction with needs = [I Int.zero], turned into a load immediate of zero. *)
  econstructor; split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply exec_Iop with (v := Vint Int.zero); eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply match_succ_states; eauto. simpl; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  apply eagree_update; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  rewrite is_int_zero_sound by auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  destruct v; simpl; auto. apply iagree_zero.
+ (* preserved *)
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit eval_addressing_lessdef. eapply add_needs_all_lessdef; eauto. eauto.
  intros (ta & U & V). inv V; try discriminate.
  destruct ta; simpl in H1; try discriminate.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit magree_load; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit aaddressing_sound; eauto. intros (bc & A & B & C).
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. apply nlive_add with bc i; assumption.
  intros (tv & P & Q).
  econstructor; split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply exec_Iload with (a := Vptr b i). eauto.
  rewrite <- U. apply eval_addressing_preserved. exact symbols_preserved.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply match_succ_states; eauto. simpl; auto.
  apply eagree_update; eauto 2 with na.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto.

- (* store *)
  TransfInstr; UseTransfer.
  destruct (nmem_contains nm (aaddressing (vanalyze cu f) # pc addr args)
             (size_chunk chunk)) eqn:CONTAINS.
+ (* preserved *)
  simpl in *.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit eval_addressing_lessdef. eapply add_needs_all_lessdef; eauto. eauto.
  intros (ta & U & V). inv V; try discriminate.
  destruct ta; simpl in H1; try discriminate.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit magree_store_parallel. eauto. eauto. instantiate (1 := te#src). eauto with na.
  instantiate (1 := nlive ge sp0 nm).
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit aaddressing_sound; eauto. intros (bc & A & B & C).
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. apply nlive_remove with bc b i; assumption.
  intros (tm' & P & Q).
  econstructor; split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply exec_Istore with (a := Vptr b i). eauto.
  rewrite <- U. apply eval_addressing_preserved. exact symbols_preserved.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply match_succ_states; eauto. simpl; auto.
  eauto 3 with na.
+ (* dead instruction, turned into a nop *)
  destruct a; simpl in H1; try discriminate.
  econstructor; split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply exec_Inop; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply match_succ_states; eauto. simpl; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply magree_store_left; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit aaddressing_sound; eauto. intros (bc & A & B & C).
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. eapply nlive_contains; eauto.

- (* call *)
  TransfInstr; UseTransfer.
  exploit find_function_translated; eauto 2 with na. intros (cu' & tfd & A & B & C).
  econstructor; split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply exec_Icall; eauto. eapply sig_function_translated; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply match_call_states with (cu := cu'); eauto.
(* Goal: Mem.extends m1 m2 *)
  constructor; auto. eapply match_stackframes_intro with (cu := cu); eauto.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  edestruct analyze_successors; eauto. simpl; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply eagree_ge; eauto. rewrite ANPC. simpl.
(* Goal: forall _ : vagree (Regmap.get val r e) (Regmap.get val r e') All, Val.lessdef (Regmap.get val r e) (Regmap.get val r e') *)
  apply eagree_update; eauto with na.
  eauto 2 with na.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply magree_extends; eauto. apply nlive_all.

- (* tailcall *)
  TransfInstr; UseTransfer.
  exploit find_function_translated; eauto 2 with na. intros (cu' & tfd & A & B & L).
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit magree_free. eauto. eauto. instantiate (1 := nlive ge stk nmem_all).
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  intros; eapply nlive_dead_stack; eauto.
  intros (tm' & C & D).
  econstructor; split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply exec_Itailcall; eauto. eapply sig_function_translated; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  erewrite stacksize_translated by eauto. eexact C.
  eapply match_call_states with (cu := cu'); eauto 2 with na.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply magree_extends; eauto. apply nlive_all.

- (* builtin *)
  TransfInstr; UseTransfer. revert ENV MEM TI.
  functional induction (transfer_builtin (vanalyze cu f)#pc ef args res ne nm);
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  simpl in *; intros.
+ (* volatile load *)
(* Goal: final_state st2 r *)
  inv H0. inv H6. rename b1 into v1.
  destruct (transfer_builtin_arg All
              (kill_builtin_res res ne,
              nmem_add nm (aaddr_arg (vanalyze cu f) # pc a1)
                (size_chunk chunk)) a1) as (ne1, nm1) eqn: TR.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  InvSoundState. exploit transfer_builtin_arg_sound; eauto.
  intros (tv1 & A & B & C & D).
  inv H1. simpl in B. inv B.
  assert (X: exists tvres, volatile_load ge chunk tm b ofs t tvres /\ Val.lessdef vres tvres).
(* Goal: forall (chunk : memory_chunk) (addr v : val) (_ : @eq (option val) (Mem.loadv chunk m addr) (@Some val v)), @ex val (fun v' : val => @eq (option val) (Mem.loadv chunk m' addr) (@Some val v')) *)
(* Goal: forall (a : builtin_arg positive) (v : val) (_ : @eval_builtin_arg positive (@Genv.to_senv fundef unit ge) (fun r : positive => Regmap.get val r e) (Vptr sp Ptrofs.zero) m a v), @ex val (fun v' : val => @eval_builtin_arg positive (@Genv.to_senv fundef unit tge) (fun r : positive => Regmap.get val r e') (Vptr sp Ptrofs.zero) m' a v') *)
  {
    inv H2.
(* Goal: Mem.extends m1 m2 *)
  * exists (Val.load_result chunk v); split; auto. constructor; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  * exploit magree_load; eauto.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
    exploit aaddr_arg_sound_1; eauto. rewrite <- AN. intros.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
    intros. eapply nlive_add; eassumption.
    intros (tv & P & Q).
(* Goal: Mem.extends m1 m2 *)
    exists tv; split; auto. constructor; auto.
  }
  destruct X as (tvres & P & Q).
  econstructor; split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply exec_Ibuiltin; eauto.
  apply eval_builtin_args_preserved with (ge1 := ge). exact symbols_preserved.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  constructor. eauto. constructor.
  eapply external_call_symbols_preserved. apply senv_preserved.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  constructor. simpl. eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply match_succ_states; eauto. simpl; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  apply eagree_set_res; auto.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto.
+ (* volatile store *)
(* Goal: final_state st2 r *)
  inv H0. inv H6. inv H7. rename b1 into v1. rename b0 into v2.
  destruct (transfer_builtin_arg (store_argument chunk)
              (kill_builtin_res res ne, nm) a2) as (ne2, nm2) eqn: TR2.
  destruct (transfer_builtin_arg All (ne2, nm2) a1) as (ne1, nm1) eqn: TR1.
  InvSoundState.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit transfer_builtin_arg_sound. eexact H4. eauto. eauto. eauto. eauto. eauto.
  intros (tv1 & A1 & B1 & C1 & D1).
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit transfer_builtin_arg_sound. eexact H3. eauto. eauto. eauto. eauto. eauto.
  intros (tv2 & A2 & B2 & C2 & D2).
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit transf_volatile_store; eauto.
  intros (EQ & tm' & P & Q). subst vres.
  econstructor; split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply exec_Ibuiltin; eauto.
  apply eval_builtin_args_preserved with (ge1 := ge). exact symbols_preserved.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  constructor. eauto. constructor. eauto. constructor.
  eapply external_call_symbols_preserved. apply senv_preserved.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  simpl; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply match_succ_states; eauto. simpl; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  apply eagree_set_res; auto.
+ (* memcpy *)
  rewrite e1 in TI.
(* Goal: final_state st2 r *)
  inv H0. inv H6. inv H7. rename b1 into v1. rename b0 into v2.
  set (adst := aaddr_arg (vanalyze cu f) # pc dst) in *.
  set (asrc := aaddr_arg (vanalyze cu f) # pc src) in *.
  destruct (transfer_builtin_arg All
              (kill_builtin_res res ne,
               nmem_add (nmem_remove nm adst sz) asrc sz) dst)
           as (ne2, nm2) eqn: TR2.
  destruct (transfer_builtin_arg All (ne2, nm2) src) as (ne1, nm1) eqn: TR1.
  InvSoundState.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit transfer_builtin_arg_sound. eexact H3. eauto. eauto. eauto. eauto. eauto.
  intros (tv1 & A1 & B1 & C1 & D1).
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit transfer_builtin_arg_sound. eexact H4. eauto. eauto. eauto. eauto. eauto.
  intros (tv2 & A2 & B2 & C2 & D2).
  inv H1.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit magree_loadbytes. eauto. eauto.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. eapply nlive_add; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  unfold asrc, vanalyze; rewrite AN; eapply aaddr_arg_sound_1; eauto.
  intros (tbytes & P & Q).
  exploit magree_storebytes_parallel.
  eapply magree_monotone. eexact D2.
  instantiate (1 := nlive ge sp0 (nmem_remove nm adst sz)).
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. apply incl_nmem_add; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eauto.
  instantiate (1 := nlive ge sp0 nm).
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. eapply nlive_remove; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  unfold adst, vanalyze; rewrite AN; eapply aaddr_arg_sound_1; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  erewrite Mem.loadbytes_length in H1 by eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  rewrite nat_of_Z_eq in H1 by omega. auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eauto.
  intros (tm' & A & B).
  econstructor; split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply exec_Ibuiltin; eauto.
  apply eval_builtin_args_preserved with (ge1 := ge). exact symbols_preserved.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  constructor. eauto. constructor. eauto. constructor.
  eapply external_call_symbols_preserved. apply senv_preserved.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  simpl in B1; inv B1. simpl in B2; inv B2. econstructor; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply match_succ_states; eauto. simpl; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  apply eagree_set_res; auto.
+ (* memcpy eliminated *)
  rewrite e1 in TI.
(* Goal: final_state st2 r *)
  inv H0. inv H6. inv H7. rename b1 into v1. rename b0 into v2.
  set (adst := aaddr_arg (vanalyze cu f) # pc dst) in *.
  set (asrc := aaddr_arg (vanalyze cu f) # pc src) in *.
  inv H1.
  econstructor; split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply exec_Inop; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply match_succ_states; eauto. simpl; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  destruct res; auto. apply eagree_set_undef; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply magree_storebytes_left; eauto.
  clear H3.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit aaddr_arg_sound; eauto.
  intros (bc & A & B & C).
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. eapply nlive_contains; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  erewrite Mem.loadbytes_length in H0 by eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  rewrite nat_of_Z_eq in H0 by omega. auto.
+ (* annot *)
  destruct (transfer_builtin_args (kill_builtin_res res ne, nm) _x2) as (ne1, nm1) eqn:TR.
  InvSoundState.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit transfer_builtin_args_sound; eauto. intros (tvl & A & B & C & D).
  inv H1.
  econstructor; split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply exec_Ibuiltin; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  apply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
  eapply external_call_symbols_preserved. apply senv_preserved.
(* Goal: final_state (Returnstate (@nil stackframe) (Vint r) tm) r *)
  constructor. eapply eventval_list_match_lessdef; eauto 2 with na.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply match_succ_states; eauto. simpl; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  apply eagree_set_res; auto.
+ (* annot val *)
  destruct (transfer_builtin_args (kill_builtin_res res ne, nm) _x2) as (ne1, nm1) eqn:TR.
  InvSoundState.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit transfer_builtin_args_sound; eauto. intros (tvl & A & B & C & D).
  inv H1. inv B. inv H6.
  econstructor; split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply exec_Ibuiltin; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  apply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
  eapply external_call_symbols_preserved. apply senv_preserved.
(* Goal: final_state (Returnstate (@nil stackframe) (Vint r) tm) r *)
  constructor.
  eapply eventval_match_lessdef; eauto 2 with na.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply match_succ_states; eauto. simpl; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  apply eagree_set_res; auto.
+ (* debug *)
  inv H1.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit can_eval_builtin_args; eauto. intros (vargs' & A).
  econstructor; split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply exec_Ibuiltin; eauto. constructor.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply match_succ_states; eauto. simpl; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  apply eagree_set_res; auto.
+ (* all other builtins *)
  assert ((fn_code tf)!pc = Some(Ibuiltin _x _x0 res pc')).
(* Goal: forall (chunk : memory_chunk) (addr v : val) (_ : @eq (option val) (Mem.loadv chunk m addr) (@Some val v)), @ex val (fun v' : val => @eq (option val) (Mem.loadv chunk m' addr) (@Some val v')) *)
(* Goal: forall (a : builtin_arg positive) (v : val) (_ : @eval_builtin_arg positive (@Genv.to_senv fundef unit ge) (fun r : positive => Regmap.get val r e) (Vptr sp Ptrofs.zero) m a v), @ex val (fun v' : val => @eval_builtin_arg positive (@Genv.to_senv fundef unit tge) (fun r : positive => Regmap.get val r e') (Vptr sp Ptrofs.zero) m' a v') *)
  {
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
    destruct _x; auto. destruct _x0; auto. destruct _x0; auto. destruct _x0; auto. contradiction.
  }
  clear y TI.
  destruct (transfer_builtin_args (kill_builtin_res res ne, nmem_all) _x0) as (ne1, nm1) eqn:TR.
  InvSoundState.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit transfer_builtin_args_sound; eauto. intros (tvl & A & B & C & D).
  exploit external_call_mem_extends; eauto 2 with na.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  eapply magree_extends; eauto. intros. apply nlive_all.
  intros (v' & tm' & P & Q & R & S).
  econstructor; split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply exec_Ibuiltin; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  apply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply external_call_symbols_preserved. apply senv_preserved. eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply match_succ_states; eauto. simpl; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  apply eagree_set_res; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply mextends_agree; eauto.

- (* conditional *)
  TransfInstr; UseTransfer. destruct (peq ifso ifnot).
+ replace (if b then ifso else ifnot) with ifso by (destruct b; congruence).
  econstructor; split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply exec_Inop; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply match_succ_states; eauto. simpl; auto.
+ econstructor; split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply exec_Icond; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply needs_of_condition_sound. eapply ma_perm; eauto. eauto. eauto with na.
  eapply match_succ_states; eauto 2 with na.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  simpl; destruct b; auto.

- (* jumptable *)
  TransfInstr; UseTransfer.
  assert (LD: Val.lessdef rs#arg te#arg) by eauto 2 with na.
(* Goal: @ex program (fun cu : program => @ex fundef (fun tfd : fundef => Logic.and (@eq (option fundef) (@Genv.find_funct fundef unit tge (Regmap.get val r trs)) (@Some fundef tfd)) (Logic.and (@eq (res fundef) (transf_fundef (romem_for cu) fd) (@OK fundef tfd)) (@linkorder program (@Linker_prog fundef unit (Linker_fundef function) Linker_unit) cu prog)))) *)
  rewrite H0 in LD. inv LD.
  econstructor; split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply exec_Ijumptable; eauto.
  eapply match_succ_states; eauto 2 with na.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  simpl. eapply list_nth_z_in; eauto.

- (* return *)
  TransfInstr; UseTransfer.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit magree_free. eauto. eauto. instantiate (1 := nlive ge stk nmem_all).
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  intros; eapply nlive_dead_stack; eauto.
  intros (tm' & A & B).
  econstructor; split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply exec_Ireturn; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  erewrite stacksize_translated by eauto. eexact A.
(* Goal: Mem.extends m1 m2 *)
  constructor; auto.
  destruct or; simpl; eauto 2 with na.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply magree_extends; eauto. apply nlive_all.

- (* internal function *)
  monadInv FUN. generalize EQ. unfold transf_function. fold (vanalyze cu f). intros EQ'.
  destruct (analyze (vanalyze cu f) f) as [an|] eqn:AN; inv EQ'.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit Mem.alloc_extends; eauto. apply Z.le_refl. apply Z.le_refl.
  intros (tm' & A & B).
  econstructor; split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  econstructor; simpl; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  simpl. econstructor; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  apply eagree_init_regs; auto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  apply mextends_agree; auto.

- (* external function *)
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit external_call_mem_extends; eauto.
  intros (res' & tm' & A & B & C & D).
  simpl in FUN. inv FUN.
  econstructor; split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  econstructor; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  econstructor; eauto.

- (* return *)
  inv STACKS. inv H1.
  econstructor; split.
(* Goal: final_state (Returnstate (@nil stackframe) (Vint r) tm) r *)
  constructor.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  econstructor; eauto. apply mextends_agree; auto.
Qed.

Lemma transf_initial_states:
  forall st1, initial_state prog st1 ->
  exists st2, initial_state tprog st2 /\ match_states st1 st2.
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. inversion H.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exploit function_ptr_translated; eauto. intros (cu & tf & A & B & C).
(* Goal: @ex state (fun st2 : state => Logic.and (initial_state tprog st2) (match_states (Callstate (@nil stackframe) f (@nil val) m0) st2)) *)
  exists (Callstate nil tf nil m0); split.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  econstructor; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  eapply (Genv.init_mem_match TRANSF); eauto.
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig tf) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) tf (@nil val) m0) *)
  replace (prog_main tprog) with (prog_main prog).
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  rewrite symbols_preserved. eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  symmetry; eapply match_program_main; eauto.
  rewrite <- H3. eapply sig_function_translated; eauto.
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  econstructor; eauto. constructor. apply Mem.extends_refl.
Qed.

Lemma transf_final_states:
  forall st1 st2 r,
  match_states st1 st2 -> final_state st1 r -> final_state st2 r.
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros. inv H0. inv H. inv STACKS. inv RES. constructor.
Qed.

(** * Semantic preservation *)

Theorem transf_program_correct:
  forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
Proof.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
  intros.
  apply forward_simulation_step with
     (match_states := fun s1 s2 => sound_state prog s1 /\ match_states s1 s2).
- apply senv_preserved.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
- simpl; intros. exploit transf_initial_states; eauto. intros [st2 [A B]].
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exists st2; intuition. eapply sound_initial; eauto.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
- simpl; intros. destruct H. eapply transf_final_states; eauto.
(* Goal: forward_simulation (semantics prog) (semantics tprog) *)
- simpl; intros. destruct H0.
(* Goal: @ex state (fun s2' : state => Logic.and (step (@Genv.globalenv fundef unit tprog) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  assert (sound_state prog s1') by (eapply sound_step; eauto).
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  fold ge; fold tge. exploit step_simulation; eauto. intros [st2' [A B]].
(* Goal: @eq signature (funsig (@External function e)) (funsig (@External function e)) *)
  exists st2'; auto.
Qed.

End PRESERVATION.
