gen_heap.v 16 KB
Newer Older
1
From stdpp Require Export namespaces.
2
From iris.bi.lib Require Import fractional.
3
From iris.proofmode Require Import tactics.
4 5
From iris.algebra Require Import auth gmap frac agree namespace_map.
From iris.base_logic.lib Require Export own.
6
Set Default Proof Using "Type".
7 8
Import uPred.

Robbert Krebbers's avatar
Robbert Krebbers committed
9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
(** This file provides a generic mechanism for a point-to connective [l ↦{q} v]
with fractional permissions (where [l : L] and [v : V] over some abstract type
[L] for locations and [V] for values). This mechanism can be plugged into a
language by using the heap invariant [gen_heap_ctx σ] where [σ : gmap L V]. See
heap-lang for an example.

Next to the point-to connective [l ↦{q} v], which keeps track of the value [v]
of a location [l], this mechanism allows one to attach "meta" or "ghost" data to
locations. This is done as follows:

- When one allocates a location, in addition to the point-to connective [l ↦ v],
  one also obtains the token [meta_token ⊤ l]. This token is an exclusive
  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:

- An authoritative RA over [gmap L (fracR * agreeR V)], which keeps track of the
  values of locations.
- An authoritative RA over [gmap L (agree gname)], which keeps track of the meta
  information of locations. This RA introduces an indirection, it keeps track of
  a ghost name for each location.
- The ghost names in the aforementioned authoritative RA refer to namespace maps
  [namespace_map (agree positive)], which store the actual meta information.
  This indirection is needed because we cannot perform frame preserving updates
  in an authoritative fragment without owning the full authoritative element
  (in other words, without the indirection [meta_set] would need [gen_heap_ctx]
  as a premise).

Note that in principle we could have used one big authoritative RA to keep track
of both values and ghost names for meta information, for example:
[gmap L (option (fracR * agreeR V) ∗ option (agree gname)]. Due to the [option]s,
this RA would be quite inconvenient to deal with. *)

Ralf Jung's avatar
Ralf Jung committed
60
Definition gen_heapUR (L V : Type) `{Countable L} : ucmraT :=
61
  gmapUR L (prodR fracR (agreeR (leibnizO V))).
62
Definition gen_metaUR (L : Type) `{Countable L} : ucmraT :=
63
  gmapUR L (agreeR gnameO).
64

Ralf Jung's avatar
Ralf Jung committed
65
Definition to_gen_heap {L V} `{Countable L} : gmap L V  gen_heapUR L V :=
66
  fmap (λ v, (1%Qp, to_agree (v : leibnizO V))).
67 68
Definition to_gen_meta `{Countable L} : gmap L gname  gen_metaUR L :=
  fmap to_agree.
69 70

(** The CMRA we need. *)
Ralf Jung's avatar
Ralf Jung committed
71
Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapG {
72
  gen_heap_inG :> inG Σ (authR (gen_heapUR L V));
73
  gen_meta_inG :> inG Σ (authR (gen_metaUR L));
74
  gen_meta_data_inG :> inG Σ (namespace_mapR (agreeR positiveO));
75 76
  gen_heap_name : gname;
  gen_meta_name : gname
77
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
78
Arguments gen_heap_name {_ _ _ _ _} _ : assert.
79
Arguments gen_meta_name {_ _ _ _ _} _ : assert.
80

81 82 83
Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
  gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V));
  gen_meta_preG_inG :> inG Σ (authR (gen_metaUR L));
84
  gen_meta_data_preG_inG :> inG Σ (namespace_mapR (agreeR positiveO));
85
}.
86

87 88 89
Definition gen_heapΣ (L V : Type) `{Countable L} : gFunctors := #[
  GFunctor (authR (gen_heapUR L V));
  GFunctor (authR (gen_metaUR L));
90
  GFunctor (namespace_mapR (agreeR positiveO))
91
].
92

Ralf Jung's avatar
Ralf Jung committed
93
Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
94
  subG (gen_heapΣ L V) Σ  gen_heapPreG L V Σ.
95
Proof. solve_inG. Qed.
96 97

Section definitions.
98
  Context `{Countable L, hG : !gen_heapG L V Σ}.
99

100
  Definition gen_heap_ctx (σ : gmap L V) : iProp Σ := ( m,
Robbert Krebbers's avatar
Robbert Krebbers committed
101 102
    (* The [⊆] is used to avoid assigning ghost information to the locations in
    the initial heap (see [gen_heap_init]). *)
103 104 105
     dom _ m  dom (gset L) σ  
    own (gen_heap_name hG) ( (to_gen_heap σ)) 
    own (gen_meta_name hG) ( (to_gen_meta m)))%I.
106 107

  Definition mapsto_def (l : L) (q : Qp) (v: V) : iProp Σ :=
108
    own (gen_heap_name hG) ( {[ l := (q, to_agree (v : leibnizO V)) ]}).
109
  Definition mapsto_aux : seal (@mapsto_def). by eexists. Qed.
110 111
  Definition mapsto := mapsto_aux.(unseal).
  Definition mapsto_eq : @mapsto = @mapsto_def := mapsto_aux.(seal_eq).
112

113
  Definition meta_token_def (l : L) (E : coPset) : iProp Σ :=
114
    ( γm, own (gen_meta_name hG) ( {[ l := to_agree γm ]}) 
115
           own γm (namespace_map_token E))%I.
116 117 118 119
  Definition meta_token_aux : seal (@meta_token_def). by eexists. Qed.
  Definition meta_token := meta_token_aux.(unseal).
  Definition meta_token_eq : @meta_token = @meta_token_def := meta_token_aux.(seal_eq).

120
  Definition meta_def `{Countable A} (l : L) (N : namespace) (x : A) : iProp Σ :=
121
    ( γm, own (gen_meta_name hG) ( {[ l := to_agree γm ]}) 
122
           own γm (namespace_map_data N (to_agree (encode x))))%I.
123 124 125
  Definition meta_aux : seal (@meta_def). by eexists. Qed.
  Definition meta {A dA cA} := meta_aux.(unseal) A dA cA.
  Definition meta_eq : @meta = @meta_def := meta_aux.(seal_eq).
126 127 128
End definitions.

Local Notation "l ↦{ q } v" := (mapsto l q v)
Robbert Krebbers's avatar
Robbert Krebbers committed
129 130
  (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
Local Notation "l ↦ v" := (mapsto l 1 v) (at level 20) : bi_scope.
131 132

Local Notation "l ↦{ q } -" := ( v, l {q} v)%I
Robbert Krebbers's avatar
Robbert Krebbers committed
133 134
  (at level 20, q at level 50, format "l  ↦{ q }  -") : bi_scope.
Local Notation "l ↦ -" := (l {1} -)%I (at level 20) : bi_scope.
135

136 137
Section to_gen_heap.
  Context (L V : Type) `{Countable L}.
138
  Implicit Types σ : gmap L V.
139
  Implicit Types m : gmap L gname.
140 141 142 143 144 145 146

  (** Conversion to heaps and back *)
  Lemma to_gen_heap_valid σ :  to_gen_heap σ.
  Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
  Lemma lookup_to_gen_heap_None σ l : σ !! l = None  to_gen_heap σ !! l = None.
  Proof. by rewrite /to_gen_heap lookup_fmap=> ->. Qed.
  Lemma gen_heap_singleton_included σ l q v :
Ralf Jung's avatar
Ralf Jung committed
147
    {[l := (q, to_agree v)]}  to_gen_heap σ  σ !! l = Some v.
148
  Proof.
Ralf Jung's avatar
Ralf Jung committed
149 150 151
    rewrite singleton_included=> -[[q' av] []].
    rewrite /to_gen_heap lookup_fmap fmap_Some_equiv => -[v' [Hl [/= -> ->]]].
    move=> /Some_pair_included_total_2 [_] /to_agree_included /leibniz_equiv_iff -> //.
152 153
  Qed.
  Lemma to_gen_heap_insert l v σ :
154
    to_gen_heap (<[l:=v]> σ) = <[l:=(1%Qp, to_agree (v:leibnizO V))]> (to_gen_heap σ).
155
  Proof. by rewrite /to_gen_heap fmap_insert. Qed.
156 157 158 159 160 161 162 163

  Lemma to_gen_meta_valid m :  to_gen_meta m.
  Proof. intros l. rewrite lookup_fmap. by case (m !! l). Qed.
  Lemma lookup_to_gen_meta_None m l : m !! l = None  to_gen_meta m !! l = None.
  Proof. by rewrite /to_gen_meta lookup_fmap=> ->. Qed.
  Lemma to_gen_meta_insert l m γm :
    to_gen_meta (<[l:=γm]> m) = <[l:=to_agree γm]> (to_gen_meta m).
  Proof. by rewrite /to_gen_meta fmap_insert. Qed.
164 165
End to_gen_heap.

166
Lemma gen_heap_init `{Countable L, !gen_heapPreG L V Σ} σ :
167 168
  (|==>  _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
Proof.
169
  iMod (own_alloc ( to_gen_heap σ)) as (γh) "Hh".
170
  { rewrite auth_auth_valid. exact: to_gen_heap_valid. }
171 172 173 174
  iMod (own_alloc ( to_gen_meta )) as (γm) "Hm".
  { rewrite auth_auth_valid. exact: to_gen_meta_valid. }
  iModIntro. iExists (GenHeapG L V Σ _ _ _ _ _ γh γm).
  iExists ; simpl. iFrame "Hh Hm". by rewrite dom_empty_L.
175 176
Qed.

177
Section gen_heap.
178
  Context {L V} `{Countable L, !gen_heapG L V Σ}.
179 180 181
  Implicit Types P Q : iProp Σ.
  Implicit Types Φ : V  iProp Σ.
  Implicit Types σ : gmap L V.
182
  Implicit Types m : gmap L gname.
183
  Implicit Types h g : gen_heapUR L V.
Robbert Krebbers's avatar
Robbert Krebbers committed
184 185
  Implicit Types l : L.
  Implicit Types v : V.
186 187

  (** General properties of mapsto *)
188
  Global Instance mapsto_timeless l q v : Timeless (l {q} v).
189 190 191
  Proof. rewrite mapsto_eq /mapsto_def. apply _. Qed.
  Global Instance mapsto_fractional l v : Fractional (λ q, l {q} v)%I.
  Proof.
192
    intros p q. by rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op
193
      op_singleton -pair_op agree_idemp.
194 195 196
  Qed.
  Global Instance mapsto_as_fractional l q v :
    AsFractional (l {q} v) (λ q, l {q} v)%I q.
197
  Proof. split. done. apply _. Qed.
198

199
  Lemma mapsto_agree l q1 q2 v1 v2 : l {q1} v1 - l {q2} v2 - v1 = v2.
200
  Proof.
201
    apply wand_intro_r.
202
    rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op own_valid discrete_valid.
203
    f_equiv. rewrite auth_frag_valid op_singleton singleton_valid -pair_op.
204
    by intros [_ ?%agree_op_invL'].
205 206
  Qed.

207 208 209 210 211 212 213
  Lemma mapsto_combine l q1 q2 v1 v2 :
    l {q1} v1 - l {q2} v2 - l {q1 + q2} v1  v1 = v2.
  Proof.
    iIntros "Hl1 Hl2". iDestruct (mapsto_agree with "Hl1 Hl2") as %->.
    iCombine "Hl1 Hl2" as "Hl". eauto with iFrame.
  Qed.

214
  Global Instance ex_mapsto_fractional l : Fractional (λ q, l {q} -)%I.
215 216 217 218
  Proof.
    intros p q. iSplit.
    - iDestruct 1 as (v) "[H1 H2]". iSplitL "H1"; eauto.
    - iIntros "[H1 H2]". iDestruct "H1" as (v1) "H1". iDestruct "H2" as (v2) "H2".
219
      iDestruct (mapsto_agree with "H1 H2") as %->. iExists v2. by iFrame.
220
  Qed.
221
  Global Instance ex_mapsto_as_fractional l q :
222
    AsFractional (l {q} -) (λ q, l {q} -)%I q.
223
  Proof. split. done. apply _. Qed.
224

225
  Lemma mapsto_valid l q v : l {q} v -  q.
226
  Proof.
227 228
    rewrite mapsto_eq /mapsto_def own_valid !discrete_valid -auth_frag_valid.
    by apply pure_mono=> /singleton_valid [??].
229
  Qed.
230
  Lemma mapsto_valid_2 l q1 q2 v1 v2 : l {q1} v1 - l {q2} v2 -  (q1 + q2)%Qp.
231
  Proof.
232
    iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %->.
233 234 235
    iApply (mapsto_valid l _ v2). by iFrame.
  Qed.

236
  (** General properties of [meta] and [meta_token] *)
237
  Global Instance meta_token_timeless l N : Timeless (meta_token l N).
238
  Proof. rewrite meta_token_eq /meta_token_def. apply _. Qed.
239
  Global Instance meta_timeless `{Countable A} l N (x : A) : Timeless (meta l N x).
240
  Proof. rewrite meta_eq /meta_def. apply _. Qed.
241
  Global Instance meta_persistent `{Countable A} l N (x : A) : Persistent (meta l N x).
242 243
  Proof. rewrite meta_eq /meta_def. apply _. Qed.

244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269
  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]".
    rewrite namespace_map_token_union //. iDestruct "Hm" as "[Hm1 Hm2]".
    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.
    iDestruct 1 as (γm1) "[#Hγm1 Hm1]". iDestruct 1 as (γm2) "[#Hγm2 Hm2]".
    iAssert  γm1 = γm2 %I as %->.
    { iDestruct (own_valid_2 with "Hγm1 Hγm2") as %Hγ; iPureIntro.
      move: Hγ. rewrite -auth_frag_op op_singleton=> /auth_frag_valid /=.
      rewrite singleton_valid. apply: agree_op_invL'. }
    iDestruct (own_valid_2 with "Hm1 Hm2") as %?%namespace_map_token_valid_op.
    iExists γm2. iFrame "Hγm2". rewrite namespace_map_token_union //. by iSplitL "Hm1".
  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.

270 271 272 273 274 275 276
  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.

277 278
  Lemma meta_agree `{Countable A} l i (x1 x2 : A) :
    meta l i x1 - meta l i x2 - x1 = x2.
279 280 281 282 283 284 285 286
  Proof.
    rewrite meta_eq /meta_def.
    iDestruct 1 as (γm1) "[Hγm1 Hm1]"; iDestruct 1 as (γm2) "[Hγm2 Hm2]".
    iAssert  γm1 = γm2 %I as %->.
    { iDestruct (own_valid_2 with "Hγm1 Hγm2") as %Hγ; iPureIntro.
      move: Hγ. rewrite -auth_frag_op op_singleton=> /auth_frag_valid /=.
      rewrite singleton_valid. apply: agree_op_invL'. }
    iDestruct (own_valid_2 with "Hm1 Hm2") as %Hγ; iPureIntro.
287 288
    move: Hγ. rewrite -namespace_map_data_op namespace_map_data_valid.
    move=> /agree_op_invL'. naive_solver.
289
  Qed.
290 291
  Lemma meta_set `{Countable A} E l (x : A) N :
     N  E  meta_token l E == meta l N x.
292 293 294
  Proof.
    rewrite meta_token_eq meta_eq /meta_token_def /meta_def.
    iDestruct 1 as (γm) "[Hγm Hm]". iExists γm. iFrame "Hγm".
295
    iApply (own_update with "Hm"). by apply namespace_map_alloc_update.
296 297 298
  Qed.

  (** Update lemmas *)
299
  Lemma gen_heap_alloc σ l v :
300
    σ !! l = None 
301
    gen_heap_ctx σ == gen_heap_ctx (<[l:=v]>σ)  l  v  meta_token l .
302
  Proof.
303 304
    iIntros (Hσl). rewrite /gen_heap_ctx mapsto_eq /mapsto_def meta_token_eq /meta_token_def /=.
    iDestruct 1 as (m Hσm) "[Hσ Hm]".
305 306
    iMod (own_update with "Hσ") as "[Hσ Hl]".
    { eapply auth_update_alloc,
307
        (alloc_singleton_local_update _ _ (1%Qp, to_agree (v:leibnizO _)))=> //.
308
      by apply lookup_to_gen_heap_None. }
309 310
    iMod (own_alloc (namespace_map_token )) as (γm) "Hγm".
    { apply namespace_map_token_valid. }
311 312 313 314 315 316 317 318 319
    iMod (own_update with "Hm") as "[Hm Hlm]".
    { eapply auth_update_alloc.
      eapply (alloc_singleton_local_update _ l (to_agree γm))=> //.
      apply lookup_to_gen_meta_None.
      move: Hσl. rewrite -!(not_elem_of_dom (D:=gset L)). set_solver. }
    iModIntro. iFrame "Hl". iSplitL "Hσ Hm"; last by eauto with iFrame.
    iExists (<[l:=γm]> m).
    rewrite to_gen_heap_insert to_gen_meta_insert !dom_insert_L. iFrame.
    iPureIntro. set_solver.
320 321
  Qed.

Amin Timany's avatar
Amin Timany committed
322
  Lemma gen_heap_alloc_gen σ σ' :
323 324
    σ' ## σ 
    gen_heap_ctx σ ==
325
    gen_heap_ctx (σ'  σ)  ([ map] l  v  σ', l  v)  ([ map] l  _  σ', meta_token l ).
326
  Proof.
327 328 329 330 331 332 333
    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.
334 335
  Qed.

336 337
  Lemma gen_heap_valid σ l q v : gen_heap_ctx σ - l {q} v - ⌜σ !! l = Some v.
  Proof.
338 339
    iDestruct 1 as (m Hσm) "[Hσ _]". iIntros "Hl".
    rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
340
    iDestruct (own_valid_2 with "Hσ Hl")
341
      as %[Hl%gen_heap_singleton_included _]%auth_both_valid; auto.
342 343 344 345 346
  Qed.

  Lemma gen_heap_update σ l v1 v2 :
    gen_heap_ctx σ - l  v1 == gen_heap_ctx (<[l:=v2]>σ)  l  v2.
  Proof.
347 348
    iDestruct 1 as (m Hσm) "[Hσ Hm]".
    iIntros "Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
349
    iDestruct (own_valid_2 with "Hσ Hl")
350
      as %[Hl%gen_heap_singleton_included _]%auth_both_valid.
351 352
    iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
    { eapply auth_update, singleton_local_update,
353
        (exclusive_local_update _ (1%Qp, to_agree (v2:leibnizO _)))=> //.
354
      by rewrite /to_gen_heap lookup_fmap Hl. }
355 356 357
    iModIntro. iFrame "Hl". iExists m. rewrite to_gen_heap_insert. iFrame.
    iPureIntro. apply (elem_of_dom_2 (D:=gset L)) in Hl.
    rewrite dom_insert_L. set_solver.
358 359
  Qed.
End gen_heap.