ghost-state.tex 11.1 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 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 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 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 135 136 137 138
\section{Extensions of the Base Logic}

In this section we discuss some additional constructions that we will within and on top of the base logic.
These are not ``extensions'' in the sense that they change the proof power of the logic, they just form useful derived principles.

\subsection{Derived rules about base connectives}
We collect here some important and frequently used derived proof rules.
\begin{mathparpagebreakable}
  \infer{}
  {\prop \Ra \propB \proves \prop \wand \propB}

  \infer{}
  {\prop * \Exists\var.\propB \provesIff \Exists\var. \prop * \propB}

  \infer{}
  {\prop * \All\var.\propB \proves \All\var. \prop * \propB}

  \infer{}
  {\always(\prop*\propB) \provesIff \always\prop * \always\propB}

  \infer{}
  {\always(\prop \Ra \propB) \proves \always\prop \Ra \always\propB}

  \infer{}
  {\always(\prop \wand \propB) \proves \always\prop \wand \always\propB}

  \infer{}
  {\always(\prop \wand \propB) \provesIff \always(\prop \Ra \propB)}

  \infer{}
  {\later(\prop \Ra \propB) \proves \later\prop \Ra \later\propB}

  \infer{}
  {\later(\prop \wand \propB) \proves \later\prop \wand \later\propB}

  \infer{}
  {\prop \proves \later\prop}
\end{mathparpagebreakable}

\subsection{Persistent assertions}
We call an assertion $\prop$ \emph{persistent} if $\prop \proves \always\prop$.
These are assertions that ``don't own anything'', so we can (and will) treat them like ``normal'' intuitionistic assertions.

Of course, $\always\prop$ is persistent for any $\prop$.
Furthermore, by the proof rules given in \Sref{sec:proof-rules}, $\TRUE$, $\FALSE$, $t = t'$ as well as $\ownGhost\gname{\mcore\melt}$ and $\mval(\melt)$ are persistent.
Persistence is preserved by conjunction, disjunction, separating conjunction as well as universal and existential quantification and $\later$.



\subsection{Timeless assertions and except-0}

One of the troubles of working in a step-indexed logic is the ``later'' modality $\later$.
It turns out that we can somewhat mitigate this trouble by working below the following \emph{except-0} modality:
\[ \diamond \prop \eqdef \later\FALSE \lor \Prop \]

This modality is useful because there is a class of assertions which we call \emph{timeless} assertions, for which we have
\[ \timeless{\prop} \eqdef \later\prop \proves \diamond\prop  \]
In other words, when working below the except-0 modality, we can \emph{strip away} the later from timeless assertions.

The following ruels can be derived about except-0:
\begin{mathpar}
  \inferH{ex0-mono}
  {\prop \proves \propB}
  {\diamond\prop \proves \diamond\propB}

  \axiomH{ex0-intro}
  {\prop \proves \diamond\prop}

  \axiomH{ex0-idem}
  {\diamond\diamond\prop \proves \diamond\prop}

\begin{array}[c]{rMcMl}
  \diamond{(\prop * \propB)} &\provesIff& \diamond\prop * \diamond\propB \\
  \diamond{(\prop \land \propB)} &\provesIff& \diamond\prop \land \diamond\propB \\
  \diamond{(\prop \lor \propB)} &\provesIff& \diamond\prop \lor \diamond\propB
\end{array}

\begin{array}[c]{rMcMl}
  \diamond{\All x. \prop} &\provesIff& \All x. \diamond{\prop}   \\
  \diamond{\Exists x. \prop} &\provesIff& \Exists x. \diamond{\prop} \\
  \diamond\always{\prop} &\provesIff& \always\diamond{\prop} \\
  \diamond\later\prop &\proves& \later{\prop}
\end{array}
\end{mathpar}

The following rules identify the class of timeless assertions:
\begin{mathparpagebreakable}
\infer
{\vctx \proves \timeless{\prop} \and \vctx \proves \timeless{\propB}}
{\vctx \proves \timeless{\prop \land \propB}}

\infer
{\vctx \proves \timeless{\prop} \and \vctx \proves \timeless{\propB}}
{\vctx \proves \timeless{\prop \lor \propB}}

\infer
{\vctx \proves \timeless{\prop} \and \vctx \proves \timeless{\propB}}
{\vctx \proves \timeless{\prop * \propB}}

\infer
{\vctx \proves \timeless{\prop}}
{\vctx \proves \timeless{\always\prop}}

\infer
{\vctx \proves \timeless{\propB}}
{\vctx \proves \timeless{\prop \Ra \propB}}

\infer
{\vctx \proves \timeless{\propB}}
{\vctx \proves \timeless{\prop \wand \propB}}

\infer
{\vctx,\var:\type \proves \timeless{\prop}}
{\vctx \proves \timeless{\All\var:\type.\prop}}

\infer
{\vctx,\var:\type \proves \timeless{\prop}}
{\vctx \proves \timeless{\Exists\var:\type.\prop}}

\axiom{\timeless{\TRUE}}

\axiom{\timeless{\FALSE}}

\infer
{\text{$\term$ or $\term'$ is a discrete COFE element}}
{\timeless{\term =_\type \term'}}

\infer
{\text{$\melt$ is a discrete COFE element}}
{\timeless{\ownM\melt}}

\infer
{\text{$\melt$ is an element of a discrete CMRA}}
{\timeless{\mval(\melt)}}
\end{mathparpagebreakable}

\subsection{DC logic: Dynamic Composeable Resources}
\label{sec:dc-logic}
139

140
The base logic described in \Sref{sec:base-logic} works over an arbitrary CMRA $\monoid$ defining the structure of the resources.
141 142 143
It turns out that we can generalize this further and permit picking CMRAs ``$\iFunc(\Prop)$'' that depend on the structure of assertions themselves.
Of course, $\Prop$ is just the syntactic type of assertions; for this to make sense we have to look at the semantics.

144
Furthermore, there is a composeability problem with the given logic: if we have one proof performed with CMRA $\monoid_1$, and another proof carried out with a \emph{different} CMRA $\monoid_2$, then the two proofs are actually carried out in two \emph{entirely separate logics} and hence cannot be combined.
145

146 147 148
Finally, in many cases just having a single ``instance'' of a CMRA available for reasoning is not enough.
For example, when reasoning about a dynamically allocated data structure, every time a new instance of that data structure is created, we will want a fresh resource governing the state of this particular instance.
While it would be possible to handle this problem whenever it comes up, it turns out to be useful to provide a general solution.
149

150
The purpose of this section is to describe how we solve these issues.
151

152 153
\paragraph{Picking the resources.}
The key ingredient that we will employ on top of the base logic is to give some more fixed structure to the resources.
154
To instantiate the DC logic (base logic with dynamic composeable resources), the user picks a family of locally contractive bifunctors $(\iFunc_i : \COFEs \to \CMRAs)_{i \in \mathcal{I}}$.
155
(This is in contrast to the base logic, where the user picks a single, fixed CMRA that has a unit.)
156 157 158 159 160

From this, we construct the bifunctor defining the overall resources as follows:
\begin{align*}
  \textdom{ResF}(\cofe^\op, \cofe) \eqdef{}& \prod_{i \in \mathcal I} \mathbb{N} \fpfn \iFunc_i(\cofe^\op, \cofe)
\end{align*}
161
(We will motivate both the use of a product and the finite partial function below.)
162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177
$\textdom{ResF}(\cofe^\op, \cofe)$ is a CMRA by lifting the individual CMRAs pointwise, and it has a unit (using the empty finite partial functions).
Furthermore, since the $\iFunc_i$ are locally contractive, so is $\textdom{ResF}$.

Now we can write down the recursive domain equation:
\[ \iPreProp \cong \UPred(\textdom{ResF}(\iPreProp, \iPreProp)) \]
$\iPreProp$ is a COFE defined as the fixed-point of a locally contractive bifunctor.
This fixed-point exists and is unique by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}.
We do not need to consider how the object is constructed. 
We only need the isomorphism, given by
\begin{align*}
  \Res &\eqdef \textdom{ResF}(\iPreProp, \iPreProp) \\
  \iProp &\eqdef \UPred(\Res) \\
	\wIso &: \iProp \nfn \iPreProp \\
	\wIso^{-1} &: \iPreProp \nfn \iProp
\end{align*}

178
Notice that $\iProp$ is the semantic model of assertions for the base logic described in \Sref{sec:base-logic} with $\Res$:
179
\[ \Sem{\Prop} \eqdef \iProp = \UPred(\Res) \]
180 181
Effectively, we just defined a way to instantiate the base logic with $\Res$ as the CMRA of resources, while providing a way for $\Res$ to depend on $\iPreProp$, which is isomorphic to $\Sem\Prop$.

182
We thus obtain all the rules of \Sref{sec:base-logic}, and furthermore, we can use the maps $\wIso$ and $\wIso^{-1}$ \emph{in the logic} to convert between logical assertions $\Sem\Prop$ and the domain $\iPreProp$ which is used in the construction of $\Res$ -- so from elements of $\iPreProp$, we can construct elements of $\Sem{\textlog M}$, which are the elements that can be owned in our logic.
183

184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222
\paragraph{Proof composeability.}
To make our proofs composeable, we \emph{generalize} our proofs over the family of functors.
This is possible because we made $\Res$ a \emph{product} of all the CMRAs picked by the user, and because we can actually work with that product ``pointwise''.
So instead of picking a \emph{concrete} family, proofs will assume to be given an \emph{arbitrary} family of functors, plus a proof that this family \emph{contains the functors they need}.
Composing two proofs is then merely a matter of conjoining the assumptions they make about the functors.
Since the logic is entirely parametric in the choice of functors, there is no trouble reasoning without full knowledge of the family of functors.

Only when the top-level proof is completed we will ``close'' the proof by picking a concrete family that contains exactly those functors the proof needs.

\paragraph{Dynamic resources.}
Finally, the use of finite partial functions lets us have as many instances of any CMRA as we could wish for:
Because there can only ever be finitely many instances already allocated, it is always possible to create a fresh instance with any desired (valid) starting state.
This is best demonstrated by giving some proof rules.

So let us first define the notion of ghost ownership that we use in this logic.
Assuming that the family of functors contains the functor $\Sigma_i$ at index $i$, and furthermore assuming that $\monoid_i = \Sigma_i(\iPreProp, \iPreProp)$, given some $\melt \in \monoid_i$ we define:
\[ \ownGhost\gname{\melt:\monoid_i} \eqdef \ownM{(\ldots, \emptyset, i:\set{\gname \mapsto \melt}, \emptyset, \ldots)} \]
This is ownership of the pair (element of the product over all the functors) that has the empty finite partial function in all components \emph{except for} the component corresponding to index $i$, where we own the element $\melt$ at index $\gname$ in the finite partial function.

We can show the following properties for this form of ownership:
\begin{mathparpagebreakable}
  \inferH{res-alloc}{\text{$G$ infinite} \and \melt \in \mval_{M_i}}
  {  \TRUE \proves \upd \Exists\gname\in G. \ownGhost\gname{\melt : M_i}
  }
  \and
  \inferH{res-update}
    {\melt \mupd_{M_i} B}
    {\ownGhost\gname{\melt : M_i} \proves \upd \Exists \meltB\in B. \ownGhost\gname{\meltB : M_i}}

  \inferH{res-empty}
  {\text{$\munit$ is a unit of $M_i$}}
  {\TRUE \proves \upd \ownGhost\gname\munit}
  
  \axiomH{res-op}
    {\ownGhost\gname{\melt : M_i} * \ownGhost\gname{\meltB : M_i} \provesIff \ownGhost\gname{\melt\mtimes\meltB : M_i}}

  \axiomH{res-valid}
    {\ownGhost\gname{\melt : M_i} \Ra \mval_{M_i}(\melt)}

223 224 225
  \inferH{res-timeless}
    {\text{$\melt$ is a discrete COFE element}}
    {\timeless{\ownGhost\gname{\melt : M_i}}}
226
\end{mathparpagebreakable}
227

228
Below, we will always work within (an instance of) the DC logic.
229 230
Whenever a CMRA is used in a proof, we implicitly assume it to be available in the global family of functors.
We will typically leave the $M_i$ implicit when asserting ghost ownership, as the type of $\melt$ will be clear from the context.
231 232 233 234 235 236 237



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