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

wip on proving vcg_wp

parent cf9e2c98
......@@ -131,9 +131,10 @@ Section vcg.
| dCStore de1 de2 =>
match vcg_sp E m de1 with
| Some (mIn, mOut, dv1) =>
mapsto_star_list m (vcg_wp E mIn de2 R (λ dv2,
mapsto_wand_list (denv_merge mIn mOut)
(IsLoc dv1 (λ dl, MapstoStar dl 1%Qp (λ _, (MapstoWand dl dv2 LLvl 1%Qp (Φ dv2)))))))
IsLoc dv1 (λ dl,
(mapsto_star_list m (vcg_wp E mIn de2 R (λ dv2,
mapsto_wand_list (denv_merge mIn mOut)
(MapstoStar dl 1%Qp (λ _, (MapstoWand dl dv2 LLvl 1%Qp (Φ dv2))))))))
| None =>
match vcg_sp E m de2 with
| Some (mIn, mOut, dv2) =>
......@@ -322,12 +323,9 @@ Section vcg_spec.
wp_interp E (vcg_wp E m de R Φ)
awp (dcexpr_interp E de) R (λ v, dv, dval_interp E dv = v wp_interp E (Φ dv)).
Proof.
Admitted.
(* revert Φ s. induction de; simpl; intros Φ s.
- iIntros "Hd". iApply awp_ret. wp_value_head.
iExists d. eauto.
- iIntros "Hd".
iApply a_load_spec.
revert Φ m. induction de; simpl; intros Φ m.
- iIntros "Hd". iApply awp_ret. wp_value_head. iExists d. eauto.
- iIntros "Hd". iApply a_load_spec.
rewrite IHde.
iApply (awp_wand with "Hd").
iIntros (?). iDestruct 1 as (dv <-) "Hd /=".
......@@ -336,9 +334,29 @@ Section vcg_spec.
iExists _,_; iFrame. iSplit; eauto.
iIntros "H". iExists _. iSplit; eauto.
by iApply "Hd".
- iIntros "H". iApply (awp_wand with "H").
iIntros (v) "H". iExists (dValUnknown v).
eauto 30 with iFrame.
- iIntros "H".
remember (vcg_sp E m de1) as sp. symmetry in Heqsp.
destruct sp as [[[mIn mOut] dv]|].
+ simpl. iDestruct "H" as (dl) "[Hdl H]". iDestruct "Hdl" as %Hdl.
rewrite mapsto_star_list_spec.
iDestruct "H" as "[Hm Hde2]".
rewrite IHde2.
iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
iDestruct ("Hsp" with "Hm") as "[HmIn Hde1]".
iApply (a_store_spec _ _ (λ l, l = dloc_interp E dl denv_interp E mOut)%I with "[Hde1] Hde2").
{ iApply (awp_wand with "Hde1").
iIntros (v) "[% $]". simplify_eq/=. rewrite Hdl. eauto. }
iNext. iIntros (l w) "[% HmOut] Hex". simplify_eq/=.
iDestruct "Hex" as (? <-) "Hwp".
rewrite mapsto_wand_list_spec.
rewrite -denv_merge_interp.
iSpecialize ("Hwp" with "[$HmIn $HmOut]"). simpl.
iDestruct "Hwp" as (w) "(Hl & Hwp)".
iExists (dval_interp E w). iFrame.
iIntros "Hl". iExists _; iSplit; eauto.
by iApply "Hwp".
+ admit.
(*
- iIntros "H".
remember (vcg_sp E s de1) as sp. symmetry in Heqsp.
destruct sp as [[[s1 s2] dv]|]; last first.
......@@ -363,7 +381,7 @@ Section vcg_spec.
iSplit.
iPureIntro. by apply dbin_op_eval_correct.
eauto with iFrame.
Qed. *)
Qed. *) Admitted.
Lemma optimize_sound (m: denv) E (Φ: wp_expr) :
......
Supports Markdown
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