@@ -83,10 +83,10 @@ The theorem is stated as general as possible so that it also applies to previous
\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:
Assume a higher-order separation logic with $\always$ and an update modality with a binary mask ${\pvs}_{\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}
{}{{\pvs}_0 \prop\proves{\pvs}_1 \prop}
\end{mathpar}
\noindent
...
...
@@ -95,25 +95,25 @@ The theorem is stated as general as possible so that it also applies to previous
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:
@@ -123,7 +123,7 @@ The theorem is stated as general as possible so that it also applies to previous
\end{mathpar}
\noindent
Then $\TRUE\proves{\upd}_1\FALSE$.
Then $\TRUE\proves{\pvs}_1\FALSE$.
\end{thm}
...
...
@@ -132,7 +132,7 @@ Then, using the standard proof rules for invariants, we show that it satisfies \
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}_0$ and ${\upd}_1$ to be the fancy update modalities $\pvs[\emptyset]$
% Taking ${\pvs}_0$ and ${\pvs}_1$ 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
...
...
@@ -167,14 +167,14 @@ We can show variants of \ruleref{sprop-agree} and \ruleref{sprop-alloc} for the
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$.
We have to show the allocation rule \[\proves{\pvs}_1\Exists\gname. \gname\Mapsto\prop.\]
From \ruleref{eq:start-alloc} we have a $\gname$ such that ${\pvs}_0\ownGhost\gname\starttoken$ holds and hence from \ruleref{eq:update-weaken-mask} we have ${\pvs}_1\ownGhost\gname\starttoken$.
Since we are proving a goal of the form ${\pvs}_1 R$ we may assume $\ownGhost\gname\starttoken$.
Thus for any $\prop$ we have ${\pvs}_1\left(\ownGhost{\gname}{\starttoken}\lor\ownGhost\gname\finishtoken*\prop\right)$.
Again since our goal is still of the form ${\pvs}_1$ 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 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}_1\always\propB$.
Since $\always\propB$ is duplicable we use one copy to close the invariant, and retain another to prove ${\pvs}_1\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.
...
...
@@ -224,9 +225,9 @@ and thus
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}_1\FALSE$ in place of $\FALSE$ in the definition of the predicate $A$:
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 ${\pvs}_1\FALSE$ in place of $\FALSE$ in the definition of the predicate $A$:
