Commit 006364e6 authored by Léon Gondelman's avatar Léon Gondelman
Browse files

wip on vcg_wp: add well-foundness lemmas of dcexpr w.r.t. known_locations

parent b79b3eb0
......@@ -4,6 +4,10 @@ From iris_c.c_translation Require Import monad translation proofmode.
Definition known_locs := list loc.
Lemma prefix_trans (E E' E'': known_locs) :
E `prefix_of` E' E' `prefix_of` E'' E `prefix_of` E''.
Proof. intros. eapply PreOrder_Transitive; eauto. Qed.
Inductive dloc :=
| dLoc : nat dloc
| dLocUnknown : loc dloc.
......@@ -236,9 +240,6 @@ Proof. by intros <-. Qed.
(** DCexpr *)
(*TODO: extend this with other constructions :
alloc, unop *)
Inductive dcexpr : Type :=
| dCRet : dval dcexpr
| dCAlloc : dcexpr dcexpr
......@@ -261,6 +262,81 @@ Fixpoint dcexpr_interp (E: known_locs) (de: dcexpr) : expr :=
| dCUnknown e1 => e1
end.
(** Well-foundness of dcexpr w.r.t. known_locs *)
Definition dval_wf (E: known_locs) (dv : dval) : bool :=
match dv with
| dLitV (dLitLoc (dLoc i)) => bool_decide (is_Some (E!!i))
| _ => true
end.
Fixpoint dcexpr_wf (E: known_locs) (de: dcexpr) : bool :=
match de with
| dCRet dv => dval_wf E dv
| dCAlloc de1 | dCLoad de1 | dCUnOp _ de1 => dcexpr_wf E de1
| dCStore de1 de2 | dCBinOp _ de1 de2 | dCSeq de1 de2 =>
dcexpr_wf E de1 && dcexpr_wf E de2
| dCUnknown _ => true
end.
(*TODO: Fuse wf_mono and interp_mono into one lemma for dval and dcexpr *)
Lemma dval_wf_mono (E E': known_locs) (dv: dval) :
dval_wf E dv E `prefix_of` E' dval_wf E' dv.
Proof.
destruct dv as [d|]; last done. destruct d; eauto.
destruct d as [i|]; last done; simplify_eq /=.
intros Hb Hpre. case_bool_decide; last done.
clear Hb. generalize dependent E. revert E'. induction i as [| i].
- intros E' E Hpre H. destruct E; first by apply is_Some_None in H.
destruct E'. by apply prefix_nil_not in Hpre.
apply prefix_cons_inv_1 in Hpre; subst. done.
- intros E' E Hpre H. destruct E'.
+ destruct E; first by apply is_Some_None in H.
by apply prefix_nil_not in Hpre.
+ destruct E; first by apply is_Some_None in H.
specialize (prefix_cons_inv_2 _ _ _ _ Hpre). intros Hpre'.
apply prefix_cons_inv_1 in Hpre. simpl. apply (IHi E' E); eauto.
Qed.
Lemma dcexpr_wf_mono (E E': known_locs) (de: dcexpr) :
dcexpr_wf E de E `prefix_of` E' dcexpr_wf E' de.
Proof.
induction de; simplify_eq /=; try eauto.
- apply dval_wf_mono.
- intros H Hpre. apply andb_prop_elim in H as [H1 H2]; eauto.
- intros H Hpre. apply andb_prop_elim in H as [H1 H2]; eauto.
- intros H Hpre. apply andb_prop_elim in H as [H1 H2]; eauto.
Qed.
Lemma dval_interp_mono (E E': known_locs) (dv: dval) :
dval_wf E dv E `prefix_of` E' dval_interp E dv = dval_interp E' dv.
Proof.
destruct dv as [d|]; last done. destruct d; eauto.
destruct d as [i|]; last done; simplify_eq /=.
intros Hb Hpre. case_bool_decide; last done.
clear Hb. generalize dependent E. revert E'. induction i as [| i].
- intros E' E Hpre H. destruct E; first by apply is_Some_None in H.
destruct E'. by apply prefix_nil_not in Hpre.
apply prefix_cons_inv_1 in Hpre; subst. done.
- intros E' E Hpre H. destruct E'.
+ destruct E; first by apply is_Some_None in H.
by apply prefix_nil_not in Hpre.
+ destruct E; first by apply is_Some_None in H.
specialize (prefix_cons_inv_2 _ _ _ _ Hpre). intros Hpre'.
apply prefix_cons_inv_1 in Hpre. simpl. apply (IHi E' E); eauto.
Qed.
Lemma dcexpr_interp_mono (E E': known_locs) (de: dcexpr) :
dcexpr_wf E de E `prefix_of` E' dcexpr_interp E de = dcexpr_interp E' de.
Proof.
induction de; simplify_eq /=; intros H Hpre;
try (by rewrite IHde ) ||
(apply andb_prop_elim in H as [H1 H2];
rewrite IHde2; [rewrite IHde1; done | done | done ];
by rewrite (IHde1 H1 Hpre (dcexpr_interp E de1))) || eauto.
do 2 f_equal. by apply dval_interp_mono.
Qed.
Global Instance dcexpr_closed E de : Closed [] (dcexpr_interp E de).
Proof. induction de; simpl; solve_closed. Qed.
......
......@@ -409,26 +409,6 @@ Section vcg_spec.
iExists E, dv', []; iSplit; first done. iFrame. unfold denv_interp. eauto.
Qed.
Lemma prefix_trans (E E' E'': known_locs) :
E `prefix_of` E' E' `prefix_of` E'' E `prefix_of` E''.
Proof. intros. eapply PreOrder_Transitive; eauto. Qed.
Lemma dloc_interp_mono E E' i :
E `prefix_of` E' l, dloc_interp E (dLoc i) = l dloc_interp E' (dLoc i) = l.
Proof. Admitted.
Lemma dval_interp_mono E E' dv :
E `prefix_of` E'
v, (dval_interp E dv) = v (dval_interp E' dv) = v.
Proof. Admitted.
Lemma dcexpr_interp_mono E E' de :
E `prefix_of` E'
e, (dcexpr_interp E de) = e (dcexpr_interp E' de) = e.
Proof. Admitted.
Lemma vcg_wp_correct R E m de Φ :
denv_interp E m -
wp_interp E (vcg_wp E m de R Φ) -
......@@ -448,25 +428,27 @@ Section vcg_spec.
iExists Ef, dvf, mf. iSplit. iPureIntro. eapply prefix_trans; done. eauto with iFrame.
- admit.
- admit.
- (* rewrite IHde. iApply a_un_op_spec. iSpecialize ("Hm" with "Hwp").
- rewrite IHde. iApply a_un_op_spec. iSpecialize ("Hm" with "Hwp").
iApply (awp_wand with "Hm"). iIntros (v) "Hex".
iDestruct "Hex" as (E' dv m' <-) "(Hm & Hwp)".
iDestruct "Hex" as (E' dv m' Hpre <-) "(Hm & Hwp)".
destruct (dun_op_eval E' u dv) as [| dw | dw] eqn:Hop; simpl.
+ iDestruct "Hwp" as (?) "[% _]"; simplify_eq /=.
+ iExists (dval_interp E' dw); iSplit.
iPureIntro. apply dun_op_eval_correct. by rewrite Hop.
eauto with iFrame.
iExists E', dw, m'; eauto with iFrame.
+ iDestruct "Hwp" as (w) "[% Hwp]"; simplify_eq /=.
iExists (dval_interp E' w). iSplit. iPureIntro.
apply dun_op_eval_correct. by rewrite Hop.
eauto with iFrame. *) admit.
iExists E', w, m'; eauto with iFrame.
- rewrite IHde1. iSpecialize ("Hm" with "Hwp"); fold vcg_wp.
iApply (a_sequence_spec with "[Hm]"); fold dcexpr_interp.
{ exists (λ: <>, dcexpr_interp E de2)%V. by unlock. }
iApply (awp_wand with "Hm"). iIntros (v) "Hex".
iDestruct "Hex" as (Enew dv m' Hpre <-) "(Hm & Hwp)". simpl. rewrite denv_unlock_interp.
iModIntro. rewrite IHde2. awp_seq. iSpecialize ("Hm" with "Hwp").
specialize (dcexpr_interp_mono E Enew de2 Hpre (dcexpr_interp E de2) eq_refl).
assert (dcexpr_wf E de2). admit.
(*TODO: fix this by extending statement of the correctness *)
specialize (dcexpr_interp_mono E Enew de2 H0 Hpre).
intro Heq; rewrite Heq. iApply (awp_wand with "Hm").
iIntros (v) "Hex".
iDestruct "Hex" as (Ef dvf mf Hpref <-) "(Hm & Hwp)". simpl.
......
Markdown is supported
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