counter_examples.v 7.13 KB
Newer Older
1
From iris.base_logic Require Import base_logic soundness.
2
From iris.proofmode Require Import tactics.
3
Set Default Proof Using "All".
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 9
  Context (M : ucmraT).
  Notation iProp := (uPred M).
10 11
  Notation "¬ P" := ( (P  False))%I : uPred_scope.
  Implicit Types P : iProp.
12

13
  (** Saved Propositions and the update modality *)
14
  Context (sprop : Type) (saved : sprop  iProp  iProp).
15
  Hypothesis sprop_persistent :  i P, PersistentP (saved i P).
16
  Hypothesis sprop_alloc_dep :
17
     (P : sprop  iProp), (|==> ( i, saved i (P i)))%I.
18
  Hypothesis sprop_agree :  i P Q, saved i P  saved i Q   (P  Q).
19

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

23
  Lemma A_alloc : (|==>  i, saved i (A i))%I.
24
  Proof. by apply sprop_alloc_dep. Qed.
25

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

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

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

50
End savedprop. End savedprop.
51 52 53

(** 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. *)
54
Module inv. Section inv.
55 56 57 58 59
  Context (M : ucmraT).
  Notation iProp := (uPred M).
  Implicit Types P : iProp.

  (** Assumptions *)
60
  (** We have the update modality (two classes: empty/full mask) *)
61
  Inductive mask := M0 | M1.
62
  Context (fupd : mask  iProp  iProp).
63

64 65 66
  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.
67
  Hypothesis fupd_frame_l :  E P Q, P  fupd E Q  fupd E (P  Q).
68
  Hypothesis fupd_mask_mono :  P, fupd M0 P  fupd M1 P.
69

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

Ralf Jung's avatar
Ralf Jung committed
77 78 79
  (* 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. *)
80 81 82 83 84 85
  (* 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 () +_⊥ ()
  *)
Ralf Jung's avatar
Ralf Jung committed
86 87 88
  Context (gname : Type).
  Context (start finished : gname  iProp).

89
  Hypothesis sts_alloc : fupd M0 ( γ, start γ).
90
  Hypotheses start_finish :  γ, start γ  fupd M0 (finished γ).
Ralf Jung's avatar
Ralf Jung committed
91

92
  Hypothesis finished_not_start :  γ, start γ  finished γ  False.
Ralf Jung's avatar
Ralf Jung committed
93

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

96
  (** We assume that we cannot update to false. *)
97
  Hypothesis consistency : ¬ (fupd M1 False).
98 99

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

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

114
  Lemma fupd_frame_r E P Q : fupd E P  Q  fupd E (P  Q).
115
  Proof. by rewrite comm fupd_frame_l comm. Qed.
116

117 118
  Global Instance elim_fupd_fupd E P Q : ElimModal (fupd E P) P (fupd E Q) (fupd E Q).
  Proof. by rewrite /ElimModal fupd_frame_r uPred.wand_elim_r fupd_fupd. Qed.
119

120
  Global Instance elim_fupd0_fupd1 P Q : ElimModal (fupd M0 P) P (fupd M1 Q) (fupd M1 Q).
121
  Proof.
122
    by rewrite /ElimModal fupd_frame_r uPred.wand_elim_r fupd_mask_mono fupd_fupd.
123 124
  Qed.

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

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

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

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

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

170
  Lemma A_alloc : fupd M1 ( i, saved i (A i)).
171
  Proof. by apply saved_alloc. Qed.
172

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

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

188 189
  Lemma contradiction : False.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
190
    apply consistency. iIntros "".
191
    iMod A_alloc as (i) "#H".
192 193
    iPoseProof (saved_NA with "H") as "HN".
    iApply "HN". iApply saved_A. done.
194 195
  Qed.
End inv. End inv.