counter_examples.v 7.12 KB
Newer Older
 Ralf Jung committed Aug 04, 2016 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 committed Aug 08, 2016 5 name-dependent allocation. *) Ralf Jung committed Aug 05, 2016 6 Module savedprop. Section savedprop. Ralf Jung committed Aug 04, 2016 7 8 Context (M : ucmraT). Notation iProp := (uPred M). Robbert Krebbers committed Aug 04, 2016 9 10 Notation "¬ P" := (□ (P → False))%I : uPred_scope. Implicit Types P : iProp. Ralf Jung committed Aug 04, 2016 11 Robbert Krebbers committed Oct 25, 2016 12 (** Saved Propositions and the update modality *) Robbert Krebbers committed Aug 05, 2016 13 Context (sprop : Type) (saved : sprop → iProp → iProp). Robbert Krebbers committed Aug 04, 2016 14 Hypothesis sprop_persistent : ∀ i P, PersistentP (saved i P). Ralf Jung committed Aug 04, 2016 15 Hypothesis sprop_alloc_dep : Robbert Krebbers committed Oct 25, 2016 16 ∀ (P : sprop → iProp), True ==★ (∃ i, saved i (P i)). Ralf Jung committed Aug 08, 2016 17 Hypothesis sprop_agree : ∀ i P Q, saved i P ∧ saved i Q ⊢ □ (P ↔ Q). Ralf Jung committed Aug 04, 2016 18 Ralf Jung committed Aug 08, 2016 19 20 21 (** A bad recursive reference: "Assertion with name [i] does not hold" *) Definition A (i : sprop) : iProp := ∃ P, ¬ P ★ saved i P. Robbert Krebbers committed Oct 25, 2016 22 Lemma A_alloc : True ==★ ∃ i, saved i (A i). Ralf Jung committed Aug 08, 2016 23 Proof. by apply sprop_alloc_dep. Qed. Ralf Jung committed Aug 04, 2016 24 Ralf Jung committed Aug 08, 2016 25 Lemma saved_NA i : saved i (A i) ⊢ ¬ A i. Ralf Jung committed Aug 04, 2016 26 Proof. Ralf Jung committed Aug 08, 2016 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. Ralf Jung committed Aug 04, 2016 32 33 Qed. Ralf Jung committed Aug 08, 2016 34 Lemma saved_A i : saved i (A i) ⊢ A i. Ralf Jung committed Aug 04, 2016 35 Proof. Ralf Jung committed Aug 08, 2016 36 37 iIntros "#Hs". iExists (A i). iFrame "#". by iApply saved_NA. Ralf Jung committed Aug 04, 2016 38 Qed. Robbert Krebbers committed Aug 05, 2016 39 40 41 42 Lemma contradiction : False. Proof. apply (@uPred.adequacy M False 1); simpl. Robbert Krebbers committed Oct 25, 2016 43 iIntros "". iUpd A_alloc as (i) "#H". Ralf Jung committed Aug 08, 2016 44 iPoseProof (saved_NA with "H") as "HN". Robbert Krebbers committed Oct 25, 2016 45 iUpdIntro. iNext. Ralf Jung committed Aug 08, 2016 46 iApply "HN". iApply saved_A. done. Robbert Krebbers committed Aug 05, 2016 47 Qed. Ralf Jung committed Aug 08, 2016 48 Ralf Jung committed Aug 05, 2016 49 End savedprop. End savedprop. Ralf Jung committed Aug 05, 2016 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. *) Ralf Jung committed Aug 05, 2016 53 Module inv. Section inv. Ralf Jung committed Aug 05, 2016 54 55 56 57 58 Context (M : ucmraT). Notation iProp := (uPred M). Implicit Types P : iProp. (** Assumptions *) Robbert Krebbers committed Oct 25, 2016 59 (** We have the update modality (two classes: empty/full mask) *) Robbert Krebbers committed Aug 05, 2016 60 Inductive mask := M0 | M1. Robbert Krebbers committed Oct 25, 2016 61 Context (fupd : mask → iProp → iProp). Ralf Jung committed Aug 05, 2016 62 Robbert Krebbers committed Oct 25, 2016 63 64 65 66 67 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. Hypothesis fupd_frame_l : ∀ E P Q, P ★ fupd E Q ⊢ fupd E (P ★ Q). Hypothesis fupd_mask_mono : ∀ P, fupd M0 P ⊢ fupd M1 P. Ralf Jung committed Aug 05, 2016 68 Robbert Krebbers committed Oct 25, 2016 69 (** We have invariants *) Ralf Jung committed Aug 05, 2016 70 Context (name : Type) (inv : name → iProp → iProp). Robbert Krebbers committed Aug 05, 2016 71 Hypothesis inv_persistent : ∀ i P, PersistentP (inv i P). Robbert Krebbers committed Oct 25, 2016 72 Hypothesis inv_alloc : ∀ P, P ⊢ fupd M1 (∃ i, inv i P). Ralf Jung committed Aug 05, 2016 73 Hypothesis inv_open : Robbert Krebbers committed Oct 25, 2016 74 ∀ i P Q R, (P ★ Q ⊢ fupd M0 (P ★ R)) → (inv i P ★ Q ⊢ fupd M1 R). Ralf Jung committed Aug 05, 2016 75 Ralf Jung committed Aug 05, 2016 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. *) Ralf Jung committed Aug 08, 2016 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 committed Aug 05, 2016 85 86 87 Context (gname : Type). Context (start finished : gname → iProp). Robbert Krebbers committed Oct 25, 2016 88 89 Hypothesis sts_alloc : True ⊢ fupd M0 (∃ γ, start γ). Hypotheses start_finish : ∀ γ, start γ ⊢ fupd M0 (finished γ). Ralf Jung committed Aug 05, 2016 90 Robbert Krebbers committed Aug 05, 2016 91 Hypothesis finished_not_start : ∀ γ, start γ ★ finished γ ⊢ False. Ralf Jung committed Aug 05, 2016 92 Robbert Krebbers committed Aug 05, 2016 93 Hypothesis finished_dup : ∀ γ, finished γ ⊢ finished γ ★ finished γ. Ralf Jung committed Aug 05, 2016 94 Robbert Krebbers committed Oct 25, 2016 95 96 (** We assume that we cannot update to false. *) Hypothesis consistency : ¬ (True ⊢ fupd M1 False). Ralf Jung committed Aug 05, 2016 97 98 (** Some general lemmas and proof mode compatibility. *) Robbert Krebbers committed Oct 25, 2016 99 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 100 Proof. Robbert Krebbers committed Oct 25, 2016 101 iIntros "(#HiP & HP)". iApply fupd_fupd. iApply inv_open; last first. Ralf Jung committed Aug 05, 2016 102 103 104 105 { iSplit; first done. iExact "HP". } iIntros "(HP & HPw)". by iApply "HPw". Qed. Robbert Krebbers committed Oct 25, 2016 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). Ralf Jung committed Aug 05, 2016 109 Proof. Robbert Krebbers committed Oct 25, 2016 110 intros P Q; rewrite !uPred.equiv_spec=> -[??]; split; by apply fupd_mono. Ralf Jung committed Aug 05, 2016 111 112 Qed. Robbert Krebbers committed Oct 25, 2016 113 114 Lemma fupd_frame_r E P Q : (fupd E P ★ Q) ⊢ fupd E (P ★ Q). Proof. by rewrite comm fupd_frame_l comm. Qed. Ralf Jung committed Aug 05, 2016 115 Robbert Krebbers committed Oct 25, 2016 116 117 Global Instance elim_fupd_fupd E P Q : ElimUpd (fupd E P) P (fupd E Q) (fupd E Q). Proof. by rewrite /ElimUpd fupd_frame_r uPred.wand_elim_r fupd_fupd. Qed. Ralf Jung committed Aug 05, 2016 118 Robbert Krebbers committed Oct 25, 2016 119 Global Instance elim_fupd0_fupd1 P Q : ElimUpd (fupd M0 P) P (fupd M1 Q) (fupd M1 Q). Ralf Jung committed Aug 05, 2016 120 Proof. Robbert Krebbers committed Oct 25, 2016 121 by rewrite /ElimUpd fupd_frame_r uPred.wand_elim_r fupd_mask_mono fupd_fupd. Ralf Jung committed Aug 05, 2016 122 123 Qed. Robbert Krebbers committed Oct 25, 2016 124 125 Global Instance exists_split_fupd0 {A} E P (Φ : A → iProp) : FromExist P Φ → FromExist (fupd E P) (λ a, fupd E (Φ a)). Ralf Jung committed Aug 05, 2016 126 127 Proof. rewrite /FromExist=>HP. apply uPred.exist_elim=> a. Robbert Krebbers committed Oct 25, 2016 128 apply fupd_mono. by rewrite -HP -(uPred.exist_intro a). Ralf Jung committed Aug 05, 2016 129 130 Qed. Derek Dreyer committed Aug 08, 2016 131 (** Now to the actual counterexample. We start with a weird form of saved propositions. *) Ralf Jung committed Aug 05, 2016 132 Definition saved (γ : gname) (P : iProp) : iProp := Robbert Krebbers committed Aug 05, 2016 133 134 ∃ i, inv i (start γ ∨ (finished γ ★ □ P)). Global Instance saved_persistent γ P : PersistentP (saved γ P) := _. Ralf Jung committed Aug 05, 2016 135 Robbert Krebbers committed Oct 25, 2016 136 Lemma saved_alloc (P : gname → iProp) : True ⊢ fupd M1 (∃ γ, saved γ (P γ)). Ralf Jung committed Aug 05, 2016 137 Proof. Robbert Krebbers committed Oct 25, 2016 138 139 iIntros "". iUpd (sts_alloc) as (γ) "Hs". iUpd (inv_alloc (start γ ∨ (finished γ ★ □ (P γ))) with "[Hs]") as (i) "#Hi". Robbert Krebbers committed Aug 05, 2016 140 { auto. } Robbert Krebbers committed Oct 25, 2016 141 iApply fupd_intro. by iExists γ, i. Ralf Jung committed Aug 05, 2016 142 143 Qed. Robbert Krebbers committed Oct 25, 2016 144 Lemma saved_cast γ P Q : saved γ P ★ saved γ Q ★ □ P ⊢ fupd M1 (□ Q). Ralf Jung committed Aug 05, 2016 145 Proof. Ralf Jung committed Aug 05, 2016 146 iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP". Ralf Jung committed Aug 05, 2016 147 iApply (inv_open' i). iSplit; first done. Robbert Krebbers committed Oct 25, 2016 148 iIntros "HaP". iAssert (fupd M0 (finished γ)) with "[HaP]" as "==> Hf". Ralf Jung committed Aug 05, 2016 149 150 { iDestruct "HaP" as "[Hs | [Hf _]]". - by iApply start_finish. Robbert Krebbers committed Oct 25, 2016 151 - by iApply fupd_intro. } Robbert Krebbers committed Aug 08, 2016 152 iDestruct (finished_dup with "Hf") as "[Hf Hf']". Robbert Krebbers committed Oct 25, 2016 153 iApply fupd_intro. iSplitL "Hf'"; first by eauto. Ralf Jung committed Aug 05, 2016 154 (* Step 2: Open the Q-invariant. *) Robbert Krebbers committed Sep 27, 2016 155 iClear (i) "HiP ". iDestruct "HsQ" as (i) "HiQ". Ralf Jung committed Aug 05, 2016 156 157 iApply (inv_open' i). iSplit; first done. iIntros "[HaQ | [_ #HQ]]". Robbert Krebbers committed Aug 05, 2016 158 { iExFalso. iApply finished_not_start. by iFrame. } Robbert Krebbers committed Oct 25, 2016 159 iApply fupd_intro. iSplitL "Hf". Robbert Krebbers committed Aug 05, 2016 160 { iRight. by iFrame. } Robbert Krebbers committed Oct 25, 2016 161 by iApply fupd_intro. Ralf Jung committed Aug 05, 2016 162 163 Qed. Ralf Jung committed Aug 05, 2016 164 (** And now we tie a bad knot. *) Robbert Krebbers committed Oct 25, 2016 165 Notation "¬ P" := (□ (P -★ fupd M1 False))%I : uPred_scope. Ralf Jung committed Aug 05, 2016 166 Definition A i : iProp := ∃ P, ¬P ★ saved i P. Robbert Krebbers committed Aug 05, 2016 167 Global Instance A_persistent i : PersistentP (A i) := _. Ralf Jung committed Aug 05, 2016 168 Robbert Krebbers committed Oct 25, 2016 169 Lemma A_alloc : True ⊢ fupd M1 (∃ i, saved i (A i)). Ralf Jung committed Aug 05, 2016 170 Proof. by apply saved_alloc. Qed. Ralf Jung committed Aug 05, 2016 171 Ralf Jung committed Aug 08, 2016 172 Lemma saved_NA i : saved i (A i) ⊢ ¬A i. Ralf Jung committed Aug 05, 2016 173 Proof. Ralf Jung committed Aug 05, 2016 174 175 iIntros "#Hi !# #HA". iPoseProof "HA" as "HA'". iDestruct "HA'" as (P) "#[HNP Hi']". Robbert Krebbers committed Oct 25, 2016 176 iUpd (saved_cast i (A i) P with "[]") as "HP". Ralf Jung committed Aug 08, 2016 177 { eauto. } Ralf Jung committed Aug 05, 2016 178 by iApply "HNP". Ralf Jung committed Aug 05, 2016 179 Qed. Ralf Jung committed Aug 05, 2016 180 Ralf Jung committed Aug 08, 2016 181 Lemma saved_A i : saved i (A i) ⊢ A i. Ralf Jung committed Aug 05, 2016 182 Proof. Ralf Jung committed Aug 08, 2016 183 184 iIntros "#Hi". iExists (A i). iFrame "#". by iApply saved_NA. Ralf Jung committed Aug 05, 2016 185 Qed. Ralf Jung committed Aug 05, 2016 186 Ralf Jung committed Aug 05, 2016 187 188 Lemma contradiction : False. Proof. Ralf Jung committed Oct 07, 2016 189 apply consistency. iIntros "". Robbert Krebbers committed Oct 25, 2016 190 iUpd A_alloc as (i) "#H". Ralf Jung committed Aug 08, 2016 191 192 iPoseProof (saved_NA with "H") as "HN". iApply "HN". iApply saved_A. done. Ralf Jung committed Aug 05, 2016 193 194 Qed. End inv. End inv.