auth.v 6.7 KB
Newer Older
1
From iris.base_logic.lib Require Export invariants.
2 3 4
From iris.algebra Require Export auth.
From iris.algebra Require Import gmap.
From iris.proofmode Require Import tactics.
5
Set Default Proof Using "Type".
6 7 8 9 10
Import uPred.

(* The CMRA we need. *)
Class authG Σ (A : ucmraT) := AuthG {
  auth_inG :> inG Σ (authR A);
11
  auth_cmra_discrete :> CmraDiscrete A;
12
}.
13
Definition authΣ (A : ucmraT) : gFunctors := #[ GFunctor (authR A) ].
14

15
Instance subG_authΣ Σ A : subG (authΣ A) Σ  CmraDiscrete A  authG Σ A.
16
Proof. solve_inG. Qed.
17 18

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

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

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

Typeclasses Opaque auth_own auth_inv auth_ctx.
58 59 60
Instance: Params (@auth_own) 4 := {}.
Instance: Params (@auth_inv) 5 := {}.
Instance: Params (@auth_ctx) 7 := {}.
61 62

Section auth.
63
  Context `{!invG Σ, !authG Σ A}.
64 65 66 67 68 69 70 71
  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.

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

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

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

  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.
98
  Global Instance auth_own_sep_homomorphism γ :
99 100
    WeakMonoidHomomorphism op uPred_sep () (auth_own γ).
  Proof. split; try apply _. apply auth_own_op. Qed.
101

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

Dan Frumin's avatar
Dan Frumin committed
105 106 107
  Lemma auth_alloc_strong N E t (I : gname  Prop) :
    pred_infinite I 
     (f t)   φ t ={E}=  γ, I γ⌝  auth_ctx γ N f φ  auth_own γ (f t).
108
  Proof.
Dan Frumin's avatar
Dan Frumin committed
109 110
    iIntros (??) "Hφ". rewrite /auth_own /auth_ctx.
    iMod (own_alloc_strong (Auth (Excl' (f t)) (f t)) I) as (γ) "[% Hγ]"; [done|done|].
111
    iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
112
    iMod (inv_alloc N _ (auth_inv γ f φ) with "[-Hγ']") as "#?".
113
    { iNext. rewrite /auth_inv. iExists t. by iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
114
    eauto.
115 116
  Qed.

Dan Frumin's avatar
Dan Frumin committed
117 118 119 120 121 122 123 124
  Lemma auth_alloc_cofinite N E t (G : gset gname) :
     (f t)   φ t ={E}=  γ, ⌜γ  G  auth_ctx γ N f φ  auth_own γ (f t).
  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.

125
  Lemma auth_alloc N E t :
126
     (f t)   φ t ={E}=  γ, auth_ctx γ N f φ  auth_own γ (f t).
127 128
  Proof.
    iIntros (?) "Hφ".
Dan Frumin's avatar
Dan Frumin committed
129
    iMod (auth_alloc_cofinite N E t  with "Hφ") as (γ) "[_ ?]"; eauto.
130 131
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
132 133
  Lemma auth_empty γ : (|==> auth_own γ ε)%I.
  Proof. by rewrite /auth_own -own_unit. Qed.
134 135

  Lemma auth_acc E γ a :
136
     auth_inv γ f φ  auth_own γ a ={E}=  t,
Ralf Jung's avatar
Ralf Jung committed
137 138
      a  f t   φ t   u b,
      (f t, a) ~l~> (f u, b)   φ u ={E}=  auth_inv γ f φ  auth_own γ b.
139
  Proof using Type*.
140
    iIntros "[Hinv Hγf]". rewrite /auth_inv /auth_own.
Robbert Krebbers's avatar
Robbert Krebbers committed
141
    iDestruct "Hinv" as (t) "[>Hγa Hφ]".
142
    iModIntro. iExists t.
143
    iDestruct (own_valid_2 with "Hγa Hγf") as % [? ?]%auth_valid_discrete_2.
144
    iSplit; first done. iFrame. iIntros (u b) "[% Hφ]".
145
    iMod (own_update_2 with "Hγa Hγf") as "[Hγa Hγf]".
Robbert Krebbers's avatar
Robbert Krebbers committed
146
    { eapply auth_update; eassumption. }
147
    iModIntro. iFrame. iExists u. iFrame.
148 149 150
  Qed.

  Lemma auth_open E N γ a :
151 152
    N  E 
    auth_ctx γ N f φ  auth_own γ a ={E,E∖↑N}=  t,
Ralf Jung's avatar
Ralf Jung committed
153
      a  f t   φ t   u b,
154
      (f t, a) ~l~> (f u, b)   φ u ={E∖↑N,E}= auth_own γ b.
155
  Proof using Type*.
156 157 158 159 160 161 162
    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". *)
163 164 165
    iMod (auth_acc with "[$Hinv $Hγf]") as (t) "(?&?&HclAuth)".
    iModIntro. iExists t. iFrame. iIntros (u b) "H".
    iMod ("HclAuth" $! u b with "H") as "(Hinv & ?)". by iMod ("Hclose" with "Hinv").
166 167
  Qed.
End auth.
Robbert Krebbers's avatar
Robbert Krebbers committed
168

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