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

working on correctness of vcg_wp for store

parent e9803281
......@@ -458,6 +458,14 @@ Section denv_spec.
denv_wf E m1 denv_wf E (denv_unlock m1).
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.
Lemma denv_wf_delete_full E dv i m m':
denv_wf E m denv_delete_full i m = Some (m', dv) denv_wf E m'.
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.
......
......@@ -194,12 +194,12 @@ Section vcg.
match vcg_sp E m [] de1 with
| Some (mIn, mOut, dv1) =>
vcg_wp E mIn de2 R (λ E mIn dv2,
vcg_wp_store E dv1 dv2 (denv_merge mOut mIn) (Φ E))
vcg_wp_store E dv1 dv2 mIn (Φ E))
| None =>
match vcg_sp E m [] de2 with
| Some (mIn, mOut, dv2) =>
vcg_wp E mIn de1 R (λ E mIn dv1,
vcg_wp_store E dv1 dv2 (denv_merge mOut mIn) (Φ E))
vcg_wp_store E dv1 dv2 mIn (Φ E))
| None => vcg_wp_unknown R E de m Φ
end
end
......@@ -425,30 +425,72 @@ Section vcg_spec.
iExists E, dv', []; 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
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
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.
destruct (dbin_op_eval E b dv1 dv2) as [ | dw | dw ] eqn:Hbin; first done.
* 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.
* destruct dw as [dw1|] eqn:Hdw; last done.
iExists (dval_interp E dw1); iSplit.
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.
Qed.
Lemma vcg_wp_bin_op_correct E0 E m mOut dv1 dv2 b Φ :
Lemma vcg_wp_store_correct E0 E m dv1 dv2 Φ :
E0 `prefix_of` E
denv_wf E (denv_merge mOut m)
denv_wf E m
dval_wf E dv2
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
denv_wf E' m' denv_interp E' m' wp_interp E' (Φ E' m' dv)).
wp_interp E (vcg_wp_store E dv1 dv2 m (Φ E)) -
l : loc, dval_interp E dv1 = #l
( v : val, l C v (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.
iIntros (Hpre Hwf) "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.
{ 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.
* destruct dw as [dw1|] eqn:Hdw; last done.
iExists (dval_interp E dw1); iSplit.
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.
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.
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.
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.
iIntros "Hl". iSpecialize ("Hwp" with "Hl").
iExists E, dv2, []; repeat (iSplit; first done). unfold denv_interp. by iFrame.
Qed.
Lemma vcg_wp_correct R E m de Φ :
dcexpr_wf E de
denv_wf E m
......@@ -471,7 +513,35 @@ Section vcg_spec.
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.
- 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.
+ destruct (vcg_sp E m [] de2) as [[[mIn mOut] dv2]|] eqn:Heqsp2; last first.
{ by iApply (vcg_wp_unknown_correct with "Hm Hwp"). }
iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
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 | done]. iSpecialize ("HmIn" with "Hwp").
iRename "HmIn" into "Hde1". simpl.
iApply (a_store_spec _ _
(λ l, v : val, l C v (l C[LLvl] dval_interp E dv2 -
E' dv m', E `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)))%I
with "[Hde1] [$Hde2]"); fold dcexpr_interp.
* iApply (awp_wand with "Hde1"). iIntros (v) "H".
iDestruct "H" as (E' dv1 m' Hpre Heq Hm'wf) "(Hm' & Hwp)"; simplify_eq /=.
specialize (dval_interp_mono _ _ _ Hwf Hpre) as ->.
specialize (denv_wf_mono _ _ _ H2 Hpre) as Hout_wf.
specialize (dval_wf_mono _ _ _ Hwf Hpre) as Hdval_wf.
specialize (denv_wf_merge _ _ _ Hout_wf Hm'wf) as Hwfmerge.
by iApply (vcg_wp_store_correct with "Hm' Hwp").
* iNext. by iIntros (l v2) "Hex (-> & HmOut)".
+ 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.
rewrite IHde2; [| done | done]. iSpecialize ("HmIn" with "Hwp").
iRename "HmIn" into "Hde2". simpl.
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.
......
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