Proof of fsval condition cmp ok

9 files changed, 545 insertions, 1138 deletions

diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index d0c826a3..4876f7ec 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -812,10 +812,10 @@ Definition transl_op
       do rd <- ireg_of res;
       do rs <- ireg_of a1;
       OK (Pxoriw rd rs n :: k)
-  | OEluiw n, nil =>
+  | OEluiw n _, a1 :: nil =>
       do rd <- ireg_of res;
       OK (Pluiw rd n :: k)
-  | OEaddiwr0 n, nil =>
+  | OEaddiwr0 n _, a1 :: nil =>
       do rd <- ireg_of res;
       OK (Paddiw rd X0 n :: k)
   | OEseql optR0, a1 :: a2 :: nil =>
@@ -860,10 +860,10 @@ Definition transl_op
       do rd <- ireg_of res;
       do rs <- ireg_of a1;
       OK (Pxoril rd rs n :: k)
-  | OEluil n, nil =>
+  | OEluil n, a1 :: nil =>
       do rd <- ireg_of res;
       OK (Pluil rd n :: k)
-  | OEaddilr0 n, nil =>
+  | OEaddilr0 n, a1 :: nil =>
       do rd <- ireg_of res;
       OK (Paddil rd X0 n :: k)
   | OEloadli n, nil =>
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index 35c5b9d6..a826455e 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -1258,10 +1258,11 @@ Opaque Int.eq.
   { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
      exists rs'; split. eexact A. eauto with asmgen. }
   (* Expanded instructions from RTL *)
-  7: econstructor; split; try apply exec_straight_one; simpl; eauto;
-  split; intros; Simpl; rewrite Int.add_commut; auto.
-  13: econstructor; split; try apply exec_straight_one; simpl; eauto;
-  split; intros; Simpl; rewrite Int64.add_commut; auto.
+  7,8,15,16:
+    econstructor; split; try apply exec_straight_one; simpl; eauto;
+    split; intros; Simpl; unfold may_undef_int; try destruct is_long; simpl;
+    try rewrite Int.add_commut; try rewrite Int64.add_commut;
+    destruct (rs (preg_of m0)); try discriminate; eauto.
   all: destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0;
   econstructor; split; try apply exec_straight_one; simpl; eauto;
   split; intros; Simpl.
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index 11a66322..103285b4 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -35,29 +35,29 @@ let n2pi () =
 
 type immt = Xoriw | Xoril | Sltiw | Sltiuw | Sltil | Sltiul
 
-let load_hilo32 dest hi lo succ k =
-  if Int.eq lo Int.zero then Iop (OEluiw hi, [], dest, succ) :: k
+let load_hilo32 a1 dest hi lo succ is_long k =
+  if Int.eq lo Int.zero then Iop (OEluiw (hi, is_long), [a1], dest, succ) :: k
   else
-    Iop (OEluiw hi, [], dest, n2pi ())
+    Iop (OEluiw (hi, is_long), [a1], dest, n2pi ())
     :: Iop (Oaddimm lo, [ dest ], dest, succ)
     :: k
 
-let load_hilo64 dest hi lo succ k =
-  if Int64.eq lo Int64.zero then Iop (OEluil hi, [], dest, succ) :: k
+let load_hilo64 a1 dest hi lo succ k =
+  if Int64.eq lo Int64.zero then Iop (OEluil hi, [a1], dest, succ) :: k
   else
-    Iop (OEluil hi, [], dest, n2pi ())
+    Iop (OEluil hi, [a1], dest, n2pi ())
     :: Iop (Oaddlimm lo, [ dest ], dest, succ)
     :: k
 
-let loadimm32 dest n succ k =
+let loadimm32 a1 dest n succ is_long k =
   match make_immed32 n with
-  | Imm32_single imm -> Iop (OEaddiwr0 imm, [], dest, succ) :: k
-  | Imm32_pair (hi, lo) -> load_hilo32 dest hi lo succ k
+  | Imm32_single imm -> Iop (OEaddiwr0 (imm, is_long), [a1], dest, succ) :: k
+  | Imm32_pair (hi, lo) -> load_hilo32 a1 dest hi lo succ is_long k
 
-let loadimm64 dest n succ k =
+let loadimm64 a1 dest n succ k =
   match make_immed64 n with
-  | Imm64_single imm -> Iop (OEaddilr0 imm, [], dest, succ) :: k
-  | Imm64_pair (hi, lo) -> load_hilo64 dest hi lo succ k
+  | Imm64_single imm -> Iop (OEaddilr0 imm, [a1], dest, succ) :: k
+  | Imm64_pair (hi, lo) -> load_hilo64 a1 dest hi lo succ k
   | Imm64_large imm -> Iop (OEloadli imm, [], dest, succ) :: k
 
 let get_opimm imm = function
@@ -68,12 +68,12 @@ let get_opimm imm = function
   | Sltil -> OEsltil imm
   | Sltiul -> OEsltiul imm
 
-let opimm32 a1 dest n succ k op opimm =
+let opimm32 a1 dest n succ is_long k op opimm =
   match make_immed32 n with
   | Imm32_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k
   | Imm32_pair (hi, lo) ->
       reg := !reg + 1;
-      load_hilo32 (r2p ()) hi lo (n2pi ())
+      load_hilo32 a1 (r2p ()) hi lo (n2pi ()) is_long
         (Iop (op, [ a1; r2p () ], dest, succ) :: k)
 
 let opimm64 a1 dest n succ k op opimm =
@@ -81,7 +81,7 @@ let opimm64 a1 dest n succ k op opimm =
   | Imm64_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k
   | Imm64_pair (hi, lo) ->
       reg := !reg + 1;
-      load_hilo64 (r2p ()) hi lo (n2pi ())
+      load_hilo64 a1 (r2p ()) hi lo (n2pi ())
         (Iop (op, [ a1; r2p () ], dest, succ) :: k)
   | Imm64_large imm ->
       reg := !reg + 1;
@@ -89,11 +89,11 @@ let opimm64 a1 dest n succ k op opimm =
       :: Iop (op, [ a1; r2p () ], dest, succ)
       :: k
 
-let xorimm32 a1 dest n succ k = opimm32 a1 dest n succ k Oxor Xoriw
+let xorimm32 a1 dest n succ is_long k = opimm32 a1 dest n succ is_long k Oxor Xoriw
 
-let sltimm32 a1 dest n succ k = opimm32 a1 dest n succ k (OEsltw None) Sltiw
+let sltimm32 a1 dest n succ is_long k = opimm32 a1 dest n succ is_long k (OEsltw None) Sltiw
 
-let sltuimm32 a1 dest n succ k = opimm32 a1 dest n succ k (OEsltuw None) Sltiuw
+let sltuimm32 a1 dest n succ is_long k = opimm32 a1 dest n succ is_long k (OEsltuw None) Sltiuw
 
 let xorimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oxorl Xoril
 
@@ -233,28 +233,28 @@ let expanse_cbranchimm_int32s cmp a1 n info succ1 succ2 k =
   if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 info succ1 succ2 k
   else (
     reg := !reg + 1;
-    loadimm32 (r2p ()) n (n2pi ())
+    loadimm32 a1 (r2p ()) n (n2pi ()) false
       (cbranch_int32s false cmp a1 (r2p ()) info succ1 succ2 k))
 
 let expanse_cbranchimm_int32u cmp a1 n info succ1 succ2 k =
   if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 info succ1 succ2 k
   else (
     reg := !reg + 1;
-    loadimm32 (r2p ()) n (n2pi ())
+    loadimm32 a1 (r2p ()) n (n2pi ()) false
       (cbranch_int32u false cmp a1 (r2p ()) info succ1 succ2 k))
 
 let expanse_cbranchimm_int64s cmp a1 n info succ1 succ2 k =
   if Int64.eq n Int64.zero then cbranch_int64s true cmp a1 a1 info succ1 succ2 k
   else (
     reg := !reg + 1;
-    loadimm64 (r2p ()) n (n2pi ())
+    loadimm64 a1 (r2p ()) n (n2pi ())
       (cbranch_int64s false cmp a1 (r2p ()) info succ1 succ2 k))
 
 let expanse_cbranchimm_int64u cmp a1 n info succ1 succ2 k =
   if Int64.eq n Int64.zero then cbranch_int64u true cmp a1 a1 info succ1 succ2 k
   else (
     reg := !reg + 1;
-    loadimm64 (r2p ()) n (n2pi ())
+    loadimm64 a1 (r2p ()) n (n2pi ())
       (cbranch_int64u false cmp a1 (r2p ()) info succ1 succ2 k))
 
 let expanse_condimm_int32s cmp a1 n dest succ k =
@@ -262,25 +262,25 @@ let expanse_condimm_int32s cmp a1 n dest succ k =
   else
     match cmp with
     | Ceq | Cne ->
-        xorimm32 a1 dest n (n2pi ())
+        xorimm32 a1 dest n (n2pi ()) false
           (cond_int32s true cmp dest dest dest succ k)
-    | Clt -> sltimm32 a1 dest n succ k
+    | Clt -> sltimm32 a1 dest n succ false k
     | Cle ->
-        if Int.eq n (Int.repr Int.max_signed) then loadimm32 dest Int.one succ k
-        else sltimm32 a1 dest (Int.add n Int.one) succ k
+        if Int.eq n (Int.repr Int.max_signed) then loadimm32 a1 dest Int.one succ false k
+        else sltimm32 a1 dest (Int.add n Int.one) succ false k
     | _ ->
         reg := !reg + 1;
-        loadimm32 (r2p ()) n (n2pi ())
+        loadimm32 a1 (r2p ()) n (n2pi ()) false
           (cond_int32s false cmp a1 (r2p ()) dest succ k)
 
 let expanse_condimm_int32u cmp a1 n dest succ k =
   if Int.eq n Int.zero then cond_int32u true cmp a1 a1 dest succ k
   else
     match cmp with
-    | Clt -> sltuimm32 a1 dest n succ k
+    | Clt -> sltuimm32 a1 dest n succ false k
     | _ ->
         reg := !reg + 1;
-        loadimm32 (r2p ()) n (n2pi ())
+        loadimm32 a1 (r2p ()) n (n2pi ()) false
           (cond_int32u false cmp a1 (r2p ()) dest succ k)
 
 let expanse_condimm_int64s cmp a1 n dest succ k =
@@ -294,11 +294,11 @@ let expanse_condimm_int64s cmp a1 n dest succ k =
     | Clt -> sltimm64 a1 dest n succ k
     | Cle ->
         if Int64.eq n (Int64.repr Int64.max_signed) then
-          loadimm32 dest Int.one succ k
+          loadimm32 a1 dest Int.one succ true k
         else sltimm64 a1 dest (Int64.add n Int64.one) succ k
     | _ ->
         reg := !reg + 1;
-        loadimm64 (r2p ()) n (n2pi ())
+        loadimm64 a1 (r2p ()) n (n2pi ())
           (cond_int64s false cmp a1 (r2p ()) dest succ k)
 
 let expanse_condimm_int64u cmp a1 n dest succ k =
@@ -308,7 +308,7 @@ let expanse_condimm_int64u cmp a1 n dest succ k =
     | Clt -> sltuimm64 a1 dest n succ k
     | _ ->
         reg := !reg + 1;
-        loadimm64 (r2p ()) n (n2pi ())
+        loadimm64 a1 (r2p ()) n (n2pi ())
           (cond_int64u false cmp a1 (r2p ()) dest succ k)
 
 let expanse_cond_fp cnot fn_cond cmp f1 f2 dest succ k =
@@ -370,7 +370,7 @@ let rec write_tree exp current code' new_order =
   | _ -> failwith "ExpansionOracle.write_tree: inconsistent instruction."
 
 let expanse (sb : superblock) code pm =
-  debug_flag := true;
+  (*debug_flag := true;*)
   let new_order = ref [] in
   let liveins = ref sb.liveins in
   let exp = ref [] in
@@ -510,7 +510,8 @@ let expanse (sb : superblock) code pm =
     sb.instructions;
   sb.instructions <- Array.of_list (List.rev !new_order);
   sb.liveins <- !liveins;
-  debug_flag := false;
+  print_ptree_regset !liveins;
+  (*debug_flag := false;*)
   (!code', !pm')
 
 let rec find_last_node_reg = function
diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v
index a0ec7732..d90c1b66 100644
--- a/riscV/NeedOp.v
+++ b/riscV/NeedOp.v
@@ -93,23 +93,23 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | OEsneuw _ => op2 (default nv)
   | OEsltw _ => op2 (default nv)
   | OEsltuw _ => op2 (default nv)
-  | OEsltiw n => op1 (default nv)
-  | OEsltiuw n => op1 (default nv)
-  | OExoriw n => op1 (bitwise nv)
-  | OEluiw n => op1 (default nv)
-  | OEaddiwr0 n => op1 (modarith nv)
+  | OEsltiw _ => op1 (default nv)
+  | OEsltiuw _ => op1 (default nv)
+  | OExoriw _ => op1 (bitwise nv)
+  | OEluiw _ _ => op1 (default nv)
+  | OEaddiwr0 _ _ => op1 (default nv) (* TODO gourdinl modarith impossible? *)
   | OEseql _ => op2 (default nv)
   | OEsnel _ => op2 (default nv)
   | OEsequl _ => op2 (default nv)
   | OEsneul _ => op2 (default nv)
   | OEsltl _ => op2 (default nv)
   | OEsltul _ => op2 (default nv)
-  | OEsltil n => op1 (default nv)
-  | OEsltiul n => op1 (default nv)
-  | OExoril n => op1 (default nv)
-  | OEluil n => op1 (default nv)
-  | OEaddilr0 n => op1 (modarith nv)
-  | OEloadli n => op1 (default nv)
+  | OEsltil _ => op1 (default nv)
+  | OEsltiul _ => op1 (default nv)
+  | OExoril _ => op1 (default nv)
+  | OEluil _ => op1 (default nv)
+  | OEaddilr0 _ => op1 (default nv) (* TODO gourdinl modarith impossible? *)
+  | OEloadli _ => op1 (default nv)
   | OEfeqd => op2 (default nv)
   | OEfltd => op2 (default nv)
   | OEfled => op2 (default nv)
@@ -184,8 +184,6 @@ Proof.
 - apply shrimm_sound; auto.
 - apply shruimm_sound; auto.
 - apply xor_sound; auto with na.
-- auto with na.
-- auto with na.
 Qed.
 
 Lemma operation_is_redundant_sound:
diff --git a/riscV/Op.v b/riscV/Op.v
index 28760a72..cd74080f 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -173,19 +173,19 @@ Inductive operation : Type :=
   (* Expansed conditions *)
   | OEseqw (optR0: option bool)                  (**r [rd <- rs1 == rs2] signed *)
   | OEsnew (optR0: option bool)                  (**r [rd <- rs1 != rs2] signed *)
-  | OEsequw (optR0: option bool)                  (**r [rd <- rs1 == rs2] unsigned *)
-  | OEsneuw (optR0: option bool)                  (**r [rd <- rs1 != rs2] unsigned *)
+  | OEsequw (optR0: option bool)                 (**r [rd <- rs1 == rs2] unsigned *)
+  | OEsneuw (optR0: option bool)                 (**r [rd <- rs1 != rs2] unsigned *)
   | OEsltw (optR0: option bool)                  (**r set-less-than *)
   | OEsltuw (optR0: option bool)                 (**r set-less-than unsigned *)
   | OEsltiw (n: int)                             (**r set-less-than immediate *)
   | OEsltiuw (n: int)                            (**r set-less-than unsigned immediate *)
   | OExoriw (n: int)                             (**r xor immediate *)
-  | OEluiw (n: int)                              (**r load upper-immediate *)
-  | OEaddiwr0 (n: int)                           (**r add immediate *)
+  | OEluiw (n: int) (is_long: bool)              (**r load upper-immediate *)
+  | OEaddiwr0 (n: int) (is_long: bool)           (**r add immediate *)
   | OEseql (optR0: option bool)                  (**r [rd <- rs1 == rs2] signed *)
   | OEsnel (optR0: option bool)                  (**r [rd <- rs1 != rs2] signed *)
-  | OEsequl (optR0: option bool)                  (**r [rd <- rs1 == rs2] unsigned *)
-  | OEsneul (optR0: option bool)                  (**r [rd <- rs1 != rs2] unsigned *)
+  | OEsequl (optR0: option bool)                 (**r [rd <- rs1 == rs2] unsigned *)
+  | OEsneul (optR0: option bool)                 (**r [rd <- rs1 != rs2] unsigned *)
   | OEsltl (optR0: option bool)                  (**r set-less-than *)
   | OEsltul (optR0: option bool)                 (**r set-less-than unsigned *)
   | OEsltil (n: int64)                           (**r set-less-than immediate *)
@@ -263,6 +263,24 @@ Definition apply_bin_r0 {B} (optR0: option bool) (sem: val -> val -> B) (v1 v2 v
   | Some false => sem v1 vz
   end.
 
+Definition may_undef_int (is_long: bool) (sem: val -> val -> val) (v1 vimm vz: val): val :=
+  if negb is_long then
+    match v1 with
+    | Vint _ => sem vimm vz
+    | _ => Vundef
+    end
+  else
+    match v1 with
+    | Vlong _ => sem vimm vz
+    | _ => Vundef
+    end.
+
+Definition may_undef_luil (v1: val) (n: int64): val :=
+  match v1 with
+  | Vlong _ => Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12)))
+  | _ => Vundef
+  end.
+
 Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool :=
   match cond, vl with
   | Ccomp c, v1 :: v2 :: nil => Val.cmp_bool c v1 v2
@@ -404,8 +422,8 @@ Definition eval_operation
   | OEsltiw n, v1::nil => Some (Val.cmp Clt v1 (Vint n))
   | OEsltiuw n, v1::nil => Some (Val.cmpu (Mem.valid_pointer m) Clt v1 (Vint n))
   | OExoriw n, v1::nil => Some (Val.xor v1 (Vint n))
-  | OEluiw n, nil => Some(Vint (Int.shl n (Int.repr 12)))
-  | OEaddiwr0 n, nil => Some (Val.add (Vint n) zero32)
+  | OEluiw n is_long, v1::nil => Some (may_undef_int is_long Val.shl v1 (Vint n) (Vint (Int.repr 12)))
+  | OEaddiwr0 n is_long, v1::nil => Some (may_undef_int is_long Val.add v1 (Vint n) zero32)
   | OEseql optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Ceq) v1 v2 zero64))
   | OEsnel optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Cne) v1 v2 zero64))
   | OEsequl optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64))
@@ -415,8 +433,8 @@ Definition eval_operation
   | OEsltil n, v1::nil => Some (Val.maketotal (Val.cmpl Clt v1 (Vlong n)))
   | OEsltiul n, v1::nil => Some (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt v1 (Vlong n)))
   | OExoril n, v1::nil => Some (Val.xorl v1 (Vlong n))
-  | OEluil n, nil => Some(Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12))))
-  | OEaddilr0 n, nil => Some (Val.addl (Vlong n) zero64)
+  | OEluil n, v1::nil => Some (may_undef_luil v1 n)
+  | OEaddilr0 n, v1::nil => Some (may_undef_int true Val.addl v1 (Vlong n) zero64)
   | OEloadli n, nil => Some (Vlong n)
   | OEfeqd, v1::v2::nil => Some (Val.cmpf Ceq v1 v2)
   | OEfltd, v1::v2::nil => Some (Val.cmpf Clt v1 v2)
@@ -605,8 +623,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | OEsltiw _ => (Tint :: nil, Tint)
   | OEsltiuw _ => (Tint :: nil, Tint)
   | OExoriw _ => (Tint :: nil, Tint)
-  | OEluiw _ => (nil, Tint)
-  | OEaddiwr0 _ => (nil, Tint)
+  | OEluiw _ _ => (Tint :: nil, Tint)
+  | OEaddiwr0 _ _ => (Tint :: nil, Tint)
   | OEseql _ => (Tlong :: Tlong :: nil, Tint)
   | OEsnel _ => (Tlong :: Tlong :: nil, Tint)
   | OEsequl _ => (Tlong :: Tlong :: nil, Tint)
@@ -616,8 +634,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | OEsltil _ => (Tlong :: nil, Tint)
   | OEsltiul _ => (Tlong :: nil, Tint)
   | OExoril _ => (Tlong :: nil, Tlong)
-  | OEluil _ => (nil, Tlong)
-  | OEaddilr0 _ => (nil, Tlong)
+  | OEluil _ => (Tlong :: nil, Tlong)
+  | OEaddilr0 _ => (Tlong :: nil, Tlong)
   | OEloadli _ => (nil, Tlong)
   | OEfeqd => (Tfloat :: Tfloat :: nil, Tint)
   | OEfltd => (Tfloat :: Tfloat :: nil, Tint)
@@ -857,9 +875,11 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* OExoriw *)
   - destruct v0...
   (* OEluiw *)
-  - trivial.
+  - unfold may_undef_int;
+    destruct v0, is_long; simpl; trivial;
+    destruct (Int.ltu _ _); cbn; trivial.
   (* OEaddiwr0 *)
-  - trivial.
+  - destruct v0, is_long; simpl; trivial.
   (* OEseql *)
   - destruct optR0 as [[]|]; simpl; unfold Val.cmpl;
     destruct Val.cmpl_bool... all: destruct b...
@@ -886,9 +906,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* OExoril *)
   - destruct v0...
   (* OEluil *)
-  - trivial.
+  - destruct v0; simpl; trivial.
   (* OEaddilr0 *)
-  - trivial.
+  - destruct v0; simpl; trivial.
   (* OEloadli *)
   - trivial.
   (* OEfeqd *)
@@ -1691,6 +1711,15 @@ Proof.
   - apply eval_cmpu_bool_inj; auto.
   (* OExoriw *)
   - inv H4; simpl; auto.
+  (* OEluiw *)
+  - unfold may_undef_int;
+    destruct is_long;
+    inv H4; simpl; auto;
+    destruct (Int.ltu _ _); auto.
+  (* OEaddiwr0 *)
+  - unfold may_undef_int;
+    destruct is_long;
+    inv H4; simpl; auto.
   (* OEseql *)
   - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl;
     inv H4; inv H2; simpl; try destruct (Int64.eq _ _); simpl; cbn; auto;
@@ -1715,6 +1744,11 @@ Proof.
   - apply eval_cmplu_bool_inj; auto.
   (* OExoril *)
   - inv H4; simpl; auto.
+  (* OEluil *)
+  - inv H4; simpl; auto.
+  (* OEaddilr0 *)
+  - unfold may_undef_int;
+    inv H4; simpl; auto.
   (* OEfeqd *)
   - inv H4; inv H2; cbn; simpl; auto.
     destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto.
diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml
index 2b5ae1f5..2738e16d 100644
--- a/riscV/PrintOp.ml
+++ b/riscV/PrintOp.ml
@@ -192,8 +192,8 @@ let print_operation reg pp = function
   | OEsltiw n, [r1] -> fprintf pp "OEsltiw(%a,%ld)" reg r1 (camlint_of_coqint n)
   | OEsltiuw n, [r1] -> fprintf pp "OEsltiuw(%a,%ld)" reg r1 (camlint_of_coqint n)
   | OExoriw n, [r1] -> fprintf pp "OExoriw(%a,%ld)" reg r1 (camlint_of_coqint n)
-  | OEluiw n, [] -> fprintf pp "OEluiw(%ld)" (camlint_of_coqint n)
-  | OEaddiwr0 n, [] -> fprintf pp "OEaddiwr0(%ld,X0)" (camlint_of_coqint n)
+  | OEluiw (n, _), [] -> fprintf pp "OEluiw(%ld)" (camlint_of_coqint n)
+  | OEaddiwr0 (n, _), [] -> fprintf pp "OEaddiwr0(%ld,X0)" (camlint_of_coqint n)
   | OEseql optR0, [r1;r2] -> fprintf pp "OEseql"; (get_optR0_s Ceq reg pp r1 r2 optR0)
   | OEsnel optR0, [r1;r2] -> fprintf pp "OEsnel"; (get_optR0_s Cne reg pp r1 r2 optR0)
   | OEsltl optR0, [r1;r2] -> fprintf pp "OEsltl"; (get_optR0_s Clt reg pp r1 r2 optR0)
diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v
index 311f2828..f17dfe7d 100644
--- a/riscV/RTLpathSE_simplify.v
+++ b/riscV/RTLpathSE_simplify.v
@@ -4,6 +4,7 @@ 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 *)
 
@@ -30,44 +31,48 @@ Definition make_lhsv_single (hvs: hsval) : list_hsval :=
 
 (* Immediate loads *)
 
-Definition load_hilo32 (hi lo: int) :=
+Definition load_hilo32 (hv1: hsval) (hi lo: int) (is_long: bool) :=
+  let hl := make_lhsv_single hv1 in
   if Int.eq lo Int.zero then
-    fSop (OEluiw hi) fSnil
+    fSop (OEluiw hi is_long) hl
   else
-    let hvs := fSop (OEluiw hi) fSnil in
-    let hl := make_lhsv_single hvs in
-    fSop (Oaddimm lo) hl.
+    let hvs := fSop (OEluiw hi is_long) hl in
+    let hl' := make_lhsv_single hvs in
+    fSop (Oaddimm lo) hl'.
 
-Definition load_hilo64 (hi lo: int64) :=
+Definition load_hilo64 (hv1: hsval) (hi lo: int64) :=
+  let hl := make_lhsv_single hv1 in
   if Int64.eq lo Int64.zero then
-    fSop (OEluil hi) fSnil
+    fSop (OEluil hi) hl
   else
-    let hvs := fSop (OEluil hi) fSnil in
+    let hvs := fSop (OEluil hi) hl in
     let hl := make_lhsv_single hvs in
     fSop (Oaddlimm lo) hl.
 
-Definition loadimm32 (n: int) :=
+Definition loadimm32 (hv1: hsval) (n: int) (is_long: bool) :=
   match make_immed32 n with
   | Imm32_single imm =>
-      fSop (OEaddiwr0 imm) fSnil
-  | Imm32_pair hi lo => load_hilo32 hi lo
+      let hl := make_lhsv_single hv1 in
+      fSop (OEaddiwr0 imm is_long) hl
+  | Imm32_pair hi lo => load_hilo32 hv1 hi lo is_long
   end.
 
-Definition loadimm64 (n: int64) :=
+Definition loadimm64 (hv1: hsval) (n: int64) :=
   match make_immed64 n with
   | Imm64_single imm =>
-      fSop (OEaddilr0 imm) fSnil
-  | Imm64_pair hi lo => load_hilo64 hi lo
+      let hl := make_lhsv_single hv1 in
+      fSop (OEaddilr0 imm) hl
+  | Imm64_pair hi lo => load_hilo64 hv1 hi lo
   | Imm64_large imm => fSop (OEloadli imm) fSnil
   end.
 
-Definition opimm32 (hv1: hsval) (n: int) (op: operation) (opimm: int -> operation) :=
+Definition opimm32 (hv1: hsval) (n: int) (op: operation) (opimm: int -> operation) (is_long: bool) :=
   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 hvs := load_hilo32 hv1 hi lo is_long in
       let hl := make_lhsv_cmp false hv1 hvs in
       fSop op hl
   end.
@@ -78,7 +83,7 @@ Definition opimm64 (hv1: hsval) (n: int64) (op: operation) (opimm: int64 -> oper
       let hl := make_lhsv_single hv1 in
       fSop (opimm imm) hl
   | Imm64_pair hi lo =>
-      let hvs := load_hilo64 hi lo in
+      let hvs := load_hilo64 hv1 hi lo in
       let hl := make_lhsv_cmp false hv1 hvs in
       fSop op hl
   | Imm64_large imm =>
@@ -87,9 +92,9 @@ Definition opimm64 (hv1: hsval) (n: int64) (op: operation) (opimm: int64 -> oper
       fSop op hl
   end.
 
-Definition xorimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oxor OExoriw.
-Definition sltimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltw None) OEsltiw.
-Definition sltuimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltuw None) OEsltiuw.
+Definition xorimm32 (hv1: hsval) (n: int) (is_long: bool) := opimm32 hv1 n Oxor OExoriw is_long.
+Definition sltimm32 (hv1: hsval) (n: int) (is_long: bool) := opimm32 hv1 n (OEsltw None) OEsltiw is_long.
+Definition sltuimm32 (hv1: hsval) (n: int) (is_long: bool) := opimm32 hv1 n (OEsltuw None) OEsltiuw is_long.
 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.
@@ -150,17 +155,17 @@ Definition expanse_condimm_int32s (cmp: comparison) (hv1: hsval) (n: int) :=
     match cmp with
     | Ceq | Cne =>
         let optR0 := make_optR0 true is_inv in
-        let hvs := xorimm32 hv1 n in
+        let hvs := xorimm32 hv1 n false in
         let hl := make_lhsv_cmp false hvs hvs in
         cond_int32s cmp hl optR0
-    | Clt => sltimm32 hv1 n
+    | Clt => sltimm32 hv1 n false
     | Cle =>
         if Int.eq n (Int.repr Int.max_signed) then
-          loadimm32 Int.one
-        else sltimm32 hv1 (Int.add n Int.one)
+          loadimm32 hv1 Int.one false
+        else sltimm32 hv1 (Int.add n Int.one) false
     | _ =>
         let optR0 := make_optR0 false is_inv in
-        let hvs := loadimm32 n in
+        let hvs := loadimm32 hv1 n false in
         let hl := make_lhsv_cmp is_inv hv1 hvs in
         cond_int32s cmp hl optR0
     end.
@@ -173,10 +178,10 @@ Definition expanse_condimm_int32u (cmp: comparison) (hv1: hsval) (n: int) :=
     cond_int32u cmp hl optR0
   else
     match cmp with
-    | Clt => sltuimm32 hv1 n
+    | Clt => sltuimm32 hv1 n false
     | _ =>
         let optR0 := make_optR0 false is_inv in
-        let hvs := loadimm32 n in
+        let hvs := loadimm32 hv1 n false in
         let hl := make_lhsv_cmp is_inv hv1 hvs in
         cond_int32u cmp hl optR0
     end.
@@ -197,11 +202,11 @@ Definition expanse_condimm_int64s (cmp: comparison) (hv1: hsval) (n: int64) :=
     | Clt => sltimm64 hv1 n
     | Cle =>
         if Int64.eq n (Int64.repr Int64.max_signed) then
-          loadimm32 Int.one
+          loadimm32 hv1 Int.one true
         else sltimm64 hv1 (Int64.add n Int64.one)
     | _ =>
         let optR0 := make_optR0 false is_inv in
-        let hvs := loadimm64 n in
+        let hvs := loadimm64 hv1 n in
         let hl := make_lhsv_cmp is_inv hv1 hvs in
         cond_int64s cmp hl optR0
     end.
@@ -217,7 +222,7 @@ Definition expanse_condimm_int64u (cmp: comparison) (hv1: hsval) (n: int64) :=
     | Clt => sltuimm64 hv1 n
     | _ =>
         let optR0 := make_optR0 false is_inv in
-        let hvs := loadimm64 n in
+        let hvs := loadimm64 hv1 n in
         let hl := make_lhsv_cmp is_inv hv1 hvs in
         cond_int64u cmp hl optR0
     end.
@@ -246,6 +251,48 @@ Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) :=
   let hl := make_lhsv_single hvs in
   if normal' then hvs else fSop (OExoriw Int.one) hl.
 
+(* Branches instructions *)
+
+Definition transl_cbranch_int32s (cmp: comparison) (optR0: option bool) :=
+  match cmp with
+  | Ceq => CEbeqw optR0
+  | Cne => CEbnew optR0
+  | Clt => CEbltw optR0
+  | Cle => CEbgew optR0
+  | Cgt => CEbltw optR0
+  | Cge => CEbgew optR0
+  end.
+
+Definition transl_cbranch_int32u (cmp: comparison) (optR0: option bool) :=
+  match cmp with
+  | Ceq => CEbequw optR0
+  | Cne => CEbneuw optR0
+  | Clt => CEbltuw optR0
+  | Cle => CEbgeuw optR0
+  | Cgt => CEbltuw optR0
+  | Cge => CEbgeuw optR0
+  end.
+
+Definition transl_cbranch_int64s (cmp: comparison) (optR0: option bool) :=
+  match cmp with
+  | Ceq => CEbeql optR0
+  | Cne => CEbnel optR0
+  | Clt => CEbltl optR0
+  | Cle => CEbgel optR0
+  | Cgt => CEbltl optR0
+  | Cge => CEbgel optR0
+  end.
+
+Definition transl_cbranch_int64u (cmp: comparison) (optR0: option bool) :=
+  match cmp with
+  | Ceq => CEbequl optR0
+  | Cne => CEbneul optR0
+  | Clt => CEbltul optR0
+  | Cle => CEbgeul optR0
+  | Cgt => CEbltul optR0
+  | Cge => CEbgeul optR0
+  end.
+
 (** Target op simplifications using "fake" values *)
 
 Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval :=
@@ -317,6 +364,111 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca
   | _, _ => None
   end.
 
+Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg) : option (condition * list_hsval) :=
+  match cond, args with
+    (*| (Ccomp c), (a1 :: a2 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      let cond := transl_cbranch_int32s c (make_optR0 false is_inv) in
+      let hv1 := fsi_sreg_get prev a1 in
+      let hv2 := fsi_sreg_get prev a2 in
+      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
+       Some (cond, lhsv)*)
+      (*| (Ccompu c), (a1 :: a2 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      let cond := transl_cbranch_int32u c (make_optR0 false is_inv) in
+      let hv1 := fsi_sreg_get prev a1 in
+      let hv2 := fsi_sreg_get prev a2 in
+      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
+      Some (cond, lhsv)
+  | (Ccompimm c n), (a1 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      let hv1 := fsi_sreg_get prev a1 in
+      (if Int.eq n Int.zero then
+        let lhsv := make_lhsv_cmp is_inv hv1 hv1 in
+        let cond := transl_cbranch_int32s c (make_optR0 true is_inv) in
+        Some (cond, lhsv)
+      else
+        let hvs := loadimm32 n in
+        let lhsv := make_lhsv_cmp is_inv hv1 hvs in
+        let cond := transl_cbranch_int32s c (make_optR0 false is_inv) in
+        Some (cond, lhsv))
+  | (Ccompuimm c n), (a1 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      let hv1 := fsi_sreg_get prev a1 in
+      (if Int.eq n Int.zero then
+        let lhsv := make_lhsv_cmp is_inv hv1 hv1 in
+        let cond := transl_cbranch_int32u c (make_optR0 true is_inv) in
+        Some (cond, lhsv)
+      else
+        let hvs := loadimm32 n in
+        let lhsv := make_lhsv_cmp is_inv hv1 hvs in
+        let cond := transl_cbranch_int32u c (make_optR0 false is_inv) in
+         Some (cond, lhsv))
+  | (Ccompl c), (a1 :: a2 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      let cond := transl_cbranch_int64s c (make_optR0 false is_inv) in
+      let hv1 := fsi_sreg_get prev a1 in
+      let hv2 := fsi_sreg_get prev a2 in
+      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
+      Some (cond, lhsv)
+  | (Ccomplu c), (a1 :: a2 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      let cond := transl_cbranch_int64u c (make_optR0 false is_inv) in
+      let hv1 := fsi_sreg_get prev a1 in
+      let hv2 := fsi_sreg_get prev a2 in
+      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
+      Some (cond, lhsv)
+  | (Ccomplimm c n), (a1 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      let hv1 := fsi_sreg_get prev a1 in
+      (if Int64.eq n Int64.zero then
+        let lhsv := make_lhsv_cmp is_inv hv1 hv1 in
+        let cond := transl_cbranch_int64s c (make_optR0 true is_inv) in
+        Some (cond, lhsv)
+      else
+        let hvs := loadimm64 n in
+        let lhsv := make_lhsv_cmp is_inv hv1 hvs in
+        let cond := transl_cbranch_int64s c (make_optR0 false is_inv) in
+        Some (cond, lhsv))
+  | (Ccompluimm c n), (a1 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      let hv1 := fsi_sreg_get prev a1 in
+      (if Int64.eq n Int64.zero then
+        let lhsv := make_lhsv_cmp is_inv hv1 hv1 in
+        let cond := transl_cbranch_int64u c (make_optR0 true is_inv) in
+        Some (cond, lhsv)
+      else
+        let hvs := loadimm64 n in
+        let lhsv := make_lhsv_cmp is_inv hv1 hvs in
+        let cond := transl_cbranch_int64u c (make_optR0 false is_inv) in
+        Some (cond, lhsv))
+  | (Ccompf c), (f1 :: f2 :: nil) =>
+      let hv1 := fsi_sreg_get prev f1 in
+      let hv2 := fsi_sreg_get prev f2 in
+      let is_inv := is_inv_cmp_float c in
+      let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
+      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
+      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
+      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
+         expanse_cbranch_fp true cond_single c lhsv*)
+  | _, _ => None
+   end.
+
 (** Auxiliary lemmas on comparisons *)
 
 (* Signed ints *)
@@ -360,6 +512,14 @@ Proof.
   repeat destruct (_ && _); simpl; auto.
 Qed.
 
+Remark ltu_12_wordsize:
+  Int.ltu (Int.repr 12) Int.iwordsize = true.
+Proof.
+  unfold Int.iwordsize, Int.zwordsize. simpl.
+  unfold Int.ltu. apply zlt_true.
+  rewrite !Int.unsigned_repr; try cbn; try omega.
+Qed.
+
 (* Signed longs *)
 
 Lemma xor_neg_ltle_cmpl: forall v1 v2,
@@ -400,6 +560,24 @@ Proof.
     rewrite Int64.xor_is_zero in EQ1; congruence.
 Qed.
 
+Lemma cmp_ltle_add_one: forall v n,
+  Int.eq n (Int.repr Int.max_signed) = false ->
+  Some (Val.of_optbool (Val.cmp_bool Clt v (Vint (Int.add n Int.one)))) =
+  Some (Val.of_optbool (Val.cmp_bool Cle v (Vint n))).
+Proof.
+  intros v n EQMAX. unfold Val.cmp_bool; destruct v; simpl; auto.
+  unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1).
+  destruct (zlt (Int.signed n) (Int.signed i)).
+  rewrite zlt_false by omega. auto.
+  rewrite zlt_true by omega. auto.
+  rewrite Int.add_signed. symmetry; apply Int.signed_repr. 
+  specialize (Int.eq_spec n (Int.repr Int.max_signed)).
+  rewrite EQMAX; simpl; intros.
+  assert (Int.signed n <> Int.max_signed).
+  { red; intros E. elim H. rewrite <- (Int.repr_signed n). rewrite E. auto. }
+  generalize (Int.signed_range n); omega.
+Qed.
+
 Lemma cmpl_ltle_add_one: forall v n,
   Int64.eq n (Int64.repr Int64.max_signed) = false ->
   Some (Val.of_optbool (Val.cmpl_bool Clt v (Vlong (Int64.add n Int64.one)))) =
@@ -418,6 +596,26 @@ Proof.
   generalize (Int64.signed_range n); omega.
 Qed.
 
+Remark lt_maxsgn_false_int: forall i,
+  Int.lt (Int.repr Int.max_signed) i = false.
+Proof.
+  intros; unfold Int.lt.
+  specialize  Int.signed_range with i; intros.
+  rewrite zlt_false; auto. destruct H.
+  rewrite Int.signed_repr; try (cbn; lia).
+  apply Z.le_ge. trivial.
+Qed.
+
+Remark lt_maxsgn_false_long: forall i,
+  Int64.lt (Int64.repr Int64.max_signed) i = false.
+Proof.
+  intros; unfold Int64.lt.
+  specialize  Int64.signed_range with i; intros.
+  rewrite zlt_false; auto. destruct H.
+  rewrite Int64.signed_repr; try (cbn; lia).
+  apply Z.le_ge. trivial.
+Qed.
+
 (* Unsigned longs *)
 
 Lemma xor_neg_ltle_cmplu: forall mptr v1 v2,
@@ -593,6 +791,66 @@ Proof.
     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;
+    try rewrite xor_neg_ltle_cmp; trivial;
+    unfold Val.cmp, may_undef_int, zero32, Val.add; simpl;
+    destruct v; auto.
+  all:
+    try rewrite ltu_12_wordsize;
+    try rewrite <- H;
+    try (apply cmp_ltle_add_one; auto);
+    try rewrite Int.add_commut, Int.add_zero_l in *;
+    try (
+    simpl; trivial;
+    try rewrite Int.xor_is_zero;
+    try destruct (Int.lt _ _) eqn:EQLT; trivial;
+    try rewrite lt_maxsgn_false_int in EQLT;
+    simpl; trivial; try discriminate; fail).
+Qed.
+
 Lemma simplify_ccompuimm_correct ge sp hst st c r n rs0 m m0 v: forall
   (SMEM : forall (m : mem) (b : Values.block) (ofs : Z),
            seval_smem ge sp (si_smem st) rs0 m0 = Some m ->
@@ -612,36 +870,31 @@ Proof.
   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.
-  (* Simplify make immediate and decompose subcases *)
   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.
-  (* Ceq, Cne, Clt = itself *)
-  all: intros; try apply Int.same_if_eq in EQIMM; subst; trivial.
-  (* Cle = xor (Clt) *)
-  all: try apply xor_neg_ltle_cmpu; trivial.
-  (* Others subcases with swap/negation *)
-  all:
-    unfold Val.cmpu;
-    try apply Int.same_if_eq in EQLO; subst;
-    try rewrite Int.add_commut, Int.add_zero_l in *; trivial;
-    try (rewrite <- xor_neg_ltle_cmpu; unfold Val.cmpu;
-    trivial; fail);
-    try (replace (Clt) with (swap_comparison Cgt) by auto;
-    rewrite Val.swap_cmpu_bool; trivial; fail);
-    try (replace (Clt) with (negate_comparison Cge) by auto;
-    rewrite Val.negate_cmpu_bool; rewrite xor_neg_optb; trivial; fail).
-  all: rewrite HMEM; trivial.
+    rewrite HMEM;
+    unfold may_undef_int, Val.cmpu;
+    destruct v; simpl; auto;
+    try rewrite EQIMM; try destruct (Archi.ptr64); simpl;
+    try rewrite ltu_12_wordsize; trivial;
+    try rewrite Int.add_commut, Int.add_zero_l;
+    try destruct (Int.ltu _ _) eqn:EQLTU; simpl;
+    try rewrite EQLTU; simpl;
+    trivial.
 Qed.
 
 Lemma simplify_ccompl_correct ge sp hst st c r r0 rs0 m0 v v0: forall
@@ -718,53 +971,64 @@ 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.
-  (* Simplify make immediate and decompose subcases *)
-  2,4,6,10,12:
-    try (specialize make_immed64_sound with n;
-    destruct (make_immed64 n) eqn:EQMKI_A0).
-  20:
-    try (specialize make_immed32_sound with (Int.one);
-    destruct (make_immed32 Int.one) eqn:EQMKI_A1).
-  20,21:
-    try (specialize make_immed64_sound with (Int64.add n Int64.one);
-    destruct (make_immed64 (Int64.add n Int64.one)) eqn:EQMKI_A2).
   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 destruct (Int64.eq lo0 Int64.zero) eqn:EQLO064;
-    try destruct (Int64.eq n (Int64.repr Int64.max_signed)) eqn:EQMAX;
+    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.
-  (* Ceq, Cne, Clt = itself *)
-  all: intros; try apply Int64.same_if_eq in EQIMM; subst;
-       try (rewrite optbool_mktotal; trivial; fail).
-  (* Others simple subcases *)
-  all:
-    unfold Val.cmpl;
-    try apply Int64.same_if_eq in EQLO64; subst;
-    try rewrite Int64.add_commut, Int64.add_zero_l in *; trivial;
-    try (rewrite <- xor_neg_ltle_cmpl; unfold Val.cmpl;
-    trivial; fail);
-    try erewrite xorl_zero_eq_cmpl; eauto;
-    try apply xor_neg_ltle_cmpl; 
-    try apply xor_neg_ltge_cmpl;
-    trivial;
-    try rewrite optbool_mktotal; trivial.
-
+    try rewrite OK2;
+    unfold may_undef_luil;
+    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, may_undef_luil, Val.addl;
+    try rewrite xorl_zero_eq_cmpl; trivial;
+    try rewrite optbool_mktotal; trivial;
+    unfold may_undef_int, zero32, Val.add; simpl;
+    destruct v; auto.
+  6,7,8:
+      try rewrite <- optbool_mktotal; trivial;
+      try rewrite Int64.add_commut, Int64.add_zero_l in *;
+      try fold (Val.cmpl Clt (Vlong i) (Vlong imm));
+      try fold (Val.cmpl Clt (Vlong i) (Vlong (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12)))));
+      try fold (Val.cmpl Clt (Vlong i) (Vlong (Int64.add (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) lo)));
+      try rewrite xor_neg_ltge_cmpl; trivial;
+      try rewrite xor_neg_ltle_cmpl; trivial.
   all:
-    try apply Int64.same_if_eq in EQLO064; subst;
-    try rewrite (Int64.add_commut (Int64.sign_ext 32 (Int64.shl hi0 (Int64.repr 12))) Int64.zero) in H;
-    try rewrite (Int64.add_commut (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) Int64.zero) in H;
-    try rewrite Int64.add_zero_l in H; try rewrite <- H;
-    try apply cmpl_ltle_add_one; auto.
-all: admit.
-Admitted.
+    try rewrite <- H;
+    try apply cmpl_ltle_add_one; auto;
+    try rewrite ltu_12_wordsize;
+    try rewrite Int.add_commut, Int.add_zero_l in *;
+    try rewrite Int64.add_commut, Int64.add_zero_l in *;
+    simpl; try rewrite lt_maxsgn_false_long;
+    try (rewrite <- H; trivial; fail);
+    simpl; trivial.
+Qed.
 
 Lemma simplify_ccompluimm_correct ge sp hst st c r n rs0 m m0 v: forall
   (SMEM : forall (m : mem) (b : Values.block) (ofs : Z),
@@ -805,7 +1069,7 @@ Proof.
   all: try apply xor_neg_ltle_cmplu; trivial.
   (* Others subcases with swap/negation *)
   all:
-    unfold Val.cmplu;
+    unfold Val.cmplu, may_undef_int, zero64, Val.addl;
     try apply Int64.same_if_eq in EQLO; subst;
     try rewrite Int64.add_commut, Int64.add_zero_l in *; trivial;
     try (rewrite <- xor_neg_ltle_cmplu; unfold Val.cmplu;
@@ -814,10 +1078,15 @@ Proof.
     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);
-    rewrite optbool_mktotal; trivial.
+    try rewrite optbool_mktotal; trivial.
   all:
+    try destruct v; simpl; auto;
+    try destruct (Archi.ptr64); simpl;
+    try rewrite EQIMM;
     try rewrite HMEM; trivial;
-    rewrite <- xor_neg_ltge_cmplu; unfold Val.cmplu; rewrite <- optbool_mktotal; 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
@@ -945,7 +1214,7 @@ Proof.
   (* Ccompu *)
   - eapply simplify_ccompu_correct; eauto.
   (* Ccompimm *)
-  - (* TODO gourdinl *) admit.
+  - eapply simplify_ccompimm_correct; eauto.
   (* Ccompuimm *)
   - eapply simplify_ccompuimm_correct; eauto.
   (* Ccompl *)
@@ -953,7 +1222,7 @@ Proof.
   (* Ccomplu *)
   - eapply simplify_ccomplu_correct; eauto.
   (* Ccomplimm *)
-  - admit.
+  - eapply simplify_ccomplimm_correct; eauto.
   (* Ccompluimm *)
   - eapply simplify_ccompluimm_correct; eauto.
   (* Ccompf *)
@@ -964,7 +1233,36 @@ Proof.
   - eapply simplify_ccompfs_correct; eauto.
   (* Cnotcompfs *)
   - eapply simplify_cnotcompfs_correct; eauto.
-      Admitted.
+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.
+
+  all:
+    repeat (destruct l; simpl in H; try congruence);
+    destruct c; inv H; simpl;
+    erewrite !fsi_sreg_get_correct; eauto;
+    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 (destruct (seval_smem ge sp (si_smem st) rs0 m0) eqn:OKmem; try congruence).
+
+  all:
+    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.*)
+  all:admit.
+Admitted.
 (*Qed.*)
 Global Opaque target_op_simplify.
-
+Global Opaque target_cbranch_expanse.
diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index 581229c6..00b49bc1 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -27,6 +27,24 @@ Definition apply_bin_r0 {B} (optR0: option bool) (sem: aval -> aval -> B) (v1 v2
   | Some false => sem v1 vz
   end.
 
+Definition may_undef_int (is_long: bool) (sem: aval -> aval -> aval) (v1 vimm vz: aval): aval :=
+  if negb is_long then
+    match v1 with
+    | I _ => sem vimm vz
+    | _ => Ifptr Ptop
+    end
+  else
+    match v1 with
+    | L _ => sem vimm vz
+    | _ => Ifptr Ptop
+    end.
+
+Definition may_undef_luil (v1: aval) (n: int64): aval :=
+  match v1 with
+  | L _ => sign_ext 32 (shll (L n) (L (Int64.repr 12)))
+  | _ => Ifptr Ptop
+  end.
+
 Definition eval_static_condition (cond: condition) (vl: list aval): abool :=
   match cond, vl with
   | Ccomp c, v1 :: v2 :: nil => cmp_bool c v1 v2
@@ -172,8 +190,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | OEsltiw n, v1::nil => of_optbool (cmp_bool Clt v1 (I n))
   | OEsltiuw n, v1::nil => of_optbool (cmpu_bool Clt v1 (I n))
   | OExoriw n, v1::nil => xor v1 (I n)
-  | OEluiw n, nil => I (Int.shl n (Int.repr 12))
-  | OEaddiwr0 n, nil => add (I n) zero32
+  | OEluiw n is_long, v1::nil => may_undef_int is_long shl v1 (I n) (I (Int.repr 12))
+  | OEaddiwr0 n is_long, v1::nil => may_undef_int is_long add v1 (I n) zero32
   | OEseql optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Ceq) v1 v2 zero64)
   | OEsnel optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Cne) v1 v2 zero64)
   | OEsequl optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64)
@@ -183,8 +201,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | OEsltil n, v1::nil => of_optbool (cmpl_bool Clt v1 (L n))
   | OEsltiul n, v1::nil => of_optbool (cmplu_bool Clt v1 (L n))
   | OExoril n, v1::nil => xorl v1 (L n)
-  | OEluil n, nil => L (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12)))
-  | OEaddilr0 n, nil => addl (L n) zero64
+  | OEluil n, v1::nil => may_undef_luil v1 n
+  | OEaddilr0 n, v1::nil => may_undef_int true addl v1 (L n) zero64
   | OEloadli n, nil => L (n)
   | OEfeqd, v1::v2::nil => of_optbool (cmpf_bool Ceq v1 v2)
   | OEfltd, v1::v2::nil => of_optbool (cmpf_bool Clt v1 v2)
@@ -340,6 +358,13 @@ Proof.
   unfold Val.cmp; apply of_optbool_sound; eauto with va.
   unfold Val.cmpu; apply of_optbool_sound; eauto with va.
   unfold zero32; simpl; eauto with va.
+
+  1,2,11,12:
+    try unfold Op.may_undef_int, may_undef_int, Op.zero32, zero32, Op.zero64, zero64;
+    try unfold Op.may_undef_luil, may_undef_luil; simpl; unfold ntop1;
+    inv H1; try destruct is_long; simpl; try destruct (Int.ltu _ _); eauto with va;
+    try apply vmatch_ifptr_i; try apply vmatch_ifptr_l.
+
   3,4,6: apply eval_cmplu_sound; auto.
   1,2,3: apply eval_cmpl_sound; auto.
   unfold Val.cmpl; apply of_optbool_maketotal_sound; eauto with va.
diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v
index 4a1a5f5b..06fdaab4 100644
--- a/scheduling/RTLpathSE_impl.v
+++ b/scheduling/RTLpathSE_impl.v
@@ -647,27 +647,6 @@ Proof.
     explore; try congruence.
 Qed.
 
-(* TODO gourdinl MOVE EXPANSIONS BELOW ELSEWHERE *)
-
-(* TODO gourdinl IF NEEDED LATER Fixpoint hlist_sval (l: list hsval): ?? list_hsval :=
-  match l with
-  | nil => hSnil()
-  | r::l =>
-    DO lhsv <~ hlist_sval l;;
-    hScons r lhsv
-   end.*)
-
-(*
-
-
-
-
-
-
-
-
- *)
-
 (** simplify a symbolic value before assignment to a register *)
 Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hsval :=
   match rsv with
@@ -687,729 +666,6 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hs
        hSload hst NOTRAP chunk addr lhsv
   end.
 
-(*
-Lemma simplify_nothing lr (hst: hsistate_local) op:
-  WHEN DO lhsv <~ hlist_args hst lr;; hSop op lhsv ~> hv
-  THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) 
-          (m0 : mem) (st : sistate_local),
-        hsilocal_refines ge sp rs0 m0 hst st ->
-        hsok_local ge sp rs0 m0 hst ->
-        (SOME args <-
-         seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0
-         IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
-            IN eval_operation ge sp op args m) <> None ->
-        seval_sval ge sp (hsval_proj hv) rs0 m0 =
-        (SOME args <-
-         seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0
-         IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
-            IN eval_operation ge sp op args m)).
-Proof.
-  wlp_simplify.
-  generalize (H0 ge sp rs0 m0 (list_sval_inj (map (si_sreg st) lr)) (si_smem st)); clear H0.
-  destruct (seval_smem ge sp (si_smem st) rs0 m0) as [m|] eqn:X; eauto.
-  intro H0; clear H0; simplify_SOME z; congruence. 
-Qed.
-
-
-Lemma xor_ceq_zero: forall v n cmp,
-  cmp = Ceq \/ cmp = Cne ->
-  Some
-    (Val.of_optbool (Val.cmp_bool cmp (Val.xor v (Vint n)) (Vint Int.zero))) =
-  Some (Val.of_optbool (Val.cmp_bool cmp v (Vint n))).
-Proof.
-  intros; destruct v; unfold Val.xor; simpl; auto.
-  destruct cmp, H; try discriminate; simpl;
-  destruct (Int.eq (Int.xor i n) Int.zero) eqn:EQ;
-  rewrite Int.xor_is_zero in EQ; rewrite EQ; trivial.
-Qed.
-
-(* TODO gourdinl Lemma xor_neg_ltge_cmp: forall v1 v2,
-  Some (Val.xor (Val.cmp Clt v1 v2) (Vint Int.one)) =
-  Some (Val.of_optbool (Val.cmp_bool Cge v1 v2)).
-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.*)
-
-(* TODO gourdinl useless? Lemma cmp_neg_ltgt_cmp: forall v1 v2,
-  Some (Val.cmp Clt v1 v2) = Some (Val.of_optbool (Val.cmp_bool Cgt v2 v1)).
-Proof.
-  intros. eapply f_equal.
-  destruct v1, v2; simpl; try congruence;
-  unfold Val.cmp; simpl; auto.
-   Qed.*)
-
-
-(* TODO gourdinl Lemma xor_neg_ltge_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) Cge v1 v2)).
-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.*)
-
-(* TODO gourdinl Lemma cmp_neg_ltgt_cmpu: forall mptr v1 v2,
-  Some (Val.cmpu (Mem.valid_pointer mptr) Clt v1 v2) =
-  Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer mptr) Cgt v2 v1)).
-Proof.
-  intros. eapply f_equal.
-  destruct v1, v2; simpl; try congruence;
-  unfold Val.cmpu; simpl; auto.
-  destruct (Archi.ptr64);
-  destruct (eq_block b b0); destruct (eq_block b0 b);
-  try congruence.
-  - repeat destruct (_ || _); simpl; auto.
-  - repeat destruct (_ && _); simpl; auto.
-   Qed.*)
-
-Lemma optbool_mktotal: forall v,
-  Some (Val.maketotal (option_map Val.of_bool v)) =
-  Some (Val.of_optbool v).
-Proof.
-  intros. eapply f_equal.
-  destruct v; simpl; auto.
-Qed.
-
-Lemma cmplu_optbool_mktotal: forall mptr cmp v1 v2,
-  Some (Val.maketotal (Val.cmplu (Mem.valid_pointer mptr) cmp v1 v2)) =
-  Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer mptr) cmp v1 v2)).
-Proof.
-  intros. eapply f_equal.
-  destruct v1, v2; simpl; try congruence;
-  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.
-Qed.
-
-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 cmp_neg_ltgt_cmpl: forall v1 v2,
-  Some (Val.maketotal (Val.cmpl Clt v1 v2)) =
-  Some (Val.of_optbool (Val.cmpl_bool Cgt 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 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 cmp_neg_ltgt_cmplu: forall mptr v1 v2,
-  Some (Val.maketotal (Val.cmplu (Mem.valid_pointer mptr) Clt v1 v2)) =
-  Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer mptr) Cgt 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.
-
-
-
-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.
-
-Lemma cmp_neg_ltgt_cmpf: forall v1 v2,
-  Some (Val.cmpf Clt v1 v2) = Some (Val.of_optbool (Val.cmpf_bool Cgt v2 v1)).
-Proof.
-  intros. eapply f_equal.
-  destruct v1, v2; simpl; try congruence;
-  unfold Val.cmpf; simpl; auto.
-  replace Cgt with (swap_comparison Clt) by auto.
-  rewrite Float.cmp_swap.
-  destruct (Float.cmp _ _ _); simpl; auto.
-Qed.
-
-Lemma cmp_neg_lege_cmpf: forall v1 v2,
-  Some (Val.cmpf Cle v1 v2) = Some (Val.of_optbool (Val.cmpf_bool Cge v2 v1)).
-Proof.
-  intros. eapply f_equal.
-  destruct v1, v2; simpl; try congruence;
-  unfold Val.cmpf; simpl; auto.
-  replace Cle with (swap_comparison Cge) by auto.
-  rewrite Float.cmp_swap.
-  destruct (Float.cmp _ _ _); simpl; auto.
-Qed.
-
-
-
-(* TODO gourdinl Lemma cmp_le_max: forall v*)
-  (*(CONTRA: Some*)
-       (*(Val.of_optbool (Val.cmp_bool Cle v (Vint (Int.repr Int.max_signed)))) =*)
-     (*None -> False),*)
-  (*Some (Vint Int.one) =*)
-  (*Some (Val.of_optbool (Val.cmp_bool Cle v (Vint (Int.repr Int.max_signed)))).*)
-(*Proof.*)
-  (*intros; destruct v. simpl in *; try discriminate CONTRA; auto.*)
-
-Lemma simplify_ccomp_correct: forall c r r0 (hst: hsistate_local),
-  WHEN DO hv1 <~ hsi_sreg_get hst r;;
-       DO hv2 <~ hsi_sreg_get hst r0;;
-       DO lhsv <~ make_lhsv_cmp (is_inv_cmp_int c) hv1 hv2;;
-       cond_int32s c lhsv None ~> hv
-  THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) 
-          (m0 : mem) (st : sistate_local),
-        hsilocal_refines ge sp rs0 m0 hst st ->
-        hsok_local ge sp rs0 m0 hst ->
-        (SOME args <-
-         seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0
-           m0
-         IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
-            IN eval_operation ge sp (Ocmp (Ccomp c)) args m) <> None ->
-        seval_sval ge sp (hsval_proj hv) rs0 m0 =
-        (SOME args <-
-         seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0
-           m0
-         IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
-            IN eval_operation ge sp (Ocmp (Ccomp c)) args m)).
-Proof.
-  unfold cond_int32s in *; destruct c;
-  wlp_simplify;
-  destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
-  all: try (simplify_SOME z; contradiction; fail).
-  all:
-    try (erewrite H7; eauto; erewrite H6; eauto; erewrite H5; eauto);
-    erewrite H4; eauto; erewrite H3; eauto; erewrite H2; eauto;
-    erewrite H1; eauto; erewrite H0; eauto; erewrite H; eauto;
-    simplify_SOME z; unfold Val.cmp.
-    - intros; apply xor_neg_ltle_cmp.
-    - intros; replace (Clt) with (swap_comparison Cgt) by auto;
-      rewrite Val.swap_cmp_bool; trivial.
-    - intros; replace (Clt) with (negate_comparison Cge) by auto;
-      rewrite Val.negate_cmp_bool.
-      rewrite xor_neg_optb; trivial.
-Qed.
-
-Lemma simplify_ccompu_correct: forall c r r0 (hst: hsistate_local),
-  WHEN DO hv1 <~ hsi_sreg_get hst r;;
-       DO hv2 <~ hsi_sreg_get hst r0;;
-       DO lhsv <~ make_lhsv_cmp (is_inv_cmp_int c) hv1 hv2;;
-       cond_int32u c lhsv None ~> hv
-  THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) 
-          (m0 : mem) (st : sistate_local),
-        hsilocal_refines ge sp rs0 m0 hst st ->
-        hsok_local ge sp rs0 m0 hst ->
-        (SOME args <-
-         seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0
-           m0
-         IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
-            IN eval_operation ge sp (Ocmp (Ccompu c)) args m) <> None ->
-        seval_sval ge sp (hsval_proj hv) rs0 m0 =
-        (SOME args <-
-         seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0
-           m0
-         IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
-            IN eval_operation ge sp (Ocmp (Ccompu c)) args m)).
-Proof.
-  unfold cond_int32u in *; destruct c;
-  wlp_simplify;
-  destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
-  all: try (simplify_SOME z; contradiction; fail).
-  all:
-    try (erewrite H7; eauto; erewrite H6; eauto; erewrite H5; eauto);
-    erewrite H4; eauto; erewrite H3; eauto; erewrite H2; eauto;
-    erewrite H1; eauto; erewrite H0; eauto; erewrite H; eauto;
-    simplify_SOME z; unfold Val.cmpu.
-    - intros; apply xor_neg_ltle_cmpu.
-    - intros; replace (Clt) with (swap_comparison Cgt) by auto;
-      rewrite Val.swap_cmpu_bool; trivial.
-    - intros; replace (Clt) with (negate_comparison Cge) by auto;
-      rewrite Val.negate_cmpu_bool.
-      rewrite xor_neg_optb; trivial.
-Qed.
-
-Lemma mkimm_single_equal: forall n imm,
-  make_immed32 n = Imm32_single imm ->
-  n = imm.
-Proof.
-  intros. unfold make_immed32 in H.
-  destruct (Int.eq _ _); inv H; auto.
-Qed.
-
-Lemma mkimm_pair_equal: forall n hi lo,
-  make_immed32 n = Imm32_pair hi lo ->
-  hi = (Int.shru (Int.sub n (Int.sign_ext 12 n)) (Int.repr 12)) /\
-  lo = (Int.sign_ext 12 n).
-Proof.
-  intros. unfold make_immed32 in H.
-  destruct (Int.eq _ _) in H; try congruence.
-  inv H. auto.
-Qed.
-
-(* TODO gourdinl Lemma mkimm_pair_lo_zero_equal: forall n hi lo,
-  make_immed32 n = Imm32_pair hi lo ->
-  Int.eq n Int.zero = false ->
-  Int.eq lo Int.zero = true ->
-  n = Int.shl hi (Int.repr 12).
-Proof.
-  intros. unfold make_immed32 in H.
-  destruct (Int.eq _ _) in H; try discriminate.
-  inv H. apply Int.same_if_eq in H1. rewrite H1.
-  rewrite Int.sub_zero_l. unfold Int.shru, Int.shl.
- *)
-
-Lemma simplify_ccompimm_correct: forall c n r (hst: hsistate_local),
-  WHEN DO hv1 <~ hsi_sreg_get hst r;; expanse_condimm_int32s c hv1 n ~> hv
-  THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) 
-          (m0 : mem) (st : sistate_local),
-        hsilocal_refines ge sp rs0 m0 hst st ->
-        hsok_local ge sp rs0 m0 hst ->
-        (SOME args <-
-         seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r])) rs0 m0
-         IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
-            IN eval_operation ge sp (Ocmp (Ccompimm c n)) args m) <> None ->
-        seval_sval ge sp (hsval_proj hv) rs0 m0 =
-        (SOME args <-
-         seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r])) rs0 m0
-         IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
-            IN eval_operation ge sp (Ocmp (Ccompimm c n)) args m)).
-Proof.
-  unfold expanse_condimm_int32s, cond_int32s in *; destruct c;
-  intros; destruct (Int.eq n Int.zero) eqn:EQIMM; simpl;
-  unfold loadimm32, sltimm32, xorimm32, opimm32, load_hilo32.
-  1,3,5,7,9,11: 
-    wlp_simplify;
-    destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence;
-    try (simplify_SOME z; contradiction; fail);
-    try erewrite H9; eauto; try erewrite H8; eauto;
-    try erewrite H7; eauto; try erewrite H6; eauto; try erewrite H5; eauto;
-    try erewrite H4; eauto; try erewrite H3; eauto; try erewrite H2; eauto;
-    try erewrite H1; eauto; try erewrite H0; eauto; try erewrite H; eauto;
-    simplify_SOME z; unfold Val.cmpu, zero32; intros; try contradiction.
-  4: rewrite <- xor_neg_ltle_cmp; unfold Val.cmp.
-  5: intros; replace (Clt) with (swap_comparison Cgt) by auto;
-     unfold Val.cmp; rewrite Val.swap_cmp_bool; trivial.
-  6: intros; replace (Clt) with (negate_comparison Cge) by auto;
-     unfold Val.cmp; rewrite Val.negate_cmp_bool; rewrite xor_neg_optb.
-  1,2,3,4,5,6: apply Int.same_if_eq in EQIMM; subst; trivial.
-  all:
-    specialize make_immed32_sound with n;
-    destruct (make_immed32 n) eqn:EQMKI;
-    try destruct (Int.eq n (Int.repr Int.max_signed)) eqn:EQMAX;
-    try destruct (Int.eq lo Int.zero) eqn:EQLO.
-  19,21,22:
-    specialize make_immed32_sound with (Int.one);
-    destruct (make_immed32 Int.one) eqn:EQMKI_A1.
-  25,26,27:
-    specialize make_immed32_sound with (Int.add n Int.one);
-    destruct (make_immed32 (Int.add n Int.one)) eqn:EQMKI_A2.
-  all:
-    wlp_simplify;
-    destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
-  all: try (simplify_SOME z; contradiction; fail).
-  all:
-    try erewrite H12; eauto; try erewrite H11; eauto;
-    try erewrite H10; eauto; try erewrite H9; eauto; try erewrite H8; eauto;
-    try erewrite H7; eauto; try erewrite H6; eauto; try erewrite H5; eauto;
-    try erewrite H4; eauto; try erewrite H3; eauto; try erewrite H2; eauto;
-    try erewrite H1; eauto; try erewrite H0; eauto; try erewrite H; eauto;
-    simplify_SOME z; unfold Val.cmp, zero32; intros; try contradiction.
-  all: try apply Int.same_if_eq in H1; subst.
-  all: try apply Int.same_if_eq in EQLO; subst.
-  all: try apply Int.same_if_eq in EQMAX; subst.
-  all: try rewrite Int.add_commut, Int.add_zero_l; trivial.
-  all: try apply xor_ceq_zero; auto.
-  (* Problème d'implémentation lié au addiwr0 ?
-     --> On dirait que comme l'instruction n'a pas d'argument une fois expansée,
-     un cas spécial se produit si l'argument de départ n'est pas un entier :
-     L'instruction addiwr0 est configurée pour toujours renvoyer Int.one,
-     mais si le premier argument de la comparaison originelle n'est pas un
-     Vint, alors on se retrouve avec :
-      Some (Vint Int.one) = Some (Val.of_optbool None)
-      <-> Some (Vint Int.zero) = Some (Vundef)
-     Il faudrait peut-être modifier la sémantique dans Op pour éliminer ce cas. *)
-  admit.
-  admit.
-  admit.
-  admit.
-  admit.
-  admit.
-  admit.
-  admit.
-  admit.
-  { apply cmp_ltle_add_one; auto. }
-  { apply Int.same_if_eq in H2; subst.
-    rewrite (Int.add_commut (Int.shl hi (Int.repr 12)) Int.zero) in H.
-    rewrite Int.add_zero_l in H. rewrite <- H.
-    apply cmp_ltle_add_one; auto. }
-  { rewrite <- H. apply cmp_ltle_add_one; auto. }
-  { rewrite (Int.add_commut (Int.shl hi (Int.repr 12))). rewrite Int.add_zero_l.
-    apply cmp_ltle_add_one. rewrite Int.add_commut, Int.add_zero_l in EQMAX.
-    auto. }
-  { apply Int.same_if_eq in H2; subst.
-    rewrite (Int.add_commut (Int.shl hi0 (Int.repr 12)) Int.zero) in H.
-    rewrite Int.add_zero_l in H. rewrite <- H.
-    rewrite (Int.add_commut (Int.shl hi (Int.repr 12)) Int.zero) in *.
-    rewrite Int.add_zero_l in *. apply cmp_ltle_add_one; auto. }
-  { rewrite <- H.
-    rewrite (Int.add_commut (Int.shl hi (Int.repr 12)) Int.zero) in *.
-   rewrite Int.add_zero_l in *. apply cmp_ltle_add_one; auto. }
-  { apply cmp_ltle_add_one; auto. }
-  { apply Int.same_if_eq in H2; subst.
-    rewrite (Int.add_commut (Int.shl hi0 (Int.repr 12)) Int.zero) in H.
-    rewrite Int.add_zero_l in H. rewrite <- H.
-     apply cmp_ltle_add_one; auto. }
-  { rewrite <- H. apply cmp_ltle_add_one; auto. }
-  { intros; replace (Clt) with (negate_comparison Cge) by auto;
-    rewrite Val.negate_cmp_bool.
-    rewrite xor_neg_optb; trivial. }
-  { intros; replace (Clt) with (negate_comparison Cge) by auto;
-    rewrite Val.negate_cmp_bool.
-    rewrite xor_neg_optb; trivial. }
-  { intros; replace (Clt) with (negate_comparison Cge) by auto;
-    rewrite Val.negate_cmp_bool.
-    rewrite xor_neg_optb; trivial. }
-  { intros; replace (Clt) with (negate_comparison Cge) by auto;
-    rewrite Val.negate_cmp_bool.
-    rewrite xor_neg_optb; trivial. }
-  { intros; replace (Clt) with (negate_comparison Cge) by auto;
-    rewrite Val.negate_cmp_bool.
-    rewrite xor_neg_optb; trivial. }
-  { intros; replace (Clt) with (negate_comparison Cge) by auto;
-    rewrite Val.negate_cmp_bool.
-    rewrite xor_neg_optb; trivial. }
-Admitted.
-(*Qed.*)
-
-
-Lemma simplify_ccompl_correct: forall c r r0 (hst: hsistate_local),
-  WHEN DO hv1 <~ hsi_sreg_get hst r;;
-       DO hv2 <~ hsi_sreg_get hst r0;;
-       DO lhsv <~ make_lhsv_cmp (is_inv_cmp_int c) hv1 hv2;;
-       cond_int64s c lhsv None ~> hv
-  THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) 
-          (m0 : mem) (st : sistate_local),
-        hsilocal_refines ge sp rs0 m0 hst st ->
-        hsok_local ge sp rs0 m0 hst ->
-        (SOME args <-
-         seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0
-           m0
-         IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
-            IN eval_operation ge sp (Ocmp (Ccompl c)) args m) <> None ->
-        seval_sval ge sp (hsval_proj hv) rs0 m0 =
-        (SOME args <-
-         seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0
-           m0
-         IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
-            IN eval_operation ge sp (Ocmp (Ccompl c)) args m)).
-Proof.
-  unfold cond_int64s in *; destruct c;
-  wlp_simplify;
-  destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
-  all: try (simplify_SOME z; contradiction; fail).
-  all:
-    try (erewrite H7; eauto; erewrite H6; eauto; erewrite H5; eauto);
-    erewrite H4; eauto; erewrite H3; eauto; erewrite H2; eauto;
-    erewrite H1; eauto; erewrite H0; eauto; erewrite H; eauto;
-    simplify_SOME z; unfold Val.cmpl.
-    1,2,3: intros; apply optbool_mktotal.
-    - intros; apply xor_neg_ltle_cmpl.
-    - intros; replace (Clt) with (swap_comparison Cgt) by auto;
-      rewrite Val.swap_cmpl_bool; trivial.
-      apply optbool_mktotal.
-    - intros; apply xor_neg_ltge_cmpl.
-Qed.
-
-Lemma simplify_ccomplu_correct: forall c r r0 (hst: hsistate_local),
-  WHEN DO hv1 <~ hsi_sreg_get hst r;;
-       DO hv2 <~ hsi_sreg_get hst r0;;
-       DO lhsv <~ make_lhsv_cmp (is_inv_cmp_int c) hv1 hv2;;
-       cond_int64u c lhsv None ~> hv
-  THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) 
-          (m0 : mem) (st : sistate_local),
-        hsilocal_refines ge sp rs0 m0 hst st ->
-        hsok_local ge sp rs0 m0 hst ->
-        (SOME args <-
-         seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0
-           m0
-         IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
-            IN eval_operation ge sp (Ocmp (Ccomplu c)) args m) <> None ->
-        seval_sval ge sp (hsval_proj hv) rs0 m0 =
-        (SOME args <-
-         seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0
-           m0
-         IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
-            IN eval_operation ge sp (Ocmp (Ccomplu c)) args m)).
-Proof.
-  unfold cond_int64u in *; destruct c;
-  wlp_simplify;
-  destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
-  all: try (simplify_SOME z; contradiction; fail).
-  all:
-    try (erewrite H7; eauto; erewrite H6; eauto; erewrite H5; eauto);
-    erewrite H4; eauto; erewrite H3; eauto; erewrite H2; eauto;
-    erewrite H1; eauto; erewrite H0; eauto; erewrite H; eauto;
-    simplify_SOME z; unfold Val.cmplu.
-    1,2,3: intros; apply optbool_mktotal.
-    - intros; apply xor_neg_ltle_cmplu.
-    - intros; replace (Clt) with (swap_comparison Cgt) by auto;
-      rewrite Val.swap_cmplu_bool; trivial.
-      apply optbool_mktotal.
-    - intros; apply xor_neg_ltge_cmplu.
-Qed.
-
-
-
-Lemma simplify_ccompf_correct: forall c r r0 (hst: hsistate_local),
-  WHEN DO hv1 <~ hsi_sreg_get hst r;;
-       DO hv2 <~ hsi_sreg_get hst r0;;
-       DO lhsv <~ make_lhsv_cmp (is_inv_cmp_float c) hv1 hv2;;
-       expanse_cond_fp false cond_float c lhsv ~> hv
-  THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) 
-          (m0 : mem) (st : sistate_local),
-        hsilocal_refines ge sp rs0 m0 hst st ->
-        hsok_local ge sp rs0 m0 hst ->
-        (SOME args <-
-         seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0
-           m0
-         IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
-            IN eval_operation ge sp (Ocmp (Ccompf c)) args m) <> None ->
-        seval_sval ge sp (hsval_proj hv) rs0 m0 =
-        (SOME args <-
-         seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0
-           m0
-         IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
-            IN eval_operation ge sp (Ocmp (Ccompf c)) args m)).
-Proof.
-  unfold expanse_cond_fp in *; destruct c;
-  wlp_simplify;
-  destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
-  all: try (simplify_SOME z; contradiction; fail).
-  all:
-    try (erewrite H9; eauto; erewrite H8; eauto);
-    try (erewrite H7; eauto; erewrite H6; eauto; erewrite H5; eauto);
-    erewrite H4; eauto; erewrite H3; eauto; erewrite H2; eauto;
-    erewrite H1; eauto; erewrite H0; eauto; erewrite H; eauto;
-    simplify_SOME z; unfold Val.cmpf.
-    - intros; apply xor_neg_eqne_cmpf.
-    - intros; replace (Clt) with (swap_comparison Cgt) by auto;
-      rewrite swap_cmpf_bool; trivial.
-    - intros; replace (Cle) with (swap_comparison Cge) by auto;
-      rewrite swap_cmpf_bool; trivial.
-Qed.
-
-Lemma simplify_cnotcompf_correct: forall c r r0 (hst: hsistate_local),
-  WHEN DO hv1 <~ hsi_sreg_get hst r;;
-       DO hv2 <~ hsi_sreg_get hst r0;;
-       DO lhsv <~ make_lhsv_cmp (is_inv_cmp_float c) hv1 hv2;;
-       expanse_cond_fp true cond_float c lhsv ~> hv
-  THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) 
-          (m0 : mem) (st : sistate_local),
-        hsilocal_refines ge sp rs0 m0 hst st ->
-        hsok_local ge sp rs0 m0 hst ->
-        (SOME args <-
-         seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0
-           m0
-         IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
-            IN eval_operation ge sp (Ocmp (Cnotcompf c)) args m) <> None ->
-        seval_sval ge sp (hsval_proj hv) rs0 m0 =
-        (SOME args <-
-         seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0
-           m0
-         IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
-            IN eval_operation ge sp (Ocmp (Cnotcompf c)) args m)).
-Proof.
-  unfold expanse_cond_fp in *; destruct c;
-  wlp_simplify;
-  destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
-  all: try (simplify_SOME z; contradiction; fail).
-  all:
-    try (erewrite H9; eauto; erewrite H8; eauto);
-    try (erewrite H7; eauto; erewrite H6; eauto; erewrite H5; eauto);
-    erewrite H4; eauto; erewrite H3; eauto; erewrite H2; eauto;
-    erewrite H1; eauto; erewrite H0; eauto; erewrite H; eauto;
-    simplify_SOME z; unfold Val.cmpf.
-    all: intros; apply f_equal;
-    try destruct z0, z2; try destruct z2, z4;
-    try destruct z8, z10;
-    simpl; trivial.
-    2: rewrite Float.cmp_ne_eq; rewrite negb_involutive; trivial.
-    4: replace (Clt) with (swap_comparison Cgt) by auto; rewrite <- Float.cmp_swap; simpl.
-    5: replace (Cle) with (swap_comparison Cge) by auto; rewrite <- Float.cmp_swap; simpl.
-    all: destruct (Float.cmp _ _ _); trivial.
-Qed.
-
-Lemma simplify_ccompfs_correct: forall c r r0 (hst: hsistate_local),
-  WHEN DO hv1 <~ hsi_sreg_get hst r;;
-       DO hv2 <~ hsi_sreg_get hst r0;;
-       DO lhsv <~ make_lhsv_cmp (is_inv_cmp_float c) hv1 hv2;;
-       expanse_cond_fp false cond_single c lhsv ~> hv
-  THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) 
-          (m0 : mem) (st : sistate_local),
-        hsilocal_refines ge sp rs0 m0 hst st ->
-        hsok_local ge sp rs0 m0 hst ->
-        (SOME args <-
-         seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0
-           m0
-         IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
-            IN eval_operation ge sp (Ocmp (Ccompfs c)) args m) <> None ->
-        seval_sval ge sp (hsval_proj hv) rs0 m0 =
-        (SOME args <-
-         seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0
-           m0
-         IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
-            IN eval_operation ge sp (Ocmp (Ccompfs c)) args m)).
-Proof.
-  unfold expanse_cond_fp in *; destruct c;
-  wlp_simplify;
-  destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
-  all: try (simplify_SOME z; contradiction; fail).
-  all:
-    try (erewrite H9; eauto; erewrite H8; eauto);
-    try (erewrite H7; eauto; erewrite H6; eauto; erewrite H5; eauto);
-    erewrite H4; eauto; erewrite H3; eauto; erewrite H2; eauto;
-    erewrite H1; eauto; erewrite H0; eauto; erewrite H; eauto;
-    simplify_SOME z; unfold Val.cmpfs.
-    - intros; apply xor_neg_eqne_cmpfs.
-    - intros; replace (Clt) with (swap_comparison Cgt) by auto;
-      rewrite swap_cmpfs_bool; trivial.
-    - intros; replace (Cle) with (swap_comparison Cge) by auto;
-      rewrite swap_cmpfs_bool; trivial.
-Qed.
-
-Lemma simplify_cnotcompfs_correct: forall c r r0 (hst: hsistate_local),
-  WHEN DO hv1 <~ hsi_sreg_get hst r;;
-       DO hv2 <~ hsi_sreg_get hst r0;;
-       DO lhsv <~ make_lhsv_cmp (is_inv_cmp_float c) hv1 hv2;;
-       expanse_cond_fp true cond_single c lhsv ~> hv
-  THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) 
-          (m0 : mem) (st : sistate_local),
-        hsilocal_refines ge sp rs0 m0 hst st ->
-        hsok_local ge sp rs0 m0 hst ->
-        (SOME args <-
-         seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0
-           m0
-         IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
-            IN eval_operation ge sp (Ocmp (Cnotcompfs c)) args m) <> None ->
-        seval_sval ge sp (hsval_proj hv) rs0 m0 =
-        (SOME args <-
-         seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0
-           m0
-         IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
-            IN eval_operation ge sp (Ocmp (Cnotcompfs c)) args m)).
-Proof.
-  unfold expanse_cond_fp in *; destruct c;
-  wlp_simplify;
-  destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
-  all: try (simplify_SOME z; contradiction; fail).
-  all:
-    try (erewrite H9; eauto; erewrite H8; eauto);
-    try (erewrite H7; eauto; erewrite H6; eauto; erewrite H5; eauto);
-    erewrite H4; eauto; erewrite H3; eauto; erewrite H2; eauto;
-    erewrite H1; eauto; erewrite H0; eauto; erewrite H; eauto;
-    simplify_SOME z; unfold Val.cmpfs.
-    all: intros; apply f_equal;
-    try destruct z0, z2; try destruct z2, z4;
-    try destruct z8, z10;
-    simpl; trivial.
-    2: rewrite Float32.cmp_ne_eq; rewrite negb_involutive; trivial.
-    4: replace (Clt) with (swap_comparison Cgt) by auto; rewrite <- Float32.cmp_swap; simpl.
-    5: replace (Cle) with (swap_comparison Cge) by auto; rewrite <- Float32.cmp_swap; simpl.
-    all: destruct (Float32.cmp _ _ _); trivial.
-   Qed.*)
-
 Lemma simplify_correct rsv lr hst:
   WHEN simplify rsv lr hst ~> hv THEN forall ge sp rs0 m0 st
     (REF: hsilocal_refines ge sp rs0 m0 hst st)
@@ -1443,8 +699,7 @@ Proof.
     destruct (eval_addressing _ _ _ _) as [a|] eqn: Ha; try congruence.
     destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
     destruct (Mem.loadv _ _ _); try congruence.
-(*Qed.*)
-Admitted.
+Qed.
 Global Opaque simplify.
 Local Hint Resolve simplify_correct: wlp.
 
@@ -1544,7 +799,7 @@ Proof.
     rewrite <- X, sok_local_set_sreg. intuition eauto.
     - destruct REF; intuition eauto.
     - generalize REF; intros (OKEQ & _). rewrite OKEQ in * |-; erewrite red_PTree_set_refines; eauto.
-     Qed.
+                    Qed.
 Global Opaque hslocal_set_sreg.
 Local Hint Resolve hslocal_set_sreg_correct: wlp.
 
@@ -1557,45 +812,7 @@ Definition make_lr_prev_cmp (is_inv: bool) (a1 a2: reg) (prev: hsistate_local) :
    hlist_args prev*)
 
 (*
-Definition transl_cbranch_int32s (cmp: comparison) (optR0: option bool) :=
-  match cmp with
-  | Ceq => CEbeqw optR0
-  | Cne => CEbnew optR0
-  | Clt => CEbltw optR0
-  | Cle => CEbgew optR0
-  | Cgt => CEbltw optR0
-  | Cge => CEbgew optR0
-  end.
 
-Definition transl_cbranch_int32u (cmp: comparison) (optR0: option bool) :=
-  match cmp with
-  | Ceq => CEbequw optR0
-  | Cne => CEbneuw optR0
-  | Clt => CEbltuw optR0
-  | Cle => CEbgeuw optR0
-  | Cgt => CEbltuw optR0
-  | Cge => CEbgeuw optR0
-  end.
-
-Definition transl_cbranch_int64s (cmp: comparison) (optR0: option bool) :=
-  match cmp with
-  | Ceq => CEbeql optR0
-  | Cne => CEbnel optR0
-  | Clt => CEbltl optR0
-  | Cle => CEbgel optR0
-  | Cgt => CEbltl optR0
-  | Cge => CEbgel optR0
-  end.
-
-Definition transl_cbranch_int64u (cmp: comparison) (optR0: option bool) :=
-  match cmp with
-  | Ceq => CEbequl optR0
-  | Cne => CEbneul optR0
-  | Clt => CEbltul optR0
-  | Cle => CEbgeul optR0
-  | Cgt => CEbltul optR0
-  | Cge => CEbgeul optR0
-  end.
 
 Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) : ?? (condition * list_hsval) :=
   let normal := is_normal_cmp cmp in
@@ -1605,132 +822,12 @@ Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) : ?? (
   if normal' then RET ((CEbnew (Some false)), hl) else RET ((CEbeqw (Some false)), hl).
   
 Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg) : ?? (condition * list_hsval) :=
-  match cond, args with
-  | (Ccomp c), (a1 :: a2 :: nil) =>
-      let is_inv := is_inv_cmp_int c in
-      let cond := transl_cbranch_int32s c (make_optR0 false is_inv) in
-      DO hv1 <~ hsi_sreg_get prev a1;;
-      DO hv2 <~ hsi_sreg_get prev a2;;
-      DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
-      RET (cond, lhsv)
-  | (Ccompu c), (a1 :: a2 :: nil) =>
-      let is_inv := is_inv_cmp_int c in
-      let cond := transl_cbranch_int32u c (make_optR0 false is_inv) in
-      DO hv1 <~ hsi_sreg_get prev a1;;
-      DO hv2 <~ hsi_sreg_get prev a2;;
-      DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
-      RET (cond, lhsv)
-  | (Ccompimm c n), (a1 :: nil) =>
-      let is_inv := is_inv_cmp_int c in
-      DO hv1 <~ hsi_sreg_get prev a1;;
-      (if Int.eq n Int.zero then
-        DO lhsv <~ make_lhsv_cmp is_inv hv1 hv1;;
-        let cond := transl_cbranch_int32s c (make_optR0 true is_inv) in
-        RET (cond, lhsv)
-      else
-        DO hvs <~ loadimm32 n;;
-        DO lhsv <~ make_lhsv_cmp is_inv hv1 hvs;;
-        let cond := transl_cbranch_int32s c (make_optR0 false is_inv) in
-        RET (cond, lhsv))
-  | (Ccompuimm c n), (a1 :: nil) =>
-      let is_inv := is_inv_cmp_int c in
-      DO hv1 <~ hsi_sreg_get prev a1;;
-      (if Int.eq n Int.zero then
-        DO lhsv <~ make_lhsv_cmp is_inv hv1 hv1;;
-        let cond := transl_cbranch_int32u c (make_optR0 true is_inv) in
-        RET (cond, lhsv)
-      else
-        DO hvs <~ loadimm32 n;;
-        DO lhsv <~ make_lhsv_cmp is_inv hv1 hvs;;
-        let cond := transl_cbranch_int32u c (make_optR0 false is_inv) in
-        RET (cond, lhsv))
-  | (Ccompl c), (a1 :: a2 :: nil) =>
-      let is_inv := is_inv_cmp_int c in
-      let cond := transl_cbranch_int64s c (make_optR0 false is_inv) in
-      DO hv1 <~ hsi_sreg_get prev a1;;
-      DO hv2 <~ hsi_sreg_get prev a2;;
-      DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
-      RET (cond, lhsv)
-  | (Ccomplu c), (a1 :: a2 :: nil) =>
-      let is_inv := is_inv_cmp_int c in
-      let cond := transl_cbranch_int64u c (make_optR0 false is_inv) in
-      DO hv1 <~ hsi_sreg_get prev a1;;
-      DO hv2 <~ hsi_sreg_get prev a2;;
-      DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
-      RET (cond, lhsv)
-  | (Ccomplimm c n), (a1 :: nil) =>
-      let is_inv := is_inv_cmp_int c in
-      DO hv1 <~ hsi_sreg_get prev a1;;
-      (if Int64.eq n Int64.zero then
-        DO lhsv <~ make_lhsv_cmp is_inv hv1 hv1;;
-        let cond := transl_cbranch_int64s c (make_optR0 true is_inv) in
-        RET (cond, lhsv)
-      else
-        DO hvs <~ loadimm64 n;;
-        DO lhsv <~ make_lhsv_cmp is_inv hv1 hvs;;
-        let cond := transl_cbranch_int64s c (make_optR0 false is_inv) in
-        RET (cond, lhsv))
-  | (Ccompluimm c n), (a1 :: nil) =>
-      let is_inv := is_inv_cmp_int c in
-      DO hv1 <~ hsi_sreg_get prev a1;;
-      (if Int64.eq n Int64.zero then
-        DO lhsv <~ make_lhsv_cmp is_inv hv1 hv1;;
-        let cond := transl_cbranch_int64u c (make_optR0 true is_inv) in
-        RET (cond, lhsv)
-      else
-        DO hvs <~ loadimm64 n;;
-        DO lhsv <~ make_lhsv_cmp is_inv hv1 hvs;;
-        let cond := transl_cbranch_int64u c (make_optR0 false is_inv) in
-        RET (cond, lhsv))
-  | (Ccompf c), (f1 :: f2 :: nil) =>
-      DO hv1 <~ hsi_sreg_get prev f1;;
-      DO hv2 <~ hsi_sreg_get prev f2;;
-      let is_inv := is_inv_cmp_float c in
-      DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
-      expanse_cbranch_fp false cond_float c lhsv
-  | (Cnotcompf c), (f1 :: f2 :: nil) =>
-      DO hv1 <~ hsi_sreg_get prev f1;;
-      DO hv2 <~ hsi_sreg_get prev f2;;
-      let is_inv := is_inv_cmp_float c in
-      DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
-      expanse_cbranch_fp true cond_float c lhsv
-  | (Ccompfs c), (f1 :: f2 :: nil) =>
-      DO hv1 <~ hsi_sreg_get prev f1;;
-      DO hv2 <~ hsi_sreg_get prev f2;;
-      let is_inv := is_inv_cmp_float c in
-      DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
-      expanse_cbranch_fp false cond_single c lhsv
-  | (Cnotcompfs c), (f1 :: f2 :: nil) =>
-      DO hv1 <~ hsi_sreg_get prev f1;;
-      DO hv2 <~ hsi_sreg_get prev f2;;
-      let is_inv := is_inv_cmp_float c in
-      DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
-      expanse_cbranch_fp true cond_single c lhsv
-  | _, _ =>
-      DO vargs <~ hlist_args prev args;;
-         RET (cond, vargs)
-   end.*)
+ *)
 
 (** ** Execution of one instruction *)
 
-
-(* TODO: This function could be defined in a specific file for each target *)
-Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg) : option (condition * list_hsval) :=
-  None.
-
-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; simpl; intros; try congruence.
-Qed.
-Global Opaque target_cbranch_expanse.
-
 Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg): ?? (condition * list_hsval) :=
-    match  target_cbranch_expanse prev cond args with
+    match target_cbranch_expanse prev cond args with
     | Some (cond', vargs) => 
       DO vargs' <~ fsval_list_proj vargs;;
       RET (cond', vargs)
@@ -1855,7 +952,7 @@ Lemma hsiexec_inst_correct i hst:
    exists st', siexec_inst i st = Some st'
     /\ (forall (REF:hsistate_refines_stat hst st), hsistate_refines_stat hst' st')
     /\ (forall ge sp rs0 m0 (REF:hsistate_refines_dyn ge sp rs0 m0 hst st), hsistate_refines_dyn ge sp rs0 m0 hst' st').
-Proof. Admitted. (*
+Proof.
   destruct i; simpl;
   try (wlp_simplify; try_simplify_someHyps; eexists; intuition eauto; fail).
   - (* refines_dyn Iop *)
@@ -1871,66 +968,19 @@ Proof. Admitted. (*
     eapply hsist_set_local_correct_dyn; eauto.
     unfold sok_local; simpl; intuition.
   - (* refines_stat Icond *)
-    unfold cbranch_expanse; destruct c eqn:EQC;
-    try apply hsiexec_cond_noexp.
-    + repeat (destruct l; try apply hsiexec_cond_noexp).
-      wlp_simplify; try_simplify_someHyps; eexists; intuition eauto.
-      * unfold hsistate_refines_stat, hsiexits_refines_stat in *; simpl; intuition.
-        constructor; simpl; eauto.
-        constructor.
-      * destruct REF as (EXREF & LREF & NEST).
-        split.
-        -- do 2 (constructor; simpl; auto).
-           intros; erewrite seval_condition_refines; eauto.
-           destruct c0; simpl; unfold seval_condition;
-           erewrite H3; eauto; erewrite H2; eauto;
-           erewrite H1; eauto; erewrite H0; eauto;
-           erewrite H; eauto; simplify_SOME z.
-           all: intros; destruct z0, z2; auto.
-        -- split; simpl; auto.
-           destruct NEST as [|st0 se lse TOP NEST];
-           econstructor; simpl; auto; constructor; auto.
-    + admit.
-    + repeat (destruct l; try apply hsiexec_cond_noexp).
-      destruct (Int.eq _ _) eqn:EQIMM; simpl.
-      1: admit.
-      
-      unfold loadimm32; destruct make_immed32 eqn:EQMKI.
-      {
-      wlp_simplify; try_simplify_someHyps; eexists; intuition eauto.
-      * unfold hsistate_refines_stat, hsiexits_refines_stat in *; simpl; intuition.
-        constructor; simpl; eauto.
-        constructor.
-      * destruct REF as (EXREF & LREF & NEST).
-        split.
-        -- do 2 (constructor; simpl; auto).
-           intros; erewrite seval_condition_refines; eauto.
-           destruct c0; simpl; unfold seval_condition.
-
-           { simpl in *. apply mkimm_single_equal in EQMKI; subst.
-             destruct (seval_smem _ _ _ _ _) eqn:EQSM; try congruence.
-             - erewrite H4; eauto; erewrite H3; eauto;
-               erewrite H2; eauto; erewrite H1; eauto;
-               try erewrite H0; eauto; try erewrite H; eauto;
-               simplify_SOME z. rewrite Int.add_zero. trivial.
-             - simplify_SOME x.
-           }
-           2: {
-    generalize (sok_local_set_sreg_simp (Rop (OEaddiwr0 imm))); simpl; eauto.
-    intros.j
-           apply hsilocal_refines_smem_refines in LREF; auto.
-
-           rewrite <- LREF. auto.
-           2: { eauto.
-           all: intros; destruct z0, z2; auto.
-        -- split; simpl; auto.
-           destruct NEST as [|st0 se lse TOP NEST];
-           econstructor; simpl; auto; constructor; auto.
-
-    + admit.
-    + admit.
-                  *)
-(*Qed.*)
+    wlp_simplify; try_simplify_someHyps; eexists; intuition eauto.
+    + unfold hsistate_refines_stat, hsiexits_refines_stat in *; simpl; intuition.
+      constructor; simpl; eauto.
+      constructor.
+    + destruct REF as (EXREF & LREF & NEST).
+      split.
+      * constructor; simpl; auto.
+        constructor; simpl; auto.
+        intros; erewrite seval_condition_refines; eauto.
+      * split; simpl; auto.
+        destruct NEST as [|st0 se lse TOP NEST];
+        econstructor; simpl; auto; constructor; auto.
+Qed.
 Global Opaque hsiexec_inst.
 Local Hint Resolve hsiexec_inst_correct: wlp.