Commit cf935c40 authored by Léo Gourdin's avatar Léo Gourdin
Browse files

[Admitted checker] Some more proof draft

parent adf1bbcd
......@@ -972,6 +972,122 @@ Proof.
- repeat destruct (_ && _); simpl; auto.
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)).
Proof.
intros. eapply f_equal.
destruct v1, v2; simpl; try congruence.
destruct (Int64.cmp _ _); 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 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;;
......@@ -1002,9 +1118,9 @@ Proof.
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.
intros; apply xor_neg_ltle_cmp.
intros; apply cmp_neg_ltgt_cmp.
intros; apply xor_neg_ltge_cmp.
Qed.
Lemma simplify_ccompu_correct: forall c r r0 (hst: hsistate_local),
......@@ -1037,9 +1153,81 @@ Proof.
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.
intros; apply xor_neg_ltle_cmpu.
intros; apply cmp_neg_ltgt_cmpu.
intros; apply xor_neg_ltge_cmpu.
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.
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.
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.
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.
Qed.
Lemma simplify_correct rsv lr hst:
......@@ -1063,8 +1251,8 @@ 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.
......@@ -1202,8 +1390,8 @@ Definition transl_cbranch_int32s (cmp: comparison) (optR0: option bool) :=
Definition transl_cbranch_int32u (cmp: comparison) (optR0: option bool) :=
match cmp with
| Ceq => CEbeqw optR0
| Cne => CEbnew optR0
| Ceq => CEbequw optR0
| Cne => CEbneuw optR0
| Clt => CEbltuw optR0
| Cle => CEbgeuw optR0
| Cgt => CEbltuw optR0
......@@ -1222,8 +1410,8 @@ Definition transl_cbranch_int64s (cmp: comparison) (optR0: option bool) :=
Definition transl_cbranch_int64u (cmp: comparison) (optR0: option bool) :=
match cmp with
| Ceq => CEbeql optR0
| Cne => CEbnel optR0
| Ceq => CEbequl optR0
| Cne => CEbneul optR0
| Clt => CEbltul optR0
| Cle => CEbgeul optR0
| Cgt => CEbltul optR0
......@@ -1319,14 +1507,60 @@ Qed.
Local Hint Resolve hsist_set_local_correct_stat: core.
Lemma hsiexec_cond_noexp (hst: hsistate): forall l c0 n n0,
WHEN DO res <~
(DO vargs <~ hlist_args (hsi_local hst) l;; RET ((c0, vargs)));;
(let (cond, vargs) := res in
RET (Some
{|
hsi_pc := n0;
hsi_exits := {|
hsi_cond := cond;
hsi_scondargs := vargs;
hsi_elocal := hsi_local hst;
hsi_ifso := n |} :: hsi_exits hst;
hsi_local := hsi_local hst |})) ~> o0
THEN (forall (hst' : hsistate) (st : sistate),
o0 = Some hst' ->
exists st' : sistate,
Some
{|
si_pc := n0;
si_exits := {|
si_cond := c0;
si_scondargs := list_sval_inj
(map (si_sreg (si_local st)) l);
si_elocal := si_local st;
si_ifso := n |} :: si_exits st;
si_local := si_local st |} = Some st' /\
(hsistate_refines_stat hst st -> hsistate_refines_stat hst' st') /\
(forall (ge : RTL.genv) (sp : val) (rs0 : regset) (m0 : mem),
hsistate_refines_dyn ge sp rs0 m0 hst st ->
hsistate_refines_dyn ge sp rs0 m0 hst' st')).
Proof.
intros.
wlp_simplify; try_simplify_someHyps; eexists; intuition eauto.
- unfold hsistate_refines_stat, hsiexits_refines_stat in *; simpl; intuition.
constructor; simpl; eauto.
constructor.
- destruct H0 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.
Lemma hsiexec_inst_correct i hst:
WHEN hsiexec_inst i hst ~> o THEN forall hst' st,
o = Some 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.
(* TODO destruct i; simpl;
Proof.
destruct i; simpl;
try (wlp_simplify; try_simplify_someHyps; eexists; intuition eauto; fail).
- (* refines_dyn Iop *)
wlp_simplify; try_simplify_someHyps; eexists; intuition eauto.
......@@ -1341,89 +1575,30 @@ Proof. Admitted.
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.
Qed.*)
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.
+ admit.
+ admit.
Admitted.
(*Qed.*)
Global Opaque hsiexec_inst.
Local Hint Resolve hsiexec_inst_correct: wlp.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment