diff --git a/docs/algebra.tex b/docs/algebra.tex index 7bfc5d4d6615abdc10396c13d08af2fc9748b88b..3295ade48b2e28050a976a3cbe9061587b77d659 100644 --- a/docs/algebra.tex +++ b/docs/algebra.tex @@ -78,10 +78,10 @@ where the $n$-equivalence at the bottom is meant to apply to the pairs of elemen In other words, extension carries the decomposition of $\meltB$ into $\meltB_1$ and $\meltB_2$ over the $n$-equivalence of $\melt$ and $\meltB$, and yields a corresponding decomposition of $\melt$ into $\melt_1$ and $\melt_2$. This operation is needed to prove that $\later$ commutes with existential quantification and separating conjunction: \begin{mathpar} - \axiom{\later(\Exists\var:\sort. \prop) \Lra \Exists\var:\sort. \later\prop} + \axiom{\later(\Exists\var:\type. \prop) \Lra \Exists\var:\type. \later\prop} \and\axiom{\later (\prop * \propB) \Lra \later\prop * \later\propB} \end{mathpar} -(This assumes that the sort $\sort$ is non-empty.) +(This assumes that the type $\type$ is non-empty.) %%% Local Variables: diff --git a/docs/derived.tex b/docs/derived.tex index b907e7dea6b510cf9bf7273a270e0bcd2c618f32..1953032d07abd07d343f26e1e6006cfce3e6b0ab 100644 --- a/docs/derived.tex +++ b/docs/derived.tex @@ -1,3 +1,277 @@ +\section{Derived Program logic}\label{sec:proglog} + +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})} +\qquad\qquad +\begin{aligned} +\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 +\end{aligned} + +We write just one mask for a view shift when $\mask_1 = \mask_2$. +The convention for omitted masks is generous: +An omitted $\mask$ is $\top$ for Hoare triples and $\emptyset$ for view shifts. + +% PDS: We're repeating ourselves. We gave Γ conventions and we're about to give Θ conventions. Also, the scope of "Below" is unclear. +% Below, we implicitly assume the same context for all judgements which don't have an explicit context at \emph{all} pre-conditions \emph{and} the conclusion. + +Henceforward, we implicitly assume a proof context, $\pfctx$, is added to every constituent of the rules. +Generally, this is an arbitrary proof context. +We write $\provesalways$ to denote judgments that can only be extended with a boxed proof context. + +\ralf{Give the actual base rules from the Coq development instead} + +\subsection{Hoare triples} +\begin{mathpar} +\inferH{Ret} + {} + {\hoare{\TRUE}{\valB}{\Ret\val. \val = \valB}[\mask]} +\and +\inferH{Bind} + {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask] \\ + \All \val. \hoare{\propB}{K[\val]}{\Ret\valB.\propC}[\mask]} + {\hoare{\prop}{K[\expr]}{\Ret\valB.\propC}[\mask]} +\and +\inferH{Csq} + {\prop \vs \prop' \\ + \hoare{\prop'}{\expr}{\Ret\val.\propB'}[\mask] \\ + \All \val. \propB' \vs \propB} + {\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask]} +\and +\inferH{Frame} + {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask]} + {\hoare{\prop * \propC}{\expr}{\Ret\val. \propB * \propC}[\mask \uplus \mask']} +\and +\inferH{AFrame} + {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask] \and \text{$\expr$ not a value} + } + {\hoare{\prop * \later\propC}{\expr}{\Ret\val. \propB * \propC}[\mask \uplus \mask']} +% \and +% \inferH{Fork} +% {\hoare{\prop}{\expr}{\Ret\any. \TRUE}[\top]} +% {\hoare{\later\prop * \later\propB}{\fork{\expr}}{\Ret\val. \val = \textsf{fRet} \land \propB}[\mask]} +\and +\inferH{ACsq} + {\prop \vs[\mask \uplus \mask'][\mask] \prop' \\ + \hoare{\prop'}{\expr}{\Ret\val.\propB'}[\mask] \\ + \All\val. \propB' \vs[\mask][\mask \uplus \mask'] \propB \\ + \physatomic{\expr} + } + {\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \mask']} +\end{mathpar} + +\subsection{View shifts} + +\begin{mathpar} +\inferH{NewInv} + {\infinite(\mask)} + {\later{\prop} \vs[\mask] \exists \iname\in\mask.\; \knowInv{\iname}{\prop}} +\and +\inferH{FpUpd} + {\melt \mupd \meltsB} + {\ownGGhost{\melt} \vs \exists \meltB \in \meltsB.\; \ownGGhost{\meltB}} +\and +\inferH{VSTrans} + {\prop \vs[\mask_1][\mask_2] \propB \and \propB \vs[\mask_2][\mask_3] \propC \and \mask_2 \subseteq \mask_1 \cup \mask_3} + {\prop \vs[\mask_1][\mask_3] \propC} +\and +\inferH{VSImp} + {\always{(\prop \Ra \propB)}} + {\prop \vs[\emptyset] \propB} +\and +\inferH{VSFrame} + {\prop \vs[\mask_1][\mask_2] \propB} + {\prop * \propC \vs[\mask_1 \uplus \mask'][\mask_2 \uplus \mask'] \propB * \propC} +\and +\inferH{VSTimeless} + {\timeless{\prop}} + {\later \prop \vs \prop} +\and +\axiomH{InvOpen} + {\knowInv{\iname}{\prop} \proves \TRUE \vs[\{ \iname \} ][\emptyset] \later \prop} +\and +\axiomH{InvClose} + {\knowInv{\iname}{\prop} \proves \later \prop \vs[\emptyset][\{ \iname \} ] \TRUE } +\end{mathpar} + +\vspace{5pt} +Note that $\timeless{\prop}$ means that $\prop$ does not depend on the step index. +Furthermore, $$\melt \mupd \meltsB \eqdef \always{\All \melt_f. \melt \sep \melt_f \Ra \Exists \meltB \in \meltsB. \meltB \sep \melt_f}$$ + +\subsection{Derived rules} + +\paragraph{Derived structural rules.} +The following are easily derived by unfolding the sugar for Hoare triples and view shifts. +\begin{mathpar} +\inferHB{Disj} + {\hoare{\prop}{\expr}{\Ret\val.\propC}[\mask] \and \hoare{\propB}{\expr}{\Ret\val.\propC}[\mask]} + {\hoare{\prop \lor \propB}{\expr}{\Ret\val.\propC}[\mask]} +\and +\inferHB{VSDisj} + {\prop \vs[\mask_1][\mask_2] \propC \and \propB \vs[\mask_1][\mask_2] \propC} + {\prop \lor \propB \vs[\mask_1][\mask_2] \propC} +\and +\inferHB{Exist} + {\All \var. \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask]} + {\hoare{\Exists \var. \prop}{\expr}{\Ret\val.\propB}[\mask]} +\and +\inferHB{VSExist} + {\All \var. (\prop \vs[\mask_1][\mask_2] \propB)} + {(\Exists \var. \prop) \vs[\mask_1][\mask_2] \propB} +\and +\inferHB{BoxOut} + {\always\propB \provesalways \hoare{\prop}{\expr}{\Ret\val.\propC}[\mask]} + {\hoare{\prop \land \always{\propB}}{\expr}{\Ret\val.\propC}[\mask]} +\and +\inferHB{VSBoxOut} + {\always\propB \provesalways \prop \vs[\mask_1][\mask_2] \propC} + {\prop \land \always{\propB} \vs[\mask_1][\mask_2] \propC} + \and +\inferH{False} + {} + {\hoare{\FALSE}{\expr}{\Ret \val. \prop}[\mask]} +\and +\inferH{VSFalse} + {} + {\FALSE \vs[\mask_1][\mask_2] \prop } +\end{mathpar} +The proofs all follow the same pattern, so we only show two of them in detail. +\begin{proof}[Proof of \ruleref{Exist}] + After unfolding the syntactic sugar for Hoare triples and removing the boxes from premise and conclusion, our goal becomes + $+ (\Exists \var. \prop(\var)) \Ra \dynA{\expr}{\Lam\val. \propB}{\mask} +$ + (remember that $\var$ is free in $\prop$) and the premise reads + $+ \All \var. \prop(\var) \Ra \dynA{\expr}{\Lam\val. \propB}{\mask}. +$ + Let $\var$ be given and assume $\prop(\var)$. + To show $\dynA{\expr}{\Lam\val. \propB}{\mask}$, apply the premise to $\var$ and $\prop(\var)$. + + For the other direction, assume + $+ \hoare{\Exists \var. \prop(\var)}{\expr}{\Ret\val. \propB}[\mask] +$ + and let $\var$ be given. + We have to show $\hoare{\prop(\var)}{\expr}{\Ret\val. \propB}[\mask]$. + This trivially follows from \ruleref{Csq} with $\prop(\var) \Ra \Exists \var. \prop(\var)$. +\end{proof} + +\begin{proof}[Proof of \ruleref{BoxOut}] + After unfolding the syntactic sugar for Hoare triples, our goal becomes + $$\label{eq:boxin:goal} + \always\pfctx \proves \always\bigl(\prop\land\always \propB \Ra \dynA{\expr}{\Lam\val. \propC}{\mask}\bigr) +$$ + while our premise reads + $$\label{eq:boxin:as} + \always\pfctx, \always\propB \proves \always(\prop \Ra \dynA{\expr}{\Lam\val. \propC}{\mask}) +$$ + By the introduction rules for $\always$ and implication, it suffices to show + $(\always\pfctx), \prop,\always \propB \proves \dynA{\expr}{\Lam\val. \propC}{\mask}$ + By modus ponens and \ruleref{Necessity}, it suffices to show~\eqref{eq:boxin:as}, which is exactly our assumption. + + For the other direction, assume~\eqref{eq:boxin:goal}. We have to show~\eqref{eq:boxin:as}. By \ruleref{AlwaysIntro} and implication introduction, it suffices to show + $(\always\pfctx), \prop,\always \propB \proves \dynA{\expr}{\Lam\val. \propC}{\mask}$ + which easily follows from~\eqref{eq:boxin:goal}. +\end{proof} + +\paragraph{Derived rules for invariants.} +Invariants can be opened around atomic expressions and view shifts. + +\begin{mathpar} +\inferH{Inv} + {\hoare{\later{\propC} * \prop } + {\expr} + {\Ret\val. \later{\propC} * \propB }[\mask] + \and \physatomic{\expr} + } + {\knowInv{\iname}{\propC} \proves \hoare{\prop} + {\expr} + {\Ret\val. \propB}[\mask \uplus \{ \iname \}] + } +\and +\inferH{VSInv} + {\later{\prop} * \propB \vs[\mask_1][\mask_2] \later{\prop} * \propC} + {\knowInv{\iname}{\prop} \proves \propB \vs[\mask_1 \uplus \{ \iname \}][\mask_2 \uplus \{ \iname \}] \propC} +\end{mathpar} + +\begin{proof}[Proof of \ruleref{Inv}] + Use \ruleref{ACsq} with $\mask_1 \eqdef \mask \cup \{\iname\}$, $\mask_2 \eqdef \mask$. + The view shifts are obtained by \ruleref{InvOpen} and \ruleref{InvClose} with framing of $\mask$ and $\prop$ or $\propB$, respectively. +\end{proof} + +\begin{proof}[Proof of \ruleref{VSInv}] +Analogous to the proof of \ruleref{Inv}, using \ruleref{VSTrans} instead of \ruleref{ACsq}. +\end{proof} + +\subsubsection{Unsound rules} + +Some rule suggestions (or rather, wishes) keep coming up, which are unsound. We collect them here. +\begin{mathpar} + \infer + {P \vs Q} + {\later P \vs \later Q} + \and + \infer + {\later(P \vs Q)} + {\later P \vs \later Q} +\end{mathpar} + +Of course, the second rule implies the first, so let's focus on that. +Since implications work under $\later$, from $\later P$ we can get $\later \pvs{Q}$. +If we now try to prove $\pvs{\later Q}$, we will be unable to establish world satisfaction in the new world: +We have no choice but to use $\later \pvs{Q}$ at one step index below what we are operating on (because we have it under a $\later$). +We can easily get world satisfaction for that lower step-index (by downwards-closedness of step-indexed predicates). +We can, however, not make much use of the world satisfaction that we get out, becaase it is one step-index too low. + +\subsection{Adequacy} + +The adequacy statement reads as follows: +\begin{align*} + &\All \mask, \expr, \val, \pred, i, \state, \state', \tpool'. + \\&( \proves \hoare{\ownPhys\state}{\expr}{x.\; \pred(x)}[\mask]) \implies + \\&\cfg{\state}{[i \mapsto \expr]} \step^\ast + \cfg{\state'}{[i \mapsto \val] \uplus \tpool'} \implies + \\&\pred(\val) +\end{align*} +where $\pred$ can mention neither resources nor invariants. + +\subsection{Axiom lifting}\label{sec:lifting} + +The following lemmas help in proving axioms for a particular language. +The first applies to expressions with side-effects, and the second to side-effect-free expressions. +\dave{Update the others, and the example, wrt the new treatment of $\predB$.} +\begin{align*} + &\All \expr, \state, \pred, \prop, \propB, \mask. \\ + &\textlog{reducible}(e) \implies \\ + &(\All \expr', \state'. \cfg{\state}{\expr} \step \cfg{\state'}{\expr'} \implies \pred(\expr', \state')) \implies \\ + &{} \proves \bigl( (\All \expr', \state'. \pred (\expr', \state') \Ra \hoare{\prop}{\expr'}{\Ret\val. \propB}[\mask]) \Ra \hoare{ \later \prop * \ownPhys{\state} }{\expr}{\Ret\val. \propB}[\mask] \bigr) \\ + \quad\\ + &\All \expr, \pred, \prop, \propB, \mask. \\ + &\textlog{reducible}(e) \implies \\ + &(\All \state, \expr_2, \state_2. \cfg{\state}{\expr} \step \cfg{\state_2}{\expr_2} \implies \state_2 = \state \land \pred(\expr_2)) \implies \\ + &{} \proves \bigl( (\All \expr'. \pred(\expr') \Ra \hoare{\prop}{\expr'}{\Ret\val. \propB}[\mask]) \Ra \hoare{\later\prop}{\expr}{\Ret\val. \propB}[\mask] \bigr) +\end{align*} +Note that $\pred$ is a meta-logic predicate---it does not depend on any world or resources being owned. + +The following specializations cover all cases of a heap-manipulating lambda calculus like $F_{\mu!}$. +\begin{align*} + &\All \expr, \expr', \prop, \propB, \mask. \\ + &\textlog{reducible}(e) \implies \\ + &(\All \state, \expr_2, \state_2. \cfg{\state}{\expr} \step \cfg{\state_2}{\expr_2} \implies \state_2 = \state \land \expr_2 = \expr') \implies \\ + &{} \proves (\hoare{\prop}{\expr'}{\Ret\val. \propB}[\mask] \Ra \hoare{\later\prop}{\expr}{\Ret\val. \propB}[\mask] ) \\ + \quad \\ + &\All \expr, \state, \pred, \mask. \\ + &\textlog{atomic}(e) \implies \\ + &\bigl(\All \expr_2, \state_2. \cfg{\state}{\expr} \step \cfg{\state_2}{\expr_2} \implies \pred(\expr_2, \state_2)\bigr) \implies \\ + &{} \proves (\hoare{ \ownPhys{\state} }{\expr}{\Ret\val. \Exists\state'. \ownPhys{\state'} \land \pred(\val, \state') }[\mask] ) +\end{align*} +The first is restricted to deterministic pure reductions, like $\beta$-reduction. +The second is suited to proving triples for (possibly non-deterministic) atomic expressions; for example, with $\expr \eqdef \;!\ell$ (dereferencing $\ell$) and $\state \eqdef h \mtimes \ell \mapsto \valB$ and $\pred(\val, \state') \eqdef \state' = (h \mtimes \ell \mapsto \valB) \land \val = \valB$, one obtains the axiom $\All h, \ell, \valB. \hoare{\ownPhys{h \mtimes \ell \mapsto \valB}}{!\ell}{\Ret\val. \val = \valB \land \ownPhys{h \mtimes \ell \mapsto \valB} }$. +%Axioms for CAS-like operations can be obtained by first deriving rules for the two possible cases, and then using the disjunction rule. + + \section{Derived constructions} In this section we describe some constructions that we will use throughout the rest of the appendix. diff --git a/docs/iris.tex b/docs/iris.tex index bc3ff6ac6ae02f6e983ac4c8e9f7ab2132fb4213..2bf008cfbab53661405adee44b51a3e00461a1dd 100644 --- a/docs/iris.tex +++ b/docs/iris.tex @@ -30,10 +30,9 @@ \input{algebra} \endgroup\clearpage\begingroup \input{constructions} -% temporarily disabled, to generate the Iris 2.0 appendix -%\endgroup\clearpage\begingroup -%\input{logic} -%\endgroup\clearpage\begingroup +\endgroup\clearpage\begingroup +\input{logic} +\endgroup\clearpage\begingroup %\input{model} %\endgroup\clearpage\begingroup %\input{derived} diff --git a/docs/logic.tex b/docs/logic.tex index e991d07a85c27d8235f2c894511244b671b4ae05..396d3ffc8b6f86eec51b445488c44ee6501ba256 100644 --- a/docs/logic.tex +++ b/docs/logic.tex @@ -1,113 +1,93 @@ +\section{Language} -\section{Parameters to the logic} - +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 \begin{itemize} -% \item A set \textdom{Exp} of \emph{expressions} (metavariable $\expr$) with a -% subset \textdom{Val} of values ($\val$). We assume that if $\expr$ is an -% expression then so is $\fork{\expr}$. We moreover assume a value -% \textsf{fRet} (giving the intended return value of a fork), and we assume that -% \begin{align*} -% \fork{\expr} &\notin \textdom{Val} \\ -% \fork{\expr_1} = \fork{\expr_2} &\implies \expr_1 = \expr_2 -% \end{align*} -\item A set $\textdom{Ectx}$ of \emph{evaluation contexts} ($\ectx$) that includes the empty context $[\; ]$, - a plugging operation $\ectx[\expr]$ that produces an expression, and context composition $\circ$ - satisfying the following axioms: - \begin{align*} - [\; ][ \expr ] &= \expr \\ - \ectx_1[\ectx_2[\expr]] &= (\ectx_1 \circ \ectx_2) [\expr] \\ - \ectx_1[\expr] = \ectx_2[\expr] &\implies \ectx_1 = \ectx_2 \\ - \ectx[\expr_1] = \ectx[\expr_2] &\implies \expr_1 = \expr_2 \\ - \ectx_1 \circ \ectx_2 = [\; ] &\implies \ectx_1 = \ectx_2 = [\; ] \\ - \ectx[\expr] \in \textdom{Val} &\implies \ectx = [\;] \\ -% \ectx[\expr] = \fork{\expr'} &\implies \ectx = [\;] - \end{align*} - -\item A set \textdom{State} of shared machine states (\eg heaps), metavariable $\state$. -\item An \emph{atomic stepping relation} $- (- \step -) \subseteq (\textdom{State} \times \textdom{Exp}) \times (\textdom{State} \times \textdom{Exp}) -$ -and notions of an expression to be \emph{reducible} or \emph{stuck}, such that -\begin{align*} - \textlog{reducible}(\expr) &\iff \Exists \state, \expr_2, \state_2. \cfg{\state}{\expr} \step \cfg{\state_2}{\expr_2} \\ -% \textlog{stuck}(\expr) &\iff \All \ectx, \expr'. \expr = \ectx[\expr'] \implies - \lnot \textlog{reducible}(\expr') -\end{align*} -and the following hold -% \begin{align*} -% &\textlog{stuck}(\fork{\expr})& \\ -% &\textlog{stuck}(\val)&\\ -% &\ectx[\expr] = \ectx'[\expr'] \implies \textlog{reducible}(\expr') \implies -% \expr \notin \textdom{Val} \implies \Exists \ectx''. \ectx' = \ectx \circ \ectx'' &\mbox{(step-by-value)} \\ -% &\ectx[\expr] = \ectx'[\fork{\expr'}] \implies -% \expr \notin \textdom{Val} \implies \Exists \ectx''. \ectx' = \ectx \circ \ectx'' &\mbox{(fork-by-value)} \\ -% \end{align*} - -\item A predicate \textlog{atomic} on expressions satisfying - \begin{align*} - &\textlog{atomic}(\expr) \implies \textlog{reducible}(\expr) &\\ - &\textlog{atomic}(\expr) \implies \cfg{\state}{\expr} \step \cfg{\state_2}{\expr_2} \implies \expr_2 \in \textdom{Val} &\mbox{(atomic-step)} - \end{align*} - - -\item A commutative monoid with zero, $M$. -That is, a set $\mcar{M}$ with two distinguished elements $\mzero$ (zero, undefined) and $\munit$ (one, unit) and an operation $\mtimes$ (times, combine) such that -\begin{align*} - \melt \mtimes \meltB &= \meltB \mtimes \melt \\ - \munit \mtimes \melt &= \melt \\ - (\melt \mtimes \meltB) \mtimes \meltC &= \melt \mtimes (\meltB \mtimes \meltC) \\ - \mzero \mtimes \melt &= \mzero \\ - \mzero &\neq \munit -\end{align*} -Let $\mcarp{M} \eqdef |\monoid| \setminus \{\mzero\}$. - -\item Arbitrary additional types and terms. +\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} +\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{()})$ + We will write $\expr_1, \state_1 \step \expr_2, \state_2$ for $\expr_1, \state_1 \step \expr_2, \state_2, ()$. \\ + 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. +\item All values are stuck: +$\expr, \_ \step \_, \_, \_ \Ra \toval(\expr) = \bot$ +\item There is a predicate defining \emph{atomic} expressions satisfying +\let\oldcr\cr +\begin{mathpar} + {\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 + \end{inbox} +}} +\end{mathpar} +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} -\section{The concurrent language} +\subsection{The concurrent language} + +For any language $\Lang$, we define the corresponding thread-pool semantics. \paragraph{Machine syntax} $- \tpool \in \textdom{ThreadPool} \eqdef \mathbb{N} \fpfn \textdom{Exp} + \tpool \in \textdom{ThreadPool} \eqdef \bigcup_n \textdom{Exp}^n$ -\judgment{Machine reduction} {\cfg{\state}{\tpool} \step - \cfg{\state'}{\tpool'}} +\judgment{Machine reduction} {\cfg{\tpool}{\state} \step + \cfg{\tpool'}{\state'}} \begin{mathpar} \infer - {\cfg{\state}{\expr} \step \cfg{\state'}{\expr'}} - {\cfg{\state}{\tpool [i \mapsto \ectx[\expr]]} \step - \cfg{\state'}{\tpool [i \mapsto \ectx[\expr']]}} -% \and -% \infer -% {} -% {\cfg{\state}{\tpool [i \mapsto \ectx[\fork{\expr}]]} \step -% \cfg{\state}{\tpool [i \mapsto \ectx[\textsf{fRet}]] [j \mapsto \expr]}} + {\expr_1, \state_1 \step \expr_2, \state_2, \expr' \and \expr' \neq ()} + {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state} \step + \cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus [\expr']}{\state'}} +\and\infer + {\expr_1, \state_1 \step \expr_2, \state_2} + {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state} \step + \cfg{\tpool \dplus [\expr_2] \dplus \tpool'}{\state'}} \end{mathpar} -\section{Syntax} -\subsection{Grammar}\label{sec:grammar} +\section{The logic} + +To instantiate Iris, you need to define the following parameters: +\begin{itemize} +\item A language $\Lang$ +\item A locally contractive functor $\iFunc : \COFEs \to \CMRAs$ defining the ghost state +\end{itemize} -\paragraph{Signatures.} -We use a signature to account syntactically for the logic's parameters. -A \emph{signature} $\Sig = (\SigType, \SigFn)$ comprises a set +\noindent +As usual for higher-order logics, you can furthermore pick a \emph{signature} $\Sig = (\SigType, \SigFn, \SigAx)$ to add more types, symbols and axioms to the language. +You have to make sure that $\SigType$ includes the base types: $- \SigType \supseteq \{ \textsort{Val}, \textsort{Exp}, \textsort{Ectx}, \textsort{State}, \textsort{Monoid}, \textsort{InvName}, \textsort{InvMask}, \Prop \} + \SigType \supseteq \{ \textsort{Val}, \textsort{Expr}, \textsort{State}, \textsort{M}, \textsort{InvName}, \textsort{InvMask}, \Prop \}$ -of base types (or base \emph{sorts}) and a set $\SigFn$ of typed function symbols. -This means that each function symbol has an associated \emph{arity} comprising a natural number $n$ and an ordered list of $n+1$ base types. +Elements of $\SigType$ are ranged over by $\sigtype$. + +Each function symbol in $\SigFn$ has an associated \emph{arity} comprising a natural number $n$ and an ordered list of $n+1$ types $\type$ (the grammar of $\type$ is defined below, and depends only on $\SigType$). We write $\sigfn : \type_1, \dots, \type_n \to \type_{n+1} \in \SigFn$ to express that $\sigfn$ is a function symbol with the indicated arity. -\dave{Say something not-too-shabby about adequacy: We don't spell out what it means.} + +Furthermore, $\SigAx$ is a set of \emph{axioms}, that is, terms $\term$ of type $\Prop$. +Again, the grammar of terms and their typing rules are defined below, and depends only on $\SigType$ and $\SigFn$, not on $\SigAx$. +Elements of $\SigAx$ are ranged over by $\sigax$. + +\section{Syntax} + +\subsection{Grammar}\label{sec:grammar} \paragraph{Syntax.} Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\textdom{Var}$ of variables (ranged over by metavariables $x$, $y$, $z$): \begin{align*} + \type ::={}& + \sigtype \mid + \unitsort \mid + \type \times \type \mid + \type \to \type +\0.4em] \term, \prop, \pred ::={}& x \mid \sigfn(\term_1, \dots, \term_n) \mid @@ -115,14 +95,14 @@ Iris syntax is built up from a signature \Sig and a countably infinite set \t (\term, \term) \mid \pi_i\; \term \mid \Lam x.\term \mid - \term\;\term \mid + \term(\term) \mid \mzero \mid \munit \mid \term \mtimes \term \mid \\& \FALSE \mid \TRUE \mid - \term =_\sort \term \mid + \term =_\type \term \mid \prop \Ra \prop \mid \prop \land \prop \mid \prop \lor \prop \mid @@ -130,8 +110,8 @@ Iris syntax is built up from a signature \Sig and a countably infinite set \t \prop \wand \prop \mid \\& \MU \var. \pred \mid - \Exists \var:\sort. \prop \mid - \All \var:\sort. \prop \mid + \Exists \var:\type. \prop \mid + \All \var:\type. \prop \mid \\& \knowInv{\term}{\prop} \mid \ownGGhost{\term} \mid @@ -139,66 +119,58 @@ Iris syntax is built up from a signature \Sig and a countably infinite set \t \always\prop \mid {\later\prop} \mid \pvsA{\prop}{\term}{\term} \mid - \dynA{\term}{\pred}{\term} \mid - \timeless{\prop} -\\[0.4em] - \sort ::={}& - \type \mid - \unitsort \mid - \sort \times \sort \mid - \sort \to \sort + \dynA{\term}{\pred}{\term} \end{align*} Recursive predicates must be \emph{guarded}: in \MU \var. \pred, the variable \var can only appear under the later \later modality. \paragraph{Metavariable conventions.} -We introduce additional metavariables ranging over terms and generally let the choice of metavariable indicate the term's sort: +We introduce additional metavariables ranging over terms and generally let the choice of metavariable indicate the term's type: \[ \begin{array}{r|l} - \text{metavariable} & \text{sort} \\\hline + \text{metavariable} & \text{type} \\\hline \term, \termB & \text{arbitrary} \\ \val, \valB & \textsort{Val} \\ \expr & \textsort{Exp} \\ - \ectx & \textsort{Ectx} \\ \state & \textsort{State} \\ \end{array} \qquad\qquad \begin{array}{r|l} - \text{metavariable} & \text{sort} \\\hline + \text{metavariable} & \text{type} \\\hline \iname & \textsort{InvName} \\ \mask & \textsort{InvMask} \\ - \melt, \meltB & \textsort{Monoid} \\ + \melt, \meltB & \textsort{M} \\ \prop, \propB, \propC & \Prop \\ - \pred, \predB, \predC & \sort\to\Prop \text{ (when \sort is clear from context)} \\ + \pred, \predB, \predC & \type\to\Prop \text{ (when \type is clear from context)} \\ \end{array} \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. \subsection{Types}\label{sec:types} Iris terms are simply-typed. -The judgment $\vctx \proves_\Sig \wtt{\term}{\sort}$ expresses that, in signature $\Sig$ and variable context $\vctx$, the term $\term$ has sort $\sort$. -In giving the rules for this judgment, we omit the signature (which does not change). +The judgment $\vctx \proves \wtt{\term}{\type}$ expresses that, in variable context $\vctx$, the term $\term$ has type $\type$. -A variable context, $\vctx = x_1:\sort_1, \dots, x_n:\sort_n$, declares a list of variables and their sorts. -In writing $\vctx, x:\sort$, we presuppose that $x$ is not already declared in $\vctx$. +A variable context, $\vctx = x_1:\type_1, \dots, x_n:\type_n$, declares a list of variables and their types. +In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $\vctx$. -\judgment{Well-typed terms}{\vctx \proves_\Sig \wtt{\term}{\sort}} +\judgment{Well-typed terms}{\vctx \proves_\Sig \wtt{\term}{\type}} \begin{mathparpagebreakable} %%% variables and function symbols - \axiom{x : \sort \proves \wtt{x}{\sort}} + \axiom{x : \type \proves \wtt{x}{\type}} \and - \infer{\vctx \proves \wtt{\term}{\sort}} - {\vctx, x:\sort' \proves \wtt{\term}{\sort}} + \infer{\vctx \proves \wtt{\term}{\type}} + {\vctx, x:\type' \proves \wtt{\term}{\type}} \and - \infer{\vctx, x:\sort', y:\sort' \proves \wtt{\term}{\sort}} - {\vctx, x:\sort' \proves \wtt{\term[x/y]}{\sort}} + \infer{\vctx, x:\type', y:\type' \proves \wtt{\term}{\type}} + {\vctx, x:\type' \proves \wtt{\term[x/y]}{\type}} \and - \infer{\vctx_1, x:\sort', y:\sort'', \vctx_2 \proves \wtt{\term}{\sort}} - {\vctx_1, x:\sort'', y:\sort', \vctx_2 \proves \wtt{\term[y/x,x/y]}{\sort}} + \infer{\vctx_1, x:\type', y:\type'', \vctx_2 \proves \wtt{\term}{\type}} + {\vctx_1, x:\type'', y:\type', \vctx_2 \proves \wtt{\term[y/x,x/y]}{\type}} \and \infer{ \vctx \proves \wtt{\term_1}{\type_1} \and @@ -212,35 +184,33 @@ In writing $\vctx, x:\sort$, we presuppose that $x$ is not already declared in $\and \axiom{\vctx \proves \wtt{\unitval}{\unitsort}} \and - \infer{\vctx \proves \wtt{\term}{\sort_1} \and \vctx \proves \wtt{\termB}{\sort_2}} - {\vctx \proves \wtt{(\term,\termB)}{\sort_1 \times \sort_2}} + \infer{\vctx \proves \wtt{\term}{\type_1} \and \vctx \proves \wtt{\termB}{\type_2}} + {\vctx \proves \wtt{(\term,\termB)}{\type_1 \times \type_2}} \and - \infer{\vctx \proves \wtt{\term}{\sort_1 \times \sort_2} \and i \in \{1, 2\}} - {\vctx \proves \wtt{\pi_i\,\term}{\sort_i}} + \infer{\vctx \proves \wtt{\term}{\type_1 \times \type_2} \and i \in \{1, 2\}} + {\vctx \proves \wtt{\pi_i\,\term}{\type_i}} %%% functions \and - \infer{\vctx, x:\sort \proves \wtt{\term}{\sort'}} - {\vctx \proves \wtt{\Lam x. \term}{\sort \to \sort'}} + \infer{\vctx, x:\type \proves \wtt{\term}{\type'}} + {\vctx \proves \wtt{\Lam x. \term}{\type \to \type'}} \and \infer - {\vctx \proves \wtt{\term}{\sort \to \sort'} \and \wtt{\termB}{\sort}} - {\vctx \proves \wtt{\term\;\termB}{\sort'}} + {\vctx \proves \wtt{\term}{\type \to \type'} \and \wtt{\termB}{\type}} + {\vctx \proves \wtt{\term(\termB)}{\type'}} %%% monoids \and - \axiom{\vctx \proves \wtt{\mzero}{\textsort{Monoid}}} -\and - \axiom{\vctx \proves \wtt{\munit}{\textsort{Monoid}}} + \infer{\vctx \proves \wtt{\term}{\textsort{M}}}{\vctx \proves \wtt{\munit(\term)}{\textsort{M}}} \and - \infer{\vctx \proves \wtt{\melt}{\textsort{Monoid}} \and \vctx \proves \wtt{\meltB}{\textsort{Monoid}}} - {\vctx \proves \wtt{\melt \mtimes \meltB}{\textsort{Monoid}}} + \infer{\vctx \proves \wtt{\melt}{\textsort{M}} \and \vctx \proves \wtt{\meltB}{\textsort{M}}} + {\vctx \proves \wtt{\melt \mtimes \meltB}{\textsort{M}}} %%% props and predicates \\ \axiom{\vctx \proves \wtt{\FALSE}{\Prop}} \and \axiom{\vctx \proves \wtt{\TRUE}{\Prop}} \and - \infer{\vctx \proves \wtt{\term}{\sort} \and \vctx \proves \wtt{\termB}{\sort}} - {\vctx \proves \wtt{\term =_\sort \termB}{\Prop}} + \infer{\vctx \proves \wtt{\term}{\type} \and \vctx \proves \wtt{\termB}{\type}} + {\vctx \proves \wtt{\term =_\type \termB}{\Prop}} \and \infer{\vctx \proves \wtt{\prop}{\Prop} \and \vctx \proves \wtt{\propB}{\Prop}} {\vctx \proves \wtt{\prop \Ra \propB}{\Prop}} @@ -258,17 +228,17 @@ In writing$\vctx, x:\sort$, we presuppose that$x$is not already declared in$ {\vctx \proves \wtt{\prop \wand \propB}{\Prop}} \and \infer{ - \vctx, \var:\sort\to\Prop \proves \wtt{\pred}{\sort\to\Prop} \and + \vctx, \var:\type\to\Prop \proves \wtt{\pred}{\type\to\Prop} \and \text{$\var$ is guarded in $\pred$} }{ - \vctx \proves \wtt{\MU \var. \pred}{\sort\to\Prop} + \vctx \proves \wtt{\MU \var. \pred}{\type\to\Prop} } \and - \infer{\vctx, x:\sort \proves \wtt{\prop}{\Prop}} - {\vctx \proves \wtt{\Exists x:\sort. \prop}{\Prop}} + \infer{\vctx, x:\type \proves \wtt{\prop}{\Prop}} + {\vctx \proves \wtt{\Exists x:\type. \prop}{\Prop}} \and - \infer{\vctx, x:\sort \proves \wtt{\prop}{\Prop}} - {\vctx \proves \wtt{\All x:\sort. \prop}{\Prop}} + \infer{\vctx, x:\type \proves \wtt{\prop}{\Prop}} + {\vctx \proves \wtt{\All x:\type. \prop}{\Prop}} \and \infer{ \vctx \proves \wtt{\prop}{\Prop} \and @@ -277,7 +247,7 @@ In writing $\vctx, x:\sort$, we presuppose that $x$ is not already declared in $\vctx \proves \wtt{\knowInv{\iname}{\prop}}{\Prop} } \and - \infer{\vctx \proves \wtt{\melt}{\textsort{Monoid}}} + \infer{\vctx \proves \wtt{\melt}{\textsort{M}}} {\vctx \proves \wtt{\ownGGhost{\melt}}{\Prop}} \and \infer{\vctx \proves \wtt{\state}{\textsort{State}}} @@ -304,33 +274,28 @@ In writing$\vctx, x:\sort$, we presuppose that$x$is not already declared in$ }{ \vctx \proves \wtt{\dynA{\expr}{\pred}{\mask}}{\Prop} } -\and - \infer{ - \vctx \proves \wtt{\prop}{\Prop} - }{ - \vctx \proves \wtt{\timeless{\prop}}{\Prop} - } \end{mathparpagebreakable} +\subsection{Timeless Propositions} + +Some propositions are \emph{timeless}, which intuitively means that step-indexing does not affect them. +This is a \emph{meta-level} assertions about propositions, defined by the following judgment. -\section{Base logic} +\judgment{Timeless Propositions}{\timeless{P}} +\ralf{Define a judgment that defines them.} + +\subsection{Base logic} + +\ralf{Go on checking below.} 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. Axioms $\prop \Ra \propB$ stand for judgments $\vctx \mid \cdot \proves \prop \Ra \propB$ with no assumptions. (Bi-implications are analogous.) -% \subsubsection{Judgments} -% -% Proof rules implicitly assume well-sortedness. - -% e\subsection{Laws of intuitionistic higher-order logic with guarded recursion over a simply-typed lambda calculus}\label{sec:HOL} - +\paragraph{Laws of intuitionistic higher-order logic.} This is entirely standard. -Soundness follows from the theorem that ${\cal U}(\any, \textdom{Prop}) -: {\cal U}^{\textrm{op}} \to \textrm{Poset}$ is a hyperdoctrine. - \begin{mathpar} \inferH{Asm} {\prop \in \pfctx} @@ -421,7 +386,7 @@ Soundness follows from the theorem that ${\cal U}(\any, \textdom{Prop}) {\pfctx \proves \term \in \pred[\mu\var \in \Pred(\sort). \pred/\var]} \end{mathpar} -\subsection{Axioms from the logic of (affine) bunched implications} +\paragraph{Laws of (affine) bunched implications.} \begin{mathpar} \begin{array}{rMcMl} \prop * \propB &\Lra& \propB * \prop \\ @@ -452,7 +417,7 @@ Soundness follows from the theorem that${\cal U}(\any, \textdom{Prop}) {\pfctx, \prop * \propB \proves \propC} \end{mathpar} -\subsection{Laws for ghosts and physical resources} +\paragraph{Laws for ghosts and physical resources.} \begin{mathpar} \begin{array}{rMcMl} @@ -468,7 +433,7 @@ Soundness follows from the theorem that ${\cal U}(\any, \textdom{Prop}) \end{array} \end{mathpar} -\subsection{Laws for the later modality}\label{sec:later} +\paragraph{Laws for the later modality.} \begin{mathpar} \inferH{Mono} @@ -492,7 +457,7 @@ Soundness follows from the theorem that${\cal U}(\any, \textdom{Prop}) \end{array} \end{mathpar} -\subsection{Laws for the always modality}\label{sec:always} +\paragraph{Laws for the always modality.} \begin{mathpar} \axiomH{Necessity} @@ -517,278 +482,10 @@ Soundness follows from the theorem that ${\cal U}(\any, \textdom{Prop}) \end{mathpar} Note that$\always$binds more tightly than$*$,$\land$,$\lor$, and$\Ra. -\section{Program logic}\label{sec:proglog} - -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})} -\qquad\qquad -\begin{aligned} -\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 -\end{aligned} - -We write just one mask for a view shift when\mask_1 = \mask_2$. -The convention for omitted masks is generous: -An omitted$\mask$is$\top$for Hoare triples and$\emptyset$for view shifts. - -% PDS: We're repeating ourselves. We gave Γ conventions and we're about to give Θ conventions. Also, the scope of "Below" is unclear. -% Below, we implicitly assume the same context for all judgements which don't have an explicit context at \emph{all} pre-conditions \emph{and} the conclusion. +\paragraph{Laws of primitive view shifts.} -Henceforward, we implicitly assume a proof context,$\pfctx$, is added to every constituent of the rules. -Generally, this is an arbitrary proof context. -We write$\provesalways$to denote judgments that can only be extended with a boxed proof context. +\paragraph{Laws of weakest preconditions.} -\ralf{Give the actual base rules from the Coq development instead} - -\subsection{Hoare triples} -\begin{mathpar} -\inferH{Ret} - {} - {\hoare{\TRUE}{\valB}{\Ret\val. \val = \valB}[\mask]} -\and -\inferH{Bind} - {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask] \\ - \All \val. \hoare{\propB}{K[\val]}{\Ret\valB.\propC}[\mask]} - {\hoare{\prop}{K[\expr]}{\Ret\valB.\propC}[\mask]} -\and -\inferH{Csq} - {\prop \vs \prop' \\ - \hoare{\prop'}{\expr}{\Ret\val.\propB'}[\mask] \\ - \All \val. \propB' \vs \propB} - {\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask]} -\and -\inferH{Frame} - {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask]} - {\hoare{\prop * \propC}{\expr}{\Ret\val. \propB * \propC}[\mask \uplus \mask']} -\and -\inferH{AFrame} - {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask] \and \text{$\expr$not a value} - } - {\hoare{\prop * \later\propC}{\expr}{\Ret\val. \propB * \propC}[\mask \uplus \mask']} -% \and -% \inferH{Fork} -% {\hoare{\prop}{\expr}{\Ret\any. \TRUE}[\top]} -% {\hoare{\later\prop * \later\propB}{\fork{\expr}}{\Ret\val. \val = \textsf{fRet} \land \propB}[\mask]} -\and -\inferH{ACsq} - {\prop \vs[\mask \uplus \mask'][\mask] \prop' \\ - \hoare{\prop'}{\expr}{\Ret\val.\propB'}[\mask] \\ - \All\val. \propB' \vs[\mask][\mask \uplus \mask'] \propB \\ - \physatomic{\expr} - } - {\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \mask']} -\end{mathpar} - -\subsection{View shifts} - -\begin{mathpar} -\inferH{NewInv} - {\infinite(\mask)} - {\later{\prop} \vs[\mask] \exists \iname\in\mask.\; \knowInv{\iname}{\prop}} -\and -\inferH{FpUpd} - {\melt \mupd \meltsB} - {\ownGGhost{\melt} \vs \exists \meltB \in \meltsB.\; \ownGGhost{\meltB}} -\and -\inferH{VSTrans} - {\prop \vs[\mask_1][\mask_2] \propB \and \propB \vs[\mask_2][\mask_3] \propC \and \mask_2 \subseteq \mask_1 \cup \mask_3} - {\prop \vs[\mask_1][\mask_3] \propC} -\and -\inferH{VSImp} - {\always{(\prop \Ra \propB)}} - {\prop \vs[\emptyset] \propB} -\and -\inferH{VSFrame} - {\prop \vs[\mask_1][\mask_2] \propB} - {\prop * \propC \vs[\mask_1 \uplus \mask'][\mask_2 \uplus \mask'] \propB * \propC} -\and -\inferH{VSTimeless} - {\timeless{\prop}} - {\later \prop \vs \prop} -\and -\axiomH{InvOpen} - {\knowInv{\iname}{\prop} \proves \TRUE \vs[\{ \iname \} ][\emptyset] \later \prop} -\and -\axiomH{InvClose} - {\knowInv{\iname}{\prop} \proves \later \prop \vs[\emptyset][\{ \iname \} ] \TRUE } -\end{mathpar} - -\vspace{5pt} -Note that$\timeless{\prop}$means that$\prop$does not depend on the step index. -Furthermore, $$\melt \mupd \meltsB \eqdef \always{\All \melt_f. \melt \sep \melt_f \Ra \Exists \meltB \in \meltsB. \meltB \sep \melt_f}$$ - -\subsection{Derived rules} - -\paragraph{Derived structural rules.} -The following are easily derived by unfolding the sugar for Hoare triples and view shifts. -\begin{mathpar} -\inferHB{Disj} - {\hoare{\prop}{\expr}{\Ret\val.\propC}[\mask] \and \hoare{\propB}{\expr}{\Ret\val.\propC}[\mask]} - {\hoare{\prop \lor \propB}{\expr}{\Ret\val.\propC}[\mask]} -\and -\inferHB{VSDisj} - {\prop \vs[\mask_1][\mask_2] \propC \and \propB \vs[\mask_1][\mask_2] \propC} - {\prop \lor \propB \vs[\mask_1][\mask_2] \propC} -\and -\inferHB{Exist} - {\All \var. \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask]} - {\hoare{\Exists \var. \prop}{\expr}{\Ret\val.\propB}[\mask]} -\and -\inferHB{VSExist} - {\All \var. (\prop \vs[\mask_1][\mask_2] \propB)} - {(\Exists \var. \prop) \vs[\mask_1][\mask_2] \propB} -\and -\inferHB{BoxOut} - {\always\propB \provesalways \hoare{\prop}{\expr}{\Ret\val.\propC}[\mask]} - {\hoare{\prop \land \always{\propB}}{\expr}{\Ret\val.\propC}[\mask]} -\and -\inferHB{VSBoxOut} - {\always\propB \provesalways \prop \vs[\mask_1][\mask_2] \propC} - {\prop \land \always{\propB} \vs[\mask_1][\mask_2] \propC} - \and -\inferH{False} - {} - {\hoare{\FALSE}{\expr}{\Ret \val. \prop}[\mask]} -\and -\inferH{VSFalse} - {} - {\FALSE \vs[\mask_1][\mask_2] \prop } -\end{mathpar} -The proofs all follow the same pattern, so we only show two of them in detail. -\begin{proof}[Proof of \ruleref{Exist}] - After unfolding the syntactic sugar for Hoare triples and removing the boxes from premise and conclusion, our goal becomes - $- (\Exists \var. \prop(\var)) \Ra \dynA{\expr}{\Lam\val. \propB}{\mask} -$ - (remember that$\var$is free in$\prop$) and the premise reads - $- \All \var. \prop(\var) \Ra \dynA{\expr}{\Lam\val. \propB}{\mask}. -$ - Let$\var$be given and assume$\prop(\var)$. - To show$\dynA{\expr}{\Lam\val. \propB}{\mask}$, apply the premise to$\var$and$\prop(\var)$. - - For the other direction, assume - $- \hoare{\Exists \var. \prop(\var)}{\expr}{\Ret\val. \propB}[\mask] -$ - and let$\var$be given. - We have to show$\hoare{\prop(\var)}{\expr}{\Ret\val. \propB}[\mask]$. - This trivially follows from \ruleref{Csq} with$\prop(\var) \Ra \Exists \var. \prop(\var)$. -\end{proof} - -\begin{proof}[Proof of \ruleref{BoxOut}] - After unfolding the syntactic sugar for Hoare triples, our goal becomes - $$\label{eq:boxin:goal} - \always\pfctx \proves \always\bigl(\prop\land\always \propB \Ra \dynA{\expr}{\Lam\val. \propC}{\mask}\bigr) -$$ - while our premise reads - $$\label{eq:boxin:as} - \always\pfctx, \always\propB \proves \always(\prop \Ra \dynA{\expr}{\Lam\val. \propC}{\mask}) -$$ - By the introduction rules for$\always$and implication, it suffices to show - $(\always\pfctx), \prop,\always \propB \proves \dynA{\expr}{\Lam\val. \propC}{\mask}$ - By modus ponens and \ruleref{Necessity}, it suffices to show~\eqref{eq:boxin:as}, which is exactly our assumption. - - For the other direction, assume~\eqref{eq:boxin:goal}. We have to show~\eqref{eq:boxin:as}. By \ruleref{AlwaysIntro} and implication introduction, it suffices to show - $(\always\pfctx), \prop,\always \propB \proves \dynA{\expr}{\Lam\val. \propC}{\mask}$ - which easily follows from~\eqref{eq:boxin:goal}. -\end{proof} - -\paragraph{Derived rules for invariants.} -Invariants can be opened around atomic expressions and view shifts. - -\begin{mathpar} -\inferH{Inv} - {\hoare{\later{\propC} * \prop } - {\expr} - {\Ret\val. \later{\propC} * \propB }[\mask] - \and \physatomic{\expr} - } - {\knowInv{\iname}{\propC} \proves \hoare{\prop} - {\expr} - {\Ret\val. \propB}[\mask \uplus \{ \iname \}] - } -\and -\inferH{VSInv} - {\later{\prop} * \propB \vs[\mask_1][\mask_2] \later{\prop} * \propC} - {\knowInv{\iname}{\prop} \proves \propB \vs[\mask_1 \uplus \{ \iname \}][\mask_2 \uplus \{ \iname \}] \propC} -\end{mathpar} - -\begin{proof}[Proof of \ruleref{Inv}] - Use \ruleref{ACsq} with$\mask_1 \eqdef \mask \cup \{\iname\}$,$\mask_2 \eqdef \mask$. - The view shifts are obtained by \ruleref{InvOpen} and \ruleref{InvClose} with framing of$\mask$and$\prop$or$\propB$, respectively. -\end{proof} - -\begin{proof}[Proof of \ruleref{VSInv}] -Analogous to the proof of \ruleref{Inv}, using \ruleref{VSTrans} instead of \ruleref{ACsq}. -\end{proof} - -\subsubsection{Unsound rules} - -Some rule suggestions (or rather, wishes) keep coming up, which are unsound. We collect them here. -\begin{mathpar} - \infer - {P \vs Q} - {\later P \vs \later Q} - \and - \infer - {\later(P \vs Q)} - {\later P \vs \later Q} -\end{mathpar} - -Of course, the second rule implies the first, so let's focus on that. -Since implications work under$\later$, from$\later P$we can get$\later \pvs{Q}$. -If we now try to prove$\pvs{\later Q}$, we will be unable to establish world satisfaction in the new world: -We have no choice but to use$\later \pvs{Q}$at one step index below what we are operating on (because we have it under a$\later). -We can easily get world satisfaction for that lower step-index (by downwards-closedness of step-indexed predicates). -We can, however, not make much use of the world satisfaction that we get out, becaase it is one step-index too low. - -\subsection{Adequacy} - -The adequacy statement reads as follows: -\begin{align*} - &\All \mask, \expr, \val, \pred, i, \state, \state', \tpool'. - \\&( \proves \hoare{\ownPhys\state}{\expr}{x.\; \pred(x)}[\mask]) \implies - \\&\cfg{\state}{[i \mapsto \expr]} \step^\ast - \cfg{\state'}{[i \mapsto \val] \uplus \tpool'} \implies - \\&\pred(\val) -\end{align*} -where\pred$can mention neither resources nor invariants. - -\subsection{Axiom lifting}\label{sec:lifting} - -The following lemmas help in proving axioms for a particular language. -The first applies to expressions with side-effects, and the second to side-effect-free expressions. -\dave{Update the others, and the example, wrt the new treatment of$\predB.} -\begin{align*} - &\All \expr, \state, \pred, \prop, \propB, \mask. \\ - &\textlog{reducible}(e) \implies \\ - &(\All \expr', \state'. \cfg{\state}{\expr} \step \cfg{\state'}{\expr'} \implies \pred(\expr', \state')) \implies \\ - &{} \proves \bigl( (\All \expr', \state'. \pred (\expr', \state') \Ra \hoare{\prop}{\expr'}{\Ret\val. \propB}[\mask]) \Ra \hoare{ \later \prop * \ownPhys{\state} }{\expr}{\Ret\val. \propB}[\mask] \bigr) \\ - \quad\\ - &\All \expr, \pred, \prop, \propB, \mask. \\ - &\textlog{reducible}(e) \implies \\ - &(\All \state, \expr_2, \state_2. \cfg{\state}{\expr} \step \cfg{\state_2}{\expr_2} \implies \state_2 = \state \land \pred(\expr_2)) \implies \\ - &{} \proves \bigl( (\All \expr'. \pred(\expr') \Ra \hoare{\prop}{\expr'}{\Ret\val. \propB}[\mask]) \Ra \hoare{\later\prop}{\expr}{\Ret\val. \propB}[\mask] \bigr) -\end{align*} -Note that\pred$is a meta-logic predicate---it does not depend on any world or resources being owned. - -The following specializations cover all cases of a heap-manipulating lambda calculus like$F_{\mu!}. -\begin{align*} - &\All \expr, \expr', \prop, \propB, \mask. \\ - &\textlog{reducible}(e) \implies \\ - &(\All \state, \expr_2, \state_2. \cfg{\state}{\expr} \step \cfg{\state_2}{\expr_2} \implies \state_2 = \state \land \expr_2 = \expr') \implies \\ - &{} \proves (\hoare{\prop}{\expr'}{\Ret\val. \propB}[\mask] \Ra \hoare{\later\prop}{\expr}{\Ret\val. \propB}[\mask] ) \\ - \quad \\ - &\All \expr, \state, \pred, \mask. \\ - &\textlog{atomic}(e) \implies \\ - &\bigl(\All \expr_2, \state_2. \cfg{\state}{\expr} \step \cfg{\state_2}{\expr_2} \implies \pred(\expr_2, \state_2)\bigr) \implies \\ - &{} \proves (\hoare{ \ownPhys{\state} }{\expr}{\Ret\val. \Exists\state'. \ownPhys{\state'} \land \pred(\val, \state') }[\mask] ) -\end{align*} -The first is restricted to deterministic pure reductions, like\beta$-reduction. -The second is suited to proving triples for (possibly non-deterministic) atomic expressions; for example, with$\expr \eqdef \;!\ell$(dereferencing$\ell$) and$\state \eqdef h \mtimes \ell \mapsto \valB$and$\pred(\val, \state') \eqdef \state' = (h \mtimes \ell \mapsto \valB) \land \val = \valB$, one obtains the axiom$\All h, \ell, \valB. \hoare{\ownPhys{h \mtimes \ell \mapsto \valB}}{!\ell}{\Ret\val. \val = \valB \land \ownPhys{h \mtimes \ell \mapsto \valB} }\$. -%Axioms for CAS-like operations can be obtained by first deriving rules for the two possible cases, and then using the disjunction rule. %%% Local Variables: %%% mode: latex diff --git a/docs/setup.tex b/docs/setup.tex index a75c3a5a95ffb218671a3d3890983f501850a632..016f0ee4d97b41cbea4145b509193a7a2aec6a37 100644 --- a/docs/setup.tex +++ b/docs/setup.tex @@ -149,6 +149,7 @@ \newcommand{\ALT}{\ |\ } +\newcommand\dplus{\mathbin{+\kern-1.0ex+}} \newcommand{\upclose}{\mathord{\uparrow}} @@ -198,31 +199,7 @@ \end{tabu}% } - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% CMRA (RESOURCE ALGEBRA) SYMBOLS & NOTATION & IDENTIFIERS -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\newcommand{\textmon}[1]{\textsc{#1}} - -\newcommand{\monoid}{M} -\newcommand{\mval}{V} - -\newcommand{\melt}{a} -\newcommand{\meltB}{b} -\newcommand{\meltC}{c} -\newcommand{\melts}{A} -\newcommand{\meltsB}{B} - -\newcommand{\mcar}[1]{|#1|} -\newcommand{\mcarp}[1]{\mcar{#1}^{+}} -\newcommand{\mzero}{\bot} -\newcommand{\munit}{\mathord{\varepsilon}} -\newcommand{\mtimes}{\mathbin{\cdot}} -\newcommand{\mdiv}{\mathbin{\div}} - -\newcommand{\mupd}{\rightsquigarrow} -\newcommand{\mincl}[1]{\ensuremath{\mathrel{\stackrel{#1}{\leq}}}} - +\newcommand{\Func}{F} % functor %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% MODEL-SPECIFIC SYMBOLS & NOTATION & IDENTIFIERS @@ -262,6 +239,36 @@ \newcommand{\PropDom}{\textdom{Prop}} \newcommand{\PredDom}{\textdom{Pred}} +\newcommand{\COFEs}{\mathcal{U}} % category of COFEs +\newcommand{\iFunc}{\Sigma} + + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% CMRA (RESOURCE ALGEBRA) SYMBOLS & NOTATION & IDENTIFIERS +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\newcommand{\textmon}[1]{\textsc{#1}} + +\newcommand{\monoid}{M} +\newcommand{\mval}{V} + +\newcommand{\melt}{a} +\newcommand{\meltB}{b} +\newcommand{\meltC}{c} +\newcommand{\melts}{A} +\newcommand{\meltsB}{B} + +\newcommand{\mcar}[1]{|#1|} +\newcommand{\mcarp}[1]{\mcar{#1}^{+}} +\newcommand{\mzero}{\bot} +\newcommand{\munit}{\mathord{\varepsilon}} +\newcommand{\mtimes}{\mathbin{\cdot}} +\newcommand{\mdiv}{\mathbin{\div}} + +\newcommand{\mupd}{\rightsquigarrow} +\newcommand{\mincl}[1]{\ensuremath{\mathrel{\stackrel{#1}{\leq}}}} + +\newcommand{\CMRAs}{\mathcal{R}} % category of CMRAs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% LOGIC SYMBOLS & NOTATION & IDENTIFIERS @@ -272,7 +279,10 @@ \newcommand{\Sig}{\mathcal{S}} \newcommand{\SigType}{\mathcal{T}} \newcommand{\SigFn}{\mathcal{F}} +\newcommand{\SigAx}{\mathcal{A}} +\newcommand{\sigtype}{T} \newcommand{\sigfn}{F} +\newcommand{\sigax}{A} \newcommand{\type}{\tau} @@ -284,8 +294,6 @@ \newcommand{\termB}{u} \newcommand{\termVal}{V} -\newcommand{\sort}{\Sigma} - \newcommand{\vctx}{\Gamma} \newcommand{\pfctx}{\Theta} @@ -425,7 +433,11 @@ \newcommand{\state}{\sigma} \newcommand{\step}{\ra} -\newcommand{\ectx}{K} +\newcommand{\toval}{\mathit{val}} +\newcommand{\ofval}{\mathit{expr}} +\newcommand{\atomic}{\mathit{atomic}} +\newcommand{\Lang}{\Lambda} + \newcommand{\tpool}{T} \newcommand{\cfg}[2]{{#1};{#2}}