wsat.v 6.23 KB
Newer Older
1 2
From iris.base_logic.lib Require Export own.
From iris.prelude Require Export coPset.
3 4
From iris.algebra Require Import gmap auth agree gset coPset.
From iris.base_logic Require Import big_op.
5
From iris.proofmode Require Import tactics.
Robbert Krebbers's avatar
Robbert Krebbers committed
6

7 8 9 10 11 12 13 14 15 16 17 18
Module invG.
  Class invG (Σ : gFunctors) : Set := WsatG {
    inv_inG :> inG Σ (authR (gmapUR positive (agreeR (laterC (iPreProp Σ)))));
    enabled_inG :> inG Σ coPset_disjR;
    disabled_inG :> inG Σ (gset_disjR positive);
    invariant_name : gname;
    enabled_name : gname;
    disabled_name : gname;
  }.
End invG.
Import invG.

19 20
Definition invariant_unfold {Σ} (P : iProp Σ) : agree (later (iPreProp Σ)) :=
  to_agree (Next (iProp_unfold P)).
21
Definition ownI `{invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
22
  own invariant_name ( {[ i := invariant_unfold P ]}).
23
Arguments ownI {_ _} _ _%I.
24
Typeclasses Opaque ownI.
25
Instance: Params (@ownI) 3.
26

27
Definition ownE `{invG Σ} (E : coPset) : iProp Σ :=
28 29
  own enabled_name (CoPset E).
Typeclasses Opaque ownE.
30
Instance: Params (@ownE) 3.
31

32
Definition ownD `{invG Σ} (E : gset positive) : iProp Σ :=
33 34
  own disabled_name (GSet E).
Typeclasses Opaque ownD.
35
Instance: Params (@ownD) 3.
36

37
Definition wsat `{invG Σ} : iProp Σ :=
38 39 40
  ( I : gmap positive (iProp Σ),
    own invariant_name ( (invariant_unfold <$> I : gmap _ _)) 
    [ map] i  Q  I,  Q  ownD {[i]}  ownE {[i]})%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
41

42 43
Section wsat.
Context `{invG Σ}.
44 45
Implicit Types P : iProp Σ.

Robbert Krebbers's avatar
Robbert Krebbers committed
46
(* Invariants *)
47
Global Instance ownI_contractive i : Contractive (@ownI Σ _ i).
Robbert Krebbers's avatar
Robbert Krebbers committed
48
Proof.
49 50
  intros n P Q HPQ. rewrite /ownI /invariant_unfold. do 4 f_equiv.
  apply Next_contractive=> j ?; by rewrite (HPQ j).
Robbert Krebbers's avatar
Robbert Krebbers committed
51
Qed.
52 53
Global Instance ownI_persistent i P : PersistentP (ownI i P).
Proof. rewrite /ownI. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
54

55
Lemma ownE_empty : True == ownE .
56 57 58 59
Proof. by rewrite (own_empty (A:=coPset_disjUR) enabled_name). Qed.
Lemma ownE_op E1 E2 : E1  E2  ownE (E1  E2)  ownE E1  ownE E2.
Proof. intros. by rewrite /ownE -own_op coPset_disj_union. Qed.
Lemma ownE_disjoint E1 E2 : ownE E1  ownE E2  E1  E2.
60
Proof. rewrite /ownE own_valid_2. by iIntros (?%coPset_disj_valid_op). Qed.
61
Lemma ownE_op' E1 E2 : E1  E2  ownE (E1  E2)  ownE E1  ownE E2.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
Proof.
63
  iSplit; [iIntros "[% ?]"; by iApply ownE_op|].
64
  iIntros "HE". iDestruct (ownE_disjoint with "HE") as %?.
65
  iSplit; first done. iApply ownE_op; by try iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
66
Qed.
67 68
Lemma ownE_singleton_twice i : ownE {[i]}  ownE {[i]}  False.
Proof. rewrite ownE_disjoint. iIntros (?); set_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
69

70
Lemma ownD_empty : True == ownD .
71 72 73 74
Proof. by rewrite (own_empty (A:=gset_disjUR _) disabled_name). Qed.
Lemma ownD_op E1 E2 : E1  E2  ownD (E1  E2)  ownD E1  ownD E2.
Proof. intros. by rewrite /ownD -own_op gset_disj_union. Qed.
Lemma ownD_disjoint E1 E2 : ownD E1  ownD E2  E1  E2.
75
Proof. rewrite /ownD own_valid_2. by iIntros (?%gset_disj_valid_op). Qed.
76
Lemma ownD_op' E1 E2 : E1  E2  ownD (E1  E2)  ownD E1  ownD E2.
Robbert Krebbers's avatar
Robbert Krebbers committed
77
Proof.
78
  iSplit; [iIntros "[% ?]"; by iApply ownD_op|].
79
  iIntros "HE". iDestruct (ownD_disjoint with "HE") as %?.
80
  iSplit; first done. iApply ownD_op; by try iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
81
Qed.
82 83 84
Lemma ownD_singleton_twice i : ownD {[i]}  ownD {[i]}  False.
Proof. rewrite ownD_disjoint. iIntros (?); set_solver. Qed.

85
Lemma invariant_lookup (I : gmap positive (iProp Σ)) i P :
86 87 88
  own invariant_name ( (invariant_unfold <$> I : gmap _ _)) 
  own invariant_name ( {[i := invariant_unfold P]}) 
   Q, I !! i = Some Q   (Q  P).
Robbert Krebbers's avatar
Robbert Krebbers committed
89
Proof.
90
  rewrite own_valid_2 auth_validI /=. iIntros "[#HI #HvI]".
91 92 93 94 95 96 97 98 99 100
  iDestruct "HI" as (I') "HI". rewrite gmap_equivI gmap_validI.
  iSpecialize ("HI" $! i). iSpecialize ("HvI" $! i).
  rewrite left_id_L lookup_fmap lookup_op lookup_singleton uPred.option_equivI.
  case: (I !! i)=> [Q|] /=; [|case: (I' !! i)=> [Q'|] /=; by iExFalso].
  iExists Q; iSplit; first done.
  iAssert (invariant_unfold Q  invariant_unfold P)%I as "?".
  { case: (I' !! i)=> [Q'|] //=.
    iRewrite "HI" in "HvI". rewrite uPred.option_validI agree_validI.
    iRewrite -"HvI" in "HI". by rewrite agree_idemp. }
  rewrite /invariant_unfold.
101
  by rewrite agree_equivI uPred.later_equivI iProp_unfold_equivI.
Robbert Krebbers's avatar
Robbert Krebbers committed
102
Qed.
103 104 105 106

Lemma ownI_open i P : wsat  ownI i P  ownE {[i]}  wsat   P  ownD {[i]}.
Proof.
  rewrite /ownI. iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[? HI]".
107 108
  iDestruct (invariant_lookup I i P with "[$Hw $Hi]") as (Q) "[% #HPQ]".
  iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ $]|HiE'] HI]"; eauto.
109 110 111
  - iSplitR "HQ"; last by iNext; iRewrite -"HPQ".
    iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
    iFrame "HI"; eauto.
112
  - iDestruct (ownE_singleton_twice with "[$HiE $HiE']") as %[].
113 114 115 116
Qed.
Lemma ownI_close i P : wsat  ownI i P   P  ownD {[i]}  wsat  ownE {[i]}.
Proof.
  rewrite /ownI. iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[? HI]".
117
  iDestruct (invariant_lookup with "[$Hw $Hi]") as (Q) "[% #HPQ]".
118
  iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto.
119
  - iDestruct (ownD_singleton_twice with "[-]") as %[]. by iFrame.
120 121 122 123 124 125
  - iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
    iFrame "HI". iLeft. iFrame "HiD". by iNext; iRewrite "HPQ".
Qed.

Lemma ownI_alloc φ P :
  ( E : gset positive,  i, i  E  φ i) 
126
  wsat   P ==  i,  (φ i)  wsat  ownI i P.
Robbert Krebbers's avatar
Robbert Krebbers committed
127
Proof.
128
  iIntros (Hfresh) "[Hw HP]". iDestruct "Hw" as (I) "[? HI]".
129 130
  iMod (own_empty (A:=gset_disjUR positive) disabled_name) as "HE".
  iMod (own_updateP with "HE") as "HE".
131
  { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None  φ i)).
132 133 134
    intros E. destruct (Hfresh (E  dom _ I))
      as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. }
  iDestruct "HE" as (X) "[Hi HE]"; iDestruct "Hi" as %(i & -> & HIi & ?).
135
  iMod (own_update with "Hw") as "[Hw HiP]".
136 137
  { eapply auth_update_alloc,
     (alloc_singleton_local_update _ i (invariant_unfold P)); last done.
138
    by rewrite /= lookup_fmap HIi. }
139
  iModIntro; iExists i;  iSplit; [done|]. rewrite /ownI; iFrame "HiP".
140 141 142 143
  iExists (<[i:=P]>I); iSplitL "Hw".
  { by rewrite fmap_insert insert_singleton_op ?lookup_fmap ?HIi. }
  iApply (big_sepM_insert _ I); first done.
  iFrame "HI". iLeft. by rewrite /ownD; iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
144
Qed.
145
End wsat.