Merge remote-tracking branch 'origin/riscv-still-asmcondexp' into riscv-work-fpinit-stillexp

3 files changed, 1088 insertions, 96 deletions

diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index 957166b6..4f9d008b 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -105,6 +105,8 @@ 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
@@ -130,6 +132,8 @@ 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
@@ -141,6 +145,66 @@ Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
   
 (** 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.
+ 
 Definition apply_bin_r0_r0r0lbl (optR0: option bool) (sem: ireg0 -> ireg0 -> label -> instruction) (r1 r2: ireg0) (lbl: label) :=
   match optR0 with
   | None => sem r1 r2 lbl
@@ -158,6 +222,59 @@ Definition apply_bin_r0_r0r0 (optR0: option bool) (sem: ireg0 -> ireg0 -> instru
 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 optR0, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2;
       OK (apply_bin_r0_r0r0lbl optR0 Pbeqw r1 r2 lbl :: k)
@@ -210,6 +327,133 @@ 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]. *)
   
@@ -523,6 +767,9 @@ 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
   | OEseqw optR0, a1 :: a2 :: nil =>
       do rd <- ireg_of res;
       do rs1 <- ireg_of a1;
diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v
index 6abad4ed..82c1917d 100644
--- a/riscV/Asmgenproof.v
+++ b/riscV/Asmgenproof.v
@@ -161,37 +161,165 @@ 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.
-  all:  destruct optR0 as [[]|]; 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 optR0 as [[]|]; TailNoLabel.
+- destruct optR0 as [[]|]; TailNoLabel.
+- destruct optR0 as [[]|]; TailNoLabel.
+- destruct optR0 as [[]|]; TailNoLabel.
+- destruct optR0 as [[]|]; TailNoLabel.
+- destruct optR0 as [[]|]; TailNoLabel.
+- destruct optR0 as [[]|]; TailNoLabel.
+- destruct optR0 as [[]|]; TailNoLabel.
+- destruct optR0 as [[]|]; TailNoLabel.
+- destruct optR0 as [[]|]; TailNoLabel.
+- destruct optR0 as [[]|]; TailNoLabel.
+- destruct optR0 as [[]|]; TailNoLabel.
+- destruct optR0 as [[]|]; TailNoLabel.
+- destruct optR0 as [[]|]; TailNoLabel.
+- destruct optR0 as [[]|]; TailNoLabel.
+- destruct optR0 as [[]|]; 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.
-  { 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. }
-  all: destruct optR0 as [[]|]; simpl; 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 optR0 as [[]|]; simpl; TailNoLabel.
+- destruct optR0 as [[]|]; simpl; TailNoLabel.
+- destruct optR0 as [[]|]; simpl; TailNoLabel.
+- destruct optR0 as [[]|]; simpl; TailNoLabel.
+- destruct optR0 as [[]|]; simpl; TailNoLabel.
+- destruct optR0 as [[]|]; simpl; TailNoLabel.
+- destruct optR0 as [[]|]; simpl; TailNoLabel.
+- destruct optR0 as [[]|]; simpl; TailNoLabel.
+- destruct optR0 as [[]|]; simpl; TailNoLabel.
+- destruct optR0 as [[]|]; simpl; TailNoLabel.
+- destruct optR0 as [[]|]; simpl; TailNoLabel.
+- destruct optR0 as [[]|]; simpl; TailNoLabel.
 Qed.
 
 Remark indexed_memory_access_label:
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index f0def29b..6d83cf5a 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -290,6 +290,102 @@ 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
@@ -321,84 +417,203 @@ 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.
-  (* Pbeqw / Cmp *)
-  { destruct optR0 as [[]|];
-    unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-    unfold zero32, Op.zero32 in *;
-    eexists; eexists; eauto; split; constructor; auto;
-    simpl in *.
-    + destruct (rs x); simpl in *; try congruence.
-      assert (HB: (Int.eq Int.zero i) = b) by congruence.
-      rewrite HB; destruct b; simpl; auto.
-    + destruct (rs x); simpl in *; try congruence.
-      assert (HB: (Int.eq i Int.zero) = b) by congruence.
-      rewrite HB; destruct b; simpl; auto.
-    + destruct (rs x); simpl in *; try congruence.
-      destruct (rs x0); try congruence.
-      assert (HB: (Int.eq i i0) = b) by congruence.
-      rewrite HB; destruct b; simpl; auto. }
-  (* Pbnew / Cmp *)
-  { destruct optR0 as [[]|];
-    unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-    unfold zero32, Op.zero32 in *;
-    eexists; eexists; eauto; split; constructor; auto;
-    simpl in *.
-    + destruct (rs x); simpl in *; try congruence.
-      assert (HB: negb (Int.eq Int.zero i) = b) by congruence.
-      rewrite HB; destruct b; simpl; auto.
-    + destruct (rs x); simpl in *; try congruence.
-      assert (HB: negb (Int.eq i Int.zero) = b) by congruence.
-      rewrite HB; destruct b; simpl; auto.
-    + destruct (rs x); simpl in *; try congruence.
-      destruct (rs x0); try congruence.
-      assert (HB: negb (Int.eq i i0) = b) by congruence.
-      rewrite HB; destruct b; simpl; auto. }
-  (* Pbeqw, Pbnew, Pbltw, Pbtluw, Pbgew, Pbgeuw / Cmpu *)
-  1-6:
-    destruct optR0 as [[]|];
-    unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-    unfold zero32, Op.zero32 in *;
-    eexists; eexists; eauto; split; constructor;
-    simpl in *; try rewrite EVAL'; auto.
-  (* Pbeql / Cmpl *)
-  { destruct optR0 as [[]|];
-    unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-    unfold zero64, Op.zero64 in *;
-    eexists; eexists; eauto; split; constructor;
-    simpl in *; auto.
-    + destruct (rs x); simpl in *; try congruence.
-      assert (HB: (Int64.eq Int64.zero i) = b) by congruence.
-      rewrite HB; destruct b; simpl; auto.
-    + destruct (rs x); simpl in *; try congruence.
-      assert (HB: (Int64.eq i Int64.zero) = b) by congruence.
-      rewrite HB; destruct b; simpl; auto.
-    + destruct (rs x); simpl in *; try congruence.
-      destruct (rs x0); try congruence.
-      assert (HB: (Int64.eq i i0) = b) by congruence.
-      rewrite HB; destruct b; simpl; auto. }
-  (* Pbnel / Cmpl *)
-  { destruct optR0 as [[]|];
-    unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-    unfold zero64, Op.zero64 in *;
-    eexists; eexists; eauto; split; constructor;
-    simpl in *; auto.
-    + destruct (rs x); simpl in *; try congruence.
-      assert (HB: negb (Int64.eq Int64.zero i) = b) by congruence.
-      rewrite HB; destruct b; simpl; auto.
-    + destruct (rs x); simpl in *; try congruence.
-      assert (HB: negb (Int64.eq i Int64.zero) = b) by congruence.
-      rewrite HB; destruct b; simpl; auto.
-    + destruct (rs x); simpl in *; try congruence.
-      destruct (rs x0); try congruence.
-      assert (HB: negb (Int64.eq i i0) = b) by congruence.
-      rewrite HB; destruct b; simpl; auto. }
-  (* Pbeql, Pbnel, Pbltl, Pbtlul, Pbgel, Pbgeul / Cmplu *)
-  1-6:
-    destruct optR0 as [[]|];
-    unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-    unfold zero64, Op.zero64 in *;
-    eexists; eexists; eauto; split; constructor;
-    simpl in *; try rewrite EVAL'; auto.
+  - 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 optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero32, Op.zero32 in *;
+  eexists; eexists; eauto; split; constructor; auto;
+  simpl in *.
+  + destruct (rs x); simpl in *; try congruence.
+    assert (HB: (Int.eq Int.zero i) = b) by congruence.
+    rewrite HB; destruct b; simpl; auto.
+  + destruct (rs x); simpl in *; try congruence.
+    assert (HB: (Int.eq i Int.zero) = b) by congruence.
+    rewrite HB; destruct b; simpl; auto.
+  + destruct (rs x); simpl in *; try congruence.
+    destruct (rs x0); try congruence.
+    assert (HB: (Int.eq i i0) = b) by congruence.
+    rewrite HB; destruct b; simpl; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero32, Op.zero32 in *;
+  eexists; eexists; eauto; split; constructor; auto;
+  simpl in *.
+  + destruct (rs x); simpl in *; try congruence.
+    assert (HB: negb (Int.eq Int.zero i) = b) by congruence.
+    rewrite HB; destruct b; simpl; auto.
+  + destruct (rs x); simpl in *; try congruence.
+    assert (HB: negb (Int.eq i Int.zero) = b) by congruence.
+    rewrite HB; destruct b; simpl; auto.
+  + destruct (rs x); simpl in *; try congruence.
+    destruct (rs x0); try congruence.
+    assert (HB: negb (Int.eq i i0) = b) by congruence.
+    rewrite HB; destruct b; simpl; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero32, Op.zero32 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero32, Op.zero32 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero32, Op.zero32 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero32, Op.zero32 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero32, Op.zero32 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero32, Op.zero32 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero64, Op.zero64 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; auto.
+  + destruct (rs x); simpl in *; try congruence.
+    assert (HB: (Int64.eq Int64.zero i) = b) by congruence.
+    rewrite HB; destruct b; simpl; auto.
+  + destruct (rs x); simpl in *; try congruence.
+    assert (HB: (Int64.eq i Int64.zero) = b) by congruence.
+    rewrite HB; destruct b; simpl; auto.
+  + destruct (rs x); simpl in *; try congruence.
+    destruct (rs x0); try congruence.
+    assert (HB: (Int64.eq i i0) = b) by congruence.
+    rewrite HB; destruct b; simpl; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero64, Op.zero64 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; auto.
+  + destruct (rs x); simpl in *; try congruence.
+    assert (HB: negb (Int64.eq Int64.zero i) = b) by congruence.
+    rewrite HB; destruct b; simpl; auto.
+  + destruct (rs x); simpl in *; try congruence.
+    assert (HB: negb (Int64.eq i Int64.zero) = b) by congruence.
+    rewrite HB; destruct b; simpl; auto.
+  + destruct (rs x); simpl in *; try congruence.
+    destruct (rs x0); try congruence.
+    assert (HB: negb (Int64.eq i i0) = b) by congruence.
+    rewrite HB; destruct b; simpl; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero64, Op.zero64 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero64, Op.zero64 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero64, Op.zero64 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero64, Op.zero64 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero64, Op.zero64 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero64, Op.zero64 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
 Qed.
 
 Lemma transl_cbranch_correct_true:
@@ -432,6 +647,405 @@ 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:
@@ -640,6 +1254,9 @@ Opaque Int.eq.
       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 *)
   7,8,15,16:
     econstructor; split; try apply exec_straight_one; simpl; eauto;