counterexamples.v 12.8 KB
Newer Older
1
From iris.bi Require Export bi.
2
From iris.proofmode Require Import tactics.
3
Set Default Proof Using "Type*".
4 5

(** This proves that we need the ▷ in a "Saved Proposition" construction with
Derek Dreyer's avatar
Derek Dreyer committed
6
name-dependent allocation. *)
7
Module savedprop. Section savedprop.
8
  Context `{BiAffine PROP}.
Robbert Krebbers's avatar
Robbert Krebbers committed
9
  Notation "¬ P" := ( (P  False))%I : bi_scope.
10
  Implicit Types P : PROP.
11

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).
22
  Hypothesis sprop_persistent :  i P, Persistent (saved i P).
23
  Hypothesis sprop_alloc_dep :
24
     (P : ident  PROP), (|==>  i, saved i (P i))%I.
25
  Hypothesis sprop_agree :  i P Q, saved i P  saved i Q   (P  Q).
26

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.
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.
37

38
  (** A bad recursive reference: "Assertion with name [i] does not hold" *)
39
  Definition A (i : ident) : PROP := ( P, ¬ P  saved i P)%I.
40

41
  Lemma A_alloc : (|==>  i, saved i (A i))%I.
42
  Proof. by apply sprop_alloc_dep. Qed.
43

44
  Lemma saved_NA i : saved i (A i)  ¬ A i.
45
  Proof.
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.
51 52
  Qed.

53
  Lemma saved_A i : saved i (A i)  A i.
54
  Proof.
55 56
    iIntros "#Hs". iExists (A i). iFrame "#".
    by iApply saved_NA.
57
  Qed.
58 59

  Lemma contradiction : False.
60
  Proof using All.
61
    apply consistency.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
    iMod A_alloc as (i) "#H".
63
    iPoseProof (saved_NA with "H") as "HN".
64
    iApply bupd_intro. iApply "HN". iApply saved_A. done.
65
  Qed.
66
End savedprop. End savedprop.
67

68

69
(** This proves that we need the ▷ when opening invariants. *)
70
Module inv. Section inv.
71
  Context `{BiAffine PROP}.
72
  Implicit Types P : PROP.
73 74

  (** Assumptions *)
75
  (** We have the update modality (two classes: empty/full mask) *)
76
  Inductive mask := M0 | M1.
77 78
  Context (fupd : mask  PROP  PROP).
  Arguments fupd _ _%I.
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.
82
  Hypothesis fupd_frame_l :  E P Q, P  fupd E Q  fupd E (P  Q).
83
  Hypothesis fupd_mask_mono :  P, fupd M0 P  fupd M1 P.
84

85
  (** We have invariants *)
86 87
  Context (name : Type) (inv : name  PROP  PROP).
  Arguments inv _ _%I.
88
  Hypothesis inv_persistent :  i P, Persistent (inv i P).
89
  Hypothesis inv_alloc :  P, P  fupd M1 ( i, inv i P).
90
  Hypothesis inv_open :
91
     i P Q R, (P  Q  fupd M0 (P  R))  (inv i P  Q  fupd M1 R).
92

Ralf Jung's avatar
Ralf Jung committed
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. *)
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 () +_## ()
101
  *)
Ralf Jung's avatar
Ralf Jung committed
102
  Context (gname : Type).
103
  Context (start finished : gname  PROP).
Ralf Jung's avatar
Ralf Jung committed
104

105
  Hypothesis sts_alloc : fupd M0 ( γ, start γ).
106
  Hypotheses start_finish :  γ, start γ  fupd M0 (finished γ).
Ralf Jung's avatar
Ralf Jung committed
107

108
  Hypothesis finished_not_start :  γ, start γ  finished γ  False.
Ralf Jung's avatar
Ralf Jung committed
109

110
  Hypothesis finished_dup :  γ, finished γ  finished γ  finished γ.
111

112
  (** We assume that we cannot update to false. *)
113
  Hypothesis consistency : ¬ (fupd M1 False).
114 115

  (** Some general lemmas and proof mode compatibility. *)
116
  Lemma inv_open' i P R : inv i P  (P - fupd M0 (P  fupd M1 R))  fupd M1 R.
117
  Proof.
118
    iIntros "(#HiP & HP)". iApply fupd_fupd. iApply inv_open; last first.
119 120 121 122
    { iSplit; first done. iExact "HP". }
    iIntros "(HP & HPw)". by iApply "HPw".
  Qed.

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).
126
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
127
    intros P Q; rewrite !bi.equiv_spec=> -[??]; split; by apply fupd_mono.
128 129
  Qed.

130
  Lemma fupd_frame_r E P Q : fupd E P  Q  fupd E (P  Q).
131
  Proof. by rewrite comm fupd_frame_l comm. Qed.
132

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.
139

140 141
  Global Instance elim_fupd0_fupd1 p P Q :
    ElimModal True p false (fupd M0 P) P (fupd M1 Q) (fupd M1 Q).
142
  Proof.
143 144
    by rewrite /ElimModal bi.intuitionistically_if_elim
      fupd_frame_r bi.wand_elim_r fupd_mask_mono fupd_fupd.
145 146
  Qed.

147
  Global Instance exists_split_fupd0 {A} E P (Φ : A  PROP) :
148
    FromExist P Φ  FromExist (fupd E P) (λ a, fupd E (Φ a)).
149
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
150 151
    rewrite /FromExist=>HP. apply bi.exist_elim=> a.
    apply fupd_mono. by rewrite -HP -(bi.exist_intro a).
152 153
  Qed.

Derek Dreyer's avatar
Derek Dreyer committed
154
  (** Now to the actual counterexample. We start with a weird form of saved propositions. *)
155 156
  Definition saved (γ : gname) (P : PROP) : PROP :=
    ( i, inv i (start γ  (finished γ   P)))%I.
157
  Global Instance saved_persistent γ P : Persistent (saved γ P) := _.
158

159
  Lemma saved_alloc (P : gname  PROP) : fupd M1 ( γ, saved γ (P γ)).
160
  Proof.
161
    iIntros "". iMod (sts_alloc) as (γ) "Hs".
162
    iMod (inv_alloc (start γ  (finished γ   (P γ)))%I with "[Hs]") as (i) "#Hi".
163
    { auto. }
164
    iApply fupd_intro. by iExists γ, i.
165 166
  Qed.

167
  Lemma saved_cast γ P Q : saved γ P  saved γ Q   P  fupd M1 ( Q).
168
  Proof.
Ralf Jung's avatar
Ralf Jung committed
169
    iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP".
170
    iApply (inv_open' i). iSplit; first done.
171
    iIntros "HaP". iAssert (fupd M0 (finished γ)) with "[HaP]" as "> Hf".
Ralf Jung's avatar
Ralf Jung committed
172 173
    { iDestruct "HaP" as "[Hs | [Hf _]]".
      - by iApply start_finish.
174
      - by iApply fupd_intro. }
175
    iDestruct (finished_dup with "Hf") as "[Hf Hf']".
176
    iApply fupd_intro. iSplitL "Hf'"; first by eauto.
Ralf Jung's avatar
Ralf Jung committed
177
    (* Step 2: Open the Q-invariant. *)
178
    iClear (i) "HiP ". iDestruct "HsQ" as (i) "HiQ".
Ralf Jung's avatar
Ralf Jung committed
179 180
    iApply (inv_open' i). iSplit; first done.
    iIntros "[HaQ | [_ #HQ]]".
181
    { iExFalso. iApply finished_not_start. by iFrame. }
182
    iApply fupd_intro. iSplitL "Hf".
183
    { iRight. by iFrame. }
184
    by iApply fupd_intro.
185 186
  Qed.

187
  (** And now we tie a bad knot. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
188
  Notation "¬ P" := ( (P - fupd M1 False))%I : bi_scope.
189
  Definition A i : PROP := ( P, ¬P  saved i P)%I.
190
  Global Instance A_persistent i : Persistent (A i) := _.
191

192
  Lemma A_alloc : fupd M1 ( i, saved i (A i)).
193
  Proof. by apply saved_alloc. Qed.
194

195
  Lemma saved_NA i : saved i (A i)  ¬A i.
196
  Proof.
Ralf Jung's avatar
Ralf Jung committed
197 198
    iIntros "#Hi !# #HA". iPoseProof "HA" as "HA'".
    iDestruct "HA'" as (P) "#[HNP Hi']".
199
    iMod (saved_cast i (A i) P with "[]") as "HP".
200
    { eauto. }
Ralf Jung's avatar
Ralf Jung committed
201
    by iApply "HNP".
202
  Qed.
203

204
  Lemma saved_A i : saved i (A i)  A i.
205
  Proof.
206 207
    iIntros "#Hi". iExists (A i). iFrame "#".
    by iApply saved_NA.
208
  Qed.
209

210
  Lemma contradiction : False.
211
  Proof using All.
Ralf Jung's avatar
Ralf Jung committed
212
    apply consistency. iIntros "".
213
    iMod A_alloc as (i) "#H".
214 215
    iPoseProof (saved_NA with "H") as "HN".
    iApply "HN". iApply saved_A. done.
216 217
  Qed.
End inv. End inv.
218 219

(** This proves that if we have linear impredicative invariants, we can still
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.
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's avatar
Ralf Jung committed
237
  (** We have cancelable invariants. (Really they would have fractions at
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.
270
End linear1. End linear1.
271

272 273
(** This proves that if we have linear impredicative invariants, we can still
drop arbitrary resources (i.e., we can "defeat" linearity).
Ralf Jung's avatar
Ralf Jung committed
274
Variant 2: the invariant can depend on the chosen [γ], and we also have
275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290
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's avatar
Ralf Jung committed
291
  (** We have cancelable invariants. (Really they would have fractions at
292 293 294
  [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).
295 296 297
  (** [cinv_alloc] delays handing out the [cinv_own] token until after the
  invariant has been created so that this can match Iron by picking
  [cinv_own γ := fcinv_own γ 1 ∗ fcinv_cancel_own γ 1]. *)
298
  Hypothesis cinv_alloc :  E,
299
    fupd E E ( γ,  P,  P - fupd E E (cinv γ P  cinv_own γ))%I.
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
  Hypothesis cinv_access :  P γ,
    cinv γ P - cinv_own γ - fupd M1 M0 ( P  cinv_own γ  ( P - fupd M0 M1 emp)).

  (** 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".
325
    iMod cinv_alloc as (γ) "Hmkinv".
Ralf Jung's avatar
Ralf Jung committed
326 327 328
    iMod ("Hmkinv" $! True%I with "[//]") as "[Hinv Htok]".
    iMod (cinv_access with "Hinv Htok") as "(Htrue & Htok & Hclose)".
    iApply "Hclose". done.
329 330
  Qed.
End linear2. End linear2.