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 156 157 158 159
Definition lit_is_unboxed (l: base_lit) : Prop :=
  match l with
  (* disallow comparing (erased) prophecies with (erased) prophecies, by considering them boxed *)
  | LitProphecy _ | LitErased => False
  | _ => True
  end.
160 161
Definition val_is_unboxed (v : val) : Prop :=
  match v with
162 163 164
  | LitV l => lit_is_unboxed l
  | InjLV (LitV l) => lit_is_unboxed l
  | InjRV (LitV l) => lit_is_unboxed l
165 166 167
  | _ => False
  end.

168 169 170 171 172 173 174
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
175 176
values is unboxed (exploiting the fact that an unboxed and a boxed value can
never be equal because these are disjoint sets). *)
177
Definition vals_compare_safe (vl v1 : val) : Prop :=
178
  val_is_unboxed vl  val_is_unboxed v1.
179
Arguments vals_compare_safe !_ !_ /.
180

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

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

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

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

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

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

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

384
(** Evaluation contexts *)
385
Inductive ectx_item :=
386 387
  | AppLCtx (v2 : val)
  | AppRCtx (e1 : expr)
388
  | UnOpCtx (op : un_op)
389 390
  | BinOpLCtx (op : bin_op) (v2 : val)
  | BinOpRCtx (op : bin_op) (e1 : expr)
391
  | IfCtx (e1 e2 : expr)
392 393
  | PairLCtx (v2 : val)
  | PairRCtx (e1 : expr)
394 395 396 397
  | FstCtx
  | SndCtx
  | InjLCtx
  | InjRCtx
398
  | CaseCtx (e1 : expr) (e2 : expr)
Amin Timany's avatar
Amin Timany committed
399 400
  | AllocNLCtx (v2 : val)
  | AllocNRCtx (e1 : expr)
401
  | LoadCtx
402 403
  | StoreLCtx (v2 : val)
  | StoreRCtx (e1 : expr)
Ralf Jung's avatar
Ralf Jung committed
404 405 406
  | CmpXchgLCtx (v1 : val) (v2 : val)
  | CmpXchgMCtx (e0 : expr) (v2 : val)
  | CmpXchgRCtx (e0 : expr) (e1 : expr)
407
  | FaaLCtx (v2 : val)
408
  | FaaRCtx (e1 : expr)
409 410 411 412 413 414 415 416
  | 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
417 418
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. *)
419 420

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

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

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

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

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

519
Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
520
  if decide (op = EqOp) then
Ralf Jung's avatar
Ralf Jung committed
521
    (* Crucially, this compares the same way as [CmpXchg]! *)
522 523 524 525
    if bool_decide (vals_compare_safe v1 v2) then
      Some $ LitV $ LitBool $ bool_decide (v1 = v2)
    else
      None
526 527 528 529 530 531 532
  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
533

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

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

Amin Timany's avatar
Amin Timany committed
542 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
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.

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

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

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

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

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

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

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

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

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

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

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

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

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