\melt\equiv\meltB\eqdef{}&\melt.\aginjV = \meltB.\aginjV\land\All n. n \in\melt.\aginjV\Ra\melt.\aginjc(n) \nequiv{n}\meltB.\aginjc(n) \\
\melt\nequiv{n}\meltB\eqdef{}& (\All m \leq n. m \in\melt.\aginjV\Lra m \in\meltB.\aginjV) \land (\All m \leq n. m \in\melt.\aginjV\Ra\melt.\aginjc(m) \nequiv{m}\meltB.\aginjc(m)) \\
\mval_n \eqdef{}&\setComp{\melt\in\agm(\cofe)}{ n \in\melt.\aginjV\land\All m \leq n. \melt.\aginjc(n) \nequiv{m}\melt.\aginjc(m) }\\
\All n. n \in\melt.V \Ra\melt.c(n) \nequiv{n}\meltB.c(n) \\
% \All n \in {\melt.V}.\, \melt.x \nequiv{n} \meltB.x \\
\melt\nequiv{n}\meltB\eqdef{}& (\All m \leq n. m \in\melt.V \Lra m \in\meltB.V) \land (\All m \leq n. m \in\melt.V \Ra\melt.c(m) \nequiv{m}\meltB.c(m)) \\
\mval_n \eqdef{}&\setComp{\melt\in\agm(\cofe)}{ n \in\melt.V \land\All m \leq n. \melt.c(n) \nequiv{m}\melt.c(m) }\\
\mcore\melt\eqdef{}&\melt\\
\melt\mtimes\meltB\eqdef{}& (\melt.\aginjc, \setComp{n}{n \in\melt.\aginjV\land n \in\meltB.\aginjV\land\melt\nequiv{n}\meltB})
\melt\mtimes\meltB\eqdef{}&\left(\melt.c, \setComp{n}{n \in\melt.V \land n \in\meltB.V \land\melt\nequiv{n}\meltB}\right)
\end{align*}
Note that the carrier $\agm(\cofe)$ is a \emph{record} consisting of the two fields $\aginjc$ and $\aginjV$.
%Note that the carrier $\agm(\cofe)$ is a \emph{record} consisting of the two fields $c$ and $V$.
$\agm(-)$ is a locally non-expansive functor from $\COFEs$ to $\CMRAs$.
You can think of the $\aginjc$ as a \emph{chain} of elements of $\cofe$ that has to converge only for $n \in\aginjV$ steps.
You can think of the $c$ as a \emph{chain} of elements of $\cofe$ that has to converge only for $n \in V$ steps.
The reason we store a chain, rather than a single element, is that $\agm(\cofe)$ needs to be a COFE itself, so we need to be able to give a limit for every chain of $\agm(\cofe)$.
However, given such a chain, we cannot constructively define its limit: Clearly, the $\aginjV$ of the limit is the limit of the $\aginjV$ of the chain.
However, given such a chain, we cannot constructively define its limit: Clearly, the $V$ of the limit is the limit of the $V$ of the chain.
But what to pick for the actual data, for the element of $\cofe$?
Only if $\aginjV=\mathbb{N}$ we have a chain of $\cofe$ that we can take a limit of; if the $\aginjV$ is smaller, the chain ``cancels'', \ie stops converging as we reach indices $n \notin\aginjV$.
Only if $V =\mathbb{N}$ we have a chain of $\cofe$ that we can take a limit of; if the $V$ is smaller, the chain ``cancels'', \ie stops converging as we reach indices $n \notin V$.
To mitigate this, we apply the usual construction to close a set; we go from elements of $\cofe$ to chains of $\cofe$.
We define an injection $\aginj$ into $\agm(\cofe)$ as follows:
...
...
@@ -160,12 +159,12 @@ All cases of composition go to $\bot$.
\mcore{\exinj(x)}\eqdef{}&\mnocore&
\mcore{\bot}\eqdef{}&\bot
\end{align*}
Remember that $\mnocore$ is the ``dummy'' element in $\maybe\monoid$ indicating (in this case) that $\exinj(x)$ has no core.
The step-indexed equivalence is inductively defined as follows:
Hereinafter we assume the global CMRA functor (served up as a parameter to Iris) is obtained from a family of functors $(F_i)_{i \in I}$ for some finite $I$ by picking
Hereinafter we assume the global CMRA functor (served up as a parameter to Iris) is obtained from a family of functors $(\iFunc_i)_{i \in I}$ for some finite $I$ by picking
We don't care so much about what concretely $\textlog{GhName}$ is, as long as it is countable and infinite.
With $M_i \eqdefF_i(\iProp)$, we write $\ownGhost{\gname}{\melt : M_i}$ (or just $\ownGhost{\gname}{\melt}$ if $M_i$ is clear from the context) for $\ownGGhost{[i \mapsto[\gname\mapsto\melt]]}$.
With $M_i \eqdef\iFunc_i(\iProp)$, we write $\ownGhost{\gname}{\melt : M_i}$ (or just $\ownGhost{\gname}{\melt}$ if $M_i$ is clear from the context) for $\ownGGhost{[i \mapsto[\gname\mapsto\melt]]}$.
In other words, $\ownGhost{\gname}{\melt : M_i}$ asserts that in the current state of monoid $M_i$, the ``ghost location'' $\gname$ is allocated and we own piece $\melt$.
From~\ruleref{pvs-update}, \ruleref{vs-update} and the frame-preserving updates in~\Sref{sec:prodm} and~\Sref{sec:fpfnm}, we have the following derived rules.
Here we define $\wpre{\expr_\f}[\mask]{\Ret\var.\prop}\eqdef\TRUE$ if $\expr_\f=\bot$ (remember that our stepping relation can, but does not have to, define a forked-off expression).
