expansions btl proofs

1 files changed, 998 insertions, 1 deletions

diff --git a/riscV/BTL_SEsimplify.v b/riscV/BTL_SEsimplify.v
index f190e6d5..a4a2785a 120000..100644
--- a/riscV/BTL_SEsimplify.v
+++ b/riscV/BTL_SEsimplify.v
@@ -1 +1,998 @@
-../aarch64/BTL_SEsimplify.v
\ No newline at end of file
+Require Import Coqlib Floats Values Memory.
+Require Import Integers.
+Require Import Op Registers.
+Require Import BTL_SEtheory.
+Require Import BTL_SEsimuref.
+Require Import Asmgen Asmgenproof1.
+
+(** Useful functions for conditions/branches expansion *)
+
+Definition is_inv_cmp_int (cmp: comparison) : bool :=
+  match cmp with | Cle | Cgt => true | _ => false end.
+
+Definition is_inv_cmp_float (cmp: comparison) : bool :=
+  match cmp with | Cge | Cgt => true | _ => false end.
+
+Definition make_optR (is_x0 is_inv: bool) : option oreg :=
+  if is_x0 then
+    (if is_inv then Some (X0_L)
+    else Some (X0_R))
+  else None.
+
+(** Functions to manage lists of "fake" values *)
+
+Definition make_lfsv_cmp (is_inv: bool) (fsv1 fsv2: sval) : list_sval :=
+  let (fsvfirst, fsvsec) := if is_inv then (fsv1, fsv2) else (fsv2, fsv1) in
+  let lfsv := fScons fsvfirst fSnil in
+  fScons fsvsec lfsv.
+
+Definition make_lfsv_single (fsv: sval) : list_sval :=
+  fScons fsv fSnil.
+
+(** * Expansion functions *)
+
+(** ** Immediate loads *)
+
+Definition load_hilo32 (hi lo: int) :=
+  if Int.eq lo Int.zero then
+    fSop (OEluiw hi) fSnil
+  else
+    let fsv := fSop (OEluiw hi) fSnil in
+    let hl := make_lfsv_single fsv in
+    fSop (OEaddiw None lo) hl.
+
+Definition load_hilo64 (hi lo: int64) :=
+  if Int64.eq lo Int64.zero then
+    fSop (OEluil hi) fSnil
+  else
+    let fsv := fSop (OEluil hi) fSnil in
+    let hl := make_lfsv_single fsv in
+    fSop (OEaddil None lo) hl.
+
+Definition loadimm32 (n: int) :=
+  match make_immed32 n with
+  | Imm32_single imm =>
+      fSop (OEaddiw (Some X0_R) imm) fSnil
+  | Imm32_pair hi lo => load_hilo32 hi lo
+  end.
+
+Definition loadimm64 (n: int64) :=
+  match make_immed64 n with
+  | Imm64_single imm =>
+      fSop (OEaddil (Some X0_R) imm) fSnil
+  | Imm64_pair hi lo => load_hilo64 hi lo
+  | Imm64_large imm => fSop (OEloadli imm) fSnil
+  end.
+
+Definition opimm32 (hv1: sval) (n: int) (op: operation) (opimm: int -> operation) :=
+  match make_immed32 n with
+  | Imm32_single imm =>
+      let hl := make_lfsv_single hv1 in
+      fSop (opimm imm) hl
+  | Imm32_pair hi lo =>
+      let fsv := load_hilo32 hi lo in
+      let hl := make_lfsv_cmp false hv1 fsv in
+      fSop op hl
+  end.
+
+Definition opimm64 (hv1: sval) (n: int64) (op: operation) (opimm: int64 -> operation) :=
+  match make_immed64 n with
+  | Imm64_single imm =>
+      let hl := make_lfsv_single hv1 in
+      fSop (opimm imm) hl
+  | Imm64_pair hi lo =>
+      let fsv := load_hilo64 hi lo in
+      let hl := make_lfsv_cmp false hv1 fsv in
+      fSop op hl
+  | Imm64_large imm =>
+      let fsv := fSop (OEloadli imm) fSnil in
+      let hl := make_lfsv_cmp false hv1 fsv in
+      fSop op hl
+  end.
+
+Definition addimm32 (hv1: sval) (n: int) (or: option oreg) := opimm32 hv1 n Oadd (OEaddiw or).
+Definition andimm32 (hv1: sval) (n: int) := opimm32 hv1 n Oand OEandiw.
+Definition orimm32 (hv1: sval) (n: int) := opimm32 hv1 n Oor OEoriw.
+Definition xorimm32 (hv1: sval) (n: int) := opimm32 hv1 n Oxor OExoriw.
+Definition sltimm32 (hv1: sval) (n: int) := opimm32 hv1 n (OEsltw None) OEsltiw.
+Definition sltuimm32 (hv1: sval) (n: int) := opimm32 hv1 n (OEsltuw None) OEsltiuw.
+Definition addimm64 (hv1: sval) (n: int64) (or: option oreg) := opimm64 hv1 n Oaddl (OEaddil or).
+Definition andimm64 (hv1: sval) (n: int64) := opimm64 hv1 n Oandl OEandil.
+Definition orimm64 (hv1: sval) (n: int64) := opimm64 hv1 n Oorl OEoril.
+Definition xorimm64 (hv1: sval) (n: int64) := opimm64 hv1 n Oxorl OExoril.
+Definition sltimm64 (hv1: sval) (n: int64) := opimm64 hv1 n (OEsltl None) OEsltil.
+Definition sltuimm64 (hv1: sval) (n: int64) := opimm64 hv1 n (OEsltul None) OEsltiul.
+(** ** Comparisons intructions *)
+
+Definition cond_int32s (cmp: comparison) (lsv: list_sval) (optR: option oreg) :=
+  match cmp with
+  | Ceq => fSop (OEseqw optR) lsv
+  | Cne => fSop (OEsnew optR) lsv
+  | Clt | Cgt => fSop (OEsltw optR) lsv
+  | Cle | Cge =>
+      let fsv := (fSop (OEsltw optR) lsv) in
+      let lfsv := make_lfsv_single fsv in
+      fSop (OExoriw Int.one) lfsv
+  end.
+
+Definition cond_int32u (cmp: comparison) (lsv: list_sval) (optR: option oreg) :=
+  match cmp with
+  | Ceq => fSop (OEsequw optR) lsv
+  | Cne => fSop (OEsneuw optR) lsv
+  | Clt | Cgt => fSop (OEsltuw optR) lsv
+  | Cle | Cge =>
+      let fsv := (fSop (OEsltuw optR) lsv) in
+      let lfsv := make_lfsv_single fsv in
+      fSop (OExoriw Int.one) lfsv
+  end.
+
+Definition cond_int64s (cmp: comparison) (lsv: list_sval) (optR: option oreg) :=
+  match cmp with
+  | Ceq => fSop (OEseql optR) lsv
+  | Cne => fSop (OEsnel optR) lsv
+  | Clt | Cgt => fSop (OEsltl optR) lsv
+  | Cle | Cge =>
+      let fsv := (fSop (OEsltl optR) lsv) in
+      let lfsv := make_lfsv_single fsv in
+      fSop (OExoriw Int.one) lfsv
+  end.
+
+Definition cond_int64u (cmp: comparison) (lsv: list_sval) (optR: option oreg) :=
+  match cmp with
+  | Ceq => fSop (OEsequl optR) lsv
+  | Cne => fSop (OEsneul optR) lsv
+  | Clt | Cgt => fSop (OEsltul optR) lsv
+  | Cle | Cge =>
+      let fsv := (fSop (OEsltul optR) lsv) in
+      let lfsv := make_lfsv_single fsv in
+      fSop (OExoriw Int.one) lfsv
+  end.
+
+Definition expanse_condimm_int32s (cmp: comparison) (fsv1: sval) (n: int) :=
+  let is_inv := is_inv_cmp_int cmp in
+  if Int.eq n Int.zero then
+    let optR := make_optR true is_inv in
+    let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in
+    cond_int32s cmp lfsv optR
+  else
+    match cmp with
+    | Ceq | Cne =>
+        let optR := make_optR true is_inv in
+        let fsv := xorimm32 fsv1 n in
+        let lfsv := make_lfsv_cmp false fsv fsv in
+        cond_int32s cmp lfsv optR
+    | Clt => sltimm32 fsv1 n
+    | Cle =>
+        if Int.eq n (Int.repr Int.max_signed) then
+          let fsv := loadimm32 Int.one in
+          let lfsv := make_lfsv_cmp false fsv1 fsv in
+          fSop (OEmayundef MUint) lfsv
+        else sltimm32 fsv1 (Int.add n Int.one)
+    | _ =>
+        let optR := make_optR false is_inv in
+        let fsv := loadimm32 n in
+        let lfsv := make_lfsv_cmp is_inv fsv1 fsv in
+        cond_int32s cmp lfsv optR
+    end.
+
+Definition expanse_condimm_int32u (cmp: comparison) (fsv1: sval) (n: int) :=
+  let is_inv := is_inv_cmp_int cmp in
+  if Int.eq n Int.zero then
+    let optR := make_optR true is_inv in
+    let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in
+    cond_int32u cmp lfsv optR
+  else
+    match cmp with
+    | Clt => sltuimm32 fsv1 n
+    | _ =>
+        let optR := make_optR false is_inv in
+        let fsv := loadimm32 n in
+        let lfsv := make_lfsv_cmp is_inv fsv1 fsv in
+        cond_int32u cmp lfsv optR
+    end.
+
+Definition expanse_condimm_int64s (cmp: comparison) (fsv1: sval) (n: int64) :=
+  let is_inv := is_inv_cmp_int cmp in
+  if Int64.eq n Int64.zero then
+    let optR := make_optR true is_inv in
+    let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in
+    cond_int64s cmp lfsv optR
+  else
+    match cmp with
+    | Ceq | Cne =>
+        let optR := make_optR true is_inv in
+        let fsv := xorimm64 fsv1 n in
+        let lfsv := make_lfsv_cmp false fsv fsv in
+        cond_int64s cmp lfsv optR
+    | Clt => sltimm64 fsv1 n
+    | Cle =>
+        if Int64.eq n (Int64.repr Int64.max_signed) then
+          let fsv := loadimm32 Int.one in
+          let lfsv := make_lfsv_cmp false fsv1 fsv in
+          fSop (OEmayundef MUlong) lfsv
+        else sltimm64 fsv1 (Int64.add n Int64.one)
+    | _ =>
+        let optR := make_optR false is_inv in
+        let fsv := loadimm64 n in
+        let lfsv := make_lfsv_cmp is_inv fsv1 fsv in
+        cond_int64s cmp lfsv optR
+    end.
+
+Definition expanse_condimm_int64u (cmp: comparison) (fsv1: sval) (n: int64) :=
+  let is_inv := is_inv_cmp_int cmp in
+  if Int64.eq n Int64.zero then
+    let optR := make_optR true is_inv in
+    let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in
+    cond_int64u cmp lfsv optR
+  else
+    match cmp with
+    | Clt => sltuimm64 fsv1 n
+    | _ =>
+        let optR := make_optR false is_inv in
+        let fsv := loadimm64 n in
+        let lfsv := make_lfsv_cmp is_inv fsv1 fsv in
+        cond_int64u cmp lfsv optR
+    end.
+
+Definition cond_float (cmp: comparison) (lsv: list_sval) :=
+  match cmp with
+  | Ceq | Cne => fSop OEfeqd lsv
+  | Clt | Cgt => fSop OEfltd lsv
+  | Cle | Cge => fSop OEfled lsv
+  end.
+
+Definition cond_single (cmp: comparison) (lsv: list_sval) :=
+  match cmp with
+  | Ceq | Cne => fSop OEfeqs lsv
+  | Clt | Cgt => fSop OEflts lsv
+  | Cle | Cge => fSop OEfles lsv
+  end.
+
+Definition is_normal_cmp cmp :=
+  match cmp with | Cne => false | _ => true end.
+
+Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lsv: list_sval) :=
+  let normal := is_normal_cmp cmp in
+  let normal' := if cnot then negb normal else normal in
+  let fsv := fn_cond cmp lsv in
+  let lfsv := make_lfsv_single fsv in
+  if normal' then fsv else fSop (OExoriw Int.one) lfsv.
+
+(** Target op simplifications using "fake" values *)
+
+Definition target_op_simplify (op: operation) (lr: list reg) (hrs: ristate): option sval :=
+  match op, lr with
+  | Ocmp (Ccomp c), a1 :: a2 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      let fsv2 := ris_sreg_get hrs a2 in
+      let is_inv := is_inv_cmp_int c in
+      let optR := make_optR false is_inv in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (cond_int32s c lfsv optR)
+  | Ocmp (Ccompu c), a1 :: a2 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      let fsv2 := ris_sreg_get hrs a2 in
+      let is_inv := is_inv_cmp_int c in
+      let optR := make_optR false is_inv in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (cond_int32u c lfsv optR)
+  | Ocmp (Ccompimm c imm), a1 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      Some (expanse_condimm_int32s c fsv1 imm)
+  | Ocmp (Ccompuimm c imm), a1 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      Some (expanse_condimm_int32u c fsv1 imm)
+  | Ocmp (Ccompl c), a1 :: a2 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      let fsv2 := ris_sreg_get hrs a2 in
+      let is_inv := is_inv_cmp_int c in
+      let optR := make_optR false is_inv in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (cond_int64s c lfsv optR)
+  | Ocmp (Ccomplu c), a1 :: a2 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      let fsv2 := ris_sreg_get hrs a2 in
+      let is_inv := is_inv_cmp_int c in
+      let optR := make_optR false is_inv in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (cond_int64u c lfsv optR)
+  | Ocmp (Ccomplimm c imm), a1 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      Some (expanse_condimm_int64s c fsv1 imm)
+  | Ocmp (Ccompluimm c imm), a1 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      Some (expanse_condimm_int64u c fsv1 imm)
+  | Ocmp (Ccompf c), f1 :: f2 :: nil =>
+      let fsv1 := ris_sreg_get hrs f1 in
+      let fsv2 := ris_sreg_get hrs f2 in
+      let is_inv := is_inv_cmp_float c in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (expanse_cond_fp false cond_float c lfsv)
+  | Ocmp (Cnotcompf c), f1 :: f2 :: nil =>
+      let fsv1 := ris_sreg_get hrs f1 in
+      let fsv2 := ris_sreg_get hrs f2 in
+      let is_inv := is_inv_cmp_float c in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (expanse_cond_fp true cond_float c lfsv)
+  | Ocmp (Ccompfs c), f1 :: f2 :: nil =>
+      let fsv1 := ris_sreg_get hrs f1 in
+      let fsv2 := ris_sreg_get hrs f2 in
+      let is_inv := is_inv_cmp_float c in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (expanse_cond_fp false cond_single c lfsv)
+  | Ocmp (Cnotcompfs c), f1 :: f2 :: nil =>
+      let fsv1 := ris_sreg_get hrs f1 in
+      let fsv2 := ris_sreg_get hrs f2 in
+      let is_inv := is_inv_cmp_float c in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (expanse_cond_fp true cond_single c lfsv)
+  | _, _ => None
+  end.
+
+Definition target_cbranch_expanse (prev: ristate) (cond: condition) (args: list reg) : option (condition * list_sval) :=
+  None.
+
+(** * Auxiliary lemmas on comparisons *)
+
+(** ** Signed ints *)
+
+Lemma xor_neg_ltle_cmp: forall v1 v2,
+  Some (Val.xor (Val.cmp Clt v1 v2) (Vint Int.one)) =
+  Some (Val.of_optbool (Val.cmp_bool Cle v2 v1)).
+Proof.
+  intros. eapply f_equal.
+  destruct v1, v2; simpl; try congruence.
+  unfold Val.cmp; simpl;
+  try rewrite Int.eq_sym;
+  try destruct (Int.eq _ _); try destruct (Int.lt _ _) eqn:ELT ; simpl;
+  try rewrite Int.xor_one_one; try rewrite Int.xor_zero_one;
+  auto.
+Qed.
+Local Hint Resolve xor_neg_ltle_cmp: core.
+
+(** ** Unsigned ints *)
+
+Lemma xor_neg_ltle_cmpu: forall mptr v1 v2,
+  Some (Val.xor (Val.cmpu (Mem.valid_pointer mptr) Clt v1 v2) (Vint Int.one)) =
+  Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer mptr) Cle v2 v1)).
+Proof.
+  intros. eapply f_equal.
+  destruct v1, v2; simpl; try congruence.
+  unfold Val.cmpu; simpl;
+  try rewrite Int.eq_sym;
+  try destruct (Int.eq _ _); try destruct (Int.ltu _ _) eqn:ELT ; simpl;
+  try rewrite Int.xor_one_one; try rewrite Int.xor_zero_one;
+  auto.
+  1,2:
+    unfold Val.cmpu, Val.cmpu_bool;
+    destruct Archi.ptr64; try destruct (_ && _); try destruct (_ || _);
+    try destruct (eq_block _ _); auto.
+  unfold Val.cmpu, Val.cmpu_bool; simpl;
+  destruct Archi.ptr64; try destruct (_ || _); simpl; auto;
+  destruct (eq_block b b0); destruct (eq_block b0 b);
+  try congruence;
+  try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _);
+  simpl; auto;
+  repeat destruct (_ && _); simpl; auto.
+Qed.
+Local Hint Resolve xor_neg_ltle_cmpu: core.
+
+Remark ltu_12_wordsize:
+  Int.ltu (Int.repr 12) Int.iwordsize = true.
+Proof.
+  unfold Int.iwordsize, Int.zwordsize. simpl.
+  unfold Int.ltu. apply zlt_true.
+  rewrite !Int.unsigned_repr; try cbn; try lia.
+Qed.
+Local Hint Resolve ltu_12_wordsize: core.
+
+(** ** Signed longs *)
+
+Lemma xor_neg_ltle_cmpl: forall v1 v2,
+  Some (Val.xor (Val.maketotal (Val.cmpl Clt v1 v2)) (Vint Int.one)) =
+  Some (Val.of_optbool (Val.cmpl_bool Cle v2 v1)).
+Proof.
+  intros. eapply f_equal.
+  destruct v1, v2; simpl; try congruence.
+  destruct (Int64.lt _ _); auto.
+Qed.
+Local Hint Resolve xor_neg_ltle_cmpl: core.
+
+Lemma xor_neg_ltge_cmpl: forall v1 v2,
+  Some (Val.xor (Val.maketotal (Val.cmpl Clt v1 v2)) (Vint Int.one)) =
+  Some (Val.of_optbool (Val.cmpl_bool Cge v1 v2)).
+Proof.
+  intros. eapply f_equal.
+  destruct v1, v2; simpl; try congruence.
+  destruct (Int64.lt _ _); auto.
+Qed.
+Local Hint Resolve xor_neg_ltge_cmpl: core.
+
+Lemma xorl_zero_eq_cmpl: forall c v1 v2,
+  c = Ceq \/ c = Cne ->
+  Some
+    (Val.maketotal
+     (option_map Val.of_bool
+       (Val.cmpl_bool c (Val.xorl v1 v2) (Vlong Int64.zero)))) =
+  Some (Val.of_optbool (Val.cmpl_bool c v1 v2)).
+Proof.
+  intros. destruct c; inv H; try discriminate;
+  destruct v1, v2; simpl; auto;
+  destruct (Int64.eq i i0) eqn:EQ0.
+  1,3:
+    apply Int64.same_if_eq in EQ0; subst;
+    rewrite Int64.xor_idem;
+    rewrite Int64.eq_true; trivial.
+  1,2:
+    destruct (Int64.eq (Int64.xor i i0) Int64.zero) eqn:EQ1; simpl; try congruence;
+    rewrite Int64.xor_is_zero in EQ1; congruence.
+Qed.
+Local Hint Resolve xorl_zero_eq_cmpl: core.
+
+Lemma cmp_ltle_add_one: forall v n,
+  Int.eq n (Int.repr Int.max_signed) = false ->
+  Some (Val.of_optbool (Val.cmp_bool Clt v (Vint (Int.add n Int.one)))) =
+  Some (Val.of_optbool (Val.cmp_bool Cle v (Vint n))).
+Proof.
+  intros v n EQMAX. unfold Val.cmp_bool; destruct v; 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 lia. auto.
+  rewrite zlt_true by lia. auto.
+  rewrite Int.add_signed. symmetry; apply Int.signed_repr. 
+  specialize (Int.eq_spec n (Int.repr Int.max_signed)).
+  rewrite EQMAX; simpl; intros.
+  assert (Int.signed n <> Int.max_signed).
+  { red; intros E. elim H. rewrite <- (Int.repr_signed n). rewrite E. auto. }
+  generalize (Int.signed_range n); lia.
+Qed.
+Local Hint Resolve cmp_ltle_add_one: core.
+
+Lemma cmpl_ltle_add_one: forall v n,
+  Int64.eq n (Int64.repr Int64.max_signed) = false ->
+  Some (Val.of_optbool (Val.cmpl_bool Clt v (Vlong (Int64.add n Int64.one)))) =
+  Some (Val.of_optbool (Val.cmpl_bool Cle v (Vlong n))).
+Proof.
+  intros v n EQMAX. unfold Val.cmpl_bool; destruct v; 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 lia. auto.
+  rewrite zlt_true by lia. auto.
+  rewrite Int64.add_signed. symmetry; apply Int64.signed_repr. 
+  specialize (Int64.eq_spec n (Int64.repr Int64.max_signed)).
+  rewrite EQMAX; simpl; intros.
+  assert (Int64.signed n <> Int64.max_signed).
+  { red; intros E. elim H. rewrite <- (Int64.repr_signed n). rewrite E. auto. }
+  generalize (Int64.signed_range n); lia.
+Qed.
+Local Hint Resolve cmpl_ltle_add_one: core.
+
+Remark lt_maxsgn_false_int: forall i,
+  Int.lt (Int.repr Int.max_signed) i = false.
+Proof.
+  intros; unfold Int.lt.
+  specialize  Int.signed_range with i; intros.
+  rewrite zlt_false; auto. destruct H.
+  rewrite Int.signed_repr; try (cbn; lia).
+  apply Z.le_ge. trivial.
+Qed.
+Local Hint Resolve lt_maxsgn_false_int: core.
+
+Remark lt_maxsgn_false_long: forall i,
+  Int64.lt (Int64.repr Int64.max_signed) i = false.
+Proof.
+  intros; unfold Int64.lt.
+  specialize  Int64.signed_range with i; intros.
+  rewrite zlt_false; auto. destruct H.
+  rewrite Int64.signed_repr; try (cbn; lia).
+  apply Z.le_ge. trivial.
+Qed.
+Local Hint Resolve lt_maxsgn_false_long: core.
+
+(** ** Unsigned longs *)
+
+Lemma xor_neg_ltle_cmplu: forall mptr v1 v2,
+  Some (Val.xor (Val.maketotal (Val.cmplu (Mem.valid_pointer mptr) Clt v1 v2)) (Vint Int.one)) =
+  Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer mptr) Cle v2 v1)).
+Proof.
+  intros. eapply f_equal.
+  destruct v1, v2; simpl; try congruence.
+  destruct (Int64.ltu _ _); auto.
+  1,2: unfold Val.cmplu; simpl; auto;
+  destruct (Archi.ptr64); simpl;
+  try destruct (eq_block _ _); simpl;
+  try destruct (_ && _); simpl;
+  try destruct (Ptrofs.cmpu _ _);
+  try destruct cmp; simpl; auto.
+  unfold Val.cmplu; simpl;
+  destruct Archi.ptr64; try destruct (_ || _); simpl; auto;
+  destruct (eq_block b b0); destruct (eq_block b0 b);
+  try congruence;
+  try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _);
+  simpl; auto;
+  repeat destruct (_ && _); simpl; auto.
+Qed.
+Local Hint Resolve xor_neg_ltle_cmplu: core.
+
+Lemma xor_neg_ltge_cmplu: forall mptr v1 v2,
+  Some (Val.xor (Val.maketotal (Val.cmplu (Mem.valid_pointer mptr) Clt v1 v2)) (Vint Int.one)) =
+  Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer mptr) Cge v1 v2)).
+Proof.
+  intros. eapply f_equal.
+  destruct v1, v2; simpl; try congruence.
+  destruct (Int64.ltu _ _); auto.
+  1,2: unfold Val.cmplu; simpl; auto;
+  destruct (Archi.ptr64); simpl;
+  try destruct (eq_block _ _); simpl;
+  try destruct (_ && _); simpl;
+  try destruct (Ptrofs.cmpu _ _);
+  try destruct cmp; simpl; auto.
+  unfold Val.cmplu; simpl;
+  destruct Archi.ptr64; try destruct (_ || _); simpl; auto;
+  destruct (eq_block b b0); destruct (eq_block b0 b);
+  try congruence;
+  try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _);
+  simpl; auto;
+  repeat destruct (_ && _); simpl; auto.
+Qed.
+Local Hint Resolve xor_neg_ltge_cmplu: core.
+
+(** ** Floats *)
+
+Lemma xor_neg_eqne_cmpf: forall v1 v2,
+  Some (Val.xor (Val.cmpf Ceq v1 v2) (Vint Int.one)) =
+  Some (Val.of_optbool (Val.cmpf_bool Cne v1 v2)).
+Proof.
+  intros. eapply f_equal.
+  destruct v1, v2; simpl; try congruence;
+  unfold Val.cmpf; simpl.
+  rewrite Float.cmp_ne_eq.
+  destruct (Float.cmp _ _ _); simpl; auto.
+Qed.
+Local Hint Resolve xor_neg_eqne_cmpf: core.
+
+(** ** Singles *)
+
+Lemma xor_neg_eqne_cmpfs: forall v1 v2,
+  Some (Val.xor (Val.cmpfs Ceq v1 v2) (Vint Int.one)) =
+  Some (Val.of_optbool (Val.cmpfs_bool Cne v1 v2)).
+Proof.
+  intros. eapply f_equal.
+  destruct v1, v2; simpl; try congruence;
+  unfold Val.cmpfs; simpl.
+  rewrite Float32.cmp_ne_eq.
+  destruct (Float32.cmp _ _ _); simpl; auto.
+Qed.
+Local Hint Resolve xor_neg_eqne_cmpfs: core.
+
+(** ** More useful lemmas *)
+
+Lemma xor_neg_optb: forall v,
+  Some (Val.xor (Val.of_optbool (option_map negb v))
+    (Vint Int.one)) = Some (Val.of_optbool v).
+Proof.
+  intros.
+  destruct v; simpl; trivial.
+  destruct b; simpl; auto.
+Qed.
+Local Hint Resolve xor_neg_optb: core.
+
+Lemma xor_neg_optb': forall v,
+  Some (Val.xor (Val.of_optbool v) (Vint Int.one)) =
+  Some (Val.of_optbool (option_map negb v)).
+Proof.
+  intros.
+  destruct v; simpl; trivial.
+  destruct b; simpl; auto.
+Qed.
+Local Hint Resolve xor_neg_optb': core.
+
+Lemma optbool_mktotal: forall v,
+  Val.maketotal (option_map Val.of_bool v) =
+  Val.of_optbool v.
+Proof.
+  intros.
+  destruct v; simpl; auto.
+Qed.
+Local Hint Resolve optbool_mktotal: core.
+
+(* TODO gourdinl move to common/Values ? *)
+Theorem swap_cmpf_bool:
+  forall c x y,
+  Val.cmpf_bool (swap_comparison c) x y = Val.cmpf_bool c y x.
+Proof.
+  destruct x; destruct y; simpl; auto. rewrite Float.cmp_swap. auto.
+Qed.
+Local Hint Resolve swap_cmpf_bool: core.
+
+Theorem swap_cmpfs_bool:
+  forall c x y,
+  Val.cmpfs_bool (swap_comparison c) x y = Val.cmpfs_bool c y x.
+Proof.
+  destruct x; destruct y; simpl; auto. rewrite Float32.cmp_swap. auto.
+Qed.
+Local Hint Resolve swap_cmpfs_bool: core.
+
+(** * Intermediates lemmas on each expanded instruction *)
+
+Lemma simplify_ccomp_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  c r r0 v v0: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (OKv1 : eval_sval ctx (st r) = Some v)
+  (OKv2 : eval_sval ctx (st r0) = Some v0),
+  eval_sval ctx
+    (cond_int32s c (make_lfsv_cmp (is_inv_cmp_int c) (hrs r) (hrs r0)) None) =
+  Some (Val.of_optbool (Val.cmp_bool c v v0)).
+Proof.
+  intros.
+  unfold cond_int32s in *; destruct c; simpl;
+  erewrite !REG_EQ, OKv1, OKv2; trivial;
+  unfold Val.cmp. eauto.
+  - replace (Clt) with (swap_comparison Cgt) by auto;
+    rewrite Val.swap_cmp_bool; trivial.
+  - replace (Clt) with (negate_comparison Cge) by auto;
+    rewrite Val.negate_cmp_bool; eauto.
+Qed.
+
+Lemma simplify_ccompu_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  c r r0 v v0: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (OKv1 : eval_sval ctx (st r) = Some v)
+  (OKv2 : eval_sval ctx (st r0) = Some v0),
+  eval_sval ctx
+    (cond_int32u c (make_lfsv_cmp (is_inv_cmp_int c) (hrs r) (hrs r0)) None) =
+  Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer (cm0 ctx)) c v v0)).
+Proof.
+  intros.
+  unfold cond_int32u in *; destruct c; simpl;
+  rewrite !REG_EQ, OKv1, OKv2; trivial;
+  unfold Val.cmpu.
+  - replace (Clt) with (swap_comparison Cgt) by auto;
+    rewrite Val.swap_cmpu_bool; trivial.
+  - replace (Clt) with (negate_comparison Cge) by auto;
+    rewrite Val.negate_cmpu_bool; eauto.
+Qed.
+
+Lemma simplify_ccompimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  c r v n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (OKv1 : eval_sval ctx (st r) = Some v),
+  eval_sval ctx (expanse_condimm_int32s c (hrs r) n) =
+  Some (Val.of_optbool (Val.cmp_bool c v (Vint n))).
+Proof.
+  intros.
+  unfold expanse_condimm_int32s, cond_int32s in *; destruct c;
+  intros; destruct (Int.eq n Int.zero) eqn:EQIMM; simpl;
+  try apply Int.same_if_eq in EQIMM; subst;
+  unfold loadimm32, sltimm32, xorimm32, opimm32, load_hilo32;
+  try rewrite !REG_EQ, OKv1;
+  unfold Val.cmp, zero32.
+  all:
+    try apply xor_neg_ltle_cmp; 
+    try apply xor_neg_ltge_cmp; trivial.
+  4: 
+    try destruct (Int.eq n (Int.repr Int.max_signed)) eqn:EQMAX; subst;
+    try apply Int.same_if_eq in EQMAX; subst; simpl.
+  4:
+    intros; try (specialize make_immed32_sound with (Int.one);
+    destruct (make_immed32 Int.one) eqn:EQMKI_A1); intros; simpl.
+  6:
+    intros; try (specialize make_immed32_sound with (Int.add n Int.one);
+    destruct (make_immed32 (Int.add n Int.one)) eqn:EQMKI_A2); intros; simpl.
+  1,2,3,8,9:
+    intros; try (specialize make_immed32_sound with (n);
+    destruct (make_immed32 n) eqn:EQMKI); intros; simpl.
+  all: 
+    try destruct (Int.eq lo Int.zero) eqn:EQLO32;
+    try apply Int.same_if_eq in EQLO32; subst;
+    try rewrite !REG_EQ, OKv1;
+    try rewrite (Int.add_commut _ Int.zero), Int.add_zero_l in H; subst; simpl;
+    unfold Val.cmp, eval_may_undef, zero32, Val.add; simpl;
+    destruct v; auto.
+  all:
+    try rewrite ltu_12_wordsize;
+    try rewrite <- H;
+    try (apply cmp_ltle_add_one; auto);
+    try rewrite Int.add_commut, Int.add_zero_l in *;
+    try (
+    simpl; trivial;
+    try rewrite Int.xor_is_zero;
+    try destruct (Int.lt _ _) eqn:EQLT; trivial;
+    try rewrite lt_maxsgn_false_int in EQLT;
+    simpl; trivial; try discriminate; fail).
+Qed.
+
+Lemma simplify_ccompuimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  c r v n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (OKv1 : eval_sval ctx (st r) = Some v),
+  eval_sval ctx (expanse_condimm_int32u c (hrs r) n) =
+  Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer (cm0 ctx)) c v (Vint n))).
+Proof.
+  intros.
+  unfold expanse_condimm_int32u, cond_int32u in *; destruct c;
+  intros; destruct (Int.eq n Int.zero) eqn:EQIMM; simpl;
+  try apply Int.same_if_eq in EQIMM; subst;
+  unfold loadimm32, sltuimm32, opimm32, load_hilo32;
+  try rewrite !REG_EQ, OKv1; trivial;
+  try rewrite xor_neg_ltle_cmpu;
+  unfold Val.cmpu, zero32.
+  all:
+    try (specialize make_immed32_sound with n;
+    destruct (make_immed32 n) eqn:EQMKI);
+    try destruct (Int.eq lo Int.zero) eqn:EQLO;
+    try apply Int.same_if_eq in EQLO; subst;
+    intros; subst; simpl;
+    try rewrite !REG_EQ, OKv1;
+    unfold eval_may_undef, Val.cmpu;
+    destruct v; simpl; auto;
+    try rewrite EQIMM; try destruct (Archi.ptr64) eqn:EQARCH; simpl;
+    try rewrite ltu_12_wordsize; trivial;
+    try rewrite Int.add_commut, Int.add_zero_l in *;
+    try destruct (Int.ltu _ _) eqn:EQLTU; simpl;
+    try rewrite EQLTU; simpl; try rewrite EQIMM;
+    try rewrite EQARCH; trivial.
+Qed.
+
+Lemma simplify_ccompl_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  c r r0 v v0: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (OKv1 : eval_sval ctx (st r) = Some v)
+  (OKv2 : eval_sval ctx (st r0) = Some v0),
+  eval_sval ctx
+    (cond_int64s c (make_lfsv_cmp (is_inv_cmp_int c) (hrs r) (hrs r0)) None) =
+  Some (Val.of_optbool (Val.cmpl_bool c v v0)).
+Proof.
+  intros.
+  unfold cond_int64s in *; destruct c; simpl;
+  rewrite !REG_EQ, OKv1, OKv2; trivial;
+  unfold Val.cmpl.
+  1,2,3: rewrite optbool_mktotal; trivial.
+  replace (Clt) with (swap_comparison Cgt) by auto;
+  rewrite Val.swap_cmpl_bool; trivial.
+  rewrite optbool_mktotal; trivial.
+Qed.
+
+Lemma simplify_ccomplu_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  c r r0 v v0: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (OKv1 : eval_sval ctx (st r) = Some v)
+  (OKv2 : eval_sval ctx (st r0) = Some v0),
+  eval_sval ctx
+    (cond_int64u c (make_lfsv_cmp (is_inv_cmp_int c) (hrs r) (hrs r0)) None) =
+  Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer (cm0 ctx)) c v v0)).
+Proof.
+  intros.
+  unfold cond_int64u in *; destruct c; simpl;
+  rewrite !REG_EQ, OKv1, OKv2; trivial;
+  unfold Val.cmplu.
+  1,2,3: rewrite optbool_mktotal; trivial; eauto.
+  replace (Clt) with (swap_comparison Cgt) by auto;
+  rewrite Val.swap_cmplu_bool; trivial.
+  rewrite optbool_mktotal; trivial.
+Qed.
+
+Lemma simplify_ccomplimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  c r v n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (OKv1 : eval_sval ctx (st r) = Some v),
+  eval_sval ctx (expanse_condimm_int64s c (hrs r) n) =
+  Some (Val.of_optbool (Val.cmpl_bool c v (Vlong n))).
+Proof.
+  intros.
+  unfold expanse_condimm_int64s, cond_int64s in *; destruct c;
+  intros; destruct (Int64.eq n Int64.zero) eqn:EQIMM; simpl;
+  try apply Int64.same_if_eq in EQIMM; subst;
+  unfold loadimm32, loadimm64, sltimm64, xorimm64, opimm64, load_hilo32, load_hilo64;
+  try rewrite !REG_EQ, OKv1;
+  unfold Val.cmpl, zero64.
+  all:
+    try apply xor_neg_ltle_cmpl; 
+    try apply xor_neg_ltge_cmpl;
+    try rewrite optbool_mktotal; trivial.
+  4: 
+    try destruct (Int64.eq n (Int64.repr Int64.max_signed)) eqn:EQMAX; subst;
+    try apply Int64.same_if_eq in EQMAX; subst; simpl.
+  4:
+    intros; try (specialize make_immed32_sound with (Int.one);
+    destruct (make_immed32 Int.one) eqn:EQMKI_A1); intros; simpl.
+  6:
+    intros; try (specialize make_immed64_sound with (Int64.add n Int64.one);
+    destruct (make_immed64 (Int64.add n Int64.one)) eqn:EQMKI_A2); intros; simpl.
+  1,2,3,9,10:
+    intros; try (specialize make_immed64_sound with (n);
+    destruct (make_immed64 n) eqn:EQMKI); intros; simpl.
+  all: 
+    try destruct (Int.eq lo Int.zero) eqn:EQLO32;
+    try apply Int.same_if_eq in EQLO32; subst;
+    try destruct (Int64.eq lo Int64.zero) eqn:EQLO64;
+    try apply Int64.same_if_eq in EQLO64; subst; simpl;
+    try rewrite !REG_EQ, OKv1;
+    try rewrite (Int64.add_commut _ Int64.zero), Int64.add_zero_l in H; subst;
+    unfold Val.cmpl, Val.addl;
+    try rewrite optbool_mktotal; trivial;
+    destruct v; auto.
+  all:
+    try rewrite <- optbool_mktotal; trivial;
+    try rewrite Int64.add_commut, Int64.add_zero_l in *;
+    try fold (Val.cmpl Clt (Vlong i) (Vlong imm));
+    try fold (Val.cmpl Clt (Vlong i) (Vlong (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12)))));
+    try fold (Val.cmpl Clt (Vlong i) (Vlong (Int64.add (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) lo))).
+  all:
+    try rewrite <- cmpl_ltle_add_one; auto;
+    try rewrite ltu_12_wordsize;
+    try rewrite Int.add_commut, Int.add_zero_l in *;
+    simpl; try rewrite lt_maxsgn_false_long;
+    try (rewrite <- H; trivial; fail);
+    simpl; trivial.
+Qed.
+
+Lemma simplify_ccompluimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  c r v n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (OKv1 : eval_sval ctx (st r) = Some v),
+  eval_sval ctx (expanse_condimm_int64u c (hrs r) n) =
+  Some (Val.of_optbool
+     (Val.cmplu_bool (Mem.valid_pointer (cm0 ctx)) c v (Vlong n))).
+Proof.
+  intros.
+  unfold expanse_condimm_int64u, cond_int64u in *; destruct c;
+  intros; destruct (Int64.eq n Int64.zero) eqn:EQIMM; simpl;
+  unfold loadimm64, sltuimm64, opimm64, load_hilo64;
+  try rewrite !REG_EQ, OKv1;
+  unfold Val.cmplu, zero64.
+  (* Simplify make immediate and decompose subcases *)
+  all:
+    try (specialize make_immed64_sound with n;
+    destruct (make_immed64 n) eqn:EQMKI);
+    try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl;
+    try rewrite !REG_EQ, OKv1.
+  (* Ceq, Cne, Clt = itself *)
+  all: intros; try apply Int64.same_if_eq in EQIMM; subst; trivial.
+  (* Cle = xor (Clt) *)
+  all: try apply xor_neg_ltle_cmplu; trivial.
+  (* Others subcases with swap/negation *)
+  all:
+    unfold Val.cmplu, eval_may_undef, zero64, Val.addl;
+    try apply Int64.same_if_eq in EQLO; subst;
+    try rewrite Int64.add_commut, Int64.add_zero_l in *; trivial;
+    try (rewrite <- xor_neg_ltle_cmplu; unfold Val.cmplu;
+    trivial; fail);
+    try rewrite optbool_mktotal; trivial.
+  all:
+    try destruct v; simpl; auto;
+    try destruct (Archi.ptr64); simpl;
+    try rewrite EQIMM;
+    try destruct (Int64.ltu _ _);
+    try rewrite <- optbool_mktotal; trivial.
+Qed.
+
+Lemma simplify_ccompf_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  c r r0 v v0: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (OKv1 : eval_sval ctx (st r) = Some v)
+  (OKv2 : eval_sval ctx (st r0) = Some v0),
+  eval_sval ctx
+    (expanse_cond_fp false cond_float c
+       (make_lfsv_cmp (is_inv_cmp_float c) (hrs r) (hrs r0))) =
+  Some (Val.of_optbool (Val.cmpf_bool c v v0)).
+Proof.
+  intros.
+  unfold expanse_cond_fp in *; destruct c; simpl;
+  rewrite !REG_EQ, OKv1, OKv2; trivial;
+  unfold Val.cmpf.
+  - replace (Clt) with (swap_comparison Cgt) by auto;
+    rewrite swap_cmpf_bool; trivial.
+  - replace (Cle) with (swap_comparison Cge) by auto;
+    rewrite swap_cmpf_bool; trivial.
+Qed.
+
+Lemma simplify_cnotcompf_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  c r r0 v v0: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (OKv1 : eval_sval ctx (st r) = Some v)
+  (OKv2 : eval_sval ctx (st r0) = Some v0),
+  eval_sval ctx
+    (expanse_cond_fp true cond_float c
+       (make_lfsv_cmp (is_inv_cmp_float c) (hrs r) (hrs r0))) =
+  Some (Val.of_optbool (option_map negb (Val.cmpf_bool c v v0))).
+Proof.
+  intros.
+  unfold expanse_cond_fp in *; destruct c; simpl;
+  rewrite !REG_EQ, OKv1, OKv2; trivial;
+  unfold Val.cmpf.
+  1,3,4: apply xor_neg_optb'.
+  all: destruct v, v0; simpl; trivial.
+  rewrite Float.cmp_ne_eq; rewrite negb_involutive; trivial.
+  1: replace (Clt) with (swap_comparison Cgt) by auto; rewrite <- Float.cmp_swap; simpl.
+  2: replace (Cle) with (swap_comparison Cge) by auto; rewrite <- Float.cmp_swap; simpl.
+  all: destruct (Float.cmp _ _ _); trivial.
+Qed.
+
+Lemma simplify_ccompfs_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  c r r0 v v0: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (OKv1 : eval_sval ctx (st r) = Some v)
+  (OKv2 : eval_sval ctx (st r0) = Some v0),  eval_sval ctx
+    (expanse_cond_fp false cond_single c
+       (make_lfsv_cmp (is_inv_cmp_float c) (hrs r) (hrs r0))) =
+  Some (Val.of_optbool (Val.cmpfs_bool c v v0)).
+Proof.
+  intros.
+  unfold expanse_cond_fp in *; destruct c; simpl;
+  rewrite !REG_EQ, OKv1, OKv2; trivial;
+  unfold Val.cmpfs.
+  - replace (Clt) with (swap_comparison Cgt) by auto;
+    rewrite swap_cmpfs_bool; trivial.
+  - replace (Cle) with (swap_comparison Cge) by auto;
+    rewrite swap_cmpfs_bool; trivial.
+Qed.
+
+Lemma simplify_cnotcompfs_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  c r r0 v v0: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (OKv1 : eval_sval ctx (st r) = Some v)
+  (OKv2 : eval_sval ctx (st r0) = Some v0),
+  eval_sval ctx
+    (expanse_cond_fp true cond_single c
+       (make_lfsv_cmp (is_inv_cmp_float c) (hrs r) (hrs r0))) =
+  Some (Val.of_optbool (option_map negb (Val.cmpfs_bool c v v0))).
+Proof.
+  intros.
+  unfold expanse_cond_fp in *; destruct c; simpl;
+  rewrite !REG_EQ, OKv1, OKv2; trivial;
+  unfold Val.cmpfs.
+  1,3,4: apply xor_neg_optb'.
+  all: destruct v, v0; simpl; trivial.
+  rewrite Float32.cmp_ne_eq; rewrite negb_involutive; trivial.
+  1: replace (Clt) with (swap_comparison Cgt) by auto; rewrite <- Float32.cmp_swap; simpl.
+  2: replace (Cle) with (swap_comparison Cge) by auto; rewrite <- Float32.cmp_swap; simpl.
+  all: destruct (Float32.cmp _ _ _); trivial.
+Qed.
+
+(* Main proof of simplification *)
+
+Lemma target_op_simplify_correct ctx op lr hrs fsv st args: forall
+   (H: target_op_simplify op lr hrs = Some fsv)
+   (REF: ris_refines ctx hrs st)
+   (OK0: ris_ok ctx hrs)
+   (OK1: eval_list_sval ctx (list_sval_inj (map (si_sreg st) lr)) = Some args),
+   eval_sval ctx fsv = eval_operation (cge ctx) (csp ctx) op args (cm0 ctx).
+Proof.
+  unfold target_op_simplify; simpl.
+  intros H ? ? ?; inv REF.
+  destruct op; try congruence.
+  (* Ocmp expansions *)
+  destruct cond; repeat (destruct lr; simpl; try congruence);
+  simpl in OK1;
+  try (destruct (eval_sval ctx (si_sreg st r)) eqn:OKv1; try congruence);
+  try (destruct (eval_sval ctx (si_sreg st r0)) eqn:OKv2; try congruence);
+  inv H; inv OK1.
+  - eapply simplify_ccomp_correct; eauto.
+  - eapply simplify_ccompu_correct; eauto.
+  - eapply simplify_ccompimm_correct; eauto.
+  - eapply simplify_ccompuimm_correct; eauto.
+  - eapply simplify_ccompl_correct; eauto.
+  - eapply simplify_ccomplu_correct; eauto.
+  - eapply simplify_ccomplimm_correct; eauto.
+  - eapply simplify_ccompluimm_correct; eauto.
+  - eapply simplify_ccompf_correct; eauto.
+  - eapply simplify_cnotcompf_correct; eauto.
+  - eapply simplify_ccompfs_correct; eauto.
+  - eapply simplify_cnotcompfs_correct; eauto.
+Qed.
+
+(*
+Lemma target_cbranch_expanse_correct hrs c l ge sp rs0 m0 st c' l': forall
+  (TARGET: target_cbranch_expanse hrs c l = Some (c', l'))
+  (LREF : hsilocal_refines ge sp rs0 m0 hrs st)
+  (OK: hsok_local ge sp rs0 m0 hrs),
+  seval_condition ge sp c' (hsval_list_proj l') (si_smem st) rs0 m0 =
+  seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0.
+Proof.
+  unfold target_cbranch_expanse, seval_condition; simpl.
+  intros H (LREF & SREF & SREG & SMEM) ?.
+  congruence.
+Qed.
+Global Opaque target_op_simplify.
+   Global Opaque target_cbranch_expanse.*)