lang.v 25.5 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 17 18 19 20 21
- 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
22

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

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

28
Module heap_lang.
29 30
Open Scope Z_scope.

31
(** Expressions and vals. *)
32
Definition proph_id := positive.
Ralf Jung's avatar
Ralf Jung committed
33

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

46
Inductive expr :=
47 48
  (* Values *)
  | Val (v : val)
49
  (* Base lambda calculus *)
50 51 52
  | Var (x : string)
  | Rec (f x : binder) (e : expr)
  | App (e1 e2 : expr)
53
  (* Base types and their operations *)
54 55 56
  | UnOp (op : un_op) (e : expr)
  | BinOp (op : bin_op) (e1 e2 : expr)
  | If (e0 e1 e2 : expr)
57
  (* Products *)
58 59 60
  | Pair (e1 e2 : expr)
  | Fst (e : expr)
  | Snd (e : expr)
61
  (* Sums *)
62 63 64
  | InjL (e : expr)
  | InjR (e : expr)
  | Case (e0 : expr) (e1 : expr) (e2 : expr)
65
  (* Concurrency *)
66
  | Fork (e : expr)
67
  (* Heap *)
Amin Timany's avatar
Amin Timany committed
68
  | AllocN (e1 e2 : expr) (* array length (positive number), initial value *)
69 70
  | Load (e : expr)
  | Store (e1 : expr) (e2 : expr)
71
  | CAS (e0 : expr) (e1 : expr) (e2 : expr)
72 73 74
  | FAA (e1 : expr) (e2 : expr)
  (* Prophecy *)
  | NewProph
75 76
  | ResolveProph (e1 : expr) (e2 : expr)
with val :=
77
  | LitV (l : base_lit)
78
  | RecV (f x : binder) (e : expr)
79 80
  | PairV (v1 v2 : val)
  | InjLV (v : val)
81
  | InjRV (v : val).
Ralf Jung's avatar
Ralf Jung committed
82

83
Bind Scope expr_scope with expr.
84 85
Bind Scope val_scope with val.

86
Definition observation : Set := proph_id * val.
87

88
Notation of_val := Val (only parsing).
89

90
Definition to_val (e : expr) : option val :=
91
  match e with
92
  | Val v => Some v
Ralf Jung's avatar
Ralf Jung committed
93
  | _ => None
94 95
  end.

96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127
(** 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.

128
(** The state: heaps of vals. *)
Ralf Jung's avatar
Ralf Jung committed
129 130
Record state : Type := {
  heap: gmap loc val;
131
  used_proph_id: gset proph_id;
Ralf Jung's avatar
Ralf Jung committed
132
}.
Ralf Jung's avatar
Ralf Jung committed
133

134 135
(** Equality and other typeclass stuff *)
Lemma to_of_val v : to_val (of_val v) = Some v.
136
Proof. by destruct v. Qed.
137 138

Lemma of_to_val e v : to_val e = Some v  of_val v = e.
139
Proof. destruct e=>//=. by intros [= <-]. Qed.
140 141

Instance of_val_inj : Inj (=) (=) of_val.
142
Proof. intros ??. congruence. Qed.
143

144
Instance base_lit_eq_dec : EqDecision base_lit.
145
Proof. solve_decision. Defined.
146
Instance un_op_eq_dec : EqDecision un_op.
147
Proof. solve_decision. Defined.
148
Instance bin_op_eq_dec : EqDecision bin_op.
149
Proof. solve_decision. Defined.
150
Instance expr_eq_dec : EqDecision expr.
151
Proof.
152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173
  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
174 175
     | AllocN e1 e2, AllocN e1' e2' =>
        cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199
     | Load e, Load e' => cast_if (decide (e = e'))
     | Store e1 e2, Store e1' e2' =>
        cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
     | CAS e0 e1 e2, CAS e0' e1' e2' =>
        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 _
     | ResolveProph e1 e2, ResolveProph e1' e2' =>
        cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
     | _, _ => 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).
200
Defined.
201 202
Instance val_eq_dec : EqDecision val.
Proof. solve_decision. Defined.
203

204 205 206
Instance base_lit_countable : Countable base_lit.
Proof.
 refine (inj_countable' (λ l, match l with
207 208 209
  | 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)
210
  end) (λ l, match l with
211 212
  | (inl (inl n), None) => LitInt n | (inl (inr b), None) => LitBool b
  | (inr (inl ()), None) => LitUnit | (inr (inr l), None) => LitLoc l
213
  | (_, Some p) => LitProphecy p
214 215 216 217 218 219 220 221 222 223
  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
224 225
  | 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
226
  | LeOp => 10 | LtOp => 11 | EqOp => 12 | OffsetOp => 13
227
  end) (λ n, match n with
228 229
  | 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
230
  | 10 => LeOp | 11 => LtOp | 12 => EqOp | _ => OffsetOp
231 232 233 234
  end) _); by intros [].
Qed.
Instance expr_countable : Countable expr.
Proof.
235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251
 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
252
     | AllocN e1 e2 => GenNode 13 [go e1; go e2]
253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286
     | Load e => GenNode 14 [go e]
     | Store e1 e2 => GenNode 15 [go e1; go e2]
     | CAS e0 e1 e2 => GenNode 16 [go e0; go e1; go e2]
     | FAA e1 e2 => GenNode 17 [go e1; go e2]
     | NewProph => GenNode 18 []
     | ResolveProph e1 e2 => GenNode 19 [go e1; go e2]
     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
287
     | GenNode 13 [e1; e2] => AllocN (go e1) (go e2)
288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310
     | GenNode 14 [e] => Load (go e)
     | GenNode 15 [e1; e2] => Store (go e1) (go e2)
     | GenNode 16 [e0; e1; e2] => CAS (go e0) (go e1) (go e2)
     | GenNode 17 [e1; e2] => FAA (go e1) (go e2)
     | GenNode 18 [] => NewProph
     | GenNode 19 [e1; e2] => ResolveProph (go e1) (go e2)
     | _ => 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.
311 312 313 314
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
315
Instance state_inhabited : Inhabited state :=
316
  populate {| heap := inhabitant; used_proph_id := inhabitant |}.
317
Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
318
Instance expr_inhabited : Inhabited expr := populate (Val inhabitant).
319 320

Canonical Structure stateC := leibnizC state.
321
Canonical Structure locC := leibnizC loc.
322 323 324
Canonical Structure valC := leibnizC val.
Canonical Structure exprC := leibnizC expr.

325
(** Evaluation contexts *)
326
Inductive ectx_item :=
327 328
  | AppLCtx (v2 : val)
  | AppRCtx (e1 : expr)
329
  | UnOpCtx (op : un_op)
330 331
  | BinOpLCtx (op : bin_op) (v2 : val)
  | BinOpRCtx (op : bin_op) (e1 : expr)
332
  | IfCtx (e1 e2 : expr)
333 334
  | PairLCtx (v2 : val)
  | PairRCtx (e1 : expr)
335 336 337 338
  | FstCtx
  | SndCtx
  | InjLCtx
  | InjRCtx
339
  | CaseCtx (e1 : expr) (e2 : expr)
Amin Timany's avatar
Amin Timany committed
340 341
  | AllocNLCtx (v2 : val)
  | AllocNRCtx (e1 : expr)
342
  | LoadCtx
343 344 345 346 347 348
  | StoreLCtx (v2 : val)
  | StoreRCtx (e1 : expr)
  | CasLCtx (v1 : val) (v2 : val)
  | CasMCtx (e0 : expr) (v2 : val)
  | CasRCtx (e0 : expr) (e1 : expr)
  | FaaLCtx (v2 : val)
349 350 351
  | FaaRCtx (e1 : expr)
  | ProphLCtx (v2 : val)
  | ProphRCtx (e1 : expr).
352

353
Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
354
  match Ki with
355 356
  | AppLCtx v2 => App e (of_val v2)
  | AppRCtx e1 => App e1 e
357
  | UnOpCtx op => UnOp op e
358
  | BinOpLCtx op v2 => BinOp op e (Val v2)
359
  | BinOpRCtx op e1 => BinOp op e1 e
360
  | IfCtx e1 e2 => If e e1 e2
361
  | PairLCtx v2 => Pair e (Val v2)
362
  | PairRCtx e1 => Pair e1 e
363 364 365 366
  | FstCtx => Fst e
  | SndCtx => Snd e
  | InjLCtx => InjL e
  | InjRCtx => InjR e
367
  | CaseCtx e1 e2 => Case e e1 e2
Amin Timany's avatar
Amin Timany committed
368 369
  | AllocNLCtx v2 => AllocN e (Val v2)
  | AllocNRCtx e1 => AllocN e1 e
370
  | LoadCtx => Load e
371
  | StoreLCtx v2 => Store e (Val v2)
372
  | StoreRCtx e1 => Store e1 e
373 374
  | CasLCtx v1 v2 => CAS e (Val v1) (Val v2)
  | CasMCtx e0 v2 => CAS e0 e (Val v2)
375
  | CasRCtx e0 e1 => CAS e0 e1 e
376
  | FaaLCtx v2 => FAA e (Val v2)
377
  | FaaRCtx e1 => FAA e1 e
378 379
  | ProphLCtx v2 => ResolveProph e (of_val v2)
  | ProphRCtx e1 => ResolveProph e1 e
Ralf Jung's avatar
Ralf Jung committed
380 381
  end.

382
(** Substitution *)
383
Fixpoint subst (x : string) (v : val) (e : expr)  : expr :=
384
  match e with
385 386
  | Val _ => e
  | Var y => if decide (x = y) then Val v else Var y
387
  | Rec f y e =>
388 389 390 391 392 393 394 395 396 397 398 399
     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
400
  | AllocN e1 e2 => AllocN (subst x v e1) (subst x v e2)
401 402 403 404
  | Load e => Load (subst x v e)
  | Store e1 e2 => Store (subst x v e1) (subst x v e2)
  | CAS e0 e1 e2 => CAS (subst x v e0) (subst x v e1) (subst x v e2)
  | FAA e1 e2 => FAA (subst x v e1) (subst x v e2)
405
  | NewProph => NewProph
406
  | ResolveProph e1 e2 => ResolveProph (subst x v e1) (subst x v e2)
407
  end.
408

409 410
Definition subst' (mx : binder) (v : val) : expr  expr :=
  match mx with BNamed x => subst x v | BAnon => id end.
411

412
(** The stepping relation *)
413 414 415
Definition un_op_eval (op : un_op) (v : val) : option val :=
  match op, v with
  | NegOp, LitV (LitBool b) => Some $ LitV $ LitBool (negb b)
416
  | NegOp, LitV (LitInt n) => Some $ LitV $ LitInt (Z.lnot n)
417
  | MinusUnOp, LitV (LitInt n) => Some $ LitV $ LitInt (- n)
418 419 420
  | _, _ => None
  end.

Amin Timany's avatar
Amin Timany committed
421
Definition bin_op_eval_int (op : bin_op) (n1 n2 : Z) : option base_lit :=
422
  match op with
Amin Timany's avatar
Amin Timany committed
423 424 425 426 427 428 429 430 431 432 433 434 435 436
  | 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 *)
437 438 439 440 441 442 443 444 445 446 447
  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
448
  | OffsetOp => None (* Pointer arithmetic *)
449 450
  end.

451
Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
452
  if decide (op = EqOp) then Some $ LitV $ LitBool $ bool_decide (v1 = v2) else
453
  match v1, v2 with
Amin Timany's avatar
Amin Timany committed
454
  | LitV (LitInt n1), LitV (LitInt n2) => LitV <$> bin_op_eval_int op n1 n2
455
  | LitV (LitBool b1), LitV (LitBool b2) => LitV <$> bin_op_eval_bool op b1 b2
Amin Timany's avatar
Amin Timany committed
456
  | LitV (LitLoc l), LitV (LitInt off) => Some $ LitV $ LitLoc (l + off)
Robbert Krebbers's avatar
Robbert Krebbers committed
457
  | _, _ => None
458 459
  end.

460 461 462 463
(** 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
464
Definition vals_cas_compare_safe (vl v1 : val) : Prop :=
465 466
  val_is_unboxed vl  val_is_unboxed v1.
Arguments vals_cas_compare_safe !_ !_ /.
Ralf Jung's avatar
Ralf Jung committed
467

Ralf Jung's avatar
Ralf Jung committed
468
Definition state_upd_heap (f: gmap loc val  gmap loc val) (σ: state) : state :=
469
  {| heap := f σ.(heap); used_proph_id := σ.(used_proph_id) |}.
Ralf Jung's avatar
Ralf Jung committed
470
Arguments state_upd_heap _ !_ /.
Amin Timany's avatar
Amin Timany committed
471

Ralf Jung's avatar
Ralf Jung committed
472
Definition state_upd_used_proph_id (f: gset proph_id  gset proph_id) (σ: state) : state :=
473 474
  {| heap := σ.(heap); used_proph_id := f σ.(used_proph_id) |}.
Arguments state_upd_used_proph_id _ !_ /.
Ralf Jung's avatar
Ralf Jung committed
475

Amin Timany's avatar
Amin Timany committed
476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514
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.

515
(* [h] is added on the right here to make [state_init_heap_singleton] true. *)
Amin Timany's avatar
Amin Timany committed
516
Definition state_init_heap (l : loc) (n : Z) (v : val) (σ : state) : state :=
517 518 519 520 521 522 523 524
  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
525

Robbert Krebbers's avatar
Robbert Krebbers committed
526
Inductive head_step : expr  state  list observation  expr  state  list expr  Prop :=
527 528 529 530 531 532 533 534 535 536 537 538
  | 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
539
     un_op_eval op v = Some v' 
540 541
     head_step (UnOp op (Val v)) σ [] (Val v') σ []
  | BinOpS op v1 v2 v' σ :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
542
     bin_op_eval op v1 v2 = Some v' 
543
     head_step (BinOp op (Val v1) (Val v2)) σ [] (Val v') σ []
544
  | IfTrueS e1 e2 σ :
545
     head_step (If (Val $ LitV $ LitBool true) e1 e2) σ [] e1 σ []
546
  | IfFalseS e1 e2 σ :
547 548 549 550 551 552 553 554 555
     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)) σ []
556
  | ForkS e σ:
557
     head_step (Fork e) σ [] (Val $ LitV LitUnit) σ [e]
Amin Timany's avatar
Amin Timany committed
558 559 560 561
  | AllocNS n v σ l :
     0 < n 
     ( i, 0  i  i < n  σ.(heap) !! (l + i) = None) 
     head_step (AllocN (Val $ LitV $ LitInt n) (Val v)) σ
562
               []
Amin Timany's avatar
Amin Timany committed
563
               (Val $ LitV $ LitLoc l) (state_init_heap l n v σ)
Ralf Jung's avatar
Ralf Jung committed
564
               []
565
  | LoadS l v σ :
Ralf Jung's avatar
Ralf Jung committed
566
     σ.(heap) !! l = Some v 
567 568 569 570
     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)) σ
571
               []
572
               (Val $ LitV LitUnit) (state_upd_heap <[l:=v]> σ)
Ralf Jung's avatar
Ralf Jung committed
573
               []
574
  | CasFailS l v1 v2 vl σ :
Ralf Jung's avatar
Ralf Jung committed
575
     σ.(heap) !! l = Some vl  vl  v1 
Ralf Jung's avatar
Ralf Jung committed
576
     vals_cas_compare_safe vl v1 
577 578 579
     head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ []
               (Val $ LitV $ LitBool false) σ []
  | CasSucS l v1 v2 σ :
Ralf Jung's avatar
Ralf Jung committed
580
     σ.(heap) !! l = Some v1 
Ralf Jung's avatar
Ralf Jung committed
581
     vals_cas_compare_safe v1 v1 
582
     head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
583
               []
584
               (Val $ LitV $ LitBool true) (state_upd_heap <[l:=v2]> σ)
Ralf Jung's avatar
Ralf Jung committed
585
               []
586
  | FaaS l i1 i2 σ :
Ralf Jung's avatar
Ralf Jung committed
587
     σ.(heap) !! l = Some (LitV (LitInt i1)) 
588
     head_step (FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2)) σ
589
               []
590
               (Val $ LitV $ LitInt i1) (state_upd_heap <[l:=LitV (LitInt (i1 + i2))]>σ)
Ralf Jung's avatar
Ralf Jung committed
591
               []
592
  | NewProphS σ p :
593
     p  σ.(used_proph_id) 
Ralf Jung's avatar
Ralf Jung committed
594
     head_step NewProph σ
595
               []
596
               (Val $ LitV $ LitProphecy p) (state_upd_used_proph_id ({[ p ]} ) σ)
Ralf Jung's avatar
Ralf Jung committed
597
               []
598
  | ResolveProphS p v σ :
599 600 601
     head_step (ResolveProph (Val $ LitV $ LitProphecy p) (Val v)) σ
               [(p, v)]
               (Val $ LitV LitUnit) σ [].
Ralf Jung's avatar
Ralf Jung committed
602

603
(** Basic properties about the language *)
604
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
605
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
606

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

611
Lemma val_head_stuck e1 σ1 κ e2 σ2 efs : head_step e1 σ1 κ e2 σ2 efs  to_val e1 = None.
612
Proof. destruct 1; naive_solver. Qed.
613

614 615
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).
616
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
617

618
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
619
  to_val e1 = None  to_val e2 = None 
620
  fill_item Ki1 e1 = fill_item Ki2 e2  Ki1 = Ki2.
621
Proof. destruct Ki1, Ki2; intros; by simplify_eq. Qed.
622

Amin Timany's avatar
Amin Timany committed
623 624 625 626 627 628 629 630 631 632 633
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.
634

635 636
Lemma new_proph_id_fresh σ :
  let p := fresh σ.(used_proph_id) in
637
  head_step NewProph σ [] (Val $ LitV $ LitProphecy p) (state_upd_used_proph_id ({[ p ]} ) σ) [].
638 639
Proof. constructor. apply is_fresh. Qed.

640 641 642 643 644
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.
645 646 647
End heap_lang.

(** Language *)
648 649 650
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.
651

652
(* Prefer heap_lang names over ectx_language names. *)
653
Export heap_lang.
654 655 656 657 658 659 660 661 662

(** 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).
Amin Timany's avatar
Amin Timany committed
663
Notation Alloc e := (AllocN (Val $ LitV $ LitInt 1) e) (only parsing).
664

665 666 667
(* Skip should be atomic, we sometimes open invariants around
   it. Hence, we need to explicitly use LamV instead of e.g., Seq. *)
Notation Skip := (App (Val $ LamV BAnon (Val $ LitV LitUnit)) (Val $ LitV LitUnit)).