From 0dbb90329ac1a8f0cfb654914a2da6062787d8cb Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Sat, 12 Mar 2016 11:09:10 +0100 Subject: [PATCH] docs: derived lifting rules --- docs/derived.tex | 59 +++++++++++++++++++++++++++++++++-- docs/logic.tex | 28 ++++++++--------- program_logic/hoare_lifting.v | 36 +++++++++++---------- 3 files changed, 90 insertions(+), 33 deletions(-) diff --git a/docs/derived.tex b/docs/derived.tex index aeb47ab4..ffb5e05e 100644 --- a/docs/derived.tex +++ b/docs/derived.tex @@ -205,9 +205,64 @@ The following rules can be derived for Hoare triples. \end{mathparpagebreakable} \paragraph{Lifting of operational semantics.} -We can derive some specialized forms of the lifting axioms for the operational semantics, as well as some forms that involve view shifts and Hoare triples. +We can derive some specialized forms of the lifting axioms for the operational semantics. +\begin{mathparpagebreakable} + \infer[wp-lift-atomic-step] + {\toval(\expr_1) = \bot \and + \red(\expr_1, \state_1) \and + \All \expr_2, \state_2, \expr_f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_f \Ra \Exists\val_2. \toval(\expr_2) = \val_2 \land \pred(\val_2,\state_2,\expr_f)} + {\later\ownPhys{\state_1} * \later\All \val, \state_2, \expr_f. \pred(\val, \state_2, \expr_f) \land \ownPhys{\state_2} \wand \prop * \wpre{\expr_f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask_1]{\Ret\val.\prop}} + + \infer[wp-lift-atomic-det-step] + {\toval(\expr_1) = \bot \and + \red(\expr_1, \state_1) \and + \All \expr'_2, \state'_2, \expr_f'. \expr_1,\state_1 \step \expr_2,\state_2,\expr_f \Ra \state_2 = \state_2' \land \toval(\expr_2') = \val_2 \land \expr_f = \expr_f'} + {\later\ownPhys{\state_1} * \later(\ownPhys{\state_2} \wand \prop[\val_2/\var] * \wpre{\expr_f}[\top]{\Ret\any.\TRUE}) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}} + + \infer[wp-lift-pure-det-step] + {\toval(\expr_1) = \bot \and + \All \state_1. \red(\expr_1, \state_1) \and + \All \state_1, \expr_2', \state_2, \expr_f'. \expr_1,\state_1 \step \expr_2,\state_2,\expr_f \Ra \state_1 = \state_2 \land \expr_2 = \expr_2' \land \expr_f = \expr_f'} + {\later ( \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr_f}[\top]{\Ret\any.\TRUE}) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}} +\end{mathparpagebreakable} -\ralf{Add these.} +Furthermore, we derive some forms that directly involve view shifts and Hoare triples. +\begin{mathparpagebreakable} + \infer[ht-lift-step] + {\mask_2 \subseteq \mask_1 \and + \toval(\expr_1) = \bot \and + \red(\expr_1, \state_1) \and + \All \expr_2, \state_2, \expr_f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_f \Ra \pred(\expr_2,\state_2,\expr_f) \\\\ + \prop \vs[\mask_1][\mask_2] \later\ownPhys{\state_1} * \later\prop' \and + \All \expr_2, \state_2, \expr_f. \pred(\expr_2, \state_2, \expr_f) * \ownPhys{\state_2} * \prop' \vs[\mask_2][\mask_1] \propB_1 * \propB_2 \\\\ + \All \expr_2, \state_2, \expr_f. \hoare{\propB_1}{\expr_2}{\Ret\val.\propC}[\mask_1] \and + \All \expr_2, \state_2, \expr_f. \hoare{\propB_2}{\expr_f}{\Ret\any. \TRUE}[\top]} + { \hoare\prop{\expr_1}{\Ret\val.\propC}[\mask_1] } + + \infer[ht-lift-atomic-step] + {\atomic(\expr_1) \and + \red(\expr_1, \state_1) \and + \All \expr_2, \state_2, \expr_f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_f \Ra \pred(\expr_2,\state_2,\expr_f) \\\\ + \prop \vs[\mask_1][\mask_2] \later\ownPhys{\state_1} * \later\prop' \and + \All \expr_2, \state_2, \expr_f. \hoare{\pred(\expr_2,\state_2,\expr_f) * \prop}{\expr_f}{\Ret\any. \TRUE}[\top]} + { \hoare{\later\ownPhys{\state_1} * \later\prop}{\expr_1}{\Ret\val.\Exists \state_2, \expr_f. \ownPhys{\state_2} * \pred(\ofval(\expr_2),\state_2,\expr_f)}[\mask_1] } + + \infer[ht-lift-pure-step] + {\toval(\expr_1) = \bot \and + \All\state_1. \red(\expr_1, \state_1) \and + \All \state_1, \expr_2, \state_2, \expr_f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_f \Ra \state_1 = \state_2 \land \pred(\expr_2,\expr_f) \\\\ + \All \expr_2, \expr_f. \hoare{\pred(\expr_2,\expr_f) * \prop}{\expr_2}{\Ret\val.\propB}[\mask_1] \and + \All \expr_2, \expr_f. \hoare{\pred(\expr_2,\expr_f) * \prop'}{\expr_f}{\Ret\any. \TRUE}[\top]} + { \hoare{\later(\prop*\prop')}{\expr_1}{\Ret\val.\propB}[\mask_1] } + + \infer[ht-lift-pure-det-step] + {\toval(\expr_1) = \bot \and + \All\state_1. \red(\expr_1, \state_1) \and + \All \state_1, \expr_2', \state_2, \expr_f'. \expr_1,\state_1 \step \expr_2,\state_2,\expr_f \Ra \state_1 = \state_2 \land \expr_2 = \expr_2' \land \expr_f = \expr_f' \\\\ + \hoare{\prop}{\expr_2}{\Ret\val.\propB}[\mask_1] \and + \hoare{\prop'}{\expr_f}{\Ret\any. \TRUE}[\top]} + { \hoare{\later(\prop*\prop')}{\expr_1}{\Ret\val.\propB}[\mask_1] } +\end{mathparpagebreakable} \subsection{Global functor and ghost ownership} diff --git a/docs/logic.tex b/docs/logic.tex index 9d89d639..1010939a 100644 --- a/docs/logic.tex +++ b/docs/logic.tex @@ -7,7 +7,7 @@ A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions} \end{mathpar} \item There exists a \emph{primitive reduction relation} $(-,- \step -,-,-) \subseteq \textdom{Expr} \times \textdom{State} \times \textdom{Expr} \times \textdom{State} \times (\textdom{Expr} \uplus \set{\bot})$ We will write $\expr_1, \state_1 \step \expr_2, \state_2$ for $\expr_1, \state_1 \step \expr_2, \state_2, \bot$. \\ - A reduction $\expr_1, \state_1 \step \expr_2, \state_2, \expr'$ indicates that, when $\expr_1$ reduces to $\expr$, a \emph{new thread} $\expr'$ is forked off. + A reduction $\expr_1, \state_1 \step \expr_2, \state_2, \expr_f$ indicates that, when $\expr_1$ reduces to $\expr$, a \emph{new thread} $\expr_f$ is forked off. \item All values are stuck: $\expr, \_ \step \_, \_, \_ \Ra \toval(\expr) = \bot$ \item There is a predicate defining \emph{atomic} expressions satisfying @@ -16,7 +16,7 @@ A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions} {\All\expr. \atomic(\expr) \Ra \toval(\expr) = \bot} \and {{ \begin{inbox} -\All\expr_1, \state_1, \expr_2, \state_2, \expr'. \atomic(\expr_1) \land \expr_1, \state_1 \step \expr_2, \state_2, \expr' \Ra {}\\\qquad\qquad\qquad\quad~~ \Exists \val_2. \toval(\expr_2) = \val_2 +\All\expr_1, \state_1, \expr_2, \state_2, \expr_f. \atomic(\expr_1) \land \expr_1, \state_1 \step \expr_2, \state_2, \expr_f \Ra {}\\\qquad\qquad\qquad\quad~~ \Exists \val_2. \toval(\expr_2) = \val_2 \end{inbox} }} \end{mathpar} @@ -26,7 +26,7 @@ It does not matter whether they fork off an arbitrary expression. \begin{defn} An expression $\expr$ and state $\state$ are \emph{reducible} (written $\red(\expr, \state)$) if - $\Exists \expr_2, \state_2, \expr'. \expr,\state \step \expr_2,\state_2,\expr'$ + $\Exists \expr_2, \state_2, \expr_f. \expr,\state \step \expr_2,\state_2,\expr_f$ \end{defn} \begin{defn}[Context] @@ -35,9 +35,9 @@ It does not matter whether they fork off an arbitrary expression. \item $\lctx$ does not turn non-values into values:\\ $\All\expr. \toval(\expr) = \bot \Ra \toval(\lctx(\expr)) = \bot$ \item One can perform reductions below $\lctx$:\\ - $\All \expr_1, \state_1, \expr_2, \state_2, \expr'. \expr_1, \state_1 \step \expr_2,\state_2,\expr' \Ra \lctx(\expr_1), \state_1 \step \lctx(\expr_2),\state_2,\expr'$ + $\All \expr_1, \state_1, \expr_2, \state_2, \expr_f. \expr_1, \state_1 \step \expr_2,\state_2,\expr_f \Ra \lctx(\expr_1), \state_1 \step \lctx(\expr_2),\state_2,\expr_f$ \item Reductions stay below $\lctx$ until there is a value in the hole:\\ - $\All \expr_1', \state_1, \expr_2, \state_2, \expr'. \toval(\expr_1') = \bot \land \lctx(\expr_1'), \state_1 \step \expr_2,\state_2,\expr' \Ra \Exists\expr_2'. \expr_2 = \lctx(\expr_2') \land \expr_1', \state_1 \step \expr_2',\state_2,\expr'$ + $\All \expr_1', \state_1, \expr_2, \state_2, \expr_f. \toval(\expr_1') = \bot \land \lctx(\expr_1'), \state_1 \step \expr_2,\state_2,\expr_f \Ra \Exists\expr_2'. \expr_2 = \lctx(\expr_2') \land \expr_1', \state_1 \step \expr_2',\state_2,\expr_f$ \end{enumerate} \end{defn} @@ -54,9 +54,9 @@ For any language $\Lang$, we define the corresponding thread-pool semantics. \cfg{\tpool'}{\state'}} \begin{mathpar} \infer - {\expr_1, \state_1 \step \expr_2, \state_2, \expr' \and \expr' \neq ()} + {\expr_1, \state_1 \step \expr_2, \state_2, \expr_f \and \expr_f \neq \bot} {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state} \step - \cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus [\expr']}{\state'}} + \cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus [\expr_f]}{\state'}} \and\infer {\expr_1, \state_1 \step \expr_2, \state_2} {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state} \step @@ -170,8 +170,6 @@ We introduce additional metavariables ranging over terms and generally let the c \] \paragraph{Variable conventions.} -We often abuse notation, using the preceding \emph{term} meta-variables to range over (bound) \emph{variables}. -We omit type annotations in binders, when the type is clear from context. We assume that, if a term occurs multiple times in a rule, its free variables are exactly those binders which are available at every occurrence. @@ -596,17 +594,19 @@ This is entirely standard. {\mask_2 \subseteq \mask_1 \and \toval(\expr_1) = \bot \and \red(\expr_1, \state_1) \and - \All \expr_2, \state_2, \expr'. \expr_1,\state_1 \step \expr_2,\state_2,\expr' \Ra \pred(\expr_2,\state_2,\expr')} - {\pvs[\mask_1][\mask_2] \later\ownPhys{\state_1} * \later\All \expr_2, \state_2, \expr'. \pred(\expr_2, \state_2, \expr') \land \ownPhys{\state_2} \wand \pvs[\mask_2][\mask_1] \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr'}[\top]{\Ret\var.\TRUE} {}\\\proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}} + \All \expr_2, \state_2, \expr_f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_f \Ra \pred(\expr_2,\state_2,\expr_f)} + { {\begin{inbox} % for some crazy reason, LaTeX is actually sensitive to the space between the "{ {" here and the "} }" below... + ~~\pvs[\mask_1][\mask_2] \later\ownPhys{\state_1} * \later\All \expr_2, \state_2, \expr_f. \pred(\expr_2, \state_2, \expr_f) \land {}\\\qquad\qquad\qquad\qquad\qquad \ownPhys{\state_2} \wand \pvs[\mask_2][\mask_1] \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr_f}[\top]{\Ret\any.\TRUE} {}\\\proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop} + \end{inbox}} } \infer[wp-lift-pure-step] {\toval(\expr_1) = \bot \and \All \state_1. \red(\expr_1, \state_1) \and - \All \state_1, \expr_2, \state_2, \expr'. \expr_1,\state_1 \step \expr_2,\state_2,\expr' \Ra \state_1 = \state_2 \land \pred(\expr_2,\expr')} - {\later\All \expr_2, \expr'. \pred(\expr_2, \expr') \wand \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr'}[\top]{\Ret\var.\TRUE} \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}} + \All \state_1, \expr_2, \state_2, \expr_f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_f \Ra \state_1 = \state_2 \land \pred(\expr_2,\expr_f)} + {\later\All \expr_2, \expr_f. \pred(\expr_2, \expr_f) \Ra \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr_f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}} \end{mathpar} -Here we define $\wpre{\expr'}[\mask]{\Ret\var.\prop} \eqdef \TRUE$ if $\expr' = \bot$ (remember that our stepping relation can, but does not have to, define a forked-off expression). +Here we define $\wpre{\expr_f}[\mask]{\Ret\var.\prop} \eqdef \TRUE$ if $\expr_f = \bot$ (remember that our stepping relation can, but does not have to, define a forked-off expression). \subsection{Adequacy} diff --git a/program_logic/hoare_lifting.v b/program_logic/hoare_lifting.v index 7318ff8e..c9dfcfed 100644 --- a/program_logic/hoare_lifting.v +++ b/program_logic/hoare_lifting.v @@ -23,19 +23,19 @@ Lemma ht_lift_step E1 E2 E2 ⊆ E1 → to_val e1 = None → reducible e1 σ1 → (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) → - ((P ={E1,E2}=> ▷ ownP σ1 ★ ▷ P') ∧ ∀ e2 σ2 ef, - (■ φ e2 σ2 ef ★ ownP σ2 ★ P' ={E2,E1}=> Φ1 e2 σ2 ef ★ Φ2 e2 σ2 ef) ∧ - {{ Φ1 e2 σ2 ef }} e2 @ E1 {{ Ψ }} ∧ - {{ Φ2 e2 σ2 ef }} ef ?@ ⊤ {{ λ _, True }}) + ((P ={E1,E2}=> ▷ ownP σ1 ★ ▷ P') ∧ + (∀ e2 σ2 ef, ■ φ e2 σ2 ef ★ ownP σ2 ★ P' ={E2,E1}=> Φ1 e2 σ2 ef ★ Φ2 e2 σ2 ef) ∧ + (∀ e2 σ2 ef, {{ Φ1 e2 σ2 ef }} e2 @ E1 {{ Ψ }}) ∧ + (∀ e2 σ2 ef, {{ Φ2 e2 σ2 ef }} ef ?@ ⊤ {{ λ _, True }})) ⊢ {{ P }} e1 @ E1 {{ Ψ }}. Proof. intros ?? Hsafe Hstep; apply: always_intro. apply impl_intro_l. rewrite (assoc _ P) {1}/vs always_elim impl_elim_r pvs_always_r. rewrite -(wp_lift_step E1 E2 φ _ e1 σ1) //; apply pvs_mono. rewrite always_and_sep_r -assoc; apply sep_mono_r. - rewrite (later_intro (∀ _, _)) -later_sep; apply later_mono. + rewrite [(_ ∧ _)%I]later_intro -later_sep; apply later_mono. apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef. - rewrite (forall_elim e2) (forall_elim σ2) (forall_elim ef). + do 3 rewrite (forall_elim e2) (forall_elim σ2) (forall_elim ef). apply wand_intro_l; rewrite !always_and_sep_l. (* Apply the view shift. *) rewrite (assoc _ _ P') -(assoc _ _ _ P') assoc. @@ -62,13 +62,14 @@ Proof. (λ e2 σ2 ef, ■ φ e2 σ2 ef ★ P)%I); try by (rewrite /φ'; eauto using atomic_not_val, atomic_step). apply and_intro; [by rewrite -vs_reflexive; apply const_intro|]. - apply forall_mono=>e2; apply forall_mono=>σ2; apply forall_mono=>ef. apply and_intro; [|apply and_intro; [|done]]. - - rewrite -vs_impl; apply: always_intro. apply impl_intro_l. + - apply forall_mono=>e2; apply forall_mono=>σ2; apply forall_mono=>ef. + rewrite -vs_impl; apply: always_intro. apply impl_intro_l. rewrite and_elim_l !assoc; apply sep_mono; last done. rewrite -!always_and_sep_l -!always_and_sep_r; apply const_elim_l=>-[??]. by repeat apply and_intro; try apply const_intro. - - apply (always_intro _ _), impl_intro_l; rewrite and_elim_l. + - apply forall_mono=>e2; apply forall_mono=>σ2; apply forall_mono=>ef. + apply (always_intro _ _), impl_intro_l; rewrite and_elim_l. rewrite -always_and_sep_r; apply const_elim_r=>-[[v Hv] ?]. rewrite -(of_to_val e2 v) // -wp_value'; []. rewrite -(exist_intro σ2) -(exist_intro ef) (of_to_val e2) //. @@ -79,16 +80,15 @@ Lemma ht_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) P P' Ψ e to_val e1 = None → (∀ σ1, reducible e1 σ1) → (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) → - (∀ e2 ef, - {{ ■ φ e2 ef ★ P }} e2 @ E {{ Ψ }} ∧ - {{ ■ φ e2 ef ★ P' }} ef ?@ ⊤ {{ λ _, True }}) + ((∀ e2 ef, {{ ■ φ e2 ef ★ P }} e2 @ E {{ Ψ }}) ∧ + (∀ e2 ef, {{ ■ φ e2 ef ★ P' }} ef ?@ ⊤ {{ λ _, True }})) ⊢ {{ ▷(P ★ P') }} e1 @ E {{ Ψ }}. Proof. intros ? Hsafe Hstep; apply: always_intro. apply impl_intro_l. rewrite -(wp_lift_pure_step E φ _ e1) //. - rewrite (later_intro (∀ _, _)) -later_and; apply later_mono. + rewrite [(_ ∧ ∀ _, _)%I]later_intro -later_and; apply later_mono. apply forall_intro=>e2; apply forall_intro=>ef; apply impl_intro_l. - rewrite (forall_elim e2) (forall_elim ef). + do 2 rewrite (forall_elim e2) (forall_elim ef). rewrite always_and_sep_l !always_and_sep_r {1}(always_sep_dup (■ _)). sep_split left: [■ φ _ _; P; {{ ■ φ _ _ ★ P }} e2 @ E {{ Ψ }}]%I. - rewrite assoc {1}/ht -always_wand_impl always_elim wand_elim_r //. @@ -106,11 +106,13 @@ Lemma ht_lift_pure_det_step Proof. intros ? Hsafe Hdet. rewrite -(ht_lift_pure_step _ (λ e2' ef', e2 = e2' ∧ ef = ef')); eauto. - apply forall_intro=>e2'; apply forall_intro=>ef'; apply and_mono. - - apply: always_intro. apply impl_intro_l. + apply and_mono. + - apply forall_intro=>e2'; apply forall_intro=>ef'. + apply: always_intro. apply impl_intro_l. rewrite -always_and_sep_l -assoc; apply const_elim_l=>-[??]; subst. by rewrite /ht always_elim impl_elim_r. - - destruct ef' as [e'|]; simpl; [|by apply const_intro]. + - apply forall_intro=>e2'; apply forall_intro=>ef'. + destruct ef' as [e'|]; simpl; [|by apply const_intro]. apply: always_intro. apply impl_intro_l. rewrite -always_and_sep_l -assoc; apply const_elim_l=>-[??]; subst. by rewrite /= /ht always_elim impl_elim_r. -- GitLab