sts.v 7.47 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
Definition sts_ownS_def `{i : stsG Λ Σ sts} (γ : gname)
Robbert Krebbers's avatar
Robbert Krebbers committed
17
    (S : sts.states sts) (T : sts.tokens sts) : iPropG Λ Σ:=
Ralf Jung's avatar
Ralf Jung committed
18
  own γ (sts_frag S T).
19
(* Perform sealing. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
20
21
22
Definition sts_ownS_aux : { x | x = @sts_ownS_def }. by eexists. Qed.
Definition sts_ownS {Λ Σ sts i} := proj1_sig sts_ownS_aux Λ Σ sts i.
Definition sts_ownS_eq : @sts_ownS = @sts_ownS_def := proj2_sig sts_ownS_aux.
23

Ralf Jung's avatar
Ralf Jung committed
24
Definition sts_own_def `{i : stsG Λ Σ sts} (γ : gname)
Robbert Krebbers's avatar
Robbert Krebbers committed
25
    (s : sts.state sts) (T : sts.tokens sts) : iPropG Λ Σ :=
Ralf Jung's avatar
Ralf Jung committed
26
27
  own γ (sts_frag_up s T).
(* Perform sealing. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
28
29
30
Definition sts_own_aux : { x | x = @sts_own_def }. by eexists. Qed.
Definition sts_own {Λ Σ sts i} := proj1_sig sts_own_aux Λ Σ sts i.
Definition sts_own_eq : @sts_own = @sts_own_def := proj2_sig sts_own_aux.
Ralf Jung's avatar
Ralf Jung committed
31
32

Definition sts_inv `{i : stsG Λ Σ sts} (γ : gname)
Robbert Krebbers's avatar
Robbert Krebbers committed
33
    (φ : sts.state sts  iPropG Λ Σ) : iPropG Λ Σ :=
Ralf Jung's avatar
Ralf Jung committed
34
35
  ( s, own γ (sts_auth s )  φ s)%I.
Definition sts_ctx `{i : stsG Λ Σ sts} (γ : gname)
Robbert Krebbers's avatar
Robbert Krebbers committed
36
    (N : namespace) (φ: sts.state sts  iPropG Λ Σ) : iPropG Λ Σ :=
Ralf Jung's avatar
Ralf Jung committed
37
38
  inv N (sts_inv γ φ).

39
40
41
42
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
43
44

Section sts.
45
  Context `{stsG Λ Σ sts} (φ : sts.state sts  iPropG Λ Σ).
Ralf Jung's avatar
Ralf Jung committed
46
47
48
  Implicit Types N : namespace.
  Implicit Types P Q R : iPropG Λ Σ.
  Implicit Types γ : gname.
Robbert Krebbers's avatar
Robbert Krebbers committed
49
50
51
52
53
  Implicit Types S : sts.states sts.
  Implicit Types T : sts.tokens sts.

  (** Setoids *)
  Global Instance sts_inv_ne n γ :
54
    Proper (pointwise_relation _ (dist n) ==> dist n) (sts_inv γ).
55
  Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
56
  Global Instance sts_inv_proper γ :
57
    Proper (pointwise_relation _ () ==> ()) (sts_inv γ).
58
  Proof. solve_proper. Qed.
59
  Global Instance sts_ownS_proper γ : Proper (() ==> () ==> ()) (sts_ownS γ).
60
  Proof. rewrite sts_ownS_eq. solve_proper. Qed.
61
  Global Instance sts_own_proper γ s : Proper (() ==> ()) (sts_own γ s).
62
  Proof. rewrite sts_own_eq. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
63
  Global Instance sts_ctx_ne n γ N :
64
    Proper (pointwise_relation _ (dist n) ==> dist n) (sts_ctx γ N).
65
  Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
66
  Global Instance sts_ctx_proper γ N :
67
    Proper (pointwise_relation _ () ==> ()) (sts_ctx γ N).
68
  Proof. solve_proper. Qed.
Ralf Jung's avatar
Ralf Jung committed
69

70
71
  (* The same rule as implication does *not* hold, as could be shown using
     sts_frag_included. *)
Ralf Jung's avatar
Ralf Jung committed
72
  Lemma sts_ownS_weaken E γ S1 S2 T1 T2 :
73
    T2  T1  S1  S2  sts.closed S2 T2 
74
    sts_ownS γ S1 T1  (|={E}=> sts_ownS γ S2 T2).
Ralf Jung's avatar
Ralf Jung committed
75
  Proof.
Ralf Jung's avatar
Ralf Jung committed
76
    intros ? ? ?. rewrite sts_ownS_eq. by apply own_update, sts_update_frag.
Ralf Jung's avatar
Ralf Jung committed
77
  Qed.
78

Ralf Jung's avatar
Ralf Jung committed
79
  Lemma sts_own_weaken E γ s S T1 T2 :
80
    T2  T1  s  S  sts.closed S T2 
81
    sts_own γ s T1  (|={E}=> sts_ownS γ S T2).
Ralf Jung's avatar
Ralf Jung committed
82
  Proof.
Ralf Jung's avatar
Ralf Jung committed
83
    intros ???. rewrite sts_ownS_eq sts_own_eq.
Ralf Jung's avatar
Ralf Jung committed
84
85
    by apply own_update, sts_update_frag_up.
  Qed.
86

Ralf Jung's avatar
Ralf Jung committed
87
  Lemma sts_ownS_op γ S1 S2 T1 T2 :
Ralf Jung's avatar
Ralf Jung committed
88
    T1  T2    sts.closed S1 T1  sts.closed S2 T2 
Ralf Jung's avatar
Ralf Jung committed
89
    sts_ownS γ (S1  S2) (T1  T2)  (sts_ownS γ S1 T1  sts_ownS γ S2 T2)%I.
Ralf Jung's avatar
Ralf Jung committed
90
  Proof. intros. by rewrite sts_ownS_eq /sts_ownS_def -own_op sts_op_frag. Qed.
Ralf Jung's avatar
Ralf Jung committed
91

92
93
  Lemma sts_alloc E N s :
    nclose N  E 
94
     φ s  (|={E}=>  γ, sts_ctx γ N φ  sts_own γ s (  sts.tok s)).
95
  Proof.
96
    intros HN. eapply sep_elim_True_r.
97
    { apply (own_alloc (sts_auth s (  sts.tok s)) N).
98
      apply sts_auth_valid; set_solver. }
99
100
    rewrite pvs_frame_l. rewrite -(pvs_mask_weaken N E) //.
    apply pvs_strip_pvs.
101
    rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
102
    trans ( sts_inv γ φ  sts_own γ s (  sts.tok s))%I.
103
    { rewrite /sts_inv -(exist_intro s) later_sep.
Ralf Jung's avatar
Ralf Jung committed
104
      ecancel [ φ _]%I. rewrite sts_own_eq.
105
      by rewrite -later_intro -own_op sts_op_auth_frag_up; last set_solver. }
Robbert Krebbers's avatar
Robbert Krebbers committed
106
    rewrite (inv_alloc N) /sts_ctx pvs_frame_r.
107
108
109
    by rewrite always_and_sep_l.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
110
  Lemma sts_opened E γ S T :
111
    ( sts_inv γ φ  sts_ownS γ S T)
112
     (|={E}=>  s,  (s  S)   φ s  own γ (sts_auth s T)).
113
  Proof.
Ralf Jung's avatar
Ralf Jung committed
114
    rewrite /sts_inv sts_ownS_eq later_exist sep_exist_r. apply exist_elim=>s.
115
116
117
    rewrite later_sep pvs_timeless !pvs_frame_r. apply pvs_mono.
    rewrite -(exist_intro s).
    rewrite [(_  ▷φ _)%I]comm -!assoc -own_op -[(▷φ _  _)%I]comm.
118
    rewrite own_valid_l discrete_valid.
Robbert Krebbers's avatar
Robbert Krebbers committed
119
    rewrite -!assoc. apply const_elim_sep_l=> Hvalid.
120
    assert (s  S) by eauto using sts_auth_frag_valid_inv.
Robbert Krebbers's avatar
Robbert Krebbers committed
121
    rewrite const_equiv // left_id comm sts_op_auth_frag //.
122
    by assert ( sts_frag S T) as [??] by eauto using cmra_valid_op_r.
123
124
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
125
  Lemma sts_closing E γ s T s' T' :
126
    sts.steps (s, T) (s', T') 
127
    ( φ s'  own γ (sts_auth s T))  (|={E}=>  sts_inv γ φ  sts_own γ s' T').
128
  Proof.
Ralf Jung's avatar
Ralf Jung committed
129
    intros Hstep. rewrite /sts_inv sts_own_eq -(exist_intro s') later_sep.
Ralf Jung's avatar
Ralf Jung committed
130
    (* TODO it would be really nice to use cancel here *)
131
    rewrite [(_   φ _)%I]comm -assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
132
    rewrite -pvs_frame_l. apply sep_mono_r. rewrite -later_intro.
133
    rewrite own_valid_l discrete_valid. apply const_elim_sep_l=>Hval.
134
    trans (|={E}=> own γ (sts_auth s' T'))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
135
    { by apply own_update, sts_update_auth. }
136
    by rewrite -own_op sts_op_auth_frag_up.
Ralf Jung's avatar
Ralf Jung committed
137
  Qed.
138

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

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

170
  Lemma sts_fsa E N P (Ψ : V  iPropG Λ Σ) γ s0 T :
Ralf Jung's avatar
Ralf Jung committed
171
    fsaV  nclose N  E 
172
173
    P  sts_ctx γ N φ 
    P  (sts_own γ s0 T   s,
Robbert Krebbers's avatar
Robbert Krebbers committed
174
           (s  sts.up s0 T)   φ s -
Ralf Jung's avatar
Ralf Jung committed
175
          fsa (E  nclose N) (λ x,  s' T',
176
             (sts.steps (s, T) (s', T'))   φ s' 
177
178
            (sts_own γ s' T' - Ψ x))) 
    P  fsa E Ψ.
Ralf Jung's avatar
Ralf Jung committed
179
  Proof.
180
    rewrite sts_own_eq. intros. eapply sts_fsaS; try done; [].
Ralf Jung's avatar
Ralf Jung committed
181
    by rewrite sts_ownS_eq sts_own_eq. 
Ralf Jung's avatar
Ralf Jung committed
182
  Qed.
Ralf Jung's avatar
Ralf Jung committed
183
End sts.