Proof of Ocmp expansions without immediate and some drafts in comment

3 files changed, 477 insertions, 52 deletions

diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index 0b1abe2a..35c5b9d6 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -377,7 +377,7 @@ Proof.
   rewrite <- Float32.cmp_swap. auto.
    Qed.
 
-(* TODO UNUSUED ? Remark branch_on_X31:
+(* TODO gourdinl UNUSUED ? Remark branch_on_X31:
   forall normal lbl (rs: regset) m b,
   rs#X31 = Val.of_bool (eqb normal b) -> 
   exec_instr ge fn (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) rs m =
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index 1e40b492..32c8731f 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -327,7 +327,7 @@ let expanse_cbranch_fp cnot fn_cond cmp f1 f2 info succ1 succ2 k =
   insn
   :: (if normal' then
       Icond (CEbnew (Some false), [ r2p (); r2p () ], succ1, succ2, info)
-     else Icond (CEbeqw (Some false), [ r2p (); r2p () ], succ1, succ2, info)) (* TODO Maybe incorrect *)
+     else Icond (CEbeqw (Some false), [ r2p (); r2p () ], succ1, succ2, info)) (* TODO gourdinl Maybe incorrect *)
   :: k
 
 let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ]
@@ -392,14 +392,14 @@ let expanse (sb : superblock) code pm =
           debug "Iop/Ccompu\n";
           exp := cond_int32u false c a1 a2 dest succ [];
           was_exp := true
-      (*| Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) ->
+      | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) ->
           debug "Iop/Ccompimm\n";
           exp := expanse_condimm_int32s c a1 imm dest succ [];
           was_exp := true
       | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) ->
           debug "Iop/Ccompuimm\n";
           exp := expanse_condimm_int32u c a1 imm dest succ [];
-          was_exp := true*)
+          was_exp := true
       | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) ->
           debug "Iop/Ccompl\n";
           exp := cond_int64s false c a1 a2 dest succ [];
@@ -408,14 +408,14 @@ let expanse (sb : superblock) code pm =
           debug "Iop/Ccomplu\n";
           exp := cond_int64u false c a1 a2 dest succ [];
           was_exp := true
-      (*| Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) ->
+      | Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) ->
           debug "Iop/Ccomplimm\n";
           exp := expanse_condimm_int64s c a1 imm dest succ [];
           was_exp := true
       | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) ->
           debug "Iop/Ccompluimm\n";
           exp := expanse_condimm_int64u c a1 imm dest succ [];
-          was_exp := true*)
+          was_exp := true
       | Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, succ) ->
           debug "Iop/Ccompf\n";
           exp := expanse_cond_fp false cond_float c f1 f2 dest succ [];
diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v
index ada0d308..b7b58ae5 100644
--- a/scheduling/RTLpathSE_impl.v
+++ b/scheduling/RTLpathSE_impl.v
@@ -597,7 +597,7 @@ Proof.
     explore; try congruence.
 Qed.
 
-(* TODO MOVE EXPANSIONS BELOW ELSEWHERE *)
+(* TODO gourdinl MOVE EXPANSIONS BELOW ELSEWHERE *)
 
 Definition is_inv_cmp_int (cmp: comparison) : bool :=
   match cmp with | Cle | Cgt => true | _ => false end.
@@ -608,7 +608,7 @@ Definition is_inv_cmp_float (cmp: comparison) : bool :=
 Definition make_optR0 (is_x0 is_inv: bool) : option bool :=
   if is_x0 then Some is_inv else None.
 
-(* TODO IF NEEDED LATER Fixpoint hlist_sval (l: list hsval): ?? list_hsval :=
+(* TODO gourdinl IF NEEDED LATER Fixpoint hlist_sval (l: list hsval): ?? list_hsval :=
   match l with
   | nil => hSnil()
   | r::l =>
@@ -663,6 +663,17 @@ Definition loadimm64 (n: int64) :=
   | Imm64_large imm => hSop (OEloadli imm) hnil
   end.
 
+Definition opimm32 (hv1: hsval) (n: int) (op: operation) (opimm: int -> operation) :=
+  match make_immed32 n with
+  | Imm32_single imm =>
+      DO hl <~ make_lhsv_single hv1;;
+      hSop (opimm imm) hl
+  | Imm32_pair hi lo =>
+      DO hvs <~ load_hilo32 hi lo;;
+      DO hl <~ make_lhsv_cmp false hv1 hvs;;
+      hSop op hl
+  end.
+
 Definition opimm64 (hv1: hsval) (n: int64) (op: operation) (opimm: int64 -> operation) :=
   match make_immed64 n with
   | Imm64_single imm =>
@@ -679,8 +690,12 @@ Definition opimm64 (hv1: hsval) (n: int64) (op: operation) (opimm: int64 -> oper
       hSop op hl
   end.
 
+Definition xorimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oxor OExoriw.
+Definition sltimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltw None) OEsltiw.
+Definition sltuimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltuw None) OEsltiuw.
 Definition xorimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oxorl OExoril.
 Definition sltimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltl None) OEsltil.
+Definition sltuimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltul None) OEsltiul.
 
 Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
   match cmp with
@@ -750,6 +765,47 @@ Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) :=
   DO hl <~ make_lhsv_single hvs;;
   if normal' then RET hvs else hSop (OExoriw Int.one) hl.
 
+Definition expanse_condimm_int32s (cmp: comparison) (hv1: hsval) (n: int) :=
+  let is_inv := is_inv_cmp_int cmp in
+  if Int.eq n Int.zero then
+    let optR0 := make_optR0 true is_inv in
+    DO hl <~ make_lhsv_cmp is_inv hv1 hv1;;
+    cond_int32s cmp hl optR0
+  else
+    match cmp with
+    | Ceq | Cne =>
+        let optR0 := make_optR0 true is_inv in
+        DO hvs <~ xorimm32 hv1 n;;
+        DO hl <~ make_lhsv_cmp false hvs hvs;;
+        cond_int32s cmp hl optR0
+    | Clt => sltimm32 hv1 n
+    | Cle =>
+        if Int.eq n (Int.repr Int.max_signed) then
+          loadimm32 Int.one
+        else sltimm32 hv1 (Int.add n Int.one)
+    | _ =>
+        let optR0 := make_optR0 false is_inv in
+        DO hvs <~ loadimm32 n;;
+        DO hl <~ make_lhsv_cmp is_inv hv1 hvs;;
+        cond_int32s cmp hl optR0
+    end.
+
+Definition expanse_condimm_int32u (cmp: comparison) (hv1: hsval) (n: int) :=
+  let is_inv := is_inv_cmp_int cmp in
+  if Int.eq n Int.zero then
+    let optR0 := make_optR0 true is_inv in
+    DO hl <~ make_lhsv_cmp is_inv hv1 hv1;;
+    cond_int32u cmp hl optR0
+  else
+    match cmp with
+    | Clt => sltuimm32 hv1 n
+    | _ =>
+        let optR0 := make_optR0 false is_inv in
+        DO hvs <~ loadimm32 n;;
+        DO hl <~ make_lhsv_cmp is_inv hv1 hvs;;
+        cond_int32u cmp hl optR0
+    end.
+
 Definition expanse_condimm_int64s (cmp: comparison) (hv1: hsval) (n: int64) :=
   let is_inv := is_inv_cmp_int cmp in
   if Int64.eq n Int64.zero then
@@ -775,6 +831,22 @@ Definition expanse_condimm_int64s (cmp: comparison) (hv1: hsval) (n: int64) :=
         cond_int64s cmp hl optR0
     end.
 
+Definition expanse_condimm_int64u (cmp: comparison) (hv1: hsval) (n: int64) :=
+  let is_inv := is_inv_cmp_int cmp in
+  if Int64.eq n Int64.zero then
+    let optR0 := make_optR0 true is_inv in
+    DO hl <~ make_lhsv_cmp is_inv hv1 hv1;;
+    cond_int64u cmp hl optR0
+  else
+    match cmp with
+    | Clt => sltuimm64 hv1 n
+    | _ =>
+        let optR0 := make_optR0 false is_inv in
+        DO hvs <~ loadimm64 n;;
+        DO hl <~ make_lhsv_cmp is_inv hv1 hvs;;
+        cond_int64u cmp hl optR0
+    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
@@ -801,6 +873,12 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hs
         let optR0 := make_optR0 false is_inv in
         DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
         cond_int32u c lhsv optR0
+    | (Ccompimm c imm), a1 :: nil =>
+        DO hv1 <~ hsi_sreg_get hst a1;;
+        expanse_condimm_int32s c hv1 imm
+    | (Ccompuimm c imm), a1 :: nil =>
+        DO hv1 <~ hsi_sreg_get hst a1;;
+        expanse_condimm_int32u c hv1 imm
     | (Ccompl c), a1 :: a2 :: nil =>
         DO hv1 <~ hsi_sreg_get hst a1;;
         DO hv2 <~ hsi_sreg_get hst a2;;
@@ -839,9 +917,12 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hs
         let is_inv := is_inv_cmp_float c in
         DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
         expanse_cond_fp true cond_single c lhsv
-        (*| (Ccomplimm c imm), a1 :: nil =>
+    | (Ccomplimm c imm), a1 :: nil =>
+        DO hv1 <~ hsi_sreg_get hst a1;;
+        expanse_condimm_int64s c hv1 imm
+    | (Ccompluimm c imm), a1 :: nil =>
         DO hv1 <~ hsi_sreg_get hst a1;;
-           expanse_condimm_int64s c hv1 imm*)
+        expanse_condimm_int64u c hv1 imm
     | _, _ =>
         DO lhsv <~ hlist_args hst lr;;
         hSop op lhsv
@@ -889,7 +970,16 @@ Proof.
   auto.
 Qed.
 
-Lemma xor_neg_ltge_cmp: forall v1 v2,
+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.
+
+(* 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.
@@ -900,15 +990,15 @@ Proof.
   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.
+   Qed.*)
 
-Lemma cmp_neg_ltgt_cmp: forall v1 v2,
+(* 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.
+   Qed.*)
 
 Lemma xor_neg_ltle_cmpu: forall mptr v1 v2,
   Some (Val.xor (Val.cmpu (Mem.valid_pointer mptr) Clt v1 v2) (Vint Int.one)) =
@@ -934,7 +1024,7 @@ Proof.
   repeat destruct (_ && _); simpl; auto.
 Qed.
 
-Lemma xor_neg_ltge_cmpu: forall mptr v1 v2,
+(* 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.
@@ -956,9 +1046,9 @@ Proof.
   try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _);
   simpl; auto;
   repeat destruct (_ && _); simpl; auto.
-Qed.
+   Qed.*)
 
-Lemma cmp_neg_ltgt_cmpu: forall mptr v1 v2,
+(* 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.
@@ -970,15 +1060,14 @@ Proof.
   try congruence.
   - repeat destruct (_ || _); simpl; auto.
   - repeat destruct (_ && _); simpl; auto.
-Qed.
+   Qed.*)
 
-Lemma cmpl_optbool_mktotal: forall cmp v1 v2,
-  Some (Val.maketotal (Val.cmpl cmp v1 v2)) =
-  Some (Val.of_optbool (Val.cmpl_bool cmp v1 v2)).
+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 v1, v2; simpl; try congruence.
-  destruct (Int64.cmp _ _); auto.
+  destruct v; simpl; auto.
 Qed.
 
 Lemma cmplu_optbool_mktotal: forall mptr cmp v1 v2,
@@ -1088,6 +1177,50 @@ Proof.
   repeat destruct (_ && _); simpl; auto.
 Qed.
 
+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.
+
+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.
+
 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;;
@@ -1117,10 +1250,13 @@ Proof.
     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.
-    intros; apply xor_neg_ltle_cmp.
-    intros; apply cmp_neg_ltgt_cmp.
-    intros; apply xor_neg_ltge_cmp.
+    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),
@@ -1152,12 +1288,119 @@ Proof.
     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.
-    intros; apply xor_neg_ltle_cmpu.
-    intros; apply cmp_neg_ltgt_cmpu.
-    intros; apply xor_neg_ltge_cmpu.
+    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.
 
+(* 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.
+ *)
+
+(* TODO gourdinl Lemma simplify_ccompuimm_correct: forall c n r (hst: hsistate_local),
+  WHEN DO hv1 <~ hsi_sreg_get hst r;; expanse_condimm_int32u 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 (Ccompuimm 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 (Ccompuimm c n)) args m)).
+Proof.
+  unfold expanse_condimm_int32u, cond_int32u in *; destruct c;
+  intros; destruct (Int.eq n Int.zero) eqn:EQIMM; simpl.
+  - wlp_simplify;
+    destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
+    all: 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.
+    apply Int.same_if_eq in EQIMM; subst. trivial.
+  - unfold loadimm32. destruct (make_immed32 n) eqn:EQMKI;
+    wlp_simplify;
+    destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
+    all: 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.
+    + apply mkimm_single_equal in EQMKI; subst.
+      rewrite Int.add_commut, Int.add_zero_l. trivial.
+    + 
+
+  2: { intros. destruct (Int.eq n Int.zero) eqn:EQIMM; simpl.
+       2: { unfold loadimm32. destruct (make_immed32 n) eqn:EQMKI.
+            2: { 
+                wlp_simplify;
+                destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
+                all: 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.
+    2: {
+    apply mkimm_single_equal in EQMKI; subst.
+    rewrite Int.add_commut, Int.add_zero_l. trivial.
+
+
+  2: {
+    wlp_simplify;
+    destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
+  all: try (simplify_SOME z; contradiction; fail).
+
+  2: {
+
+  all:
+    try (erewrite H7; eauto; erewrite H6; eauto; 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.
+  all:
+    try apply Int.same_if_eq in H0; subst; trivial.
+
+  erewrite H0.
+
+
+    - 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 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;;
@@ -1187,11 +1430,13 @@ Proof.
     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.
-    1,2,3: intros; apply cmpl_optbool_mktotal.
-    intros; apply xor_neg_ltle_cmpl.
-    intros; apply cmp_neg_ltgt_cmpl.
-    intros; apply xor_neg_ltge_cmpl.
+    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),
@@ -1223,11 +1468,186 @@ Proof.
     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.
-    1,2,3: intros; apply cmplu_optbool_mktotal.
-    intros; apply xor_neg_ltle_cmplu.
-    intros; apply cmp_neg_ltgt_cmplu.
-    intros; apply xor_neg_ltge_cmplu.
+    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.
+
+(* TODO gourdinl move to common/Values ? *)
+Theorem swap_cmpf_bool:
+  forall c x y,
+  Val.cmpf_bool (swap_comparison c) x y = Val.cmpf_bool c y x.
+Proof.
+  destruct x; destruct y; simpl; auto. rewrite Float.cmp_swap. auto.
+Qed.
+
+Theorem swap_cmpfs_bool:
+  forall c x y,
+  Val.cmpfs_bool (swap_comparison c) x y = Val.cmpfs_bool c y x.
+Proof.
+  destruct x; destruct y; simpl; auto. rewrite Float32.cmp_swap. auto.
+Qed.
+
+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:
@@ -1251,12 +1671,16 @@ Proof.
     { destruct cond; repeat (destruct lr; try apply simplify_nothing).
       + apply simplify_ccomp_correct.
       + apply simplify_ccompu_correct.
+      + admit.
+      + admit.
       + apply simplify_ccompl_correct.
       + apply simplify_ccomplu_correct.
       + admit.
       + admit.
-      + admit.
-      + admit. }
+      + apply simplify_ccompf_correct.
+      + apply simplify_cnotcompf_correct.
+      + apply simplify_ccompfs_correct.
+      + apply simplify_cnotcompfs_correct. }
   - (* Rload *)
     destruct trap; wlp_simplify.
     erewrite H0; eauto.
@@ -1266,7 +1690,8 @@ 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.*)
+Admitted.
 Global Opaque simplify.
 Local Hint Resolve simplify_correct: wlp.
 
@@ -1334,7 +1759,7 @@ Lemma hslocal_set_sreg_correct hst r rsv lr:
   WHEN hslocal_set_sreg hst r rsv lr ~> hst' THEN forall ge sp rs0 m0 st
     (REF: hsilocal_refines ge sp rs0 m0 hst st),
     hsilocal_refines ge sp rs0 m0 hst' (slocal_set_sreg st r (rsv lr st)).
-Proof. (* TODO
+Proof.
   wlp_simplify.
   + (* may_trap ~> true *)
     assert (X: sok_local ge sp rs0 m0 (slocal_set_sreg st r (rsv lr st)) <->
@@ -1366,13 +1791,13 @@ Proof. (* TODO
     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.*) Admitted.
+Qed.
 Global Opaque hslocal_set_sreg.
 Local Hint Resolve hslocal_set_sreg_correct: wlp.
 
-(* TODO MOVE ELSEWHERE Branch expansion *)
+(* TODO gourdinl MOVE ELSEWHERE Branch expansion *)
 
-(* XXX NOT SURE IF THIS DEF IS NEEDED
+(* TODO gourdinl NOT SURE IF THIS DEF IS NEEDED
  * SHOULD WE TAKE THE PREV STATE INTO ACCOUNT HERE?
 Definition make_lr_prev_cmp (is_inv: bool) (a1 a2: reg) (prev: hsistate_local) : ?? list_hsval :=
   if is_inv then
@@ -1971,8 +2396,8 @@ Hint Resolve revmap_check_single_correct: wlp.
 Global Opaque revmap_check_single.
 
 Definition hsiexit_simu_check (dm: PTree.t node) (f: RTLpath.function) (hse1 hse2: hsistate_exit): ?? unit :=
-  (* TODO struct_check (hsi_cond hse1) (hsi_cond hse2) "hsiexit_simu_check: conditions do not match";;*)
-  (*phys_check (hsi_scondargs hse1) (hsi_scondargs hse2) "hsiexit_simu_check: args do not match";;*)
+  struct_check (hsi_cond hse1) (hsi_cond hse2) "hsiexit_simu_check: conditions do not match";;
+  phys_check (hsi_scondargs hse1) (hsi_scondargs hse2) "hsiexit_simu_check: args do not match";;
   revmap_check_single dm (hsi_ifso hse1) (hsi_ifso hse2);;
   DO path <~ some_or_fail ((fn_path f) ! (hsi_ifso hse1)) "hsiexit_simu_check: internal error";;
   hsilocal_frame_simu_check (Regset.elements path.(input_regs)) (hsi_elocal hse1) (hsi_elocal hse2).
@@ -1981,8 +2406,8 @@ Lemma hsiexit_simu_check_correct dm f hse1 hse2:
   WHEN hsiexit_simu_check dm f hse1 hse2 ~> _ THEN
   hsiexit_simu_spec dm f hse1 hse2.
 Proof.
-  unfold hsiexit_simu_spec; wlp_simplify. Admitted.
-(*Qed.*)
+  unfold hsiexit_simu_spec; wlp_simplify.
+Qed.
 Hint Resolve hsiexit_simu_check_correct: wlp.
 Global Opaque hsiexit_simu_check.