From aaa49526068f528f2233de0dace43549432fba52 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 12 Apr 2008 12:55:21 +0000
Subject: Revu gestion retaddr et link dans Stacking

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@604 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/Machabstr2concr.v | 735 ++++++++++++++++++++++------------------------
 1 file changed, 355 insertions(+), 380 deletions(-)

(limited to 'backend/Machabstr2concr.v')

diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v
index ffdfb336..2dd3134f 100644
--- a/backend/Machabstr2concr.v
+++ b/backend/Machabstr2concr.v
@@ -27,7 +27,6 @@ Require Import Mach.
 Require Import Machtyping.
 Require Import Machabstr.
 Require Import Machconcr.
-Require Import Stackingproof.
 Require Import PPCgenretaddr.
 
 (** Two semantics were defined for the Mach intermediate language:
@@ -48,27 +47,6 @@ Require Import PPCgenretaddr.
   Mach semantics as input).
 *)
 
-Remark align_16_top_ge:
-  forall lo hi,
-  hi <= align_16_top lo hi.
-Proof.
-  intros. unfold align_16_top. apply Zmax_bound_r. 
-  assert (forall x, x <= (x + 15) / 16 * 16).
-  intro. assert (16 > 0). omega.
-  generalize (Z_div_mod_eq (x + 15) 16 H). intro.
-  replace ((x + 15) / 16 * 16) with ((x + 15) - (x + 15) mod 16).
-  generalize (Z_mod_lt (x + 15) 16 H). omega. 
-  rewrite Zmult_comm. omega.
-  generalize (H (hi - lo)). omega. 
-Qed.
-
-Remark align_16_top_pos:
-  forall lo hi,
-  0 <= align_16_top lo hi.
-Proof.
-  intros. unfold align_16_top. apply Zmax_bound_l. omega.
-Qed.
-
 Remark size_type_chunk:
   forall ty, size_chunk (chunk_of_type ty) = AST.typesize ty.
 Proof.
@@ -79,11 +57,16 @@ Qed.
 
 (** ** Agreement for one frame *)
 
+Section FRAME_MATCH.
+
+Variable f: function.
+Hypothesis wt_f: wt_function f.
+
 (** The core idea of the simulation proof is that for all active
   functions, the memory-allocated activation record, in the concrete 
   semantics, contains the same data as the Cminor stack block
   (at positive offsets) and the frame of the function (at negative
-  offsets) in the abstract semantics.
+  offsets) in the abstract semantics
 
   This intuition (activation record = Cminor stack data + frame)
   is formalized by the following predicate [frame_match fr sp base mm ms].
@@ -91,19 +74,18 @@ Qed.
   semantics. [ms] is the current memory state in the concrete semantics.
   The stack pointer is [Vptr sp base] in both semantics. *)
 
-Inductive frame_match (fr: frame) (sp: block) (base: int) 
+Inductive frame_match (fr: frame)
+                      (sp: block) (base: int) 
                       (mm ms: mem) : Prop :=
   frame_match_intro:
     valid_block ms sp ->
     low_bound mm sp = 0 ->
-    low_bound ms sp = fr.(fr_low) ->
+    low_bound ms sp = -f.(fn_framesize) ->
     high_bound ms sp >= 0 ->
-    fr.(fr_low) <= -24 ->
-    Int.min_signed <= fr.(fr_low) ->
-    base = Int.repr fr.(fr_low) ->
+    base = Int.repr (-f.(fn_framesize)) ->
     (forall ty ofs,
-       fr.(fr_low) + 24 <= ofs -> ofs + AST.typesize ty <= 0 ->
-       load (chunk_of_type ty) ms sp ofs = Some(fr.(fr_contents) ty ofs)) ->
+       -f.(fn_framesize) <= ofs -> ofs + AST.typesize ty <= 0 ->
+       load (chunk_of_type ty) ms sp ofs = Some(fr ty ofs)) ->
     frame_match fr sp base mm ms.
 
 (** The following two innocuous-looking lemmas are the key results
@@ -140,22 +122,36 @@ Qed.
   to reading the corresponding slot from the frame
   (in the abstract semantics).  *)
 
+Lemma frame_match_load_stack:
+  forall fr sp base mm ms ty ofs,
+  frame_match fr sp base mm ms ->
+  0 <= Int.signed ofs /\ Int.signed ofs + AST.typesize ty <= f.(fn_framesize) ->
+  load_stack ms (Vptr sp base) ty ofs = 
+  Some (fr ty (Int.signed ofs - f.(fn_framesize))).
+Proof.
+  intros. inv H.
+  unfold load_stack, Val.add, loadv.
+  replace (Int.signed (Int.add (Int.repr (- fn_framesize f)) ofs))
+     with (Int.signed ofs - fn_framesize f).
+  apply H6. omega. omega.
+  inv wt_f.
+  assert (Int.signed (Int.repr (-fn_framesize f)) = -fn_framesize f).
+    apply Int.signed_repr.
+    assert (0 <= Int.max_signed). compute; congruence. omega.
+  rewrite int_add_no_overflow. rewrite H. omega.
+  rewrite H. split. omega.
+  apply Zle_trans with 0. generalize (AST.typesize_pos ty). omega. 
+  compute; congruence.
+Qed.
+
 Lemma frame_match_get_slot:
   forall fr sp base mm ms ty ofs v,
   frame_match fr sp base mm ms ->
-  get_slot fr ty (Int.signed ofs) v ->
+  get_slot f fr ty (Int.signed ofs) v ->
   load_stack ms (Vptr sp base) ty ofs = Some v.
 Proof.
-  intros. inv H. inv H0. 
-  unfold load_stack, Val.add, loadv. 
-  assert (Int.signed (Int.repr (fr_low fr)) = fr_low fr).
-    apply Int.signed_repr.
-    split. auto. apply Zle_trans with (-24). auto. compute; congruence.
-  assert (Int.signed (Int.add (Int.repr (fr_low fr)) ofs) = fr_low fr + Int.signed ofs).
-    rewrite int_add_no_overflow. rewrite H0. auto.
-    rewrite H0. split. omega. apply Zle_trans with 0.
-    generalize (AST.typesize_pos ty). omega. compute; congruence.
-  rewrite H9. apply H8. omega. auto.
+  intros. inversion H. inv H0. eapply frame_match_load_stack; eauto.
+  inv H7. auto.
 Qed.
 
 (** Assigning a value to a frame slot (in the abstract semantics)
@@ -163,41 +159,42 @@ Qed.
   (in the concrete semantics).  Moreover, agreement between frames
   and activation records is preserved. *)
 
-Lemma frame_match_set_slot:
-  forall fr sp base mm ms ty ofs v fr',
+Lemma frame_match_store_stack:
+  forall fr sp base mm ms ty ofs v,
   frame_match fr sp base mm ms ->
-  set_slot fr ty (Int.signed ofs) v fr' ->
+  0 <= Int.signed ofs /\ Int.signed ofs + AST.typesize ty <= f.(fn_framesize) ->
   Val.has_type v ty ->
   Mem.extends mm ms ->
   exists ms',
     store_stack ms (Vptr sp base) ty ofs v = Some ms' /\
-    frame_match fr' sp base mm ms' /\
-    Mem.extends mm ms' /\
-    Int.signed base + 24 <= Int.signed (Int.add base ofs).
+    frame_match (update ty (Int.signed ofs - f.(fn_framesize)) v fr) sp base mm ms' /\
+    Mem.extends mm ms'.
 Proof.
-  intros. inv H. inv H0.
+  intros. inv H. inv wt_f.
   unfold store_stack, Val.add, storev.
-  assert (Int.signed (Int.repr (fr_low fr)) = fr_low fr).
-    apply Int.signed_repr.
-    split. auto. apply Zle_trans with (-24). auto. compute; congruence.
-  assert (Int.signed (Int.add (Int.repr (fr_low fr)) ofs) = fr_low fr + Int.signed ofs).
-    rewrite int_add_no_overflow. congruence. 
-    rewrite H0. split. omega. apply Zle_trans with 0.
-    generalize (AST.typesize_pos ty). omega. compute; congruence.
-  rewrite H11.
-  assert (exists ms', store (chunk_of_type ty) ms sp (fr_low fr + Int.signed ofs) v = Some ms').
+  assert (Int.signed (Int.add (Int.repr (- fn_framesize f)) ofs) =
+          Int.signed ofs - fn_framesize f).
+  assert (Int.signed (Int.repr (-fn_framesize f)) = -fn_framesize f).
+    apply Int.signed_repr. 
+    assert (0 <= Int.max_signed). compute; congruence. omega.
+  rewrite int_add_no_overflow. rewrite H. omega.
+  rewrite H. split. omega.
+  apply Zle_trans with 0. generalize (AST.typesize_pos ty). omega. 
+  compute; congruence.
+  rewrite H.
+  assert (exists ms', store (chunk_of_type ty) ms sp (Int.signed ofs - fn_framesize f) v = Some ms').
     apply valid_access_store. 
     constructor. auto. omega.
     rewrite size_type_chunk. omega.
-  destruct H12 as [ms' STORE]. 
+  destruct H7 as [ms' STORE]. 
   generalize (low_bound_store _ _ _ _ _ _ STORE sp). intro LB.
   generalize (high_bound_store _ _ _ _ _ _ STORE sp). intro HB.
   exists ms'. 
   split. exact STORE.
   (* frame match *)
-  split. constructor; simpl fr_low; try congruence.
-    eauto with mem. intros. simpl.
-    destruct (zeq (fr_low fr + Int.signed ofs) ofs0). subst ofs0.
+  split. constructor; try congruence.
+    eauto with mem. intros. unfold update.
+    destruct (zeq (Int.signed ofs - fn_framesize f) ofs0). subst ofs0.
     destruct (typ_eq ty ty0). subst ty0.
     (* same *)
     transitivity (Some (Val.load_result (chunk_of_type ty) v)).
@@ -206,33 +203,45 @@ Proof.
     (* mismatch *)
     eapply load_store_mismatch'; eauto with mem.
     destruct ty; destruct ty0; simpl; congruence.
-    destruct (zle (ofs0 + AST.typesize ty0) (fr_low fr + Int.signed ofs)).
+    destruct (zle (ofs0 + AST.typesize ty0) (Int.signed ofs - fn_framesize f)).
     (* disjoint *)
-    rewrite <- H10; auto. eapply load_store_other; eauto.
+    rewrite <- H8; auto. eapply load_store_other; eauto.
     right; left. rewrite size_type_chunk; auto.
-    destruct (zle (fr_low fr + Int.signed ofs + AST.typesize ty)).
-    rewrite <- H10; auto. eapply load_store_other; eauto.
+    destruct (zle (Int.signed ofs - fn_framesize f + AST.typesize ty)).
+    rewrite <- H8; auto. eapply load_store_other; eauto.
     right; right. rewrite size_type_chunk; auto.
     (* overlap *)
     eapply load_store_overlap'; eauto with mem.
     rewrite size_type_chunk; auto. 
     rewrite size_type_chunk; auto.
   (* extends *)
-  split. eapply store_outside_extends; eauto.
+  eapply store_outside_extends; eauto.
   left. rewrite size_type_chunk. omega.
-  (* bound *)
-  omega.
+Qed.
+
+Lemma frame_match_set_slot:
+  forall fr sp base mm ms ty ofs v fr',
+  frame_match fr sp base mm ms ->
+  set_slot f fr ty (Int.signed ofs) v fr' ->
+  Val.has_type v ty ->
+  Mem.extends mm ms ->
+  exists ms',
+    store_stack ms (Vptr sp base) ty ofs v = Some ms' /\
+    frame_match fr' sp base mm ms' /\
+    Mem.extends mm ms'.
+Proof.
+  intros. inv H0. eapply frame_match_store_stack; eauto. 
+  inv H3. auto.
 Qed.
 
 (** Agreement is preserved by stores within blocks other than the
-  one pointed to by [sp], or to the low 24 bytes
-  of the [sp] block. *)
+  one pointed to by [sp]. *)
 
 Lemma frame_match_store_other:
   forall fr sp base mm ms chunk b ofs v ms',
   frame_match fr sp base mm ms ->
   store chunk ms b ofs v = Some ms' ->
-  sp <> b \/ ofs + size_chunk chunk <= fr_low fr + 24 ->
+  sp <> b ->
   frame_match fr sp base mm ms'.
 Proof.
   intros. inv H. 
@@ -242,11 +251,13 @@ Proof.
   eauto with mem. 
   congruence.
   congruence.
-  intros. rewrite <- H9; auto. 
+  intros. rewrite <- H7; auto. 
   eapply load_store_other; eauto.
-  elim H1; intro. auto. right. rewrite size_type_chunk. omega. 
 Qed.
 
+(** Agreement is preserved by parallel stores in the Machabstr
+  and the Machconcr semantics. *)
+
 Lemma frame_match_store:
   forall fr sp base mm ms chunk b ofs v mm' ms',
   frame_match fr sp base mm ms ->
@@ -262,31 +273,11 @@ Proof.
   apply frame_match_intro; auto.
   eauto with mem.
   congruence. congruence. congruence.
-  intros. rewrite <- H9; auto. eapply load_store_other; eauto.
+  intros. rewrite <- H7; auto. eapply load_store_other; eauto.
   destruct (zeq sp b). subst b. right. 
   rewrite size_type_chunk. 
   assert (valid_access mm chunk sp ofs) by eauto with mem.
-  inv H10. left. omega.
-  auto.
-Qed.
-
-(** The low 24 bytes of a frame are preserved by a parallel
-    store in the two memory states. *)
-
-Lemma frame_match_store_link_invariant:
-  forall fr sp base mm ms chunk b ofs v mm' ms' ofs',
-  frame_match fr sp base mm ms ->
-  store chunk mm b ofs v = Some mm' ->
-  store chunk ms b ofs v = Some ms' ->
-  ofs' <= fr_low fr + 20 -> 
-  load Mint32 ms' sp ofs' = load Mint32 ms sp ofs'.
-Proof.
-  intros. inv H.
-  eapply load_store_other; eauto.
-  destruct (eq_block sp b). subst b.
-  right; left. change (size_chunk Mint32) with 4. 
-  assert (valid_access mm chunk sp ofs) by eauto with mem.
-  inv H. omega. 
+  inv H8. left. omega.
   auto.
 Qed.
 
@@ -297,14 +288,12 @@ Qed.
   remain true. *)
 
 Lemma frame_match_new:
-  forall mm ms mm' ms' sp sp' f,
+  forall mm ms mm' ms' sp sp',
   mm.(nextblock) = ms.(nextblock) ->
   alloc mm 0 f.(fn_stacksize) = (mm', sp) ->
-  alloc ms (- f.(fn_framesize)) (align_16_top (- f.(fn_framesize)) f.(fn_stacksize)) = (ms', sp') ->
-  f.(fn_framesize) >= 24 ->
-  f.(fn_framesize) <= -Int.min_signed ->
+  alloc ms (- f.(fn_framesize)) f.(fn_stacksize) = (ms', sp') ->
   sp = sp' /\
-  frame_match (init_frame f) sp (Int.repr (-f.(fn_framesize))) mm' ms'.
+  frame_match empty_frame sp (Int.repr (-f.(fn_framesize))) mm' ms'.
 Proof.
   intros. 
   assert (sp = sp').
@@ -315,13 +304,12 @@ Proof.
   generalize (low_bound_alloc_same _ _ _ _ _ H1). intro LBs.
   generalize (high_bound_alloc_same _ _ _ _ _ H0). intro HBm.
   generalize (high_bound_alloc_same _ _ _ _ _ H1). intro HBs.
+  inv wt_f.
   constructor; simpl; eauto with mem.
-  rewrite HBs. apply Zle_ge. apply align_16_top_pos.
-  omega. omega.
+  rewrite HBs. auto.
   intros.
-  eapply load_alloc_same'; eauto. omega. 
-  rewrite size_type_chunk. apply Zle_trans with 0. auto.
-  apply align_16_top_pos.
+  eapply load_alloc_same'; eauto.  
+  rewrite size_type_chunk. omega.
 Qed.
 
 Lemma frame_match_alloc:
@@ -334,13 +322,13 @@ Lemma frame_match_alloc:
 Proof.
   intros. inversion H0.
   assert (valid_block mm sp). red. rewrite H. auto.
-  exploit low_bound_alloc_other. eexact H1. eexact H11. intro LBm.
-  exploit high_bound_alloc_other. eexact H1. eexact H11. intro HBm.
+  exploit low_bound_alloc_other. eexact H1. eexact H9. intro LBm.
+  exploit high_bound_alloc_other. eexact H1. eexact H9. intro HBm.
   exploit low_bound_alloc_other. eexact H2. eexact H3. intro LBs.
   exploit high_bound_alloc_other. eexact H2. eexact H3. intro HBs.
   apply frame_match_intro.
   eapply valid_block_alloc; eauto.
-  congruence. congruence. congruence. auto. auto. auto. 
+  congruence. congruence. congruence. auto. auto.
   intros. eapply load_alloc_other; eauto. 
 Qed.
 
@@ -360,9 +348,138 @@ Proof.
   generalize (high_bound_free ms _ _ H0); intro HBs.
   apply frame_match_intro; auto.
   congruence. congruence. congruence.
-  intros. rewrite <- H8; auto. apply load_free. auto.
+  intros. rewrite <- H6; auto. apply load_free. auto.
+Qed.
+
+End FRAME_MATCH.
+
+(** ** Accounting for the return address and back link *)
+
+Section EXTEND_FRAME.
+
+Variable f: function.
+Hypothesis wt_f: wt_function f.
+Variable cs: list Machconcr.stackframe.
+
+Definition extend_frame (fr: frame) : frame :=
+  update Tint (Int.signed f.(fn_retaddr_ofs) - f.(fn_framesize)) (parent_ra cs)
+    (update Tint (Int.signed f.(fn_link_ofs) - f.(fn_framesize)) (parent_sp cs)
+      fr).
+
+Lemma get_slot_extends:
+  forall fr ty ofs v,
+  get_slot f fr ty ofs v ->
+  get_slot f (extend_frame fr) ty ofs v.
+Proof.
+  intros. inv H. constructor. auto.
+  inv H0. inv wt_f. generalize (AST.typesize_pos ty); intro.
+  unfold extend_frame. rewrite update_other. rewrite update_other. auto.
+  simpl; omega. simpl; omega.
+Qed.
+
+Lemma update_commut:
+  forall ty1 ofs1 v1 ty2 ofs2 v2 fr,
+  ofs1 + AST.typesize ty1 <= ofs2 \/
+  ofs2 + AST.typesize ty2 <= ofs1 ->
+  update ty1 ofs1 v1 (update ty2 ofs2 v2 fr) =
+  update ty2 ofs2 v2 (update ty1 ofs1 v1 fr).
+Proof.
+  intros. unfold frame.
+  apply extensionality. intro ty. apply extensionality. intro ofs.
+  generalize (AST.typesize_pos ty1).
+  generalize (AST.typesize_pos ty2).
+  generalize (AST.typesize_pos ty); intros.
+  unfold update.
+  set (sz1 := AST.typesize ty1) in *.
+  set (sz2 := AST.typesize ty2) in *.
+  set (sz := AST.typesize ty) in *.
+  destruct (zeq ofs1 ofs).
+  rewrite zeq_false. 
+  destruct (zle (ofs + sz) ofs2). auto.
+  destruct (zle (ofs2 + sz2) ofs). auto.
+  destruct (typ_eq ty1 ty); auto.
+  replace sz with sz1 in z. omegaContradiction. unfold sz1, sz; congruence.
+  omega.
+
+  destruct (zle (ofs + sz) ofs1).
+  auto.
+  destruct (zle (ofs1 + sz1) ofs).
+  auto.
+
+  destruct (zeq ofs2 ofs).
+  destruct (typ_eq ty2 ty); auto.
+  replace sz with sz2 in z. omegaContradiction. unfold sz2, sz; congruence.
+  destruct (zle (ofs + sz) ofs2); auto.
+  destruct (zle (ofs2 + sz2) ofs); auto.
+Qed.
+
+Lemma set_slot_extends:
+  forall fr ty ofs v fr',
+  set_slot f fr ty ofs v fr' ->
+  set_slot f (extend_frame fr) ty ofs v (extend_frame fr').
+Proof.
+  intros. inv H. constructor. auto.
+  inv H0. inv wt_f. generalize (AST.typesize_pos ty); intro.
+  unfold extend_frame. 
+  rewrite (update_commut ty). rewrite (update_commut ty). auto.
+  simpl. omega. 
+  simpl. omega.
+Qed.
+
+Lemma frame_match_load_link:
+  forall fr sp base mm ms,
+  frame_match f (extend_frame fr) sp base mm ms ->
+  load_stack ms (Vptr sp base) Tint f.(fn_link_ofs) = Some (parent_sp cs).
+Proof.
+  intros. inversion wt_f.
+  replace (parent_sp cs) with
+   (extend_frame fr Tint (Int.signed f.(fn_link_ofs) - f.(fn_framesize))).
+  eapply frame_match_load_stack; eauto.
+  unfold extend_frame. rewrite update_other. apply update_same. simpl. omega. 
+Qed.
+
+Lemma frame_match_load_retaddr:
+  forall fr sp base mm ms,
+  frame_match f (extend_frame fr) sp base mm ms ->
+  load_stack ms (Vptr sp base) Tint f.(fn_retaddr_ofs) = Some (parent_ra cs).
+Proof.
+  intros. inversion wt_f.
+  replace (parent_ra cs) with
+   (extend_frame fr Tint (Int.signed f.(fn_retaddr_ofs) - f.(fn_framesize))).
+  eapply frame_match_load_stack; eauto.
+  unfold extend_frame. apply update_same.
+Qed.
+
+Lemma frame_match_function_entry:
+  forall mm ms mm' ms1 sp sp',
+  extends mm ms ->
+  alloc mm 0 f.(fn_stacksize) = (mm', sp) ->
+  alloc ms (- f.(fn_framesize)) f.(fn_stacksize) = (ms1, sp') ->
+  Val.has_type (parent_sp cs) Tint ->
+  Val.has_type (parent_ra cs) Tint ->
+  let base := Int.repr (-f.(fn_framesize)) in
+  exists ms2, exists ms3,
+  sp = sp' /\
+  store_stack ms1 (Vptr sp base) Tint f.(fn_link_ofs) (parent_sp cs) = Some ms2 /\
+  store_stack ms2 (Vptr sp base) Tint f.(fn_retaddr_ofs) (parent_ra cs) = Some ms3 /\
+  frame_match f (extend_frame empty_frame) sp base mm' ms3 /\
+  extends mm' ms3.
+Proof.
+  intros. inversion wt_f.
+  exploit alloc_extends; eauto. omega. omega. intros [A EXT0].
+  exploit frame_match_new. eauto. inv H. eexact H4. eauto. eauto. eauto.
+  fold base. intros [C FM0].
+  destruct (frame_match_store_stack _ wt_f _ _ _ _ _ Tint _ _
+              FM0 wt_function_link H2 EXT0)
+  as [ms2 [STORE1 [FM1 EXT1]]].
+  destruct (frame_match_store_stack _ wt_f _ _ _ _ _ Tint _ _
+              FM1 wt_function_retaddr H3 EXT1)
+  as [ms3 [STORE2 [FM3 EXT3]]].
+  exists ms2; exists ms3; auto.
 Qed.
 
+End EXTEND_FRAME.
+
 (** ** Invariant for stacks *)
 
 Section SIMULATION.
@@ -380,31 +497,27 @@ Let ge := Genv.globalenv p.
   their addresses increase strictly from caller to callee.
 *)
 
+Definition stack_below (ts: list Machconcr.stackframe) (b: block) : Prop :=
+  match parent_sp ts with
+  | Vptr sp base' => sp < b
+  | _ => False
+  end.
+
 Inductive match_stacks: 
       list Machabstr.stackframe -> list Machconcr.stackframe ->
-      block -> int -> mem -> mem -> Prop :=
-  | match_stacks_nil: forall sp base mm ms,
-      load Mint32 ms sp (Int.signed base) = Some (Vptr Mem.nullptr Int.zero) ->
-      load Mint32 ms sp (Int.signed base + 12) = Some Vzero ->
-      match_stacks nil nil sp base mm ms
-  | match_stacks_cons: forall f sp' base' c fr s fb ra ts sp base mm ms,
-      frame_match fr sp' base' mm ms ->
-      sp' < sp ->
-      load Mint32 ms sp (Int.signed base) = Some (Vptr sp' base') ->
-      load Mint32 ms sp (Int.signed base + 12) = Some ra ->
+      mem -> mem -> Prop :=
+  | match_stacks_nil: forall mm ms,
+      match_stacks nil nil mm ms
+  | match_stacks_cons: forall fb sp base c fr s f ra ts mm ms,
       Genv.find_funct_ptr ge fb = Some (Internal f) ->
-      match_stacks s ts sp' base' mm ms ->
-      match_stacks (Machabstr.Stackframe f (Vptr sp' base') c fr :: s)
-                   (Machconcr.Stackframe fb (Vptr sp' base') ra c :: ts)
-                   sp base mm ms.
-
-Remark frame_match_base_eq:
-  forall fr sp base mm ms,
-  frame_match fr sp base mm ms -> Int.signed base = fr_low fr.
-Proof.
-  intros. inv H. apply Int.signed_repr. split; auto.
-  apply Zle_trans with (-24); auto. compute; congruence.
-Qed.
+      wt_function f ->
+      frame_match f (extend_frame f ts fr) sp base mm ms ->
+      stack_below ts sp ->
+      Val.has_type ra Tint ->
+      match_stacks s ts mm ms ->
+      match_stacks (Machabstr.Stackframe f (Vptr sp base) c fr :: s)
+                   (Machconcr.Stackframe fb (Vptr sp base) ra c :: ts)
+                   mm ms.
 
 (** If [match_stacks] holds, a lookup in the parent frame in the
   Machabstr semantics corresponds to two memory loads in the
@@ -412,230 +525,128 @@ Qed.
   activation record, the second to read within this record. *)
 
 Lemma match_stacks_get_parent:
-  forall s ts sp base mm ms ty ofs v,
-  match_stacks s ts sp base mm ms ->
-  get_slot (parent_frame s) ty (Int.signed ofs) v ->
-  exists parent,
-     load_stack ms (Vptr sp base) Tint (Int.repr 0) = Some parent
-  /\ load_stack ms parent ty ofs = Some v.
+  forall s ts mm ms ty ofs v,
+  match_stacks s ts mm ms ->
+  get_slot (parent_function s) (parent_frame s) ty (Int.signed ofs) v ->
+  load_stack ms (Machconcr.parent_sp ts) ty ofs = Some v.
 Proof.
   intros. inv H; simpl in H0. 
-  inv H0. simpl in H3. elimtype False. generalize (AST.typesize_pos ty). omega.
-  exists (Vptr sp' base'); split.
-  unfold load_stack. simpl. rewrite Int.add_zero. auto.
-  eapply frame_match_get_slot; eauto.
+  inv H0. inv H. simpl in H1. elimtype False. generalize (AST.typesize_pos ty). omega.
+  simpl. eapply frame_match_get_slot; eauto.
+  eapply get_slot_extends; eauto. 
 Qed.
 
-(** If [match_stacks] holds, reading memory at offsets 0 and 12
-  from the stack pointer returns the stack pointer and return
-  address of the caller, respectively. *)
+(** Preservation of the [match_stacks] invariant
+    by various kinds of memory stores. *)
 
-Lemma match_stacks_load_links:
-  forall fr s ts sp base mm ms,
-  frame_match fr sp base mm ms ->
-  match_stacks s ts sp base mm ms ->
-  load_stack ms (Vptr sp base) Tint (Int.repr 0) = Some (parent_sp ts) /\
-  load_stack ms (Vptr sp base) Tint (Int.repr 12) = Some (parent_ra ts).
-Proof.
-  intros. unfold load_stack. simpl. rewrite Int.add_zero.
-  replace (Int.signed (Int.add base (Int.repr 12)))
-     with (Int.signed base + 12).
-  inv H0; simpl; auto.
-  inv H. rewrite Int.add_signed. 
-  change (Int.signed (Int.repr 12)) with 12.
-  repeat rewrite Int.signed_repr. auto.
-  split. omega. apply Zle_trans with (-12). omega. compute; congruence.
-  split. auto. apply Zle_trans with (-24). auto. compute; congruence.
-Qed.
-
-(** The [match_stacks] invariant is preserved by memory stores
-  outside the 24-byte reserved area at the bottom of activation records.
-*)
+Remark stack_below_trans:
+  forall ts b b', 
+  stack_below ts b -> b <= b' -> stack_below ts b'.
+Proof.
+  unfold stack_below; intros. 
+  destruct (parent_sp ts); auto. omega.
+Qed.
 
 Lemma match_stacks_store_other:
-  forall s ts sp base ms mm,
-  match_stacks s ts sp base mm ms ->
+  forall s ts ms mm,
+  match_stacks s ts mm ms ->
   forall chunk b ofs v ms',
   store chunk ms b ofs v = Some ms' ->
-  sp < b ->
-  match_stacks s ts sp base mm ms'.
+  stack_below ts b ->
+  match_stacks s ts mm ms'.
 Proof.
   induction 1; intros.
-  assert (sp <> b). unfold block; omega.
   constructor.
-  rewrite <- H. eapply load_store_other; eauto.
-  rewrite <- H0. eapply load_store_other; eauto.
-  assert (sp <> b). unfold block; omega.
+  red in H6; simpl in H6. 
   econstructor; eauto.
   eapply frame_match_store_other; eauto.
-  left. unfold block; omega.
-  rewrite <- H1. eapply load_store_other; eauto.
-  rewrite <- H2. eapply load_store_other; eauto.
-  eapply IHmatch_stacks; eauto. omega.
+  unfold block; omega.
+  eapply IHmatch_stacks; eauto.
+  eapply stack_below_trans; eauto. omega.
 Qed.
 
 Lemma match_stacks_store_slot:
-  forall s ts sp base ms mm,
-  match_stacks s ts sp base mm ms ->
-  forall ty ofs v ms',
-  store_stack ms (Vptr sp base) ty ofs v = Some ms' ->
-  Int.signed base + 24 <= Int.signed (Int.add base ofs) ->
-  match_stacks s ts sp base mm ms'.
+  forall s ts ms mm,
+  match_stacks s ts mm ms ->
+  forall ty ofs v ms' b i,
+  stack_below ts b ->
+  store_stack ms (Vptr b i) ty ofs v = Some ms' ->
+  match_stacks s ts mm ms'.
 Proof.
   intros.
-  unfold store_stack in H0. simpl in H0. 
-  assert (load Mint32 ms' sp (Int.signed base) = load Mint32 ms sp (Int.signed base)).
-  eapply load_store_other; eauto.
-  right; left. change (size_chunk Mint32) with 4; omega.
-  assert (load Mint32 ms' sp (Int.signed base + 12) = load Mint32 ms sp (Int.signed base + 12)).
-  eapply load_store_other; eauto.
-  right; left. change (size_chunk Mint32) with 4; omega.
+  unfold store_stack in H1. simpl in H1.
   inv H.
-  constructor; congruence.
-  constructor; auto.
+  constructor.
+  red in H0; simpl in H0.
+  econstructor; eauto.
   eapply frame_match_store_other; eauto.
-  left; unfold block; omega.
-  congruence. congruence.
+  unfold block; omega.
   eapply match_stacks_store_other; eauto. 
+  eapply stack_below_trans; eauto. omega.
 Qed.
 
 Lemma match_stacks_store:
-  forall s ts sp base ms mm,
-  match_stacks s ts sp base mm ms ->
-  forall fr chunk b ofs v mm' ms',
-  frame_match fr sp base mm ms ->
+  forall s ts ms mm,
+  match_stacks s ts mm ms ->
+  forall chunk b ofs v mm' ms',
   store chunk mm b ofs v = Some mm' ->
   store chunk ms b ofs v = Some ms' ->
-  match_stacks s ts sp base mm' ms'.
+  match_stacks s ts mm' ms'.
 Proof.
   induction 1; intros.
-  assert (Int.signed base = fr_low fr) by (eapply frame_match_base_eq; eauto).
   constructor.
-  rewrite <- H. eapply frame_match_store_link_invariant; eauto. omega.
-  rewrite <- H0. eapply frame_match_store_link_invariant; eauto. omega.
-  assert (Int.signed base = fr_low fr0) by (eapply frame_match_base_eq; eauto).
   econstructor; eauto.
-  eapply frame_match_store; eauto. 
-  rewrite <- H1. eapply frame_match_store_link_invariant; eauto. omega.
-  rewrite <- H2. eapply frame_match_store_link_invariant; eauto. omega.
+  eapply frame_match_store; eauto.
 Qed.
 
 Lemma match_stacks_alloc:
-  forall s ts sp base ms mm,
-  match_stacks s ts sp base mm ms ->
+  forall s ts ms mm,
+  match_stacks s ts mm ms ->
   forall lom him mm' bm los his ms' bs,
   mm.(nextblock) = ms.(nextblock) ->
   alloc mm lom him = (mm', bm) ->
   alloc ms los his = (ms', bs) ->
-  match_stacks s ts sp base mm' ms'.
+  match_stacks s ts mm' ms'.
 Proof.
   induction 1; intros.
   constructor.
-  rewrite <- H; eapply load_alloc_unchanged; eauto with mem.
-  rewrite <- H0; eapply load_alloc_unchanged; eauto with mem.
   econstructor; eauto.
   eapply frame_match_alloc; eauto.
-  rewrite <- H1; eapply load_alloc_unchanged; eauto with mem.
-  rewrite <- H2; eapply load_alloc_unchanged; eauto with mem.
 Qed.
 
 Lemma match_stacks_free:
-  forall s ts sp base ms mm,
-  match_stacks s ts sp base mm ms ->
+  forall s ts ms mm,
+  match_stacks s ts mm ms ->
   forall b,
-  sp < b ->
-  match_stacks s ts sp base (Mem.free mm b) (Mem.free ms b).
+  stack_below ts b ->
+  match_stacks s ts (Mem.free mm b) (Mem.free ms b).
 Proof.
   induction 1; intros.
-  assert (sp <> b). unfold block; omega.
   constructor.
-  rewrite <- H. apply load_free; auto.
-  rewrite <- H0. apply load_free; auto.
-  assert (sp <> b). unfold block; omega.
+  red in H5; simpl in H5.
   econstructor; eauto.
   eapply frame_match_free; eauto. unfold block; omega.
-  rewrite <- H1. apply load_free; auto.
-  rewrite <- H2. apply load_free; auto.
-  eapply IHmatch_stacks; eauto. omega.
-Qed.
-
-(** Invocation of a function temporarily violates the [mach_stacks]
-  invariant: the return address and back link are not yet stored
-  in the appropriate parts of the activation record.  
-  The following [match_stacks_partial] predicate is a weaker version
-  of [match_stacks] that captures this situation. *)
-
-Inductive match_stacks_partial: 
-      list Machabstr.stackframe -> list Machconcr.stackframe ->
-      mem -> mem -> Prop :=
-  | match_stacks_partial_nil: forall mm ms,
-      match_stacks_partial nil nil mm ms
-  | match_stacks_partial_cons: forall f sp base c fr s fb ra ts mm ms,
-      frame_match fr sp base mm ms ->
-      sp < ms.(nextblock) ->
-      Genv.find_funct_ptr ge fb = Some (Internal f) ->
-      match_stacks s ts sp base mm ms ->
-      Val.has_type ra Tint ->
-      match_stacks_partial (Machabstr.Stackframe f (Vptr sp base) c fr :: s)
-                           (Machconcr.Stackframe fb (Vptr sp base) ra c :: ts)
-                           mm ms.
-
-Lemma match_stacks_match_stacks_partial:
-  forall s ts sp base mm ms,
-  match_stacks s ts sp base mm ms ->
-  match_stacks_partial s ts (free mm sp) (free ms sp).
-Proof.
-  intros. inv H. constructor.
-  econstructor. 
-  eapply frame_match_free; eauto. unfold block; omega.
-  simpl. inv H0; auto.
-  auto.
-  apply match_stacks_free; auto.
-  generalize (Mem.load_inv _ _ _ _ _ H3). intros [A B].
-  rewrite B.
-  destruct (getN (pred_size_chunk Mint32) (Int.signed base + 12)
-                 (contents (blocks ms sp))); exact I.
+  eapply IHmatch_stacks; eauto.
+  eapply stack_below_trans; eauto. omega.
 Qed.
 
 Lemma match_stacks_function_entry:
-  forall s ts mm ms lom him mm' los his ms' stk ms'' ms''' base,
-  match_stacks_partial s ts mm ms ->
+  forall s ts mm ms lom him mm' los his ms' stk,
+  match_stacks s ts mm ms ->
   alloc mm lom him = (mm', stk) ->
   alloc ms los his = (ms', stk) ->
-  store Mint32 ms' stk (Int.signed base) (parent_sp ts) = Some ms'' ->
-  store Mint32 ms'' stk (Int.signed base + 12) (parent_ra ts) = Some ms''' ->
-  match_stacks s ts stk base mm' ms'''.
+  match_stacks s ts mm' ms' /\ stack_below ts stk.
 Proof.
-  intros. 
-  assert (WT_SP: Val.has_type (parent_sp ts) Tint).
-    inv H; simpl; auto.
-  assert (WT_RA: Val.has_type (parent_ra ts) Tint).
-    inv H; simpl; auto.
-  assert (load Mint32 ms''' stk (Int.signed base) = Some (parent_sp ts)).
-    transitivity (load Mint32 ms'' stk (Int.signed base)).
-    eapply load_store_other; eauto. right; left. simpl. omega.
-    transitivity (Some (Val.load_result (chunk_of_type Tint) (parent_sp ts))).
-    simpl chunk_of_type. eapply load_store_same; eauto. 
-    decEq. apply load_result_ty. auto.
-  assert (load Mint32 ms''' stk (Int.signed base + 12) = Some (parent_ra ts)).
-    transitivity (Some (Val.load_result (chunk_of_type Tint) (parent_ra ts))).
-    simpl chunk_of_type. eapply load_store_same; eauto. 
-    decEq. apply load_result_ty. auto.
-  inv H; simpl in *.
-  constructor; auto.
-  assert (sp < stk). rewrite (alloc_result _ _ _ _ _ H1). auto.
-  assert (sp <> stk). unfold block; omega.
-  assert (nextblock mm = nextblock ms).
-  rewrite <- (alloc_result _ _ _ _ _ H0). 
-  rewrite <- (alloc_result _ _ _ _ _ H1). auto.
-  econstructor; eauto.
-  eapply frame_match_store_other; eauto. 
-  eapply frame_match_store_other; eauto.
-  eapply frame_match_alloc with (mm := mm) (ms := ms); eauto.
-  eapply match_stacks_store_other; eauto. 
-  eapply match_stacks_store_other; eauto.
-  eapply match_stacks_alloc with (mm := mm) (ms := ms); eauto.
- Qed.
+  intros.
+  assert (stk = nextblock mm). eapply Mem.alloc_result; eauto.
+  assert (stk = nextblock ms). eapply Mem.alloc_result; eauto.
+  split.
+  eapply match_stacks_alloc; eauto. congruence.
+  red. 
+  inv H; simpl.
+  unfold nullptr. apply Zgt_lt. apply nextblock_pos. 
+  inv H6. red in H. rewrite H3. auto. 
+Qed.
 
 (** ** Invariant between states. *)
 
@@ -651,27 +662,27 @@ Inductive match_states:
             Machabstr.state -> Machconcr.state -> Prop :=
   | match_states_intro:
       forall s f sp base c rs fr mm ts fb ms
-        (STACKS: match_stacks s ts sp base mm ms)
-        (FM: frame_match fr sp base mm ms)
+        (STACKS: match_stacks s ts mm ms)
+        (FM: frame_match f (extend_frame f ts fr) sp base mm ms)
+        (BELOW: stack_below ts sp)
         (MEXT: Mem.extends mm ms)
         (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)),
       match_states (Machabstr.State s f (Vptr sp base) c rs fr mm)
                    (Machconcr.State ts fb (Vptr sp base) c rs ms)
   | match_states_call:
       forall s f rs mm ts fb ms
-        (STACKS: match_stacks_partial s ts mm ms)
+        (STACKS: match_stacks s ts mm ms)
         (MEXT: Mem.extends mm ms)
         (FIND: Genv.find_funct_ptr ge fb = Some f),
       match_states (Machabstr.Callstate s f rs mm)
                    (Machconcr.Callstate ts fb rs ms)
   | match_states_return:
       forall s rs mm ts ms
-        (STACKS: match_stacks_partial s ts mm ms)
+        (STACKS: match_stacks s ts mm ms)
         (MEXT: Mem.extends mm ms),
       match_states (Machabstr.Returnstate s rs mm)
                    (Machconcr.Returnstate ts rs ms).
 
-
 (** * The proof of simulation *)
 
 (** The proof of simulation relies on diagrams of the following form:
@@ -710,29 +721,23 @@ Qed.
 
 Lemma transl_extcall_arguments:
   forall rs s sg args ts m ms,
-  Machabstr.extcall_arguments rs (parent_frame s) sg args ->
-  match_stacks_partial s ts m ms ->
+  Machabstr.extcall_arguments (parent_function s) rs (parent_frame s) sg args ->
+  match_stacks s ts m ms ->
   extcall_arguments rs ms (parent_sp ts) sg args.
 Proof.
   unfold Machabstr.extcall_arguments, extcall_arguments; intros.
-  assert (forall ty ofs v,
-    get_slot (parent_frame s) ty (Int.signed ofs) v ->
-    load_stack ms (parent_sp ts) ty ofs = Some v).
-  inv H0; simpl; intros.
-  inv H0. simpl in H2. elimtype False. generalize (AST.typesize_pos ty). omega.
-  eapply frame_match_get_slot; eauto.
   assert (forall locs vals,
-    Machabstr.extcall_args rs (parent_frame s) locs vals ->
+    Machabstr.extcall_args (parent_function s) rs (parent_frame s) locs vals ->
     extcall_args rs ms (parent_sp ts) locs vals).
-  induction locs; intros; inversion H2; subst; clear H2.
+  induction locs; intros; inv H1.
   constructor.
   constructor; auto.
-  inversion H7; subst; clear H7. 
-  constructor.
-  constructor. auto.  
+  inv H6. constructor. constructor. eapply match_stacks_get_parent; eauto.
   auto.
 Qed.
 
+Hypothesis wt_prog: wt_program p.
+
 Theorem step_equiv:
   forall s1 t s2, Machabstr.step ge s1 t s2 ->
   forall s1' (MS: match_states s1 s1') (WTS: wt_state s1),
@@ -746,27 +751,33 @@ Proof.
   econstructor; eauto with coqlib.
 
   (* Mgetstack *)
+  assert (WTF: wt_function f) by (inv WTS; auto).
   exists (State ts fb (Vptr sp0 base) c (rs#dst <- v) ms); split.
-  apply exec_Mgetstack; auto. eapply frame_match_get_slot; eauto.
+  constructor; auto.
+  eapply frame_match_get_slot; eauto.
+  eapply get_slot_extends; eauto.
   econstructor; eauto with coqlib.
 
   (* Msetstack *)
+  assert (WTF: wt_function f) by (inv WTS; auto).
   assert (Val.has_type (rs src) ty).
     inv WTS. 
     generalize (wt_function_instrs _ WTF _ (is_tail_in TAIL)); intro WTI.
     inv WTI. apply WTRS.
-  exploit frame_match_set_slot; eauto. 
-  intros [ms' [STORE [FM' [EXT' BOUND]]]].
+  exploit frame_match_set_slot; eauto.
+    eapply set_slot_extends; eauto.
+  intros [ms' [STORE [FM' EXT']]].
   exists (State ts fb (Vptr sp0 base) c rs ms'); split.
   apply exec_Msetstack; auto.
   econstructor; eauto.
   eapply match_stacks_store_slot; eauto.
 
   (* Mgetparam *)
-  exploit match_stacks_get_parent; eauto. 
-  intros [parent [LOAD1 LOAD2]].
+  assert (WTF: wt_function f) by (inv WTS; auto).
   exists (State ts fb (Vptr sp0 base) c (rs#dst <- v) ms); split.
-  eapply exec_Mgetparam; eauto. 
+  eapply exec_Mgetparam; eauto.
+    eapply frame_match_load_link; eauto.
+    eapply match_stacks_get_parent; eauto.
   econstructor; eauto with coqlib. 
  
   (* Mop *)
@@ -802,16 +813,17 @@ Proof.
   econstructor; split.
   eapply exec_Mcall; eauto. 
   econstructor; eauto. 
-  econstructor; eauto. inv FM; auto. exact I.  
+  econstructor; eauto. inv WTS; auto. exact I.
 
   (* Mtailcall *)
+  assert (WTF: wt_function f) by (inv WTS; auto).
   exploit find_function_find_function_ptr; eauto. 
   intros [fb' [FIND' FINDFUNCT]].
-  exploit match_stacks_load_links; eauto. intros [LOAD1 LOAD2].
   econstructor; split.
   eapply exec_Mtailcall; eauto.
-  econstructor; eauto.
-  eapply match_stacks_match_stacks_partial; eauto. 
+    eapply frame_match_load_link; eauto.
+    eapply frame_match_load_retaddr; eauto.
+  econstructor; eauto. eapply match_stacks_free; auto.
   apply free_extends; auto.
 
   (* Malloc *)
@@ -841,67 +853,32 @@ Proof.
   econstructor; eauto.
 
   (* Mreturn *)
-  exploit match_stacks_load_links; eauto. intros [LOAD1 LOAD2].
+  assert (WTF: wt_function f) by (inv WTS; auto).
   econstructor; split.
   eapply exec_Mreturn; eauto.
-  econstructor; eauto.  
-  eapply match_stacks_match_stacks_partial; eauto. 
+    eapply frame_match_load_link; eauto.
+    eapply frame_match_load_retaddr; eauto.
+  econstructor; eauto. eapply match_stacks_free; eauto.   
   apply free_extends; auto.
 
   (* internal function *)
-  assert (WTF: wt_function f). inv WTS. inv H5. auto. inv WTF.
-  caseEq (alloc ms (- f.(fn_framesize))
-                   (align_16_top (- f.(fn_framesize)) f.(fn_stacksize))).
+  assert (WTF: wt_function f). inv WTS. inv H5. auto.
+  caseEq (alloc ms (- f.(fn_framesize)) f.(fn_stacksize)).
   intros ms' stk' ALLOC.
-  exploit (alloc_extends m ms m' ms' 0 (fn_stacksize f)
-               (- fn_framesize f)
-               (align_16_top (- fn_framesize f) (fn_stacksize f))); eauto.
-  omega. apply align_16_top_ge. 
-  intros [EQ EXT']. subst stk'.
-  exploit (frame_match_new m ms); eauto. inv MEXT; auto.
-  intros [EQ FM]. clear EQ.
-  set (sp := Vptr stk (Int.repr (- fn_framesize f))).
-  assert (exists ms'', store Mint32 ms' stk (- fn_framesize f) (parent_sp ts) = Some ms'').
-    apply valid_access_store. constructor. 
-    eauto with mem.
-    rewrite (low_bound_alloc_same _ _ _ _ _ ALLOC). omega.
-    rewrite (high_bound_alloc_same _ _ _ _ _ ALLOC).
-    change (size_chunk Mint32) with 4. 
-    apply Zle_trans with 0. omega. apply align_16_top_pos.
-  destruct H0 as [ms'' STORE1].
-  assert (exists ms''', store Mint32 ms'' stk (- fn_framesize f + 12) (parent_ra ts) = Some ms''').
-    apply valid_access_store. constructor. 
-    eauto with mem.
-    rewrite (low_bound_store _ _ _ _ _ _ STORE1 stk). 
-    rewrite (low_bound_alloc_same _ _ _ _ _ ALLOC). omega.
-    rewrite (high_bound_store _ _ _ _ _ _ STORE1 stk). 
-    rewrite (high_bound_alloc_same _ _ _ _ _ ALLOC).
-    change (size_chunk Mint32) with 4. 
-    apply Zle_trans with 0. omega. apply align_16_top_pos.
-  destruct H0 as [ms''' STORE2].
-  assert (RANGE1: Int.min_signed <= - fn_framesize f <= Int.max_signed).
-  split. omega. apply Zle_trans with (-24). omega. compute;congruence.
-  assert (RANGE2: Int.min_signed <= - fn_framesize f + 12 <= Int.max_signed).
-  split. omega. apply Zle_trans with (-12). omega. compute;congruence.
+  assert (Val.has_type (parent_sp ts) Tint).
+    inv STACKS; simpl; auto.
+  assert (Val.has_type (parent_ra ts) Tint).
+    inv STACKS; simpl; auto.
+  destruct (frame_match_function_entry _ WTF _ _ _ _ _ _ _
+              MEXT H ALLOC H0 H1)
+  as [ms2 [ms3 [EQ [STORE1 [STORE2 [FM MEXT']]]]]].
+  subst stk'.
   econstructor; split.
   eapply exec_function_internal; eauto.
-  unfold store_stack. simpl. rewrite Int.add_zero. 
-  rewrite Int.signed_repr. eauto. auto.
-  unfold store_stack. simpl. rewrite Int.add_signed.
-  change (Int.signed (Int.repr 12)) with 12.
-  repeat rewrite Int.signed_repr; eauto.
-  (* match states *)
-  unfold sp; econstructor; eauto.
-  eapply match_stacks_function_entry; eauto.
-  rewrite Int.signed_repr; eauto.
-  rewrite Int.signed_repr; eauto.
-  eapply frame_match_store_other with (ms := ms''); eauto.
-  eapply frame_match_store_other with (ms := ms'); eauto. 
-  simpl. right; omega. simpl. right; omega.
-  eapply store_outside_extends with (m2 := ms''); eauto.
-  eapply store_outside_extends with (m2 := ms'); eauto.
-  rewrite (low_bound_alloc_same _ _ _ _ _ H). simpl; omega.
-  rewrite (low_bound_alloc_same _ _ _ _ _ H). simpl; omega.
+  exploit match_stacks_function_entry; eauto. intros [STACKS' BELOW].
+  econstructor; eauto.
+  eapply match_stacks_store_slot with (ms := ms2); eauto.
+  eapply match_stacks_store_slot with (ms := ms'); eauto.
 
   (* external function *)
   econstructor; split.
@@ -916,8 +893,6 @@ Proof.
   econstructor; eauto.
 Qed.
 
-Hypothesis wt_prog: wt_program p.
-
 Lemma equiv_initial_states:
   forall st1, Machabstr.initial_state p st1 ->
   exists st2, Machconcr.initial_state p st2 /\ match_states st1 st2 /\ wt_state st1.
-- 
cgit