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

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

18 19 20 21 22 23 24 25 26 27 28
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.
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
  Global Instance auth_ctx_persistent N φ : Persistent (auth_ctx N φ).
34 35
  Proof. apply _. Qed.
End definitions.
Ralf Jung's avatar
Ralf Jung committed
36

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

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

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

56
  Lemma auth_alloc N E a :
57
     a  nclose N  E 
58
     φ a  (|={E}=>  γ, auth_ctx γ N φ  auth_own γ a).
59
  Proof.
60
    intros Ha HN. eapply sep_elim_True_r.
61 62
    { by eapply (own_alloc (Auth (Excl a) a) E). }
    rewrite pvs_frame_l. apply pvs_strip_pvs.
63
    rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
64
    trans ( auth_inv γ φ  auth_own γ a)%I.
65
    { rewrite /auth_inv -(exist_intro a) later_sep.
Ralf Jung's avatar
Ralf Jung committed
66
      ecancel [ φ _]%I.
67
      by rewrite -later_intro -own_op auth_both_op. }
68
    rewrite (inv_alloc N E) // /auth_ctx pvs_frame_r. apply pvs_mono.
69
    by rewrite always_and_sep_l.
70 71
  Qed.

72
  Lemma auth_empty γ E : True  |={E}=> auth_own γ .
73
  Proof. by rewrite -own_empty. Qed.
74

75
  Lemma auth_opened E γ a :
76
    ( auth_inv γ φ  auth_own γ a)
77
     (|={E}=>  a',  (a  a')   φ (a  a')  own γ ( (a  a')   a)).
Ralf Jung's avatar
Ralf Jung committed
78
  Proof.
79
    rewrite /auth_inv. rewrite later_exist sep_exist_r. apply exist_elim=>b.
Ralf Jung's avatar
Ralf Jung committed
80 81
    rewrite later_sep [( own _ _)%I]pvs_timeless !pvs_frame_r. apply pvs_mono.
    rewrite own_valid_l discrete_valid -!assoc. apply const_elim_sep_l=>Hv.
82
    rewrite [(▷φ _  _)%I]comm assoc -own_op.
83 84
    rewrite own_valid_r auth_validI /= and_elim_l sep_exist_l sep_exist_r /=.
    apply exist_elim=>a'.
85
    rewrite left_id -(exist_intro a').
86 87
    apply (eq_rewrite b (a  a') (λ x,  x   φ x  own γ ( x   a))%I).
    { by move=>n x y /timeless_iff ->. }
88
    { by eauto with I. }
Ralf Jung's avatar
Ralf Jung committed
89 90
    rewrite -valid_intro; last by apply Hv.
    rewrite left_id comm. auto with I.
Ralf Jung's avatar
Ralf Jung committed
91
  Qed.
Ralf Jung's avatar
Ralf Jung committed
92

93
  Lemma auth_closing `{!LocalUpdate Lv L} E γ a a' :
94
    Lv a   (L a  a') 
95
    ( φ (L a  a')  own γ ( (a  a')   a))
96
     (|={E}=>  auth_inv γ φ  auth_own γ (L a)).
Ralf Jung's avatar
Ralf Jung committed
97
  Proof.
98
    intros HL Hv. rewrite /auth_inv -(exist_intro (L a  a')).
Ralf Jung's avatar
Ralf Jung committed
99
    (* TODO it would be really nice to use cancel here *)
100
    rewrite later_sep [(_  ▷φ _)%I]comm -assoc.
101
    rewrite -pvs_frame_l. apply sep_mono_r.
Ralf Jung's avatar
Ralf Jung committed
102
    rewrite -later_intro -own_op.
103
    by apply own_update, (auth_local_update_l L).
Ralf Jung's avatar
Ralf Jung committed
104 105
  Qed.

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

108
  Lemma auth_fsa E N P (Ψ : V  iPropG Λ Σ) γ a :
109
    fsaV 
Ralf Jung's avatar
Ralf Jung committed
110
    nclose N  E 
111 112
    P  auth_ctx γ N φ 
    P  ( auth_own γ a   a',
113
            (a  a')   φ (a  a') -
114 115
          fsa (E  nclose N) (λ x,  L Lv (Hup : LocalUpdate Lv L),
             (Lv a   (L a  a'))   φ (L a  a') 
116
            (auth_own γ (L a) - Ψ x))) 
117
    P  fsa E Ψ.
Ralf Jung's avatar
Ralf Jung committed
118
  Proof.
119
    rewrite /auth_ctx=>? HN Hinv Hinner.
120
    eapply (inv_fsa fsa); eauto. rewrite Hinner=>{Hinner Hinv P HN}.
121
    apply wand_intro_l. rewrite assoc.
122 123
    rewrite (pvs_timeless (E  N)) pvs_frame_l pvs_frame_r.
    apply (fsa_strip_pvs fsa).
124
    rewrite (auth_opened (E  N)) !pvs_frame_r !sep_exist_r.
125
    apply (fsa_strip_pvs fsa). apply exist_elim=>a'.
126
    rewrite (forall_elim a'). rewrite [(_  _)%I]comm.
127
    eapply wand_apply_r; first (by eapply (wand_frame_l (own γ _))); last first.
128
    { rewrite assoc [(_  own _ _)%I]comm -assoc discrete_valid.  done. }
129
    rewrite fsa_frame_l.
Ralf Jung's avatar
Ralf Jung committed
130
    apply (fsa_mono_pvs fsa)=> x.
131 132 133
    rewrite sep_exist_l; apply exist_elim=> L.
    rewrite sep_exist_l; apply exist_elim=> Lv.
    rewrite sep_exist_l; apply exist_elim=> ?.
134
    rewrite comm -!assoc. apply const_elim_sep_l=>-[HL Hv].
135
    rewrite assoc [(_  (_ - _))%I]comm -assoc.
136 137
    rewrite (auth_closing (E  N)) //; [].
    rewrite pvs_frame_l. apply pvs_mono.
138
    by rewrite assoc [(_  _)%I]comm -assoc wand_elim_l.
Ralf Jung's avatar
Ralf Jung committed
139
  Qed.
140
  Lemma auth_fsa' L `{!LocalUpdate Lv L} E N P (Ψ : V  iPropG Λ Σ) γ a :
141 142
    fsaV 
    nclose N  E 
143 144
    P  auth_ctx γ N φ 
    P  ( auth_own γ a  ( a',
145
            (a  a')   φ (a  a') -
146 147
          fsa (E  nclose N) (λ x,
             (Lv a   (L a  a'))   φ (L a  a') 
148
            (auth_own γ (L a) - Ψ x)))) 
149
    P  fsa E Ψ.
150 151
  Proof.
    intros ??? HP. eapply auth_fsa with N γ a; eauto.
Ralf Jung's avatar
Ralf Jung committed
152
    rewrite HP; apply sep_mono_r, forall_mono=> a'.
153 154 155
    apply wand_mono; first done. apply (fsa_mono fsa)=> b.
    rewrite -(exist_intro L). by repeat erewrite <-exist_intro by apply _.
  Qed.
156
End auth.