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

(** Correctness proof for common subexpression elimination. *)

Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
Require Import AST Linking.
Require Import Values Memory Events Globalenvs Smallstep.
Require Import Op Registers RTL.
Require Import ValueDomain ValueAOp ValueAnalysis.
Require Import CSEdomain CombineOp CombineOpproof CSE.

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: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  intros. eapply match_transform_partial_program_contextual; eauto.
Qed.

(** * Soundness of operations over value numberings *)

Remark wf_equation_incr:
  forall next1 next2 e,
  wf_equation next1 e -> Ple next1 next2 -> wf_equation next2 e.
Proof.
(* Goal: forall (next1 : CSEdomain.valnum) (next2 : positive) (e : equation) (_ : wf_equation next1 e) (_ : Ple next1 next2), wf_equation next2 e *)
  unfold wf_equation; intros; destruct e. destruct H. split.
(* Goal: Plt v0 next2 *)
  apply Pos.lt_le_trans with next1; auto.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  red; intros. apply Pos.lt_le_trans with next1; auto. apply H1; auto.
Qed.

(** Extensionality with respect to valuations. *)

Definition valu_agree (valu1 valu2: valuation) (upto: valnum) :=
  forall v, Plt v upto -> valu2 v = valu1 v.

Section EXTEN.

Variable valu1: valuation.
Variable upto: valnum.
Variable valu2: valuation.
Hypothesis AGREE: valu_agree valu1 valu2 upto.
Variable ge: genv.
Variable sp: val.
Variable rs: regset.
Variable m: mem.

Lemma valnums_val_exten:
  forall vl,
  (forall v, In v vl -> Plt v upto) ->
  map valu2 vl = map valu1 vl.
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  intros. apply list_map_exten. intros. symmetry. auto.
Qed.

Lemma rhs_eval_to_exten:
  forall r v,
  rhs_eval_to valu1 ge sp m r v ->
  (forall v, In v (valnums_rhs r) -> Plt v upto) ->
  rhs_eval_to valu2 ge sp m r v.
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  intros. inv H; simpl in *.
(* Goal: match_states s1' s2' *)
- constructor. rewrite valnums_val_exten by assumption. auto.
(* Goal: match_states s1' s2' *)
- econstructor; eauto. rewrite valnums_val_exten by assumption. auto.
Qed.

Lemma equation_holds_exten:
  forall e,
  equation_holds valu1 ge sp m e ->
  wf_equation upto e ->
  equation_holds valu2 ge sp m e.
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  intros. destruct e. destruct H0. inv H.
(* Goal: match_states s1' s2' *)
- constructor. rewrite AGREE by auto. apply rhs_eval_to_exten; auto.
(* Goal: match_states s1' s2' *)
- econstructor. apply rhs_eval_to_exten; eauto. rewrite AGREE by auto. auto.
Qed.

Lemma numbering_holds_exten:
  forall n,
  numbering_holds valu1 ge sp rs m n ->
  Ple n.(num_next) upto ->
  numbering_holds valu2 ge sp rs m n.
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  intros. destruct H. constructor; intros.
(* Goal: match_states s1' s2' *)
- auto.
(* Goal: match_states s1' s2' *)
- apply equation_holds_exten. auto.
(* Goal: wf_equation upto eq *)
  eapply wf_equation_incr; eauto with cse.
(* Goal: match_states s1' s2' *)
- rewrite AGREE. eauto. eapply Pos.lt_le_trans; eauto. eapply wf_num_reg; eauto.
Qed.

End EXTEN.

Ltac splitall := repeat (match goal with |- _ /\ _ => split end).

Lemma valnum_reg_holds:
  forall valu1 ge sp rs m n r n' v,
  numbering_holds valu1 ge sp rs m n ->
  valnum_reg n r = (n', v) ->
  exists valu2,
     numbering_holds valu2 ge sp rs m n'
  /\ rs#r = valu2 v
  /\ valu_agree valu1 valu2 n.(num_next)
  /\ Plt v n'.(num_next)
  /\ Ple n.(num_next) n'.(num_next).
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  unfold valnum_reg; intros.
(* Goal: @ex valuation (fun valu2 : valuation => Logic.and (numbering_holds valu2 ge sp rs m n') (Logic.and (@eq val (Regmap.get val r rs) (valu2 v)) (Logic.and (valu_agree valu1 valu2 (num_next n)) (Logic.and (Plt v (num_next n')) (Ple (num_next n) (num_next n')))))) *)
  destruct (num_reg n)!r as [v'|] eqn:NR.
- inv H0. exists valu1; splitall.
(* Goal: match_states s1' s2' *)
  + auto.
  + eauto with cse.
(* Goal: match_states s1' s2' *)
  + red; auto.
  + eauto with cse.
  + apply Ple_refl.
- inv H0; simpl.
(* Goal: @ex valuation (fun valu2 : valuation => Logic.and (numbering_holds valu2 ge sp rs m (mknumbering (Pos.succ (num_next n)) (num_eqs n) (@PTree.set CSEdomain.valnum r (num_next n) (num_reg n)) (@PMap.set (list reg) (num_next n) (@cons reg r (@nil reg)) (num_val n)))) (Logic.and (@eq val (Regmap.get val r rs) (valu2 (num_next n))) (Logic.and (valu_agree valu1 valu2 (num_next n)) (Logic.and (Plt (num_next n) (Pos.succ (num_next n))) (Ple (num_next n) (Pos.succ (num_next n))))))) *)
  set (valu2 := fun vn => if peq vn n.(num_next) then rs#r else valu1 vn).
(* Goal: @ex valuation (fun valu2 : valuation => numbering_holds valu2 ge sp rs' m (mknumbering (Pos.succ (num_next n)) (@cons equation (Eq (num_next n) true rh) (num_eqs n)) (@PTree.set CSEdomain.valnum rd (num_next n) (num_reg n)) (update_reg n rd (num_next n)))) *)
  assert (AG: valu_agree valu1 valu2 n.(num_next)).
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  { red; intros. unfold valu2. apply peq_false. apply Plt_ne; auto. }
(* Goal: @ex valuation (fun valu2 : valuation => Logic.and (numbering_holds valu2 ge sp rs m (mknumbering (Pos.succ (num_next n)) (num_eqs n) (@PTree.set CSEdomain.valnum r (num_next n) (num_reg n)) (@PMap.set (list reg) (num_next n) (@cons reg r (@nil reg)) (num_val n)))) (Logic.and (@eq val (Regmap.get val r rs) (valu2 (num_next n))) (Logic.and (valu_agree valu1 valu2 (num_next n)) (Logic.and (Plt (num_next n) (Pos.succ (num_next n))) (Ple (num_next n) (Pos.succ (num_next n))))))) *)
  exists valu2; splitall.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
+ constructor; simpl; intros.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
* constructor; simpl; intros.
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
  apply wf_equation_incr with (num_next n). eauto with cse. xomega.
(* Goal: @eq val (Regmap.get val r (Regmap.set val dst (Regmap.get val src rs) rs)) (valu2 v) *)
  rewrite PTree.gsspec in H0. destruct (peq r0 r).
(* Goal: Plt (num_next n) (Pos.succ (num_next n)) *)
(* Goal: Plt v (Pos.succ (num_next n)) *)
  inv H0; xomega.
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
  apply Plt_trans_succ; eauto with cse.
(* Goal: @eq (option valnum) (@PTree.get valnum r (@PTree.set valnum rd vd (num_reg n))) (@Some positive v) *)
  rewrite PMap.gsspec in H0. destruct (peq v (num_next n)).
(* Goal: match_states s1' s2' *)
  replace r0 with r by (simpl in H0; intuition). rewrite PTree.gss. subst; auto.
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
  exploit wf_num_val; eauto with cse. intro.
(* Goal: match_states s1' s2' *)
  rewrite PTree.gso by congruence. auto.
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
* eapply equation_holds_exten; eauto with cse.
(* Goal: @eq val (Regmap.get val r rs') (valu2 v) *)
* unfold valu2. rewrite PTree.gsspec in H0. destruct (peq r0 r).
(* Goal: match_states s1' s2' *)
  inv H0. rewrite peq_true; auto.
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
  rewrite peq_false. eauto with cse. apply Plt_ne; eauto with cse.
(* Goal: match_states s1' s2' *)
+ unfold valu2. rewrite peq_true; auto.
(* Goal: match_states s1' s2' *)
+ auto.
+ xomega.
+ xomega.
Qed.

Lemma valnum_regs_holds:
  forall rl valu1 ge sp rs m n n' vl,
  numbering_holds valu1 ge sp rs m n ->
  valnum_regs n rl = (n', vl) ->
  exists valu2,
     numbering_holds valu2 ge sp rs m n'
  /\ rs##rl = map valu2 vl
  /\ valu_agree valu1 valu2 n.(num_next)
  /\ (forall v, In v vl -> Plt v n'.(num_next))
  /\ Ple n.(num_next) n'.(num_next).
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  induction rl; simpl; intros.
(* Goal: match_states s1' s2' *)
- inv H0. exists valu1; splitall; auto. red; auto. simpl; tauto. xomega.
- destruct (valnum_reg n a) as [n1 v1] eqn:V1.
(* Goal: @ex valuation (fun valu2 : valuation => Logic.and (numbering_holds valu2 ge sp rs m n') (Logic.and (@eq (list val) (@cons val (Regmap.get val a rs) (@map positive val (fun r : positive => Regmap.get val r rs) rl)) (@map CSEdomain.valnum val valu2 vl)) (Logic.and (valu_agree valu1 valu2 (num_next n)) (Logic.and (forall (v : valnum) (_ : @In valnum v vl), Plt v (num_next n')) (Ple (num_next n) (num_next n')))))) *)
  destruct (valnum_regs n1 rl) as [n2 vs] eqn:V2.
(* Goal: final_state st2 r *)
  inv H0.
(* Goal: match_states s1' s2' *)
  exploit valnum_reg_holds; eauto.
(* Goal: forall _ : @ex valuation (fun valu2 : valuation => Logic.and (numbering_holds valu2 ge sp rs m n1) (Logic.and (@eq (list val) (@map positive val (fun r : positive => Regmap.get val r rs) args) (@map CSEdomain.valnum val valu2 vl)) (Logic.and (valu_agree valu1 valu2 (num_next n)) (Logic.and (forall (v : valnum) (_ : @In valnum v vl), Plt v (num_next n1)) (Ple (num_next n) (num_next n1)))))), @ex valuation (fun valu2 : valuation => numbering_holds valu2 ge sp (Regmap.set val dst v rs) m (add_rhs n1 dst (Op op vl))) *)
  intros (valu2 & A & B & C & D & E).
(* Goal: match_states s1' s2' *)
  exploit (IHrl valu2); eauto.
(* Goal: forall _ : @ex valuation (fun valu3 : valuation => Logic.and (numbering_holds valu3 ge sp rs m n') (Logic.and (@eq (list val) (@map positive val (fun r : positive => Regmap.get val r rs) rl) (@map CSEdomain.valnum val valu3 vs)) (Logic.and (valu_agree valu2 valu3 (num_next n1)) (Logic.and (forall (v : valnum) (_ : @In valnum v vs), Plt v (num_next n')) (Ple (num_next n1) (num_next n')))))), @ex valuation (fun valu2 : valuation => Logic.and (numbering_holds valu2 ge sp rs m n') (Logic.and (@eq (list val) (@cons val (Regmap.get val a rs) (@map positive val (fun r : positive => Regmap.get val r rs) rl)) (@map CSEdomain.valnum val valu2 (@cons valnum v1 vs))) (Logic.and (valu_agree valu1 valu2 (num_next n)) (Logic.and (forall (v : valnum) (_ : @In valnum v (@cons valnum v1 vs)), Plt v (num_next n')) (Ple (num_next n) (num_next n')))))) *)
  intros (valu3 & P & Q & R & S & T).
(* Goal: @ex valuation (fun valu2 : valuation => Logic.and (numbering_holds valu2 ge sp rs m n') (Logic.and (@eq (list val) (@cons val (Regmap.get val a rs) (@map positive val (fun r : positive => Regmap.get val r rs) rl)) (@map CSEdomain.valnum val valu2 (@cons valnum v1 vs))) (Logic.and (valu_agree valu1 valu2 (num_next n)) (Logic.and (forall (v : valnum) (_ : @In valnum v (@cons valnum v1 vs)), Plt v (num_next n')) (Ple (num_next n) (num_next n')))))) *)
  exists valu3; splitall.
(* Goal: match_states s1' s2' *)
  + auto.
(* Goal: match_states s1' s2' *)
  + simpl; f_equal; auto. rewrite R; auto.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  + red; intros. transitivity (valu2 v); auto. apply R. xomega.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  + simpl; intros. destruct H0; auto. subst v1; xomega.
  + xomega.
Qed.

Lemma find_valnum_rhs_charact:
  forall rh v eqs,
  find_valnum_rhs rh eqs = Some v -> In (Eq v true rh) eqs.
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  induction eqs; simpl; intros.
- inv H.
- destruct a. destruct (strict && eq_rhs rh r) eqn:T.
(* Goal: match_states s1' s2' *)
  + InvBooleans. inv H. left; auto.
(* Goal: match_states s1' s2' *)
  + right; eauto.
Qed.

Lemma find_valnum_rhs'_charact:
  forall rh v eqs,
  find_valnum_rhs' rh eqs = Some v -> exists strict, In (Eq v strict rh) eqs.
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  induction eqs; simpl; intros.
- inv H.
- destruct a. destruct (eq_rhs rh r) eqn:T.
(* Goal: match_states s1' s2' *)
  + inv H. exists strict; auto.
(* Goal: match_states s1' s2' *)
  + exploit IHeqs; eauto. intros [s IN]. exists s; auto.
Qed.

Lemma find_valnum_num_charact:
  forall v r eqs, find_valnum_num v eqs = Some r -> In (Eq v true r) eqs.
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  induction eqs; simpl; intros.
- inv H.
- destruct a. destruct (strict && peq v v0) eqn:T.
(* Goal: match_states s1' s2' *)
  + InvBooleans. inv H. auto.
(* Goal: match_states s1' s2' *)
  + eauto.
Qed.

Lemma reg_valnum_sound:
  forall n v r valu ge sp rs m,
  reg_valnum n v = Some r ->
  numbering_holds valu ge sp rs m n ->
  rs#r = valu v.
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  unfold reg_valnum; intros. destruct (num_val n)#v as [ | r1 rl] eqn:E; inv H.
(* Goal: match_states s1' s2' *)
  eapply num_holds_reg; eauto. eapply wf_num_val; eauto with cse.
(* Goal: @In reg r (@PMap.get (list reg) v (num_val n)) *)
  rewrite E; auto with coqlib.
Qed.

Lemma regs_valnums_sound:
  forall n valu ge sp rs m,
  numbering_holds valu ge sp rs m n ->
  forall vl rl,
  regs_valnums n vl = Some rl ->
  rs##rl = map valu vl.
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  induction vl; simpl; intros.
(* Goal: match_states s1' s2' *)
- inv H0; auto.
- destruct (reg_valnum n a) as [r1|] eqn:RV1; try discriminate.
(* Goal: final_state st2 r *)
  destruct (regs_valnums n vl) as [rl1|] eqn:RVL; inv H0.
(* Goal: match_states s1' s2' *)
  simpl; f_equal. eapply reg_valnum_sound; eauto. eauto.
Qed.

Lemma find_rhs_sound:
  forall n rh r valu ge sp rs m,
  find_rhs n rh = Some r ->
  numbering_holds valu ge sp rs m n ->
  exists v, rhs_eval_to valu ge sp m rh v /\ Val.lessdef v rs#r.
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  unfold find_rhs; intros. destruct (find_valnum_rhs' rh (num_eqs n)) as [vres|] eqn:E; try discriminate.
(* Goal: match_states s1' s2' *)
  exploit find_valnum_rhs'_charact; eauto. intros [strict IN].
(* Goal: match_states s1' s2' *)
  erewrite reg_valnum_sound by eauto.
(* Goal: match_states s1' s2' *)
  exploit num_holds_eq; eauto. intros EH. inv EH.
(* Goal: match_states s1' s2' *)
- exists (valu vres); auto.
(* Goal: match_states s1' s2' *)
- exists v; auto.
Qed.

Remark in_remove:
  forall (A: Type) (eq: forall (x y: A), {x=y}+{x<>y}) x y l,
  In y (List.remove eq x l) <-> x <> y /\ In y l.
Proof.
(* Goal: forall (A : Type) (eq0 : forall x y : A, sumbool (@eq A x y) (not (@eq A x y))) (x y : A) (l : list A), iff (@In A y (@remove A eq0 x l)) (Logic.and (not (@eq A x y)) (@In A y l)) *)
  induction l; simpl.
(* Goal: match_states s1' s2' *)
  tauto.
(* Goal: iff (@In A y (if eq x a then @remove A eq x l else @cons A a (@remove A eq x l))) (Logic.and (not (@Logic.eq A x y)) (Logic.or (@Logic.eq A a y) (@In A y l))) *)
  destruct (eq x a).
(* Goal: match_states s1' s2' *)
  subst a. rewrite IHl. tauto.
(* Goal: iff (Logic.or (@Logic.eq A a y) (@In A y (@remove A eq x l))) (Logic.and (not (@Logic.eq A x y)) (Logic.or (@Logic.eq A a y) (@In A y l))) *)
  simpl. rewrite IHl. intuition congruence.
Qed.

Lemma forget_reg_charact:
  forall n rd r v,
  wf_numbering n ->
  In r (PMap.get v (forget_reg n rd)) -> r <> rd /\ In r (PMap.get v n.(num_val)).
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  unfold forget_reg; intros.
(* Goal: Logic.and (not (@eq reg r rd)) (@In reg r (@PMap.get (list reg) v (num_val n))) *)
  destruct (PTree.get rd n.(num_reg)) as [vd|] eqn:GET.
- rewrite PMap.gsspec in H0. destruct (peq v vd).
  + subst v. rewrite in_remove in H0. intuition.
(* Goal: match_states s1' s2' *)
  + split; auto. exploit wf_num_val; eauto. congruence.
(* Goal: match_states s1' s2' *)
- split; auto. exploit wf_num_val; eauto. congruence.
Qed.

Lemma update_reg_charact:
  forall n rd vd r v,
  wf_numbering n ->
  In r (PMap.get v (update_reg n rd vd)) ->
  PTree.get r (PTree.set rd vd n.(num_reg)) = Some v.
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  unfold update_reg; intros.
(* Goal: @eq (option valnum) (@PTree.get valnum r (@PTree.set valnum rd vd (num_reg n))) (@Some positive v) *)
  rewrite PMap.gsspec in H0.
(* Goal: @eq (option valnum) (@PTree.get valnum r (@PTree.set valnum rd vd (num_reg n))) (@Some positive v) *)
  destruct (peq v vd).
- subst v. destruct H0.
+ subst r. apply PTree.gss.
(* Goal: match_states s1' s2' *)
+ exploit forget_reg_charact; eauto. intros [A B].
(* Goal: match_states s1' s2' *)
  rewrite PTree.gso by auto. eapply wf_num_val; eauto.
(* Goal: match_states s1' s2' *)
- exploit forget_reg_charact; eauto. intros [A B].
(* Goal: match_states s1' s2' *)
  rewrite PTree.gso by auto. eapply wf_num_val; eauto.
Qed.

Lemma rhs_eval_to_inj:
  forall valu ge sp m rh v1 v2,
  rhs_eval_to valu ge sp m rh v1 -> rhs_eval_to valu ge sp m rh v2 -> v1 = v2.
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  intros. inv H; inv H0; congruence.
Qed.

Lemma add_rhs_holds:
  forall valu1 ge sp rs m n rd rh rs',
  numbering_holds valu1 ge sp rs m n ->
  rhs_eval_to valu1 ge sp m rh (rs'#rd) ->
  wf_rhs n.(num_next) rh ->
  (forall r, r <> rd -> rs'#r = rs#r) ->
  exists valu2, numbering_holds valu2 ge sp rs' m (add_rhs n rd rh).
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  unfold add_rhs; intros.
(* Goal: @ex valuation (fun valu2 : valuation => numbering_holds valu2 ge sp rs' m match find_valnum_rhs rh (num_eqs n) with | Some vres => mknumbering (num_next n) (num_eqs n) (@PTree.set valnum rd vres (num_reg n)) (update_reg n rd vres) | None => mknumbering (Pos.succ (num_next n)) (@cons equation (Eq (num_next n) true rh) (num_eqs n)) (@PTree.set CSEdomain.valnum rd (num_next n) (num_reg n)) (update_reg n rd (num_next n)) end) *)
  destruct (find_valnum_rhs rh n.(num_eqs)) as [vres|] eqn:FIND.

- (* A value number exists already *)
(* Goal: match_states s1' s2' *)
  exploit find_valnum_rhs_charact; eauto. intros IN.
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
  exploit wf_num_eqs; eauto with cse. intros [A B].
(* Goal: match_states s1' s2' *)
  exploit num_holds_eq; eauto. intros EH. inv EH.
(* Goal: @ex valuation (fun valu2 : valuation => numbering_holds valu2 ge sp rs' m (mknumbering (num_next n) (num_eqs n) (@PTree.set valnum rd vres (num_reg n)) (update_reg n rd vres))) *)
  assert (rs'#rd = valu1 vres) by (eapply rhs_eval_to_inj; eauto).
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  exists valu1; constructor; simpl; intros.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
+ constructor; simpl; intros.
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
  * eauto with cse.
  * rewrite PTree.gsspec in H5. destruct (peq r rd).
(* Goal: match_states s1' s2' *)
    inv H5. auto.
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
    eauto with cse.
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
  * eapply update_reg_charact; eauto with cse.
+ eauto with cse.
+ rewrite PTree.gsspec in H5. destruct (peq r rd).
(* Goal: @eq (option V) (sem op (@map valnum val valu vl)) (@Some V res) *)
(* Goal: @eq (option V) (sem op' (@map positive val (fun r : positive => Regmap.get val r rs) rl')) (@Some V res) *)
  congruence.
(* Goal: match_states s1' s2' *)
  rewrite H2 by auto. eauto with cse.

- (* Assigning a new value number *)
(* Goal: @ex valuation (fun valu2 : valuation => numbering_holds valu2 ge sp rs' m (mknumbering (Pos.succ (num_next n)) (@cons equation (Eq (num_next n) true rh) (num_eqs n)) (@PTree.set CSEdomain.valnum rd (num_next n) (num_reg n)) (update_reg n rd (num_next n)))) *)
  set (valu2 := fun v => if peq v n.(num_next) then rs'#rd else valu1 v).
(* Goal: @ex valuation (fun valu2 : valuation => numbering_holds valu2 ge sp rs' m (mknumbering (Pos.succ (num_next n)) (@cons equation (Eq (num_next n) true rh) (num_eqs n)) (@PTree.set CSEdomain.valnum rd (num_next n) (num_reg n)) (update_reg n rd (num_next n)))) *)
  assert (AG: valu_agree valu1 valu2 n.(num_next)).
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  { red; intros. unfold valu2. apply peq_false. apply Plt_ne; auto. }
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  exists valu2; constructor; simpl; intros.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
+ constructor; simpl; intros.
(* Goal: Logic.and (sound_state prog s1') (match_states s1' s2') *)
  * destruct H3. inv H3. simpl; split. xomega.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
    red; intros. apply Plt_trans_succ; eauto.
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
    apply wf_equation_incr with (num_next n). eauto with cse. xomega.
  * rewrite PTree.gsspec in H3. destruct (peq r rd).
(* Goal: Plt (num_next n) (Pos.succ (num_next n)) *)
(* Goal: Plt v (Pos.succ (num_next n)) *)
    inv H3. xomega.
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
    apply Plt_trans_succ; eauto with cse.
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
  * apply update_reg_charact; eauto with cse.
+ destruct H3. inv H3.
(* Goal: final_state (Returnstate (@nil stackframe) (Vint r) m') r *)
  constructor. unfold valu2 at 2; rewrite peq_true.
(* Goal: match_states s1' s2' *)
  eapply rhs_eval_to_exten; eauto.
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
  eapply equation_holds_exten; eauto with cse.
+ rewrite PTree.gsspec in H3. unfold valu2. destruct (peq r rd).
(* Goal: match_states s1' s2' *)
  inv H3. rewrite peq_true; auto.
(* Goal: match_states s1' s2' *)
  rewrite peq_false. rewrite H2 by auto. eauto with cse.
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
  apply Plt_ne; eauto with cse.
Qed.

Lemma add_op_holds:
  forall valu1 ge sp rs m n op (args: list reg) v dst,
  numbering_holds valu1 ge sp rs m n ->
  eval_operation ge sp op rs##args m = Some v ->
  exists valu2, numbering_holds valu2 ge sp (rs#dst <- v) m (add_op n dst op args).
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  unfold add_op; intros.
(* Goal: @ex valuation (fun valu2 : valuation => numbering_holds valu2 ge sp (Regmap.set val dst v rs) m match @is_move_operation reg op args with | Some r => let (n1, v) := valnum_reg n r in mknumbering (num_next n1) (num_eqs n1) (@PTree.set valnum dst v (num_reg n1)) (update_reg n1 dst v) | None => let (n1, vs) := valnum_regs n args in add_rhs n1 dst (Op op vs) end) *)
  destruct (is_move_operation op args) as [src|] eqn:ISMOVE.
- (* special case for moves *)
(* Goal: match_states s1' s2' *)
  exploit is_move_operation_correct; eauto. intros [A B]; subst op args.
(* Goal: final_state st2 r *)
  simpl in H0. inv H0.
(* Goal: @ex valuation (fun valu2 : valuation => numbering_holds valu2 ge sp (Regmap.set val dst (Regmap.get val src rs) rs) m (let (n1, v) := valnum_reg n src in mknumbering (num_next n1) (num_eqs n1) (@PTree.set valnum dst v (num_reg n1)) (update_reg n1 dst v))) *)
  destruct (valnum_reg n src) as [n1 vsrc] eqn:VN.
(* Goal: match_states s1' s2' *)
  exploit valnum_reg_holds; eauto.
(* Goal: forall _ : @ex valuation (fun valu2 : valuation => Logic.and (numbering_holds valu2 ge sp rs m n1) (Logic.and (@eq (list val) (@map positive val (fun r : positive => Regmap.get val r rs) args) (@map CSEdomain.valnum val valu2 vl)) (Logic.and (valu_agree valu1 valu2 (num_next n)) (Logic.and (forall (v : valnum) (_ : @In valnum v vl), Plt v (num_next n1)) (Ple (num_next n) (num_next n1)))))), @ex valuation (fun valu2 : valuation => numbering_holds valu2 ge sp (Regmap.set val dst v rs) m (add_rhs n1 dst (Op op vl))) *)
  intros (valu2 & A & B & C & D & E).
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  exists valu2; constructor; simpl; intros.
+ constructor; simpl; intros; eauto with cse.
  * rewrite PTree.gsspec in H0. destruct (peq r dst).
(* Goal: match_states s1' s2' *)
    inv H0. auto.
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
    eauto with cse.
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
  * eapply update_reg_charact; eauto with cse.
+ eauto with cse.
+ rewrite PTree.gsspec in H0. rewrite Regmap.gsspec.
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
  destruct (peq r dst). congruence. eauto with cse.

- (* general case *)
(* Goal: @ex valuation (fun valu2 : valuation => numbering_holds valu2 ge sp (Regmap.set val dst v rs) m (let (n1, vs) := valnum_regs n args in add_rhs n1 dst (Op op vs))) *)
  destruct (valnum_regs n args) as [n1 vl] eqn:VN.
(* Goal: match_states s1' s2' *)
  exploit valnum_regs_holds; eauto.
(* Goal: forall _ : @ex valuation (fun valu2 : valuation => Logic.and (numbering_holds valu2 ge sp rs m n1) (Logic.and (@eq (list val) (@map positive val (fun r : positive => Regmap.get val r rs) args) (@map CSEdomain.valnum val valu2 vl)) (Logic.and (valu_agree valu1 valu2 (num_next n)) (Logic.and (forall (v : valnum) (_ : @In valnum v vl), Plt v (num_next n1)) (Ple (num_next n) (num_next n1)))))), @ex valuation (fun valu2 : valuation => numbering_holds valu2 ge sp (Regmap.set val dst v rs) m (add_rhs n1 dst (Op op vl))) *)
  intros (valu2 & A & B & C & D & E).
(* Goal: match_states s1' s2' *)
  eapply add_rhs_holds; eauto.
(* Goal: final_state (Returnstate (@nil stackframe) (Vint r) m') r *)
+ constructor. rewrite Regmap.gss. congruence.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
+ intros. apply Regmap.gso; auto.
Qed.

Lemma add_load_holds:
  forall valu1 ge sp rs m n addr (args: list reg) a chunk v dst,
  numbering_holds valu1 ge sp rs m n ->
  eval_addressing ge sp addr rs##args = Some a ->
  Mem.loadv chunk m a = Some v ->
  exists valu2, numbering_holds valu2 ge sp (rs#dst <- v) m (add_load n dst chunk addr args).
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  unfold add_load; intros.
(* Goal: @ex valuation (fun valu2 : valuation => numbering_holds valu2 ge sp (Regmap.set val dst v rs) m (let (n1, vs) := valnum_regs n args in add_rhs n1 dst (Op op vs))) *)
  destruct (valnum_regs n args) as [n1 vl] eqn:VN.
(* Goal: match_states s1' s2' *)
  exploit valnum_regs_holds; eauto.
(* Goal: forall _ : @ex valuation (fun valu2 : valuation => Logic.and (numbering_holds valu2 ge sp rs m n1) (Logic.and (@eq (list val) (@map positive val (fun r : positive => Regmap.get val r rs) args) (@map CSEdomain.valnum val valu2 vl)) (Logic.and (valu_agree valu1 valu2 (num_next n)) (Logic.and (forall (v : valnum) (_ : @In valnum v vl), Plt v (num_next n1)) (Ple (num_next n) (num_next n1)))))), @ex valuation (fun valu2 : valuation => numbering_holds valu2 ge sp (Regmap.set val dst v rs) m (add_rhs n1 dst (Op op vl))) *)
  intros (valu2 & A & B & C & D & E).
(* Goal: match_states s1' s2' *)
  eapply add_rhs_holds; eauto.
(* Goal: match_states s1' s2' *)
+ econstructor. rewrite <- B; eauto. rewrite Regmap.gss; auto.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
+ intros. apply Regmap.gso; auto.
Qed.

Lemma set_unknown_holds:
  forall valu ge sp rs m n r v,
  numbering_holds valu ge sp rs m n ->
  numbering_holds valu ge sp (rs#r <- v) m (set_unknown n r).
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  intros; constructor; simpl; intros.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
- constructor; simpl; intros.
  + eauto with cse.
  + rewrite PTree.grspec in H0. destruct (PTree.elt_eq r0 r).
(* Goal: @ex program (fun cu : program => @ex fundef (fun tfd : fundef => Logic.and (@eq (option fundef) (@None fundef) (@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)))) *)
    discriminate.
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
    eauto with cse.
  + exploit forget_reg_charact; eauto with cse. intros [A B].
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
    rewrite PTree.gro; eauto with cse.
- eauto with cse.
- rewrite PTree.grspec in H0. destruct (PTree.elt_eq r0 r).
(* Goal: @ex program (fun cu : program => @ex fundef (fun tfd : fundef => Logic.and (@eq (option fundef) (@None fundef) (@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)))) *)
  discriminate.
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
  rewrite Regmap.gso; eauto with cse.
Qed.

Lemma set_res_unknown_holds:
  forall valu ge sp rs m n r v,
  numbering_holds valu ge sp rs m n ->
  numbering_holds valu ge sp (regmap_setres r v rs) m (set_res_unknown n r).
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  intros. destruct r; simpl; auto. apply set_unknown_holds; auto.
Qed.

Lemma kill_eqs_charact:
  forall pred l strict r eqs,
  In (Eq l strict r) (kill_eqs pred eqs) ->
  pred r = false /\ In (Eq l strict r) eqs.
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  induction eqs; simpl; intros.
(* Goal: match_states s1' s2' *)
- tauto.
- destruct a. destruct (pred r0) eqn:PRED.
(* Goal: match_states s1' s2' *)
  tauto.
(* Goal: match_states s1' s2' *)
  inv H. inv H0. auto. tauto.
Qed.

Lemma kill_equations_hold:
  forall valu ge sp rs m n pred m',
  numbering_holds valu ge sp rs m n ->
  (forall r v,
      pred r = false ->
      rhs_eval_to valu ge sp m r v ->
      rhs_eval_to valu ge sp m' r v) ->
  numbering_holds valu ge sp rs m' (kill_equations pred n).
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  intros; constructor; simpl; intros.
- constructor; simpl; intros; eauto with cse.
(* Goal: match_states s1' s2' *)
  destruct e. exploit kill_eqs_charact; eauto. intros [A B]. eauto with cse.
(* Goal: match_states s1' s2' *)
- destruct eq. exploit kill_eqs_charact; eauto. intros [A B].
(* Goal: match_states s1' s2' *)
  exploit num_holds_eq; eauto. intro EH; inv EH; econstructor; eauto.
- eauto with cse.
Qed.

Lemma kill_all_loads_hold:
  forall valu ge sp rs m n m',
  numbering_holds valu ge sp rs m n ->
  numbering_holds valu ge sp rs m' (kill_all_loads n).
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  intros. eapply kill_equations_hold; eauto.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  unfold filter_loads; intros. inv H1.
(* Goal: match_states s1' s2' *)
  constructor. rewrite <- H2. apply op_depends_on_memory_correct; auto.
(* Goal: @ex program (fun cu : program => @ex fundef (fun tfd : fundef => Logic.and (@eq (option fundef) (@None fundef) (@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)))) *)
  discriminate.
Qed.

Lemma kill_loads_after_store_holds:
  forall valu ge sp rs m n addr args a chunk v m' bc approx ae am,
  numbering_holds valu ge (Vptr sp Ptrofs.zero) rs m n ->
  eval_addressing ge (Vptr sp Ptrofs.zero) addr rs##args = Some a ->
  Mem.storev chunk m a v = Some m' ->
  genv_match bc ge ->
  bc sp = BCstack ->
  ematch bc rs ae ->
  approx = VA.State ae am ->
  numbering_holds valu ge (Vptr sp Ptrofs.zero) rs m'
                           (kill_loads_after_store approx n chunk addr args).
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  intros. apply kill_equations_hold with m; auto.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  intros. unfold filter_after_store in H6; inv H7.
(* Goal: match_states s1' s2' *)
- constructor. rewrite <- H8. apply op_depends_on_memory_correct; auto.
- destruct (regs_valnums n vl) as [rl|] eqn:RV; try discriminate.
(* Goal: match_states s1' s2' *)
  econstructor; eauto. rewrite <- H9.
(* Goal: @ex program (fun cu : program => @ex fundef (fun tfd : fundef => Logic.and (@eq (option fundef) (@None fundef) (@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)))) *)
  destruct a; simpl in H1; try discriminate.
(* Goal: @ex program (fun cu : program => @ex fundef (fun tfd : fundef => Logic.and (@eq (option fundef) (@None fundef) (@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)))) *)
  destruct a0; simpl in H9; try discriminate.
(* Goal: iff (@In A y (@cons A a (@remove A eq x l))) (Logic.and (not (@Logic.eq A x y)) (Logic.or (@Logic.eq A a y) (@In A y l))) *)
  simpl.
  rewrite negb_false_iff in H6. unfold aaddressing in H6.
(* Goal: match_states s1' s2' *)
  eapply Mem.load_store_other. eauto.
(* Goal: match_states s1' s2' *)
  eapply pdisjoint_sound. eauto.
(* Goal: match_states s1' s2' *)
  apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto.
(* Goal: match_states s1' s2' *)
  erewrite <- regs_valnums_sound by eauto. eauto with va.
  apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto with va.
Qed.

Lemma store_normalized_range_sound:
  forall bc chunk v,
  vmatch bc v (store_normalized_range chunk) ->
  Val.lessdef (Val.load_result chunk v) v.
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  intros. unfold Val.load_result; remember Archi.ptr64 as ptr64.
(* Goal: match_states s1' s2' *)
  destruct chunk; simpl in *; destruct v; auto.
(* Goal: match_states s1' s2' *)
- inv H. rewrite is_sgn_sign_ext in H4 by omega. rewrite H4; auto.
(* Goal: match_states s1' s2' *)
- inv H. rewrite is_uns_zero_ext in H4 by omega. rewrite H4; auto.
(* Goal: match_states s1' s2' *)
- inv H. rewrite is_sgn_sign_ext in H4 by omega. rewrite H4; auto.
(* Goal: match_states s1' s2' *)
- inv H. rewrite is_uns_zero_ext in H4 by omega. rewrite H4; auto.
(* Goal: match_states s1' s2' *)
- destruct ptr64; auto.
(* Goal: match_states s1' s2' *)
- destruct ptr64; auto.
(* Goal: match_states s1' s2' *)
- destruct ptr64; auto.
Qed.

Lemma add_store_result_hold:
  forall valu1 ge sp rs m' n addr args a chunk m src bc ae approx am,
  numbering_holds valu1 ge sp rs m' n ->
  eval_addressing ge sp addr rs##args = Some a ->
  Mem.storev chunk m a rs#src = Some m' ->
  ematch bc rs ae ->
  approx = VA.State ae am ->
  exists valu2, numbering_holds valu2 ge sp rs m' (add_store_result approx n chunk addr args src).
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  unfold add_store_result; intros.
  unfold avalue; rewrite H3.
  destruct (vincl (AE.get src ae) (store_normalized_range chunk)) eqn:INCL.
- destruct (valnum_reg n src) as [n1 vsrc] eqn:VR1.
  destruct (valnum_regs n1 args) as [n2 vargs] eqn:VR2.
(* Goal: match_states s1' s2' *)
  exploit valnum_reg_holds; eauto. intros (valu2 & A & B & C & D & E).
(* Goal: match_states s1' s2' *)
  exploit valnum_regs_holds; eauto. intros (valu3 & P & Q & R & S & T).
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  exists valu3. constructor; simpl; intros.
+ constructor; simpl; intros; eauto with cse.
(* Goal: Logic.and (sound_state prog s1') (match_states s1' s2') *)
  destruct H4; eauto with cse. subst e. split.
(* Goal: match_states s1' s2' *)
  eapply Pos.lt_le_trans; eauto.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  red; simpl; intros. auto.
+ destruct H4; eauto with cse. subst eq. apply eq_holds_lessdef with (Val.load_result chunk rs#src).
(* Goal: match_states s1' s2' *)
  apply load_eval_to with a. rewrite <- Q; auto.
(* Goal: match_states s1' s2' *)
  destruct a; try discriminate. simpl. eapply Mem.load_store_same; eauto.
(* Goal: match_states s1' s2' *)
  rewrite B. rewrite R by auto. apply store_normalized_range_sound with bc.
(* Goal: match_states s1' s2' *)
  rewrite <- B. eapply vmatch_ge. apply vincl_ge; eauto. apply H2.
+ eauto with cse.

(* Goal: match_states s1' s2' *)
- exists valu1; auto.
Qed.

Lemma kill_loads_after_storebytes_holds:
  forall valu ge sp rs m n dst b ofs bytes m' bc approx ae am sz,
  numbering_holds valu ge (Vptr sp Ptrofs.zero) rs m n ->
  pmatch bc b ofs dst ->
  Mem.storebytes m b (Ptrofs.unsigned ofs) bytes = Some m' ->
  genv_match bc ge ->
  bc sp = BCstack ->
  ematch bc rs ae ->
  approx = VA.State ae am ->
  length bytes = nat_of_Z sz -> sz >= 0 ->
  numbering_holds valu ge (Vptr sp Ptrofs.zero) rs m'
                           (kill_loads_after_storebytes approx n dst sz).
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  intros. apply kill_equations_hold with m; auto.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  intros. unfold filter_after_store in H8; inv H9.
(* Goal: match_states s1' s2' *)
- constructor. rewrite <- H10. apply op_depends_on_memory_correct; auto.
- destruct (regs_valnums n vl) as [rl|] eqn:RV; try discriminate.
(* Goal: match_states s1' s2' *)
  econstructor; eauto. rewrite <- H11.
(* Goal: @ex program (fun cu : program => @ex fundef (fun tfd : fundef => Logic.and (@eq (option fundef) (@None fundef) (@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)))) *)
  destruct a; simpl in H10; try discriminate.
(* Goal: iff (@In A y (@cons A a (@remove A eq x l))) (Logic.and (not (@Logic.eq A x y)) (Logic.or (@Logic.eq A a y) (@In A y l))) *)
  simpl.
  rewrite negb_false_iff in H8.
(* Goal: match_states s1' s2' *)
  eapply Mem.load_storebytes_other. eauto.
(* Goal: match_states s1' s2' *)
  rewrite H6. rewrite nat_of_Z_eq by auto.
(* Goal: match_states s1' s2' *)
  eapply pdisjoint_sound. eauto.
(* Goal: match_states s1' s2' *)
  unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto.
(* Goal: match_states s1' s2' *)
  erewrite <- regs_valnums_sound by eauto. eauto with va.
(* Goal: match_states s1' s2' *)
  auto.
Qed.

Lemma load_memcpy:
  forall m b1 ofs1 sz bytes b2 ofs2 m' chunk i v,
  Mem.loadbytes m b1 ofs1 sz = Some bytes ->
  Mem.storebytes m b2 ofs2 bytes = Some m' ->
  Mem.load chunk m b1 i = Some v ->
  ofs1 <= i -> i + size_chunk chunk <= ofs1 + sz ->
  (align_chunk chunk | ofs2 - ofs1) ->
  Mem.load chunk m' b2 (i + (ofs2 - ofs1)) = Some v.
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  intros.
(* Goal: @eq (option val) (Mem.load chunk m' b2 (Z.add i (Z.sub ofs2 ofs1))) (@Some val v) *)
  generalize (size_chunk_pos chunk); intros SPOS.
  set (n1 := i - ofs1).
(* Goal: @eq (option val) (Mem.load chunk m' b2 (Z.add i (Z.sub ofs2 ofs1))) (@Some val v) *)
  set (n2 := size_chunk chunk).
  set (n3 := sz - (n1 + n2)).
  replace sz with (n1 + (n2 + n3)) in H by (unfold n3, n2, n1; omega).
(* Goal: match_states s1' s2' *)
  exploit Mem.loadbytes_split; eauto.
(* Goal: Z.ge n1 Z0 *)
  unfold n1; omega.
(* Goal: Z.ge n3 Z0 *)
(* Goal: forall _ : @ex (list memval) (fun bytes1 : list memval => @ex (list memval) (fun bytes2 : list memval => Logic.and (@eq (option (list memval)) (Mem.loadbytes m b1 (Z.add ofs1 n1) n2) (@Some (list memval) bytes1)) (Logic.and (@eq (option (list memval)) (Mem.loadbytes m b1 (Z.add (Z.add ofs1 n1) n2) n3) (@Some (list memval) bytes2)) (@eq (list memval) bytes23 (@app memval bytes1 bytes2))))), @eq (option val) (Mem.load chunk m' b2 (Z.add i (Z.sub ofs2 ofs1))) (@Some val v) *)
  unfold n3, n2, n1; omega.
(* Goal: forall _ : @ex (list memval) (fun bytes1 : list memval => @ex (list memval) (fun bytes2 : list memval => Logic.and (@eq (option (list memval)) (Mem.loadbytes m b1 ofs1 n1) (@Some (list memval) bytes1)) (Logic.and (@eq (option (list memval)) (Mem.loadbytes m b1 (Z.add ofs1 n1) (Z.add n2 n3)) (@Some (list memval) bytes2)) (@eq (list memval) bytes (@app memval bytes1 bytes2))))), @eq (option val) (Mem.load chunk m' b2 (Z.add i (Z.sub ofs2 ofs1))) (@Some val v) *)
  intros (bytes1 & bytes23 & LB1 & LB23 & EQ).
(* Goal: @eq (option val) (Mem.load chunk m' b2 (Z.add i (Z.sub ofs2 ofs1))) (@Some val v) *)
  clear H.
(* Goal: match_states s1' s2' *)
  exploit Mem.loadbytes_split; eauto.
(* Goal: Z.ge n2 Z0 *)
(* Goal: Logic.or (not (@eq block b2 b2)) (Logic.or (Z.le (Z.add (Z.add ofs2 n1) n2) (Z.add (Z.add ofs2 n1) n2)) (Z.le (Z.add (Z.add (Z.add ofs2 n1) n2) (Z.of_nat (@Datatypes.length memval bytes3))) (Z.add ofs2 n1))) *)
  unfold n2; omega.
(* Goal: Z.ge n3 Z0 *)
(* Goal: forall _ : @ex (list memval) (fun bytes1 : list memval => @ex (list memval) (fun bytes2 : list memval => Logic.and (@eq (option (list memval)) (Mem.loadbytes m b1 (Z.add ofs1 n1) n2) (@Some (list memval) bytes1)) (Logic.and (@eq (option (list memval)) (Mem.loadbytes m b1 (Z.add (Z.add ofs1 n1) n2) n3) (@Some (list memval) bytes2)) (@eq (list memval) bytes23 (@app memval bytes1 bytes2))))), @eq (option val) (Mem.load chunk m' b2 (Z.add i (Z.sub ofs2 ofs1))) (@Some val v) *)
  unfold n3, n2, n1; omega.
(* Goal: forall _ : @ex (list memval) (fun bytes1 : list memval => @ex (list memval) (fun bytes2 : list memval => Logic.and (@eq (option (list memval)) (Mem.loadbytes m b1 (Z.add ofs1 n1) n2) (@Some (list memval) bytes1)) (Logic.and (@eq (option (list memval)) (Mem.loadbytes m b1 (Z.add (Z.add ofs1 n1) n2) n3) (@Some (list memval) bytes2)) (@eq (list memval) bytes23 (@app memval bytes1 bytes2))))), @eq (option val) (Mem.load chunk m' b2 (Z.add i (Z.sub ofs2 ofs1))) (@Some val v) *)
  intros (bytes2 & bytes3 & LB2 & LB3 & EQ').
(* Goal: @eq (option val) (Mem.load chunk m' b2 (Z.add i (Z.sub ofs2 ofs1))) (@Some val v) *)
  subst bytes23; subst bytes.
(* Goal: match_states s1' s2' *)
  exploit Mem.load_loadbytes; eauto. intros (bytes2' & A & B).
(* Goal: @eq (option val) (Mem.load chunk m' b2 (Z.add i (Z.sub ofs2 ofs1))) (@Some val v) *)
  assert (bytes2' = bytes2).
  { replace (ofs1 + n1) with i in LB2 by (unfold n1; omega). unfold n2 in LB2. congruence.  }
(* Goal: @eq (option val) (Mem.load chunk m' b2 (Z.add i (Z.sub ofs2 ofs1))) (@Some val v) *)
  subst bytes2'.
(* Goal: match_states s1' s2' *)
  exploit Mem.storebytes_split; eauto. intros (m1 & SB1 & SB23).
(* Goal: @eq (option val) (Mem.load chunk m' b2 (Z.add i (Z.sub ofs2 ofs1))) (@Some val v) *)
  clear H0.
(* Goal: match_states s1' s2' *)
  exploit Mem.storebytes_split; eauto. intros (m2 & SB2 & SB3).
(* Goal: @eq (option val) (Mem.load chunk m' b2 (Z.add i (Z.sub ofs2 ofs1))) (@Some val v) *)
  clear SB23.
(* Goal: @eq (option val) (Mem.load chunk m' b2 (Z.add i (Z.sub ofs2 ofs1))) (@Some val v) *)
  assert (L1: Z.of_nat (length bytes1) = n1).
(* Goal: match_states s1' s2' *)
  { erewrite Mem.loadbytes_length by eauto. apply nat_of_Z_eq. unfold n1; omega. }
(* Goal: @eq (option val) (Mem.load chunk m' b2 (Z.add i (Z.sub ofs2 ofs1))) (@Some val v) *)
  assert (L2: Z.of_nat (length bytes2) = n2).
(* Goal: match_states s1' s2' *)
  { erewrite Mem.loadbytes_length by eauto. apply nat_of_Z_eq. unfold n2; omega. }
  rewrite L1 in *. rewrite L2 in *.
  assert (LB': Mem.loadbytes m2 b2 (ofs2 + n1) n2 = Some bytes2).
(* Goal: match_states s1' s2' *)
  { rewrite <- L2. eapply Mem.loadbytes_storebytes_same; eauto. }
  assert (LB'': Mem.loadbytes m' b2 (ofs2 + n1) n2 = Some bytes2).
(* Goal: match_states s1' s2' *)
  { rewrite <- LB'. eapply Mem.loadbytes_storebytes_other; eauto.
(* Goal: Z.ge n2 Z0 *)
(* Goal: Logic.or (not (@eq block b2 b2)) (Logic.or (Z.le (Z.add (Z.add ofs2 n1) n2) (Z.add (Z.add ofs2 n1) n2)) (Z.le (Z.add (Z.add (Z.add ofs2 n1) n2) (Z.of_nat (@Datatypes.length memval bytes3))) (Z.add ofs2 n1))) *)
    unfold n2; omega.
    right; left; omega. }
(* Goal: match_states s1' s2' *)
  exploit Mem.load_valid_access; eauto. intros [P Q].
(* Goal: @eq (option val) (Mem.load chunk m' b2 (Z.add i (Z.sub ofs2 ofs1))) (@Some val v) *)
  rewrite B. apply Mem.loadbytes_load.
  replace (i + (ofs2 - ofs1)) with (ofs2 + n1) by (unfold n1; omega).
(* Goal: @eq (option (list memval)) (Mem.loadbytes m' b2 (Z.add ofs2 n1) (size_chunk chunk)) (@Some (list memval) bytes2) *)
(* Goal: Z.divide (align_chunk chunk) (Z.add i (Z.sub ofs2 ofs1)) *)
  exact LB''.
(* Goal: match_states s1' s2' *)
  apply Z.divide_add_r; auto.
Qed.

Lemma shift_memcpy_eq_wf:
  forall src sz delta e e' next,
  shift_memcpy_eq src sz delta e = Some e' ->
  wf_equation next e ->
  wf_equation next e'.
Proof with (try discriminate).
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  unfold shift_memcpy_eq; intros.
(* Goal: wf_equation (num_next n) e *)
  destruct e. destruct r... destruct a...
  try (rename i into ofs).
  destruct (zle src (Ptrofs.unsigned ofs) &&
        zle (Ptrofs.unsigned ofs + size_chunk m) (src + sz) &&
        zeq (delta mod align_chunk m) 0 && zle 0 (Ptrofs.unsigned ofs + delta) &&
        zle (Ptrofs.unsigned ofs + delta) Ptrofs.max_unsigned)...
(* Goal: Logic.and (sound_state prog s1') (match_states s1' s2') *)
  inv H. destruct H0. split. auto. red; simpl; tauto.
Qed.

Lemma shift_memcpy_eq_holds:
  forall src dst sz e e' m sp bytes m' valu ge,
  shift_memcpy_eq src sz (dst - src) e = Some e' ->
  Mem.loadbytes m sp src sz = Some bytes ->
  Mem.storebytes m sp dst bytes = Some m' ->
  equation_holds valu ge (Vptr sp Ptrofs.zero) m e ->
  equation_holds valu ge (Vptr sp Ptrofs.zero) m' e'.
Proof with (try discriminate).
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  intros. set (delta := dst - src) in *. unfold shift_memcpy_eq in H.
  destruct e as [l strict rhs] eqn:E.
  destruct rhs as [op vl | chunk addr vl]...
  destruct addr...
  try (rename i into ofs).
  set (i1 := Ptrofs.unsigned ofs) in *. set (j := i1 + delta) in *.
  destruct (zle src i1)...
  destruct (zle (i1 + size_chunk chunk) (src + sz))...
  destruct (zeq (delta mod align_chunk chunk) 0)...
  destruct (zle 0 j)...
  destruct (zle j Ptrofs.max_unsigned)...
(* Goal: final_state st2 r *)
  simpl in H; inv H.
  assert (LD: forall v,
    Mem.loadv chunk m (Vptr sp ofs) = Some v ->
    Mem.loadv chunk m' (Vptr sp (Ptrofs.repr j)) = Some v).
(* Goal: forall (b : block) (o i : Ptrofs.int) (_ : pmatch bc b o (Stk i)), Logic.and (@eq block b sp) (@eq Ptrofs.int i o) *)
(* Goal: numbering_holds valu ge (Vptr sp Ptrofs.zero) rs m' (mknumbering (num_next n2) (add_memcpy_eqs (Ptrofs.unsigned ofs) sz (Z.sub (Ptrofs.unsigned ofs0) (Ptrofs.unsigned ofs)) (num_eqs n1) (num_eqs n2)) (num_reg n2) (num_val n2)) *)
  {
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
    simpl; intros. rewrite Ptrofs.unsigned_repr by omega.
(* Goal: match_states s1' s2' *)
    unfold j, delta. eapply load_memcpy; eauto.
(* Goal: match_states s1' s2' *)
    apply Zmod_divide; auto. generalize (align_chunk_pos chunk); omega.
  }
  inv H2.
(* Goal: match_states s1' s2' *)
+ inv H3. exploit eval_addressing_Ainstack_inv; eauto. intros [E1 E2].
(* Goal: iff (@In A y (@remove A eq x l)) (Logic.and (not (@Logic.eq A x y)) (Logic.or (@Logic.eq A a y) (@In A y l))) *)
(* Goal: iff (@In A y (@cons A a (@remove A eq x l))) (Logic.and (not (@Logic.eq A x y)) (Logic.or (@Logic.eq A a y) (@In A y l))) *)
  simpl in E2; rewrite Ptrofs.add_zero_l in E2. subst a.
(* Goal: final_state (Returnstate (@nil stackframe) (Vint r) m') r *)
  apply eq_holds_strict. econstructor. rewrite eval_addressing_Ainstack.
(* Goal: match_states s1' s2' *)
  simpl. rewrite Ptrofs.add_zero_l. eauto.
(* Goal: match_states s1' s2' *)
  apply LD; auto.
(* Goal: match_states s1' s2' *)
+ inv H4. exploit eval_addressing_Ainstack_inv; eauto. intros [E1 E2].
(* Goal: iff (@In A y (@remove A eq x l)) (Logic.and (not (@Logic.eq A x y)) (Logic.or (@Logic.eq A a y) (@In A y l))) *)
(* Goal: iff (@In A y (@cons A a (@remove A eq x l))) (Logic.and (not (@Logic.eq A x y)) (Logic.or (@Logic.eq A a y) (@In A y l))) *)
  simpl in E2; rewrite Ptrofs.add_zero_l in E2. subst a.
(* Goal: match_states s1' s2' *)
  apply eq_holds_lessdef with v; auto.
(* Goal: match_states s1' s2' *)
  econstructor. rewrite eval_addressing_Ainstack. simpl. rewrite Ptrofs.add_zero_l. eauto.
(* Goal: match_states s1' s2' *)
  apply LD; auto.
Qed.

Lemma add_memcpy_eqs_charact:
  forall e' src sz delta eqs2 eqs1,
  In e' (add_memcpy_eqs src sz delta eqs1 eqs2) ->
  In e' eqs2 \/ exists e, In e eqs1 /\ shift_memcpy_eq src sz delta e = Some e'.
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  induction eqs1; simpl; intros.
(* Goal: match_states s1' s2' *)
- auto.
- destruct (shift_memcpy_eq src sz delta a) as [e''|] eqn:SHIFT.
(* Goal: Smallstep.final_state (semantics tprog) s2 r *)
  + destruct H. subst e''. right; exists a; auto.
(* Goal: match_states s1' s2' *)
    destruct IHeqs1 as [A | [e [A B]]]; auto. right; exists e; auto.
(* Goal: match_states s1' s2' *)
  + destruct IHeqs1 as [A | [e [A B]]]; auto. right; exists e; auto.
Qed.

Lemma add_memcpy_holds:
  forall m bsrc osrc sz bytes bdst odst m' valu ge sp rs n1 n2 bc asrc adst,
  Mem.loadbytes m bsrc (Ptrofs.unsigned osrc) sz = Some bytes ->
  Mem.storebytes m bdst (Ptrofs.unsigned odst) bytes = Some m' ->
  numbering_holds valu ge (Vptr sp Ptrofs.zero) rs m n1 ->
  numbering_holds valu ge (Vptr sp Ptrofs.zero) rs m' n2 ->
  pmatch bc bsrc osrc asrc ->
  pmatch bc bdst odst adst ->
  bc sp = BCstack ->
  Ple (num_next n1) (num_next n2) ->
  numbering_holds valu ge (Vptr sp Ptrofs.zero) rs m' (add_memcpy n1 n2 asrc adst sz).
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  intros. unfold add_memcpy.
(* Goal: match_states s1' s2' *)
  destruct asrc; auto; destruct adst; auto.
  assert (A: forall b o i, pmatch bc b o (Stk i) -> b = sp /\ i = o).
(* Goal: forall (b : block) (o i : Ptrofs.int) (_ : pmatch bc b o (Stk i)), Logic.and (@eq block b sp) (@eq Ptrofs.int i o) *)
(* Goal: numbering_holds valu ge (Vptr sp Ptrofs.zero) rs m' (mknumbering (num_next n2) (add_memcpy_eqs (Ptrofs.unsigned ofs) sz (Z.sub (Ptrofs.unsigned ofs0) (Ptrofs.unsigned ofs)) (num_eqs n1) (num_eqs n2)) (num_reg n2) (num_val n2)) *)
  {
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
    intros. inv H7. split; auto. eapply bc_stack; eauto.
  }
(* Goal: equation_holds valu2 ge sp m eq *)
  apply A in H3; destruct H3. subst bsrc ofs.
(* Goal: numbering_holds valu ge (Vptr sp Ptrofs.zero) rs m' (mknumbering (num_next n2) (add_memcpy_eqs (Ptrofs.unsigned osrc) sz (Z.sub (Ptrofs.unsigned ofs0) (Ptrofs.unsigned osrc)) (num_eqs n1) (num_eqs n2)) (num_reg n2) (num_val n2)) *)
  apply A in H4; destruct H4. subst bdst ofs0.
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
  constructor; simpl; intros; eauto with cse.
- constructor; simpl; eauto with cse.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  intros. exploit add_memcpy_eqs_charact; eauto. intros [X | (e0 & X & Y)].
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
  eauto with cse.
(* Goal: match_states s1' s2' *)
  apply wf_equation_incr with (num_next n1); auto.
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
  eapply shift_memcpy_eq_wf; eauto with cse.
(* Goal: match_states s1' s2' *)
- exploit add_memcpy_eqs_charact; eauto. intros [X | (e0 & X & Y)].
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
  eauto with cse.
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
  eapply shift_memcpy_eq_holds; eauto with cse.
Qed.

(** Correctness of operator reduction *)

Section REDUCE.

Variable A: Type.
Variable f: (valnum -> option rhs) -> A -> list valnum -> option (A * list valnum).
Variable V: Type.
Variable ge: genv.
Variable sp: val.
Variable rs: regset.
Variable m: mem.
Variable sem: A -> list val -> option V.
Hypothesis f_sound:
  forall eqs valu op args op' args',
  (forall v rhs, eqs v = Some rhs -> rhs_eval_to valu ge sp m rhs (valu v)) ->
  f eqs op args = Some(op', args') ->
  sem op' (map valu args') = sem op (map valu args).
Variable n: numbering.
Variable valu: valnum -> val.
Hypothesis n_holds: numbering_holds valu ge sp rs m n.

Lemma reduce_rec_sound:
  forall niter op args op' rl' res,
  reduce_rec A f n niter op args = Some(op', rl') ->
  sem op (map valu args) = Some res ->
  sem op' (rs##rl') = Some res.
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  induction niter; simpl; intros.
(* Goal: @ex program (fun cu : program => @ex fundef (fun tfd : fundef => Logic.and (@eq (option fundef) (@None fundef) (@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)))) *)
  discriminate.
  destruct (f (fun v : valnum => find_valnum_num v (num_eqs n)) op args)
           as [[op1 args1] | ] eqn:?.
  assert (sem op1 (map valu args1) = Some res).
(* Goal: match_states s1' s2' *)
    rewrite <- H0. eapply f_sound; eauto.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
    simpl; intros.
(* Goal: match_states s1' s2' *)
    exploit num_holds_eq; eauto.
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
(* Goal: equation_holds valu ge (Vptr sp Ptrofs.zero) m' eq *)
    eapply find_valnum_num_charact; eauto with cse.
(* Goal: match_states s1' s2' *)
    intros EH; inv EH; auto.
  destruct (reduce_rec A f n niter op1 args1) as [[op2 rl2] | ] eqn:?.
(* Goal: match_states s1' s2' *)
  inv H. eapply IHniter; eauto.
  destruct (regs_valnums n args1) as [rl|] eqn:?.
(* Goal: match_states s1' s2' *)
  inv H. erewrite regs_valnums_sound; eauto.
(* Goal: @ex program (fun cu : program => @ex fundef (fun tfd : fundef => Logic.and (@eq (option fundef) (@None fundef) (@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)))) *)
  discriminate.
(* Goal: @ex program (fun cu : program => @ex fundef (fun tfd : fundef => Logic.and (@eq (option fundef) (@None fundef) (@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)))) *)
  discriminate.
Qed.

Lemma reduce_sound:
  forall op rl vl op' rl' res,
  reduce A f n op rl vl = (op', rl') ->
  map valu vl = rs##rl ->
  sem op rs##rl = Some res ->
  sem op' rs##rl' = Some res.
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  unfold reduce; intros.
(* Goal: final_state st2 r *)
  destruct (reduce_rec A f n 4%nat op vl) as [[op1 rl1] | ] eqn:?; inv H.
(* Goal: match_states s1' s2' *)
  eapply reduce_rec_sound; eauto. congruence.
(* Goal: match_states s1' s2' *)
  auto.
Qed.

End REDUCE.

(** The numberings associated to each instruction by the static analysis
  are inductively satisfiable, in the following sense: the numbering
  at the function entry point is satisfiable, and for any RTL execution
  from [pc] to [pc'], satisfiability at [pc] implies
  satisfiability at [pc']. *)

Theorem analysis_correct_1:
  forall ge sp rs m f vapprox approx pc pc' i,
  analyze f vapprox = Some approx ->
  f.(fn_code)!pc = Some i -> In pc' (successors_instr i) ->
  (exists valu, numbering_holds valu ge sp rs m (transfer f vapprox pc approx!!pc)) ->
  (exists valu, numbering_holds valu ge sp rs m approx!!pc').
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  intros.
(* Goal: @ex valuation (fun valu : valuation => numbering_holds valu ge sp rs m (@PMap.get numbering pc' approx)) *)
  assert (Numbering.ge approx!!pc' (transfer f vapprox pc approx!!pc)).
(* Goal: match_states s1' s2' *)
    eapply Solver.fixpoint_solution; eauto.
(* Goal: match_states s1' s2' *)
  destruct H2 as [valu NH]. exists valu; apply H3. auto.
Qed.

Theorem analysis_correct_entry:
  forall ge sp rs m f vapprox approx,
  analyze f vapprox = Some approx ->
  exists valu, numbering_holds valu ge sp rs m approx!!(f.(fn_entrypoint)).
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  intros.
(* Goal: @ex valuation (fun valu : valuation => numbering_holds valu ge sp rs m (@PMap.get numbering (fn_entrypoint f) approx)) *)
  replace (approx!!(f.(fn_entrypoint))) with Solver.L.top.
(* Goal: @ex valuation (fun valu : valuation => numbering_holds valu ge sp rs m Solver.L.top) *)
(* Goal: @eq Solver.L.t Solver.L.top (@PMap.get numbering (fn_entrypoint f) approx) *)
  exists (fun v => Vundef). apply empty_numbering_holds.
(* Goal: @eq Solver.L.t Solver.L.top (@PMap.get numbering (fn_entrypoint f) approx) *)
  symmetry. eapply Solver.fixpoint_entry; eauto.
Qed.

(** * Semantic preservation *)

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 funct_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_preserved:
  forall rm f tf, transf_fundef rm f = OK tf -> funsig tf = funsig f.
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  unfold transf_fundef; intros. destruct f; monadInv H; auto.
(* Goal: @eq signature (funsig (@Internal function x)) (funsig (@Internal function f)) *)
  unfold transf_function in EQ.
(* Goal: match_states s1' s2' *)
  destruct (analyze f (vanalyze rm f)); try discriminate. inv EQ; auto.
Qed.

Definition transf_function' (f: function) (approxs: PMap.t numbering) : function :=
  mkfunction
    f.(fn_sig)
    f.(fn_params)
    f.(fn_stacksize)
    (transf_code approxs f.(fn_code))
    f.(fn_entrypoint).

Definition regs_lessdef (rs1 rs2: regset) : Prop :=
  forall r, Val.lessdef (rs1#r) (rs2#r).

Lemma regs_lessdef_regs:
  forall rs1 rs2, regs_lessdef rs1 rs2 ->
  forall rl, Val.lessdef_list rs1##rl rs2##rl.
Proof.
(* Goal: match_states s1' s2' *)
  induction rl; constructor; auto.
Qed.

Lemma set_reg_lessdef:
  forall r v1 v2 rs1 rs2,
  Val.lessdef v1 v2 -> regs_lessdef rs1 rs2 -> regs_lessdef (rs1#r <- v1) (rs2#r <- v2).
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  intros; red; intros. repeat rewrite Regmap.gsspec.
(* Goal: match_states s1' s2' *)
  destruct (peq r0 r); auto.
Qed.

Lemma init_regs_lessdef:
  forall rl vl1 vl2,
  Val.lessdef_list vl1 vl2 ->
  regs_lessdef (init_regs vl1 rl) (init_regs vl2 rl).
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  induction rl; simpl; intros.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  red; intros. rewrite Regmap.gi. auto.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  inv H. red; intros. rewrite Regmap.gi. auto.
(* Goal: match_states s1' s2' *)
  apply set_reg_lessdef; auto.
Qed.

Lemma find_function_translated:
  forall ros rs fd rs',
  find_function ge ros rs = Some fd ->
  regs_lessdef rs rs' ->
  exists cu tfd, find_function tge ros rs' = Some tfd
              /\ transf_fundef (romem_for cu) fd = OK tfd
              /\ linkorder cu prog.
Proof.
(* Goal: forall (ros : sum reg ident) (rs : regset) (fd : fundef) (rs' : regset) (_ : @eq (option fundef) (find_function ge ros rs) (@Some fundef fd)) (_ : regs_lessdef rs rs'), @ex program (fun cu : program => @ex fundef (fun tfd : fundef => Logic.and (@eq (option fundef) (find_function tge ros rs') (@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)))) *)
  unfold find_function; intros; destruct ros.
- specialize (H0 r). inv H0.
(* Goal: match_states s1' s2' *)
  apply functions_translated; auto.
  rewrite <- H2 in H; discriminate.
- rewrite symbols_preserved. destruct (Genv.find_symbol ge i).
(* Goal: match_states s1' s2' *)
  apply funct_ptr_translated; auto.
(* Goal: @ex program (fun cu : program => @ex fundef (fun tfd : fundef => Logic.and (@eq (option fundef) (@None fundef) (@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)))) *)
  discriminate.
Qed.

(** The proof of semantic preservation is a simulation argument using
  diagrams of the following form:
<<
           st1 --------------- st2
            |                   |
           t|                   |t
            |                   |
            v                   v
           st1'--------------- st2'
>>
  Left: RTL execution in the original program.  Right: RTL execution in
  the optimized program.  Precondition (top) and postcondition (bottom):
  agreement between the states, including the fact that
  the numbering at [pc] (returned by the static analysis) is satisfiable.
*)

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

Inductive match_stackframes: list stackframe -> list stackframe -> Prop :=
  | match_stackframes_nil:
      match_stackframes nil nil
  | match_stackframes_cons:
      forall res sp pc rs f s rs' s' cu approx
           (LINK: linkorder cu prog)
           (ANALYZE: analyze cu f = Some approx)
           (SAT: forall v m, exists valu, numbering_holds valu ge sp (rs#res <- v) m approx!!pc)
           (RLD: regs_lessdef rs rs')
           (STACKS: match_stackframes s s'),
    match_stackframes
      (Stackframe res f sp pc rs :: s)
      (Stackframe res (transf_function' f approx) sp pc rs' :: s').

Inductive match_states: state -> state -> Prop :=
  | match_states_intro:
      forall s sp pc rs m s' rs' m' f cu approx
             (LINK: linkorder cu prog)
             (ANALYZE: analyze cu f = Some approx)
             (SAT: exists valu, numbering_holds valu ge sp rs m approx!!pc)
             (RLD: regs_lessdef rs rs')
             (MEXT: Mem.extends m m')
             (STACKS: match_stackframes s s'),
      match_states (State s f sp pc rs m)
                   (State s' (transf_function' f approx) sp pc rs' m')
  | match_states_call:
      forall s f tf args m s' args' m' cu
             (LINK: linkorder cu prog)
             (STACKS: match_stackframes s s')
             (TFD: transf_fundef (romem_for cu) f = OK tf)
             (ARGS: Val.lessdef_list args args')
             (MEXT: Mem.extends m m'),
      match_states (Callstate s f args m)
                   (Callstate s' tf args' m')
  | match_states_return:
      forall s s' v v' m m'
             (STACK: match_stackframes s s')
             (RES: Val.lessdef v v')
             (MEXT: Mem.extends m m'),
      match_states (Returnstate s v m)
                   (Returnstate s' v' m').

Ltac TransfInstr :=
  match goal with
  | H1: (PTree.get ?pc ?c = Some ?instr), f: function, approx: PMap.t numbering |- _ =>
      cut ((transf_function' f approx).(fn_code)!pc = Some(transf_instr approx!!pc instr));
      [ simpl transf_instr
      | unfold transf_function', transf_code; simpl; rewrite PTree.gmap;
        unfold option_map; rewrite H1; reflexivity ]
  end.

(** The proof of simulation is a case analysis over the transition
  in the source code. *)

Lemma transf_step_correct:
  forall s1 t s2, step ge s1 t s2 ->
  forall s1' (MS: match_states s1 s1') (SOUND: sound_state prog s1),
  exists s2', step tge s1' t s2' /\ match_states s2 s2'.
Proof.
  induction 1; intros; inv MS; try (TransfInstr; intro C).

  (* Inop *)
(* Goal: Logic.and (sound_state prog s1') (match_states s1' s2') *)
- econstructor; split.
(* Goal: match_states s1' s2' *)
  eapply exec_Inop; eauto.
(* Goal: match_states s1' s2' *)
  econstructor; eauto.
(* Goal: match_states s1' s2' *)
  eapply analysis_correct_1; eauto. simpl; auto.
(* Goal: match_states s1' s2' *)
  unfold transfer; rewrite H; auto.

  (* Iop *)
- destruct (is_trivial_op op) eqn:TRIV.
+ (* unchanged *)
(* Goal: match_states s1' s2' *)
  exploit eval_operation_lessdef. eapply regs_lessdef_regs; eauto. eauto. eauto.
  intros [v' [A B]].
(* Goal: Logic.and (sound_state prog s1') (match_states s1' s2') *)
  econstructor; split.
(* Goal: match_states s1' s2' *)
  eapply exec_Iop with (v := v'); eauto.
  rewrite <- A. apply eval_operation_preserved. exact symbols_preserved.
(* Goal: match_states s1' s2' *)
  econstructor; eauto.
(* Goal: match_states s1' s2' *)
  eapply analysis_correct_1; eauto. simpl; auto.
  unfold transfer; rewrite H.
(* Goal: match_states s1' s2' *)
  destruct SAT as [valu NH]. eapply add_op_holds; eauto.
(* Goal: match_states s1' s2' *)
  apply set_reg_lessdef; auto.
+ (* possibly optimized *)
  destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
  destruct SAT as [valu1 NH1].
(* Goal: match_states s1' s2' *)
  exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q).
  destruct (find_rhs n1 (Op op vl)) as [r|] eqn:?.
* (* replaced by move *)
(* Goal: match_states s1' s2' *)
  exploit find_rhs_sound; eauto. intros (v' & EV & LD).
  assert (v' = v) by (inv EV; congruence). subst v'.
(* Goal: Logic.and (sound_state prog s1') (match_states s1' s2') *)
  econstructor; split.
(* Goal: match_states s1' s2' *)
  eapply exec_Iop; eauto. simpl; eauto.
(* Goal: match_states s1' s2' *)
  econstructor; eauto.
(* Goal: match_states s1' s2' *)
  eapply analysis_correct_1; eauto. simpl; auto.
  unfold transfer; rewrite H.
(* Goal: match_states s1' s2' *)
  eapply add_op_holds; eauto.
(* Goal: match_states s1' s2' *)
  apply set_reg_lessdef; auto.
(* Goal: match_states s1' s2' *)
  eapply Val.lessdef_trans; eauto.
* (* possibly simplified *)
  destruct (reduce operation combine_op n1 op args vl) as [op' args'] eqn:?.
  assert (RES: eval_operation ge sp op' rs##args' m = Some v).
(* Goal: match_states s1' s2' *)
    eapply reduce_sound with (sem := fun op vl => eval_operation ge sp op vl m); eauto.
(* Goal: match_states s1' s2' *)
    intros; eapply combine_op_sound; eauto.
(* Goal: match_states s1' s2' *)
  exploit eval_operation_lessdef. eapply regs_lessdef_regs; eauto. eauto. eauto.
  intros [v' [A B]].
(* Goal: Logic.and (sound_state prog s1') (match_states s1' s2') *)
  econstructor; split.
(* Goal: match_states s1' s2' *)
  eapply exec_Iop with (v := v'); eauto.
  rewrite <- A. apply eval_operation_preserved. exact symbols_preserved.
(* Goal: match_states s1' s2' *)
  econstructor; eauto.
(* Goal: match_states s1' s2' *)
  eapply analysis_correct_1; eauto. simpl; auto.
  unfold transfer; rewrite H.
(* Goal: match_states s1' s2' *)
  eapply add_op_holds; eauto.
(* Goal: match_states s1' s2' *)
  apply set_reg_lessdef; auto.

- (* Iload *)
  destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
  destruct SAT as [valu1 NH1].
(* Goal: match_states s1' s2' *)
  exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q).
  destruct (find_rhs n1 (Load chunk addr vl)) as [r|] eqn:?.
+ (* replaced by move *)
(* Goal: match_states s1' s2' *)
  exploit find_rhs_sound; eauto. intros (v' & EV & LD).
  assert (v' = v) by (inv EV; congruence). subst v'.
(* Goal: Logic.and (sound_state prog s1') (match_states s1' s2') *)
  econstructor; split.
(* Goal: match_states s1' s2' *)
  eapply exec_Iop; eauto. simpl; eauto.
(* Goal: match_states s1' s2' *)
  econstructor; eauto.
(* Goal: match_states s1' s2' *)
  eapply analysis_correct_1; eauto. simpl; auto.
  unfold transfer; rewrite H.
(* Goal: match_states s1' s2' *)
  eapply add_load_holds; eauto.
(* Goal: match_states s1' s2' *)
  apply set_reg_lessdef; auto. eapply Val.lessdef_trans; eauto.
+ (* load is preserved, but addressing is possibly simplified *)
  destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args'] eqn:?.
  assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a).
(* Goal: match_states s1' s2' *)
  { eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto.
(* Goal: match_states s1' s2' *)
    intros; eapply combine_addr_sound; eauto. }
(* Goal: match_states s1' s2' *)
  exploit eval_addressing_lessdef. apply regs_lessdef_regs; eauto. eexact ADDR.
  intros [a' [A B]].
  assert (ADDR': eval_addressing tge sp addr' rs'##args' = Some a').
  { rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. }
(* Goal: match_states s1' s2' *)
  exploit Mem.loadv_extends; eauto.
  intros [v' [X Y]].
(* Goal: Logic.and (sound_state prog s1') (match_states s1' s2') *)
  econstructor; split.
(* Goal: match_states s1' s2' *)
  eapply exec_Iload; eauto.
(* Goal: match_states s1' s2' *)
  econstructor; eauto.
(* Goal: match_states s1' s2' *)
  eapply analysis_correct_1; eauto. simpl; auto.
  unfold transfer; rewrite H.
(* Goal: match_states s1' s2' *)
  eapply add_load_holds; eauto.
(* Goal: match_states s1' s2' *)
  apply set_reg_lessdef; auto.

- (* Istore *)
  destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
  destruct SAT as [valu1 NH1].
(* Goal: match_states s1' s2' *)
  exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q).
  destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args'] eqn:?.
  assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a).
(* Goal: match_states s1' s2' *)
  { eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto.
(* Goal: match_states s1' s2' *)
    intros; eapply combine_addr_sound; eauto. }
(* Goal: match_states s1' s2' *)
  exploit eval_addressing_lessdef. apply regs_lessdef_regs; eauto. eexact ADDR.
  intros [a' [A B]].
  assert (ADDR': eval_addressing tge sp addr' rs'##args' = Some a').
  { rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. }
(* Goal: match_states s1' s2' *)
  exploit Mem.storev_extends; eauto. intros [m'' [X Y]].
(* Goal: Logic.and (sound_state prog s1') (match_states s1' s2') *)
  econstructor; split.
(* Goal: match_states s1' s2' *)
  eapply exec_Istore; eauto.
(* Goal: match_states s1' s2' *)
  econstructor; eauto.
(* Goal: match_states s1' s2' *)
  eapply analysis_correct_1; eauto. simpl; auto.
  unfold transfer; rewrite H.
  InvSoundState.
(* Goal: match_states s1' s2' *)
  eapply add_store_result_hold; eauto.
(* Goal: match_states s1' s2' *)
  eapply kill_loads_after_store_holds; eauto.

- (* Icall *)
(* Goal: match_states s1' s2' *)
  exploit find_function_translated; eauto. intros (cu' & tf & FIND' & TRANSF' & LINK').
(* Goal: Logic.and (sound_state prog s1') (match_states s1' s2') *)
  econstructor; split.
(* Goal: match_states s1' s2' *)
  eapply exec_Icall; eauto.
(* Goal: match_states s1' s2' *)
  eapply sig_preserved; eauto.
(* Goal: match_states s1' s2' *)
  econstructor; eauto.
(* Goal: match_states s1' s2' *)
  eapply match_stackframes_cons with (cu := cu); eauto.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  intros. eapply analysis_correct_1; eauto. simpl; auto.
  unfold transfer; rewrite H.
(* Goal: numbering_holds (fun _ : CSEdomain.valnum => Vundef) ge sp rs m Solver.L.top *)
(* Goal: @eq Solver.L.t Solver.L.top (@PMap.get numbering (fn_entrypoint f) approx) *)
  exists (fun _ => Vundef); apply empty_numbering_holds.
(* Goal: match_states s1' s2' *)
  apply regs_lessdef_regs; auto.

- (* Itailcall *)
(* Goal: match_states s1' s2' *)
  exploit find_function_translated; eauto. intros (cu' & tf & FIND' & TRANSF' & LINK').
(* Goal: match_states s1' s2' *)
  exploit Mem.free_parallel_extends; eauto. intros [m'' [A B]].
(* Goal: Logic.and (sound_state prog s1') (match_states s1' s2') *)
  econstructor; split.
(* Goal: match_states s1' s2' *)
  eapply exec_Itailcall; eauto.
(* Goal: match_states s1' s2' *)
  eapply sig_preserved; eauto.
(* Goal: match_states s1' s2' *)
  econstructor; eauto.
(* Goal: match_states s1' s2' *)
  apply regs_lessdef_regs; auto.

- (* Ibuiltin *)
(* Goal: match_states s1' s2' *)
  exploit (@eval_builtin_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)); eauto.
  intros (vargs' & A & B).
(* Goal: match_states s1' s2' *)
  exploit external_call_mem_extends; eauto.
  intros (v' & m1' & P & Q & R & S).
(* Goal: Logic.and (sound_state prog s1') (match_states s1' s2') *)
  econstructor; split.
(* Goal: match_states s1' s2' *)
  eapply exec_Ibuiltin; eauto.
(* Goal: match_states s1' s2' *)
  eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
(* Goal: match_states s1' s2' *)
  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
(* Goal: match_states s1' s2' *)
  econstructor; eauto.
(* Goal: match_states s1' s2' *)
  eapply analysis_correct_1; eauto. simpl; auto.
* unfold transfer; rewrite H.
  destruct SAT as [valu NH].
  assert (CASE1: exists valu, numbering_holds valu ge sp (regmap_setres res vres rs) m' empty_numbering).
(* Goal: forall (b : block) (o i : Ptrofs.int) (_ : pmatch bc b o (Stk i)), Logic.and (@eq block b sp) (@eq Ptrofs.int i o) *)
(* Goal: numbering_holds valu ge (Vptr sp Ptrofs.zero) rs m' (mknumbering (num_next n2) (add_memcpy_eqs (Ptrofs.unsigned ofs) sz (Z.sub (Ptrofs.unsigned ofs0) (Ptrofs.unsigned ofs)) (num_eqs n1) (num_eqs n2)) (num_reg n2) (num_val n2)) *)
  { exists valu; apply empty_numbering_holds. }
  assert (CASE2: m' = m -> exists valu, numbering_holds valu ge sp (regmap_setres res vres rs) m' (set_res_unknown approx#pc res)).
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  { intros. subst m'. exists valu. apply set_res_unknown_holds; auto. }
  assert (CASE3: exists valu, numbering_holds valu ge sp (regmap_setres res vres rs) m'
                         (set_res_unknown (kill_all_loads approx#pc) res)).
(* Goal: match_states s1' s2' *)
  { exists valu. apply set_res_unknown_holds. eapply kill_all_loads_hold; eauto. }
  destruct ef.
  + apply CASE1.
  + apply CASE3.
  + apply CASE1.
(* Goal: match_states s1' s2' *)
  + apply CASE2; inv H1; auto.
  + apply CASE3.
  + apply CASE1.
  + apply CASE1.
(* Goal: match_states s1' s2' *)
  + inv H0; auto. inv H3; auto. inv H4; auto.
(* Goal: rhs_eval_to valu ge sp m' r v *)
    simpl in H1. inv H1.
    exists valu.
    apply set_res_unknown_holds.
    InvSoundState. unfold vanalyze; rewrite AN.
    assert (pmatch bc bsrc osrc (aaddr_arg (VA.State ae am) a0))
    by (eapply aaddr_arg_sound_1; eauto).
    assert (pmatch bc bdst odst (aaddr_arg (VA.State ae am) a1))
    by (eapply aaddr_arg_sound_1; eauto).
(* Goal: match_states s1' s2' *)
    eapply add_memcpy_holds; eauto.
(* Goal: match_states s1' s2' *)
    eapply kill_loads_after_storebytes_holds; eauto.
(* Goal: match_states s1' s2' *)
    eapply Mem.loadbytes_length; eauto.
(* Goal: Ple (num_next n') (num_next n') *)
    simpl. apply Ple_refl.
(* Goal: match_states s1' s2' *)
  + apply CASE2; inv H1; auto.
(* Goal: match_states s1' s2' *)
  + apply CASE2; inv H1; auto.
  + apply CASE1.
(* Goal: match_states s1' s2' *)
  + apply CASE2; inv H1; auto.
(* Goal: match_states s1' s2' *)
* apply set_res_lessdef; auto.

- (* Icond *)
  destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
  elim SAT; intros valu1 NH1.
(* Goal: match_states s1' s2' *)
  exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q).
  destruct (reduce condition combine_cond n1 cond args vl) as [cond' args'] eqn:?.
  assert (RES: eval_condition cond' rs##args' m = Some b).
(* Goal: match_states s1' s2' *)
  { eapply reduce_sound with (sem := fun cond vl => eval_condition cond vl m); eauto.
(* Goal: match_states s1' s2' *)
    intros; eapply combine_cond_sound; eauto. }
(* Goal: Logic.and (sound_state prog s1') (match_states s1' s2') *)
  econstructor; split.
(* Goal: match_states s1' s2' *)
  eapply exec_Icond; eauto.
(* Goal: match_states s1' s2' *)
  eapply eval_condition_lessdef; eauto. apply regs_lessdef_regs; auto.
(* Goal: match_states s1' s2' *)
  econstructor; eauto.
  destruct b; eapply analysis_correct_1; eauto; simpl; auto;
(* Goal: match_states s1' s2' *)
  unfold transfer; rewrite H; auto.

- (* Ijumptable *)
  generalize (RLD arg); rewrite H0; intro LD; inv LD.
(* Goal: Logic.and (sound_state prog s1') (match_states s1' s2') *)
  econstructor; split.
(* Goal: match_states s1' s2' *)
  eapply exec_Ijumptable; eauto.
(* Goal: match_states s1' s2' *)
  econstructor; eauto.
(* Goal: match_states s1' s2' *)
  eapply analysis_correct_1; eauto. simpl. eapply list_nth_z_in; eauto.
(* Goal: match_states s1' s2' *)
  unfold transfer; rewrite H; auto.

- (* Ireturn *)
(* Goal: match_states s1' s2' *)
  exploit Mem.free_parallel_extends; eauto. intros [m'' [A B]].
(* Goal: Logic.and (sound_state prog s1') (match_states s1' s2') *)
  econstructor; split.
(* Goal: match_states s1' s2' *)
  eapply exec_Ireturn; eauto.
(* Goal: match_states s1' s2' *)
  econstructor; eauto.
(* Goal: match_states s1' s2' *)
  destruct or; simpl; auto.

- (* internal function *)
(* Goal: @eq signature (funsig (@Internal function x)) (funsig (@Internal function f)) *)
  monadInv TFD. unfold transf_function in EQ. fold (analyze cu f) in EQ.
  destruct (analyze cu f) as [approx|] eqn:?; inv EQ.
(* Goal: match_states s1' s2' *)
  exploit Mem.alloc_extends; eauto. apply Z.le_refl. apply Z.le_refl.
  intros (m'' & A & B).
(* Goal: Logic.and (sound_state prog s1') (match_states s1' s2') *)
  econstructor; split.
(* Goal: match_states s1' s2' *)
  eapply exec_function_internal; simpl; eauto.
(* Goal: match_states s1' s2' *)
  simpl. econstructor; eauto.
(* Goal: match_states s1' s2' *)
  eapply analysis_correct_entry; eauto.
(* Goal: match_states s1' s2' *)
  apply init_regs_lessdef; auto.

- (* external function *)
  monadInv TFD.
(* Goal: match_states s1' s2' *)
  exploit external_call_mem_extends; eauto.
  intros (v' & m1' & P & Q & R & S).
(* Goal: Logic.and (sound_state prog s1') (match_states s1' s2') *)
  econstructor; split.
(* Goal: match_states s1' s2' *)
  eapply exec_function_external; eauto.
(* Goal: match_states s1' s2' *)
  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
(* Goal: match_states s1' s2' *)
  econstructor; eauto.

- (* return *)
(* Goal: final_state (Returnstate s' (Vint r) m') r *)
  inv STACK.
(* Goal: Logic.and (sound_state prog s1') (match_states s1' s2') *)
  econstructor; split.
(* Goal: match_states s1' s2' *)
  eapply exec_return; eauto.
(* Goal: match_states s1' s2' *)
  econstructor; eauto.
(* Goal: match_states s1' s2' *)
  apply set_reg_lessdef; auto.
Qed.

Lemma transf_initial_states:
  forall st1, initial_state prog st1 ->
  exists st2, initial_state tprog st2 /\ match_states st1 st2.
Proof.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  intros. inversion H.
(* Goal: match_states s1' s2' *)
  exploit funct_ptr_translated; eauto. intros (cu & tf & A & B & C).
(* Goal: Logic.and (sound_state prog s1') (match_states s1' s2') *)
  exists (Callstate nil tf nil m0); split.
(* Goal: match_states s1' s2' *)
  econstructor; eauto.
(* Goal: match_states s1' s2' *)
  eapply (Genv.init_mem_match TRANSF); eauto.
  replace (prog_main tprog) with (prog_main prog).
(* Goal: match_states s1' s2' *)
  rewrite symbols_preserved. eauto.
(* Goal: @eq Solver.L.t Solver.L.top (@PMap.get numbering (fn_entrypoint f) approx) *)
  symmetry. eapply match_program_main; eauto.
(* Goal: match_states s1' s2' *)
  rewrite <- H3. eapply sig_preserved; eauto.
(* Goal: match_states s1' s2' *)
  econstructor. eauto. constructor. auto. auto. 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: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
  intros. inv H0. inv H. inv RES. inv STACK. constructor.
Qed.

Theorem transf_program_correct:
  forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
Proof.
  eapply forward_simulation_step with
    (match_states := fun s1 s2 => sound_state prog s1 /\ match_states s1 s2).
- apply senv_preserved.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
- intros. exploit transf_initial_states; eauto. intros [s2 [A B]].
(* Goal: Logic.and (sound_state prog s1') (match_states s1' s2') *)
  exists s2. split. auto. split. apply sound_initial; auto. auto.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
- intros. destruct H. eapply transf_final_states; eauto.
(* Goal: forall (s1 : Smallstep.state (semantics prog)) (t : trace) (s1' : Smallstep.state (semantics prog)) (_ : Smallstep.step (semantics prog) (globalenv (semantics prog)) s1 t s1') (s2 : Smallstep.state (semantics tprog)) (_ : Logic.and (sound_state prog s1) (match_states s1 s2)), @ex (Smallstep.state (semantics tprog)) (fun s2' : Smallstep.state (semantics tprog) => Logic.and (Smallstep.step (semantics tprog) (globalenv (semantics tprog)) s2 t s2') (Logic.and (sound_state prog s1') (match_states s1' s2'))) *)
- intros. destruct H0. exploit transf_step_correct; eauto.
(* Goal: Logic.and (sound_state prog s1') (match_states s1' s2') *)
  intros [s2' [A B]]. exists s2'; split. auto. split. eapply sound_step; eauto. auto.
Qed.

End PRESERVATION.
