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

Ralf Jung's avatar
Ralf Jung committed
8 9
Definition gen_heapUR (L V : Type) `{Countable L} : ucmraT :=
  gmapUR L (prodR fracR (agreeR (leibnizC V))).
10 11 12
Definition gen_metaUR (L : Type) `{Countable L} : ucmraT :=
  gmapUR L (agreeR gnameC).

Ralf Jung's avatar
Ralf Jung committed
13 14
Definition to_gen_heap {L V} `{Countable L} : gmap L V  gen_heapUR L V :=
  fmap (λ v, (1%Qp, to_agree (v : leibnizC V))).
15 16
Definition to_gen_meta `{Countable L} : gmap L gname  gen_metaUR L :=
  fmap to_agree.
17 18

(** The CMRA we need. *)
Ralf Jung's avatar
Ralf Jung committed
19
Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapG {
20
  gen_heap_inG :> inG Σ (authR (gen_heapUR L V));
21 22 23 24
  gen_meta_inG :> inG Σ (authR (gen_metaUR L));
  gen_meta_data_inG :> inG Σ (csumR (exclR unitC) (agreeR positiveC));
  gen_heap_name : gname;
  gen_meta_name : gname
25
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
26
Arguments gen_heap_name {_ _ _ _ _} _ : assert.
27
Arguments gen_meta_name {_ _ _ _ _} _ : assert.
28

29 30 31 32 33
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));
  gen_meta_data_preG_inG :> inG Σ (csumR (exclR unitC) (agreeR positiveC));
}.
34

35 36 37 38 39
Definition gen_heapΣ (L V : Type) `{Countable L} : gFunctors := #[
  GFunctor (authR (gen_heapUR L V));
  GFunctor (authR (gen_metaUR L));
  GFunctor (csumR (exclR unitC) (agreeR positiveC))
].
40

Ralf Jung's avatar
Ralf Jung committed
41
Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
42
  subG (gen_heapΣ L V) Σ  gen_heapPreG L V Σ.
43
Proof. solve_inG. Qed.
44 45

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

48 49 50 51
  Definition gen_heap_ctx (σ : gmap L V) : iProp Σ := ( m,
     dom _ m  dom (gset L) σ  
    own (gen_heap_name hG) ( (to_gen_heap σ)) 
    own (gen_meta_name hG) ( (to_gen_meta m)))%I.
52 53

  Definition mapsto_def (l : L) (q : Qp) (v: V) : iProp Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
54
    own (gen_heap_name hG) ( {[ l := (q, to_agree (v : leibnizC V)) ]}).
55
  Definition mapsto_aux : seal (@mapsto_def). by eexists. Qed.
56 57
  Definition mapsto := mapsto_aux.(unseal).
  Definition mapsto_eq : @mapsto = @mapsto_def := mapsto_aux.(seal_eq).
58 59 60 61 62 63 64 65 66 67 68 69 70 71

  Definition meta_token_def (l : L) : iProp Σ :=
    ( γm, own (gen_meta_name hG) ( {[ l := to_agree γm ]}) 
           own γm (Cinl (Excl ())))%I.
  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).

  Definition meta_def `{Countable A} (l : L) (x : A) : iProp Σ :=
    ( γm, own (gen_meta_name hG) ( {[ l := to_agree γm ]}) 
           own γm (Cinr (to_agree (encode x))))%I.
  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).
72 73 74
End definitions.

Local Notation "l ↦{ q } v" := (mapsto l q v)
Robbert Krebbers's avatar
Robbert Krebbers committed
75 76
  (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.
77 78

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

82 83
Section to_gen_heap.
  Context (L V : Type) `{Countable L}.
84
  Implicit Types σ : gmap L V.
85
  Implicit Types m : gmap L gname.
86 87 88 89 90 91 92

  (** 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
93
    {[l := (q, to_agree v)]}  to_gen_heap σ  σ !! l = Some v.
94
  Proof.
Ralf Jung's avatar
Ralf Jung committed
95 96 97
    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 -> //.
98 99
  Qed.
  Lemma to_gen_heap_insert l v σ :
Ralf Jung's avatar
Ralf Jung committed
100
    to_gen_heap (<[l:=v]> σ) = <[l:=(1%Qp, to_agree (v:leibnizC V))]> (to_gen_heap σ).
101
  Proof. by rewrite /to_gen_heap fmap_insert. Qed.
102 103 104 105 106 107 108 109

  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.
110 111
End to_gen_heap.

112
Lemma gen_heap_init `{Countable L, !gen_heapPreG L V Σ} σ :
113 114
  (|==>  _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
Proof.
115
  iMod (own_alloc ( to_gen_heap σ)) as (γh) "Hh".
116
  { rewrite auth_auth_valid. exact: to_gen_heap_valid. }
117 118 119 120
  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.
121 122
Qed.

123
Section gen_heap.
124
  Context {L V} `{Countable L, !gen_heapG L V Σ}.
125 126 127
  Implicit Types P Q : iProp Σ.
  Implicit Types Φ : V  iProp Σ.
  Implicit Types σ : gmap L V.
128
  Implicit Types m : gmap L gname.
129
  Implicit Types h g : gen_heapUR L V.
Robbert Krebbers's avatar
Robbert Krebbers committed
130 131
  Implicit Types l : L.
  Implicit Types v : V.
132 133

  (** General properties of mapsto *)
134
  Global Instance mapsto_timeless l q v : Timeless (l {q} v).
135 136 137
  Proof. rewrite mapsto_eq /mapsto_def. apply _. Qed.
  Global Instance mapsto_fractional l v : Fractional (λ q, l {q} v)%I.
  Proof.
138
    intros p q. by rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op
Ralf Jung's avatar
Ralf Jung committed
139
      op_singleton pair_op agree_idemp.
140 141 142
  Qed.
  Global Instance mapsto_as_fractional l q v :
    AsFractional (l {q} v) (λ q, l {q} v)%I q.
143
  Proof. split. done. apply _. Qed.
144

Robbert Krebbers's avatar
Robbert Krebbers committed
145
  Lemma mapsto_agree l q1 q2 v1 v2 : l {q1} v1 - l {q2} v2 - v1 = v2.
146
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
147
    apply wand_intro_r.
148
    rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op own_valid discrete_valid.
149
    f_equiv. rewrite auth_frag_valid op_singleton singleton_valid pair_op.
150
    by intros [_ ?%agree_op_invL'].
151 152
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
153
  Global Instance ex_mapsto_fractional l : Fractional (λ q, l {q} -)%I.
154 155 156 157
  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".
Robbert Krebbers's avatar
Robbert Krebbers committed
158
      iDestruct (mapsto_agree with "H1 H2") as %->. iExists v2. by iFrame.
159
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
160
  Global Instance ex_mapsto_as_fractional l q :
161
    AsFractional (l {q} -) (λ q, l {q} -)%I q.
162
  Proof. split. done. apply _. Qed.
163

Robbert Krebbers's avatar
Robbert Krebbers committed
164
  Lemma mapsto_valid l q v : l {q} v -  q.
165
  Proof.
166 167
    rewrite mapsto_eq /mapsto_def own_valid !discrete_valid -auth_frag_valid.
    by apply pure_mono=> /singleton_valid [??].
168
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
169
  Lemma mapsto_valid_2 l q1 q2 v1 v2 : l {q1} v1 - l {q2} v2 -  (q1 + q2)%Qp.
170
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
171
    iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %->.
172 173 174
    iApply (mapsto_valid l _ v2). by iFrame.
  Qed.

175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202
  (** General properties of [meta] and [meta_token] *)
  Global Instance meta_token_timeless l : Timeless (meta_token l).
  Proof. rewrite meta_token_eq /meta_token_def. apply _. Qed.
  Global Instance meta_timeless `{Countable A} l (x : A) : Timeless (meta l x).
  Proof. rewrite meta_eq /meta_def. apply _. Qed.
  Global Instance meta_persistent `{Countable A} l (x : A) : Persistent (meta l x).
  Proof. rewrite meta_eq /meta_def. apply _. Qed.

  Lemma meta_agree `{Countable A} l (x1 x2 : A) :
    meta l x1 - meta l x2 - x1 = x2.
  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.
    move: Hγ=> /agree_op_invL'. by intros ?%(inj _).
  Qed.
  Lemma meta_set `{Countable A} l (x : A) : meta_token l == meta l x.
  Proof.
    rewrite meta_token_eq meta_eq /meta_token_def /meta_def.
    iDestruct 1 as (γm) "[Hγm Hm]". iExists γm. iFrame "Hγm".
    iApply (own_update with "Hm"). by apply cmra_update_exclusive.
  Qed.

  (** Update lemmas *)
203
  Lemma gen_heap_alloc σ l v :
204 205
    σ !! l = None 
    gen_heap_ctx σ == gen_heap_ctx (<[l:=v]>σ)  l  v  meta_token l.
206
  Proof.
207 208
    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]".
209 210
    iMod (own_update with "Hσ") as "[Hσ Hl]".
    { eapply auth_update_alloc,
Ralf Jung's avatar
Ralf Jung committed
211
        (alloc_singleton_local_update _ _ (1%Qp, to_agree (v:leibnizC _)))=> //.
212
      by apply lookup_to_gen_heap_None. }
213 214 215 216 217 218 219 220 221 222
    iMod (own_alloc (Cinl (Excl ()))) as (γm) "Hγm"; first done.
    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.
223 224
  Qed.

Amin Timany's avatar
Amin Timany committed
225
  Lemma gen_heap_alloc_gen σ σ' :
226 227 228
    σ' ## σ 
    gen_heap_ctx σ ==
    gen_heap_ctx (σ'  σ)  ([ map] l  v  σ', l  v)  ([ map] l  _  σ', meta_token l).
Robbert Krebbers's avatar
Robbert Krebbers committed
229
  Proof.
230 231 232 233 234 235 236
    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
237 238
  Qed.

239 240
  Lemma gen_heap_valid σ l q v : gen_heap_ctx σ - l {q} v - ⌜σ !! l = Some v.
  Proof.
241 242
    iDestruct 1 as (m Hσm) "[Hσ _]". iIntros "Hl".
    rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
243
    iDestruct (own_valid_2 with "Hσ Hl")
244
      as %[Hl%gen_heap_singleton_included _]%auth_both_valid; auto.
245 246 247 248 249
  Qed.

  Lemma gen_heap_update σ l v1 v2 :
    gen_heap_ctx σ - l  v1 == gen_heap_ctx (<[l:=v2]>σ)  l  v2.
  Proof.
250 251
    iDestruct 1 as (m Hσm) "[Hσ Hm]".
    iIntros "Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
252
    iDestruct (own_valid_2 with "Hσ Hl")
253
      as %[Hl%gen_heap_singleton_included _]%auth_both_valid.
254 255
    iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
    { eapply auth_update, singleton_local_update,
Ralf Jung's avatar
Ralf Jung committed
256
        (exclusive_local_update _ (1%Qp, to_agree (v2:leibnizC _)))=> //.
257
      by rewrite /to_gen_heap lookup_fmap Hl. }
258 259 260
    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.
261 262
  Qed.
End gen_heap.