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

well-foundness relation for denv: many admitted lemmas, used in the vcg_wp correctness proof.

parent aafa852b
......@@ -429,4 +429,40 @@ Section denv_spec.
- destruct di as [x q dv]. simpl.
destruct x; iModIntro; iFrame.
Qed.
(** well-foundness of denv *)
Fixpoint denv_wf (E: known_locs) (m: denv) : bool :=
match m with
| [] => true
| Some (DenvItem _ _ dv) :: m' => dval_wf E dv && denv_wf E m'
| None :: m' => denv_wf E m'
end.
(* Definition denv_wf_interp E m : iProp Σ := ([∗ list] i↦dio ∈ m,
from_option (λ '(DenvItem _ _ dv), ⌜is_true (dval_wf E dv)⌝) True dio)%I.*)
(*Lemma denv_wf_spec (E: known_locs) (m: denv) :
is_true(denv_wf E m) → denv_wf_interp E m.
Proof. Admitted.*)
Lemma denv_wf_mono E E' m :
denv_wf E m E `prefix_of` E' denv_wf E' m.
Proof. Admitted.
Lemma denv_wf_merge E m1 m2 :
denv_wf E m1 denv_wf E m2 denv_wf E (denv_merge m1 m2).
Proof. Admitted.
Lemma denv_wf_unlock E m1 :
denv_wf E m1 denv_wf E (denv_unlock m1).
Proof. Admitted.
Lemma denv_interp_mono E E' m :
denv_wf E m E `prefix_of` E'
denv_interp E m - denv_interp E' m.
Proof. Admitted.
(** / well-foundness of denv *)
End denv_spec.
......@@ -75,7 +75,7 @@ Section tests_vcg.
iExists [k;l], [Some (DenvItem ULvl 1 (dLitV (dLitInt 12)))].
iExists (dLitV (dLitInt 10)). iSplit; [done|]. iSplit; [done|].
iFrame "Hk"; iSplitR; first done.
simpl. iIntros "!> Hk Hl".
simpl. iSplit. done. iIntros "!> Hk Hl".
iApply ("He" with "Hk"); iIntros "Hk".
iExists [k;l], [Some (DenvItem ULvl 1 (dLitV (dLitInt 12)));
Some (DenvItem ULvl 1 (dLitV (dLitInt 2)))].
......
......@@ -139,6 +139,7 @@ Section vcg.
E' m' dv,
v = dval_interp E' dv
E `prefix_of` E'
is_true (denv_wf E' m')
denv_interp E' m'
wp_interp_sane E' (Φ E' m' dv))%I.
Arguments vcg_wp_unknown : simpl never.
......@@ -370,97 +371,119 @@ Section vcg_spec.
iApply "Hawp". by rewrite /denv_interp.
Qed.
Lemma vcg_sp_wf E de m mIn mOut dv :
denv_wf E m
dcexpr_wf E de
vcg_sp E m [] de = Some (mIn, mOut, dv)
denv_wf E mIn denv_wf E mOut dval_wf E dv .
Proof. Admitted.
Lemma vcg_wp_unknown_correct R E m de Φ :
denv_wf E m
denv_interp E m -
wp_interp E (vcg_wp_unknown R E de m Φ) -
awp (dcexpr_interp E de) R (λ v, E' dv m',
E `prefix_of` E' dval_interp E' dv = v
denv_interp E' m' wp_interp E' (Φ E' m' dv)).
denv_wf E' m' 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").
iIntros (Hmwf) "Hm Hwp". iSpecialize ("Hwp" with "Hm").
iApply (awp_wand with "Hwp"). iIntros (v) "H".
iDestruct "H" as (E' m' dv ->) "(Hpre & Hm & Hwp)".
iDestruct "H" as (E' m' dv ->) "(% & % & Hm & Hwp)".
rewrite wp_interp_sane_sound.
iExists E', dv, m'. by iSplit; first done; iFrame.
iExists E', dv, m'. repeat (iSplit; first done); iFrame.
naive_solver.
Qed.
Lemma vcg_wp_load_correct E m dv Φ :
denv_wf E m
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', E `prefix_of` E' dval_interp E' dv' = w
denv_interp E' m' wp_interp E' (Φ E' m' dv')).
denv_wf E' m' 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 /=.
* destruct (denv_lookup_interp E i q dv' m) as [m0 Hm0]; first assumption.
rewrite Hm0. iIntros "[Hi Hm0] HΦ". apply is_dloc_some in Hdloc. simplify_eq/=.
rewrite Hm0. iIntros (Hmwf) "[Hi Hm0] HΦ". apply is_dloc_some in Hdloc. simplify_eq/=.
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. by iFrame.
* rewrite mapsto_wand_list_spec. iIntros "Hm Hwp". iSpecialize ("Hwp" with "Hm"). simpl.
rewrite Hm0. iSplit; first done. eauto with iFrame.
* rewrite mapsto_wand_list_spec. iIntros (Hmwf) "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. unfold denv_interp. eauto.
+ rewrite mapsto_wand_list_spec. iIntros "Hm Hwp". iSpecialize ("Hwp" with "Hm"); simpl.
iExists E, dv', []; repeat (iSplit; first done); iFrame.
unfold denv_interp, denv_wf. eauto.
+ rewrite mapsto_wand_list_spec. iIntros (Hmwf) "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. unfold denv_interp. eauto.
iExists E, dv', []; iSplit; first done. iFrame. unfold denv_interp, denv_wf. eauto.
Qed.
Lemma vcg_wp_correct R E m de Φ :
dcexpr_wf E de
denv_wf E m
denv_interp E m -
wp_interp E (vcg_wp E m de R Φ) -
awp (dcexpr_interp E de) R (λ v, E' dv m',
E `prefix_of` E' dval_interp E' dv = v
denv_interp E' m' wp_interp E' (Φ E' m' dv)).
denv_wf E' m' denv_interp E' m' wp_interp E' (Φ E' m' dv)).
Proof.
revert Φ E m. induction de; intros Φ E m Hwf; iIntros "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; last done. 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' Hpre <-) "(Hm & Hwp)".
iPoseProof (vcg_wp_load_correct E' m' with "Hm Hwp") as "Hload".
revert Φ E m. induction de; intros Φ E m Hwf; iIntros (Hmwf) "Hm Hwp".
- iApply awp_ret. wp_value_head.
iExists E, d, m. iSplit; first done; by iFrame.
- by iApply (vcg_wp_unknown_correct with "Hm Hwp").
- rewrite IHde; last done. iRename "Hm" into "Hawp".
iSpecialize ("Hawp" with "Hwp"); simpl.
iApply (a_load_spec_exists_frac with "[Hawp]"). iApply (awp_wand with "Hawp").
iIntros (v) "H". iDestruct "H" as (E' dv m' Hpre <- Hm'wf) "(Hm & Hwp)".
iPoseProof (vcg_wp_load_correct E' m' with "Hm Hwp") as "Hload". done.
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. iFrame. by iSplit; first by iPureIntro; trans E'; done.
iExists Ef, dvf, mf. iFrame. by iSplit; first by iPureIntro; trans E'; done. done.
- admit.
- rewrite{1} /vcg_wp; fold vcg_wp.
destruct (vcg_sp E m [] de1) as [[[mIn mOut] dv1]|] eqn:Heqsp; last first.
+ destruct (vcg_sp E m [] de2) as [[[mIn mOut] dv2]|] eqn:Heqsp2; last first.
{ iApply (vcg_wp_unknown_correct with "[$Hm] [$Hwp]"). }
{ by iApply (vcg_wp_unknown_correct with "Hm Hwp"). }
iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
iDestruct ("Hsp" with "Hm") as "[Hm Hde2]". iClear "Hsp". clear Heqsp2 Heqsp.
rewrite IHde1; last first.
{ simpl in Hwf. apply andb_prop_elim in Hwf. by destruct Hwf. }
iSpecialize ("Hm" with "Hwp").
iApply (a_bin_op_spec with "[$Hm] [$Hde2]"); fold dcexpr_interp.
simpl in Hwf; apply andb_prop_elim in Hwf; destruct Hwf as [Hwf1 Hwf2].
specialize (vcg_sp_wf _ _ _ _ _ _ Hmwf Hwf2 Heqsp2) as (H1 & H2 & Hwf).
iDestruct ("Hsp" with "[$Hm]") as "[HmIn Hde2]"; iClear "Hsp"; clear Heqsp2 Heqsp.
rewrite IHde1; [| done |]. iSpecialize ("HmIn" with "Hwp").
iApply (a_bin_op_spec with "[$HmIn] [$Hde2]"); fold dcexpr_interp.
iNext. iIntros (v1 v2) "Hex (-> & HmOut)".
iDestruct "Hex" as (E' dv1 m' Hpre <-) "(Hm' & Hwp)"; simplify_eq /=.
iDestruct "Hex" as (E' dv1 m' Hpre <- Hm'wf) "(Hm' & Hwp)"; simplify_eq /=.
rewrite /vcg_wp_bin_op.
destruct (dbin_op_eval E' b dv1 dv2) as [ | dw | dw ] eqn:Hbin; first done.
* iExists (dval_interp E' dw); iSplit.
{ iPureIntro. (*TODO: we need (dval_interp E dv2) = (dval_interp E' dv2) *) admit. }
{ iPureIntro.
rewrite (dval_interp_mono _ _ _ Hwf Hpre).
apply dbin_op_eval_correct. by rewrite Hbin. }
iExists E', dw, (denv_merge mOut m').
rewrite -denv_merge_interp. iFrame. repeat (iSplit; first done).
(*TODO: we have to relate denv_interp and prefix_of *) admit.
iSplit. iPureIntro. apply denv_wf_merge. by eapply denv_wf_mono; done. done.
iApply (denv_interp_mono with "HmOut"); done.
* destruct dw as [dw1|] eqn:Hdw; last done.
iExists (dval_interp E' dw1); iSplit.
{ iPureIntro. (*TODO: we need (dval_interp E dv2) = (dval_interp E' dv2) *) admit. }
{ iPureIntro. rewrite (dval_interp_mono _ _ _ Hwf Hpre).
apply dbin_op_eval_correct. by rewrite Hbin. }
iExists E', dw1, (denv_merge mOut m').
rewrite -denv_merge_interp. iFrame. repeat (iSplit; first done).
(*TODO: we have to relate denv_interp and prefix_of *) admit.
iSplit. iPureIntro. apply denv_wf_merge. by eapply denv_wf_mono; done. done.
iApply (denv_interp_mono with "HmOut"); done.
* done.
+ admit.
- rewrite IHde; last done. iApply a_un_op_spec. iSpecialize ("Hm" with "Hwp").
iApply (awp_wand with "Hm"). iIntros (v) "Hex".
iDestruct "Hex" as (E' dv m' Hpre <-) "(Hm & Hwp)".
iDestruct "Hex" as (E' dv m' Hpre <- Hm'wf) "(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.
......@@ -470,13 +493,14 @@ Section vcg_spec.
iExists (dval_interp E' w). iSplit. iPureIntro.
apply dun_op_eval_correct. by rewrite Hop.
iExists E', w, m'; eauto with iFrame.
- rewrite IHde1; last first.
+ done.
- rewrite IHde1; last first. done.
{ simpl in Hwf. apply andb_prop_elim in Hwf. by destruct Hwf. }
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.
iDestruct "Hex" as (Enew dv m' Hpre <- Hm'wf) "(Hm & Hwp)". simpl.
rewrite denv_unlock_interp.
iModIntro. rewrite IHde2. awp_seq. iSpecialize ("Hm" with "Hwp").
simpl in Hwf; apply andb_prop_elim in Hwf; destruct Hwf.
......@@ -486,14 +510,16 @@ Section vcg_spec.
iDestruct "Hex" as (Ef dvf mf Hpref <-) "(Hm & Hwp)". simpl.
iExists Ef, dvf, mf. iSplit. iPureIntro. trans Enew ; done. iSplit; first done.
iFrame. simpl in Hwf; apply andb_prop_elim in Hwf; destruct Hwf.
by eapply dcexpr_wf_mono in Hpre.
- iApply (vcg_wp_unknown_correct with "Hm Hwp").
by eapply dcexpr_wf_mono in Hpre.
by apply denv_wf_unlock.
- by iApply (vcg_wp_unknown_correct with "Hm Hwp").
Admitted.
Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E de :
MapstoListFromEnv Γs_in Γs_out Γls
E = penv_to_known_locs Γls
dcexpr_wf E de
denv_wf (penv_to_known_locs Γls) m
ListOfMapsto Γls E m
IntoDCexpr E e de
environments.envs_entails (environments.Envs Γp Γs_out c)
......@@ -502,15 +528,15 @@ Section vcg_spec.
environments.envs_entails (environments.Envs Γp Γs_in c) (awp e R Φ).
Proof.
rewrite /IntoDCexpr /=. intros Hsplit ->.
rewrite /ListOfMapsto. intros Hwf Hpenv -> Hgoal.
rewrite /ListOfMapsto. intros Hwf Hmwf Hpenv -> Hgoal.
eapply tac_envs_split_mapsto; try eassumption.
revert Hgoal. rewrite environments.envs_entails_eq.
rewrite (vcg_wp_correct R); last done.
iIntros (->) "H1 H2". rewrite wp_interp_sane_sound.
iSpecialize ("H2" with "H1"). iApply (awp_wand with "H2").
iIntros (v) "H". iDestruct "H" as (E' dv m' Hpre) "(-> & Hm & Hwp)".
rewrite mapsto_wand_list_spec. iApply ("Hwp" with "Hm").
Qed.
iIntros (v) "H". iDestruct "H" as (E' dv m' Hpre) "(-> & Hmwf & Hm & Hwp)".
rewrite mapsto_wand_list_spec. iApply ("Hwp" with "Hm"). done.
Qed.
End vcg_spec.
......@@ -520,7 +546,8 @@ Ltac vcg_solver :=
eapply tac_vcg_sound;
[ apply _ (* MapstoListFromEnv Γs_in Γs_out Γls *)
| compute; reflexivity (* E = penv_to_known_locs Γls *)
| (* dcexpr_wf E de *)
| (* dcexpr_wf E de *)
| (* denv_wf E m *)
| apply _ (* ListOfMapsto Γls E m *)
| apply _ (* IntoDCexpr E e dce *)
| simpl ]; intuition.
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