sts.v 7.97 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 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
Definition stsGF (sts : stsT) : iFunctor := constF (stsRA sts).
12
Instance inGF_stsG sts `{inGF Λ Σ (stsGF sts)}
13 14
  `{Inhabited (sts.state sts)} : stsG Λ Σ sts.
Proof. split; try apply _. apply: inGF_inG. Qed.
15

Ralf Jung's avatar
Ralf Jung committed
16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44
Definition sts_ownS_def `{i : stsG Λ Σ sts} (γ : gname)
           (S : sts.states sts) (T : sts.tokens sts) : iPropG Λ Σ:=
  own γ (sts_frag S T).
Definition sts_own_def `{i : stsG Λ Σ sts} (γ : gname)
           (s : sts.state sts) (T : sts.tokens sts) : iPropG Λ Σ :=
  own γ (sts_frag_up s T).
(* Perform sealing. *)
Module Type StsOwnSig.
  Parameter sts_ownS :  `{i : stsG Λ Σ sts} (γ : gname)
           (S : sts.states sts) (T : sts.tokens sts), iPropG Λ Σ.
  Parameter sts_own :  `{i : stsG Λ Σ sts} (γ : gname)
           (s : sts.state sts) (T : sts.tokens sts), iPropG Λ Σ.
  Axiom sts_ownS_def : @sts_ownS = @sts_ownS_def.
  Axiom sts_own_def : @sts_own = @sts_own_def.
End StsOwnSig.
Module Export StsOwn : StsOwnSig.
  Definition sts_ownS := @sts_ownS_def.
  Definition sts_own := @sts_own_def.
  Definition sts_ownS_def := Logic.eq_refl (@sts_ownS_def).
  Definition sts_own_def := Logic.eq_refl (@sts_own_def).
End StsOwn. 

Definition sts_inv `{i : stsG Λ Σ sts} (γ : gname)
           (φ : sts.state sts  iPropG Λ Σ) : iPropG Λ Σ :=
  ( s, own γ (sts_auth s )  φ s)%I.
Definition sts_ctx `{i : stsG Λ Σ sts} (γ : gname)
           (N : namespace) (φ: sts.state sts  iPropG Λ Σ) : iPropG Λ Σ :=
  inv N (sts_inv γ φ).

45 46 47 48
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
49 50

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

  (** Setoids *)
  Global Instance sts_inv_ne n γ :
60
    Proper (pointwise_relation _ (dist n) ==> dist n) (sts_inv γ).
Robbert Krebbers's avatar
Robbert Krebbers committed
61 62
  Proof. by intros φ1 φ2 Hφ; rewrite /sts_inv; setoid_rewrite Hφ. Qed.
  Global Instance sts_inv_proper γ :
63
    Proper (pointwise_relation _ () ==> ()) (sts_inv γ).
Robbert Krebbers's avatar
Robbert Krebbers committed
64
  Proof. by intros φ1 φ2 Hφ; rewrite /sts_inv; setoid_rewrite Hφ. Qed.
65
  Global Instance sts_ownS_proper γ : Proper (() ==> () ==> ()) (sts_ownS γ).
Ralf Jung's avatar
Ralf Jung committed
66 67 68
  Proof.
    intros S1 S2 HS T1 T2 HT. by rewrite !sts_ownS_def /Top.sts_ownS_def HS HT.
  Qed.
69
  Global Instance sts_own_proper γ s : Proper (() ==> ()) (sts_own γ s).
Ralf Jung's avatar
Ralf Jung committed
70
  Proof. intros T1 T2 HT. by rewrite !sts_own_def /Top.sts_own_def HT. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
71
  Global Instance sts_ctx_ne n γ N :
72
    Proper (pointwise_relation _ (dist n) ==> dist n) (sts_ctx γ N).
Robbert Krebbers's avatar
Robbert Krebbers committed
73 74
  Proof. by intros φ1 φ2 Hφ; rewrite /sts_ctx Hφ. Qed.
  Global Instance sts_ctx_proper γ N :
75
    Proper (pointwise_relation _ () ==> ()) (sts_ctx γ N).
Robbert Krebbers's avatar
Robbert Krebbers committed
76
  Proof. by intros φ1 φ2 Hφ; rewrite /sts_ctx Hφ. Qed.
Ralf Jung's avatar
Ralf Jung committed
77

78 79
  (* The same rule as implication does *not* hold, as could be shown using
     sts_frag_included. *)
Ralf Jung's avatar
Ralf Jung committed
80
  Lemma sts_ownS_weaken E γ S1 S2 T1 T2 :
81
    T2  T1  S1  S2  sts.closed S2 T2 
82
    sts_ownS γ S1 T1  (|={E}=> sts_ownS γ S2 T2).
Ralf Jung's avatar
Ralf Jung committed
83 84 85
  Proof.
    intros ? ? ?. rewrite sts_ownS_def. by apply own_update, sts_update_frag.
  Qed.
86

Ralf Jung's avatar
Ralf Jung committed
87
  Lemma sts_own_weaken E γ s S T1 T2 :
88
    T2  T1  s  S  sts.closed S T2 
89
    sts_own γ s T1  (|={E}=> sts_ownS γ S T2).
Ralf Jung's avatar
Ralf Jung committed
90 91 92 93
  Proof.
    intros ???. rewrite sts_ownS_def sts_own_def.
    by apply own_update, sts_update_frag_up.
  Qed.
94

Ralf Jung's avatar
Ralf Jung committed
95
  Lemma sts_ownS_op γ S1 S2 T1 T2 :
Ralf Jung's avatar
Ralf Jung committed
96
    T1  T2    sts.closed S1 T1  sts.closed S2 T2 
Ralf Jung's avatar
Ralf Jung committed
97
    sts_ownS γ (S1  S2) (T1  T2)  (sts_ownS γ S1 T1  sts_ownS γ S2 T2)%I.
Ralf Jung's avatar
Ralf Jung committed
98 99 100
  Proof.
    intros. by rewrite sts_ownS_def /Top.sts_ownS_def -own_op sts_op_frag.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
101

102 103
  Lemma sts_alloc E N s :
    nclose N  E 
104
     φ s  (|={E}=>  γ, sts_ctx γ N φ  sts_own γ s (  sts.tok s)).
105
  Proof.
106
    intros HN. eapply sep_elim_True_r.
107
    { apply (own_alloc (sts_auth s (  sts.tok s)) N).
108
      apply sts_auth_valid; set_solver. }
109 110
    rewrite pvs_frame_l. rewrite -(pvs_mask_weaken N E) //.
    apply pvs_strip_pvs.
111
    rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
112
    trans ( sts_inv γ φ  sts_own γ s (  sts.tok s))%I.
113
    { rewrite /sts_inv -(exist_intro s) later_sep.
Ralf Jung's avatar
Ralf Jung committed
114
      ecancel [ φ _]%I. rewrite sts_own_def.
115
      by rewrite -later_intro -own_op sts_op_auth_frag_up; last set_solver. }
Robbert Krebbers's avatar
Robbert Krebbers committed
116
    rewrite (inv_alloc N) /sts_ctx pvs_frame_r.
117 118 119
    by rewrite always_and_sep_l.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
120
  Lemma sts_opened E γ S T :
121
    ( sts_inv γ φ  sts_ownS γ S T)
122
     (|={E}=>  s,  (s  S)   φ s  own γ (sts_auth s T)).
123
  Proof.
Ralf Jung's avatar
Ralf Jung committed
124
    rewrite /sts_inv sts_ownS_def later_exist sep_exist_r. apply exist_elim=>s.
125 126 127 128
    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
129 130 131
    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 //.
132 133 134
    assert ( sts_frag S T) as Hv by
          by eapply cmra_valid_op_r, discrete_valid.
    apply (Hv 0).
135 136
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
137
  Lemma sts_closing E γ s T s' T' :
138
    sts.steps (s, T) (s', T') 
139
    ( φ s'  own γ (sts_auth s T))  (|={E}=>  sts_inv γ φ  sts_own γ s' T').
140
  Proof.
Ralf Jung's avatar
Ralf Jung committed
141
    intros Hstep. rewrite /sts_inv sts_own_def -(exist_intro s') later_sep.
Ralf Jung's avatar
Ralf Jung committed
142
    (* TODO it would be really nice to use cancel here *)
143
    rewrite [(_   φ _)%I]comm -assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
144
    rewrite -pvs_frame_l. apply sep_mono_r. rewrite -later_intro.
Ralf Jung's avatar
Ralf Jung committed
145
    rewrite own_valid_l discrete_validI. apply const_elim_sep_l=>Hval.
146
    trans (|={E}=> own γ (sts_auth s' T'))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
147
    { by apply own_update, sts_update_auth. }
148
    by rewrite -own_op sts_op_auth_frag_up.
Ralf Jung's avatar
Ralf Jung committed
149
  Qed.
150

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

153
  Lemma sts_fsaS E N P (Ψ : V  iPropG Λ Σ) γ S T :
Ralf Jung's avatar
Ralf Jung committed
154
    fsaV  nclose N  E 
155 156
    P  sts_ctx γ N φ 
    P  (sts_ownS γ S T   s,
157
           (s  S)   φ s -
Ralf Jung's avatar
Ralf Jung committed
158
          fsa (E  nclose N) (λ x,  s' T',
159
             sts.steps (s, T) (s', T')   φ s' 
160 161
            (sts_own γ s' T' - Ψ x))) 
    P  fsa E Ψ.
162
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
163
    rewrite /sts_ctx=>? HN Hinv Hinner.
164 165
    eapply (inv_fsa fsa); eauto. rewrite Hinner=>{Hinner Hinv P HN}.
    apply wand_intro_l. rewrite assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
    rewrite (sts_opened (E  N)) !pvs_frame_r !sep_exist_r.
167 168
    apply (fsa_strip_pvs fsa). apply exist_elim=>s.
    rewrite (forall_elim s). rewrite [(_  _)%I]comm.
169 170 171
    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
172
    apply (fsa_mono_pvs fsa)=> x.
173
    rewrite sep_exist_l; apply exist_elim=> s'.
Ralf Jung's avatar
Ralf Jung committed
174 175
    rewrite sep_exist_l; apply exist_elim=>T'.
    rewrite comm -!assoc. apply const_elim_sep_l=>-Hstep.
176
    rewrite assoc [(_  (_ - _))%I]comm -assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
177
    rewrite (sts_closing (E  N)) //; [].
178 179 180 181
    rewrite pvs_frame_l. apply pvs_mono.
    by rewrite assoc [(_  _)%I]comm -assoc wand_elim_l.
  Qed.

182
  Lemma sts_fsa E N P (Ψ : V  iPropG Λ Σ) γ s0 T :
Ralf Jung's avatar
Ralf Jung committed
183
    fsaV  nclose N  E 
184 185
    P  sts_ctx γ N φ 
    P  (sts_own γ s0 T   s,
Robbert Krebbers's avatar
Robbert Krebbers committed
186
           (s  sts.up s0 T)   φ s -
Ralf Jung's avatar
Ralf Jung committed
187
          fsa (E  nclose N) (λ x,  s' T',
188
             (sts.steps (s, T) (s', T'))   φ s' 
189 190
            (sts_own γ s' T' - Ψ x))) 
    P  fsa E Ψ.
Ralf Jung's avatar
Ralf Jung committed
191 192 193 194
  Proof.
    rewrite sts_own_def. intros. eapply sts_fsaS; try done; [].
    by rewrite sts_ownS_def sts_own_def. 
  Qed.
Ralf Jung's avatar
Ralf Jung committed
195
End sts.