counter_examples.v 7.02 KB
Newer Older
1 2 3 4
From iris.algebra Require Import upred.
From iris.proofmode Require Import tactics.

(** This proves that we need the ▷ in a "Saved Proposition" construction with
Derek Dreyer's avatar
Derek Dreyer committed
5
name-dependent allocation. *)
6
Module savedprop. Section savedprop.
7 8
  Context (M : ucmraT).
  Notation iProp := (uPred M).
9 10
  Notation "¬ P" := ( (P  False))%I : uPred_scope.
  Implicit Types P : iProp.
11

12
  (* Saved Propositions and view shifts. *)
13
  Context (sprop : Type) (saved : sprop  iProp  iProp).
14
  Hypothesis sprop_persistent :  i P, PersistentP (saved i P).
15
  Hypothesis sprop_alloc_dep :
16
     (P : sprop  iProp), True =r=> ( i, saved i (P i)).
17
  Hypothesis sprop_agree :  i P Q, saved i P  saved i Q   (P  Q).
18

19 20 21 22 23
  (** A bad recursive reference: "Assertion with name [i] does not hold" *)
  Definition A (i : sprop) : iProp :=  P, ¬ P  saved i P.

  Lemma A_alloc : True =r=>  i, saved i (A i).
  Proof. by apply sprop_alloc_dep. Qed.
24

25
  Lemma saved_NA i : saved i (A i)  ¬ A i.
26
  Proof.
27 28 29 30 31
    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.
32 33
  Qed.

34
  Lemma saved_A i : saved i (A i)  A i.
35
  Proof.
36 37
    iIntros "#Hs". iExists (A i). iFrame "#".
    by iApply saved_NA.
38
  Qed.
39 40 41 42

  Lemma contradiction : False.
  Proof.
    apply (@uPred.adequacy M False 1); simpl.
43 44 45 46
    iIntros "". iVs A_alloc as (i) "#H".
    iPoseProof (saved_NA with "H") as "HN".
    iVsIntro. iNext.
    iApply "HN". iApply saved_A. done.
47
  Qed.
48

49
End savedprop. End savedprop.
50 51 52

(** This proves that we need the ▷ when opening invariants. *)
(** We fork in [uPred M] for any M, but the proof would work in any BI. *)
53
Module inv. Section inv.
54 55 56 57 58 59
  Context (M : ucmraT).
  Notation iProp := (uPred M).
  Implicit Types P : iProp.

  (** Assumptions *)
  (* We have view shifts (two classes: empty/full mask) *)
60 61
  Inductive mask := M0 | M1.
  Context (pvs : mask  iProp  iProp).
62

63 64 65 66 67
  Hypothesis pvs_intro :  E P, P  pvs E P.
  Hypothesis pvs_mono :  E P Q, (P  Q)  pvs E P  pvs E Q.
  Hypothesis pvs_pvs :  E P, pvs E (pvs E P)  pvs E P.
  Hypothesis pvs_frame_l :  E P Q, P  pvs E Q  pvs E (P  Q).
  Hypothesis pvs_mask_mono :  P, pvs M0 P  pvs M1 P.
68 69 70

  (* We have invariants *)
  Context (name : Type) (inv : name  iProp  iProp).
71
  Hypothesis inv_persistent :  i P, PersistentP (inv i P).
72
  Hypothesis inv_alloc :  P, P  pvs M1 ( i, inv i P).
73
  Hypothesis inv_open :
74
     i P Q R, (P  Q  pvs M0 (P  R))  (inv i P  Q  pvs M1 R).
75

76 77 78
  (* 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. *)
79 80 81 82 83 84
  (* 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.
     * Ex () +_⊥ ()
  *)
85 86 87
  Context (gname : Type).
  Context (start finished : gname  iProp).

88 89
  Hypothesis sts_alloc : True  pvs M0 ( γ, start γ).
  Hypotheses start_finish :  γ, start γ  pvs M0 (finished γ).
90

91
  Hypothesis finished_not_start :  γ, start γ  finished γ  False.
92

93
  Hypothesis finished_dup :  γ, finished γ  finished γ  finished γ.
94

Ralf Jung's avatar
Ralf Jung committed
95
  (* We assume that we cannot view shift to false. *)
96
  Hypothesis soundness : ¬ (True  pvs M1 False).
97 98

  (** Some general lemmas and proof mode compatibility. *)
99
  Lemma inv_open' i P R : inv i P  (P - pvs M0 (P  pvs M1 R))  pvs M1 R.
100
  Proof.
101
    iIntros "(#HiP & HP)". iApply pvs_pvs. iApply inv_open; last first.
102 103 104 105
    { iSplit; first done. iExact "HP". }
    iIntros "(HP & HPw)". by iApply "HPw".
  Qed.

106 107 108
  Instance pvs_mono' E : Proper (() ==> ()) (pvs E).
  Proof. intros P Q ?. by apply pvs_mono. Qed.
  Instance pvs_proper E : Proper (() ==> ()) (pvs E).
109
  Proof.
110
    intros P Q; rewrite !uPred.equiv_spec=> -[??]; split; by apply pvs_mono.
111 112
  Qed.

113 114
  Lemma pvs_frame_r E P Q : (pvs E P  Q)  pvs E (P  Q).
  Proof. by rewrite comm pvs_frame_l comm. Qed.
115

116 117
  Global Instance elim_pvs_pvs E P Q : ElimVs (pvs E P) P (pvs E Q) (pvs E Q).
  Proof. by rewrite /ElimVs pvs_frame_r uPred.wand_elim_r pvs_pvs. Qed.
118

119
  Global Instance elim_pvs0_pvs1 P Q : ElimVs (pvs M0 P) P (pvs M1 Q) (pvs M1 Q).
120
  Proof.
121
    by rewrite /ElimVs pvs_frame_r uPred.wand_elim_r pvs_mask_mono pvs_pvs.
122 123
  Qed.

124 125
  Global Instance exists_split_pvs0 {A} E P (Φ : A  iProp) :
    FromExist P Φ  FromExist (pvs E P) (λ a, pvs E (Φ a)).
126 127
  Proof.
    rewrite /FromExist=>HP. apply uPred.exist_elim=> a.
128
    apply pvs_mono. by rewrite -HP -(uPred.exist_intro a).
129 130
  Qed.

Derek Dreyer's avatar
Derek Dreyer committed
131
  (** Now to the actual counterexample. We start with a weird form of saved propositions. *)
132
  Definition saved (γ : gname) (P : iProp) : iProp :=
133 134
     i, inv i (start γ  (finished γ   P)).
  Global Instance saved_persistent γ P : PersistentP (saved γ P) := _.
135

136
  Lemma saved_alloc (P : gname  iProp) : True  pvs M1 ( γ, saved γ (P γ)).
137
  Proof.
138 139
    iIntros "". iVs (sts_alloc) as (γ) "Hs".
    iVs (inv_alloc (start γ  (finished γ   (P γ))) with "[Hs]") as (i) "#Hi".
140 141
    { auto. }
    iApply pvs_intro. by iExists γ, i.
142 143
  Qed.

144
  Lemma saved_cast γ P Q : saved γ P  saved γ Q   P  pvs M1 ( Q).
145
  Proof.
146
    iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP".
147
    iApply (inv_open' i). iSplit; first done.
148
    iIntros "HaP". iAssert (pvs M0 (finished γ)) with "[HaP]" as "==> Hf".
149 150
    { iDestruct "HaP" as "[Hs | [Hf _]]".
      - by iApply start_finish.
151
      - by iApply pvs_intro. }
152
    iDestruct (finished_dup with "Hf") as "[Hf Hf']".
153
    iApply pvs_intro. iSplitL "Hf'"; first by eauto.
154
    (* Step 2: Open the Q-invariant. *)
155
    iClear (i) "HiP ". iDestruct "HsQ" as (i) "HiQ".
156 157
    iApply (inv_open' i). iSplit; first done.
    iIntros "[HaQ | [_ #HQ]]".
158 159 160 161
    { iExFalso. iApply finished_not_start. by iFrame. }
    iApply pvs_intro. iSplitL "Hf".
    { iRight. by iFrame. }
    by iApply pvs_intro.
162 163
  Qed.

164
  (** And now we tie a bad knot. *)
165
  Notation "¬ P" := ( (P - pvs M1 False))%I : uPred_scope.
166
  Definition A i : iProp :=  P, ¬P  saved i P.
167
  Global Instance A_persistent i : PersistentP (A i) := _.
168

169
  Lemma A_alloc : True  pvs M1 ( i, saved i (A i)).
170
  Proof. by apply saved_alloc. Qed.
171

172
  Lemma saved_NA i : saved i (A i)  ¬A i.
173
  Proof.
174 175
    iIntros "#Hi !# #HA". iPoseProof "HA" as "HA'".
    iDestruct "HA'" as (P) "#[HNP Hi']".
176 177
    iVs (saved_cast i (A i) P with "[]") as "HP".
    { eauto. }
178
    by iApply "HNP".
179
  Qed.
180

181
  Lemma saved_A i : saved i (A i)  A i.
182
  Proof.
183 184
    iIntros "#Hi". iExists (A i). iFrame "#".
    by iApply saved_NA.
185
  Qed.
186

187 188
  Lemma contradiction : False.
  Proof.
189 190
    apply soundness. iIntros "".
    iVs A_alloc as (i) "#H".
191 192
    iPoseProof (saved_NA with "H") as "HN".
    iApply "HN". iApply saved_A. done.
193 194
  Qed.
End inv. End inv.