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

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

18 19
Section definitions.
  Context `{authG Λ Σ A} (γ : gname).
20
  Definition auth_own (a : A) : iPropG Λ Σ :=
21 22 23 24 25 26 27 28
    own γ ( a).
  Definition auth_inv (φ : A  iPropG Λ Σ) : iPropG Λ Σ :=
    ( a, own γ ( a)  φ a)%I.
  Definition auth_ctx (N : namespace) (φ : A  iPropG Λ Σ) : iPropG Λ Σ :=
    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) 5.
Instance: Params (@auth_own) 5.
Instance: Params (@auth_ctx) 6.
47

48
Section auth.
49
  Context `{AuthI : authG Λ Σ A}.
50
  Context (φ : A  iPropG Λ Σ) {φ_proper : Proper (() ==> ()) φ}.
51
  Implicit Types N : namespace.
52
  Implicit Types P Q R : iPropG Λ Σ.
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.
58
  Lemma auth_own_valid γ a : auth_own γ a   a.
59
  Proof. by rewrite /auth_own own_valid auth_validI. Qed.
60

61
  Lemma auth_alloc_strong N E a (G : gset gname) :
62
     a  nclose N  E 
63
     φ a ={E}=>  γ, (γ  G)  auth_ctx γ N φ  auth_own γ a.
64
  Proof.
65
    iIntros {??} "Hφ". rewrite /auth_own /auth_ctx.
66
    iPvs (own_alloc_strong (Auth (Excl' a) a) _ G) as {γ} "[% Hγ]"; first done.
67
    iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
68
    iPvs (inv_alloc N _ (auth_inv γ φ) with "[-Hγ']"); first done.
69 70
    { iNext. iExists a. by iFrame. }
    iPvsIntro; iExists γ. iSplit; first by iPureIntro. by iFrame.
71 72 73 74 75 76
  Qed.

  Lemma auth_alloc N E a :
     a  nclose N  E 
     φ a ={E}=>  γ, auth_ctx γ N φ  auth_own γ a.
  Proof.
77 78
    iIntros {??} "Hφ".
    iPvs (auth_alloc_strong N E a  with "Hφ") as {γ} "[_ ?]"; [done..|].
79
    by iExists γ.
80 81
  Qed.

82
  Lemma auth_empty γ E : True ={E}=> auth_own γ .
83
  Proof. by rewrite -own_empty. Qed.
84

85 86
  Context {V} (fsa : FSA Λ (globalF Σ) V) `{!FrameShiftAssertion fsaV fsa}.

87 88
  Lemma auth_fsa E N (Ψ : V  iPropG Λ Σ) γ a :
    fsaV  nclose N  E 
89 90 91 92
    auth_ctx γ N φ   auth_own γ a  ( af,
        (a  af)   φ (a  af) -
      fsa (E  nclose N) (λ x,  b,
         (a ~l~> b @ Some af)   φ (b  af)  (auth_own γ b - Ψ x)))
93
      fsa E Ψ.
Ralf Jung's avatar
Ralf Jung committed
94
  Proof.
95 96 97
    iIntros {??} "(#? & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
    iInv N as {a'} "[Hγ Hφ]".
    iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
98
    iDestruct (own_valid _ with "#Hγ") as "Hvalid".
99
    iDestruct (auth_validI _ with "Hvalid") as "[Ha' %]"; simpl; iClear "Hvalid".
100
    iDestruct "Ha'" as {af} "Ha'"; iDestruct "Ha'" as %Ha'.
101 102 103
    rewrite ->(left_id _ _) in Ha'; setoid_subst.
    iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ".
    { iApply "HΨ"; by iSplit. }
104
    iIntros {v}; iDestruct 1 as {b} "(% & Hφ & HΨ)".
105
    iPvs (own_update _ with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto.
106
    iPvsIntro. iSplitL "Hφ Hγ"; last by iApply "HΨ".
107
    iNext. iExists (b  af). by iFrame.
108
  Qed.
109
End auth.