locking_heap.v 32.7 KB
Newer Older
1 2
From iris.algebra Require Import cmra auth gmap frac agree.
From iris.bi.lib Require Import fractional.
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.
6
Set Default Proof Using "Type".
7
Local Open Scope nat_scope.
8

9 10 11 12
Inductive lvl :=
  | LLvl : lvl
  | ULvl : lvl.
Canonical Structure lvlC := leibnizC lvl.
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
23
Arguments lvl_op !_ !_ /.
24 25 26
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
27 28 29 30 31
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
32
Proof.
33
  split.
Robbert Krebbers's avatar
Robbert Krebbers committed
34 35
  - intros [[] ->%leibniz_equiv]; by destruct lv1.
  - exists lv2. by destruct lv1, lv2.
Dan Frumin's avatar
Dan Frumin committed
36 37
Qed.

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

41
Lemma lvl_ra_mixin : RAMixin lvl.
Dan Frumin's avatar
Dan Frumin committed
42 43 44
Proof.
  apply ra_total_mixin; try by eauto.
  - solve_proper.
45 46 47 48 49
  - 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
50 51
Qed.

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

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

Dan Frumin's avatar
Dan Frumin committed
60 61 62 63
(** Here we use a Primitive Record to get an eta-rule for cloc
See: https://coq.inria.fr/refman/language/gallina-extensions.html#primitive-record-types
*)
Set Primitive Projections.
64
Record cloc := CLoc {
Robbert Krebbers's avatar
Robbert Krebbers committed
65
  cloc_base : loc;
66
  cloc_offset : Z
Dan Frumin's avatar
Dan Frumin committed
67
}.
68 69 70
Unset Primitive Projections.
Add Printing Constructor cloc.

Dan Frumin's avatar
Dan Frumin committed
71 72 73 74 75
Instance cloc_eq_dec : EqDecision cloc | 0.
Proof. solve_decision. Qed.
Instance cloc_countable : Countable cloc | 0.
Proof.
  apply inj_countable' with
Robbert Krebbers's avatar
Robbert Krebbers committed
76
      (f:=(λ x, (cloc_base x, cloc_offset x)))
77
      (g:=λ '(l,n), CLoc l n).
Dan Frumin's avatar
Dan Frumin committed
78 79 80
  reflexivity. (* This line wouldn't work if we were not using primitive projections *)
Qed.
Instance cloc_inhabited : Inhabited cloc | 0 :=
81 82
  populate (CLoc inhabitant inhabitant).

Dan Frumin's avatar
Dan Frumin committed
83
(* Auth (CLoc -> (Q * Level)) *)
84
Definition locking_heapUR : ucmraT :=
Robbert Krebbers's avatar
Robbert Krebbers committed
85
  gmapUR cloc (prodR (prodR fracR lvlUR) (agreeR valC)).
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
86
Definition heap_block_infoUR : ucmraT :=
87
  gmapUR loc (agreeR (prodC boolC natC)).
88 89 90 91

(** The CMRA we need. *)
Class locking_heapG (Σ : gFunctors) := LHeapG {
  lheap_inG :> inG Σ (authR locking_heapUR);
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
92 93 94 95 96 97 98
  lheap_block_info_inG :> inG Σ (authR heap_block_infoUR);
  lheap_name : gname;
  lheap_block_info_name : gname
}.
Class locking_heapPreG (Σ : gFunctors) := {
  lheap_preG_inG :> inG Σ (authR locking_heapUR);
  lheap_preG_block_info_inG :> inG Σ (authR heap_block_infoUR);
99 100 101
}.

Definition locking_heapΣ : gFunctors :=
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
102
  #[GFunctor (authR locking_heapUR); GFunctor (authR heap_block_infoUR)].
103 104 105 106 107 108 109 110

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
111
  Definition to_locking_heap (σ : gmap cloc (lvl * val)) : locking_heapUR :=
112
    fmap (λ '(lv,v), (1%Qp, lv, to_agree v)) σ.
113

Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
114
  Inductive heap_block :=
115 116 117 118
    (* true = alloc, false = local *)
    | ActiveBlock : bool  list (lvl * val)  heap_block
    | FreedBlock : bool  nat  heap_block.
  Definition heap_block_info (b : heap_block) : bool * nat :=
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
119
    match b with
120 121
    | ActiveBlock b lvvs => (b,length lvvs)
    | FreedBlock b n => (b,n)
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
122
    end.
123 124 125
  Global Instance maybe_active_block : Maybe2 ActiveBlock := λ b,
    match b with ActiveBlock k lvvs => Some (k,lvvs) | _ => None end.

Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
126
  Definition to_heap_block_info (τ : gmap loc heap_block) : heap_block_infoUR :=
127
   to_agree  heap_block_info <$> τ.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
128 129 130

  Definition heap_blocks_lookup (τ : gmap loc heap_block) (cl : cloc) : option (lvl * val) :=
    b  τ !! cloc_base cl;
131
    ''(_, lvvs)  maybe2 ActiveBlock b;
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
132 133
    lvvs !! Z.to_nat (cloc_offset cl).

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

138 139
  (** Pointer arithmetic *)
  Definition cloc_lt (p q : cloc) : bool :=
Robbert Krebbers's avatar
Robbert Krebbers committed
140
    bool_decide (cloc_base p = cloc_base q)
141 142
    && bool_decide (cloc_offset p < cloc_offset q)%Z.
  Definition cloc_plus (cl : cloc) (i : Z) : cloc :=
Robbert Krebbers's avatar
Robbert Krebbers committed
143
    CLoc (cloc_base cl) (i + cloc_offset cl).
144

Dan Frumin's avatar
Dan Frumin committed
145
  Definition cloc_to_val (cl : cloc) : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
146 147
    locked (SOMEV (#(cloc_base cl), #(cloc_offset cl)))%V.

148
  Definition cloc_of_val (v : val) : option cloc :=
Dan Frumin's avatar
Dan Frumin committed
149
    match v return option cloc with
Robbert Krebbers's avatar
Robbert Krebbers committed
150
    | SOMEV (LitV (LitLoc l), LitV (LitInt i))%V => Some (CLoc l i)
151 152
    | _ => None
    end.
Robbert Krebbers's avatar
Robbert Krebbers committed
153 154

  Definition full_locking_heap (σ : gmap cloc (lvl * val)) :=
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
155
    ( τ : gmap loc heap_block,
156 157
       map_Forall (λ cl _, 0  cloc_offset cl)%Z σ 
         cl, (0  cloc_offset cl)%Z 
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
158
          σ !! cl = heap_blocks_lookup τ cl  
Robbert Krebbers's avatar
Robbert Krebbers committed
159
      own lheap_name ( (to_locking_heap σ)) 
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
160 161
      own lheap_block_info_name ( (to_heap_block_info τ)) 
      [ map] lb  τ, match b with
162 163
                       | ActiveBlock k lvvs =>  lv,
                          l  SOMEV (#k,lv) 
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
164
                           is_list lv (snd <$> lvvs) 
165
                       | FreedBlock _ _ => l  NONEV
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
166
                       end)%I.
167

Robbert Krebbers's avatar
Robbert Krebbers committed
168 169 170
  Definition mapsto_def (cl : cloc) (lv : lvl) (q : frac) (v: val) : iProp Σ :=
    ( lv',
      lv  lv' 
171
       0  cloc_offset cl %Z 
Robbert Krebbers's avatar
Robbert Krebbers committed
172
      own lheap_name ( {[ cl := (q, lv', to_agree v) ]}))%I.
173 174 175
  Definition mapsto_aux : seal (@mapsto_def). by eexists. Qed.
  Definition mapsto := unseal mapsto_aux.
  Definition mapsto_eq : @mapsto = @mapsto_def := seal_eq mapsto_aux.
Robbert Krebbers's avatar
Robbert Krebbers committed
176

177
  Definition block_info_def (cl : cloc) (k : bool) (n : nat) : iProp Σ :=
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
178
    ( cloc_offset cl = 0    n  0  
179
     own lheap_block_info_name ( {[ cloc_base cl := to_agree (k,n) ]}))%I.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
180 181 182 183
  Definition block_info_aux : seal (@block_info_def). by eexists. Qed.
  Definition block_info := unseal block_info_aux.
  Definition block_info_eq : @block_info = @block_info_def := seal_eq block_info_aux.

Robbert Krebbers's avatar
Robbert Krebbers committed
184 185
  Definition mapsto_list (cl : cloc) (q : frac) (vs : list val) : iProp Σ :=
    ([ list] i  v  vs, mapsto (cloc_plus cl i) ULvl q v)%I.
186 187
End definitions.

Robbert Krebbers's avatar
Robbert Krebbers committed
188 189 190 191
Typeclasses Opaque mapsto_list.

Infix "+∗" := (cloc_plus) (at level 50) : stdpp_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
192 193 194 195 196 197 198 199 200
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.
201

202
Notation "cl ↦C{ q }∗ vs" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
203
  (mapsto_list cl q vs)%I
204 205
  (at level 20, q at level 50, format "cl  ↦C{ q }∗  vs") : bi_scope.
Notation "cl ↦C∗ vs" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
206
  (mapsto_list cl 1 vs)%I
207 208
  (at level 20, format "cl  ↦C∗  vs") : bi_scope.

Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
209
Lemma to_locking_heap_valid σ :  to_locking_heap σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
210
Proof. intros cl. rewrite lookup_fmap. by destruct (σ !! cl) as [[]|]. Qed.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
211 212
Lemma to_heap_block_info_valid τ :  to_heap_block_info τ.
Proof. intros l. rewrite lookup_fmap. by destruct (τ !! l) as [[]|]. Qed.
213

214 215
Lemma locking_heap_init `{locking_heapPreG Σ, !heapG Σ} :
  (|==>  _ : locking_heapG Σ, full_locking_heap )%I.
216
Proof.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
217
  iMod (own_alloc ( to_locking_heap )) as (γ1) "Hh1".
Hai Dang's avatar
Hai Dang committed
218
  { by apply auth_auth_valid. }
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
219
  iMod (own_alloc ( to_heap_block_info )) as (γ2) "Hh2".
Hai Dang's avatar
Hai Dang committed
220
  { by apply auth_auth_valid. }
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
221
  iModIntro. iExists (LHeapG Σ _ _ γ1 γ2), . iFrame; auto 10.
222 223 224
Qed.

Section properties.
Robbert Krebbers's avatar
Robbert Krebbers committed
225
  Context `{locking_heapG Σ, !heapG Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
226
  Implicit Type σ : gmap cloc (lvl * val).
227
  Implicit Type lv : lvl.
228
  Implicit Type l : loc.
Robbert Krebbers's avatar
Robbert Krebbers committed
229
  Implicit Type cl : cloc.
230

231 232 233 234
  Lemma mapsto_offset_non_neg cl lv q v :
    cl C[lv]{q} v -  (0  cloc_offset cl)%Z .
  Proof. rewrite mapsto_eq /mapsto_def. by iDestruct 1 as (lv1 ??) "_". Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
235 236
  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
237 238
  Proof.
    rewrite mapsto_eq /mapsto_def.
239
    iDestruct 1 as (lv1 ??) "Hl1". iDestruct 1 as (lv2 ? _) "Hl2".
Hai Dang's avatar
Hai Dang committed
240 241
    iDestruct (own_valid_2 with "Hl1 Hl2") as %Ho. iPureIntro.
    revert Ho. rewrite auth_frag_valid op_singleton singleton_valid. by intros [_ ?%agree_op_invL'].
Dan Frumin's avatar
Dan Frumin committed
242 243
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
244 245
  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
246 247
  Proof.
    rewrite mapsto_eq /mapsto_def.
248
    iDestruct 1 as (lv1 ??) "Hl1". iDestruct 1 as (lv2 ? _) "Hl2".
249
    iExists (lv1  lv2). iSplitR.
Robbert Krebbers's avatar
Robbert Krebbers committed
250 251
    { iPureIntro. by apply: cmra_mono. }
    iCombine "Hl1 Hl2" as "Hl". rewrite frac_op'. by iFrame.
Dan Frumin's avatar
Dan Frumin committed
252 253
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
254 255
  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).
256 257 258 259 260
  Proof.
    rewrite /FromSep. iIntros "[Hl1 Hl2]".
    iApply (mapsto_combine with "Hl1 Hl2").
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
261 262 263 264 265 266
  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.
267
      iDestruct 1 as (lv' ??) "Hl". rewrite -(lvl_idemp lv').
Robbert Krebbers's avatar
Robbert Krebbers committed
268 269 270 271 272 273 274 275
      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.

Robbert Krebbers's avatar
Robbert Krebbers committed
276 277 278
  Global Instance mapsto_list_timeless cl q vs : Timeless (cl C{q} vs).
  Proof. rewrite /mapsto_list; apply _. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
279 280 281 282 283 284 285 286 287 288
  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.

Robbert Krebbers's avatar
Robbert Krebbers committed
289
  Lemma cloc_plus_0 cl : cl + 0 = cl.
Dan Frumin's avatar
Dan Frumin committed
290
  Proof. reflexivity. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
291
  Lemma cloc_plus_plus cl i j : (cl + i) + j = cl + (i + j).
292
  Proof. by rewrite /cloc_plus /= Z.add_assoc (Z.add_comm i j). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308
  Global Instance cloc_plus_inj cl : Inj (=) (=) (cloc_plus cl).
  Proof. intros i j [=]; lia. Qed.

  Lemma mapsto_list_nil cl q : cl C{q} []  True.
  Proof. done. Qed.
  Lemma mapsto_list_singleton cl q v : cl C{q} [v]  cl C{q} v.
  Proof. by rewrite /mapsto_list big_sepL_singleton. Qed.
  Lemma mapsto_list_app cl q vs1 vs2 :
    cl C{q} (vs1 ++ vs2)  cl C{q} vs1  (cl + length vs1) C{q} vs2.
  Proof.
    rewrite /mapsto_list /= big_sepL_app.
    by setoid_rewrite cloc_plus_plus; setoid_rewrite Nat2Z.inj_add.
  Qed.
  Lemma mapsto_list_cons cl q v vs :
    cl C{q} (v :: vs)  cl C{q} v  (cl + 1) C{q} vs.
  Proof. by rewrite (mapsto_list_app _ _ [_]) mapsto_list_singleton. Qed.
309

310
  Global Instance block_info_persistent cl k n : Persistent (block_info cl k n).
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
311
  Proof. rewrite block_info_eq. apply _. Qed.
312
  Global Instance block_info_timeless cl k n : Timeless (block_info cl k n).
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
313 314
  Proof. rewrite block_info_eq. apply _. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
315
  Lemma cloc_to_val_eq : cloc_to_val = λ cl, SOMEV (#(cloc_base cl), #(cloc_offset cl))%V.
316
  Proof. rewrite /cloc_to_val. by unlock. Qed.
317
  Lemma cloc_of_to_val cl : cloc_of_val (cloc_to_val cl) = Some cl.
318
  Proof. destruct cl. by rewrite cloc_to_val_eq. Qed.
319
  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
320
  Proof.
321
    rewrite /cloc_of_val cloc_to_val_eq=> ?.
322
    destruct cl; repeat (case_match || simplify_option_eq); auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
323
  Qed.
324 325 326
  Global Instance cloc_to_val_inj : Inj (=) (=) cloc_to_val.
  Proof. intros cl1 cl2 Hcl. apply (inj Some). by rewrite -!cloc_of_to_val Hcl. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
327 328
  Lemma to_locking_heap_insert σ cl lv v :
    to_locking_heap (<[cl:=(lv,v)]> σ) = <[cl:=(1%Qp, lv, to_agree v)]>(to_locking_heap σ).
329 330
  Proof. by rewrite /to_locking_heap fmap_insert. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
331 332
  Lemma to_locking_heap_lookup_Some σ li lv v :
    σ !! li = Some (lv,v)  to_locking_heap σ !! li = Some (1%Qp, lv, to_agree v).
333
  Proof. rewrite /to_locking_heap lookup_fmap => -> //. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
334 335
  Lemma to_locking_heap_lookup_None σ li :
    σ !! li = None  to_locking_heap σ !! li = None.
336
  Proof. rewrite /to_locking_heap lookup_fmap => -> //. Qed.
337

Robbert Krebbers's avatar
Robbert Krebbers committed
338 339
  Lemma locked_locs_lock σ cl v :
    locked_locs (<[cl:=(LLvl,v)]>σ) = {[cl]}  locked_locs σ.
340
  Proof.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
341
    rewrite /locked_locs map_filter_insert; last done.
342 343 344
    apply dom_insert_L.
  Qed.

Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
345 346 347 348
  Lemma locked_locs_delete σ cl :
    locked_locs (delete cl σ) = locked_locs σ  {[cl]}.
  Proof. by rewrite /locked_locs map_filter_delete dom_delete_L. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
349 350 351
  Lemma locked_locs_unlock σ cl v :
    σ !! cl = Some (LLvl,v) 
    locked_locs (<[cl:=(ULvl,v)]>σ) = locked_locs σ  {[cl]}.
352 353
  Proof.
    intros Hl. rewrite /locked_locs -dom_delete_L. f_equal.
354 355
    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
356 357
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
358 359 360
  Lemma locked_locs_alloc_unlocked σ cl v :
    σ !! cl = None 
    locked_locs (<[cl:=(ULvl,v)]>σ) = locked_locs σ.
Dan Frumin's avatar
Dan Frumin committed
361 362
  Proof.
    intros Hl. rewrite /locked_locs. f_equal.
363 364
    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
365
  Qed.
366

Robbert Krebbers's avatar
Robbert Krebbers committed
367 368 369
  Lemma heap_singleton_included σ cl lv q v :
    {[cl := (q, lv, to_agree v)]}  to_locking_heap σ 
     lv', lv  lv'  σ !! cl = Some (lv', v).
370
  Proof.
371 372 373 374
    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''.
375 376
  Qed.

377 378 379
  Lemma block_info_singleton_included τ l k n :
    {[l := to_agree (k,n)]}  to_heap_block_info τ 
     b, τ !! l = Some b  heap_block_info b = (k,n).
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
380 381 382 383 384 385
  Proof.
    rewrite singleton_included=> -[mn].
    rewrite /to_heap_block_info lookup_fmap fmap_Some_equiv=> -[[b [-> ->]]] /=.
    move=> /Some_included_total /to_agree_included /leibniz_equiv_iff; eauto.
  Qed.

386 387
  Lemma full_locking_heap_unlocked_value σ cl v q :
    cl C{q} v - full_locking_heap σ - ⌜σ !! cl = Some (ULvl,v).
388 389
  Proof.
    rewrite mapsto_eq /mapsto_def /full_locking_heap.
390 391
    iDestruct 1 as ([] []%lvl_included _) "Hl".
    iDestruct 1 as (τ Hτ) "[Hfull Hmap]".
Robbert Krebbers's avatar
Robbert Krebbers committed
392
    iDestruct (own_valid_2 with "Hfull Hl")
Hai Dang's avatar
Hai Dang committed
393
      as %[[[] [[]%lvl_included Hl]]%heap_singleton_included _]%auth_both_valid; auto.
394 395
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
396
  Lemma full_locking_heap_unlocked σ cl v q :
397
    cl C{q} v - full_locking_heap σ - cl  locked_locs σ⌝.
398
  Proof.
399 400 401 402 403 404
    iIntros "Hcl Hσ".
    iDestruct (full_locking_heap_unlocked_value with "Hcl Hσ") as %Hcl.
    iPureIntro.
    rewrite /locked_locs.
    apply not_elem_of_dom, map_filter_lookup_None.
    right. intros [??]. by rewrite Hcl=>[= <- <-].
Dan Frumin's avatar
Dan Frumin committed
405 406
  Qed.

407
  Lemma full_locking_heap_locked_present σ cl v q :
Robbert Krebbers's avatar
Robbert Krebbers committed
408
    cl C[LLvl]{q} v - full_locking_heap σ - is_Some (σ !! cl).
Dan Frumin's avatar
Dan Frumin committed
409 410
  Proof.
    rewrite mapsto_eq /mapsto_def /full_locking_heap.
411
    iDestruct 1 as (lv _ _) "Hl". iDestruct 1 as (τ Hτ) "[Hfull Hmap]".
Robbert Krebbers's avatar
Robbert Krebbers committed
412
    iDestruct (own_valid_2 with "Hfull Hl")
Hai Dang's avatar
Hai Dang committed
413
      as %[[y [? ?]]%heap_singleton_included _]%auth_both_valid; eauto.
414 415
  Qed.

416
  Lemma full_locking_heap_load_upd cl lv q v σ :
417
    full_locking_heap σ - cl C[lv]{q} v ==  (k : bool) ll vs,
418 419
       is_list ll vs  
       vs !! Z.to_nat (cloc_offset cl) = Some v  
420 421
      cloc_base cl  SOMEV (#k,ll) 
      (cloc_base cl  SOMEV (#k,ll) - full_locking_heap σ  cl C[lv]{q} v).
422
  Proof.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
423
    iDestruct 1 as (τ [Hnat Hτ]) "(Hσ & Hτ & H)".
424
    rewrite mapsto_eq /mapsto_def; iDestruct 1 as (lv' ??) "Hl".
Robbert Krebbers's avatar
Robbert Krebbers committed
425
    iDestruct (own_valid_2 with "Hσ Hl")
Hai Dang's avatar
Hai Dang committed
426
      as %[(lv''&?&Hσ)%heap_singleton_included _]%auth_both_valid.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
427
    move: (Hσ). rewrite Hτ; last by eauto.
428
    intros ([k lvvs|?]&?&Hi)%bind_Some; simplify_eq/=.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
429
    iDestruct (big_sepM_lookup_acc with "H") as "[H Hclose]"; first done.
430
    iDestruct "H" as (ll) "[Hll %]". iModIntro. iExists k, ll, lvvs.*2.
431
    repeat iSplit; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
432
    { iPureIntro. by rewrite list_lookup_fmap Hi. }
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
433 434
    iIntros "{$Hll} Hll". iDestruct ("Hclose" with "[Hll]") as "H"; eauto.
    iSplitL "Hσ Hτ H"; first (iExists τ; by eauto with iFrame).
Robbert Krebbers's avatar
Robbert Krebbers committed
435
    iExists lv'. auto.
Dan Frumin's avatar
Dan Frumin committed
436 437
  Qed.

438
  Lemma full_locking_heap_store_upd cl lv v σ :
439
    full_locking_heap σ - cl C[lv] v ==  (k : bool) ll vs,
440 441
       is_list ll vs  
       vs !! Z.to_nat (cloc_offset cl) = Some v  
442
      cloc_base cl  SOMEV (#k, ll) 
Dan Frumin's avatar
Dan Frumin committed
443
      ( ll' lv' v',
444
         is_list ll' (<[Z.to_nat (cloc_offset cl):=v']>vs)  -
445
        cloc_base cl  SOMEV (#k, ll') ==
Robbert Krebbers's avatar
Robbert Krebbers committed
446
        full_locking_heap (<[cl:=(lv',v')]>σ)  cl C[lv'] v').
Dan Frumin's avatar
Dan Frumin committed
447
  Proof.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
448
    iDestruct 1 as (τ [Hnat Hτ]) "(Hσ & Hτ & H)".
449
    rewrite mapsto_eq /mapsto_def; iDestruct 1 as (lv' ??) "Hl".
Robbert Krebbers's avatar
Robbert Krebbers committed
450
    iDestruct (own_valid_2 with "Hσ Hl")
Hai Dang's avatar
Hai Dang committed
451
      as %[(lv''&?&Hσ)%heap_singleton_included _]%auth_both_valid.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
452
    move: (Hσ). rewrite Hτ; last by eauto.
453
    intros ([k lvvs|?]&Hτl&Hi)%bind_Some; simplify_eq/=.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
454
    iDestruct (big_sepM_delete with "H") as "[Hcl H]"; first done.
455
    iDestruct "Hcl" as (ll) "[Hll %]". iModIntro. iExists k, ll, lvvs.*2.
456
    repeat iSplit; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
457 458 459 460 461 462
    { 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. }
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
463
    iModIntro. iSplitL "Hσ Hτ H Hll"; last auto.
464 465
    iExists (<[cloc_base cl:=
      ActiveBlock k (<[Z.to_nat (cloc_offset cl):=(lv''',v')]> lvvs)]>τ).
466
    rewrite to_locking_heap_insert. iFrame "Hσ". iSplit.
467 468 469
    { iPureIntro. split; [by apply map_Forall_insert_2; eauto|].
      destruct cl as [l i]=> -[l' i'] ?; simpl in *.
      assert (0  i)%Z by (by eapply (Hnat (CLoc l i))).
470 471
      destruct (decide (l' = l)) as [->|?].
      { destruct (decide (i' = i)) as [->|?].
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
472 473 474
        - rewrite /heap_blocks_lookup /= !lookup_insert /= list_lookup_insert //.
          by eapply lookup_lt_Some.
        - rewrite /heap_blocks_lookup lookup_insert /=.
475
          rewrite list_lookup_insert_ne ?Z2Nat.inj_iff //=.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
476 477 478 479 480 481 482
          rewrite lookup_insert_ne; last congruence.
          by rewrite Hτ //= /heap_blocks_lookup /= Hτl. }
      rewrite /heap_blocks_lookup /= !lookup_insert_ne; [|congruence..].
      by rewrite Hτ. }
    iSplitL "Hτ".
    { rewrite /to_heap_block_info fmap_insert insert_id //.
      by rewrite lookup_fmap Hτl /= insert_length. }
Robbert Krebbers's avatar
Robbert Krebbers committed
483
    rewrite -insert_delete.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
484
    iApply (big_sepM_insert with "[$H Hll]"); first by rewrite lookup_delete.
485
    iExists ll'. iFrame. rewrite list_fmap_insert /=. auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
486 487
  Qed.

488 489
  Definition alloc_heap (σ : gmap cloc (lvl * val)) (l : loc) :
      list val  nat  gmap cloc (lvl * val) :=
490
    foldr (λ v go (i : nat), <[CLoc l i:=(ULvl,v)]> (go (S i))) (λ _, σ).
491 492

  Lemma alloc_heap_None σ l vs j1 j2 :
493 494
    ( i, σ !! CLoc l i = None) 
    j2 < j1  alloc_heap σ l vs j1 !! (CLoc l j2) = None.
495 496 497 498 499 500 501
  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.

502 503 504
  Lemma alloc_heap_lookup σ l vs (i j : nat) :
    ( i, σ !! CLoc l i = None) 
    alloc_heap σ l vs j !! CLoc l (j + i) = ((ULvl,) <$> vs) !! i.
505 506 507 508
  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.
509 510 511
    { by rewrite Z.add_0_r lookup_insert. }
    rewrite Nat2Z.inj_succ Z.add_succ_r -Z.add_succ_l -Nat2Z.inj_succ.
    rewrite lookup_insert_ne; last (intros [=]; lia).
512 513 514 515 516
    apply (IH i (S j)).
  Qed.

  Lemma alloc_heap_lookup_ne σ l l' vs i j :
    l  l' 
517
    alloc_heap σ l vs j !! CLoc l' i = σ !! CLoc l' i.
518 519 520 521 522 523
  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 :
524
    ( i, σ !! CLoc l i = None) 
525 526 527 528 529 530
    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.

531
  Lemma full_locking_heap_alloc_upd l (k : bool) ll vs σ :
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
532
    is_list ll vs  vs  [] 
533
    full_locking_heap σ - l  SOMEV (#k,ll) ==
534
      i, σ !! CLoc l i = None  
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
535
    full_locking_heap (alloc_heap σ l vs O) 
536
    block_info (CLoc l 0) k (length vs)  CLoc l 0 C vs.
Robbert Krebbers's avatar
Robbert Krebbers committed
537
  Proof.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
538
    intros Hll Hnil. iDestruct 1 as (τ [Hnat Hτ]) "(Hσ & Hτ &H)". iIntros "Hll".
539
    iAssert  τ !! l = None %I as %Hτi.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
540 541 542 543 544 545
    { rewrite eq_None_not_Some. iIntros ([b ?]).
      iDestruct (big_sepM_lookup with "H") as "H"; first done.
      destruct b as [lvv|n].
      - iDestruct "H" as (lv) "[Hll' _]".
        by iDestruct (mapsto_valid_2 with "Hll Hll'") as %[].
      - by iDestruct (mapsto_valid_2 with "Hll H") as %[]. }
546 547
    iAssert   i, σ !! CLoc l i = None %I as %Hσi.
    { iIntros (i) "!%". apply eq_None_not_Some=> -[[lv v] Hi].
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
548 549
      move: (Hi). rewrite Hτ; last by eauto.
      by rewrite /heap_blocks_lookup /= Hτi. }
550 551
    iAssert (|==> own lheap_name ( to_locking_heap (alloc_heap σ l vs 0)) 
      [ list] iv  vs, own lheap_name ( {[ CLoc l (i+0) := (1%Qp, ULvl,to_agree v) ]}))%I
552
      with "[Hσ]" as ">[Hσ Hl]".
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
553
    { clear Hll Hnil. change 0%Z with (Z.of_nat 0). generalize 0=> j.
554 555 556 557
      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,
558
          (alloc_singleton_local_update _ (CLoc l j)
Dan Frumin's avatar
Dan Frumin committed
559
                                        (1%Qp, ULvl, to_agree v)); try done.
560
        apply to_locking_heap_lookup_None. rewrite alloc_heap_None //. lia. }
Dan Frumin's avatar
Dan Frumin committed
561 562
      iModIntro.
      rewrite -to_locking_heap_insert /=. iFrame "Hσ Hl".
563
      iApply (big_sepL_impl with "Hls"); iIntros "!>" (k' w _) "?".
564
      by rewrite Nat2Z.inj_succ Z.add_succ_r -Z.add_succ_l -Nat2Z.inj_succ. }
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
565 566
    iMod (own_update with "Hτ") as "[Hτ Hinfo]".
    { apply auth_update_alloc,
567
        (alloc_singleton_local_update _ l (to_agree (k, length vs)))=> //.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
568 569
      by rewrite /to_heap_block_info lookup_fmap Hτi. }
    iModIntro. iSplit; first done. iSplitL "Hσ H Hτ Hll".
570
    { iExists (<[l:=ActiveBlock k ((ULvl,) <$> vs)]> τ). iFrame "Hσ". iSplit.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
571
      { iPureIntro. split.
572 573 574
        { clear -Hnat. generalize 0. induction vs as [|v vs IH]=> j //=.
          apply map_Forall_insert_2; simpl; eauto with lia. }
        move=> -[l' i] /= ? . destruct (decide (l' = l)) as [->|].
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
575 576 577 578 579 580 581 582 583 584 585
        - rewrite /heap_blocks_lookup /= lookup_insert /=.
          rewrite -{1}(Z2Nat.id i) //. by apply (alloc_heap_lookup _ _ _ _ 0).
        - rewrite /heap_blocks_lookup /= lookup_insert_ne //=.
          by rewrite alloc_heap_lookup_ne // Hτ. }
      iSplitL "Hτ".
      { by rewrite /to_heap_block_info /= !fmap_insert /= fmap_length. }
      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. }
    iSplitL "Hinfo".
    { rewrite block_info_eq /block_info_def. eauto 10 using nil_length_inv. }
Robbert Krebbers's avatar
Robbert Krebbers committed
586
    rewrite /mapsto_list.
587
    iApply (big_sepL_impl with "Hl"); iIntros "!>" (i v _) "Hl".
588
    rewrite mapsto_eq /mapsto_def /=. eauto 10 with lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
589 590
  Qed.

Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631
  Fixpoint free_heap (σ : gmap cloc (lvl * val)) (l : loc)
      (n : nat) : gmap cloc (lvl * val) :=
    match n with
    | 0 => σ
    | S n => delete (CLoc l n) (free_heap σ l n)
    end.

  Lemma locked_locs_free_heap σ cl l (n : nat) :
    cl  locked_locs σ 
    ¬(cloc_base cl = l  (0  cloc_offset cl < n)%Z) 
    cl  locked_locs (free_heap σ l n).
  Proof.
    induction n as [|n IH]; simpl; intros; auto.
    rewrite locked_locs_delete. set_solver by eauto with lia.
  Qed.

  Lemma free_heap_lookup σ l (n : nat) cl :
    cloc_base cl = l  (0  cloc_offset cl < n)%Z 
    free_heap σ l n !! cl = None.
  Proof.
    intros. induction n as [|n IH]; simpl; intros; auto with lia.
    destruct (decide (cloc_offset cl = n)).
    - destruct cl as [l' j]; simplify_eq/=. by rewrite lookup_delete.
    - rewrite lookup_delete_ne; last (destruct cl; naive_solver lia). eauto with lia.
  Qed.

  Lemma free_heap_lookup_ge σ l (n : nat) cl :
    cloc_base cl = l  (n  cloc_offset cl)%Z 
    free_heap σ l n !! cl = σ !! cl.
  Proof.
    intros. induction n as [|n IH]; simpl; intros; auto with lia.
    rewrite lookup_delete_ne; last (destruct cl; naive_solver lia). eauto with lia.
  Qed.

  Lemma free_heap_lookup_ne σ l n cl :
    cloc_base cl  l  free_heap σ l n !! cl = σ !! cl.
  Proof.
    intros. induction n as [|n IH]=> //=.
    by rewrite lookup_delete_ne; last (destruct cl; naive_solver).
  Qed.

632
  Lemma full_locking_heap_free_upd cl k vs σ :
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
633
    full_locking_heap σ -
634
    block_info cl k (length vs) -
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
635 636 637
    cl C vs ==  ll,
       cloc_offset cl = 0  
       is_list ll vs  
638
      cloc_base cl  SOMEV (#k, ll) 
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
639 640 641 642 643 644 645
      (cloc_base cl  NONEV -
        full_locking_heap (free_heap σ (cloc_base cl) (length vs))).
  Proof.
    iDestruct 1 as (τ [Hnat Hτ]) "(Hσ & Hτ &H)".
    rewrite block_info_eq /block_info_def; iIntros "(Hoff & % & Hinfo) Hcl".
    iDestruct "Hoff" as %Hoff.
    iDestruct (own_valid_2 with "Hτ Hinfo")
Hai Dang's avatar
Hai Dang committed
646
      as %[(b&Hb&?)%block_info_singleton_included _]%auth_both_valid.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
647
    iDestruct (big_sepM_delete with "H") as "[Hb H]"; first done.
648
    destruct b as [k' lvvs|k' n]; simplify_eq/=; last first.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
649 650 651 652
    { destruct vs as [|v vs]; simplify_eq/=.
      rewrite /mapsto_list mapsto_eq /mapsto_def; iDestruct "Hcl" as "[Hcl _]".
      iDestruct "Hcl" as (lv' _ _) "Hcl". rewrite cloc_plus_0.
      iDestruct (own_valid_2 with "Hσ Hcl")
Hai Dang's avatar
Hai Dang committed
653
        as %[(lv''&_&Hcl)%heap_singleton_included ?]%auth_both_valid.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
654 655 656 657 658 659 660 661
      contradict Hcl. rewrite Hτ ?Hoff //. by rewrite /heap_blocks_lookup Hb. }
    iDestruct "Hb" as (ll) "[Hll %]".
    iAssert  vs = lvvs.*2 %I as %->.
    { iApply bi.pure_mono; [apply list_eq_same_length; by rewrite ?fmap_length|].
      iIntros (i v1 v2 _ ? Hi). rewrite /mapsto_list mapsto_eq /mapsto_def.
      iDestruct (big_sepL_lookup with "Hcl") as "Hcl"; first done.
      iDestruct "Hcl" as (lv' _ _) "Hcl".
      iDestruct (own_valid_2 with "Hσ Hcl")
Hai Dang's avatar
Hai Dang committed
662
        as %[(lv''&_&Hcl)%heap_singleton_included ?]%auth_both_valid.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678
      iPureIntro; move: Hcl.
      rewrite Hτ /heap_blocks_lookup /cloc_plus /= ?Hoff; last lia.
      rewrite Hb /= Z.add_0_r Nat2Z.id.
      move: Hi. by rewrite list_lookup_fmap fmap_Some=> -[[??] [-> ->]] []. }
    iAssert (own lheap_name ( to_locking_heap
      (free_heap σ (cloc_base cl) (length lvvs.*2))))%I with "[> Hcl Hσ]" as "Hσ".
    { generalize (lvvs.*2)=> vs.
      iInduction vs as [|v vs] "IH" using rev_ind; simpl; auto.
      rewrite mapsto_list_app mapsto_list_singleton mapsto_eq /mapsto_def.
      iDestruct "Hcl" as "[Hcl Hcl']"; iDestruct "Hcl'" as (lv' _ _) "Hcl'".
      iMod ("IH" with "Hcl Hσ") as "Hσ". iApply (own_update_2 with "Hσ Hcl'").
      rewrite /cloc_plus Hoff Z.add_0_r.
      rewrite app_length Nat.add_comm /= /to_locking_heap fmap_delete.
      apply auth_update_dealloc, delete_singleton_local_update, _. }
    rewrite fmap_length.
    iModIntro. iExists _. do 2 (iSplit; first done). iIntros "{$Hll} Hll".
679
    iExists (<[cloc_base cl:=FreedBlock k (length lvvs.*2)]> τ). iSplit.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698
    { iPureIntro; split.
      { generalize (length lvvs); intros n.
        induction n; simpl; eauto. by apply map_Forall_delete. }
      intros cl' ?. destruct (decide (cloc_base cl = cloc_base cl')) as [Hcl|].
      - rewrite /heap_blocks_lookup Hcl lookup_insert /=.
        destruct (Z_lt_le_dec (cloc_offset cl') (length lvvs)%Z).
        + by rewrite free_heap_lookup.
        + rewrite free_heap_lookup_ge // Hτ //.
          rewrite /heap_blocks_lookup -Hcl Hb /=.
          apply lookup_ge_None_2, Nat2Z.inj_le. by rewrite Z2Nat.id.
      - rewrite free_heap_lookup_ne // Hτ //.
        rewrite /heap_blocks_lookup lookup_insert_ne //. }
    iFrame "Hσ". iSplitL "Hτ".
    { rewrite /to_heap_block_info fmap_insert insert_id //.
      by rewrite lookup_fmap Hb /= fmap_length. }
    rewrite -insert_delete.
    iApply big_sepM_insert; first by rewrite lookup_delete. iFrame.
  Qed.

699
  Lemma full_locking_heap_unlock cl v lv q σ :
Robbert Krebbers's avatar
Robbert Krebbers committed
700 701 702
    full_locking_heap σ - cl C[lv]{q} v ==
    full_locking_heap (<[cl:=(ULvl,v)]>σ)  cl C{q} v.
  Proof.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
703
    iDestruct 1 as (τ [Hnat Hτ]) "(Hσ & Hτ &H)".
704
    rewrite mapsto_eq /mapsto_def; iDestruct 1 as (lv' ??) "Hl".
Robbert Krebbers's avatar
Robbert Krebbers committed
705
    iDestruct (own_valid_2 with "Hσ Hl")
Hai Dang's avatar
Hai Dang committed
706
      as %[(lv''&?&Hσ)%heap_singleton_included _]%auth_both_valid.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
707
    move: (Hσ); rewrite Hτ; last by eauto.
708
    intros ([k lvvs|?]&Hτl&Hi)%bind_Some; simplify_eq/=.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
709 710
    iDestruct (big_sepM_delete with "H") as "[Hcl H]"; first done.
    iDestruct "Hcl" as (ll) "[Hll %]".
Robbert Krebbers's avatar
Robbert Krebbers committed
711 712 713 714
    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
715
      intros h Hh. fold_leibniz. intros ->. split; eauto. }
Robbert Krebbers's avatar
Robbert Krebbers committed
716
    iModIntro. iSplitR "Hl"; last by eauto with iFrame.
717 718
    iExists (<[cloc_base cl:=
      ActiveBlock k (<[Z.to_nat (cloc_offset cl):=(ULvl,v)]> lvvs)]>τ).
719
    rewrite to_locking_heap_insert. iFrame "Hσ". iSplit.
720 721 722
    { iPureIntro. split; [by apply map_Forall_insert_2; eauto|].
      destruct cl as [l i]=> -[l' i'] ?; simpl in *.
      assert (0  i)%Z by (by eapply (Hnat (CLoc l i))).
723 724
      destruct (decide (l' = l)) as [->|?].
      { destruct (decide (i' = i)) as [->|?].
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
725 726 727
        - rewrite /heap_blocks_lookup /= !lookup_insert /= list_lookup_insert //.
          by eapply lookup_lt_Some.
        - rewrite /heap_blocks_lookup /= lookup_insert /=.
728
          rewrite list_lookup_insert_ne ?Z2Nat.inj_iff //=.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
729 730 731 732 733 734 735
          rewrite lookup_insert_ne; last congruence.
          by rewrite Hτ // /heap_blocks_lookup /= Hτl. }
      rewrite /heap_blocks_lookup /= !lookup_insert_ne; [|congruence..].
      by rewrite Hτ. }
    iSplitL "Hτ".
    { rewrite /to_heap_block_info /= fmap_insert insert_id //.
      by rewrite lookup_fmap Hτl /= insert_length. }
Robbert Krebbers's avatar
Robbert Krebbers committed
736
    rewrite -insert_delete.
Robbert Krebbers's avatar
Free!  
Robbert Krebbers committed
737
    iApply (big_sepM_insert with "[$H Hll]"); first by rewrite lookup_delete.
Robbert Krebbers's avatar
Robbert Krebbers committed
738 739
    iExists ll. iFrame.
    by rewrite list_fmap_insert /= list_insert_id ?list_lookup_fmap ?Hi.
740 741
  Qed.
End properties.
Robbert Krebbers's avatar
Robbert Krebbers committed
742 743 744 745 746 747

Section proofmode.
  Context `{locking_heapG Σ, !heapG Σ}.

  Global Instance into_pure_mapsto_nil cl q : IntoPure (cl C{q} []) True.
  Proof. done. Qed.
748 749
  Global Instance from_pure_mapsto_nil cl q : FromPure false (cl C{q} []) True | 100.
  Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779

  Global Instance into_sep_mapsto_list_cons cl q vs v vs' :
    IsCons vs v vs' 
    IntoSep (cl C{q} vs) (cl C{q} v) ((cl + 1) C{q} vs').
  Proof. rewrite /IsCons=> ->. by rewrite /IntoSep mapsto_list_cons. Qed.
  Global Instance into_sep_mapsto_list_app cl q vs vs1 vs2 :
    IsApp vs vs1 vs2 
    IntoSep (cl C{q} vs) (cl C{q} vs1) ((cl + length vs1) C{q} vs2).
  Proof. rewrite /IsApp=> ->. by rewrite /IntoSep mapsto_list_app. Qed.

  Global Instance from_sep_mapsto_list_cons cl q vs v vs' :
    IsCons vs v vs' 
    FromSep (cl C{q} vs) (cl C{q} v) ((cl + 1) C{q} vs').
  Proof. rewrite /IsCons=> ->. by rewrite /FromSep mapsto_list_cons. Qed.
  Global Instance from_sep_mapsto_list_app cl q vs vs1 vs2 :
    IsApp vs vs1 vs2 
    FromSep (cl C{q} vs) (cl C{q} vs1) ((cl + length vs1) C{q} vs2).
  Proof. rewrite /IsApp=> ->. by rewrite /FromSep mapsto_list_app. Qed.

  Global Instance frame_big_sepL_cons p R Q cl q vs v vs' :
    IsCons vs v vs' 
    Frame p R (cl C{q} v  (cl + 1) C{q} vs') Q 
    Frame p R (cl C{q} vs) Q.
  Proof. rewrite /IsCons=>->. by rewrite /Frame mapsto_list_cons. Qed.
  Global Instance frame_big_sepL_app p R Q cl q vs vs1 vs2 :
    IsApp vs vs1 vs2 
    Frame p R (cl C{q} vs1  (cl + length vs1) C{q} vs2) Q 
    Frame p R (cl C{q} vs) Q.
  Proof. rewrite /IsApp=>->. by rewrite /Frame mapsto_list_app. Qed.
End proofmode.