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

6
7
8
9
10
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ !_ !_ /.
Local Arguments unit _ _ !_ /.

Module sts.
Ralf Jung's avatar
Ralf Jung committed
11
12
13
14
(** This module is *not* meant to be imported. Instead, just use "sts.ctx" etc.
    like you would use "auth_ctx" etc. *)
Export algebra.sts.sts.

Robbert Krebbers's avatar
Robbert Krebbers committed
15
Class InG Λ Σ (i : gid) (sts : stsT) := {
Ralf Jung's avatar
Ralf Jung committed
16
17
  inG :> ghost_ownership.InG Λ Σ i (sts.RA sts);
  inh :> Inhabited (state sts);
Ralf Jung's avatar
Ralf Jung committed
18
19
20
}.

Section definitions.
Robbert Krebbers's avatar
Robbert Krebbers committed
21
  Context {Λ Σ} (i : gid) (sts : stsT) `{!InG Λ Σ i sts} (γ : gname).
Ralf Jung's avatar
Ralf Jung committed
22
23
24
25
26
27
28
  Definition inv  (φ : state sts  iPropG Λ Σ) : iPropG Λ Σ :=
    ( s, own i γ (auth sts s )  φ s)%I.
  Definition in_states (S : set (state sts)) (T: set (token sts)) : iPropG Λ Σ:=
    own i γ (frag sts S T)%I.
  Definition in_state (s : state sts) (T: set (token sts)) : iPropG Λ Σ :=
    in_states (up sts s T) T.
  Definition ctx (N : namespace) (φ : state sts  iPropG Λ Σ) : iPropG Λ Σ :=
29
    invariants.inv N (inv φ).
Ralf Jung's avatar
Ralf Jung committed
30
End definitions.
Ralf Jung's avatar
Ralf Jung committed
31
32
33
34
Instance: Params (@inv) 6.
Instance: Params (@in_states) 6.
Instance: Params (@in_state) 6.
Instance: Params (@ctx) 7.
Ralf Jung's avatar
Ralf Jung committed
35
36

Section sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
37
  Context {Λ Σ} (i : gid) (sts : stsT) `{!InG Λ Σ StsI sts}.
Ralf Jung's avatar
Ralf Jung committed
38
  Context (φ : state sts  iPropG Λ Σ).
Ralf Jung's avatar
Ralf Jung committed
39
40
41
42
  Implicit Types N : namespace.
  Implicit Types P Q R : iPropG Λ Σ.
  Implicit Types γ : gname.

43
44
  (* The same rule as implication does *not* hold, as could be shown using
     sts_frag_included. *)
Ralf Jung's avatar
Ralf Jung committed
45
46
47
  Lemma in_states_weaken E γ S1 S2 T :
    S1  S2  closed sts S2 T 
    in_states StsI sts γ S1 T  pvs E E (in_states StsI sts γ S2 T).
48
  Proof.
Ralf Jung's avatar
Ralf Jung committed
49
    rewrite /in_states=>Hs Hcl. apply own_update, sts_update_frag; done.
50
51
  Qed.

Ralf Jung's avatar
Ralf Jung committed
52
53
54
  Lemma in_state_states E γ s S T :
    s  S  closed sts S T 
    in_state StsI sts γ s T  pvs E E (in_states StsI sts γ S T).
55
  Proof.
Ralf Jung's avatar
Ralf Jung committed
56
57
    move=>Hs Hcl. apply in_states_weaken; last done.
    move=>s' Hup. eapply closed_steps in Hcl;last (hnf in Hup; eexact Hup);done.
58
59
  Qed.

60
  Lemma alloc N s :
Ralf Jung's avatar
Ralf Jung committed
61
62
    φ s  pvs N N ( γ, ctx StsI sts γ N φ 
                        in_state StsI sts γ s (set_all  sts.(tok) s)).
63
64
  Proof.
    eapply sep_elim_True_r.
Ralf Jung's avatar
Ralf Jung committed
65
    { eapply (own_alloc StsI (auth sts s (set_all  sts.(tok) s)) N).
66
67
68
      apply discrete_valid=>/=. solve_elem_of. }
    rewrite pvs_frame_l. apply pvs_strip_pvs.
    rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
Ralf Jung's avatar
Ralf Jung committed
69
70
    transitivity ( inv StsI sts γ φ 
                    in_state StsI sts γ s (set_all  sts.(tok) s))%I.
71
72
73
74
    { rewrite /inv -later_intro -(exist_intro s).
      rewrite [(_  φ _)%I]comm -assoc. apply sep_mono; first done.
      rewrite -own_op. apply equiv_spec, own_proper.
      split; first split; simpl.
Ralf Jung's avatar
Ralf Jung committed
75
76
77
78
79
      - intros; solve_elem_of+.
      - intros _. split_ands; first by solve_elem_of+.
        + apply closed_up. solve_elem_of+.
        + constructor; last solve_elem_of+. apply sts.elem_of_up. 
      - intros _. constructor. solve_elem_of+. }
80
81
82
83
    rewrite (inv_alloc N) /ctx pvs_frame_r. apply pvs_mono.
    by rewrite always_and_sep_l.
  Qed.

84
  Lemma opened E γ S T :
Ralf Jung's avatar
Ralf Jung committed
85
86
    ( inv StsI sts γ φ  in_states StsI sts γ S T)
       pvs E E ( s,  (s  S)   φ s  own StsI γ (auth sts s T)).
87
  Proof.
Ralf Jung's avatar
Ralf Jung committed
88
    rewrite /inv /in_states later_exist sep_exist_r. apply exist_elim=>s.
89
90
91
92
    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.
Ralf Jung's avatar
Ralf Jung committed
93
94
    rewrite -!assoc. apply const_elim_sep_l=>-[_ [Hcl Hdisj]].
    simpl in Hdisj, Hcl. inversion_clear Hdisj. rewrite const_equiv // left_id.
95
96
    rewrite comm. apply sep_mono; first done.
    apply equiv_spec, own_proper. split; first split; simpl.
Ralf Jung's avatar
Ralf Jung committed
97
    - intros Hdisj. split_ands; first by solve_elem_of+.
98
99
      + done.
      + constructor; [done | solve_elem_of-].
100
    - intros _. by eapply closed_disjoint'.
Ralf Jung's avatar
Ralf Jung committed
101
    - intros _. constructor. solve_elem_of+.
102
103
  Qed.

Ralf Jung's avatar
Ralf Jung committed
104
  Lemma closing E γ s T s' T' :
Ralf Jung's avatar
Ralf Jung committed
105
106
107
    step sts (s, T) (s', T') 
    ( φ s'  own StsI γ (auth sts s T))
     pvs E E ( inv StsI sts γ φ  in_state StsI sts γ s' T').
108
  Proof.
Ralf Jung's avatar
Ralf Jung committed
109
    intros Hstep. rewrite /inv /in_states -(exist_intro s').
Ralf Jung's avatar
Ralf Jung committed
110
111
112
    rewrite later_sep [(_  ▷φ _)%I]comm -assoc.
    rewrite -pvs_frame_l. apply sep_mono; first done.
    rewrite -later_intro.
Ralf Jung's avatar
Ralf Jung committed
113
114
115
    rewrite own_valid_l discrete_validI. apply const_elim_sep_l=>Hval.
    simpl in Hval. transitivity (pvs E E (own StsI γ (auth sts s' T'))).
    { by apply own_update, sts.update_auth. }
Ralf Jung's avatar
Ralf Jung committed
116
117
    apply pvs_mono. rewrite -own_op. apply equiv_spec, own_proper.
    split; first split; simpl.
Ralf Jung's avatar
Ralf Jung committed
118
119
    - intros _.
      set Tf := set_all  sts.(tok) s  T.
Ralf Jung's avatar
Ralf Jung committed
120
      assert (closed sts (up sts s Tf) Tf).
Ralf Jung's avatar
Ralf Jung committed
121
122
123
124
125
126
127
128
      { apply closed_up. rewrite /Tf. solve_elem_of+. }
      eapply step_closed; [done..| |].
      + apply elem_of_up.
      + rewrite /Tf. solve_elem_of+.
    - intros ?. split_ands; first by solve_elem_of+.
      + apply closed_up. done.
      + constructor; last solve_elem_of+. apply elem_of_up.
    - intros _. constructor. solve_elem_of+.
Ralf Jung's avatar
Ralf Jung committed
129
  Qed.
130

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

Ralf Jung's avatar
Ralf Jung committed
133
134
  Lemma states_fsa E N P (Q : V  iPropG Λ Σ) γ S T :
    fsaV  nclose N  E 
135
    P  ctx StsI sts γ N φ 
Ralf Jung's avatar
Ralf Jung committed
136
    P  (in_states StsI sts γ S T   s,
137
           (s  S)   φ s -
Ralf Jung's avatar
Ralf Jung committed
138
          fsa (E  nclose N) (λ x,  s' T',
Ralf Jung's avatar
Ralf Jung committed
139
140
             (step sts (s, T) (s', T'))   φ s' 
            (in_state StsI sts γ s' T' - Q x))) 
141
142
    P  fsa E Q.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
143
    rewrite /ctx=>? HN Hinv Hinner.
144
145
146
147
148
149
150
151
    eapply (inv_fsa fsa); eauto. rewrite Hinner=>{Hinner Hinv P HN}.
    apply wand_intro_l. rewrite assoc.
    rewrite (opened (E  N)) !pvs_frame_r !sep_exist_r.
    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
152
    apply (fsa_mono_pvs fsa)=> x.
153
    rewrite sep_exist_l; apply exist_elim=> s'.
Ralf Jung's avatar
Ralf Jung committed
154
155
    rewrite sep_exist_l; apply exist_elim=>T'.
    rewrite comm -!assoc. apply const_elim_sep_l=>-Hstep.
156
157
158
159
160
161
    rewrite assoc [(_  (_ - _))%I]comm -assoc.
    rewrite (closing (E  N)) //; [].
    rewrite pvs_frame_l. apply pvs_mono.
    by rewrite assoc [(_  _)%I]comm -assoc wand_elim_l.
  Qed.

Ralf Jung's avatar
Ralf Jung committed
162
163
164
  Lemma state_fsa E N P (Q : V  iPropG Λ Σ) γ s0 T :
    fsaV  nclose N  E 
    P  ctx StsI sts γ N φ 
Ralf Jung's avatar
Ralf Jung committed
165
166
    P  (in_state StsI sts γ s0 T   s,
           (s  up sts s0 T)   φ s -
Ralf Jung's avatar
Ralf Jung committed
167
          fsa (E  nclose N) (λ x,  s' T',
Ralf Jung's avatar
Ralf Jung committed
168
169
             (step sts (s, T) (s', T'))   φ s' 
            (in_state StsI sts γ s' T' - Q x))) 
Ralf Jung's avatar
Ralf Jung committed
170
171
172
173
174
    P  fsa E Q.
  Proof.
    rewrite {1}/state. apply states_fsa.
  Qed.

175
176
End sts.

Ralf Jung's avatar
Ralf Jung committed
177
End sts.