auth.v 8.95 KB
Newer Older
1
2
3
4
(** This logic-level wrapper on top of the [auth] RA turns out to be much harder
to use than just directly using the RA, hence it is deprecated and will be
removed entirely after some grace period. *)

5
6
From iris.algebra Require Export auth.
From iris.algebra Require Import gmap.
Ralf Jung's avatar
Ralf Jung committed
7
From iris.proofmode Require Import tactics.
8
From iris.base_logic.lib Require Export invariants.
Ralf Jung's avatar
Ralf Jung committed
9
From iris.prelude Require Import options.
10
11
12
Import uPred.

(* The CMRA we need. *)
13
Class authG Σ (A : ucmra) := AuthG {
14
  auth_inG : inG Σ (authR A);
15
  auth_cmra_discrete :> CmraDiscrete A;
16
}.
17
Local Existing Instance auth_inG.
18

19
Definition authΣ (A : ucmra) : gFunctors := #[ GFunctor (authR A) ].
20

21
Global Instance subG_authΣ Σ A : subG (authΣ A) Σ  CmraDiscrete A  authG Σ A.
22
Proof. solve_inG. Qed.
23
24

Section definitions.
25
  Context `{!invGS Σ, !authG Σ A} {T : Type} (γ : gname).
Robbert Krebbers's avatar
Robbert Krebbers committed
26

27
28
29
  Definition auth_own (a : A) : iProp Σ :=
    own γ ( a).
  Definition auth_inv (f : T  A) (φ : T  iProp Σ) : iProp Σ :=
30
     t, own γ ( f t)  φ t.
31
32
33
  Definition auth_ctx (N : namespace) (f : T  A) (φ : T  iProp Σ) : iProp Σ :=
    inv N (auth_inv f φ).

34
  Global Instance auth_own_ne : NonExpansive auth_own.
35
36
37
  Proof. solve_proper. Qed.
  Global Instance auth_own_proper : Proper (() ==> ()) auth_own.
  Proof. solve_proper. Qed.
38
  Global Instance auth_own_timeless a : Timeless (auth_own a).
39
  Proof. apply _. Qed.
40
  Global Instance auth_own_core_id a : CoreId a  Persistent (auth_own a).
Robbert Krebbers's avatar
Robbert Krebbers committed
41
42
43
44
45
46
47
  Proof. apply _. Qed.

  Global Instance auth_inv_ne n :
    Proper (pointwise_relation T (dist n) ==>
            pointwise_relation T (dist n) ==> dist n) auth_inv.
  Proof. solve_proper. Qed.
  Global Instance auth_inv_proper :
48
    Proper (pointwise_relation T () ==>
Robbert Krebbers's avatar
Robbert Krebbers committed
49
50
51
52
53
            pointwise_relation T () ==> ()) auth_inv.
  Proof. solve_proper. Qed.
  Global Instance auth_ctx_ne N n :
    Proper (pointwise_relation T (dist n) ==>
            pointwise_relation T (dist n) ==> dist n) (auth_ctx N).
54
  Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
55
  Global Instance auth_ctx_proper N :
56
    Proper (pointwise_relation T () ==>
Robbert Krebbers's avatar
Robbert Krebbers committed
57
            pointwise_relation T () ==> ()) (auth_ctx N).
58
  Proof. solve_proper. Qed.
59
  Global Instance auth_ctx_persistent N f φ : Persistent (auth_ctx N f φ).
60
61
62
63
  Proof. apply _. Qed.
End definitions.

Typeclasses Opaque auth_own auth_inv auth_ctx.
64
65
66
Global Instance: Params (@auth_own) 4 := {}.
Global Instance: Params (@auth_inv) 5 := {}.
Global Instance: Params (@auth_ctx) 7 := {}.
67
68

Section auth.
69
  Context `{!invGS Σ, !authG Σ A}.
70
71
72
73
74
75
76
77
  Context {T : Type} `{!Inhabited T}.
  Context (f : T  A) (φ : T  iProp Σ).
  Implicit Types N : namespace.
  Implicit Types P Q R : iProp Σ.
  Implicit Types a b : A.
  Implicit Types t u : T.
  Implicit Types γ : gname.

78
  Lemma auth_own_op γ a b : auth_own γ (a  b)  auth_own γ a  auth_own γ b.
79
80
  Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
81
(*
82
  Global Instance from_and_auth_own γ a b1 b2 :
83
    IsOp a b1 b2 →
84
    FromAnd false (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 90.
85
  Proof. rewrite /IsOp /FromAnd=> ->. by rewrite auth_own_op. Qed.
86
  Global Instance from_and_auth_own_persistent γ a b1 b2 :
87
    IsOp a b1 b2 → Or (CoreId b1) (CoreId b2) →
88
89
90
    FromAnd true (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 91.
  Proof.
    intros ? Hper; apply mk_from_and_persistent; [destruct Hper; apply _|].
91
    by rewrite -auth_own_op -is_op.
92
93
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
94
  Global Instance into_and_auth_own p γ a b1 b2 :
95
    IsOp a b1 b2 →
Robbert Krebbers's avatar
Robbert Krebbers committed
96
    IntoAnd p (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 90.
97
  Proof. intros. apply mk_into_and_sep. by rewrite (is_op a) auth_own_op. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
98
*)
99
100
101
102

  Lemma auth_own_mono γ a b : a  b  auth_own γ b  auth_own γ a.
  Proof. intros [? ->]. by rewrite auth_own_op sep_elim_l. Qed.
  Lemma auth_own_valid γ a : auth_own γ a   a.
103
  Proof. by rewrite /auth_own own_valid auth_frag_validI. Qed.
104
  Global Instance auth_own_sep_homomorphism γ :
105
106
    WeakMonoidHomomorphism op uPred_sep () (auth_own γ).
  Proof. split; try apply _. apply auth_own_op. Qed.
107

108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
  Lemma big_opL_auth_own {B} γ (g : nat  B  A) (l : list B) :
    l  [] 
    auth_own γ ([^op list] kx  l, g k x) 
             [ list] kx  l, auth_own γ (g k x).
  Proof. apply (big_opL_commute1 _). Qed.
  Lemma big_opM_auth_own `{Countable K} {B} γ (g : K  B  A) (m : gmap K B) :
    m   
    auth_own γ ([^op map] kx  m, g k x) 
             [ map] kx  m, auth_own γ (g k x).
  Proof. apply (big_opM_commute1 _). Qed.
  Lemma big_opS_auth_own `{Countable B} γ (g : B  A) (X : gset B) :
    X   
    auth_own γ ([^op set] x  X, g x)  [ set] x  X, auth_own γ (g x).
  Proof. apply (big_opS_commute1 _). Qed.
  Lemma big_opMS_auth_own `{Countable B} γ (g : B  A) (X : gmultiset B) :
    X   
    auth_own γ ([^op mset] x  X, g x)  [ mset] x  X, auth_own γ (g x).
  Proof. apply (big_opMS_commute1 _). Qed.

  Global Instance auth_own_cmra_sep_entails_homomorphism γ :
    MonoidHomomorphism op uPred_sep () (auth_own γ).
  Proof.
    split; [split|]; try apply _.
    - intros. by rewrite auth_own_op.
    - apply (affine _).
  Qed.

  Lemma big_opL_auth_own_1 {B} γ (g : nat  B  A) (l : list B) :
    auth_own γ ([^op list] kx  l, g k x) 
             [ list] kx  l, auth_own γ (g k x).
  Proof. apply (big_opL_commute _). Qed.
  Lemma big_opM_auth_own_1 `{Countable K} {B} γ (g : K  B  A)
        (m : gmap K B) :
    auth_own γ ([^op map] kx  m, g k x)  [ map] kx  m, auth_own γ (g k x).
  Proof. apply (big_opM_commute _). Qed.
  Lemma big_opS_auth_own_1 `{Countable B} γ (g : B  A) (X : gset B) :
    auth_own γ ([^op set] x  X, g x)  [ set] x  X, auth_own γ (g x).
  Proof. apply (big_opS_commute _). Qed.
  Lemma big_opMS_auth_own_1 `{Countable B} γ (g : B  A)
        (X : gmultiset B) :
    auth_own γ ([^op mset] x  X, g x)  [ mset] x  X, auth_own γ (g x).
  Proof. apply (big_opMS_commute _). Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
151
152
153
  Global Instance own_mono' γ : Proper (flip () ==> ()) (auth_own γ).
  Proof. intros a1 a2. apply auth_own_mono. Qed.

Dan Frumin's avatar
Dan Frumin committed
154
155
  Lemma auth_alloc_strong N E t (I : gname  Prop) :
    pred_infinite I 
156
     (f t)   φ t ={E}=  γ, I γ⌝  auth_ctx γ N f φ  auth_own γ (f t).
157
  Proof.
Dan Frumin's avatar
Dan Frumin committed
158
    iIntros (??) "Hφ". rewrite /auth_own /auth_ctx.
159
    iMod (own_alloc_strong ( f t   f t) I) as (γ) "[% [Hγ Hγ']]";
160
      [done|by apply auth_both_valid_discrete|].
161
    iMod (inv_alloc N _ (auth_inv γ f φ) with "[-Hγ']") as "#?".
162
    { iNext. rewrite /auth_inv. iExists t. by iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
163
    eauto.
164
165
  Qed.

Dan Frumin's avatar
Dan Frumin committed
166
  Lemma auth_alloc_cofinite N E t (G : gset gname) :
167
     (f t)   φ t ={E}=  γ, ⌜γ  G  auth_ctx γ N f φ  auth_own γ (f t).
Dan Frumin's avatar
Dan Frumin committed
168
169
170
171
172
173
  Proof.
    intros ?. apply auth_alloc_strong=>//.
    apply (pred_infinite_set (C:=gset gname)) => E'.
    exists (fresh (G  E')). apply not_elem_of_union, is_fresh.
  Qed.

174
  Lemma auth_alloc N E t :
175
     (f t)   φ t ={E}=  γ, auth_ctx γ N f φ  auth_own γ (f t).
176
177
  Proof.
    iIntros (?) "Hφ".
Dan Frumin's avatar
Dan Frumin committed
178
    iMod (auth_alloc_cofinite N E t  with "Hφ") as (γ) "[_ ?]"; eauto.
179
180
  Qed.

Gregory Malecha's avatar
Gregory Malecha committed
181
  Lemma auth_empty γ :  |==> auth_own γ ε.
Robbert Krebbers's avatar
Robbert Krebbers committed
182
  Proof. by rewrite /auth_own -own_unit. Qed.
183

184
  Lemma auth_inv_acc E γ a :
185
     auth_inv γ f φ  auth_own γ a ={E}=  t,
Ralf Jung's avatar
Ralf Jung committed
186
187
      a  f t   φ t   u b,
      (f t, a) ~l~> (f u, b)   φ u ={E}=  auth_inv γ f φ  auth_own γ b.
188
  Proof using Type*.
189
    iIntros "[Hinv Hγf]". rewrite /auth_inv /auth_own.
Robbert Krebbers's avatar
Robbert Krebbers committed
190
    iDestruct "Hinv" as (t) "[>Hγa Hφ]".
191
    iModIntro. iExists t.
192
    iDestruct (own_valid_2 with "Hγa Hγf") as % [? ?]%auth_both_valid_discrete.
193
    iSplit; first done. iFrame. iIntros (u b) "[% Hφ]".
194
    iMod (own_update_2 with "Hγa Hγf") as "[Hγa Hγf]".
Robbert Krebbers's avatar
Robbert Krebbers committed
195
    { eapply auth_update; eassumption. }
196
    iModIntro. iFrame. iExists u. iFrame.
197
198
  Qed.

Ralf Jung's avatar
Ralf Jung committed
199
  Lemma auth_acc E N γ a :
200
201
    N  E 
    auth_ctx γ N f φ  auth_own γ a ={E,E∖↑N}=  t,
Ralf Jung's avatar
Ralf Jung committed
202
      a  f t   φ t   u b,
203
      (f t, a) ~l~> (f u, b)   φ u ={E∖↑N,E}= auth_own γ b.
204
  Proof using Type*.
205
206
    iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose".
    (* The following is essentially a very trivial composition of the accessors
Ralf Jung's avatar
Ralf Jung committed
207
       [auth_inv_acc] and [inv_acc] -- but since we don't have any good support
208
209
210
211
       for that currently, this gets more tedious than it should, with us having
       to unpack and repack various proofs.
       TODO: Make this mostly automatic, by supporting "opening accessors
       around accessors". *)
212
    iMod (auth_inv_acc with "[$Hinv $Hγf]") as (t) "(?&?&HclAuth)".
213
214
    iModIntro. iExists t. iFrame. iIntros (u b) "H".
    iMod ("HclAuth" $! u b with "H") as "(Hinv & ?)". by iMod ("Hclose" with "Hinv").
215
216
  Qed.
End auth.
Robbert Krebbers's avatar
Robbert Krebbers committed
217

Ralf Jung's avatar
Ralf Jung committed
218
Global Arguments auth_acc {_ _ _} [_] {_} [_] _ _ _ _ _ _ _.