lang.v 22.3 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 79
  | CAS (e0 : expr) (e1 : expr) (e2 : expr)
  | FAA (e1 : expr) (e2 : expr).
Ralf Jung's avatar
Ralf Jung committed
80

81 82
Bind Scope expr_scope with expr.

83 84 85 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
  | Lit _ => true
  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e =>
     is_closed X e
90
  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 =>
91 92 93 94 95
     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
96
Class Closed (X : list string) (e : expr) := closed : is_closed X e.
97
Instance closed_proof_irrel X e : ProofIrrel (Closed X e).
98
Proof. rewrite /Closed. apply _. Qed.
99 100
Instance closed_dec X e : Decision (Closed X e).
Proof. rewrite /Closed. apply _. Defined.
101

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

109 110
Bind Scope val_scope with val.

111 112
Inductive observation := prophecy_observation_todo.

113
Fixpoint of_val (v : val) : expr :=
Ralf Jung's avatar
Ralf Jung committed
114
  match v with
115
  | RecV f x e => Rec f x e
116
  | LitV l => Lit l
117 118 119
  | 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
120
  end.
121

122
Fixpoint to_val (e : expr) : option val :=
123
  match e with
124 125
  | Rec f x e =>
     if decide (Closed (f :b: x :b: []) e) then Some (RecV f x e) else None
126
  | Lit l => Some (LitV l)
127 128 129
  | 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
130
  | _ => None
131 132
  end.

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

165 166
(** The state: heaps of vals. *)
Definition state := gmap loc val.
Ralf Jung's avatar
Ralf Jung committed
167

168 169 170 171 172 173 174 175 176 177 178 179 180 181
(** 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.

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

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

281 282 283 284 285 286 287
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.

288
(** Evaluation contexts *)
289
Inductive ectx_item :=
290 291
  | AppLCtx (v2 : val)
  | AppRCtx (e1 : expr)
292
  | UnOpCtx (op : un_op)
293 294
  | BinOpLCtx (op : bin_op) (v2 : val)
  | BinOpRCtx (op : bin_op) (e1 : expr)
295
  | IfCtx (e1 e2 : expr)
296 297
  | PairLCtx (v2 : val)
  | PairRCtx (e1 : expr)
298 299 300 301
  | FstCtx
  | SndCtx
  | InjLCtx
  | InjRCtx
302
  | CaseCtx (e1 : expr) (e2 : expr)
303 304
  | AllocCtx
  | LoadCtx
305 306 307 308 309 310 311
  | StoreLCtx (v2 : val)
  | StoreRCtx (e1 : expr)
  | CasLCtx (v1 : val) (v2 : val)
  | CasMCtx (e0 : expr) (v2 : val)
  | CasRCtx (e0 : expr) (e1 : expr)
  | FaaLCtx (v2 : val)
  | FaaRCtx (e1 : expr).
312

313
Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
314
  match Ki with
315 316
  | AppLCtx v2 => App e (of_val v2)
  | AppRCtx e1 => App e1 e
317
  | UnOpCtx op => UnOp op e
318 319
  | BinOpLCtx op v2 => BinOp op e (of_val v2)
  | BinOpRCtx op e1 => BinOp op e1 e
320
  | IfCtx e1 e2 => If e e1 e2
321 322
  | PairLCtx v2 => Pair e (of_val v2)
  | PairRCtx e1 => Pair e1 e
323 324 325 326
  | FstCtx => Fst e
  | SndCtx => Snd e
  | InjLCtx => InjL e
  | InjRCtx => InjR e
327
  | CaseCtx e1 e2 => Case e e1 e2
328 329
  | AllocCtx => Alloc e
  | LoadCtx => Load e
330 331 332 333 334 335 336
  | 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
Ralf Jung's avatar
Ralf Jung committed
337 338
  end.

339
(** Substitution *)
340 341 342
Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
  match e with
  | Var y => if decide (x = y) then es else Var y
343
  | Rec f y e =>
344 345
     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)
346
  | Lit l => Lit l
347 348 349 350 351 352 353 354 355 356 357 358 359 360
  | 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)
361
  | FAA e1 e2 => FAA (subst x es e1) (subst x es e2)
362
  end.
363

364
Definition subst' (mx : binder) (es : expr) : expr  expr :=
365
  match mx with BNamed x => subst x es | BAnon => id end.
366

367
(** The stepping relation *)
368 369 370
Definition un_op_eval (op : un_op) (v : val) : option val :=
  match op, v with
  | NegOp, LitV (LitBool b) => Some $ LitV $ LitBool (negb b)
371
  | NegOp, LitV (LitInt n) => Some $ LitV $ LitInt (Z.lnot n)
372
  | MinusUnOp, LitV (LitInt n) => Some $ LitV $ LitInt (- n)
373 374 375
  | _, _ => None
  end.

376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403
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.

404
Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
405
  if decide (op = EqOp) then Some $ LitV $ LitBool $ bool_decide (v1 = v2) else
406 407 408
  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
409
  | _, _ => None
410 411
  end.

412 413 414 415
(** 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
416
Definition vals_cas_compare_safe (vl v1 : val) : Prop :=
417 418
  val_is_unboxed vl  val_is_unboxed v1.
Arguments vals_cas_compare_safe !_ !_ /.
Ralf Jung's avatar
Ralf Jung committed
419

420
Inductive head_step : expr  state  option observation -> expr  state  list (expr)  Prop :=
421
  | BetaS f x e1 e2 v2 e' σ :
422
     to_val e2 = Some v2 
423
     Closed (f :b: x :b: []) e1 
424
     e' = subst' x (of_val v2) (subst' f (Rec f x e1) e1) 
425
     head_step (App (Rec f x e1) e2) σ None e' σ []
426 427
  | UnOpS op e v v' σ :
     to_val e = Some v 
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
428
     un_op_eval op v = Some v' 
429
     head_step (UnOp op e) σ None (of_val v') σ []
430 431
  | 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
432
     bin_op_eval op v1 v2 = Some v' 
433
     head_step (BinOp op e1 e2) σ None (of_val v') σ []
434
  | IfTrueS e1 e2 σ :
435
     head_step (If (Lit $ LitBool true) e1 e2) σ None e1 σ []
436
  | IfFalseS e1 e2 σ :
437
     head_step (If (Lit $ LitBool false) e1 e2) σ None e2 σ []
438 439
  | FstS e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
440
     head_step (Fst (Pair e1 e2)) σ None e1 σ []
441 442
  | SndS e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
443
     head_step (Snd (Pair e1 e2)) σ None e2 σ []
444
  | CaseLS e0 v0 e1 e2 σ :
445
     to_val e0 = Some v0 
446
     head_step (Case (InjL e0) e1 e2) σ None (App e1 e0) σ []
447
  | CaseRS e0 v0 e1 e2 σ :
448
     to_val e0 = Some v0 
449
     head_step (Case (InjR e0) e1 e2) σ None (App e2 e0) σ []
450
  | ForkS e σ:
451
     head_step (Fork e) σ None (Lit LitUnit) σ [e]
452 453
  | AllocS e v σ l :
     to_val e = Some v  σ !! l = None 
454
     head_step (Alloc e) σ None (Lit $ LitLoc l) (<[l:=v]>σ) []
455 456
  | LoadS l v σ :
     σ !! l = Some v 
457
     head_step (Load (Lit $ LitLoc l)) σ None (of_val v) σ []
458 459
  | StoreS l e v σ :
     to_val e = Some v  is_Some (σ !! l) 
460
     head_step (Store (Lit $ LitLoc l) e) σ None (Lit LitUnit) (<[l:=v]>σ) []
461 462 463
  | CasFailS l e1 v1 e2 v2 vl σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some vl  vl  v1 
Ralf Jung's avatar
Ralf Jung committed
464
     vals_cas_compare_safe vl v1 
465
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ None (Lit $ LitBool false) σ []
466 467 468
  | CasSucS l e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some v1 
Ralf Jung's avatar
Ralf Jung committed
469
     vals_cas_compare_safe v1 v1 
470
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ None (Lit $ LitBool true) (<[l:=v2]>σ) []
Ralf Jung's avatar
Ralf Jung committed
471
  | FaaS l i1 e2 i2 σ :
472 473
     to_val e2 = Some (LitV (LitInt i2)) 
     σ !! l = Some (LitV (LitInt i1)) 
474
     head_step (FAA (Lit $ LitLoc l) e2) σ None (Lit $ LitInt i1) (<[l:=LitV (LitInt (i1 + i2))]>σ) [].
Ralf Jung's avatar
Ralf Jung committed
475

476
(** Basic properties about the language *)
477
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
478
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
479

480 481 482
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.
483

484
Lemma val_head_stuck e1 σ1 κ e2 σ2 efs : head_step e1 σ1 κ e2 σ2 efs  to_val e1 = None.
485
Proof. destruct 1; naive_solver. Qed.
486

487 488
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).
489
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
490

491
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
492
  to_val e1 = None  to_val e2 = None 
493
  fill_item Ki1 e1 = fill_item Ki2 e2  Ki1 = Ki2.
494
Proof.
495
  destruct Ki1, Ki2; intros; try discriminate; simplify_eq/=;
496
    repeat match goal with
497 498
    | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
    end; auto.
Ralf Jung's avatar
Ralf Jung committed
499
Qed.
500

501
Lemma alloc_fresh e v σ :
502
  let l := fresh (dom (gset loc) σ) in
503
  to_val e = Some v  head_step (Alloc e) σ None (Lit (LitLoc l)) (<[l:=v]>σ) [].
Robbert Krebbers's avatar
Robbert Krebbers committed
504
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset loc)), is_fresh. Qed.
505

506 507 508 509 510
(* 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
511
(** Closed expressions *)
512
Lemma is_closed_weaken X Y e : is_closed X e  X  Y  is_closed Y e.
Robbert Krebbers's avatar
Robbert Krebbers committed
513 514
Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.

515
Lemma is_closed_weaken_nil X e : is_closed [] e  is_closed X e.
516
Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
517

518 519 520
Lemma is_closed_of_val X v : is_closed X (of_val v).
Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.

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

524 525 526 527 528 529 530 531 532 533 534 535 536 537 538
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
539
Proof.
540
  revert X. induction e=> X /=; rewrite ?bool_decide_spec ?andb_True=> ??;
Robbert Krebbers's avatar
Robbert Krebbers committed
541 542
    repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver.
Qed.
543

544 545
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.
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
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.
577 578 579 580 581 582

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.
583 584 585
End heap_lang.

(** Language *)
586 587 588
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.
589

590
(* Prefer heap_lang names over ectx_language names. *)
591
Export heap_lang.
592 593 594 595 596 597 598 599 600 601 602

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