path: root/riscV/BTL_SEsimplify.v

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 lfsv := make_lfsv_single fsv in
    fSop (OEaddiw None lo) lfsv.

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 lfsv := make_lfsv_single fsv in
    fSop (OEaddil None lo) lfsv.

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 (fsv1: sval) (n: int) (op: operation) (opimm: int -> operation) :=
  match make_immed32 n with
  | Imm32_single imm =>
      let lfsv := make_lfsv_single fsv1 in
      fSop (opimm imm) lfsv
  | Imm32_pair hi lo =>
      let fsv := load_hilo32 hi lo in
      let lfsv := make_lfsv_cmp false fsv1 fsv in
      fSop op lfsv
  end.

Definition opimm64 (fsv1: sval) (n: int64) (op: operation) (opimm: int64 -> operation) :=
  match make_immed64 n with
  | Imm64_single imm =>
      let lfsv := make_lfsv_single fsv1 in
      fSop (opimm imm) lfsv
  | Imm64_pair hi lo =>
      let fsv := load_hilo64 hi lo in
      let lfsv := make_lfsv_cmp false fsv1 fsv in
      fSop op lfsv
  | Imm64_large imm =>
      let fsv := fSop (OEloadli imm) fSnil in
      let lfsv := make_lfsv_cmp false fsv1 fsv in
      fSop op lfsv
  end.

Definition addimm32 (fsv1: sval) (n: int) (or: option oreg) := opimm32 fsv1 n Oadd (OEaddiw or).
Definition andimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n Oand OEandiw.
Definition orimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n Oor OEoriw.
Definition xorimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n Oxor OExoriw.
Definition sltimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n (OEsltw None) OEsltiw.
Definition sltuimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n (OEsltuw None) OEsltiuw.
Definition addimm64 (fsv1: sval) (n: int64) (or: option oreg) := opimm64 fsv1 n Oaddl (OEaddil or).
Definition andimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n Oandl OEandil.
Definition orimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n Oorl OEoril.
Definition xorimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n Oxorl OExoril.
Definition sltimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n (OEsltl None) OEsltil.
Definition sltuimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 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.

(** ** Branches instructions *)

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

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

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

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

Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lfsv: list_sval) : (condition * list_sval) :=
  let normal := is_normal_cmp cmp in
  let normal' := if cnot then negb normal else normal in
  let fsv := fn_cond cmp lfsv in
  let lfsv' := make_lfsv_cmp false fsv fsv in
  if normal' then ((CEbnew (Some X0_R)), lfsv') else ((CEbeqw (Some X0_R)), 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)
  | Ofloatconst f, nil =>
      let fsv := loadimm64 (Float.to_bits f) in
      let lfsv := make_lfsv_single fsv in
      Some (fSop (Ofloat_of_bits) lfsv)
  | Osingleconst f, nil =>
      let fsv := loadimm32 (Float32.to_bits f) in
      let lfsv := make_lfsv_single fsv in
      Some (fSop (Osingle_of_bits) lfsv)
  | Ointconst n, nil =>
      Some (loadimm32 n)
  | Olongconst n, nil =>
      Some (loadimm64 n)
  | Oaddimm n, a1 :: nil =>
      let fsv1 := ris_sreg_get hrs a1 in
      Some (addimm32 fsv1 n None)
  | Oaddlimm n, a1 :: nil =>
      let fsv1 := ris_sreg_get hrs a1 in
      Some (addimm64 fsv1 n None)
  | Oandimm n, a1 :: nil =>
      let fsv1 := ris_sreg_get hrs a1 in
      Some (andimm32 fsv1 n)
  | Oandlimm n, a1 :: nil =>
      let fsv1 := ris_sreg_get hrs a1 in
      Some (andimm64 fsv1 n)
  | Oorimm n, a1 :: nil =>
      let fsv1 := ris_sreg_get hrs a1 in
      Some (orimm32 fsv1 n)
  | Oorlimm n, a1 :: nil =>
      let fsv1 := ris_sreg_get hrs a1 in
      Some (orimm64 fsv1 n)
  | Oxorimm n, a1 :: nil =>
      let fsv1 := ris_sreg_get hrs a1 in
      Some (xorimm32 fsv1 n)
  | Oxorlimm n, a1 :: nil =>
      let fsv1 := ris_sreg_get hrs a1 in
      Some (xorimm64 fsv1 n)
  | Ocast8signed, a1 :: nil =>
      let fsv1 := ris_sreg_get hrs a1 in
      let lfsv := make_lfsv_single fsv1 in
      let fsv := fSop (Oshlimm (Int.repr 24)) lfsv in
      let hl' := make_lfsv_single fsv in
      Some (fSop (Oshrimm (Int.repr 24)) hl')
  | Ocast16signed, a1 :: nil =>
      let fsv1 := ris_sreg_get hrs a1 in
      let lfsv := make_lfsv_single fsv1 in
      let fsv := fSop (Oshlimm (Int.repr 16)) lfsv in
      let hl' := make_lfsv_single fsv in
      Some (fSop (Oshrimm (Int.repr 16)) hl')
  | Ocast32unsigned, a1 :: nil =>
      let fsv1 := ris_sreg_get hrs a1 in
      let lfsv := make_lfsv_single fsv1 in
      let cast32s_s := fSop Ocast32signed lfsv in
      let cast32s_l := make_lfsv_single cast32s_s in
      let sllil_s := fSop (Oshllimm (Int.repr 32)) cast32s_l in
      let sllil_l := make_lfsv_single sllil_s in
      Some (fSop (Oshrluimm (Int.repr 32)) sllil_l)
  | Oshrximm n, a1 :: nil =>
      let fsv1 := ris_sreg_get hrs a1 in
      let lfsv := make_lfsv_single fsv1 in
      if Int.eq n Int.zero then
        let lhl := make_lfsv_cmp false fsv1 fsv1 in
        Some (fSop (OEmayundef (MUshrx n)) lhl)
      else
        if Int.eq n Int.one then
          let srliw_s := fSop (Oshruimm (Int.repr 31)) lfsv in
          let srliw_l := make_lfsv_cmp false fsv1 srliw_s in
          let addw_s := fSop Oadd srliw_l in
          let addw_l := make_lfsv_single addw_s in
          let sraiw_s := fSop (Oshrimm Int.one) addw_l in
          let sraiw_l := make_lfsv_cmp false sraiw_s sraiw_s in
          Some (fSop (OEmayundef (MUshrx n)) sraiw_l)
        else 
          let sraiw_s := fSop (Oshrimm (Int.repr 31)) lfsv in
          let sraiw_l := make_lfsv_single sraiw_s in
          let srliw_s := fSop (Oshruimm (Int.sub Int.iwordsize n)) sraiw_l in
          let srliw_l := make_lfsv_cmp false fsv1 srliw_s in
          let addw_s := fSop Oadd srliw_l in
          let addw_l := make_lfsv_single addw_s in
          let sraiw_s' := fSop (Oshrimm n) addw_l in
          let sraiw_l' := make_lfsv_cmp false sraiw_s' sraiw_s' in
          Some (fSop (OEmayundef (MUshrx n)) sraiw_l')
  | Oshrxlimm n, a1 :: nil =>
      let fsv1 := ris_sreg_get hrs a1 in
      let lfsv := make_lfsv_single fsv1 in
      if Int.eq n Int.zero then
        let lhl := make_lfsv_cmp false fsv1 fsv1 in
        Some (fSop (OEmayundef (MUshrxl n)) lhl)
      else
        if Int.eq n Int.one then
          let srlil_s := fSop (Oshrluimm (Int.repr 63)) lfsv in
          let srlil_l := make_lfsv_cmp false fsv1 srlil_s in
          let addl_s := fSop Oaddl srlil_l in
          let addl_l := make_lfsv_single addl_s in
          let srail_s := fSop (Oshrlimm Int.one) addl_l in
          let srail_l := make_lfsv_cmp false srail_s srail_s in
          Some (fSop (OEmayundef (MUshrxl n)) srail_l)
        else
          let srail_s := fSop (Oshrlimm (Int.repr 63)) lfsv in
          let srail_l := make_lfsv_single srail_s in
          let srlil_s := fSop (Oshrluimm (Int.sub Int64.iwordsize' n)) srail_l in
          let srlil_l := make_lfsv_cmp false fsv1 srlil_s in
          let addl_s := fSop Oaddl srlil_l in
          let addl_l := make_lfsv_single addl_s in
          let srail_s' := fSop (Oshrlimm n) addl_l in
          let srail_l' := make_lfsv_cmp false srail_s' srail_s' in
          Some (fSop (OEmayundef (MUshrxl n)) srail_l')

  | _, _ => None
  end.

Definition target_cbranch_expanse (prev: ristate) (cond: condition) (args: list reg) : option (condition * list_sval) :=
  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_optR false is_inv) in
      let fsv1 := ris_sreg_get prev a1 in
      let fsv2 := ris_sreg_get prev a2 in
      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
      Some (cond, lfsv)
  | (Ccompu c), (a1 :: a2 :: nil) =>
      let is_inv := is_inv_cmp_int c in
      let cond := transl_cbranch_int32u c (make_optR false is_inv) in
      let fsv1 := ris_sreg_get prev a1 in
      let fsv2 := ris_sreg_get prev a2 in
      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
      Some (cond, lfsv)
  | (Ccompimm c n), (a1 :: nil) =>
      let is_inv := is_inv_cmp_int c in
      let fsv1 := ris_sreg_get prev a1 in
      (if Int.eq n Int.zero then
        let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in
        let cond := transl_cbranch_int32s c (make_optR true is_inv) in
        Some (cond, lfsv)
      else
        let fsv := loadimm32 n in
        let lfsv := make_lfsv_cmp is_inv fsv1 fsv in
        let cond := transl_cbranch_int32s c (make_optR false is_inv) in
        Some (cond, lfsv))
  | (Ccompuimm c n), (a1 :: nil) =>
      let is_inv := is_inv_cmp_int c in
      let fsv1 := ris_sreg_get prev a1 in
      (if Int.eq n Int.zero then
        let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in
        let cond := transl_cbranch_int32u c (make_optR true is_inv) in
        Some (cond, lfsv)
      else
        let fsv := loadimm32 n in
        let lfsv := make_lfsv_cmp is_inv fsv1 fsv in
        let cond := transl_cbranch_int32u c (make_optR false is_inv) in
         Some (cond, lfsv))
  | (Ccompl c), (a1 :: a2 :: nil) =>
      let is_inv := is_inv_cmp_int c in
      let cond := transl_cbranch_int64s c (make_optR false is_inv) in
      let fsv1 := ris_sreg_get prev a1 in
      let fsv2 := ris_sreg_get prev a2 in
      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
      Some (cond, lfsv)
  | (Ccomplu c), (a1 :: a2 :: nil) =>
      let is_inv := is_inv_cmp_int c in
      let cond := transl_cbranch_int64u c (make_optR false is_inv) in
      let fsv1 := ris_sreg_get prev a1 in
      let fsv2 := ris_sreg_get prev a2 in
      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
      Some (cond, lfsv)
  | (Ccomplimm c n), (a1 :: nil) =>
      let is_inv := is_inv_cmp_int c in
      let fsv1 := ris_sreg_get prev a1 in
      (if Int64.eq n Int64.zero then
        let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in
        let cond := transl_cbranch_int64s c (make_optR true is_inv) in
        Some (cond, lfsv)
      else
        let fsv := loadimm64 n in
        let lfsv := make_lfsv_cmp is_inv fsv1 fsv in
        let cond := transl_cbranch_int64s c (make_optR false is_inv) in
        Some (cond, lfsv))
  | (Ccompluimm c n), (a1 :: nil) =>
      let is_inv := is_inv_cmp_int c in
      let fsv1 := ris_sreg_get prev a1 in
      (if Int64.eq n Int64.zero then
        let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in
        let cond := transl_cbranch_int64u c (make_optR true is_inv) in
        Some (cond, lfsv)
      else
        let fsv := loadimm64 n in
        let lfsv := make_lfsv_cmp is_inv fsv1 fsv in
        let cond := transl_cbranch_int64u c (make_optR false is_inv) in
        Some (cond, lfsv))
  | (Ccompf c), (f1 :: f2 :: nil) =>
      let fsv1 := ris_sreg_get prev f1 in
      let fsv2 := ris_sreg_get prev f2 in
      let is_inv := is_inv_cmp_float c in
      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
      Some (expanse_cbranch_fp false cond_float c lfsv)
  | (Cnotcompf c), (f1 :: f2 :: nil) =>
      let fsv1 := ris_sreg_get prev f1 in
      let fsv2 := ris_sreg_get prev f2 in
      let is_inv := is_inv_cmp_float c in
      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
      Some (expanse_cbranch_fp true cond_float c lfsv)
  | (Ccompfs c), (f1 :: f2 :: nil) =>
      let fsv1 := ris_sreg_get prev f1 in
      let fsv2 := ris_sreg_get prev f2 in
      let is_inv := is_inv_cmp_float c in
      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
      Some (expanse_cbranch_fp false cond_single c lfsv)
  | (Cnotcompfs c), (f1 :: f2 :: nil) =>
      let fsv1 := ris_sreg_get prev f1 in
      let fsv2 := ris_sreg_get prev f2 in
      let is_inv := is_inv_cmp_float c in
      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
      Some (expanse_cbranch_fp true cond_single c lfsv)
  | _, _ => 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.
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.

(** * 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 Val.swap_cmpf_bool; trivial.
  - replace (Cle) with (swap_comparison Cge) by auto;
    rewrite Val.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 Val.swap_cmpfs_bool; trivial.
  - replace (Cle) with (swap_comparison Cge) by auto;
    rewrite Val.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.

Lemma simplify_intconst_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
  args fsv lr n: forall
  (H : match lr with
       | nil => Some (loadimm32 n)
       | _ :: _ => None
       end = Some fsv)
  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
  eval_sval ctx fsv =
  eval_operation (cge ctx) (csp ctx) (Ointconst n) args (cm0 ctx).
Proof.
  intros.
  repeat (destruct lr; simpl; try congruence);
  simpl in OK1; inv OK1; inv H; simpl;
  unfold loadimm32, load_hilo32, make_lfsv_single; simpl;
  specialize make_immed32_sound with (n);
  destruct (make_immed32 (n)) eqn:EQMKI; intros; simpl;
  try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl;
  try apply Int.same_if_eq in EQLO; subst;
  try rewrite Int.add_commut, Int.add_zero_l;
  try rewrite ltu_12_wordsize; try rewrite H; trivial.
Qed.

Lemma simplify_longconst_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
  args fsv lr n: forall
  (H : match lr with
       | nil => Some (loadimm64 n)
       | _ :: _ => None
       end = Some fsv)
  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
  eval_sval ctx fsv =
  eval_operation (cge ctx) (csp ctx) (Olongconst n) args (cm0 ctx).
Proof.
  intros.
  repeat (destruct lr; simpl; try congruence);
  simpl in OK1; inv OK1; inv H; simpl;
  unfold loadimm64, load_hilo64, make_lfsv_single; simpl;
  specialize make_immed64_sound with (n);
  destruct (make_immed64 (n)) eqn:EQMKI; intros; simpl;
  try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl;
  try apply Int64.same_if_eq in EQLO; subst;
  try rewrite Int64.add_commut, Int64.add_zero_l;
  try rewrite Int64.add_commut;
  try rewrite ltu_12_wordsize; try rewrite H; trivial.
Qed.

Lemma simplify_floatconst_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
  args fsv lr n: forall
  (H : match lr with
       | nil =>
           Some
             (fSop Ofloat_of_bits
                (make_lfsv_single (loadimm64 (Float.to_bits n))))
       | _ :: _ => None
       end = Some fsv)
  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
  eval_sval ctx fsv =
  eval_operation (cge ctx) (csp ctx) (Ofloatconst n) args (cm0 ctx).
Proof.
  intros.
  repeat (destruct lr; simpl; try congruence);
  simpl in OK1; inv OK1; inv H; simpl;
  unfold loadimm64, load_hilo64; simpl;
  specialize make_immed64_sound with (Float.to_bits n);
  destruct (make_immed64 (Float.to_bits n)) eqn:EQMKI; intros;
  try destruct (Int64.eq lo Int64.zero) eqn:EQLO;
  simpl.
  - try rewrite Int64.add_commut, Int64.add_zero_l; inv H;
    try rewrite Float.of_to_bits; trivial.
  - apply Int64.same_if_eq in EQLO; subst.
    try rewrite Int64.add_commut, Int64.add_zero_l in H.
    rewrite <- H; try rewrite Float.of_to_bits; trivial.
  - rewrite <- H; try rewrite Float.of_to_bits; trivial.
  - rewrite <- H; try rewrite Float.of_to_bits; trivial.
Qed.

Lemma simplify_singleconst_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
  args fsv lr n: forall
  (H : match lr with
       | nil =>
           Some
             (fSop Osingle_of_bits
                (make_lfsv_single (loadimm32 (Float32.to_bits n))))
       | _ :: _ => None
       end = Some fsv)
  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
  eval_sval ctx fsv =
  eval_operation (cge ctx) (csp ctx) (Osingleconst n) args (cm0 ctx).
Proof.
  intros.
  repeat (destruct lr; simpl; try congruence);
  simpl in OK1; inv OK1; inv H; simpl;
  unfold loadimm32, load_hilo32; simpl;
  specialize make_immed32_sound with (Float32.to_bits n);
  destruct (make_immed32 (Float32.to_bits n)) eqn:EQMKI; intros;
  try destruct (Int.eq lo Int.zero) eqn:EQLO;
  simpl.
  { try rewrite Int.add_commut, Int.add_zero_l; inv H;
    try rewrite Float32.of_to_bits; trivial. }
  all:
    try apply Int.same_if_eq in EQLO; subst;
    try rewrite Int.add_commut, Int.add_zero_l in H; simpl;
    rewrite ltu_12_wordsize; simpl; try rewrite <- H;
    try rewrite Float32.of_to_bits; trivial.
Qed.

Lemma simplify_cast8signed_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
  args fsv lr: forall
  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
  (H : match lr with
       | nil => None
       | a1 :: nil =>
           Some
             (fSop (Oshrimm (Int.repr 24))
                (make_lfsv_single
                   (fSop (Oshlimm (Int.repr 24)) (make_lfsv_single (hrs a1)))))
       | a1 :: _ :: _ => None
       end = Some fsv)
  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
  eval_sval ctx fsv =
  eval_operation (cge ctx) (csp ctx) Ocast8signed args (cm0 ctx).
Proof.
  intros.
  repeat (destruct lr; simpl; try congruence);
  simpl in OK1; inv H; simpl;
  rewrite !REG_EQ.
  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1.
  unfold Val.shr, Val.shl, Val.sign_ext;
  destruct v; simpl; auto.
  assert (A: Int.ltu (Int.repr 24) Int.iwordsize = true) by auto.
  rewrite A. rewrite Int.sign_ext_shr_shl; simpl; trivial. cbn; lia.
Qed.

Lemma simplify_cast16signed_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
  args fsv lr: forall
  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
  (H : match lr with
       | nil => None
       | a1 :: nil =>
           Some
             (fSop (Oshrimm (Int.repr 16))
                (make_lfsv_single
                   (fSop (Oshlimm (Int.repr 16)) (make_lfsv_single (hrs a1)))))
       | a1 :: _ :: _ => None
       end = Some fsv)
  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
  eval_sval ctx fsv =
  eval_operation (cge ctx) (csp ctx) Ocast16signed args (cm0 ctx).
Proof.
  intros.
  repeat (destruct lr; simpl; try congruence);
  simpl in OK1; inv H; simpl;
  rewrite !REG_EQ.
  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1.
  unfold Val.shr, Val.shl, Val.sign_ext;
  destruct v; simpl; auto.
  assert (A: Int.ltu (Int.repr 16) Int.iwordsize = true) by auto.
  rewrite A. rewrite Int.sign_ext_shr_shl; simpl; trivial. cbn; lia.
Qed.

Lemma simplify_addimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
  args fsv lr n: forall
  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
  (H : match lr with
       | nil => None
       | a1 :: nil => Some (addimm32 (hrs a1) n None)
       | a1 :: _ :: _ => None
       end = Some fsv)
  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
  eval_sval ctx fsv =
  eval_operation (cge ctx) (csp ctx) (Oaddimm n) args (cm0 ctx).
Proof.
  intros.
  repeat (destruct lr; simpl; try congruence);
  simpl in OK1; inv H; simpl.
  unfold addimm32, opimm32, load_hilo32, make_lfsv_cmp; simpl;
  specialize make_immed32_sound with (n);
  destruct (make_immed32 (n)) eqn:EQMKI; intros; simpl;
  try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl;
  rewrite !REG_EQ;
  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial.
  apply Int.same_if_eq in EQLO; subst;
  rewrite Int.add_commut, Int.add_zero_l;
  rewrite ltu_12_wordsize; trivial.
Qed.

Lemma simplify_andimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
  args fsv lr n: forall
  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
  (H : match lr with
       | nil => None
       | a1 :: nil => Some (andimm32 (hrs a1) n)
       | a1 :: _ :: _ => None
       end = Some fsv)
  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
  eval_sval ctx fsv =
  eval_operation (cge ctx) (csp ctx) (Oandimm n) args (cm0 ctx).
Proof.
  intros.
  repeat (destruct lr; simpl; try congruence);
  simpl in OK1; inv H; simpl.
  unfold andimm32, opimm32, load_hilo32, make_lfsv_cmp; simpl;
  specialize make_immed32_sound with (n);
  destruct (make_immed32 (n)) eqn:EQMKI; intros; simpl;
  try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl;
  rewrite !REG_EQ;
  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial.
  fold (Val.and (Vint imm) v); rewrite Val.and_commut; trivial.
  apply Int.same_if_eq in EQLO; subst;
  rewrite Int.add_commut, Int.add_zero_l;
  rewrite ltu_12_wordsize; trivial.
Qed.

Lemma simplify_orimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
  args fsv lr n: forall
  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
  (H : match lr with
       | nil => None
       | a1 :: nil => Some (orimm32 (hrs a1) n)
       | a1 :: _ :: _ => None
       end = Some fsv)
  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
  eval_sval ctx fsv =
  eval_operation (cge ctx) (csp ctx) (Oorimm n) args (cm0 ctx).
Proof.
  intros.
  repeat (destruct lr; simpl; try congruence);
  simpl in OK1; inv H; simpl.
  unfold orimm32, opimm32, load_hilo32, make_lfsv_cmp; simpl;
  specialize make_immed32_sound with (n);
  destruct (make_immed32 (n)) eqn:EQMKI; intros; simpl;
  try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl;
  rewrite !REG_EQ;
  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial.
  fold (Val.or (Vint imm) v); rewrite Val.or_commut; trivial.
  apply Int.same_if_eq in EQLO; subst;
  rewrite Int.add_commut, Int.add_zero_l;
  rewrite ltu_12_wordsize; trivial.
Qed.

Lemma simplify_xorimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
  args fsv lr n: forall
  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
  (H : match lr with
       | nil => None
       | a1 :: nil => Some (xorimm32 (hrs a1) n)
       | a1 :: _ :: _ => None
       end = Some fsv)
  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
  eval_sval ctx fsv =
  eval_operation (cge ctx) (csp ctx) (Oxorimm n) args (cm0 ctx).
Proof.
  intros.
  repeat (destruct lr; simpl; try congruence);
  simpl in OK1; inv H; simpl.
  unfold xorimm32, opimm32, load_hilo32, make_lfsv_cmp; simpl;
  specialize make_immed32_sound with (n);
  destruct (make_immed32 (n)) eqn:EQMKI; intros; simpl;
  try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl;
  rewrite !REG_EQ;
  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial.
  apply Int.same_if_eq in EQLO; subst;
  rewrite Int.add_commut, Int.add_zero_l;
  rewrite ltu_12_wordsize; trivial.
Qed.

Lemma simplify_shrximm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
  args fsv lr n: forall
  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
  (H : match lr with
       | nil => None
       | a1 :: nil =>
           if Int.eq n Int.zero
           then
            Some
              (fSop (OEmayundef (MUshrx n))
                 (make_lfsv_cmp false (hrs a1) (hrs a1)))
           else
            if Int.eq n Int.one
            then
             Some
               (fSop (OEmayundef (MUshrx n))
                  (make_lfsv_cmp false
                     (fSop (Oshrimm Int.one)
                        (make_lfsv_single
                           (fSop Oadd
                              (make_lfsv_cmp false (hrs a1)
                                 (fSop (Oshruimm (Int.repr 31))
                                    (make_lfsv_single (hrs a1)))))))
                     (fSop (Oshrimm Int.one)
                        (make_lfsv_single
                           (fSop Oadd
                              (make_lfsv_cmp false (hrs a1)
                                 (fSop (Oshruimm (Int.repr 31))
                                    (make_lfsv_single (hrs a1)))))))))
            else
             Some
               (fSop (OEmayundef (MUshrx n))
                  (make_lfsv_cmp false
                     (fSop (Oshrimm n)
                        (make_lfsv_single
                           (fSop Oadd
                              (make_lfsv_cmp false (hrs a1)
                                 (fSop (Oshruimm (Int.sub Int.iwordsize n))
                                    (make_lfsv_single
                                       (fSop (Oshrimm (Int.repr 31))
                                          (make_lfsv_single (hrs a1)))))))))
                     (fSop (Oshrimm n)
                        (make_lfsv_single
                           (fSop Oadd
                              (make_lfsv_cmp false (hrs a1)
                                 (fSop (Oshruimm (Int.sub Int.iwordsize n))
                                    (make_lfsv_single
                                       (fSop (Oshrimm (Int.repr 31))
                                          (make_lfsv_single (hrs a1)))))))))))
       | a1 :: _ :: _ => None
       end = Some fsv)
  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
  eval_sval ctx fsv =
  eval_operation (cge ctx) (csp ctx) (Oshrximm n) args (cm0 ctx).
Proof.
  intros.
  repeat (destruct lr; simpl; try congruence).
  assert (A: Int.ltu Int.zero (Int.repr 31) = true) by auto.
  assert (B: Int.ltu (Int.repr 31) Int.iwordsize = true) by auto.
  assert (C: Int.ltu Int.one Int.iwordsize = true) by auto.
  destruct (Int.eq n Int.zero) eqn:EQ0;
  destruct (Int.eq n Int.one) eqn:EQ1.
  { apply Int.same_if_eq in EQ0.
    apply Int.same_if_eq in EQ1; subst. discriminate. }
  all:
    simpl in OK1; inv H; simpl;
    rewrite !REG_EQ;
    destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1;
    destruct (Val.shrx v (Vint n)) eqn:TOTAL; cbn;
    unfold eval_may_undef.
  2,4,6:
    unfold Val.shrx in TOTAL;
    destruct v; simpl in TOTAL; simpl; try congruence;
    try rewrite B; simpl; try rewrite C; simpl;
    try destruct (Val.shr _ _);
    destruct (Int.ltu n (Int.repr 31)); try congruence.
  - destruct v; simpl in TOTAL; try congruence;
    apply Int.same_if_eq in EQ0; subst;
    rewrite A, Int.shrx_zero in TOTAL;
    [auto | cbn; lia].
  - apply Int.same_if_eq in EQ1; subst;
    unfold Val.shr, Val.shru, Val.shrx, Val.add; simpl;
    destruct v; simpl in *; try discriminate; trivial.
    rewrite B, C.
    rewrite Int.shrx1_shr in TOTAL; auto.
  - exploit Val.shrx_shr_2; eauto. rewrite EQ0.
    intros; subst.
    destruct v; simpl in *; try discriminate; trivial.
    rewrite B in *.
    destruct Int.ltu eqn:EQN0 in TOTAL; try discriminate.
    simpl in *.
    destruct Int.ltu eqn:EQN1 in TOTAL; try discriminate.
    replace Int.iwordsize with (Int.repr 32) in * by auto.
    rewrite !EQN1. simpl in *.
    destruct Int.ltu eqn:EQN2 in TOTAL; try discriminate.
    rewrite !EQN2. rewrite EQN0.
    reflexivity.
Qed.

Lemma simplify_cast32unsigned_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
  args fsv lr: forall
  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
  (H : match lr with
       | nil => None
       | a1 :: nil =>
           Some
             (fSop (Oshrluimm (Int.repr 32))
                (make_lfsv_single
                   (fSop (Oshllimm (Int.repr 32))
                      (make_lfsv_single
                         (fSop Ocast32signed (make_lfsv_single (hrs a1)))))))
       | a1 :: _ :: _ => None
       end = Some fsv)
  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
  eval_sval ctx fsv =
  eval_operation (cge ctx) (csp ctx) Ocast32unsigned args (cm0 ctx).
Proof.
  intros.
  repeat (destruct lr; simpl; try congruence);
  simpl in OK1; inv H; simpl.
  rewrite !REG_EQ;
  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1.
  unfold Val.shrlu, Val.shll, Val.longofint, Val.longofintu.
  destruct v; simpl; auto.
  assert (A: Int.ltu (Int.repr 32) Int64.iwordsize' = true) by auto.
  rewrite A. rewrite Int64.shru'_shl'; auto.
  replace (Int.ltu (Int.repr 32) (Int.repr 32)) with (false) by auto.
  rewrite cast32unsigned_from_cast32signed.
  replace Int64.zwordsize with 64 by auto.
  rewrite Int.unsigned_repr; cbn; try lia.
  replace (Int.sub (Int.repr 32) (Int.repr 32)) with (Int.zero) by auto.
  rewrite Int64.shru'_zero. reflexivity.
Qed.

Lemma simplify_addlimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
  args fsv lr n: forall
  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
  (H : match lr with
       | nil => None
       | a1 :: nil => Some (addimm64 (hrs a1) n None)
       | a1 :: _ :: _ => None
       end = Some fsv)
  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
  eval_sval ctx fsv =
  eval_operation (cge ctx) (csp ctx) (Oaddlimm n) args (cm0 ctx).
Proof.
  intros.
  repeat (destruct lr; simpl; try congruence);
  simpl in OK1; inv H; simpl;
  unfold addimm64, opimm64, load_hilo64, make_lfsv_cmp; simpl;
  specialize make_immed64_sound with (n);
  destruct (make_immed64 (n)) eqn:EQMKI; intros; simpl;
  try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl;
  rewrite !REG_EQ;
  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial.
  apply Int64.same_if_eq in EQLO; subst.
  rewrite Int64.add_commut, Int64.add_zero_l; trivial.
Qed.

Lemma simplify_andlimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
  args fsv lr n: forall
  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
  (H : match lr with
       | nil => None
       | a1 :: nil => Some (andimm64 (hrs a1) n)
       | a1 :: _ :: _ => None
       end = Some fsv)
  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
  eval_sval ctx fsv =
  eval_operation (cge ctx) (csp ctx) (Oandlimm n) args (cm0 ctx).
Proof.
  intros.
  repeat (destruct lr; simpl; try congruence);
  simpl in OK1; inv H; simpl;
  unfold andimm64, opimm64, load_hilo64, make_lfsv_cmp; simpl;
  specialize make_immed64_sound with (n);
  destruct (make_immed64 (n)) eqn:EQMKI; intros; simpl;
  try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl;
  rewrite !REG_EQ;
  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial.
  fold (Val.andl (Vlong imm) v); rewrite Val.andl_commut; trivial.
  apply Int64.same_if_eq in EQLO; subst;
  rewrite Int64.add_commut, Int64.add_zero_l; trivial.
Qed.

Lemma simplify_orlimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
  args fsv lr n: forall
  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
  (H : match lr with
       | nil => None
       | a1 :: nil => Some (orimm64 (hrs a1) n)
       | a1 :: _ :: _ => None
       end = Some fsv)
  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
  eval_sval ctx fsv =
  eval_operation (cge ctx) (csp ctx) (Oorlimm n) args (cm0 ctx).
Proof.
  intros.
  repeat (destruct lr; simpl; try congruence);
  simpl in OK1; inv H; simpl;
  unfold orimm64, opimm64, load_hilo64, make_lfsv_cmp; simpl;
  specialize make_immed64_sound with (n);
  destruct (make_immed64 (n)) eqn:EQMKI; intros; simpl;
  try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl;
  rewrite !REG_EQ;
  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial.
  fold (Val.orl (Vlong imm) v); rewrite Val.orl_commut; trivial.
  apply Int64.same_if_eq in EQLO; subst;
  rewrite Int64.add_commut, Int64.add_zero_l; trivial.
Qed.

Lemma simplify_xorlimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
  args fsv lr n: forall
  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
  (H : match lr with
       | nil => None
       | a1 :: nil => Some (xorimm64 (hrs a1) n)
       | a1 :: _ :: _ => None
       end = Some fsv)
  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
  eval_sval ctx fsv =
  eval_operation (cge ctx) (csp ctx) (Oxorlimm n) args (cm0 ctx).
Proof.
  intros.
  repeat (destruct lr; simpl; try congruence);
  simpl in OK1; inv H; simpl;
  unfold xorimm64, opimm64, load_hilo64, make_lfsv_cmp; simpl;
  specialize make_immed64_sound with (n);
  destruct (make_immed64 (n)) eqn:EQMKI; intros; simpl;
  try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl;
  rewrite !REG_EQ;
  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial.
  apply Int64.same_if_eq in EQLO; subst;
  rewrite Int64.add_commut, Int64.add_zero_l; trivial.
Qed.

Lemma simplify_shrxlimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
  args fsv lr n: forall
  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
  (H : match lr with
       | nil => None
       | a1 :: nil =>
           if Int.eq n Int.zero
           then
            Some
              (fSop (OEmayundef (MUshrxl n))
                 (make_lfsv_cmp false (hrs a1) (hrs a1)))
           else
            if Int.eq n Int.one
            then
             Some
               (fSop (OEmayundef (MUshrxl n))
                  (make_lfsv_cmp false
                     (fSop (Oshrlimm Int.one)
                        (make_lfsv_single
                           (fSop Oaddl
                              (make_lfsv_cmp false (hrs a1)
                                 (fSop (Oshrluimm (Int.repr 63))
                                    (make_lfsv_single (hrs a1)))))))
                     (fSop (Oshrlimm Int.one)
                        (make_lfsv_single
                           (fSop Oaddl
                              (make_lfsv_cmp false (hrs a1)
                                 (fSop (Oshrluimm (Int.repr 63))
                                    (make_lfsv_single (hrs a1)))))))))
            else
             Some
               (fSop (OEmayundef (MUshrxl n))
                  (make_lfsv_cmp false
                     (fSop (Oshrlimm n)
                        (make_lfsv_single
                           (fSop Oaddl
                              (make_lfsv_cmp false (hrs a1)
                                 (fSop (Oshrluimm (Int.sub Int64.iwordsize' n))
                                    (make_lfsv_single
                                       (fSop (Oshrlimm (Int.repr 63))
                                          (make_lfsv_single (hrs a1)))))))))
                     (fSop (Oshrlimm n)
                        (make_lfsv_single
                           (fSop Oaddl
                              (make_lfsv_cmp false (hrs a1)
                                 (fSop (Oshrluimm (Int.sub Int64.iwordsize' n))
                                    (make_lfsv_single
                                       (fSop (Oshrlimm (Int.repr 63))
                                          (make_lfsv_single (hrs a1)))))))))))
       | a1 :: _ :: _ => None
       end = Some fsv)
  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
  eval_sval ctx fsv =
  eval_operation (cge ctx) (csp ctx) (Oshrxlimm n) args (cm0 ctx).
Proof.
  intros.
  repeat (destruct lr; simpl; try congruence).
  assert (A: Int.ltu Int.zero (Int.repr 63) = true) by auto.
  assert (B: Int.ltu (Int.repr 63) Int64.iwordsize' = true) by auto.
  assert (C: Int.ltu Int.one Int64.iwordsize' = true) by auto.
  destruct (Int.eq n Int.zero) eqn:EQ0;
  destruct (Int.eq n Int.one) eqn:EQ1.
  { apply Int.same_if_eq in EQ0.
    apply Int.same_if_eq in EQ1; subst. discriminate. }
  all:
    simpl in OK1; inv H; simpl;
    rewrite !REG_EQ;
    destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1;
    destruct (Val.shrxl v (Vint n)) eqn:TOTAL; cbn;
    unfold eval_may_undef.
  2,4,6:
    unfold Val.shrxl in TOTAL;
    destruct v; simpl in TOTAL; simpl; try congruence;
    try rewrite B; simpl; try rewrite C; simpl;
    try destruct (Val.shrl _ _);
    destruct (Int.ltu n (Int.repr 63)); try congruence.
  - destruct v; simpl in TOTAL; try congruence;
    apply Int.same_if_eq in EQ0; subst;
    rewrite A, Int64.shrx'_zero in *.
    assumption.
  - apply Int.same_if_eq in EQ1; subst;
    unfold Val.shrl, Val.shrlu, Val.shrxl, Val.addl; simpl;
    destruct v; simpl in *; try discriminate; trivial.
    rewrite B, C.
    rewrite Int64.shrx'1_shr' in TOTAL; auto.
  - exploit Val.shrxl_shrl_2; eauto. rewrite EQ0.
    intros; subst.
    destruct v; simpl in *; try discriminate; trivial.
    rewrite B in *.
    destruct Int.ltu eqn:EQN0 in TOTAL; try discriminate.
    simpl in *.
    destruct Int.ltu eqn:EQN1 in TOTAL; try discriminate.
    replace Int64.iwordsize' with (Int.repr 64) in * by auto.
    rewrite !EQN1. simpl in *.
    destruct Int.ltu eqn:EQN2 in TOTAL; try discriminate.
    rewrite !EQN2. rewrite EQN0.
    reflexivity.
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.
  eapply simplify_intconst_correct; eauto.
  eapply simplify_longconst_correct; eauto.
  eapply simplify_floatconst_correct; eauto. 
  eapply simplify_singleconst_correct; eauto. 
  eapply simplify_cast8signed_correct; eauto.
  eapply simplify_cast16signed_correct; eauto.
  eapply simplify_addimm_correct; eauto.
  eapply simplify_andimm_correct; eauto.
  eapply simplify_orimm_correct; eauto.
  eapply simplify_xorimm_correct; eauto.
  eapply simplify_shrximm_correct; eauto.
  eapply simplify_cast32unsigned_correct; eauto.
  eapply simplify_addlimm_correct; eauto.
  eapply simplify_andlimm_correct; eauto.
  eapply simplify_orlimm_correct; eauto.
  eapply simplify_xorlimm_correct; eauto.
  eapply simplify_shrxlimm_correct; eauto.
  (* 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 ctx st c' l': forall
  (TARGET: target_cbranch_expanse hrs c l = Some (c', l'))
  (REF: ris_refines ctx hrs st)
  (OK: ris_ok ctx hrs),
  eval_scondition ctx c' l' =
  eval_scondition ctx c (list_sval_inj (map (si_sreg st) l)).
Proof.
  unfold target_cbranch_expanse, eval_scondition; simpl.
  intros H ? ?. inversion REF.
  destruct c; try congruence;
  repeat (destruct l; simpl in H; try congruence).
  1,2,5,6:
    destruct c; inv H; simpl;
    rewrite !REG_EQ;
    try (destruct (eval_smem ctx (si_smem st)) eqn:OKmem; try congruence);
    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);
    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;
    rewrite !REG_EQ;
    try (destruct (eval_smem ctx (si_smem st)) eqn:OKmem; try congruence);
    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);
    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 eval_may_undef; 
    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;
    try rewrite Int64.add_commut;
    try rewrite Int.add_zero_l; try rewrite 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;
    rewrite !REG_EQ;
    try (destruct (eval_smem ctx (si_smem st)) eqn:OKmem; try congruence);
    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);
    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.