lifting.v 12.6 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
Require Import prelude.gmap iris.lifting.
2
Require Export iris.weakestpre barrier.parameter.
3
4
Import uPred.

5
6
7
Section lifting.
Implicit Types P : iProp Σ.
Implicit Types Q : ival Σ  iProp Σ.
Ralf Jung's avatar
Ralf Jung committed
8
9

(** Bind. *)
10
Lemma wp_bind {E e} K Q :
11
12
  wp E e (λ v, wp E (fill K (v2e v)) Q)  wp E (fill K e) Q.
Proof. apply (wp_bind (K:=fill K)), fill_is_ctx. Qed.
Ralf Jung's avatar
Ralf Jung committed
13

14
(** Base axioms for core primitives of the language: Stateful reductions. *)
15
16
17
18
19

Lemma wp_lift_step E1 E2 (φ : expr  state  Prop) Q e1 σ1 :
  E1  E2  to_val e1 = None 
  reducible e1 σ1 
  ( e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef  ef = None  φ e2 σ2) 
20
21
22
  pvs E2 E1 (ownP σ1    e2 σ2, ( φ e2 σ2  ownP σ2) -
    pvs E1 E2 (wp E2 e2 Q))
   wp E2 e1 Q.
23
24
Proof.
  intros ? He Hsafe Hstep.
25
  (* RJ: working around https://coq.inria.fr/bugs/show_bug.cgi?id=4536 *)
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
  etransitivity; last eapply wp_lift_step with (σ2 := σ1)
    (φ0 := λ e' σ' ef, ef = None  φ e' σ'); last first.
  - intros e2 σ2 ef Hstep'%prim_ectx_step; last done.
    by apply Hstep.
  - destruct Hsafe as (e' & σ' & ? & ?).
    do 3 eexists. exists EmptyCtx. do 2 eexists.
    split_ands; try (by rewrite fill_empty); eassumption.
  - done.
  - eassumption.
  - apply pvs_mono. apply sep_mono; first done.
    apply later_mono. apply forall_mono=>e2. apply forall_mono=>σ2.
    apply forall_intro=>ef. apply wand_intro_l.
    rewrite always_and_sep_l' -associative -always_and_sep_l'.
    apply const_elim_l; move=>[-> Hφ]. eapply const_intro_l; first eexact Hφ.
    rewrite always_and_sep_l' associative -always_and_sep_l' wand_elim_r.
    apply pvs_mono. rewrite right_id. done.
Qed.
43
44
45

(* TODO RJ: Figure out some better way to make the
   postcondition a predicate over a *location* *)
46
Lemma wp_alloc_pst E σ e v Q :
47
  e2v e = Some v 
48
49
  (ownP σ  ( l, (σ !! l = None)  ownP (<[l:=v]>σ) - Q (LocV l)))
        wp E (Alloc e) Q.
50
Proof.
51
  (* RJ FIXME (also for most other lemmas in this file): rewrite would be nicer... *)
52
  intros Hvl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
53
    (φ := λ e' σ',  l, e' = Loc l  σ' = <[l:=v]>σ  σ !! l = None);
54
    last first.
55
  - intros e2 σ2 ef Hstep. inversion_clear Hstep. split; first done.
56
    rewrite Hv in Hvl. inversion_clear Hvl.
57
    eexists; split_ands; done.
58
  - set (l := fresh $ dom (gset loc) σ).
59
    exists (Loc l), ((<[l:=v]>)σ), None. eapply AllocS; first done.
60
    apply (not_elem_of_dom (D := gset loc)). apply is_fresh.
61
62
  - reflexivity.
  - reflexivity.
63
  - rewrite -pvs_intro. apply sep_mono; first done. apply later_mono.
64
    apply forall_intro=>e2. apply forall_intro=>σ2.
65
66
    apply wand_intro_l. rewrite -pvs_intro.
    rewrite always_and_sep_l' -associative -always_and_sep_l'.
67
    apply const_elim_l. intros [l [-> [-> Hl]]].
68
    rewrite (forall_elim l). eapply const_intro_l; first eexact Hl.
69
70
    rewrite always_and_sep_l' associative -always_and_sep_l' wand_elim_r.
    rewrite -wp_value'; done.
71
Qed.
Ralf Jung's avatar
Ralf Jung committed
72

73
Lemma wp_load_pst E σ l v Q :
Ralf Jung's avatar
Ralf Jung committed
74
  σ !! l = Some v 
75
  (ownP σ  (ownP σ - Q v))  wp E (Load (Loc l)) Q.
Ralf Jung's avatar
Ralf Jung committed
76
77
Proof.
  intros Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
78
79
80
    (φ := λ e' σ', e' = v2e v  σ' = σ); last first.
  - intros e2 σ2 ef Hstep. move: Hl. inversion_clear Hstep=>{σ}.
    rewrite Hlookup. case=>->. done.
81
  - do 3 eexists. econstructor; eassumption.
Ralf Jung's avatar
Ralf Jung committed
82
83
  - reflexivity.
  - reflexivity.
84
85
  - rewrite -pvs_intro.
    apply sep_mono; first done. apply later_mono.
86
    apply forall_intro=>e2. apply forall_intro=>σ2.
87
88
    apply wand_intro_l. rewrite -pvs_intro.
    rewrite always_and_sep_l' -associative -always_and_sep_l'.
89
    apply const_elim_l. intros [-> ->].
90
    by rewrite wand_elim_r -wp_value.
Ralf Jung's avatar
Ralf Jung committed
91
92
Qed.

93
Lemma wp_store_pst E σ l e v v' Q :
94
  e2v e = Some v 
Ralf Jung's avatar
Ralf Jung committed
95
  σ !! l = Some v' 
96
  (ownP σ  (ownP (<[l:=v]>σ) - Q LitUnitV))  wp E (Store (Loc l) e) Q.
Ralf Jung's avatar
Ralf Jung committed
97
Proof.
98
  intros Hvl Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
99
100
    (φ := λ e' σ', e' = LitUnit  σ' = <[l:=v]>σ); last first.
  - intros e2 σ2 ef Hstep. move: Hl. inversion_clear Hstep=>{σ2}.
101
102
    rewrite Hvl in Hv. inversion_clear Hv. done.
  - do 3 eexists. eapply StoreS; last (eexists; eassumption). eassumption.
Ralf Jung's avatar
Ralf Jung committed
103
104
  - reflexivity.
  - reflexivity.
105
106
  - rewrite -pvs_intro.
    apply sep_mono; first done. apply later_mono.
107
    apply forall_intro=>e2. apply forall_intro=>σ2.
108
109
    apply wand_intro_l. rewrite -pvs_intro.
    rewrite always_and_sep_l' -associative -always_and_sep_l'.
110
    apply const_elim_l. intros [-> ->].
111
    by rewrite wand_elim_r -wp_value'.
Ralf Jung's avatar
Ralf Jung committed
112
Qed.
113

114
Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Q :
Ralf Jung's avatar
Ralf Jung committed
115
116
  e2v e1 = Some v1  e2v e2 = Some v2 
  σ !! l = Some v'  v' <> v1 
117
  (ownP σ  (ownP σ - Q LitFalseV))  wp E (Cas (Loc l) e1 e2) Q.
Ralf Jung's avatar
Ralf Jung committed
118
119
120
121
122
123
124
125
126
127
Proof.
  intros Hvl Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
    (φ := λ e' σ', e' = LitFalse  σ' = σ); last first.
  - intros e2' σ2' ef Hstep. inversion_clear Hstep; first done.
    (* FIXME this rewriting is rather ugly. *)
    exfalso. rewrite Hvl in Hv1. case:Hv1=>?; subst v1. rewrite Hlookup in H.
    case:H=>?; subst v'. done.
  - do 3 eexists. eapply CasFailS; eassumption.
  - reflexivity.
  - reflexivity.
128
129
  - rewrite -pvs_intro.
    apply sep_mono; first done. apply later_mono.
Ralf Jung's avatar
Ralf Jung committed
130
    apply forall_intro=>e2'. apply forall_intro=>σ2'.
131
132
    apply wand_intro_l. rewrite -pvs_intro.
    rewrite always_and_sep_l' -associative -always_and_sep_l'.
Ralf Jung's avatar
Ralf Jung committed
133
    apply const_elim_l. intros [-> ->].
134
    by rewrite wand_elim_r -wp_value'.
Ralf Jung's avatar
Ralf Jung committed
135
136
Qed.

137
Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Q :
Ralf Jung's avatar
Ralf Jung committed
138
139
  e2v e1 = Some v1  e2v e2 = Some v2 
  σ !! l = Some v1 
140
  (ownP σ  (ownP (<[l:=v2]>σ) - Q LitTrueV))  wp E (Cas (Loc l) e1 e2) Q.
Ralf Jung's avatar
Ralf Jung committed
141
142
143
144
145
146
147
148
149
150
151
152
Proof.
  intros Hvl Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
    (φ := λ e' σ', e' = LitTrue  σ' = <[l:=v2]>σ); last first.
  - intros e2' σ2' ef Hstep. move:H. inversion_clear Hstep=>H.
    (* FIXME this rewriting is rather ugly. *)
    + exfalso. rewrite H in Hlookup. case:Hlookup=>?; subst vl.
      rewrite Hvl in Hv1. case:Hv1=>?; subst v1. done.
    + rewrite H in Hlookup. case:Hlookup=>?; subst v1.
      rewrite Hl in Hv2. case:Hv2=>?; subst v2. done.
  - do 3 eexists. eapply CasSucS; eassumption.
  - reflexivity.
  - reflexivity.
153
154
  - rewrite -pvs_intro.
    apply sep_mono; first done. apply later_mono.
Ralf Jung's avatar
Ralf Jung committed
155
    apply forall_intro=>e2'. apply forall_intro=>σ2'.
156
157
    apply wand_intro_l. rewrite -pvs_intro.
    rewrite always_and_sep_l' -associative -always_and_sep_l'.
Ralf Jung's avatar
Ralf Jung committed
158
    apply const_elim_l. intros [-> ->].
159
    by rewrite wand_elim_r -wp_value'.
Ralf Jung's avatar
Ralf Jung committed
160
161
Qed.

162
163
164
(** Base axioms for core primitives of the language: Stateless reductions *)

Lemma wp_fork E e :
165
   wp coPset_all e (λ _, True)  wp E (Fork e) (λ v, (v = LitUnitV)).
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
Proof.
  etransitivity; last eapply wp_lift_pure_step with
    (φ := λ e' ef, e' = LitUnit  ef = Some e);
    last first.
  - intros σ1 e2 σ2 ef Hstep%prim_ectx_step; last first.
    { do 3 eexists. eapply ForkS. }
    inversion_clear Hstep. done.
  - intros ?. do 3 eexists. exists EmptyCtx. do 2 eexists.
    split_ands; try (by rewrite fill_empty); [].
    eapply ForkS.
  - reflexivity.
  - apply later_mono.
    apply forall_intro=>e2. apply forall_intro=>ef.
    apply impl_intro_l. apply const_elim_l. intros [-> ->].
    (* FIXME RJ This is ridicolous. *)
    transitivity (True  wp coPset_all e (λ _ : ival Σ, True))%I;
      first by rewrite left_id.
    apply sep_mono; last reflexivity.
184
185
    rewrite -wp_value'; last reflexivity.
    by apply const_intro.
186
Qed.
187
188
189
190
191

Lemma wp_lift_pure_step E (φ : expr  Prop) Q e1 :
  to_val e1 = None 
  ( σ1, reducible e1 σ1) 
  ( σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef  σ1 = σ2  ef = None  φ e2) 
192
  (  e2,  φ e2  wp E e2 Q)  wp E e1 Q.
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
Proof.
  intros He Hsafe Hstep.
  (* RJ: working around https://coq.inria.fr/bugs/show_bug.cgi?id=4536 *)
  etransitivity; last eapply wp_lift_pure_step with
    (φ0 := λ e' ef, ef = None  φ e'); last first.
  - intros σ1 e2 σ2 ef Hstep'%prim_ectx_step; last done.
    by apply Hstep.
  - intros σ1. destruct (Hsafe σ1) as (e' & σ' & ? & ?).
    do 3 eexists. exists EmptyCtx. do 2 eexists.
    split_ands; try (by rewrite fill_empty); eassumption.
  - done.
  - apply later_mono. apply forall_mono=>e2. apply forall_intro=>ef.
    apply impl_intro_l. apply const_elim_l; move=>[-> Hφ].
    eapply const_intro_l; first eexact Hφ. rewrite impl_elim_r.
    rewrite right_id. done.
Qed.
209

210
211
Lemma wp_rec E ef e v Q :
  e2v e = Some v 
212
  wp E ef.[Rec ef, e /] Q  wp E (App (Rec ef) e) Q.
213
214
Proof.
  etransitivity; last eapply wp_lift_pure_step with
215
    (φ := λ e', e' = ef.[Rec ef, e /]); last first.
216
  - intros ? ? ? ? Hstep. inversion_clear Hstep. done.
217
  - intros ?. do 3 eexists. eapply BetaS; eassumption.
218
219
220
221
222
  - reflexivity.
  - apply later_mono, forall_intro=>e2. apply impl_intro_l.
    apply const_elim_l=>->. done.
Qed.

Ralf Jung's avatar
Ralf Jung committed
223
Lemma wp_plus n1 n2 E Q :
224
  Q (LitNatV (n1 + n2))  wp E (Plus (LitNat n1) (LitNat n2)) Q.
225
226
227
228
229
230
231
232
Proof.
  etransitivity; last eapply wp_lift_pure_step with
    (φ := λ e', e' = LitNat (n1 + n2)); last first.
  - intros ? ? ? ? Hstep. inversion_clear Hstep; done.
  - intros ?. do 3 eexists. econstructor.
  - reflexivity.
  - apply later_mono, forall_intro=>e2. apply impl_intro_l.
    apply const_elim_l=>->.
Ralf Jung's avatar
Ralf Jung committed
233
234
235
236
237
    rewrite -wp_value'; last reflexivity; done.
Qed.

Lemma wp_le_true n1 n2 E Q :
  n1  n2 
238
  Q LitTrueV  wp E (Le (LitNat n1) (LitNat n2)) Q.
Ralf Jung's avatar
Ralf Jung committed
239
240
241
242
243
244
245
246
247
248
249
250
251
Proof.
  intros Hle. etransitivity; last eapply wp_lift_pure_step with
    (φ := λ e', e' = LitTrue); last first.
  - intros ? ? ? ? Hstep. inversion_clear Hstep; first done.
    exfalso. eapply le_not_gt with (n := n1); eassumption.
  - intros ?. do 3 eexists. econstructor; done.
  - reflexivity.
  - apply later_mono, forall_intro=>e2. apply impl_intro_l.
    apply const_elim_l=>->.
    rewrite -wp_value'; last reflexivity; done.
Qed.

Lemma wp_le_false n1 n2 E Q :
Ralf Jung's avatar
Ralf Jung committed
252
  n1 > n2 
253
  Q LitFalseV  wp E (Le (LitNat n1) (LitNat n2)) Q.
Ralf Jung's avatar
Ralf Jung committed
254
255
256
257
Proof.
  intros Hle. etransitivity; last eapply wp_lift_pure_step with
    (φ := λ e', e' = LitFalse); last first.
  - intros ? ? ? ? Hstep. inversion_clear Hstep; last done.
Ralf Jung's avatar
Ralf Jung committed
258
259
    exfalso. eapply le_not_gt with (n := n1); eassumption.
  - intros ?. do 3 eexists. econstructor; done.
Ralf Jung's avatar
Ralf Jung committed
260
261
262
  - reflexivity.
  - apply later_mono, forall_intro=>e2. apply impl_intro_l.
    apply const_elim_l=>->.
263
264
    rewrite -wp_value'; last reflexivity; done.
Qed.
Ralf Jung's avatar
Ralf Jung committed
265
266
267

Lemma wp_fst e1 v1 e2 v2 E Q :
  e2v e1 = Some v1  e2v e2 = Some v2 
268
  Q v1  wp E (Fst (Pair e1 e2)) Q.
Ralf Jung's avatar
Ralf Jung committed
269
270
271
272
273
274
275
276
277
278
279
280
281
Proof.
  intros Hv1 Hv2. etransitivity; last eapply wp_lift_pure_step with
    (φ := λ e', e' = e1); last first.
  - intros ? ? ? ? Hstep. inversion_clear Hstep. done.
  - intros ?. do 3 eexists. econstructor; eassumption.
  - reflexivity.
  - apply later_mono, forall_intro=>e2'. apply impl_intro_l.
    apply const_elim_l=>->.
    rewrite -wp_value'; last eassumption; done.
Qed.

Lemma wp_snd e1 v1 e2 v2 E Q :
  e2v e1 = Some v1  e2v e2 = Some v2 
282
  Q v2  wp E (Snd (Pair e1 e2)) Q.
Ralf Jung's avatar
Ralf Jung committed
283
284
285
286
287
288
289
290
291
292
293
294
295
Proof.
  intros Hv1 Hv2. etransitivity; last eapply wp_lift_pure_step with
    (φ := λ e', e' = e2); last first.
  - intros ? ? ? ? Hstep. inversion_clear Hstep; done.
  - intros ?. do 3 eexists. econstructor; eassumption.
  - reflexivity.
  - apply later_mono, forall_intro=>e2'. apply impl_intro_l.
    apply const_elim_l=>->.
    rewrite -wp_value'; last eassumption; done.
Qed.

Lemma wp_case_inl e0 v0 e1 e2 E Q :
  e2v e0 = Some v0 
296
  wp E e1.[e0/] Q  wp E (Case (InjL e0) e1 e2) Q.
Ralf Jung's avatar
Ralf Jung committed
297
298
299
300
301
302
303
304
305
306
307
308
Proof.
  intros Hv0. etransitivity; last eapply wp_lift_pure_step with
    (φ := λ e', e' = e1.[e0/]); last first.
  - intros ? ? ? ? Hstep. inversion_clear Hstep; done.
  - intros ?. do 3 eexists. econstructor; eassumption.
  - reflexivity.
  - apply later_mono, forall_intro=>e1'. apply impl_intro_l.
    by apply const_elim_l=>->.
Qed.

Lemma wp_case_inr e0 v0 e1 e2 E Q :
  e2v e0 = Some v0 
309
  wp E e2.[e0/] Q  wp E (Case (InjR e0) e1 e2) Q.
Ralf Jung's avatar
Ralf Jung committed
310
311
312
313
314
315
316
317
318
Proof.
  intros Hv0. etransitivity; last eapply wp_lift_pure_step with
    (φ := λ e', e' = e2.[e0/]); last first.
  - intros ? ? ? ? Hstep. inversion_clear Hstep; done.
  - intros ?. do 3 eexists. econstructor; eassumption.
  - reflexivity.
  - apply later_mono, forall_intro=>e2'. apply impl_intro_l.
    by apply const_elim_l=>->.
Qed.
319

Ralf Jung's avatar
Ralf Jung committed
320
(** Some derived stateless axioms *)
321

Ralf Jung's avatar
Ralf Jung committed
322
323
324
Lemma wp_le n1 n2 E P Q :
  (n1  n2  P  Q LitTrueV) 
  (n1 > n2  P  Q LitFalseV) 
325
  P  wp E (Le (LitNat n1) (LitNat n2)) Q.
Ralf Jung's avatar
Ralf Jung committed
326
327
328
329
330
331
332
Proof.
  intros HPle HPgt.
  assert (Decision (n1  n2)) as Hn12 by apply _.
  destruct Hn12 as [Hle|Hgt].
  - rewrite -wp_le_true; auto.
  - assert (n1 > n2) by omega. rewrite -wp_le_false; auto.
Qed.
333
End lifting.