The (C)OFE structure on many types can be easily obtained by pointwise lifting of the structure of the components.
This is what we do for option $\maybe\cofe$, product $(M_i)_{i \in I}$ (with $I$ some finite index set), sum $\cofe+\cofe'$ and finite partial functions $K \fpfn\monoid$ (with $K$ infinite countable).
\subsection{Next (type-level later)}
\subsection{Next (Type-Level Later)}
Given a OFE $\cofe$, we define $\latert\cofe$ as follows (using a datatype-like notation to define the type):
\begin{align*}
...
...
@@ -51,7 +51,7 @@ connective.
\clearpage
\section{RA and CMRA constructions}
\section{RA and CMRA Constructions}
\subsection{Product}
\label{sec:prodm}
...
...
@@ -116,7 +116,7 @@ We can easily extend this to a full CMRA by defining a suitable core, namely
\end{align*}
Notice that this core is total, as the result always lies in $\maybe\monoid$ (rather than in $\maybe{\mathord{\maybe\monoid}}$).
\subsection{Finite partial function}
\subsection{Finite Partial Functions}
\label{sec:fpfnm}
Given some infinite countable $K$ and some CMRA $\monoid$, the set of finite partial functions $K \fpfn\monoid$ is equipped with a CMRA structure by lifting everything pointwise.
Given a state-transition system~(STS, \ie a directed graph) $(\STSS, {\stsstep}\subseteq\STSS\times\STSS)$, a set of tokens $\STST$, and a labeling $\STSL: \STSS\ra\wp(\STST)$ of \emph{protocol-owned} tokens for each state, we construct an RA modeling an authoritative current state and permitting transitions given a \emph{bound} on the current state and a set of \emph{locally-owned} tokens.
Sometimes it is necessary to maintain invariants that we need to open non-atomically.
Clearly, for this mechanism to be sound we need something that prevents us from opening the same invariant twice, something like the masks that avoid reentrancy on the ``normal'', atomic invariants.
In this section we discuss some additional constructions that we define 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}
\subsection{Derived Rules about Base Connectives}
We collect here some important and frequently used derived proof rules.
\begin{mathparpagebreakable}
\infer{}
...
...
@@ -42,7 +42,7 @@ We collect here some important and frequently used derived proof rules.
Noteworthy here is the fact that $\prop\proves\later\prop$ can be derived from Löb induction, and $\TRUE\proves\plainly\TRUE$ can be derived via $\plainly$ commuting with universal quantification ranging over the empty type $0$.
\subsection{Persistent assertions}
\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.
...
...
@@ -52,7 +52,7 @@ Persistence is preserved by conjunction, disjunction, separating conjunction as
\subsection{Timeless assertions and except-0}
\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:
In this section we provide proofs of some logical inconsistencies that arise when slight changes are made to the Iris logic.
\subsection{Saved propositions without a later}
\subsection{Saved Propositions without a Later}
\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.
...
...
@@ -75,7 +75,7 @@ With this lemma in hand, the proof of \thmref{thm:counterexample-1} is simple.
Together with the rule \ruleref{sprop-alloc} we thus derive $\upd\FALSE$.
\end{proof}
\subsection{Invariants without a later}
\subsection{Invariants without a Later}
\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.