auth.v 4.24 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
11
12
13
14
15
16
17
18
19
20
21
Class AuthInG Λ Σ (i : gid) (A : cmraT) `{Empty A} := {
  auth_inG :> InG Λ Σ i (authRA A);
  auth_identity :> CMRAIdentity A;
  auth_timeless (a : A) :> Timeless a;
}.

Definition auth_inv {Λ Σ A} (i : gid) `{AuthInG Λ Σ i A}
  (γ : gname) (φ : A  iPropG Λ Σ) : iPropG Λ Σ := ( a, own i γ ( a)  φ a)%I.
Definition auth_own {Λ Σ A} (i : gid) `{AuthInG Λ Σ i A}
  (γ : gname) (a : A) : iPropG Λ Σ := own i γ ( a).
Definition auth_ctx {Λ Σ A} (i : gid) `{AuthInG Λ Σ i A}
    (γ : gname) (N : namespace) (φ : A  iPropG Λ Σ) : iPropG Λ Σ :=
  inv N (auth_inv i γ φ).
Instance: Params (@auth_inv) 7.
Instance: Params (@auth_own) 7.
Instance: Params (@auth_ctx) 8.

22
Section auth.
23
  Context `{AuthInG Λ Σ AuthI A}.
24
  Context (φ : A  iPropG Λ Σ) {Hφ :  n, Proper (dist n ==> dist n) φ}.
25
  Implicit Types N : namespace.
26
  Implicit Types P Q R : iPropG Λ Σ.
27
28
29
  Implicit Types a b : A.
  Implicit Types γ : gname.

30
31
  Lemma auth_alloc N a :
     a  φ a  pvs N N ( γ, auth_ctx AuthI γ N φ  auth_own AuthI γ a).
32
  Proof.
33
34
35
36
    intros Ha. rewrite -(right_id True%I ()%I (φ _)).
    rewrite (own_alloc AuthI (Auth (Excl a) a) N) //; [].
    rewrite pvs_frame_l. apply pvs_strip_pvs.
    rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
37
    transitivity ( auth_inv AuthI γ φ  auth_own AuthI γ a)%I.
38
    { rewrite /auth_inv -later_intro -(exist_intro a).
39
      by rewrite [(_  φ _)%I]comm -assoc /auth_own -own_op auth_both_op. }
40
    rewrite (inv_alloc N) /auth_ctx pvs_frame_r. apply pvs_mono.
41
    by rewrite always_and_sep_l.
42
43
  Qed.

44
  Lemma auth_empty γ E : True  pvs E E (auth_own AuthI γ ).
45
46
  Proof. by rewrite own_update_empty /auth_own. Qed.

47
  Lemma auth_opened E a γ :
48
49
    ( auth_inv AuthI γ φ  auth_own AuthI γ a)
     pvs E E ( a',  φ (a  a')  own AuthI γ ( (a  a')   a)).
Ralf Jung's avatar
Ralf Jung committed
50
  Proof.
51
52
53
    rewrite /auth_inv later_exist sep_exist_r. apply exist_elim=>b.
    rewrite later_sep [( own _ _ _)%I]pvs_timeless !pvs_frame_r. apply pvs_mono.
    rewrite /auth_own [(_   φ _)%I]comm -assoc -own_op.
54
    rewrite own_valid_r auth_validI /= and_elim_l !sep_exist_l /=.
55
56
57
58
    apply exist_elim=> a'.
    rewrite left_id -(exist_intro a').
    apply (eq_rewrite b (a  a') (λ x,
       φ x  own AuthI γ ( x   a))%I); [solve_ne| |]; auto with I.
Ralf Jung's avatar
Ralf Jung committed
59
  Qed.
Ralf Jung's avatar
Ralf Jung committed
60

61
62
  Lemma auth_closing E `{!LocalUpdate Lv L} a a' γ :
    Lv a   (L a  a') 
63
    ( φ (L a  a')  own AuthI γ ( (a  a')   a))
64
     pvs E E ( auth_inv AuthI γ φ  auth_own AuthI γ (L a)).
Ralf Jung's avatar
Ralf Jung committed
65
  Proof.
66
    intros HL Hv. rewrite /auth_inv /auth_own -(exist_intro (L a  a')).
67
    rewrite later_sep [(_  ▷φ _)%I]comm -assoc.
Ralf Jung's avatar
Ralf Jung committed
68
    rewrite -pvs_frame_l. apply sep_mono; first done.
69
70
    rewrite -later_intro -own_op.
    by apply own_update, (auth_local_update_l L).
Ralf Jung's avatar
Ralf Jung committed
71
72
  Qed.

73
  (* Notice how the user has to prove that `b⋅a'` is valid at all
74
75
     step-indices. However, since A is timeless, that should not be
     a restriction.  *)
76
  Lemma auth_fsa {X : Type} {FSA} (FSAs : FrameShiftAssertion (A:=X) FSA)
77
        `{!LocalUpdate Lv L} N E P (Q : X  iPropG Λ Σ) R γ a :
Ralf Jung's avatar
Ralf Jung committed
78
    nclose N  E 
79
80
81
82
    R  auth_ctx AuthI γ N φ 
    R  (auth_own AuthI γ a   a', ▷φ (a  a') - FSA (E  nclose N) (λ x,
           (Lv a   (L a  a')) 
           φ (L a  a')  (auth_own AuthI γ (L a) - Q x))) 
83
    R  FSA E Q.
Ralf Jung's avatar
Ralf Jung committed
84
  Proof.
85
86
87
    rewrite /auth_ctx=>HN Hinv Hinner.
    eapply inv_fsa; [eassumption..|]. rewrite Hinner=>{Hinner Hinv R}.
    apply wand_intro_l.
88
    rewrite assoc auth_opened !pvs_frame_r !sep_exist_r.
89
    apply fsa_strip_pvs; first done. apply exist_elim=>a'.
90
91
92
    rewrite (forall_elim a'). rewrite [(_  _)%I]comm.
    rewrite -[((_  _)  _)%I]assoc wand_elim_r fsa_frame_l.
    apply fsa_mono_pvs; first done. intros x. rewrite comm -!assoc.
93
    apply const_elim_sep_l=>-[HL Hv].
94
    rewrite assoc [(_  (_ - _))%I]comm -assoc.
95
    rewrite auth_closing //; []. erewrite pvs_frame_l. apply pvs_mono.
96
    by rewrite assoc [(_  _)%I]comm -assoc wand_elim_l.
Ralf Jung's avatar
Ralf Jung committed
97
  Qed.
98
End auth.