pviewshifts.v 10.6 KB
Newer Older
1 2 3
From prelude Require Export co_pset.
From program_logic Require Export model.
From 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

12
Program Definition pvs {Λ Σ} (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.
27 28
Arguments pvs {_ _} _ _ _%I : simpl never.
Instance: Params (@pvs) 4.
Robbert Krebbers's avatar
Robbert Krebbers committed
29

30 31 32 33 34 35 36
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
37
Section pvs.
38 39 40
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P Q : iProp Λ Σ.
Implicit Types m : iGst Λ Σ.
41
Transparent uPred_holds.
Robbert Krebbers's avatar
Robbert Krebbers committed
42

43
Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
44
Proof.
45
  intros P Q HPQ; split=> n' r1 ??; simpl; split; intros HP rf k Ef σ ???;
Robbert Krebbers's avatar
Robbert Krebbers committed
46
    destruct (HP rf k Ef σ) as (r2&?&?); auto;
47
    exists r2; split_and?; auto; apply HPQ; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
48
Qed.
49
Global Instance pvs_proper E1 E2 : Proper (() ==> ()) (@pvs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
50 51
Proof. apply ne_proper, _. Qed.

52
Lemma pvs_intro E P : P  |={E}=> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
53
Proof.
54
  split=> n r ? HP rf k Ef σ ???; exists r; split; last done.
Robbert Krebbers's avatar
Robbert Krebbers committed
55
  apply uPred_weaken with n r; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
56
Qed.
57
Lemma pvs_mono E1 E2 P Q : P  Q  (|={E1,E2}=> P)  (|={E1,E2}=> Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
58
Proof.
59 60 61
  intros HPQ; split=> n r ? HP rf k Ef σ ???.
  destruct (HP rf k Ef σ) as (r2&?&?); eauto.
  exists r2; eauto using uPred_in_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
Qed.
63
Lemma pvs_timeless E P : TimelessP P  ( P)  (|={E}=> P).
Robbert Krebbers's avatar
Robbert Krebbers committed
64
Proof.
65
  rewrite uPred.timelessP_spec=> HP.
66
  uPred.unseal; split=>-[|n] r ? HP' rf k Ef σ ???; first lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
67
  exists r; split; last done.
Robbert Krebbers's avatar
Robbert Krebbers committed
68
  apply HP, uPred_weaken with n r; eauto using cmra_validN_le.
Robbert Krebbers's avatar
Robbert Krebbers committed
69 70
Qed.
Lemma pvs_trans E1 E2 E3 P :
71
  E2  E1  E3  (|={E1,E2}=> |={E2,E3}=> P)  (|={E1,E3}=> P).
Robbert Krebbers's avatar
Robbert Krebbers committed
72
Proof.
73
  intros ?; split=> n r1 ? HP1 rf k Ef σ ???.
Robbert Krebbers's avatar
Robbert Krebbers committed
74 75 76
  destruct (HP1 rf k Ef σ) as (r2&HP2&?); auto.
Qed.
Lemma pvs_mask_frame E1 E2 Ef P :
77
  Ef  (E1  E2) =   (|={E1,E2}=> P)  (|={E1  Ef,E2  Ef}=> P).
Robbert Krebbers's avatar
Robbert Krebbers committed
78
Proof.
79
  intros ?; split=> n r ? HP rf k Ef' σ ???.
80 81
  destruct (HP rf k (EfEf') σ) as (r'&?&?); rewrite ?(assoc_L _); eauto.
  by exists r'; rewrite -(assoc_L _).
Robbert Krebbers's avatar
Robbert Krebbers committed
82
Qed.
83
Lemma pvs_frame_r E1 E2 P Q : ((|={E1,E2}=> P)  Q)  (|={E1,E2}=> P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
84
Proof.
85
  uPred.unseal; split; intros n r ? (r1&r2&Hr&HP&?) rf k Ef σ ???.
Robbert Krebbers's avatar
Robbert Krebbers committed
86
  destruct (HP (r2  rf) k Ef σ) as (r'&?&?); eauto.
87 88
  { by rewrite assoc -(dist_le _ _ _ _ Hr); last lia. }
  exists (r'  r2); split; last by rewrite -assoc.
89
  exists r', r2; split_and?; auto; apply uPred_weaken with n r2; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
90
Qed.
91
Lemma pvs_openI i P : ownI i P  (|={{[i]},}=>  P).
Robbert Krebbers's avatar
Robbert Krebbers committed
92
Proof.
93
  uPred.unseal; split=> -[|n] r ? Hinv rf [|k] Ef σ ???; try lia.
94
  apply ownI_spec in Hinv; last auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
95 96
  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. }
97
  exists (rP  r); split; last by rewrite (left_id_L _ _) -assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
98
  eapply uPred_weaken with (S k) rP; eauto using cmra_included_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
99
Qed.
100
Lemma pvs_closeI i P : (ownI i P   P)  (|={,{[i]}}=> True).
Robbert Krebbers's avatar
Robbert Krebbers committed
101
Proof.
102
  uPred.unseal; split=> -[|n] r ? [? HP] rf [|k] Ef σ ? HE ?; try lia.
103
  exists ; split; [done|].
104
  rewrite left_id; apply wsat_close with P r.
Robbert Krebbers's avatar
Robbert Krebbers committed
105
  - apply ownI_spec, uPred_weaken with (S n) r; auto.
106
  - set_solver +HE.
107
  - by rewrite -(left_id_L  () Ef).
Robbert Krebbers's avatar
Robbert Krebbers committed
108
  - apply uPred_weaken with n r; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
109
Qed.
110
Lemma pvs_ownG_updateP E m (P : iGst Λ Σ  Prop) :
111
  m ~~>: P  ownG m  (|={E}=>  m',  P m'  ownG m').
Robbert Krebbers's avatar
Robbert Krebbers committed
112
Proof.
113
  intros Hup%option_updateP'.
114
  uPred.unseal; split=> -[|n] r ? /ownG_spec Hinv rf [|k] Ef σ ???; try lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
115
  destruct (wsat_update_gst k (E  Ef) σ r rf (Some m) P) as (m'&?&?); eauto.
116
  { apply cmra_includedN_le with (S n); auto. }
Robbert Krebbers's avatar
Robbert Krebbers committed
117 118
  by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|].
Qed.
119
Lemma pvs_ownG_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)}
Robbert Krebbers's avatar
Robbert Krebbers committed
120
    E (P : iGst Λ Σ  Prop) :
121
   ~~>: P  True  (|={E}=>  m',  P m'  ownG m').
Robbert Krebbers's avatar
Robbert Krebbers committed
122
Proof.
123
  intros Hup; uPred.unseal; split=> -[|n] r ? _ rf [|k] Ef σ ???; try lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
124 125 126 127
  destruct (wsat_update_gst k (E  Ef) σ r rf  P) as (m'&?&?); eauto.
  { apply cmra_empty_leastN. }
  { apply cmra_updateP_compose_l with (Some ), option_updateP with P;
      auto using option_update_None. }
128
  exists (update_gst m' r); by split; [exists m'; split; [|apply ownG_spec]|].
Robbert Krebbers's avatar
Robbert Krebbers committed
129
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.
132 133
  intros ?; rewrite /ownI; uPred.unseal.
  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.
Robbert Krebbers's avatar
Robbert Krebbers committed
135
  { apply uPred_weaken with n r; 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 *)
141
Opaque uPred_holds.
Robbert Krebbers's avatar
Robbert Krebbers committed
142
Import uPred.
143
Global Instance pvs_mono' E1 E2 : Proper (() ==> ()) (@pvs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
144
Proof. intros P Q; apply pvs_mono. Qed.
145 146 147
Global Instance pvs_flip_mono' E1 E2 :
  Proper (flip () ==> flip ()) (@pvs Λ Σ E1 E2).
Proof. intros P Q; apply pvs_mono. Qed.
148
Lemma pvs_trans' E P : (|={E}=> |={E}=> P)  (|={E}=> P).
149
Proof. apply pvs_trans; set_solver. Qed.
150
Lemma pvs_strip_pvs E P Q : P  (|={E}=> Q)  (|={E}=> P)  (|={E}=> Q).
151
Proof. move=>->. by rewrite pvs_trans'. Qed.
152
Lemma pvs_frame_l E1 E2 P Q : (P  |={E1,E2}=> Q)  (|={E1,E2}=> P  Q).
153
Proof. rewrite !(comm _ P); apply pvs_frame_r. Qed.
154
Lemma pvs_always_l E1 E2 P Q `{!AlwaysStable P} :
155
  (P  |={E1,E2}=> Q)  (|={E1,E2}=> P  Q).
156
Proof. by rewrite !always_and_sep_l pvs_frame_l. Qed.
157
Lemma pvs_always_r E1 E2 P Q `{!AlwaysStable Q} :
158
  ((|={E1,E2}=> P)  Q)  (|={E1,E2}=> P  Q).
159
Proof. by rewrite !always_and_sep_r pvs_frame_r. Qed.
160
Lemma pvs_impl_l E1 E2 P Q : ( (P  Q)  (|={E1,E2}=> P))  (|={E1,E2}=> Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
161
Proof. by rewrite pvs_always_l always_elim impl_elim_l. Qed.
162
Lemma pvs_impl_r E1 E2 P Q : ((|={E1,E2}=> P)   (P  Q))  (|={E1,E2}=> Q).
163
Proof. by rewrite comm pvs_impl_l. Qed.
164
Lemma pvs_wand_l E1 E2 P Q R :
165
  P  (|={E1,E2}=> Q)  ((Q - R)  P)  (|={E1,E2}=> R).
166
Proof. intros ->. rewrite pvs_frame_l. apply pvs_mono, wand_elim_l. Qed.
167
Lemma pvs_wand_r E1 E2 P Q R :
168
  P  (|={E1,E2}=> Q)  (P  (Q - R))  (|={E1,E2}=> R).
169
Proof. rewrite comm. apply pvs_wand_l. Qed.
Ralf Jung's avatar
Ralf Jung committed
170 171 172
Lemma pvs_sep E P Q:
  ((|={E}=> P)  (|={E}=> Q))  (|={E}=> P  Q).
Proof. rewrite pvs_frame_r pvs_frame_l pvs_trans //. set_solver. Qed.
Ralf Jung's avatar
Ralf Jung committed
173

174
Lemma pvs_mask_frame' E1 E1' E2 E2' P :
175 176
  E1'  E1  E2'  E2  E1  E1' = E2  E2' 
  (|={E1',E2'}=> P)  (|={E1,E2}=> P).
177
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
178
  intros HE1 HE2 HEE.
179
  rewrite (pvs_mask_frame _ _ (E1  E1')); last set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
180
  by rewrite {2}HEE -!union_difference_L.
181
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 215
  fsa_mask_frame_mono E1 E2 Φ Ψ :
    E1  E2  ( a, Φ a  Ψ a)  fsa E1 Φ  fsa E2 Ψ;
216
  fsa_trans3 E Φ : (|={E}=> fsa E (λ a, |={E}=> Φ a))  fsa E Φ;
217
  fsa_open_close E1 E2 Φ :
218
    fsaV  E2  E1  (|={E1,E2}=> fsa E2 (λ a, |={E2,E1}=> Φ a))  fsa E1 Φ;
219
  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 Λ Σ.
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.
237
Lemma fsa_mono_pvs E Φ Ψ : ( a, Φ a  (|={E}=> Ψ a))  fsa E Φ  fsa E Ψ.
238
Proof. intros. rewrite -[fsa E Ψ]fsa_trans3 -pvs_intro. by apply fsa_mono. Qed.
239 240
End fsa.

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