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.