Asmcondexp branche useful to benchmark expansions

1 files changed, 695 insertions, 78 deletions

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;