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
  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.
35
  Global Instance sts_ownS_proper : Proper (() ==> () ==> ()) sts_ownS.
36
  Proof. solve_proper. Qed.
37
  Global Instance sts_own_proper s : Proper (() ==> ()) (sts_own s).
38 39 40 41 42
  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 :
43
    Proper (pointwise_relation _ () ==> ()) (sts_ctx N).
44
  Proof. solve_proper. Qed.
45
  Global Instance sts_ctx_persistent N φ : PersistentP (sts_ctx N φ).
46 47 48
  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 :
Robbert Krebbers's avatar
Robbert Krebbers committed
75
    T1  T2  sts.closed S1 T1  sts.closed S2 T2 
76
    sts_ownS γ (S1  S2) (T1  T2)  (sts_ownS γ S1 T1  sts_ownS γ S2 T2).
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
            (sts_own γ s' T' - Ψ x))) 
134
    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
            (sts_own γ s' T' - Ψ x))) 
163
    P  fsa E Ψ.
164
  Proof. by apply sts_fsaS. Qed.
Ralf Jung's avatar
Ralf Jung committed
165
End sts.