lang.v 12.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. *)
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).
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).
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 :=
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)
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.
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
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 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 ef : head_step e1 σ1 e2 σ2 ef  to_val e1 = None.
298
Proof. destruct 1; naive_solver. Qed.
299

300
Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef :
301
  head_step (fill_item Ki e) σ1 e2 σ2 ef  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]>σ) None.
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 := {|
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
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.