pviewshifts.v 11.4 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
  intros Λ Σ E1 E2 P r1 r2 n HP Hr rf k Ef σ ?? Hwsat; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
19 20 21
  apply HP; auto. by rewrite (dist_le _ _ _ _ Hr); last lia.
Qed.
Next Obligation.
22 23
  intros Λ Σ E1 E2 P n r1 r2 HP [r3 ?] rf k Ef σ ?? Hws; setoid_subst.
  destruct (HP (r3  rf) k Ef σ) as (r'&?&Hws'); rewrite ?(assoc op); auto.
24
  exists (r'  r3); rewrite -assoc; split; last done.
25
  apply uPred_mono with r'; eauto using cmra_included_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
26
Qed.
27
Next Obligation. naive_solver. Qed.
Ralf Jung's avatar
Ralf Jung committed
28 29 30 31 32 33

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.
34
Instance: Params (@pvs) 4.
Robbert Krebbers's avatar
Robbert Krebbers committed
35

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

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

50 51 52
Lemma pvs_zero E1 E2 P r : pvs_def E1 E2 P 0 r.
Proof. intros ?????. exfalso. omega. Qed.

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

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

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

170
Lemma pvs_mask_frame' E1 E1' E2 E2' P :
171
  E1'  E1  E2'  E2  E1  E1' = E2  E2' 
172
  (|={E1',E2'}=> P)  (|={E1,E2}=> P).
173
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
174
  intros HE1 HE2 HEE.
175
  rewrite (pvs_mask_frame _ _ (E1  E1')); last set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
176
  by rewrite {2}HEE -!union_difference_L.
177
Qed.
178 179 180 181
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.
Ralf Jung's avatar
Ralf Jung committed
182 183 184

Lemma pvs_mask_frame_mono E1 E1' E2 E2' P Q :
  E1'  E1  E2'  E2  E1  E1' = E2  E2' 
185
  P  Q  (|={E1',E2'}=> P)  (|={E1,E2}=> Q).
Ralf Jung's avatar
Ralf Jung committed
186 187
Proof. intros HE1 HE2 HEE ->. by apply pvs_mask_frame'. Qed.

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

197
Lemma pvs_mask_weaken E1 E2 P : E1  E2  (|={E1}=> P)  (|={E2}=> P).
Robbert Krebbers's avatar
Robbert Krebbers committed
198
Proof. auto using pvs_mask_frame'. Qed.
Ralf Jung's avatar
Ralf Jung committed
199

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

(** * 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. *)
212 213
Notation FSA Λ Σ A := (coPset  (A  iProp Λ Σ)  iProp Λ Σ).
Class FrameShiftAssertion {Λ Σ A} (fsaV : Prop) (fsa : FSA Λ Σ A) := {
214
  fsa_mask_frame_mono E1 E2 Φ Ψ :
215 216
    E1  E2  ( a, Φ a  Ψ a)  fsa E1 Φ  fsa E2 Ψ;
  fsa_trans3 E Φ : (|={E}=> fsa E (λ a, |={E}=> Φ a))  fsa E Φ;
217
  fsa_open_close E1 E2 Φ :
218 219
    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)
220 221
}.

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

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

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

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