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

1 files changed, 1877 insertions, 939 deletions

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.