lang.v 12.6 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  list (expr)  Prop :=
229
  | BetaS f x e1 e2 v2 e' σ :
230
     to_val e2 = Some v2 
231
     Closed (f :b: x :b: []) e1 
232
     e' = subst' x (of_val v2) (subst' f (Rec f x e1) e1) 
233
     head_step (App (Rec f x e1) e2) σ e' σ []
234
  | UnOpS op l l' σ :
235
     un_op_eval op l = Some l'  
236
     head_step (UnOp op (Lit l)) σ (Lit l') σ []
237
  | BinOpS op l1 l2 l' σ :
238
     bin_op_eval op l1 l2 = Some l'  
239
     head_step (BinOp op (Lit l1) (Lit l2)) σ (Lit l') σ []
240
  | IfTrueS e1 e2 σ :
241
     head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ []
242
  | IfFalseS e1 e2 σ :
243
     head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ []
244
245
  | FstS e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
246
     head_step (Fst (Pair e1 e2)) σ e1 σ []
247
248
  | SndS e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
249
     head_step (Snd (Pair e1 e2)) σ e2 σ []
250
  | CaseLS e0 v0 e1 e2 σ :
251
     to_val e0 = Some v0 
252
     head_step (Case (InjL e0) e1 e2) σ (App e1 e0) σ []
253
  | CaseRS e0 v0 e1 e2 σ :
254
     to_val e0 = Some v0 
255
     head_step (Case (InjR e0) e1 e2) σ (App e2 e0) σ []
256
  | ForkS e σ:
257
     head_step (Fork e) σ (Lit LitUnit) σ [e]
258
259
  | AllocS e v σ l :
     to_val e = Some v  σ !! l = None 
260
     head_step (Alloc e) σ (Lit $ LitLoc l) (<[l:=v]>σ) []
261
262
  | LoadS l v σ :
     σ !! l = Some v 
263
     head_step (Load (Lit $ LitLoc l)) σ (of_val v) σ []
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]>σ) []
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) σ []
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]>σ) [].
Ralf Jung's avatar
Ralf Jung committed
275

276
277
(** Basic properties about the language *)
Lemma to_of_val v : to_val (of_val v) = Some v.
278
279
280
Proof.
  by induction v; simplify_option_eq; repeat f_equal; try apply (proof_irrel _).
Qed.
281

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

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

290
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
291
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
292

293
294
295
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.
296

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
319
320
321
322
(** 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.

323
324
325
326
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
327
Proof.
328
  revert X. induction e=> X /=; rewrite ?bool_decide_spec ?andb_True=> ??;
Robbert Krebbers's avatar
Robbert Krebbers committed
329
330
    repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver.
Qed.
331

332
333
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.
334

335
336
Lemma is_closed_of_val X v : is_closed X (of_val v).
Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.
337

Ralf Jung's avatar
Ralf Jung committed
338
(** Equality and other typeclass stuff *)
339
340
341
342
343
344
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.
345
346
Instance expr_dec_eq (e1 e2 : expr) : Decision (e1 = e2).
Proof. solve_decision. Defined.
347
Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2).
348
Proof.
349
350
 refine (cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
Defined.
Ralf Jung's avatar
Ralf Jung committed
351

352
Instance expr_inhabited : Inhabited (expr) := populate (Lit LitUnit).
Ralf Jung's avatar
Ralf Jung committed
353
Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
354
355
356

Canonical Structure stateC := leibnizC state.
Canonical Structure valC := leibnizC val.
357
Canonical Structure exprC := leibnizC expr.
358
359
360
End heap_lang.

(** Language *)
361
362
Program Instance heap_ectxi_lang :
  EctxiLanguage
363
    (heap_lang.expr) heap_lang.val heap_lang.ectx_item heap_lang.state := {|
Robbert Krebbers's avatar
Robbert Krebbers committed
364
  of_val := heap_lang.of_val; to_val := heap_lang.to_val;
365
  fill_item := heap_lang.fill_item; head_step := heap_lang.head_step
Robbert Krebbers's avatar
Robbert Krebbers committed
366
|}.
367
Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
368
369
  heap_lang.val_stuck, heap_lang.fill_item_val, heap_lang.fill_item_no_val_inj,
  heap_lang.head_ctx_step_val.
370

371
Canonical Structure heap_lang := ectx_lang (heap_lang.expr).
372

373
(* Prefer heap_lang names over ectx_language names. *)
374
Export heap_lang.