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
  intros Λ Σ E1 E2 P r1 r2 n1 n2 HP [r3 ?] Hn ? rf k Ef σ ?? Hws; setoid_subst.
23 24
  destruct (HP (r3rf) k Ef σ) as (r'&?&Hws'); rewrite ?(assoc op); auto.
  exists (r'  r3); rewrite -assoc; split; last done.
Robbert Krebbers's avatar
Robbert Krebbers committed
25
  apply uPred_weaken with k r'; eauto using cmra_included_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
26
Qed.
Ralf Jung's avatar
Ralf Jung committed
27 28 29 30 31 32

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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