vcgen.v 15.2 KB
 Dan Frumin committed Jun 07, 2018 1 ``````From iris.heap_lang Require Export proofmode notation. `````` Dan Frumin committed Jun 08, 2018 2 ``````From iris.algebra Require Import frac. `````` Dan Frumin committed Jun 07, 2018 3 ``````From iris.bi Require Import big_op. `````` 4 ``````From iris_c.vcgen Require Import dcexpr env splitenv. `````` Dan Frumin committed Jun 07, 2018 5 6 7 ``````From iris_c.c_translation Require Import monad translation proofmode. From iris_c.lib Require Import locking_heap U. `````` Robbert Krebbers committed Jun 13, 2018 8 9 10 11 12 13 ``````(* TODO: Inductive dfrac := | dFrac : frac → dfrac | dFracUnknown : nat → nat → frac → dfrac. *) `````` Léon Gondelman committed Jun 08, 2018 14 15 16 17 18 19 20 `````` (*TODO: Understand how to correctly deal with levels and fractions in - exhale_list, i.e., what are levels and fractions of those ressources that are given in the very end to the postcondition - computations of vcg_sp, i.e. what are levels and fractions given back `````` Dan Frumin committed Jun 08, 2018 21 22 23 24 25 26 `````` by vcg_sp in case of load and store - Add ExistsFracLevel to wp_expr ExistsFracLevel Φ ~ ∃ q x, Φ q x - Add levels to env_ps/env_ps_dv - Deep embedding of fractions *) `````` Léon Gondelman committed Jun 08, 2018 27 `````` `````` Dan Frumin committed Jun 07, 2018 28 29 30 ``````Section vcg. Context `{amonadG Σ}. `````` 31 32 `````` (** Deep embedding of formulae used to build the verification condition generator *) `````` Robbert Krebbers committed Jun 13, 2018 33 `````` (** TODO: remove Par *) `````` Léon Gondelman committed Jun 07, 2018 34 `````` Inductive wp_expr := `````` Dan Frumin committed Jun 07, 2018 35 `````` | Base : iProp Σ → wp_expr `````` Léon Gondelman committed Jun 08, 2018 36 `````` | Inhale : dloc → frac → (dval → wp_expr) → wp_expr `````` Léon Gondelman committed Jun 11, 2018 37 `````` | InhaleKnown : dloc → dval → level → frac → wp_expr → wp_expr `````` Léon Gondelman committed Jun 11, 2018 38 `````` | Exhale : dloc → dval → level → frac → wp_expr → wp_expr `````` Dan Frumin committed Jun 07, 2018 39 40 41 42 `````` | IsSome {A} : doption A → (A → wp_expr) → wp_expr | IsLoc : dval → (dloc → wp_expr) → wp_expr | UMod : wp_expr → wp_expr | Par : `````` Dan Frumin committed Jun 08, 2018 43 44 `````` ((val → iProp Σ) → wp_expr) → ((val → iProp Σ) → wp_expr) → `````` Dan Frumin committed Jun 07, 2018 45 `````` (dval → dval → wp_expr) → wp_expr. `````` Dan Frumin committed Jun 08, 2018 46 `````` Arguments Base _%I. `````` Dan Frumin committed Jun 07, 2018 47 `````` `````` Léon Gondelman committed Jun 08, 2018 48 `````` Fixpoint wp_interp (E : env_locs) (a : wp_expr) : iProp Σ := `````` Dan Frumin committed Jun 07, 2018 49 50 `````` match a with | Base P => P `````` Léon Gondelman committed Jun 08, 2018 51 52 `````` | Inhale dl q Φ => ∃ dv, dloc_interp E dl ↦U{q} dval_interp E dv ∗ wp_interp E (Φ dv) `````` Léon Gondelman committed Jun 11, 2018 53 54 55 56 `````` | InhaleKnown dl dv x q Φ => mapsto (dloc_interp E dl) x q (dval_interp E dv) ∗ wp_interp E Φ | Exhale dl dv x q Φ => mapsto (dloc_interp E dl) x q (dval_interp E dv) -∗ wp_interp E Φ `````` Dan Frumin committed Jun 07, 2018 57 58 59 60 `````` | IsSome dmx Φ => ∃ x, ⌜doption_interp dmx = Some x⌝ ∧ wp_interp E (Φ x) | IsLoc dv Φ => ∃ dl : dloc, ⌜dval_interp E dv = #(dloc_interp E dl)⌝ ∧ wp_interp E (Φ dl) | UMod P => U (wp_interp E P) `````` Dan Frumin committed Jun 08, 2018 61 `````` | Par P1 P2 P3 => ∃ (Ψ1 Ψ2 : val → iProp Σ), `````` Dan Frumin committed Jun 07, 2018 62 63 `````` wp_interp E (P1 Ψ1) ∗ wp_interp E (P2 Ψ2) ∗ `````` Dan Frumin committed Jun 08, 2018 64 `````` ∀ (v1 v2 : val), Ψ1 v1 -∗ Ψ2 v2 -∗ wp_interp E (P3 (dValUnknown v1) (dValUnknown v2)) `````` Léon Gondelman committed Jun 08, 2018 65 `````` end%I. `````` Dan Frumin committed Jun 07, 2018 66 `````` `````` Léon Gondelman committed Jun 08, 2018 67 `````` Fixpoint wp_interp_sane (E : env_locs) (a : wp_expr) : iProp Σ := `````` Dan Frumin committed Jun 07, 2018 68 69 `````` match a with | Base Φ => Φ `````` Léon Gondelman committed Jun 08, 2018 70 71 `````` | Inhale dl q Φ => ∃ v, dloc_interp E dl ↦U{q} v ∗ wp_interp_sane E (Φ (dValUnknown v)) `````` Léon Gondelman committed Jun 11, 2018 72 73 74 75 `````` | InhaleKnown dl dv x q Φ => mapsto (dloc_interp E dl) x q (dval_interp E dv) ∗ wp_interp_sane E Φ | Exhale dl dv x q Φ => mapsto (dloc_interp E dl) x q (dval_interp E dv) -∗ wp_interp_sane E Φ `````` Dan Frumin committed Jun 07, 2018 76 77 78 79 80 81 `````` | IsSome dmx Φ => ∃ x, ⌜doption_interp dmx = Some x⌝ ∧ wp_interp_sane E (Φ x) | IsLoc dv Φ => ∃ l : loc, ⌜dval_interp E dv = #l⌝ ∧ wp_interp_sane E (Φ (dLocUnknown l)) | UMod P => U (wp_interp_sane E P) | Par P1 P2 P3 => ∃ Ψ1 Ψ2 : val → iProp Σ, `````` Dan Frumin committed Jun 08, 2018 82 83 `````` wp_interp_sane E (P1 Ψ1) ∗ wp_interp_sane E (P2 Ψ2) ∗ `````` Dan Frumin committed Jun 07, 2018 84 85 86 87 88 89 90 91 92 93 `````` ∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ wp_interp_sane E (P3 (dValUnknown v1) (dValUnknown v2)) end%I. Lemma wp_interp_sane_sound E a : wp_interp_sane E a ⊢ wp_interp E a. Proof. generalize dependent E. induction a. - done. - simpl. iIntros (E) "He". iDestruct "He" as (v) "[H1 H2]". iExists (dValUnknown v). simpl. iFrame. by iApply H0. `````` Léon Gondelman committed Jun 11, 2018 94 `````` - simpl. iIntros (E) "(He & H)". iFrame. by iApply IHa. `````` Dan Frumin committed Jun 07, 2018 95 96 97 98 99 100 101 102 `````` - simpl. iIntros (E) "He H". iApply IHa. by iApply "He". - simpl. iIntros (E) "He". iDestruct "He" as (v) "[H1 H2]". iExists v. iFrame. by iApply H0. - simpl. iIntros (E) "He". iDestruct "He" as (l) "[H1 H2]". iExists (dLocUnknown l). simpl. iFrame. by iApply H0. - simpl. intros E. by apply U_mono. - simpl. intros E. iDestruct 1 as (Ψ1 Ψ2) "(HΨ1 & HΨ2 & HΦ)". `````` Dan Frumin committed Jun 08, 2018 103 `````` iExists _,_. `````` Dan Frumin committed Jun 07, 2018 104 105 `````` iSplitL "HΨ1". by iApply H0. iSplitL "HΨ2". by iApply H1. `````` Dan Frumin committed Jun 08, 2018 106 107 `````` iIntros (v1 v2) "Hv1 Hv2". iApply H2. iApply ("HΦ" with "Hv1 Hv2"). `````` Dan Frumin committed Jun 07, 2018 108 109 `````` Qed. `````` 110 `````` Fixpoint append_exhale_list (ps : env_ps_dv) (Φ : wp_expr) : wp_expr := `````` Léon Gondelman committed Jun 08, 2018 111 `````` match ps with `````` 112 `````` | (i, ((x,q), dv)) :: s' => Exhale (dLoc i) dv x q (append_exhale_list s' Φ) `````` Léon Gondelman committed Jun 08, 2018 113 114 115 `````` | [] => Φ end. `````` Léon Gondelman committed Jun 11, 2018 116 117 118 119 120 121 `````` Fixpoint append_inhale_list (ps : env_ps_dv) (Φ : wp_expr) : wp_expr := match ps with | (i, ((x,q), dv)) :: s' => InhaleKnown (dLoc i) dv x q (append_inhale_list s' Φ) | [] => Φ end. `````` 122 `````` Lemma vcg_inhale_list_sound E s t : `````` Léon Gondelman committed Jun 11, 2018 123 124 125 126 127 128 129 130 `````` wp_interp E (append_inhale_list s t) -∗ env_ps_dv_interp E s ∗ wp_interp E t. Proof. unfold env_ps_dv_interp. induction s as [| [i [[x q] w]] s']; simpl. - by iIntros "\$ _". - iIntros "[H1 H2]". iFrame "H1". by iApply (IHs' with "H2"). Qed. `````` 131 132 `````` Lemma vcg_exhale_list_sound E s t : wp_interp E (append_exhale_list s t) -∗ env_ps_dv_interp E s -∗ wp_interp E t. `````` Léon Gondelman committed Jun 08, 2018 133 `````` Proof. `````` Léon Gondelman committed Jun 11, 2018 134 135 `````` unfold env_ps_dv_interp. induction s as [| [i [[x q] w]] s']; simpl. `````` Léon Gondelman committed Jun 08, 2018 136 137 138 139 140 `````` - by iIntros "\$ _". - iIntros "H [H1 H2]". iSpecialize ("H" with "H1"). iApply (IHs' with "H H2"). Qed. `````` 141 142 143 `````` (* vcg_sp E s de = Some (s1, s2, dv) `````` Dan Frumin committed Jun 08, 2018 144 145 146 `````` - s1 = s / resources for de - s2 = new resources that you get from de *) `````` Léon Gondelman committed Jun 08, 2018 147 `````` Fixpoint vcg_sp (E: env_locs) (s: env_ps_dv) (de : dcexpr) : `````` Dan Frumin committed Jun 08, 2018 148 `````` option (env_ps_dv * env_ps_dv * dval) := `````` Léon Gondelman committed Jun 08, 2018 149 `````` match de with `````` Dan Frumin committed Jun 09, 2018 150 `````` | dCVal dv => Some (s, nil, dv) `````` Léon Gondelman committed Jun 08, 2018 151 `````` | dCLoad de1 => `````` 152 `````` ''(s1, s2, dv1) ← vcg_sp E s de1; `````` 153 154 `````` i ← is_dloc E dv1; ''(s1', ((x, q), dv2)) ← find_and_remove s1 (dLoc i); `````` 155 `````` if (bool_decide (x = ULvl)) `````` Léon Gondelman committed Jun 11, 2018 156 157 `````` then (* NB: 'x' can be a Coq variable, so here we can't check that 'x' is Ulvl *) `````` 158 `````` Some ((i, ((x, (q/2)%Qp), dv2)) :: s1', (i, ((x, (q/2)%Qp), dv2)) :: s2, dv2) `````` Léon Gondelman committed Jun 11, 2018 159 `````` else None `````` Léon Gondelman committed Jun 08, 2018 160 `````` | dCStore de1 de2 => `````` Léon Gondelman committed Jun 11, 2018 161 162 `````` ''(s1, s2, dv1) ← vcg_sp E s de1; i ← is_dloc E dv1; `````` 163 164 165 166 `````` ''(s1', s2', dv2) ← vcg_sp E s1 de2; (* we can't use s1 below any more *) ''(s1'', s2'', ((x, q), _)) ← find_and_remove_2 s1' (s2 ++ s2') (dLoc i); (* NB: this should be fixed, adding 'q' & 'x' to env *) `````` 167 `````` if (bool_decide (q = Qp_one) && bool_decide (x = ULvl)) `````` 168 `````` then Some (s1'', (i, ((LLvl, 1%Qp), dv2)) :: s2'', dv2) `````` 169 `````` else None `````` Léon Gondelman committed Jun 08, 2018 170 `````` | dCBinOp op de1 de2 => `````` Léon Gondelman committed Jun 11, 2018 171 `````` ''(s1, s2, dv1) ← vcg_sp E s de1; `````` Dan Frumin committed Jun 08, 2018 172 173 `````` ''(s1', s2', dv2) ← vcg_sp E s1 de2; match dbin_op_eval E op dv1 dv2 with `````` Léon Gondelman committed Jun 11, 2018 174 `````` | dSome dv => Some (s1', s2 ++ s2', dv) `````` Robbert Krebbers committed Jun 13, 2018 175 176 `````` (* | dUnknown (Some dv) => Some (s1', s2 ++ s2', dv) (*TODO: not sure here *) RK: probably just fail with None *) `````` Léon Gondelman committed Jun 11, 2018 177 `````` | dNone | dUnknown _ => None `````` Dan Frumin committed Jun 08, 2018 178 `````` end `````` Léon Gondelman committed Jun 08, 2018 179 180 `````` end. `````` 181 182 `````` Lemma vcg_sp_correct E s de ps1 ps2 dv R : vcg_sp E s de = Some (ps1, ps2, dv) → `````` Léon Gondelman committed Jun 11, 2018 183 `````` env_ps_dv_interp E s -∗ `````` 184 185 `````` env_ps_dv_interp E ps1 ∗ awp (dcexpr_interp E de) R (λ v, ⌜v = dval_interp E dv⌝ ∧ env_ps_dv_interp E ps2). `````` Dan Frumin committed Jun 09, 2018 186 `````` Proof. `````` 187 188 `````` revert s ps1 ps2 dv. induction de; iIntros (s ps1 ps2 dv Hsp) "Hs"; simplify_eq/=. `````` Léon Gondelman committed Jun 11, 2018 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 `````` - iFrame. iApply awp_ret. wp_value_head. iSplit; eauto. unfold env_ps_dv_interp. done. - specialize (IHde s). destruct (vcg_sp E s de) as [[[s1' s2'] dv1]|]; simplify_eq /=. destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=. destruct d as [l|?]; simplify_eq/=. remember (find_and_remove s1' (dLoc l)) as Hfar. destruct Hfar as [[s1'' [[x q] dv'']]|]; simplify_eq/=. case_bool_decide; simplify_eq/=. rewrite IHde; last done. iDestruct "Hs" as "[Hs1' Hawp]". rewrite find_and_remove_env_ps_dv_interp; last done. iDestruct "Hs1'" as "[Hs1'' [Hl1 Hl2]]". iFrame "Hl1 Hs1''". iApply a_load_spec. iApply (awp_wand with "Hawp"). iIntros (?) "[% Hs2']". simplify_eq/=. iExists _, _. iSplit; eauto. iFrame "Hl2". iIntros "Hl2". iSplit; eauto. by iFrame. `````` 206 207 `````` - specialize (IHde1 s). destruct (vcg_sp E s de1) as [[[s1 s2] dv1]|]; simplify_eq /=. `````` Léon Gondelman committed Jun 11, 2018 208 209 `````` destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=. destruct d as [l|?]; simplify_eq/=. `````` 210 211 212 213 214 215 216 217 218 219 `````` specialize (IHde2 s1). destruct (vcg_sp E s1 de2) as [[[s1' s2'] dv2]|]; simplify_eq /=. remember (find_and_remove_2 s1' (s2++s2') (dLoc l)) as Hfar. destruct Hfar as [[[s1'' s2''] [[x q] dv'']]|]; simplify_eq/=. repeat (case_bool_decide; simplify_eq/=). rewrite IHde1; last done. iDestruct "Hs" as "[Hs1 Hawp1]". rewrite IHde2; last done. iDestruct "Hs1" as "[Hs1' Hawp2]". rewrite find_and_remove_2_env_ps_dv_interp; last done. iDestruct "Hs1'" as "[\$ Hl]". iApply (a_store_spec _ _ (λ j, ⌜j = dloc_interp E (dLoc l)⌝ ∧ env_ps_dv_interp E s2)%I with "[Hawp1] Hawp2"). `````` Léon Gondelman committed Jun 11, 2018 220 221 `````` { iApply (awp_wand with "Hawp1"). iIntros (?) "[% H]". simplify_eq/=. iExists _; eauto. } `````` 222 223 224 `````` iNext. iIntros (? ?) "[% Hs2] [% Hs2']". simplify_eq/=. iExists _. rewrite -env_ps_dv_interp_app. iDestruct ("Hl" with "[\$Hs2 \$Hs2']") as "[Hs2'' \$]". `````` Léon Gondelman committed Jun 11, 2018 225 `````` iIntros "Hl". iSplit; eauto. `````` 226 `````` iFrame "Hl Hs2''". `````` Léon Gondelman committed Jun 11, 2018 227 228 229 230 231 232 233 234 235 236 237 238 `````` - specialize (IHde1 s). destruct (vcg_sp E s de1) as [[[s1' s2'] dv1]|]; simplify_eq /=. specialize (IHde2 s1'). destruct (vcg_sp E s1' de2) as [[[s1'' s2''] dv2]|]; simplify_eq /=. remember (dbin_op_eval E b dv1 dv2) as Hboe. destruct Hboe; simplify_eq/=. rewrite IHde1; last done. iDestruct "Hs" as "[Hs1' Hawp1]". rewrite IHde2; last done. iDestruct "Hs1'" as "[\$ Hawp2]". iApply (a_bin_op_spec with "Hawp1 Hawp2"). iNext. iIntros (? ?) "[% Hs2'] [% Hs2'']"; simplify_eq/=. iExists (dval_interp E dv). repeat iSplit; eauto. + iPureIntro. apply dbin_op_eval_correct. rewrite -HeqHboe. reflexivity. `````` Léon Gondelman committed Jun 11, 2018 239 `````` + iCombine "Hs2' Hs2''" as "Hs2". iFrame. `````` 240 `````` Qed. `````` Léon Gondelman committed Jun 11, 2018 241 `````` `````` 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 `````` (* Suggestion for vcg_wp *) (* Fixpoint vcg_wp (E: env_locs) (s: env_ps_dv) (de : dcexpr) (R : iProp Σ) (Φ : dval → wp_expr) : wp_expr := match vcg_sp E s de with | Some (s1, s2, dv) => append_inhale_list s1 (append_exhale_list s2 (Φ dv)) | None => match de with | dCVal dv => Φ dv | dCLoad de1 => vcg_wp E s de1 R (λ dv, IsLoc dv (λ l, Inhale l 1%Qp (λ w, Exhale l w ULvl 1%Qp (Φ w)))) | dCBinOp op de1 de2 => match vcg_sp E s de1 with | Some (s1, s2, dv1) => append_inhale_list s (vcg_wp E s1 de2 R (λ dv2, append_exhale_list (s1 ++ s2) (IsSome (dbin_op_eval E op dv1 dv2) Φ))) | None => match vcg_sp E s de2 with | Some (s1, s2, dv2) => append_inhale_list s (vcg_wp E s1 de1 R (λ dv1, append_exhale_list (s1 ++ s2) (IsSome (dbin_op_eval E op dv1 dv2) Φ))) | None => Base (awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ (dValUnknown v)))) end end | dCStore de1 de2 => (*TODO*) Base (awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ (dValUnknown v)))) end end. *) `````` Dan Frumin committed Jun 09, 2018 267 `````` Fixpoint vcg_wp (E: env_locs) (s: env_ps_dv) (de : dcexpr) (R : iProp Σ) (Φ : dval → wp_expr) : wp_expr := `````` Dan Frumin committed Jun 08, 2018 268 269 `````` match de with | dCVal dv => Φ dv `````` Léon Gondelman committed Jun 11, 2018 270 `````` | dCLoad de1 => vcg_wp E s de1 R (λ dv, IsLoc dv (λ l, Inhale l 1%Qp (λ w, Exhale l w ULvl 1%Qp (Φ w)))) `````` Léon Gondelman committed Jun 08, 2018 271 272 273 `````` | dCBinOp op de1 de2 => match vcg_sp E s de1 with | Some (s1, s2, dv1) => `````` Léon Gondelman committed Jun 11, 2018 274 `````` append_inhale_list s (vcg_wp E s1 de2 R (λ dv2, `````` 275 `````` append_exhale_list (s1 ++ s2) (IsSome (dbin_op_eval E op dv1 dv2) Φ))) `````` Dan Frumin committed Jun 09, 2018 276 `````` | None => Base (awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ (dValUnknown v)))) `````` Léon Gondelman committed Jun 08, 2018 277 `````` end `````` Dan Frumin committed Jun 09, 2018 278 `````` | _ => Base (awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ (dValUnknown v)))) `````` Dan Frumin committed Jun 07, 2018 279 280 `````` end. `````` Dan Frumin committed Jun 08, 2018 281 `````` Lemma vcg_wp_correct R E s de Φ : `````` Dan Frumin committed Jun 09, 2018 282 `````` wp_interp E (vcg_wp E s de R Φ) ⊢ `````` Dan Frumin committed Jun 08, 2018 283 `````` awp (dcexpr_interp E de) R (λ v, ∃ dv, ⌜dval_interp E dv = v ⌝ ∧ wp_interp E (Φ dv)). `````` Dan Frumin committed Jun 09, 2018 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 `````` Proof. revert Φ s. induction de; simpl; intros Φ s. - 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 /=". iDestruct "Hd" as (dl ?) "Hd". iDestruct "Hd" as (dw) "[Hl Hd]". 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 s de1) as sp. symmetry in Heqsp. `````` Léon Gondelman committed Jun 11, 2018 303 `````` destruct sp as [[[s1 s2] dv]|]; last first. `````` Léon Gondelman committed Jun 11, 2018 304 305 306 `````` { iApply (awp_wand with "H"). iIntros (v) "H". iExists (dValUnknown v). eauto 30 with iFrame. } `````` 307 `````` rewrite vcg_inhale_list_sound. `````` Léon Gondelman committed Jun 11, 2018 308 `````` iDestruct "H" as "[Henv Hde2]". `````` Léon Gondelman committed Jun 11, 2018 309 `````` rewrite IHde2. `````` Léon Gondelman committed Jun 11, 2018 310 311 312 313 314 315 `````` iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption. iDestruct ("Hsp" with "Henv") as "[Henv Hde1]". iApply (a_bin_op_spec with "Hde1 Hde2"). iNext. iIntros (? ?) "(% & H) Hex". iDestruct "Hex" as (? <-) "Hwp". simplify_eq /=. `````` 316 `````` rewrite vcg_exhale_list_sound. `````` Léon Gondelman committed Jun 11, 2018 317 318 319 320 321 322 323 324 `````` rewrite -env_ps_dv_interp_app. iSpecialize ("Hwp" with "[\$Henv \$H]"). simpl. iDestruct "Hwp" as (w) "(% & Hwp)". iExists (dval_interp E w). iSplit. iPureIntro. by apply dbin_op_eval_correct. eauto with iFrame. `````` Léon Gondelman committed Jun 11, 2018 325 `````` Qed. `````` Dan Frumin committed Jun 07, 2018 326 `````` `````` 327 `````` Lemma tac_vcg_sound Γs_in Γs_out Γls Γp ps c e R Φ E dce : `````` Dan Frumin committed Jun 07, 2018 328 329 330 `````` MapstoListFromEnv Γs_in Γs_out Γls → E = env_to_known_locs Γls → ListOfMapsto Γls E ps → `````` Dan Frumin committed Jun 08, 2018 331 `````` IntoDCexpr E e dce → `````` 332 333 `````` coq_tactics.envs_entails (coq_tactics.Envs Γp Γs_out c) (env_ps_dv_interp E ps -∗ wp_interp_sane E (vcg_wp E ps dce R (λ dv, Base (Φ (dval_interp E dv))))) → `````` Dan Frumin committed Jun 08, 2018 334 `````` coq_tactics.envs_entails (coq_tactics.Envs Γp Γs_in c) (awp e R Φ). `````` Dan Frumin committed Jun 07, 2018 335 `````` Proof. `````` Dan Frumin committed Jun 08, 2018 336 `````` rewrite /IntoDCexpr /=. intros Hsplit ->. `````` 337 `````` rewrite /ListOfMapsto. intros Hexhale -> Hgoal. `````` Dan Frumin committed Jun 07, 2018 338 339 `````` eapply tac_envs_split_mapsto; try eassumption. revert Hgoal. rewrite coq_tactics.envs_entails_eq. `````` Dan Frumin committed Jun 09, 2018 340 `````` rewrite wp_interp_sane_sound (vcg_wp_correct R). `````` Dan Frumin committed Jun 08, 2018 341 `````` intros ->. iIntros "H1 H2". `````` Dan Frumin committed Jun 07, 2018 342 `````` iSpecialize ("H1" with "H2"). iApply (awp_wand with "H1"). `````` Dan Frumin committed Jun 08, 2018 343 `````` iIntros (v) "H". by iDestruct "H" as (dv) "[-> \$]". `````` Dan Frumin committed Jun 07, 2018 344 345 `````` Qed. `````` 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 ``````End vcg. (* Ltac vcg_solver := eapply tac_vcg_sound; [ apply _ | compute; reflexivity | apply _ | apply _ | simpl ]. Section Tests_vcg. Context `{amonadG Σ}. Notation "l ↦( x , q ) v" := (mapsto l x q%Qp v%V) (at level 20, q at level 50, format "l ↦( x , q ) v"). Lemma test1 (l : loc) : l ↦U #1 -∗ awp (a_load (a_ret #l))%E True (fun v => ⌜v = #1⌝ ∗ l ↦U #1). Proof. iIntros "Hl". vcg_solver. iIntros "[H _]"; simplify_eq /=. unfold ps_lvl, ps_frc. simpl in *. Admitted. Lemma test2 (l : loc) : l ↦U #1 -∗ awp (a_store (a_ret #l) (a_ret #3))%E True (fun v => ⌜v = #3⌝ ∗ l ↦L #3). Proof. iIntros "Hl". vcg_solver. iIntros "[H _]"; simplify_eq /=. simpl. iExists (λ v, ∃ l : loc, ⌜v = #l⌝ ∗ l ↦U #1)%I, (λ v, l ↦U #1)%I. repeat iSplitL; eauto. iIntros (v1 v2). iDestruct 1 as (l' ->) "Hl'". iIntros "Hl". iExists l'. iSplit; eauto. iExists #1. iFrame. Qed. *)``````