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

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

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

*)


18 19 20
Delimit Scope expr_scope with E.
Delimit Scope val_scope with V.

21
Module heap_lang.
22 23
Open Scope Z_scope.

24
(** Expressions and vals. *)
25
Definition loc := positive. (* Really, any countable type. *)
26
Definition proph := positive.
Ralf Jung's avatar
Ralf Jung committed
27

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

38
Inductive binder := BAnon | BNamed : string  binder.
Ralf Jung's avatar
Ralf Jung committed
39 40
Delimit Scope binder_scope with bind.
Bind Scope binder_scope with binder.
41 42 43
Definition cons_binder (mx : binder) (X : list string) : list string :=
  match mx with BAnon => X | BNamed x => x :: X end.
Infix ":b:" := cons_binder (at level 60, right associativity).
44
Instance binder_eq_dec_eq : EqDecision binder.
45 46 47 48 49 50 51 52 53
Proof. solve_decision. Defined.

Instance set_unfold_cons_binder x mx X P :
  SetUnfold (x  X) P  SetUnfold (x  mx :b: X) (BNamed x = mx  P).
Proof.
  constructor. rewrite -(set_unfold (x  X) P).
  destruct mx; rewrite /= ?elem_of_cons; naive_solver.
Qed.

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

84 85
Bind Scope expr_scope with expr.

86 87 88 89
Fixpoint is_closed (X : list string) (e : expr) : bool :=
  match e with
  | Var x => bool_decide (x  X)
  | Rec f x e => is_closed (f :b: x :b: X) e
90
  | Lit _ | NewProph => true
91 92
  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e =>
     is_closed X e
93
  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 | ResolveProph e1 e2 =>
94 95 96 97 98
     is_closed X e1 && is_closed X e2
  | If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
     is_closed X e0 && is_closed X e1 && is_closed X e2
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
99
Class Closed (X : list string) (e : expr) := closed : is_closed X e.
100
Instance closed_proof_irrel X e : ProofIrrel (Closed X e).
101
Proof. rewrite /Closed. apply _. Qed.
102 103
Instance closed_dec X e : Decision (Closed X e).
Proof. rewrite /Closed. apply _. Defined.
104

105
Inductive val :=
106
  | RecV (f x : binder) (e : expr) `{!Closed (f :b: x :b: []) e}
107
  | LitV (l : base_lit)
108 109
  | PairV (v1 v2 : val)
  | InjLV (v : val)
110
  | InjRV (v : val).
Ralf Jung's avatar
Ralf Jung committed
111

112 113
Bind Scope val_scope with val.

114
Definition observation : Set := proph * val.
115

116
Fixpoint of_val (v : val) : expr :=
Ralf Jung's avatar
Ralf Jung committed
117
  match v with
118
  | RecV f x e => Rec f x e
119
  | LitV l => Lit l
120 121 122
  | PairV v1 v2 => Pair (of_val v1) (of_val v2)
  | InjLV v => InjL (of_val v)
  | InjRV v => InjR (of_val v)
Ralf Jung's avatar
Ralf Jung committed
123
  end.
124

125
Fixpoint to_val (e : expr) : option val :=
126
  match e with
127 128
  | Rec f x e =>
     if decide (Closed (f :b: x :b: []) e) then Some (RecV f x e) else None
129
  | Lit l => Some (LitV l)
130 131 132
  | Pair e1 e2 => v1  to_val e1; v2  to_val e2; Some (PairV v1 v2)
  | InjL e => InjLV <$> to_val e
  | InjR e => InjRV <$> to_val e
Ralf Jung's avatar
Ralf Jung committed
133
  | _ => None
134 135
  end.

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 162 163 164 165 166 167
(** 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.

168
(** The state: heaps of vals. *)
169
Definition state : Type := gmap loc val * gset proph.
Ralf Jung's avatar
Ralf Jung committed
170

171 172 173 174 175 176 177 178 179 180 181 182 183 184
(** Equality and other typeclass stuff *)
Lemma to_of_val v : to_val (of_val v) = Some v.
Proof.
  by induction v; simplify_option_eq; repeat f_equal; try apply (proof_irrel _).
Qed.

Lemma of_to_val e v : to_val e = Some v  of_val v = e.
Proof.
  revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
Qed.

Instance of_val_inj : Inj (=) (=) of_val.
Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.

185
Instance base_lit_eq_dec : EqDecision base_lit.
186
Proof. solve_decision. Defined.
187
Instance un_op_eq_dec : EqDecision un_op.
188
Proof. solve_decision. Defined.
189
Instance bin_op_eq_dec : EqDecision bin_op.
190
Proof. solve_decision. Defined.
191
Instance expr_eq_dec : EqDecision expr.
192
Proof. solve_decision. Defined.
193
Instance val_eq_dec : EqDecision val.
194
Proof.
195
 refine (λ v v', cast_if (decide (of_val v = of_val v'))); abstract naive_solver.
196 197
Defined.

198 199 200
Instance base_lit_countable : Countable base_lit.
Proof.
 refine (inj_countable' (λ l, match l with
201 202 203
  | 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)
204
  end) (λ l, match l with
205 206
  | (inl (inl n), None) => LitInt n | (inl (inr b), None) => LitBool b
  | (inr (inl ()), None) => LitUnit | (inr (inr l), None) => LitLoc l
207
  | (_, Some p) => LitProphecy p
208 209 210 211 212 213 214 215 216 217
  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
218 219 220
  | PlusOp => 0 | MinusOp => 1 | MultOp => 2 | QuotOp => 3 | RemOp => 4
  | AndOp => 5 | OrOp => 6 | XorOp => 7 | ShiftLOp => 8 | ShiftROp => 9
  | LeOp => 10 | LtOp => 11 | EqOp => 12
221
  end) (λ n, match n with
222 223 224
  | 0 => PlusOp | 1 => MinusOp | 2 => MultOp | 3 => QuotOp | 4 => RemOp
  | 5 => AndOp | 6 => OrOp | 7 => XorOp | 8 => ShiftLOp | 9 => ShiftROp
  | 10 => LeOp | 11 => LtOp | _ => EqOp
225 226 227 228 229 230 231 232 233 234 235
  end) _); by intros [].
Qed.
Instance binder_countable : Countable binder.
Proof.
 refine (inj_countable' (λ b, match b with BNamed s => Some s | BAnon => None end)
  (λ b, match b with Some s => BNamed s | None => BAnon end) _); by intros [].
Qed.
Instance expr_countable : Countable expr.
Proof.
 set (enc := fix go e :=
  match e with
236 237
  | Var x => GenLeaf (Some (inl (inl x)))
  | Rec f x e => GenNode 0 [GenLeaf (Some ((inl (inr f)))); GenLeaf (Some (inl (inr x))); go e]
238
  | App e1 e2 => GenNode 1 [go e1; go e2]
239 240 241
  | Lit l => GenLeaf (Some (inr (inl l)))
  | UnOp op e => GenNode 2 [GenLeaf (Some (inr (inr (inl op)))); go e]
  | BinOp op e1 e2 => GenNode 3 [GenLeaf (Some (inr (inr (inr op)))); go e1; go e2]
242 243 244 245 246 247 248 249 250 251 252 253
  | If e0 e1 e2 => GenNode 4 [go e0; go e1; go e2]
  | Pair e1 e2 => GenNode 5 [go e1; go e2]
  | Fst e => GenNode 6 [go e]
  | Snd e => GenNode 7 [go e]
  | InjL e => GenNode 8 [go e]
  | InjR e => GenNode 9 [go e]
  | Case e0 e1 e2 => GenNode 10 [go e0; go e1; go e2]
  | Fork e => GenNode 11 [go e]
  | Alloc e => GenNode 12 [go e]
  | Load e => GenNode 13 [go e]
  | Store e1 e2 => GenNode 14 [go e1; go e2]
  | CAS e0 e1 e2 => GenNode 15 [go e0; go e1; go e2]
254
  | FAA e1 e2 => GenNode 16 [go e1; go e2]
255 256
  | NewProph => GenLeaf None
  | ResolveProph e1 e2 => GenNode 17 [go e1; go e2]
257 258 259
  end).
 set (dec := fix go e :=
  match e with
260 261
  | GenLeaf (Some(inl (inl x))) => Var x
  | GenNode 0 [GenLeaf (Some (inl (inr f))); GenLeaf (Some (inl (inr x))); e] => Rec f x (go e)
262
  | GenNode 1 [e1; e2] => App (go e1) (go e2)
263 264 265
  | GenLeaf (Some (inr (inl l))) => Lit l
  | GenNode 2 [GenLeaf (Some (inr (inr (inl op)))); e] => UnOp op (go e)
  | GenNode 3 [GenLeaf (Some (inr (inr (inr op)))); e1; e2] => BinOp op (go e1) (go e2)
266 267 268 269 270 271 272 273 274 275 276 277
  | GenNode 4 [e0; e1; e2] => If (go e0) (go e1) (go e2)
  | GenNode 5 [e1; e2] => Pair (go e1) (go e2)
  | GenNode 6 [e] => Fst (go e)
  | GenNode 7 [e] => Snd (go e)
  | GenNode 8 [e] => InjL (go e)
  | GenNode 9 [e] => InjR (go e)
  | GenNode 10 [e0; e1; e2] => Case (go e0) (go e1) (go e2)
  | GenNode 11 [e] => Fork (go e)
  | GenNode 12 [e] => Alloc (go e)
  | GenNode 13 [e] => Load (go e)
  | GenNode 14 [e1; e2] => Store (go e1) (go e2)
  | GenNode 15 [e0; e1; e2] => CAS (go e0) (go e1) (go e2)
278
  | GenNode 16 [e1; e2] => FAA (go e1) (go e2)
279 280
  | GenLeaf None => NewProph
  | GenNode 17 [e1; e2] => ResolveProph (go e1) (go e2)
281 282 283 284 285 286 287
  | _ => Lit LitUnit (* dummy *)
  end).
 refine (inj_countable' enc dec _). intros e. induction e; f_equal/=; auto.
Qed.
Instance val_countable : Countable val.
Proof. refine (inj_countable of_val to_val _); auto using to_of_val. Qed.

288 289 290 291 292 293 294
Instance expr_inhabited : Inhabited expr := populate (Lit LitUnit).
Instance val_inhabited : Inhabited val := populate (LitV LitUnit).

Canonical Structure stateC := leibnizC state.
Canonical Structure valC := leibnizC val.
Canonical Structure exprC := leibnizC expr.

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

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

350
(** Substitution *)
351 352 353
Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
  match e with
  | Var y => if decide (x = y) then es else Var y
354
  | Rec f y e =>
355 356
     Rec f y $ if decide (BNamed x  f  BNamed x  y) then subst x es e else e
  | App e1 e2 => App (subst x es e1) (subst x es e2)
357
  | Lit l => Lit l
358 359 360 361 362 363 364 365 366 367 368 369 370 371
  | UnOp op e => UnOp op (subst x es e)
  | BinOp op e1 e2 => BinOp op (subst x es e1) (subst x es e2)
  | If e0 e1 e2 => If (subst x es e0) (subst x es e1) (subst x es e2)
  | Pair e1 e2 => Pair (subst x es e1) (subst x es e2)
  | Fst e => Fst (subst x es e)
  | Snd e => Snd (subst x es e)
  | InjL e => InjL (subst x es e)
  | InjR e => InjR (subst x es e)
  | Case e0 e1 e2 => Case (subst x es e0) (subst x es e1) (subst x es e2)
  | Fork e => Fork (subst x es e)
  | Alloc e => Alloc (subst x es e)
  | Load e => Load (subst x es e)
  | Store e1 e2 => Store (subst x es e1) (subst x es e2)
  | CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
372
  | FAA e1 e2 => FAA (subst x es e1) (subst x es e2)
373 374
  | NewProph => NewProph
  | ResolveProph e1 e2 => ResolveProph (subst x es e1) (subst x es e2)
375
  end.
376

377
Definition subst' (mx : binder) (es : expr) : expr  expr :=
378
  match mx with BNamed x => subst x es | BAnon => id end.
379

380
(** The stepping relation *)
381 382 383
Definition un_op_eval (op : un_op) (v : val) : option val :=
  match op, v with
  | NegOp, LitV (LitBool b) => Some $ LitV $ LitBool (negb b)
384
  | NegOp, LitV (LitInt n) => Some $ LitV $ LitInt (Z.lnot n)
385
  | MinusUnOp, LitV (LitInt n) => Some $ LitV $ LitInt (- n)
386 387 388
  | _, _ => None
  end.

389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416
Definition bin_op_eval_int (op : bin_op) (n1 n2 : Z) : base_lit :=
  match op with
  | PlusOp => LitInt (n1 + n2)
  | MinusOp => LitInt (n1 - n2)
  | MultOp => LitInt (n1 * n2)
  | QuotOp => LitInt (n1 `quot` n2)
  | RemOp => LitInt (n1 `rem` n2)
  | AndOp => LitInt (Z.land n1 n2)
  | OrOp => LitInt (Z.lor n1 n2)
  | XorOp => LitInt (Z.lxor n1 n2)
  | ShiftLOp => LitInt (n1  n2)
  | ShiftROp => LitInt (n1  n2)
  | LeOp => LitBool (bool_decide (n1  n2))
  | LtOp => LitBool (bool_decide (n1 < n2))
  | EqOp => LitBool (bool_decide (n1 = n2))
  end.

Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
  match op with
  | PlusOp | MinusOp | MultOp | QuotOp | RemOp => None (* Arithmetic *)
  | AndOp => Some (LitBool (b1 && b2))
  | OrOp => Some (LitBool (b1 || b2))
  | XorOp => Some (LitBool (xorb b1 b2))
  | ShiftLOp | ShiftROp => None (* Shifts *)
  | LeOp | LtOp => None (* InEquality *)
  | EqOp => Some (LitBool (bool_decide (b1 = b2)))
  end.

417
Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
418
  if decide (op = EqOp) then Some $ LitV $ LitBool $ bool_decide (v1 = v2) else
419 420 421
  match v1, v2 with
  | LitV (LitInt n1), LitV (LitInt n2) => Some $ LitV $ bin_op_eval_int op n1 n2
  | LitV (LitBool b1), LitV (LitBool b2) => LitV <$> bin_op_eval_bool op b1 b2
Robbert Krebbers's avatar
Robbert Krebbers committed
422
  | _, _ => None
423 424
  end.

425 426 427 428
(** 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
429
Definition vals_cas_compare_safe (vl v1 : val) : Prop :=
430 431
  val_is_unboxed vl  val_is_unboxed v1.
Arguments vals_cas_compare_safe !_ !_ /.
Ralf Jung's avatar
Ralf Jung committed
432

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

496
(** Basic properties about the language *)
497
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
498
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
499

500 501 502
Lemma fill_item_val Ki e :
  is_Some (to_val (fill_item Ki e))  is_Some (to_val e).
Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
503

504
Lemma val_head_stuck e1 σ1 κ e2 σ2 efs : head_step e1 σ1 κ e2 σ2 efs  to_val e1 = None.
505
Proof. destruct 1; naive_solver. Qed.
506

507 508
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).
509
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
510

511
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
512
  to_val e1 = None  to_val e2 = None 
513
  fill_item Ki1 e1 = fill_item Ki2 e2  Ki1 = Ki2.
514
Proof.
515
  destruct Ki1, Ki2; intros; try discriminate; simplify_eq/=;
516
    repeat match goal with
517 518
    | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
    end; auto.
Ralf Jung's avatar
Ralf Jung committed
519
Qed.
520

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

526 527 528 529 530
Lemma new_proph_fresh σ :
  let p := fresh σ.2 in
  head_step NewProph σ None (Lit $ LitProphecy p) (σ.1, {[ p ]}  σ.2) [].
Proof. constructor. apply is_fresh. Qed.

531 532 533 534 535
(* Misc *)
Lemma to_val_rec f x e `{!Closed (f :b: x :b: []) e} :
  to_val (Rec f x e) = Some (RecV f x e).
Proof. rewrite /to_val. case_decide=> //. do 2 f_equal; apply proof_irrel. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
536
(** Closed expressions *)
537
Lemma is_closed_weaken X Y e : is_closed X e  X  Y  is_closed Y e.
Robbert Krebbers's avatar
Robbert Krebbers committed
538 539
Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.

540
Lemma is_closed_weaken_nil X e : is_closed [] e  is_closed X e.
541
Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
542

543 544 545
Lemma is_closed_of_val X v : is_closed X (of_val v).
Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.

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

549 550 551 552 553 554 555 556 557 558 559 560 561 562 563
Lemma is_closed_subst X e x es :
  is_closed [] es  is_closed (x :: X) e  is_closed X (subst x es e).
Proof.
  intros ?. revert X.
  induction e=> X /= ?; destruct_and?; split_and?; simplify_option_eq;
    try match goal with
    | H : ¬(_  _) |- _ => apply not_and_l in H as [?%dec_stable|?%dec_stable]
    end; eauto using is_closed_weaken with set_solver.
Qed.
Lemma is_closed_do_subst' X e x es :
  is_closed [] es  is_closed (x :b: X) e  is_closed X (subst' x es e).
Proof. destruct x; eauto using is_closed_subst. Qed.

(* Substitution *)
Lemma subst_is_closed X e x es : is_closed X e  x  X  subst x es e = e.
Robbert Krebbers's avatar
Robbert Krebbers committed
564
Proof.
565
  revert X. induction e=> X /=; rewrite ?bool_decide_spec ?andb_True=> ??;
Robbert Krebbers's avatar
Robbert Krebbers committed
566 567
    repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver.
Qed.
568

569 570
Lemma subst_is_closed_nil e x es : is_closed [] e  subst x es e = e.
Proof. intros. apply subst_is_closed with []; set_solver. Qed.
571

572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601
Lemma subst_subst e x es es' :
  Closed [] es'  subst x es (subst x es' e) = subst x es' e.
Proof.
  intros. induction e; simpl; try (f_equal; by auto);
    simplify_option_eq; auto using subst_is_closed_nil with f_equal.
Qed.
Lemma subst_subst' e x es es' :
  Closed [] es'  subst' x es (subst' x es' e) = subst' x es' e.
Proof. destruct x; simpl; auto using subst_subst. Qed.

Lemma subst_subst_ne e x y es es' :
  Closed [] es  Closed [] es'  x  y 
  subst x es (subst y es' e) = subst y es' (subst x es e).
Proof.
  intros. induction e; simpl; try (f_equal; by auto);
    simplify_option_eq; auto using eq_sym, subst_is_closed_nil with f_equal.
Qed.
Lemma subst_subst_ne' e x y es es' :
  Closed [] es  Closed [] es'  x  y 
  subst' x es (subst' y es' e) = subst' y es' (subst' x es e).
Proof. destruct x, y; simpl; auto using subst_subst_ne with congruence. Qed.

Lemma subst_rec' f y e x es :
  x = f  x = y  x = BAnon 
  subst' x es (Rec f y e) = Rec f y e.
Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.
Lemma subst_rec_ne' f y e x es :
  (x  f  f = BAnon)  (x  y  y = BAnon) 
  subst' x es (Rec f y e) = Rec f y (subst' x es e).
Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.
602 603 604 605 606 607

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.
608 609 610
End heap_lang.

(** Language *)
611 612 613
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.
614

615
(* Prefer heap_lang names over ectx_language names. *)
616
Export heap_lang.
617 618 619 620 621 622 623 624 625 626 627

(** Define some derived forms. *)
Notation Lam x e := (Rec BAnon x e) (only parsing).
Notation Let x e1 e2 := (App (Lam x e2) e1) (only parsing).
Notation Seq e1 e2 := (Let BAnon e1 e2) (only parsing).
Notation LamV x e := (RecV BAnon x e) (only parsing).
Notation LetCtx x e2 := (AppRCtx (LamV x e2)) (only parsing).
Notation SeqCtx e2 := (LetCtx BAnon e2) (only parsing).
Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)) (only parsing).

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