lang.v 14.6 KB
Newer Older
1
From iris.program_logic Require Export ectx_language ectxi_language.
2
From iris.algebra Require Export ofe.
Ralf Jung's avatar
Ralf Jung committed
3 4
From stdpp Require Export strings.
From stdpp Require Import gmap.
5
Set Default Proof Using "Type".
6

7
Module heap_lang.
8 9
Open Scope Z_scope.

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

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

20
Inductive binder := BAnon | BNamed : string  binder.
Ralf Jung's avatar
Ralf Jung committed
21 22
Delimit Scope binder_scope with bind.
Bind Scope binder_scope with binder.
23 24 25
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).
26
Instance binder_eq_dec_eq : EqDecision binder.
27 28 29 30 31 32 33 34 35
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.

36
Inductive expr :=
37
  (* Base lambda calculus *)
38 39 40
  | Var (x : string)
  | Rec (f x : binder) (e : expr)
  | App (e1 e2 : expr)
41 42
  (* Base types and their operations *)
  | Lit (l : base_lit)
43 44 45
  | UnOp (op : un_op) (e : expr)
  | BinOp (op : bin_op) (e1 e2 : expr)
  | If (e0 e1 e2 : expr)
46
  (* Products *)
47 48 49
  | Pair (e1 e2 : expr)
  | Fst (e : expr)
  | Snd (e : expr)
50
  (* Sums *)
51 52 53
  | InjL (e : expr)
  | InjR (e : expr)
  | Case (e0 : expr) (e1 : expr) (e2 : expr)
54
  (* Concurrency *)
55
  | Fork (e : expr)
56
  (* Heap *)
57 58 59 60
  | 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
61

62
Bind Scope expr_scope with expr.
63 64 65 66 67 68 69 70 71 72 73 74 75 76

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
77
Class Closed (X : list string) (e : expr) := closed : is_closed X e.
78 79 80 81
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.
82

83
Inductive val :=
84
  | RecV (f x : binder) (e : expr) `{!Closed (f :b: x :b: []) e}
85
  | LitV (l : base_lit)
86 87
  | PairV (v1 v2 : val)
  | InjLV (v : val)
88
  | InjRV (v : val).
Ralf Jung's avatar
Ralf Jung committed
89

90
Bind Scope val_scope with val.
91

92
Fixpoint of_val (v : val) : expr :=
Ralf Jung's avatar
Ralf Jung committed
93
  match v with
94
  | RecV f x e _ => Rec f x e
95
  | LitV l => Lit l
96 97 98
  | 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
99
  end.
100

101
Fixpoint to_val (e : expr) : option val :=
102
  match e with
103 104
  | Rec f x e =>
     if decide (Closed (f :b: x :b: []) e) then Some (RecV f x e) else None
105
  | Lit l => Some (LitV l)
106 107 108
  | 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
109
  | _ => None
110 111
  end.

112 113
(** The state: heaps of vals. *)
Definition state := gmap loc val.
Ralf Jung's avatar
Ralf Jung committed
114

115 116 117 118 119 120 121 122 123 124 125 126 127 128
(** Equality and other typeclass stuff *)
Lemma to_of_val v : to_val (of_val v) = Some v.
Proof.
  by induction v; simplify_option_eq; repeat f_equal; try apply (proof_irrel _).
Qed.

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

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

129
Instance base_lit_eq_dec : EqDecision base_lit.
130
Proof. solve_decision. Defined.
131
Instance un_op_eq_dec : EqDecision un_op.
132
Proof. solve_decision. Defined.
133
Instance bin_op_eq_dec : EqDecision bin_op.
134
Proof. solve_decision. Defined.
135
Instance expr_eq_dec : EqDecision expr.
136
Proof. solve_decision. Defined.
137
Instance val_eq_dec : EqDecision val.
138
Proof.
139
 refine (λ v v', cast_if (decide (of_val v = of_val v'))); abstract naive_solver.
140 141 142 143 144 145 146 147 148
Defined.

Instance expr_inhabited : Inhabited expr := populate (Lit LitUnit).
Instance val_inhabited : Inhabited val := populate (LitV LitUnit).

Canonical Structure stateC := leibnizC state.
Canonical Structure valC := leibnizC val.
Canonical Structure exprC := leibnizC expr.

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

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

196
(** Substitution *)
197 198 199
Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
  match e with
  | Var y => if decide (x = y) then es else Var y
200
  | Rec f y e =>
201 202
     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)
203
  | Lit l => Lit l
204 205 206 207 208 209 210 211 212 213 214 215 216 217
  | 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)
218
  end.
219

220
Definition subst' (mx : binder) (es : expr) : expr  expr :=
221
  match mx with BNamed x => subst x es | BAnon => id end.
222

223
(** The stepping relation *)
224 225 226 227
Definition un_op_eval (op : un_op) (v : val) : option val :=
  match op, v with
  | NegOp, LitV (LitBool b) => Some $ LitV $ LitBool (negb b)
  | MinusUnOp, LitV (LitInt n) => Some $ LitV $ LitInt (- n)
228 229 230
  | _, _ => None
  end.

231 232 233 234 235 236 237
Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
  match op, v1, v2 with
  | PlusOp, LitV (LitInt n1), LitV (LitInt n2) => Some $ LitV $ LitInt (n1 + n2)
  | MinusOp, LitV (LitInt n1), LitV (LitInt n2) => Some $ LitV $ LitInt (n1 - n2)
  | LeOp, LitV (LitInt n1), LitV (LitInt n2) => Some $ LitV $ LitBool $ bool_decide (n1  n2)
  | LtOp, LitV (LitInt n1), LitV (LitInt n2) => Some $ LitV $ LitBool $ bool_decide (n1 < n2)
  | EqOp, v1, v2 => Some $ LitV $ LitBool $ bool_decide (v1 = v2)
238 239 240
  | _, _, _ => None
  end.

241
Inductive head_step : expr  state  expr  state  list (expr)  Prop :=
242
  | BetaS f x e1 e2 v2 e' σ :
243
     to_val e2 = Some v2 
244
     Closed (f :b: x :b: []) e1 
245
     e' = subst' x (of_val v2) (subst' f (Rec f x e1) e1) 
246
     head_step (App (Rec f x e1) e2) σ e' σ []
247 248 249 250 251 252 253 254
  | UnOpS op e v v' σ :
     to_val e = Some v 
     un_op_eval op v = Some v'  
     head_step (UnOp op e) σ (of_val v') σ []
  | BinOpS op e1 e2 v1 v2 v' σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     bin_op_eval op v1 v2 = Some v'  
     head_step (BinOp op e1 e2) σ (of_val v') σ []
255
  | IfTrueS e1 e2 σ :
256
     head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ []
257
  | IfFalseS e1 e2 σ :
258
     head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ []
259 260
  | FstS e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
261
     head_step (Fst (Pair e1 e2)) σ e1 σ []
262 263
  | SndS e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
264
     head_step (Snd (Pair e1 e2)) σ e2 σ []
265
  | CaseLS e0 v0 e1 e2 σ :
266
     to_val e0 = Some v0 
267
     head_step (Case (InjL e0) e1 e2) σ (App e1 e0) σ []
268
  | CaseRS e0 v0 e1 e2 σ :
269
     to_val e0 = Some v0 
270
     head_step (Case (InjR e0) e1 e2) σ (App e2 e0) σ []
271
  | ForkS e σ:
272
     head_step (Fork e) σ (Lit LitUnit) σ [e]
273 274
  | AllocS e v σ l :
     to_val e = Some v  σ !! l = None 
275
     head_step (Alloc e) σ (Lit $ LitLoc l) (<[l:=v]>σ) []
276 277
  | LoadS l v σ :
     σ !! l = Some v 
278
     head_step (Load (Lit $ LitLoc l)) σ (of_val v) σ []
279 280
  | StoreS l e v σ :
     to_val e = Some v  is_Some (σ !! l) 
281
     head_step (Store (Lit $ LitLoc l) e) σ (Lit LitUnit) (<[l:=v]>σ) []
282 283 284
  | CasFailS l e1 v1 e2 v2 vl σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some vl  vl  v1 
285
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool false) σ []
286 287 288
  | CasSucS l e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some v1 
289
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) [].
Ralf Jung's avatar
Ralf Jung committed
290

291
(** Basic properties about the language *)
292
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
293
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
294

295 296 297
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.
298

299
Lemma val_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs  to_val e1 = None.
300
Proof. destruct 1; naive_solver. Qed.
301

302 303
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).
304
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
305

306
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
307
  to_val e1 = None  to_val e2 = None 
308
  fill_item Ki1 e1 = fill_item Ki2 e2  Ki1 = Ki2.
309
Proof.
310
  destruct Ki1, Ki2; intros; try discriminate; simplify_eq/=;
311
    repeat match goal with
312 313
    | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
    end; auto.
Ralf Jung's avatar
Ralf Jung committed
314
Qed.
315

316 317
Lemma alloc_fresh e v σ :
  let l := fresh (dom _ σ) in
318
  to_val e = Some v  head_step (Alloc e) σ (Lit (LitLoc l)) (<[l:=v]>σ) [].
319
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
320

321 322 323 324 325
(* Misc *)
Lemma to_val_rec f x e `{!Closed (f :b: x :b: []) e} :
  to_val (Rec f x e) = Some (RecV f x e).
Proof. rewrite /to_val. case_decide=> //. do 2 f_equal; apply proof_irrel. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
326
(** Closed expressions *)
327
Lemma is_closed_weaken X Y e : is_closed X e  X  Y  is_closed Y e.
Robbert Krebbers's avatar
Robbert Krebbers committed
328 329
Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.

330
Lemma is_closed_weaken_nil X e : is_closed [] e  is_closed X e.
331
Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
332

333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350
Lemma is_closed_of_val X v : is_closed X (of_val v).
Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.

Lemma is_closed_subst X e x es :
  is_closed [] es  is_closed (x :: X) e  is_closed X (subst x es e).
Proof.
  intros ?. revert X.
  induction e=> X /= ?; destruct_and?; split_and?; simplify_option_eq;
    try match goal with
    | H : ¬(_  _) |- _ => apply not_and_l in H as [?%dec_stable|?%dec_stable]
    end; eauto using is_closed_weaken with set_solver.
Qed.
Lemma is_closed_do_subst' X e x es :
  is_closed [] es  is_closed (x :b: X) e  is_closed X (subst' x es e).
Proof. destruct x; eauto using is_closed_subst. Qed.

(* Substitution *)
Lemma subst_is_closed X e x es : is_closed X e  x  X  subst x es e = e.
Robbert Krebbers's avatar
Robbert Krebbers committed
351
Proof.
352
  revert X. induction e=> X /=; rewrite ?bool_decide_spec ?andb_True=> ??;
Robbert Krebbers's avatar
Robbert Krebbers committed
353 354
    repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver.
Qed.
355

356 357
Lemma subst_is_closed_nil e x es : is_closed [] e  subst x es e = e.
Proof. intros. apply subst_is_closed with []; set_solver. Qed.
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 387 388
Lemma subst_subst e x es es' :
  Closed [] es'  subst x es (subst x es' e) = subst x es' e.
Proof.
  intros. induction e; simpl; try (f_equal; by auto);
    simplify_option_eq; auto using subst_is_closed_nil with f_equal.
Qed.
Lemma subst_subst' e x es es' :
  Closed [] es'  subst' x es (subst' x es' e) = subst' x es' e.
Proof. destruct x; simpl; auto using subst_subst. Qed.

Lemma subst_subst_ne e x y es es' :
  Closed [] es  Closed [] es'  x  y 
  subst x es (subst y es' e) = subst y es' (subst x es e).
Proof.
  intros. induction e; simpl; try (f_equal; by auto);
    simplify_option_eq; auto using eq_sym, subst_is_closed_nil with f_equal.
Qed.
Lemma subst_subst_ne' e x y es es' :
  Closed [] es  Closed [] es'  x  y 
  subst' x es (subst' y es' e) = subst' y es' (subst' x es e).
Proof. destruct x, y; simpl; auto using subst_subst_ne with congruence. Qed.

Lemma subst_rec' f y e x es :
  x = f  x = y  x = BAnon 
  subst' x es (Rec f y e) = Rec f y e.
Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.
Lemma subst_rec_ne' f y e x es :
  (x  f  f = BAnon)  (x  y  y = BAnon) 
  subst' x es (Rec f y e) = Rec f y (subst' x es e).
Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.
389 390 391
End heap_lang.

(** Language *)
392 393
Program Instance heap_ectxi_lang :
  EctxiLanguage
394
    (heap_lang.expr) heap_lang.val heap_lang.ectx_item heap_lang.state := {|
Robbert Krebbers's avatar
Robbert Krebbers committed
395
  of_val := heap_lang.of_val; to_val := heap_lang.to_val;
396
  fill_item := heap_lang.fill_item; head_step := heap_lang.head_step
Robbert Krebbers's avatar
Robbert Krebbers committed
397
|}.
398
Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
399 400
  heap_lang.val_stuck, heap_lang.fill_item_val, 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.
406 407 408 409 410 411 412 413 414 415

(** Define some derived forms *)
Notation Lam x e := (Rec BAnon x e).
Notation Let x e1 e2 := (App (Lam x e2) e1).
Notation Seq e1 e2 := (Let BAnon e1 e2).
Notation LamV x e := (RecV BAnon x e).
Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
Notation SeqCtx e2 := (LetCtx BAnon e2).
Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)).