vcgen.v 13.1 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. `````` Léon Gondelman committed Jun 13, 2018 46 `````` `````` Dan Frumin committed Jun 08, 2018 47 `````` Arguments Base _%I. `````` Dan Frumin committed Jun 07, 2018 48 `````` `````` Léon Gondelman committed Jun 08, 2018 49 `````` Fixpoint wp_interp (E : env_locs) (a : wp_expr) : iProp Σ := `````` Dan Frumin committed Jun 07, 2018 50 51 `````` match a with | Base P => P `````` Léon Gondelman committed Jun 08, 2018 52 53 `````` | 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 54 55 56 57 `````` | 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 58 59 60 61 `````` | 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 62 `````` | Par P1 P2 P3 => ∃ (Ψ1 Ψ2 : val → iProp Σ), `````` Dan Frumin committed Jun 07, 2018 63 64 `````` wp_interp E (P1 Ψ1) ∗ wp_interp E (P2 Ψ2) ∗ `````` Dan Frumin committed Jun 08, 2018 65 `````` ∀ (v1 v2 : val), Ψ1 v1 -∗ Ψ2 v2 -∗ wp_interp E (P3 (dValUnknown v1) (dValUnknown v2)) `````` Léon Gondelman committed Jun 13, 2018 66 `````` end%I. `````` Dan Frumin committed Jun 07, 2018 67 `````` `````` Léon Gondelman committed Jun 08, 2018 68 `````` Fixpoint wp_interp_sane (E : env_locs) (a : wp_expr) : iProp Σ := `````` Dan Frumin committed Jun 07, 2018 69 70 `````` match a with | Base Φ => Φ `````` Léon Gondelman committed Jun 08, 2018 71 72 `````` | Inhale dl q Φ => ∃ v, dloc_interp E dl ↦U{q} v ∗ wp_interp_sane E (Φ (dValUnknown v)) `````` Léon Gondelman committed Jun 11, 2018 73 74 75 76 `````` | 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 77 78 79 80 81 82 `````` | 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 83 84 `````` wp_interp_sane E (P1 Ψ1) ∗ wp_interp_sane E (P2 Ψ2) ∗ `````` Dan Frumin committed Jun 07, 2018 85 86 87 88 `````` ∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ wp_interp_sane E (P3 (dValUnknown v1) (dValUnknown v2)) end%I. `````` 89 `````` Fixpoint append_exhale_list (ps : env_ps_dv) (Φ : wp_expr) : wp_expr := `````` Léon Gondelman committed Jun 08, 2018 90 `````` match ps with `````` 91 `````` | (i, ((x,q), dv)) :: s' => Exhale (dLoc i) dv x q (append_exhale_list s' Φ) `````` Léon Gondelman committed Jun 08, 2018 92 93 94 `````` | [] => Φ end. `````` Léon Gondelman committed Jun 11, 2018 95 96 97 98 99 100 `````` 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. `````` Léon Gondelman committed Jun 13, 2018 101 `````` (* vcg_sp E s de = Some (s1, s2, dv) `````` Dan Frumin committed Jun 08, 2018 102 103 104 `````` - s1 = s / resources for de - s2 = new resources that you get from de *) `````` Léon Gondelman committed Jun 08, 2018 105 `````` Fixpoint vcg_sp (E: env_locs) (s: env_ps_dv) (de : dcexpr) : `````` Dan Frumin committed Jun 08, 2018 106 `````` option (env_ps_dv * env_ps_dv * dval) := `````` Léon Gondelman committed Jun 08, 2018 107 `````` match de with `````` Dan Frumin committed Jun 09, 2018 108 `````` | dCVal dv => Some (s, nil, dv) `````` Léon Gondelman committed Jun 08, 2018 109 `````` | dCLoad de1 => `````` 110 `````` ''(s1, s2, dv1) ← vcg_sp E s de1; `````` 111 112 `````` i ← is_dloc E dv1; ''(s1', ((x, q), dv2)) ← find_and_remove s1 (dLoc i); `````` 113 `````` if (bool_decide (x = ULvl)) `````` Léon Gondelman committed Jun 11, 2018 114 115 `````` then (* NB: 'x' can be a Coq variable, so here we can't check that 'x' is Ulvl *) `````` 116 `````` Some ((i, ((x, (q/2)%Qp), dv2)) :: s1', (i, ((x, (q/2)%Qp), dv2)) :: s2, dv2) `````` Léon Gondelman committed Jun 11, 2018 117 `````` else None `````` Léon Gondelman committed Jun 08, 2018 118 `````` | dCStore de1 de2 => `````` Léon Gondelman committed Jun 11, 2018 119 120 `````` ''(s1, s2, dv1) ← vcg_sp E s de1; i ← is_dloc E dv1; `````` 121 122 123 124 `````` ''(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 *) `````` 125 `````` if (bool_decide (q = Qp_one) && bool_decide (x = ULvl)) `````` 126 `````` then Some (s1'', (i, ((LLvl, 1%Qp), dv2)) :: s2'', dv2) `````` 127 `````` else None `````` Léon Gondelman committed Jun 08, 2018 128 `````` | dCBinOp op de1 de2 => `````` Léon Gondelman committed Jun 11, 2018 129 `````` ''(s1, s2, dv1) ← vcg_sp E s de1; `````` Dan Frumin committed Jun 08, 2018 130 131 `````` ''(s1', s2', dv2) ← vcg_sp E s1 de2; match dbin_op_eval E op dv1 dv2 with `````` Léon Gondelman committed Jun 11, 2018 132 `````` | dSome dv => Some (s1', s2 ++ s2', dv) `````` Robbert Krebbers committed Jun 13, 2018 133 134 `````` (* | 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 135 `````` | dNone | dUnknown _ => None `````` Dan Frumin committed Jun 08, 2018 136 `````` end `````` Léon Gondelman committed Jun 08, 2018 137 138 `````` end. `````` Léon Gondelman committed Jun 13, 2018 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 `````` Fixpoint vcg_wp (E: env_locs) (s: env_ps_dv) (de : dcexpr) (R : iProp Σ) (Φ : dval → wp_expr) : wp_expr := 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 => Base (awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ (dValUnknown v)))) end | _ => Base (awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ (dValUnknown v)))) end. End vcg. Section vcg_spec. Context `{amonadG Σ}. 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. - simpl. iIntros (E) "(He & H)". iFrame. by iApply IHa. - 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Φ)". iExists _,_. iSplitL "HΨ1". by iApply H0. iSplitL "HΨ2". by iApply H1. iIntros (v1 v2) "Hv1 Hv2". iApply H2. iApply ("HΦ" with "Hv1 Hv2"). Qed. Lemma vcg_inhale_list_sound E s t : 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. 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. Proof. unfold env_ps_dv_interp. induction s as [| [i [[x q] w]] s']; simpl. - by iIntros "\$ _". - iIntros "H [H1 H2]". iSpecialize ("H" with "H1"). iApply (IHs' with "H H2"). Qed. `````` 200 201 `````` 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 202 `````` env_ps_dv_interp E s -∗ `````` 203 204 `````` 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 205 `````` Proof. `````` 206 207 `````` revert s ps1 ps2 dv. induction de; iIntros (s ps1 ps2 dv Hsp) "Hs"; simplify_eq/=. `````` Léon Gondelman committed Jun 11, 2018 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 `````` - 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. `````` 225 226 `````` - specialize (IHde1 s). destruct (vcg_sp E s de1) as [[[s1 s2] dv1]|]; simplify_eq /=. `````` Léon Gondelman committed Jun 11, 2018 227 228 `````` destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=. destruct d as [l|?]; simplify_eq/=. `````` 229 230 231 232 233 234 235 236 237 238 `````` 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 239 240 `````` { iApply (awp_wand with "Hawp1"). iIntros (?) "[% H]". simplify_eq/=. iExists _; eauto. } `````` 241 242 243 `````` 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 244 `````` iIntros "Hl". iSplit; eauto. `````` 245 `````` iFrame "Hl Hs2''". `````` Léon Gondelman committed Jun 11, 2018 246 247 248 249 250 251 252 253 254 255 256 257 `````` - 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 258 `````` + iCombine "Hs2' Hs2''" as "Hs2". iFrame. `````` 259 `````` Qed. `````` Léon Gondelman committed Jun 11, 2018 260 `````` `````` Dan Frumin committed Jun 08, 2018 261 `````` Lemma vcg_wp_correct R E s de Φ : `````` Dan Frumin committed Jun 09, 2018 262 `````` wp_interp E (vcg_wp E s de R Φ) ⊢ `````` Dan Frumin committed Jun 08, 2018 263 `````` awp (dcexpr_interp E de) R (λ v, ∃ dv, ⌜dval_interp E dv = v ⌝ ∧ wp_interp E (Φ dv)). `````` Dan Frumin committed Jun 09, 2018 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 `````` 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 283 `````` destruct sp as [[[s1 s2] dv]|]; last first. `````` Léon Gondelman committed Jun 11, 2018 284 285 286 `````` { iApply (awp_wand with "H"). iIntros (v) "H". iExists (dValUnknown v). eauto 30 with iFrame. } `````` 287 `````` rewrite vcg_inhale_list_sound. `````` Léon Gondelman committed Jun 11, 2018 288 `````` iDestruct "H" as "[Henv Hde2]". `````` Léon Gondelman committed Jun 11, 2018 289 `````` rewrite IHde2. `````` Léon Gondelman committed Jun 11, 2018 290 291 292 293 294 295 `````` 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 /=. `````` 296 `````` rewrite vcg_exhale_list_sound. `````` Léon Gondelman committed Jun 11, 2018 297 298 299 300 301 302 303 304 `````` 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 305 `````` Qed. `````` Dan Frumin committed Jun 07, 2018 306 `````` `````` 307 `````` Lemma tac_vcg_sound Γs_in Γs_out Γls Γp ps c e R Φ E dce : `````` Dan Frumin committed Jun 07, 2018 308 309 310 `````` MapstoListFromEnv Γs_in Γs_out Γls → E = env_to_known_locs Γls → ListOfMapsto Γls E ps → `````` Dan Frumin committed Jun 08, 2018 311 `````` IntoDCexpr E e dce → `````` 312 313 `````` 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 314 `````` coq_tactics.envs_entails (coq_tactics.Envs Γp Γs_in c) (awp e R Φ). `````` Dan Frumin committed Jun 07, 2018 315 `````` Proof. `````` Dan Frumin committed Jun 08, 2018 316 `````` rewrite /IntoDCexpr /=. intros Hsplit ->. `````` 317 `````` rewrite /ListOfMapsto. intros Hexhale -> Hgoal. `````` Dan Frumin committed Jun 07, 2018 318 319 `````` eapply tac_envs_split_mapsto; try eassumption. revert Hgoal. rewrite coq_tactics.envs_entails_eq. `````` Dan Frumin committed Jun 09, 2018 320 `````` rewrite wp_interp_sane_sound (vcg_wp_correct R). `````` Dan Frumin committed Jun 08, 2018 321 `````` intros ->. iIntros "H1 H2". `````` Dan Frumin committed Jun 07, 2018 322 `````` iSpecialize ("H1" with "H2"). iApply (awp_wand with "H1"). `````` Dan Frumin committed Jun 08, 2018 323 `````` iIntros (v) "H". by iDestruct "H" as (dv) "[-> \$]". `````` Dan Frumin committed Jun 07, 2018 324 325 `````` Qed. `````` Léon Gondelman committed Jun 13, 2018 326 ``End vcg_spec.``