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
Definition authΣ (A : ucmra) : gFunctors := #[ GFunctor (authR A) ].
19

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

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

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

33
  Global Instance auth_own_ne : NonExpansive auth_own.
34
35
36
  Proof. solve_proper. Qed.
  Global Instance auth_own_proper : Proper (() ==> ()) auth_own.
  Proof. solve_proper. Qed.
37
  Global Instance auth_own_timeless a : Timeless (auth_own a).
38
  Proof. apply _. Qed.
39
  Global Instance auth_own_core_id a : CoreId a  Persistent (auth_own a).
Robbert Krebbers's avatar
Robbert Krebbers committed
40
41
42
43
44
45
46
  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 :
47
    Proper (pointwise_relation T () ==>
Robbert Krebbers's avatar
Robbert Krebbers committed
48
49
50
51
52
            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).
53
  Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
54
  Global Instance auth_ctx_proper N :
55
    Proper (pointwise_relation T () ==>
Robbert Krebbers's avatar
Robbert Krebbers committed
56
            pointwise_relation T () ==> ()) (auth_ctx N).
57
  Proof. solve_proper. Qed.
58
  Global Instance auth_ctx_persistent N f φ : Persistent (auth_ctx N f φ).
59
60
61
62
  Proof. apply _. Qed.
End definitions.

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

Section auth.
68
  Context `{!invGS Σ, !authG Σ A}.
69
70
71
72
73
74
75
76
  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.

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

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

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

  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.
102
  Proof. by rewrite /auth_own own_valid auth_frag_validI. Qed.
103
  Global Instance auth_own_sep_homomorphism γ :
104
105
    WeakMonoidHomomorphism op uPred_sep () (auth_own γ).
  Proof. split; try apply _. apply auth_own_op. Qed.
106

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
  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
150
151
152
  Global Instance own_mono' γ : Proper (flip () ==> ()) (auth_own γ).
  Proof. intros a1 a2. apply auth_own_mono. Qed.

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

Dan Frumin's avatar
Dan Frumin committed
165
  Lemma auth_alloc_cofinite N E t (G : gset gname) :
166
     (f t)   φ t ={E}=  γ, ⌜γ  G  auth_ctx γ N f φ  auth_own γ (f t).
Dan Frumin's avatar
Dan Frumin committed
167
168
169
170
171
172
  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.

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

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

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

Ralf Jung's avatar
Ralf Jung committed
198
  Lemma auth_acc E N γ a :
199
200
    N  E 
    auth_ctx γ N f φ  auth_own γ a ={E,E∖↑N}=  t,
Ralf Jung's avatar
Ralf Jung committed
201
      a  f t   φ t   u b,
202
      (f t, a) ~l~> (f u, b)   φ u ={E∖↑N,E}= auth_own γ b.
203
  Proof using Type*.
204
205
    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
206
       [auth_inv_acc] and [inv_acc] -- but since we don't have any good support
207
208
209
210
       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". *)
211
    iMod (auth_inv_acc with "[$Hinv $Hγf]") as (t) "(?&?&HclAuth)".
212
213
    iModIntro. iExists t. iFrame. iIntros (u b) "H".
    iMod ("HclAuth" $! u b with "H") as "(Hinv & ?)". by iMod ("Hclose" with "Hinv").
214
215
  Qed.
End auth.
Robbert Krebbers's avatar
Robbert Krebbers committed
216

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