pviewshifts.v 10.9 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

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 44 45
Context {Λ : language} {Σ : iFunctor}.
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.
Ralf Jung's avatar
Ralf Jung committed
118
  rewrite pvs_eq. intros Hup%option_updateP'.
119
  uPred.unseal; split=> -[|n] r ? /ownG_spec Hinv rf [|k] Ef σ ???; try lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
120
  destruct (wsat_update_gst k (E  Ef) σ r rf (Some 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_ownG_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)}
Robbert Krebbers's avatar
Robbert Krebbers committed
125
    E (P : iGst Λ Σ  Prop) :
126
   ~~>: P  True  (|={E}=>  m',  P m'  ownG m').
Robbert Krebbers's avatar
Robbert Krebbers committed
127
Proof.
Ralf Jung's avatar
Ralf Jung committed
128
  rewrite pvs_eq. intros Hup; uPred.unseal; split=> -[|n] r ? _ rf [|k] Ef σ ???; try lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
129 130 131 132
  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. }
133
  exists (update_gst m' r); by split; [exists m'; split; [|apply ownG_spec]|].
Robbert Krebbers's avatar
Robbert Krebbers committed
134
Qed.
135
Lemma pvs_allocI E P : ¬set_finite E   P  (|={E}=>  i,  (i  E)  ownI i P).
Robbert Krebbers's avatar
Robbert Krebbers committed
136
Proof.
Ralf Jung's avatar
Ralf Jung committed
137
  rewrite pvs_eq. intros ?; rewrite /ownI; uPred.unseal.
138
  split=> -[|n] r ? HP rf [|k] Ef σ ???; try lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
139
  destruct (wsat_alloc k E Ef σ rf P r) as (i&?&?&?); auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
140
  { apply uPred_weaken with n r; eauto. }
141
  exists (Res {[ i := to_agree (Next (iProp_unfold P)) ]}  ).
142
  split; [|done]. by exists i; split; rewrite /uPred_holds /=.
Robbert Krebbers's avatar
Robbert Krebbers committed
143 144
Qed.

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

178
Lemma pvs_mask_frame' E1 E1' E2 E2' P :
179 180
  E1'  E1  E2'  E2  E1  E1' = E2  E2' 
  (|={E1',E2'}=> P)  (|={E1,E2}=> P).
181
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
182
  intros HE1 HE2 HEE.
183
  rewrite (pvs_mask_frame _ _ (E1  E1')); last set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
184
  by rewrite {2}HEE -!union_difference_L.
185
Qed.
Ralf Jung's avatar
Ralf Jung committed
186 187 188

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

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

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

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

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

226 227
Section fsa.
Context {Λ Σ A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa}.
228
Implicit Types Φ Ψ : A  iProp Λ Σ.
229

230
Lemma fsa_mono E Φ Ψ : ( a, Φ a  Ψ a)  fsa E Φ  fsa E Ψ.
231
Proof. apply fsa_mask_frame_mono; auto. Qed.
232
Lemma fsa_mask_weaken E1 E2 Φ : E1  E2  fsa E1 Φ  fsa E2 Φ.
233
Proof. intros. apply fsa_mask_frame_mono; auto. Qed.
234
Lemma fsa_frame_l E P Φ : (P  fsa E Φ)  fsa E (λ a, P  Φ a).
235
Proof. rewrite comm fsa_frame_r. apply fsa_mono=>a. by rewrite comm. Qed.
236
Lemma fsa_strip_pvs E P Φ : P  fsa E Φ  (|={E}=> P)  fsa E Φ.
237
Proof.
238 239
  move=>->. rewrite -{2}fsa_trans3.
  apply pvs_mono, fsa_mono=>a; apply pvs_intro.
240
Qed.
241
Lemma fsa_mono_pvs E Φ Ψ : ( a, Φ a  (|={E}=> Ψ a))  fsa E Φ  fsa E Ψ.
242
Proof. intros. rewrite -[fsa E Ψ]fsa_trans3 -pvs_intro. by apply fsa_mono. Qed.
243 244
End fsa.

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