Ralf Jung committed Dec 10, 2017 1 \section{Logical Paradoxes}  Ralf Jung committed Jan 23, 2017 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 committed Dec 10, 2017 7 \subsection{Saved Propositions without a Later}  Ralf Jung committed Jan 23, 2017 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}  Robbert Krebbers committed Dec 10, 2017 16 If there exists a type $\GName$ and a proposition $\_ \Mapsto \_ : \GName \to \Prop \to \Prop$ associating names $\gamma : \GName$ to propositions and satisfying:  Ralf Jung committed Jan 23, 2017 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$.  Robbert Krebbers committed Dec 10, 2017 31 Notice that these are immutable locations, so the maps-to proposition is persistent.  Ralf Jung committed Jan 23, 2017 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 committed Dec 10, 2017 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.}  Ralf Jung committed Jan 23, 2017 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. %  Robbert Krebbers committed Dec 10, 2017 39 The key to proving \thmref{thm:counterexample-1} is the following proposition:  Ralf Jung committed Jan 23, 2017 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 committed Dec 10, 2017 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.  Robbert Krebbers committed Dec 10, 2017 47 In other words, $\prop$ says that the proposition named $\gname$ expresses its own negation.  Ralf Jung committed Jan 23, 2017 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 committed Dec 10, 2017 78 \subsection{Invariants without a Later}  Ralf Jung committed Jan 23, 2017 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  Robbert Krebbers committed Dec 10, 2017 93  Assume a type $\InvName$ and a proposition $\knowInv{\cdot}{\cdot} : \InvName \to \Prop \to \Prop$ satisfying:  Ralf Jung committed Jan 23, 2017 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 committed Aug 13, 2018 135 % Taking ${\upd}_0$ and ${\upd}_1$ to be the fancy update modalities $\pvs[\emptyset]$  Ralf Jung committed Jan 23, 2017 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 committed Aug 13, 2018 170  $$\proves {\upd}_1 \Exists \gname. \gname \Mapsto \prop(\gname)$$.  Ralf Jung committed Jan 23, 2017 171 172 \end{lem} \begin{proof}  Ralf Jung committed Aug 13, 2018 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$.  Ralf Jung committed Jan 23, 2017 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 committed Aug 13, 2018 186  \gname \Mapsto \prop * \gname \Mapsto \propB * \always \prop \proves {\upd}_1 \always \propB  Ralf Jung committed Jan 23, 2017 187 188 189 $$ and thus $$ Ralf Jung committed Aug 13, 2018 190  \gname \Mapsto \prop * \gname \Mapsto \propB \proves ({\upd}_1 \always \prop) \Lra ({\upd}_1 \always \propB).  Ralf Jung committed Jan 23, 2017 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 committed Aug 13, 2018 197  $\gname \Mapsto \prop * \gname \Mapsto \propB * \always \prop \proves {\upd}_1 \always \propB.$  Ralf Jung committed Jan 23, 2017 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 committed Aug 13, 2018 209  \ownGhost{\gname}{\finishtoken} * \gname \Mapsto \prop * \gname \Mapsto \propB * \always \prop \proves {\upd}_1 \always \propB.$  Ralf Jung committed Jan 23, 2017 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 committed Aug 13, 2018 216  Since $\always \propB$ is duplicable we use one copy to close the invariant, and retain another to prove ${\upd}_1 \always \propB$.  Ralf Jung committed Jan 23, 2017 217 218  \end{enumerate} \item By applying the above twice, we easily obtain  Ralf Jung committed Aug 13, 2018 219 $\gname \Mapsto \prop * \gname \Mapsto \propB \proves ({\upd}_1 \always \prop) \Lra ({\upd}_1 \always \propB)$  Ralf Jung committed Jan 23, 2017 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 committed Aug 13, 2018 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$:  Ralf Jung committed Jan 23, 2017 228 we let $$ Ralf Jung committed Aug 13, 2018 229  A(\gname) \eqdef \Exists \prop : \Prop. \always (\prop \Ra {\upd}_1 \FALSE) \land \gname \Mapsto \prop$$  Ralf Jung committed Jan 23, 2017 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: