Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found
Select Git revision

Target

Select target project
  • iris/iris
  • jeehoon.kang/iris-coq
  • amintimany/iris-coq
  • dfrumin/iris-coq
  • Villetaneuse/iris
  • gares/iris
  • shiatsumat/iris
  • Blaisorblade/iris
  • jihgfee/iris-coq
  • mrhaandi/iris
  • tlsomers/iris
  • Quarkbeast/iris-coq
  • janno/iris
  • amaurremi/iris-coq
  • proux/iris
  • tchajed/iris
  • herbelin/iris-coq
  • msammler/iris-coq
  • maximedenes/iris-coq
  • bpeters/iris
  • haidang/iris
  • lepigre/iris
  • lczch/iris
  • simonspies/iris
  • gpirlea/iris
  • dkhalanskiyjb/iris
  • gmalecha/iris
  • germanD/iris
  • aa755/iris
  • jules/iris
  • abeln/iris
  • simonfv/iris
  • atrieu/iris
  • arthuraa/iris
  • simonh/iris
  • jung/iris
  • mattam82/iris
  • Armael/iris
  • adamAndMath/iris
  • gmevel/iris
  • snyke7/iris
  • johannes/iris
  • NiklasM/iris
  • simonspies/iris-parametric-index
  • svancollem/iris
  • proux1/iris
  • wmansky/iris
  • LukeXuan/iris
  • ivanbakel/iris
  • SkySkimmer/iris
  • tjhance/iris
  • yiyunliu/iris
  • Lee-Janggun/iris
  • thomas-lamiaux/iris
  • dongjae/iris
  • dnezam/iris
  • Tragicus/iris
  • clef-men/iris
  • ffengyu/iris
59 results
Select Git revision
Show changes
Commits on Source (3)
From program_logic Require Export language.
From prelude Require Export strings.
From prelude Require Export strings stringmap.
From prelude Require Import gmap.
Module heap_lang.
......@@ -15,35 +15,45 @@ Inductive un_op : Set :=
Inductive bin_op : Set :=
| PlusOp | MinusOp | LeOp | LtOp | EqOp.
Inductive expr :=
(* expr X is the type of expressions with free variables bounded by X.
I removed the "empty binder" hack since it does not go well with
proof irrelevance of the proof required for [Var]. If we really want
that back, we should change the binders in [Rec] to "option string". *)
Inductive expr {X : stringset} : Type :=
(* Base lambda calculus *)
| Var (x : string)
| Rec (f x : string) (e : expr)
| App (e1 e2 : expr)
| Var (x : string) {H : x X} : @expr X
| Rec (f x : string) (e : @expr ((X {[ x ]}) {[ f ]})) : @expr X
| App (e1 e2 : @expr X) : @expr X
(* Base types and their operations *)
| Lit (l : base_lit)
| UnOp (op : un_op) (e : expr)
| BinOp (op : bin_op) (e1 e2 : expr)
| If (e0 e1 e2 : expr)
| Lit (l : base_lit) : @expr X
| UnOp (op : un_op) (e : @expr X) : @expr X
| BinOp (op : bin_op) (e1 e2 : @expr X) : @expr X
| If (e0 e1 e2 : @expr X) : @expr X
(* Products *)
| Pair (e1 e2 : expr)
| Fst (e : expr)
| Snd (e : expr)
| Pair (e1 e2 : @expr X) : @expr X
| Fst (e : @expr X) : @expr X
| Snd (e : @expr X) : @expr X
(* Sums *)
| InjL (e : expr)
| InjR (e : expr)
| Case (e0 : expr) (x1 : string) (e1 : expr) (x2 : string) (e2 : expr)
| InjL (e : @expr X) : @expr X
| InjR (e : @expr X) : @expr X
| Case (e0 e1 e2 : @expr X) : @expr X
(* Concurrency *)
| Fork (e : expr)
| Fork (e : @expr X) : @expr X
(* Heap *)
| Loc (l : loc)
| Alloc (e : expr)
| Load (e : expr)
| Store (e1 : expr) (e2 : expr)
| Cas (e0 : expr) (e1 : expr) (e2 : expr).
| Loc (l : loc) : @expr X
| Alloc (e : @expr X) : @expr X
| Load (e : @expr X) : @expr X
| Store (e1 e2 : @expr X) : @expr X
| Cas (e0 e1 e2 : @expr X) : @expr X.
(* X should be explicit for a few of them: Those that do not take an expr of the same X *)
Arguments expr _ : clear implicits.
Arguments Var _ _ {_} : clear implicits.
Arguments Rec _ _ _ _ : clear implicits.
Arguments Lit _ _ : clear implicits.
Arguments Loc _ _ : clear implicits.
Inductive val :=
| RecV (f x : string) (e : expr) (* e should be closed *)
| RecV (f x : string) (e : expr (( {[ x ]}) {[ f ]}))
| LitV (l : base_lit)
| PairV (v1 v2 : val)
| InjLV (v : val)
......@@ -56,25 +66,56 @@ Global Instance un_op_dec_eq (op1 op2 : un_op) : Decision (op1 = op2).
Proof. solve_decision. Defined.
Global Instance bin_op_dec_eq (op1 op2 : bin_op) : Decision (op1 = op2).
Proof. solve_decision. Defined.
Global Instance expr_dec_eq (e1 e2 : expr) : Decision (e1 = e2).
(*Global Instance expr_dec_eq {X} (e1 e2 : expr X) : Decision (e1 = e2).
Proof. solve_decision. Defined.
Global Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2).
Proof. solve_decision. Defined.
Proof. solve_decision. Defined.*)
Delimit Scope lang_scope with L.
Bind Scope lang_scope with expr val.
Fixpoint of_val (v : val) : expr :=
match v with
| RecV f x e => Rec f x e
| LitV l => Lit l
| PairV v1 v2 => Pair (of_val v1) (of_val v2)
| InjLV v => InjL (of_val v)
| InjRV v => InjR (of_val v)
| LocV l => Loc l
Definition expr_cast {X1 X2} {H : X1 = X2} (e : expr X1) : expr X2 :=
eq_rect _ (λ X, expr X) e _ H.
Program Fixpoint expr_weaken {X1 X2 : stringset} {H : X1 X2} (e : expr X1) : expr X2 :=
match e return _ with
| Var x Hx => Var X2 x
| Rec f x e => Rec X2 f x (expr_weaken e)
| App e1 e2 => App (expr_weaken (H:=H) e1) (expr_weaken (H:=H) e2)
| Lit l => Lit X2 l
| UnOp op e => UnOp op (expr_weaken (H:=H) e)
| BinOp op e1 e2 => BinOp op (expr_weaken (H:=H) e1) (expr_weaken (H:=H) e2)
| If e0 e1 e2 => If (expr_weaken (H:=H) e0) (expr_weaken (H:=H) e1) (expr_weaken (H:=H) e2)
| Pair e1 e2 => Pair (expr_weaken (H:=H) e1) (expr_weaken (H:=H) e2)
| Fst e => Fst (expr_weaken (H:=H) e)
| Snd e => Snd (expr_weaken (H:=H) e)
| InjL e => InjL (expr_weaken (H:=H) e)
| InjR e => InjR (expr_weaken (H:=H) e)
| Case e0 e1 e2 => Case (expr_weaken (H:=H) e0) (expr_weaken (H:=H) e1) (expr_weaken (H:=H) e2)
| Fork e => Fork (expr_weaken (H:=H) e)
| Loc l => Loc X2 l
| Alloc e => Alloc (expr_weaken (H:=H) e)
| Load e => Load (expr_weaken (H:=H) e)
| Store e1 e2 => Store (expr_weaken (H:=H) e1) (expr_weaken (H:=H) e2)
| Cas e0 e1 e2 => Cas (expr_weaken (H:=H) e0) (expr_weaken (H:=H) e1) (expr_weaken (H:=H) e2)
end.
Fixpoint to_val (e : expr) : option val :=
match e with
Solve Obligations with set_solver.
Program Fixpoint of_val X (v : val) : expr X :=
match v return expr X with
| RecV f x e => Rec X f x (expr_weaken e)
| LitV l => Lit X l
| PairV v1 v2 => Pair (of_val X v1) (of_val X v2)
| InjLV v => InjL (of_val X v)
| InjRV v => InjR (of_val X v)
| LocV l => Loc X l
end.
Solve Obligations with set_solver.
Fixpoint to_val (e : expr ) : option val :=
match e return option val with
(* The LHS of thus ⊆ must be like the argument of Rec, the RHS
must be like the argument of RecV. *)
| Rec f x e => Some (RecV f x e)
| Lit l => Some (LitV l)
| Pair e1 e2 => v1 to_val e1; v2 to_val e2; Some (PairV v1 v2)
......@@ -89,82 +130,94 @@ Definition state := gmap loc val.
(** Evaluation contexts *)
Inductive ectx_item :=
| AppLCtx (e2 : expr)
| AppLCtx (e2 : expr )
| AppRCtx (v1 : val)
| UnOpCtx (op : un_op)
| BinOpLCtx (op : bin_op) (e2 : expr)
| BinOpLCtx (op : bin_op) (e2 : expr )
| BinOpRCtx (op : bin_op) (v1 : val)
| IfCtx (e1 e2 : expr)
| PairLCtx (e2 : expr)
| IfCtx (e1 e2 : expr )
| PairLCtx (e2 : expr )
| PairRCtx (v1 : val)
| FstCtx
| SndCtx
| InjLCtx
| InjRCtx
| CaseCtx (x1 : string) (e1 : expr) (x2 : string) (e2 : expr)
| CaseCtx (e1 : expr ) (e2 : expr )
| AllocCtx
| LoadCtx
| StoreLCtx (e2 : expr)
| StoreLCtx (e2 : expr )
| StoreRCtx (v1 : val)
| CasLCtx (e1 : expr) (e2 : expr)
| CasMCtx (v0 : val) (e2 : expr)
| CasLCtx (e1 : expr ) (e2 : expr )
| CasMCtx (v0 : val) (e2 : expr )
| CasRCtx (v0 : val) (v1 : val).
Notation ectx := (list ectx_item).
Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
match Ki with
Definition fill_item (Ki : ectx_item) (e : expr ) : expr :=
match Ki return expr with
| AppLCtx e2 => App e e2
| AppRCtx v1 => App (of_val v1) e
| AppRCtx v1 => App (of_val v1) e
| UnOpCtx op => UnOp op e
| BinOpLCtx op e2 => BinOp op e e2
| BinOpRCtx op v1 => BinOp op (of_val v1) e
| BinOpRCtx op v1 => BinOp op (of_val v1) e
| IfCtx e1 e2 => If e e1 e2
| PairLCtx e2 => Pair e e2
| PairRCtx v1 => Pair (of_val v1) e
| PairRCtx v1 => Pair (of_val v1) e
| FstCtx => Fst e
| SndCtx => Snd e
| InjLCtx => InjL e
| InjRCtx => InjR e
| CaseCtx x1 e1 x2 e2 => Case e x1 e1 x2 e2
| CaseCtx e1 e2 => Case e e1 e2
| AllocCtx => Alloc e
| LoadCtx => Load e
| StoreLCtx e2 => Store e e2
| StoreRCtx v1 => Store (of_val v1) e
| StoreRCtx v1 => Store (of_val v1) e
| 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
| CasMCtx v0 e2 => Cas (of_val v0) e e2
| CasRCtx v0 v1 => Cas (of_val v0) (of_val v1) e
end.
Definition fill (K : ectx) (e : expr) : expr := fold_right fill_item e K.
Definition fill (K : ectx) (e : expr ) : expr := fold_right fill_item e K.
(** Substitution *)
(** We have [subst e "" v = e] to deal with anonymous binders *)
Fixpoint subst (e : expr) (x : string) (v : val) : expr :=
match e with
| Var y => if decide (x = y x "") then of_val v else Var y
| Rec f y e => Rec f y (if decide (x f x y) then subst e x v else e)
| App e1 e2 => App (subst e1 x v) (subst e2 x v)
| Lit l => Lit l
| UnOp op e => UnOp op (subst e x v)
| BinOp op e1 e2 => BinOp op (subst e1 x v) (subst e2 x v)
| If e0 e1 e2 => If (subst e0 x v) (subst e1 x v) (subst e2 x v)
| Pair e1 e2 => Pair (subst e1 x v) (subst e2 x v)
| Fst e => Fst (subst e x v)
| Snd e => Snd (subst e x v)
| InjL e => InjL (subst e x v)
| InjR e => InjR (subst e x v)
| Case e0 x1 e1 x2 e2 =>
Case (subst e0 x v)
x1 (if decide (x x1) then subst e1 x v else e1)
x2 (if decide (x x2) then subst e2 x v else e2)
| Fork e => Fork (subst e x v)
| Loc l => Loc l
| Alloc e => Alloc (subst e x v)
| Load e => Load (subst e x v)
| Store e1 e2 => Store (subst e1 x v) (subst e2 x v)
| Cas e0 e1 e2 => Cas (subst e0 x v) (subst e1 x v) (subst e2 x v)
Program Fixpoint subst X (x : string) (v : val) (e : expr (X {[ x ]})) :
expr X :=
match e return expr X with
| Var y Hx => if decide (x = y) then of_val X v
else Var X y
| Rec f y e => Rec X f y (if decide (x f x y)
then subst ((X {[ y ]}) {[ f ]}) x v (expr_cast e)
else expr_cast e)
| App e1 e2 => App (subst X x v e1) (subst X x v e2)
| Lit l => Lit X l
| UnOp op e => UnOp op (subst X x v e)
| BinOp op e1 e2 => BinOp op (subst X x v e1) (subst X x v e2)
| If e0 e1 e2 => If (subst X x v e0) (subst X x v e1) (subst X x v e2)
| Pair e1 e2 => Pair (subst X x v e1) (subst X x v e2)
| Fst e => Fst (subst X x v e)
| Snd e => Snd (subst X x v e)
| InjL e => InjL (subst X x v e)
| InjR e => InjR (subst X x v e)
| Case e0 e1 e2 =>
Case (subst X x v e0) (subst X x v e1) (subst X x v e2)
| Fork e => Fork (subst X x v e)
| Loc l => Loc X l
| Alloc e => Alloc (subst X x v e)
| Load e => Load (subst X x v e)
| Store e1 e2 => Store (subst X x v e1) (subst X x v e2)
| Cas e0 e1 e2 => Cas (subst X x v e0) (subst X x v e1) (subst X x v e2)
end.
Next Obligation. set_solver. Qed.
Next Obligation. set_solver. Qed.
(* FIXME fix this *)
Next Obligation.
intros ??????? [H%dec_stable|H%dec_stable]%not_and_l; subst.
- apply elem_of_equiv_L=>x.
destruct (decide (x = f)); set_solver.
- apply elem_of_equiv_L=>x.
destruct (decide (x = y)); set_solver.
Qed.
(** The stepping relation *)
Definition un_op_eval (op : un_op) (l : base_lit) : option base_lit :=
match op, l with
......@@ -183,55 +236,61 @@ Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
| _, _, _ => None
end.
Inductive head_step : expr state expr state option expr Prop :=
| BetaS f x e1 e2 v2 σ :
Inductive head_step : expr state expr state option (expr ) Prop :=
(* The second "x" in the type of [e1] should be an "f". *)
| BetaS (f x : string) (e1 : expr (( {[ x ]}) {[ x ]})) (e2 : expr ) v2 (σ : state) :
to_val e2 = Some v2
head_step (App (Rec f x e1) e2) σ
(subst (subst e1 f (RecV f x e1)) x v2) σ None
head_step (App (Rec f x e1) e2) σ
(subst x v2 (subst ( {[ x ]}) f (RecV f x e1) e1)) σ None.
Set Printing All.
Print head_step.
| UnOpS op l l' σ :
un_op_eval op l = Some l'
head_step (UnOp op (Lit l)) σ (Lit l') σ None
head_step (UnOp op (Lit l)) σ (Lit l') σ None
| BinOpS op l1 l2 l' σ :
bin_op_eval op l1 l2 = Some l'
head_step (BinOp op (Lit l1) (Lit l2)) σ (Lit l') σ None
head_step (BinOp op (Lit l1) (Lit l2)) σ (Lit l') σ None
| IfTrueS e1 e2 σ :
head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ None
head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ None
| IfFalseS e1 e2 σ :
head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ None
head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ None
| 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
| CaseLS e0 v0 x1 e1 x2 e2 σ :
| CaseLS e0 v0 e1 e2 σ :
to_val e0 = Some v0
head_step (Case (InjL e0) x1 e1 x2 e2) σ (subst e1 x1 v0) σ None
| CaseRS e0 v0 x1 e1 x2 e2 σ :
head_step (Case (InjL e0) e1 e2) σ (App e1 (of_val v0)) σ None
| CaseRS e0 v0 e1 e2 σ :
to_val e0 = Some v0
head_step (Case (InjR e0) x1 e1 x2 e2) σ (subst e2 x2 v0) σ None
head_step (Case (InjR e0) e1 e2) σ (App e2 (of_val v0)) σ None
| ForkS e σ:
head_step (Fork e) σ (Lit LitUnit) σ (Some e)
head_step (Fork e) σ (Lit LitUnit) σ (Some e)
| AllocS e v σ l :
to_val e = Some v σ !! l = None
head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None
head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None
| LoadS l v σ :
σ !! l = Some v
head_step (Load (Loc l)) σ (of_val v) σ None
head_step (Load (Loc l)) σ (of_val v) σ None
| StoreS l e v σ :
to_val e = Some v is_Some (σ !! l)
head_step (Store (Loc l) e) σ (Lit LitUnit) (<[l:=v]>σ) None
head_step (Store (Loc l) e) σ (Lit LitUnit) (<[l:=v]>σ) None
| CasFailS l e1 v1 e2 v2 vl σ :
to_val e1 = Some v1 to_val e2 = Some v2
σ !! l = Some vl vl v1
head_step (Cas (Loc l) e1 e2) σ (Lit $ LitBool false) σ None
head_step (Cas (Loc l) e1 e2) σ (Lit $ LitBool false) σ None
| CasSucS l e1 v1 e2 v2 σ :
to_val e1 = Some v1 to_val e2 = Some v2
σ !! l = Some v1
head_step (Cas (Loc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None.
head_step (Cas (Loc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None.
(** Atomic expressions *)
Definition atomic (e: expr) : Prop :=
Definition atomic (e: expr ) : Prop :=
match e with
| Alloc e => is_Some (to_val e)
| Load e => is_Some (to_val e)
......@@ -245,25 +304,71 @@ Definition atomic (e: expr) : Prop :=
(** Close reduction under evaluation contexts.
We could potentially make this a generic construction. *)
Inductive prim_step
(e1 : expr) (σ1 : state) (e2 : expr) (σ2: state) (ef: option expr) : Prop :=
(e1 : expr ) (σ1 : state) (e2 : expr ) (σ2: state) (ef: option (expr )) : Prop :=
Ectx_step K e1' e2' :
e1 = fill K e1' e2 = fill K e2'
head_step e1' σ1 e2' σ2 ef prim_step e1 σ1 e2 σ2 ef.
(** The equalities we need for some lemmas. *)
Lemma stringset_eq_1 {X : stringset} :
X = X.
Proof. set_solver. Qed.
Lemma stringset_eq_2 {f x : string} :
(({[f; x]} {[f]}) {[x]}) = ( : stringset).
Proof. set_solver. Qed.
Lemma stringset_subseteq_1 {X : stringset} :
X.
Proof. set_solver. Qed.
(** Properties of the cast operators *)
Lemma not_or_l {P Q : Prop} `{Decision P} : ¬(P Q) ¬P ¬Q.
Proof. destruct (decide P); tauto. Qed.
Lemma not_or_r {P Q : Prop} `{Decision Q} : ¬(P Q) ¬P ¬Q.
Proof. destruct (decide Q); tauto. Qed.
Lemma expr_weaken_id {X : stringset} {H : X X} (e : expr X) :
expr_weaken (H:=H) e = e.
Proof.
induction e; simpl; by (f_equal; try apply proof_irrel; eauto).
Qed.
Lemma expr_weaken_cast_id {X Y : stringset} {H1 : Y X} {H2 : X = Y} (e : expr X) :
expr_weaken (H:=H1) (expr_cast (H:=H2) e) = e.
Proof.
destruct H2. by apply expr_weaken_id.
Qed.
Lemma expr_weaken_cast_weaken_id {X Y Z : stringset} {H1 : Z X} {H2 : Y = Z} {H3 : X Y} (e : expr X) :
expr_weaken (H:=H1) (expr_cast (H:=H2) (expr_weaken (H:=H3) e)) = e.
Proof.
destruct H2. assert (X = Y) by set_solver. subst Y. by rewrite !expr_weaken_id.
Qed.
Lemma expr_cast_val {X Y : stringset} {H : X = Y} e:
to_val (expr_cast (H:=H) e) = to_val e.
Proof. destruct H. done. Qed.
(** Basic properties about the language *)
Lemma to_of_val v : to_val (of_val v) = Some v.
Proof. by induction v; simplify_option_eq. Qed.
Proof.
induction v; simpl; try case_match; simplify_option_eq; try done.
- f_equiv. f_equiv. by rewrite expr_weaken_cast_id.
- exfalso. apply H. set_solver+.
Qed.
Lemma of_to_val e v : to_val e = Some v of_val v = e.
Lemma of_to_val' X (e : expr X) v : to_val e = Some v expr_weaken (H:=stringset_subseteq_1) (of_val v) = e.
Proof.
revert v; induction e; intros; simplify_option_eq; auto with f_equal.
f_equiv. by rewrite expr_weaken_cast_weaken_id.
Qed.
Instance: Inj (=) (=) of_val.
Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
Proof. destruct Ki; intros ?? H; simpl in *; inversion_clear H; done. Qed.
Instance ectx_fill_inj K : Inj (=) (=) (fill K).
Proof. red; induction K as [|Ki K IH]; naive_solver. Qed.
......@@ -294,6 +399,7 @@ Lemma atomic_fill_item Ki e : atomic (fill_item Ki e) → is_Some (to_val e).
Proof.
intros. destruct Ki; simplify_eq/=; destruct_conjs;
repeat (case_match || contradiction); eauto.
simpl. case_match; first by eauto. exfalso. apply n. set_solver+.
Qed.
Lemma atomic_fill K e : atomic (fill K e) to_val e = None K = [].
......@@ -307,6 +413,7 @@ Lemma atomic_head_step e1 σ1 e2 σ2 ef :
Proof.
destruct 2; simpl; rewrite ?to_of_val; try by eauto.
repeat (case_match || contradiction || simplify_eq/=); eauto.
rewrite expr_cast_val.
Qed.
Lemma atomic_step e1 σ1 e2 σ2 ef :
......