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

5
(** The CMRA we need. *)
6
Class stsG Λ Σ (sts : stsT) := StsG {
7
  sts_inG :> inG Λ Σ (stsR sts);
Robbert Krebbers's avatar
Robbert Krebbers committed
8
  sts_inhabited :> Inhabited (sts.state sts);
Ralf Jung's avatar
Ralf Jung committed
9
}.
10
Coercion sts_inG : stsG >-> inG.
11
(** The Functor we need. *)
12
Definition stsGF (sts : stsT) : rFunctor := constRF (stsR sts).
13
(* Show and register that they match. *)
14
Instance inGF_stsG sts `{inGF Λ Σ (stsGF sts)}
15
16
  `{Inhabited (sts.state sts)} : stsG Λ Σ sts.
Proof. split; try apply _. apply: inGF_inG. Qed.
17

18
19
20
21
22
23
24
25
26
27
Section definitions.
  Context `{i : stsG Λ Σ sts} (γ : gname).
  Definition sts_ownS (S : sts.states sts) (T : sts.tokens sts) : iPropG Λ Σ:=
    own γ (sts_frag S T).
  Definition sts_own (s : sts.state sts) (T : sts.tokens sts) : iPropG Λ Σ :=
    own γ (sts_frag_up s T).
  Definition sts_inv (φ : sts.state sts  iPropG Λ Σ) : iPropG Λ Σ :=
    ( s, own γ (sts_auth s )  φ s)%I.
  Definition sts_ctx (N : namespace) (φ: sts.state sts  iPropG Λ Σ) : iPropG Λ Σ :=
    inv N (sts_inv φ).
Ralf Jung's avatar
Ralf Jung committed
28

29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
  Global Instance sts_inv_ne n :
    Proper (pointwise_relation _ (dist n) ==> dist n) sts_inv.
  Proof. solve_proper. Qed.
  Global Instance sts_inv_proper :
    Proper (pointwise_relation _ () ==> ()) sts_inv.
  Proof. solve_proper. Qed.
  Global Instance sts_ownS_proper : Proper (() ==> () ==> ()) sts_ownS.
  Proof. solve_proper. Qed.
  Global Instance sts_own_proper s : Proper (() ==> ()) (sts_own s).
  Proof. solve_proper. Qed.
  Global Instance sts_ctx_ne n N :
    Proper (pointwise_relation _ (dist n) ==> dist n) (sts_ctx N).
  Proof. solve_proper. Qed.
  Global Instance sts_ctx_proper N :
    Proper (pointwise_relation _ () ==> ()) (sts_ctx N).
  Proof. solve_proper. Qed.
  Global Instance sts_ctx_always_stable N φ : AlwaysStable (sts_ctx N φ).
  Proof. apply _. Qed.
End definitions.
Typeclasses Opaque sts_own sts_ownS sts_ctx.
49
50
51
52
Instance: Params (@sts_inv) 5.
Instance: Params (@sts_ownS) 5.
Instance: Params (@sts_own) 6.
Instance: Params (@sts_ctx) 6.
Ralf Jung's avatar
Ralf Jung committed
53
54

Section sts.
55
  Context `{stsG Λ Σ sts} (φ : sts.state sts  iPropG Λ Σ).
Ralf Jung's avatar
Ralf Jung committed
56
57
58
  Implicit Types N : namespace.
  Implicit Types P Q R : iPropG Λ Σ.
  Implicit Types γ : gname.
Robbert Krebbers's avatar
Robbert Krebbers committed
59
60
61
62
  Implicit Types S : sts.states sts.
  Implicit Types T : sts.tokens sts.

  (** Setoids *)
Ralf Jung's avatar
Ralf Jung committed
63

64
65
  (* The same rule as implication does *not* hold, as could be shown using
     sts_frag_included. *)
Ralf Jung's avatar
Ralf Jung committed
66
  Lemma sts_ownS_weaken E γ S1 S2 T1 T2 :
67
    T2  T1  S1  S2  sts.closed S2 T2 
68
    sts_ownS γ S1 T1  (|={E}=> sts_ownS γ S2 T2).
69
  Proof. intros ? ? ?. by apply own_update, sts_update_frag. Qed.
70

Ralf Jung's avatar
Ralf Jung committed
71
  Lemma sts_own_weaken E γ s S T1 T2 :
72
    T2  T1  s  S  sts.closed S T2 
73
    sts_own γ s T1  (|={E}=> sts_ownS γ S T2).
74
  Proof. intros ???. by apply own_update, sts_update_frag_up. Qed.
75

Ralf Jung's avatar
Ralf Jung committed
76
  Lemma sts_ownS_op γ S1 S2 T1 T2 :
Ralf Jung's avatar
Ralf Jung committed
77
    T1  T2    sts.closed S1 T1  sts.closed S2 T2 
Ralf Jung's avatar
Ralf Jung committed
78
    sts_ownS γ (S1  S2) (T1  T2)  (sts_ownS γ S1 T1  sts_ownS γ S2 T2)%I.
79
  Proof. intros. by rewrite /sts_ownS -own_op sts_op_frag. Qed.
Ralf Jung's avatar
Ralf Jung committed
80

81
82
  Lemma sts_alloc E N s :
    nclose N  E 
83
     φ s  (|={E}=>  γ, sts_ctx γ N φ  sts_own γ s (  sts.tok s)).
84
  Proof.
85
    intros HN. eapply sep_elim_True_r.
86
    { apply (own_alloc (sts_auth s (  sts.tok s)) E).
87
      apply sts_auth_valid; set_solver. }
88
    rewrite pvs_frame_l. apply pvs_strip_pvs.
89
    rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
90
    trans ( sts_inv γ φ  sts_own γ s (  sts.tok s))%I.
91
    { rewrite /sts_inv -(exist_intro s) later_sep.
92
      ecancel [ φ _]%I.
93
      by rewrite -later_intro -own_op sts_op_auth_frag_up; last set_solver. }
94
    rewrite (inv_alloc N E) // /sts_ctx pvs_frame_r.
95
96
97
    by rewrite always_and_sep_l.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
98
  Lemma sts_opened E γ S T :
99
    ( sts_inv γ φ  sts_ownS γ S T)
100
     (|={E}=>  s,  (s  S)   φ s  own γ (sts_auth s T)).
101
  Proof.
102
    rewrite /sts_inv later_exist sep_exist_r. apply exist_elim=>s.
103
    rewrite later_sep pvs_timeless !pvs_frame_r. apply pvs_mono.
104
105
106
    rewrite -(exist_intro s). ecancel [ φ _]%I.
    rewrite -own_op own_valid_l discrete_valid.
    apply const_elim_sep_l=> Hvalid.
107
    assert (s  S) by eauto using sts_auth_frag_valid_inv.
108
    rewrite const_equiv // left_id sts_op_auth_frag //.
109
    by assert ( sts_frag S T) as [??] by eauto using cmra_valid_op_r.
110
111
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
112
  Lemma sts_closing E γ s T s' T' :
113
    sts.steps (s, T) (s', T') 
114
    ( φ s'  own γ (sts_auth s T))  (|={E}=>  sts_inv γ φ  sts_own γ s' T').
115
  Proof.
116
    intros Hstep. rewrite /sts_inv -(exist_intro s') later_sep.
Ralf Jung's avatar
Ralf Jung committed
117
    (* TODO it would be really nice to use cancel here *)
118
    rewrite [(_   φ _)%I]comm -assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
119
    rewrite -pvs_frame_l. apply sep_mono_r. rewrite -later_intro.
120
    rewrite own_valid_l discrete_valid. apply const_elim_sep_l=>Hval.
121
    trans (|={E}=> own γ (sts_auth s' T'))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
122
    { by apply own_update, sts_update_auth. }
123
    by rewrite -own_op sts_op_auth_frag_up.
Ralf Jung's avatar
Ralf Jung committed
124
  Qed.
125

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

128
  Lemma sts_fsaS E N P (Ψ : V  iPropG Λ Σ) γ S T :
Ralf Jung's avatar
Ralf Jung committed
129
    fsaV  nclose N  E 
130
131
    P  sts_ctx γ N φ 
    P  (sts_ownS γ S T   s,
132
           (s  S)   φ s -
Ralf Jung's avatar
Ralf Jung committed
133
          fsa (E  nclose N) (λ x,  s' T',
134
             sts.steps (s, T) (s', T')   φ s' 
135
136
            (sts_own γ s' T' - Ψ x))) 
    P  fsa E Ψ.
137
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
138
    rewrite /sts_ctx=>? HN Hinv Hinner.
139
140
    eapply (inv_fsa fsa); eauto. rewrite Hinner=>{Hinner Hinv P HN}.
    apply wand_intro_l. rewrite assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
141
    rewrite (sts_opened (E  N)) !pvs_frame_r !sep_exist_r.
142
143
    apply (fsa_strip_pvs fsa). apply exist_elim=>s.
    rewrite (forall_elim s). rewrite [(_  _)%I]comm.
144
145
146
    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
147
    apply (fsa_mono_pvs fsa)=> x.
148
    rewrite sep_exist_l; apply exist_elim=> s'.
Ralf Jung's avatar
Ralf Jung committed
149
150
    rewrite sep_exist_l; apply exist_elim=>T'.
    rewrite comm -!assoc. apply const_elim_sep_l=>-Hstep.
151
    rewrite assoc [(_  (_ - _))%I]comm -assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
152
    rewrite (sts_closing (E  N)) //; [].
153
154
155
156
    rewrite pvs_frame_l. apply pvs_mono.
    by rewrite assoc [(_  _)%I]comm -assoc wand_elim_l.
  Qed.

157
  Lemma sts_fsa E N P (Ψ : V  iPropG Λ Σ) γ s0 T :
Ralf Jung's avatar
Ralf Jung committed
158
    fsaV  nclose N  E 
159
160
    P  sts_ctx γ N φ 
    P  (sts_own γ s0 T   s,
Robbert Krebbers's avatar
Robbert Krebbers committed
161
           (s  sts.up s0 T)   φ s -
Ralf Jung's avatar
Ralf Jung committed
162
          fsa (E  nclose N) (λ x,  s' T',
163
             (sts.steps (s, T) (s', T'))   φ s' 
164
165
            (sts_own γ s' T' - Ψ x))) 
    P  fsa E Ψ.
166
  Proof. by apply sts_fsaS. Qed.
Ralf Jung's avatar
Ralf Jung committed
167
End sts.