weakestpre.v 9.1 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
3
4
5
6
7
8
9
Require Export iris.pviewshifts.
Require Import iris.wsat.
Local Hint Extern 10 (_  _) => omega.
Local Hint Extern 100 (@eq coPset _ _) => eassumption || solve_elem_of.
Local Hint Extern 100 (_  _) => solve_elem_of.
Local Hint Extern 10 ({_} _) =>
  repeat match goal with H : wsat _ _ _ _ |- _ => apply wsat_valid in H end;
  solve_validN.

10
11
Record wp_go {Σ} (E : coPset) (Q Qfork : iexpr Σ  nat  iRes Σ  Prop)
    (k : nat) (rf : iRes Σ) (e1 : iexpr Σ) (σ1 : istate Σ) := {
12
  wf_safe : reducible e1 σ1;
Robbert Krebbers's avatar
Robbert Krebbers committed
13
14
15
16
17
18
19
20
  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'
}.
CoInductive wp_pre {Σ} (E : coPset)
21
     (Q : ival Σ  iProp Σ) : iexpr Σ  nat  iRes Σ  Prop :=
Robbert Krebbers's avatar
Robbert Krebbers committed
22
23
24
25
26
27
28
29
30
31
32
33
34
  | wp_pre_value n r v : Q v n r  wp_pre E Q (of_val v) n r
  | wp_pre_step n r1 e1 :
     to_val e1 = None 
     ( rf k Ef σ1,
       1 < k < n  E  Ef =  
       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.
Program Definition wp {Σ} (E : coPset) (e : iexpr Σ)
  (Q : ival Σ  iProp Σ) : iProp Σ := {| uPred_holds := wp_pre E Q e |}.
Next Obligation.
  intros Σ E e Q r1 r2 n Hwp Hr.
35
  destruct Hwp as [|n r1 e2 ? Hgo]; constructor; rewrite -?Hr; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
36
37
  intros rf k Ef σ1 ?; rewrite -(dist_le _ _ _ _ Hr); naive_solver.
Qed.
38
39
40
41
42
Next Obligation.
  intros Σ E e Q r; destruct (to_val e) as [v|] eqn:?.
  * by rewrite -(of_to_val e v) //; constructor.
  * constructor; auto with lia.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
43
44
45
Next Obligation.
  intros Σ E e Q r1 r2 n1; revert Q E e r1 r2.
  induction n1 as [n1 IH] using lt_wf_ind; intros Q E e r1 r1' n2.
46
  destruct 1 as [|n1 r1 e1 ? Hgo].
Robbert Krebbers's avatar
Robbert Krebbers committed
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
  * 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];
      rewrite ?(associative _) -?Hr; auto; constructor; [done|].
    intros e2 σ2 ef ?; destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
    exists r2, (r2'  rf'); split_ands; eauto 10 using (IH k), @ra_included_l.
    by rewrite -!(associative _) (associative _ r2).
Qed.
Instance: Params (@wp) 3.

Section wp.
Context {Σ : iParam}.
Implicit Types P : iProp Σ.
Implicit Types Q : ival Σ  iProp Σ.
Implicit Types v : ival Σ.
Implicit Types e : iexpr Σ.
63
Transparent uPred_holds.
Robbert Krebbers's avatar
Robbert Krebbers committed
64
65
66
67
68
69

Lemma wp_weaken E1 E2 e Q1 Q2 r n n' :
  E1  E2  ( v r n', n'  n  {n'} r  Q1 v n' r  Q2 v n' r) 
  n'  n  {n'} r  wp E1 e Q1 n' r  wp E2 e Q2 n' r.
Proof.
  intros HE HQ; revert e r; induction n' as [n' IH] using lt_wf_ind; intros e r.
70
  destruct 3 as [|n' r e1 ? Hgo]; constructor; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
  intros rf k Ef σ1 ???.
  assert (E2  Ef = E1  (E2  E1  Ef)) as HE'.
  { by rewrite (associative_L _) -union_difference_L. }
  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.
Global Instance wp_ne E e n :
  Proper (pointwise_relation _ (dist n) ==> dist n) (wp E e).
Proof. by intros Q Q' HQ; split; apply wp_weaken with n; try apply HQ. Qed.
Global Instance wp_proper E e :
  Proper (pointwise_relation _ () ==> ()) (wp E e).
Proof.
  by intros Q Q' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
88
89
Lemma wp_value_inv E Q v n r : wp E (of_val v) Q n r  Q v n r.
Proof.
90
  inversion 1 as [|??? He]; simplify_equality; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
91
92
93
94
95
96
  by rewrite ?to_of_val in He.
Qed.
Lemma wp_step_inv E Ef Q e k n σ r rf :
  to_val e = None  1 < k < n  E  Ef =  
  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 σ.
97
Proof. intros He; destruct 3; [by rewrite ?to_of_val in He|eauto]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
98

Robbert Krebbers's avatar
Robbert Krebbers committed
99
100
101
102
103
104
105
106
Lemma wp_value E Q v : Q v  wp E (of_val v) Q.
Proof. by constructor. Qed.
Lemma wp_mono E e Q1 Q2 : ( v, Q1 v  Q2 v)  wp E e Q1  wp E e Q2.
Proof. by intros HQ r n ?; apply wp_weaken with n; intros; try apply HQ. Qed.
Lemma wp_pvs E e Q : pvs E E (wp E e Q)  wp E e (λ v, pvs E E (Q v)).
Proof.
  intros r [|n] ?; [done|]; intros Hvs.
  destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|].
Robbert Krebbers's avatar
Robbert Krebbers committed
107
  { by constructor; eapply pvs_mono, Hvs; [intros ???; apply wp_value_inv|]. }
Robbert Krebbers's avatar
Robbert Krebbers committed
108
109
  constructor; [done|intros rf k Ef σ1 ???].
  destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto.
110
  inversion Hwp as [|???? Hgo]; subst; [by rewrite to_of_val in He|].
Robbert Krebbers's avatar
Robbert Krebbers committed
111
112
113
114
115
116
117
118
119
120
121
122
  destruct (Hgo rf k Ef σ1) as [Hsafe Hstep]; auto.
  split; [done|intros e2 σ2 ef ?].
  destruct (Hstep e2 σ2 ef) as (r2&r2'&?&Hwp'&?); auto.
  exists r2, r2'; split_ands; auto.
  eapply wp_mono, Hwp'; auto using pvs_intro.
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.
  intros ? He r n ? Hvs; constructor; eauto using atomic_not_value.
  intros rf k Ef σ1 ???.
  destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto.
123
  inversion Hwp as [|???? Hgo]; subst; [by destruct (atomic_of_val v)|].
Robbert Krebbers's avatar
Robbert Krebbers committed
124
125
126
  destruct (Hgo rf k Ef σ1) as [Hsafe Hstep]; clear Hgo; auto.
  split; [done|intros e2 σ2 ef ?].
  destruct (Hstep e2 σ2 ef) as (r2&r2'&?&Hwp'&?); clear Hsafe Hstep; auto.
127
128
  destruct Hwp' as [k r2 v Hvs'|k r2 e2 Hgo];
    [|destruct (atomic_step e σ1 e2 σ2 ef); naive_solver].
Robbert Krebbers's avatar
Robbert Krebbers committed
129
130
131
132
133
134
135
136
137
138
  destruct (Hvs' (r2'  rf) k Ef σ2) as (r3&[]); rewrite ?(associative _); auto.
  by exists r3, r2'; split_ands; [rewrite -(associative _)|constructor|].
Qed.
Lemma wp_mask_weaken E1 E2 e Q : E1  E2  wp E1 e Q  wp E2 e Q.
Proof. by intros HE r n ?; apply wp_weaken with n. 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.
139
  destruct 1 as [|n r e ? Hgo]; constructor; [exists r, rR; eauto|auto|].
Robbert Krebbers's avatar
Robbert Krebbers committed
140
141
142
143
144
145
146
147
148
149
150
151
152
  intros rf k Ef σ1 ???; destruct (Hgo (rRrf) k Ef σ1) as [Hsafe Hstep]; auto.
  { by rewrite (associative _). }
  split; [done|intros e2 σ2 ef ?].
  destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
  exists (r2  rR), r2'; split_ands; auto.
  * by rewrite -(associative _ r2)
      (commutative _ rR) !(associative _) -(associative _ _ rR).
  * 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.
153
  destruct Hwp as [|[|n] r e ? Hgo]; [by rewrite to_of_val in He|done|].
Robbert Krebbers's avatar
Robbert Krebbers committed
154
155
156
157
158
159
160
161
162
163
164
165
166
167
  constructor; [done|intros rf k Ef σ1 ???].
  destruct (Hgo (rRrf) k Ef σ1) as [Hsafe Hstep];rewrite ?(associative _);auto.
  split; [done|intros e2 σ2 ef ?].
  destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
  exists (r2  rR), r2'; split_ands; auto.
  * by rewrite -(associative _ r2)
      (commutative _ rR) !(associative _) -(associative _ _ rR).
  * apply wp_frame_r; [auto|exists r2, rR; split_ands; auto].
    eapply uPred_weaken with rR n; eauto.
Qed.
Lemma wp_bind `(HK : is_ctx K) E e Q :
  wp E e (λ v, wp E (K (of_val v)) Q)  wp E (K e) Q.
Proof.
  intros r n; revert e r; induction n as [n IH] using lt_wf_ind; intros e r ?.
168
  destruct 1 as [|n r e ? Hgo]; [|constructor]; auto using is_ctx_value.
Robbert Krebbers's avatar
Robbert Krebbers committed
169
170
171
172
173
174
175
176
177
178
179
  intros rf k Ef σ1 ???; destruct (Hgo rf k Ef σ1) as [Hsafe Hstep]; auto.
  split.
  { destruct Hsafe as (e2&σ2&ef&?).
    by exists (K e2), σ2, ef; apply is_ctx_step_preserved. }
  intros e2 σ2 ef ?.
  destruct (is_ctx_step _ HK e σ1 e2 σ2 ef) as (e2'&->&?); auto.
  destruct (Hstep e2' σ2 ef) as (r2&r2'&?&?&?); auto.
  exists r2, r2'; split_ands; try eapply IH; eauto.
Qed.

(* Derived rules *)
180
Opaque uPred_holds.
Robbert Krebbers's avatar
Robbert Krebbers committed
181
182
183
184
Import uPred.
Global Instance wp_mono' E e :
  Proper (pointwise_relation _ () ==> ()) (wp E e).
Proof. by intros Q Q' ?; apply wp_mono. Qed.
185
186
187
188
189
190
191
Lemma wp_value' E Q e v : 
  to_val e = Some v 
  Q v  wp E e Q.
Proof.
  intros Hv. apply of_to_val in Hv.
  rewrite -Hv. by apply wp_value.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
192
193
194
195
196
197
198
199
Lemma wp_frame_l E e Q R : (R  wp E e Q)  wp E e (λ v, R  Q v).
Proof. setoid_rewrite (commutative _ R); apply wp_frame_r. Qed.
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.
  rewrite (commutative _ ( R)%I); setoid_rewrite (commutative _ R).
  apply wp_frame_later_r.
Qed.
200
201
202
203
204
205
Lemma wp_always_l E e Q R `{!AlwaysStable R} :
  (R  wp E e Q)  wp E e (λ v, R  Q v).
Proof. by setoid_rewrite (always_and_sep_l' _ _); rewrite wp_frame_l. Qed.
Lemma wp_always_r E e Q R `{!AlwaysStable R} :
  (wp E e Q  R)  wp E e (λ v, Q v  R).
Proof. by setoid_rewrite (always_and_sep_r' _ _); rewrite wp_frame_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
206
207
208
Lemma wp_impl_l E e Q1 Q2 : ((  v, Q1 v  Q2 v)  wp E e Q1)  wp E e Q2.
Proof.
  rewrite wp_always_l; apply wp_mono=> v.
209
  by rewrite always_elim (forall_elim v) impl_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
210
211
212
213
Qed.
Lemma wp_impl_r E e Q1 Q2 : (wp E e Q1    v, Q1 v  Q2 v)  wp E e Q2.
Proof. by rewrite (commutative _) wp_impl_l. Qed.
End wp.