Commit f88e1b37 authored by Dan Frumin's avatar Dan Frumin

Use a single tp_pure tactic that depends on the PureExec typeclass

+ add some discussion in comments.org
parent 3f2ae145
......@@ -141,7 +141,7 @@ Section proof.
unfold with_lock. unlock.
tp_rec j.
tp_rec j.
tp_rec j; eauto using to_of_val.
tp_rec j.
tp_bind j (App acquire (Loc l)).
tp_apply j steps_acquire with "Hl" as "Hl".
tp_rec j.
......
......@@ -146,7 +146,7 @@ Section masked.
iDestruct (interp_env_dom with "HΓ") as %Hdom.
(* TODO: how to get rid of/ simplify those proofs? *)
assert (Closed (x :b: f :b: )
(env_subst (delete f (delete x (fst <$> vvs))) e)).
(subst_p (delete f (delete x (fst <$> vvs))) e)).
{ eapply subst_p_closes; eauto.
rewrite ?dom_delete_binder Hdom.
rewrite dom_fmap.
......@@ -160,13 +160,12 @@ Section masked.
set_solver.
+ rewrite ?(right_id union).
rewrite (comm union {[x]} {[f]}) !assoc.
rewrite difference_union_id.
rewrite difference_union_id.
rewrite -!assoc (comm union {[f]} {[x]}) !assoc.
rewrite difference_union_id.
set_solver.
}
rewrite difference_union_id.
set_solver. }
assert (Closed (x :b: f :b: )
(env_subst (delete f (delete x (snd <$> vvs))) e')).
(subst_p (delete f (delete x (snd <$> vvs))) e')).
{ eapply subst_p_closes; eauto.
rewrite ?dom_delete_binder Hdom.
rewrite dom_fmap.
......@@ -185,13 +184,14 @@ Section masked.
rewrite difference_union_id.
set_solver.
}
iModIntro. value_case; eauto. rewrite decide_left; eauto.
iModIntro. value_case; eauto.
{ rewrite decide_left; eauto. }
iExists (RecV f x (subst_p (delete f (delete x (snd <$> vvs))) e')). iIntros "{$Hj} !#".
iLöb as "IH". iIntros ([v v']) "#Hiv". simpl. iIntros (j' K') "Hj".
iModIntro. simpl.
iApply (wp_rec _ f x (subst_p _ e)); eauto 2 using to_of_val. iNext.
iApply fupd_wp.
tp_rec j'; auto.
tp_rec j'.
pose (vvs':=(<[x:=(v,v')]>(<[f:=(RecV f x (subst_p (delete f (delete x (fst <$> vvs))) e), RecV f x (subst_p (delete f (delete x (snd <$> vvs))) e'))]>vvs))).
iAssert (interp_env (<[x:=τ1]> (<[f:=TArrow τ1 τ2]> Γ)) Δ vvs') as "#HΓ'".
{ unfold vvs'. destruct f as [|f], x as [|x]; cbn; eauto;
......@@ -249,24 +249,25 @@ Section masked.
iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
smart_bind j (env_subst _ e0) (env_subst _ e0') "IH1" v v' "IH1".
iDestruct "IH1" as "[Hiv|Hiv]";
iDestruct "Hiv" as ([w w']) "[% #Hw]"; simplify_eq; iApply fupd_wp.
- tp_case_inl j; eauto.
iApply wp_case_inl; eauto using to_of_val. fold of_val.
iDestruct "Hiv" as ([w w']) "[% #Hw]"; simplify_eq;
tp_case j.
- iApply wp_case_inl; eauto using to_of_val. fold of_val.
iNext.
iSpecialize ("IH2" with "Hs [HΓ]"); auto.
tp_bind j (env_subst (snd <$> vvs) e1').
iApply (fupd_mask_mono _); eauto.
iMod ("IH2" with "Hj") as "IH2". iModIntro. iNext. simpl.
iApply fupd_wp. iApply (fupd_mask_mono _); eauto.
iMod ("IH2" with "Hj") as "IH2". iModIntro.
wp_bind (env_subst (fst <$> vvs) e1).
iApply (wp_wand with "IH2").
iIntros (v). iDestruct 1 as (v') "[Hj #Ht]".
iSpecialize ("Ht" $! (w, w') with "Hw Hj"). cbn.
by iApply fupd_wp.
- tp_case_inr j; eauto.
iApply wp_case_inr; eauto using to_of_val. fold of_val.
- iApply wp_case_inr; eauto using to_of_val. fold of_val.
iNext.
iSpecialize ("IH3" with "Hs [HΓ]"); auto.
tp_bind j (env_subst (snd <$> vvs) e2').
iApply (fupd_mask_mono _); eauto.
iMod ("IH3" with "Hj") as "IH3". iModIntro. iNext. simpl.
iApply fupd_wp. iApply (fupd_mask_mono _); eauto.
iMod ("IH3" with "Hj") as "IH3". iModIntro.
wp_bind (env_subst (fst <$> vvs) e2).
iApply (wp_wand with "IH3").
iIntros (v). iDestruct 1 as (v') "[Hj #Ht]".
......@@ -285,12 +286,11 @@ Section masked.
iIntros (?) "IH1 IH2 IH3".
iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
smart_bind j (env_subst _ e0) (env_subst _ e0') "IH1" v v' "IH1".
iDestruct "IH1" as ([]) "[% %]"; simplify_eq/=; iApply fupd_wp.
- tp_if_true j; eauto. iModIntro.
iApply wp_if_true. iNext. iApply fupd_wp.
iDestruct "IH1" as ([]) "[% %]"; simplify_eq/=;
tp_if j.
- iApply wp_if_true. iNext.
smart_bind j (env_subst _ e1) (env_subst _ e1') "IH2" v v' "?".
- tp_if_false j; eauto. iModIntro.
iApply wp_if_false. iNext. iApply fupd_wp.
- iApply wp_if_false. iNext.
smart_bind j (env_subst _ e2) (env_subst _ e2') "IH3" v v' "?".
Qed.
......@@ -308,11 +308,10 @@ Section masked.
smart_bind j (env_subst _ e2) (env_subst _ e2') "IH2" w w' "IH2".
iDestruct "IH1" as (n) "[% %]"; simplify_eq/=.
iDestruct "IH2" as (n') "[% %]"; simplify_eq/=.
iApply fupd_wp.
destruct (binop_nat_typed_safe op n n' _ Hopτ) as [v' Hopv'].
tp_binop j; eauto; tp_normalise j.
iApply wp_nat_binop; eauto. iModIntro. iExists _; iSplitL; eauto.
repeat iModIntro.
iModIntro.
destruct op; simpl in Hopv'; simplify_eq/=; try destruct eq_nat_dec; try destruct le_dec;
try destruct lt_dec; eauto.
Qed.
......@@ -331,11 +330,9 @@ Section masked.
smart_bind j (env_subst _ e2) (env_subst _ e2') "IH2" w w' "IH2".
iDestruct "IH1" as (n) "[% %]"; simplify_eq/=.
iDestruct "IH2" as (n') "[% %]"; simplify_eq/=.
iApply fupd_wp.
destruct (binop_bool_typed_safe op n n' _ Hopτ) as [v' Hopv'].
tp_binop j; eauto; tp_normalise j.
iApply wp_nat_binop; eauto. iModIntro. iExists _; iSplitL; eauto.
repeat iModIntro.
destruct op; simpl in Hopv'; simplify_eq/=; try destruct eq_nat_dec; try destruct le_dec;
try destruct lt_dec; eauto.
Qed.
......
(* the contents of this file sould belong elsewhere *)
From iris.proofmode Require Import tactics.
From iris_logrel.F_mu_ref_conc Require Import lang subst tactics rules rules_binary logrel_binary.
From iris_logrel.F_mu_ref_conc Require Import lang logrel_binary.
Definition lamsubst (e : expr) (v : val) : expr :=
match e with
......
From iris_logrel.F_mu_ref_conc Require Export fundamental_binary logrel_binary.
From iris.proofmode Require Import tactics.
From iris_logrel.F_mu_ref_conc Require Import rules_binary hax.
From iris.program_logic Require Import ectx_lifting.
From iris_logrel.F_mu_ref_conc Require Export lang subst hax.
Class PureExec (P : Prop) (e1 e2 : expr) := {
pure_exec_safe : P -> σ, head_reducible e1 σ;
......@@ -18,7 +15,7 @@ split; intros Hval.
- intros. by inv_head_step.
Qed.
Instance pure_rec f x e1 e2 v2 `{Closed (x :b: f :b: ) e1} `(to_val e2 = Some v2) :
Instance pure_rec f x e1 e2 v2 `{Closed (Rec f x e1)} `(to_val e2 = Some v2) :
PureExec True
(App (Rec f x e1) e2)
(subst' f (Rec f x e1) (subst' x e2 e1)).
......@@ -40,7 +37,7 @@ split; intros ?; subst.
Qed.
Instance pure_fst e1 v1 e2 v2 `(to_val e1 = Some v1) `(to_val e2 = Some v2) :
PureExec True (Fst (e1, e2)) e1.
PureExec True (Fst (Pair e1 e2)) e1.
Proof.
split; intros ?.
- intros. do 3 eexists. econstructor; eauto using to_of_val.
......@@ -48,7 +45,7 @@ split; intros ?.
Qed.
Instance pure_snd e1 v1 e2 v2 `(to_val e1 = Some v1) `(to_val e2 = Some v2) :
PureExec True (Snd (e1, e2)) e2.
PureExec True (Snd (Pair e1 e2)) e2.
Proof.
split; intros ?.
- intros. do 3 eexists. econstructor; eauto using to_of_val.
......@@ -64,7 +61,7 @@ split; intros ?.
Qed.
Instance pure_if_true e1 e2 `{Closed e1} `{Closed e2} :
Instance pure_if_true e1 e2 :
PureExec True (If true e1 e2) e1.
Proof.
split; intros ?.
......@@ -72,7 +69,7 @@ split; intros ?.
- intros. by inv_head_step.
Qed.
Instance pure_if_false e1 e2 `{Closed e1} `{Closed e2} :
Instance pure_if_false e1 e2 :
PureExec True (If false e1 e2) e2.
Proof.
split; intros ?.
......@@ -80,7 +77,7 @@ split; intros ?.
- intros. by inv_head_step.
Qed.
Instance pure_case_inl e0 v `(to_val e0 = Some v) e1 e2 `{Closed e1} `{Closed e2} :
Instance pure_case_inl e0 v `(to_val e0 = Some v) e1 e2 :
PureExec True (Case (InjL e0) e1 e2) (e1 e0).
Proof.
split; intros ?.
......@@ -88,7 +85,7 @@ split; intros ?.
- intros. by inv_head_step.
Qed.
Instance pure_case_inr e0 v `(to_val e0 = Some v) e1 e2 `{Closed e1} `{Closed e2} :
Instance pure_case_inr e0 v `(to_val e0 = Some v) e1 e2 :
PureExec True (Case (InjR e0) e1 e2) (e2 e0).
Proof.
split; intros ?.
......
This diff is collapsed.
......@@ -113,6 +113,10 @@ Ltac of_expr e :=
| _ =>
lazymatch goal with
| [H : to_val e = Some ?ev |- _] =>
(* DF: The reason why we do /not/ produce `Val ev` here is that
`of_val ev` is generally not going to be definitionally equal
to `e`. Since we want to solve certain things "by computation"
this sort of defats the purpose. *)
constr:(@ClosedExpr e (to_val_closed e ev H))
| [H : Closed e |- _] => constr:(@ClosedExpr e H)
| [H : Is_true (is_closed e) |- _] => constr:(@ClosedExpr e H)
......@@ -254,6 +258,31 @@ Ltac solve_closed :=
Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
Hint Extern 0 (Closed _ _) => solve_closed.
(* TODO: This is horrible, but it actually works. *)
(* DF: *)
(* The issue here is that some lemmas about Rec's depend on the *)
(* specific assumption that [Closed (x :b: f :b: ) ebody] holds. *)
(* This duplication leads to confusion and necessitates monstrosities likes this one. *)
Ltac solve_closed2 :=
lazymatch goal with
| [ H: Closed ?X (Rec ?f ?x ?e) |- Closed (?x :b: ?f :b: ?X) ?e ] =>
change (Closed X (Rec f x e)); apply H
| [ |- Closed (?x :b: ?f :b: ?X) ?e ] =>
change (Closed X (Rec f x e)); solve_closed
| [ H: Closed (?x :b: ?f :b: ?X) ?e |- Closed ?X (Rec ?f ?x ?e) ] =>
change (Closed (x :b: f :b: X) e); apply H
| _ => solve_closed
end.
Hint Extern 1 (Closed _ _) => solve_closed2 : typeclass_instances.
(* Hint Extern 1 (Closed _ _) => solve_closed2. *)
(* DF: I used it for automatically discharging assumptions for the PureExec instances *)
Ltac lookup_to_val :=
lazymatch goal with
| [ H: to_val ?e = Some ?v |- to_val ?e = Some _ ] => apply H
end.
Hint Extern 1 (to_val _ = Some _) => lookup_to_val : typeclass_instances.
Ltac simpl_subst :=
cbn[subst'];
repeat match goal with
......
......@@ -116,3 +116,56 @@ environment substitution. But then we have =subst_p (<[x:=(v,v')]>
...) e=. You would like to convert that to =subst' x ..= so that one
can actually use the hypothesis.
* Comments on the design
** Common setting for different symbolic execution tactics
There are multiple layers of tactics for symbolic execution in the code.
*** Layers of tactics
We have symbolic execution rules (either as lemmas or as tactics and tactic lemmas) for
- WP calculus
- Symbolic execution in the ghost threadpool
- Symbolic execution in the relational interpretation
*** Tactics and tactic lemmas
Here we make a distinction between an actual /tactic/ and a /tacic lemma/.
A /tactic lemma/ is a lemma in Coq that is a Coq proposition that is saying more than a certain ~iProp~ holds.
Hence, the tacic lemma is typechecked. A /tactic/ is an actual piece of Ltac code that makes it more convenient to apply the aforementioned lemma.
For instance, this is a tactic lemma for symbolically executing a ~Load~ in the ghost threadpool.
#+BEGIN_SRC coq
Lemma tac_tp_load `{logrelG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K' e l v Q q :
nclose specN ⊆ E1 →
envs_lookup i1 Δ1 = Some (p, spec_ctx ρ) →
envs_lookup_delete i2 Δ1 = Some (false, j ⤇ e, Δ2)%I →
e = fill K' (Load (Loc l)) →
envs_lookup i3 Δ2 = Some (false, l ↦ₛ{q} v)%I →
envs_simple_replace i3 false
(Esnoc (Esnoc Enil i2 (j ⤇ fill K' (of_val v))) i3 (l ↦ₛ{q} v)%I) Δ2 = Some Δ3 →
(Δ3 ⊢ |={E1,E2}=> Q) →
(Δ1 ⊢ |={E1,E2}=> Q).
#+END_SRC
It takes care of managing the context in a typesafe way.
Then this lemma is actually applied with the help of the following tactic
#+BEGIN_SRC coq
Tactic Notation "tp_load" constr(j) :=
iStartProof;
eapply (tac_tp_load j);
[solve_ndisj || fail "tp_load: cannot prove 'nclose specN ⊆ ?'"
|iAssumptionCore || fail "tp_load: cannot find spec_ctx" (* spec_ctx *)
|iAssumptionCore || fail "tp_load: cannot find '" j " ⤇ ?'"
|tp_bind_helper
|iAssumptionCore || fail "tp_load: cannot find '? ↦ₛ ?'"
|env_cbv; reflexivity || fail "tp_load: this should not happen"
|(* new goal *)].
#+END_SRC
The tactic itself provides error messages as well as some means of discharging the assumptions for the tactic lemma.
Since the tactic lemma is being ~eapply~ed, it is always important to think about the order we put the assumptions in the lemma.
At the moment we apply the lemma Coq's unification mechanism instantiates ~Δ1~, ~E1~, ~E2~, and ~Q~.
We need to make sure that by discharging the assumptions in the correct order we can instantiate ~Δ3~ to something meaningful.
For instance, the fourth assumption says something about the shape of the expression that is executed in thread ~j~; however, this expression is not known until we lookup it up in the context.
Hence, the fourth assumption should come *after* the third one.
Likewise, the fifth assumption says that there is a resource ~l ↦ₛ v~ in context ~Δ2~, but we only know the location ~l~ once we decompose the expression ~e~ into an evaluation context and a load expression.
Thus, this assumption should come after ~e = fill K'(Load (Loc l))~.
*** Pure reductions
Since ultimately all the levels of the symbolic executions operate on the same language we can share some machinery between the levels.
One observation is that the easiest (as well as the most numerous) tactics to write are those that preform symbolic execution of pure reductions.
To that extent we would like to have one generic "pure symbolic reduction" tactic/tactic lemma per level.
This is achieved by writing "open ended" tactic lemmas that are parameterized over a typeclass of pure reductions.
The typeclass ~PureExec φ e1 e2~ says that there is a pure (and deterministic) reduction from ~e1~ to ~e2~ in the language under some (pure) assumption φ.
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