gen_heap.v 15.1 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]). *)
Ralf Jung's avatar
Ralf Jung committed
101
102
103
     dom _ m  dom (gset L) σ  
    ghost_map_auth (gen_heap_name hG) 1 σ 
    ghost_map_auth (gen_meta_name hG) 1 m.
104

105
  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
  Definition mapsto_aux : seal (@mapsto_def). Proof. by eexists. Qed.
108
109
  Definition mapsto := mapsto_aux.(unseal).
  Definition mapsto_eq : @mapsto = @mapsto_def := mapsto_aux.(seal_eq).
110

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
128
129
(** FIXME: Refactor these notations using custom entries once Coq bug #13654
has been fixed. *)
130
131
132
133
134
135
136
137
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.
138

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

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

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

167
168
  Lemma mapsto_combine l dq1 dq2 v1 v2 :
    l {dq1} v1 - l {dq2} v2 - l {dq1  dq2} v1  v1 = v2.
Ralf Jung's avatar
Ralf Jung committed
169
  Proof. rewrite mapsto_eq. apply ghost_map_elem_combine. Qed.
170

171
172
  Lemma mapsto_frac_ne l1 l2 dq1 dq2 v1 v2 :
    ¬ (dq1  dq2)  l1 {dq1} v1 - l2 {dq2} v2 - l1  l2.
Ralf Jung's avatar
Ralf Jung committed
173
  Proof. rewrite mapsto_eq. apply ghost_map_elem_frac_ne. Qed.
174
  Lemma mapsto_ne l1 l2 dq2 v1 v2 : l1  v1 - l2 {dq2} v2 - l1  l2.
Ralf Jung's avatar
Ralf Jung committed
175
  Proof. rewrite mapsto_eq. apply ghost_map_elem_ne. Qed.
176

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

182
183
184
185
186
187
  (** 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.

188
  (** General properties of [meta] and [meta_token] *)
189
  Global Instance meta_token_timeless l N : Timeless (meta_token l N).
Ralf Jung's avatar
Ralf Jung committed
190
  Proof. rewrite meta_token_eq. apply _. Qed.
191
  Global Instance meta_timeless `{Countable A} l N (x : A) : Timeless (meta l N x).
Ralf Jung's avatar
Ralf Jung committed
192
  Proof. rewrite meta_eq. apply _. Qed.
193
  Global Instance meta_persistent `{Countable A} l N (x : A) : Persistent (meta l N x).
Ralf Jung's avatar
Ralf Jung committed
194
  Proof. rewrite meta_eq. apply _. Qed.
195

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.
    rewrite meta_token_eq /meta_token_def. intros ?. iDestruct 1 as (γm1) "[#Hγm Hm]".
200
    rewrite reservation_map_token_union //. iDestruct "Hm" as "[Hm1 Hm2]".
201
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.
    rewrite meta_token_eq /meta_token_def.
207
    iIntros "(%γm1 & #Hγm1 & Hm1) (%γm2 & #Hγm2 & Hm2)".
Ralf Jung's avatar
Ralf Jung committed
208
    iDestruct (ghost_map_elem_valid_2 with "Hγm1 Hγm2") as %[_ ->].
209
210
    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".
211
212
213
214
215
216
217
218
  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.

219
220
221
222
223
224
225
  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.

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

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

265
  Lemma gen_heap_alloc_big σ σ' :
266
    σ' ## σ 
267
268
    gen_heap_interp σ ==
    gen_heap_interp (σ'  σ)  ([ map] l  v  σ', l  v)  ([ map] l  _  σ', meta_token l ).
Robbert Krebbers's avatar
Robbert Krebbers committed
269
  Proof.
270
271
272
273
274
275
276
    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
277
278
  Qed.

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

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

299
300
(** 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
301
[gen_heapGS] instance are related to the original [gen_heapGpreS] instance,
302
whereas [gen_heap_init] forgets about that relation. *)
303
Lemma gen_heap_init_names `{Countable L, !gen_heapGpreS L V Σ} σ :
304
   |==>  γh γm : gname,
305
    let hG := GenHeapGS L V Σ γh γm in
Ralf Jung's avatar
Ralf Jung committed
306
    gen_heap_interp σ  ([ map] l  v  σ, l  v)  ([ map] l  _  σ, meta_token l ).
307
Proof.
Ralf Jung's avatar
Ralf Jung committed
308
309
  iMod (ghost_map_alloc_empty (K:=L) (V:=V)) as (γh) "Hh".
  iMod (ghost_map_alloc_empty (K:=L) (V:=gname)) as (γm) "Hm".
310
  iExists γh, γm.
311
  iAssert (gen_heap_interp (hG:=GenHeapGS _ _ _ γh γm) ) with "[Hh Hm]" as "Hinterp".
Ralf Jung's avatar
Ralf Jung committed
312
  { iExists ; simpl. iFrame "Hh Hm". by rewrite dom_empty_L. }
313
314
  iMod (gen_heap_alloc_big with "Hinterp") as "(Hinterp & $ & $)".
  { apply map_disjoint_empty_r. }
Ralf Jung's avatar
Ralf Jung committed
315
  rewrite right_id_L. done.
316
Qed.
317

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