lifting.v 8.05 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
121
122
123

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

Lemma wp_fork E e :
124
   wp (Σ:=Σ) coPset_all e (λ _, True)  wp (Σ:=Σ) E (Fork e) (λ v, (v = LitUnitV)).
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
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.
143
144
    rewrite -wp_value'; last reflexivity.
    by apply const_intro.
145
Qed.
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167

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

Ralf Jung's avatar
Ralf Jung committed
169
170
Lemma wp_rec' E e v Q :
  wp (Σ:=Σ) E (e.[Rec e, v2e v /]) Q  wp (Σ:=Σ) E (App (Rec e) (v2e v)) Q.
171
172
173
174
175
176
177
178
179
180
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
181
182
Lemma wp_lam E e v Q :
  wp (Σ:=Σ) E (e.[v2e v/]) Q  wp (Σ:=Σ) E (App (Lam e) (v2e v)) Q.
183
Proof.
Ralf Jung's avatar
Ralf Jung committed
184
  rewrite -wp_rec'.
185
186
187
188
189
  (* 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
190
191
Lemma wp_plus n1 n2 E Q :
  Q (LitNatV (n1 + n2))  wp (Σ:=Σ) E (Plus (LitNat n1) (LitNat n2)) Q.
192
193
194
195
196
197
198
199
200
201
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.