counterexamples.v 12.9 KB
 Robbert Krebbers committed Oct 30, 2017 1 ``````From iris.bi Require Export bi. `````` Ralf Jung committed Aug 04, 2016 2 ``````From iris.proofmode Require Import tactics. `````` Ralf Jung committed Jan 05, 2017 3 ``````Set Default Proof Using "Type*". `````` Ralf Jung committed Aug 04, 2016 4 5 `````` (** This proves that we need the ▷ in a "Saved Proposition" construction with `````` Derek Dreyer committed Aug 08, 2016 6 ``````name-dependent allocation. *) `````` Ralf Jung committed Aug 05, 2016 7 ``````Module savedprop. Section savedprop. `````` Jacques-Henri Jourdan committed Dec 04, 2017 8 `````` Context `{BiAffine PROP}. `````` Robbert Krebbers committed Oct 30, 2017 9 `````` Notation "¬ P" := (□ (P → False))%I : bi_scope. `````` Robbert Krebbers committed Oct 30, 2017 10 `````` Implicit Types P : PROP. `````` Ralf Jung committed Aug 04, 2016 11 `````` `````` Robbert Krebbers committed Oct 30, 2017 12 13 14 15 16 17 18 19 20 21 `````` Context (bupd : PROP → PROP). Notation "|==> Q" := (bupd Q) (at level 99, Q at level 200, format "|==> Q") : bi_scope. Hypothesis bupd_intro : ∀ P, P ⊢ |==> P. Hypothesis bupd_mono : ∀ P Q, (P ⊢ Q) → (|==> P) ⊢ |==> Q. Hypothesis bupd_trans : ∀ P, (|==> |==> P) ⊢ |==> P. Hypothesis bupd_frame_r : ∀ P R, (|==> P) ∗ R ⊢ |==> (P ∗ R). Context (ident : Type) (saved : ident → PROP → PROP). `````` Robbert Krebbers committed Oct 25, 2017 22 `````` Hypothesis sprop_persistent : ∀ i P, Persistent (saved i P). `````` Ralf Jung committed Aug 04, 2016 23 `````` Hypothesis sprop_alloc_dep : `````` Robbert Krebbers committed Oct 30, 2017 24 `````` ∀ (P : ident → PROP), (|==> ∃ i, saved i (P i))%I. `````` Ralf Jung committed Aug 08, 2016 25 `````` Hypothesis sprop_agree : ∀ i P Q, saved i P ∧ saved i Q ⊢ □ (P ↔ Q). `````` Ralf Jung committed Aug 04, 2016 26 `````` `````` Robbert Krebbers committed Oct 30, 2017 27 28 29 30 31 `````` (** We assume that we cannot update to false. *) Hypothesis consistency : ¬(|==> False)%I. Instance bupd_mono' : Proper ((⊢) ==> (⊢)) bupd. Proof. intros P Q ?. by apply bupd_mono. Qed. `````` Robbert Krebbers committed Apr 04, 2018 32 33 34 35 36 `````` Instance elim_modal_bupd p P Q : ElimModal True p false (|==> P) P (|==> Q) (|==> Q). Proof. by rewrite /ElimModal bi.intuitionistically_if_elim bupd_frame_r bi.wand_elim_r bupd_trans. Qed. `````` Robbert Krebbers committed Oct 30, 2017 37 `````` `````` Ralf Jung committed Aug 08, 2016 38 `````` (** A bad recursive reference: "Assertion with name [i] does not hold" *) `````` Robbert Krebbers committed Oct 30, 2017 39 `````` Definition A (i : ident) : PROP := (∃ P, ¬ P ∗ saved i P)%I. `````` Ralf Jung committed Aug 08, 2016 40 `````` `````` 41 `````` Lemma A_alloc : (|==> ∃ i, saved i (A i))%I. `````` Ralf Jung committed Aug 08, 2016 42 `````` Proof. by apply sprop_alloc_dep. Qed. `````` Ralf Jung committed Aug 04, 2016 43 `````` `````` Ralf Jung committed Aug 08, 2016 44 `````` Lemma saved_NA i : saved i (A i) ⊢ ¬ A i. `````` Ralf Jung committed Aug 04, 2016 45 `````` Proof. `````` Ralf Jung committed Aug 08, 2016 46 47 48 49 50 `````` iIntros "#Hs !# #HA". iPoseProof "HA" as "HA'". iDestruct "HA'" as (P) "[#HNP HsP]". iApply "HNP". iDestruct (sprop_agree i P (A i) with "[]") as "#[_ HP]". { eauto. } iApply "HP". done. `````` Ralf Jung committed Aug 04, 2016 51 52 `````` Qed. `````` Ralf Jung committed Aug 08, 2016 53 `````` Lemma saved_A i : saved i (A i) ⊢ A i. `````` Ralf Jung committed Aug 04, 2016 54 `````` Proof. `````` Ralf Jung committed Aug 08, 2016 55 56 `````` iIntros "#Hs". iExists (A i). iFrame "#". by iApply saved_NA. `````` Ralf Jung committed Aug 04, 2016 57 `````` Qed. `````` Robbert Krebbers committed Aug 05, 2016 58 59 `````` Lemma contradiction : False. `````` Ralf Jung committed Jan 05, 2017 60 `````` Proof using All. `````` Robbert Krebbers committed Oct 30, 2017 61 `````` apply consistency. `````` Robbert Krebbers committed Oct 30, 2017 62 `````` iMod A_alloc as (i) "#H". `````` Ralf Jung committed Aug 08, 2016 63 `````` iPoseProof (saved_NA with "H") as "HN". `````` Robbert Krebbers committed Oct 30, 2017 64 `````` iApply bupd_intro. iApply "HN". iApply saved_A. done. `````` Robbert Krebbers committed Aug 05, 2016 65 `````` Qed. `````` Ralf Jung committed Aug 05, 2016 66 ``````End savedprop. End savedprop. `````` Ralf Jung committed Aug 05, 2016 67 `````` `````` Robbert Krebbers committed Oct 30, 2017 68 `````` `````` Ralf Jung committed Aug 05, 2016 69 ``````(** This proves that we need the ▷ when opening invariants. *) `````` Ralf Jung committed Aug 05, 2016 70 ``````Module inv. Section inv. `````` Jacques-Henri Jourdan committed Dec 04, 2017 71 `````` Context `{BiAffine PROP}. `````` Robbert Krebbers committed Oct 30, 2017 72 `````` Implicit Types P : PROP. `````` Ralf Jung committed Aug 05, 2016 73 74 `````` (** Assumptions *) `````` Robbert Krebbers committed Oct 25, 2016 75 `````` (** We have the update modality (two classes: empty/full mask) *) `````` Robbert Krebbers committed Aug 05, 2016 76 `````` Inductive mask := M0 | M1. `````` Robbert Krebbers committed Oct 30, 2017 77 78 `````` Context (fupd : mask → PROP → PROP). Arguments fupd _ _%I. `````` Robbert Krebbers committed Oct 25, 2016 79 80 81 `````` Hypothesis fupd_intro : ∀ E P, P ⊢ fupd E P. Hypothesis fupd_mono : ∀ E P Q, (P ⊢ Q) → fupd E P ⊢ fupd E Q. Hypothesis fupd_fupd : ∀ E P, fupd E (fupd E P) ⊢ fupd E P. `````` Robbert Krebbers committed Nov 03, 2016 82 `````` Hypothesis fupd_frame_l : ∀ E P Q, P ∗ fupd E Q ⊢ fupd E (P ∗ Q). `````` Robbert Krebbers committed Oct 25, 2016 83 `````` Hypothesis fupd_mask_mono : ∀ P, fupd M0 P ⊢ fupd M1 P. `````` Ralf Jung committed Aug 05, 2016 84 `````` `````` Robbert Krebbers committed Oct 25, 2016 85 `````` (** We have invariants *) `````` Robbert Krebbers committed Oct 30, 2017 86 87 `````` Context (name : Type) (inv : name → PROP → PROP). Arguments inv _ _%I. `````` Robbert Krebbers committed Oct 25, 2017 88 `````` Hypothesis inv_persistent : ∀ i P, Persistent (inv i P). `````` Robbert Krebbers committed Oct 25, 2016 89 `````` Hypothesis inv_alloc : ∀ P, P ⊢ fupd M1 (∃ i, inv i P). `````` Ralf Jung committed Aug 05, 2016 90 `````` Hypothesis inv_open : `````` Robbert Krebbers committed Nov 03, 2016 91 `````` ∀ i P Q R, (P ∗ Q ⊢ fupd M0 (P ∗ R)) → (inv i P ∗ Q ⊢ fupd M1 R). `````` Ralf Jung committed Aug 05, 2016 92 `````` `````` Ralf Jung committed Aug 05, 2016 93 94 95 `````` (* We have tokens for a little "two-state STS": [start] -> [finish]. state. [start] also asserts the exact state; it is only ever owned by the invariant. [finished] is duplicable. *) `````` Ralf Jung committed Aug 08, 2016 96 97 98 99 `````` (* Posssible implementations of these axioms: * Using the STS monoid of a two-state STS, where [start] is the authoritative saying the state is exactly [start], and [finish] is the "we are at least in state [finish]" typically owned by threads. `````` 100 `````` * Ex () +_## () `````` Ralf Jung committed Aug 08, 2016 101 `````` *) `````` Ralf Jung committed Aug 05, 2016 102 `````` Context (gname : Type). `````` Robbert Krebbers committed Oct 30, 2017 103 `````` Context (start finished : gname → PROP). `````` Ralf Jung committed Aug 05, 2016 104 `````` `````` 105 `````` Hypothesis sts_alloc : fupd M0 (∃ γ, start γ). `````` Robbert Krebbers committed Oct 25, 2016 106 `````` Hypotheses start_finish : ∀ γ, start γ ⊢ fupd M0 (finished γ). `````` Ralf Jung committed Aug 05, 2016 107 `````` `````` Robbert Krebbers committed Nov 03, 2016 108 `````` Hypothesis finished_not_start : ∀ γ, start γ ∗ finished γ ⊢ False. `````` Ralf Jung committed Aug 05, 2016 109 `````` `````` Robbert Krebbers committed Nov 03, 2016 110 `````` Hypothesis finished_dup : ∀ γ, finished γ ⊢ finished γ ∗ finished γ. `````` Ralf Jung committed Aug 05, 2016 111 `````` `````` Robbert Krebbers committed Oct 25, 2016 112 `````` (** We assume that we cannot update to false. *) `````` 113 `````` Hypothesis consistency : ¬ (fupd M1 False). `````` Ralf Jung committed Aug 05, 2016 114 115 `````` (** Some general lemmas and proof mode compatibility. *) `````` Robbert Krebbers committed Nov 03, 2016 116 `````` Lemma inv_open' i P R : inv i P ∗ (P -∗ fupd M0 (P ∗ fupd M1 R)) ⊢ fupd M1 R. `````` Ralf Jung committed Aug 05, 2016 117 `````` Proof. `````` Robbert Krebbers committed Oct 25, 2016 118 `````` iIntros "(#HiP & HP)". iApply fupd_fupd. iApply inv_open; last first. `````` Ralf Jung committed Aug 05, 2016 119 120 121 122 `````` { iSplit; first done. iExact "HP". } iIntros "(HP & HPw)". by iApply "HPw". Qed. `````` Robbert Krebbers committed Oct 25, 2016 123 124 125 `````` Instance fupd_mono' E : Proper ((⊢) ==> (⊢)) (fupd E). Proof. intros P Q ?. by apply fupd_mono. Qed. Instance fupd_proper E : Proper ((⊣⊢) ==> (⊣⊢)) (fupd E). `````` Ralf Jung committed Aug 05, 2016 126 `````` Proof. `````` Robbert Krebbers committed Oct 30, 2017 127 `````` intros P Q; rewrite !bi.equiv_spec=> -[??]; split; by apply fupd_mono. `````` Ralf Jung committed Aug 05, 2016 128 129 `````` Qed. `````` 130 `````` Lemma fupd_frame_r E P Q : fupd E P ∗ Q ⊢ fupd E (P ∗ Q). `````` Robbert Krebbers committed Oct 25, 2016 131 `````` Proof. by rewrite comm fupd_frame_l comm. Qed. `````` Ralf Jung committed Aug 05, 2016 132 `````` `````` Robbert Krebbers committed Apr 04, 2018 133 134 135 136 137 138 `````` Global Instance elim_fupd_fupd p E P Q : ElimModal True p false (fupd E P) P (fupd E Q) (fupd E Q). Proof. by rewrite /ElimModal bi.intuitionistically_if_elim fupd_frame_r bi.wand_elim_r fupd_fupd. Qed. `````` Ralf Jung committed Aug 05, 2016 139 `````` `````` Robbert Krebbers committed Apr 04, 2018 140 141 `````` Global Instance elim_fupd0_fupd1 p P Q : ElimModal True p false (fupd M0 P) P (fupd M1 Q) (fupd M1 Q). `````` Ralf Jung committed Aug 05, 2016 142 `````` Proof. `````` Robbert Krebbers committed Apr 04, 2018 143 144 `````` by rewrite /ElimModal bi.intuitionistically_if_elim fupd_frame_r bi.wand_elim_r fupd_mask_mono fupd_fupd. `````` Ralf Jung committed Aug 05, 2016 145 146 `````` Qed. `````` Robbert Krebbers committed Oct 30, 2017 147 `````` Global Instance exists_split_fupd0 {A} E P (Φ : A → PROP) : `````` Robbert Krebbers committed Oct 25, 2016 148 `````` FromExist P Φ → FromExist (fupd E P) (λ a, fupd E (Φ a)). `````` Ralf Jung committed Aug 05, 2016 149 `````` Proof. `````` Robbert Krebbers committed Oct 30, 2017 150 151 `````` rewrite /FromExist=>HP. apply bi.exist_elim=> a. apply fupd_mono. by rewrite -HP -(bi.exist_intro a). `````` Ralf Jung committed Aug 05, 2016 152 153 `````` Qed. `````` Derek Dreyer committed Aug 08, 2016 154 `````` (** Now to the actual counterexample. We start with a weird form of saved propositions. *) `````` Robbert Krebbers committed Oct 30, 2017 155 156 `````` Definition saved (γ : gname) (P : PROP) : PROP := (∃ i, inv i (start γ ∨ (finished γ ∗ □ P)))%I. `````` Robbert Krebbers committed Oct 25, 2017 157 `````` Global Instance saved_persistent γ P : Persistent (saved γ P) := _. `````` Ralf Jung committed Aug 05, 2016 158 `````` `````` Robbert Krebbers committed Oct 30, 2017 159 `````` Lemma saved_alloc (P : gname → PROP) : fupd M1 (∃ γ, saved γ (P γ)). `````` Ralf Jung committed Aug 05, 2016 160 `````` Proof. `````` Robbert Krebbers committed Oct 25, 2016 161 `````` iIntros "". iMod (sts_alloc) as (γ) "Hs". `````` Robbert Krebbers committed Oct 30, 2017 162 `````` iMod (inv_alloc (start γ ∨ (finished γ ∗ □ (P γ)))%I with "[Hs]") as (i) "#Hi". `````` Robbert Krebbers committed Aug 05, 2016 163 `````` { auto. } `````` Robbert Krebbers committed Oct 25, 2016 164 `````` iApply fupd_intro. by iExists γ, i. `````` Ralf Jung committed Aug 05, 2016 165 166 `````` Qed. `````` Robbert Krebbers committed Nov 03, 2016 167 `````` Lemma saved_cast γ P Q : saved γ P ∗ saved γ Q ∗ □ P ⊢ fupd M1 (□ Q). `````` Ralf Jung committed Aug 05, 2016 168 `````` Proof. `````` Ralf Jung committed Aug 05, 2016 169 `````` iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP". `````` Ralf Jung committed Aug 05, 2016 170 `````` iApply (inv_open' i). iSplit; first done. `````` Robbert Krebbers committed Oct 25, 2016 171 `````` iIntros "HaP". iAssert (fupd M0 (finished γ)) with "[HaP]" as "> Hf". `````` Ralf Jung committed Aug 05, 2016 172 173 `````` { iDestruct "HaP" as "[Hs | [Hf _]]". - by iApply start_finish. `````` Robbert Krebbers committed Oct 25, 2016 174 `````` - by iApply fupd_intro. } `````` Robbert Krebbers committed Aug 08, 2016 175 `````` iDestruct (finished_dup with "Hf") as "[Hf Hf']". `````` Robbert Krebbers committed Oct 25, 2016 176 `````` iApply fupd_intro. iSplitL "Hf'"; first by eauto. `````` Ralf Jung committed Aug 05, 2016 177 `````` (* Step 2: Open the Q-invariant. *) `````` Robbert Krebbers committed Sep 27, 2016 178 `````` iClear (i) "HiP ". iDestruct "HsQ" as (i) "HiQ". `````` Ralf Jung committed Aug 05, 2016 179 180 `````` iApply (inv_open' i). iSplit; first done. iIntros "[HaQ | [_ #HQ]]". `````` Robbert Krebbers committed Aug 05, 2016 181 `````` { iExFalso. iApply finished_not_start. by iFrame. } `````` Robbert Krebbers committed Oct 25, 2016 182 `````` iApply fupd_intro. iSplitL "Hf". `````` Robbert Krebbers committed Aug 05, 2016 183 `````` { iRight. by iFrame. } `````` Robbert Krebbers committed Oct 25, 2016 184 `````` by iApply fupd_intro. `````` Ralf Jung committed Aug 05, 2016 185 186 `````` Qed. `````` Ralf Jung committed Aug 05, 2016 187 `````` (** And now we tie a bad knot. *) `````` Robbert Krebbers committed Oct 30, 2017 188 `````` Notation "¬ P" := (□ (P -∗ fupd M1 False))%I : bi_scope. `````` Robbert Krebbers committed Oct 30, 2017 189 `````` Definition A i : PROP := (∃ P, ¬P ∗ saved i P)%I. `````` Robbert Krebbers committed Oct 25, 2017 190 `````` Global Instance A_persistent i : Persistent (A i) := _. `````` Ralf Jung committed Aug 05, 2016 191 `````` `````` 192 `````` Lemma A_alloc : fupd M1 (∃ i, saved i (A i)). `````` Ralf Jung committed Aug 05, 2016 193 `````` Proof. by apply saved_alloc. Qed. `````` Ralf Jung committed Aug 05, 2016 194 `````` `````` Ralf Jung committed Aug 08, 2016 195 `````` Lemma saved_NA i : saved i (A i) ⊢ ¬A i. `````` Ralf Jung committed Aug 05, 2016 196 `````` Proof. `````` Ralf Jung committed Aug 05, 2016 197 198 `````` iIntros "#Hi !# #HA". iPoseProof "HA" as "HA'". iDestruct "HA'" as (P) "#[HNP Hi']". `````` Robbert Krebbers committed Oct 25, 2016 199 `````` iMod (saved_cast i (A i) P with "[]") as "HP". `````` Ralf Jung committed Aug 08, 2016 200 `````` { eauto. } `````` Ralf Jung committed Aug 05, 2016 201 `````` by iApply "HNP". `````` Ralf Jung committed Aug 05, 2016 202 `````` Qed. `````` Ralf Jung committed Aug 05, 2016 203 `````` `````` Ralf Jung committed Aug 08, 2016 204 `````` Lemma saved_A i : saved i (A i) ⊢ A i. `````` Ralf Jung committed Aug 05, 2016 205 `````` Proof. `````` Ralf Jung committed Aug 08, 2016 206 207 `````` iIntros "#Hi". iExists (A i). iFrame "#". by iApply saved_NA. `````` Ralf Jung committed Aug 05, 2016 208 `````` Qed. `````` Ralf Jung committed Aug 05, 2016 209 `````` `````` Ralf Jung committed Aug 05, 2016 210 `````` Lemma contradiction : False. `````` Ralf Jung committed Jan 05, 2017 211 `````` Proof using All. `````` Ralf Jung committed Oct 07, 2016 212 `````` apply consistency. iIntros "". `````` Robbert Krebbers committed Oct 25, 2016 213 `````` iMod A_alloc as (i) "#H". `````` Ralf Jung committed Aug 08, 2016 214 215 `````` iPoseProof (saved_NA with "H") as "HN". iApply "HN". iApply saved_A. done. `````` Ralf Jung committed Aug 05, 2016 216 217 `````` Qed. End inv. End inv. `````` Ralf Jung committed Feb 02, 2020 218 219 `````` (** This proves that if we have linear impredicative invariants, we can still `````` Ralf Jung committed Feb 06, 2020 220 221 222 223 ``````drop arbitrary resources (i.e., we can "defeat" linearity). Variant 1: a strong invariant creation lemma that lets us create invariants in the "open" state. *) Module linear1. Section linear1. `````` Ralf Jung committed Feb 02, 2020 224 225 226 227 228 229 230 231 232 233 234 235 236 `````` Context {PROP: sbi}. Implicit Types P : PROP. (** Assumptions. *) (** We have the mask-changing update modality (two classes: empty/full mask) *) Inductive mask := M0 | M1. Context (fupd : mask → mask → PROP → PROP). Arguments fupd _ _ _%I. Hypothesis fupd_intro : ∀ E P, P ⊢ fupd E E P. Hypothesis fupd_mono : ∀ E1 E2 P Q, (P ⊢ Q) → fupd E1 E2 P ⊢ fupd E1 E2 Q. Hypothesis fupd_fupd : ∀ E1 E2 E3 P, fupd E1 E2 (fupd E2 E3 P) ⊢ fupd E1 E3 P. Hypothesis fupd_frame_l : ∀ E1 E2 P Q, P ∗ fupd E1 E2 Q ⊢ fupd E1 E2 (P ∗ Q). `````` Ralf Jung committed Feb 06, 2020 237 `````` (** We have cancelable invariants. (Really they would have fractions at `````` Ralf Jung committed Feb 02, 2020 238 239 240 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 267 268 269 `````` [cinv_own] but we do not need that. They would also have a name matching the [mask] type, but we do not need that either.) *) Context (gname : Type) (cinv : gname → PROP → PROP) (cinv_own : gname → PROP). Hypothesis cinv_alloc_open : ∀ P, (fupd M1 M0 (∃ γ, cinv γ P ∗ cinv_own γ ∗ (▷ P -∗ fupd M0 M1 emp)))%I. (** Some general lemmas and proof mode compatibility. *) Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (fupd E1 E2). Proof. intros P Q ?. by apply fupd_mono. Qed. Instance fupd_proper E1 E2 : Proper ((⊣⊢) ==> (⊣⊢)) (fupd E1 E2). Proof. intros P Q; rewrite !bi.equiv_spec=> -[??]; split; by apply fupd_mono. Qed. Lemma fupd_frame_r E1 E2 P Q : fupd E1 E2 P ∗ Q ⊢ fupd E1 E2 (P ∗ Q). Proof. by rewrite comm fupd_frame_l comm. Qed. Global Instance elim_fupd_fupd p E1 E2 E3 P Q : ElimModal True p false (fupd E1 E2 P) P (fupd E1 E3 Q) (fupd E2 E3 Q). Proof. by rewrite /ElimModal bi.intuitionistically_if_elim fupd_frame_r bi.wand_elim_r fupd_fupd. Qed. (** Counterexample: now we can make any resource disappear. *) Lemma leak P : P -∗ fupd M1 M1 emp. Proof. iIntros "HP". set (INV := (∃ γ Q, cinv γ Q ∗ cinv_own γ ∗ P)%I). iMod (cinv_alloc_open INV) as (γ) "(Hinv & Htok & Hclose)". iApply "Hclose". iNext. iExists γ, _. iFrame. Qed. `````` Ralf Jung committed Feb 06, 2020 270 ``````End linear1. End linear1. `````` Ralf Jung committed Feb 02, 2020 271 `````` `````` Ralf Jung committed Feb 06, 2020 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 ``````(** This proves that if we have linear impredicative invariants, we can still drop arbitrary resources (i.e., we can "defeat" linearity). Variant 2: the invariant can depend on the chose gname, and we also have an accessor that gives back the invariant token immediately, not just after the invariant got closed again. *) Module linear2. Section linear2. Context {PROP: sbi}. Implicit Types P : PROP. (** Assumptions. *) (** We have the mask-changing update modality (two classes: empty/full mask) *) Inductive mask := M0 | M1. Context (fupd : mask → mask → PROP → PROP). Arguments fupd _ _ _%I. Hypothesis fupd_intro : ∀ E P, P ⊢ fupd E E P. Hypothesis fupd_mono : ∀ E1 E2 P Q, (P ⊢ Q) → fupd E1 E2 P ⊢ fupd E1 E2 Q. Hypothesis fupd_fupd : ∀ E1 E2 E3 P, fupd E1 E2 (fupd E2 E3 P) ⊢ fupd E1 E3 P. Hypothesis fupd_frame_l : ∀ E1 E2 P Q, P ∗ fupd E1 E2 Q ⊢ fupd E1 E2 (P ∗ Q). `````` Ralf Jung committed Feb 06, 2020 291 `````` (** We have cancelable invariants. (Really they would have fractions at `````` Ralf Jung committed Feb 06, 2020 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 `````` [cinv_own] but we do not need that. They would also have a name matching the [mask] type, but we do not need that either.) *) Context (gname : Type) (cinv : gname → PROP → PROP) (cinv_own : gname → PROP). Hypothesis cinv_alloc : ∀ E, fupd E E (∃ γ, cinv_own γ ∗ (∀ P, ▷ P -∗ fupd E E (cinv γ P)))%I. Hypothesis cinv_access : ∀ P γ, cinv γ P -∗ cinv_own γ -∗ fupd M1 M0 (▷ P ∗ cinv_own γ ∗ (▷ P -∗ fupd M0 M1 emp)). Hypothesis cinv_own_excl : ∀ E γ, ▷ cinv_own γ -∗ ▷ cinv_own γ -∗ fupd E E False. (** Some general lemmas and proof mode compatibility. *) Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (fupd E1 E2). Proof. intros P Q ?. by apply fupd_mono. Qed. Instance fupd_proper E1 E2 : Proper ((⊣⊢) ==> (⊣⊢)) (fupd E1 E2). Proof. intros P Q; rewrite !bi.equiv_spec=> -[??]; split; by apply fupd_mono. Qed. Lemma fupd_frame_r E1 E2 P Q : fupd E1 E2 P ∗ Q ⊢ fupd E1 E2 (P ∗ Q). Proof. by rewrite comm fupd_frame_l comm. Qed. Global Instance elim_fupd_fupd p E1 E2 E3 P Q : ElimModal True p false (fupd E1 E2 P) P (fupd E1 E3 Q) (fupd E2 E3 Q). Proof. by rewrite /ElimModal bi.intuitionistically_if_elim fupd_frame_r bi.wand_elim_r fupd_fupd. Qed. (** Counterexample: now we can make any resource disappear. *) Lemma leak P : P -∗ fupd M1 M1 emp. Proof. iIntros "HP". iMod cinv_alloc as (γ) "(Htok & Hmkinv)". set (INV := (P ∨ cinv_own γ ∗ P)%I). iMod ("Hmkinv" \$! INV with "[HP]") as "Hinv". { iLeft. done. } iMod (cinv_access with "Hinv Htok") as "([HP|Hinv] & Htok & Hclose)"; last first. { iDestruct "Hinv" as "(Htok' & ?)". iMod (cinv_own_excl with "Htok Htok'") as "[]". } iApply "Hclose". iNext. iRight. iFrame. Qed. End linear2. End linear2.``````