Revised Stacking and Asmgen passes and Mach semantics:

- no more prediction of return addresses (Asmgenretaddr is gone)
- instead, punch a hole for the retaddr in Mach stack frame and
  fill this hole with the return address in the Asmgen proof.



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

5 files changed, 459 insertions, 1562 deletions

diff --git a/ia32/Asm.v b/ia32/Asm.v
index a78c8bf..87d9dc9 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -68,6 +68,10 @@ Coercion IR: ireg >-> preg.
 Coercion FR: freg >-> preg.
 Coercion CR: crbit >-> preg.
 
+(** Conventional names for stack pointer ([SP]) and return address ([RA]) *)
+
+Notation "'SP'" := ESP (only parsing).
+
 (** ** Instruction set. *)
 
 Definition label := positive.
@@ -197,6 +201,8 @@ with annot_param : Type :=
   | APstack: memory_chunk -> Z -> annot_param.
 
 Definition code := list instruction.
+Definition function := code.
+Definition fn_code (f: function) : code := f.
 Definition fundef := AST.fundef code.
 Definition program := AST.program fundef unit.
 
@@ -863,3 +869,30 @@ Ltac Equalities :=
 (* final states *)
   inv H; inv H0. congruence.
 Qed.
+
+(** Classification functions for processor registers (used in Asmgenproof). *)
+
+Definition data_preg (r: preg) : bool :=
+  match r with
+  | PC => false
+  | IR _ => true
+  | FR _ => true
+  | ST0 => true
+  | CR _ => false
+  | RA => false
+  end.
+
+Definition nontemp_preg (r: preg) : bool :=
+  match r with
+  | PC => false
+  | IR ECX => false
+  | IR EDX => false
+  | IR _ => true
+  | FR XMM6 => false
+  | FR XMM7 => false
+  | FR _ => true
+  | ST0 => false
+  | CR _ => false
+  | RA => false
+  end.
+
diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v
index 6b7cbf9..a7a629b 100644
--- a/ia32/Asmgen.v
+++ b/ia32/Asmgen.v
@@ -549,7 +549,7 @@ Fixpoint transl_code (f: Mach.function) (il: list Mach.instruction)  (edx_is_par
   around, leading to incorrect executions. *)
 
 Definition transf_function (f: Mach.function) : res Asm.code :=
-  do c <- transl_code f f.(fn_code) true;
+  do c <- transl_code f f.(Mach.fn_code) true;
   if zlt (list_length_z c) Int.max_unsigned 
   then OK (Pallocframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) :: c)
   else Error (msg "code size exceeded").
diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v
index d618d44..e43552e 100644
--- a/ia32/Asmgenproof.v
+++ b/ia32/Asmgenproof.v
@@ -25,12 +25,10 @@ Require Import Smallstep.
 Require Import Op.
 Require Import Locations.
 Require Import Mach.
-Require Import Machsem.
-Require Import Machtyping.
 Require Import Conventions.
 Require Import Asm.
 Require Import Asmgen.
-Require Import Asmgenretaddr.
+Require Import Asmgenproof0.
 Require Import Asmgenproof1.
 
 Section PRESERVATION.
@@ -77,65 +75,6 @@ Qed.
 
 (** * Properties of control flow *)
 
-Lemma find_instr_in:
-  forall c pos i,
-  find_instr pos c = Some i -> In i c.
-Proof.
-  induction c; simpl. intros; discriminate.
-  intros until i. case (zeq pos 0); intros.
-  left; congruence. right; eauto.
-Qed.
-
-Lemma find_instr_tail:
-  forall c1 i c2 pos,
-  code_tail pos c1 (i :: c2) ->
-  find_instr pos c1 = Some i.
-Proof.
-  induction c1; simpl; intros.
-  inv H.
-  destruct (zeq pos 0). subst pos.
-  inv H. auto. generalize (code_tail_pos _ _ _ H4). intro. omegaContradiction.
-  inv H. congruence. replace (pos0 + 1 - 1) with pos0 by omega.
-  eauto.
-Qed.
-
-Remark code_tail_bounds:
-  forall fn ofs i c,
-  code_tail ofs fn (i :: c) -> 0 <= ofs < list_length_z fn.
-Proof.
-  assert (forall ofs fn c, code_tail ofs fn c ->
-          forall i c', c = i :: c' -> 0 <= ofs < list_length_z fn).
-  induction 1; intros; simpl. 
-  rewrite H. rewrite list_length_z_cons. generalize (list_length_z_pos c'). omega.
-  rewrite list_length_z_cons. generalize (IHcode_tail _ _ H0). omega.
-  eauto.
-Qed.
-
-Lemma code_tail_next:
-  forall fn ofs i c,
-  code_tail ofs fn (i :: c) ->
-  code_tail (ofs + 1) fn c.
-Proof.
-  assert (forall ofs fn c, code_tail ofs fn c ->
-          forall i c', c = i :: c' -> code_tail (ofs + 1) fn c').
-  induction 1; intros.
-  subst c. constructor. constructor.
-  constructor. eauto.
-  eauto.
-Qed.
-
-Lemma code_tail_next_int:
-  forall fn ofs i c,
-  list_length_z fn <= Int.max_unsigned ->
-  code_tail (Int.unsigned ofs) fn (i :: c) ->
-  code_tail (Int.unsigned (Int.add ofs Int.one)) fn c.
-Proof.
-  intros. rewrite Int.add_unsigned.
-  change (Int.unsigned Int.one) with 1.
-  rewrite Int.unsigned_repr. apply code_tail_next with i; auto.
-  generalize (code_tail_bounds _ _ _ _ H0). omega. 
-Qed.
-
 Lemma transf_function_no_overflow:
   forall f tf,
   transf_function f = OK tf -> list_length_z tf <= Int.max_unsigned.
@@ -144,73 +83,9 @@ Proof.
   rewrite list_length_z_cons. omega. 
 Qed.
 
-(** [transl_code_at_pc pc fn c] holds if the code pointer [pc] points
-  within the IA32 code generated by translating Mach function [fn],
-  and [c] is the tail of the generated code at the position corresponding
-  to the code pointer [pc]. *)
-
-Inductive transl_code_at_pc: val -> block -> Mach.function -> Mach.code -> bool ->
-                                             Asm.code -> Asm.code -> Prop :=
-  transl_code_at_pc_intro:
-    forall b ofs f c ep tf tc,
-    Genv.find_funct_ptr ge b = Some (Internal f) ->
-    transf_function f = OK tf ->
-    transl_code f c ep = OK tc ->
-    code_tail (Int.unsigned ofs) tf tc ->
-    transl_code_at_pc (Vptr b ofs) b f c ep tf tc.
-
-(** The following lemmas show that straight-line executions
-  (predicate [exec_straight]) correspond to correct PPC executions
-  (predicate [exec_steps]) under adequate [transl_code_at_pc] hypotheses. *)
-
-Lemma exec_straight_steps_1:
-  forall fn c rs m c' rs' m',
-  exec_straight tge fn c rs m c' rs' m' ->
-  list_length_z fn <= Int.max_unsigned ->
-  forall b ofs,
-  rs#PC = Vptr b ofs ->
-  Genv.find_funct_ptr tge b = Some (Internal fn) ->
-  code_tail (Int.unsigned ofs) fn c ->
-  plus step tge (State rs m) E0 (State rs' m').
-Proof.
-  induction 1; intros.
-  apply plus_one.
-  econstructor; eauto. 
-  eapply find_instr_tail. eauto.
-  eapply plus_left'.
-  econstructor; eauto. 
-  eapply find_instr_tail. eauto.
-  apply IHexec_straight with b (Int.add ofs Int.one). 
-  auto. rewrite H0. rewrite H3. reflexivity.
-  auto. 
-  apply code_tail_next_int with i; auto.
-  traceEq.
-Qed.
-    
-Lemma exec_straight_steps_2:
-  forall fn c rs m c' rs' m',
-  exec_straight tge fn c rs m c' rs' m' ->
-  list_length_z fn <= Int.max_unsigned ->
-  forall b ofs,
-  rs#PC = Vptr b ofs ->
-  Genv.find_funct_ptr tge b = Some (Internal fn) ->
-  code_tail (Int.unsigned ofs) fn c ->
-  exists ofs',
-     rs'#PC = Vptr b ofs'
-  /\ code_tail (Int.unsigned ofs') fn c'.
-Proof.
-  induction 1; intros.
-  exists (Int.add ofs Int.one). split.
-  rewrite H0. rewrite H2. auto.
-  apply code_tail_next_int with i1; auto.
-  apply IHexec_straight with (Int.add ofs Int.one).
-  auto. rewrite H0. rewrite H3. reflexivity. auto. 
-  apply code_tail_next_int with i; auto.
-Qed.
-
 Lemma exec_straight_exec:
-  forall fb f c ep tf tc c' rs m rs' m',
-  transl_code_at_pc (rs PC) fb f c ep tf tc ->
+  forall f c ep tf tc c' rs m rs' m',
+  transl_code_at_pc ge (rs PC) f c ep tf tc ->
   exec_straight tge tf tc rs m c' rs' m' ->
   plus step tge (State rs m) E0 (State rs' m').
 Proof.
@@ -221,11 +96,11 @@ Proof.
 Qed.
 
 Lemma exec_straight_at:
-  forall fb f c ep tf tc c' ep' tc' rs m rs' m',
-  transl_code_at_pc (rs PC) fb f c ep tf tc ->
+  forall f c ep tf tc c' ep' tc' rs m rs' m',
+  transl_code_at_pc ge (rs PC) f c ep tf tc ->
   transl_code f c' ep' = OK tc' ->
   exec_straight tge tf tc rs m tc' rs' m' ->
-  transl_code_at_pc (rs' PC) fb f c' ep' tf tc'.
+  transl_code_at_pc ge (rs' PC) f c' ep' tf tc'.
 Proof.
   intros. inv H. 
   exploit exec_straight_steps_2; eauto. 
@@ -235,36 +110,6 @@ Proof.
   rewrite PC'. constructor; auto.
 Qed.
 
-(** Correctness of the return addresses predicted by
-    [Asmgen.return_address_offset]. *)
-
-Remark code_tail_no_bigger:
-  forall pos c1 c2, code_tail pos c1 c2 -> (length c2 <= length c1)%nat.
-Proof.
-  induction 1; simpl; omega.
-Qed.
-
-Remark code_tail_unique:
-  forall fn c pos pos',
-  code_tail pos fn c -> code_tail pos' fn c -> pos = pos'.
-Proof.
-  induction fn; intros until pos'; intros ITA CT; inv ITA; inv CT; auto.
-  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
-  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
-  f_equal. eauto.
-Qed.
-
-Lemma return_address_offset_correct:
-  forall b ofs fb f c tf tc ofs',
-  transl_code_at_pc (Vptr b ofs) fb f c false tf tc ->
-  return_address_offset f c ofs' ->
-  ofs' = ofs.
-Proof.
-  intros. inv H0. inv H. 
-  exploit code_tail_unique. eexact H12. eapply H1; eauto. intro.
-  subst ofs0. apply Int.repr_unsigned.
-Qed.
-
 (** The [find_label] function returns the code tail starting at the
   given label.  A connection with [code_tail] is then established. *)
 
@@ -446,7 +291,6 @@ Proof.
   destruct c0; auto.
 Qed.
 
-
 Remark transl_op_label:
   forall op args r k c,
   transl_op op args r k = OK c ->
@@ -534,7 +378,7 @@ Qed.
 Lemma transl_find_label:
   forall f tf,
   transf_function f = OK tf ->
-  match Mach.find_label lbl f.(fn_code) with
+  match Mach.find_label lbl f.(Mach.fn_code) with
   | None => find_label lbl tf = None
   | Some c => exists tc, find_label lbl tf = Some tc /\ transl_code f c false = OK tc
   end.
@@ -553,10 +397,10 @@ Lemma find_label_goto_label:
   Genv.find_funct_ptr ge b = Some (Internal f) ->
   transf_function f = OK tf ->
   rs PC = Vptr b ofs ->
-  Mach.find_label lbl f.(fn_code) = Some c' ->
+  Mach.find_label lbl f.(Mach.fn_code) = Some c' ->
   exists tc', exists rs',
     goto_label tf lbl rs m = Next rs' m  
-  /\ transl_code_at_pc (rs' PC) b f c' false tf tc'
+  /\ transl_code_at_pc ge (rs' PC) f c' false tf tc'
   /\ forall r, r <> PC -> rs'#r = rs#r.
 Proof.
   intros. exploit (transl_find_label lbl f tf); eauto. rewrite H2. 
@@ -590,61 +434,51 @@ Qed.
 - Mach register values and PPC register values agree.
 *)
 
-Inductive match_stack: list Machsem.stackframe -> Prop :=
-  | match_stack_nil:
-      match_stack nil
-  | match_stack_cons: forall fb sp ra c s f tf tc,
-      Genv.find_funct_ptr ge fb = Some (Internal f) ->
-      transl_code_at_pc ra fb f c false tf tc ->
-      sp <> Vundef -> ra <> Vundef ->
-      match_stack s ->
-      match_stack (Stackframe fb sp ra c :: s).
-
-Inductive match_states: Machsem.state -> Asm.state -> Prop :=
+Inductive match_states: Mach.state -> Asm.state -> Prop :=
   | match_states_intro:
-      forall s fb sp c ep ms m m' rs f tf tc
-        (STACKS: match_stack s)
-        (FIND: Genv.find_funct_ptr ge fb = Some (Internal f))
+      forall s f sp c ep ms m m' rs tf tc ra
+        (STACKS: match_stack ge s m m' ra sp)
         (MEXT: Mem.extends m m')
-        (AT: transl_code_at_pc (rs PC) fb f c ep tf tc)
-        (AG: agree ms sp rs)
+        (AT: transl_code_at_pc ge (rs PC) f c ep tf tc)
+        (AG: agree ms (Vptr sp Int.zero) rs)
+        (RSA: retaddr_stored_at m m' sp (Int.unsigned f.(fn_retaddr_ofs)) ra)
         (DXP: ep = true -> rs#EDX = parent_sp s),
-      match_states (Machsem.State s fb sp c ms m)
+      match_states (Mach.State s f (Vptr sp Int.zero) c ms m)
                    (Asm.State rs m')
   | match_states_call:
-      forall s fb ms m m' rs
-        (STACKS: match_stack s)
+      forall s fd ms m m' rs fb
+        (STACKS: match_stack ge s m m' (rs RA) (Mem.nextblock m))
         (MEXT: Mem.extends m m')
         (AG: agree ms (parent_sp s) rs)
         (ATPC: rs PC = Vptr fb Int.zero)
-        (ATLR: rs RA = parent_ra s),
-      match_states (Machsem.Callstate s fb ms m)
+        (FUNCT: Genv.find_funct_ptr ge fb = Some fd)
+        (WTRA: Val.has_type (rs RA) Tint),
+      match_states (Mach.Callstate s fd ms m)
                    (Asm.State rs m')
   | match_states_return:
       forall s ms m m' rs
-        (STACKS: match_stack s)
+        (STACKS: match_stack ge s m m' (rs PC) (Mem.nextblock m))
         (MEXT: Mem.extends m m')
-        (AG: agree ms (parent_sp s) rs)
-        (ATPC: rs PC = parent_ra s),
-      match_states (Machsem.Returnstate s ms m)
+        (AG: agree ms (parent_sp s) rs),
+      match_states (Mach.Returnstate s ms m)
                    (Asm.State rs m').
 
 Lemma exec_straight_steps:
-  forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2,
-  match_stack s ->
+  forall s f rs1 i c ep tf tc m1' m2 m2' sp ms2 ra,
+  match_stack ge s m2 m2' ra sp ->
   Mem.extends m2 m2' ->
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  transl_code_at_pc (rs1 PC) fb f (i :: c) ep tf tc ->
-  (forall k c, transl_instr f i ep k = OK c ->
+  retaddr_stored_at m2 m2' sp (Int.unsigned f.(fn_retaddr_ofs)) ra ->
+  transl_code_at_pc ge (rs1 PC) f (i :: c) ep tf tc ->
+  (forall k c (TR: transl_instr f i ep k = OK c),
    exists rs2,
        exec_straight tge tf c rs1 m1' k rs2 m2'
-    /\ agree ms2 sp rs2
+    /\ agree ms2 (Vptr sp Int.zero) rs2
     /\ (edx_preserved ep i = true -> rs2#EDX = parent_sp s)) ->
   exists st',
   plus step tge (State rs1 m1') E0 st' /\
-  match_states (Machsem.State s fb sp c ms2 m2) st'.
+  match_states (Mach.State s f (Vptr sp Int.zero) c ms2 m2) st'.
 Proof.
-  intros. inversion H2. subst. monadInv H7. 
+  intros. inversion H2; subst. monadInv H7. 
   exploit H3; eauto. intros [rs2 [A [B C]]]. 
   exists (State rs2 m2'); split.
   eapply exec_straight_exec; eauto. 
@@ -652,23 +486,23 @@ Proof.
 Qed.
 
 Lemma exec_straight_steps_goto:
-  forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c',
-  match_stack s ->
+  forall s f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c' ra,
+  match_stack ge s m2 m2' ra sp ->
   Mem.extends m2 m2' ->
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  Mach.find_label lbl f.(fn_code) = Some c' ->
-  transl_code_at_pc (rs1 PC) fb f (i :: c) ep tf tc ->
+  retaddr_stored_at m2 m2' sp (Int.unsigned f.(fn_retaddr_ofs)) ra ->
+  Mach.find_label lbl f.(Mach.fn_code) = Some c' ->
+  transl_code_at_pc ge (rs1 PC) f (i :: c) ep tf tc ->
   edx_preserved ep i = false ->
-  (forall k c, transl_instr f i ep k = OK c ->
+  (forall k c (TR: transl_instr f i ep k = OK c),
    exists jmp, exists k', exists rs2,
        exec_straight tge tf c rs1 m1' (jmp :: k') rs2 m2'
-    /\ agree ms2 sp rs2
+    /\ agree ms2 (Vptr sp Int.zero) rs2
     /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2') ->
   exists st',
   plus step tge (State rs1 m1') E0 st' /\
-  match_states (Machsem.State s fb sp c' ms2 m2) st'.
+  match_states (Mach.State s f (Vptr sp Int.zero) c' ms2 m2) st'.
 Proof.
-  intros. inversion H3. subst. monadInv H9.
+  intros. inversion H3; subst. monadInv H9.
   exploit H5; eauto. intros [jmp [k' [rs2 [A [B C]]]]].
   generalize (functions_transl _ _ _ H7 H8); intro FN.
   generalize (transf_function_no_overflow _ _ H8); intro NOOV.
@@ -684,164 +518,99 @@ Proof.
   rewrite C. eexact GOTO.
   traceEq.
   econstructor; eauto.
-  apply agree_exten with rs2; auto with ppcgen.
+  apply agree_exten with rs2; auto with asmgen.
   congruence.
 Qed.
 
-Lemma parent_sp_def: forall s, match_stack s -> parent_sp s <> Vundef.
-Proof. induction 1; simpl. congruence. auto. Qed.
-
-Lemma parent_ra_def: forall s, match_stack s -> parent_ra s <> Vundef.
-Proof. induction 1; simpl. unfold Vzero. congruence. auto. Qed.
-
-Lemma lessdef_parent_sp:
-  forall s v,
-  match_stack s -> Val.lessdef (parent_sp s) v -> v = parent_sp s.
-Proof.
-  intros. inv H0. auto. exploit parent_sp_def; eauto. tauto.
-Qed.
-
-Lemma lessdef_parent_ra:
-  forall s v,
-  match_stack s -> Val.lessdef (parent_ra s) v -> v = parent_ra s.
-Proof.
-  intros. inv H0. auto. exploit parent_ra_def; eauto. tauto.
-Qed.
-
 (** We need to show that, in the simulation diagram, we cannot
   take infinitely many Mach transitions that correspond to zero
   transitions on the PPC side.  Actually, all Mach transitions
   correspond to at least one Asm transition, except the
-  transition from [Machsem.Returnstate] to [Machsem.State].
+  transition from [Mach.Returnstate] to [Mach.State].
   So, the following integer measure will suffice to rule out
   the unwanted behaviour. *)
 
-Definition measure (s: Machsem.state) : nat :=
+Definition measure (s: Mach.state) : nat :=
   match s with
-  | Machsem.State _ _ _ _ _ _ => 0%nat
-  | Machsem.Callstate _ _ _ _ => 0%nat
-  | Machsem.Returnstate _ _ _ => 1%nat
+  | Mach.State _ _ _ _ _ _ => 0%nat
+  | Mach.Callstate _ _ _ _ => 0%nat
+  | Mach.Returnstate _ _ _ => 1%nat
   end.
 
-(** We show the simulation diagram by case analysis on the Mach transition
-  on the left.  Since the proof is large, we break it into one lemma
-  per transition. *)
-
-Definition exec_instr_prop (s1: Machsem.state) (t: trace) (s2: Machsem.state) : Prop :=
-  forall s1' (MS: match_states s1 s1'),
-  (exists s2', plus step tge s1' t s2' /\ match_states s2 s2')
-  \/ (measure s2 < measure s1 /\ t = E0 /\ match_states s2 s1')%nat.
-
+(** This is the simulation diagram.  We prove it by case analysis on the Mach transition. *)
 
-Lemma exec_Mlabel_prop:
-  forall (s : list stackframe) (fb : block) (sp : val)
-         (lbl : Mach.label) (c : list Mach.instruction) (ms : Mach.regset)
-         (m : mem),
-  exec_instr_prop (Machsem.State s fb sp (Mlabel lbl :: c) ms m) E0
-                  (Machsem.State s fb sp c ms m).
+Theorem step_simulation:
+  forall S1 t S2, Mach.step ge S1 t S2 ->
+  forall S1' (MS: match_states S1 S1'),
+  (exists S2', plus step tge S1' t S2' /\ match_states S2 S2')
+  \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat.
 Proof.
-  intros; red; intros; inv MS.
+  induction 1; intros; inv MS.
+
+- (* Mlabel *)
   left; eapply exec_straight_steps; eauto; intros. 
-  monadInv H. econstructor; split. apply exec_straight_one. simpl; eauto. auto. 
+  monadInv TR. econstructor; split. apply exec_straight_one. simpl; eauto. auto. 
   split. apply agree_nextinstr; auto. simpl; congruence.
-Qed.
 
-Lemma exec_Mgetstack_prop:
-  forall (s : list stackframe) (fb : block) (sp : val) (ofs : int)
-         (ty : typ) (dst : mreg) (c : list Mach.instruction)
-         (ms : Mach.regset) (m : mem) (v : val),
-  load_stack m sp ty ofs = Some v ->
-  exec_instr_prop (Machsem.State s fb sp (Mgetstack ofs ty dst :: c) ms m) E0
-                  (Machsem.State s fb sp c (Regmap.set dst v ms) m).
-Proof.
-  intros; red; intros; inv MS.
+- (* Mgetstack *)
   unfold load_stack in H.
   exploit Mem.loadv_extends; eauto. intros [v' [A B]].
   rewrite (sp_val _ _ _ AG) in A.
-  left; eapply exec_straight_steps; eauto. intros. simpl in H0. 
+  left; eapply exec_straight_steps; eauto. intros. simpl in TR.
   exploit loadind_correct; eauto. intros [rs' [P [Q R]]].
   exists rs'; split. eauto.
   split. eapply agree_set_mreg; eauto. congruence.
   simpl; congruence.
-Qed.
 
-Lemma exec_Msetstack_prop:
-  forall (s : list stackframe) (fb : block) (sp : val) (src : mreg)
-         (ofs : int) (ty : typ) (c : list Mach.instruction)
-         (ms : mreg -> val) (m m' : mem),
-  store_stack m sp ty ofs (ms src) = Some m' ->
-  exec_instr_prop (Machsem.State s fb sp (Msetstack src ofs ty :: c) ms m) E0
-                  (Machsem.State s fb sp c (undef_setstack ms) m').
-Proof.
-  intros; red; intros; inv MS.
+- (* Msetstack *)
   unfold store_stack in H.
-  assert (Val.lessdef (ms src) (rs (preg_of src))). eapply preg_val; eauto.
+  assert (Val.lessdef (rs src) (rs0 (preg_of src))). eapply preg_val; eauto.
   exploit Mem.storev_extends; eauto. intros [m2' [A B]]. 
-  rewrite (sp_val _ _ _ AG) in A.
-  left; eapply exec_straight_steps; eauto. intros. simpl in H1.
+  left; eapply exec_straight_steps; eauto.
+  eapply match_stack_storev; eauto. 
+  eapply retaddr_stored_at_storev; eauto. 
+  rewrite (sp_val _ _ _ AG) in A. intros. simpl in TR.
   exploit storeind_correct; eauto. intros [rs' [P Q]].
   exists rs'; split. eauto.
   split. unfold undef_setstack. eapply agree_undef_move; eauto.
-  simpl; intros. rewrite Q; auto with ppcgen.
-Qed.
+  simpl; intros. rewrite Q; auto with asmgen.
 
-Lemma exec_Mgetparam_prop:
-  forall (s : list stackframe) (fb : block) (f: Mach.function) (sp : val)
-         (ofs : int) (ty : typ) (dst : mreg) (c : list Mach.instruction)
-         (ms : Mach.regset) (m : mem) (v : val),
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  load_stack m sp Tint f.(fn_link_ofs) = Some (parent_sp s) ->
-  load_stack m (parent_sp s) ty ofs = Some v ->
-  exec_instr_prop (Machsem.State s fb sp (Mgetparam ofs ty dst :: c) ms m) E0
-                  (Machsem.State s fb sp c (Regmap.set dst v (Regmap.set IT1 Vundef ms)) m).
-Proof.
-  intros; red; intros; inv MS.
-  assert (f0 = f) by congruence. subst f0.
+- (* Mgetparam *)
   unfold load_stack in *. 
-  exploit Mem.loadv_extends. eauto. eexact H0. auto. 
+  exploit Mem.loadv_extends. eauto. eexact H. auto. 
   intros [parent' [A B]]. rewrite (sp_val _ _ _ AG) in A.
-  assert (parent' = parent_sp s). inv B. auto. rewrite <- H3 in H1. simpl in H1. congruence.
-  subst parent'.
-  exploit Mem.loadv_extends. eauto. eexact H1. auto. 
+  exploit lessdef_parent_sp; eauto. clear B; intros B; subst parent'.
+  exploit Mem.loadv_extends. eauto. eexact H0. auto. 
   intros [v' [C D]].
 Opaque loadind.
   left; eapply exec_straight_steps; eauto; intros. 
   assert (DIFF: negb (mreg_eq dst IT1) = true -> IR EDX <> preg_of dst).
-    intros. change (IR EDX) with (preg_of IT1). red; intros.
-    exploit preg_of_injective; eauto. intros. subst dst. 
-    unfold proj_sumbool in H3. rewrite dec_eq_true in H3. simpl in H3. congruence.
-  destruct ep; simpl in H2.
+    intros. change (IR EDX) with (preg_of IT1). red; intros. 
+    unfold proj_sumbool in H1. destruct (mreg_eq dst IT1); try discriminate.
+    elim n. eapply preg_of_injective; eauto.
+  destruct ep; simpl in TR.
 (* EDX contains parent *)
-  exploit loadind_correct. eexact H2.
-  instantiate (2 := rs). rewrite DXP; eauto.  
+  exploit loadind_correct. eexact TR.
+  instantiate (2 := rs0). rewrite DXP; eauto.  
   intros [rs1 [P [Q R]]].
   exists rs1; split. eauto. 
   split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto.
   simpl; intros. rewrite R; auto.
 (* EDX does not contain parent *)
-  monadInv H2.
+  monadInv TR.
   exploit loadind_correct. eexact EQ0. eauto. intros [rs1 [P [Q R]]]. simpl in Q.
   exploit loadind_correct. eexact EQ. instantiate (2 := rs1). rewrite Q. eauto.
   intros [rs2 [S [T U]]]. 
   exists rs2; split. eapply exec_straight_trans; eauto.
   split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto.
-  simpl; intros. rewrite U; auto. 
-Qed.
+  simpl; intros. rewrite U; auto.
 
-Lemma exec_Mop_prop:
-  forall (s : list stackframe) (fb : block) (sp : val) (op : operation)
-         (args : list mreg) (res : mreg) (c : list Mach.instruction)
-         (ms : mreg -> val) (m : mem) (v : val),
-  eval_operation ge sp op ms ## args m = Some v ->
-  exec_instr_prop (Machsem.State s fb sp (Mop op args res :: c) ms m) E0
-                  (Machsem.State s fb sp c (Regmap.set res v (undef_op op ms)) m).
-Proof.
-  intros; red; intros; inv MS.
-  assert (eval_operation tge sp op ms##args m = Some v). 
+- (* Mop *)
+  assert (eval_operation tge (Vptr sp0 Int.zero) op rs##args m = Some v). 
     rewrite <- H. apply eval_operation_preserved. exact symbols_preserved.
   exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eexact H0.
   intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A. 
-  left; eapply exec_straight_steps; eauto; intros. simpl in H1. 
+  left; eapply exec_straight_steps; eauto; intros. simpl in TR.
   exploit transl_op_correct; eauto. intros [rs2 [P [Q R]]]. 
   assert (S: Val.lessdef v (rs2 (preg_of res))) by (eapply Val.lessdef_trans; eauto).
   exists rs2; split. eauto.
@@ -850,209 +619,135 @@ Proof.
   destruct op; try (eapply agree_set_undef_mreg; eauto).
   eapply agree_set_undef_move_mreg; eauto. 
   simpl; congruence.
-Qed.
 
-Lemma exec_Mload_prop:
-  forall (s : list stackframe) (fb : block) (sp : val)
-         (chunk : memory_chunk) (addr : addressing) (args : list mreg)
-         (dst : mreg) (c : list Mach.instruction) (ms : mreg -> val)
-         (m : mem) (a v : val),
-  eval_addressing ge sp addr ms ## args = Some a ->
-  Mem.loadv chunk m a = Some v ->
-  exec_instr_prop (Machsem.State s fb sp (Mload chunk addr args dst :: c) ms m)
-               E0 (Machsem.State s fb sp c (Regmap.set dst v (undef_temps ms)) m).
-Proof.
-  intros; red; intros; inv MS.
-  assert (eval_addressing tge sp addr ms##args = Some a). 
+- (* Mload *)
+  assert (eval_addressing tge (Vptr sp0 Int.zero) addr rs##args = Some a). 
     rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
   exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1.
   intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.
   exploit Mem.loadv_extends; eauto. intros [v' [C D]].
-  left; eapply exec_straight_steps; eauto; intros. simpl in H2. 
+  left; eapply exec_straight_steps; eauto; intros. simpl in TR.
   exploit transl_load_correct; eauto. intros [rs2 [P [Q R]]]. 
   exists rs2; split. eauto.
   split. eapply agree_set_undef_mreg; eauto. congruence.
   simpl; congruence.
-Qed.
 
-Lemma exec_Mstore_prop:
-  forall (s : list stackframe) (fb : block) (sp : val)
-         (chunk : memory_chunk) (addr : addressing) (args : list mreg)
-         (src : mreg) (c : list Mach.instruction) (ms : mreg -> val)
-         (m m' : mem) (a : val),
-  eval_addressing ge sp addr ms ## args = Some a ->
-  Mem.storev chunk m a (ms src) = Some m' ->
-  exec_instr_prop (Machsem.State s fb sp (Mstore chunk addr args src :: c) ms m) E0
-                  (Machsem.State s fb sp c (undef_temps ms) m').
-Proof.
-  intros; red; intros; inv MS.
-  assert (eval_addressing tge sp addr ms##args = Some a). 
+- (* Mstore *)
+  assert (eval_addressing tge (Vptr sp0 Int.zero) addr rs##args = Some a). 
     rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
   exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1.
   intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.
-  assert (Val.lessdef (ms src) (rs (preg_of src))). eapply preg_val; eauto.
+  assert (Val.lessdef (rs src) (rs0 (preg_of src))). eapply preg_val; eauto.
   exploit Mem.storev_extends; eauto. intros [m2' [C D]].
-  left; eapply exec_straight_steps; eauto; intros. simpl in H3. 
+  left; eapply exec_straight_steps; eauto.
+  eapply match_stack_storev; eauto.
+  eapply retaddr_stored_at_storev; eauto.
+  intros. simpl in TR. 
   exploit transl_store_correct; eauto. intros [rs2 [P Q]]. 
   exists rs2; split. eauto.
   split. eapply agree_exten_temps; eauto. 
   simpl; congruence.
-Qed.
 
-Lemma exec_Mcall_prop:
-  forall (s : list stackframe) (fb : block) (sp : val)
-         (sig : signature) (ros : mreg + ident) (c : Mach.code)
-         (ms : Mach.regset) (m : mem) (f : function) (f' : block)
-         (ra : int),
-  find_function_ptr ge ros ms = Some f' ->
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  return_address_offset f c ra ->
-  exec_instr_prop (Machsem.State s fb sp (Mcall sig ros :: c) ms m) E0
-                  (Callstate (Stackframe fb sp (Vptr fb ra) c :: s) f' ms m).
-Proof.
-  intros; red; intros; inv MS.
-  assert (f0 = f) by congruence. subst f0.
+- (* Mcall *)
   inv AT. 
   assert (NOOV: list_length_z tf <= Int.max_unsigned).
     eapply transf_function_no_overflow; eauto.
-  destruct ros as [rf|fid]; simpl in H; monadInv H5.
-  (* Indirect call *)
-  assert (DEST: ms rf = Vptr f' Int.zero).
-    destruct (ms rf); try discriminate.
-    generalize (Int.eq_spec i Int.zero); destruct (Int.eq i Int.zero); congruence.
-  clear H.
-  generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1.
-  assert (TCA: transl_code_at_pc (Vptr fb (Int.add ofs Int.one)) fb f c false tf x).
+  destruct ros as [rf|fid]; simpl in H; monadInv H3.
++ (* Indirect call *)
+  exploit Genv.find_funct_inv; eauto. intros [bf EQ2].
+  rewrite EQ2 in H; rewrite  Genv.find_funct_find_funct_ptr in H. 
+  assert (rs0 x0 = Vptr bf Int.zero).
+    exploit ireg_val; eauto. rewrite EQ2; intros LD; inv LD; auto.
+  generalize (code_tail_next_int _ _ _ _ NOOV H4). intro CT1.
+  assert (TCA: transl_code_at_pc ge (Vptr b (Int.add ofs Int.one)) f c false tf x).
     econstructor; eauto. 
-  exploit return_address_offset_correct; eauto. intros; subst ra.
   left; econstructor; split.
   apply plus_one. eapply exec_step_internal. eauto.
   eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
   simpl. eauto. 
-  constructor; auto. 
-  econstructor; eauto. eapply agree_sp_def; eauto. congruence.
-  simpl. eapply agree_exten; eauto. intros. repeat rewrite Pregmap.gso; auto with ppcgen.
-  exploit ireg_val; eauto. rewrite DEST. intros LD. inv LD. auto.
-  rewrite <- H2. auto. 
-  (* Direct call *)
-  generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1.
-  assert (TCA: transl_code_at_pc (Vptr fb (Int.add ofs Int.one)) fb f c false tf x).
+  econstructor; eauto. 
+  econstructor; eauto.
+  rewrite <- H0. eexact TCA. 
+  change (Mem.valid_block m sp0). eapply retaddr_stored_at_valid; eauto. 
+  simpl. eapply agree_exten; eauto. intros. Simplifs. 
+  rewrite <- H0. exact I.
++ (* Direct call *)
+  destruct (Genv.find_symbol ge fid) as [bf|] eqn:FS; try discriminate.
+  generalize (code_tail_next_int _ _ _ _ NOOV H4). intro CT1.
+  assert (TCA: transl_code_at_pc ge (Vptr b (Int.add ofs Int.one)) f c false tf x).
     econstructor; eauto. 
-  exploit return_address_offset_correct; eauto. intros; subst ra.
   left; econstructor; split.
   apply plus_one. eapply exec_step_internal. eauto.
   eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
-  simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite H. eauto.
-  constructor; auto. 
-  econstructor; eauto. eapply agree_sp_def; eauto. congruence.
-  simpl. eapply agree_exten; eauto. intros. repeat rewrite Pregmap.gso; auto with ppcgen.
-  rewrite <- H2. auto.
-Qed.
-
-Lemma agree_change_sp:
-  forall ms sp rs sp',
-  agree ms sp rs -> sp' <> Vundef ->
-  agree ms sp' (rs#ESP <- sp').
-Proof.
-  intros. inv H. split. apply Pregmap.gss. auto. 
-  intros. rewrite Pregmap.gso; auto with ppcgen.
-Qed.
+  simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite FS. eauto.
+  econstructor; eauto. 
+  econstructor; eauto.
+  rewrite <- H0. eexact TCA.
+  change (Mem.valid_block m sp0). eapply retaddr_stored_at_valid; eauto. 
+  simpl. eapply agree_exten; eauto. intros. Simplifs.
+  auto.
+  rewrite <- H0. exact I.
 
-Lemma exec_Mtailcall_prop:
-  forall (s : list stackframe) (fb stk : block) (soff : int)
-         (sig : signature) (ros : mreg + ident) (c : list Mach.instruction)
-         (ms : Mach.regset) (m : mem) (f: Mach.function) (f' : block) m',
-  find_function_ptr ge ros ms = Some f' ->
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
-  load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
-  Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-  exec_instr_prop
-          (Machsem.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0
-          (Callstate s f' ms m').
-Proof.
-  intros; red; intros; inv MS.
-  assert (f0 = f) by congruence. subst f0.
+- (* Mtailcall *)
   inv AT. 
   assert (NOOV: list_length_z tf <= Int.max_unsigned).
     eapply transf_function_no_overflow; eauto.
   rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *.
-  exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [parent' [A B]]. 
+  exploit Mem.loadv_extends. eauto. eexact H0. auto. simpl. intros [parent' [A B]]. 
   exploit lessdef_parent_sp; eauto. intros. subst parent'. clear B.
-  exploit Mem.loadv_extends. eauto. eexact H2. auto. simpl. intros [ra' [C D]].
-  exploit lessdef_parent_ra; eauto. intros. subst ra'. clear D.
-  exploit Mem.free_parallel_extends; eauto. intros [m2' [E F]]. 
-  destruct ros as [rf|fid]; simpl in H; monadInv H7.
-  (* Indirect call *)
-  assert (DEST: ms rf = Vptr f' Int.zero).
-    destruct (ms rf); try discriminate.
-    generalize (Int.eq_spec i Int.zero); destruct (Int.eq i Int.zero); congruence.
-  clear H.
-  generalize (code_tail_next_int _ _ _ _ NOOV H8). intro CT1.
+  assert (C: Mem.loadv Mint32 m'0 (Val.add (rs0 ESP) (Vint (fn_retaddr_ofs f))) = Some ra).
+Opaque Int.repr.
+    erewrite agree_sp; eauto. simpl. rewrite Int.add_zero_l.
+    eapply rsa_contains; eauto.
+  exploit retaddr_stored_at_can_free; eauto. intros [m2' [E F]].
+  assert (M: match_stack ge s m'' m2' ra (Mem.nextblock m'')).
+    apply match_stack_change_bound with stk.
+    eapply match_stack_free_left; eauto. 
+    eapply match_stack_free_left; eauto. 
+    eapply match_stack_free_right; eauto.
+    omega.
+    apply Z.lt_le_incl. change (Mem.valid_block m'' stk).
+    eapply Mem.valid_block_free_1; eauto. eapply Mem.valid_block_free_1; eauto. 
+    eapply retaddr_stored_at_valid; eauto.
+  destruct ros as [rf|fid]; simpl in H; monadInv H6.
++ (* Indirect call *)
+  exploit Genv.find_funct_inv; eauto. intros [bf EQ2].
+  rewrite EQ2 in H; rewrite  Genv.find_funct_find_funct_ptr in H. 
+  assert (rs0 x0 = Vptr bf Int.zero).
+    exploit ireg_val; eauto. rewrite EQ2; intros LD; inv LD; auto.
+  generalize (code_tail_next_int _ _ _ _ NOOV H7). intro CT1.
   left; econstructor; split.
   eapply plus_left. eapply exec_step_internal. eauto.
   eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
   simpl. rewrite C. rewrite A. rewrite <- (sp_val _ _ _ AG). rewrite E. eauto.
   apply star_one. eapply exec_step_internal. 
-  transitivity (Val.add rs#PC Vone). auto. rewrite <- H4. simpl. eauto.
+  transitivity (Val.add rs0#PC Vone). auto. rewrite <- H3. simpl. eauto.
   eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
   simpl. eauto. traceEq.
-  constructor; auto.
+  econstructor; eauto.
   apply agree_set_other; auto. apply agree_nextinstr. apply agree_set_other; auto.
   eapply agree_change_sp; eauto. eapply parent_sp_def; eauto.
-  rewrite Pregmap.gss. rewrite nextinstr_inv; auto with ppcgen.
-  repeat rewrite Pregmap.gso; auto with ppcgen. 
-  exploit ireg_val; eauto. rewrite DEST. intros LD. inv LD. auto.
-  generalize (preg_of_not_ESP rf). rewrite (ireg_of_eq _ _ EQ1). congruence.
-  (* Direct call *)
-  generalize (code_tail_next_int _ _ _ _ NOOV H8). intro CT1.
+  Simplifs. rewrite Pregmap.gso; auto. 
+  generalize (preg_of_not_SP rf). rewrite (ireg_of_eq _ _ EQ1). congruence.
+  change (Val.has_type ra Tint). eapply retaddr_stored_at_type; eauto.
++ (* Direct call *)
+  destruct (Genv.find_symbol ge fid) as [bf|] eqn:FS; try discriminate.
+  generalize (code_tail_next_int _ _ _ _ NOOV H7). intro CT1.
   left; econstructor; split.
   eapply plus_left. eapply exec_step_internal. eauto.
   eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
   simpl. rewrite C. rewrite A. rewrite <- (sp_val _ _ _ AG). rewrite E. eauto.
   apply star_one. eapply exec_step_internal. 
-  transitivity (Val.add rs#PC Vone). auto. rewrite <- H4. simpl. eauto.
+  transitivity (Val.add rs0#PC Vone). auto. rewrite <- H3. simpl. eauto.
   eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
   simpl. eauto. traceEq.
-  constructor; auto.
+  econstructor; eauto.
   apply agree_set_other; auto. apply agree_nextinstr. apply agree_set_other; auto.
   eapply agree_change_sp; eauto. eapply parent_sp_def; eauto.
-  rewrite Pregmap.gss. unfold symbol_offset. rewrite symbols_preserved. rewrite H. auto.
-Qed.
+  rewrite Pregmap.gss. unfold symbol_offset. rewrite symbols_preserved. rewrite FS. auto.
+  change (Val.has_type ra Tint). eapply retaddr_stored_at_type; eauto.
 
-Lemma exec_Mgoto_prop:
-  forall (s : list stackframe) (fb : block) (f : function) (sp : val)
-         (lbl : Mach.label) (c : list Mach.instruction) (ms : Mach.regset)
-         (m : mem) (c' : Mach.code),
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  Mach.find_label lbl (fn_code f) = Some c' ->
-  exec_instr_prop (Machsem.State s fb sp (Mgoto lbl :: c) ms m) E0
-                  (Machsem.State s fb sp c' ms m).
-Proof.
-  intros; red; intros; inv MS.
-  assert (f0 = f) by congruence. subst f0.
-  inv AT. monadInv H4. 
-  exploit find_label_goto_label; eauto. intros [tc' [rs' [GOTO [AT2 INV]]]].
-  left; exists (State rs' m'); split.
-  apply plus_one. econstructor; eauto.
-  eapply functions_transl; eauto.
-  eapply find_instr_tail; eauto.
-  simpl; eauto.
-  econstructor; eauto.
-  eapply agree_exten; eauto with ppcgen.
-  congruence.
-Qed.
-
-Lemma exec_Mbuiltin_prop:
-  forall (s : list stackframe) (f : block) (sp : val)
-         (ms : Mach.regset) (m : mem) (ef : external_function)
-         (args : list mreg) (res : mreg) (b : list Mach.instruction)
-         (t : trace) (v : val) (m' : mem),
-  external_call ef ge ms ## args m t v m' ->
-  exec_instr_prop (Machsem.State s f sp (Mbuiltin ef args res :: b) ms m) t
-                  (Machsem.State s f sp b (Regmap.set res v (undef_temps ms)) m').
-Proof.
-  intros; red; intros; inv MS.
+- (* Mbuiltin *)
   inv AT. monadInv H3. 
   exploit functions_transl; eauto. intro FN.
   generalize (transf_function_no_overflow _ _ H2); intro NOOV.
@@ -1064,28 +759,21 @@ Proof.
   eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
   econstructor; eauto.
+  eapply match_stack_extcall; eauto. 
+  intros; eapply external_call_max_perm; eauto. 
   instantiate (2 := tf); instantiate (1 := x).
   unfold nextinstr_nf, nextinstr. rewrite Pregmap.gss.
-  simpl undef_regs. repeat rewrite Pregmap.gso; auto with ppcgen. 
+  simpl undef_regs. repeat rewrite Pregmap.gso; auto with asmgen. 
   rewrite <- H0. simpl. econstructor; eauto.
   eapply code_tail_next_int; eauto.
   apply agree_nextinstr_nf. eapply agree_set_undef_mreg; eauto. 
   rewrite Pregmap.gss. auto. 
-  intros. repeat rewrite Pregmap.gso; auto with ppcgen.
+  intros. Simplifs. 
+  eapply retaddr_stored_at_extcall; eauto. 
+  intros; eapply external_call_max_perm; eauto. 
   congruence.
-Qed.
 
-Lemma exec_Mannot_prop:
-  forall (s : list stackframe) (f : block) (sp : val)
-         (ms : Mach.regset) (m : mem) (ef : external_function)
-         (args : list Mach.annot_param) (b : list Mach.instruction)
-         (vargs: list val) (t : trace) (v : val) (m' : mem),
-  Machsem.annot_arguments ms m sp args vargs ->
-  external_call ef ge vargs m t v m' ->
-  exec_instr_prop (Machsem.State s f sp (Mannot ef args :: b) ms m) t
-                  (Machsem.State s f sp b ms m').
-Proof.
-  intros; red; intros; inv MS.
+- (* Mannot *)
   inv AT. monadInv H4. 
   exploit functions_transl; eauto. intro FN.
   generalize (transf_function_no_overflow _ _ H3); intro NOOV.
@@ -1098,32 +786,35 @@ Proof.
   eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
   eapply match_states_intro with (ep := false); eauto with coqlib.
+  eapply match_stack_extcall; eauto. 
+  intros; eapply external_call_max_perm; eauto. 
   unfold nextinstr. rewrite Pregmap.gss. 
   rewrite <- H1; simpl. econstructor; eauto.
   eapply code_tail_next_int; eauto. 
   apply agree_nextinstr. auto.
+  eapply retaddr_stored_at_extcall; eauto. 
+  intros; eapply external_call_max_perm; eauto. 
   congruence.
-Qed.
 
-Lemma exec_Mcond_true_prop:
-  forall (s : list stackframe) (fb : block) (f : function) (sp : val)
-         (cond : condition) (args : list mreg) (lbl : Mach.label)
-         (c : list Mach.instruction) (ms : mreg -> val) (m : mem)
-         (c' : Mach.code),
-  eval_condition cond ms ## args m = Some true ->
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  Mach.find_label lbl (fn_code f) = Some c' ->
-  exec_instr_prop (Machsem.State s fb sp (Mcond cond args lbl :: c) ms m) E0
-                  (Machsem.State s fb sp c' (undef_temps ms) m).
-Proof.
-  intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0.
+- (* Mgoto *)
+  inv AT. monadInv H3. 
+  exploit find_label_goto_label; eauto. intros [tc' [rs' [GOTO [AT2 INV]]]].
+  left; exists (State rs' m'); split.
+  apply plus_one. econstructor; eauto.
+  eapply functions_transl; eauto.
+  eapply find_instr_tail; eauto.
+  simpl; eauto.
+  econstructor; eauto.
+  eapply agree_exten; eauto with asmgen.
+  congruence.
+
+- (* Mcond true *)
   exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
   left; eapply exec_straight_steps_goto; eauto.
-  intros. simpl in H2.
-  destruct (transl_cond_correct tge tf cond args _ _ rs m' H2)
+  intros. simpl in TR.
+  destruct (transl_cond_correct tge tf cond args _ _ rs0 m' TR)
   as [rs' [A [B C]]]. 
-  rewrite EC in B (* 8.4 *)
-   || (unfold PregEq.t in B; rewrite EC in B) (* 8.3 *).
+  rewrite EC in B.
   destruct (testcond_for_condition cond); simpl in *.
 (* simple jcc *)
   exists (Pjcc c1 lbl); exists k; exists rs'.
@@ -1131,47 +822,37 @@ Proof.
   split. eapply agree_exten_temps; eauto. 
   simpl. rewrite B. auto.
 (* jcc; jcc *)
-  destruct (eval_testcond c1 rs') as [b1|] eqn:?;
-  destruct (eval_testcond c2 rs') as [b2|] eqn:?; inv B.
+  destruct (eval_testcond c1 rs') as [b1|] eqn:TC1;
+  destruct (eval_testcond c2 rs') as [b2|] eqn:TC2; inv B.
   destruct b1.   
   (* first jcc jumps *)
   exists (Pjcc c1 lbl); exists (Pjcc c2 lbl :: k); exists rs'.
   split. eexact A.
   split. eapply agree_exten_temps; eauto. 
-  simpl. rewrite Heqo. auto.
+  simpl. rewrite TC1. auto.
   (* second jcc jumps *)
   exists (Pjcc c2 lbl); exists k; exists (nextinstr rs').
   split. eapply exec_straight_trans. eexact A. 
-  eapply exec_straight_one. simpl. rewrite Heqo. auto. auto.
-  split. eapply agree_exten_temps; eauto. 
-  intros. rewrite nextinstr_inv; auto with ppcgen.
-  simpl. rewrite eval_testcond_nextinstr. rewrite Heqo0.
+  eapply exec_straight_one. simpl. rewrite TC1. auto. auto.
+  split. eapply agree_exten_temps; eauto.
+  intros; Simplifs.
+  simpl. rewrite eval_testcond_nextinstr. rewrite TC2.
   destruct b2; auto || discriminate.
 (* jcc2 *)
-  destruct (eval_testcond c1 rs') as [b1|] eqn:?;
-  destruct (eval_testcond c2 rs') as [b2|] eqn:?; inv B.
-  destruct (andb_prop _ _ H4). subst. 
+  destruct (eval_testcond c1 rs') as [b1|] eqn:TC1;
+  destruct (eval_testcond c2 rs') as [b2|] eqn:TC2; inv B.
+  destruct (andb_prop _ _ H2). subst. 
   exists (Pjcc2 c1 c2 lbl); exists k; exists rs'.
   split. eexact A.
   split. eapply agree_exten_temps; eauto. 
-  simpl. rewrite Heqo; rewrite Heqo0; auto. 
-Qed.
+  simpl. rewrite TC1; rewrite TC2; auto.
 
-Lemma exec_Mcond_false_prop:
-  forall (s : list stackframe) (fb : block) (sp : val)
-         (cond : condition) (args : list mreg) (lbl : Mach.label)
-         (c : list Mach.instruction) (ms : mreg -> val) (m : mem),
-  eval_condition cond ms ## args m = Some false ->
-  exec_instr_prop (Machsem.State s fb sp (Mcond cond args lbl :: c) ms m) E0
-                  (Machsem.State s fb sp c (undef_temps ms) m).
-Proof.
-  intros; red; intros; inv MS.
+- (* Mcond false *)
   exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
-  left; eapply exec_straight_steps; eauto. intros. simpl in H0. 
-  destruct (transl_cond_correct tge tf cond args _ _ rs m' H0)
+  left; eapply exec_straight_steps; eauto. intros. simpl in TR. 
+  destruct (transl_cond_correct tge tf cond args _ _ rs0 m' TR)
   as [rs' [A [B C]]]. 
-  rewrite EC in B (* 8.4 *)
-   || (unfold PregEq.t in B; rewrite EC in B) (* 8.3 *).
+  rewrite EC in B.
   destruct (testcond_for_condition cond); simpl in *.
 (* simple jcc *)
   econstructor; split.
@@ -1180,149 +861,119 @@ Proof.
   split. apply agree_nextinstr. eapply agree_exten_temps; eauto.
   simpl; congruence.
 (* jcc ; jcc *)
-  destruct (eval_testcond c1 rs') as [b1|] eqn:?;
-  destruct (eval_testcond c2 rs') as [b2|] eqn:?; inv B.
-  destruct (orb_false_elim _ _ H2); subst.
+  destruct (eval_testcond c1 rs') as [b1|] eqn:TC1;
+  destruct (eval_testcond c2 rs') as [b2|] eqn:TC2; inv B.
+  destruct (orb_false_elim _ _ H1); subst.
   econstructor; split.
   eapply exec_straight_trans. eexact A. 
-  eapply exec_straight_two. simpl. rewrite Heqo. eauto. auto. 
-  simpl. rewrite eval_testcond_nextinstr. rewrite Heqo0. eauto. auto. auto.
+  eapply exec_straight_two. simpl. rewrite TC1. eauto. auto. 
+  simpl. rewrite eval_testcond_nextinstr. rewrite TC2. eauto. auto. auto.
   split. apply agree_nextinstr. apply agree_nextinstr. eapply agree_exten_temps; eauto.
   simpl; congruence.
 (* jcc2 *)
-  destruct (eval_testcond c1 rs') as [b1|] eqn:?;
-  destruct (eval_testcond c2 rs') as [b2|] eqn:?; inv B.
+  destruct (eval_testcond c1 rs') as [b1|] eqn:TC1;
+  destruct (eval_testcond c2 rs') as [b2|] eqn:TC2; inv B.
   exists (nextinstr rs'); split.
   eapply exec_straight_trans. eexact A. 
   apply exec_straight_one. simpl. 
-  rewrite Heqo; rewrite Heqo0. 
+  rewrite TC1; rewrite TC2. 
   destruct b1. simpl in *. subst b2. auto. auto.
   auto.
   split. apply agree_nextinstr. eapply agree_exten_temps; eauto.
-  rewrite H2; congruence.
-Qed.
+  rewrite H1; congruence.
 
-Lemma exec_Mjumptable_prop:
-  forall (s : list stackframe) (fb : block) (f : function) (sp : val)
-         (arg : mreg) (tbl : list Mach.label) (c : list Mach.instruction)
-         (rs : mreg -> val) (m : mem) (n : int) (lbl : Mach.label)
-         (c' : Mach.code),
-  rs arg = Vint n ->
-  list_nth_z tbl (Int.unsigned n) = Some lbl ->
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  Mach.find_label lbl (fn_code f) = Some c' ->
-  exec_instr_prop
-    (Machsem.State s fb sp (Mjumptable arg tbl :: c) rs m) E0
-    (Machsem.State s fb sp c' (undef_temps rs) m).
-Proof.
-  intros; red; intros; inv MS.
-  assert (f0 = f) by congruence. subst f0.
-  inv AT. monadInv H6. 
+- (* Mjumptable *)
+  inv AT. monadInv H5. 
   exploit functions_transl; eauto. intro FN.
-  generalize (transf_function_no_overflow _ _ H5); intro NOOV.
+  generalize (transf_function_no_overflow _ _ H4); intro NOOV.
   exploit find_label_goto_label. eauto. eauto. instantiate (2 := rs0#ECX <- Vundef #EDX <- Vundef). 
-  rewrite Pregmap.gso; auto with ppcgen. rewrite Pregmap.gso; auto with ppcgen. eauto. eauto. 
+  repeat (rewrite Pregmap.gso by auto with asmgen). eauto. eauto. 
   intros [tc' [rs' [A [B C]]]].
   exploit ireg_val; eauto. rewrite H. intros LD; inv LD.
   left; econstructor; split.
   apply plus_one. econstructor; eauto. 
   eapply find_instr_tail; eauto. 
-  simpl. rewrite <- H9. unfold Mach.label in H0; unfold label; rewrite H0. eauto.
+  simpl. rewrite <- H8. unfold Mach.label in H0; unfold label; rewrite H0. eauto.
   econstructor; eauto. 
-  eapply agree_exten_temps; eauto. intros. rewrite C; auto with ppcgen. 
-  repeat rewrite Pregmap.gso; auto with ppcgen. 
+  eapply agree_exten_temps; eauto. intros. rewrite C; auto with asmgen. Simplifs. 
   congruence.
-Qed.
 
-Lemma exec_Mreturn_prop:
-  forall (s : list stackframe) (fb stk : block) (soff : int)
-         (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function) m',
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
-  load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
-  Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-  exec_instr_prop (Machsem.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0
-                  (Returnstate s ms m').
-Proof.
-  intros; red; intros; inv MS.
-  assert (f0 = f) by congruence. subst f0.
+- (* Mreturn *)
   inv AT. 
   assert (NOOV: list_length_z tf <= Int.max_unsigned).
     eapply transf_function_no_overflow; eauto.
   rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *.
-  exploit Mem.loadv_extends. eauto. eexact H0. auto. simpl. intros [parent' [A B]]. 
+  exploit Mem.loadv_extends. eauto. eexact H. auto. simpl. intros [parent' [A B]]. 
   exploit lessdef_parent_sp; eauto. intros. subst parent'. clear B.
-  exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [ra' [C D]].
-  exploit lessdef_parent_ra; eauto. intros. subst ra'. clear D.
-  exploit Mem.free_parallel_extends; eauto. intros [m2' [E F]]. 
-  monadInv H6.
+  assert (C: Mem.loadv Mint32 m'0 (Val.add (rs0 ESP) (Vint (fn_retaddr_ofs f))) = Some ra).
+Opaque Int.repr.
+    erewrite agree_sp; eauto. simpl. rewrite Int.add_zero_l.
+    eapply rsa_contains; eauto.
+  exploit retaddr_stored_at_can_free; eauto. intros [m2' [E F]].
+  assert (M: match_stack ge s m'' m2' ra (Mem.nextblock m'')).
+    apply match_stack_change_bound with stk.
+    eapply match_stack_free_left; eauto.
+    eapply match_stack_free_left; eauto.
+    eapply match_stack_free_right; eauto. omega.
+    apply Z.lt_le_incl. change (Mem.valid_block m'' stk).
+    eapply Mem.valid_block_free_1; eauto. eapply Mem.valid_block_free_1; eauto. 
+    eapply retaddr_stored_at_valid; eauto.
+  monadInv H5.
   exploit code_tail_next_int; eauto. intro CT1.
   left; econstructor; split.
   eapply plus_left. eapply exec_step_internal. eauto.
   eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
   simpl. rewrite C. rewrite A. rewrite <- (sp_val _ _ _ AG). rewrite E. eauto.
   apply star_one. eapply exec_step_internal. 
-  transitivity (Val.add rs#PC Vone). auto. rewrite <- H3. simpl. eauto.
+  transitivity (Val.add rs0#PC Vone). auto. rewrite <- H2. simpl. eauto.
   eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
   simpl. eauto. traceEq.
   constructor; auto.
   apply agree_set_other; auto. apply agree_nextinstr. apply agree_set_other; auto.
   eapply agree_change_sp; eauto. eapply parent_sp_def; eauto.
-Qed.
 
-Lemma exec_function_internal_prop:
-  forall (s : list stackframe) (fb : block) (ms : Mach.regset)
-         (m : mem) (f : function) (m1 m2 m3 : mem) (stk : block),
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  Mem.alloc m 0 (fn_stacksize f) = (m1, stk) ->
-  let sp := Vptr stk Int.zero in
-  store_stack m1 sp Tint f.(fn_link_ofs) (parent_sp s) = Some m2 ->
-  store_stack m2 sp Tint f.(fn_retaddr_ofs) (parent_ra s) = Some m3 ->
-  exec_instr_prop (Machsem.Callstate s fb ms m) E0
-                  (Machsem.State s fb sp (fn_code f) (undef_temps ms) m3).
-Proof.
-  intros; red; intros; inv MS.
+- (* internal function *)
   exploit functions_translated; eauto. intros [tf [A B]]. monadInv B.
   generalize EQ; intros EQ'. monadInv EQ'. 
   destruct (zlt (list_length_z x0) Int.max_unsigned); inversion EQ1. clear EQ1.
   unfold store_stack in *. 
   exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. 
   intros [m1' [C D]].
-  exploit Mem.storev_extends. eauto. eexact H1. eauto. eauto. 
-  intros [m2' [E F]].
-  exploit Mem.storev_extends. eexact F. eauto. eauto. eauto. 
-  intros [m3' [P Q]].
+  assert (E: Mem.extends m2 m1') by (eapply Mem.free_left_extends; eauto).
+  exploit Mem.storev_extends. eexact E. eexact H1. eauto. eauto. 
+  intros [m2' [F G]].
+  exploit retaddr_stored_at_can_alloc. eexact H. eauto. eauto. eauto. eauto. 
+  auto. auto. auto. auto. eauto. 
+  intros [m3' [P [Q R]]].
   left; econstructor; split.
   apply plus_one. econstructor; eauto. 
-  rewrite <- H4; simpl. eauto. 
-  simpl. rewrite C. simpl in E. rewrite (sp_val _ _ _ AG) in E. rewrite E.
-  rewrite ATLR. simpl in P. rewrite P. eauto. 
-  econstructor; eauto. 
-  unfold nextinstr. rewrite Pregmap.gss. repeat rewrite Pregmap.gso; auto with ppcgen. 
+  subst x; simpl. rewrite Int.unsigned_zero. simpl. eauto. 
+  simpl. rewrite C. simpl in F. rewrite (sp_val _ _ _ AG) in F. rewrite F.
+  rewrite Int.add_zero_l. rewrite P. eauto. 
+  econstructor; eauto.
+  assert (STK: stk = Mem.nextblock m) by (eapply Mem.alloc_result; eauto).
+  rewrite <- STK in STACKS. simpl in F. simpl in H1.
+  eapply match_stack_invariant; eauto.
+  intros. eapply Mem.perm_alloc_4; eauto. eapply Mem.perm_free_3; eauto. 
+  eapply Mem.perm_store_2; eauto. unfold block; omega.
+  intros. eapply Mem.perm_store_1; eauto. eapply Mem.perm_store_1; eauto. 
+  eapply Mem.perm_alloc_1; eauto. 
+  intros. erewrite Mem.load_store_other. 2: eauto.
+  erewrite Mem.load_store_other. 2: eauto. 
+  eapply Mem.load_alloc_other; eauto.
+  left; unfold block; omega.
+  left; unfold block; omega.
+  unfold nextinstr. rewrite Pregmap.gss. repeat rewrite Pregmap.gso; auto with asmgen. 
   rewrite ATPC. simpl. constructor; eauto.
-  subst x. eapply code_tail_next_int. rewrite list_length_z_cons. omega. 
+  subst x. unfold fn_code. eapply code_tail_next_int. rewrite list_length_z_cons. omega. 
   constructor. 
   apply agree_nextinstr. eapply agree_change_sp; eauto.
-  apply agree_exten_temps with rs; eauto.
-  intros. apply Pregmap.gso; auto with ppcgen.
+  apply agree_exten_temps with rs0; eauto.
+  intros; Simplifs.
   congruence. 
-  intros. rewrite nextinstr_inv; auto with ppcgen. 
-  rewrite Pregmap.gso; auto with ppcgen. 
-  rewrite Pregmap.gss. eapply agree_sp; eauto. 
-Qed.
+  intros. Simplifs. eapply agree_sp; eauto.
 
-Lemma exec_function_external_prop:
-  forall (s : list stackframe) (fb : block) (ms : Mach.regset)
-         (m : mem) (t0 : trace) (ms' : RegEq.t -> val)
-         (ef : external_function) (args : list val) (res : val) (m': mem),
-  Genv.find_funct_ptr ge fb = Some (External ef) ->
-  external_call ef ge args m t0 res m' ->
-  Machsem.extcall_arguments ms m (parent_sp s) (ef_sig ef) args ->
-  ms' = Regmap.set (loc_result (ef_sig ef)) res ms ->
-  exec_instr_prop (Machsem.Callstate s fb ms m)
-               t0 (Machsem.Returnstate s ms' m').
-Proof.
-  intros; red; intros; inv MS.
+- (* external function *)
   exploit functions_translated; eauto.
   intros [tf [A B]]. simpl in B. inv B.
   exploit extcall_arguments_match; eauto. 
@@ -1334,63 +985,38 @@ Proof.
   eapply external_call_symbols_preserved; eauto. 
   exact symbols_preserved. exact varinfo_preserved.
   econstructor; eauto.
+  rewrite Pregmap.gss. apply match_stack_change_bound with (Mem.nextblock m). 
+  eapply match_stack_extcall; eauto.
+  intros. eapply external_call_max_perm; eauto.
+  eapply external_call_nextblock; eauto.
   unfold loc_external_result.
   eapply agree_set_mreg; eauto. 
-  rewrite Pregmap.gso; auto with ppcgen. rewrite Pregmap.gss. auto. 
-  intros. repeat rewrite Pregmap.gso; auto with ppcgen.
-Qed.
+  rewrite Pregmap.gso; auto with asmgen. rewrite Pregmap.gss. auto. 
+  intros; Simplifs.
 
-Lemma exec_return_prop:
-  forall (s : list stackframe) (fb : block) (sp ra : val)
-         (c : Mach.code) (ms : Mach.regset) (m : mem),
-  exec_instr_prop (Machsem.Returnstate (Stackframe fb sp ra c :: s) ms m) E0
-                  (Machsem.State s fb sp c ms m).
-Proof.
-  intros; red; intros; inv MS. inv STACKS. simpl in *.
+- (* return *)
+  inv STACKS. simpl in *.
   right. split. omega. split. auto. 
-  econstructor; eauto. rewrite ATPC; eauto.  
-  congruence.
+  econstructor; eauto. congruence.
 Qed.
 
-Theorem transf_instr_correct:
-  forall s1 t s2, Machsem.step ge s1 t s2 ->
-  exec_instr_prop s1 t s2.
-Proof
-  (Machsem.step_ind ge exec_instr_prop
-           exec_Mlabel_prop
-           exec_Mgetstack_prop
-           exec_Msetstack_prop
-           exec_Mgetparam_prop
-           exec_Mop_prop
-           exec_Mload_prop
-           exec_Mstore_prop
-           exec_Mcall_prop
-           exec_Mtailcall_prop
-           exec_Mbuiltin_prop
-           exec_Mannot_prop
-           exec_Mgoto_prop
-           exec_Mcond_true_prop
-           exec_Mcond_false_prop
-           exec_Mjumptable_prop
-           exec_Mreturn_prop
-           exec_function_internal_prop
-           exec_function_external_prop
-           exec_return_prop).
-
 Lemma transf_initial_states:
-  forall st1, Machsem.initial_state prog st1 ->
+  forall st1, Mach.initial_state prog st1 ->
   exists st2, Asm.initial_state tprog st2 /\ match_states st1 st2.
 Proof.
   intros. inversion H. unfold ge0 in *.
+  exploit functions_translated; eauto. intros [tf [A B]]. 
   econstructor; split.
   econstructor.
   eapply Genv.init_mem_transf_partial; eauto.
   replace (symbol_offset (Genv.globalenv tprog) (prog_main tprog) Int.zero)
-     with (Vptr fb Int.zero).
-  econstructor; eauto. constructor. apply Mem.extends_refl.
-  split. auto. unfold parent_sp; congruence.
-  intros. repeat rewrite Pregmap.gso; auto with ppcgen.
-  destruct r; simpl; congruence.
+     with (Vptr b Int.zero).
+  econstructor; eauto.
+  constructor.
+  apply Mem.extends_refl.
+  split. auto. intros. rewrite Regmap.gi. auto. 
+  reflexivity. 
+  exact I.
   unfold symbol_offset. 
   rewrite (transform_partial_program_main _ _ TRANSF). 
   rewrite symbols_preserved. unfold ge; rewrite H1. auto.
@@ -1398,21 +1024,22 @@ Qed.
 
 Lemma transf_final_states:
   forall st1 st2 r, 
-  match_states st1 st2 -> Machsem.final_state st1 r -> Asm.final_state st2 r.
+  match_states st1 st2 -> Mach.final_state st1 r -> Asm.final_state st2 r.
 Proof.
-  intros. inv H0. inv H. constructor. auto. 
+  intros. inv H0. inv H. inv STACKS. constructor.
+  auto. 
   compute in H1. 
   generalize (preg_val _ _ _ AX AG). rewrite H1. intros LD; inv LD. auto.
 Qed.
 
 Theorem transf_program_correct:
-  forward_simulation (Machsem.semantics prog) (Asm.semantics tprog).
+  forward_simulation (Mach.semantics prog) (Asm.semantics tprog).
 Proof.
   eapply forward_simulation_star with (measure := measure).
   eexact symbols_preserved.
   eexact transf_initial_states.
   eexact transf_final_states.
-  exact transf_instr_correct. 
+  exact step_simulation.
 Qed.
 
 End PRESERVATION.
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index b524539..75d59a4 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -23,233 +23,29 @@ Require Import Globalenvs.
 Require Import Op.
 Require Import Locations.
 Require Import Mach.
-Require Import Machsem.
 Require Import Machtyping.
 Require Import Asm.
 Require Import Asmgen.
+Require Import Asmgenproof0.
 Require Import Conventions.
 
 Open Local Scope error_monad_scope.
 
 (** * Correspondence between Mach registers and IA32 registers *)
 
-Hint Extern 2 (_ <> _) => congruence: ppcgen.
-
-Lemma preg_of_injective:
-  forall r1 r2, preg_of r1 = preg_of r2 -> r1 = r2.
-Proof.
-  destruct r1; destruct r2; simpl; intros; reflexivity || discriminate.
-Qed.
-
-Lemma preg_of_not_ESP:
-  forall r, preg_of r <> ESP.
-Proof.
-  destruct r; simpl; congruence.
-Qed.
-
-Lemma preg_of_not_PC:
-  forall r, preg_of r <> PC.
-Proof.
-  destruct r; simpl; congruence.
-Qed.
-
-Hint Resolve preg_of_not_ESP preg_of_not_PC: ppcgen.
-
-Lemma ireg_of_eq:
-  forall r r', ireg_of r = OK r' -> preg_of r = IR r'.
-Proof.
-  unfold ireg_of; intros. destruct (preg_of r); inv H; auto.
-Qed.
-
-Lemma freg_of_eq:
-  forall r r', freg_of r = OK r' -> preg_of r = FR r'.
-Proof.
-  unfold freg_of; intros. destruct (preg_of r); inv H; auto.
-Qed.
-
-(** Agreement between Mach register sets and IA32 register sets. *)
-
-Record agree (ms: Mach.regset) (sp: val) (rs: Asm.regset) : Prop := mkagree {
-  agree_sp: rs#ESP = sp;
-  agree_sp_def: sp <> Vundef;
-  agree_mregs: forall r: mreg, Val.lessdef (ms r) (rs#(preg_of r))
-}.
-
-Lemma preg_val:
-  forall ms sp rs r,
-  agree ms sp rs -> Val.lessdef (ms r) rs#(preg_of r).
-Proof.
-  intros. destruct H. auto.
-Qed.
-
-Lemma preg_vals:
-  forall ms sp rs, agree ms sp rs ->
-  forall l, Val.lessdef_list (map ms l) (map rs (map preg_of l)).
-Proof.
-  induction l; simpl. constructor. constructor. eapply preg_val; eauto. auto.
-Qed.
-
-Lemma ireg_val:
-  forall ms sp rs r r',
-  agree ms sp rs ->
-  ireg_of r = OK r' ->
-  Val.lessdef (ms r) rs#r'.
-Proof.
-  intros. rewrite <- (ireg_of_eq _ _ H0). eapply preg_val; eauto.
-Qed.
-
-Lemma freg_val:
-  forall ms sp rs r r',
-  agree ms sp rs ->
-  freg_of r = OK r' ->
-  Val.lessdef (ms r) (rs#r').
-Proof.
-  intros. rewrite <- (freg_of_eq _ _ H0). eapply preg_val; eauto.
-Qed.
-
-Lemma sp_val:
-  forall ms sp rs,
-  agree ms sp rs ->
-  sp = rs#ESP.
-Proof.
-  intros. destruct H; auto.
-Qed.
-
-Hint Resolve preg_val ireg_val freg_val sp_val: ppcgen.
-
-Definition important_preg (r: preg) : bool :=
-  match r with
-  | PC => false
-  | IR _ => true
-  | FR _ => true
-  | ST0 => true
-  | CR _ => false
-  | RA => false
-  end.
-
-Lemma preg_of_important:
-  forall r, important_preg (preg_of r) = true.
-Proof.
-  intros. destruct r; reflexivity.
-Qed.
-
-Lemma important_diff:
-  forall r r',
-  important_preg r = true -> important_preg r' = false -> r <> r'.
-Proof.
-  congruence.
-Qed.
-Hint Resolve important_diff: ppcgen.
-
-Lemma agree_exten:
-  forall ms sp rs rs',
-  agree ms sp rs ->
-  (forall r, important_preg r = true -> rs'#r = rs#r) ->
-  agree ms sp rs'.
-Proof.
-  intros. destruct H. split. 
-  rewrite H0; auto. auto.
-  intros. rewrite H0; auto. apply preg_of_important.
-Qed.
-
-(** Preservation of register agreement under various assignments. *)
-
-Lemma agree_set_mreg:
-  forall ms sp rs r v rs',
-  agree ms sp rs ->
-  Val.lessdef v (rs'#(preg_of r)) ->
-  (forall r', important_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') ->
-  agree (Regmap.set r v ms) sp rs'.
-Proof.
-  intros. destruct H. split.
-  rewrite H1; auto. apply sym_not_equal. apply preg_of_not_ESP.
-  auto.
-  intros. unfold Regmap.set. destruct (RegEq.eq r0 r). congruence. 
-  rewrite H1. auto. apply preg_of_important.
-  red; intros; elim n. eapply preg_of_injective; eauto.
-Qed.
-
-Lemma agree_set_other:
-  forall ms sp rs r v,
-  agree ms sp rs ->
-  important_preg r = false ->
-  agree ms sp (rs#r <- v).
-Proof.
-  intros. apply agree_exten with rs. auto.
-  intros. apply Pregmap.gso. congruence.
-Qed.
-
-Lemma agree_nextinstr:
-  forall ms sp rs,
-  agree ms sp rs -> agree ms sp (nextinstr rs).
-Proof.
-  intros. unfold nextinstr. apply agree_set_other. auto. auto.
-Qed.
-
-Lemma agree_undef_unimportant_regs:
-  forall ms sp rl rs,
-  agree ms sp rs ->
-  (forall r, In r rl -> important_preg r = false) ->
-  agree ms sp (undef_regs rl rs).
-Proof.
-  induction rl; simpl; intros. auto.
-  apply IHrl. apply agree_exten with rs; auto.
-  intros. apply Pregmap.gso. red; intros; subst.
-  assert (important_preg a = false) by auto. congruence.
-  intros. apply H0; auto.
-Qed.
-
 Lemma agree_nextinstr_nf:
   forall ms sp rs,
   agree ms sp rs -> agree ms sp (nextinstr_nf rs).
 Proof.
   intros. unfold nextinstr_nf. apply agree_nextinstr. 
-  apply agree_undef_unimportant_regs. auto.
-  intro. simpl. ElimOrEq; auto.
-Qed.
-
-Definition nontemp_preg (r: preg) : bool :=
-  match r with
-  | PC => false
-  | IR ECX => false
-  | IR EDX => false
-  | IR _ => true
-  | FR XMM6 => false
-  | FR XMM7 => false
-  | FR _ => true
-  | ST0 => false
-  | CR _ => false
-  | RA => false
-  end.
-
-Lemma nontemp_diff:
-  forall r r',
-  nontemp_preg r = true -> nontemp_preg r' = false -> r <> r'.
-Proof.
-  congruence.
-Qed.
-
-Hint Resolve nontemp_diff: ppcgen.
-
-Lemma agree_exten_temps:
-  forall ms sp rs rs',
-  agree ms sp rs ->
-  (forall r, nontemp_preg r = true -> rs'#r = rs#r) ->
-  agree (undef_temps ms) sp rs'.
-Proof.
-  intros. destruct H. split. 
-  rewrite H0; auto. auto. 
-  intros. unfold undef_temps. 
-  destruct (In_dec mreg_eq r temporary_regs).
-  rewrite Mach.undef_regs_same; auto. 
-  rewrite Mach.undef_regs_other; auto. rewrite H0; auto.
-  simpl in n. destruct r; auto; intuition.
+  apply agree_undef_regs. auto.
+  intro. simpl. ElimOrEq; auto. 
 Qed.
 
 Lemma agree_undef_move:
   forall ms sp rs rs',
   agree ms sp rs ->
-  (forall r, important_preg r = true -> r <> ST0 -> rs'#r = rs#r) ->
+  (forall r, data_preg r = true -> r <> ST0 -> rs'#r = rs#r) ->
   agree (undef_move ms) sp rs'.
 Proof.
   intros. destruct H. split. 
@@ -258,30 +54,16 @@ Proof.
   destruct (In_dec mreg_eq r destroyed_at_move_regs).
   rewrite Mach.undef_regs_same; auto. 
   rewrite Mach.undef_regs_other; auto.
-  assert (important_preg (preg_of r) = true /\ preg_of r <> ST0).
+  assert (data_preg (preg_of r) = true /\ preg_of r <> ST0).
     simpl in n. destruct r; simpl; auto; intuition congruence.
   destruct H. rewrite H0; auto.
 Qed.
 
-Lemma agree_set_undef_mreg:
-  forall ms sp rs r v rs',
-  agree ms sp rs ->
-  Val.lessdef v (rs'#(preg_of r)) ->
-  (forall r', nontemp_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') ->
-  agree (Regmap.set r v (undef_temps ms)) sp rs'.
-Proof.
-  intros. apply agree_set_mreg with (rs'#(preg_of r) <- (rs#(preg_of r))); auto.
-  eapply agree_exten_temps; eauto. 
-  intros. unfold Pregmap.set. destruct (PregEq.eq r0 (preg_of r)). 
-  congruence. auto. 
-  intros. rewrite Pregmap.gso; auto. 
-Qed.
-
 Lemma agree_set_undef_move_mreg:
   forall ms sp rs r v rs',
   agree ms sp rs ->
   Val.lessdef v (rs'#(preg_of r)) ->
-  (forall r', important_preg r' = true /\ r' <> ST0 -> r' <> preg_of r -> rs'#r' = rs#r') ->
+  (forall r', data_preg r' = true /\ r' <> ST0 -> r' <> preg_of r -> rs'#r' = rs#r') ->
   agree (Regmap.set r v (undef_move ms)) sp rs'.
 Proof.
   intros. apply agree_set_mreg with (rs'#(preg_of r) <- (rs#(preg_of r))); auto.
@@ -293,30 +75,6 @@ Qed.
 
 (** Useful properties of the PC register. *)
 
-Lemma nextinstr_inv:
-  forall r rs,
-  r <> PC ->
-  (nextinstr rs)#r = rs#r.
-Proof.
-  intros. unfold nextinstr. apply Pregmap.gso. red; intro; subst. auto.
-Qed.
-
-Lemma nextinstr_inv2:
-  forall r rs,
-  nontemp_preg r = true ->
-  (nextinstr rs)#r = rs#r.
-Proof.
-  intros. apply nextinstr_inv. red; intro; subst; discriminate.
-Qed.
-
-Lemma nextinstr_set_preg:
-  forall rs m v,
-  (nextinstr (rs#(preg_of m) <- v))#PC = Val.add rs#PC Vone.
-Proof.
-  intros. unfold nextinstr. rewrite Pregmap.gss. 
-  rewrite Pregmap.gso. auto. apply sym_not_eq. apply preg_of_not_PC. 
-Qed.
-
 Lemma nextinstr_nf_inv:
   forall r rs, 
   match r with PC => False | CR _ => False | _ => True end ->
@@ -333,18 +91,16 @@ Qed.
 
 Lemma nextinstr_nf_inv1:
   forall r rs,
-  important_preg r = true -> (nextinstr_nf rs)#r = rs#r.
+  data_preg r = true -> (nextinstr_nf rs)#r = rs#r.
 Proof.
-  intros. apply nextinstr_nf_inv. unfold important_preg in H. 
-  destruct r; auto; congruence.
+  intros. apply nextinstr_nf_inv. destruct r; auto || discriminate.
 Qed.
 
 Lemma nextinstr_nf_inv2:
   forall r rs, 
   nontemp_preg r = true -> (nextinstr_nf rs)#r = rs#r.
 Proof.
-  intros. apply nextinstr_nf_inv. unfold nontemp_preg in H. 
-  destruct r; auto; congruence.
+  intros. apply nextinstr_nf_inv1; auto with asmgen.
 Qed.
 
 Lemma nextinstr_nf_set_preg:
@@ -356,210 +112,70 @@ Proof.
   apply nextinstr_set_preg.
 Qed.
 
-(** Connection between Mach and Asm calling conventions for external
-    functions. *)
-
-Lemma extcall_arg_match:
-  forall ms sp rs m m' l v,
-  agree ms sp rs ->
-  Machsem.extcall_arg ms m sp l v ->
-  Mem.extends m m' ->
-  exists v', Asm.extcall_arg rs m' l v' /\ Val.lessdef v v'.
-Proof.
-  intros. inv H0.
-  exists (rs#(preg_of r)); split. constructor. eauto with ppcgen.
-  unfold load_stack in H2. 
-  exploit Mem.loadv_extends; eauto. intros [v' [A B]].
-  rewrite (sp_val _ _ _ H) in A. 
-  exists v'; split; auto. destruct ty; econstructor; eauto.
-Qed.
-
-Lemma extcall_args_match:
-  forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
-  forall ll vl,
-  list_forall2 (Machsem.extcall_arg ms m sp) ll vl ->
-  exists vl', list_forall2 (Asm.extcall_arg rs m') ll vl' /\ Val.lessdef_list vl vl'.
-Proof.
-  induction 3.
-  exists (@nil val); split; constructor.
-  exploit extcall_arg_match; eauto. intros [v1' [A B]].
-  destruct IHlist_forall2 as [vl' [C D]].
-  exists(v1' :: vl'); split. constructor; auto. constructor; auto.
-Qed.
-
-Lemma extcall_arguments_match:
-  forall ms m sp rs sg args m',
-  agree ms sp rs ->
-  Machsem.extcall_arguments ms m sp sg args ->
-  Mem.extends m m' ->
-  exists args', Asm.extcall_arguments rs m' sg args' /\ Val.lessdef_list args args'.
-Proof.
-  unfold Machsem.extcall_arguments, Asm.extcall_arguments; intros.
-  eapply extcall_args_match; eauto.
-Qed.
-
-(** Translation of arguments to annotations. *)
+(** Useful simplification tactic *)
 
-Lemma annot_arg_match:
-  forall ms sp rs m m' p v,
-  agree ms sp rs ->
-  Mem.extends m m' ->
-  Machsem.annot_arg ms m sp p v ->
-  exists v', Asm.annot_arg rs m' (transl_annot_param p) v' /\ Val.lessdef v v'.
-Proof.
-  intros. inv H1; simpl.
-(* reg *)
-  exists (rs (preg_of r)); split. 
-  unfold preg_of. destruct (mreg_type r); constructor. 
-  eapply preg_val; eauto.
-(* stack *)
-  exploit Mem.load_extends; eauto. intros [v' [A B]].
-  exists v'; split; auto. 
-  inv H. econstructor; eauto. 
-Qed.
+Ltac Simplif :=
+  match goal with
+  | [ |- nextinstr_nf _ _ = _ ] =>
+      ((rewrite nextinstr_nf_inv by auto with asmgen)
+       || (rewrite nextinstr_nf_inv1 by auto with asmgen)); auto
+  | [ |- nextinstr _ _ = _ ] =>
+      ((rewrite nextinstr_inv by auto with asmgen)
+       || (rewrite nextinstr_inv1 by auto with asmgen)); auto
+  | [ |- Pregmap.get ?x (Pregmap.set ?x _ _) = _ ] =>
+      rewrite Pregmap.gss; auto
+  | [ |- Pregmap.set ?x _ _ ?x = _ ] =>
+      rewrite Pregmap.gss; auto
+  | [ |- Pregmap.get _ (Pregmap.set _ _ _) = _ ] =>
+      rewrite Pregmap.gso by (auto with asmgen); auto
+  | [ |- Pregmap.set _ _ _ _ = _ ] =>
+      rewrite Pregmap.gso by (auto with asmgen); auto
+  end.
 
-Lemma annot_arguments_match:
-  forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
-  forall pl vl,
-  Machsem.annot_arguments ms m sp pl vl ->
-  exists vl', Asm.annot_arguments rs m' (map transl_annot_param pl) vl'
-           /\ Val.lessdef_list vl vl'.
-Proof.
-  induction 3; intros. 
-  exists (@nil val); split. constructor. constructor.
-  exploit annot_arg_match; eauto. intros [v1' [A B]].
-  destruct IHlist_forall2 as [vl' [C D]].
-  exists (v1' :: vl'); split; constructor; auto.
-Qed.
+Ltac Simplifs := repeat Simplif.
 
-(** * Execution of straight-line code *)
+(** * Correctness of IA32 constructor functions *)
 
-Section STRAIGHTLINE.
+Section CONSTRUCTORS.
 
 Variable ge: genv.
 Variable fn: code.
 
-(** Straight-line code is composed of processor instructions that execute
-  in sequence (no branches, no function calls and returns).
-  The following inductive predicate relates the machine states
-  before and after executing a straight-line sequence of instructions.
-  Instructions are taken from the first list instead of being fetched
-  from memory. *)
-
-Inductive exec_straight: code -> regset -> mem -> 
-                         code -> regset -> mem -> Prop :=
-  | exec_straight_one:
-      forall i1 c rs1 m1 rs2 m2,
-      exec_instr ge fn i1 rs1 m1 = Next rs2 m2 ->
-      rs2#PC = Val.add rs1#PC Vone ->
-      exec_straight (i1 :: c) rs1 m1 c rs2 m2
-  | exec_straight_step:
-      forall i c rs1 m1 rs2 m2 c' rs3 m3,
-      exec_instr ge fn i rs1 m1 = Next rs2 m2 ->
-      rs2#PC = Val.add rs1#PC Vone ->
-      exec_straight c rs2 m2 c' rs3 m3 ->
-      exec_straight (i :: c) rs1 m1 c' rs3 m3.
-
-Lemma exec_straight_trans:
-  forall c1 rs1 m1 c2 rs2 m2 c3 rs3 m3,
-  exec_straight c1 rs1 m1 c2 rs2 m2 ->
-  exec_straight c2 rs2 m2 c3 rs3 m3 ->
-  exec_straight c1 rs1 m1 c3 rs3 m3.
-Proof.
-  induction 1; intros.
-  apply exec_straight_step with rs2 m2; auto.
-  apply exec_straight_step with rs2 m2; auto.
-Qed.
-
-Lemma exec_straight_two:
-  forall i1 i2 c rs1 m1 rs2 m2 rs3 m3,
-  exec_instr ge fn i1 rs1 m1 = Next rs2 m2 ->
-  exec_instr ge fn i2 rs2 m2 = Next rs3 m3 ->
-  rs2#PC = Val.add rs1#PC Vone ->
-  rs3#PC = Val.add rs2#PC Vone ->
-  exec_straight (i1 :: i2 :: c) rs1 m1 c rs3 m3.
-Proof.
-  intros. apply exec_straight_step with rs2 m2; auto.
-  apply exec_straight_one; auto.
-Qed.
-
-Lemma exec_straight_three:
-  forall i1 i2 i3 c rs1 m1 rs2 m2 rs3 m3 rs4 m4,
-  exec_instr ge fn i1 rs1 m1 = Next rs2 m2 ->
-  exec_instr ge fn i2 rs2 m2 = Next rs3 m3 ->
-  exec_instr ge fn i3 rs3 m3 = Next rs4 m4 ->
-  rs2#PC = Val.add rs1#PC Vone ->
-  rs3#PC = Val.add rs2#PC Vone ->
-  rs4#PC = Val.add rs3#PC Vone ->
-  exec_straight (i1 :: i2 :: i3 :: c) rs1 m1 c rs4 m4.
-Proof.
-  intros. apply exec_straight_step with rs2 m2; auto.
-  eapply exec_straight_two; eauto.
-Qed.
-
-(** * Correctness of IA32 constructor functions *)
-
 (** Smart constructor for moves. *)
 
 Lemma mk_mov_correct:
   forall rd rs k c rs1 m,
   mk_mov rd rs k = OK c ->
   exists rs2,
-     exec_straight c rs1 m k rs2 m
+     exec_straight ge fn c rs1 m k rs2 m
   /\ rs2#rd = rs1#rs
-  /\ forall r, important_preg r = true -> r <> ST0 -> r <> rd -> rs2#r = rs1#r.
+  /\ forall r, data_preg r = true -> r <> ST0 -> r <> rd -> rs2#r = rs1#r.
 Proof.
   unfold mk_mov; intros. 
   destruct rd; try (monadInv H); destruct rs; monadInv H.
 (* mov *)
   econstructor. split. apply exec_straight_one. simpl. eauto. auto. 
-  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
-  intros. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gso. auto. 
+  split. Simplifs. intros; Simplifs. 
 (* movd *)
   econstructor. split. apply exec_straight_one. simpl. eauto. auto. 
-  split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
-  intros. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gso. auto. 
+  split. Simplifs. intros; Simplifs.
 (* getfp0 *)
   econstructor. split. apply exec_straight_one. simpl. eauto. auto. 
-  split. rewrite nextinstr_inv; auto with ppcgen. 
-  rewrite Pregmap.gso; auto with ppcgen.
-  apply Pregmap.gss.
-  intros. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gso; auto. rewrite Pregmap.gso; auto.
+  split. Simplifs. intros; Simplifs.
 (* setfp0 *)
   econstructor. split. apply exec_straight_one. simpl. eauto. auto. 
-  split. auto. 
-  intros. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gso. auto. 
+  split. Simplifs. intros; Simplifs.
 Qed.
 
 (** Smart constructor for shifts *)
 
-Ltac SRes :=
-  match goal with
-  | [ |- nextinstr _ _ = _ ] => rewrite nextinstr_inv; [auto | auto with ppcgen]
-  | [ |- nextinstr_nf _ _ = _ ] => rewrite nextinstr_nf_inv; [auto | auto with ppcgen]
-  | [ |- Pregmap.get ?x (Pregmap.set ?x _ _) = _ ] => rewrite Pregmap.gss; auto
-  | [ |- Pregmap.set ?x _ _ ?x = _ ] => rewrite Pregmap.gss; auto
-  | [ |- Pregmap.get _ (Pregmap.set _ _ _) = _ ] => rewrite Pregmap.gso; [auto | auto with ppcgen]
-  | [ |- Pregmap.set _ _ _ _ = _ ] => rewrite Pregmap.gso; [auto | auto with ppcgen]
-  end.
-
-Ltac SOther :=
-  match goal with
-  | [ |- nextinstr _ _ = _ ] => rewrite nextinstr_inv; [auto | auto with ppcgen]
-  | [ |- nextinstr_nf _ _ = _ ] => rewrite nextinstr_nf_inv2; [auto | auto with ppcgen]
-  | [ |- Pregmap.get ?x (Pregmap.set ?x _ _) = _ ] => rewrite Pregmap.gss; auto
-  | [ |- Pregmap.set ?x _ _ ?x = _ ] => rewrite Pregmap.gss; auto
-  | [ |- Pregmap.get _ (Pregmap.set _ _ _) = _ ] => rewrite Pregmap.gso; [auto | auto with ppcgen]
-  | [ |- Pregmap.set _ _ _ _ = _ ] => rewrite Pregmap.gso; [auto | auto with ppcgen]
-  end.
-
 Lemma mk_shift_correct:
   forall sinstr ssem r1 r2 k c rs1 m,
   mk_shift sinstr r1 r2 k = OK c ->
   (forall r c rs m,
    exec_instr ge c (sinstr r) rs m = Next (nextinstr_nf (rs#r <- (ssem rs#r rs#ECX))) m) ->
   exists rs2,
-     exec_straight c rs1 m k rs2 m
+     exec_straight ge fn c rs1 m k rs2 m
   /\ rs2#r1 = ssem rs1#r1 rs1#r2
   /\ forall r, nontemp_preg r = true -> r <> r1 -> rs2#r = rs1#r.
 Proof.
@@ -568,8 +184,7 @@ Proof.
 (* fast case *)
   monadInv H.
   econstructor. split. apply exec_straight_one. apply H0. auto. 
-  split. repeat SRes.
-  intros. repeat SOther.
+  split. Simplifs. intros; Simplifs.
 (* xchg case *)
   destruct (ireg_eq r1 ECX); monadInv H. 
   econstructor. split. eapply exec_straight_three.
@@ -577,15 +192,12 @@ Proof.
   apply H0.
   simpl; eauto.
   auto. auto. auto. 
-  split. repeat SRes. repeat rewrite nextinstr_inv; auto with ppcgen. 
-  rewrite Pregmap.gss. decEq. rewrite Pregmap.gso; auto with ppcgen. apply Pregmap.gss.
-  intros. destruct (preg_eq r r2). subst. repeat SRes. repeat SOther.
+  split. Simplifs. f_equal. Simplifs.
+  intros; Simplifs. destruct (preg_eq r r2). subst r. Simplifs. Simplifs.
 (* general case *)
   econstructor. split. eapply exec_straight_two. simpl; eauto. apply H0. 
   auto. auto. 
-  split. repeat SRes. repeat rewrite nextinstr_inv; auto with ppcgen.
-  rewrite Pregmap.gss. decEq. rewrite Pregmap.gso; auto. congruence.
-  intros. repeat SOther.
+  split. Simplifs. f_equal. Simplifs. intros. Simplifs. 
 Qed.
 
 (** Parallel move 2 *)
@@ -594,7 +206,7 @@ Lemma mk_mov2_correct:
   forall src1 dst1 src2 dst2 k rs m,
   dst1 <> dst2 ->
   exists rs',
-     exec_straight (mk_mov2 src1 dst1 src2 dst2 k) rs m k rs' m
+     exec_straight ge fn (mk_mov2 src1 dst1 src2 dst2 k) rs m k rs' m
   /\ rs'#dst1 = rs#src1
   /\ rs'#dst2 = rs#src2
   /\ forall r, r <> PC -> r <> dst1 -> r <> dst2 -> rs'#r = rs#r.
@@ -603,22 +215,22 @@ Proof.
 (* single moves *)
   destruct (ireg_eq src1 dst1). subst.
   econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split. repeat SRes. split. repeat SRes. intros; repeat SOther. 
+  intuition Simplifs.
   destruct (ireg_eq src2 dst2). subst.
   econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split. repeat SRes. split. repeat SRes. intros; repeat SOther. 
+  intuition Simplifs.
 (* xchg *)
   destruct (ireg_eq src2 dst1). destruct (ireg_eq src1 dst2).
   subst. econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split. repeat SRes. split. repeat SRes. intros; repeat SOther.
+  intuition Simplifs.
 (* move 2; move 1 *)
   subst. econstructor; split. eapply exec_straight_two.
   simpl; eauto. simpl; eauto. auto. auto.
-  split. repeat SRes. split. repeat SRes. intros; repeat SOther.
+  intuition Simplifs.
 (* move 1; move 2*)
   subst. econstructor; split. eapply exec_straight_two.
   simpl; eauto. simpl; eauto. auto. auto.
-  split. repeat SRes. split. repeat SRes. intros; repeat SOther.
+  intuition Simplifs.
 Qed.
 
 (** Smart constructor for division *)
@@ -636,7 +248,7 @@ Lemma mk_div_correct:
   dsem rs1#r1 rs1#r2 = Some vq ->
   msem rs1#r1 rs1#r2 = Some vr ->
   exists rs2,
-     exec_straight c rs1 m k rs2 m
+     exec_straight ge fn c rs1 m k rs2 m
   /\ rs2#r1 = vq
   /\ forall r, nontemp_preg r = true -> r <> r1 -> rs2#r = rs1#r.
 Proof.
@@ -647,15 +259,13 @@ Proof.
   rewrite H0.
   change (nextinstr rs1 # ECX <- (rs1 EDX) EAX) with (rs1#EAX). 
   change ((nextinstr rs1 # ECX <- (rs1 EDX)) # EDX <- Vundef ECX) with (rs1#EDX).
-  rewrite H1. rewrite H2. eauto. auto. auto. 
-  split. SRes. 
-  intros. repeat SOther.
+  rewrite H1. rewrite H2. eauto. auto. auto.
+  intuition Simplifs.
 (* r1=EAX r2<>EDX *)
   econstructor. split. eapply exec_straight_one. rewrite H0. 
   replace (rs1 # EDX <- Vundef r2) with (rs1 r2). rewrite H1; rewrite H2. eauto. 
-  symmetry. SOther. auto.
-  split. SRes.
-  intros. repeat SOther. 
+  symmetry. Simplifs. auto. 
+  intuition Simplifs.
 (* r1 <> EAX *)
   monadInv H.
   set (rs2 := nextinstr (rs1#XMM7 <- (rs1#EAX))).
@@ -669,10 +279,10 @@ Proof.
   rewrite H1; rewrite H2. eauto.  
   simpl; eauto. simpl; eauto.
   auto. auto. auto. 
-  split. repeat SRes.
+  split. Simplifs. 
   intros. destruct (preg_eq r EAX). subst.
-  repeat SRes. rewrite D; auto with ppcgen. 
-  repeat SOther. rewrite D; auto with ppcgen. unfold rs2; repeat SOther.
+  Simplifs. rewrite D; auto with asmgen. 
+  Simplifs. rewrite D; auto with asmgen. unfold rs2; Simplifs.
 Qed.
 
 (** Smart constructor for modulus *)
@@ -690,7 +300,7 @@ Lemma mk_mod_correct:
   dsem rs1#r1 rs1#r2 = Some vq ->
   msem rs1#r1 rs1#r2 = Some vr ->
   exists rs2,
-     exec_straight c rs1 m k rs2 m
+     exec_straight ge fn c rs1 m k rs2 m
   /\ rs2#r1 = vr
   /\ forall r, nontemp_preg r = true -> r <> r1 -> rs2#r = rs1#r.
 Proof.
@@ -705,16 +315,14 @@ Proof.
   rewrite H1. rewrite H2. eauto.
   simpl; eauto.
   auto. auto. auto. 
-  split. SRes. 
-  intros. repeat SOther.
+  intuition Simplifs.
 (* r1=EAX r2<>EDX *)
   econstructor. split. eapply exec_straight_two. rewrite H0. 
   replace (rs1 # EDX <- Vundef r2) with (rs1 r2). rewrite H1; rewrite H2. eauto. 
-  symmetry. SOther. 
+  symmetry. Simplifs.
   simpl; eauto. 
-  auto. auto. 
-  split. SRes.
-  intros. repeat SOther. 
+  auto. auto.
+  intuition Simplifs.
 (* r1 <> EAX *)
   monadInv H.
   set (rs2 := nextinstr (rs1#XMM7 <- (rs1#EAX))).
@@ -728,10 +336,10 @@ Proof.
   rewrite H1; rewrite H2. eauto.  
   simpl; eauto. simpl; eauto.
   auto. auto. auto. 
-  split. repeat SRes.
+  split. Simplifs. 
   intros. destruct (preg_eq r EAX). subst.
-  repeat SRes. rewrite D; auto with ppcgen. 
-  repeat SOther. rewrite D; auto with ppcgen. unfold rs2; repeat SOther.
+  Simplifs. rewrite D; auto with asmgen.
+  Simplifs. rewrite D; auto with asmgen. unfold rs2; Simplifs.
 Qed.
 
 Remark divs_mods_exist:
@@ -765,7 +373,7 @@ Lemma mk_shrximm_correct:
   mk_shrximm r1 n k = OK c ->
   Val.shrx (rs1#r1) (Vint n) = Some v ->
   exists rs2,
-     exec_straight c rs1 m k rs2 m
+     exec_straight ge fn c rs1 m k rs2 m
   /\ rs2#r1 = v
   /\ forall r, nontemp_preg r = true -> r <> r1 -> rs2#r = rs1#r.
 Proof.
@@ -781,25 +389,26 @@ Proof.
   set (rs3 := nextinstr (rs2#tmp <- (Vint x'))).
   set (rs4 := nextinstr (if Int.lt x Int.zero then rs3#r1 <- (Vint x') else rs3)).
   set (rs5 := nextinstr_nf (rs4#r1 <- (Val.shr rs4#r1 (Vint n)))).
-  assert (rs3#r1 = Vint x). unfold rs3. SRes. SRes. 
-  assert (rs3#tmp = Vint x'). unfold rs3. SRes. SRes. 
+  assert (rs3#r1 = Vint x). unfold rs3. Simplifs. 
+  assert (rs3#tmp = Vint x'). unfold rs3. Simplifs. 
   exists rs5. split. 
   apply exec_straight_step with rs2 m. simpl. rewrite A. simpl. rewrite Int.and_idem. auto. auto.
   apply exec_straight_step with rs3 m. simpl. 
   change (rs2 r1) with (rs1 r1). rewrite A. simpl. 
   rewrite (Int.add_commut Int.zero tnm1). rewrite Int.add_zero. auto. auto.
   apply exec_straight_step with rs4 m. simpl. 
-  change (rs3 SOF) with (rs2 SOF). unfold rs2. rewrite nextinstr_inv; auto with ppcgen. 
-  unfold compare_ints. rewrite Pregmap.gso; auto with ppcgen. rewrite Pregmap.gss.
+  change (rs3 SOF) with (rs2 SOF). unfold rs2. rewrite nextinstr_inv; auto with asmgen. 
+  unfold compare_ints. rewrite Pregmap.gso; auto with asmgen. rewrite Pregmap.gss.
   unfold Val.cmp. simpl. unfold rs4. destruct (Int.lt x Int.zero); simpl; auto. rewrite H0; auto.
   unfold rs4. destruct (Int.lt x Int.zero); simpl; auto.
   apply exec_straight_one. auto. auto.
-  split. unfold rs5. SRes. SRes. unfold rs4. rewrite nextinstr_inv; auto with ppcgen.
-  destruct (Int.lt x Int.zero). rewrite Pregmap.gss. rewrite A; auto. rewrite A; rewrite H; auto.
-  intros. unfold rs5. repeat SOther. unfold rs4. SOther.
-  transitivity (rs3#r). destruct (Int.lt x Int.zero). SOther. auto. 
-  unfold rs3. repeat SOther. unfold rs2. repeat SOther. 
-  unfold compare_ints. repeat SOther. 
+  split. unfold rs5. Simplifs. unfold rs4. Simplifs.
+  f_equal. destruct (Int.lt x Int.zero).
+  Simplifs. rewrite A. auto. Simplifs. congruence. 
+  intros. unfold rs5; Simplifs. unfold rs4; Simplifs. 
+  transitivity (rs3#r).
+  destruct (Int.lt x Int.zero). Simplifs. auto. 
+  unfold rs3; Simplifs. unfold rs2; Simplifs. unfold compare_ints; Simplifs.
 Qed.
 
 (** Smart constructor for integer conversions *)
@@ -810,18 +419,16 @@ Lemma mk_intconv_correct:
   (forall c rd rs r m,
    exec_instr ge c (mk rd rs) r m = Next (nextinstr (r#rd <- (sem r#rs))) m) ->
   exists rs2,
-     exec_straight c rs1 m k rs2 m
+     exec_straight ge fn c rs1 m k rs2 m
   /\ rs2#rd = sem rs1#rs
   /\ forall r, nontemp_preg r = true -> r <> rd -> rs2#r = rs1#r.
 Proof.
   unfold mk_intconv; intros. destruct (low_ireg rs); monadInv H.
   econstructor. split. apply exec_straight_one. rewrite H0. eauto. auto. 
-  split. repeat SRes.
-  intros. repeat SOther.
+  intuition Simplifs.
   econstructor. split. eapply exec_straight_two. 
-  simpl. eauto. apply H0. auto. auto. 
-  split. repeat SRes. 
-  intros. repeat SOther. 
+  simpl. eauto. apply H0. auto. auto.
+  intuition Simplifs.
 Qed.
 
 (** Smart constructor for small stores *)
@@ -845,15 +452,15 @@ Lemma mk_smallstore_correct:
   (forall c r addr rs m,
    exec_instr ge c (sto addr r) rs m = exec_store ge chunk m addr rs r) ->
   exists rs2,
-     exec_straight c rs1 m1 k rs2 m2
+     exec_straight ge fn c rs1 m1 k rs2 m2
   /\ forall r, nontemp_preg r = true -> rs2#r = rs1#r.
 Proof.
   unfold mk_smallstore; intros. 
   remember (low_ireg r) as low. destruct low.
 (* low reg *)
   monadInv H. econstructor; split. apply exec_straight_one. rewrite H1. 
-  unfold exec_store. rewrite H0. eauto. auto. 
-  intros. SOther.
+  unfold exec_store. rewrite H0. eauto. auto.
+  intros; Simplifs.
 (* high reg *)
    remember (addressing_mentions addr ECX) as mentions. destruct mentions; monadInv H.
 (* ECX is mentioned. *)
@@ -863,7 +470,7 @@ Proof.
   econstructor; split.
   apply exec_straight_three with rs2 m1 rs3 m1. 
   simpl. auto. 
-  simpl. replace (rs2 r) with (rs1 r). auto. symmetry. unfold rs2. repeat SRes. 
+  simpl. replace (rs2 r) with (rs1 r). auto. symmetry. unfold rs2; Simplifs. 
   rewrite H1. unfold exec_store. simpl. rewrite Int.add_zero. 
   change (rs3 EDX) with (rs1 r).
   change (rs3 ECX) with (eval_addrmode ge addr rs1).
@@ -873,7 +480,7 @@ Proof.
   destruct (eval_addrmode ge addr rs1); simpl in H0; try discriminate.
   simpl. rewrite Int.add_zero; auto. 
   auto. auto. auto. 
-  intros. repeat SOther. unfold rs3. repeat SOther. unfold rs2. repeat SOther.
+  intros. Simplifs. unfold rs3; Simplifs. unfold rs2; Simplifs. 
 (* ECX is not mentioned *)
   set (rs2 := nextinstr (rs1#ECX <- (rs1 r))).
   econstructor; split.
@@ -882,9 +489,9 @@ Proof.
   rewrite H1. unfold exec_store. 
   rewrite (addressing_mentions_correct addr ECX rs2 rs1); auto.
   change (rs2 ECX) with (rs1 r). rewrite H0. eauto. 
-  intros. unfold rs2. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gso; auto with ppcgen.
-  auto. auto. 
-  intros. rewrite dec_eq_false. repeat SOther. unfold rs2. repeat SOther. congruence.
+  intros. unfold rs2; Simplifs.
+  auto. auto.
+  intros. rewrite dec_eq_false. Simplifs. unfold rs2; Simplifs. congruence.
 Qed.
 
 (** Accessing slots in the stack frame *)
@@ -894,9 +501,9 @@ Lemma loadind_correct:
   loadind base ofs ty dst k = OK c ->
   Mem.loadv (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) = Some v ->
   exists rs',
-     exec_straight c rs m k rs' m
+     exec_straight ge fn c rs m k rs' m
   /\ rs'#(preg_of dst) = v
-  /\ forall r, important_preg r = true -> r <> preg_of dst -> rs'#r = rs#r.
+  /\ forall r, data_preg r = true -> r <> preg_of dst -> rs'#r = rs#r.
 Proof.
   unfold loadind; intros.
   set (addr := Addrmode (Some base) None (inl (ident * int) ofs)) in *.
@@ -907,16 +514,14 @@ Proof.
   monadInv H.
   rewrite (ireg_of_eq _ _ EQ). econstructor.
   split. apply exec_straight_one. simpl. unfold exec_load. rewrite H1. rewrite H0.
-  eauto. auto. 
-  split. repeat SRes. 
-  intros. rewrite nextinstr_nf_inv1; auto. SOther.
+  eauto. auto.
+  intuition Simplifs.
   (* float *)
   exists (nextinstr_nf (rs#(preg_of dst) <- v)).
   split. destruct (preg_of dst); inv H; apply exec_straight_one; simpl; auto.
   unfold exec_load. rewrite H1; rewrite H0; auto. 
-  unfold exec_load. rewrite H1; rewrite H0; auto. 
-  split. rewrite nextinstr_nf_inv1. SRes. apply preg_of_important.
-  intros. rewrite nextinstr_nf_inv1; auto. SOther.
+  unfold exec_load. rewrite H1; rewrite H0; auto.
+  intuition Simplifs.
 Qed.
 
 Lemma storeind_correct:
@@ -924,8 +529,8 @@ Lemma storeind_correct:
   storeind src base ofs ty k = OK c ->
   Mem.storev (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) (rs#(preg_of src)) = Some m' ->
   exists rs',
-     exec_straight c rs m k rs' m'
-  /\ forall r, important_preg r = true -> r <> ST0 -> rs'#r = rs#r.
+     exec_straight ge fn c rs m k rs' m'
+  /\ forall r, data_preg r = true -> r <> ST0 -> rs'#r = rs#r.
 Proof.
   unfold storeind; intros.
   set (addr := Addrmode (Some base) None (inl (ident * int) ofs)) in *.
@@ -937,7 +542,7 @@ Proof.
   rewrite (ireg_of_eq _ _ EQ) in H0. econstructor.
   split. apply exec_straight_one. simpl. unfold exec_store. rewrite H1. rewrite H0.
   eauto. auto. 
-  intros. apply nextinstr_nf_inv1; auto. 
+  intros; Simplifs.
   (* float *)
   destruct (preg_of src); inv H.
   econstructor; split. apply exec_straight_one.
@@ -945,7 +550,7 @@ Proof.
   intros. apply nextinstr_nf_inv1; auto.
   econstructor; split. apply exec_straight_one.
   simpl. unfold exec_store. rewrite H1; rewrite H0. eauto. auto.
-  intros. rewrite nextinstr_nf_inv1; auto. rewrite dec_eq_true. apply Pregmap.gso; auto.
+  intros. Simplifs. rewrite dec_eq_true. Simplifs. 
 Qed.
 
 (** Translation of addressing modes *)
@@ -1010,7 +615,7 @@ Proof.
   split. auto. 
   split. auto.
   split. auto.
-  intros. repeat SOther. 
+  intros. Simplifs.
 Qed.
 
 Lemma int_signed_eq:
@@ -1139,7 +744,7 @@ Proof.
   split. auto. 
   split. auto.
   split. auto.
-  intros. repeat SOther. 
+  intros. Simplifs.
 Qed.
 
 Definition eval_extcond (xc: extcond) (rs: regset) : option bool :=
@@ -1158,112 +763,6 @@ Definition eval_extcond (xc: extcond) (rs: regset) : option bool :=
       end
   end.
 
-(*******
-
-Definition swap_floats {A: Type} (c: comparison) (n1 n2: A) : A :=
-  match c with
-  | Clt | Cle => n2
-  | Ceq | Cne | Cgt | Cge => n1
-  end.
-
-Lemma testcond_for_float_comparison_correct:
-  forall c v1 v2 rs b,
-  Val.cmpf_bool c v1 v2 = Some b ->
-  eval_extcond (testcond_for_condition (Ccompf c))
-               (nextinstr (compare_floats (swap_floats c v1 v2)
-                                         (swap_floats c v2 v1) rs)) = Some b.
-Proof.
-  intros. destruct v1; destruct v2; simpl in H; inv H.
-  assert (SWP: forall f1 f2, Vfloat (swap_floats c f1 f2) = swap_floats c (Vfloat f1) (Vfloat f2)).
-    destruct c; auto.
-  generalize (compare_floats_spec rs (swap_floats c f f0) (swap_floats c f0 f)).
-  repeat rewrite <- SWP.
-  set (rs' := nextinstr (compare_floats (Vfloat (swap_floats c f f0))
-                                      (Vfloat (swap_floats c f0 f)) rs)).
-  intros [A [B [C D]]].
-  unfold eval_extcond, eval_testcond. rewrite A; rewrite B; rewrite C.
-  destruct c; simpl.
-(* eq *)
-  rewrite Float.cmp_ne_eq.
-  destruct (Float.cmp Ceq f f0). auto.
-  simpl. destruct (Float.cmp Clt f f0 || Float.cmp Cgt f f0); auto.
-(* ne *)
-  rewrite Float.cmp_ne_eq.
-  destruct (Float.cmp Ceq f f0). auto.
-  simpl. destruct (Float.cmp Clt f f0 || Float.cmp Cgt f f0); auto.
-(* lt *)
-  rewrite <- (Float.cmp_swap Cge f f0).
-  rewrite <- (Float.cmp_swap Cne f f0).
-  simpl.
-  rewrite Float.cmp_ne_eq. rewrite Float.cmp_le_lt_eq.
-  caseEq (Float.cmp Clt f f0); intros; simpl.
-  caseEq (Float.cmp Ceq f f0); intros; simpl. 
-  elimtype False. eapply Float.cmp_lt_eq_false; eauto. 
-  auto. 
-  destruct (Float.cmp Ceq f f0); auto.
-(* le *)
-  rewrite <- (Float.cmp_swap Cge f f0). simpl.
-  destruct (Float.cmp Cle f f0); auto.
-(* gt *)
-  rewrite Float.cmp_ne_eq. rewrite Float.cmp_ge_gt_eq. 
-  caseEq (Float.cmp Cgt f f0); intros; simpl.
-  caseEq (Float.cmp Ceq f f0); intros; simpl. 
-  elimtype False. eapply Float.cmp_gt_eq_false; eauto. 
-  auto. 
-  destruct (Float.cmp Ceq f f0); auto.
-(* ge *)
-  destruct (Float.cmp Cge f f0); auto.
-Qed.
-
-Lemma testcond_for_neg_float_comparison_correct:
-  forall c n1 n2 rs,
-  eval_extcond (testcond_for_condition (Cnotcompf c))
-               (nextinstr (compare_floats (Vfloat (swap_floats c n1 n2))
-                                          (Vfloat (swap_floats c n2 n1)) rs)) =
-  Some(negb(Float.cmp c n1 n2)).
-Proof.
-  intros.
-  generalize (compare_floats_spec rs (swap_floats c n1 n2) (swap_floats c n2 n1)).
-  set (rs' := nextinstr (compare_floats (Vfloat (swap_floats c n1 n2))
-                                        (Vfloat (swap_floats c n2 n1)) rs)).
-  intros [A [B [C D]]].
-  unfold eval_extcond, eval_testcond. rewrite A; rewrite B; rewrite C.
-  destruct c; simpl.
-(* eq *)
-  rewrite Float.cmp_ne_eq.
-  caseEq (Float.cmp Ceq n1 n2); intros.
-  auto.
-  simpl. destruct (Float.cmp Clt n1 n2 || Float.cmp Cgt n1 n2); auto.
-(* ne *)
-  rewrite Float.cmp_ne_eq.
-  caseEq (Float.cmp Ceq n1 n2); intros.
-  auto.
-  simpl. destruct (Float.cmp Clt n1 n2 || Float.cmp Cgt n1 n2); auto.
-(* lt *)
-  rewrite <- (Float.cmp_swap Cge n1 n2).
-  rewrite <- (Float.cmp_swap Cne n1 n2).
-  simpl.
-  rewrite Float.cmp_ne_eq. rewrite Float.cmp_le_lt_eq.
-  caseEq (Float.cmp Clt n1 n2); intros; simpl.
-  caseEq (Float.cmp Ceq n1 n2); intros; simpl. 
-  elimtype False. eapply Float.cmp_lt_eq_false; eauto.
-  auto. 
-  destruct (Float.cmp Ceq n1 n2); auto.
-(* le *)
-  rewrite <- (Float.cmp_swap Cge n1 n2). simpl.
-  destruct (Float.cmp Cle n1 n2); auto.
-(* gt *)
-  rewrite Float.cmp_ne_eq. rewrite Float.cmp_ge_gt_eq. 
-  caseEq (Float.cmp Cgt n1 n2); intros; simpl.
-  caseEq (Float.cmp Ceq n1 n2); intros; simpl. 
-  elimtype False. eapply Float.cmp_gt_eq_false; eauto. 
-  auto. 
-  destruct (Float.cmp Ceq n1 n2); auto.
-(* ge *)
-  destruct (Float.cmp Cge n1 n2); auto.
-Qed.
-***************)
-
 Definition swap_floats {A: Type} (c: comparison) (n1 n2: A) : A :=
   match c with
   | Clt | Cle => n2
@@ -1379,15 +878,15 @@ Remark compare_floats_inv:
 Proof.
   intros. 
   assert (DFL: undef_regs (CR ZF :: CR CF :: CR PF :: CR SOF :: nil) rs r = rs r).
-    simpl. repeat SOther.
-  unfold compare_floats; destruct vx; destruct vy; auto. repeat SOther.
+    simpl. Simplifs. 
+  unfold compare_floats; destruct vx; destruct vy; auto. Simplifs. 
 Qed.  
 
 Lemma transl_cond_correct:
   forall cond args k c rs m,
   transl_cond cond args k = OK c ->
   exists rs',
-     exec_straight c rs m k rs' m
+     exec_straight ge fn c rs m k rs' m
   /\ match eval_condition cond (map rs (map preg_of args)) m with
      | None => True
      | Some b => eval_extcond (testcond_for_condition cond) rs' = Some b
@@ -1401,88 +900,87 @@ Proof.
   econstructor. split. apply exec_straight_one. simpl. eauto. auto.
   split. destruct (Val.cmp_bool c0 (rs x) (rs x0)) eqn:?; auto.
   eapply testcond_for_signed_comparison_correct; eauto. 
-  intros. unfold compare_ints. repeat SOther.
+  intros. unfold compare_ints. Simplifs.
 (* compu *)
   simpl. rewrite (ireg_of_eq _ _ EQ). rewrite (ireg_of_eq _ _ EQ1).
   econstructor. split. apply exec_straight_one. simpl. eauto. auto.
   split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (rs x0)) eqn:?; auto.
   eapply testcond_for_unsigned_comparison_correct; eauto. 
-  intros. unfold compare_ints. repeat SOther.
+  intros. unfold compare_ints. Simplifs.
 (* compimm *)
   simpl. rewrite (ireg_of_eq _ _ EQ). destruct (Int.eq_dec i Int.zero).
   econstructor; split. apply exec_straight_one. simpl; eauto. auto. 
   split. destruct (rs x); simpl; auto. subst. rewrite Int.and_idem.
   eapply testcond_for_signed_comparison_correct; eauto. 
-  intros. unfold compare_ints. repeat SOther.
+  intros. unfold compare_ints. Simplifs.
   econstructor; split. apply exec_straight_one. simpl; eauto. auto. 
   split. destruct (Val.cmp_bool c0 (rs x) (Vint i)) eqn:?; auto.
   eapply testcond_for_signed_comparison_correct; eauto. 
-  intros. unfold compare_ints. repeat SOther.
+  intros. unfold compare_ints. Simplifs.
 (* compuimm *)
   simpl. rewrite (ireg_of_eq _ _ EQ).
   econstructor. split. apply exec_straight_one. simpl. eauto. auto.
   split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (Vint i)) eqn:?; auto.
   eapply testcond_for_unsigned_comparison_correct; eauto. 
-  intros. unfold compare_ints. repeat SOther.
+  intros. unfold compare_ints. Simplifs.
 (* compf *)
   simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1).
   exists (nextinstr (compare_floats (swap_floats c0 (rs x) (rs x0)) (swap_floats c0 (rs x0) (rs x)) rs)).
   split. apply exec_straight_one. 
   destruct c0; simpl; auto.
-  unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats_inv; auto with ppcgen. 
+  unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats_inv; auto with asmgen. 
   split. destruct (rs x); destruct (rs x0); simpl; auto.
   repeat rewrite swap_floats_commut. apply testcond_for_float_comparison_correct.
-  intros. SOther. apply compare_floats_inv; auto with ppcgen. 
+  intros. Simplifs. apply compare_floats_inv; auto with asmgen. 
 (* notcompf *)
   simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1).
   exists (nextinstr (compare_floats (swap_floats c0 (rs x) (rs x0)) (swap_floats c0 (rs x0) (rs x)) rs)).
   split. apply exec_straight_one. 
   destruct c0; simpl; auto.
-  unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats_inv; auto with ppcgen. 
+  unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats_inv; auto with asmgen. 
   split. destruct (rs x); destruct (rs x0); simpl; auto.
   repeat rewrite swap_floats_commut. apply testcond_for_neg_float_comparison_correct.
-  intros. SOther. apply compare_floats_inv; auto with ppcgen. 
+  intros. Simplifs. apply compare_floats_inv; auto with asmgen. 
 (* maskzero *)
   simpl. rewrite (ireg_of_eq _ _ EQ).
   econstructor. split. apply exec_straight_one. simpl; eauto. auto.
   split. destruct (rs x); simpl; auto. 
   generalize (compare_ints_spec rs (Vint (Int.and i0 i)) Vzero m).
   intros [A B]. rewrite A. unfold Val.cmpu; simpl. destruct (Int.eq (Int.and i0 i) Int.zero); auto.
-  intros. unfold compare_ints. repeat SOther.
+  intros. unfold compare_ints. Simplifs.
 (* masknotzero *)
   simpl. rewrite (ireg_of_eq _ _ EQ).
   econstructor. split. apply exec_straight_one. simpl; eauto. auto.
   split. destruct (rs x); simpl; auto. 
   generalize (compare_ints_spec rs (Vint (Int.and i0 i)) Vzero m).
   intros [A B]. rewrite A. unfold Val.cmpu; simpl. destruct (Int.eq (Int.and i0 i) Int.zero); auto.
-  intros. unfold compare_ints. repeat SOther.
+  intros. unfold compare_ints. Simplifs.
 Qed.
 
 Remark eval_testcond_nextinstr:
   forall c rs, eval_testcond c (nextinstr rs) = eval_testcond c rs.
 Proof.
-  intros. unfold eval_testcond. repeat rewrite nextinstr_inv; auto with ppcgen.
+  intros. unfold eval_testcond. repeat rewrite nextinstr_inv; auto with asmgen.
 Qed.
 
 Remark eval_testcond_set_ireg:
   forall c rs r v, eval_testcond c (rs#(IR r) <- v) = eval_testcond c rs.
 Proof.
-  intros. unfold eval_testcond. repeat rewrite Pregmap.gso; auto with ppcgen.
+  intros. unfold eval_testcond. repeat rewrite Pregmap.gso; auto with asmgen.
 Qed.
 
 Lemma mk_setcc_correct:
   forall cond rd k rs1 m,
   exists rs2,
-  exec_straight (mk_setcc cond rd k) rs1 m k rs2 m
+  exec_straight ge fn (mk_setcc cond rd k) rs1 m k rs2 m
   /\ rs2#rd = Val.of_optbool(eval_extcond cond rs1)
   /\ forall r, nontemp_preg r = true -> r <> rd -> rs2#r = rs1#r.
 Proof.
   intros. destruct cond; simpl in *.
 (* base *)
   econstructor; split.
-  apply exec_straight_one. simpl; eauto. auto. 
-  split. SRes. SRes. 
-  intros; repeat SOther.
+  apply exec_straight_one. simpl; eauto. auto.
+  intuition Simplifs.
 (* or *)
   assert (Val.of_optbool
     match eval_testcond c1 rs1 with
@@ -1506,16 +1004,15 @@ Proof.
   simpl. rewrite eval_testcond_nextinstr. repeat rewrite eval_testcond_set_ireg. eauto.
   simpl; eauto.
   auto. auto. auto.
-  split. SRes. 
-  intros. repeat SOther.
+  intuition Simplifs.
   econstructor; split.
   eapply exec_straight_three.
   simpl; eauto.
   simpl. rewrite eval_testcond_nextinstr. repeat rewrite eval_testcond_set_ireg. eauto. 
   simpl. eauto. 
   auto. auto. auto.
-  split. repeat SRes. rewrite Val.or_commut. decEq; repeat SRes. 
-  intros. repeat SOther.
+  split. Simplifs. rewrite Val.or_commut. f_equal; Simplifs. 
+  intros. Simplifs.
 (* and *)
   assert (Val.of_optbool
     match eval_testcond c1 rs1 with
@@ -1539,16 +1036,15 @@ Proof.
   simpl. rewrite eval_testcond_nextinstr. repeat rewrite eval_testcond_set_ireg. eauto.
   simpl; eauto.
   auto. auto. auto.
-  split. SRes. 
-  intros. repeat SOther.
+  intuition Simplifs.
   econstructor; split.
   eapply exec_straight_three.
   simpl; eauto.
   simpl. rewrite eval_testcond_nextinstr. repeat rewrite eval_testcond_set_ireg. eauto. 
   simpl. eauto. 
   auto. auto. auto.
-  split. repeat SRes. rewrite Val.and_commut. decEq; repeat SRes. 
-  intros. repeat SOther.
+  split. Simplifs. rewrite Val.and_commut. f_equal; Simplifs. 
+  intros. Simplifs.
 Qed.
 
 (** Translation of arithmetic operations. *)
@@ -1567,33 +1063,32 @@ Ltac ArgsInv :=
 Ltac TranslOp :=
   econstructor; split;
   [ apply exec_straight_one; [ simpl; eauto | auto ] 
-  | split; [ repeat SRes | intros; repeat SOther ]].
-
+  | split; [ Simplifs | intros; Simplifs ]].
 
 Lemma transl_op_correct:
   forall op args res k c (rs: regset) m v,
   transl_op op args res k = OK c ->
   eval_operation ge (rs#ESP) op (map rs (map preg_of args)) m = Some v ->
   exists rs',
-     exec_straight c rs m k rs' m
+     exec_straight ge fn c rs m k rs' m
   /\ Val.lessdef v rs'#(preg_of res)
   /\ forall r, 
-     match op with Omove => important_preg r = true /\ r <> ST0 | _ => nontemp_preg r = true end ->
+     match op with Omove => data_preg r = true /\ r <> ST0 | _ => nontemp_preg r = true end ->
      r <> preg_of res -> rs' r = rs r.
 Proof.
   intros until v; intros TR EV.
   assert (SAME:
   (exists rs',
-     exec_straight c rs m k rs' m
+     exec_straight ge fn c rs m k rs' m
   /\ rs'#(preg_of res) = v
   /\ forall r, 
-     match op with Omove => important_preg r = true /\ r <> ST0 | _ => nontemp_preg r = true end ->
+     match op with Omove => data_preg r = true /\ r <> ST0 | _ => nontemp_preg r = true end ->
      r <> preg_of res -> rs' r = rs r) ->
   exists rs',
-     exec_straight c rs m k rs' m
+     exec_straight ge fn c rs m k rs' m
   /\ Val.lessdef v rs'#(preg_of res)
   /\ forall r, 
-     match op with Omove => important_preg r = true /\ r <> ST0 | _ => nontemp_preg r = true end ->
+     match op with Omove => data_preg r = true /\ r <> ST0 | _ => nontemp_preg r = true end ->
      r <> preg_of res -> rs' r = rs r).
   intros [rs' [A [B C]]]. subst v. exists rs'; auto. 
 
@@ -1643,7 +1138,7 @@ Proof.
   apply SAME. eapply mk_shift_correct; eauto.
 (* lea *)
   exploit transl_addressing_mode_correct; eauto. intros EA.
-  TranslOp. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss; auto.
+  TranslOp. rewrite nextinstr_inv; auto with asmgen. rewrite Pregmap.gss; auto.
 (* intoffloat *)
   apply SAME. TranslOp. rewrite H0; auto.
 (* floatofint *)
@@ -1667,7 +1162,7 @@ Lemma transl_load_correct:
   eval_addressing ge (rs#ESP) addr (map rs (map preg_of args)) = Some a ->
   Mem.loadv chunk m a = Some v ->
   exists rs',
-     exec_straight c rs m k rs' m
+     exec_straight ge fn c rs m k rs' m
   /\ rs'#(preg_of dest) = v
   /\ forall r, nontemp_preg r = true -> r <> preg_of dest -> rs'#r = rs#r.
 Proof.
@@ -1679,15 +1174,15 @@ Proof.
     unfold exec_load. rewrite EA'. rewrite H1. auto.
   assert (rs2 PC = Val.add (rs PC) Vone).
     transitivity (Val.add ((rs#(preg_of dest) <- v) PC) Vone).
-    auto. decEq. apply Pregmap.gso; auto with ppcgen.
+    auto. decEq. apply Pregmap.gso; auto with asmgen.
   exists rs2. split. 
   destruct chunk; ArgsInv; apply exec_straight_one; auto.
   (* Mfloat64 -> Mfloat64al32 *)
   rewrite <- H. simpl. unfold exec_load. rewrite H1.
   destruct (eval_addrmode ge x rs); simpl in *; try discriminate.
   erewrite Mem.load_float64al32; eauto. 
-  split. unfold rs2. rewrite nextinstr_nf_inv1. SRes. apply preg_of_important.
-  intros. unfold rs2. repeat SOther. 
+  split. unfold rs2. rewrite nextinstr_nf_inv1. Simplifs. apply preg_of_data.
+  intros. unfold rs2. Simplifs. 
 Qed.
 
 Lemma transl_store_correct:
@@ -1696,7 +1191,7 @@ Lemma transl_store_correct:
   eval_addressing ge (rs#ESP) addr (map rs (map preg_of args)) = Some a ->
   Mem.storev chunk m a (rs (preg_of src)) = Some m' ->
   exists rs',
-     exec_straight c rs m k rs' m'
+     exec_straight ge fn c rs m k rs' m'
   /\ forall r, nontemp_preg r = true -> rs'#r = rs#r.
 Proof.
   unfold transl_store; intros. monadInv H. 
@@ -1717,28 +1212,29 @@ Proof.
   rewrite H1. eauto.
   destruct (eval_addrmode ge x rs); simpl; auto. rewrite Mem.store_signed_unsigned_16; auto.
   auto.
-  intros. SOther.
+  intros. Simplifs.
 (* int16unsigned *)
   econstructor; split.
   apply exec_straight_one. simpl. unfold exec_store. rewrite H1. eauto. auto.
-  intros. SOther.
+  intros. Simplifs.
 (* int32 *)
   econstructor; split.
   apply exec_straight_one. simpl. unfold exec_store. rewrite H1. eauto. auto.
-  intros. SOther.
+  intros. Simplifs.
 (* float32 *)
   econstructor; split.
   apply exec_straight_one. simpl. unfold exec_store. rewrite H1. eauto. auto.
-  intros. SOther.
+  intros. Simplifs.
 (* float64 *)
   econstructor; split.
   apply exec_straight_one. simpl. unfold exec_store. erewrite Mem.storev_float64al32; eauto. auto.
-  intros. SOther.
+  intros. Simplifs.
 (* float64al32 *)
   econstructor; split.
   apply exec_straight_one. simpl. unfold exec_store. rewrite H1. eauto. auto.
-  intros. SOther.
+  intros. Simplifs.
 Qed.
 
-End STRAIGHTLINE.
+End CONSTRUCTORS.
+
 
diff --git a/ia32/Asmgenretaddr.v b/ia32/Asmgenretaddr.v
deleted file mode 100644
index 29d2ba0..0000000
--- a/ia32/Asmgenretaddr.v
+++ /dev/null
@@ -1,259 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Predictor for return addresses in generated IA32 code.
-
-    The [return_address_offset] predicate defined here is used in the
-    semantics for Mach (module [Machsem]) to determine the
-    return addresses that are stored in activation records. *)
-
-Require Import Coqlib.
-Require Import AST.
-Require Import Errors.
-Require Import Integers.
-Require Import Floats.
-Require Import Op.
-Require Import Locations.
-Require Import Mach.
-Require Import Asm.
-Require Import Asmgen.
-
-(** The ``code tail'' of an instruction list [c] is the list of instructions
-  starting at PC [pos]. *)
-
-Inductive code_tail: Z -> code -> code -> Prop :=
-  | code_tail_0: forall c,
-      code_tail 0 c c
-  | code_tail_S: forall pos i c1 c2,
-      code_tail pos c1 c2 ->
-      code_tail (pos + 1) (i :: c1) c2.
-
-Lemma code_tail_pos:
-  forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0.
-Proof.
-  induction 1. omega. omega.
-Qed.
-
-(** Consider a Mach function [f] and a sequence [c] of Mach instructions
-  representing the Mach code that remains to be executed after a
-  function call returns.  The predicate [return_address_offset f c ofs]
-  holds if [ofs] is the integer offset of the PPC instruction
-  following the call in the Asm code obtained by translating the
-  code of [f]. Graphically:
-<<
-     Mach function f    |--------- Mcall ---------|
-         Mach code c    |                |--------|
-                        |                 \        \
-                        |                  \        \
-                        |                   \        \
-     Asm code           |                    |--------|
-     Asm function       |------------- Pcall ---------|
-
-                        <-------- ofs ------->
->>
-*)
-
-Inductive return_address_offset: Mach.function -> Mach.code -> int -> Prop :=
-  | return_address_offset_intro:
-      forall f c ofs,
-      (forall tf tc,
-       transf_function f = OK tf ->
-       transl_code f c false = OK tc ->
-       code_tail ofs tf tc) ->
-      return_address_offset f c (Int.repr ofs).
-
-(** We now show that such an offset always exists if the Mach code [c]
-  is a suffix of [f.(fn_code)].  This holds because the translation
-  from Mach to PPC is compositional: each Mach instruction becomes
-  zero, one or several PPC instructions, but the order of instructions
-  is preserved. *)
-
-Lemma is_tail_code_tail:
-  forall c1 c2, is_tail c1 c2 -> exists ofs, code_tail ofs c2 c1.
-Proof.
-  induction 1. exists 0; constructor.
-  destruct IHis_tail as [ofs CT]. exists (ofs + 1); constructor; auto.
-Qed.
-
-Hint Resolve is_tail_refl: ppcretaddr.
-
-Ltac IsTail :=
-  eauto with ppcretaddr;
-  match goal with
-  | [ |- is_tail _ (_ :: _) ] => constructor; IsTail
-  | [ H: Error _ = OK _ |- _ ] => discriminate
-  | [ H: OK _ = OK _ |- _ ] => inv H; IsTail
-  | [ H: bind _ _ = OK _ |- _ ] => monadInv H; IsTail
-  | [ H: (if ?x then _ else _) = OK _ |- _ ] => destruct x; IsTail
-  | [ H: match ?x with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct x; IsTail
-  | _ => idtac
-  end.
-
-Lemma mk_mov_tail:
-  forall rd rs k c, mk_mov rd rs k = OK c -> is_tail k c.
-Proof.
-  unfold mk_mov; intros. destruct rd; IsTail; destruct rs; IsTail.
-Qed.
-
-Lemma mk_shift_tail:
-  forall si r1 r2 k c, mk_shift si r1 r2 k = OK c -> is_tail k c.
-Proof.
-  unfold mk_shift; intros; IsTail.
-Qed.
-
-Lemma mk_mov2_tail:
-  forall r1 r2 r3 r4 k, is_tail k (mk_mov2 r1 r2 r3 r4 k).
-Proof.
-  unfold mk_mov2; intros.
-  destruct (ireg_eq r1 r2). IsTail.
-  destruct (ireg_eq r3 r4). IsTail.
-  destruct (ireg_eq r3 r2); IsTail.
-  destruct (ireg_eq r1 r4); IsTail.
-Qed.
-
-Lemma mk_div_tail:
-  forall di r1 r2 k c, mk_div di r1 r2 k = OK c -> is_tail k c.
-Proof.
-  unfold mk_div; intros; IsTail.
-  eapply is_tail_trans. 2: eapply mk_mov2_tail. IsTail.
-Qed.
-
-Lemma mk_mod_tail:
-  forall di r1 r2 k c, mk_mod di r1 r2 k = OK c -> is_tail k c.
-Proof.
-  unfold mk_mod; intros; IsTail.
-  eapply is_tail_trans. 2: eapply mk_mov2_tail. IsTail.
-Qed.
-
-Lemma mk_shrximm_tail:
-  forall r n k c, mk_shrximm r n k = OK c -> is_tail k c.
-Proof.
-  unfold mk_shrximm; intros; IsTail.
-Qed.
-
-Lemma mk_intconv_tail:
-  forall mk rd rs k c, mk_intconv mk rd rs k = OK c -> is_tail k c.
-Proof.
-  unfold mk_intconv; intros; IsTail.
-Qed.
-
-Lemma mk_smallstore_tail:
-  forall sto addr rs k c, mk_smallstore sto addr rs k = OK c -> is_tail k c.
-Proof.
-  unfold mk_smallstore; intros; IsTail.
-Qed.
-
-Lemma loadind_tail:
-  forall base ofs ty dst k c, loadind base ofs ty dst k = OK c -> is_tail k c.
-Proof.
-  unfold loadind; intros. destruct ty; IsTail. destruct (preg_of dst); IsTail.
-Qed.
-
-Lemma storeind_tail:
-  forall src base ofs ty k c, storeind src base ofs ty k = OK c -> is_tail k c.
-Proof.
-  unfold storeind; intros. destruct ty; IsTail. destruct (preg_of src); IsTail.
-Qed.
-
-Lemma mk_setcc_tail:
-  forall cond rd k, is_tail k (mk_setcc cond rd k).
-Proof.
-  unfold mk_setcc; intros. destruct cond.
-  IsTail.
-  destruct (ireg_eq rd EDX); IsTail.
-  destruct (ireg_eq rd EDX); IsTail.
-Qed.
-
-Lemma mk_jcc_tail:
-  forall cond lbl k, is_tail k (mk_jcc cond lbl k).
-Proof.
-  unfold mk_jcc; intros. destruct cond; IsTail.
-Qed.
-
-Hint Resolve mk_mov_tail mk_shift_tail mk_div_tail mk_mod_tail mk_shrximm_tail
-             mk_intconv_tail mk_smallstore_tail loadind_tail storeind_tail
-             mk_setcc_tail mk_jcc_tail : ppcretaddr.
-
-Lemma transl_cond_tail:
-  forall cond args k c, transl_cond cond args k = OK c -> is_tail k c.
-Proof.
-  unfold transl_cond; intros. destruct cond; IsTail; destruct (Int.eq_dec i Int.zero); IsTail.
-Qed.
-
-Lemma transl_op_tail:
-  forall op args res k c, transl_op op args res k = OK c -> is_tail k c.
-Proof.
-  unfold transl_op; intros. destruct op; IsTail. 
-  eapply is_tail_trans. 2: eapply transl_cond_tail; eauto. IsTail.
-Qed.
-
-Lemma transl_load_tail:
-  forall chunk addr args dest k c, transl_load chunk addr args dest k = OK c -> is_tail k c.
-Proof.
-  unfold transl_load; intros. IsTail. destruct chunk; IsTail. 
-Qed.
-
-Lemma transl_store_tail:
-  forall chunk addr args src k c, transl_store chunk addr args src k = OK c -> is_tail k c.
-Proof.
-  unfold transl_store; intros. IsTail. destruct chunk; IsTail. 
-Qed.
-
-Lemma transl_instr_tail:
-  forall f i ep k c, transl_instr f i ep k = OK c -> is_tail k c.
-Proof.
-  unfold transl_instr; intros. destruct i; IsTail.
-  eapply is_tail_trans; eapply loadind_tail; eauto.
-  eapply transl_op_tail; eauto.
-  eapply transl_load_tail; eauto.
-  eapply transl_store_tail; eauto.
-  destruct s0; IsTail.
-  destruct s0; IsTail.
-  eapply is_tail_trans. 2: eapply transl_cond_tail; eauto. IsTail.
-Qed.
-
-Lemma transl_code_tail: 
-  forall f c1 c2, is_tail c1 c2 ->
-  forall tc2 ep2, transl_code f c2 ep2 = OK tc2 ->
-  exists tc1, exists ep1, transl_code f c1 ep1 = OK tc1 /\ is_tail tc1 tc2.
-Proof.
-  induction 1; simpl; intros.
-  exists tc2; exists ep2; split; auto with coqlib.
-  monadInv H0. exploit IHis_tail; eauto. intros [tc1 [ep1 [A B]]].
-  exists tc1; exists ep1; split. auto. 
-  apply is_tail_trans with x. auto. eapply transl_instr_tail; eauto.
-Qed.
-
-Lemma return_address_exists:
-  forall f sg ros c, is_tail (Mcall sg ros :: c) f.(fn_code) ->
-  exists ra, return_address_offset f c ra.
-Proof.
-  intros.
-  caseEq (transf_function f). intros tf TF.
-  assert (exists tc1, transl_code f (fn_code f) true = OK tc1 /\ is_tail tc1 tf).
-    monadInv TF.
-    destruct (zlt (list_length_z x) Int.max_unsigned); monadInv EQ0.
-    econstructor; eauto with coqlib.
-  destruct H0 as [tc2 [A B]].
-  exploit transl_code_tail; eauto. intros [tc1 [ep [C D]]].
-Opaque transl_instr.
-  monadInv C.
-  assert (is_tail x tf).
-    apply is_tail_trans with tc2; auto.
-    apply is_tail_trans with tc1; auto.
-    eapply transl_instr_tail; eauto.
-  exploit is_tail_code_tail. eexact H0. intros [ofs C].
-  exists (Int.repr ofs). constructor; intros. congruence. 
-  intros. exists (Int.repr 0). constructor; intros; congruence.
-Qed.
-
-