auth.v 6.22 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From algebra Require Export auth.
2
From program_logic Require Export invariants ghost_ownership.
3
Import uPred.
4

5
6
7
8
9
10
Class AuthInG Λ Σ (i : gid) (A : cmraT) `{Empty A} := {
  auth_inG :> InG Λ Σ i (authRA A);
  auth_identity :> CMRAIdentity A;
  auth_timeless (a : A) :> Timeless a;
}.

11
12
(* TODO: Once we switched to RAs, it is no longer necessary to remember that a is
   constantly valid. *)
13
14
15
16
17
18
19
20
Section definitions.
  Context {Λ Σ A} (i : gid) `{AuthInG Λ Σ i A} (γ : gname).
  Definition auth_inv (φ : A  iPropG Λ Σ) : iPropG Λ Σ :=
    ( a, (  a  own i γ ( a))  φ a)%I.
  Definition auth_own (a : A) : iPropG Λ Σ := own i γ ( a).
  Definition auth_ctx (N : namespace) (φ : A  iPropG Λ Σ) : iPropG Λ Σ :=
    inv N (auth_inv φ).
End definitions.
21
22
23
Instance: Params (@auth_inv) 7.
Instance: Params (@auth_own) 7.
Instance: Params (@auth_ctx) 8.
24

25
Section auth.
26
  Context `{AuthInG Λ Σ AuthI A}.
27
  Context (φ : A  iPropG Λ Σ) {φ_proper : Proper (() ==> ()) φ}.
28
  Implicit Types N : namespace.
29
  Implicit Types P Q R : iPropG Λ Σ.
30
31
32
  Implicit Types a b : A.
  Implicit Types γ : gname.

33
34
35
36
37
  Global Instance auth_own_ne n γ :
    Proper (dist n ==> dist n) (auth_own AuthI γ).
  Proof. by rewrite /auth_own=> a b ->. Qed.
  Global Instance auth_own_proper γ : Proper (() ==> ()) (auth_own AuthI γ).
  Proof. by rewrite /auth_own=> a b ->. Qed.
38
39
40
  Lemma auto_own_op γ a b :
    auth_own AuthI γ (a  b)  (auth_own AuthI γ a  auth_own AuthI γ b)%I.
  Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
41
42
  Lemma auto_own_valid γ a : auth_own AuthI γ a   a.
  Proof. by rewrite /auth_own own_valid auth_validI. Qed.
43

44
45
  Lemma auth_alloc N a :
     a  φ a  pvs N N ( γ, auth_ctx AuthI γ N φ  auth_own AuthI γ a).
46
  Proof.
47
48
    intros Ha. eapply sep_elim_True_r.
    { by eapply (own_alloc AuthI (Auth (Excl a) a) N). }
49
50
    rewrite pvs_frame_l. apply pvs_strip_pvs.
    rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
51
    transitivity ( auth_inv AuthI γ φ  auth_own AuthI γ a)%I.
52
    { rewrite /auth_inv -later_intro -(exist_intro a).
53
      rewrite const_equiv // left_id.
54
      rewrite [(_  φ _)%I]comm -assoc. apply sep_mono; first done.
55
56
      rewrite /auth_own -own_op auth_both_op. done. }
    rewrite (inv_alloc N) /auth_ctx pvs_frame_r. apply pvs_mono.
57
    by rewrite always_and_sep_l.
58
59
  Qed.

60
  Lemma auth_empty E γ : True  pvs E E (auth_own AuthI γ ).
61
62
  Proof. by rewrite own_update_empty /auth_own. Qed.

63
  Lemma auth_opened E γ a :
64
    ( auth_inv AuthI γ φ  auth_own AuthI γ a)
65
     pvs E E ( a',   (a  a')   φ (a  a')  own AuthI γ ( (a  a')   a)).
Ralf Jung's avatar
Ralf Jung committed
66
  Proof.
67
    rewrite /auth_inv. rewrite later_exist sep_exist_r. apply exist_elim=>b.
68
69
70
    rewrite later_sep [((_  _))%I]pvs_timeless !pvs_frame_r. apply pvs_mono.
    rewrite always_and_sep_l -!assoc. apply const_elim_sep_l=>Hv.
    rewrite /auth_own [(▷φ _  _)%I]comm assoc -own_op.
71
72
    rewrite own_valid_r auth_validI /= and_elim_l sep_exist_l sep_exist_r /=.
    apply exist_elim=>a'.
73
    rewrite left_id -(exist_intro a').
74
    apply (eq_rewrite b (a  a') (λ x, ■✓x  ▷φ x  own AuthI γ ( x   a))%I).
75
    { by move=>n ? ? /timeless_iff ->. }
76
    { by eauto with I. }
77
    rewrite const_equiv // left_id comm.
Ralf Jung's avatar
Ralf Jung committed
78
79
80
    apply sep_mono; first done.
    by rewrite sep_elim_l.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
81

82
  Lemma auth_closing `{!LocalUpdate Lv L} E γ a a' :
83
    Lv a   (L a  a') 
84
    ( φ (L a  a')  own AuthI γ ( (a  a')   a))
85
     pvs E E ( auth_inv AuthI γ φ  auth_own AuthI γ (L a)).
Ralf Jung's avatar
Ralf Jung committed
86
  Proof.
87
    intros HL Hv. rewrite /auth_inv /auth_own -(exist_intro (L a  a')).
88
    rewrite later_sep [(_  ▷φ _)%I]comm -assoc.
Ralf Jung's avatar
Ralf Jung committed
89
    rewrite -pvs_frame_l. apply sep_mono; first done.
90
    rewrite const_equiv // left_id -later_intro -own_op.
91
    by apply own_update, (auth_local_update_l L).
Ralf Jung's avatar
Ralf Jung committed
92
93
  Qed.

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

96
  (* Notice how the user has to prove that `b⋅a'` is valid at all
97
     step-indices. However, since A is timeless, that should not be
98
99
     a restriction. *)
  Lemma auth_fsa E N P (Q : V  iPropG Λ Σ) γ a :
100
    fsaV 
Ralf Jung's avatar
Ralf Jung committed
101
    nclose N  E 
102
    P  auth_ctx AuthI γ N φ 
103
    P  (auth_own AuthI γ a   a',
104
            (a  a')   φ (a  a') -
105
106
107
          fsa (E  nclose N) (λ x,  L Lv (Hup : LocalUpdate Lv L),
             (Lv a   (L a  a'))   φ (L a  a') 
            (auth_own AuthI γ (L a) - Q x))) 
108
    P  fsa E Q.
Ralf Jung's avatar
Ralf Jung committed
109
  Proof.
110
    rewrite /auth_ctx=>? HN Hinv Hinner.
111
    eapply (inv_fsa fsa); eauto. rewrite Hinner=>{Hinner Hinv P HN}.
112
113
    apply wand_intro_l. rewrite assoc.
    rewrite (auth_opened (E  N)) !pvs_frame_r !sep_exist_r.
114
    apply (fsa_strip_pvs fsa). apply exist_elim=>a'.
115
    rewrite (forall_elim a'). rewrite [(_  _)%I]comm.
116
117
118
    (* Getting this wand eliminated is really annoying. *)
    rewrite [(_  _)%I]comm -!assoc [(▷φ _  _  _)%I]assoc [(▷φ _  _)%I]comm.
    rewrite wand_elim_r fsa_frame_l.
Ralf Jung's avatar
Ralf Jung committed
119
    apply (fsa_mono_pvs fsa)=> x.
120
121
122
    rewrite sep_exist_l; apply exist_elim=> L.
    rewrite sep_exist_l; apply exist_elim=> Lv.
    rewrite sep_exist_l; apply exist_elim=> ?.
123
    rewrite comm -!assoc. apply const_elim_sep_l=>-[HL Hv].
124
    rewrite assoc [(_  (_ - _))%I]comm -assoc.
125
126
    rewrite (auth_closing (E  N)) //; [].
    rewrite pvs_frame_l. apply pvs_mono.
127
    by rewrite assoc [(_  _)%I]comm -assoc wand_elim_l.
Ralf Jung's avatar
Ralf Jung committed
128
  Qed.
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
  Lemma auth_fsa' L `{!LocalUpdate Lv L} E N P (Q: V  iPropG Λ Σ) γ a :
    fsaV 
    nclose N  E 
    P  auth_ctx AuthI γ N φ 
    P  (auth_own AuthI γ a  ( a',
            (a  a')   φ (a  a') -
          fsa (E  nclose N) (λ x,
             (Lv a   (L a  a'))   φ (L a  a') 
            (auth_own AuthI γ (L a) - Q x)))) 
    P  fsa E Q.
  Proof.
    intros ??? HP. eapply auth_fsa with N γ a; eauto.
    rewrite HP; apply sep_mono; first done; apply forall_mono=> a'.
    apply wand_mono; first done. apply (fsa_mono fsa)=> b.
    rewrite -(exist_intro L). by repeat erewrite <-exist_intro by apply _.
  Qed.
145
End auth.