auth.v 6.99 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From algebra Require Export auth upred_tactics.
2
From program_logic Require Export invariants global_functor.
3
Import uPred.
4

5
6
Class authG Λ Σ (A : cmraT) `{Empty A} := AuthG {
  auth_inG :> inG Λ Σ (authRA A);
7
  auth_identity :> CMRAIdentity A;
Ralf Jung's avatar
Ralf Jung committed
8
  (* TODO: Once we switched to RAs, this can be removed. *)
9
10
11
  auth_timeless (a : A) :> Timeless a;
}.

12
13
14
15
Definition authGF (A : cmraT) : iFunctor := constF (authRA A).
Instance authGF_inGF (A : cmraT) `{inGF Λ Σ (authGF A)}
  `{CMRAIdentity A,  a : A, Timeless a} : authG Λ Σ A.
Proof. split; try apply _. apply: inGF_inG. Qed.
16

Ralf Jung's avatar
Ralf Jung committed
17
18
19
20
21
22
23
24
25
26
27
28
29
Definition auth_own_def `{authG Λ Σ A} (γ : gname) (a : A) : iPropG Λ Σ :=
  own γ ( a).
(* Perform sealing *)
Module Type AuthOwnSig.
  Parameter auth_own :  `{authG Λ Σ A} (γ : gname) (a : A), iPropG Λ Σ.
  Axiom auth_own_eq : @auth_own = @auth_own_def.
End AuthOwnSig.
Module Export AuthOwn : AuthOwnSig.
  Definition auth_own := @auth_own_def.
  Definition auth_own_eq := Logic.eq_refl (@auth_own).
End AuthOwn. 

(* TODO: Once we switched to RAs, it is no longer necessary to remember that a
Ralf Jung's avatar
Ralf Jung committed
30
     is constantly valid. *)
Ralf Jung's avatar
Ralf Jung committed
31
32
33
34
35
Definition auth_inv`{authG Λ Σ A} (γ : gname) (φ : A  iPropG Λ Σ) : iPropG Λ Σ :=
  ( a, (  a  own γ ( a))  φ a)%I.
Definition auth_ctx`{authG Λ Σ A} (γ : gname) (N : namespace) (φ : A  iPropG Λ Σ) : iPropG Λ Σ :=
  inv N (auth_inv γ φ).

36
37
38
Instance: Params (@auth_inv) 6.
Instance: Params (@auth_own) 6.
Instance: Params (@auth_ctx) 7.
39

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

48
  Global Instance auth_own_ne n γ : Proper (dist n ==> dist n) (auth_own γ).
Ralf Jung's avatar
Ralf Jung committed
49
  Proof. by rewrite auth_own_eq /auth_own_def=> a b ->. Qed.
50
  Global Instance auth_own_proper γ : Proper (() ==> ()) (auth_own γ).
Ralf Jung's avatar
Ralf Jung committed
51
52
53
54
  Proof. by rewrite auth_own_eq /auth_own_def=> a b ->. Qed.
  Global Instance auth_own_timeless γ a : TimelessP (auth_own γ a).
  Proof. rewrite auth_own_eq. apply _. Qed.

Ralf Jung's avatar
Ralf Jung committed
55
  Lemma auth_own_op γ a b :
56
    auth_own γ (a  b)  (auth_own γ a  auth_own γ b)%I.
Ralf Jung's avatar
Ralf Jung committed
57
  Proof. by rewrite auth_own_eq /auth_own_def -own_op auth_frag_op. Qed.
Ralf Jung's avatar
Ralf Jung committed
58
  Lemma auth_own_valid γ a : auth_own γ a   a.
Ralf Jung's avatar
Ralf Jung committed
59
  Proof. by rewrite auth_own_eq /auth_own_def own_valid auth_validI. Qed.
60

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

77
  Lemma auth_empty γ E : True  (|={E}=> auth_own γ ).
Ralf Jung's avatar
Ralf Jung committed
78
  Proof. by rewrite auth_own_eq -own_update_empty. Qed.
79

80
  Lemma auth_opened E γ a :
81
    ( auth_inv γ φ  auth_own γ a)
82
     (|={E}=>  a',   (a  a')   φ (a  a')  own γ ( (a  a')   a)).
Ralf Jung's avatar
Ralf Jung committed
83
  Proof.
84
    rewrite /auth_inv. rewrite later_exist sep_exist_r. apply exist_elim=>b.
85
86
    rewrite later_sep [((_  _))%I]pvs_timeless !pvs_frame_r. apply pvs_mono.
    rewrite always_and_sep_l -!assoc. apply const_elim_sep_l=>Hv.
Ralf Jung's avatar
Ralf Jung committed
87
    rewrite auth_own_eq [(▷φ _  _)%I]comm assoc -own_op.
88
89
    rewrite own_valid_r auth_validI /= and_elim_l sep_exist_l sep_exist_r /=.
    apply exist_elim=>a'.
90
    rewrite left_id -(exist_intro a').
91
    apply (eq_rewrite b (a  a') (λ x,   x   φ x  own γ ( x   a))%I).
92
    { by move=>n ? ? /timeless_iff ->. }
93
    { by eauto with I. }
94
    rewrite const_equiv // left_id comm.
Ralf Jung's avatar
Ralf Jung committed
95
    apply sep_mono_r. by rewrite sep_elim_l.
Ralf Jung's avatar
Ralf Jung committed
96
  Qed.
Ralf Jung's avatar
Ralf Jung committed
97

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

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

113
  (* Notice how the user has to prove that `b⋅a'` is valid at all
114
     step-indices. However, since A is timeless, that should not be
115
     a restriction. *)
116
  Lemma auth_fsa E N P (Ψ : V  iPropG Λ Σ) γ a :
117
    fsaV 
Ralf Jung's avatar
Ralf Jung committed
118
    nclose N  E 
119
120
    P  auth_ctx γ N φ 
    P  ( auth_own γ a   a',
121
            (a  a')   φ (a  a') -
122
123
          fsa (E  nclose N) (λ x,  L Lv (Hup : LocalUpdate Lv L),
             (Lv a   (L a  a'))   φ (L a  a') 
124
125
            (auth_own γ (L a) - Ψ x))) 
    P  fsa E Ψ.
Ralf Jung's avatar
Ralf Jung committed
126
  Proof.
127
    rewrite /auth_ctx=>? HN Hinv Hinner.
128
    eapply (inv_fsa fsa); eauto. rewrite Hinner=>{Hinner Hinv P HN}.
129
    apply wand_intro_l. rewrite assoc.
130
131
    rewrite (pvs_timeless (E  N)) pvs_frame_l pvs_frame_r.
    apply (fsa_strip_pvs fsa).
132
    rewrite (auth_opened (E  N)) !pvs_frame_r !sep_exist_r.
133
    apply (fsa_strip_pvs fsa). apply exist_elim=>a'.
134
    rewrite (forall_elim a'). rewrite [(_  _)%I]comm.
135
136
137
    eapply wand_apply_r; first (by eapply (wand_frame_l (own γ _))); last first.
    { rewrite assoc [(_  own _ _)%I]comm -assoc. done. }
    rewrite fsa_frame_l.
Ralf Jung's avatar
Ralf Jung committed
138
    apply (fsa_mono_pvs fsa)=> x.
139
140
141
    rewrite sep_exist_l; apply exist_elim=> L.
    rewrite sep_exist_l; apply exist_elim=> Lv.
    rewrite sep_exist_l; apply exist_elim=> ?.
142
    rewrite comm -!assoc. apply const_elim_sep_l=>-[HL Hv].
143
    rewrite assoc [(_  (_ - _))%I]comm -assoc.
144
145
    rewrite (auth_closing (E  N)) //; [].
    rewrite pvs_frame_l. apply pvs_mono.
146
    by rewrite assoc [(_  _)%I]comm -assoc wand_elim_l.
Ralf Jung's avatar
Ralf Jung committed
147
  Qed.
148
  Lemma auth_fsa' L `{!LocalUpdate Lv L} E N P (Ψ : V  iPropG Λ Σ) γ a :
149
150
    fsaV 
    nclose N  E 
151
152
    P  auth_ctx γ N φ 
    P  ( auth_own γ a  ( a',
153
154
155
            (a  a')   φ (a  a') -
          fsa (E  nclose N) (λ x,
             (Lv a   (L a  a'))   φ (L a  a') 
156
157
            (auth_own γ (L a) - Ψ x)))) 
    P  fsa E Ψ.
158
159
  Proof.
    intros ??? HP. eapply auth_fsa with N γ a; eauto.
Ralf Jung's avatar
Ralf Jung committed
160
    rewrite HP; apply sep_mono_r, forall_mono=> a'.
161
162
163
    apply wand_mono; first done. apply (fsa_mono fsa)=> b.
    rewrite -(exist_intro L). by repeat erewrite <-exist_intro by apply _.
  Qed.
164
End auth.