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: