na_invariants.v 3.45 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 5
Import uPred.

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

8
Definition thread_id := gname.
9

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

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

16
  Definition na_own (tid : thread_id) (E : coPset) : iProp Σ :=
17
    own tid (CoPset E, ).
18

19
  Definition na_inv (tid : thread_id) (N : namespace) (P : iProp Σ) : iProp Σ :=
20
    ( i, i  N 
21
          inv N (P  own tid (, GSet {[i]})  na_own tid {[i]}))%I.
22 23
End defs.

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

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

30 31
  Global Instance na_own_timeless tid E : TimelessP (na_own tid E).
  Proof. rewrite /na_own; apply _. Qed.
32

33 34 35
  Global Instance na_inv_ne tid N n : Proper (dist n ==> dist n) (na_inv tid N).
  Proof. rewrite /na_inv. solve_proper. Qed.
  Global Instance na_inv_proper tid N : Proper (() ==> ()) (na_inv tid N).
36 37
  Proof. apply (ne_proper _). Qed.

38 39
  Global Instance na_inv_persistent tid N P : PersistentP (na_inv tid N P).
  Proof. rewrite /na_inv; apply _. Qed.
40

41
  Lemma na_alloc : (|==>  tid, na_own tid )%I.
42
  Proof. by apply own_alloc. Qed.
43

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

50 51
  Lemma na_own_union tid E1 E2 :
    E1  E2  na_own tid (E1  E2)  na_own tid E1  na_own tid E2.
52
  Proof.
53
    intros ?. by rewrite /na_own -own_op pair_op left_id coPset_disj_union.
54 55
  Qed.

56
  Lemma na_inv_alloc tid E N P :  P ={E}= na_inv tid N P.
57 58
  Proof.
    iIntros "HP".
59
    iMod (own_empty (prodUR coPset_disjUR (gset_disjUR positive)) tid) as "Hempty".
60
    iMod (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
61
    { apply prod_updateP'. apply cmra_updateP_id, (reflexivity (R:=eq)).
62 63
      apply (gset_disj_alloc_empty_updateP_strong' (λ i, i  N)).
      intros Ef. exists (coPpick ( N  coPset.of_gset Ef)).
64 65 66 67
      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. }
68
    simpl. iDestruct "Hm" as %(<- & i & -> & ?).
69
    rewrite /na_inv.
70
    iMod (inv_alloc N with "[-]"); last (iModIntro; iExists i; eauto).
71 72 73
    iNext. iLeft. by iFrame.
  Qed.

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