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

factor out the postcondtion in vcg_wp lemmas

parent 3c9f273a
......@@ -9,18 +9,12 @@ Section tests_vcg.
Context `{amonadG Σ}.
Lemma test0 (l1 l2 : loc) (e: expr) `{Closed [] e}:
l1 C #1 - l2 C #1 - awp e True (λ _, True) - awp (alloc 1; e ; ∗ᶜ l1) True (λ v, l1 C #1 l2 C #1).
(* Lemma test0 (l1 l2 : loc) (e: expr) `{Closed [] e}:
l1 ↦C #1 -∗ l2 ↦C #1 -∗ awp e True (λ _, True) -∗
awp (allocᶜ ♯1;ᶜ e ;ᶜ ∗ᶜ ♯l1) True (λ v, l1 ↦C #1 ∗ l2 ↦C #1).
Proof.
iIntros "Hl1 Hl2 Hawp". vcg_solver.
iIntros "Hl2 Hl1". iApply a_alloc_spec. awp_ret_value.
iIntros (k) "Hk".
vcg_continue.
iModIntro.
iIntros "Hl2 Hl1 Hk".
Abort.
iIntros "Hl2 Hl1". Abort. *)
Lemma test1 (l k : loc) (e: expr) `{Closed [] e}:
( Φ v, k C v - (k C #12 - Φ v) - awp e True Φ) -
......@@ -39,14 +33,12 @@ Section tests_vcg.
vcg_continue. eauto.
Qed.
Lemma test3 (k : loc) :
Lemma test2 (k : loc) :
k C #10 - awp (alloc 11 = ∗ᶜ♯k + 2) True (λ v, True).
Proof.
iIntros "Hk". vcg_solver.
iIntros "Hk".
iApply a_alloc_spec. iApply awp_ret. iApply wp_value.
iIntros (l) "Hl".
vcg_continue.
iIntros "Hk". iApply a_alloc_spec. awp_ret_value.
iIntros (l) "Hl". vcg_continue.
eauto 42 with iFrame.
Qed.
......
......@@ -28,22 +28,15 @@ Section vcg_continue.
FromKnownLocs (PenvItem l x q v :: Γls) E_old (l :: E_new) | 100.
Proof. done. Qed.
Lemma tac_exists_known_locs Γs_in Γs_out Γls Γp c ps v E_old E_new (Φ: known_locs denv dval iProp Σ):
MapstoListFromEnv Γs_in Γs_out Γls
FromKnownLocs Γls E_old E_new
ListOfMapsto Γls (E_old ++ E_new) ps
envs_entails (Envs Γp Γs_out c)
(denv_wf (E_old ++ E_new) ps Φ (E_old ++ E_new) ps (dValUnknown v))
envs_entails (Envs Γp Γs_in c)
( (E': known_locs) (m': denv) (dv: dval),
v = dval_interp E' dv E_old `prefix_of` E'
(denv_wf E' m')
dval_wf E' dv
denv_interp E' m'
Φ E' m' dv)%I.
envs_entails (Envs Γp Γs_in c) (vcg_wp_postcondition E_old Φ v).
Proof.
unfold vcg_wp_postcondition.
intros Hsplit. rewrite /ListOfMapsto environments.envs_entails_eq=> Hexhale.
unfold of_envs. simpl. intros HGls Hgoal.
rewrite mapsto_list_from_env.
......@@ -57,17 +50,17 @@ Section vcg_continue.
* by left.
* right. by apply Hsplit.
}
iExists (E_old++E_new), ps, (dValUnknown v). repeat iSplit; eauto using prefix_app_r.
iExists (E_old++E_new), (dValUnknown v), ps. repeat iSplit; eauto using prefix_app_r.
iFrame. by iApply HGls.
Qed.
End vcg_continue.
(* TODO: How to avoid computing mapsto_wand and dloc under vcg_wp_unknown ? *)
(* Arguments dloc_interp : simpl never. *)
(* Arguments vcg_wp_unknown : simpl never. *)
Declare Reduction vcg_cbv :=
cbv [ vcg_wp vcg_wp_bin_op vcg_wp_store vcg_wp_load vcg_wp_unknown mapsto_wand_list].
cbv [ vcg_wp vcg_wp_bin_op vcg_wp_store vcg_wp_load mapsto_wand_list].
Ltac vcg_compute :=
match goal with
......
......@@ -91,19 +91,23 @@ Section vcg.
| dCAlloc _ | dCUnknown _ => None
end.
Definition vcg_wp_unknown (R : iProp Σ) (E: known_locs) (de: dcexpr) (m: denv)
(Φ : known_locs denv dval iProp Σ) : iProp Σ :=
mapsto_wand_list E m
(awp (dcexpr_interp E de) R (λ v,
E' m' dv,
Definition vcg_wp_postcondition (E: known_locs)
(Φ : known_locs denv dval iProp Σ) : val iProp Σ :=
λ v, ( E' dv m',
v = dval_interp E' dv
E `prefix_of` E'
(denv_wf E' m')
dval_wf E' dv
denv_interp E' m'
(Φ E' m' dv)))%I.
Arguments vcg_wp_unknown : simpl never.
(Φ E' m' dv))%I.
Arguments vcg_wp_postcondition : simpl never.
Definition vcg_wp_unknown (R : iProp Σ) (E: known_locs) (de: dcexpr) (m: denv)
(Φ : known_locs denv dval iProp Σ) : iProp Σ :=
mapsto_wand_list E m (awp (dcexpr_interp E de) R (vcg_wp_postcondition E Φ)).
Definition vcg_wp_load (E : known_locs) (dv : dval) (m : denv)
(Φ : denv dval iProp Σ) : iProp Σ :=
......@@ -449,14 +453,13 @@ Section vcg_spec.
denv_wf E m
denv_interp E m -
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 dval_wf E' dv
denv_wf E' m' denv_interp E' m' Φ E' m' dv).
awp (dcexpr_interp E de) R (vcg_wp_postcondition E Φ).
Proof.
rewrite /vcg_wp_unknown mapsto_wand_list_spec.
iIntros (Hmwf) "Hm Hwp". iSpecialize ("Hwp" with "Hm").
iApply (awp_wand with "Hwp"). iIntros (v) "H".
iDestruct "H" as (E' m' dv ->) "(% & % & Hm & Hwp)".
iDestruct "H" as (E' dv m' ->) "(% & % & Hm & Hwp)".
unfold vcg_wp_postcondition.
iExists E', dv, m'. repeat (iSplit; first done); iFrame.
Qed.
......@@ -464,31 +467,29 @@ Section vcg_spec.
denv_wf E m
denv_interp E m -
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 dval_wf E' dv'
denv_wf E' m' denv_interp E' m' Φ E' m' dv').
(l:loc) q w, dval_interp E dv = #l
l C{q} w (l C{q} w - (vcg_wp_postcondition E Φ w)).
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 (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. iSplit; first done.
eapply denv_lookup_wf in Hlkp; eauto with iFrame.
iExists (dloc_interp E (dLoc i)), q, (dval_interp E dv');
iSplit; first done. iFrame. iIntros "Hl".
iExists E, dv', m; repeat (iSplit; first done). iFrame.
rewrite Hm0. eapply denv_lookup_wf in Hlkp; eauto with iFrame.
* rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
iSpecialize ("Hwp" with "Hm"). simpl.
iDestruct "Hwp" as (q v') "[Hl Hwp]". apply is_dloc_some in Hdloc. subst.
iExists (dloc_interp E (dLoc i)), q, v'. iSplit; first done.
iFrame. iIntros "Hl". iSpecialize ("Hwp" with "Hl").
iExists (dloc_interp E (dLoc i)), q, v'; iSplit; first done. iFrame.
iIntros "Hl". iSpecialize ("Hwp" with "Hl").
iExists E, (dValUnknown v'), []; 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 (l) "(-> & Hwp)". iDestruct "Hwp" as (q v') "[Hl Hwp]".
iExists l, q, v'. iSplit; first done.
iFrame. iIntros "Hl". iSpecialize ("Hwp" with "Hl").
iDestruct "Hwp" as (l) "(% & Hwp)". iDestruct "Hwp" as (q v') "[Hl Hwp]".
iExists l, q, v'; iSplit; first done. iFrame. iIntros "Hl".
iSpecialize ("Hwp" with "Hl").
iExists E, (dValUnknown v'), []; iSplit; first done.
iFrame. unfold denv_interp, denv_wf. eauto.
Qed.
......@@ -500,8 +501,7 @@ Section vcg_spec.
vcg_wp_bin_op E b dv1 dv2 (denv_merge mOut m) (Φ E) -
denv_interp E mOut -
w : val, bin_op_eval b (dval_interp E dv1) (dval_interp E dv2) = Some w
( E' dv m', E0 `prefix_of` E' dval_interp E' dv = w dval_wf E' dv
denv_wf E' m' denv_interp E' m' Φ E' m' dv).
(vcg_wp_postcondition E Φ w).
Proof.
iIntros (Hpre Hwf1 Hwf2 Hwf3) "Hm Hwp HmOut". rewrite /vcg_wp_bin_op.
destruct (dbin_op_eval E b dv1 dv2) as [ | dw | dw ] eqn:Hbin; first done.
......@@ -518,17 +518,15 @@ Section vcg_spec.
apply dbin_op_eval_dUnknown_wf in Hbin; try done. eauto with iFrame.
Qed.
Lemma vcg_wp_store_correct E0 E m dv1 dv2 Φ :
Lemma vcg_wp_store_correct E0 E m dv1 dv2 Φ :
E0 `prefix_of` E
denv_wf E m
dval_wf E dv2
denv_interp E m -
vcg_wp_store E dv1 dv2 m (Φ E) -
(l : loc) (w : val), dval_interp E dv1 = #l
l C w (l C[LLvl] dval_interp E dv2 -
E' dv m', E0 `prefix_of` E' dval_interp E' dv = dval_interp E dv2
dval_wf E' dv denv_wf E' m' denv_interp E' m' Φ E' m' dv).
Proof.
(l : loc) (w : val), dval_interp E dv1 = #l l C w
(l C[LLvl] dval_interp E dv2 - vcg_wp_postcondition E0 Φ (dval_interp E dv2)).
Proof.
iIntros (Hpre Hwf Hwf2) "Hm Hwp". rewrite{1} /vcg_wp_store; fold vcg_wp.
destruct (is_dloc E dv1) as [i|] eqn:Hdloc.
- apply is_dloc_some in Hdloc; rewrite Hdloc.
......@@ -539,7 +537,7 @@ Section vcg_spec.
iIntros "Hl". iExists E, dv2, (denv_insert i LLvl 1 dv2 m'); repeat (iSplit; first done).
iSplit. iPureIntro. apply denv_wf_insert; last done.
by specialize (denv_wf_delete_full E dv_old i m m' Hwf Hdel) as Hdelwf.
rewrite -denv_insert_interp. iFrame.
rewrite -denv_insert_interp. eauto with iFrame.
+ rewrite mapsto_wand_list_spec.
iSpecialize ("Hwp" with "[Hm]"); iFrame.
iDestruct "Hwp" as (dv_old) "[Hl Hwp]";
......@@ -553,18 +551,23 @@ Section vcg_spec.
iExists l,v ; iSplit; first done. iFrame.
iIntros "Hl". iSpecialize ("Hwp" with "Hl").
iExists E, dv2, []; repeat (iSplit; first done). unfold denv_interp. by iFrame.
Qed.
Qed.
Lemma vcg_wp_postcondition_mono E E' Φ w:
E `prefix_of` E' vcg_wp_postcondition E' Φ w - vcg_wp_postcondition E Φ w.
Proof.
iIntros (Hpre) "Hp".
iDestruct "Hp" as (E1 dv m' ? Hpre1 ?) "(% & Hm' & H)"; simplify_eq /=.
iExists E1, dv, m'; repeat (iSplit; first done).
iSplit. iPureIntro. by trans E'. eauto with iFrame.
Qed.
(* Use `vcg_wp_unknown` in this spec to shorten it (and to get all the
conjunctions in the same order. *)
Lemma vcg_wp_correct R E m de Φ :
Lemma vcg_wp_correct R E m de Φ :
dcexpr_wf E de
denv_wf E m
denv_interp E m -
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 dval_wf E' dv
denv_wf E' m' denv_interp E' m' Φ E' m' dv).
awp (dcexpr_interp E de) R (vcg_wp_postcondition E Φ).
Proof.
revert Φ E m. induction de; intros Φ E m Hwf; iIntros (Hmwf) "Hm Hwp".
- iApply awp_ret. wp_value_head.
......@@ -573,13 +576,15 @@ Section vcg_spec.
- rewrite IHde //. 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 Hwf2) "(Hm & Hwp)".
iIntros (v) "H". unfold vcg_wp_postcondition.
iDestruct "H" as (E' dv m' Heq Hwf0 Hm'wf Hwf2) "(Hm & Hwp)".
iPoseProof (vcg_wp_load_correct E' m' with "Hm Hwp") as "Hload"; first 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' <- Hwf3 Hwf4) "(Hmf & Hwp)".
iExists Ef, dvf, mf. iFrame. iSplit; first by iPureIntro; trans E'. done.
iDestruct "Hload" as (l q w) "(% & Hl & Hwp)". rewrite Heq.
iExists l, q, w. iSplit; first done. iFrame. iIntros "Hl".
iSpecialize ("Hwp" with "Hl"). unfold vcg_wp_postcondition.
iDestruct "Hwp" as (Ef dvf mf Hpre' Hwf5 Hwf3 Hwf4) "(Hmf & Hwp)".
iExists Ef, dvf, mf. iFrame. iSplit; first by iPureIntro. iSplit.
iPureIntro. trans E'; done. done.
- rewrite{1} /vcg_wp; fold vcg_wp.
simpl in Hwf. apply andb_prop_elim in Hwf as [Hwf1 Hwf2].
destruct (vcg_sp E m [] de1) as [[[[mIn mOut] mNew] dv1]|] eqn:Heqsp; last first.
......@@ -590,9 +595,9 @@ Section vcg_spec.
clear Heqsp2 Heqsp.
iDestruct (IHde1 with "HmIn Hwp") as "Hde1"; try done.
iApply (a_store_spec with "Hde1 Hde2"). iIntros "!>" (v1 v2).
iDestruct 1 as (E' dw m' ? <- ?) "(% & Hm' & H)". iIntros "[-> HmNew]".
iDestruct 1 as (E' dw m' ? Hpre ?) "(% & Hm' & H)". iIntros "[-> HmNew]".
rewrite (dval_interp_mono E E') //.
iApply (vcg_wp_store_correct with "[-H] H");
rewrite H4. iApply (vcg_wp_store_correct with "[-H] H");
eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
rewrite -!denv_merge_interp. iFrame "Hm'".
rewrite -!(denv_interp_mono E E'); eauto. iFrame.
......@@ -600,8 +605,8 @@ Section vcg_spec.
iDestruct (vcg_sp_correct with "Hm") as "[HmIn [HmOut Hde1]]"; first done. clear Heqsp.
iDestruct (IHde2 with "HmIn Hwp") as "Hde2"; try done.
iApply (a_store_spec with "Hde1 Hde2"). iIntros "!>" (v1 v2).
iIntros "[-> HmNew]". iDestruct 1 as (E' d_new m' ? <- ?) "(% & Hm' & H)".
rewrite (dval_interp_mono E E') //.
iIntros "[-> HmNew]". iDestruct 1 as (E' d_new m' ? Hpre ?) "(% & Hm' & H)".
rewrite (dval_interp_mono E E') //. rewrite H4.
iApply (vcg_wp_store_correct with "[-H] H");
eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
rewrite -!denv_merge_interp. iFrame "Hm'".
......@@ -617,9 +622,17 @@ Section vcg_spec.
rewrite IHde1; [| done | done]. iSpecialize ("HmIn" with "Hwp").
iApply (a_bin_op_spec with "HmIn Hde2"); fold dcexpr_interp.
iNext. iIntros (v1 v2) "Hex (-> & HmNew)".
iDestruct "Hex" as (E' dv1 m' Hpre <- Hm'wf) "(% & Hm' & Hwp)"; simplify_eq /=.
iDestruct "Hex" as (E' dv1 m' Heq Hpre Hm'wf) "(% & Hm' & Hwp)"; simplify_eq /=.
rewrite (dval_interp_mono E E' dv2); eauto.
iPoseProof (denv_interp_mono with "HmOut") as "HmOut'"; [done | done |].
iAssert (( w : val,
bin_op_eval b (dval_interp E' dv1) (dval_interp E' dv2) = Some w
vcg_wp_postcondition E' Φ w) -
w : val, bin_op_eval b (dval_interp E' dv1) (dval_interp E' dv2) = Some w
vcg_wp_postcondition E Φ w)%I as "Hassert".
iIntros "H". iDestruct "H" as (w) "(H1 & H2)".
iExists w. iFrame. iApply vcg_wp_postcondition_mono; done.
iApply "Hassert".
iApply (vcg_wp_bin_op_correct with "[Hm' HmOut'] Hwp [HmNew]");
eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
* rewrite -denv_merge_interp. iFrame.
......@@ -631,20 +644,28 @@ Section vcg_spec.
iRename "HmIn" into "Hde2".
iApply (a_bin_op_spec with "Hde1 Hde2"); fold dcexpr_interp.
iNext. iIntros (v1 v2) "(-> & HmNew) Hex".
iDestruct "Hex" as (E' dv2 m' Hpre <- Hm'wf) "(% & Hm' & Hwp)"; simplify_eq /=.
iDestruct "Hex" as (E' dv2 m' Hpre Hpre' Hm'wf) "(% & Hm' & Hwp)"; simplify_eq /=.
rewrite (dval_interp_mono E E' dv1); eauto.
iPoseProof (denv_interp_mono with "HmOut") as "HmOut'"; [done | done |].
iAssert (( w : val,
bin_op_eval b (dval_interp E' dv1) (dval_interp E' dv2) = Some w
vcg_wp_postcondition E' Φ w) -
w : val, bin_op_eval b (dval_interp E' dv1) (dval_interp E' dv2) = Some w
vcg_wp_postcondition E Φ w)%I as "Hassert".
iIntros "H". iDestruct "H" as (w) "(H1 & H2)".
iExists w. iFrame. iApply vcg_wp_postcondition_mono; done.
iApply "Hassert".
iApply (vcg_wp_bin_op_correct with "[Hm' HmOut'] Hwp [HmNew]");
eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
* rewrite -denv_merge_interp. iFrame.
* iApply (denv_interp_mono with "HmNew"); eauto.
- 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' Hpre <- Hm'wf) "(% & Hm & Hwp)".
iDestruct "Hex" as (E' dv m' Hpre 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.
iPureIntro. apply dun_op_eval_correct. by rewrite Hop.
+ rewrite Hpre. iExists (dval_interp E' dw); iSplit.
iPureIntro. eapply dun_op_eval_correct. by rewrite Hop.
iExists E', dw, m'. apply dun_op_eval_dSome_wf in Hop; last done.
eauto with iFrame.
+ iDestruct "Hwp" as (w) "[% Hwp]"; simplify_eq /=.
......@@ -657,15 +678,17 @@ Section vcg_spec.
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'wf) "(% & Hm & Hwp)". simpl.
iDestruct "Hex" as (Enew dv m' Hpre Hpre' Hm'wf) "(% & Hm & Hwp)". simpl.
rewrite denv_unlock_interp.
iModIntro. rewrite IHde2 //. awp_seq. iSpecialize ("Hm" with "Hwp").
specialize (dcexpr_interp_mono E Enew de2 Hwf2 Hpre).
specialize (dcexpr_interp_mono E Enew de2 Hwf2 Hpre').
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. trans Enew ; done. iSplit; first done.
iFrame. by eapply dcexpr_wf_mono in Hpre. by apply denv_wf_unlock.
iIntros (v1) "Hex".
iDestruct "Hex" as (Ef dvf mf Hpref Hpre3 Hyp4 Hyp5) "(Hm & Hwp)". simpl.
iExists Ef, dvf, mf; iSplit; first done. iSplit. iPureIntro. trans Enew ; done.
iSplit; first done.
iFrame. iPureIntro; done. eapply dcexpr_wf_mono in Hwf2.
done. done. by apply denv_wf_unlock.
- by iApply (vcg_wp_unknown_correct with "Hm Hwp").
Qed.
......@@ -688,7 +711,11 @@ Section vcg_spec.
rewrite (vcg_wp_correct R); last done.
iIntros (->) "H1 H2".
iSpecialize ("H2" with "H1"). iApply (awp_wand with "H2").
iIntros (v) "H". iDestruct "H" as (E' dv m' Hpre) "(-> & % & % & Hm & Hwp)".
iIntros (v) "H". unfold vcg_wp_postcondition.
iDestruct "H" as (E' dv m' Hpre) "(% & % & % & Hm & Hwp)".
rewrite Hpre.
rewrite mapsto_wand_list_spec. iApply ("Hwp" with "Hm"). done.
Qed.
Qed.
End vcg_spec.
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