auth.v 5.97 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
From iris.program_logic Require Export invariants.
From iris.algebra Require Export auth.
From iris.algebra Require Import gmap.
From iris.proofmode Require Import tactics.
Import uPred.

(* The CMRA we need. *)
Class authG Σ (A : ucmraT) := AuthG {
  auth_inG :> inG Σ (authR A);
  auth_discrete :> CMRADiscrete A;
}.
Definition authΣ (A : ucmraT) : gFunctors := #[ GFunctor (constRF (authR A)) ].

Instance subG_authΣ Σ A : subG (authΣ A) Σ  CMRADiscrete A  authG Σ A.
Proof. intros ?%subG_inG ?. by split. Qed.

Section definitions.
Robbert Krebbers's avatar
Robbert Krebbers committed
18
19
  Context `{irisG Λ Σ, authG Σ A} {T : Type} (γ : gname).

20
21
22
23
24
25
26
27
28
29
30
31
32
  Definition auth_own (a : A) : iProp Σ :=
    own γ ( a).
  Definition auth_inv (f : T  A) (φ : T  iProp Σ) : iProp Σ :=
    ( t, own γ ( f t)  φ t)%I.
  Definition auth_ctx (N : namespace) (f : T  A) (φ : T  iProp Σ) : iProp Σ :=
    inv N (auth_inv f φ).

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

Typeclasses Opaque auth_own auth_inv auth_ctx.
Instance: Params (@auth_own) 4.
Robbert Krebbers's avatar
Robbert Krebbers committed
58
59
Instance: Params (@auth_inv) 5.
Instance: Params (@auth_ctx) 8.
60
61
62
63
64
65
66
67
68
69
70
71
72
73

Section auth.
  Context `{irisG Λ Σ, authG Σ A}.
  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.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
74
75
76
77
78
79
80
81
  Global Instance from_sep_auth_own γ a b1 b2 :
    FromOp a b1 b2 
    FromSep (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 90.
  Proof. rewrite /FromOp /FromSep=> <-. by rewrite auth_own_op. Qed.
  Global Instance into_and_auth_own p γ a b1 b2 :
    IntoOp a b1 b2 
    IntoAnd p (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 90.
  Proof. intros. apply mk_into_and_sep. by rewrite (into_op a) auth_own_op. Qed.
82
83
84
85
86
87

  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.
  Proof. by rewrite /auth_own own_valid auth_validI. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
88
89
90
91
92
  Global Instance auth_own_cmra_homomorphism : CMRAHomomorphism (auth_own γ).
  Proof. split. apply _. apply auth_own_op. Qed.
  Global Instance own_mono' γ : Proper (flip () ==> ()) (auth_own γ).
  Proof. intros a1 a2. apply auth_own_mono. Qed.

93
94
95
96
97
98
  Lemma auth_alloc_strong N E t (G : gset gname) :
     (f t)   φ t ={E}=>  γ,  (γ  G)  auth_ctx γ N f φ  auth_own γ (f t).
  Proof.
    iIntros (?) "Hφ". rewrite /auth_own /auth_ctx.
    iVs (own_alloc_strong (Auth (Excl' (f t)) (f t)) G) as (γ) "[% Hγ]"; first done.
    iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
Robbert Krebbers's avatar
Robbert Krebbers committed
99
    iVs (inv_alloc N _ (auth_inv γ f φ) with "[-Hγ']") as "#?".
100
    { iNext. rewrite /auth_inv. iExists t. by iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
101
    eauto.
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
  Qed.

  Lemma auth_alloc N E t :
     (f t)   φ t ={E}=>  γ, auth_ctx γ N f φ  auth_own γ (f t).
  Proof.
    iIntros (?) "Hφ".
    iVs (auth_alloc_strong N E t  with "Hφ") as (γ) "[_ ?]"; eauto.
  Qed.

  Lemma auth_empty γ : True =r=> auth_own γ .
  Proof. by rewrite /auth_own -own_empty. Qed.

  Lemma auth_acc E γ a :
     auth_inv γ f φ  auth_own γ a ={E}=>  t,
       (a  f t)   φ t   u b,
       ((f t, a) ~l~> (f u, b))   φ u ={E}=  auth_inv γ f φ  auth_own γ b.
  Proof.
    iIntros "(Hinv & Hγf)". rewrite /auth_inv /auth_own.
Robbert Krebbers's avatar
Robbert Krebbers committed
120
121
122
    iDestruct "Hinv" as (t) "[>Hγa Hφ]".
    iVsIntro. iExists t.
    iDestruct (own_valid_2 with "[$Hγa $Hγf]") as % [? ?]%auth_valid_discrete_2.
123
    iSplit; first done. iFrame. iIntros (u b) "[% Hφ]".
Robbert Krebbers's avatar
Robbert Krebbers committed
124
125
    iVs (own_update_2 with "[$Hγa $Hγf]") as "[Hγa Hγf]".
    { eapply auth_update; eassumption. }
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
    iVsIntro. iFrame. iExists u. iFrame.
  Qed.

  Lemma auth_open E N γ a :
    nclose N  E 
    auth_ctx γ N f φ  auth_own γ a ={E,EN}=>  t,
       (a  f t)   φ t   u b,
       ((f t, a) ~l~> (f u, b))   φ u ={EN,E}= auth_own γ b.
  Proof.
    iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose".
    (* The following is essentially a very trivial composition of the accessors
       [auth_acc] and [inv_open] -- but since we don't have any good support
       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". *)
Robbert Krebbers's avatar
Robbert Krebbers committed
142
    iVs (auth_acc with "[$Hinv $Hγf]") as (t) "(?&?&HclAuth)".
143
144
145
146
    iVsIntro. iExists t. iFrame. iIntros (u b) "H".
    iVs ("HclAuth" $! u b with "H") as "(Hinv & ?)". by iVs ("Hclose" with "Hinv").
  Qed.
End auth.
Robbert Krebbers's avatar
Robbert Krebbers committed
147
148

Arguments auth_open {_ _ _ _} [_] {_} [_] _ _ _ _ _ _ _.