Commit b8549d28 by Robbert Krebbers

### Hack on store case in wp.

parent e11d1407
 ... ... @@ -86,34 +86,35 @@ Section proofs. Qed. Lemma a_store_spec R Φ Ψ1 Ψ2 e1 e2 : awp e1 R (λ v, ∃ l : loc, ⌜v = #l⌝ ∧ Ψ1 l)-∗ awp e1 R Ψ1 -∗ awp e2 R Ψ2 -∗ ▷ (∀ (l : loc) w, Ψ1 l -∗ Ψ2 w -∗ (∃ v, l ↦C v ∗ (l ↦C[LLvl] w -∗ Φ w))) -∗ ▷ (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ ∃ (l : loc) w, ⌜ v1 = #l ⌝ ∧ l ↦C w ∗ (l ↦C[LLvl] v2 -∗ Φ v2)) -∗ awp (a_store e1 e2) R Φ. Proof. iIntros "H1 H2 HΦ". awp_apply (a_wp_awp with "H1"); iIntros (v1) "H1". awp_lam. awp_apply (a_wp_awp with "H2"); iIntros (v2) "H2". awp_lam. iApply awp_bind. iApply (awp_par with "H1 H2"). iIntros "!>" (w1 w2) "H1 H2 !>". iDestruct "H1" as (l ->) "H1". awp_lam. iDestruct ("HΦ" with "H1 H2") as (v) "[Hv HΦ]". iIntros "!>" (w1 w2) "H1 H2 !>". awp_lam. iDestruct ("HΦ" with "H1 H2") as (l w ->) "[Hl HΦ]". iApply awp_atomic_env. iIntros (env) "Henv HR". rewrite {2}/env_inv. iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)". iDestruct "Hlocks" as %Hlocks. iDestruct (locked_locs_unlocked with "Hv Hσ") as %Hl. iDestruct (locked_locs_unlocked with "Hl Hσ") as %Hl. assert (#l ∉ X). { unfold correct_locks in *. intros Hx. apply Hl. destruct (Hlocks _ Hx) as [l' [? Hl']]. by simplify_eq/=. } wp_let. wp_proj. wp_apply (mset_add_spec with "[\$HX]"); eauto. iIntros "HX". wp_seq. iDestruct (full_locking_heap_unlocked with "Hv Hσ") as %?. iMod (locking_heap_change_lock _ _ ULvl LLvl with "Hσ Hv") as "[Hσ Hv]". iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %?. iMod (locking_heap_change_lock _ _ ULvl LLvl with "Hσ Hl") as "[Hσ Hl]". do 2 wp_proj. rewrite mapsto_eq /mapsto_def. iDestruct "Hv" as (b') "(Hb' & Hv & Hl)". iDestruct "Hl" as (b') "(Hb' & Hv & Hl)". rewrite (big_sepM_lookup_acc _ _ l ULvl); last done. iDestruct "Hls" as "[Hl' Hls]". iDestruct "Hl'" as (?) "Hl'". ... ...
 ... ... @@ -13,11 +13,9 @@ TODO - Write more tests with unknown stuff in it add tests like `!(l := 10;;;; l)` - Support alloc in `vcg_wp` - Automatically come up with the new `E`, `m` and `dv` and stuff in the unknown case - Automatically come up with the new `E`, `m` and `dv` and stuff in the unknown case - Finish the proofs - Maybe drop `wp_expr`? We are not taking it as an input of anything anymore - Maybe generate vcg_unknown in the cases None and '_' in vcg_store and vcg_load Less urgent TODO ... ... @@ -194,12 +192,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 mIn (Φ E)) vcg_wp_store E dv1 dv2 (denv_merge mOut 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 mIn (Φ E)) vcg_wp_store E dv1 dv2 (denv_merge mOut mIn) (Φ E)) | None => vcg_wp_unknown R E de m Φ end end ... ... @@ -275,12 +273,12 @@ Section vcg_spec. iIntros "H1 H2". iApply (mapsto_wand_list_aux_spec with "H1 H2"). Qed. Lemma vcg_sp_correct' E de mIn mOut mIn' mOut' dv R : Lemma vcg_sp_correct' R E de mIn mOut mIn' mOut' dv : vcg_sp E mIn mOut de = Some (mIn', mOut', dv) → 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. ... ... @@ -359,9 +357,9 @@ Section vcg_spec. iIntros (?) "[_ HmOut1]". rewrite (denv_unlock_interp E mOut1). iModIntro. iSpecialize ("Hawp2" with "HmOut1"). awp_seq. iApply "Hawp2". Qed. Qed. *) Admitted. Lemma vcg_sp_correct E de m mIn mOut dv R : Lemma vcg_sp_correct R E de m mIn mOut dv : vcg_sp E m [] de = Some (mIn, mOut, dv) → denv_interp E m -∗ denv_interp E mIn ∗ awp (dcexpr_interp E de) R (λ v, ⌜v = dval_interp E dv⌝ ∧ denv_interp E mOut). ... ... @@ -454,15 +452,15 @@ Section vcg_spec. dval_wf E dv2 → denv_interp E m -∗ 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 -∗ ∃ (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. ⌜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. 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. ... ... @@ -487,11 +485,11 @@ Section vcg_spec. 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. Qed. *) Admitted. Lemma vcg_wp_correct R E m de Φ : (* Use `vcg_wp_unknown` in this spec to shorten it (and to get all the conjunctions in the same order. *) Lemma vcg_wp_correct R E m de Φ : dcexpr_wf E de → denv_wf E m → denv_interp E m -∗ ... ... @@ -514,40 +512,27 @@ Section vcg_spec. 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. - rewrite{1} /vcg_wp; fold vcg_wp. simpl in Hwf; apply andb_prop_elim in Hwf; destruct Hwf as [Hwf1 Hwf2]. 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. + 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. iDestruct (vcg_sp_correct R with "Hm") as "[HmIn Hde2]"; first done. 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]". 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. + 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. 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"). ... ... @@ -559,7 +544,7 @@ Section vcg_spec. iPoseProof (denv_interp_mono with "HmOut") as "HmOut'"; [done | done |]. specialize (denv_wf_merge _ _ _ Hout_wf Hm'wf) as Hwfmerge. iApply (vcg_wp_bin_op_correct with "[Hm'] [Hwp] [HmOut']"); eauto. + iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption. + 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"). ... ... @@ -604,7 +589,7 @@ Section vcg_spec. by eapply dcexpr_wf_mono in Hpre. by apply denv_wf_unlock. - by iApply (vcg_wp_unknown_correct with "Hm Hwp"). Admitted. Admitted. Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E de : MapstoListFromEnv Γs_in Γs_out Γls → ... ... @@ -628,7 +613,6 @@ Section vcg_spec. iIntros (v) "H". iDestruct "H" as (E' dv m' Hpre) "(-> & Hmwf & Hm & Hwp)". rewrite mapsto_wand_list_spec. iApply ("Hwp" with "Hm"). done. Qed. End vcg_spec. Arguments wp_interp : simpl never. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!