na_invariants.v 3.75 KB
Newer Older
1
From iris.base_logic.lib Require Export invariants.
2
From iris.algebra Require Export gmap gset coPset.
3
From iris.proofmode Require Import tactics.
4
Set Default Proof Using "Type*".
5 6
Import uPred.

7 8
(* Non-atomic ("thread-local") invariants. *)

Ralf Jung's avatar
Ralf Jung committed
9
Definition na_inv_pool_name := gname.
10

11
Class na_invG Σ :=
12
  tl_inG :> inG Σ (prodR coPset_disjR (gset_disjR positive)).
13 14

Section defs.
15
  Context `{invG Σ, na_invG Σ}.
16

Ralf Jung's avatar
Ralf Jung committed
17 18
  Definition na_own (p : na_inv_pool_name) (E : coPset) : iProp Σ :=
    own p (CoPset E, ).
19

Ralf Jung's avatar
Ralf Jung committed
20
  Definition na_inv (p : na_inv_pool_name) (N : namespace) (P : iProp Σ) : iProp Σ :=
21
    ( i, i  N 
Ralf Jung's avatar
Ralf Jung committed
22
          inv N (P  own p (, GSet {[i]})  na_own p {[i]}))%I.
23 24
End defs.

25 26
Instance: Params (@na_inv) 3.
Typeclasses Opaque na_own na_inv.
27 28

Section proofs.
29
  Context `{invG Σ, na_invG Σ}.
30

Ralf Jung's avatar
Ralf Jung committed
31
  Global Instance na_own_timeless p E : TimelessP (na_own p E).
32
  Proof. rewrite /na_own; apply _. Qed.
33

Ralf Jung's avatar
Ralf Jung committed
34
  Global Instance na_inv_ne p N n : Proper (dist n ==> dist n) (na_inv p N).
35
  Proof. rewrite /na_inv. solve_proper. Qed.
Ralf Jung's avatar
Ralf Jung committed
36
  Global Instance na_inv_proper p N : Proper (() ==> ()) (na_inv p N).
37 38
  Proof. apply (ne_proper _). Qed.

Ralf Jung's avatar
Ralf Jung committed
39
  Global Instance na_inv_persistent p N P : PersistentP (na_inv p N P).
40
  Proof. rewrite /na_inv; apply _. Qed.
41

Ralf Jung's avatar
Ralf Jung committed
42
  Lemma na_alloc : (|==>  p, na_own p )%I.
43
  Proof. by apply own_alloc. Qed.
44

Ralf Jung's avatar
Ralf Jung committed
45
  Lemma na_own_disjoint p E1 E2 : na_own p E1 - na_own p E2 - E1  E2.
46
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
47
    apply wand_intro_r.
48
    rewrite /na_own -own_op own_valid -coPset_disj_valid_op. by iIntros ([? _]).
49 50
  Qed.

Ralf Jung's avatar
Ralf Jung committed
51 52
  Lemma na_own_union p E1 E2 :
    E1  E2  na_own p (E1  E2)  na_own p E1  na_own p E2.
53
  Proof.
54
    intros ?. by rewrite /na_own -own_op pair_op left_id coPset_disj_union.
55 56
  Qed.

Ralf Jung's avatar
Ralf Jung committed
57 58 59 60 61 62 63
  Lemma na_own_acc E2 E1 tid :
    E2  E1  na_own tid E1 - na_own tid E2  (na_own tid E2 - na_own tid E1).
  Proof.
    intros HF. assert (E1 = E2  (E1  E2)) as -> by exact: union_difference_L.
    rewrite na_own_union; last by set_solver+. iIntros "[$ $]". auto.
  Qed.

Ralf Jung's avatar
Ralf Jung committed
64
  Lemma na_inv_alloc p E N P :  P ={E}= na_inv p N P.
65 66
  Proof.
    iIntros "HP".
Ralf Jung's avatar
Ralf Jung committed
67
    iMod (own_empty (prodUR coPset_disjUR (gset_disjUR positive)) p) as "Hempty".
68
    iMod (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
69
    { apply prod_updateP'. apply cmra_updateP_id, (reflexivity (R:=eq)).
70 71
      apply (gset_disj_alloc_empty_updateP_strong' (λ i, i  N)).
      intros Ef. exists (coPpick ( N  coPset.of_gset Ef)).
72 73 74 75
      rewrite -coPset.elem_of_of_gset comm -elem_of_difference.
      apply coPpick_elem_of=> Hfin.
      eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
      apply of_gset_finite. }
76
    simpl. iDestruct "Hm" as %(<- & i & -> & ?).
77
    rewrite /na_inv.
78
    iMod (inv_alloc N with "[-]"); last (iModIntro; iExists i; eauto).
79 80 81
    iNext. iLeft. by iFrame.
  Qed.

Ralf Jung's avatar
Ralf Jung committed
82
  Lemma na_inv_open p E F N P :
83
    N  E  N  F 
Ralf Jung's avatar
Ralf Jung committed
84 85
    na_inv p N P - na_own p F ={E}=  P  na_own p (F∖↑N) 
                       ( P  na_own p (F∖↑N) ={E}= na_own p F).
86
  Proof.
87
    rewrite /na_inv. iIntros (??) "#Htlinv Htoks".
88
    iDestruct "Htlinv" as (i) "[% Hinv]".
Ralf Jung's avatar
Ralf Jung committed
89
    rewrite [F as X in na_own p X](union_difference_L (N) F) //.
90
    rewrite [X in (X  _)](union_difference_L {[i]} (N)) ?na_own_union; [|set_solver..].
Robbert Krebbers's avatar
Robbert Krebbers committed
91
    iDestruct "Htoks" as "[[Htoki $] $]".
92
    iInv N as "[[$ >Hdis]|>Htoki2]" "Hclose".
93 94
    - iMod ("Hclose" with "[Htoki]") as "_"; first auto.
      iIntros "!> [HP $]".
95
      iInv N as "[[_ >Hdis2]|>Hitok]" "Hclose".
96
      + iDestruct (own_valid_2 with "Hdis Hdis2") as %[_ Hval%gset_disj_valid_op].
Robbert Krebbers's avatar
Tweak.  
Robbert Krebbers committed
97
        set_solver.
98
      + iFrame. iApply "Hclose". iNext. iLeft. by iFrame.
99
    - iDestruct (na_own_disjoint with "Htoki Htoki2") as %?. set_solver.
100
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
101
End proofs.