ghost_map.v 10.9 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
2
3
4
(** A "ghost map" (or "ghost heap") with a proposition controlling authoritative
ownership of the entire heap, and a "points-to-like" proposition for (mutable,
fractional, or persistent read-only) ownership of individual elements. *)
From iris.bi.lib Require Import fractional.
Ralf Jung's avatar
Ralf Jung committed
5
From iris.proofmode Require Import proofmode.
Ralf Jung's avatar
Ralf Jung committed
6
7
From iris.algebra Require Import gmap_view.
From iris.algebra Require Export dfrac.
Ralf Jung's avatar
Ralf Jung committed
8
From iris.base_logic.lib Require Export own.
Ralf Jung's avatar
Ralf Jung committed
9
From iris.prelude Require Import options.
Ralf Jung's avatar
Ralf Jung committed
10
11
12
13
14

(** The CMRA we need.
FIXME: This is intentionally discrete-only, but
should we support setoids via [Equiv]? *)
Class ghost_mapG Σ (K V : Type) `{Countable K} := GhostMapG {
15
  ghost_map_inG : inG Σ (gmap_viewR K (leibnizO V));
Ralf Jung's avatar
Ralf Jung committed
16
}.
17
Local Existing Instance ghost_map_inG.
Ralf Jung's avatar
Ralf Jung committed
18
19
Definition ghost_mapΣ (K V : Type) `{Countable K} : gFunctors :=
  #[ GFunctor (gmap_viewR K (leibnizO V)) ].
Ralf Jung's avatar
Ralf Jung committed
20

Ralf Jung's avatar
Ralf Jung committed
21
Global Instance subG_ghost_mapΣ Σ (K V : Type) `{Countable K} :
Ralf Jung's avatar
Ralf Jung committed
22
23
24
25
26
27
28
  subG (ghost_mapΣ K V) Σ  ghost_mapG Σ K V.
Proof. solve_inG. Qed.

Section definitions.
  Context `{ghost_mapG Σ K V}.

  Definition ghost_map_auth_def (γ : gname) (q : Qp) (m : gmap K V) : iProp Σ :=
29
    own γ (gmap_view_auth (V:=leibnizO V) (DfracOwn q) m).
Ralf Jung's avatar
Ralf Jung committed
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
  Definition ghost_map_auth_aux : seal (@ghost_map_auth_def). Proof. by eexists. Qed.
  Definition ghost_map_auth := ghost_map_auth_aux.(unseal).
  Definition ghost_map_auth_eq : @ghost_map_auth = @ghost_map_auth_def := ghost_map_auth_aux.(seal_eq).

  Definition ghost_map_elem_def (γ : gname) (k : K) (dq : dfrac) (v : V) : iProp Σ :=
    own γ (gmap_view_frag (V:=leibnizO V) k dq v).
  Definition ghost_map_elem_aux : seal (@ghost_map_elem_def). Proof. by eexists. Qed.
  Definition ghost_map_elem := ghost_map_elem_aux.(unseal).
  Definition ghost_map_elem_eq : @ghost_map_elem = @ghost_map_elem_def := ghost_map_elem_aux.(seal_eq).
End definitions.

(** FIXME: Refactor these notations using custom entries once Coq bug #13654
has been fixed. *)
Notation "k ↪[ γ ]{ dq } v" := (ghost_map_elem γ k dq v)
  (at level 20, γ at level 50, dq at level 50, format "k  ↪[ γ ]{ dq }  v") : bi_scope.
Notation "k ↪[ γ ]{# q } v" := (k [γ]{DfracOwn q} v)%I
  (at level 20, γ at level 50, q at level 50, format "k  ↪[ γ ]{# q }  v") : bi_scope.
Ralf Jung's avatar
Ralf Jung committed
47
48
49
50
Notation "k ↪[ γ ] v" := (k [γ]{#1} v)%I
  (at level 20, γ at level 50, format "k  ↪[ γ ]  v") : bi_scope.
Notation "k ↪[ γ ]□ v" := (k [γ]{DfracDiscarded} v)%I
  (at level 20, γ at level 50) : bi_scope.
Ralf Jung's avatar
Ralf Jung committed
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70

Local Ltac unseal := rewrite
  ?ghost_map_auth_eq /ghost_map_auth_def
  ?ghost_map_elem_eq /ghost_map_elem_def.

Section lemmas.
  Context `{ghost_mapG Σ K V}.
  Implicit Types (k : K) (v : V) (dq : dfrac) (q : Qp) (m : gmap K V).

  (** * Lemmas about the map elements *)
  Global Instance ghost_map_elem_timeless k γ dq v : Timeless (k [γ]{dq} v).
  Proof. unseal. apply _. Qed.
  Global Instance ghost_map_elem_persistent k γ v : Persistent (k [γ] v).
  Proof. unseal. apply _. Qed.
  Global Instance ghost_map_elem_fractional k γ v : Fractional (λ q, k [γ]{#q} v)%I.
  Proof. unseal. intros p q. rewrite -own_op gmap_view_frag_add //. Qed.
  Global Instance ghost_map_elem_as_fractional k γ q v :
    AsFractional (k [γ]{#q} v) (λ q, k [γ]{#q} v)%I q.
  Proof. split; first done. apply _. Qed.

71
72
73
74
75
76
77
78
79
  Local Lemma ghost_map_elems_unseal γ m dq :
    ([ map] k  v  m, k [γ]{dq} v) ==
    own γ ([^op map] kv  m, gmap_view_frag (V:=leibnizO V) k dq v).
  Proof.
    unseal. destruct (decide (m = )) as [->|Hne].
    - rewrite !big_opM_empty. iIntros "_". iApply own_unit.
    - rewrite big_opM_own //. iIntros "?". done.
  Qed.

Ralf Jung's avatar
Ralf Jung committed
80
  Lemma ghost_map_elem_valid k γ dq v : k [γ]{dq} v - ⌜✓ dq.
Ralf Jung's avatar
Ralf Jung committed
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
  Proof.
    unseal. iIntros "Helem".
    iDestruct (own_valid with "Helem") as %?%gmap_view_frag_valid.
    done.
  Qed.
  Lemma ghost_map_elem_valid_2 k γ dq1 dq2 v1 v2 :
    k [γ]{dq1} v1 - k [γ]{dq2} v2 - ⌜✓ (dq1  dq2)  v1 = v2.
  Proof.
    unseal. iIntros "H1 H2".
    iDestruct (own_valid_2 with "H1 H2") as %?%gmap_view_frag_op_valid_L.
    done.
  Qed.
  Lemma ghost_map_elem_agree k γ dq1 dq2 v1 v2 :
    k [γ]{dq1} v1 - k [γ]{dq2} v2 - v1 = v2.
  Proof.
    iIntros "Helem1 Helem2".
    iDestruct (ghost_map_elem_valid_2 with "Helem1 Helem2") as %[_ ?].
    done.
  Qed.

  Lemma ghost_map_elem_combine k γ dq1 dq2 v1 v2 :
    k [γ]{dq1} v1 - k [γ]{dq2} v2 - k [γ]{dq1  dq2} v1  v1 = v2.
  Proof.
    iIntros "Hl1 Hl2". iDestruct (ghost_map_elem_agree with "Hl1 Hl2") as %->.
    unseal. iCombine "Hl1 Hl2" as "Hl". eauto with iFrame.
  Qed.

Ralf Jung's avatar
Ralf Jung committed
108
  Lemma ghost_map_elem_frac_ne γ k1 k2 dq1 dq2 v1 v2 :
Ralf Jung's avatar
Ralf Jung committed
109
110
111
112
113
    ¬  (dq1  dq2)  k1 [γ]{dq1} v1 - k2 [γ]{dq2} v2 - k1  k2.
  Proof.
    iIntros (?) "H1 H2"; iIntros (->).
    by iDestruct (ghost_map_elem_valid_2 with "H1 H2") as %[??].
  Qed.
Ralf Jung's avatar
Ralf Jung committed
114
  Lemma ghost_map_elem_ne γ k1 k2 dq2 v1 v2 :
Ralf Jung's avatar
Ralf Jung committed
115
    k1 [γ] v1 - k2 [γ]{dq2} v2 - k1  k2.
Ralf Jung's avatar
Ralf Jung committed
116
  Proof. apply ghost_map_elem_frac_ne. apply: exclusive_l. Qed.
Ralf Jung's avatar
Ralf Jung committed
117
118

  (** Make an element read-only. *)
Ralf Jung's avatar
Ralf Jung committed
119
120
  Lemma ghost_map_elem_persist k γ dq v :
    k [γ]{dq} v == k [γ] v.
121
  Proof. unseal. iApply own_update. apply gmap_view_frag_persist. Qed.
Ralf Jung's avatar
Ralf Jung committed
122
123
124
125
126
127
128

  (** * Lemmas about [ghost_map_auth] *)
  Lemma ghost_map_alloc_strong P m :
    pred_infinite P 
     |==>  γ, P γ⌝  ghost_map_auth γ 1 m  [ map] k  v  m, k [γ] v.
  Proof.
    unseal. intros.
129
    iMod (own_alloc_strong (gmap_view_auth (V:=leibnizO V) (DfracOwn 1) ) P)
Ralf Jung's avatar
Ralf Jung committed
130
      as (γ) "[% Hauth]"; first done.
Ralf Jung's avatar
Ralf Jung committed
131
132
133
134
135
136
137
138
    { apply gmap_view_auth_valid. }
    iExists γ. iSplitR; first done.
    rewrite -big_opM_own_1 -own_op. iApply (own_update with "Hauth").
    etrans; first apply: (gmap_view_alloc_big (V:=leibnizO V) _ m (DfracOwn 1)).
    - apply map_disjoint_empty_r.
    - done.
    - rewrite right_id. done.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
139
140
  Lemma ghost_map_alloc_strong_empty P :
    pred_infinite P 
Ralf Jung's avatar
Ralf Jung committed
141
     |==>  γ, P γ⌝  ghost_map_auth γ 1 ( : gmap K V).
Ralf Jung's avatar
Ralf Jung committed
142
143
144
  Proof.
    intros. iMod (ghost_map_alloc_strong P ) as (γ) "(% & Hauth & _)"; eauto.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
145
146
147
148
149
150
151
  Lemma ghost_map_alloc m :
     |==>  γ, ghost_map_auth γ 1 m  [ map] k  v  m, k [γ] v.
  Proof.
    iMod (ghost_map_alloc_strong (λ _, True) m) as (γ) "[_ Hmap]".
    - by apply pred_infinite_True.
    - eauto.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
152
  Lemma ghost_map_alloc_empty :
Ralf Jung's avatar
Ralf Jung committed
153
     |==>  γ, ghost_map_auth γ 1 ( : gmap K V).
Ralf Jung's avatar
Ralf Jung committed
154
155
156
  Proof.
    intros. iMod (ghost_map_alloc ) as (γ) "(Hauth & _)"; eauto.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
157
158
159
160

  Global Instance ghost_map_auth_timeless γ q m : Timeless (ghost_map_auth γ q m).
  Proof. unseal. apply _. Qed.
  Global Instance ghost_map_auth_fractional γ m : Fractional (λ q, ghost_map_auth γ q m)%I.
Ralf Jung's avatar
Ralf Jung committed
161
  Proof. intros p q. unseal. rewrite -own_op -gmap_view_auth_dfrac_op //. Qed.
Ralf Jung's avatar
Ralf Jung committed
162
163
164
165
166
167
168
  Global Instance ghost_map_auth_as_fractional γ q m :
    AsFractional (ghost_map_auth γ q m) (λ q, ghost_map_auth γ q m)%I q.
  Proof. split; first done. apply _. Qed.

  Lemma ghost_map_auth_valid γ q m : ghost_map_auth γ q m - q  1%Qp.
  Proof.
    unseal. iIntros "Hauth".
169
    iDestruct (own_valid with "Hauth") as %?%gmap_view_auth_dfrac_valid.
Ralf Jung's avatar
Ralf Jung committed
170
171
172
    done.
  Qed.
  Lemma ghost_map_auth_valid_2 γ q1 q2 m1 m2 :
Ralf Jung's avatar
Ralf Jung committed
173
    ghost_map_auth γ q1 m1 - ghost_map_auth γ q2 m2 - (q1 + q2  1)%Qp  m1 = m2.
Ralf Jung's avatar
Ralf Jung committed
174
175
  Proof.
    unseal. iIntros "H1 H2".
176
    iDestruct (own_valid_2 with "H1 H2") as %[??]%gmap_view_auth_dfrac_op_valid_L.
Ralf Jung's avatar
Ralf Jung committed
177
178
179
    done.
  Qed.
  Lemma ghost_map_auth_agree γ q1 q2 m1 m2 :
Ralf Jung's avatar
Ralf Jung committed
180
    ghost_map_auth γ q1 m1 - ghost_map_auth γ q2 m2 - m1 = m2.
Ralf Jung's avatar
Ralf Jung committed
181
182
183
184
185
186
187
  Proof.
    iIntros "H1 H2".
    iDestruct (ghost_map_auth_valid_2 with "H1 H2") as %[_ ?].
    done.
  Qed.

  (** * Lemmas about the interaction of [ghost_map_auth] with the elements *)
Ralf Jung's avatar
tweaks    
Ralf Jung committed
188
  Lemma ghost_map_lookup {γ q m k dq v} :
Ralf Jung's avatar
Ralf Jung committed
189
190
191
    ghost_map_auth γ q m - k [γ]{dq} v - m !! k = Some v.
  Proof.
    unseal. iIntros "Hauth Hel".
192
    iDestruct (own_valid_2 with "Hauth Hel") as %[?[??]]%gmap_view_both_dfrac_valid_L.
Ralf Jung's avatar
Ralf Jung committed
193
194
195
    eauto.
  Qed.

Ralf Jung's avatar
Ralf Jung committed
196
  Lemma ghost_map_insert {γ m} k v :
Ralf Jung's avatar
Ralf Jung committed
197
198
199
200
201
202
    m !! k = None 
    ghost_map_auth γ 1 m == ghost_map_auth γ 1 (<[k := v]> m)  k [γ] v.
  Proof.
    unseal. intros ?. rewrite -own_op.
    iApply own_update. apply: gmap_view_alloc; done.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
203
204
205
206
207
208
209
210
  Lemma ghost_map_insert_persist {γ m} k v :
    m !! k = None 
    ghost_map_auth γ 1 m == ghost_map_auth γ 1 (<[k := v]> m)  k [γ] v.
  Proof.
    iIntros (?) "Hauth".
    iMod (ghost_map_insert k with "Hauth") as "[$ Helem]"; first done.
    iApply ghost_map_elem_persist. done.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
211

Ralf Jung's avatar
Ralf Jung committed
212
213
  Lemma ghost_map_delete {γ m k v} :
    ghost_map_auth γ 1 m - k [γ] v == ghost_map_auth γ 1 (delete k m).
Ralf Jung's avatar
Ralf Jung committed
214
  Proof.
Ralf Jung's avatar
Ralf Jung committed
215
    unseal. apply bi.wand_intro_r. rewrite -own_op.
Ralf Jung's avatar
Ralf Jung committed
216
217
218
    iApply own_update. apply: gmap_view_delete.
  Qed.

Ralf Jung's avatar
Ralf Jung committed
219
220
221
  Lemma ghost_map_update {γ m k v} w :
    ghost_map_auth γ 1 m - k [γ] v == ghost_map_auth γ 1 (<[k := w]> m)  k [γ] w.
  Proof.
222
223
    unseal. apply bi.wand_intro_r. rewrite -!own_op.
    apply own_update. apply: gmap_view_update.
Ralf Jung's avatar
Ralf Jung committed
224
225
  Qed.

226
  (** Big-op versions of above lemmas *)
Ralf Jung's avatar
tweaks    
Ralf Jung committed
227
228
  Lemma ghost_map_lookup_big {γ q m} m0 :
    ghost_map_auth γ q m -
229
230
231
    ([ map] kv  m0, k [γ] v) -
    m0  m.
  Proof.
232
233
234
235
    iIntros "Hauth Hfrag". rewrite map_subseteq_spec. iIntros (k v Hm0).
    iDestruct (ghost_map_lookup with "Hauth [Hfrag]") as %->.
    { rewrite big_sepM_lookup; done. }
    done.
236
237
  Qed.

238
239
240
241
242
  Lemma ghost_map_insert_big {γ m} m' :
    m' ## m 
    ghost_map_auth γ 1 m ==
    ghost_map_auth γ 1 (m'  m)  ([ map] k  v  m', k [γ] v).
  Proof.
243
244
    unseal. intros ?. rewrite -big_opM_own_1 -own_op.
    apply own_update. apply: gmap_view_alloc_big; done.
245
  Qed.
246
247
248
249
250
251
252
253
254
255
  Lemma ghost_map_insert_persist_big {γ m} m' :
    m' ## m 
    ghost_map_auth γ 1 m ==
    ghost_map_auth γ 1 (m'  m)  ([ map] k  v  m', k [γ] v).
  Proof.
    iIntros (Hdisj) "Hauth".
    iMod (ghost_map_insert_big m' with "Hauth") as "[$ Helem]"; first done.
    iApply big_sepM_bupd. iApply (big_sepM_impl with "Helem").
    iIntros "!#" (k v) "_". iApply ghost_map_elem_persist.
  Qed.
256

Ralf Jung's avatar
tweaks    
Ralf Jung committed
257
  Lemma ghost_map_delete_big {γ m} m0 :
258
    ghost_map_auth γ 1 m -
Ralf Jung's avatar
tweaks    
Ralf Jung committed
259
260
    ([ map] kv  m0, k [γ] v) ==
    ghost_map_auth γ 1 (m  m0).
261
  Proof.
262
263
264
    iIntros "Hauth Hfrag". iMod (ghost_map_elems_unseal with "Hfrag") as "Hfrag".
    unseal. iApply (own_update_2 with "Hauth Hfrag").
    apply: gmap_view_delete_big.
265
266
  Qed.

Ralf Jung's avatar
tweaks    
Ralf Jung committed
267
  Theorem ghost_map_update_big {γ m} m0 m1 :
268
269
    dom (gset K) m0 = dom (gset K) m1 
    ghost_map_auth γ 1 m -
Ralf Jung's avatar
tweaks    
Ralf Jung committed
270
271
    ([ map] kv  m0, k [γ] v) ==
    ghost_map_auth γ 1 (m1  m) 
272
273
        [ map] kv  m1, k [γ] v.
  Proof.
274
275
276
277
    iIntros (?) "Hauth Hfrag". iMod (ghost_map_elems_unseal with "Hfrag") as "Hfrag".
    unseal. rewrite -big_opM_own_1 -own_op.
    iApply (own_update_2 with "Hauth Hfrag").
    apply: gmap_view_update_big. done.
278
279
  Qed.

Ralf Jung's avatar
Ralf Jung committed
280
End lemmas.