From 843905d8bc99525bf3da92de3f88d7c103557ef4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 7 Mar 2016 19:39:18 +0100
Subject: [PATCH] docs: give pvs and wp rules
---
docs/logic.tex | 98 ++++++++++++++++++++++++++++++++++----
docs/setup.tex | 18 +++----
program_logic/hoare.v | 8 ++--
program_logic/weakestpre.v | 6 +--
4 files changed, 103 insertions(+), 27 deletions(-)
diff --git a/docs/logic.tex b/docs/logic.tex
index 0af9326d8..e12cdd02c 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 404dc0c0c..dffcfb29c 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 667a5960d..2d9ae6896 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 c87f8635f..b32a05890 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 }}.
--
GitLab