pviewshifts.v 10.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.
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 41
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.

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

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

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

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

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

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

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

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

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

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

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

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