gen_heap.v 15.2 KB
Newer Older
1
From stdpp Require Export namespaces.
2
From iris.algebra Require Import reservation_map agree frac.
3
From iris.algebra Require Export dfrac.
4
From iris.bi.lib Require Import fractional.
Ralf Jung's avatar
Ralf Jung committed
5
From iris.proofmode Require Import proofmode.
6
From iris.base_logic.lib Require Export own.
Ralf Jung's avatar
Ralf Jung committed
7
From iris.base_logic.lib Require Import ghost_map.
Ralf Jung's avatar
Ralf Jung committed
8
From iris.prelude Require Import options.
9
10
Import uPred.

Ralf Jung's avatar
Ralf Jung committed
11
(** This file provides a generic mechanism for a language-level point-to
12
connective [l ↦{dq} v] reflecting the physical heap.  This library is designed to
Ralf Jung's avatar
Ralf Jung committed
13
be used as a singleton (i.e., with only a single instance existing in any
14
proof), with the [gen_heapGS] typeclass providing the ghost names of that unique
Ralf Jung's avatar
Ralf Jung committed
15
16
17
18
instance.  That way, [mapsto] does not need an explicit [gname] parameter.
This mechanism can be plugged into a language and related to the physical heap
by using [gen_heap_interp σ] in the state interpretation of the weakest
precondition. See heap-lang for an example.
19

Ralf Jung's avatar
Ralf Jung committed
20
If you are looking for a library providing "ghost heaps" independent of the
Ralf Jung's avatar
Ralf Jung committed
21
22
23
physical state, you will likely want explicit ghost names to disambiguate
multiple heaps and are thus better off using [ghost_map], or (if you need more
flexibility), directly using the underlying [algebra.lib.gmap_view].
Robbert Krebbers's avatar
Robbert Krebbers committed
24

Ralf Jung's avatar
Ralf Jung committed
25
This library is generic in the types [L] for locations and [V] for values and
26
supports fractional permissions.  Next to the point-to connective [l ↦{dq} v],
Ralf Jung's avatar
Ralf Jung committed
27
28
which keeps track of the value [v] of a location [l], this library also provides
a way to attach "meta" or "ghost" data to locations. This is done as follows:
Robbert Krebbers's avatar
Robbert Krebbers committed
29
30

- When one allocates a location, in addition to the point-to connective [l ↦ v],
31
  one also obtains the token [meta_token l ⊤]. This token is an exclusive
Robbert Krebbers's avatar
Robbert Krebbers committed
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
  resource that denotes that no meta data has been associated with the
  namespaces in the mask [⊤] for the location [l].
- Meta data tokens can be split w.r.t. namespace masks, i.e.
  [meta_token l (E1 ∪ E2) ⊣⊢ meta_token l E1 ∗ meta_token l E2] if [E1 ## E2].
- Meta data can be set using the update [meta_token l E ==∗ meta l N x] provided
  [↑N ⊆ E], and [x : A] for any countable [A]. The [meta l N x] connective is
  persistent and denotes the knowledge that the meta data [x] has been
  associated with namespace [N] to the location [l].

To make the mechanism as flexible as possible, the [x : A] in [meta l N x] can
be of any countable type [A]. This means that you can associate e.g. single
ghost names, but also tuples of ghost names, etc.

To further increase flexibility, the [meta l N x] and [meta_token l E]
connectives are annotated with a namespace [N] and mask [E]. That way, one can
assign a map of meta information to a location. This is particularly useful when
building abstractions, then one can gradually assign more ghost information to a
location instead of having to do all of this at once. We use namespaces so that
these can be matched up with the invariant namespaces. *)

(** To implement this mechanism, we use three resource algebras:

Ralf Jung's avatar
Ralf Jung committed
54
55
56
57
- A [gmap_view L V], which keeps track of the values of locations.
- A [gmap_view L gname], which keeps track of the meta information of
  locations. More specifically, this RA introduces an indirection: it keeps
  track of a ghost name for each location.
Robbert Krebbers's avatar
Robbert Krebbers committed
58
- The ghost names in the aforementioned authoritative RA refer to namespace maps
59
  [reservation_map (agree positive)], which store the actual meta information.
Robbert Krebbers's avatar
Robbert Krebbers committed
60
61
  This indirection is needed because we cannot perform frame preserving updates
  in an authoritative fragment without owning the full authoritative element
62
  (in other words, without the indirection [meta_set] would need [gen_heap_interp]
Robbert Krebbers's avatar
Robbert Krebbers committed
63
  as a premise).
Ralf Jung's avatar
Ralf Jung committed
64
 *)
Robbert Krebbers's avatar
Robbert Krebbers committed
65

Ralf Jung's avatar
Ralf Jung committed
66
(** The CMRAs we need, and the global ghost names we are using. *)
67

68
Class gen_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
69
70
  gen_heapGpreS_heap : ghost_mapG Σ L V;
  gen_heapGpreS_meta : ghost_mapG Σ L gname;
71
  gen_heapGpreS_meta_data : inG Σ (reservation_mapR (agreeR positiveO));
72
}.
73
Local Existing Instances gen_heapGpreS_meta_data gen_heapGpreS_heap gen_heapGpreS_meta.
74

75
Class gen_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapGS {
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
76
  gen_heap_inG : gen_heapGpreS L V Σ;
Ralf Jung's avatar
Ralf Jung committed
77
78
79
  gen_heap_name : gname;
  gen_meta_name : gname
}.
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
80
Local Existing Instance gen_heap_inG.
81
Global Arguments GenHeapGS L V Σ {_ _ _} _ _.
Ralf Jung's avatar
Ralf Jung committed
82
83
Global Arguments gen_heap_name {L V Σ _ _} _ : assert.
Global Arguments gen_meta_name {L V Σ _ _} _ : assert.
84

85
Definition gen_heapΣ (L V : Type) `{Countable L} : gFunctors := #[
Ralf Jung's avatar
Ralf Jung committed
86
87
  ghost_mapΣ L V;
  ghost_mapΣ L gname;
88
  GFunctor (reservation_mapR (agreeR positiveO))
89
].
90

91
92
Global Instance subG_gen_heapGpreS {Σ L V} `{Countable L} :
  subG (gen_heapΣ L V) Σ  gen_heapGpreS L V Σ.
93
Proof. solve_inG. Qed.
94
95

Section definitions.
96
  Context `{Countable L, hG : !gen_heapGS L V Σ}.
97

98
  Definition gen_heap_interp (σ : gmap L V) : iProp Σ :=  m : gmap L gname,
Robbert Krebbers's avatar
Robbert Krebbers committed
99
100
    (* The [⊆] is used to avoid assigning ghost information to the locations in
    the initial heap (see [gen_heap_init]). *)
101
     dom m  dom σ  
Ralf Jung's avatar
Ralf Jung committed
102
103
    ghost_map_auth (gen_heap_name hG) 1 σ 
    ghost_map_auth (gen_meta_name hG) 1 m.
104

105
  Local Definition mapsto_def (l : L) (dq : dfrac) (v: V) : iProp Σ :=
Ralf Jung's avatar
Ralf Jung committed
106
    l [gen_heap_name hG]{dq} v.
107
  Local Definition mapsto_aux : seal (@mapsto_def). Proof. by eexists. Qed.
108
  Definition mapsto := mapsto_aux.(unseal).
109
  Local Definition mapsto_unseal : @mapsto = @mapsto_def := mapsto_aux.(seal_eq).
110

111
  Local Definition meta_token_def (l : L) (E : coPset) : iProp Σ :=
112
     γm, l [gen_meta_name hG] γm  own γm (reservation_map_token E).
113
  Local Definition meta_token_aux : seal (@meta_token_def). Proof. by eexists. Qed.
114
  Definition meta_token := meta_token_aux.(unseal).
115
116
  Local Definition meta_token_unseal :
    @meta_token = @meta_token_def := meta_token_aux.(seal_eq).
117

118
119
  (** TODO: The use of [positives_flatten] violates the namespace abstraction
  (see the proof of [meta_set]. *)
120
  Local Definition meta_def `{Countable A} (l : L) (N : namespace) (x : A) : iProp Σ :=
Ralf Jung's avatar
Ralf Jung committed
121
     γm, l [gen_meta_name hG] γm 
122
          own γm (reservation_map_data (positives_flatten N) (to_agree (encode x))).
123
  Local Definition meta_aux : seal (@meta_def). Proof. by eexists. Qed.
Ralf Jung's avatar
Ralf Jung committed
124
  Definition meta := meta_aux.(unseal).
125
  Local Definition meta_unseal : @meta = @meta_def := meta_aux.(seal_eq).
126
End definitions.
Ralf Jung's avatar
Ralf Jung committed
127
Global Arguments meta {L _ _ V Σ _ A _ _} l N x.
128

Robbert Krebbers's avatar
Robbert Krebbers committed
129
130
(** FIXME: Refactor these notations using custom entries once Coq bug #13654
has been fixed. *)
131
132
133
134
135
136
137
138
Local Notation "l ↦{ dq } v" := (mapsto l dq v)
  (at level 20, format "l  ↦{ dq }  v") : bi_scope.
Local Notation "l ↦□ v" := (mapsto l DfracDiscarded v)
  (at level 20, format "l  ↦□  v") : bi_scope.
Local Notation "l ↦{# q } v" := (mapsto l (DfracOwn q) v)
  (at level 20, format "l  ↦{# q }  v") : bi_scope.
Local Notation "l ↦ v" := (mapsto l (DfracOwn 1) v)
  (at level 20, format "l  ↦  v") : bi_scope.
139

140
Section gen_heap.
141
  Context {L V} `{Countable L, !gen_heapGS L V Σ}.
142
143
144
  Implicit Types P Q : iProp Σ.
  Implicit Types Φ : V  iProp Σ.
  Implicit Types σ : gmap L V.
145
  Implicit Types m : gmap L gname.
Robbert Krebbers's avatar
Robbert Krebbers committed
146
147
  Implicit Types l : L.
  Implicit Types v : V.
148
149

  (** General properties of mapsto *)
150
  Global Instance mapsto_timeless l dq v : Timeless (l {dq} v).
151
  Proof. rewrite mapsto_unseal. apply _. Qed.
152
  Global Instance mapsto_fractional l v : Fractional (λ q, l {#q} v)%I.
153
  Proof. rewrite mapsto_unseal. apply _. Qed.
154
  Global Instance mapsto_as_fractional l q v :
155
    AsFractional (l {#q} v) (λ q, l {#q} v)%I q.
156
  Proof. rewrite mapsto_unseal. apply _. Qed.
157
  Global Instance mapsto_persistent l v : Persistent (l ↦□ v).
158
  Proof. rewrite mapsto_unseal. apply _. Qed.
159

160
  Lemma mapsto_valid l dq v : l {dq} v - ⌜✓ dq%Qp.
161
  Proof. rewrite mapsto_unseal. apply ghost_map_elem_valid. Qed.
162
  Lemma mapsto_valid_2 l dq1 dq2 v1 v2 : l {dq1} v1 - l {dq2} v2 - ⌜✓ (dq1  dq2)  v1 = v2.
163
  Proof. rewrite mapsto_unseal. apply ghost_map_elem_valid_2. Qed.
164
  (** Almost all the time, this is all you really need. *)
165
  Lemma mapsto_agree l dq1 dq2 v1 v2 : l {dq1} v1 - l {dq2} v2 - v1 = v2.
166
  Proof. rewrite mapsto_unseal. apply ghost_map_elem_agree. Qed.
167

168
169
  Lemma mapsto_combine l dq1 dq2 v1 v2 :
    l {dq1} v1 - l {dq2} v2 - l {dq1  dq2} v1  v1 = v2.
170
  Proof. rewrite mapsto_unseal. apply ghost_map_elem_combine. Qed.
171

172
173
  Lemma mapsto_frac_ne l1 l2 dq1 dq2 v1 v2 :
    ¬ (dq1  dq2)  l1 {dq1} v1 - l2 {dq2} v2 - l1  l2.
174
  Proof. rewrite mapsto_unseal. apply ghost_map_elem_frac_ne. Qed.
175
  Lemma mapsto_ne l1 l2 dq2 v1 v2 : l1  v1 - l2 {dq2} v2 - l1  l2.
176
  Proof. rewrite mapsto_unseal. apply ghost_map_elem_ne. Qed.
177

178
  (** Permanently turn any points-to predicate into a persistent
179
      points-to predicate. *)
180
  Lemma mapsto_persist l dq v : l {dq} v == l ↦□ v.
181
  Proof. rewrite mapsto_unseal. apply ghost_map_elem_persist. Qed.
Abel Nieto's avatar
Abel Nieto committed
182

183
184
185
186
187
188
  (** Framing support *)
  Global Instance frame_mapsto p l v q1 q2 RES :
    FrameFractionalHyps p (l {#q1} v) (λ q, l {#q} v)%I RES q1 q2 
    Frame p (l {#q1} v) (l {#q2} v) RES | 5.
  Proof. apply: frame_fractional. Qed.

189
  (** General properties of [meta] and [meta_token] *)
190
  Global Instance meta_token_timeless l N : Timeless (meta_token l N).
191
  Proof. rewrite meta_token_unseal. apply _. Qed.
192
  Global Instance meta_timeless `{Countable A} l N (x : A) : Timeless (meta l N x).
193
  Proof. rewrite meta_unseal. apply _. Qed.
194
  Global Instance meta_persistent `{Countable A} l N (x : A) : Persistent (meta l N x).
195
  Proof. rewrite meta_unseal. apply _. Qed.
196

197
198
199
  Lemma meta_token_union_1 l E1 E2 :
    E1 ## E2  meta_token l (E1  E2) - meta_token l E1  meta_token l E2.
  Proof.
200
    rewrite meta_token_unseal /meta_token_def. intros ?. iDestruct 1 as (γm1) "[#Hγm Hm]".
201
    rewrite reservation_map_token_union //. iDestruct "Hm" as "[Hm1 Hm2]".
202
203
204
205
206
    iSplitL "Hm1"; eauto.
  Qed.
  Lemma meta_token_union_2 l E1 E2 :
    meta_token l E1 - meta_token l E2 - meta_token l (E1  E2).
  Proof.
207
    rewrite meta_token_unseal /meta_token_def.
208
    iIntros "(%γm1 & #Hγm1 & Hm1) (%γm2 & #Hγm2 & Hm2)".
Ralf Jung's avatar
Ralf Jung committed
209
    iDestruct (ghost_map_elem_valid_2 with "Hγm1 Hγm2") as %[_ ->].
210
211
    iDestruct (own_valid_2 with "Hm1 Hm2") as %?%reservation_map_token_valid_op.
    iExists γm2. iFrame "Hγm2". rewrite reservation_map_token_union //. by iSplitL "Hm1".
212
213
214
215
216
217
218
219
  Qed.
  Lemma meta_token_union l E1 E2 :
    E1 ## E2  meta_token l (E1  E2)  meta_token l E1  meta_token l E2.
  Proof.
    intros; iSplit; first by iApply meta_token_union_1.
    iIntros "[Hm1 Hm2]". by iApply (meta_token_union_2 with "Hm1 Hm2").
  Qed.

220
221
222
223
224
225
226
  Lemma meta_token_difference l E1 E2 :
    E1  E2  meta_token l E2  meta_token l E1  meta_token l (E2  E1).
  Proof.
    intros. rewrite {1}(union_difference_L E1 E2) //.
    by rewrite meta_token_union; last set_solver.
  Qed.

227
228
  Lemma meta_agree `{Countable A} l i (x1 x2 : A) :
    meta l i x1 - meta l i x2 - x1 = x2.
229
  Proof.
230
    rewrite meta_unseal /meta_def.
231
    iIntros "(%γm1 & Hγm1 & Hm1) (%γm2 & Hγm2 & Hm2)".
Ralf Jung's avatar
Ralf Jung committed
232
    iDestruct (ghost_map_elem_valid_2 with "Hγm1 Hγm2") as %[_ ->].
233
    iDestruct (own_valid_2 with "Hm1 Hm2") as %Hγ; iPureIntro.
234
    move: Hγ. rewrite -reservation_map_data_op reservation_map_data_valid.
Ralf Jung's avatar
Ralf Jung committed
235
    move=> /to_agree_op_inv_L. naive_solver.
236
  Qed.
237
238
  Lemma meta_set `{Countable A} E l (x : A) N :
     N  E  meta_token l E == meta l N x.
239
  Proof.
240
    rewrite meta_token_unseal meta_unseal /meta_token_def /meta_def.
241
    iDestruct 1 as (γm) "[Hγm Hm]". iExists γm. iFrame "Hγm".
242
    iApply (own_update with "Hm").
243
    apply reservation_map_alloc; last done.
244
    cut (positives_flatten N @{coPset} N); first by set_solver.
245
246
    (* TODO: Avoid unsealing here. *)
    rewrite namespaces.nclose_unseal. apply elem_coPset_suffixes.
247
    exists 1%positive. by rewrite left_id_L.
248
249
250
  Qed.

  (** Update lemmas *)
251
  Lemma gen_heap_alloc σ l v :
252
    σ !! l = None 
253
    gen_heap_interp σ == gen_heap_interp (<[l:=v]>σ)  l  v  meta_token l .
254
  Proof.
255
    iIntros (Hσl). rewrite /gen_heap_interp mapsto_unseal /mapsto_def meta_token_unseal /meta_token_def /=.
256
    iDestruct 1 as (m Hσm) "[Hσ Hm]".
Ralf Jung's avatar
Ralf Jung committed
257
    iMod (ghost_map_insert l with "Hσ") as "[Hσ Hl]"; first done.
258
259
    iMod (own_alloc (reservation_map_token )) as (γm) "Hγm".
    { apply reservation_map_token_valid. }
Ralf Jung's avatar
Ralf Jung committed
260
    iMod (ghost_map_insert_persist l with "Hm") as "[Hm Hlm]".
261
    { move: Hσl. rewrite -!not_elem_of_dom. set_solver. }
262
    iModIntro. iFrame "Hl". iSplitL "Hσ Hm"; last by eauto with iFrame.
263
264
    iExists (<[l:=γm]> m). iFrame. iPureIntro.
    rewrite !dom_insert_L. set_solver.
265
266
  Qed.

267
  Lemma gen_heap_alloc_big σ σ' :
268
    σ' ## σ 
269
270
    gen_heap_interp σ ==
    gen_heap_interp (σ'  σ)  ([ map] l  v  σ', l  v)  ([ map] l  _  σ', meta_token l ).
Robbert Krebbers's avatar
Robbert Krebbers committed
271
  Proof.
272
273
274
275
276
277
278
    revert σ; induction σ' as [| l v σ' Hl IH] using map_ind; iIntros (σ Hdisj) "Hσ".
    { rewrite left_id_L. auto. }
    iMod (IH with "Hσ") as "[Hσ'σ Hσ']"; first by eapply map_disjoint_insert_l.
    decompose_map_disjoint.
    rewrite !big_opM_insert // -insert_union_l //.
    by iMod (gen_heap_alloc with "Hσ'σ") as "($ & $ & $)";
      first by apply lookup_union_None.
Robbert Krebbers's avatar
Robbert Krebbers committed
279
280
  Qed.

281
  Lemma gen_heap_valid σ l dq v : gen_heap_interp σ - l {dq} v - ⌜σ !! l = Some v.
282
  Proof.
283
    iDestruct 1 as (m Hσm) "[Hσ _]". iIntros "Hl".
284
    rewrite /gen_heap_interp mapsto_unseal.
Ralf Jung's avatar
Ralf Jung committed
285
    by iDestruct (ghost_map_lookup with "Hσ Hl") as %?.
286
287
288
  Qed.

  Lemma gen_heap_update σ l v1 v2 :
289
    gen_heap_interp σ - l  v1 == gen_heap_interp (<[l:=v2]>σ)  l  v2.
290
  Proof.
291
    iDestruct 1 as (m Hσm) "[Hσ Hm]".
292
    iIntros "Hl". rewrite /gen_heap_interp mapsto_unseal /mapsto_def.
Ralf Jung's avatar
Ralf Jung committed
293
294
    iDestruct (ghost_map_lookup with "Hσ Hl") as %Hl.
    iMod (ghost_map_update with "Hσ Hl") as "[Hσ Hl]".
295
    iModIntro. iFrame "Hl". iExists m. iFrame.
296
    iPureIntro. apply elem_of_dom_2 in Hl.
297
    rewrite dom_insert_L. set_solver.
298
299
  Qed.
End gen_heap.
300

301
302
(** This variant of [gen_heap_init] should only be used when absolutely needed.
The key difference to [gen_heap_init] is that the [inG] instances in the new
303
[gen_heapGS] instance are related to the original [gen_heapGpreS] instance,
304
whereas [gen_heap_init] forgets about that relation. *)
305
Lemma gen_heap_init_names `{Countable L, !gen_heapGpreS L V Σ} σ :
306
   |==>  γh γm : gname,
307
    let hG := GenHeapGS L V Σ γh γm in
Ralf Jung's avatar
Ralf Jung committed
308
    gen_heap_interp σ  ([ map] l  v  σ, l  v)  ([ map] l  _  σ, meta_token l ).
309
Proof.
Ralf Jung's avatar
Ralf Jung committed
310
311
  iMod (ghost_map_alloc_empty (K:=L) (V:=V)) as (γh) "Hh".
  iMod (ghost_map_alloc_empty (K:=L) (V:=gname)) as (γm) "Hm".
312
  iExists γh, γm.
313
  iAssert (gen_heap_interp (hG:=GenHeapGS _ _ _ γh γm) ) with "[Hh Hm]" as "Hinterp".
Ralf Jung's avatar
Ralf Jung committed
314
  { iExists ; simpl. iFrame "Hh Hm". by rewrite dom_empty_L. }
315
316
  iMod (gen_heap_alloc_big with "Hinterp") as "(Hinterp & $ & $)".
  { apply map_disjoint_empty_r. }
Ralf Jung's avatar
Ralf Jung committed
317
  rewrite right_id_L. done.
318
Qed.
319

320
321
Lemma gen_heap_init `{Countable L, !gen_heapGpreS L V Σ} σ :
   |==>  _ : gen_heapGS L V Σ,
322
323
324
    gen_heap_interp σ  ([ map] l  v  σ, l  v)  ([ map] l  _  σ, meta_token l ).
Proof.
  iMod (gen_heap_init_names σ) as (γh γm) "Hinit".
325
  iExists (GenHeapGS _ _ _ γh γm).
326
327
  done.
Qed.