path: root/riscV/RTLpathSE_simplify.v

Require Import Coqlib Floats Values Memory.
Require Import Integers.
Require Import Op Registers.
Require Import RTLpathSE_theory.
Require Import RTLpathSE_simu_specs.
Require Import Asmgen Asmgenproof1.
Require Import Lia.

(** 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_optR0 (is_x0 is_inv: bool) : option bool :=
  if is_x0 then Some is_inv else None.

(** Functions to manage lists of "fake" values *)

Definition make_lhsv_cmp (is_inv: bool) (hv1 hv2: hsval) : list_hsval :=
  let (hvfirst, hvsec) := if is_inv then (hv1, hv2) else (hv2, hv1) in
  let lhsv := fScons hvfirst fSnil in
  fScons hvsec lhsv.

Definition make_lhsv_single (hvs: hsval) : list_hsval :=
  fScons hvs fSnil.

(** Expansion functions *)

(* Immediate loads *)

Definition load_hilo32 (hi lo: int) :=
  if Int.eq lo Int.zero then
    fSop (OEluiw hi) fSnil
  else
    let hvs := fSop (OEluiw hi) fSnil in
    let hl := make_lhsv_single hvs in
    fSop (Oaddimm lo) hl.

Definition load_hilo64 (hi lo: int64) :=
  if Int64.eq lo Int64.zero then
    fSop (OEluil hi) fSnil
  else
    let hvs := fSop (OEluil hi) fSnil in
    let hl := make_lhsv_single hvs in
    fSop (Oaddlimm lo) hl.

Definition loadimm32 (n: int) :=
  match make_immed32 n with
  | Imm32_single imm =>
      fSop (OEaddiwr0 imm) fSnil
  | Imm32_pair hi lo => load_hilo32 hi lo
  end.

Definition loadimm64 (n: int64) :=
  match make_immed64 n with
  | Imm64_single imm =>
      fSop (OEaddilr0 imm) fSnil
  | Imm64_pair hi lo => load_hilo64 hi lo
  | Imm64_large imm => fSop (OEloadli imm) fSnil
  end.

Definition opimm32 (hv1: hsval) (n: int) (op: operation) (opimm: int -> operation) :=
  match make_immed32 n with
  | Imm32_single imm =>
      let hl := make_lhsv_single hv1 in
      fSop (opimm imm) hl
  | Imm32_pair hi lo =>
      let hvs := load_hilo32 hi lo in
      let hl := make_lhsv_cmp false hv1 hvs in
      fSop op hl
  end.

Definition opimm64 (hv1: hsval) (n: int64) (op: operation) (opimm: int64 -> operation) :=
  match make_immed64 n with
  | Imm64_single imm =>
      let hl := make_lhsv_single hv1 in
      fSop (opimm imm) hl
  | Imm64_pair hi lo =>
      let hvs := load_hilo64 hi lo in
      let hl := make_lhsv_cmp false hv1 hvs in
      fSop op hl
  | Imm64_large imm =>
      let hvs := fSop (OEloadli imm) fSnil in
      let hl := make_lhsv_cmp false hv1 hvs in
      fSop op hl
  end.

Definition xorimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oxor OExoriw.
Definition sltimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltw None) OEsltiw.
Definition sltuimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltuw None) OEsltiuw.
Definition xorimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oxorl OExoril.
Definition sltimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltl None) OEsltil.
Definition sltuimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltul None) OEsltiul.

(* Comparisons intructions *)

Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
  match cmp with
  | Ceq => fSop (OEseqw optR0) lhsv
  | Cne => fSop (OEsnew optR0) lhsv
  | Clt | Cgt => fSop (OEsltw optR0) lhsv
  | Cle | Cge =>
      let hvs := (fSop (OEsltw optR0) lhsv) in
      let hl := make_lhsv_single hvs in
      fSop (OExoriw Int.one) hl
  end.

Definition cond_int32u (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
  match cmp with
  | Ceq => fSop (OEsequw optR0) lhsv
  | Cne => fSop (OEsneuw optR0) lhsv
  | Clt | Cgt => fSop (OEsltuw optR0) lhsv
  | Cle | Cge =>
      let hvs := (fSop (OEsltuw optR0) lhsv) in
      let hl := make_lhsv_single hvs in
      fSop (OExoriw Int.one) hl
  end.

Definition cond_int64s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
  match cmp with
  | Ceq => fSop (OEseql optR0) lhsv
  | Cne => fSop (OEsnel optR0) lhsv
  | Clt | Cgt => fSop (OEsltl optR0) lhsv
  | Cle | Cge =>
      let hvs := (fSop (OEsltl optR0) lhsv) in
      let hl := make_lhsv_single hvs in
      fSop (OExoriw Int.one) hl
  end.

Definition cond_int64u (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
  match cmp with
  | Ceq => fSop (OEsequl optR0) lhsv
  | Cne => fSop (OEsneul optR0) lhsv
  | Clt | Cgt => fSop (OEsltul optR0) lhsv
  | Cle | Cge =>
      let hvs := (fSop (OEsltul optR0) lhsv) in
      let hl := make_lhsv_single hvs in
      fSop (OExoriw Int.one) hl
  end.

Definition expanse_condimm_int32s (cmp: comparison) (hv1: hsval) (n: int) :=
  let is_inv := is_inv_cmp_int cmp in
  if Int.eq n Int.zero then
    let optR0 := make_optR0 true is_inv in
    let hl := make_lhsv_cmp is_inv hv1 hv1 in
    cond_int32s cmp hl optR0
  else
    match cmp with
    | Ceq | Cne =>
        let optR0 := make_optR0 true is_inv in
        let hvs := xorimm32 hv1 n in
        let hl := make_lhsv_cmp false hvs hvs in
        cond_int32s cmp hl optR0
    | Clt => sltimm32 hv1 n
    | Cle =>
        if Int.eq n (Int.repr Int.max_signed) then
          let hvs := loadimm32 Int.one in
          let hl := make_lhsv_cmp false hv1 hvs in
          fSop (OEmayundef false) hl
        else sltimm32 hv1 (Int.add n Int.one)
    | _ =>
        let optR0 := make_optR0 false is_inv in
        let hvs := loadimm32 n in
        let hl := make_lhsv_cmp is_inv hv1 hvs in
        cond_int32s cmp hl optR0
    end.

Definition expanse_condimm_int32u (cmp: comparison) (hv1: hsval) (n: int) :=
  let is_inv := is_inv_cmp_int cmp in
  if Int.eq n Int.zero then
    let optR0 := make_optR0 true is_inv in
    let hl := make_lhsv_cmp is_inv hv1 hv1 in
    cond_int32u cmp hl optR0
  else
    match cmp with
    | Clt => sltuimm32 hv1 n
    | _ =>
        let optR0 := make_optR0 false is_inv in
        let hvs := loadimm32 n in
        let hl := make_lhsv_cmp is_inv hv1 hvs in
        cond_int32u cmp hl optR0
    end.

Definition expanse_condimm_int64s (cmp: comparison) (hv1: hsval) (n: int64) :=
  let is_inv := is_inv_cmp_int cmp in
  if Int64.eq n Int64.zero then
    let optR0 := make_optR0 true is_inv in
    let hl := make_lhsv_cmp is_inv hv1 hv1 in
    cond_int64s cmp hl optR0
  else
    match cmp with
    | Ceq | Cne =>
        let optR0 := make_optR0 true is_inv in
        let hvs := xorimm64 hv1 n in
        let hl := make_lhsv_cmp false hvs hvs in
        cond_int64s cmp hl optR0
    | Clt => sltimm64 hv1 n
    | Cle =>
        if Int64.eq n (Int64.repr Int64.max_signed) then
          let hvs := loadimm32 Int.one in
          let hl := make_lhsv_cmp false hv1 hvs in
          fSop (OEmayundef true) hl
        else sltimm64 hv1 (Int64.add n Int64.one)
    | _ =>
        let optR0 := make_optR0 false is_inv in
        let hvs := loadimm64 n in
        let hl := make_lhsv_cmp is_inv hv1 hvs in
        cond_int64s cmp hl optR0
    end.

Definition expanse_condimm_int64u (cmp: comparison) (hv1: hsval) (n: int64) :=
  let is_inv := is_inv_cmp_int cmp in
  if Int64.eq n Int64.zero then
    let optR0 := make_optR0 true is_inv in
    let hl := make_lhsv_cmp is_inv hv1 hv1 in
    cond_int64u cmp hl optR0
  else
    match cmp with
    | Clt => sltuimm64 hv1 n
    | _ =>
        let optR0 := make_optR0 false is_inv in
        let hvs := loadimm64 n in
        let hl := make_lhsv_cmp is_inv hv1 hvs in
        cond_int64u cmp hl optR0
    end.

Definition cond_float (cmp: comparison) (lhsv: list_hsval) :=
  match cmp with
  | Ceq | Cne => fSop OEfeqd lhsv
  | Clt | Cgt => fSop OEfltd lhsv
  | Cle | Cge => fSop OEfled lhsv
  end.

Definition cond_single (cmp: comparison) (lhsv: list_hsval) :=
  match cmp with
  | Ceq | Cne => fSop OEfeqs lhsv
  | Clt | Cgt => fSop OEflts lhsv
  | Cle | Cge => fSop OEfles lhsv
  end.

Definition is_normal_cmp cmp :=
  match cmp with | Cne => false | _ => true end.

Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) :=
  let normal := is_normal_cmp cmp in
  let normal' := if cnot then negb normal else normal in
  let hvs := fn_cond cmp lhsv in
  let hl := make_lhsv_single hvs in
  if normal' then hvs else fSop (OExoriw Int.one) hl.

(* Branches instructions *)

Definition transl_cbranch_int32s (cmp: comparison) (optR0: option bool) :=
  match cmp with
  | Ceq => CEbeqw optR0
  | Cne => CEbnew optR0
  | Clt => CEbltw optR0
  | Cle => CEbgew optR0
  | Cgt => CEbltw optR0
  | Cge => CEbgew optR0
  end.

Definition transl_cbranch_int32u (cmp: comparison) (optR0: option bool) :=
  match cmp with
  | Ceq => CEbequw optR0
  | Cne => CEbneuw optR0
  | Clt => CEbltuw optR0
  | Cle => CEbgeuw optR0
  | Cgt => CEbltuw optR0
  | Cge => CEbgeuw optR0
  end.

Definition transl_cbranch_int64s (cmp: comparison) (optR0: option bool) :=
  match cmp with
  | Ceq => CEbeql optR0
  | Cne => CEbnel optR0
  | Clt => CEbltl optR0
  | Cle => CEbgel optR0
  | Cgt => CEbltl optR0
  | Cge => CEbgel optR0
  end.

Definition transl_cbranch_int64u (cmp: comparison) (optR0: option bool) :=
  match cmp with
  | Ceq => CEbequl optR0
  | Cne => CEbneul optR0
  | Clt => CEbltul optR0
  | Cle => CEbgeul optR0
  | Cgt => CEbltul optR0
  | Cge => CEbgeul optR0
  end.

Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) : (condition * list_hsval) :=
  let normal := is_normal_cmp cmp in
  let normal' := if cnot then negb normal else normal in
  let hvs := fn_cond cmp lhsv in
  let hl := make_lhsv_cmp false hvs hvs in
  if normal' then ((CEbnew (Some false)), hl) else ((CEbeqw (Some false)), hl).

(** Target op simplifications using "fake" values *)

Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval :=
  match op, lr with
  | Ocmp (Ccomp c), a1 :: a2 :: nil =>
      let hv1 := fsi_sreg_get hst a1 in
      let hv2 := fsi_sreg_get hst a2 in
      let is_inv := is_inv_cmp_int c in
      let optR0 := make_optR0 false is_inv in
      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
      Some (cond_int32s c lhsv optR0)
  | Ocmp (Ccompu c), a1 :: a2 :: nil =>
      let hv1 := fsi_sreg_get hst a1 in
      let hv2 := fsi_sreg_get hst a2 in
      let is_inv := is_inv_cmp_int c in
      let optR0 := make_optR0 false is_inv in
      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
      Some (cond_int32u c lhsv optR0)
  | Ocmp (Ccompimm c imm), a1 :: nil =>
      let hv1 := fsi_sreg_get hst a1 in
      Some (expanse_condimm_int32s c hv1 imm)
  | Ocmp (Ccompuimm c imm), a1 :: nil =>
      let hv1 := fsi_sreg_get hst a1 in
      Some (expanse_condimm_int32u c hv1 imm)
  | Ocmp (Ccompl c), a1 :: a2 :: nil =>
      let hv1 := fsi_sreg_get hst a1 in
      let hv2 := fsi_sreg_get hst a2 in
      let is_inv := is_inv_cmp_int c in
      let optR0 := make_optR0 false is_inv in
      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
      Some (cond_int64s c lhsv optR0)
  | Ocmp (Ccomplu c), a1 :: a2 :: nil =>
      let hv1 := fsi_sreg_get hst a1 in
      let hv2 := fsi_sreg_get hst a2 in
      let is_inv := is_inv_cmp_int c in
      let optR0 := make_optR0 false is_inv in
      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
      Some (cond_int64u c lhsv optR0)
  | Ocmp (Ccomplimm c imm), a1 :: nil =>
      let hv1 := fsi_sreg_get hst a1 in
      Some (expanse_condimm_int64s c hv1 imm)
  | Ocmp (Ccompluimm c imm), a1 :: nil =>
      let hv1 := fsi_sreg_get hst a1 in
      Some (expanse_condimm_int64u c hv1 imm)
  | Ocmp (Ccompf c), f1 :: f2 :: nil =>
      let hv1 := fsi_sreg_get hst f1 in
      let hv2 := fsi_sreg_get hst f2 in
      let is_inv := is_inv_cmp_float c in
      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
      Some (expanse_cond_fp false cond_float c lhsv)
  | Ocmp (Cnotcompf c), f1 :: f2 :: nil =>
      let hv1 := fsi_sreg_get hst f1 in
      let hv2 := fsi_sreg_get hst f2 in
      let is_inv := is_inv_cmp_float c in
      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
      Some (expanse_cond_fp true cond_float c lhsv)
  | Ocmp (Ccompfs c), f1 :: f2 :: nil =>
      let hv1 := fsi_sreg_get hst f1 in
      let hv2 := fsi_sreg_get hst f2 in
      let is_inv := is_inv_cmp_float c in
      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
      Some (expanse_cond_fp false cond_single c lhsv)
  | Ocmp (Cnotcompfs c), f1 :: f2 :: nil =>
      let hv1 := fsi_sreg_get hst f1 in
      let hv2 := fsi_sreg_get hst f2 in
      let is_inv := is_inv_cmp_float c in
      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
      Some (expanse_cond_fp true cond_single c lhsv)
  | Ofloatconst f, nil =>
      let bits_const := fSop (Olongconst (Float.to_bits f)) fSnil in
      let hl := make_lhsv_single bits_const in
      Some (fSop (Ofloat_of_bits) hl)
  | Osingleconst f, nil =>
      let bits_const := fSop (Ointconst (Float32.to_bits f)) fSnil in
      let hl := make_lhsv_single bits_const in
      Some (fSop (Osingle_of_bits) hl)
  | _, _ => None
  end.

Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg) : option (condition * list_hsval) :=
  match cond, args with
  | (Ccomp c), (a1 :: a2 :: nil) =>
      let is_inv := is_inv_cmp_int c in
      let cond := transl_cbranch_int32s c (make_optR0 false is_inv) in
      let hv1 := fsi_sreg_get prev a1 in
      let hv2 := fsi_sreg_get prev a2 in
      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
      Some (cond, lhsv)
  | (Ccompu c), (a1 :: a2 :: nil) =>
      let is_inv := is_inv_cmp_int c in
      let cond := transl_cbranch_int32u c (make_optR0 false is_inv) in
      let hv1 := fsi_sreg_get prev a1 in
      let hv2 := fsi_sreg_get prev a2 in
      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
      Some (cond, lhsv)
  | (Ccompimm c n), (a1 :: nil) =>
      let is_inv := is_inv_cmp_int c in
      let hv1 := fsi_sreg_get prev a1 in
      (if Int.eq n Int.zero then
        let lhsv := make_lhsv_cmp is_inv hv1 hv1 in
        let cond := transl_cbranch_int32s c (make_optR0 true is_inv) in
        Some (cond, lhsv)
      else
        let hvs := loadimm32 n in
        let lhsv := make_lhsv_cmp is_inv hv1 hvs in
        let cond := transl_cbranch_int32s c (make_optR0 false is_inv) in
        Some (cond, lhsv))
  | (Ccompuimm c n), (a1 :: nil) =>
      let is_inv := is_inv_cmp_int c in
      let hv1 := fsi_sreg_get prev a1 in
      (if Int.eq n Int.zero then
        let lhsv := make_lhsv_cmp is_inv hv1 hv1 in
        let cond := transl_cbranch_int32u c (make_optR0 true is_inv) in
        Some (cond, lhsv)
      else
        let hvs := loadimm32 n in
        let lhsv := make_lhsv_cmp is_inv hv1 hvs in
        let cond := transl_cbranch_int32u c (make_optR0 false is_inv) in
         Some (cond, lhsv))
  | (Ccompl c), (a1 :: a2 :: nil) =>
      let is_inv := is_inv_cmp_int c in
      let cond := transl_cbranch_int64s c (make_optR0 false is_inv) in
      let hv1 := fsi_sreg_get prev a1 in
      let hv2 := fsi_sreg_get prev a2 in
      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
      Some (cond, lhsv)
  | (Ccomplu c), (a1 :: a2 :: nil) =>
      let is_inv := is_inv_cmp_int c in
      let cond := transl_cbranch_int64u c (make_optR0 false is_inv) in
      let hv1 := fsi_sreg_get prev a1 in
      let hv2 := fsi_sreg_get prev a2 in
      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
      Some (cond, lhsv)
  | (Ccomplimm c n), (a1 :: nil) =>
      let is_inv := is_inv_cmp_int c in
      let hv1 := fsi_sreg_get prev a1 in
      (if Int64.eq n Int64.zero then
        let lhsv := make_lhsv_cmp is_inv hv1 hv1 in
        let cond := transl_cbranch_int64s c (make_optR0 true is_inv) in
        Some (cond, lhsv)
      else
        let hvs := loadimm64 n in
        let lhsv := make_lhsv_cmp is_inv hv1 hvs in
        let cond := transl_cbranch_int64s c (make_optR0 false is_inv) in
        Some (cond, lhsv))
  | (Ccompluimm c n), (a1 :: nil) =>
      let is_inv := is_inv_cmp_int c in
      let hv1 := fsi_sreg_get prev a1 in
      (if Int64.eq n Int64.zero then
        let lhsv := make_lhsv_cmp is_inv hv1 hv1 in
        let cond := transl_cbranch_int64u c (make_optR0 true is_inv) in
        Some (cond, lhsv)
      else
        let hvs := loadimm64 n in
        let lhsv := make_lhsv_cmp is_inv hv1 hvs in
        let cond := transl_cbranch_int64u c (make_optR0 false is_inv) in
        Some (cond, lhsv))
  | (Ccompf c), (f1 :: f2 :: nil) =>
      let hv1 := fsi_sreg_get prev f1 in
      let hv2 := fsi_sreg_get prev f2 in
      let is_inv := is_inv_cmp_float c in
      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
      Some (expanse_cbranch_fp false cond_float c lhsv)
  | (Cnotcompf c), (f1 :: f2 :: nil) =>
      let hv1 := fsi_sreg_get prev f1 in
      let hv2 := fsi_sreg_get prev f2 in
      let is_inv := is_inv_cmp_float c in
      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
      Some (expanse_cbranch_fp true cond_float c lhsv)
  | (Ccompfs c), (f1 :: f2 :: nil) =>
      let hv1 := fsi_sreg_get prev f1 in
      let hv2 := fsi_sreg_get prev f2 in
      let is_inv := is_inv_cmp_float c in
      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
      Some (expanse_cbranch_fp false cond_single c lhsv)
  | (Cnotcompfs c), (f1 :: f2 :: nil) =>
      let hv1 := fsi_sreg_get prev f1 in
      let hv2 := fsi_sreg_get prev f2 in
      let is_inv := is_inv_cmp_float c in
      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
      Some (expanse_cbranch_fp true cond_single c lhsv)
  | _, _ => None
   end.

(** 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.

(* 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.

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 omega.
Qed.

(* 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.

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.

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.

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 omega. auto.
  rewrite zlt_true by omega. 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); omega.
Qed.

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 omega. auto.
  rewrite zlt_true by omega. 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); omega.
Qed.

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.

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.

(* 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.

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.

(* 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.

(* 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.

(* 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.

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.

Lemma optbool_mktotal: forall v,
  Val.maketotal (option_map Val.of_bool v) =
  Val.of_optbool v.
Proof.
  intros.
  destruct v; simpl; auto.
Qed.

(* 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.

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.

(* Intermediates lemmas on each expansed instruction *)

Lemma simplify_ccomp_correct ge sp hst st c r r0 rs0 m0 v v0: forall
  (SREG: forall r: positive,
          hsi_sreg_eval ge sp hst r rs0 m0 =
          seval_sval ge sp (si_sreg st r) rs0 m0)
  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
  (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0),
  seval_sval ge sp
    (hsval_proj
       (cond_int32s c
          (make_lhsv_cmp (is_inv_cmp_int c) (fsi_sreg_get hst r)
             (fsi_sreg_get hst r0)) None)) rs0 m0 =
  Some (Val.of_optbool (Val.cmp_bool c v v0)).
Proof.
  intros.
  unfold cond_int32s in *; destruct c; simpl;
  erewrite !fsi_sreg_get_correct; eauto;
  rewrite OKv1, OKv2; trivial;
  unfold Val.cmp.
  - apply xor_neg_ltle_cmp.
  - 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.
    rewrite xor_neg_optb; trivial.
Qed.

Lemma simplify_ccompu_correct ge sp hst st c r r0 rs0 m m0 v v0: forall
  (SMEM : forall (m : mem) (b : Values.block) (ofs : Z),
           seval_smem ge sp (si_smem st) rs0 m0 = Some m ->
           Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
  (SREG: forall r: positive,
          hsi_sreg_eval ge sp hst r rs0 m0 =
          seval_sval ge sp (si_sreg st r) rs0 m0)
  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
  (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0)
  (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m),
  seval_sval ge sp
    (hsval_proj
       (cond_int32u c
          (make_lhsv_cmp (is_inv_cmp_int c) (fsi_sreg_get hst r)
             (fsi_sreg_get hst r0)) None)) rs0 m0 =
  Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer m) c v v0)).
Proof.
  intros.
  erewrite (cmpu_bool_valid_pointer_eq (Mem.valid_pointer m) (Mem.valid_pointer m0)).
  2: eauto.
  unfold cond_int32u in *; destruct c; simpl;
  erewrite !fsi_sreg_get_correct; eauto;
  rewrite OKv1, OKv2; trivial;
  unfold Val.cmpu.
  - apply xor_neg_ltle_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.
    rewrite xor_neg_optb; trivial.
Qed.

Lemma simplify_ccompimm_correct ge sp hst st c r n rs0 m m0 v: forall
  (SMEM : forall (m : mem) (b : Values.block) (ofs : Z),
           seval_smem ge sp (si_smem st) rs0 m0 = Some m ->
           Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
  (SREG: forall r: positive,
          hsi_sreg_eval ge sp hst r rs0 m0 =
          seval_sval ge sp (si_sreg st r) rs0 m0)
  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
  (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m),
  seval_sval ge sp
    (hsval_proj (expanse_condimm_int32s c (fsi_sreg_get hst r) n)) rs0 m0 =
  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 erewrite !fsi_sreg_get_correct; eauto;
  try rewrite 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 erewrite fSop_correct; eauto; simpl;
    try erewrite !fsi_sreg_get_correct; eauto;
    try rewrite OKv1;
    try rewrite OK2;
    try rewrite (Int.add_commut _ Int.zero), Int.add_zero_l in H; subst;
    unfold Val.cmp, may_undef_int, 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 ge sp hst st c r n rs0 m m0 v: forall
  (SMEM : forall (m : mem) (b : Values.block) (ofs : Z),
           seval_smem ge sp (si_smem st) rs0 m0 = Some m ->
           Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
  (SREG: forall r: positive,
          hsi_sreg_eval ge sp hst r rs0 m0 =
          seval_sval ge sp (si_sreg st r) rs0 m0)
  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
  (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m),
  seval_sval ge sp
    (hsval_proj (expanse_condimm_int32u c (fsi_sreg_get hst r) n)) rs0 m0 =
  Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer m) c v (Vint n))).
Proof.
  intros.
  assert (HMEM: Val.cmpu_bool (Mem.valid_pointer m) c v (Vint n) =
          Val.cmpu_bool (Mem.valid_pointer m0) c v (Vint n)).
  erewrite (cmpu_bool_valid_pointer_eq (Mem.valid_pointer m) (Mem.valid_pointer m0)); eauto.
  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 erewrite !fsi_sreg_get_correct; eauto;
  try rewrite 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;
    try erewrite fSop_correct; eauto; simpl;
    try erewrite !fsi_sreg_get_correct; eauto;
    try rewrite OKv1;
    try rewrite OK2;
    rewrite HMEM;
    unfold may_undef_int, 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 ge sp hst st c r r0 rs0 m0 v v0: forall
  (SREG: forall r: positive,
          hsi_sreg_eval ge sp hst r rs0 m0 =
          seval_sval ge sp (si_sreg st r) rs0 m0)
  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
  (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0),
  seval_sval ge sp
    (hsval_proj
       (cond_int64s c
          (make_lhsv_cmp (is_inv_cmp_int c) (fsi_sreg_get hst r)
             (fsi_sreg_get hst r0)) None)) rs0 m0 =
  Some (Val.of_optbool (Val.cmpl_bool c v v0)).
Proof.
  intros.
  unfold cond_int64s in *; destruct c; simpl;
  erewrite !fsi_sreg_get_correct; eauto;
  rewrite OKv1, OKv2; trivial;
  unfold Val.cmpl.
  1,2,3: rewrite optbool_mktotal; trivial.
  - apply xor_neg_ltle_cmpl.
  - replace (Clt) with (swap_comparison Cgt) by auto;
    rewrite Val.swap_cmpl_bool; trivial.
    rewrite optbool_mktotal; trivial.
  - apply xor_neg_ltge_cmpl.
Qed.

Lemma simplify_ccomplu_correct ge sp hst st c r r0 rs0 m m0 v v0: forall
  (SMEM : forall (m : mem) (b : Values.block) (ofs : Z),
           seval_smem ge sp (si_smem st) rs0 m0 = Some m ->
           Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
  (SREG: forall r: positive,
          hsi_sreg_eval ge sp hst r rs0 m0 =
          seval_sval ge sp (si_sreg st r) rs0 m0)
  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
  (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0)
  (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m),
  seval_sval ge sp
    (hsval_proj
       (cond_int64u c
          (make_lhsv_cmp (is_inv_cmp_int c) (fsi_sreg_get hst r)
             (fsi_sreg_get hst r0)) None)) rs0 m0 =
  Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer m) c v v0)).
Proof.
  intros.
  erewrite (cmplu_bool_valid_pointer_eq (Mem.valid_pointer m) (Mem.valid_pointer m0)).
  2: eauto.
  unfold cond_int64u in *; destruct c; simpl;
  erewrite !fsi_sreg_get_correct; eauto;
  rewrite OKv1, OKv2; trivial;
  unfold Val.cmplu.
  1,2,3: rewrite optbool_mktotal; trivial.
  - apply xor_neg_ltle_cmplu.
  - replace (Clt) with (swap_comparison Cgt) by auto;
    rewrite Val.swap_cmplu_bool; trivial.
    rewrite optbool_mktotal; trivial.
  - apply xor_neg_ltge_cmplu.
Qed.

Lemma simplify_ccomplimm_correct ge sp hst st c r n rs0 m m0 v: forall
  (SMEM : forall (m : mem) (b : Values.block) (ofs : Z),
           seval_smem ge sp (si_smem st) rs0 m0 = Some m ->
           Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
  (SREG: forall r: positive,
          hsi_sreg_eval ge sp hst r rs0 m0 =
          seval_sval ge sp (si_sreg st r) rs0 m0)
  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
  (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m),
  seval_sval ge sp
    (hsval_proj (expanse_condimm_int64s c (fsi_sreg_get hst r) n)) rs0 m0 =
  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 erewrite !fsi_sreg_get_correct; eauto;
  try rewrite 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;
    try erewrite fSop_correct; eauto; simpl;
    try erewrite !fsi_sreg_get_correct; eauto;
    try rewrite OKv1;
    try rewrite OK2;
    try rewrite (Int64.add_commut _ Int64.zero), Int64.add_zero_l in H; subst;
    try fold (Val.cmpl Clt v (Vlong imm));
    try rewrite xor_neg_ltge_cmpl; trivial;
    try rewrite xor_neg_ltle_cmpl; trivial;
    unfold Val.cmpl, Val.addl;
    try rewrite xorl_zero_eq_cmpl; trivial;
    try rewrite optbool_mktotal; trivial;
    unfold may_undef_int, zero32, Val.add; simpl;
    destruct v; auto.
  6,7,8:
      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)));
      try rewrite xor_neg_ltge_cmpl; trivial;
      try rewrite xor_neg_ltle_cmpl; trivial.
  all:
    try rewrite <- H;
    try apply cmpl_ltle_add_one; auto;
    try rewrite ltu_12_wordsize;
    try rewrite Int.add_commut, Int.add_zero_l in *;
    try rewrite Int64.add_commut, Int64.add_zero_l in *;
    simpl; try rewrite lt_maxsgn_false_long;
    try (rewrite <- H; trivial; fail);
    simpl; trivial.
Qed.

Lemma simplify_ccompluimm_correct ge sp hst st c r n rs0 m m0 v: forall
  (SMEM : forall (m : mem) (b : Values.block) (ofs : Z),
           seval_smem ge sp (si_smem st) rs0 m0 = Some m ->
           Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
  (SREG: forall r: positive,
          hsi_sreg_eval ge sp hst r rs0 m0 =
          seval_sval ge sp (si_sreg st r) rs0 m0)
  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
  (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m),
  seval_sval ge sp
    (hsval_proj (expanse_condimm_int64u c (fsi_sreg_get hst r) n)) rs0 m0 =
  Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer m) c v (Vlong n))).
Proof.
  intros.
  assert (HMEM: Val.cmplu_bool (Mem.valid_pointer m) c v (Vlong n) =
          Val.cmplu_bool (Mem.valid_pointer m0) c v (Vlong n)).
  erewrite (cmplu_bool_valid_pointer_eq (Mem.valid_pointer m) (Mem.valid_pointer m0)); eauto.
  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 erewrite !fsi_sreg_get_correct; eauto;
  try rewrite 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;
    try erewrite fSop_correct; eauto; simpl;
    try erewrite !fsi_sreg_get_correct; eauto;
    try rewrite OKv1;
    try rewrite OK2;
    rewrite HMEM.
  (* 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, may_undef_int, 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 (replace (Clt) with (swap_comparison Cgt) by auto;
    rewrite Val.swap_cmplu_bool; trivial; fail);
    try (replace (Clt) with (negate_comparison Cge) by auto;
    rewrite Val.negate_cmplu_bool; rewrite xor_neg_optb; trivial; fail);
    try rewrite optbool_mktotal; trivial.
  all:
    try destruct v; simpl; auto;
    try destruct (Archi.ptr64); simpl;
    try rewrite EQIMM;
    try rewrite HMEM; trivial;
    try destruct (Int64.ltu _ _);
    try rewrite <- xor_neg_ltge_cmplu; unfold Val.cmplu;
    try rewrite <- optbool_mktotal; trivial.
Qed.

Lemma simplify_ccompf_correct ge sp hst st c r r0 rs0 m0 v v0: forall
  (SREG: forall r: positive,
          hsi_sreg_eval ge sp hst r rs0 m0 =
          seval_sval ge sp (si_sreg st r) rs0 m0)
  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
  (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0),
  seval_sval ge sp
    (hsval_proj
       (expanse_cond_fp false cond_float c
          (make_lhsv_cmp (is_inv_cmp_float c) (fsi_sreg_get hst r)
             (fsi_sreg_get hst r0)))) rs0 m0 =
  Some (Val.of_optbool (Val.cmpf_bool c v v0)).
Proof.
  intros.
  unfold expanse_cond_fp in *; destruct c; simpl;
  erewrite !fsi_sreg_get_correct; eauto;
  rewrite OKv1, OKv2; trivial;
  unfold Val.cmpf.
  - apply xor_neg_eqne_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 ge sp hst st c r r0 rs0 m0 v v0: forall
  (SREG: forall r: positive,
          hsi_sreg_eval ge sp hst r rs0 m0 =
          seval_sval ge sp (si_sreg st r) rs0 m0)
  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
  (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0),
  seval_sval ge sp
    (hsval_proj
       (expanse_cond_fp true cond_float c
          (make_lhsv_cmp (is_inv_cmp_float c) (fsi_sreg_get hst r)
             (fsi_sreg_get hst r0)))) rs0 m0 =
  Some (Val.of_optbool (option_map negb (Val.cmpf_bool c v v0))).
Proof.
  intros.
  unfold expanse_cond_fp in *; destruct c; simpl;
  erewrite !fsi_sreg_get_correct; eauto;
  rewrite 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 ge sp hst st c r r0 rs0 m0 v v0: forall
  (SREG: forall r: positive,
          hsi_sreg_eval ge sp hst r rs0 m0 =
          seval_sval ge sp (si_sreg st r) rs0 m0)
  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
  (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0),
  seval_sval ge sp
    (hsval_proj
       (expanse_cond_fp false cond_single c
          (make_lhsv_cmp (is_inv_cmp_float c) (fsi_sreg_get hst r)
             (fsi_sreg_get hst r0)))) rs0 m0 =
  Some (Val.of_optbool (Val.cmpfs_bool c v v0)).
Proof.
  intros.
  unfold expanse_cond_fp in *; destruct c; simpl;
  erewrite !fsi_sreg_get_correct; eauto;
  rewrite OKv1, OKv2; trivial;
  unfold Val.cmpfs.
  - apply xor_neg_eqne_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 ge sp hst st c r r0 rs0 m0 v v0: forall
  (SREG: forall r: positive,
          hsi_sreg_eval ge sp hst r rs0 m0 =
          seval_sval ge sp (si_sreg st r) rs0 m0)
  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
  (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0),
  seval_sval ge sp
    (hsval_proj
       (expanse_cond_fp true cond_single c
          (make_lhsv_cmp (is_inv_cmp_float c) (fsi_sreg_get hst r)
             (fsi_sreg_get hst r0)))) rs0 m0 =
  Some (Val.of_optbool (option_map negb (Val.cmpfs_bool c v v0))).
Proof.
  intros.
  unfold expanse_cond_fp in *; destruct c; simpl;
  erewrite !fsi_sreg_get_correct; eauto;
  rewrite 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 op lr hst fsv ge sp rs0 m0 st args m: forall
   (H: target_op_simplify op lr hst = Some fsv)
   (REF: hsilocal_refines ge sp rs0 m0 hst st)
   (OK0: hsok_local ge sp rs0 m0 hst)
   (OK1: seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args)
   (OK2: seval_smem ge sp (si_smem st) rs0 m0 = Some m),
   seval_sval ge sp (hsval_proj fsv) rs0 m0 = eval_operation ge sp op args m.
Proof.
  unfold target_op_simplify; simpl.
  intros H (LREF & SREF & SREG & SMEM) ? ? ?.
  destruct op; try congruence.
  (* FP const expansions *)
  1,2:
    repeat (destruct lr; simpl; try congruence);
    simpl in OK1; inv OK1; inv H; simpl;
    try rewrite Float.of_to_bits;
    try rewrite Float32.of_to_bits; trivial.
  (* Ocmp expansions *)
  destruct cond; repeat (destruct lr; simpl; try congruence);
  simpl in OK1;
  try (destruct (seval_sval ge sp (si_sreg st r) rs0 m0) eqn:OKv1; try congruence);
  try (destruct (seval_sval ge sp (si_sreg st r0) rs0 m0) eqn:OKv2; try congruence);
  inv H; inv OK1.
  (* Ccomp *)
  - eapply simplify_ccomp_correct; eauto.
  (* Ccompu *)
  - eapply simplify_ccompu_correct; eauto.
  (* Ccompimm *)
  - eapply simplify_ccompimm_correct; eauto.
  (* Ccompuimm *)
  - eapply simplify_ccompuimm_correct; eauto.
  (* Ccompl *)
  - eapply simplify_ccompl_correct; eauto.
  (* Ccomplu *)
  - eapply simplify_ccomplu_correct; eauto.
  (* Ccomplimm *)
  - eapply simplify_ccomplimm_correct; eauto.
  (* Ccompluimm *)
  - eapply simplify_ccompluimm_correct; eauto.
  (* Ccompf *)
  - eapply simplify_ccompf_correct; eauto.
  (* Cnotcompf *)
  - eapply simplify_cnotcompf_correct; eauto.
  (* Ccompfs *)
  - eapply simplify_ccompfs_correct; eauto.
  (* Cnotcompfs *)
  - eapply simplify_cnotcompfs_correct; eauto.
Qed.

Lemma target_cbranch_expanse_correct hst c l ge sp rs0 m0 st c' l': forall
  (TARGET: target_cbranch_expanse hst c l = Some (c', l'))
  (LREF : hsilocal_refines ge sp rs0 m0 hst st)
  (OK: hsok_local ge sp rs0 m0 hst),
  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) ?.
  destruct c; try congruence;
  repeat (destruct l; simpl in H; try congruence).
  1,2,5,6:
    destruct c; inv H; simpl;
    try erewrite !fsi_sreg_get_correct; eauto;
    try (destruct (seval_smem ge sp (si_smem st) rs0 m0) eqn:OKmem; try congruence);
    try (destruct (seval_sval ge sp (si_sreg st r) rs0 m0) eqn:OKv1; try congruence);
    try (destruct (seval_sval ge sp (si_sreg st r0) rs0 m0) eqn:OKv2; try congruence);
    try replace (Cle) with (swap_comparison Cge) by auto;
    try replace (Clt) with (swap_comparison Cgt) by auto;
    try rewrite Val.swap_cmp_bool; trivial;
    try rewrite Val.swap_cmpu_bool; trivial;
    try rewrite Val.swap_cmpl_bool; trivial;
    try rewrite Val.swap_cmplu_bool; trivial.
  1,2,3,4:
    try destruct (Int.eq n Int.zero) eqn: EQIMM;
    try apply Int.same_if_eq in EQIMM;
    try destruct (Int64.eq n Int64.zero) eqn: EQIMM;
    try apply Int64.same_if_eq in EQIMM;
    destruct c; inv H; simpl;
    try erewrite !fsi_sreg_get_correct; eauto;
    try (destruct (seval_smem ge sp (si_smem st) rs0 m0) eqn:OKmem; try congruence);
    try (destruct (seval_sval ge sp (si_sreg st r) rs0 m0) eqn:OKv1; try congruence);
    try (destruct (seval_sval ge sp (si_sreg st r0) rs0 m0) eqn:OKv2; try congruence);
    unfold loadimm32, load_hilo32, Val.cmp, Val.cmpu, zero32;
    unfold loadimm64, load_hilo64, Val.cmpl, Val.cmplu, zero64;
    intros; try (specialize make_immed32_sound with (n);
    destruct (make_immed32 n) eqn:EQMKI); intros; simpl;
    intros; try (specialize make_immed64_sound with (n);
    destruct (make_immed64 n) eqn:EQMKI); intros; simpl;
    try rewrite EQLO; simpl;
    try destruct (Int.eq lo Int.zero) eqn:EQLO;
    try destruct (Int64.eq lo Int64.zero) eqn:EQLO;
    try apply Int.same_if_eq in EQLO; simpl; trivial;
    try apply Int64.same_if_eq in EQLO; simpl; trivial;
    unfold may_undef_int; 
    try erewrite !fsi_sreg_get_correct; eauto;
    try rewrite OKv1; simpl; trivial;
    try destruct v; try rewrite H;
    try rewrite ltu_12_wordsize; try rewrite EQLO;
    try rewrite Int.add_commut, Int.add_zero_l;
    try rewrite Int64.add_commut, Int64.add_zero_l;
    auto; simpl;
    try rewrite H in EQIMM;
    try rewrite EQLO in EQIMM;
    try rewrite Int.add_commut, Int.add_zero_l in EQIMM;
    try rewrite Int64.add_commut, Int64.add_zero_l in EQIMM;
    try rewrite EQIMM; simpl;
    try destruct (Archi.ptr64); trivial.

    1,2,3,4:
    destruct c; inv H; simpl;
    try erewrite !fsi_sreg_get_correct; eauto;
    try (destruct (seval_smem ge sp (si_smem st) rs0 m0) eqn:OKmem; try congruence);
    try (destruct (seval_sval ge sp (si_sreg st r) rs0 m0) eqn:OKv1; try congruence);
    try (destruct (seval_sval ge sp (si_sreg st r0) rs0 m0) eqn:OKv2; try congruence);
    unfold zero32, zero64, Val.cmpf, Val.cmpfs;
    destruct v, v0; simpl; trivial;
    try rewrite Float.cmp_ne_eq;
    try rewrite Float32.cmp_ne_eq;
    try rewrite <- Float.cmp_swap; simpl;
    try rewrite <- Float32.cmp_swap; simpl;
    try destruct (Float.cmp _ _); simpl;
    try destruct (Float32.cmp _ _); simpl;
    try rewrite Int.eq_true; simpl;
    try rewrite Int.eq_false; try apply Int.one_not_zero;
    simpl; trivial.
Qed.
Global Opaque target_op_simplify.
Global Opaque target_cbranch_expanse.