lang.v 30.3 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
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,
Ralf Jung's avatar
Ralf Jung committed
31
32
33
34
35
to distinguish a resolution originating from a successful [CmpXchg] from one
originating from a failing [CmpXchg]. For example:
 - [Resolve (CmpXchg #l #n #(n+1)) #p v] will behave as [CmpXchg #l #n #(n+1)],
   which means step to a value-boole pair [(n', b)] while updating the heap, but
   in the meantime the prophecy variable [p] will be resolved to [(n', b), v)].
36
37
38
39
40
41
42
43
 - [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:
Ralf Jung's avatar
Ralf Jung committed
44
45
 - [Resolve (CmpXchg #l #n (#n + #1)) #p v] will first be reduced (with by a
   context-step) to [Resolve (CmpXchg #l #n #(n+1) #p v], and then behave as
46
   described above.
Ralf Jung's avatar
Ralf Jung committed
47
 - However, [Resolve ((λ: "n", CmpXchg #l "n" ("n" + #1)) #n) #p v] is stuck.
48
49
50
51
52
   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
  | LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitErased
65
  | 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)
Ralf Jung's avatar
Ralf Jung committed
100
  | CmpXchg (e0 : expr) (e1 : expr) (e2 : expr) (* Compare-exchange *)
101
  | FAA (e1 : expr) (e2 : expr) (* Fetch-and-add *)
102
103
  (* 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
(** 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
Ralf Jung's avatar
Ralf Jung committed
118
wrapped operation is a CmpXchg). The second value is the one that the prophecy
119
120
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
(** 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. *)
154
155
Definition lit_is_unboxed (l: base_lit) : Prop :=
  match l with
Ralf Jung's avatar
Ralf Jung committed
156
157
  (** Disallow comparing (erased) prophecies with (erased) prophecies, by
  considering them boxed. *)
158
159
160
  | LitProphecy _ | LitErased => False
  | _ => True
  end.
161
162
Definition val_is_unboxed (v : val) : Prop :=
  match v with
163
164
165
  | LitV l => lit_is_unboxed l
  | InjLV (LitV l) => lit_is_unboxed l
  | InjRV (LitV l) => lit_is_unboxed l
166
167
168
  | _ => False
  end.

169
170
171
172
173
174
175
Instance lit_is_unboxed_dec l : Decision (lit_is_unboxed l).
Proof. destruct l; simpl; exact (decide _). Defined.
Instance val_is_unboxed_dec v : Decision (val_is_unboxed v).
Proof. destruct v as [ | | | [] | [] ]; simpl; exact (decide _). Defined.

(** We just compare the word-sized representation of two values, without looking
into boxed data.  This works out fine if at least one of the to-be-compared
176
177
values is unboxed (exploiting the fact that an unboxed and a boxed value can
never be equal because these are disjoint sets). *)
178
Definition vals_compare_safe (vl v1 : val) : Prop :=
179
  val_is_unboxed vl  val_is_unboxed v1.
180
Arguments vals_compare_safe !_ !_ /.
181

182
(** The state: heaps of vals. *)
Ralf Jung's avatar
Ralf Jung committed
183
184
Record state : Type := {
  heap: gmap loc val;
185
  used_proph_id: gset proph_id;
Ralf Jung's avatar
Ralf Jung committed
186
}.
Ralf Jung's avatar
Ralf Jung committed
187

188
189
(** Equality and other typeclass stuff *)
Lemma to_of_val v : to_val (of_val v) = Some v.
190
Proof. by destruct v. Qed.
191
192

Lemma of_to_val e v : to_val e = Some v  of_val v = e.
193
Proof. destruct e=>//=. by intros [= <-]. Qed.
194
195

Instance of_val_inj : Inj (=) (=) of_val.
196
Proof. intros ??. congruence. Qed.
197

198
Instance base_lit_eq_dec : EqDecision base_lit.
199
Proof. solve_decision. Defined.
200
Instance un_op_eq_dec : EqDecision un_op.
201
Proof. solve_decision. Defined.
202
Instance bin_op_eq_dec : EqDecision bin_op.
203
Proof. solve_decision. Defined.
204
Instance expr_eq_dec : EqDecision expr.
205
Proof.
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
  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
228
229
     | AllocN e1 e2, AllocN e1' e2' =>
        cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
230
231
232
     | Load e, Load e' => cast_if (decide (e = e'))
     | Store e1 e2, Store e1' e2' =>
        cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
Ralf Jung's avatar
Ralf Jung committed
233
     | CmpXchg e0 e1 e2, CmpXchg e0' e1' e2' =>
234
235
236
237
        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 _
238
239
     | Resolve e0 e1 e2, Resolve e0' e1' e2' =>
        cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
240
241
242
243
244
245
246
247
248
249
250
251
252
253
     | _, _ => 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).
254
Defined.
255
256
Instance val_eq_dec : EqDecision val.
Proof. solve_decision. Defined.
257

258
259
260
Instance base_lit_countable : Countable base_lit.
Proof.
 refine (inj_countable' (λ l, match l with
261
262
263
264
265
266
  | LitInt n => (inl (inl n), None)
  | LitBool b => (inl (inr b), None)
  | LitUnit => (inr (inl false), None)
  | LitErased => (inr (inl true), None)
  | LitLoc l => (inr (inr l), None)
  | LitProphecy p => (inr (inl false), Some p)
267
  end) (λ l, match l with
268
269
270
271
272
  | (inl (inl n), None) => LitInt n
  | (inl (inr b), None) => LitBool b
  | (inr (inl false), None) => LitUnit
  | (inr (inl true), None) => LitErased
  | (inr (inr l), None) => LitLoc l
273
  | (_, Some p) => LitProphecy p
274
275
276
277
278
279
280
281
282
283
  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
284
285
  | 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
286
  | LeOp => 10 | LtOp => 11 | EqOp => 12 | OffsetOp => 13
287
  end) (λ n, match n with
288
289
  | 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
290
  | 10 => LeOp | 11 => LtOp | 12 => EqOp | _ => OffsetOp
291
292
293
294
  end) _); by intros [].
Qed.
Instance expr_countable : Countable expr.
Proof.
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
 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
312
     | AllocN e1 e2 => GenNode 13 [go e1; go e2]
313
314
     | Load e => GenNode 14 [go e]
     | Store e1 e2 => GenNode 15 [go e1; go e2]
Ralf Jung's avatar
Ralf Jung committed
315
     | CmpXchg e0 e1 e2 => GenNode 16 [go e0; go e1; go e2]
316
317
     | FAA e1 e2 => GenNode 17 [go e1; go e2]
     | NewProph => GenNode 18 []
318
     | Resolve e0 e1 e2 => GenNode 19 [go e0; go e1; go e2]
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
     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
347
     | GenNode 13 [e1; e2] => AllocN (go e1) (go e2)
348
349
     | GenNode 14 [e] => Load (go e)
     | GenNode 15 [e1; e2] => Store (go e1) (go e2)
Ralf Jung's avatar
Ralf Jung committed
350
     | GenNode 16 [e0; e1; e2] => CmpXchg (go e0) (go e1) (go e2)
351
352
     | GenNode 17 [e1; e2] => FAA (go e1) (go e2)
     | GenNode 18 [] => NewProph
353
     | GenNode 19 [e0; e1; e2] => Resolve (go e0) (go e1) (go e2)
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
     | _ => 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.
371
372
373
374
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
375
Instance state_inhabited : Inhabited state :=
376
  populate {| heap := inhabitant; used_proph_id := inhabitant |}.
377
Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
378
Instance expr_inhabited : Inhabited expr := populate (Val inhabitant).
379

380
381
382
383
Canonical Structure stateO := leibnizO state.
Canonical Structure locO := leibnizO loc.
Canonical Structure valO := leibnizO val.
Canonical Structure exprO := leibnizO expr.
384

385
(** Evaluation contexts *)
386
Inductive ectx_item :=
387
388
  | AppLCtx (v2 : val)
  | AppRCtx (e1 : expr)
389
  | UnOpCtx (op : un_op)
390
391
  | BinOpLCtx (op : bin_op) (v2 : val)
  | BinOpRCtx (op : bin_op) (e1 : expr)
392
  | IfCtx (e1 e2 : expr)
393
394
  | PairLCtx (v2 : val)
  | PairRCtx (e1 : expr)
395
396
397
398
  | FstCtx
  | SndCtx
  | InjLCtx
  | InjRCtx
399
  | CaseCtx (e1 : expr) (e2 : expr)
Amin Timany's avatar
Amin Timany committed
400
401
  | AllocNLCtx (v2 : val)
  | AllocNRCtx (e1 : expr)
402
  | LoadCtx
403
404
  | StoreLCtx (v2 : val)
  | StoreRCtx (e1 : expr)
Ralf Jung's avatar
Ralf Jung committed
405
406
407
  | CmpXchgLCtx (v1 : val) (v2 : val)
  | CmpXchgMCtx (e0 : expr) (v2 : val)
  | CmpXchgRCtx (e0 : expr) (e1 : expr)
408
  | FaaLCtx (v2 : val)
409
  | FaaRCtx (e1 : expr)
410
411
412
413
414
415
416
417
  | 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
Ralf Jung's avatar
Ralf Jung committed
418
419
closure will reduce [Resolve (CmpXchg #l #n (#n + #1)) #p #v] into [Resolve
(CmpXchg #l #n #(n+1)) #p #v], but it cannot context-step any further. *)
420
421

Fixpoint fill_item (Ki : ectx_item) (e : expr) : expr :=
422
  match Ki with
423
424
  | AppLCtx v2 => App e (of_val v2)
  | AppRCtx e1 => App e1 e
425
  | UnOpCtx op => UnOp op e
426
  | BinOpLCtx op v2 => BinOp op e (Val v2)
427
  | BinOpRCtx op e1 => BinOp op e1 e
428
  | IfCtx e1 e2 => If e e1 e2
429
  | PairLCtx v2 => Pair e (Val v2)
430
  | PairRCtx e1 => Pair e1 e
431
432
433
434
  | FstCtx => Fst e
  | SndCtx => Snd e
  | InjLCtx => InjL e
  | InjRCtx => InjR e
435
  | CaseCtx e1 e2 => Case e e1 e2
Amin Timany's avatar
Amin Timany committed
436
437
  | AllocNLCtx v2 => AllocN e (Val v2)
  | AllocNRCtx e1 => AllocN e1 e
438
  | LoadCtx => Load e
439
  | StoreLCtx v2 => Store e (Val v2)
440
  | StoreRCtx e1 => Store e1 e
Ralf Jung's avatar
Ralf Jung committed
441
442
443
  | CmpXchgLCtx v1 v2 => CmpXchg e (Val v1) (Val v2)
  | CmpXchgMCtx e0 v2 => CmpXchg e0 e (Val v2)
  | CmpXchgRCtx e0 e1 => CmpXchg e0 e1 e
444
  | FaaLCtx v2 => FAA e (Val v2)
445
  | FaaRCtx e1 => FAA e1 e
446
447
448
  | 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
449
450
  end.

451
(** Substitution *)
452
Fixpoint subst (x : string) (v : val) (e : expr)  : expr :=
453
  match e with
454
455
  | Val _ => e
  | Var y => if decide (x = y) then Val v else Var y
456
  | Rec f y e =>
457
458
459
460
461
462
463
464
465
466
467
468
     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
469
  | AllocN e1 e2 => AllocN (subst x v e1) (subst x v e2)
470
471
  | Load e => Load (subst x v e)
  | Store e1 e2 => Store (subst x v e1) (subst x v e2)
Ralf Jung's avatar
Ralf Jung committed
472
  | CmpXchg e0 e1 e2 => CmpXchg (subst x v e0) (subst x v e1) (subst x v e2)
473
  | FAA e1 e2 => FAA (subst x v e1) (subst x v e2)
474
  | NewProph => NewProph
475
  | Resolve ex e1 e2 => Resolve (subst x v ex) (subst x v e1) (subst x v e2)
476
  end.
477

478
479
Definition subst' (mx : binder) (v : val) : expr  expr :=
  match mx with BNamed x => subst x v | BAnon => id end.
480

481
(** The stepping relation *)
482
483
484
Definition un_op_eval (op : un_op) (v : val) : option val :=
  match op, v with
  | NegOp, LitV (LitBool b) => Some $ LitV $ LitBool (negb b)
485
  | NegOp, LitV (LitInt n) => Some $ LitV $ LitInt (Z.lnot n)
486
  | MinusUnOp, LitV (LitInt n) => Some $ LitV $ LitInt (- n)
487
488
489
  | _, _ => None
  end.

Amin Timany's avatar
Amin Timany committed
490
Definition bin_op_eval_int (op : bin_op) (n1 n2 : Z) : option base_lit :=
491
  match op with
Amin Timany's avatar
Amin Timany committed
492
493
494
495
496
497
498
499
500
501
502
503
504
505
  | 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 *)
506
507
508
509
510
511
512
513
514
515
516
  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
517
  | OffsetOp => None (* Pointer arithmetic *)
518
519
  end.

520
Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
521
  if decide (op = EqOp) then
Ralf Jung's avatar
Ralf Jung committed
522
    (* Crucially, this compares the same way as [CmpXchg]! *)
523
    if decide (vals_compare_safe v1 v2) then
524
525
526
      Some $ LitV $ LitBool $ bool_decide (v1 = v2)
    else
      None
527
528
529
530
531
532
533
  else
    match v1, v2 with
    | LitV (LitInt n1), LitV (LitInt n2) => LitV <$> bin_op_eval_int op n1 n2
    | LitV (LitBool b1), LitV (LitBool b2) => LitV <$> bin_op_eval_bool op b1 b2
    | LitV (LitLoc l), LitV (LitInt off) => Some $ LitV $ LitLoc (l + off)
    | _, _ => None
    end.
Ralf Jung's avatar
Ralf Jung committed
534

Ralf Jung's avatar
Ralf Jung committed
535
Definition state_upd_heap (f: gmap loc val  gmap loc val) (σ: state) : state :=
536
  {| heap := f σ.(heap); used_proph_id := σ.(used_proph_id) |}.
Ralf Jung's avatar
Ralf Jung committed
537
Arguments state_upd_heap _ !_ /.
Amin Timany's avatar
Amin Timany committed
538

Ralf Jung's avatar
Ralf Jung committed
539
Definition state_upd_used_proph_id (f: gset proph_id  gset proph_id) (σ: state) : state :=
540
541
  {| heap := σ.(heap); used_proph_id := f σ.(used_proph_id) |}.
Arguments state_upd_used_proph_id _ !_ /.
Ralf Jung's avatar
Ralf Jung committed
542

Amin Timany's avatar
Amin Timany committed
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
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.

582
(* [h] is added on the right here to make [state_init_heap_singleton] true. *)
Amin Timany's avatar
Amin Timany committed
583
Definition state_init_heap (l : loc) (n : Z) (v : val) (σ : state) : state :=
584
585
586
587
588
589
590
591
  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
592

Robbert Krebbers's avatar
Robbert Krebbers committed
593
Inductive head_step : expr  state  list observation  expr  state  list expr  Prop :=
594
595
596
597
598
599
600
601
602
603
604
605
  | 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
606
     un_op_eval op v = Some v' 
607
608
     head_step (UnOp op (Val v)) σ [] (Val v') σ []
  | BinOpS op v1 v2 v' σ :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
609
     bin_op_eval op v1 v2 = Some v' 
610
     head_step (BinOp op (Val v1) (Val v2)) σ [] (Val v') σ []
611
  | IfTrueS e1 e2 σ :
612
     head_step (If (Val $ LitV $ LitBool true) e1 e2) σ [] e1 σ []
613
  | IfFalseS e1 e2 σ :
614
615
616
617
618
619
620
621
622
     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)) σ []
623
  | ForkS e σ:
624
     head_step (Fork e) σ [] (Val $ LitV LitUnit) σ [e]
Amin Timany's avatar
Amin Timany committed
625
626
627
628
  | AllocNS n v σ l :
     0 < n 
     ( i, 0  i  i < n  σ.(heap) !! (l + i) = None) 
     head_step (AllocN (Val $ LitV $ LitInt n) (Val v)) σ
629
               []
Amin Timany's avatar
Amin Timany committed
630
               (Val $ LitV $ LitLoc l) (state_init_heap l n v σ)
Ralf Jung's avatar
Ralf Jung committed
631
               []
632
  | LoadS l v σ :
Ralf Jung's avatar
Ralf Jung committed
633
     σ.(heap) !! l = Some v 
634
635
636
637
     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)) σ
638
               []
639
               (Val $ LitV LitUnit) (state_upd_heap <[l:=v]> σ)
Ralf Jung's avatar
Ralf Jung committed
640
               []
Ralf Jung's avatar
Ralf Jung committed
641
  | CmpXchgS l v1 v2 vl σ b :
642
     σ.(heap) !! l = Some vl 
643
     (* Crucially, this compares the same way as [EqOp]! *)
644
645
     vals_compare_safe vl v1 
     b = bool_decide (vl = v1) 
Ralf Jung's avatar
Ralf Jung committed
646
     head_step (CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
647
               []
Ralf Jung's avatar
Ralf Jung committed
648
               (Val $ PairV vl (LitV $ LitBool b)) (if b then state_upd_heap <[l:=v2]> σ else σ)
Ralf Jung's avatar
Ralf Jung committed
649
               []
650
  | FaaS l i1 i2 σ :
Ralf Jung's avatar
Ralf Jung committed
651
     σ.(heap) !! l = Some (LitV (LitInt i1)) 
652
     head_step (FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2)) σ
653
               []
654
               (Val $ LitV $ LitInt i1) (state_upd_heap <[l:=LitV (LitInt (i1 + i2))]>σ)
Ralf Jung's avatar
Ralf Jung committed
655
               []
656
  | NewProphS σ p :
657
     p  σ.(used_proph_id) 
Ralf Jung's avatar
Ralf Jung committed
658
     head_step NewProph σ
659
               []
660
               (Val $ LitV $ LitProphecy p) (state_upd_used_proph_id ({[ p ]} ) σ)
Ralf Jung's avatar
Ralf Jung committed
661
               []
662
663
664
665
  | 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
666

667
(** Basic properties about the language *)
668
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
669
Proof. induction Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
670

671
672
Lemma fill_item_val Ki e :
  is_Some (to_val (fill_item Ki e))  is_Some (to_val e).
673
Proof. intros [v ?]. induction Ki; simplify_option_eq; eauto. Qed.
674

675
Lemma val_head_stuck e1 σ1 κ e2 σ2 efs : head_step e1 σ1 κ e2 σ2 efs  to_val e1 = None.
676
Proof. destruct 1; naive_solver. Qed.
677

678
679
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).
680
Proof. revert κ e2. induction Ki; inversion_clear 1; simplify_option_eq; eauto. Qed.
681

682
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
683
  to_val e1 = None  to_val e2 = None 
684
  fill_item Ki1 e1 = fill_item Ki2 e2  Ki1 = Ki2.
685
Proof. revert Ki1. induction Ki2, Ki1; naive_solver eauto with f_equal. Qed.
686

Amin Timany's avatar
Amin Timany committed
687
688
689
690
691
692
693
694
695
696
697
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.
698

699
700
Lemma new_proph_id_fresh σ :
  let p := fresh σ.(used_proph_id) in
701
  head_step NewProph σ [] (Val $ LitV $ LitProphecy p) (state_upd_used_proph_id ({[ p ]} ) σ) [].
702
703
Proof. constructor. apply is_fresh. Qed.

704
705
706
707
708
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.
709
710
711
End heap_lang.

(** Language *)
712
713
714
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.
715

716
(* Prefer heap_lang names over ectx_language names. *)
717
Export heap_lang.
718

719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
(* 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.