Removing expansions from Asmgen

5 files changed, 43 insertions, 1401 deletions

diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml
index c5cd6817..3f9d3359 100644
--- a/riscV/Asmexpand.ml
+++ b/riscV/Asmexpand.ml
@@ -23,6 +23,7 @@ open Asm
 open Asmexpandaux
 open AST
 open Camlcoq
+open Asmgen
 open! Integers
 
 exception Error of string
@@ -44,11 +45,13 @@ let align n a = (n + a - 1) land (-a)
 (* Emit instruction sequences that set or offset a register by a constant. *)
 
 let expand_loadimm32 dst n =
-  List.iter emit (Asmgen.loadimm32 dst n [])
+  match make_immed32 n with
+  | Imm32_single imm -> emit (Paddiw (dst, X0, imm))
+  | Imm32_pair (hi, lo) -> List.iter emit (load_hilo32 dst hi lo [])
 let expand_addptrofs dst src n =
-  List.iter emit (Asmgen.addptrofs dst src n [])
+  List.iter emit (addptrofs dst src n [])
 let expand_storeind_ptr src base ofs =
-  List.iter emit (Asmgen.storeind_ptr src base ofs [])
+  List.iter emit (storeind_ptr src base ofs [])
 
 (* Built-ins.  They come in two flavors:
    - annotation statements: take their arguments in registers or stack
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index 3e84e950..da6c0101 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -86,12 +86,6 @@ Definition make_immed64 (val: int64) :=
 Definition load_hilo32 (r: ireg) (hi lo: int) k :=
   if Int.eq lo Int.zero then Pluiw r hi :: k
   else Pluiw r hi :: Paddiw r r lo :: k.
-  
-Definition loadimm32 (r: ireg) (n: int) (k: code) :=
-  match make_immed32 n with
-  | Imm32_single imm => Paddiw r X0 imm :: k
-  | Imm32_pair hi lo => load_hilo32 r hi lo k
-  end.
 
 Definition opimm32 (op: ireg -> ireg0 -> ireg0 -> instruction)
                    (opimm: ireg -> ireg0 -> int -> instruction)
@@ -102,23 +96,11 @@ Definition opimm32 (op: ireg -> ireg0 -> ireg0 -> instruction)
   end.
 
 Definition addimm32 := opimm32 Paddw Paddiw.
-Definition andimm32 := opimm32 Pandw Pandiw.
-Definition orimm32  := opimm32 Porw  Poriw.
-Definition xorimm32 := opimm32 Pxorw Pxoriw.
-Definition sltimm32 := opimm32 Psltw Psltiw.
-Definition sltuimm32 := opimm32 Psltuw Psltiuw.
   
 Definition load_hilo64 (r: ireg) (hi lo: int64) k :=
   if Int64.eq lo Int64.zero then Pluil r hi :: k
   else Pluil r hi :: Paddil r r lo :: k.
 
-Definition loadimm64 (r: ireg) (n: int64) (k: code) :=
-  match make_immed64 n with
-  | Imm64_single imm => Paddil r X0 imm :: k
-  | Imm64_pair hi lo => load_hilo64 r hi lo k
-  | Imm64_large imm  => Ploadli r imm :: k
-  end.
-
 Definition opimm64 (op: ireg -> ireg0 -> ireg0 -> instruction)
                    (opimm: ireg -> ireg0 -> int64 -> instruction)
                    (rd rs: ireg) (n: int64) (k: code) :=
@@ -129,11 +111,6 @@ Definition opimm64 (op: ireg -> ireg0 -> ireg0 -> instruction)
   end.
 
 Definition addimm64 := opimm64 Paddl Paddil.
-Definition andimm64 := opimm64 Pandl Pandil.
-Definition orimm64  := opimm64 Porl  Poril.
-Definition xorimm64 := opimm64 Pxorl  Pxoril.
-Definition sltimm64 := opimm64 Psltl Psltil.
-Definition sltuimm64 := opimm64 Psltul Psltiul.
 
 Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
   if Ptrofs.eq_dec n Ptrofs.zero then
@@ -143,68 +120,6 @@ Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
     then addimm64 rd rs (Ptrofs.to_int64 n) k
     else addimm32 rd rs (Ptrofs.to_int n) k.
   
-(** Translation of conditional branches. *)
-
-Definition transl_cbranch_int32s (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
-  match cmp with
-  | Ceq => Pbeqw r1 r2 lbl
-  | Cne => Pbnew r1 r2 lbl
-  | Clt => Pbltw r1 r2 lbl
-  | Cle => Pbgew r2 r1 lbl
-  | Cgt => Pbltw r2 r1 lbl
-  | Cge => Pbgew r1 r2 lbl
-  end.
-
-Definition transl_cbranch_int32u (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
-  match cmp with
-  | Ceq => Pbeqw  r1 r2 lbl
-  | Cne => Pbnew  r1 r2 lbl
-  | Clt => Pbltuw r1 r2 lbl
-  | Cle => Pbgeuw r2 r1 lbl
-  | Cgt => Pbltuw r2 r1 lbl
-  | Cge => Pbgeuw r1 r2 lbl
-  end.
-
-Definition transl_cbranch_int64s (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
-  match cmp with
-  | Ceq => Pbeql r1 r2 lbl
-  | Cne => Pbnel r1 r2 lbl
-  | Clt => Pbltl r1 r2 lbl
-  | Cle => Pbgel r2 r1 lbl
-  | Cgt => Pbltl r2 r1 lbl
-  | Cge => Pbgel r1 r2 lbl
-  end.
-
-Definition transl_cbranch_int64u (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
-  match cmp with
-  | Ceq => Pbeql  r1 r2 lbl
-  | Cne => Pbnel  r1 r2 lbl
-  | Clt => Pbltul r1 r2 lbl
-  | Cle => Pbgeul r2 r1 lbl
-  | Cgt => Pbltul r2 r1 lbl
-  | Cge => Pbgeul r1 r2 lbl
-  end.
-
-Definition transl_cond_float (cmp: comparison) (rd: ireg) (fs1 fs2: freg) :=
-  match cmp with
-  | Ceq => (Pfeqd rd fs1 fs2, true)
-  | Cne => (Pfeqd rd fs1 fs2, false)
-  | Clt => (Pfltd rd fs1 fs2, true)
-  | Cle => (Pfled rd fs1 fs2, true)
-  | Cgt => (Pfltd rd fs2 fs1, true)
-  | Cge => (Pfled rd fs2 fs1, true)
-  end.
-  
-Definition transl_cond_single (cmp: comparison) (rd: ireg) (fs1 fs2: freg) :=
-  match cmp with
-  | Ceq => (Pfeqs rd fs1 fs2, true)
-  | Cne => (Pfeqs rd fs1 fs2, false)
-  | Clt => (Pflts rd fs1 fs2, true)
-  | Cle => (Pfles rd fs1 fs2, true)
-  | Cgt => (Pflts rd fs2 fs1, true)
-  | Cge => (Pfles rd fs2 fs1, true)
-   end.
-
 (** Functions to select a special register according to the op "oreg" argument from RTL *)
 
 Definition apply_bin_oreg_ireg0 (optR: option oreg) (r1 r2: ireg0): (ireg0 * ireg0) :=
@@ -223,59 +138,6 @@ Definition get_oreg (optR: option oreg) (r: ireg0) :=
 Definition transl_cbranch
            (cond: condition) (args: list mreg) (lbl: label) (k: code) :=
   match cond, args with
-  | Ccomp c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cbranch_int32s c r1 r2 lbl :: k)
-  | Ccompu c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cbranch_int32u c r1 r2 lbl :: k)
-  | Ccompimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (if Int.eq n Int.zero then
-            transl_cbranch_int32s c r1 X0 lbl :: k
-          else
-            loadimm32 X31 n (transl_cbranch_int32s c r1 X31 lbl :: k))
-  | Ccompuimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (if Int.eq n Int.zero then
-            transl_cbranch_int32u c r1 X0 lbl :: k
-          else
-            loadimm32 X31 n (transl_cbranch_int32u c r1 X31 lbl :: k))
-  | Ccompl c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cbranch_int64s c r1 r2 lbl :: k)
-  | Ccomplu c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cbranch_int64u c r1 r2 lbl :: k)
-  | Ccomplimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (if Int64.eq n Int64.zero then
-            transl_cbranch_int64s c r1 X0 lbl :: k
-          else
-            loadimm64 X31 n (transl_cbranch_int64s c r1 X31 lbl :: k))
-  | Ccompluimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (if Int64.eq n Int64.zero then
-            transl_cbranch_int64u c r1 X0 lbl :: k
-          else
-            loadimm64 X31 n (transl_cbranch_int64u c r1 X31 lbl :: k))
-  | Ccompf c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_float c X31 r1 r2 in
-      OK (insn :: (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) :: k)
-  | Cnotcompf c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_float c X31 r1 r2 in
-      OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k)
-  | Ccompfs c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_single c X31 r1 r2 in
-      OK (insn :: (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) :: k)
-  | Cnotcompfs c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_single c X31 r1 r2 in
-   OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k)
-
   | CEbeqw optR, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2;
       let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
@@ -344,133 +206,6 @@ Definition transl_cbranch
       Error(msg "Asmgen.transl_cond_branch")
   end.
 
-(** Translation of a condition operator.  The generated code sets the
-  [rd] target register to 0 or 1 depending on the truth value of the
-  condition. *)
-
-Definition transl_cond_int32s (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) :=
-  match cmp with
-  | Ceq => Pseqw rd r1 r2 :: k
-  | Cne => Psnew rd r1 r2 :: k
-  | Clt => Psltw rd r1 r2 :: k
-  | Cle => Psltw rd r2 r1 :: Pxoriw rd rd Int.one :: k
-  | Cgt => Psltw rd r2 r1 :: k
-  | Cge => Psltw rd r1 r2 :: Pxoriw rd rd Int.one :: k
-  end.
-
-Definition transl_cond_int32u (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) :=
-  match cmp with
-  | Ceq => Pseqw rd r1 r2 :: k
-  | Cne => Psnew rd r1 r2 :: k
-  | Clt => Psltuw rd r1 r2 :: k
-  | Cle => Psltuw rd r2 r1 :: Pxoriw rd rd Int.one :: k
-  | Cgt => Psltuw rd r2 r1 :: k
-  | Cge => Psltuw rd r1 r2 :: Pxoriw rd rd Int.one :: k
-  end.
-
-Definition transl_cond_int64s (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) :=
-  match cmp with
-  | Ceq => Pseql rd r1 r2 :: k
-  | Cne => Psnel rd r1 r2 :: k
-  | Clt => Psltl rd r1 r2 :: k
-  | Cle => Psltl rd r2 r1 :: Pxoriw rd rd Int.one :: k
-  | Cgt => Psltl rd r2 r1 :: k
-  | Cge => Psltl rd r1 r2 :: Pxoriw rd rd Int.one :: k
-  end.
-
-Definition transl_cond_int64u (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) :=
-  match cmp with
-  | Ceq => Pseql rd r1 r2 :: k
-  | Cne => Psnel rd r1 r2 :: k
-  | Clt => Psltul rd r1 r2 :: k
-  | Cle => Psltul rd r2 r1 :: Pxoriw rd rd Int.one :: k
-  | Cgt => Psltul rd r2 r1 :: k
-  | Cge => Psltul rd r1 r2 :: Pxoriw rd rd Int.one :: k
-  end.
-
-Definition transl_condimm_int32s (cmp: comparison) (rd: ireg) (r1: ireg) (n: int) (k: code) :=
-  if Int.eq n Int.zero then transl_cond_int32s cmp rd r1 X0 k else
-  match cmp with
-  | Ceq | Cne => xorimm32 rd r1 n (transl_cond_int32s cmp rd rd X0 k)
-  | Clt => sltimm32 rd r1 n k
-  | Cle => if Int.eq n (Int.repr Int.max_signed)
-           then loadimm32 rd Int.one k
-           else sltimm32 rd r1 (Int.add n Int.one) k
-  | _   => loadimm32 X31 n (transl_cond_int32s cmp rd r1 X31 k)
-  end.
-
-Definition transl_condimm_int32u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int) (k: code) :=
-  if Int.eq n Int.zero then transl_cond_int32u cmp rd r1 X0 k else
-  match cmp with
-  | Clt => sltuimm32 rd r1 n k
-  | _   => loadimm32 X31 n (transl_cond_int32u cmp rd r1 X31 k)
-  end.
-
-Definition transl_condimm_int64s (cmp: comparison) (rd: ireg) (r1: ireg) (n: int64) (k: code) :=
-  if Int64.eq n Int64.zero then transl_cond_int64s cmp rd r1 X0 k else
-  match cmp with
-  | Ceq | Cne => xorimm64 rd r1 n (transl_cond_int64s cmp rd rd X0 k)
-  | Clt => sltimm64 rd r1 n k
-  | Cle => if Int64.eq n (Int64.repr Int64.max_signed)
-           then loadimm32 rd Int.one k
-           else sltimm64 rd r1 (Int64.add n Int64.one) k
-  | _   => loadimm64 X31 n (transl_cond_int64s cmp rd r1 X31 k)
-  end.
-
-Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int64) (k: code) :=
-  if Int64.eq n Int64.zero then transl_cond_int64u cmp rd r1 X0 k else
-  match cmp with
-  | Clt => sltuimm64 rd r1 n k
-  | _   => loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k)
-   end.
-
-Definition transl_cond_op
-           (cond: condition) (rd: ireg) (args: list mreg) (k: code) :=
-  match cond, args with
-  | Ccomp c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cond_int32s c rd r1 r2 k)
-  | Ccompu c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cond_int32u c rd r1 r2 k)
-  | Ccompimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (transl_condimm_int32s c rd r1 n k)
-  | Ccompuimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (transl_condimm_int32u c rd r1 n k)
-  | Ccompl c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cond_int64s c rd r1 r2 k)
-  | Ccomplu c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-     OK (transl_cond_int64u c rd r1 r2 k)
-  | Ccomplimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (transl_condimm_int64s c rd r1 n k)
-  | Ccompluimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-     OK (transl_condimm_int64u c rd r1 n k)
-  | Ccompf c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_float c rd r1 r2 in
-      OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k)
-  | Cnotcompf c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_float c rd r1 r2 in
-      OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k)
-  | Ccompfs c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_single c rd r1 r2 in
-      OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k)
-  | Cnotcompfs c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_single c rd r1 r2 in
-     OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k)
-  | _, _ =>
-      Error(msg "Asmgen.transl_cond_op")
-   end.
-
 (** Translation of the arithmetic operation [r <- op(args)].
   The corresponding instructions are prepended to [k]. *)
   
@@ -483,22 +218,6 @@ Definition transl_op
       | FR r, FR a => OK (Pfmv r a :: k)
       |  _  ,  _   => Error(msg "Asmgen.Omove")
       end
-  | Ointconst n, nil =>
-      do rd <- ireg_of res;
-      OK (loadimm32 rd n k)
-  | Olongconst n, nil =>
-      do rd <- ireg_of res;
-      OK (loadimm64 rd n k)
-  | Ofloatconst f, nil =>
-      do rd <- freg_of res;
-      OK (if Float.eq_dec f Float.zero
-          then Pfcvtdw rd X0 :: k
-          else Ploadfi rd f :: k)
-  | Osingleconst f, nil =>
-      do rd <- freg_of res;
-      OK (if Float32.eq_dec f Float32.zero
-          then Pfcvtsw rd X0 :: k
-          else Ploadsi rd f :: k)
   | Oaddrsymbol s ofs, nil =>
       do rd <- ireg_of res;
       OK (if Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)
@@ -508,18 +227,9 @@ Definition transl_op
       do rd <- ireg_of res;
       OK (addptrofs rd SP n k)
 
-  | Ocast8signed, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- ireg_of a1;
-      OK (Pslliw rd rs (Int.repr 24) :: Psraiw rd rd (Int.repr 24) :: k)
-  | Ocast16signed, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- ireg_of a1;
-      OK (Pslliw rd rs (Int.repr 16) :: Psraiw rd rd (Int.repr 16) :: k)
   | Oadd, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Paddw rd rs1 rs2 :: k)
-  | Oaddimm n, a1 :: nil =>
-      do rd  <- ireg_of res; do rs <- ireg_of a1;
-      OK (addimm32 rd rs n k)
   | Oneg, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (Psubw rd X0 rs :: k)
@@ -550,21 +260,12 @@ Definition transl_op
   | Oand, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pandw rd rs1 rs2 :: k)
-  | Oandimm n, a1 :: nil =>
-      do rd  <- ireg_of res; do rs <- ireg_of a1;
-      OK (andimm32 rd rs n k)
   | Oor, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Porw rd rs1 rs2 :: k)
-  | Oorimm n, a1 :: nil =>
-      do rd  <- ireg_of res; do rs <- ireg_of a1;
-      OK (orimm32 rd rs n k)
   | Oxor, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pxorw rd rs1 rs2 :: k)
-  | Oxorimm n, a1 :: nil =>
-      do rd  <- ireg_of res; do rs <- ireg_of a1;
-      OK (xorimm32 rd rs n k)
   | Oshl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Psllw rd rs1 rs2 :: k)
@@ -583,19 +284,6 @@ Definition transl_op
   | Oshruimm n, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
       OK (Psrliw rd rs n :: k)
-  | Oshrximm n, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- ireg_of a1;
-        OK (if Int.eq n Int.zero
-            then Pmv rd rs :: k
-            else if Int.eq n Int.one
-                 then Psrliw X31 rs (Int.repr 31) ::
-                      Paddw X31 rs X31 ::
-                      Psraiw rd X31 Int.one :: k
-                 else Psraiw X31 rs (Int.repr 31) ::
-                      Psrliw X31 X31 (Int.sub Int.iwordsize n) ::
-                      Paddw X31 rs X31 ::
-                      Psraiw rd X31 n :: k)  
-
   (* [Omakelong], [Ohighlong]  should not occur *)
   | Olowlong, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
@@ -604,16 +292,9 @@ Definition transl_op
       do rd <- ireg_of res; do rs <- ireg_of a1;
       assertion (ireg_eq rd rs);
       OK (Pcvtw2l rd :: k)
-  | Ocast32unsigned, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- ireg_of a1;
-      assertion (ireg_eq rd rs);
-      OK (Pcvtw2l rd :: Psllil rd rd (Int.repr 32) :: Psrlil rd rd (Int.repr 32) :: k)
   | Oaddl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Paddl rd rs1 rs2 :: k)
-  | Oaddlimm n, a1 :: nil =>
-      do rd  <- ireg_of res; do rs <- ireg_of a1;
-      OK (addimm64 rd rs n k)
   | Onegl, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (Psubl rd X0 rs :: k)
@@ -644,21 +325,12 @@ Definition transl_op
   | Oandl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pandl rd rs1 rs2 :: k)
-  | Oandlimm n, a1 :: nil =>
-      do rd  <- ireg_of res; do rs <- ireg_of a1;
-      OK (andimm64 rd rs n k)
   | Oorl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Porl rd rs1 rs2 :: k)
-  | Oorlimm n, a1 :: nil =>
-      do rd  <- ireg_of res; do rs <- ireg_of a1;
-      OK (orimm64 rd rs n k)
   | Oxorl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pxorl rd rs1 rs2 :: k)
-  | Oxorlimm n, a1 :: nil =>
-      do rd  <- ireg_of res; do rs <- ireg_of a1;
-      OK (xorimm64 rd rs n k)
   | Oshll, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pslll rd rs1 rs2 :: k)
@@ -677,19 +349,6 @@ Definition transl_op
   | Oshrluimm n, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
       OK (Psrlil rd rs n :: k)
-  | Oshrxlimm n, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- ireg_of a1;
-        OK (if Int.eq n Int.zero
-            then Pmv rd rs :: k
-            else if Int.eq n Int.one
-                 then Psrlil X31 rs (Int.repr 63) ::
-                      Paddl X31 rs X31 ::
-                      Psrail rd X31 Int.one :: k
-                 else Psrail X31 rs (Int.repr 63) ::
-                      Psrlil X31 X31 (Int.sub Int64.iwordsize' n) ::
-                      Paddl X31 rs X31 ::
-                      Psrail rd X31 n :: k)  
-
   | Onegf, a1 :: nil =>
       do rd <- freg_of res; do rs <- freg_of a1;
       OK (Pfnegd rd rs :: k)
@@ -784,9 +443,6 @@ Definition transl_op
   | Osingleoflongu, a1 :: nil =>
       do rd <- freg_of res; do rs <- ireg_of a1;
       OK (Pfcvtslu rd rs :: k)
-  | Ocmp cmp, _ =>
-      do rd <- ireg_of res;
-     transl_cond_op cmp rd args k
 
   (* Instructions expanded in RTL *)
   | OEseqw optR, a1 :: a2 :: nil =>
diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v
index 509eac94..4af8352c 100644
--- a/riscV/Asmgenproof.v
+++ b/riscV/Asmgenproof.v
@@ -115,14 +115,6 @@ Qed.
 
 Section TRANSL_LABEL.
 
-Remark loadimm32_label:
-  forall r n k, tail_nolabel k (loadimm32 r n k).
-Proof.
-  intros; unfold loadimm32. destruct (make_immed32 n); TailNoLabel.
-  unfold load_hilo32. destruct (Int.eq lo Int.zero); TailNoLabel.
-Qed.
-Hint Resolve loadimm32_label: labels.
-
 Remark opimm32_label:
   forall op opimm r1 r2 n k,
   (forall r1 r2 r3, nolabel (op r1 r2 r3)) ->
@@ -134,14 +126,6 @@ Proof.
 Qed.
 Hint Resolve opimm32_label: labels.
 
-Remark loadimm64_label:
-  forall r n k, tail_nolabel k (loadimm64 r n k).
-Proof.
-  intros; unfold loadimm64. destruct (make_immed64 n); TailNoLabel.
-  unfold load_hilo64. destruct (Int64.eq lo Int64.zero); TailNoLabel.
-Qed.
-Hint Resolve loadimm64_label: labels.
-
 Remark opimm64_label:
   forall op opimm r1 r2 n k,
   (forall r1 r2 r3, nolabel (op r1 r2 r3)) ->
@@ -161,165 +145,25 @@ Proof.
 Qed.
 Hint Resolve addptrofs_label: labels.
 
-Remark transl_cond_float_nolabel:
-  forall c r1 r2 r3 insn normal,
-  transl_cond_float c r1 r2 r3 = (insn, normal) -> nolabel insn.
-Proof.
-  unfold transl_cond_float; intros. destruct c; inv H; exact I.
-Qed.
-
-Remark transl_cond_single_nolabel:
-  forall c r1 r2 r3 insn normal,
-  transl_cond_single c r1 r2 r3 = (insn, normal) -> nolabel insn.
-Proof.
-  unfold transl_cond_single; intros. destruct c; inv H; exact I.
-   Qed.
-
 Remark transl_cbranch_label:
   forall cond args lbl k c,
   transl_cbranch cond args lbl k = OK c -> tail_nolabel k c.
 Proof.
   intros. unfold transl_cbranch in H; destruct cond; TailNoLabel.
-- destruct c0; simpl; TailNoLabel.
-- destruct c0; simpl; TailNoLabel.
-- destruct (Int.eq n Int.zero).
-  destruct c0; simpl; TailNoLabel.
-  apply tail_nolabel_trans with (transl_cbranch_int32s c0 x X31 lbl :: k).
-  auto with labels. destruct c0; simpl; TailNoLabel.
-- destruct (Int.eq n Int.zero).
-  destruct c0; simpl; TailNoLabel.
-  apply tail_nolabel_trans with (transl_cbranch_int32u c0 x X31 lbl :: k).
-  auto with labels. destruct c0; simpl; TailNoLabel.
-- destruct c0; simpl; TailNoLabel.
-- destruct c0; simpl; TailNoLabel.
-- destruct (Int64.eq n Int64.zero).
-  destruct c0; simpl; TailNoLabel.
-  apply tail_nolabel_trans with (transl_cbranch_int64s c0 x X31 lbl :: k).
-  auto with labels. destruct c0; simpl; TailNoLabel.
-- destruct (Int64.eq n Int64.zero).
-  destruct c0; simpl; TailNoLabel.
-  apply tail_nolabel_trans with (transl_cbranch_int64u c0 x X31 lbl :: k).
-  auto with labels. destruct c0; simpl; TailNoLabel.
-- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. 
-     destruct normal; TailNoLabel.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
+  all: destruct optR as [[]|]; simpl in *; TailNoLabel.
 Qed.
 
-Remark transl_cond_op_label:
-  forall cond args r k c,
-  transl_cond_op cond r args k = OK c -> tail_nolabel k c.
-Proof.
-  intros. unfold transl_cond_op in H; destruct cond; TailNoLabel.
-- destruct c0; simpl; TailNoLabel.
-- destruct c0; simpl; TailNoLabel. 
-- unfold transl_condimm_int32s.
-  destruct (Int.eq n Int.zero).
-+ destruct c0; simpl; TailNoLabel.
-+ destruct c0; simpl.
-* eapply tail_nolabel_trans; [apply opimm32_label; intros; exact I | TailNoLabel].
-* eapply tail_nolabel_trans; [apply opimm32_label; intros; exact I | TailNoLabel].
-* apply opimm32_label; intros; exact I.
-* destruct (Int.eq n (Int.repr Int.max_signed)). apply loadimm32_label. apply opimm32_label; intros; exact I.
-* eapply tail_nolabel_trans. apply loadimm32_label. TailNoLabel.
-* eapply tail_nolabel_trans. apply loadimm32_label. TailNoLabel.
-- unfold transl_condimm_int32u.
-  destruct (Int.eq n Int.zero).
-+ destruct c0; simpl; TailNoLabel.
-+ destruct c0; simpl; 
-  try (eapply tail_nolabel_trans; [apply loadimm32_label | TailNoLabel]).
-  apply opimm32_label; intros; exact I.
-- destruct c0; simpl; TailNoLabel.
-     - destruct c0; simpl; TailNoLabel.
-- unfold transl_condimm_int64s.
-  destruct (Int64.eq n Int64.zero).
-+ destruct c0; simpl; TailNoLabel.
-+ destruct c0; simpl.
-* eapply tail_nolabel_trans; [apply opimm64_label; intros; exact I | TailNoLabel].
-* eapply tail_nolabel_trans; [apply opimm64_label; intros; exact I | TailNoLabel].
-* apply opimm64_label; intros; exact I.
-* destruct (Int64.eq n (Int64.repr Int64.max_signed)). apply loadimm32_label. apply opimm64_label; intros; exact I.
-* eapply tail_nolabel_trans. apply loadimm64_label. TailNoLabel.
-* eapply tail_nolabel_trans. apply loadimm64_label. TailNoLabel.
-- unfold transl_condimm_int64u.
-  destruct (Int64.eq n Int64.zero).
-+ destruct c0; simpl; TailNoLabel.
-+ destruct c0; simpl; 
-  try (eapply tail_nolabel_trans; [apply loadimm64_label | TailNoLabel]).
-     apply opimm64_label; intros; exact I.
-- destruct (transl_cond_float c0 r x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-- destruct (transl_cond_float c0 r x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-- destruct (transl_cond_single c0 r x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-- destruct (transl_cond_single c0 r x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-   Qed.
-
 Remark transl_op_label:
   forall op args r k c,
   transl_op op args r k = OK c -> tail_nolabel k c.
 Proof.
 Opaque Int.eq.
-  unfold transl_op; intros; destruct op; TailNoLabel.
+  unfold transl_op; intros; destruct op; TailNoLabel;
+  try (destruct optR as [[]|]; simpl in *; TailNoLabel).
 - destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel.
-- destruct (Float.eq_dec n Float.zero); TailNoLabel.
-- destruct (Float32.eq_dec n Float32.zero); TailNoLabel.
 - destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)).
 + eapply tail_nolabel_trans; [|apply addptrofs_label]. TailNoLabel.
 + TailNoLabel. 
-- apply opimm32_label; intros; exact I.
-- apply opimm32_label; intros; exact I.
-- apply opimm32_label; intros; exact I.
-- apply opimm32_label; intros; exact I.
-- destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel.
-- apply opimm64_label; intros; exact I.
-- apply opimm64_label; intros; exact I.
-- apply opimm64_label; intros; exact I.
-- apply opimm64_label; intros; exact I.
-- destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel.
-- eapply transl_cond_op_label; eauto.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
-- destruct optR as [[]|]; simpl in *; TailNoLabel.
 Qed.
 
 Remark indexed_memory_access_label:
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index 2293e001..faa066b0 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -129,22 +129,6 @@ Proof.
   intros; Simpl.
 Qed.
 
-Lemma loadimm32_correct:
-  forall rd n k rs m,
-  exists rs',
-     exec_straight ge fn (loadimm32 rd n k) rs m k rs' m
-  /\ rs'#rd = Vint n
-  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
-Proof.
-  unfold loadimm32; intros. generalize (make_immed32_sound n); intros E.
-  destruct (make_immed32 n). 
-- subst imm. econstructor; split. 
-  apply exec_straight_one. simpl; eauto. auto.
-  split. rewrite Int.add_zero_l; Simpl. 
-  intros; Simpl.
-- rewrite E. apply load_hilo32_correct.
-Qed.
-
 Lemma opimm32_correct:
   forall (op: ireg -> ireg0 -> ireg0 -> instruction)
          (opi: ireg -> ireg0 -> int -> instruction)
@@ -195,27 +179,6 @@ Proof.
   intros; Simpl.
 Qed.
 
-Lemma loadimm64_correct:
-  forall rd n k rs m,
-  exists rs',
-     exec_straight ge fn (loadimm64 rd n k) rs m k rs' m
-  /\ rs'#rd = Vlong n
-  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
-Proof.
-  unfold loadimm64; intros. generalize (make_immed64_sound n); intros E.
-  destruct (make_immed64 n). 
-- subst imm. econstructor; split. 
-  apply exec_straight_one. simpl; eauto. auto.
-  split. rewrite Int64.add_zero_l; Simpl. 
-  intros; Simpl.
-- exploit load_hilo64_correct; eauto. intros (rs' & A & B & C).
-  rewrite E. exists rs'; eauto.
-- subst imm. econstructor; split. 
-  apply exec_straight_one. simpl; eauto. auto.
-  split. Simpl. 
-  intros; Simpl.
-Qed.
-
 Lemma opimm64_correct:
   forall (op: ireg -> ireg0 -> ireg0 -> instruction)
          (opi: ireg -> ireg0 -> int64 -> instruction)
@@ -290,102 +253,6 @@ Proof.
   rewrite H0 in B. inv B. auto.
 Qed.
 
-(** Translation of conditional branches *)
-
-Lemma transl_cbranch_int32s_correct:
-  forall cmp r1 r2 lbl (rs: regset) m b,
-  Val.cmp_bool cmp rs##r1 rs##r2 = Some b ->
-  exec_instr ge fn (transl_cbranch_int32s cmp r1 r2 lbl) rs m =
-  eval_branch fn lbl rs m (Some b).
-Proof.
-  intros. destruct cmp; simpl; rewrite ? H.
-- destruct rs##r1; simpl in H; try discriminate. destruct rs##r2; inv H.
-  simpl; auto.
-- destruct rs##r1; simpl in H; try discriminate. destruct rs##r2; inv H.
-  simpl; auto.
-- auto.
-- rewrite <- Val.swap_cmp_bool. simpl. rewrite H; auto.
-- rewrite <- Val.swap_cmp_bool. simpl. rewrite H; auto.
-- auto.
-Qed.
-
-Lemma transl_cbranch_int32u_correct:
-  forall cmp r1 r2 lbl (rs: regset) m b,
-  Val.cmpu_bool (Mem.valid_pointer m) cmp rs##r1 rs##r2 = Some b ->
-  exec_instr ge fn (transl_cbranch_int32u cmp r1 r2 lbl) rs m =
-  eval_branch fn lbl rs m (Some b).
-Proof.
-  intros. destruct cmp; simpl; rewrite ? H; auto.
-- rewrite <- Val.swap_cmpu_bool. simpl. rewrite H; auto.
-- rewrite <- Val.swap_cmpu_bool. simpl. rewrite H; auto.
-Qed.
-
-Lemma transl_cbranch_int64s_correct:
-  forall cmp r1 r2 lbl (rs: regset) m b,
-  Val.cmpl_bool cmp rs###r1 rs###r2 = Some b ->
-  exec_instr ge fn (transl_cbranch_int64s cmp r1 r2 lbl) rs m =
-  eval_branch fn lbl rs m (Some b).
-Proof.
-  intros. destruct cmp; simpl; rewrite ? H.
-- destruct rs###r1; simpl in H; try discriminate. destruct rs###r2; inv H.
-  simpl; auto.
-- destruct rs###r1; simpl in H; try discriminate. destruct rs###r2; inv H.
-  simpl; auto.
-- auto.
-- rewrite <- Val.swap_cmpl_bool. simpl. rewrite H; auto.
-- rewrite <- Val.swap_cmpl_bool. simpl. rewrite H; auto.
-- auto.
-Qed.
-
-Lemma transl_cbranch_int64u_correct:
-  forall cmp r1 r2 lbl (rs: regset) m b,
-  Val.cmplu_bool (Mem.valid_pointer m) cmp rs###r1 rs###r2 = Some b ->
-  exec_instr ge fn (transl_cbranch_int64u cmp r1 r2 lbl) rs m =
-  eval_branch fn lbl rs m (Some b).
-Proof.
-  intros. destruct cmp; simpl; rewrite ? H; auto.
-- rewrite <- Val.swap_cmplu_bool. simpl. rewrite H; auto.
-- rewrite <- Val.swap_cmplu_bool. simpl. rewrite H; auto.
-Qed.
-
-Lemma transl_cond_float_correct:
-  forall (rs: regset) m cmp rd r1 r2 insn normal v,
-  transl_cond_float cmp rd r1 r2 = (insn, normal) ->
-  v = (if normal then Val.cmpf cmp rs#r1 rs#r2 else Val.notbool (Val.cmpf cmp rs#r1 rs#r2)) ->
-  exec_instr ge fn insn rs m = Next (nextinstr (rs#rd <- v)) m.
-Proof.
-  intros. destruct cmp; simpl in H; inv H; auto. 
-- rewrite Val.negate_cmpf_eq. auto.
-- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpf, Val.cmpf_bool.
-  rewrite <- Float.cmp_swap. auto.
-- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpf, Val.cmpf_bool.
-  rewrite <- Float.cmp_swap. auto.
-Qed.
-
-Lemma transl_cond_single_correct:
-  forall (rs: regset) m cmp rd r1 r2 insn normal v,
-  transl_cond_single cmp rd r1 r2 = (insn, normal) ->
-  v = (if normal then Val.cmpfs cmp rs#r1 rs#r2 else Val.notbool (Val.cmpfs cmp rs#r1 rs#r2)) ->
-  exec_instr ge fn insn rs m = Next (nextinstr (rs#rd <- v)) m.
-Proof.
-  intros. destruct cmp; simpl in H; inv H; auto. 
-- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool.
-  rewrite Float32.cmp_ne_eq. destruct (Float32.cmp Ceq f0 f); auto.
-- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool.
-  rewrite <- Float32.cmp_swap. auto.
-- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool.
-  rewrite <- Float32.cmp_swap. auto.
-   Qed.
-
-(* TODO gourdinl UNUSUED ? Remark branch_on_X31:
-  forall normal lbl (rs: regset) m b,
-  rs#X31 = Val.of_bool (eqb normal b) -> 
-  exec_instr ge fn (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) rs m =
-  eval_branch fn lbl rs m (Some b).
-Proof.
-  intros. destruct normal; simpl; rewrite H; simpl; destruct b; reflexivity. 
-   Qed.*)
-
 Ltac ArgsInv :=
   repeat (match goal with
   | [ H: Error _ = OK _ |- _ ] => discriminate
@@ -417,219 +284,46 @@ Proof.
   { apply eval_condition_lessdef with (map ms args) m; auto. eapply preg_vals; eauto. }
   clear EVAL MEXT AG.
   destruct cond; simpl in TRANSL; ArgsInv.
-  - exists rs, (transl_cbranch_int32s c0 x x0 lbl).
-  intuition auto. constructor. apply transl_cbranch_int32s_correct; auto.
-- exists rs, (transl_cbranch_int32u c0 x x0 lbl).
-  intuition auto. constructor. apply transl_cbranch_int32u_correct; auto.
-- predSpec Int.eq Int.eq_spec n Int.zero.
-+ subst n. exists rs, (transl_cbranch_int32s c0 x X0 lbl).
-  intuition auto. constructor. apply transl_cbranch_int32s_correct; auto.
-+ exploit (loadimm32_correct X31 n); eauto. intros (rs' & A & B & C).
-  exists rs', (transl_cbranch_int32s c0 x X31 lbl).
-  split. constructor; eexact A. split; auto.
-  apply transl_cbranch_int32s_correct; auto.
-  simpl; rewrite B, C; eauto with asmgen.
-- predSpec Int.eq Int.eq_spec n Int.zero.
-+ subst n. exists rs, (transl_cbranch_int32u c0 x X0 lbl).
-  intuition auto. constructor. apply transl_cbranch_int32u_correct; auto.
-+ exploit (loadimm32_correct X31 n); eauto. intros (rs' & A & B & C).
-  exists rs', (transl_cbranch_int32u c0 x X31 lbl).
-  split. constructor; eexact A. split; auto.
-  apply transl_cbranch_int32u_correct; auto.
-  simpl; rewrite B, C; eauto with asmgen.
-- exists rs, (transl_cbranch_int64s c0 x x0 lbl).
-  intuition auto. constructor. apply transl_cbranch_int64s_correct; auto.
-- exists rs, (transl_cbranch_int64u c0 x x0 lbl).
-  intuition auto. constructor. apply transl_cbranch_int64u_correct; auto.
-- predSpec Int64.eq Int64.eq_spec n Int64.zero.
-+ subst n. exists rs, (transl_cbranch_int64s c0 x X0 lbl).
-  intuition auto. constructor. apply transl_cbranch_int64s_correct; auto.
-+ exploit (loadimm64_correct X31 n); eauto. intros (rs' & A & B & C).
-  exists rs', (transl_cbranch_int64s c0 x X31 lbl).
-  split. constructor; eexact A. split; auto.
-  apply transl_cbranch_int64s_correct; auto.
-  simpl; rewrite B, C; eauto with asmgen.
-- predSpec Int64.eq Int64.eq_spec n Int64.zero.
-+ subst n. exists rs, (transl_cbranch_int64u c0 x X0 lbl).
-  intuition auto. constructor. apply transl_cbranch_int64u_correct; auto.
-+ exploit (loadimm64_correct X31 n); eauto. intros (rs' & A & B & C).
-  exists rs', (transl_cbranch_int64u c0 x X31 lbl).
-  split. constructor; eexact A. split; auto.
-  apply transl_cbranch_int64u_correct; auto.
-  simpl; rewrite B, C; eauto with asmgen.
-- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2.
-  set (v := if normal then Val.cmpf c0 rs#x rs#x0 else Val.notbool (Val.cmpf c0 rs#x rs#x0)).
-  assert (V: v = Val.of_bool (eqb normal b)).
-  { unfold v, Val.cmpf. rewrite EVAL'. destruct normal, b; reflexivity. }
-  econstructor; econstructor.
-  split. constructor. apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto.
-  split. rewrite V; destruct normal, b; reflexivity.
-  intros; Simpl.
-- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2.
-  assert (EVAL'': Val.cmpf_bool c0 (rs x) (rs x0) = Some (negb b)).
-  { destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; inv EVAL'; auto. }
-  set (v := if normal then Val.cmpf c0 rs#x rs#x0 else Val.notbool (Val.cmpf c0 rs#x rs#x0)).
-  assert (V: v = Val.of_bool (xorb normal b)).
-  { unfold v, Val.cmpf. rewrite EVAL''. destruct normal, b; reflexivity. }
-  econstructor; econstructor.
-  split. constructor. apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto.
-  split. rewrite V; destruct normal, b; reflexivity.
-  intros; Simpl.
-- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2.
-  set (v := if normal then Val.cmpfs c0 rs#x rs#x0 else Val.notbool (Val.cmpfs c0 rs#x rs#x0)).
-  assert (V: v = Val.of_bool (eqb normal b)).
-  { unfold v, Val.cmpfs. rewrite EVAL'. destruct normal, b; reflexivity. }
-  econstructor; econstructor.
-  split. constructor. apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto.
-  split. rewrite V; destruct normal, b; reflexivity.
-  intros; Simpl.
-- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2.
-  assert (EVAL'': Val.cmpfs_bool c0 (rs x) (rs x0) = Some (negb b)).
-  { destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; inv EVAL'; auto. }
-  set (v := if normal then Val.cmpfs c0 rs#x rs#x0 else Val.notbool (Val.cmpfs c0 rs#x rs#x0)).
-  assert (V: v = Val.of_bool (xorb normal b)).
-  { unfold v, Val.cmpfs. rewrite EVAL''. destruct normal, b; reflexivity. }
-  econstructor; econstructor.
-  split. constructor. apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto.
-  split. rewrite V; destruct normal, b; reflexivity.
-     intros; Simpl.
-
-- destruct optR as [[]|];
-  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
-  unfold zero32, Op.zero32 in *;
-  destruct (rs x) eqn:EQRS; simpl in *; try congruence;
-  inv EQ2; eexists; eexists; eauto; split; constructor; auto;
-  simpl in *.
-  + rewrite EQRS;
-    assert (HB: (Int.eq Int.zero i) = b) by congruence.
+  all:
+    destruct optR as [[]|];
+    unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+    unfold zero32, Op.zero32 in *;
+    unfold zero64, Op.zero64 in *; inv EQ2;
+    try (destruct (rs x); simpl in EVAL'; discriminate; fail);
+    try (eexists; eexists; eauto; split; constructor;
+    simpl in *; try rewrite EVAL'; auto; fail).
+  all:
+    destruct (rs x) eqn:EQRS; simpl in *; try congruence;
+    eexists; eexists; eauto; split; constructor; auto;
+    simpl in *; rewrite EQRS.
+  - assert (HB: (Int.eq Int.zero i) = b) by congruence;
     rewrite HB; destruct b; simpl; auto.
-  + rewrite EQRS;
-    assert (HB: (Int.eq i Int.zero) = b) by congruence.
+  - assert (HB: (Int.eq i Int.zero) = b) by congruence.
     rewrite <- HB; destruct b; simpl; auto.
-  + rewrite EQRS;
-    destruct (rs x0); try congruence.
+  - destruct (rs x0); try congruence.
     assert (HB: (Int.eq i i0) = b) by congruence.
     rewrite <- HB; destruct b; simpl; auto.
-- destruct optR as [[]|];
-  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
-  unfold zero32, Op.zero32 in *;
-  destruct (rs x) eqn:EQRS; simpl in *; try congruence;
-  inv EQ2; eexists; eexists; eauto; split; constructor; auto;
-  simpl in *.
-  + rewrite EQRS;
-    assert (HB: negb (Int.eq Int.zero i) = b) by congruence.
+  - assert (HB: negb (Int.eq Int.zero i) = b) by congruence.
     rewrite HB; destruct b; simpl; auto.
-  + rewrite EQRS;
-    assert (HB: negb (Int.eq i Int.zero) = b) by congruence.
+  - assert (HB: negb (Int.eq i Int.zero) = b) by congruence.
     rewrite <- HB; destruct b; simpl; auto.
-  + rewrite EQRS;
-    destruct (rs x0); try congruence.
+  - destruct (rs x0); try congruence.
     assert (HB: negb (Int.eq i i0) = b) by congruence.
     rewrite <- HB; destruct b; simpl; auto.
-- destruct optR as [[]|];
-  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
-  unfold zero32, Op.zero32 in *; inv EQ2;
-  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; try rewrite EVAL'; auto.
-- destruct optR as [[]|];
-  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
-  unfold zero32, Op.zero32 in *; inv EQ2;
-  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; try rewrite EVAL'; auto.
-- destruct optR as [[]|];
-  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
-  unfold zero32, Op.zero32 in *; inv EQ2;
-  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; try rewrite EVAL'; auto.
-- destruct optR as [[]|];
-  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
-  unfold zero32, Op.zero32 in *; inv EQ2;
-  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; try rewrite EVAL'; auto.
-- destruct optR as [[]|];
-  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
-  unfold zero32, Op.zero32 in *; inv EQ2;
-  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; try rewrite EVAL'; auto.
-- destruct optR as [[]|];
-  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
-  unfold zero32, Op.zero32 in *; inv EQ2;
-  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; try rewrite EVAL'; auto.
-- destruct optR as [[]|];
-  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
-  unfold zero32, Op.zero32 in *; inv EQ2;
-  destruct (rs x) eqn:EQRS; simpl in *; try congruence;
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; auto.
-  + rewrite EQRS;
-    assert (HB: (Int64.eq Int64.zero i) = b) by congruence.
+  - assert (HB: (Int64.eq Int64.zero i) = b) by congruence.
     rewrite HB; destruct b; simpl; auto.
-  + rewrite EQRS;
-    assert (HB: (Int64.eq i Int64.zero) = b) by congruence.
+  - assert (HB: (Int64.eq i Int64.zero) = b) by congruence.
     rewrite <- HB; destruct b; simpl; auto.
-  + rewrite EQRS;
-    destruct (rs x0); try congruence.
+  - destruct (rs x0); try congruence.
     assert (HB: (Int64.eq i i0) = b) by congruence.
     rewrite <- HB; destruct b; simpl; auto.
-- destruct optR as [[]|];
-  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
-  unfold zero32, Op.zero32 in *; inv EQ2;
-  destruct (rs x) eqn:EQRS; simpl in *; try congruence;
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; auto.
-  + rewrite EQRS;
-    assert (HB: negb (Int64.eq Int64.zero i) = b) by congruence.
+  - assert (HB: negb (Int64.eq Int64.zero i) = b) by congruence.
     rewrite HB; destruct b; simpl; auto.
-  + rewrite EQRS;
-    assert (HB: negb (Int64.eq i Int64.zero) = b) by congruence.
+  - assert (HB: negb (Int64.eq i Int64.zero) = b) by congruence.
     rewrite <- HB; destruct b; simpl; auto.
-  + rewrite EQRS;
-    destruct (rs x0); try congruence.
+  - destruct (rs x0); try congruence.
     assert (HB: negb (Int64.eq i i0) = b) by congruence.
     rewrite <- HB; destruct b; simpl; auto.
-- destruct optR as [[]|];
-  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
-  unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
-  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; try rewrite EVAL'; auto.
-- destruct optR as [[]|];
-  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
-  unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
-  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; try rewrite EVAL'; auto.
-- destruct optR as [[]|];
-  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
-  unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
-  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; try rewrite EVAL'; auto.
-- destruct optR as [[]|];
-  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
-  unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
-  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; try rewrite EVAL'; auto.
-- destruct optR as [[]|];
-  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
-  unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
-  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; try rewrite EVAL'; auto.
-- destruct optR as [[]|];
-  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
-  unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
-  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; try rewrite EVAL'; auto.
 Qed.
 
 Lemma transl_cbranch_correct_true:
@@ -663,417 +357,6 @@ Proof.
   intros; Simpl. 
 Qed.
 
-(** Translation of condition operators *)
-
-Lemma transl_cond_int32s_correct:
-  forall cmp rd r1 r2 k rs m,
-  exists rs',
-     exec_straight ge fn (transl_cond_int32s cmp rd r1 r2 k) rs m k rs' m
-  /\ Val.lessdef (Val.cmp cmp rs##r1 rs##r2) rs'#rd
-  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
-Proof.
-  intros. destruct cmp; simpl. 
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmp. rewrite <- Val.swap_cmp_bool.
-  simpl. rewrite (Val.negate_cmp_bool Clt). 
-  destruct (Val.cmp_bool Clt rs##r2 rs##r1) as [[]|]; auto.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. unfold Val.cmp. rewrite <- Val.swap_cmp_bool. auto.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmp. rewrite (Val.negate_cmp_bool Clt). 
-  destruct (Val.cmp_bool Clt rs##r1 rs##r2) as [[]|]; auto.
-Qed.
-
-Lemma transl_cond_int32u_correct:
-  forall cmp rd r1 r2 k rs m,
-  exists rs',
-     exec_straight ge fn (transl_cond_int32u cmp rd r1 r2 k) rs m k rs' m
-  /\ rs'#rd = Val.cmpu (Mem.valid_pointer m) cmp rs##r1 rs##r2
-  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
-Proof.
-  intros. destruct cmp; simpl. 
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmpu. rewrite <- Val.swap_cmpu_bool.
-  simpl. rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Cle). 
-  destruct (Val.cmpu_bool (Mem.valid_pointer m) Cle rs##r1 rs##r2) as [[]|]; auto.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. unfold Val.cmpu. rewrite <- Val.swap_cmpu_bool. auto.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmpu. rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Clt). 
-  destruct (Val.cmpu_bool (Mem.valid_pointer m) Clt rs##r1 rs##r2) as [[]|]; auto.
-Qed.
-
-Lemma transl_cond_int64s_correct:
-  forall cmp rd r1 r2 k rs m,
-  exists rs',
-     exec_straight ge fn (transl_cond_int64s cmp rd r1 r2 k) rs m k rs' m
-  /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs###r1 rs###r2)) rs'#rd
-  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
-Proof.
-  intros. destruct cmp; simpl. 
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. destruct (rs###r1); auto. destruct (rs###r2); auto.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. destruct (rs###r1); auto. destruct (rs###r2); auto.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmpl. rewrite <- Val.swap_cmpl_bool.
-  simpl. rewrite (Val.negate_cmpl_bool Clt). 
-  destruct (Val.cmpl_bool Clt rs###r2 rs###r1) as [[]|]; auto.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. unfold Val.cmpl. rewrite <- Val.swap_cmpl_bool. auto.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmpl. rewrite (Val.negate_cmpl_bool Clt). 
-  destruct (Val.cmpl_bool Clt rs###r1 rs###r2) as [[]|]; auto.
-Qed.
-
-Lemma transl_cond_int64u_correct:
-  forall cmp rd r1 r2 k rs m,
-  exists rs',
-     exec_straight ge fn (transl_cond_int64u cmp rd r1 r2 k) rs m k rs' m
-  /\ rs'#rd = Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs###r1 rs###r2)
-  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
-Proof.
-  intros. destruct cmp; simpl. 
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmplu. rewrite <- Val.swap_cmplu_bool.
-  simpl. rewrite (Val.negate_cmplu_bool (Mem.valid_pointer m) Cle). 
-  destruct (Val.cmplu_bool (Mem.valid_pointer m) Cle rs###r1 rs###r2) as [[]|]; auto.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. unfold Val.cmplu. rewrite <- Val.swap_cmplu_bool. auto.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmplu. rewrite (Val.negate_cmplu_bool (Mem.valid_pointer m) Clt). 
-  destruct (Val.cmplu_bool (Mem.valid_pointer m) Clt rs###r1 rs###r2) as [[]|]; auto.
-Qed.
-
-Lemma transl_condimm_int32s_correct:
-  forall cmp rd r1 n k rs m,
-  r1 <> X31 ->
-  exists rs',
-     exec_straight ge fn (transl_condimm_int32s cmp rd r1 n k) rs m k rs' m
-  /\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd
-  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
-Proof.
-  intros. unfold transl_condimm_int32s.
-  predSpec Int.eq Int.eq_spec n Int.zero.
-- subst n. exploit transl_cond_int32s_correct. intros (rs' & A & B & C).
-  exists rs'; eauto.
-- assert (DFL:
-    exists rs',
-      exec_straight ge fn (loadimm32 X31 n (transl_cond_int32s cmp rd r1 X31 k)) rs m k rs' m
-   /\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd
-   /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
-  { exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
-    exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2).
-    exists rs2; split. 
-    eapply exec_straight_trans. eexact A1. eexact A2. 
-    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. auto.
-    intros; transitivity (rs1 r); auto. }
-  destruct cmp.
-+ unfold xorimm32. 
-  exploit (opimm32_correct Pxorw Pxoriw Val.xor); eauto. intros (rs1 & A1 & B1 & C1).
-  exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2).
-  exists rs2; split. 
-  eapply exec_straight_trans. eexact A1. eexact A2. 
-  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
-  unfold Val.cmp in B2; simpl in B2; rewrite Int.xor_is_zero in B2. exact B2.
-  intros; transitivity (rs1 r); auto.
-+ unfold xorimm32. 
-  exploit (opimm32_correct Pxorw Pxoriw Val.xor); eauto. intros (rs1 & A1 & B1 & C1).
-  exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2).
-  exists rs2; split. 
-  eapply exec_straight_trans. eexact A1. eexact A2. 
-  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
-  unfold Val.cmp in B2; simpl in B2; rewrite Int.xor_is_zero in B2. exact B2.
-  intros; transitivity (rs1 r); auto.
-+ exploit (opimm32_correct Psltw Psltiw (Val.cmp Clt)); eauto. intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
-+ predSpec Int.eq Int.eq_spec n (Int.repr Int.max_signed).
-* subst n. exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. 
-  unfold Val.cmp; destruct (rs#r1); simpl; auto. rewrite B1. 
-  unfold Int.lt. rewrite zlt_false. auto. 
-  change (Int.signed (Int.repr Int.max_signed)) with Int.max_signed.
-  generalize (Int.signed_range i); omega.
-* exploit (opimm32_correct Psltw Psltiw (Val.cmp Clt)); eauto. intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. 
-  rewrite B1. unfold Val.cmp; simpl; destruct (rs#r1); simpl; auto.
-  unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1).
-  destruct (zlt (Int.signed n) (Int.signed i)).
-  rewrite zlt_false by omega. auto.
-  rewrite zlt_true by omega. auto.
-  rewrite Int.add_signed. symmetry; apply Int.signed_repr. 
-  assert (Int.signed n <> Int.max_signed).
-  { red; intros E. elim H1. rewrite <- (Int.repr_signed n). rewrite E. auto. }
-  generalize (Int.signed_range n); omega.
-+ apply DFL.
-+ apply DFL.
-Qed.
-
-Lemma transl_condimm_int32u_correct:
-  forall cmp rd r1 n k rs m,
-  r1 <> X31 ->
-  exists rs',
-     exec_straight ge fn (transl_condimm_int32u cmp rd r1 n k) rs m k rs' m
-  /\ Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp rs#r1 (Vint n)) rs'#rd
-  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
-Proof.
-  intros. unfold transl_condimm_int32u.
-  predSpec Int.eq Int.eq_spec n Int.zero.
-- subst n. exploit transl_cond_int32u_correct. intros (rs' & A & B & C).
-  exists rs'; split. eexact A. split; auto. rewrite B; auto.
-- assert (DFL:
-    exists rs',
-      exec_straight ge fn (loadimm32 X31 n (transl_cond_int32u cmp rd r1 X31 k)) rs m k rs' m
-   /\ Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp rs#r1 (Vint n)) rs'#rd
-   /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
-  { exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
-    exploit transl_cond_int32u_correct; eauto. intros (rs2 & A2 & B2 & C2).
-    exists rs2; split. 
-    eapply exec_straight_trans. eexact A1. eexact A2. 
-    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. rewrite B2; auto.
-    intros; transitivity (rs1 r); auto. }
-  destruct cmp.
-+ apply DFL.
-+ apply DFL.
-+ exploit (opimm32_correct Psltuw Psltiuw (Val.cmpu (Mem.valid_pointer m) Clt) m); eauto.
-  intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
-+ apply DFL.
-+ apply DFL.
-+ apply DFL.
-Qed.
-
-Lemma transl_condimm_int64s_correct:
-  forall cmp rd r1 n k rs m,
-  r1 <> X31 ->
-  exists rs',
-     exec_straight ge fn (transl_condimm_int64s cmp rd r1 n k) rs m k rs' m
-  /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd
-  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
-Proof.
-  intros. unfold transl_condimm_int64s.
-  predSpec Int64.eq Int64.eq_spec n Int64.zero.
-- subst n. exploit transl_cond_int64s_correct. intros (rs' & A & B & C).
-  exists rs'; eauto.
-- assert (DFL:
-    exists rs',
-      exec_straight ge fn (loadimm64 X31 n (transl_cond_int64s cmp rd r1 X31 k)) rs m k rs' m
-   /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd
-   /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
-  { exploit loadimm64_correct; eauto. intros (rs1 & A1 & B1 & C1).
-    exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2).
-    exists rs2; split. 
-    eapply exec_straight_trans. eexact A1. eexact A2. 
-    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. auto.
-    intros; transitivity (rs1 r); auto. }
-  destruct cmp.
-+ unfold xorimm64. 
-  exploit (opimm64_correct Pxorl Pxoril Val.xorl); eauto. intros (rs1 & A1 & B1 & C1).
-  exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2).
-  exists rs2; split. 
-  eapply exec_straight_trans. eexact A1. eexact A2. 
-  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
-  unfold Val.cmpl in B2; simpl in B2; rewrite Int64.xor_is_zero in B2. exact B2.
-  intros; transitivity (rs1 r); auto.
-+ unfold xorimm64. 
-  exploit (opimm64_correct Pxorl Pxoril Val.xorl); eauto. intros (rs1 & A1 & B1 & C1).
-  exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2).
-  exists rs2; split. 
-  eapply exec_straight_trans. eexact A1. eexact A2. 
-  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
-  unfold Val.cmpl in B2; simpl in B2; rewrite Int64.xor_is_zero in B2. exact B2.
-  intros; transitivity (rs1 r); auto.
-+ exploit (opimm64_correct Psltl Psltil (fun v1 v2 => Val.maketotal (Val.cmpl Clt v1 v2))); eauto. intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
-+ predSpec Int64.eq Int64.eq_spec n (Int64.repr Int64.max_signed).
-* subst n. exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. 
-  unfold Val.cmpl; destruct (rs#r1); simpl; auto. rewrite B1. 
-  unfold Int64.lt. rewrite zlt_false. auto. 
-  change (Int64.signed (Int64.repr Int64.max_signed)) with Int64.max_signed.
-  generalize (Int64.signed_range i); omega.
-* exploit (opimm64_correct Psltl Psltil (fun v1 v2 => Val.maketotal (Val.cmpl Clt v1 v2))); eauto. intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. 
-  rewrite B1. unfold Val.cmpl; simpl; destruct (rs#r1); simpl; auto.
-  unfold Int64.lt. replace (Int64.signed (Int64.add n Int64.one)) with (Int64.signed n + 1).
-  destruct (zlt (Int64.signed n) (Int64.signed i)).
-  rewrite zlt_false by omega. auto.
-  rewrite zlt_true by omega. auto.
-  rewrite Int64.add_signed. symmetry; apply Int64.signed_repr. 
-  assert (Int64.signed n <> Int64.max_signed).
-  { red; intros E. elim H1. rewrite <- (Int64.repr_signed n). rewrite E. auto. }
-  generalize (Int64.signed_range n); omega.
-+ apply DFL.
-+ apply DFL.
-Qed.
-
-Lemma transl_condimm_int64u_correct:
-  forall cmp rd r1 n k rs m,
-  r1 <> X31 ->
-  exists rs',
-     exec_straight ge fn (transl_condimm_int64u cmp rd r1 n k) rs m k rs' m
-  /\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd
-  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
-Proof.
-  intros. unfold transl_condimm_int64u.
-  predSpec Int64.eq Int64.eq_spec n Int64.zero.
-- subst n. exploit transl_cond_int64u_correct. intros (rs' & A & B & C).
-  exists rs'; split. eexact A. split; auto. rewrite B; auto.
-- assert (DFL:
-    exists rs',
-      exec_straight ge fn (loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k)) rs m k rs' m
-   /\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd
-   /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
-  { exploit loadimm64_correct; eauto. intros (rs1 & A1 & B1 & C1).
-    exploit transl_cond_int64u_correct; eauto. intros (rs2 & A2 & B2 & C2).
-    exists rs2; split. 
-    eapply exec_straight_trans. eexact A1. eexact A2. 
-    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. rewrite B2; auto.
-    intros; transitivity (rs1 r); auto. }
-  destruct cmp.
-+ apply DFL.
-+ apply DFL.
-+ exploit (opimm64_correct Psltul Psltiul (fun v1 v2 => Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt v1 v2)) m); eauto.
-  intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
-+ apply DFL.
-+ apply DFL.
-+ apply DFL.
-   Qed.
-
-Lemma transl_cond_op_correct:
-  forall cond rd args k c rs m,
-  transl_cond_op cond rd args k = OK c ->
-  exists rs',
-     exec_straight ge fn c rs m k rs' m
-  /\ Val.lessdef (Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m)) rs'#rd
-  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
-Proof.
-  assert (MKTOT: forall ob, Val.of_optbool ob = Val.maketotal (option_map Val.of_bool ob)).
-  { destruct ob as [[]|]; reflexivity. }
-  intros until m; intros TR.
-  destruct cond; simpl in TR; ArgsInv.
-+ (* cmp *)
-  exploit transl_cond_int32s_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto.
-+ (* cmpu *)
-  exploit transl_cond_int32u_correct; eauto. intros (rs' & A & B & C).
-  exists rs'; repeat split; eauto. rewrite B; auto.
-+ (* cmpimm *)
-  apply transl_condimm_int32s_correct; eauto with asmgen.
-+ (* cmpuimm *)
-  apply transl_condimm_int32u_correct; eauto with asmgen.
-+ (* cmpl *)
-  exploit transl_cond_int64s_correct; eauto. intros (rs' & A & B & C).
-  exists rs'; repeat split; eauto. rewrite MKTOT; eauto.
-+ (* cmplu *)
-  exploit transl_cond_int64u_correct; eauto. intros (rs' & A & B & C).
-   exists rs'; repeat split; eauto. rewrite B, MKTOT; eauto.
-+ (* cmplimm *)
-  exploit transl_condimm_int64s_correct; eauto. instantiate (1 := x); eauto with asmgen. 
-  intros (rs' & A & B & C).
-  exists rs'; repeat split; eauto. rewrite MKTOT; eauto.
-+ (* cmpluimm *)
-  exploit transl_condimm_int64u_correct; eauto. instantiate (1 := x); eauto with asmgen. 
-  intros (rs' & A & B & C).
-   exists rs'; repeat split; eauto. rewrite MKTOT; eauto.
-+ (* cmpf *)
-  destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR.
-  fold (Val.cmpf c0 (rs x) (rs x0)).
-  set (v := Val.cmpf c0 (rs x) (rs x0)).
-  destruct normal; inv EQ2.
-* econstructor; split.
-  apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto.
-  split; intros; Simpl.
-* econstructor; split.
-  eapply exec_straight_two.
-  eapply transl_cond_float_correct with (v := Val.notbool v); eauto.
-  simpl; reflexivity.
-  auto. auto.
-  split; intros; Simpl. unfold v, Val.cmpf. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; auto.
-+ (* notcmpf *)
-  destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR.
-  rewrite Val.notbool_negb_3. fold (Val.cmpf c0 (rs x) (rs x0)).
-  set (v := Val.cmpf c0 (rs x) (rs x0)).
-  destruct normal; inv EQ2.
-* econstructor; split.
-  eapply exec_straight_two.
-  eapply transl_cond_float_correct with (v := v); eauto.
-  simpl; reflexivity.
-  auto. auto.
-  split; intros; Simpl. unfold v, Val.cmpf. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; auto.
-* econstructor; split.
-  apply exec_straight_one. eapply transl_cond_float_correct with (v := Val.notbool v); eauto. auto.
-  split; intros; Simpl.
-+ (* cmpfs *)
-  destruct (transl_cond_single c0 rd x x0) as [insn normal] eqn:TR.
-  fold (Val.cmpfs c0 (rs x) (rs x0)).
-  set (v := Val.cmpfs c0 (rs x) (rs x0)).
-  destruct normal; inv EQ2.
-* econstructor; split.
-  apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto.
-  split; intros; Simpl.
-* econstructor; split.
-  eapply exec_straight_two.
-  eapply transl_cond_single_correct with (v := Val.notbool v); eauto.
-  simpl; reflexivity.
-  auto. auto.
-  split; intros; Simpl. unfold v, Val.cmpfs. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; auto.
-+ (* notcmpfs *)
-  destruct (transl_cond_single c0 rd x x0) as [insn normal] eqn:TR.
-  rewrite Val.notbool_negb_3. fold (Val.cmpfs c0 (rs x) (rs x0)).
-  set (v := Val.cmpfs c0 (rs x) (rs x0)).
-  destruct normal; inv EQ2.
-* econstructor; split.
-  eapply exec_straight_two.
-  eapply transl_cond_single_correct with (v := v); eauto.
-  simpl; reflexivity.
-  auto. auto.
-  split; intros; Simpl. unfold v, Val.cmpfs. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; auto.
-* econstructor; split.
-  apply exec_straight_one. eapply transl_cond_single_correct with (v := Val.notbool v); eauto. auto.
-  split; intros; Simpl.
-   Qed.
-
-(** Some arithmetic properties. *)
-
-Remark cast32unsigned_from_cast32signed:
-  forall i, Int64.repr (Int.unsigned i) = Int64.zero_ext 32 (Int64.repr (Int.signed i)).
-Proof.
-  intros. apply Int64.same_bits_eq; intros. 
-  rewrite Int64.bits_zero_ext, !Int64.testbit_repr by tauto.
-  rewrite Int.bits_signed by tauto. fold (Int.testbit i i0).
-  change Int.zwordsize with 32.
-  destruct (zlt i0 32). auto. apply Int.bits_above. auto.
-Qed.
-
 (* Translation of arithmetic operations *)
 
 Ltac SimplEval H :=
@@ -1103,28 +386,6 @@ Opaque Int.eq.
   unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl.
   (* move *)
   { destruct (preg_of res), (preg_of m0); inv TR; TranslOpSimpl. }
-  (* intconst *)
-  { exploit loadimm32_correct; eauto. intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen. }
-  (* longconst *)
-  { exploit loadimm64_correct; eauto. intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen. }
-  (* floatconst *)
-  { destruct (Float.eq_dec n Float.zero).
-    + subst n. econstructor; split. 
-      apply exec_straight_one. simpl; eauto. auto.
-      split; intros; Simpl. 
-    + econstructor; split. 
-      apply exec_straight_one. simpl; eauto. auto.
-      split; intros; Simpl. }
-  (* singleconst *)
-  { destruct (Float32.eq_dec n Float32.zero).
-    + subst n. econstructor; split. 
-      apply exec_straight_one. simpl; eauto. auto.
-      split; intros; Simpl. 
-    + econstructor; split. 
-      apply exec_straight_one. simpl; eauto. auto.
-      split; intros; Simpl. }
   (* addrsymbol *)
   { destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)).
     + set (rs1 := nextinstr (rs#x <- (Genv.symbol_address ge id Ptrofs.zero))).
@@ -1141,138 +402,6 @@ Opaque Int.eq.
   (* stackoffset *)
   { exploit addptrofs_correct. instantiate (1 := X2); auto with asmgen. intros (rs' & A & B & C).
   exists rs'; split; eauto. auto with asmgen. }
-  (* cast8signed *)
-  { econstructor; split.
-  eapply exec_straight_two. simpl;eauto. simpl;eauto. auto. auto.
-  split; intros; Simpl.
-  assert (A: Int.ltu (Int.repr 24) Int.iwordsize = true) by auto.
-  destruct (rs x0); auto; simpl. rewrite A; simpl. rewrite A. 
-  apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. }
-  (* cast16signed *)
-  { econstructor; split.
-  eapply exec_straight_two. simpl;eauto. simpl;eauto. auto. auto.
-  split; intros; Simpl.
-  assert (A: Int.ltu (Int.repr 16) Int.iwordsize = true) by auto.
-  destruct (rs x0); auto; simpl. rewrite A; simpl. rewrite A. 
-  apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. }
-  (* addimm *)
-  { exploit (opimm32_correct Paddw Paddiw Val.add); auto. instantiate (1 := x0); eauto with asmgen.
-  intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen. }
-  (* andimm *)
-  { exploit (opimm32_correct Pandw Pandiw Val.and); auto. instantiate (1 := x0); eauto with asmgen.
-  intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen. }
-  (* orimm *)
-  exploit (opimm32_correct Porw Poriw Val.or); auto. instantiate (1 := x0); eauto with asmgen.
-  { intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen. }
-  (* xorimm *)
-  { exploit (opimm32_correct Pxorw Pxoriw Val.xor); auto. instantiate (1 := x0); eauto with asmgen.
-  intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen. }
-  (* shrximm *)
-  { destruct (Val.shrx (rs x0) (Vint n)) eqn:TOTAL; cbn.
-    {
-    exploit Val.shrx_shr_3; eauto. intros E; subst v.
-    destruct (Int.eq n Int.zero).
-  + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-    split; intros; Simpl. 
-  + destruct (Int.eq n Int.one).
-    * econstructor; split.
-      eapply exec_straight_step. simpl; reflexivity. auto.
-      eapply exec_straight_step. simpl; reflexivity. auto.
-      apply exec_straight_one. simpl; reflexivity. auto.
-      split; intros; Simpl.
-    * change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n).
-      econstructor; split.
-      eapply exec_straight_step. simpl; reflexivity. auto. 
-      eapply exec_straight_step. simpl; reflexivity. auto. 
-      eapply exec_straight_step. simpl; reflexivity. auto. 
-      apply exec_straight_one. simpl; reflexivity. auto. 
-      split; intros; Simpl.
-    }
-    destruct (Int.eq n Int.zero).
-  + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-    split; intros; Simpl. 
-  + destruct (Int.eq n Int.one).
-    * econstructor; split.
-      eapply exec_straight_step. simpl; reflexivity. auto.
-      eapply exec_straight_step. simpl; reflexivity. auto.
-      apply exec_straight_one. simpl; reflexivity. auto.
-      split; intros; Simpl.
-    * change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n).
-      econstructor; split.
-      eapply exec_straight_step. simpl; reflexivity. auto. 
-      eapply exec_straight_step. simpl; reflexivity. auto. 
-      eapply exec_straight_step. simpl; reflexivity. auto. 
-      apply exec_straight_one. simpl; reflexivity. auto. 
-      split; intros; Simpl. }
-  (* longofintu *)
-  { econstructor; split.
-  eapply exec_straight_three. simpl; eauto. simpl; eauto. simpl; eauto. auto. auto. auto.
-  split; intros; Simpl. destruct (rs x0); auto. simpl. 
-  assert (A: Int.ltu (Int.repr 32) Int64.iwordsize' = true) by auto.
-  rewrite A; simpl. rewrite A. apply Val.lessdef_same. f_equal.
-  rewrite cast32unsigned_from_cast32signed. apply Int64.zero_ext_shru_shl. compute; auto. }
-  (* addlimm *)
-  { exploit (opimm64_correct Paddl Paddil Val.addl); auto. instantiate (1 := x0); eauto with asmgen.
-  intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen. }
-  (* andimm *)
-  { exploit (opimm64_correct Pandl Pandil Val.andl); auto. instantiate (1 := x0); eauto with asmgen.
-  intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen. }
-  (* orimm *)
-  { exploit (opimm64_correct Porl Poril Val.orl); auto. instantiate (1 := x0); eauto with asmgen.
-  intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen. }
-  (* xorimm *)
-  { exploit (opimm64_correct Pxorl Pxoril Val.xorl); auto. instantiate (1 := x0); eauto with asmgen.
-  intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen. }
-  (* shrxlimm *)
-  { destruct (Val.shrxl (rs x0) (Vint n)) eqn:TOTAL.
-    {
-     exploit Val.shrxl_shrl_3; eauto. intros E; subst v.
-    destruct (Int.eq n Int.zero).
-  + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-    split; intros; Simpl. 
-  + destruct (Int.eq n Int.one).
-    * econstructor; split.
-      eapply exec_straight_step. simpl; reflexivity. auto.
-      eapply exec_straight_step. simpl; reflexivity. auto.
-      apply exec_straight_one. simpl; reflexivity. auto.
-      split; intros; Simpl.
-
-    * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n).
-      econstructor; split.
-      eapply exec_straight_step. simpl; reflexivity. auto. 
-      eapply exec_straight_step. simpl; reflexivity. auto. 
-      eapply exec_straight_step. simpl; reflexivity. auto. 
-      apply exec_straight_one. simpl; reflexivity. auto. 
-      split; intros; Simpl.
-    }
-    destruct (Int.eq n Int.zero).
-  + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-    split; intros; Simpl. 
-  + destruct (Int.eq n Int.one).
-    * econstructor; split.
-      eapply exec_straight_step. simpl; reflexivity. auto.
-      eapply exec_straight_step. simpl; reflexivity. auto.
-      apply exec_straight_one. simpl; reflexivity. auto.
-      split; intros; Simpl.
-
-    * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n).
-      econstructor; split.
-      eapply exec_straight_step. simpl; reflexivity. auto. 
-      eapply exec_straight_step. simpl; reflexivity. auto. 
-      eapply exec_straight_step. simpl; reflexivity. auto. 
-      apply exec_straight_one. simpl; reflexivity. auto. 
-      split; intros; Simpl. }
-  (* cond *)
-  { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
-     exists rs'; split. eexact A. eauto with asmgen. }
   (* Expanded instructions from RTL *)
   9,10,19,20:
     econstructor; split; try apply exec_straight_one; simpl; eauto;
diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v
index d55d94ad..33e2db61 100644
--- a/riscV/RTLpathSE_simplify.v
+++ b/riscV/RTLpathSE_simplify.v
@@ -847,6 +847,16 @@ Proof.
   destruct x; destruct y; simpl; auto. rewrite Float32.cmp_swap. auto.
 Qed.
 
+Remark cast32unsigned_from_cast32signed:
+  forall i, Int64.repr (Int.unsigned i) = Int64.zero_ext 32 (Int64.repr (Int.signed i)).
+Proof.
+  intros. apply Int64.same_bits_eq; intros. 
+  rewrite Int64.bits_zero_ext, !Int64.testbit_repr by tauto.
+  rewrite Int.bits_signed by tauto. fold (Int.testbit i i0).
+  change Int.zwordsize with 32.
+  destruct (zlt i0 32). auto. apply Int.bits_above. auto.
+Qed.
+
 (** * Intermediates lemmas on each expanded instruction *)
 
 Lemma simplify_ccomp_correct ge sp hst st c r r0 rs0 m0 v v0: forall