lang.v 23.9 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

Ralf Jung's avatar
Ralf Jung committed
7
8
9
10
11
12
13
14
(** heap_lang.  A fairly simple language used for common Iris examples.

- This is a right-to-left evaluated language, like CakeML and OCaml.  The reason
  for this is that it makes curried functions usable: Given a WP for [f a b], we
  know that any effects [f] might have to not matter until after *both* [a] and
  [b] are evaluated.  With left-to-right evaluation, that triple is basically
  useless the user let-expands [b].

15
16
17
18
19
20
- For prophecy variables, we annotate the reduction steps with an "observation"
  and tweak adequacy such that WP knows all future observations.  There is
  another possible choice: Use non-deterministic choice when creating a prophecy
  variable ([NewProph]), and when resolving it ([ResolveProph]) make the
  program diverge unless the variable matches.  That, however, requires an
  erasure proof that this endless loop does not make specifications useless.
Ralf Jung's avatar
Ralf Jung committed
21

22
*)
Ralf Jung's avatar
Ralf Jung committed
23

24
25
26
Delimit Scope expr_scope with E.
Delimit Scope val_scope with V.

27
Module heap_lang.
28
29
Open Scope Z_scope.

30
(** Expressions and vals. *)
31
Definition loc := positive. (* Really, any countable type. *)
32
Definition proph := positive.
Ralf Jung's avatar
Ralf Jung committed
33

34
Inductive base_lit : Set :=
35
  | LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitLoc (l : loc) | LitProphecy (p: proph).
36
Inductive un_op : Set :=
37
  | NegOp | MinusUnOp.
38
Inductive bin_op : Set :=
39
40
41
42
  | PlusOp | MinusOp | MultOp | QuotOp | RemOp (* Arithmetic *)
  | AndOp | OrOp | XorOp (* Bitwise *)
  | ShiftLOp | ShiftROp (* Shifts *)
  | LeOp | LtOp | EqOp. (* Relations *)
43

44
Inductive binder := BAnon | BNamed : string  binder.
Ralf Jung's avatar
Ralf Jung committed
45
46
Delimit Scope binder_scope with bind.
Bind Scope binder_scope with binder.
47
48
49
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).
50
Instance binder_eq_dec_eq : EqDecision binder.
51
52
53
54
55
56
57
58
59
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.

60
Inductive expr :=
61
  (* Base lambda calculus *)
62
63
64
  | Var (x : string)
  | Rec (f x : binder) (e : expr)
  | App (e1 e2 : expr)
65
66
  (* Base types and their operations *)
  | Lit (l : base_lit)
67
68
69
  | UnOp (op : un_op) (e : expr)
  | BinOp (op : bin_op) (e1 e2 : expr)
  | If (e0 e1 e2 : expr)
70
  (* Products *)
71
72
73
  | Pair (e1 e2 : expr)
  | Fst (e : expr)
  | Snd (e : expr)
74
  (* Sums *)
75
76
77
  | InjL (e : expr)
  | InjR (e : expr)
  | Case (e0 : expr) (e1 : expr) (e2 : expr)
78
  (* Concurrency *)
79
  | Fork (e : expr)
80
  (* Heap *)
81
82
83
  | Alloc (e : expr)
  | Load (e : expr)
  | Store (e1 : expr) (e2 : expr)
84
  | CAS (e0 : expr) (e1 : expr) (e2 : expr)
85
86
87
88
  | FAA (e1 : expr) (e2 : expr)
  (* Prophecy *)
  | NewProph
  | ResolveProph (e1 : expr) (e2 : expr).
Ralf Jung's avatar
Ralf Jung committed
89

90
91
Bind Scope expr_scope with expr.

92
93
94
95
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
96
  | Lit _ | NewProph => true
97
98
  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e =>
     is_closed X e
99
  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 | ResolveProph e1 e2 =>
100
101
102
103
104
     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
105
Class Closed (X : list string) (e : expr) := closed : is_closed X e.
106
Instance closed_proof_irrel X e : ProofIrrel (Closed X e).
107
Proof. rewrite /Closed. apply _. Qed.
108
109
Instance closed_dec X e : Decision (Closed X e).
Proof. rewrite /Closed. apply _. Defined.
110

111
Inductive val :=
112
  | RecV (f x : binder) (e : expr) `{!Closed (f :b: x :b: []) e}
113
  | LitV (l : base_lit)
114
115
  | PairV (v1 v2 : val)
  | InjLV (v : val)
116
  | InjRV (v : val).
Ralf Jung's avatar
Ralf Jung committed
117

118
119
Bind Scope val_scope with val.

120
Definition observation : Set := proph * val.
121

122
Fixpoint of_val (v : val) : expr :=
Ralf Jung's avatar
Ralf Jung committed
123
  match v with
124
  | RecV f x e => Rec f x e
125
  | LitV l => Lit l
126
127
128
  | 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
129
  end.
130

131
Fixpoint to_val (e : expr) : option val :=
132
  match e with
133
134
  | Rec f x e =>
     if decide (Closed (f :b: x :b: []) e) then Some (RecV f x e) else None
135
  | Lit l => Some (LitV l)
136
137
138
  | 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
139
  | _ => None
140
141
  end.

142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
(** 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.

174
(** The state: heaps of vals. *)
175
Definition state : Type := gmap loc val * gset proph.
176
Implicit Type σ : state.
Ralf Jung's avatar
Ralf Jung committed
177

178
179
180
181
182
183
184
185
186
187
188
189
190
191
(** 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.

192
Instance base_lit_eq_dec : EqDecision base_lit.
193
Proof. solve_decision. Defined.
194
Instance un_op_eq_dec : EqDecision un_op.
195
Proof. solve_decision. Defined.
196
Instance bin_op_eq_dec : EqDecision bin_op.
197
Proof. solve_decision. Defined.
198
Instance expr_eq_dec : EqDecision expr.
199
Proof. solve_decision. Defined.
200
Instance val_eq_dec : EqDecision val.
201
Proof.
202
 refine (λ v v', cast_if (decide (of_val v = of_val v'))); abstract naive_solver.
203
204
Defined.

205
206
207
Instance base_lit_countable : Countable base_lit.
Proof.
 refine (inj_countable' (λ l, match l with
208
209
210
  | LitInt n => (inl (inl n), None) | LitBool b => (inl (inr b), None)
  | LitUnit => (inr (inl ()), None) | LitLoc l => (inr (inr l), None)
  | LitProphecy p => (inr (inl ()), Some p)
211
  end) (λ l, match l with
212
213
  | (inl (inl n), None) => LitInt n | (inl (inr b), None) => LitBool b
  | (inr (inl ()), None) => LitUnit | (inr (inr l), None) => LitLoc l
214
  | (_, Some p) => LitProphecy p
215
216
217
218
219
220
221
222
223
224
  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
225
226
227
  | 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
228
  end) (λ n, match n with
229
230
231
  | 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
232
233
234
235
236
237
238
239
240
241
242
  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
243
244
  | Var x => GenLeaf (Some (inl (inl x)))
  | Rec f x e => GenNode 0 [GenLeaf (Some ((inl (inr f)))); GenLeaf (Some (inl (inr x))); go e]
245
  | App e1 e2 => GenNode 1 [go e1; go e2]
246
247
248
  | Lit l => GenLeaf (Some (inr (inl l)))
  | UnOp op e => GenNode 2 [GenLeaf (Some (inr (inr (inl op)))); go e]
  | BinOp op e1 e2 => GenNode 3 [GenLeaf (Some (inr (inr (inr op)))); go e1; go e2]
249
250
251
252
253
254
255
256
257
258
259
260
  | 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]
261
  | FAA e1 e2 => GenNode 16 [go e1; go e2]
262
263
  | NewProph => GenLeaf None
  | ResolveProph e1 e2 => GenNode 17 [go e1; go e2]
264
265
266
  end).
 set (dec := fix go e :=
  match e with
267
268
  | GenLeaf (Some(inl (inl x))) => Var x
  | GenNode 0 [GenLeaf (Some (inl (inr f))); GenLeaf (Some (inl (inr x))); e] => Rec f x (go e)
269
  | GenNode 1 [e1; e2] => App (go e1) (go e2)
270
271
272
  | GenLeaf (Some (inr (inl l))) => Lit l
  | GenNode 2 [GenLeaf (Some (inr (inr (inl op)))); e] => UnOp op (go e)
  | GenNode 3 [GenLeaf (Some (inr (inr (inr op)))); e1; e2] => BinOp op (go e1) (go e2)
273
274
275
276
277
278
279
280
281
282
283
284
  | 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)
285
  | GenNode 16 [e1; e2] => FAA (go e1) (go e2)
286
287
  | GenLeaf None => NewProph
  | GenNode 17 [e1; e2] => ResolveProph (go e1) (go e2)
288
289
290
291
292
293
294
  | _ => 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.

295
296
297
298
299
300
301
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.

302
(** Evaluation contexts *)
303
Inductive ectx_item :=
304
305
  | AppLCtx (v2 : val)
  | AppRCtx (e1 : expr)
306
  | UnOpCtx (op : un_op)
307
308
  | BinOpLCtx (op : bin_op) (v2 : val)
  | BinOpRCtx (op : bin_op) (e1 : expr)
309
  | IfCtx (e1 e2 : expr)
310
311
  | PairLCtx (v2 : val)
  | PairRCtx (e1 : expr)
312
313
314
315
  | FstCtx
  | SndCtx
  | InjLCtx
  | InjRCtx
316
  | CaseCtx (e1 : expr) (e2 : expr)
317
318
  | AllocCtx
  | LoadCtx
319
320
321
322
323
324
  | StoreLCtx (v2 : val)
  | StoreRCtx (e1 : expr)
  | CasLCtx (v1 : val) (v2 : val)
  | CasMCtx (e0 : expr) (v2 : val)
  | CasRCtx (e0 : expr) (e1 : expr)
  | FaaLCtx (v2 : val)
325
326
327
  | FaaRCtx (e1 : expr)
  | ProphLCtx (v2 : val)
  | ProphRCtx (e1 : expr).
328

329
Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
330
  match Ki with
331
332
  | AppLCtx v2 => App e (of_val v2)
  | AppRCtx e1 => App e1 e
333
  | UnOpCtx op => UnOp op e
334
335
  | BinOpLCtx op v2 => BinOp op e (of_val v2)
  | BinOpRCtx op e1 => BinOp op e1 e
336
  | IfCtx e1 e2 => If e e1 e2
337
338
  | PairLCtx v2 => Pair e (of_val v2)
  | PairRCtx e1 => Pair e1 e
339
340
341
342
  | FstCtx => Fst e
  | SndCtx => Snd e
  | InjLCtx => InjL e
  | InjRCtx => InjR e
343
  | CaseCtx e1 e2 => Case e e1 e2
344
345
  | AllocCtx => Alloc e
  | LoadCtx => Load e
346
347
348
349
350
351
352
  | StoreLCtx v2 => Store e (of_val v2)
  | StoreRCtx e1 => Store e1 e
  | CasLCtx v1 v2 => CAS e (of_val v1) (of_val v2)
  | CasMCtx e0 v2 => CAS e0 e (of_val v2)
  | CasRCtx e0 e1 => CAS e0 e1 e
  | FaaLCtx v2 => FAA e (of_val v2)
  | FaaRCtx e1 => FAA e1 e
353
354
  | ProphLCtx v2 => ResolveProph e (of_val v2)
  | ProphRCtx e1 => ResolveProph e1 e
Ralf Jung's avatar
Ralf Jung committed
355
356
  end.

357
(** Substitution *)
358
359
360
Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
  match e with
  | Var y => if decide (x = y) then es else Var y
361
  | Rec f y e =>
362
363
     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)
364
  | Lit l => Lit l
365
366
367
368
369
370
371
372
373
374
375
376
377
378
  | 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)
379
  | FAA e1 e2 => FAA (subst x es e1) (subst x es e2)
380
381
  | NewProph => NewProph
  | ResolveProph e1 e2 => ResolveProph (subst x es e1) (subst x es e2)
382
  end.
383

384
Definition subst' (mx : binder) (es : expr) : expr  expr :=
385
  match mx with BNamed x => subst x es | BAnon => id end.
386

387
(** The stepping relation *)
388
389
390
Definition un_op_eval (op : un_op) (v : val) : option val :=
  match op, v with
  | NegOp, LitV (LitBool b) => Some $ LitV $ LitBool (negb b)
391
  | NegOp, LitV (LitInt n) => Some $ LitV $ LitInt (Z.lnot n)
392
  | MinusUnOp, LitV (LitInt n) => Some $ LitV $ LitInt (- n)
393
394
395
  | _, _ => None
  end.

396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
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.

424
Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
425
  if decide (op = EqOp) then Some $ LitV $ LitBool $ bool_decide (v1 = v2) else
426
427
428
  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
429
  | _, _ => None
430
431
  end.

432
433
434
435
(** 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
436
Definition vals_cas_compare_safe (vl v1 : val) : Prop :=
437
438
  val_is_unboxed vl  val_is_unboxed v1.
Arguments vals_cas_compare_safe !_ !_ /.
Ralf Jung's avatar
Ralf Jung committed
439

440
Inductive head_step : expr  state  option observation -> expr  state  list (expr)  Prop :=
441
  | BetaS f x e1 e2 v2 e' σ :
442
     to_val e2 = Some v2 
443
     Closed (f :b: x :b: []) e1 
444
     e' = subst' x (of_val v2) (subst' f (Rec f x e1) e1) 
445
     head_step (App (Rec f x e1) e2) σ None e' σ []
446
447
  | UnOpS op e v v' σ :
     to_val e = Some v 
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
448
     un_op_eval op v = Some v' 
449
     head_step (UnOp op e) σ None (of_val v') σ []
450
451
  | 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
452
     bin_op_eval op v1 v2 = Some v' 
453
     head_step (BinOp op e1 e2) σ None (of_val v') σ []
454
  | IfTrueS e1 e2 σ :
455
     head_step (If (Lit $ LitBool true) e1 e2) σ None e1 σ []
456
  | IfFalseS e1 e2 σ :
457
     head_step (If (Lit $ LitBool false) e1 e2) σ None e2 σ []
458
459
  | FstS e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
460
     head_step (Fst (Pair e1 e2)) σ None e1 σ []
461
462
  | SndS e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
463
     head_step (Snd (Pair e1 e2)) σ None e2 σ []
464
  | CaseLS e0 v0 e1 e2 σ :
465
     to_val e0 = Some v0 
466
     head_step (Case (InjL e0) e1 e2) σ None (App e1 e0) σ []
467
  | CaseRS e0 v0 e1 e2 σ :
468
     to_val e0 = Some v0 
469
     head_step (Case (InjR e0) e1 e2) σ None (App e2 e0) σ []
470
  | ForkS e σ:
471
     head_step (Fork e) σ None (Lit LitUnit) σ [e]
472
  | AllocS e v σ l :
473
474
     to_val e = Some v  σ.1 !! l = None 
     head_step (Alloc e) σ None (Lit $ LitLoc l) (<[l:=v]>σ.1, σ.2) []
475
  | LoadS l v σ :
476
     σ.1 !! l = Some v 
477
     head_step (Load (Lit $ LitLoc l)) σ None (of_val v) σ []
478
  | StoreS l e v σ :
479
480
     to_val e = Some v  is_Some (σ.1 !! l) 
     head_step (Store (Lit $ LitLoc l) e) σ None (Lit LitUnit) (<[l:=v]>σ.1, σ.2) []
481
482
  | CasFailS l e1 v1 e2 v2 vl σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
483
     σ.1 !! l = Some vl  vl  v1 
Ralf Jung's avatar
Ralf Jung committed
484
     vals_cas_compare_safe vl v1 
485
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ None (Lit $ LitBool false) σ []
486
487
  | CasSucS l e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
488
     σ.1 !! l = Some v1 
Ralf Jung's avatar
Ralf Jung committed
489
     vals_cas_compare_safe v1 v1 
490
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ None (Lit $ LitBool true) (<[l:=v2]>σ.1, σ.2) []
Ralf Jung's avatar
Ralf Jung committed
491
  | FaaS l i1 e2 i2 σ :
492
     to_val e2 = Some (LitV (LitInt i2)) 
493
494
495
496
497
498
499
500
501
     σ.1 !! l = Some (LitV (LitInt i1)) 
     head_step (FAA (Lit $ LitLoc l) e2) σ None (Lit $ LitInt i1) (<[l:=LitV (LitInt (i1 + i2))]>σ.1, σ.2) []
  | NewProphS σ p :
     p  σ.2 
     head_step NewProph σ None (Lit $ LitProphecy p) (σ.1, {[ p ]}  σ.2) []
  | ResolveProphS e1 p e2 v σ :
     to_val e1 = Some (LitV $ LitProphecy p) 
     to_val e2 = Some v 
     head_step (ResolveProph e1 e2) σ (Some (p, v)) (Lit LitUnit) σ [].
Ralf Jung's avatar
Ralf Jung committed
502

503
(** Basic properties about the language *)
504
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
505
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
506

507
508
509
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.
510

511
Lemma val_head_stuck e1 σ1 κ e2 σ2 efs : head_step e1 σ1 κ e2 σ2 efs  to_val e1 = None.
512
Proof. destruct 1; naive_solver. Qed.
513

514
515
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).
516
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
517

518
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
519
  to_val e1 = None  to_val e2 = None 
520
  fill_item Ki1 e1 = fill_item Ki2 e2  Ki1 = Ki2.
521
Proof.
522
  destruct Ki1, Ki2; intros; try discriminate; simplify_eq/=;
523
    repeat match goal with
524
525
    | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
    end; auto.
Ralf Jung's avatar
Ralf Jung committed
526
Qed.
527

528
Lemma alloc_fresh e v σ :
529
530
  let l := fresh (dom (gset loc) σ.1) in
  to_val e = Some v  head_step (Alloc e) σ None (Lit (LitLoc l)) (<[l:=v]>σ.1, σ.2) [].
Robbert Krebbers's avatar
Robbert Krebbers committed
531
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset loc)), is_fresh. Qed.
532

533
534
535
536
537
Lemma new_proph_fresh σ :
  let p := fresh σ.2 in
  head_step NewProph σ None (Lit $ LitProphecy p) (σ.1, {[ p ]}  σ.2) [].
Proof. constructor. apply is_fresh. Qed.

538
539
540
541
542
(* 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
543
(** Closed expressions *)
544
Lemma is_closed_weaken X Y e : is_closed X e  X  Y  is_closed Y e.
Robbert Krebbers's avatar
Robbert Krebbers committed
545
546
Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.

547
Lemma is_closed_weaken_nil X e : is_closed [] e  is_closed X e.
548
Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
549

550
551
552
Lemma is_closed_of_val X v : is_closed X (of_val v).
Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.

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

556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
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
571
Proof.
572
  revert X. induction e=> X /=; rewrite ?bool_decide_spec ?andb_True=> ??;
Robbert Krebbers's avatar
Robbert Krebbers committed
573
574
    repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver.
Qed.
575

576
577
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.
578

579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
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.
609
610
611
612
613
614

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.
615
616
617
End heap_lang.

(** Language *)
618
619
620
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.
621

622
(* Prefer heap_lang names over ectx_language names. *)
623
Export heap_lang.
624
625
626
627
628
629
630
631
632
633
634

(** 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)).