lang.v 24 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
(** 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].

15 16 17 18 19 20
- For prophecy variables, we annotate the reduction steps with an "observation"
  and tweak adequacy such that WP knows all future observations.  There is
  another possible choice: Use non-deterministic choice when creating a prophecy
  variable ([NewProph]), and when resolving it ([ResolveProph]) make the
  program diverge unless the variable matches.  That, however, requires an
  erasure proof that this endless loop does not make specifications useless.
Ralf Jung's avatar
Ralf Jung committed
21

22
*)
Ralf Jung's avatar
Ralf Jung committed
23

24 25 26
Delimit Scope expr_scope with E.
Delimit Scope val_scope with V.

27
Module heap_lang.
28 29
Open Scope Z_scope.

30
(** Expressions and vals. *)
31
Definition loc := positive. (* Really, any countable type. *)
32
Definition proph := positive.
Ralf Jung's avatar
Ralf Jung committed
33

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

44
Inductive binder := BAnon | BNamed : string  binder.
Ralf Jung's avatar
Ralf Jung committed
45 46
Delimit Scope binder_scope with bind.
Bind Scope binder_scope with binder.
47 48 49
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).
50
Instance binder_eq_dec_eq : EqDecision binder.
51 52 53 54 55 56 57 58 59
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.

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

90 91
Bind Scope expr_scope with expr.

92 93 94 95
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
96
  | Lit _ | NewProph => true
97 98
  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e =>
     is_closed X e
99
  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 | ResolveProph e1 e2 =>
100 101 102 103 104
     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
105
Class Closed (X : list string) (e : expr) := closed : is_closed X e.
106
Instance closed_proof_irrel X e : ProofIrrel (Closed X e).
107
Proof. rewrite /Closed. apply _. Qed.
108 109
Instance closed_dec X e : Decision (Closed X e).
Proof. rewrite /Closed. apply _. Defined.
110

111
Inductive val :=
112
  | RecV (f x : binder) (e : expr) `{!Closed (f :b: x :b: []) e}
113
  | LitV (l : base_lit)
114 115
  | PairV (v1 v2 : val)
  | InjLV (v : val)
116
  | InjRV (v : val).
Ralf Jung's avatar
Ralf Jung committed
117

118 119
Bind Scope val_scope with val.

120
Definition observation : Set := proph * val.
121

122
Fixpoint of_val (v : val) : expr :=
Ralf Jung's avatar
Ralf Jung committed
123
  match v with
124
  | RecV f x e => Rec f x e
125
  | LitV l => Lit l
126 127 128
  | 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
129
  end.
130

131
Fixpoint to_val (e : expr) : option val :=
132
  match e with
133 134
  | Rec f x e =>
     if decide (Closed (f :b: x :b: []) e) then Some (RecV f x e) else None
135
  | Lit l => Some (LitV l)
136 137 138
  | 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
139
  | _ => None
140 141
  end.

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 168 169 170 171 172 173
(** 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.

174
(** The state: heaps of vals. *)
175
Definition state : Type := gmap loc val * gset proph.
176
Implicit Type σ : state.
Ralf Jung's avatar
Ralf Jung committed
177

178 179 180 181 182 183 184 185 186 187 188 189 190 191
(** 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.

192
Instance base_lit_eq_dec : EqDecision base_lit.
193
Proof. solve_decision. Defined.
194
Instance un_op_eq_dec : EqDecision un_op.
195
Proof. solve_decision. Defined.
196
Instance bin_op_eq_dec : EqDecision bin_op.
197
Proof. solve_decision. Defined.
198
Instance expr_eq_dec : EqDecision expr.
199
Proof. solve_decision. Defined.
200
Instance val_eq_dec : EqDecision val.
201
Proof.
202
 refine (λ v v', cast_if (decide (of_val v = of_val v'))); abstract naive_solver.
203 204
Defined.

205 206 207
Instance base_lit_countable : Countable base_lit.
Proof.
 refine (inj_countable' (λ l, match l with
208 209 210
  | 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)
211
  end) (λ l, match l with
212 213
  | (inl (inl n), None) => LitInt n | (inl (inr b), None) => LitBool b
  | (inr (inl ()), None) => LitUnit | (inr (inr l), None) => LitLoc l
214
  | (_, Some p) => LitProphecy p
215 216 217 218 219 220 221 222 223 224
  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
225 226 227
  | 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
228
  end) (λ n, match n with
229 230 231
  | 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
232 233 234 235 236 237 238 239 240 241 242
  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
243 244
  | 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]
245
  | App e1 e2 => GenNode 1 [go e1; go e2]
246 247 248
  | 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]
249 250 251 252 253 254 255 256 257 258 259 260
  | 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]
261
  | FAA e1 e2 => GenNode 16 [go e1; go e2]
262 263
  | NewProph => GenLeaf None
  | ResolveProph e1 e2 => GenNode 17 [go e1; go e2]
264 265 266
  end).
 set (dec := fix go e :=
  match e with
267 268
  | 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)
269
  | GenNode 1 [e1; e2] => App (go e1) (go e2)
270 271 272
  | 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)
273 274 275 276 277 278 279 280 281 282 283 284
  | 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)
285
  | GenNode 16 [e1; e2] => FAA (go e1) (go e2)
286 287
  | GenLeaf None => NewProph
  | GenNode 17 [e1; e2] => ResolveProph (go e1) (go e2)
288 289 290 291 292 293 294
  | _ => 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.

295 296 297 298 299 300 301
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.

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

329
Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
330
  match Ki with
331 332
  | AppLCtx v2 => App e (of_val v2)
  | AppRCtx e1 => App e1 e
333
  | UnOpCtx op => UnOp op e
334 335
  | BinOpLCtx op v2 => BinOp op e (of_val v2)
  | BinOpRCtx op e1 => BinOp op e1 e
336
  | IfCtx e1 e2 => If e e1 e2
337 338
  | PairLCtx v2 => Pair e (of_val v2)
  | PairRCtx e1 => Pair e1 e
339 340 341 342
  | FstCtx => Fst e
  | SndCtx => Snd e
  | InjLCtx => InjL e
  | InjRCtx => InjR e
343
  | CaseCtx e1 e2 => Case e e1 e2
344 345
  | AllocCtx => Alloc e
  | LoadCtx => Load e
346 347 348 349 350 351 352
  | 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
353 354
  | ProphLCtx v2 => ResolveProph e (of_val v2)
  | ProphRCtx e1 => ResolveProph e1 e
Ralf Jung's avatar
Ralf Jung committed
355 356
  end.

357
(** Substitution *)
358 359 360
Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
  match e with
  | Var y => if decide (x = y) then es else Var y
361
  | Rec f y e =>
362 363
     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)
364
  | Lit l => Lit l
365 366 367 368 369 370 371 372 373 374 375 376 377 378
  | 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)
379
  | FAA e1 e2 => FAA (subst x es e1) (subst x es e2)
380 381
  | NewProph => NewProph
  | ResolveProph e1 e2 => ResolveProph (subst x es e1) (subst x es e2)
382
  end.
383

384
Definition subst' (mx : binder) (es : expr) : expr  expr :=
385
  match mx with BNamed x => subst x es | BAnon => id end.
386

387
(** The stepping relation *)
388 389 390
Definition un_op_eval (op : un_op) (v : val) : option val :=
  match op, v with
  | NegOp, LitV (LitBool b) => Some $ LitV $ LitBool (negb b)
391
  | NegOp, LitV (LitInt n) => Some $ LitV $ LitInt (Z.lnot n)
392
  | MinusUnOp, LitV (LitInt n) => Some $ LitV $ LitInt (- n)
393 394 395
  | _, _ => None
  end.

396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423
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.

424
Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
425
  if decide (op = EqOp) then Some $ LitV $ LitBool $ bool_decide (v1 = v2) else
426 427 428
  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
429
  | _, _ => None
430 431
  end.

432 433 434 435
(** 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
436
Definition vals_cas_compare_safe (vl v1 : val) : Prop :=
437 438
  val_is_unboxed vl  val_is_unboxed v1.
Arguments vals_cas_compare_safe !_ !_ /.
Ralf Jung's avatar
Ralf Jung committed
439

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

512
(** Basic properties about the language *)
513
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
514
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
515

516 517 518
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.
519

520
Lemma val_head_stuck e1 σ1 κ e2 σ2 efs : head_step e1 σ1 κ e2 σ2 efs  to_val e1 = None.
521
Proof. destruct 1; naive_solver. Qed.
522

523 524
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).
525
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
526

527
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
528
  to_val e1 = None  to_val e2 = None 
529
  fill_item Ki1 e1 = fill_item Ki2 e2  Ki1 = Ki2.
530
Proof.
531
  destruct Ki1, Ki2; intros; try discriminate; simplify_eq/=;
532
    repeat match goal with
533 534
    | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
    end; auto.
Ralf Jung's avatar
Ralf Jung committed
535
Qed.
536

537
Lemma alloc_fresh e v σ :
538 539
  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
540
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset loc)), is_fresh. Qed.
541

542 543 544 545 546
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.

547 548 549 550 551
(* 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
552
(** Closed expressions *)
553
Lemma is_closed_weaken X Y e : is_closed X e  X  Y  is_closed Y e.
Robbert Krebbers's avatar
Robbert Krebbers committed
554 555
Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.

556
Lemma is_closed_weaken_nil X e : is_closed [] e  is_closed X e.
557
Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
558

559 560 561
Lemma is_closed_of_val X v : is_closed X (of_val v).
Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.

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

565 566 567 568 569 570 571 572 573 574 575 576 577 578 579
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
580
Proof.
581
  revert X. induction e=> X /=; rewrite ?bool_decide_spec ?andb_True=> ??;
Robbert Krebbers's avatar
Robbert Krebbers committed
582 583
    repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver.
Qed.
584

585 586
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.
587

588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617
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.
618 619 620 621 622 623

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.
624 625 626
End heap_lang.

(** Language *)
627 628 629
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.
630

631
(* Prefer heap_lang names over ectx_language names. *)
632
Export heap_lang.
633 634 635 636 637 638 639 640 641 642 643

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