Commit d1be2253 authored by Dan Frumin's avatar Dan Frumin

Use `PureExec` for pure symbolic execution rules

parent 8ec7cd1e
......@@ -128,14 +128,8 @@ Proof.
intros Hfill Hpure Hϕ Hb ? Hp. subst.
destruct b.
- destruct Hb as [[_ ?] | Hb']; last by inversion Hb'. subst.
rewrite -(bin_log_pure_l Δ Γ E2 K e1 e2 t τ).
{ exact Hp. }
{ intros. apply pure_exec_safe. exact Hϕ. }
{ intros. apply pure_exec_puredet; eauto. }
- rewrite -(bin_log_pure_masked_l Δ Γ E1 E2 K e1 e2 t τ).
{ exact Hp. }
{ intros. apply pure_exec_safe. exact Hϕ. }
{ intros. apply pure_exec_puredet; eauto. }
by rewrite -(bin_log_pure_l Δ Γ E2 K e1 e2 t τ _ _ Hϕ).
- by rewrite -(bin_log_pure_masked_l Δ Γ E1 E2 K e1 e2 t τ _ _ Hϕ).
Qed.
Tactic Notation "rel_pure_l" open_constr(ef) :=
......@@ -179,14 +173,7 @@ Lemma tac_rel_pure_r `{logrelG Σ} K e1 ℶ E1 E2 Δ Γ e e2 eres ϕ t τ :
envs_entails (bin_log_related E1 E2 Δ Γ t e τ).
Proof.
intros Hfill Hpure Hϕ ?? Hp. subst.
rewrite -(bin_log_pure_r Δ Γ E1 E2 K e1 e2 t τ).
{ exact Hp. }
{ assumption. }
{ intros σ.
destruct Hpure as [Hsafe Hstep].
destruct (Hsafe σ Hϕ) as [e2' [σ2' [? Hstep']]].
destruct (Hstep _ _ _ _ Hϕ Hstep') as (? & ? & ?); subst.
done. }
by rewrite -(bin_log_pure_r Δ Γ E1 E2 K e1 e2 t τ).
Qed.
Tactic Notation "rel_pure_r" open_constr(ef) :=
......
......@@ -30,7 +30,7 @@ Proof.
Qed.
Ltac tp_bind_helper :=
rewrite ?fill_app /=;
rewrite /=;
lazymatch goal with
| |- fill ?K ?e = fill _ ?efoc =>
reshape_expr e ltac:(fun K' e' =>
......@@ -184,12 +184,7 @@ Proof.
rewrite Hfill.
rewrite comm.
rewrite (assoc _ (spec_ctx ρ) (j _)%I).
rewrite step_pure //; last first.
{ intros σ.
destruct Hpure as [Hsafe Hstep].
destruct (Hsafe σ Hϕ) as [e2' [σ2' [? Hstep']]].
destruct (Hstep _ _ _ _ Hϕ Hstep') as (? & ? & ?); subst.
done. }
rewrite step_pure //.
rewrite -[Q]elim_modal.
apply uPred.sep_mono_r.
apply uPred.wand_intro_l.
......
......@@ -102,69 +102,68 @@ Section properties.
(** ** Forward reductions on the LHS *)
(* TODO: should this be an instance? *)
Lemma pureexec_subst_p ϕ e e' es :
PureExec ϕ e e'
PureExec ϕ (subst_p es e) (subst_p es e').
Proof.
intros Hpure.
apply hoist_pred_pure_exec. intros Hϕ.
assert (Hsafe : σ, reducible (subst_p es e) σ).
{ intros; apply subst_p_safe; eauto using pure_exec_safe. }
assert (to_val (subst_p es e) = None) as Hval.
{ destruct (Hsafe ) as [e2 [σ2 [efs Hs]]].
by eapply language.val_stuck. }
split; eauto. intros.
cut (σ1 = σ2 subst_p es e' = e2' [] = efs); first by naive_solver.
eapply subst_p_det; eauto.
- intros σ. destruct (pure_exec_safe σ Hϕ) as (? & ? & ? & Hsafez).
destruct (pure_exec_puredet _ _ _ _ Hϕ Hsafez) as (?&?&?).
simplify_eq. apply Hsafez.
- intros ???? Hs.
destruct (pure_exec_puredet _ _ _ _ Hϕ Hs) as (?&?&?).
by simplify_eq.
Qed.
Lemma bin_log_pure_l Δ (Γ : stringmap type) (E : coPset)
(K' : list ectx_item) (e e' t : expr) (τ : type)
(Hsafe' : σ, reducible e σ)
(Hdet' : σ1 e2 σ2 efs, prim_step e σ1 e2 σ2 efs -> σ1=σ2 /\ e'=e2 /\ efs = []) :
(K' : list ectx_item) (e e' t : expr) (τ : type) ϕ :
PureExec ϕ e e'
ϕ
({E;Δ;Γ} fill K' e' log t : τ)
{E;Δ;Γ} fill K' e log t : τ.
Proof.
intros Hpure Hϕ.
rewrite bin_log_related_eq.
iIntros "IH".
iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
iIntros "IH" (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
rewrite /env_subst.
rewrite fill_subst. iModIntro.
assert (Hsafe : σ, reducible (subst_p (fst <$> vvs) e) σ).
{ intros; apply subst_p_safe; eauto. }
assert (to_val (subst_p (fst <$> vvs) e) = None) as Hval.
{ destruct (Hsafe ) as [e2 [σ2 [efs Hs]]].
by eapply language.val_stuck. }
iApply (wp_bind (subst_ctx (fst <$> vvs) K')).
iApply wp_lift_pure_det_step; eauto.
{ apply subst_p_det; eauto.
- intros σ. destruct (Hsafe' σ) as (e2' & σ2' & efs & Hsafez).
destruct (Hdet' _ _ _ _ Hsafez) as (?&?&?).
simplify_eq. apply Hsafez.
- intros ? ? ? ? Hs.
destruct (Hdet' _ _ _ _ Hs) as (?&?&?).
by simplify_eq. }
iModIntro. iNext. iModIntro. simpl; iSplitL; last done.
iSpecialize ("IH" with "Hs [HΓ] Hj"); auto. simpl.
iApply wp_pure_step_later; [ | apply Hϕ | ].
{ apply pure_exec_ctx; first apply _.
apply pureexec_subst_p. eassumption. }
iNext. iApply fupd_wp.
iSpecialize ("IH" with "Hs [HΓ] Hj"); first done.
rewrite /env_subst fill_subst.
iApply wp_bind_inv.
iApply fupd_wp. by iApply (fupd_mask_mono E).
by iApply (fupd_mask_mono E).
Qed.
Lemma bin_log_pure_masked_l (Δ : list D) (Γ : stringmap type) (E1 E2 : coPset)
(K' : list ectx_item) (e e' t : expr) (τ : type)
(Hsafe' : σ, reducible e σ)
(Hdet': σ1 e2 σ2 efs, prim_step e σ1 e2 σ2 efs -> σ1=σ2 /\ e'=e2 /\ efs = []) :
(K' : list ectx_item) (e e' t : expr) (τ : type) ϕ :
PureExec ϕ e e'
ϕ
{E1,E2;Δ;Γ} fill K' e' log t : τ
{E1,E2;Δ;Γ} fill K' e log t : τ.
Proof.
intros Hpure Hϕ.
rewrite bin_log_related_eq.
iIntros "IH".
iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
rewrite /env_subst fill_subst.
assert (Hsafe : σ, reducible (subst_p (fst <$> vvs) e) σ).
{ intros. by eapply subst_p_safe. }
assert (to_val (subst_p (fst <$> vvs) e) = None) as Hval.
{ destruct (Hsafe ) as [e2 [σ2 [efs Hs]]].
by eapply language.val_stuck. }
iApply (wp_bind (subst_ctx _ K')).
iApply wp_pure_step_later; [ | apply Hϕ | ].
{ apply pure_exec_ctx; first apply _.
apply pureexec_subst_p. eassumption. }
iMod ("IH" with "Hs [HΓ] Hj") as "IH"; auto.
iModIntro.
iApply wp_lift_pure_det_step; eauto.
{ apply subst_p_det; eauto.
- intros σ. destruct (Hsafe' σ) as (e2' & σ2' & efs & Hsafez).
destruct (Hdet' _ _ _ _ Hsafez) as (?&?&?).
simplify_eq. apply Hsafez.
- intros ? ? ? ? Hs.
destruct (Hdet' _ _ _ _ Hs) as (?&?&?).
by simplify_eq. }
iModIntro. iNext. iModIntro. iSplitL; last done.
rewrite /env_subst fill_subst /=.
by iApply wp_bind_inv.
iModIntro. iNext. simpl.
rewrite /env_subst fill_subst /= //.
Qed.
Lemma bin_log_related_wp_l Δ Γ E K e1 e2 τ
......@@ -215,21 +214,20 @@ Section properties.
(** ** Forward reductions on the RHS *)
Lemma bin_log_pure_r Δ Γ E1 E2 K' e e' t τ
(Hspec : nclose specN E1) :
( σ, prim_step e σ e' σ [])
(Hspec : nclose specN E1) ϕ :
PureExec ϕ e e'
ϕ
{E1,E2;Δ;Γ} t log fill K' e' : τ
{E1,E2;Δ;Γ} t log fill K' e : τ.
Proof.
rewrite bin_log_related_eq /bin_log_related_def.
iIntros (Hstep) "Hlog".
iIntros (Hpure Hϕ) "Hlog".
iIntros (vvs ρ) "#Hs #HΓ".
iIntros (j K) "Hj /=".
assert (Hsafe : σ, prim_step (subst_p (snd <$> vvs) e) σ (subst_p (snd <$> vvs) e') σ []).
{ intros.
rewrite -(fmap_nil (subst_p (snd <$> vvs))).
by apply subst_p_prim_step. }
rewrite /env_subst fill_subst -fill_app.
iMod (step_pure _ _ _ _ (subst_p _ e) (env_subst (snd <$> vvs) e') with "[Hs Hj]") as "Hj"; eauto.
assert (PureExec ϕ (subst_p (snd <$> vvs) e) (subst_p (snd <$> vvs) e')).
{ apply pureexec_subst_p. eassumption. }
tp_pure j; auto.
rewrite fill_app -fill_subst.
iDestruct ("Hlog" with "Hs [HΓ] Hj") as "Hlog"; auto.
Qed.
......@@ -406,106 +404,62 @@ Section properties.
(** ** (Pure) reductions on the left *)
(* TODO: I have to 'refine' here for some reason *)
Local Ltac solve_red H :=
iApply (bin_log_pure_l with H); auto;
[ intros; apply pure_exec_safe
| intros ???? Hst;
refine (@pure_exec_puredet F_mu_ref_conc_lang _ _ _ _ _ _ _ _ _ Hst)
]; eauto.
Local Ltac solve_red_masked H :=
iApply (bin_log_pure_masked_l with H); auto;
[ intros; apply pure_exec_safe
| intros ???? Hst;
refine (@pure_exec_puredet F_mu_ref_conc_lang _ _ _ _ _ _ _ _ _ Hst)
]; eauto.
Lemma bin_log_related_rec_l Δ Γ E K (f x : binder) e e' v t τ
(Hclosed : Closed (x :b: f :b: ) e) :
(to_val e' = Some v)
({E;Δ;Γ} (fill K (subst' f (Rec f x e) (subst' x e' e))) log t : τ)
{E;Δ;Γ} (fill K (App (Rec f x e) e')) log t : τ.
Proof.
iIntros (?) "Hlog".
solve_red "Hlog".
Qed.
Proof. iIntros. by iApply bin_log_pure_l. Qed.
Lemma bin_log_related_fst_l Δ Γ E K v1 v2 e τ :
({E;Δ;Γ} fill K (of_val v1) log e : τ)
{E;Δ;Γ} fill K (Fst (Pair (of_val v1) (of_val v2))) log e : τ.
Proof.
iIntros "Hlog".
solve_red "Hlog".
Qed.
Proof. iIntros. by iApply bin_log_pure_l. Qed.
Lemma bin_log_related_snd_l Δ Γ E K v1 v2 e τ :
({E;Δ;Γ} (fill K (of_val v2)) log e : τ)
{E;Δ;Γ} (fill K (Snd (Pair (of_val v1) (of_val v2)))) log e : τ.
Proof.
iIntros "Hlog".
solve_red "Hlog".
Qed.
Proof. iIntros. by iApply bin_log_pure_l. Qed.
Lemma bin_log_related_tlam_l Δ Γ E K e t τ
(Hclosed : Closed e) :
({E;Δ;Γ} fill K e log t : τ)
{E;Δ;Γ} (fill K (TApp (TLam e))) log t : τ.
Proof.
iIntros "Hlog".
solve_red "Hlog".
Qed.
Proof. iIntros. by iApply bin_log_pure_l. Qed.
Lemma bin_log_related_fold_l Δ Γ E K e v t τ :
(to_val e = Some v)
({E;Δ;Γ} fill K e log t : τ)
{E;Δ;Γ} (fill K (Unfold (Fold e))) log t : τ.
Proof.
iIntros (?) "Hlog".
solve_red "Hlog".
Qed.
Proof. iIntros. by iApply bin_log_pure_l. Qed.
Lemma bin_log_related_pack_l Δ Γ E K e e' v t τ :
to_val e = Some v
({E;Δ;Γ} fill K (App e' e) log t : τ)
{E;Δ;Γ} fill K (Unpack (Pack e) e') log t : τ.
Proof.
iIntros (?) "Hlog".
solve_red "Hlog".
Qed.
Proof. iIntros. by iApply bin_log_pure_l. Qed.
Lemma bin_log_related_case_inl_l Δ Γ E K e v e1 e2 t τ :
to_val e = Some v
({E;Δ;Γ} fill K (App e1 e) log t : τ)
{E;Δ;Γ} fill K (Case (InjL e) e1 e2) log t : τ.
Proof.
iIntros (?) "Hlog".
solve_red "Hlog".
Qed.
Proof. iIntros. by iApply bin_log_pure_l. Qed.
Lemma bin_log_related_case_inr_l Δ Γ E K e v e1 e2 t τ :
to_val e = Some v
({E;Δ;Γ} fill K (App e2 e) log t : τ)
{E;Δ;Γ} fill K (Case (InjR e) e1 e2) log t : τ.
Proof.
iIntros (?) "Hlog".
solve_red "Hlog".
Qed.
Proof. iIntros. by iApply bin_log_pure_l. Qed.
Lemma bin_log_related_if_true_l Δ Γ E K e1 e2 t τ :
({E;Δ;Γ} fill K e1 log t : τ)
{E;Δ;Γ} fill K (If #true e1 e2) log t : τ.
Proof.
iIntros "Hlog".
solve_red "Hlog".
Qed.
Proof. iIntros. by iApply bin_log_pure_l. Qed.
Lemma bin_log_related_if_false_l Δ Γ E K e1 e2 t τ :
({E;Δ;Γ} fill K e2 log t : τ)
{E;Δ;Γ} (fill K (If #false e1 e2)) log t : τ.
Proof.
iIntros "Hlog".
solve_red "Hlog".
Qed.
Proof. iIntros. by iApply bin_log_pure_l. Qed.
Lemma bin_log_related_binop_l Δ Γ E K op e1 e2 v1 v2 v t τ :
to_val e1 = Some v1
......@@ -513,76 +467,43 @@ Section properties.
binop_eval op v1 v2 = Some v
({E;Δ;Γ} fill K (of_val v) log t : τ)
{E;Δ;Γ} (fill K (BinOp op e1 e2)) log t : τ.
Proof.
iIntros (???) "Hlog".
solve_red "Hlog".
Qed.
Proof. iIntros. by iApply bin_log_pure_l. Qed.
(** ** (Pure) reductions on the RHS. *)
Lemma bin_log_pure_head_step_r Δ Γ E1 E2 K' e e' t τ
(Hspec : nclose specN E1) :
( σ, head_step e σ e' σ [])
{E1,E2;Δ;Γ} t log fill K' e' : τ
{E1,E2;Δ;Γ} t log fill K' e : τ.
Proof.
intros Hst. apply bin_log_pure_r; eauto.
intros. apply head_prim_step. apply Hst.
Qed.
Lemma bin_log_related_rec_r Δ Γ E1 E2 K f x e e' t v' τ
(Hspec : nclose specN E1)
(Hclosed : Closed (x :b: f :b: ) e) :
(to_val e' = Some v')
{E1,E2;Δ;Γ} t log fill K (subst' f (Rec f x e) (subst' x e' e)) : τ
{E1,E2;Δ;Γ} t log fill K (App (Rec f x e) e') : τ.
Proof.
iIntros (?) "Hlog".
iApply (bin_log_pure_head_step_r with "Hlog"); auto; intros.
econstructor; eauto.
Qed.
Proof. iIntros. iApply bin_log_pure_r; eauto. Qed.
Lemma bin_log_related_fst_r Δ Γ E1 E2 K e v1 v2 τ
(Hspec : nclose specN E1) :
{E1,E2;Δ;Γ} e log (fill K (of_val v1)) : τ
{E1,E2;Δ;Γ} e log (fill K (Fst (Pair (of_val v1) (of_val v2)))) : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_head_step_r with "Hlog"); auto; intros.
{ econstructor; eauto. }
Qed.
Proof. iIntros. iApply bin_log_pure_r; eauto. Qed.
Lemma bin_log_related_snd_r Δ Γ E1 E2 K e v1 v2 τ
(Hspec : nclose specN E1) :
{E1,E2;Δ;Γ} e log (fill K (of_val v2)) : τ
{E1,E2;Δ;Γ} e log (fill K (Snd (Pair (of_val v1) (of_val v2)))) : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_head_step_r with "Hlog"); auto; intros.
{ econstructor; eauto. }
Qed.
Proof. iIntros. iApply bin_log_pure_r; eauto. Qed.
Lemma bin_log_related_tlam_r Δ Γ E1 E2 K e t τ
(Hclosed : Closed e)
(Hspec : nclose specN E1) :
{E1,E2;Δ;Γ} t log fill K e : τ
{E1,E2;Δ;Γ} t log fill K (TApp (TLam e)) : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_head_step_r with "Hlog"); auto; intros.
{ econstructor; eauto. }
Qed.
Proof. iIntros. iApply bin_log_pure_r; eauto. Qed.
Lemma bin_log_related_fold_r Δ Γ E1 E2 K e v t τ
(Hval : to_val e = Some v)
(Hspec : nclose specN E1) :
{E1,E2;Δ;Γ} t log fill K e : τ
{E1,E2;Δ;Γ} t log fill K (Unfold (Fold e)) : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_head_step_r with "Hlog"); auto; intros.
{ econstructor; eauto. }
Qed.
Proof. iIntros. iApply bin_log_pure_r; eauto. Qed.
Lemma bin_log_related_pack_r Δ Γ E1 E2 K e e' v t τ
(Hclosed : Closed e')
......@@ -590,11 +511,7 @@ Section properties.
(Hspec : nclose specN E1) :
{E1,E2;Δ;Γ} t log fill K (App e' e) : τ
{E1,E2;Δ;Γ} t log fill K (Unpack (Pack e) e') : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_head_step_r with "Hlog"); auto; intros.
{ econstructor; eauto. }
Qed.
Proof. iIntros. iApply bin_log_pure_r; eauto. Qed.
Lemma bin_log_related_case_inl_r Δ Γ E1 E2 K e v e1 e2 t τ
(Hclosed1 : Closed e1)
......@@ -603,11 +520,7 @@ Section properties.
(Hspec : nclose specN E1) :
{E1,E2;Δ;Γ} t log (fill K (App e1 e)) : τ
{E1,E2;Δ;Γ} t log (fill K (Case (InjL e) e1 e2)) : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_head_step_r with "Hlog"); auto; intros.
{ econstructor; eauto. }
Qed.
Proof. iIntros. iApply bin_log_pure_r; eauto. Qed.
Lemma bin_log_related_case_inr_r Δ Γ E1 E2 K e v e1 e2 t τ
(Hclosed1 : Closed e1)
......@@ -616,11 +529,7 @@ Section properties.
(Hspec : nclose specN E1) :
{E1,E2;Δ;Γ} t log (fill K (App e2 e)) : τ
{E1,E2;Δ;Γ} t log (fill K (Case (InjR e) e1 e2)) : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_head_step_r with "Hlog"); auto; intros.
{ econstructor; eauto. }
Qed.
Proof. iIntros. iApply bin_log_pure_r; eauto. Qed.
Lemma bin_log_related_if_true_r Δ Γ E1 E2 K e e1 e2 τ
(Hspec : nclose specN E1)
......@@ -628,11 +537,7 @@ Section properties.
(Hclosed2 : Closed e2) :
{E1,E2;Δ;Γ} e log (fill K e1) : τ
{E1,E2;Δ;Γ} e log (fill K (If #true e1 e2)) : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_head_step_r with "Hlog"); auto; intros.
{ econstructor; eauto. }
Qed.
Proof. iIntros. iApply bin_log_pure_r; eauto. Qed.
Lemma bin_log_related_if_false_r Δ Γ E1 E2 K e e1 e2 τ
(Hspec : nclose specN E1)
......@@ -640,11 +545,7 @@ Section properties.
(Hclosed2 : Closed e2) :
{E1,E2;Δ;Γ} e log (fill K e2) : τ
{E1,E2;Δ;Γ} e log (fill K (If #false e1 e2)) : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_head_step_r with "Hlog"); auto; intros.
{ econstructor; eauto. }
Qed.
Proof. iIntros. iApply bin_log_pure_r; eauto. Qed.
Lemma bin_log_related_binop_r Δ Γ E1 E2 K op e1 e2 v1 v2 v t τ
(Hspec : nclose specN E1) :
......@@ -653,11 +554,7 @@ Section properties.
binop_eval op v1 v2 = Some v
{E1,E2;Δ;Γ} t log fill K (of_val v) : τ
{E1,E2;Δ;Γ} t log (fill K (BinOp op e1 e2)) : τ.
Proof.
iIntros (???) "Hlog".
iApply (bin_log_pure_head_step_r with "Hlog"); auto; intros.
{ econstructor; eauto. }
Qed.
Proof. iIntros. iApply bin_log_pure_r; eauto. Qed.
(** ** Stateful reductions on the LHS *)
......
......@@ -52,7 +52,7 @@ Section rules.
by apply head_prim_step.
Qed.
Lemma step_pure E ρ j K e e' :
Lemma step_pure_old E ρ j K e e' :
( σ, prim_step e σ e' σ [])
nclose specN E
spec_ctx ρ j fill K e ={E}= j fill K e'.
......@@ -69,6 +69,21 @@ Section rules.
iFrame. iPureIntro. eapply rtc_r, step_insert_no_fork_prim; eauto.
Qed.
Lemma step_pure E ρ j K e e' ϕ :
PureExec ϕ e e'
nclose specN E
ϕ
spec_ctx ρ j fill K e ={E}= j fill K e'.
Proof.
intros Hpure Hcl Hϕ.
rewrite step_pure_old //; last first.
intros σ.
destruct Hpure as [Hsafe Hstep].
destruct (Hsafe σ Hϕ) as [e2' [σ2' [? Hstep']]].
destruct (Hstep _ _ _ _ Hϕ Hstep') as (? & ? & ?); subst.
done.
Qed.
Lemma step_alloc E ρ j K e v:
to_val e = Some v nclose specN E
spec_ctx ρ j fill K (ref e) ={E}= l, j fill K #l l ↦ₛ v.
......
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