lang.v 19.5 KB
Newer Older
1
From iris.program_logic Require Export ectx_language ectxi_language.
2
From iris.algebra Require Export cofe.
3
4
From iris.prelude Require Export strings.
From iris.prelude Require Import gmap.
5

6
Module heap_lang.
7
8
Open Scope Z_scope.

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

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

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

23
24
25
26
27
28
29
30
31
32
33
34
35
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
36
(** A typeclass for whether a variable is bound in a given
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
37
   context. Making this a typeclass means we can use typeclass search
Ralf Jung's avatar
Ralf Jung committed
38
39
40
41
   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. *)
42
43
Class VarBound (x : string) (X : list string) :=
  var_bound : bool_decide (x  X).
44
45
(* There is no need to restrict this hint to terms without evars, [vm_compute]
will fail in case evars are arround. *)
46
47
48
49
50
51
52
53
54
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.
55

56
Inductive expr (X : list string) :=
57
  (* Base lambda calculus *)
Ralf Jung's avatar
Ralf Jung committed
58
59
60
61
62
63
64
      (* 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. *)
65
66
67
  | Var (x : string) `{VarBound x X}
  | Rec (f x : binder) (e : expr (f :b: x :b: X))
  | App (e1 e2 : expr X)
68
69
  (* Base types and their operations *)
  | Lit (l : base_lit)
70
71
72
  | UnOp (op : un_op) (e : expr X)
  | BinOp (op : bin_op) (e1 e2 : expr X)
  | If (e0 e1 e2 : expr X)
73
  (* Products *)
74
75
76
  | Pair (e1 e2 : expr X)
  | Fst (e : expr X)
  | Snd (e : expr X)
77
  (* Sums *)
78
79
80
  | InjL (e : expr X)
  | InjR (e : expr X)
  | Case (e0 : expr X) (e1 : expr X) (e2 : expr X)
81
  (* Concurrency *)
82
  | Fork (e : expr X)
83
  (* Heap *)
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
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 Alloc {_} _%E.
Arguments Load {_} _%E.
Arguments Store {_} _%E _%E.
108
Arguments CAS {_} _%E _%E _%E.
109

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

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

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

Fixpoint to_val (e : expr []) : option val :=
133
  match e with
134
  | Rec f x e => Some (RecV f x e)
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
(** The state: heaps of vals. *)
Definition state := gmap loc val.
Ralf Jung's avatar
Ralf Jung committed
144

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

168
Definition fill_item (Ki : ectx_item) (e : expr []) : expr [] :=
169
170
171
  match Ki with
  | AppLCtx e2 => App e e2
  | AppRCtx v1 => App (of_val v1) e
172
173
174
175
  | 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
176
177
178
179
180
181
  | PairLCtx e2 => Pair e e2
  | PairRCtx v1 => Pair (of_val v1) e
  | FstCtx => Fst e
  | SndCtx => Snd e
  | InjLCtx => InjL e
  | InjRCtx => InjR e
182
  | CaseCtx e1 e2 => Case e e1 e2
183
184
185
186
  | AllocCtx => Alloc e
  | LoadCtx => Load e
  | StoreLCtx e2 => Store e e2
  | StoreRCtx v1 => Store (of_val v1) e
187
188
189
  | 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
190
191
  end.

192
(** Substitution *)
193
(** We have [subst' e BAnon v = e] to deal with anonymous binders *)
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
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)
  | Alloc e => Alloc (wexpr H e)
  | Load  e => Load (wexpr H e)
  | Store e1 e2 => Store (wexpr H e1) (wexpr H e2)
217
  | CAS e0 e1 e2 => CAS (wexpr H e0) (wexpr H e1) (wexpr H e2)
218
219
220
  end.
Solve Obligations with set_solver.

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

223
224
225
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
226
    (Hfy : BNamed x  f  BNamed x  y) :
227
228
229
230
231
232
233
234
235
236
  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
237
  | Var y _ => if decide (x = y) then wexpr' es else @Var _ y _
238
  | Rec f y e =>
239
240
241
242
243
     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)
244
  | Lit l => Lit l
245
246
247
248
249
250
251
252
  | 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)
253
  | Case e0 e1 e2 =>
254
255
256
257
258
     Case (wsubst x es H e0) (wsubst x es H e1) (wsubst x es H e2)
  | Fork e => Fork (wsubst x es H e)
  | 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)
259
  | CAS e0 e1 e2 => CAS (wsubst x es H e0) (wsubst x es H e1) (wsubst x es H e2)
260
  end.
261
262
263
264
265
266
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.
267

268
(** The stepping relation *)
269
270
Definition un_op_eval (op : un_op) (l : base_lit) : option base_lit :=
  match op, l with
271
  | NegOp, LitBool b => Some (LitBool (negb b))
272
  | MinusUnOp, LitInt n => Some (LitInt (- n))
273
274
275
276
277
  | _, _ => None
  end.

Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
  match op, l1, l2 with
278
279
280
281
282
  | 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)
283
284
285
  | _, _, _ => None
  end.

286
287
Inductive head_step : expr []  state  expr []  state  option (expr [])  Prop :=
  | BetaS f x e1 e2 v2 e' σ :
288
     to_val e2 = Some v2 
289
290
     e' = subst' x (of_val v2) (subst' f (Rec f x e1) e1) 
     head_step (App (Rec f x e1) e2) σ e' σ None
291
  | UnOpS op l l' σ :
292
293
     un_op_eval op l = Some l'  
     head_step (UnOp op (Lit l)) σ (Lit l') σ None
294
  | BinOpS op l1 l2 l' σ :
295
296
297
     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
298
     head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ None
299
  | IfFalseS e1 e2 σ :
Ralf Jung's avatar
Ralf Jung committed
300
     head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ None
301
302
303
304
305
306
  | 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
307
  | CaseLS e0 v0 e1 e2 σ :
308
     to_val e0 = Some v0 
309
310
     head_step (Case (InjL e0) e1 e2) σ (App e1 e0) σ None
  | CaseRS e0 v0 e1 e2 σ :
311
     to_val e0 = Some v0 
312
     head_step (Case (InjR e0) e1 e2) σ (App e2 e0) σ None
313
  | ForkS e σ:
314
     head_step (Fork e) σ (Lit LitUnit) σ (Some e)
315
316
  | AllocS e v σ l :
     to_val e = Some v  σ !! l = None 
317
     head_step (Alloc e) σ (Lit $ LitLoc l) (<[l:=v]>σ) None
318
319
  | LoadS l v σ :
     σ !! l = Some v 
320
     head_step (Load (Lit $ LitLoc l)) σ (of_val v) σ None
321
322
  | StoreS l e v σ :
     to_val e = Some v  is_Some (σ !! l) 
323
     head_step (Store (Lit $ LitLoc l) e) σ (Lit LitUnit) (<[l:=v]>σ) None
324
325
326
  | CasFailS l e1 v1 e2 v2 vl σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some vl  vl  v1 
327
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool false) σ None
328
329
330
  | CasSucS l e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some v1 
331
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None.
Ralf Jung's avatar
Ralf Jung committed
332

333
(** Atomic expressions *)
334
Definition atomic (e: expr []) : bool :=
335
  match e with
336
337
338
339
340
  | Alloc e => bool_decide (is_Some (to_val e))
  | Load e => bool_decide (is_Some (to_val e))
  | Store e1 e2 => bool_decide (is_Some (to_val e1)  is_Some (to_val e2))
  | CAS e0 e1 e2 =>
    bool_decide (is_Some (to_val e0)  is_Some (to_val e1)  is_Some (to_val e2))
Ralf Jung's avatar
Ralf Jung committed
341
  (* Make "skip" atomic *)
342
343
  | App (Rec _ _ (Lit _)) (Lit _) => true
  | _ => false
344
  end.
345

346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
(** 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/=);
377
    unfold wexpr'; auto using var_proof_irrel, wexpr_wexpr with f_equal.
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
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.

404
405
(** Basic properties about the language *)
Lemma to_of_val v : to_val (of_val v) = Some v.
406
Proof. by induction v; simplify_option_eq. Qed.
407

408
Lemma of_to_val e v : to_val e = Some v  of_val v = e.
409
Proof.
410
411
412
413
414
415
416
  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.
417
Qed.
418

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

422
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
423
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
424

425
426
427
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.
428

429
Lemma val_stuck e1 σ1 e2 σ2 ef :
430
431
  head_step e1 σ1 e2 σ2 ef  to_val e1 = None.
Proof. destruct 1; naive_solver. Qed.
432

433
Lemma atomic_not_val e : atomic e  to_val e = None.
434
Proof. by destruct e. Qed.
435

436
437
Lemma atomic_fill_item Ki e : atomic (fill_item Ki e)  is_Some (to_val e).
Proof.
438
  intros. destruct Ki; simplify_eq/=; destruct_and?;
439
440
441
    repeat (case_match || contradiction); eauto.
Qed.

442
Lemma atomic_step e1 σ1 e2 σ2 ef :
443
  atomic e1  head_step e1 σ1 e2 σ2 ef  is_Some (to_val e2).
Ralf Jung's avatar
Ralf Jung committed
444
Proof.
445
  destruct 2; simpl; rewrite ?to_of_val; try by eauto. subst.
446
  unfold subst'; repeat (case_match || contradiction || simplify_eq/=); eauto.
Ralf Jung's avatar
Ralf Jung committed
447
Qed.
448

449
Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef :
450
  head_step (fill_item Ki e) σ1 e2 σ2 ef  is_Some (to_val e).
451
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; eauto. Qed.
452

453
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
454
  to_val e1 = None  to_val e2 = None 
455
  fill_item Ki1 e1 = fill_item Ki2 e2  Ki1 = Ki2.
456
Proof.
457
  destruct Ki1, Ki2; intros; try discriminate; simplify_eq/=;
458
    repeat match goal with
459
460
    | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
    end; auto.
Ralf Jung's avatar
Ralf Jung committed
461
Qed.
462

463
464
Lemma alloc_fresh e v σ :
  let l := fresh (dom _ σ) in
465
  to_val e = Some v  head_step (Alloc e) σ (Lit (LitLoc l)) (<[l:=v]>σ) None.
466
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
467

Ralf Jung's avatar
Ralf Jung committed
468
(** Equality and other typeclass stuff *)
469
470
471
472
473
474
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.
475

476
477
478
479
480
481
482
483
484
485
486
487
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' |
488
    CAS e0 e1 e2, CAS e0' e1' e2' =>
489
490
491
492
     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'
  | _, _ => false
493
  end.
494
Lemma expr_beq_correct {X} (e1 e2 : expr X) : expr_beq e1 e2  e1 = e2.
495
Proof.
496
497
498
499
  split.
  * revert e2; induction e1; intros [] * ?; simpl in *;
      destruct_and?; subst; repeat f_equal/=; auto; try apply proof_irrel.
  * intros ->. induction e2; naive_solver.
500
Qed.
501
Instance expr_dec_eq {X} (e1 e2 : expr X) : Decision (e1 = e2).
502
Proof.
503
504
505
 refine (cast_if (decide (expr_beq e1 e2))); by rewrite -expr_beq_correct.
Defined.
Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2).
506
Proof.
507
508
 refine (cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
Defined.
Ralf Jung's avatar
Ralf Jung committed
509
510
511

Instance expr_inhabited X : Inhabited (expr X) := populate (Lit LitUnit).
Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
512
513
514
515

Canonical Structure stateC := leibnizC state.
Canonical Structure valC := leibnizC val.
Canonical Structure exprC X := leibnizC (expr X).
516
517
518
End heap_lang.

(** Language *)
519
520
521
Program Instance heap_ectxi_lang :
  EctxiLanguage
    (heap_lang.expr []) heap_lang.val heap_lang.ectx_item heap_lang.state := {|
Robbert Krebbers's avatar
Robbert Krebbers committed
522
  of_val := heap_lang.of_val; to_val := heap_lang.to_val;
523
  fill_item := heap_lang.fill_item;
Robbert Krebbers's avatar
Robbert Krebbers committed
524
525
  atomic := heap_lang.atomic; head_step := heap_lang.head_step;
|}.
526
Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
527
  heap_lang.val_stuck, heap_lang.atomic_not_val, heap_lang.atomic_step,
528
529
  heap_lang.fill_item_val, heap_lang.atomic_fill_item,
  heap_lang.fill_item_no_val_inj, heap_lang.head_ctx_step_val.
530

531
Canonical Structure heap_lang := ectx_lang (heap_lang.expr []).
532

533
(* Prefer heap_lang names over ectx_language names. *)
534
Export heap_lang.