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