gen_inv_heap.v 11.6 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
2
3
4
5
6
7
8
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
From iris.algebra Require Import auth excl gmap.
From iris.base_logic.lib Require Import own invariants gen_heap.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".

(** An "invariant" location is a location that has some invariant about its
value attached to it, and that can never be deallocated explicitly by the
program.  It provides a persistent witness that will always allow reading the
location, guaranteeing that the value read will satisfy the invariant.

This is useful for data structures like RDCSS that need to read locations long
after their ownership has been passed back to the client, but do not care *what*
it is that they are reading in that case. In that extreme case, the invariant
may just be [True].

Since invariant locations cannot be deallocated, they only make sense when
modelling languages with garbage collection.  Note that heap_lang does not
actually have explicit dealloaction. However, the proof rules we provide for
heap operations currently are conservative in the sense that they do not expose
this fact.  By making "invariant" locations a separate assertion, we can keep
all the other proofs that do not need it conservative.  *)

Definition inv_heapN: namespace := nroot .@ "inv_heap".
Local Notation "l ↦ v" := (mapsto l 1 v) (at level 20) : bi_scope.

Definition inv_heap_mapUR (L V : Type) `{Countable L} : ucmraT := gmapUR L $ prodR
  (optionR $ exclR $ leibnizO V)
  (agreeR (V -d> PropO)).

Definition to_inv_heap {L V : Type} `{Countable L}
    (h: gmap L (V * (V -d> PropO))) : inv_heap_mapUR L V :=
  prod_map (λ x, Excl' x) to_agree <$> h.

Class inv_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := Inv_HeapG {
  inv_heap_inG :> inG Σ (authR (inv_heap_mapUR L V));
  inv_heap_name : gname
}.
Arguments Inv_HeapG _ _ {_ _ _ _}.
Arguments inv_heap_name {_ _ _ _ _} _ : assert.

Class inv_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
  inv_heap_preG_inG :> inG Σ (authR (inv_heap_mapUR L V))
}.

Definition inv_heapΣ (L V : Type) `{Countable L} : gFunctors :=
  #[ GFunctor (authR (inv_heap_mapUR L V)) ].

Instance subG_inv_heapPreG (L V : Type) `{Countable L} {Σ} :
  subG (inv_heapΣ L V) Σ  inv_heapPreG L V Σ.
Proof. solve_inG. Qed.

Ralf Jung's avatar
Ralf Jung committed
52
Section definitions.
Ralf Jung's avatar
Ralf Jung committed
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
  Context {L V : Type} `{Countable L}.
  Context `{!invG Σ, !gen_heapG L V Σ, gG: !inv_heapG L V Σ}.

  Definition inv_heap_inv_P : iProp Σ :=
    ( h : gmap L (V * (V -d> PropO)),
        own (inv_heap_name gG) ( to_inv_heap h) 
        [ map] l  p  h, p.2 p.1  l  p.1)%I.

  Definition inv_heap_inv : iProp Σ := inv inv_heapN inv_heap_inv_P.

  Definition inv_mapsto_own (l : L) (v : V) (I : V  Prop) : iProp Σ :=
    own (inv_heap_name gG) ( {[l := (Excl' v, to_agree I) ]}).

  Definition inv_mapsto (l : L) (I : V  Prop) : iProp Σ :=
    own (inv_heap_name gG) ( {[l := (None, to_agree I)]}).

Ralf Jung's avatar
Ralf Jung committed
69
70
End definitions.

Ralf Jung's avatar
Ralf Jung committed
71
72
Local Notation "l '↦□' I" := (inv_mapsto l I%stdpp%type)
  (at level 20, format "l  '↦□'  I") : bi_scope.
Ralf Jung's avatar
Ralf Jung committed
73

74
Local Notation "l '↦_' I v" := (inv_mapsto_own l v I%stdpp%type)
Ralf Jung's avatar
Ralf Jung committed
75
  (at level 20, I at level 9, format "l  '↦_' I  v") : bi_scope.
Ralf Jung's avatar
Ralf Jung committed
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115

(* [inv_heap_inv] has no parameters to infer the types from, so we need to
   make them explicit. *)
Arguments inv_heap_inv _ _ {_ _ _ _ _ _}.

Instance: Params (@inv_mapsto_own) 8 := {}.
Instance: Params (@inv_mapsto) 7 := {}.

Section to_inv_heap.
  Context {L V : Type} `{Countable L}.
  Implicit Types (h : gmap L (V * (V -d> PropO))).

  Lemma to_inv_heap_valid h :  to_inv_heap h.
  Proof. intros l. rewrite lookup_fmap. by case (h !! l). Qed.

  Lemma to_inv_heap_singleton l v I :
    to_inv_heap {[l := (v, I)]} =@{inv_heap_mapUR L V} {[l := (Excl' v, to_agree I)]}.
  Proof. by rewrite /to_inv_heap fmap_insert fmap_empty. Qed.

  Lemma to_inv_heap_insert l v I h :
    to_inv_heap (<[l := (v, I)]> h) = <[l := (Excl' v, to_agree I)]> (to_inv_heap h).
  Proof. by rewrite /to_inv_heap fmap_insert. Qed.

  Lemma lookup_to_inv_heap_None h l :
    h !! l = None  to_inv_heap h !! l = None.
  Proof. by rewrite /to_inv_heap lookup_fmap=> ->. Qed.

  Lemma lookup_to_inv_heap_Some h l v I :
    h !! l = Some (v, I)  to_inv_heap h !! l = Some (Excl' v, to_agree I).
  Proof. by rewrite /to_inv_heap lookup_fmap=> ->. Qed.

  Lemma lookup_to_inv_heap_Some_2 h l v' I' :
    to_inv_heap h !! l  Some (v', I') 
     v I, v' = Excl' v  I'  to_agree I  h !! l = Some (v, I).
  Proof.
    rewrite /to_inv_heap /prod_map lookup_fmap. rewrite fmap_Some_equiv.
    intros ([] & Hsome & [Heqv HeqI]); simplify_eq/=; eauto.
  Qed.
End to_inv_heap.

Ralf Jung's avatar
Ralf Jung committed
116
Lemma inv_heap_init (L V : Type) `{Countable L, !invG Σ, !gen_heapG L V Σ, !inv_heapPreG L V Σ} E :
Ralf Jung's avatar
Ralf Jung committed
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
   |==>  _ : inv_heapG L V Σ, |={E}=> inv_heap_inv L V.
Proof.
  iMod (own_alloc ( (to_inv_heap ))) as (γ) "H●".
  { rewrite auth_auth_valid. exact: to_inv_heap_valid. }
  iModIntro.
  iExists (Inv_HeapG L V γ).
  iAssert (inv_heap_inv_P (gG := Inv_HeapG L V γ)) with "[H●]" as "P".
  { iExists _. iFrame. done. }
  iApply (inv_alloc inv_heapN E inv_heap_inv_P with "P").
Qed.

Section inv_heap.
  Context {L V : Type} `{Countable L}.
  Context `{!invG Σ, !gen_heapG L V Σ, gG: !inv_heapG L V Σ}.
  Implicit Types (l : L) (v : V) (I : V  Prop).
  Implicit Types (h : gmap L (V * (V -d> PropO))).

  (** * Helpers *)

  Lemma inv_mapsto_lookup_Some l h I :
Ralf Jung's avatar
Ralf Jung committed
137
    l ↦□ I - own (inv_heap_name gG) ( to_inv_heap h) -
Ralf Jung's avatar
Ralf Jung committed
138
139
140
141
142
143
144
145
146
147
148
149
     v I', h !! l = Some (v, I')   w, I w  I' w .
  Proof.
    iIntros "Hl_inv H◯".
    iDestruct (own_valid_2 with "H◯ Hl_inv") as %[Hincl Hvalid]%auth_both_valid.
    iPureIntro.
    move: Hincl; rewrite singleton_included_l; intros ([v' I'] & Hsome & Hincl).
    apply lookup_to_inv_heap_Some_2 in Hsome as (v'' & I'' & _ & HI & Hh).
    move: Hincl; rewrite HI Some_included_total pair_included
      to_agree_included; intros [??]; eauto.
  Qed.

  Lemma inv_mapsto_own_lookup_Some l v h I :
Ralf Jung's avatar
Ralf Jung committed
150
    l _I v - own (inv_heap_name gG) ( to_inv_heap h) -
Ralf Jung's avatar
Ralf Jung committed
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
      I', h !! l = Some (v, I')   w, I w  I' w .
  Proof.
    iIntros "Hl_inv H●".
    iDestruct (own_valid_2 with "H● Hl_inv") as %[Hincl Hvalid]%auth_both_valid.
    iPureIntro.
    move: Hincl; rewrite singleton_included_l; intros ([v' I'] & Hsome & Hincl).
    apply lookup_to_inv_heap_Some_2 in Hsome as (v'' & I'' & -> & HI & Hh).
    move: Hincl; rewrite HI Some_included_total pair_included
      Excl_included to_agree_included; intros [-> ?]; eauto.
  Qed.

  (** * Typeclass instances *)

  (* FIXME(Coq #6294): needs new unification
  The uses of [apply:] and [move: ..; rewrite ..] (by lack of [apply: .. in ..])
  in this file are needed because Coq's default unification algorithm fails. *)
  Global Instance inv_mapsto_own_proper l v :
    Proper (pointwise_relation _ iff ==> ()) (inv_mapsto_own l v).
  Proof.
    intros I1 I2 ?. rewrite /inv_mapsto_own. do 2 f_equiv.
    apply: singletonM_proper. f_equiv. by apply: to_agree_proper.
  Qed.
  Global Instance inv_mapsto_proper l :
    Proper (pointwise_relation _ iff ==> ()) (inv_mapsto l).
  Proof.
    intros I1 I2 ?. rewrite /inv_mapsto. do 2 f_equiv.
    apply: singletonM_proper. f_equiv. by apply: to_agree_proper.
  Qed.

Ralf Jung's avatar
Ralf Jung committed
180
181
182
  Global Instance inv_heap_inv_persistent : Persistent (inv_heap_inv L V).
  Proof. apply _. Qed.

Ralf Jung's avatar
Ralf Jung committed
183
  Global Instance inv_mapsto_persistent l I : Persistent (l ↦□ I).
Ralf Jung's avatar
Ralf Jung committed
184
  Proof. apply _. Qed.
Ralf Jung's avatar
Ralf Jung committed
185

Ralf Jung's avatar
Ralf Jung committed
186
  Global Instance inv_mapsto_timeless l I : Timeless (l ↦□ I).
Ralf Jung's avatar
Ralf Jung committed
187
  Proof. apply _. Qed.
Ralf Jung's avatar
Ralf Jung committed
188

Ralf Jung's avatar
Ralf Jung committed
189
  Global Instance inv_mapsto_own_timeless l v I : Timeless (l _I v).
Ralf Jung's avatar
Ralf Jung committed
190
  Proof. apply _. Qed.
Ralf Jung's avatar
Ralf Jung committed
191
192
193
194
195
196

  (** * Public lemmas *)

  Lemma make_inv_mapsto l v I E :
    inv_heapN  E 
    I v 
Ralf Jung's avatar
Ralf Jung committed
197
    inv_heap_inv L V - l  v ={E}= l _I v.
Ralf Jung's avatar
Ralf Jung committed
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
  Proof.
    iIntros (HN HI) "#Hinv Hl".
    iMod (inv_acc_timeless _ inv_heapN with "Hinv") as "[HP Hclose]"; first done.
    iDestruct "HP" as (h) "[H● HsepM]".
    destruct (h !! l) as [v'| ] eqn: Hlookup.
    - (* auth map contains l --> contradiction *)
      iDestruct (big_sepM_lookup with "HsepM") as "[_ Hl']"; first done.
      by iDestruct (mapsto_valid_2 with "Hl Hl'") as %?.
    - iMod (own_update with "H●") as "[H● H◯]".
      { apply lookup_to_inv_heap_None in Hlookup.
        apply (auth_update_alloc _
          (to_inv_heap (<[l:=(v,I)]> h)) (to_inv_heap ({[l:=(v,I)]}))).
        rewrite to_inv_heap_insert to_inv_heap_singleton.
        by apply: alloc_singleton_local_update. }
      iMod ("Hclose" with "[H● HsepM Hl]").
      + iExists _.
        iDestruct (big_sepM_insert _ _ _ (_,_) with "[$HsepM $Hl]")
          as "HsepM"; auto with iFrame.
      + iModIntro. by rewrite /inv_mapsto_own to_inv_heap_singleton.
  Qed.

Ralf Jung's avatar
Ralf Jung committed
219
  Lemma inv_mapsto_own_inv l v I : l _I v - l ↦□ I.
Ralf Jung's avatar
Ralf Jung committed
220
221
222
223
224
225
226
227
228
229
  Proof.
    apply own_mono, auth_frag_mono. rewrite singleton_included pair_included.
    right. split; [apply: ucmra_unit_least|done].
  Qed.

  (** An accessor to make use of [inv_mapsto_own].
    This opens the invariant *before* consuming [inv_mapsto_own] so that you can use
    this before opening an atomic update that provides [inv_mapsto_own]!. *)
  Lemma inv_mapsto_own_acc_strong E :
    inv_heapN  E 
Ralf Jung's avatar
Ralf Jung committed
230
    inv_heap_inv L V ={E, E  inv_heapN}=  l v I, l _I v -
Ralf Jung's avatar
Ralf Jung committed
231
232
233
234
      (I v  l  v  ( w, I w  - l  w ==
        inv_mapsto_own l w I  |={E  inv_heapN, E}=> True)).
  Proof.
    iIntros (HN) "#Hinv".
Ralf Jung's avatar
Ralf Jung committed
235
    iMod (inv_acc_timeless _ inv_heapN _ with "Hinv") as "[HP Hclose]"; first done.
Ralf Jung's avatar
Ralf Jung committed
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
    iIntros "!>" (l v I) "Hl_inv".
    iDestruct "HP" as (h) "[H● HsepM]".
    iDestruct (inv_mapsto_own_lookup_Some with "Hl_inv H●") as %(I'&?&HI').
    setoid_rewrite HI'.
    iDestruct (big_sepM_delete with "HsepM") as "[[HI Hl] HsepM]"; first done.
    iIntros "{$HI $Hl}" (w ?) "Hl".
    iMod (own_update_2 with "H● Hl_inv") as "[H● H◯]".
    { apply (auth_update _ _ (<[l := (Excl' w, to_agree I')]> (to_inv_heap h))
             {[l := (Excl' w, to_agree I)]}).
      apply: singleton_local_update.
      { by apply lookup_to_inv_heap_Some. }
      apply: prod_local_update_1. apply: option_local_update.
      apply: exclusive_local_update. done. }
    iDestruct (big_sepM_insert _ _ _ (w, I') with "[$HsepM $Hl //]") as "HsepM".
    { apply lookup_delete. }
    rewrite insert_delete -to_inv_heap_insert. iIntros "!> {$H◯}".
    iApply ("Hclose" with "[H● HsepM]"). iExists _; by iFrame.
  Qed.

  (** Derive a more standard accessor. *)
  Lemma inv_mapsto_own_acc E l v I:
    inv_heapN  E 
Ralf Jung's avatar
Ralf Jung committed
258
259
    inv_heap_inv L V - l _I v ={E, E  inv_heapN}=
      (I v  l  v  ( w, I w  - l  w ={E  inv_heapN, E}= l _I w)).
Ralf Jung's avatar
Ralf Jung committed
260
261
262
263
264
265
266
267
268
269
  Proof.
    iIntros (?) "#Hinv Hl".
    iMod (inv_mapsto_own_acc_strong with "Hinv") as "Hacc"; first done.
    iDestruct ("Hacc" with "Hl") as "(HI & Hl & Hclose)".
    iIntros "!> {$HI $Hl}" (w) "HI Hl".
    iMod ("Hclose" with "HI Hl") as "[$ $]".
  Qed.

  Lemma inv_mapsto_acc l I E :
    inv_heapN  E 
Ralf Jung's avatar
Ralf Jung committed
270
    inv_heap_inv L V - l ↦□ I ={E, E  inv_heapN}=
Ralf Jung's avatar
Ralf Jung committed
271
272
273
     v, I v  l  v  (l  v ={E  inv_heapN, E}= True).
  Proof.
    iIntros (HN) "#Hinv Hl_inv".
Ralf Jung's avatar
Ralf Jung committed
274
    iMod (inv_acc_timeless _ inv_heapN _ with "Hinv") as "[HP Hclose]"; first done.
Ralf Jung's avatar
Ralf Jung committed
275
276
277
    iModIntro.
    iDestruct "HP" as (h) "[H● HsepM]".
    iDestruct (inv_mapsto_lookup_Some with "Hl_inv H●") as %(v&I'&?&HI').
Ralf Jung's avatar
Ralf Jung committed
278
    iDestruct (big_sepM_lookup_acc with "HsepM") as "[[#HI Hl] HsepM]"; first done.
Ralf Jung's avatar
Ralf Jung committed
279
280
281
282
283
284
285
286
    setoid_rewrite HI'.
    iExists _. iIntros "{$HI $Hl} Hl".
    iMod ("Hclose" with "[H● HsepM Hl]"); last done.
    iExists _. iFrame "H●". iApply ("HsepM" with "[$Hl //]").
  Qed.

End inv_heap.

Ralf Jung's avatar
Ralf Jung committed
287
Typeclasses Opaque inv_heap_inv inv_mapsto inv_mapsto_own.