weakestpre.v 13.7 KB
Newer Older
1
From iris.proofmode Require Import base tactics classes.
2 3
From iris.base_logic.lib Require Export fancy_updates.
From iris.program_logic Require Export language.
4 5
(* FIXME: If we import iris.bi.weakestpre earlier texan triples do not
   get pretty-printed correctly. *)
6
From iris.bi Require Export weakestpre.
7
Set Default Proof Using "Type".
8 9
Import uPred.

Robbert Krebbers's avatar
Robbert Krebbers committed
10
Class irisG (Λ : language) (Σ : gFunctors) := IrisG {
11
  iris_invG :> invG Σ;
12 13 14 15 16 17

  (** The state interpretation is an invariant that should hold in between each
  step of reduction. Here [Λstate] is the global state, [list Λobservation] are
  the remaining observations, and [nat] is the number of forked-off threads
  (not the total number of threads, which is one higher because there is always
  a main thread). *)
Robbert Krebbers's avatar
Robbert Krebbers committed
18
  state_interp : state Λ  list (observation Λ)  nat  iProp Σ;
19 20 21 22

  (** A fixed postcondition for any forked-off thread. For most languages, e.g.
  heap_lang, this will simply be [True]. However, it is useful if one wants to
  keep track of resources precisely, as in e.g. Iron. *)
23
  fork_post : val Λ  iProp Σ;
24
}.
25
Global Opaque iris_invG.
26

27
Definition wp_pre `{!irisG Λ Σ} (s : stuckness)
28 29
    (wp : coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ) :
    coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ := λ E e1 Φ,
30 31
  match to_val e1 with
  | Some v => |={E}=> Φ v
32 33 34 35 36 37
  | None =>  σ1 κ κs n,
     state_interp σ1 (κ ++ κs) n ={E,}=
       if s is NotStuck then reducible e1 σ1 else True 
        e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs ={,,E}=
         state_interp σ2 κs (length efs + n) 
         wp E e2 Φ 
38
         [ list] i  ef  efs, wp  ef fork_post
39
  end%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
40

41
Local Instance wp_pre_contractive `{!irisG Λ Σ} s : Contractive (wp_pre s).
42 43
Proof.
  rewrite /wp_pre=> n wp wp' Hwp E e1 Φ.
44
  repeat (f_contractive || f_equiv); apply Hwp.
Robbert Krebbers's avatar
Robbert Krebbers committed
45
Qed.
46

47
Definition wp_def `{!irisG Λ Σ} (s : stuckness) :
48
  coPset  expr Λ  (val Λ  iProp Σ)  iProp Σ := fixpoint (wp_pre s).
49 50 51
Definition wp_aux `{!irisG Λ Σ} : seal (@wp_def Λ Σ _). by eexists. Qed.
Instance wp' `{!irisG Λ Σ} : Wp Λ (iProp Σ) stuckness := wp_aux.(unseal).
Definition wp_eq `{!irisG Λ Σ} : wp = @wp_def Λ Σ _ := wp_aux.(seal_eq).
52

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

61
(* Weakest pre *)
62 63
Lemma wp_unfold s E e Φ :
  WP e @ s; E {{ Φ }}  wp_pre s (wp (PROP:=iProp Σ)  s) E e Φ.
64
Proof. rewrite wp_eq. apply (fixpoint_unfold (wp_pre s)). Qed.
65

66
Global Instance wp_ne s E e n :
67
  Proper (pointwise_relation _ (dist n) ==> dist n) (wp (PROP:=iProp Σ) s E e).
Robbert Krebbers's avatar
Robbert Krebbers committed
68
Proof.
69
  revert e. induction (lt_wf n) as [n _ IH]=> e Φ Ψ HΦ.
70 71 72 73
  rewrite !wp_unfold /wp_pre.
  (* FIXME: figure out a way to properly automate this proof *)
  (* FIXME: reflexivity, as being called many times by f_equiv and f_contractive
  is very slow here *)
74
  do 24 (f_contractive || f_equiv). apply IH; first lia.
Ralf Jung's avatar
Ralf Jung committed
75
  intros v. eapply dist_le; eauto with lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
76
Qed.
77
Global Instance wp_proper s E e :
78
  Proper (pointwise_relation _ () ==> ()) (wp (PROP:=iProp Σ) s E e).
Robbert Krebbers's avatar
Robbert Krebbers committed
79
Proof.
80
  by intros Φ Φ' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
Robbert Krebbers's avatar
Robbert Krebbers committed
81
Qed.
82

83
Lemma wp_value' s E Φ v : Φ v  WP of_val v @ s; E {{ Φ }}.
84
Proof. iIntros "HΦ". rewrite wp_unfold /wp_pre to_of_val. auto. Qed.
85
Lemma wp_value_inv' s E Φ v : WP of_val v @ s; E {{ Φ }} ={E}= Φ v.
86
Proof. by rewrite wp_unfold /wp_pre to_of_val. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
87

88 89
Lemma wp_strong_mono s1 s2 E1 E2 e Φ Ψ :
  s1  s2  E1  E2 
90
  WP e @ s1; E1 {{ Φ }} - ( v, Φ v ={E2}= Ψ v) - WP e @ s2; E2 {{ Ψ }}.
91
Proof.
92
  iIntros (? HE) "H HΦ". iLöb as "IH" forall (e E1 E2 HE Φ Ψ).
93
  rewrite !wp_unfold /wp_pre.
94
  destruct (to_val e) as [v|] eqn:?.
95
  { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
96
  iIntros (σ1 κ κs n) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
97
  iMod ("H" with "[$]") as "[% H]".
98
  iModIntro. iSplit; [by destruct s1, s2|]. iIntros (e2 σ2 efs Hstep).
99 100 101
  iMod ("H" with "[//]") as "H". iIntros "!> !>".
  iMod "H" as "(Hσ & H & Hefs)".
  iMod "Hclose" as "_". iModIntro. iFrame "Hσ". iSplitR "Hefs".
102
  - iApply ("IH" with "[//] H HΦ").
103 104
  - iApply (big_sepL_impl with "Hefs"); iIntros "!#" (k ef _).
    iIntros "H". iApply ("IH" with "[] H"); auto.
105 106 107
Qed.

Lemma fupd_wp s E e Φ : (|={E}=> WP e @ s; E {{ Φ }})  WP e @ s; E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
108
Proof.
109
  rewrite wp_unfold /wp_pre. iIntros "H". destruct (to_val e) as [v|] eqn:?.
110
  { by iMod "H". }
111
  iIntros (σ1 κ κs n) "Hσ1". iMod "H". by iApply "H".
112
Qed.
113
Lemma wp_fupd s E e Φ : WP e @ s; E {{ v, |={E}=> Φ v }}  WP e @ s; E {{ Φ }}.
114
Proof. iIntros "H". iApply (wp_strong_mono s s E with "H"); auto. Qed.
115

Ralf Jung's avatar
Ralf Jung committed
116
Lemma wp_atomic s E1 E2 e Φ `{!Atomic (stuckness_to_atomicity s) e} :
117
  (|={E1,E2}=> WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})  WP e @ s; E1 {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
118
Proof.
David Swasey's avatar
David Swasey committed
119
  iIntros "H". rewrite !wp_unfold /wp_pre.
120 121
  destruct (to_val e) as [v|] eqn:He.
  { by iDestruct "H" as ">>> $". }
122
  iIntros (σ1 κ κs n) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
123
  iModIntro. iIntros (e2 σ2 efs Hstep).
124 125
  iMod ("H" with "[//]") as "H". iIntros "!>!>".
  iMod "H" as "(Hσ & H & Hefs)". destruct s.
126
  - rewrite !wp_unfold /wp_pre. destruct (to_val e2) as [v2|] eqn:He2.
David Swasey's avatar
David Swasey committed
127
    + iDestruct "H" as ">> $". by iFrame.
128
    + iMod ("H" $! _ [] with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ? & ?).
129 130
      by edestruct (atomic _ _ _ _ _ Hstep).
  - destruct (atomic _ _ _ _ _ Hstep) as [v <-%of_to_val].
131 132
    iMod (wp_value_inv' with "H") as ">H".
    iModIntro. iFrame "Hσ Hefs". by iApply wp_value'.
Robbert Krebbers's avatar
Robbert Krebbers committed
133
Qed.
134

135
Lemma wp_step_fupd s E1 E2 e P Φ :
136
  to_val e = None  E2  E1 
137
  (|={E1,E2}=> P) - WP e @ s; E2 {{ v, P ={E1}= Φ v }} - WP e @ s; E1 {{ Φ }}.
138
Proof.
139
  rewrite !wp_unfold /wp_pre. iIntros (-> ?) "HR H".
140
  iIntros (σ1 κ κs n) "Hσ". iMod "HR". iMod ("H" with "[$]") as "[$ H]".
141
  iIntros "!>" (e2 σ2 efs Hstep). iMod ("H" $! e2 σ2 efs with "[% //]") as "H".
142 143 144
  iIntros "!>!>". iMod "H" as "(Hσ & H & Hefs)".
  iMod "HR". iModIntro. iFrame "Hσ Hefs".
  iApply (wp_strong_mono s s E2 with "H"); [done..|].
145
  iIntros (v) "H". by iApply "H".
Robbert Krebbers's avatar
Robbert Krebbers committed
146
Qed.
147

148
Lemma wp_bind K `{!LanguageCtx K} s E e Φ :
149
  WP e @ s; E {{ v, WP K (of_val v) @ s; E {{ Φ }} }}  WP K e @ s; 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
  destruct (to_val e) as [v|] eqn:He.
  { apply of_to_val in He as <-. by iApply fupd_wp. }
  rewrite wp_unfold /wp_pre fill_not_val //.
155
  iIntros (σ1 κ κs n) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
156 157
  { iPureIntro. destruct s; last done.
    unfold reducible in *. naive_solver eauto using fill_step. }
158
  iIntros (e2 σ2 efs Hstep).
159
  destruct (fill_step_inv e σ1 κ e2 σ2 efs) as (e2'&->&?); auto.
160
  iMod ("H" $! e2' σ2 efs with "[//]") as "H". iIntros "!>!>".
161 162
  iMod "H" as "(Hσ & H & Hefs)".
  iModIntro. iFrame "Hσ Hefs". by iApply "IH".
Robbert Krebbers's avatar
Robbert Krebbers committed
163 164
Qed.

165
Lemma wp_bind_inv K `{!LanguageCtx K} s E e Φ :
166
  WP K e @ s; E {{ Φ }}  WP e @ s; E {{ v, WP K (of_val v) @ s; E {{ Φ }} }}.
167 168 169 170 171
Proof.
  iIntros "H". iLöb as "IH" forall (E e Φ). rewrite !wp_unfold /wp_pre.
  destruct (to_val e) as [v|] eqn:He.
  { apply of_to_val in He as <-. by rewrite !wp_unfold /wp_pre. }
  rewrite fill_not_val //.
172
  iIntros (σ1 κ κs n) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
173
  { destruct s; eauto using reducible_fill. }
174 175
  iIntros (e2 σ2 efs Hstep).
  iMod ("H" $! (K e2) σ2 efs with "[]") as "H"; [by eauto using fill_step|].
176 177
  iIntros "!>!>". iMod "H" as "(Hσ & H & Hefs)".
  iModIntro. iFrame "Hσ Hefs". by iApply "IH".
178 179
Qed.

180
(** * Derived rules *)
181
Lemma wp_mono s E e Φ Ψ : ( v, Φ v  Ψ v)  WP e @ s; E {{ Φ }}  WP e @ s; E {{ Ψ }}.
182
Proof.
183 184
  iIntros (HΦ) "H"; iApply (wp_strong_mono with "H"); auto.
  iIntros (v) "?". by iApply HΦ.
185
Qed.
David Swasey's avatar
David Swasey committed
186
Lemma wp_stuck_mono s1 s2 E e Φ :
187
  s1  s2  WP e @ s1; E {{ Φ }}  WP e @ s2; E {{ Φ }}.
188
Proof. iIntros (?) "H". iApply (wp_strong_mono with "H"); auto. Qed.
189 190 191
Lemma wp_stuck_weaken s E e Φ :
  WP e @ s; E {{ Φ }}  WP e @ E ?{{ Φ }}.
Proof. apply wp_stuck_mono. by destruct s. Qed.
192
Lemma wp_mask_mono s E1 E2 e Φ : E1  E2  WP e @ s; E1 {{ Φ }}  WP e @ s; E2 {{ Φ }}.
193
Proof. iIntros (?) "H"; iApply (wp_strong_mono with "H"); auto. Qed.
194
Global Instance wp_mono' s E e :
195
  Proper (pointwise_relation _ () ==> ()) (wp (PROP:=iProp Σ) s E e).
196
Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
197 198 199
Global Instance wp_flip_mono' s E e :
  Proper (pointwise_relation _ (flip ()) ==> (flip ())) (wp (PROP:=iProp Σ) s E e).
Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
200

201 202
Lemma wp_value s E Φ e v : IntoVal e v  Φ v  WP e @ s; E {{ Φ }}.
Proof. intros <-. by apply wp_value'. Qed.
203
Lemma wp_value_fupd' s E Φ v : (|={E}=> Φ v)  WP of_val v @ s; E {{ Φ }}.
204
Proof. intros. by rewrite -wp_fupd -wp_value'. Qed.
205 206
Lemma wp_value_fupd s E Φ e v `{!IntoVal e v} :
  (|={E}=> Φ v)  WP e @ s; E {{ Φ }}.
207
Proof. intros. rewrite -wp_fupd -wp_value //. Qed.
208 209
Lemma wp_value_inv s E Φ e v : IntoVal e v  WP e @ s; E {{ Φ }} ={E}= Φ v.
Proof. intros <-. by apply wp_value_inv'. Qed.
210

211
Lemma wp_frame_l s E e Φ R : R  WP e @ s; E {{ Φ }}  WP e @ s; E {{ v, R  Φ v }}.
212
Proof. iIntros "[? H]". iApply (wp_strong_mono with "H"); auto with iFrame. Qed.
213
Lemma wp_frame_r s E e Φ R : WP e @ s; E {{ Φ }}  R  WP e @ s; E {{ v, Φ v  R }}.
214
Proof. iIntros "[H ?]". iApply (wp_strong_mono with "H"); auto with iFrame. Qed.
215

216
Lemma wp_frame_step_l s E1 E2 e Φ R :
217
  to_val e = None  E2  E1 
218
  (|={E1,E2}=> R)  WP e @ s; E2 {{ Φ }}  WP e @ s; E1 {{ v, R  Φ v }}.
219
Proof.
220
  iIntros (??) "[Hu Hwp]". iApply (wp_step_fupd with "Hu"); try done.
221 222
  iApply (wp_mono with "Hwp"). by iIntros (?) "$$".
Qed.
223
Lemma wp_frame_step_r s E1 E2 e Φ R :
224
  to_val e = None  E2  E1 
225
  WP e @ s; E2 {{ Φ }}  (|={E1,E2}=> R)  WP e @ s; E1 {{ v, Φ v  R }}.
Ralf Jung's avatar
Ralf Jung committed
226
Proof.
227
  rewrite [(WP _ @ _; _ {{ _ }}  _)%I]comm; setoid_rewrite (comm _ _ R).
228
  apply wp_frame_step_l.
Ralf Jung's avatar
Ralf Jung committed
229
Qed.
230 231 232 233 234 235 236 237 238
Lemma wp_frame_step_l' s E e Φ R :
  to_val e = None   R  WP e @ s; E {{ Φ }}  WP e @ s; E {{ v, R  Φ v }}.
Proof. iIntros (?) "[??]". iApply (wp_frame_step_l s E E); try iFrame; eauto. Qed.
Lemma wp_frame_step_r' s E e Φ R :
  to_val e = None  WP e @ s; E {{ Φ }}   R  WP e @ s; E {{ v, Φ v  R }}.
Proof. iIntros (?) "[??]". iApply (wp_frame_step_r s E E); try iFrame; eauto. Qed.

Lemma wp_wand s E e Φ Ψ :
  WP e @ s; E {{ Φ }} - ( v, Φ v - Ψ v) - WP e @ s; E {{ Ψ }}.
239
Proof.
240 241
  iIntros "Hwp H". iApply (wp_strong_mono with "Hwp"); auto.
  iIntros (?) "?". by iApply "H".
242
Qed.
243 244
Lemma wp_wand_l s E e Φ Ψ :
  ( v, Φ v - Ψ v)  WP e @ s; E {{ Φ }}  WP e @ s; E {{ Ψ }}.
245
Proof. iIntros "[H Hwp]". iApply (wp_wand with "Hwp H"). Qed.
246 247
Lemma wp_wand_r s E e Φ Ψ :
  WP e @ s; E {{ Φ }}  ( v, Φ v - Ψ v)  WP e @ s; E {{ Ψ }}.
248
Proof. iIntros "[Hwp H]". iApply (wp_wand with "Hwp H"). Qed.
249
Lemma wp_frame_wand_l s E e Q Φ :
Ralf Jung's avatar
Ralf Jung committed
250
  Q  WP e @ s; E {{ v, Q - Φ v }} - WP e @ s; E {{ Φ }}.
251 252 253
Proof.
  iIntros "[HQ HWP]". iApply (wp_wand with "HWP").
  iIntros (v) "HΦ". by iApply "HΦ".
Ralf Jung's avatar
Ralf Jung committed
254
Qed.
255

Robbert Krebbers's avatar
Robbert Krebbers committed
256
End wp.
257 258 259

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

264
  Global Instance frame_wp p s E e R Φ Ψ :
265
    ( v, Frame p R (Φ v) (Ψ v)) 
266 267
    Frame p R (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Ψ }}).
  Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
268

269
  Global Instance is_except_0_wp s E e Φ : IsExcept0 (WP e @ s; E {{ Φ }}).
270
  Proof. by rewrite /IsExcept0 -{2}fupd_wp -except_0_fupd -fupd_intro. Qed.
271

272 273 274 275 276 277 278 279 280 281 282 283 284 285 286
  Global Instance elim_modal_bupd_wp p s E e P Φ :
    ElimModal True p false (|==> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
  Proof.
    by rewrite /ElimModal intuitionistically_if_elim
      (bupd_fupd E) fupd_frame_r wand_elim_r fupd_wp.
  Qed.

  Global Instance elim_modal_fupd_wp p s E e P Φ :
    ElimModal True p false (|={E}=> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
  Proof.
    by rewrite /ElimModal intuitionistically_if_elim
      fupd_frame_r wand_elim_r fupd_wp.
  Qed.

  Global Instance elim_modal_fupd_wp_atomic p s E1 E2 e P Φ :
Ralf Jung's avatar
Ralf Jung committed
287
    Atomic (stuckness_to_atomicity s) e 
288
    ElimModal True p false (|={E1,E2}=> P) P
289
            (WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I.
290 291 292 293
  Proof.
    intros. by rewrite /ElimModal intuitionistically_if_elim
      fupd_frame_r wand_elim_r wp_atomic.
  Qed.
294 295 296 297

  Global Instance add_modal_fupd_wp s E e P Φ :
    AddModal (|={E}=> P) P (WP e @ s; E {{ Φ }}).
  Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_wp. Qed.
298

Ralf Jung's avatar
Ralf Jung committed
299
  Global Instance elim_acc_wp {X} E1 E2 α β γ e s Φ :
300
    Atomic (stuckness_to_atomicity s) e 
301 302
    ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1)
            α β γ (WP e @ s; E1 {{ Φ }})
303
            (λ x, WP e @ s; E2 {{ v, |={E2}=> β x  (γ x -? Φ v) }})%I.
304
  Proof.
305
    intros ?. rewrite /ElimAcc.
306
    iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
307
    iApply (wp_wand with "(Hinner Hα)").
308
    iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
309 310
  Qed.

Ralf Jung's avatar
Ralf Jung committed
311
  Global Instance elim_acc_wp_nonatomic {X} E α β γ e s Φ :
312 313
    ElimAcc (X:=X) (fupd E E) (fupd E E)
            α β γ (WP e @ s; E {{ Φ }})
314
            (λ x, WP e @ s; E {{ v, |={E}=> β x  (γ x -? Φ v) }})%I.
315
  Proof.
316
    rewrite /ElimAcc.
317 318
    iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
    iApply wp_fupd.
319
    iApply (wp_wand with "(Hinner Hα)").
320
    iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
321
  Qed.
322
End proofmode_classes.