From 91a07b5ef9935780942a53108ac80ef354a76248 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Sat, 19 Dec 2020 18:40:04 +0100
Subject: Cleanup

---
 aarch64/Asmblockgenproof1.v | 1740 +++++++++++++++++++++----------------------
 1 file changed, 870 insertions(+), 870 deletions(-)

(limited to 'aarch64/Asmblockgenproof1.v')

diff --git a/aarch64/Asmblockgenproof1.v b/aarch64/Asmblockgenproof1.v
index dd7803cd..e26c24e7 100644
--- a/aarch64/Asmblockgenproof1.v
+++ b/aarch64/Asmblockgenproof1.v
@@ -137,10 +137,10 @@ Lemma decompose_int_wf:
 Proof.
 Local Opaque Zzero_ext.
   induction N as [ | N]; simpl; intros.
-- constructor.
-- set (frag := Zzero_ext 16 (Z.shiftr n p)) in *. destruct (Z.eqb frag 0).
-+ apply IHN. omega.
-+ econstructor. reflexivity. omega. apply IHN; omega. 
+  - constructor.
+  - set (frag := Zzero_ext 16 (Z.shiftr n p)) in *. destruct (Z.eqb frag 0).
+    + apply IHN. omega.
+    + econstructor. reflexivity. omega. apply IHN; omega. 
 Qed.
 
 Fixpoint recompose_int (accu: Z) (l: list (Z * Z)) : Z :=
@@ -158,35 +158,35 @@ Lemma decompose_int_correct:
    if zlt i p then Z.testbit accu i else Z.testbit n i).
 Proof.
   induction N as [ | N]; intros until accu; intros PPOS ABOVE i RANGE.
-- simpl. rewrite zlt_true; auto. xomega.
-- rewrite inj_S in RANGE. simpl.
-  set (frag := Zzero_ext 16 (Z.shiftr n p)).
-  assert (FRAG: forall i, p <= i < p + 16 -> Z.testbit n i = Z.testbit frag (i - p)).
-  { unfold frag; intros. rewrite Zzero_ext_spec by omega. rewrite zlt_true by omega.
-    rewrite Z.shiftr_spec by omega. f_equal; omega. }
-  destruct (Z.eqb_spec frag 0).
-+ rewrite IHN.
-* destruct (zlt i p). rewrite zlt_true by omega. auto.
-  destruct (zlt i (p + 16)); auto.
-  rewrite ABOVE by omega. rewrite FRAG by omega. rewrite e, Z.testbit_0_l. auto.
-* omega.
-* intros; apply ABOVE; omega.
-* xomega.
-+ simpl. rewrite IHN.
-* destruct (zlt i (p + 16)).
-** rewrite Zinsert_spec by omega. unfold proj_sumbool.
-   rewrite zlt_true by omega.
-   destruct (zlt i p).
-   rewrite zle_false by omega. auto.
-   rewrite zle_true by omega. simpl. symmetry; apply FRAG; omega.
-** rewrite Z.ldiff_spec, Z.shiftl_spec by omega.
-   change 65535 with (two_p 16 - 1). rewrite Ztestbit_two_p_m1 by omega.
-   rewrite zlt_false by omega. rewrite zlt_false by omega. apply andb_true_r. 
-* omega.
-* intros. rewrite Zinsert_spec by omega. unfold proj_sumbool.
-  rewrite zle_true by omega. rewrite zlt_false by omega. simpl.
-  apply ABOVE. omega.
-* xomega.
+  - simpl. rewrite zlt_true; auto. xomega.
+  - rewrite inj_S in RANGE. simpl.
+    set (frag := Zzero_ext 16 (Z.shiftr n p)).
+    assert (FRAG: forall i, p <= i < p + 16 -> Z.testbit n i = Z.testbit frag (i - p)).
+    { unfold frag; intros. rewrite Zzero_ext_spec by omega. rewrite zlt_true by omega.
+      rewrite Z.shiftr_spec by omega. f_equal; omega. }
+    destruct (Z.eqb_spec frag 0).
+    + rewrite IHN.
+      * destruct (zlt i p). rewrite zlt_true by omega. auto.
+        destruct (zlt i (p + 16)); auto.
+        rewrite ABOVE by omega. rewrite FRAG by omega. rewrite e, Z.testbit_0_l. auto.
+      * omega.
+      * intros; apply ABOVE; omega.
+      * xomega.
+    + simpl. rewrite IHN.
+      * destruct (zlt i (p + 16)).
+        ** rewrite Zinsert_spec by omega. unfold proj_sumbool.
+           rewrite zlt_true by omega.
+           destruct (zlt i p).
+           rewrite zle_false by omega. auto.
+           rewrite zle_true by omega. simpl. symmetry; apply FRAG; omega.
+        ** rewrite Z.ldiff_spec, Z.shiftl_spec by omega.
+           change 65535 with (two_p 16 - 1). rewrite Ztestbit_two_p_m1 by omega.
+           rewrite zlt_false by omega. rewrite zlt_false by omega. apply andb_true_r. 
+      * omega.
+      * intros. rewrite Zinsert_spec by omega. unfold proj_sumbool.
+        rewrite zle_true by omega. rewrite zlt_false by omega. simpl.
+        apply ABOVE. omega.
+      * xomega.
 Qed.
 
 Corollary decompose_int_eqmod: forall N n,
@@ -238,10 +238,10 @@ Proof.
   intros. apply equal_same_bits; intros.
   rewrite Zinsert_spec by omega. unfold proj_sumbool.
   destruct (zlt i p); [rewrite zle_false by omega|rewrite zle_true by omega]; simpl.
-- rewrite Z.testbit_0_l, Z.shiftl_spec_low by auto. auto.
-- rewrite Z.shiftl_spec by omega. 
-  destruct (zlt i (p + l)); auto.
-  rewrite Zzero_ext_spec, zlt_false, Z.testbit_0_l by omega. auto.
+  - rewrite Z.testbit_0_l, Z.shiftl_spec_low by auto. auto.
+  - rewrite Z.shiftl_spec by omega. 
+    destruct (zlt i (p + l)); auto.
+    rewrite Zzero_ext_spec, zlt_false, Z.testbit_0_l by omega. auto.
 Qed.
 
 Lemma recompose_int_negated:
@@ -249,15 +249,15 @@ Lemma recompose_int_negated:
   forall accu, recompose_int (Z.lnot accu) (negate_decomposition l) = Z.lnot (recompose_int accu l).
 Proof.
   induction 1; intros accu; simpl.
-- auto.
-- rewrite <- IHwf_decomposition. f_equal. apply equal_same_bits; intros. 
-  rewrite Z.lnot_spec, ! Zinsert_spec, Z.lxor_spec, Z.lnot_spec by omega.
-  unfold proj_sumbool.
-  destruct (zle p i); simpl; auto.
-  destruct (zlt i (p + 16)); simpl; auto.
-  change 65535 with (two_p 16 - 1).
-  rewrite Ztestbit_two_p_m1 by omega. rewrite zlt_true by omega.
-  apply xorb_true_r. 
+  - auto.
+  - rewrite <- IHwf_decomposition. f_equal. apply equal_same_bits; intros. 
+    rewrite Z.lnot_spec, ! Zinsert_spec, Z.lxor_spec, Z.lnot_spec by omega.
+    unfold proj_sumbool.
+    destruct (zle p i); simpl; auto.
+    destruct (zlt i (p + 16)); simpl; auto.
+    change 65535 with (two_p 16 - 1).
+    rewrite Ztestbit_two_p_m1 by omega. rewrite zlt_true by omega.
+    apply xorb_true_r. 
 Qed.
 
 Lemma exec_loadimm_k_w:
@@ -271,16 +271,16 @@ Lemma exec_loadimm_k_w:
   /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
 Proof.
   induction 1; intros rs accu ACCU; simpl.
-- exists rs; split. apply exec_straight_opt_refl. auto.
-- destruct (IHwf_decomposition
-                ((rs#rd <- (insert_in_int rs#rd n p 16)))
-                (Zinsert accu n p 16))
-  as (rs' & P & Q & R).
-  Simpl. rewrite ACCU. simpl. f_equal. apply Int.eqm_samerepr. 
-  apply Zinsert_eqmod. auto. omega. apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
-  exists rs'; split.
-  eapply exec_straight_opt_step_opt. simpl. eauto. auto.
-  split. exact Q. intros; Simpl. rewrite R by auto. Simpl.
+  - exists rs; split. apply exec_straight_opt_refl. auto.
+  - destruct (IHwf_decomposition
+                  ((rs#rd <- (insert_in_int rs#rd n p 16)))
+                  (Zinsert accu n p 16))
+    as (rs' & P & Q & R).
+    Simpl. rewrite ACCU. simpl. f_equal. apply Int.eqm_samerepr. 
+    apply Zinsert_eqmod. auto. omega. apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
+    exists rs'; split.
+    eapply exec_straight_opt_step_opt. simpl. eauto. auto.
+    split. exact Q. intros; Simpl. rewrite R by auto. Simpl.
 Qed.
 
 Lemma exec_loadimm_z_w:
@@ -292,19 +292,19 @@ Lemma exec_loadimm_z_w:
   /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
 Proof.
   unfold loadimm_z; destruct 1.
-- econstructor; split.
-  apply exec_straight_one. simpl; eauto. auto.
-  split. Simpl.
-  intros; Simpl.
-- set (accu0 := Zinsert 0 n p 16).
-  set (rs1 := rs#rd <- (Vint (Int.repr accu0))).
-  destruct (exec_loadimm_k_w rd k m l H1 rs1 accu0) as (rs2 & P & Q & R); auto.
-  unfold rs1; Simpl.
-  exists rs2; split.
-  eapply exec_straight_opt_step; eauto.
-  simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; omega.
-  split. exact Q. 
-  intros. rewrite R by auto. unfold rs1; Simpl.
+  - econstructor; split.
+    apply exec_straight_one. simpl; eauto. auto.
+    split. Simpl.
+    intros; Simpl.
+  - set (accu0 := Zinsert 0 n p 16).
+    set (rs1 := rs#rd <- (Vint (Int.repr accu0))).
+    destruct (exec_loadimm_k_w rd k m l H1 rs1 accu0) as (rs2 & P & Q & R); auto.
+    unfold rs1; Simpl.
+    exists rs2; split.
+    eapply exec_straight_opt_step; eauto.
+    simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; omega.
+    split. exact Q. 
+    intros. rewrite R by auto. unfold rs1; Simpl.
 Qed.
 
 Lemma exec_loadimm_n_w:
@@ -316,22 +316,22 @@ Lemma exec_loadimm_n_w:
   /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
 Proof.
   unfold loadimm_n; destruct 1.
-- econstructor; split.
-  apply exec_straight_one. simpl; eauto. auto.
-  split. Simpl. 
-  intros; Simpl.
-- set (accu0 := Z.lnot (Zinsert 0 n p 16)).
-  set (rs1 := rs#rd <- (Vint (Int.repr accu0))).
-  destruct (exec_loadimm_k_w rd k m (negate_decomposition l) 
-                                    (negate_decomposition_wf l H1)
-                                    rs1 accu0) as (rs2 & P & Q & R).
-  unfold rs1; Simpl.
-  exists rs2; split.
-  eapply exec_straight_opt_step; eauto.
-  simpl. unfold rs1. do 5 f_equal.
-  unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; omega.
-  split. unfold accu0 in Q; rewrite recompose_int_negated in Q by auto. exact Q.
-  intros. rewrite R by auto. unfold rs1; Simpl.
+  - econstructor; split.
+    apply exec_straight_one. simpl; eauto. auto.
+    split. Simpl. 
+    intros; Simpl.
+  - set (accu0 := Z.lnot (Zinsert 0 n p 16)).
+    set (rs1 := rs#rd <- (Vint (Int.repr accu0))).
+    destruct (exec_loadimm_k_w rd k m (negate_decomposition l) 
+                                      (negate_decomposition_wf l H1)
+                                      rs1 accu0) as (rs2 & P & Q & R).
+    unfold rs1; Simpl.
+    exists rs2; split.
+    eapply exec_straight_opt_step; eauto.
+    simpl. unfold rs1. do 5 f_equal.
+    unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; omega.
+    split. unfold accu0 in Q; rewrite recompose_int_negated in Q by auto. exact Q.
+    intros. rewrite R by auto. unfold rs1; Simpl.
 Qed.
 
 Lemma exec_loadimm32:
@@ -343,23 +343,23 @@ Lemma exec_loadimm32:
 Proof.
   unfold loadimm32, loadimm; intros.
   destruct (is_logical_imm32 n).
-- econstructor; split.
-  apply exec_straight_one. simpl; eauto. auto.
-  split. Simpl. rewrite Int.repr_unsigned, Int.or_zero_l; auto.
-  intros; Simpl.
-- set (dz := decompose_int 2%nat (Int.unsigned n) 0).
-  set (dn := decompose_int 2%nat (Z.lnot (Int.unsigned n)) 0).
-  assert (A: Int.repr (recompose_int 0 dz) = n).
-  { transitivity (Int.repr (Int.unsigned n)).
-    apply Int.eqm_samerepr. apply decompose_int_eqmod. 
-    apply Int.repr_unsigned. }
-  assert (B: Int.repr (Z.lnot (recompose_int 0 dn)) = n).
-  { transitivity (Int.repr (Int.unsigned n)).
-    apply Int.eqm_samerepr. apply decompose_notint_eqmod. 
-    apply Int.repr_unsigned. }
-  destruct Nat.leb.
-+ rewrite <- A. apply exec_loadimm_z_w. apply decompose_int_wf; omega.
-+ rewrite <- B. apply exec_loadimm_n_w. apply decompose_int_wf; omega.
+  - econstructor; split.
+    apply exec_straight_one. simpl; eauto. auto.
+    split. Simpl. rewrite Int.repr_unsigned, Int.or_zero_l; auto.
+    intros; Simpl.
+  - set (dz := decompose_int 2%nat (Int.unsigned n) 0).
+    set (dn := decompose_int 2%nat (Z.lnot (Int.unsigned n)) 0).
+    assert (A: Int.repr (recompose_int 0 dz) = n).
+    { transitivity (Int.repr (Int.unsigned n)).
+      apply Int.eqm_samerepr. apply decompose_int_eqmod. 
+      apply Int.repr_unsigned. }
+    assert (B: Int.repr (Z.lnot (recompose_int 0 dn)) = n).
+    { transitivity (Int.repr (Int.unsigned n)).
+      apply Int.eqm_samerepr. apply decompose_notint_eqmod. 
+      apply Int.repr_unsigned. }
+    destruct Nat.leb.
+    + rewrite <- A. apply exec_loadimm_z_w. apply decompose_int_wf; omega.
+    + rewrite <- B. apply exec_loadimm_n_w. apply decompose_int_wf; omega.
 Qed.
 
 Lemma exec_loadimm_k_x:
@@ -373,16 +373,16 @@ Lemma exec_loadimm_k_x:
   /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
 Proof.
   induction 1; intros rs accu ACCU; simpl.
-- exists rs; split. apply exec_straight_opt_refl. auto.
-- destruct (IHwf_decomposition
-                (rs#rd <- (insert_in_long rs#rd n p 16))
-                (Zinsert accu n p 16))
-  as (rs' & P & Q & R).
-  Simpl. rewrite ACCU. simpl. f_equal. apply Int64.eqm_samerepr. 
-  apply Zinsert_eqmod. auto. omega. apply Int64.eqm_sym; apply Int64.eqm_unsigned_repr.
-  exists rs'; split.
-  eapply exec_straight_opt_step_opt. simpl; eauto. auto.
-  split. exact Q. intros; Simpl. rewrite R by auto. Simpl.
+  - exists rs; split. apply exec_straight_opt_refl. auto.
+  - destruct (IHwf_decomposition
+                  (rs#rd <- (insert_in_long rs#rd n p 16))
+                  (Zinsert accu n p 16))
+    as (rs' & P & Q & R).
+    Simpl. rewrite ACCU. simpl. f_equal. apply Int64.eqm_samerepr. 
+    apply Zinsert_eqmod. auto. omega. apply Int64.eqm_sym; apply Int64.eqm_unsigned_repr.
+    exists rs'; split.
+    eapply exec_straight_opt_step_opt. simpl; eauto. auto.
+    split. exact Q. intros; Simpl. rewrite R by auto. Simpl.
 Qed.
 
 Lemma exec_loadimm_z_x:
@@ -394,19 +394,19 @@ Lemma exec_loadimm_z_x:
   /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
 Proof.
   unfold loadimm_z; destruct 1.
-- econstructor; split.
-  apply exec_straight_one. simpl; eauto. auto.
-  split. Simpl.
-  intros; Simpl.
-- set (accu0 := Zinsert 0 n p 16).
-  set (rs1 := rs#rd <- (Vlong (Int64.repr accu0))).
-  destruct (exec_loadimm_k_x rd k m l H1 rs1 accu0) as (rs2 & P & Q & R); auto.
-  unfold rs1; Simpl.
-  exists rs2; split.
-  eapply exec_straight_opt_step; eauto.
-  simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; omega.
-  split. exact Q. 
-  intros. rewrite R by auto. unfold rs1; Simpl.
+  - econstructor; split.
+    apply exec_straight_one. simpl; eauto. auto.
+    split. Simpl.
+    intros; Simpl.
+  - set (accu0 := Zinsert 0 n p 16).
+    set (rs1 := rs#rd <- (Vlong (Int64.repr accu0))).
+    destruct (exec_loadimm_k_x rd k m l H1 rs1 accu0) as (rs2 & P & Q & R); auto.
+    unfold rs1; Simpl.
+    exists rs2; split.
+    eapply exec_straight_opt_step; eauto.
+    simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; omega.
+    split. exact Q. 
+    intros. rewrite R by auto. unfold rs1; Simpl.
 Qed.
 
 Lemma exec_loadimm_n_x:
@@ -418,22 +418,22 @@ Lemma exec_loadimm_n_x:
   /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
 Proof.
   unfold loadimm_n; destruct 1.
-- econstructor; split.
-  apply exec_straight_one. simpl; eauto. auto.
-  split. Simpl. 
-  intros; Simpl.
-- set (accu0 := Z.lnot (Zinsert 0 n p 16)).
-  set (rs1 := rs#rd <- (Vlong (Int64.repr accu0))).
-  destruct (exec_loadimm_k_x rd k m (negate_decomposition l) 
-                                    (negate_decomposition_wf l H1)
-                                    rs1 accu0) as (rs2 & P & Q & R).
-  unfold rs1; Simpl.
-  exists rs2; split.
-  eapply exec_straight_opt_step; eauto.
-  simpl. unfold rs1. do 5 f_equal.
-  unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; omega.
-  split. unfold accu0 in Q; rewrite recompose_int_negated in Q by auto. exact Q.
-  intros. rewrite R by auto. unfold rs1; Simpl.
+  - econstructor; split.
+    apply exec_straight_one. simpl; eauto. auto.
+    split. Simpl. 
+    intros; Simpl.
+  - set (accu0 := Z.lnot (Zinsert 0 n p 16)).
+    set (rs1 := rs#rd <- (Vlong (Int64.repr accu0))).
+    destruct (exec_loadimm_k_x rd k m (negate_decomposition l) 
+                                      (negate_decomposition_wf l H1)
+                                      rs1 accu0) as (rs2 & P & Q & R).
+    unfold rs1; Simpl.
+    exists rs2; split.
+    eapply exec_straight_opt_step; eauto.
+    simpl. unfold rs1. do 5 f_equal.
+    unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; omega.
+    split. unfold accu0 in Q; rewrite recompose_int_negated in Q by auto. exact Q.
+    intros. rewrite R by auto. unfold rs1; Simpl.
 Qed.
 
 Lemma exec_loadimm64:
@@ -445,23 +445,23 @@ Lemma exec_loadimm64:
 Proof.
   unfold loadimm64, loadimm; intros.
   destruct (is_logical_imm64 n).
-- econstructor; split.
-  apply exec_straight_one. simpl; eauto. auto.
-  split. Simpl. rewrite Int64.repr_unsigned, Int64.or_zero_l; auto.
-  intros; Simpl.
-- set (dz := decompose_int 4%nat (Int64.unsigned n) 0).
-  set (dn := decompose_int 4%nat (Z.lnot (Int64.unsigned n)) 0).
-  assert (A: Int64.repr (recompose_int 0 dz) = n).
-  { transitivity (Int64.repr (Int64.unsigned n)).
-    apply Int64.eqm_samerepr. apply decompose_int_eqmod. 
-    apply Int64.repr_unsigned. }
-  assert (B: Int64.repr (Z.lnot (recompose_int 0 dn)) = n).
-  { transitivity (Int64.repr (Int64.unsigned n)).
-    apply Int64.eqm_samerepr. apply decompose_notint_eqmod. 
-    apply Int64.repr_unsigned. }
-  destruct Nat.leb.
-+ rewrite <- A. apply exec_loadimm_z_x. apply decompose_int_wf; omega.
-+ rewrite <- B. apply exec_loadimm_n_x. apply decompose_int_wf; omega.
+  - econstructor; split.
+    apply exec_straight_one. simpl; eauto. auto.
+    split. Simpl. rewrite Int64.repr_unsigned, Int64.or_zero_l; auto.
+    intros; Simpl.
+  - set (dz := decompose_int 4%nat (Int64.unsigned n) 0).
+    set (dn := decompose_int 4%nat (Z.lnot (Int64.unsigned n)) 0).
+    assert (A: Int64.repr (recompose_int 0 dz) = n).
+    { transitivity (Int64.repr (Int64.unsigned n)).
+      apply Int64.eqm_samerepr. apply decompose_int_eqmod. 
+      apply Int64.repr_unsigned. }
+    assert (B: Int64.repr (Z.lnot (recompose_int 0 dn)) = n).
+    { transitivity (Int64.repr (Int64.unsigned n)).
+      apply Int64.eqm_samerepr. apply decompose_notint_eqmod. 
+      apply Int64.repr_unsigned. }
+    destruct Nat.leb.
+    + rewrite <- A. apply exec_loadimm_z_x. apply decompose_int_wf; omega.
+    + rewrite <- B. apply exec_loadimm_n_x. apply decompose_int_wf; omega.
 Qed.
 
 (** Add immediate *)
@@ -483,17 +483,17 @@ Proof.
   assert (E: Int.unsigned n = nhi + nlo) by (unfold nhi; omega).
   rewrite <- (Int.repr_unsigned n).
   destruct (Z.eqb_spec nhi 0); [|destruct (Z.eqb_spec nlo 0)].
-- econstructor; split. apply exec_straight_one. apply SEM. Simpl. 
-  split. Simpl. do 3 f_equal; omega.
-  intros; Simpl.
-- econstructor; split. apply exec_straight_one. apply SEM. Simpl. 
-  split. Simpl. do 3 f_equal; omega.
-  intros; Simpl.
-- econstructor; split. eapply exec_straight_two.
-  apply SEM. apply SEM. simpl. Simpl.
-  split. Simpl. simpl.  rewrite ASSOC. do 2 f_equal. apply Int.eqm_samerepr.
-  rewrite E. auto with ints.
-  intros; Simpl.
+  - econstructor; split. apply exec_straight_one. apply SEM. Simpl. 
+    split. Simpl. do 3 f_equal; omega.
+    intros; Simpl.
+  - econstructor; split. apply exec_straight_one. apply SEM. Simpl. 
+    split. Simpl. do 3 f_equal; omega.
+    intros; Simpl.
+  - econstructor; split. eapply exec_straight_two.
+    apply SEM. apply SEM. simpl. Simpl.
+    split. Simpl. simpl.  rewrite ASSOC. do 2 f_equal. apply Int.eqm_samerepr.
+    rewrite E. auto with ints.
+    intros; Simpl.
 Qed.
 
 Lemma exec_addimm32:
@@ -506,22 +506,22 @@ Lemma exec_addimm32:
 Proof.
   intros. unfold addimm32. set (nn := Int.neg n).
   destruct (Int.eq n (Int.zero_ext 24 n)); [| destruct (Int.eq nn (Int.zero_ext 24 nn))].
-- apply exec_addimm_aux_32 with (sem := Val.add). auto. intros; apply Val.add_assoc. 
-- rewrite <- Val.sub_opp_add.
-  apply exec_addimm_aux_32 with (sem := Val.sub). auto.
-  intros. rewrite ! Val.sub_add_opp, Val.add_assoc. rewrite Int.neg_add_distr. auto.
-- destruct (Int.lt n Int.zero).
-+ rewrite <- Val.sub_opp_add; fold nn.
-  edestruct (exec_loadimm32 X16 nn) as (rs1 & A & B & C).
-  econstructor; split.
-  eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. auto.
-  split. Simpl. rewrite B, C; eauto with asmgen.
-  intros; Simpl.
-+ edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C).
-  econstructor; split.
-  eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. auto.
-  split. Simpl. rewrite B, C; eauto with asmgen.
-  intros; Simpl.
+  - apply exec_addimm_aux_32 with (sem := Val.add). auto. intros; apply Val.add_assoc. 
+  - rewrite <- Val.sub_opp_add.
+    apply exec_addimm_aux_32 with (sem := Val.sub). auto.
+    intros. rewrite ! Val.sub_add_opp, Val.add_assoc. rewrite Int.neg_add_distr. auto.
+  - destruct (Int.lt n Int.zero).
+    + rewrite <- Val.sub_opp_add; fold nn.
+      edestruct (exec_loadimm32 X16 nn) as (rs1 & A & B & C).
+      econstructor; split.
+      eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. auto.
+      split. Simpl. rewrite B, C; eauto with asmgen.
+      intros; Simpl.
+    + edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C).
+      econstructor; split.
+      eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. auto.
+      split. Simpl. rewrite B, C; eauto with asmgen.
+      intros; Simpl.
 Qed.
 
 Lemma exec_addimm_aux_64:
@@ -541,17 +541,17 @@ Proof.
   assert (E: Int64.unsigned n = nhi + nlo) by (unfold nhi; omega).
   rewrite <- (Int64.repr_unsigned n).
   destruct (Z.eqb_spec nhi 0); [|destruct (Z.eqb_spec nlo 0)].
-- econstructor; split. apply exec_straight_one. apply SEM. Simpl. 
-  split. Simpl. do 3 f_equal; omega.
-  intros; Simpl.
-- econstructor; split. apply exec_straight_one. apply SEM. Simpl. 
-  split. Simpl. do 3 f_equal; omega.
-  intros; Simpl.
-- econstructor; split. eapply exec_straight_two.
-  apply SEM. apply SEM. Simpl. Simpl.
-  split. Simpl. rewrite ASSOC. do 2 f_equal. apply Int64.eqm_samerepr.
-  rewrite E. auto with ints.
-  intros; Simpl.
+  - econstructor; split. apply exec_straight_one. apply SEM. Simpl. 
+    split. Simpl. do 3 f_equal; omega.
+    intros; Simpl.
+  - econstructor; split. apply exec_straight_one. apply SEM. Simpl. 
+    split. Simpl. do 3 f_equal; omega.
+    intros; Simpl.
+  - econstructor; split. eapply exec_straight_two.
+    apply SEM. apply SEM. Simpl. Simpl.
+    split. Simpl. rewrite ASSOC. do 2 f_equal. apply Int64.eqm_samerepr.
+    rewrite E. auto with ints.
+    intros; Simpl.
 Qed.
 
 Lemma exec_addimm64:
@@ -565,22 +565,22 @@ Proof.
   intros. 
   unfold addimm64. set (nn := Int64.neg n).
   destruct (Int64.eq n (Int64.zero_ext 24 n)); [| destruct (Int64.eq nn (Int64.zero_ext 24 nn))].
-- apply exec_addimm_aux_64 with (sem := Val.addl). auto. intros; apply Val.addl_assoc. 
-- rewrite <- Val.subl_opp_addl.
-  apply exec_addimm_aux_64 with (sem := Val.subl). auto.
-  intros. rewrite ! Val.subl_addl_opp, Val.addl_assoc. rewrite Int64.neg_add_distr. auto.
-- destruct (Int64.lt n Int64.zero).
-+ rewrite <- Val.subl_opp_addl; fold nn.
-  edestruct (exec_loadimm64 X16 nn) as (rs1 & A & B & C).
-  econstructor; split.
-  eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. Simpl. 
-  split. Simpl. rewrite B, C; eauto with asmgen. simpl. rewrite Int64.shl'_zero. auto.
-  intros; Simpl.
-+ edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C).
-  econstructor; split.
-  eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. Simpl. 
-  split. Simpl. rewrite B, C; eauto with asmgen. simpl. rewrite Int64.shl'_zero. auto.
-  intros; Simpl.
+  - apply exec_addimm_aux_64 with (sem := Val.addl). auto. intros; apply Val.addl_assoc. 
+  - rewrite <- Val.subl_opp_addl.
+    apply exec_addimm_aux_64 with (sem := Val.subl). auto.
+    intros. rewrite ! Val.subl_addl_opp, Val.addl_assoc. rewrite Int64.neg_add_distr. auto.
+  - destruct (Int64.lt n Int64.zero).
+    + rewrite <- Val.subl_opp_addl; fold nn.
+      edestruct (exec_loadimm64 X16 nn) as (rs1 & A & B & C).
+      econstructor; split.
+      eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. Simpl. 
+      split. Simpl. rewrite B, C; eauto with asmgen. simpl. rewrite Int64.shl'_zero. auto.
+      intros; Simpl.
+    + edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C).
+      econstructor; split.
+      eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. Simpl. 
+      split. Simpl. rewrite B, C; eauto with asmgen. simpl. rewrite Int64.shl'_zero. auto.
+      intros; Simpl.
 Qed.
 
 (** Logical immediate *)
@@ -604,15 +604,15 @@ Lemma exec_logicalimm32:
 Proof.
   intros until sem; intros SEM1 SEM2; intros. unfold logicalimm32.
   destruct (is_logical_imm32 n).
-- econstructor; split. 
-  apply exec_straight_one. apply SEM1.
-  split. Simpl. rewrite Int.repr_unsigned; auto. intros; Simpl.
-- edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C).
-  econstructor; split.
-  eapply exec_straight_trans. eexact A.  
-  apply exec_straight_one. apply SEM2.
-  split. Simpl. f_equal; auto. apply C; auto with asmgen.
-  intros; Simpl. 
+  - econstructor; split. 
+    apply exec_straight_one. apply SEM1.
+    split. Simpl. rewrite Int.repr_unsigned; auto. intros; Simpl.
+  - edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C).
+    econstructor; split.
+    eapply exec_straight_trans. eexact A.  
+    apply exec_straight_one. apply SEM2.
+    split. Simpl. f_equal; auto. apply C; auto with asmgen.
+    intros; Simpl. 
 Qed.
 
 Lemma exec_logicalimm64:
@@ -634,15 +634,15 @@ Lemma exec_logicalimm64:
 Proof.
   intros until sem; intros SEM1 SEM2; intros. unfold logicalimm64.
   destruct (is_logical_imm64 n).
-- econstructor; split. 
-  apply exec_straight_one. apply SEM1.
-  split. Simpl. rewrite Int64.repr_unsigned. auto. intros; Simpl.
-- edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C).
-  econstructor; split.
-  eapply exec_straight_trans. eexact A.  
-  apply exec_straight_one. apply SEM2.
-  split. Simpl. f_equal; auto. apply C; auto with asmgen.
-  intros; Simpl. 
+  - econstructor; split. 
+    apply exec_straight_one. apply SEM1.
+    split. Simpl. rewrite Int64.repr_unsigned. auto. intros; Simpl.
+  - edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C).
+    econstructor; split.
+    eapply exec_straight_trans. eexact A.  
+    apply exec_straight_one. apply SEM2.
+    split. Simpl. f_equal; auto. apply C; auto with asmgen.
+    intros; Simpl. 
 Qed.
 
 (** Load address of symbol *)
@@ -655,22 +655,22 @@ Lemma exec_loadsymbol: forall rd s ofs k rs m,
   /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
 Proof.
   unfold loadsymbol; intros. destruct (Archi.pic_code tt).
-- predSpec Ptrofs.eq Ptrofs.eq_spec ofs Ptrofs.zero.
-+ subst ofs. econstructor; split.
-  apply exec_straight_one. simpl; eauto.
-  split. Simpl. intros; Simpl.
-+ exploit exec_addimm64. instantiate (1 := rd). simpl. destruct H; congruence.
-  intros (rs1 & A & B & C).
-  econstructor; split.
-  econstructor. simpl; eauto. auto. eexact A. 
-  split. simpl in B; rewrite B. Simpl. 
-  rewrite <- Genv.shift_symbol_address_64 by auto.
-  rewrite Ptrofs.add_zero_l, Ptrofs.of_int64_to_int64 by auto. auto.
-  intros. rewrite C by auto. Simpl.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto.
-  split. Simpl.
-  intros; Simpl.
+  - predSpec Ptrofs.eq Ptrofs.eq_spec ofs Ptrofs.zero.
+    + subst ofs. econstructor; split.
+      apply exec_straight_one. simpl; eauto.
+      split. Simpl. intros; Simpl.
+    + exploit exec_addimm64. instantiate (1 := rd). simpl. destruct H; congruence.
+      intros (rs1 & A & B & C).
+      econstructor; split.
+      econstructor. simpl; eauto. auto. eexact A. 
+      split. simpl in B; rewrite B. Simpl. 
+      rewrite <- Genv.shift_symbol_address_64 by auto.
+      rewrite Ptrofs.add_zero_l, Ptrofs.of_int64_to_int64 by auto. auto.
+      intros. rewrite C by auto. Simpl.
+  - econstructor; split.
+    eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto.
+    split. Simpl.
+    intros; Simpl.
 Qed.
 
 (** Shifted operands *)
@@ -754,18 +754,18 @@ Lemma exec_move_extended: forall rd r1 ex (a: amount64) k rs m,
   /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
 Proof.
   unfold move_extended; intros. predSpec Int.eq Int.eq_spec a Int.zero.
-- exploit (exec_move_extended_base rd r1 ex). intros (rs' & A & B & C).
-  exists rs'; split. eexact A. split. unfold Op.eval_extend. rewrite H. rewrite B.
-  destruct ex, (rs r1); simpl; auto; rewrite Int64.shl'_zero; auto.
-  auto.
-- Local Opaque Val.addl.
-  exploit (exec_move_extended_base rd r1 ex). intros (rs' & A & B & C).
-  econstructor; split.
-  eapply exec_straight_trans. eexact A. apply exec_straight_one.
-  unfold exec_basic, exec_arith_instr, arith_eval_rr0r.
-  change (SOlsl a) with (transl_shift Slsl a). rewrite transl_eval_shiftl''. eauto. auto.
-  split. Simpl. rewrite B. auto. 
-  intros; Simpl.
+  - exploit (exec_move_extended_base rd r1 ex). intros (rs' & A & B & C).
+    exists rs'; split. eexact A. split. unfold Op.eval_extend. rewrite H. rewrite B.
+    destruct ex, (rs r1); simpl; auto; rewrite Int64.shl'_zero; auto.
+    auto.
+  - Local Opaque Val.addl.
+    exploit (exec_move_extended_base rd r1 ex). intros (rs' & A & B & C).
+    econstructor; split.
+    eapply exec_straight_trans. eexact A. apply exec_straight_one.
+    unfold exec_basic, exec_arith_instr, arith_eval_rr0r.
+    change (SOlsl a) with (transl_shift Slsl a). rewrite transl_eval_shiftl''. eauto. auto.
+    split. Simpl. rewrite B. auto. 
+    intros; Simpl.
 Qed.
 
 Lemma exec_arith_extended:
@@ -786,17 +786,17 @@ Lemma exec_arith_extended:
   /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
 Proof.
   intros sem insnX insnS EX ES; intros. unfold arith_extended. destruct (Int.ltu a (Int.repr 5)).
-- econstructor; split. 
-  apply exec_straight_one. rewrite EX; eauto. auto.
-  split. Simpl. f_equal. destruct ex; auto.
-  intros; Simpl.
-- exploit (exec_move_extended_base X16 r2 ex). intros (rs' & A & B & C).
-  econstructor; split.
-  eapply exec_straight_trans. eexact A. apply exec_straight_one. 
-  rewrite ES. eauto. auto.
-  split. Simpl. unfold ir0. rewrite C by eauto with asmgen. f_equal. 
-  rewrite B. destruct ex; auto.
-  intros; Simpl.
+  - econstructor; split. 
+    apply exec_straight_one. rewrite EX; eauto. auto.
+    split. Simpl. f_equal. destruct ex; auto.
+    intros; Simpl.
+  - exploit (exec_move_extended_base X16 r2 ex). intros (rs' & A & B & C).
+    econstructor; split.
+    eapply exec_straight_trans. eexact A. apply exec_straight_one. 
+    rewrite ES. eauto. auto.
+    split. Simpl. unfold ir0. rewrite C by eauto with asmgen. f_equal. 
+    rewrite B. destruct ex; auto.
+    intros; Simpl.
 Qed. 
 
 (** Extended right shift *)
@@ -811,15 +811,15 @@ Lemma exec_shrx32: forall (rd r1: ireg) (n: int) k v (rs: regset) m,
 Proof.
   unfold shrx32; intros. apply Val.shrx_shr_2 in H.
   destruct (Int.eq n Int.zero) eqn:E0.
-- econstructor; split. apply exec_straight_one; simpl; eauto. 
-  split. Simpl. subst v; auto. intros; Simpl.
-- econstructor; split. eapply exec_straight_three.
-  unfold exec_basic, exec_arith_instr, arith_eval_rr0r.
-  rewrite or_zero_eval_shift_op_int by congruence. eauto.
-  simpl; eauto.
-  unfold exec_basic, exec_arith_instr, arith_eval_rr0r.
-  rewrite or_zero_eval_shift_op_int by congruence. eauto.
-  split. subst v; Simpl. intros; Simpl.
+  - econstructor; split. apply exec_straight_one; simpl; eauto. 
+    split. Simpl. subst v; auto. intros; Simpl.
+  - econstructor; split. eapply exec_straight_three.
+    unfold exec_basic, exec_arith_instr, arith_eval_rr0r.
+    rewrite or_zero_eval_shift_op_int by congruence. eauto.
+    simpl; eauto.
+    unfold exec_basic, exec_arith_instr, arith_eval_rr0r.
+    rewrite or_zero_eval_shift_op_int by congruence. eauto.
+    split. subst v; Simpl. intros; Simpl.
 Qed.
 
 Lemma exec_shrx32_none: forall (rd r1: ireg) (n: int) k x (rs: regset) m,
@@ -832,15 +832,15 @@ Lemma exec_shrx32_none: forall (rd r1: ireg) (n: int) k x (rs: regset) m,
 Proof.
   unfold shrx32; intros.
   destruct (Int.eq n Int.zero) eqn:E0.
-- econstructor; split. apply exec_straight_one; simpl; eauto. 
-  split. Simpl. auto. intros; Simpl.
-- econstructor; split. eapply exec_straight_three.
-  unfold exec_basic, exec_arith_instr, arith_eval_rr0r.
-  rewrite or_zero_eval_shift_op_int by congruence. eauto.
-  simpl; eauto.
-  unfold exec_basic, exec_arith_instr, arith_eval_rr0r.
-  rewrite or_zero_eval_shift_op_int by congruence. eauto.
-  split. Simpl. intros; Simpl.
+  - econstructor; split. apply exec_straight_one; simpl; eauto. 
+    split. Simpl. auto. intros; Simpl.
+  - econstructor; split. eapply exec_straight_three.
+    unfold exec_basic, exec_arith_instr, arith_eval_rr0r.
+    rewrite or_zero_eval_shift_op_int by congruence. eauto.
+    simpl; eauto.
+    unfold exec_basic, exec_arith_instr, arith_eval_rr0r.
+    rewrite or_zero_eval_shift_op_int by congruence. eauto.
+    split. Simpl. intros; Simpl.
 Qed.
 
 Lemma exec_shrx64: forall (rd r1: ireg) (n: int) k v (rs: regset) m,
@@ -853,15 +853,15 @@ Lemma exec_shrx64: forall (rd r1: ireg) (n: int) k v (rs: regset) m,
 Proof.
   unfold shrx64; intros. apply Val.shrxl_shrl_2 in H.
   destruct (Int.eq n Int.zero) eqn:E.
-- econstructor; split. apply exec_straight_one; simpl; eauto. 
-  split. Simpl. subst v; auto. intros; Simpl.
-- econstructor; split. eapply exec_straight_three.
-  unfold exec_basic, exec_arith_instr, arith_eval_rr0r.
-  rewrite or_zero_eval_shift_op_long by congruence. eauto.
-  simpl; eauto.
-  unfold exec_basic, exec_arith_instr, arith_eval_rr0r.
-  rewrite or_zero_eval_shift_op_long by congruence. eauto.
-  split. subst v; Simpl. intros; Simpl.
+  - econstructor; split. apply exec_straight_one; simpl; eauto. 
+    split. Simpl. subst v; auto. intros; Simpl.
+  - econstructor; split. eapply exec_straight_three.
+    unfold exec_basic, exec_arith_instr, arith_eval_rr0r.
+    rewrite or_zero_eval_shift_op_long by congruence. eauto.
+    simpl; eauto.
+    unfold exec_basic, exec_arith_instr, arith_eval_rr0r.
+    rewrite or_zero_eval_shift_op_long by congruence. eauto.
+    split. subst v; Simpl. intros; Simpl.
 Qed.
 
 Lemma exec_shrx64_none: forall (rd r1: ireg) (n: int) k x (rs: regset) m,
@@ -874,15 +874,15 @@ Lemma exec_shrx64_none: forall (rd r1: ireg) (n: int) k x (rs: regset) m,
 Proof.
   unfold shrx64; intros.
   destruct (Int.eq n Int.zero) eqn:E.
-- econstructor; split. apply exec_straight_one; simpl; eauto. 
-  split. Simpl. auto. intros; Simpl.
-- econstructor; split. eapply exec_straight_three.
-  unfold exec_basic, exec_arith_instr, arith_eval_rr0r.
-  rewrite or_zero_eval_shift_op_long by congruence. eauto.
-  simpl; eauto.
-  unfold exec_basic, exec_arith_instr, arith_eval_rr0r.
-  rewrite or_zero_eval_shift_op_long by congruence. eauto.
-  split. Simpl. intros; Simpl.
+  - econstructor; split. apply exec_straight_one; simpl; eauto. 
+    split. Simpl. auto. intros; Simpl.
+  - econstructor; split. eapply exec_straight_three.
+    unfold exec_basic, exec_arith_instr, arith_eval_rr0r.
+    rewrite or_zero_eval_shift_op_long by congruence. eauto.
+    simpl; eauto.
+    unfold exec_basic, exec_arith_instr, arith_eval_rr0r.
+    rewrite or_zero_eval_shift_op_long by congruence. eauto.
+    split. Simpl. intros; Simpl.
 Qed.
 
 Ltac TranslOpBase :=
@@ -913,14 +913,14 @@ Proof.
   destruct v1; try discriminate; destruct v2; try discriminate.
   simpl in H; inv H.
   unfold Val_cmpu; simpl. destruct c; simpl.
-- destruct (Int.eq i i0); auto.
-- destruct (Int.eq i i0); auto.
-- rewrite Int.lt_sub_overflow. destruct (Int.lt i i0); auto.
-- rewrite Int.lt_sub_overflow, Int.not_lt.
-  destruct (Int.eq i i0), (Int.lt i i0); auto.
-- rewrite Int.lt_sub_overflow, (Int.lt_not i). 
-  destruct (Int.eq i i0), (Int.lt i i0); auto.
-- rewrite Int.lt_sub_overflow. destruct (Int.lt i i0); auto.
+  - destruct (Int.eq i i0); auto.
+  - destruct (Int.eq i i0); auto.
+  - rewrite Int.lt_sub_overflow. destruct (Int.lt i i0); auto.
+  - rewrite Int.lt_sub_overflow, Int.not_lt.
+    destruct (Int.eq i i0), (Int.lt i i0); auto.
+  - rewrite Int.lt_sub_overflow, (Int.lt_not i). 
+    destruct (Int.eq i i0), (Int.lt i i0); auto.
+  - rewrite Int.lt_sub_overflow. destruct (Int.lt i i0); auto.
 Qed.
 
 Lemma eval_testcond_compare_uint: forall c v1 v2 b rs,
@@ -933,12 +933,12 @@ Proof.
   destruct v1; try discriminate; destruct v2; try discriminate.
   simpl in H; inv H.
   unfold Val_cmpu; simpl. destruct c; simpl.
-- destruct (Int.eq i i0); auto.
-- destruct (Int.eq i i0); auto.
-- destruct (Int.ltu i i0); auto.
-- rewrite (Int.not_ltu i). destruct (Int.eq i i0), (Int.ltu i i0); auto.
-- rewrite (Int.ltu_not i). destruct (Int.eq i i0), (Int.ltu i i0); auto.
-- destruct (Int.ltu i i0); auto.
+  - destruct (Int.eq i i0); auto.
+  - destruct (Int.eq i i0); auto.
+  - destruct (Int.ltu i i0); auto.
+  - rewrite (Int.not_ltu i). destruct (Int.eq i i0), (Int.ltu i i0); auto.
+  - rewrite (Int.ltu_not i). destruct (Int.eq i i0), (Int.ltu i i0); auto.
+  - destruct (Int.ltu i i0); auto.
 Qed.
 
 Lemma compare_long_spec: forall rs v1 v2,
@@ -978,14 +978,14 @@ Proof.
   destruct v1; try discriminate; destruct v2; try discriminate.
   simpl in H; inv H.
   unfold Val_cmplu; simpl. destruct c; simpl.
-- destruct (Int64.eq i i0); auto.
-- destruct (Int64.eq i i0); auto.
-- rewrite int64_sub_overflow. destruct (Int64.lt i i0); auto.
-- rewrite int64_sub_overflow, Int64.not_lt.
-  destruct (Int64.eq i i0), (Int64.lt i i0); auto.
-- rewrite int64_sub_overflow, (Int64.lt_not i). 
-  destruct (Int64.eq i i0), (Int64.lt i i0); auto.
-- rewrite int64_sub_overflow. destruct (Int64.lt i i0); auto.
+  - destruct (Int64.eq i i0); auto.
+  - destruct (Int64.eq i i0); auto.
+  - rewrite int64_sub_overflow. destruct (Int64.lt i i0); auto.
+  - rewrite int64_sub_overflow, Int64.not_lt.
+    destruct (Int64.eq i i0), (Int64.lt i i0); auto.
+  - rewrite int64_sub_overflow, (Int64.lt_not i). 
+    destruct (Int64.eq i i0), (Int64.lt i i0); auto.
+  - rewrite int64_sub_overflow. destruct (Int64.lt i i0); auto.
 Qed.
 
 Lemma eval_testcond_compare_ulong: forall c v1 v2 b rs,
@@ -996,37 +996,37 @@ Proof.
   set (rs' := compare_long rs v1 v2). intros (B & C & D & E).
   unfold eval_testcond; rewrite B, C, D, E; unfold Val_cmplu.
   destruct v1; try discriminate; destruct v2; try discriminate; simpl in H.
-- (* int-int *)
-  inv H. destruct c; simpl.
-+ destruct (Int64.eq i i0); auto.
-+ destruct (Int64.eq i i0); auto.
-+ destruct (Int64.ltu i i0); auto.
-+ rewrite (Int64.not_ltu i). destruct (Int64.eq i i0), (Int64.ltu i i0); auto.
-+ rewrite (Int64.ltu_not i). destruct (Int64.eq i i0), (Int64.ltu i i0); auto.
-+ destruct (Int64.ltu i i0); auto.
-- (* int-ptr *)
-  simpl.
-  destruct (Archi.ptr64); simpl; try discriminate.
-  destruct (Int64.eq i Int64.zero); simpl; try discriminate.
-  destruct c; simpl in H; inv H; reflexivity.
-- (* ptr-int *)
-  simpl.
-  destruct (Archi.ptr64); simpl; try discriminate.
-  destruct (Int64.eq i0 Int64.zero); try discriminate.
-  destruct c; simpl in H; inv H; reflexivity.
-- (* ptr-ptr *)
-  simpl. 
-  destruct (eq_block b0 b1).
-  destruct (Archi.ptr64); simpl; try discriminate.
-  inv H.
-  destruct c; simpl.
-* destruct (Ptrofs.eq i i0); auto.
-* destruct (Ptrofs.eq i i0); auto.
-* destruct (Ptrofs.ltu i i0); auto.
-* rewrite (Ptrofs.not_ltu i). destruct (Ptrofs.eq i i0), (Ptrofs.ltu i i0); auto.
-* rewrite (Ptrofs.ltu_not i). destruct (Ptrofs.eq i i0), (Ptrofs.ltu i i0); auto.
-* destruct (Ptrofs.ltu i i0); auto.
-* destruct c; simpl in H; inv H; reflexivity.
+  - (* int-int *)
+    inv H. destruct c; simpl.
+    + destruct (Int64.eq i i0); auto.
+    + destruct (Int64.eq i i0); auto.
+    + destruct (Int64.ltu i i0); auto.
+    + rewrite (Int64.not_ltu i). destruct (Int64.eq i i0), (Int64.ltu i i0); auto.
+    + rewrite (Int64.ltu_not i). destruct (Int64.eq i i0), (Int64.ltu i i0); auto.
+    + destruct (Int64.ltu i i0); auto.
+  - (* int-ptr *)
+    simpl.
+    destruct (Archi.ptr64); simpl; try discriminate.
+    destruct (Int64.eq i Int64.zero); simpl; try discriminate.
+    destruct c; simpl in H; inv H; reflexivity.
+  - (* ptr-int *)
+    simpl.
+    destruct (Archi.ptr64); simpl; try discriminate.
+    destruct (Int64.eq i0 Int64.zero); try discriminate.
+    destruct c; simpl in H; inv H; reflexivity.
+  - (* ptr-ptr *)
+    simpl. 
+    destruct (eq_block b0 b1).
+    destruct (Archi.ptr64); simpl; try discriminate.
+    inv H.
+    destruct c; simpl.
+    * destruct (Ptrofs.eq i i0); auto.
+    * destruct (Ptrofs.eq i i0); auto.
+    * destruct (Ptrofs.ltu i i0); auto.
+    * rewrite (Ptrofs.not_ltu i). destruct (Ptrofs.eq i i0), (Ptrofs.ltu i i0); auto.
+    * rewrite (Ptrofs.ltu_not i). destruct (Ptrofs.eq i i0), (Ptrofs.ltu i i0); auto.
+    * destruct (Ptrofs.ltu i i0); auto.
+    * destruct c; simpl in H; inv H; reflexivity.
 Qed.
 
 Lemma compare_float_spec: forall rs f1 f2,
@@ -1132,179 +1132,179 @@ Lemma transl_cond_correct:
   /\ forall r, data_preg r = true -> rs'#r = rs#r.
 Proof.
   intros until m; intros TR. destruct cond; simpl in TR; ArgsInv.
-- (* Ccomp *)
-  econstructor; split. apply exec_straight_one. simpl; eauto.
-  split; intros. apply eval_testcond_compare_sint; auto. 
-  destruct r; reflexivity || discriminate.
-- (* Ccompu *)
-  econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split; intros. apply eval_testcond_compare_uint; auto. 
-  destruct r; reflexivity || discriminate.
-- (* Ccompimm *)
-  destruct (is_arith_imm32 n); [|destruct (is_arith_imm32 (Int.neg n))].
-+ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_sint; auto. 
-  destruct r; reflexivity || discriminate.
-+ econstructor; split.
-  apply exec_straight_one. simpl. rewrite Int.repr_unsigned, Int.neg_involutive. eauto. auto.
-  split; intros. apply eval_testcond_compare_sint; auto. 
-  destruct r; reflexivity || discriminate.
-+ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C).
-  econstructor; split.
-  eapply exec_straight_trans. eexact A. apply exec_straight_one.
-  simpl. rewrite B, C by eauto with asmgen. eauto.
-  split; intros. apply eval_testcond_compare_sint; auto. 
-  transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
-- (* Ccompuimm *)
-  destruct (is_arith_imm32 n); [|destruct (is_arith_imm32 (Int.neg n))].
-+ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_uint; auto. 
-  destruct r; reflexivity || discriminate.
-+ econstructor; split.
-  apply exec_straight_one. simpl. rewrite Int.repr_unsigned, Int.neg_involutive. eauto. auto.
-  split; intros. apply eval_testcond_compare_uint; auto. 
-  destruct r; reflexivity || discriminate.
-+ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C).
-  econstructor; split.
-  eapply exec_straight_trans. eexact A. apply exec_straight_one.
-  simpl. rewrite B, C by eauto with asmgen. eauto. auto.
-  split; intros. apply eval_testcond_compare_uint; auto. 
-  transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
-- (* Ccompshift *)
-  econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split; intros. rewrite transl_eval_shift. apply eval_testcond_compare_sint; auto. 
-  destruct r; reflexivity || discriminate.
-- (* Ccompushift *)
-  econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split; intros. rewrite transl_eval_shift. apply eval_testcond_compare_uint; auto. 
-  destruct r; reflexivity || discriminate.
-- (* Cmaskzero *)
-  destruct (is_logical_imm32 n).
-+ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Ceq); auto.
-  destruct r; reflexivity || discriminate.
-+ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C).
-  econstructor; split.
-  eapply exec_straight_trans. eexact A.
-  apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. auto.
-  split; intros. apply (eval_testcond_compare_sint Ceq); auto.
-  transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
-- (* Cmasknotzero *)
-  destruct (is_logical_imm32 n).
-+ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Cne); auto.
-  destruct r; reflexivity || discriminate.
-+ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C).
-  econstructor; split.
-  eapply exec_straight_trans. eexact A.
-  apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. auto.
-  split; intros. apply (eval_testcond_compare_sint Cne); auto.
-  transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
-- (* Ccompl *)
-  econstructor; split. apply exec_straight_one. simpl; eauto.
-  split; intros. apply eval_testcond_compare_slong; auto. 
-  destruct r; reflexivity || discriminate.
-- (* Ccomplu *)
-  econstructor; split. apply exec_straight_one. simpl; eauto.
-  split; intros. apply eval_testcond_compare_ulong; auto.
-  erewrite Val_cmplu_bool_correct; eauto.
-  destruct r; reflexivity || discriminate.
-- (* Ccomplimm *)
-  destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))].
-+ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_slong; auto. 
-  destruct r; reflexivity || discriminate.
-+ econstructor; split.
-  apply exec_straight_one. simpl. rewrite Int64.repr_unsigned, Int64.neg_involutive. eauto.
-  split; intros. apply eval_testcond_compare_slong; auto. 
-  destruct r; reflexivity || discriminate.
-+ exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C).
-  econstructor; split.
-  eapply exec_straight_trans. eexact A. apply exec_straight_one.
-  simpl. rewrite B, C by eauto with asmgen. eauto. auto.
-  split; intros. apply eval_testcond_compare_slong; auto. 
-  transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
-- (* Ccompluimm *)
-  destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))].
-+ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_ulong; auto.
-  erewrite Val_cmplu_bool_correct; eauto.
-  destruct r; reflexivity || discriminate.
-+ econstructor; split.
-  apply exec_straight_one. simpl. rewrite Int64.repr_unsigned, Int64.neg_involutive. eauto.
-  split; intros. apply eval_testcond_compare_ulong; auto.
-  erewrite Val_cmplu_bool_correct; eauto.
-  destruct r; reflexivity || discriminate.
-+ exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C).
-  econstructor; split.
-  eapply exec_straight_trans. eexact A. apply exec_straight_one.
-  simpl. rewrite B, C by eauto with asmgen. eauto.
-  split; intros. apply eval_testcond_compare_ulong; auto.
-  erewrite Val_cmplu_bool_correct; eauto. 
-  transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
-- (* Ccomplshift *)
-  econstructor; split. apply exec_straight_one. simpl; eauto.
-  split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_slong; auto. 
-  destruct r; reflexivity || discriminate.
-- (* Ccomplushift *)
-  econstructor; split. apply exec_straight_one. simpl; eauto.
-  split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_ulong; auto.
-  erewrite Val_cmplu_bool_correct; eauto. 
-  destruct r; reflexivity || discriminate.
-- (* Cmasklzero *)
-  destruct (is_logical_imm64 n).
-+ econstructor; split. apply exec_straight_one. simpl; eauto.
-  split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Ceq); auto.
-  destruct r; reflexivity || discriminate.
-+ exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C).
-  econstructor; split.
-  eapply exec_straight_trans. eexact A.
-  apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto.
-  split; intros. apply (eval_testcond_compare_slong Ceq); auto.
-  transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
-- (* Cmasknotzero *)
-  destruct (is_logical_imm64 n).
-+ econstructor; split. apply exec_straight_one. simpl; eauto.
-  split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Cne); auto.
-  destruct r; reflexivity || discriminate.
-+ exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C).
-  econstructor; split.
-  eapply exec_straight_trans. eexact A.
-  apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto.
-  split; intros. apply (eval_testcond_compare_slong Cne); auto.
-  transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
-- (* Ccompf *)
-  econstructor; split. apply exec_straight_one. simpl; eauto.
-  split; intros. apply eval_testcond_compare_float; auto.
-  destruct r; discriminate || rewrite compare_float_inv; auto.
-- (* Cnotcompf *)
-  econstructor; split. apply exec_straight_one. simpl; eauto.
-  split; intros. apply eval_testcond_compare_not_float; auto.
-  destruct r; discriminate || rewrite compare_float_inv; auto.
-- (* Ccompfzero *)
-  econstructor; split. apply exec_straight_one. simpl; eauto.
-  split; intros. apply eval_testcond_compare_float; auto.
-  destruct r; discriminate || rewrite compare_float_inv; auto.
-- (* Cnotcompfzero *)
-  econstructor; split. apply exec_straight_one. simpl; eauto.
-  split; intros. apply eval_testcond_compare_not_float; auto.
-  destruct r; discriminate || rewrite compare_float_inv; auto.
-- (* Ccompfs *)
-  econstructor; split. apply exec_straight_one. simpl; eauto.
-  split; intros. apply eval_testcond_compare_single; auto.
-  destruct r; discriminate || rewrite compare_single_inv; auto.
-- (* Cnotcompfs *)
-  econstructor; split. apply exec_straight_one. simpl; eauto.
-  split; intros. apply eval_testcond_compare_not_single; auto.
-  destruct r; discriminate || rewrite compare_single_inv; auto.
-- (* Ccompfszero *)
-  econstructor; split. apply exec_straight_one. simpl; eauto.
-  split; intros. apply eval_testcond_compare_single; auto.
-  destruct r; discriminate || rewrite compare_single_inv; auto.
-- (* Cnotcompfszero *)
-  econstructor; split. apply exec_straight_one. simpl; eauto.
-  split; intros. apply eval_testcond_compare_not_single; auto.
-  destruct r; discriminate || rewrite compare_single_inv; auto.
+  - (* Ccomp *)
+    econstructor; split. apply exec_straight_one. simpl; eauto.
+    split; intros. apply eval_testcond_compare_sint; auto. 
+    destruct r; reflexivity || discriminate.
+  - (* Ccompu *)
+    econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+    split; intros. apply eval_testcond_compare_uint; auto. 
+    destruct r; reflexivity || discriminate.
+  - (* Ccompimm *)
+    destruct (is_arith_imm32 n); [|destruct (is_arith_imm32 (Int.neg n))].
+    + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+      split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_sint; auto. 
+      destruct r; reflexivity || discriminate.
+    + econstructor; split.
+      apply exec_straight_one. simpl. rewrite Int.repr_unsigned, Int.neg_involutive. eauto. auto.
+      split; intros. apply eval_testcond_compare_sint; auto. 
+      destruct r; reflexivity || discriminate.
+    + exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C).
+      econstructor; split.
+      eapply exec_straight_trans. eexact A. apply exec_straight_one.
+      simpl. rewrite B, C by eauto with asmgen. eauto.
+      split; intros. apply eval_testcond_compare_sint; auto. 
+      transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
+  - (* Ccompuimm *)
+    destruct (is_arith_imm32 n); [|destruct (is_arith_imm32 (Int.neg n))].
+    + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+      split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_uint; auto. 
+      destruct r; reflexivity || discriminate.
+    + econstructor; split.
+      apply exec_straight_one. simpl. rewrite Int.repr_unsigned, Int.neg_involutive. eauto. auto.
+      split; intros. apply eval_testcond_compare_uint; auto. 
+      destruct r; reflexivity || discriminate.
+    + exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C).
+      econstructor; split.
+      eapply exec_straight_trans. eexact A. apply exec_straight_one.
+      simpl. rewrite B, C by eauto with asmgen. eauto. auto.
+      split; intros. apply eval_testcond_compare_uint; auto. 
+      transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
+  - (* Ccompshift *)
+    econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+    split; intros. rewrite transl_eval_shift. apply eval_testcond_compare_sint; auto. 
+    destruct r; reflexivity || discriminate.
+  - (* Ccompushift *)
+    econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+    split; intros. rewrite transl_eval_shift. apply eval_testcond_compare_uint; auto. 
+    destruct r; reflexivity || discriminate.
+  - (* Cmaskzero *)
+    destruct (is_logical_imm32 n).
+    + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+      split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Ceq); auto.
+      destruct r; reflexivity || discriminate.
+    + exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C).
+      econstructor; split.
+      eapply exec_straight_trans. eexact A.
+      apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. auto.
+      split; intros. apply (eval_testcond_compare_sint Ceq); auto.
+      transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
+  - (* Cmasknotzero *)
+    destruct (is_logical_imm32 n).
+    + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+      split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Cne); auto.
+      destruct r; reflexivity || discriminate.
+    + exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C).
+      econstructor; split.
+      eapply exec_straight_trans. eexact A.
+      apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. auto.
+      split; intros. apply (eval_testcond_compare_sint Cne); auto.
+      transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
+  - (* Ccompl *)
+    econstructor; split. apply exec_straight_one. simpl; eauto.
+    split; intros. apply eval_testcond_compare_slong; auto. 
+    destruct r; reflexivity || discriminate.
+  - (* Ccomplu *)
+    econstructor; split. apply exec_straight_one. simpl; eauto.
+    split; intros. apply eval_testcond_compare_ulong; auto.
+    erewrite Val_cmplu_bool_correct; eauto.
+    destruct r; reflexivity || discriminate.
+  - (* Ccomplimm *)
+    destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))].
+    + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+      split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_slong; auto. 
+      destruct r; reflexivity || discriminate.
+    + econstructor; split.
+      apply exec_straight_one. simpl. rewrite Int64.repr_unsigned, Int64.neg_involutive. eauto.
+      split; intros. apply eval_testcond_compare_slong; auto. 
+      destruct r; reflexivity || discriminate.
+    + exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C).
+      econstructor; split.
+      eapply exec_straight_trans. eexact A. apply exec_straight_one.
+      simpl. rewrite B, C by eauto with asmgen. eauto. auto.
+      split; intros. apply eval_testcond_compare_slong; auto. 
+      transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
+  - (* Ccompluimm *)
+    destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))].
+    + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+      split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_ulong; auto.
+      erewrite Val_cmplu_bool_correct; eauto.
+      destruct r; reflexivity || discriminate.
+    + econstructor; split.
+      apply exec_straight_one. simpl. rewrite Int64.repr_unsigned, Int64.neg_involutive. eauto.
+      split; intros. apply eval_testcond_compare_ulong; auto.
+      erewrite Val_cmplu_bool_correct; eauto.
+      destruct r; reflexivity || discriminate.
+    + exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C).
+      econstructor; split.
+      eapply exec_straight_trans. eexact A. apply exec_straight_one.
+      simpl. rewrite B, C by eauto with asmgen. eauto.
+      split; intros. apply eval_testcond_compare_ulong; auto.
+      erewrite Val_cmplu_bool_correct; eauto. 
+      transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
+  - (* Ccomplshift *)
+    econstructor; split. apply exec_straight_one. simpl; eauto.
+    split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_slong; auto. 
+    destruct r; reflexivity || discriminate.
+  - (* Ccomplushift *)
+    econstructor; split. apply exec_straight_one. simpl; eauto.
+    split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_ulong; auto.
+    erewrite Val_cmplu_bool_correct; eauto. 
+    destruct r; reflexivity || discriminate.
+  - (* Cmasklzero *)
+    destruct (is_logical_imm64 n).
+    + econstructor; split. apply exec_straight_one. simpl; eauto.
+      split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Ceq); auto.
+      destruct r; reflexivity || discriminate.
+    + exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C).
+      econstructor; split.
+      eapply exec_straight_trans. eexact A.
+      apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto.
+      split; intros. apply (eval_testcond_compare_slong Ceq); auto.
+      transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
+  - (* Cmasknotzero *)
+    destruct (is_logical_imm64 n).
+    + econstructor; split. apply exec_straight_one. simpl; eauto.
+      split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Cne); auto.
+      destruct r; reflexivity || discriminate.
+    + exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C).
+      econstructor; split.
+      eapply exec_straight_trans. eexact A.
+      apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto.
+      split; intros. apply (eval_testcond_compare_slong Cne); auto.
+      transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
+  - (* Ccompf *)
+    econstructor; split. apply exec_straight_one. simpl; eauto.
+    split; intros. apply eval_testcond_compare_float; auto.
+    destruct r; discriminate || rewrite compare_float_inv; auto.
+  - (* Cnotcompf *)
+    econstructor; split. apply exec_straight_one. simpl; eauto.
+    split; intros. apply eval_testcond_compare_not_float; auto.
+    destruct r; discriminate || rewrite compare_float_inv; auto.
+  - (* Ccompfzero *)
+    econstructor; split. apply exec_straight_one. simpl; eauto.
+    split; intros. apply eval_testcond_compare_float; auto.
+    destruct r; discriminate || rewrite compare_float_inv; auto.
+  - (* Cnotcompfzero *)
+    econstructor; split. apply exec_straight_one. simpl; eauto.
+    split; intros. apply eval_testcond_compare_not_float; auto.
+    destruct r; discriminate || rewrite compare_float_inv; auto.
+  - (* Ccompfs *)
+    econstructor; split. apply exec_straight_one. simpl; eauto.
+    split; intros. apply eval_testcond_compare_single; auto.
+    destruct r; discriminate || rewrite compare_single_inv; auto.
+  - (* Cnotcompfs *)
+    econstructor; split. apply exec_straight_one. simpl; eauto.
+    split; intros. apply eval_testcond_compare_not_single; auto.
+    destruct r; discriminate || rewrite compare_single_inv; auto.
+  - (* Ccompfszero *)
+    econstructor; split. apply exec_straight_one. simpl; eauto.
+    split; intros. apply eval_testcond_compare_single; auto.
+    destruct r; discriminate || rewrite compare_single_inv; auto.
+  - (* Cnotcompfszero *)
+    econstructor; split. apply exec_straight_one. simpl; eauto.
+    split; intros. apply eval_testcond_compare_not_single; auto.
+    destruct r; discriminate || rewrite compare_single_inv; auto.
 Qed.
 
 Lemma transl_cond_correct':
@@ -1351,90 +1351,90 @@ Local Opaque transl_cond transl_cond_branch_default.
   destruct args as [ | a1 args]; simpl in TR; auto.
   destruct args as [ | a2 args]; simpl in TR; auto.
   destruct cond; simpl in TR; auto.
-- (* Ccompimm *)
-  destruct c0; auto; destruct (Int.eq n Int.zero) eqn:N0; auto; 
-  apply Int.same_if_eq in N0; subst n; ArgsInv.
-+ (* Ccompimm Cne 0 *)
-  econstructor; split. econstructor.
-  split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV.
-  unfold incrPC. Simpl. rewrite EQRSX. simpl. auto.
-+ (* Ccompimm Ceq 0 *)
-  econstructor; split. econstructor.
-  split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. simpl.
-  unfold incrPC. Simpl. rewrite EQRSX. simpl.
-  destruct (Int.eq i Int.zero); auto.
-- (* Ccompuimm *)
-  destruct c0; auto; destruct (Int.eq n Int.zero) eqn:N0; auto.
-  apply Int.same_if_eq in N0; subst n; ArgsInv.
-+ (* Ccompuimm Cne 0 *)
-  econstructor; split. econstructor.
-  split; auto. simpl. apply Val_cmpu_bool_correct in EV.
-  unfold incrPC. Simpl. rewrite EV. auto.
-+ (* Ccompuimm Ceq 0 *)
-  monadInv TR. ArgsInv. simpl in *.
-  econstructor; split. econstructor.
-  split; auto. simpl. unfold incrPC. Simpl.
-  apply Int.same_if_eq in N0; subst.
-  rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Cne), EV.
-  destruct b; auto.
-- (* Cmaskzero *)
-  destruct (Int.is_power2 n) as [bit|] eqn:P2; auto. ArgsInv.
-  econstructor; split. econstructor.
-  split; auto. simpl.
-  erewrite <- Int.mul_pow2, Int.mul_commut, Int.mul_one by eauto.
-  unfold incrPC. Simpl.
-  rewrite (Val.negate_cmp_bool Ceq), EV. destruct b; auto.
-- (* Cmasknotzero *)
-  destruct (Int.is_power2 n) as [bit|] eqn:P2; auto. ArgsInv.
-  econstructor; split. econstructor.
-  split; auto. simpl.
-  erewrite <- Int.mul_pow2, Int.mul_commut, Int.mul_one by eauto.
-  unfold incrPC. Simpl.
-  rewrite EV. auto.
-- (* Ccomplimm *)
-  destruct c0; auto; destruct (Int64.eq n Int64.zero) eqn:N0; auto; 
-  apply Int64.same_if_eq in N0; subst n; ArgsInv.
-+ (* Ccomplimm Cne 0 *)
-  econstructor; split. econstructor.
-  split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV.
-  unfold incrPC. Simpl. rewrite EQRSX. simpl. auto.
-+ (* Ccomplimm Ceq 0 *)
-  econstructor; split. econstructor.
-  split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. simpl.
-  unfold incrPC. Simpl. rewrite EQRSX. simpl.
-  destruct (Int64.eq i Int64.zero); auto.
-- (* Ccompluimm *)
-  destruct c0; auto; destruct (Int64.eq n Int64.zero) eqn:N0; auto;
-  apply Int64.same_if_eq in N0; subst n; ArgsInv.
-+ (* Ccompluimm Cne 0 *)
-  econstructor; split. econstructor.
-  split; auto. simpl. apply Val_cmplu_bool_correct in EV.
-  unfold incrPC. Simpl. rewrite EV. auto.
-+ (* Ccompluimm Ceq 0 *)
-  econstructor; split. econstructor.
-  split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. simpl.
-  unfold incrPC. Simpl. rewrite EQRSX. simpl.
-  destruct (Int64.eq i Int64.zero); auto.
-  unfold incrPC. Simpl. rewrite EQRSX. simpl.
-  rewrite SF in *; simpl in *.
-  rewrite Int64.eq_true in *.
-  destruct ((Mem.valid_pointer m b0 (Ptrofs.unsigned i) || Mem.valid_pointer m b0 (Ptrofs.unsigned i - 1))); simpl in *.
-  assert (b = true). { destruct b; try congruence. }
-  rewrite H; auto. discriminate.
-- (* Cmasklzero *)
-  destruct (Int64.is_power2' n) as [bit|] eqn:P2; auto. ArgsInv.
-  econstructor; split. econstructor.
-  split; auto.
-  erewrite <- Int64.mul_pow2', Int64.mul_commut, Int64.mul_one by eauto.
-  unfold incrPC. Simpl.
-  rewrite (Val.negate_cmpl_bool Ceq), EV. destruct b; auto.
-- (* Cmasklnotzero *)
-  destruct (Int64.is_power2' n) as [bit|] eqn:P2; auto. ArgsInv.
-  econstructor; split. econstructor.
-  split; auto.
-  erewrite <- Int64.mul_pow2', Int64.mul_commut, Int64.mul_one by eauto.
-  unfold incrPC. Simpl.
-  rewrite EV. auto.
+  - (* Ccompimm *)
+    destruct c0; auto; destruct (Int.eq n Int.zero) eqn:N0; auto; 
+    apply Int.same_if_eq in N0; subst n; ArgsInv.
+    + (* Ccompimm Cne 0 *)
+      econstructor; split. econstructor.
+      split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV.
+      unfold incrPC. Simpl. rewrite EQRSX. simpl. auto.
+    + (* Ccompimm Ceq 0 *)
+      econstructor; split. econstructor.
+      split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. simpl.
+      unfold incrPC. Simpl. rewrite EQRSX. simpl.
+      destruct (Int.eq i Int.zero); auto.
+  - (* Ccompuimm *)
+    destruct c0; auto; destruct (Int.eq n Int.zero) eqn:N0; auto.
+    apply Int.same_if_eq in N0; subst n; ArgsInv.
+    + (* Ccompuimm Cne 0 *)
+      econstructor; split. econstructor.
+      split; auto. simpl. apply Val_cmpu_bool_correct in EV.
+      unfold incrPC. Simpl. rewrite EV. auto.
+    + (* Ccompuimm Ceq 0 *)
+      monadInv TR. ArgsInv. simpl in *.
+      econstructor; split. econstructor.
+      split; auto. simpl. unfold incrPC. Simpl.
+      apply Int.same_if_eq in N0; subst.
+      rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Cne), EV.
+      destruct b; auto.
+  - (* Cmaskzero *)
+    destruct (Int.is_power2 n) as [bit|] eqn:P2; auto. ArgsInv.
+    econstructor; split. econstructor.
+    split; auto. simpl.
+    erewrite <- Int.mul_pow2, Int.mul_commut, Int.mul_one by eauto.
+    unfold incrPC. Simpl.
+    rewrite (Val.negate_cmp_bool Ceq), EV. destruct b; auto.
+  - (* Cmasknotzero *)
+    destruct (Int.is_power2 n) as [bit|] eqn:P2; auto. ArgsInv.
+    econstructor; split. econstructor.
+    split; auto. simpl.
+    erewrite <- Int.mul_pow2, Int.mul_commut, Int.mul_one by eauto.
+    unfold incrPC. Simpl.
+    rewrite EV. auto.
+  - (* Ccomplimm *)
+    destruct c0; auto; destruct (Int64.eq n Int64.zero) eqn:N0; auto; 
+    apply Int64.same_if_eq in N0; subst n; ArgsInv.
+    + (* Ccomplimm Cne 0 *)
+      econstructor; split. econstructor.
+      split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV.
+      unfold incrPC. Simpl. rewrite EQRSX. simpl. auto.
+    + (* Ccomplimm Ceq 0 *)
+      econstructor; split. econstructor.
+      split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. simpl.
+      unfold incrPC. Simpl. rewrite EQRSX. simpl.
+      destruct (Int64.eq i Int64.zero); auto.
+  - (* Ccompluimm *)
+    destruct c0; auto; destruct (Int64.eq n Int64.zero) eqn:N0; auto;
+    apply Int64.same_if_eq in N0; subst n; ArgsInv.
+    + (* Ccompluimm Cne 0 *)
+      econstructor; split. econstructor.
+      split; auto. simpl. apply Val_cmplu_bool_correct in EV.
+      unfold incrPC. Simpl. rewrite EV. auto.
+    + (* Ccompluimm Ceq 0 *)
+      econstructor; split. econstructor.
+      split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. simpl.
+      unfold incrPC. Simpl. rewrite EQRSX. simpl.
+      destruct (Int64.eq i Int64.zero); auto.
+      unfold incrPC. Simpl. rewrite EQRSX. simpl.
+      rewrite SF in *; simpl in *.
+      rewrite Int64.eq_true in *.
+      destruct ((Mem.valid_pointer m b0 (Ptrofs.unsigned i) || Mem.valid_pointer m b0 (Ptrofs.unsigned i - 1))); simpl in *.
+      assert (b = true). { destruct b; try congruence. }
+      rewrite H; auto. discriminate.
+  - (* Cmasklzero *)
+    destruct (Int64.is_power2' n) as [bit|] eqn:P2; auto. ArgsInv.
+    econstructor; split. econstructor.
+    split; auto.
+    erewrite <- Int64.mul_pow2', Int64.mul_commut, Int64.mul_one by eauto.
+    unfold incrPC. Simpl.
+    rewrite (Val.negate_cmpl_bool Ceq), EV. destruct b; auto.
+  - (* Cmasklnotzero *)
+    destruct (Int64.is_power2' n) as [bit|] eqn:P2; auto. ArgsInv.
+    econstructor; split. econstructor.
+    split; auto.
+    erewrite <- Int64.mul_pow2', Int64.mul_commut, Int64.mul_one by eauto.
+    unfold incrPC. Simpl.
+    rewrite EV. auto.
 Qed.
 
 Lemma transl_op_correct:
@@ -1451,200 +1451,200 @@ Local Opaque Int.eq Int64.eq Val.add Val.addl Int.zwordsize Int64.zwordsize.
   intros until c; intros TR EV.
   unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl;
   try (rewrite <- transl_eval_shift; TranslOpSimpl).
-- (* move *)
-  destruct (preg_of res), (preg_of m0); try destruct d; try destruct d0; inv TR; TranslOpSimpl.
-- (* intconst *)
-  exploit exec_loadimm32. intros (rs' & A & B & C).
-  exists rs'; split. eexact A. split. rewrite B; auto. intros; auto with asmgen.
-- (* longconst *)
-  exploit exec_loadimm64. intros (rs' & A & B & C).
-  exists rs'; split. eexact A. split. rewrite B; auto. intros; auto with asmgen.
-- (* floatconst *)
-  destruct (Float.eq_dec n Float.zero).
-+ subst n. TranslOpSimpl. 
-+ TranslOpSimplN.
-- (* singleconst *)
-  destruct (Float32.eq_dec n Float32.zero).
-+ subst n. TranslOpSimpl. 
-+ TranslOpSimplN.
-- (* loadsymbol *)
-  exploit (exec_loadsymbol x id ofs). eauto with asmgen. intros (rs' & A & B & C).
-  exists rs'; split. eexact A. split. rewrite B; auto. auto.
-- (* addrstack *)
-  exploit (exec_addimm64 x XSP (Ptrofs.to_int64 ofs)); try discriminate. simpl; eauto with asmgen.
-  intros (rs' & A & B & C).
-  exists rs'; split. eexact A. split. replace (DR XSP) with (SP) in B by auto. rewrite B.
-Local Transparent Val.addl.
-  destruct (rs SP); simpl; auto. rewrite Ptrofs.of_int64_to_int64 by auto. auto.
-  auto.
-- (* shift *)
-  rewrite <- transl_eval_shift'. TranslOpSimpl.
-- (* addimm *)
-  exploit (exec_addimm32 x x0 n). eauto with asmgen. intros (rs' & A & B & C).
-  exists rs'; split. eexact A. split. rewrite B; auto. auto.
-- (* mul *)
-  TranslOpBase.
-Local Transparent Val.add.
-  destruct (rs x0); auto; destruct (rs x1); auto. simpl. rewrite Int.add_zero_l; auto.
-- (* andimm *)
-  exploit (exec_logicalimm32 (Pandimm W) (Pand W)).
-  intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
-  intros (rs' & A & B & C). 
-  exists rs'; split. eexact A. split. rewrite B; auto. auto.
-- (* orimm *)
-  exploit (exec_logicalimm32 (Porrimm W) (Porr W)). 
-  intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
-  intros (rs' & A & B & C). 
-  exists rs'; split. eexact A. split. rewrite B; auto. auto.
-- (* xorimm *)
-  exploit (exec_logicalimm32 (Peorimm W) (Peor W)). 
-  intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
-  intros (rs' & A & B & C). 
-  exists rs'; split. eexact A. split. rewrite B; auto. auto.
-- (* not *)
-  TranslOpBase.
-  destruct (rs x0); auto. simpl. rewrite Int.or_zero_l; auto. 
-- (* notshift *)
-  TranslOpBase.
-  destruct (eval_shift s (rs x0) a); auto. simpl. rewrite Int.or_zero_l; auto. 
-- (* shrx *)
-  assert (Val.maketotal (Val.shrx (rs x0) (Vint n)) = Val.maketotal (Val.shrx (rs x0) (Vint n))) by eauto.
-  destruct (Val.shrx) eqn:E.
-  + exploit (exec_shrx32 x x0 n); eauto with asmgen. intros (rs' & A & B & C).
+  - (* move *)
+    destruct (preg_of res), (preg_of m0); try destruct d; try destruct d0; inv TR; TranslOpSimpl.
+  - (* intconst *)
+    exploit exec_loadimm32. intros (rs' & A & B & C).
+    exists rs'; split. eexact A. split. rewrite B; auto. intros; auto with asmgen.
+  - (* longconst *)
+    exploit exec_loadimm64. intros (rs' & A & B & C).
+    exists rs'; split. eexact A. split. rewrite B; auto. intros; auto with asmgen.
+  - (* floatconst *)
+    destruct (Float.eq_dec n Float.zero).
+    + subst n. TranslOpSimpl. 
+    + TranslOpSimplN.
+  - (* singleconst *)
+    destruct (Float32.eq_dec n Float32.zero).
+    + subst n. TranslOpSimpl. 
+    + TranslOpSimplN.
+  - (* loadsymbol *)
+    exploit (exec_loadsymbol x id ofs). eauto with asmgen. intros (rs' & A & B & C).
+    exists rs'; split. eexact A. split. rewrite B; auto. auto.
+  - (* addrstack *)
+    exploit (exec_addimm64 x XSP (Ptrofs.to_int64 ofs)); try discriminate. simpl; eauto with asmgen.
+    intros (rs' & A & B & C).
+    exists rs'; split. eexact A. split. replace (DR XSP) with (SP) in B by auto. rewrite B.
+  Local Transparent Val.addl.
+    destruct (rs SP); simpl; auto. rewrite Ptrofs.of_int64_to_int64 by auto. auto.
+    auto.
+  - (* shift *)
+    rewrite <- transl_eval_shift'. TranslOpSimpl.
+  - (* addimm *)
+    exploit (exec_addimm32 x x0 n). eauto with asmgen. intros (rs' & A & B & C).
+    exists rs'; split. eexact A. split. rewrite B; auto. auto.
+  - (* mul *)
+    TranslOpBase.
+  Local Transparent Val.add.
+    destruct (rs x0); auto; destruct (rs x1); auto. simpl. rewrite Int.add_zero_l; auto.
+  - (* andimm *)
+    exploit (exec_logicalimm32 (Pandimm W) (Pand W)).
+    intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
+    intros (rs' & A & B & C). 
+    exists rs'; split. eexact A. split. rewrite B; auto. auto.
+  - (* orimm *)
+    exploit (exec_logicalimm32 (Porrimm W) (Porr W)). 
+    intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
+    intros (rs' & A & B & C). 
+    exists rs'; split. eexact A. split. rewrite B; auto. auto.
+  - (* xorimm *)
+    exploit (exec_logicalimm32 (Peorimm W) (Peor W)). 
+    intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
+    intros (rs' & A & B & C). 
+    exists rs'; split. eexact A. split. rewrite B; auto. auto.
+  - (* not *)
+    TranslOpBase.
+    destruct (rs x0); auto. simpl. rewrite Int.or_zero_l; auto. 
+  - (* notshift *)
+    TranslOpBase.
+    destruct (eval_shift s (rs x0) a); auto. simpl. rewrite Int.or_zero_l; auto. 
+  - (* shrx *)
+    assert (Val.maketotal (Val.shrx (rs x0) (Vint n)) = Val.maketotal (Val.shrx (rs x0) (Vint n))) by eauto.
+    destruct (Val.shrx) eqn:E.
+    + exploit (exec_shrx32 x x0 n); eauto with asmgen. intros (rs' & A & B & C).
+      econstructor; split. eexact A. split. rewrite B; auto. auto.
+    + exploit (exec_shrx32_none x x0 n); eauto with asmgen.
+  - (* zero-ext *)
+    TranslOpBase.
+    destruct (rs x0); auto; simpl. rewrite Int.shl_zero. auto.
+  - (* sign-ext *)
+    TranslOpBase.
+    destruct (rs x0); auto; simpl. rewrite Int.shl_zero. auto.
+  - (* shlzext *)
+    TranslOpBase.
+    destruct (rs x0); simpl; auto. rewrite <- Int.shl_zero_ext_min; auto using a32_range.
+  - (* shlsext *)
+    TranslOpBase.
+    destruct (rs x0); simpl; auto. rewrite <- Int.shl_sign_ext_min; auto using a32_range.
+  - (* zextshr *)
+    TranslOpBase.
+    destruct (rs x0); simpl; auto. rewrite ! a32_range; simpl. rewrite <- Int.zero_ext_shru_min; auto using a32_range.
+  - (* sextshr *)
+    TranslOpBase.
+    destruct (rs x0); simpl; auto. rewrite ! a32_range; simpl. rewrite <- Int.sign_ext_shr_min; auto using a32_range.
+  - (* shiftl *)
+    rewrite <- transl_eval_shiftl'. TranslOpSimpl.
+  - (* extend *)
+    exploit (exec_move_extended x0 x1 x a k). intros (rs' & A & B & C).
+    econstructor; split. eexact A. 
+    split. rewrite B; auto. eauto with asmgen.
+  - (* addlshift *)
+    TranslOpBase.
+  - (* addext *)
+    exploit (exec_arith_extended Val.addl Paddext (Padd X)).
+    auto. auto. instantiate (1 := x1). eauto with asmgen. intros (rs' & A & B & C).
     econstructor; split. eexact A. split. rewrite B; auto. auto.
-  + exploit (exec_shrx32_none x x0 n); eauto with asmgen.
-- (* zero-ext *)
-  TranslOpBase.
-  destruct (rs x0); auto; simpl. rewrite Int.shl_zero. auto.
-- (* sign-ext *)
-  TranslOpBase.
-  destruct (rs x0); auto; simpl. rewrite Int.shl_zero. auto.
-- (* shlzext *)
-  TranslOpBase.
-  destruct (rs x0); simpl; auto. rewrite <- Int.shl_zero_ext_min; auto using a32_range.
-- (* shlsext *)
-  TranslOpBase.
-  destruct (rs x0); simpl; auto. rewrite <- Int.shl_sign_ext_min; auto using a32_range.
-- (* zextshr *)
-  TranslOpBase.
-  destruct (rs x0); simpl; auto. rewrite ! a32_range; simpl. rewrite <- Int.zero_ext_shru_min; auto using a32_range.
-- (* sextshr *)
-  TranslOpBase.
-  destruct (rs x0); simpl; auto. rewrite ! a32_range; simpl. rewrite <- Int.sign_ext_shr_min; auto using a32_range.
-- (* shiftl *)
-  rewrite <- transl_eval_shiftl'. TranslOpSimpl.
-- (* extend *)
-  exploit (exec_move_extended x0 x1 x a k). intros (rs' & A & B & C).
-  econstructor; split. eexact A. 
-  split. rewrite B; auto. eauto with asmgen.
-- (* addlshift *)
-  TranslOpBase.
-- (* addext *)
-  exploit (exec_arith_extended Val.addl Paddext (Padd X)).
-  auto. auto. instantiate (1 := x1). eauto with asmgen. intros (rs' & A & B & C).
-  econstructor; split. eexact A. split. rewrite B; auto. auto.
-- (* addlimm *)
-  exploit (exec_addimm64 x x0 n). simpl. generalize (ireg_of_not_X16 _ _ EQ1). congruence.
-  intros (rs' & A & B & C).
-  exists rs'; split. eexact A. split. simpl in B; rewrite B; auto. auto.
-- (* neglshift *)
-  TranslOpBase.
-- (* sublshift *)
-  TranslOpBase.
-- (* subext *)
-  exploit (exec_arith_extended Val.subl Psubext (Psub X)).
-  auto. auto. instantiate (1 := x1). eauto with asmgen. intros (rs' & A & B & C).
-  econstructor; split. eexact A. split. rewrite B; auto. auto.
-- (* mull *)
-  TranslOpBase.
-  destruct (rs x0); auto; destruct (rs x1); auto. simpl. rewrite Int64.add_zero_l; auto.
-- (* andlshift *)
-  TranslOpBase.
-- (* andlimm *)
-  exploit (exec_logicalimm64 (Pandimm X) (Pand X)). 
-  intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
-  intros (rs' & A & B & C). 
-  exists rs'; split. eexact A. split. rewrite B; auto. auto.
-- (* orlshift *)
-  TranslOpBase.
-- (* orlimm *)
-  exploit (exec_logicalimm64 (Porrimm X) (Porr X)). 
-  intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
-  intros (rs' & A & B & C). 
-  exists rs'; split. eexact A. split. rewrite B; auto. auto.
-- (* orlshift *)
-  TranslOpBase.
-- (* xorlimm *)
-  exploit (exec_logicalimm64 (Peorimm X) (Peor X)). 
-  intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
-  intros (rs' & A & B & C). 
-  exists rs'; split. eexact A. split. rewrite B; auto. auto.
-- (* notl *)
-  TranslOpBase.
-  destruct (rs x0); auto. simpl. rewrite Int64.or_zero_l; auto.
-- (* notlshift *)
-  TranslOpBase.
-  destruct (eval_shiftl s (rs x0) a); auto. simpl. rewrite Int64.or_zero_l; auto.
-- (* biclshift *)
-  TranslOpBase.
-- (* ornlshift *)
-  TranslOpBase.
-- (* eqvlshift *)
-  TranslOpBase.
-- (* shrx *)
-  assert (Val.maketotal (Val.shrxl (rs x0) (Vint n)) = Val.maketotal (Val.shrxl (rs x0) (Vint n))) by eauto.
-  destruct (Val.shrxl) eqn:E.
-  + exploit (exec_shrx64 x x0 n); eauto with asmgen. intros (rs' & A & B & C).
+  - (* addlimm *)
+    exploit (exec_addimm64 x x0 n). simpl. generalize (ireg_of_not_X16 _ _ EQ1). congruence.
+    intros (rs' & A & B & C).
+    exists rs'; split. eexact A. split. simpl in B; rewrite B; auto. auto.
+  - (* neglshift *)
+    TranslOpBase.
+  - (* sublshift *)
+    TranslOpBase.
+  - (* subext *)
+    exploit (exec_arith_extended Val.subl Psubext (Psub X)).
+    auto. auto. instantiate (1 := x1). eauto with asmgen. intros (rs' & A & B & C).
     econstructor; split. eexact A. split. rewrite B; auto. auto.
-  + exploit (exec_shrx64_none x x0 n); eauto with asmgen.
-- (* zero-ext-l *)
-  TranslOpBase.
-  destruct (rs x0); auto; simpl. rewrite Int64.shl'_zero. auto.
-- (* sign-ext-l *)
-  TranslOpBase.
-  destruct (rs x0); auto; simpl. rewrite Int64.shl'_zero. auto.
-- (* shllzext *)
-  TranslOpBase.
-  destruct (rs x0); simpl; auto. rewrite <- Int64.shl'_zero_ext_min; auto using a64_range.
-- (* shllsext *)
-  TranslOpBase.
-  destruct (rs x0); simpl; auto. rewrite <- Int64.shl'_sign_ext_min; auto using a64_range.
-- (* zextshrl *)
-  TranslOpBase.
-  destruct (rs x0); simpl; auto. rewrite ! a64_range; simpl. rewrite <- Int64.zero_ext_shru'_min; auto using a64_range.
-- (* sextshrl *)
-  TranslOpBase.
-  destruct (rs x0); simpl; auto. rewrite ! a64_range; simpl. rewrite <- Int64.sign_ext_shr'_min; auto using a64_range.
-- (* condition *)
-  exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C).
-  econstructor; split.
-  eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto.
-  split. Simpl. destruct (eval_condition cond (map rs (map preg_of args)) m) as [b|]; simpl in *.
-  rewrite (B b) by auto. auto. 
-  auto.
-  intros; Simpl.
-- (* select *)
-  destruct (preg_of res) as [[ir|fr]|cr|] eqn:RES; monadInv TR.
-  + (* integer *)
-    generalize (ireg_of_eq _ _ EQ) (ireg_of_eq _ _ EQ1); intros E1 E2; rewrite E1, E2.
+  - (* mull *)
+    TranslOpBase.
+    destruct (rs x0); auto; destruct (rs x1); auto. simpl. rewrite Int64.add_zero_l; auto.
+  - (* andlshift *)
+    TranslOpBase.
+  - (* andlimm *)
+    exploit (exec_logicalimm64 (Pandimm X) (Pand X)). 
+    intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
+    intros (rs' & A & B & C). 
+    exists rs'; split. eexact A. split. rewrite B; auto. auto.
+  - (* orlshift *)
+    TranslOpBase.
+  - (* orlimm *)
+    exploit (exec_logicalimm64 (Porrimm X) (Porr X)). 
+    intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
+    intros (rs' & A & B & C). 
+    exists rs'; split. eexact A. split. rewrite B; auto. auto.
+  - (* orlshift *)
+    TranslOpBase.
+  - (* xorlimm *)
+    exploit (exec_logicalimm64 (Peorimm X) (Peor X)). 
+    intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen.
+    intros (rs' & A & B & C). 
+    exists rs'; split. eexact A. split. rewrite B; auto. auto.
+  - (* notl *)
+    TranslOpBase.
+    destruct (rs x0); auto. simpl. rewrite Int64.or_zero_l; auto.
+  - (* notlshift *)
+    TranslOpBase.
+    destruct (eval_shiftl s (rs x0) a); auto. simpl. rewrite Int64.or_zero_l; auto.
+  - (* biclshift *)
+    TranslOpBase.
+  - (* ornlshift *)
+    TranslOpBase.
+  - (* eqvlshift *)
+    TranslOpBase.
+  - (* shrx *)
+    assert (Val.maketotal (Val.shrxl (rs x0) (Vint n)) = Val.maketotal (Val.shrxl (rs x0) (Vint n))) by eauto.
+    destruct (Val.shrxl) eqn:E.
+    + exploit (exec_shrx64 x x0 n); eauto with asmgen. intros (rs' & A & B & C).
+      econstructor; split. eexact A. split. rewrite B; auto. auto.
+    + exploit (exec_shrx64_none x x0 n); eauto with asmgen.
+  - (* zero-ext-l *)
+    TranslOpBase.
+    destruct (rs x0); auto; simpl. rewrite Int64.shl'_zero. auto.
+  - (* sign-ext-l *)
+    TranslOpBase.
+    destruct (rs x0); auto; simpl. rewrite Int64.shl'_zero. auto.
+  - (* shllzext *)
+    TranslOpBase.
+    destruct (rs x0); simpl; auto. rewrite <- Int64.shl'_zero_ext_min; auto using a64_range.
+  - (* shllsext *)
+    TranslOpBase.
+    destruct (rs x0); simpl; auto. rewrite <- Int64.shl'_sign_ext_min; auto using a64_range.
+  - (* zextshrl *)
+    TranslOpBase.
+    destruct (rs x0); simpl; auto. rewrite ! a64_range; simpl. rewrite <- Int64.zero_ext_shru'_min; auto using a64_range.
+  - (* sextshrl *)
+    TranslOpBase.
+    destruct (rs x0); simpl; auto. rewrite ! a64_range; simpl. rewrite <- Int64.sign_ext_shr'_min; auto using a64_range.
+  - (* condition *)
     exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C).
     econstructor; split.
-    eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto.
+    eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto.
     split. Simpl. destruct (eval_condition cond (map rs (map preg_of args)) m) as [b|]; simpl in *.
-    rewrite (B b) by auto. rewrite !C. apply Val.lessdef_normalize.
-    rewrite <- E2; auto with asmgen. rewrite <- E1; auto with asmgen.
-    auto.
-    intros; Simpl.
-  + (* FP *)
-    generalize (freg_of_eq _ _ EQ) (freg_of_eq _ _ EQ1); intros E1 E2; rewrite E1, E2.
-    exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C).
-    econstructor; split.
-    eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto.
-    split. Simpl. destruct (eval_condition cond (map rs (map preg_of args)) m) as [b|]; simpl in *.
-    rewrite (B b) by auto. rewrite !C. apply Val.lessdef_normalize.
-    rewrite <- E2; auto with asmgen. rewrite <- E1; auto with asmgen.
+    rewrite (B b) by auto. auto. 
     auto.
     intros; Simpl.
+  - (* select *)
+    destruct (preg_of res) as [[ir|fr]|cr|] eqn:RES; monadInv TR.
+    + (* integer *)
+      generalize (ireg_of_eq _ _ EQ) (ireg_of_eq _ _ EQ1); intros E1 E2; rewrite E1, E2.
+      exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C).
+      econstructor; split.
+      eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto.
+      split. Simpl. destruct (eval_condition cond (map rs (map preg_of args)) m) as [b|]; simpl in *.
+      rewrite (B b) by auto. rewrite !C. apply Val.lessdef_normalize.
+      rewrite <- E2; auto with asmgen. rewrite <- E1; auto with asmgen.
+      auto.
+      intros; Simpl.
+    + (* FP *)
+      generalize (freg_of_eq _ _ EQ) (freg_of_eq _ _ EQ1); intros E1 E2; rewrite E1, E2.
+      exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C).
+      econstructor; split.
+      eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto.
+      split. Simpl. destruct (eval_condition cond (map rs (map preg_of args)) m) as [b|]; simpl in *.
+      rewrite (B b) by auto. rewrite !C. apply Val.lessdef_normalize.
+      rewrite <- E2; auto with asmgen. rewrite <- E1; auto with asmgen.
+      auto.
+      intros; Simpl.
 Qed.
 
 (** Translation of addressing modes, loads, stores *)
@@ -1660,68 +1660,68 @@ Lemma transl_addressing_correct:
 Proof.
   intros until o; intros TR EV.
   unfold transl_addressing in TR; destruct addr; ArgsInv; SimplEval EV.
-- (* Aindexed *)
-  destruct (offset_representable sz ofs); inv EQ0.
-+ econstructor; econstructor; split. apply exec_straight_opt_refl.
-  auto.
-+ exploit (exec_loadimm64 X16 ofs). intros (rs' & A & B & C).
-  econstructor; exists rs'; split. apply exec_straight_opt_intro; eexact A.
-  split. simpl. rewrite B, C by eauto with asmgen. auto.
-  eauto with asmgen.
-- (* Aindexed2 *)
-  econstructor; econstructor; split. apply exec_straight_opt_refl.
-  auto.
-- (* Aindexed2shift *)
-  destruct (Int.eq a Int.zero) eqn:E; [|destruct (Int.eq (Int.shl Int.one a) (Int.repr sz))]; inv EQ2.
-+ apply Int.same_if_eq in E. rewrite E.
-  econstructor; econstructor; split. apply exec_straight_opt_refl.
-  split; auto. simpl.
-  rewrite Val.addl_commut in H0. destruct (rs x0); try discriminate.
-  unfold Val.shll. rewrite Int64.shl'_zero. auto.
-+ econstructor; econstructor; split. apply exec_straight_opt_refl.
-  auto. 
-+ econstructor; econstructor; split.
-  apply exec_straight_opt_intro. apply exec_straight_one. simpl; eauto.
-  split. simpl. Simpl. rewrite H0. simpl. rewrite Ptrofs.add_zero. auto.
-  intros; Simpl.
-- (* Aindexed2ext *)
-  destruct (Int.eq a Int.zero || Int.eq (Int.shl Int.one a) (Int.repr sz)); inv EQ2.
-+ econstructor; econstructor; split. apply exec_straight_opt_refl.
-  split; auto. destruct x; auto.
-+ exploit (exec_arith_extended Val.addl Paddext (Padd X)); auto.
-  instantiate (1 := x0). eauto with asmgen.
-  intros (rs' & A & B & C).
-  econstructor; exists rs'; split.
-  apply exec_straight_opt_intro. eexact A. 
-  split. simpl. rewrite B. rewrite Val.addl_assoc. f_equal.
-  unfold Op.eval_extend; destruct x, (rs x1); simpl; auto; rewrite ! a64_range;
-  simpl; rewrite Int64.add_zero; auto.
-  intros. apply C; eauto with asmgen.
-- (* Aglobal *)
-  destruct (Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz); inv TR.
-+ econstructor; econstructor; split.
-  apply exec_straight_opt_intro. apply exec_straight_one. simpl; eauto.
-  split. simpl. Simpl. rewrite symbol_high_low. simpl in EV. congruence.
-  intros; Simpl.
-+ exploit (exec_loadsymbol X16 id ofs). auto. intros (rs' & A & B & C).
-  econstructor; exists rs'; split.
-  apply exec_straight_opt_intro. eexact A.
-  split. simpl. 
-  rewrite B. rewrite <- Genv.shift_symbol_address_64, Ptrofs.add_zero by auto. 
-  simpl in EV. congruence. 
-  auto with asmgen.
-- (* Ainstrack *)
-  assert (E: Val.addl (rs SP) (Vlong (Ptrofs.to_int64 ofs)) = Vptr b o).
-  { simpl in EV. inv EV. destruct (rs SP); simpl in H1; inv H1. simpl. 
-    rewrite Ptrofs.of_int64_to_int64 by auto. auto. }   
-  destruct (offset_representable sz (Ptrofs.to_int64 ofs)); inv TR.
-+ econstructor; econstructor; split. apply exec_straight_opt_refl.
-  auto.
-+ exploit (exec_loadimm64 X16 (Ptrofs.to_int64 ofs)). intros (rs' & A & B & C).
-  econstructor; exists rs'; split.
-  apply exec_straight_opt_intro. eexact A.
-  split. simpl. rewrite B, C by eauto with asmgen. auto.
-  auto with asmgen.
+  - (* Aindexed *)
+    destruct (offset_representable sz ofs); inv EQ0.
+    + econstructor; econstructor; split. apply exec_straight_opt_refl.
+      auto.
+    + exploit (exec_loadimm64 X16 ofs). intros (rs' & A & B & C).
+      econstructor; exists rs'; split. apply exec_straight_opt_intro; eexact A.
+      split. simpl. rewrite B, C by eauto with asmgen. auto.
+      eauto with asmgen.
+  - (* Aindexed2 *)
+    econstructor; econstructor; split. apply exec_straight_opt_refl.
+    auto.
+  - (* Aindexed2shift *)
+    destruct (Int.eq a Int.zero) eqn:E; [|destruct (Int.eq (Int.shl Int.one a) (Int.repr sz))]; inv EQ2.
+    + apply Int.same_if_eq in E. rewrite E.
+      econstructor; econstructor; split. apply exec_straight_opt_refl.
+      split; auto. simpl.
+      rewrite Val.addl_commut in H0. destruct (rs x0); try discriminate.
+      unfold Val.shll. rewrite Int64.shl'_zero. auto.
+    + econstructor; econstructor; split. apply exec_straight_opt_refl.
+      auto. 
+    + econstructor; econstructor; split.
+      apply exec_straight_opt_intro. apply exec_straight_one. simpl; eauto.
+      split. simpl. Simpl. rewrite H0. simpl. rewrite Ptrofs.add_zero. auto.
+      intros; Simpl.
+  - (* Aindexed2ext *)
+    destruct (Int.eq a Int.zero || Int.eq (Int.shl Int.one a) (Int.repr sz)); inv EQ2.
+    + econstructor; econstructor; split. apply exec_straight_opt_refl.
+      split; auto. destruct x; auto.
+    + exploit (exec_arith_extended Val.addl Paddext (Padd X)); auto.
+      instantiate (1 := x0). eauto with asmgen.
+      intros (rs' & A & B & C).
+      econstructor; exists rs'; split.
+      apply exec_straight_opt_intro. eexact A. 
+      split. simpl. rewrite B. rewrite Val.addl_assoc. f_equal.
+      unfold Op.eval_extend; destruct x, (rs x1); simpl; auto; rewrite ! a64_range;
+      simpl; rewrite Int64.add_zero; auto.
+      intros. apply C; eauto with asmgen.
+  - (* Aglobal *)
+    destruct (Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz); inv TR.
+    + econstructor; econstructor; split.
+      apply exec_straight_opt_intro. apply exec_straight_one. simpl; eauto.
+      split. simpl. Simpl. rewrite symbol_high_low. simpl in EV. congruence.
+      intros; Simpl.
+    + exploit (exec_loadsymbol X16 id ofs). auto. intros (rs' & A & B & C).
+      econstructor; exists rs'; split.
+      apply exec_straight_opt_intro. eexact A.
+      split. simpl. 
+      rewrite B. rewrite <- Genv.shift_symbol_address_64, Ptrofs.add_zero by auto. 
+      simpl in EV. congruence. 
+      auto with asmgen.
+  - (* Ainstrack *)
+    assert (E: Val.addl (rs SP) (Vlong (Ptrofs.to_int64 ofs)) = Vptr b o).
+    { simpl in EV. inv EV. destruct (rs SP); simpl in H1; inv H1. simpl. 
+      rewrite Ptrofs.of_int64_to_int64 by auto. auto. }   
+    destruct (offset_representable sz (Ptrofs.to_int64 ofs)); inv TR.
+    + econstructor; econstructor; split. apply exec_straight_opt_refl.
+      auto.
+    + exploit (exec_loadimm64 X16 (Ptrofs.to_int64 ofs)). intros (rs' & A & B & C).
+      econstructor; exists rs'; split.
+      apply exec_straight_opt_intro. eexact A.
+      split. simpl. rewrite B, C by eauto with asmgen. auto.
+      auto with asmgen.
 Qed.
 
 Lemma transl_load_correct:
@@ -1806,11 +1806,11 @@ Proof.
   assert (Val.addl rs#base (Vlong (Ptrofs.to_int64 ofs)) = Vptr b i).
   { destruct (rs base); try discriminate. simpl in *. rewrite Ptrofs.of_int64_to_int64 by auto. auto. }
   destruct offset_representable.
-- econstructor; econstructor; split. apply exec_straight_opt_refl. auto. 
-- exploit (exec_loadimm64 X16); eauto. intros (rs' & A & B & C).
-  econstructor; econstructor; split. apply exec_straight_opt_intro; eexact A.
-  split. simpl. rewrite B, C; eauto; try discriminate.
-  unfold preg_of_iregsp in H. destruct base; auto. auto.
+  - econstructor; econstructor; split. apply exec_straight_opt_refl. auto. 
+  - exploit (exec_loadimm64 X16); eauto. intros (rs' & A & B & C).
+    econstructor; econstructor; split. apply exec_straight_opt_intro; eexact A.
+    split. simpl. rewrite B, C; eauto; try discriminate.
+    unfold preg_of_iregsp in H. destruct base; auto. auto.
 Qed.
 
 Lemma loadptr_correct: forall (base: iregsp) ofs dst k m v (rs: regset),
@@ -1952,4 +1952,4 @@ Proof.
   intros. Simpl.
 Qed.
 
-End CONSTRUCTORS.
\ No newline at end of file
+End CONSTRUCTORS.
-- 
cgit