[Admitted checker] Duplicating Asm Ceq/Cne and draft checker proof

1 files changed, 320 insertions, 55 deletions

diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v
index 509697de..7a90fd3a 100644
--- a/scheduling/RTLpathSE_impl.v
+++ b/scheduling/RTLpathSE_impl.v
@@ -687,7 +687,7 @@ Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool)
   | Ceq => hSop (OEseqw optR0) lhsv
   | Cne => hSop (OEsnew optR0) lhsv
   | Clt | Cgt => hSop (OEsltw optR0) lhsv
-  | Cle | Cge=>
+  | Cle | Cge =>
       DO hvs <~ (hSop (OEsltw optR0) lhsv);;
       DO hl <~ make_lhsv_single hvs;;
       hSop (OExoriw Int.one) hl
@@ -695,10 +695,10 @@ Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool)
 
 Definition cond_int32u (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
   match cmp with
-  | Ceq => hSop (OEseqw optR0) lhsv
-  | Cne => hSop (OEsnew optR0) lhsv
+  | Ceq => hSop (OEsequw optR0) lhsv
+  | Cne => hSop (OEsneuw optR0) lhsv
   | Clt | Cgt => hSop (OEsltuw optR0) lhsv
-  | Cle | Cge=>
+  | Cle | Cge =>
       DO hvs <~ (hSop (OEsltuw optR0) lhsv);;
       DO hl <~ make_lhsv_single hvs;;
       hSop (OExoriw Int.one) hl
@@ -717,8 +717,8 @@ Definition cond_int64s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool)
 
 Definition cond_int64u (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
   match cmp with
-  | Ceq => hSop (OEseql optR0) lhsv
-  | Cne => hSop (OEsnel optR0) lhsv
+  | Ceq => hSop (OEsequl optR0) lhsv
+  | Cne => hSop (OEsneul optR0) lhsv
   | Clt | Cgt => hSop (OEsltul optR0) lhsv
   | Cle | Cge =>
       DO hvs <~ (hSop (OEsltul optR0) lhsv);;
@@ -778,78 +778,270 @@ Definition expanse_condimm_int64s (cmp: comparison) (hv1: hsval) (n: int64) :=
 (** simplify a symbolic value before assignment to a register *)
 Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hsval :=
   match rsv with
-  | Rop op =>
-     (*match is_move_operation op lr with*)
-     (*| Some arg => hsi_sreg_get hst arg [>* optimization of Omove <]*)
-     (*| None =>*)
-       (*DO lhsv <~ hlist_args hst lr;;*)
-       (*hSop op lhsv*)
-     (*end;;*)
-    match op, lr with
-    | Ocmp (Ccomp c), a1 :: a2 :: nil =>
+  | Rop (Omove as op) =>
+     match is_move_operation op lr with
+     | Some arg => hsi_sreg_get hst arg (* optimization of Omove *)
+     | None =>
+       DO lhsv <~ hlist_args hst lr;;
+       hSop op lhsv
+     end
+  | Rop ((Ocmp cond) as op) =>
+    match cond, lr with
+    | (Ccomp c), a1 :: a2 :: nil =>
         DO hv1 <~ hsi_sreg_get hst a1;;
         DO hv2 <~ hsi_sreg_get hst a2;;
         let is_inv := is_inv_cmp_int c in
         let optR0 := make_optR0 false is_inv in
         DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
         cond_int32s c lhsv optR0
-    | Ocmp (Ccompu c), a1 :: a2 :: nil =>
+    | (Ccompu c), a1 :: a2 :: nil =>
         DO hv1 <~ hsi_sreg_get hst a1;;
         DO hv2 <~ hsi_sreg_get hst a2;;
         let is_inv := is_inv_cmp_int c in
         let optR0 := make_optR0 false is_inv in
         DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
         cond_int32u c lhsv optR0
-    | Ocmp (Ccompl c), a1 :: a2 :: nil =>
+    | (Ccompl c), a1 :: a2 :: nil =>
         DO hv1 <~ hsi_sreg_get hst a1;;
         DO hv2 <~ hsi_sreg_get hst a2;;
         let is_inv := is_inv_cmp_int c in
         let optR0 := make_optR0 false is_inv in
         DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
         cond_int64s c lhsv optR0
-    | Ocmp (Ccomplu c), a1 :: a2 :: nil =>
+    | (Ccomplu c), a1 :: a2 :: nil =>
         DO hv1 <~ hsi_sreg_get hst a1;;
         DO hv2 <~ hsi_sreg_get hst a2;;
         let is_inv := is_inv_cmp_int c in
         let optR0 := make_optR0 false is_inv in
         DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
         cond_int64u c lhsv optR0
-    | Ocmp (Ccompf c), f1 :: f2 :: nil =>
+    | (Ccompf c), f1 :: f2 :: nil =>
         DO hv1 <~ hsi_sreg_get hst f1;;
         DO hv2 <~ hsi_sreg_get hst f2;;
         let is_inv := is_inv_cmp_float c in
         DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
         expanse_cond_fp false cond_float c lhsv
-    | Ocmp (Cnotcompf c), f1 :: f2 :: nil =>
+    | (Cnotcompf c), f1 :: f2 :: nil =>
         DO hv1 <~ hsi_sreg_get hst f1;;
         DO hv2 <~ hsi_sreg_get hst f2;;
         let is_inv := is_inv_cmp_float c in
         DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
         expanse_cond_fp true cond_float c lhsv
-    | Ocmp (Ccompfs c), f1 :: f2 :: nil =>
+    | (Ccompfs c), f1 :: f2 :: nil =>
         DO hv1 <~ hsi_sreg_get hst f1;;
         DO hv2 <~ hsi_sreg_get hst f2;;
         let is_inv := is_inv_cmp_float c in
         DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
         expanse_cond_fp false cond_single c lhsv
-    | Ocmp (Cnotcompfs c), f1 :: f2 :: nil =>
+    | (Cnotcompfs c), f1 :: f2 :: nil =>
         DO hv1 <~ hsi_sreg_get hst f1;;
         DO hv2 <~ hsi_sreg_get hst f2;;
         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
-        (*| Ocmp (Ccomplimm c imm), a1 :: nil =>
+        (*| (Ccomplimm c imm), a1 :: nil =>
         DO hv1 <~ hsi_sreg_get hst a1;;
            expanse_condimm_int64s c hv1 imm*)
     | _, _ =>
         DO lhsv <~ hlist_args hst lr;;
         hSop op lhsv
     end
+  | Rop op =>
+       DO lhsv <~ hlist_args hst lr;;
+       hSop op lhsv
   | Rload _ chunk addr => 
        DO lhsv <~ hlist_args hst lr;;
        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_neg_ltle_cmp: forall v1 v2,
+  Some (Val.xor (Val.cmp Clt v1 v2) (Vint Int.one)) =
+  Some (Val.of_optbool (Val.cmp_bool Cle v2 v1)).
+Proof.
+  intros. eapply f_equal.
+  destruct v1, v2; simpl; try congruence.
+  unfold Val.cmp; simpl;
+  try rewrite Int.eq_sym;
+  try destruct (Int.eq _ _); try destruct (Int.lt _ _) eqn:ELT ; simpl;
+  try rewrite Int.xor_one_one; try rewrite Int.xor_zero_one;
+  auto.
+Qed.
+
+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.
+
+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.
+
+Lemma xor_neg_ltle_cmpu: forall mptr v1 v2,
+  Some (Val.xor (Val.cmpu (Mem.valid_pointer mptr) Clt v1 v2) (Vint Int.one)) =
+  Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer mptr) Cle v2 v1)).
+Proof.
+  intros. eapply f_equal.
+  destruct v1, v2; simpl; try congruence.
+  unfold Val.cmpu; simpl;
+  try rewrite Int.eq_sym;
+  try destruct (Int.eq _ _); try destruct (Int.ltu _ _) eqn:ELT ; simpl;
+  try rewrite Int.xor_one_one; try rewrite Int.xor_zero_one;
+  auto.
+  1,2:
+    unfold Val.cmpu, Val.cmpu_bool;
+    destruct Archi.ptr64; try destruct (_ && _); try destruct (_ || _);
+    try destruct (eq_block _ _); auto.
+  unfold Val.cmpu, Val.cmpu_bool; simpl;
+  destruct Archi.ptr64; try destruct (_ || _); simpl; auto;
+  destruct (eq_block b b0); destruct (eq_block b0 b);
+  try congruence;
+  try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _);
+  simpl; auto;
+  repeat destruct (_ && _); simpl; auto.
+Qed.
+
+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.
+
+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 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.
+    simplify_SOME z; intros; apply xor_neg_ltle_cmp.
+    simplify_SOME z; intros; apply cmp_neg_ltgt_cmp.
+    simplify_SOME z; intros; apply xor_neg_ltge_cmp.
+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.
+    simplify_SOME z; intros; apply xor_neg_ltle_cmpu.
+    simplify_SOME z; intros; apply cmp_neg_ltgt_cmpu.
+    simplify_SOME z; intros; apply xor_neg_ltge_cmpu.
+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)
@@ -857,26 +1049,26 @@ Lemma simplify_correct rsv lr hst:
     (OK1: seval_sval ge sp (rsv lr st) rs0 m0 <> None),
     sval_refines ge sp rs0 m0 hv (rsv lr st).
 Proof.
-  (*  destruct rsv; simpl; auto.
-  - destruct op; wlp_simplify.
-    try (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). (* absurd case *)
-
-    erewrite H0; eauto. simplify_SOME args.
-    intros. congruence. eauto.
-
-    destruct (is_move_operation _ _) eqn: Hmove; wlp_simplify.
-    + exploit is_move_operation_correct; eauto.
-      intros (Hop & Hlsv); subst; simpl in *.
-      simplify_SOME z.
-      * erewrite H; eauto.
-      * try_simplify_someHyps; congruence.
-      * congruence.
-    + clear Hmove.
-      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. (* absurd case *)
+  destruct rsv; simpl; auto.
+  - destruct op eqn:EQOP; try apply simplify_nothing.
+    { destruct (is_move_operation _ _) eqn: Hmove.
+      + wlp_simplify.
+        exploit is_move_operation_correct; eauto.
+        intros (Hop & Hlsv); subst; simpl in *.
+        simplify_SOME z.
+        * erewrite H; eauto.
+        * try_simplify_someHyps; congruence.
+        * congruence.
+      + apply simplify_nothing. }
+    { destruct cond; repeat (destruct lr; try apply simplify_nothing).
+      + apply simplify_ccomp_correct.
+      + apply simplify_ccompu_correct.
+      + admit.
+      + admit.
+      + admit.
+      + admit.
+      + admit.
+      + admit. }
   - (* Rload *)
     destruct trap; wlp_simplify.
     erewrite H0; eauto.
@@ -886,7 +1078,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.*) Admitted.
 Global Opaque simplify.
 Local Hint Resolve simplify_correct: wlp.
 
@@ -1038,30 +1230,30 @@ Definition transl_cbranch_int64u (cmp: comparison) (optR0: option bool) :=
   | Cge => CEbgeul optR0
   end.
 
-Definition cbranch_expanse (prev: hsistate_local) (i: instruction) : ?? (condition * list_hsval) :=
-  match i with
-  | Icond (Ccomp c) (a1 :: a2 :: nil) _ _ _ =>
+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)
-  | Icond (Ccompu c) (a1 :: a2 :: nil) _ _ _ =>
+  | (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)
-  | Icond (Ccompl c) (a1 :: a2 :: nil) _ _ _ =>
+  | (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)
-  | Icond (Ccomplu c) (a1 :: a2 :: nil) _ _ _ =>
+  | (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;;
@@ -1071,10 +1263,9 @@ Definition cbranch_expanse (prev: hsistate_local) (i: instruction) : ?? (conditi
       (*  | Icond (Ccompimm c n) (a1 :: nil) _ _ _ =>
       let cond := transl_cbranch_int32s c (make_optR0 c) in
          RET (cond, a1 :: a1 :: nil)*)
-  | Icond cond args _ _ _ =>
+  | _, _ =>
       DO vargs <~ hlist_args prev args;;
          RET (cond, vargs)
-  | _ => FAILWITH "cbranch_expanse: not an Icond"
   end.
 
 (** ** Execution of one instruction *)
@@ -1094,7 +1285,7 @@ Definition hsiexec_inst (i: instruction) (hst: hsistate): ?? (option hsistate) :
       RET (Some (hsist_set_local hst pc' next))
   | Icond cond args ifso ifnot _ =>
       let prev := hst.(hsi_local) in
-      DO res <~ cbranch_expanse prev i;;
+      DO res <~ cbranch_expanse prev cond args;;
       let (cond, vargs) := res in
       let ex := {| hsi_cond:=cond; hsi_scondargs:=vargs; hsi_elocal := prev; hsi_ifso := ifso |} in
       RET (Some {| hsi_pc := ifnot; hsi_exits := ex::hst.(hsi_exits); hsi_local := prev |})
@@ -1134,27 +1325,101 @@ 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. (*
-  destruct i; simpl; wlp_simplify; try_simplify_someHyps; eexists; intuition eauto.
+Proof. Admitted.
+  (* TODO destruct i; simpl;
+  try (wlp_simplify; try_simplify_someHyps; eexists; intuition eauto; fail).
   - (* refines_dyn Iop *)
+    wlp_simplify; try_simplify_someHyps; eexists; intuition eauto.
     eapply hsist_set_local_correct_dyn; eauto.
     generalize (sok_local_set_sreg_simp (Rop o)); simpl; eauto.
   - (* refines_dyn Iload *)
+    wlp_simplify; try_simplify_someHyps; eexists; intuition eauto.
     eapply hsist_set_local_correct_dyn; eauto.
     generalize (sok_local_set_sreg_simp (Rload t0 m a)); simpl; eauto.
   - (* refines_dyn Istore *)
+    wlp_simplify; try_simplify_someHyps; eexists; intuition eauto.
     eapply hsist_set_local_correct_dyn; eauto.
     unfold sok_local; simpl; intuition.
   - (* refines_stat Icond *)
+    unfold cbranch_expanse; destruct c eqn:EQC; simpl in *.
+    destruct l.
+    2: {
+      destruct l.
+      2: {
+        destruct l.
+        { 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).
+    (*eapply hsist_set_local_correct_dyn; eauto.*)
+    split.
+    + constructor; simpl; auto.
+      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 args.
+      {
+      intros. destruct args0, args2; auto;
+      unfold Val.cmpu_bool, Val.cmp_bool;
+      destruct Archi.ptr64; auto. simpl.
+      destruct (_ && _).
+      try destruct (Int.eq _ _); auto.
+      try destruct (Mem.valid_pointer _ _ _ || Mem.valid_pointer _ _ _);
+      simpl. congruence.
+
+
+
+
+
+
+      destruct args, args1; try congruence; auto.
+      destruct args1; try congruence; auto.
+      destruct args1; try congruence; auto.
+      destruct v1.
+      unfold Val.cmpu_bool, Val.cmp_bool.
+      erewrite H3.
+
+      destruct c eqn:EQC; simpl; eauto.
+      8: { destruct (hlist_args (hsi_local hst) l) in Hexta.
+        destruct  in Hexta.
+
+
+      destruct exta; simpl in *.
+      destruct Hexta.
+    + split; simpl; auto.
+      destruct NEST as [|st0 se lse TOP NEST];
+      econstructor; simpl; auto; constructor; auto.
+
+    
+    wlp_simplify; try_simplify_someHyps; eexists; intuition eauto;
+    
     unfold hsistate_refines_stat, hsiexits_refines_stat in *; simpl; intuition.
     constructor; simpl; eauto.
     constructor.
   - (* refines_dyn Icond *)
     destruct REF as (EXREF & LREF & NEST).
+    destruct exta. simpl.
     split.
     + constructor; simpl; auto.
       constructor; simpl; auto.
       intros; erewrite seval_condition_refines; eauto.
+
+      destruct c eqn:EQC; simpl; eauto.
+      8: { destruct (hlist_args (hsi_local hst) l) in Hexta.
+        destruct  in Hexta.
+
+
+      destruct exta; simpl in *.
+      destruct Hexta.
     + split; simpl; auto.
       destruct NEST as [|st0 se lse TOP NEST];
       econstructor; simpl; auto; constructor; auto.