Proof of fsval condition cmp ok

1 files changed, 18 insertions, 968 deletions

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.