weakestpre.v 11 KB
Newer Older
1
2
From program_logic Require Export pviewshifts.
From program_logic Require Import wsat.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
Local Hint Extern 10 (_  _) => omega.
4
5
6
Local Hint Extern 100 (@eq coPset _ _) => eassumption || set_solver.
Local Hint Extern 100 (_  _) => set_solver.
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) (rf : iRes Λ Σ) (e1 : expr Λ) (σ1 : state Λ) := {
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
27
  | wp_pre_step n r1 e1 :
     to_val e1 = None 
     ( rf k Ef σ1,
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 rf e1 σ1) 
32
     wp_pre E Φ e1 n r1.
33
Program Definition wp {Λ Σ} (E : coPset) (e : expr Λ)
34
  (Φ : val Λ  iProp Λ Σ) : iProp Λ Σ := {| uPred_holds := wp_pre E Φ e |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
35
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
36
  intros Λ Σ E e Φ n r1 r2 Hwp Hr.
37
  destruct Hwp as [|n r1 e2 ? Hgo]; constructor; rewrite -?Hr; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
38
39
40
  intros rf k Ef σ1 ?; rewrite -(dist_le _ _ _ _ Hr); naive_solver.
Qed.
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
41
42
  intros Λ Σ E e Φ n1 n2 r1 r2; revert Φ E e n2 r1 r2.
  induction n1 as [n1 IH] using lt_wf_ind; intros Φ E e n2 r1 r1'.
43
  destruct 1 as [|n1 r1 e1 ? Hgo].
44
45
  - constructor; eauto using uPred_weaken.
  - intros [rf' Hr] ??; constructor; [done|intros rf k Ef σ1 ???].
Robbert Krebbers's avatar
Robbert Krebbers committed
46
    destruct (Hgo (rf'  rf) k Ef σ1) as [Hsafe Hstep];
47
      rewrite ?assoc -?Hr; auto; constructor; [done|].
Robbert Krebbers's avatar
Robbert Krebbers committed
48
    intros e2 σ2 ef ?; destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
49
    exists r2, (r2'  rf'); split_and?; eauto 10 using (IH k), cmra_included_l.
50
    by rewrite -!assoc (assoc _ r2).
Robbert Krebbers's avatar
Robbert Krebbers committed
51
Qed.
52
Instance: Params (@wp) 4.
Robbert Krebbers's avatar
Robbert Krebbers committed
53

54
55
56
57
58
59
60
Notation "|| e @ E {{ Φ } }" := (wp E e Φ)
  (at level 20, e, Φ at level 200,
   format "||  e  @  E  {{  Φ  } }") : uPred_scope.
Notation "|| e {{ Φ } }" := (wp  e Φ)
  (at level 20, e, Φ at level 200,
   format "||  e   {{  Φ  } }") : uPred_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
61
Section wp.
62
63
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P : iProp Λ Σ.
64
Implicit Types Φ : val Λ  iProp Λ Σ.
65
66
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
67
Transparent uPred_holds.
Robbert Krebbers's avatar
Robbert Krebbers committed
68

69
70
Global Instance wp_ne E e n :
  Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ E e).
Robbert Krebbers's avatar
Robbert Krebbers committed
71
Proof.
72
  cut ( Φ Ψ, ( v, Φ v {n} Ψ v) 
Robbert Krebbers's avatar
Robbert Krebbers committed
73
     n' r, n'  n  {n'} r  wp E e Φ n' r  wp E e Ψ n' r).
74
  { by intros help Φ Ψ HΦΨ; split; apply help. }
Robbert Krebbers's avatar
Robbert Krebbers committed
75
  intros Φ Ψ HΦΨ n' r; revert e r.
76
77
78
79
80
  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. }
  constructor; [done|]=> rf k Ef σ1 ???.
  destruct (Hgo rf k Ef σ1) as [Hsafe Hstep]; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
81
82
  split; [done|intros e2 σ2 ef ?].
  destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
83
  exists r2, r2'; split_and?; [|eapply IH|]; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
84
85
Qed.
Global Instance wp_proper E e :
86
  Proper (pointwise_relation _ () ==> ()) (@wp Λ Σ E e).
Robbert Krebbers's avatar
Robbert Krebbers committed
87
Proof.
88
  by intros Φ Φ' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
Robbert Krebbers's avatar
Robbert Krebbers committed
89
Qed.
90
Lemma wp_mask_frame_mono E1 E2 e Φ Ψ :
91
  E1  E2  ( v, Φ v  Ψ v)  || e @ E1 {{ Φ }}  || e @ E2 {{ Ψ }}.
92
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
  intros HE HΦ n r; revert e r; induction n as [n IH] using lt_wf_ind=> e r.
94
95
96
97
  destruct 2 as [n' r v HpvsQ|n' r e1 ? Hgo].
  { constructor; eapply pvs_mask_frame_mono, HpvsQ; eauto. }
  constructor; [done|]=> rf k Ef σ1 ???.
  assert (E2  Ef = E1  (E2  E1  Ef)) as HE'.
98
  { by rewrite assoc_L -union_difference_L. }
99
100
101
  destruct (Hgo rf k ((E2  E1)  Ef) σ1) as [Hsafe Hstep]; rewrite -?HE'; auto.
  split; [done|intros e2 σ2 ef ?].
  destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
102
  exists r2, r2'; split_and?; [rewrite HE'|eapply IH|]; eauto.
103
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
104

105
106
Lemma wp_value_inv E Φ v n r :
  || of_val v @ E {{ Φ }}%I n r  (|={E}=> Φ v)%I n r.
Robbert Krebbers's avatar
Robbert Krebbers committed
107
Proof.
108
  by inversion 1 as [|??? He]; [|rewrite ?to_of_val in He]; simplify_eq.
Robbert Krebbers's avatar
Robbert Krebbers committed
109
Qed.
110
Lemma wp_step_inv E Ef Φ e k n σ r rf :
111
  to_val e = None  0 < k < n  E  Ef =  
112
  || e @ E {{ Φ }}%I n r  wsat (S k) (E  Ef) σ (r  rf) 
113
  wp_go (E  Ef) (λ e, wp E e Φ) (λ e, wp  e (λ _, True%I)) k rf e σ.
114
Proof. intros He; destruct 3; [by rewrite ?to_of_val in He|eauto]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
115

116
Lemma wp_value' E Φ v : Φ v  || of_val v @ E {{ Φ }}.
117
Proof. by constructor; apply pvs_intro. Qed.
118
Lemma pvs_wp E e Φ : (|={E}=> || e @ E {{ Φ }})  || e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
119
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
120
  intros n r ? Hvs.
Robbert Krebbers's avatar
Robbert Krebbers committed
121
  destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|].
122
123
124
  { constructor; eapply pvs_trans', pvs_mono, Hvs; eauto.
    intros ???; apply wp_value_inv. }
  constructor; [done|]=> rf k Ef σ1 ???.
Robbert Krebbers's avatar
Robbert Krebbers committed
125
  destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto.
126
127
  eapply wp_step_inv with (S k) r'; eauto.
Qed.
128
Lemma wp_pvs E e Φ : || e @  E {{ λ v, |={E}=> Φ v }}  || e @ E {{ Φ }}.
129
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
130
  intros n r; revert e r; induction n as [n IH] using lt_wf_ind=> e r Hr HΦ.
131
  destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|].
132
  { constructor; apply pvs_trans', (wp_value_inv _ (pvs E E  Φ)); auto. }
133
  constructor; [done|]=> rf k Ef σ1 ???.
134
  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
135
136
  split; [done|intros e2 σ2 ef ?].
  destruct (Hstep e2 σ2 ef) as (r2&r2'&?&Hwp'&?); auto.
137
  exists r2, r2'; split_and?; [|apply (IH k)|]; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
138
Qed.
139
Lemma wp_atomic E1 E2 e Φ :
140
141
  E2  E1  atomic e 
  (|={E1,E2}=> || e @ E2 {{ λ v, |={E2,E1}=> Φ v }})  || e @ E1 {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
142
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
143
  intros ? He n r ? Hvs; constructor; eauto using atomic_not_val.
Robbert Krebbers's avatar
Robbert Krebbers committed
144
145
  intros rf k Ef σ1 ???.
  destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto.
146
  destruct (wp_step_inv E2 Ef (pvs E2 E1  Φ) e k (S k) σ1 r' rf)
147
148
    as [Hsafe Hstep]; auto using atomic_not_val.
  split; [done|]=> e2 σ2 ef ?.
Robbert Krebbers's avatar
Robbert Krebbers committed
149
  destruct (Hstep e2 σ2 ef) as (r2&r2'&?&Hwp'&?); clear Hsafe Hstep; auto.
150
151
  destruct Hwp' as [k r2 v Hvs'|k r2 e2 Hgo];
    [|destruct (atomic_step e σ1 e2 σ2 ef); naive_solver].
152
  apply pvs_trans in Hvs'; auto.
153
  destruct (Hvs' (r2'  rf) k Ef σ2) as (r3&[]); rewrite ?assoc; auto.
154
  exists r3, r2'; split_and?; last done.
155
156
  - by rewrite -assoc.
  - constructor; apply pvs_intro; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
157
Qed.
158
Lemma wp_frame_r E e Φ R : (|| e @ E {{ Φ }}  R)  || e @ E {{ λ v, Φ v  R }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
159
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
160
  intros n r' Hvalid (r&rR&Hr&Hwp&?); revert Hvalid.
Robbert Krebbers's avatar
Robbert Krebbers committed
161
162
  rewrite Hr; clear Hr; revert e r Hwp.
  induction n as [n IH] using lt_wf_ind; intros e r1.
163
164
165
166
  destruct 1 as [|n r e ? Hgo]=>?.
  { constructor; apply pvs_frame_r; auto. exists r, rR; eauto. }
  constructor; [done|]=> rf k Ef σ1 ???.
  destruct (Hgo (rRrf) k Ef σ1) as [Hsafe Hstep]; auto.
167
  { by rewrite assoc. }
Robbert Krebbers's avatar
Robbert Krebbers committed
168
169
  split; [done|intros e2 σ2 ef ?].
  destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
170
  exists (r2  rR), r2'; split_and?; auto.
171
  - by rewrite -(assoc _ r2)
172
      (comm _ rR) !assoc -(assoc _ _ rR).
173
  - apply IH; eauto using uPred_weaken.
Robbert Krebbers's avatar
Robbert Krebbers committed
174
Qed.
175
Lemma wp_frame_later_r E e Φ R :
176
  to_val e = None  (|| e @ E {{ Φ }}   R)  || e @ E {{ λ v, Φ v  R }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
177
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
178
  intros He n r' Hvalid (r&rR&Hr&Hwp&?); revert Hvalid; rewrite Hr; clear Hr.
179
180
  destruct Hwp as [|n r e ? Hgo]; [by rewrite to_of_val in He|].
  constructor; [done|]=>rf k Ef σ1 ???; destruct n as [|n]; first omega.
181
  destruct (Hgo (rRrf) k Ef σ1) as [Hsafe Hstep];rewrite ?assoc;auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
182
183
  split; [done|intros e2 σ2 ef ?].
  destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
184
  exists (r2  rR), r2'; split_and?; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
185
  - by rewrite -(assoc _ r2) (comm _ rR) !assoc -(assoc _ _ rR).
186
  - apply wp_frame_r; [auto|exists r2, rR; split_and?; auto].
Robbert Krebbers's avatar
Robbert Krebbers committed
187
    eapply uPred_weaken with n rR; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
188
Qed.
189
Lemma wp_bind `{LanguageCtx Λ K} E e Φ :
190
  || e @ E {{ λ v, || K (of_val v) @ E {{ Φ }} }}  || K e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
191
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
192
  intros n r; revert e r; induction n as [n IH] using lt_wf_ind=> e r ?.
193
194
195
  destruct 1 as [|n r e ? Hgo]; [by apply pvs_wp|].
  constructor; auto using fill_not_val=> rf k Ef σ1 ???.
  destruct (Hgo rf k Ef σ1) as [Hsafe Hstep]; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
196
197
  split.
  { destruct Hsafe as (e2&σ2&ef&?).
198
    by exists (K e2), σ2, ef; apply fill_step. }
Robbert Krebbers's avatar
Robbert Krebbers committed
199
  intros e2 σ2 ef ?.
200
  destruct (fill_step_inv e σ1 e2 σ2 ef) as (e2'&->&?); auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
201
  destruct (Hstep e2' σ2 ef) as (r2&r2'&?&?&?); auto.
202
  exists r2, r2'; split_and?; try eapply IH; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
203
204
Qed.

205
(** * Derived rules *)
206
Opaque uPred_holds.
Robbert Krebbers's avatar
Robbert Krebbers committed
207
Import uPred.
208
Lemma wp_mono E e Φ Ψ : ( v, Φ v  Ψ v)  || e @ E {{ Φ }}  || e @ E {{ Ψ }}.
209
Proof. by apply wp_mask_frame_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
210
Global Instance wp_mono' E e :
211
  Proper (pointwise_relation _ () ==> ()) (@wp Λ Σ E e).
212
Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
213
214
Lemma wp_strip_pvs E e P Φ :
  P  || e @ E {{ Φ }}  (|={E}=> P)  || e @ E {{ Φ }}.
215
Proof. move=>->. by rewrite pvs_wp. Qed.
216
Lemma wp_value E Φ e v : to_val e = Some v  Φ v  || e @ E {{ Φ }}.
217
Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed.
218
219
Lemma wp_value_pvs E Φ e v :
  to_val e = Some v  (|={E}=> Φ v)  || e @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
220
Proof. intros. rewrite -wp_pvs. rewrite -wp_value //. Qed.
221
Lemma wp_frame_l E e Φ R : (R  || e @ E {{ Φ }})  || e @ E {{ λ v, R  Φ v }}.
222
Proof. setoid_rewrite (comm _ R); apply wp_frame_r. Qed.
223
Lemma wp_frame_later_l E e Φ R :
224
  to_val e = None  ( R  || e @ E {{ Φ }})  || e @ E {{ λ v, R  Φ v }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
225
Proof.
226
  rewrite (comm _ ( R)%I); setoid_rewrite (comm _ R).
Robbert Krebbers's avatar
Robbert Krebbers committed
227
228
  apply wp_frame_later_r.
Qed.
229
Lemma wp_always_l E e Φ R `{!AlwaysStable R} :
230
  (R  || e @ E {{ Φ }})  || e @ E {{ λ v, R  Φ v }}.
231
Proof. by setoid_rewrite (always_and_sep_l _ _); rewrite wp_frame_l. Qed.
232
Lemma wp_always_r E e Φ R `{!AlwaysStable R} :
233
  (|| e @ E {{ Φ }}  R)  || e @ E {{ λ v, Φ v  R }}.
234
Proof. by setoid_rewrite (always_and_sep_r _ _); rewrite wp_frame_r. Qed.
235
236
Lemma wp_impl_l E e Φ Ψ :
  ((  v, Φ v  Ψ v)  || e @ E {{ Φ }})  || e @ E {{ Ψ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
237
Proof.
238
  rewrite wp_always_l; apply wp_mono=> // v.
239
  by rewrite always_elim (forall_elim v) impl_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
240
Qed.
241
242
Lemma wp_impl_r E e Φ Ψ :
  (|| e @ E {{ Φ }}   ( v, Φ v  Ψ v))  || e @ E {{ Ψ }}.
243
Proof. by rewrite comm wp_impl_l. Qed.
244
245
Lemma wp_mask_weaken E1 E2 e Φ :
  E1  E2  || e @ E1 {{ Φ }}  || e @ E2 {{ Φ }}.
246
247
248
Proof. auto using wp_mask_frame_mono. Qed.

(** * Weakest-pre is a FSA. *)
249
Definition wp_fsa (e : expr Λ) : FSA Λ Σ (val Λ) := λ E, wp E e.
250
Global Arguments wp_fsa _ _ / _.
251
Global Instance wp_fsa_prf : FrameShiftAssertion (atomic e) (wp_fsa e).
252
Proof.
253
  rewrite /wp_fsa; split; auto using wp_mask_frame_mono, wp_atomic, wp_frame_r.
254
  intros E Φ. by rewrite -(pvs_wp E e Φ) -(wp_pvs E e Φ).
255
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
256
End wp.