weakestpre.v 13.6 KB
Newer Older
1
2
From iris.program_logic Require Export pviewshifts.
From iris.program_logic Require Import wsat.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
Local Hint Extern 10 (_  _) => omega.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
5
Local Hint Extern 100 (_  _) => set_solver.
Local Hint Extern 100 (_ _) => set_solver.
6
Local Hint Extern 100 (@subseteq coPset _ _ _) => 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
Record wp_go {Λ Σ} (E : coPset) (Φ Φfork : expr Λ  nat  iRes Λ Σ  Prop)
13
    (k : nat) (σ1 : state Λ) (rf : iRes Λ Σ) (e1 : expr Λ) := {
14
  wf_safe : reducible e1 σ1;
Robbert Krebbers's avatar
Robbert Krebbers committed
15
16
17
18
  wp_step e2 σ2 ef :
    prim_step e1 σ1 e2 σ2 ef 
     r2 r2',
      wsat k E σ2 (r2  r2'  rf) 
19
20
      Φ e2 k r2 
       e', ef = Some e'  Φfork e' k r2'
Robbert Krebbers's avatar
Robbert Krebbers committed
21
}.
22
CoInductive wp_pre {Λ Σ} (E : coPset)
23
     (Φ : val Λ  iProp Λ Σ) : expr Λ  nat  iRes Λ Σ  Prop :=
24
  | wp_pre_value n r v : (|={E}=> Φ v)%I n r  wp_pre E Φ (of_val v) n r
Robbert Krebbers's avatar
Robbert Krebbers committed
25
26
  | wp_pre_step n r1 e1 :
     to_val e1 = None 
27
     ( k Ef σ1 rf,
Robbert Krebbers's avatar
Robbert Krebbers committed
28
       0 < k < n  E  Ef 
Robbert Krebbers's avatar
Robbert Krebbers committed
29
       wsat (S k) (E  Ef) σ1 (r1  rf) 
30
       wp_go (E  Ef) (wp_pre E Φ)
31
                      (wp_pre  (λ _, True%I)) k σ1 rf e1) 
32
     wp_pre E Φ e1 n r1.
Ralf Jung's avatar
Ralf Jung committed
33
Program Definition wp_def {Λ Σ} (E : coPset) (e : expr Λ)
34
  (Φ : val Λ  iProp Λ Σ) : iProp Λ Σ := {| uPred_holds := wp_pre E Φ e |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
35
Next Obligation.
36
37
38
39
  intros Λ Σ E e Φ n r1 r2; revert Φ E e r1 r2.
  induction n as [n IH] using lt_wf_ind; intros Φ E e r1 r1'.
  destruct 1 as [|n r1 e1 ? Hgo].
  - constructor; eauto using uPred_mono.
40
41
  - intros [rf' Hr]; constructor; [done|intros k Ef σ1 rf ???].
    destruct (Hgo k Ef σ1 (rf'  rf)) as [Hsafe Hstep];
42
      rewrite ?assoc -?(dist_le _ _ _ _ Hr); auto; constructor; [done|].
Robbert Krebbers's avatar
Robbert Krebbers committed
43
    intros e2 σ2 ef ?; destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
44
    exists r2, (r2'  rf'); split_and?; eauto 10 using (IH k), cmra_includedN_l.
45
    by rewrite -!assoc (assoc _ r2).
Robbert Krebbers's avatar
Robbert Krebbers committed
46
Qed.
47
48
Next Obligation. destruct 1; constructor; eauto using uPred_closed. Qed.

Ralf Jung's avatar
Ralf Jung committed
49
50
51
52
53
54
(* Perform sealing. *)
Definition wp_aux : { x | x = @wp_def }. by eexists. Qed.
Definition wp := proj1_sig wp_aux.
Definition wp_eq : @wp = @wp_def := proj2_sig wp_aux.

Arguments wp {_ _} _ _ _.
55
Instance: Params (@wp) 4.
Robbert Krebbers's avatar
Robbert Krebbers committed
56

57
Notation "'WP' e @ E {{ Φ } }" := (wp E e Φ)
58
  (at level 20, e, Φ at level 200,
59
60
   format "'WP'  e  @  E  {{  Φ  } }") : uPred_scope.
Notation "'WP' e {{ Φ } }" := (wp  e Φ)
61
  (at level 20, e, Φ at level 200,
62
   format "'WP'  e  {{  Φ  } }") : uPred_scope.
63

64
65
66
67
68
69
70
Notation "'WP' e @ E {{ v , Q } }" := (wp E e (λ v, Q))
  (at level 20, e, Q at level 200,
   format "'WP'  e  @  E  {{  v ,  Q  } }") : uPred_scope.
Notation "'WP' e {{ v , Q } }" := (wp  e (λ v, Q))
  (at level 20, e, Q at level 200,
   format "'WP'  e  {{  v ,  Q  } }") : uPred_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
71
Section wp.
72
Context {Λ : language} {Σ : iFunctor}.
73
Implicit Types P : iProp Λ Σ.
74
Implicit Types Φ : val Λ  iProp Λ Σ.
75
76
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Robbert Krebbers's avatar
Robbert Krebbers committed
77

78
79
Global Instance wp_ne E e n :
  Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ E e).
Robbert Krebbers's avatar
Robbert Krebbers committed
80
Proof.
81
  cut ( Φ Ψ, ( v, Φ v {n} Ψ v) 
Robbert Krebbers's avatar
Robbert Krebbers committed
82
     n' r, n'  n  {n'} r  wp E e Φ n' r  wp E e Ψ n' r).
Ralf Jung's avatar
Ralf Jung committed
83
84
  { rewrite wp_eq. intros help Φ Ψ HΦΨ. by do 2 split; apply help. }
  rewrite wp_eq. intros Φ Ψ HΦΨ n' r; revert e r.
85
86
87
  induction n' as [n' IH] using lt_wf_ind=> e r.
  destruct 3 as [n' r v HpvsQ|n' r e1 ? Hgo].
  { constructor. by eapply pvs_ne, HpvsQ; eauto. }
88
89
  constructor; [done|]=> k Ef σ1 rf ???.
  destruct (Hgo k Ef σ1 rf) as [Hsafe Hstep]; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
90
91
  split; [done|intros e2 σ2 ef ?].
  destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
92
  exists r2, r2'; split_and?; [|eapply IH|]; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
94
Qed.
Global Instance wp_proper E e :
95
  Proper (pointwise_relation _ () ==> ()) (@wp Λ Σ E e).
Robbert Krebbers's avatar
Robbert Krebbers committed
96
Proof.
97
  by intros Φ Φ' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
Robbert Krebbers's avatar
Robbert Krebbers committed
98
Qed.
99

100
Lemma wp_mask_frame_mono E1 E2 e Φ Ψ :
101
  E1  E2  ( v, Φ v  Ψ v)  WP e @ E1 {{ Φ }}  WP e @ E2 {{ Ψ }}.
102
Proof.
Ralf Jung's avatar
Ralf Jung committed
103
  rewrite wp_eq. intros HE HΦ; split=> n r.
104
  revert e r; induction n as [n IH] using lt_wf_ind=> e r.
105
106
  destruct 2 as [n' r v HpvsQ|n' r e1 ? Hgo].
  { constructor; eapply pvs_mask_frame_mono, HpvsQ; eauto. }
107
  constructor; [done|]=> k Ef σ1 rf ???.
108
  assert (E2  Ef = E1  (E2  E1  Ef)) as HE'.
109
  { by rewrite assoc_L -union_difference_L. }
110
  destruct (Hgo k ((E2  E1)  Ef) σ1 rf) as [Hsafe Hstep]; rewrite -?HE'; auto.
111
112
  split; [done|intros e2 σ2 ef ?].
  destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
113
  exists r2, r2'; split_and?; [rewrite HE'|eapply IH|]; eauto.
114
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
115

116
117
118
119
120
121
122
Lemma wp_zero E e Φ r : wp_def E e Φ 0 r.
Proof.
  case EQ: (to_val e).
  - rewrite -(of_to_val _ _ EQ). constructor. rewrite pvs_eq.
    exact: pvs_zero.
  - constructor; first done. intros ?????. exfalso. omega.
Qed.
123
Lemma wp_value_inv E Φ v n r : wp_def E (of_val v) Φ n r  pvs E E (Φ v) n r.
Robbert Krebbers's avatar
Robbert Krebbers committed
124
Proof.
125
  by inversion 1 as [|??? He]; [|rewrite ?to_of_val in He]; simplify_eq.
Robbert Krebbers's avatar
Robbert Krebbers committed
126
Qed.
127
Lemma wp_step_inv E Ef Φ e k n σ r rf :
Robbert Krebbers's avatar
Robbert Krebbers committed
128
  to_val e = None  0 < k < n  E  Ef 
Ralf Jung's avatar
Ralf Jung committed
129
  wp_def E e Φ n r  wsat (S k) (E  Ef) σ (r  rf) 
130
  wp_go (E  Ef) (λ e, wp_def E e Φ) (λ e, wp_def  e (λ _, True%I)) k σ rf e.
Ralf Jung's avatar
Ralf Jung committed
131
132
133
Proof.
  intros He; destruct 3; [by rewrite ?to_of_val in He|eauto].
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
134

135
Lemma wp_value' E Φ v : Φ v  WP of_val v @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
136
Proof. rewrite wp_eq. split=> n r; constructor; by apply pvs_intro. Qed.
137
Lemma pvs_wp E e Φ : (|={E}=> WP e @ E {{ Φ }})  WP e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
138
Proof.
Ralf Jung's avatar
Ralf Jung committed
139
  rewrite wp_eq. split=> n r ? Hvs.
Robbert Krebbers's avatar
Robbert Krebbers committed
140
  destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|].
141
  { constructor; eapply pvs_trans', pvs_mono, Hvs; eauto.
142
    split=> ???; apply wp_value_inv. }
143
144
  constructor; [done|]=> k Ef σ1 rf ???.
  rewrite pvs_eq in Hvs. destruct (Hvs (S k) Ef σ1 rf) as (r'&Hwp&?); auto.
145
146
  eapply wp_step_inv with (S k) r'; eauto.
Qed.
147
Lemma wp_pvs E e Φ : WP e @ E {{ v, |={E}=> Φ v }}  WP e @ E {{ Φ }}.
148
Proof.
Ralf Jung's avatar
Ralf Jung committed
149
150
  rewrite wp_eq. split=> n r; revert e r;
    induction n as [n IH] using lt_wf_ind=> e r Hr HΦ.
151
  destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|].
152
  { constructor; apply pvs_trans', (wp_value_inv _ (pvs E E  Φ)); auto. }
153
  constructor; [done|]=> k Ef σ1 rf ???.
154
  destruct (wp_step_inv E Ef (pvs E E  Φ) e k n σ1 r rf) as [? Hstep]; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
156
  split; [done|intros e2 σ2 ef ?].
  destruct (Hstep e2 σ2 ef) as (r2&r2'&?&Hwp'&?); auto.
157
  exists r2, r2'; split_and?; [|apply (IH k)|]; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
158
Qed.
159
Lemma wp_atomic E1 E2 e Φ :
160
  E2  E1  atomic e 
161
  (|={E1,E2}=> WP e @ E2 {{ v, |={E2,E1}=> Φ v }})  WP e @ E1 {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
162
Proof.
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
  rewrite wp_eq pvs_eq. intros ? He; split=> n r ? Hvs.
  destruct (to_val e) as [v|] eqn:Hvale.
  - apply of_to_val in Hvale. subst e. eapply wp_pre_value. rewrite pvs_eq.
    intros k Ef σ rf ???. destruct (Hvs k Ef σ rf) as (r'&Hwp&?); auto.
    apply wp_value_inv in Hwp. rewrite pvs_eq in Hwp.
    destruct (Hwp k Ef σ rf) as (r2'&HΦ&?); auto.
  - apply wp_pre_step. done. intros k Ef σ1 rf ???.
    destruct (Hvs (S k) Ef σ1 rf) as (r'&Hwp&?); auto.
    destruct (wp_step_inv E2 Ef (pvs_def E2 E1  Φ) e k (S k) σ1 r' rf)
      as [Hsafe Hstep]; auto; [].
    split; [done|]=> e2 σ2 ef ?.
    destruct (Hstep e2 σ2 ef) as (r2&r2'&?&Hwp'&?); clear Hsafe Hstep; auto.
    destruct Hwp' as [k r2 v Hvs'|k r2 e2 Hgo];
      [|destruct (He σ1 e2 σ2 ef); naive_solver].
    rewrite -pvs_eq in Hvs'. apply pvs_trans in Hvs';auto. rewrite pvs_eq in Hvs'.
    destruct (Hvs' k Ef σ2 (r2'  rf)) as (r3&[]); rewrite ?assoc; auto.
    exists r3, r2'; split_and?; last done.
    + by rewrite -assoc.
    + constructor; apply pvs_intro; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
182
Qed.
183
Lemma wp_frame_r E e Φ R : WP e @ E {{ Φ }}  R  WP e @ E {{ v, Φ v  R }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
184
Proof.
Ralf Jung's avatar
Ralf Jung committed
185
186
  rewrite wp_eq. uPred.unseal; split; intros n r' Hvalid (r&rR&Hr&Hwp&?).
  revert Hvalid. rewrite Hr; clear Hr; revert e r Hwp.
Robbert Krebbers's avatar
Robbert Krebbers committed
187
  induction n as [n IH] using lt_wf_ind; intros e r1.
188
  destruct 1 as [|n r e ? Hgo]=>?.
189
190
  { constructor. rewrite -uPred_sep_eq; apply pvs_frame_r; auto.
    uPred.unseal; exists r, rR; eauto. }
191
192
  constructor; [done|]=> k Ef σ1 rf ???.
  destruct (Hgo k Ef σ1 (rRrf)) as [Hsafe Hstep]; auto.
193
  { by rewrite assoc. }
Robbert Krebbers's avatar
Robbert Krebbers committed
194
195
  split; [done|intros e2 σ2 ef ?].
  destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
196
  exists (r2  rR), r2'; split_and?; auto.
197
  - by rewrite -(assoc _ r2) (comm _ rR) !assoc -(assoc _ _ rR).
198
  - apply IH; eauto using uPred_closed.
Robbert Krebbers's avatar
Robbert Krebbers committed
199
Qed.
Ralf Jung's avatar
Ralf Jung committed
200
201
Lemma wp_frame_step_r E E1 E2 e Φ R :
  to_val e = None  E  E1  E2  E1 
202
  WP e @ E {{ Φ }}  (|={E1,E2}=>  |={E2,E1}=> R)
Robbert Krebbers's avatar
Robbert Krebbers committed
203
204
   WP e @ E  E1 {{ v, Φ v  R }}.
Proof.
Ralf Jung's avatar
Ralf Jung committed
205
206
  rewrite wp_eq pvs_eq=> He ??.
  uPred.unseal; split; intros n r' Hvalid (r&rR&Hr&Hwp&HR); cofe_subst.
207
  constructor; [done|]=> k Ef σ1 rf ?? Hws1.
208
  destruct Hwp as [|n r e ? Hgo]; [by rewrite to_of_val in He|].
Ralf Jung's avatar
Ralf Jung committed
209
  (* "execute" HR *)
210
  destruct (HR (S k) (E  Ef) σ1 (r  rf)) as (s&Hvs&Hws2); auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
211
212
213
  { eapply wsat_proper, Hws1; first by set_solver+.
    by rewrite assoc [rR  _]comm. }
  clear Hws1 HR.
Ralf Jung's avatar
Ralf Jung committed
214
  (* Take a step *)
215
  destruct (Hgo k (E2  Ef) σ1 (s  rf)) as [Hsafe Hstep]; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
216
217
218
  { eapply wsat_proper, Hws2; first by set_solver+.
    by rewrite !assoc [s  _]comm. }
  clear Hgo.
Robbert Krebbers's avatar
Robbert Krebbers committed
219
  split; [done|intros e2 σ2 ef ?].
Ralf Jung's avatar
Ralf Jung committed
220
221
  destruct (Hstep e2 σ2 ef) as (r2&r2'&Hws3&?&?); auto. clear Hws2.
  (* Execute 2nd part of the view shift *)
222
  destruct (Hvs k (E  Ef) σ2 (r2  r2'  rf)) as (t&HR&Hws4); auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
223
224
225
  { eapply wsat_proper, Hws3; first by set_solver+.
    by rewrite !assoc [_  s]comm !assoc. }
  clear Hvs Hws3.
Ralf Jung's avatar
Ralf Jung committed
226
  (* Execute the rest of e *)
227
  exists (r2  t), r2'; split_and?; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
228
229
230
  - eapply wsat_proper, Hws4; first by set_solver+.
    by rewrite !assoc [_  t]comm.
  - rewrite -uPred_sep_eq. move: wp_frame_r. rewrite wp_eq=>Hframe.
Ralf Jung's avatar
Ralf Jung committed
231
    apply Hframe; first by auto. uPred.unseal; exists r2, t; split_and?; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
232
    move: wp_mask_frame_mono. rewrite wp_eq=>Hmask.
Ralf Jung's avatar
Ralf Jung committed
233
    eapply (Hmask E); by auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
234
Qed.
235
Lemma wp_bind `{LanguageCtx Λ K} E e Φ :
236
  WP e @ E {{ v, WP K (of_val v) @ E {{ Φ }} }}  WP K e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
237
Proof.
Ralf Jung's avatar
Ralf Jung committed
238
239
240
241
  rewrite wp_eq. split=> n r; revert e r;
    induction n as [n IH] using lt_wf_ind=> e r ?.
  destruct 1 as [|n r e ? Hgo].
  { rewrite -wp_eq. apply pvs_wp; rewrite ?wp_eq; done. }
242
243
  constructor; auto using fill_not_val=> k Ef σ1 rf ???.
  destruct (Hgo k Ef σ1 rf) as [Hsafe Hstep]; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
244
245
  split.
  { destruct Hsafe as (e2&σ2&ef&?).
246
    by exists (K e2), σ2, ef; apply fill_step. }
Robbert Krebbers's avatar
Robbert Krebbers committed
247
  intros e2 σ2 ef ?.
248
  destruct (fill_step_inv e σ1 e2 σ2 ef) as (e2'&->&?); auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
249
  destruct (Hstep e2' σ2 ef) as (r2&r2'&?&?&?); auto.
250
  exists r2, r2'; split_and?; try eapply IH; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
251
252
Qed.

253
(** * Derived rules *)
Robbert Krebbers's avatar
Robbert Krebbers committed
254
Import uPred.
255
Lemma wp_mono E e Φ Ψ : ( v, Φ v  Ψ v)  WP e @ E {{ Φ }}  WP e @ E {{ Ψ }}.
256
Proof. by apply wp_mask_frame_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
257
Global Instance wp_mono' E e :
258
  Proper (pointwise_relation _ () ==> ()) (@wp Λ Σ E e).
259
Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
260
Lemma wp_strip_pvs E e P Φ :
261
  (P  WP e @ E {{ Φ }})  (|={E}=> P)  WP e @ E {{ Φ }}.
262
Proof. move=>->. by rewrite pvs_wp. Qed.
263
Lemma wp_value E Φ e v : to_val e = Some v  Φ v  WP e @ E {{ Φ }}.
264
Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed.
265
266
Lemma wp_value_pvs' E Φ v : (|={E}=> Φ v)  WP of_val v @ E {{ Φ }}.
Proof. intros. by rewrite -wp_pvs -wp_value'. Qed.
267
Lemma wp_value_pvs E Φ e v :
268
  to_val e = Some v  (|={E}=> Φ v)  WP e @ E {{ Φ }}.
269
Proof. intros. rewrite -wp_pvs -wp_value //. Qed.
270
Lemma wp_frame_l E e Φ R : R  WP e @ E {{ Φ }}  WP e @ E {{ v, R  Φ v }}.
271
Proof. setoid_rewrite (comm _ R); apply wp_frame_r. Qed.
Ralf Jung's avatar
Ralf Jung committed
272
Lemma wp_frame_step_r' E e Φ R :
273
  to_val e = None  WP e @ E {{ Φ }}   R  WP e @ E {{ v, Φ v  R }}.
Ralf Jung's avatar
Ralf Jung committed
274
275
276
277
278
279
280
Proof.
  intros. rewrite {2}(_ : E = E  ); last by set_solver.
  rewrite -(wp_frame_step_r E  ); [|auto|set_solver..].
  apply sep_mono_r. rewrite -!pvs_intro. done.
Qed.
Lemma wp_frame_step_l E E1 E2 e Φ R :
  to_val e = None  E  E1  E2  E1 
281
  (|={E1,E2}=>  |={E2,E1}=> R)  WP e @ E {{ Φ }}
282
   WP e @ (E  E1) {{ v, R  Φ v }}.
Ralf Jung's avatar
Ralf Jung committed
283
284
285
286
287
Proof.
  rewrite [((|={E1,E2}=> _)  _)%I]comm; setoid_rewrite (comm _ R).
  apply wp_frame_step_r.
Qed.
Lemma wp_frame_step_l' E e Φ R :
288
  to_val e = None   R  WP e @ E {{ Φ }}  WP e @ E {{ v, R  Φ v }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
289
Proof.
290
  rewrite (comm _ ( R)%I); setoid_rewrite (comm _ R).
Ralf Jung's avatar
Ralf Jung committed
291
  apply wp_frame_step_r'.
Robbert Krebbers's avatar
Robbert Krebbers committed
292
Qed.
293
Lemma wp_always_l E e Φ R `{!PersistentP R} :
294
  R  WP e @ E {{ Φ }}  WP e @ E {{ v, R  Φ v }}.
295
Proof. by setoid_rewrite (always_and_sep_l _ _); rewrite wp_frame_l. Qed.
296
Lemma wp_always_r E e Φ R `{!PersistentP R} :
297
  WP e @ E {{ Φ }}  R  WP e @ E {{ v, Φ v  R }}.
298
Proof. by setoid_rewrite (always_and_sep_r _ _); rewrite wp_frame_r. Qed.
299
Lemma wp_wand_l E e Φ Ψ :
300
  ( v, Φ v - Ψ v)  WP e @ E {{ Φ }}  WP e @ E {{ Ψ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
301
Proof.
302
  rewrite wp_frame_l. apply wp_mono=> v. by rewrite (forall_elim v) wand_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
303
Qed.
304
Lemma wp_wand_r E e Φ Ψ :
305
  WP e @ E {{ Φ }}  ( v, Φ v - Ψ v)  WP e @ E {{ Ψ }}.
306
307
Proof. by rewrite comm wp_wand_l. Qed.

308
Lemma wp_mask_weaken E1 E2 e Φ :
309
  E1  E2  WP e @ E1 {{ Φ }}  WP e @ E2 {{ Φ }}.
310
311
312
Proof. auto using wp_mask_frame_mono. Qed.

(** * Weakest-pre is a FSA. *)
313
Definition wp_fsa (e : expr Λ) : FSA Λ Σ (val Λ) := λ E, wp E e.
314
Global Arguments wp_fsa _ _ / _.
315
Global Instance wp_fsa_prf : FrameShiftAssertion (atomic e) (wp_fsa e).
316
Proof.
317
  rewrite /wp_fsa; split; auto using wp_mask_frame_mono, wp_atomic, wp_frame_r.
318
  intros E Φ. by rewrite -(pvs_wp E e Φ) -(wp_pvs E e Φ).
319
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
320
End wp.