Commit 3d448c5d authored by Ralf Jung's avatar Ralf Jung

state adequacy wp-based

parent acdcc20a
...@@ -9,19 +9,18 @@ ...@@ -9,19 +9,18 @@
\ralf{Sync this with Coq.} \ralf{Sync this with Coq.}
Hoare triples and view shifts are syntactic sugar for weakest (liberal) preconditions and primitive view shifts, respectively: Hoare triples and view shifts are syntactic sugar for weakest (liberal) preconditions and primitive view shifts, respectively:
\[ % \[
\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \Ra \dynA{\expr}{\lambda\Ret\val.\propB}{\mask})} % \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \Ra \dynA{\expr}{\lambda\Ret\val.\propB}{\mask})}
\qquad\qquad % \qquad\qquad
\begin{aligned} % \begin{aligned}
\prop \vs[\mask_1][\mask_2] \propB &\eqdef \always{(\prop \Ra \pvsA{\propB}{\mask_1}{\mask_2})} \\ % \prop \vs[\mask_1][\mask_2] \propB &\eqdef \always{(\prop \Ra \pvsA{\propB}{\mask_1}{\mask_2})} \\
\prop \vsE[\mask_1][\mask_2] \propB &\eqdef \prop \vs[\mask_1][\mask_2] \propB \land \propB \vs[\mask2][\mask_1] \prop % \prop \vsE[\mask_1][\mask_2] \propB &\eqdef \prop \vs[\mask_1][\mask_2] \propB \land \propB \vs[\mask2][\mask_1] \prop
\end{aligned} % \end{aligned}
\] % \]
We write just one mask for a view shift when $\mask_1 = \mask_2$. We write just one mask for a view shift when $\mask_1 = \mask_2$.
The convention for omitted masks is generous: The convention for omitted masks is generous:
An omitted $\mask$ is $\top$ for Hoare triples and $\emptyset$ for view shifts. An omitted $\mask$ is $\top$ for Hoare triples and $\emptyset$ for view shifts.
We write $\provesalways$ to denote judgments that can only be extended with a boxed proof context, in contrast to our usual convention of allowing the context to be extended with any assertions.
\paragraph{Hoare triples.} \paragraph{Hoare triples.}
\begin{mathpar} \begin{mathpar}
...@@ -120,12 +119,12 @@ The following are easily derived by unfolding the sugar for Hoare triples and vi ...@@ -120,12 +119,12 @@ The following are easily derived by unfolding the sugar for Hoare triples and vi
{\All \var. (\prop \vs[\mask_1][\mask_2] \propB)} {\All \var. (\prop \vs[\mask_1][\mask_2] \propB)}
{(\Exists \var. \prop) \vs[\mask_1][\mask_2] \propB} {(\Exists \var. \prop) \vs[\mask_1][\mask_2] \propB}
\and \and
\inferHB{BoxOut} \inferHB{HtBox}
{\always\propB \provesalways \hoare{\prop}{\expr}{\Ret\val.\propC}[\mask]} {\always\propB \proves \hoare{\prop}{\expr}{\Ret\val.\propC}[\mask]}
{\hoare{\prop \land \always{\propB}}{\expr}{\Ret\val.\propC}[\mask]} {\hoare{\prop \land \always{\propB}}{\expr}{\Ret\val.\propC}[\mask]}
\and \and
\inferHB{VSBoxOut} \inferHB{VsBox}
{\always\propB \provesalways \prop \vs[\mask_1][\mask_2] \propC} {\always\propB \proves \prop \vs[\mask_1][\mask_2] \propC}
{\prop \land \always{\propB} \vs[\mask_1][\mask_2] \propC} {\prop \land \always{\propB} \vs[\mask_1][\mask_2] \propC}
\and \and
\inferH{False} \inferH{False}
......
...@@ -115,8 +115,8 @@ Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\t ...@@ -115,8 +115,8 @@ Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\t
\ownPhys{\term} \mid \ownPhys{\term} \mid
\always\prop \mid \always\prop \mid
{\later\prop} \mid {\later\prop} \mid
\pvsA{\prop}{\term}{\term} \mid \pvs[\term][\term] \prop\mid
\dynA{\term}{\pred}{\term} \wpre{\term}{\pred}[\term]
\end{align*} \end{align*}
Recursive predicates must be \emph{guarded}: in $\MU \var. \pred$, the variable $\var$ can only appear under the later $\later$ modality. Recursive predicates must be \emph{guarded}: in $\MU \var. \pred$, the variable $\var$ can only appear under the later $\later$ modality.
...@@ -263,7 +263,7 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $ ...@@ -263,7 +263,7 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
\vctx \proves \wtt{\mask}{\textsort{InvMask}} \and \vctx \proves \wtt{\mask}{\textsort{InvMask}} \and
\vctx \proves \wtt{\mask'}{\textsort{InvMask}} \vctx \proves \wtt{\mask'}{\textsort{InvMask}}
}{ }{
\vctx \proves \wtt{\pvsA{\prop}{\mask}{\mask'}}{\Prop} \vctx \proves \wtt{\pvs[\mask][\mask'] \prop}{\Prop}
} }
\and \and
\infer{ \infer{
...@@ -271,7 +271,7 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $ ...@@ -271,7 +271,7 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
\vctx \proves \wtt{\pred}{\textsort{Val} \to \Prop} \and \vctx \proves \wtt{\pred}{\textsort{Val} \to \Prop} \and
\vctx \proves \wtt{\mask}{\textsort{InvMask}} \vctx \proves \wtt{\mask}{\textsort{InvMask}}
}{ }{
\vctx \proves \wtt{\dynA{\expr}{\pred}{\mask}}{\Prop} \vctx \proves \wtt{\wpre{\expr}{\pred}[\mask]}{\Prop}
} }
\end{mathparpagebreakable} \end{mathparpagebreakable}
...@@ -288,6 +288,7 @@ This is a \emph{meta-level} assertions about propositions, defined by the follow ...@@ -288,6 +288,7 @@ This is a \emph{meta-level} assertions about propositions, defined by the follow
The judgment $\vctx \mid \pfctx \proves \prop$ says that with free variables $\vctx$, proposition $\prop$ holds whenever all assumptions $\pfctx$ hold. The judgment $\vctx \mid \pfctx \proves \prop$ says that with free variables $\vctx$, proposition $\prop$ holds whenever all assumptions $\pfctx$ hold.
We implicitly assume that an arbitrary variable context, $\vctx$, is added to every constituent of the rules. We implicitly assume that an arbitrary variable context, $\vctx$, is added to every constituent of the rules.
Furthermore, an arbitrary \emph{boxed} assertion context $\always\pfctx$ may be added to every constituent.
Axioms $\prop \Ra \propB$ stand for judgments $\vctx \mid \cdot \proves \prop \Ra \propB$ with no assumptions. Axioms $\prop \Ra \propB$ stand for judgments $\vctx \mid \cdot \proves \prop \Ra \propB$ with no assumptions.
(Bi-implications are analogous.) (Bi-implications are analogous.)
...@@ -500,17 +501,17 @@ This is entirely standard. ...@@ -500,17 +501,17 @@ This is entirely standard.
\subsection{Adequacy} \subsection{Adequacy}
~\\\ralf{Check if this is still accurate. Port to weakest-pre.}
The adequacy statement reads as follows: The adequacy statement reads as follows:
\begin{align*} \begin{align*}
&\All \mask, \expr, \val, \pred, i, \state, \state', \tpool'. &\All \mask, \expr, \val, \pred, i, \state, \melt, \state', \tpool'.
\\&( \proves \hoare{\ownPhys\state}{\expr}{x.\; \pred(x)}[\mask]) \implies \\&(\All n. \melt \in \mval_n) \Ra
\\&\cfg{\state}{[i \mapsto \expr]} \step^\ast \\&( \ownPhys\state * \ownGGhost\melt \proves \wpre{\expr}{x.\; \pred(x)}[\mask]) \Ra
\cfg{\state'}{[i \mapsto \val] \uplus \tpool'} \implies \\&\cfg{\state}{[\expr]} \step^\ast
\cfg{\state'}{[\val] \dplus \tpool'} \Ra
\\&\pred(\val) \\&\pred(\val)
\end{align*} \end{align*}
where $\pred$ can mention neither resources nor invariants. where $\pred$ is a \emph{meta-level} predicate over values, \ie it can mention neither resources nor invariants.
% RJ: If we want this section back, we should port it to primitive view shifts and prove it in Coq. % RJ: If we want this section back, we should port it to primitive view shifts and prove it in Coq.
......
...@@ -318,7 +318,6 @@ ...@@ -318,7 +318,6 @@
\def\Lam #1.{\lambda #1.\spac}% \def\Lam #1.{\lambda #1.\spac}%
\newcommand{\proves}{\vdash} \newcommand{\proves}{\vdash}
\newcommand{\provesalways}{\vdash_{\!\!\boxempty}}
\newcommand{\wand}{\;{{\mbox{---}}\!\!{*}}\;} \newcommand{\wand}{\;{{\mbox{---}}\!\!{*}}\;}
...@@ -327,12 +326,8 @@ ...@@ -327,12 +326,8 @@
\newcommand{\gmapsto}{\hookrightarrow}% \newcommand{\gmapsto}{\hookrightarrow}%
\newcommand{\fgmapsto}[1][\mathrm{-}]{\xhookrightarrow{#1}}% \newcommand{\fgmapsto}[1][\mathrm{-}]{\xhookrightarrow{#1}}%
\newcommand{\dyn}[2]{\textlog{wp}({#1}, {#2})} \NewDocumentCommand\wpre{m m o}%
\newcommand{\adyn}[2]{{#1}\;\llparenthesis{#2}\rrparenthesis} {{#1} \spac \{#2\}_{#3}}
\newcommand{\dynpred}[2]{\textdom{wp}({#1}, {#2})}
\newcommand{\dynA}[3]{\textlog{wp}_{#3}({#1}, {#2})}
\newcommand{\pvs}[1]{\textlog{vs}({#1})}
\newcommand{\pvsA}[3]{\textlog{vs}_{#2}^{#3}({#1})}
\newcommand{\later}{\mathord{\triangleright}} \newcommand{\later}{\mathord{\triangleright}}
\newcommand{\always}{\Box{}} \newcommand{\always}{\Box{}}
...@@ -369,6 +364,8 @@ ...@@ -369,6 +364,8 @@
\NewDocumentCommand \vsL {O{} O{}} {\vsGen[#1]{\Lleftarrow}[#2]} \NewDocumentCommand \vsL {O{} O{}} {\vsGen[#1]{\Lleftarrow}[#2]}
\NewDocumentCommand \vsE {O{} O{}} % \NewDocumentCommand \vsE {O{} O{}} %
{\vsGen[#1]{\Lleftarrow\!\!\!\Rrightarrow}[#2]} {\vsGen[#1]{\Lleftarrow\!\!\!\Rrightarrow}[#2]}
\NewDocumentCommand \pvs {O{} O{}} {\mathord{\vsGen[#1]{{\mid\kern-0.4ex\Rrightarrow}}[#2]}}
%% Hoare Triples %% Hoare Triples
\newcommand*{\hoaresizebox}[1]{% \newcommand*{\hoaresizebox}[1]{%
......
...@@ -54,8 +54,8 @@ Proof. ...@@ -54,8 +54,8 @@ Proof.
apply uPred_weaken with (k + n) r2; eauto using cmra_included_l. } apply uPred_weaken with (k + n) r2; eauto using cmra_included_l. }
by rewrite -Permutation_middle /= big_op_app. by rewrite -Permutation_middle /= big_op_app.
Qed. Qed.
Lemma ht_adequacy_steps P Φ k n e1 t2 σ1 σ2 r1 : Lemma wp_adequacy_steps P Φ k n e1 t2 σ1 σ2 r1 :
{{ P }} e1 {{ Φ }} P #> e1 {{ Φ }}
nsteps step k ([e1],σ1) (t2,σ2) nsteps step k ([e1],σ1) (t2,σ2)
1 < n wsat (k + n) σ1 r1 1 < n wsat (k + n) σ1 r1
P (k + n) r1 P (k + n) r1
...@@ -64,65 +64,89 @@ Proof. ...@@ -64,65 +64,89 @@ Proof.
intros Hht ????; apply (nsteps_wptp [Φ] k n ([e1],σ1) (t2,σ2) [r1]); intros Hht ????; apply (nsteps_wptp [Φ] k n ([e1],σ1) (t2,σ2) [r1]);
rewrite /big_op ?right_id; auto. rewrite /big_op ?right_id; auto.
constructor; last constructor. constructor; last constructor.
move: Hht; rewrite /ht; uPred.unseal=> Hht. apply Hht; by eauto using cmra_included_unit.
apply Hht with (k + n) r1; by eauto using cmra_included_unit.
Qed. Qed.
Lemma ht_adequacy_own Φ e1 t2 σ1 m σ2 :
Lemma wp_adequacy_own Φ e1 t2 σ1 m σ2 :
m m
{{ ownP σ1 ownG m }} e1 {{ Φ }} (ownP σ1 ownG m) #> e1 {{ Φ }}
rtc step ([e1],σ1) (t2,σ2) rtc step ([e1],σ1) (t2,σ2)
rs2 Φs', wptp 2 t2 (Φ :: Φs') rs2 wsat 2 σ2 (big_op rs2). rs2 Φs', wptp 2 t2 (Φ :: Φs') rs2 wsat 2 σ2 (big_op rs2).
Proof. Proof.
intros Hv ? [k ?]%rtc_nsteps. intros Hv ? [k ?]%rtc_nsteps.
eapply ht_adequacy_steps with (r1 := (Res (Excl σ1) (Some m))); eauto; [|]. eapply wp_adequacy_steps with (r1 := (Res (Excl σ1) (Some m))); eauto; [|].
{ by rewrite Nat.add_comm; apply wsat_init, cmra_valid_validN. } { by rewrite Nat.add_comm; apply wsat_init, cmra_valid_validN. }
uPred.unseal; exists (Res (Excl σ1) ), (Res (Some m)); split_and?. uPred.unseal; exists (Res (Excl σ1) ), (Res (Some m)); split_and?.
- by rewrite Res_op ?left_id ?right_id. - by rewrite Res_op ?left_id ?right_id.
- rewrite /ownP; uPred.unseal; rewrite /uPred_holds //=. - rewrite /ownP; uPred.unseal; rewrite /uPred_holds //=.
- by apply ownG_spec. - by apply ownG_spec.
Qed. Qed.
Theorem ht_adequacy_result E φ e v t2 σ1 m σ2 :
Theorem wp_adequacy_result E φ e v t2 σ1 m σ2 :
m m
{{ ownP σ1 ownG m }} e @ E {{ λ v', φ v' }} (ownP σ1 ownG m) #> e @ E {{ λ v', φ v' }}
rtc step ([e], σ1) (of_val v :: t2, σ2) rtc step ([e], σ1) (of_val v :: t2, σ2)
φ v. φ v.
Proof. Proof.
intros Hv ? Hs. intros Hv ? Hs.
destruct (ht_adequacy_own (λ v', φ v')%I e (of_val v :: t2) σ1 m σ2) destruct (wp_adequacy_own (λ v', φ v')%I e (of_val v :: t2) σ1 m σ2)
as (rs2&Qs&Hwptp&?); auto. as (rs2&Qs&Hwptp&?); auto.
{ by rewrite -(ht_mask_weaken E ). } { by rewrite -(wp_mask_weaken E ). }
inversion Hwptp as [|?? r ?? rs Hwp _]; clear Hwptp; subst. inversion Hwptp as [|?? r ?? rs Hwp _]; clear Hwptp; subst.
move: Hwp. rewrite wp_eq. uPred.unseal=> /wp_value_inv Hwp. move: Hwp. rewrite wp_eq. uPred.unseal=> /wp_value_inv Hwp.
rewrite pvs_eq in Hwp. rewrite pvs_eq in Hwp.
destruct (Hwp (big_op rs) 2 σ2) as [r' []]; rewrite ?right_id_L; auto. destruct (Hwp (big_op rs) 2 σ2) as [r' []]; rewrite ?right_id_L; auto.
Qed. Qed.
Lemma ht_adequacy_reducible E Φ e1 e2 t2 σ1 m σ2 :
Lemma ht_adequacy_result E φ e v t2 σ1 m σ2 :
m m
{{ ownP σ1 ownG m }} e1 @ E {{ Φ }} {{ ownP σ1 ownG m }} e @ E {{ λ v', φ v' }}
rtc step ([e], σ1) (of_val v :: t2, σ2)
φ v.
Proof.
intros ? Hht. eapply wp_adequacy_result with (E:=E); first done.
move:Hht. by rewrite /ht uPred.always_elim=>/uPred.impl_entails.
Qed.
Lemma wp_adequacy_reducible E Φ e1 e2 t2 σ1 m σ2 :
m
(ownP σ1 ownG m) #> e1 @ E {{ Φ }}
rtc step ([e1], σ1) (t2, σ2) rtc step ([e1], σ1) (t2, σ2)
e2 t2 to_val e2 = None reducible e2 σ2. e2 t2 to_val e2 = None reducible e2 σ2.
Proof. Proof.
intros Hv ? Hs [i ?]%elem_of_list_lookup He. intros Hv ? Hs [i ?]%elem_of_list_lookup He.
destruct (ht_adequacy_own Φ e1 t2 σ1 m σ2) as (rs2&Φs&?&?); auto. destruct (wp_adequacy_own Φ e1 t2 σ1 m σ2) as (rs2&Φs&?&?); auto.
{ by rewrite -(ht_mask_weaken E ). } { by rewrite -(wp_mask_weaken E ). }
destruct (Forall3_lookup_l (λ e Φ r, wp e Φ 2 r) t2 destruct (Forall3_lookup_l (λ e Φ r, wp e Φ 2 r) t2
(Φ :: Φs) rs2 i e2) as (Φ'&r2&?&?&Hwp); auto. (Φ :: Φs) rs2 i e2) as (Φ'&r2&?&?&Hwp); auto.
destruct (wp_step_inv Φ' e2 1 2 σ2 r2 (big_op (delete i rs2))); destruct (wp_step_inv Φ' e2 1 2 σ2 r2 (big_op (delete i rs2)));
rewrite ?right_id_L ?big_op_delete; auto. rewrite ?right_id_L ?big_op_delete; auto.
by rewrite -wp_eq. by rewrite -wp_eq.
Qed. Qed.
Theorem ht_adequacy_safe E Φ e1 t2 σ1 m σ2 :
Theorem wp_adequacy_safe E Φ e1 t2 σ1 m σ2 :
m m
{{ ownP σ1 ownG m }} e1 @ E {{ Φ }} (ownP σ1 ownG m) #> e1 @ E {{ Φ }}
rtc step ([e1], σ1) (t2, σ2) rtc step ([e1], σ1) (t2, σ2)
Forall (λ e, is_Some (to_val e)) t2 t3 σ3, step (t2, σ2) (t3, σ3). Forall (λ e, is_Some (to_val e)) t2 t3 σ3, step (t2, σ2) (t3, σ3).
Proof. Proof.
intros. intros.
destruct (decide (Forall (λ e, is_Some (to_val e)) t2)) as [|Ht2]; [by left|]. destruct (decide (Forall (λ e, is_Some (to_val e)) t2)) as [|Ht2]; [by left|].
apply (not_Forall_Exists _), Exists_exists in Ht2; destruct Ht2 as (e2&?&He2). apply (not_Forall_Exists _), Exists_exists in Ht2; destruct Ht2 as (e2&?&He2).
destruct (ht_adequacy_reducible E Φ e1 e2 t2 σ1 m σ2) as (e3&σ3&ef&?); destruct (wp_adequacy_reducible E Φ e1 e2 t2 σ1 m σ2) as (e3&σ3&ef&?);
rewrite ?eq_None_not_Some; auto. rewrite ?eq_None_not_Some; auto.
destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto. destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto.
right; exists (t2' ++ e3 :: t2'' ++ option_list ef), σ3; econstructor; eauto. right; exists (t2' ++ e3 :: t2'' ++ option_list ef), σ3; econstructor; eauto.
Qed. Qed.
Lemma ht_adequacy_safe E Φ e1 t2 σ1 m σ2 :
m
{{ ownP σ1 ownG m }} e1 @ E {{ Φ }}
rtc step ([e1], σ1) (t2, σ2)
Forall (λ e, is_Some (to_val e)) t2 t3 σ3, step (t2, σ2) (t3, σ3).
Proof.
intros ? Hht. eapply wp_adequacy_safe with (E:=E) (Φ:=Φ); first done.
move:Hht. by rewrite /ht uPred.always_elim=>/uPred.impl_entails.
Qed.
End adequacy. End adequacy.
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