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

5
6
Class stsG Λ Σ (sts : stsT) := StsG {
  sts_inG :> inG Λ Σ (stsRA sts);
Robbert Krebbers's avatar
Robbert Krebbers committed
7
  sts_inhabited :> Inhabited (sts.state sts);
Ralf Jung's avatar
Ralf Jung committed
8
}.
9
Coercion sts_inG : stsG >-> inG.
Ralf Jung's avatar
Ralf Jung committed
10
11

Section definitions.
12
  Context `{i : stsG Λ Σ sts} (γ : gname).
Robbert Krebbers's avatar
Robbert Krebbers committed
13
14
  Import sts.
  Definition sts_inv (φ : state sts  iPropG Λ Σ) : iPropG Λ Σ :=
15
    ( s, own γ (sts_auth s )  φ s)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
16
  Definition sts_ownS (S : states sts) (T : tokens sts) : iPropG Λ Σ:=
17
    own γ (sts_frag S T).
Robbert Krebbers's avatar
Robbert Krebbers committed
18
  Definition sts_own (s : state sts) (T : tokens sts) : iPropG Λ Σ :=
19
    own γ (sts_frag_up s T).
Robbert Krebbers's avatar
Robbert Krebbers committed
20
21
  Definition sts_ctx (N : namespace) (φ: state sts  iPropG Λ Σ) : iPropG Λ Σ :=
    inv N (sts_inv φ).
Ralf Jung's avatar
Ralf Jung committed
22
End definitions.
23
24
25
26
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
27
28

Section sts.
29
  Context `{stsG Λ Σ sts} (φ : sts.state sts  iPropG Λ Σ).
Ralf Jung's avatar
Ralf Jung committed
30
31
32
  Implicit Types N : namespace.
  Implicit Types P Q R : iPropG Λ Σ.
  Implicit Types γ : gname.
Robbert Krebbers's avatar
Robbert Krebbers committed
33
34
35
36
37
  Implicit Types S : sts.states sts.
  Implicit Types T : sts.tokens sts.

  (** Setoids *)
  Global Instance sts_inv_ne n γ :
38
    Proper (pointwise_relation _ (dist n) ==> dist n) (sts_inv γ).
Robbert Krebbers's avatar
Robbert Krebbers committed
39
40
  Proof. by intros φ1 φ2 Hφ; rewrite /sts_inv; setoid_rewrite Hφ. Qed.
  Global Instance sts_inv_proper γ :
41
    Proper (pointwise_relation _ () ==> ()) (sts_inv γ).
Robbert Krebbers's avatar
Robbert Krebbers committed
42
  Proof. by intros φ1 φ2 Hφ; rewrite /sts_inv; setoid_rewrite Hφ. Qed.
43
  Global Instance sts_ownS_proper γ : Proper (() ==> () ==> ()) (sts_ownS γ).
Robbert Krebbers's avatar
Robbert Krebbers committed
44
  Proof. intros S1 S2 HS T1 T2 HT. by rewrite /sts_ownS HS HT. Qed.
45
46
  Global Instance sts_own_proper γ s : Proper (() ==> ()) (sts_own γ s).
  Proof. intros T1 T2 HT. by rewrite /sts_own HT. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
47
  Global Instance sts_ctx_ne n γ N :
48
    Proper (pointwise_relation _ (dist n) ==> dist n) (sts_ctx γ N).
Robbert Krebbers's avatar
Robbert Krebbers committed
49
50
  Proof. by intros φ1 φ2 Hφ; rewrite /sts_ctx Hφ. Qed.
  Global Instance sts_ctx_proper γ N :
51
    Proper (pointwise_relation _ () ==> ()) (sts_ctx γ N).
Robbert Krebbers's avatar
Robbert Krebbers committed
52
  Proof. by intros φ1 φ2 Hφ; rewrite /sts_ctx Hφ. Qed.
Ralf Jung's avatar
Ralf Jung committed
53

54
55
  (* The same rule as implication does *not* hold, as could be shown using
     sts_frag_included. *)
Ralf Jung's avatar
Ralf Jung committed
56
57
58
59
60
61
62
63
  (* TODO: sts.closed forces the user to prove that S2 is inhabited. This is
     silly, we know that S1 is inhabited since we own it, and hence S2 is
     inhabited, too. Probably, sts.closed should really just be about closedness.
     I think keeping disjointnes of the token stuff in there is fine, since it
     does not incur any unnecessary side-conditions.
     Then we additionally demand for validity that S is nonempty, rather than
     making that part of "closed".
   *)
Ralf Jung's avatar
Ralf Jung committed
64
65
  Lemma sts_ownS_weaken E γ S1 S2 T1 T2 :
    T1  T2  S1  S2  sts.closed S2 T2 
66
    sts_ownS γ S1 T1  (|={E}=> sts_ownS γ S2 T2).
Ralf Jung's avatar
Ralf Jung committed
67
  Proof. intros -> ? ?. by apply own_update, sts_update_frag. Qed.
68

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
97
  Lemma sts_opened E γ S T :
98
    ( sts_inv γ φ  sts_ownS γ S T)
99
     (|={E}=>  s,  (s  S)   φ s  own γ (sts_auth s T)).
100
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
101
    rewrite /sts_inv /sts_ownS later_exist sep_exist_r. apply exist_elim=>s.
102
103
104
105
    rewrite later_sep pvs_timeless !pvs_frame_r. apply pvs_mono.
    rewrite -(exist_intro s).
    rewrite [(_  ▷φ _)%I]comm -!assoc -own_op -[(▷φ _  _)%I]comm.
    rewrite own_valid_l discrete_validI.
Robbert Krebbers's avatar
Robbert Krebbers committed
106
107
108
109
110
    rewrite -!assoc. apply const_elim_sep_l=> Hvalid.
    assert (s  S) by (by eapply sts_auth_frag_valid_inv, discrete_valid).
    rewrite const_equiv // left_id comm sts_op_auth_frag //.
    (* this is horrible, but will be fixed whenever we have RAs back *)
    by rewrite -sts_frag_valid; eapply cmra_valid_op_r, discrete_valid.
111
112
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
113
  Lemma sts_closing E γ s T s' T' :
114
    sts.steps (s, T) (s', T') 
115
    ( φ s'  own γ (sts_auth s T))  (|={E}=>  sts_inv γ φ  sts_own γ s' T').
116
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
117
    intros Hstep. rewrite /sts_inv /sts_own -(exist_intro s').
Ralf Jung's avatar
Ralf Jung committed
118
    rewrite later_sep [(_  ▷φ _)%I]comm -assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
119
    rewrite -pvs_frame_l. apply sep_mono_r. rewrite -later_intro.
Ralf Jung's avatar
Ralf Jung committed
120
    rewrite own_valid_l discrete_validI. 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 Ψ.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
  Proof. apply sts_fsaS. Qed.
Ralf Jung's avatar
Ralf Jung committed
167
End sts.