lang.v 21.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
8
9
Delimit Scope expr_scope with E.
Delimit Scope val_scope with V.

10
Module heap_lang.
11
12
Open Scope Z_scope.

13
(** Expressions and vals. *)
14
Definition loc := positive. (* Really, any countable type. *)
Ralf Jung's avatar
Ralf Jung committed
15

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

26
Inductive binder := BAnon | BNamed : string  binder.
Ralf Jung's avatar
Ralf Jung committed
27
28
Delimit Scope binder_scope with bind.
Bind Scope binder_scope with binder.
29
30
31
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).
32
Instance binder_eq_dec_eq : EqDecision binder.
33
34
35
36
37
38
39
40
41
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.

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

69
70
Bind Scope expr_scope with expr.

71
72
73
74
75
76
77
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
78
  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 =>
79
80
81
82
83
     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
84
Class Closed (X : list string) (e : expr) := closed : is_closed X e.
85
Instance closed_proof_irrel X e : ProofIrrel (Closed X e).
86
Proof. rewrite /Closed. apply _. Qed.
87
88
Instance closed_dec X e : Decision (Closed X e).
Proof. rewrite /Closed. apply _. Defined.
89

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

97
98
Bind Scope val_scope with val.

99
Fixpoint of_val (v : val) : expr :=
Ralf Jung's avatar
Ralf Jung committed
100
  match v with
101
  | RecV f x e => Rec f x e
102
  | LitV l => Lit l
103
104
105
  | 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
106
  end.
107

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

119
120
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
(** We assume the following encoding of values to 64-bit words: The least 3
significant bits of every word are a "tag", and we have 61 bits of payload,
which is enough if all pointers are 8-byte-aligned (common on 64bit
architectures). The tags have the following meaning:

0: Payload is the data for a LitV (LitInt _).
1: Payload is the data for a InjLV (LitV (LitInt _)).
2: Payload is the data for a InjRV (LitV (LitInt _)).
3: Payload is the data for a LitV (LitLoc _).
4: Payload is the data for a InjLV (LitV (LitLoc _)).
4: Payload is the data for a InjRV (LitV (LitLoc _)).
6: Payload is one of the following finitely many values, which 61 bits are more
   than enough to encode:
   LitV LitUnit, InjLV (LitV LitUnit), InjRV (LitV LitUnit),
   LitV (LitBool _), InjLV (LitV (LitBool _)), InjRV (LitV (LitBool _)).
7: Value is boxed, i.e., payload is a pointer to some read-only memory area on
   the heap which stores whether this is a RecV, PairV, InjLV or InjRV and the
   relevant data for those cases. However, the boxed representation is never
   used if any of the above representations could be used.

Ignoring (as usual) the fact that we have to fit the infinite Z/loc into 61
bits, this means every value is machine-word-sized and can hence be atomically
read and written.  Also notice that the sets of boxed and unboxed values are
disjoint. *)
Definition val_is_unboxed (v : val) : Prop :=
  match v with
  | LitV _ => True
  | InjLV (LitV _) => True
  | InjRV (LitV _) => True
  | _ => False
  end.

151
152
(** The state: heaps of vals. *)
Definition state := gmap loc val.
Ralf Jung's avatar
Ralf Jung committed
153

154
155
156
157
158
159
160
161
162
163
164
165
166
167
(** 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.

168
Instance base_lit_eq_dec : EqDecision base_lit.
169
Proof. solve_decision. Defined.
170
Instance un_op_eq_dec : EqDecision un_op.
171
Proof. solve_decision. Defined.
172
Instance bin_op_eq_dec : EqDecision bin_op.
173
Proof. solve_decision. Defined.
174
Instance expr_eq_dec : EqDecision expr.
175
Proof. solve_decision. Defined.
176
Instance val_eq_dec : EqDecision val.
177
Proof.
178
 refine (λ v v', cast_if (decide (of_val v = of_val v'))); abstract naive_solver.
179
180
Defined.

181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
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
199
200
201
  | 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
202
  end) (λ n, match n with
203
204
205
  | 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
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
  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]
235
  | FAA e1 e2 => GenNode 16 [go e1; go e2]
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
  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)
257
  | GenNode 16 [e1; e2] => FAA (go e1) (go e2)
258
259
260
261
262
263
264
  | _ => 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.

265
266
267
268
269
270
271
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.

272
(** Evaluation contexts *)
273
Inductive ectx_item :=
274
  | AppLCtx (e2 : expr)
275
  | AppRCtx (v1 : val)
276
  | UnOpCtx (op : un_op)
277
  | BinOpLCtx (op : bin_op) (e2 : expr)
278
  | BinOpRCtx (op : bin_op) (v1 : val)
279
280
  | IfCtx (e1 e2 : expr)
  | PairLCtx (e2 : expr)
281
282
283
284
285
  | PairRCtx (v1 : val)
  | FstCtx
  | SndCtx
  | InjLCtx
  | InjRCtx
286
  | CaseCtx (e1 : expr) (e2 : expr)
287
288
  | AllocCtx
  | LoadCtx
289
  | StoreLCtx (e2 : expr)
290
  | StoreRCtx (v1 : val)
291
  | CasLCtx (e1 : expr) (e2 : expr)
292
  | CasMCtx (v0 : val) (e2 : expr)
293
294
295
  | CasRCtx (v0 : val) (v1 : val)
  | FaaLCtx (e2 : expr)
  | FaaRCtx (v1 : val).
296

297
Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
298
299
300
  match Ki with
  | AppLCtx e2 => App e e2
  | AppRCtx v1 => App (of_val v1) e
301
302
303
304
  | 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
305
306
307
308
309
310
  | PairLCtx e2 => Pair e e2
  | PairRCtx v1 => Pair (of_val v1) e
  | FstCtx => Fst e
  | SndCtx => Snd e
  | InjLCtx => InjL e
  | InjRCtx => InjR e
311
  | CaseCtx e1 e2 => Case e e1 e2
312
313
  | AllocCtx => Alloc e
  | LoadCtx => Load e
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
314
  | StoreLCtx e2 => Store e e2
315
  | StoreRCtx v1 => Store (of_val v1) e
316
317
318
  | 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
319
320
  | FaaLCtx e2 => FAA e e2
  | FaaRCtx v1 => FAA (of_val v1) e
Ralf Jung's avatar
Ralf Jung committed
321
322
  end.

323
(** Substitution *)
324
325
326
Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
  match e with
  | Var y => if decide (x = y) then es else Var y
327
  | Rec f y e =>
328
329
     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)
330
  | Lit l => Lit l
331
332
333
334
335
336
337
338
339
340
341
342
343
344
  | 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)
345
  | FAA e1 e2 => FAA (subst x es e1) (subst x es e2)
346
  end.
347

348
Definition subst' (mx : binder) (es : expr) : expr  expr :=
349
  match mx with BNamed x => subst x es | BAnon => id end.
350

351
(** The stepping relation *)
352
353
354
Definition un_op_eval (op : un_op) (v : val) : option val :=
  match op, v with
  | NegOp, LitV (LitBool b) => Some $ LitV $ LitBool (negb b)
355
  | NegOp, LitV (LitInt n) => Some $ LitV $ LitInt (Z.lnot n)
356
  | MinusUnOp, LitV (LitInt n) => Some $ LitV $ LitInt (- n)
357
358
359
  | _, _ => None
  end.

360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
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.

388
Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
389
  if decide (op = EqOp) then Some $ LitV $ LitBool $ bool_decide (v1 = v2) else
390
391
392
  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
393
  | _, _ => None
394
395
  end.

396
397
398
399
(** CAS just compares the word-sized representation of the two values, it cannot
look into boxed data.  This works out fine if at least one of the to-be-compared
values is unboxed (exploiting the fact that an unboxed and a boxed value can
never be equal because these are disjoint sets).  *)
Ralf Jung's avatar
Ralf Jung committed
400
Definition vals_cas_compare_safe (vl v1 : val) : Prop :=
401
402
  val_is_unboxed vl  val_is_unboxed v1.
Arguments vals_cas_compare_safe !_ !_ /.
Ralf Jung's avatar
Ralf Jung committed
403

404
Inductive head_step : expr  state  expr  state  list (expr)  Prop :=
405
  | BetaS f x e1 e2 v2 e' σ :
406
     to_val e2 = Some v2 
407
     Closed (f :b: x :b: []) e1 
408
     e' = subst' x (of_val v2) (subst' f (Rec f x e1) e1) 
409
     head_step (App (Rec f x e1) e2) σ e' σ []
410
411
  | UnOpS op e v v' σ :
     to_val e = Some v 
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
412
     un_op_eval op v = Some v' 
413
414
415
     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
416
     bin_op_eval op v1 v2 = Some v' 
417
     head_step (BinOp op e1 e2) σ (of_val v') σ []
418
  | IfTrueS e1 e2 σ :
419
     head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ []
420
  | IfFalseS e1 e2 σ :
421
     head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ []
422
423
  | FstS e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
424
     head_step (Fst (Pair e1 e2)) σ e1 σ []
425
426
  | SndS e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
427
     head_step (Snd (Pair e1 e2)) σ e2 σ []
428
  | CaseLS e0 v0 e1 e2 σ :
429
     to_val e0 = Some v0 
430
     head_step (Case (InjL e0) e1 e2) σ (App e1 e0) σ []
431
  | CaseRS e0 v0 e1 e2 σ :
432
     to_val e0 = Some v0 
433
     head_step (Case (InjR e0) e1 e2) σ (App e2 e0) σ []
434
  | ForkS e σ:
435
     head_step (Fork e) σ (Lit LitUnit) σ [e]
436
437
  | AllocS e v σ l :
     to_val e = Some v  σ !! l = None 
438
     head_step (Alloc e) σ (Lit $ LitLoc l) (<[l:=v]>σ) []
439
440
  | LoadS l v σ :
     σ !! l = Some v 
441
     head_step (Load (Lit $ LitLoc l)) σ (of_val v) σ []
442
443
  | StoreS l e v σ :
     to_val e = Some v  is_Some (σ !! l) 
444
     head_step (Store (Lit $ LitLoc l) e) σ (Lit LitUnit) (<[l:=v]>σ) []
445
446
447
  | 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
448
     vals_cas_compare_safe vl v1 
449
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool false) σ []
450
451
452
  | 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
453
     vals_cas_compare_safe v1 v1 
454
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) []
Ralf Jung's avatar
Ralf Jung committed
455
  | FaaS l i1 e2 i2 σ :
456
457
458
459
     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
460

461
(** Basic properties about the language *)
462
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
463
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
464

465
466
467
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.
468

469
Lemma val_head_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs  to_val e1 = None.
470
Proof. destruct 1; naive_solver. Qed.
471

472
473
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).
474
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
475

476
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
477
  to_val e1 = None  to_val e2 = None 
478
  fill_item Ki1 e1 = fill_item Ki2 e2  Ki1 = Ki2.
479
Proof.
480
  destruct Ki1, Ki2; intros; try discriminate; simplify_eq/=;
481
    repeat match goal with
482
483
    | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
    end; auto.
Ralf Jung's avatar
Ralf Jung committed
484
Qed.
485

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

491
492
493
494
495
(* 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
496
(** Closed expressions *)
497
Lemma is_closed_weaken X Y e : is_closed X e  X  Y  is_closed Y e.
Robbert Krebbers's avatar
Robbert Krebbers committed
498
499
Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.

500
Lemma is_closed_weaken_nil X e : is_closed [] e  is_closed X e.
501
Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
502

503
504
505
Lemma is_closed_of_val X v : is_closed X (of_val v).
Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.

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

509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
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
524
Proof.
525
  revert X. induction e=> X /=; rewrite ?bool_decide_spec ?andb_True=> ??;
Robbert Krebbers's avatar
Robbert Krebbers committed
526
527
    repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver.
Qed.
528

529
530
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.
531

532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
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.
562
563
564
565
566
567

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.
568
569
570
End heap_lang.

(** Language *)
571
572
573
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.
574

575
(* Prefer heap_lang names over ectx_language names. *)
576
Export heap_lang.
577
578
579
580
581
582
583
584
585
586
587

(** Define some derived forms. *)
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).

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