lang.v 12.3 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
Bind Scope expr_scope with expr.
62
63
64
65
66
67
68
69
70
71
72
73
74
75

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

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

89
Bind Scope val_scope with val.
90

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

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

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

114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
(** 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.

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.
Instance expr_dec_eq (e1 e2 : expr) : Decision (e1 = e2).
Proof. solve_decision. Defined.
Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2).
Proof.
 refine (cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
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.

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

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

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

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

222
(** The stepping relation *)
223
224
225
226
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)
227
228
229
  | _, _ => None
  end.

230
231
232
233
234
235
236
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)
237
238
239
  | _, _, _ => None
  end.

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

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

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

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

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

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

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

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

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

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

336
337
Lemma is_closed_of_val X v : is_closed X (of_val v).
Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.
338
339
340
End heap_lang.

(** Language *)
341
342
Program Instance heap_ectxi_lang :
  EctxiLanguage
343
    (heap_lang.expr) heap_lang.val heap_lang.ectx_item heap_lang.state := {|
Robbert Krebbers's avatar
Robbert Krebbers committed
344
  of_val := heap_lang.of_val; to_val := heap_lang.to_val;
345
  fill_item := heap_lang.fill_item; head_step := heap_lang.head_step
Robbert Krebbers's avatar
Robbert Krebbers committed
346
|}.
347
Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
348
349
  heap_lang.val_stuck, heap_lang.fill_item_val, heap_lang.fill_item_no_val_inj,
  heap_lang.head_ctx_step_val.
350

351
Canonical Structure heap_lang := ectx_lang (heap_lang.expr).
352

353
(* Prefer heap_lang names over ectx_language names. *)
354
Export heap_lang.