k1c -> kvx changes

1 files changed, 2499 insertions, 0 deletions

diff --git a/kvx/Asmblockgenproof1.v b/kvx/Asmblockgenproof1.v
new file mode 100644
index 00000000..74b9b62b
--- /dev/null
+++ b/kvx/Asmblockgenproof1.v
@@ -0,0 +1,2499 @@
+(* *************************************************************)
+(*                                                             *)
+(*             The Compcert verified compiler                  *)
+(*                                                             *)
+(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
+(*           Xavier Leroy       INRIA Paris-Rocquencourt       *)
+(*           David Monniaux     CNRS, VERIMAG                  *)
+(*           Cyril Six          Kalray                         *)
+(*                                                             *)
+(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
+(*  This file is distributed under the terms of the INRIA      *)
+(*  Non-Commercial License Agreement.                          *)
+(*                                                             *)
+(* *************************************************************)
+
+(** * Proof of correctness for individual instructions *)
+
+Require Import Coqlib Errors Maps.
+Require Import AST Integers Floats Values Memory Globalenvs.
+Require Import Op Locations Machblock Conventions.
+Require Import Asmblock Asmblockgen Asmblockgenproof0 Asmblockprops.
+Require Import Chunks.
+
+Import PArithCoercions.
+
+(** Decomposition of integer constants. *)
+
+Lemma make_immed32_sound:
+  forall n,
+  match make_immed32 n with
+  | Imm32_single imm => n = imm
+  end.
+Proof.
+  intros; unfold make_immed32. set (lo := Int.sign_ext 12 n).
+  predSpec Int.eq Int.eq_spec n lo; auto.
+Qed.
+
+Lemma make_immed64_sound:
+  forall n,
+  match make_immed64 n with
+  | Imm64_single imm => n = imm
+  end.
+Proof.
+  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.
+
+
+(** Properties of registers *)
+
+Lemma ireg_of_not_RTMP:
+  forall m r, ireg_of m = OK r -> IR r <> IR RTMP.
+Proof.
+  intros. erewrite <- ireg_of_eq; eauto with asmgen.
+Qed.
+
+Lemma ireg_of_not_RTMP':
+  forall m r, ireg_of m = OK r -> r <> RTMP.
+Proof.
+  intros. apply ireg_of_not_RTMP in H. congruence.
+Qed.
+
+Hint Resolve ireg_of_not_RTMP ireg_of_not_RTMP': asmgen.
+
+
+(** Useful simplification tactic *)
+
+Ltac Simplif :=
+  ((rewrite nextblock_inv by eauto with asmgen)
+  || (rewrite nextblock_inv1 by eauto with asmgen)
+  || (rewrite Pregmap.gss)
+  || (rewrite nextblock_pc)
+  || (rewrite Pregmap.gso by eauto with asmgen)
+  ); auto with asmgen.
+
+Ltac Simpl := repeat Simplif.
+
+(** * Correctness of RISC-V constructor functions *)
+
+Section CONSTRUCTORS.
+
+Variable ge: genv.
+Variable fn: function.
+
+Lemma loadimm32_correct:
+  forall rd n k rs m,
+  exists rs',
+     exec_straight ge (loadimm32 rd n ::g k) rs m k rs' m
+  /\ rs'#rd = Vint n
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
+Proof.
+  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. Simpl.
+  intros; Simpl.
+Qed.
+
+Lemma loadimm64_correct:
+  forall rd n k rs m,
+  exists rs',
+     exec_straight ge (loadimm64 rd n ::g k) rs m k rs' m
+  /\ rs'#rd = Vlong n
+  /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> rs'#r = rs#r.
+Proof.
+  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. Simpl. 
+  intros; Simpl.
+Qed.
+
+Lemma opimm64_correct:
+  forall (op: arith_name_rrr)
+         (opi: arith_name_rri64)
+         (sem: val -> val -> val) m,
+  (forall d s1 s2 rs,
+   exec_basic_instr ge (op d s1 s2) rs m = Next ((rs#d <- (sem rs#s1 rs#s2))) m) ->
+  (forall d s n rs,
+   exec_basic_instr ge (opi d s n) rs m = Next ((rs#d <- (sem rs#s (Vlong n)))) m) ->
+  forall rd r1 n k rs,
+  r1 <> RTMP ->
+  exists rs',
+     exec_straight ge (opimm64 op opi rd r1 n ::g k) rs m k rs' m
+  /\ rs'#rd = sem rs#r1 (Vlong n)
+  /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> rs'#r = rs#r.
+Proof.
+  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.
+Qed.
+
+(** Add offset to pointer *)
+
+Lemma addptrofs_correct:
+  forall rd r1 n k rs m,
+  r1 <> RTMP ->
+  exists rs',
+     exec_straight ge (addptrofs rd r1 n ::g k) rs m k rs' m
+  /\ Val.lessdef (Val.offset_ptr rs#r1 n) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> rs'#r = rs#r.
+Proof.
+  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.
+- unfold addimm64.
+  exploit (opimm64_correct Paddl Paddil Val.addl); eauto. intros (rs' & A & B & C).
+  exists rs'; split. eexact A. split; auto.
+  rewrite B. destruct (rs r1); simpl; auto.
+  rewrite Ptrofs.of_int64_to_int64 by auto. auto.
+Qed.
+
+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).
+
+Inductive exec_straight_opt: list instruction -> regset -> mem -> list instruction -> regset -> mem -> Prop :=
+  | exec_straight_opt_refl: forall c rs m,
+      exec_straight_opt c rs m c rs m
+  | exec_straight_opt_intro: forall c1 rs1 m1 c2 rs2 m2,
+      exec_straight ge c1 rs1 m1 c2 rs2 m2 ->
+      exec_straight_opt c1 rs1 m1 c2 rs2 m2.
+
+Remark exec_straight_opt_right:
+  forall c3 rs3 m3 c1 rs1 m1 c2 rs2 m2,
+  exec_straight_opt c1 rs1 m1 c2 rs2 m2 ->
+  exec_straight ge c2 rs2 m2 c3 rs3 m3 ->
+  exec_straight ge c1 rs1 m1 c3 rs3 m3.
+Proof.
+  destruct 1; intros. auto. eapply exec_straight_trans; eauto. 
+Qed.
+
+Lemma transl_comp_correct:
+  forall cmp r1 r2 lbl k rs m tbb b,
+  exists rs',
+     exec_straight ge (transl_comp cmp Signed r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
+  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
+  /\ ( Val.cmp_bool cmp rs#r1 rs#r2 = Some b ->
+       exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
+        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
+  .
+Proof.
+  intros. esplit. split.
+- unfold transl_comp. apply exec_straight_one; simpl; eauto.
+- split.
+  + intros; Simpl.
+  + intros.
+    remember (rs # RTMP <- (compare_int (itest_for_cmp cmp Signed) rs # r1 rs # r2)) as rs'.
+    simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+    { 
+      assert ((nextblock tbb rs') # RTMP = (compare_int (itest_for_cmp cmp Signed) rs # r1 rs # r2)).
+      { rewrite Heqrs'. auto. }
+      rewrite H0. rewrite <- H.
+      remember (Val.cmp_bool cmp rs#r1 rs#r2) as cmpbool.
+      destruct cmp; simpl;
+      unfold Val.cmp; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
+      destruct b0; simpl; auto.
+    }
+    rewrite H0. simpl; auto.
+Qed.
+
+Lemma transl_compi_correct:
+  forall cmp r1 n lbl k rs m tbb b,
+  exists rs',
+     exec_straight ge (transl_compi cmp Signed r1 n lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
+  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
+  /\ ( Val.cmp_bool cmp rs#r1 (Vint n) = Some b ->
+       exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
+        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
+  .
+Proof.
+  intros. esplit. split.
+- unfold transl_compi. apply exec_straight_one; simpl; eauto.
+- split.
+  + intros; Simpl.
+  + intros.
+    remember (rs # RTMP <- (compare_int (itest_for_cmp cmp Signed) rs # r1 (Vint n))) as rs'.
+    simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+    { 
+      assert ((nextblock tbb rs') # RTMP = (compare_int (itest_for_cmp cmp Signed) rs # r1 (Vint n))).
+      { rewrite Heqrs'. auto. }
+      rewrite H0. rewrite <- H.
+      remember (Val.cmp_bool cmp rs#r1 (Vint n)) as cmpbool.
+      destruct cmp; simpl;
+      unfold Val.cmp; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
+      destruct b0; simpl; auto.
+    }
+    rewrite H0. simpl; auto.
+Qed.
+
+Lemma transl_compu_correct:
+  forall cmp r1 r2 lbl k rs m tbb b,
+  exists rs',
+     exec_straight ge (transl_comp cmp Unsigned r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
+  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
+  /\ (Val_cmpu_bool cmp rs#r1 rs#r2 = Some b ->
+       exec_control ge fn (Some (PCtlFlow ((Pcb BTwnez RTMP lbl)))) (nextblock tbb rs') m
+        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
+  .
+Proof.
+  intros. esplit. split.
+- unfold transl_comp. apply exec_straight_one; simpl; eauto.
+- split.
+  + intros; Simpl.
+  + intros.
+    remember (rs # RTMP <- (compare_int (itest_for_cmp cmp Unsigned) rs # r1 rs # r2)) as rs'.
+    simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+    { 
+      assert ((nextblock tbb rs') # RTMP = (compare_int (itest_for_cmp cmp Unsigned) rs # r1 rs # r2)).
+      { rewrite Heqrs'. auto. }
+      rewrite H0. rewrite <- H.
+      remember (Val_cmpu_bool cmp rs#r1 rs#r2) as cmpubool.
+      destruct cmp; simpl; unfold Val_cmpu;
+        rewrite <- Heqcmpubool; destruct cmpubool; simpl; auto;
+      destruct b0; simpl; auto.
+    }
+    rewrite H0. simpl; auto.
+Qed.
+
+Lemma transl_compui_correct:
+  forall cmp r1 n lbl k rs m tbb b,
+  exists rs',
+     exec_straight ge (transl_compi cmp Unsigned r1 n lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
+  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
+  /\ (Val_cmpu_bool cmp rs#r1 (Vint n) = Some b ->
+       exec_control ge fn (Some (PCtlFlow ((Pcb BTwnez RTMP lbl)))) (nextblock tbb rs') m
+        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
+  .
+Proof.
+  intros. esplit. split.
+- unfold transl_compi. apply exec_straight_one; simpl; eauto.
+- split.
+  + intros; Simpl.
+  + intros.
+    remember (rs # RTMP <- (compare_int (itest_for_cmp cmp Unsigned) rs # r1 (Vint n))) as rs'.
+    simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+    { 
+      assert ((nextblock tbb rs') # RTMP = (compare_int (itest_for_cmp cmp Unsigned) rs # r1 (Vint n))).
+      { rewrite Heqrs'. auto. }
+      rewrite H0. rewrite <- H.
+      remember (Val_cmpu_bool cmp rs#r1 (Vint n)) as cmpubool.
+      destruct cmp; simpl; unfold Val_cmpu;
+        rewrite <- Heqcmpubool; destruct cmpubool; simpl; auto;
+      destruct b0; simpl; auto.
+    }
+    rewrite H0. simpl; auto.
+Qed.
+
+Lemma transl_compl_correct:
+  forall cmp r1 r2 lbl k rs m tbb b,
+  exists rs',
+     exec_straight ge (transl_compl cmp Signed r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
+  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
+  /\ ( Val.cmpl_bool cmp rs#r1 rs#r2 = Some b ->
+       exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
+        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
+  .
+Proof.
+  intros. esplit. split.
+- unfold transl_compl. apply exec_straight_one; simpl; eauto.
+- split.
+  + intros; Simpl.
+  + intros.
+    remember (rs # RTMP <- (compare_long (itest_for_cmp cmp Signed) rs # r1 rs # r2)) as rs'.
+    simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+    { 
+      assert ((nextblock tbb rs') # RTMP = (compare_long (itest_for_cmp cmp Signed) rs # r1 rs # r2)).
+      { rewrite Heqrs'. auto. }
+      rewrite H0. rewrite <- H.
+      remember (Val.cmpl_bool cmp rs#r1 rs#r2) as cmpbool.
+      destruct cmp; simpl;
+      unfold compare_long, Val.cmpl;
+      rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
+      destruct b0; simpl; auto.
+    }
+    rewrite H0. simpl; auto.
+Qed.
+
+Lemma transl_compil_correct:
+  forall cmp r1 n lbl k rs m tbb b,
+  exists rs',
+     exec_straight ge (transl_compil cmp Signed r1 n lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
+  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
+  /\ ( Val.cmpl_bool cmp rs#r1 (Vlong n) = Some b ->
+       exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
+        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
+  .
+Proof.
+  intros. esplit. split.
+- unfold transl_compil. apply exec_straight_one; simpl; eauto.
+- split.
+  + intros; Simpl.
+  + intros.
+    remember (rs # RTMP <- (compare_long (itest_for_cmp cmp Signed) rs # r1 (Vlong n))) as rs'.
+    simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+    { 
+      assert ((nextblock tbb rs') # RTMP = (compare_long (itest_for_cmp cmp Signed) rs # r1 (Vlong n))).
+      { rewrite Heqrs'. auto. }
+      rewrite H0. rewrite <- H.
+      remember (Val.cmpl_bool cmp rs#r1 (Vlong n)) as cmpbool.
+      destruct cmp; simpl;
+      unfold compare_long, Val.cmpl;
+      rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
+      destruct b0; simpl; auto.
+    }
+    rewrite H0. simpl; auto.
+Qed.
+
+Lemma swap_comparison_cmpf_eq:
+  forall v1 v2 cmp,
+  (Val.cmpf cmp v1 v2) = (Val.cmpf (swap_comparison cmp) v2 v1).
+Proof.
+  intros. unfold Val.cmpf. unfold Val.cmpf_bool. destruct v1; destruct v2; auto.
+  rewrite Float.cmp_swap. auto.
+Qed.
+
+Lemma swap_comparison_cmpf_bool:
+  forall cmp ft v1 v2,
+  ftest_for_cmp cmp = Reversed ft ->
+  Val.cmpf_bool cmp v1 v2 = Val.cmpf_bool (swap_comparison cmp) v2 v1.
+Proof.
+  intros. unfold Val.cmpf_bool. destruct v1; destruct v2; auto. rewrite Float.cmp_swap. reflexivity.
+Qed.
+
+Lemma transl_compf_correct:
+  forall cmp r1 r2 lbl k rs m tbb b,
+  exists rs',
+     exec_straight ge (transl_comp_float64 cmp r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
+  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
+  /\ ( Val.cmpf_bool cmp rs#r1 rs#r2 = Some b ->
+       exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
+        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
+  .
+Proof.
+  intros. unfold transl_comp_float64. destruct (ftest_for_cmp cmp) eqn:FT.
+  * esplit. split.
+    - apply exec_straight_one; simpl; eauto.
+    - split.
+      + intros; Simpl.
+      + intros. remember (rs # RTMP <- (compare_float _ _ _)) as rs'.
+        simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+        { 
+          assert ((nextblock tbb rs') # RTMP = (compare_float ft (rs r1) (rs r2))).
+          { rewrite Heqrs'. auto. }
+          rewrite H0. rewrite <- H.
+          remember (Val.cmpf_bool cmp rs#r1 rs#r2) as cmpbool.
+          destruct cmp; simpl;
+          unfold compare_float;
+          unfold Val.cmpf; simpl in FT; inversion FT; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
+          destruct b0; simpl; auto.
+        }
+        rewrite H0. simpl; auto.
+  * esplit. split.
+    - apply exec_straight_one; simpl; eauto.
+    - split.
+      + intros; Simpl.
+      + intros. remember (rs # RTMP <- (compare_float _ _ _)) as rs'.
+        simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+        { 
+          assert ((nextblock tbb rs') # RTMP = (compare_float ft (rs r2) (rs r1))).
+          { rewrite Heqrs'. auto. }
+          rewrite H0. rewrite <- H.
+          remember (Val.cmpf_bool cmp rs#r1 rs#r2) as cmpbool.
+          erewrite swap_comparison_cmpf_bool in Heqcmpbool; eauto.
+          destruct cmp; simpl;
+          unfold compare_float;
+          unfold Val.cmpf; simpl in FT; inversion FT; simpl in Heqcmpbool; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
+          destruct b0; simpl; auto.
+        }
+        rewrite H0. simpl; auto.
+Qed.
+
+Lemma cmpf_bool_ne_eq:
+  forall v1 v2,
+  Val.cmpf_bool Cne v1 v2 = option_map negb (Val.cmpf_bool Ceq v1 v2).
+Proof.
+  intros. unfold Val.cmpf_bool. destruct v1; destruct v2; auto. rewrite Float.cmp_ne_eq. simpl. reflexivity.
+Qed.
+
+Lemma cmpf_bool_ne_eq_rev:
+  forall v1 v2,
+  Val.cmpf_bool Ceq v1 v2 = option_map negb (Val.cmpf_bool Cne v1 v2).
+Proof.
+  intros. unfold Val.cmpf_bool. destruct v1; destruct v2; auto. rewrite Float.cmp_ne_eq. simpl. rewrite negb_involutive. reflexivity.
+Qed.
+
+Lemma option_map_negb_negb:
+  forall v,
+  option_map negb (option_map negb v) = v.
+Proof.
+  destruct v; simpl; auto. rewrite negb_involutive. reflexivity.
+Qed.
+
+Lemma notbool_option_map_negb:
+  forall v, Val.notbool (Val.of_optbool v) = Val.of_optbool (option_map negb v).
+Proof.
+  unfold Val.notbool. unfold Val.of_optbool.
+  destruct v; auto. destruct b; auto.
+Qed.
+
+Lemma swap_comparison_cmpf_bool_notftest:
+  forall cmp ft v1 v2,
+  notftest_for_cmp cmp = Reversed ft ->
+  Val.cmpf_bool cmp v1 v2 = Val.cmpf_bool (swap_comparison cmp) v2 v1.
+Proof.
+  intros. unfold Val.cmpf_bool. destruct v1; destruct v2; auto. rewrite Float.cmp_swap. reflexivity.
+Qed.
+
+Lemma transl_compnotf_correct:
+  forall cmp r1 r2 lbl k rs m tbb b,
+  exists rs',
+     exec_straight ge (transl_comp_notfloat64 cmp r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
+  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
+  /\   (option_map negb (Val.cmpf_bool cmp rs#r1 rs#r2) = Some b ->
+       exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
+        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
+  .
+Proof.
+  intros. unfold transl_comp_notfloat64. destruct (notftest_for_cmp cmp) eqn:FT.
+  * esplit. split.
+    - apply exec_straight_one; simpl; eauto.
+    - split.
+      + intros; Simpl.
+      + intros. remember (rs # RTMP <- (compare_float _ _ _)) as rs'.
+        simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+        { 
+          assert ((nextblock tbb rs') # RTMP = (compare_float ft (rs r1) (rs r2))).
+          { rewrite Heqrs'. auto. }
+          rewrite H0. rewrite <- H.
+          remember (option_map negb (Val.cmpf_bool cmp rs#r1 rs#r2)) as cmpbool.
+          destruct cmp; simpl;
+          unfold compare_float;
+          unfold Val.cmpf; simpl in FT; inversion FT.
+          * rewrite cmpf_bool_ne_eq; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+          * rewrite cmpf_bool_ne_eq_rev. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+          * rewrite notbool_option_map_negb. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+          * rewrite notbool_option_map_negb. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+        }
+        rewrite H0. simpl; auto.
+  * esplit. split.
+    - apply exec_straight_one; simpl; eauto.
+    - split.
+      + intros; Simpl.
+      + intros. remember (rs # RTMP <- (compare_float _ _ _)) as rs'.
+        simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+        { 
+          assert ((nextblock tbb rs') # RTMP = (compare_float ft (rs r2) (rs r1))).
+          { rewrite Heqrs'. auto. }
+          rewrite H0. rewrite <- H.
+          remember (Val.cmpf_bool cmp rs#r1 rs#r2) as cmpbool.
+          erewrite swap_comparison_cmpf_bool_notftest in Heqcmpbool; eauto.
+          destruct cmp; simpl;
+          unfold compare_float;
+          unfold Val.cmpf; simpl in FT; inversion FT; simpl in Heqcmpbool.
+          * rewrite notbool_option_map_negb. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+          * rewrite notbool_option_map_negb. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+        }
+        rewrite H0. simpl; auto.
+Qed.
+
+Lemma swap_comparison_cmpfs_bool:
+  forall cmp ft v1 v2,
+  ftest_for_cmp cmp = Reversed ft ->
+  Val.cmpfs_bool cmp v1 v2 = Val.cmpfs_bool (swap_comparison cmp) v2 v1.
+Proof.
+  intros. unfold Val.cmpfs_bool. destruct v1; destruct v2; auto. rewrite Float32.cmp_swap. reflexivity.
+Qed.
+
+Lemma transl_compfs_correct:
+  forall cmp r1 r2 lbl k rs m tbb b,
+  exists rs',
+     exec_straight ge (transl_comp_float32 cmp r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
+  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
+  /\ ( Val.cmpfs_bool cmp rs#r1 rs#r2 = Some b ->
+       exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
+        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
+  .
+Proof.
+  intros. unfold transl_comp_float32. destruct (ftest_for_cmp cmp) eqn:FT.
+  * esplit. split.
+    - apply exec_straight_one; simpl; eauto.
+    - split.
+      + intros; Simpl.
+      + intros. remember (rs # RTMP <- (compare_single _ _ _)) as rs'.
+        simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+        { 
+          assert ((nextblock tbb rs') # RTMP = (compare_single ft (rs r1) (rs r2))).
+          { rewrite Heqrs'. auto. }
+          rewrite H0. rewrite <- H.
+          remember (Val.cmpfs_bool cmp rs#r1 rs#r2) as cmpbool.
+          destruct cmp; simpl;
+          unfold compare_single;
+          unfold Val.cmpfs; simpl in FT; inversion FT; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
+          destruct b0; simpl; auto.
+        }
+        rewrite H0. simpl; auto.
+  * esplit. split.
+    - apply exec_straight_one; simpl; eauto.
+    - split.
+      + intros; Simpl.
+      + intros. remember (rs # RTMP <- (compare_single _ _ _)) as rs'.
+        simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+        { 
+          assert ((nextblock tbb rs') # RTMP = (compare_single ft (rs r2) (rs r1))).
+          { rewrite Heqrs'. auto. }
+          rewrite H0. rewrite <- H.
+          remember (Val.cmpfs_bool cmp rs#r1 rs#r2) as cmpbool.
+          erewrite swap_comparison_cmpfs_bool in Heqcmpbool; eauto.
+          destruct cmp; simpl;
+          unfold compare_single;
+          unfold Val.cmpfs; simpl in FT; inversion FT; simpl in Heqcmpbool; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
+          destruct b0; simpl; auto.
+        }
+        rewrite H0. simpl; auto.
+Qed.
+
+Lemma swap_comparison_cmpfs_bool_notftest:
+  forall cmp ft v1 v2,
+  notftest_for_cmp cmp = Reversed ft ->
+  Val.cmpfs_bool cmp v1 v2 = Val.cmpfs_bool (swap_comparison cmp) v2 v1.
+Proof.
+  intros. unfold Val.cmpfs_bool. destruct v1; destruct v2; auto. rewrite Float32.cmp_swap. reflexivity.
+Qed.
+
+Lemma cmpfs_bool_ne_eq:
+  forall v1 v2,
+  Val.cmpfs_bool Cne v1 v2 = option_map negb (Val.cmpfs_bool Ceq v1 v2).
+Proof.
+  intros. unfold Val.cmpfs_bool. destruct v1; destruct v2; auto. rewrite Float32.cmp_ne_eq. simpl. reflexivity.
+Qed.
+
+Lemma cmpfs_bool_ne_eq_rev:
+  forall v1 v2,
+  Val.cmpfs_bool Ceq v1 v2 = option_map negb (Val.cmpfs_bool Cne v1 v2).
+Proof.
+  intros. unfold Val.cmpfs_bool. destruct v1; destruct v2; auto. rewrite Float32.cmp_ne_eq. simpl. rewrite negb_involutive. reflexivity.
+Qed.
+
+Lemma transl_compnotfs_correct:
+  forall cmp r1 r2 lbl k rs m tbb b,
+  exists rs',
+     exec_straight ge (transl_comp_notfloat32 cmp r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
+  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
+  /\   (option_map negb (Val.cmpfs_bool cmp rs#r1 rs#r2) = Some b ->
+       exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
+        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
+  .
+Proof.
+  intros. unfold transl_comp_notfloat32. destruct (notftest_for_cmp cmp) eqn:FT.
+  * esplit. split.
+    - apply exec_straight_one; simpl; eauto.
+    - split.
+      + intros; Simpl.
+      + intros. remember (rs # RTMP <- (compare_single _ _ _)) as rs'.
+        simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+        { 
+          assert ((nextblock tbb rs') # RTMP = (compare_single ft (rs r1) (rs r2))).
+          { rewrite Heqrs'. auto. }
+          rewrite H0. rewrite <- H.
+          remember (option_map negb (Val.cmpfs_bool cmp rs#r1 rs#r2)) as cmpbool.
+          destruct cmp; simpl;
+          unfold compare_single;
+          unfold Val.cmpfs; simpl in FT; inversion FT.
+          * rewrite cmpfs_bool_ne_eq; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+          * rewrite cmpfs_bool_ne_eq_rev. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+          * rewrite notbool_option_map_negb. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+          * rewrite notbool_option_map_negb. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+        }
+        rewrite H0. simpl; auto.
+  * esplit. split.
+    - apply exec_straight_one; simpl; eauto.
+    - split.
+      + intros; Simpl.
+      + intros. remember (rs # RTMP <- (compare_single _ _ _)) as rs'.
+        simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+        { 
+          assert ((nextblock tbb rs') # RTMP = (compare_single ft (rs r2) (rs r1))).
+          { rewrite Heqrs'. auto. }
+          rewrite H0. rewrite <- H.
+          remember (Val.cmpfs_bool cmp rs#r1 rs#r2) as cmpbool.
+          erewrite swap_comparison_cmpfs_bool_notftest in Heqcmpbool; eauto.
+          destruct cmp; simpl;
+          unfold compare_single;
+          unfold Val.cmpfs; simpl in FT; inversion FT; simpl in Heqcmpbool.
+          * rewrite notbool_option_map_negb. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+          * rewrite notbool_option_map_negb. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+        }
+        rewrite H0. simpl; auto.
+Qed.
+
+Lemma transl_complu_correct:
+  forall cmp r1 r2 lbl k rs m tbb b,
+  exists rs',
+     exec_straight ge (transl_compl cmp Unsigned r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
+  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
+  /\ ( Val_cmplu_bool cmp rs#r1 rs#r2 = Some b ->
+       exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
+        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
+  .
+Proof.
+  intros. esplit. split.
+- unfold transl_compl. apply exec_straight_one; simpl; eauto.
+- split.
+  + intros; Simpl.
+  + intros.
+    remember (rs # RTMP <- (compare_long (itest_for_cmp cmp Unsigned) rs # r1 rs # r2)) as rs'.
+    simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+    { 
+      assert ((nextblock tbb rs') # RTMP = (compare_long (itest_for_cmp cmp Unsigned) rs # r1 rs # r2)).
+      { rewrite Heqrs'. auto. }
+      rewrite H0. rewrite <- H.
+      remember (Val_cmplu_bool cmp rs#r1 rs#r2) as cmpbool.
+      destruct cmp; simpl;
+      unfold compare_long, Val_cmplu; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
+      destruct b0; simpl; auto.
+    }
+    rewrite H0. simpl; auto.
+Qed.
+
+Lemma transl_compilu_correct:
+  forall cmp r1 n lbl k rs m tbb b,
+  exists rs',
+     exec_straight ge (transl_compil cmp Unsigned r1 n lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
+  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
+  /\ ( Val_cmplu_bool cmp rs#r1 (Vlong n) = Some b ->
+       exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
+        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
+  .
+Proof.
+  intros. esplit. split.
+- unfold transl_compil. apply exec_straight_one; simpl; eauto.
+- split.
+  + intros; Simpl.
+  + intros.
+    remember (rs # RTMP <- (compare_long (itest_for_cmp cmp Unsigned) rs # r1 (Vlong n))) as rs'.
+    simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+    { 
+      assert ((nextblock tbb rs') # RTMP = (compare_long (itest_for_cmp cmp Unsigned) rs # r1 (Vlong n))).
+      { rewrite Heqrs'. auto. }
+      rewrite H0. rewrite <- H.
+      remember (Val_cmplu_bool cmp rs#r1 (Vlong n)) as cmpbool.
+      destruct cmp; simpl;
+      unfold compare_long, Val_cmplu; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
+      destruct b0; simpl; auto.
+    }
+    rewrite H0. simpl; auto.
+Qed.
+
+Lemma transl_opt_compuimm_correct:
+  forall n cmp r1 lbl k rs m b tbb c,
+  select_comp n cmp = Some c ->
+  exists rs', exists insn,
+     exec_straight_opt (transl_opt_compuimm n cmp r1 lbl k) rs m ((PControl insn) ::g k) rs' m
+  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
+  /\ ( Val_cmpu_bool cmp rs#r1 (Vint n) = Some b ->
+       exec_control ge fn (Some insn) (nextblock tbb rs') m = eval_branch fn lbl (nextblock tbb rs') m (Some b))
+  .
+Proof.
+  intros.
+(*   unfold transl_opt_compuimm. unfold select_comp in H. rewrite H; simpl. *)
+  remember c as c'.
+  destruct c'.
+  - (* c = Ceq *)
+    assert (Int.eq n Int.zero = true) as H'. 
+    { remember (Int.eq n Int.zero) as termz. destruct termz; auto.
+      generalize H. unfold select_comp; rewrite <- Heqtermz; simpl.
+      discriminate. }
+    assert (n = (Int.repr 0)) as H0. { 
+      destruct (Int.eq_dec n (Int.repr 0)) as [Ha|Ha]; auto. 
+      generalize (Int.eq_false _ _ Ha).  unfold Int.zero in H'.
+      rewrite H'. discriminate.
+    }
+    assert (Ceq = cmp). { 
+      remember cmp as c0'. destruct c0'; auto; generalize H; unfold select_comp;
+      rewrite H'; simpl; auto;
+      intros; contradict H; discriminate.
+    }
+    unfold transl_opt_compuimm. subst. rewrite H'.
+
+    exists rs, (Pcbu BTweqz r1 lbl).
+    split.
+    * constructor.
+    * split; auto. simpl. intros.
+      assert (rs r1 = (nextblock tbb rs) r1).
+        unfold nextblock, incrPC. Simpl. rewrite H1 in H0.
+      (*assert (Val.cmp_bool Ceq (rs r1) (Vint (Int.repr 0)) = Some b) as EVAL'S.
+      { rewrite <- H2. rewrite <- H0. rewrite <- H1. auto. }*)
+      auto;
+      unfold eval_branch. rewrite H0; auto.
+  - (* c = Cne *)
+    assert (Int.eq n Int.zero = true) as H'. 
+    { remember (Int.eq n Int.zero) as termz. destruct termz; auto.
+      generalize H. unfold select_comp; rewrite <- Heqtermz; simpl.
+      discriminate. }
+    assert (n = (Int.repr 0)) as H0. { 
+      destruct (Int.eq_dec n (Int.repr 0)) as [Ha|Ha]; auto. 
+      generalize (Int.eq_false _ _ Ha).  unfold Int.zero in H'.
+      rewrite H'. discriminate.
+    }
+    assert (Cne = cmp). { 
+      remember cmp as c0'. destruct c0'; auto; generalize H; unfold select_comp;
+      rewrite H'; simpl; auto;
+      intros; contradict H; discriminate.
+    }
+    unfold transl_opt_compuimm. subst. rewrite H'.
+
+    exists rs, (Pcbu BTwnez r1 lbl).
+    split.
+    * constructor.
+    * split; auto. simpl. intros.
+      assert (rs r1 = (nextblock tbb rs) r1).
+        unfold nextblock, incrPC. Simpl. rewrite H1 in H0.
+      auto;
+      unfold eval_branch. rewrite H0. auto.
+  - (* c = Clt *) contradict H; unfold select_comp; destruct (Int.eq n Int.zero);
+    destruct cmp; discriminate.
+  - (* c = Cle *) contradict H; unfold select_comp; destruct (Int.eq n Int.zero);
+    destruct cmp; discriminate.
+  - (* c = Cgt *) contradict H; unfold select_comp; destruct (Int.eq n Int.zero);
+    destruct cmp; discriminate.
+  - (* c = Cge *) contradict H; unfold select_comp; destruct (Int.eq n Int.zero);
+    destruct cmp; discriminate.
+Qed.
+
+Lemma transl_opt_compluimm_correct:
+  forall n cmp r1 lbl k rs m b tbb c,
+  select_compl n cmp = Some c ->
+  exists rs', exists insn,
+     exec_straight_opt (transl_opt_compluimm n cmp r1 lbl k) rs m ((PControl insn) ::g k) rs' m
+  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)
+  /\ ( Val_cmplu_bool cmp rs#r1 (Vlong n) = Some b ->
+       exec_control ge fn (Some insn) (nextblock tbb rs') m = eval_branch fn lbl (nextblock tbb rs') m (Some b))
+  .
+Proof.
+  intros.
+(*   unfold transl_opt_compluimm; rewrite H; simpl. *)
+  remember c as c'.
+  destruct c'.
+  - (* c = Ceq *)
+    assert (Int64.eq n Int64.zero = true) as H'. 
+    { remember (Int64.eq n Int64.zero) as termz. destruct termz; auto.
+      generalize H. unfold select_compl; rewrite <- Heqtermz; simpl.
+      discriminate. }
+    assert (n = (Int64.repr 0)) as H0. { 
+      destruct (Int64.eq_dec n (Int64.repr 0)) as [Ha|Ha]; auto. 
+      generalize (Int64.eq_false _ _ Ha).  unfold Int64.zero in H'.
+      rewrite H'. discriminate.
+    }
+    assert (Ceq = cmp). { 
+      remember cmp as c0'. destruct c0'; auto; generalize H; unfold select_compl;
+      rewrite H'; simpl; auto;
+      intros; contradict H; discriminate.
+    }
+    unfold transl_opt_compluimm; subst; rewrite H'.
+
+    exists rs, (Pcbu BTdeqz r1 lbl).
+    split.
+    * constructor.
+    * split; auto. simpl. intros.
+      assert (rs r1 = (nextblock tbb rs) r1).
+        unfold nextblock, incrPC. Simpl. rewrite H1 in H0.
+      auto;
+      unfold eval_branch. rewrite H0; auto.
+  - (* c = Cne *)
+    assert (Int64.eq n Int64.zero = true) as H'. 
+    { remember (Int64.eq n Int64.zero) as termz. destruct termz; auto.
+      generalize H. unfold select_compl; rewrite <- Heqtermz; simpl.
+      discriminate. }
+    assert (n = (Int64.repr 0)) as H0. { 
+      destruct (Int64.eq_dec n (Int64.repr 0)) as [Ha|Ha]; auto. 
+      generalize (Int64.eq_false _ _ Ha).  unfold Int64.zero in H'.
+      rewrite H'. discriminate.
+    }
+    assert (Cne = cmp). { 
+      remember cmp as c0'. destruct c0'; auto; generalize H; unfold select_compl;
+      rewrite H'; simpl; auto;
+      intros; contradict H; discriminate.
+    }
+    unfold transl_opt_compluimm; subst; rewrite H'.
+
+    exists rs, (Pcbu BTdnez r1 lbl).
+    split.
+    * constructor.
+    * split; auto. simpl. intros.
+      assert (rs r1 = (nextblock tbb rs) r1).
+        unfold nextblock, incrPC. Simpl. rewrite H1 in H0.
+      auto;
+      unfold eval_branch. rewrite H0; auto.
+  - (* c = Clt *) contradict H; unfold select_compl; destruct (Int64.eq n Int64.zero);
+    destruct cmp; discriminate.
+  - (* c = Cle *) contradict H; unfold select_compl; destruct (Int64.eq n Int64.zero);
+    destruct cmp; discriminate.
+  - (* c = Cgt *) contradict H; unfold select_compl; destruct (Int64.eq n Int64.zero);
+    destruct cmp; discriminate.
+  - (* c = Cge *) contradict H; unfold select_compl; destruct (Int64.eq n Int64.zero);
+    destruct cmp; discriminate.
+Qed.
+
+Local Hint Resolve Val_cmpu_bool_correct Val_cmplu_bool_correct: core.
+
+Lemma transl_cbranch_correct_1:
+  forall cond args lbl k c m ms b sp rs m' tbb,
+  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 c rs m' ((PControl insn) ::g k) rs' m'
+  /\ exec_control ge fn (Some insn) (nextblock tbb rs') m' = eval_branch fn lbl (nextblock tbb rs') m' (Some b)
+  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
+Proof.
+  intros until tbb; 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.
+(* Ccomp *)
+- exploit (transl_comp_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C).
+  exists rs', (Pcb BTwnez RTMP lbl).
+  split.
+  + constructor. eexact A.
+  + split; auto. apply C; auto.
+(* Ccompu *)
+- exploit (transl_compu_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C).
+  exists rs', (Pcb BTwnez RTMP lbl).
+  split.
+  + constructor. eexact A.
+  + split; auto. apply C; eauto.
+(* Ccompimm *)
+- remember (Int.eq n Int.zero) as eqz.
+  destruct eqz.
+  + assert (n = (Int.repr 0)). { 
+        destruct (Int.eq_dec n (Int.repr 0)) as [H|H]; auto. 
+        generalize (Int.eq_false _ _ H).  unfold Int.zero in Heqeqz.
+        rewrite <- Heqeqz. discriminate.
+    }
+    exists rs, (Pcb (btest_for_cmpswz c0) x lbl).
+    split. 
+    * constructor.
+    * split; auto.
+      assert (rs x = (nextblock tbb rs) x).
+        unfold nextblock, incrPC. Simpl. rewrite H0 in EVAL'. clear H0.
+      destruct c0; simpl; auto;
+      unfold eval_branch; rewrite <- H; rewrite EVAL'; auto.
+  + exploit (transl_compi_correct c0 x n lbl); eauto. intros (rs'2 & A' & B' & C').
+    exists rs'2, (Pcb BTwnez RTMP lbl).
+    split.
+    * constructor. eexact A'.
+    * split; auto.
+      { apply C'; auto. }
+(* Ccompuimm *)
+- remember (select_comp n c0) as selcomp.
+  destruct selcomp.
+  + exploit (transl_opt_compuimm_correct n c0 x lbl k). apply eq_sym. apply Heqselcomp.
+    intros (rs' & i & A & B & C).
+    exists rs', i.
+    split.
+    * apply A.
+    * split; auto. apply C. apply EVAL'.
+  + assert (transl_opt_compuimm n c0 x lbl k = transl_compi c0 Unsigned x n lbl k).
+    { unfold transl_opt_compuimm.
+      destruct (Int.eq n Int.zero) eqn:EQN.
+      all: unfold select_comp in Heqselcomp; rewrite EQN in Heqselcomp; destruct c0; simpl in *; auto.
+      all: discriminate. }
+    rewrite H. clear H.
+    exploit (transl_compui_correct c0 x n lbl); eauto. intros (rs'2 & A' & B' & C').
+    exists rs'2, (Pcb BTwnez RTMP lbl).
+    split.
+    * constructor. eexact A'.
+    * split; auto.
+      { apply C'; auto. }
+(* Ccompl *)
+- exploit (transl_compl_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C).
+  exists rs', (Pcb BTwnez RTMP lbl).
+  split.
+  + constructor. eexact A.
+  + split; auto. apply C; auto.
+(* Ccomplu *)
+- exploit (transl_complu_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C).
+  exists rs', (Pcb BTwnez RTMP lbl).
+  split.
+  + constructor. eexact A.
+  + split; auto. apply C; eauto.
+(* Ccomplimm *)
+- remember (Int64.eq n Int64.zero) as eqz.
+  destruct eqz.
+  + assert (n = (Int64.repr 0)). { 
+        destruct (Int64.eq_dec n (Int64.repr 0)) as [H|H]; auto. 
+        generalize (Int64.eq_false _ _ H).  unfold Int64.zero in Heqeqz.
+        rewrite <- Heqeqz. discriminate.
+    }
+    exists rs, (Pcb (btest_for_cmpsdz c0) x lbl).
+    split. 
+    * constructor.
+    * split; auto.
+      assert (rs x = (nextblock tbb rs) x).
+        unfold nextblock, incrPC. Simpl. rewrite H0 in EVAL'. clear H0.
+      destruct c0; simpl; auto;
+      unfold eval_branch; rewrite <- H; rewrite EVAL'; auto.
+  + exploit (transl_compil_correct c0 x n lbl); eauto. intros (rs'2 & A' & B' & C').
+    exists rs'2, (Pcb BTwnez RTMP lbl).
+    split.
+    * constructor. eexact A'.
+    * split; auto.
+      { apply C'; auto. }
+
+(* Ccompluimm *)
+- remember (select_compl n c0) as selcomp.
+  destruct selcomp.
+  + exploit (transl_opt_compluimm_correct n c0 x lbl k). apply eq_sym. apply Heqselcomp.
+    intros (rs' & i & A & B & C).
+    exists rs', i.
+    split.
+    * apply A.
+    * split; eauto. (*  apply C. apply EVAL'. *)
+  + assert (transl_opt_compluimm n c0 x lbl k = transl_compil c0 Unsigned x n lbl k).
+    { unfold transl_opt_compluimm.
+      destruct (Int64.eq n Int64.zero) eqn:EQN.
+      all: unfold select_compl in Heqselcomp; rewrite EQN in Heqselcomp; destruct c0; simpl in *; auto.
+      all: discriminate. }
+    rewrite H. clear H.
+    exploit (transl_compilu_correct c0 x n lbl); eauto. intros (rs'2 & A' & B' & C').
+    exists rs'2, (Pcb BTwnez RTMP lbl).
+    split.
+    * constructor. eexact A'.
+    * split; auto.
+      { apply C'; auto. eapply Val_cmplu_bool_correct; eauto. }
+
+(* Ccompf *)
+- exploit (transl_compf_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C).
+  exists rs', (Pcb BTwnez RTMP lbl).
+  split.
+  + constructor. eexact A.
+  + split; auto. apply C; auto.
+
+(* Cnotcompf *)
+- exploit (transl_compnotf_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C).
+  exists rs', (Pcb BTwnez RTMP lbl).
+  split.
+  + constructor. eexact A.
+  + split; auto. apply C; auto.
+
+(* Ccompfs *)
+- exploit (transl_compfs_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C).
+  exists rs', (Pcb BTwnez RTMP lbl).
+  split.
+  + constructor. eexact A.
+  + split; auto. apply C; auto.
+
+(* Cnotcompfs *)
+- exploit (transl_compnotfs_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C).
+  exists rs', (Pcb BTwnez RTMP lbl).
+  split.
+  + constructor. eexact A.
+  + split; auto. apply C; auto.
+Qed.
+
+Lemma transl_cbranch_correct_true:
+  forall cond args lbl k c m ms sp rs m' tbb,
+  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 c rs m' ((PControl insn) ::g k) rs' m'
+  /\ exec_control ge fn (Some insn) (nextblock tbb rs') m' = goto_label fn lbl (nextblock tbb rs') m'
+  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
+Proof.
+  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 tbb 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', exists insn,
+     exec_straight_opt c rs m' ((PControl insn) ::g k) rs' m'
+  /\ exec_control ge fn (Some insn) (nextblock tbb rs') m' = Next (nextblock tbb rs') m'
+  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
+Proof.
+  intros. exploit transl_cbranch_correct_1. all: eauto. simpl eval_branch. instantiate (1 := tbb).
+  intros (rs' & insn & A & B & C). rewrite regset_same_assign in B.
+  eexists; eexists. split; try split. all: eassumption.
+Qed.
+
+(** Translation of condition operators *)
+
+Lemma transl_cond_int32s_correct:
+  forall cmp rd r1 r2 k rs m,
+  exists rs',
+     exec_straight ge (basics_to_code (transl_cond_int32s cmp rd r1 r2 k)) rs m (basics_to_code 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. destruct cmp; simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+Qed.
+
+
+Lemma transl_cond_int32u_correct:
+  forall cmp rd r1 r2 k rs m,
+  exists rs',
+     exec_straight ge (basics_to_code (transl_cond_int32u cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m
+  /\ rs'#rd = Val_cmpu cmp rs#r1 rs#r2
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
+Proof.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+Qed.
+
+Lemma transl_cond_int64s_correct:
+  forall cmp rd r1 r2 k rs m,
+  exists rs',
+     exec_straight ge (basics_to_code (transl_cond_int64s cmp rd r1 r2 k)) rs m (basics_to_code 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. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+Qed.
+
+Lemma transl_cond_int64u_correct:
+  forall cmp rd r1 r2 k rs m,
+  exists rs',
+     exec_straight ge (basics_to_code (transl_cond_int64u cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m
+  /\ rs'#rd = Val_cmplu cmp rs#r1 rs#r2
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
+Proof.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+Qed.
+
+Lemma transl_condimm_int32s_correct:
+  forall cmp rd r1 n k rs m,
+  r1 <> RTMP ->
+  exists rs',
+     exec_straight ge (basics_to_code (transl_condimm_int32s cmp rd r1 n k)) rs m (basics_to_code k) rs' m
+  /\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> rs'#r = rs#r.
+Proof.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+Qed.
+
+Local Hint Resolve Val_cmpu_correct Val_cmplu_correct: core.
+
+Lemma transl_condimm_int32u_correct:
+  forall cmp rd r1 n k rs m,
+  r1 <> RTMP ->
+  exists rs',
+     exec_straight ge (basics_to_code (transl_condimm_int32u cmp rd r1 n k)) rs m (basics_to_code 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 <> RTMP -> rs'#r = rs#r.
+Proof.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+Qed.
+
+Lemma transl_condimm_int64s_correct:
+  forall cmp rd r1 n k rs m,
+  r1 <> RTMP ->
+  exists rs',
+     exec_straight ge (basics_to_code (transl_condimm_int64s cmp rd r1 n k)) rs m (basics_to_code k) rs' m
+  /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> rs'#r = rs#r.
+Proof.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+Qed.
+
+Lemma transl_condimm_int64u_correct:
+  forall cmp rd r1 n k rs m,
+  r1 <> RTMP ->
+  exists rs',
+     exec_straight ge (basics_to_code (transl_condimm_int64u cmp rd r1 n k)) rs m (basics_to_code 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 <> RTMP -> rs'#r = rs#r.
+Proof.
+  intros. destruct cmp; simpl;
+  (econstructor; split; 
+  [ apply exec_straight_one; [simpl; eauto] | 
+    split; intros; Simpl; unfold compare_long; eauto]).
+Qed.
+
+Lemma swap_comparison_cmpfs:
+  forall v1 v2 cmp,
+  Val.lessdef (Val.cmpfs cmp v1 v2) (Val.cmpfs (swap_comparison cmp) v2 v1).
+Proof.
+  intros. unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct v1; destruct v2; auto.
+  rewrite Float32.cmp_swap. auto.
+Qed.
+
+Lemma transl_cond_float32_correct:
+  forall cmp rd r1 r2 k rs m,
+  exists rs',
+     exec_straight ge (basics_to_code (transl_cond_float32 cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m
+  /\ Val.lessdef (Val.cmpfs cmp rs#r1 rs#r2) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
+Proof.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl. apply swap_comparison_cmpfs.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl. apply swap_comparison_cmpfs.
+- econstructor; split. apply exec_straight_one; [simpl;
+ eauto].
+  split; intros; Simpl.
+Qed.
+
+Lemma transl_cond_nofloat32_correct:
+  forall cmp rd r1 r2 k rs m,
+  exists rs',
+     exec_straight ge (basics_to_code (transl_cond_notfloat32 cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m
+  /\ Val.lessdef (Val.of_optbool (option_map negb (Val.cmpfs_bool cmp (rs r1) (rs r2)))) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
+Proof.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto.
+  rewrite Float32.cmp_ne_eq. auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto.
+  rewrite Float32.cmp_ne_eq. simpl. destruct (Float32.cmp Ceq f f0); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl.
+  destruct (Float32.cmp Clt f f0); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl.
+  cutrewrite (Cge = swap_comparison Cle); auto. rewrite Float32.cmp_swap.
+  destruct (Float32.cmp _ _ _); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl.
+  cutrewrite (Clt = swap_comparison Cgt); auto. rewrite Float32.cmp_swap.
+  destruct (Float32.cmp _ _ _); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl.
+  destruct (Float32.cmp _ _ _); auto.
+Qed.
+
+Lemma swap_comparison_cmpf:
+  forall v1 v2 cmp,
+  Val.lessdef (Val.cmpf cmp v1 v2) (Val.cmpf (swap_comparison cmp) v2 v1).
+Proof.
+  intros. unfold Val.cmpf. unfold Val.cmpf_bool. destruct v1; destruct v2; auto.
+  rewrite Float.cmp_swap. auto.
+Qed.
+
+Lemma transl_cond_float64_correct:
+  forall cmp rd r1 r2 k rs m,
+  exists rs',
+     exec_straight ge (basics_to_code (transl_cond_float64 cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m
+  /\ Val.lessdef (Val.cmpf cmp rs#r1 rs#r2) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
+Proof.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl. apply swap_comparison_cmpf.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl. apply swap_comparison_cmpf.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+Qed.
+
+Lemma transl_cond_nofloat64_correct:
+  forall cmp rd r1 r2 k rs m,
+  exists rs',
+     exec_straight ge (basics_to_code (transl_cond_notfloat64 cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m
+  /\ Val.lessdef (Val.of_optbool (option_map negb (Val.cmpf_bool cmp (rs r1) (rs r2)))) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
+Proof.
+  intros. destruct cmp; simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto.
+  rewrite Float.cmp_ne_eq. auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto.
+  rewrite Float.cmp_ne_eq. simpl. destruct (Float.cmp Ceq f f0); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl.
+  destruct (Float.cmp Clt f f0); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl.
+  cutrewrite (Cge = swap_comparison Cle); auto. rewrite Float.cmp_swap.
+  destruct (Float.cmp _ _ _); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl.
+  cutrewrite (Clt = swap_comparison Cgt); auto. rewrite Float.cmp_swap.
+  destruct (Float.cmp _ _ _); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto].
+  split; intros; Simpl.
+  unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl.
+  destruct (Float.cmp _ _ _); auto.
+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 (basics_to_code c) rs m (basics_to_code 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 <> RTMP -> rs'#r = rs#r.
+Proof.
+  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. simpl. intros (rs' & A & B & C). exists rs'; eauto.
++ (* cmpu *)
+  exploit transl_cond_int32u_correct; eauto. simpl. intros (rs' & A & B & C).
+  exists rs'; repeat split; eauto. rewrite B; eapply Val_cmpu_correct.
++ (* 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. simpl. intros (rs' & A & B & C).
+  exists rs'; repeat split; eauto. rewrite MKTOT; eauto.
++ (* cmplu *)
+  exploit transl_cond_int64u_correct; eauto. simpl. intros (rs' & A & B & C).
+  exists rs'; repeat split; eauto. rewrite B, MKTOT; eauto.
+  eapply Val_cmplu_correct.
++ (* cmplimm *)
+  exploit transl_condimm_int64s_correct; eauto. instantiate (1 := x); eauto with asmgen. simpl. 
+  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. simpl. 
+  intros (rs' & A & B & C).
+  exists rs'; repeat split; eauto. rewrite MKTOT; eauto.
++ (* cmpfloat *) 
+  exploit transl_cond_float64_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto.
++ (* cmpnosingle *)
+  exploit transl_cond_nofloat64_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto.
++ (* cmpsingle *) 
+  exploit transl_cond_float32_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto.
++ (* cmpnosingle *)
+  exploit transl_cond_nofloat32_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto.
+Qed.
+
+(* Translation of arithmetic operations *)
+
+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.
+
+Ltac TranslOpSimpl :=
+  econstructor; split;
+  [ apply exec_straight_one; reflexivity
+  | split; [ apply Val.lessdef_same; simpl; Simpl; fail | intros; simpl; Simpl; fail ] ].
+
+Lemma int_eq_comm:
+  forall (x y: int),
+  (Int.eq x y) = (Int.eq y x).
+Proof.
+  intros.
+  unfold Int.eq.
+  unfold zeq.
+  destruct (Z.eq_dec _ _); destruct (Z.eq_dec _ _); congruence.
+Qed.
+
+Lemma int64_eq_comm:
+  forall (x y: int64),
+  (Int64.eq x y) = (Int64.eq y x).
+Proof.
+  intros.
+  unfold Int64.eq.
+  unfold zeq.
+  destruct (Z.eq_dec _ _); destruct (Z.eq_dec _ _); congruence.
+Qed.
+
+Lemma select_same_lessdef:
+  forall ty c v,
+    Val.lessdef (Val.select c v v ty) v.
+Proof.
+  intros.
+  unfold Val.select.
+  destruct c; try econstructor.
+  replace (if b then v else v) with v by (destruct b ; trivial).
+  destruct v; destruct ty; simpl; econstructor.
+Qed.
+
+Lemma if_neg : forall X,
+    forall a,
+    forall b c : X,
+    (if (negb a) then b else c) = (if a then c else b).
+Proof.
+  destruct a; reflexivity.
+Qed.
+
+Lemma int_ltu_to_neq:
+  forall x,
+    Int.ltu Int.zero x = negb (Int.eq x Int.zero).
+Proof.
+  intros.
+  unfold Int.ltu, Int.eq.
+  change (Int.unsigned Int.zero) with 0.
+  pose proof (Int.unsigned_range x) as RANGE.
+  unfold zlt, zeq.
+  destruct (Z_lt_dec _ _); destruct (Z.eq_dec _ _); trivial; omega.
+Qed.
+
+Lemma int64_ltu_to_neq:
+  forall x,
+    Int64.ltu Int64.zero x = negb (Int64.eq x Int64.zero).
+Proof.
+  intros.
+  unfold Int64.ltu, Int64.eq.
+  change (Int64.unsigned Int64.zero) with 0.
+  pose proof (Int64.unsigned_range x) as RANGE.
+  unfold zlt, zeq.
+  destruct (Z_lt_dec _ _); destruct (Z.eq_dec _ _); trivial; omega.
+Qed.
+
+Ltac splitall := repeat match goal with |- _ /\ _ => split end.
+
+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 (basics_to_code c) rs m (basics_to_code 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.
+  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.
+- (* Omove *)
+  destruct (preg_of res), (preg_of m0); inv TR; TranslOpSimpl.
+- (* Oaddrsymbol *)
+  destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)).
++ set (rs1 := (rs#x <- (Genv.symbol_address ge id Ptrofs.zero))).
+  exploit (addptrofs_correct x x ofs (basics_to_code 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.
+- (* Oaddrstack *)
+  exploit addptrofs_correct. instantiate (1 := SP); auto with asmgen. intros (rs' & A & B & C).
+  exists rs'; split; eauto. auto with asmgen.
+- (* Ocast8signed *)
+  econstructor; split.
+  eapply exec_straight_two. simpl;eauto. simpl;eauto.
+  repeat split; intros; simpl; Simpl.
+  assert (A: Int.ltu (Int.repr 24) Int.iwordsize = true) by auto.
+  destruct (rs x0); auto; simpl. rewrite A; simpl. Simpl. unfold Val.shr. rewrite A.
+  apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity.
+- (* Ocast16signed *)
+  econstructor; split.
+  eapply exec_straight_two. simpl;eauto. simpl;eauto.
+  repeat split; intros; Simpl.
+  assert (A: Int.ltu (Int.repr 16) Int.iwordsize = true) by auto.
+  destruct (rs x0); auto; simpl. rewrite A; simpl. Simpl. unfold Val.shr. rewrite A. 
+  apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity.
+- (* Oshrximm *)
+  econstructor; split.
+  + apply exec_straight_one. simpl. eauto.
+  + repeat split.
+    * rewrite Pregmap.gss.
+      destruct (rs x0); simpl; trivial.
+      unfold Val.maketotal.
+      destruct (Int.ltu _ _); simpl; trivial.
+    * intros.
+      rewrite Pregmap.gso; trivial.
+- (* Oshrxlimm *)
+  econstructor; split.
+  + apply exec_straight_one. simpl. eauto.
+  + repeat split.
+    * rewrite Pregmap.gss.
+      destruct (rs x0); simpl; trivial.
+      unfold Val.maketotal.
+      destruct (Int.ltu _ _); simpl; trivial.
+    * intros.
+      rewrite Pregmap.gso; trivial.
+      
+- (* Ocmp *)
+  exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
+  exists rs'; repeat split; eauto with asmgen.
+  
+- (* Osel *)
+  unfold conditional_move in *.
+  destruct (ireg_eq _ _).
+  {
+    subst x. inv EQ2.
+    econstructor; split.
+    {
+      apply exec_straight_one.
+      simpl. reflexivity.
+    }
+    split.
+    { apply select_same_lessdef. } 
+    intros; trivial.
+  }
+
+  destruct c0; simpl in *.
+
+    all: destruct c.
+    all: simpl in *.
+    all: inv EQ2.
+    all: econstructor; splitall.
+    all: try apply exec_straight_one.
+    all: intros; simpl; trivial.
+    all: unfold Val.select, cmove, cmoveu; simpl.
+    all: destruct (rs x1); simpl; trivial.
+    all: try rewrite int_ltu_to_neq.
+    all: try rewrite int64_ltu_to_neq.
+    all: try change (Int64.eq Int64.zero Int64.zero) with true.
+    all: try destruct Archi.ptr64.
+    all: try rewrite Pregmap.gss.
+    all: repeat rewrite if_neg.
+    all: simpl.
+    all: try destruct (_ || _).
+    all: try apply Val.lessdef_normalize.
+    all: trivial. (* no more lessdef *)
+    all: apply Pregmap.gso; congruence.
+
+- (* Oselimm *)
+  unfold conditional_move_imm32 in *.
+  destruct c0; simpl in *.
+
+    all: destruct c.
+    all: simpl in *.
+    all: inv EQ0.
+    all: econstructor; splitall.
+    all: try apply exec_straight_one.
+    all: intros; simpl; trivial.
+    all: unfold Val.select, cmove, cmoveu; simpl.
+    all: destruct (rs x0); simpl; trivial.
+    all: try rewrite int_ltu_to_neq.
+    all: try rewrite int64_ltu_to_neq.
+    all: try change (Int64.eq Int64.zero Int64.zero) with true.
+    all: try destruct Archi.ptr64.
+    all: try rewrite Pregmap.gss.
+    all: repeat rewrite if_neg.
+    all: simpl.
+    all: try destruct (_ || _).
+    all: try apply Val.lessdef_normalize.
+    all: trivial. (* no more lessdef *)
+    all: apply Pregmap.gso; congruence.
+
+- (* Osellimm *)
+  unfold conditional_move_imm64 in *.
+  destruct c0; simpl in *.
+
+    all: destruct c.
+    all: simpl in *.
+    all: inv EQ0.
+    all: econstructor; splitall.
+    all: try apply exec_straight_one.
+    all: intros; simpl; trivial.
+    all: unfold Val.select, cmove, cmoveu; simpl.
+    all: destruct (rs x0); simpl; trivial.
+    all: try rewrite int_ltu_to_neq.
+    all: try rewrite int64_ltu_to_neq.
+    all: try change (Int64.eq Int64.zero Int64.zero) with true.
+    all: try destruct Archi.ptr64.
+    all: try rewrite Pregmap.gss.
+    all: repeat rewrite if_neg.
+    all: simpl.
+    all: try destruct (_ || _).
+    all: try apply Val.lessdef_normalize.
+    all: trivial. (* no more lessdef *)
+    all: apply Pregmap.gso; congruence.
+Qed.
+
+(** Memory accesses *)
+
+Lemma indexed_memory_access_correct:
+  forall mk_instr base ofs k rs m,
+  exists base' ofs' rs' ptr',
+     exec_straight_opt (indexed_memory_access mk_instr base ofs ::g k) rs m
+                       (mk_instr base' ofs' ::g k) rs' m
+  /\ eval_offset ofs' = OK ptr'
+  /\ Val.offset_ptr rs'#base' ptr' = Val.offset_ptr rs#base ofs
+  /\ forall r, r <> PC -> rs'#r = rs#r.
+Proof.
+  unfold indexed_memory_access; intros.
+  (* destruct Archi.ptr64 eqn:SF. *)
+  assert (Archi.ptr64 = true) as SF; auto.
+- generalize (make_immed64_sound (Ptrofs.to_int64 ofs)); intros EQ.
+  destruct (make_immed64 (Ptrofs.to_int64 ofs)).
++ econstructor; econstructor; econstructor; econstructor; split.
+  apply exec_straight_opt_refl. 
+  split; auto. simpl. subst imm. rewrite Ptrofs.of_int64_to_int64 by auto. auto.
+Qed.
+
+
+Lemma indexed_load_access_correct:
+  forall trap chunk (mk_instr: ireg -> offset -> basic) rd m,
+  (forall base ofs rs,
+     exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset trap 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 ->
+  exists rs',
+     exec_straight ge (indexed_memory_access mk_instr base ofs ::g k) rs m k rs' m
+  /\ rs'#rd = v
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
+Proof.
+  intros until m; intros EXEC; intros until v; intros LOAD.
+  exploit indexed_memory_access_correct; eauto.
+  intros (base' & ofs' & rs' & ptr' & A & PtrEq & B & C).
+  econstructor; split.
+  eapply exec_straight_opt_right. eexact A. apply exec_straight_one. rewrite EXEC.
+  unfold exec_load_offset. unfold parexec_load_offset. rewrite PtrEq. rewrite B, LOAD. eauto. Simpl. 
+  split; intros; Simpl. auto.
+Qed.
+
+Lemma indexed_store_access_correct:
+  forall chunk (mk_instr: ireg -> offset -> basic) r1 m,
+  (forall base ofs rs,
+     exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset 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' ->
+  exists rs',
+     exec_straight ge (indexed_memory_access mk_instr base ofs ::g k) rs m k rs' m'
+  /\ forall r, r <> PC -> rs'#r = rs#r.
+Proof.
+  intros until m; intros EXEC; intros until m'; intros STORE.
+  exploit indexed_memory_access_correct. (* instantiate (1 := base). eauto. *)
+  intros (base' & ofs' & rs' & ptr' & A & PtrEq & B & C).
+  econstructor; split.
+  eapply exec_straight_opt_right. eapply A. apply exec_straight_one. rewrite EXEC.
+  unfold exec_store_offset. unfold parexec_store_offset. rewrite PtrEq. rewrite B, C, STORE.
+    eauto.
+    discriminate.
+  auto.
+Qed.
+
+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 ->
+  exists rs',
+     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
+  /\ rs'#(preg_of dst) = v
+  /\ forall r, r <> PC -> r <> preg_of dst -> rs'#r = rs#r.
+Proof.
+  intros until v; intros TR LOAD. 
+  assert (A: exists mk_instr rd,
+                preg_of dst = IR rd
+             /\ c = indexed_memory_access mk_instr base ofs :: k
+             /\ forall base' ofs' rs',
+                   exec_basic_instr ge (mk_instr base' ofs') rs' m =
+                   exec_load_offset TRAP (chunk_of_type ty) rs' m rd base' ofs').
+  { unfold loadind in TR.
+    destruct ty, (preg_of dst); inv TR; econstructor; esplit; eauto. }
+  destruct A as (mk_instr & rd & rdEq & B & C). subst c. rewrite rdEq.
+  eapply indexed_load_access_correct; eauto with asmgen. 
+Qed.
+
+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' ->
+  exists rs',
+     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m'
+  /\ forall r, r <> PC -> rs'#r = rs#r.
+Proof.
+  intros until m'; intros TR STORE.
+  assert (A: exists mk_instr rr,
+                preg_of src = IR rr
+             /\ c = indexed_memory_access mk_instr base ofs :: k
+             /\ forall base' ofs' rs',
+                   exec_basic_instr ge (mk_instr base' ofs') rs' m =
+                   exec_store_offset (chunk_of_type ty) rs' m rr base' ofs').
+  { unfold storeind in TR. destruct ty, (preg_of src); inv TR; econstructor; esplit; eauto. }
+  destruct A as (mk_instr & rr & rsEq & B & C). subst c.
+  eapply indexed_store_access_correct; eauto with asmgen.
+  congruence.
+Qed.
+
+Ltac bsimpl := unfold exec_bblock; simpl.
+
+Lemma Pget_correct:
+  forall (dst: gpreg) (src: preg) k (rs: regset) m,
+  src = RA ->
+  exists rs',
+     exec_straight ge (Pget dst src ::g k) rs m k rs' m
+  /\ rs'#dst = rs#src
+  /\ forall r, r <> PC -> r <> dst -> rs'#r = rs#r.
+Proof.
+  intros. econstructor; econstructor; econstructor.
+- rewrite H. bsimpl. auto.
+- Simpl.
+- intros. Simpl.
+Qed.
+
+Lemma Pset_correct:
+  forall (dst: preg) (src: gpreg) k (rs: regset) m,
+  dst = RA ->
+  exists rs',
+     exec_straight ge (Pset dst src ::g k) rs m k rs' m
+  /\ rs'#dst = rs#src
+  /\ forall r, r <> PC -> r <> dst -> rs'#r = rs#r.
+Proof.
+  intros. econstructor; econstructor; econstructor; simpl.
+  rewrite H. auto.
+  Simpl.
+  Simpl.
+  intros. rewrite H. Simpl.
+Qed.
+
+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 ->
+  exists rs',
+     exec_straight ge (loadind_ptr base ofs dst ::g k) rs m k rs' m
+  /\ rs'#dst = v
+  /\ forall r, r <> PC -> r <> dst -> rs'#r = rs#r.
+Proof.
+  intros. eapply indexed_load_access_correct; eauto with asmgen.
+  intros. unfold Mptr. assert (Archi.ptr64 = true). auto. rewrite H0.
+  instantiate (1 := TRAP).
+  auto.
+Qed.
+
+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' ->
+  exists rs',
+     exec_straight ge (storeind_ptr src base ofs ::g k) rs m k rs' m'
+  /\ forall r, r <> PC -> rs'#r = rs#r.
+Proof.
+  intros. eapply indexed_store_access_correct with (r1 := src); eauto with asmgen.
+  intros. unfold Mptr. assert (Archi.ptr64 = true); auto.
+Qed.
+
+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' ptr,
+     exec_straight_opt (basics_to_code c) rs m (mk_instr base ofs ::g (basics_to_code k)) rs' m
+  /\ eval_offset ofs = OK ptr
+  /\ Val.offset_ptr rs'#base ptr = v
+  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
+Proof.
+  intros until v; intros TR EV. 
+  unfold transl_memory_access in TR; destruct addr; ArgsInv.
+- (* indexed *)
+  inv EV. exploit indexed_memory_access_correct; eauto. intros (base' & ofs' & rs' & ptr' & EOPT & EVALOFF & VALOFF & RSEQ).
+  eexists; eexists; eexists; eexists. split; try split; try split.
+  eapply EOPT. unfold eval_offset in EVALOFF. inv EVALOFF. eauto.
+  { intros. destruct r; rewrite RSEQ; auto. }
+- (* global *)
+  simpl in EV. inv EV. inv TR.  econstructor; econstructor; econstructor; econstructor; split.
+  constructor. apply exec_straight_one. simpl; eauto. auto. 
+  split; split; intros; Simpl.
+  assert (Val.lessdef (Val.offset_ptr (Genv.symbol_address ge i i0) Ptrofs.zero) (Genv.symbol_address ge i i0)).
+  { apply Val.offset_ptr_zero. }
+  remember (Genv.symbol_address ge i i0) as symbol.
+  destruct symbol; auto.
+  + contradict Heqsymbol; unfold Genv.symbol_address.
+    destruct (Genv.find_symbol ge i); discriminate.
+  + contradict Heqsymbol; unfold Genv.symbol_address;
+    destruct (Genv.find_symbol ge i); discriminate.
+  + contradict Heqsymbol; unfold Genv.symbol_address;
+    destruct (Genv.find_symbol ge i); discriminate.
+  + contradict Heqsymbol; unfold Genv.symbol_address;
+    destruct (Genv.find_symbol ge i); discriminate.
+  + simpl. rewrite Ptrofs.add_zero; auto.
+- (* stack *)
+  inv TR. inv EV. 
+  exploit indexed_memory_access_correct; eauto. intros (base' & ofs' & rs' & ptr' & EOPT & EVALOFF & VALOFF & RSEQ).
+  eexists; eexists; eexists; eexists. split; try split; try split.
+  eapply EOPT. unfold eval_offset in EVALOFF. inv EVALOFF. eauto.
+  { intros. destruct r; rewrite RSEQ; auto. }
+Qed.
+
+Lemma transl_memory_access2_correct:
+  forall mk_instr addr args k c (rs: regset) m v,
+  transl_memory_access2 mk_instr addr args k = OK c ->
+  eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
+  exists base ro mro mr1 rs',
+     args = mr1 :: mro :: nil
+  /\ ireg_of mro = OK ro
+  /\ exec_straight_opt (basics_to_code c) rs m (mk_instr base ro ::g (basics_to_code k)) rs' m
+  /\ Val.addl rs'#base rs'#ro = v
+  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
+Proof.
+  intros until v; intros TR EV. 
+  unfold transl_memory_access2 in TR; destruct addr; ArgsInv.
+  inv EV. repeat eexists. eassumption. econstructor; eauto.
+Qed.
+
+Lemma transl_memory_access2XS_correct:
+  forall chunk mk_instr (scale : Z) args k c (rs: regset) m v,
+  transl_memory_access2XS chunk mk_instr scale args k = OK c ->
+  eval_addressing ge rs#SP (Aindexed2XS scale) (map rs (map preg_of args)) = Some v ->
+  exists base ro mro mr1 rs',
+     args = mr1 :: mro :: nil
+  /\ ireg_of mro = OK ro
+  /\ exec_straight_opt (basics_to_code c) rs m (mk_instr base ro ::g (basics_to_code k)) rs' m
+  /\ Val.addl rs'#base (Val.shll rs'#ro (Vint (Int.repr scale))) = v
+  /\ (forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r)
+  /\ scale = (zscale_of_chunk chunk).
+Proof.
+  intros until v; intros TR EV. 
+  unfold transl_memory_access2XS in TR; ArgsInv.
+  inv EV. repeat eexists. eassumption. econstructor; eauto.
+  symmetry.
+  apply Z.eqb_eq.
+  assumption.
+Qed.
+
+Lemma transl_load_access2_correct:
+  forall trap chunk (mk_instr: ireg -> ireg -> basic) addr args k c rd (rs: regset) m v mro mr1 ro v',
+  args = mr1 :: mro :: nil ->
+  ireg_of mro = OK ro ->
+  (forall base rs,
+     exec_basic_instr ge (mk_instr base ro) rs m = exec_load_reg trap chunk rs m rd base ro) ->
+  transl_memory_access2 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' ->
+  exists rs',
+     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
+  /\ rs'#rd = v'
+  /\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r.
+Proof.
+  intros until v'; intros ARGS IREGE INSTR TR EV LOAD. 
+  exploit transl_memory_access2_correct; eauto.
+  intros (base & ro2 & mro2 & mr2 & rs' & ARGSS & IREGEQ & A & B & C). rewrite ARGSS in ARGS. inversion ARGS. subst mr2 mro2. clear ARGS.
+  econstructor; split.
+  eapply exec_straight_opt_right. eexact A. apply exec_straight_one. assert (ro = ro2) by congruence. subst ro2.
+  rewrite INSTR. unfold exec_load_reg. unfold parexec_load_reg. rewrite B, LOAD. reflexivity. Simpl. 
+  split; intros; Simpl. auto.
+Qed.
+
+Lemma transl_load_access2_correct_notrap2:
+  forall chunk (mk_instr: ireg -> ireg -> basic) addr args k c rd (rs: regset) m v mro mr1 ro,
+  args = mr1 :: mro :: nil ->
+  ireg_of mro = OK ro ->
+  (forall base rs,
+     exec_basic_instr ge (mk_instr base ro) rs m = exec_load_reg NOTRAP chunk rs m rd base ro) ->
+  transl_memory_access2 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 = None ->
+  exists rs',
+     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
+  /\ rs'#rd = concrete_default_notrap_load_value chunk
+  /\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r.
+Proof.
+  intros until ro; intros ARGS IREGE INSTR TR EV LOAD. 
+  exploit transl_memory_access2_correct; eauto.
+  intros (base & ro2 & mro2 & mr2 & rs' & ARGSS & IREGEQ & A & B & C). rewrite ARGSS in ARGS. inversion ARGS. subst mr2 mro2. clear ARGS.
+  econstructor; split.
+  eapply exec_straight_opt_right. eexact A. apply exec_straight_one. assert (ro = ro2) by congruence. subst ro2.
+  rewrite INSTR. unfold exec_load_reg. unfold parexec_load_reg. rewrite B, LOAD. reflexivity. Simpl. 
+  split; intros; Simpl. auto.
+Qed.
+
+Lemma transl_load_access2XS_correct:
+  forall trap chunk (mk_instr: ireg -> ireg -> basic) (scale : Z) args k c rd (rs: regset) m v mro mr1 ro v',
+  args = mr1 :: mro :: nil ->
+  ireg_of mro = OK ro ->
+  (forall base rs,
+     exec_basic_instr ge (mk_instr base ro) rs m = exec_load_regxs trap chunk rs m rd base ro) ->
+  transl_memory_access2XS chunk mk_instr scale args k = OK c ->
+  eval_addressing ge rs#SP (Aindexed2XS scale) (map rs (map preg_of args)) = Some v ->
+  Mem.loadv chunk m v = Some v' ->
+  exists rs',
+     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
+  /\ rs'#rd = v'
+  /\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r.
+Proof.
+  intros until v'; intros ARGS IREGE INSTR TR EV LOAD. 
+  exploit transl_memory_access2XS_correct; eauto.
+  intros (base & ro2 & mro2 & mr2 & rs' & ARGSS & IREGEQ & A & B & C & D). rewrite ARGSS in ARGS. inversion ARGS. subst mr2 mro2. clear ARGS.
+  econstructor; split.
+  eapply exec_straight_opt_right. eexact A. apply exec_straight_one. assert (ro = ro2) by congruence. subst ro2.
+  rewrite INSTR. unfold exec_load_regxs. unfold parexec_load_regxs.
+  unfold scale_of_chunk.
+  subst scale.
+  rewrite B, LOAD. reflexivity. Simpl. 
+  split. trivial. intros. Simpl.
+Qed.
+
+Lemma transl_load_access2XS_correct_notrap2:
+  forall chunk (mk_instr: ireg -> ireg -> basic) (scale : Z) args k c rd (rs: regset) m v mro mr1 ro,
+  args = mr1 :: mro :: nil ->
+  ireg_of mro = OK ro ->
+  (forall base rs,
+     exec_basic_instr ge (mk_instr base ro) rs m = exec_load_regxs NOTRAP chunk rs m rd base ro) ->
+  transl_memory_access2XS chunk mk_instr scale args k = OK c ->
+  eval_addressing ge rs#SP (Aindexed2XS scale) (map rs (map preg_of args)) = Some v ->
+  Mem.loadv chunk m v = None ->
+  exists rs',
+     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
+  /\ rs'#rd = concrete_default_notrap_load_value chunk
+  /\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r.
+Proof.
+  intros until ro; intros ARGS IREGE INSTR TR EV LOAD. 
+  exploit transl_memory_access2XS_correct; eauto.
+  intros (base & ro2 & mro2 & mr2 & rs' & ARGSS & IREGEQ & A & B & C & D). rewrite ARGSS in ARGS. inversion ARGS. subst mr2 mro2. clear ARGS.
+  econstructor; split.
+  eapply exec_straight_opt_right. eexact A. apply exec_straight_one. assert (ro = ro2) by congruence. subst ro2.
+  rewrite INSTR. unfold exec_load_regxs. unfold parexec_load_regxs.
+  unfold scale_of_chunk.
+  subst scale.
+  rewrite B, LOAD. reflexivity. Simpl. 
+  split. trivial. intros. Simpl.
+Qed.
+
+Lemma transl_load_access_correct:
+  forall trap chunk (mk_instr: ireg -> offset -> basic) addr args k c rd (rs: regset) m v v',
+  (forall base ofs rs,
+     exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset trap 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' ->
+  exists rs',
+     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
+  /\ rs'#rd = v'
+  /\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r.
+Proof.
+  intros until v'; intros INSTR TR EV LOAD. 
+  exploit transl_memory_access_correct; eauto.
+  intros (base & ofs & rs' & ptr & A & PtrEq & B & C).
+  econstructor; split.
+  eapply exec_straight_opt_right. eexact A. apply exec_straight_one. 
+  rewrite INSTR. unfold exec_load_offset. unfold parexec_load_offset. rewrite PtrEq, B, LOAD. reflexivity. Simpl. 
+  split; intros; Simpl. auto.
+Qed.
+
+Lemma transl_load_access_correct_notrap2:
+  forall chunk (mk_instr: ireg -> offset -> basic) addr args k c rd (rs: regset) m v,
+  (forall base ofs rs,
+     exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset NOTRAP 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 = None ->
+  exists rs',
+     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
+  /\ rs'#rd = concrete_default_notrap_load_value chunk
+  /\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r.
+Proof.
+  intros until v; intros INSTR TR EV LOAD. 
+  exploit transl_memory_access_correct; eauto.
+  intros (base & ofs & rs' & ptr & A & PtrEq & B & C).
+  econstructor; split.
+  eapply exec_straight_opt_right. eexact A. apply exec_straight_one. 
+  rewrite INSTR. unfold exec_load_offset. unfold parexec_load_offset. rewrite PtrEq, B, LOAD. reflexivity. Simpl. 
+  split. trivial. intros. Simpl.
+Qed.
+
+Lemma transl_load_memory_access_ok:
+  forall addr trap chunk args dst k c rs a v m,
+  (match addr with Aindexed2XS _ | Aindexed2 => False | _ => True end) ->
+  transl_load trap chunk addr args dst k = OK c ->
+  eval_addressing ge (rs (IR SP)) addr (map rs (map preg_of args)) = Some a ->
+  Mem.loadv chunk m a = Some v ->
+  exists mk_instr rd,
+     preg_of dst = IR rd
+  /\ transl_memory_access mk_instr addr args k = OK c
+  /\ forall base ofs rs,
+        exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset trap chunk rs m rd base ofs.
+Proof.
+  intros until m. intros ADDR TR ? ?.
+  unfold transl_load in TR. destruct addr; try contradiction.
+  - monadInv TR. destruct chunk; ArgsInv; econstructor; (esplit; eauto).
+  - monadInv TR. destruct chunk. all: ArgsInv; destruct args; try discriminate; monadInv EQ0; eexists; eexists; split; try split;
+    [ instantiate (1 := (PLoadRRO _ _ x)); simpl; reflexivity
+    | eauto ].
+  - monadInv TR. destruct chunk. all: ArgsInv; destruct args; try discriminate; monadInv EQ0; eexists; eexists; split; try split;
+    [ instantiate (1 := (PLoadRRO _ _ x)); simpl; reflexivity
+    | eauto ].
+Qed.
+
+Lemma transl_load_memory_access_ok_notrap2:
+  forall addr chunk args dst k c rs a m,
+  (match addr with Aindexed2XS _ | Aindexed2 => False | _ => True end) ->
+  transl_load NOTRAP chunk addr args dst k = OK c ->
+  eval_addressing ge (rs (IR SP)) addr (map rs (map preg_of args)) = Some a ->
+  Mem.loadv chunk m a = None ->
+  exists mk_instr rd,
+     preg_of dst = IR rd
+  /\ transl_memory_access mk_instr addr args k = OK c
+  /\ forall base ofs rs,
+        exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset NOTRAP chunk rs m rd base ofs.
+Proof.
+  intros until m. intros ADDR TR ? ?.
+  unfold transl_load in TR. destruct addr; try contradiction.
+  - monadInv TR. destruct chunk; ArgsInv; econstructor; (esplit; eauto).
+  - monadInv TR. destruct chunk. all: ArgsInv; destruct args; try discriminate; monadInv EQ0; eexists; eexists; split; try split;
+    [ instantiate (1 := (PLoadRRO _ _ x)); simpl; reflexivity
+    | eauto ].
+  - monadInv TR. destruct chunk. all: ArgsInv; destruct args; try discriminate; monadInv EQ0; eexists; eexists; split; try split;
+    [ instantiate (1 := (PLoadRRO _ _ x)); simpl; reflexivity
+    | eauto ].
+Qed.
+
+Lemma transl_load_memory_access2_ok:
+  forall trap chunk args dst k c rs a v m,
+  transl_load trap chunk Aindexed2 args dst k = OK c ->
+  eval_addressing ge (rs (IR SP)) Aindexed2 (map rs (map preg_of args)) = Some a ->
+  Mem.loadv chunk m a = Some v ->
+  exists mk_instr mr0 mro rd ro,
+      args = mr0 :: mro :: nil
+   /\ preg_of dst = IR rd
+   /\ preg_of mro = IR ro
+   /\ transl_memory_access2 mk_instr Aindexed2 args k = OK c
+   /\ forall base rs,
+      exec_basic_instr ge (mk_instr base ro) rs m = exec_load_reg trap chunk rs m rd base ro.
+Proof.
+  intros until m. intros TR ? ?.
+  unfold transl_load in TR. subst. monadInv TR. destruct chunk. all:
+  unfold transl_memory_access2 in EQ0; repeat (destruct args; try discriminate); monadInv EQ0; ArgsInv; repeat eexists;
+  [ unfold ireg_of in EQ0; destruct (preg_of m1); eauto; try discriminate; monadInv EQ0; reflexivity
+  | rewrite EQ1; rewrite EQ0; simpl; instantiate (1 := (PLoadRRR _ _ x)); simpl; reflexivity
+  | eauto].
+Qed.
+
+
+Lemma transl_load_memory_access2_ok_notrap2:
+  forall chunk args dst k c rs a m,
+  transl_load NOTRAP chunk Aindexed2 args dst k = OK c ->
+  eval_addressing ge (rs (IR SP)) Aindexed2 (map rs (map preg_of args)) = Some a ->
+  Mem.loadv chunk m a = None ->
+  exists mk_instr mr0 mro rd ro,
+      args = mr0 :: mro :: nil
+   /\ preg_of dst = IR rd
+   /\ preg_of mro = IR ro
+   /\ transl_memory_access2 mk_instr Aindexed2 args k = OK c
+   /\ forall base rs,
+      exec_basic_instr ge (mk_instr base ro) rs m = exec_load_reg NOTRAP chunk rs m rd base ro.
+Proof.
+  intros until m. intros TR ? ?.
+  unfold transl_load in TR. subst. monadInv TR. destruct chunk. all:
+  unfold transl_memory_access2 in EQ0; repeat (destruct args; try discriminate); monadInv EQ0; ArgsInv; repeat eexists;
+  [ unfold ireg_of in EQ0; destruct (preg_of m1); eauto; try discriminate; monadInv EQ0; reflexivity
+  | rewrite EQ1; rewrite EQ0; simpl; instantiate (1 := (PLoadRRR _ _ x)); simpl; reflexivity
+  | eauto].
+Qed.
+
+Lemma transl_load_memory_access2XS_ok:
+  forall scale trap chunk args dst k c rs a v m,
+  transl_load trap chunk (Aindexed2XS scale) args dst k = OK c ->
+  eval_addressing ge (rs (IR SP)) (Aindexed2XS scale) (map rs (map preg_of args)) = Some a ->
+  Mem.loadv chunk m a = Some v ->
+  exists mk_instr mr0 mro rd ro,
+      args = mr0 :: mro :: nil
+   /\ preg_of dst = IR rd
+   /\ preg_of mro = IR ro
+   /\ transl_memory_access2XS chunk mk_instr scale args k = OK c
+   /\ forall base rs,
+      exec_basic_instr ge (mk_instr base ro) rs m = exec_load_regxs trap chunk rs m rd base ro.
+Proof.
+  intros until m. intros TR ? ?.
+  unfold transl_load in TR. subst. monadInv TR. destruct chunk. all:
+  unfold transl_memory_access2XS in EQ0; repeat (destruct args; try discriminate); monadInv EQ0; ArgsInv; repeat eexists;
+  [ unfold ireg_of in EQ0; destruct (preg_of m1); eauto; try discriminate; monadInv EQ0; reflexivity
+  | rewrite EQ1; rewrite EQ0; simpl; instantiate (1 := (PLoadRRRXS _ _ x)); simpl; rewrite Heqb; eauto
+  | eauto].
+Qed.
+
+
+Lemma transl_load_memory_access2XS_ok_notrap2:
+  forall scale chunk args dst k c rs a m,
+  transl_load NOTRAP chunk (Aindexed2XS scale) args dst k = OK c ->
+  eval_addressing ge (rs (IR SP)) (Aindexed2XS scale) (map rs (map preg_of args)) = Some a ->
+  Mem.loadv chunk m a = None ->
+  exists mk_instr mr0 mro rd ro,
+      args = mr0 :: mro :: nil
+   /\ preg_of dst = IR rd
+   /\ preg_of mro = IR ro
+   /\ transl_memory_access2XS chunk mk_instr scale args k = OK c
+   /\ forall base rs,
+      exec_basic_instr ge (mk_instr base ro) rs m = exec_load_regxs NOTRAP chunk rs m rd base ro.
+Proof.
+  intros until m. intros TR ? ?.
+  unfold transl_load in TR. subst. monadInv TR. destruct chunk. all:
+  unfold transl_memory_access2XS in EQ0; repeat (destruct args; try discriminate); monadInv EQ0; ArgsInv; repeat eexists;
+  [ unfold ireg_of in EQ0; destruct (preg_of m1); eauto; try discriminate; monadInv EQ0; reflexivity
+  | rewrite EQ1; rewrite EQ0; simpl; instantiate (1 := (PLoadRRRXS _ _ x)); simpl; rewrite Heqb; eauto
+  | eauto].
+Qed.
+
+Lemma transl_load_correct:
+  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 (basics_to_code c) rs m (basics_to_code k) rs' m
+  /\ rs'#(preg_of dst) = v
+  /\ forall r, r <> PC -> r <> RTMP -> r <> preg_of dst -> rs'#r = rs#r.
+Proof.
+  intros until v; intros TR EV LOAD. destruct addr.
+  - exploit transl_load_memory_access2XS_ok; eauto. intros (mk_instr & mr0 & mro & rd & ro & argsEq & rdEq & roEq & B & C).
+    rewrite rdEq. eapply transl_load_access2XS_correct; eauto with asmgen. unfold ireg_of. rewrite roEq. reflexivity.
+  - exploit transl_load_memory_access2_ok; eauto. intros (mk_instr & mr0 & mro & rd & ro & argsEq & rdEq & roEq & B & C).
+    rewrite rdEq. eapply transl_load_access2_correct; eauto with asmgen. unfold ireg_of. rewrite roEq. reflexivity.
+  - exploit transl_load_memory_access_ok; eauto; try discriminate; try (simpl; reflexivity).
+    intros A; destruct A as (mk_instr & rd & rdEq & B & C); rewrite rdEq;
+      eapply transl_load_access_correct; eauto with asmgen.
+  - exploit transl_load_memory_access_ok; eauto; try discriminate; try (simpl; reflexivity).
+    intros A; destruct A as (mk_instr & rd & rdEq & B & C); rewrite rdEq;
+      eapply transl_load_access_correct; eauto with asmgen.
+  - exploit transl_load_memory_access_ok; eauto; try discriminate; try (simpl; reflexivity).
+    intros A; destruct A as (mk_instr & rd & rdEq & B & C); rewrite rdEq;
+      eapply transl_load_access_correct; eauto with asmgen.
+Qed.
+
+Lemma transl_load_correct_notrap2:
+  forall chunk addr args dst k c (rs: regset) m a,
+  transl_load NOTRAP 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 = None ->
+  exists rs',
+     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
+  /\ rs'#(preg_of dst) = (concrete_default_notrap_load_value chunk)
+  /\ forall r, r <> PC -> r <> RTMP -> r <> preg_of dst -> rs'#r = rs#r.
+Proof.
+  intros until a; intros TR EV LOAD. destruct addr.
+  - exploit transl_load_memory_access2XS_ok_notrap2; eauto. intros (mk_instr & mr0 & mro & rd & ro & argsEq & rdEq & roEq & B & C).
+    rewrite rdEq. eapply transl_load_access2XS_correct_notrap2; eauto with asmgen. unfold ireg_of. rewrite roEq. reflexivity.
+  - exploit transl_load_memory_access2_ok_notrap2; eauto. intros (mk_instr & mr0 & mro & rd & ro & argsEq & rdEq & roEq & B & C).
+    rewrite rdEq. eapply transl_load_access2_correct_notrap2; eauto with asmgen. unfold ireg_of. rewrite roEq. reflexivity.
+  - exploit transl_load_memory_access_ok_notrap2; eauto; try discriminate; try (simpl; reflexivity).
+    intros A; destruct A as (mk_instr & rd & rdEq & B & C); rewrite rdEq;
+      eapply transl_load_access_correct_notrap2; eauto with asmgen.
+  - exploit transl_load_memory_access_ok_notrap2; eauto; try discriminate; try (simpl; reflexivity).
+    intros A; destruct A as (mk_instr & rd & rdEq & B & C); rewrite rdEq;
+      eapply transl_load_access_correct_notrap2; eauto with asmgen.
+  - exploit transl_load_memory_access_ok_notrap2; eauto; try discriminate; try (simpl; reflexivity).
+    intros A; destruct A as (mk_instr & rd & rdEq & B & C); rewrite rdEq;
+      eapply transl_load_access_correct_notrap2; eauto with asmgen.
+Qed.
+
+Lemma transl_store_access2_correct:
+  forall chunk (mk_instr: ireg -> ireg -> basic) addr args k c r1 (rs: regset) m v mr1 mro ro m',
+  args = mr1 :: mro :: nil ->
+  ireg_of mro = OK ro ->
+  (forall base rs,
+     exec_basic_instr ge (mk_instr base ro) rs m = exec_store_reg chunk rs m r1 base ro) ->
+  transl_memory_access2 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 <> RTMP ->
+  exists rs',
+     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m'
+  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
+Proof.
+  intros until m'; intros ARGS IREG INSTR TR EV STORE NOT31. 
+  exploit transl_memory_access2_correct; eauto.
+  intros (base & ro2 & mr2 & mro2 & rs' & ARGSS & IREGG & A & B & C). rewrite ARGSS in ARGS. inversion ARGS. subst mro2 mr2. clear ARGS.
+  econstructor; split.
+  eapply exec_straight_opt_right. eexact A. apply exec_straight_one. assert (ro = ro2) by congruence. subst ro2.
+  rewrite INSTR. unfold exec_store_reg. unfold parexec_store_reg. rewrite B. rewrite C; try discriminate. rewrite STORE. auto.
+  intro. inv H. contradiction.
+  auto.
+Qed.
+
+Lemma transl_store_access2XS_correct:
+  forall chunk (mk_instr: ireg -> ireg -> basic) scale args k c r1 (rs: regset) m v mr1 mro ro m',
+  args = mr1 :: mro :: nil ->
+  ireg_of mro = OK ro ->
+  (forall base rs,
+     exec_basic_instr ge (mk_instr base ro) rs m = exec_store_regxs chunk rs m r1 base ro) ->
+  transl_memory_access2XS chunk mk_instr scale args k = OK c ->
+  eval_addressing ge rs#SP (Aindexed2XS scale) (map rs (map preg_of args)) = Some v ->
+  Mem.storev chunk m v rs#r1 = Some m' ->
+  r1 <> RTMP ->
+  exists rs',
+     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m'
+  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
+Proof.
+  intros until m'; intros ARGS IREG INSTR TR EV STORE NOT31. 
+  exploit transl_memory_access2XS_correct; eauto.
+  intros (base & ro2 & mr2 & mro2 & rs' & ARGSS & IREGG & A & B & C & D). rewrite ARGSS in ARGS. inversion ARGS. subst mro2 mr2. clear ARGS.
+  econstructor; split.
+  eapply exec_straight_opt_right. eexact A. apply exec_straight_one. assert (ro = ro2) by congruence. subst ro2.
+  rewrite INSTR. unfold exec_store_regxs. unfold parexec_store_regxs.
+  unfold scale_of_chunk.
+  subst scale.
+  rewrite B. rewrite C; try discriminate. rewrite STORE. auto.
+  intro. inv H. contradiction.
+  auto.
+Qed.
+
+Lemma transl_store_access_correct:
+  forall chunk (mk_instr: ireg -> offset -> basic) addr args k c r1 (rs: regset) m v m',
+  (forall base ofs rs,
+     exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset 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 <> RTMP ->
+  exists rs',
+     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m'
+  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
+Proof.
+  intros until m'; intros INSTR TR EV STORE NOT31. 
+  exploit transl_memory_access_correct; eauto.
+  intros (base & ofs & rs' & ptr & A & PtrEq & B & C).
+  econstructor; split.
+  eapply exec_straight_opt_right. eexact A. apply exec_straight_one. 
+  rewrite INSTR. unfold exec_store_offset. unfold parexec_store_offset. rewrite PtrEq, B. rewrite C; try discriminate. rewrite STORE. auto.
+  intro. inv H. contradiction.
+  auto.
+Qed.
+
+
+Remark exec_store_offset_8_sign rs m x base ofs:
+  exec_store_offset Mint8unsigned rs m x base ofs = exec_store_offset Mint8signed rs m x base ofs.
+Proof.
+  unfold exec_store_offset. unfold parexec_store_offset. unfold eval_offset; auto. unfold Mem.storev.
+  destruct (Val.offset_ptr _ _); auto. erewrite <- Mem.store_signed_unsigned_8. reflexivity.
+Qed.
+
+Remark exec_store_offset_16_sign rs m x base ofs:
+  exec_store_offset Mint16unsigned rs m x base ofs = exec_store_offset Mint16signed rs m x base ofs.
+Proof.
+  unfold exec_store_offset. unfold parexec_store_offset. unfold eval_offset; auto. unfold Mem.storev.
+  destruct (Val.offset_ptr _ _); auto. erewrite <- Mem.store_signed_unsigned_16. reflexivity.
+Qed.
+
+Lemma transl_store_memory_access_ok:
+  forall addr chunk args src k c rs a m m',
+  (match addr with Aindexed2XS _ | Aindexed2 => False | _ => True end) ->
+  transl_store chunk addr args src k = OK c ->
+  eval_addressing ge (rs (IR SP)) addr (map rs (map preg_of args)) = Some a ->
+  Mem.storev chunk m a (rs (preg_of src)) = Some m' ->
+  exists mk_instr chunk' rr,
+     preg_of src = IR rr
+  /\ transl_memory_access mk_instr addr args k = OK c
+  /\ (forall base ofs rs,
+       exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset chunk' rs m rr base ofs)
+  /\ Mem.storev chunk m a rs#(preg_of src) = Mem.storev chunk' m a rs#(preg_of src).
+Proof.
+  intros until m'. intros ? TR ? ?.
+  unfold transl_store in TR. destruct addr; try contradiction.
+  - monadInv TR. destruct chunk. all:
+    ArgsInv; eexists; eexists; eexists; split; try split; [
+      repeat (destruct args; try discriminate); eassumption
+    | split; eauto; intros; simpl; try reflexivity].
+    eapply exec_store_offset_8_sign.
+    eapply exec_store_offset_16_sign.
+  - monadInv TR. destruct chunk. all:
+    ArgsInv; eexists; eexists; eexists; split; try split;
+    [ repeat (destruct args; try discriminate); instantiate (1 := PStoreRRO _ x); simpl; eassumption
+    | split; eauto; intros; simpl; try reflexivity].
+    eapply exec_store_offset_8_sign.
+    eapply exec_store_offset_16_sign.
+  - monadInv TR. destruct chunk. all:
+    ArgsInv; eexists; eexists; eexists; split; try split;
+    [ repeat (destruct args; try discriminate); instantiate (1 := PStoreRRO _ x); simpl; eassumption
+    | split; eauto; intros; simpl; try reflexivity].
+    eapply exec_store_offset_8_sign.
+    eapply exec_store_offset_16_sign.
+Qed.
+
+Remark exec_store_reg_8_sign rs m x base ofs:
+  exec_store_reg Mint8unsigned rs m x base ofs = exec_store_reg Mint8signed rs m x base ofs.
+Proof.
+  unfold exec_store_reg. unfold parexec_store_reg. unfold Mem.storev. destruct (Val.addl _ _); auto.
+  erewrite <- Mem.store_signed_unsigned_8. reflexivity.
+Qed.
+
+Remark exec_store_reg_16_sign rs m x base ofs:
+  exec_store_reg Mint16unsigned rs m x base ofs = exec_store_reg Mint16signed rs m x base ofs.
+Proof.
+  unfold exec_store_reg. unfold parexec_store_reg. unfold Mem.storev. destruct (Val.addl _ _); auto.
+  erewrite <- Mem.store_signed_unsigned_16. reflexivity.
+Qed.
+
+Remark exec_store_regxs_8_sign rs m x base ofs:
+  exec_store_regxs Mint8unsigned rs m x base ofs = exec_store_regxs Mint8signed rs m x base ofs.
+Proof.
+  unfold exec_store_regxs. unfold parexec_store_regxs. unfold Mem.storev. destruct (Val.addl _ _); auto.
+  erewrite <- Mem.store_signed_unsigned_8. reflexivity.
+Qed.
+
+Remark exec_store_regxs_16_sign rs m x base ofs:
+  exec_store_regxs Mint16unsigned rs m x base ofs = exec_store_regxs Mint16signed rs m x base ofs.
+Proof.
+  unfold exec_store_regxs. unfold parexec_store_regxs. unfold Mem.storev. destruct (Val.addl _ _); auto.
+  erewrite <- Mem.store_signed_unsigned_16. reflexivity.
+Qed.
+
+Lemma transl_store_memory_access2_ok:
+  forall addr chunk args src k c rs a m m',
+  addr = Aindexed2 ->
+  transl_store chunk addr args src k = OK c ->
+  eval_addressing ge (rs (IR SP)) addr (map rs (map preg_of args)) = Some a ->
+  Mem.storev chunk m a (rs (preg_of src)) = Some m' ->
+  exists mk_instr chunk' rr mr0 mro ro,
+     args = mr0 :: mro :: nil
+  /\ preg_of mro = IR ro
+  /\ preg_of src = IR rr
+  /\ transl_memory_access2 mk_instr addr args k = OK c
+  /\ (forall base rs,
+       exec_basic_instr ge (mk_instr base ro) rs m = exec_store_reg chunk' rs m rr base ro)
+  /\ Mem.storev chunk m a rs#(preg_of src) = Mem.storev chunk' m a rs#(preg_of src).
+Proof.
+  intros until m'. intros ? TR ? ?.
+  unfold transl_store in TR. subst addr. monadInv TR. destruct chunk. all:
+  unfold transl_memory_access2 in EQ0; repeat (destruct args; try discriminate); monadInv EQ0; ArgsInv; repeat eexists;
+  [ ArgsInv; reflexivity
+  | rewrite EQ1; rewrite EQ0; instantiate (1 := (PStoreRRR _ x)); simpl; reflexivity
+  | eauto ].
+  - simpl. intros. eapply exec_store_reg_8_sign.
+  - simpl. intros. eapply exec_store_reg_16_sign.
+Qed.
+
+Lemma transl_store_memory_access2XS_ok:
+  forall scale chunk args src k c rs a m m',
+  transl_store chunk (Aindexed2XS scale) args src k = OK c ->
+  eval_addressing ge (rs (IR SP)) (Aindexed2XS scale) (map rs (map preg_of args)) = Some a ->
+  Mem.storev chunk m a (rs (preg_of src)) = Some m' ->
+  exists mk_instr chunk' rr mr0 mro ro,
+     args = mr0 :: mro :: nil
+  /\ preg_of mro = IR ro
+  /\ preg_of src = IR rr
+  /\ transl_memory_access2XS chunk' mk_instr scale args k = OK c
+  /\ (forall base rs,
+       exec_basic_instr ge (mk_instr base ro) rs m = exec_store_regxs chunk' rs m rr base ro)
+  /\ Mem.storev chunk m a rs#(preg_of src) = Mem.storev chunk' m a rs#(preg_of src).
+Proof.
+  intros until m'. intros TR ? ?.
+  unfold transl_store in TR. monadInv TR. destruct chunk. all:
+  unfold transl_memory_access2XS in EQ0; repeat (destruct args; try discriminate); monadInv EQ0; ArgsInv; repeat eexists;
+  [ ArgsInv; reflexivity
+  | rewrite EQ1; rewrite EQ0; instantiate (1 := (PStoreRRRXS _ x)); simpl; rewrite Heqb; eauto
+  | eauto ].
+  - simpl. intros. eapply exec_store_regxs_8_sign.
+  - simpl. intros. eapply exec_store_regxs_16_sign.
+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#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 (basics_to_code c) rs m (basics_to_code k) rs' m'
+  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
+Proof.
+  intros until m'; intros TR EV STORE. destruct addr.
+  - exploit transl_store_memory_access2XS_ok; eauto. intros (mk_instr & chunk' & rr & mr0 & mro & ro & argsEq & roEq & srcEq & A & B & C).
+    eapply transl_store_access2XS_correct; eauto with asmgen. unfold ireg_of. rewrite roEq. reflexivity. congruence.
+    destruct rr; try discriminate. destruct src; simpl in srcEq; try discriminate.
+  - exploit transl_store_memory_access2_ok; eauto. intros (mk_instr & chunk' & rr & mr0 & mro & ro & argsEq & roEq & srcEq & A & B & C).
+    eapply transl_store_access2_correct; eauto with asmgen. unfold ireg_of. rewrite roEq. reflexivity. congruence.
+    destruct rr; try discriminate. destruct src; simpl in srcEq; try discriminate.
+  - exploit transl_store_memory_access_ok; eauto; try discriminate; try (simpl; reflexivity).
+    intro A;
+    destruct A as (mk_instr & chunk' & rr & rrEq & B & C & D);
+    rewrite D in STORE; clear D; 
+    eapply transl_store_access_correct; eauto with asmgen; try congruence;
+    destruct rr; try discriminate; destruct src; try discriminate.
+  - exploit transl_store_memory_access_ok; eauto; try discriminate; try (simpl; reflexivity).
+    intro A;
+    destruct A as (mk_instr & chunk' & rr & rrEq & B & C & D);
+    rewrite D in STORE; clear D; 
+    eapply transl_store_access_correct; eauto with asmgen; try congruence;
+    destruct rr; try discriminate; destruct src; try discriminate.
+  - exploit transl_store_memory_access_ok; eauto; try discriminate; try (simpl; reflexivity).
+    intro A;
+    destruct A as (mk_instr & chunk' & rr & rrEq & B & C & D);
+    rewrite D in STORE; clear D; 
+    eapply transl_store_access_correct; eauto with asmgen; try congruence;
+    destruct rr; try discriminate; destruct src; try discriminate.
+Qed.
+
+Lemma make_epilogue_correct:
+  forall ge0 f m stk soff cs m' ms rs k tm,
+  Mach.load_stack m (Vptr stk soff) Tptr f.(fn_link_ofs) = Some (parent_sp cs) ->
+  Mach.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 (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 <> RTMP -> r <> GPRA -> 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) GPRA (Pset RA GPRA ::g Pfreeframe (fn_stacksize f) (fn_link_ofs f) ::g k))
+            rs tm).
+  - rewrite <- (sp_val _ _ rs AG). simpl. eexact LRA'.
+  - intros (rs1 & A1 & B1 & C1).
+    assert (agree ms (Vptr stk soff) rs1) as AG1.
+    + destruct AG.
+      apply mkagree; auto.
+      rewrite C1; discriminate || auto.
+      intro. rewrite C1; auto; destruct r; simpl; try discriminate.
+    + exploit (Pset_correct RA GPRA (Pfreeframe (fn_stacksize f) (fn_link_ofs f) ::g k) rs1 tm). auto.
+      intros (rs2 & A2 & B2 & C2).
+      econstructor; econstructor; split.
+      * eapply exec_straight_trans.
+        { eexact A1. }
+        { eapply exec_straight_trans.
+          { eapply A2. }
+          { apply exec_straight_one. simpl.
+            rewrite (C2 SP) by auto with asmgen. rewrite <- (sp_val _ _ rs1 AG1). simpl; rewrite LP'.
+            rewrite FREE'. eauto. } }
+      * split. apply agree_set_other; auto with asmgen. 
+    apply agree_change_sp with (Vptr stk soff).
+    apply agree_exten with rs; auto. intros; rewrite C2; auto with asmgen.
+    eapply parent_sp_def; eauto.
+  split. auto.
+  split. Simpl. rewrite B2. auto.
+  split. Simpl. 
+  intros. Simpl.
+  rewrite C2; auto.
+Qed.
+
+End CONSTRUCTORS.
+
+