The idea behind the \emph{boxes} is to have an proposition $\prop$ that is actually split into a number of pieces, each of which can be taken out and back in separately.
The idea behind the \emph{boxes} is to have a proposition $\prop$ that is actually split into a number of pieces, each of which can be taken out and back in separately.
In some sense, this is a replacement for having an ``authoritative PCM of Iris propositions itself''.
In some sense, this is a replacement for having an ``authoritative PCM of Iris propositions itself''.
It is similar to the pattern involving saved propositions that was used for the barrier~\cite{iris2}, but more complicated because there are some operations that we want to perform without a later.
It is similar to the pattern involving saved propositions that was used for the barrier~\cite{iris2}, but more complicated because there are some operations that we want to perform without a later.
Roughly, the idea is that a \emph{box} is a container for an proposition $\prop$.
Roughly, the idea is that a \emph{box} is a container for a proposition $\prop$.
A box consists of a bunch of \emph{slices} which decompose $\prop$ into a separating conjunction of the propositions $\propB_\sname$ governed by the individual slices.
A box consists of a bunch of \emph{slices} which decompose $\prop$ into a separating conjunction of the propositions $\propB_\sname$ governed by the individual slices.
Each slice is either \emph{full} (it right now contains $\propB_\sname$), or \emph{empty} (it does not contain anything currently).
Each slice is either \emph{full} (it right now contains $\propB_\sname$), or \emph{empty} (it does not contain anything currently).
The proposition governing the box keeps track of the state of all the slices that make up the box.
The proposition governing the box keeps track of the state of all the slices that make up the box.
@@ -23,7 +23,7 @@ We assume to have the following four cameras available:
...
@@ -23,7 +23,7 @@ We assume to have the following four cameras available:
\end{align*}
\end{align*}
The last two are the tokens used for managing invariants, $\textdom{Inv}$ is the monoid used to manage the invariants themselves.
The last two are the tokens used for managing invariants, $\textdom{Inv}$ is the monoid used to manage the invariants themselves.
We assume that at the beginning of the verification, instances named $\gname_{\textdom{State}}$, $\gname_{\textdom{Inv}}$, $\gname_{\textdom{En}}$ and $\gname_{\textdom{Dis}}$ of these cameras have been created, such that these names are globally known.
We assume that at the beginning of the verification, instances named $\gname_{\textdom{Inv}}$, $\gname_{\textdom{En}}$ and $\gname_{\textdom{Dis}}$ of these cameras have been created, such that these names are globally known.
\paragraph{World Satisfaction.}
\paragraph{World Satisfaction.}
We can now define the proposition $W$ (\emph{world satisfaction}) which ensures that the enabled invariants are actually maintained:
We can now define the proposition $W$ (\emph{world satisfaction}) which ensures that the enabled invariants are actually maintained:
