weakestpre.v 10.1 KB
Newer Older
1
From iris.program_logic Require Export pviewshifts.
2
From iris.program_logic Require Import wsat.
3
From iris.algebra Require Import upred_big_op.
4
From iris.prelude Require Export coPset.
5
From iris.proofmode Require Import tactics classes.
6
7
8
9
10
11
12
13
14
15
Import uPred.

Definition wp_pre `{irisG Λ Σ}
    (wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
    coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ, (
  (* value case *)
  ( v, to_val e1 = Some v  |={E}=> Φ v) 
  (* step case *)
  (to_val e1 = None   σ1,
     ownP_auth σ1 ={E,}=  reducible e1 σ1 
16
       e2 σ2 efs,  prim_step e1 σ1 e2 σ2 efs ={,E}=
17
       ownP_auth σ2  wp E e2 Φ 
18
       [ list] ef  efs, wp  ef (λ _, True)))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
19

20
21
22
23
24
Local Instance wp_pre_contractive `{irisG Λ Σ} : Contractive wp_pre.
Proof.
  rewrite /wp_pre=> n wp wp' Hwp E e1 Φ.
  apply or_ne, and_ne, forall_ne; auto=> σ1; apply wand_ne; auto.
  apply pvs_ne, sep_ne, later_contractive; auto=> i ?.
25
  apply forall_ne=> e2; apply forall_ne=> σ2; apply forall_ne=> efs.
26
  apply wand_ne, pvs_ne, sep_ne, sep_ne; auto; first by apply Hwp.
27
  apply big_opL_ne=> ? ef. by apply Hwp.
Robbert Krebbers's avatar
Robbert Krebbers committed
28
Qed.
29

30
31
Definition wp_def `{irisG Λ Σ} :
  coPset  expr Λ  (val Λ  iProp Σ)  iProp Σ := fixpoint wp_pre.
Ralf Jung's avatar
Ralf Jung committed
32
33
34
35
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.

Janno's avatar
Janno committed
36
Arguments wp {_ _ _} _ _%E _.
37
Instance: Params (@wp) 5.
Robbert Krebbers's avatar
Robbert Krebbers committed
38

Janno's avatar
Janno committed
39
Notation "'WP' e @ E {{ Φ } }" := (wp E e%E Φ)
40
  (at level 20, e, Φ at level 200,
41
   format "'WP'  e  @  E  {{  Φ  } }") : uPred_scope.
Janno's avatar
Janno committed
42
Notation "'WP' e {{ Φ } }" := (wp  e%E Φ)
43
  (at level 20, e, Φ at level 200,
44
   format "'WP'  e  {{  Φ  } }") : uPred_scope.
45

Janno's avatar
Janno committed
46
Notation "'WP' e @ E {{ v , Q } }" := (wp E e%E (λ v, Q))
47
48
  (at level 20, e, Q at level 200,
   format "'WP'  e  @  E  {{  v ,  Q  } }") : uPred_scope.
Janno's avatar
Janno committed
49
Notation "'WP' e {{ v , Q } }" := (wp  e%E (λ v, Q))
50
51
52
  (at level 20, e, Q at level 200,
   format "'WP'  e  {{  v ,  Q  } }") : uPred_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
53
Section wp.
54
55
56
Context `{irisG Λ Σ}.
Implicit Types P : iProp Σ.
Implicit Types Φ : val Λ  iProp Σ.
57
58
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Robbert Krebbers's avatar
Robbert Krebbers committed
59

60
61
62
Lemma wp_unfold E e Φ : WP e @ E {{ Φ }}  wp_pre wp E e Φ.
Proof. rewrite wp_eq. apply (fixpoint_unfold wp_pre). Qed.

63
Global Instance wp_ne E e n :
64
  Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ _ E e).
Robbert Krebbers's avatar
Robbert Krebbers committed
65
Proof.
66
67
68
69
70
71
72
  revert e. induction (lt_wf n) as [n _ IH]=> e Φ Ψ HΦ.
  rewrite !wp_unfold /wp_pre. apply or_ne, and_ne; auto; first solve_proper.
  apply forall_ne=> σ1.
  apply wand_ne, pvs_ne, sep_ne, later_contractive; auto=> i ?.
  apply forall_ne=> e2; apply forall_ne=> σ2; apply forall_ne=> ef.
  apply wand_ne, pvs_ne, sep_ne, sep_ne; auto.
  apply IH; [done|]=> v. eapply dist_le; eauto with omega.
Robbert Krebbers's avatar
Robbert Krebbers committed
73
74
Qed.
Global Instance wp_proper E e :
75
  Proper (pointwise_relation _ () ==> ()) (@wp Λ Σ _ E e).
Robbert Krebbers's avatar
Robbert Krebbers committed
76
Proof.
77
  by intros Φ Φ' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
Robbert Krebbers's avatar
Robbert Krebbers committed
78
Qed.
79

80
Lemma wp_value' E Φ v : Φ v  WP of_val v @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
81
Proof.
82
83
  iIntros "HΦ". rewrite wp_unfold /wp_pre.
  iLeft; iExists v; rewrite to_of_val; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
84
Qed.
85
Lemma wp_value_inv E Φ v : WP of_val v @ E {{ Φ }} ={E}=> Φ v.
Ralf Jung's avatar
Ralf Jung committed
86
Proof.
87
88
  rewrite wp_unfold /wp_pre to_of_val. iIntros "[H|[% _]]"; [|done].
  by iDestruct "H" as (v') "[% ?]"; simplify_eq.
Ralf Jung's avatar
Ralf Jung committed
89
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
90

91
92
93
Lemma wp_strong_mono E1 E2 e Φ Ψ :
  E1  E2  ( v, Φ v ={E2}= Ψ v)  WP e @ E1 {{ Φ }}  WP e @ E2 {{ Ψ }}.
Proof.
94
  iIntros (?) "[HΦ H]". iLöb as "IH" forall (e). rewrite !wp_unfold /wp_pre.
95
96
97
98
99
100
  iDestruct "H" as "[Hv|[% H]]"; [iLeft|iRight].
  { iDestruct "Hv" as (v) "[% Hv]". iExists v; iSplit; first done.
    iApply ("HΦ" with "==>[-]"). by iApply (pvs_mask_mono E1 _). }
  iSplit; [done|]; iIntros (σ1) "Hσ".
  iApply (pvs_trans _ E1); iApply pvs_intro'; auto. iIntros "Hclose".
  iVs ("H" $! σ1 with "Hσ") as "[$ H]".
101
102
  iVsIntro. iNext. iIntros (e2 σ2 efs Hstep).
  iVs ("H" $! _ σ2 efs with "[#]") as "($ & H & $)"; auto.
103
104
105
  iVs "Hclose" as "_". by iApply ("IH" with "HΦ").
Qed.

106
Lemma pvs_wp E e Φ : (|={E}=> WP e @ E {{ Φ }})  WP e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
107
Proof.
108
109
110
111
112
113
  rewrite wp_unfold /wp_pre. iIntros "H". destruct (to_val e) as [v|] eqn:?.
  { iLeft. iExists v; iSplit; first done.
    by iVs "H" as "[H|[% ?]]"; [iDestruct "H" as (v') "[% ?]"|]; simplify_eq. }
  iRight; iSplit; [done|]; iIntros (σ1) "Hσ1".
  iVs "H" as "[H|[% H]]"; last by iApply "H".
  iDestruct "H" as (v') "[% ?]"; simplify_eq.
114
Qed.
115
Lemma wp_pvs E e Φ : WP e @ E {{ v, |={E}=> Φ v }}  WP e @ E {{ Φ }}.
116
Proof. iIntros "H". iApply (wp_strong_mono E); try iFrame; auto. Qed.
117

118
Lemma wp_atomic E1 E2 e Φ :
119
  atomic e 
120
  (|={E1,E2}=> WP e @ E2 {{ v, |={E2,E1}=> Φ v }})  WP e @ E1 {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
121
Proof.
122
123
124
125
126
127
128
  iIntros (Hatomic) "H". destruct (to_val e) as [v|] eqn:He.
  { apply of_to_val in He as <-. iApply wp_pvs. iApply wp_value'.
    iVs "H". by iVs (wp_value_inv with "H"). }
  setoid_rewrite wp_unfold; rewrite /wp_pre. iRight; iSplit; auto.
  iIntros (σ1) "Hσ". iVs "H" as "[H|[_ H]]".
  { iDestruct "H" as (v') "[% ?]"; simplify_eq. }
  iVs ("H" $! σ1 with "Hσ") as "[$ H]".
129
  iVsIntro. iNext. iIntros (e2 σ2 efs Hstep).
130
  destruct (Hatomic _ _ _ _ Hstep) as [v <-%of_to_val].
131
  iVs ("H" $! _ σ2 efs with "[#]") as "($ & H & $)"; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
132
  iVs (wp_value_inv with "H") as "==> H". by iApply wp_value'.
Robbert Krebbers's avatar
Robbert Krebbers committed
133
Qed.
134
135
136

Lemma wp_frame_step_l E1 E2 e Φ R :
  to_val e = None  E2  E1 
137
  (|={E1,E2}=> R)  WP e @ E2 {{ Φ }}  WP e @ E1 {{ v, R  Φ v }}.
138
139
140
141
142
Proof.
  rewrite !wp_unfold /wp_pre. iIntros (??) "[HR [Hv|[_ H]]]".
  { iDestruct "Hv" as (v) "[% Hv]"; simplify_eq. }
  iRight; iSplit; [done|]. iIntros (σ1) "Hσ".
  iVs "HR". iVs ("H" $! _ with "Hσ") as "[$ H]".
143
144
  iVsIntro; iNext; iIntros (e2 σ2 efs Hstep).
  iVs ("H" $! e2 σ2 efs with "[%]") as "($ & H & $)"; auto.
145
  iVs "HR". iVsIntro. iApply (wp_strong_mono E2 _ _ Φ); try iFrame; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
146
Qed.
147

148
Lemma wp_bind `{LanguageCtx Λ K} E e Φ :
149
  WP e @ E {{ v, WP K (of_val v) @ E {{ Φ }} }}  WP K e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
Proof.
151
  iIntros "H". iLöb as "IH" forall (E e Φ). rewrite wp_unfold /wp_pre.
152
153
154
155
156
157
158
  iDestruct "H" as "[Hv|[% H]]".
  { iDestruct "Hv" as (v) "[Hev Hv]"; iDestruct "Hev" as % <-%of_to_val.
    by iApply pvs_wp. }
  rewrite wp_unfold /wp_pre. iRight; iSplit; eauto using fill_not_val.
  iIntros (σ1) "Hσ". iVs ("H" $! _ with "Hσ") as "[% H]".
  iVsIntro; iSplit.
  { iPureIntro. unfold reducible in *. naive_solver eauto using fill_step. }
159
160
161
  iNext; iIntros (e2 σ2 efs Hstep).
  destruct (fill_step_inv e σ1 e2 σ2 efs) as (e2'&->&?); auto.
  iVs ("H" $! e2' σ2 efs with "[%]") as "($ & H & $)"; auto.
162
  by iApply "IH".
Robbert Krebbers's avatar
Robbert Krebbers committed
163
164
Qed.

165
(** * Derived rules *)
166
Lemma wp_mono E e Φ Ψ : ( v, Φ v  Ψ v)  WP e @ E {{ Φ }}  WP e @ E {{ Ψ }}.
167
168
Proof.
  iIntros (HΦ) "H"; iApply (wp_strong_mono E E); auto.
169
  iFrame. iIntros (v) "?". by iApply HΦ.
170
171
172
Qed.
Lemma wp_mask_mono E1 E2 e Φ : E1  E2  WP e @ E1 {{ Φ }}  WP e @ E2 {{ Φ }}.
Proof. iIntros (?) "H"; iApply (wp_strong_mono E1 E2); auto. iFrame; eauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
173
Global Instance wp_mono' E e :
174
  Proper (pointwise_relation _ () ==> ()) (@wp Λ Σ _ E e).
175
Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
176

177
Lemma wp_value E Φ e v : to_val e = Some v  Φ v  WP e @ E {{ Φ }}.
178
Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed.
179
180
Lemma wp_value_pvs' E Φ v : (|={E}=> Φ v)  WP of_val v @ E {{ Φ }}.
Proof. intros. by rewrite -wp_pvs -wp_value'. Qed.
181
Lemma wp_value_pvs E Φ e v :
182
  to_val e = Some v  (|={E}=> Φ v)  WP e @ E {{ Φ }}.
183
Proof. intros. rewrite -wp_pvs -wp_value //. Qed.
184

185
Lemma wp_frame_l E e Φ R : R  WP e @ E {{ Φ }}  WP e @ E {{ v, R  Φ v }}.
186
187
188
189
190
191
Proof. iIntros "[??]". iApply (wp_strong_mono E E _ Φ); try iFrame; eauto. Qed.
Lemma wp_frame_r E e Φ R : WP e @ E {{ Φ }}  R  WP e @ E {{ v, Φ v  R }}.
Proof. iIntros "[??]". iApply (wp_strong_mono E E _ Φ); try iFrame; eauto. Qed.

Lemma wp_frame_step_r E1 E2 e Φ R :
  to_val e = None  E2  E1 
192
  WP e @ E2 {{ Φ }}  (|={E1,E2}=> R)  WP e @ E1 {{ v, Φ v  R }}.
Ralf Jung's avatar
Ralf Jung committed
193
Proof.
194
195
  rewrite [(WP _ @ _ {{ _ }}  _)%I]comm; setoid_rewrite (comm _ _ R).
  apply wp_frame_step_l.
Ralf Jung's avatar
Ralf Jung committed
196
197
Qed.
Lemma wp_frame_step_l' E e Φ R :
198
  to_val e = None   R  WP e @ E {{ Φ }}  WP e @ E {{ v, R  Φ v }}.
199
200
201
202
203
Proof. iIntros (?) "[??]". iApply (wp_frame_step_l E E); try iFrame; eauto. Qed.
Lemma wp_frame_step_r' E e Φ R :
  to_val e = None  WP e @ E {{ Φ }}   R  WP e @ E {{ v, Φ v  R }}.
Proof. iIntros (?) "[??]". iApply (wp_frame_step_r E E); try iFrame; eauto. Qed.

204
Lemma wp_wand_l E e Φ Ψ :
205
  ( v, Φ v - Ψ v)  WP e @ E {{ Φ }}  WP e @ E {{ Ψ }}.
206
207
208
209
Proof.
  iIntros "[H Hwp]". iApply (wp_strong_mono E); auto.
  iFrame "Hwp". iIntros (?) "?". by iApply "H".
Qed.
210
Lemma wp_wand_r E e Φ Ψ :
211
  WP e @ E {{ Φ }}  ( v, Φ v - Ψ v)  WP e @ E {{ Ψ }}.
212
Proof. by rewrite comm wp_wand_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
213
End wp.
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242

(** Proofmode class instances *)
Section proofmode_classes.
  Context `{irisG Λ Σ}.
  Implicit Types P Q : iProp Σ.
  Implicit Types Φ : val Λ  iProp Σ.

  Global Instance frame_wp E e R Φ Ψ :
    ( v, Frame R (Φ v) (Ψ v))  Frame R (WP e @ E {{ Φ }}) (WP e @ E {{ Ψ }}).
  Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.

  Global Instance is_except_last_wp E e Φ : IsExceptLast (WP e @ E {{ Φ }}).
  Proof. by rewrite /IsExceptLast -{2}pvs_wp -except_last_pvs -pvs_intro. Qed.

  Global Instance elim_vs_rvs_wp E e P Φ :
    ElimVs (|=r=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
  Proof. by rewrite /ElimVs (rvs_pvs E) pvs_frame_r wand_elim_r pvs_wp. Qed.

  Global Instance elim_vs_pvs_wp E e P Φ :
    ElimVs (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
  Proof. by rewrite /ElimVs pvs_frame_r wand_elim_r pvs_wp. Qed.

  (* lower precedence, if possible, it should always pick elim_vs_pvs_wp *)
  Global Instance elim_vs_pvs_wp_atomic E1 E2 e P Φ :
    atomic e 
    ElimVs (|={E1,E2}=> P) P
           (WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
  Proof. intros. by rewrite /ElimVs pvs_frame_r wand_elim_r wp_atomic. Qed.
End proofmode_classes.