Commit 44d3bd53 by Léon Gondelman

### work in progress on vcg_wp_correct

parent e813e722
 ... ... @@ -383,37 +383,47 @@ Section vcg_spec. iExists E', dv, m'. iSplit; first done; iFrame. Qed. Lemma vcg_wp_load_correct E m dv Φ : 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', ⌜dval_interp E' dv' = w⌝ ∧ denv_interp E' m' ∗ wp_interp E' (Φ E' m' dv')). 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 /=. * apply (denv_lookup_interp i q dv' m) in Hlkp. apply is_dloc_some in Hdloc. destruct Hlkp as [m0 Hlkp]. subst. iIntros "Hm Hwp". iExists (dloc_interp E (dLoc i)), q, (dval_interp E dv'). rewrite denv_insert_interp. iDestruct "Hm" as "[Hm0 Hi]". iFrame. iSplit. by simplify_eq /=. iIntros "Hl". iExists E, dv', (denv_insert i ULvl q dv' m0); iSplit; first done. rewrite denv_insert_interp. iFrame. * rewrite mapsto_wand_list_spec. iIntros "Hm Hwp". 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. iIntros "Hm Hwp". 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. 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⌝ ∧ 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. revert Φ m. induction de; intros Φ m; iIntros "Hm Hwp". - iApply awp_ret. wp_value_head. iExists E, d, m. iSplit; first done; iFrame. - iApply (vcg_wp_unknown_correct with "Hm Hwp"). - rewrite IHde. iSpecialize ("Hm" with "Hwp"); 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. iApply (vcg_wp_load_correct with "Hm Hwp"). 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. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!