lang.v 21 KB
Newer Older
1
From iris.program_logic Require Export ectx_language.
2
3
From iris.prelude Require Export strings.
From iris.prelude Require Import gmap.
4

5
Module heap_lang.
6
7
Open Scope Z_scope.

8
(** Expressions and vals. *)
9
Definition loc := positive. (* Really, any countable type. *)
Ralf Jung's avatar
Ralf Jung committed
10

11
Inductive base_lit : Set :=
12
  | LitInt (n : Z) | LitBool (b : bool) | LitUnit.
13
Inductive un_op : Set :=
14
  | NegOp | MinusUnOp.
15
16
17
Inductive bin_op : Set :=
  | PlusOp | MinusOp | LeOp | LtOp | EqOp.

18
Inductive binder := BAnon | BNamed : string  binder.
Ralf Jung's avatar
Ralf Jung committed
19
20
Delimit Scope binder_scope with bind.
Bind Scope binder_scope with binder.
21

22
23
24
25
26
27
28
29
30
31
32
33
34
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).
Instance binder_dec_eq (x1 x2 : binder) : Decision (x1 = x2).
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.

Ralf Jung's avatar
Ralf Jung committed
35
36
37
38
39
40
(** A typeclass for whether a variable is bound in a given
   context. Making this a typeclass means we can use tpeclass search
   to program solving these constraints, so this becomes extensible.
   Also, since typeclass search runs *after* unification, Coq has already
   inferred the X for us; if we were to go for embedded proof terms ot
   tactics, Coq would do things in the wrong order. *)
41
42
Class VarBound (x : string) (X : list string) :=
  var_bound : bool_decide (x  X).
43
44
(* There is no need to restrict this hint to terms without evars, [vm_compute]
will fail in case evars are arround. *)
45
46
47
48
49
50
51
52
53
Hint Extern 0 (VarBound _ _) => vm_compute; exact I : typeclass_instances. 

Instance var_bound_proof_irrel x X : ProofIrrel (VarBound x X).
Proof. rewrite /VarBound. apply _. Qed.
Instance set_unfold_var_bound x X P :
  SetUnfold (x  X) P  SetUnfold (VarBound x X) P.
Proof.
  constructor. by rewrite /VarBound bool_decide_spec (set_unfold (x  X) P).
Qed.
54

55
Inductive expr (X : list string) :=
56
  (* Base lambda calculus *)
Ralf Jung's avatar
Ralf Jung committed
57
58
59
60
61
62
63
      (* Var is the only place where the terms contain a proof. The fact that they
       contain a proof at all is suboptimal, since this means two seeminlgy
       convertible terms could differ in their proofs. However, this also has
       some advantages:
       * We can make the [X] an index, so we can do non-dependent match.
       * In expr_weaken, we can push the proof all the way into Var, making
         sure that proofs never block computation. *)
64
65
66
  | Var (x : string) `{VarBound x X}
  | Rec (f x : binder) (e : expr (f :b: x :b: X))
  | App (e1 e2 : expr X)
67
68
  (* Base types and their operations *)
  | Lit (l : base_lit)
69
70
71
  | UnOp (op : un_op) (e : expr X)
  | BinOp (op : bin_op) (e1 e2 : expr X)
  | If (e0 e1 e2 : expr X)
72
  (* Products *)
73
74
75
  | Pair (e1 e2 : expr X)
  | Fst (e : expr X)
  | Snd (e : expr X)
76
  (* Sums *)
77
78
79
  | InjL (e : expr X)
  | InjR (e : expr X)
  | Case (e0 : expr X) (e1 : expr X) (e2 : expr X)
80
  (* Concurrency *)
81
  | Fork (e : expr X)
82
83
  (* Heap *)
  | Loc (l : loc)
84
85
86
  | Alloc (e : expr X)
  | Load (e : expr X)
  | Store (e1 : expr X) (e2 : expr X)
87
  | CAS (e0 : expr X) (e1 : expr X) (e2 : expr X).
Ralf Jung's avatar
Ralf Jung committed
88

89
90
Bind Scope expr_scope with expr.
Delimit Scope expr_scope with E.
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
Arguments Var {_} _ {_}.
Arguments Rec {_} _ _ _%E.
Arguments App {_} _%E _%E.
Arguments Lit {_} _.
Arguments UnOp {_} _ _%E.
Arguments BinOp {_} _ _%E _%E.
Arguments If {_} _%E _%E _%E.
Arguments Pair {_} _%E _%E.
Arguments Fst {_} _%E.
Arguments Snd {_} _%E.
Arguments InjL {_} _%E.
Arguments InjR {_} _%E.
Arguments Case {_} _%E _%E _%E.
Arguments Fork {_} _%E.
Arguments Loc {_} _.
Arguments Alloc {_} _%E.
Arguments Load {_} _%E.
Arguments Store {_} _%E _%E.
109
Arguments CAS {_} _%E _%E _%E.
110

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

119
120
Bind Scope val_scope with val.
Delimit Scope val_scope with V.
121
122
123
Arguments PairV _%V _%V.
Arguments InjLV _%V.
Arguments InjRV _%V.
124

125
Definition signal : val := RecV BAnon (BNamed "x") (Store (Var "x") (Lit (LitInt 1))).
126

127
Fixpoint of_val (v : val) : expr [] :=
Ralf Jung's avatar
Ralf Jung committed
128
  match v with
129
  | RecV f x e => Rec f x e
130
  | LitV l => Lit l
131
132
133
  | PairV v1 v2 => Pair (of_val v1) (of_val v2)
  | InjLV v => InjL (of_val v)
  | InjRV v => InjR (of_val v)
134
  | LocV l => Loc l
Ralf Jung's avatar
Ralf Jung committed
135
  end.
136
137

Fixpoint to_val (e : expr []) : option val :=
138
  match e with
139
  | Rec f x e => Some (RecV f x e)
140
  | Lit l => Some (LitV l)
141
142
143
  | 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
144
  | Loc l => Some (LocV l)
Ralf Jung's avatar
Ralf Jung committed
145
  | _ => None
146
147
  end.

148
149
(** The state: heaps of vals. *)
Definition state := gmap loc val.
Ralf Jung's avatar
Ralf Jung committed
150

151
(** Evaluation contexts *)
152
Inductive ectx_item :=
153
  | AppLCtx (e2 : expr [])
154
  | AppRCtx (v1 : val)
155
  | UnOpCtx (op : un_op)
156
  | BinOpLCtx (op : bin_op) (e2 : expr [])
157
  | BinOpRCtx (op : bin_op) (v1 : val)
158
159
  | IfCtx (e1 e2 : expr [])
  | PairLCtx (e2 : expr [])
160
161
162
163
164
  | PairRCtx (v1 : val)
  | FstCtx
  | SndCtx
  | InjLCtx
  | InjRCtx
165
  | CaseCtx (e1 : expr []) (e2 : expr [])
166
167
  | AllocCtx
  | LoadCtx
168
  | StoreLCtx (e2 : expr [])
169
  | StoreRCtx (v1 : val)
170
171
  | CasLCtx (e1 : expr [])  (e2 : expr [])
  | CasMCtx (v0 : val) (e2 : expr [])
172
  | CasRCtx (v0 : val) (v1 : val).
173

174
Notation ectx := (list ectx_item).
175

176
Definition fill_item (Ki : ectx_item) (e : expr []) : expr [] :=
177
178
179
  match Ki with
  | AppLCtx e2 => App e e2
  | AppRCtx v1 => App (of_val v1) e
180
181
182
183
  | UnOpCtx op => UnOp op e
  | BinOpLCtx op e2 => BinOp op e e2
  | BinOpRCtx op v1 => BinOp op (of_val v1) e
  | IfCtx e1 e2 => If e e1 e2
184
185
186
187
188
189
  | PairLCtx e2 => Pair e e2
  | PairRCtx v1 => Pair (of_val v1) e
  | FstCtx => Fst e
  | SndCtx => Snd e
  | InjLCtx => InjL e
  | InjRCtx => InjR e
190
  | CaseCtx e1 e2 => Case e e1 e2
191
192
193
194
  | AllocCtx => Alloc e
  | LoadCtx => Load e
  | StoreLCtx e2 => Store e e2
  | StoreRCtx v1 => Store (of_val v1) e
195
196
197
  | CasLCtx e1 e2 => CAS e e1 e2
  | CasMCtx v0 e2 => CAS (of_val v0) e e2
  | CasRCtx v0 v1 => CAS (of_val v0) (of_val v1) e
Ralf Jung's avatar
Ralf Jung committed
198
  end.
199
Definition fill (K : ectx) (e : expr []) : expr [] := fold_right fill_item e K.
Ralf Jung's avatar
Ralf Jung committed
200

201
(** Substitution *)
202
(** We have [subst' e BAnon v = e] to deal with anonymous binders *)
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
Lemma wexpr_rec_prf {X Y} (H : X `included` Y) {f x} :
  f :b: x :b: X `included` f :b: x :b: Y.
Proof. set_solver. Qed.

Program Fixpoint wexpr {X Y} (H : X `included` Y) (e : expr X) : expr Y :=
  match e return expr Y with
  | Var x _ => @Var _ x _
  | Rec f x e => Rec f x (wexpr (wexpr_rec_prf H) e)
  | App e1 e2 => App (wexpr H e1) (wexpr H e2)
  | Lit l => Lit l
  | UnOp op e => UnOp op (wexpr H e)
  | BinOp op e1 e2 => BinOp op (wexpr H e1) (wexpr H e2)
  | If e0 e1 e2 => If (wexpr H e0) (wexpr H e1) (wexpr H e2)
  | Pair e1 e2 => Pair (wexpr H e1) (wexpr H e2)
  | Fst e => Fst (wexpr H e)
  | Snd e => Snd (wexpr H e)
  | InjL e => InjL (wexpr H e)
  | InjR e => InjR (wexpr H e)
  | Case e0 e1 e2 => Case (wexpr H e0) (wexpr H e1) (wexpr H e2)
  | Fork e => Fork (wexpr H e)
  | Loc l => Loc l
  | Alloc e => Alloc (wexpr H e)
  | Load  e => Load (wexpr H e)
  | Store e1 e2 => Store (wexpr H e1) (wexpr H e2)
227
  | CAS e0 e1 e2 => CAS (wexpr H e0) (wexpr H e1) (wexpr H e2)
228
229
230
  end.
Solve Obligations with set_solver.

Robbert Krebbers's avatar
Robbert Krebbers committed
231
Definition wexpr' {X} (e : expr []) : expr X := wexpr (included_nil _) e.
232

233
234
235
Definition of_val' {X} (v : val) : expr X := wexpr (included_nil _) (of_val v).

Lemma wsubst_rec_true_prf {X Y x} (H : X `included` x :: Y) {f y}
Robbert Krebbers's avatar
Robbert Krebbers committed
236
    (Hfy : BNamed x  f  BNamed x  y) :
237
238
239
240
241
242
243
244
245
246
  f :b: y :b: X `included` x :: f :b: y :b: Y.
Proof. set_solver. Qed.
Lemma wsubst_rec_false_prf {X Y x} (H : X `included` x :: Y) {f y}
    (Hfy : ¬(BNamed x  f  BNamed x  y)) :
  f :b: y :b: X `included` f :b: y :b: Y.
Proof. move: Hfy=>/not_and_l [/dec_stable|/dec_stable]; set_solver. Qed.

Program Fixpoint wsubst {X Y} (x : string) (es : expr [])
    (H : X `included` x :: Y) (e : expr X)  : expr Y :=
  match e return expr Y with
247
  | Var y _ => if decide (x = y) then wexpr' es else @Var _ y _
248
  | Rec f y e =>
249
250
251
252
253
     Rec f y $ match decide (BNamed x  f  BNamed x  y) return _ with
               | left Hfy => wsubst x es (wsubst_rec_true_prf H Hfy) e
               | right Hfy => wexpr (wsubst_rec_false_prf H Hfy) e
               end
  | App e1 e2 => App (wsubst x es H e1) (wsubst x es H e2)
254
  | Lit l => Lit l
255
256
257
258
259
260
261
262
  | UnOp op e => UnOp op (wsubst x es H e)
  | BinOp op e1 e2 => BinOp op (wsubst x es H e1) (wsubst x es H e2)
  | If e0 e1 e2 => If (wsubst x es H e0) (wsubst x es H e1) (wsubst x es H e2)
  | Pair e1 e2 => Pair (wsubst x es H e1) (wsubst x es H e2)
  | Fst e => Fst (wsubst x es H e)
  | Snd e => Snd (wsubst x es H e)
  | InjL e => InjL (wsubst x es H e)
  | InjR e => InjR (wsubst x es H e)
263
  | Case e0 e1 e2 =>
264
265
     Case (wsubst x es H e0) (wsubst x es H e1) (wsubst x es H e2)
  | Fork e => Fork (wsubst x es H e)
266
  | Loc l => Loc l
267
268
269
  | Alloc e => Alloc (wsubst x es H e)
  | Load e => Load (wsubst x es H e)
  | Store e1 e2 => Store (wsubst x es H e1) (wsubst x es H e2)
270
  | CAS e0 e1 e2 => CAS (wsubst x es H e0) (wsubst x es H e1) (wsubst x es H e2)
271
  end.
272
273
274
275
276
277
Solve Obligations with set_solver.

Definition subst {X} (x : string) (es : expr []) (e : expr (x :: X)) : expr X :=
  wsubst x es (λ z, id) e.
Definition subst' {X} (mx : binder) (es : expr []) : expr (mx :b: X)  expr X :=
  match mx with BNamed x => subst x es | BAnon => id end.
278

279
(** The stepping relation *)
280
281
Definition un_op_eval (op : un_op) (l : base_lit) : option base_lit :=
  match op, l with
282
  | NegOp, LitBool b => Some (LitBool (negb b))
283
  | MinusUnOp, LitInt n => Some (LitInt (- n))
284
285
286
287
288
  | _, _ => None
  end.

Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
  match op, l1, l2 with
289
290
291
292
293
  | PlusOp, LitInt n1, LitInt n2 => Some $ LitInt (n1 + n2)
  | MinusOp, LitInt n1, LitInt n2 => Some $ LitInt (n1 - n2)
  | LeOp, LitInt n1, LitInt n2 => Some $ LitBool $ bool_decide (n1  n2)
  | LtOp, LitInt n1, LitInt n2 => Some $ LitBool $ bool_decide (n1 < n2)
  | EqOp, LitInt n1, LitInt n2 => Some $ LitBool $ bool_decide (n1 = n2)
294
295
296
  | _, _, _ => None
  end.

297
298
Inductive head_step : expr []  state  expr []  state  option (expr [])  Prop :=
  | BetaS f x e1 e2 v2 e' σ :
299
     to_val e2 = Some v2 
300
301
     e' = subst' x (of_val v2) (subst' f (Rec f x e1) e1) 
     head_step (App (Rec f x e1) e2) σ e' σ None
302
  | UnOpS op l l' σ :
303
304
     un_op_eval op l = Some l'  
     head_step (UnOp op (Lit l)) σ (Lit l') σ None
305
  | BinOpS op l1 l2 l' σ :
306
307
308
     bin_op_eval op l1 l2 = Some l'  
     head_step (BinOp op (Lit l1) (Lit l2)) σ (Lit l') σ None
  | IfTrueS e1 e2 σ :
Ralf Jung's avatar
Ralf Jung committed
309
     head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ None
310
  | IfFalseS e1 e2 σ :
Ralf Jung's avatar
Ralf Jung committed
311
     head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ None
312
313
314
315
316
317
  | FstS e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     head_step (Fst (Pair e1 e2)) σ e1 σ None
  | SndS e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     head_step (Snd (Pair e1 e2)) σ e2 σ None
318
  | CaseLS e0 v0 e1 e2 σ :
319
     to_val e0 = Some v0 
320
321
     head_step (Case (InjL e0) e1 e2) σ (App e1 e0) σ None
  | CaseRS e0 v0 e1 e2 σ :
322
     to_val e0 = Some v0 
323
     head_step (Case (InjR e0) e1 e2) σ (App e2 e0) σ None
324
  | ForkS e σ:
325
     head_step (Fork e) σ (Lit LitUnit) σ (Some e)
326
327
328
329
330
331
332
333
  | AllocS e v σ l :
     to_val e = Some v  σ !! l = None 
     head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None
  | LoadS l v σ :
     σ !! l = Some v 
     head_step (Load (Loc l)) σ (of_val v) σ None
  | StoreS l e v σ :
     to_val e = Some v  is_Some (σ !! l) 
334
     head_step (Store (Loc l) e) σ (Lit LitUnit) (<[l:=v]>σ) None
335
336
337
  | CasFailS l e1 v1 e2 v2 vl σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some vl  vl  v1 
338
     head_step (CAS (Loc l) e1 e2) σ (Lit $ LitBool false) σ None
339
340
341
  | CasSucS l e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some v1 
342
     head_step (CAS (Loc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None.
Ralf Jung's avatar
Ralf Jung committed
343

344
(** Atomic expressions *)
345
Definition atomic (e: expr []) : Prop :=
346
347
348
349
  match e with
  | Alloc e => is_Some (to_val e)
  | Load e => is_Some (to_val e)
  | Store e1 e2 => is_Some (to_val e1)  is_Some (to_val e2)
350
  | CAS e0 e1 e2 => is_Some (to_val e0)  is_Some (to_val e1)  is_Some (to_val e2)
Ralf Jung's avatar
Ralf Jung committed
351
352
  (* Make "skip" atomic *)
  | App (Rec _ _ (Lit _)) (Lit _) => True
353
354
  | _ => False
  end.
355

356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
(** Substitution *)
Lemma var_proof_irrel X x H1 H2 : @Var X x H1 = @Var X x H2.
Proof. f_equal. by apply (proof_irrel _). Qed.

Lemma wexpr_id X (H : X `included` X) e : wexpr H e = e.
Proof. induction e; f_equal/=; auto. by apply (proof_irrel _). Qed.
Lemma wexpr_proof_irrel X Y (H1 H2 : X `included` Y) e : wexpr H1 e = wexpr H2 e.
Proof.
  revert Y H1 H2; induction e; simpl; auto using var_proof_irrel with f_equal.
Qed.
Lemma wexpr_wexpr X Y Z (H1 : X `included` Y) (H2 : Y `included` Z) H3 e :
  wexpr H2 (wexpr H1 e) = wexpr H3 e.
Proof.
  revert Y Z H1 H2 H3.
  induction e; simpl; auto using var_proof_irrel with f_equal.
Qed.
Lemma wexpr_wexpr' X Y Z (H1 : X `included` Y) (H2 : Y `included` Z) e :
  wexpr H2 (wexpr H1 e) = wexpr (transitivity H1 H2) e.
Proof. apply wexpr_wexpr. Qed.

Lemma wsubst_proof_irrel X Y x es (H1 H2 : X `included` x :: Y) e :
  wsubst x es H1 e = wsubst x es H2 e.
Proof.
  revert Y H1 H2; induction e; simpl; intros; repeat case_decide;
    auto using var_proof_irrel, wexpr_proof_irrel with f_equal.
Qed.
Lemma wexpr_wsubst X Y Z x es (H1: X `included` x::Y) (H2: Y `included` Z) H3 e:
  wexpr H2 (wsubst x es H1 e) = wsubst x es H3 e.
Proof.
  revert Y Z H1 H2 H3.
  induction e; intros; repeat (case_decide || simplify_eq/=);
387
    unfold wexpr'; auto using var_proof_irrel, wexpr_wexpr with f_equal.
388
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
Qed.
Lemma wsubst_wexpr X Y Z x es (H1: X `included` Y) (H2: Y `included` x::Z) H3 e:
  wsubst x es H2 (wexpr H1 e) = wsubst x es H3 e.
Proof.
  revert Y Z H1 H2 H3.
  induction e; intros; repeat (case_decide || simplify_eq/=);
    auto using var_proof_irrel, wexpr_wexpr with f_equal.
Qed.
Lemma wsubst_wexpr' X Y Z x es (H1: X `included` Y) (H2: Y `included` x::Z) e:
  wsubst x es H2 (wexpr H1 e) = wsubst x es (transitivity H1 H2) e.
Proof. apply wsubst_wexpr. Qed.

Lemma wsubst_closed X Y x es (H1 : X `included` x :: Y) H2 (e : expr X) :
  x  X  wsubst x es H1 e = wexpr H2 e.
Proof.
  revert Y H1 H2.
  induction e; intros; repeat (case_decide || simplify_eq/=);
    auto using var_proof_irrel, wexpr_proof_irrel with f_equal set_solver.
  exfalso; set_solver.
Qed.
Lemma wsubst_closed_nil x es H (e : expr []) : wsubst x es H e = e.
Proof.
  rewrite -{2}(wexpr_id _ (reflexivity []) e).
  apply wsubst_closed, not_elem_of_nil.
Qed.

414
415
(** Basic properties about the language *)
Lemma to_of_val v : to_val (of_val v) = Some v.
416
Proof. by induction v; simplify_option_eq. Qed.
417

418
Lemma of_to_val e v : to_val e = Some v  of_val v = e.
419
Proof.
420
421
422
423
424
425
426
  revert e v. cut ( X (e : expr X) (H : X = ) v,
    to_val (eq_rect _ expr e _ H) = Some v  of_val v = eq_rect _ expr e _ H).
  { intros help e v. apply (help  e eq_refl). }
  intros X e; induction e; intros HX ??; simplify_option_eq;
    repeat match goal with
    | IH :  _ :  = , _ |- _ => specialize (IH eq_refl); simpl in IH
    end; auto with f_equal.
427
Qed.
428

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

432
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
433
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
434

435
Instance fill_inj K : Inj (=) (=) (fill K).
436
Proof. red; induction K as [|Ki K IH]; naive_solver. Qed.
437

438
Lemma fill_val K e : is_Some (to_val (fill K e))  is_Some (to_val e).
439
Proof.
440
  intros [v' Hv']; revert v' Hv'.
441
  induction K as [|[]]; intros; simplify_option_eq; eauto.
442
Qed.
443

444
445
Lemma fill_not_val K e : to_val e = None  to_val (fill K e) = None.
Proof. rewrite !eq_None_not_Some; eauto using fill_val. Qed.
446

447
Lemma val_stuck e1 σ1 e2 σ2 ef :
448
449
  head_step e1 σ1 e2 σ2 ef  to_val e1 = None.
Proof. destruct 1; naive_solver. Qed.
450

451
452
Lemma atomic_not_val e : atomic e  to_val e = None.
Proof. destruct e; naive_solver. Qed.
453

454
455
Lemma atomic_fill_item Ki e : atomic (fill_item Ki e)  is_Some (to_val e).
Proof.
456
  intros. destruct Ki; simplify_eq/=; destruct_and?;
457
458
459
    repeat (case_match || contradiction); eauto.
Qed.

460
Lemma atomic_fill K e : atomic (fill K e)  to_val e = None  K = [].
461
Proof.
462
463
  destruct K as [|Ki K]; [done|].
  rewrite eq_None_not_Some=> /= ? []; eauto using atomic_fill_item, fill_val.
464
Qed.
465

466
Lemma atomic_step e1 σ1 e2 σ2 ef :
467
  atomic e1  head_step e1 σ1 e2 σ2 ef  is_Some (to_val e2).
Ralf Jung's avatar
Ralf Jung committed
468
Proof.
469
  destruct 2; simpl; rewrite ?to_of_val; try by eauto. subst.
470
  unfold subst'; repeat (case_match || contradiction || simplify_eq/=); eauto.
Ralf Jung's avatar
Ralf Jung committed
471
Qed.
472

473
Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef :
474
  head_step (fill_item Ki e) σ1 e2 σ2 ef  is_Some (to_val e).
475
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; eauto. Qed.
476

477
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
478
  to_val e1 = None  to_val e2 = None 
479
  fill_item Ki1 e1 = fill_item Ki2 e2  Ki1 = Ki2.
480
Proof.
481
  destruct Ki1, Ki2; intros; try discriminate; simplify_eq/=;
482
    repeat match goal with
483
484
    | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
    end; auto.
Ralf Jung's avatar
Ralf Jung committed
485
Qed.
486

487
488
489
490
491
(* When something does a step, and another decomposition of the same expression
has a non-val [e] in the hole, then [K] is a left sub-context of [K'] - in
other words, [e] also contains the reducible expression *)
Lemma step_by_val K K' e1 e1' σ1 e2 σ2 ef :
  fill K e1 = fill K' e1'  to_val e1 = None  head_step e1' σ1 e2 σ2 ef 
492
  exists K'', K' = K ++ K''. (* K `prefix_of` K' *)
493
Proof.
494
  intros Hfill Hred Hnval; revert K' Hfill.
495
  induction K as [|Ki K IH]; simpl; intros K' Hfill; first by eauto.
496
  destruct K' as [|Ki' K']; simplify_eq/=.
Ralf Jung's avatar
Ralf Jung committed
497
  { exfalso; apply (eq_None_not_Some (to_val (fill K e1)));
498
499
      eauto using fill_not_val, head_ctx_step_val. }
  cut (Ki = Ki'); [naive_solver eauto using prefix_of_cons|].
500
  eauto using fill_item_no_val_inj, val_stuck, fill_not_val.
501
Qed.
502

503
504
505
Lemma alloc_fresh e v σ :
  let l := fresh (dom _ σ) in
  to_val e = Some v  head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None.
506
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
507

Ralf Jung's avatar
Ralf Jung committed
508
(** Equality and other typeclass stuff *)
509
510
511
512
513
514
Instance base_lit_dec_eq (l1 l2 : base_lit) : Decision (l1 = l2).
Proof. solve_decision. Defined.
Instance un_op_dec_eq (op1 op2 : un_op) : Decision (op1 = op2).
Proof. solve_decision. Defined.
Instance bin_op_dec_eq (op1 op2 : bin_op) : Decision (op1 = op2).
Proof. solve_decision. Defined.
515

516
517
518
519
520
521
522
523
524
525
526
527
Fixpoint expr_beq {X Y} (e : expr X) (e' : expr Y) : bool :=
  match e, e' with
  | Var x _, Var x' _ => bool_decide (x = x')
  | Rec f x e, Rec f' x' e' =>
     bool_decide (f = f') && bool_decide (x = x') && expr_beq e e'
  | App e1 e2, App e1' e2' | Pair e1 e2, Pair e1' e2' |
    Store e1 e2, Store e1' e2' => expr_beq e1 e1' && expr_beq e2 e2'
  | Lit l, Lit l' => bool_decide (l = l')
  | UnOp op e, UnOp op' e' => bool_decide (op = op') && expr_beq e e'
  | BinOp op e1 e2, BinOp op' e1' e2' =>
     bool_decide (op = op') && expr_beq e1 e1' && expr_beq e2 e2'
  | If e0 e1 e2, If e0' e1' e2' | Case e0 e1 e2, Case e0' e1' e2' |
528
    CAS e0 e1 e2, CAS e0' e1' e2' =>
529
530
531
532
533
     expr_beq e0 e0' && expr_beq e1 e1' && expr_beq e2 e2'
  | Fst e, Fst e' | Snd e, Snd e' | InjL e, InjL e' | InjR e, InjR e' |
    Fork e, Fork e' | Alloc e, Alloc e' | Load e, Load e' => expr_beq e e'
  | Loc l, Loc l' => bool_decide (l = l')
  | _, _ => false
534
  end.
535
Lemma expr_beq_correct {X} (e1 e2 : expr X) : expr_beq e1 e2  e1 = e2.
536
Proof.
537
538
539
540
  split.
  * revert e2; induction e1; intros [] * ?; simpl in *;
      destruct_and?; subst; repeat f_equal/=; auto; try apply proof_irrel.
  * intros ->. induction e2; naive_solver.
541
Qed.
542
Instance expr_dec_eq {X} (e1 e2 : expr X) : Decision (e1 = e2).
543
Proof.
544
545
546
 refine (cast_if (decide (expr_beq e1 e2))); by rewrite -expr_beq_correct.
Defined.
Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2).
547
Proof.
548
549
 refine (cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
Defined.
Ralf Jung's avatar
Ralf Jung committed
550
551
552

Instance expr_inhabited X : Inhabited (expr X) := populate (Lit LitUnit).
Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
553
554
555
End heap_lang.

(** Language *)
Robbert Krebbers's avatar
Robbert Krebbers committed
556
557
558
559
560
561
562
Program Instance heap_ectx_lang :
  EctxLanguage
    (heap_lang.expr []) heap_lang.val heap_lang.ectx heap_lang.state := {|
  of_val := heap_lang.of_val; to_val := heap_lang.to_val;
  empty_ectx := []; comp_ectx := (++); fill := heap_lang.fill; 
  atomic := heap_lang.atomic; head_step := heap_lang.head_step;
|}.
563
Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
564
  heap_lang.val_stuck, heap_lang.atomic_not_val, heap_lang.atomic_step,
Robbert Krebbers's avatar
Robbert Krebbers committed
565
  heap_lang.fill_not_val, heap_lang.atomic_fill,
566
  heap_lang.step_by_val, fold_right_app, app_eq_nil.
567

568
Canonical Structure heap_lang := ectx_lang heap_ectx_lang.
569
570
571

Global Instance heap_lang_ctx_item Ki :
  LanguageCtx heap_lang (heap_lang.fill_item Ki).
572
Proof. change (LanguageCtx heap_lang (heap_lang.fill [Ki])). apply _. Qed.
573

574
(* Prefer heap_lang names over ectx_language names. *)
575
Export heap_lang.