From adf1bbcd5c356a0cb75c412357a3b7af23795f47 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 11 Feb 2021 20:03:49 +0100 Subject: [Admitted checker] Duplicating Asm Ceq/Cne and draft checker proof --- scheduling/RTLpathSE_impl.v | 375 +++++++++++++++++++++++++++++++++++++------- 1 file changed, 320 insertions(+), 55 deletions(-) (limited to 'scheduling') 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. -- cgit