@@ -46,8 +46,9 @@ We collect here some important and frequently used derived proof rules.
An assertion $\prop$ is \emph{persistent} if $\prop\proves\always\prop$.
\end{defn}
\ralf{Needs update.}
Of course, $\always\prop$ is persistent for any $\prop$.
Furthermore, by the proof rules given in \Sref{sec:proof-rules}, $t = t'$ as well as $\ownGGhost{\mcore\melt}$, $\mval(\melt)$ and $\knowInv\iname\prop$ are persistent.
Furthermore, by the proof rules given in \Sref{sec:proof-rules}, $t = t'$ as well as $\ownGhost\gname{\mcore\melt}$, $\mval(\melt)$ and $\knowInv\iname\prop$ are persistent.
Persistence is preserved by conjunction, disjunction, separating conjunction as well as universal and existential quantification.
In our proofs, we will implicitly add and remove $\always$ from persistent assertions as necessary, and generally treat them like normal, non-linear assumptions.
...
...
@@ -98,7 +99,7 @@ The following rules can be derived for view shifts.
@@ -240,10 +241,11 @@ We can derive some specialized forms of the lifting axioms for the operational s
\subsection{Global functor and ghost ownership}
\ralf{Should be entirely redundant.}
Hereinafter we assume the global CMRA functor (served up as a parameter to Iris) is obtained from a family of functors $(\iFunc_i)_{i \in I}$ for some finite $I$ by picking
We don't care so much about what concretely $\textlog{GhName}$ is, as long as it is countable and infinite.
With $M_i \eqdef\iFunc_i(\iProp)$, we write $\ownGhost{\gname}{\melt : M_i}$ (or just $\ownGhost{\gname}{\melt}$ if $M_i$ is clear from the context) for $\ownGGhost{[i \mapsto[\gname\mapsto\melt]]}$.
With $M_i \eqdef\iFunc_i(\iProp)$, we write $\ownGhost{\gname}{\melt : M_i}$ (or just $\ownGhost{\gname}{\melt}$ if $M_i$ is clear from the context) for $\ownM{[i \mapsto[\gname\mapsto\melt]]}$.
In other words, $\ownGhost{\gname}{\melt : M_i}$ asserts that in the current state of monoid $M_i$, the ``ghost location'' $\gname$ is allocated and we own piece $\melt$.
From~\ruleref{pvs-update}, \ruleref{vs-update} and the frame-preserving updates in~\Sref{sec:prodm} and~\Sref{sec:fpfnm}, we have the following derived rules.
@@ -6,21 +8,21 @@ A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions}
\item There exist functions $\ofval : \textdom{Val}\to\textdom{Expr}$ and $\toval : \textdom{Expr}\pfn\textdom{val}$ (notice the latter is partial), such that
\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_\f$ indicates that, when $\expr_1$ reduces to $\expr_2$, a \emph{new thread}$\expr_\f$ is forked off.
\item There exists a \emph{primitive reduction relation}\[(-,-\step-,-,-)\subseteq\textdom{Expr}\times\textdom{State}\times\textdom{Expr}\times\textdom{State}\times(\cup_n \textdom{Expr}^n)\]
A reduction$\expr_1, \state_1\step\expr_2, \state_2, \overline\expr$ indicates that, when $\expr_1$ reduces to $\expr_2$, the new threads in the list $\overline\expr$ is forked off.
We will write$\expr_1, \state_1\step\expr_2, \state_2$ for $\expr_1, \state_1\step\expr_2, \state_2, ()$, \ie when no threads are forked off.\\
\item All values are stuck:
\[\expr, \_\step\_, \_, \_\Ra\toval(\expr)=\bot\]
\end{itemize}
\begin{defn}
An expression $\expr$ and state $\state$ are \emph{reducible} (written $\red(\expr, \state)$) if
@@ -62,6 +60,7 @@ For any language $\Lang$, we define the corresponding thread-pool semantics.
\label{sec:program-logic}
This section describes how to build a program logic for an arbitrary language (\cf\Sref{sec:language}) on top of the logic described in \Sref{sec:hogs}.
So in the following, we assume that some language $\Lang$ was fixed.
@@ -82,24 +81,56 @@ Finally, $\textmon{State}$ is used to provide the program with a view of the phy
Furthermore, we assume that instances named $\gname_{\textmon{State}}$, $\gname_{\textmon{Inv}}$, $\gname_{\textmon{En}}$ and $\gname_{\textmon{Dis}}$ of these CMRAs have been created.
(We will discuss later how this assumption is discharged.)
\paragraph{World Satisfaction.}
We can now define the assertion $W$ (\emph{world satisfaction}) which ensures that the enabled invariants are actually maintained:
\begin{align*}
W \eqdef{}&\Exists I : \mathbb N \fpfn\Prop. \ownGhost{\gname_{\textmon{Inv}}}{\authfull\aginj(\latertinj(\wIso(I)))}
%
%(∃ I : gmap positive (iProp Σ),
% own invariant_name (● (invariant_unfold <$> I : gmap _ _)) ★
% [★ map] i ↦ Q ∈ I, ▷ Q ★ ownD {[i]} ∨ ownE {[i]})
W \eqdef{}&\Exists I : \mathbb N \fpfn\Prop. \ownGhost{\gname_{\textmon{Inv}}}{\authfull\aginj(\latertinj(\wIso(I)))} * \Sep_{\iname\in\dom(I)}\left( \later I(\iname) * \ownGhost{\gname_{\textmon{Dis}}}{\set{\iname}}\lor\ownGhost{\gname_{\textmon{En}}}{\set{\iname}}\right)
\end{align*}
\paragraph{Invariants.}
The following assertion states that an invariant with name $\iname$ exists and maintains assertion $\prop$:
Next, we define \emph{view updates}, which are essentially the same as the resource updates of the base logic ($\Sref{sec:base-logic}$), except that they also have access to world satisfaction and can enable and disable invariants:
\[\pvs[\mask_1][\mask_2]\prop\eqdef W *\ownGhost{\gname_{\textmon{En}}}{\mask_1}\wand W *\ownGhost{\gname_{\textmon{En}}}{\mask_2}*\prop\]
We further define the notions of \emph{view shifts} and \emph{linear view shifts}:
Finally, we can define the core piece of the program logic, the assertion that reasons about program behavior: Weakest precondition, from which Hoare triples will be derived.
We assume that everything making up the definition of the language, \ie values, expressions, states, the conversion functions, reduction relation and all their properties, are suitably reflected into the logic (\ie they are part of the signature $\Sig$).
\ralf{TODO: Right now, this is a dump of all the things that moved out of the base...}
To instantiate Iris, you need to define the following parameters:
\begin{itemize}
\item A language $\Lang$, and
\item a locally contractive bifunctor $\iFunc : \COFEs\to\CMRAs$ defining the ghost state, such that for all COFEs $\cofe$, the CMRA $\iFunc(A)$ has a unit. (By \lemref{lem:cmra-unit-total-core}, this means that the core of $\iFunc(\cofe)$ is a total function.)
\end{itemize}
We will write $\pvs[\term]\prop$ for $\pvs[\term][\term]\prop$.
If we omit the mask, then it is $\top$ for weakest precondition $\wpre\expr{\Ret\var.\prop}$ and $\emptyset$ for primitive view shifts $\pvs\prop$.
...
...
@@ -138,7 +169,7 @@ We introduce additional metavariables ranging over terms and generally let the c
\infer
{\text{$\melt$ is a discrete COFE element}}
{\timeless{\ownGGhost\melt}}
{\timeless{\ownM\melt}}
\infer
{\text{$\melt$ is an element of a discrete CMRA}}
...
...
@@ -198,7 +229,7 @@ We introduce additional metavariables ranging over terms and generally let the c
