A \emph{language}$\Lang$ consists of a set \Expr{} of \emph{expressions} (metavariable $\expr$), a set \Val{} of \emph{values} (metavariable $\val$), and a nonempty set \State of \emph{states} (metavariable $\state$) such that
A \emph{language}$\Lang$ consists of a set \Expr{} of \emph{expressions} (metavariable $\expr$), a set \Val{} of \emph{values} (metavariable $\val$), and a nonempty set $\State$ of \emph{states} (metavariable $\state$) such that
\begin{itemize}[itemsep=0pt]
\item There exist functions $\ofval : \Val\to\Expr$ and $\toval : \Expr\pfn\Val$ (notice the latter is partial), such that
@@ -118,7 +118,6 @@ We assume to have the following four CMRAs available:
\textmon{Dis}\eqdef{}&\finpset{\InvName}
\end{align*}
The last two are the tokens used for managing invariants, $\textmon{Inv}$ is the monoid used to manage the invariants themselves.
Finally, $\textmon{State}$ is used to provide the program with a view of the physical state of the machine.
We assume that at the beginning of the verification, instances named $\gname_{\textmon{State}}$, $\gname_{\textmon{Inv}}$, $\gname_{\textmon{En}}$ and $\gname_{\textmon{Dis}}$ of these CMRAs have been created, such that these names are globally known.
...
...
@@ -190,14 +189,15 @@ Fancy updates satisfy the following basic proof rules:
We can further define the notions of \emph{view shifts} and \emph{linear view shifts}:
These two are useful when writing down specifications and for comparing with previous versions of Iris, but for reasoning, it is typically easier to just work directly with fancy updates.
Still, just to give an idea of what view shifts ``are'', here are some proof rules for them:
@@ -217,7 +217,7 @@ Still, just to give an idea of what view shifts ``are'', here are some proof rul
\and
\inferH{vs-timeless}
{\timeless{\prop}}
{\later\prop\vs\prop}
{\later\prop\vs[\emptyset]\prop}
% \inferH{vs-allocI}
% {\infinite(\mask)}
...
...
@@ -252,15 +252,15 @@ Finally, we can define the core piece of the program logic, the assertion that r
\paragraph{Defining weakest precondition.}
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$).
We further assume (as a parameter) a predicate $S : \State\to\iProp$ that interprets the physical state as an Iris assertion.
We further assume (as a parameter) a predicate $I : \State\to\iProp$ that interprets the physical state as an Iris assertion.
This can be instantiated, for example, with ownership of an authoritative RA to tie the physical state to fragments that are used for user-level proofs.
Notice that the state invariant $S$ used by the weakest precondition is chosen \emph{after} doing a fancy update, which allows it to depend on the names of ghost variables that are picked in that initial fancy update.
...
...
@@ -501,7 +501,20 @@ Additionally, opening the accessor provides us with $\All\varB. \propB' \vsW[\ma
This linear view shift tells us that in order to \emph{close} the accessor again and go back to mask $\mask_1$, we have to pick some $\varB$ and establish the corresponding $\propB'$.
After closing, we will obtain $\propC$.
Using \ruleref{vs-trans} and \ruleref{Ht-atomic} (or the corresponding proof rules for fancy updates and weakest preconditions), we can show that it is possible to open an accessor around any view shift and any \emph{atomic} expression.
Using \ruleref{vs-trans} and \ruleref{Ht-atomic} (or the corresponding proof rules for fancy updates and weakest preconditions), we can show that it is possible to open an accessor around any view shift and any \emph{atomic} expression:
