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

Ralf Jung's avatar
Ralf Jung committed
8
9
10
11
12
13
(** 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
Ralf Jung's avatar
Ralf Jung committed
14
  useless unless the user let-expands [b].
Ralf Jung's avatar
Ralf Jung committed
15

16
- For prophecy variables, we annotate the reduction steps with an "observation"
17
  and tweak adequacy such that WP knows all future observations. There is
18
  another possible choice: Use non-deterministic choice when creating a prophecy
19
20
  variable ([NewProph]), and when resolving it ([Resolve]) make the
  program diverge unless the variable matches. That, however, requires an
21
  erasure proof that this endless loop does not make specifications useless.
Ralf Jung's avatar
Ralf Jung committed
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
The expression [Resolve e p v] attaches a prophecy resolution (for prophecy
variable [p] to value [v]) to the top-level head-reduction step of [e]. The
prophecy resolution happens simultaneously with the head-step being taken.
Furthermore, it is required that the head-step produces a value (otherwise
the [Resolve] is stuck), and this value is also attached to the resolution.
A prophecy variable is thus resolved to a pair containing (1) the result
value of the wrapped expression (called [e] above), and (2) the value that
was attached by the [Resolve] (called [v] above). This allows, for example,
to distinguish a resolution originating from a successful [CAS] from one
originating from a failing [CAS]. For example:
 - [Resolve (CAS #l #n #(n+1)) #p v] will behave as [CAS #l #n #(n+1)],
   which means step to a boolean [b] while updating the heap, but in the
   meantime the prophecy variable [p] will be resolved to [(#b, v)].
 - [Resolve (! #l) #p v] will behave as [! #l], that is return the value
   [w] pointed to by [l] on the heap (assuming it was allocated properly),
   but it will additionally resolve [p] to the pair [(w,v)].

Note that the sub-expressions of [Resolve e p v] (i.e., [e], [p] and [v])
are reduced as usual, from right to left. However, the evaluation of [e]
is restricted so that the head-step to which the resolution is attached
cannot be taken by the context. For example:
 - [Resolve (CAS #l #n (#n + #1)) #p v] will first be reduced (with by a
   context-step) to [Resolve (CAS #l #n #(n+1) #p v], and then behave as
   described above.
 - However, [Resolve ((λ: "n", CAS #l "n" ("n" + #1)) #n) #p v] is stuck.
   Indeed, it can only be evaluated using a head-step (it is a β-redex),
   but the process does not yield a value.

The mechanism described above supports nesting [Resolve] expressions to
attach several prophecy resolutions to a head-redex. *)
Ralf Jung's avatar
Ralf Jung committed
53

54
55
56
Delimit Scope expr_scope with E.
Delimit Scope val_scope with V.

57
Module heap_lang.
58
59
Open Scope Z_scope.

60
(** Expressions and vals. *)
61
Definition proph_id := positive.
Ralf Jung's avatar
Ralf Jung committed
62

63
Inductive base_lit : Set :=
64
65
  | LitInt (n : Z) | LitBool (b : bool) | LitUnit
  | LitLoc (l : loc) | LitProphecy (p: proph_id).
66
Inductive un_op : Set :=
67
  | NegOp | MinusUnOp.
68
Inductive bin_op : Set :=
69
70
71
  | PlusOp | MinusOp | MultOp | QuotOp | RemOp (* Arithmetic *)
  | AndOp | OrOp | XorOp (* Bitwise *)
  | ShiftLOp | ShiftROp (* Shifts *)
Amin Timany's avatar
Amin Timany committed
72
73
  | LeOp | LtOp | EqOp (* Relations *)
  | OffsetOp. (* Pointer offset *)
74

75
Inductive expr :=
76
77
  (* Values *)
  | Val (v : val)
78
  (* Base lambda calculus *)
79
80
81
  | Var (x : string)
  | Rec (f x : binder) (e : expr)
  | App (e1 e2 : expr)
82
  (* Base types and their operations *)
83
84
85
  | UnOp (op : un_op) (e : expr)
  | BinOp (op : bin_op) (e1 e2 : expr)
  | If (e0 e1 e2 : expr)
86
  (* Products *)
87
88
89
  | Pair (e1 e2 : expr)
  | Fst (e : expr)
  | Snd (e : expr)
90
  (* Sums *)
91
92
93
  | InjL (e : expr)
  | InjR (e : expr)
  | Case (e0 : expr) (e1 : expr) (e2 : expr)
94
  (* Concurrency *)
95
  | Fork (e : expr)
96
  (* Heap *)
Amin Timany's avatar
Amin Timany committed
97
  | AllocN (e1 e2 : expr) (* array length (positive number), initial value *)
98
99
  | Load (e : expr)
  | Store (e1 : expr) (e2 : expr)
100
  | CAS (e0 : expr) (e1 : expr) (e2 : expr)
101
102
103
  | FAA (e1 : expr) (e2 : expr)
  (* Prophecy *)
  | NewProph
104
  | Resolve (e0 : expr) (e1 : expr) (e2 : expr) (* wrapped expr, proph, val *)
105
with val :=
106
  | LitV (l : base_lit)
107
  | RecV (f x : binder) (e : expr)
108
109
  | PairV (v1 v2 : val)
  | InjLV (v : val)
110
  | InjRV (v : val).
Ralf Jung's avatar
Ralf Jung committed
111

112
Bind Scope expr_scope with expr.
113
114
Bind Scope val_scope with val.

115
116
117
118
119
120
(** An observation associates a prophecy variable (identifier) to a pair of
values. The first value is the one that was returned by the (atomic) operation
during which the prophecy resolution happened (typically, a boolean when the
wrapped operation is a CAS). The second value is the one that the prophecy
variable was actually resolved to. *)
Definition observation : Set := proph_id * (val * val).
121

122
Notation of_val := Val (only parsing).
123

124
Definition to_val (e : expr) : option val :=
125
  match e with
126
  | Val v => Some v
Ralf Jung's avatar
Ralf Jung committed
127
  | _ => None
128
129
  end.

130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
(** 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.

162
(** The state: heaps of vals. *)
Ralf Jung's avatar
Ralf Jung committed
163
164
Record state : Type := {
  heap: gmap loc val;
165
  used_proph_id: gset proph_id;
Ralf Jung's avatar
Ralf Jung committed
166
}.
Ralf Jung's avatar
Ralf Jung committed
167

168
169
(** Equality and other typeclass stuff *)
Lemma to_of_val v : to_val (of_val v) = Some v.
170
Proof. by destruct v. Qed.
171
172

Lemma of_to_val e v : to_val e = Some v  of_val v = e.
173
Proof. destruct e=>//=. by intros [= <-]. Qed.
174
175

Instance of_val_inj : Inj (=) (=) of_val.
176
Proof. intros ??. congruence. Qed.
177

178
Instance base_lit_eq_dec : EqDecision base_lit.
179
Proof. solve_decision. Defined.
180
Instance un_op_eq_dec : EqDecision un_op.
181
Proof. solve_decision. Defined.
182
Instance bin_op_eq_dec : EqDecision bin_op.
183
Proof. solve_decision. Defined.
184
Instance expr_eq_dec : EqDecision expr.
185
Proof.
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
  refine (
   fix go (e1 e2 : expr) {struct e1} : Decision (e1 = e2) :=
     match e1, e2 with
     | Val v, Val v' => cast_if (decide (v = v'))
     | Var x, Var x' => cast_if (decide (x = x'))
     | Rec f x e, Rec f' x' e' =>
        cast_if_and3 (decide (f = f')) (decide (x = x')) (decide (e = e'))
     | App e1 e2, App e1' e2' => cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
     | UnOp o e, UnOp o' e' => cast_if_and (decide (o = o')) (decide (e = e'))
     | BinOp o e1 e2, BinOp o' e1' e2' =>
        cast_if_and3 (decide (o = o')) (decide (e1 = e1')) (decide (e2 = e2'))
     | If e0 e1 e2, If e0' e1' e2' =>
        cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
     | Pair e1 e2, Pair e1' e2' =>
        cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
     | Fst e, Fst e' => cast_if (decide (e = e'))
     | Snd e, Snd e' => cast_if (decide (e = e'))
     | InjL e, InjL e' => cast_if (decide (e = e'))
     | InjR e, InjR e' => cast_if (decide (e = e'))
     | Case e0 e1 e2, Case e0' e1' e2' =>
        cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
     | Fork e, Fork e' => cast_if (decide (e = e'))
Amin Timany's avatar
Amin Timany committed
208
209
     | AllocN e1 e2, AllocN e1' e2' =>
        cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
210
211
212
213
214
215
216
217
     | Load e, Load e' => cast_if (decide (e = e'))
     | Store e1 e2, Store e1' e2' =>
        cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
     | CAS e0 e1 e2, CAS e0' e1' e2' =>
        cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
     | FAA e1 e2, FAA e1' e2' =>
        cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
     | NewProph, NewProph => left _
218
219
     | Resolve e0 e1 e2, Resolve e0' e1' e2' =>
        cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
220
221
222
223
224
225
226
227
228
229
230
231
232
233
     | _, _ => right _
     end
   with gov (v1 v2 : val) {struct v1} : Decision (v1 = v2) :=
     match v1, v2 with
     | LitV l, LitV l' => cast_if (decide (l = l'))
     | RecV f x e, RecV f' x' e' =>
        cast_if_and3 (decide (f = f')) (decide (x = x')) (decide (e = e'))
     | PairV e1 e2, PairV e1' e2' =>
        cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
     | InjLV e, InjLV e' => cast_if (decide (e = e'))
     | InjRV e, InjRV e' => cast_if (decide (e = e'))
     | _, _ => right _
     end
   for go); try (clear go gov; abstract intuition congruence).
234
Defined.
235
236
Instance val_eq_dec : EqDecision val.
Proof. solve_decision. Defined.
237

238
239
240
Instance base_lit_countable : Countable base_lit.
Proof.
 refine (inj_countable' (λ l, match l with
241
242
243
  | 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)
244
  end) (λ l, match l with
245
246
  | (inl (inl n), None) => LitInt n | (inl (inr b), None) => LitBool b
  | (inr (inl ()), None) => LitUnit | (inr (inr l), None) => LitLoc l
247
  | (_, Some p) => LitProphecy p
248
249
250
251
252
253
254
255
256
257
  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
258
259
  | PlusOp => 0 | MinusOp => 1 | MultOp => 2 | QuotOp => 3 | RemOp => 4
  | AndOp => 5 | OrOp => 6 | XorOp => 7 | ShiftLOp => 8 | ShiftROp => 9
Amin Timany's avatar
Amin Timany committed
260
  | LeOp => 10 | LtOp => 11 | EqOp => 12 | OffsetOp => 13
261
  end) (λ n, match n with
262
263
  | 0 => PlusOp | 1 => MinusOp | 2 => MultOp | 3 => QuotOp | 4 => RemOp
  | 5 => AndOp | 6 => OrOp | 7 => XorOp | 8 => ShiftLOp | 9 => ShiftROp
Amin Timany's avatar
Amin Timany committed
264
  | 10 => LeOp | 11 => LtOp | 12 => EqOp | _ => OffsetOp
265
266
267
268
  end) _); by intros [].
Qed.
Instance expr_countable : Countable expr.
Proof.
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
 set (enc :=
   fix go e :=
     match e with
     | Val v => GenNode 0 [gov v]
     | Var x => GenLeaf (inl (inl x))
     | Rec f x e => GenNode 1 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); go e]
     | App e1 e2 => GenNode 2 [go e1; go e2]
     | UnOp op e => GenNode 3 [GenLeaf (inr (inr (inl op))); go e]
     | BinOp op e1 e2 => GenNode 4 [GenLeaf (inr (inr (inr op))); go e1; go e2]
     | If e0 e1 e2 => GenNode 5 [go e0; go e1; go e2]
     | Pair e1 e2 => GenNode 6 [go e1; go e2]
     | Fst e => GenNode 7 [go e]
     | Snd e => GenNode 8 [go e]
     | InjL e => GenNode 9 [go e]
     | InjR e => GenNode 10 [go e]
     | Case e0 e1 e2 => GenNode 11 [go e0; go e1; go e2]
     | Fork e => GenNode 12 [go e]
Amin Timany's avatar
Amin Timany committed
286
     | AllocN e1 e2 => GenNode 13 [go e1; go e2]
287
288
289
290
291
     | Load e => GenNode 14 [go e]
     | Store e1 e2 => GenNode 15 [go e1; go e2]
     | CAS e0 e1 e2 => GenNode 16 [go e0; go e1; go e2]
     | FAA e1 e2 => GenNode 17 [go e1; go e2]
     | NewProph => GenNode 18 []
292
     | Resolve e0 e1 e2 => GenNode 19 [go e0; go e1; go e2]
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
     end
   with gov v :=
     match v with
     | LitV l => GenLeaf (inr (inl l))
     | RecV f x e =>
        GenNode 0 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); go e]
     | PairV v1 v2 => GenNode 1 [gov v1; gov v2]
     | InjLV v => GenNode 2 [gov v]
     | InjRV v => GenNode 3 [gov v]
     end
   for go).
 set (dec :=
   fix go e :=
     match e with
     | GenNode 0 [v] => Val (gov v)
     | GenLeaf (inl (inl x)) => Var x
     | GenNode 1 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); e] => Rec f x (go e)
     | GenNode 2 [e1; e2] => App (go e1) (go e2)
     | GenNode 3 [GenLeaf (inr (inr (inl op))); e] => UnOp op (go e)
     | GenNode 4 [GenLeaf (inr (inr (inr op))); e1; e2] => BinOp op (go e1) (go e2)
     | GenNode 5 [e0; e1; e2] => If (go e0) (go e1) (go e2)
     | GenNode 6 [e1; e2] => Pair (go e1) (go e2)
     | GenNode 7 [e] => Fst (go e)
     | GenNode 8 [e] => Snd (go e)
     | GenNode 9 [e] => InjL (go e)
     | GenNode 10 [e] => InjR (go e)
     | GenNode 11 [e0; e1; e2] => Case (go e0) (go e1) (go e2)
     | GenNode 12 [e] => Fork (go e)
Amin Timany's avatar
Amin Timany committed
321
     | GenNode 13 [e1; e2] => AllocN (go e1) (go e2)
322
323
324
325
326
     | GenNode 14 [e] => Load (go e)
     | GenNode 15 [e1; e2] => Store (go e1) (go e2)
     | GenNode 16 [e0; e1; e2] => CAS (go e0) (go e1) (go e2)
     | GenNode 17 [e1; e2] => FAA (go e1) (go e2)
     | GenNode 18 [] => NewProph
327
     | GenNode 19 [e0; e1; e2] => Resolve (go e0) (go e1) (go e2)
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
     | _ => Val $ LitV LitUnit (* dummy *)
     end
   with gov v :=
     match v with
     | GenLeaf (inr (inl l)) => LitV l
     | GenNode 0 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); e] => RecV f x (go e)
     | GenNode 1 [v1; v2] => PairV (gov v1) (gov v2)
     | GenNode 2 [v] => InjLV (gov v)
     | GenNode 3 [v] => InjRV (gov v)
     | _ => LitV LitUnit (* dummy *)
     end
   for go).
 refine (inj_countable' enc dec _).
 refine (fix go (e : expr) {struct e} := _ with gov (v : val) {struct v} := _ for go).
 - destruct e as [v| | | | | | | | | | | | | | | | | | | |]; simpl; f_equal;
     [exact (gov v)|done..].
 - destruct v; by f_equal.
345
346
347
348
Qed.
Instance val_countable : Countable val.
Proof. refine (inj_countable of_val to_val _); auto using to_of_val. Qed.

Ralf Jung's avatar
Ralf Jung committed
349
Instance state_inhabited : Inhabited state :=
350
  populate {| heap := inhabitant; used_proph_id := inhabitant |}.
351
Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
352
Instance expr_inhabited : Inhabited expr := populate (Val inhabitant).
353
354

Canonical Structure stateC := leibnizC state.
355
Canonical Structure locC := leibnizC loc.
356
357
358
Canonical Structure valC := leibnizC val.
Canonical Structure exprC := leibnizC expr.

359
(** Evaluation contexts *)
360
Inductive ectx_item :=
361
362
  | AppLCtx (v2 : val)
  | AppRCtx (e1 : expr)
363
  | UnOpCtx (op : un_op)
364
365
  | BinOpLCtx (op : bin_op) (v2 : val)
  | BinOpRCtx (op : bin_op) (e1 : expr)
366
  | IfCtx (e1 e2 : expr)
367
368
  | PairLCtx (v2 : val)
  | PairRCtx (e1 : expr)
369
370
371
372
  | FstCtx
  | SndCtx
  | InjLCtx
  | InjRCtx
373
  | CaseCtx (e1 : expr) (e2 : expr)
Amin Timany's avatar
Amin Timany committed
374
375
  | AllocNLCtx (v2 : val)
  | AllocNRCtx (e1 : expr)
376
  | LoadCtx
377
378
379
380
381
382
  | StoreLCtx (v2 : val)
  | StoreRCtx (e1 : expr)
  | CasLCtx (v1 : val) (v2 : val)
  | CasMCtx (e0 : expr) (v2 : val)
  | CasRCtx (e0 : expr) (e1 : expr)
  | FaaLCtx (v2 : val)
383
  | FaaRCtx (e1 : expr)
384
385
386
387
388
389
390
391
392
393
394
395
  | ResolveLCtx (ctx : ectx_item) (v1 : val) (v2 : val)
  | ResolveMCtx (e0 : expr) (v2 : val)
  | ResolveRCtx (e0 : expr) (e1 : expr).

(** Contextual closure will only reduce [e] in [Resolve e (Val _) (Val _)] if
the local context of [e] is non-empty. As a consequence, the first argument of
[Resolve] is not completely evaluated (down to a value) by contextual closure:
no head steps (i.e., surface reductions) are taken. This means that contextual
closure will reduce [Resolve (CAS #l #n (#n + #1)) #p #v] into [Resolve (CAS
#l #n #(n+1)) #p #v], but it cannot context-step any further. *)

Fixpoint fill_item (Ki : ectx_item) (e : expr) : expr :=
396
  match Ki with
397
398
  | AppLCtx v2 => App e (of_val v2)
  | AppRCtx e1 => App e1 e
399
  | UnOpCtx op => UnOp op e
400
  | BinOpLCtx op v2 => BinOp op e (Val v2)
401
  | BinOpRCtx op e1 => BinOp op e1 e
402
  | IfCtx e1 e2 => If e e1 e2
403
  | PairLCtx v2 => Pair e (Val v2)
404
  | PairRCtx e1 => Pair e1 e
405
406
407
408
  | FstCtx => Fst e
  | SndCtx => Snd e
  | InjLCtx => InjL e
  | InjRCtx => InjR e
409
  | CaseCtx e1 e2 => Case e e1 e2
Amin Timany's avatar
Amin Timany committed
410
411
  | AllocNLCtx v2 => AllocN e (Val v2)
  | AllocNRCtx e1 => AllocN e1 e
412
  | LoadCtx => Load e
413
  | StoreLCtx v2 => Store e (Val v2)
414
  | StoreRCtx e1 => Store e1 e
415
416
  | CasLCtx v1 v2 => CAS e (Val v1) (Val v2)
  | CasMCtx e0 v2 => CAS e0 e (Val v2)
417
  | CasRCtx e0 e1 => CAS e0 e1 e
418
  | FaaLCtx v2 => FAA e (Val v2)
419
  | FaaRCtx e1 => FAA e1 e
420
421
422
  | ResolveLCtx K v1 v2 => Resolve (fill_item K e) (Val v1) (Val v2)
  | ResolveMCtx ex v2 => Resolve ex e (Val v2)
  | ResolveRCtx ex e1 => Resolve ex e1 e
Ralf Jung's avatar
Ralf Jung committed
423
424
  end.

425
(** Substitution *)
426
Fixpoint subst (x : string) (v : val) (e : expr)  : expr :=
427
  match e with
428
429
  | Val _ => e
  | Var y => if decide (x = y) then Val v else Var y
430
  | Rec f y e =>
431
432
433
434
435
436
437
438
439
440
441
442
     Rec f y $ if decide (BNamed x  f  BNamed x  y) then subst x v e else e
  | App e1 e2 => App (subst x v e1) (subst x v e2)
  | UnOp op e => UnOp op (subst x v e)
  | BinOp op e1 e2 => BinOp op (subst x v e1) (subst x v e2)
  | If e0 e1 e2 => If (subst x v e0) (subst x v e1) (subst x v e2)
  | Pair e1 e2 => Pair (subst x v e1) (subst x v e2)
  | Fst e => Fst (subst x v e)
  | Snd e => Snd (subst x v e)
  | InjL e => InjL (subst x v e)
  | InjR e => InjR (subst x v e)
  | Case e0 e1 e2 => Case (subst x v e0) (subst x v e1) (subst x v e2)
  | Fork e => Fork (subst x v e)
Amin Timany's avatar
Amin Timany committed
443
  | AllocN e1 e2 => AllocN (subst x v e1) (subst x v e2)
444
445
446
447
  | Load e => Load (subst x v e)
  | Store e1 e2 => Store (subst x v e1) (subst x v e2)
  | CAS e0 e1 e2 => CAS (subst x v e0) (subst x v e1) (subst x v e2)
  | FAA e1 e2 => FAA (subst x v e1) (subst x v e2)
448
  | NewProph => NewProph
449
  | Resolve ex e1 e2 => Resolve (subst x v ex) (subst x v e1) (subst x v e2)
450
  end.
451

452
453
Definition subst' (mx : binder) (v : val) : expr  expr :=
  match mx with BNamed x => subst x v | BAnon => id end.
454

455
(** The stepping relation *)
456
457
458
Definition un_op_eval (op : un_op) (v : val) : option val :=
  match op, v with
  | NegOp, LitV (LitBool b) => Some $ LitV $ LitBool (negb b)
459
  | NegOp, LitV (LitInt n) => Some $ LitV $ LitInt (Z.lnot n)
460
  | MinusUnOp, LitV (LitInt n) => Some $ LitV $ LitInt (- n)
461
462
463
  | _, _ => None
  end.

Amin Timany's avatar
Amin Timany committed
464
Definition bin_op_eval_int (op : bin_op) (n1 n2 : Z) : option base_lit :=
465
  match op with
Amin Timany's avatar
Amin Timany committed
466
467
468
469
470
471
472
473
474
475
476
477
478
479
  | PlusOp => Some $ LitInt (n1 + n2)
  | MinusOp => Some $ LitInt (n1 - n2)
  | MultOp => Some $ LitInt (n1 * n2)
  | QuotOp => Some $ LitInt (n1 `quot` n2)
  | RemOp => Some $ LitInt (n1 `rem` n2)
  | AndOp => Some $ LitInt (Z.land n1 n2)
  | OrOp => Some $ LitInt (Z.lor n1 n2)
  | XorOp => Some $ LitInt (Z.lxor n1 n2)
  | ShiftLOp => Some $ LitInt (n1  n2)
  | ShiftROp => Some $ LitInt (n1  n2)
  | LeOp => Some $ LitBool (bool_decide (n1  n2))
  | LtOp => Some $ LitBool (bool_decide (n1 < n2))
  | EqOp => Some $ LitBool (bool_decide (n1 = n2))
  | OffsetOp => None (* Pointer arithmetic *)
480
481
482
483
484
485
486
487
488
489
490
  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)))
Amin Timany's avatar
Amin Timany committed
491
  | OffsetOp => None (* Pointer arithmetic *)
492
493
  end.

494
Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
495
  if decide (op = EqOp) then Some $ LitV $ LitBool $ bool_decide (v1 = v2) else
496
  match v1, v2 with
Amin Timany's avatar
Amin Timany committed
497
  | LitV (LitInt n1), LitV (LitInt n2) => LitV <$> bin_op_eval_int op n1 n2
498
  | LitV (LitBool b1), LitV (LitBool b2) => LitV <$> bin_op_eval_bool op b1 b2
Amin Timany's avatar
Amin Timany committed
499
  | LitV (LitLoc l), LitV (LitInt off) => Some $ LitV $ LitLoc (l + off)
Robbert Krebbers's avatar
Robbert Krebbers committed
500
  | _, _ => None
501
502
  end.

503
504
505
506
(** 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
507
Definition vals_cas_compare_safe (vl v1 : val) : Prop :=
508
509
  val_is_unboxed vl  val_is_unboxed v1.
Arguments vals_cas_compare_safe !_ !_ /.
Ralf Jung's avatar
Ralf Jung committed
510

Ralf Jung's avatar
Ralf Jung committed
511
Definition state_upd_heap (f: gmap loc val  gmap loc val) (σ: state) : state :=
512
  {| heap := f σ.(heap); used_proph_id := σ.(used_proph_id) |}.
Ralf Jung's avatar
Ralf Jung committed
513
Arguments state_upd_heap _ !_ /.
Amin Timany's avatar
Amin Timany committed
514

Ralf Jung's avatar
Ralf Jung committed
515
Definition state_upd_used_proph_id (f: gset proph_id  gset proph_id) (σ: state) : state :=
516
517
  {| heap := σ.(heap); used_proph_id := f σ.(used_proph_id) |}.
Arguments state_upd_used_proph_id _ !_ /.
Ralf Jung's avatar
Ralf Jung committed
518

Amin Timany's avatar
Amin Timany committed
519
520
521
522
523
524
525
526
527
528
529
530
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
Fixpoint heap_array (l : loc) (vs : list val) : gmap loc val :=
  match vs with
  | [] => 
  | v :: vs' => {[l := v]}  heap_array (l + 1) vs'
  end.

Lemma heap_array_singleton l v : heap_array l [v] = {[l := v]}.
Proof. by rewrite /heap_array right_id. Qed.

Lemma heap_array_lookup l vs w k :
  heap_array l vs !! k = Some w 
   j, 0  j  k = l + j  vs !! (Z.to_nat j) = Some w.
Proof.
  revert k l; induction vs as [|v' vs IH]=> l' l /=.
  { rewrite lookup_empty. naive_solver lia. }
  rewrite -insert_union_singleton_l lookup_insert_Some IH. split.
  - intros [[-> ->] | (Hl & j & ? & -> & ?)].
    { exists 0. rewrite loc_add_0. naive_solver lia. }
    exists (1 + j). rewrite loc_add_assoc !Z.add_1_l Z2Nat.inj_succ; auto with lia.
  - intros (j & ? & -> & Hil). destruct (decide (j = 0)); simplify_eq/=.
    { rewrite loc_add_0; eauto. }
    right. split.
    { rewrite -{1}(loc_add_0 l). intros ?%(inj _); lia. }
    assert (Z.to_nat j = S (Z.to_nat (j - 1))) as Hj.
    { rewrite -Z2Nat.inj_succ; last lia. f_equal; lia. }
    rewrite Hj /= in Hil.
    exists (j - 1). rewrite loc_add_assoc Z.add_sub_assoc Z.add_simpl_l.
    auto with lia.
Qed.

Lemma heap_array_map_disjoint (h : gmap loc val) (l : loc) (vs : list val) :
  ( i, (0  i)  (i < length vs)  h !! (l + i) = None) 
  (heap_array l vs) ## h.
Proof.
  intros Hdisj. apply map_disjoint_spec=> l' v1 v2.
  intros (j&?&->&Hj%lookup_lt_Some%inj_lt)%heap_array_lookup.
  move: Hj. rewrite Z2Nat.id // => ?. by rewrite Hdisj.
Qed.

558
(* [h] is added on the right here to make [state_init_heap_singleton] true. *)
Amin Timany's avatar
Amin Timany committed
559
Definition state_init_heap (l : loc) (n : Z) (v : val) (σ : state) : state :=
560
561
562
563
564
565
566
567
  state_upd_heap (λ h, heap_array l (replicate (Z.to_nat n) v)  h) σ.

Lemma state_init_heap_singleton l v σ :
  state_init_heap l 1 v σ = state_upd_heap <[l:=v]> σ.
Proof.
  destruct σ as [h p]. rewrite /state_init_heap /=. f_equiv.
  rewrite right_id insert_union_singleton_l. done.
Qed.
Amin Timany's avatar
Amin Timany committed
568

Robbert Krebbers's avatar
Robbert Krebbers committed
569
Inductive head_step : expr  state  list observation  expr  state  list expr  Prop :=
570
571
572
573
574
575
576
577
578
579
580
581
  | RecS f x e σ :
     head_step (Rec f x e) σ [] (Val $ RecV f x e) σ []
  | PairS v1 v2 σ :
     head_step (Pair (Val v1) (Val v2)) σ [] (Val $ PairV v1 v2) σ []
  | InjLS v σ :
     head_step (InjL $ Val v) σ [] (Val $ InjLV v) σ []
  | InjRS v σ :
     head_step (InjR $ Val v) σ [] (Val $ InjRV v) σ []
  | BetaS f x e1 v2 e' σ :
     e' = subst' x v2 (subst' f (RecV f x e1) e1) 
     head_step (App (Val $ RecV f x e1) (Val v2)) σ [] e' σ []
  | UnOpS op v v' σ :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
582
     un_op_eval op v = Some v' 
583
584
     head_step (UnOp op (Val v)) σ [] (Val v') σ []
  | BinOpS op v1 v2 v' σ :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
585
     bin_op_eval op v1 v2 = Some v' 
586
     head_step (BinOp op (Val v1) (Val v2)) σ [] (Val v') σ []
587
  | IfTrueS e1 e2 σ :
588
     head_step (If (Val $ LitV $ LitBool true) e1 e2) σ [] e1 σ []
589
  | IfFalseS e1 e2 σ :
590
591
592
593
594
595
596
597
598
     head_step (If (Val $ LitV $ LitBool false) e1 e2) σ [] e2 σ []
  | FstS v1 v2 σ :
     head_step (Fst (Val $ PairV v1 v2)) σ [] (Val v1) σ []
  | SndS v1 v2 σ :
     head_step (Snd (Val $ PairV v1 v2)) σ [] (Val v2) σ []
  | CaseLS v e1 e2 σ :
     head_step (Case (Val $ InjLV v) e1 e2) σ [] (App e1 (Val v)) σ []
  | CaseRS v e1 e2 σ :
     head_step (Case (Val $ InjRV v) e1 e2) σ [] (App e2 (Val v)) σ []
599
  | ForkS e σ:
600
     head_step (Fork e) σ [] (Val $ LitV LitUnit) σ [e]
Amin Timany's avatar
Amin Timany committed
601
602
603
604
  | AllocNS n v σ l :
     0 < n 
     ( i, 0  i  i < n  σ.(heap) !! (l + i) = None) 
     head_step (AllocN (Val $ LitV $ LitInt n) (Val v)) σ
605
               []
Amin Timany's avatar
Amin Timany committed
606
               (Val $ LitV $ LitLoc l) (state_init_heap l n v σ)
Ralf Jung's avatar
Ralf Jung committed
607
               []
608
  | LoadS l v σ :
Ralf Jung's avatar
Ralf Jung committed
609
     σ.(heap) !! l = Some v 
610
611
612
613
     head_step (Load (Val $ LitV $ LitLoc l)) σ [] (of_val v) σ []
  | StoreS l v σ :
     is_Some (σ.(heap) !! l) 
     head_step (Store (Val $ LitV $ LitLoc l) (Val v)) σ
614
               []
615
               (Val $ LitV LitUnit) (state_upd_heap <[l:=v]> σ)
Ralf Jung's avatar
Ralf Jung committed
616
               []
617
  | CasFailS l v1 v2 vl σ :
Ralf Jung's avatar
Ralf Jung committed
618
     σ.(heap) !! l = Some vl  vl  v1 
Ralf Jung's avatar
Ralf Jung committed
619
     vals_cas_compare_safe vl v1 
620
621
622
     head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ []
               (Val $ LitV $ LitBool false) σ []
  | CasSucS l v1 v2 σ :
Ralf Jung's avatar
Ralf Jung committed
623
     σ.(heap) !! l = Some v1 
Ralf Jung's avatar
Ralf Jung committed
624
     vals_cas_compare_safe v1 v1 
625
     head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
626
               []
627
               (Val $ LitV $ LitBool true) (state_upd_heap <[l:=v2]> σ)
Ralf Jung's avatar
Ralf Jung committed
628
               []
629
  | FaaS l i1 i2 σ :
Ralf Jung's avatar
Ralf Jung committed
630
     σ.(heap) !! l = Some (LitV (LitInt i1)) 
631
     head_step (FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2)) σ
632
               []
633
               (Val $ LitV $ LitInt i1) (state_upd_heap <[l:=LitV (LitInt (i1 + i2))]>σ)
Ralf Jung's avatar
Ralf Jung committed
634
               []
635
  | NewProphS σ p :
636
     p  σ.(used_proph_id) 
Ralf Jung's avatar
Ralf Jung committed
637
     head_step NewProph σ
638
               []
639
               (Val $ LitV $ LitProphecy p) (state_upd_used_proph_id ({[ p ]} ) σ)
Ralf Jung's avatar
Ralf Jung committed
640
               []
641
642
643
644
  | ResolveS p v e σ w σ' κs ts :
     head_step e σ κs (Val v) σ' ts 
     head_step (Resolve e (Val $ LitV $ LitProphecy p) (Val w)) σ
               (κs ++ [(p, (v, w))]) (Val v) σ' ts.
Ralf Jung's avatar
Ralf Jung committed
645

646
(** Basic properties about the language *)
647
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
648
Proof. induction Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
649

650
651
Lemma fill_item_val Ki e :
  is_Some (to_val (fill_item Ki e))  is_Some (to_val e).
652
Proof. intros [v ?]. induction Ki; simplify_option_eq; eauto. Qed.
653

654
Lemma val_head_stuck e1 σ1 κ e2 σ2 efs : head_step e1 σ1 κ e2 σ2 efs  to_val e1 = None.
655
Proof. destruct 1; naive_solver. Qed.
656

657
658
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).
659
Proof. revert κ e2. induction Ki; inversion_clear 1; simplify_option_eq; eauto. Qed.
660

661
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
662
  to_val e1 = None  to_val e2 = None 
663
  fill_item Ki1 e1 = fill_item Ki2 e2  Ki1 = Ki2.
664
Proof. revert Ki1. induction Ki2, Ki1; naive_solver eauto with f_equal. Qed.
665

Amin Timany's avatar
Amin Timany committed
666
667
668
669
670
671
672
673
674
675
676
Lemma alloc_fresh v n σ :
  let l := fresh_locs (dom (gset loc) σ.(heap)) n in
  0 < n 
  head_step (AllocN ((Val $ LitV $ LitInt $ n)) (Val v)) σ []
            (Val $ LitV $ LitLoc l) (state_init_heap l n v σ) [].
Proof.
  intros.
  apply AllocNS; first done.
  intros. apply (not_elem_of_dom (D := gset loc)).
  by apply fresh_locs_fresh.
Qed.
677

678
679
Lemma new_proph_id_fresh σ :
  let p := fresh σ.(used_proph_id) in
680
  head_step NewProph σ [] (Val $ LitV $ LitProphecy p) (state_upd_used_proph_id ({[ p ]} ) σ) [].
681
682
Proof. constructor. apply is_fresh. Qed.

683
684
685
686
687
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.
688
689
690
End heap_lang.

(** Language *)
691
692
693
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.
694

695
(* Prefer heap_lang names over ectx_language names. *)
696
Export heap_lang.
697

698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
(* The following lemma is not provable using the axioms of [ectxi_language].
The proof requires a case analysis over context items ([destruct i] on the
last line), which in all cases yields a non-value. To prove this lemma for
[ectxi_language] in general, we would require that a term of the form
[fill_item i e] is never a value. *)
Lemma to_val_fill_some K e v : to_val (fill K e) = Some v  K = []  e = Val v.
Proof.
  intro H. destruct K as [|Ki K]; first by apply of_to_val in H. exfalso.
  assert (to_val e  None) as He.
  { intro A. by rewrite fill_not_val in H. }
  assert ( w, e = Val w) as [w ->].
  { destruct e; try done; eauto. }
  assert (to_val (fill (Ki :: K) (Val w)) = None).
  { destruct Ki; simpl; apply fill_not_val; done. }
  by simplify_eq.
Qed.

Lemma prim_step_to_val_is_head_step e σ1 κs w σ2 efs :
  prim_step e σ1 κs (Val w) σ2 efs  head_step e σ1 κs (Val w) σ2 efs.
Proof.
  intro H. destruct H as [K e1 e2 H1 H2].
  assert (to_val (fill K e2) = Some w) as H3; first by rewrite -H2.
  apply to_val_fill_some in H3 as [-> ->]. subst e. done.
Qed.

Lemma irreducible_resolve e v1 v2 σ :
  irreducible e σ  irreducible (Resolve e (Val v1) (Val v2)) σ.
Proof.
  intros H κs ** [Ks e1' e2' Hfill -> step]. simpl in *.
  induction Ks as [|K Ks _] using rev_ind; simpl in Hfill.
  - subst e1'. inversion step. eapply H. by apply head_prim_step.
  - rewrite fill_app /= in Hfill.
    destruct K; (inversion Hfill; subst; clear Hfill; try
      match goal with | H : Val ?v = fill Ks ?e |- _ =>
        (assert (to_val (fill Ks e) = Some v) as HEq by rewrite -H //);
        apply to_val_fill_some in HEq; destruct HEq as [-> ->]; inversion step
      end).
    apply (H κs (fill_item K (foldl (flip fill_item) e2' Ks)) σ' efs).
    econstructor 1 with (K := Ks ++ [K]); last done; simpl; by rewrite fill_app.
Qed.