sts.v 6.81 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
2
3
4
From algebra Require Export sts.
From program_logic Require Export invariants ghost_ownership.
Import uPred.

Robbert Krebbers's avatar
Robbert Krebbers committed
5
6
7
Class STSInG Λ Σ (i : gid) (sts : stsT) := {
  sts_inG :> ghost_ownership.InG Λ Σ i (stsRA sts);
  sts_inhabited :> Inhabited (sts.state sts);
Ralf Jung's avatar
Ralf Jung committed
8
9
10
}.

Section definitions.
Robbert Krebbers's avatar
Robbert Krebbers committed
11
12
13
14
15
16
17
18
19
20
  Context {Λ Σ} (i : gid) (sts : stsT) `{!STSInG Λ Σ i sts} (γ : gname).
  Import sts.
  Definition sts_inv (φ : state sts  iPropG Λ Σ) : iPropG Λ Σ :=
    ( s, own i γ (sts_auth s )  φ s)%I.
  Definition sts_ownS (S : states sts) (T : tokens sts) : iPropG Λ Σ:=
    own i γ (sts_frag S T).
  Definition sts_own (s : state sts) (T : tokens sts) : iPropG Λ Σ :=
    own i γ (sts_frag_up s T).
  Definition sts_ctx (N : namespace) (φ: state sts  iPropG Λ Σ) : iPropG Λ Σ :=
    inv N (sts_inv φ).
Ralf Jung's avatar
Ralf Jung committed
21
End definitions.
Robbert Krebbers's avatar
Robbert Krebbers committed
22
23
24
25
Instance: Params (@sts_inv) 6.
Instance: Params (@sts_ownS) 6.
Instance: Params (@sts_own) 7.
Instance: Params (@sts_ctx) 7.
Ralf Jung's avatar
Ralf Jung committed
26
27

Section sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
28
29
  Context {Λ Σ} (i : gid) (sts : stsT) `{!STSInG Λ Σ StsI sts}.
  Context (φ : sts.state sts  iPropG Λ Σ).
Ralf Jung's avatar
Ralf Jung committed
30
31
32
  Implicit Types N : namespace.
  Implicit Types P Q R : iPropG Λ Σ.
  Implicit Types γ : gname.
Robbert Krebbers's avatar
Robbert Krebbers committed
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
  Implicit Types S : sts.states sts.
  Implicit Types T : sts.tokens sts.

  (** Setoids *)
  Global Instance sts_inv_ne n γ :
    Proper (pointwise_relation _ (dist n) ==> dist n) (sts_inv StsI sts γ).
  Proof. by intros φ1 φ2 Hφ; rewrite /sts_inv; setoid_rewrite Hφ. Qed.
  Global Instance sts_inv_proper γ :
    Proper (pointwise_relation _ () ==> ()) (sts_inv StsI sts γ).
  Proof. by intros φ1 φ2 Hφ; rewrite /sts_inv; setoid_rewrite Hφ. Qed.
  Global Instance sts_ownS_proper γ :
    Proper (() ==> () ==> ()) (sts_ownS StsI sts γ).
  Proof. intros S1 S2 HS T1 T2 HT. by rewrite /sts_ownS HS HT. Qed.
  Global Instance sts_own_proper γ s :
    Proper (() ==> ()) (sts_ownS StsI sts γ s).
  Proof. intros T1 T2 HT. by rewrite /sts_ownS HT. Qed.
  Global Instance sts_ctx_ne n γ N :
    Proper (pointwise_relation _ (dist n) ==> dist n) (sts_ctx StsI sts γ N).
  Proof. by intros φ1 φ2 Hφ; rewrite /sts_ctx Hφ. Qed.
  Global Instance sts_ctx_proper γ N :
    Proper (pointwise_relation _ () ==> ()) (sts_ctx StsI sts γ N).
  Proof. by intros φ1 φ2 Hφ; rewrite /sts_ctx Hφ. Qed.
Ralf Jung's avatar
Ralf Jung committed
55

56
57
  (* The same rule as implication does *not* hold, as could be shown using
     sts_frag_included. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
58
59
60
61
  Lemma sts_ownS_weaken E γ S1 S2 T :
    S1  S2  sts.closed S2 T 
    sts_ownS StsI sts γ S1 T  pvs E E (sts_ownS StsI sts γ S2 T).
  Proof. intros. by apply own_update, sts_update_frag. Qed.
62

Robbert Krebbers's avatar
Robbert Krebbers committed
63
64
65
66
  Lemma sts_own_weaken E γ s S T :
    s  S  sts.closed S T 
    sts_own StsI sts γ s T  pvs E E (sts_ownS StsI sts γ S T).
  Proof. intros. by apply own_update, sts_update_frag_up. Qed.
67

Robbert Krebbers's avatar
Robbert Krebbers committed
68
69
70
  Lemma sts_alloc N s :
    φ s  pvs N N ( γ, sts_ctx StsI sts γ N φ 
                        sts_own StsI sts γ s (set_all  sts.tok s)).
71
72
  Proof.
    eapply sep_elim_True_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
73
74
    { apply (own_alloc StsI (sts_auth s (set_all  sts.tok s)) N).
      apply sts_auth_valid; solve_elem_of. }
75
76
    rewrite pvs_frame_l. apply pvs_strip_pvs.
    rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
Robbert Krebbers's avatar
Robbert Krebbers committed
77
78
79
80
81
82
    transitivity ( sts_inv StsI sts γ φ 
                    sts_own StsI sts γ s (set_all  sts.tok s))%I.
    { rewrite /sts_inv -later_intro -(exist_intro s).
      rewrite [(_  φ _)%I]comm -assoc. apply sep_mono_r.
      by rewrite -own_op sts_op_auth_frag_up; last solve_elem_of+. }
    rewrite (inv_alloc N) /sts_ctx pvs_frame_r.
83
84
85
    by rewrite always_and_sep_l.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
86
87
88
  Lemma sts_opened E γ S T :
    ( sts_inv StsI sts γ φ  sts_ownS StsI sts γ S T)
     pvs E E ( s,  (s  S)   φ s  own StsI γ (sts_auth s T)).
89
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
90
    rewrite /sts_inv /sts_ownS later_exist sep_exist_r. apply exist_elim=>s.
91
92
93
94
    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
95
96
97
98
99
    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 //.
    (* this is horrible, but will be fixed whenever we have RAs back *)
    by rewrite -sts_frag_valid; eapply cmra_valid_op_r, discrete_valid.
100
101
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
102
103
104
105
  Lemma sts_closing E γ s T s' T' :
    sts.step (s, T) (s', T') 
    ( φ s'  own StsI γ (sts_auth s T))
     pvs E E ( sts_inv StsI sts γ φ  sts_own StsI sts γ s' T').
106
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
107
    intros Hstep. rewrite /sts_inv /sts_own -(exist_intro s').
Ralf Jung's avatar
Ralf Jung committed
108
    rewrite later_sep [(_  ▷φ _)%I]comm -assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
109
    rewrite -pvs_frame_l. apply sep_mono_r. rewrite -later_intro.
Ralf Jung's avatar
Ralf Jung committed
110
    rewrite own_valid_l discrete_validI. apply const_elim_sep_l=>Hval.
Robbert Krebbers's avatar
Robbert Krebbers committed
111
112
113
    transitivity (pvs E E (own StsI γ (sts_auth s' T'))).
    { by apply own_update, sts_update_auth. }
    by rewrite -own_op sts_op_auth_frag_up; last by inversion_clear Hstep.
Ralf Jung's avatar
Ralf Jung committed
114
  Qed.
115

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

Robbert Krebbers's avatar
Robbert Krebbers committed
118
  Lemma sts_fsaS E N P (Q : V  iPropG Λ Σ) γ S T :
Ralf Jung's avatar
Ralf Jung committed
119
    fsaV  nclose N  E 
Robbert Krebbers's avatar
Robbert Krebbers committed
120
121
    P  sts_ctx StsI sts γ N φ 
    P  (sts_ownS StsI sts γ S T   s,
122
           (s  S)   φ s -
Ralf Jung's avatar
Ralf Jung committed
123
          fsa (E  nclose N) (λ x,  s' T',
Robbert Krebbers's avatar
Robbert Krebbers committed
124
125
             sts.step (s, T) (s', T')   φ s' 
            (sts_own StsI sts γ s' T' - Q x))) 
126
127
    P  fsa E Q.
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
128
    rewrite /sts_ctx=>? HN Hinv Hinner.
129
130
    eapply (inv_fsa fsa); eauto. rewrite Hinner=>{Hinner Hinv P HN}.
    apply wand_intro_l. rewrite assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
131
    rewrite (sts_opened (E  N)) !pvs_frame_r !sep_exist_r.
132
133
134
135
136
    apply (fsa_strip_pvs fsa). apply exist_elim=>s.
    rewrite (forall_elim s). rewrite [(_  _)%I]comm.
    (* Getting this wand eliminated is really annoying. *)
    rewrite [(_  _)%I]comm -!assoc [(▷φ _  _  _)%I]assoc [(▷φ _  _)%I]comm.
    rewrite wand_elim_r fsa_frame_l.
Ralf Jung's avatar
Ralf Jung committed
137
    apply (fsa_mono_pvs fsa)=> x.
138
    rewrite sep_exist_l; apply exist_elim=> s'.
Ralf Jung's avatar
Ralf Jung committed
139
140
    rewrite sep_exist_l; apply exist_elim=>T'.
    rewrite comm -!assoc. apply const_elim_sep_l=>-Hstep.
141
    rewrite assoc [(_  (_ - _))%I]comm -assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
142
    rewrite (sts_closing (E  N)) //; [].
143
144
145
146
    rewrite pvs_frame_l. apply pvs_mono.
    by rewrite assoc [(_  _)%I]comm -assoc wand_elim_l.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
147
  Lemma sts_fsa E N P (Q : V  iPropG Λ Σ) γ s0 T :
Ralf Jung's avatar
Ralf Jung committed
148
    fsaV  nclose N  E 
Robbert Krebbers's avatar
Robbert Krebbers committed
149
150
151
    P  sts_ctx StsI sts γ N φ 
    P  (sts_own StsI sts γ s0 T   s,
           (s  sts.up s0 T)   φ s -
Ralf Jung's avatar
Ralf Jung committed
152
          fsa (E  nclose N) (λ x,  s' T',
Robbert Krebbers's avatar
Robbert Krebbers committed
153
154
             (sts.step (s, T) (s', T'))   φ s' 
            (sts_own StsI sts γ s' T' - Q x))) 
Ralf Jung's avatar
Ralf Jung committed
155
    P  fsa E Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
  Proof. apply sts_fsaS. Qed.
Ralf Jung's avatar
Ralf Jung committed
157
End sts.