Commit a7deb3f5 by Léon Gondelman

work in progress on vcg_wp_correct

parent 756fb75f
 ... ... @@ -49,7 +49,7 @@ Section denv. | S i => None :: denv_singleton i lv q dv end. Fixpoint denv_lookup (i : nat) (m: denv) : option (frac * dval) := Fixpoint denv_lookup (i : nat) (m : denv) : option (frac * dval) := match m with | [] => None | dio :: m' => ... ... @@ -129,12 +129,15 @@ Section denv. End denv. Section denv_spec. Context `{amonadG Σ}. Context `{amonadG Σ}. Lemma is_dloc_some E dv i: is_dloc E dv = Some i → dv = dLitV (dLitLoc (dLoc i)). Proof. destruct dv as [d|]; [destruct d|]; intros; simplify_eq /=. by destruct d; simplify_eq. Qed. Definition denv_interp (L : known_locs) (m : denv) : iProp Σ := ([∗ list] i ↦ dio ∈ m, from_option (λ '(DenvItem lv q dv), dloc_interp L (dLoc i) ↦C[lv]{q} dval_interp L dv) True dio)%I. dloc_interp L (dLoc i) ↦C[lv]{q} dval_interp L dv) True dio)%I. Definition penv_interp (m : penv) : iProp Σ := ([∗ list] p ∈ m, penv_loc p ↦C[penv_level p]{penv_frac p} penv_val p)%I. ... ... @@ -144,6 +147,10 @@ Section denv_spec. ⊣⊢ denv_interp E m ∗ dloc_interp E (dLoc i) ↦C[x]{q} dval_interp E dv. Proof. Admitted. Lemma denv_lookup_interp i q dv m: denv_lookup i m = Some (q, dv) → exists m', m = (denv_insert i ULvl q dv m'). Proof. Admitted. (* RK: this only holds in one direction *) Lemma denv_merge_interp E m1 m2 : denv_interp E m1 ∗ denv_interp E m2 ⊣⊢ denv_interp E (denv_merge m1 m2). ... ...
 ... ... @@ -187,7 +187,7 @@ Section vcg. match de with | dCRet dv => Φ E m dv | dCLoad de1 => vcg_wp E m de1 R (λ E m' dv, vcg_wp_load E dv m (Φ E)) vcg_wp E m de1 R (λ E m' dv, vcg_wp_load E dv m' (Φ E)) | dCStore de1 de2 => match vcg_sp E m [] de1 with | Some (mIn, mOut, dv1) => ... ... @@ -354,25 +354,83 @@ Section vcg_spec. iApply "Hawp". by rewrite /denv_interp. Qed. Lemma vcg_wp_unknown_correct R E m de Φ : denv_interp E m -∗ wp_interp E (vcg_wp_unknown R E de m Φ) -∗ awp (dcexpr_interp E de) R (λ v, ∃ E' dv m', ⌜dval_interp E' dv = v⌝ ∧ 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"). iApply (awp_wand with "Hwp"). iIntros (v) "H". iDestruct "H" as (E' m' dv ->) "(Hpre & Hm & Hwp)". rewrite wp_interp_sane_sound. iExists E', dv, m'. iSplit; first done; iFrame. Qed. Lemma vcg_wp_correct R E m de Φ : denv_interp E m -∗ wp_interp E (vcg_wp E m de R Φ) -∗ awp (dcexpr_interp E de) R (λ v, ∃ E' dv m', ⌜dval_interp E dv = v⌝ ∧ wp_interp E (Φ E' m' dv)). Proof. Admitted. (* revert Φ m. induction de; intros Φ m. - iIntros "Hd". iApply awp_ret. wp_value_head. eauto. - iIntros "Hawp". iApply (awp_wand with "Hawp"). iIntros (v) "H". rewrite wp_interp_sane_sound. iExists _,_; iFrame; eauto. - iIntros "Hd". rewrite (IHde _ _). iApply (a_load_spec_exists_frac with "[Hd]"). iApply (awp_wand with "Hd"). iIntros (?). iDestruct 1 as (dv m' <-) "Hd /=". iDestruct "Hd" as (dl ?) "Hd". iDestruct "Hd" as (q dw) "H". iExists (dloc_interp E dl), q, (dval_interp E dw); iSplit; first done. iDestruct "H" as "[Hl Hwp]". iFrame. iIntros "Hd". iExists _, _; iSplit; first done. by iApply "Hwp". - iIntros "H". simpl. destruct (vcg_sp E m de1) as [[[mIn mOut] dv]|] eqn:Heqsp; last first. { destruct (vcg_sp E m de2) as [[[mIn mOut] dv]|] eqn:Heqsp2; last first. { iApply (awp_wand with "H"). iIntros (v) "H". iExists (dValUnknown v). eauto 30 with iFrame. } (λ v, ∃ E' dv m', ⌜dval_interp E' dv = v⌝ ∧ denv_interp E' m' ∗ wp_interp E' (Φ E' m' dv)). Proof. revert Φ m. induction de; intros Φ m; iIntros "Hm". - iIntros "Hd". iApply awp_ret. wp_value_head. iExists E, d, m. iSplit; first done; iFrame. - iIntros "Hawp". iApply (vcg_wp_unknown_correct with "Hm Hawp"). - iIntros "Hd". rewrite IHde. iSpecialize ("Hm" with "Hd"). simpl. iApply (a_load_spec_exists_frac with "[Hm]"). iApply (awp_wand with "Hm"). iIntros (v) "H". iDestruct "H" as (E' dv m' <-) "(Hm & Hwp)". 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 /=. * apply (denv_lookup_interp i q dv' m') in Hlkp. apply is_dloc_some in Hdloc. destruct Hlkp as [m0 Hlkp]. subst. iExists (dloc_interp E' (dLoc i)), q, (dval_interp E' dv'). rewrite denv_insert_interp. iDestruct "Hm" as "[Hm0 Hi]". iFrame. iSplit. simplify_eq /=; done. iIntros "Hl". iExists E', dv', (denv_insert i ULvl q dv' m0); iSplit; first done. iFrame. rewrite denv_insert_interp. iFrame. * rewrite mapsto_wand_list_spec. 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. by unfold denv_interp. + rewrite mapsto_wand_list_spec. 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. by unfold denv_interp. Admitted. (* - iIntros "H". rewrite /vcg_wp. destruct (vcg_sp E m [] de1) as [[[mIn mOut] dv]|] eqn:Heqsp; last first. { destruct (vcg_sp E m [] de2) as [[[mIn mOut] dv]|] eqn:Heqsp2; last first. { iApply (vcg_wp_unknown_correct with "[\$Hm] [\$H]"). } fold vcg_wp. iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption. iDestruct ("Hsp" with "Hm") as "[Hm Hde2]". iClear "Hsp". clear Heqsp2 Heqsp. rewrite IHde1. iSpecialize ("Hm" with "H"). iApply (a_store_spec _ _ (λ l, ∃ (E' : known_locs) (dv0 : dval) (m' : denv), ⌜dval_interp E' dv0 = #l⌝ ∧ denv_interp E' m' ∗ wp_interp E' (vcg_wp_store E' dv0 dv (denv_merge mOut m') (Φ E')) )%I (λ v : val, ⌜v = dval_interp E dv⌝ ∧ denv_interp E mOut)%I with "[Hm] [\$Hde2]"); fold dcexpr_interp. * iApply (awp_wand with "Hm"). iIntros (v) "H". iDestruct "H" as (E' dv1 m') "(<- & Hdv1 & Hwp)". unfold vcg_wp_store. destruct (is_dloc E' dv1) as [i|] eqn:Hdloc. ** apply is_dloc_some in Hdloc. subst. iExists (dloc_interp E' (dLoc i)); iSplit; first done. destruct (denv_delete_full i (denv_merge mOut m')) as [[m'0 dv_old]|] eqn:Hdel; simplify_eq/=. *** apply (denv_delete_full_interp E') in Hdel. rewrite denv_insert_interp. rewrite IHde; last done. iDestruct "HmIn" as "[HmIn1 Hawp]". admit. * admit. (*wp_interp E' (MapstoStarFull (dLoc i) (λ _ : dval, MapstoWand (dLoc i) dv LLvl 1 (Φ E' [] dv)))*) * rewrite IHde1. } fold vcg_wp. iApply (awp_wand with "H"). iIntros (v) "H". iExists (dValUnknown v). eauto 30 with iFrame. } rewrite mapsto_star_list_spec. iDestruct "H" as "[Henv Hde1]". rewrite mapsto_wand_list_spec IHde1. iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption. iDestruct ("Hsp" with "Henv") as "[Hm1 Hde2]". iSpecialize ("Hde1" with "Hm1"). ... ...
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