Merge of branch "unsigned-offsets":

- In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int.
  (Fixes issue with wrong comparison of pointers across 0x8000_0000)
- Revised Stacking pass to not use negative SP offsets.
- Add pointer validity checks to Cminor ... Mach
  to support the use of memory injections in Stacking.
- Cleaned up Stacklayout modules.
- IA32: improved code generation for Mgetparam.
- ARM: improved code generation for op-immediate instructions.


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

29 files changed, 2115 insertions, 1359 deletions

diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index daa53e5..e7d9995 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -618,7 +618,7 @@ Proof.
   unfold ls1. simpl. apply Locmap.guo. eapply regalloc_not_temporary; eauto. 
   (* Not a move *)
   intros INMO CORR CODE.
-  assert (eval_operation tge sp op (map ls (map assign args)) = Some v).
+  assert (eval_operation tge sp op (map ls (map assign args)) m = Some v).
     replace (map ls (map assign args)) with (rs##args).
     rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. 
     eapply agree_eval_regs; eauto.
@@ -706,7 +706,7 @@ Proof.
   eapply agree_reg_list_live; eauto.
 
   (* Icond, true *)
-  assert (COND: eval_condition cond (map ls (map assign args)) = Some true).
+  assert (COND: eval_condition cond (map ls (map assign args)) m = Some true).
     replace (map ls (map assign args)) with (rs##args). auto.
     eapply agree_eval_regs; eauto.
   econstructor; split.
@@ -715,7 +715,7 @@ Proof.
   eapply agree_undef_temps; eauto.
   eapply agree_reg_list_live. eauto.
   (* Icond, false *)
-  assert (COND: eval_condition cond (map ls (map assign args)) = Some false).
+  assert (COND: eval_condition cond (map ls (map assign args)) m = Some false).
     replace (map ls (map assign args)) with (rs##args). auto.
     eapply agree_eval_regs; eauto.
   econstructor; split.
diff --git a/backend/Bounds.v b/backend/Bounds.v
index 514895b..0415670 100644
--- a/backend/Bounds.v
+++ b/backend/Bounds.v
@@ -10,7 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Computation of resource bounds forr Linear code. *)
+(** Computation of resource bounds for Linear code. *)
 
 Require Import Coqlib.
 Require Import Maps.
@@ -36,11 +36,13 @@ Record bounds : Type := mkbounds {
   bound_int_callee_save: Z;
   bound_float_callee_save: Z;
   bound_outgoing: Z;
+  bound_stack_data: Z;
   bound_int_local_pos: bound_int_local >= 0;
   bound_float_local_pos: bound_float_local >= 0;
   bound_int_callee_save_pos: bound_int_callee_save >= 0;
   bound_float_callee_save_pos: bound_float_callee_save >= 0;
-  bound_outgoing_pos: bound_outgoing >= 0
+  bound_outgoing_pos: bound_outgoing >= 0;
+  bound_stack_data_pos: bound_stack_data >= 0
 }.
 
 (** The following predicates define the correctness of a set of bounds
@@ -186,15 +188,19 @@ Program Definition function_bounds :=
     (max_over_regs_of_funct float_callee_save)
     (Zmax (max_over_instrs outgoing_space)
           (max_over_slots_of_funct outgoing_slot))
+    (Zmax f.(fn_stacksize) 0)
     (max_over_slots_of_funct_pos int_local)
     (max_over_slots_of_funct_pos float_local)
     (max_over_regs_of_funct_pos int_callee_save)
     (max_over_regs_of_funct_pos float_callee_save)
-    _.
+    _ _.
 Next Obligation.
   apply Zle_ge. eapply Zle_trans. 2: apply Zmax2.
   apply Zge_le. apply max_over_slots_of_funct_pos.  
 Qed.
+Next Obligation.
+  apply Zle_ge. apply Zmax2.
+Qed.
 
 (** We now show the correctness of the inferred bounds. *)
 
diff --git a/backend/CSE.v b/backend/CSE.v
index 45b50d6..44ed590 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -188,15 +188,19 @@ Definition add_unknown (n: numbering) (rd: reg) :=
               n.(num_eqs)
               (PTree.set rd n.(num_next) n.(num_reg)).
 
-(** [kill_load n] removes all equations involving memory loads.
+(** [kill_load n] removes all equations involving memory loads,
+  as well as those involving memory-dependent operators.
   It is used to reflect the effect of a memory store, which can
   potentially invalidate all such equations. *)
 
 Fixpoint kill_load_eqs (eqs: list (valnum * rhs)) : list (valnum * rhs) :=
   match eqs with
   | nil => nil
-  | (_, Load _ _ _) :: rem => kill_load_eqs rem
-  | v_rh :: rem => v_rh :: kill_load_eqs rem
+  | eq :: rem =>
+      match eq with
+      | (_, Op op _)  => if op_depends_on_memory op then kill_load_eqs rem else eq :: kill_load_eqs rem
+      | (_, Load _ _ _) => kill_load_eqs rem
+      end
   end.
 
 Definition kill_loads (n: numbering) : numbering :=
@@ -252,7 +256,7 @@ Definition equation_holds
      (vres: valnum) (rh: rhs) : Prop :=
   match rh with
   | Op op vl =>
-      eval_operation ge sp op (List.map valuation vl) =
+      eval_operation ge sp op (List.map valuation vl) m =
       Some (valuation vres)
   | Load chunk addr vl =>
       exists a,
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index 275b9fd..53576ad 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -208,9 +208,10 @@ Lemma kill_load_eqs_incl:
 Proof.
   induction eqs; simpl; intros.
   apply incl_refl.
-  destruct a. destruct r. apply incl_same_head; auto.
-  auto.
-  apply incl_tl. auto.
+  destruct a. destruct r. 
+  destruct (op_depends_on_memory o). auto with coqlib. 
+  apply incl_same_head; auto.
+  auto with coqlib.
 Qed.
 
 Lemma wf_kill_loads:
@@ -400,7 +401,7 @@ Definition rhs_evals_to
     (valu: valnum -> val) (rh: rhs) (v: val) : Prop :=
   match rh with
   | Op op vl => 
-      eval_operation ge sp op (List.map valu vl) = Some v
+      eval_operation ge sp op (List.map valu vl) m = Some v
   | Load chunk addr vl =>
       exists a,
       eval_addressing ge sp addr (List.map valu vl) = Some a /\
@@ -481,7 +482,7 @@ Lemma add_op_satisfiable:
   forall n rs op args dst v,
   wf_numbering n ->
   numbering_satisfiable ge sp rs m n ->
-  eval_operation ge sp op rs##args = Some v ->
+  eval_operation ge sp op rs##args m = Some v ->
   numbering_satisfiable ge sp (rs#dst <- v) m (add_op n dst op args).
 Proof.
   intros. inversion H0.
@@ -547,36 +548,22 @@ Proof.
   eauto.
 Qed.
 
-(** Allocation of a fresh memory block preserves satisfiability. *)
-
-Lemma alloc_satisfiable:
-  forall lo hi b m' rs n,
-  Mem.alloc m lo hi = (m', b) ->
-  numbering_satisfiable ge sp rs m n ->
-  numbering_satisfiable ge sp rs m' n.
-Proof.
-  intros. destruct H0 as [valu [A B]].
-  exists valu; split; intros.
-  generalize (A _ _ H0). destruct rh; simpl.
-  auto.
-  intros [addr [C D]]. exists addr; split. auto.
-  destruct addr; simpl in *; try discriminate. 
-  eapply Mem.load_alloc_other; eauto. 
-  eauto.
-Qed.
-
 (** [kill_load] preserves satisfiability.  Moreover, the resulting numbering
   is satisfiable in any concrete memory state. *)
 
 Lemma kill_load_eqs_ops:
   forall v rhs eqs,
   In (v, rhs) (kill_load_eqs eqs) ->
-  match rhs with Op _ _ => True | Load _ _ _ => False end.
+  match rhs with
+  | Op op _ => op_depends_on_memory op = false
+  | Load _ _ _ => False
+  end.
 Proof.
   induction eqs; simpl; intros.
   elim H.
-  destruct a. destruct r. 
-  elim H; intros. inversion H0; subst v0; subst rhs. auto.
+  destruct a. destruct r. destruct (op_depends_on_memory o) as [] _eqn.
+  apply IHeqs; auto.
+  simpl in H; destruct H. inv H. auto. 
   apply IHeqs. auto. 
   apply IHeqs. auto.
 Qed.
@@ -590,7 +577,9 @@ Proof.
   exists x. split; intros.
   generalize (H _ _ (H1 _ H2)). 
   generalize (kill_load_eqs_ops _ _ _ H2).
-  destruct rh; simpl; tauto.
+  destruct rh; simpl.
+  intros. rewrite <- H4. apply op_depends_on_memory_correct; auto.
+  tauto.
   apply H0. auto. 
 Qed.
 
@@ -645,7 +634,7 @@ Lemma find_op_correct:
   wf_numbering n ->
   numbering_satisfiable ge sp rs m n ->
   find_op n op args = Some r ->
-  eval_operation ge sp op rs##args = Some rs#r.
+  eval_operation ge sp op rs##args m = Some rs#r.
 Proof.
   intros until r. intros WF [valu NH].
   unfold find_op. caseEq (valnum_regs n args). intros n' vl VR FIND.
@@ -834,14 +823,14 @@ Proof.
 
   (* Iop *)
   exists (State s' (transf_function f) sp pc' (rs#res <- v) m); split.
-  assert (eval_operation tge sp op rs##args = Some v).
+  assert (eval_operation tge sp op rs##args m = Some v).
     rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved.
   generalize C; clear C.
   case (is_trivial_op op).
   intro. eapply exec_Iop'; eauto. 
   caseEq (find_op (analyze f)!!pc op args). intros r FIND CODE.
   eapply exec_Iop'; eauto. simpl. 
-  assert (eval_operation ge sp op rs##args = Some rs#r).
+  assert (eval_operation ge sp op rs##args m = Some rs#r).
     eapply find_op_correct; eauto.
     eapply wf_analyze; eauto.
   congruence.
diff --git a/backend/CastOptimproof.v b/backend/CastOptimproof.v
index b04e061..ab04d0e 100644
--- a/backend/CastOptimproof.v
+++ b/backend/CastOptimproof.v
@@ -168,9 +168,9 @@ Proof.
 Qed.
 
 Lemma approx_operation_correct:
-  forall app rs (ge: genv) sp op args v,
+  forall app rs (ge: genv) sp op args m v,
   regs_match_approx app rs ->
-  eval_operation ge sp op rs##args = Some v ->
+  eval_operation ge sp op rs##args m = Some v ->
   val_match_approx (approx_operation op (approx_regs app args)) v.
 Proof.
   intros. destruct op; simpl; try (exact I). 
@@ -324,10 +324,10 @@ Qed.
 (** Correctness of [transf_operation]. *)
 
 Lemma transf_operation_correct:
-  forall (ge: genv) app rs sp op args v,
+  forall (ge: genv) app rs sp op args m v,
   regs_match_approx app rs ->
-  eval_operation ge sp op rs##args = Some v ->
-  eval_operation ge sp (transf_operation op (approx_regs app args)) rs##args = Some v.
+  eval_operation ge sp op rs##args m = Some v ->
+  eval_operation ge sp (transf_operation op (approx_regs app args)) rs##args m = Some v.
 Proof.
   intros until v. intro RMA.
   assert (A: forall a r, Approx.bge a (approx_reg app r) = true -> val_match_approx a rs#r).
diff --git a/backend/Cminor.v b/backend/Cminor.v
index a3a166c..45e060d 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -254,7 +254,7 @@ Definition eval_compare_null (c: comparison) (n: int) : option val :=
   if Int.eq n Int.zero then eval_compare_mismatch c else None.
 
 Definition eval_binop
-            (op: binary_operation) (arg1 arg2: val): option val :=
+            (op: binary_operation) (arg1 arg2: val) (m: mem): option val :=
   match op, arg1, arg2 with
   | Oadd, Vint n1, Vint n2 => Some (Vint (Int.add n1 n2))
   | Oadd, Vint n1, Vptr b2 n2 => Some (Vptr b2 (Int.add n2 n1))
@@ -287,16 +287,19 @@ Definition eval_binop
   | Odivf, Vfloat f1, Vfloat f2 => Some (Vfloat (Float.div f1 f2))
   | Ocmp c, Vint n1, Vint n2 =>
       Some (Val.of_bool(Int.cmp c n1 n2))
-  | Ocmp c, Vptr b1 n1, Vptr b2 n2 =>
-      if eq_block b1 b2
-      then Some(Val.of_bool(Int.cmp c n1 n2))
-      else eval_compare_mismatch c
-  | Ocmp c, Vptr b1 n1, Vint n2 =>
-      eval_compare_null c n2
-  | Ocmp c, Vint n1, Vptr b2 n2 =>
-      eval_compare_null c n1
   | Ocmpu c, Vint n1, Vint n2 =>
       Some (Val.of_bool(Int.cmpu c n1 n2))
+  | Ocmpu c, Vptr b1 n1, Vptr b2 n2 =>
+      if Mem.valid_pointer m b1 (Int.unsigned n1)
+      && Mem.valid_pointer m b2 (Int.unsigned n2) then
+        if eq_block b1 b2
+        then Some(Val.of_bool(Int.cmpu c n1 n2))
+        else eval_compare_mismatch c
+      else None
+  | Ocmpu c, Vptr b1 n1, Vint n2 =>
+      eval_compare_null c n2
+  | Ocmpu c, Vint n1, Vptr b2 n2 =>
+      eval_compare_null c n1
   | Ocmpf c, Vfloat f1, Vfloat f2 =>
       Some (Val.of_bool (Float.cmp c f1 f2))
   | _, _, _ => None
@@ -330,7 +333,7 @@ Inductive eval_expr: expr -> val -> Prop :=
   | eval_Ebinop: forall op a1 a2 v1 v2 v,
       eval_expr a1 v1 ->
       eval_expr a2 v2 ->
-      eval_binop op v1 v2 = Some v ->
+      eval_binop op v1 v2 m = Some v ->
       eval_expr (Ebinop op a1 a2) v
   | eval_Eload: forall chunk addr vaddr v,
       eval_expr addr vaddr ->
diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index 29f7178..8a82c42 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -164,7 +164,7 @@ Inductive eval_expr: letenv -> expr -> val -> Prop :=
       eval_expr le (Evar id) v
   | eval_Eop: forall le op al vl v,
       eval_exprlist le al vl ->
-      eval_operation ge sp op vl = Some v ->
+      eval_operation ge sp op vl m = Some v ->
       eval_expr le (Eop op al) v
   | eval_Eload: forall le chunk addr al vl vaddr v,
       eval_exprlist le al vl ->
@@ -190,7 +190,7 @@ with eval_condexpr: letenv -> condexpr -> bool -> Prop :=
       eval_condexpr le CEfalse false
   | eval_CEcond: forall le cond al vl b,
       eval_exprlist le al vl ->
-      eval_condition cond vl = Some b ->
+      eval_condition cond vl m = Some b ->
       eval_condexpr le (CEcond cond al) b
   | eval_CEcondition: forall le a b c vb1 vb2,
       eval_condexpr le a vb1 ->
diff --git a/backend/Constprop.v b/backend/Constprop.v
index 47c40e3..39568a3 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -206,7 +206,7 @@ Definition transf_instr (app: D.t) (instr: instruction) :=
   | Ijumptable arg tbl =>
       match intval (approx_reg app) arg with
       | Some n =>
-          match list_nth_z tbl (Int.signed n) with
+          match list_nth_z tbl (Int.unsigned n) with
           | Some s => Inop s
           | None => instr
           end
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index 1dad518..d534c75 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -283,13 +283,13 @@ Proof.
   exists (State s' (transf_function f) sp pc' (rs#res <- v) m); split.
   TransfInstr. caseEq (op_strength_reduction (approx_reg (analyze f)!!pc) op args);
   intros op' args' OSR.
-  assert (eval_operation tge sp op' rs##args' = Some v).
+  assert (eval_operation tge sp op' rs##args' m = Some v).
     rewrite (eval_operation_preserved _ _ symbols_preserved). 
-    generalize (op_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs
+    generalize (op_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs m
                   MATCH op args v).
     rewrite OSR; simpl. auto.
   generalize (eval_static_operation_correct ge op sp
-               (approx_regs (analyze f)!!pc args) rs##args v
+               (approx_regs (analyze f)!!pc args) rs##args m v
                (approx_regs_val_list _ _ _ args MATCH) H0).
   case (eval_static_operation op (approx_regs (analyze f)!!pc args)); intros;
   simpl in H2;
@@ -370,14 +370,14 @@ Proof.
   exists (State s' (transf_function f) sp ifso rs m); split. 
   caseEq (cond_strength_reduction (approx_reg (analyze f)!!pc) cond args);
   intros cond' args' CSR.
-  assert (eval_condition cond' rs##args' = Some true).
+  assert (eval_condition cond' rs##args' m = Some true).
     generalize (cond_strength_reduction_correct
-                  ge (approx_reg (analyze f)!!pc) rs MATCH cond args).
+                  ge (approx_reg (analyze f)!!pc) rs m MATCH cond args).
     rewrite CSR.  intro. congruence.
   TransfInstr. rewrite CSR. 
   caseEq (eval_static_condition cond (approx_regs (analyze f)!!pc args)).
   intros b ESC. 
-  generalize (eval_static_condition_correct ge cond _ _ _
+  generalize (eval_static_condition_correct ge cond _ _ m _
                (approx_regs_val_list _ _ _ args MATCH) ESC); intro.
   replace b with true. intro; eapply exec_Inop; eauto. congruence.
   intros. eapply exec_Icond_true; eauto.
@@ -390,14 +390,14 @@ Proof.
   exists (State s' (transf_function f) sp ifnot rs m); split. 
   caseEq (cond_strength_reduction (approx_reg (analyze f)!!pc) cond args);
   intros cond' args' CSR.
-  assert (eval_condition cond' rs##args' = Some false).
+  assert (eval_condition cond' rs##args' m = Some false).
     generalize (cond_strength_reduction_correct
-                  ge (approx_reg (analyze f)!!pc) rs MATCH cond args).
+                  ge (approx_reg (analyze f)!!pc) rs m MATCH cond args).
     rewrite CSR.  intro. congruence.
   TransfInstr. rewrite CSR. 
   caseEq (eval_static_condition cond (approx_regs (analyze f)!!pc args)).
   intros b ESC. 
-  generalize (eval_static_condition_correct ge cond _ _ _
+  generalize (eval_static_condition_correct ge cond _ _ m _
                (approx_regs_val_list _ _ _ args MATCH) ESC); intro.
   replace b with false. intro; eapply exec_Inop; eauto. congruence.
   intros. eapply exec_Icond_false; eauto.
diff --git a/backend/Conventions.v b/backend/Conventions.v
index 9778f6a..c11bf47 100644
--- a/backend/Conventions.v
+++ b/backend/Conventions.v
@@ -191,6 +191,22 @@ Proof.
   intros; simpl. tauto.
 Qed.
 
+Lemma incoming_slot_in_parameters:
+  forall ofs ty sg,
+  In (S (Incoming ofs ty)) (loc_parameters sg) ->
+  In (S (Outgoing ofs ty)) (loc_arguments sg).
+Proof.
+  intros.
+  unfold loc_parameters in H. 
+  change (S (Incoming ofs ty)) with (parameter_of_argument (S (Outgoing ofs ty))) in H.
+  exploit list_in_map_inv. eexact H. intros [x [A B]]. simpl in A.
+  exploit loc_arguments_acceptable; eauto. unfold loc_argument_acceptable; intros.
+  destruct x; simpl in A; try discriminate.
+  destruct s; try contradiction. 
+  inv A. auto.
+Qed. 
+
+
 (** * Tail calls *)
 
 (** A tail-call is possible for a signature if the corresponding
diff --git a/backend/LTL.v b/backend/LTL.v
index a68352f..6e3effd 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -168,7 +168,7 @@ Inductive step: state -> trace -> state -> Prop :=
   | exec_Lop:
       forall s f sp pc rs m op args res pc' v,
       (fn_code f)!pc = Some(Lop op args res pc') ->
-      eval_operation ge sp op (map rs args) = Some v ->
+      eval_operation ge sp op (map rs args) m = Some v ->
       step (State s f sp pc rs m)
         E0 (State s f sp pc' (Locmap.set res v (undef_temps rs)) m)
   | exec_Lload:
@@ -210,20 +210,20 @@ Inductive step: state -> trace -> state -> Prop :=
   | exec_Lcond_true:
       forall s f sp pc rs m cond args ifso ifnot,
       (fn_code f)!pc = Some(Lcond cond args ifso ifnot) ->
-      eval_condition cond (map rs args) = Some true ->
+      eval_condition cond (map rs args) m = Some true ->
       step (State s f sp pc rs m)
         E0 (State s f sp ifso (undef_temps rs) m)
   | exec_Lcond_false:
       forall s f sp pc rs m cond args ifso ifnot,
       (fn_code f)!pc = Some(Lcond cond args ifso ifnot) ->
-      eval_condition cond (map rs args) = Some false ->
+      eval_condition cond (map rs args) m = Some false ->
       step (State s f sp pc rs m)
         E0 (State s f sp ifnot (undef_temps rs) m)
   | exec_Ljumptable:
       forall s f sp pc rs m arg tbl n pc',
       (fn_code f)!pc = Some(Ljumptable arg tbl) ->
       rs arg = Vint n ->
-      list_nth_z tbl (Int.signed n) = Some pc' ->
+      list_nth_z tbl (Int.unsigned n) = Some pc' ->
       step (State s f sp pc rs m)
         E0 (State s f sp pc' (undef_temps rs) m)
   | exec_Lreturn:
diff --git a/backend/LTLin.v b/backend/LTLin.v
index d6c5fa7..5f12390 100644
--- a/backend/LTLin.v
+++ b/backend/LTLin.v
@@ -158,7 +158,7 @@ Definition find_function (ros: loc + ident) (rs: locset) : option fundef :=
 Inductive step: state -> trace -> state -> Prop :=
   | exec_Lop:
       forall s f sp op args res b rs m v,
-      eval_operation ge sp op (map rs args) = Some v ->
+      eval_operation ge sp op (map rs args) m = Some v ->
       step (State s f sp (Lop op args res :: b) rs m)
         E0 (State s f sp b (Locmap.set res v (undef_temps rs)) m)
   | exec_Lload:
@@ -203,19 +203,19 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State s f sp b' rs m)
   | exec_Lcond_true:
       forall s f sp cond args lbl b rs m b',
-      eval_condition cond (map rs args) = Some true ->
+      eval_condition cond (map rs args) m = Some true ->
       find_label lbl f.(fn_code) = Some b' ->
       step (State s f sp (Lcond cond args lbl :: b) rs m)
         E0 (State s f sp b' (undef_temps rs) m)
   | exec_Lcond_false:
       forall s f sp cond args lbl b rs m,
-      eval_condition cond (map rs args) = Some false ->
+      eval_condition cond (map rs args) m = Some false ->
       step (State s f sp (Lcond cond args lbl :: b) rs m)
         E0 (State s f sp b (undef_temps rs) m)
   | exec_Ljumptable:
       forall s f sp arg tbl b rs m n lbl b',
       rs arg = Vint n ->
-      list_nth_z tbl (Int.signed n) = Some lbl ->
+      list_nth_z tbl (Int.unsigned n) = Some lbl ->
       find_label lbl f.(fn_code) = Some b' ->
       step (State s f sp (Ljumptable arg tbl :: b) rs m)
         E0 (State s f sp b' (undef_temps rs) m)
diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v
index ad3ad64..c928f3f 100644
--- a/backend/LTLintyping.v
+++ b/backend/LTLintyping.v
@@ -89,7 +89,7 @@ Inductive wt_instr : instruction -> Prop :=
       forall arg tbl,
       Loc.type arg = Tint ->
       loc_acceptable arg ->
-      list_length_z tbl * 4 <= Int.max_signed ->
+      list_length_z tbl * 4 <= Int.max_unsigned ->
       wt_instr (Ljumptable arg tbl)
   | wt_Lreturn: 
       forall optres,
diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v
index 7afae2d..791c755 100644
--- a/backend/LTLtyping.v
+++ b/backend/LTLtyping.v
@@ -109,7 +109,7 @@ Inductive wt_instr : instruction -> Prop :=
       Loc.type arg = Tint ->
       loc_acceptable arg ->
       (forall lbl, In lbl tbl -> valid_successor lbl) ->
-      list_length_z tbl * 4 <= Int.max_signed ->
+      list_length_z tbl * 4 <= Int.max_unsigned ->
       wt_instr (Ljumptable arg tbl)
   | wt_Lreturn: 
       forall optres,
diff --git a/backend/Linear.v b/backend/Linear.v
index 40f7e41..31c3fed 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -123,7 +123,8 @@ Definition reglist (rs: locset) (rl: list mreg) : list val :=
 
   [call_regs caller] returns the location set at function entry,
   as a function of the location set [caller] of the calling function.
-- Machine registers have the same values as in the caller.
+- Temporary registers are undefined.
+- Other machine registers have the same values as in the caller.
 - Incoming stack slots (used for parameter passing) have the same
   values as the corresponding outgoing stack slots (used for argument
   passing) in the caller.
@@ -133,7 +134,7 @@ Definition reglist (rs: locset) (rl: list mreg) : list val :=
 Definition call_regs (caller: locset) : locset :=
   fun (l: loc) =>
     match l with
-    | R r => caller (R r)
+    | R r => if In_dec Loc.eq (R r) temporaries then Vundef else caller (R r)
     | S (Local ofs ty) => Vundef
     | S (Incoming ofs ty) => caller (S (Outgoing ofs ty))
     | S (Outgoing ofs ty) => Vundef
@@ -262,7 +263,7 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State s f sp b (Locmap.set (S sl) (rs (R r)) rs) m)
   | exec_Lop:
       forall s f sp op args res b rs m v,
-      eval_operation ge sp op (reglist rs args) = Some v ->
+      eval_operation ge sp op (reglist rs args) m = Some v ->
       step (State s f sp (Lop op args res :: b) rs m)
         E0 (State s f sp b (Locmap.set (R res) v (undef_op op rs)) m)
   | exec_Lload:
@@ -306,19 +307,19 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State s f sp b' rs m)
   | exec_Lcond_true:
       forall s f sp cond args lbl b rs m b',
-      eval_condition cond (reglist rs args) = Some true ->
+      eval_condition cond (reglist rs args) m = Some true ->
       find_label lbl f.(fn_code) = Some b' ->
       step (State s f sp (Lcond cond args lbl :: b) rs m)
         E0 (State s f sp b' (undef_temps rs) m)
   | exec_Lcond_false:
       forall s f sp cond args lbl b rs m,
-      eval_condition cond (reglist rs args) = Some false ->
+      eval_condition cond (reglist rs args) m = Some false ->
       step (State s f sp (Lcond cond args lbl :: b) rs m)
         E0 (State s f sp b (undef_temps rs) m)
   | exec_Ljumptable:
       forall s f sp arg tbl b rs m n lbl b',
       rs (R arg) = Vint n ->
-      list_nth_z tbl (Int.signed n) = Some lbl ->
+      list_nth_z tbl (Int.unsigned n) = Some lbl ->
       find_label lbl f.(fn_code) = Some b' ->
       step (State s f sp (Ljumptable arg tbl :: b) rs m)
         E0 (State s f sp b' (undef_temps rs) m)
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 4ea2ea9..ef6194c 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -16,10 +16,10 @@ Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
 Require Import Integers.
-Require Import Memdata.
+Require Import Values.
 Require Import Op.
-Require Import RTL.
 Require Import Locations.
+Require Import LTL.
 Require Import Linear.
 Require Import Conventions.
 
@@ -106,7 +106,7 @@ Inductive wt_instr : instruction -> Prop :=
   | wt_Ljumptable:
       forall arg tbl,
       mreg_type arg = Tint ->
-      list_length_z tbl * 4 <= Int.max_signed ->
+      list_length_z tbl * 4 <= Int.max_unsigned ->
       wt_instr (Ljumptable arg tbl)
   | wt_Lreturn: 
       wt_instr (Lreturn).
@@ -129,3 +129,66 @@ Inductive wt_fundef: fundef -> Prop :=
 Definition wt_program (p: program) : Prop :=
   forall i f, In (i, f) (prog_funct p) -> wt_fundef f.
 
+(** Typing the run-time state.  These definitions are used in [Stackingproof]. *)
+
+Require Import Values.
+
+Definition wt_locset (ls: locset) : Prop :=
+  forall l, Val.has_type (ls l) (Loc.type l).
+
+Lemma wt_setloc:
+  forall ls l v,
+  Val.has_type v (Loc.type l) -> wt_locset ls -> wt_locset (Locmap.set l v ls).
+Proof.
+  intros; red; intros.
+  unfold Locmap.set. 
+  destruct (Loc.eq l l0). congruence.
+  destruct (Loc.overlap l l0).  red. auto.
+  auto.
+Qed.
+
+Lemma wt_undef_temps:
+  forall ls, wt_locset ls -> wt_locset (undef_temps ls).
+Proof.
+  unfold undef_temps. generalize temporaries. induction l; simpl; intros.
+  auto.
+  apply IHl. apply wt_setloc; auto. red; auto.
+Qed.
+
+Lemma wt_undef_op:
+  forall op ls, wt_locset ls -> wt_locset (undef_op op ls).
+Proof.
+  intros. generalize (wt_undef_temps ls H); intro. case op; simpl; auto.
+Qed.
+
+Lemma wt_undef_getstack:
+  forall s ls, wt_locset ls -> wt_locset (undef_getstack s ls).
+Proof.
+  intros. unfold undef_getstack. destruct s; auto. apply wt_setloc; auto. red; auto.
+Qed.
+
+Lemma wt_call_regs:
+  forall ls, wt_locset ls -> wt_locset (call_regs ls).
+Proof.
+  intros; red; intros. unfold call_regs. destruct l. auto. 
+  destruct (in_dec Loc.eq (R m) temporaries). red; auto. auto.
+  destruct s. red; auto. 
+  change (Loc.type (S (Incoming z t))) with (Loc.type (S (Outgoing z t))). auto.
+  red; auto.
+Qed.
+
+Lemma wt_return_regs:
+  forall caller callee,
+  wt_locset caller -> wt_locset callee -> wt_locset (return_regs caller callee).
+Proof.
+  intros; red; intros.
+  unfold return_regs. destruct l; auto. 
+  destruct (in_dec Loc.eq (R m) temporaries); auto.
+  destruct (in_dec Loc.eq (R m) destroyed_at_call); auto.
+Qed.
+
+Lemma wt_init:
+  wt_locset (Locmap.init Vundef).
+Proof.
+  red; intros. unfold Locmap.init. red; auto.
+Qed.
diff --git a/backend/Mach.v b/backend/Mach.v
index c6a692a..223d5ab 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -13,8 +13,7 @@
 (** The Mach intermediate language: abstract syntax.
 
   Mach is the last intermediate language before generation of assembly
-  code.  This file defines the abstract syntax for Mach; two dynamic
-  semantics are given in modules [Machabstr] and [Machconcr].
+  code.  
 *)
 
 Require Import Coqlib.
@@ -25,6 +24,7 @@ Require Import Values.
 Require Import Memory.
 Require Import Events.
 Require Import Globalenvs.
+Require Import Smallstep.
 Require Import Op.
 Require Import Locations.
 Require Import Conventions.
@@ -40,7 +40,7 @@ Require Import Conventions.
   [Mgetstack] and [Msetstack] to read and write within the activation
   record for the current function, at a given word offset and with a
   given type; and [Mgetparam], to read within the activation record of
-  the caller.
+  the caller. 
 
   These instructions implement a more concrete view of the activation
   record than the the [Lgetstack] and [Lsetstack] instructions of
@@ -72,7 +72,6 @@ Record function: Type := mkfunction
   { fn_sig: signature;
     fn_code: code;
     fn_stacksize: Z;
-    fn_framesize: Z;
     fn_link_ofs: int;
     fn_retaddr_ofs: int }.
 
diff --git a/backend/Machconcr.v b/backend/Machconcr.v
index 5a98dd9..3f2a2e1 100644
--- a/backend/Machconcr.v
+++ b/backend/Machconcr.v
@@ -147,15 +147,15 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State s f sp (Msetstack src ofs ty :: c) rs m)
         E0 (State s f sp c rs m')
   | exec_Mgetparam:
-      forall s fb f sp parent ofs ty dst c rs m v,
+      forall s fb f sp ofs ty dst c rs m v,
       Genv.find_funct_ptr ge fb = Some (Internal f) ->
-      load_stack m sp Tint f.(fn_link_ofs) = Some parent ->
-      load_stack m parent ty ofs = Some v ->
+      load_stack m sp Tint f.(fn_link_ofs) = Some (parent_sp s) ->
+      load_stack m (parent_sp s) ty ofs = Some v ->
       step (State s fb sp (Mgetparam ofs ty dst :: c) rs m)
         E0 (State s fb sp c (rs # IT1 <- Vundef # dst <- v) m)
   | exec_Mop:
       forall s f sp op args res c rs m v,
-      eval_operation ge sp op rs##args = Some v ->
+      eval_operation ge sp op rs##args m = Some v ->
       step (State s f sp (Mop op args res :: c) rs m)
         E0 (State s f sp c ((undef_op op rs)#res <- v) m)
   | exec_Mload:
@@ -184,7 +184,7 @@ Inductive step: state -> trace -> state -> Prop :=
       Genv.find_funct_ptr ge fb = Some (Internal f) ->
       load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
       load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
-      Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' ->
+      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
       step (State s fb (Vptr stk soff) (Mtailcall sig ros :: c) rs m)
         E0 (Callstate s f' rs m')
   | exec_Mbuiltin:
@@ -200,20 +200,20 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State s fb sp c' rs m)
   | exec_Mcond_true:
       forall s fb f sp cond args lbl c rs m c',
-      eval_condition cond rs##args = Some true ->
+      eval_condition cond rs##args m = Some true ->
       Genv.find_funct_ptr ge fb = Some (Internal f) ->
       find_label lbl f.(fn_code) = Some c' ->
       step (State s fb sp (Mcond cond args lbl :: c) rs m)
         E0 (State s fb sp c' (undef_temps rs) m)
   | exec_Mcond_false:
       forall s f sp cond args lbl c rs m,
-      eval_condition cond rs##args = Some false ->
+      eval_condition cond rs##args m = Some false ->
       step (State s f sp (Mcond cond args lbl :: c) rs m)
         E0 (State s f sp c (undef_temps rs) m)
   | exec_Mjumptable:
       forall s fb f sp arg tbl c rs m n lbl c',
       rs arg = Vint n ->
-      list_nth_z tbl (Int.signed n) = Some lbl ->
+      list_nth_z tbl (Int.unsigned n) = Some lbl ->
       Genv.find_funct_ptr ge fb = Some (Internal f) ->
       find_label lbl f.(fn_code) = Some c' ->
       step (State s fb sp (Mjumptable arg tbl :: c) rs m)
@@ -223,18 +223,18 @@ Inductive step: state -> trace -> state -> Prop :=
       Genv.find_funct_ptr ge fb = Some (Internal f) ->
       load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
       load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
-      Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' ->
+      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
       step (State s fb (Vptr stk soff) (Mreturn :: c) rs m)
         E0 (Returnstate s rs m')
   | exec_function_internal:
       forall s fb rs m f m1 m2 m3 stk,
       Genv.find_funct_ptr ge fb = Some (Internal f) ->
-      Mem.alloc m (- f.(fn_framesize)) f.(fn_stacksize) = (m1, stk) ->
-      let sp := Vptr stk (Int.repr (-f.(fn_framesize))) in
+      Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) ->
+      let sp := Vptr stk Int.zero in
       store_stack m1 sp Tint f.(fn_link_ofs) (parent_sp s) = Some m2 ->
       store_stack m2 sp Tint f.(fn_retaddr_ofs) (parent_ra s) = Some m3 ->
       step (Callstate s fb rs m)
-        E0 (State s fb sp f.(fn_code) rs m3)
+        E0 (State s fb sp f.(fn_code) (undef_temps rs) m3)
   | exec_function_external:
       forall s fb rs m t rs' ef args res m',
       Genv.find_funct_ptr ge fb = Some (External ef) ->
diff --git a/backend/Machtyping.v b/backend/Machtyping.v
index 93ac00c..95ceafe 100644
--- a/backend/Machtyping.v
+++ b/backend/Machtyping.v
@@ -87,7 +87,7 @@ Inductive wt_instr : instruction -> Prop :=
   | wt_Mjumptable:
       forall arg tbl,
       mreg_type arg = Tint ->
-      list_length_z tbl * 4 <= Int.max_signed ->
+      list_length_z tbl * 4 <= Int.max_unsigned ->
       wt_instr (Mjumptable arg tbl)
   | wt_Mreturn: 
       wt_instr Mreturn.
@@ -96,24 +96,7 @@ Record wt_function (f: function) : Prop := mk_wt_function {
   wt_function_instrs:
     forall instr, In instr f.(fn_code) -> wt_instr instr;
   wt_function_stacksize:
-    f.(fn_stacksize) >= 0;
-  wt_function_framesize:
-    0 <= f.(fn_framesize) <= -Int.min_signed;
-  wt_function_framesize_aligned:
-    (4 | f.(fn_framesize));
-  wt_function_link:
-    0 <= Int.signed f.(fn_link_ofs)
-    /\ Int.signed f.(fn_link_ofs) + 4 <= f.(fn_framesize);
-  wt_function_link_aligned:
-    (4 | Int.signed f.(fn_link_ofs));
-  wt_function_retaddr:
-    0 <= Int.signed f.(fn_retaddr_ofs)
-    /\ Int.signed f.(fn_retaddr_ofs) + 4 <= f.(fn_framesize);
-  wt_function_retaddr_aligned:
-    (4 | Int.signed f.(fn_retaddr_ofs));
-  wt_function_link_retaddr:
-    Int.signed f.(fn_retaddr_ofs) + 4 <= Int.signed f.(fn_link_ofs)
-    \/ Int.signed f.(fn_link_ofs) + 4 <= Int.signed f.(fn_retaddr_ofs)
+    0 <= f.(fn_stacksize) <= Int.max_unsigned
 }.
 
 Inductive wt_fundef: fundef -> Prop :=
@@ -125,227 +108,3 @@ Inductive wt_fundef: fundef -> Prop :=
 
 Definition wt_program (p: program) : Prop :=
   forall i f, In (i, f) (prog_funct p) -> wt_fundef f.
-
-(** * Type soundness *)
-
-Require Import Machabstr.
-
-(** We show a weak type soundness result for the abstract semantics
-    of Mach: for a well-typed Mach program, if a transition is taken
-    from a state where registers hold values of their static types,
-    registers in the final state hold values of their static types
-    as well.  This is a subject reduction theorem for our type system.
-    It is used in the proof of implication from the abstract Mach
-    semantics to the concrete Mach semantics (file [Machabstr2concr]).
-*)
-
-Definition wt_regset (rs: regset) : Prop :=
-  forall r, Val.has_type (rs r) (mreg_type r).
-
-Definition wt_frame (fr: frame) : Prop :=
-  forall ty ofs, Val.has_type (fr ty ofs) ty.
-
-Lemma wt_setreg:
-  forall (rs: regset) (r: mreg) (v: val),
-  Val.has_type v (mreg_type r) ->
-  wt_regset rs -> wt_regset (rs#r <- v).
-Proof.
-  intros; red; intros. unfold Regmap.set. 
-  case (RegEq.eq r0 r); intro.
-  subst r0; assumption.
-  apply H0.
-Qed.
-
-Lemma wt_undef_temps:
-  forall rs, wt_regset rs -> wt_regset (undef_temps rs).
-Proof.
-  unfold undef_temps. 
-  generalize (int_temporaries ++ float_temporaries).
-  induction l; simpl; intros. auto.
-  apply IHl. red; intros. unfold Regmap.set.
-  destruct (RegEq.eq r a). constructor. auto. 
-Qed.
-
-Lemma wt_undef_op:
-  forall op rs, wt_regset rs -> wt_regset (undef_op op rs).
-Proof.
-  intros. set (W := wt_undef_temps rs H). 
-  destruct op; simpl; auto.
-Qed.
-
-Lemma wt_undef_getparam:
-  forall rs, wt_regset rs -> wt_regset (rs#IT1 <- Vundef).
-Proof.
-  intros; red; intros. unfold Regmap.set. 
-  destruct (RegEq.eq r IT1). constructor. auto.
-Qed.
-
-Lemma wt_get_slot:
-  forall f fr ty ofs v,
-  get_slot f fr ty ofs v ->
-  wt_frame fr ->
-  Val.has_type v ty. 
-Proof.
-  induction 1; intros.
-  subst v. apply H1.
-Qed.
-
-Lemma wt_set_slot:
-  forall f fr ty ofs v fr',
-  set_slot f fr ty ofs v fr' ->
-  wt_frame fr ->
-  Val.has_type v ty ->
-  wt_frame fr'.
-Proof.
-  intros. induction H. subst fr'; red; intros. unfold update.
-  destruct (zeq (ofs - f.(fn_framesize)) ofs0).
-  destruct (typ_eq ty ty0). congruence. exact I.
-  destruct (zle (ofs0 + AST.typesize ty0) (ofs - f.(fn_framesize))).
-  apply H0.
-  destruct (zle (ofs - f.(fn_framesize) + AST.typesize ty) ofs0).
-  apply H0.
-  exact I.
-Qed.
-
-Lemma wt_empty_frame:
-  wt_frame empty_frame.
-Proof.
-  intros; red; intros; exact I.
-Qed.
-
-Lemma is_tail_find_label:
-  forall lbl c c', find_label lbl c = Some c' -> is_tail c' c.
-Proof.
-  induction c; simpl.
-  intros; discriminate.
-  case (is_label lbl a); intros.
-  injection H; intro; subst c'. constructor. constructor.
-  constructor; auto.
-Qed.
-
-Section SUBJECT_REDUCTION.
-
-Inductive wt_stackframe: stackframe -> Prop :=
-  | wt_stackframe_intro: forall f sp c fr,
-      wt_function f ->
-      Val.has_type sp Tint ->
-      is_tail c f.(fn_code) ->
-      wt_frame fr ->
-      wt_stackframe (Stackframe f sp c fr).
-
-Inductive wt_state: state -> Prop :=
-  | wt_state_intro: forall stk f sp c rs fr m
-      (STK: forall s, In s stk -> wt_stackframe s)
-      (WTF: wt_function f)
-      (WTSP: Val.has_type sp Tint)
-      (TAIL: is_tail c f.(fn_code))
-      (WTRS: wt_regset rs)
-      (WTFR: wt_frame fr),
-      wt_state (State stk f sp c rs fr m)
-  | wt_state_call: forall stk f rs m,
-      (forall s, In s stk -> wt_stackframe s) ->
-      wt_fundef f ->
-      wt_regset rs ->
-      wt_state (Callstate stk f rs m)
-  | wt_state_return: forall stk rs m,
-      (forall s, In s stk -> wt_stackframe s) ->
-      wt_regset rs ->
-      wt_state (Returnstate stk rs m).
-
-Variable p: program.
-Hypothesis wt_p: wt_program p.
-Let ge := Genv.globalenv p.
-
-Lemma subject_reduction:
-  forall s1 t s2, step ge s1 t s2 ->
-  forall (WTS: wt_state s1), wt_state s2.
-Proof.
-  induction 1; intros; inv WTS;
-  try (generalize (wt_function_instrs _ WTF _ (is_tail_in TAIL)); intro WTI;
-       eapply wt_state_intro; eauto with coqlib).
-
-  apply wt_setreg; auto. inv WTI. eapply wt_get_slot; eauto.
-
-  eapply wt_set_slot; eauto. inv WTI; auto. 
-
-  assert (mreg_type dst = ty).
-    inv WTI; auto.
-  assert (wt_frame (parent_frame s)).
-    destruct s; simpl. apply wt_empty_frame. 
-    generalize (STK s (in_eq _ _)); intro. inv H1. auto. 
-  apply wt_setreg; auto.
-  rewrite H0. eapply wt_get_slot; eauto.
-  apply wt_undef_getparam; auto.
-
-(* op *)
-  apply wt_setreg; auto.
-  inv WTI.
-  (* move *)
-  simpl in H. inv H. rewrite <- H1. apply WTRS.
-  (* not move *)
-  replace (mreg_type res) with (snd (type_of_operation op)).
-  apply type_of_operation_sound with fundef unit ge rs##args sp; auto.
-  rewrite <- H4; reflexivity.
-  apply wt_undef_op; auto.
-
-(* load *)
-  apply wt_setreg; auto. inv WTI. rewrite H6. eapply type_of_chunk_correct; eauto.
-  apply wt_undef_temps; auto.
-
-(* store *)
-  apply wt_undef_temps; auto.
-
-(* call *)
-  assert (WTFD: wt_fundef f').
-    destruct ros; simpl in H.
-    apply (Genv.find_funct_prop wt_fundef _ _ wt_p H).
-    destruct (Genv.find_symbol ge i); try discriminate.
-    apply (Genv.find_funct_ptr_prop wt_fundef _ _ wt_p H).
-  econstructor; eauto.
-  intros. elim H0; intro. subst s0. econstructor; eauto with coqlib.
-  auto.
-
-(* tailcall *)
-  assert (WTFD: wt_fundef f').
-    destruct ros; simpl in H.
-    apply (Genv.find_funct_prop wt_fundef _ _ wt_p H).
-    destruct (Genv.find_symbol ge i); try discriminate.
-    apply (Genv.find_funct_ptr_prop wt_fundef _ _ wt_p H).
-  econstructor; eauto.
-
-(* extcall *)
-  apply wt_setreg; auto. 
-  inv WTI. rewrite H4. eapply external_call_well_typed; eauto.
-  apply wt_undef_temps; auto.
-
-(* goto *)  
-  apply is_tail_find_label with lbl; congruence.
-(* cond *)
-  apply is_tail_find_label with lbl; congruence. apply wt_undef_temps; auto.
-  apply wt_undef_temps; auto.
-(* jumptable *)
-  apply is_tail_find_label with lbl; congruence. apply wt_undef_temps; auto. 
-
-(* return *)
-  econstructor; eauto.
-
-(* internal function *)
-  econstructor; eauto with coqlib. inv H5; auto. exact I. 
-  apply wt_empty_frame.
-
-(* external function *)
-  econstructor; eauto. apply wt_setreg; auto.
-  generalize (external_call_well_typed _ _ _ _ _ _ _ H).  
-  unfold proj_sig_res, loc_result.
-  destruct (sig_res (ef_sig ef)).
-  destruct t0; simpl; auto.
-  simpl; auto.
-
-(* returnstate *)
-  generalize (H1 _ (in_eq _ _)); intro. inv H.
-  econstructor; eauto. 
-  eauto with coqlib.
-Qed.
-
-End SUBJECT_REDUCTION.
-
diff --git a/backend/RTL.v b/backend/RTL.v
index 208c7b1..2cb2719 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -217,7 +217,7 @@ Inductive step: state -> trace -> state -> Prop :=
   | exec_Iop:
       forall s f sp pc rs m op args res pc' v,
       (fn_code f)!pc = Some(Iop op args res pc') ->
-      eval_operation ge sp op rs##args = Some v ->
+      eval_operation ge sp op rs##args m = Some v ->
       step (State s f sp pc rs m)
         E0 (State s f sp pc' (rs#res <- v) m)
   | exec_Iload:
@@ -258,20 +258,20 @@ Inductive step: state -> trace -> state -> Prop :=
   | exec_Icond_true:
       forall s f sp pc rs m cond args ifso ifnot,
       (fn_code f)!pc = Some(Icond cond args ifso ifnot) ->
-      eval_condition cond rs##args = Some true ->
+      eval_condition cond rs##args m = Some true ->
       step (State s f sp pc rs m)
         E0 (State s f sp ifso rs m)
   | exec_Icond_false:
       forall s f sp pc rs m cond args ifso ifnot,
       (fn_code f)!pc = Some(Icond cond args ifso ifnot) ->
-      eval_condition cond rs##args = Some false ->
+      eval_condition cond rs##args m = Some false ->
       step (State s f sp pc rs m)
         E0 (State s f sp ifnot rs m)
   | exec_Ijumptable:
       forall s f sp pc rs m arg tbl n pc',
       (fn_code f)!pc = Some(Ijumptable arg tbl) ->
       rs#arg = Vint n ->
-      list_nth_z tbl (Int.signed n) = Some pc' ->
+      list_nth_z tbl (Int.unsigned n) = Some pc' ->
       step (State s f sp pc rs m)
         E0 (State s f sp pc' rs m)
   | exec_Ireturn:
@@ -303,7 +303,7 @@ Inductive step: state -> trace -> state -> Prop :=
 Lemma exec_Iop':
   forall s f sp pc rs m op args res pc' rs' v,
   (fn_code f)!pc = Some(Iop op args res pc') ->
-  eval_operation ge sp op rs##args = Some v ->
+  eval_operation ge sp op rs##args m = Some v ->
   rs' = (rs#res <- v) ->
   step (State s f sp pc rs m)
     E0 (State s f sp pc' rs' m).
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index 24f8c1a..e72b000 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -419,6 +419,7 @@ Lemma transl_switch_correct:
   nth_error nexits act = Some nd /\
   match_env map e nil rs'.
 Proof.
+  Opaque Int.sub.
   induction 1; simpl; intros.
 (* action *)
   inv H3. exists n; exists rs; intuition.
@@ -584,7 +585,7 @@ Lemma transl_expr_Eop_correct:
          (vargs : list val) (v : val),
   eval_exprlist ge sp e m le args vargs ->
   transl_exprlist_prop le args vargs ->
-  eval_operation ge sp op vargs = Some v ->
+  eval_operation ge sp op vargs m = Some v ->
   transl_expr_prop le (Eop op args) v.
 Proof.
   intros; red; intros. inv TE.
@@ -730,7 +731,7 @@ Lemma transl_condition_CEcond_correct:
          (vargs : list val) (b : bool),
   eval_exprlist ge sp e m le args vargs ->
   transl_exprlist_prop le args vargs ->
-  eval_condition cond vargs = Some b ->
+  eval_condition cond vargs m = Some b ->
   transl_condition_prop le (CEcond cond args) b.
 Proof.
   intros; red; intros; inv TE.
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 533c47a..a002746 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -123,7 +123,7 @@ Inductive wt_instr : instruction -> Prop :=
       forall arg tbl,
       env arg = Tint ->
       (forall s, In s tbl -> valid_successor s) ->
-      list_length_z tbl * 4 <= Int.max_signed ->
+      list_length_z tbl * 4 <= Int.max_unsigned ->
       wt_instr (Ijumptable arg tbl)
   | wt_Ireturn: 
       forall optres,
@@ -245,7 +245,7 @@ Definition check_instr (i: instruction) : bool :=
   | Ijumptable arg tbl =>
       check_reg arg Tint
       && List.forallb check_successor tbl
-      && zle (list_length_z tbl * 4) Int.max_signed
+      && zle (list_length_z tbl * 4) Int.max_unsigned
   | Ireturn optres =>
       match optres, funct.(fn_sig).(sig_res) with
       | None, None => true
@@ -527,7 +527,7 @@ Proof.
   econstructor; eauto.
   apply wt_regset_assign. auto.
   replace (env res) with (snd (type_of_operation op)).
-  apply type_of_operation_sound with fundef unit ge rs##args sp; auto.
+  eapply type_of_operation_sound; eauto.
   rewrite <- H6. reflexivity.
   (* Iload *)
   econstructor; eauto.
diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v
index a3ed303..09a9101 100644
--- a/backend/Reloadproof.v
+++ b/backend/Reloadproof.v
@@ -156,10 +156,10 @@ Proof.
 Qed.
 
 Lemma not_enough_temporaries_addr:
-  forall (ge: genv) sp addr src args ls v,
+  forall (ge: genv) sp addr src args ls v m,
   enough_temporaries (src :: args) = false ->
   eval_addressing ge sp addr (List.map ls args) = Some v ->
-  eval_operation ge sp (op_for_binary_addressing addr) (List.map ls args) = Some v.
+  eval_operation ge sp (op_for_binary_addressing addr) (List.map ls args) m = Some v.
 Proof.
   intros.
   apply eval_op_for_binary_addressing; auto.
@@ -692,7 +692,8 @@ Proof.
   unfold call_regs, parameter_of_argument. 
   generalize (loc_arguments_acceptable _ _ H). 
   unfold loc_argument_acceptable. 
-  destruct x. auto.
+  destruct x.
+  intros. destruct (in_dec Loc.eq (R m) temporaries). contradiction. auto.
   destruct s; intros; try contradiction. auto.
 Qed. 
 
@@ -1015,9 +1016,9 @@ Proof.
   exploit add_reloads_correct. 
     eapply enough_temporaries_op_args; eauto. auto.
   intros [ls2 [A [B C]]]. instantiate (1 := ls) in B. 
-  assert (exists tv, eval_operation tge sp op (reglist ls2 (regs_for args)) = Some tv
+  assert (exists tv, eval_operation tge sp op (reglist ls2 (regs_for args)) tm = Some tv
                      /\ Val.lessdef v tv).
-    apply eval_operation_lessdef with (map rs args); auto.
+    apply eval_operation_lessdef with (map rs args) m; auto.
     rewrite B. eapply agree_locs; eauto. 
     rewrite <- H. apply eval_operation_preserved. exact symbols_preserved.
   destruct H1 as [tv [P Q]].
@@ -1291,7 +1292,7 @@ Proof.
   intros [ls2 [A [B C]]].
   left; econstructor; split.
   eapply plus_right. eauto. eapply exec_Lcond_true; eauto.
-  rewrite B. apply eval_condition_lessdef with (map rs args); auto.
+  rewrite B. apply eval_condition_lessdef with (map rs args) m; auto.
   eapply agree_locs; eauto. 
   apply find_label_transf_function; eauto.
   traceEq.
@@ -1306,7 +1307,7 @@ Proof.
   intros [ls2 [A [B C]]].
   left; econstructor; split.
   eapply plus_right. eauto. eapply exec_Lcond_false; eauto.
-  rewrite B. apply eval_condition_lessdef with (map rs args); auto.
+  rewrite B. apply eval_condition_lessdef with (map rs args) m; auto.
   eapply agree_locs; eauto. 
   traceEq.
   econstructor; eauto with coqlib.
diff --git a/backend/Selection.v b/backend/Selection.v
index 68fb9ba..9e11bc3 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -78,7 +78,7 @@ Fixpoint condexpr_of_expr (e: expr) : condexpr :=
   | Econdition ce e1 e2 =>
       CEcondition ce (condexpr_of_expr e1) (condexpr_of_expr e2)
   | _ =>
-      CEcond (Ccompimm Cne Int.zero) (e:::Enil)
+      CEcond (Ccompuimm Cne Int.zero) (e:::Enil)
   end.
 
 (** Conversion of loads and stores *)
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index d997015..d475f26 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -86,7 +86,7 @@ Lemma eval_base_condition_of_expr:
   eval_expr ge sp e m le a v ->
   Val.bool_of_val v b ->
   eval_condexpr ge sp e m le 
-                (CEcond (Ccompimm Cne Int.zero) (a ::: Enil))
+                (CEcond (Ccompuimm Cne Int.zero) (a ::: Enil))
                 b.
 Proof.
   intros. 
@@ -97,7 +97,7 @@ Qed.
 Lemma is_compare_neq_zero_correct:
   forall c v b,
   is_compare_neq_zero c = true ->
-  eval_condition c (v :: nil) = Some b ->
+  eval_condition c (v :: nil) m = Some b ->
   Val.bool_of_val v b.
 Proof.
   intros.
@@ -107,17 +107,18 @@ Proof.
 
   simpl in H0. destruct v; inv H0. 
   generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intros; simpl.
-  subst i; constructor. constructor; auto. constructor.
+  subst i; constructor. constructor; auto.
 
   simpl in H0. destruct v; inv H0. 
   generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intros; simpl.
   subst i; constructor. constructor; auto.
+  constructor.
 Qed.
 
 Lemma is_compare_eq_zero_correct:
   forall c v b,
   is_compare_eq_zero c = true ->
-  eval_condition c (v :: nil) = Some b ->
+  eval_condition c (v :: nil) m = Some b ->
   Val.bool_of_val v (negb b).
 Proof.
   intros. apply is_compare_neq_zero_correct with (negate_condition c).
@@ -145,8 +146,8 @@ Proof.
   eapply eval_base_condition_of_expr; eauto.
 
   inv H0. simpl in H7.
-  assert (eval_condition c vl = Some b).
-    destruct (eval_condition c vl); try discriminate.
+  assert (eval_condition c vl m = Some b).
+    destruct (eval_condition c vl m); try discriminate.
     destruct b0; inv H7; inversion H1; congruence.
   assert (eval_condexpr ge sp e m le (CEcond c e0) b).
     eapply eval_CEcond; eauto.
@@ -230,7 +231,7 @@ Lemma eval_sel_binop:
   forall le op a1 a2 v1 v2 v,
   eval_expr ge sp e m le a1 v1 ->
   eval_expr ge sp e m le a2 v2 ->
-  eval_binop op v1 v2 = Some v ->
+  eval_binop op v1 v2 m = Some v ->
   eval_expr ge sp e m le (sel_binop op a1 a2) v.
 Proof.
   destruct op; simpl; intros; FuncInv; try subst v.
@@ -263,13 +264,15 @@ Proof.
   apply eval_subf; auto.
   apply eval_mulf; auto.
   apply eval_divf; auto.
-  apply eval_comp_int; auto.
-  eapply eval_comp_int_ptr; eauto.
-  eapply eval_comp_ptr_int; eauto.
+  apply eval_comp; auto.
+  eapply eval_compu_int; eauto.
+  eapply eval_compu_int_ptr; eauto.
+  eapply eval_compu_ptr_int; eauto.
+  destruct (Mem.valid_pointer m b (Int.unsigned i) &&
+            Mem.valid_pointer m b0 (Int.unsigned i0)) as [] _eqn; try congruence.
   destruct (eq_block b b0); inv H1.
-  eapply eval_comp_ptr_ptr; eauto.
-  eapply eval_comp_ptr_ptr_2; eauto.
-  eapply eval_compu; eauto.
+  eapply eval_compu_ptr_ptr; eauto.
+  eapply eval_compu_ptr_ptr_2; eauto.
   eapply eval_compf; eauto.
 Qed.
 
diff --git a/backend/Stacking.v b/backend/Stacking.v
index 2ea08be..09d98d6 100644
--- a/backend/Stacking.v
+++ b/backend/Stacking.v
@@ -118,19 +118,17 @@ Definition restore_callee_save (fe: frame_env) (k: Mach.code) :=
 (** * Code transformation. *)
 
 (** Translation of operations and addressing mode.
-  In Linear, the stack pointer has offset 0, i.e. points to the
-  beginning of the Cminor stack data block.  In Mach, the stack
-  pointer points to the bottom of the activation record,
-  at offset [- fe.(fe_size)] where [fe] is the frame environment.
+  The Cminor stack data block starts at offset 0 in Linear,
+  but at offset [fe.(fe_stack_data)] in Mach.
   Operations and addressing mode that are relative to the stack pointer
-  must therefore be offset by [fe.(fe_size)] to preserve their
+  must therefore be offset by [fe.(fe_stack_data)] to preserve their
   behaviour. *)
 
 Definition transl_op (fe: frame_env) (op: operation) :=
-  shift_stack_operation (Int.repr fe.(fe_size)) op.
+  shift_stack_operation (Int.repr fe.(fe_stack_data)) op.
 
 Definition transl_addr (fe: frame_env) (addr: addressing) :=
-  shift_stack_addressing (Int.repr fe.(fe_size)) addr.
+  shift_stack_addressing (Int.repr fe.(fe_stack_data)) addr.
 
 (** Translation of a Linear instruction.  Prepends the corresponding
   Mach instructions to the given list of instructions.
@@ -193,8 +191,8 @@ Definition transl_instr
   by the translation of the function body.
 
   Subtle point: the compiler must check that the frame is no
-  larger than [- Int.min_signed] bytes, otherwise arithmetic overflows
-  could occur during frame accesses using signed machine integers as
+  larger than [Int.max_unsigned] bytes, otherwise arithmetic overflows
+  could occur during frame accesses using unsigned machine integers as
   offsets. *)
 
 Definition transl_code
@@ -208,15 +206,12 @@ Open Local Scope string_scope.
 
 Definition transf_function (f: Linear.function) : res Mach.function :=
   let fe := make_env (function_bounds f) in
-  if zlt f.(Linear.fn_stacksize) 0 then
-    Error (msg "Stacking.transf_function") 
-  else if zlt (- Int.min_signed) fe.(fe_size) then
+  if zlt Int.max_unsigned fe.(fe_size) then
     Error (msg "Too many spilled variables, stack size exceeded")
   else
     OK (Mach.mkfunction
          f.(Linear.fn_sig)
          (transl_body f fe)
-         f.(Linear.fn_stacksize)
          fe.(fe_size)
          (Int.repr fe.(fe_ofs_link))
          (Int.repr fe.(fe_ofs_retaddr))).
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index 5b06c71..c32886c 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -12,13 +12,7 @@
 
 (** Correctness proof for the translation from Linear to Mach. *)
 
-(** This file proves semantic preservation for the [Stacking] pass.
-  For the target language Mach, we use the abstract semantics
-  given in file [Machabstr], where a part of the activation record
-  is not resident in memory.  Combined with the semantic equivalence
-  result between the two Mach semantics (see file [Machabstr2concr]),
-  the proof in this file also shows semantic preservation with
-  respect to the concrete Mach semantics. *)
+(** This file proves semantic preservation for the [Stacking] pass. *)
 
 Require Import Coqlib.
 Require Import Maps.
@@ -36,15 +30,13 @@ Require LTL.
 Require Import Linear.
 Require Import Lineartyping.
 Require Import Mach.
-Require Import Machabstr.
+Require Import Machconcr.
 Require Import Bounds.
 Require Import Conventions.
 Require Import Stacklayout.
 Require Import Stacking.
 
-(** * Properties of frames and frame accesses *)
-
-(** ``Good variable'' properties for frame accesses. *)
+(** * Properties of frame offsets *)
 
 Lemma typesize_typesize:
   forall ty, AST.typesize ty = 4 * Locations.typesize ty.
@@ -52,6 +44,12 @@ Proof.
   destruct ty; auto.
 Qed.
 
+Remark size_type_chunk:
+  forall ty, size_chunk (chunk_of_type ty) = AST.typesize ty.
+Proof.
+  destruct ty; reflexivity.
+Qed.
+
 Section PRESERVATION.
 
 Variable prog: Linear.program.
@@ -63,7 +61,6 @@ Let tge := Genv.globalenv tprog.
 
 Section FRAME_PROPERTIES.
 
-Variable stack: list Machabstr.stackframe.
 Variable f: Linear.function.
 Let b := function_bounds f.
 Let fe := make_env b.
@@ -74,27 +71,30 @@ Lemma unfold_transf_function:
   tf = Mach.mkfunction
          f.(Linear.fn_sig)
          (transl_body f fe)
-         f.(Linear.fn_stacksize)
          fe.(fe_size)
          (Int.repr fe.(fe_ofs_link))
          (Int.repr fe.(fe_ofs_retaddr)).
 Proof.
   generalize TRANSF_F. unfold transf_function.
-  case (zlt (Linear.fn_stacksize f) 0). intros; discriminate.
-  case (zlt (- Int.min_signed) (fe_size (make_env (function_bounds f)))).
+  destruct (zlt Int.max_unsigned (fe_size (make_env (function_bounds f)))).
   intros; discriminate.
   intros. unfold fe. unfold b. congruence.
 Qed.
 
-Lemma size_no_overflow: fe.(fe_size) <= -Int.min_signed.
+Lemma size_no_overflow: fe.(fe_size) <= Int.max_unsigned.
 Proof.
   generalize TRANSF_F. unfold transf_function.
-  case (zlt (Linear.fn_stacksize f) 0). intros; discriminate.
-  case (zlt (- Int.min_signed) (fe_size (make_env (function_bounds f)))).
+  destruct (zlt Int.max_unsigned (fe_size (make_env (function_bounds f)))).
   intros; discriminate.
-  intros. unfold fe, b. omega.
+  intros. unfold fe. unfold b. omega.
 Qed.
 
+Remark bound_stack_data_stacksize:
+  f.(Linear.fn_stacksize) <= b.(bound_stack_data).
+Proof.
+  unfold b, function_bounds, bound_stack_data. apply Zmax1.
+Qed.  
+
 (** A frame index is valid if it lies within the resource bounds
   of the current function. *)
 
@@ -135,18 +135,26 @@ Definition index_diff (idx1 idx2: frame_index) : Prop :=
   | _, _ => True
   end.
 
+Lemma index_diff_sym:
+  forall idx1 idx2, index_diff idx1 idx2 -> index_diff idx2 idx1.
+Proof.
+  unfold index_diff; intros. 
+  destruct idx1; destruct idx2; intuition.
+Qed.
+
 Ltac AddPosProps :=
   generalize (bound_int_local_pos b); intro;
   generalize (bound_float_local_pos b); intro;
   generalize (bound_int_callee_save_pos b); intro;
   generalize (bound_float_callee_save_pos b); intro;
   generalize (bound_outgoing_pos b); intro;
-  generalize (align_float_part b); intro.
+  generalize (bound_stack_data_pos b); intro.
 
-Lemma size_pos: fe.(fe_size) >= 0.
+Lemma size_pos: 0 <= fe.(fe_size).
 Proof.
+  generalize (frame_env_separated b). intuition.
   AddPosProps.
-  unfold fe, make_env, fe_size. omega.
+  unfold fe. omega.
 Qed.
 
 Opaque function_bounds.
@@ -155,61 +163,79 @@ Lemma offset_of_index_disj:
   forall idx1 idx2,
   index_valid idx1 -> index_valid idx2 ->
   index_diff idx1 idx2 ->
-  offset_of_index fe idx1 + 4 * typesize (type_of_index idx1) <= offset_of_index fe idx2 \/
-  offset_of_index fe idx2 + 4 * typesize (type_of_index idx2) <= offset_of_index fe idx1.
+  offset_of_index fe idx1 + AST.typesize (type_of_index idx1) <= offset_of_index fe idx2 \/
+  offset_of_index fe idx2 + AST.typesize (type_of_index idx2) <= offset_of_index fe idx1.
 Proof.
+  intros idx1 idx2 V1 V2 DIFF.
+  generalize (frame_env_separated b). intuition. fold fe in H.
   AddPosProps.
-  intros.
   destruct idx1; destruct idx2;
   try (destruct t); try (destruct t0);
-  unfold offset_of_index, fe, make_env,
-    fe_size, fe_ofs_int_local, fe_ofs_int_callee_save,
-    fe_ofs_float_local, fe_ofs_float_callee_save,
-    fe_ofs_link, fe_ofs_retaddr, fe_ofs_arg,
-    type_of_index, typesize;
-  simpl in H5; simpl in H6; simpl in H7;
+  unfold offset_of_index, type_of_index, AST.typesize;
+  simpl in V1; simpl in V2; simpl in DIFF;
   try omega.
   assert (z <> z0). intuition auto. omega.
   assert (z <> z0). intuition auto. omega.
 Qed.
 
+Lemma offset_of_index_disj_stack_data_1:
+  forall idx,
+  index_valid idx ->
+  offset_of_index fe idx + AST.typesize (type_of_index idx) <= fe.(fe_stack_data)
+  \/ fe.(fe_stack_data) + b.(bound_stack_data) <= offset_of_index fe idx.
+Proof.
+  intros idx V.
+  generalize (frame_env_separated b). intuition. fold fe in H.
+  AddPosProps.
+  destruct idx; try (destruct t);
+  unfold offset_of_index, type_of_index, AST.typesize;
+  simpl in V;
+  omega.
+Qed.
+
+Lemma offset_of_index_disj_stack_data_2:
+  forall idx,
+  index_valid idx ->
+  offset_of_index fe idx + AST.typesize (type_of_index idx) <= fe.(fe_stack_data)
+  \/ fe.(fe_stack_data) + f.(Linear.fn_stacksize) <= offset_of_index fe idx.
+Proof.
+  intros. 
+  exploit offset_of_index_disj_stack_data_1; eauto.
+  generalize bound_stack_data_stacksize. 
+  omega.
+Qed.
+
+(** Alignment properties *)
+
 Remark aligned_4_4x: forall x, (4 | 4 * x).
 Proof. intro. exists x; ring. Qed.
 
 Remark aligned_4_8x: forall x, (4 | 8 * x).
 Proof. intro. exists (x * 2); ring. Qed.
 
-Remark aligned_4_align8: forall x, (4 | align x 8).
-Proof. 
-  intro. apply Zdivides_trans with 8. exists 2; auto. apply align_divides. omega.
-Qed.
-
-Hint Resolve Zdivide_0 Zdivide_refl Zdivide_plus_r
-             aligned_4_4x aligned_4_8x aligned_4_align8: align_4.
+Remark aligned_8_4:
+  forall x, (8 | x) -> (4 | x).
+Proof. intros. apply Zdivides_trans with 8; auto. exists 2; auto. Qed.
 
+Hint Resolve Zdivide_0 Zdivide_refl Zdivide_plus_r 
+             aligned_4_4x aligned_4_8x aligned_8_4: align_4.
 Hint Extern 4 (?X | ?Y) => (exists (Y/X); reflexivity) : align_4.
 
 Lemma offset_of_index_aligned:
   forall idx, (4 | offset_of_index fe idx).
 Proof.
   intros.
-  destruct idx;
-  unfold offset_of_index, fe, make_env,
-    fe_size, fe_ofs_int_local, fe_ofs_int_callee_save,
-    fe_ofs_float_local, fe_ofs_float_callee_save,
-    fe_ofs_link, fe_ofs_retaddr, fe_ofs_arg;
+  generalize (frame_env_aligned b). intuition. fold fe in H. intuition.
+  destruct idx; try (destruct t);
+  unfold offset_of_index, type_of_index, AST.typesize;
   auto with align_4.
-  destruct t; auto with align_4.
 Qed.
 
-Lemma frame_size_aligned:
-  (4 | fe_size fe).
+Lemma fe_stack_data_aligned:
+  (4 | fe_stack_data fe).
 Proof.
-  unfold offset_of_index, fe, make_env,
-    fe_size, fe_ofs_int_local, fe_ofs_int_callee_save,
-    fe_ofs_float_local, fe_ofs_float_callee_save,
-    fe_ofs_link, fe_ofs_retaddr, fe_ofs_arg;
-  auto with align_4.
+  intros.
+  generalize (frame_env_aligned b). intuition. fold fe in H. intuition.
 Qed.
 
 (** The following lemmas give sufficient conditions for indices
@@ -262,19 +288,26 @@ Lemma offset_of_index_valid:
   forall idx,
   index_valid idx ->
   0 <= offset_of_index fe idx /\
-  offset_of_index fe idx + 4 * typesize (type_of_index idx) <= fe.(fe_size).
+  offset_of_index fe idx + AST.typesize (type_of_index idx) <= fe.(fe_size).
 Proof.
+  intros idx V.
+  generalize (frame_env_separated b). intros [A B]. fold fe in A. fold fe in B.
+  AddPosProps.
+  destruct idx; try (destruct t);
+  unfold offset_of_index, type_of_index, AST.typesize;
+  simpl in V;
+  omega.
+Qed.
+
+(** The image of the Linear stack data block lies within the bounds of the frame. *)
+
+Lemma stack_data_offset_valid:
+  0 <= fe.(fe_stack_data) /\ fe.(fe_stack_data) + b.(bound_stack_data) <= fe.(fe_size).
+Proof.
+  generalize (frame_env_separated b). intros [A B]. fold fe in A. fold fe in B.
   AddPosProps.
-  intros.
-  destruct idx; try destruct t;
-  unfold offset_of_index, fe, make_env,
-    fe_size, fe_ofs_int_local, fe_ofs_int_callee_save,
-    fe_ofs_float_local, fe_ofs_float_callee_save,
-    fe_ofs_link, fe_ofs_retaddr, fe_ofs_arg,
-    type_of_index, typesize;
-  unfold index_valid in H5; simpl typesize in H5;
   omega.
-Qed. 
+Qed.
 
 (** Offsets for valid index are representable as signed machine integers
   without loss of precision. *)
@@ -282,142 +315,248 @@ Qed.
 Lemma offset_of_index_no_overflow:
   forall idx,
   index_valid idx ->
-  Int.signed (Int.repr (offset_of_index fe idx)) = offset_of_index fe idx.
+  Int.unsigned (Int.repr (offset_of_index fe idx)) = offset_of_index fe idx.
 Proof.
   intros.
   generalize (offset_of_index_valid idx H). intros [A B].
-  apply Int.signed_repr.
-  split. apply Zle_trans with 0; auto. compute; intro; discriminate.
-  assert (offset_of_index fe idx < fe_size fe).
-    generalize (typesize_pos (type_of_index idx)); intro. omega.
-  apply Zlt_succ_le. 
-  change (Zsucc Int.max_signed) with (- Int.min_signed).
-  generalize size_no_overflow. omega. 
+  apply Int.unsigned_repr.
+  generalize (AST.typesize_pos (type_of_index idx)).
+  generalize size_no_overflow. 
+  omega.
 Qed.
 
-(** Characterization of the [get_slot] and [set_slot]
-  operations in terms of the following [index_val] and [set_index_val]
-  frame access functions. *)
+(** Likewise, for offsets within the Linear stack slot, after shifting. *)
 
-Definition index_val (idx: frame_index) (fr: frame) :=
-  fr (type_of_index idx) (offset_of_index fe idx - tf.(fn_framesize)).
+Lemma shifted_stack_offset_no_overflow:
+  forall ofs,
+  0 <= Int.unsigned ofs < Linear.fn_stacksize f ->
+  Int.unsigned (Int.add ofs (Int.repr fe.(fe_stack_data))) 
+  = Int.unsigned ofs + fe.(fe_stack_data).
+Proof.
+  intros. unfold Int.add.
+  generalize size_no_overflow stack_data_offset_valid bound_stack_data_stacksize; intros.
+  AddPosProps.
+  replace (Int.unsigned (Int.repr (fe_stack_data fe))) with (fe_stack_data fe).
+  apply Int.unsigned_repr. omega. 
+  symmetry. apply Int.unsigned_repr. omega.
+Qed.
 
-Definition set_index_val (idx: frame_index) (v: val) (fr: frame) :=
-  update (type_of_index idx) (offset_of_index fe idx - tf.(fn_framesize)) v fr.
+(** * Contents of frame slots *)
 
-Lemma slot_valid_index:
-  forall idx,
-  index_valid idx -> idx <> FI_link -> idx <> FI_retaddr ->
-  slot_valid tf (type_of_index idx) (offset_of_index fe idx).
+Inductive index_contains (m: mem) (sp: block) (idx: frame_index) (v: val) : Prop :=
+  | index_contains_intro:
+      index_valid idx ->
+      Mem.load (chunk_of_type (type_of_index idx)) m sp (offset_of_index fe idx) = Some v ->
+      index_contains m sp idx v.
+
+Lemma index_contains_load_stack:
+  forall m sp idx v,
+  index_contains m sp idx v ->
+  load_stack m (Vptr sp Int.zero) (type_of_index idx)
+              (Int.repr (offset_of_index fe idx)) = Some v.
+Proof.
+  intros. inv H. 
+  unfold load_stack, Mem.loadv, Val.add. rewrite Int.add_commut. rewrite Int.add_zero.
+  rewrite offset_of_index_no_overflow; auto.
+Qed.
+
+(** Good variable properties for [index_contains] *)
+
+Lemma gss_index_contains_base:
+  forall idx m m' sp v,
+  Mem.store (chunk_of_type (type_of_index idx)) m sp (offset_of_index fe idx) v = Some m' ->
+  index_valid idx ->
+  exists v',
+     index_contains m' sp idx v'
+  /\ decode_encode_val v (chunk_of_type (type_of_index idx)) (chunk_of_type (type_of_index idx)) v'.
+Proof.
+  intros. 
+  exploit Mem.load_store_similar. eauto. reflexivity. 
+  intros [v' [A B]].
+  exists v'; split; auto. constructor; auto.
+Qed.
+
+Lemma gss_index_contains:
+  forall idx m m' sp v,
+  Mem.store (chunk_of_type (type_of_index idx)) m sp (offset_of_index fe idx) v = Some m' ->
+  index_valid idx ->
+  Val.has_type v (type_of_index idx) ->
+  index_contains m' sp idx v.
+Proof.
+  intros. exploit gss_index_contains_base; eauto. intros [v' [A B]].
+  assert (v' = v).
+    destruct v; destruct (type_of_index idx); simpl in *; intuition congruence.
+  subst v'. auto.
+Qed.
+
+Lemma gso_index_contains:
+  forall idx m m' sp v idx' v',
+  Mem.store (chunk_of_type (type_of_index idx)) m sp (offset_of_index fe idx) v = Some m' ->
+  index_valid idx ->
+  index_contains m sp idx' v' ->
+  index_diff idx idx' ->
+  index_contains m' sp idx' v'.
+Proof.
+  intros. inv H1. constructor; auto. 
+  rewrite <- H4. eapply Mem.load_store_other; eauto.
+  right. repeat rewrite size_type_chunk. 
+  apply offset_of_index_disj; auto. apply index_diff_sym; auto.
+Qed.
+
+Lemma store_other_index_contains:
+  forall chunk m blk ofs v' m' sp idx v,
+  Mem.store chunk m blk ofs v' = Some m' ->
+  blk <> sp \/
+    (fe.(fe_stack_data) <= ofs /\ ofs + size_chunk chunk <= fe.(fe_stack_data) + f.(Linear.fn_stacksize)) ->
+  index_contains m sp idx v ->
+  index_contains m' sp idx v.
+Proof.
+  intros. inv H1. constructor; auto. rewrite <- H3. 
+  eapply Mem.load_store_other; eauto. 
+  destruct H0. auto. right. 
+  exploit offset_of_index_disj_stack_data_2; eauto. intros.
+  rewrite size_type_chunk.
+  omega.
+Qed.
+
+Definition frame_perm_freeable (m: mem) (sp: block): Prop :=
+  forall ofs,
+  0 <= ofs < fe.(fe_size) ->
+  ofs < fe.(fe_stack_data) \/ fe.(fe_stack_data) + f.(Linear.fn_stacksize) <= ofs ->
+  Mem.perm m sp ofs Freeable.
+
+Lemma offset_of_index_perm:
+  forall m sp idx,
+  index_valid idx ->
+  frame_perm_freeable m sp ->
+  Mem.range_perm m sp (offset_of_index fe idx) (offset_of_index fe idx + AST.typesize (type_of_index idx)) Freeable.
 Proof.
   intros.
-  destruct (offset_of_index_valid idx H) as [A B].
-  rewrite <- typesize_typesize in B.
-  rewrite unfold_transf_function; constructor.
-  auto. unfold fn_framesize. auto.
-  unfold fn_link_ofs. change (fe_ofs_link fe) with (offset_of_index fe FI_link).
-  rewrite offset_of_index_no_overflow.
-  exploit (offset_of_index_disj idx FI_link).
-    auto. exact I. red. destruct idx; auto || congruence.
-  intro. rewrite typesize_typesize. assumption.
-  exact I.
-  unfold fn_retaddr_ofs. change (fe_ofs_retaddr fe) with (offset_of_index fe FI_retaddr).
-  rewrite offset_of_index_no_overflow.
-  exploit (offset_of_index_disj idx FI_retaddr).
-    auto. exact I. red. destruct idx; auto || congruence.
-  intro. rewrite typesize_typesize. assumption.
-  exact I.
-  apply offset_of_index_aligned.
-Qed.
-
-Lemma get_slot_index:
-  forall fr idx ty v,
-  index_valid idx -> idx <> FI_link -> idx <> FI_retaddr ->
-  ty = type_of_index idx ->
-  v = index_val idx fr ->
-  get_slot tf fr ty (Int.signed (Int.repr (offset_of_index fe idx))) v.
-Proof.
-  intros. subst v; subst ty. rewrite offset_of_index_no_overflow; auto.
-  unfold index_val. apply get_slot_intro; auto.
-  apply slot_valid_index; auto.
-Qed.
-
-Lemma set_slot_index:
-  forall fr idx v,
-  index_valid idx -> idx <> FI_link -> idx <> FI_retaddr ->
-  set_slot tf fr (type_of_index idx) (Int.signed (Int.repr (offset_of_index fe idx)))
-                 v (set_index_val idx v fr).
-Proof.
-  intros.  rewrite offset_of_index_no_overflow; auto.
-  apply set_slot_intro. 
-  apply slot_valid_index; auto.
-  unfold set_index_val. auto.
-Qed.
-
-(** ``Good variable'' properties for [index_val] and [set_index_val]. *)
-
-Lemma get_set_index_val_same:
-  forall fr idx v,
-  index_val idx (set_index_val idx v fr) = v.
-Proof.
-  intros. unfold index_val, set_index_val. apply update_same. 
-Qed.
-
-Lemma get_set_index_val_other:
-  forall fr idx idx' v,
-  index_valid idx -> index_valid idx' -> index_diff idx idx' ->
-  index_val idx' (set_index_val idx v fr) = index_val idx' fr.
-Proof.
-  intros. unfold index_val, set_index_val. apply update_other.
-  repeat rewrite typesize_typesize. 
-  exploit (offset_of_index_disj idx idx'); auto. omega.
-Qed.
-
-Lemma get_set_index_val_overlap:
-  forall ofs1 ty1 ofs2 ty2 v fr,
-  S (Outgoing ofs1 ty1) <> S (Outgoing ofs2 ty2) ->
-  Loc.overlap (S (Outgoing ofs1 ty1)) (S (Outgoing ofs2 ty2)) = true ->
-  index_val (FI_arg ofs2 ty2) (set_index_val (FI_arg ofs1 ty1) v fr) = Vundef.
-Proof.
-  intros. unfold index_val, set_index_val, offset_of_index, type_of_index.
-  assert (~(ofs1 + typesize ty1 <= ofs2 \/ ofs2 + typesize ty2 <= ofs1)).
-  destruct (orb_prop _ _ H0). apply Loc.overlap_aux_true_1. auto. 
-  apply Loc.overlap_aux_true_2. auto.
-  unfold update. 
-  destruct (zeq (fe_ofs_arg + 4 * ofs1 - fn_framesize tf)
-                (fe_ofs_arg + 4 * ofs2 - fn_framesize tf)).
-  destruct (typ_eq ty1 ty2). 
-  elim H. decEq. decEq. omega. auto.
-  auto.
-  repeat rewrite typesize_typesize.
-  rewrite zle_false. apply zle_false. omega. omega.
+  exploit offset_of_index_valid; eauto. intros [A B].
+  exploit offset_of_index_disj_stack_data_2; eauto. intros.
+  red; intros. apply H0. omega. omega.
 Qed.
 
-(** Accessing stack-based arguments in the caller's frame. *)
+Lemma store_index_succeeds:
+  forall m sp idx v,
+  index_valid idx ->
+  frame_perm_freeable m sp ->
+  exists m',
+  Mem.store (chunk_of_type (type_of_index idx)) m sp (offset_of_index fe idx) v = Some m'.
+Proof.
+  intros.
+  destruct (Mem.valid_access_store m (chunk_of_type (type_of_index idx)) sp (offset_of_index fe idx) v) as [m' ST].
+  constructor.
+  rewrite size_type_chunk. 
+  apply Mem.range_perm_implies with Freeable; auto with mem.
+  apply offset_of_index_perm; auto.
+  replace (align_chunk (chunk_of_type (type_of_index idx))) with 4.
+  apply offset_of_index_aligned; auto.
+  destruct (type_of_index idx); auto.
+  exists m'; auto.
+Qed.
 
-Definition get_parent_slot (cs: list stackframe) (ofs: Z) (ty: typ) (v: val) : Prop :=
-  get_slot (parent_function cs) (parent_frame cs)
-           ty (Int.signed (Int.repr (fe_ofs_arg + 4 * ofs))) v.
+Lemma store_stack_succeeds:
+  forall m sp idx v m',
+  index_valid idx ->
+  Mem.store (chunk_of_type (type_of_index idx)) m sp (offset_of_index fe idx) v = Some m' ->
+  store_stack m (Vptr sp Int.zero) (type_of_index idx) (Int.repr (offset_of_index fe idx)) v = Some m'.
+Proof.
+  intros. unfold store_stack, Mem.storev, Val.add.
+  rewrite Int.add_commut. rewrite Int.add_zero.
+  rewrite offset_of_index_no_overflow; auto.
+Qed.
 
-(** * Agreement between location sets and Mach environments *)
+(** A variant of [index_contains], up to a memory injection. *)
 
-(** The following [agree] predicate expresses semantic agreement between:
-- on the Linear side, the current location set [ls] and the location
-  set of the caller [ls0];
-- on the Mach side, a register set [rs], a frame [fr] and a call stack [cs].
-*)
+Definition index_contains_inj (j: meminj) (m: mem) (sp: block) (idx: frame_index) (v: val) : Prop :=
+  exists v', index_contains m sp idx v' /\ val_inject j v v'.
 
-Record agree (ls ls0: locset) (rs: regset) (fr: frame) (cs: list stackframe): Prop :=
-  mk_agree {
-    (** Machine registers have the same values on the Linear and Mach sides. *)
-    agree_reg:
-      forall r, ls (R r) = rs r;
+Lemma gss_index_contains_inj:
+  forall j idx m m' sp v v',
+  Mem.store (chunk_of_type (type_of_index idx)) m sp (offset_of_index fe idx) v' = Some m' ->
+  index_valid idx ->
+  Val.has_type v (type_of_index idx) ->
+  val_inject j v v' ->
+  index_contains_inj j m' sp idx v.
+Proof.
+  intros. exploit gss_index_contains_base; eauto. intros [v'' [A B]].
+  exists v''; split; auto.
+  inv H2; destruct (type_of_index idx); simpl in *; try contradiction; subst; auto.
+  econstructor; eauto.
+Qed.
 
-    (** Machine registers outside the bounds of the current function
-        have the same values they had at function entry.  In other terms,
-        these registers are never assigned. *)
+Lemma gso_index_contains_inj:
+  forall j idx m m' sp v idx' v',
+  Mem.store (chunk_of_type (type_of_index idx)) m sp (offset_of_index fe idx) v = Some m' ->
+  index_valid idx ->
+  index_contains_inj j m sp idx' v' ->
+  index_diff idx idx' ->
+  index_contains_inj j m' sp idx' v'.
+Proof.
+  intros. destruct H1 as [v'' [A B]]. exists v''; split; auto.
+  eapply gso_index_contains; eauto.
+Qed.
+
+Lemma store_other_index_contains_inj:
+  forall j chunk m b ofs v' m' sp idx v,
+  Mem.store chunk m b ofs v' = Some m' ->
+  b <> sp \/
+    (fe.(fe_stack_data) <= ofs /\ ofs + size_chunk chunk <= fe.(fe_stack_data) + f.(Linear.fn_stacksize)) ->
+  index_contains_inj j m sp idx v ->
+  index_contains_inj j m' sp idx v.
+Proof.
+  intros. destruct H1 as [v'' [A B]]. exists v''; split; auto.
+  eapply store_other_index_contains; eauto.
+Qed.
+
+Lemma index_contains_inj_incr:
+  forall j m sp idx v j',
+  index_contains_inj j m sp idx v ->
+  inject_incr j j' ->
+  index_contains_inj j' m sp idx v.
+Proof.
+  intros. destruct H as [v'' [A B]]. exists v''; split; auto. eauto. 
+Qed.
+
+Lemma index_contains_inj_undef:
+  forall j m sp idx,
+  index_valid idx ->
+  frame_perm_freeable m sp ->
+  index_contains_inj j m sp idx Vundef.
+Proof.
+  intros. 
+  exploit (Mem.valid_access_load m (chunk_of_type (type_of_index idx)) sp (offset_of_index fe idx)).
+  constructor. 
+  rewrite size_type_chunk.
+  apply Mem.range_perm_implies with Freeable; auto with mem.
+  apply offset_of_index_perm; auto. 
+  replace (align_chunk (chunk_of_type (type_of_index idx))) with 4. 
+  apply offset_of_index_aligned. destruct (type_of_index idx); auto.
+  intros [v C]. 
+  exists v; split; auto. constructor; auto. 
+Qed.
+
+Hint Resolve store_other_index_contains_inj index_contains_inj_incr: stacking.
+
+(** * Agreement between location sets and Mach states *)
+
+(** Agreement with Mach register states *)
+
+Definition agree_regs (j: meminj) (ls: locset) (rs: regset) : Prop :=
+  forall r, val_inject j (ls (R r)) (rs r).
+
+(** Agreement over data stored in memory *)
+
+Record agree_frame (j: meminj) (ls ls0: locset)
+                   (m: mem) (sp: block)
+                   (m': mem) (sp': block)
+                   (parent retaddr: val) : Prop :=
+  mk_agree_frame {
+
+    (** Unused registers have the same value as in the caller *)
     agree_unused_reg:
-      forall r, ~(mreg_within_bounds b r) -> rs r = ls0 (R r);
+       forall r, ~(mreg_within_bounds b r) -> ls (R r) = ls0 (R r);
 
     (** Local and outgoing stack slots (on the Linear side) have
         the same values as the one loaded from the current Mach frame 
@@ -425,244 +564,440 @@ Record agree (ls ls0: locset) (rs: regset) (fr: frame) (cs: list stackframe): Pr
     agree_locals:
       forall ofs ty, 
       slot_within_bounds f b (Local ofs ty) ->
-      ls (S (Local ofs ty)) = index_val (FI_local ofs ty) fr;
+      index_contains_inj j m' sp' (FI_local ofs ty) (ls (S (Local ofs ty)));
     agree_outgoing:
       forall ofs ty, 
       slot_within_bounds f b (Outgoing ofs ty) ->
-      ls (S (Outgoing ofs ty)) = index_val (FI_arg ofs ty) fr;
+      index_contains_inj j m' sp' (FI_arg ofs ty) (ls (S (Outgoing ofs ty)));
 
-    (** Incoming stack slots (on the Linear side) have
-        the same values as the one loaded from the parent Mach frame 
-        at the corresponding offsets. *)
+    (** Incoming stack slots have the same value as the
+        corresponding Outgoing stack slots in the caller *)
     agree_incoming:
-      forall ofs ty,
-      In (S (Incoming ofs ty)) (loc_parameters f.(Linear.fn_sig)) ->
-      get_parent_slot cs ofs ty (ls (S (Incoming ofs ty)));
+       forall ofs ty, 
+       In (S (Incoming ofs ty)) (loc_parameters f.(Linear.fn_sig)) ->
+       ls (S (Incoming ofs ty)) = ls0 (S (Outgoing ofs ty));
+
+    (** The back link and return address slots of the Mach frame contain
+        the [parent] and [retaddr] values, respectively. *)
+    agree_link:
+      index_contains m' sp' FI_link parent;
+    agree_retaddr:
+      index_contains m' sp' FI_retaddr retaddr;
 
     (** The areas of the frame reserved for saving used callee-save
         registers always contain the values that those registers had
-        on function entry. *)
+        in the caller. *)
     agree_saved_int:
       forall r,
       In r int_callee_save_regs ->
       index_int_callee_save r < b.(bound_int_callee_save) ->
-      index_val (FI_saved_int (index_int_callee_save r)) fr = ls0 (R r);
+      index_contains_inj j m' sp' (FI_saved_int (index_int_callee_save r)) (ls0 (R r));
     agree_saved_float:
       forall r,
       In r float_callee_save_regs ->
       index_float_callee_save r < b.(bound_float_callee_save) ->
-      index_val (FI_saved_float (index_float_callee_save r)) fr = ls0 (R r)
+      index_contains_inj j m' sp' (FI_saved_float (index_float_callee_save r)) (ls0 (R r));
+
+    (** Mapping between the Linear stack pointer and the Mach stack pointer *)
+    agree_inj:
+      j sp = Some(sp', fe.(fe_stack_data));
+    agree_inj_unique:
+      forall b delta, j b = Some(sp', delta) -> b = sp /\ delta = fe.(fe_stack_data);
+
+    (** The Linear and Mach stack pointers are valid *)
+    agree_valid_linear:
+      Mem.valid_block m sp;
+    agree_valid_mach:
+      Mem.valid_block m' sp';
+
+    (** Bounds of the Linear stack data block *)
+    agree_bounds:
+      Mem.bounds m sp = (0, f.(Linear.fn_stacksize));
+
+    (** Permissions on the frame part of the Mach stack block *)
+    agree_perm:
+      frame_perm_freeable m' sp';
+
+    (** Current locset is well-typed *)
+    agree_wt_ls:
+      wt_locset ls
   }.
 
-Hint Resolve agree_reg agree_unused_reg 
-             agree_locals agree_outgoing agree_incoming
-             agree_saved_int agree_saved_float: stacking.
+Hint Resolve agree_unused_reg agree_locals agree_outgoing agree_incoming
+             agree_link agree_retaddr agree_saved_int agree_saved_float
+             agree_valid_linear agree_valid_mach agree_perm
+             agree_wt_ls: stacking.
 
-(** Values of registers and register lists. *)
+(** Auxiliary predicate used at call points *)
 
-Lemma agree_eval_reg:
-  forall ls ls0 rs fr cs r,
-  agree ls ls0 rs fr cs -> rs r = ls (R r).
+Definition agree_callee_save (ls ls0: locset) : Prop :=
+  forall l,
+  match l with
+  | R r => In r int_callee_save_regs \/ In r float_callee_save_regs
+  | S s => True
+  end ->
+  ls l = ls0 l.
+
+(** ** Properties of [agree_regs]. *)
+
+(** Values of registers *)
+
+Lemma agree_reg:
+  forall j ls rs r,
+  agree_regs j ls rs -> val_inject j (ls (R r)) (rs r).
 Proof.
-  intros. symmetry. eauto with stacking.
+  intros. auto. 
 Qed.
 
-Lemma agree_eval_regs:
-  forall ls ls0 rs fr cs rl,
-  agree ls ls0 rs cs fr -> rs##rl = reglist ls rl.
+Lemma agree_reglist:
+  forall j ls rs rl,
+  agree_regs j ls rs -> val_list_inject j (reglist ls rl) (rs##rl).
 Proof.
   induction rl; simpl; intros.
-  auto. f_equal. eapply agree_eval_reg; eauto. auto.
+  auto. constructor. eauto with stacking. auto. 
 Qed.
 
-Hint Resolve agree_eval_reg agree_eval_regs: stacking.
+Hint Resolve agree_reg agree_reglist: stacking.
 
-(** Preservation of agreement under various assignments:
-  of machine registers, of local slots, of outgoing slots. *)
+(** Preservation under assignments of machine registers. *)
 
-Lemma agree_set_reg:
-  forall ls ls0 rs fr cs r v,
-  agree ls ls0 rs fr cs ->
-  mreg_within_bounds b r ->
-  agree (Locmap.set (R r) v ls) ls0 (Regmap.set r v rs) fr cs.
-Proof.
-  intros. constructor; eauto with stacking.
-  intros. case (mreg_eq r r0); intro.
-  subst r0. rewrite Locmap.gss; rewrite Regmap.gss; auto.
-  rewrite Locmap.gso. rewrite Regmap.gso. eauto with stacking.
-  auto. red. auto.
-  intros. rewrite Regmap.gso. eauto with stacking. 
-  red; intro; subst r0. contradiction.
-  intros. rewrite Locmap.gso. eauto with stacking. red. auto.
-  intros. rewrite Locmap.gso. eauto with stacking. red. auto.
-  intros. rewrite Locmap.gso. eauto with stacking. red. auto.
-Qed.
-
-Lemma agree_set_local:
-  forall ls ls0 rs fr cs v ofs ty,
-  agree ls ls0 rs fr cs ->
-  slot_within_bounds f b (Local ofs ty) ->
-  exists fr',
-    set_slot tf fr ty (Int.signed (Int.repr (offset_of_index fe (FI_local ofs ty)))) v fr' /\
-    agree (Locmap.set (S (Local ofs ty)) v ls) ls0 rs fr' cs.
+Lemma agree_regs_set_reg:
+  forall j ls rs r v v',
+  agree_regs j ls rs ->
+  val_inject j v v' ->
+  agree_regs j (Locmap.set (R r) v ls) (Regmap.set r v' rs).
 Proof.
-  intros.
-  exists (set_index_val (FI_local ofs ty) v fr); split.
-  set (idx := FI_local ofs ty). 
-  change ty with (type_of_index idx).
-  apply set_slot_index; unfold idx. auto with stacking. congruence. congruence.
-  constructor; eauto with stacking.
-  (* agree_reg *)
-  intros. rewrite Locmap.gso. eauto with stacking. red; auto.
-  (* agree_local *)
-  intros. case (slot_eq (Local ofs ty) (Local ofs0 ty0)); intro.
-  rewrite <- e. rewrite Locmap.gss. 
-  replace (FI_local ofs0 ty0) with (FI_local ofs ty).
-  symmetry. apply get_set_index_val_same. congruence.
-  assert (ofs <> ofs0 \/ ty <> ty0).
-    case (zeq ofs ofs0); intro. compare ty ty0; intro.
-    congruence. tauto.  tauto. 
-  rewrite Locmap.gso. rewrite get_set_index_val_other; eauto with stacking.
-  red. auto.
-  (* agree_outgoing *)
-  intros. rewrite Locmap.gso. rewrite get_set_index_val_other; eauto with stacking.
-  red; auto. red; auto.
-  (* agree_incoming *)
-  intros. rewrite Locmap.gso. eauto with stacking. red. auto.
-  (* agree_saved_int *)
-  intros. rewrite get_set_index_val_other; eauto with stacking.
-  red; auto.
-  (* agree_saved_float *)
-  intros. rewrite get_set_index_val_other; eauto with stacking.
-  red; auto.
+  intros; red; intros. 
+  unfold Regmap.set. destruct (RegEq.eq r0 r). subst r0. 
+  rewrite Locmap.gss; auto.
+  rewrite Locmap.gso; auto. red. auto.
 Qed.
 
-Lemma agree_set_outgoing:
-  forall ls ls0 rs fr cs v ofs ty,
-  agree ls ls0 rs fr cs ->
-  slot_within_bounds f b (Outgoing ofs ty) ->
-  exists fr',
-    set_slot tf fr ty (Int.signed (Int.repr (offset_of_index fe (FI_arg ofs ty)))) v fr' /\
-    agree (Locmap.set (S (Outgoing ofs ty)) v ls) ls0 rs fr' cs.
+Lemma agree_regs_undef_temps:
+  forall j ls rs,
+  agree_regs j ls rs ->
+  agree_regs j (LTL.undef_temps ls) (undef_temps rs).
+Proof.
+  unfold LTL.undef_temps, undef_temps.
+  change temporaries with (List.map R (int_temporaries ++ float_temporaries)).
+  generalize (int_temporaries ++ float_temporaries).
+  induction l; simpl; intros.
+  auto. 
+  apply IHl. apply agree_regs_set_reg; auto. 
+Qed.
+
+Lemma agree_regs_undef_op:
+  forall op j ls rs,
+  agree_regs j ls rs ->
+  agree_regs j (Linear.undef_op op ls) (undef_op (transl_op fe op) rs).
 Proof.
   intros.
-  exists (set_index_val (FI_arg ofs ty) v fr); split.
-  set (idx := FI_arg ofs ty). 
-  change ty with (type_of_index idx).
-  apply set_slot_index; unfold idx. auto with stacking. congruence. congruence.
-  constructor; eauto with stacking.
-  (* agree_reg *)
-  intros. rewrite Locmap.gso. eauto with stacking. red; auto.
-  (* agree_local *)
-  intros. rewrite Locmap.gso. rewrite get_set_index_val_other; eauto with stacking.
-  red; auto. red; auto.
-  (* agree_outgoing *)
-  intros. unfold Locmap.set. 
-  case (Loc.eq (S (Outgoing ofs ty)) (S (Outgoing ofs0 ty0))); intro.
-  (* same location *)
-  replace ofs0 with ofs by congruence. replace ty0 with ty by congruence.
-  symmetry. apply get_set_index_val_same.
-  (* overlapping locations *)
-  caseEq (Loc.overlap (S (Outgoing ofs ty)) (S (Outgoing ofs0 ty0))); intros.
-  symmetry. apply get_set_index_val_overlap; auto.
-  (* disjoint locations *)
-  rewrite get_set_index_val_other; eauto with stacking.
-  red. eapply Loc.overlap_aux_false_1; eauto.
-  (* agree_incoming *)
-  intros. rewrite Locmap.gso. eauto with stacking. red. auto.
-  (* saved ints *)
-  intros. rewrite get_set_index_val_other; eauto with stacking. red; auto.
-  (* saved floats *)
-  intros. rewrite get_set_index_val_other; eauto with stacking. red; auto.
+  generalize (agree_regs_undef_temps _ _ _ H). 
+  destruct op; simpl; auto.
 Qed.
 
-Lemma agree_undef_regs:
-  forall rl ls ls0 rs fr cs,
-  agree ls ls0 rs fr cs ->
-  (forall r, In r rl -> In (R r) temporaries) ->
-  agree (Locmap.undef (List.map R rl) ls) ls0 (undef_regs rl rs) fr cs.
+(** Preservation under assignment of stack slot *)
+
+Lemma agree_regs_set_slot:
+  forall j ls rs ss v,
+  agree_regs j ls rs ->
+  agree_regs j (Locmap.set (S ss) v ls) rs.
 Proof.
-  induction rl; intros; simpl.
+  intros; red; intros. rewrite Locmap.gso; auto. red. destruct ss; auto.
+Qed.
+
+(** Preservation by increasing memory injections *)
+
+Lemma agree_regs_inject_incr:
+  forall j ls rs j',
+  agree_regs j ls rs -> inject_incr j j' -> agree_regs j' ls rs.
+Proof.
+  intros; red; intros; eauto with stacking.
+Qed.
+
+(** Preservation at function entry. *)
+
+Lemma agree_regs_call_regs:
+  forall j ls rs,
+  agree_regs j ls rs ->
+  agree_regs j (call_regs ls) (undef_temps rs).
+Proof.
+  intros. 
+  assert (agree_regs j (LTL.undef_temps ls) (undef_temps rs)).
+    apply agree_regs_undef_temps; auto.
+  unfold call_regs; intros; red; intros.
+  destruct (in_dec Loc.eq (R r) temporaries).
   auto.
-  eapply IHrl; eauto. 
-  apply agree_set_reg; auto with coqlib.
-  assert (In (R a) temporaries) by auto with coqlib.
-  red. destruct (mreg_type a).
-  destruct (zlt (index_int_callee_save a) 0). 
-  generalize (bound_int_callee_save_pos b). omega. 
-  elim (int_callee_save_not_destroyed a). auto. apply index_int_callee_save_pos2; auto.
-  destruct (zlt (index_float_callee_save a) 0). 
-  generalize (bound_float_callee_save_pos b). omega. 
-  elim (float_callee_save_not_destroyed a). auto. apply index_float_callee_save_pos2; auto.
-  intros. apply H0. auto with coqlib.
-Qed.
-
-Lemma agree_undef_temps:
-  forall ls ls0 rs fr cs,
-  agree ls ls0 rs fr cs ->
-  agree (LTL.undef_temps ls) ls0 (Mach.undef_temps rs) fr cs.
-Proof.
-  intros. unfold undef_temps, LTL.undef_temps. 
+  generalize (H0 r). unfold LTL.undef_temps. rewrite Locmap.guo. auto.
+  apply Loc.reg_notin; auto.
+Qed.
+
+(** ** Properties of [agree_frame] *)
+
+(** Preservation under assignment of machine register. *)
+
+Lemma agree_frame_set_reg:
+  forall j ls ls0 m sp m' sp' parent ra r v,
+  agree_frame j ls ls0 m sp m' sp' parent ra ->
+  mreg_within_bounds b r ->
+  Val.has_type v (Loc.type (R r)) ->
+  agree_frame j (Locmap.set (R r) v ls) ls0 m sp m' sp' parent ra.
+Proof.
+  intros. inv H; constructor; auto; intros.
+  rewrite Locmap.gso. auto. red. intuition congruence.
+  rewrite Locmap.gso; auto. red; auto.
+  rewrite Locmap.gso; auto. red; auto.
+  rewrite Locmap.gso; auto. red; auto.
+  apply wt_setloc; auto.
+Qed.
+
+Remark temporary_within_bounds:
+  forall r, In (R r) temporaries -> mreg_within_bounds b r.
+Proof.
+  intros; red. destruct (mreg_type r). 
+  destruct (zlt (index_int_callee_save r) 0). 
+  generalize (bound_int_callee_save_pos b). omega.
+  exploit int_callee_save_not_destroyed. 
+  left. eauto with coqlib. apply index_int_callee_save_pos2; auto.
+  contradiction.
+  destruct (zlt (index_float_callee_save r) 0). 
+  generalize (bound_float_callee_save_pos b). omega.
+  exploit float_callee_save_not_destroyed. 
+  left. eauto with coqlib. apply index_float_callee_save_pos2; auto.
+  contradiction.
+Qed.
+
+Lemma agree_frame_undef_temps:
+  forall j ls ls0 m sp m' sp' parent ra,
+  agree_frame j ls ls0 m sp m' sp' parent ra ->
+  agree_frame j (LTL.undef_temps ls) ls0 m sp m' sp' parent ra.
+Proof.
+  intros until ra.
+  assert (forall regs ls,
+         incl (List.map R regs) temporaries ->
+         agree_frame j ls ls0 m sp m' sp' parent ra ->
+         agree_frame j (Locmap.undef (List.map R regs) ls) ls0 m sp m' sp' parent ra).
+  induction regs; simpl; intros.
+  auto.
+  apply IHregs; eauto with coqlib.
+  apply agree_frame_set_reg; auto. 
+  apply temporary_within_bounds; eauto with coqlib.
+  red; auto.
+  intros. unfold LTL.undef_temps.
   change temporaries with (List.map R (int_temporaries ++ float_temporaries)).
-  apply agree_undef_regs; auto.
+  apply H; auto. apply incl_refl. 
+Qed.
+
+Lemma agree_frame_undef_op:
+  forall j ls ls0 m sp m' sp' parent ra op,
+  agree_frame j ls ls0 m sp m' sp' parent ra ->
+  agree_frame j (Linear.undef_op op ls) ls0 m sp m' sp' parent ra.
+Proof.
   intros. 
-  change temporaries with (List.map R (int_temporaries ++ float_temporaries)).
-  apply List.in_map. auto. 
+  exploit agree_frame_undef_temps; eauto. destruct op; simpl; auto.
 Qed.
 
-Lemma agree_undef_op:
-  forall op env ls ls0 rs fr cs,
-  agree ls ls0 rs fr cs ->
-  agree (Linear.undef_op op ls) ls0 (Mach.undef_op (transl_op env op) rs) fr cs.
+(** Preservation by assignment to local slot *)
+
+Lemma agree_frame_set_local:
+  forall j ls ls0 m sp m' sp' parent retaddr ofs ty v v' m'',
+  agree_frame j ls ls0 m sp m' sp' parent retaddr ->
+  slot_within_bounds f b (Local ofs ty) ->
+  val_inject j v v' ->
+  Val.has_type v ty ->
+  Mem.store (chunk_of_type ty) m' sp' (offset_of_index fe (FI_local ofs ty)) v' = Some m'' ->
+  agree_frame j (Locmap.set (S (Local ofs ty)) v ls) ls0 m sp m'' sp' parent retaddr.
 Proof.
-  intros. exploit agree_undef_temps; eauto. intro. 
-  destruct op; simpl; auto.
+  intros. inv H. 
+  change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_local ofs ty))) in H3.
+  constructor; auto; intros.
+(* unused *)
+  rewrite Locmap.gso; auto. red; auto.
+(* local *)
+  unfold Locmap.set. simpl. destruct (Loc.eq (S (Local ofs ty)) (S (Local ofs0 ty0))).
+  inv e. eapply gss_index_contains_inj; eauto. 
+  eapply gso_index_contains_inj. eauto. simpl; auto. eauto with stacking.
+  simpl. destruct (zeq ofs ofs0); auto. destruct (typ_eq ty ty0); auto. congruence.
+(* outgoing *)
+  rewrite Locmap.gso. eapply gso_index_contains_inj; eauto with stacking.
+  simpl; auto. red; auto.
+(* incoming *)
+  rewrite Locmap.gso; auto. red; auto.
+(* parent *)
+  eapply gso_index_contains; eauto. red; auto.
+(* retaddr *)
+  eapply gso_index_contains; eauto. red; auto.
+(* int callee save *)
+  eapply gso_index_contains_inj; eauto. simpl; auto. 
+(* float callee save *)
+  eapply gso_index_contains_inj; eauto. simpl; auto.
+(* valid *)
+  eauto with mem.
+(* perm *)
+  red; intros. eapply Mem.perm_store_1; eauto.
+(* wt *)
+  apply wt_setloc; auto. 
+Qed.
+
+(** Preservation by assignment to outgoing slot *)
+
+Lemma agree_frame_set_outgoing:
+  forall j ls ls0 m sp m' sp' parent retaddr ofs ty v v' m'',
+  agree_frame j ls ls0 m sp m' sp' parent retaddr ->
+  slot_within_bounds f b (Outgoing ofs ty) ->
+  val_inject j v v' ->
+  Val.has_type v ty ->
+  Mem.store (chunk_of_type ty) m' sp' (offset_of_index fe (FI_arg ofs ty)) v' = Some m'' ->
+  agree_frame j (Locmap.set (S (Outgoing ofs ty)) v ls) ls0 m sp m'' sp' parent retaddr.
+Proof.
+  intros. inv H. 
+  change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_arg ofs ty))) in H3.
+  constructor; auto; intros.
+(* unused *)
+  rewrite Locmap.gso; auto. red; auto.
+(* local *)
+  rewrite Locmap.gso. eapply gso_index_contains_inj; eauto. simpl; auto. red; auto.
+(* outgoing *)
+  unfold Locmap.set. simpl. destruct (Loc.eq (S (Outgoing ofs ty)) (S (Outgoing ofs0 ty0))).
+  inv e. eapply gss_index_contains_inj; eauto.
+  case_eq (Loc.overlap_aux ty ofs ofs0 || Loc.overlap_aux ty0 ofs0 ofs); intros.
+  apply index_contains_inj_undef. auto.
+  red; intros. eapply Mem.perm_store_1; eauto.
+  eapply gso_index_contains_inj; eauto.
+  red. eapply Loc.overlap_aux_false_1; eauto.
+(* incoming *)
+  rewrite Locmap.gso; auto. red; auto.
+(* parent *)
+  eapply gso_index_contains; eauto with stacking. red; auto.
+(* retaddr *)
+  eapply gso_index_contains; eauto with stacking. red; auto.
+(* int callee save *)
+  eapply gso_index_contains_inj; eauto with stacking. simpl; auto. 
+(* float callee save *)
+  eapply gso_index_contains_inj; eauto with stacking. simpl; auto.
+(* valid *)
+  eauto with mem stacking.
+(* perm *)
+  red; intros. eapply Mem.perm_store_1; eauto.
+(* wt *)
+  apply wt_setloc; auto. 
 Qed.
 
-Lemma agree_undef_getparam:
-  forall ls ls0 rs fr cs,
-  agree ls ls0 rs fr cs ->
-  agree (Locmap.set (R IT1) Vundef ls) ls0 (rs#IT1 <- Vundef) fr cs.
+(** General invariance property with respect to memory changes. *)
+
+Lemma agree_frame_invariant:
+  forall j ls ls0 m sp m' sp' parent retaddr m1 m1',
+  agree_frame j ls ls0 m sp m' sp' parent retaddr ->
+  (Mem.valid_block m sp -> Mem.valid_block m1 sp) ->
+  (Mem.bounds m1 sp = Mem.bounds m sp) ->
+  (Mem.valid_block m' sp' -> Mem.valid_block m1' sp') ->
+  (forall chunk ofs v,
+     ofs + size_chunk chunk <= fe.(fe_stack_data) \/
+     fe.(fe_stack_data) + f.(Linear.fn_stacksize) <= ofs ->
+     Mem.load chunk m' sp' ofs = Some v ->
+     Mem.load chunk m1' sp' ofs = Some v) ->
+  (forall ofs p,
+     ofs < fe.(fe_stack_data) \/ fe.(fe_stack_data) + f.(Linear.fn_stacksize) <= ofs ->
+     Mem.perm m' sp' ofs p -> Mem.perm m1' sp' ofs p) ->
+  agree_frame j ls ls0 m1 sp m1' sp' parent retaddr.
 Proof.
-  intros. exploit (agree_undef_regs (IT1 :: nil)); eauto.
-  simpl; intros. intuition congruence. 
+  intros.
+  assert (IC: forall idx v,
+              index_contains m' sp' idx v -> index_contains m1' sp' idx v).
+    intros. inv H5.
+    exploit offset_of_index_disj_stack_data_2; eauto. intros. 
+    constructor; eauto. apply H3; auto. rewrite size_type_chunk; auto.
+  assert (ICI: forall idx v,
+              index_contains_inj j m' sp' idx v -> index_contains_inj j m1' sp' idx v).
+    intros. destruct H5 as [v' [A B]]. exists v'; split; auto. 
+  inv H; constructor; auto; intros.
+  rewrite H1; auto.
+  red; intros. apply H4; auto.
 Qed.
 
-Lemma agree_return_regs:
-  forall ls ls0 rs fr cs rs',
-  agree ls ls0 rs fr cs ->
-  (forall r,
-    ~In r int_callee_save_regs -> ~In r float_callee_save_regs ->
-    rs' r = rs r) ->
-  (forall r,
-    In r int_callee_save_regs \/ In r float_callee_save_regs ->
-    rs' r = ls0 (R r)) ->
-  (forall r, return_regs ls0 ls (R r) = rs' r).
+(** A variant of the latter, for use with external calls *)
+
+Lemma agree_frame_extcall_invariant:
+  forall j ls ls0 m sp m' sp' parent retaddr m1 m1',
+  agree_frame j ls ls0 m sp m' sp' parent retaddr ->
+  (Mem.valid_block m sp -> Mem.valid_block m1 sp) ->
+  (Mem.bounds m1 sp = Mem.bounds m sp) ->
+  (Mem.valid_block m' sp' -> Mem.valid_block m1' sp') ->
+  mem_unchanged_on (loc_out_of_reach j m) m' m1' ->
+  agree_frame j ls ls0 m1 sp m1' sp' parent retaddr.
 Proof.
-  intros; unfold return_regs.
-  case (In_dec Loc.eq (R r) temporaries); intro.
-  rewrite H0. eapply agree_reg; eauto. 
-    apply int_callee_save_not_destroyed; auto.
-    apply float_callee_save_not_destroyed; auto.
-  case (In_dec Loc.eq (R r) destroyed_at_call); intro.
-  rewrite H0. eapply agree_reg; eauto.
-    apply int_callee_save_not_destroyed; auto.
-    apply float_callee_save_not_destroyed; auto.
-  symmetry; apply H1.
-  generalize (register_classification r); tauto.
+  intros.
+  assert (REACH: forall ofs,
+     ofs < fe.(fe_stack_data) \/ fe.(fe_stack_data) + f.(Linear.fn_stacksize) <= ofs ->
+    loc_out_of_reach j m sp' ofs).
+  intros; red; intros. exploit agree_inj_unique; eauto. intros [EQ1 EQ2]; subst.
+  rewrite (agree_bounds _ _ _ _ _ _ _ _ _ H). unfold fst, snd. omega.
+  eapply agree_frame_invariant; eauto.
+  intros. apply H3. intros. apply REACH. omega. auto. 
+  intros. apply H3; auto. 
 Qed.
 
-(** Agreement over callee-save registers and stack locations *)
+(** Preservation by parallel stores in the Linear and Mach codes *)
 
-Definition agree_callee_save (ls1 ls2: locset) : Prop :=
-  forall l,
-  match l with
-  | R r => In r int_callee_save_regs \/ In r float_callee_save_regs
-  | S s => True
-  end ->
-  ls2 l = ls1 l.
+Lemma agree_frame_parallel_stores:
+  forall j ls ls0 m sp m' sp' parent retaddr chunk addr addr' v v' m1 m1',
+  agree_frame j ls ls0 m sp m' sp' parent retaddr ->
+  Mem.inject j m m' ->
+  val_inject j addr addr' ->
+  Mem.storev chunk m addr v = Some m1 ->
+  Mem.storev chunk m' addr' v' = Some m1' ->
+  agree_frame j ls ls0 m1 sp m1' sp' parent retaddr.
+Proof.
+Opaque Int.add.
+  intros until m1'. intros AG MINJ VINJ STORE1 STORE2.
+  inv VINJ; simpl in *; try discriminate.
+  eapply agree_frame_invariant; eauto.
+  eauto with mem.
+  eapply Mem.bounds_store; eauto. 
+  eauto with mem.
+  intros. rewrite <- H1. eapply Mem.load_store_other; eauto. 
+    destruct (zeq sp' b2); auto.
+    subst b2. right.
+    exploit agree_inj_unique; eauto. intros [P Q]. subst b1 delta.
+    exploit Mem.store_valid_access_3. eexact STORE1. intros [A B].
+    exploit Mem.range_perm_in_bounds. eexact A. generalize (size_chunk_pos chunk); omega.
+    rewrite (agree_bounds _ _ _ _ _ _ _ _ _ AG). unfold fst,snd. intros [C D].
+    rewrite shifted_stack_offset_no_overflow. omega.
+    generalize (size_chunk_pos chunk); omega. 
+  intros; eauto with mem.
+Qed.
+
+(** Preservation by increasing memory injections (allocations and external calls) *)
 
-Remark mreg_not_within_bounds:
+Lemma agree_frame_inject_incr:
+  forall j ls ls0 m sp m' sp' parent retaddr m1 m1' j',
+  agree_frame j ls ls0 m sp m' sp' parent retaddr ->
+  inject_incr j j' -> inject_separated j j' m1 m1' ->
+  Mem.valid_block m1' sp' ->
+  agree_frame j' ls ls0 m sp m' sp' parent retaddr.
+Proof.
+  intros. inv H. constructor; auto; intros; eauto with stacking.
+  case_eq (j b0). 
+  intros [b' delta'] EQ. rewrite (H0 _ _ _ EQ) in H. inv H. auto. 
+  intros EQ. exploit H1. eauto. eauto. intros [A B]. contradiction.
+Qed.
+
+Remark inject_alloc_separated:
+  forall j m1 m2 j' b1 b2 delta,
+  inject_incr j j' ->
+  j' b1 = Some(b2, delta) ->
+  (forall b, b <> b1 -> j' b = j b) ->
+  ~Mem.valid_block m1 b1 -> ~Mem.valid_block m2 b2 ->
+  inject_separated j j' m1 m2.
+Proof.
+  intros. red. intros.
+  destruct (eq_block b0 b1). subst b0. rewrite H0 in H5; inv H5. tauto.
+  rewrite H1 in H5. congruence. auto.
+Qed.
+
+(** Preservation at return points (when [ls] is changed but not [ls0]). *)
+
+Remark mreg_not_within_bounds_callee_save:
   forall r,
   ~mreg_within_bounds b r -> In r int_callee_save_regs \/ In r float_callee_save_regs.
 Proof.
@@ -674,19 +1009,38 @@ Proof.
   generalize (bound_float_callee_save_pos b). omega.
 Qed.
 
-Lemma agree_callee_save_agree:
-  forall ls ls1 ls2 rs fr cs,
-  agree ls ls1 rs fr cs ->
-  agree_callee_save ls1 ls2 ->
-  agree ls ls2 rs fr cs.
+Lemma agree_frame_return:
+  forall j ls ls0 m sp m' sp' parent retaddr ls',
+  agree_frame j ls ls0 m sp m' sp' parent retaddr ->
+  agree_callee_save ls' ls ->
+  wt_locset ls' ->
+  agree_frame j ls' ls0 m sp m' sp' parent retaddr.
 Proof.
-  intros. inv H. constructor; auto.
-  intros. rewrite agree_unused_reg0; auto.
-  symmetry. apply H0. apply mreg_not_within_bounds; auto.
-  intros. rewrite (H0 (R r)); auto. 
-  intros. rewrite (H0 (R r)); auto. 
+  intros. red in H0. inv H; constructor; auto; intros.
+  rewrite H0; auto. apply mreg_not_within_bounds_callee_save; auto. 
+  rewrite H0; auto.
+  rewrite H0; auto.
+  rewrite H0; auto.
 Qed.
 
+(** Preservation at tailcalls (when [ls0] is changed but not [ls]). *)
+
+Lemma agree_frame_tailcall:
+  forall j ls ls0 m sp m' sp' parent retaddr ls0',
+  agree_frame j ls ls0 m sp m' sp' parent retaddr ->
+  agree_callee_save ls0 ls0' ->
+  agree_frame j ls ls0' m sp m' sp' parent retaddr.
+Proof.
+  intros. red in H0. inv H; constructor; auto; intros.
+  rewrite <- H0; auto. apply mreg_not_within_bounds_callee_save; auto. 
+  rewrite <- H0; auto.
+  rewrite <- H0; auto.
+  rewrite <- H0; auto.
+Qed.
+
+
+(** Properties of [agree_callee_save]. *)
+
 Lemma agree_callee_save_return_regs:
   forall ls1 ls2,
   agree_callee_save (return_regs ls1 ls2) ls1.
@@ -705,33 +1059,11 @@ Lemma agree_callee_save_set_result:
   agree_callee_save ls1 ls2 ->
   agree_callee_save (Locmap.set (R (loc_result sg)) v ls1) ls2.
 Proof.
-  intros; red; intros. rewrite H; auto. 
-  symmetry; apply Locmap.gso. destruct l; simpl; auto.
+  intros; red; intros. rewrite <- H; auto. 
+  apply Locmap.gso. destruct l; simpl; auto.
   red; intro. subst m. elim (loc_result_not_callee_save _ H0).
 Qed.
 
-(** A variant of [agree] used for return frames. *)
-
-Definition agree_frame (ls ls0: locset) (fr: frame) (cs: list stackframe): Prop :=
-  exists rs, agree ls ls0 rs fr cs.
-
-Lemma agree_frame_agree:
-  forall ls1 ls2 rs fr cs ls0,
-  agree_frame ls1 ls0 fr cs ->
-  agree_callee_save ls2 ls1 ->
-  (forall r, rs r = ls2 (R r)) ->
-  agree ls2 ls0 rs fr cs.
-Proof.
-  intros. destruct H as [rs' AG]. inv AG.
-  constructor; auto.
-  intros. rewrite <- agree_unused_reg0; auto.
-  rewrite <- agree_reg0. rewrite H1. symmetry; apply H0.
-  apply mreg_not_within_bounds; auto.
-  intros. rewrite <- H0; auto.
-  intros. rewrite <- H0; auto.
-  intros. rewrite <- H0; auto.
-Qed.
-
 (** * Correctness of saving and restoring of callee-save registers *)
 
 (** The following lemmas show the correctness of the register saving
@@ -745,17 +1077,35 @@ Variable bound: frame_env -> Z.
 Variable number: mreg -> Z.
 Variable mkindex: Z -> frame_index.
 Variable ty: typ.
-Variable sp: val.
+Variable j: meminj.
+Variable cs: list stackframe.
+Variable fb: block.
+Variable sp: block.
 Variable csregs: list mreg.
+Variable ls: locset.
+Variable rs: regset.
+
+Inductive stores_in_frame: mem -> mem -> Prop :=
+  | stores_in_frame_refl: forall m,
+      stores_in_frame m m
+  | stores_in_frame_step: forall m1 chunk ofs v m2 m3,
+       ofs + size_chunk chunk <= fe.(fe_stack_data)
+       \/ fe.(fe_stack_data) + f.(Linear.fn_stacksize) <= ofs ->
+       Mem.store chunk m1 sp ofs v = Some m2 ->
+       stores_in_frame m2 m3 ->
+       stores_in_frame m1 m3.
+
+Remark stores_in_frame_trans:
+  forall m1 m2, stores_in_frame m1 m2 ->
+  forall m3, stores_in_frame m2 m3 -> stores_in_frame m1 m3.
+Proof.
+  induction 1; intros. auto. econstructor; eauto.
+Qed.
 
 Hypothesis number_inj: 
   forall r1 r2, In r1 csregs -> In r2 csregs -> r1 <> r2 -> number r1 <> number r2.
 Hypothesis mkindex_valid:
   forall r, In r csregs -> number r < bound fe -> index_valid (mkindex (number r)).
-Hypothesis mkindex_not_link:
-  forall z, mkindex z <> FI_link.
-Hypothesis mkindex_not_retaddr:
-  forall z, mkindex z <> FI_retaddr.
 Hypothesis mkindex_typ:
   forall z, type_of_index (mkindex z) = ty.
 Hypothesis mkindex_inj:
@@ -763,170 +1113,350 @@ Hypothesis mkindex_inj:
 Hypothesis mkindex_diff:
   forall r idx,
   idx <> mkindex (number r) -> index_diff (mkindex (number r)) idx.
+Hypothesis csregs_typ:
+  forall r, In r csregs -> mreg_type r = ty.
+
+Hypothesis agree: agree_regs j ls rs.
+Hypothesis wt_ls: wt_locset ls.
 
 Lemma save_callee_save_regs_correct:
-  forall l k rs fr m,
+  forall l k m,
   incl l csregs ->
   list_norepet l ->
-  exists fr',
+  frame_perm_freeable m sp ->
+  exists m',
     star step tge 
-       (State stack tf sp
-         (save_callee_save_regs bound number mkindex ty fe l k) rs fr m)
-    E0 (State stack tf sp k rs fr' m)
+       (State cs fb (Vptr sp Int.zero)
+         (save_callee_save_regs bound number mkindex ty fe l k) rs m)
+    E0 (State cs fb (Vptr sp Int.zero) k rs m')
   /\ (forall r,
        In r l -> number r < bound fe ->
-       index_val (mkindex (number r)) fr' = rs r)
-  /\ (forall idx,
+       index_contains_inj j m' sp (mkindex (number r)) (ls (R r)))
+  /\ (forall idx v,
        index_valid idx ->
        (forall r,
          In r l -> number r < bound fe -> idx <> mkindex (number r)) ->
-       index_val idx fr' = index_val idx fr).
+       index_contains m sp idx v ->
+       index_contains m' sp idx v)
+  /\ stores_in_frame m m'
+  /\ frame_perm_freeable m' sp.
 Proof.
   induction l; intros; simpl save_callee_save_regs.
   (* base case *)
-  exists fr. split. apply star_refl.
-  split. intros. elim H1.
+  exists m. split. apply star_refl. 
+  split. intros. elim H2.
+  split. auto.
+  split. constructor.
   auto.
   (* inductive case *)
-  set (k1 := save_callee_save_regs bound number mkindex ty fe l k).
   assert (R1: incl l csregs). eauto with coqlib.
   assert (R2: list_norepet l). inversion H0; auto.
   unfold save_callee_save_reg.
   destruct (zlt (number a) (bound fe)).
   (* a store takes place *)
-  set (fr1 := set_index_val (mkindex (number a)) (rs a) fr).
-  exploit (IHl k rs fr1 m); auto. 
-  fold k1. intros [fr' [A [B C]]].
-  exists fr'.
-  split. eapply star_left. 
-  apply exec_Msetstack. instantiate (1 := fr1). 
-  unfold fr1. rewrite <- (mkindex_typ (number a)).
-  eapply set_slot_index; eauto with coqlib.
-  eexact A.
+  exploit store_index_succeeds. apply (mkindex_valid a); auto with coqlib. 
+  eauto. instantiate (1 := rs a). intros [m1 ST].
+  exploit (IHl k m1).  auto with coqlib. auto. 
+  red; eauto with mem.
+  intros [m' [A [B [C [D E]]]]].
+  exists m'. 
+  split. eapply star_left; eauto. constructor. 
+  rewrite <- (mkindex_typ (number a)). 
+  apply store_stack_succeeds; auto with coqlib.
   traceEq.
-  split. intros. simpl in H1. destruct H1. subst r.
-    rewrite C. unfold fr1. apply get_set_index_val_same.
-    apply mkindex_valid; auto with coqlib.
-    intros. apply mkindex_inj. apply number_inj; auto with coqlib.
-    inversion H0. congruence.
-    apply B; auto.
-  intros. rewrite C; auto with coqlib. 
-    unfold fr1. apply get_set_index_val_other; auto with coqlib. 
+  split; intros.
+  simpl in H2. destruct (mreg_eq a r). subst r.
+  assert (index_contains_inj j m1 sp (mkindex (number a)) (ls (R a))).
+    eapply gss_index_contains_inj; eauto.
+    rewrite mkindex_typ. rewrite <- (csregs_typ a). apply wt_ls. auto with coqlib.
+  destruct H4 as [v' [P Q]].
+  exists v'; split; auto. apply C; auto. 
+  intros. apply mkindex_inj. apply number_inj; auto with coqlib. 
+  inv H0. intuition congruence.
+  apply B; auto with coqlib. 
+  intuition congruence.
+  split. intros.
+  apply C; auto with coqlib.
+  eapply gso_index_contains; eauto with coqlib. 
+  split. econstructor; eauto.
+  rewrite size_type_chunk. apply offset_of_index_disj_stack_data_2; eauto with coqlib.
+  auto.
   (* no store takes place *)
-  exploit (IHl k rs fr m); auto. intros [fr' [A [B C]]].
-  exists fr'.
-  split. exact A.
-  split. intros. simpl in H1; destruct H1. subst r. omegaContradiction.
-    apply B; auto. 
-  intros. apply C; auto with coqlib.
+  exploit (IHl k m); auto with coqlib. 
+  intros [m' [A [B [C [D E]]]]].
+  exists m'; intuition. 
+  simpl in H2. destruct H2. subst r. omegaContradiction. apply B; auto.
+  apply C; auto with coqlib.
+  intros. eapply H3; eauto. auto with coqlib.
 Qed.
 
-End SAVE_CALLEE_SAVE. 
+End SAVE_CALLEE_SAVE.
 
-Lemma save_callee_save_int_correct:
-  forall k sp rs fr m,
-  exists fr',
+Lemma save_callee_save_correct:
+  forall j ls rs sp cs fb k m,
+  agree_regs j ls rs -> wt_locset ls ->
+  frame_perm_freeable m sp ->
+  exists m',
     star step tge 
-       (State stack tf sp
-         (save_callee_save_int fe k) rs fr m)
-    E0 (State stack tf sp k rs fr' m)
+       (State cs fb (Vptr sp Int.zero) (save_callee_save fe k) rs m)
+    E0 (State cs fb (Vptr sp Int.zero) k rs m')
+  /\ (forall r,
+       In r int_callee_save_regs -> index_int_callee_save r < b.(bound_int_callee_save) ->
+       index_contains_inj j m' sp (FI_saved_int (index_int_callee_save r)) (ls (R r)))
   /\ (forall r,
-       In r int_callee_save_regs ->
-       index_int_callee_save r < bound_int_callee_save b ->
-       index_val (FI_saved_int (index_int_callee_save r)) fr' = rs r)
-  /\ (forall idx,
+       In r float_callee_save_regs -> index_float_callee_save r < b.(bound_float_callee_save) ->
+       index_contains_inj j m' sp (FI_saved_float (index_float_callee_save r)) (ls (R r)))
+  /\ (forall idx v,
        index_valid idx ->
-       match idx with FI_saved_int _ => False | _ => True end ->
-       index_val idx fr' = index_val idx fr).
+       match idx with FI_saved_int _ => False | FI_saved_float _ => False | _ => True end ->
+       index_contains m sp idx v ->
+       index_contains m' sp idx v)
+  /\ stores_in_frame sp m m'
+  /\ frame_perm_freeable m' sp.
 Proof.
   intros.
-  exploit (save_callee_save_regs_correct fe_num_int_callee_save index_int_callee_save FI_saved_int
-                                         Tint sp int_callee_save_regs).
-  exact index_int_callee_save_inj.
-  intros. red. split; auto. generalize (index_int_callee_save_pos r H). omega.
-  intro; congruence.
-  intro; congruence.
+  exploit (save_callee_save_regs_correct 
+             fe_num_int_callee_save
+             index_int_callee_save
+             FI_saved_int Tint
+             j cs fb sp int_callee_save_regs ls rs).
+  intros. apply index_int_callee_save_inj; auto. 
+  intros. simpl. split. apply Zge_le. apply index_int_callee_save_pos; auto. assumption.
   auto.
   intros; congruence.
-  intros until idx. destruct idx; simpl; auto. congruence.
-  apply incl_refl.
+  intros; simpl. destruct idx; auto. congruence.
+  intros. apply int_callee_save_type. auto.
+  auto.
+  auto.
+  apply incl_refl. 
   apply int_callee_save_norepet.
-  intros [fr' [A [B C]]]. 
-  exists fr'; intuition. unfold save_callee_save_int; eauto. 
-  apply C. auto. intros; subst idx. auto.
+  eauto.
+  intros [m1 [A [B [C [D E]]]]].
+  exploit (save_callee_save_regs_correct 
+             fe_num_float_callee_save
+             index_float_callee_save
+             FI_saved_float Tfloat
+             j cs fb sp float_callee_save_regs ls rs).
+  intros. apply index_float_callee_save_inj; auto. 
+  intros. simpl. split. apply Zge_le. apply index_float_callee_save_pos; auto. assumption.
+  simpl; auto.
+  intros; congruence.
+  intros; simpl. destruct idx; auto. congruence.
+  intros. apply float_callee_save_type. auto.
+  auto. 
+  auto.
+  apply incl_refl. 
+  apply float_callee_save_norepet.
+  eexact E.
+  intros [m2 [P [Q [R [S T]]]]].
+  exists m2.
+  split. unfold save_callee_save, save_callee_save_int, save_callee_save_float.
+  eapply star_trans; eauto. 
+  split; intros.
+  destruct (B r H2 H3) as [v [X Y]]. exists v; split; auto. apply R.
+  apply index_saved_int_valid; auto. 
+  intros. congruence.
+  auto.
+  split. intros. apply Q; auto.
+  split. intros. apply R. auto.
+  intros. destruct idx; contradiction||congruence.
+  apply C. auto. 
+  intros. destruct idx; contradiction||congruence.
+  auto.
+  split. eapply stores_in_frame_trans; eauto.
+  auto.
 Qed.
 
-Lemma save_callee_save_float_correct:
-  forall k sp rs fr m,
-  exists fr',
-    star step tge 
-       (State stack tf sp
-         (save_callee_save_float fe k) rs fr m)
-    E0 (State stack tf sp k rs fr' m)
-  /\ (forall r,
-       In r float_callee_save_regs ->
-       index_float_callee_save r < bound_float_callee_save b ->
-       index_val (FI_saved_float (index_float_callee_save r)) fr' = rs r)
-  /\ (forall idx,
-       index_valid idx ->
-       match idx with FI_saved_float _ => False | _ => True end ->
-       index_val idx fr' = index_val idx fr).
+(** Properties of sequences of stores in the frame. *)
+
+Lemma stores_in_frame_inject:
+  forall j sp sp' m,
+  (forall b delta, j b = Some(sp', delta) -> b = sp /\ delta = fe.(fe_stack_data)) ->
+  Mem.bounds m sp = (0, f.(Linear.fn_stacksize)) ->
+  forall m1 m2, stores_in_frame sp' m1 m2 -> Mem.inject j m m1 -> Mem.inject j m m2.
 Proof.
-  intros.
-  exploit (save_callee_save_regs_correct fe_num_float_callee_save index_float_callee_save FI_saved_float
-                                         Tfloat sp float_callee_save_regs).
-  exact index_float_callee_save_inj.
-  intros. red. split; auto. generalize (index_float_callee_save_pos r H). omega.
-  intro; congruence.
-  intro; congruence.
+  induction 3; intros.
   auto.
-  intros; congruence.
-  intros until idx. destruct idx; simpl; auto. congruence.
-  apply incl_refl.
-  apply float_callee_save_norepet. eauto.
-  intros [fr' [A [B C]]].
-  exists fr'. split. unfold save_callee_save_float; eauto.
-  split. auto. 
-  intros. apply C. auto. intros; subst. red; intros; subst idx. contradiction. 
+  apply IHstores_in_frame.
+  intros. eapply Mem.store_outside_inject; eauto.
+  intros. exploit H; eauto. intros [A B]; subst.
+  rewrite H0; unfold fst, snd. omega.
 Qed.
 
-Lemma save_callee_save_correct:
-  forall sp k rs m ls cs,
-  (forall r, rs r = ls (R r)) ->
-  (forall ofs ty,
-     In (S (Outgoing ofs ty)) (loc_arguments f.(Linear.fn_sig)) ->
-     get_parent_slot cs ofs ty (ls (S (Outgoing ofs ty)))) ->
-  exists fr',
-    star step tge
-       (State stack tf sp (save_callee_save fe k) rs empty_frame m)
-    E0 (State stack tf sp k rs fr' m)
-  /\ agree (call_regs ls) ls rs fr' cs.
-Proof.
-  intros. unfold save_callee_save.
-  exploit save_callee_save_int_correct; eauto. 
-  intros [fr1 [A1 [B1 C1]]].
-  exploit save_callee_save_float_correct. 
-  intros [fr2 [A2 [B2 C2]]].
-  exists fr2.
-  split. eapply star_trans. eexact A1. eexact A2. traceEq.
-  constructor; unfold call_regs; auto.
-  (* agree_local *)
-  intros. rewrite C2; auto with stacking. 
-  rewrite C1; auto with stacking. 
-  (* agree_outgoing *)
-  intros. rewrite C2; auto with stacking. 
-  rewrite C1; auto with stacking.
-  (* agree_incoming *)
-  intros. apply H0. unfold loc_parameters in H1.
-  exploit list_in_map_inv; eauto. intros [l [A B]].
-  exploit loc_arguments_acceptable; eauto. intro C.
-  destruct l; simpl in A. discriminate.
-  simpl in C. destruct s; try contradiction. inv A. auto.
-  (* agree_saved_int *)
-  intros. rewrite C2; auto with stacking.
-  rewrite B1; auto with stacking. 
-  (* agree_saved_float *)
-  intros. rewrite B2; auto with stacking. 
+Lemma stores_in_frame_valid:
+  forall b sp m m', stores_in_frame sp m m' -> Mem.valid_block m b -> Mem.valid_block m' b.
+Proof.
+  induction 1; intros. auto. apply IHstores_in_frame. eauto with mem.
+Qed.
+
+Lemma stores_in_frame_perm:
+  forall b ofs p sp m m', stores_in_frame sp m m' -> Mem.perm m b ofs p -> Mem.perm m' b ofs p.
+Proof.
+  induction 1; intros. auto. apply IHstores_in_frame. eauto with mem.
+Qed.
+
+Lemma stores_in_frame_contents:
+  forall chunk b ofs sp, b < sp ->
+  forall m m', stores_in_frame sp m m' -> 
+  Mem.load chunk m' b ofs = Mem.load chunk m b ofs.
+Proof.
+  induction 2. auto. 
+  rewrite IHstores_in_frame. eapply Mem.load_store_other; eauto.
+  left; unfold block; omega.
+Qed.
+
+(** As a corollary of the previous lemmas, we obtain the following
+  correctness theorem for the execution of a function prologue
+  (allocation of the frame + saving of the link and return address +
+  saving of the used callee-save registers). *)
+
+Lemma function_prologue_correct:
+  forall j ls ls0 rs m1 m1' m2 sp parent ra cs fb k,
+  agree_regs j ls rs ->
+  agree_callee_save ls ls0 ->
+  wt_locset ls ->
+  Mem.inject j m1 m1' ->
+  Mem.alloc m1 0 f.(Linear.fn_stacksize) = (m2, sp) ->
+  Val.has_type parent Tint -> Val.has_type ra Tint ->
+  exists j', exists m2', exists sp', exists m3', exists m4', exists m5',
+     Mem.alloc m1' 0 tf.(fn_stacksize) = (m2', sp')
+  /\ store_stack m2' (Vptr sp' Int.zero) Tint tf.(fn_link_ofs) parent = Some m3'
+  /\ store_stack m3' (Vptr sp' Int.zero) Tint tf.(fn_retaddr_ofs) ra = Some m4'
+  /\ star step tge 
+         (State cs fb (Vptr sp' Int.zero) (save_callee_save fe k) (undef_temps rs) m4')
+      E0 (State cs fb (Vptr sp' Int.zero) k (undef_temps rs) m5')
+  /\ agree_regs j' (call_regs ls) (undef_temps rs)
+  /\ agree_frame j' (call_regs ls) ls0 m2 sp m5' sp' parent ra
+  /\ inject_incr j j'
+  /\ inject_separated j j' m1 m1'
+  /\ Mem.inject j' m2 m5'
+  /\ stores_in_frame sp' m2' m5'.
+Proof.
+  intros until k; intros AGREGS AGCS WTREGS INJ1 ALLOC TYPAR TYRA.
+  rewrite unfold_transf_function.
+  unfold fn_stacksize, fn_link_ofs, fn_retaddr_ofs.
+  (* Allocation step *)
+  caseEq (Mem.alloc m1' 0 (fe_size fe)). intros m2' sp' ALLOC'.
+  exploit Mem.alloc_left_mapped_inject.
+    eapply Mem.alloc_right_inject; eauto.
+    eauto.
+    instantiate (1 := sp'). eauto with mem.
+    instantiate (1 := fe_stack_data fe).
+    generalize stack_data_offset_valid (bound_stack_data_pos b) size_no_overflow; omega.
+    right. rewrite (Mem.bounds_alloc_same _ _ _ _ _ ALLOC'). unfold fst, snd.
+    split. omega. apply size_no_overflow.
+    intros. apply Mem.perm_implies with Freeable; auto with mem. 
+    eapply Mem.perm_alloc_2; eauto.
+    generalize stack_data_offset_valid bound_stack_data_stacksize; omega.
+    red. intros. apply Zdivides_trans with 4. 
+    destruct chunk; simpl; auto with align_4.
+    apply fe_stack_data_aligned.
+    intros.
+      assert (Mem.valid_block m1' sp'). eapply Mem.valid_block_inject_2; eauto.
+      assert (~Mem.valid_block m1' sp') by eauto with mem.
+      contradiction.
+  intros [j' [INJ2 [INCR [MAP1 MAP2]]]].
+  assert (PERM: frame_perm_freeable m2' sp').
+    red; intros. eapply Mem.perm_alloc_2; eauto.
+  (* Store of parent *)
+  exploit (store_index_succeeds m2' sp' FI_link parent). red; auto. auto. 
+  intros [m3' STORE2].
+  (* Store of retaddr *)
+  exploit (store_index_succeeds m3' sp' FI_retaddr ra). red; auto. red; eauto with mem.
+  intros [m4' STORE3].
+  (* Saving callee-save registers *)
+  assert (PERM4: frame_perm_freeable m4' sp').
+    red; intros. eauto with mem. 
+  exploit save_callee_save_correct. 
+    apply agree_regs_undef_temps.
+    eapply agree_regs_inject_incr; eauto.
+    apply wt_undef_temps. auto.
+    eexact PERM4.
+  intros [m5' [STEPS [ICS [FCS [OTHERS [STORES PERM5]]]]]].
+  (* stores in frames *)
+  assert (SIF: stores_in_frame sp' m2' m5').
+    econstructor; eauto. 
+    rewrite size_type_chunk. apply offset_of_index_disj_stack_data_2; auto. red; auto.
+    econstructor; eauto.
+    rewrite size_type_chunk. apply offset_of_index_disj_stack_data_2; auto. red; auto.
+  (* separation *)
+  assert (SEP: forall b0 delta, j' b0 = Some(sp', delta) -> b0 = sp /\ delta = fe_stack_data fe).
+    intros. destruct (zeq b0 sp). 
+    subst b0. rewrite MAP1 in H; inv H; auto.
+    rewrite MAP2 in H; auto. 
+    assert (Mem.valid_block m1' sp'). eapply Mem.valid_block_inject_2; eauto.
+    assert (~Mem.valid_block m1' sp') by eauto with mem.
+    contradiction.
+  (* Conclusions *)
+  exists j'; exists m2'; exists sp'; exists m3'; exists m4'; exists m5'.
+  split. auto.
+  (* store parent *)
+  split. change Tint with (type_of_index FI_link). 
+  change (fe_ofs_link fe) with (offset_of_index fe FI_link).
+  apply store_stack_succeeds; auto. red; auto.
+  (* store retaddr *)
+  split. change Tint with (type_of_index FI_retaddr). 
+  change (fe_ofs_retaddr fe) with (offset_of_index fe FI_retaddr).
+  apply store_stack_succeeds; auto. red; auto.
+  (* saving of registers *)
+  split. eexact STEPS.
+  (* agree_regs *)
+  split. apply agree_regs_call_regs. apply agree_regs_inject_incr with j; auto.
+  (* agree frame *)
+  split. constructor; intros.
+    (* unused regs *)
+    unfold call_regs. destruct (in_dec Loc.eq (R r) temporaries).
+    elim H. apply temporary_within_bounds; auto.
+    apply AGCS. apply mreg_not_within_bounds_callee_save; auto.
+    (* locals *)
+    simpl. apply index_contains_inj_undef; auto.
+    (* outgoing *)
+    simpl. apply index_contains_inj_undef; auto.
+    (* incoming *)
+    unfold call_regs. apply AGCS. auto.
+    (* parent *)
+    apply OTHERS; auto. red; auto.
+    eapply gso_index_contains; eauto. red; auto.
+    eapply gss_index_contains; eauto. red; auto.
+    red; auto.
+    (* retaddr *)
+    apply OTHERS; auto. red; auto.
+    eapply gss_index_contains; eauto. red; auto.
+    (* int callee save *)
+    rewrite <- AGCS. replace (ls (R r)) with (LTL.undef_temps ls (R r)).
+    apply ICS; auto.
+    unfold LTL.undef_temps. apply Locmap.guo. apply Loc.reg_notin. 
+    red; intros; exploit int_callee_save_not_destroyed; eauto. 
+    auto.
+    (* float callee save *)
+    rewrite <- AGCS. replace (ls (R r)) with (LTL.undef_temps ls (R r)).
+    apply FCS; auto.
+    unfold LTL.undef_temps. apply Locmap.guo. apply Loc.reg_notin. 
+    red; intros; exploit float_callee_save_not_destroyed; eauto. 
+    auto.
+    (* inj *)
+    auto.
+    (* inj_unique *)
+    auto.
+    (* valid sp *)
+    eauto with mem.
+    (* valid sp' *)
+    eapply stores_in_frame_valid with (m := m2'); eauto with mem.
+    (* bounds *)
+    eapply Mem.bounds_alloc_same; eauto.
+    (* perms *)
+    auto.
+    (* wt *)
+    apply wt_call_regs; auto.
+  (* incr *)
+  split. auto.
+  (* separated *)
+  split. eapply inject_alloc_separated; eauto with mem.
+  (* inject *)
+  split. eapply stores_in_frame_inject; eauto.
+  eapply Mem.bounds_alloc_same; eauto.
+  (* stores in frame *)
+  auto.
 Qed.
 
 (** The following lemmas show the correctness of the register reloading
@@ -940,165 +1470,436 @@ Variable bound: frame_env -> Z.
 Variable number: mreg -> Z.
 Variable mkindex: Z -> frame_index.
 Variable ty: typ.
-Variable sp: val.
 Variable csregs: list mreg.
+Variable j: meminj.
+Variable cs: list stackframe.
+Variable fb: block.
+Variable sp: block.
+Variable ls0: locset.
+Variable m: mem.
+
 Hypothesis mkindex_valid:
   forall r, In r csregs -> number r < bound fe -> index_valid (mkindex (number r)).
-Hypothesis mkindex_not_link:
-  forall z, mkindex z <> FI_link.
-Hypothesis mkindex_not_retaddr:
-  forall z, mkindex z <> FI_retaddr.
 Hypothesis mkindex_typ:
   forall z, type_of_index (mkindex z) = ty.
 Hypothesis number_within_bounds:
   forall r, In r csregs ->
   (number r < bound fe <-> mreg_within_bounds b r).
 Hypothesis mkindex_val:
-  forall ls ls0 rs fr cs r, 
-  agree ls ls0 rs fr cs -> In r csregs -> number r < bound fe ->
-  index_val (mkindex (number r)) fr = ls0 (R r).
+  forall r,
+  In r csregs -> number r < bound fe ->
+  index_contains_inj j m sp (mkindex (number r)) (ls0 (R r)).
+
+Definition agree_unused (ls0: locset) (rs: regset) : Prop :=
+  forall r, ~(mreg_within_bounds b r) -> val_inject j (ls0 (R r)) (rs r).
 
 Lemma restore_callee_save_regs_correct:
-  forall k fr m ls0 l ls rs cs,
+  forall l rs k,
   incl l csregs ->
   list_norepet l -> 
-  agree ls ls0 rs fr cs ->
-  exists ls', exists rs',
+  agree_unused ls0 rs ->
+  exists rs',
     star step tge
-      (State stack tf sp
-        (restore_callee_save_regs bound number mkindex ty fe l k) rs fr m)
-   E0 (State stack tf sp k rs' fr m)
-  /\ (forall r, In r l -> rs' r = ls0 (R r))
+      (State cs fb (Vptr sp Int.zero)
+        (restore_callee_save_regs bound number mkindex ty fe l k) rs m)
+   E0 (State cs fb (Vptr sp Int.zero) k rs' m)
+  /\ (forall r, In r l -> val_inject j (ls0 (R r)) (rs' r))
   /\ (forall r, ~(In r l) -> rs' r = rs r)
-  /\ agree ls' ls0 rs' fr cs.
+  /\ agree_unused ls0 rs'.
 Proof.
   induction l; intros; simpl restore_callee_save_regs.
   (* base case *)
-  exists ls. exists rs. 
-  split. apply star_refl. 
-  split. intros. elim H2. 
-  split. auto. auto.
+  exists rs. intuition. apply star_refl.
   (* inductive case *)
-  set (k1 := restore_callee_save_regs bound number mkindex ty fe l k).
   assert (R0: In a csregs). apply H; auto with coqlib.
   assert (R1: incl l csregs). eauto with coqlib.
   assert (R2: list_norepet l). inversion H0; auto.
   unfold restore_callee_save_reg.
   destruct (zlt (number a) (bound fe)).
-  set (ls1 := Locmap.set (R a) (ls0 (R a)) ls).
-  set (rs1 := Regmap.set a (ls0 (R a)) rs).
-  assert (R3: agree ls1 ls0 rs1 fr cs). 
-    unfold ls1, rs1. apply agree_set_reg. auto. 
-    rewrite <- number_within_bounds; auto. 
-  generalize (IHl ls1 rs1 cs R1 R2 R3). 
-  intros [ls' [rs' [A [B [C D]]]]].
-  exists ls'. exists rs'. split. 
-  apply star_left with E0 (State stack tf sp k1 rs1 fr m) E0.
-  unfold rs1; apply exec_Mgetstack. apply get_slot_index; auto. 
-  symmetry. eapply mkindex_val; eauto.  
-  auto. traceEq.
-  split. intros. elim H2; intros.
-  subst r. rewrite C. unfold rs1. apply Regmap.gss. inversion H0; auto.
+  exploit (mkindex_val a); auto. intros [v [X Y]].
+  set (rs1 := Regmap.set a v rs).
+  exploit (IHl rs1 k); eauto.
+    red; intros. unfold rs1. unfold Regmap.set. destruct (RegEq.eq r a).
+    subst r. auto.
+    auto.
+  intros [rs' [A [B [C D]]]].
+  exists rs'. split. 
+  eapply star_left. 
+  constructor. rewrite <- (mkindex_typ (number a)). apply index_contains_load_stack. eauto.   
+  eauto. traceEq.
+  split. intros. destruct H2.
+  subst r. rewrite C. unfold rs1. rewrite Regmap.gss. auto. inv H0; auto.
   auto.
   split. intros. simpl in H2. rewrite C. unfold rs1. apply Regmap.gso.
   apply sym_not_eq; tauto. tauto.
-  assumption.
+  auto.
   (* no load takes place *)
-  generalize (IHl ls rs cs R1 R2 H1).  
-  intros [ls' [rs' [A [B [C D]]]]].
-  exists ls'; exists rs'. split. assumption.
-  split. intros. elim H2; intros. 
-  subst r. apply (agree_unused_reg _ _ _ _ _ D).
+  exploit (IHl rs k); auto.
+  intros [rs' [A [B [C D]]]].
+  exists rs'. split. assumption.
+  split. intros. destruct H2.
+  subst r. apply D. 
   rewrite <- number_within_bounds. auto. auto. auto.
   split. intros. simpl in H2. apply C. tauto.
-  assumption.
-Qed.
-
-End RESTORE_CALLEE_SAVE.
-
-Lemma restore_int_callee_save_correct:
-  forall sp k fr m ls0 ls rs cs,
-  agree ls ls0 rs fr cs ->
-  exists ls', exists rs',
-    star step tge
-       (State stack tf sp
-         (restore_callee_save_int fe k) rs fr m)
-    E0 (State stack tf sp k rs' fr m)
-  /\ (forall r, In r int_callee_save_regs -> rs' r = ls0 (R r))
-  /\ (forall r, ~(In r int_callee_save_regs) -> rs' r = rs r)
-  /\ agree ls' ls0 rs' fr cs.
-Proof.
-  intros. unfold restore_callee_save_int.
-  apply restore_callee_save_regs_correct with int_callee_save_regs ls.
-  intros; simpl. split; auto. generalize (index_int_callee_save_pos r H0). omega.
-  intros; congruence.
-  intros; congruence.
-  auto.
-  intros. unfold mreg_within_bounds. 
-  rewrite (int_callee_save_type r H0). tauto. 
-  eauto with stacking. 
-  apply incl_refl.
-  apply int_callee_save_norepet.
   auto.
 Qed.
 
-Lemma restore_float_callee_save_correct:
-  forall sp k fr m ls0 ls rs cs,
-  agree ls ls0 rs fr cs ->
-  exists ls', exists rs',
-    star step tge
-       (State stack tf sp
-          (restore_callee_save_float fe k) rs fr m)
-    E0 (State stack tf sp k rs' fr m)
-  /\ (forall r, In r float_callee_save_regs -> rs' r = ls0 (R r))
-  /\ (forall r, ~(In r float_callee_save_regs) -> rs' r = rs r)
-  /\ agree ls' ls0 rs' fr cs.
-Proof.
-  intros. unfold restore_callee_save_float.
-  apply restore_callee_save_regs_correct with float_callee_save_regs ls.
-  intros; simpl. split; auto. generalize (index_float_callee_save_pos r H0). omega.
-  intros; congruence.
-  intros; congruence.
-  auto.
-  intros. unfold mreg_within_bounds. 
-  rewrite (float_callee_save_type r H0). tauto. 
-  eauto with stacking. 
-  apply incl_refl.
-  apply float_callee_save_norepet.
-  auto.
-Qed.
+End RESTORE_CALLEE_SAVE.
 
 Lemma restore_callee_save_correct:
-  forall sp k fr m ls0 ls rs cs,
-  agree ls ls0 rs fr cs ->
+  forall j ls ls0 m sp m' sp' pa ra cs fb rs k,
+  agree_frame j ls ls0 m sp m' sp' pa ra ->
+  agree_unused j ls0 rs ->
   exists rs',
     star step tge
-       (State stack tf sp (restore_callee_save fe k) rs fr m)
-    E0 (State stack tf sp k rs' fr m)
+       (State cs fb (Vptr sp' Int.zero) (restore_callee_save fe k) rs m')
+    E0 (State cs fb (Vptr sp' Int.zero) k rs' m')
   /\ (forall r, 
         In r int_callee_save_regs \/ In r float_callee_save_regs -> 
-        rs' r = ls0 (R r))
+        val_inject j (ls0 (R r)) (rs' r))
   /\ (forall r, 
         ~(In r int_callee_save_regs) ->
         ~(In r float_callee_save_regs) ->
         rs' r = rs r).
 Proof.
-  intros. unfold restore_callee_save.
-  exploit restore_int_callee_save_correct; eauto.
-  intros [ls1 [rs1 [A [B [C D]]]]].
-  exploit restore_float_callee_save_correct. eexact D.
-  intros [ls2 [rs2 [P [Q [R S]]]]].
-  exists rs2. split. eapply star_trans. eexact A. eexact P. traceEq.
-  split. intros. elim H0; intros.
-  rewrite R. apply B. auto. apply list_disjoint_notin with int_callee_save_regs.
-  apply int_float_callee_save_disjoint. auto.
-  apply Q. auto.
-  intros. rewrite R. apply C. auto. auto.
+  intros. 
+    exploit (restore_callee_save_regs_correct 
+             fe_num_int_callee_save
+             index_int_callee_save
+             FI_saved_int
+             Tint
+             int_callee_save_regs
+             j cs fb sp' ls0 m'); auto.
+  intros. unfold mreg_within_bounds. rewrite (int_callee_save_type r H1). tauto.
+  eapply agree_saved_int; eauto. 
+  apply incl_refl.
+  apply int_callee_save_norepet.
+  eauto.
+  intros [rs1 [A [B [C D]]]].
+  exploit (restore_callee_save_regs_correct 
+             fe_num_float_callee_save
+             index_float_callee_save
+             FI_saved_float
+             Tfloat
+             float_callee_save_regs
+             j cs fb sp' ls0 m'); auto.
+  intros. unfold mreg_within_bounds. rewrite (float_callee_save_type r H1). tauto.
+  eapply agree_saved_float; eauto. 
+  apply incl_refl.
+  apply float_callee_save_norepet.
+  eexact D.
+  intros [rs2 [P [Q [R S]]]].
+  exists rs2.
+  split. unfold restore_callee_save. eapply star_trans; eauto.
+  split. intros. destruct H1.
+    rewrite R. apply B; auto. red; intros. exploit int_float_callee_save_disjoint; eauto.
+    apply Q; auto.
+  intros. rewrite R; auto.
+Qed.
+
+(** As a corollary, we obtain the following correctness result for
+  the execution of a function epilogue (reloading of used callee-save
+  registers + reloading of the link and return address + freeing
+  of the frame). *)
+
+Lemma function_epilogue_correct:
+  forall j ls ls0 m sp m' sp' pa ra cs fb rs k m1,
+  agree_regs j ls rs ->
+  agree_frame j ls ls0 m sp m' sp' pa ra ->
+  Mem.inject j m m' ->
+  Mem.free m sp 0 f.(Linear.fn_stacksize) = Some m1 ->
+  exists rs1, exists m1',
+     load_stack m' (Vptr sp' Int.zero) Tint tf.(fn_link_ofs) = Some pa
+  /\ load_stack m' (Vptr sp' Int.zero) Tint tf.(fn_retaddr_ofs) = Some ra
+  /\ Mem.free m' sp' 0 tf.(fn_stacksize) = Some m1'
+  /\ star step tge
+       (State cs fb (Vptr sp' Int.zero) (restore_callee_save fe k) rs m')
+    E0 (State cs fb (Vptr sp' Int.zero) k rs1 m')
+  /\ agree_regs j (return_regs ls0 ls) rs1
+  /\ agree_callee_save (return_regs ls0 ls) ls0
+  /\ rs1 IT1 = rs IT1
+  /\ Mem.inject j m1 m1'.
+Proof.
+  intros.
+  (* can free *)
+  destruct (Mem.range_perm_free m' sp' 0 (fn_stacksize tf)) as [m1' FREE].
+  rewrite unfold_transf_function; unfold fn_stacksize. red; intros.
+  assert (EITHER: fe_stack_data fe <= ofs < fe_stack_data fe + Linear.fn_stacksize f
+              \/ (ofs < fe_stack_data fe \/ fe_stack_data fe + Linear.fn_stacksize f <= ofs))
+  by omega.
+  destruct EITHER.
+  replace ofs with ((ofs - fe_stack_data fe) + fe_stack_data fe) by omega.
+  eapply Mem.perm_inject with (f := j). eapply agree_inj; eauto. eauto. 
+  eapply Mem.free_range_perm; eauto. omega.
+  eapply agree_perm; eauto. 
+  (* inject after free *)
+  assert (INJ1: Mem.inject j m1 m1').
+  eapply Mem.free_inject with (l := (sp, 0, f.(Linear.fn_stacksize)) :: nil); eauto.
+  simpl. rewrite H2. auto.
+  intros. exploit agree_inj_unique; eauto. intros [P Q]; subst b1 delta.
+  exists 0; exists (Linear.fn_stacksize f); split. auto with coqlib.
+  exploit Mem.perm_in_bounds; eauto. 
+  rewrite (agree_bounds _ _ _ _ _ _ _ _ _ H0). auto.
+  (* can execute epilogue *)
+  exploit restore_callee_save_correct; eauto.
+    instantiate (1 := rs). red; intros. 
+    rewrite <- (agree_unused_reg _ _ _ _ _ _ _ _ _ H0). auto. auto. 
+  intros [rs1 [A [B C]]].
+  (* conclusions *)
+  exists rs1; exists m1'.
+  split. rewrite unfold_transf_function; unfold fn_link_ofs. 
+    eapply index_contains_load_stack with (idx := FI_link); eauto with stacking.
+  split. rewrite unfold_transf_function; unfold fn_retaddr_ofs. 
+    eapply index_contains_load_stack with (idx := FI_retaddr); eauto with stacking.
+  split. auto.
+  split. eexact A.
+  split. red;intros. unfold return_regs. 
+    generalize (register_classification r) (int_callee_save_not_destroyed r) (float_callee_save_not_destroyed r); intros.
+    destruct (in_dec Loc.eq (R r) temporaries).
+    rewrite C; auto. 
+    destruct (in_dec Loc.eq (R r) destroyed_at_call).
+    rewrite C; auto.
+    intuition.
+  split. apply agree_callee_save_return_regs.
+  split. apply C. apply int_callee_save_not_destroyed. left; simpl; auto. 
+  apply float_callee_save_not_destroyed. left; simpl; auto.
+  auto.
 Qed.
 
 End FRAME_PROPERTIES.
 
-(** * Semantic preservation *)
+(** * Call stack invariant *)
+
+Inductive match_globalenvs (j: meminj) (bound: Z) : Prop :=
+  | match_globalenvs_intro
+      (POS: bound > 0)
+      (DOMAIN: forall b, b < bound -> j b = Some(b, 0))
+      (IMAGE: forall b1 b2 delta, j b1 = Some(b2, delta) -> b2 < bound -> b1 = b2)
+      (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> b < bound)
+      (INFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound).
+
+Inductive match_stacks (j: meminj) (m m': mem): 
+       list Linear.stackframe -> list stackframe -> signature -> Z -> Z -> Prop :=
+  | match_stacks_empty: forall sg hi bound bound',
+      hi <= bound -> hi <= bound' -> match_globalenvs j hi ->
+      tailcall_possible sg ->
+      match_stacks j m m' nil nil sg bound bound'
+  | match_stacks_cons: forall f sp ls c cs fb sp' ra c' cs' sg bound bound' trf
+        (TAIL: is_tail c (Linear.fn_code f))
+        (WTF: wt_function f)
+        (FINDF: Genv.find_funct_ptr tge fb = Some (Internal trf))
+        (TRF: transf_function f = OK trf)
+        (TRC: transl_code (make_env (function_bounds f)) c = c')
+        (TY_RA: Val.has_type ra Tint)
+        (FRM: agree_frame f j ls (parent_locset cs) m sp m' sp' (parent_sp cs') (parent_ra cs'))
+        (ARGS: forall ofs ty,
+             In (S (Outgoing ofs ty)) (loc_arguments sg) ->
+             slot_within_bounds f (function_bounds f) (Outgoing ofs ty))
+        (STK: match_stacks j m m' cs cs' (Linear.fn_sig f) sp sp')
+        (BELOW: sp < bound)
+        (BELOW': sp' < bound'),
+      match_stacks j m m'
+                   (Linear.Stackframe f (Vptr sp Int.zero) ls c :: cs)
+                   (Stackframe fb (Vptr sp' Int.zero) ra c' :: cs')
+                   sg bound bound'.
+
+(** Invariance with respect to change of bounds. *)
+
+Lemma match_stacks_change_bounds:
+  forall j m1 m' cs cs' sg bound bound',
+  match_stacks j m1 m' cs cs' sg bound bound' ->
+  forall xbound xbound',
+  bound <= xbound -> bound' <= xbound' ->
+  match_stacks j m1 m' cs cs' sg xbound xbound'.
+Proof.
+  induction 1; intros. 
+  apply match_stacks_empty with hi; auto. omega. omega.
+  econstructor; eauto. omega. omega.
+Qed.
+
+(** Invariance with respect to change of [m]. *)
+
+Lemma match_stacks_change_linear_mem:
+  forall j m1 m2 m' cs cs' sg bound bound',
+  match_stacks j m1 m' cs cs' sg bound bound' ->
+  (forall b, b < bound -> Mem.valid_block m1 b -> Mem.valid_block m2 b) ->
+  (forall b, b < bound -> Mem.bounds m2 b = Mem.bounds m1 b) ->
+  match_stacks j m2 m' cs cs' sg bound bound'.
+Proof.
+  induction 1; intros.
+  econstructor; eauto.
+  econstructor; eauto.
+  eapply agree_frame_invariant; eauto. 
+  apply IHmatch_stacks.
+  intros. apply H0; auto. omega.
+  intros. apply H1. omega.
+Qed.
+
+(** Invariance with respect to change of [m']. *)
+
+Lemma match_stacks_change_mach_mem:
+  forall j m m1' m2' cs cs' sg bound bound',
+  match_stacks j m m1' cs cs' sg bound bound' ->
+  (forall b, b < bound' -> Mem.valid_block m1' b -> Mem.valid_block m2' b) ->
+  (forall b ofs p, b < bound' -> Mem.perm m1' b ofs p -> Mem.perm m2' b ofs p) ->
+  (forall chunk b ofs v, b < bound' -> Mem.load chunk m1' b ofs = Some v -> Mem.load chunk m2' b ofs = Some v) ->
+  match_stacks j m m2' cs cs' sg bound bound'.
+Proof.
+  induction 1; intros.
+  econstructor; eauto.
+  econstructor; eauto.
+  eapply agree_frame_invariant; eauto. 
+  apply IHmatch_stacks. 
+  intros; apply H0; auto; omega.
+  intros; apply H1; auto; omega.
+  intros; apply H2; auto. omega.
+Qed.
+
+(** A variant of the latter, for use with external calls *)
+
+Lemma match_stacks_change_mem_extcall:
+  forall j m1 m2 m1' m2' cs cs' sg bound bound',
+  match_stacks j m1 m1' cs cs' sg bound bound' ->
+  (forall b, b < bound -> Mem.valid_block m1 b -> Mem.valid_block m2 b) ->
+  (forall b, b < bound -> Mem.bounds m2 b = Mem.bounds m1 b) ->
+  (forall b, b < bound' -> Mem.valid_block m1' b -> Mem.valid_block m2' b) ->
+  mem_unchanged_on (loc_out_of_reach j m1) m1' m2' ->
+  match_stacks j m2 m2' cs cs' sg bound bound'.
+Proof.
+  induction 1; intros.
+  econstructor; eauto.
+  econstructor; eauto.
+  eapply agree_frame_extcall_invariant; eauto.
+  apply IHmatch_stacks. 
+  intros; apply H0; auto; omega.
+  intros; apply H1; omega.
+  intros; apply H2; auto; omega.
+  auto.
+Qed.
+
+(** Invariance with respect to change of [j]. *)
+
+Lemma match_stacks_change_meminj:
+  forall j j' m m' m1 m1',
+  inject_incr j j' ->
+  inject_separated j j' m1 m1' ->
+  forall cs cs' sg bound bound',
+  match_stacks j m m' cs cs' sg bound bound' ->
+  bound' <= Mem.nextblock m1' ->
+  match_stacks j' m m' cs cs' sg bound bound'.
+Proof.
+  induction 3; intros.
+  apply match_stacks_empty with hi; auto.
+  inv H3. constructor; auto.
+  intros. red in H0. case_eq (j b1).
+  intros [b' delta'] EQ. rewrite (H _ _ _ EQ) in H3. inv H3. eauto.
+  intros EQ. exploit H0; eauto. intros [A B]. elim B. red. omega. 
+  econstructor; eauto. 
+  eapply agree_frame_inject_incr; eauto. red; omega. 
+  apply IHmatch_stacks. omega.
+Qed.
+
+(** Preservation by parallel stores in Linear and Mach. *)
+
+Lemma match_stacks_parallel_stores:
+  forall j m m' chunk addr addr' v v' m1 m1',
+  Mem.inject j m m' ->
+  val_inject j addr addr' ->
+  Mem.storev chunk m addr v = Some m1 ->
+  Mem.storev chunk m' addr' v' = Some m1' ->
+  forall cs cs' sg bound bound',
+  match_stacks j m m' cs cs' sg bound bound' ->
+  match_stacks j m1 m1' cs cs' sg bound bound'.
+Proof.
+  intros until m1'. intros MINJ VINJ STORE1 STORE2.
+  induction 1.
+  econstructor; eauto.
+  econstructor; eauto.
+  eapply agree_frame_parallel_stores; eauto.
+Qed.
+
+(** Invariance by external calls. *)
+
+Lemma match_stack_change_extcall:
+  forall ec args m1 res t m2 args' m1' res' t' m2' j j',
+  external_call ec ge args m1 t res m2 ->
+  external_call ec ge args' m1' t' res' m2' ->
+  inject_incr j j' ->
+  inject_separated j j' m1 m1' ->
+  mem_unchanged_on (loc_out_of_reach j m1) m1' m2' ->
+  forall cs cs' sg bound bound',
+  match_stacks j m1 m1' cs cs' sg bound bound' ->
+  bound <= Mem.nextblock m1 -> bound' <= Mem.nextblock m1' ->
+  match_stacks j' m2 m2' cs cs' sg bound bound'.
+Proof.
+  intros. 
+  eapply match_stacks_change_meminj; eauto. 
+  eapply match_stacks_change_mem_extcall; eauto.
+  intros; eapply external_call_valid_block; eauto.
+  intros; eapply external_call_bounds; eauto. red; omega.
+  intros; eapply external_call_valid_block; eauto.
+Qed.
+
+(** Invariance with respect to change of signature *)
+
+Lemma match_stacks_change_sig:
+  forall sg1 j m m' cs cs' sg bound bound',
+  match_stacks j m m' cs cs' sg bound bound' ->
+  tailcall_possible sg1 ->
+  match_stacks j m m' cs cs' sg1 bound bound'.
+Proof.
+  induction 1; intros. econstructor; eauto. econstructor; eauto. 
+  intros. elim (H0 _ H1). 
+Qed.
+
+(** [match_stacks] implies [match_globalenvs], which implies [meminj_preserves_globals]. *)
+
+Lemma match_stacks_globalenvs:
+  forall j m m' cs cs' sg bound bound',
+  match_stacks j m m' cs cs' sg bound bound' ->
+  exists hi, match_globalenvs j hi.
+Proof.
+  induction 1. exists hi; auto. auto.
+Qed.
+
+Lemma match_stacks_preserves_globals:
+  forall j m m' cs cs' sg bound bound',
+  match_stacks j m m' cs cs' sg bound bound' ->
+  meminj_preserves_globals ge j.
+Proof.
+  intros. exploit match_stacks_globalenvs; eauto. intros [hi MG]. inv MG.
+  split. eauto. split. eauto. intros. symmetry. eauto. 
+Qed.
+
+(** Typing properties of [match_stacks]. *)
+
+Lemma match_stacks_wt_locset:
+  forall j m m' cs cs' sg bound bound',
+  match_stacks j m m' cs cs' sg bound bound' ->
+  wt_locset (parent_locset cs).
+Proof.
+  induction 1; simpl.
+  unfold Locmap.init; red; intros; red; auto.
+  inv FRM; auto.
+Qed.
+
+Lemma match_stacks_type_sp:
+  forall j m m' cs cs' sg bound bound',
+  match_stacks j m m' cs cs' sg bound bound' ->
+  Val.has_type (parent_sp cs') Tint.
+Proof.
+  induction 1; simpl; auto.
+Qed.
+
+Lemma match_stacks_type_retaddr:
+  forall j m m' cs cs' sg bound bound',
+  match_stacks j m m' cs cs' sg bound bound' ->
+  Val.has_type (parent_ra cs') Tint.
+Proof.
+  induction 1; simpl; auto.
+Qed.
+
+(** * Syntactic properties of the translation *)
 
 (** Preservation of code labels through the translation. *)
 
@@ -1170,19 +1971,86 @@ Qed.
 
 End LABELS.
 
-(** Code inclusion property for Linear executions. *)
+(** Code tail property for Linear executions. *)
 
-Lemma find_label_incl:
+Lemma find_label_tail:
   forall lbl c c', 
-  Linear.find_label lbl c = Some c' -> incl c' c.
+  Linear.find_label lbl c = Some c' -> is_tail c' c.
 Proof.
   induction c; simpl.
   intros; discriminate.
   intro c'. case (Linear.is_label lbl a); intros.
-  injection H; intro; subst c'. red; intros; auto with coqlib. 
-  apply incl_tl. auto.
+  injection H; intro; subst c'. auto with coqlib.
+  auto with coqlib.
 Qed.
 
+(** Code tail property for translations *)
+
+Lemma is_tail_save_callee_save_regs:
+  forall bound number mkindex ty fe csl k,
+  is_tail k (save_callee_save_regs bound number mkindex ty fe csl k).
+Proof.
+  induction csl; intros; simpl. auto with coqlib.
+  unfold save_callee_save_reg. destruct (zlt (number a) (bound fe)). 
+  constructor; auto. auto.
+Qed.
+
+Lemma is_tail_save_callee_save:
+  forall fe k,
+  is_tail k (save_callee_save fe k).
+Proof.
+  intros. unfold save_callee_save, save_callee_save_int, save_callee_save_float.
+  eapply is_tail_trans; apply is_tail_save_callee_save_regs.
+Qed.
+
+Lemma is_tail_restore_callee_save_regs:
+  forall bound number mkindex ty fe csl k,
+  is_tail k (restore_callee_save_regs bound number mkindex ty fe csl k).
+Proof.
+  induction csl; intros; simpl. auto with coqlib.
+  unfold restore_callee_save_reg. destruct (zlt (number a) (bound fe)). 
+  constructor; auto. auto.
+Qed.
+
+Lemma is_tail_restore_callee_save:
+  forall fe k,
+  is_tail k (restore_callee_save fe k).
+Proof.
+  intros. unfold restore_callee_save, restore_callee_save_int, restore_callee_save_float.
+  eapply is_tail_trans; apply is_tail_restore_callee_save_regs.
+Qed.
+
+Lemma is_tail_transl_instr:
+  forall fe i k,
+  is_tail k (transl_instr fe i k).
+Proof.
+  intros. destruct i; unfold transl_instr; auto with coqlib.
+  destruct s; auto with coqlib.
+  destruct s; auto with coqlib.
+  eapply is_tail_trans. 2: apply is_tail_restore_callee_save. auto with coqlib.
+  eapply is_tail_trans. 2: apply is_tail_restore_callee_save. auto with coqlib.
+Qed.
+
+Lemma is_tail_transl_code:
+  forall fe c1 c2, is_tail c1 c2 -> is_tail (transl_code fe c1) (transl_code fe c2).
+Proof.
+  induction 1; simpl. auto with coqlib. 
+  eapply is_tail_trans. eauto. apply is_tail_transl_instr.
+Qed.
+
+Lemma is_tail_transf_function:
+  forall f tf c,
+  transf_function f = OK tf ->
+  is_tail c (Linear.fn_code f) ->
+  is_tail (transl_code (make_env (function_bounds f)) c) (fn_code tf).
+Proof.
+  intros. rewrite (unfold_transf_function _ _ H). simpl. 
+  unfold transl_body. eapply is_tail_trans. 2: apply is_tail_save_callee_save.
+  apply is_tail_transl_code; auto.
+Qed.
+
+(** * Semantic preservation *)
+
 (** Preservation / translation of global symbols and functions. *)
 
 Lemma symbols_preserved:
@@ -1221,35 +2089,35 @@ Lemma sig_preserved:
   forall f tf, transf_fundef f = OK tf -> Mach.funsig tf = Linear.funsig f.
 Proof.
   intros until tf; unfold transf_fundef, transf_partial_fundef.
-  destruct f. unfold transf_function. 
-  destruct (zlt (Linear.fn_stacksize f) 0). simpl; congruence.
-  destruct (zlt (- Int.min_signed) (fe_size (make_env (function_bounds f)))). simpl; congruence.
-  unfold bind. intros. inversion H; reflexivity. 
-  intro. inversion H. reflexivity.
-Qed.
-
-Lemma stacksize_preserved:
-  forall f tf, transf_function f = OK tf -> Mach.fn_stacksize tf = Linear.fn_stacksize f.
-Proof.
-  intros until tf; unfold transf_function. 
-  destruct (zlt (Linear.fn_stacksize f) 0). simpl; congruence.
-  destruct (zlt (- Int.min_signed) (fe_size (make_env (function_bounds f)))). simpl; congruence.
-  intros. inversion H; reflexivity. 
+  destruct f; intros; monadInv H.
+  rewrite (unfold_transf_function _ _ EQ). auto. 
+  auto.
 Qed.
 
 Lemma find_function_translated:
-  forall f0 tf0 ls ls0 rs fr cs ros f,
-  agree f0 tf0 ls ls0 rs fr cs ->
+  forall j ls rs m m' cs cs' sg bound bound' ros f,
+  agree_regs j ls rs ->
+  match_stacks j m m' cs cs' sg bound bound' ->
   Linear.find_function ge ros ls = Some f ->
-  exists tf,
-  find_function tge ros rs = Some tf /\ transf_fundef f = OK tf.
+  exists bf, exists tf,
+     find_function_ptr tge ros rs = Some bf
+  /\ Genv.find_funct_ptr tge bf = Some tf
+  /\ transf_fundef f = OK tf.
 Proof.
-  intros until f; intro AG.
-  destruct ros; simpl.
-  rewrite (agree_eval_reg _ _ _ _ _ _ _ m AG). intro.
-  apply functions_translated; auto.
-  rewrite symbols_preserved. destruct (Genv.find_symbol ge i); try congruence.
-  intro. apply function_ptr_translated; auto.
+  intros until f; intros AG MS FF.
+  exploit match_stacks_globalenvs; eauto. intros [hi MG]. 
+  destruct ros; simpl in FF.
+  exploit Genv.find_funct_inv; eauto. intros [b EQ]. rewrite EQ in FF. 
+  rewrite Genv.find_funct_find_funct_ptr in FF. 
+  exploit function_ptr_translated; eauto. intros [tf [A B]].
+  exists b; exists tf; split; auto. simpl.
+  generalize (AG m0). rewrite EQ. intro INJ. inv INJ.
+  exploit Genv.find_funct_ptr_negative. unfold ge in FF; eexact FF. intros. 
+  inv MG. rewrite (DOMAIN b) in H2. inv H2. auto. omega. 
+  revert FF. case_eq (Genv.find_symbol ge i); intros; try discriminate. 
+  exploit function_ptr_translated; eauto. intros [tf [A B]].
+  exists b; exists tf; split; auto. simpl. 
+  rewrite symbols_preserved. auto.
 Qed.
 
 Hypothesis wt_prog: wt_program prog.
@@ -1264,84 +2132,59 @@ Proof.
   intro. eapply Genv.find_funct_ptr_prop; eauto. 
 Qed.
 
-(** Correctness of stack pointer relocation in operations and
-  addressing modes. *)
-
-Definition shift_sp (tf: Mach.function) (sp: val) :=
-  Val.add sp (Vint (Int.repr (-tf.(fn_framesize)))).
-
-Remark shift_sp_eq:
-  forall f tf sp,
-  transf_function f = OK tf ->
-  shift_sp tf sp = Val.sub sp (Vint (Int.repr (fe_size (make_env (function_bounds f))))).
-Proof.
-  intros. unfold shift_sp.
-  replace (fe_size (make_env (function_bounds f))) with (fn_framesize tf).
-  rewrite <- Int.neg_repr. destruct sp; simpl; auto; rewrite Int.sub_add_opp; auto.
-  rewrite (unfold_transf_function _ _ H). auto.
-Qed.
-
-Lemma shift_eval_operation:
-  forall f tf sp op args v,
-  transf_function f = OK tf ->
-  eval_operation ge sp op args = Some v ->
-  eval_operation tge (shift_sp tf sp) 
-                 (transl_op (make_env (function_bounds f)) op) args = Some v.
-Proof.
-  intros. rewrite <- H0. rewrite (shift_sp_eq f tf sp H). unfold transl_op.
-  rewrite (eval_operation_preserved ge tge). 
-  apply shift_stack_eval_operation.
-  exact symbols_preserved.
-Qed.
-
-Lemma shift_eval_addressing:
-  forall f tf sp addr args v,
-  transf_function f = OK tf ->
-  eval_addressing ge sp addr args = Some v ->
-  eval_addressing tge (shift_sp tf sp) 
-                 (transl_addr (make_env (function_bounds f)) addr) args =
-  Some v.
-Proof.
-  intros. rewrite <- H0. rewrite (shift_sp_eq f tf sp H). unfold transl_addr.
-  rewrite (eval_addressing_preserved ge tge). 
-  apply shift_stack_eval_addressing.
-  exact symbols_preserved.
-Qed.
-
 (** Preservation of the arguments to an external call. *)
 
 Section EXTERNAL_ARGUMENTS.
 
-Variable cs: list Machabstr.stackframe.
+Variable j: meminj.
+Variables m m': mem.
+Variable cs: list Linear.stackframe.
+Variable cs': list stackframe.
+Variable sg: signature.
+Variables bound bound': Z.
+Hypothesis MS: match_stacks j m m' cs cs' sg bound bound'.
 Variable ls: locset.
 Variable rs: regset.
-Variable sg: signature.
+Hypothesis AGR: agree_regs j ls rs.
+Hypothesis AGCS: agree_callee_save ls (parent_locset cs).
 
-Hypothesis AG1: forall r, rs r = ls (R r).
-Hypothesis AG2: forall (ofs : Z) (ty : typ),
-      In (S (Outgoing ofs ty)) (loc_arguments sg) ->
-      get_parent_slot cs ofs ty (ls (S (Outgoing ofs ty))).
+Lemma transl_external_argument:
+  forall l,
+  In l (loc_arguments sg) ->
+  exists v, extcall_arg rs m' (parent_sp cs') l v /\ val_inject j (ls l) v.
+Proof.
+  intros.
+  assert (loc_argument_acceptable l). apply loc_arguments_acceptable with sg; auto.
+  destruct l; red in H0.
+  exists (rs m0); split. constructor. auto. 
+  destruct s; try contradiction.
+  inv MS. 
+  elim (H4 _ H).
+  unfold parent_sp. 
+  exploit agree_outgoing; eauto. intros [v [A B]].
+  exists v; split.
+  constructor. 
+  eapply index_contains_load_stack with (idx := FI_arg z t); eauto. 
+  red in AGCS. rewrite AGCS; auto.
+Qed.
 
 Lemma transl_external_arguments_rec:
   forall locs,
   incl locs (loc_arguments sg) ->
-  extcall_args (parent_function cs) rs (parent_frame cs) locs ls##locs.
+  exists vl,
+  extcall_args rs m' (parent_sp cs') locs vl /\ val_list_inject j ls##locs vl.
 Proof.
   induction locs; simpl; intros.
-  constructor.
-  constructor. 
-  assert (loc_argument_acceptable a). 
-    apply loc_arguments_acceptable with sg; auto with coqlib.
-  destruct a; red in H0.
-  rewrite <- AG1. constructor. 
-  destruct s; try contradiction.
-  constructor. change (get_parent_slot cs z t (ls (S (Outgoing z t)))).
-apply AG2. auto with coqlib. 
-  apply IHlocs; eauto with coqlib.
+  exists (@nil val); split. constructor. constructor.
+  exploit transl_external_argument; eauto with coqlib. intros [v [A B]].
+  exploit IHlocs; eauto with coqlib. intros [vl [C D]].
+  exists (v :: vl); split; constructor; auto.
 Qed.
 
 Lemma transl_external_arguments:
-  extcall_arguments (parent_function cs) rs (parent_frame cs) sg (ls ## (loc_arguments sg)).
+  exists vl,
+  extcall_arguments rs m' (parent_sp cs') sg vl /\
+  val_list_inject j (ls ## (loc_arguments sg)) vl.
 Proof.
   unfold extcall_arguments. 
   apply transl_external_arguments_rec.
@@ -1364,61 +2207,53 @@ End EXTERNAL_ARGUMENTS.
   below.  It implies:
 - Agreement between, on the Linear side, the location sets [ls]
   and [parent_locset s] of the current function and its caller,
-  and on the Mach side the register set [rs], the frame [fr]
-  and the caller's frame [parent_frame ts].
-- Inclusion between the Linear code [c] and the code of the
+  and on the Mach side the register set [rs] and the contents of
+  the memory area corresponding to the stack frame.
+- The Linear code [c] is a suffix of the code of the
   function [f] being executed.
+- Memory injection between the Linear and the Mach memory states.
 - Well-typedness of [f].
 *)
 
-Inductive match_stacks: list Linear.stackframe -> list Machabstr.stackframe -> Prop :=
-  | match_stacks_nil:
-      match_stacks nil nil
-  | match_stacks_cons:
-      forall f sp c ls tf fr s ts,
-      match_stacks s ts ->
-      transf_function f = OK tf ->
-      wt_function f ->
-      agree_frame f tf ls (parent_locset s) fr ts ->
-      incl c (Linear.fn_code f) ->
-      match_stacks
-       (Linear.Stackframe f sp ls c :: s)
-       (Machabstr.Stackframe tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) c) fr :: ts).
-
-Inductive match_states: Linear.state -> Machabstr.state -> Prop :=
+Inductive match_states: Linear.state -> Machconcr.state -> Prop :=
   | match_states_intro:
-      forall s f sp c ls m ts tf rs fr
-        (STACKS: match_stacks s ts)
+      forall cs f sp c ls m cs' fb sp' rs m' j tf
+        (MINJ: Mem.inject j m m')
+        (STACKS: match_stacks j m m' cs cs' f.(Linear.fn_sig) sp sp')
         (TRANSL: transf_function f = OK tf)
+        (FIND: Genv.find_funct_ptr tge fb = Some (Internal tf))
         (WTF: wt_function f)
-        (AG: agree f tf ls (parent_locset s) rs fr ts)
-        (INCL: incl c (Linear.fn_code f)),
-      match_states (Linear.State s f sp c ls m)
-                   (Machabstr.State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) c) rs fr m)
+        (AGREGS: agree_regs j ls rs)
+        (AGFRAME: agree_frame f j ls (parent_locset cs) m sp m' sp' (parent_sp cs') (parent_ra cs'))
+        (TAIL: is_tail c (Linear.fn_code f)),
+      match_states (Linear.State cs f (Vptr sp Int.zero) c ls m)
+                  (Machconcr.State cs' fb (Vptr sp' Int.zero) (transl_code (make_env (function_bounds f)) c) rs m')
   | match_states_call:
-      forall s f ls m ts tf rs
-        (STACKS: match_stacks s ts)
+      forall cs f ls m cs' fb rs m' j tf
+        (MINJ: Mem.inject j m m')
+        (STACKS: match_stacks j m m' cs cs' (Linear.funsig f) (Mem.nextblock m) (Mem.nextblock m'))
         (TRANSL: transf_fundef f = OK tf)
+        (FIND: Genv.find_funct_ptr tge fb = Some tf)
         (WTF: wt_fundef f)
-        (AG1: forall r, rs r = ls (R r))
-        (AG2: forall ofs ty, 
-                In (S (Outgoing ofs ty)) (loc_arguments (Linear.funsig f)) ->
-                get_parent_slot ts ofs ty (ls (S (Outgoing ofs ty))))
-        (AG3: agree_callee_save ls (parent_locset s)),
-      match_states (Linear.Callstate s f ls m)
-                   (Machabstr.Callstate ts tf rs m)
+        (WTLS: wt_locset ls)
+        (AGREGS: agree_regs j ls rs)
+        (AGLOCS: agree_callee_save ls (parent_locset cs)),
+      match_states (Linear.Callstate cs f ls m)
+                  (Machconcr.Callstate cs' fb rs m')
   | match_states_return:
-      forall s ls m ts rs
-        (STACKS: match_stacks s ts)
-        (AG1: forall r, rs r = ls (R r))
-        (AG2: agree_callee_save ls (parent_locset s)),
-      match_states (Linear.Returnstate s ls m)
-                   (Machabstr.Returnstate ts rs m).
+      forall cs ls m cs' rs m' j sg 
+        (MINJ: Mem.inject j m m')
+        (STACKS: match_stacks j m m' cs cs' sg (Mem.nextblock m) (Mem.nextblock m'))
+        (WTLS: wt_locset ls)
+        (AGREGS: agree_regs j ls rs)
+        (AGLOCS: agree_callee_save ls (parent_locset cs)),
+      match_states (Linear.Returnstate cs ls m)
+                  (Machconcr.Returnstate cs' rs m').
 
 Theorem transf_step_correct:
   forall s1 t s2, Linear.step ge s1 t s2 ->
   forall s1' (MS: match_states s1 s1'),
-  exists s2', plus step tge s1' t s2' /\ match_states s2 s2'.
+  exists s2', plus Machconcr.step tge s1' t s2' /\ match_states s2 s2'.
 Proof.
   assert (RED: forall f i c,
           transl_code (make_env (function_bounds f)) (i :: c) = 
@@ -1428,142 +2263,209 @@ Proof.
   induction 1; intros;
   try inv MS;
   try rewrite RED;
-  try (generalize (WTF _ (INCL _ (in_eq _ _))); intro WTI);
-  try (generalize (function_is_within_bounds f WTF _ (INCL _ (in_eq _ _)));
+  try (generalize (WTF _ (is_tail_in TAIL)); intro WTI);
+  try (generalize (function_is_within_bounds f WTF _ (is_tail_in TAIL));
        intro BOUND; simpl in BOUND);
   unfold transl_instr.
+
   (* Lgetstack *)
   inv WTI. destruct BOUND. unfold undef_getstack; destruct sl.
   (* Lgetstack, local *)
-  exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b)
-             (rs0#r <- (rs (S (Local z t)))) fr m); split.
-  apply plus_one. apply exec_Mgetstack.
-  apply get_slot_index. auto. apply index_local_valid. auto. congruence. congruence. auto.
-  eapply agree_locals; eauto.
-  econstructor; eauto with coqlib. 
-  apply agree_set_reg; auto.
+  exploit agree_locals; eauto. intros [v [A B]].
+  econstructor; split.
+  apply plus_one. apply exec_Mgetstack. 
+  eapply index_contains_load_stack; eauto.
+  econstructor; eauto with coqlib.
+  apply agree_regs_set_reg; auto.
+  apply agree_frame_set_reg; auto. simpl; rewrite <- H1. eapply agree_wt_ls; eauto.
   (* Lgetstack, incoming *)
-  exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b)
-             (rs0 # IT1 <- Vundef # r <- (rs (S (Incoming z t)))) fr m); split.
-  apply plus_one. apply exec_Mgetparam.
-  change (get_parent_slot ts z t (rs (S (Incoming z t)))).
-  eapply agree_incoming; eauto.
-  econstructor; eauto with coqlib. 
-  apply agree_set_reg; auto. apply agree_undef_getparam; auto.
+  red in H2. exploit incoming_slot_in_parameters; eauto. intros IN_ARGS.
+  inv STACKS. elim (H6 _ IN_ARGS). 
+  exploit agree_outgoing. eexact FRM. eapply ARGS; eauto.
+  intros [v [A B]].
+  econstructor; split.
+  apply plus_one. eapply exec_Mgetparam; eauto. 
+  rewrite (unfold_transf_function _ _ TRANSL). unfold fn_link_ofs. 
+  eapply index_contains_load_stack with (idx := FI_link). eauto. eapply agree_link; eauto. 
+  simpl parent_sp.
+  change (offset_of_index (make_env (function_bounds f)) (FI_arg z t))
+    with (offset_of_index (make_env (function_bounds f0)) (FI_arg z t)).
+  eapply index_contains_load_stack with (idx := FI_arg z t). eauto. eauto.
+  exploit agree_incoming; eauto. intros EQ; simpl in EQ.
+  econstructor; eauto with coqlib. econstructor; eauto.
+  apply agree_regs_set_reg. apply agree_regs_set_reg. auto. auto. congruence. 
+  eapply agree_frame_set_reg; eauto. eapply agree_frame_set_reg; eauto. 
+  apply temporary_within_bounds. unfold temporaries; auto with coqlib.
+  simpl; auto. simpl; rewrite <- H1. eapply agree_wt_ls; eauto.
   (* Lgetstack, outgoing *)
-  exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b)
-             (rs0#r <- (rs (S (Outgoing z t)))) fr m); split.
-  apply plus_one. apply exec_Mgetstack.
-  apply get_slot_index. auto. apply index_arg_valid. auto. congruence. congruence. auto.
-  eapply agree_outgoing; eauto.
-  econstructor; eauto with coqlib. 
-  apply agree_set_reg; auto.
-
-  (* Lsetstack *)
-  inv WTI. destruct sl.
-
-  (* Lsetstack, local *)
-  generalize (agree_set_local _ _ TRANSL _ _ _ _ _ (rs0 r) _ _ AG BOUND).
-  intros [fr' [SET AG']].
+  exploit agree_outgoing; eauto. intros [v [A B]].
   econstructor; split.
-  apply plus_one. eapply exec_Msetstack; eauto.
+  apply plus_one. apply exec_Mgetstack. 
+  eapply index_contains_load_stack; eauto.
   econstructor; eauto with coqlib.
-  replace (rs (R r)) with (rs0 r). auto.
-  symmetry. eapply agree_reg; eauto.
-  (* Lsetstack, incoming *)
-  contradiction.
-  (* Lsetstack, outgoing *)
-  generalize (agree_set_outgoing _ _ TRANSL _ _ _ _ _ (rs0 r) _ _ AG BOUND).
-  intros [fr' [SET AG']].
+  apply agree_regs_set_reg; auto.
+  apply agree_frame_set_reg; auto. simpl; rewrite <- H1; eapply agree_wt_ls; eauto.
+
+  (* Lsetstack *)
+  inv WTI.
+  set (idx := match sl with
+              | Local ofs ty => FI_local ofs ty
+              | Incoming ofs ty => FI_link (*dummy*)
+              | Outgoing ofs ty => FI_arg ofs ty
+              end).
+  assert (index_valid f idx).
+    unfold idx; destruct sl.
+    apply index_local_valid; auto.
+    red; auto.
+    apply index_arg_valid; auto.
+  exploit store_index_succeeds; eauto. eapply agree_perm; eauto.
+  instantiate (1 := rs0 r). intros [m1' STORE].
   econstructor; split.
-  apply plus_one. eapply exec_Msetstack; eauto.
+  apply plus_one. destruct sl; simpl in H3.
+    econstructor. eapply store_stack_succeeds with (idx := idx); eauto. 
+    contradiction.
+    econstructor. eapply store_stack_succeeds with (idx := idx); eauto. 
   econstructor; eauto with coqlib.
-  replace (rs (R r)) with (rs0 r). auto.
-  symmetry. eapply agree_reg; eauto.
+  eapply Mem.store_outside_inject; eauto. 
+    intros. exploit agree_inj_unique; eauto. intros [EQ1 EQ2]; subst b' delta.
+    rewrite (agree_bounds _ _ _ _ _ _ _ _ _ _ AGFRAME). unfold fst, snd. rewrite Zplus_0_l. 
+    rewrite size_type_chunk. 
+    exploit offset_of_index_disj_stack_data_2; eauto.
+    omega.
+  apply match_stacks_change_mach_mem with m'; auto.
+  eauto with mem. eauto with mem. intros. rewrite <- H4; eapply Mem.load_store_other; eauto. left; unfold block; omega.
+  apply agree_regs_set_slot; auto.
+  destruct sl.
+    eapply agree_frame_set_local; eauto. simpl in H1; rewrite H1; eapply agree_wt_ls; eauto.
+    simpl in H3; contradiction.
+    eapply agree_frame_set_outgoing; eauto. simpl in H1; rewrite H1; eapply agree_wt_ls; eauto.
 
   (* Lop *)
-  set (op' := transl_op (make_env (function_bounds f)) op).
-  exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b) ((undef_op op' rs0)#res <- v) fr m); split.
-  apply plus_one. apply exec_Mop. 
-  apply shift_eval_operation. auto. 
-  change mreg with RegEq.t.
-  rewrite (agree_eval_regs _ _ _ _ _ _ _ args AG). auto.
+  assert (Val.has_type v (mreg_type res)).
+    inv WTI. simpl in H. inv H. rewrite <- H1. eapply agree_wt_ls; eauto. 
+    replace (mreg_type res) with (snd (type_of_operation op)).
+    eapply type_of_operation_sound; eauto. 
+    rewrite <- H4; auto.
+  assert (exists v',
+          eval_operation ge (Vptr sp' Int.zero) (transl_op (make_env (function_bounds f)) op) rs0##args m' = Some v'
+       /\ val_inject j v v').
+  eapply eval_operation_inject; eauto.
+  eapply match_stacks_preserves_globals; eauto.
+  eapply agree_inj; eauto. eapply agree_reglist; eauto.
+  destruct H1 as [v' [A B]].
+  econstructor; split. 
+  apply plus_one. constructor. 
+  instantiate (1 := v'). rewrite <- A. apply eval_operation_preserved. 
+  exact symbols_preserved.
   econstructor; eauto with coqlib.
-  apply agree_set_reg; auto. apply agree_undef_op; auto.
+  apply agree_regs_set_reg; auto. apply agree_regs_undef_op; auto. 
+  apply agree_frame_set_reg; auto. apply agree_frame_undef_op; auto.
 
   (* Lload *)
-  exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b) ((undef_temps rs0)#dst <- v) fr m); split.
-  apply plus_one; eapply exec_Mload; eauto.
-  apply shift_eval_addressing; auto. 
-  change mreg with RegEq.t.
-  rewrite (agree_eval_regs _ _ _ _ _ _ _ args AG). eauto.
+  assert (exists a',
+          eval_addressing ge (Vptr sp' Int.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a'
+       /\ val_inject j a a').
+  eapply eval_addressing_inject; eauto. 
+  eapply match_stacks_preserves_globals; eauto.
+  eapply agree_inj; eauto. eapply agree_reglist; eauto.
+  destruct H1 as [a' [A B]].
+  exploit Mem.loadv_inject; eauto. intros [v' [C D]].
+  econstructor; split. 
+  apply plus_one. econstructor. 
+  instantiate (1 := a'). rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved.
+  eexact C.
   econstructor; eauto with coqlib.
-  apply agree_set_reg; auto. apply agree_undef_temps; auto.
+  apply agree_regs_set_reg; auto. apply agree_regs_undef_temps; auto. 
+  apply agree_frame_set_reg; auto. apply agree_frame_undef_temps; auto.
+  simpl. inv WTI. rewrite H6. 
+  inv B; simpl in H0; try discriminate. eapply Mem.load_type; eauto.
 
   (* Lstore *)
+  assert (exists a',
+          eval_addressing ge (Vptr sp' Int.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a'
+       /\ val_inject j a a').
+  eapply eval_addressing_inject; eauto. 
+  eapply match_stacks_preserves_globals; eauto.
+  eapply agree_inj; eauto. eapply agree_reglist; eauto.
+  destruct H1 as [a' [A B]].
+  exploit Mem.storev_mapped_inject; eauto. intros [m1' [C D]].
+  econstructor; split. 
+  apply plus_one. econstructor. 
+  instantiate (1 := a'). rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved.
+  eexact C.
+  econstructor; eauto with coqlib.
+  eapply match_stacks_parallel_stores. eexact MINJ. eexact B. eauto. eauto. auto. 
+  apply agree_regs_undef_temps; auto. 
+  apply agree_frame_undef_temps; auto.
+  eapply agree_frame_parallel_stores; eauto.
+
+  (* Lcall *)
+  exploit find_function_translated; eauto. intros [bf [tf' [A [B C]]]].
+  exploit is_tail_transf_function; eauto. intros IST. simpl in IST.
+  exploit Asmgenretaddr.return_address_exists. eexact IST.
+  intros [ra D].
   econstructor; split.
-  apply plus_one; eapply exec_Mstore; eauto.
-  apply shift_eval_addressing; eauto. 
-  change mreg with RegEq.t.
-  rewrite (agree_eval_regs _ _ _ _ _ _ _ args AG). eauto.
-  rewrite (agree_eval_reg _ _ _ _ _ _ _ src AG). eauto.
-  econstructor; eauto with coqlib. apply agree_undef_temps; auto.
-
-  (* Lcall *) 
-  assert (WTF': wt_fundef f'). eapply find_function_well_typed; eauto.
-  exploit find_function_translated; eauto. 
-  intros [tf' [FIND' TRANSL']].
-  econstructor; split.
-  apply plus_one; eapply exec_Mcall; eauto.
-  econstructor; eauto. 
+  apply plus_one. econstructor; eauto.
+  econstructor; eauto.
   econstructor; eauto with coqlib.
-  exists rs0; auto.
-  intro. symmetry. eapply agree_reg; eauto.
-  intros.
-  assert (slot_within_bounds f (function_bounds f) (Outgoing ofs ty)).
-  red. simpl. generalize (loc_arguments_bounded _ _ _ H0). 
-  generalize (loc_arguments_acceptable _ _ H0). unfold loc_argument_acceptable. 
-  omega.
-  unfold get_parent_slot, parent_function, parent_frame. 
-  change (fe_ofs_arg + 4 * ofs)
-    with (offset_of_index (make_env (function_bounds f)) (FI_arg ofs ty)).
-  apply get_slot_index. auto. apply index_arg_valid. auto. congruence. congruence. auto.
-  eapply agree_outgoing; eauto.
-  simpl. red; auto.
-
-  (* Ltailcall *) 
-  assert (WTF': wt_fundef f'). eapply find_function_well_typed; eauto.
-  exploit find_function_translated; eauto. 
-  intros [tf' [FIND' TRANSL']].
-  generalize (restore_callee_save_correct ts _ _ TRANSL
-               (shift_sp tf (Vptr stk Int.zero)) 
-               (Mtailcall (Linear.funsig f') ros :: transl_code (make_env (function_bounds f)) b)
-               _ m _ _ _ _ AG).
-  intros [rs2 [A [B C]]].
-  assert (FIND'': find_function tge ros rs2 = Some tf').
-    rewrite <- FIND'. destruct ros; simpl; auto.
-    inv WTI. rewrite C. auto. 
-    simpl. intuition congruence. simpl. intuition congruence. 
+  simpl; auto.
+  intros; red. split.
+    generalize (loc_arguments_acceptable _ _ H0). simpl. omega.
+    apply Zle_trans with (size_arguments (Linear.funsig f')); auto.
+    apply loc_arguments_bounded; auto.
+  eapply agree_valid_linear; eauto.
+  eapply agree_valid_mach; eauto.
+  eapply find_function_well_typed; eauto.
+  eapply agree_wt_ls; eauto. 
+  simpl; red; auto.
+
+  (* Ltailcall *)
+  exploit find_function_translated; eauto. intros [bf [tf' [A [B C]]]].
+  exploit function_epilogue_correct; eauto.
+  intros [rs1 [m1' [P [Q [R [S [T [U [V W]]]]]]]]].
   econstructor; split.
-  eapply plus_right. eexact A. 
-  simpl shift_sp. eapply exec_Mtailcall; eauto.
-  rewrite (stacksize_preserved _ _ TRANSL); eauto.
+  eapply plus_right. eexact S. econstructor; eauto.
+  replace (find_function_ptr tge ros rs1)
+     with (find_function_ptr tge ros rs0). eauto.
+  destruct ros; simpl; auto. inv WTI. rewrite V; auto. 
   traceEq.
-  econstructor; eauto. 
-  intros; symmetry; eapply agree_return_regs; eauto.
-  intros. inv WTI. generalize (H4 _ H0). tauto.
-  apply agree_callee_save_return_regs.
+  econstructor; eauto.
+  inv WTI. apply match_stacks_change_sig with (Linear.fn_sig f); auto.
+  apply match_stacks_change_bounds with stk sp'.
+  apply match_stacks_change_linear_mem with m. 
+  apply match_stacks_change_mach_mem with m'0.
+  auto. 
+  eauto with mem. intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega. 
+  intros. rewrite <- H2. eapply Mem.load_free; eauto. left; unfold block; omega.
+  eauto with mem. intros. eapply Mem.bounds_free; eauto.
+  apply Zlt_le_weak. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. 
+  apply Zlt_le_weak. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. 
+  eapply find_function_well_typed; eauto.
+  apply wt_return_regs; auto. eapply match_stacks_wt_locset; eauto. eapply agree_wt_ls; eauto.
 
   (* Lbuiltin *)
+  exploit external_call_mem_inject; eauto. 
+    eapply match_stacks_preserves_globals; eauto.
+    eapply agree_reglist; eauto. 
+  intros [j' [res' [m1' [A [B [C [D [E [F G]]]]]]]]].
   econstructor; split.
-  apply plus_one. apply exec_Mbuiltin.
-  change mreg with RegEq.t.
-  rewrite (agree_eval_regs _ _ _ _ _ _ _ args AG).
+  apply plus_one. econstructor; eauto. 
   eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
   econstructor; eauto with coqlib.
-  apply agree_set_reg; auto. apply agree_undef_temps; auto.
- 
+  eapply match_stack_change_extcall; eauto.
+  apply Zlt_le_weak. change (Mem.valid_block m sp0). eapply agree_valid_linear; eauto.
+  apply Zlt_le_weak. change (Mem.valid_block m'0 sp'). eapply agree_valid_mach; eauto.
+  apply agree_regs_set_reg; auto. apply agree_regs_undef_temps; auto. eapply agree_regs_inject_incr; eauto.
+  apply agree_frame_set_reg; auto. apply agree_frame_undef_temps; auto.
+  eapply agree_frame_inject_incr; eauto. 
+  apply agree_frame_extcall_invariant with m m'0; auto.
+  eapply external_call_valid_block; eauto.
+  eapply external_call_bounds; eauto. eapply agree_valid_linear; eauto.
+  eapply external_call_valid_block; eauto.
+  eapply agree_valid_mach; eauto.
+  inv WTI. simpl; rewrite H4. eapply external_call_well_typed; eauto.
+
   (* Llabel *)
   econstructor; split.
   apply plus_one; apply exec_Mlabel.
@@ -1571,124 +2473,160 @@ Proof.
 
   (* Lgoto *)
   econstructor; split.
-  apply plus_one; apply exec_Mgoto.
+  apply plus_one; eapply exec_Mgoto; eauto.
   apply transl_find_label; eauto.
   econstructor; eauto. 
-  eapply find_label_incl; eauto.
+  eapply find_label_tail; eauto.
 
   (* Lcond, true *)
   econstructor; split.
-  apply plus_one; apply exec_Mcond_true.
-  rewrite <- (agree_eval_regs _ _ _ _ _ _ _ args AG) in H; eauto.
-  apply transl_find_label; eauto.
-  econstructor; eauto. apply agree_undef_temps; auto.
-  eapply find_label_incl; eauto.
+  apply plus_one. eapply exec_Mcond_true; eauto.
+  eapply eval_condition_inject; eauto. eapply agree_reglist; eauto.
+  eapply transl_find_label; eauto. 
+  econstructor; eauto with coqlib.
+  apply agree_regs_undef_temps; auto.
+  apply agree_frame_undef_temps; auto.
+  eapply find_label_tail; eauto.
 
   (* Lcond, false *)
   econstructor; split.
-  apply plus_one; apply exec_Mcond_false.
-  rewrite <- (agree_eval_regs _ _ _ _ _ _ _ args AG) in H; auto.
-  econstructor; eauto with coqlib. apply agree_undef_temps; auto.
+  apply plus_one. eapply exec_Mcond_false; eauto.
+  eapply eval_condition_inject; eauto. eapply agree_reglist; eauto.
+  econstructor; eauto with coqlib.
+  apply agree_regs_undef_temps; auto.
+  apply agree_frame_undef_temps; auto.
 
   (* Ljumptable *)
+  assert (rs0 arg = Vint n).
+    generalize (AGREGS arg). rewrite H. intro IJ; inv IJ; auto.
   econstructor; split.
-  apply plus_one; eapply exec_Mjumptable.
-  rewrite <- (agree_eval_reg _ _ _ _ _ _ _ arg AG) in H; eauto.
-  eauto. 
+  apply plus_one; eapply exec_Mjumptable; eauto. 
   apply transl_find_label; eauto.
-  econstructor; eauto. apply agree_undef_temps; auto.
-  eapply find_label_incl; eauto.
+  econstructor; eauto.
+  apply agree_regs_undef_temps; auto.
+  apply agree_frame_undef_temps; auto.
+  eapply find_label_tail; eauto.
 
   (* Lreturn *)
-  exploit restore_callee_save_correct; eauto.
-  intros [ls' [A [B C]]].
+  exploit function_epilogue_correct; eauto.
+  intros [rs1 [m1' [P [Q [R [S [T [U [V W]]]]]]]]].
   econstructor; split.
-  eapply plus_right. eauto. 
-  simpl shift_sp. econstructor; eauto.
-  rewrite (stacksize_preserved _ _ TRANSL); eauto.
+  eapply plus_right. eexact S. econstructor; eauto.
   traceEq.
-  econstructor; eauto. 
-  intros. symmetry. eapply agree_return_regs; eauto.
-  apply agree_callee_save_return_regs.  
+  econstructor; eauto.
+  apply match_stacks_change_bounds with stk sp'.
+  apply match_stacks_change_linear_mem with m. 
+  apply match_stacks_change_mach_mem with m'0.
+  eauto. 
+  eauto with mem. intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega. 
+  intros. rewrite <- H1. eapply Mem.load_free; eauto. left; unfold block; omega.
+  eauto with mem. intros. eapply Mem.bounds_free; eauto.
+  apply Zlt_le_weak. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. 
+  apply Zlt_le_weak. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. 
+  apply wt_return_regs; auto. eapply match_stacks_wt_locset; eauto. eapply agree_wt_ls; eauto.
 
   (* internal function *)
-  generalize TRANSL; clear TRANSL. 
-  unfold transf_fundef, transf_partial_fundef.
+  revert TRANSL. unfold transf_fundef, transf_partial_fundef.
   caseEq (transf_function f); simpl; try congruence.
   intros tfn TRANSL EQ. inversion EQ; clear EQ; subst tf.
   inversion WTF as [|f' WTFN]. subst f'.
-  set (sp := Vptr stk Int.zero) in *.
-  set (tsp := shift_sp tfn sp).
-  set (fe := make_env (function_bounds f)).
-  exploit save_callee_save_correct; eauto. 
-  intros [fr [EXP AG]].
+  exploit function_prologue_correct; eauto.
+  eapply match_stacks_type_sp; eauto. 
+  eapply match_stacks_type_retaddr; eauto.
+  intros [j' [m2' [sp' [m3' [m4' [m5' [A [B [C [D [E [F [G [J [K L]]]]]]]]]]]]]]].
   econstructor; split.
-  eapply plus_left.
-  eapply exec_function_internal; eauto.
-  rewrite (unfold_transf_function f tfn TRANSL); simpl; eexact H. 
-  replace (Mach.fn_code tfn) with
-          (transl_body f (make_env (function_bounds f))).    
-  replace (Vptr stk (Int.repr (- fn_framesize tfn))) with tsp.
-  unfold transl_body. eexact EXP.
-  unfold tsp, shift_sp, sp. unfold Val.add. 
-  rewrite Int.add_commut. rewrite Int.add_zero. auto.
-  rewrite (unfold_transf_function f tfn TRANSL). simpl. auto.
-  traceEq.
-  unfold tsp. econstructor; eauto with coqlib.
-  eapply agree_callee_save_agree; eauto. 
+  eapply plus_left. econstructor; eauto. 
+  rewrite (unfold_transf_function _ _ TRANSL). unfold fn_code. unfold transl_body. 
+  eexact D. traceEq.
+  generalize (Mem.alloc_result _ _ _ _ _ H). intro SP_EQ. 
+  generalize (Mem.alloc_result _ _ _ _ _ A). intro SP'_EQ.
+  econstructor; eauto. 
+  apply match_stacks_change_mach_mem with m'0.
+  apply match_stacks_change_linear_mem with m.
+  rewrite SP_EQ; rewrite SP'_EQ.
+  eapply match_stacks_change_meminj; eauto. omega.
+  eauto with mem. intros. eapply Mem.bounds_alloc_other; eauto. unfold block; omega. 
+  intros. eapply stores_in_frame_valid; eauto with mem. 
+  intros. eapply stores_in_frame_perm; eauto with mem.
+  intros. rewrite <- H1. transitivity (Mem.load chunk m2' b ofs). eapply stores_in_frame_contents; eauto.
+  eapply Mem.load_alloc_unchanged; eauto. red. congruence.
+  auto with coqlib.
 
   (* external function *)
   simpl in TRANSL. inversion TRANSL; subst tf.
   inversion WTF. subst ef0.
-  exploit transl_external_arguments; eauto. intro EXTARGS.
+  exploit transl_external_arguments; eauto. intros [vl [ARGS VINJ]].
+  exploit external_call_mem_inject; eauto. 
+  eapply match_stacks_preserves_globals; eauto.
+  intros [j' [res' [m1' [A [B [C [D [E [F G]]]]]]]]].
   econstructor; split.
   apply plus_one. eapply exec_function_external; eauto.
   eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
   econstructor; eauto.
-  intros. unfold Regmap.set. case (RegEq.eq r (loc_result (ef_sig ef))); intro.
-  rewrite e. rewrite Locmap.gss; auto. rewrite Locmap.gso; auto.
-  red; auto.
-  apply agree_callee_save_set_result; auto.
+  apply match_stacks_change_bounds with (Mem.nextblock m) (Mem.nextblock m'0).
+  eapply match_stack_change_extcall; eauto. omega. omega.
+  exploit external_call_valid_block. eexact H. 
+    instantiate (1 := (Mem.nextblock m - 1)). red; omega. unfold Mem.valid_block; omega.
+  exploit external_call_valid_block. eexact A. 
+    instantiate (1 := (Mem.nextblock m'0 - 1)). red; omega. unfold Mem.valid_block; omega.
+  apply wt_setloc; auto. simpl. rewrite loc_result_type.
+  change (Val.has_type res (proj_sig_res (ef_sig ef))). 
+  eapply external_call_well_typed; eauto. 
+  apply agree_regs_set_reg; auto. apply agree_regs_inject_incr with j; auto. 
+  apply agree_callee_save_set_result; auto. 
 
   (* return *)
-  inv STACKS. 
+  inv STACKS. simpl in AGLOCS.  
   econstructor; split.
   apply plus_one. apply exec_return. 
-  econstructor; eauto. simpl in AG2.  
-  eapply agree_frame_agree; eauto.
+  econstructor; eauto.
+  apply agree_frame_return with rs0; auto. 
 Qed.
 
 Lemma transf_initial_states:
   forall st1, Linear.initial_state prog st1 ->
-  exists st2, Machabstr.initial_state tprog st2 /\ match_states st1 st2.
+  exists st2, Machconcr.initial_state tprog st2 /\ match_states st1 st2.
 Proof.
-  intros. inversion H.
+  intros. inv H.
   exploit function_ptr_translated; eauto. intros [tf [FIND TR]].
   econstructor; split.
   econstructor. 
   eapply Genv.init_mem_transf_partial; eauto.
   rewrite (transform_partial_program_main _ _ TRANSF). 
   rewrite symbols_preserved. eauto.
-  eauto. 
-  econstructor; eauto. constructor. 
-  eapply Genv.find_funct_ptr_prop; eauto.
-  intros. rewrite H3 in H5. simpl in H5. contradiction.
-  simpl; red; auto.
+  econstructor; eauto.
+  eapply Genv.initmem_inject; eauto.
+  apply match_stacks_empty with (Mem.nextblock m0). omega. omega.
+  constructor.
+    apply Mem.nextblock_pos.
+    intros. unfold Mem.flat_inj. apply zlt_true; auto.
+    unfold Mem.flat_inj; intros. destruct (zlt b1 (Mem.nextblock m0)); congruence.
+    intros. change (Mem.valid_block m0 b0). eapply Genv.find_symbol_not_fresh; eauto.
+    intros. change (Mem.valid_block m0 b0). eapply Genv.find_var_info_not_fresh; eauto.
+  rewrite H3. red; intros. contradiction.
+  eapply Genv.find_funct_ptr_prop. eexact wt_prog. 
+  fold ge0; eauto.
+  apply wt_init.
+  unfold Locmap.init. red; intros; auto.
+  unfold parent_locset. red; auto.
 Qed.
 
 Lemma transf_final_states:
   forall st1 st2 r, 
-  match_states st1 st2 -> Linear.final_state st1 r -> Machabstr.final_state st2 r.
+  match_states st1 st2 -> Linear.final_state st1 r -> Machconcr.final_state st2 r.
 Proof.
-  intros. inv H0. inv H. inv STACKS. econstructor. rewrite AG1; auto.
+  intros. inv H0. inv H. inv STACKS.
+  constructor.
+  set (rres := loc_result {| sig_args := nil; sig_res := Some Tint |}) in *.
+  generalize (AGREGS rres). rewrite H1. intros IJ; inv IJ. auto.
 Qed.
 
 Theorem transf_program_correct:
   forall (beh: program_behavior), not_wrong beh ->
-  Linear.exec_program prog beh -> Machabstr.exec_program tprog beh.
+  Linear.exec_program prog beh -> Machconcr.exec_program tprog beh.
 Proof.
-  unfold Linear.exec_program, Machabstr.exec_program; intros.
+  unfold Linear.exec_program, Machconcr.exec_program; intros.
   eapply simulation_plus_preservation; eauto.
   eexact transf_initial_states.
   eexact transf_final_states.
diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v
index b42dbbb..d00d1b2 100644
--- a/backend/Stackingtyping.v
+++ b/backend/Stackingtyping.v
@@ -204,42 +204,20 @@ Lemma wt_transf_function:
   wt_function tf.
 Proof.
   intros. 
-  generalize H; unfold transf_function.
-  case (zlt (Linear.fn_stacksize f) 0); intro.
-  intros; discriminate.
-  case (zlt (- Int.min_signed) (fe_size (make_env (function_bounds f)))); intro.
-  intros; discriminate. intro EQ.
-  generalize (unfold_transf_function f tf H); intro.
+  exploit unfold_transf_function; eauto. intro EQ.
   set (b := function_bounds f) in *.
   set (fe := make_env b) in *.
-  assert (fn_framesize tf = fe_size fe).
-    subst tf; reflexivity.
-  assert (Int.signed tf.(fn_link_ofs) = offset_of_index fe FI_link).
-    rewrite H1; unfold fn_link_ofs. 
-    change (fe_ofs_link fe) with (offset_of_index fe FI_link).
-    unfold fe, b; eapply offset_of_index_no_overflow. eauto. red; auto. 
-  assert (Int.signed tf.(fn_retaddr_ofs) = offset_of_index fe FI_retaddr).
-    rewrite H1; unfold fn_retaddr_ofs. 
-    change (fe_ofs_retaddr fe) with (offset_of_index fe FI_retaddr).
-    unfold fe, b; eapply offset_of_index_no_overflow. eauto. red; auto. 
   constructor.
   change (wt_instrs (fn_code tf)).
-  rewrite H1; simpl; unfold transl_body. 
+  rewrite EQ; simpl; unfold transl_body. 
   unfold fe, b; apply wt_save_callee_save; auto. 
   unfold transl_code. apply wt_fold_right. 
   intros. eapply wt_transl_instr; eauto. 
-  red; intros. elim H5.
-  subst tf; simpl; auto.
-  rewrite H2. generalize (size_pos f). fold b; fold fe; omega.
-  rewrite H1. change (4 | fe_size fe). unfold fe, b. apply frame_size_aligned.   
-  rewrite H3; rewrite H2. change 4 with (4 * typesize (type_of_index FI_link)).
-  unfold fe, b; apply offset_of_index_valid. red; auto.
-  rewrite H3. unfold fe,b; apply offset_of_index_aligned.
-  rewrite H4; rewrite H2. change 4 with (4 * typesize (type_of_index FI_retaddr)).
-  unfold fe, b; apply offset_of_index_valid. red; auto.
-  rewrite H4. unfold fe,b; apply offset_of_index_aligned.
-  rewrite H3; rewrite H4.
-  apply (offset_of_index_disj f FI_retaddr FI_link); red; auto.
+  red; intros. elim H1.
+  rewrite EQ; unfold fn_stacksize.
+  generalize (size_pos f).
+  generalize (size_no_overflow _ _ H).
+  unfold fe, b. omega.
 Qed.
 
 Lemma wt_transf_fundef:
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
index 11e6be2..ca8e915 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -512,14 +512,14 @@ Proof.
   TransfInstr. 
   left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) ifso rs' m'); split.
   eapply exec_Icond_true; eauto.
-  apply eval_condition_lessdef with (rs##args); auto. apply regset_get_list; auto.
+  apply eval_condition_lessdef with (rs##args) m; auto. apply regset_get_list; auto.
   constructor; auto. 
 
 (* cond false *)
   TransfInstr. 
   left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) ifnot rs' m'); split.
   eapply exec_Icond_false; eauto.
-  apply eval_condition_lessdef with (rs##args); auto. apply regset_get_list; auto.
+  apply eval_condition_lessdef with (rs##args) m; auto. apply regset_get_list; auto.
   constructor; auto. 
 
 (* jumptable *)