gen_heap.v 6.76 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From iris.algebra Require Import auth gmap frac agree.
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 10 11
Definition gen_heapUR (L V : Type) `{Countable L} : ucmraT :=
  gmapUR L (prodR fracR (agreeR (leibnizC V))).
Definition to_gen_heap {L V} `{Countable L} : gmap L V  gen_heapUR L V :=
  fmap (λ v, (1%Qp, to_agree (v : leibnizC V))).
12 13

(** The CMRA we need. *)
Ralf Jung's avatar
Ralf Jung committed
14
Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapG {
15 16 17
  gen_heap_inG :> inG Σ (authR (gen_heapUR L V));
  gen_heap_name : gname
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
18
Arguments gen_heap_name {_ _ _ _ _} _ : assert.
19

Ralf Jung's avatar
Ralf Jung committed
20
Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} :=
21 22
  { gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V)) }.

Ralf Jung's avatar
Ralf Jung committed
23
Definition gen_heapΣ (L V : Type) `{Countable L} : gFunctors :=
24
  #[GFunctor (authR (gen_heapUR L V))].
25

Ralf Jung's avatar
Ralf Jung committed
26
Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
27
  subG (gen_heapΣ L V) Σ  gen_heapPreG L V Σ.
28
Proof. solve_inG. Qed.
29 30

Section definitions.
Robbert Krebbers's avatar
Robbert Krebbers committed
31
  Context `{hG : gen_heapG L V Σ}.
32 33

  Definition gen_heap_ctx (σ : gmap L V) : iProp Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
34
    own (gen_heap_name hG) ( (to_gen_heap σ)).
35 36

  Definition mapsto_def (l : L) (q : Qp) (v: V) : iProp Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
37
    own (gen_heap_name hG) ( {[ l := (q, to_agree (v : leibnizC V)) ]}).
38
  Definition mapsto_aux : seal (@mapsto_def). by eexists. Qed.
39 40
  Definition mapsto := mapsto_aux.(unseal).
  Definition mapsto_eq : @mapsto = @mapsto_def := mapsto_aux.(seal_eq).
41 42 43
End definitions.

Local Notation "l ↦{ q } v" := (mapsto l q v)
Robbert Krebbers's avatar
Robbert Krebbers committed
44 45
  (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.
46 47

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

51 52
Section to_gen_heap.
  Context (L V : Type) `{Countable L}.
53 54 55 56 57 58 59 60
  Implicit Types σ : gmap L V.

  (** 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
61
    {[l := (q, to_agree v)]}  to_gen_heap σ  σ !! l = Some v.
62
  Proof.
Ralf Jung's avatar
Ralf Jung committed
63 64 65
    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 -> //.
66 67
  Qed.
  Lemma to_gen_heap_insert l v σ :
Ralf Jung's avatar
Ralf Jung committed
68
    to_gen_heap (<[l:=v]> σ) = <[l:=(1%Qp, to_agree (v:leibnizC V))]> (to_gen_heap σ).
69
  Proof. by rewrite /to_gen_heap fmap_insert. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
70 71 72
  Lemma to_gen_heap_delete l σ :
    to_gen_heap (delete l σ) = delete l (to_gen_heap σ).
  Proof. by rewrite /to_gen_heap fmap_delete. Qed.
73 74
End to_gen_heap.

75 76 77 78 79 80 81 82
Lemma gen_heap_init `{gen_heapPreG L V Σ} σ :
  (|==>  _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
Proof.
  iMod (own_alloc ( to_gen_heap σ)) as (γ) "Hh".
  { apply: auth_auth_valid. exact: to_gen_heap_valid. }
  iModIntro. by iExists (GenHeapG L V Σ _ _ _ γ).
Qed.

83 84 85 86 87 88
Section gen_heap.
  Context `{gen_heapG L V Σ}.
  Implicit Types P Q : iProp Σ.
  Implicit Types Φ : V  iProp Σ.
  Implicit Types σ : gmap L V.
  Implicit Types h g : gen_heapUR L V.
Robbert Krebbers's avatar
Robbert Krebbers committed
89 90
  Implicit Types l : L.
  Implicit Types v : V.
91 92

  (** General properties of mapsto *)
93
  Global Instance mapsto_timeless l q v : Timeless (l {q} v).
94 95 96
  Proof. rewrite mapsto_eq /mapsto_def. apply _. Qed.
  Global Instance mapsto_fractional l v : Fractional (λ q, l {q} v)%I.
  Proof.
97
    intros p q. by rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op
Ralf Jung's avatar
Ralf Jung committed
98
      op_singleton pair_op agree_idemp.
99 100 101
  Qed.
  Global Instance mapsto_as_fractional l q v :
    AsFractional (l {q} v) (λ q, l {q} v)%I q.
102
  Proof. split. done. apply _. Qed.
103

Robbert Krebbers's avatar
Robbert Krebbers committed
104
  Lemma mapsto_agree l q1 q2 v1 v2 : l {q1} v1 - l {q2} v2 - v1 = v2.
105
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
106
    apply wand_intro_r.
107
    rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op own_valid discrete_valid.
108
    f_equiv=> /auth_own_valid /=. rewrite op_singleton singleton_valid pair_op.
109
    by intros [_ ?%agree_op_invL'].
110 111
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
112
  Global Instance ex_mapsto_fractional l : Fractional (λ q, l {q} -)%I.
113 114 115 116
  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
117
      iDestruct (mapsto_agree with "H1 H2") as %->. iExists v2. by iFrame.
118
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
119
  Global Instance ex_mapsto_as_fractional l q :
120
    AsFractional (l {q} -) (λ q, l {q} -)%I q.
121
  Proof. split. done. apply _. Qed.
122

Robbert Krebbers's avatar
Robbert Krebbers committed
123
  Lemma mapsto_valid l q v : l {q} v -  q.
124 125 126 127
  Proof.
    rewrite mapsto_eq /mapsto_def own_valid !discrete_valid.
    by apply pure_mono=> /auth_own_valid /singleton_valid [??].
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
128
  Lemma mapsto_valid_2 l q1 q2 v1 v2 : l {q1} v1 - l {q2} v2 -  (q1 + q2)%Qp.
129
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
130
    iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %->.
131 132 133 134 135 136 137 138 139
    iApply (mapsto_valid l _ v2). by iFrame.
  Qed.

  Lemma gen_heap_alloc σ l v :
    σ !! l = None  gen_heap_ctx σ == gen_heap_ctx (<[l:=v]>σ)  l  v.
  Proof.
    iIntros (?) "Hσ". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
    iMod (own_update with "Hσ") as "[Hσ Hl]".
    { eapply auth_update_alloc,
Ralf Jung's avatar
Ralf Jung committed
140
        (alloc_singleton_local_update _ _ (1%Qp, to_agree (v:leibnizC _)))=> //.
141 142 143 144
      by apply lookup_to_gen_heap_None. }
    iModIntro. rewrite to_gen_heap_insert. iFrame.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
145 146 147 148 149 150 151 152
  Lemma gen_heap_dealloc σ l v :
    gen_heap_ctx σ - l  v == gen_heap_ctx (delete l σ).
  Proof.
    iIntros "Hσ Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
    rewrite to_gen_heap_delete. iApply (own_update_2 with "Hσ Hl").
    eapply auth_update_dealloc, (delete_singleton_local_update _ _ _).
  Qed.

153 154 155 156 157 158 159 160 161 162 163 164 165 166 167
  Lemma gen_heap_valid σ l q v : gen_heap_ctx σ - l {q} v - ⌜σ !! l = Some v.
  Proof.
    iIntros "Hσ Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
    iDestruct (own_valid_2 with "Hσ Hl")
      as %[Hl%gen_heap_singleton_included _]%auth_valid_discrete_2; auto.
  Qed.

  Lemma gen_heap_update σ l v1 v2 :
    gen_heap_ctx σ - l  v1 == gen_heap_ctx (<[l:=v2]>σ)  l  v2.
  Proof.
    iIntros "Hσ Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
    iDestruct (own_valid_2 with "Hσ Hl")
      as %[Hl%gen_heap_singleton_included _]%auth_valid_discrete_2.
    iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
    { eapply auth_update, singleton_local_update,
Ralf Jung's avatar
Ralf Jung committed
168
        (exclusive_local_update _ (1%Qp, to_agree (v2:leibnizC _)))=> //.
169 170 171 172
      by rewrite /to_gen_heap lookup_fmap Hl. }
    iModIntro. rewrite to_gen_heap_insert. iFrame.
  Qed.
End gen_heap.