(** Correctness proof for RTL generation: main proof. *)

Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Mem.
Require Import Events.
Require Import Globalenvs.
Require Import Op.
Require Import Registers.
Require Import Cminor.
Require Import RTL.
Require Import RTLgen.
Require Import RTLgenproof1.

Section CORRECTNESS.

Variable prog: Cminor.program.
Variable tprog: RTL.program.
Hypothesis TRANSL: transl_program prog = Some tprog.

Let ge : Cminor.genv := Genv.globalenv prog.
Let tge : RTL.genv := Genv.globalenv tprog.

(** Relationship between the global environments for the original
  Cminor program and the generated RTL program. *)

Lemma symbols_preserved:
  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof.
  intro. unfold ge, tge. 
  apply Genv.find_symbol_transf_partial with transl_fundef.
  exact TRANSL.
Qed.

Lemma function_ptr_translated:
  forall (b: block) (f: Cminor.fundef),
  Genv.find_funct_ptr ge b = Some f ->
  exists tf,
  Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Some tf.
Proof.
  intros. 
  generalize 
   (Genv.find_funct_ptr_transf_partial transl_fundef TRANSL H).
  case (transl_fundef f).
  intros tf [A B]. exists tf. tauto.
  intros [A B]. elim B. reflexivity.
Qed.

Lemma functions_translated:
  forall (v: val) (f: Cminor.fundef),
  Genv.find_funct ge v = Some f ->
  exists tf,
  Genv.find_funct tge v = Some tf /\ transl_fundef f = Some tf.
Proof.
  intros. 
  generalize 
   (Genv.find_funct_transf_partial transl_fundef TRANSL H).
  case (transl_fundef f).
  intros tf [A B]. exists tf. tauto.
  intros [A B]. elim B. reflexivity.
Qed.

Lemma sig_transl_function:
  forall (f: Cminor.fundef) (tf: RTL.fundef),
  transl_fundef f = Some tf ->
  RTL.funsig tf = Cminor.funsig f.
Proof.
  intros until tf. unfold transl_fundef, transf_partial_fundef.
  case f; intro.
  unfold transl_function. 
  case (transl_fun f0 init_state); intros.
  discriminate.
  destruct p. inversion H. reflexivity.
  intro. inversion H. reflexivity.
Qed.

(** Correctness of the code generated by [add_move]. *)

Lemma add_move_correct:
  forall r1 r2 sp nd s ns s' rs m,
  add_move r1 r2 nd s = OK ns s' ->
  exists rs',
  exec_instrs tge s'.(st_code) sp ns rs m E0 nd rs' m /\
  rs'#r2 = rs#r1 /\
  (forall r, r <> r2 -> rs'#r = rs#r).
Proof.
  intros until m. 
  unfold add_move. case (Reg.eq r1 r2); intro.
  monadSimpl. subst s'; subst r2; subst ns. 
  exists rs. split. apply exec_refl. split. auto. auto.
  intro. exists (rs#r2 <- (rs#r1)).
  split. apply exec_one. eapply exec_Iop. eauto with rtlg. 
  reflexivity. 
  split. apply Regmap.gss. 
  intros. apply Regmap.gso; auto.
Qed.

(** The proof of semantic preservation for the translation of expressions
  is a simulation argument based on diagrams of the following form:
<<
                    I /\ P
       e, m, a ------------- ns, rs, m
         ||                      |
         ||                      |*
         ||                      |
         \/                      v
       e', m', v ----------- nd, rs', m'
                    I /\ Q
>>
  where [transl_expr map mut a rd nd s = OK ns s'].
  The left vertical arrow represents an evaluation of the expression [a]
  (assumption).  The right vertical arrow represents the execution of
  zero, one or several instructions in the generated RTL flow graph
  found in the final state [s'] (conclusion).  

  The invariant [I] is the agreement between Cminor environments and
  RTL register environment, as captured by [match_envs].

  The preconditions [P] include the well-formedness of the compilation
  environment [mut] and the validity of [rd] as a target register.

  The postconditions [Q] state that in the final register environment
  [rs'], register [rd] contains value [v], and most other registers
  valid in [s] are unchanged w.r.t. the initial register environment
  [rs]. (See below for a precise specification of ``most other
  registers''.)

  We formalize this simulation property by the following predicate
  parameterized by the Cminor evaluation (left arrow).  *)

Definition transl_expr_correct 
  (sp: val) (le: letenv) (e: env) (m: mem) (a: expr)
              (t: trace) (m': mem) (v: val) : Prop :=
  forall map rd nd s ns s' rs
    (MWF: map_wf map s)
    (TE: transl_expr map a rd nd s = OK ns s')
    (ME: match_env map e le rs)
    (TRG: target_reg_ok s map a rd),
  exists rs',
     exec_instrs tge s'.(st_code) sp ns rs m t nd rs' m'
  /\ match_env map e le rs'
  /\ rs'#rd = v
  /\ (forall r,
       reg_valid r s -> reg_in_map map r \/ r <> rd -> rs'#r = rs#r).

(** The simulation properties for lists of expressions and for
  conditional expressions are similar. *)

Definition transl_exprlist_correct 
  (sp: val) (le: letenv) (e: env) (m: mem) (al: exprlist)
              (t: trace) (m': mem) (vl: list val) : Prop :=
  forall map rl nd s ns s' rs
    (MWF: map_wf map s)
    (TE: transl_exprlist map al rl nd s = OK ns s')
    (ME: match_env map e le rs)
    (TRG: target_regs_ok s map al rl),
  exists rs',
     exec_instrs tge s'.(st_code) sp ns rs m t nd rs' m'
  /\ match_env map e le rs'
  /\ rs'##rl = vl
  /\ (forall r,
       reg_valid r s -> reg_in_map map r \/ ~(In r rl) -> rs'#r = rs#r).

Definition transl_condition_correct 
  (sp: val) (le: letenv) (e: env) (m: mem) (a: condexpr)
              (t: trace) (m': mem) (vb: bool) : Prop :=
  forall map ntrue nfalse s ns s' rs
    (MWF: map_wf map s)
    (TE: transl_condition map a ntrue nfalse s = OK ns s')
    (ME: match_env map e le rs),
  exists rs',
     exec_instrs tge s'.(st_code) sp ns rs m t (if vb then ntrue else nfalse) rs' m'
  /\ match_env map e le rs'
  /\ (forall r, reg_valid r s -> rs'#r = rs#r).

(** For statements, we define the following auxiliary predicates
  relating the outcome of the Cminor execution with the final node
  and value of the return register in the RTL execution. *)

Definition outcome_node
    (out: outcome)
    (ncont: node) (nexits: list node) (nret: node) (nd: node) : Prop :=
  match out with
  | Out_normal => ncont = nd
  | Out_exit n => nth_error nexits n = Some nd
  | Out_return _ => nret = nd
  end.

Definition match_return_reg
    (rs: regset) (rret: option reg) (v: val) : Prop :=
  match rret with
  | None => True
  | Some r => rs#r = v
  end.

Definition match_return_outcome
    (out: outcome) (rret: option reg) (rs: regset) : Prop :=
  match out with
  | Out_normal => True
  | Out_exit n => True
  | Out_return optv =>
      match rret, optv with
      | None, None => True
      | Some r, Some v => rs#r = v
      | _, _ => False
      end
  end.

(** The simulation diagram for the translation of statements
  is of the following form:
<<
                    I /\ P
       e, m, a ------------- ns, rs, m
         ||                      |
         ||                      |*
         ||                      |
         \/                      v
       e', m', out --------- nd, rs', m'
                    I /\ Q
>>
  where [transl_stmt map a ncont nexits nret rret s = OK ns s'].
  The left vertical arrow represents an execution of the statement [a]
  (assumption).  The right vertical arrow represents the execution of
  zero, one or several instructions in the generated RTL flow graph
  found in the final state [s'] (conclusion).  

  The invariant [I] is the agreement between Cminor environments and
  RTL register environment, as captured by [match_envs].

  The preconditions [P] include the well-formedness of the compilation
  environment [mut] and the agreement between the outcome [out]
  and the end node [nd].

  The postcondition [Q] states agreement between the outcome [out]
  and the value of the return register [rret]. *)

Definition transl_stmt_correct 
  (sp: val) (e: env) (m: mem) (a: stmt)
  (t: trace) (e': env) (m': mem) (out: outcome) : Prop :=
  forall map ncont nexits nret rret s ns s' nd rs
    (MWF: map_wf map s)
    (TE: transl_stmt map a ncont nexits nret rret s = OK ns s')
    (ME: match_env map e nil rs)
    (OUT: outcome_node out ncont nexits nret nd)
    (RRG: return_reg_ok s map rret),
  exists rs',
     exec_instrs tge s'.(st_code) sp ns rs m t nd rs' m'
  /\ match_env map e' nil rs'
  /\ match_return_outcome out rret rs'.

(** Finally, the correctness condition for the translation of functions
  is that the translated RTL function, when applied to the same arguments
  as the original Cminor function, returns the same value and performs
  the same modifications on the memory state. *)

Definition transl_function_correct
    (m: mem) (f: Cminor.fundef) (vargs: list val)
    (t: trace) (m':mem) (vres: val) : Prop :=
  forall tf
    (TE: transl_fundef f = Some tf),
  exec_function tge tf vargs m t vres m'.

(** The correctness of the translation is a huge induction over
  the Cminor evaluation derivation for the source program.  To keep
  the proof manageable, we put each case of the proof in a separate
  lemma.  There is one lemma for each Cminor evaluation rule.
  It takes as hypotheses the premises of the Cminor evaluation rule,
  plus the induction hypotheses, that is, the [transl_expr_correct], etc,
  corresponding to the evaluations of sub-expressions or sub-statements. *)

Lemma transl_expr_Evar_correct:
  forall (sp: val) (le: letenv) (e: env) (m: mem) (id: ident) (v: val),
  e!id = Some v ->
  transl_expr_correct sp le e m (Evar id) E0 m v.
Proof.
  intros; red; intros. monadInv TE. intro. 
  generalize EQ; unfold find_var. caseEq (map_vars map)!id.
  intros r' MV; monadSimpl. subst s0; subst r'. 
  generalize (add_move_correct _ _ sp _ _ _ _ rs m TE0).
  intros [rs1 [EX1 [RES1 OTHER1]]].
  exists rs1.
(* Exec *)
  split. assumption.
(* Match-env *)
  split. inversion TRG; subst.
  (* Optimized case rd = r *)
  rewrite MV in H3; injection H3; intro; subst r.
  apply match_env_exten with rs.
  intros. case (Reg.eq r rd); intro.
  subst r; assumption. apply OTHER1; assumption.
  assumption. 
  (* General case rd is temp *)
  apply match_env_invariant with rs.
  assumption. intros. apply OTHER1. congruence. 
(* Result value *)
  split. rewrite RES1. eauto with rtlg.
(* Other regs *)
  intros. destruct (Reg.eq rd r0).
  subst r0. inversion TRG; subst. 
  congruence.
  byContradiction. tauto.
  auto.

  intro; monadSimpl.
Qed.

Lemma transl_expr_Eop_correct:
  forall (sp: val) (le : letenv) (e : env) (m : mem) (op : operation)
         (al : exprlist) (t: trace) (m1 : mem) (vl : list val)
         (v: val),
  eval_exprlist ge sp le e m al t m1 vl ->
  transl_exprlist_correct sp le e m al t m1 vl ->
  eval_operation ge sp op vl = Some v ->
  transl_expr_correct sp le e m (Eop op al) t m1 v.
Proof.
  intros until v. intros EEL TEL EOP. red; intros.
  simpl in TE. monadInv TE. intro EQ1. 
  exploit TEL. 2: eauto. eauto with rtlg. eauto. eauto with rtlg.
  intros [rs1 [EX1 [ME1 [RR1 RO1]]]].
  exists (rs1#rd <- v).
(* Exec *)
  split. eapply exec_trans. eexact EX1. 
  apply exec_instrs_incr with s1. eauto with rtlg.
  apply exec_one; eapply exec_Iop. eauto with rtlg.
  subst vl. 
  rewrite (@eval_operation_preserved Cminor.fundef RTL.fundef ge tge). 
  eexact EOP.
  exact symbols_preserved. traceEq.
(* Match-env *)
  split. inversion TRG. eauto with rtlg.
(* Result reg *)
  split. apply Regmap.gss.
(* Other regs *)
  intros. rewrite Regmap.gso.
  apply RO1. eauto with rtlg. 
  destruct (In_dec Reg.eq r l).
  left. elim (alloc_regs_fresh_or_in_map _ _ _ _ _ MWF EQ r i); intro.
  auto. byContradiction; eauto with rtlg.  
  right; auto.
  red; intro; subst r. 
  elim H0; intro. inversion TRG. contradiction.
  tauto.
Qed.

Lemma transl_expr_Eload_correct:
 forall (sp: val) (le : letenv) (e : env) (m : mem)
    (chunk : memory_chunk) (addr : addressing) 
    (al : exprlist) (t: trace) (m1 : mem) (v : val) 
    (vl : list val) (a: val),
  eval_exprlist ge sp le e m al t m1 vl ->
  transl_exprlist_correct sp le e m al t m1 vl ->
  eval_addressing ge sp addr vl = Some a ->
  Mem.loadv chunk m1 a = Some v ->
  transl_expr_correct sp le e m (Eload chunk addr al) t m1 v.
Proof.
  intros; red; intros. simpl in TE. monadInv TE. intro EQ1. clear TE.
  assert (MWF1: map_wf map s1). eauto with rtlg.
  assert (TRG1: target_regs_ok s1 map al l). eauto with rtlg. 
  generalize (H0 _ _ _ _ _ _ _ MWF1 EQ1 ME TRG1).
  intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
  exists (rs1#rd <- v).
(* Exec *)
  split. eapply exec_trans. eexact EX1. 
  apply exec_instrs_incr with s1. eauto with rtlg.
  apply exec_one. eapply exec_Iload. eauto with rtlg.
  rewrite RES1. rewrite (@eval_addressing_preserved _ _ ge tge).
  eexact H1. exact symbols_preserved. assumption. traceEq.
(* Match-env *)
  split. eapply match_env_update_temp. assumption. inversion TRG. assumption.
(* Result *)
  split. apply Regmap.gss.
(* Other regs *)
  intros. rewrite Regmap.gso. apply OTHER1.
  eauto with rtlg.  
  case (In_dec Reg.eq r l); intro.
  elim (alloc_regs_fresh_or_in_map _ _ _ _ _ MWF EQ r i); intro.
  tauto. byContradiction. eauto with rtlg.
  tauto.
  red; intro; subst r. inversion TRG. tauto. 
Qed.

Lemma transl_expr_Estore_correct:
 forall (sp: val) (le : letenv) (e : env) (m : mem)
    (chunk : memory_chunk) (addr : addressing) 
    (al : exprlist) (b : expr) (t t1: trace) (m1 : mem) 
    (vl : list val) (t2: trace) (m2 m3 : mem) 
    (v : val) (a: val),
  eval_exprlist ge sp le e m al t1 m1 vl ->
  transl_exprlist_correct sp le e m al t1 m1 vl ->
  eval_expr ge sp le e m1 b t2 m2 v ->
  transl_expr_correct sp le e m1 b t2 m2 v ->
  eval_addressing ge sp addr vl = Some a -> 
  Mem.storev chunk m2 a v = Some m3 ->
  t = t1 ** t2 ->
  transl_expr_correct sp le e m (Estore chunk addr al b) t m3 v.
Proof.
  intros; red; intros. simpl in TE; monadInv TE. intro EQ2; clear TE.
  assert (MWF2: map_wf map s2). 
    apply map_wf_incr with s. 
    apply state_incr_trans2 with s0 s1; eauto with rtlg.
    assumption. 
  assert (TRG2: target_regs_ok s2 map al l). 
    apply target_regs_ok_incr with s0; eauto with rtlg.
  generalize (H0 _ _ _ _ _ _ _ MWF2 EQ2 ME TRG2).
  intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
  assert (MWF1: map_wf map s1). eauto with rtlg.
  assert (TRG1: target_reg_ok s1 map b rd).
    inversion TRG. apply target_reg_other; eauto with rtlg.
  generalize (H2 _ _ _ _ _ _ _ MWF1 EQ1 ME1 TRG1).
  intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]].
  exists rs2.
(* Exec *)
  split. eapply exec_trans. eexact EX1. 
  apply exec_instrs_incr with s2. eauto with rtlg.
  eapply exec_trans. eexact EX2. 
  apply exec_instrs_incr with s1. eauto with rtlg.
  apply exec_one. eapply exec_Istore. eauto with rtlg.
  assert (rs2##l = rs1##l).
    apply list_map_exten. intros r' IN. symmetry. apply OTHER2.
    eauto with rtlg. eauto with rtlg. 
    elim (alloc_regs_fresh_or_in_map _ _ _ _ _ MWF EQ r' IN); intro.
    tauto. right. apply sym_not_equal. 
    apply valid_fresh_different with s. inversion TRG; assumption.
    assumption.
  rewrite H6; rewrite RES1. 
  rewrite (@eval_addressing_preserved _ _ ge tge).
  eexact H3. exact symbols_preserved. 
  rewrite RES2. assumption.
  reflexivity. traceEq. 
(* Match-env *)
  split. assumption.
(* Result *)
  split. assumption.
(* Other regs *)
  intro r'; intros. transitivity (rs1#r').
  apply OTHER2. apply reg_valid_incr with s; eauto with rtlg. 
  assumption. 
  apply OTHER1. apply reg_valid_incr with s.
  apply state_incr_trans2 with s0 s1; eauto with rtlg. assumption.
  case (In_dec Reg.eq r' l); intro.
    elim (alloc_regs_fresh_or_in_map _ _ _ _ _ MWF EQ r' i); intro.
  tauto. byContradiction; eauto with rtlg. tauto.
Qed.  

Lemma transl_expr_Ecall_correct:
 forall (sp: val) (le : letenv) (e : env) (m : mem) 
    (sig : signature) (a : expr) (bl : exprlist) (t t1: trace)
    (m1: mem) (t2: trace) (m2 : mem) 
    (t3: trace) (m3: mem) (vf : val) 
    (vargs : list val) (vres : val) (f : Cminor.fundef),
  eval_expr ge sp le e m a t1 m1 vf ->
  transl_expr_correct sp le e m a t1 m1 vf ->
  eval_exprlist ge sp le e m1 bl t2 m2 vargs ->
  transl_exprlist_correct sp le e m1 bl t2 m2 vargs ->
  Genv.find_funct ge vf = Some f ->
  Cminor.funsig f = sig ->
  eval_funcall ge m2 f vargs t3 m3 vres ->
  transl_function_correct m2 f vargs t3 m3 vres ->
  t = t1 ** t2 ** t3 ->
  transl_expr_correct sp le e m (Ecall sig a bl) t m3 vres.
Proof.
  intros. red; simpl; intros.
  monadInv TE. intro EQ3. clear TE.
  assert (MWFa: map_wf map s3).
    apply map_wf_incr with s. 
    apply state_incr_trans3 with s0 s1 s2; eauto with rtlg.
    assumption.
  assert (TRGr: target_reg_ok s3 map a r). 
    apply target_reg_ok_incr with s0.
    apply state_incr_trans2 with s1 s2; eauto with rtlg.
    eauto with rtlg.
  generalize (H0 _ _ _ _ _ _ _ MWFa EQ3 ME TRGr).
  intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
  clear MWFa TRGr.
  assert (MWFbl: map_wf map s2).
    apply map_wf_incr with s. 
    apply state_incr_trans2 with s0 s1; eauto with rtlg.
    assumption.
  assert (TRGl: target_regs_ok s2 map bl l).
    apply target_regs_ok_incr with s1; eauto with rtlg.
  generalize (H2 _ _ _ _ _ _ _ MWFbl EQ2 ME1 TRGl).
  intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]].
  clear MWFbl TRGl.
 
  generalize (functions_translated vf f H3). intros [tf [TFIND TF]]. 
  generalize (H6 tf TF). intro EXF.

  assert (EX3: exec_instrs tge (st_code s2) sp n rs2 m2
                     t3 nd (rs2#rd <- vres) m3).
  apply exec_one. eapply exec_Icall.
  eauto with rtlg. simpl. replace (rs2#r) with vf. eexact TFIND.
  rewrite <- RES1. symmetry. apply OTHER2.
  apply reg_valid_incr with s0; eauto with rtlg.
  assert (MWFs0: map_wf map s0). eauto with rtlg.
  case (In_dec Reg.eq r l); intro.
  elim (alloc_regs_fresh_or_in_map _ _ _ _ _ MWFs0 EQ0 r i); intro.
  tauto. byContradiction. apply valid_fresh_absurd with r s0.
  eauto with rtlg. assumption.
  tauto.
  generalize (sig_transl_function _ _ TF). congruence.
  rewrite RES2. assumption.

  exists (rs2#rd <- vres).
(* Exec *)
  split. eapply exec_trans. eexact EX1. 
  apply exec_instrs_incr with s3. eauto with rtlg.
  eapply exec_trans. eexact EX2. 
  apply exec_instrs_incr with s2. eauto with rtlg.
  eexact EX3. reflexivity. traceEq. 
(* Match env *)
  split. apply match_env_update_temp. assumption.
  inversion TRG. assumption.
(* Result *)
  split. apply Regmap.gss.
(* Other regs *)
  intros.
  rewrite Regmap.gso. transitivity (rs1#r0). 
  apply OTHER2. 
    apply reg_valid_incr with s. 
    apply state_incr_trans2 with s0 s1; eauto with rtlg.
    assumption.
    assert (MWFs0: map_wf map s0). eauto with rtlg.
    case (In_dec Reg.eq r0 l); intro.
    elim (alloc_regs_fresh_or_in_map _ _ _ _ _ MWFs0 EQ0 r0 i); intro.
    tauto. byContradiction. apply valid_fresh_absurd with r0 s0.
    eauto with rtlg. assumption.
    tauto.
  apply OTHER1.
    apply reg_valid_incr with s.
    apply state_incr_trans3 with s0 s1 s2; eauto with rtlg.
    assumption.
    case (Reg.eq r0 r); intro.
    subst r0.
    elim (alloc_reg_fresh_or_in_map _ _ _ _ _ MWF EQ); intro.
    tauto. byContradiction; eauto with rtlg.
    tauto.
  red; intro; subst r0.
  inversion TRG. tauto. 
Qed.

Lemma transl_expr_Econdition_correct:
 forall (sp: val) (le : letenv) (e : env) (m : mem) 
    (a : condexpr) (b c : expr) (t t1: trace) (m1 : mem) 
    (v1 : bool) (t2: trace) (m2 : mem) (v2 : val),
  eval_condexpr ge sp le e m a t1 m1 v1 ->
  transl_condition_correct sp le e m a t1 m1 v1 ->
  eval_expr ge sp le e m1 (if v1 then b else c) t2 m2 v2 ->
  transl_expr_correct sp le e m1 (if v1 then b else c) t2 m2 v2 ->
  t = t1 ** t2 ->
  transl_expr_correct sp le e m (Econdition a b c) t m2 v2.
Proof.
  intros; red; intros. simpl in TE; monadInv TE. intro EQ1; clear TE.

  assert (MWF1: map_wf map s1).
    apply map_wf_incr with s. eauto with rtlg. assumption.
  generalize (H0 _ _ _ _ _ _ _ MWF1 EQ1 ME).
  intros [rs1 [EX1 [ME1 OTHER1]]].
  destruct v1.

  assert (MWF0: map_wf map s0). eauto with rtlg.
  assert (TRG0: target_reg_ok s0 map b rd).
    inversion TRG. apply target_reg_other; eauto with rtlg.
  generalize (H2 _ _ _ _ _ _ _ MWF0 EQ0 ME1 TRG0).  
  intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]].
  exists rs2.
(* Exec *)
  split. eapply exec_trans. eexact EX1. 
  apply exec_instrs_incr with s1. eauto with rtlg.
  eexact EX2. auto.
(* Match-env *)
  split. assumption.
(* Result value *)
  split. assumption.
(* Other regs *)
  intros. transitivity (rs1#r). 
  apply OTHER2; auto. eauto with rtlg.
  apply OTHER1; auto. apply reg_valid_incr with s.
  apply state_incr_trans with s0; eauto with rtlg. assumption.

  assert (TRGc: target_reg_ok s map c rd).
    inversion TRG. apply target_reg_other; auto.
  generalize (H2 _ _ _ _ _ _ _ MWF EQ ME1 TRGc).  
  intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]].
  exists rs2.
(* Exec *)
  split. eapply exec_trans. eexact EX1. 
  apply exec_instrs_incr with s0. eauto with rtlg.
  eexact EX2. auto.
(* Match-env *)
  split. assumption.
(* Result value *)
  split. assumption.
(* Other regs *)
  intros. transitivity (rs1#r). 
  apply OTHER2; auto. eauto with rtlg.
  apply OTHER1; auto. apply reg_valid_incr with s.
  apply state_incr_trans2 with s0 s1; eauto with rtlg. assumption.
Qed.

Lemma transl_expr_Elet_correct:
  forall (sp: val) (le : letenv) (e : env) (m : mem) 
    (a b : expr) (t t1: trace) (m1 : mem) (v1 : val) 
    (t2: trace) (m2 : mem) (v2 : val),
  eval_expr ge sp le e m a t1 m1 v1 ->
  transl_expr_correct sp le e m a t1 m1 v1 ->
  eval_expr ge sp (v1 :: le) e m1 b t2 m2 v2 ->
  transl_expr_correct sp (v1 :: le) e m1 b t2 m2 v2 ->
  t = t1 ** t2 ->
  transl_expr_correct sp le e m (Elet a b) t m2 v2.
Proof.
  intros; red; intros.
  simpl in TE; monadInv TE. intro EQ1.
  assert (MWF1: map_wf map s1). eauto with rtlg.
  assert (TRG1: target_reg_ok s1 map a r).
  eapply target_reg_other; eauto with rtlg.
  generalize (H0 _ _ _ _ _ _ _ MWF1 EQ1 ME TRG1).
  intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
  assert (MWF2: map_wf (add_letvar map r) s0). 
  apply add_letvar_wf; eauto with rtlg. 
  assert (ME2: match_env (add_letvar map r) e (v1 :: le) rs1).
  apply match_env_letvar; assumption.
  assert (TRG2: target_reg_ok s0 (add_letvar map r) b rd).
  inversion TRG. apply target_reg_other. 
  unfold reg_in_map, add_letvar; simpl. red; intro.
  elim H10; intro. apply H4. left. assumption.
  elim H11; intro. apply valid_fresh_absurd with rd s.
  assumption. rewrite <- H12. eauto with rtlg.
  apply H4. right. assumption.
  eauto with rtlg.
  generalize (H2 _ _ _ _ _ _ _ MWF2 EQ0 ME2 TRG2).
  intros [rs2 [EX2 [ME3 [RES2 OTHER2]]]].
  exists rs2.
(* Exec *)
  split. eapply exec_trans. eexact EX1. 
  apply exec_instrs_incr with s1. eauto with rtlg. eexact EX2. auto.
(* Match-env *)
  split. apply mk_match_env. exact (me_vars _ _ _ _ ME3). 
  generalize (me_letvars _ _ _ _ ME3). 
  unfold add_letvar; simpl. intro X; injection X; auto.
(* Result *)
  split. assumption.
(* Other regs *)
  intros. transitivity (rs1#r0). 
  apply OTHER2. eauto with rtlg. 
  elim H5; intro. left. 
  unfold reg_in_map, add_letvar; simpl.
  unfold reg_in_map in H6; tauto.
  tauto.
  apply OTHER1. eauto with rtlg.
  right. red; intro. apply valid_fresh_absurd with r0 s.
  assumption. rewrite H6. eauto with rtlg.
Qed.

Lemma transl_expr_Eletvar_correct:
  forall (sp: val) (le : list val) (e : env) 
    (m : mem) (n : nat) (v : val),
  nth_error le n = Some v ->
  transl_expr_correct sp le e m (Eletvar n) E0 m v.
Proof.
  intros; red; intros. 
  simpl in TE; monadInv TE. intro EQ1.
  generalize EQ. unfold find_letvar. 
  caseEq (nth_error (map_letvars map) n).
  intros r0 NE; monadSimpl. subst s0; subst r0.
  generalize (add_move_correct _ _ sp _ _ _ _ rs m EQ1).
  intros [rs1 [EX1 [RES1 OTHER1]]].
  exists rs1.
(* Exec *)
  split. exact EX1.
(* Match-env *)
  split. inversion TRG.
  assert (r = rd). congruence.
  subst r. apply match_env_exten with rs. 
  intros. case (Reg.eq r rd); intro. subst r; auto. auto. auto.
  apply match_env_invariant with rs. auto. 
  intros. apply OTHER1. red;intro;subst r1. contradiction.
(* Result *)
  split. rewrite RES1. 
  generalize H. rewrite <- (me_letvars _ _ _ _ ME). 
  change positive with reg.
  rewrite list_map_nth. rewrite NE. simpl. congruence. 
(* Other regs *)
  intros. inversion TRG. 
  assert (r = rd). congruence. subst r.
  case (Reg.eq r0 rd); intro. subst r0; auto. auto. 
  apply OTHER1. red; intro; subst r0. tauto.

  intro; monadSimpl.
Qed.

Lemma transl_expr_Ealloc_correct:
  forall (sp: val) (le : letenv) (e : env) (m : mem) 
    (a : expr) (t: trace) (m1 : mem) (n: int)
    (m2: mem) (b: block),
  eval_expr ge sp le e m a t m1 (Vint n) ->
  transl_expr_correct sp le e m a t m1 (Vint n) ->
  Mem.alloc m1 0 (Int.signed n) = (m2, b) ->
  transl_expr_correct sp le e m (Ealloc a) t m2 (Vptr b Int.zero).
Proof.
  intros until b; intros EE TEC ALLOC; red; intros.
  simpl in TE. monadInv TE. intro EQ1.
  assert (TRG': target_reg_ok s1 map a r); eauto with rtlg.
  assert (MWF': map_wf map s1). eauto with rtlg.
  generalize (TEC _ _ _ _ _ _ _ MWF' EQ1 ME TRG').
  intros [rs1 [EX1 [ME1 [RR1 RO1]]]].
  exists (rs1#rd <- (Vptr b Int.zero)).
(* Exec *)
  split. eapply exec_trans. eexact EX1. 
  apply exec_instrs_incr with s1. eauto with rtlg.
  apply exec_one; eapply exec_Ialloc. eauto with rtlg.
  eexact RR1. assumption. traceEq. 
(* Match-env *)
  split. inversion TRG. eauto with rtlg.
(* Result *)
  split. apply Regmap.gss.
(* Other regs *)
  intros. rewrite Regmap.gso.
  apply RO1. eauto with rtlg. 
  case (Reg.eq r0 r); intro.
  subst r0. left. elim (alloc_reg_fresh_or_in_map _ _ _ _ _ MWF EQ); intro. 
  auto. byContradiction; eauto with rtlg.
  right; assumption.
  elim H0; intro. red; intro. subst r0. inversion TRG. contradiction. 
  auto.
Qed.

Lemma transl_condition_CEtrue_correct:
  forall (sp: val) (le : letenv) (e : env) (m : mem),
  transl_condition_correct sp le e m CEtrue E0 m true.
Proof.
  intros; red; intros. simpl in TE; monadInv TE. subst ns.
  exists rs. split. apply exec_refl. split. auto. auto.
Qed.    

Lemma transl_condition_CEfalse_correct:
  forall (sp: val) (le : letenv) (e : env) (m : mem),
  transl_condition_correct sp le e m CEfalse E0 m false.
Proof.
  intros; red; intros. simpl in TE; monadInv TE. subst ns.
  exists rs. split. apply exec_refl. split. auto. auto.
Qed.    

Lemma transl_condition_CEcond_correct:
  forall (sp: val) (le : letenv) (e : env) (m : mem)
    (cond : condition) (al : exprlist) (t1: trace)
    (m1 : mem) (vl : list val) (b : bool),
  eval_exprlist ge sp le e m al t1 m1 vl ->
  transl_exprlist_correct sp le e m al t1 m1 vl ->
  eval_condition cond vl =  Some b ->
  transl_condition_correct sp le e m (CEcond cond al) t1 m1 b.
Proof.
  intros; red; intros. simpl in TE; monadInv TE. intro EQ1; clear TE.
  assert (MWF1: map_wf map s1). eauto with rtlg.
  assert (TRG: target_regs_ok s1 map al l).  eauto with rtlg.
  generalize (H0 _ _ _ _ _ _ _ MWF1 EQ1 ME TRG).
  intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
  exists rs1.
(* Exec *)
  split. eapply exec_trans. eexact EX1. 
  apply exec_instrs_incr with s1. eauto with rtlg.
  apply exec_one. 
  destruct b.
  eapply exec_Icond_true. eauto with rtlg. 
  rewrite RES1. assumption.
  eapply exec_Icond_false. eauto with rtlg. 
  rewrite RES1. assumption.
  traceEq.
(* Match-env *)
  split. assumption.
(* Regs *)
  intros. apply OTHER1. eauto with rtlg. 
  case (In_dec Reg.eq r l); intro.
  elim (alloc_regs_fresh_or_in_map _ _ _ _ _ MWF EQ r i); intro.
  tauto. byContradiction; eauto with rtlg.
  tauto.
Qed.

Lemma transl_condition_CEcondition_correct:
  forall (sp: val) (le : letenv) (e : env) (m : mem)
    (a b c : condexpr) (t t1: trace) (m1 : mem) 
    (vb1 : bool) (t2: trace) (m2 : mem) (vb2 : bool),
  eval_condexpr ge sp le e m a t1 m1 vb1 ->
  transl_condition_correct sp le e m a t1 m1 vb1 ->
  eval_condexpr ge sp le e m1 (if vb1 then b else c) t2 m2 vb2 ->
  transl_condition_correct sp le e m1 (if vb1 then b else c) t2 m2 vb2 ->
  t = t1 ** t2 ->
  transl_condition_correct sp le e m (CEcondition a b c) t m2 vb2.
Proof.
  intros; red; intros. simpl in TE; monadInv TE. intro EQ1; clear TE.
  assert (MWF1: map_wf map s1). eauto with rtlg.
  generalize (H0 _ _ _ _ _ _ _ MWF1 EQ1 ME).
  intros [rs1 [EX1 [ME1 OTHER1]]].
  destruct vb1.

  assert (MWF0: map_wf map s0). eauto with rtlg.
  generalize (H2 _ _ _ _ _ _ _ MWF0 EQ0 ME1).
  intros [rs2 [EX2 [ME2 OTHER2]]].
  exists rs2.
  split. eapply exec_trans. eexact EX1. 
  apply exec_instrs_incr with s1. eauto with rtlg.
  eexact EX2. auto.
  split. assumption. 
  intros. transitivity (rs1#r). 
  apply OTHER2; eauto with rtlg.
  apply OTHER1; eauto with rtlg.

  generalize (H2 _ _ _ _ _ _ _ MWF EQ ME1).
  intros [rs2 [EX2 [ME2 OTHER2]]].
  exists rs2.
  split. eapply exec_trans. eexact EX1. 
  apply exec_instrs_incr with s0. eauto with rtlg.
  eexact EX2. auto.
  split. assumption. 
  intros. transitivity (rs1#r). 
  apply OTHER2; eauto with rtlg.
  apply OTHER1; eauto with rtlg.
Qed.
 
Lemma transl_exprlist_Enil_correct:
  forall (sp: val) (le : letenv) (e : env) (m : mem),
  transl_exprlist_correct sp le e m Enil E0 m nil.
Proof.
  intros; red; intros. 
  generalize TE. simpl. destruct rl; monadSimpl. 
  subst s'; subst ns. exists rs.
  split. apply exec_refl.
  split. assumption.
  split. reflexivity.
  intros. reflexivity.
Qed.

Lemma transl_exprlist_Econs_correct:
  forall (sp: val) (le : letenv) (e : env) (m : mem) 
    (a : expr) (bl : exprlist) (t t1: trace) (m1 : mem) 
    (v : val) (t2: trace) (m2 : mem) (vl : list val),
  eval_expr ge sp le e m a t1 m1 v ->
  transl_expr_correct sp le e m a t1 m1 v ->
  eval_exprlist ge sp le e m1 bl t2 m2 vl ->
  transl_exprlist_correct sp le e m1 bl t2 m2 vl ->
  t = t1 ** t2 ->
  transl_exprlist_correct sp le e m (Econs a bl) t m2 (v :: vl).
Proof.
  intros. red. intros. 
  inversion TRG.
  rewrite <- H10 in TE. simpl in TE. monadInv TE. intro EQ1.
  assert (MWF1: map_wf map s1); eauto with rtlg.
  assert (TRG1: target_reg_ok s1 map a r); eauto with rtlg.
  generalize (H0 _ _ _ _ _ _ _ MWF1 EQ1 ME TRG1).
  intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
  generalize (H2 _ _ _ _ _ _ _ MWF EQ ME1 H11).
  intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]].
  exists rs2.
(* Exec *)
  split. eapply exec_trans. eexact EX1. 
  apply exec_instrs_incr with s1. eauto with rtlg. 
  eexact EX2. auto. 
(* Match-env *)
  split. assumption.
(* Results *)
  split. simpl. rewrite RES2. rewrite OTHER2. rewrite RES1.
  reflexivity.
  eauto with rtlg. 
  eauto with rtlg.
(* Other regs *)
  simpl. intros.
  transitivity (rs1#r0).
  apply OTHER2; auto. tauto. 
  apply OTHER1; auto. eauto with rtlg. 
  elim H13; intro. left; assumption. right; apply sym_not_equal; tauto.
Qed.

Lemma transl_funcall_internal_correct:
  forall (m : mem) (f : Cminor.function)
         (vargs : list val) (m1 : mem) (sp : block) (e : env) (t : trace)
         (e2 : env) (m2 : mem) (out : outcome) (vres : val),
  Mem.alloc m 0 (fn_stackspace f) = (m1, sp) ->
  set_locals (fn_vars f) (set_params vargs (Cminor.fn_params f)) = e ->
  exec_stmt ge (Vptr sp Int.zero) e m1 (fn_body f) t e2 m2 out ->
  transl_stmt_correct (Vptr sp Int.zero) e m1 (fn_body f) t e2 m2 out ->
  outcome_result_value out f.(Cminor.fn_sig).(sig_res) vres ->
  transl_function_correct m (Internal f)
            vargs t (Mem.free m2 sp) vres.
Proof.
  intros; red; intros.
  generalize TE. unfold transl_fundef, transl_function; simpl.
  caseEq (transl_fun f init_state).
  intros; discriminate.
  intros ns s. unfold transl_fun. monadSimpl. 
  subst ns. intros EQ4. injection EQ4; intro TF; clear EQ4.
  subst s4.

  pose (rs := init_regs vargs x).
  assert (ME: match_env y0 e nil rs).
  rewrite <- H0. unfold rs. 
  eapply match_init_env_init_reg; eauto. 

  assert (OUT: outcome_node out n nil n n).
  red. generalize H3. unfold outcome_result_value.
  destruct out; contradiction || auto. 
 
  assert (MWF1: map_wf y0 s1).
  eapply add_vars_wf. eexact EQ0. 
  eapply add_vars_wf. eexact EQ.
  apply init_mapping_wf.

  assert (MWF: map_wf y0 s3).
  apply map_wf_incr with s1. apply state_incr_trans with s2; eauto with rtlg.
  assumption.

  set (rr := ret_reg (Cminor.fn_sig f) r) in *.
  assert (RRG: return_reg_ok s3 y0 rr).
  apply return_reg_ok_incr with s2. eauto with rtlg. 
  unfold rr; apply new_reg_return_ok with s1; assumption.

  generalize (H2 _ _ _ _ _ _ _ _ _ rs MWF EQ3 ME OUT RRG).
  intros [rs1 [EX1 [ME1 MR1]]].

  rewrite <- TF. apply exec_funct_internal with m1 n rs1 rr; simpl.
  assumption.
  exact EX1.
  apply instr_at_incr with s3.
  eauto with rtlg. discriminate. eauto with rtlg.
  generalize MR1. unfold match_return_outcome.
  generalize H3. unfold outcome_result_value.
  unfold rr, ret_reg; destruct (sig_res (Cminor.fn_sig f)).
  unfold regmap_optget. destruct out; try contradiction.
  destruct o; try contradiction. intros; congruence.
  unfold regmap_optget. destruct out; contradiction||auto.
  destruct o; contradiction||auto.
Qed.

Lemma transl_funcall_external_correct:
  forall (ef : external_function) (m : mem) (args : list val) (t: trace) (res : val),
  event_match ef args t res ->
  transl_function_correct m (External ef) args t m res.
Proof.
  intros; red; intros. unfold transl_function in TE; simpl in TE.
  inversion TE; subst tf. 
  apply exec_funct_external. auto.
Qed.

Lemma transl_stmt_Sskip_correct:
  forall (sp: val) (e : env) (m : mem),
  transl_stmt_correct sp e m Sskip E0 e m Out_normal.
Proof.
  intros; red; intros. simpl in TE. monadInv TE.
  subst s'; subst ns.
  simpl in OUT. subst ncont. 
  exists rs. simpl. intuition. apply exec_refl.
Qed.

Lemma transl_stmt_Sseq_continue_correct:
  forall (sp : val) (e : env) (m : mem) (t: trace) (s1 : stmt)
         (t1: trace) (e1 : env) (m1 : mem) (s2 : stmt) (t2: trace)
         (e2 : env) (m2 : mem) (out : outcome),
  exec_stmt ge sp e m s1 t1 e1 m1 Out_normal ->
  transl_stmt_correct sp e m s1 t1 e1 m1 Out_normal ->
  exec_stmt ge sp e1 m1 s2 t2 e2 m2 out ->
  transl_stmt_correct sp e1 m1 s2 t2 e2 m2 out ->
  t = t1 ** t2 ->
  transl_stmt_correct sp e m (Sseq s1 s2) t e2 m2 out.
Proof.
  intros; red; intros. simpl in TE; monadInv TE. intro EQ0.
  assert (MWF1: map_wf map s0). eauto with rtlg.
  assert (OUTs: outcome_node Out_normal n nexits nret n).
    simpl. auto.
  assert (RRG1: return_reg_ok s0 map rret). eauto with rtlg.
  generalize (H0 _ _ _ _ _ _ _ _ _ _ MWF1 EQ0 ME OUTs RRG1).
  intros [rs1 [EX1 [ME1 MR1]]].
  generalize (H2 _ _ _ _ _ _ _ _ _ _ MWF EQ ME1 OUT RRG).
  intros [rs2 [EX2 [ME2 MR2]]].
  exists rs2.
(* Exec *)
  split. eapply exec_trans. eexact EX1. 
  apply exec_instrs_incr with s0. eauto with rtlg.
  eexact EX2. auto.
(* Match-env + return *)
  tauto.
Qed.

Lemma transl_stmt_Sseq_stop_correct:
  forall (sp : val) (e : env) (m : mem) (t: trace) (s1 s2 : stmt) (e1 : env)
         (m1 : mem) (out : outcome),
  exec_stmt ge sp e m s1 t e1 m1 out ->
  transl_stmt_correct sp e m s1 t e1 m1 out ->
  out <> Out_normal ->
  transl_stmt_correct sp e m (Sseq s1 s2) t e1 m1 out.
Proof.
  intros; red; intros. 
  simpl in TE; monadInv TE. intro EQ0; clear TE.
  assert (MWF1: map_wf map s0). eauto with rtlg.
  assert (OUTs: outcome_node out n nexits nret nd).
    destruct out; simpl; auto. tauto. 
  assert (RRG1: return_reg_ok s0 map rret). eauto with rtlg.
  exact (H0 _ _ _ _ _ _ _ _ _ _ MWF1 EQ0 ME OUTs RRG1).
Qed.

Lemma transl_stmt_Sexpr_correct:
  forall (sp: val) (e : env) (m : mem) (a : expr) (t: trace)
    (m1 : mem) (v : val),
  eval_expr ge sp nil e m a t m1 v ->
  transl_expr_correct sp nil e m a t m1 v ->
  transl_stmt_correct sp e m (Sexpr a) t e m1 Out_normal.
Proof.
  intros; red; intros.
  simpl in OUT. subst nd.
  unfold transl_stmt in TE. monadInv TE. intro EQ1.
  assert (MWF0: map_wf map s0). eauto with rtlg.
  assert (TRG: target_reg_ok s0 map a r). eauto with rtlg.
  generalize (H0 _ _ _ _ _ _ _ MWF0 EQ1 ME TRG).
  intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
  exists rs1; simpl; tauto.
Qed.

Lemma transl_stmt_Sassign_correct:
 forall (sp: val) (e : env) (m : mem) 
    (id : ident) (a : expr) (t: trace) (m1 : mem) (v : val),
  eval_expr ge sp nil e m a t m1 v ->
  transl_expr_correct sp nil e m a t m1 v ->
  transl_stmt_correct sp e m (Sassign id a) t (PTree.set id v e) m1 Out_normal.
Proof.
  intros; red; intros.
  simpl in TE. monadInv TE. intro EQ2. 
  assert (MWF0: map_wf map s2). 
    apply map_wf_incr with s. eauto 6 with rtlg. auto.
  assert (TRGa: target_reg_ok s2 map a r0). eauto 6 with rtlg.
  generalize (H0 _ _ _ _ _ _ _ MWF0 EQ2 ME TRGa).
  intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
  generalize (add_move_correct _ _ sp _ _ _ _ rs1 m1 EQ1).
  intros [rs2 [EX2 [RES2 OTHER2]]].
  exists rs2.
(* Exec *)
  split. inversion OUT; subst. eapply exec_trans. eexact EX1.
  apply exec_instrs_incr with s2. eauto with rtlg.
  eexact EX2. traceEq.
(* Match-env *)
  split. 
  apply match_env_update_var with rs1 r s s0; auto.
  congruence.
(* Outcome *)
  simpl; auto.
Qed.

Lemma transl_stmt_Sifthenelse_correct:
  forall (sp: val) (e : env) (m : mem) (a : condexpr)
    (s1 s2 : stmt) (t t1: trace) (m1 : mem) 
    (v1 : bool) (t2: trace) (e2 : env) (m2 : mem) (out : outcome),
  eval_condexpr ge sp nil e m a t1 m1 v1 ->
  transl_condition_correct sp nil e m a t1 m1 v1 ->
  exec_stmt ge sp e m1 (if v1 then s1 else s2) t2 e2 m2 out ->
  transl_stmt_correct sp e m1 (if v1 then s1 else s2) t2 e2 m2 out ->
  t = t1 ** t2 ->
  transl_stmt_correct sp e m (Sifthenelse a s1 s2) t e2 m2 out.
Proof.
  intros; red; intros until rs; intro MWF.
  simpl. case (more_likely a s1 s2); monadSimpl; intro EQ2; intros.
  assert (MWF1: map_wf map s3). eauto with rtlg.
  generalize (H0 _ _ _ _ _ _ rs MWF1 EQ2 ME).
  intros [rs1 [EX1 [ME1 OTHER1]]].
  destruct v1.
  assert (MWF0: map_wf map s0). eauto with rtlg.
  assert (RRG0: return_reg_ok s0 map rret). eauto with rtlg.
  generalize (H2 _ _ _ _ _ _ _ _ _ _ MWF0 EQ0 ME1 OUT RRG0).
  intros [rs2 [EX2 [ME2 MRE2]]].
  exists rs2. split.
  eapply exec_trans. eexact EX1. apply exec_instrs_incr with s3.
  eauto with rtlg. eexact EX2. auto.
  tauto.
  generalize (H2 _ _ _ _ _ _ _ _ _ _ MWF EQ ME1 OUT RRG).
  intros [rs2 [EX2 [ME2 MRE2]]].
  exists rs2. split.
  eapply exec_trans. eexact EX1. apply exec_instrs_incr with s0.
  eauto with rtlg. eexact EX2. auto.
  tauto.

  assert (MWF1: map_wf map s3). eauto with rtlg.
  generalize (H0 _ _ _ _ _ _ rs MWF1 EQ2 ME).
  intros [rs1 [EX1 [ME1 OTHER1]]].
  destruct v1.
  generalize (H2 _ _ _ _ _ _ _ _ _ _ MWF EQ ME1 OUT RRG).
  intros [rs2 [EX2 [ME2 MRE2]]].
  exists rs2. split.
  eapply exec_trans. eexact EX1. apply exec_instrs_incr with s0.
  eauto with rtlg. eexact EX2. auto.
  tauto.
  assert (MWF0: map_wf map s0). eauto with rtlg.
  assert (RRG0: return_reg_ok s0 map rret). eauto with rtlg.
  generalize (H2 _ _ _ _ _ _ _ _ _ _ MWF0 EQ0 ME1 OUT RRG0).
  intros [rs2 [EX2 [ME2 MRE2]]].
  exists rs2. split.
  eapply exec_trans. eexact EX1. apply exec_instrs_incr with s3.
  eauto with rtlg. eexact EX2. auto.
  tauto.
Qed.

Lemma transl_stmt_Sloop_loop_correct:
  forall (sp: val) (e : env) (m : mem) (sl : stmt) (t t1: trace)
    (e1 : env) (m1 : mem) (t2: trace) (e2 : env) (m2 : mem) 
    (out : outcome),
  exec_stmt ge sp e m sl t1 e1 m1 Out_normal ->
  transl_stmt_correct sp e m sl t1 e1 m1 Out_normal ->
  exec_stmt ge sp e1 m1 (Sloop sl) t2 e2 m2 out ->
  transl_stmt_correct sp e1 m1 (Sloop sl) t2 e2 m2 out ->
  t = t1 ** t2 ->
  transl_stmt_correct sp e m (Sloop sl) t e2 m2 out.
Proof.
  intros; red; intros.
  generalize TE. simpl. monadSimpl. subst s2; subst n0. intros.
  assert (MWF0: map_wf map s0). apply map_wf_incr with s.
  eapply reserve_instr_incr; eauto.
  assumption.
  assert (OUT0: outcome_node Out_normal n nexits nret n).
  unfold outcome_node. auto.
  assert (RRG0: return_reg_ok s0 map rret). 
  apply return_reg_ok_incr with s.
  eapply reserve_instr_incr; eauto.
  assumption.
  generalize (H0 _ _ _ _ _ _ _ _ _ _ MWF0 EQ0 ME OUT0 RRG0).
  intros [rs1 [EX1 [ME1 MR1]]].
  generalize (H2 _ _ _ _ _ _ _ _ _ _ MWF TE ME1 OUT RRG).
  intros [rs2 [EX2 [ME2 MR2]]].
  exists rs2.
  split. eapply exec_trans.
  apply exec_instrs_extends with s1. 
  eapply update_instr_extends.
  eexact EQ. eauto with rtlg. eexact EQ1. eexact EX1.
  apply exec_trans with E0 ns rs1 m1 t2.
  apply exec_one. apply exec_Inop. 
  generalize EQ1. unfold update_instr. 
  case (plt n (st_nextnode s1)); intro; monadSimpl.
  rewrite <- H5. simpl. apply PTree.gss.
  exact EX2.
  reflexivity. traceEq. 
  tauto.
Qed.

Lemma transl_stmt_Sloop_stop_correct:
  forall (sp: val) (e : env) (m : mem) (t: trace) (sl : stmt) 
    (e1 : env) (m1 : mem) (out : outcome),
  exec_stmt ge sp e m sl t e1 m1 out ->
  transl_stmt_correct sp e m sl t e1 m1 out ->
  out <> Out_normal ->
  transl_stmt_correct sp e m (Sloop sl) t e1 m1 out.
Proof.
  intros; red; intros.
  simpl in TE. monadInv TE. subst s2; subst n0.
  assert (MWF0: map_wf map s0). apply map_wf_incr with s.
  eapply reserve_instr_incr; eauto. assumption.
  assert (OUT0: outcome_node out n nexits nret nd).
  generalize OUT. unfold outcome_node. 
  destruct out; auto. elim H1; auto.
  assert (RRG0: return_reg_ok s0 map rret). 
  apply return_reg_ok_incr with s.
  eapply reserve_instr_incr; eauto.
  assumption.
  generalize (H0 _ _ _ _ _ _ _ _ _ _ MWF0 EQ0 ME OUT0 RRG0).
  intros [rs1 [EX1 [ME1 MR1]]].
  exists rs1. split.
  apply exec_instrs_extends with s1. 
  eapply update_instr_extends.
  eexact EQ. eauto with rtlg. eexact EQ1. eexact EX1.
  tauto.
Qed.  

Lemma transl_stmt_Sblock_correct:
  forall (sp: val) (e : env) (m : mem) (sl : stmt) (t: trace)
    (e1 : env) (m1 : mem) (out : outcome),
  exec_stmt ge sp e m sl t e1 m1 out ->
  transl_stmt_correct sp e m sl t e1 m1 out ->
  transl_stmt_correct sp e m (Sblock sl) t e1 m1 (outcome_block out).
Proof.
  intros; red; intros. simpl in TE. 
  assert (OUT': outcome_node out ncont (ncont :: nexits) nret nd).
  generalize OUT. unfold outcome_node, outcome_block.
  destruct out.
  auto.
  destruct n. simpl. intro; unfold value; congruence.
  simpl. auto.
  auto.
  generalize (H0 _ _ _ _ _ _ _ _ _ _ MWF TE ME OUT' RRG).
  intros [rs1 [EX1 [ME1 MR1]]].
  exists rs1. 
  split. assumption.
  split. assumption.
  generalize MR1. unfold match_return_outcome, outcome_block.
  destruct out; auto. 
  destruct n; simpl; auto.
Qed.

Lemma transl_exit_correct:
  forall nexits ex s nd s',
  transl_exit nexits ex s = OK nd s' ->
  nth_error nexits ex = Some nd.
Proof.
  intros until s'. unfold transl_exit. 
  case (nth_error nexits ex); intros; simplify_eq H; congruence.
Qed.

Lemma transl_stmt_Sexit_correct:
  forall (sp: val) (e : env) (m : mem) (n : nat),
  transl_stmt_correct sp e m (Sexit n) E0 e m (Out_exit n).
Proof.
  intros; red; intros. 
  simpl in TE. simpl in OUT. 
  generalize (transl_exit_correct _ _ _ _ _ TE); intro.
  assert (ns = nd). congruence. subst ns.
  exists rs. simpl. intuition. apply exec_refl.
Qed.

Lemma transl_switch_correct:
  forall sp rs m r i nexits nd default cases s ns s',
  transl_switch r nexits cases default s = OK ns s' ->
  nth_error nexits (switch_target i default cases) = Some nd ->
  rs#r = Vint i ->
  exec_instrs tge s'.(st_code) sp ns rs m E0 nd rs m.
Proof.
  induction cases; simpl; intros.
  generalize (transl_exit_correct _ _ _ _ _ H). intros.
  assert (ns = nd). congruence. subst ns. apply exec_refl.
  destruct a as [key1 exit1]. monadInv H. clear H. intro EQ1.
  caseEq (Int.eq i key1); intro IEQ; rewrite IEQ in H0.
  (* i = key1 *)
  apply exec_trans with E0 n0 rs m E0. apply exec_one. 
  eapply exec_Icond_true. eauto with rtlg. simpl. rewrite H1. congruence.
  generalize (transl_exit_correct _ _ _ _ _ EQ0); intro.
  assert (n0 = nd). congruence. subst n0. apply exec_refl. traceEq.
  (* i <> key1 *)
  apply exec_trans with E0 n rs m E0. apply exec_one.
  eapply exec_Icond_false. eauto with rtlg. simpl. rewrite H1. congruence.
  apply exec_instrs_incr with s0; eauto with rtlg. traceEq.
Qed.

Lemma transl_stmt_Sswitch_correct:
  forall (sp : val) (e : env) (m : mem) (a : expr)
         (cases : list (int * nat)) (default : nat) 
         (t1 : trace) (m1 : mem) (n : int),
  eval_expr ge sp nil e m a t1 m1 (Vint n) ->
  transl_expr_correct sp nil e m a t1 m1 (Vint n) ->
  transl_stmt_correct sp e m (Sswitch a cases default) t1 e m1
         (Out_exit (switch_target n default cases)).
Proof.
  intros; red; intros. monadInv TE. clear TE; intros EQ1.
  simpl in OUT. 
  assert (state_incr s s1). eauto with rtlg.

  red in H0. 
  assert (MWF1: map_wf map s1). eauto with rtlg.
  assert (TRG1: target_reg_ok s1 map a r). eauto with rtlg.
  destruct (H0 _ _ _ _ _ _ _ MWF1 EQ1 ME TRG1)
        as [rs' [EXEC1 [ME1 [RES1 OTHER1]]]].
  simpl. exists rs'.
  (* execution *)
  split. eapply exec_trans. eexact EXEC1. 
  apply exec_instrs_incr with s1. eauto with rtlg.
  eapply transl_switch_correct; eauto. traceEq. 
  (* match_env & match_reg *)
  tauto.
Qed.

Lemma transl_stmt_Sreturn_none_correct:
  forall (sp: val) (e : env) (m : mem),
  transl_stmt_correct sp e m (Sreturn None) E0 e m (Out_return None).
Proof.
  intros; red; intros. generalize TE. simpl.
  destruct rret; monadSimpl. 
  simpl in OUT. subst ns; subst nret.
  exists rs. intuition. apply exec_refl.
Qed.

Lemma transl_stmt_Sreturn_some_correct:
  forall (sp: val) (e : env) (m : mem) (a : expr) (t: trace)
    (m1 : mem) (v : val),
  eval_expr ge sp nil e m a t m1 v ->
  transl_expr_correct sp nil e m a t m1 v ->
  transl_stmt_correct sp e m (Sreturn (Some a)) t e m1 (Out_return (Some v)).
Proof.
  intros; red; intros. generalize TE; simpl.
  destruct rret. intro EQ.
  assert (TRG: target_reg_ok s map a r).
  inversion RRG. apply target_reg_other; auto.
  generalize (H0 _ _ _ _ _ _ _ MWF EQ ME TRG).
  intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
  simpl in OUT. subst nd. exists rs1. tauto.

  monadSimpl.
Qed.

(** The correctness of the translation then follows by application
  of the mutual induction principle for Cminor evaluation derivations
  to the lemmas above. *)

Scheme eval_expr_ind_5 := Minimality for eval_expr Sort Prop
  with eval_condexpr_ind_5 := Minimality for eval_condexpr Sort Prop
  with eval_exprlist_ind_5 := Minimality for eval_exprlist Sort Prop
  with eval_funcall_ind_5 := Minimality for eval_funcall Sort Prop
  with exec_stmt_ind_5 := Minimality for exec_stmt Sort Prop.

Theorem transl_function_correctness:
  forall m f vargs t m' vres,
  eval_funcall ge m f vargs t m' vres ->
  transl_function_correct m f vargs t m' vres.
Proof
  (eval_funcall_ind_5 ge
    transl_expr_correct
    transl_condition_correct
    transl_exprlist_correct
    transl_function_correct
    transl_stmt_correct

    transl_expr_Evar_correct
    transl_expr_Eop_correct
    transl_expr_Eload_correct
    transl_expr_Estore_correct
    transl_expr_Ecall_correct
    transl_expr_Econdition_correct
    transl_expr_Elet_correct
    transl_expr_Eletvar_correct
    transl_expr_Ealloc_correct
    transl_condition_CEtrue_correct
    transl_condition_CEfalse_correct
    transl_condition_CEcond_correct
    transl_condition_CEcondition_correct
    transl_exprlist_Enil_correct
    transl_exprlist_Econs_correct
    transl_funcall_internal_correct
    transl_funcall_external_correct
    transl_stmt_Sskip_correct
    transl_stmt_Sexpr_correct
    transl_stmt_Sassign_correct
    transl_stmt_Sifthenelse_correct
    transl_stmt_Sseq_continue_correct
    transl_stmt_Sseq_stop_correct
    transl_stmt_Sloop_loop_correct
    transl_stmt_Sloop_stop_correct
    transl_stmt_Sblock_correct
    transl_stmt_Sexit_correct
    transl_stmt_Sswitch_correct
    transl_stmt_Sreturn_none_correct
    transl_stmt_Sreturn_some_correct).

Theorem transl_program_correct:
  forall (t: trace) (r: val),
  Cminor.exec_program prog t r ->
  RTL.exec_program tprog t r.
Proof.
  intros t r [b [f [m [SYMB [FUNC [SIG EVAL]]]]]].
  generalize (function_ptr_translated _ _ FUNC).
  intros [tf [TFIND TRANSLF]].
  red; exists b; exists tf; exists m.
  split. rewrite symbols_preserved. 
  replace (prog_main tprog) with (prog_main prog).
  assumption. 
  symmetry; apply transform_partial_program_main with transl_fundef.
  exact TRANSL.
  split. exact TFIND.
  split. generalize (sig_transl_function _ _ TRANSLF). congruence.
  unfold fundef; rewrite (Genv.init_mem_transf_partial transl_fundef prog TRANSL).
  exact (transl_function_correctness _ _ _ _ _ _ EVAL _ TRANSLF).
Qed.

End CORRECTNESS.