auth.v 4.08 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
Require Export algebra.auth algebra.functor.
2
Require Export program_logic.invariants program_logic.ghost_ownership.
3
Import uPred.
4 5

Section auth.
6
  Context {A : cmraT} `{Empty A, !CMRAIdentity A} `{! a : A, Timeless a}.
7 8
  Context {Λ : language} {Σ : iFunctorG} (AuthI : gid) `{!InG Λ Σ AuthI (authRA A)}.
  Context (N : namespace) (φ : A  iPropG Λ Σ).
9

10
  Implicit Types P Q R : iPropG Λ Σ.
11 12 13 14 15
  Implicit Types a b : A.
  Implicit Types γ : gname.

  (* TODO: Need this to be proven somewhere. *)
  Hypothesis auth_valid :
16
    forall a b, ( Auth (Excl a) b : iPropG Λ Σ)  ( b', a  b  b').
17

18
  Definition auth_inv (γ : gname) : iPropG Λ Σ :=
19
    ( a, own AuthI γ ( a)  φ a)%I.
20 21
  Definition auth_own (γ : gname) (a : A) : iPropG Λ Σ := own AuthI γ ( a).
  Definition auth_ctx (γ : gname) : iPropG Λ Σ := inv N (auth_inv γ).
22 23 24

  Lemma auth_alloc a :
    a  φ a  pvs N N ( γ, auth_ctx γ  auth_own γ a).
25
  Proof.
26 27 28 29 30 31
    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 γ).
    transitivity (auth_inv γ  auth_own γ a)%I.
    { rewrite /auth_inv -later_intro -(exist_intro a).
32
      rewrite [(_  φ _)%I]comm -assoc. apply sep_mono; first done.
33 34
      rewrite /auth_own -own_op auth_both_op. done. }
    rewrite (inv_alloc N) /auth_ctx pvs_frame_r. apply pvs_mono.
35
    by rewrite always_and_sep_l.
36 37
  Qed.

38 39 40 41
  Lemma auth_empty γ E :
    True  pvs E E (auth_own γ ).
  Proof. by rewrite own_update_empty /auth_own. Qed.

Ralf Jung's avatar
Ralf Jung committed
42 43
  Context {Hφ :  n, Proper (dist n ==> dist n) φ}.

44 45
  Lemma auth_opened E a γ :
    (auth_inv γ  auth_own γ a)  pvs E E ( a', ▷φ (a  a')  own AuthI γ ( (a  a')   a)).
Ralf Jung's avatar
Ralf Jung committed
46
  Proof.
47 48
    rewrite /auth_inv. rewrite later_exist sep_exist_r. apply exist_elim=>b.
    rewrite later_sep [(own _ _ _)%I]pvs_timeless !pvs_frame_r. apply pvs_mono.
49
    rewrite /auth_own [(_  ▷φ _)%I]comm -assoc -own_op.
50 51
    rewrite own_valid_r auth_valid !sep_exist_l /=. apply exist_elim=>a'.
    rewrite [  _]left_id -(exist_intro a').
Ralf Jung's avatar
Ralf Jung committed
52
    apply (eq_rewrite b (a  a')
53
              (λ x, ▷φ x  own AuthI γ ( x   a))%I); first by solve_ne.
Ralf Jung's avatar
Ralf Jung committed
54 55 56 57
    { by rewrite !sep_elim_r. }
    apply sep_mono; first done.
    by rewrite sep_elim_l.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
58

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

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