diff --git a/docs/logic.tex b/docs/logic.tex index 0af9326d88e450de865379cf71528ba0c71e41d4..e12cdd02ca2e034d74cc66caa03e3af8bc92c15b 100644 --- a/docs/logic.tex +++ b/docs/logic.tex @@ -1,6 +1,6 @@ \section{Language} -A \emph{language} $\Lang$ consists of a set \textdom{Exp} of \emph{expressions} (metavariable $\expr$), a set \textdom{Val} of \emph{values} (metavariable $\val$), and a set \textdom{State} of \emph{states} (metvariable $\state$) such that +A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions} (metavariable $\expr$), a set \textdom{Val} of \emph{values} (metavariable $\val$), and a set \textdom{State} of \emph{states} (metvariable $\state$) such that \begin{itemize} \item There exist functions $\ofval : \textdom{Val} \to \textdom{Expr}$ and $\toval : \textdom{Expr} \pfn \textdom{val}$ (notice the latter is partial), such that \begin{mathpar} {\All \expr, \val. \toval(\expr) = \val \Ra \ofval(\val) = \expr} \and {\All\val. \toval(\ofval(\val)) = \val} @@ -24,6 +24,15 @@ In other words, atomic expression \emph{reduce in one step to a value}. It does not matter whether they fork off an arbitrary expression. \end{itemize} +\begin{defn}[Context] + A function $\lctx : \textdom{Expr} \to \textdom{Expr}$ is a \emph{context} if the following conditions are satisfied + \begin{align*} + \All\expr.& \toval(\expr) = \bot \Ra \toval(\lctx(\expr)) = \bot \tagH{lang-ctx-not-val}\\ + \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' \tagH{lang-ctx-step}\\ + \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' \tagH{lang-ctx-step-inv} + \end{align*} +\end{defn} + \subsection{The concurrent language} For any language $\Lang$, we define the corresponding thread-pool semantics. @@ -116,11 +125,12 @@ Iris syntax is built up from a signature $\Sig$ and a countably infinite set \t \always\prop \mid {\later\prop} \mid \pvs[\term][\term] \prop\mid - \wpre{\term}{\pred}[\term] + \wpre{\term}{\Ret\var.\term}[\term] \end{align*} Recursive predicates must be \emph{guarded}: in\MU \var. \pred$, the variable$\var$can only appear under the later$\later$modality. Note that$\always$and$\later$bind more tightly than$*$,$\wand$,$\land$,$\lor$, and$\Ra$. +We will write$\pvs[\term] \prop$for$\pvs[\term][\term] \prop$. \paragraph{Metavariable conventions.} We introduce additional metavariables ranging over terms and generally let the choice of metavariable indicate the term's type: @@ -129,7 +139,7 @@ We introduce additional metavariables ranging over terms and generally let the c \text{metavariable} & \text{type} \\\hline \term, \termB & \text{arbitrary} \\ \val, \valB & \textsort{Val} \\ - \expr & \textsort{Exp} \\ + \expr & \textsort{Expr} \\ \state & \textsort{State} \\ \end{array} \qquad\qquad @@ -267,11 +277,11 @@ In writing$\vctx, x:\type$, we presuppose that$x$is not already declared in$ } \and \infer{ - \vctx \proves \wtt{\expr}{\textsort{Exp}} \and - \vctx \proves \wtt{\pred}{\textsort{Val} \to \Prop} \and + \vctx \proves \wtt{\expr}{\textsort{Expr}} \and + \vctx,\var:\textsort{Val} \proves \wtt{\term}{\Prop} \and \vctx \proves \wtt{\mask}{\textsort{InvMask}} }{ - \vctx \proves \wtt{\wpre{\expr}{\pred}[\mask]}{\Prop} + \vctx \proves \wtt{\wpre{\expr}{\Ret\var.\term}[\mask]}{\Prop} } \end{mathparpagebreakable} @@ -456,13 +466,83 @@ This is entirely standard. \always{\All x. \prop} &\Lra& \All x. \always{\prop} \\ \always{\Exists x. \prop} &\Lra& \Exists x. \always{\prop} \\ \end{array} +\and +{ \term =_\type \term' \Ra \always \term =_\type \term'} +\and +{ \knowInv\iname\prop \Ra \always \knowInv\iname\prop} +\and +{ \ownGGhost{\munit(\melt)} \Ra \always \ownGGhost{\munit(\melt)}} \end{mathpar} \paragraph{Laws of primitive view shifts.} -~\\\ralf{Add these.} +\begin{mathpar} +\infer[pvs-intro] +{}{\prop \proves \pvs[\mask] \prop} + +\infer[pvs-mono] +{\prop \proves \propB} +{\pvs[\mask_1][\mask_2] \prop \proves \pvs[\mask_1][\mask_2] \propB} + +\infer[pvs-timeless] +{\timeless\prop} +{\later\prop \proves \pvs[\mask] \prop} + +\infer[pvs-trans] +{\mask_2 \subseteq \mask_1 \cup \mask_3} +{\pvs[\mask_1][\mask_2] \pvs[\mask_2][\mask_3] \prop \proves \pvs[\mask_1][\mask_3] \prop} + +\infer[pvs-mask-frame] +{}{\pvs[\mask_1][\mask_2] \prop \proves \pvs[\mask_1 \uplus \mask_f][\mask_2 \uplus \mask_f] \prop} + +\infer[pvs-frame] +{}{\propB * \pvs[\mask_1][\mask_2]\prop \proves \pvs[\mask_1][\mask_2] \propB * \prop} + +\infer[pvs-allocI] +{\text{$\mask$ is infinite}} +{\later\prop \proves \pvs[\mask] \Exists \iname \in \mask. \knowInv\iname\prop} + +\infer[pvs-openI] +{}{\knowInv\iname\prop \proves \pvs[\set\iname][\emptyset] \later\prop} + +\infer[pvs-closeI] +{}{\knowInv\iname\prop \land \later\prop \proves \pvs[\emptyset][\set\iname] \TRUE} + +\infer[pvs-update] +{\melt \mupd \meltsB} +{\ownGGhost\melt \proves \pvs[\mask] \Exists\meltB\in\meltsB. \ownGGhost\meltB} +\end{mathpar} \paragraph{Laws of weakest preconditions.} -~\\\ralf{Add these.} +\begin{mathpar} +\infer[wp-value] +{}{\prop[\val/\var] \proves \wpre{\val}{\Ret\var.\prop}[\mask]} + +\infer[wp-mono] +{\mask_1 \subseteq \mask_2 \and \var:\textsort{val}\mid\prop \proves \propB} +{\wpre\expr{\Ret\var.\prop}[\mask_1] \proves \wpre\expr{\Ret\var.\propB}[\mask_2]} + +\infer[pvs-wp] +{}{\pvs[\mask] \wpre\expr{\Ret\var.\prop}[\mask] \proves \wpre\expr{\Ret\var.\prop}[\mask]} + +\infer[wp-pvs] +{}{\wpre\expr{\Ret\var.\pvs[\mask] \prop}[\mask] \proves \wpre\expr{\Ret\var.\prop}[\mask]} + +\infer[wp-atomic] +{\mask_2 \subseteq \mask_1 \and \physatomic{\expr}} +{\pvs[\mask_1][\mask_2] \wpre\expr{\Ret\var. \pvs[\mask_2][\mask_1]\prop}[\mask_2] + \proves \wpre\expr{\Ret\var.\prop}[\mask_1]} + +\infer[wp-frame] +{}{\propB * \wpre\expr{\Ret\var.\prop}[\mask] \proves \wpre\expr{\Ret\var.\propB*\prop}[\mask]} + +\infer[wp-frame-step] +{\toval(\expr) = \bot} +{\later\propB * \wpre\expr{\Ret\var.\prop}[\mask] \proves \wpre\expr{\Ret\var.\propB*\prop}[\mask]} + +\infer[wp-bind] +{\text{$\lctx$ is a context}} +{\wpre\expr{\Ret\var. \wpre{\lctx(\ofval(\var))}{\Ret\varB.\prop}[\mask]}[\mask] \proves \wpre{\lctx(\expr)}{\Ret\varB.\prop}[\mask]} +\end{mathpar} \subsection{Lifting of operational semantics}\label{sec:lifting} ~\\\ralf{Add this.} @@ -504,7 +584,7 @@ This is entirely standard. The adequacy statement reads as follows: \begin{align*} - &\All \mask, \expr, \val, \pred, i, \state, \melt, \state', \tpool'. + &\All \mask, \expr, \val, \pred, \state, \melt, \state', \tpool'. \\&(\All n. \melt \in \mval_n) \Ra \\&( \ownPhys\state * \ownGGhost\melt \proves \wpre{\expr}{x.\; \pred(x)}[\mask]) \Ra \\&\cfg{\state}{[\expr]} \step^\ast diff --git a/docs/setup.tex b/docs/setup.tex index 404dc0c0c353c9eb040ff77179245b50ed8a186a..dffcfb29c5cc15f2ffdbe1d4624516d0c7583351 100644 --- a/docs/setup.tex +++ b/docs/setup.tex @@ -21,6 +21,7 @@ \usepackage{tabu} \usepackage{dashbox} +\usepackage{tensor} \usepackage{\basedir pftools} @@ -135,12 +136,6 @@ %% MATH SYMBOLS & NOTATION & IDENTIFIERS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% superscript to the left -\def\presuper#1#2% - {\mathop{}% - \mathopen{\vphantom{#2}}^{#1}% - \kern-\scriptspace% - #2} \DeclareMathOperator*{\Sep}{\scalerel*{\ast}{\sum}} \newcommand{\bigast}{\Sep} @@ -326,8 +321,8 @@ \newcommand{\gmapsto}{\hookrightarrow}% \newcommand{\fgmapsto}[1][\mathrm{-}]{\xhookrightarrow{#1}}% -\NewDocumentCommand\wpre{m m o}% - {{#1} \spac \{#2\}_{#3}} +\NewDocumentCommand\wpre{m m O{}}% + {{#1} \spac \prescript{}{#3}{\kern-0.2ex\{#2\}}} \newcommand{\later}{\mathord{\triangleright}} \newcommand{\always}{\Box{}} @@ -347,7 +342,7 @@ \newcommand*{\ownGhost}[2]{\boxedassert[densely dashed]{#2}[#1]} \newcommand*{\ownGGhost}[1]{\boxedassert[densely dashed]{#1}} -\newcommand{\ownPhys}[1]{\lfloor#1\rfloor} +\newcommand{\ownPhys}[1]{\textlog{Phy}(#1)} %% View Shifts \NewDocumentCommand \vsGen {O{} m O{}}% @@ -357,14 +352,14 @@ {#2}_{#1}% }{% % Two masks - \presuper{#1}{#2}^{#3} + \tensor*[^{#1}]{#2}{^{#3}} }% }}% \NewDocumentCommand \vs {O{} O{}} {\vsGen[#1]{\Rrightarrow}[#2]} \NewDocumentCommand \vsL {O{} O{}} {\vsGen[#1]{\Lleftarrow}[#2]} \NewDocumentCommand \vsE {O{} O{}} % {\vsGen[#1]{\Lleftarrow\!\!\!\Rrightarrow}[#2]} -\NewDocumentCommand \pvs {O{} O{}} {\mathord{\vsGen[#1]{{\mid\kern-0.4ex\Rrightarrow}}[#2]}} +\NewDocumentCommand \pvs {O{} O{}} {\mathord{\vsGen[#1]{{\mid\kern-0.4ex\Rrightarrow\kern-0.25ex}}[#2]\kern0.2ex}} %% Hoare Triples @@ -428,6 +423,7 @@ \newcommand{\valB}{w} \newcommand{\state}{\sigma} \newcommand{\step}{\ra} +\newcommand{\lctx}{K} \newcommand{\toval}{\mathit{val}} \newcommand{\ofval}{\mathit{expr}} diff --git a/program_logic/hoare.v b/program_logic/hoare.v index 667a5960d6601d3b1761650940169f6a8791ccc9..2d9ae68961c3792bfce79eb79ed66b3eb9879523 100644 --- a/program_logic/hoare.v +++ b/program_logic/hoare.v @@ -97,20 +97,20 @@ Lemma ht_frame_r E P Φ R e : {{ P }} e @ E {{ Φ }} ⊑ {{ P ★ R }} e @ E {{ λ v, Φ v ★ R }}. Proof. setoid_rewrite (comm _ _ R); apply ht_frame_l. Qed. -Lemma ht_frame_later_l E P R e Φ : +Lemma ht_frame_step_l E P R e Φ : to_val e = None → {{ P }} e @ E {{ Φ }} ⊑ {{ ▷ R ★ P }} e @ E {{ λ v, R ★ Φ v }}. Proof. intros; apply always_intro', impl_intro_l. rewrite always_and_sep_r -assoc (sep_and P) always_elim impl_elim_r. - by rewrite wp_frame_later_l //; apply wp_mono=>v; rewrite pvs_frame_l. + by rewrite wp_frame_step_l //; apply wp_mono=>v; rewrite pvs_frame_l. Qed. -Lemma ht_frame_later_r E P Φ R e : +Lemma ht_frame_step_r E P Φ R e : to_val e = None → {{ P }} e @ E {{ Φ }} ⊑ {{ P ★ ▷ R }} e @ E {{ λ v, Φ v ★ R }}. Proof. rewrite (comm _ _ (▷ R)%I); setoid_rewrite (comm _ _ R). - apply ht_frame_later_l. + apply ht_frame_step_l. Qed. End hoare. diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v index c87f8635f29e86f93d1532c1615737a96b4bf995..b32a0589052df2bca28a8bebabc5fa7e1b1b7214 100644 --- a/program_logic/weakestpre.v +++ b/program_logic/weakestpre.v @@ -182,7 +182,7 @@ Proof. (comm _ rR) !assoc -(assoc _ _ rR). - apply IH; eauto using uPred_weaken. Qed. -Lemma wp_frame_later_r E e Φ R : +Lemma wp_frame_step_r E e Φ R : to_val e = None → (#> e @ E {{ Φ }} ★ ▷ R) ⊑ #> e @ E {{ λ v, Φ v ★ R }}. Proof. rewrite wp_eq. intros He; uPred.unseal; split; intros n r' Hvalid (r&rR&Hr&Hwp&?). @@ -233,11 +233,11 @@ Lemma wp_value_pvs E Φ e v : Proof. intros. rewrite -wp_pvs. rewrite -wp_value //. Qed. Lemma wp_frame_l E e Φ R : (R ★ #> e @ E {{ Φ }}) ⊑ #> e @ E {{ λ v, R ★ Φ v }}. Proof. setoid_rewrite (comm _ R); apply wp_frame_r. Qed. -Lemma wp_frame_later_l E e Φ R : +Lemma wp_frame_step_l E e Φ R : to_val e = None → (▷ R ★ #> e @ E {{ Φ }}) ⊑ #> e @ E {{ λ v, R ★ Φ v }}. Proof. rewrite (comm _ (▷ R)%I); setoid_rewrite (comm _ R). - apply wp_frame_later_r. + apply wp_frame_step_r. Qed. Lemma wp_always_l E e Φ R `{!AlwaysStable R} : (R ∧ #> e @ E {{ Φ }}) ⊑ #> e @ E {{ λ v, R ∧ Φ v }}.