weakestpre.v 10.2 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
4
5
Local Hint Extern 10 (_  _) => omega.
Local Hint Extern 100 (@eq coPset _ _) => eassumption || solve_elem_of.
Local Hint Extern 100 (_  _) => solve_elem_of.
6
Local Hint Extern 100 (@subseteq coPset _ _ _) => solve_elem_of.
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
13
Record wp_go {Λ Σ} (E : coPset) (Q Qfork : expr Λ  nat  iRes Λ Σ  Prop)
    (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
19
20
21
  wp_step e2 σ2 ef :
    prim_step e1 σ1 e2 σ2 ef 
     r2 r2',
      wsat k E σ2 (r2  r2'  rf) 
      Q e2 k r2 
       e', ef = Some e'  Qfork e' k r2'
}.
22
23
CoInductive wp_pre {Λ Σ} (E : coPset)
     (Q : val Λ  iProp Λ Σ) : expr Λ  nat  iRes Λ Σ  Prop :=
24
  | wp_pre_value n r v : pvs E E (Q v) n r  wp_pre E Q (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
30
31
32
       wsat (S k) (E  Ef) σ1 (r1  rf) 
       wp_go (E  Ef) (wp_pre E Q)
                      (wp_pre coPset_all (λ _, True%I)) k rf e1 σ1) 
     wp_pre E Q e1 n r1.
33
34
Program Definition wp {Λ Σ} (E : coPset) (e : expr Λ)
  (Q : val Λ  iProp Λ Σ) : iProp Λ Σ := {| uPred_holds := wp_pre E Q e |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
35
Next Obligation.
36
  intros Λ Σ E e Q r1 r2 n 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.
41
  intros Λ Σ E e Q r1 r2 n1; revert Q E e r1 r2.
Robbert Krebbers's avatar
Robbert Krebbers committed
42
  induction n1 as [n1 IH] using lt_wf_ind; intros Q E e r1 r1' n2.
43
  destruct 1 as [|n1 r1 e1 ? Hgo].
Robbert Krebbers's avatar
Robbert Krebbers committed
44
45
46
  * constructor; eauto using uPred_weaken.
  * intros [rf' Hr] ??; constructor; [done|intros rf k Ef σ1 ???].
    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_ands; 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

Section wp.
55
56
57
58
59
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P : iProp Λ Σ.
Implicit Types Q : val Λ  iProp Λ Σ.
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
60
Transparent uPred_holds.
Robbert Krebbers's avatar
Robbert Krebbers committed
61

62
63
Global Instance wp_ne E e n :
  Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ E e).
Robbert Krebbers's avatar
Robbert Krebbers committed
64
Proof.
65
  cut ( Q1 Q2, ( v, Q1 v {n} Q2 v) 
66
67
68
69
70
71
72
73
     r n', n'  n  {n'} r  wp E e Q1 n' r  wp E e Q2 n' r).
  { by intros help Q Q' HQ; split; apply help. }
  intros Q1 Q2 HQ r n'; revert e r.
  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
74
75
  split; [done|intros e2 σ2 ef ?].
  destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
76
  exists r2, r2'; split_ands; [|eapply IH|]; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
77
78
Qed.
Global Instance wp_proper E e :
79
  Proper (pointwise_relation _ () ==> ()) (@wp Λ Σ E e).
Robbert Krebbers's avatar
Robbert Krebbers committed
80
81
82
Proof.
  by intros Q Q' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
Qed.
83
84
85
86
87
88
89
90
Lemma wp_mask_frame_mono E1 E2 e Q1 Q2 :
  E1  E2  ( v, Q1 v  Q2 v)  wp E1 e Q1  wp E2 e Q2.
Proof.
  intros HE HQ r n; revert e r; induction n as [n IH] using lt_wf_ind=> e r.
  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'.
91
  { by rewrite assoc_L -union_difference_L. }
92
93
94
95
96
  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.
  exists r2, r2'; split_ands; [rewrite HE'|eapply IH|]; eauto.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
97

98
Lemma wp_value_inv E Q v n r : wp E (of_val v) Q n r  pvs E E (Q v) n r.
Robbert Krebbers's avatar
Robbert Krebbers committed
99
Proof.
100
  by inversion 1 as [|??? He]; [|rewrite ?to_of_val in He]; simplify_equality.
Robbert Krebbers's avatar
Robbert Krebbers committed
101
102
Qed.
Lemma wp_step_inv E Ef Q e k n σ r rf :
103
  to_val e = None  0 < k < n  E  Ef =  
Robbert Krebbers's avatar
Robbert Krebbers committed
104
105
  wp E e Q n r  wsat (S k) (E  Ef) σ (r  rf) 
  wp_go (E  Ef) (λ e, wp E e Q) (λ e, wp coPset_all e (λ _, True%I)) k rf e σ.
106
Proof. intros He; destruct 3; [by rewrite ?to_of_val in He|eauto]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
107

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

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

(** * Weakest-pre is a FSA. *)
Global Instance wp_fsa e : atomic e  FrameShiftAssertion (λ E Q, wp E e Q).
Proof.
  split; intros.
  - apply wp_mask_frame_mono; auto.
  - apply wp_atomic; auto.
  - apply wp_frame_r; auto.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
242
End wp.