lifting.v 13.1 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.

Ralf Jung's avatar
Ralf Jung committed
5
6
7
8
(* TODO RJ: Figure out a way to to always use our Σ. *)

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

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

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) 
  pvs E2 E1 (ownP (Σ:=Σ) σ1    e2 σ2, ( φ e2 σ2  ownP (Σ:=Σ) σ2) -
    pvs E1 E2 (wp (Σ:=Σ) E2 e2 Q))
   wp (Σ:=Σ) E2 e1 Q.
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
69
70
    rewrite (forall_elim _ l). eapply const_intro_l; first eexact Hl.
    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
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208

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) 
  (  e2,  φ e2  wp (Σ:=Σ) E e2 Q)  wp (Σ:=Σ) E e1 Q.
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
212
Lemma wp_rec E ef e v Q :
  e2v e = Some v 
  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.

223
224
225
Lemma wp_lam E ef e v Q :
  e2v e = Some v 
  wp (Σ:=Σ) E ef.[e/] Q  wp (Σ:=Σ) E (App (Lam ef) e) Q.
226
Proof.
227
  intros Hv. rewrite -wp_rec; last eassumption.
228
229
230
231
232
  (* RJ: This pulls in functional extensionality. If that bothers us, we have
     to talk to the Autosubst guys. *)
  by asimpl.
Qed.

Ralf Jung's avatar
Ralf Jung committed
233
234
Lemma wp_plus n1 n2 E Q :
  Q (LitNatV (n1 + n2))  wp (Σ:=Σ) E (Plus (LitNat n1) (LitNat n2)) Q.
235
236
237
238
239
240
241
242
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
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
    rewrite -wp_value'; last reflexivity; done.
Qed.

Lemma wp_le_true n1 n2 E Q :
  n1  n2 
  Q LitTrueV  wp (Σ:=Σ) E (Le (LitNat n1) (LitNat n2)) Q.
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 :
262
  ~(n1  n2) 
Ralf Jung's avatar
Ralf Jung committed
263
264
265
266
267
  Q LitFalseV  wp (Σ:=Σ) E (Le (LitNat n1) (LitNat n2)) Q.
Proof.
  intros Hle. etransitivity; last eapply wp_lift_pure_step with
    (φ := λ e', e' = LitFalse); last first.
  - intros ? ? ? ? Hstep. inversion_clear Hstep; last done.
268
269
    exfalso. omega.
  - intros ?. do 3 eexists. econstructor; omega.
Ralf Jung's avatar
Ralf Jung committed
270
271
272
  - reflexivity.
  - apply later_mono, forall_intro=>e2. apply impl_intro_l.
    apply const_elim_l=>->.
273
274
    rewrite -wp_value'; last reflexivity; done.
Qed.
Ralf Jung's avatar
Ralf Jung committed
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305

Lemma wp_fst e1 v1 e2 v2 E Q :
  e2v e1 = Some v1  e2v e2 = Some v2 
  Q v1  wp (Σ:=Σ) E (Fst (Pair e1 e2)) Q.
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 
  Q v2  wp (Σ:=Σ) E (Snd (Pair e1 e2)) Q.
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 
306
  wp (Σ:=Σ) E e1.[e0/] Q  wp (Σ:=Σ) E (Case (InjL e0) e1 e2) Q.
Ralf Jung's avatar
Ralf Jung committed
307
308
309
310
311
312
313
314
315
316
317
318
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 
319
  wp (Σ:=Σ) E e2.[e0/] Q  wp (Σ:=Σ) E (Case (InjR e0) e1 e2) Q.
Ralf Jung's avatar
Ralf Jung committed
320
321
322
323
324
325
326
327
328
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.
329
330
331
332
333
334
335
336
337

(** Some stateless axioms that incorporate bind *)

Lemma wp_let e1 e2 E Q :
  wp (Σ:=Σ) E e1 (λ v, wp (Σ:=Σ) E (e2.[v2e v/]) Q)  wp (Σ:=Σ) E (Let e1 e2) Q.
Proof.
  rewrite -(wp_bind _ _ (LetCtx EmptyCtx e2)). apply wp_mono=>v.
  rewrite -wp_lam //. by rewrite v2v.
Qed.