lang.v 19.5 KB
Newer Older
1
From iris.program_logic Require Export language ectx_language ectxi_language.
2
From iris.algebra Require Export ofe.
Ralf Jung's avatar
Ralf Jung committed
3
4
From stdpp Require Export strings.
From stdpp Require Import gmap.
5
Set Default Proof Using "Type".
6

7
Module heap_lang.
8
9
Open Scope Z_scope.

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

13
Inductive base_lit : Set :=
14
  | LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitLoc (l : loc).
15
Inductive un_op : Set :=
16
  | NegOp | MinusUnOp.
17
Inductive bin_op : Set :=
18
19
20
21
  | PlusOp | MinusOp | MultOp | QuotOp | RemOp (* Arithmetic *)
  | AndOp | OrOp | XorOp (* Bitwise *)
  | ShiftLOp | ShiftROp (* Shifts *)
  | LeOp | LtOp | EqOp. (* Relations *)
22

23
Inductive binder := BAnon | BNamed : string  binder.
Ralf Jung's avatar
Ralf Jung committed
24
25
Delimit Scope binder_scope with bind.
Bind Scope binder_scope with binder.
26
27
28
Definition cons_binder (mx : binder) (X : list string) : list string :=
  match mx with BAnon => X | BNamed x => x :: X end.
Infix ":b:" := cons_binder (at level 60, right associativity).
29
Instance binder_eq_dec_eq : EqDecision binder.
30
31
32
33
34
35
36
37
38
Proof. solve_decision. Defined.

Instance set_unfold_cons_binder x mx X P :
  SetUnfold (x  X) P  SetUnfold (x  mx :b: X) (BNamed x = mx  P).
Proof.
  constructor. rewrite -(set_unfold (x  X) P).
  destruct mx; rewrite /= ?elem_of_cons; naive_solver.
Qed.

39
Inductive expr :=
40
  (* Base lambda calculus *)
41
42
43
  | Var (x : string)
  | Rec (f x : binder) (e : expr)
  | App (e1 e2 : expr)
44
45
  (* Base types and their operations *)
  | Lit (l : base_lit)
46
47
48
  | UnOp (op : un_op) (e : expr)
  | BinOp (op : bin_op) (e1 e2 : expr)
  | If (e0 e1 e2 : expr)
49
  (* Products *)
50
51
52
  | Pair (e1 e2 : expr)
  | Fst (e : expr)
  | Snd (e : expr)
53
  (* Sums *)
54
55
56
  | InjL (e : expr)
  | InjR (e : expr)
  | Case (e0 : expr) (e1 : expr) (e2 : expr)
57
  (* Concurrency *)
58
  | Fork (e : expr)
59
  (* Heap *)
60
61
62
  | Alloc (e : expr)
  | Load (e : expr)
  | Store (e1 : expr) (e2 : expr)
63
64
  | CAS (e0 : expr) (e1 : expr) (e2 : expr)
  | FAA (e1 : expr) (e2 : expr).
Ralf Jung's avatar
Ralf Jung committed
65

66
Bind Scope expr_scope with expr.
67
68
69
70
71
72
73
74

Fixpoint is_closed (X : list string) (e : expr) : bool :=
  match e with
  | Var x => bool_decide (x  X)
  | Rec f x e => is_closed (f :b: x :b: X) e
  | Lit _ => true
  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e =>
     is_closed X e
75
  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 =>
76
77
78
79
80
     is_closed X e1 && is_closed X e2
  | If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
     is_closed X e0 && is_closed X e1 && is_closed X e2
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
81
Class Closed (X : list string) (e : expr) := closed : is_closed X e.
82
Instance closed_proof_irrel X e : ProofIrrel (Closed X e).
83
Proof. rewrite /Closed. apply _. Qed.
84
85
Instance closed_dec X e : Decision (Closed X e).
Proof. rewrite /Closed. apply _. Defined.
86

87
Inductive val :=
88
  | RecV (f x : binder) (e : expr) `{!Closed (f :b: x :b: []) e}
89
  | LitV (l : base_lit)
90
91
  | PairV (v1 v2 : val)
  | InjLV (v : val)
92
  | InjRV (v : val).
Ralf Jung's avatar
Ralf Jung committed
93

94
Bind Scope val_scope with val.
95

96
Fixpoint of_val (v : val) : expr :=
Ralf Jung's avatar
Ralf Jung committed
97
  match v with
98
  | RecV f x e => Rec f x e
99
  | LitV l => Lit l
100
101
102
  | PairV v1 v2 => Pair (of_val v1) (of_val v2)
  | InjLV v => InjL (of_val v)
  | InjRV v => InjR (of_val v)
Ralf Jung's avatar
Ralf Jung committed
103
  end.
104

105
Fixpoint to_val (e : expr) : option val :=
106
  match e with
107
108
  | Rec f x e =>
     if decide (Closed (f :b: x :b: []) e) then Some (RecV f x e) else None
109
  | Lit l => Some (LitV l)
110
111
112
  | 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
Ralf Jung's avatar
Ralf Jung committed
113
  | _ => None
114
115
  end.

116
117
(** The state: heaps of vals. *)
Definition state := gmap loc val.
Ralf Jung's avatar
Ralf Jung committed
118

119
120
121
122
123
124
125
126
127
128
129
130
131
132
(** Equality and other typeclass stuff *)
Lemma to_of_val v : to_val (of_val v) = Some v.
Proof.
  by induction v; simplify_option_eq; repeat f_equal; try apply (proof_irrel _).
Qed.

Lemma of_to_val e v : to_val e = Some v  of_val v = e.
Proof.
  revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
Qed.

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

133
Instance base_lit_eq_dec : EqDecision base_lit.
134
Proof. solve_decision. Defined.
135
Instance un_op_eq_dec : EqDecision un_op.
136
Proof. solve_decision. Defined.
137
Instance bin_op_eq_dec : EqDecision bin_op.
138
Proof. solve_decision. Defined.
139
Instance expr_eq_dec : EqDecision expr.
140
Proof. solve_decision. Defined.
141
Instance val_eq_dec : EqDecision val.
142
Proof.
143
 refine (λ v v', cast_if (decide (of_val v = of_val v'))); abstract naive_solver.
144
145
Defined.

146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
Instance base_lit_countable : Countable base_lit.
Proof.
 refine (inj_countable' (λ l, match l with
  | LitInt n => inl (inl n) | LitBool b => inl (inr b)
  | LitUnit => inr (inl ()) | LitLoc l => inr (inr l)
  end) (λ l, match l with
  | inl (inl n) => LitInt n | inl (inr b) => LitBool b
  | inr (inl ()) => LitUnit | inr (inr l) => LitLoc l
  end) _); by intros [].
Qed.
Instance un_op_finite : Countable un_op.
Proof.
 refine (inj_countable' (λ op, match op with NegOp => 0 | MinusUnOp => 1 end)
  (λ n, match n with 0 => NegOp | _ => MinusUnOp end) _); by intros [].
Qed.
Instance bin_op_countable : Countable bin_op.
Proof.
 refine (inj_countable' (λ op, match op with
164
165
166
  | PlusOp => 0 | MinusOp => 1 | MultOp => 2 | QuotOp => 3 | RemOp => 4
  | AndOp => 5 | OrOp => 6 | XorOp => 7 | ShiftLOp => 8 | ShiftROp => 9
  | LeOp => 10 | LtOp => 11 | EqOp => 12
167
  end) (λ n, match n with
168
169
170
  | 0 => PlusOp | 1 => MinusOp | 2 => MultOp | 3 => QuotOp | 4 => RemOp
  | 5 => AndOp | 6 => OrOp | 7 => XorOp | 8 => ShiftLOp | 9 => ShiftROp
  | 10 => LeOp | 11 => LtOp | _ => EqOp
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
  end) _); by intros [].
Qed.
Instance binder_countable : Countable binder.
Proof.
 refine (inj_countable' (λ b, match b with BNamed s => Some s | BAnon => None end)
  (λ b, match b with Some s => BNamed s | None => BAnon end) _); by intros [].
Qed.
Instance expr_countable : Countable expr.
Proof.
 set (enc := fix go e :=
  match e with
  | Var x => GenLeaf (inl (inl x))
  | Rec f x e => GenNode 0 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); go e]
  | App e1 e2 => GenNode 1 [go e1; go e2]
  | Lit l => GenLeaf (inr (inl l))
  | UnOp op e => GenNode 2 [GenLeaf (inr (inr (inl op))); go e]
  | BinOp op e1 e2 => GenNode 3 [GenLeaf (inr (inr (inr op))); go e1; go e2]
  | If e0 e1 e2 => GenNode 4 [go e0; go e1; go e2]
  | Pair e1 e2 => GenNode 5 [go e1; go e2]
  | Fst e => GenNode 6 [go e]
  | Snd e => GenNode 7 [go e]
  | InjL e => GenNode 8 [go e]
  | InjR e => GenNode 9 [go e]
  | Case e0 e1 e2 => GenNode 10 [go e0; go e1; go e2]
  | Fork e => GenNode 11 [go e]
  | Alloc e => GenNode 12 [go e]
  | Load e => GenNode 13 [go e]
  | Store e1 e2 => GenNode 14 [go e1; go e2]
  | CAS e0 e1 e2 => GenNode 15 [go e0; go e1; go e2]
200
  | FAA e1 e2 => GenNode 16 [go e1; go e2]
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
  end).
 set (dec := fix go e :=
  match e with
  | GenLeaf (inl (inl x)) => Var x
  | GenNode 0 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); e] => Rec f x (go e)
  | GenNode 1 [e1; e2] => App (go e1) (go e2)
  | GenLeaf (inr (inl l)) => Lit l
  | GenNode 2 [GenLeaf (inr (inr (inl op))); e] => UnOp op (go e)
  | GenNode 3 [GenLeaf (inr (inr (inr op))); e1; e2] => BinOp op (go e1) (go e2)
  | GenNode 4 [e0; e1; e2] => If (go e0) (go e1) (go e2)
  | GenNode 5 [e1; e2] => Pair (go e1) (go e2)
  | GenNode 6 [e] => Fst (go e)
  | GenNode 7 [e] => Snd (go e)
  | GenNode 8 [e] => InjL (go e)
  | GenNode 9 [e] => InjR (go e)
  | GenNode 10 [e0; e1; e2] => Case (go e0) (go e1) (go e2)
  | GenNode 11 [e] => Fork (go e)
  | GenNode 12 [e] => Alloc (go e)
  | GenNode 13 [e] => Load (go e)
  | GenNode 14 [e1; e2] => Store (go e1) (go e2)
  | GenNode 15 [e0; e1; e2] => CAS (go e0) (go e1) (go e2)
222
  | GenNode 16 [e1; e2] => FAA (go e1) (go e2)
223
224
225
226
227
228
229
  | _ => Lit LitUnit (* dummy *)
  end).
 refine (inj_countable' enc dec _). intros e. induction e; f_equal/=; auto.
Qed.
Instance val_countable : Countable val.
Proof. refine (inj_countable of_val to_val _); auto using to_of_val. Qed.

230
231
232
233
234
235
236
Instance expr_inhabited : Inhabited expr := populate (Lit LitUnit).
Instance val_inhabited : Inhabited val := populate (LitV LitUnit).

Canonical Structure stateC := leibnizC state.
Canonical Structure valC := leibnizC val.
Canonical Structure exprC := leibnizC expr.

237
(** Evaluation contexts *)
238
Inductive ectx_item :=
239
  | AppLCtx (e2 : expr)
240
  | AppRCtx (v1 : val)
241
  | UnOpCtx (op : un_op)
242
  | BinOpLCtx (op : bin_op) (e2 : expr)
243
  | BinOpRCtx (op : bin_op) (v1 : val)
244
245
  | IfCtx (e1 e2 : expr)
  | PairLCtx (e2 : expr)
246
247
248
249
250
  | PairRCtx (v1 : val)
  | FstCtx
  | SndCtx
  | InjLCtx
  | InjRCtx
251
  | CaseCtx (e1 : expr) (e2 : expr)
252
253
  | AllocCtx
  | LoadCtx
254
  | StoreLCtx (e2 : expr)
255
  | StoreRCtx (v1 : val)
256
  | CasLCtx (e1 : expr) (e2 : expr)
257
  | CasMCtx (v0 : val) (e2 : expr)
258
259
260
  | CasRCtx (v0 : val) (v1 : val)
  | FaaLCtx (e2 : expr)
  | FaaRCtx (v1 : val).
261

262
Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
263
264
265
  match Ki with
  | AppLCtx e2 => App e e2
  | AppRCtx v1 => App (of_val v1) e
266
267
268
269
  | 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
270
271
272
273
274
275
  | PairLCtx e2 => Pair e e2
  | PairRCtx v1 => Pair (of_val v1) e
  | FstCtx => Fst e
  | SndCtx => Snd e
  | InjLCtx => InjL e
  | InjRCtx => InjR e
276
  | CaseCtx e1 e2 => Case e e1 e2
277
278
  | AllocCtx => Alloc e
  | LoadCtx => Load e
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
279
  | StoreLCtx e2 => Store e e2
280
  | StoreRCtx v1 => Store (of_val v1) e
281
282
283
  | 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
284
285
  | FaaLCtx e2 => FAA e e2
  | FaaRCtx v1 => FAA (of_val v1) e
Ralf Jung's avatar
Ralf Jung committed
286
287
  end.

288
(** Substitution *)
289
290
291
Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
  match e with
  | Var y => if decide (x = y) then es else Var y
292
  | Rec f y e =>
293
294
     Rec f y $ if decide (BNamed x  f  BNamed x  y) then subst x es e else e
  | App e1 e2 => App (subst x es e1) (subst x es e2)
295
  | Lit l => Lit l
296
297
298
299
300
301
302
303
304
305
306
307
308
309
  | UnOp op e => UnOp op (subst x es e)
  | BinOp op e1 e2 => BinOp op (subst x es e1) (subst x es e2)
  | If e0 e1 e2 => If (subst x es e0) (subst x es e1) (subst x es e2)
  | Pair e1 e2 => Pair (subst x es e1) (subst x es e2)
  | Fst e => Fst (subst x es e)
  | Snd e => Snd (subst x es e)
  | InjL e => InjL (subst x es e)
  | InjR e => InjR (subst x es e)
  | Case e0 e1 e2 => Case (subst x es e0) (subst x es e1) (subst x es e2)
  | Fork e => Fork (subst x es e)
  | Alloc e => Alloc (subst x es e)
  | Load e => Load (subst x es e)
  | Store e1 e2 => Store (subst x es e1) (subst x es e2)
  | CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
310
  | FAA e1 e2 => FAA (subst x es e1) (subst x es e2)
311
  end.
312

313
Definition subst' (mx : binder) (es : expr) : expr  expr :=
314
  match mx with BNamed x => subst x es | BAnon => id end.
315

316
(** The stepping relation *)
317
318
319
Definition un_op_eval (op : un_op) (v : val) : option val :=
  match op, v with
  | NegOp, LitV (LitBool b) => Some $ LitV $ LitBool (negb b)
320
  | NegOp, LitV (LitInt n) => Some $ LitV $ LitInt (Z.lnot n)
321
  | MinusUnOp, LitV (LitInt n) => Some $ LitV $ LitInt (- n)
322
323
324
  | _, _ => None
  end.

325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
Definition bin_op_eval_int (op : bin_op) (n1 n2 : Z) : base_lit :=
  match op with
  | PlusOp => LitInt (n1 + n2)
  | MinusOp => LitInt (n1 - n2)
  | MultOp => LitInt (n1 * n2)
  | QuotOp => LitInt (n1 `quot` n2)
  | RemOp => LitInt (n1 `rem` n2)
  | AndOp => LitInt (Z.land n1 n2)
  | OrOp => LitInt (Z.lor n1 n2)
  | XorOp => LitInt (Z.lxor n1 n2)
  | ShiftLOp => LitInt (n1  n2)
  | ShiftROp => LitInt (n1  n2)
  | LeOp => LitBool (bool_decide (n1  n2))
  | LtOp => LitBool (bool_decide (n1 < n2))
  | EqOp => LitBool (bool_decide (n1 = n2))
  end.

Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
  match op with
  | PlusOp | MinusOp | MultOp | QuotOp | RemOp => None (* Arithmetic *)
  | AndOp => Some (LitBool (b1 && b2))
  | OrOp => Some (LitBool (b1 || b2))
  | XorOp => Some (LitBool (xorb b1 b2))
  | ShiftLOp | ShiftROp => None (* Shifts *)
  | LeOp | LtOp => None (* InEquality *)
  | EqOp => Some (LitBool (bool_decide (b1 = b2)))
  end.

353
Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
354
  if decide (op = EqOp) then Some $ LitV $ LitBool $ bool_decide (v1 = v2) else
355
356
357
  match v1, v2 with
  | LitV (LitInt n1), LitV (LitInt n2) => Some $ LitV $ bin_op_eval_int op n1 n2
  | LitV (LitBool b1), LitV (LitBool b2) => LitV <$> bin_op_eval_bool op b1 b2
Robbert Krebbers's avatar
Robbert Krebbers committed
358
  | _, _ => None
359
360
  end.

361
Inductive head_step : expr  state  expr  state  list (expr)  Prop :=
362
  | BetaS f x e1 e2 v2 e' σ :
363
     to_val e2 = Some v2 
364
     Closed (f :b: x :b: []) e1 
365
     e' = subst' x (of_val v2) (subst' f (Rec f x e1) e1) 
366
     head_step (App (Rec f x e1) e2) σ e' σ []
367
368
  | UnOpS op e v v' σ :
     to_val e = Some v 
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
369
     un_op_eval op v = Some v' 
370
371
372
     head_step (UnOp op e) σ (of_val v') σ []
  | BinOpS op e1 e2 v1 v2 v' σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
373
     bin_op_eval op v1 v2 = Some v' 
374
     head_step (BinOp op e1 e2) σ (of_val v') σ []
375
  | IfTrueS e1 e2 σ :
376
     head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ []
377
  | IfFalseS e1 e2 σ :
378
     head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ []
379
380
  | FstS e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
381
     head_step (Fst (Pair e1 e2)) σ e1 σ []
382
383
  | SndS e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
384
     head_step (Snd (Pair e1 e2)) σ e2 σ []
385
  | CaseLS e0 v0 e1 e2 σ :
386
     to_val e0 = Some v0 
387
     head_step (Case (InjL e0) e1 e2) σ (App e1 e0) σ []
388
  | CaseRS e0 v0 e1 e2 σ :
389
     to_val e0 = Some v0 
390
     head_step (Case (InjR e0) e1 e2) σ (App e2 e0) σ []
391
  | ForkS e σ:
392
     head_step (Fork e) σ (Lit LitUnit) σ [e]
393
394
  | AllocS e v σ l :
     to_val e = Some v  σ !! l = None 
395
     head_step (Alloc e) σ (Lit $ LitLoc l) (<[l:=v]>σ) []
396
397
  | LoadS l v σ :
     σ !! l = Some v 
398
     head_step (Load (Lit $ LitLoc l)) σ (of_val v) σ []
399
400
  | StoreS l e v σ :
     to_val e = Some v  is_Some (σ !! l) 
401
     head_step (Store (Lit $ LitLoc l) e) σ (Lit LitUnit) (<[l:=v]>σ) []
402
403
404
  | CasFailS l e1 v1 e2 v2 vl σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some vl  vl  v1 
405
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool false) σ []
406
407
408
  | CasSucS l e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some v1 
409
410
411
412
413
414
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) []
   | FaaS l i1 e2 i2 σ :
     to_val e2 = Some (LitV (LitInt i2)) 
     σ !! l = Some (LitV (LitInt i1)) 
     head_step (FAA (Lit $ LitLoc l) e2) σ (Lit $ LitInt i1) (<[l:=LitV (LitInt (i1 + i2))]>σ) [].

Ralf Jung's avatar
Ralf Jung committed
415

416
(** Basic properties about the language *)
417
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
418
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
419

420
421
422
Lemma fill_item_val Ki e :
  is_Some (to_val (fill_item Ki e))  is_Some (to_val e).
Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
423

424
Lemma val_head_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs  to_val e1 = None.
425
Proof. destruct 1; naive_solver. Qed.
426

427
428
Lemma head_ctx_step_val Ki e σ1 e2 σ2 efs :
  head_step (fill_item Ki e) σ1 e2 σ2 efs  is_Some (to_val e).
429
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
430

431
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
432
  to_val e1 = None  to_val e2 = None 
433
  fill_item Ki1 e1 = fill_item Ki2 e2  Ki1 = Ki2.
434
Proof.
435
  destruct Ki1, Ki2; intros; try discriminate; simplify_eq/=;
436
    repeat match goal with
437
438
    | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
    end; auto.
Ralf Jung's avatar
Ralf Jung committed
439
Qed.
440

441
Lemma alloc_fresh e v σ :
442
  let l := fresh (dom (gset loc) σ) in
443
  to_val e = Some v  head_step (Alloc e) σ (Lit (LitLoc l)) (<[l:=v]>σ) [].
Robbert Krebbers's avatar
Robbert Krebbers committed
444
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset loc)), is_fresh. Qed.
445

446
447
448
449
450
(* Misc *)
Lemma to_val_rec f x e `{!Closed (f :b: x :b: []) e} :
  to_val (Rec f x e) = Some (RecV f x e).
Proof. rewrite /to_val. case_decide=> //. do 2 f_equal; apply proof_irrel. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
451
(** Closed expressions *)
452
Lemma is_closed_weaken X Y e : is_closed X e  X  Y  is_closed Y e.
Robbert Krebbers's avatar
Robbert Krebbers committed
453
454
Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.

455
Lemma is_closed_weaken_nil X e : is_closed [] e  is_closed X e.
456
Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
457

458
459
460
Lemma is_closed_of_val X v : is_closed X (of_val v).
Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.

461
Lemma is_closed_to_val X e v : to_val e = Some v  is_closed X e.
Robbert Krebbers's avatar
Robbert Krebbers committed
462
Proof. intros <-%of_to_val. apply is_closed_of_val. Qed.
463

464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
Lemma is_closed_subst X e x es :
  is_closed [] es  is_closed (x :: X) e  is_closed X (subst x es e).
Proof.
  intros ?. revert X.
  induction e=> X /= ?; destruct_and?; split_and?; simplify_option_eq;
    try match goal with
    | H : ¬(_  _) |- _ => apply not_and_l in H as [?%dec_stable|?%dec_stable]
    end; eauto using is_closed_weaken with set_solver.
Qed.
Lemma is_closed_do_subst' X e x es :
  is_closed [] es  is_closed (x :b: X) e  is_closed X (subst' x es e).
Proof. destruct x; eauto using is_closed_subst. Qed.

(* Substitution *)
Lemma subst_is_closed X e x es : is_closed X e  x  X  subst x es e = e.
Robbert Krebbers's avatar
Robbert Krebbers committed
479
Proof.
480
  revert X. induction e=> X /=; rewrite ?bool_decide_spec ?andb_True=> ??;
Robbert Krebbers's avatar
Robbert Krebbers committed
481
482
    repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver.
Qed.
483

484
485
Lemma subst_is_closed_nil e x es : is_closed [] e  subst x es e = e.
Proof. intros. apply subst_is_closed with []; set_solver. Qed.
486

487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
Lemma subst_subst e x es es' :
  Closed [] es'  subst x es (subst x es' e) = subst x es' e.
Proof.
  intros. induction e; simpl; try (f_equal; by auto);
    simplify_option_eq; auto using subst_is_closed_nil with f_equal.
Qed.
Lemma subst_subst' e x es es' :
  Closed [] es'  subst' x es (subst' x es' e) = subst' x es' e.
Proof. destruct x; simpl; auto using subst_subst. Qed.

Lemma subst_subst_ne e x y es es' :
  Closed [] es  Closed [] es'  x  y 
  subst x es (subst y es' e) = subst y es' (subst x es e).
Proof.
  intros. induction e; simpl; try (f_equal; by auto);
    simplify_option_eq; auto using eq_sym, subst_is_closed_nil with f_equal.
Qed.
Lemma subst_subst_ne' e x y es es' :
  Closed [] es  Closed [] es'  x  y 
  subst' x es (subst' y es' e) = subst' y es' (subst' x es e).
Proof. destruct x, y; simpl; auto using subst_subst_ne with congruence. Qed.

Lemma subst_rec' f y e x es :
  x = f  x = y  x = BAnon 
  subst' x es (Rec f y e) = Rec f y e.
Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.
Lemma subst_rec_ne' f y e x es :
  (x  f  f = BAnon)  (x  y  y = BAnon) 
  subst' x es (Rec f y e) = Rec f y (subst' x es e).
Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.
517
518
519
520
521
522

Lemma heap_lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
Proof.
  split; apply _ || eauto using to_of_val, of_to_val, val_head_stuck,
    fill_item_val, fill_item_no_val_inj, head_ctx_step_val.
Qed.
523
524
525
End heap_lang.

(** Language *)
526
527
528
Canonical Structure heap_ectxi_lang := EctxiLanguage heap_lang.heap_lang_mixin.
Canonical Structure heap_ectx_lang := EctxLanguageOfEctxi heap_ectxi_lang.
Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang.
529

530
(* Prefer heap_lang names over ectx_language names. *)
531
Export heap_lang.
532
533

(** Define some derived forms *)
534
535
536
537
538
539
540
541
Notation Lam x e := (Rec BAnon x e) (only parsing).
Notation Let x e1 e2 := (App (Lam x e2) e1) (only parsing).
Notation Seq e1 e2 := (Let BAnon e1 e2) (only parsing).
Notation LamV x e := (RecV BAnon x e) (only parsing).
Notation LetCtx x e2 := (AppRCtx (LamV x e2)) (only parsing).
Notation SeqCtx e2 := (LetCtx BAnon e2) (only parsing).
Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)) (only parsing).

542
Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).