sts.v 6.77 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
  Lemma sts_ownS_weaken E γ S1 S2 T1 T2 :
    T1  T2  S1  S2  sts.closed S2 T2 
58
    sts_ownS γ S1 T1  (|={E}=> sts_ownS γ S2 T2).
Ralf Jung's avatar
Ralf Jung committed
59
  Proof. intros -> ? ?. by apply own_update, sts_update_frag. Qed.
60

Ralf Jung's avatar
Ralf Jung committed
61
62
  Lemma sts_own_weaken E γ s S T1 T2 :
    T1  T2  s  S  sts.closed S T2 
63
    sts_own γ s T1  (|={E}=> sts_ownS γ S T2).
64
  Proof. intros -> ??. by apply own_update, sts_update_frag_up. Qed.
65

Ralf Jung's avatar
Ralf Jung committed
66
  Lemma sts_ownS_op γ S1 S2 T1 T2 :
Ralf Jung's avatar
Ralf Jung committed
67
    T1  T2    sts.closed S1 T1  sts.closed S2 T2 
Ralf Jung's avatar
Ralf Jung committed
68
    sts_ownS γ (S1  S2) (T1  T2)  (sts_ownS γ S1 T1  sts_ownS γ S2 T2)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
69
  Proof. intros. by rewrite /sts_ownS -own_op sts_op_frag. Qed.
Ralf Jung's avatar
Ralf Jung committed
70

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

Robbert Krebbers's avatar
Robbert Krebbers committed
89
  Lemma sts_opened E γ S T :
90
    ( sts_inv γ φ  sts_ownS γ S T)
91
     (|={E}=>  s,  (s  S)   φ s  own γ (sts_auth s T)).
92
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
    rewrite /sts_inv /sts_ownS later_exist sep_exist_r. apply exist_elim=>s.
94
95
96
97
    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
98
99
100
101
102
    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.
103
104
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
105
  Lemma sts_closing E γ s T s' T' :
106
    sts.steps (s, T) (s', T') 
107
    ( φ s'  own γ (sts_auth s T))  (|={E}=>  sts_inv γ φ  sts_own γ s' T').
108
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
109
    intros Hstep. rewrite /sts_inv /sts_own -(exist_intro s').
Ralf Jung's avatar
Ralf Jung committed
110
    rewrite later_sep [(_  ▷φ _)%I]comm -assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
111
    rewrite -pvs_frame_l. apply sep_mono_r. rewrite -later_intro.
Ralf Jung's avatar
Ralf Jung committed
112
    rewrite own_valid_l discrete_validI. apply const_elim_sep_l=>Hval.
113
    transitivity (|={E}=> own γ (sts_auth s' T'))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
114
    { by apply own_update, sts_update_auth. }
115
    by rewrite -own_op sts_op_auth_frag_up.
Ralf Jung's avatar
Ralf Jung committed
116
  Qed.
117

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

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

149
  Lemma sts_fsa E N P (Ψ : V  iPropG Λ Σ) γ s0 T :
Ralf Jung's avatar
Ralf Jung committed
150
    fsaV  nclose N  E 
151
152
    P  sts_ctx γ N φ 
    P  (sts_own γ s0 T   s,
Robbert Krebbers's avatar
Robbert Krebbers committed
153
           (s  sts.up s0 T)   φ s -
Ralf Jung's avatar
Ralf Jung committed
154
          fsa (E  nclose N) (λ x,  s' T',
155
             (sts.steps (s, T) (s', T'))   φ s' 
156
157
            (sts_own γ s' T' - Ψ x))) 
    P  fsa E Ψ.
Robbert Krebbers's avatar
Robbert Krebbers committed
158
  Proof. apply sts_fsaS. Qed.
Ralf Jung's avatar
Ralf Jung committed
159
End sts.