Commit 6b4d8596 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Support multiple steps in `PureExec`.

parent 18729ff5
...@@ -53,7 +53,8 @@ Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step. ...@@ -53,7 +53,8 @@ Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
Local Ltac solve_pure_exec := Local Ltac solve_pure_exec :=
unfold IntoVal in *; unfold IntoVal in *;
repeat match goal with H : AsVal _ |- _ => destruct H as [??] end; subst; repeat match goal with H : AsVal _ |- _ => destruct H as [??] end; subst;
apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ]. intros ?; apply nsteps_once, pure_head_step_pure_step;
constructor; [solve_exec_safe | solve_exec_puredet].
Class AsRec (e : expr) (f x : binder) (erec : expr) := Class AsRec (e : expr) (f x : binder) (erec : expr) :=
as_rec : e = Rec f x erec. as_rec : e = Rec f x erec.
...@@ -64,37 +65,37 @@ Proof. by unlock. Qed. ...@@ -64,37 +65,37 @@ Proof. by unlock. Qed.
Instance pure_rec f x (erec e1 e2 : expr) Instance pure_rec f x (erec e1 e2 : expr)
`{!AsVal e2, AsRec e1 f x erec, Closed (f :b: x :b: []) erec} : `{!AsVal e2, AsRec e1 f x erec, Closed (f :b: x :b: []) erec} :
PureExec True (App e1 e2) (subst' x e2 (subst' f e1 erec)). PureExec True 1 (App e1 e2) (subst' x e2 (subst' f e1 erec)).
Proof. unfold AsRec in *; solve_pure_exec. Qed. Proof. unfold AsRec in *; solve_pure_exec. Qed.
Instance pure_unop op e v v' `{!IntoVal e v} : Instance pure_unop op e v v' `{!IntoVal e v} :
PureExec (un_op_eval op v = Some v') (UnOp op e) (of_val v'). PureExec (un_op_eval op v = Some v') 1 (UnOp op e) (of_val v').
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Instance pure_binop op e1 e2 v1 v2 v' `{!IntoVal e1 v1, !IntoVal e2 v2} : Instance pure_binop op e1 e2 v1 v2 v' `{!IntoVal e1 v1, !IntoVal e2 v2} :
PureExec (bin_op_eval op v1 v2 = Some v') (BinOp op e1 e2) (of_val v'). PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op e1 e2) (of_val v').
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Instance pure_if_true e1 e2 : PureExec True (If (Lit (LitBool true)) e1 e2) e1. Instance pure_if_true e1 e2 : PureExec True 1 (If (Lit (LitBool true)) e1 e2) e1.
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Instance pure_if_false e1 e2 : PureExec True (If (Lit (LitBool false)) e1 e2) e2. Instance pure_if_false e1 e2 : PureExec True 1 (If (Lit (LitBool false)) e1 e2) e2.
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Instance pure_fst e1 e2 v1 `{!IntoVal e1 v1, !AsVal e2} : Instance pure_fst e1 e2 v1 `{!IntoVal e1 v1, !AsVal e2} :
PureExec True (Fst (Pair e1 e2)) e1. PureExec True 1 (Fst (Pair e1 e2)) e1.
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Instance pure_snd e1 e2 v2 `{!AsVal e1, !IntoVal e2 v2} : Instance pure_snd e1 e2 v2 `{!AsVal e1, !IntoVal e2 v2} :
PureExec True (Snd (Pair e1 e2)) e2. PureExec True 1 (Snd (Pair e1 e2)) e2.
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Instance pure_case_inl e0 v e1 e2 `{!IntoVal e0 v} : Instance pure_case_inl e0 v e1 e2 `{!IntoVal e0 v} :
PureExec True (Case (InjL e0) e1 e2) (App e1 e0). PureExec True 1 (Case (InjL e0) e1 e2) (App e1 e0).
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} : Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} :
PureExec True (Case (InjR e0) e1 e2) (App e2 e0). PureExec True 1 (Case (InjR e0) e1 e2) (App e2 e0).
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Section lifting. Section lifting.
......
...@@ -30,18 +30,18 @@ Tactic Notation "wp_expr_eval" tactic(t) := ...@@ -30,18 +30,18 @@ Tactic Notation "wp_expr_eval" tactic(t) :=
Ltac wp_expr_simpl := wp_expr_eval simpl. Ltac wp_expr_simpl := wp_expr_eval simpl.
Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst. Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ Φ : Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ n Φ :
PureExec φ e1 e2 PureExec φ n e1 e2
φ φ
MaybeIntoLaterNEnvs 1 Δ Δ' MaybeIntoLaterNEnvs n Δ Δ'
envs_entails Δ' (WP e2 @ s; E {{ Φ }}) envs_entails Δ' (WP e2 @ s; E {{ Φ }})
envs_entails Δ (WP e1 @ s; E {{ Φ }}). envs_entails Δ (WP e1 @ s; E {{ Φ }}).
Proof. Proof.
rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=. rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
rewrite HΔ' -lifting.wp_pure_step_later //. rewrite HΔ' -lifting.wp_pure_step_later //.
Qed. Qed.
Lemma tac_twp_pure `{heapG Σ} Δ s E e1 e2 φ Φ : Lemma tac_twp_pure `{heapG Σ} Δ s E e1 e2 φ n Φ :
PureExec φ e1 e2 PureExec φ n e1 e2
φ φ
envs_entails Δ (WP e2 @ s; E [{ Φ }]) envs_entails Δ (WP e2 @ s; E [{ Φ }])
envs_entails Δ (WP e1 @ s; E [{ Φ }]). envs_entails Δ (WP e1 @ s; E [{ Φ }]).
......
...@@ -206,23 +206,24 @@ Section ectx_language. ...@@ -206,23 +206,24 @@ Section ectx_language.
econstructor; eauto. econstructor; eauto.
Qed. Qed.
Lemma det_head_step_pure_exec (P : Prop) e1 e2 : Record pure_head_step (e1 e2 : expr Λ) := {
( σ, P head_reducible e1 σ) pure_head_step_safe σ1 : head_reducible e1 σ1;
( σ1 e2' σ2 efs, pure_head_step_det σ1 e2' σ2 efs :
P head_step e1 σ1 e2' σ2 efs σ1 = σ2 e2=e2' efs = []) head_step e1 σ1 e2' σ2 efs σ1 = σ2 e2 = e2' efs = []
PureExec P e1 e2. }.
Lemma pure_head_step_pure_step e1 e2 : pure_head_step e1 e2 pure_step e1 e2.
Proof. Proof.
intros Hp1 Hp2. split. intros [Hp1 Hp2]. split.
- intros σ ?. destruct (Hp1 σ) as (e2' & σ2 & efs & ?); first done. - intros σ. destruct (Hp1 σ) as (e2' & σ2 & efs & ?).
eexists e2', σ2, efs. by apply head_prim_step. eexists e2', σ2, efs. by apply head_prim_step.
- intros σ1 e2' σ2 efs ? ?%head_reducible_prim_step; eauto. - intros σ1 e2' σ2 efs ?%head_reducible_prim_step; eauto.
Qed. Qed.
Global Instance pure_exec_fill K e1 e2 φ : Global Instance pure_exec_fill K φ n e1 e2 :
PureExec φ e1 e2 PureExec φ n e1 e2
PureExec φ (fill K e1) (fill K e2). PureExec φ n (fill K e1) (fill K e2).
Proof. apply: pure_exec_ctx. Qed. Proof. apply: pure_exec_ctx. Qed.
End ectx_language. End ectx_language.
Arguments ectx_lang : clear implicits. Arguments ectx_lang : clear implicits.
......
...@@ -133,31 +133,40 @@ Section language. ...@@ -133,31 +133,40 @@ Section language.
by rewrite -!Permutation_middle !assoc_L Ht. by rewrite -!Permutation_middle !assoc_L Ht.
Qed. Qed.
Class PureExec (P : Prop) (e1 e2 : expr Λ) := { Record pure_step (e1 e2 : expr Λ) := {
pure_exec_safe σ : pure_step_safe σ1 : reducible e1 σ1;
P reducible e1 σ; pure_step_det σ1 e2' σ2 efs :
pure_exec_puredet σ1 e2' σ2 efs : prim_step e1 σ1 e2' σ2 efs σ1 = σ2 e2 = e2' efs = []
P prim_step e1 σ1 e2' σ2 efs σ1 = σ2 e2 = e2' efs = [];
}. }.
Lemma hoist_pred_pure_exec (P : Prop) (e1 e2 : expr Λ) : (* TODO: Exclude the case of [n=0], either here, or in [wp_pure] to avoid it
(P PureExec True e1 e2) succeeding when it did not actually do anything. *)
PureExec P e1 e2. Class PureExec (φ : Prop) (n : nat) (e1 e2 : expr Λ) :=
Proof. intros HPE. split; intros; eapply HPE; eauto. Qed. pure_exec : φ nsteps pure_step n e1 e2.
(* We do not make this an instance because it is awfully general. *) Lemma pure_step_ctx K `{LanguageCtx Λ K} e1 e2 :
Lemma pure_exec_ctx K `{LanguageCtx Λ K} e1 e2 φ : pure_step e1 e2
PureExec φ e1 e2 pure_step (K e1) (K e2).
PureExec φ (K e1) (K e2).
Proof. Proof.
intros [Hred Hstep]. split. intros [Hred Hstep]. split.
- unfold reducible in *. naive_solver eauto using fill_step. - unfold reducible in *. naive_solver eauto using fill_step.
- intros σ1 e2' σ2 efs ? Hpstep. - intros σ1 e2' σ2 efs Hpstep.
destruct (fill_step_inv e1 σ1 e2' σ2 efs) as (e2'' & -> & ?); [|exact Hpstep|]. destruct (fill_step_inv e1 σ1 e2' σ2 efs) as (e2'' & -> & ?); [|exact Hpstep|].
+ destruct (Hred σ1) as (? & ? & ? & ?); eauto using val_stuck. + destruct (Hred σ1) as (? & ? & ? & ?); eauto using val_stuck.
+ edestruct (Hstep σ1 e2'' σ2 efs) as (-> & -> & ->); auto. + destruct (Hstep σ1 e2'' σ2 efs) as (-> & -> & ->); auto.
Qed. Qed.
Lemma pure_step_nsteps_ctx K `{LanguageCtx Λ K} n e1 e2 :
nsteps pure_step n e1 e2
nsteps pure_step n (K e1) (K e2).
Proof. induction 1; econstructor; eauto using pure_step_ctx. Qed.
(* We do not make this an instance because it is awfully general. *)
Lemma pure_exec_ctx K `{LanguageCtx Λ K} φ n e1 e2 :
PureExec φ n e1 e2
PureExec φ n (K e1) (K e2).
Proof. rewrite /PureExec; eauto using pure_step_nsteps_ctx. Qed.
(* This is a family of frequent assumptions for PureExec *) (* This is a family of frequent assumptions for PureExec *)
Class IntoVal (e : expr Λ) (v : val Λ) := Class IntoVal (e : expr Λ) (v : val Λ) :=
into_val : of_val v = e. into_val : of_val v = e.
......
...@@ -123,23 +123,25 @@ Proof. ...@@ -123,23 +123,25 @@ Proof.
by iIntros (e' efs' σ (_&->&->)%Hpuredet). by iIntros (e' efs' σ (_&->&->)%Hpuredet).
Qed. Qed.
Lemma wp_pure_step_fupd `{Inhabited (state Λ)} s E E' e1 e2 φ Φ : Lemma wp_pure_step_fupd `{Inhabited (state Λ)} s E E' e1 e2 φ n Φ :
PureExec φ e1 e2 PureExec φ n e1 e2
φ φ
(|={E,E'}=> WP e2 @ s; E {{ Φ }}) WP e1 @ s; E {{ Φ }}. Nat.iter n (λ P, |={E,E'}=> P) (WP e2 @ s; E {{ Φ }}) WP e1 @ s; E {{ Φ }}.
Proof. Proof.
iIntros ([??] Hφ) "HWP". iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ).
iApply (wp_lift_pure_det_step with "[HWP]"). iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done.
- intros σ. specialize (pure_exec_safe σ). destruct s; eauto using reducible_not_val. iApply wp_lift_pure_det_step.
- intros σ. specialize (Hsafe σ). destruct s; eauto using reducible_not_val.
- destruct s; naive_solver. - destruct s; naive_solver.
- by rewrite big_sepL_nil right_id. - rewrite /= right_id. by iApply (step_fupd_wand with "Hwp").
Qed. Qed.
Lemma wp_pure_step_later `{Inhabited (state Λ)} s E e1 e2 φ Φ : Lemma wp_pure_step_later `{Inhabited (state Λ)} s E e1 e2 φ n Φ :
PureExec φ e1 e2 PureExec φ n e1 e2
φ φ
WP e2 @ s; E {{ Φ }} WP e1 @ s; E {{ Φ }}. ^n WP e2 @ s; E {{ Φ }} WP e1 @ s; E {{ Φ }}.
Proof. Proof.
intros ??. rewrite -wp_pure_step_fupd //. rewrite -step_fupd_intro //. intros Hexec ?. rewrite -wp_pure_step_fupd //. clear Hexec.
induction n as [|n IH]; by rewrite //= -step_fupd_intro // IH.
Qed. Qed.
End lifting. End lifting.
...@@ -68,12 +68,14 @@ Proof. ...@@ -68,12 +68,14 @@ Proof.
by iIntros "!>" (e' efs' σ (_&->&->)%Hpuredet). by iIntros "!>" (e' efs' σ (_&->&->)%Hpuredet).
Qed. Qed.
Lemma twp_pure_step `{Inhabited (state Λ)} s E e1 e2 φ Φ : Lemma twp_pure_step `{Inhabited (state Λ)} s E e1 e2 φ n Φ :
PureExec φ e1 e2 PureExec φ n e1 e2
φ φ
WP e2 @ s; E [{ Φ }] WP e1 @ s; E [{ Φ }]. WP e2 @ s; E [{ Φ }] WP e1 @ s; E [{ Φ }].
Proof. Proof.
iIntros ([??] Hφ) "HWP". iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ).
iApply (twp_lift_pure_det_step with "[HWP]"); [eauto|naive_solver|auto]. iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done.
iApply twp_lift_pure_det_step; [done|naive_solver|].
iModIntro. rewrite /= right_id. by iApply "IH".
Qed. Qed.
End lifting. End lifting.
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