lifting.v 12.9 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
15
16
(** Base axioms for core primitives of the language: Stateful reductions.
    These are the lemmas basd on the physical state; we will derive versions
    based on a ghost "mapsto"-predicate later. *)
17
18
19
20
21
22
23
24
25
26

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.
27
  (* RJ: working around https://coq.inria.fr/bugs/show_bug.cgi?id=4536 *)
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
  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.
45
46
47

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

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

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

116
Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Q :
Ralf Jung's avatar
Ralf Jung committed
117
118
  e2v e1 = Some v1  e2v e2 = Some v2 
  σ !! l = Some v'  v' <> v1 
119
  (ownP (Σ:=Σ) σ  (ownP σ - Q LitFalseV))  wp (Σ:=Σ) E (Cas (Loc l) e1 e2) Q.
Ralf Jung's avatar
Ralf Jung committed
120
121
122
123
124
125
126
127
128
129
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.
130
131
  - rewrite -pvs_intro.
    apply sep_mono; first done. apply later_mono.
Ralf Jung's avatar
Ralf Jung committed
132
    apply forall_intro=>e2'. apply forall_intro=>σ2'.
133
134
    apply wand_intro_l. rewrite -pvs_intro.
    rewrite always_and_sep_l' -associative -always_and_sep_l'.
Ralf Jung's avatar
Ralf Jung committed
135
    apply const_elim_l. intros [-> ->].
136
    by rewrite wand_elim_r -wp_value'.
Ralf Jung's avatar
Ralf Jung committed
137
138
Qed.

139
Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Q :
Ralf Jung's avatar
Ralf Jung committed
140
141
  e2v e1 = Some v1  e2v e2 = Some v2 
  σ !! l = Some v1 
142
  (ownP (Σ:=Σ) σ  (ownP (<[l:=v2]>σ) - Q LitTrueV))  wp (Σ:=Σ) E (Cas (Loc l) e1 e2) Q.
Ralf Jung's avatar
Ralf Jung committed
143
144
145
146
147
148
149
150
151
152
153
154
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.
155
156
  - rewrite -pvs_intro.
    apply sep_mono; first done. apply later_mono.
Ralf Jung's avatar
Ralf Jung committed
157
    apply forall_intro=>e2'. apply forall_intro=>σ2'.
158
159
    apply wand_intro_l. rewrite -pvs_intro.
    rewrite always_and_sep_l' -associative -always_and_sep_l'.
Ralf Jung's avatar
Ralf Jung committed
160
    apply const_elim_l. intros [-> ->].
161
    by rewrite wand_elim_r -wp_value'.
Ralf Jung's avatar
Ralf Jung committed
162
163
Qed.

164
165
166
(** Base axioms for core primitives of the language: Stateless reductions *)

Lemma wp_fork E e :
167
   wp (Σ:=Σ) coPset_all e (λ _, True)  wp (Σ:=Σ) E (Fork e) (λ v, (v = LitUnitV)).
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
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.
186
187
    rewrite -wp_value'; last reflexivity.
    by apply const_intro.
188
Qed.
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210

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.
211

212
Lemma wp_rec E e v Q :
Ralf Jung's avatar
Ralf Jung committed
213
  wp (Σ:=Σ) E (e.[Rec e, v2e v /]) Q  wp (Σ:=Σ) E (App (Rec e) (v2e v)) Q.
214
215
216
217
218
219
220
221
222
223
Proof.
  etransitivity; last eapply wp_lift_pure_step with
    (φ := λ e', e' = e.[Rec e, v2e v /]); last first.
  - intros ? ? ? ? Hstep. inversion_clear Hstep. done.
  - intros ?. do 3 eexists. eapply BetaS. by rewrite v2v.
  - reflexivity.
  - apply later_mono, forall_intro=>e2. apply impl_intro_l.
    apply const_elim_l=>->. done.
Qed.

Ralf Jung's avatar
Ralf Jung committed
224
225
Lemma wp_lam E e v Q :
  wp (Σ:=Σ) E (e.[v2e v/]) Q  wp (Σ:=Σ) E (App (Lam e) (v2e v)) Q.
226
Proof.
227
  rewrite -wp_rec.
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
262
263
264
265
266
267
268
269
270
271
272
    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 :
  n1 > n2 
  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.
    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=>->.
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
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328

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 
  wp (Σ:=Σ) E (e1.[e0/]) Q  wp (Σ:=Σ) E (Case (InjL e0) e1 e2) Q.
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 
  wp (Σ:=Σ) E (e2.[e0/]) Q  wp (Σ:=Σ) E (Case (InjR e0) e1 e2) Q.
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.