Newer
Older
\section{Extensions of the Base Logic}

Ralf Jung
committed
In this section we discuss some additional constructions that we define within and on top of the base logic.

Ralf Jung
committed
These are not ``extensions'' in the sense that they change the proof power of the logic, they just form useful derived principles.

Ralf Jung
committed
We collect here some important and frequently used derived proof rules.

Ralf Jung
committed
\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}
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
\end{mathparpagebreakable}
Verifying that existential quantifiers commute with separating conjunction requires an intermediate step using a magic wand: From $P * \exists x, Q \vdash \Exists x. P * Q$ we can deduce $\Exists x. Q \vdash P \wand \Exists x. P * Q$ and then proceed via $\exists$-elimination.
\subsection{Derived Rules about Modalities}
Iris comes with 4 built-in modalities ($\always$, $\plainly$, $\upd$ and $\later$) and, as we will see, plenty of derived modalities.
However, almost all of them fall into one of two categories (except for $\later$, as we will see): they are either \emph{always-style} modalities (``something holds in all/many (future) worlds'') or \emph{eventually-style} modalities (``something holds in a possible (future) world'').
\emph{Eventually-style modalities} are characterized by being easy to ``add''/introduce, but hard to ``remove''/eliminate.
Consider, for example, the basic update modality $\upd$:
we have $\prop \proves \upd\prop$ (\ruleref{upd-intro}), but the inverse direction does not hold.
Instead, from \ruleref{upd-mono} and \ruleref{upd-trans}, we can derive the following elimination principle:
\begin{mathpar}
\infer[upd-E]
{\prop \proves \upd\propB}
{\upd\prop \proves \upd\propB}
\end{mathpar}
In other words, we can remove an $\upd$ in front of an assumption \emph{if} the goal is itself wrapped in $\upd$.
Another way to view this rule is to think of it as a \emph{bind rule}.
Indeed, together with \ruleref{upd-intro}, this rule shows that $\upd$ forms a monad.
\emph{Always-style modalities}, on the other hand, are easy to ``remove''/eliminate, but hard to ``add''/introduce.
The most widely used example of that in Iris is the persistence modality $\always$:
we have $\always\prop \proves \prop$ (\ruleref{pers-elim}), but the inverse direction does not hold.
Instead, from \ruleref{pers-mono} and $\always{\prop} \proves \always\always\prop$, we can derive the following introduction principle:
\begin{mathpar}
\infer[$\always$-I]
{\always\prop \proves \propB}
{\always\prop \proves \always\propB}
\end{mathpar}
In other words, we can remove an $\always$ from the goal \emph{if} all our assumptions are wrapped in $\always$.
This matches the algebraic structure of a comonad.
In particular, both eventually-style and always-style modalities are \emph{idempotent}: we have $\upd\upd\prop \provesIff \upd\prop$ and $\always\always\prop \provesIff \always\prop$.
Beyond this, all modalities come with plenty of rules that show how they commute around other connectives and modalities.
And, of course, they come with a few ``defining rules'' that give the modalities their individual meaning, \ie for the update modality, that would be \ruleref{upd-update}.
In the following, we briefly discuss each of the modalities.
\paragraph{Update modality.}
As already mentioned, the update modality is an eventually-style modality:
\begin{mathpar}
\inferhref{upd-E}{upd-elim}
{\prop \proves \upd\propB}
{\upd\prop \proves \upd\propB}
\inferH{upd-idemp}
{}{\upd\upd\prop \provesIff \upd\prop}
\end{mathpar}
Beyond this (and the obvious variant of \ruleref{upd-frame} that exploits commutativity of separating conjunction), there are no outstandingly interesting derived rules.
\paragraph{Persistence modality.}
As already mentioned, the persistence modality is an always-style modality:
\begin{mathpar}
\inferhref{$\always$-I}{pers-intro}
{\always\prop \proves \propB}
{\always\prop \proves \always\propB}
\inferhref{$\always$-idemp}{pers-idemp}
{}{\always\always\prop \provesIff \always\prop}
\end{mathpar}
Some further interesting derived rules include:
\begin{mathparpagebreakable}
\infer{}
{\always(\prop\land\propB) \provesIff \always\prop \land \always\propB}
\infer{}
{\always(\prop\lor\propB) \provesIff \always\prop \lor \always\propB}

Ralf Jung
committed
\infer{}
{\always\TRUE \provesIff \TRUE}
\infer{}
{\always\FALSE \provesIff \FALSE}
\\

Ralf Jung
committed
\infer{}
{\always(\prop*\propB) \provesIff \always\prop * \always\propB}
\infer{}
{\always\prop*\propB \provesIff \always\prop \land \propB}
\infer{}
{\always(\prop \wand \propB) \provesIff \always(\prop \Ra \propB)}
\\

Ralf Jung
committed
\infer{}
{\always(\prop \Ra \propB) \proves \always\prop \Ra \always\propB}
\infer{}
{\always(\prop \wand \propB) \proves \always\prop \wand \always\propB}
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
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
\end{mathparpagebreakable}
In particular, the persistence modality commutes around conjunction, disjunction, separating conjunction as well as universal and existential quantification.
Commuting around conjunction can be derived from the primitive rule that says it commutes around universal quantification (as conjunction is equivalent to a universal quantification of a Boolean), and similar for disjunction.
$\TRUE \provesIff \always\TRUE$ (which is basically persistence ``commuting around'' the nullary operator $\TRUE$) can be derived via $\always$ commuting with universal quantification ranging over the empty type.
A similar rule holds for $\FALSE$.
Moreover, if (at least) one conjunct is below the persistence modality, then conjunction and separating conjunction coincide.
\paragraph{Plainness modality.}
The plainness modality is very similar to the persistence modality (in fact, we have $\plainly\prop \proves \always\prop$, but the inverse does not hold).
It is always-style:
\begin{mathpar}
\infer[$\plainly$-I]
{\plainly\prop \proves \propB}
{\plainly\prop \proves \plainly\propB}
\infer{}{\plainly\plainly\prop \provesIff \plainly\prop}
\end{mathpar}
It also commutes around separating conjunction, conjunction, disjunction, universal and existential quantification (and $\TRUE$ and $\FALSE$).
The key difference to the persistence modality $\always$ is that $\plainly$ provides a \emph{propositional extensionality} principle:
\[ \plainly ( ( P \Ra Q) \land (Q \Ra P ) ) \proves P =_{\Prop} Q \]
In contrast, $\always$ permits using some forms of ghost state ($\ownM\melt \proves \always{\ownM{\mcore\melt}}$).
Having both of these principles for the same modality would lead to a contradiction:
imagine we have an RA with elements $\melt$, $\meltB$ such that $\mcore\melt$ is incompatible with $\meltB$ (\ie $\neg\mvalFull(\mcore\melt \mtimes \meltB)$).
Then we can prove:
\[
\ownM{\mcore\melt} \proves
\always\ownM{\mcore\melt} \proves
\always ( ( \FALSE \Ra \ownM\meltB ) \land ( \ownM\meltB \Ra \FALSE ) )
\]
The first implication is trivial, the second implication follows because $\always\ownM{\mcore\melt} \land \ownM\meltB \proves \ownM{\mcore\melt} * \ownM\meltB \proves \mval(\mcore\melt \mtimes \meltB)$.
But now, if we had propositional extensionality for $\always$ the way we do for $\plainly$, we could deduce $\FALSE =_{\Prop} \ownM\meltB$, and that is clearly wrong.
This issue arises because $\always$, as we have seen, still lets us use some resources from the context, while propositional equality has to hold completely disregarding current resources.
\paragraph{Later modality.}
The later modality is the ``odd one out'' in the sense that it is neither eventually-style nor always-style, because it is not idempotent:%
\footnote{This means $\later$ is neither a monad nor a comonad---it does form an applicative functor, though.}
with $\later$, the number of times the modality is applied matters, and we can get rid of \emph{exactly one} layer of $\later$ in the assumptions only by doing the same in the conclusion (\ruleref{later-mono}).
Some derived rules:
\begin{mathparpagebreakable}
\inferhref{L{\"o}b}{Loeb}
{}
{(\later\prop\Ra\prop) \proves \prop}

Ralf Jung
committed
\infer{}
{\later(\prop \Ra \propB) \proves \later\prop \Ra \later\propB}
\infer{}
{\later(\prop \wand \propB) \proves \later\prop \wand \later\propB}
\\
\infer{}
{\later(\prop\land\propB) \provesIff \later\prop \land \later\propB}

Ralf Jung
committed
{\later(\prop\lor\propB) \provesIff \later\prop \lor \later\propB}
\infer{\text{$\type$ is inhabited}}
{\later(\Exists x:\type. \prop) \provesIff \Exists x:\type. \later\prop}

Ralf Jung
committed
\infer{}
{\later\TRUE \provesIff \TRUE}
\infer{}
{\later(\prop*\propB) \provesIff \later\prop * \later\propB}
\infer{}
{\later\always\prop \provesIff \always\later\prop}
\infer{}
{\later\plainly\prop \provesIff \plainly\later\prop}
\end{mathparpagebreakable}
Noteworthy here is the fact that Löb induction (\ruleref{Loeb}) can be derived from $\later$-introduction and the fact that we can take fixed-points of functions where the recursive occurrences are below $\later$~\cite{Loeb}.%
\footnote{Also see \url{https://en.wikipedia.org/wiki/L\%C3\%B6b\%27s_theorem}.}
Also, $\later$ commutes over separating conjunction, conjunction, disjunction, universal quantification and \emph{non-empty} existential quantification, as well as both the persistence and the plainness modality.
\subsection{Persistent Propositions}
We call a proposition $\prop$ \emph{persistent} if $\prop \proves \always\prop$.
These are propositions that ``do not own anything'', so we can (and will) treat them like ``normal'' intuitionistic propositions.

Ralf Jung
committed
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 Propositions and Except-0}

Ralf Jung
committed
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 \]
Except-0 satisfies the usual laws of a ``monadic'' modality (similar to, \eg the update modalities):

Ralf Jung
committed
\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}
In particular, from \ruleref{ex0-mono} and \ruleref{ex0-idem} we can derive a ``bind''-like elimination rule:
\begin{mathpar}
\inferH{ex0-elim}
{\prop \proves \diamond\propB}
{\diamond\prop \proves \diamond\propB}
\end{mathpar}
This modality is useful because there is a class of propositions which we call \emph{timeless} propositions, 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 propositions (using \ruleref{ex0-elim}):
\begin{mathpar}
\inferH{ex0-timeless-strip}{\timeless{\prop} \and \prop \proves \diamond\propB}
{\later\prop \proves \diamond\propB}
\end{mathpar}
In fact, it turns out that we can strip away later from timeless propositions even when working under the later modality:
\begin{mathpar}
\inferH{later-timeless-strip}{\timeless{\prop} \and \prop \proves \later \propB}
{\later\prop \proves \later\propB}
\end{mathpar}
This follows from $\later \prop \proves \later\FALSE \lor \prop$, and then by straightforward disjunction elimination.

Ralf Jung
committed
The following rules identify the class of timeless propositions:

Ralf Jung
committed
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
\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 OFE element}}

Ralf Jung
committed
{\timeless{\term =_\type \term'}}
\infer
{\text{$\melt$ is a discrete OFE element}}

Ralf Jung
committed
{\timeless{\ownM\melt}}
\infer
{\text{$\melt$ is an element of a discrete camera}}

Ralf Jung
committed
{\timeless{\mval(\melt)}}
\end{mathparpagebreakable}

Ralf Jung
committed
\subsection{Dynamic Composeable Higher-Order Resources}
\label{sec:composeable-resources}
The base logic described in \Sref{sec:base-logic} works over an arbitrary camera $\monoid$ defining the structure of the resources.
It turns out that we can generalize this further and permit picking cameras ``$\iFunc(\Prop)$'' that depend on the structure of propositions themselves.
Of course, $\Prop$ is just the syntactic type of propositions; for this to make sense we have to look at the semantics.
Furthermore, there is a composability problem with the given logic: if we have one proof performed with camera $\monoid_1$, and another proof carried out with a \emph{different} camera $\monoid_2$, then the two proofs are actually carried out in two \emph{entirely separate logics} and hence cannot be combined.
Finally, in many cases just having a single ``instance'' of a camera 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.
The purpose of this section is to describe how we solve these issues.
\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.
To instantiate the logic with dynamic higher-order ghost state, the user picks a family of locally contractive bifunctors $(\iFunc_i : \COFEs^\op \times \COFEs \to \CMRAs)_{i \in \mathcal{I}}$.

Ralf Jung
committed
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
(This is in contrast to the base logic, where the user picks a single, fixed camera that has a unit.)
From this, we construct the bifunctor defining the overall resources as follows:
\begin{align*}
\GName \eqdef{}& \nat \\
\textdom{ResF}(\ofe^\op, \ofe) \eqdef{}& \prod_{i \in \mathcal I} \GName \fpfn \iFunc_i(\ofe^\op, \ofe)
\end{align*}
We will motivate both the use of a product and the finite partial function below.
$\textdom{ResF}(\ofe^\op, \ofe)$ is a camera by lifting the individual cameras pointwise, and it has a unit (using the empty finite partial function).
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)) \]
Here, $\iPreProp$ is a COFE defined as the fixed-point of a locally contractive bifunctor, which exists and is unique up to isomorphism by \thmref{thm:america_rutten}, so we obtain some object $\iPreProp$ such that:
\begin{align*}
\Res &\eqdef \textdom{ResF}(\iPreProp, \iPreProp) \\
\iProp &\eqdef \UPred(\Res) \\
\wIso &: \iProp \nfn \iPreProp \\
\wIso^{-1} &: \iPreProp \nfn \iProp \\
\wIso(\wIso^{-1}(x)) &\eqdef x \\
\wIso^{-1}(\wIso(x)) &\eqdef x
\end{align*}
Now we can instantiate the base logic described in \Sref{sec:base-logic} with $\Res$ as the chosen camera:
\[ \Sem{\Prop} \eqdef \UPred(\Res) \]
We obtain that $\Sem{\Prop} = \iProp$.
Effectively, we just defined a way to instantiate the base logic with $\Res$ as the camera of resources, while providing a way for $\Res$ to depend on $\iPreProp$, which is isomorphic to $\Sem\Prop$.
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 propositions $\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.
\paragraph{Proof composability.}
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 cameras 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 camera 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:\mapsingleton \gname \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)}
\inferH{res-timeless}
{\text{$\melt$ is a discrete OFE element}}
{\timeless{\ownGhost\gname{\melt : M_i}}}
\end{mathparpagebreakable}
Below, we will always work within (an instance of) the logic as described here.
Whenever a camera 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.