sts.v 6.78 KB
Newer Older
1
2
From iris.algebra Require Export sts upred_tactics.
From iris.program_logic Require Export invariants ghost_ownership.
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) : gFunctor := GFunctor (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
  Implicit Types S : sts.states sts.
  Implicit Types T : sts.tokens sts.

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

Ralf Jung's avatar
Ralf Jung committed
69
  Lemma sts_own_weaken E γ s S T1 T2 :
70
    T2  T1  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.
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)) E).
85
      apply sts_auth_valid; set_solver. }
86
    rewrite pvs_frame_l. apply pvs_strip_pvs.
87
    rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
88
    trans ( sts_inv γ φ  sts_own γ s (  sts.tok s))%I.
89
    { rewrite /sts_inv -(exist_intro s) later_sep.
90
      ecancel [ φ _]%I.
91
      by rewrite -later_intro -own_op sts_op_auth_frag_up; last set_solver. }
92
    rewrite (inv_alloc N E) // /sts_ctx pvs_frame_r.
93
94
95
    by rewrite always_and_sep_l.
  Qed.

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

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

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

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

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