lang.v 13.5 KB
Newer Older
1
2
3
From program_logic Require Export language.
From prelude Require Export strings.
From prelude Require Import gmap.
4

5
Module heap_lang.
6
7
Open Scope Z_scope.

8
(** Expressions and vals. *)
9
Definition loc := positive. (* Really, any countable type. *)
Ralf Jung's avatar
Ralf Jung committed
10

11
Inductive base_lit : Set :=
12
  | LitInt (n : Z) | LitBool (b : bool) | LitUnit.
13
Inductive un_op : Set :=
14
  | NegOp | MinusUnOp.
15
16
17
Inductive bin_op : Set :=
  | PlusOp | MinusOp | LeOp | LtOp | EqOp.

18
19
Inductive binder := BAnon | BNamed : string  binder.

20
Delimit Scope binder_scope with binder.
21
Bind Scope binder_scope with binder.
22

Ralf Jung's avatar
Ralf Jung committed
23
Inductive expr :=
24
  (* Base lambda calculus *)
25
  | Var (x : string)
26
  | Rec (f x : binder) (e : expr)
27
  | App (e1 e2 : expr)
28
29
30
31
32
  (* Base types and their operations *)
  | Lit (l : base_lit)
  | UnOp (op : un_op) (e : expr)
  | BinOp (op : bin_op) (e1 e2 : expr)
  | If (e0 e1 e2 : expr)
33
34
35
36
37
38
39
  (* Products *)
  | Pair (e1 e2 : expr)
  | Fst (e : expr)
  | Snd (e : expr)
  (* Sums *)
  | InjL (e : expr)
  | InjR (e : expr)
40
  | Case (e0 : expr) (e1 : expr) (e2 : expr)
41
42
43
44
45
46
47
48
  (* Concurrency *)
  | Fork (e : expr)
  (* Heap *)
  | Loc (l : loc)
  | Alloc (e : expr)
  | Load (e : expr)
  | Store (e1 : expr) (e2 : expr)
  | Cas (e0 : expr) (e1 : expr) (e2 : expr).
Ralf Jung's avatar
Ralf Jung committed
49

50
51
52
Bind Scope expr_scope with expr.
Delimit Scope expr_scope with E.

53
Inductive val :=
54
  | RecV (f x : binder) (e : expr) (* e should be closed *)
55
  | LitV (l : base_lit)
56
57
58
59
  | PairV (v1 v2 : val)
  | InjLV (v : val)
  | InjRV (v : val)
  | LocV (l : loc).
Ralf Jung's avatar
Ralf Jung committed
60

61
62
Bind Scope val_scope with val.
Delimit Scope val_scope with V.
63

64
Global Instance base_lit_dec_eq (l1 l2 : base_lit) : Decision (l1 = l2).
65
Proof. solve_decision. Defined.
66
Global Instance un_op_dec_eq (op1 op2 : un_op) : Decision (op1 = op2).
67
Proof. solve_decision. Defined.
68
Global Instance bin_op_dec_eq (op1 op2 : bin_op) : Decision (op1 = op2).
69
Proof. solve_decision. Defined.
70
71
Global Instance binder_dec_eq (x1 x2 : binder) : Decision (x1 = x2).
Proof. solve_decision. Defined.
72
Global Instance expr_dec_eq (e1 e2 : expr) : Decision (e1 = e2).
73
Proof. solve_decision. Defined.
74
Global Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2).
75
Proof. solve_decision. Defined.
76

77
Fixpoint of_val (v : val) : expr :=
Ralf Jung's avatar
Ralf Jung committed
78
  match v with
79
  | RecV f x e => Rec f x e
80
  | LitV l => Lit l
81
82
83
  | PairV v1 v2 => Pair (of_val v1) (of_val v2)
  | InjLV v => InjL (of_val v)
  | InjRV v => InjR (of_val v)
84
  | LocV l => Loc l
Ralf Jung's avatar
Ralf Jung committed
85
  end.
86
Fixpoint to_val (e : expr) : option val :=
87
  match e with
88
  | Rec f x e => Some (RecV f x e)
89
  | Lit l => Some (LitV l)
90
91
92
  | Pair e1 e2 => v1  to_val e1; v2  to_val e2; Some (PairV v1 v2)
  | InjL e => InjLV <$> to_val e
  | InjR e => InjRV <$> to_val e
93
  | Loc l => Some (LocV l)
Ralf Jung's avatar
Ralf Jung committed
94
  | _ => None
95
96
  end.

97
98
(** The state: heaps of vals. *)
Definition state := gmap loc val.
Ralf Jung's avatar
Ralf Jung committed
99

100
(** Evaluation contexts *)
101
102
103
Inductive ectx_item :=
  | AppLCtx (e2 : expr)
  | AppRCtx (v1 : val)
104
105
106
107
  | UnOpCtx (op : un_op)
  | BinOpLCtx (op : bin_op) (e2 : expr)
  | BinOpRCtx (op : bin_op) (v1 : val)
  | IfCtx (e1 e2 : expr)
108
109
110
111
112
113
  | PairLCtx (e2 : expr)
  | PairRCtx (v1 : val)
  | FstCtx
  | SndCtx
  | InjLCtx
  | InjRCtx
114
  | CaseCtx (e1 : expr) (e2 : expr)
115
116
117
118
119
120
121
  | AllocCtx
  | LoadCtx
  | StoreLCtx (e2 : expr)
  | StoreRCtx (v1 : val)
  | CasLCtx (e1 : expr)  (e2 : expr)
  | CasMCtx (v0 : val) (e2 : expr)
  | CasRCtx (v0 : val) (v1 : val).
122

123
Notation ectx := (list ectx_item).
124

125
Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
126
127
128
  match Ki with
  | AppLCtx e2 => App e e2
  | AppRCtx v1 => App (of_val v1) e
129
130
131
132
  | UnOpCtx op => UnOp op e
  | BinOpLCtx op e2 => BinOp op e e2
  | BinOpRCtx op v1 => BinOp op (of_val v1) e
  | IfCtx e1 e2 => If e e1 e2
133
134
135
136
137
138
  | PairLCtx e2 => Pair e e2
  | PairRCtx v1 => Pair (of_val v1) e
  | FstCtx => Fst e
  | SndCtx => Snd e
  | InjLCtx => InjL e
  | InjRCtx => InjR e
139
  | CaseCtx e1 e2 => Case e e1 e2
140
141
142
143
144
145
146
  | AllocCtx => Alloc e
  | LoadCtx => Load e
  | StoreLCtx e2 => Store e e2
  | StoreRCtx v1 => Store (of_val v1) e
  | CasLCtx e1 e2 => Cas e e1 e2
  | CasMCtx v0 e2 => Cas (of_val v0) e e2
  | CasRCtx v0 v1 => Cas (of_val v0) (of_val v1) e
Ralf Jung's avatar
Ralf Jung committed
147
  end.
148
Definition fill (K : ectx) (e : expr) : expr := fold_right fill_item e K.
Ralf Jung's avatar
Ralf Jung committed
149

150
(** Substitution *)
151
(** We have [subst' e BAnon v = e] to deal with anonymous binders *)
152
153
Fixpoint subst (e : expr) (x : string) (v : val) : expr :=
  match e with
154
155
156
  | Var y => if decide (x = y) then of_val v else Var y
  | Rec f y e =>
     Rec f y (if decide (BNamed x  f  BNamed x  y) then subst e x v else e)
157
158
159
160
161
162
163
164
165
166
  | App e1 e2 => App (subst e1 x v) (subst e2 x v)
  | Lit l => Lit l
  | UnOp op e => UnOp op (subst e x v)
  | BinOp op e1 e2 => BinOp op (subst e1 x v) (subst e2 x v)
  | If e0 e1 e2 => If (subst e0 x v) (subst e1 x v) (subst e2 x v)
  | Pair e1 e2 => Pair (subst e1 x v) (subst e2 x v)
  | Fst e => Fst (subst e x v)
  | Snd e => Snd (subst e x v)
  | InjL e => InjL (subst e x v)
  | InjR e => InjR (subst e x v)
167
168
  | Case e0 e1 e2 =>
     Case (subst e0 x v) (subst e1 x v) (subst e2 x v)
169
170
171
172
173
174
175
  | Fork e => Fork (subst e x v)
  | Loc l => Loc l
  | Alloc e => Alloc (subst e x v)
  | Load e => Load (subst e x v)
  | Store e1 e2 => Store (subst e1 x v) (subst e2 x v)
  | Cas e0 e1 e2 => Cas (subst e0 x v) (subst e1 x v) (subst e2 x v)
  end.
176
Definition subst' (e : expr) (mx : binder) (v : val) : expr :=
177
  match mx with BNamed x => subst e x v | BAnon => e end.
178

179
(** The stepping relation *)
180
181
Definition un_op_eval (op : un_op) (l : base_lit) : option base_lit :=
  match op, l with
182
  | NegOp, LitBool b => Some (LitBool (negb b))
183
  | MinusUnOp, LitInt n => Some (LitInt (- n))
184
185
186
187
188
  | _, _ => None
  end.

Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
  match op, l1, l2 with
189
190
191
192
193
  | PlusOp, LitInt n1, LitInt n2 => Some $ LitInt (n1 + n2)
  | MinusOp, LitInt n1, LitInt n2 => Some $ LitInt (n1 - n2)
  | LeOp, LitInt n1, LitInt n2 => Some $ LitBool $ bool_decide (n1  n2)
  | LtOp, LitInt n1, LitInt n2 => Some $ LitBool $ bool_decide (n1 < n2)
  | EqOp, LitInt n1, LitInt n2 => Some $ LitBool $ bool_decide (n1 = n2)
194
195
196
  | _, _, _ => None
  end.

197
Inductive head_step : expr  state  expr  state  option expr  Prop :=
198
  | BetaS f x e1 e2 v2 σ :
199
     to_val e2 = Some v2 
200
     head_step (App (Rec f x e1) e2) σ
201
       (subst' (subst' e1 f (RecV f x e1)) x v2) σ None
202
  | UnOpS op l l' σ :
203
204
     un_op_eval op l = Some l'  
     head_step (UnOp op (Lit l)) σ (Lit l') σ None
205
  | BinOpS op l1 l2 l' σ :
206
207
208
     bin_op_eval op l1 l2 = Some l'  
     head_step (BinOp op (Lit l1) (Lit l2)) σ (Lit l') σ None
  | IfTrueS e1 e2 σ :
Ralf Jung's avatar
Ralf Jung committed
209
     head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ None
210
  | IfFalseS e1 e2 σ :
Ralf Jung's avatar
Ralf Jung committed
211
     head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ None
212
213
214
215
216
217
  | FstS e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     head_step (Fst (Pair e1 e2)) σ e1 σ None
  | SndS e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     head_step (Snd (Pair e1 e2)) σ e2 σ None
218
  | CaseLS e0 v0 e1 e2 σ :
219
     to_val e0 = Some v0 
220
221
     head_step (Case (InjL e0) e1 e2) σ (App e1 e0) σ None
  | CaseRS e0 v0 e1 e2 σ :
222
     to_val e0 = Some v0 
223
     head_step (Case (InjR e0) e1 e2) σ (App e2 e0) σ None
224
  | ForkS e σ:
225
     head_step (Fork e) σ (Lit LitUnit) σ (Some e)
226
227
228
229
230
231
232
233
  | AllocS e v σ l :
     to_val e = Some v  σ !! l = None 
     head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None
  | LoadS l v σ :
     σ !! l = Some v 
     head_step (Load (Loc l)) σ (of_val v) σ None
  | StoreS l e v σ :
     to_val e = Some v  is_Some (σ !! l) 
234
     head_step (Store (Loc l) e) σ (Lit LitUnit) (<[l:=v]>σ) None
235
236
237
  | CasFailS l e1 v1 e2 v2 vl σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some vl  vl  v1 
Ralf Jung's avatar
Ralf Jung committed
238
     head_step (Cas (Loc l) e1 e2) σ (Lit $ LitBool false) σ None
239
240
241
  | CasSucS l e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some v1 
Ralf Jung's avatar
Ralf Jung committed
242
     head_step (Cas (Loc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None.
Ralf Jung's avatar
Ralf Jung committed
243

244
(** Atomic expressions *)
245
Definition atomic (e: expr) : Prop :=
246
247
248
249
250
  match e with
  | Alloc e => is_Some (to_val e)
  | Load e => is_Some (to_val e)
  | Store e1 e2 => is_Some (to_val e1)  is_Some (to_val e2)
  | Cas e0 e1 e2 => is_Some (to_val e0)  is_Some (to_val e1)  is_Some (to_val e2)
Ralf Jung's avatar
Ralf Jung committed
251
252
  (* Make "skip" atomic *)
  | App (Rec _ _ (Lit _)) (Lit _) => True
253
254
  | _ => False
  end.
255

256
257
258
259
(** Close reduction under evaluation contexts.
We could potentially make this a generic construction. *)
Inductive prim_step
    (e1 : expr) (σ1 : state) (e2 : expr) (σ2: state) (ef: option expr) : Prop :=
260
  Ectx_step K e1' e2' :
261
262
263
264
265
    e1 = fill K e1'  e2 = fill K e2' 
    head_step e1' σ1 e2' σ2 ef  prim_step e1 σ1 e2 σ2 ef.

(** Basic properties about the language *)
Lemma to_of_val v : to_val (of_val v) = Some v.
266
Proof. by induction v; simplify_option_eq. Qed.
267

268
Lemma of_to_val e v : to_val e = Some v  of_val v = e.
269
Proof.
270
  revert v; induction e; intros; simplify_option_eq; auto with f_equal.
271
Qed.
272

273
274
Instance: Inj (=) (=) of_val.
Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
275

276
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
277
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
278

279
Instance ectx_fill_inj K : Inj (=) (=) (fill K).
280
Proof. red; induction K as [|Ki K IH]; naive_solver. Qed.
281

282
283
Lemma fill_app K1 K2 e : fill (K1 ++ K2) e = fill K1 (fill K2 e).
Proof. revert e; induction K1; simpl; auto with f_equal. Qed.
284

285
Lemma fill_val K e : is_Some (to_val (fill K e))  is_Some (to_val e).
286
Proof.
287
  intros [v' Hv']; revert v' Hv'.
288
  induction K as [|[]]; intros; simplify_option_eq; eauto.
289
Qed.
290

291
292
Lemma fill_not_val K e : to_val e = None  to_val (fill K e) = None.
Proof. rewrite !eq_None_not_Some; eauto using fill_val. Qed.
293

294
Lemma val_head_stuck e1 σ1 e2 σ2 ef :
295
296
  head_step e1 σ1 e2 σ2 ef  to_val e1 = None.
Proof. destruct 1; naive_solver. Qed.
297

298
299
Lemma val_stuck e1 σ1 e2 σ2 ef : prim_step e1 σ1 e2 σ2 ef  to_val e1 = None.
Proof. intros [??? -> -> ?]; eauto using fill_not_val, val_head_stuck. Qed.
300

301
302
Lemma atomic_not_val e : atomic e  to_val e = None.
Proof. destruct e; naive_solver. Qed.
303

304
305
306
307
308
309
Lemma atomic_fill_item Ki e : atomic (fill_item Ki e)  is_Some (to_val e).
Proof.
  intros. destruct Ki; simplify_eq/=; destruct_conjs;
    repeat (case_match || contradiction); eauto.
Qed.

310
Lemma atomic_fill K e : atomic (fill K e)  to_val e = None  K = [].
311
Proof.
312
313
  destruct K as [|Ki K]; [done|].
  rewrite eq_None_not_Some=> /= ? []; eauto using atomic_fill_item, fill_val.
314
Qed.
315

316
317
Lemma atomic_head_step e1 σ1 e2 σ2 ef :
  atomic e1  head_step e1 σ1 e2 σ2 ef  is_Some (to_val e2).
Ralf Jung's avatar
Ralf Jung committed
318
Proof.
319
  destruct 2; simpl; rewrite ?to_of_val; try by eauto.
320
  unfold subst'; repeat (case_match || contradiction || simplify_eq/=); eauto.
Ralf Jung's avatar
Ralf Jung committed
321
Qed.
322

323
324
Lemma atomic_step e1 σ1 e2 σ2 ef :
  atomic e1  prim_step e1 σ1 e2 σ2 ef  is_Some (to_val e2).
325
Proof.
326
  intros Hatomic [K e1' e2' -> -> Hstep].
327
  assert (K = []) as -> by eauto 10 using atomic_fill, val_head_stuck.
328
  naive_solver eauto using atomic_head_step.
Ralf Jung's avatar
Ralf Jung committed
329
Qed.
330

331
Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef :
332
  head_step (fill_item Ki e) σ1 e2 σ2 ef  is_Some (to_val e).
333
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; eauto. Qed.
334

335
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
336
  to_val e1 = None  to_val e2 = None 
337
  fill_item Ki1 e1 = fill_item Ki2 e2  Ki1 = Ki2.
338
Proof.
339
  destruct Ki1, Ki2; intros; try discriminate; simplify_eq/=;
340
    repeat match goal with
341
342
    | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
    end; auto.
Ralf Jung's avatar
Ralf Jung committed
343
Qed.
344

345
346
347
348
349
350
(* When something does a step, and another decomposition of the same expression
has a non-val [e] in the hole, then [K] is a left sub-context of [K'] - in
other words, [e] also contains the reducible expression *)
Lemma step_by_val K K' e1 e1' σ1 e2 σ2 ef :
  fill K e1 = fill K' e1'  to_val e1 = None  head_step e1' σ1 e2 σ2 ef 
  K `prefix_of` K'.
351
Proof.
352
353
  intros Hfill Hred Hnval; revert K' Hfill.
  induction K as [|Ki K IH]; simpl; intros K' Hfill; auto using prefix_of_nil.
354
  destruct K' as [|Ki' K']; simplify_eq/=.
Ralf Jung's avatar
Ralf Jung committed
355
  { exfalso; apply (eq_None_not_Some (to_val (fill K e1)));
356
357
      eauto using fill_not_val, head_ctx_step_val. }
  cut (Ki = Ki'); [naive_solver eauto using prefix_of_cons|].
358
  eauto using fill_item_no_val_inj, val_head_stuck, fill_not_val.
359
Qed.
360

361
362
363
Lemma alloc_fresh e v σ :
  let l := fresh (dom _ σ) in
  to_val e = Some v  head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None.
364
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
365
366
367
368
369
370
371
372
373
End heap_lang.

(** Language *)
Program Canonical Structure heap_lang : language := {|
  expr := heap_lang.expr; val := heap_lang.val; state := heap_lang.state;
  of_val := heap_lang.of_val; to_val := heap_lang.to_val;
  atomic := heap_lang.atomic; prim_step := heap_lang.prim_step;
|}.
Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
374
  heap_lang.val_stuck, heap_lang.atomic_not_val, heap_lang.atomic_step.
375

376
Global Instance heap_lang_ctx K : LanguageCtx heap_lang (heap_lang.fill K).
377
Proof.
378
  split.
379
380
  - eauto using heap_lang.fill_not_val.
  - intros ????? [K' e1' e2' Heq1 Heq2 Hstep].
381
    by exists (K ++ K') e1' e2'; rewrite ?heap_lang.fill_app ?Heq1 ?Heq2.
382
  - intros e1 σ1 e2 σ2 ? Hnval [K'' e1'' e2'' Heq1 -> Hstep].
383
384
    destruct (heap_lang.step_by_val
      K K'' e1 e1'' σ1 e2'' σ2 ef) as [K' ->]; eauto.
385
    rewrite heap_lang.fill_app in Heq1; apply (inj _) in Heq1.
Ralf Jung's avatar
Ralf Jung committed
386
    exists (heap_lang.fill K' e2''); rewrite heap_lang.fill_app; split; auto.
387
    econstructor; eauto.
388
Qed.
389
390
391
392
393
394
395

Global Instance heap_lang_ctx_item Ki :
  LanguageCtx heap_lang (heap_lang.fill_item Ki).
Proof.
  change (LanguageCtx heap_lang (heap_lang.fill [Ki])).
  by apply _.
Qed.