lang.v 13.7 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
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.

35
Inductive expr :=
36
  (* Base lambda calculus *)
37 38 39
  | Var (x : string)
  | Rec (f x : binder) (e : expr)
  | App (e1 e2 : expr)
40 41
  (* Base types and their operations *)
  | Lit (l : base_lit)
42 43 44
  | UnOp (op : un_op) (e : expr)
  | BinOp (op : bin_op) (e1 e2 : expr)
  | If (e0 e1 e2 : expr)
45
  (* Products *)
46 47 48
  | Pair (e1 e2 : expr)
  | Fst (e : expr)
  | Snd (e : expr)
49
  (* Sums *)
50 51 52
  | InjL (e : expr)
  | InjR (e : expr)
  | Case (e0 : expr) (e1 : expr) (e2 : expr)
53
  (* Concurrency *)
54
  | Fork (e : expr)
55
  (* Heap *)
56 57 58 59
  | Alloc (e : expr)
  | Load (e : expr)
  | Store (e1 : expr) (e2 : expr)
  | CAS (e0 : expr) (e1 : expr) (e2 : expr).
Ralf Jung's avatar
Ralf Jung committed
60

61 62
Bind Scope expr_scope with expr.
Delimit Scope expr_scope with E.
63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93
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.
Arguments CAS _%E _%E _%E.

Fixpoint is_closed (X : list string) (e : expr) : bool :=
  match e with
  | Var x => bool_decide (x  X)
  | Rec f x e => is_closed (f :b: x :b: X) e
  | Lit _ => true
  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e =>
     is_closed X e
  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 =>
     is_closed X e1 && is_closed X e2
  | If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
     is_closed X e0 && is_closed X e1 && is_closed X e2
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
94
Class Closed (X : list string) (e : expr) := closed : is_closed X e.
95 96 97 98
Instance closed_proof_irrel env e : ProofIrrel (Closed env e).
Proof. rewrite /Closed. apply _. Qed.
Instance closed_decision env e : Decision (Closed env e).
Proof. rewrite /Closed. apply _. Qed.
99

100
Inductive val :=
101
  | RecV (f x : binder) (e : expr) `{!Closed (f :b: x :b: []) e}
102
  | LitV (l : base_lit)
103 104
  | PairV (v1 v2 : val)
  | InjLV (v : val)
105
  | InjRV (v : val).
Ralf Jung's avatar
Ralf Jung committed
106

107 108
Bind Scope val_scope with val.
Delimit Scope val_scope with V.
109 110 111
Arguments PairV _%V _%V.
Arguments InjLV _%V.
Arguments InjRV _%V.
112

113
Fixpoint of_val (v : val) : expr :=
Ralf Jung's avatar
Ralf Jung committed
114
  match v with
115
  | RecV f x e _ => Rec f x e
116
  | LitV l => Lit l
117 118 119
  | 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
120
  end.
121

122
Fixpoint to_val (e : expr) : option val :=
123
  match e with
124 125
  | Rec f x e =>
     if decide (Closed (f :b: x :b: []) e) then Some (RecV f x e) else None
126
  | Lit l => Some (LitV l)
127 128 129
  | 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
130
  | _ => None
131 132
  end.

133 134
(** The state: heaps of vals. *)
Definition state := gmap loc val.
Ralf Jung's avatar
Ralf Jung committed
135

136
(** Evaluation contexts *)
137
Inductive ectx_item :=
138
  | AppLCtx (e2 : expr)
139
  | AppRCtx (v1 : val)
140
  | UnOpCtx (op : un_op)
141
  | BinOpLCtx (op : bin_op) (e2 : expr)
142
  | BinOpRCtx (op : bin_op) (v1 : val)
143 144
  | IfCtx (e1 e2 : expr)
  | PairLCtx (e2 : expr)
145 146 147 148 149
  | PairRCtx (v1 : val)
  | FstCtx
  | SndCtx
  | InjLCtx
  | InjRCtx
150
  | CaseCtx (e1 : expr) (e2 : expr)
151 152
  | AllocCtx
  | LoadCtx
153
  | StoreLCtx (e2 : expr)
154
  | StoreRCtx (v1 : val)
155 156
  | CasLCtx (e1 : expr)  (e2 : expr)
  | CasMCtx (v0 : val) (e2 : expr)
157
  | CasRCtx (v0 : val) (v1 : val).
158

159
Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
160 161 162
  match Ki with
  | AppLCtx e2 => App e e2
  | AppRCtx v1 => App (of_val v1) e
163 164 165 166
  | 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
167 168 169 170 171 172
  | PairLCtx e2 => Pair e e2
  | PairRCtx v1 => Pair (of_val v1) e
  | FstCtx => Fst e
  | SndCtx => Snd e
  | InjLCtx => InjL e
  | InjRCtx => InjR e
173
  | CaseCtx e1 e2 => Case e e1 e2
174 175
  | AllocCtx => Alloc e
  | LoadCtx => Load e
176
  | StoreLCtx e2 => Store e e2 
177
  | StoreRCtx v1 => Store (of_val v1) e
178 179 180
  | 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
181 182
  end.

183
(** Substitution *)
184 185 186
Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
  match e with
  | Var y => if decide (x = y) then es else Var y
187
  | Rec f y e =>
188 189
     Rec f y $ if decide (BNamed x  f  BNamed x  y) then subst x es e else e
  | App e1 e2 => App (subst x es e1) (subst x es e2)
190
  | Lit l => Lit l
191 192 193 194 195 196 197 198 199 200 201 202 203 204
  | UnOp op e => UnOp op (subst x es e)
  | BinOp op e1 e2 => BinOp op (subst x es e1) (subst x es e2)
  | If e0 e1 e2 => If (subst x es e0) (subst x es e1) (subst x es e2)
  | Pair e1 e2 => Pair (subst x es e1) (subst x es e2)
  | Fst e => Fst (subst x es e)
  | Snd e => Snd (subst x es e)
  | InjL e => InjL (subst x es e)
  | InjR e => InjR (subst x es e)
  | Case e0 e1 e2 => Case (subst x es e0) (subst x es e1) (subst x es e2)
  | Fork e => Fork (subst x es e)
  | Alloc e => Alloc (subst x es e)
  | Load e => Load (subst x es e)
  | Store e1 e2 => Store (subst x es e1) (subst x es e2)
  | CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
205
  end.
206

207
Definition subst' (mx : binder) (es : expr) : expr  expr :=
208
  match mx with BNamed x => subst x es | BAnon => id end.
209

210
(** The stepping relation *)
211 212
Definition un_op_eval (op : un_op) (l : base_lit) : option base_lit :=
  match op, l with
213
  | NegOp, LitBool b => Some (LitBool (negb b))
214
  | MinusUnOp, LitInt n => Some (LitInt (- n))
215 216 217 218 219
  | _, _ => None
  end.

Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
  match op, l1, l2 with
220 221 222 223 224
  | 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)
225 226 227
  | _, _, _ => None
  end.

228
Inductive head_step : expr  state  expr  state  option (expr)  Prop :=
229
  | BetaS f x e1 e2 v2 e' σ :
230
     to_val e2 = Some v2 
231
     Closed (f :b: x :b: []) e1 
232 233
     e' = subst' x (of_val v2) (subst' f (Rec f x e1) e1) 
     head_step (App (Rec f x e1) e2) σ e' σ None
234
  | UnOpS op l l' σ :
235 236
     un_op_eval op l = Some l'  
     head_step (UnOp op (Lit l)) σ (Lit l') σ None
237
  | BinOpS op l1 l2 l' σ :
238 239 240
     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
241
     head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ None
242
  | IfFalseS e1 e2 σ :
Ralf Jung's avatar
Ralf Jung committed
243
     head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ None
244 245 246 247 248 249
  | 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
250
  | CaseLS e0 v0 e1 e2 σ :
251
     to_val e0 = Some v0 
252 253
     head_step (Case (InjL e0) e1 e2) σ (App e1 e0) σ None
  | CaseRS e0 v0 e1 e2 σ :
254
     to_val e0 = Some v0 
255
     head_step (Case (InjR e0) e1 e2) σ (App e2 e0) σ None
256
  | ForkS e σ:
257
     head_step (Fork e) σ (Lit LitUnit) σ (Some e)
258 259
  | AllocS e v σ l :
     to_val e = Some v  σ !! l = None 
260
     head_step (Alloc e) σ (Lit $ LitLoc l) (<[l:=v]>σ) None
261 262
  | LoadS l v σ :
     σ !! l = Some v 
263
     head_step (Load (Lit $ LitLoc l)) σ (of_val v) σ None
264 265
  | StoreS l e v σ :
     to_val e = Some v  is_Some (σ !! l) 
266
     head_step (Store (Lit $ LitLoc l) e) σ (Lit LitUnit) (<[l:=v]>σ) None
267 268 269
  | CasFailS l e1 v1 e2 v2 vl σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some vl  vl  v1 
270
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool false) σ None
271 272 273
  | CasSucS l e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some v1 
274
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None.
Ralf Jung's avatar
Ralf Jung committed
275

276
(** Atomic expressions *)
277
Definition atomic (e: expr) :=
278
  match e with
279 280 281
  | 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)
282
  | CAS e0 e1 e2 =>
283
     is_Some (to_val e0)  is_Some (to_val e1)  is_Some (to_val e2)
Ralf Jung's avatar
Ralf Jung committed
284
  (* Make "skip" atomic *)
285 286
  | App (Rec _ _ (Lit _)) (Lit _) => True
  | _ => False
287
  end.
288

289 290
(** Basic properties about the language *)
Lemma to_of_val v : to_val (of_val v) = Some v.
291 292 293
Proof.
  by induction v; simplify_option_eq; repeat f_equal; try apply (proof_irrel _).
Qed.
294

295
Lemma of_to_val e v : to_val e = Some v  of_val v = e.
296
Proof.
297
  revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
298
Qed.
299

300
Instance of_val_inj : Inj (=) (=) of_val.
301
Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
302

303
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
304
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
305

306 307 308
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.
309

310
Lemma val_stuck e1 σ1 e2 σ2 ef : head_step e1 σ1 e2 σ2 ef  to_val e1 = None.
311
Proof. destruct 1; naive_solver. Qed.
312

313
Lemma atomic_not_val e : atomic e  to_val e = None.
314
Proof. by destruct e. Qed.
315

316 317
Lemma atomic_fill_item Ki e : atomic (fill_item Ki e)  is_Some (to_val e).
Proof.
318
  intros. destruct Ki; simplify_eq/=; destruct_and?;
319
    repeat (simpl || case_match || contradiction); eauto.
320 321
Qed.

322
Lemma atomic_step e1 σ1 e2 σ2 ef :
323
  atomic e1  head_step e1 σ1 e2 σ2 ef  is_Some (to_val e2).
Ralf Jung's avatar
Ralf Jung committed
324
Proof.
325
  destruct 2; simpl; rewrite ?to_of_val; try by eauto. subst.
326
  unfold subst'; repeat (case_match || contradiction || simplify_eq/=); eauto.
Ralf Jung's avatar
Ralf Jung committed
327
Qed.
328

329
Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef :
330
  head_step (fill_item Ki e) σ1 e2 σ2 ef  is_Some (to_val e).
331
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
332

333
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
334
  to_val e1 = None  to_val e2 = None 
335
  fill_item Ki1 e1 = fill_item Ki2 e2  Ki1 = Ki2.
336
Proof.
337
  destruct Ki1, Ki2; intros; try discriminate; simplify_eq/=;
338
    repeat match goal with
339 340
    | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
    end; auto.
Ralf Jung's avatar
Ralf Jung committed
341
Qed.
342

343 344
Lemma alloc_fresh e v σ :
  let l := fresh (dom _ σ) in
345
  to_val e = Some v  head_step (Alloc e) σ (Lit (LitLoc l)) (<[l:=v]>σ) None.
346
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
347

Robbert Krebbers's avatar
Robbert Krebbers committed
348 349 350 351
(** Closed expressions *)
Lemma is_closed_weaken X Y e : is_closed X e  X `included` Y  is_closed Y e.
Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.

352 353 354 355
Lemma is_closed_weaken_nil X e : is_closed [] e  is_closed X e.
Proof. intros. by apply is_closed_weaken with [], included_nil. Qed.

Lemma is_closed_subst X e x es : is_closed X e  x  X  subst x es e = e.
Robbert Krebbers's avatar
Robbert Krebbers committed
356
Proof.
357
  revert X. induction e=> X /=; rewrite ?bool_decide_spec ?andb_True=> ??;
Robbert Krebbers's avatar
Robbert Krebbers committed
358 359
    repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver.
Qed.
360

361 362
Lemma is_closed_nil_subst e x es : is_closed [] e  subst x es e = e.
Proof. intros. apply is_closed_subst with []; set_solver. Qed.
363

364 365
Lemma is_closed_of_val X v : is_closed X (of_val v).
Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.
366

Ralf Jung's avatar
Ralf Jung committed
367
(** Equality and other typeclass stuff *)
368 369 370 371 372 373
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.
374 375
Instance expr_dec_eq (e1 e2 : expr) : Decision (e1 = e2).
Proof. solve_decision. Defined.
376
Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2).
377
Proof.
378 379
 refine (cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
Defined.
Ralf Jung's avatar
Ralf Jung committed
380

381
Instance expr_inhabited : Inhabited (expr) := populate (Lit LitUnit).
Ralf Jung's avatar
Ralf Jung committed
382
Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
383 384 385

Canonical Structure stateC := leibnizC state.
Canonical Structure valC := leibnizC val.
386
Canonical Structure exprC := leibnizC expr.
387 388 389
End heap_lang.

(** Language *)
390 391
Program Instance heap_ectxi_lang :
  EctxiLanguage
392
    (heap_lang.expr) heap_lang.val heap_lang.ectx_item heap_lang.state := {|
Robbert Krebbers's avatar
Robbert Krebbers committed
393
  of_val := heap_lang.of_val; to_val := heap_lang.to_val;
394
  fill_item := heap_lang.fill_item;
Robbert Krebbers's avatar
Robbert Krebbers committed
395 396
  atomic := heap_lang.atomic; head_step := heap_lang.head_step;
|}.
397
Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
398
  heap_lang.val_stuck, heap_lang.atomic_not_val, heap_lang.atomic_step,
399 400
  heap_lang.fill_item_val, heap_lang.atomic_fill_item,
  heap_lang.fill_item_no_val_inj, heap_lang.head_ctx_step_val.
401

402
Canonical Structure heap_lang := ectx_lang (heap_lang.expr).
403

404
(* Prefer heap_lang names over ectx_language names. *)
405
Export heap_lang.