Initial import of compcert

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 1302 insertions, 0 deletions

diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
new file mode 100644
index 00000000..98462d28
--- /dev/null
+++ b/backend/RTLgenproof.v
@@ -0,0 +1,1302 @@
+(** 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 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_function.
+  exact TRANSL.
+Qed.
+
+Lemma function_ptr_translated:
+  forall (b: block) (f: Cminor.function),
+  Genv.find_funct_ptr ge b = Some f ->
+  exists tf,
+  Genv.find_funct_ptr tge b = Some tf /\ transl_function f = Some tf.
+Proof.
+  intros. 
+  generalize 
+   (Genv.find_funct_ptr_transf_partial transl_function TRANSL H).
+  case (transl_function f).
+  intros tf [A B]. exists tf. tauto.
+  intros [A B]. elim B. reflexivity.
+Qed.
+
+Lemma functions_translated:
+  forall (v: val) (f: Cminor.function),
+  Genv.find_funct ge v = Some f ->
+  exists tf,
+  Genv.find_funct tge v = Some tf /\ transl_function f = Some tf.
+Proof.
+  intros. 
+  generalize 
+   (Genv.find_funct_transf_partial transl_function TRANSL H).
+  case (transl_function f).
+  intros tf [A B]. exists tf. tauto.
+  intros [A B]. elim B. 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  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)
+                         (e': env) (m': mem) (v: val) : Prop :=
+  forall map mut rd nd s ns s' rs
+    (MWF: map_wf map s)
+    (TE: transl_expr map mut a rd nd s = OK ns s')
+    (ME: match_env map e le rs)
+    (MUT: incl (mutated_expr a) mut)
+    (TRG: target_reg_ok s map mut a rd),
+  exists rs',
+     exec_instrs tge s'.(st_code) sp ns rs m nd rs' m'
+  /\ match_env map e' le rs'
+  /\ rs'#rd = v
+  /\ (forall r,
+       reg_valid r s -> ~(mutated_reg map mut r) ->
+       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)
+                         (e': env) (m': mem) (vl: list val) : Prop :=
+  forall map mut rl nd s ns s' rs
+    (MWF: map_wf map s)
+    (TE: transl_exprlist map mut al rl nd s = OK ns s')
+    (ME: match_env map e le rs)
+    (MUT: incl (mutated_exprlist al) mut)
+    (TRG: target_regs_ok s map mut al rl),
+  exists rs',
+     exec_instrs tge s'.(st_code) sp ns rs m nd rs' m'
+  /\ match_env map e' le rs'
+  /\ rs'##rl = vl
+  /\ (forall r,
+       reg_valid r s -> ~(mutated_reg map mut r) ->
+       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)
+                         (e': env) (m': mem) (vb: bool) : Prop :=
+  forall map mut ntrue nfalse s ns s' rs
+    (MWF: map_wf map s)
+    (TE: transl_condition map mut a ntrue nfalse s = OK ns s')
+    (ME: match_env map e le rs)
+    (MUT: incl (mutated_condexpr a) mut),
+  exists rs',
+     exec_instrs tge s'.(st_code) sp ns rs m (if vb then ntrue else nfalse) rs' m'
+  /\ match_env map e' le rs'
+  /\ (forall r,
+        reg_valid r s -> ~(mutated_reg map mut r) ->
+        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 and
+  lists 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)
+            (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 nd rs' m'
+  /\ match_env map e' nil rs'
+  /\ match_return_outcome out rret rs'.
+
+Definition transl_stmtlist_correct 
+  (sp: val) (e: env) (m: mem) (al: stmtlist)
+            (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_stmtlist map al 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 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.function) (vargs: list val)
+    (m':mem) (vres: val) : Prop :=
+  forall tf
+    (TE: transl_function f = Some tf),
+  exec_function tge tf vargs m 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) e 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.
+  (* Optimized case rd = r *)
+  rewrite MV in H5; injection H5; 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. red; intro; subst r1. contradiction.
+(* Result value *)
+  split. rewrite RES1. eauto with rtlg.
+(* Other regs *)
+  intros. case (Reg.eq rd r0); intro.
+  subst r0. inversion TRG. 
+  rewrite MV in H8; injection H8; intro; subst r. apply RES1.
+  byContradiction. tauto. 
+  apply OTHER1; auto.
+
+  intro; monadSimpl.
+Qed.
+
+Lemma transl_expr_Eop_correct:
+  forall (sp: val) (le : letenv) (e : env) (m : mem) (op : operation)
+         (al : exprlist) (e1 : env) (m1 : mem) (vl : list val)
+         (v: val),
+  eval_exprlist ge sp le e m al e1 m1 vl ->
+  transl_exprlist_correct sp le e m al e1 m1 vl ->
+  eval_operation ge sp op vl = Some v ->
+  transl_expr_correct sp le e m (Eop op al) e1 m1 v.
+Proof.
+  intros until v. intros EEL TEL EOP. red; intros.
+  simpl in TE. monadInv TE. intro EQ1. 
+  simpl in MUT. 
+  assert (TRG': target_regs_ok s1 map mut al l); eauto with rtlg.
+  assert (MWF': map_wf map s1). eauto with rtlg.
+  generalize (TEL _ _ _ _ _ _ _ _ MWF' EQ1 ME MUT TRG').
+  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.function RTL.function ge tge). 
+  eexact EOP.
+  exact symbols_preserved.
+(* 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. assumption.
+  case (In_dec Reg.eq r l); intro.
+  left. elim (alloc_regs_fresh_or_in_map _ _ _ _ _ _ MWF EQ r i); intro.
+  assumption. byContradiction; eauto with rtlg.
+  right; assumption.
+  red; intro; subst r. 
+  elim H1; intro. inversion TRG. contradiction.
+  tauto.
+Qed.
+
+Lemma transl_expr_Eassign_correct:
+ forall (sp: val) (le : letenv) (e : env) (m : mem) 
+    (id : ident) (a : expr) (e1 : env) (m1 : mem) 
+    (v : val),
+  eval_expr ge sp le e m a e1 m1 v ->
+  transl_expr_correct sp le e m a e1 m1 v ->
+  transl_expr_correct sp le e m (Eassign id a) (PTree.set id v e1) m1 v.
+Proof.
+  intros; red; intros.
+  simpl in TE. monadInv TE. intro EQ1. 
+  simpl in MUT.
+  assert (MWF0: map_wf map s1). eauto with rtlg.
+  assert (MUTa: incl (mutated_expr a) mut). 
+  red. intros. apply MUT. simpl. tauto. 
+  assert (TRGa: target_reg_ok s1 map mut a rd).
+  inversion TRG. apply target_reg_other; eauto with rtlg.
+  generalize (H0 _ _ _ _ _ _ _ _ MWF0 EQ1 ME MUTa TRGa).
+  intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
+  generalize (add_move_correct _ _ sp _ _ _ _ rs1 m1 EQ0).
+  intros [rs2 [EX2 [RES2 OTHER2]]].
+  exists rs2.
+(* Exec *)
+  split. eapply exec_trans. eexact EX1.
+  apply exec_instrs_incr with s1. eauto with rtlg.
+  exact EX2. 
+(* Match-env *)
+  split. 
+  apply match_env_update_var with rs1 r s s0; auto.
+  congruence.
+(* Result *)
+  split. case (Reg.eq rd r); intro.
+  subst r. congruence.
+  rewrite OTHER2; auto.
+(* Other regs *)
+  intros. transitivity (rs1#r0). 
+  apply OTHER2. red; intro; subst r0. 
+  apply H2. red. exists id. split. apply MUT. red; tauto.
+  generalize EQ; unfold find_var. 
+  destruct ((map_vars map)!id); monadSimpl. congruence. 
+  apply OTHER1. eauto with rtlg. assumption. assumption.
+Qed.
+
+Lemma transl_expr_Eload_correct:
+ forall (sp: val) (le : letenv) (e : env) (m : mem)
+    (chunk : memory_chunk) (addr : addressing) 
+    (al : exprlist) (e1 : env) (m1 : mem) (v : val) 
+    (vl : list val) (a: val),
+  eval_exprlist ge sp le e m al e1 m1 vl ->
+  transl_exprlist_correct sp le e m al e1 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) e1 m1 v.
+Proof.
+  intros; red; intros. simpl in TE. monadInv TE. intro EQ1. clear TE.
+  simpl in MUT.
+  assert (MWF1: map_wf map s1). eauto with rtlg.
+  assert (TRG1: target_regs_ok s1 map mut al l). eauto with rtlg. 
+  generalize (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME MUT 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.
+(* 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. 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.
+  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) (e1 : env) (m1 : mem) 
+    (vl : list val) (e2 : env) (m2 m3 : mem) 
+    (v : val) (a: val),
+  eval_exprlist ge sp le e m al e1 m1 vl ->
+  transl_exprlist_correct sp le e m al e1 m1 vl ->
+  eval_expr ge sp le e1 m1 b e2 m2 v ->
+  transl_expr_correct sp le e1 m1 b e2 m2 v ->
+  eval_addressing ge sp addr vl = Some a -> 
+  Mem.storev chunk m2 a v = Some m3 ->
+  transl_expr_correct sp le e m (Estore chunk addr al b) e2 m3 v.
+Proof.
+  intros; red; intros. simpl in TE; monadInv TE. intro EQ2; clear TE.
+  simpl in MUT. 
+  assert (MWF2: map_wf map s2). 
+    apply map_wf_incr with s. 
+    apply state_incr_trans2 with s0 s1; eauto with rtlg.
+    assumption. 
+  assert (MUT2: incl (mutated_exprlist al) mut). eauto with coqlib.
+  assert (TRG2: target_regs_ok s2 map mut al l). 
+    apply target_regs_ok_incr with s0; eauto with rtlg.
+  generalize (H0 _ _ _ _ _ _ _ _ MWF2 EQ2 ME MUT2 TRG2).
+  intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
+  assert (MWF1: map_wf map s1). eauto with rtlg.
+  assert (MUT1: incl (mutated_expr b) mut). eauto with coqlib.
+  assert (TRG1: target_reg_ok s1 map mut b rd).
+    inversion TRG. apply target_reg_other; eauto with rtlg.
+  generalize (H2 _ _ _ _ _ _ _ _ MWF1 EQ1 ME1 MUT1 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 H5; rewrite RES1. 
+  rewrite (@eval_addressing_preserved _ _ ge tge).
+  eexact H3. exact symbols_preserved. 
+  rewrite RES2. assumption.
+(* 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. assumption.
+  apply OTHER1. apply reg_valid_incr with s.
+  apply state_incr_trans2 with s0 s1; eauto with rtlg. assumption.
+  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) 
+    (e1 e2 : env) (m1 m2 m3 : mem) (vf : val) 
+    (vargs : list val) (vres : val) (f : Cminor.function),
+  eval_expr ge sp le e m a e1 m1 vf ->
+  transl_expr_correct sp le e m a e1 m1 vf ->
+  eval_exprlist ge sp le e1 m1 bl e2 m2 vargs ->
+  transl_exprlist_correct sp le e1 m1 bl e2 m2 vargs ->
+  Genv.find_funct ge vf = Some f ->
+  Cminor.fn_sig f = sig ->
+  eval_funcall ge m2 f vargs m3 vres ->
+  transl_function_correct m2 f vargs m3 vres ->
+  transl_expr_correct sp le e m (Ecall sig a bl) e2 m3 vres.
+Proof.
+  intros. red; simpl; intros.
+  monadInv TE. intro EQ3. clear TE.
+  assert (MUTa: incl (mutated_expr a) mut). eauto with coqlib.
+  assert (MUTbl: incl (mutated_exprlist bl) mut). eauto with coqlib.
+  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 mut 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 MUTa TRGr).
+  intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
+  clear MUTa 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 mut bl l).
+    apply target_regs_ok_incr with s1; eauto with rtlg.
+  generalize (H2 _ _ _ _ _ _ _ _ MWFbl EQ2 ME1 MUTbl TRGl).
+  intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]].
+  clear MUTbl 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
+                     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.
+  apply target_reg_not_mutated with s0 a. 
+  eauto with rtlg. 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 TF. unfold transl_function.
+  destruct (transl_fun f init_state).
+  intro; discriminate. destruct p. intros. injection TF0. intro.
+  rewrite <- H7; simpl. auto.
+  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.
+  exact EX3.
+(* 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.
+    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.
+    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) (e1 : env) (m1 : mem) 
+    (v1 : bool) (e2 : env) (m2 : mem) (v2 : val),
+  eval_condexpr ge sp le e m a e1 m1 v1 ->
+  transl_condition_correct sp le e m a e1 m1 v1 ->
+  eval_expr ge sp le e1 m1 (if v1 then b else c) e2 m2 v2 ->
+  transl_expr_correct sp le e1 m1 (if v1 then b else c) e2 m2 v2 ->
+  transl_expr_correct sp le e m (Econdition a b c) e2 m2 v2.
+Proof.
+  intros; red; intros. simpl in TE; monadInv TE. intro EQ1; clear TE.
+  simpl in MUT. 
+
+  assert (MWF1: map_wf map s1).
+    apply map_wf_incr with s. eauto with rtlg. assumption.
+  assert (MUT1: incl (mutated_condexpr a) mut). eauto with coqlib.
+  generalize (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME MUT1).
+  intros [rs1 [EX1 [ME1 OTHER1]]].
+  destruct v1.
+
+  assert (MWF0: map_wf map s0). eauto with rtlg.
+  assert (MUT0: incl (mutated_expr b) mut). eauto with coqlib.
+  assert (TRG0: target_reg_ok s0 map mut b rd).
+    inversion TRG. apply target_reg_other; eauto with rtlg.
+  generalize (H2 _ _ _ _ _ _ _ _ MWF0 EQ0 ME1 MUT0 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.
+  exact EX2.
+(* 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 (MUTc: incl (mutated_expr c) mut). eauto with coqlib.
+  assert (TRGc: target_reg_ok s map mut c rd).
+    inversion TRG. apply target_reg_other; auto.
+  generalize (H2 _ _ _ _ _ _ _ _ MWF EQ ME1 MUTc 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.
+  exact EX2.
+(* 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) (e1 : env) (m1 : mem) (v1 : val) 
+    (e2 : env) (m2 : mem) (v2 : val),
+  eval_expr ge sp le e m a e1 m1 v1 ->
+  transl_expr_correct sp le e m a e1 m1 v1 ->
+  eval_expr ge sp (v1 :: le) e1 m1 b e2 m2 v2 ->
+  transl_expr_correct sp (v1 :: le) e1 m1 b e2 m2 v2 ->
+  transl_expr_correct sp le e m (Elet a b) e2 m2 v2.
+Proof.
+  intros; red; intros.
+  simpl in TE; monadInv TE. intro EQ1.
+  simpl in MUT.
+  assert (MWF1: map_wf map s1). eauto with rtlg.
+  assert (MUT1: incl (mutated_expr a) mut). eauto with coqlib.
+  assert (TRG1: target_reg_ok s1 map mut a r).
+  eapply target_reg_other; eauto with rtlg.
+  generalize (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME MUT1 TRG1).
+  intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
+  assert (MWF2: map_wf (add_letvar map r) s0). 
+  apply add_letvar_wf; eauto with rtlg. 
+  assert (MUT2: incl (mutated_expr b) mut). eauto with coqlib.
+  assert (ME2: match_env (add_letvar map r) e1 (v1 :: le) rs1).
+  apply match_env_letvar; assumption.
+  assert (TRG2: target_reg_ok s0 (add_letvar map r) mut b rd).
+  inversion TRG. apply target_reg_other. 
+  unfold reg_in_map, add_letvar; simpl. red; intro.
+  elim H10; intro. apply H3. left. assumption.
+  elim H11; intro. apply valid_fresh_absurd with rd s.
+  assumption. rewrite <- H12. eauto with rtlg.
+  apply H3. right. assumption.
+  eauto with rtlg.
+  generalize (H2 _ _ _ _ _ _ _ _ MWF2 EQ0 ME2 MUT2 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. exact EX2.
+(* 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. 
+  unfold mutated_reg. unfold add_letvar; simpl. assumption.
+  elim H5; intro. left. 
+  unfold reg_in_map, add_letvar; simpl.
+  unfold reg_in_map in H6; tauto.
+  tauto.
+  apply OTHER1. eauto with rtlg.
+  assumption. 
+  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) e 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_condition_CEtrue_correct:
+  forall (sp: val) (le : letenv) (e : env) (m : mem),
+  transl_condition_correct sp le e m CEtrue e 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 e 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) (e1 : env) 
+    (m1 : mem) (vl : list val) (b : bool),
+  eval_exprlist ge sp le e m al e1 m1 vl ->
+  transl_exprlist_correct sp le e m al e1 m1 vl ->
+  eval_condition cond vl =  Some b ->
+  transl_condition_correct sp le e m (CEcond cond al) e1 m1 b.
+Proof.
+  intros; red; intros. simpl in TE; monadInv TE. intro EQ1; clear TE.
+  assert (MWF1: map_wf map s1). eauto with rtlg.
+  simpl in MUT.
+  assert (TRG: target_regs_ok s1 map mut al l).
+    eauto with rtlg.
+  generalize (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME MUT 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.
+(* Match-env *)
+  split. assumption.
+(* Regs *)
+  intros. apply OTHER1. 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_condition_CEcondition_correct:
+  forall (sp: val) (le : letenv) (e : env) (m : mem)
+    (a b c : condexpr) (e1 : env) (m1 : mem) 
+    (vb1 : bool) (e2 : env) (m2 : mem) (vb2 : bool),
+  eval_condexpr ge sp le e m a e1 m1 vb1 ->
+  transl_condition_correct sp le e m a e1 m1 vb1 ->
+  eval_condexpr ge sp le e1 m1 (if vb1 then b else c) e2 m2 vb2 ->
+  transl_condition_correct sp le e1 m1 (if vb1 then b else c) e2 m2 vb2 ->
+  transl_condition_correct sp le e m (CEcondition a b c) e2 m2 vb2.
+Proof.
+  intros; red; intros. simpl in TE; monadInv TE. intro EQ1; clear TE.
+  simpl in MUT.
+  assert (MWF1: map_wf map s1). eauto with rtlg.
+  assert (MUTa: incl (mutated_condexpr a) mut). eauto with coqlib.
+  generalize (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME MUTa).
+  intros [rs1 [EX1 [ME1 OTHER1]]].
+  destruct vb1.
+
+  assert (MWF0: map_wf map s0). eauto with rtlg.
+  assert (MUTb: incl (mutated_condexpr b) mut). eauto with coqlib.
+  generalize (H2 _ _ _ _ _ _ _ _ MWF0 EQ0 ME1 MUTb).
+  intros [rs2 [EX2 [ME2 OTHER2]]].
+  exists rs2.
+  split. eapply exec_trans. eexact EX1. 
+  apply exec_instrs_incr with s1. eauto with rtlg.
+  exact EX2.
+  split. assumption. 
+  intros. transitivity (rs1#r). 
+  apply OTHER2; eauto with rtlg.
+  apply OTHER1; eauto with rtlg.
+
+  assert (MUTc: incl (mutated_condexpr c) mut). eauto with coqlib.
+  generalize (H2 _ _ _ _ _ _ _ _ MWF EQ ME1 MUTc).
+  intros [rs2 [EX2 [ME2 OTHER2]]].
+  exists rs2.
+  split. eapply exec_trans. eexact EX1. 
+  apply exec_instrs_incr with s0. eauto with rtlg.
+  exact EX2.
+  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 e 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) (e1 : env) (m1 : mem) 
+    (v : val) (e2 : env) (m2 : mem) (vl : list val),
+  eval_expr ge sp le e m a e1 m1 v ->
+  transl_expr_correct sp le e m a e1 m1 v ->
+  eval_exprlist ge sp le e1 m1 bl e2 m2 vl ->
+  transl_exprlist_correct sp le e1 m1 bl e2 m2 vl ->
+  transl_exprlist_correct sp le e m (Econs a bl) e2 m2 (v :: vl).
+Proof.
+  intros. red. intros. 
+  inversion TRG.
+  rewrite <- H10 in TE. simpl in TE. monadInv TE. intro EQ1.
+  simpl in MUT.
+  assert (MUT1: incl (mutated_expr a) mut); eauto with coqlib.
+  assert (MUT2: incl (mutated_exprlist bl) mut); eauto with coqlib.
+  assert (MWF1: map_wf map s1); eauto with rtlg.
+  assert (TRG1: target_reg_ok s1 map mut a r); eauto with rtlg.
+  generalize (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME MUT1 TRG1).
+  intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
+  generalize (H2 _ _ _ _ _ _ _ _ MWF EQ ME1 MUT2 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. assumption.
+(* Match-env *)
+  split. assumption.
+(* Results *)
+  split. simpl. rewrite RES2. rewrite OTHER2. rewrite RES1.
+  reflexivity.
+  eauto with rtlg. 
+  eauto with rtlg.
+  assumption.
+(* Other regs *)
+  simpl. intros.
+  transitivity (rs1#r0).
+  apply OTHER2; auto. tauto. 
+  apply OTHER1; auto. eauto with rtlg. 
+  elim H14; intro. left; assumption. right; apply sym_not_equal; tauto.
+Qed.
+
+Lemma transl_funcall_correct:
+  forall (m : mem) (f : Cminor.function) (vargs : list val) 
+    (m1 : mem) (sp : block) (e e2 : env) (m2 : mem) 
+    (out : outcome) (vres : val),
+  Mem.alloc m 0 (fn_stackspace f) = (m1, sp) ->
+  set_locals (Cminor.fn_vars f) (set_params vargs (Cminor.fn_params f)) = e ->
+  exec_stmtlist ge (Vptr sp Int.zero) e m1 (fn_body f) e2 m2 out ->
+  transl_stmtlist_correct (Vptr sp Int.zero) e m1 (fn_body f) e2 m2 out ->
+  outcome_result_value out f.(Cminor.fn_sig).(sig_res) vres ->
+  transl_function_correct m f vargs (Mem.free m2 sp) vres.
+Proof.
+  intros; red; intros.
+  generalize TE. unfold transl_function.
+  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.
+
+  assert (RRG: return_reg_ok s3 y0 (ret_reg (Cminor.fn_sig f) r)).
+  apply return_reg_ok_incr with s2. eauto with rtlg. 
+  apply new_reg_return_ok with s1; assumption.
+
+  generalize (H2 _ _ _ _ _ _ _ _ _ rs MWF EQ3 ME OUT RRG).
+  intros [rs1 [EX1 [ME1 MR1]]].
+
+  apply exec_funct with m1 n rs1 (ret_reg (Cminor.fn_sig f) r).
+  rewrite <- TF; simpl; assumption.
+  rewrite <- TF; simpl. exact EX1.
+  rewrite <- TF; simpl. 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 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_stmt_Sexpr_correct:
+  forall (sp: val) (e : env) (m : mem) (a : expr) 
+    (e1 : env) (m1 : mem) (v : val),
+  eval_expr ge sp nil e m a e1 m1 v ->
+  transl_expr_correct sp nil e m a e1 m1 v ->
+  transl_stmt_correct sp e m (Sexpr a) e1 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 (mutated_expr a) a r). eauto with rtlg.
+  generalize (H0 _ _ _ _ _ _ _ _ MWF0 EQ1 ME (incl_refl (mutated_expr a)) TRG).
+  intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
+  exists rs1; simpl; tauto.
+Qed.
+
+Lemma transl_stmt_Sifthenelse_correct:
+  forall (sp: val) (e : env) (m : mem) (a : condexpr)
+    (sl1 sl2 : stmtlist) (e1 : env) (m1 : mem) 
+    (v1 : bool) (e2 : env) (m2 : mem) (out : outcome),
+  eval_condexpr ge sp nil e m a e1 m1 v1 ->
+  transl_condition_correct sp nil e m a e1 m1 v1 ->
+  exec_stmtlist ge sp e1 m1 (if v1 then sl1 else sl2) e2 m2 out ->
+  transl_stmtlist_correct sp e1 m1 (if v1 then sl1 else sl2) e2 m2 out ->
+  transl_stmt_correct sp e m (Sifthenelse a sl1 sl2) e2 m2 out.
+Proof.
+  intros; red; intros until rs; intro MWF.
+  simpl. case (more_likely a sl1 sl2); monadSimpl; intro EQ2; intros.
+  assert (MWF1: map_wf map s1). eauto with rtlg.
+  generalize (H0 _ _ _ _ _ _ _ rs MWF1 EQ2 ME (incl_refl _)).
+  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 s1.
+  eauto with rtlg. exact EX2.
+  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. exact EX2.
+  tauto.
+
+  assert (MWF1: map_wf map s1). eauto with rtlg.
+  generalize (H0 _ _ _ _ _ _ _ rs MWF1 EQ2 ME (incl_refl _)).
+  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. exact EX2.
+  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 s1.
+  eauto with rtlg. exact EX2.
+  tauto.
+Qed.
+
+Lemma transl_stmt_Sloop_loop_correct:
+  forall (sp: val) (e : env) (m : mem) (sl : stmtlist) 
+    (e1 : env) (m1 : mem) (e2 : env) (m2 : mem) 
+    (out : outcome),
+  exec_stmtlist ge sp e m sl e1 m1 Out_normal ->
+  transl_stmtlist_correct sp e m sl e1 m1 Out_normal ->
+  exec_stmt ge sp e1 m1 (Sloop sl) e2 m2 out ->
+  transl_stmt_correct sp e1 m1 (Sloop sl) e2 m2 out ->
+  transl_stmt_correct sp e m (Sloop sl) 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 ns rs1 m1.
+  apply exec_one. apply exec_Inop. 
+  generalize EQ1. unfold update_instr. 
+  case (plt n (st_nextnode s1)); intro; monadSimpl.
+  rewrite <- H4. simpl. apply PTree.gss.
+  exact EX2.
+  tauto.
+Qed.
+
+Lemma transl_stmt_Sloop_stop_correct:
+  forall (sp: val) (e : env) (m : mem) (sl : stmtlist) 
+    (e1 : env) (m1 : mem) (out : outcome),
+  exec_stmtlist ge sp e m sl e1 m1 out ->
+  transl_stmtlist_correct sp e m sl e1 m1 out ->
+  out <> Out_normal ->
+  transl_stmt_correct sp e m (Sloop sl) 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 : stmtlist) 
+    (e1 : env) (m1 : mem) (out : outcome),
+  exec_stmtlist ge sp e m sl e1 m1 out ->
+  transl_stmtlist_correct sp e m sl e1 m1 out ->
+  transl_stmt_correct sp e m (Sblock sl) 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_stmt_Sexit_correct:
+  forall (sp: val) (e : env) (m : mem) (n : nat),
+  transl_stmt_correct sp e m (Sexit n) e m (Out_exit n).
+Proof.
+  intros; red; intros. 
+  generalize TE. simpl. caseEq (nth_error nexits n).
+  intros n' NE. monadSimpl. subst n'.
+  simpl in OUT. assert (ns = nd). congruence. subst ns.
+  exists rs. intuition. apply exec_refl.
+  intro. monadSimpl.
+Qed.
+
+Lemma transl_stmt_Sreturn_none_correct:
+  forall (sp: val) (e : env) (m : mem),
+  transl_stmt_correct sp e m (Sreturn None) 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) 
+    (e1 : env) (m1 : mem) (v : val),
+  eval_expr ge sp nil e m a e1 m1 v ->
+  transl_expr_correct sp nil e m a e1 m1 v ->
+  transl_stmt_correct sp e m (Sreturn (Some a)) e1 m1 (Out_return (Some v)).
+Proof.
+  intros; red; intros. generalize TE; simpl.
+  destruct rret. intro EQ.
+  assert (TRG: target_reg_ok s map (mutated_expr a) a r).
+  inversion RRG. apply target_reg_other; auto.
+  generalize (H0 _ _ _ _ _ _ _ _ MWF EQ ME (incl_refl _) TRG).
+  intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
+  simpl in OUT. subst nd. exists rs1. tauto.
+
+  monadSimpl.
+Qed.
+  
+Lemma transl_stmtlist_Snil_correct:
+  forall (sp: val) (e : env) (m : mem),
+  transl_stmtlist_correct sp e m Snil 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_stmtlist_Scons_continue_correct:
+  forall (sp: val) (e : env) (m : mem) (s : stmt) 
+    (sl : stmtlist) (e1 : env) (m1 : mem) (e2 : env) 
+    (m2 : mem) (out : outcome),
+  exec_stmt ge sp e m s e1 m1 Out_normal ->
+  transl_stmt_correct sp e m s e1 m1 Out_normal ->
+  exec_stmtlist ge sp e1 m1 sl e2 m2 out ->
+  transl_stmtlist_correct sp e1 m1 sl e2 m2 out ->
+  transl_stmtlist_correct sp e m (Scons s sl) e2 m2 out.
+Proof.
+  intros; red; intros. simpl in TE; monadInv TE. intro EQ0.
+  assert (MWF1: map_wf map s1). eauto with rtlg.
+  assert (OUTs: outcome_node Out_normal n nexits nret n).
+    simpl. auto.
+  assert (RRG1: return_reg_ok s1 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 s1. eauto with rtlg.
+  exact EX2.
+(* Match-env + return *)
+  tauto.
+Qed.
+
+Lemma transl_stmtlist_Scons_stop_correct:
+  forall (sp: val) (e : env) (m : mem) (s : stmt) 
+    (sl : stmtlist) (e1 : env) (m1 : mem) (out : outcome),
+  exec_stmt ge sp e m s e1 m1 out ->
+  transl_stmt_correct sp e m s e1 m1 out ->
+  out <> Out_normal ->
+  transl_stmtlist_correct sp e m (Scons s sl) e1 m1 out.
+Proof.
+  intros; red; intros. 
+  simpl in TE; monadInv TE. intro EQ0; clear TE.
+  assert (MWF1: map_wf map s1). eauto with rtlg.
+  assert (OUTs: outcome_node out n nexits nret nd).
+    destruct out; simpl; auto. tauto. 
+  assert (RRG1: return_reg_ok s1 map rret). eauto with rtlg.
+  exact (H0 _ _ _ _ _ _ _ _ _ _ MWF1 EQ0 ME OUTs RRG1).
+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_6 := Minimality for eval_expr Sort Prop
+  with eval_condexpr_ind_6 := Minimality for eval_condexpr Sort Prop
+  with eval_exprlist_ind_6 := Minimality for eval_exprlist Sort Prop
+  with eval_funcall_ind_6 := Minimality for eval_funcall Sort Prop
+  with exec_stmt_ind_6 := Minimality for exec_stmt Sort Prop
+  with exec_stmtlist_ind_6 := Minimality for exec_stmtlist Sort Prop.
+
+Theorem transl_function_correctness:
+  forall m f vargs m' vres,
+  eval_funcall ge m f vargs m' vres ->
+  transl_function_correct m f vargs m' vres.
+Proof
+  (eval_funcall_ind_6 ge
+    transl_expr_correct
+    transl_condition_correct
+    transl_exprlist_correct
+    transl_function_correct
+    transl_stmt_correct
+    transl_stmtlist_correct
+
+    transl_expr_Evar_correct
+    transl_expr_Eassign_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_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_correct
+    transl_stmt_Sexpr_correct
+    transl_stmt_Sifthenelse_correct
+    transl_stmt_Sloop_loop_correct
+    transl_stmt_Sloop_stop_correct
+    transl_stmt_Sblock_correct
+    transl_stmt_Sexit_correct
+    transl_stmt_Sreturn_none_correct
+    transl_stmt_Sreturn_some_correct
+    transl_stmtlist_Snil_correct
+    transl_stmtlist_Scons_continue_correct
+    transl_stmtlist_Scons_stop_correct).
+
+Theorem transl_program_correct:
+  forall (r: val),
+  Cminor.exec_program prog r ->
+  RTL.exec_program tprog r.
+Proof.
+  intros 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_function.
+  exact TRANSL.
+  split. exact TFIND.
+  split. generalize TRANSLF. unfold transl_function.
+  destruct (transl_fun f init_state).
+  intro; discriminate. destruct p; intro EQ; injection EQ; intro EQ1.
+  rewrite <- EQ1. simpl. congruence. 
+  rewrite (Genv.init_mem_transf_partial transl_function prog TRANSL).
+  exact (transl_function_correctness _ _ _ _ _ EVAL _ TRANSLF).
+Qed.
+
+End CORRECTNESS.