lang.v 22.7 KB
Newer Older
1
From program_logic Require Export language.
2
From prelude Require Export strings.
3
From 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 19
Inductive binder := BAnon | BNamed : string  binder.

20 21 22
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).
23
Delimit Scope binder_scope with bind.
24
Bind Scope binder_scope with binder.
25 26 27 28 29 30 31 32 33 34
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 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245
  end.
Solve Obligations with set_solver.

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}
    (Hfy :BNamed x  f  BNamed x  y) :
  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
  | Var y _ => if decide (x = y) then wexpr _ es else @Var _ y _
246
  | Rec f y e =>
247 248 249 250 251
     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)
252
  | Lit l => Lit l
253 254 255 256 257 258 259 260
  | 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)
261
  | Case e0 e1 e2 =>
262 263
     Case (wsubst x es H e0) (wsubst x es H e1) (wsubst x es H e2)
  | Fork e => Fork (wsubst x es H e)
264
  | Loc l => Loc l
265 266 267
  | 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)
268
  | CAS e0 e1 e2 => CAS (wsubst x es H e0) (wsubst x es H e1) (wsubst x es H e2)
269
  end.
270 271 272 273 274 275
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.
276

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

Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
  match op, l1, l2 with
287 288 289 290 291
  | 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)
292 293 294
  | _, _, _ => None
  end.

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

342
(** Atomic expressions *)
343
Definition atomic (e: expr []) : Prop :=
344 345 346 347
  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)
348
  | 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
349 350
  (* Make "skip" atomic *)
  | App (Rec _ _ (Lit _)) (Lit _) => True
351 352
  | _ => False
  end.
353

354 355
(** Close reduction under evaluation contexts.
We could potentially make this a generic construction. *)
356 357
Inductive prim_step (e1 : expr []) (σ1 : state)
    (e2 : expr []) (σ2: state) (ef: option (expr [])) : Prop :=
358
  Ectx_step K e1' e2' :
359 360 361
    e1 = fill K e1'  e2 = fill K e2' 
    head_step e1' σ1 e2' σ2 ef  prim_step e1 σ1 e2 σ2 ef.

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 387 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 414 415 416 417 418 419
(** 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/=);
    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) 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.

Ralf Jung's avatar
Ralf Jung committed
420 421 422 423
Lemma of_val'_closed (v : val) :
  of_val' v = of_val v.
Proof. by rewrite /of_val' wexpr_id. Qed.

Ralf Jung's avatar
Ralf Jung committed
424 425 426 427 428 429 430 431 432 433 434
(** to_val propagation.
    TODO: automatically appliy in wp_tactics? *)
Lemma to_val_InjL e v : to_val e = Some v  to_val (InjL e) = Some (InjLV v).
Proof. move=>H. simpl. by rewrite H. Qed.
Lemma to_val_InjR e v : to_val e = Some v  to_val (InjR e) = Some (InjRV v).
Proof. move=>H. simpl. by rewrite H. Qed.
Lemma to_val_Pair e1 e2 v1 v2 :
  to_val e1 = Some v1  to_val e2 = Some v2 
  to_val (Pair e1 e2) = Some (PairV v1 v2).
Proof. move=>H1 H2. simpl. by rewrite H1 H2. Qed.

435 436
(** Basic properties about the language *)
Lemma to_of_val v : to_val (of_val v) = Some v.
437
Proof. by induction v; simplify_option_eq. Qed.
438

439
Lemma of_to_val e v : to_val e = Some v  of_val v = e.
440
Proof.
441 442 443 444 445 446 447
  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.
448
Qed.
449

450 451
Instance: Inj (=) (=) of_val.
Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
452

453
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
454
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
455

456
Instance ectx_fill_inj K : Inj (=) (=) (fill K).
457
Proof. red; induction K as [|Ki K IH]; naive_solver. Qed.
458

459 460
Lemma fill_app K1 K2 e : fill (K1 ++ K2) e = fill K1 (fill K2 e).
Proof. revert e; induction K1; simpl; auto with f_equal. Qed.
461

462
Lemma fill_val K e : is_Some (to_val (fill K e))  is_Some (to_val e).
463
Proof.
464
  intros [v' Hv']; revert v' Hv'.
465
  induction K as [|[]]; intros; simplify_option_eq; eauto.
466
Qed.
467

468 469
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.
470

471
Lemma val_head_stuck e1 σ1 e2 σ2 ef :
472 473
  head_step e1 σ1 e2 σ2 ef  to_val e1 = None.
Proof. destruct 1; naive_solver. Qed.
474

475 476
Lemma val_stuck e1 σ1 e2 σ2 ef : prim_step e1 σ1 e2 σ2 ef  to_val e1 = None.
Proof. intros [??? -> -> ?]; eauto using fill_not_val, val_head_stuck. Qed.
477

478 479
Lemma atomic_not_val e : atomic e  to_val e = None.
Proof. destruct e; naive_solver. Qed.
480

481 482
Lemma atomic_fill_item Ki e : atomic (fill_item Ki e)  is_Some (to_val e).
Proof.
483
  intros. destruct Ki; simplify_eq/=; destruct_and?;
484 485 486
    repeat (case_match || contradiction); eauto.
Qed.

487
Lemma atomic_fill K e : atomic (fill K e)  to_val e = None  K = [].
488
Proof.
489 490
  destruct K as [|Ki K]; [done|].
  rewrite eq_None_not_Some=> /= ? []; eauto using atomic_fill_item, fill_val.
491
Qed.
492

493 494
Lemma atomic_head_step e1 σ1 e2 σ2 ef :
  atomic e1  head_step e1 σ1 e2 σ2 ef  is_Some (to_val e2).
Ralf Jung's avatar
Ralf Jung committed
495
Proof.
496
  destruct 2; simpl; rewrite ?to_of_val; try by eauto. subst.
497
  unfold subst'; repeat (case_match || contradiction || simplify_eq/=); eauto.
Ralf Jung's avatar
Ralf Jung committed
498
Qed.
499

500 501
Lemma atomic_step e1 σ1 e2 σ2 ef :
  atomic e1  prim_step e1 σ1 e2 σ2 ef  is_Some (to_val e2).
502
Proof.
503
  intros Hatomic [K e1' e2' -> -> Hstep].
504
  assert (K = []) as -> by eauto 10 using atomic_fill, val_head_stuck.
505
  naive_solver eauto using atomic_head_step.
Ralf Jung's avatar
Ralf Jung committed
506
Qed.
507

508
Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef :
509
  head_step (fill_item Ki e) σ1 e2 σ2 ef  is_Some (to_val e).
510
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; eauto. Qed.
511

512
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
513
  to_val e1 = None  to_val e2 = None 
514
  fill_item Ki1 e1 = fill_item Ki2 e2  Ki1 = Ki2.
515
Proof.
516
  destruct Ki1, Ki2; intros; try discriminate; simplify_eq/=;
517
    repeat match goal with
518 519
    | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
    end; auto.
Ralf Jung's avatar
Ralf Jung committed
520
Qed.
521

522 523 524 525 526 527
(* 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 
  K `prefix_of` K'.
528
Proof.
529 530
  intros Hfill Hred Hnval; revert K' Hfill.
  induction K as [|Ki K IH]; simpl; intros K' Hfill; auto using prefix_of_nil.
531
  destruct K' as [|Ki' K']; simplify_eq/=.
Ralf Jung's avatar
Ralf Jung committed
532
  { exfalso; apply (eq_None_not_Some (to_val (fill K e1)));
533 534
      eauto using fill_not_val, head_ctx_step_val. }
  cut (Ki = Ki'); [naive_solver eauto using prefix_of_cons|].
535
  eauto using fill_item_no_val_inj, val_head_stuck, fill_not_val.
536
Qed.
537

538 539 540
Lemma alloc_fresh e v σ :
  let l := fresh (dom _ σ) in
  to_val e = Some v  head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None.
541
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
542

Ralf Jung's avatar
Ralf Jung committed
543
(** Equality and other typeclass stuff *)
544 545 546 547 548 549
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.
550

551 552 553 554 555 556 557 558 559 560 561 562
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' |
563
    CAS e0 e1 e2, CAS e0' e1' e2' =>
564 565 566 567 568
     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
569
  end.
570
Lemma expr_beq_correct {X} (e1 e2 : expr X) : expr_beq e1 e2  e1 = e2.
571
Proof.
572 573 574 575
  split.
  * revert e2; induction e1; intros [] * ?; simpl in *;
      destruct_and?; subst; repeat f_equal/=; auto; try apply proof_irrel.
  * intros ->. induction e2; naive_solver.
576
Qed.
577
Instance expr_dec_eq {X} (e1 e2 : expr X) : Decision (e1 = e2).
578
Proof.
579 580 581
 refine (cast_if (decide (expr_beq e1 e2))); by rewrite -expr_beq_correct.
Defined.
Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2).
582
Proof.
583 584
 refine (cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
Defined.
Ralf Jung's avatar
Ralf Jung committed
585 586 587

Instance expr_inhabited X : Inhabited (expr X) := populate (Lit LitUnit).
Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
588 589 590 591
End heap_lang.

(** Language *)
Program Canonical Structure heap_lang : language := {|
592
  expr := heap_lang.expr []; val := heap_lang.val; state := heap_lang.state;
593 594 595 596
  of_val := heap_lang.of_val; to_val := heap_lang.to_val;
  atomic := heap_lang.atomic; prim_step := heap_lang.prim_step;
|}.
Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
597
  heap_lang.val_stuck, heap_lang.atomic_not_val, heap_lang.atomic_step.
598

599
Global Instance heap_lang_ctx K : LanguageCtx heap_lang (heap_lang.fill K).
600
Proof.
601
  split.
602 603
  - eauto using heap_lang.fill_not_val.
  - intros ????? [K' e1' e2' Heq1 Heq2 Hstep].
604
    by exists (K ++ K') e1' e2'; rewrite ?heap_lang.fill_app ?Heq1 ?Heq2.
605
  - intros e1 σ1 e2 σ2 ? Hnval [K'' e1'' e2'' Heq1 -> Hstep].
606 607
    destruct (heap_lang.step_by_val
      K K'' e1 e1'' σ1 e2'' σ2 ef) as [K' ->]; eauto.
608
    rewrite heap_lang.fill_app in Heq1; apply (inj _) in Heq1.
Ralf Jung's avatar
Ralf Jung committed
609
    exists (heap_lang.fill K' e2''); rewrite heap_lang.fill_app; split; auto.
610
    econstructor; eauto.
611
Qed.
612 613 614

Global Instance heap_lang_ctx_item Ki :
  LanguageCtx heap_lang (heap_lang.fill_item Ki).
615
Proof. change (LanguageCtx heap_lang (heap_lang.fill [Ki])). apply _. Qed.
616 617 618

(* Prefer heap_lang names over language names. *)
Export heap_lang.