Add scheduling oracle to Verilog

1 files changed, 1455 insertions, 1367 deletions

diff --git a/verilog/Asmgenproof1.v b/verilog/Asmgenproof1.v
index 7cff1047..42ab8375 100644
--- a/verilog/Asmgenproof1.v
+++ b/verilog/Asmgenproof1.v
@@ -2,1541 +2,1629 @@
 (*                                                                     *)
 (*              The Compcert verified compiler                         *)
 (*                                                                     *)
-(*                  Xavier Leroy, INRIA Paris                          *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*           Prashanth Mundkur, SRI International                      *)
 (*                                                                     *)
 (*  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.     *)
 (*                                                                     *)
+(*  The contributions by Prashanth Mundkur are reused and adapted      *)
+(*  under the terms of a Contributor License Agreement between         *)
+(*  SRI International and INRIA.                                       *)
+(*                                                                     *)
 (* *********************************************************************)
 
-(** Correctness proof for x86-64 generation: auxiliary results. *)
-
-Require Import Coqlib.
-Require Import AST Errors Integers Floats Values Memory Globalenvs.
-Require Import Op Locations Conventions Mach Asm.
-Require Import Asmgen Asmgenproof0.
+Require Import Coqlib Errors Maps.
+Require Import AST Zbits Integers Floats Values Memory Globalenvs.
+Require Import Op Locations Mach Conventions.
+Require Import Asm Asmgen Asmgenproof0.
 
-Local Open Scope error_monad_scope.
+(** Decomposition of integer constants. *)
 
-(** * Correspondence between Mach registers and x86 registers *)
-
-Lemma agree_nextinstr_nf:
-  forall ms sp rs,
-  agree ms sp rs -> agree ms sp (nextinstr_nf rs).
+Lemma make_immed32_sound:
+  forall n,
+  match make_immed32 n with
+  | Imm32_single imm => n = imm
+  | Imm32_pair hi lo => n = Int.add (Int.shl hi (Int.repr 12)) lo
+  end.
 Proof.
-  intros. unfold nextinstr_nf. apply agree_nextinstr.
-  apply agree_undef_nondata_regs. auto.
-  simpl; intros. intuition (subst r; auto).
+  intros; unfold make_immed32. set (lo := Int.sign_ext 12 n).
+  predSpec Int.eq Int.eq_spec n lo.
+- auto.
+- set (m := Int.sub n lo).
+  assert (A: eqmod (two_p 12) (Int.unsigned lo) (Int.unsigned n)) by (apply Int.eqmod_sign_ext'; compute; auto).
+  assert (B: eqmod (two_p 12) (Int.unsigned n - Int.unsigned  lo) 0).
+  { replace 0 with (Int.unsigned n - Int.unsigned n) by lia.
+    auto using eqmod_sub, eqmod_refl. }
+  assert (C: eqmod (two_p 12) (Int.unsigned m) 0).
+  { apply eqmod_trans with (Int.unsigned n - Int.unsigned lo); auto.
+    apply eqmod_divides with Int.modulus. apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
+    exists (two_p (32-12)); auto. }
+  assert (D: Int.modu m (Int.repr 4096) = Int.zero).
+  { apply eqmod_mod_eq in C. unfold Int.modu. 
+    change (Int.unsigned (Int.repr 4096)) with (two_p 12). rewrite C. 
+    reflexivity.
+    apply two_p_gt_ZERO; lia. }
+  rewrite <- (Int.divu_pow2 m (Int.repr 4096) (Int.repr 12)) by auto.
+  rewrite Int.shl_mul_two_p. 
+  change (two_p (Int.unsigned (Int.repr 12))) with 4096.
+  replace (Int.mul (Int.divu m (Int.repr 4096)) (Int.repr 4096)) with m.
+  unfold m. rewrite Int.sub_add_opp. rewrite Int.add_assoc. rewrite <- (Int.add_commut lo).
+  rewrite Int.add_neg_zero. rewrite Int.add_zero. auto.
+  rewrite (Int.modu_divu_Euclid m (Int.repr 4096)) at 1 by (vm_compute; congruence).
+  rewrite D. apply Int.add_zero.
 Qed.
 
-(** Useful properties of the PC register. *)
-
-Lemma nextinstr_nf_inv:
-  forall r rs,
-  match r with PC => False | CR _ => False | _ => True end ->
-  (nextinstr_nf rs)#r = rs#r.
+Lemma make_immed64_sound:
+  forall n,
+  match make_immed64 n with
+  | Imm64_single imm => n = imm
+  | Imm64_pair hi lo => n = Int64.add (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) lo
+  | Imm64_large imm => n = imm
+  end.
 Proof.
-  intros. unfold nextinstr_nf. rewrite nextinstr_inv.
-  simpl. repeat rewrite Pregmap.gso; auto;
-  red; intro; subst; contradiction.
-  red; intro; subst; contradiction.
+  intros; unfold make_immed64. set (lo := Int64.sign_ext 12 n).
+  predSpec Int64.eq Int64.eq_spec n lo.
+- auto.
+- set (m := Int64.sub n lo).
+  set (p := Int64.zero_ext 20 (Int64.shru m (Int64.repr 12))).
+  predSpec Int64.eq Int64.eq_spec n (Int64.add (Int64.sign_ext 32 (Int64.shl p (Int64.repr 12))) lo).
+  auto.
+  auto.
 Qed.
 
-Lemma nextinstr_nf_inv1:
-  forall r rs,
-  data_preg r = true -> (nextinstr_nf rs)#r = rs#r.
+(** Properties of registers *)
+
+Lemma ireg_of_not_X31:
+  forall m r, ireg_of m = OK r -> IR r <> IR X31.
 Proof.
-  intros. apply nextinstr_nf_inv. destruct r; auto || discriminate.
+  intros. erewrite <- ireg_of_eq; eauto with asmgen.
 Qed.
 
-Lemma nextinstr_nf_set_preg:
-  forall rs m v,
-  (nextinstr_nf (rs#(preg_of m) <- v))#PC = Val.offset_ptr rs#PC Ptrofs.one.
+Lemma ireg_of_not_X31':
+  forall m r, ireg_of m = OK r -> r <> X31.
 Proof.
-  intros. unfold nextinstr_nf.
-  transitivity (nextinstr (rs#(preg_of m) <- v) PC). auto.
-  apply nextinstr_set_preg.
+  intros. apply ireg_of_not_X31 in H. congruence.
 Qed.
 
+Global Hint Resolve ireg_of_not_X31 ireg_of_not_X31': asmgen.
+
 (** Useful simplification tactic *)
 
 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.
+  ((rewrite nextinstr_inv by eauto with asmgen)
+  || (rewrite nextinstr_inv1 by eauto with asmgen)
+  || (rewrite Pregmap.gss)
+  || (rewrite nextinstr_pc)
+  || (rewrite Pregmap.gso by eauto with asmgen)); auto with asmgen.
 
-Ltac Simplifs := repeat Simplif.
+Ltac Simpl := repeat Simplif.
 
-(** * Correctness of x86-64 constructor functions *)
+(** * Correctness of RISC-V constructor functions *)
 
 Section CONSTRUCTORS.
 
 Variable ge: genv.
 Variable fn: function.
 
-(** Smart constructor for moves. *)
+(** 32-bit integer constants and arithmetic *)
 
-Lemma mk_mov_correct:
-  forall rd rs k c rs1 m,
-  mk_mov rd rs k = OK c ->
-  exists rs2,
-     exec_straight ge fn c rs1 m k rs2 m
-  /\ rs2#rd = rs1#rs
-  /\ forall r, data_preg r = true -> r <> rd -> rs2#r = rs1#r.
+Lemma load_hilo32_correct:
+  forall rd hi lo k rs m,
+  exists rs',
+     exec_straight ge fn (load_hilo32 rd hi lo k) rs m k rs' m
+  /\ rs'#rd = Vint (Int.add (Int.shl hi (Int.repr 12)) lo)
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#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. Simplifs. intros; Simplifs.
-(* movsd *)
-  econstructor. split. apply exec_straight_one. simpl. eauto. auto.
-  split. Simplifs. intros; Simplifs.
+  unfold load_hilo32; intros. 
+  predSpec Int.eq Int.eq_spec lo Int.zero.
+- subst lo. econstructor; split. 
+  apply exec_straight_one. simpl; eauto. auto.
+  split. rewrite Int.add_zero. Simpl.
+  intros; Simpl.
+- econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split. Simpl. 
+  intros; Simpl.
 Qed.
 
-(** Properties of division *)
-
-Lemma divu_modu_exists:
-  forall v1 v2,
-  Val.divu v1 v2 <> None \/ Val.modu v1 v2 <> None ->
-  exists n d q r,
-     v1 = Vint n /\ v2 = Vint d
-  /\ Int.divmodu2 Int.zero n d = Some(q, r)
-  /\ Val.divu v1 v2 = Some (Vint q) /\ Val.modu v1 v2 = Some (Vint r).
+Lemma loadimm32_correct:
+  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
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
 Proof.
-  intros v1 v2; unfold Val.divu, Val.modu.
-  destruct v1; try (intuition discriminate).
-  destruct v2; try (intuition discriminate).
-  predSpec Int.eq Int.eq_spec i0 Int.zero ; try (intuition discriminate).
-  intros _. exists i, i0, (Int.divu i i0), (Int.modu i i0); intuition auto.
-  apply Int.divmodu2_divu_modu; auto.
+  unfold loadimm32; intros. generalize (make_immed32_sound n); intros E.
+  destruct (make_immed32 n). 
+- subst imm. econstructor; split. 
+  apply exec_straight_one. simpl; eauto. auto.
+  split. rewrite Int.add_zero_l; Simpl. 
+  intros; Simpl.
+- rewrite E. apply load_hilo32_correct.
 Qed.
 
-Lemma divs_mods_exists:
-  forall v1 v2,
-  Val.divs v1 v2 <> None \/ Val.mods v1 v2 <> None ->
-  exists nh nl d q r,
-     Val.shr v1 (Vint (Int.repr 31)) = Vint nh /\ v1 = Vint nl /\ v2 = Vint d
-  /\ Int.divmods2 nh nl d = Some(q, r)
-  /\ Val.divs v1 v2 = Some (Vint q) /\ Val.mods v1 v2 = Some (Vint r).
+Lemma opimm32_correct:
+  forall (op: ireg -> ireg0 -> ireg0 -> instruction)
+         (opi: ireg -> ireg0 -> int -> instruction)
+         (sem: val -> val -> val) m,
+  (forall d s1 s2 rs,
+   exec_instr ge fn (op d s1 s2) rs m = Next (nextinstr (rs#d <- (sem rs##s1 rs##s2))) m) ->
+  (forall d s n rs,
+   exec_instr ge fn (opi d s n) rs m = Next (nextinstr (rs#d <- (sem rs##s (Vint n)))) m) ->
+  forall rd r1 n k rs,
+  r1 <> X31 ->
+  exists rs',
+     exec_straight ge fn (opimm32 op opi rd r1 n k) rs m k rs' m
+  /\ rs'#rd = sem rs##r1 (Vint n)
+  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
 Proof.
-  intros v1 v2; unfold Val.divs, Val.mods.
-  destruct v1; try (intuition discriminate).
-  destruct v2; try (intuition discriminate).
-  destruct (Int.eq i0 Int.zero
-            || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone) eqn:OK;
-  try (intuition discriminate).
-  intros _.
-  InvBooleans.
-  exists (Int.shr i (Int.repr 31)), i, i0, (Int.divs i i0), (Int.mods i i0); intuition auto.
-  rewrite Int.shr_lt_zero. apply Int.divmods2_divs_mods.
-  red; intros; subst i0; rewrite Int.eq_true in H; discriminate.
-  revert H0. predSpec Int.eq Int.eq_spec i (Int.repr Int.min_signed); auto.
-  predSpec Int.eq Int.eq_spec i0 Int.mone; auto.
-  discriminate.
+  intros. unfold opimm32. generalize (make_immed32_sound n); intros E.
+  destruct (make_immed32 n). 
+- subst imm. econstructor; split. 
+  apply exec_straight_one. rewrite H0. simpl; eauto. auto.
+  split. Simpl. intros; Simpl.
+- destruct (load_hilo32_correct X31 hi lo (op rd r1 X31 :: k) rs m)
+  as (rs' & A & B & C).
+  econstructor; split.
+  eapply exec_straight_trans. eexact A. apply exec_straight_one. 
+  rewrite H; eauto. auto.
+  split. Simpl. simpl. rewrite B, C, E. auto. congruence. congruence.
+  intros; Simpl. 
 Qed.
 
-Lemma divlu_modlu_exists:
-  forall v1 v2,
-  Val.divlu v1 v2 <> None \/ Val.modlu v1 v2 <> None ->
-  exists n d q r,
-     v1 = Vlong n /\ v2 = Vlong d
-  /\ Int64.divmodu2 Int64.zero n d = Some(q, r)
-  /\ Val.divlu v1 v2 = Some (Vlong q) /\ Val.modlu v1 v2 = Some (Vlong r).
+(** 64-bit integer constants and arithmetic *)
+
+Lemma load_hilo64_correct:
+  forall rd hi lo k rs m,
+  exists rs',
+     exec_straight ge fn (load_hilo64 rd hi lo k) rs m k rs' m
+  /\ rs'#rd = Vlong (Int64.add (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) lo)
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
 Proof.
-  intros v1 v2; unfold Val.divlu, Val.modlu.
-  destruct v1; try (intuition discriminate).
-  destruct v2; try (intuition discriminate).
-  predSpec Int64.eq Int64.eq_spec i0 Int64.zero ; try (intuition discriminate).
-  intros _. exists i, i0, (Int64.divu i i0), (Int64.modu i i0); intuition auto.
-  apply Int64.divmodu2_divu_modu; auto.
+  unfold load_hilo64; intros. 
+  predSpec Int64.eq Int64.eq_spec lo Int64.zero.
+- subst lo. econstructor; split. 
+  apply exec_straight_one. simpl; eauto. auto.
+  split. rewrite Int64.add_zero. Simpl.
+  intros; Simpl.
+- econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split. Simpl. 
+  intros; Simpl.
 Qed.
 
-Lemma divls_modls_exists:
-  forall v1 v2,
-  Val.divls v1 v2 <> None \/ Val.modls v1 v2 <> None ->
-  exists nh nl d q r,
-     Val.shrl v1 (Vint (Int.repr 63)) = Vlong nh /\ v1 = Vlong nl /\ v2 = Vlong d
-  /\ Int64.divmods2 nh nl d = Some(q, r)
-  /\ Val.divls v1 v2 = Some (Vlong q) /\ Val.modls v1 v2 = Some (Vlong r).
+Lemma loadimm64_correct:
+  forall rd n k rs m,
+  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 -> r <> X31 -> rs'#r = rs#r.
 Proof.
-  intros v1 v2; unfold Val.divls, Val.modls.
-  destruct v1; try (intuition discriminate).
-  destruct v2; try (intuition discriminate).
-  destruct (Int64.eq i0 Int64.zero
-            || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone) eqn:OK;
-  try (intuition discriminate).
-  intros _.
-  InvBooleans.
-  exists (Int64.shr i (Int64.repr 63)), i, i0, (Int64.divs i i0), (Int64.mods i i0); intuition auto.
-  rewrite Int64.shr_lt_zero. apply Int64.divmods2_divs_mods.
-  red; intros; subst i0; rewrite Int64.eq_true in H; discriminate.
-  revert H0. predSpec Int64.eq Int64.eq_spec i (Int64.repr Int64.min_signed); auto.
-  predSpec Int64.eq Int64.eq_spec i0 Int64.mone; auto.
-  discriminate.
+  unfold loadimm64; intros. generalize (make_immed64_sound n); intros E.
+  destruct (make_immed64 n). 
+- subst imm. econstructor; split. 
+  apply exec_straight_one. simpl; eauto. auto.
+  split. rewrite Int64.add_zero_l; Simpl. 
+  intros; Simpl.
+- exploit load_hilo64_correct; eauto. intros (rs' & A & B & C).
+  rewrite E. exists rs'; eauto.
+- subst imm. econstructor; split. 
+  apply exec_straight_one. simpl; eauto. auto.
+  split. Simpl. 
+  intros; Simpl.
 Qed.
 
-(** Smart constructor for [shrx] *)
-
-Lemma mk_shrximm_correct:
-  forall n k c (rs1: regset) v m,
-  mk_shrximm n k = OK c ->
-  Val.shrx (rs1#RAX) (Vint n) = Some v ->
-  exists rs2,
-     exec_straight ge fn c rs1 m k rs2 m
-  /\ rs2#RAX = v
-  /\ forall r, data_preg r = true -> r <> RAX -> r <> RCX -> rs2#r = rs1#r.
+Lemma opimm64_correct:
+  forall (op: ireg -> ireg0 -> ireg0 -> instruction)
+         (opi: ireg -> ireg0 -> int64 -> instruction)
+         (sem: val -> val -> val) m,
+  (forall d s1 s2 rs,
+   exec_instr ge fn (op d s1 s2) rs m = Next (nextinstr (rs#d <- (sem rs###s1 rs###s2))) m) ->
+  (forall d s n rs,
+   exec_instr ge fn (opi d s n) rs m = Next (nextinstr (rs#d <- (sem rs###s (Vlong n)))) m) ->
+  forall rd r1 n k rs,
+  r1 <> X31 ->
+  exists rs',
+     exec_straight ge fn (opimm64 op opi rd r1 n k) rs m k rs' m
+  /\ rs'#rd = sem rs##r1 (Vlong n)
+  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
 Proof.
-  unfold mk_shrximm; intros. inv H.
-  exploit Val.shrx_shr; eauto. intros [x [y [A [B C]]]].
-  inversion B; clear B; subst y; subst v; clear H0.
-  set (tnm1 := Int.sub (Int.shl Int.one n) Int.one).
-  set (x' := Int.add x tnm1).
-  set (rs2 := nextinstr (compare_ints (Vint x) (Vint Int.zero) rs1 m)).
-  set (rs3 := nextinstr (rs2#RCX <- (Vint x'))).
-  set (v' := if Int.lt x Int.zero then Vint x' else Vint x).
-  set (rs4 := nextinstr (rs3#RAX <- v')).
-  set (rs5 := nextinstr_nf (rs4#RAX <- (Val.shr rs4#RAX (Vint n)))).
-  assert (rs3#RAX = Vint x). unfold rs3. Simplifs.
-  assert (rs3#RCX = 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 RAX) with (rs1 RAX). rewrite A. simpl.
-  rewrite Int.repr_unsigned. rewrite Int.add_zero_l. auto. auto.
-  apply exec_straight_step with rs4 m. simpl.
-  rewrite Int.lt_sub_overflow. unfold rs4, v'. rewrite H, H0. destruct (Int.lt x Int.zero); simpl; auto.
-  auto.
-  apply exec_straight_one. auto. auto.
-  split. unfold rs5. Simplifs. unfold rs4. rewrite nextinstr_inv; auto with asmgen.
-  rewrite Pregmap.gss. unfold v'. rewrite A. reflexivity.
-  intros. unfold rs5. Simplifs. unfold rs4. Simplifs.
-  unfold rs3. Simplifs. unfold rs2. Simplifs.
-  unfold compare_ints. Simplifs.
+  intros. unfold opimm64. generalize (make_immed64_sound n); intros E.
+  destruct (make_immed64 n). 
+- subst imm. econstructor; split. 
+  apply exec_straight_one. rewrite H0. simpl; eauto. auto.
+  split. Simpl. intros; Simpl.
+- destruct (load_hilo64_correct X31 hi lo (op rd r1 X31 :: k) rs m)
+  as (rs' & A & B & C).
+  econstructor; split.
+  eapply exec_straight_trans. eexact A. apply exec_straight_one. 
+  rewrite H; eauto. auto.
+  split. Simpl. simpl. rewrite B, C, E. auto. congruence. congruence.
+  intros; Simpl. 
+- subst imm. econstructor; split. 
+  eapply exec_straight_two. simpl; eauto. rewrite H. simpl; eauto. auto. auto.
+  split. Simpl. intros; Simpl.
 Qed.
 
-(** Smart constructor for [shrxl] *)
+(** Add offset to pointer *)
 
-Lemma mk_shrxlimm_correct:
-  forall n k c (rs1: regset) v m,
-  mk_shrxlimm n k = OK c ->
-  Val.shrxl (rs1#RAX) (Vint n) = Some v ->
-  exists rs2,
-     exec_straight ge fn c rs1 m k rs2 m
-  /\ rs2#RAX = v
-  /\ forall r, data_preg r = true -> r <> RAX -> r <> RDX -> rs2#r = rs1#r.
+Lemma addptrofs_correct:
+  forall rd r1 n k rs m,
+  r1 <> X31 ->
+  exists rs',
+     exec_straight ge fn (addptrofs rd r1 n k) rs m k rs' m
+  /\ Val.lessdef (Val.offset_ptr rs#r1 n) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
 Proof.
-  unfold mk_shrxlimm; intros. exploit Val.shrxl_shrl_2; eauto. intros EQ.
-  destruct (Int.eq n Int.zero); inv H.
-- econstructor; split. apply exec_straight_one. simpl; reflexivity. auto.
-  split. Simplifs. intros; Simplifs.
-- set (v1 := Val.shrl (rs1 RAX) (Vint (Int.repr 63))) in *.
-  set (v2 := Val.shrlu v1 (Vint (Int.sub (Int.repr 64) n))) in *.
-  set (v3 := Val.addl (rs1 RAX) v2) in *.
-  set (v4 := Val.shrl v3 (Vint n)) in *.
-  set (rs2 := nextinstr_nf (rs1#RDX <- v1)).
-  set (rs3 := nextinstr_nf (rs2#RDX <- v2)).
-  set (rs4 := nextinstr (rs3#RAX <- v3)).
-  set (rs5 := nextinstr_nf (rs4#RAX <- v4)).
-  assert (X: forall v1 v2,
-             Val.addl v1 (Val.addl v2 (Vlong Int64.zero)) = Val.addl v1 v2).
-  { intros. unfold Val.addl; destruct Archi.ptr64 eqn:SF, v0; auto; destruct v5; auto.
-    rewrite Int64.add_zero; auto.
-    rewrite Ptrofs.add_zero; auto.
-    rewrite Int64.add_zero; auto.
-    rewrite Int64.add_zero; auto. }
-  exists rs5; split.
-  eapply exec_straight_trans with (rs2 := rs3).
-  eapply exec_straight_two with (rs2 := rs2); reflexivity.
-  eapply exec_straight_two with (rs2 := rs4).
-  simpl. rewrite X. reflexivity. reflexivity. reflexivity. reflexivity.
-  split. unfold rs5; Simplifs.
-  intros. unfold rs5; Simplifs. unfold rs4; Simplifs. unfold rs3; Simplifs. unfold rs2; Simplifs.
+  unfold addptrofs; intros.
+  destruct (Ptrofs.eq_dec n Ptrofs.zero).
+- subst n. econstructor; split.
+  apply exec_straight_one. simpl; eauto. auto.
+  split. Simpl. destruct (rs r1); simpl; auto. rewrite Ptrofs.add_zero; auto.
+  intros; Simpl.
+- destruct Archi.ptr64 eqn:SF.
++ unfold addimm64.
+  exploit (opimm64_correct Paddl Paddil Val.addl); eauto. intros (rs' & A & B & C).
+  exists rs'; split. eexact A. split; auto.
+  rewrite B. simpl. destruct (rs r1); simpl; auto. rewrite SF.
+  rewrite Ptrofs.of_int64_to_int64 by auto. auto.
++ unfold addimm32.
+  exploit (opimm32_correct Paddw Paddiw Val.add); eauto. intros (rs' & A & B & C).
+  exists rs'; split. eexact A. split; auto.
+  rewrite B. simpl. destruct (rs r1); simpl; auto. rewrite SF.
+  rewrite Ptrofs.of_int_to_int by auto. auto.
 Qed.
 
-(** Smart constructor for integer conversions *)
-
-Lemma mk_intconv_correct:
-  forall mk sem rd rs k c rs1 m,
-  mk_intconv mk rd rs k = OK c ->
-  (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 ge fn c rs1 m k rs2 m
-  /\ rs2#rd = sem rs1#rs
-  /\ forall r, data_preg r = true -> r <> rd -> r <> RAX -> rs2#r = rs1#r.
+Lemma addptrofs_correct_2:
+  forall rd r1 n k (rs: regset) m b ofs,
+  r1 <> X31 -> rs#r1 = Vptr b ofs ->
+  exists rs',
+     exec_straight ge fn (addptrofs rd r1 n k) rs m k rs' m
+  /\ rs'#rd = Vptr b (Ptrofs.add ofs n)
+  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
 Proof.
-  unfold mk_intconv; intros. destruct (Archi.ptr64 || low_ireg rs); monadInv H.
-  econstructor. split. apply exec_straight_one. rewrite H0. eauto. auto.
-  split. Simplifs. intros. Simplifs.
-  econstructor. split. eapply exec_straight_two.
-  simpl. eauto. apply H0. auto. auto.
-  split. Simplifs. intros. Simplifs.
+  intros. exploit (addptrofs_correct rd r1 n); eauto. intros (rs' & A & B & C).
+  exists rs'; intuition eauto. 
+  rewrite H0 in B. inv B. auto.
 Qed.
 
-(** Smart constructor for small stores *)
+(** Translation of conditional branches *)
 
-Lemma addressing_mentions_correct:
-  forall a r (rs1 rs2: regset),
-  (forall (r': ireg), r' <> r -> rs1 r' = rs2 r') ->
-  addressing_mentions a r = false ->
-  eval_addrmode32 ge a rs1 = eval_addrmode32 ge a rs2.
+Lemma transl_cbranch_int32s_correct:
+  forall cmp r1 r2 lbl (rs: regset) m b,
+  Val.cmp_bool cmp rs##r1 rs##r2 = Some b ->
+  exec_instr ge fn (transl_cbranch_int32s cmp r1 r2 lbl) rs m =
+  eval_branch fn lbl rs m (Some b).
 Proof.
-  intros until rs2; intro AG. unfold addressing_mentions, eval_addrmode32.
-  destruct a. intros. destruct (orb_false_elim _ _ H). unfold proj_sumbool in *.
-  decEq. destruct base; auto. apply AG. destruct (ireg_eq r i); congruence.
-  decEq. destruct ofs as [[r' sc] | ]; auto. rewrite AG; auto. destruct (ireg_eq r r'); congruence.
+  intros. destruct cmp; simpl; rewrite ? H.
+- destruct rs##r1; simpl in H; try discriminate. destruct rs##r2; inv H.
+  simpl; auto.
+- destruct rs##r1; simpl in H; try discriminate. destruct rs##r2; inv H.
+  simpl; auto.
+- auto.
+- rewrite <- Val.swap_cmp_bool. simpl. rewrite H; auto.
+- rewrite <- Val.swap_cmp_bool. simpl. rewrite H; auto.
+- auto.
 Qed.
 
-Lemma mk_storebyte_correct:
-  forall addr r k c rs1 m1 m2,
-  mk_storebyte addr r k = OK c ->
-  Mem.storev Mint8unsigned m1 (eval_addrmode ge addr rs1) (rs1 r) = Some m2 ->
-  exists rs2,
-     exec_straight ge fn c rs1 m1 k rs2 m2
-  /\ forall r, data_preg r = true -> preg_notin r (if Archi.ptr64 then nil else AX :: CX :: nil) -> rs2#r = rs1#r.
+Lemma transl_cbranch_int32u_correct:
+  forall cmp r1 r2 lbl (rs: regset) m b,
+  Val.cmpu_bool (Mem.valid_pointer m) cmp rs##r1 rs##r2 = Some b ->
+  exec_instr ge fn (transl_cbranch_int32u cmp r1 r2 lbl) rs m =
+  eval_branch fn lbl rs m (Some b).
 Proof.
-  unfold mk_storebyte; intros.
-  destruct (Archi.ptr64 || low_ireg r) eqn:E.
-(* low reg *)
-  monadInv H. econstructor; split. apply exec_straight_one.
-  simpl. unfold exec_store. rewrite H0. eauto. auto.
-  intros; Simplifs.
-(* high reg *)
-  InvBooleans. rewrite H1; simpl. destruct (addressing_mentions addr RAX) eqn:E; monadInv H.
-(* RAX is mentioned. *)
-  assert (r <> RCX). { red; intros; subst r; discriminate H2. }
-  set (rs2 := nextinstr (rs1#RCX <- (eval_addrmode32 ge addr rs1))).
-  set (rs3 := nextinstr (rs2#RAX <- (rs1 r))).
-  econstructor; split.
-  apply exec_straight_three with rs2 m1 rs3 m1.
-  simpl. auto.
-  simpl. replace (rs2 r) with (rs1 r). auto. symmetry. unfold rs2; Simplifs.
-  simpl. unfold exec_store. unfold eval_addrmode; rewrite H1; simpl. rewrite Int.add_zero.
-  change (rs3 RAX) with (rs1 r).
-  change (rs3 RCX) with (eval_addrmode32 ge addr rs1).
-  replace (Val.add (eval_addrmode32 ge addr rs1) (Vint Int.zero))
-     with (eval_addrmode ge addr rs1).
-  rewrite H0. eauto.
-  unfold eval_addrmode in *; rewrite H1 in *.
-  destruct (eval_addrmode32 ge addr rs1); simpl in H0; try discriminate H0.
-  simpl. rewrite H1. rewrite Ptrofs.add_zero; auto.
-  auto. auto. auto.
-  intros. destruct H4. Simplifs. unfold rs3; Simplifs. unfold rs2; Simplifs.
-(* RAX is not mentioned *)
-  set (rs2 := nextinstr (rs1#RAX <- (rs1 r))).
-  econstructor; split.
-  apply exec_straight_two with rs2 m1.
-  simpl. auto.
-  simpl. unfold exec_store. unfold eval_addrmode in *; rewrite H1 in *.
-  rewrite (addressing_mentions_correct addr RAX rs2 rs1); auto.
-  change (rs2 RAX) with (rs1 r). rewrite H0. eauto.
-  intros. unfold rs2; Simplifs.
-  auto. auto.
-  intros. destruct H3. simpl. Simplifs. unfold rs2; Simplifs.
+  intros. destruct cmp; simpl; rewrite ? H; auto.
+- rewrite <- Val.swap_cmpu_bool. simpl. rewrite H; auto.
+- rewrite <- Val.swap_cmpu_bool. simpl. rewrite H; auto.
 Qed.
 
-(** Accessing slots in the stack frame *)
-
-Remark eval_addrmode_indexed:
-  forall (base: ireg) ofs (rs: regset),
-  match rs#base with Vptr _ _ => True | _ => False end ->
-  eval_addrmode ge (Addrmode (Some base) None (inl _ (Ptrofs.unsigned ofs))) rs = Val.offset_ptr rs#base ofs.
+Lemma transl_cbranch_int64s_correct:
+  forall cmp r1 r2 lbl (rs: regset) m b,
+  Val.cmpl_bool cmp rs###r1 rs###r2 = Some b ->
+  exec_instr ge fn (transl_cbranch_int64s cmp r1 r2 lbl) rs m =
+  eval_branch fn lbl rs m (Some b).
 Proof.
-  intros. destruct (rs#base) eqn:BASE; try contradiction.
-  intros; unfold eval_addrmode; destruct Archi.ptr64 eqn:SF; simpl; rewrite BASE; simpl; rewrite SF; simpl.
-- apply f_equal. apply f_equal. rewrite Int64.add_zero_l. rewrite <- (Ptrofs.repr_unsigned ofs) at 2. auto with ptrofs.
--  apply f_equal. apply f_equal. rewrite Int.add_zero_l. rewrite <- (Ptrofs.repr_unsigned ofs) at 2. auto with ptrofs.
+  intros. destruct cmp; simpl; rewrite ? H.
+- destruct rs###r1; simpl in H; try discriminate. destruct rs###r2; inv H.
+  simpl; auto.
+- destruct rs###r1; simpl in H; try discriminate. destruct rs###r2; inv H.
+  simpl; auto.
+- auto.
+- rewrite <- Val.swap_cmpl_bool. simpl. rewrite H; auto.
+- rewrite <- Val.swap_cmpl_bool. simpl. rewrite H; auto.
+- auto.
 Qed.
 
-Ltac loadind_correct_solve :=
-  match goal with
-  | H: Error _ = OK _ |- _ => discriminate H
-  | H: OK _ = OK _ |- _ => inv H
-  | H: match ?x with _ => _ end = OK _ |- _ => destruct x eqn:?; loadind_correct_solve
-  | _ => idtac
-  end.
-
-Lemma loadind_correct:
-  forall (base: ireg) ofs ty dst k (rs: regset) c m v,
-  loadind base ofs ty dst k = OK c ->
-  Mem.loadv (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) = Some 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.
+Lemma transl_cbranch_int64u_correct:
+  forall cmp r1 r2 lbl (rs: regset) m b,
+  Val.cmplu_bool (Mem.valid_pointer m) cmp rs###r1 rs###r2 = Some b ->
+  exec_instr ge fn (transl_cbranch_int64u cmp r1 r2 lbl) rs m =
+  eval_branch fn lbl rs m (Some b).
 Proof.
-  unfold loadind; intros.
-  set (addr := Addrmode (Some base) None (inl (ident * ptrofs) (Ptrofs.unsigned ofs))) in *.
-  assert (eval_addrmode ge addr rs = Val.offset_ptr rs#base ofs).
-  { apply eval_addrmode_indexed. destruct (rs base); auto || discriminate. }
-  rewrite <- H1 in H0.
-  exists (nextinstr_nf (rs#(preg_of dst) <- v)); split.
-- loadind_correct_solve; apply exec_straight_one; auto; simpl in *; unfold exec_load; rewrite ?Heqb, ?H0; auto.
-- intuition Simplifs.
+  intros. destruct cmp; simpl; rewrite ? H; auto.
+- rewrite <- Val.swap_cmplu_bool. simpl. rewrite H; auto.
+- rewrite <- Val.swap_cmplu_bool. simpl. rewrite H; auto.
 Qed.
 
-Lemma storeind_correct:
-  forall (base: ireg) ofs ty src k (rs: regset) c m m',
-  storeind src base ofs ty k = OK c ->
-  Mem.storev (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) (rs#(preg_of src)) = Some m' ->
-  exists rs',
-     exec_straight ge fn c rs m k rs' m'
-  /\ forall r, data_preg r = true -> preg_notin r (destroyed_by_setstack ty) -> rs'#r = rs#r.
+Lemma transl_cond_float_correct:
+  forall (rs: regset) m cmp rd r1 r2 insn normal v,
+  transl_cond_float cmp rd r1 r2 = (insn, normal) ->
+  v = (if normal then Val.cmpf cmp rs#r1 rs#r2 else Val.notbool (Val.cmpf cmp rs#r1 rs#r2)) ->
+  exec_instr ge fn insn rs m = Next (nextinstr (rs#rd <- v)) m.
 Proof.
-  unfold storeind; intros.
-  set (addr := Addrmode (Some base) None (inl (ident * ptrofs) (Ptrofs.unsigned ofs))) in *.
-  assert (eval_addrmode ge addr rs = Val.offset_ptr rs#base ofs).
-  { apply eval_addrmode_indexed. destruct (rs base); auto || discriminate. }
-  rewrite <- H1 in H0.
-  loadind_correct_solve; simpl in H0;
-  (econstructor; split;
-  [apply exec_straight_one; [simpl; unfold exec_store; rewrite ?Heqb, H0;eauto|auto]
-  |simpl; intros; unfold undef_regs; repeat Simplifs]).
+  intros. destruct cmp; simpl in H; inv H; auto. 
+- rewrite Val.negate_cmpf_eq. auto.
+- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpf, Val.cmpf_bool.
+  rewrite <- Float.cmp_swap. auto.
+- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpf, Val.cmpf_bool.
+  rewrite <- Float.cmp_swap. auto.
 Qed.
 
-(** Translation of addressing modes *)
-
-Lemma transl_addressing_mode_32_correct:
-  forall addr args am (rs: regset) v,
-  transl_addressing addr args = OK am ->
-  eval_addressing32 ge (rs RSP) addr (List.map rs (List.map preg_of args)) = Some v ->
-  Val.lessdef v (eval_addrmode32 ge am rs).
+Lemma transl_cond_single_correct:
+  forall (rs: regset) m cmp rd r1 r2 insn normal v,
+  transl_cond_single cmp rd r1 r2 = (insn, normal) ->
+  v = (if normal then Val.cmpfs cmp rs#r1 rs#r2 else Val.notbool (Val.cmpfs cmp rs#r1 rs#r2)) ->
+  exec_instr ge fn insn rs m = Next (nextinstr (rs#rd <- v)) m.
 Proof.
-  assert (A: forall id ofs, Archi.ptr64 = false ->
-          Val.add (Vint Int.zero) (Genv.symbol_address ge id ofs) = Genv.symbol_address ge id ofs).
-  { intros. unfold Val.add; rewrite H. unfold Genv.symbol_address.
-    destruct (Genv.find_symbol ge id); auto. rewrite Ptrofs.add_zero; auto. }
-  assert (C: forall v i,
-    Val.lessdef (Val.mul v (Vint (Int.repr i)))
-               (if zeq i 1 then v else Val.mul v (Vint (Int.repr i)))).
-  { intros. destruct (zeq i 1); subst; auto.
-    destruct v; simpl; auto. rewrite Int.mul_one; auto. }
-  unfold transl_addressing; intros.
-  destruct addr; repeat (destruct args; try discriminate H); simpl in H0; FuncInv;
-  monadInv H; try (erewrite ! ireg_of_eq by eauto); unfold eval_addrmode32.
-- simpl; rewrite Int.add_zero_l; auto.
-- rewrite Val.add_assoc. apply Val.add_lessdef; auto.
-- rewrite Val.add_permut. apply Val.add_lessdef; auto. simpl; rewrite Int.add_zero_l; auto.
-- apply Val.add_lessdef; auto. apply Val.add_lessdef; auto.
-- rewrite ! A by auto. auto.
-- rewrite Val.add_commut. rewrite A by auto. auto.
-- rewrite Val.add_permut. rewrite Val.add_commut. apply Val.add_lessdef; auto. rewrite A; auto.
-- simpl. unfold Val.add; rewrite Heqb.
-  destruct (rs RSP); simpl; auto.
-  rewrite Int.add_zero_l. apply Val.lessdef_same; f_equal; f_equal.
-  symmetry. transitivity (Ptrofs.repr (Ptrofs.signed i)). auto with ptrofs. auto with ints.
-Qed.
-
-Lemma transl_addressing_mode_64_correct:
-  forall addr args am (rs: regset) v,
-  transl_addressing addr args = OK am ->
-  eval_addressing64 ge (rs RSP) addr (List.map rs (List.map preg_of args)) = Some v ->
-  Val.lessdef v (eval_addrmode64 ge am rs).
+  intros. destruct cmp; simpl in H; inv H; auto. 
+- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool.
+  rewrite Float32.cmp_ne_eq. destruct (Float32.cmp Ceq f0 f); auto.
+- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool.
+  rewrite <- Float32.cmp_swap. auto.
+- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool.
+  rewrite <- Float32.cmp_swap. auto.
+   Qed.
+
+(* TODO gourdinl UNUSUED ? Remark branch_on_X31:
+  forall normal lbl (rs: regset) m b,
+  rs#X31 = Val.of_bool (eqb normal b) -> 
+  exec_instr ge fn (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) rs m =
+  eval_branch fn lbl rs m (Some b).
 Proof.
-  assert (A: forall id ofs, Archi.ptr64 = true ->
-          Val.addl (Vlong Int64.zero) (Genv.symbol_address ge id ofs) = Genv.symbol_address ge id ofs).
-  { intros. unfold Val.addl; rewrite H. unfold Genv.symbol_address.
-    destruct (Genv.find_symbol ge id); auto. rewrite Ptrofs.add_zero; auto. }
-  assert (C: forall v i,
-    Val.lessdef (Val.mull v (Vlong (Int64.repr i)))
-               (if zeq i 1 then v else Val.mull v (Vlong (Int64.repr i)))).
-  { intros. destruct (zeq i 1); subst; auto.
-    destruct v; simpl; auto. rewrite Int64.mul_one; auto. }
-  unfold transl_addressing; intros.
-  destruct addr; repeat (destruct args; try discriminate H); simpl in H0; FuncInv;
-  monadInv H; try (erewrite ! ireg_of_eq by eauto); unfold eval_addrmode64.
-- simpl; rewrite Int64.add_zero_l; auto.
-- rewrite Val.addl_assoc. apply Val.addl_lessdef; auto.
-- rewrite Val.addl_permut. apply Val.addl_lessdef; auto. simpl; rewrite Int64.add_zero_l; auto.
-- apply Val.addl_lessdef; auto. apply Val.addl_lessdef; auto.
-- rewrite ! A by auto. auto.
-- unfold Val.addl; rewrite Heqb. destruct (rs RSP); auto. simpl.
-  rewrite Int64.add_zero_l. apply Val.lessdef_same; f_equal; f_equal.
-  symmetry. transitivity (Ptrofs.repr (Ptrofs.signed i)). auto with ptrofs. auto with ints.
-Qed.
+  intros. destruct normal; simpl; rewrite H; simpl; destruct b; reflexivity. 
+   Qed.*)
 
-Lemma transl_addressing_mode_correct:
-  forall addr args am (rs: regset) v,
-  transl_addressing addr args = OK am ->
-  eval_addressing ge (rs RSP) addr (List.map rs (List.map preg_of args)) = Some v ->
-  Val.lessdef v (eval_addrmode ge am rs).
+Ltac ArgsInv :=
+  repeat (match goal with
+  | [ H: Error _ = OK _ |- _ ] => discriminate
+  | [ H: match ?args with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct args
+  | [ H: bind _ _ = OK _ |- _ ] => monadInv H
+  | [ H: match _ with left _ => _ | right _ => assertion_failed end = OK _ |- _ ] => monadInv H; ArgsInv
+  | [ H: match _ with true => _ | false => assertion_failed end = OK _ |- _ ] => monadInv H; ArgsInv
+  end);
+  subst;
+  repeat (match goal with
+  | [ H: ireg_of _ = OK _ |- _ ] => simpl in *; rewrite (ireg_of_eq _ _ H) in *
+  | [ H: freg_of _ = OK _ |- _ ] => simpl in *; rewrite (freg_of_eq _ _ H) in *
+  end).
+
+Lemma transl_cbranch_correct_1:
+  forall cond args lbl k c m ms b sp rs m',
+  transl_cbranch cond args lbl k = OK c ->
+  eval_condition cond (List.map ms args) m = Some b ->
+  agree ms sp rs ->
+  Mem.extends m m' ->
+  exists rs', exists insn,
+     exec_straight_opt ge fn c rs m' (insn :: k) rs' m'
+  /\ exec_instr ge fn insn rs' m' = eval_branch fn lbl rs' m' (Some b)
+  /\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r.
 Proof.
-  unfold eval_addressing, eval_addrmode; intros. destruct Archi.ptr64.
-  eapply transl_addressing_mode_64_correct; eauto.
-  eapply transl_addressing_mode_32_correct; eauto.
+  intros until m'; intros TRANSL EVAL AG MEXT.
+  set (vl' := map rs (map preg_of args)). 
+  assert (EVAL': eval_condition cond vl' m' = Some b).
+  { apply eval_condition_lessdef with (map ms args) m; auto. eapply preg_vals; eauto. }
+  clear EVAL MEXT AG.
+  destruct cond; simpl in TRANSL; ArgsInv.
+  - exists rs, (transl_cbranch_int32s c0 x x0 lbl).
+  intuition auto. constructor. apply transl_cbranch_int32s_correct; auto.
+- exists rs, (transl_cbranch_int32u c0 x x0 lbl).
+  intuition auto. constructor. apply transl_cbranch_int32u_correct; auto.
+- predSpec Int.eq Int.eq_spec n Int.zero.
++ subst n. exists rs, (transl_cbranch_int32s c0 x X0 lbl).
+  intuition auto. constructor. apply transl_cbranch_int32s_correct; auto.
++ exploit (loadimm32_correct X31 n); eauto. intros (rs' & A & B & C).
+  exists rs', (transl_cbranch_int32s c0 x X31 lbl).
+  split. constructor; eexact A. split; auto.
+  apply transl_cbranch_int32s_correct; auto.
+  simpl; rewrite B, C; eauto with asmgen.
+- predSpec Int.eq Int.eq_spec n Int.zero.
++ subst n. exists rs, (transl_cbranch_int32u c0 x X0 lbl).
+  intuition auto. constructor. apply transl_cbranch_int32u_correct; auto.
++ exploit (loadimm32_correct X31 n); eauto. intros (rs' & A & B & C).
+  exists rs', (transl_cbranch_int32u c0 x X31 lbl).
+  split. constructor; eexact A. split; auto.
+  apply transl_cbranch_int32u_correct; auto.
+  simpl; rewrite B, C; eauto with asmgen.
+- exists rs, (transl_cbranch_int64s c0 x x0 lbl).
+  intuition auto. constructor. apply transl_cbranch_int64s_correct; auto.
+- exists rs, (transl_cbranch_int64u c0 x x0 lbl).
+  intuition auto. constructor. apply transl_cbranch_int64u_correct; auto.
+- predSpec Int64.eq Int64.eq_spec n Int64.zero.
++ subst n. exists rs, (transl_cbranch_int64s c0 x X0 lbl).
+  intuition auto. constructor. apply transl_cbranch_int64s_correct; auto.
++ exploit (loadimm64_correct X31 n); eauto. intros (rs' & A & B & C).
+  exists rs', (transl_cbranch_int64s c0 x X31 lbl).
+  split. constructor; eexact A. split; auto.
+  apply transl_cbranch_int64s_correct; auto.
+  simpl; rewrite B, C; eauto with asmgen.
+- predSpec Int64.eq Int64.eq_spec n Int64.zero.
++ subst n. exists rs, (transl_cbranch_int64u c0 x X0 lbl).
+  intuition auto. constructor. apply transl_cbranch_int64u_correct; auto.
++ exploit (loadimm64_correct X31 n); eauto. intros (rs' & A & B & C).
+  exists rs', (transl_cbranch_int64u c0 x X31 lbl).
+  split. constructor; eexact A. split; auto.
+  apply transl_cbranch_int64u_correct; auto.
+  simpl; rewrite B, C; eauto with asmgen.
+- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2.
+  set (v := if normal then Val.cmpf c0 rs#x rs#x0 else Val.notbool (Val.cmpf c0 rs#x rs#x0)).
+  assert (V: v = Val.of_bool (eqb normal b)).
+  { unfold v, Val.cmpf. rewrite EVAL'. destruct normal, b; reflexivity. }
+  econstructor; econstructor.
+  split. constructor. apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto.
+  split. rewrite V; destruct normal, b; reflexivity.
+  intros; Simpl.
+- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2.
+  assert (EVAL'': Val.cmpf_bool c0 (rs x) (rs x0) = Some (negb b)).
+  { destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; inv EVAL'; auto. }
+  set (v := if normal then Val.cmpf c0 rs#x rs#x0 else Val.notbool (Val.cmpf c0 rs#x rs#x0)).
+  assert (V: v = Val.of_bool (xorb normal b)).
+  { unfold v, Val.cmpf. rewrite EVAL''. destruct normal, b; reflexivity. }
+  econstructor; econstructor.
+  split. constructor. apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto.
+  split. rewrite V; destruct normal, b; reflexivity.
+  intros; Simpl.
+- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2.
+  set (v := if normal then Val.cmpfs c0 rs#x rs#x0 else Val.notbool (Val.cmpfs c0 rs#x rs#x0)).
+  assert (V: v = Val.of_bool (eqb normal b)).
+  { unfold v, Val.cmpfs. rewrite EVAL'. destruct normal, b; reflexivity. }
+  econstructor; econstructor.
+  split. constructor. apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto.
+  split. rewrite V; destruct normal, b; reflexivity.
+  intros; Simpl.
+- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2.
+  assert (EVAL'': Val.cmpfs_bool c0 (rs x) (rs x0) = Some (negb b)).
+  { destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; inv EVAL'; auto. }
+  set (v := if normal then Val.cmpfs c0 rs#x rs#x0 else Val.notbool (Val.cmpfs c0 rs#x rs#x0)).
+  assert (V: v = Val.of_bool (xorb normal b)).
+  { unfold v, Val.cmpfs. rewrite EVAL''. destruct normal, b; reflexivity. }
+  econstructor; econstructor.
+  split. constructor. apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto.
+  split. rewrite V; destruct normal, b; reflexivity.
+     intros; Simpl.
+
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *;
+  destruct (rs x) eqn:EQRS; simpl in *; try congruence;
+  inv EQ2; eexists; eexists; eauto; split; constructor; auto;
+  simpl in *.
+  + rewrite EQRS;
+    assert (HB: (Int.eq Int.zero i) = b) by congruence.
+    rewrite HB; destruct b; simpl; auto.
+  + rewrite EQRS;
+    assert (HB: (Int.eq i Int.zero) = b) by congruence.
+    rewrite <- HB; destruct b; simpl; auto.
+  + rewrite EQRS;
+    destruct (rs x0); try congruence.
+    assert (HB: (Int.eq i i0) = b) by congruence.
+    rewrite <- HB; destruct b; simpl; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *;
+  destruct (rs x) eqn:EQRS; simpl in *; try congruence;
+  inv EQ2; eexists; eexists; eauto; split; constructor; auto;
+  simpl in *.
+  + rewrite EQRS;
+    assert (HB: negb (Int.eq Int.zero i) = b) by congruence.
+    rewrite HB; destruct b; simpl; auto.
+  + rewrite EQRS;
+    assert (HB: negb (Int.eq i Int.zero) = b) by congruence.
+    rewrite <- HB; destruct b; simpl; auto.
+  + rewrite EQRS;
+    destruct (rs x0); try congruence.
+    assert (HB: negb (Int.eq i i0) = b) by congruence.
+    rewrite <- HB; destruct b; simpl; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *; inv EQ2;
+  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *; inv EQ2;
+  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *; inv EQ2;
+  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *; inv EQ2;
+  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *; inv EQ2;
+  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *; inv EQ2;
+  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *; inv EQ2;
+  destruct (rs x) eqn:EQRS; simpl in *; try congruence;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; auto.
+  + rewrite EQRS;
+    assert (HB: (Int64.eq Int64.zero i) = b) by congruence.
+    rewrite HB; destruct b; simpl; auto.
+  + rewrite EQRS;
+    assert (HB: (Int64.eq i Int64.zero) = b) by congruence.
+    rewrite <- HB; destruct b; simpl; auto.
+  + rewrite EQRS;
+    destruct (rs x0); try congruence.
+    assert (HB: (Int64.eq i i0) = b) by congruence.
+    rewrite <- HB; destruct b; simpl; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *; inv EQ2;
+  destruct (rs x) eqn:EQRS; simpl in *; try congruence;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; auto.
+  + rewrite EQRS;
+    assert (HB: negb (Int64.eq Int64.zero i) = b) by congruence.
+    rewrite HB; destruct b; simpl; auto.
+  + rewrite EQRS;
+    assert (HB: negb (Int64.eq i Int64.zero) = b) by congruence.
+    rewrite <- HB; destruct b; simpl; auto.
+  + rewrite EQRS;
+    destruct (rs x0); try congruence.
+    assert (HB: negb (Int64.eq i i0) = b) by congruence.
+    rewrite <- HB; destruct b; simpl; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
+  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
+  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
+  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
+  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
+  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
+  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
 Qed.
 
-Lemma normalize_addrmode_32_correct:
-  forall am rs, eval_addrmode32 ge (normalize_addrmode_32 am) rs = eval_addrmode32 ge am rs.
+Lemma transl_cbranch_correct_true:
+  forall cond args lbl k c m ms sp rs m',
+  transl_cbranch cond args lbl k = OK c ->
+  eval_condition cond (List.map ms args) m = Some true ->
+  agree ms sp rs ->
+  Mem.extends m m' ->
+  exists rs', exists insn,
+     exec_straight_opt ge fn c rs m' (insn :: k) rs' m'
+  /\ exec_instr ge fn insn rs' m' = goto_label fn lbl rs' m'
+  /\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r.
 Proof.
-  intros; destruct am as [base ofs [n|r]]; simpl; auto. rewrite Int.repr_signed. auto.
-Qed.
-
-Lemma normalize_addrmode_64_correct:
-  forall am rs,
-  eval_addrmode64 ge am rs =
-  match normalize_addrmode_64 am with
-  | (am', None) => eval_addrmode64 ge am' rs
-  | (am', Some delta) => Val.addl (eval_addrmode64 ge am' rs) (Vlong delta)
-  end.
+  intros. eapply transl_cbranch_correct_1 with (b := true); eauto.
+Qed. 
+
+Lemma transl_cbranch_correct_false:
+  forall cond args lbl k c m ms sp rs m',
+  transl_cbranch cond args lbl k = OK c ->
+  eval_condition cond (List.map ms args) m = Some false ->
+  agree ms sp rs ->
+  Mem.extends m m' ->
+  exists rs',
+     exec_straight ge fn c rs m' k rs' m'
+  /\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r.
 Proof.
-  intros; destruct am as [base ofs [n|[id delta]]]; simpl.
-- destruct (offset_in_range n); auto; simpl.
-  rewrite ! Val.addl_assoc. apply f_equal. apply f_equal. simpl. rewrite Int64.add_zero_l; auto.
-- destruct Archi.ptr64 eqn:SF; auto; simpl;
-  destruct (ptroffset_in_range delta); auto. simpl.
-  rewrite ! Val.addl_assoc. apply f_equal. apply f_equal.
-  rewrite <- Genv.shift_symbol_address_64 by auto.
-  f_equal. rewrite Ptrofs.add_zero_l, Ptrofs.of_int64_to_int64 by auto. auto.
+  intros. exploit transl_cbranch_correct_1; eauto. simpl. 
+  intros (rs' & insn & A & B & C).
+  exists (nextinstr rs').
+  split. eapply exec_straight_opt_right; eauto. apply exec_straight_one; auto.
+  intros; Simpl. 
 Qed.
 
-(** Processor conditions and comparisons *)
+(** Translation of condition operators *)
 
-Lemma compare_ints_spec:
-  forall rs v1 v2 m,
-  let rs' := nextinstr (compare_ints v1 v2 rs m) in
-     rs'#ZF = Val.cmpu (Mem.valid_pointer m) Ceq v1 v2
-  /\ rs'#CF = Val.cmpu (Mem.valid_pointer m) Clt v1 v2
-  /\ rs'#SF = Val.negative (Val.sub v1 v2)
-  /\ rs'#OF = Val.sub_overflow v1 v2
-  /\ (forall r, data_preg r = true -> rs'#r = rs#r).
+Lemma transl_cond_int32s_correct:
+  forall cmp rd r1 r2 k rs m,
+  exists rs',
+     exec_straight ge fn (transl_cond_int32s cmp rd r1 r2 k) rs m k rs' m
+  /\ Val.lessdef (Val.cmp cmp rs##r1 rs##r2) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
 Proof.
-  intros. unfold rs'; unfold compare_ints.
-  split. auto.
-  split. auto.
-  split. auto.
-  split. auto.
-  intros. Simplifs.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split; intros; Simpl. unfold Val.cmp. rewrite <- Val.swap_cmp_bool.
+  simpl. rewrite (Val.negate_cmp_bool Clt). 
+  destruct (Val.cmp_bool Clt rs##r2 rs##r1) as [[]|]; auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl. unfold Val.cmp. rewrite <- Val.swap_cmp_bool. auto.
+- econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split; intros; Simpl. unfold Val.cmp. rewrite (Val.negate_cmp_bool Clt). 
+  destruct (Val.cmp_bool Clt rs##r1 rs##r2) as [[]|]; auto.
 Qed.
 
-Lemma testcond_for_signed_comparison_32_correct:
-  forall c v1 v2 rs m b,
-  Val.cmp_bool c v1 v2 = Some b ->
-  eval_testcond (testcond_for_signed_comparison c)
-                (nextinstr (compare_ints v1 v2 rs m)) = Some b.
+Lemma transl_cond_int32u_correct:
+  forall cmp rd r1 r2 k rs m,
+  exists rs',
+     exec_straight ge fn (transl_cond_int32u cmp rd r1 r2 k) rs m k rs' m
+  /\ rs'#rd = Val.cmpu (Mem.valid_pointer m) cmp rs##r1 rs##r2
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
 Proof.
-  intros. generalize (compare_ints_spec rs v1 v2 m).
-  set (rs' := nextinstr (compare_ints v1 v2 rs m)).
-  intros [A [B [C [D E]]]].
-  destruct v1; destruct v2; simpl in H; inv H.
-  unfold eval_testcond. rewrite A; rewrite B; rewrite C; rewrite D.
-  simpl. unfold Val.cmp, Val.cmpu.
-  rewrite Int.lt_sub_overflow.
-  destruct c; simpl.
-  destruct (Int.eq i i0); auto.
-  destruct (Int.eq i i0); auto.
-  destruct (Int.lt i i0); auto.
-  rewrite Int.not_lt. destruct (Int.lt i i0); simpl; destruct (Int.eq i i0); auto.
-  rewrite (Int.lt_not i i0). destruct (Int.lt i i0); destruct (Int.eq i i0); reflexivity.
-  destruct (Int.lt i i0); reflexivity.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split; intros; Simpl. unfold Val.cmpu. rewrite <- Val.swap_cmpu_bool.
+  simpl. rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Cle). 
+  destruct (Val.cmpu_bool (Mem.valid_pointer m) Cle rs##r1 rs##r2) as [[]|]; auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl. unfold Val.cmpu. rewrite <- Val.swap_cmpu_bool. auto.
+- econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split; intros; Simpl. unfold Val.cmpu. rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Clt). 
+  destruct (Val.cmpu_bool (Mem.valid_pointer m) Clt rs##r1 rs##r2) as [[]|]; auto.
 Qed.
 
-Lemma testcond_for_unsigned_comparison_32_correct:
-  forall c v1 v2 rs m b,
-  Val.cmpu_bool (Mem.valid_pointer m) c v1 v2 = Some b ->
-  eval_testcond (testcond_for_unsigned_comparison c)
-                (nextinstr (compare_ints v1 v2 rs m)) = Some b.
+Lemma transl_cond_int64s_correct:
+  forall cmp rd r1 r2 k rs m,
+  exists rs',
+     exec_straight ge fn (transl_cond_int64s cmp rd r1 r2 k) rs m k rs' m
+  /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs###r1 rs###r2)) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
 Proof.
-  intros. generalize (compare_ints_spec rs v1 v2 m).
-  set (rs' := nextinstr (compare_ints v1 v2 rs m)).
-  intros [A [B [C [D E]]]].
-  unfold eval_testcond. rewrite A; rewrite B. unfold Val.cmpu, Val.cmp.
-  destruct v1; destruct v2; simpl in H; FuncInv; subst.
-- (* int int *)
-  destruct c; simpl; auto.
-  destruct (Int.eq i i0); reflexivity.
-  destruct (Int.eq i i0); auto.
-  destruct (Int.ltu i i0); auto.
-  rewrite Int.not_ltu. destruct (Int.ltu i i0); simpl; destruct (Int.eq i i0); auto.
-  rewrite (Int.ltu_not i i0). destruct (Int.ltu i i0); destruct (Int.eq i i0); reflexivity.
-  destruct (Int.ltu i i0); reflexivity.
-- (* int ptr *)
-  unfold Val.cmpu_bool; rewrite Heqb1.
-  destruct (Int.eq i Int.zero &&
-    (Mem.valid_pointer m b0 (Ptrofs.unsigned i0) || Mem.valid_pointer m b0 (Ptrofs.unsigned i0 - 1))); try discriminate H.
-  destruct c; simpl in *; inv H; reflexivity.
-- (* ptr int *)
-  unfold Val.cmpu_bool; rewrite Heqb1.
-  destruct (Int.eq i0 Int.zero &&
-    (Mem.valid_pointer m b0 (Ptrofs.unsigned i) || Mem.valid_pointer m b0 (Ptrofs.unsigned i - 1))); try discriminate H.
-  destruct c; simpl in *; inv H; reflexivity.
-- (* ptr ptr *)
-  unfold Val.cmpu_bool; rewrite Heqb2.
-  fold (Mem.weak_valid_pointer m b0 (Ptrofs.unsigned i)) in *.
-  fold (Mem.weak_valid_pointer m b1 (Ptrofs.unsigned i0)) in *.
-  destruct (eq_block b0 b1).
-  destruct (Mem.weak_valid_pointer m b0 (Ptrofs.unsigned i) &&
-            Mem.weak_valid_pointer m b1 (Ptrofs.unsigned i0)); inv H.
-  destruct c; simpl; auto.
-  destruct (Ptrofs.eq i i0); auto.
-  destruct (Ptrofs.eq i i0); auto.
-  destruct (Ptrofs.ltu i i0); auto.
-  rewrite Ptrofs.not_ltu. destruct (Ptrofs.ltu i i0); simpl; destruct (Ptrofs.eq i i0); auto.
-  rewrite (Ptrofs.ltu_not i i0). destruct (Ptrofs.ltu i i0); destruct (Ptrofs.eq i i0); reflexivity.
-  destruct (Ptrofs.ltu i i0); reflexivity.
-  destruct (Mem.valid_pointer m b0 (Ptrofs.unsigned i) &&
-            Mem.valid_pointer m b1 (Ptrofs.unsigned i0)); try discriminate H.
-  destruct c; simpl in *; inv H; reflexivity.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl. destruct (rs###r1); auto. destruct (rs###r2); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl. destruct (rs###r1); auto. destruct (rs###r2); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split; intros; Simpl. unfold Val.cmpl. rewrite <- Val.swap_cmpl_bool.
+  simpl. rewrite (Val.negate_cmpl_bool Clt). 
+  destruct (Val.cmpl_bool Clt rs###r2 rs###r1) as [[]|]; auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl. unfold Val.cmpl. rewrite <- Val.swap_cmpl_bool. auto.
+- econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split; intros; Simpl. unfold Val.cmpl. rewrite (Val.negate_cmpl_bool Clt). 
+  destruct (Val.cmpl_bool Clt rs###r1 rs###r2) as [[]|]; auto.
 Qed.
 
-Lemma compare_longs_spec:
-  forall rs v1 v2 m,
-  let rs' := nextinstr (compare_longs v1 v2 rs m) in
-     rs'#ZF = Val.maketotal (Val.cmplu (Mem.valid_pointer m) Ceq v1 v2)
-  /\ rs'#CF = Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt v1 v2)
-  /\ rs'#SF = Val.negativel (Val.subl v1 v2)
-  /\ rs'#OF = Val.subl_overflow v1 v2
-  /\ (forall r, data_preg r = true -> rs'#r = rs#r).
+Lemma transl_cond_int64u_correct:
+  forall cmp rd r1 r2 k rs m,
+  exists rs',
+     exec_straight ge fn (transl_cond_int64u cmp rd r1 r2 k) rs m k rs' m
+  /\ rs'#rd = Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs###r1 rs###r2)
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
 Proof.
-  intros. unfold rs'; unfold compare_longs.
-  split. auto.
-  split. auto.
-  split. auto.
-  split. auto.
-  intros. Simplifs.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split; intros; Simpl. unfold Val.cmplu. rewrite <- Val.swap_cmplu_bool.
+  simpl. rewrite (Val.negate_cmplu_bool (Mem.valid_pointer m) Cle). 
+  destruct (Val.cmplu_bool (Mem.valid_pointer m) Cle rs###r1 rs###r2) as [[]|]; auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl. unfold Val.cmplu. rewrite <- Val.swap_cmplu_bool. auto.
+- econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split; intros; Simpl. unfold Val.cmplu. rewrite (Val.negate_cmplu_bool (Mem.valid_pointer m) Clt). 
+  destruct (Val.cmplu_bool (Mem.valid_pointer m) Clt rs###r1 rs###r2) as [[]|]; auto.
 Qed.
 
-Lemma int64_sub_overflow:
-  forall x y,
-  Int.xor (Int.repr (Int64.unsigned (Int64.sub_overflow x y Int64.zero)))
-          (Int.repr (Int64.unsigned (Int64.negative (Int64.sub x y)))) =
-  (if Int64.lt x y then Int.one else Int.zero).
+Lemma transl_condimm_int32s_correct:
+  forall cmp rd r1 n k rs m,
+  r1 <> X31 ->
+  exists rs',
+     exec_straight ge fn (transl_condimm_int32s cmp rd r1 n k) rs m k rs' m
+  /\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
 Proof.
-  intros.
-  transitivity (Int.repr (Int64.unsigned (if Int64.lt x y then Int64.one else Int64.zero))).
-  rewrite <- (Int64.lt_sub_overflow x y).
-  unfold Int64.sub_overflow, Int64.negative.
-  set (s := Int64.signed x - Int64.signed y - Int64.signed Int64.zero).
-  destruct (zle Int64.min_signed s && zle s Int64.max_signed);
-  destruct (Int64.lt (Int64.sub x y) Int64.zero);
-  auto.
-  destruct (Int64.lt x y); auto.
+  intros. unfold transl_condimm_int32s.
+  predSpec Int.eq Int.eq_spec n Int.zero.
+- subst n. exploit transl_cond_int32s_correct. intros (rs' & A & B & C).
+  exists rs'; eauto.
+- assert (DFL:
+    exists rs',
+      exec_straight ge fn (loadimm32 X31 n (transl_cond_int32s cmp rd r1 X31 k)) rs m k rs' m
+   /\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd
+   /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
+  { exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
+    exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2).
+    exists rs2; split. 
+    eapply exec_straight_trans. eexact A1. eexact A2. 
+    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. auto.
+    intros; transitivity (rs1 r); auto. }
+  destruct cmp.
++ unfold xorimm32. 
+  exploit (opimm32_correct Pxorw Pxoriw Val.xor); eauto. intros (rs1 & A1 & B1 & C1).
+  exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2).
+  exists rs2; split. 
+  eapply exec_straight_trans. eexact A1. eexact A2. 
+  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
+  unfold Val.cmp in B2; simpl in B2; rewrite Int.xor_is_zero in B2. exact B2.
+  intros; transitivity (rs1 r); auto.
++ unfold xorimm32. 
+  exploit (opimm32_correct Pxorw Pxoriw Val.xor); eauto. intros (rs1 & A1 & B1 & C1).
+  exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2).
+  exists rs2; split. 
+  eapply exec_straight_trans. eexact A1. eexact A2. 
+  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
+  unfold Val.cmp in B2; simpl in B2; rewrite Int.xor_is_zero in B2. exact B2.
+  intros; transitivity (rs1 r); auto.
++ exploit (opimm32_correct Psltw Psltiw (Val.cmp Clt)); eauto. intros (rs1 & A1 & B1 & C1).
+  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
++ predSpec Int.eq Int.eq_spec n (Int.repr Int.max_signed).
+* subst n. exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
+  exists rs1; split. eexact A1. split; auto. 
+  unfold Val.cmp; destruct (rs#r1); simpl; auto. rewrite B1. 
+  unfold Int.lt. rewrite zlt_false. auto. 
+  change (Int.signed (Int.repr Int.max_signed)) with Int.max_signed.
+  generalize (Int.signed_range i); lia.
+* exploit (opimm32_correct Psltw Psltiw (Val.cmp Clt)); eauto. intros (rs1 & A1 & B1 & C1).
+  exists rs1; split. eexact A1. split; auto. 
+  rewrite B1. unfold Val.cmp; simpl; destruct (rs#r1); simpl; auto.
+  unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1).
+  destruct (zlt (Int.signed n) (Int.signed i)).
+  rewrite zlt_false by lia. auto.
+  rewrite zlt_true by lia. auto.
+  rewrite Int.add_signed. symmetry; apply Int.signed_repr. 
+  assert (Int.signed n <> Int.max_signed).
+  { red; intros E. elim H1. rewrite <- (Int.repr_signed n). rewrite E. auto. }
+  generalize (Int.signed_range n); lia.
++ apply DFL.
++ apply DFL.
 Qed.
 
-Lemma testcond_for_signed_comparison_64_correct:
-  forall c v1 v2 rs m b,
-  Val.cmpl_bool c v1 v2 = Some b ->
-  eval_testcond (testcond_for_signed_comparison c)
-                (nextinstr (compare_longs v1 v2 rs m)) = Some b.
+Lemma transl_condimm_int32u_correct:
+  forall cmp rd r1 n k rs m,
+  r1 <> X31 ->
+  exists rs',
+     exec_straight ge fn (transl_condimm_int32u cmp rd r1 n k) rs m k rs' m
+  /\ Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp rs#r1 (Vint n)) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
 Proof.
-  intros. generalize (compare_longs_spec rs v1 v2 m).
-  set (rs' := nextinstr (compare_longs v1 v2 rs m)).
-  intros [A [B [C [D E]]]].
-  destruct v1; destruct v2; simpl in H; inv H.
-  unfold eval_testcond. rewrite A; rewrite B; rewrite C; rewrite D.
-  simpl; rewrite int64_sub_overflow.
-  destruct c; simpl.
-  destruct (Int64.eq i i0); auto.
-  destruct (Int64.eq i i0); auto.
-  destruct (Int64.lt i i0); auto.
-  rewrite Int64.not_lt. destruct (Int64.lt i i0); simpl; destruct (Int64.eq i i0); auto.
-  rewrite (Int64.lt_not i i0). destruct (Int64.lt i i0); destruct (Int64.eq i i0); reflexivity.
-  destruct (Int64.lt i i0); reflexivity.
+  intros. unfold transl_condimm_int32u.
+  predSpec Int.eq Int.eq_spec n Int.zero.
+- subst n. exploit transl_cond_int32u_correct. intros (rs' & A & B & C).
+  exists rs'; split. eexact A. split; auto. rewrite B; auto.
+- assert (DFL:
+    exists rs',
+      exec_straight ge fn (loadimm32 X31 n (transl_cond_int32u cmp rd r1 X31 k)) rs m k rs' m
+   /\ Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp rs#r1 (Vint n)) rs'#rd
+   /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
+  { exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
+    exploit transl_cond_int32u_correct; eauto. intros (rs2 & A2 & B2 & C2).
+    exists rs2; split. 
+    eapply exec_straight_trans. eexact A1. eexact A2. 
+    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. rewrite B2; auto.
+    intros; transitivity (rs1 r); auto. }
+  destruct cmp.
++ apply DFL.
++ apply DFL.
++ exploit (opimm32_correct Psltuw Psltiuw (Val.cmpu (Mem.valid_pointer m) Clt) m); eauto.
+  intros (rs1 & A1 & B1 & C1).
+  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
++ apply DFL.
++ apply DFL.
++ apply DFL.
 Qed.
 
-Lemma testcond_for_unsigned_comparison_64_correct:
-  forall c v1 v2 rs m b,
-  Val.cmplu_bool (Mem.valid_pointer m) c v1 v2 = Some b ->
-  eval_testcond (testcond_for_unsigned_comparison c)
-                (nextinstr (compare_longs v1 v2 rs m)) = Some b.
+Lemma transl_condimm_int64s_correct:
+  forall cmp rd r1 n k rs m,
+  r1 <> X31 ->
+  exists rs',
+     exec_straight ge fn (transl_condimm_int64s cmp rd r1 n k) rs m k rs' m
+  /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
 Proof.
-  intros. generalize (compare_longs_spec rs v1 v2 m).
-  set (rs' := nextinstr (compare_longs v1 v2 rs m)).
-  intros [A [B [C [D E]]]].
-  unfold eval_testcond. rewrite A; rewrite B.
-  destruct v1; destruct v2; simpl in H; FuncInv; subst.
-- (* int int *)
-  destruct c; simpl; auto.
-  destruct (Int64.eq i i0); reflexivity.
-  destruct (Int64.eq i i0); auto.
-  destruct (Int64.ltu i i0); auto.
-  rewrite Int64.not_ltu. destruct (Int64.ltu i i0); simpl; destruct (Int64.eq i i0); auto.
-  rewrite (Int64.ltu_not i i0). destruct (Int64.ltu i i0); destruct (Int64.eq i i0); reflexivity.
-  destruct (Int64.ltu i i0); reflexivity.
-- (* int ptr *)
-  unfold Val.cmplu; simpl; destruct Archi.ptr64; try discriminate.
-  destruct (Int64.eq i Int64.zero &&
-    (Mem.valid_pointer m b0 (Ptrofs.unsigned i0) || Mem.valid_pointer m b0 (Ptrofs.unsigned i0 - 1))) eqn:?; try discriminate H.
-  destruct c; simpl in *; inv H; auto.
-- (* ptr int *)
-  unfold Val.cmplu; simpl; destruct Archi.ptr64; try discriminate.
-  destruct (Int64.eq i0 Int64.zero &&
-    (Mem.valid_pointer m b0 (Ptrofs.unsigned i) || Mem.valid_pointer m b0 (Ptrofs.unsigned i - 1))) eqn:?; try discriminate H.
-  destruct c; simpl in *; inv H; auto.
-- (* ptr ptr *)
-  unfold Val.cmplu; simpl; destruct Archi.ptr64; try discriminate H.
-  fold (Mem.weak_valid_pointer m b0 (Ptrofs.unsigned i)) in *.
-  fold (Mem.weak_valid_pointer m b1 (Ptrofs.unsigned i0)) in *.
-  destruct (eq_block b0 b1).
-  destruct (Mem.weak_valid_pointer m b0 (Ptrofs.unsigned i) &&
-            Mem.weak_valid_pointer m b1 (Ptrofs.unsigned i0)); inv H.
-  destruct c; simpl; auto.
-  destruct (Ptrofs.eq i i0); auto.
-  destruct (Ptrofs.eq i i0); auto.
-  destruct (Ptrofs.ltu i i0); auto.
-  rewrite Ptrofs.not_ltu. destruct (Ptrofs.ltu i i0); simpl; destruct (Ptrofs.eq i i0); auto.
-  rewrite (Ptrofs.ltu_not i i0). destruct (Ptrofs.ltu i i0); destruct (Ptrofs.eq i i0); reflexivity.
-  destruct (Ptrofs.ltu i i0); reflexivity.
-  destruct (Mem.valid_pointer m b0 (Ptrofs.unsigned i) &&
-            Mem.valid_pointer m b1 (Ptrofs.unsigned i0)); try discriminate H.
-  destruct c; simpl in *; inv H; reflexivity.
+  intros. unfold transl_condimm_int64s.
+  predSpec Int64.eq Int64.eq_spec n Int64.zero.
+- subst n. exploit transl_cond_int64s_correct. intros (rs' & A & B & C).
+  exists rs'; eauto.
+- assert (DFL:
+    exists rs',
+      exec_straight ge fn (loadimm64 X31 n (transl_cond_int64s cmp rd r1 X31 k)) rs m k rs' m
+   /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd
+   /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
+  { exploit loadimm64_correct; eauto. intros (rs1 & A1 & B1 & C1).
+    exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2).
+    exists rs2; split. 
+    eapply exec_straight_trans. eexact A1. eexact A2. 
+    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. auto.
+    intros; transitivity (rs1 r); auto. }
+  destruct cmp.
++ unfold xorimm64. 
+  exploit (opimm64_correct Pxorl Pxoril Val.xorl); eauto. intros (rs1 & A1 & B1 & C1).
+  exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2).
+  exists rs2; split. 
+  eapply exec_straight_trans. eexact A1. eexact A2. 
+  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
+  unfold Val.cmpl in B2; simpl in B2; rewrite Int64.xor_is_zero in B2. exact B2.
+  intros; transitivity (rs1 r); auto.
++ unfold xorimm64. 
+  exploit (opimm64_correct Pxorl Pxoril Val.xorl); eauto. intros (rs1 & A1 & B1 & C1).
+  exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2).
+  exists rs2; split. 
+  eapply exec_straight_trans. eexact A1. eexact A2. 
+  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
+  unfold Val.cmpl in B2; simpl in B2; rewrite Int64.xor_is_zero in B2. exact B2.
+  intros; transitivity (rs1 r); auto.
++ exploit (opimm64_correct Psltl Psltil (fun v1 v2 => Val.maketotal (Val.cmpl Clt v1 v2))); eauto. intros (rs1 & A1 & B1 & C1).
+  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
++ predSpec Int64.eq Int64.eq_spec n (Int64.repr Int64.max_signed).
+* subst n. exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
+  exists rs1; split. eexact A1. split; auto. 
+  unfold Val.cmpl; destruct (rs#r1); simpl; auto. rewrite B1. 
+  unfold Int64.lt. rewrite zlt_false. auto. 
+  change (Int64.signed (Int64.repr Int64.max_signed)) with Int64.max_signed.
+  generalize (Int64.signed_range i); lia.
+* exploit (opimm64_correct Psltl Psltil (fun v1 v2 => Val.maketotal (Val.cmpl Clt v1 v2))); eauto. intros (rs1 & A1 & B1 & C1).
+  exists rs1; split. eexact A1. split; auto. 
+  rewrite B1. unfold Val.cmpl; simpl; destruct (rs#r1); simpl; auto.
+  unfold Int64.lt. replace (Int64.signed (Int64.add n Int64.one)) with (Int64.signed n + 1).
+  destruct (zlt (Int64.signed n) (Int64.signed i)).
+  rewrite zlt_false by lia. auto.
+  rewrite zlt_true by lia. auto.
+  rewrite Int64.add_signed. symmetry; apply Int64.signed_repr. 
+  assert (Int64.signed n <> Int64.max_signed).
+  { red; intros E. elim H1. rewrite <- (Int64.repr_signed n). rewrite E. auto. }
+  generalize (Int64.signed_range n); lia.
++ apply DFL.
++ apply DFL.
 Qed.
 
-Lemma compare_floats_spec:
-  forall rs n1 n2,
-  let rs' := nextinstr (compare_floats (Vfloat n1) (Vfloat n2) rs) in
-     rs'#ZF = Val.of_bool (Float.cmp Ceq n1 n2 || negb (Float.ordered n1 n2))
-  /\ rs'#CF = Val.of_bool (negb (Float.cmp Cge n1 n2))
-  /\ rs'#PF = Val.of_bool (negb (Float.ordered n1 n2))
-  /\ (forall r, data_preg r = true -> rs'#r = rs#r).
+Lemma transl_condimm_int64u_correct:
+  forall cmp rd r1 n k rs m,
+  r1 <> X31 ->
+  exists rs',
+     exec_straight ge fn (transl_condimm_int64u cmp rd r1 n k) rs m k rs' m
+  /\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
 Proof.
-  intros. unfold rs'; unfold compare_floats.
-  split. auto.
-  split. auto.
-  split. auto.
-  intros. Simplifs.
-Qed.
-
-Lemma compare_floats32_spec:
-  forall rs n1 n2,
-  let rs' := nextinstr (compare_floats32 (Vsingle n1) (Vsingle n2) rs) in
-     rs'#ZF = Val.of_bool (Float32.cmp Ceq n1 n2 || negb (Float32.ordered n1 n2))
-  /\ rs'#CF = Val.of_bool (negb (Float32.cmp Cge n1 n2))
-  /\ rs'#PF = Val.of_bool (negb (Float32.ordered n1 n2))
-  /\ (forall r, data_preg r = true -> rs'#r = rs#r).
+  intros. unfold transl_condimm_int64u.
+  predSpec Int64.eq Int64.eq_spec n Int64.zero.
+- subst n. exploit transl_cond_int64u_correct. intros (rs' & A & B & C).
+  exists rs'; split. eexact A. split; auto. rewrite B; auto.
+- assert (DFL:
+    exists rs',
+      exec_straight ge fn (loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k)) rs m k rs' m
+   /\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd
+   /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
+  { exploit loadimm64_correct; eauto. intros (rs1 & A1 & B1 & C1).
+    exploit transl_cond_int64u_correct; eauto. intros (rs2 & A2 & B2 & C2).
+    exists rs2; split. 
+    eapply exec_straight_trans. eexact A1. eexact A2. 
+    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. rewrite B2; auto.
+    intros; transitivity (rs1 r); auto. }
+  destruct cmp.
++ apply DFL.
++ apply DFL.
++ exploit (opimm64_correct Psltul Psltiul (fun v1 v2 => Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt v1 v2)) m); eauto.
+  intros (rs1 & A1 & B1 & C1).
+  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
++ apply DFL.
++ apply DFL.
++ apply DFL.
+   Qed.
+
+Lemma transl_cond_op_correct:
+  forall cond rd args k c rs m,
+  transl_cond_op cond rd args k = OK c ->
+  exists rs',
+     exec_straight ge fn c rs m k rs' m
+  /\ Val.lessdef (Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m)) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
 Proof.
-  intros. unfold rs'; unfold compare_floats32.
-  split. auto.
-  split. auto.
-  split. auto.
-  intros. Simplifs.
-Qed.
-
-Definition eval_extcond (xc: extcond) (rs: regset) : option bool :=
-  match xc with
-  | Cond_base c =>
-      eval_testcond c rs
-  | Cond_and c1 c2 =>
-      match eval_testcond c1 rs, eval_testcond c2 rs with
-      | Some b1, Some b2 => Some (b1 && b2)
-      | _, _ => None
-      end
-  | Cond_or c1 c2 =>
-      match eval_testcond c1 rs, eval_testcond c2 rs with
-      | Some b1, Some b2 => Some (b1 || b2)
-      | _, _ => None
-      end
-  end.
+  assert (MKTOT: forall ob, Val.of_optbool ob = Val.maketotal (option_map Val.of_bool ob)).
+  { destruct ob as [[]|]; reflexivity. }
+  intros until m; intros TR.
+  destruct cond; simpl in TR; ArgsInv.
++ (* cmp *)
+  exploit transl_cond_int32s_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto.
++ (* cmpu *)
+  exploit transl_cond_int32u_correct; eauto. intros (rs' & A & B & C).
+  exists rs'; repeat split; eauto. rewrite B; auto.
++ (* cmpimm *)
+  apply transl_condimm_int32s_correct; eauto with asmgen.
++ (* cmpuimm *)
+  apply transl_condimm_int32u_correct; eauto with asmgen.
++ (* cmpl *)
+  exploit transl_cond_int64s_correct; eauto. intros (rs' & A & B & C).
+  exists rs'; repeat split; eauto. rewrite MKTOT; eauto.
++ (* cmplu *)
+  exploit transl_cond_int64u_correct; eauto. intros (rs' & A & B & C).
+   exists rs'; repeat split; eauto. rewrite B, MKTOT; eauto.
++ (* cmplimm *)
+  exploit transl_condimm_int64s_correct; eauto. instantiate (1 := x); eauto with asmgen. 
+  intros (rs' & A & B & C).
+  exists rs'; repeat split; eauto. rewrite MKTOT; eauto.
++ (* cmpluimm *)
+  exploit transl_condimm_int64u_correct; eauto. instantiate (1 := x); eauto with asmgen. 
+  intros (rs' & A & B & C).
+   exists rs'; repeat split; eauto. rewrite MKTOT; eauto.
++ (* cmpf *)
+  destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR.
+  fold (Val.cmpf c0 (rs x) (rs x0)).
+  set (v := Val.cmpf c0 (rs x) (rs x0)).
+  destruct normal; inv EQ2.
+* econstructor; split.
+  apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto.
+  split; intros; Simpl.
+* econstructor; split.
+  eapply exec_straight_two.
+  eapply transl_cond_float_correct with (v := Val.notbool v); eauto.
+  simpl; reflexivity.
+  auto. auto.
+  split; intros; Simpl. unfold v, Val.cmpf. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; auto.
++ (* notcmpf *)
+  destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR.
+  rewrite Val.notbool_negb_3. fold (Val.cmpf c0 (rs x) (rs x0)).
+  set (v := Val.cmpf c0 (rs x) (rs x0)).
+  destruct normal; inv EQ2.
+* econstructor; split.
+  eapply exec_straight_two.
+  eapply transl_cond_float_correct with (v := v); eauto.
+  simpl; reflexivity.
+  auto. auto.
+  split; intros; Simpl. unfold v, Val.cmpf. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; auto.
+* econstructor; split.
+  apply exec_straight_one. eapply transl_cond_float_correct with (v := Val.notbool v); eauto. auto.
+  split; intros; Simpl.
++ (* cmpfs *)
+  destruct (transl_cond_single c0 rd x x0) as [insn normal] eqn:TR.
+  fold (Val.cmpfs c0 (rs x) (rs x0)).
+  set (v := Val.cmpfs c0 (rs x) (rs x0)).
+  destruct normal; inv EQ2.
+* econstructor; split.
+  apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto.
+  split; intros; Simpl.
+* econstructor; split.
+  eapply exec_straight_two.
+  eapply transl_cond_single_correct with (v := Val.notbool v); eauto.
+  simpl; reflexivity.
+  auto. auto.
+  split; intros; Simpl. unfold v, Val.cmpfs. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; auto.
++ (* notcmpfs *)
+  destruct (transl_cond_single c0 rd x x0) as [insn normal] eqn:TR.
+  rewrite Val.notbool_negb_3. fold (Val.cmpfs c0 (rs x) (rs x0)).
+  set (v := Val.cmpfs c0 (rs x) (rs x0)).
+  destruct normal; inv EQ2.
+* econstructor; split.
+  eapply exec_straight_two.
+  eapply transl_cond_single_correct with (v := v); eauto.
+  simpl; reflexivity.
+  auto. auto.
+  split; intros; Simpl. unfold v, Val.cmpfs. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; auto.
+* econstructor; split.
+  apply exec_straight_one. eapply transl_cond_single_correct with (v := Val.notbool v); eauto. auto.
+  split; intros; Simpl.
+   Qed.
 
-Definition swap_floats {A: Type} (c: comparison) (n1 n2: A) : A :=
-  match c with
-  | Clt | Cle => n2
-  | Ceq | Cne | Cgt | Cge => n1
-  end.
+(** Some arithmetic properties. *)
 
-Lemma testcond_for_float_comparison_correct:
-  forall c n1 n2 rs,
-  eval_extcond (testcond_for_condition (Ccompf c))
-               (nextinstr (compare_floats (Vfloat (swap_floats c n1 n2))
-                                          (Vfloat (swap_floats c n2 n1)) rs)) =
-  Some(Float.cmp c n1 n2).
+Remark cast32unsigned_from_cast32signed:
+  forall i, Int64.repr (Int.unsigned i) = Int64.zero_ext 32 (Int64.repr (Int.signed i)).
 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 *)
-Transparent Float.cmp Float.ordered.
-  unfold Float.ordered, Float.cmp; destruct (Float.compare n1 n2) as [[]|]; reflexivity.
-- (* ne *)
-  unfold Float.ordered, Float.cmp; destruct (Float.compare n1 n2) as [[]|]; reflexivity.
-- (* lt *)
-  rewrite <- (Float.cmp_swap Clt n2 n1). simpl. unfold Float.ordered. 
-  destruct (Float.compare n2 n1) as [[]|]; reflexivity.
-- (* le *)
-  rewrite <- (Float.cmp_swap Cge n1 n2). simpl.
-  destruct (Float.compare n1 n2) as [[]|]; auto.
-- (* gt *)
- unfold Float.ordered, Float.cmp; destruct (Float.compare n1 n2) as [[]|]; reflexivity.
-- (* ge *)
-  destruct (Float.cmp Cge n1 n2); auto.
-Opaque Float.cmp Float.ordered.
+  intros. apply Int64.same_bits_eq; intros. 
+  rewrite Int64.bits_zero_ext, !Int64.testbit_repr by tauto.
+  rewrite Int.bits_signed by tauto. fold (Int.testbit i i0).
+  change Int.zwordsize with 32.
+  destruct (zlt i0 32). auto. apply Int.bits_above. 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 *)
-Transparent Float.cmp Float.ordered.
-  unfold Float.ordered, Float.cmp; destruct (Float.compare n1 n2) as [[]|]; reflexivity.
-- (* ne *)
-  unfold Float.ordered, Float.cmp; destruct (Float.compare n1 n2) as [[]|]; reflexivity.
-- (* lt *)
-  rewrite <- (Float.cmp_swap Clt n2 n1). simpl. unfold Float.ordered. 
-  destruct (Float.compare n2 n1) as [[]|]; reflexivity.
-- (* le *)
-  rewrite <- (Float.cmp_swap Cge n1 n2). simpl.
-  destruct (Float.compare n1 n2) as [[]|]; auto.
-- (* gt *)
- unfold Float.ordered, Float.cmp; destruct (Float.compare n1 n2) as [[]|]; reflexivity.
-- (* ge *)
-  destruct (Float.cmp Cge n1 n2); auto.
-Opaque Float.cmp Float.ordered.
-Qed.
+(* Translation of arithmetic operations *)
 
-Lemma testcond_for_float32_comparison_correct:
-  forall c n1 n2 rs,
-  eval_extcond (testcond_for_condition (Ccompfs c))
-               (nextinstr (compare_floats32 (Vsingle (swap_floats c n1 n2))
-                                            (Vsingle (swap_floats c n2 n1)) rs)) =
-  Some(Float32.cmp c n1 n2).
-Proof.
-  intros.
-  generalize (compare_floats32_spec rs (swap_floats c n1 n2) (swap_floats c n2 n1)).
-  set (rs' := nextinstr (compare_floats32 (Vsingle (swap_floats c n1 n2))
-                                        (Vsingle (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 *)
-Transparent Float32.cmp Float32.ordered.
-  unfold Float32.ordered, Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; reflexivity.
-- (* ne *)
-  unfold Float32.ordered, Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; reflexivity.
-- (* lt *)
-  rewrite <- (Float32.cmp_swap Clt n2 n1). simpl. unfold Float32.ordered. 
-  destruct (Float32.compare n2 n1) as [[]|]; reflexivity.
-- (* le *)
-  rewrite <- (Float32.cmp_swap Cge n1 n2). simpl.
-  destruct (Float32.compare n1 n2) as [[]|]; auto.
-- (* gt *)
- unfold Float32.ordered, Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; reflexivity.
-- (* ge *)
-  destruct (Float32.cmp Cge n1 n2); auto.
-Opaque Float32.cmp Float32.ordered.
-Qed.
+Ltac SimplEval H :=
+  match type of H with
+  | Some _ = None _ => discriminate
+  | Some _ = Some _ => inv H
+  | ?a = Some ?b => let A := fresh in assert (A: Val.maketotal a = b) by (rewrite H; reflexivity)
+end.
 
-Lemma testcond_for_neg_float32_comparison_correct:
-  forall c n1 n2 rs,
-  eval_extcond (testcond_for_condition (Cnotcompfs c))
-               (nextinstr (compare_floats32 (Vsingle (swap_floats c n1 n2))
-                                            (Vsingle (swap_floats c n2 n1)) rs)) =
-  Some(negb(Float32.cmp c n1 n2)).
-Proof.
-  intros.
-  generalize (compare_floats32_spec rs (swap_floats c n1 n2) (swap_floats c n2 n1)).
-  set (rs' := nextinstr (compare_floats32 (Vsingle (swap_floats c n1 n2))
-                                          (Vsingle (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 *)
-Transparent Float32.cmp Float32.ordered.
-  unfold Float32.ordered, Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; reflexivity.
-- (* ne *)
-  unfold Float32.ordered, Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; reflexivity.
-- (* lt *)
-  rewrite <- (Float32.cmp_swap Clt n2 n1). simpl. unfold Float32.ordered. 
-  destruct (Float32.compare n2 n1) as [[]|]; reflexivity.
-- (* le *)
-  rewrite <- (Float32.cmp_swap Cge n1 n2). simpl.
-  destruct (Float32.compare n1 n2) as [[]|]; auto.
-- (* gt *)
- unfold Float32.ordered, Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; reflexivity.
-- (* ge *)
-  destruct (Float32.cmp Cge n1 n2); auto.
-Opaque Float32.cmp Float32.ordered.
-Qed.
+Ltac TranslOpSimpl :=
+  econstructor; split;
+  [ apply exec_straight_one; [simpl; eauto | reflexivity]
+  | split; [ apply Val.lessdef_same; Simpl; fail | intros; Simpl; fail ] ].
 
-Remark swap_floats_commut:
-  forall (A B: Type) c (f: A -> B) x y, swap_floats c (f x) (f y) = f (swap_floats c x y).
+Lemma transl_op_correct:
+  forall op args res k (rs: regset) m v c,
+  transl_op op args res k = OK c ->
+  eval_operation ge (rs#SP) op (map rs (map preg_of args)) m = Some v ->
+  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.
 Proof.
-  intros. destruct c; auto.
+  assert (SAME: forall v1 v2, v1 = v2 -> Val.lessdef v2 v1). { intros; subst; auto. }
+Opaque Int.eq.
+  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), (preg_of m0); inv TR; TranslOpSimpl. }
+  (* intconst *)
+  { exploit loadimm32_correct; eauto. intros (rs' & A & B & C).
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* longconst *)
+  { exploit loadimm64_correct; eauto. intros (rs' & A & B & C).
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* floatconst *)
+  { destruct (Float.eq_dec n Float.zero).
+    + subst n. econstructor; split. 
+      apply exec_straight_one. simpl; eauto. auto.
+      split; intros; Simpl. 
+    + econstructor; split. 
+      apply exec_straight_one. simpl; eauto. auto.
+      split; intros; Simpl. }
+  (* singleconst *)
+  { destruct (Float32.eq_dec n Float32.zero).
+    + subst n. econstructor; split. 
+      apply exec_straight_one. simpl; eauto. auto.
+      split; intros; Simpl. 
+    + econstructor; split. 
+      apply exec_straight_one. simpl; eauto. auto.
+      split; intros; Simpl. }
+  (* addrsymbol *)
+  { destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)).
+    + set (rs1 := nextinstr (rs#x <- (Genv.symbol_address ge id Ptrofs.zero))).
+      exploit (addptrofs_correct x x ofs k rs1 m); eauto with asmgen. 
+      intros (rs2 & A & B & C).
+      exists rs2; split. 
+      apply exec_straight_step with rs1 m; auto.
+      split. replace ofs with (Ptrofs.add Ptrofs.zero ofs) by (apply Ptrofs.add_zero_l). 
+      rewrite Genv.shift_symbol_address.
+      replace (rs1 x) with (Genv.symbol_address ge id Ptrofs.zero) in B by (unfold rs1; Simpl).
+      exact B.
+      intros. rewrite C by eauto with asmgen. unfold rs1; Simpl.  
+    + TranslOpSimpl. }
+  (* stackoffset *)
+  { exploit addptrofs_correct. instantiate (1 := X2); auto with asmgen. intros (rs' & A & B & C).
+  exists rs'; split; eauto. auto with asmgen. }
+  (* cast8signed *)
+  { econstructor; split.
+  eapply exec_straight_two. simpl;eauto. simpl;eauto. auto. auto.
+  split; intros; Simpl.
+  assert (A: Int.ltu (Int.repr 24) Int.iwordsize = true) by auto.
+  destruct (rs x0); auto; simpl. rewrite A; simpl. rewrite A. 
+  apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. }
+  (* cast16signed *)
+  { econstructor; split.
+  eapply exec_straight_two. simpl;eauto. simpl;eauto. auto. auto.
+  split; intros; Simpl.
+  assert (A: Int.ltu (Int.repr 16) Int.iwordsize = true) by auto.
+  destruct (rs x0); auto; simpl. rewrite A; simpl. rewrite A. 
+  apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. }
+  (* addimm *)
+  { exploit (opimm32_correct Paddw Paddiw Val.add); auto. instantiate (1 := x0); eauto with asmgen.
+  intros (rs' & A & B & C).
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* andimm *)
+  { exploit (opimm32_correct Pandw Pandiw Val.and); auto. instantiate (1 := x0); eauto with asmgen.
+  intros (rs' & A & B & C).
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* orimm *)
+  exploit (opimm32_correct Porw Poriw Val.or); auto. instantiate (1 := x0); eauto with asmgen.
+  { intros (rs' & A & B & C).
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* xorimm *)
+  { exploit (opimm32_correct Pxorw Pxoriw Val.xor); auto. instantiate (1 := x0); eauto with asmgen.
+  intros (rs' & A & B & C).
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* shrximm *)
+  { destruct (Val.shrx (rs x0) (Vint n)) eqn:TOTAL; cbn.
+    {
+    exploit Val.shrx_shr_3; eauto. intros E; subst v.
+    destruct (Int.eq n Int.zero).
+  + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+    split; intros; Simpl. 
+  + destruct (Int.eq n Int.one).
+    * econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      apply exec_straight_one. simpl; reflexivity. auto.
+      split; intros; Simpl.
+    * change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n).
+      econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      apply exec_straight_one. simpl; reflexivity. auto. 
+      split; intros; Simpl.
+    }
+    destruct (Int.eq n Int.zero).
+  + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+    split; intros; Simpl. 
+  + destruct (Int.eq n Int.one).
+    * econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      apply exec_straight_one. simpl; reflexivity. auto.
+      split; intros; Simpl.
+    * change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n).
+      econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      apply exec_straight_one. simpl; reflexivity. auto. 
+      split; intros; Simpl. }
+  (* longofintu *)
+  { econstructor; split.
+  eapply exec_straight_three. simpl; eauto. simpl; eauto. simpl; eauto. auto. auto. auto.
+  split; intros; Simpl. destruct (rs x0); auto. simpl. 
+  assert (A: Int.ltu (Int.repr 32) Int64.iwordsize' = true) by auto.
+  rewrite A; simpl. rewrite A. apply Val.lessdef_same. f_equal.
+  rewrite cast32unsigned_from_cast32signed. apply Int64.zero_ext_shru_shl. compute; auto. }
+  (* addlimm *)
+  { exploit (opimm64_correct Paddl Paddil Val.addl); auto. instantiate (1 := x0); eauto with asmgen.
+  intros (rs' & A & B & C).
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* andimm *)
+  { exploit (opimm64_correct Pandl Pandil Val.andl); auto. instantiate (1 := x0); eauto with asmgen.
+  intros (rs' & A & B & C).
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* orimm *)
+  { exploit (opimm64_correct Porl Poril Val.orl); auto. instantiate (1 := x0); eauto with asmgen.
+  intros (rs' & A & B & C).
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* xorimm *)
+  { exploit (opimm64_correct Pxorl Pxoril Val.xorl); auto. instantiate (1 := x0); eauto with asmgen.
+  intros (rs' & A & B & C).
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* shrxlimm *)
+  { destruct (Val.shrxl (rs x0) (Vint n)) eqn:TOTAL.
+    {
+     exploit Val.shrxl_shrl_3; eauto. intros E; subst v.
+    destruct (Int.eq n Int.zero).
+  + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+    split; intros; Simpl. 
+  + destruct (Int.eq n Int.one).
+    * econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      apply exec_straight_one. simpl; reflexivity. auto.
+      split; intros; Simpl.
+
+    * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n).
+      econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      apply exec_straight_one. simpl; reflexivity. auto. 
+      split; intros; Simpl.
+    }
+    destruct (Int.eq n Int.zero).
+  + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+    split; intros; Simpl. 
+  + destruct (Int.eq n Int.one).
+    * econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      apply exec_straight_one. simpl; reflexivity. auto.
+      split; intros; Simpl.
+
+    * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n).
+      econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      apply exec_straight_one. simpl; reflexivity. auto. 
+      split; intros; Simpl. }
+  (* cond *)
+  { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
+     exists rs'; split. eexact A. eauto with asmgen. }
+  (* Expanded instructions from RTL *)
+  9,10,19,20:
+    econstructor; split; try apply exec_straight_one; simpl; eauto;
+    split; intros; Simpl; try destruct (rs x0);
+    try rewrite Int64.add_commut;
+    try rewrite Int.add_commut; auto;
+    try rewrite Int64.and_commut;
+    try rewrite Int.and_commut; auto;
+    try rewrite Int64.or_commut;
+    try rewrite Int.or_commut; auto.
+  1-16:
+    destruct optR as [[]|]; try discriminate;
+    unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; try inv EQ3; try inv EQ2;
+    try destruct (Int.eq _ _) eqn:A; try inv H0;
+    try destruct (Int64.eq _ _) eqn:A; try inv H1;
+    econstructor; split; try apply exec_straight_one; simpl; eauto;
+    split; intros; Simpl;
+    try apply Int.same_if_eq in A; subst;
+    try apply Int64.same_if_eq in A; subst;
+    unfold get_sp;
+    try destruct (rs x0); auto;
+    try destruct (rs x1); auto;
+    try destruct (rs X2); auto;
+    try destruct Archi.ptr64 eqn:B;
+    try fold (Val.add (Vint Int.zero) (get_sp (rs X2)));
+    try fold (Val.addl (Vlong Int64.zero) (get_sp (rs X2)));
+    try rewrite Val.add_commut; auto;
+    try rewrite Val.addl_commut; auto;
+    try rewrite Int.add_commut; auto;
+    try rewrite Int64.add_commut; auto;
+    replace (Ptrofs.of_int Int.zero) with (Ptrofs.zero) by auto;
+    replace (Ptrofs.of_int64 Int64.zero) with (Ptrofs.zero) by auto;
+    try rewrite Ptrofs.add_zero; auto.
+  (* mayundef *)
+  { destruct (ireg_eq x x0); inv EQ2;
+    econstructor; split;
+    try apply exec_straight_one; simpl; eauto;
+    split; unfold eval_may_undef;
+    destruct mu eqn:EQMU; simpl; intros; Simpl; auto.
+    all:
+      destruct (rs (preg_of m0)) eqn:EQM0; simpl; auto;
+      destruct (rs x0); simpl; auto; Simpl;
+      try destruct (Int.ltu _ _); simpl;
+      Simpl; auto. }
+  (* select *)
+  { econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+  split; intros; Simpl.
+  apply Val.lessdef_normalize. }
 Qed.
 
-Remark compare_floats_inv:
-  forall vx vy rs r,
-  r <> CR ZF -> r <> CR CF -> r <> CR PF -> r <> CR SF -> r <> CR OF ->
-  compare_floats vx vy rs r = rs r.
-Proof.
-  intros.
-  assert (DFL: undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil) rs r = rs r).
-    simpl. Simplifs.
-  unfold compare_floats; destruct vx; destruct vy; auto. Simplifs.
-Qed.
+(** Memory accesses *)
 
-Remark compare_floats32_inv:
-  forall vx vy rs r,
-  r <> CR ZF -> r <> CR CF -> r <> CR PF -> r <> CR SF -> r <> CR OF ->
-  compare_floats32 vx vy rs r = rs r.
+Lemma indexed_memory_access_correct:
+  forall mk_instr base ofs k rs m,
+  base <> X31 ->
+  exists base' ofs' rs',
+     exec_straight_opt ge fn (indexed_memory_access mk_instr base ofs k) rs m
+                       (mk_instr base' ofs' :: k) rs' m
+  /\ Val.offset_ptr rs'#base' (eval_offset ge ofs') = Val.offset_ptr rs#base ofs
+  /\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r.
 Proof.
-  intros.
-  assert (DFL: undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil) rs r = rs r).
-    simpl. Simplifs.
-  unfold compare_floats32; destruct vx; destruct vy; auto. Simplifs.
+  unfold indexed_memory_access; intros.
+  destruct Archi.ptr64 eqn:SF.
+- generalize (make_immed64_sound (Ptrofs.to_int64 ofs)); intros EQ.
+  destruct (make_immed64 (Ptrofs.to_int64 ofs)).
++ econstructor; econstructor; econstructor; split.
+  apply exec_straight_opt_refl. 
+  split; auto. simpl. subst imm. rewrite Ptrofs.of_int64_to_int64 by auto. auto.
++ econstructor; econstructor; econstructor; split. 
+  constructor. eapply exec_straight_two. 
+  simpl; eauto. simpl; eauto. auto. auto. 
+  split; intros; Simpl. destruct (rs base); auto; simpl. rewrite SF. simpl.
+  rewrite Ptrofs.add_assoc. f_equal. f_equal. 
+  rewrite <- (Ptrofs.of_int64_to_int64 SF ofs). rewrite EQ. 
+  symmetry; auto with ptrofs.
++ econstructor; econstructor; econstructor; split. 
+  constructor. eapply exec_straight_two. 
+  simpl; eauto. simpl; eauto. auto. auto. 
+  split; intros; Simpl. unfold eval_offset. destruct (rs base); auto; simpl. rewrite SF. simpl.
+  rewrite Ptrofs.add_zero. subst imm. rewrite Ptrofs.of_int64_to_int64 by auto. auto.
+- generalize (make_immed32_sound (Ptrofs.to_int ofs)); intros EQ.
+  destruct (make_immed32 (Ptrofs.to_int ofs)).
++ econstructor; econstructor; econstructor; split.
+  apply exec_straight_opt_refl. 
+  split; auto. simpl. subst imm. rewrite Ptrofs.of_int_to_int by auto. auto.
++ econstructor; econstructor; econstructor; split. 
+  constructor. eapply exec_straight_two. 
+  simpl; eauto. simpl; eauto. auto. auto. 
+  split; intros; Simpl. destruct (rs base); auto; simpl. rewrite SF. simpl.
+  rewrite Ptrofs.add_assoc. f_equal. f_equal. 
+  rewrite <- (Ptrofs.of_int_to_int SF ofs). rewrite EQ. 
+  symmetry; auto with ptrofs.
 Qed.
 
-Lemma transl_cond_correct:
-  forall cond args k c rs m,
-  transl_cond cond args k = OK c ->
+Lemma indexed_load_access_correct:
+  forall chunk (mk_instr: ireg -> offset -> instruction) rd m,
+  (forall base ofs rs,
+     exec_instr ge fn (mk_instr base ofs) rs m = exec_load ge chunk rs m rd base ofs) ->
+  forall (base: ireg) ofs k (rs: regset) v,
+  Mem.loadv chunk m (Val.offset_ptr rs#base ofs) = Some v ->
+  base <> X31 -> rd <> PC ->
   exists rs',
-     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
-              /\ eval_extcond (testcond_for_condition (negate_condition cond)) rs' = Some (negb b)
-     end
-  /\ forall r, data_preg r = true -> rs'#r = rs r.
+     exec_straight ge fn (indexed_memory_access mk_instr base ofs k) rs m k rs' m
+  /\ rs'#rd = v
+  /\ forall r, r <> PC -> r <> X31 -> r <> rd -> rs'#r = rs#r.
 Proof.
-  unfold transl_cond; intros.
-  destruct cond; repeat (destruct args; try discriminate); monadInv H.
-- (* comp *)
-  simpl. rewrite (ireg_of_eq _ _ EQ). rewrite (ireg_of_eq _ _ EQ1).
-  econstructor. split. apply exec_straight_one. simpl. eauto. auto.
-  split. destruct (Val.cmp_bool c0 (rs x) (rs x0)) eqn:?; auto. split.
-  eapply testcond_for_signed_comparison_32_correct; eauto.
-  eapply testcond_for_signed_comparison_32_correct; eauto.
-  rewrite Val.negate_cmp_bool, Heqo; auto.
-  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. split.
-  eapply testcond_for_unsigned_comparison_32_correct; eauto.
-  eapply testcond_for_unsigned_comparison_32_correct; eauto.
-  rewrite Val.negate_cmpu_bool, Heqo; auto.
-  intros. unfold compare_ints. Simplifs.
-- (* compimm *)
-  simpl. rewrite (ireg_of_eq _ _ EQ). destruct (Int.eq_dec n Int.zero).
-  econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split. destruct (rs x); simpl; auto. subst. rewrite Int.and_idem. split.
-  eapply testcond_for_signed_comparison_32_correct; eauto.
-  eapply testcond_for_signed_comparison_32_correct; eauto.
-  rewrite Val.negate_cmp_bool; auto.
-  intros. unfold compare_ints. Simplifs.
-  econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split. destruct (Val.cmp_bool c0 (rs x) (Vint n)) eqn:?; auto. split.
-  eapply testcond_for_signed_comparison_32_correct; eauto.
-  eapply testcond_for_signed_comparison_32_correct; eauto.
-  rewrite Val.negate_cmp_bool, Heqo; auto.
-  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 n)) eqn:?; auto; split.
-  eapply testcond_for_unsigned_comparison_32_correct; eauto.
-  eapply testcond_for_unsigned_comparison_32_correct; eauto.
-  rewrite Val.negate_cmpu_bool, Heqo; auto.
-  intros. unfold compare_ints. Simplifs.
-- (* compl *)
-  simpl. rewrite (ireg_of_eq _ _ EQ). rewrite (ireg_of_eq _ _ EQ1).
-  econstructor. split. apply exec_straight_one. simpl. eauto. auto.
-  split. destruct (Val.cmpl_bool c0 (rs x) (rs x0)) eqn:?; auto. split.
-  eapply testcond_for_signed_comparison_64_correct; eauto.
-  eapply testcond_for_signed_comparison_64_correct; eauto.
-  rewrite Val.negate_cmpl_bool, Heqo; auto.
-  intros. unfold compare_longs. Simplifs.
-- (* complu *)
-  simpl. rewrite (ireg_of_eq _ _ EQ). rewrite (ireg_of_eq _ _ EQ1).
-  econstructor. split. apply exec_straight_one. simpl. eauto. auto.
-  split. destruct (Val.cmplu_bool (Mem.valid_pointer m) c0 (rs x) (rs x0)) eqn:?; auto. split.
-  eapply testcond_for_unsigned_comparison_64_correct; eauto.
-  eapply testcond_for_unsigned_comparison_64_correct; eauto.
-  rewrite Val.negate_cmplu_bool, Heqo; auto.
-  intros. unfold compare_longs. Simplifs.
-- (* compimm *)
-  simpl. rewrite (ireg_of_eq _ _ EQ). destruct (Int64.eq_dec n Int64.zero).
-  econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split. destruct (rs x); simpl; auto. subst. rewrite Int64.and_idem. split.
-  eapply testcond_for_signed_comparison_64_correct; eauto.
-  eapply testcond_for_signed_comparison_64_correct; eauto.
-  rewrite Val.negate_cmpl_bool; auto.
-  intros. unfold compare_longs. Simplifs.
-  econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split. destruct (Val.cmpl_bool c0 (rs x) (Vlong n)) eqn:?; auto. split.
-  eapply testcond_for_signed_comparison_64_correct; eauto.
-  eapply testcond_for_signed_comparison_64_correct; eauto.
-  rewrite Val.negate_cmpl_bool, Heqo; auto.
-  intros. unfold compare_longs. Simplifs.
-- (* compuimm *)
-  simpl. rewrite (ireg_of_eq _ _ EQ).
-  econstructor. split. apply exec_straight_one. simpl. eauto. auto.
-  split. destruct (Val.cmplu_bool (Mem.valid_pointer m) c0 (rs x) (Vlong n)) eqn:?; auto. split.
-  eapply testcond_for_unsigned_comparison_64_correct; eauto.
-  eapply testcond_for_unsigned_comparison_64_correct; eauto.
-  rewrite Val.negate_cmplu_bool, Heqo; auto.
-  intros. unfold compare_longs. 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 asmgen.
-  split. destruct (rs x); destruct (rs x0); simpl; auto.
-  repeat rewrite swap_floats_commut. split.
-  apply testcond_for_float_comparison_correct.
-  apply testcond_for_neg_float_comparison_correct.
-  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 asmgen.
-  split. destruct (rs x); destruct (rs x0); simpl; auto.
-  repeat rewrite swap_floats_commut. split.
-  apply testcond_for_neg_float_comparison_correct.
-  rewrite negb_involutive. apply testcond_for_float_comparison_correct.
-  intros. Simplifs. apply compare_floats_inv; auto with asmgen.
-- (* compfs *)
-  simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1).
-  exists (nextinstr (compare_floats32 (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_floats32_inv; auto with asmgen.
-  split. destruct (rs x); destruct (rs x0); simpl; auto.
-  repeat rewrite swap_floats_commut. split.
-  apply testcond_for_float32_comparison_correct.
-  apply testcond_for_neg_float32_comparison_correct.
-  intros. Simplifs. apply compare_floats32_inv; auto with asmgen.
-- (* notcompfs *)
-  simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1).
-  exists (nextinstr (compare_floats32 (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_floats32_inv; auto with asmgen.
-  split. destruct (rs x); destruct (rs x0); simpl; auto.
-  repeat rewrite swap_floats_commut. split.
-  apply testcond_for_neg_float32_comparison_correct.
-  rewrite negb_involutive. apply testcond_for_float32_comparison_correct.
-  intros. Simplifs. apply compare_floats32_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 i n)) Vzero m).
-  intros [A B]. rewrite A. unfold Val.cmpu; simpl. destruct (Int.eq (Int.and i n) Int.zero); auto.
-  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 i n)) Vzero m).
-  intros [A B]. rewrite A. unfold Val.cmpu; simpl. destruct (Int.eq (Int.and i n) Int.zero); auto.
-  intros. unfold compare_ints. Simplifs.
+  intros until m; intros EXEC; intros until v; intros LOAD NOT31 NOTPC.
+  exploit indexed_memory_access_correct; eauto.
+  intros (base' & ofs' & rs' & A & B & C).
+  econstructor; split.
+  eapply exec_straight_opt_right. eexact A. apply exec_straight_one. rewrite EXEC.
+  unfold exec_load. rewrite B, LOAD. eauto. Simpl. 
+  split; intros; Simpl.
 Qed.
 
-Remark eval_testcond_nextinstr:
-  forall c rs, eval_testcond c (nextinstr rs) = eval_testcond c rs.
+Lemma indexed_store_access_correct:
+  forall chunk (mk_instr: ireg -> offset -> instruction) r1 m,
+  (forall base ofs rs,
+     exec_instr ge fn (mk_instr base ofs) rs m = exec_store ge chunk rs m r1 base ofs) ->
+  forall (base: ireg) ofs k (rs: regset) m',
+  Mem.storev chunk m (Val.offset_ptr rs#base ofs) (rs#r1) = Some m' ->
+  base <> X31 -> r1 <> X31 -> r1 <> PC ->
+  exists rs',
+     exec_straight ge fn (indexed_memory_access mk_instr base ofs k) rs m k rs' m'
+  /\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r.
 Proof.
-  intros. unfold eval_testcond. repeat rewrite nextinstr_inv; auto with asmgen.
+  intros until m; intros EXEC; intros until m'; intros STORE NOT31 NOT31' NOTPC.
+  exploit indexed_memory_access_correct; eauto.
+  intros (base' & ofs' & rs' & A & B & C).
+  econstructor; split.
+  eapply exec_straight_opt_right. eexact A. apply exec_straight_one. rewrite EXEC.
+  unfold exec_store. rewrite B, C, STORE by auto. eauto. auto. 
+  intros; Simpl.
 Qed.
 
-Remark eval_testcond_set_ireg:
-  forall c rs r v, eval_testcond c (rs#(IR r) <- v) = eval_testcond c rs.
+Lemma loadind_correct:
+  forall (base: ireg) ofs ty dst k c (rs: regset) m v,
+  loadind base ofs ty dst k = OK c ->
+  Mem.loadv (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) = Some v ->
+  base <> X31 ->
+  exists rs',
+     exec_straight ge fn c rs m k rs' m
+  /\ rs'#(preg_of dst) = v
+  /\ forall r, r <> PC -> r <> X31 -> r <> preg_of dst -> rs'#r = rs#r.
 Proof.
-  intros. unfold eval_testcond. repeat rewrite Pregmap.gso; auto with asmgen.
+  intros until v; intros TR LOAD NOT31. 
+  assert (A: exists mk_instr,
+                c = indexed_memory_access mk_instr base ofs k
+             /\ forall base' ofs' rs',
+                   exec_instr ge fn (mk_instr base' ofs') rs' m =
+                   exec_load ge (chunk_of_type ty) rs' m (preg_of dst) base' ofs').
+  { unfold loadind in TR. destruct ty, (preg_of dst); inv TR; econstructor; split; eauto. }
+  destruct A as (mk_instr & B & C). subst c. 
+  eapply indexed_load_access_correct; eauto with asmgen. 
 Qed.
 
-Lemma mk_setcc_base_correct:
-  forall cond rd k rs1 m,
-  exists rs2,
-  exec_straight ge fn (mk_setcc_base cond rd k) rs1 m k rs2 m
-  /\ rs2#rd = Val.of_optbool(eval_extcond cond rs1)
-  /\ forall r, data_preg r = true -> r <> RAX /\ r <> RCX -> r <> rd -> rs2#r = rs1#r.
+Lemma storeind_correct:
+  forall (base: ireg) ofs ty src k c (rs: regset) m m',
+  storeind src base ofs ty k = OK c ->
+  Mem.storev (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) rs#(preg_of src) = Some m' ->
+  base <> X31 ->
+  exists rs',
+     exec_straight ge fn c rs m k rs' m'
+  /\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r.
 Proof.
-  intros. destruct cond; simpl in *.
-- (* base *)
-  econstructor; split.
-  apply exec_straight_one. simpl; eauto. auto.
-  split. Simplifs. intros; Simplifs.
-- (* or *)
-  assert (Val.of_optbool
-    match eval_testcond c1 rs1 with
-    | Some b1 =>
-        match eval_testcond c2 rs1 with
-        | Some b2 => Some (b1 || b2)
-        | None => None
-        end
-    | None => None
-    end =
-    Val.or (Val.of_optbool (eval_testcond c1 rs1)) (Val.of_optbool (eval_testcond c2 rs1))).
-  destruct (eval_testcond c1 rs1). destruct (eval_testcond c2 rs1).
-  destruct b; destruct b0; auto.
-  destruct b; auto.
-  auto.
-  rewrite H; clear H.
-  destruct (ireg_eq rd RAX).
-  subst rd. 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.
-  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. Simplifs. rewrite Val.or_commut. decEq; Simplifs.
-  intros. destruct H0; Simplifs.
-- (* and *)
-  assert (Val.of_optbool
-    match eval_testcond c1 rs1 with
-    | Some b1 =>
-        match eval_testcond c2 rs1 with
-        | Some b2 => Some (b1 && b2)
-        | None => None
-        end
-    | None => None
-    end =
-    Val.and (Val.of_optbool (eval_testcond c1 rs1)) (Val.of_optbool (eval_testcond c2 rs1))).
-  {
-    destruct (eval_testcond c1 rs1). destruct (eval_testcond c2 rs1).
-    destruct b; destruct b0; auto.
-    destruct b; auto.
-    auto.
-  }
-  rewrite H; clear H.
-  destruct (ireg_eq rd RAX).
-  subst rd. 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.
-  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. Simplifs. rewrite Val.and_commut. decEq; Simplifs.
-  intros. destruct H0; Simplifs.
+  intros until m'; intros TR STORE NOT31. 
+  assert (A: exists mk_instr,
+                c = indexed_memory_access mk_instr base ofs k
+             /\ forall base' ofs' rs',
+                   exec_instr ge fn (mk_instr base' ofs') rs' m =
+                   exec_store ge (chunk_of_type ty) rs' m (preg_of src) base' ofs').
+  { unfold storeind in TR. destruct ty, (preg_of src); inv TR; econstructor; split; eauto. }
+  destruct A as (mk_instr & B & C). subst c. 
+  eapply indexed_store_access_correct; eauto with asmgen. 
 Qed.
 
-Lemma mk_setcc_correct:
-  forall cond rd k rs1 m,
-  exists rs2,
-  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, data_preg r = true -> r <> RAX /\ r <> RCX -> r <> rd -> rs2#r = rs1#r.
+Lemma loadind_ptr_correct:
+  forall (base: ireg) ofs (dst: ireg) k (rs: regset) m v,
+  Mem.loadv Mptr m (Val.offset_ptr rs#base ofs) = Some v ->
+  base <> X31 ->
+  exists rs',
+     exec_straight ge fn (loadind_ptr base ofs dst k) rs m k rs' m
+  /\ rs'#dst = v
+  /\ forall r, r <> PC -> r <> X31 -> r <> dst -> rs'#r = rs#r.
 Proof.
-  intros. unfold mk_setcc. destruct (Archi.ptr64 || low_ireg rd).
-- apply mk_setcc_base_correct.
-- exploit mk_setcc_base_correct. intros [rs2 [A [B C]]].
-  econstructor; split. eapply exec_straight_trans. eexact A. apply exec_straight_one.
-    simpl. eauto. simpl. auto.
-  intuition Simplifs.
+  intros. eapply indexed_load_access_correct; eauto with asmgen.
+  intros. unfold Mptr. destruct Archi.ptr64; auto. 
 Qed.
 
-Definition negate_extcond (xc: extcond) : extcond :=
-  match xc with
-  | Cond_base c => Cond_base (negate_testcond c)
-  | Cond_and c1 c2 => Cond_or (negate_testcond c1) (negate_testcond c2)
-  | Cond_or c1 c2 => Cond_and (negate_testcond c1) (negate_testcond c2)
-  end.
-
-Remark negate_testcond_for_condition:
-  forall cond,
-  negate_extcond (testcond_for_condition cond) = testcond_for_condition (negate_condition cond).
+Lemma storeind_ptr_correct:
+  forall (base: ireg) ofs (src: ireg) k (rs: regset) m m',
+  Mem.storev Mptr m (Val.offset_ptr rs#base ofs) rs#src = Some m' ->
+  base <> X31 -> src <> X31 ->
+  exists rs',
+     exec_straight ge fn (storeind_ptr src base ofs k) rs m k rs' m'
+  /\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r.
 Proof.
-  intros. destruct cond; try destruct c; reflexivity.
+  intros. eapply indexed_store_access_correct with (r1 := src); eauto with asmgen.
+  intros. unfold Mptr. destruct Archi.ptr64; auto. 
 Qed.
 
-Lemma mk_sel_correct:
-  forall xc ty rd r2 k c ob rs m,
-  mk_sel xc rd r2 k = OK c ->
-  rd <> r2 ->
-  match ob with
-  | Some b => eval_extcond xc rs = Some b /\ eval_extcond (negate_extcond xc) rs = Some (negb b)
-  | None => True
-  end ->
-  exists rs',
-     exec_straight ge fn c rs m k rs' m
-  /\ Val.lessdef (Val.select ob rs#rd rs#r2 ty) rs'#rd
-  /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs r.
+Lemma transl_memory_access_correct:
+  forall mk_instr addr args k c (rs: regset) m v,
+  transl_memory_access mk_instr addr args k = OK c ->
+  eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
+  exists base ofs rs',
+     exec_straight_opt ge fn c rs m (mk_instr base ofs :: k) rs' m
+  /\ Val.offset_ptr rs'#base (eval_offset ge ofs) = v
+  /\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r.
 Proof.
-  intros. destruct xc; monadInv H; simpl in H1.
-- econstructor; split.
-  eapply exec_straight_one. reflexivity. reflexivity.
-  set (v :=  match eval_testcond (negate_testcond c0) rs with
-     | Some true => rs r2
-     | Some false => rs rd
-     | None => Vundef
-     end).
-  split. rewrite nextinstr_inv, Pregmap.gss by eauto with asmgen.
-  destruct ob; simpl; auto. destruct H1 as [_ B]; unfold v; rewrite B. 
-  destruct b; apply Val.lessdef_normalize.
-  intros; Simplifs.
-- econstructor; split.
-  eapply exec_straight_two. 
-  reflexivity. reflexivity. reflexivity. reflexivity.
-  set (v1 :=  match eval_testcond (negate_testcond c1) rs with
-     | Some true => rs r2
-     | Some false => rs rd
-     | None => Vundef
-     end).
-  rewrite eval_testcond_nextinstr, eval_testcond_set_ireg. 
-  set (v2 :=  match eval_testcond (negate_testcond c2) rs with
-     | Some true => nextinstr rs # rd <- v1 r2
-     | Some false => nextinstr rs # rd <- v1 rd
-     | None => Vundef
-     end).
-  split. rewrite nextinstr_inv, Pregmap.gss by eauto with asmgen.
-  destruct ob; simpl; auto.
-  destruct H1 as [_ B]. 
-  destruct (eval_testcond (negate_testcond c1) rs) as [b1|]; try discriminate.
-  destruct (eval_testcond (negate_testcond c2) rs) as [b2|]; try discriminate.
-  inv B. apply negb_sym in H1. subst b.
-  replace v2 with (if b2 then rs#r2 else v1).
-  unfold v1. destruct b1, b2; apply Val.lessdef_normalize.
-  unfold v2. destruct b2; symmetry; Simplifs.
-  intros; Simplifs.
+  intros until v; intros TR EV. 
+  unfold transl_memory_access in TR; destruct addr; ArgsInv.
+- (* indexed *)
+  inv EV. apply indexed_memory_access_correct; eauto with asmgen.
+- (* global *)
+  simpl in EV. inv EV. inv TR.  econstructor; econstructor; econstructor; split.
+  constructor. apply exec_straight_one. simpl; eauto. auto. 
+  split; intros; Simpl. unfold eval_offset. apply low_high_half.
+- (* stack *)
+  inv TR. inv EV. apply indexed_memory_access_correct; eauto with asmgen.
 Qed.
 
-Lemma transl_sel_correct:
-  forall ty cond args rd r2 k c rs m,
-  transl_sel cond args rd r2 k = OK c ->
+Lemma transl_load_access_correct:
+  forall chunk (mk_instr: ireg -> offset -> instruction) addr args k c rd (rs: regset) m v v',
+  (forall base ofs rs,
+     exec_instr ge fn (mk_instr base ofs) rs m = exec_load ge chunk rs m rd base ofs) ->
+  transl_memory_access mk_instr addr args k = OK c ->
+  eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
+  Mem.loadv chunk m v = Some v' ->
+  rd <> PC ->
   exists rs',
      exec_straight ge fn c rs m k rs' m
-  /\ Val.lessdef (Val.select (eval_condition cond (map rs (map preg_of args)) m) rs#rd rs#r2 ty) rs'#rd
-  /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs r.
+  /\ rs'#rd = v'
+  /\ forall r, r <> PC -> r <> X31 -> r <> rd -> rs'#r = rs#r.
 Proof.
-  unfold transl_sel; intros. destruct (ireg_eq rd r2); monadInv H. 
-- econstructor; split. 
-  apply exec_straight_one; reflexivity.
-  split. rewrite nextinstr_inv, Pregmap.gss by auto with asmgen. 
-  destruct eval_condition as [[]|]; simpl; auto using Val.lessdef_normalize.
-  intros; Simplifs.
-- destruct (transl_cond_correct _ _ _ _ rs m EQ0) as (rs1 & A & B & C).
-  rewrite <- negate_testcond_for_condition in B.
-  destruct (mk_sel_correct _ ty _ _ _ _ _ rs1 m EQ n B) as (rs2 & D & E & F).
-  exists rs2; split. 
-  eapply exec_straight_trans; eauto. 
-  split. rewrite ! C in E by auto with asmgen. exact E.
-  intros. rewrite F; auto.
+  intros until v'; intros INSTR TR EV LOAD NOTPC. 
+  exploit transl_memory_access_correct; eauto.
+  intros (base & ofs & rs' & A & B & C).
+  econstructor; split.
+  eapply exec_straight_opt_right. eexact A. apply exec_straight_one. 
+  rewrite INSTR. unfold exec_load. rewrite B, LOAD. reflexivity. Simpl. 
+  split; intros; Simpl.
 Qed.
 
-(** Translation of arithmetic operations. *)
-
-Ltac ArgsInv :=
-  match goal with
-  | [ H: Error _ = OK _ |- _ ] => discriminate
-  | [ H: match ?args with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct args; ArgsInv
-  | [ H: bind _ _ = OK _ |- _ ] => monadInv H; ArgsInv
-  | [ H: match _ with left _ => _ | right _ => assertion_failed end = OK _ |- _ ] => monadInv H; ArgsInv
-  | [ H: match _ with true => _ | false => assertion_failed end = OK _ |- _ ] => monadInv H; ArgsInv
-  | [ H: ireg_of _ = OK _ |- _ ] => simpl in *; rewrite (ireg_of_eq _ _ H) in *; 
-                                    let X := fresh "EQ" in generalize (ireg_of_eq _ _ H); intros X;
-                                    clear H; ArgsInv
-  | [ H: freg_of _ = OK _ |- _ ] => simpl in *; rewrite (freg_of_eq _ _ H) in *; clear H; ArgsInv
-  | _ => idtac
-  end.
-
-Ltac TranslOp :=
-  econstructor; split;
-  [ apply exec_straight_one; [ simpl; eauto | auto ]
-  | 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#RSP) op (map rs (map preg_of args)) m = Some v ->
+Lemma transl_store_access_correct:
+  forall chunk (mk_instr: ireg -> offset -> instruction) addr args k c r1 (rs: regset) m v m',
+  (forall base ofs rs,
+     exec_instr ge fn (mk_instr base ofs) rs m = exec_store ge chunk rs m r1 base ofs) ->
+  transl_memory_access mk_instr addr args k = OK c ->
+  eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
+  Mem.storev chunk m v rs#r1 = Some m' ->
+  r1 <> PC -> r1 <> X31 ->
   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.
+     exec_straight ge fn c rs m k rs' m'
+  /\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r.
 Proof.
-Transparent destroyed_by_op.
-  intros until v; intros TR EV.
-  assert (SAME:
-  (exists rs',
-     exec_straight ge fn c rs m k rs' m
-  /\ rs'#(preg_of res) = v
-  /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r) ->
-  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).
-  {
-    intros [rs' [A [B C]]]. subst v. exists rs'; auto.
-  }
-
-  destruct op; simpl in TR; ArgsInv; simpl in EV; try (inv EV); try (apply SAME; TranslOp; fail).
-(* move *)
-  exploit mk_mov_correct; eauto. intros [rs2 [A [B C]]].
-  apply SAME. exists rs2. eauto.
-(* intconst *)
-  apply SAME. destruct (Int.eq_dec n Int.zero). subst n. TranslOp. TranslOp.
-(* longconst *)
-  apply SAME. destruct (Int64.eq_dec n Int64.zero). subst n. TranslOp. TranslOp.
-(* floatconst *)
-  apply SAME. destruct (Float.eq_dec n Float.zero). subst n. TranslOp. TranslOp.
-(* singleconst *)
-  apply SAME. destruct (Float32.eq_dec n Float32.zero). subst n. TranslOp. TranslOp.
-(* cast8signed *)
-  apply SAME. eapply mk_intconv_correct; eauto.
-(* cast8unsigned *)
-  apply SAME. eapply mk_intconv_correct; eauto.
-(* mulhs *)
-  apply SAME. TranslOp. destruct H1. Simplifs.
-(* mulhu *)
-  apply SAME. TranslOp. destruct H1. Simplifs.
-(* div *)
-  apply SAME.
-  exploit (divs_mods_exists (rs RAX) (rs RCX)). left; congruence.
-  intros (nh & nl & d & q & r & A & B & C & D & E & F).
-  set (rs1 := nextinstr_nf (rs#RDX <- (Vint nh))).
-  econstructor; split.
-  eapply exec_straight_two with (rs2 := rs1). simpl. rewrite A. reflexivity.
-  simpl. change (rs1 RAX) with (rs RAX); rewrite B.
-  change (rs1 RCX) with (rs RCX); rewrite C.
-  rewrite D. reflexivity. auto. auto.
-  split. change (Vint q = v). congruence.
-  simpl; intros. destruct H2. unfold rs1; Simplifs.
-(* divu *)
-  apply SAME.
-  exploit (divu_modu_exists (rs RAX) (rs RCX)). left; congruence.
-  intros (n & d & q & r & B & C & D & E & F).
-  set (rs1 := nextinstr_nf (rs#RDX <- Vzero)).
-  econstructor; split.
-  eapply exec_straight_two with (rs2 := rs1). reflexivity.
-  simpl. change (rs1 RAX) with (rs RAX); rewrite B.
-  change (rs1 RCX) with (rs RCX); rewrite C.
-  rewrite D. reflexivity. auto. auto.
-  split. change (Vint q = v). congruence.
-  simpl; intros. destruct H2. unfold rs1; Simplifs.
-(* mod *)
-  apply SAME.
-  exploit (divs_mods_exists (rs RAX) (rs RCX)). right; congruence.
-  intros (nh & nl & d & q & r & A & B & C & D & E & F).
-  set (rs1 := nextinstr_nf (rs#RDX <- (Vint nh))).
-  econstructor; split.
-  eapply exec_straight_two with (rs2 := rs1). simpl. rewrite A. reflexivity.
-  simpl. change (rs1 RAX) with (rs RAX); rewrite B.
-  change (rs1 RCX) with (rs RCX); rewrite C.
-  rewrite D. reflexivity. auto. auto.
-  split. change (Vint r = v). congruence.
-  simpl; intros. destruct H2. unfold rs1; Simplifs.
-(* modu *)
-  apply SAME.
-  exploit (divu_modu_exists (rs RAX) (rs RCX)). right; congruence.
-  intros (n & d & q & r & B & C & D & E & F).
-  set (rs1 := nextinstr_nf (rs#RDX <- Vzero)).
-  econstructor; split.
-  eapply exec_straight_two with (rs2 := rs1). reflexivity.
-  simpl. change (rs1 RAX) with (rs RAX); rewrite B.
-  change (rs1 RCX) with (rs RCX); rewrite C.
-  rewrite D. reflexivity. auto. auto.
-  split. change (Vint r = v). congruence.
-  simpl; intros. destruct H2. unfold rs1; Simplifs.
-(* shrximm *)
-  apply SAME. eapply mk_shrximm_correct; eauto.
-(* lea *)
-  exploit transl_addressing_mode_32_correct; eauto. intros EA.
-  TranslOp. rewrite nextinstr_inv; auto with asmgen. rewrite Pregmap.gss. rewrite normalize_addrmode_32_correct; auto.
-(* mullhs *)
-  apply SAME. TranslOp. destruct H1. Simplifs.
-(* mullhu *)
-  apply SAME. TranslOp. destruct H1. Simplifs.
-(* divl *)
-  apply SAME.
-  exploit (divls_modls_exists (rs RAX) (rs RCX)). left; congruence.
-  intros (nh & nl & d & q & r & A & B & C & D & E & F).
-  set (rs1 := nextinstr_nf (rs#RDX <- (Vlong nh))).
+  intros until m'; intros INSTR TR EV STORE NOTPC NOT31. 
+  exploit transl_memory_access_correct; eauto.
+  intros (base & ofs & rs' & A & B & C).
   econstructor; split.
-  eapply exec_straight_two with (rs2 := rs1). simpl. rewrite A. reflexivity.
-  simpl. change (rs1 RAX) with (rs RAX); rewrite B.
-  change (rs1 RCX) with (rs RCX); rewrite C.
-  rewrite D. reflexivity. auto. auto.
-  split. change (Vlong q = v). congruence.
-  simpl; intros. destruct H2. unfold rs1; Simplifs.
-(* divlu *)
-  apply SAME.
-  exploit (divlu_modlu_exists (rs RAX) (rs RCX)). left; congruence.
-  intros (n & d & q & r & B & C & D & E & F).
-  set (rs1 := nextinstr_nf (rs#RDX <- (Vlong Int64.zero))).
-  econstructor; split.
-  eapply exec_straight_two with (rs2 := rs1). reflexivity.
-  simpl. change (rs1 RAX) with (rs RAX); rewrite B.
-  change (rs1 RCX) with (rs RCX); rewrite C.
-  rewrite D. reflexivity. auto. auto.
-  split. change (Vlong q = v). congruence.
-  simpl; intros. destruct H2. unfold rs1; Simplifs.
-(* modl *)
-  apply SAME.
-  exploit (divls_modls_exists (rs RAX) (rs RCX)). right; congruence.
-  intros (nh & nl & d & q & r & A & B & C & D & E & F).
-  set (rs1 := nextinstr_nf (rs#RDX <- (Vlong nh))).
-  econstructor; split.
-  eapply exec_straight_two with (rs2 := rs1). simpl. rewrite A. reflexivity.
-  simpl. change (rs1 RAX) with (rs RAX); rewrite B.
-  change (rs1 RCX) with (rs RCX); rewrite C.
-  rewrite D. reflexivity. auto. auto.
-  split. change (Vlong r = v). congruence.
-  simpl; intros. destruct H2. unfold rs1; Simplifs.
-(* modlu *)
-  apply SAME.
-  exploit (divlu_modlu_exists (rs RAX) (rs RCX)). right; congruence.
-  intros (n & d & q & r & B & C & D & E & F).
-  set (rs1 := nextinstr_nf (rs#RDX <- (Vlong Int64.zero))).
-  econstructor; split.
-  eapply exec_straight_two with (rs2 := rs1). reflexivity.
-  simpl. change (rs1 RAX) with (rs RAX); rewrite B.
-  change (rs1 RCX) with (rs RCX); rewrite C.
-  rewrite D. reflexivity. auto. auto.
-  split. change (Vlong r = v). congruence.
-  simpl; intros. destruct H2. unfold rs1; Simplifs.
-(* shrxlimm *)
-  apply SAME. eapply mk_shrxlimm_correct; eauto.
-(* leal *)
-  exploit transl_addressing_mode_64_correct; eauto. intros EA.
-  generalize (normalize_addrmode_64_correct x rs). destruct (normalize_addrmode_64 x) as [am' [delta|]]; intros EV.
-  econstructor; split. eapply exec_straight_two.
-  simpl. reflexivity.  simpl. reflexivity. auto. auto.
-  split. rewrite nextinstr_nf_inv by auto. rewrite Pregmap.gss. rewrite nextinstr_inv by auto with asmgen.
-  rewrite Pregmap.gss. rewrite <- EV; auto.
-  intros; Simplifs.
-  TranslOp. rewrite nextinstr_inv; auto with asmgen. rewrite Pregmap.gss; auto. rewrite <- EV; auto.
-(* intoffloat *)
-  apply SAME. TranslOp. rewrite H0; auto.
-(* floatofint *)
-  apply SAME. TranslOp. rewrite H0; auto.
-(* intofsingle *)
-  apply SAME. TranslOp. rewrite H0; auto.
-(* singleofint *)
-  apply SAME. TranslOp. rewrite H0; auto.
-(* longoffloat *)
-  apply SAME. TranslOp. rewrite H0; auto.
-(* floatoflong *)
-  apply SAME. TranslOp. rewrite H0; auto.
-(* longofsingle *)
-  apply SAME. TranslOp. rewrite H0; auto.
-(* singleoflong *)
-  apply SAME. TranslOp. rewrite H0; auto.
-(* condition *)
-  exploit transl_cond_correct; eauto. intros [rs2 [P [Q R]]].
-  exploit mk_setcc_correct; eauto. intros [rs3 [S [T U]]].
-  exists rs3.
-  split. eapply exec_straight_trans. eexact P. eexact S.
-  split. rewrite T. destruct (eval_condition cond rs ## (preg_of ## args) m).
-  destruct Q as [Q _]. rewrite Q. auto.
-  simpl; auto.
-  intros. transitivity (rs2 r); auto.
-(* selection *)
-  rewrite EQ1. exploit transl_sel_correct; eauto. intros (rs' & A & B & C).
-  exists rs'; split. eexact A. eauto.
+  eapply exec_straight_opt_right. eexact A. apply exec_straight_one. 
+  rewrite INSTR. unfold exec_store. rewrite B, C, STORE by auto. reflexivity. auto.
+  intros; Simpl.
 Qed.
 
-(** Translation of memory loads. *)
-
 Lemma transl_load_correct:
-  forall trap chunk addr args dest k c (rs: regset) m a v,
-  transl_load trap chunk addr args dest k = OK c ->
-  eval_addressing ge (rs#RSP) addr (map rs (map preg_of args)) = Some a ->
+  forall trap chunk addr args dst k c (rs: regset) m a v,
+  transl_load trap chunk addr args dst k = OK c ->
+  eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some a ->
   Mem.loadv chunk m a = Some v ->
   exists rs',
      exec_straight ge fn c rs m k rs' m
-  /\ rs'#(preg_of dest) = v
-  /\ forall r, data_preg r = true -> r <> preg_of dest -> rs'#r = rs#r.
+  /\ rs'#(preg_of dst) = v
+  /\ forall r, r <> PC -> r <> X31 -> r <> preg_of dst -> rs'#r = rs#r.
 Proof.
-  unfold transl_load; intros.
-  destruct trap; simpl; try discriminate.
-  monadInv H.
-  exploit transl_addressing_mode_correct; eauto. intro EA.
-  assert (EA': eval_addrmode ge x rs = a). destruct a; simpl in H1; try discriminate; inv EA; auto.
-  set (rs2 := nextinstr_nf (rs#(preg_of dest) <- v)).
-  assert (exec_load ge chunk m x rs (preg_of dest) = Next rs2 m).
-    unfold exec_load. rewrite EA'. rewrite H1. auto.
-  assert (rs2 PC = Val.offset_ptr (rs PC) Ptrofs.one).
-    transitivity (Val.offset_ptr ((rs#(preg_of dest) <- v) PC) Ptrofs.one).
-    auto. decEq. apply Pregmap.gso; auto with asmgen.
-  exists rs2. split.
-  destruct chunk; ArgsInv; apply exec_straight_one; auto.
-  split. unfold rs2. rewrite nextinstr_nf_inv1. Simplifs. apply preg_of_data.
-  intros. unfold rs2. Simplifs.
+  intros until v; intros TR EV LOAD.
+  destruct trap; try (simpl in *; discriminate).
+  assert (A: exists mk_instr,
+      transl_memory_access mk_instr addr args k = OK c
+   /\ forall base ofs rs,
+        exec_instr ge fn (mk_instr base ofs) rs m = exec_load ge chunk rs m (preg_of dst) base ofs).
+  { unfold transl_load in TR; destruct chunk; ArgsInv; econstructor; (split; [eassumption|auto]). }
+  destruct A as (mk_instr & B & C).
+  eapply transl_load_access_correct; eauto with asmgen.
 Qed.
 
 Lemma transl_store_correct:
   forall chunk addr args src k c (rs: regset) m a m',
   transl_store chunk addr args src k = OK c ->
-  eval_addressing ge (rs#RSP) addr (map rs (map preg_of args)) = Some a ->
-  Mem.storev chunk m a (rs (preg_of src)) = Some m' ->
+  eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some a ->
+  Mem.storev chunk m a rs#(preg_of src) = Some m' ->
   exists rs',
      exec_straight ge fn c rs m k rs' m'
-  /\ forall r, data_preg r = true -> preg_notin r (destroyed_by_store chunk addr) -> rs'#r = rs#r.
+  /\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r.
 Proof.
-  unfold transl_store; intros. monadInv H.
-  exploit transl_addressing_mode_correct; eauto. intro EA.
-  assert (EA': eval_addrmode ge x rs = a). destruct a; simpl in H1; try discriminate; inv EA; auto.
-  rewrite <- EA' in H1. destruct chunk; ArgsInv.
-(* int8signed *)
-  eapply mk_storebyte_correct; eauto.
-  destruct (eval_addrmode ge x rs); simpl; auto. rewrite <- Mem.store_signed_unsigned_8; auto.
-(* int8unsigned *)
-  eapply mk_storebyte_correct; eauto.
-(* int16signed *)
-  econstructor; split.
-  apply exec_straight_one. simpl. unfold exec_store.
-  replace (Mem.storev Mint16unsigned m (eval_addrmode ge x rs) (rs x0))
-     with (Mem.storev Mint16signed m (eval_addrmode ge x rs) (rs x0)).
-  rewrite H1. eauto.
-  destruct (eval_addrmode ge x rs); simpl; auto. rewrite Mem.store_signed_unsigned_16; auto.
-  auto.
-  intros. Simplifs.
-(* int16unsigned *)
-  econstructor; split.
-  apply exec_straight_one. simpl. unfold exec_store. rewrite H1. eauto. auto.
-  intros. Simplifs.
-(* int32 *)
-  econstructor; split.
-  apply exec_straight_one. simpl. unfold exec_store. rewrite H1. eauto. auto.
-  intros. Simplifs.
-(* int64 *)
-  econstructor; split.
-  apply exec_straight_one. simpl. unfold exec_store. rewrite H1. eauto. auto.
-  intros. Simplifs.
-(* float32 *)
-  econstructor; split.
-  apply exec_straight_one. simpl. unfold exec_store. rewrite H1. eauto. auto.
-  intros. Transparent destroyed_by_store. simpl in H2. simpl. Simplifs.
-(* float64 *)
-  econstructor; split.
-  apply exec_straight_one. simpl. unfold exec_store. rewrite H1. eauto. auto.
-  intros. Simplifs.
+  intros until m'; intros TR EV STORE. 
+  assert (A: exists mk_instr chunk',
+      transl_memory_access mk_instr addr args k = OK c
+   /\ (forall base ofs rs,
+        exec_instr ge fn (mk_instr base ofs) rs m = exec_store ge chunk' rs m (preg_of src) base ofs)
+   /\ Mem.storev chunk m a rs#(preg_of src) = Mem.storev chunk' m a rs#(preg_of src)).
+  { unfold transl_store in TR; destruct chunk; ArgsInv;
+    (econstructor; econstructor; split; [eassumption | split; [ intros; simpl; reflexivity | auto]]).
+    destruct a; auto. apply Mem.store_signed_unsigned_8. 
+    destruct a; auto. apply Mem.store_signed_unsigned_16. 
+  }
+  destruct A as (mk_instr & chunk' & B & C & D).
+  rewrite D in STORE; clear D. 
+  eapply transl_store_access_correct; eauto with asmgen.
+Qed.
+
+(** Function epilogues *)
+
+Lemma make_epilogue_correct:
+  forall ge0 f m stk soff cs m' ms rs k tm,
+  load_stack m (Vptr stk soff) Tptr f.(fn_link_ofs) = Some (parent_sp 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 ->
+  match_stack ge0 cs ->
+  exists rs', exists tm',
+     exec_straight ge fn (make_epilogue f k) rs tm k rs' tm'
+  /\ agree ms (parent_sp cs) rs'
+  /\ Mem.extends m' tm'
+  /\ rs'#RA = parent_ra cs
+  /\ rs'#SP = parent_sp cs
+  /\ (forall r, r <> PC -> r <> RA -> r <> SP -> r <> X31 -> rs'#r = rs#r).
+Proof.
+  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. 
+  rewrite chunk_of_Tptr in *. 
+  exploit (loadind_ptr_correct SP (fn_retaddr_ofs f) RA (Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: k) rs tm).
+    rewrite <- (sp_val _ _ _ AG). simpl. eexact LRA'. congruence.
+  intros (rs1 & A1 & B1 & C1).
+  econstructor; econstructor; split.
+  eapply exec_straight_trans. eexact A1. apply exec_straight_one. simpl. 
+    rewrite (C1 X2) by auto with asmgen. rewrite <- (sp_val _ _ _ AG). simpl; rewrite LP'. 
+    rewrite FREE'. eauto. auto. 
+  split. apply agree_nextinstr. apply agree_set_other; auto with asmgen. 
+    apply agree_change_sp with (Vptr stk soff).
+    apply agree_exten with rs; auto. intros; apply C1; auto with asmgen.
+    eapply parent_sp_def; eauto.
+  split. auto.
+  split. Simpl. 
+  split. Simpl. 
+  intros. Simpl. 
 Qed.
 
 End CONSTRUCTORS.