weakestpre.v 8.9 KB
Newer Older
1
From iris.program_logic Require Export pviewshifts.
2
From iris.program_logic Require Import ownership.
3
From iris.algebra Require Import upred_big_op.
4 5 6 7 8 9 10 11 12 13 14 15
From iris.prelude Require Export coPset.
From iris.proofmode Require Import tactics pviewshifts.
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_sepL_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 94 95 96 97 98 99 100
Lemma wp_strong_mono E1 E2 e Φ Ψ :
  E1  E2  ( v, Φ v ={E2}= Ψ v)  WP e @ E1 {{ Φ }}  WP e @ E2 {{ Ψ }}.
Proof.
  iIntros (?) "[HΦ H]". iLöb (e) as "IH". rewrite !wp_unfold /wp_pre.
  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 137 138 139 140 141 142

Lemma wp_frame_step_l E1 E2 e Φ R :
  to_val e = None  E2  E1 
  (|={E1,E2}=>  |={E2,E1}=> R)  WP e @ E2 {{ Φ }}  WP e @ E1 {{ v, R  Φ v }}.
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 152 153 154 155 156 157 158
  iIntros "H". iLöb (E e Φ) as "IH". rewrite wp_unfold /wp_pre.
  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 192
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 
  WP e @ E2 {{ Φ }}  (|={E1,E2}=>  |={E2,E1}=> 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.