lifting.v 8.45 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
Require Import prelude.gmap program_logic.lifting program_logic.ownership.
2
Require Export program_logic.weakestpre heap_lang.heap_lang_tactics.
3
Import uPred heap_lang.
4
Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
5

6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
(** The substitution operation [gsubst e x ev] behaves just as [subst] but
in case [e] does not contain the free variable [x] it will return [e] in a
way that is syntactically equal (i.e. without any Coq-level delta reduction
performed) *)
Definition gsubst_lift {A B C} (f : A  B  C)
    (x : A) (y : B) (mx : option A) (my : option B) : option C :=
  match mx, my with
  | Some x, Some y => Some (f x y)
  | Some x, None => Some (f x y)
  | None, Some y => Some (f x y)
  | None, None => None
  end.
Fixpoint gsubst_go (e : expr) (x : string) (ev : expr) : option expr :=
  match e with
  | Var y => if decide (x = y  x  "") then Some ev else None
  | Rec f y e =>
     if decide (x  f  x  y) then Rec f y <$> gsubst_go e x ev else None
  | App e1 e2 => gsubst_lift App e1 e2 (gsubst_go e1 x ev) (gsubst_go e2 x ev)
  | Lit l => None
  | UnOp op e => UnOp op <$> gsubst_go e x ev
  | BinOp op e1 e2 =>
     gsubst_lift (BinOp op) e1 e2 (gsubst_go e1 x ev) (gsubst_go e2 x ev)
  | If e0 e1 e2 =>
     gsubst_lift id (If e0 e1) e2
       (gsubst_lift If e0 e1 (gsubst_go e0 x ev) (gsubst_go e1 x ev))
       (gsubst_go e2 x ev)
  | Pair e1 e2 => gsubst_lift Pair e1 e2 (gsubst_go e1 x ev) (gsubst_go e2 x ev)
  | Fst e => Fst <$> gsubst_go e x ev
  | Snd e => Snd <$> gsubst_go e x ev
  | InjL e => InjL <$> gsubst_go e x ev
  | InjR e => InjR <$> gsubst_go e x ev
  | Case e0 x1 e1 x2 e2 =>
     gsubst_lift id (Case e0 x1 e1 x2) e2
       (gsubst_lift (λ e0' e1', Case e0' x1 e1' x2) e0 e1
         (gsubst_go e0 x ev)
         (if decide (x  x1) then gsubst_go e1 x ev else None))
       (if decide (x  x2) then gsubst_go e2 x ev else None)
  | Fork e => Fork <$> gsubst_go e x ev
  | Loc l => None
  | Alloc e => Alloc <$> gsubst_go e x ev
  | Load e => Load <$> gsubst_go e x ev
  | Store e1 e2 => gsubst_lift Store e1 e2 (gsubst_go e1 x ev) (gsubst_go e2 x ev)
  | Cas e0 e1 e2 =>
     gsubst_lift id (Cas e0 e1) e2
       (gsubst_lift Cas e0 e1 (gsubst_go e0 x ev) (gsubst_go e1 x ev))
       (gsubst_go e2 x ev)
  end.
Definition gsubst (e : expr) (x : string) (ev : expr) : expr :=
  from_option e (gsubst_go e x ev).
Arguments gsubst !_ _ _/.

57
Section lifting.
58
59
Context {Σ : iFunctor}.
Implicit Types P : iProp heap_lang Σ.
60
61
Implicit Types Q : val  iProp heap_lang Σ.
Implicit Types K : ectx.
62
Implicit Types ef : option expr.
Ralf Jung's avatar
Ralf Jung committed
63

64
65
66
67
68
69
70
71
72
73
74
75
76
77
Lemma gsubst_None e x v : gsubst_go e x (of_val v) = None  e = subst e x v.
Proof.
  induction e; simpl; unfold gsubst_lift; intros;
    repeat (simplify_option_equality || case_match); f_equal; auto.
Qed.
Lemma gsubst_correct e x v : gsubst e x (of_val v) = subst e x v.
Proof.
  unfold gsubst; destruct (gsubst_go e x (of_val v)) as [e'|] eqn:He; simpl;
    last by apply gsubst_None.
  revert e' He; induction e; simpl; unfold gsubst_lift; intros;
    repeat (simplify_option_equality || case_match);
    f_equal; auto using gsubst_None.
Qed.

Ralf Jung's avatar
Ralf Jung committed
78
(** Bind. *)
79
Lemma wp_bind {E e} K Q :
80
  wp E e (λ v, wp E (fill K (of_val v)) Q)  wp E (fill K e) Q.
81
82
83
84
85
Proof. apply weakestpre.wp_bind. Qed.

Lemma wp_bindi {E e} Ki Q :
  wp E e (λ v, wp E (fill_item Ki (of_val v)) Q)  wp E (fill_item Ki e) Q.
Proof. apply weakestpre.wp_bind. Qed.
Ralf Jung's avatar
Ralf Jung committed
86

87
(** Base axioms for core primitives of the language: Stateful reductions. *)
88
Lemma wp_alloc_pst E σ e v Q :
89
  to_val e = Some v 
90
  (ownP σ   ( l, σ !! l = None  ownP (<[l:=v]>σ) - Q (LocV l)))
91
        wp E (Alloc e) Q.
92
Proof.
93
  (* TODO RJ: This works around ssreflect bug #22. *)
94
95
  intros. set (φ v' σ' ef :=  l,
    ef = None  v' = LocV l  σ' = <[l:=v]>σ  σ !! l = None).
96
  rewrite -(wp_lift_atomic_step (Alloc e) φ σ) // /φ;
Ralf Jung's avatar
Ralf Jung committed
97
    last by intros; inv_step; eauto 8.
98
  apply sep_mono, later_mono; first done.
99
100
  apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.
  apply wand_intro_l.
101
  rewrite always_and_sep_l' -associative -always_and_sep_l'.
102
103
  apply const_elim_l=>-[l [-> [-> [-> ?]]]].
  by rewrite (forall_elim l) right_id const_equiv // left_id wand_elim_r.
104
Qed.
105

106
Lemma wp_load_pst E σ l v Q :
Ralf Jung's avatar
Ralf Jung committed
107
  σ !! l = Some v 
108
  (ownP σ   (ownP σ - Q v))  wp E (Load (Loc l)) Q.
Ralf Jung's avatar
Ralf Jung committed
109
Proof.
110
111
  intros. rewrite -(wp_lift_atomic_det_step σ v σ None) ?right_id //;
    last by intros; inv_step; eauto using to_of_val.
Ralf Jung's avatar
Ralf Jung committed
112
Qed.
113

114
Lemma wp_store_pst E σ l e v v' Q :
115
  to_val e = Some v  σ !! l = Some v' 
116
  (ownP σ   (ownP (<[l:=v]>σ) - Q (LitV LitUnit)))  wp E (Store (Loc l) e) Q.
Ralf Jung's avatar
Ralf Jung committed
117
Proof.
118
  intros. rewrite -(wp_lift_atomic_det_step σ (LitV LitUnit) (<[l:=v]>σ) None)
119
    ?right_id //; last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
120
Qed.
121

122
Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Q :
123
  to_val e1 = Some v1  to_val e2 = Some v2  σ !! l = Some v'  v'  v1 
Ralf Jung's avatar
Ralf Jung committed
124
  (ownP σ   (ownP σ - Q (LitV $ LitBool false)))  wp E (Cas (Loc l) e1 e2) Q.
Ralf Jung's avatar
Ralf Jung committed
125
Proof.
Ralf Jung's avatar
Ralf Jung committed
126
  intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool false) σ None)
127
    ?right_id //; last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
128
Qed.
129

130
Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Q :
131
  to_val e1 = Some v1  to_val e2 = Some v2  σ !! l = Some v1 
Ralf Jung's avatar
Ralf Jung committed
132
  (ownP σ   (ownP (<[l:=v2]>σ) - Q (LitV $ LitBool true)))
133
   wp E (Cas (Loc l) e1 e2) Q.
Ralf Jung's avatar
Ralf Jung committed
134
Proof.
Ralf Jung's avatar
Ralf Jung committed
135
  intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool true) (<[l:=v2]>σ) None)
136
    ?right_id //; last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
137
138
Qed.

139
140
(** Base axioms for core primitives of the language: Stateless reductions *)
Lemma wp_fork E e :
141
   wp (Σ:=Σ) coPset_all e (λ _, True)  wp E (Fork e) (λ v, v = LitV LitUnit).
142
Proof.
143
  rewrite -(wp_lift_pure_det_step (Fork e) (Lit LitUnit) (Some e)) //=;
144
    last by intros; inv_step; eauto.
145
  apply later_mono, sep_intro_True_l; last done.
146
  by rewrite -(wp_value' _ _ (Lit _)) //; apply const_intro.
147
Qed.
148

149
150
Lemma wp_rec E f x e1 e2 v Q :
  to_val e2 = Some v 
151
   wp E (gsubst (gsubst e1 f (Rec f x e1)) x e2) Q  wp E (App (Rec f x e1) e2) Q.
152
Proof.
153
154
  intros <-%of_to_val; rewrite gsubst_correct (gsubst_correct _ _ (RecV _ _ _)).
  rewrite -(wp_lift_pure_det_step (App _ _)
155
    (subst (subst e1 f (RecV f x e1)) x v) None) ?right_id //=;
156
    intros; inv_step; eauto.
157
Qed.
158
159
160
161
162
Lemma wp_rec' E e1 f x erec e2 v Q :
  e1 = Rec f x erec 
  to_val e2 = Some v 
   wp E (gsubst (gsubst erec f e1) x e2) Q  wp E (App e1 e2) Q.
Proof. intros ->; apply wp_rec. Qed.
163

164
165
166
Lemma wp_un_op E op l l' Q :
  un_op_eval op l = Some l' 
   Q (LitV l')  wp E (UnOp op (Lit l)) Q.
167
Proof.
168
  intros. rewrite -(wp_lift_pure_det_step (UnOp op _) (Lit l') None)
169
    ?right_id -?wp_value' //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
170
Qed.
171

172
173
174
Lemma wp_bin_op E op l1 l2 l' Q :
  bin_op_eval op l1 l2 = Some l' 
   Q (LitV l')  wp E (BinOp op (Lit l1) (Lit l2)) Q.
Ralf Jung's avatar
Ralf Jung committed
175
Proof.
176
  intros Heval. rewrite -(wp_lift_pure_det_step (BinOp op _ _) (Lit l') None)
177
    ?right_id -?wp_value' //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
178
Qed.
179

Ralf Jung's avatar
Ralf Jung committed
180
Lemma wp_if_true E e1 e2 Q :  wp E e1 Q  wp E (If (Lit $ LitBool true) e1 e2) Q.
Ralf Jung's avatar
Ralf Jung committed
181
Proof.
182
  rewrite -(wp_lift_pure_det_step (If _ _ _) e1 None)
183
    ?right_id //; intros; inv_step; eauto.
184
185
Qed.

Ralf Jung's avatar
Ralf Jung committed
186
Lemma wp_if_false E e1 e2 Q :  wp E e2 Q  wp E (If (Lit $ LitBool false) e1 e2) Q.
187
188
Proof.
  rewrite -(wp_lift_pure_det_step (If _ _ _) e2 None)
189
    ?right_id //; intros; inv_step; eauto.
190
Qed.
191

192
Lemma wp_fst E e1 v1 e2 v2 Q :
193
  to_val e1 = Some v1  to_val e2 = Some v2 
194
   Q v1  wp E (Fst $ Pair e1 e2) Q.
Ralf Jung's avatar
Ralf Jung committed
195
Proof.
196
197
  intros. rewrite -(wp_lift_pure_det_step (Fst _) e1 None)
    ?right_id -?wp_value' //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
198
Qed.
199

200
Lemma wp_snd E e1 v1 e2 v2 Q :
201
  to_val e1 = Some v1  to_val e2 = Some v2 
202
   Q v2  wp E (Snd $ Pair e1 e2) Q.
Ralf Jung's avatar
Ralf Jung committed
203
Proof.
204
205
  intros. rewrite -(wp_lift_pure_det_step (Snd _) e2 None)
    ?right_id -?wp_value' //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
206
Qed.
207

208
Lemma wp_case_inl E e0 v0 x1 e1 x2 e2 Q :
209
  to_val e0 = Some v0 
210
   wp E (gsubst e1 x1 e0) Q  wp E (Case (InjL e0) x1 e1 x2 e2) Q.
Ralf Jung's avatar
Ralf Jung committed
211
Proof.
212
213
214
  intros <-%of_to_val; rewrite gsubst_correct.
  rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _) (subst e1 x1 v0) None)
    ?right_id //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
215
Qed.
216

217
Lemma wp_case_inr E e0 v0 x1 e1 x2 e2 Q :
218
  to_val e0 = Some v0 
219
   wp E (gsubst e2 x2 e0) Q  wp E (Case (InjR e0) x1 e1 x2 e2) Q.
Ralf Jung's avatar
Ralf Jung committed
220
Proof.
221
222
223
  intros <-%of_to_val; rewrite gsubst_correct.
  rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _) (subst e2 x2 v0) None)
    ?right_id //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
224
Qed.
225

226
End lifting.