auth.v 4.56 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 59 60 61

  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.

62 63 64 65
  Global Instance auth_own_persistent γ a :
    Persistent a  PersistentP (auth_own γ a).
  Proof. rewrite /auth_own. apply _. Qed.

66
  Lemma auth_own_valid γ a : auth_own γ a   a.
67
  Proof. by rewrite /auth_own own_valid auth_validI. Qed.
68

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

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

90
  Lemma auth_empty γ E : True ={E}=> auth_own γ .
91
  Proof. by rewrite -own_empty. Qed.
92

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

95 96
  Lemma auth_fsa E N (Ψ : V  iPropG Λ Σ) γ a :
    fsaV  nclose N  E 
97 98 99 100
    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)))
101
      fsa E Ψ.
Ralf Jung's avatar
Ralf Jung committed
102
  Proof.
103 104
    iIntros (??) "(#? & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
    iInv N as (a') "[Hγ Hφ]".
105
    iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
106
    iDestruct (own_valid with "#Hγ") as "Hvalid".
107
    iDestruct (auth_validI _ with "Hvalid") as "[Ha' %]"; simpl; iClear "Hvalid".
108
    iDestruct "Ha'" as (af) "Ha'"; iDestruct "Ha'" as %Ha'.
109 110 111
    rewrite ->(left_id _ _) in Ha'; setoid_subst.
    iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ".
    { iApply "HΨ"; by iSplit. }
112
    iIntros (v); iDestruct 1 as (b) "(% & Hφ & HΨ)".
113
    iPvs (own_update with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto.
114
    iPvsIntro. iSplitL "Hφ Hγ"; last by iApply "HΨ".
115
    iNext. iExists (b  af). by iFrame.
116
  Qed.
117
End auth.