auth.v 4.45 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 : cmraT) `{Empty A} := AuthG {
8
  auth_inG :> inG Λ Σ (authR A);
Ralf Jung's avatar
Ralf Jung committed
9
  auth_identity :> CMRAUnit A;
10
  auth_timeless :> CMRADiscrete A;
11
}.
12
(* The Functor we need. *)
13
Definition authGF (A : cmraT) : gFunctor := GFunctor (constRF (authR A)).
14
(* Show and register that they match. *)
15
Instance authGF_inGF (A : cmraT) `{inGF Λ Σ (authGF A)}
Ralf Jung's avatar
Ralf Jung committed
16
  `{CMRAUnit A, CMRADiscrete A} : authG Λ Σ A.
17
Proof. split; try apply _. apply: inGF_inG. Qed.
18

19 20 21 22 23 24 25 26 27 28 29
Section definitions.
  Context `{authG Λ Σ A} (γ : gname).
  Definition auth_own  (a : A) : iPropG Λ Σ :=
    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.
30
  Global Instance auth_own_proper : Proper (() ==> ()) auth_own.
31 32 33
  Proof. solve_proper. Qed.
  Global Instance auth_own_timeless a : TimelessP (auth_own a).
  Proof. apply _. Qed.
34
  Global Instance auth_ctx_persistent N φ : PersistentP (auth_ctx N φ).
35 36
  Proof. apply _. Qed.
End definitions.
Ralf Jung's avatar
Ralf Jung committed
37

38
Typeclasses Opaque auth_own auth_ctx.
39 40 41
Instance: Params (@auth_inv) 6.
Instance: Params (@auth_own) 6.
Instance: Params (@auth_ctx) 7.
42

43
Section auth.
44
  Context `{AuthI : authG Λ Σ A}.
45
  Context (φ : A  iPropG Λ Σ) {φ_proper : Proper (() ==> ()) φ}.
46
  Implicit Types N : namespace.
47
  Implicit Types P Q R : iPropG Λ Σ.
48 49 50
  Implicit Types a b : A.
  Implicit Types γ : gname.

Ralf Jung's avatar
Ralf Jung committed
51
  Lemma auth_own_op γ a b :
52
    auth_own γ (a  b)  (auth_own γ a  auth_own γ b).
53
  Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
54
  Lemma auth_own_valid γ a : auth_own γ a   a.
55
  Proof. by rewrite /auth_own own_valid auth_validI. Qed.
56

57
  Lemma auth_alloc N E a :
58
     a  nclose N  E 
59
     φ a  (|={E}=>  γ, auth_ctx γ N φ  auth_own γ a).
60
  Proof.
61 62 63 64 65 66
    iIntros {??} "Hφ". rewrite /auth_own /auth_ctx.
    iPvs (own_alloc (Auth (Excl a) a)) as {γ} "Hγ"; first done.
    iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
    iPvs (inv_alloc N _ (auth_inv γ φ) with "-[Hγ']"); first done.
    { iNext. iExists a. by iFrame "Hφ". }
    iPvsIntro; iExists γ; by iFrame "Hγ'".
67 68
  Qed.

69
  Lemma auth_empty γ E : True  |={E}=> auth_own γ .
70
  Proof. by rewrite -own_empty. Qed.
71

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

74 75 76 77 78 79 80 81
  Lemma auth_fsa E N (Ψ : V  iPropG Λ Σ) γ a :
    fsaV  nclose N  E 
    (auth_ctx γ N φ   auth_own γ a   a',
        (a  a')   φ (a  a') -
      fsa (E  nclose N) (λ x,  L Lv (Hup : LocalUpdate Lv L),
         (Lv a   (L a  a'))   φ (L a  a') 
        (auth_own γ (L a) - Ψ x)))
      fsa E Ψ.
Ralf Jung's avatar
Ralf Jung committed
82
  Proof.
83 84 85 86 87 88 89 90 91 92 93 94 95 96
    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γ".
    iDestruct (own_valid _ with "Hγ !") as "Hvalid".
    iDestruct (auth_validI _ with "Hvalid") as "[Ha' %]"; simpl; iClear "Hvalid".
    iDestruct "Ha'" as {b} "Ha'"; iDestruct "Ha'" as %Ha'.
    rewrite ->(left_id _ _) in Ha'; setoid_subst.
    iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ".
    { iApply "HΨ"; by iSplit. }
    iIntros {v} "HL". iDestruct "HL" as {L Lv ?} "(% & Hφ & HΨ)".
    iPvs (own_update _ with "Hγ") as "[Hγ Hγf]".
    { apply (auth_local_update_l L); tauto. }
    iPvsIntro. iSplitL "Hφ Hγ"; last by iApply "HΨ".
    iNext. iExists (L a  b). by iFrame "Hφ".
Ralf Jung's avatar
Ralf Jung committed
97
  Qed.
98 99 100 101 102 103 104 105 106

  Lemma auth_fsa' L `{!LocalUpdate Lv L} E N (Ψ : V  iPropG Λ Σ) γ a :
    fsaV  nclose N  E 
    (auth_ctx γ N φ   auth_own γ a  ( a',
        (a  a')   φ (a  a') -
      fsa (E  nclose N) (λ x,
         (Lv a   (L a  a'))   φ (L a  a') 
        (auth_own γ (L a) - Ψ x))))
     fsa E Ψ.
107
  Proof.
108 109 110 111
    iIntros {??} "(#Ha & Hγf & HΨ)"; iApply (auth_fsa E N Ψ γ a); auto.
    iFrame "Ha Hγf". iIntros {a'} "H".
    iApply fsa_wand_r; iSplitL; first by iApply "HΨ".
    iIntros {v} "?"; by iExists L, Lv, _.
112
  Qed.
113
End auth.