na_invariants.v 4.78 KB
Newer Older
1
From iris.proofmode Require Import tactics.
2 3
From iris.algebra Require Import gset coPset.
From iris.base_logic.lib Require Export invariants.
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 13 14 15 16
  na_inv_inG :> inG Σ (prodR coPset_disjR (gset_disjR positive)).
Definition na_invΣ : gFunctors :=
  #[ GFunctor (constRF (prodR coPset_disjR (gset_disjR positive))) ].
Instance subG_na_invG {Σ} : subG na_invΣ Σ  na_invG Σ.
Proof. solve_inG. Qed.
17 18

Section defs.
19
  Context `{!invG Σ, !na_invG Σ}.
20

Ralf Jung's avatar
Ralf Jung committed
21
  Definition na_own (p : na_inv_pool_name) (E : coPset) : iProp Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
22
    own p (CoPset E, GSet ).
23

Ralf Jung's avatar
Ralf Jung committed
24
  Definition na_inv (p : na_inv_pool_name) (N : namespace) (P : iProp Σ) : iProp Σ :=
25
    ( i, i  (N:coPset) 
Robbert Krebbers's avatar
Robbert Krebbers committed
26
          inv N (P  own p (CoPset , GSet {[i]})  na_own p {[i]}))%I.
27 28
End defs.

29
Instance: Params (@na_inv) 3 := {}.
30
Typeclasses Opaque na_own na_inv.
31 32

Section proofs.
33
  Context `{!invG Σ, !na_invG Σ}.
34

35
  Global Instance na_own_timeless p E : Timeless (na_own p E).
36
  Proof. rewrite /na_own; apply _. Qed.
37

38
  Global Instance na_inv_ne p N : NonExpansive (na_inv p N).
39
  Proof. rewrite /na_inv. solve_proper. Qed.
Ralf Jung's avatar
Ralf Jung committed
40
  Global Instance na_inv_proper p N : Proper (() ==> ()) (na_inv p N).
41 42
  Proof. apply (ne_proper _). Qed.

43
  Global Instance na_inv_persistent p N P : Persistent (na_inv p N P).
44
  Proof. rewrite /na_inv; apply _. Qed.
45

46 47 48 49
  Lemma na_inv_iff p N P Q :   (P  Q) - na_inv p N P - na_inv p N Q.
  Proof.
    iIntros "#HPQ". rewrite /na_inv. iDestruct 1 as (i ?) "#Hinv".
    iExists i. iSplit; first done. iApply (inv_iff with "[] Hinv").
50 51
    iNext; iAlways.
    iSplit; iIntros "[[? Ho]|$]"; iLeft; iFrame "Ho"; by iApply "HPQ".
52 53
  Qed.

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

57
  Lemma na_own_disjoint p E1 E2 : na_own p E1 - na_own p E2 - E1 ## E2.
58
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
59
    apply wand_intro_r.
60
    rewrite /na_own -own_op own_valid -coPset_disj_valid_op. by iIntros ([? _]).
61 62
  Qed.

Ralf Jung's avatar
Ralf Jung committed
63
  Lemma na_own_union p E1 E2 :
64
    E1 ## E2  na_own p (E1  E2)  na_own p E1  na_own p E2.
65
  Proof.
66
    intros ?. by rewrite /na_own -own_op -pair_op left_id coPset_disj_union.
67 68
  Qed.

Ralf Jung's avatar
Ralf Jung committed
69 70 71 72 73 74 75
  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
76
  Lemma na_inv_alloc p E N P :  P ={E}= na_inv p N P.
77 78
  Proof.
    iIntros "HP".
Robbert Krebbers's avatar
Robbert Krebbers committed
79
    iMod (own_unit (prodUR coPset_disjUR (gset_disjUR positive)) p) as "Hempty".
80
    iMod (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
81
    { apply prod_updateP'. apply cmra_updateP_id, (reflexivity (R:=eq)).
82
      apply (gset_disj_alloc_empty_updateP_strong' (λ i, i  (N:coPset))).
Robbert Krebbers's avatar
Robbert Krebbers committed
83 84
      intros Ef. exists (coPpick ( N  gset_to_coPset Ef)).
      rewrite -elem_of_gset_to_coPset comm -elem_of_difference.
85 86
      apply coPpick_elem_of=> Hfin.
      eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
Robbert Krebbers's avatar
Robbert Krebbers committed
87
      apply gset_to_coPset_finite. }
88
    simpl. iDestruct "Hm" as %(<- & i & -> & ?).
89
    rewrite /na_inv.
90
    iMod (inv_alloc N with "[-]"); last (iModIntro; iExists i; eauto).
91 92 93
    iNext. iLeft. by iFrame.
  Qed.

Ralf Jung's avatar
Ralf Jung committed
94
  Lemma na_inv_open p E F N P :
95
    N  E  N  F 
Ralf Jung's avatar
Ralf Jung committed
96 97
    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).
98
  Proof.
99 100
    rewrite /na_inv. iIntros (??) "#Hnainv Htoks".
    iDestruct "Hnainv" as (i) "[% Hinv]".
Ralf Jung's avatar
Ralf Jung committed
101
    rewrite [F as X in na_own p X](union_difference_L (N) F) //.
102
    rewrite [X in (X  _)](union_difference_L {[i]} (N)) ?na_own_union; [|set_solver..].
Robbert Krebbers's avatar
Robbert Krebbers committed
103
    iDestruct "Htoks" as "[[Htoki $] $]".
104
    iInv "Hinv" as "[[$ >Hdis]|>Htoki2]" "Hclose".
105 106
    - iMod ("Hclose" with "[Htoki]") as "_"; first auto.
      iIntros "!> [HP $]".
107
      iInv N as "[[_ >Hdis2]|>Hitok]".
108
      + iDestruct (own_valid_2 with "Hdis Hdis2") as %[_ Hval%gset_disj_valid_op].
Robbert Krebbers's avatar
Robbert Krebbers committed
109
        set_solver.
110
      + iSplitR "Hitok"; last by iFrame. eauto with iFrame.
111
    - iDestruct (na_own_disjoint with "Htoki Htoki2") as %?. set_solver.
112
  Qed.
113

114
  Global Instance into_inv_na p N P : IntoInv (na_inv p N P) N := {}.
115

116
  Global Instance into_acc_na p F E N P :
117
    IntoAcc (X:=unit) (na_inv p N P)
118
            (N  E  N  F) (na_own p F) (fupd E E) (fupd E E)
119 120
            (λ _,  P  na_own p (F∖↑N))%I (λ _,  P  na_own p (F∖↑N))%I
              (λ _, Some (na_own p F))%I.
121
  Proof.
122 123
    rewrite /IntoAcc /accessor. iIntros ((?&?)) "#Hinv Hown".
    rewrite exist_unit -assoc /=.
124
    iApply (na_inv_open with "Hinv"); done.
125
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
126
End proofs.