Commit f4fb2305 authored by Ralf Jung's avatar Ralf Jung

define an interface of "evaluation-context-based languages" and use it for heap_lang

parent 4e756c6d
...@@ -70,6 +70,7 @@ program_logic/pviewshifts.v ...@@ -70,6 +70,7 @@ program_logic/pviewshifts.v
program_logic/resources.v program_logic/resources.v
program_logic/hoare.v program_logic/hoare.v
program_logic/language.v program_logic/language.v
program_logic/ectx_language.v
program_logic/ghost_ownership.v program_logic/ghost_ownership.v
program_logic/global_functor.v program_logic/global_functor.v
program_logic/saved_prop.v program_logic/saved_prop.v
......
From iris.program_logic Require Export language. From iris.program_logic Require Export ectx_language.
From iris.prelude Require Export strings. From iris.prelude Require Export strings.
From iris.prelude Require Import gmap. From iris.prelude Require Import gmap.
...@@ -355,14 +355,6 @@ Definition atomic (e: expr []) : Prop := ...@@ -355,14 +355,6 @@ Definition atomic (e: expr []) : Prop :=
| _ => False | _ => False
end. end.
(** 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 :=
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.
(** Substitution *) (** Substitution *)
Lemma var_proof_irrel X x H1 H2 : @Var X x H1 = @Var X x H2. Lemma var_proof_irrel X x H1 H2 : @Var X x H1 = @Var X x H2.
Proof. f_equal. by apply (proof_irrel _). Qed. Proof. f_equal. by apply (proof_irrel _). Qed.
...@@ -457,11 +449,12 @@ Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed. ...@@ -457,11 +449,12 @@ Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki). Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed. Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
Instance ectx_fill_inj K : Inj (=) (=) (fill K). Instance fill_inj K : Inj (=) (=) (fill K).
Proof. red; induction K as [|Ki K IH]; naive_solver. Qed. Proof. red; induction K as [|Ki K IH]; naive_solver. Qed.
Lemma fill_app K1 K2 e : fill (K1 ++ K2) e = fill K1 (fill K2 e). Lemma fill_inj' K e1 e2 :
Proof. revert e; induction K1; simpl; auto with f_equal. Qed. fill K e1 = fill K e2 e1 = e2.
Proof. eapply fill_inj. Qed.
Lemma fill_val K e : is_Some (to_val (fill K e)) is_Some (to_val e). Lemma fill_val K e : is_Some (to_val (fill K e)) is_Some (to_val e).
Proof. Proof.
...@@ -472,13 +465,10 @@ Qed. ...@@ -472,13 +465,10 @@ Qed.
Lemma fill_not_val K e : to_val e = None to_val (fill K e) = None. Lemma fill_not_val K e : to_val e = None to_val (fill K e) = None.
Proof. rewrite !eq_None_not_Some; eauto using fill_val. Qed. Proof. rewrite !eq_None_not_Some; eauto using fill_val. Qed.
Lemma val_head_stuck e1 σ1 e2 σ2 ef : Lemma val_stuck e1 σ1 e2 σ2 ef :
head_step e1 σ1 e2 σ2 ef to_val e1 = None. head_step e1 σ1 e2 σ2 ef to_val e1 = None.
Proof. destruct 1; naive_solver. Qed. Proof. destruct 1; naive_solver. Qed.
Lemma val_stuck e1 σ1 e2 σ2 ef : prim_step e1 σ1 e2 σ2 ef to_val e1 = None.
Proof. intros [??? -> -> ?]; eauto using fill_not_val, val_head_stuck. Qed.
Lemma atomic_not_val e : atomic e to_val e = None. Lemma atomic_not_val e : atomic e to_val e = None.
Proof. destruct e; naive_solver. Qed. Proof. destruct e; naive_solver. Qed.
...@@ -494,21 +484,13 @@ Proof. ...@@ -494,21 +484,13 @@ Proof.
rewrite eq_None_not_Some=> /= ? []; eauto using atomic_fill_item, fill_val. rewrite eq_None_not_Some=> /= ? []; eauto using atomic_fill_item, fill_val.
Qed. Qed.
Lemma atomic_head_step e1 σ1 e2 σ2 ef : Lemma atomic_step e1 σ1 e2 σ2 ef :
atomic e1 head_step e1 σ1 e2 σ2 ef is_Some (to_val e2). atomic e1 head_step e1 σ1 e2 σ2 ef is_Some (to_val e2).
Proof. Proof.
destruct 2; simpl; rewrite ?to_of_val; try by eauto. subst. destruct 2; simpl; rewrite ?to_of_val; try by eauto. subst.
unfold subst'; repeat (case_match || contradiction || simplify_eq/=); eauto. unfold subst'; repeat (case_match || contradiction || simplify_eq/=); eauto.
Qed. Qed.
Lemma atomic_step e1 σ1 e2 σ2 ef :
atomic e1 prim_step e1 σ1 e2 σ2 ef is_Some (to_val e2).
Proof.
intros Hatomic [K e1' e2' -> -> Hstep].
assert (K = []) as -> by eauto 10 using atomic_fill, val_head_stuck.
naive_solver eauto using atomic_head_step.
Qed.
Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef : Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef :
head_step (fill_item Ki e) σ1 e2 σ2 ef is_Some (to_val e). head_step (fill_item Ki e) σ1 e2 σ2 ef is_Some (to_val e).
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; eauto. Qed. Proof. destruct Ki; inversion_clear 1; simplify_option_eq; eauto. Qed.
...@@ -528,15 +510,15 @@ has a non-val [e] in the hole, then [K] is a left sub-context of [K'] - in ...@@ -528,15 +510,15 @@ has a non-val [e] in the hole, then [K] is a left sub-context of [K'] - in
other words, [e] also contains the reducible expression *) other words, [e] also contains the reducible expression *)
Lemma step_by_val K K' e1 e1' σ1 e2 σ2 ef : Lemma step_by_val K K' e1 e1' σ1 e2 σ2 ef :
fill K e1 = fill K' e1' to_val e1 = None head_step e1' σ1 e2 σ2 ef fill K e1 = fill K' e1' to_val e1 = None head_step e1' σ1 e2 σ2 ef
K `prefix_of` K'. exists K'', K' = K ++ K''. (* K `prefix_of` K' *)
Proof. Proof.
intros Hfill Hred Hnval; revert K' Hfill. intros Hfill Hred Hnval; revert K' Hfill.
induction K as [|Ki K IH]; simpl; intros K' Hfill; auto using prefix_of_nil. induction K as [|Ki K IH]; simpl; intros K' Hfill; first by eauto.
destruct K' as [|Ki' K']; simplify_eq/=. destruct K' as [|Ki' K']; simplify_eq/=.
{ exfalso; apply (eq_None_not_Some (to_val (fill K e1))); { exfalso; apply (eq_None_not_Some (to_val (fill K e1)));
eauto using fill_not_val, head_ctx_step_val. } eauto using fill_not_val, head_ctx_step_val. }
cut (Ki = Ki'); [naive_solver eauto using prefix_of_cons|]. cut (Ki = Ki'); [naive_solver eauto using prefix_of_cons|].
eauto using fill_item_no_val_inj, val_head_stuck, fill_not_val. eauto using fill_item_no_val_inj, val_stuck, fill_not_val.
Qed. Qed.
Lemma alloc_fresh e v σ : Lemma alloc_fresh e v σ :
...@@ -592,31 +574,23 @@ Instance val_inhabited : Inhabited val := populate (LitV LitUnit). ...@@ -592,31 +574,23 @@ Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
End heap_lang. End heap_lang.
(** Language *) (** Language *)
Program Canonical Structure heap_lang : language := {| Program Canonical Structure heap_ectx_lang :
expr := heap_lang.expr []; val := heap_lang.val; state := heap_lang.state; ectx_language (heap_lang.expr []) heap_lang.val heap_lang.ectx heap_lang.state
:= {|
of_val := heap_lang.of_val; to_val := heap_lang.to_val; of_val := heap_lang.of_val; to_val := heap_lang.to_val;
atomic := heap_lang.atomic; prim_step := heap_lang.prim_step; empty_ectx := []; comp_ectx := app; fill := heap_lang.fill;
|}. atomic := heap_lang.atomic; head_step := heap_lang.head_step;
|}.
Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val, Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
heap_lang.val_stuck, heap_lang.atomic_not_val, heap_lang.atomic_step. heap_lang.val_stuck, heap_lang.atomic_not_val, heap_lang.atomic_step,
heap_lang.fill_inj', heap_lang.fill_not_val, heap_lang.atomic_fill,
heap_lang.step_by_val, fold_right_app.
Global Instance heap_lang_ctx K : LanguageCtx heap_lang (heap_lang.fill K). Canonical Structure heap_lang := ectx_lang heap_ectx_lang.
Proof.
split.
- eauto using heap_lang.fill_not_val.
- intros ????? [K' e1' e2' Heq1 Heq2 Hstep].
by exists (K ++ K') e1' e2'; rewrite ?heap_lang.fill_app ?Heq1 ?Heq2.
- intros e1 σ1 e2 σ2 ? Hnval [K'' e1'' e2'' Heq1 -> Hstep].
destruct (heap_lang.step_by_val
K K'' e1 e1'' σ1 e2'' σ2 ef) as [K' ->]; eauto.
rewrite heap_lang.fill_app in Heq1; apply (inj _) in Heq1.
exists (heap_lang.fill K' e2''); rewrite heap_lang.fill_app; split; auto.
econstructor; eauto.
Qed.
Global Instance heap_lang_ctx_item Ki : Global Instance heap_lang_ctx_item Ki :
LanguageCtx heap_lang (heap_lang.fill_item Ki). LanguageCtx heap_lang (heap_lang.fill_item Ki).
Proof. change (LanguageCtx heap_lang (heap_lang.fill [Ki])). apply _. Qed. Proof. change (LanguageCtx heap_lang (heap_lang.fill [Ki])). apply _. Qed.
(* Prefer heap_lang names over language names. *) (* Prefer heap_lang names over ectx_language names. *)
Export heap_lang. Export heap_lang.
...@@ -15,8 +15,8 @@ Implicit Types ef : option (expr []). ...@@ -15,8 +15,8 @@ Implicit Types ef : option (expr []).
(** Bind. *) (** Bind. *)
Lemma wp_bind {E e} K Φ : Lemma wp_bind {E e} K Φ :
WP e @ E {{ λ v, WP fill K (of_val v) @ E {{ Φ }}}} WP fill K e @ E {{ Φ }}. WP e @ E {{ λ v, WP fill K (of_val v) @ E {{ Φ }} }} WP fill K e @ E {{ Φ }}.
Proof. apply weakestpre.wp_bind. Qed. Proof. apply: weakestpre.wp_bind. Qed.
(** Base axioms for core primitives of the language: Stateful reductions. *) (** Base axioms for core primitives of the language: Stateful reductions. *)
Lemma wp_alloc_pst E σ e v Φ : Lemma wp_alloc_pst E σ e v Φ :
......
...@@ -13,13 +13,13 @@ Ltac inv_step := ...@@ -13,13 +13,13 @@ Ltac inv_step :=
| _ => progress simplify_map_eq/= (* simplify memory stuff *) | _ => progress simplify_map_eq/= (* simplify memory stuff *)
| H : to_val _ = Some _ |- _ => apply of_to_val in H | H : to_val _ = Some _ |- _ => apply of_to_val in H
| H : context [to_val (of_val _)] |- _ => rewrite to_of_val in H | H : context [to_val (of_val _)] |- _ => rewrite to_of_val in H
| H : prim_step _ _ _ _ _ |- _ => destruct H; subst | H : prim_step _ _ _ _ _ _ |- _ => destruct H; subst
| H : _ = fill ?K ?e |- _ => | H : _ = fill ?K ?e |- _ =>
destruct K as [|[]]; destruct K as [|[]];
simpl in H; first [subst e|discriminate H|injection H as H] simpl in H; first [subst e|discriminate H|injection H as H]
(* ensure that we make progress for each subgoal *) (* ensure that we make progress for each subgoal *)
| H : head_step ?e _ _ _ _, Hv : of_val ?v = fill ?K ?e |- _ => | H : head_step ?e _ _ _ _, Hv : of_val ?v = fill ?K ?e |- _ =>
apply val_head_stuck, (fill_not_val K) in H; apply val_stuck, (fill_not_val K) in H;
by rewrite -Hv to_of_val in H (* maybe use a helper lemma here? *) by rewrite -Hv to_of_val in H (* maybe use a helper lemma here? *)
| H : head_step ?e _ _ _ _ |- _ => | H : head_step ?e _ _ _ _ |- _ =>
try (is_var e; fail 1); (* inversion yields many goals if e is a variable try (is_var e; fail 1); (* inversion yields many goals if e is a variable
...@@ -81,7 +81,7 @@ Ltac do_step tac := ...@@ -81,7 +81,7 @@ Ltac do_step tac :=
try match goal with |- language.reducible _ _ => eexists _, _, _ end; try match goal with |- language.reducible _ _ => eexists _, _, _ end;
simpl; simpl;
match goal with match goal with
| |- prim_step ?e1 ?σ1 ?e2 ?σ2 ?ef => | |- prim_step _ ?e1 ?σ1 ?e2 ?σ2 ?ef =>
reshape_expr e1 ltac:(fun K e1' => reshape_expr e1 ltac:(fun K e1' =>
eapply Ectx_step with K e1' _; [reflexivity|reflexivity|]; eapply Ectx_step with K e1' _; [reflexivity|reflexivity|];
first [apply alloc_fresh|econstructor; try reflexivity; simpl_subst]; first [apply alloc_fresh|econstructor; try reflexivity; simpl_subst];
......
From iris.algebra Require Export base.
From iris.program_logic Require Export language.
(* We need to make thos arguments indices that we want canonical structure
inference to use a keys. *)
Class ectx_language (expr val ectx state : Type) := EctxLanguage {
of_val : val expr;
to_val : expr option val;
empty_ectx : ectx;
comp_ectx : ectx ectx ectx;
fill : ectx expr expr;
atomic : expr Prop;
head_step : expr state expr state option expr Prop;
to_of_val v : to_val (of_val v) = Some v;
of_to_val e v : to_val e = Some v of_val v = e;
val_stuck e1 σ1 e2 σ2 ef : head_step e1 σ1 e2 σ2 ef to_val e1 = None;
fill_empty e : fill empty_ectx e = e;
fill_comp K1 K2 e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e;
fill_inj K e1 e2 : fill K e1 = fill K e2 e1 = e2;
fill_not_val K e : to_val e = None to_val (fill K e) = None;
step_by_val K K' e1 e1' σ1 e2 σ2 ef :
fill K e1 = fill K' e1'
to_val e1 = None
head_step e1' σ1 e2 σ2 ef
exists K'', K' = comp_ectx K K'';
atomic_not_val e : atomic e to_val e = None;
atomic_step e1 σ1 e2 σ2 ef :
atomic e1
head_step e1 σ1 e2 σ2 ef
is_Some (to_val e2);
atomic_fill e K :
atomic (fill K e)
to_val e = None
K = empty_ectx;
}.
Arguments of_val {_ _ _ _ _} _.
Arguments to_val {_ _ _ _ _} _.
Arguments empty_ectx {_ _ _ _ _}.
Arguments comp_ectx {_ _ _ _ _} _ _.
Arguments fill {_ _ _ _ _} _ _.
Arguments atomic {_ _ _ _ _} _.
Arguments head_step {_ _ _ _ _} _ _ _ _ _.
Arguments to_of_val {_ _ _ _ _} _.
Arguments of_to_val {_ _ _ _ _} _ _ _.
Arguments val_stuck {_ _ _ _ _} _ _ _ _ _ _.
Arguments fill_empty {_ _ _ _ _} _.
Arguments fill_comp {_ _ _ _ _} _ _ _.
Arguments fill_inj {_ _ _ _ _} _ _ _ _.
Arguments fill_not_val {_ _ _ _ _} _ _ _.
Arguments step_by_val {_ _ _ _ _} _ _ _ _ _ _ _ _ _ _ _.
Arguments atomic_not_val {_ _ _ _ _} _ _.
Arguments atomic_step {_ _ _ _ _} _ _ _ _ _ _ _.
Arguments atomic_fill {_ _ _ _ _} _ _ _ _.
(* From an ectx_language, we can construct a language. *)
Section Language.
Context {expr val ectx state : Type} (Λ : ectx_language expr val ectx state).
Implicit Types (e : expr) (K : ectx).
Inductive prim_step (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.
Lemma val_prim_stuck e1 σ1 e2 σ2 ef :
prim_step e1 σ1 e2 σ2 ef to_val e1 = None.
Proof. intros [??? -> -> ?]; eauto using fill_not_val, val_stuck. Qed.
Lemma atomic_prim_step e1 σ1 e2 σ2 ef :
atomic e1 prim_step e1 σ1 e2 σ2 ef is_Some (to_val e2).
Proof.
intros Hatomic [K e1' e2' -> -> Hstep].
assert (K = empty_ectx) as -> by eauto 10 using atomic_fill, val_stuck.
eapply atomic_step; first done. by rewrite !fill_empty.
Qed.
Canonical Structure ectx_lang : language := {|
language.expr := expr; language.val := val; language.state := state;
language.of_val := of_val; language.to_val := to_val;
language.atomic := atomic; language.prim_step := prim_step;
language.to_of_val := to_of_val; language.of_to_val := of_to_val;
language.val_stuck := val_prim_stuck; language.atomic_not_val := atomic_not_val;
language.atomic_step := atomic_prim_step
|}.
(* Every evaluation context is a context. *)
Global Instance ectx_lang_ctx K : LanguageCtx ectx_lang (fill K).
Proof.
split.
- eauto using fill_not_val.
- intros ????? [K' e1' e2' Heq1 Heq2 Hstep].
by exists (comp_ectx K K') e1' e2'; rewrite ?Heq1 ?Heq2 ?fill_comp.
- intros e1 σ1 e2 σ2 ? Hnval [K'' e1'' e2'' Heq1 -> Hstep].
destruct (step_by_val K K'' e1 e1'' σ1 e2'' σ2 ef) as [K' ->]; eauto.
rewrite -fill_comp in Heq1; apply fill_inj in Heq1.
exists (fill K' e2''); rewrite -fill_comp; split; auto.
econstructor; eauto.
Qed.
End Language.
\ No newline at end of file
...@@ -5,13 +5,13 @@ Import uPred. ...@@ -5,13 +5,13 @@ Import uPred.
Section LangTests. Section LangTests.
Definition add : expr [] := (#21 + #21)%E. Definition add : expr [] := (#21 + #21)%E.
Goal σ, prim_step add σ (#42) σ None. Goal σ, prim_step heap_ectx_lang add σ (#42) σ None.
Proof. intros; do_step done. Qed. Proof. intros; do_step done. Qed.
Definition rec_app : expr [] := ((rec: "f" "x" := '"f" '"x") #0)%E. Definition rec_app : expr [] := ((rec: "f" "x" := '"f" '"x") #0)%E.
Goal σ, prim_step rec_app σ rec_app σ None. Goal σ, prim_step heap_ectx_lang rec_app σ rec_app σ None.
Proof. intros. rewrite /rec_app. do_step done. Qed. Proof. intros. rewrite /rec_app. do_step done. Qed.
Definition lam : expr [] := (λ: "x", '"x" + #21)%E. Definition lam : expr [] := (λ: "x", '"x" + #21)%E.
Goal σ, prim_step (lam #21)%E σ add σ None. Goal σ, prim_step heap_ectx_lang (lam #21)%E σ add σ None.
Proof. intros. rewrite /lam. do_step done. Qed. Proof. intros. rewrite /lam. do_step done. Qed.
End LangTests. End LangTests.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment