pviewshifts.v 11.3 KB
Newer Older
1 2 3
From iris.prelude Require Export co_pset.
From iris.program_logic Require Export model.
From iris.program_logic Require Import ownership wsat.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
Local Hint Extern 10 (_  _) => omega.
Robbert Krebbers's avatar
Robbert Krebbers committed
5
Local Hint Extern 100 (_  _) => set_solver.
6
Local Hint Extern 100 (_  _) => set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
Local Hint Extern 10 ({_} _) =>
8 9 10
  repeat match goal with
  | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega
  end; solve_validN.
Robbert Krebbers's avatar
Robbert Krebbers committed
11

Ralf Jung's avatar
Ralf Jung committed
12
Program Definition pvs_def {Λ Σ} (E1 E2 : coPset) (P : iProp Λ Σ) : iProp Λ Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
13
  {| uPred_holds n r1 :=  rf k Ef σ,
Robbert Krebbers's avatar
Robbert Krebbers committed
14
       0 < k  n  E1  E2  Ef 
Robbert Krebbers's avatar
Robbert Krebbers committed
15 16 17
       wsat k (E1  Ef) σ (r1  rf) 
        r2, P k r2  wsat k (E2  Ef) σ (r2  rf) |}.
Next Obligation.
18 19
  intros Λ Σ E1 E2 P n r1 r2 HP [r3 Hr2] rf k Ef σ ??.
  rewrite (dist_le _ _ _ _ Hr2); last lia. intros Hws.
20
  destruct (HP (r3  rf) k Ef σ) as (r'&?&Hws'); rewrite ?(assoc op); auto.
21
  exists (r'  r3); rewrite -assoc; split; last done.
22
  apply uPred_mono with r'; eauto using cmra_includedN_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
23
Qed.
24
Next Obligation. naive_solver. Qed.
Ralf Jung's avatar
Ralf Jung committed
25 26 27 28 29 30

Definition pvs_aux : { x | x = @pvs_def }. by eexists. Qed.
Definition pvs := proj1_sig pvs_aux.
Definition pvs_eq : @pvs = @pvs_def := proj2_sig pvs_aux.

Arguments pvs {_ _} _ _ _%I.
31
Instance: Params (@pvs) 4.
Robbert Krebbers's avatar
Robbert Krebbers committed
32

33
Notation "|={ E1 , E2 }=> Q" := (pvs E1 E2 Q%I)
34
  (at level 99, E1, E2 at level 50, Q at level 200,
35 36
   format "|={ E1 , E2 }=>  Q") : uPred_scope.
Notation "|={ E }=> Q" := (pvs E E Q%I)
37
  (at level 99, E at level 50, Q at level 200,
38
   format "|={ E }=>  Q") : uPred_scope.
39
Notation "|==> Q" := (pvs   Q%I)
40
  (at level 99, Q at level 200, format "|==>  Q") : uPred_scope.
41

Robbert Krebbers's avatar
Robbert Krebbers committed
42
Section pvs.
43
Context {Λ : language} {Σ : iFunctor}.
44 45
Implicit Types P Q : iProp Λ Σ.
Implicit Types m : iGst Λ Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
46

47 48 49
Lemma pvs_zero E1 E2 P r : pvs_def E1 E2 P 0 r.
Proof. intros ?????. exfalso. omega. Qed.

50
Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
51
Proof.
Ralf Jung's avatar
Ralf Jung committed
52
  rewrite pvs_eq.
53
  intros P Q HPQ; split=> n' r1 ??; simpl; split; intros HP rf k Ef σ ???;
Robbert Krebbers's avatar
Robbert Krebbers committed
54
    destruct (HP rf k Ef σ) as (r2&?&?); auto;
55
    exists r2; split_and?; auto; apply HPQ; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
56
Qed.
57
Global Instance pvs_proper E1 E2 : Proper (() ==> ()) (@pvs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
58 59
Proof. apply ne_proper, _. Qed.

60
Lemma pvs_intro E P : P  |={E}=> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
61
Proof.
Ralf Jung's avatar
Ralf Jung committed
62
  rewrite pvs_eq. split=> n r ? HP rf k Ef σ ???; exists r; split; last done.
63
  apply uPred_closed with n; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
64
Qed.
65
Lemma pvs_mono E1 E2 P Q : P  Q  (|={E1,E2}=> P)  (|={E1,E2}=> Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
66
Proof.
Ralf Jung's avatar
Ralf Jung committed
67
  rewrite pvs_eq. intros HPQ; split=> n r ? HP rf k Ef σ ???.
68 69
  destruct (HP rf k Ef σ) as (r2&?&?); eauto.
  exists r2; eauto using uPred_in_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
70
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
71
Lemma pvs_timeless E P : TimelessP P   P  (|={E}=> P).
Robbert Krebbers's avatar
Robbert Krebbers committed
72
Proof.
Ralf Jung's avatar
Ralf Jung committed
73
  rewrite pvs_eq uPred.timelessP_spec=> HP.
74
  uPred.unseal; split=>-[|n] r ? HP' rf k Ef σ ???; first lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
75
  exists r; split; last done.
76
  apply HP, uPred_closed with n; eauto using cmra_validN_le.
Robbert Krebbers's avatar
Robbert Krebbers committed
77 78
Qed.
Lemma pvs_trans E1 E2 E3 P :
79
  E2  E1  E3  (|={E1,E2}=> |={E2,E3}=> P)  (|={E1,E3}=> P).
Robbert Krebbers's avatar
Robbert Krebbers committed
80
Proof.
Ralf Jung's avatar
Ralf Jung committed
81
  rewrite pvs_eq. intros ?; split=> n r1 ? HP1 rf k Ef σ ???.
Robbert Krebbers's avatar
Robbert Krebbers committed
82 83 84
  destruct (HP1 rf k Ef σ) as (r2&HP2&?); auto.
Qed.
Lemma pvs_mask_frame E1 E2 Ef P :
Robbert Krebbers's avatar
Robbert Krebbers committed
85
  Ef  E1  E2  (|={E1,E2}=> P)  (|={E1  Ef,E2  Ef}=> P).
Robbert Krebbers's avatar
Robbert Krebbers committed
86
Proof.
Ralf Jung's avatar
Ralf Jung committed
87
  rewrite pvs_eq. intros ?; split=> n r ? HP rf k Ef' σ ???.
88 89
  destruct (HP rf k (EfEf') σ) as (r'&?&?); rewrite ?(assoc_L _); eauto.
  by exists r'; rewrite -(assoc_L _).
Robbert Krebbers's avatar
Robbert Krebbers committed
90
Qed.
91
Lemma pvs_frame_r E1 E2 P Q : ((|={E1,E2}=> P)  Q)  (|={E1,E2}=> P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
92
Proof.
Ralf Jung's avatar
Ralf Jung committed
93
  rewrite pvs_eq. uPred.unseal; split; intros n r ? (r1&r2&Hr&HP&?) rf k Ef σ ???.
Robbert Krebbers's avatar
Robbert Krebbers committed
94
  destruct (HP (r2  rf) k Ef σ) as (r'&?&?); eauto.
95 96
  { by rewrite assoc -(dist_le _ _ _ _ Hr); last lia. }
  exists (r'  r2); split; last by rewrite -assoc.
97
  exists r', r2; split_and?; auto. apply uPred_closed with n; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
98
Qed.
99
Lemma pvs_openI i P : ownI i P  (|={{[i]},}=>  P).
Robbert Krebbers's avatar
Robbert Krebbers committed
100
Proof.
Ralf Jung's avatar
Ralf Jung committed
101
  rewrite pvs_eq. uPred.unseal; split=> -[|n] r ? Hinv rf [|k] Ef σ ???; try lia.
102
  apply ownI_spec in Hinv; last auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
103 104
  destruct (wsat_open k Ef σ (r  rf) i P) as (rP&?&?); auto.
  { rewrite lookup_wld_op_l ?Hinv; eauto; apply dist_le with (S n); eauto. }
105
  exists (rP  r); split; last by rewrite (left_id_L _ _) -assoc.
106
  eapply uPred_mono with rP; eauto using cmra_includedN_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
107
Qed.
108
Lemma pvs_closeI i P : (ownI i P   P)  (|={,{[i]}}=> True).
Robbert Krebbers's avatar
Robbert Krebbers committed
109
Proof.
Ralf Jung's avatar
Ralf Jung committed
110
  rewrite pvs_eq. uPred.unseal; split=> -[|n] r ? [? HP] rf [|k] Ef σ ? HE ?; try lia.
111
  exists ; split; [done|].
112
  rewrite left_id; apply wsat_close with P r.
113
  - apply ownI_spec, uPred_closed with (S n); auto.
114
  - set_solver +HE.
115
  - by rewrite -(left_id_L  () Ef).
116
  - apply uPred_closed with n; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
117
Qed.
118
Lemma pvs_ownG_updateP E m (P : iGst Λ Σ  Prop) :
119
  m ~~>: P  ownG m  (|={E}=>  m',  P m'  ownG m').
Robbert Krebbers's avatar
Robbert Krebbers committed
120
Proof.
121
  rewrite pvs_eq. intros Hup.
122
  uPred.unseal; split=> -[|n] r ? /ownG_spec Hinv rf [|k] Ef σ ???; try lia.
123
  destruct (wsat_update_gst k (E  Ef) σ r rf m P) as (m'&?&?); eauto.
124
  { apply cmra_includedN_le with (S n); auto. }
Robbert Krebbers's avatar
Robbert Krebbers committed
125 126
  by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|].
Qed.
127
Lemma pvs_allocI E P : ¬set_finite E   P  (|={E}=>  i,  (i  E)  ownI i P).
Robbert Krebbers's avatar
Robbert Krebbers committed
128
Proof.
Ralf Jung's avatar
Ralf Jung committed
129
  rewrite pvs_eq. intros ?; rewrite /ownI; uPred.unseal.
130
  split=> -[|n] r ? HP rf [|k] Ef σ ???; try lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
131
  destruct (wsat_alloc k E Ef σ rf P r) as (i&?&?&?); auto.
132
  { apply uPred_closed with n; eauto. }
133
  exists (Res {[ i := to_agree (Next (iProp_unfold P)) ]}  ).
134
  split; [|done]. by exists i; split; rewrite /uPred_holds /=.
Robbert Krebbers's avatar
Robbert Krebbers committed
135 136
Qed.

137
(** * Derived rules *)
Robbert Krebbers's avatar
Robbert Krebbers committed
138
Import uPred.
139
Global Instance pvs_mono' E1 E2 : Proper (() ==> ()) (@pvs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
140
Proof. intros P Q; apply pvs_mono. Qed.
141
Global Instance pvs_flip_mono' E1 E2 :
142
  Proper (flip () ==> flip ()) (@pvs Λ Σ E1 E2).
143
Proof. intros P Q; apply pvs_mono. Qed.
144
Lemma pvs_trans' E P : (|={E}=> |={E}=> P)  (|={E}=> P).
145
Proof. apply pvs_trans; set_solver. Qed.
146
Lemma pvs_strip_pvs E P Q : P  (|={E}=> Q)  (|={E}=> P)  (|={E}=> Q).
147
Proof. move=>->. by rewrite pvs_trans'. Qed.
148
Lemma pvs_frame_l E1 E2 P Q : (P  |={E1,E2}=> Q)  (|={E1,E2}=> P  Q).
149
Proof. rewrite !(comm _ P); apply pvs_frame_r. Qed.
150
Lemma pvs_always_l E1 E2 P Q `{!PersistentP P} :
151
  (P  |={E1,E2}=> Q)  (|={E1,E2}=> P  Q).
152
Proof. by rewrite !always_and_sep_l pvs_frame_l. Qed.
153
Lemma pvs_always_r E1 E2 P Q `{!PersistentP Q} :
154
  ((|={E1,E2}=> P)  Q)  (|={E1,E2}=> P  Q).
155
Proof. by rewrite !always_and_sep_r pvs_frame_r. Qed.
156
Lemma pvs_impl_l E1 E2 P Q : ( (P  Q)  (|={E1,E2}=> P))  (|={E1,E2}=> Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
157
Proof. by rewrite pvs_always_l always_elim impl_elim_l. Qed.
158
Lemma pvs_impl_r E1 E2 P Q : ((|={E1,E2}=> P)   (P  Q))  (|={E1,E2}=> Q).
159
Proof. by rewrite comm pvs_impl_l. Qed.
160 161 162 163
Lemma pvs_wand_l E1 E2 P Q : ((P - Q)  (|={E1,E2}=> P))  (|={E1,E2}=> Q).
Proof. by rewrite pvs_frame_l wand_elim_l. Qed.
Lemma pvs_wand_r E1 E2 P Q : ((|={E1,E2}=> P)  (P - Q))  (|={E1,E2}=> Q).
Proof. by rewrite pvs_frame_r wand_elim_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
164
Lemma pvs_sep E P Q : ((|={E}=> P)  (|={E}=> Q))  (|={E}=> P  Q).
Ralf Jung's avatar
Ralf Jung committed
165
Proof. rewrite pvs_frame_r pvs_frame_l pvs_trans //. set_solver. Qed.
166

167
Lemma pvs_mask_frame' E1 E1' E2 E2' P :
168
  E1'  E1  E2'  E2  E1  E1' = E2  E2' 
169
  (|={E1',E2'}=> P)  (|={E1,E2}=> P).
170
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
171
  intros HE1 HE2 HEE.
172
  rewrite (pvs_mask_frame _ _ (E1  E1')); last set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
173
  by rewrite {2}HEE -!union_difference_L.
174
Qed.
175 176 177 178
Lemma pvs_openI' E i P : i  E  ownI i P  (|={E, E  {[i]}}=>  P).
Proof. intros. etrans. apply pvs_openI. apply pvs_mask_frame'; set_solver. Qed.
Lemma pvs_closeI' E i P : i  E  (ownI i P   P)  (|={E  {[i]}, E}=> True).
Proof. intros. etrans. apply pvs_closeI. apply pvs_mask_frame'; set_solver. Qed.
179 180 181

Lemma pvs_mask_frame_mono E1 E1' E2 E2' P Q :
  E1'  E1  E2'  E2  E1  E1' = E2  E2' 
182
  P  Q  (|={E1',E2'}=> P)  (|={E1,E2}=> Q).
183 184
Proof. intros HE1 HE2 HEE ->. by apply pvs_mask_frame'. Qed.

185
(** It should be possible to give a stronger version of this rule
Ralf Jung's avatar
Ralf Jung committed
186 187
   that does not force the conclusion view shift to have twice the
   same mask. However, even expressing the side-conditions on the
188
   mask becomes really ugly then, and we have not found an instance
Ralf Jung's avatar
Ralf Jung committed
189
   where that would be useful. *)
Ralf Jung's avatar
Ralf Jung committed
190
Lemma pvs_trans3 E1 E2 Q :
191
  E2  E1  (|={E1,E2}=> |={E2}=> |={E2,E1}=> Q)  (|={E1}=> Q).
192
Proof. intros HE. rewrite !pvs_trans; set_solver. Qed.
Ralf Jung's avatar
Ralf Jung committed
193

194
Lemma pvs_mask_weaken E1 E2 P : E1  E2  (|={E1}=> P)  (|={E2}=> P).
Robbert Krebbers's avatar
Robbert Krebbers committed
195
Proof. auto using pvs_mask_frame'. Qed.
196

197
Lemma pvs_ownG_update E m m' : m ~~> m'  ownG m  (|={E}=> ownG m').
Robbert Krebbers's avatar
Robbert Krebbers committed
198
Proof.
199
  intros; rewrite (pvs_ownG_updateP E _ (m' =)); last by apply cmra_update_updateP.
Robbert Krebbers's avatar
Robbert Krebbers committed
200 201 202
  by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.const_elim_l=> ->.
Qed.
End pvs.
203 204 205 206 207 208

(** * Frame Shift Assertions. *)
(* Yes, the name is horrible...
   Frame Shift Assertions take a mask and a predicate over some type (that's
   their "postcondition"). They support weakening the mask, framing resources
   into the postcondition, and composition witn mask-changing view shifts. *)
209 210
Notation FSA Λ Σ A := (coPset  (A  iProp Λ Σ)  iProp Λ Σ).
Class FrameShiftAssertion {Λ Σ A} (fsaV : Prop) (fsa : FSA Λ Σ A) := {
211
  fsa_mask_frame_mono E1 E2 Φ Ψ :
212 213
    E1  E2  ( a, Φ a  Ψ a)  fsa E1 Φ  fsa E2 Ψ;
  fsa_trans3 E Φ : (|={E}=> fsa E (λ a, |={E}=> Φ a))  fsa E Φ;
214
  fsa_open_close E1 E2 Φ :
215 216
    fsaV  E2  E1  (|={E1,E2}=> fsa E2 (λ a, |={E2,E1}=> Φ a))  fsa E1 Φ;
  fsa_frame_r E P Φ : (fsa E Φ  P)  fsa E (λ a, Φ a  P)
217 218
}.

219 220
Section fsa.
Context {Λ Σ A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa}.
221
Implicit Types Φ Ψ : A  iProp Λ Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
222
Import uPred.
223

224
Lemma fsa_mono E Φ Ψ : ( a, Φ a  Ψ a)  fsa E Φ  fsa E Ψ.
225
Proof. apply fsa_mask_frame_mono; auto. Qed.
226
Lemma fsa_mask_weaken E1 E2 Φ : E1  E2  fsa E1 Φ  fsa E2 Φ.
227
Proof. intros. apply fsa_mask_frame_mono; auto. Qed.
228
Lemma fsa_frame_l E P Φ : (P  fsa E Φ)  fsa E (λ a, P  Φ a).
229
Proof. rewrite comm fsa_frame_r. apply fsa_mono=>a. by rewrite comm. Qed.
230
Lemma fsa_strip_pvs E P Φ : P  fsa E Φ  (|={E}=> P)  fsa E Φ.
231
Proof.
232 233
  move=>->. rewrite -{2}fsa_trans3.
  apply pvs_mono, fsa_mono=>a; apply pvs_intro.
234
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
235 236
Lemma fsa_pvs_fsa E Φ : (|={E}=> fsa E Φ)  fsa E Φ.
Proof. apply (anti_symm ()); [by apply fsa_strip_pvs|apply pvs_intro]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
237 238 239 240 241
Lemma pvs_fsa_fsa E Φ : fsa E (λ a, |={E}=> Φ a)  fsa E Φ.
Proof.
  apply (anti_symm ()); [|apply fsa_mono=> a; apply pvs_intro].
  by rewrite (pvs_intro E (fsa E _)) fsa_trans3.
Qed.
242
Lemma fsa_mono_pvs E Φ Ψ : ( a, Φ a  (|={E}=> Ψ a))  fsa E Φ  fsa E Ψ.
243
Proof. intros. rewrite -[fsa E Ψ]fsa_trans3 -pvs_intro. by apply fsa_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
244 245 246 247 248 249 250
Lemma fsa_wand_l E Φ Ψ : (( a, Φ a - Ψ a)  fsa E Φ)  (fsa E Ψ).
Proof.
  rewrite fsa_frame_l. apply fsa_mono=> a.
  by rewrite (forall_elim a) wand_elim_l.
Qed.
Lemma fsa_wand_r E Φ Ψ : (fsa E Φ   a, Φ a - Ψ a)  (fsa E Ψ).
Proof. by rewrite (comm _ (fsa _ _)) fsa_wand_l. Qed.
251 252
End fsa.

253
Definition pvs_fsa {Λ Σ} : FSA Λ Σ () := λ E Φ, (|={E}=> Φ ())%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
254 255
Arguments pvs_fsa _ _ _ _/.

256
Instance pvs_fsa_prf {Λ Σ} : FrameShiftAssertion True (@pvs_fsa Λ Σ).
257
Proof.
258 259
  rewrite /pvs_fsa.
  split; auto using pvs_mask_frame_mono, pvs_trans3, pvs_frame_r.
260
Qed.