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

finished the proof of correctness for vcg_wp.

parent 96f5c3a3
......@@ -304,6 +304,31 @@ Proof.
- intros H Hpre. apply andb_prop_elim in H as [H1 H2]; eauto.
Qed.
Lemma dun_op_eval_dSome_wf E dv u dw:
dval_wf E dv dun_op_eval E u dv = dSome dw dval_wf E dw.
Proof.
Admitted.
Lemma dun_op_eval_dUnknown_wf E dv u w:
dval_wf E dv dun_op_eval E u dv = dUnknown (Some w) dval_wf E w.
Proof.
Admitted.
Lemma dbin_op_eval_dSome_wf E dv1 dv2 op dw:
dval_wf E dv1 dval_wf E dv2
dbin_op_eval E op dv1 dv2 = dSome dw dval_wf E dw.
Proof.
Admitted.
Lemma dbin_op_eval_dUnknown_wf E dv1 dv2 op w:
dval_wf E dv1 dval_wf E dv2
dbin_op_eval E op dv1 dv2 = dUnknown (Some w) dval_wf E w.
Proof.
Admitted.
(** / Well-foundness of dcexpr w.r.t. known_locs *)
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.
......
......@@ -458,6 +458,10 @@ Section denv_spec.
denv_wf E m1 denv_wf E (denv_unlock m1).
Proof. Admitted.
Lemma denv_lookup_wf E i m q dv :
denv_wf E m denv_lookup i m = Some (q, dv) dval_wf E dv.
Proof. Admitted.
Lemma denv_wf_insert E i x q dv m:
denv_wf E m dval_wf E dv denv_wf E (denv_insert i x q dv m).
Proof. Admitted.
......
......@@ -119,7 +119,8 @@ Section vcg.
E' m' dv,
v = dval_interp E' dv
E `prefix_of` E'
(denv_wf E' m')
(denv_wf E' m')
dval_wf E' dv
denv_interp E' m'
wp_interp E' (Φ E' m' dv))%I.
Arguments vcg_wp_unknown : simpl never.
......@@ -242,7 +243,7 @@ Section vcg_spec.
denv_interp E mIn -
denv_interp E mIn'
(denv_interp E mOut - awp (dcexpr_interp E de) R (λ v, v = dval_interp E dv denv_interp E mOut')).
Proof. (*
Proof.
revert mIn mOut mIn' mOut' dv. induction de;
iIntros (mIn mOut mIn' mOut' dv Hsp) "HmIn"; simplify_eq/=.
- iFrame. iIntros "HmOut". iApply awp_ret. wp_value_head. iSplit; eauto.
......@@ -275,15 +276,15 @@ Section vcg_spec.
iSpecialize ("Hawp2" with "[]"). rewrite /denv_interp; done.
iSpecialize ("Hawp1" with "HmOut").
iApply (a_store_spec _ _
(λ j, ⌜j = dloc_interp E (dLoc i)⌝ ∧ denv_interp E mOut1)%I with "[Hawp1] Hawp2").
(λ j, j = #(dloc_interp E (dLoc i)) denv_interp E mOut1)%I with "[Hawp1] Hawp2").
{ iApply (awp_wand with "Hawp1").
iIntros (?) "[% H]". simplify_eq/=. iExists _; eauto. }
iIntros (?) "[% H]". simplify_eq/=. eauto. }
iNext. iIntros (? ?) "[% HmOut1] [% HmOut2]". simplify_eq/=.
iExists _. rewrite -denv_merge_interp.
iExists _. rewrite -denv_merge_interp. iExists _.
iDestruct ("Hl" with "[$HmOut1 $HmOut2]") as "[HmOut3 $]".
iIntros "Hl". iSplit; eauto.
iSplit; eauto. iIntros "Hl".
rewrite -denv_insert_interp.
iFrame "Hl HmOut3".
iFrame "Hl HmOut3". done.
- specialize (IHde1 mIn mOut).
destruct (vcg_sp E mIn mOut de1) as [[[mIn1 mOut1] dv1]|]; simplify_eq /=.
specialize (IHde2 mIn1 []).
......@@ -321,7 +322,7 @@ Section vcg_spec.
iIntros (?) "[_ HmOut1]". rewrite (denv_unlock_interp E mOut1).
iModIntro. iSpecialize ("Hawp2" with "HmOut1").
awp_seq. iApply "Hawp2".
Qed. *) Admitted.
Qed.
Lemma vcg_sp_correct R E de m mIn mOut dv :
vcg_sp E m [] de = Some (mIn, mOut, dv)
......@@ -345,7 +346,7 @@ 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',
E `prefix_of` E' dval_interp E' dv = v
E `prefix_of` E' dval_interp E' dv = v dval_wf E' dv
denv_wf E' m' denv_interp E' m' wp_interp E' (Φ E' m' dv)).
Proof.
rewrite /vcg_wp_unknown mapsto_wand_list_spec.
......@@ -360,7 +361,7 @@ Section vcg_spec.
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
E' dv' m', E `prefix_of` E' dval_interp E' dv' = w dval_wf E' 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.
......@@ -370,7 +371,8 @@ 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. iSplit; first done. eauto with iFrame.
rewrite Hm0. iSplit; first done.
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.
......@@ -383,33 +385,36 @@ Section vcg_spec.
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.
iExists E, (dValUnknown v'), []; iSplit; first done.
iFrame. unfold denv_interp, denv_wf. eauto.
Qed.
Lemma vcg_wp_bin_op_correct E0 E m mOut dv1 dv2 b Φ :
E0 `prefix_of` E
E0 `prefix_of` E dval_wf E dv1 dval_wf E dv2
denv_wf E (denv_merge mOut m)
denv_interp E m -
wp_interp E (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
( E' dv m', E0 `prefix_of` E' dval_interp E' dv = w dval_wf E' dv
denv_wf E' m' denv_interp E' m' wp_interp E' (Φ E' m' dv)).
Proof.
iIntros (Hpre Hwf) "Hm Hwp HmOut". rewrite /vcg_wp_bin_op.
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.
* iExists (dval_interp E dw); iSplit.
* iExists (dval_interp E dw); iSplit.
{ iPureIntro. apply dbin_op_eval_correct. by rewrite Hbin. }
iExists E, dw, (denv_merge mOut m).
rewrite -denv_merge_interp. repeat (iSplit; first done); iFrame.
apply dbin_op_eval_dSome_wf in Hbin; try done.
rewrite -denv_merge_interp //. eauto with iFrame.
* destruct dw as [dw1|] eqn:Hdw; last done.
iExists (dval_interp E dw1); iSplit.
iPureIntro. apply dbin_op_eval_correct. by rewrite Hbin.
iPureIntro. apply dbin_op_eval_correct. by rewrite Hbin.
iExists E, dw1, (denv_merge mOut m).
rewrite -denv_merge_interp. repeat (iSplit; first done). iFrame.
rewrite -denv_merge_interp.
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
......@@ -418,37 +423,33 @@ Section vcg_spec.
(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
denv_wf E' m' denv_interp E' m' wp_interp E' (Φ E' m' dv)).
Proof. (*
dval_wf E' dv denv_wf E' m' denv_interp E' m' wp_interp E' (Φ E' m' dv)).
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.
iExists (dloc_interp E (dLoc i)). iSplit; first done.
destruct (denv_delete_full i m) as [[m' dv_old]|] eqn:Hdel.
+ iPoseProof (denv_delete_full_interp E) as "Hdel". eassumption.
iSpecialize ("Hdel" with "[Hm]"); iFrame.
iDestruct "Hdel" as "[HmDel Hl]".
iExists (dval_interp E dv_old). iFrame.
iIntros "Hl".
iExists E, dv2, (denv_insert i LLvl 1 dv2 m'); repeat (iSplit; first done).
iSplit. iPureIntro. apply denv_wf_insert; last done.
+ iExists (dloc_interp E (dLoc i)), (dval_interp E dv_old); iSplit; first done.
iPoseProof (denv_delete_full_interp E) as "Hdel". eassumption.
iSpecialize ("Hdel" with "[$Hm]"). iDestruct "Hdel" as "[HmDel Hl]"; iFrame.
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 mapsto_wand_list_spec.
iSpecialize ("Hwp" with "[Hm]"); iFrame.
iDestruct "Hwp" as (dv_old) "[Hl Hwp]"; fold wp_interp.
iExists (dval_interp E dv_old). iFrame.
iExists (dloc_interp E (dLoc i)), dv_old; iSplit; first done. iFrame.
iIntros "Hl". iSpecialize ("Hwp" with "Hl").
iExists E, dv2, []; repeat (iSplit; first done). unfold denv_interp. by iFrame.
- rewrite mapsto_wand_list_spec.
iSpecialize ("Hwp" with "[Hm]"); iFrame.
iDestruct "Hwp" as (dl ->) "Hwp"; fold wp_interp.
iDestruct "Hwp" as (dv) "[Hdv Hwp]"; fold wp_interp.
iExists (dloc_interp E dl); iSplit; first done.
iExists (dval_interp E dv). iFrame.
iDestruct "Hwp" as (l ->) "Hwp"; fold wp_interp.
iDestruct "Hwp" as (v) "[Hdv Hwp]"; fold wp_interp.
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. *) Admitted.
Qed.
(* Use `vcg_wp_unknown` in this spec to shorten it (and to get all the
conjunctions in the same order. *)
......@@ -458,22 +459,23 @@ Section vcg_spec.
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
E `prefix_of` E' dval_interp E' dv = v dval_wf E' 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 (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".
- 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) "(Hm & Hwp)".
iPoseProof (vcg_wp_load_correct E' m' with "Hm Hwp") as "Hload". done.
iIntros (v) "H". iDestruct "H" as (E' dv m' Hpre <- 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' <-) "(Hmf & Hwp)".
iExists Ef, dvf, mf. iFrame. by iSplit; first by iPureIntro; trans E'; done. done.
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.
- 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] dv1]|] eqn:Heqsp; last first.
......@@ -484,12 +486,20 @@ 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 "[-> HmOut]".
iDestruct 1 as (E' dw m' ? <- ?) "(% & Hm' & H)". iIntros "[-> HmOut]".
rewrite (dval_interp_mono E E') //.
iApply (vcg_wp_store_correct with "[Hm' HmOut] H");
eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
iApply denv_merge_interp. iFrame "Hm'". by iApply (denv_interp_mono with "HmOut").
+ specialize (vcg_sp_wf _ _ _ _ _ _ Hmwf Hwf1 Heqsp) as (H1 & H2 & Hwf).
iDestruct (vcg_sp_correct R with "Hm") as "[HmIn 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 "[-> HmOut]". iDestruct 1 as (E' d_new m' ? <- ?) "(% & Hm' & H)".
rewrite (dval_interp_mono E E') //.
iApply (vcg_wp_store_correct with "[Hm' HmOut] H");
eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
iApply denv_merge_interp. iFrame "Hm'". by iApply (denv_interp_mono with "HmOut").
+ admit.
- rewrite{1} /vcg_wp; fold vcg_wp.
simpl in Hwf; apply andb_prop_elim in Hwf; destruct Hwf as [Hwf1 Hwf2].
destruct (vcg_sp E m [] de1) as [[[mIn mOut] dv1]|] eqn:Heqsp; last first.
......@@ -501,12 +511,13 @@ 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 (-> & HmOut)".
iDestruct "Hex" as (E' dv1 m' Hpre <- Hm'wf) "(Hm' & Hwp)"; simplify_eq /=.
iDestruct "Hex" as (E' dv1 m' Hpre <- Hm'wf) "(% & Hm' & Hwp)"; simplify_eq /=.
specialize (dval_interp_mono _ _ _ Hwf Hpre) as ->.
specialize (denv_wf_mono _ _ _ H2 Hpre) as Hout_wf.
iPoseProof (denv_interp_mono with "HmOut") as "HmOut'"; [done | done |].
specialize (denv_wf_merge _ _ _ Hout_wf Hm'wf) as Hwfmerge.
specialize (denv_wf_merge _ _ _ Hout_wf H0) as Hwfmerge.
iApply (vcg_wp_bin_op_correct with "[Hm'] [Hwp] [HmOut']"); eauto.
by eapply dval_wf_mono.
+ iPoseProof (vcg_sp_correct R) as "Hsp". eassumption.
specialize (vcg_sp_wf _ _ _ _ _ _ Hmwf Hwf1 Heqsp) as (H1 & H2 & Hwf).
iDestruct ("Hsp" with "[$Hm]") as "[HmIn Hde1]"; iClear "Hsp"; clear Heqsp.
......@@ -514,45 +525,43 @@ Section vcg_spec.
iRename "HmIn" into "Hde2".
iApply (a_bin_op_spec with "[$Hde1] [$Hde2]"); fold dcexpr_interp.
iNext. iIntros (v1 v2) "(-> & HmOut) Hex".
iDestruct "Hex" as (E' dv2 m' Hpre <- Hm'wf) "(Hm' & Hwp)"; simplify_eq /=.
iDestruct "Hex" as (E' dv2 m' Hpre <- Hm'wf) "(% & Hm' & Hwp)"; simplify_eq /=.
specialize (dval_interp_mono _ _ _ Hwf Hpre) as ->.
specialize (denv_wf_mono _ _ _ H2 Hpre) as Hout_wf.
iPoseProof (denv_interp_mono with "HmOut") as "HmOut'"; [done | done |].
specialize (denv_wf_merge _ _ _ Hout_wf Hm'wf) as Hwfmerge.
specialize (denv_wf_merge _ _ _ Hout_wf H0) as Hwfmerge.
iApply (vcg_wp_bin_op_correct with "[Hm'] [Hwp] [HmOut']"); eauto.
- rewrite IHde; last done. iApply a_un_op_spec. iSpecialize ("Hm" with "Hwp").
by eapply dval_wf_mono.
- 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 <- 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.
iExists E', dw, m'; eauto with iFrame.
iExists E', dw, m'. apply dun_op_eval_dSome_wf in Hop; last done.
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.
iExists E', w, m'; eauto with iFrame.
+ 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.
iExists E', w, m'. apply dun_op_eval_dUnknown_wf in Hop; last done.
eauto with iFrame.
- simpl in Hwf; apply andb_prop_elim in Hwf as [Hwf1 Hwf2].
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'wf) "(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.
specialize (dcexpr_interp_mono E Enew de2 H1 Hpre).
iModIntro. rewrite IHde2 //. awp_seq. iSpecialize ("Hm" with "Hwp").
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. simpl in Hwf; apply andb_prop_elim in Hwf; destruct Hwf.
by eapply dcexpr_wf_mono in Hpre.
by apply denv_wf_unlock.
iFrame. by eapply dcexpr_wf_mono in Hpre. by apply denv_wf_unlock.
- by iApply (vcg_wp_unknown_correct with "Hm Hwp").
Admitted.
Qed.
Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E de :
MapstoListFromEnv Γs_in Γs_out Γls
......@@ -573,7 +582,7 @@ 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) "(-> & Hmwf & Hm & Hwp)".
iIntros (v) "H". iDestruct "H" as (E' dv m' Hpre) "(-> & % & % & Hm & Hwp)".
rewrite mapsto_wand_list_spec. iApply ("Hwp" with "Hm"). done.
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