pviewshifts.v 10.5 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.
5 6
Local Hint Extern 100 (@eq coPset _ _) => set_solver.
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 σ,
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 36 37 38 39 40
Notation "|={ E1 , E2 }=> Q" := (pvs E1 E2 Q%I)
  (at level 199, E1, E2 at level 50, Q at level 200,
   format "|={ E1 , E2 }=>  Q") : uPred_scope.
Notation "|={ E }=> Q" := (pvs E E Q%I)
  (at level 199, E at level 50, Q at level 200,
   format "|={ E }=>  Q") : uPred_scope.
41 42
Notation "|==> Q" := (pvs   Q%I)
  (at level 199, 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
Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
50
Proof.
Ralf Jung's avatar
Ralf Jung committed
51
  rewrite pvs_eq.
52
  intros P Q HPQ; split=> n' r1 ??; simpl; split; intros HP rf k Ef σ ???;
Robbert Krebbers's avatar
Robbert Krebbers committed
53
    destruct (HP rf k Ef σ) as (r2&?&?); auto;
54
    exists r2; split_and?; auto; apply HPQ; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
55
Qed.
56
Global Instance pvs_proper E1 E2 : Proper (() ==> ()) (@pvs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
57 58
Proof. apply ne_proper, _. Qed.

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

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

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

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

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

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

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

217 218
Section fsa.
Context {Λ Σ A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa}.
219
Implicit Types Φ Ψ : A  iProp Λ Σ.
220

221
Lemma fsa_mono E Φ Ψ : ( a, Φ a  Ψ a)  fsa E Φ  fsa E Ψ.
222
Proof. apply fsa_mask_frame_mono; auto. Qed.
223
Lemma fsa_mask_weaken E1 E2 Φ : E1  E2  fsa E1 Φ  fsa E2 Φ.
224
Proof. intros. apply fsa_mask_frame_mono; auto. Qed.
225
Lemma fsa_frame_l E P Φ : (P  fsa E Φ)  fsa E (λ a, P  Φ a).
226
Proof. rewrite comm fsa_frame_r. apply fsa_mono=>a. by rewrite comm. Qed.
227
Lemma fsa_strip_pvs E P Φ : P  fsa E Φ  (|={E}=> P)  fsa E Φ.
228
Proof.
229 230
  move=>->. rewrite -{2}fsa_trans3.
  apply pvs_mono, fsa_mono=>a; apply pvs_intro.
231
Qed.
232
Lemma fsa_mono_pvs E Φ Ψ : ( a, Φ a  (|={E}=> Ψ a))  fsa E Φ  fsa E Ψ.
233
Proof. intros. rewrite -[fsa E Ψ]fsa_trans3 -pvs_intro. by apply fsa_mono. Qed.
234 235
End fsa.

236
Definition pvs_fsa {Λ Σ} : FSA Λ Σ () := λ E Φ, (|={E}=> Φ ())%I.
237
Instance pvs_fsa_prf {Λ Σ} : FrameShiftAssertion True (@pvs_fsa Λ Σ).
238
Proof.
239 240
  rewrite /pvs_fsa.
  split; auto using pvs_mask_frame_mono, pvs_trans3, pvs_frame_r.
241
Qed.
242 243

Lemma pvs_mk_fsa {Λ Σ} E (P Q : iProp Λ Σ) :
244 245
  P  pvs_fsa E (λ _, Q) 
  P  |={E}=> Q.
246
Proof. by intros ?. Qed.