counter_examples.v 7.1 KB
Newer Older
1
From iris.base_logic Require Import base_logic soundness.
2 3 4
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 the update modality *)
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), (|==> ( i, saved i (P i)))%I.
17
  Hypothesis sprop_agree :  i P Q, saved i P  saved i Q   (P  Q).
18

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

22
  Lemma A_alloc : (|==>  i, saved i (A i))%I.
23
  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

  Lemma contradiction : False.
  Proof.
42
    apply (@soundness M False 1); simpl.
43
    iIntros "". iMod A_alloc as (i) "#H".
44
    iPoseProof (saved_NA with "H") as "HN".
45
    iModIntro. iNext.
46
    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
  Context (M : ucmraT).
  Notation iProp := (uPred M).
  Implicit Types P : iProp.

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

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

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

Ralf Jung's avatar
Ralf Jung committed
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 () +_⊥ ()
  *)
Ralf Jung's avatar
Ralf Jung committed
85 86 87
  Context (gname : Type).
  Context (start finished : gname  iProp).

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

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

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

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

  (** Some general lemmas and proof mode compatibility. *)
99
  Lemma inv_open' i P R : inv i P  (P - fupd M0 (P  fupd M1 R))  fupd M1 R.
100
  Proof.
101
    iIntros "(#HiP & HP)". iApply fupd_fupd. 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 fupd_mono' E : Proper (() ==> ()) (fupd E).
  Proof. intros P Q ?. by apply fupd_mono. Qed.
  Instance fupd_proper E : Proper (() ==> ()) (fupd E).
109
  Proof.
110
    intros P Q; rewrite !uPred.equiv_spec=> -[??]; split; by apply fupd_mono.
111 112
  Qed.

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

116 117
  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.
118

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

124 125
  Global Instance exists_split_fupd0 {A} E P (Φ : A  iProp) :
    FromExist P Φ  FromExist (fupd E P) (λ a, fupd E (Φ a)).
126 127
  Proof.
    rewrite /FromExist=>HP. apply uPred.exist_elim=> a.
128
    apply fupd_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. *)
Ralf Jung's avatar
Ralf Jung committed
132
  Definition saved (γ : gname) (P : iProp) : iProp :=
133
     i, inv i (start γ  (finished γ   P)).
134
  Global Instance saved_persistent γ P : PersistentP (saved γ P) := _.
135

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

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

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

169
  Lemma A_alloc : fupd 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.
Ralf Jung's avatar
Ralf Jung committed
174 175
    iIntros "#Hi !# #HA". iPoseProof "HA" as "HA'".
    iDestruct "HA'" as (P) "#[HNP Hi']".
176
    iMod (saved_cast i (A i) P with "[]") as "HP".
177
    { eauto. }
Ralf Jung's avatar
Ralf Jung committed
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.
Ralf Jung's avatar
Ralf Jung committed
189
    apply consistency. iIntros "".
190
    iMod 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.