lang.v 12.2 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
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).
25
Instance binder_eq_dec_eq : EqDecision binder.
26
27
28
29
30
31
32
33
34
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
(** 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.

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