cancellable invariants

docs/constructions.tex

@@ -202,7 +202,7 @@ We define an RA structure on the rational numbers in $(0, 1]$ as follows:
 \begin{align*}
   \fracm \eqdef{}& \fracinj(\mathbb{Q} \cap (0, 1]) \mid \mundef \\
   \mvalFull(\melt) \eqdef{}& \melt \neq \mundef \\
-  \fracinj(x) \mtimes \fracinj(y) \eqdef{}& \fracinj(x + y) \quad \text{if $x + y \leq 1$} \\
+  \fracinj(q_1) \mtimes \fracinj(q_2) \eqdef{}& \fracinj(q_1 + q_2) \quad \text{if $q_1 + q_2 \leq 1$} \\
   \mcore{\fracinj(x)} \eqdef{}& \bot \\
   \mcore{\mundef} \eqdef{}& \mundef
 \end{align*}

docs/derived.tex

 \section{Derived Constructions}
 
+\subsection{Cancellable Invariants}
+
+Iris invariants as described in \Sref{sec:invariants} are persistent---once established, they hold forever.
+However, based on them, it is possible to \emph{encode} a form of invariants that can be ``cancelled'' again.
+
+First, we need some ghost state:
+\begin{align*}
+  \textmon{CInvTok} \eqdef{}& \fracm
+\end{align*}
+
+Now we define:
+\begin{align*}
+  \CInvTok{\gname}{q} \eqdef{}& \ownGhost\gname{q} \\
+  \CInv{\gname}{\namesp}{\prop} \eqdef{}& \knowInv\namesp{\prop \lor \ownGhost\gname{1}}
+\end{align*}
+
+It is then straight-forward to prove:
+\begin{mathpar}
+  \inferH{CInv-new}{}
+  {\later\prop \vs[\bot] \Exists \gname. \CInvTok\gname{1} * \always\CInv\gname\namesp\prop}
+
+  \inferH{CInv-acc}{}
+  {\CInv\gname\namesp\prop \proves \Acc[\namesp][\emptyset]{\CInvTok\gname{q}}{\later\prop}}
+
+  \inferH{CInv-cancel}{}
+  {\CInv\gname\namesp\prop \proves \CInvTok\gname{1} \vs[\namesp] \later\prop}
+\end{mathpar}
+
+Cancellable invariants are useful, for example, when reasoning about data structures that will be deallocated:  Every reference to the data structure comes with a fraction of the token, and when all fractions have been gathered, \ruleref{CInv-cancel} is used to cancel the invariant, after which the data structure can be deallocated.
+
 \subsection{Non-atomic (``Thread-Local'') Invariants}
 
 Sometimes it is necessary to maintain invariants that we need to open non-atomically.
@@ -40,16 +70,16 @@ To simplify this construction,we piggy-back into ``normal'' invariants.
 
 We easily obtain:
 \begin{mathpar}
-  \axiom
+  \axiomH{NAInv-new-pool}
   {\TRUE \vs[\bot] \Exists\pid. \NaTok\pid}
 
-  \axiom
+  \axiomH{NAInv-tok-split}
   {\NaTokE\pid{\mask_1 \uplus \mask_2} \Lra \NaTokE\pid{\mask_1} * \NaTokE\pid{\mask_2}}
   
-  \axiom
+  \axiomH{NAInv-new-inv}
   {\later\prop  \vs[\namesp] \always\NaInv\pid\namesp\prop}
 
-  \axiom
+  \axiomH{NAInv-acc}
   {\NaInv\pid\namesp\prop \proves \Acc[\namesp]{\NaTokE\pid\namesp}{\later\prop}}
 \end{mathpar}
 from which we can derive

docs/iris.sty

@@ -409,6 +409,7 @@
 
 % Fraction
 \newcommand{\fracm}{\ensuremath{\textmon{Frac}}}
+\newcommand{\fracinj}{\textlog{frac}}
 
 % Exclusive
 \newcommand{\exm}{\ensuremath{\textmon{Ex}}}
@@ -452,6 +453,10 @@
 %% Stored Propositions
 \newcommand{\mapstoprop}{\mathrel{\kern-0.5ex\tikz[baseline=(m)]{\node at (0,0) (m){}; \draw[line cap=round] (0,0.16) -- (0,-0.004);}\kern-1.5ex\Ra}}
 
+%% Cancellable invariants
+\newcommand\CInv[3]{\textlog{CInv}^{#1,#2}(#3)}
+\newcommand*\CInvTok[2]{{[}\textrm{CInv}:#1{]}_{#2}}
+
 %% Non-atomic invariants
 \newcommand*\pid{p}
 \newcommand\NaInv[3]{\textlog{NaInv}^{#1.#2}(#3)}

[Robbert Krebbers]

straight-forward is one word :). i.e. no hyphen.

[Ralf Jung]

Actually the usual form seems to be straight forward.

[Robbert Krebbers]

No, it's one word.

https://dictionary.cambridge.org/dictionary/english/straightforward

[Ralf Jung]

All right, fixes. Thanks!