cleanup

1 files changed, 0 insertions, 2077 deletions

diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v
deleted file mode 100644
index 2370ad66..00000000
--- a/riscV/RTLpathSE_simplify.v
+++ /dev/null
@@ -1,2077 +0,0 @@
-Require Import Coqlib Floats Values Memory.
-Require Import Integers.
-Require Import Op Registers.
-Require Import RTLpathSE_theory.
-Require Import RTLpathSE_simu_specs.
-Require Import Asmgen Asmgenproof1.
-Require Import Lia.
-
-(** Useful functions for conditions/branches expansion *)
-
-Definition is_inv_cmp_int (cmp: comparison) : bool :=
-  match cmp with | Cle | Cgt => true | _ => false end.
-
-Definition is_inv_cmp_float (cmp: comparison) : bool :=
-  match cmp with | Cge | Cgt => true | _ => false end.
-
-Definition make_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_lhsv_cmp (is_inv: bool) (hv1 hv2: hsval) : list_hsval :=
-  let (hvfirst, hvsec) := if is_inv then (hv1, hv2) else (hv2, hv1) in
-  let lhsv := fScons hvfirst fSnil in
-  fScons hvsec lhsv.
-
-Definition make_lhsv_single (hvs: hsval) : list_hsval :=
-  fScons hvs fSnil.
-
-(** * Expansion functions *)
-
-(** ** Immediate loads *)
-
-Definition load_hilo32 (hi lo: int) :=
-  if Int.eq lo Int.zero then
-    fSop (OEluiw hi) fSnil
-  else
-    let hvs := fSop (OEluiw hi) fSnil in
-    let hl := make_lhsv_single hvs in
-    fSop (OEaddiw None lo) hl.
-
-Definition load_hilo64 (hi lo: int64) :=
-  if Int64.eq lo Int64.zero then
-    fSop (OEluil hi) fSnil
-  else
-    let hvs := fSop (OEluil hi) fSnil in
-    let hl := make_lhsv_single hvs in
-    fSop (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: hsval) (n: int) (op: operation) (opimm: int -> operation) :=
-  match make_immed32 n with
-  | Imm32_single imm =>
-      let hl := make_lhsv_single hv1 in
-      fSop (opimm imm) hl
-  | Imm32_pair hi lo =>
-      let hvs := load_hilo32 hi lo in
-      let hl := make_lhsv_cmp false hv1 hvs in
-      fSop op hl
-  end.
-
-Definition opimm64 (hv1: hsval) (n: int64) (op: operation) (opimm: int64 -> operation) :=
-  match make_immed64 n with
-  | Imm64_single imm =>
-      let hl := make_lhsv_single hv1 in
-      fSop (opimm imm) hl
-  | Imm64_pair hi lo =>
-      let hvs := load_hilo64 hi lo in
-      let hl := make_lhsv_cmp false hv1 hvs in
-      fSop op hl
-  | Imm64_large imm =>
-      let hvs := fSop (OEloadli imm) fSnil in
-      let hl := make_lhsv_cmp false hv1 hvs in
-      fSop op hl
-  end.
-
-Definition addimm32 (hv1: hsval) (n: int) (or: option oreg) := opimm32 hv1 n Oadd (OEaddiw or).
-Definition andimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oand OEandiw.
-Definition orimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oor OEoriw.
-Definition xorimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oxor OExoriw.
-Definition sltimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltw None) OEsltiw.
-Definition sltuimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltuw None) OEsltiuw.
-Definition addimm64 (hv1: hsval) (n: int64) (or: option oreg) := opimm64 hv1 n Oaddl (OEaddil or).
-Definition andimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oandl OEandil.
-Definition orimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oorl OEoril.
-Definition xorimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oxorl OExoril.
-Definition sltimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltl None) OEsltil.
-Definition sltuimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltul None) OEsltiul.
-
-(** ** Comparisons intructions *)
-
-Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR: option oreg) :=
-  match cmp with
-  | Ceq => fSop (OEseqw optR) lhsv
-  | Cne => fSop (OEsnew optR) lhsv
-  | Clt | Cgt => fSop (OEsltw optR) lhsv
-  | Cle | Cge =>
-      let hvs := (fSop (OEsltw optR) lhsv) in
-      let hl := make_lhsv_single hvs in
-      fSop (OExoriw Int.one) hl
-  end.
-
-Definition cond_int32u (cmp: comparison) (lhsv: list_hsval) (optR: option oreg) :=
-  match cmp with
-  | Ceq => fSop (OEsequw optR) lhsv
-  | Cne => fSop (OEsneuw optR) lhsv
-  | Clt | Cgt => fSop (OEsltuw optR) lhsv
-  | Cle | Cge =>
-      let hvs := (fSop (OEsltuw optR) lhsv) in
-      let hl := make_lhsv_single hvs in
-      fSop (OExoriw Int.one) hl
-  end.
-
-Definition cond_int64s (cmp: comparison) (lhsv: list_hsval) (optR: option oreg) :=
-  match cmp with
-  | Ceq => fSop (OEseql optR) lhsv
-  | Cne => fSop (OEsnel optR) lhsv
-  | Clt | Cgt => fSop (OEsltl optR) lhsv
-  | Cle | Cge =>
-      let hvs := (fSop (OEsltl optR) lhsv) in
-      let hl := make_lhsv_single hvs in
-      fSop (OExoriw Int.one) hl
-  end.
-
-Definition cond_int64u (cmp: comparison) (lhsv: list_hsval) (optR: option oreg) :=
-  match cmp with
-  | Ceq => fSop (OEsequl optR) lhsv
-  | Cne => fSop (OEsneul optR) lhsv
-  | Clt | Cgt => fSop (OEsltul optR) lhsv
-  | Cle | Cge =>
-      let hvs := (fSop (OEsltul optR) lhsv) in
-      let hl := make_lhsv_single hvs in
-      fSop (OExoriw Int.one) hl
-  end.
-
-Definition expanse_condimm_int32s (cmp: comparison) (hv1: hsval) (n: int) :=
-  let is_inv := is_inv_cmp_int cmp in
-  if Int.eq n Int.zero then
-    let optR := make_optR true is_inv in
-    let hl := make_lhsv_cmp is_inv hv1 hv1 in
-    cond_int32s cmp hl optR
-  else
-    match cmp with
-    | Ceq | Cne =>
-        let optR := make_optR true is_inv in
-        let hvs := xorimm32 hv1 n in
-        let hl := make_lhsv_cmp false hvs hvs in
-        cond_int32s cmp hl optR
-    | Clt => sltimm32 hv1 n
-    | Cle =>
-        if Int.eq n (Int.repr Int.max_signed) then
-          let hvs := loadimm32 Int.one in
-          let hl := make_lhsv_cmp false hv1 hvs in
-          fSop (OEmayundef MUint) hl
-        else sltimm32 hv1 (Int.add n Int.one)
-    | _ =>
-        let optR := make_optR false is_inv in
-        let hvs := loadimm32 n in
-        let hl := make_lhsv_cmp is_inv hv1 hvs in
-        cond_int32s cmp hl optR
-    end.
-
-Definition expanse_condimm_int32u (cmp: comparison) (hv1: hsval) (n: int) :=
-  let is_inv := is_inv_cmp_int cmp in
-  if Int.eq n Int.zero then
-    let optR := make_optR true is_inv in
-    let hl := make_lhsv_cmp is_inv hv1 hv1 in
-    cond_int32u cmp hl optR
-  else
-    match cmp with
-    | Clt => sltuimm32 hv1 n
-    | _ =>
-        let optR := make_optR false is_inv in
-        let hvs := loadimm32 n in
-        let hl := make_lhsv_cmp is_inv hv1 hvs in
-        cond_int32u cmp hl optR
-    end.
-
-Definition expanse_condimm_int64s (cmp: comparison) (hv1: hsval) (n: int64) :=
-  let is_inv := is_inv_cmp_int cmp in
-  if Int64.eq n Int64.zero then
-    let optR := make_optR true is_inv in
-    let hl := make_lhsv_cmp is_inv hv1 hv1 in
-    cond_int64s cmp hl optR
-  else
-    match cmp with
-    | Ceq | Cne =>
-        let optR := make_optR true is_inv in
-        let hvs := xorimm64 hv1 n in
-        let hl := make_lhsv_cmp false hvs hvs in
-        cond_int64s cmp hl optR
-    | Clt => sltimm64 hv1 n
-    | Cle =>
-        if Int64.eq n (Int64.repr Int64.max_signed) then
-          let hvs := loadimm32 Int.one in
-          let hl := make_lhsv_cmp false hv1 hvs in
-          fSop (OEmayundef MUlong) hl
-        else sltimm64 hv1 (Int64.add n Int64.one)
-    | _ =>
-        let optR := make_optR false is_inv in
-        let hvs := loadimm64 n in
-        let hl := make_lhsv_cmp is_inv hv1 hvs in
-        cond_int64s cmp hl optR
-    end.
-
-Definition expanse_condimm_int64u (cmp: comparison) (hv1: hsval) (n: int64) :=
-  let is_inv := is_inv_cmp_int cmp in
-  if Int64.eq n Int64.zero then
-    let optR := make_optR true is_inv in
-    let hl := make_lhsv_cmp is_inv hv1 hv1 in
-    cond_int64u cmp hl optR
-  else
-    match cmp with
-    | Clt => sltuimm64 hv1 n
-    | _ =>
-        let optR := make_optR false is_inv in
-        let hvs := loadimm64 n in
-        let hl := make_lhsv_cmp is_inv hv1 hvs in
-        cond_int64u cmp hl optR
-    end.
-
-Definition cond_float (cmp: comparison) (lhsv: list_hsval) :=
-  match cmp with
-  | Ceq | Cne => fSop OEfeqd lhsv
-  | Clt | Cgt => fSop OEfltd lhsv
-  | Cle | Cge => fSop OEfled lhsv
-  end.
-
-Definition cond_single (cmp: comparison) (lhsv: list_hsval) :=
-  match cmp with
-  | Ceq | Cne => fSop OEfeqs lhsv
-  | Clt | Cgt => fSop OEflts lhsv
-  | Cle | Cge => fSop OEfles lhsv
-  end.
-
-Definition is_normal_cmp cmp :=
-  match cmp with | Cne => false | _ => true end.
-
-Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) :=
-  let normal := is_normal_cmp cmp in
-  let normal' := if cnot then negb normal else normal in
-  let hvs := fn_cond cmp lhsv in
-  let hl := make_lhsv_single hvs in
-  if normal' then hvs else fSop (OExoriw Int.one) hl.
-
-(** ** Branches instructions *)
-
-Definition transl_cbranch_int32s (cmp: comparison) (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 (lhsv: list_hsval) : (condition * list_hsval) :=
-  let normal := is_normal_cmp cmp in
-  let normal' := if cnot then negb normal else normal in
-  let hvs := fn_cond cmp lhsv in
-  let hl := make_lhsv_cmp false hvs hvs in
-  if normal' then ((CEbnew (Some X0_R)), hl) else ((CEbeqw (Some X0_R)), hl).
-
-(** * Target simplifications using "fake" values *)
-
-Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval :=
-  match op, lr with
-  | Ocmp (Ccomp c), a1 :: a2 :: nil =>
-      let hv1 := fsi_sreg_get hst a1 in
-      let hv2 := fsi_sreg_get hst a2 in
-      let is_inv := is_inv_cmp_int c in
-      let optR := make_optR false is_inv in
-      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
-      Some (cond_int32s c lhsv optR)
-  | Ocmp (Ccompu c), a1 :: a2 :: nil =>
-      let hv1 := fsi_sreg_get hst a1 in
-      let hv2 := fsi_sreg_get hst a2 in
-      let is_inv := is_inv_cmp_int c in
-      let optR := make_optR false is_inv in
-      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
-      Some (cond_int32u c lhsv optR)
-  | Ocmp (Ccompimm c imm), a1 :: nil =>
-      let hv1 := fsi_sreg_get hst a1 in
-      Some (expanse_condimm_int32s c hv1 imm)
-  | Ocmp (Ccompuimm c imm), a1 :: nil =>
-      let hv1 := fsi_sreg_get hst a1 in
-      Some (expanse_condimm_int32u c hv1 imm)
-  | Ocmp (Ccompl c), a1 :: a2 :: nil =>
-      let hv1 := fsi_sreg_get hst a1 in
-      let hv2 := fsi_sreg_get hst a2 in
-      let is_inv := is_inv_cmp_int c in
-      let optR := make_optR false is_inv in
-      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
-      Some (cond_int64s c lhsv optR)
-  | Ocmp (Ccomplu c), a1 :: a2 :: nil =>
-      let hv1 := fsi_sreg_get hst a1 in
-      let hv2 := fsi_sreg_get hst a2 in
-      let is_inv := is_inv_cmp_int c in
-      let optR := make_optR false is_inv in
-      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
-      Some (cond_int64u c lhsv optR)
-  | Ocmp (Ccomplimm c imm), a1 :: nil =>
-      let hv1 := fsi_sreg_get hst a1 in
-      Some (expanse_condimm_int64s c hv1 imm)
-  | Ocmp (Ccompluimm c imm), a1 :: nil =>
-      let hv1 := fsi_sreg_get hst a1 in
-      Some (expanse_condimm_int64u c hv1 imm)
-  | Ocmp (Ccompf c), f1 :: f2 :: nil =>
-      let hv1 := fsi_sreg_get hst f1 in
-      let hv2 := fsi_sreg_get hst f2 in
-      let is_inv := is_inv_cmp_float c in
-      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
-      Some (expanse_cond_fp false cond_float c lhsv)
-  | Ocmp (Cnotcompf c), f1 :: f2 :: nil =>
-      let hv1 := fsi_sreg_get hst f1 in
-      let hv2 := fsi_sreg_get hst f2 in
-      let is_inv := is_inv_cmp_float c in
-      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
-      Some (expanse_cond_fp true cond_float c lhsv)
-  | Ocmp (Ccompfs c), f1 :: f2 :: nil =>
-      let hv1 := fsi_sreg_get hst f1 in
-      let hv2 := fsi_sreg_get hst f2 in
-      let is_inv := is_inv_cmp_float c in
-      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
-      Some (expanse_cond_fp false cond_single c lhsv)
-  | Ocmp (Cnotcompfs c), f1 :: f2 :: nil =>
-      let hv1 := fsi_sreg_get hst f1 in
-      let hv2 := fsi_sreg_get hst f2 in
-      let is_inv := is_inv_cmp_float c in
-      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
-      Some (expanse_cond_fp true cond_single c lhsv)
-  | Ofloatconst f, nil =>
-      let hvs := loadimm64 (Float.to_bits f) in
-      let hl := make_lhsv_single hvs in
-      Some (fSop (Ofloat_of_bits) hl)
-  | Osingleconst f, nil =>
-      let hvs := loadimm32 (Float32.to_bits f) in
-      let hl := make_lhsv_single hvs in
-      Some (fSop (Osingle_of_bits) hl)
-  | Ointconst n, nil =>
-      Some (loadimm32 n)
-  | Olongconst n, nil =>
-      Some (loadimm64 n)
-  | Oaddimm n, a1 :: nil =>
-      let hv1 := fsi_sreg_get hst a1 in
-      Some (addimm32 hv1 n None)
-  | Oaddlimm n, a1 :: nil =>
-      let hv1 := fsi_sreg_get hst a1 in
-      Some (addimm64 hv1 n None)
-  | Oandimm n, a1 :: nil =>
-      let hv1 := fsi_sreg_get hst a1 in
-      Some (andimm32 hv1 n)
-  | Oandlimm n, a1 :: nil =>
-      let hv1 := fsi_sreg_get hst a1 in
-      Some (andimm64 hv1 n)
-  | Oorimm n, a1 :: nil =>
-      let hv1 := fsi_sreg_get hst a1 in
-      Some (orimm32 hv1 n)
-  | Oorlimm n, a1 :: nil =>
-      let hv1 := fsi_sreg_get hst a1 in
-      Some (orimm64 hv1 n)
-  | Oxorimm n, a1 :: nil =>
-      let hv1 := fsi_sreg_get hst a1 in
-      Some (xorimm32 hv1 n)
-  | Oxorlimm n, a1 :: nil =>
-      let hv1 := fsi_sreg_get hst a1 in
-      Some (xorimm64 hv1 n)
-  | Ocast8signed, a1 :: nil =>
-      let hv1 := fsi_sreg_get hst a1 in
-      let hl := make_lhsv_single hv1 in
-      let hvs := fSop (Oshlimm (Int.repr 24)) hl in
-      let hl' := make_lhsv_single hvs in
-      Some (fSop (Oshrimm (Int.repr 24)) hl')
-  | Ocast16signed, a1 :: nil =>
-      let hv1 := fsi_sreg_get hst a1 in
-      let hl := make_lhsv_single hv1 in
-      let hvs := fSop (Oshlimm (Int.repr 16)) hl in
-      let hl' := make_lhsv_single hvs in
-      Some (fSop (Oshrimm (Int.repr 16)) hl')
-  | Ocast32unsigned, a1 :: nil =>
-      let hv1 := fsi_sreg_get hst a1 in
-      let hl := make_lhsv_single hv1 in
-      let cast32s_s := fSop Ocast32signed hl in
-      let cast32s_l := make_lhsv_single cast32s_s in
-      let sllil_s := fSop (Oshllimm (Int.repr 32)) cast32s_l in
-      let sllil_l := make_lhsv_single sllil_s in
-      Some (fSop (Oshrluimm (Int.repr 32)) sllil_l)
-  | Oshrximm n, a1 :: nil =>
-      let hv1 := fsi_sreg_get hst a1 in
-      let hl := make_lhsv_single hv1 in
-      if Int.eq n Int.zero then
-        let lhl := make_lhsv_cmp false hv1 hv1 in
-        Some (fSop (OEmayundef (MUshrx n)) lhl)
-      else
-        if Int.eq n Int.one then
-          let srliw_s := fSop (Oshruimm (Int.repr 31)) hl in
-          let srliw_l := make_lhsv_cmp false hv1 srliw_s in
-          let addw_s := fSop Oadd srliw_l in
-          let addw_l := make_lhsv_single addw_s in
-          let sraiw_s := fSop (Oshrimm Int.one) addw_l in
-          let sraiw_l := make_lhsv_cmp false sraiw_s sraiw_s in
-          Some (fSop (OEmayundef (MUshrx n)) sraiw_l)
-        else 
-          let sraiw_s := fSop (Oshrimm (Int.repr 31)) hl in
-          let sraiw_l := make_lhsv_single sraiw_s in
-          let srliw_s := fSop (Oshruimm (Int.sub Int.iwordsize n)) sraiw_l in
-          let srliw_l := make_lhsv_cmp false hv1 srliw_s in
-          let addw_s := fSop Oadd srliw_l in
-          let addw_l := make_lhsv_single addw_s in
-          let sraiw_s' := fSop (Oshrimm n) addw_l in
-          let sraiw_l' := make_lhsv_cmp false sraiw_s' sraiw_s' in
-          Some (fSop (OEmayundef (MUshrx n)) sraiw_l')
-  | Oshrxlimm n, a1 :: nil =>
-      let hv1 := fsi_sreg_get hst a1 in
-      let hl := make_lhsv_single hv1 in
-      if Int.eq n Int.zero then
-        let lhl := make_lhsv_cmp false hv1 hv1 in
-        Some (fSop (OEmayundef (MUshrxl n)) lhl)
-      else
-        if Int.eq n Int.one then
-          let srlil_s := fSop (Oshrluimm (Int.repr 63)) hl in
-          let srlil_l := make_lhsv_cmp false hv1 srlil_s in
-          let addl_s := fSop Oaddl srlil_l in
-          let addl_l := make_lhsv_single addl_s in
-          let srail_s := fSop (Oshrlimm Int.one) addl_l in
-          let srail_l := make_lhsv_cmp false srail_s srail_s in
-          Some (fSop (OEmayundef (MUshrxl n)) srail_l)
-        else
-          let srail_s := fSop (Oshrlimm (Int.repr 63)) hl in
-          let srail_l := make_lhsv_single srail_s in
-          let srlil_s := fSop (Oshrluimm (Int.sub Int64.iwordsize' n)) srail_l in
-          let srlil_l := make_lhsv_cmp false hv1 srlil_s in
-          let addl_s := fSop Oaddl srlil_l in
-          let addl_l := make_lhsv_single addl_s in
-          let srail_s' := fSop (Oshrlimm n) addl_l in
-          let srail_l' := make_lhsv_cmp false srail_s' srail_s' in
-          Some (fSop (OEmayundef (MUshrxl n)) srail_l')
-  | _, _ => None
-  end.
-
-Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg) : option (condition * list_hsval) :=
-  match cond, args with
-  | (Ccomp c), (a1 :: a2 :: nil) =>
-      let is_inv := is_inv_cmp_int c in
-      let cond := transl_cbranch_int32s c (make_optR false is_inv) in
-      let hv1 := fsi_sreg_get prev a1 in
-      let hv2 := fsi_sreg_get prev a2 in
-      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
-      Some (cond, lhsv)
-  | (Ccompu c), (a1 :: a2 :: nil) =>
-      let is_inv := is_inv_cmp_int c in
-      let cond := transl_cbranch_int32u c (make_optR false is_inv) in
-      let hv1 := fsi_sreg_get prev a1 in
-      let hv2 := fsi_sreg_get prev a2 in
-      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
-      Some (cond, lhsv)
-  | (Ccompimm c n), (a1 :: nil) =>
-      let is_inv := is_inv_cmp_int c in
-      let hv1 := fsi_sreg_get prev a1 in
-      (if Int.eq n Int.zero then
-        let lhsv := make_lhsv_cmp is_inv hv1 hv1 in
-        let cond := transl_cbranch_int32s c (make_optR true is_inv) in
-        Some (cond, lhsv)
-      else
-        let hvs := loadimm32 n in
-        let lhsv := make_lhsv_cmp is_inv hv1 hvs in
-        let cond := transl_cbranch_int32s c (make_optR false is_inv) in
-        Some (cond, lhsv))
-  | (Ccompuimm c n), (a1 :: nil) =>
-      let is_inv := is_inv_cmp_int c in
-      let hv1 := fsi_sreg_get prev a1 in
-      (if Int.eq n Int.zero then
-        let lhsv := make_lhsv_cmp is_inv hv1 hv1 in
-        let cond := transl_cbranch_int32u c (make_optR true is_inv) in
-        Some (cond, lhsv)
-      else
-        let hvs := loadimm32 n in
-        let lhsv := make_lhsv_cmp is_inv hv1 hvs in
-        let cond := transl_cbranch_int32u c (make_optR false is_inv) in
-         Some (cond, lhsv))
-  | (Ccompl c), (a1 :: a2 :: nil) =>
-      let is_inv := is_inv_cmp_int c in
-      let cond := transl_cbranch_int64s c (make_optR false is_inv) in
-      let hv1 := fsi_sreg_get prev a1 in
-      let hv2 := fsi_sreg_get prev a2 in
-      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
-      Some (cond, lhsv)
-  | (Ccomplu c), (a1 :: a2 :: nil) =>
-      let is_inv := is_inv_cmp_int c in
-      let cond := transl_cbranch_int64u c (make_optR false is_inv) in
-      let hv1 := fsi_sreg_get prev a1 in
-      let hv2 := fsi_sreg_get prev a2 in
-      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
-      Some (cond, lhsv)
-  | (Ccomplimm c n), (a1 :: nil) =>
-      let is_inv := is_inv_cmp_int c in
-      let hv1 := fsi_sreg_get prev a1 in
-      (if Int64.eq n Int64.zero then
-        let lhsv := make_lhsv_cmp is_inv hv1 hv1 in
-        let cond := transl_cbranch_int64s c (make_optR true is_inv) in
-        Some (cond, lhsv)
-      else
-        let hvs := loadimm64 n in
-        let lhsv := make_lhsv_cmp is_inv hv1 hvs in
-        let cond := transl_cbranch_int64s c (make_optR false is_inv) in
-        Some (cond, lhsv))
-  | (Ccompluimm c n), (a1 :: nil) =>
-      let is_inv := is_inv_cmp_int c in
-      let hv1 := fsi_sreg_get prev a1 in
-      (if Int64.eq n Int64.zero then
-        let lhsv := make_lhsv_cmp is_inv hv1 hv1 in
-        let cond := transl_cbranch_int64u c (make_optR true is_inv) in
-        Some (cond, lhsv)
-      else
-        let hvs := loadimm64 n in
-        let lhsv := make_lhsv_cmp is_inv hv1 hvs in
-        let cond := transl_cbranch_int64u c (make_optR false is_inv) in
-        Some (cond, lhsv))
-  | (Ccompf c), (f1 :: f2 :: nil) =>
-      let hv1 := fsi_sreg_get prev f1 in
-      let hv2 := fsi_sreg_get prev f2 in
-      let is_inv := is_inv_cmp_float c in
-      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
-      Some (expanse_cbranch_fp false cond_float c lhsv)
-  | (Cnotcompf c), (f1 :: f2 :: nil) =>
-      let hv1 := fsi_sreg_get prev f1 in
-      let hv2 := fsi_sreg_get prev f2 in
-      let is_inv := is_inv_cmp_float c in
-      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
-      Some (expanse_cbranch_fp true cond_float c lhsv)
-  | (Ccompfs c), (f1 :: f2 :: nil) =>
-      let hv1 := fsi_sreg_get prev f1 in
-      let hv2 := fsi_sreg_get prev f2 in
-      let is_inv := is_inv_cmp_float c in
-      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
-      Some (expanse_cbranch_fp false cond_single c lhsv)
-  | (Cnotcompfs c), (f1 :: f2 :: nil) =>
-      let hv1 := fsi_sreg_get prev f1 in
-      let hv2 := fsi_sreg_get prev f2 in
-      let is_inv := is_inv_cmp_float c in
-      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
-      Some (expanse_cbranch_fp true cond_single c lhsv)
-  | _, _ => None
-   end.
-
-(** * Auxiliary lemmas on comparisons *)
-
-(** ** Signed ints *)
-
-Lemma xor_neg_ltle_cmp: forall v1 v2,
-  Some (Val.xor (Val.cmp Clt v1 v2) (Vint Int.one)) =
-  Some (Val.of_optbool (Val.cmp_bool Cle v2 v1)).
-Proof.
-  intros. eapply f_equal.
-  destruct v1, v2; simpl; try congruence.
-  unfold Val.cmp; simpl;
-  try rewrite Int.eq_sym;
-  try destruct (Int.eq _ _); try destruct (Int.lt _ _) eqn:ELT ; simpl;
-  try rewrite Int.xor_one_one; try rewrite Int.xor_zero_one;
-  auto.
-Qed.
-
-(** ** Unsigned ints *)
-
-Lemma xor_neg_ltle_cmpu: forall mptr v1 v2,
-  Some (Val.xor (Val.cmpu (Mem.valid_pointer mptr) Clt v1 v2) (Vint Int.one)) =
-  Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer mptr) Cle v2 v1)).
-Proof.
-  intros. eapply f_equal.
-  destruct v1, v2; simpl; try congruence.
-  unfold Val.cmpu; simpl;
-  try rewrite Int.eq_sym;
-  try destruct (Int.eq _ _); try destruct (Int.ltu _ _) eqn:ELT ; simpl;
-  try rewrite Int.xor_one_one; try rewrite Int.xor_zero_one;
-  auto.
-  1,2:
-    unfold Val.cmpu, Val.cmpu_bool;
-    destruct Archi.ptr64; try destruct (_ && _); try destruct (_ || _);
-    try destruct (eq_block _ _); auto.
-  unfold Val.cmpu, Val.cmpu_bool; simpl;
-  destruct Archi.ptr64; try destruct (_ || _); simpl; auto;
-  destruct (eq_block b b0); destruct (eq_block b0 b);
-  try congruence;
-  try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _);
-  simpl; auto;
-  repeat destruct (_ && _); simpl; auto.
-Qed.
-
-Remark ltu_12_wordsize:
-  Int.ltu (Int.repr 12) Int.iwordsize = true.
-Proof.
-  unfold Int.iwordsize, Int.zwordsize. simpl.
-  unfold Int.ltu. apply zlt_true.
-  rewrite !Int.unsigned_repr; try cbn; try lia.
-Qed.
-
-(** ** Signed longs *)
-
-Lemma xor_neg_ltle_cmpl: forall v1 v2,
-  Some (Val.xor (Val.maketotal (Val.cmpl Clt v1 v2)) (Vint Int.one)) =
-  Some (Val.of_optbool (Val.cmpl_bool Cle v2 v1)).
-Proof.
-  intros. eapply f_equal.
-  destruct v1, v2; simpl; try congruence.
-  destruct (Int64.lt _ _); auto.
-Qed.
-
-Lemma xor_neg_ltge_cmpl: forall v1 v2,
-  Some (Val.xor (Val.maketotal (Val.cmpl Clt v1 v2)) (Vint Int.one)) =
-  Some (Val.of_optbool (Val.cmpl_bool Cge v1 v2)).
-Proof.
-  intros. eapply f_equal.
-  destruct v1, v2; simpl; try congruence.
-  destruct (Int64.lt _ _); auto.
-Qed.
-
-Lemma xorl_zero_eq_cmpl: forall c v1 v2,
-  c = Ceq \/ c = Cne ->
-  Some
-    (Val.maketotal
-     (option_map Val.of_bool
-       (Val.cmpl_bool c (Val.xorl v1 v2) (Vlong Int64.zero)))) =
-  Some (Val.of_optbool (Val.cmpl_bool c v1 v2)).
-Proof.
-  intros. destruct c; inv H; try discriminate;
-  destruct v1, v2; simpl; auto;
-  destruct (Int64.eq i i0) eqn:EQ0.
-  1,3:
-    apply Int64.same_if_eq in EQ0; subst;
-    rewrite Int64.xor_idem;
-    rewrite Int64.eq_true; trivial.
-  1,2:
-    destruct (Int64.eq (Int64.xor i i0) Int64.zero) eqn:EQ1; simpl; try congruence;
-    rewrite Int64.xor_is_zero in EQ1; congruence.
-Qed.
-
-Lemma cmp_ltle_add_one: forall v n,
-  Int.eq n (Int.repr Int.max_signed) = false ->
-  Some (Val.of_optbool (Val.cmp_bool Clt v (Vint (Int.add n Int.one)))) =
-  Some (Val.of_optbool (Val.cmp_bool Cle v (Vint n))).
-Proof.
-  intros v n EQMAX. unfold Val.cmp_bool; destruct v; simpl; auto.
-  unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1).
-  destruct (zlt (Int.signed n) (Int.signed i)).
-  rewrite zlt_false by 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.
-
-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.
-
-Remark lt_maxsgn_false_int: forall i,
-  Int.lt (Int.repr Int.max_signed) i = false.
-Proof.
-  intros; unfold Int.lt.
-  specialize  Int.signed_range with i; intros.
-  rewrite zlt_false; auto. destruct H.
-  rewrite Int.signed_repr; try (cbn; lia).
-  apply Z.le_ge. trivial.
-Qed.
-
-Remark lt_maxsgn_false_long: forall i,
-  Int64.lt (Int64.repr Int64.max_signed) i = false.
-Proof.
-  intros; unfold Int64.lt.
-  specialize  Int64.signed_range with i; intros.
-  rewrite zlt_false; auto. destruct H.
-  rewrite Int64.signed_repr; try (cbn; lia).
-  apply Z.le_ge. trivial.
-Qed.
-
-(** ** Unsigned longs *)
-
-Lemma xor_neg_ltle_cmplu: forall mptr v1 v2,
-  Some (Val.xor (Val.maketotal (Val.cmplu (Mem.valid_pointer mptr) Clt v1 v2)) (Vint Int.one)) =
-  Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer mptr) Cle v2 v1)).
-Proof.
-  intros. eapply f_equal.
-  destruct v1, v2; simpl; try congruence.
-  destruct (Int64.ltu _ _); auto.
-  1,2: unfold Val.cmplu; simpl; auto;
-  destruct (Archi.ptr64); simpl;
-  try destruct (eq_block _ _); simpl;
-  try destruct (_ && _); simpl;
-  try destruct (Ptrofs.cmpu _ _);
-  try destruct cmp; simpl; auto.
-  unfold Val.cmplu; simpl;
-  destruct Archi.ptr64; try destruct (_ || _); simpl; auto;
-  destruct (eq_block b b0); destruct (eq_block b0 b);
-  try congruence;
-  try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _);
-  simpl; auto;
-  repeat destruct (_ && _); simpl; auto.
-Qed.
-
-Lemma xor_neg_ltge_cmplu: forall mptr v1 v2,
-  Some (Val.xor (Val.maketotal (Val.cmplu (Mem.valid_pointer mptr) Clt v1 v2)) (Vint Int.one)) =
-  Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer mptr) Cge v1 v2)).
-Proof.
-  intros. eapply f_equal.
-  destruct v1, v2; simpl; try congruence.
-  destruct (Int64.ltu _ _); auto.
-  1,2: unfold Val.cmplu; simpl; auto;
-  destruct (Archi.ptr64); simpl;
-  try destruct (eq_block _ _); simpl;
-  try destruct (_ && _); simpl;
-  try destruct (Ptrofs.cmpu _ _);
-  try destruct cmp; simpl; auto.
-  unfold Val.cmplu; simpl;
-  destruct Archi.ptr64; try destruct (_ || _); simpl; auto;
-  destruct (eq_block b b0); destruct (eq_block b0 b);
-  try congruence;
-  try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _);
-  simpl; auto;
-  repeat destruct (_ && _); simpl; auto.
-Qed.
-
-(** ** Floats *)
-
-Lemma xor_neg_eqne_cmpf: forall v1 v2,
-  Some (Val.xor (Val.cmpf Ceq v1 v2) (Vint Int.one)) =
-  Some (Val.of_optbool (Val.cmpf_bool Cne v1 v2)).
-Proof.
-  intros. eapply f_equal.
-  destruct v1, v2; simpl; try congruence;
-  unfold Val.cmpf; simpl.
-  rewrite Float.cmp_ne_eq.
-  destruct (Float.cmp _ _ _); simpl; auto.
-Qed.
-
-(** ** Singles *)
-
-Lemma xor_neg_eqne_cmpfs: forall v1 v2,
-  Some (Val.xor (Val.cmpfs Ceq v1 v2) (Vint Int.one)) =
-  Some (Val.of_optbool (Val.cmpfs_bool Cne v1 v2)).
-Proof.
-  intros. eapply f_equal.
-  destruct v1, v2; simpl; try congruence;
-  unfold Val.cmpfs; simpl.
-  rewrite Float32.cmp_ne_eq.
-  destruct (Float32.cmp _ _ _); simpl; auto.
-Qed.
-
-(** ** More useful lemmas *)
-
-Lemma xor_neg_optb: forall v,
-  Some (Val.xor (Val.of_optbool (option_map negb v))
-    (Vint Int.one)) = Some (Val.of_optbool v).
-Proof.
-  intros.
-  destruct v; simpl; trivial.
-  destruct b; simpl; auto.
-Qed.
-
-Lemma xor_neg_optb': forall v,
-  Some (Val.xor (Val.of_optbool v) (Vint Int.one)) =
-  Some (Val.of_optbool (option_map negb v)).
-Proof.
-  intros.
-  destruct v; simpl; trivial.
-  destruct b; simpl; auto.
-Qed.
-
-Lemma optbool_mktotal: forall v,
-  Val.maketotal (option_map Val.of_bool v) =
-  Val.of_optbool v.
-Proof.
-  intros.
-  destruct v; simpl; auto.
-Qed.
-
-(** * Intermediates lemmas on each expanded instruction *)
-
-Lemma simplify_ccomp_correct ge sp hst st c r r0 rs0 m0 v v0: forall
-  (SREG: forall r: positive,
-          hsi_sreg_eval ge sp hst r rs0 m0 =
-          seval_sval ge sp (si_sreg st r) rs0 m0)
-  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
-  (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0),
-  seval_sval ge sp
-    (hsval_proj
-       (cond_int32s c
-          (make_lhsv_cmp (is_inv_cmp_int c) (fsi_sreg_get hst r)
-             (fsi_sreg_get hst r0)) None)) rs0 m0 =
-  Some (Val.of_optbool (Val.cmp_bool c v v0)).
-Proof.
-  intros.
-  unfold cond_int32s in *; destruct c; simpl;
-  erewrite !fsi_sreg_get_correct; eauto;
-  rewrite OKv1, OKv2; trivial;
-  unfold Val.cmp.
-  - apply xor_neg_ltle_cmp.
-  - replace (Clt) with (swap_comparison Cgt) by auto;
-    rewrite Val.swap_cmp_bool; trivial.
-  - replace (Clt) with (negate_comparison Cge) by auto;
-    rewrite Val.negate_cmp_bool.
-    rewrite xor_neg_optb; trivial.
-Qed.
-
-Lemma simplify_ccompu_correct ge sp hst st c r r0 rs0 m m0 v v0: forall
-  (SMEM : forall (m : mem) (b : Values.block) (ofs : Z),
-           seval_smem ge sp (si_smem st) rs0 m0 = Some m ->
-           Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
-  (SREG: forall r: positive,
-          hsi_sreg_eval ge sp hst r rs0 m0 =
-          seval_sval ge sp (si_sreg st r) rs0 m0)
-  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
-  (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0)
-  (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m),
-  seval_sval ge sp
-    (hsval_proj
-       (cond_int32u c
-          (make_lhsv_cmp (is_inv_cmp_int c) (fsi_sreg_get hst r)
-             (fsi_sreg_get hst r0)) None)) rs0 m0 =
-  Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer m) c v v0)).
-Proof.
-  intros.
-  erewrite (cmpu_bool_valid_pointer_eq (Mem.valid_pointer m) (Mem.valid_pointer m0)).
-  2: eauto.
-  unfold cond_int32u in *; destruct c; simpl;
-  erewrite !fsi_sreg_get_correct; eauto;
-  rewrite OKv1, OKv2; trivial;
-  unfold Val.cmpu.
-  - apply xor_neg_ltle_cmpu.
-  - replace (Clt) with (swap_comparison Cgt) by auto;
-    rewrite Val.swap_cmpu_bool; trivial.
-  - replace (Clt) with (negate_comparison Cge) by auto;
-    rewrite Val.negate_cmpu_bool.
-    rewrite xor_neg_optb; trivial.
-Qed.
-
-Lemma simplify_ccompimm_correct ge sp hst st c r n rs0 m m0 v: forall
-  (SMEM : forall (m : mem) (b : Values.block) (ofs : Z),
-           seval_smem ge sp (si_smem st) rs0 m0 = Some m ->
-           Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
-  (SREG: forall r: positive,
-          hsi_sreg_eval ge sp hst r rs0 m0 =
-          seval_sval ge sp (si_sreg st r) rs0 m0)
-  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
-  (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m),
-  seval_sval ge sp
-    (hsval_proj (expanse_condimm_int32s c (fsi_sreg_get hst r) n)) rs0 m0 =
-  Some (Val.of_optbool (Val.cmp_bool c v (Vint n))).
-Proof.
-  intros.
-  unfold expanse_condimm_int32s, cond_int32s in *; destruct c;
-  intros; destruct (Int.eq n Int.zero) eqn:EQIMM; simpl;
-  try apply Int.same_if_eq in EQIMM; subst;
-  unfold loadimm32, sltimm32, xorimm32, opimm32, load_hilo32;
-  try erewrite !fsi_sreg_get_correct; eauto;
-  try rewrite OKv1;
-  unfold Val.cmp, zero32.
-  all:
-    try apply xor_neg_ltle_cmp; 
-    try apply xor_neg_ltge_cmp; trivial.
-  4: 
-    try destruct (Int.eq n (Int.repr Int.max_signed)) eqn:EQMAX; subst;
-    try apply Int.same_if_eq in EQMAX; subst; simpl.
-  4:
-    intros; try (specialize make_immed32_sound with (Int.one);
-    destruct (make_immed32 Int.one) eqn:EQMKI_A1); intros; simpl.
-  6:
-    intros; try (specialize make_immed32_sound with (Int.add n Int.one);
-    destruct (make_immed32 (Int.add n Int.one)) eqn:EQMKI_A2); intros; simpl.
-  1,2,3,8,9:
-    intros; try (specialize make_immed32_sound with (n);
-    destruct (make_immed32 n) eqn:EQMKI); intros; simpl.
-  all: 
-    try destruct (Int.eq lo Int.zero) eqn:EQLO32;
-    try apply Int.same_if_eq in EQLO32; subst;
-    try erewrite fSop_correct; eauto; simpl;
-    try erewrite !fsi_sreg_get_correct; eauto;
-    try rewrite OKv1;
-    try rewrite OK2;
-    try rewrite (Int.add_commut _ Int.zero), Int.add_zero_l in H; subst;
-    unfold Val.cmp, 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 rewrite Int.add_commut;
-    try rewrite <- H; try rewrite cmp_ltle_add_one;
-    try rewrite Int.add_zero_l;
-    try (
-    simpl; trivial;
-    try rewrite Int.xor_is_zero;
-    try destruct (Int.lt _ _) eqn:EQLT; trivial;
-    try rewrite lt_maxsgn_false_int in EQLT;
-    simpl; trivial; try discriminate; fail).
-Qed.
-
-Lemma simplify_ccompuimm_correct ge sp hst st c r n rs0 m m0 v: forall
-  (SMEM : forall (m : mem) (b : Values.block) (ofs : Z),
-           seval_smem ge sp (si_smem st) rs0 m0 = Some m ->
-           Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
-  (SREG: forall r: positive,
-          hsi_sreg_eval ge sp hst r rs0 m0 =
-          seval_sval ge sp (si_sreg st r) rs0 m0)
-  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
-  (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m),
-  seval_sval ge sp
-    (hsval_proj (expanse_condimm_int32u c (fsi_sreg_get hst r) n)) rs0 m0 =
-  Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer m) c v (Vint n))).
-Proof.
-  intros.
-  assert (HMEM: Val.cmpu_bool (Mem.valid_pointer m) c v (Vint n) =
-          Val.cmpu_bool (Mem.valid_pointer m0) c v (Vint n)).
-  erewrite (cmpu_bool_valid_pointer_eq (Mem.valid_pointer m) (Mem.valid_pointer m0)); eauto.
-  unfold expanse_condimm_int32u, cond_int32u in *; destruct c;
-  intros; destruct (Int.eq n Int.zero) eqn:EQIMM; simpl;
-  try apply Int.same_if_eq in EQIMM; subst;
-  unfold loadimm32, sltuimm32, opimm32, load_hilo32;
-  try erewrite !fsi_sreg_get_correct; eauto;
-  try rewrite OKv1; trivial;
-  try rewrite xor_neg_ltle_cmpu;
-  unfold Val.cmpu, zero32.
-  all:
-    try (specialize make_immed32_sound with n;
-    destruct (make_immed32 n) eqn:EQMKI);
-    try destruct (Int.eq lo Int.zero) eqn:EQLO;
-    try apply Int.same_if_eq in EQLO; subst;
-    intros; subst;
-    try erewrite fSop_correct; eauto; simpl;
-    try erewrite !fsi_sreg_get_correct; eauto;
-    try rewrite OKv1;
-    try rewrite OK2;
-    rewrite HMEM;
-    unfold 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 rewrite Int.add_zero_l;
-    try destruct (Int.ltu _ _) eqn:EQLTU; simpl;
-    try rewrite EQLTU; simpl; try rewrite EQIMM;
-    try rewrite EQARCH; trivial.
-Qed.
-
-Lemma simplify_ccompl_correct ge sp hst st c r r0 rs0 m0 v v0: forall
-  (SREG: forall r: positive,
-          hsi_sreg_eval ge sp hst r rs0 m0 =
-          seval_sval ge sp (si_sreg st r) rs0 m0)
-  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
-  (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0),
-  seval_sval ge sp
-    (hsval_proj
-       (cond_int64s c
-          (make_lhsv_cmp (is_inv_cmp_int c) (fsi_sreg_get hst r)
-             (fsi_sreg_get hst r0)) None)) rs0 m0 =
-  Some (Val.of_optbool (Val.cmpl_bool c v v0)).
-Proof.
-  intros.
-  unfold cond_int64s in *; destruct c; simpl;
-  erewrite !fsi_sreg_get_correct; eauto;
-  rewrite OKv1, OKv2; trivial;
-  unfold Val.cmpl.
-  1,2,3: rewrite optbool_mktotal; trivial.
-  - apply xor_neg_ltle_cmpl.
-  - replace (Clt) with (swap_comparison Cgt) by auto;
-    rewrite Val.swap_cmpl_bool; trivial.
-    rewrite optbool_mktotal; trivial.
-  - apply xor_neg_ltge_cmpl.
-Qed.
-
-Lemma simplify_ccomplu_correct ge sp hst st c r r0 rs0 m m0 v v0: forall
-  (SMEM : forall (m : mem) (b : Values.block) (ofs : Z),
-           seval_smem ge sp (si_smem st) rs0 m0 = Some m ->
-           Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
-  (SREG: forall r: positive,
-          hsi_sreg_eval ge sp hst r rs0 m0 =
-          seval_sval ge sp (si_sreg st r) rs0 m0)
-  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
-  (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0)
-  (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m),
-  seval_sval ge sp
-    (hsval_proj
-       (cond_int64u c
-          (make_lhsv_cmp (is_inv_cmp_int c) (fsi_sreg_get hst r)
-             (fsi_sreg_get hst r0)) None)) rs0 m0 =
-  Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer m) c v v0)).
-Proof.
-  intros.
-  erewrite (cmplu_bool_valid_pointer_eq (Mem.valid_pointer m) (Mem.valid_pointer m0)).
-  2: eauto.
-  unfold cond_int64u in *; destruct c; simpl;
-  erewrite !fsi_sreg_get_correct; eauto;
-  rewrite OKv1, OKv2; trivial;
-  unfold Val.cmplu.
-  1,2,3: rewrite optbool_mktotal; trivial.
-  - apply xor_neg_ltle_cmplu.
-  - replace (Clt) with (swap_comparison Cgt) by auto;
-    rewrite Val.swap_cmplu_bool; trivial.
-    rewrite optbool_mktotal; trivial.
-  - apply xor_neg_ltge_cmplu.
-Qed.
-
-Lemma simplify_ccomplimm_correct ge sp hst st c r n rs0 m m0 v: forall
-  (SMEM : forall (m : mem) (b : Values.block) (ofs : Z),
-           seval_smem ge sp (si_smem st) rs0 m0 = Some m ->
-           Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
-  (SREG: forall r: positive,
-          hsi_sreg_eval ge sp hst r rs0 m0 =
-          seval_sval ge sp (si_sreg st r) rs0 m0)
-  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
-  (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m),
-  seval_sval ge sp
-    (hsval_proj (expanse_condimm_int64s c (fsi_sreg_get hst r) n)) rs0 m0 =
-  Some (Val.of_optbool (Val.cmpl_bool c v (Vlong n))).
-Proof.
-  intros.
-  unfold expanse_condimm_int64s, cond_int64s in *; destruct c;
-  intros; destruct (Int64.eq n Int64.zero) eqn:EQIMM; simpl;
-  try apply Int64.same_if_eq in EQIMM; subst;
-  unfold loadimm32, loadimm64, sltimm64, xorimm64, opimm64, load_hilo32, load_hilo64;
-  try erewrite !fsi_sreg_get_correct; eauto;
-  try rewrite OKv1;
-  unfold Val.cmpl, zero64.
-  all:
-    try apply xor_neg_ltle_cmpl; 
-    try apply xor_neg_ltge_cmpl;
-    try rewrite optbool_mktotal; trivial.
-  4: 
-    try destruct (Int64.eq n (Int64.repr Int64.max_signed)) eqn:EQMAX; subst;
-    try apply Int64.same_if_eq in EQMAX; subst; simpl.
-  4:
-    intros; try (specialize make_immed32_sound with (Int.one);
-    destruct (make_immed32 Int.one) eqn:EQMKI_A1); intros; simpl.
-  6:
-    intros; try (specialize make_immed64_sound with (Int64.add n Int64.one);
-    destruct (make_immed64 (Int64.add n Int64.one)) eqn:EQMKI_A2); intros; simpl.
-  1,2,3,9,10:
-    intros; try (specialize make_immed64_sound with (n);
-    destruct (make_immed64 n) eqn:EQMKI); intros; simpl.
-  all: 
-    try destruct (Int.eq lo Int.zero) eqn:EQLO32;
-    try apply Int.same_if_eq in EQLO32; subst;
-    try destruct (Int64.eq lo Int64.zero) eqn:EQLO64;
-    try apply Int64.same_if_eq in EQLO64; subst;
-    try erewrite fSop_correct; eauto; simpl;
-    try erewrite !fsi_sreg_get_correct; eauto;
-    try rewrite OKv1;
-    try rewrite OK2;
-    try rewrite (Int64.add_commut _ Int64.zero), Int64.add_zero_l in H; subst;
-    try fold (Val.cmpl Clt v (Vlong imm));
-    try rewrite xor_neg_ltge_cmpl; trivial;
-    try rewrite xor_neg_ltle_cmpl; trivial;
-    unfold Val.cmpl, Val.addl;
-    try rewrite xorl_zero_eq_cmpl; trivial;
-    try rewrite optbool_mktotal; trivial;
-    unfold eval_may_undef, zero32, Val.add; simpl;
-    destruct v; auto.
-  1,2,3,4,5,6,7,8,9,10,11,12:
-      try rewrite <- optbool_mktotal; trivial;
-      try rewrite Int64.add_commut, Int64.add_zero_l in *;
-      try fold (Val.cmpl Clt (Vlong i) (Vlong imm));
-      try fold (Val.cmpl Clt (Vlong i) (Vlong (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12)))));
-      try fold (Val.cmpl Clt (Vlong i) (Vlong (Int64.add (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) lo)));
-      try rewrite xor_neg_ltge_cmpl; trivial;
-      try rewrite xor_neg_ltle_cmpl; trivial.
-  6:
-    rewrite <- H;
-    try apply cmpl_ltle_add_one; auto.
-  all:
-    try rewrite <- H;
-    try apply cmpl_ltle_add_one; auto;
-    try rewrite <- cmpl_ltle_add_one; auto;
-    try rewrite ltu_12_wordsize;
-    try rewrite Int.add_commut, Int.add_zero_l in *;
-    try rewrite Int64.add_commut, Int64.add_zero_l in *;
-    try rewrite Int64.add_zero_l;
-    simpl; try rewrite lt_maxsgn_false_long;
-    try (rewrite <- H; trivial; fail);
-    simpl; trivial.
-Qed.
-
-Lemma simplify_ccompluimm_correct ge sp hst st c r n rs0 m m0 v: forall
-  (SMEM : forall (m : mem) (b : Values.block) (ofs : Z),
-           seval_smem ge sp (si_smem st) rs0 m0 = Some m ->
-           Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
-  (SREG: forall r: positive,
-          hsi_sreg_eval ge sp hst r rs0 m0 =
-          seval_sval ge sp (si_sreg st r) rs0 m0)
-  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
-  (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m),
-  seval_sval ge sp
-    (hsval_proj (expanse_condimm_int64u c (fsi_sreg_get hst r) n)) rs0 m0 =
-  Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer m) c v (Vlong n))).
-Proof.
-  intros.
-  assert (HMEM: Val.cmplu_bool (Mem.valid_pointer m) c v (Vlong n) =
-          Val.cmplu_bool (Mem.valid_pointer m0) c v (Vlong n)).
-  erewrite (cmplu_bool_valid_pointer_eq (Mem.valid_pointer m) (Mem.valid_pointer m0)); eauto.
-  unfold expanse_condimm_int64u, cond_int64u in *; destruct c;
-  intros; destruct (Int64.eq n Int64.zero) eqn:EQIMM; simpl;
-  unfold loadimm64, sltuimm64, opimm64, load_hilo64;
-  try erewrite !fsi_sreg_get_correct; eauto;
-  try rewrite OKv1;
-  unfold Val.cmplu, zero64.
-  (* Simplify make immediate and decompose subcases *)
-  all:
-    try (specialize make_immed64_sound with n;
-    destruct (make_immed64 n) eqn:EQMKI);
-    try destruct (Int64.eq lo Int64.zero) eqn:EQLO;
-    try erewrite fSop_correct; eauto; simpl;
-    try erewrite !fsi_sreg_get_correct; eauto;
-    try rewrite OKv1;
-    try rewrite OK2;
-    rewrite HMEM.
-  (* Ceq, Cne, Clt = itself *)
-  all: intros; try apply Int64.same_if_eq in EQIMM; subst; trivial.
-  (* Cle = xor (Clt) *)
-  all: try apply xor_neg_ltle_cmplu; trivial.
-  (* Others subcases with swap/negation *)
-  all:
-    unfold Val.cmplu, 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 Int64.add_zero_l;
-    try (rewrite <- xor_neg_ltle_cmplu; unfold Val.cmplu;
-    trivial; fail);
-    try (replace (Clt) with (swap_comparison Cgt) by auto;
-    rewrite Val.swap_cmplu_bool; trivial; fail);
-    try (replace (Clt) with (negate_comparison Cge) by auto;
-    rewrite Val.negate_cmplu_bool; rewrite xor_neg_optb; trivial; fail);
-    try rewrite optbool_mktotal; trivial.
-  all:
-    try destruct v; simpl; auto;
-    try destruct (Archi.ptr64); simpl;
-    try rewrite EQIMM;
-    try rewrite HMEM; trivial;
-    try destruct (Int64.ltu _ _);
-    try rewrite <- xor_neg_ltge_cmplu; unfold Val.cmplu;
-    try rewrite <- optbool_mktotal; trivial.
-Qed.
-
-Lemma simplify_ccompf_correct ge sp hst st c r r0 rs0 m0 v v0: forall
-  (SREG: forall r: positive,
-          hsi_sreg_eval ge sp hst r rs0 m0 =
-          seval_sval ge sp (si_sreg st r) rs0 m0)
-  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
-  (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0),
-  seval_sval ge sp
-    (hsval_proj
-       (expanse_cond_fp false cond_float c
-          (make_lhsv_cmp (is_inv_cmp_float c) (fsi_sreg_get hst r)
-             (fsi_sreg_get hst r0)))) rs0 m0 =
-  Some (Val.of_optbool (Val.cmpf_bool c v v0)).
-Proof.
-  intros.
-  unfold expanse_cond_fp in *; destruct c; simpl;
-  erewrite !fsi_sreg_get_correct; eauto;
-  rewrite OKv1, OKv2; trivial;
-  unfold Val.cmpf.
-  - apply xor_neg_eqne_cmpf.
-  - replace (Clt) with (swap_comparison Cgt) by auto;
-    rewrite Val.swap_cmpf_bool; trivial.
-  - replace (Cle) with (swap_comparison Cge) by auto;
-    rewrite Val.swap_cmpf_bool; trivial.
-Qed.
-
-Lemma simplify_cnotcompf_correct ge sp hst st c r r0 rs0 m0 v v0: forall
-  (SREG: forall r: positive,
-          hsi_sreg_eval ge sp hst r rs0 m0 =
-          seval_sval ge sp (si_sreg st r) rs0 m0)
-  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
-  (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0),
-  seval_sval ge sp
-    (hsval_proj
-       (expanse_cond_fp true cond_float c
-          (make_lhsv_cmp (is_inv_cmp_float c) (fsi_sreg_get hst r)
-             (fsi_sreg_get hst r0)))) rs0 m0 =
-  Some (Val.of_optbool (option_map negb (Val.cmpf_bool c v v0))).
-Proof.
-  intros.
-  unfold expanse_cond_fp in *; destruct c; simpl;
-  erewrite !fsi_sreg_get_correct; eauto;
-  rewrite OKv1, OKv2; trivial;
-  unfold Val.cmpf.
-  1,3,4: apply xor_neg_optb'.
-  all: destruct v, v0; simpl; trivial.
-  rewrite Float.cmp_ne_eq; rewrite negb_involutive; trivial.
-  1: replace (Clt) with (swap_comparison Cgt) by auto; rewrite <- Float.cmp_swap; simpl.
-  2: replace (Cle) with (swap_comparison Cge) by auto; rewrite <- Float.cmp_swap; simpl.
-  all: destruct (Float.cmp _ _ _); trivial.
-Qed.
-
-Lemma simplify_ccompfs_correct ge sp hst st c r r0 rs0 m0 v v0: forall
-  (SREG: forall r: positive,
-          hsi_sreg_eval ge sp hst r rs0 m0 =
-          seval_sval ge sp (si_sreg st r) rs0 m0)
-  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
-  (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0),
-  seval_sval ge sp
-    (hsval_proj
-       (expanse_cond_fp false cond_single c
-          (make_lhsv_cmp (is_inv_cmp_float c) (fsi_sreg_get hst r)
-             (fsi_sreg_get hst r0)))) rs0 m0 =
-  Some (Val.of_optbool (Val.cmpfs_bool c v v0)).
-Proof.
-  intros.
-  unfold expanse_cond_fp in *; destruct c; simpl;
-  erewrite !fsi_sreg_get_correct; eauto;
-  rewrite OKv1, OKv2; trivial;
-  unfold Val.cmpfs.
-  - apply xor_neg_eqne_cmpfs.
-  - replace (Clt) with (swap_comparison Cgt) by auto;
-    rewrite Val.swap_cmpfs_bool; trivial.
-  - replace (Cle) with (swap_comparison Cge) by auto;
-    rewrite Val.swap_cmpfs_bool; trivial.
-Qed.
-
-Lemma simplify_cnotcompfs_correct ge sp hst st c r r0 rs0 m0 v v0: forall
-  (SREG: forall r: positive,
-          hsi_sreg_eval ge sp hst r rs0 m0 =
-          seval_sval ge sp (si_sreg st r) rs0 m0)
-  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
-  (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0),
-  seval_sval ge sp
-    (hsval_proj
-       (expanse_cond_fp true cond_single c
-          (make_lhsv_cmp (is_inv_cmp_float c) (fsi_sreg_get hst r)
-             (fsi_sreg_get hst r0)))) rs0 m0 =
-  Some (Val.of_optbool (option_map negb (Val.cmpfs_bool c v v0))).
-Proof.
-  intros.
-  unfold expanse_cond_fp in *; destruct c; simpl;
-  erewrite !fsi_sreg_get_correct; eauto;
-  rewrite OKv1, OKv2; trivial;
-  unfold Val.cmpfs.
-  1,3,4: apply xor_neg_optb'.
-  all: destruct v, v0; simpl; trivial.
-  rewrite Float32.cmp_ne_eq; rewrite negb_involutive; trivial.
-  1: replace (Clt) with (swap_comparison Cgt) by auto; rewrite <- Float32.cmp_swap; simpl.
-  2: replace (Cle) with (swap_comparison Cge) by auto; rewrite <- Float32.cmp_swap; simpl.
-  all: destruct (Float32.cmp _ _ _); trivial.
-Qed.
-
-Lemma simplify_floatconst_correct ge sp rs0 m0 args m n fsv lr st: forall
-  (H : match lr with
-    | nil =>
-        Some
-          (fSop Ofloat_of_bits
-             (make_lhsv_single (loadimm64 (Float.to_bits n))))
-    | _ :: _ => None
-    end = Some fsv)
-  (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args),
-  seval_sval ge sp (hsval_proj fsv) rs0 m0 =
-  eval_operation ge sp (Ofloatconst n) args m.
-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 ge sp rs0 m0 args m n fsv lr st: forall
-  (H : match lr with
-    | nil =>
-        Some
-          (fSop Osingle_of_bits
-             (make_lhsv_single (loadimm32 (Float32.to_bits n))))
-    | _ :: _ => None
-    end = Some fsv)
-  (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args),
-  seval_sval ge sp (hsval_proj fsv) rs0 m0 =
-  eval_operation ge sp (Osingleconst n) args m.
-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_addimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall
-  (SREG: forall r: positive,
-          hsi_sreg_eval ge sp hst r rs0 m0 =
-          seval_sval ge sp (si_sreg st r) rs0 m0)
-  (H : match lr with
-    | nil => None
-    | a1 :: nil => Some (addimm32 (fsi_sreg_get hst a1) n None)
-    | a1 :: _ :: _ => None
-    end = Some fsv)
-  (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args),
-  seval_sval ge sp (hsval_proj fsv) rs0 m0 =
-  eval_operation ge sp (Oaddimm n) args m.
-Proof.
-  intros.
-  repeat (destruct lr; simpl; try congruence);
-  simpl in OK1; inv OK1; inv H; simpl;
-  unfold addimm32, opimm32, load_hilo32, make_lhsv_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;
-  erewrite !fsi_sreg_get_correct; eauto;
-  destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1.
-  fold (Val.add (Vint imm) v); rewrite Val.add_commut; trivial.
-  all:
-    try apply Int.same_if_eq in EQLO; subst;
-    try rewrite Int.add_commut, Int.add_zero_l;
-    try rewrite ltu_12_wordsize; trivial.
-Qed.
-
-Lemma simplify_addlimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall
-  (SREG: forall r: positive,
-          hsi_sreg_eval ge sp hst r rs0 m0 =
-          seval_sval ge sp (si_sreg st r) rs0 m0)
-  (H : match lr with
-    | nil => None
-    | a1 :: nil => Some (addimm64 (fsi_sreg_get hst a1) n None)
-    | a1 :: _ :: _ => None
-    end = Some fsv)
-  (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args),
-  seval_sval ge sp (hsval_proj fsv) rs0 m0 =
-  eval_operation ge sp (Oaddlimm n) args m.
-Proof.
-  intros.
-  repeat (destruct lr; simpl; try congruence);
-  simpl in OK1; inv OK1; inv H; simpl;
-  unfold addimm64, opimm64, load_hilo64, make_lhsv_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;
-  erewrite !fsi_sreg_get_correct; eauto;
-  destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1.
-  fold (Val.addl (Vlong imm) v); rewrite Val.addl_commut; trivial.
-  all:
-    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; trivial.
-Qed.
-
-Lemma simplify_andimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall
-  (SREG: forall r: positive,
-          hsi_sreg_eval ge sp hst r rs0 m0 =
-          seval_sval ge sp (si_sreg st r) rs0 m0)
-  (H : match lr with
-    | nil => None
-    | a1 :: nil => Some (andimm32 (fsi_sreg_get hst a1) n)
-    | a1 :: _ :: _ => None
-    end = Some fsv)
-  (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args),
-  seval_sval ge sp (hsval_proj fsv) rs0 m0 =
-  eval_operation ge sp (Oandimm n) args m.
-Proof.
-  intros.
-  repeat (destruct lr; simpl; try congruence);
-  simpl in OK1; inv OK1; inv H; simpl;
-  unfold andimm32, opimm32, load_hilo32, make_lhsv_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;
-  erewrite !fsi_sreg_get_correct; eauto;
-  destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1.
-  fold (Val.and (Vint imm) v); rewrite Val.and_commut; trivial.
-  all:
-    try apply Int.same_if_eq in EQLO; subst;
-    try rewrite Int.add_commut, Int.add_zero_l;
-    try rewrite ltu_12_wordsize; trivial.
-Qed.
-
-Lemma simplify_andlimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall
-  (SREG: forall r: positive,
-          hsi_sreg_eval ge sp hst r rs0 m0 =
-          seval_sval ge sp (si_sreg st r) rs0 m0)
-  (H : match lr with
-    | nil => None
-    | a1 :: nil => Some (andimm64 (fsi_sreg_get hst a1) n)
-    | a1 :: _ :: _ => None
-    end = Some fsv)
-  (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args),
-  seval_sval ge sp (hsval_proj fsv) rs0 m0 =
-  eval_operation ge sp (Oandlimm n) args m.
-Proof.
-  intros.
-  repeat (destruct lr; simpl; try congruence);
-  simpl in OK1; inv OK1; inv H; simpl;
-  unfold andimm64, opimm64, load_hilo64, make_lhsv_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;
-  erewrite !fsi_sreg_get_correct; eauto;
-  destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1.
-  fold (Val.andl (Vlong imm) v); rewrite Val.andl_commut; trivial.
-  all:
-    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; trivial.
-Qed.
-
-Lemma simplify_orimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall
-  (SREG: forall r: positive,
-          hsi_sreg_eval ge sp hst r rs0 m0 =
-          seval_sval ge sp (si_sreg st r) rs0 m0)
-  (H : match lr with
-    | nil => None
-    | a1 :: nil => Some (orimm32 (fsi_sreg_get hst a1) n)
-    | a1 :: _ :: _ => None
-    end = Some fsv)
-  (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args),
-  seval_sval ge sp (hsval_proj fsv) rs0 m0 =
-  eval_operation ge sp (Oorimm n) args m.
-Proof.
-  intros.
-  repeat (destruct lr; simpl; try congruence);
-  simpl in OK1; inv OK1; inv H; simpl;
-  unfold orimm32, opimm32, load_hilo32, make_lhsv_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;
-  erewrite !fsi_sreg_get_correct; eauto;
-  destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1.
-  fold (Val.or (Vint imm) v); rewrite Val.or_commut; trivial.
-  all:
-    try apply Int.same_if_eq in EQLO; subst;
-    try rewrite Int.add_commut, Int.add_zero_l;
-    try rewrite ltu_12_wordsize; trivial.
-Qed.
-
-Lemma simplify_orlimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall
-  (SREG: forall r: positive,
-          hsi_sreg_eval ge sp hst r rs0 m0 =
-          seval_sval ge sp (si_sreg st r) rs0 m0)
-  (H : match lr with
-    | nil => None
-    | a1 :: nil => Some (orimm64 (fsi_sreg_get hst a1) n)
-    | a1 :: _ :: _ => None
-    end = Some fsv)
-  (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args),
-  seval_sval ge sp (hsval_proj fsv) rs0 m0 =
-  eval_operation ge sp (Oorlimm n) args m.
-Proof.
-  intros.
-  repeat (destruct lr; simpl; try congruence);
-  simpl in OK1; inv OK1; inv H; simpl;
-  unfold orimm64, opimm64, load_hilo64, make_lhsv_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;
-  erewrite !fsi_sreg_get_correct; eauto;
-  destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1.
-  fold (Val.orl (Vlong imm) v); rewrite Val.orl_commut; trivial.
-  all:
-    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; trivial.
-Qed.
-
-Lemma simplify_xorimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall
-  (SREG: forall r: positive,
-          hsi_sreg_eval ge sp hst r rs0 m0 =
-          seval_sval ge sp (si_sreg st r) rs0 m0)
-  (H : match lr with
-    | nil => None
-    | a1 :: nil => Some (xorimm32 (fsi_sreg_get hst a1) n)
-    | a1 :: _ :: _ => None
-    end = Some fsv)
-  (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args),
-  seval_sval ge sp (hsval_proj fsv) rs0 m0 =
-  eval_operation ge sp (Oxorimm n) args m.
-Proof.
-  intros.
-  repeat (destruct lr; simpl; try congruence);
-  simpl in OK1; inv OK1; inv H; simpl;
-  unfold xorimm32, opimm32, load_hilo32, make_lhsv_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;
-  erewrite !fsi_sreg_get_correct; eauto;
-  destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1.
-  fold (Val.xor (Vint imm) v); rewrite Val.xor_commut; trivial.
-  all:
-    try apply Int.same_if_eq in EQLO; subst;
-    try rewrite Int.add_commut, Int.add_zero_l;
-    try rewrite ltu_12_wordsize; trivial.
-Qed.
-
-Lemma simplify_xorlimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall
-  (SREG: forall r: positive,
-          hsi_sreg_eval ge sp hst r rs0 m0 =
-          seval_sval ge sp (si_sreg st r) rs0 m0)
-  (H : match lr with
-    | nil => None
-    | a1 :: nil => Some (xorimm64 (fsi_sreg_get hst a1) n)
-    | a1 :: _ :: _ => None
-    end = Some fsv)
-  (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args),
-  seval_sval ge sp (hsval_proj fsv) rs0 m0 =
-  eval_operation ge sp (Oxorlimm n) args m.
-Proof.
-  intros.
-  repeat (destruct lr; simpl; try congruence);
-  simpl in OK1; inv OK1; inv H; simpl;
-  unfold xorimm64, opimm64, load_hilo64, make_lhsv_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;
-  erewrite !fsi_sreg_get_correct; eauto;
-  destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1.
-  fold (Val.xorl (Vlong imm) v); rewrite Val.xorl_commut; trivial.
-  all:
-    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; trivial.
-Qed.
-
-Lemma simplify_intconst_correct ge sp rs0 m0 args m n fsv lr st: forall
-  (H : match lr with
-    | nil => Some (loadimm32 n)
-    | _ :: _ => None
-    end = Some fsv)
-  (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args),
-  seval_sval ge sp (hsval_proj fsv) rs0 m0 =
-  eval_operation ge sp (Ointconst n) args m.
-Proof.
-  intros.
-  repeat (destruct lr; simpl; try congruence);
-  simpl in OK1; inv OK1; inv H; simpl;
-  unfold loadimm32, load_hilo32, make_lhsv_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 ge sp rs0 m0 args m n fsv lr st: forall
-  (H : match lr with
-    | nil => Some (loadimm64 n)
-    | _ :: _ => None
-    end = Some fsv)
-  (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args),
-  seval_sval ge sp (hsval_proj fsv) rs0 m0 =
-  eval_operation ge sp (Olongconst n) args m.
-Proof.
-  intros.
-  repeat (destruct lr; simpl; try congruence);
-  simpl in OK1; inv OK1; inv H; simpl;
-  unfold loadimm64, load_hilo64, make_lhsv_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_cast8signed_correct ge sp rs0 m0 lr hst fsv st args m: forall
-  (SREG: forall r: positive,
-          hsi_sreg_eval ge sp hst r rs0 m0 =
-          seval_sval ge sp (si_sreg st r) rs0 m0)
-  (H : match lr with
-       | nil => None
-       | a1 :: nil =>
-           Some
-             (fSop (Oshrimm (Int.repr 24))
-                (make_lhsv_single
-                   (fSop (Oshlimm (Int.repr 24))
-                      (make_lhsv_single (fsi_sreg_get hst a1)))))
-       | a1 :: _ :: _ => None
-       end = Some fsv)
-  (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args),
-  seval_sval ge sp (hsval_proj fsv) rs0 m0 =
-  eval_operation ge sp Ocast8signed args m.
-Proof.
-  intros.
-  repeat (destruct lr; simpl; try congruence);
-  simpl in OK1; inv OK1; inv H; simpl;
-  erewrite !fsi_sreg_get_correct; eauto;
-  destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1.
-  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 ge sp rs0 m0 lr hst fsv st args m: forall
-  (SREG: forall r: positive,
-          hsi_sreg_eval ge sp hst r rs0 m0 =
-          seval_sval ge sp (si_sreg st r) rs0 m0)
-  (H : match lr with
-       | nil => None
-       | a1 :: nil =>
-           Some
-             (fSop (Oshrimm (Int.repr 16))
-                (make_lhsv_single
-                   (fSop (Oshlimm (Int.repr 16))
-                      (make_lhsv_single (fsi_sreg_get hst a1)))))
-       | a1 :: _ :: _ => None
-       end = Some fsv)
-  (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args),
-  seval_sval ge sp (hsval_proj fsv) rs0 m0 =
-  eval_operation ge sp Ocast16signed args m.
-Proof.
-  intros.
-  repeat (destruct lr; simpl; try congruence);
-  simpl in OK1; inv OK1; inv H; simpl;
-  erewrite !fsi_sreg_get_correct; eauto;
-  destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1.
-  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_shrximm_correct ge sp rs0 m0 lr hst fsv st args m n: forall
-  (SREG: forall r: positive,
-          hsi_sreg_eval ge sp hst r rs0 m0 =
-          seval_sval ge sp (si_sreg st r) rs0 m0)
-  (H : match lr with
-       | nil => None
-       | a1 :: nil =>
-           if Int.eq n Int.zero
-           then
-            Some
-              (fSop (OEmayundef (MUshrx n))
-                 (make_lhsv_cmp false (fsi_sreg_get hst a1)
-                    (fsi_sreg_get hst a1)))
-           else
-            if Int.eq n Int.one
-            then
-             Some
-               (fSop (OEmayundef (MUshrx n))
-                  (make_lhsv_cmp false
-                     (fSop (Oshrimm Int.one)
-                        (make_lhsv_single
-                           (fSop Oadd
-                              (make_lhsv_cmp false (fsi_sreg_get hst a1)
-                                 (fSop (Oshruimm (Int.repr 31))
-                                    (make_lhsv_single (fsi_sreg_get hst a1)))))))
-                     (fSop (Oshrimm Int.one)
-                        (make_lhsv_single
-                           (fSop Oadd
-                              (make_lhsv_cmp false (fsi_sreg_get hst a1)
-                                 (fSop (Oshruimm (Int.repr 31))
-                                    (make_lhsv_single (fsi_sreg_get hst a1)))))))))
-            else
-             Some
-               (fSop (OEmayundef (MUshrx n))
-                  (make_lhsv_cmp false
-                     (fSop (Oshrimm n)
-                        (make_lhsv_single
-                           (fSop Oadd
-                              (make_lhsv_cmp false (fsi_sreg_get hst a1)
-                                 (fSop (Oshruimm (Int.sub Int.iwordsize n))
-                                    (make_lhsv_single
-                                       (fSop (Oshrimm (Int.repr 31))
-                                          (make_lhsv_single
-                                             (fsi_sreg_get hst a1)))))))))
-                     (fSop (Oshrimm n)
-                        (make_lhsv_single
-                           (fSop Oadd
-                              (make_lhsv_cmp false (fsi_sreg_get hst a1)
-                                 (fSop (Oshruimm (Int.sub Int.iwordsize n))
-                                    (make_lhsv_single
-                                       (fSop (Oshrimm (Int.repr 31))
-                                          (make_lhsv_single
-                                             (fsi_sreg_get hst a1)))))))))))
-       | a1 :: _ :: _ => None
-       end = Some fsv)
-  (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args),
-  seval_sval ge sp (hsval_proj fsv) rs0 m0 =
-  eval_operation ge sp (Oshrximm n) args m.
-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 OK1; inv H; simpl;
-    erewrite !fsi_sreg_get_correct; eauto;
-    destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1;
-    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_shrxlimm_correct ge sp rs0 m0 lr hst fsv st args m n: forall
-  (SREG: forall r: positive,
-          hsi_sreg_eval ge sp hst r rs0 m0 =
-          seval_sval ge sp (si_sreg st r) rs0 m0)
-  (H : match lr with
-       | nil => None
-       | a1 :: nil =>
-           if Int.eq n Int.zero
-           then
-            Some
-              (fSop (OEmayundef (MUshrxl n))
-                 (make_lhsv_cmp false (fsi_sreg_get hst a1)
-                    (fsi_sreg_get hst a1)))
-           else
-            if Int.eq n Int.one
-            then
-             Some
-               (fSop (OEmayundef (MUshrxl n))
-                  (make_lhsv_cmp false
-                     (fSop (Oshrlimm Int.one)
-                        (make_lhsv_single
-                           (fSop Oaddl
-                              (make_lhsv_cmp false (fsi_sreg_get hst a1)
-                                 (fSop (Oshrluimm (Int.repr 63))
-                                    (make_lhsv_single (fsi_sreg_get hst a1)))))))
-                     (fSop (Oshrlimm Int.one)
-                        (make_lhsv_single
-                           (fSop Oaddl
-                              (make_lhsv_cmp false (fsi_sreg_get hst a1)
-                                 (fSop (Oshrluimm (Int.repr 63))
-                                    (make_lhsv_single (fsi_sreg_get hst a1)))))))))
-            else
-             Some
-               (fSop (OEmayundef (MUshrxl n))
-                  (make_lhsv_cmp false
-                     (fSop (Oshrlimm n)
-                        (make_lhsv_single
-                           (fSop Oaddl
-                              (make_lhsv_cmp false (fsi_sreg_get hst a1)
-                                 (fSop (Oshrluimm (Int.sub Int64.iwordsize' n))
-                                    (make_lhsv_single
-                                       (fSop (Oshrlimm (Int.repr 63))
-                                          (make_lhsv_single
-                                             (fsi_sreg_get hst a1)))))))))
-                     (fSop (Oshrlimm n)
-                        (make_lhsv_single
-                           (fSop Oaddl
-                              (make_lhsv_cmp false (fsi_sreg_get hst a1)
-                                 (fSop (Oshrluimm (Int.sub Int64.iwordsize' n))
-                                    (make_lhsv_single
-                                       (fSop (Oshrlimm (Int.repr 63))
-                                          (make_lhsv_single
-                                             (fsi_sreg_get hst a1)))))))))))
-       | a1 :: _ :: _ => None
-       end = Some fsv)
-  (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args),
-  seval_sval ge sp (hsval_proj fsv) rs0 m0 =
-  eval_operation ge sp (Oshrxlimm n) args m.
-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 OK1; inv H; simpl;
-    erewrite !fsi_sreg_get_correct; eauto;
-    destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1;
-    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.
-
-Lemma simplify_cast32unsigned_correct ge sp rs0 m0 lr hst fsv st args m: forall
-  (SREG: forall r: positive,
-          hsi_sreg_eval ge sp hst r rs0 m0 =
-          seval_sval ge sp (si_sreg st r) rs0 m0)
-  (H : match lr with
-      | nil => None
-      | a1 :: nil =>
-          Some
-            (fSop (Oshrluimm (Int.repr 32))
-               (make_lhsv_single
-                  (fSop (Oshllimm (Int.repr 32))
-                     (make_lhsv_single
-                        (fSop Ocast32signed
-                           (make_lhsv_single (fsi_sreg_get hst a1)))))))
-      | a1 :: _ :: _ => None
-      end = Some fsv)
-  (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args),
-  seval_sval ge sp (hsval_proj fsv) rs0 m0 =
-  eval_operation ge sp Ocast32unsigned args m.
-Proof.
-  intros.
-  repeat (destruct lr; simpl; try congruence);
-  simpl in OK1; inv OK1; inv H; simpl;
-  erewrite !fsi_sreg_get_correct; eauto;
-  destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1.
-  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.
-
-(** * Main proof of simplification *)
-
-Lemma target_op_simplify_correct op lr hst fsv ge sp rs0 m0 st args m: forall
-   (H: target_op_simplify op lr hst = Some fsv)
-   (REF: hsilocal_refines ge sp rs0 m0 hst st)
-   (OK0: hsok_local ge sp rs0 m0 hst)
-   (OK1: seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args)
-   (OK2: seval_smem ge sp (si_smem st) rs0 m0 = Some m),
-   seval_sval ge sp (hsval_proj fsv) rs0 m0 = eval_operation ge sp op args m.
-Proof.
-  unfold target_op_simplify; simpl.
-  intros H (LREF & SREF & SREG & SMEM) ? ? ?.
-  destruct op; try congruence.
-  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 (seval_sval ge sp (si_sreg st r) rs0 m0) eqn:OKv1; try congruence);
-  try (destruct (seval_sval ge sp (si_sreg st r0) rs0 m0) eqn:OKv2; try congruence);
-  inv H; inv OK1.
-  - 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 hst c l ge sp rs0 m0 st c' l': forall
-  (TARGET: target_cbranch_expanse hst c l = Some (c', l'))
-  (LREF : hsilocal_refines ge sp rs0 m0 hst st)
-  (OK: hsok_local ge sp rs0 m0 hst),
-  seval_condition ge sp c' (hsval_list_proj l') (si_smem st) rs0 m0 =
-  seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0.
-Proof.
-  unfold target_cbranch_expanse, seval_condition; simpl.
-  intros H (LREF & SREF & SREG & SMEM) ?.
-  destruct c; try congruence;
-  repeat (destruct l; simpl in H; try congruence).
-  1,2,5,6:
-    destruct c; inv H; simpl;
-    try erewrite !fsi_sreg_get_correct; eauto;
-    try (destruct (seval_smem ge sp (si_smem st) rs0 m0) eqn:OKmem; try congruence);
-    try (destruct (seval_sval ge sp (si_sreg st r) rs0 m0) eqn:OKv1; try congruence);
-    try (destruct (seval_sval ge sp (si_sreg st r0) rs0 m0) eqn:OKv2; try congruence);
-    try replace (Cle) with (swap_comparison Cge) by auto;
-    try replace (Clt) with (swap_comparison Cgt) by auto;
-    try rewrite Val.swap_cmp_bool; trivial;
-    try rewrite Val.swap_cmpu_bool; trivial;
-    try rewrite Val.swap_cmpl_bool; trivial;
-    try rewrite Val.swap_cmplu_bool; trivial.
-  1,2,3,4:
-    try destruct (Int.eq n Int.zero) eqn: EQIMM;
-    try apply Int.same_if_eq in EQIMM;
-    try destruct (Int64.eq n Int64.zero) eqn: EQIMM;
-    try apply Int64.same_if_eq in EQIMM;
-    destruct c; inv H; simpl;
-    try erewrite !fsi_sreg_get_correct; eauto;
-    try (destruct (seval_smem ge sp (si_smem st) rs0 m0) eqn:OKmem; try congruence);
-    try (destruct (seval_sval ge sp (si_sreg st r) rs0 m0) eqn:OKv1; try congruence);
-    try (destruct (seval_sval ge sp (si_sreg st r0) rs0 m0) eqn:OKv2; try congruence);
-    unfold loadimm32, load_hilo32, Val.cmp, Val.cmpu, zero32;
-    unfold loadimm64, load_hilo64, Val.cmpl, Val.cmplu, zero64;
-    intros; try (specialize make_immed32_sound with (n);
-    destruct (make_immed32 n) eqn:EQMKI); intros; simpl;
-    intros; try (specialize make_immed64_sound with (n);
-    destruct (make_immed64 n) eqn:EQMKI); intros; simpl;
-    try rewrite EQLO; simpl;
-    try destruct (Int.eq lo Int.zero) eqn:EQLO;
-    try destruct (Int64.eq lo Int64.zero) eqn:EQLO;
-    try apply Int.same_if_eq in EQLO; simpl; trivial;
-    try apply Int64.same_if_eq in EQLO; simpl; trivial;
-    unfold 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;
-    try erewrite !fsi_sreg_get_correct; eauto;
-    try (destruct (seval_smem ge sp (si_smem st) rs0 m0) eqn:OKmem; try congruence);
-    try (destruct (seval_sval ge sp (si_sreg st r) rs0 m0) eqn:OKv1; try congruence);
-    try (destruct (seval_sval ge sp (si_sreg st r0) rs0 m0) eqn:OKv2; try congruence);
-    unfold zero32, zero64, Val.cmpf, Val.cmpfs;
-    destruct v, v0; simpl; trivial;
-    try rewrite Float.cmp_ne_eq;
-    try rewrite Float32.cmp_ne_eq;
-    try rewrite <- Float.cmp_swap; simpl;
-    try rewrite <- Float32.cmp_swap; simpl;
-    try destruct (Float.cmp _ _); simpl;
-    try destruct (Float32.cmp _ _); simpl;
-    try rewrite Int.eq_true; simpl;
-    try rewrite Int.eq_false; try apply Int.one_not_zero;
-    simpl; trivial.
-Qed.
-Global Opaque target_op_simplify.
-Global Opaque target_cbranch_expanse.