Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3

4 files changed, 242 insertions, 555 deletions

diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v
index 024c9a17..683530d4 100644
--- a/aarch64/Asmgen.v
+++ b/aarch64/Asmgen.v
@@ -969,8 +969,8 @@ Definition transl_addressing (sz: Z) (addr: Op.addressing) (args: list mreg)
 (** Translation of loads and stores *)
 
 Definition transl_load (trap: trapping_mode)
-                       (chunk: memory_chunk) (addr: Op.addressing)
-                       (args: list mreg) (dst: mreg) (k: code) : res code :=
+           (chunk: memory_chunk) (addr: Op.addressing)
+           (args: list mreg) (dst: mreg) (k: code) : res code :=
   match trap with
   | NOTRAP => Error (msg "Asmgen.transl_load non-trapping loads unsupported on aarch64")
   | TRAP =>
@@ -1061,13 +1061,8 @@ Definition storeptr (src: ireg) (base: iregsp) (ofs: ptrofs) (k: code) :=
 (** Function epilogue *)
 
 Definition make_epilogue (f: Mach.function) (k: code) :=
-  (* FIXME
-     Cannot be used because memcpy destroys X30;
-     issue being discussed with X. Leroy *)
-  (* if is_leaf_function f
-  then Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k
-  else*) loadptr XSP f.(fn_retaddr_ofs) RA
-         (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k).
+  loadptr XSP f.(fn_retaddr_ofs) RA
+    (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k).
   
 (** Translation of a Mach instruction. *)
 
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index df88043f..7dfe6153 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -337,12 +337,7 @@ Qed.
 Remark make_epilogue_label:
   forall f k, tail_nolabel k (make_epilogue f k).
 Proof.
-  unfold make_epilogue; intros.
-  (* FIXME destruct is_leaf_function.
-  { TailNoLabel. } *)
-  eapply tail_nolabel_trans.
-  apply loadptr_label.
-  TailNoLabel.
+  unfold make_epilogue; intros. eapply tail_nolabel_trans. apply loadptr_label. TailNoLabel.
 Qed.
 
 Lemma transl_instr_label:
@@ -477,8 +472,7 @@ Inductive match_states: Mach.state -> Asm.state -> Prop :=
         (MEXT: Mem.extends m m')
         (AT: transl_code_at_pc ge (rs PC) fb f c ep tf tc)
         (AG: agree ms sp rs)
-        (DXP: ep = true -> rs#X29 = parent_sp s)
-        (LEAF: is_leaf_function f = true -> rs#RA = parent_ra s),
+        (DXP: ep = true -> rs#X29 = parent_sp s),
       match_states (Mach.State s fb sp c ms m)
                    (Asm.State rs m')
   | match_states_call:
@@ -509,17 +503,16 @@ Lemma exec_straight_steps:
    exists rs2,
        exec_straight tge tf c rs1 m1' k rs2 m2'
     /\ agree ms2 sp rs2
-    /\ (it1_is_parent ep i = true -> rs2#X29 = parent_sp s)
-    /\ (is_leaf_function f = true -> rs2#RA = parent_ra s)) ->
+    /\ (it1_is_parent ep i = true -> rs2#X29 = parent_sp s)) ->
   exists st',
   plus step tge (State rs1 m1') E0 st' /\
   match_states (Mach.State s fb sp c ms2 m2) st'.
 Proof.
   intros. inversion H2. subst. monadInv H7.
-  exploit H3; eauto. intros [rs2 [A [B [C D]]]].
+  exploit H3; eauto. intros [rs2 [A [B C]]].
   exists (State rs2 m2'); split.
-  - eapply exec_straight_exec; eauto.
-  - econstructor; eauto. eapply exec_straight_at; eauto.
+  eapply exec_straight_exec; eauto.
+  econstructor; eauto. eapply exec_straight_at; eauto.
 Qed.
 
 Lemma exec_straight_steps_goto:
@@ -534,14 +527,13 @@ Lemma exec_straight_steps_goto:
    exists jmp, exists k', exists rs2,
        exec_straight tge tf c rs1 m1' (jmp :: k') rs2 m2'
     /\ agree ms2 sp rs2
-    /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2'
-    /\ (is_leaf_function f = true -> rs2#RA = parent_ra s)) ->
+    /\ 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 (Mach.State s fb sp c' ms2 m2) st'.
 Proof.
   intros. inversion H3. subst. monadInv H9.
-  exploit H5; eauto. intros [jmp [k' [rs2 [A [B [C D]]]]]].
+  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.
   exploit exec_straight_steps_2; eauto.
@@ -558,7 +550,6 @@ Proof.
   econstructor; eauto.
   apply agree_exten with rs2; auto with asmgen.
   congruence.
-  rewrite OTH by congruence; auto.
 Qed.
 
 Lemma exec_straight_opt_steps_goto:
@@ -573,14 +564,13 @@ Lemma exec_straight_opt_steps_goto:
    exists jmp, exists k', exists rs2,
        exec_straight_opt tge tf c rs1 m1' (jmp :: k') rs2 m2'
     /\ agree ms2 sp rs2
-    /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2'
-    /\ (is_leaf_function f = true -> rs2#RA = parent_ra s)) ->
+    /\ 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 (Mach.State s fb sp c' ms2 m2) st'.
 Proof.
   intros. inversion H3. subst. monadInv H9.
-  exploit H5; eauto. intros [jmp [k' [rs2 [A [B [C D]]]]]].
+  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.
   inv A.
@@ -593,7 +583,6 @@ Proof.
   econstructor; eauto.
   apply agree_exten with rs2; auto with asmgen.
   congruence.
-  rewrite OTH by congruence; auto.
 - exploit exec_straight_steps_2; eauto.
   intros [ofs' [PC2 CT2]].
   exploit find_label_goto_label; eauto.
@@ -608,7 +597,6 @@ Proof.
   econstructor; eauto.
   apply agree_exten with rs2; auto with asmgen.
   congruence.
-  rewrite OTH by congruence; auto.
 Qed.
 
 (** We need to show that, in the simulation diagram, we cannot
@@ -641,7 +629,7 @@ Qed.
 
 Theorem step_simulation:
   forall S1 t S2, Mach.step return_address_offset ge S1 t S2 ->
-  forall S1' (MS: match_states S1 S1')  (WF: wf_state ge S1),
+  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.
@@ -650,20 +638,17 @@ Proof.
 - (* Mlabel *)
   left; eapply exec_straight_steps; eauto; intros.
   monadInv TR. econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split. { apply agree_nextinstr; auto. }
-  split. { simpl; congruence. }
-  rewrite nextinstr_inv by congruence; assumption.
+  split. apply agree_nextinstr; auto. simpl; congruence.
 
 - (* 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 TR.
-  exploit loadind_correct; eauto with asmgen. intros [rs' [P [Q [R S]]]].
+  exploit loadind_correct; eauto with asmgen. intros [rs' [P [Q R]]].
   exists rs'; split. eauto.
-  split. { eapply agree_set_mreg; eauto with asmgen. congruence. }
-  split. { simpl; congruence. }
-  rewrite S. assumption.
+  split. eapply agree_set_mreg; eauto with asmgen. congruence.
+  simpl; congruence.
 
 - (* Msetstack *)
   unfold store_stack in H.
@@ -671,12 +656,10 @@ Proof.
   exploit Mem.storev_extends; eauto. intros [m2' [A B]].
   left; eapply exec_straight_steps; eauto.
   rewrite (sp_val _ _ _ AG) in A. intros. simpl in TR.
-  exploit storeind_correct; eauto with asmgen. intros [rs' [P [Q R]]].
+  exploit storeind_correct; eauto with asmgen. intros [rs' [P Q]].
   exists rs'; split. eauto.
   split. eapply agree_undef_regs; eauto with asmgen.
-  simpl; intros.
-  split. rewrite Q; auto with asmgen.
-  rewrite R. assumption.
+  simpl; intros. rewrite Q; auto with asmgen.
 
 - (* Mgetparam *)
   assert (f0 = f) by congruence; subst f0.
@@ -692,45 +675,39 @@ Opaque loadind.
 (* X30 contains parent *)
   exploit loadind_correct. eexact EQ.
   instantiate (2 := rs0). simpl; rewrite DXP; eauto. simpl; congruence.
-  intros [rs1 [P [Q [R S]]]].
+  intros [rs1 [P [Q R]]].
   exists rs1; split. eauto.
   split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen.
-  simpl; split; intros.
-  { rewrite R; auto with asmgen.
-    apply preg_of_not_X29; auto.
-  }
-  { rewrite S; auto. }
-    
+  simpl; intros. rewrite R; auto with asmgen.
+  apply preg_of_not_X29; auto.
 (* X30 does not contain parent *)
   exploit loadptr_correct. eexact A. simpl; congruence. intros [rs1 [P [Q R]]].
   exploit loadind_correct. eexact EQ. instantiate (2 := rs1). simpl; rewrite Q. eauto. simpl; congruence.
-  intros [rs2 [S [T [U V]]]].
+  intros [rs2 [S [T U]]].
   exists rs2; split. eapply exec_straight_trans; eauto.
   split. eapply agree_set_mreg. eapply agree_set_mreg. eauto. eauto.
   instantiate (1 := rs1#X29 <- (rs2#X29)). intros.
   rewrite Pregmap.gso; auto with asmgen.
   congruence.
   intros. unfold Pregmap.set. destruct (PregEq.eq r' X29). congruence. auto with asmgen.
-  split; simpl; intros. rewrite U; auto with asmgen.
+  simpl; intros. rewrite U; auto with asmgen.
   apply preg_of_not_X29; auto.
-  rewrite V. rewrite R by congruence. auto.
-  
+
 - (* Mop *)
   assert (eval_operation tge sp op (map 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 TR.
-  exploit transl_op_correct; eauto. intros [rs2 [P [Q [R S]]]].
+  exploit transl_op_correct; eauto. intros [rs2 [P [Q R]]].
   exists rs2; split. eauto. split.
   apply agree_set_undef_mreg with rs0; auto. 
   apply Val.lessdef_trans with v'; auto.
-  split; simpl; intros. InvBooleans. 
+  simpl; intros. InvBooleans. 
   rewrite R; auto. apply preg_of_not_X29; auto.
 Local Transparent destroyed_by_op.
   destruct op; try exact I; simpl; congruence.
-  rewrite S.
-  auto.
+
 - (* Mload *)
   destruct trap.
   {
@@ -740,16 +717,14 @@ Local Transparent destroyed_by_op.
   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 TR.
-  exploit transl_load_correct; eauto. intros [rs2 [P [Q [R S]]]].
+  exploit transl_load_correct; eauto. intros [rs2 [P [Q R]]].
   exists rs2; split. eauto.
   split. eapply agree_set_undef_mreg; eauto. congruence.
-  split. simpl; congruence.
-  rewrite S. assumption.
+  simpl; congruence.
   }
-  
   (* Mload notrap1 *)
   inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate.
-
+  
 - (* Mload notrap *)
   inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate.
 
@@ -764,11 +739,10 @@ Local Transparent destroyed_by_op.
   assert (Val.lessdef (rs src) (rs0 (preg_of src))) by (eapply preg_val; eauto).
   exploit Mem.storev_extends; eauto. intros [m2' [C D]].
   left; eapply exec_straight_steps; eauto.
-  intros. simpl in TR. exploit transl_store_correct; eauto. intros [rs2 [P [Q R]]].
+  intros. simpl in TR. exploit transl_store_correct; eauto. intros [rs2 [P Q]].
   exists rs2; split. eauto.
   split. eapply agree_undef_regs; eauto with asmgen.
-  split. simpl; congruence.
-  rewrite R. assumption.
+  simpl; congruence.
 
 - (* Mcall *)
   assert (f0 = f) by congruence.  subst f0.
@@ -880,18 +854,6 @@ Local Transparent destroyed_by_op.
   simpl. rewrite undef_regs_other_2; auto. Simpl.
   congruence.
 
-  Simpl.
-  rewrite set_res_other by trivial.
-  rewrite undef_regs_other.
-  assumption.
-  intro.
-  rewrite in_map_iff.
-  intros (x0 & PREG & IN).
-  subst r'.
-  intro.
-  apply (preg_of_not_RA x0).
-  congruence.
-  
 - (* Mgoto *)
   assert (f0 = f) by congruence. subst f0.
   inv AT. monadInv H4.
@@ -905,33 +867,25 @@ Local Transparent destroyed_by_op.
   eapply agree_exten; eauto with asmgen.
   congruence.
 
-  rewrite INV by congruence.
-  assumption.
-  
 - (* Mcond true *)
   assert (f0 = f) by congruence. subst f0.
   exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
   left; eapply exec_straight_opt_steps_goto; eauto.
   intros. simpl in TR.
-  exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C & D).
+  exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C).
   exists jmp; exists k; exists rs'.
   split. eexact A. 
   split. apply agree_exten with rs0; auto with asmgen.
-  split.
-  exact B.
-  rewrite D. exact LEAF.
+  exact B. 
 
 - (* Mcond false *)
   exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
   left; eapply exec_straight_steps; eauto. intros. simpl in TR.
-  exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C & D).
+  exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C).
   econstructor; split.
   eapply exec_straight_opt_right. eexact A. apply exec_straight_one. eexact B. auto.
   split. apply agree_exten with rs0; auto. intros. Simpl.
-  split.
   simpl; congruence.
-  Simpl. rewrite D.
-  exact LEAF.
 
 - (* Mjumptable *)
   assert (f0 = f) by congruence. subst f0.
@@ -953,10 +907,6 @@ Local Transparent destroyed_by_op.
   simpl. intros. rewrite C; auto with asmgen. Simpl.
   congruence.
 
-  rewrite C by congruence.
-  repeat rewrite Pregmap.gso by congruence.
-  assumption.
-  
 - (* Mreturn *)
   assert (f0 = f) by congruence. subst f0.
   inversion AT; subst. simpl in H6; monadInv H6.
@@ -999,7 +949,7 @@ Local Transparent destroyed_by_op.
     simpl preg_of_iregsp. change (rs2 X30) with (rs0 X30). rewrite ATLR. 
     change (rs2 X2) with sp. eexact P. 
     simpl; congruence. congruence.
-  intros (rs3 & U & V & W).
+  intros (rs3 & U & V).
   assert (EXEC_PROLOGUE:
             exec_straight tge tf
               tf.(fn_code) rs0 m'
@@ -1026,10 +976,6 @@ Local Transparent destroyed_at_function_entry. simpl.
   unfold sp; congruence.
   intros. rewrite V by auto with asmgen. reflexivity.
 
-  rewrite W.
-  unfold rs2.
-  Simpl.
-  
 - (* external function *)
   exploit functions_translated; eauto.
   intros [tf [A B]]. simpl in B. inv B.
@@ -1049,10 +995,6 @@ Local Transparent destroyed_at_function_entry. simpl.
   right. split. omega. split. auto.
   rewrite <- ATPC in H5.
   econstructor; eauto. congruence.
-  inv WF.
-  inv STACK.
-  inv H1.
-  congruence.
 Qed.
 
 Lemma transf_initial_states:
@@ -1088,17 +1030,11 @@ Qed.
 Theorem transf_program_correct:
   forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog).
 Proof.
-  eapply forward_simulation_star with (measure := measure)
-         (match_states := fun S1 S2 => match_states S1 S2 /\ wf_state ge S1).
-  - apply senv_preserved.
-  - simpl; intros. exploit transf_initial_states; eauto.
-    intros (s2 & A & B).
-    exists s2; intuition auto. apply wf_initial; auto.
-  - simpl; intros. destruct H as [MS WF]. eapply transf_final_states; eauto.
-  - simpl; intros. destruct H0 as [MS WF]. 
-    exploit step_simulation; eauto. intros [ (s2' & A & B) | (A & B & C) ].
-    + left; exists s2'; intuition auto. eapply wf_step; eauto. 
-    + right; intuition auto. eapply wf_step; eauto.
+  eapply forward_simulation_star with (measure := measure).
+  apply senv_preserved.
+  eexact transf_initial_states.
+  eexact transf_final_states.
+  exact step_simulation.
 Qed.
 
 End PRESERVATION.
diff --git a/aarch64/Asmgenproof1.v b/aarch64/Asmgenproof1.v
index 35f1f2d7..869d1a31 100644
--- a/aarch64/Asmgenproof1.v
+++ b/aarch64/Asmgenproof1.v
@@ -22,51 +22,6 @@ Local Transparent Archi.ptr64.
 
 (** Properties of registers *)
 
-Lemma preg_of_not_RA:
-  forall r, (preg_of r) <> RA.
-Proof.
-  destruct r; discriminate.
-Qed.
-
-Lemma RA_not_written:
-  forall (rs : regset) dst v,
-    rs # (preg_of dst) <- v RA = rs RA.
-Proof.
-  intros.
-  apply Pregmap.gso.
-  intro.
-  symmetry in H.
-  exact (preg_of_not_RA dst H).
-Qed.
-
-Hint Resolve RA_not_written : asmgen.
-
-Lemma RA_not_written2:
-  forall (rs : regset) dst v i,
-    preg_of dst = i ->
-    rs # i <- v RA = rs RA.
-Proof.
-  intros.
-  subst i.
-  apply RA_not_written.
-Qed.
-
-Hint Resolve RA_not_written2 : asmgen.
-
-Lemma RA_not_written3:
-  forall (rs : regset) dst v i,
-    ireg_of dst = OK i ->
-    rs # i <- v RA = rs RA.
-Proof.
-  intros.
-  unfold ireg_of in H.
-  destruct preg_of eqn:PREG; try discriminate.
-  replace i0 with i in * by congruence.
-  eapply RA_not_written2; eassumption.
-Qed.
-
-Hint Resolve RA_not_written3 : asmgen.
-
 Lemma preg_of_iregsp_not_PC: forall r, preg_of_iregsp r <> PC.
 Proof.
   destruct r; simpl; congruence.
@@ -84,6 +39,19 @@ Proof.
   red; intros; subst x. elim (preg_of_not_X16 r); auto.
 Qed.
 
+Lemma ireg_of_not_X16': forall r x, ireg_of r = OK x -> IR x <> IR X16.
+Proof.
+  intros. apply ireg_of_not_X16 in H. congruence.
+Qed.
+
+Hint Resolve preg_of_not_X16 ireg_of_not_X16 ireg_of_not_X16': asmgen.
+
+Lemma preg_of_not_RA:
+  forall r, (preg_of r) <> RA.
+Proof.
+  destruct r; discriminate.
+Qed.
+
 Lemma ireg_of_not_RA: forall r x, ireg_of r = OK x -> x <> RA.
 Proof.
   unfold ireg_of; intros. destruct (preg_of r) eqn:E; inv H.
@@ -104,13 +72,6 @@ Qed.
 
 Hint Resolve ireg_of_not_RA ireg_of_not_RA' ireg_of_not_RA'' : asmgen.
 
-Lemma ireg_of_not_X16': forall r x, ireg_of r = OK x -> IR x <> IR X16.
-Proof.
-  intros. apply ireg_of_not_X16 in H. congruence.
-Qed.
-
-Hint Resolve preg_of_not_X16 ireg_of_not_X16 ireg_of_not_X16': asmgen.
-
 (** Useful simplification tactic *)
 
 
@@ -270,49 +231,42 @@ Qed.
 Lemma exec_loadimm_k_w:
   forall (rd: ireg) k m l,
   wf_decomposition l ->
-  rd <> RA ->
   forall (rs: regset) accu,
   rs#rd = Vint (Int.repr accu) ->
   exists rs',
      exec_straight_opt ge fn (loadimm_k W rd l k) rs m k rs' m
   /\ rs'#rd = Vint (Int.repr (recompose_int accu l))
-  /\ (forall r, r <> PC -> r <> rd -> rs'#r = rs#r)
-  /\ rs' # RA = rs # RA.
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
 Proof.
-  induction 1; intros RD_NOT_RA rs accu ACCU; simpl.                          
+  induction 1; intros rs accu ACCU; simpl.
 - exists rs; split. apply exec_straight_opt_refl. auto.
-- destruct (IHwf_decomposition RD_NOT_RA
+- destruct (IHwf_decomposition
                 (nextinstr (rs#rd <- (insert_in_int rs#rd n p 16)))
                 (Zinsert accu n p 16))
-  as (rs' & P & Q & R & S).
+  as (rs' & P & Q & R).
   Simpl. rewrite ACCU. simpl. f_equal. apply Int.eqm_samerepr. 
   apply Zinsert_eqmod. auto. omega. apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
   exists rs'; split.
   eapply exec_straight_opt_step_opt. simpl; eauto. auto. exact P.
-  split. exact Q.
-  split.
-  { intros; Simpl.
-    rewrite R by auto. Simpl. }
-  { rewrite S. Simpl. }
+  split. exact Q. intros; Simpl. rewrite R by auto. Simpl.
 Qed.
 
 Lemma exec_loadimm_z_w:
   forall rd l k rs m,
   wf_decomposition l ->
-  rd <> RA ->
   exists rs',
      exec_straight ge fn (loadimm_z W rd l k) rs m k rs' m
   /\ rs'#rd = Vint (Int.repr (recompose_int 0 l))
   /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
 Proof.
-  unfold loadimm_z; destruct 1; intro RD_NOT_RA.
+  unfold loadimm_z; destruct 1.
 - econstructor; split.
   apply exec_straight_one. simpl; eauto. auto.
   split. Simpl.
   intros; Simpl.
 - set (accu0 := Zinsert 0 n p 16).
   set (rs1 := nextinstr (rs#rd <- (Vint (Int.repr accu0)))).
-  destruct (exec_loadimm_k_w rd k m l H1 RD_NOT_RA rs1 accu0) as (rs2 & P & Q & R & S); auto.
+  destruct (exec_loadimm_k_w rd k m l H1 rs1 accu0) as (rs2 & P & Q & R); auto.
   unfold rs1; Simpl.
   exists rs2; split.
   eapply exec_straight_opt_step; eauto.
@@ -325,13 +279,12 @@ Qed.
 Lemma exec_loadimm_n_w:
   forall rd l k rs m,
   wf_decomposition l ->
-  rd <> RA ->
   exists rs',
      exec_straight ge fn (loadimm_n W rd l k) rs m k rs' m
   /\ rs'#rd = Vint (Int.repr (Z.lnot (recompose_int 0 l)))
   /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
 Proof.
-  unfold loadimm_n; destruct 1; intro RD_NOT_RA.
+  unfold loadimm_n; destruct 1.
 - econstructor; split.
   apply exec_straight_one. simpl; eauto. auto.
   split. Simpl. 
@@ -340,8 +293,7 @@ Proof.
   set (rs1 := nextinstr (rs#rd <- (Vint (Int.repr accu0)))).
   destruct (exec_loadimm_k_w rd k m (negate_decomposition l) 
                                     (negate_decomposition_wf l H1)
-                                    RD_NOT_RA rs1 accu0)
-    as (rs2 & P & Q & R & S).
+                                    rs1 accu0) as (rs2 & P & Q & R).
   unfold rs1; Simpl.
   exists rs2; split.
   eapply exec_straight_opt_step; eauto.
@@ -353,8 +305,7 @@ Proof.
 Qed.
 
 Lemma exec_loadimm32:
-  forall rd n k rs m
-  (RD_NOT_RA : rd <> RA),
+  forall rd n k rs m,
   exists rs',
      exec_straight ge fn (loadimm32 rd n k) rs m k rs' m
   /\ rs'#rd = Vint n
@@ -377,14 +328,13 @@ Proof.
     apply Int.eqm_samerepr. apply decompose_notint_eqmod. 
     apply Int.repr_unsigned. }
   destruct Nat.leb.
-+ rewrite <- A. apply exec_loadimm_z_w. apply decompose_int_wf; omega. trivial.
-+ rewrite <- B. apply exec_loadimm_n_w. apply decompose_int_wf; omega. trivial.
++ rewrite <- A. apply exec_loadimm_z_w. apply decompose_int_wf; omega.
++ rewrite <- B. apply exec_loadimm_n_w. apply decompose_int_wf; omega.
 Qed.
 
 Lemma exec_loadimm_k_x:
   forall (rd: ireg) k m l,
-    wf_decomposition l ->
-    rd <> RA ->
+  wf_decomposition l ->
   forall (rs: regset) accu,
   rs#rd = Vlong (Int64.repr accu) ->
   exists rs',
@@ -392,9 +342,9 @@ Lemma exec_loadimm_k_x:
   /\ rs'#rd = Vlong (Int64.repr (recompose_int accu l))
   /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
 Proof.
-  induction 1; intros RD_NOT_RA rs accu ACCU; simpl.
+  induction 1; intros rs accu ACCU; simpl.
 - exists rs; split. apply exec_straight_opt_refl. auto.
-- destruct (IHwf_decomposition RD_NOT_RA
+- destruct (IHwf_decomposition
                 (nextinstr (rs#rd <- (insert_in_long rs#rd n p 16)))
                 (Zinsert accu n p 16))
   as (rs' & P & Q & R).
@@ -408,20 +358,19 @@ Qed.
 Lemma exec_loadimm_z_x:
   forall rd l k rs m,
   wf_decomposition l ->
-    rd <> RA ->
   exists rs',
      exec_straight ge fn (loadimm_z X rd l k) rs m k rs' m
   /\ rs'#rd = Vlong (Int64.repr (recompose_int 0 l))
   /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
 Proof.
-  unfold loadimm_z; destruct 1; intro RD_NOT_RA.
+  unfold loadimm_z; destruct 1.
 - econstructor; split.
   apply exec_straight_one. simpl; eauto. auto.
   split. Simpl.
   intros; Simpl.
 - set (accu0 := Zinsert 0 n p 16).
   set (rs1 := nextinstr (rs#rd <- (Vlong (Int64.repr accu0)))).
-  destruct (exec_loadimm_k_x rd k m l H1 RD_NOT_RA rs1 accu0) as (rs2 & P & Q & R); auto.
+  destruct (exec_loadimm_k_x rd k m l H1 rs1 accu0) as (rs2 & P & Q & R); auto.
   unfold rs1; Simpl.
   exists rs2; split.
   eapply exec_straight_opt_step; eauto.
@@ -434,13 +383,12 @@ Qed.
 Lemma exec_loadimm_n_x:
   forall rd l k rs m,
   wf_decomposition l ->
-  rd <> RA ->
   exists rs',
      exec_straight ge fn (loadimm_n X rd l k) rs m k rs' m
   /\ rs'#rd = Vlong (Int64.repr (Z.lnot (recompose_int 0 l)))
   /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
 Proof.
-  unfold loadimm_n; destruct 1; intro RD_NOT_RA.
+  unfold loadimm_n; destruct 1.
 - econstructor; split.
   apply exec_straight_one. simpl; eauto. auto.
   split. Simpl. 
@@ -449,7 +397,7 @@ Proof.
   set (rs1 := nextinstr (rs#rd <- (Vlong (Int64.repr accu0)))).
   destruct (exec_loadimm_k_x rd k m (negate_decomposition l) 
                                     (negate_decomposition_wf l H1)
-                                    RD_NOT_RA rs1 accu0) as (rs2 & P & Q & R).
+                                    rs1 accu0) as (rs2 & P & Q & R).
   unfold rs1; Simpl.
   exists rs2; split.
   eapply exec_straight_opt_step; eauto.
@@ -462,13 +410,12 @@ Qed.
 
 Lemma exec_loadimm64:
   forall rd n k rs m,
-    rd <> RA ->
   exists rs',
      exec_straight ge fn (loadimm64 rd n k) rs m k rs' m
   /\ rs'#rd = Vlong n
   /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
 Proof.
-  unfold loadimm64, loadimm; intros until m; intro RD_NOT_RA.
+  unfold loadimm64, loadimm; intros.
   destruct (is_logical_imm64 n).
 - econstructor; split.
   apply exec_straight_one. simpl; eauto. auto.
@@ -485,8 +432,8 @@ Proof.
     apply Int64.eqm_samerepr. apply decompose_notint_eqmod. 
     apply Int64.repr_unsigned. }
   destruct Nat.leb.
-+ rewrite <- A. apply exec_loadimm_z_x. apply decompose_int_wf; omega. trivial.
-+ rewrite <- B. apply exec_loadimm_n_x. apply decompose_int_wf; omega. trivial.
++ rewrite <- A. apply exec_loadimm_z_x. apply decompose_int_wf; omega.
++ rewrite <- B. apply exec_loadimm_n_x. apply decompose_int_wf; omega.
 Qed.
 
 (** Add immediate *)
@@ -498,59 +445,55 @@ Lemma exec_addimm_aux_32:
       Next (nextinstr (rs#rd <- (sem rs#r1 (Vint (Int.repr n))))) m) ->
   (forall v n1 n2, sem (sem v (Vint n1)) (Vint n2) = sem v (Vint (Int.add n1 n2))) ->
   forall rd r1 n k rs m,
-    (IR RA) <> (preg_of_iregsp (RR1 rd)) ->
   exists rs',
      exec_straight ge fn (addimm_aux insn rd r1 (Int.unsigned n) k) rs m k rs' m
   /\ rs'#rd = sem rs#r1 (Vint n)
-  /\ (forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r)
-  /\ rs' # RA = rs # RA.
+  /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
 Proof.
-  intros insn sem SEM ASSOC; intros until m; intro RD_NOT_RA. unfold addimm_aux.
+  intros insn sem SEM ASSOC; intros. unfold addimm_aux.
   set (nlo := Zzero_ext 12 (Int.unsigned n)). set (nhi := Int.unsigned n - nlo).
   assert (E: Int.unsigned n = nhi + nlo) by (unfold nhi; omega).
   rewrite <- (Int.repr_unsigned n).
   destruct (Z.eqb_spec nhi 0); [|destruct (Z.eqb_spec nlo 0)].
 - econstructor; split. apply exec_straight_one. apply SEM. Simpl. 
   split. Simpl. do 3 f_equal; omega.
-  split; intros; Simpl.
+  intros; Simpl.
 - econstructor; split. apply exec_straight_one. apply SEM. Simpl. 
   split. Simpl. do 3 f_equal; omega.
-  split; intros; Simpl.
+  intros; Simpl.
 - econstructor; split. eapply exec_straight_two.
   apply SEM. apply SEM. Simpl. Simpl.
   split. Simpl. rewrite ASSOC. do 2 f_equal. apply Int.eqm_samerepr.
   rewrite E. auto with ints.
-  split; intros; Simpl.
+  intros; Simpl.
 Qed.
 
 Lemma exec_addimm32:
   forall rd r1 n k rs m,
   r1 <> X16 ->
-  (IR RA) <> (preg_of_iregsp (RR1 rd)) ->
   exists rs',
      exec_straight ge fn (addimm32 rd r1 n k) rs m k rs' m
   /\ rs'#rd = Val.add rs#r1 (Vint n)
-  /\ (forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r)
-  /\ rs' # RA = rs # RA.
+  /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
 Proof.
   intros. unfold addimm32. set (nn := Int.neg n).
   destruct (Int.eq n (Int.zero_ext 24 n)); [| destruct (Int.eq nn (Int.zero_ext 24 nn))].
-- apply exec_addimm_aux_32 with (sem := Val.add); auto. intros; apply Val.add_assoc. 
+- apply exec_addimm_aux_32 with (sem := Val.add). auto. intros; apply Val.add_assoc. 
 - rewrite <- Val.sub_opp_add.
-  apply exec_addimm_aux_32 with (sem := Val.sub); auto.
+  apply exec_addimm_aux_32 with (sem := Val.sub). auto.
   intros. rewrite ! Val.sub_add_opp, Val.add_assoc. rewrite Int.neg_add_distr. auto.
 - destruct (Int.lt n Int.zero).
 + rewrite <- Val.sub_opp_add; fold nn.
-  edestruct (exec_loadimm32 X16 nn) as (rs1 & A & B & C). congruence.
+  edestruct (exec_loadimm32 X16 nn) as (rs1 & A & B & C).
   econstructor; split.
   eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. auto.
   split. Simpl. rewrite B, C; eauto with asmgen.
-  split; intros; Simpl.
-+ edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C). congruence.
+  intros; Simpl.
++ edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C).
   econstructor; split.
   eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. auto.
   split. Simpl. rewrite B, C; eauto with asmgen.
-  split; intros; Simpl.
+  intros; Simpl.
 Qed.
 
 Lemma exec_addimm_aux_64:
@@ -560,12 +503,10 @@ Lemma exec_addimm_aux_64:
       Next (nextinstr (rs#rd <- (sem rs#r1 (Vlong (Int64.repr n))))) m) ->
   (forall v n1 n2, sem (sem v (Vlong n1)) (Vlong n2) = sem v (Vlong (Int64.add n1 n2))) ->
   forall rd r1 n k rs m,
-  (IR RA) <> (preg_of_iregsp (RR1 rd)) ->
   exists rs',
      exec_straight ge fn (addimm_aux insn rd r1 (Int64.unsigned n) k) rs m k rs' m
   /\ rs'#rd = sem rs#r1 (Vlong n)
-  /\ (forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r)
-  /\ rs' # RA = rs # RA.
+  /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
 Proof.
   intros insn sem SEM ASSOC; intros. unfold addimm_aux.
   set (nlo := Zzero_ext 12 (Int64.unsigned n)). set (nhi := Int64.unsigned n - nlo).
@@ -574,46 +515,44 @@ Proof.
   destruct (Z.eqb_spec nhi 0); [|destruct (Z.eqb_spec nlo 0)].
 - econstructor; split. apply exec_straight_one. apply SEM. Simpl. 
   split. Simpl. do 3 f_equal; omega.
-  split; intros; Simpl.
+  intros; Simpl.
 - econstructor; split. apply exec_straight_one. apply SEM. Simpl. 
   split. Simpl. do 3 f_equal; omega.
-  split; intros; Simpl.
+  intros; Simpl.
 - econstructor; split. eapply exec_straight_two.
   apply SEM. apply SEM. Simpl. Simpl.
   split. Simpl. rewrite ASSOC. do 2 f_equal. apply Int64.eqm_samerepr.
   rewrite E. auto with ints.
-  split; intros; Simpl.
+  intros; Simpl.
 Qed.
 
 Lemma exec_addimm64:
   forall rd r1 n k rs m,
   preg_of_iregsp r1 <> X16 ->
-  (IR RA) <> (preg_of_iregsp (RR1 rd)) ->
   exists rs',
      exec_straight ge fn (addimm64 rd r1 n k) rs m k rs' m
   /\ rs'#rd = Val.addl rs#r1 (Vlong n)
-  /\ (forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r)
-  /\ rs' # RA = rs # RA.
+  /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
 Proof.
   intros. 
   unfold addimm64. set (nn := Int64.neg n).
   destruct (Int64.eq n (Int64.zero_ext 24 n)); [| destruct (Int64.eq nn (Int64.zero_ext 24 nn))].
-- apply exec_addimm_aux_64 with (sem := Val.addl); auto. intros; apply Val.addl_assoc. 
+- apply exec_addimm_aux_64 with (sem := Val.addl). auto. intros; apply Val.addl_assoc. 
 - rewrite <- Val.subl_opp_addl.
-  apply exec_addimm_aux_64 with (sem := Val.subl); auto.
+  apply exec_addimm_aux_64 with (sem := Val.subl). auto.
   intros. rewrite ! Val.subl_addl_opp, Val.addl_assoc. rewrite Int64.neg_add_distr. auto.
 - destruct (Int64.lt n Int64.zero).
 + rewrite <- Val.subl_opp_addl; fold nn.
-  edestruct (exec_loadimm64 X16 nn) as (rs1 & A & B & C). congruence.
+  edestruct (exec_loadimm64 X16 nn) as (rs1 & A & B & C).
   econstructor; split.
   eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. Simpl. 
   split. Simpl. rewrite B, C; eauto with asmgen. simpl. rewrite Int64.shl'_zero. auto.
-  split; intros; Simpl.
-+ edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C). congruence.
+  intros; Simpl.
++ edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C).
   econstructor; split.
   eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. Simpl. 
   split. Simpl. rewrite B, C; eauto with asmgen. simpl. rewrite Int64.shl'_zero. auto.
-  split; intros; Simpl.
+  intros; Simpl.
 Qed.
 
 (** Logical immediate *)
@@ -630,25 +569,22 @@ Lemma exec_logicalimm32:
       Next (nextinstr (rs#rd <- (sem rs##r1 (eval_shift_op_int rs#r2 s)))) m) ->
   forall rd r1 n k rs m,
   r1 <> X16 ->
-  (IR RA) <> (preg_of_iregsp (RR1 rd)) ->
   exists rs',
      exec_straight ge fn (logicalimm32 insn1 insn2 rd r1 n k) rs m k rs' m
   /\ rs'#rd = sem rs#r1 (Vint n)
-  /\ (forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r)
-  /\ rs' # RA = rs # RA.
+  /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
 Proof.
   intros until sem; intros SEM1 SEM2; intros. unfold logicalimm32.
   destruct (is_logical_imm32 n).
 - econstructor; split. 
   apply exec_straight_one. apply SEM1. reflexivity. 
-  split. Simpl. rewrite Int.repr_unsigned; auto.
-  split; intros; Simpl.
-- edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C). congruence.
+  split. Simpl. rewrite Int.repr_unsigned; auto. intros; Simpl.
+- edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C).
   econstructor; split.
   eapply exec_straight_trans. eexact A.  
   apply exec_straight_one. apply SEM2. reflexivity.
   split. Simpl. f_equal; auto. apply C; auto with asmgen.
-  split; intros; Simpl. 
+  intros; Simpl. 
 Qed.
 
 Lemma exec_logicalimm64:
@@ -663,58 +599,50 @@ Lemma exec_logicalimm64:
       Next (nextinstr (rs#rd <- (sem rs###r1 (eval_shift_op_long rs#r2 s)))) m) ->
   forall rd r1 n k rs m,
   r1 <> X16 ->
-  (IR RA) <> (preg_of_iregsp (RR1 rd)) ->
   exists rs',
      exec_straight ge fn (logicalimm64 insn1 insn2 rd r1 n k) rs m k rs' m
   /\ rs'#rd = sem rs#r1 (Vlong n)
-  /\ (forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r)
-  /\ rs' # RA = rs # RA.
+  /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
 Proof.
   intros until sem; intros SEM1 SEM2; intros. unfold logicalimm64.
   destruct (is_logical_imm64 n).
 - econstructor; split. 
   apply exec_straight_one. apply SEM1. reflexivity. 
-  split. Simpl. rewrite Int64.repr_unsigned. auto.
-  split; intros; Simpl.
-- edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C). congruence.
+  split. Simpl. rewrite Int64.repr_unsigned. auto. intros; Simpl.
+- edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C).
   econstructor; split.
   eapply exec_straight_trans. eexact A.  
   apply exec_straight_one. apply SEM2. reflexivity.
   split. Simpl. f_equal; auto. apply C; auto with asmgen.
-  split; intros; Simpl. 
+  intros; Simpl. 
 Qed.
 
 (** Load address of symbol *)
 
 Lemma exec_loadsymbol: forall rd s ofs k rs m,
-    rd <> X16 \/ Archi.pic_code tt = false ->
-    (IR RA) <> (preg_of_iregsp (RR1 rd)) ->
+  rd <> X16 \/ Archi.pic_code tt = false ->
   exists rs',
      exec_straight ge fn (loadsymbol rd s ofs k) rs m k rs' m
   /\ rs'#rd = Genv.symbol_address ge s ofs
-  /\ (forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r)
-  /\ rs'#RA = rs#RA.
+  /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
 Proof.
   unfold loadsymbol; intros. destruct (Archi.pic_code tt).
 - predSpec Ptrofs.eq Ptrofs.eq_spec ofs Ptrofs.zero.
 + subst ofs. econstructor; split.
   apply exec_straight_one; [simpl; eauto | reflexivity].
-  split. Simpl. split; intros; Simpl.
-  
+  split. Simpl. intros; Simpl.
 + exploit exec_addimm64. instantiate (1 := rd). simpl. destruct H; congruence.
-  instantiate (1 := rd). assumption.
-  intros (rs1 & A & B & C & D).
+  intros (rs1 & A & B & C).
   econstructor; split.
   econstructor. simpl; eauto. auto. eexact A. 
   split. simpl in B; rewrite B. Simpl. 
   rewrite <- Genv.shift_symbol_address_64 by auto.
   rewrite Ptrofs.add_zero_l, Ptrofs.of_int64_to_int64 by auto. auto.
-  split; intros. rewrite C by auto; Simpl.
-  rewrite D. Simpl.
+  intros. rewrite C by auto. Simpl.
 - econstructor; split.
   eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto.
   split. Simpl. rewrite symbol_high_low; auto. 
-  split; intros; Simpl.
+  intros; Simpl.
 Qed.
 
 (** Shifted operands *)
@@ -823,25 +751,23 @@ Lemma exec_arith_extended:
       Next (nextinstr (rs#rd <- (sem rs###r1 (eval_shift_op_long rs#r2 s)))) m) ->
   forall (rd r1 r2: ireg) (ex: extension) (a: amount64) (k: code) rs m,
   r1 <> X16 ->
-  (IR RA) <> (preg_of_iregsp (RR1 rd)) ->
   exists rs',
      exec_straight ge fn (arith_extended insnX insnS rd r1 r2 ex a k) rs m k rs' m
   /\ rs'#rd = sem rs#r1 (Op.eval_extend ex rs#r2 a)
-  /\ (forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r)
-  /\ rs' # RA = rs # RA.
+  /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
 Proof.
   intros sem insnX insnS EX ES; intros. unfold arith_extended. destruct (Int.ltu a (Int.repr 5)).
 - econstructor; split. 
   apply exec_straight_one. rewrite EX; eauto. auto.
   split. Simpl. f_equal. destruct ex; auto.
-  split; intros; Simpl.
+  intros; Simpl.
 - exploit (exec_move_extended_base X16 r2 ex). intros (rs' & A & B & C).
   econstructor; split.
   eapply exec_straight_trans. eexact A. apply exec_straight_one. 
   rewrite ES. eauto. auto.
   split. Simpl. unfold ir0x. rewrite C by eauto with asmgen. f_equal. 
   rewrite B. destruct ex; auto.
-  split; intros; Simpl.
+  intros; Simpl.
 Qed. 
 
 (** Extended right shift *)
@@ -1236,56 +1162,6 @@ Ltac ArgsInv :=
   | [ H: freg_of _ = OK _ |- _ ] => simpl in *; rewrite (freg_of_eq _ _ H) in *
   end).
 
-Lemma compare_int_RA:
-  forall rs a b m,
-    compare_int rs a b m X30 = rs X30.
-Proof.
-  unfold compare_int.
-  intros.
-  repeat rewrite Pregmap.gso by congruence.
-  trivial.
-Qed.
-
-Hint Resolve compare_int_RA : asmgen.
-
-Lemma compare_long_RA:
-  forall rs a b m,
-    compare_long rs a b m X30 = rs X30.
-Proof.
-  unfold compare_long.
-  intros.
-  repeat rewrite Pregmap.gso by congruence.
-  trivial.
-Qed.
-
-Hint Resolve compare_long_RA : asmgen.
-
-Lemma compare_float_RA:
-  forall rs a b,
-    compare_float rs a b X30 = rs X30.
-Proof.
-  unfold compare_float.
-  intros.
-  destruct a; destruct b.
-  all: repeat rewrite Pregmap.gso by congruence; trivial.
-Qed.
-
-Hint Resolve compare_float_RA : asmgen.
-  
-
-Lemma compare_single_RA:
-  forall rs a b,
-    compare_single rs a b X30 = rs X30.
-Proof.
-  unfold compare_single.
-  intros.
-  destruct a; destruct b.
-  all: repeat rewrite Pregmap.gso by congruence; trivial.
-Qed.
-
-Hint Resolve compare_single_RA : asmgen.
-  
-                                         
 Lemma transl_cond_correct:
   forall cond args k c rs m,
   transl_cond cond args k = OK c ->
@@ -1294,218 +1170,185 @@ Lemma transl_cond_correct:
   /\ (forall b,
       eval_condition cond (map rs (map preg_of args)) m = Some b ->
       eval_testcond (cond_for_cond cond) rs' = Some b)
-  /\ (forall r, data_preg r = true -> rs'#r = rs#r)
-  /\ rs' # RA = rs # RA.
+  /\ forall r, data_preg r = true -> rs'#r = rs#r.
 Proof.
   intros until m; intros TR. destruct cond; simpl in TR; ArgsInv.
 - (* Ccomp *)
   econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  repeat split; intros. apply eval_testcond_compare_sint; auto. 
+  split; intros. apply eval_testcond_compare_sint; auto. 
   destruct r; reflexivity || discriminate.
 - (* Ccompu *)
   econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  repeat split; intros. apply eval_testcond_compare_uint; auto. 
+  split; intros. apply eval_testcond_compare_uint; auto. 
   destruct r; reflexivity || discriminate.
 - (* Ccompimm *)
   destruct (is_arith_imm32 n); [|destruct (is_arith_imm32 (Int.neg n))].
 + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  repeat split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_sint; auto. 
+  split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_sint; auto. 
   destruct r; reflexivity || discriminate.
 + econstructor; split.
   apply exec_straight_one. simpl. rewrite Int.repr_unsigned, Int.neg_involutive. eauto. auto.
-  repeat split; intros. apply eval_testcond_compare_sint; auto. 
+  split; intros. apply eval_testcond_compare_sint; auto. 
   destruct r; reflexivity || discriminate.
-+ exploit (exec_loadimm32 X16 n). congruence. intros (rs' & A & B & C).
++ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C).
   econstructor; split.
   eapply exec_straight_trans. eexact A. apply exec_straight_one.
   simpl. rewrite B, C by eauto with asmgen. eauto. auto.
-  repeat split; intros. apply eval_testcond_compare_sint; auto. 
-  transitivity (rs' r). destruct r; reflexivity || discriminate.
-  auto with asmgen.
-  Simpl. rewrite compare_int_RA.
-  apply C; congruence.
+  split; intros. apply eval_testcond_compare_sint; auto. 
+  transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
 - (* Ccompuimm *)
   destruct (is_arith_imm32 n); [|destruct (is_arith_imm32 (Int.neg n))].
 + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  repeat split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_uint; auto. 
+  split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_uint; auto. 
   destruct r; reflexivity || discriminate.
 + econstructor; split.
   apply exec_straight_one. simpl. rewrite Int.repr_unsigned, Int.neg_involutive. eauto. auto.
-  repeat split; intros. apply eval_testcond_compare_uint; auto. 
+  split; intros. apply eval_testcond_compare_uint; auto. 
   destruct r; reflexivity || discriminate.
-+ exploit (exec_loadimm32 X16 n). congruence. intros (rs' & A & B & C).
++ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C).
   econstructor; split.
   eapply exec_straight_trans. eexact A. apply exec_straight_one.
   simpl. rewrite B, C by eauto with asmgen. eauto. auto.
-  repeat split; intros. apply eval_testcond_compare_uint; auto. 
+  split; intros. apply eval_testcond_compare_uint; auto. 
   transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
-  Simpl. rewrite compare_int_RA.
-  apply C; congruence.  
 - (* Ccompshift *)
   econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  repeat split; intros. rewrite transl_eval_shift. apply eval_testcond_compare_sint; auto. 
+  split; intros. rewrite transl_eval_shift. apply eval_testcond_compare_sint; auto. 
   destruct r; reflexivity || discriminate.
 - (* Ccompushift *)
   econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  repeat split; intros. rewrite transl_eval_shift. apply eval_testcond_compare_uint; auto. 
+  split; intros. rewrite transl_eval_shift. apply eval_testcond_compare_uint; auto. 
   destruct r; reflexivity || discriminate.
 - (* Cmaskzero *)
   destruct (is_logical_imm32 n).
 + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  repeat split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Ceq); auto.
+  split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Ceq); auto.
   destruct r; reflexivity || discriminate.
-+ exploit (exec_loadimm32 X16 n). congruence. intros (rs' & A & B & C).
++ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C).
   econstructor; split.
   eapply exec_straight_trans. eexact A.
   apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. auto.
-  repeat split; intros. apply (eval_testcond_compare_sint Ceq); auto.
+  split; intros. apply (eval_testcond_compare_sint Ceq); auto.
   transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
-  Simpl. rewrite compare_int_RA.
-  apply C; congruence.
-
 - (* Cmasknotzero *)
   destruct (is_logical_imm32 n).
 + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  repeat split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Cne); auto.
+  split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Cne); auto.
   destruct r; reflexivity || discriminate.
-
-+ exploit (exec_loadimm32 X16 n). congruence. intros (rs' & A & B & C).
++ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C).
   econstructor; split.
   eapply exec_straight_trans. eexact A.
   apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. auto.
-  repeat split; intros. apply (eval_testcond_compare_sint Cne); auto.
+  split; intros. apply (eval_testcond_compare_sint Cne); auto.
   transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
-  Simpl. rewrite compare_int_RA.
-  apply C; congruence.
-  
 - (* Ccompl *)
   econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  repeat split; intros. apply eval_testcond_compare_slong; auto. 
+  split; intros. apply eval_testcond_compare_slong; auto. 
   destruct r; reflexivity || discriminate.
 - (* Ccomplu *)
   econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  repeat split; intros. apply eval_testcond_compare_ulong; auto. 
+  split; intros. apply eval_testcond_compare_ulong; auto. 
   destruct r; reflexivity || discriminate.
 - (* Ccomplimm *)
   destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))].
 + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  repeat split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_slong; auto. 
+  split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_slong; auto. 
   destruct r; reflexivity || discriminate.
 + econstructor; split.
   apply exec_straight_one. simpl. rewrite Int64.repr_unsigned, Int64.neg_involutive. eauto. auto.
-  repeat split; intros. apply eval_testcond_compare_slong; auto. 
+  split; intros. apply eval_testcond_compare_slong; auto. 
   destruct r; reflexivity || discriminate.
-+ exploit (exec_loadimm64 X16 n). congruence. intros (rs' & A & B & C).
++ exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C).
   econstructor; split.
   eapply exec_straight_trans. eexact A. apply exec_straight_one.
   simpl. rewrite B, C by eauto with asmgen. eauto. auto.
-  repeat split; intros. apply eval_testcond_compare_slong; auto. 
+  split; intros. apply eval_testcond_compare_slong; auto. 
   transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
-  Simpl. rewrite compare_long_RA.
-  apply C; congruence.
-
 - (* Ccompluimm *)
   destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))].
 + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  repeat split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_ulong; auto. 
+  split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_ulong; auto. 
   destruct r; reflexivity || discriminate.
 + econstructor; split.
   apply exec_straight_one. simpl. rewrite Int64.repr_unsigned, Int64.neg_involutive. eauto. auto.
-  repeat split; intros. apply eval_testcond_compare_ulong; auto. 
+  split; intros. apply eval_testcond_compare_ulong; auto. 
   destruct r; reflexivity || discriminate.
-+ exploit (exec_loadimm64 X16 n). congruence. intros (rs' & A & B & C).
++ exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C).
   econstructor; split.
   eapply exec_straight_trans. eexact A. apply exec_straight_one.
   simpl. rewrite B, C by eauto with asmgen. eauto. auto.
-  repeat split; intros. apply eval_testcond_compare_ulong; auto. 
+  split; intros. apply eval_testcond_compare_ulong; auto. 
   transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
-  Simpl. rewrite compare_long_RA.
-  apply C; congruence.
-  
 - (* Ccomplshift *)
   econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  repeat split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_slong; auto. 
+  split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_slong; auto. 
   destruct r; reflexivity || discriminate.
 - (* Ccomplushift *)
   econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  repeat split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_ulong; auto. 
+  split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_ulong; auto. 
   destruct r; reflexivity || discriminate.
 - (* Cmasklzero *)
   destruct (is_logical_imm64 n).
 + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  repeat split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Ceq); auto.
+  split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Ceq); auto.
   destruct r; reflexivity || discriminate.
-+ exploit (exec_loadimm64 X16 n). congruence. intros (rs' & A & B & C).
++ exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C).
   econstructor; split.
   eapply exec_straight_trans. eexact A.
   apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. auto.
-  repeat split; intros. apply (eval_testcond_compare_slong Ceq); auto.
+  split; intros. apply (eval_testcond_compare_slong Ceq); auto.
   transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
-  Simpl. rewrite compare_long_RA.
-  apply C; congruence.
-
 - (* Cmasknotzero *)
   destruct (is_logical_imm64 n).
 + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  repeat split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Cne); auto.
+  split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Cne); auto.
   destruct r; reflexivity || discriminate.
-+ exploit (exec_loadimm64 X16 n). congruence. intros (rs' & A & B & C).
++ exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C).
   econstructor; split.
   eapply exec_straight_trans. eexact A.
   apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. auto.
-  repeat split; intros. apply (eval_testcond_compare_slong Cne); auto.
+  split; intros. apply (eval_testcond_compare_slong Cne); auto.
   transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
-    Simpl. rewrite compare_long_RA.
-  apply C; congruence.
-
 - (* Ccompf *)
   econstructor; split. apply exec_straight_one. simpl; eauto.
   rewrite compare_float_inv; auto.
-  repeat split; intros. apply eval_testcond_compare_float; auto.
+  split; intros. apply eval_testcond_compare_float; auto.
   destruct r; discriminate || rewrite compare_float_inv; auto.
-  Simpl. 
 - (* Cnotcompf *)
   econstructor; split. apply exec_straight_one. simpl; eauto.
   rewrite compare_float_inv; auto.
-  repeat split; intros. apply eval_testcond_compare_not_float; auto.
+  split; intros. apply eval_testcond_compare_not_float; auto.
   destruct r; discriminate || rewrite compare_float_inv; auto.
-  Simpl. 
 - (* Ccompfzero *)
   econstructor; split. apply exec_straight_one. simpl; eauto.
   rewrite compare_float_inv; auto.
-  repeat split; intros. apply eval_testcond_compare_float; auto.
+  split; intros. apply eval_testcond_compare_float; auto.
   destruct r; discriminate || rewrite compare_float_inv; auto.
-  Simpl.
 - (* Cnotcompfzero *)
   econstructor; split. apply exec_straight_one. simpl; eauto.
   rewrite compare_float_inv; auto.
-  repeat split; intros. apply eval_testcond_compare_not_float; auto.
+  split; intros. apply eval_testcond_compare_not_float; auto.
   destruct r; discriminate || rewrite compare_float_inv; auto.
-  Simpl.
 - (* Ccompfs *)
   econstructor; split. apply exec_straight_one. simpl; eauto.
   rewrite compare_single_inv; auto.
-  repeat split; intros. apply eval_testcond_compare_single; auto.
+  split; intros. apply eval_testcond_compare_single; auto.
   destruct r; discriminate || rewrite compare_single_inv; auto.
-  Simpl.
 - (* Cnotcompfs *)
   econstructor; split. apply exec_straight_one. simpl; eauto.
   rewrite compare_single_inv; auto.
-  repeat split; intros. apply eval_testcond_compare_not_single; auto.
+  split; intros. apply eval_testcond_compare_not_single; auto.
   destruct r; discriminate || rewrite compare_single_inv; auto.
-  Simpl.
 - (* Ccompfszero *)
   econstructor; split. apply exec_straight_one. simpl; eauto.
   rewrite compare_single_inv; auto.
-  repeat split; intros. apply eval_testcond_compare_single; auto.
+  split; intros. apply eval_testcond_compare_single; auto.
   destruct r; discriminate || rewrite compare_single_inv; auto.
-  Simpl.
 - (* Cnotcompfszero *)
   econstructor; split. apply exec_straight_one. simpl; eauto.
   rewrite compare_single_inv; auto.
-  repeat split; intros. apply eval_testcond_compare_not_single; auto.
+  split; intros. apply eval_testcond_compare_not_single; auto.
   destruct r; discriminate || rewrite compare_single_inv; auto.
-  Simpl.
 Qed.
 
 (** Translation of conditional branches *)
@@ -1518,8 +1361,7 @@ Lemma transl_cond_branch_correct:
      exec_straight_opt ge fn c rs m (insn :: k) rs' m
   /\ exec_instr ge fn insn rs' m =
          (if b then goto_label fn lbl rs' m else Next (nextinstr rs') m)
-  /\ (forall r, data_preg r = true -> rs'#r = rs#r)
-  /\ rs' # RA = rs # RA.
+  /\ forall r, data_preg r = true -> rs'#r = rs#r.
 Proof.
   intros until b; intros TR EV.
   assert (DFL:
@@ -1528,14 +1370,13 @@ Proof.
        exec_straight_opt ge fn c rs m (insn :: k) rs' m
     /\ exec_instr ge fn insn rs' m =
          (if b then goto_label fn lbl rs' m else Next (nextinstr rs') m)
-    /\ (forall r, data_preg r = true -> rs'#r = rs#r)
-     /\ rs' # RA = rs # RA ).
+    /\ forall r, data_preg r = true -> rs'#r = rs#r).
   {
     unfold transl_cond_branch_default; intros.
-    exploit transl_cond_correct; eauto. intros (rs' & A & B & C & D).
+    exploit transl_cond_correct; eauto. intros (rs' & A & B & C).
     exists rs', (Pbc (cond_for_cond cond) lbl); split.
     apply exec_straight_opt_intro. eexact A.
-    repeat split; auto. simpl. rewrite (B b) by auto. auto.
+    split; auto. simpl. rewrite (B b) by auto. auto. 
   }
 Local Opaque transl_cond transl_cond_branch_default.
   destruct args as [ | a1 args]; simpl in TR; auto.
@@ -1629,15 +1470,13 @@ Ltac TranslOpSimpl :=
   [ apply exec_straight_one; [simpl; eauto | reflexivity]
   | split; [ rewrite ? transl_eval_shift, ? transl_eval_shiftl;
              apply Val.lessdef_same; Simpl; fail
-           | split; [ intros; Simpl; fail
-                    | intros; Simpl; eauto with asmgen; fail] ]].
+           | intros; Simpl; fail ] ].
 
 Ltac TranslOpBase :=
   econstructor; split;
   [ apply exec_straight_one; [simpl; eauto | reflexivity]
   | split; [ rewrite ? transl_eval_shift, ? transl_eval_shiftl; Simpl
-           | split; [ intros; Simpl; fail
-                    | intros; Simpl; eapply RA_not_written2; eauto] ]].
+           | intros; Simpl; fail ] ].
 
 Lemma transl_op_correct:
   forall op args res k (rs: regset) m v c,
@@ -1646,29 +1485,21 @@ Lemma transl_op_correct:
   exists rs',
      exec_straight ge fn c rs m k rs' m
   /\ Val.lessdef v rs'#(preg_of res)
-  /\ (forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r)
-  /\ rs' RA = rs RA.
+  /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r.
 Proof.
 Local Opaque Int.eq Int64.eq Val.add Val.addl Int.zwordsize Int64.zwordsize.
   intros until c; intros TR EV.
   unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl.
 - (* move *)
   destruct (preg_of res) eqn:RR; try discriminate; destruct (preg_of m0) eqn:R1; inv TR.
-  all: TranslOpSimpl.
++ TranslOpSimpl.
++ TranslOpSimpl.
 - (* intconst *)
-  exploit exec_loadimm32. apply (ireg_of_not_RA res); eassumption.
-  intros (rs' & A & B & C).
-  exists rs'; split. eexact A. split. rewrite B; auto.
-  split. intros; auto with asmgen.
-  apply C. congruence.
-  eapply ireg_of_not_RA''; eauto.
+  exploit exec_loadimm32. intros (rs' & A & B & C).
+  exists rs'; split. eexact A. split. rewrite B; auto. intros; auto with asmgen.
 - (* longconst *)
-  exploit exec_loadimm64. apply (ireg_of_not_RA res); eassumption.
-  intros (rs' & A & B & C).
-  exists rs'; split. eexact A. split. rewrite B; auto.
-  split. intros; auto with asmgen.
-  apply C. congruence.
-  eapply ireg_of_not_RA''; eauto.
+  exploit exec_loadimm64. intros (rs' & A & B & C).
+  exists rs'; split. eexact A. split. rewrite B; auto. intros; auto with asmgen.
 - (* floatconst *)
   destruct (Float.eq_dec n Float.zero).
 + subst n. TranslOpSimpl. 
@@ -1678,15 +1509,11 @@ Local Opaque Int.eq Int64.eq Val.add Val.addl Int.zwordsize Int64.zwordsize.
 + subst n. TranslOpSimpl. 
 + TranslOpSimpl.
 - (* loadsymbol *)
-  exploit (exec_loadsymbol x id ofs). eauto with asmgen.
-  apply (ireg_of_not_RA'' res); eassumption. 
-  intros (rs' & A & B & C & D).
-  exists rs'; split. eexact A. split. rewrite B; auto.
-  split; auto.
+  exploit (exec_loadsymbol x id ofs). eauto with asmgen. intros (rs' & A & B & C).
+  exists rs'; split. eexact A. split. rewrite B; auto. auto.
 - (* addrstack *)
   exploit (exec_addimm64 x XSP (Ptrofs.to_int64 ofs)). simpl; eauto with asmgen.
-  apply (ireg_of_not_RA'' res); eassumption. 
-  intros (rs' & A & B & C & D).
+  intros (rs' & A & B & C).
   exists rs'; split. eexact A. split. simpl in B; rewrite B.
 Local Transparent Val.addl.
   destruct (rs SP); simpl; auto. rewrite Ptrofs.of_int64_to_int64 by auto. auto.
@@ -1694,8 +1521,7 @@ Local Transparent Val.addl.
 - (* shift *)
   rewrite <- transl_eval_shift'. TranslOpSimpl.
 - (* addimm *)
-  exploit (exec_addimm32 x x0 n). eauto with asmgen. eapply ireg_of_not_RA''; eassumption.
-  intros (rs' & A & B & C & D).
+  exploit (exec_addimm32 x x0 n). eauto with asmgen. intros (rs' & A & B & C).
   exists rs'; split. eexact A. split. rewrite B; auto. auto.
 - (* mul *)
   TranslOpBase.
@@ -1703,20 +1529,18 @@ Local Transparent Val.add.
   destruct (rs x0); auto; destruct (rs x1); auto. simpl. rewrite Int.add_zero_l; auto.
 - (* andimm *)
   exploit (exec_logicalimm32 (Pandimm W) (Pand W)). 
-  intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. apply (ireg_of_not_RA'' res); eassumption.
-  intros (rs' & A & B & C & D). 
-  exists rs'; split. eexact A. split. rewrite B; auto.
-  split; auto.
+  intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
+  intros (rs' & A & B & C). 
+  exists rs'; split. eexact A. split. rewrite B; auto. auto.
 - (* orimm *)
   exploit (exec_logicalimm32 (Porrimm W) (Porr W)). 
-  intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.  apply (ireg_of_not_RA'' res); eassumption.
-  intros (rs' & A & B & C & D). 
-  exists rs'; split. eexact A. split. rewrite B; auto.
-  split; auto.
+  intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
+  intros (rs' & A & B & C). 
+  exists rs'; split. eexact A. split. rewrite B; auto. auto.
 - (* xorimm *)
   exploit (exec_logicalimm32 (Peorimm W) (Peor W)). 
-  intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. apply (ireg_of_not_RA'' res); eassumption.
-  intros (rs' & A & B & C & D). 
+  intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
+  intros (rs' & A & B & C). 
   exists rs'; split. eexact A. split. rewrite B; auto. auto.
 - (* not *)
   TranslOpBase.
@@ -1728,16 +1552,15 @@ Local Transparent Val.add.
   destruct (Val.shrx (rs x0) (Vint n)) eqn:TOTAL.
   {
     exploit (exec_shrx32 x x0 n); eauto with asmgen. apply (ireg_of_not_RA'' res); eassumption.
-  intros (rs' & A & B & C & D).
-  econstructor; split. eexact A. split. rewrite B; auto.
-  split; auto.
+    intros (rs' & A & B & C & D).
+    econstructor; split. eexact A. split. rewrite B; auto.
+    auto.
   }
   exploit (exec_shrx32_none x x0 n); eauto with asmgen. apply (ireg_of_not_RA'' res); eassumption.
   intros (rs' & A & B & C).
   econstructor; split. { eexact A. }
   split. { cbn. constructor. }
-  split; auto.           
-  
+  auto.           
 - (* zero-ext *)
   TranslOpBase.
   destruct (rs x0); auto; simpl. rewrite Int.shl_zero. auto.
@@ -1761,47 +1584,36 @@ Local Transparent Val.add.
 - (* extend *)
   exploit (exec_move_extended x0 x1 x a k). intros (rs' & A & B & C).
   econstructor; split. eexact A. 
-  split. rewrite B; auto.
-  split; eauto with asmgen.
+  split. rewrite B; auto. eauto with asmgen.
 - (* addext *)
   exploit (exec_arith_extended Val.addl Paddext (Padd X)).
-  auto. auto. instantiate (1 := x1). eauto with asmgen.
-  apply (ireg_of_not_RA'' res); eassumption.
-  intros (rs' & A & B & C & D).
-  econstructor; split. eexact A. split. rewrite B; auto.
-  split; auto.
+  auto. auto. instantiate (1 := x1). eauto with asmgen. intros (rs' & A & B & C).
+  econstructor; split. eexact A. split. rewrite B; auto. auto.
 - (* addlimm *)
   exploit (exec_addimm64 x x0 n). simpl. generalize (ireg_of_not_X16 _ _ EQ1). congruence.
-  apply (ireg_of_not_RA'' res); eassumption.
-  intros (rs' & A & B & C & D).
+  intros (rs' & A & B & C).
   exists rs'; split. eexact A. split. simpl in B; rewrite B; auto. auto.
 - (* subext *)
   exploit (exec_arith_extended Val.subl Psubext (Psub X)).
-  auto. auto. instantiate (1 := x1). eauto with asmgen.
-  apply (ireg_of_not_RA'' res); eassumption.
-  intros (rs' & A & B & C & D).
-  econstructor; split. eexact A. split. rewrite B; auto.
-  split; auto.
+  auto. auto. instantiate (1 := x1). eauto with asmgen. intros (rs' & A & B & C).
+  econstructor; split. eexact A. split. rewrite B; auto. auto.
 - (* mull *)
   TranslOpBase.
   destruct (rs x0); auto; destruct (rs x1); auto. simpl. rewrite Int64.add_zero_l; auto.
 - (* andlimm *)
   exploit (exec_logicalimm64 (Pandimm X) (Pand X)). 
   intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
-  apply (ireg_of_not_RA'' res); eassumption.
-  intros (rs' & A & B & C & D). 
+  intros (rs' & A & B & C). 
   exists rs'; split. eexact A. split. rewrite B; auto. auto.
 - (* orlimm *)
   exploit (exec_logicalimm64 (Porrimm X) (Porr X)). 
   intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
-  apply (ireg_of_not_RA'' res); eassumption.
-  intros (rs' & A & B & C & D). 
+  intros (rs' & A & B & C). 
   exists rs'; split. eexact A. split. rewrite B; auto. auto.
 - (* xorlimm *)
   exploit (exec_logicalimm64 (Peorimm X) (Peor X)). 
   intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
-  apply (ireg_of_not_RA'' res); eassumption.
-  intros (rs' & A & B & C & D). 
+  intros (rs' & A & B & C). 
   exists rs'; split. eexact A. split. rewrite B; auto. auto.
 - (* notl *)
   TranslOpBase.
@@ -1809,7 +1621,7 @@ Local Transparent Val.add.
 - (* notlshift *)
   TranslOpBase.
   destruct (eval_shiftl s (rs x0) a); auto. simpl. rewrite Int64.or_zero_l; auto.
-- (* shrx *)
+- (* shrxl *)
   destruct (Val.shrxl (rs x0) (Vint n)) eqn:TOTAL.
   {
   exploit (exec_shrx64 x x0 n); eauto with asmgen.
@@ -1820,8 +1632,7 @@ Local Transparent Val.add.
   intros (rs' & A & B & C).
   econstructor; split. { eexact A. }
   split. { cbn. constructor. }
-  split; auto.           
-
+  auto.
 - (* zero-ext-l *)
   TranslOpBase.
   destruct (rs x0); auto; simpl. rewrite Int64.shl'_zero. auto.
@@ -1841,37 +1652,35 @@ Local Transparent Val.add.
   TranslOpBase.
   destruct (rs x0); simpl; auto. rewrite ! a64_range; simpl. rewrite <- Int64.sign_ext_shr'_min; auto using a64_range.
 - (* condition *)
-  exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C & D).
+  exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C).
   econstructor; split.
   eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto.
   split. Simpl. destruct (eval_condition cond (map rs (map preg_of args)) m) as [b|]; simpl in *.
   rewrite (B b) by auto. auto. 
   auto.
-  split; intros; Simpl.
+  intros; Simpl.
 - (* select *)
   destruct (preg_of res) eqn:RES; monadInv TR.
   + (* integer *)
     generalize (ireg_of_eq _ _ EQ) (ireg_of_eq _ _ EQ1); intros E1 E2; rewrite E1, E2.
-    exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C & D).
+    exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C).
     econstructor; split.
     eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto.
     split. Simpl. destruct (eval_condition cond (map rs (map preg_of args)) m) as [b|]; simpl in *.
     rewrite (B b) by auto. rewrite !C. apply Val.lessdef_normalize.
     rewrite <- E2; auto with asmgen. rewrite <- E1; auto with asmgen.
     auto.
-    split; intros; Simpl.
-    rewrite <- D.
-    eapply RA_not_written2; eassumption.
+    intros; Simpl.
   + (* FP *)
     generalize (freg_of_eq _ _ EQ) (freg_of_eq _ _ EQ1); intros E1 E2; rewrite E1, E2.
-    exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C & D).
+    exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C).
     econstructor; split.
     eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto.
     split. Simpl. destruct (eval_condition cond (map rs (map preg_of args)) m) as [b|]; simpl in *.
     rewrite (B b) by auto. rewrite !C. apply Val.lessdef_normalize.
     rewrite <- E2; auto with asmgen. rewrite <- E1; auto with asmgen.
     auto.
-    split; intros; Simpl.
+    intros; Simpl.
 Qed.
 
 (** Translation of addressing modes, loads, stores *)
@@ -1883,8 +1692,7 @@ Lemma transl_addressing_correct:
   exists ad rs',
      exec_straight_opt ge fn c rs m (insn ad :: k) rs' m
   /\ Asm.eval_addressing ge ad rs' = Vptr b o
-  /\ (forall r, data_preg r = true -> rs' r = rs r)
-  /\ rs' # RA = rs # RA.
+  /\ forall r, data_preg r = true -> rs' r = rs r.
 Proof.
   intros until o; intros TR EV.
   unfold transl_addressing in TR; destruct addr; ArgsInv; SimplEval EV.
@@ -1892,10 +1700,10 @@ Proof.
   destruct (offset_representable sz ofs); inv EQ0.
 + econstructor; econstructor; split. apply exec_straight_opt_refl.
   auto.
-+ exploit (exec_loadimm64 X16 ofs). congruence. intros (rs' & A & B & C).
++ exploit (exec_loadimm64 X16 ofs). intros (rs' & A & B & C).
   econstructor; exists rs'; split. apply exec_straight_opt_intro; eexact A.
   split. simpl. rewrite B, C by eauto with asmgen. auto.
-  split; eauto with asmgen.
+  eauto with asmgen.
 - (* Aindexed2 *)
   econstructor; econstructor; split. apply exec_straight_opt_refl.
   auto.
@@ -1911,38 +1719,33 @@ Proof.
 + econstructor; econstructor; split.
   apply exec_straight_opt_intro. apply exec_straight_one. simpl; eauto. auto.
   split. simpl. Simpl. rewrite H0. simpl. rewrite Ptrofs.add_zero. auto.
-  split; intros; Simpl.
+  intros; Simpl.
 - (* Aindexed2ext *)
   destruct (Int.eq a Int.zero || Int.eq (Int.shl Int.one a) (Int.repr sz)); inv EQ2.
 + econstructor; econstructor; split. apply exec_straight_opt_refl.
   split; auto. destruct x; auto.
 + exploit (exec_arith_extended Val.addl Paddext (Padd X)); auto.
   instantiate (1 := x0). eauto with asmgen.
-  instantiate (1 := X16). simpl. congruence.
-  intros (rs' & A & B & C & D).
+  intros (rs' & A & B & C).
   econstructor; exists rs'; split.
   apply exec_straight_opt_intro. eexact A. 
   split. simpl. rewrite B. rewrite Val.addl_assoc. f_equal.
   unfold Op.eval_extend; destruct x, (rs x1); simpl; auto; rewrite ! a64_range;
   simpl; rewrite Int64.add_zero; auto.
-  split; intros.
-  apply C; eauto with asmgen.
-  trivial.
+  intros. apply C; eauto with asmgen.
 - (* Aglobal *)
   destruct (Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz); inv TR.
 + econstructor; econstructor; split.
   apply exec_straight_opt_intro. apply exec_straight_one. simpl; eauto. auto.
   split. simpl. Simpl. rewrite symbol_high_low. simpl in EV. congruence.
-  split; intros; Simpl.
-+ exploit (exec_loadsymbol X16 id ofs). auto.
-  simpl. congruence.
-  intros (rs' & A & B & C & D).
+  intros; Simpl.
++ exploit (exec_loadsymbol X16 id ofs). auto. intros (rs' & A & B & C).
   econstructor; exists rs'; split.
   apply exec_straight_opt_intro. eexact A.
   split. simpl. 
   rewrite B. rewrite <- Genv.shift_symbol_address_64, Ptrofs.add_zero by auto. 
   simpl in EV. congruence. 
-  split; auto with asmgen.
+  auto with asmgen.
 - (* Ainstrack *)
   assert (E: Val.addl (rs SP) (Vlong (Ptrofs.to_int64 ofs)) = Vptr b o).
   { simpl in EV. inv EV. destruct (rs SP); simpl in H1; inv H1. simpl. 
@@ -1950,9 +1753,7 @@ Proof.
   destruct (offset_representable sz (Ptrofs.to_int64 ofs)); inv TR.
 + econstructor; econstructor; split. apply exec_straight_opt_refl.
   auto.
-+ exploit (exec_loadimm64 X16 (Ptrofs.to_int64 ofs)).
-  simpl. congruence.
-  intros (rs' & A & B & C).
++ exploit (exec_loadimm64 X16 (Ptrofs.to_int64 ofs)). intros (rs' & A & B & C).
   econstructor; exists rs'; split.
   apply exec_straight_opt_intro. eexact A.
   split. simpl. rewrite B, C by eauto with asmgen. auto.
@@ -1967,10 +1768,9 @@ Lemma transl_load_correct:
   exists rs',
      exec_straight ge fn c rs m k rs' m
   /\ rs'#(preg_of dst) = v
-  /\ (forall r, data_preg r = true -> r <> preg_of dst -> rs' r = rs r)
-  /\ rs' # RA = rs # RA.
+  /\ forall r, data_preg r = true -> r <> preg_of dst -> rs' r = rs r.
 Proof.
-  intros. destruct vaddr; try discriminate. 
+  intros. destruct vaddr; try discriminate.
   assert (A: exists sz insn,
                 transl_addressing sz addr args insn k = OK c
              /\ (forall ad rs', exec_instr ge fn (insn ad) rs' m =
@@ -1981,17 +1781,14 @@ Proof.
     do 2 econstructor; (split; [eassumption|auto]).
   }
   destruct A as (sz & insn & B & C).
-  exploit transl_addressing_correct. eexact B. eexact H0. intros (ad & rs' & P & Q & R & S).
+  exploit transl_addressing_correct. eexact B. eexact H0. intros (ad & rs' & P & Q & R).
   assert (X: exec_load ge chunk (fun v => v) ad (preg_of dst) rs' m =
              Next (nextinstr (rs'#(preg_of dst) <- v)) m).
   { unfold exec_load. rewrite Q, H1. auto. }
   econstructor; split.
   eapply exec_straight_opt_right. eexact P.
   apply exec_straight_one. rewrite C, X; eauto. Simpl. 
-  split. Simpl.
-  split; intros; Simpl.
-  rewrite <- S.
-  apply RA_not_written.
+  split. Simpl. intros; Simpl.
 Qed.
 
 Lemma transl_store_correct:
@@ -2001,8 +1798,7 @@ Lemma transl_store_correct:
   Mem.storev chunk m vaddr rs#(preg_of src) = Some m' ->
   exists rs',
      exec_straight ge fn c rs m k rs' m'
-     /\ (forall r, data_preg r = true -> rs' r = rs r)
-     /\ rs' # RA = rs # RA.
+  /\ forall r, data_preg r = true -> rs' r = rs r.
 Proof.
   intros. destruct vaddr; try discriminate. 
   set (chunk' := match chunk with Mint8signed => Mint8unsigned
@@ -2018,7 +1814,7 @@ Proof.
     do 2 econstructor; (split; [eassumption|auto]).
   }
   destruct A as (sz & insn & B & C).
-  exploit transl_addressing_correct. eexact B. eexact H0. intros (ad & rs' & P & Q & R & S).                                                  
+  exploit transl_addressing_correct. eexact B. eexact H0. intros (ad & rs' & P & Q & R).
   assert (X: Mem.storev chunk' m (Vptr b i) rs#(preg_of src) = Some m').
   { rewrite <- H1. unfold chunk'. destruct chunk; auto; simpl; symmetry.
     apply Mem.store_signed_unsigned_8.
@@ -2029,7 +1825,7 @@ Proof.
   econstructor; split.
   eapply exec_straight_opt_right. eexact P.
   apply exec_straight_one. rewrite C, Y; eauto. Simpl. 
-  split; intros; Simpl.
+  intros; Simpl.
 Qed.
 
 (** Translation of indexed memory accesses *)
@@ -2047,9 +1843,7 @@ Proof.
   { destruct (rs base); try discriminate. simpl in *. rewrite Ptrofs.of_int64_to_int64 by auto. auto. }
   destruct offset_representable.
 - econstructor; econstructor; split. apply exec_straight_opt_refl. auto. 
-- exploit (exec_loadimm64 X16); eauto.
-  simpl. congruence.
-  intros (rs' & A & B & C).
+- exploit (exec_loadimm64 X16); eauto. intros (rs' & A & B & C).
   econstructor; econstructor; split. apply exec_straight_opt_intro; eexact A.
   split. simpl. rewrite B, C by eauto with asmgen. auto. auto.
 Qed.
@@ -2060,7 +1854,7 @@ Lemma loadptr_correct: forall (base: iregsp) ofs dst k m v (rs: regset),
   exists rs',
      exec_straight ge fn (loadptr base ofs dst k) rs m k rs' m
   /\ rs'#dst = v
-  /\ (forall r, r <> PC -> r <> X16 -> r <> dst -> rs' r = rs r).
+  /\ forall r, r <> PC -> r <> X16 -> r <> dst -> rs' r = rs r.
 Proof.
   intros. 
   destruct (Val.offset_ptr rs#base ofs) eqn:V; try discriminate.
@@ -2068,8 +1862,7 @@ Proof.
   econstructor; split.
   eapply exec_straight_opt_right. eexact A.
   apply exec_straight_one. simpl. unfold exec_load. rewrite B, H. eauto. auto.
-  split. Simpl.
-  intros; Simpl.
+  split. Simpl. intros; Simpl.
 Qed.
 
 Lemma storeptr_correct: forall (base: iregsp) ofs (src: ireg) k m m' (rs: regset),
@@ -2078,8 +1871,7 @@ Lemma storeptr_correct: forall (base: iregsp) ofs (src: ireg) k m m' (rs: regset
   src <> X16 ->
   exists rs',
      exec_straight ge fn (storeptr src base ofs k) rs m k rs' m'
-  /\ (forall r, r <> PC -> r <> X16 -> rs' r = rs r)
-  /\ rs' RA = rs RA.
+  /\ forall r, r <> PC -> r <> X16 -> rs' r = rs r.
 Proof.
   intros. 
   destruct (Val.offset_ptr rs#base ofs) eqn:V; try discriminate.
@@ -2087,7 +1879,7 @@ Proof.
   econstructor; split.
   eapply exec_straight_opt_right. eexact A.
   apply exec_straight_one. simpl. unfold exec_store. rewrite B, C, H by eauto with asmgen. eauto. auto.
-  split; intros; Simpl.
+  intros; Simpl.
 Qed.
 
 Lemma loadind_correct: forall (base: iregsp) ofs ty dst k c (rs: regset) m v,
@@ -2097,8 +1889,7 @@ Lemma loadind_correct: forall (base: iregsp) ofs ty dst k c (rs: regset) m v,
   exists rs',
      exec_straight ge fn c rs m k rs' m
   /\ rs'#(preg_of dst) = v
-  /\ (forall r, data_preg r = true -> r <> preg_of dst -> rs' r = rs r)
-  /\ rs' RA = rs RA.
+  /\ forall r, data_preg r = true -> r <> preg_of dst -> rs' r = rs r.
 Proof.
   intros. 
   destruct (Val.offset_ptr rs#base ofs) eqn:V; try discriminate.
@@ -2114,10 +1905,7 @@ Proof.
   econstructor; split.
   eapply exec_straight_opt_right. eexact A.
   apply exec_straight_one. rewrite SEM. unfold exec_load. rewrite B, H0. eauto. Simpl.
-  split. Simpl.
-  split. intros; Simpl.
-  Simpl. rewrite RA_not_written.
-  apply C; congruence.
+  split. Simpl. intros; Simpl.
 Qed.
 
 Lemma storeind_correct: forall (base: iregsp) ofs ty src k c (rs: regset) m m',
@@ -2126,8 +1914,7 @@ Lemma storeind_correct: forall (base: iregsp) ofs ty src k c (rs: regset) m m',
   preg_of_iregsp base <> IR X16 ->
   exists rs',
      exec_straight ge fn c rs m k rs' m'
-     /\ (forall r, data_preg r = true -> rs' r = rs r)
-     /\ rs' RA = rs RA.
+  /\ forall r, data_preg r = true -> rs' r = rs r.
 Proof.
   intros. 
   destruct (Val.offset_ptr rs#base ofs) eqn:V; try discriminate.
@@ -2145,15 +1932,13 @@ Proof.
   apply exec_straight_one. rewrite SEM.
   unfold exec_store. rewrite B, C, H0 by eauto with asmgen. eauto.
   Simpl.
-  split. intros; Simpl.
-  Simpl. 
+  intros; Simpl.
 Qed.
 
 Lemma make_epilogue_correct:
   forall ge0 f m stk soff cs m' ms rs k tm,
-  (is_leaf_function f = true -> rs # (IR RA) = parent_ra cs) ->
   load_stack m (Vptr stk soff) Tptr f.(fn_link_ofs) = Some (parent_sp cs) ->
-  ((* FIXME is_leaf_function f = false -> *) load_stack m (Vptr stk soff) Tptr f.(fn_retaddr_ofs) = Some (parent_ra cs)) ->
+  load_stack m (Vptr stk soff) Tptr f.(fn_retaddr_ofs) = Some (parent_ra cs) ->
   Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
   agree ms (Vptr stk soff) rs ->
   Mem.extends m tm ->
@@ -2164,46 +1949,18 @@ Lemma make_epilogue_correct:
   /\ Mem.extends m' tm'
   /\ rs'#RA = parent_ra cs
   /\ rs'#SP = parent_sp cs
-  /\ (forall r, r <> PC -> r <> SP -> r <> RA -> r <> X16 -> rs'#r = rs#r).
+  /\ (forall r, r <> PC -> r <> SP -> r <> X30 -> r <> X16 -> rs'#r = rs#r).
 Proof.
-  intros until tm; intros LEAF_RA LP LRA FREE AG MEXT MCS.
-
-  (* FIXME
-  Cannot be used at this point
-  destruct (is_leaf_function f) eqn:IS_LEAF.
-  {
-  exploit Mem.loadv_extends. eauto. eexact LP. auto. simpl. intros (parent' & LP' & LDP').
-  exploit lessdef_parent_sp; eauto. intros EQ; subst parent'; clear LDP'.
-  exploit Mem.free_parallel_extends; eauto. intros (tm' & FREE' & MEXT').
-  unfold make_epilogue.
-  rewrite IS_LEAF.
-
-  econstructor; econstructor; split.
-  apply exec_straight_one. simpl.
-  rewrite <- (sp_val _ _ _ AG). simpl; rewrite LP'. 
-    rewrite FREE'. eauto. auto. 
-  split. apply agree_nextinstr. apply agree_set_other; auto.
-  apply agree_change_sp with (Vptr stk soff).
-  apply agree_exten with rs; auto.
-  eapply parent_sp_def; eauto.
-  split. auto.
-  split. Simpl.
-  split. Simpl.
-  intros. Simpl.
-  }
-  lapply LRA. 2: reflexivity.
-  clear LRA. intro LRA. *)
+  intros until tm; intros LP LRA FREE AG MEXT MCS.
   exploit Mem.loadv_extends. eauto. eexact LP. auto. simpl. intros (parent' & LP' & LDP').
   exploit Mem.loadv_extends. eauto. eexact LRA. auto. simpl. intros (ra' & LRA' & LDRA').
   exploit lessdef_parent_sp; eauto. intros EQ; subst parent'; clear LDP'.
   exploit lessdef_parent_ra; eauto. intros EQ; subst ra'; clear LDRA'.
   exploit Mem.free_parallel_extends; eauto. intros (tm' & FREE' & MEXT').
-  unfold make_epilogue.
-  (* FIXME rewrite IS_LEAF. *)
+  unfold make_epilogue. 
   exploit (loadptr_correct XSP (fn_retaddr_ofs f)).
     instantiate (2 := rs). simpl. rewrite <- (sp_val _ _ _ AG). simpl. eexact LRA'. simpl; congruence.
   intros (rs1 & A1 & B1 & C1).
-
   econstructor; econstructor; split.
   eapply exec_straight_trans. eexact A1. apply exec_straight_one. simpl. 
     simpl; rewrite (C1 SP) by auto with asmgen. rewrite <- (sp_val _ _ _ AG). simpl; rewrite LP'. 
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 7ddbcc34..505b7545 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -573,8 +573,7 @@ Definition is_trapping_op (op : operation) :=
   match op with
   | Odiv | Odivl | Odivu | Odivlu
   | Oshrximm _ | Oshrxlimm _
-  | Ointoffloat | Ointuoffloat
-  | Ofloatofint | Ofloatofintu
+  | Ointoffloat     
   | Olongoffloat
   | Ofloatoflong => true
   | _ => false