locking_heap.v 18.8 KB
Newer Older
Dan Frumin's avatar
Dan Frumin committed
1
2
From iris.algebra Require Import cmra auth gmap frac agree.
From iris.bi.lib Require Import fractional.
Dan Frumin's avatar
Dan Frumin committed
3
4
From iris.base_logic.lib Require Export own.
From iris.proofmode Require Import tactics.
Robbert Krebbers's avatar
Robbert Krebbers committed
5
From iris_c.lib Require Import list.
Dan Frumin's avatar
Dan Frumin committed
6
Set Default Proof Using "Type".
7
Local Open Scope nat_scope.
Dan Frumin's avatar
Dan Frumin committed
8

9
10
11
12
Inductive lvl :=
  | LLvl : lvl
  | ULvl : lvl.
Canonical Structure lvlC := leibnizC lvl.
Dan Frumin's avatar
Dan Frumin committed
13

14
Instance lvl_EqDecision : EqDecision lvl.
Léon Gondelman's avatar
Léon Gondelman committed
15
16
Proof. solve_decision. Defined.

17
18
Instance lvl_op : Op lvl := λ lv1 lv2,
  match lv1, lv2 with
Dan Frumin's avatar
Dan Frumin committed
19
20
21
22
  | ULvl,_ => ULvl
  | _,ULvl => ULvl
  | _,_ => LLvl
  end.
23
24
25
Instance lvl_valid : Valid lvl := λ _, True.
Instance lvl_unit : Unit lvl := LLvl.
Instance lvl_pcore : PCore lvl := λ _, Some LLvl.
Robbert Krebbers's avatar
Robbert Krebbers committed
26
27
28
29
30
Lemma lvl_included lv1 lv2 :
  lv1  lv2  match lv2 with
              | ULvl => True
              | LLvl => if lv1 is LLvl then True else False
              end.
Dan Frumin's avatar
Dan Frumin committed
31
Proof.
32
  split.
Robbert Krebbers's avatar
Robbert Krebbers committed
33
34
  - intros [[] ->%leibniz_equiv]; by destruct lv1.
  - exists lv2. by destruct lv1, lv2.
Dan Frumin's avatar
Dan Frumin committed
35
36
Qed.

37
38
Lemma lvl_idemp (lv : lvl) : lv  lv = lv.
Proof. by destruct lv. Qed.
Dan Frumin's avatar
Dan Frumin committed
39

40
Lemma lvl_ra_mixin : RAMixin lvl.
Dan Frumin's avatar
Dan Frumin committed
41
42
43
Proof.
  apply ra_total_mixin; try by eauto.
  - solve_proper.
44
45
46
47
48
  - by intros [] [] [].
  - by intros [] [].
  - by intros [].
  - intros lv1 lv2 ?%lvl_included.
    apply lvl_included. destruct lv1, lv2; compute; firstorder.
Dan Frumin's avatar
Dan Frumin committed
49
50
Qed.

51
Canonical Structure lvlR : cmraT := discreteR lvl lvl_ra_mixin.
Dan Frumin's avatar
Dan Frumin committed
52
53
54
Global Instance lvl_cmra_discrete : CmraDiscrete lvlR.
Proof. apply discrete_cmra_discrete. Qed.

55
Lemma lvl_ucmra_mixin : UcmraMixin lvl.
56
Proof. split; try (apply _ || done). by intros []. Qed.
57
Canonical Structure lvlUR : ucmraT := UcmraT lvl lvl_ucmra_mixin.
Dan Frumin's avatar
Dan Frumin committed
58
59

(* Auth (Loc -> (Q * Level)) *)
60
61
62
63
Definition cloc : Type := loc * nat.
Instance cloc_eq_dec : EqDecision cloc | 0 := _.
Instance cloc_countable : Countable cloc | 0 := _.
Instance cloc_inhabited : Inhabited cloc | 0 := _.
Robbert Krebbers's avatar
Robbert Krebbers committed
64

Dan Frumin's avatar
Dan Frumin committed
65
Definition locking_heapUR : ucmraT :=
Robbert Krebbers's avatar
Robbert Krebbers committed
66
  gmapUR cloc (prodR (prodR fracR lvlUR) (agreeR valC)).
Dan Frumin's avatar
Dan Frumin committed
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85

(** The CMRA we need. *)
Class locking_heapG (Σ : gFunctors) := LHeapG {
  lheap_inG :> inG Σ (authR locking_heapUR);
  lheap_name : gname
}.
Class locking_heapPreG (Σ : gFunctors) :=
  { lheap_preG_inG :> inG Σ (authR locking_heapUR) }.

Definition locking_heapΣ : gFunctors :=
  #[GFunctor (authR locking_heapUR)].

Instance subG_heapPreG {Σ} :
  subG locking_heapΣ Σ  locking_heapPreG Σ.
Proof. solve_inG. Qed.

Section definitions.
  Context `{hG : locking_heapG Σ, !heapG Σ}.

Robbert Krebbers's avatar
Robbert Krebbers committed
86
  Definition to_locking_heap (σ : gmap cloc (lvl * val)) : locking_heapUR :=
87
    fmap (λ '(lv,v), (1%Qp, lv, to_agree v)) σ.
Dan Frumin's avatar
Dan Frumin committed
88

Dan Frumin's avatar
Dan Frumin committed
89
  (* σ^{-1}(L) *)
Robbert Krebbers's avatar
Robbert Krebbers committed
90
91
  Definition locked_locs (σ : gmap cloc (lvl * val)) : gset cloc :=
    dom _ (filter (λ x, x.2.1 = LLvl) σ).
Dan Frumin's avatar
Dan Frumin committed
92

93
94
95
  (** Pointer arithmetic *)
  Definition cloc_lt (p q : cloc) : bool :=
    bool_decide (p.1 = q.1  p.2 < q.2).
96
97
98
99
100
101
  Definition cloc_add (cl : cloc) (i : nat) : cloc := (cl.1, cl.2 + i).

  Definition cloc_to_val (cl : cloc) : val := (#cl.1, #cl.2).
  Definition cloc_of_val (v : val) : option cloc :=
    match v return option (loc * nat) with
    | (LitV (LitLoc l), LitV (LitInt i))%V => guard (0  i)%Z; Some (l, Z.to_nat i)
Robbert Krebbers's avatar
Robbert Krebbers committed
102
103
104
105
106
    | _ => None
    end.

  Definition full_locking_heap (σ : gmap cloc (lvl * val)) :=
    ( τ : gmap loc (list (lvl * val)),
107
        cl, σ !! cl = τ !! cl.1 = lookup (M:=list _) cl.2  
Robbert Krebbers's avatar
Robbert Krebbers committed
108
      own lheap_name ( (to_locking_heap σ)) 
109
      [ map] llvvs  τ,  lv, l  SOMEV lv   is_list lv (snd <$> lvvs) )%I.
Dan Frumin's avatar
Dan Frumin committed
110

Robbert Krebbers's avatar
Robbert Krebbers committed
111
112
113
114
  Definition mapsto_def (cl : cloc) (lv : lvl) (q : frac) (v: val) : iProp Σ :=
    ( lv',
      lv  lv' 
      own lheap_name ( {[ cl := (q, lv', to_agree v) ]}))%I.
Dan Frumin's avatar
Dan Frumin committed
115
116
117
118
119
120

  Definition mapsto_aux : seal (@mapsto_def). by eexists. Qed.
  Definition mapsto := unseal mapsto_aux.
  Definition mapsto_eq : @mapsto = @mapsto_def := seal_eq mapsto_aux.
End definitions.

Robbert Krebbers's avatar
Robbert Krebbers committed
121
122
123
124
125
126
127
128
129
Notation "cl ↦C[ lv ]{ q } v" :=
  (mapsto cl lv q%Qp v%V)
  (at level 20, lv, q at level 50, format "cl  ↦C[ lv ]{ q }  v") : bi_scope.
Notation "cl ↦C[ lv ] v" := (cl C[lv]{1} v)%I
  (at level 20, lv at level 50, format "cl  ↦C[ lv ]  v") : bi_scope.
Notation "cl ↦C{ q } v" := (cl C[ULvl]{q} v)%I
  (at level 20, q at level 50, format "cl  ↦C{ q }  v") : bi_scope.
Notation "cl ↦C v" := (cl C[ULvl]{1} v)%I
  (at level 20, format "cl  ↦C  v") : bi_scope.
130

131
132
133
134
135
136
137
Notation "cl ↦C{ q }∗ vs" :=
  ([ list] i  v  vs, cloc_add cl i C{q} v)%I
  (at level 20, q at level 50, format "cl  ↦C{ q }∗  vs") : bi_scope.
Notation "cl ↦C∗ vs" :=
  ([ list] i  v  vs, cloc_add cl i C v)%I
  (at level 20, format "cl  ↦C∗  vs") : bi_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
138
139
Lemma to_locking_heap_valid (σ : gmap cloc (lvl * val)) :  to_locking_heap σ.
Proof. intros cl. rewrite lookup_fmap. by destruct (σ !! cl) as [[]|]. Qed.
Dan Frumin's avatar
Dan Frumin committed
140

141
142
Lemma locking_heap_init `{locking_heapPreG Σ, !heapG Σ} :
  (|==>  _ : locking_heapG Σ, full_locking_heap )%I.
Dan Frumin's avatar
Dan Frumin committed
143
Proof.
144
  iMod (own_alloc ( to_locking_heap )) as (γ) "Hh".
Dan Frumin's avatar
Dan Frumin committed
145
  { apply: auth_auth_valid. exact: to_locking_heap_valid. }
146
  iModIntro. iExists (LHeapG Σ _ γ), . auto.
Dan Frumin's avatar
Dan Frumin committed
147
148
149
150
Qed.

Section properties.
  Context `{hG : locking_heapG Σ, !heapG Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
151
  Implicit Type σ : gmap cloc (lvl * val).
152
  Implicit Type lv : lvl.
Dan Frumin's avatar
Dan Frumin committed
153
  Implicit Type l : loc.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
155
  Implicit Type i : nat.
  Implicit Type cl : cloc.
Dan Frumin's avatar
Dan Frumin committed
156

Robbert Krebbers's avatar
Robbert Krebbers committed
157
158
  Lemma mapsto_value_agree lv lv' cl q q' v v' :
    cl C[lv]{q} v - cl C[lv']{q'} v' - v = v'.
Dan Frumin's avatar
Dan Frumin committed
159
160
  Proof.
    rewrite mapsto_eq /mapsto_def.
161
162
163
    iDestruct 1 as (lv1 ?) "Hl1". iDestruct 1 as (lv2 ?) "Hl2".
    iDestruct (own_valid_2 with "Hl1 Hl2") as %Ho%auth_own_valid. iPureIntro.
    revert Ho. rewrite /= op_singleton singleton_valid. by intros [_ ?%agree_op_invL'].
Dan Frumin's avatar
Dan Frumin committed
164
165
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
166
167
  Lemma mapsto_combine lv lv' cl q q' v :
    cl C[lv]{q} v - cl C[lv']{q'} v - cl C[lvlv']{q+q'} v.
Dan Frumin's avatar
Dan Frumin committed
168
169
  Proof.
    rewrite mapsto_eq /mapsto_def.
170
171
    iDestruct 1 as (lv1 ?) "Hl1". iDestruct 1 as (lv2 ?) "Hl2".
    iExists (lv1  lv2). iSplitR.
Robbert Krebbers's avatar
Robbert Krebbers committed
172
173
    { iPureIntro. by apply: cmra_mono. }
    iCombine "Hl1 Hl2" as "Hl". rewrite frac_op'. by iFrame.
Dan Frumin's avatar
Dan Frumin committed
174
175
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
176
177
  Global Instance from_sep_mapsto cl lv lv' q q' v :
    FromSep (cl C[lvlv']{q+q'} v) (cl C[lv]{q} v) (cl C[lv']{q'} v).
178
179
180
181
182
  Proof.
    rewrite /FromSep. iIntros "[Hl1 Hl2]".
    iApply (mapsto_combine with "Hl1 Hl2").
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
  Global Instance mapsto_timeless cl lv q v : Timeless (cl C[lv]{q} v).
  Proof. rewrite mapsto_eq /mapsto_def. apply _. Qed.

  Global Instance mapsto_fractional cl lv v : Fractional (λ q, cl C[lv]{q} v)%I.
  Proof.
    intros p q. iSplit.
    - rewrite mapsto_eq /mapsto_def.
      iDestruct 1 as (lv' ?) "Hl". rewrite -(lvl_idemp lv').
      iDestruct "Hl" as "[Hl Hl']". iSplitL "Hl"; eauto 10.
    - iIntros "[H1 H2]". iDestruct (mapsto_combine with "H1 H2") as "H".
      by rewrite lvl_idemp.
  Qed.

  Global Instance mapsto_as_fractional cl q lv v :
    AsFractional (cl C[lv]{q} v) (λ q, cl C[lv]{q} v)%I q.
  Proof. split. done. apply _. Qed.

  Lemma mapsto_downgrade' lv lv' cl q v :
    lv  lv'  cl C[lv']{q} v - cl C[lv]{q} v.
  Proof.
    rewrite mapsto_eq /mapsto_def. iDestruct 1 as (lv'' ?) "Hl".
    iExists lv''. iSplit; eauto. iPureIntro. by transitivity lv'.
  Qed.

  Lemma mapsto_downgrade lv cl q v : cl C{q} v - cl C[lv]{q} v.
  Proof. apply mapsto_downgrade'. by apply lvl_included. Qed.

210
211
212
  Lemma cloc_of_to_val cl : cloc_of_val (cloc_to_val cl) = Some cl.
  Proof. destruct cl. by rewrite /= option_guard_True ?Nat2Z.id; last lia. Qed.
  Lemma cloc_to_of_val v cl : cloc_of_val v = Some cl  cloc_to_val cl = v.
Robbert Krebbers's avatar
Robbert Krebbers committed
213
  Proof.
214
215
    rewrite /cloc_of_val /cloc_to_val=> ?.
    destruct cl; repeat (case_match || simplify_option_eq); auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
216
217
218
219
220
    by rewrite Z2Nat.inj_pos positive_nat_Z.
  Qed.

  Lemma to_locking_heap_insert σ cl lv v :
    to_locking_heap (<[cl:=(lv,v)]> σ) = <[cl:=(1%Qp, lv, to_agree v)]>(to_locking_heap σ).
Dan Frumin's avatar
Dan Frumin committed
221
222
  Proof. by rewrite /to_locking_heap fmap_insert. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
223
224
  Lemma to_locking_heap_lookup_Some σ li lv v :
    σ !! li = Some (lv,v)  to_locking_heap σ !! li = Some (1%Qp, lv, to_agree v).
Dan Frumin's avatar
Dan Frumin committed
225
  Proof. rewrite /to_locking_heap lookup_fmap => -> //. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
226
227
  Lemma to_locking_heap_lookup_None σ li :
    σ !! li = None  to_locking_heap σ !! li = None.
Dan Frumin's avatar
Dan Frumin committed
228
  Proof. rewrite /to_locking_heap lookup_fmap => -> //. Qed.
Dan Frumin's avatar
Dan Frumin committed
229

Robbert Krebbers's avatar
Robbert Krebbers committed
230
231
  Lemma locked_locs_lock σ cl v :
    locked_locs (<[cl:=(LLvl,v)]>σ) = {[cl]}  locked_locs σ.
Dan Frumin's avatar
Dan Frumin committed
232
233
234
235
236
  Proof.
    rewrite /locked_locs -map_filter_lookup_insert; last done.
    apply dom_insert_L.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
237
238
239
  Lemma locked_locs_unlock σ cl v :
    σ !! cl = Some (LLvl,v) 
    locked_locs (<[cl:=(ULvl,v)]>σ) = locked_locs σ  {[cl]}.
Dan Frumin's avatar
Dan Frumin committed
240
241
  Proof.
    intros Hl. rewrite /locked_locs -dom_delete_L. f_equal.
242
243
    apply map_eq=> j. apply option_eq=> x.
    rewrite lookup_delete_Some !map_filter_lookup_Some lookup_insert_Some. naive_solver.
Dan Frumin's avatar
Dan Frumin committed
244
245
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
246
247
248
  Lemma locked_locs_alloc_unlocked σ cl v :
    σ !! cl = None 
    locked_locs (<[cl:=(ULvl,v)]>σ) = locked_locs σ.
Dan Frumin's avatar
Dan Frumin committed
249
250
  Proof.
    intros Hl. rewrite /locked_locs. f_equal.
251
252
    apply map_eq => j. apply option_eq=> x.
    rewrite !map_filter_lookup_Some lookup_insert_Some. naive_solver.
Dan Frumin's avatar
Dan Frumin committed
253
  Qed.
Dan Frumin's avatar
Dan Frumin committed
254

Robbert Krebbers's avatar
Robbert Krebbers committed
255
256
257
  Lemma heap_singleton_included σ cl lv q v :
    {[cl := (q, lv, to_agree v)]}  to_locking_heap σ 
     lv', lv  lv'  σ !! cl = Some (lv', v).
Dan Frumin's avatar
Dan Frumin committed
258
  Proof.
259
260
261
262
    rewrite singleton_included=> -[[[q' lv'] av] []].
    rewrite /to_gen_heap lookup_fmap fmap_Some_equiv => -[[lv'' av'] [Hl [/= -> ->]]].
    move=> /Some_pair_included_total_2 [/Some_pair_included_total_2] [_] Hxb'.
    move=> /to_agree_included /leibniz_equiv_iff=> ->. by exists lv''.
Dan Frumin's avatar
Dan Frumin committed
263
264
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
265
266
  Lemma locked_locs_unlocked σ cl v q :
    cl C{q} v - full_locking_heap σ - cl  locked_locs σ⌝.
Dan Frumin's avatar
Dan Frumin committed
267
268
  Proof.
    rewrite mapsto_eq /mapsto_def /full_locking_heap.
Robbert Krebbers's avatar
Robbert Krebbers committed
269
270
271
272
    iDestruct 1 as (lv ?%lvl_included) "Hl". iDestruct 1 as (τ Hτ) "[Hfull Hmap]".
    iDestruct (own_valid_2 with "Hfull Hl")
      as %[[lv' [?%lvl_included Hl]]%heap_singleton_included _]%auth_valid_discrete_2.
    assert (lv' = ULvl) as -> by (by destruct lv', lv).
Dan Frumin's avatar
Dan Frumin committed
273
    iPureIntro. rewrite /locked_locs.
Robbert Krebbers's avatar
Robbert Krebbers committed
274
275
    apply not_elem_of_dom, map_filter_lookup_None.
    right. intros [??]. by rewrite Hl=>[= <- <-].
Dan Frumin's avatar
Dan Frumin committed
276
277
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
278
279
  Lemma full_locking_heap_unlocked σ cl v q :
    cl C{q} v - full_locking_heap σ - ⌜σ !! cl = Some (ULvl,v).
Dan Frumin's avatar
Dan Frumin committed
280
281
  Proof.
    rewrite mapsto_eq /mapsto_def /full_locking_heap.
Robbert Krebbers's avatar
Robbert Krebbers committed
282
283
284
    iDestruct 1 as ([] []%lvl_included) "Hl". iDestruct 1 as (τ Hτ) "[Hfull Hmap]".
    iDestruct (own_valid_2 with "Hfull Hl")
      as %[[[] [[]%lvl_included Hl]]%heap_singleton_included _]%auth_valid_discrete_2; auto.
Dan Frumin's avatar
Dan Frumin committed
285
286
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
287
288
  Lemma full_locking_heap_present σ cl v q :
    cl C[LLvl]{q} v - full_locking_heap σ - is_Some (σ !! cl).
Dan Frumin's avatar
Dan Frumin committed
289
290
  Proof.
    rewrite mapsto_eq /mapsto_def /full_locking_heap.
Robbert Krebbers's avatar
Robbert Krebbers committed
291
292
293
    iDestruct 1 as (lv _) "Hl". iDestruct 1 as (τ Hτ) "[Hfull Hmap]".
    iDestruct (own_valid_2 with "Hfull Hl")
      as %[[y [? ?]]%heap_singleton_included _]%auth_valid_discrete_2; eauto.
Dan Frumin's avatar
Dan Frumin committed
294
295
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
296
  Lemma locking_heap_load cl lv q v σ :
297
298
    full_locking_heap σ - cl C[lv]{q} v ==  ll vs,
       is_list ll vs    vs !! cl.2 = Some v  
299
      cl.1  SOMEV ll  (cl.1  SOMEV ll - full_locking_heap σ  cl C[lv]{q} v).
Dan Frumin's avatar
Dan Frumin committed
300
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
301
302
303
304
    iDestruct 1 as (τ Hτ) "[Hσ Hτ]".
    rewrite mapsto_eq /mapsto_def; iDestruct 1 as (lv' ?) "Hl".
    iDestruct (own_valid_2 with "Hσ Hl")
      as %[(lv''&?&Hσ)%heap_singleton_included _]%auth_valid_discrete_2.
305
    move: (Hσ); rewrite Hτ=> /bind_Some [lvvs [? Hi]].
Robbert Krebbers's avatar
Robbert Krebbers committed
306
    iDestruct (big_sepM_lookup_acc with "Hτ") as "[H Hclose]"; first done.
307
    iDestruct "H" as (ll) "[Hll %]". iModIntro. iExists ll, lvvs.*2.
Robbert Krebbers's avatar
Robbert Krebbers committed
308
309
310
311
312
    repeat iSplit; auto.
    { iPureIntro. by rewrite list_lookup_fmap Hi. }
    iIntros "{$Hll} Hll". iDestruct ("Hclose" with "[Hll]") as "Hτ"; eauto.
    iSplitL "Hσ Hτ"; first (iExists τ; by eauto with iFrame).
    iExists lv'. auto.
Dan Frumin's avatar
Dan Frumin committed
313
314
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
315
  Lemma locking_heap_store cl lv v σ :
316
317
    full_locking_heap σ - cl C[lv] v ==  ll vs,
       is_list ll vs    vs !! cl.2 = Some v  
318
319
      cl.1  SOMEV ll 
      ( ll' lv' v',  is_list ll' (<[cl.2:=v']>vs)  - cl.1  SOMEV ll' ==
Robbert Krebbers's avatar
Robbert Krebbers committed
320
        full_locking_heap (<[cl:=(lv',v')]>σ)  cl C[lv'] v').
Dan Frumin's avatar
Dan Frumin committed
321
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
322
323
324
325
    iDestruct 1 as (τ Hτ) "[Hσ Hτ]".
    rewrite mapsto_eq /mapsto_def; iDestruct 1 as (lv' ?) "Hl".
    iDestruct (own_valid_2 with "Hσ Hl")
      as %[(lv''&?&Hσ)%heap_singleton_included _]%auth_valid_discrete_2.
326
    move: (Hσ); rewrite Hτ=> /bind_Some [lvvs [Hτl Hi]].
Robbert Krebbers's avatar
Robbert Krebbers committed
327
    iDestruct (big_sepM_delete with "Hτ") as "[H Hτ]"; first done.
328
    iDestruct "H" as (ll) "[Hll %]". iModIntro. iExists ll, lvvs.*2.
Robbert Krebbers's avatar
Robbert Krebbers committed
329
330
331
332
333
334
335
336
    repeat iSplit; auto.
    { iPureIntro. by rewrite list_lookup_fmap Hi. }
    iIntros "{$Hll}" (ll' lv''' v' ?) "Hll".
    iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
    { by eapply auth_update, singleton_local_update,
        (exclusive_local_update _ (1%Qp, lv''', to_agree v'));
        first by apply to_locking_heap_lookup_Some. }
    iModIntro. iSplitL "Hσ Hτ Hll"; last auto.
337
338
339
340
341
342
343
344
345
    iExists (<[cl.1:=(<[cl.2:=(lv''',v')]> lvvs)]>τ).
    rewrite to_locking_heap_insert. iFrame "Hσ". iSplit.
    { destruct cl as [l i]; iPureIntro=> -[l' i']; simpl in *.
      destruct (decide (l' = l)) as [->|?].
      { destruct (decide (i' = i)) as [->|?].
        - rewrite !lookup_insert /= list_lookup_insert //. by eapply lookup_lt_Some.
        - rewrite lookup_insert /= list_lookup_insert_ne //.
          rewrite lookup_insert_ne; last congruence. by rewrite Hτ Hτl. }
      rewrite !lookup_insert_ne; [|congruence..]. by rewrite Hτ. }
Robbert Krebbers's avatar
Robbert Krebbers committed
346
347
348
349
350
    rewrite -insert_delete.
    iApply (big_sepM_insert with "[$Hτ Hll]"); first by rewrite lookup_delete.
    iExists ll'. iFrame. by rewrite list_fmap_insert.
  Qed.

351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
  Definition alloc_heap (σ : gmap cloc (lvl * val)) (l : loc) :
      list val  nat  gmap cloc (lvl * val) :=
    foldr (λ v go i, <[(l,i):=(ULvl,v)]> (go (S i))) (λ _, σ).

  Lemma alloc_heap_None σ l vs j1 j2 :
    ( i, σ !! (l,i) = None)  
    j2 < j1  alloc_heap σ l vs j1 !! (l, j2) = None.
  Proof.
    intros Hσi. revert j1 j2. induction vs as [|v' vs IH]=> j1 j2 ?; csimpl.
    { by rewrite Hσi. }
    rewrite lookup_insert_ne; last (intros [=]; lia).
    by rewrite IH; last lia.
  Qed.

  Lemma alloc_heap_lookup σ l vs i j :
    ( i, σ !! (l,i) = None)  
    alloc_heap σ l vs j !! (l, j + i) = ((ULvl,) <$> vs) !! i.
  Proof.
    intros Hσi. revert i j. induction vs as [|v vs IH]=> i j; csimpl.
    { by rewrite Hσi. }
    destruct i as [|i]; simpl.
    { by rewrite Nat.add_0_r lookup_insert. }
    rewrite Nat.add_succ_r lookup_insert_ne; last (intros [=]; lia).
    apply (IH i (S j)).
  Qed.

  Lemma alloc_heap_lookup_ne σ l l' vs i j :
    l  l' 
    alloc_heap σ l vs j !! (l', i) = σ !! (l', i).
  Proof.
    intros Hl. revert i j. induction vs as [|v vs IH]=> i j //; csimpl.
    by rewrite lookup_insert_ne; last congruence.
  Qed.

  Lemma locked_locs_alloc_heap σ l vs j :
    ( i, σ !! (l,i) = None)  
    locked_locs (alloc_heap σ l vs j) = locked_locs σ.
  Proof.
    intros ?. revert j. induction vs as [|v vs IH]=> j //=.
    rewrite locked_locs_alloc_unlocked // alloc_heap_None //; lia.
  Qed.

  Lemma locking_heap_alloc l ll vs σ :
Robbert Krebbers's avatar
Robbert Krebbers committed
394
    is_list ll vs 
395
    full_locking_heap σ - l  SOMEV ll ==
396
397
      i, σ !! (l,i) = None  
    full_locking_heap (alloc_heap σ l vs O)  (l,0) C vs.
Robbert Krebbers's avatar
Robbert Krebbers committed
398
  Proof.
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
    intros Hll. iDestruct 1 as (τ Hτ) "[Hσ Hτ]". iIntros "Hll".
    set (f := foldr (λ v go i, <[(l,i):=(ULvl,v)]> (go (S i))) (λ _, σ)).
    iAssert  τ !! l = None %I as %Hτi.
    { rewrite eq_None_not_Some. iIntros ([lvv ?]).
      iDestruct (big_sepM_lookup with "Hτ") as (ll') "[Hll' _]"; first done.
      by iDestruct (mapsto_valid_2 with "Hll Hll'") as %[]. }
    iAssert   i, σ !! (l,i) = None %I as %Hσi.
    { iIntros (i). by rewrite Hτ Hτi. }
    iAssert (|==> own lheap_name ( to_locking_heap (f vs 0)) 
      [ list] iv  vs, own lheap_name ( {[ (l,0 + i) := (1%Qp, ULvl,to_agree v) ]}))%I
      with "[Hσ]" as ">[Hσ Hl]".
    { clear Hll. generalize 0=> j.
      iInduction vs as [|v vs] "IH" forall (j); simpl; first by iFrame.
      iMod ("IH" $! (S j) with "Hσ") as "[Hσ Hls]".
      iMod (own_update with "Hσ") as "[Hσ Hl]".
      { eapply auth_update_alloc,
          (alloc_singleton_local_update _ (l,j) (1%Qp, ULvl, to_agree v)); try done.
        apply to_locking_heap_lookup_None. rewrite alloc_heap_None //. lia. }
      iModIntro. rewrite -to_locking_heap_insert Nat.add_0_r; iFrame "Hσ Hl".
      iApply (big_sepL_impl with "Hls"); iIntros "!>" (k w _) "?".
      by rewrite Nat.add_succ_r. }
    iModIntro. iSplit; first done. iSplitL "Hσ Hτ Hll".
    { iExists (<[l:=(ULvl,) <$> vs]> τ). iFrame "Hσ". iSplit.
      - iPureIntro=> -[l' i] /=. destruct (decide (l' = l)) as [->|].
        + rewrite lookup_insert /=. by apply (alloc_heap_lookup _ _ _ _ 0).
        + by rewrite lookup_insert_ne //= alloc_heap_lookup_ne // Hτ.
      - iApply (big_sepM_insert with "[$Hτ Hll]"); first done.
        iExists _. iFrame "Hll".
        by rewrite -list_fmap_compose (list_fmap_ext _ id _ vs) ?list_fmap_id. }
    iApply (big_sepL_impl with "Hl"); iIntros "!>" (i v _) "Hl".
    rewrite mapsto_eq /mapsto_def. eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
430
431
432
433
434
435
436
437
438
439
  Qed.

  Lemma locking_heap_unlock cl v lv q σ :
    full_locking_heap σ - cl C[lv]{q} v ==
    full_locking_heap (<[cl:=(ULvl,v)]>σ)  cl C{q} v.
  Proof.
    iDestruct 1 as (τ Hτ) "[Hσ Hτ]".
    rewrite mapsto_eq /mapsto_def; iDestruct 1 as (lv' ?) "Hl".
    iDestruct (own_valid_2 with "Hσ Hl")
      as %[(lv''&?&Hσ)%heap_singleton_included _]%auth_valid_discrete_2.
440
    move: (Hσ); rewrite Hτ=> /bind_Some [lvvs [Hτl Hi]].
Robbert Krebbers's avatar
Robbert Krebbers committed
441
442
443
444
445
446
    iDestruct (big_sepM_delete with "Hτ") as "[H Hτ]"; first done.
    iDestruct "H" as (ll) "[Hll %]".
    iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
    { eapply auth_update, singleton_local_update, prod_local_update_1,
        prod_local_update_2, (local_update_unital_discrete _ _ ULvl ULvl);
        first by apply to_locking_heap_lookup_Some.
Dan Frumin's avatar
Dan Frumin committed
447
      intros h Hh. fold_leibniz. intros ->. split; eauto. }
Robbert Krebbers's avatar
Robbert Krebbers committed
448
    iModIntro. iSplitR "Hl"; last by eauto with iFrame.
449
450
451
452
453
454
455
456
457
    iExists (<[cl.1:=(<[cl.2:=(ULvl,v)]> lvvs)]>τ).
    rewrite to_locking_heap_insert. iFrame "Hσ". iSplit.
    { destruct cl as [l i]; iPureIntro=> -[l' i']; simpl in *.
      destruct (decide (l' = l)) as [->|?].
      { destruct (decide (i' = i)) as [->|?].
        - rewrite !lookup_insert /= list_lookup_insert //. by eapply lookup_lt_Some.
        - rewrite lookup_insert /= list_lookup_insert_ne //.
          rewrite lookup_insert_ne; last congruence. by rewrite Hτ Hτl. }
      rewrite !lookup_insert_ne; [|congruence..]. by rewrite Hτ. }
Robbert Krebbers's avatar
Robbert Krebbers committed
458
459
460
461
    rewrite -insert_delete.
    iApply (big_sepM_insert with "[$Hτ Hll]"); first by rewrite lookup_delete.
    iExists ll. iFrame.
    by rewrite list_fmap_insert /= list_insert_id ?list_lookup_fmap ?Hi.
Dan Frumin's avatar
Dan Frumin committed
462
463
  Qed.
End properties.