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

working on vcg_wp

parent 6780792e
......@@ -373,21 +373,21 @@ Section vcg_spec.
denv_interp E m -
wp_interp E (vcg_wp_unknown R E de m Φ) -
awp (dcexpr_interp E de) R
(λ v, E' dv m', dval_interp E' dv = v denv_interp E' m' wp_interp E' (Φ E' m' dv)).
(λ v, E' dv m', E `prefix_of` E' dval_interp E' dv = v denv_interp E' m' wp_interp E' (Φ E' m' dv)).
Proof.
rewrite /vcg_wp_unknown mapsto_wand_list_spec.
iIntros "Hm Hwp". iSpecialize ("Hwp" with "Hm").
iApply (awp_wand with "Hwp"). iIntros (v) "H".
iDestruct "H" as (E' m' dv ->) "(Hpre & Hm & Hwp)".
rewrite wp_interp_sane_sound.
iExists E', dv, m'. iSplit; first done; iFrame.
iExists E', dv, m'. by iSplit; first done; iFrame.
Qed.
Lemma vcg_wp_load_correct E m dv Φ :
denv_interp E m -
wp_interp E (vcg_wp_load E dv m (Φ E)) -
(l:loc) q w, dval_interp E dv = #l l C{q} w (l C{q} w -
E' dv' m', dval_interp E' dv' = w denv_interp E' m' wp_interp E' (Φ E' m' dv')).
E' dv' m', E `prefix_of` E' dval_interp E' dv' = w denv_interp E' m' wp_interp E' (Φ E' m' dv')).
Proof.
rewrite /vcg_wp_load. destruct (is_dloc E dv) as [i|] eqn:Hdloc.
+ destruct (denv_lookup i m) as [[q dv'] |] eqn:Hlkp; simpl; simplify_eq /=.
......@@ -396,35 +396,59 @@ Section vcg_spec.
iExists (dloc_interp E (dLoc i)), q, (dval_interp E dv').
iSplit. simplify_eq /=; done. iFrame. iIntros "Hl".
iExists E, dv', m; iSplit; first done. iFrame.
rewrite Hm0. iFrame.
rewrite Hm0. by iFrame.
* rewrite mapsto_wand_list_spec. iIntros "Hm Hwp". iSpecialize ("Hwp" with "Hm"). simpl.
iDestruct "Hwp" as (q dv') "[Hl Hwp]". apply is_dloc_some in Hdloc. subst.
iExists (dloc_interp E (dLoc i)), q, (dval_interp E dv'). iSplit; first done.
iFrame. iIntros "Hl". iSpecialize ("Hwp" with "Hl").
iExists E, dv', []; iSplit; first done. iFrame. by unfold denv_interp.
iExists E, dv', []; iSplit; first done. iFrame. unfold denv_interp. eauto.
+ rewrite mapsto_wand_list_spec. iIntros "Hm Hwp". iSpecialize ("Hwp" with "Hm"); simpl.
iDestruct "Hwp" as (dl) "(-> & Hwp)". iDestruct "Hwp" as (q dv') "[Hl Hwp]".
iExists (dloc_interp E dl), q, (dval_interp E dv'). iSplit; first done.
iFrame. iIntros "Hl". iSpecialize ("Hwp" with "Hl").
iExists E, dv', []; iSplit; first done. iFrame. by unfold denv_interp.
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 Φ) -
awp (dcexpr_interp E de) R
(λ v, E' dv m', dval_interp E' dv = v denv_interp E' m' wp_interp E' (Φ E' m' dv)).
(λ v, E' dv m', E `prefix_of` E' dval_interp E' dv = v denv_interp E' m' wp_interp E' (Φ E' m' dv)).
Proof.
revert Φ E m. induction de; intros Φ E m; iIntros "Hm Hwp".
- iApply awp_ret. wp_value_head. iExists E, d, m. iSplit; first done; iFrame.
- iApply (vcg_wp_unknown_correct with "Hm Hwp").
- iApply awp_ret. wp_value_head. iExists E, d, m. iSplit; first done; by iFrame.
- iApply (vcg_wp_unknown_correct with "Hm Hwp").
- rewrite IHde. iSpecialize ("Hm" with "Hwp"); simpl.
iApply (a_load_spec_exists_frac with "[Hm]"). iApply (awp_wand with "Hm").
iIntros (v) "H". iDestruct "H" as (E' dv m' <-) "(Hm & Hwp)".
iApply (vcg_wp_load_correct with "Hm Hwp").
iIntros (v) "H". iDestruct "H" as (E' dv m' Hpre <-) "(Hm & Hwp)".
iPoseProof (vcg_wp_load_correct E' m' with "Hm Hwp") as "Hload".
iDestruct "Hload" as (l q w ->) "(Hl & Hwp)".
iExists l, q, w; iSplit; first done. iFrame. iIntros "Hl".
iSpecialize ("Hwp" with "Hl"). iDestruct "Hwp" as (Ef dvf mf Hpre' <-) "(Hmf & Hwp)".
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)".
destruct (dun_op_eval E' u dv) as [| dw | dw] eqn:Hop; simpl.
......@@ -435,15 +459,19 @@ Section vcg_spec.
+ 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.
eauto with iFrame. *) admit.
- 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' <-) "(Hm & Hwp)". simpl. rewrite denv_unlock_interp.
iDestruct "Hex" as (Enew dv m' Hpre <-) "(Hm & Hwp)". simpl. rewrite denv_unlock_interp.
iModIntro. rewrite IHde2. awp_seq. iSpecialize ("Hm" with "Hwp").
(* TODO: Need to make the main statement stronger by requiring that
E `prefix_of` E', just as in unknown case. *) admit.
specialize (dcexpr_interp_mono E Enew de2 Hpre (dcexpr_interp E de2) eq_refl).
intro Heq; rewrite Heq. iApply (awp_wand with "Hm").
iIntros (v) "Hex".
iDestruct "Hex" as (Ef dvf mf Hpref <-) "(Hm & Hwp)". simpl.
iExists Ef, dvf, mf. iSplit. iPureIntro. eapply prefix_trans; done. iSplit; first done.
iFrame.
- iApply (vcg_wp_unknown_correct with "Hm Hwp").
Admitted.
......
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