weakestpre.v 8.91 KB
Newer Older
1
From iris.program_logic Require Export pviewshifts.
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
From iris.program_logic Require Import ownership.
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 
       e2 σ2 ef,  prim_step e1 σ1 e2 σ2 ef ={,E}=
       ownP_auth σ2  wp E e2 Φ 
       from_option (flip (wp ) (λ _, True)) True ef))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
18

19
20
21
22
23
24
25
26
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 ?.
  apply forall_ne=> e2; apply forall_ne=> σ2; apply forall_ne=> ef.
  apply wand_ne, pvs_ne, sep_ne, sep_ne; auto; first by apply Hwp.
  destruct ef; first apply Hwp; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
27
Qed.
28

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

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

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

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

52
53
Notation wp_fork ef := (from_option (flip (wp ) (λ _, True)) True ef)%I.

Robbert Krebbers's avatar
Robbert Krebbers committed
54
Section wp.
55
56
57
Context `{irisG Λ Σ}.
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
62
63
Lemma wp_unfold E e Φ : WP e @ E {{ Φ }}  wp_pre wp E e Φ.
Proof. rewrite wp_eq. apply (fixpoint_unfold wp_pre). Qed.

64
Global Instance wp_ne E e n :
65
  Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ _ E e).
Robbert Krebbers's avatar
Robbert Krebbers committed
66
Proof.
67
68
69
70
71
72
73
  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
74
75
Qed.
Global Instance wp_proper E e :
76
  Proper (pointwise_relation _ () ==> ()) (@wp Λ Σ _ E e).
Robbert Krebbers's avatar
Robbert Krebbers committed
77
Proof.
78
  by intros Φ Φ' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
Robbert Krebbers's avatar
Robbert Krebbers committed
79
Qed.
80

81
Lemma wp_value' E Φ v : Φ v  WP of_val v @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
82
Proof.
83
84
  iIntros "HΦ". rewrite wp_unfold /wp_pre.
  iLeft; iExists v; rewrite to_of_val; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
85
Qed.
86
Lemma wp_value_inv E Φ v : WP of_val v @ E {{ Φ }} ={E}=> Φ v.
Ralf Jung's avatar
Ralf Jung committed
87
Proof.
88
89
  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
90
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
91

92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
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]".
  iVsIntro. iNext. iIntros (e2 σ2 ef Hstep).
  iVs ("H" $! _ σ2 ef with "[#]") as "($ & H & $)"; auto.
  iVs "Hclose" as "_". by iApply ("IH" with "HΦ").
Qed.

107
Lemma pvs_wp E e Φ : (|={E}=> WP e @ E {{ Φ }})  WP e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
108
Proof.
109
110
111
112
113
114
  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.
115
Qed.
116
Lemma wp_pvs E e Φ : WP e @ E {{ v, |={E}=> Φ v }}  WP e @ E {{ Φ }}.
117
Proof. iIntros "H". iApply (wp_strong_mono E); try iFrame; auto. Qed.
118

119
Lemma wp_atomic E1 E2 e Φ :
120
  atomic e 
121
  (|={E1,E2}=> WP e @ E2 {{ v, |={E2,E1}=> Φ v }})  WP e @ E1 {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
122
Proof.
123
124
125
126
127
128
129
130
131
132
  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]".
  iVsIntro. iNext. iIntros (e2 σ2 ef Hstep).
  destruct (Hatomic _ _ _ _ Hstep) as [v <-%of_to_val].
  iVs ("H" $! _ σ2 ef with "[#]") as "($ & H & $)"; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
133
  iVs (wp_value_inv with "H") as "==> H". by iApply wp_value'.
Robbert Krebbers's avatar
Robbert Krebbers committed
134
Qed.
135
136
137
138
139
140
141
142
143
144
145
146

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]".
  iVsIntro; iNext; iIntros (e2 σ2 ef Hstep).
  iVs ("H" $! e2 σ2 ef with "[%]") as "($ & H & $)"; auto.
  iVs "HR". iVsIntro. iApply (wp_strong_mono E2 _ _ Φ); try iFrame; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
147
Qed.
148

149
Lemma wp_bind `{LanguageCtx Λ K} E e Φ :
150
  WP e @ E {{ v, WP K (of_val v) @ E {{ Φ }} }}  WP K e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
151
Proof.
152
153
154
155
156
157
158
159
160
  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. }
  iNext; iIntros (e2 σ2 ef Hstep).
161
  destruct (fill_step_inv e σ1 e2 σ2 ef) as (e2'&->&?); auto.
162
163
  iVs ("H" $! e2' σ2 ef with "[%]") as "($ & H & $)"; auto.
  by iApply "IH".
Robbert Krebbers's avatar
Robbert Krebbers committed
164
165
Qed.

166
(** * Derived rules *)
167
Lemma wp_mono E e Φ Ψ : ( v, Φ v  Ψ v)  WP e @ E {{ Φ }}  WP e @ E {{ Ψ }}.
168
169
Proof.
  iIntros (HΦ) "H"; iApply (wp_strong_mono E E); auto.
170
  iFrame. iIntros (v) "?". by iApply HΦ.
171
172
173
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
174
Global Instance wp_mono' E e :
175
  Proper (pointwise_relation _ () ==> ()) (@wp Λ Σ _ E e).
176
Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
177

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

186
Lemma wp_frame_l E e Φ R : R  WP e @ E {{ Φ }}  WP e @ E {{ v, R  Φ v }}.
187
188
189
190
191
192
193
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
194
Proof.
195
196
  rewrite [(WP _ @ _ {{ _ }}  _)%I]comm; setoid_rewrite (comm _ _ R).
  apply wp_frame_step_l.
Ralf Jung's avatar
Ralf Jung committed
197
198
Qed.
Lemma wp_frame_step_l' E e Φ R :
199
  to_val e = None   R  WP e @ E {{ Φ }}  WP e @ E {{ v, R  Φ v }}.
200
201
202
203
204
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.

205
Lemma wp_wand_l E e Φ Ψ :
206
  ( v, Φ v - Ψ v)  WP e @ E {{ Φ }}  WP e @ E {{ Ψ }}.
207
208
209
210
Proof.
  iIntros "[H Hwp]". iApply (wp_strong_mono E); auto.
  iFrame "Hwp". iIntros (?) "?". by iApply "H".
Qed.
211
Lemma wp_wand_r E e Φ Ψ :
212
  WP e @ E {{ Φ }}  ( v, Φ v - Ψ v)  WP e @ E {{ Ψ }}.
213
Proof. by rewrite comm wp_wand_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
214
End wp.