wsat.v 7.41 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.
6
Set Default Proof Using "Type*".
Robbert Krebbers's avatar
Robbert Krebbers committed
7

8 9 10 11 12 13 14 15 16 17 18 19
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.

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

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
47
(* Invariants *)
48 49
Instance invariant_unfold_contractive : Contractive (@invariant_unfold Σ).
Proof. solve_contractive. Qed.
50
Global Instance ownI_contractive i : Contractive (@ownI Σ _ i).
51
Proof. solve_contractive. 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 56
Lemma ownE_empty : (|==> ownE )%I.
Proof. by rewrite /uPred_valid (own_empty (coPset_disjUR) enabled_name). Qed.
57
Lemma ownE_op E1 E2 : E1  E2  ownE (E1  E2)  ownE E1  ownE E2.
58
Proof. intros. by rewrite /ownE -own_op coPset_disj_union. Qed.
Ralf Jung's avatar
Ralf Jung committed
59
Lemma ownE_disjoint E1 E2 : ownE E1  ownE E2  E1  E2.
60
Proof. rewrite /ownE -own_op own_valid. by iIntros (?%coPset_disj_valid_op). Qed.
Ralf Jung's avatar
Ralf Jung committed
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
Lemma ownE_singleton_twice i : ownE {[i]}  ownE {[i]}  False.
68
Proof. rewrite ownE_disjoint. iIntros (?); set_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
69

70 71
Lemma ownD_empty : (|==> ownD )%I.
Proof. by rewrite /uPred_valid (own_empty (gset_disjUR positive) disabled_name). Qed.
72
Lemma ownD_op E1 E2 : E1  E2  ownD (E1  E2)  ownD E1  ownD E2.
73
Proof. intros. by rewrite /ownD -own_op gset_disj_union. Qed.
Ralf Jung's avatar
Ralf Jung committed
74
Lemma ownD_disjoint E1 E2 : ownD E1  ownD E2  E1  E2.
75
Proof. rewrite /ownD -own_op own_valid. by iIntros (?%gset_disj_valid_op). Qed.
Ralf Jung's avatar
Ralf Jung committed
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
Lemma ownD_singleton_twice i : ownD {[i]}  ownD {[i]}  False.
83 84
Proof. rewrite ownD_disjoint. iIntros (?); set_solver. Qed.

85
Lemma invariant_lookup (I : gmap positive (iProp Σ)) i P :
86
  own invariant_name ( (invariant_unfold <$> I : gmap _ _)) 
87
  own invariant_name ( {[i := invariant_unfold P]}) 
Ralf Jung's avatar
Ralf Jung committed
88
   Q, I !! i = Some Q   (Q  P).
Robbert Krebbers's avatar
Robbert Krebbers committed
89
Proof.
90
  rewrite -own_op own_valid 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
Lemma ownI_open i P : wsat  ownI i P  ownE {[i]}  wsat   P  ownD {[i]}.
105 106
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
Qed.
114
Lemma ownI_close i P : wsat  ownI i P   P  ownD {[i]}  wsat  ownE {[i]}.
115 116
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) 
Ralf Jung's avatar
Ralf Jung committed
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
  iMod (own_empty (gset_disjUR positive) disabled_name) as "HE".
130
  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 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167

Lemma ownI_alloc_open φ P :
  ( E : gset positive,  i, i  E  φ i) 
  wsat ==  i, ⌜φ i  (ownE {[i]} - wsat)  ownI i P  ownD {[i]}.
Proof.
  iIntros (Hfresh) "Hw". iDestruct "Hw" as (I) "[? HI]".
  iMod (own_empty (gset_disjUR positive) disabled_name) as "HD".
  iMod (own_updateP with "HD") as "HD".
  { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None  φ i)).
    intros E. destruct (Hfresh (E  dom _ I))
      as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. }
  iDestruct "HD" as (X) "[Hi HD]"; iDestruct "Hi" as %(i & -> & HIi & ?).
  iMod (own_update with "Hw") as "[Hw HiP]".
  { eapply auth_update_alloc,
     (alloc_singleton_local_update _ i (invariant_unfold P)); last done.
    by rewrite /= lookup_fmap HIi. }
  iModIntro; iExists i;  iSplit; [done|]. rewrite /ownI; iFrame "HiP".
  rewrite -/(ownD _). iFrame "HD".
  iIntros "HE". 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". by iRight.
Qed.
168
End wsat.