lifting.v 12.2 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:
49
50
  e2v e = Some v 
  ownP (Σ:=Σ) σ  wp (Σ:=Σ) E (Alloc e)
51
52
       (λ v',  l, (v' = LocV l  σ !! l = None)  ownP (Σ:=Σ) (<[l:=v]>σ)).
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
65
66
67
  - reflexivity.
  - reflexivity.
  - (* RJ FIXME I am sure there is a better way to invoke right_id, but I could not find it. *)
    rewrite -pvs_intro. rewrite -{1}[ownP σ](@right_id _ _ _ _ uPred.sep_True).
    apply sep_mono; first done. rewrite -later_intro.
68
    apply forall_intro=>e2. apply forall_intro=>σ2.
69
    apply wand_intro_l. rewrite right_id. rewrite -pvs_intro.
70
    apply const_elim_l. intros [l [-> [-> Hl]]].
71
72
73
74
    rewrite -wp_value'; last reflexivity.
    erewrite <-exist_intro with (a := l). apply and_intro.
    + by apply const_intro.
    + done.
75
Qed.
Ralf Jung's avatar
Ralf Jung committed
76

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

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

Ralf Jung's avatar
Ralf Jung committed
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' :
  e2v e1 = Some v1  e2v e2 = Some v2 
  σ !! l = Some v'  v' <> v1 
  ownP (Σ:=Σ) σ  wp (Σ:=Σ) E (Cas (Loc l) e1 e2)
       (λ v', (v' = LitFalseV)  ownP (Σ:=Σ) σ).
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.
  - rewrite -pvs_intro. rewrite -{1}[ownP σ](@right_id _ _ _ _ uPred.sep_True).
    apply sep_mono; first done. rewrite -later_intro.
    apply forall_intro=>e2'. apply forall_intro=>σ2'.
    apply wand_intro_l. rewrite right_id. rewrite -pvs_intro.
    apply const_elim_l. intros [-> ->].
    rewrite -wp_value'; last reflexivity. apply and_intro.
    + by apply const_intro.
    + done.
Qed.

Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 :
  e2v e1 = Some v1  e2v e2 = Some v2 
  σ !! l = Some v1 
  ownP (Σ:=Σ) σ  wp (Σ:=Σ) E (Cas (Loc l) e1 e2)
       (λ v', (v' = LitTrueV)  ownP (Σ:=Σ) (<[l:=v2]>σ)).
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.
  - rewrite -pvs_intro. rewrite -{1}[ownP σ](@right_id _ _ _ _ uPred.sep_True).
    apply sep_mono; first done. rewrite -later_intro.
    apply forall_intro=>e2'. apply forall_intro=>σ2'.
    apply wand_intro_l. rewrite right_id. rewrite -pvs_intro.
    apply const_elim_l. intros [-> ->].
    rewrite -wp_value'; last reflexivity. apply and_intro.
    + by apply const_intro.
    + done.
Qed.

173
174
175
(** Base axioms for core primitives of the language: Stateless reductions *)

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

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

Ralf Jung's avatar
Ralf Jung committed
221
222
Lemma wp_rec' E e v Q :
  wp (Σ:=Σ) E (e.[Rec e, v2e v /]) Q  wp (Σ:=Σ) E (App (Rec e) (v2e v)) Q.
223
224
225
226
227
228
229
230
231
232
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
233
234
Lemma wp_lam E e v Q :
  wp (Σ:=Σ) E (e.[v2e v/]) Q  wp (Σ:=Σ) E (App (Lam e) (v2e v)) Q.
235
Proof.
Ralf Jung's avatar
Ralf Jung committed
236
  rewrite -wp_rec'.
237
238
239
240
241
  (* 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
242
243
Lemma wp_plus n1 n2 E Q :
  Q (LitNatV (n1 + n2))  wp (Σ:=Σ) E (Plus (LitNat n1) (LitNat n2)) Q.
244
245
246
247
248
249
250
251
252
253
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=>->.
    rewrite -wp_value'; last reflexivity; done.
Qed.
Ralf Jung's avatar
Ralf Jung committed
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
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

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.