auth.v 4.31 KB
Newer Older
1
From iris.algebra Require Export auth upred_tactics.
2
From iris.algebra Require Import gmap.
3
From iris.program_logic Require Export invariants ghost_ownership.
4
From iris.proofmode Require Import invariants ghost_ownership.
5
Import uPred.
6

7
(* The CMRA we need. *)
8 9
Class authG Σ (A : ucmraT) := AuthG {
  auth_inG :> inG Σ (authR A);
10
  auth_timeless :> CMRADiscrete A;
11
}.
12
(* The Functor we need. *)
13
Definition authGF (A : ucmraT) : gFunctor := GFunctor (constRF (authR A)).
14
(* Show and register that they match. *)
15
Instance authGF_inGF `{inGF Σ (authGF A), CMRADiscrete A} : authG Σ A.
16
Proof. split; try apply _. apply: inGF_inG. Qed.
17

18
Section definitions.
19 20
  Context `{irisG Λ Σ, authG Σ A} (γ : gname).
  Definition auth_own (a : A) : iProp Σ :=
21
    own γ ( a).
22
  Definition auth_inv (φ : A  iProp Σ) : iProp Σ :=
23
    ( a, own γ ( a)  φ a)%I.
24
  Definition auth_ctx (N : namespace) (φ : A  iProp Σ) : iProp Σ :=
25 26 27 28
    inv N (auth_inv φ).

  Global Instance auth_own_ne n : Proper (dist n ==> dist n) auth_own.
  Proof. solve_proper. Qed.
29
  Global Instance auth_own_proper : Proper (() ==> ()) auth_own.
30 31 32
  Proof. solve_proper. Qed.
  Global Instance auth_own_timeless a : TimelessP (auth_own a).
  Proof. apply _. Qed.
33 34 35 36 37 38
  Global Instance auth_inv_ne n : 
    Proper (pointwise_relation A (dist n) ==> dist n) (auth_inv).
  Proof. solve_proper. Qed.
  Global Instance auth_ctx_ne n N :
    Proper (pointwise_relation A (dist n) ==> dist n) (auth_ctx N).
  Proof. solve_proper. Qed.
39
  Global Instance auth_ctx_persistent N φ : PersistentP (auth_ctx N φ).
40 41
  Proof. apply _. Qed.
End definitions.
Ralf Jung's avatar
Ralf Jung committed
42

43
Typeclasses Opaque auth_own auth_ctx.
44 45 46
Instance: Params (@auth_inv) 6.
Instance: Params (@auth_own) 6.
Instance: Params (@auth_ctx) 7.
47

48
Section auth.
49 50
  Context `{irisG Λ Σ, authG Σ A}.
  Context (φ : A  iProp Σ) {φ_proper : Proper (() ==> ()) φ}.
51
  Implicit Types N : namespace.
52
  Implicit Types P Q R : iProp Σ.
53 54 55
  Implicit Types a b : A.
  Implicit Types γ : gname.

56
  Lemma auth_own_op γ a b : auth_own γ (a  b)  auth_own γ a  auth_own γ b.
57
  Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
58

Zhen Zhang's avatar
Zhen Zhang committed
59
  Global Instance from_sep_own_authM γ a b :
60
    FromSep (auth_own γ (a  b)) (auth_own γ a) (auth_own γ b) | 90.
Zhen Zhang's avatar
Zhen Zhang committed
61 62
  Proof. by rewrite /FromSep auth_own_op. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
63 64 65
  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.

Robbert Krebbers's avatar
Robbert Krebbers committed
66 67 68 69
  Global Instance auth_own_persistent γ a :
    Persistent a  PersistentP (auth_own γ a).
  Proof. rewrite /auth_own. apply _. Qed.

70
  Lemma auth_own_valid γ a : auth_own γ a   a.
71
  Proof. by rewrite /auth_own own_valid auth_validI. Qed.
72

73
  Lemma auth_alloc_strong N E a (G : gset gname) :
74
     a   φ a ={E}=>  γ,  (γ  G)  auth_ctx γ N φ  auth_own γ a.
75
  Proof.
76 77
    iIntros (?) "Hφ". rewrite /auth_own /auth_ctx.
    iVs (own_alloc_strong (Auth (Excl' a) a) G) as (γ) "[% Hγ]"; first done.
78
    iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
79
    iVs (inv_alloc N _ (auth_inv γ φ) with "[-Hγ']").
80
    { iNext. iExists a. by iFrame. }
81
    iVsIntro; iExists γ. iSplit; first by iPureIntro. by iFrame.
82 83 84
  Qed.

  Lemma auth_alloc N E a :
85
     a   φ a ={E}=>  γ, auth_ctx γ N φ  auth_own γ a.
86
  Proof.
87 88
    iIntros (?) "Hφ".
    iVs (auth_alloc_strong N E a  with "Hφ") as (γ) "[_ ?]"; eauto.
89 90
  Qed.

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

94 95 96 97 98
  Lemma auth_open E N γ a :
    nclose N  E 
    auth_ctx γ N φ   auth_own γ a ={E,EN}=>  af,
        (a  af)   φ (a  af)   b,
       (a ~l~> b @ Some af)   φ (b  af) ={EN,E}= auth_own γ b.
Ralf Jung's avatar
Ralf Jung committed
99
  Proof.
100 101
    iIntros (?) "(#? & Hγf)". rewrite /auth_ctx /auth_own.
    iInv N as (a') "[Hγ Hφ]" "Hclose".
102
    iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
103 104 105 106 107 108
    iDestruct (own_valid with "#Hγ") as % [[af Ha'] ?]%auth_valid_discrete.
    simpl in Ha'; rewrite ->(left_id _ _) in Ha'; setoid_subst.
    iVsIntro. iExists af; iFrame "Hφ"; iSplit; first done.
    iIntros (b) "[% Hφ]".
    iVs (own_update with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto.
    iVs ("Hclose" with "[Hφ Hγ]") as "_"; auto.
109
    iNext. iExists (b  af). by iFrame.
110
  Qed.
111
End auth.