In this section we provide proofs of some logical inconsistencies that arise when slight changes are made to the Iris logic.
\subsection{Saved propositions without a later}
\label{sec:saved-prop-no-later}
As a preparation for the proof about invariants in \Sref{app:section:invariants-without-a-later}, we show that omitting the later modality from a variant of \emph{saved propositions} leads to a contradiction.
Saved propositions have been introduced in prior work~\cite{dodds:higher-order-sync,iris2} to prove correctness of synchronization primitives; we will explain all that is necessary here.
The counterexample assumes a higher-order logic with separating conjunction, magic wand and the modalities $\always$ and $\upd$ satisfying the rules in \Sref{sec:base-logic}.
\begin{thm}
\label{thm:counterexample-1}
If there exists a type $\GName$ and an assertion $\_\Mapsto\_ : \GName\to\Prop\to\Prop$ associating names $\gamma : \GName$ to propositions and satisfying:
\gname\Mapsto P \proves{}&\always (\gname\Mapsto P)
\tagH{sprop-persist}\\
\gname\Mapsto\prop * \gname\Mapsto\propB\proves{}
&
\prop\Lra\propB
\tagH{sprop-agree}
\end{align}
then $\proves\upd\FALSE$.
\end{thm}
The type $\GName$ should be thought of as the type of ``locations'' and $\gname\Mapsto P$ should be read as stating that location $\gname$ ``stores'' proposition $P$.
Notice that these are immutable locations, so the maps-to assertion is persistent.
The rule \ruleref{sprop-alloc} is then thought of as allocation, and the rule \ruleref{sprop-agree} states that a given location $\gname$ can only store \emph{one} proposition, so multiple witnesses covering the same location must agree.
%Compared to saved propositions in prior work, \ruleref{sprop-alloc} is stronger since the stored proposition can depend on the name being allocated.
%\derek{Can't we cut the above sentence? This makes it sound like we are doing something weird that we ought not to be since prior work didn't do it. But in fact, I thought that in our construction we don't really need to rely on this feature at all! So I'm confused.}
The conclusion of \ruleref{sprop-agree} usually is guarded by a $\later$.
The point of this theorem is to show that said later is \emph{essential}, as removing it introduces inconsistency.
%
The key to proving \thmref{thm:counterexample-1} is the following assertion:
Intuitively, $A(\gname)$ says that the saved proposition named $\gname$ does \emph{not} hold, \ie we can disprove it.
Using \ruleref{sprop-persist}, it is immediate that $A(\gname)$ is persistent.
Now, by applying \ruleref{sprop-alloc} with $A$, we obtain a proof of $\prop\eqdef\gname\Mapsto A(\gname)$: this says that the proposition named $\gname$ is the assertion saying that it, itself, doesn't hold.
In other words, $\prop$ says that the assertion named $\gname$ expresses its own negation.
Unsurprisingly, that leads to a contradiction, as is shown in the following lemma:
\begin{lem}\label{lem:saved-prop-counterexample-not-agname} We have $\gname\Mapsto A(\gname)\proves\always\lnot A(\gname)$ and $\gname\Mapsto A(\gname)\proves A(\gname)$. \end{lem}
\item First we show $\gname\Mapsto A(\gname)\proves\always\lnot A(\gname)$.
Since $\gname\Mapsto A(\gname)$ is persistent it suffices to show $\gname\Mapsto A(\gname)\proves\lnot A(\gname)$.
Suppose $\gname\Mapsto A(\gname)$ and $A(\gname)$.
Then by definition of \(A\) there is a $\prop$ such that $\always\lnot\prop$ and $\gname\Mapsto\prop$.
By \ruleref{sprop-agree} we have $\prop\Lra A(\gname)$ and so from $\lnot\prop$ we get $\lnot A(\gname)$, which leads to a contradiction with $A(\gname)$.
\item Using the first item we can now prove $\gname\Mapsto A(\gname)\proves A(\gname)$.
Together with the rule \ruleref{sprop-alloc} we thus derive $\upd\FALSE$.
\end{proof}
\subsection{Invariants without a later}
\label{app:section:invariants-without-a-later}
Now we come to the main paradox: if we remove the $\later$ from \ruleref{inv-open}, the logic becomes inconsistent.
The theorem is stated as general as possible so taht it also applies to previous, less powerful versions of Iris.
\begin{thm}
\label{thm:counterexample-2}
Assume a higher-order separation logic with $\always$ and an update modality with a binary mask ${\upd}_{\set{0,1}}$ (think: empty mask and full mask) satisfying strong monad rules with respect to separating conjunction and such that:
\begin{mathpar}
\inferhref{weaken-mask}{eq:update-weaken-mask}
{}{{\upd}_0 \prop\proves{\upd}_1 \prop}
\end{mathpar}
\noindent
Assume a type $\InvName$ and an assertion $\knowInv{\cdot}{\cdot} : \InvName\to\Prop\to\Prop$ satisfying:
Finally, assume the existence of a type $\GName$ and two tokens $\ownGhost{\cdot}{\starttoken} : \GName\to\Prop$ and $\ownGhost{\cdot}{\finishtoken}: \GName\to\Prop$ parameterized by $\GName$ and satisfying the following properties:
The core of the proof is defining the $\Mapsto$ from the previous counterexample using invariants.
Then, using the standard proof rules for invariants, we show that it satisfies \ruleref{sprop-alloc} and \ruleref{sprop-persist}.
Furthermore, assuming the rule for opening invariants without a $\later$, we can prove a slightly weaker version of \ruleref{sprop-agree}, which is sufficient for deriving a contradiction.
% Taking ${\upd}_\bot$ and ${\upd}_\top$ to be the fancy update modalities $\pvs[\emptyset]$
% and $\pvs[\nat]$, respectively, we can see that Iris
% \emph{almost} satisfies these axioms. First, to implement the tokens,
% we can use the RA with the carrier
% $\{\mundef,\epsilon,\starttoken,\finishtoken\}$ and operation
% $\epsilon \mtimes x = x \mtimes \epsilon = x$,
% $\finishtoken \mtimes \finishtoken = \finishtoken$ and otherwise
% $x \mtimes y = \mundef$. Then, observe that the rules for
% $\knowInv{\cdot}{\cdot}$ are special cases of (derivable) invariant
% rules in Iris. The fly in the ointment is the \ruleref{eq:inv-open}
% rule: in Iris, this rule would protect each occurrence of $\prop$
% in the premise of the rule with a $\later$, whereas here they are
% unprotected.
We start by defining $\Mapsto$ satisfying (almost) the assumptions of \lemref{lem:counterexample-invariants-saved-prop-agree}.
%
\begin{defn}
We define $\_\Mapsto\_ : \GName\to\Prop\to\Prop$ as:
Note that using \ruleref{eq:inv-persistent}, it is immediate that $\gname\Mapsto\prop$ is persistent.
We use the tokens $\ownGhost\gname\starttoken$ and $\ownGhost\gname\finishtoken$ to model invariants that can be initialized ``lazily'': $\ownGhost\gname\starttoken$ indicates that the invariant is still not initialized, whereas the duplicable $\ownGhost\gname\finishtoken$ indicates it has been initialized with a resource satisfying $\prop$.%
%\footnote{We would usually require the token to be persistent, but it turns out the proof also works with the weaker assumption of duplicability.}
% RK: cut the footnote, it takes space. Maybe restore later
% TODO, explain this ...
We can show variants of \ruleref{sprop-agree} and \ruleref{sprop-alloc} for the defined $\Mapsto$.
We have to show the allocation rule \[\proves{\upd}_\top\Exists\gname. \gname\Mapsto\prop.\]
From \ruleref{eq:start-alloc} we have a $\gname$ such that ${\upd}_\bot\ownGhost\gname\starttoken$ holds and hence from \ruleref{eq:update-weaken-mask} we have ${\upd}_\top\ownGhost\gname\starttoken$.
Since we are proving a goal of the form ${\upd}_\top R$ we may assume $\ownGhost\gname\starttoken$.
Thus for any $\prop$ we have ${\upd}_\top\left(\ownGhost{\gname}{\starttoken}\lor\ownGhost\gname\finishtoken*\prop\right)$.
Again since our goal is still of the form ${\upd}_\top$ we may assume $\ownGhost{\gname}{\starttoken}\lor\ownGhost\gname\finishtoken*\always\prop$.
The rule \ruleref{eq:inv-alloc} then gives us precisely what we need.
We use \ruleref{eq:inv-open} to open the invariant in $\gname\Mapsto\prop$ and consider two cases:
%
\begin{enumerate}
\item$\ownGhost\gname\starttoken$(the invariant is ``uninitialized'') : In this case, we use \ruleref{eq:start-finish} to ``initialize'' the invariant and obtain $\ownGhost{\gname}{\finishtoken}$.
Then we duplicate $\ownGhost\gname\finishtoken$, and use it together with $\always\prop$ to close the invariant.
\item$\ownGhost\gname\finishtoken*\always\prop$ (the invariant is ``initialized''): In this case we duplicate $\ownGhost\gname\finishtoken$, and use a copy to close the invariant.
\end{enumerate}
%
After closing the invariant, we have obtained $\ownGhost\gname\finishtoken$.
We proceed by using \ruleref{eq:inv-open} to open the other invariant in $\gname\Mapsto\propB$, and we again consider two cases:
\begin{enumerate}
\item$\ownGhost{\gname}{\starttoken}$ (the invariant is ``uninitialized''): As witnessed by \ruleref{eq:start-not-finished}, this cannot happen, so we derive a contradiction.
Notice that this is a key point of the proof: because the two invariants ($\gname\Mapsto\prop$ and $\gname\Mapsto\propB$) \emph{share} the ghost name $\gname$, initializing one of them is enough to show that the other one has been initialized.
Essentially, this is an indirect way of saying that really, we have been opening the same invariant two times.
\item$\ownGhost{\gname}{\finishtoken}*\always\propB$ (the invariant is ``initialized''):
Since $\always\propB$ is duplicable we use one copy to close the invariant, and retain another to prove ${\upd}_\top\always\propB$.
\end{enumerate}
\item By applying the above twice, we easily obtain
% When allocating $\gname \Mapsto \prop(\gname)$ in \lemref{lem:counterexample-invariants-saved-prop-alloc}, we will start off in ``state'' $\ownGhost \gname \starttoken$, and once we have $P$ in \lemref{lem:counterexample-invariants-saved-prop-agree} we use \ruleref{eq:start-finish} to transition to $\ownGhost\gname \finishtoken$, obtaining ourselves a copy of said token.
% Finally, we use this token with $\gname \Mapsto \propB$ to obtain a proof of $\propB$.
Intuitively, \lemref{lem:counterexample-invariants-saved-prop-agree} shows that we can ``convert'' a proof from $\prop$ to $\propB$.
We are now in a position to replay the counterexample from \Sref{sec:saved-prop-no-later}.
The only difference is that because \lemref{lem:counterexample-invariants-saved-prop-agree} is slightly weaker than the rule \ruleref{sprop-agree} of \thmref{thm:counterexample-1}, we need to use ${\upd}_\top\FALSE$ in place of $\FALSE$ in the definition of the predicate $A$:
