paradoxes.tex 14.2 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
\section{Logical Paradoxes}
2 3 4 5 6
\newcommand{\starttoken}{\textsc{s}}
\newcommand{\finishtoken}{\textsc{f}}

In this section we provide proofs of some logical inconsistencies that arise when slight changes are made to the Iris logic.

Ralf Jung's avatar
Ralf Jung committed
7
\subsection{Saved Propositions without a Later}
8 9 10 11 12 13 14 15
\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}
16
If there exists a type $\GName$ and a proposition $\_ \Mapsto \_ : \GName \to \Prop \to \Prop$ associating names $\gamma : \GName$ to propositions and satisfying:
17 18 19 20 21 22 23 24 25 26 27 28 29 30
\begin{align}
    \proves{}& \upd \Exists \gname : \GName. \gname \Mapsto P(\gname)
               \tagH{sprop-alloc} \\
    \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$.
31
Notice that these are immutable locations, so the maps-to proposition is persistent.
32 33 34
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
35
%\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 do not really need to rely on this feature at all!  So I'm confused.}
36 37 38
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.
%
39
The key to proving \thmref{thm:counterexample-1} is the following proposition:
40 41 42 43 44 45
\begin{defn}
$A(\gname) \eqdef \Exists \prop : \Prop. \always\lnot \prop \land \gname \Mapsto \prop$.
\end{defn}
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.

Robbert Krebbers's avatar
Robbert Krebbers committed
46
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 proposition saying that it, itself, does not hold.
47
In other words, $\prop$ says that the proposition named $\gname$ expresses its own negation.
48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77
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}
\begin{proof}%[\lemref{lem:saved-prop-counterexample-not-agname}]
\leavevmode
  \begin{itemize}
  \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)$.
    We need to prove
    \begin{align*}
      \Exists \prop : \Prop. \always \lnot \prop \land \gname \Mapsto \prop.
    \end{align*}
    We do so by picking $\prop$ to be $A(\gname)$, which leaves us to prove \(\always \lnot A(\gname) \land \gname \Mapsto A(\gname)\).
    The last conjunct holds by assumption, and the first conjunct follows from the previous item of this lemma.
  \end{itemize}
\end{proof}

With this lemma in hand, the proof of \thmref{thm:counterexample-1} is simple.
\begin{proof}[\thmref{thm:counterexample-1}]
  Using the previous lemmas we have
  \begin{align*}
    \proves \All \gname. \lnot (\gname \Mapsto A(\gname)).
  \end{align*}
  Together with the rule \ruleref{sprop-alloc} we thus derive $\upd \FALSE$.
\end{proof}

Ralf Jung's avatar
Ralf Jung committed
78
\subsection{Invariants without a Later}
79 80 81 82 83 84 85 86 87 88 89 90 91 92
\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
93
  Assume a type $\InvName$ and a proposition $\knowInv{\cdot}{\cdot} : \InvName \to \Prop \to \Prop$ satisfying:
94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134
%
  \begin{mathpar}
    \inferhref{inv-alloc}{eq:inv-alloc}
    {}
    {\prop \proves {\upd}_1 \Exists \iname. \knowInv \iname \prop}
    \and
    \inferhref{inv-persist}{eq:inv-persistent}
    {}
    {\knowInv \iname \prop \proves \always \knowInv \iname \prop}
    \and
    \inferhref{inv-open-nolater}{eq:inv-open}
    {\prop * \propB \proves {\upd}_0 (\prop * \propC) }
    {\knowInv \iname \prop * \propB \proves {\upd}_1 \propC}
  \end{mathpar}

\noindent
  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:
  \begin{mathpar}
    \inferhref{start-alloc}{eq:start-alloc}
    {}{\proves {\upd}_0 \Exists \gname. \ownGhost \gname \starttoken}
    \and
    \inferhref{start-finish}{eq:start-finish}
    {}{\ownGhost \gname \starttoken \proves {\upd}_0 \ownGhost \gname \finishtoken}
    \and
    \inferhref{start-not-finished}{eq:start-not-finished}
    {}{\ownGhost \gname \starttoken * \ownGhost \gname \finishtoken \proves \FALSE}
    \and
    \inferhref{finished-dup}{eq:finished-dup}
    {}{\ownGhost \gname \finishtoken \proves \ownGhost \gname \finishtoken * \ownGhost \gname \finishtoken}
  \end{mathpar}

\noindent
  Then $\TRUE \proves{\upd}_1 \FALSE$.
\end{thm}


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.


Ralf Jung's avatar
Ralf Jung committed
135
% Taking ${\upd}_0$ and ${\upd}_1$ to be the fancy update modalities $\pvs[\emptyset]$
136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169
% 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:
%
\begin{align*}
  \gname \Mapsto \prop \eqdef \Exists \iname. \knowInv \iname {\ownGhost \gname \starttoken \lor \ownGhost \gname \finishtoken * \always \prop}.
\end{align*}
\end{defn}
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$.
\begin{lem}
  \label{lem:counterexample-invariants-saved-prop-alloc}
We have
Ralf Jung's avatar
Ralf Jung committed
170
  \(\proves {\upd}_1 \Exists \gname. \gname \Mapsto \prop(\gname)\).
171 172
\end{lem}
\begin{proof}
Ralf Jung's avatar
Ralf Jung committed
173 174 175 176 177
  We have to show the allocation rule \[\proves {\upd}_1 \Exists \gname. \gname \Mapsto \prop.\]
    From \ruleref{eq:start-alloc} we have a $\gname$ such that ${\upd}_0 \ownGhost \gname \starttoken$ holds and hence from \ruleref{eq:update-weaken-mask} we have ${\upd}_1\ownGhost\gname \starttoken$.
    Since we are proving a goal of the form ${\upd}_1 R$ we may assume $\ownGhost \gname \starttoken$.
    Thus for any $\prop$ we have ${\upd}_1\left(\ownGhost{\gname}{\starttoken} \lor \ownGhost \gname \finishtoken * \prop\right)$.
    Again since our goal is still of the form ${\upd}_1$ we may assume $\ownGhost{\gname}{\starttoken} \lor \ownGhost \gname \finishtoken * \always \prop$.
178 179 180 181 182 183 184 185
    The rule \ruleref{eq:inv-alloc} then gives us precisely what we need.
 \qed \end{proof}

%
\begin{lem}
\label{lem:counterexample-invariants-saved-prop-agree}
We have
  \(
Ralf Jung's avatar
Ralf Jung committed
186
  \gname \Mapsto \prop * \gname \Mapsto \propB * \always \prop \proves {\upd}_1 \always \propB
187 188 189
  \)
and thus
  \(
Ralf Jung's avatar
Ralf Jung committed
190
  \gname \Mapsto \prop * \gname \Mapsto \propB \proves ({\upd}_1 \always \prop) \Lra ({\upd}_1 \always \propB).
191 192 193 194 195 196
  \)
\end{lem}

\begin{proof}[\lemref{lem:counterexample-invariants-saved-prop-agree}]
\begin{itemize}
  \item We first show
Ralf Jung's avatar
Ralf Jung committed
197
    \[\gname \Mapsto \prop * \gname \Mapsto \propB * \always \prop \proves {\upd}_1 \always \propB.\]
198 199 200 201 202 203 204 205 206 207 208
    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$.
    Hence, it is sufficient to prove
    \[
Ralf Jung's avatar
Ralf Jung committed
209
      \ownGhost{\gname}{\finishtoken} * \gname \Mapsto \prop * \gname \Mapsto \propB * \always \prop \proves {\upd}_1 \always \propB.\]
210 211 212 213 214 215
    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''):
Ralf Jung's avatar
Ralf Jung committed
216
      Since $\always \propB$ is duplicable we use one copy to close the invariant, and retain another to prove ${\upd}_1 \always \propB$.
217 218
    \end{enumerate}
\item By applying the above twice, we easily obtain
Ralf Jung's avatar
Ralf Jung committed
219
\[ \gname \Mapsto \prop * \gname \Mapsto \propB \proves ({\upd}_1 \always \prop) \Lra ({\upd}_1 \always \propB) \]
220 221 222 223 224 225 226
\end{itemize}
\qed \end{proof}
% 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}.
Ralf Jung's avatar
Ralf Jung committed
227
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}_1 \FALSE$ in place of $\FALSE$ in the definition of the predicate $A$:
228
we let \(
Ralf Jung's avatar
Ralf Jung committed
229
  A(\gname) \eqdef \Exists \prop : \Prop. \always (\prop \Ra {\upd}_1 \FALSE) \land \gname \Mapsto \prop\)
230 231 232 233 234 235 236 237
and replay the proof that we have presented above.

%TODO: What about executing a view shift under a later?

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "iris"
%%% End: