identifiers that do not appear elsewhere in a configuration.

§.§ Dynamic Semantics

In order to avoid duplicating rules depending on whether reads are
destructive or not, we define the following helper function:

\[
\begin{array}{lrcll}
\Get(F[x \mapsto v],             & \mathbf{drop}\ x) & = & (v, F[x \mapsto \mathbf{undef}]) \\
\Get(F[x \mapsto (k, \iota)],    & x)                & = & ((k, \iota), F[x \mapsto (k, \iota)]) & \text{ if } k \not\eq \Var \land k \not\eq \Iso \\
\Get(F,                          & use)              & = & \FUndef & \text{ otherwise } \\
\end{array}
\]

where $\FUndef$ denotes the undefined value.

$\xrightarrow{\Eff}$ 'Region semantics

§.§.§ Helper Functions and Predicates

We use the following helper definitions:

Viewpoint adaptation of a value amounts to viewpoint adaptation on
its capability (defined in Section <ref>).

\[
\VPA{k}{(k'~\iota)} = (\VPA{k}{k'})~\iota
\]

We can look up objects in a store $S$ given their identifier.

\[
\begin{array}{rcl}
\mathsf{load}((\iota \mapsto o, S), \iota') & = &
\begin{cases}
o & \text{if } \iota = \iota'\\
\mathsf{load}(S, \iota') & \text{otherwise}
\end{cases}\\
\mathsf{load}(\varepsilon, \iota') & = & \FUndef
\end{array}
\]

Looking up an object on the region stack goes through the local
stores of each frame from the top down.

\[
\begin{array}{rcl}
\mathsf{stack\_load}((r, S, F) :: RS, \iota) & = &
\begin{cases}
o & \text{if } \mathsf{load}(S, \iota) = o\\
\mathsf{stack\_load}(S, \iota) & \text{otherwise}
\end{cases}\\
\mathsf{stack\_load}(\varepsilon, \iota) & = & \FUndef
\end{array}
\]

Looking up an object on the heap goes through the regions left to

\[
\begin{array}{rcl}
\mathsf{heap\_load}(H_1 * H_2, \iota) & = &
\begin{cases}
o & \text{if } \mathsf{heap\_load}(H_1, \iota) = o\\
\mathsf{heap\_load}(H_2, \iota) & \text{otherwise}
\end{cases}\\
\mathsf{heap\_load}((r, S), \iota) & = & \mathsf{load}(S, \iota)
\]

The top-level lookup function $\mathsf{cfg\_load}$ performs a
lookup on a given stack and heap using the helper functions above.
Note that an object identifier $\iota$ can only appear in the
domain of a single store $S$ in a well-formed configuration.

\[
\mathsf{cfg\_load}(RS, H, \iota) =
\begin{cases}
o & \text{if } \mathsf{stack\_load}(RS, \iota) = o\\
\mathsf{heap\_load}(H, \iota) & \text{otherwise}
\end{cases}
\]

Similarly, we can update a store $S$ with a new object for a given
object identifier.

\[
\begin{array}{rcl}
\mathsf{store}((\iota \mapsto o, S), \iota', o') & = &
\begin{cases}
\iota \mapsto o', S & \text{if } \iota = \iota'\\
\iota \mapsto o, \mathsf{store}(S, \iota', o') & \text{otherwise}
\end{cases}\\
\mathsf{store}(\varepsilon, \iota', o') & = & \FUndef
\end{array}
\]

When storing an object on the stack, we always store in the
top-most frame, so we don't need a function for traversing the
stack. When storing to the heap, we go from left to right.

\[
\begin{array}{rcl}
\mathsf{heap\_store}(H_1 * H_2, \iota, o) & = &
\begin{cases}
H_1' * H_2 & \text{if } \mathsf{heap\_store}(H_1, \iota, o) = H_1'\\
H_1 * \mathsf{heap\_store}(H_2, \iota, o) & \text{otherwise}
\end{cases}\\
\mathsf{heap\_store}((r, S), \iota, o) & = &
\begin{cases}
(r, S') & \text{if } \mathsf{store}(S, \iota, o) = S'\\
\FUndef    & \text{otherwise}
\end{cases}
\end{array}
\]

When freezing a region, we need to calculate the reachable regions
from the region being frozen. We define a relation
$\mathsf{reachable\_step}$ which holds when a region $R$ has an
object with a reference to an object in another region $R'$.
Calculating the reachable regions amounts to calculating the
transitive closure of $\mathsf{reachable\_step}$.

\[
\begin{array}{l}
\mathsf{reachable\_regions}(R, H) =
\{R' ~|~ \mathsf{reachable\_step}^+(R, R')\}\\
\quad\textit{where}\\
\quad\mathsf{reachable\_step}(R, R') \equiv
R' \in H
\land o[f\mapsto \iota] \in \mathbf{rng}(R.S)
\land \iota \in \mathbf{dom}(R'.S)

\end{array}
\]

§.§ Well-Formedness Rules

$\Gammas \vdash \RCfg$Region configuration

$\Gammas;\Delta;\Psi \vdash \RCfg$Region configuration types

$\Gammas;\Delta;\Delta;\Psi \vdash \RS$Region stack types

$\Delta;\Delta;\Psi \vdash H$Region heap types

$\Delta;\Delta \vdash S$Region subheap types

$\Delta;\Gamma \vdash F$Region variable types

$\CLTag \subtag \CL$Subtagging

§.§ Predicates on Graphs

We will now define some predicates used to define the invariants of our system.
These are defined in terms of the object graph of the configuration. Therefore
we first define the set of graphs $\GraphSet$, and a mapping $G: \RCfgSet \to
\GraphSet$, where $\RCfgSet$ is the set of region configurations.

§.§.§ Region Configuration Graph

The the elements of $\GraphSet$ are tuples $(\LocSet, \RefSet)$ of vertices $\LocSet$
(locations) and edges $\RefSet$ (refereces). We represent the vertices
and edges as

\[
\begin{array}{rcll}
\Loc  & ::= & \Heap(r, \iota) ~|~ \Temp(r, \iota) ~|~ \Root(r) & \text{Location} \\
\REF & ::= & \Loc \RefTo{f, k} \Loc' & \text{Reference, marked with field and
\end{array}
\]

We call the set of all locations and references $\AllLocs$ and
$\AllRefs$ respectively.

\[
\begin{aligned}
&\Rid(\Heap(r, \iota)) &=\quad r \\
&\Rid(\Temp(r, \iota)) &=\quad r \\
&\Rid(\Root(r)) &=\quad r
\end{aligned}
\]

Since all $\Loc$ contains a region id $r$, we can define a shorthand $\Loc[\cdot]$ with a hole for $r$ as

\[
\Loc[\cdot] ::= \Heap(\cdot, \iota) ~|~ \Temp(\cdot, \iota) ~|~ \Root(\cdot)
\]

We define $\cupdisj$ as the union of two disjoint sets.

\[
A \cupdisj B = \begin{cases}
A \cup B  & \text{ if } A \cap B = \emptyset \\
\FUndef      & \text{ otherwise}
\end{cases}
\]

where $\FUndef$ denotes the undefined value. In particular,
if any of $A$ or $B$ is $\FUndef$ we let $A \cap B = \FUndef$, and thus $A
\cupdisj B = \FUndef$. For sets $S, S'$, and $A, B \subseteq S$, $f: S \to S'$,
we define $\cupdisj_f$ by

\[
A \cupdisj_f B = \begin{cases}
A \cup B  & \text{ if } I_f(A) \cap I_f(B) = \emptyset \\
\FUndef      & \text{ otherwise}
\end{cases}
\]

where $I_f(A)$ is the image of $f$ restricted to the set $A$. Furthermore
$I_f(\FUndef) = \FUndef$. We call $f$ above a separating function.

For the definition of $G$ we define the separating function $\SepLoc$ as

\[
\begin{array}{lcl}
\SepLoc(\Heap(r, \iota)) & = & \ObjSep(\iota) \\
\SepLoc(\Temp(r, \iota)) & = & \ObjSep(\iota) \\
\SepLoc(\Root(r)) & = & \Root(r)
\end{array}
\]

Assuming $\LocSet^* = \LocSet \cupdisj_\SepLoc \LocSet' \neq \FUndef$ we see that
all object ids in $\LocSet^*$ are unique, and furthermore that there is at most
one $\Root(r)$ for each region id $r$.

We are now ready to start defining the graph of a region configuration $\RCfg$.
We write

\[
G(\RCfglong{RS; \Hop; \Hcl; \Hfr}) = (\LocSet, \RefSet)
\]

\[
\LocSet = \LocRS(RS) \cupdisj_{\SepLoc} \LocH(\Hop) \cupdisj_{\SepLoc} \LocH(\Hcl)
\cupdisj_{\SepLoc} \LocH(\Hfr)
\]

\[
\begin{array}{lcl}
\LocRS((r, S, F)::RS) & = & \LocS^\Temp(S) \cupdisj_\SepLoc \{ \Root(r) \}
\cupdisj_\SepLoc \LocRS(RS) \\
\LocRS(\NilRS) & = & \emptyset \vspace{1em} \\
\LocH(H_1 * H_2) & = & \LocH(H_1) \cupdisj_\SepLoc \LocH(H_2) \\
\LocH((r, S))    & = & \LocS^\Heap(r; S) \vspace{1em} \\
\LocS^\Heap(r; S, \iota \mapsto \_) & = & \LocS^\Heap(r; S) \cupdisj_\SepLoc \{
\Heap(r, \iota) \} \\
\LocS^\Temp(r; S, \iota \mapsto \_) & = & \LocS^\Temp(r; S) \cupdisj_\SepLoc \{
\Temp(r, \iota) \} \\
\LocS^*(\NilS)    & = & \emptyset
\end{array}
\]

Because of the properties of $\SepLoc$ mentioned above (in particular the
uniqueness of object ids $\iota$), given that $\LocSet \neq \FUndef$ we can
define a partial function $\Loc_\LocSet: \Oid \partialto \LocSet$ as

\[
\Loc_\LocSet(\iota) = \begin{cases}
\Heap(r, \iota) & \text{ if } \Heap(r, \iota) \in
\LocSet \\
\Temp(r, \iota) & \text{ if } \Heap(r, \iota) \in
\LocSet
\end{cases}
\]

We move on to $\RefSet$. We define the separating function $\SepRef$ as

\[
\SepRef\left(\Loc \RefTo{f, k} \Loc'\right) = (loc, f)
\]

We can use this as a separating function to ensure that uniqueness constraints
on field names in a well-formed configuration will be mirrored in the
construction of $\RefSet$. I.e. only configurations where each object or frame
has at most one field with a certain name will have a well-defined graph.

Given $\Loc_\LocSet$ as above we have

\[
\RefSet = \RefRS(RS) \cupdisj^\SepRef \RefH(\Hop) \cupdisj^\SepRef \RefH(\Hcl)
\cupdisj^\SepRef \RefH(\Hfr)
\]

\[
\begin{array}{lcl}
\RefRS((r, S, F)::RS) & = & \RefS(S) \cupdisj^\SepRef \RefF(\Root(r); F)
\cupdisj^\SepRef \RefRS(RS) \\
\RefRS(\NilRS) & = & \emptyset \vspace{1em} \\
\RefH(H_1 * H_2) & = & \RefH(H_1) \cupdisj^\SepRef \RefH(H_2) \\
\RefH((r, S)) & = & \RefS(S) \vspace{1em} \\
\RefS(S, \iota \mapsto (CL, F)) & = & \RefS(S) \cupdisj^\SepRef
\RefF(\Loc_\LocSet(\iota); F) \\
\RefS(\NilS) & = & \emptyset \vspace{1em} \\
\RefF(\Loc; F, f \mapsto (k, \iota)) & = & \RefF(F) \cupdisj^\SepRef \{ \Loc
\RefTo{f, k} \Loc_\LocSet(\iota)
\} \\
\RefF(\Loc; F, f \mapsto \Undef) & = & \RefF(F) \\
\RefF(\NilF) & = & \emptyset
\end{array}
\]

We want to have some kind of sanity check on a graph. Therefore we define
well-formedness of a graph $\Graph$, $\WFG(\Graph)$
as a predicate on a graph, as

\[
\begin{array}{lcl}
\WFG((\LocSet, \RefSet)) & \iff & \WFSrcDst(\LocSet, \RefSet) \AN
\WFRefs(\RefSet) \\
\WFSrcDst(\LocSet, \RefSet) & \iff & \begin{aligned}[t]
\forall & \Loc \RefTo{f, k} \Loc' \in
\RefSet. \\
&\Loc \in \LocSet \AN \Loc'
\in \LocSet
\end{aligned} \\
\WFRefs(\RefSet) & \iff & \begin{aligned}[t]
\forall & \REF_1 = (\Loc \RefTo{f, \_} \_) ~, \REF_2
= (\Loc \RefTo{f', \_} \_) \in \RefSet. \\
& \REF_1 = \REF_2 \OR f \neq f'
\end{aligned}
\end{array}
\]

For a well-formed graph $\Graph = (\LocSet, \RefSet)$ we can define the partial

\[
\begin{array}{lcl}
\REF_\RefSet(\Loc, f) & = & \begin{cases}
\Loc \RefTo{f, k} \Loc' & \text{ if } \Loc
\RefTo{f, k} \Loc'
\in \RefSet \\
\FUndef & \text{ otherwise}
\end{cases} \\

\end{array}
\]

Furthermore we define shorthands

\[
\begin{array}{lcl}
\Loc_\Graph(\iota) & = & \Loc_\LocSet(\iota) \\
\REF_\Graph(\Loc, f) & = & \REF_\RefSet(\Loc, f) \\
\REF_\Graph(\iota, f) & = & \REF_\Graph(\Loc_\Graph(\iota), f)
\end{array}
\]

§.§.§ Region Orders and Sets

We define $\rho$ to talk about ordering of regions.

\[
\begin{array}{rccl}
\rho & ::= & r \rhosep{x.f} \rho ~|~ \Nilrho & \text{Region ordering}
\end{array}
\]

If we do not care about $x.f$ we write a shorthand $r \rhosepe \rho$.

From a well formed region stack $\Gammas \vdash \RS$,  we can generate a $\rho$:

\[
\begin{array}{lcl}
\rho(\Gamma \rhosep{x.f} \Gammas, (r, S, F)::RS) & = & r \rhosep{x.f} \rho(RS) \\
\rho(\NilGammas, \NilRS) & = & \Nilrho
\end{array}
\]

We extend this definition to region configurations, $\rho(\Gammas, \RCfg)$, in the
obvious way.

We define ordering of region ids under $\rho$ as

$\rho \vdash r < r' \quad \rho \vdash r \leq r'$Region ordering

We define

\[
\begin{array}{lcl}
\Regions(H_1 * H_2) &=& \Regions(H_1) \cupdisj \Regions(H_2) \\
\Regions((r, S)) & = & \{ r \}
\end{array}
\]

\[
\begin{array}{lcl}
\Open(\RCfglong{RS; \Hop; \Hcl; \Hfr}) &= & \Regions(\Hop) \\
\Closed(\RCfglong{RS; \Hop; \Hcl; \Hfr}) &= & \Regions(\Hcl) \\
\Frozen(\RCfglong{RS; \Hop; \Hcl; \Hfr}) &= & \Regions(\Hfr)
\end{array}
\]

We define intersection of $\rho$ and a set of region ids in the obvious way. The
relation $\vdash \rho, \Cl, \Fr$ is simply disjointness of $\rho$ and the region id
sets $\Cl, \Fr$:

\[
\vdash \rho, \Cl, \Fr  \iff \rho \cap \Cl = \rho \cap \Fr = \Cl \cap \Fr = \emptyset
\]

§.§.§ Capability Semantics

The predicate () is defined using three auxilliary
predicates as follows.

\[
\begin{aligned}
\CapOK(\Gammas, \RCfg) \iff & \VarUnique(G(\RCfg)) \AN \\
&\RegionOrder(\rho(\Gammas, \RCfg), \Closed(\RCfg), \Frozen(\RCfg), G(\RCfg)) \AN \\
&\LocationOK(G(\RCfg)) \\
&\DeepFreeze(\Frozen(\RCfg), G(\RCfg))
\end{aligned}
\]

The three auxilliary predicates are defined using the object graph $G(\RCfg)$ as

\[
\RegionOrder(\rho, \Cl, \Fr, \Graph) \iff \forall \REF \in \Graph.
\regionorder1(\rho, \Cl, \Fr, \REF)
\]

\[
\begin{aligned}
\regionorder1(\rho, \Cl, \Fr,
&(\Loc[r] \RefTo{f, k} \Loc'[r']))\\
&\iff \\
& (k = \Mut &\implies& r = r') &\AN \\
& (k = \Tmp &\implies& r = r') &\AN \\
& (k = \Var &\implies& r = r') &\AN \\
& (k = \Paused &\implies& \rho \vdash r' < r) &\AN \\
& (k = \Iso &\implies& r \neq r' \AN (r' \in \Cl \OR ((\rho \vdash r < r') \OR r' \in
\Fr \AN r \in \Fr ))) &\AN \\
& (k = \Imm &\implies& r' \in \Fr)) &
\end{aligned}
\end{aligned}
\]

\[
\locationok(\Graph) \iff \forall \REF \in \Graph. \locationok1(\REF)
\]

\[
\begin{aligned}
\locationok1(&\Loc \RefTo{f, k} \Loc') \\
&\iff \\
& (k = \Mut &\implies& \Loc' = \Heap(r', \iota')) &\AN \\
& (k = \Tmp &\implies& ((\Loc = \Root(r) \OR \Loc = \Temp(r, \iota))
\AN \Loc' = \Temp(r', \iota'))) &\AN \\
& (k = \Var &\implies& (\Loc = \Root(r) \AN \Loc' = \Temp(r', \iota')))
& \AN \\
& (k = \Paused &\implies& ((\Loc = \Root(r) \OR \Loc =
\Temp(r, \iota)) \AN \Loc' \neq \Root(r')))
&\AN \\
& (k = \Iso &\implies& \Loc' = \Heap(r', \iota')) &\AN \\
& (k = \Imm &\implies& \Loc' = \Heap(r', \iota')) &
\end{aligned}
\end{aligned}
\]

\[
\deepfreeze(\Fr, \Graph) \iff \forall \REF \in \Graph. \deepfreeze1(\Fr, \REF)
\]

\[
\deepfreeze1(\Fr, \Loc[r] \refto{\_, \_} \loc'[r']) \iff r \in \Fr \implies r'
\in \Fr
\]

\[
\VarUnique(\Graph) \iff \begin{aligned}[t]
\forall &\REF_1, Ref_2\in \Graph. \\
&\VPU(\REF_1, \REF_2)
\end{aligned}
\]

\[
\VPU(\REF_1, \REF_2) \iff
\begin{aligned}[t]
&\REF_1 = \_ \RefTo{\_, \Var} \Loc \AN &\\
&\REF_2 = \_ \RefTo{\_, \_} \Loc &\implies \REF_1 = \REF_2
\end{aligned}
\]

§.§.§ Topology Invariant

Finally we define $\TopOK(\RCfg)$. We again use the graph representation to
formulate it.

\[
\begin{aligned}
\TopOK(&\Gammas, \RCfg)\iff  \\
&\topokgraph(\rho(\Gammas, \RCfg), \Frozen(\RCfg), G(\RCfg)) \AN \\
&\entrypointsok(\rho(\Gammas, \RCfg), G(\RCfg))
\end{aligned}
\]

\[
\begin{aligned}
\topokgraph(\rho, \Fr, \Graph) &\iff \\
\forall &\REF_1,\REF_2 \in \Graph. \\
&\ToppOK(\rho, \Fr, \REF_1, \REF_2)
\end{aligned}
\end{aligned}
\]

\[
\begin{aligned}
\ToppOK(&\rho, \Fr, \REF_1, \REF_2) \iff \\
\REF_1 = &~\Loc_1[r_1] \RefTo{\_, \_} \Loc_1'[r_1'] \AN \\
\REF_2 = &~\Loc_2[r_2] \RefTo{\_, \_} \Loc_2'[r_2'] \\
\implies & \begin{aligned}[t]
&\REF_1 = \REF_2 &\OR \\
&r_1' \neq r_2' &\OR \\
&r_1' \in \Fr \OR r_2' \in \Fr &\OR \\
&\rho \vdash r_1' \leq r_1 \OR \rho \vdash r_2' \leq r_2 &
\end{aligned}
\end{aligned}
\end{aligned}
\]

Note that the topology invariant in the paper also relies on the source of
backward pointing references being $\temp$ locations. This is not included in
this version, but still holds because of $\capok$.

\[
\begin{aligned}
&\entrypointsok(r' \rhosep{x.f} r :: \rho, \Graph) \iff \\
&\ruut(r) \refto{x, k_x} \loc_x[r^*] \in \Graph \AN \\
&\loc_x[r^*] \refto{f, k_f} \Heap(r', \_) \in \Graph \AN \\
&\entrypointsok(r :: \rho, \Graph)
\end{aligned}
\]

\[
\begin{aligned}
&\entrypointsok(r :: \Nilrho, \Graph) \iff \text{true}
\end{aligned}
\]

§ EFFECTS

\[
\begin{array}{rcl}
\Use & ::= & x ~|~ \kw{drop}~x\\
\Eff & ::= & \load{x, y.f}\\
& ~|~ & \swap{x, y.f, \Use}\\
& ~|~ & \bind{\many{x = \Use}}\\
& ~|~ & \halloc{x, k, \#C, \many{\Use}}\\
& ~|~ & \salloc{x, k, \CLTag, \many{\Use}}\\
& ~|~ & \enter{w, k, y.f, CL, \many{x = \Use}}\\
& ~|~ & \badenter{x.f}\\
& ~|~ & \exit{x, \Use, y.f, w.g}\\
& ~|~ & \cast{x, \Use, k~C}\\
& ~|~ & \nocast{x, \Use, k~C}\\
& ~|~ & \bind{\many{x = \Use}}\\
& ~|~ & \epsilon\\
\end{array}
\]

§.§ Well-Formed Effects

We use the following helper predicate for a capability pointing
into an open region:

\[
\mathbf{open}(k) \iff k \in \{\Mut, \Tmp, \Var, \Paused\}
\]

Effects are typed under a stack of contexts $\Gammas$, defined in
Section <ref>.

$\Gammas \vdash \Eff \dashv \Gammas$Well-formed Effects

§ COMMAND SEMANTICS

\[
\begin{array}{rcll}
e & ::= & \Use ~|~ \kw{let}~x = b~\kw{in}~e
~|~ \kw{if}~\kw{typetest}(\Use, t) \SB y => e \FB \SB y => e \FB & \text{Expressions} \\
\Use & ::= & x ~|~ \kw{drop}~x & \text{Variable usage}\\
b & ::= & \c{*}\lval
~|~ \lval~\c{:=}~\Use
~|~ \fnc(\many{use})
~|~ \kw{var}~\Use
~|~ \kw{new}~k~C(\many{use})& \text{Bound expressions}\\
& ~|~ & \kw{enter}~\lval~[\many{y=\Use}] \SB z~\c{=>}~e \FB
~|~ \kw{freeze}~\Use
~|~ \kw{merge}~\Use
~|~ e\\
\lval & ::= & x ~|~ x.f & \text{L-values}\\
de & ::= & e ~|~ \kw{let}~x = db~\kw{in}~e ~|~ \textbf{Failure} & \text{Dynamic expressions}\\
db & ::= & b ~|~ de ~|~ \kw{entered}~x.f~y.f' \SB de \FB & \text{Dynamic bound expressions}\\
de[\bullet] & ::= & \bullet ~|~ \kw{let}~x = \bullet~\kw{in}~e
~|~ \kw{let}~x = \kw{entered}~y.f~w.f' \SB \bullet \FB~\kw{in}~e & \text{Execution context}\\
\CCfg & ::= & \SB de \FB & \text{Dynamic configuration}
\end{array}
\]

The syntax of the command language is in A-normal form (ANF).

An expression is a  of a name (a potentially destructive
read), the binding of an expression $b$ to a name, or a dynamic
type test, where the value is rebound in the chosen branch in
order to track the type.

Note that we model mutable variables as objects, created with the
syntax $\kw{var}~\Use$. A bound expression is a field access, a
field update, a function call, the creation of a variable or an
object, an enter block, or a freeze or merge.

An enter block enters through a variable $x$ or a field $x.f$ and
explicitly captures variables $\many{\Use}$, potentially
destructively, as $\many{y}$. The bridge object is bound to $z$
and the body $e$ of the block is executed. The capture list is for
convenience only, and could be inferred based on variable usage in

During execution, an enter block reduces to a entered
block, which stores the field entered through and the field in
which the new bridge object can be found when exiting the region.

The only difference between dynamic expressions $de$ and static
expressions $e$ is that dynamic expressions can contain
entered blocks in the currently bound expression being
evaluated, or denote failure.

We use an execution context $de[\bullet]$ to find the inner-most
dynamic expression to evaluate.

A dynamic configuration is just a dynamic expression.

We assume the existence of a table of well-formed functions such
that if
$\mathbf{fnctype}(\fnc) = (t_1, ..., t_n) \rightarrow t$,
$\mathbf{fnclookup}(\fnc) = (x_1, ..., x_n) \rightarrow e$
and $x_1 : t_1, ..., x_n : t_n \vdash e : t \dashv \Gamma'$ for
some $\Gamma'$. We further assume that function lookup renames all
let-bound variables to globally fresh names to avoid accidental

§.§ Dynamic Semantics

Because the command language is in ANF, many rules differ only in
which effect they emit. In order to avoid duplicating rules, for
expressions with the shape $\kw{let}~x~=~e_1~\kw{in}~e_2$ we define a
helper function to calculate the effect of $b$:

\[
\begin{array}{lcl}
\mathbf{effect}(x, \c{*y.f})                     & = & \load{x, y.f}\\
\mathbf{effect}(x, \c{*y})                       & = & \load{x, y.val}\\
\mathbf{effect}(x, \c{y.f := }\Use)              & = & \swap{x, y.f, \Use}\\
\mathbf{effect}(x, \c{y   := }\Use)              & = & \swap{x, y.val, \Use}\\
\mathbf{effect}(x, \kw{new}~\Mut~C(\many{\Use})) & = & \halloc{x, \Mut, \#C, \many{\Use}}\\
\mathbf{effect}(x, \kw{new}~\Iso~C(\many{\Use})) & = & \halloc{x, \Iso, \#C, \many{\Use}}\\
\mathbf{effect}(x, \kw{new}~\Tmp~C(\many{\Use})) & = & \salloc{x, \Tmp, \#C, \many{\Use}}\\
\mathbf{effect}(x, \kw{var}~\Use)                & = & \salloc{x, \Var, \#\Cell, \Use}\\
\mathbf{effect}(x, \kw{freeze}~\Use)             & = & \freeze{x, \Use}\\
\mathbf{effect}(x, \kw{merge}~\Use)              & = & \merge{x, \Use}\\
\mathbf{effect}(x, \Use)                         & = & \bind{x = \Use}\\
\end{array}
\]

$de \ComStep{\Eff} de$Command semantics

§.§ Static Semantics

\[
\begin{array}{rcll}
t & ::= & k~C ~|~ k~\c{Cell}[t] ~|~ t\c{|}t & \text{Types}\\
\Gamma & ::= & \Gamma, x : t ~|~ \Gamma, x : \Undef ~|~ \varepsilon & \text{Typing context}\\
\Gammas & ::= & \Gammas\underset{x.f}{::}\Gamma ~|~ \varepsilon & \text{Dynamic typing context}
\end{array}
\]

A type is a class $C$ with a capability $k$, a Çȩļļ with a
given type ( ML-style ref cells), or a union $t_1\c{|}t_2$ of
two types.

A typing context maps variables to types, or remembers that they
have been consumed.

When typing a dynamic expression, we use a stack of typing
contexts mirroring the stack of open regions. Each $::$ between
two contexts in the stack is marked with $x.f$ denoting the field
through which we entered the next region. Whenever we don't care
about this field, we omit it for readability.

When dealing with union types, we sometimes need to merge two
different contexts with the same domain but (possibly) different
codomains. This is done with the following function:

\[
(\Gamma_1\c{|}\Gamma_2) =
\left\{
\begin{array}{llcl}
(\Gamma_1'\c{|}\Gamma_2'), x : t_1\c{|}t_2 &
\text{if } \Gamma_1 = \Gamma_1', x : t_1 & \text{ and }& \Gamma_2 = \Gamma_2', x : t_2\\
(\Gamma_1'\c{|}\Gamma_2'), x : \Undef &
\text{if } \Gamma_1 = \Gamma_1', x : \Undef & \text{ and }& \Gamma_2 = \Gamma_2', x : t_2\\
(\Gamma_1'\c{|}\Gamma_2'), x : \Undef &
\text{if } \Gamma_1 = \Gamma_1', x : t_1 & \text{ and }& \Gamma_2 = \Gamma_2', x : \Undef\\
(\Gamma_1'\c{|}\Gamma_2'), x : \Undef &
\text{if } \Gamma_1 = \Gamma_1', x : \Undef & \text{ and }& \Gamma_2 = \Gamma_2', x : \Undef\\
\varepsilon & \text{if } \Gamma_1 = \varepsilon & \text{ and } & \Gamma_2 = \varepsilon
\end{array}
\right.
\]

\[
(\many{\Gamma}_1\c{|}\many{\Gamma}_2) =
\left\{
\begin{array}{llcl}
(\Gamma_1'\c{|}\Gamma_2') :: (\many{\Gamma}_1'\c{|}\many{\Gamma}_2') &
\text{if } \many{\Gamma}_1 = \Gamma_1' :: \many{\Gamma_1}' & \text{ and }& \many{\Gamma}_2 = \Gamma_2' :: \many{\Gamma}_2'\\
\varepsilon & \text{if } \many{\Gamma}_1 = \varepsilon & \text{ and } & \many{\Gamma}_2 = \varepsilon
\end{array}
\right.
\]

We sometimes need to compare what variables are defined for a certain $\Gamma$
or $\Gammas$. We use define $\defined$ as follows

\[
\begin{array}{lcl}
\defined(\Gamma, x: t) & = & \defined(\Gamma) \cup \{ x \} \\
\defined(\Gamma, x : \Undef) & = & \defined(\Gamma) \\
\defined(\NilGamma) & = & \emptyset \\
\end{array}
\]

To compare $\Gammas_1$ and $\Gammas_2$, we check pairwise set inclusion of
defined sets:

\[
\begin{aligned}
\Gamma :: \Gammas &\gammadefincl \Gamma' :: \Gammas' \iff \\
&\defined(\Gamma) \subseteq \defined(\Gamma') \AN \\
&\Gammas \gammadefincl \Gammas'
\end{aligned}
\]

We further use the following helper functions and predicates
(viewpoint adaptation is in Table <ref>):

We use $\mathit{make\_iso}$ and $\mathit{make\_mut}$ to change all
occurrences of  to  and vice versa for a type (all
other capabilities remain unchanged).

\[
\begin{array}{rcl}
\mathit{make\_iso}(k~CL) & = &
\begin{cases}
\Iso~CL & \text{if } k = \Mut\\
k~CL    & \text{otherwise}
\end{cases}\\
\mathit{make\_iso}(t_1~|~t_2) & = & \mathit{make\_iso}(t_1) ~|~ \mathit{make\_iso}(t_2)
\end{array}
\]

\[
\begin{array}{rcl}
\mathit{make\_mut}(k~CL) & = &
\begin{cases}
\Mut~CL & \text{if } k = \Iso\\
k~CL    & \text{otherwise}
\end{cases}\\
\mathit{make\_mut}(t_1~|~t_2) & = & \mathit{make\_mut}(t_1) ~|~ \mathit{make\_mut}(t_2)
\end{array}
\]

We use the predicate $\Kap(\many{k}, t)$ to check if all
capabilities in a type are in $\many{k}$. We omit brackets for
singleton sets (the first case below), and use the complement
notation $\Kap(\{k\}^c, t)$ for checking that capability $k$ does
not occur anywhere in $t$.

\[
\begin{array}{rcl}
\Kap(k, t) & \equiv & \Kap(\{k\}, t)\\
\Kap(\many{k}, k' CL)     & \iff & k' \in \many{k}\\
\Kap(\many{k}, t_1~|~t_2) & \iff & \Kap(\many{k}, t_1) \land \Kap(\many{k}, t_2)
\end{array}
\]

We use $\mathbf{classtype}(t)$ to check if a type is definitely a
class type:

\[
\mathbf{classtype}(t) \iff \forall k~CL \in t.~ \exists C. CL = C
\]

Viewpoint adaptation.

If the capabilities of x̧ and f̧ are $\alpha$ and $\beta$,
then the capability of x̧.̧f̧ is $\VPA{\alpha}{\beta} = \gamma$,
which we read as “$\alpha$ sees $\beta$ as $\gamma$.”

Note that this table is slightly different from the one in the
paper since we only use it for non-destructive reads.

Capability     5cCapability on f̧

on x̧

$\FUndef$              $\FUndef{}$     $\FUndef$

$\FUndef$      $\FUndef$      $\FUndef$     $\FUndef{}$       $\FUndef$

\[
\begin{array}{rcl}
\VPA{k}{(k'~CL)} & = &
\begin{cases}
k''~CL & \text{if } \VPA{k}{k'} = k''\\
\FUndef{} & \text{otherwise}
\end{cases}\\
\VPA{k}{(t_1~|~t_2)} & = &
\begin{cases}
t_1'~|~t_2' & \text{if } \VPA{k}{t_1} = t_1' \text{ and } \VPA{k}{t_2} = t_2'\\
\FUndef{} & \text{otherwise}
\end{cases}
\end{array}
\]

We extend viewpoint adaptation to $k \sees \Gamma$ and $k \sees F$ by mapping
over the elements of $\Gamma$ and $F$ respectively.

$\Gamma \vdash e \dashv \Gamma\quad\Gamma \vdash b \dashv \Gamma$Command Language Typing

$\Gammas \vdash de \dashv \Gamma\quad\Gammas \vdash db \dashv \Gamma$Command Language Dynamic Typing

$\vdash t$Well-formedness of types

$t <: t$Subtyping

$\Gammas \vdash \SB de \FB$Well-formedness of dynamic configuration

$\vdash \Gamma$Well-formedness of typing contexts

$\vdash \Gammas$Well-formedness of dynamic typing contexts

§ PROOFS

§.§ Theorem: Progress of Command Language

\[
\begin{array}{l}
\many{\Gamma} \vdash \SB de \FB \implies\\
\quad de = \Use \OR de = \mathbf{Failure} \OR
\exists \Eff, de'.~ de \ComStep{\Eff} de'\\
\end{array}
\]

§.§.§ Proof Sketch

The proof of progress is very simple since there are very few
rules that have premises that can be false: function calls must
refer to existing functions and objects can only be constructed
with capability ,  or . All other rules are
always applicable when the expression has the right shape.

§.§.§ Proof of Theorem

We begin by inversion of $\many{\Gamma} \vdash \SB de \FB$ and get
$\many{\Gamma} \vdash de : t \dashv \Gamma'$. We proceed by
induction over the dynamic typing judgment.

cmd-dyn-ty-failure, $de = \mathbf{Failure}$

Proof holds trivially

cmd-dyn-ty-expr, $de = e$

* $\Gammas = \Gamma$

We proceed by induction over the static typing judgment
$\Gamma \vdash de : t \dashv \Gamma'$:

cmd-ty-use-keep, $de = x$

Proof holds trivially.

cmd-ty-use-drop, $de = \kw{drop}~x$

Proof holds trivially.

cmd-ty-typetest, $de = \kw{if}~\kw{typetest}(\Use, t_1)\{y \c{=>} e_1\}\{y \c{=>} e_2\}$

We pick any $k~CL$.

* If $k~CL<:t$, the configuration steps by

* If $k~CL\not<:t$, the
configuration steps by cmd-if-typetest-false.

cmd-ty-let[pf]case:let, $de = \kw{let}~x=b~\kw{in}~e$

By cmd-ty-let we have

* $\Gamma \vdash b : t' \dashv \Gamma''$ ass:wft

We proceed by cases on the shape of $b$.

* If $b = \fnc(\Use_1, ..., \Use_n)$, then by the
inversion lemma with ass:wft we get
$\mathbf{fnctype}(\fnc) = (t_1, ..., t_n) \rightarrow t''$,
and thus by assumptions about the function table
$\mathbf{fnclookup}(\fnc) = (x_1, ..., x_n) \rightarrow
e_{body}$. The configuration steps by cmd-call.

* If $b = \kw{new}~k~C(\Use_1, ..., \Use_n)$, then by the
inversion lemma with ass:wft we get
$k \in \{\Mut, \Tmp, \Iso\}$. The configuration steps by

* If $b = \kw{enter}...$, the configuration steps by
cmd-enter-field, cmd-enter-var or

* For all remaining cases, the configuration steps by

cmd-dyn-ty-let, $de = \kw{let}~x=db~\kw{in}~e$

* $\Gammas = \many{\Gamma}' :: \Gamma$

We proceed by cases on whether $db$ is in the syntactic category
of $b$ or not.

* If it is, the proof collapses to case [pf]case:let,
since every non-dynamic typing derivation needs to use
cmd-dyn-ty-expr, which requires an empty $\many{\Gamma}$.

* If it is not, we have either $db = de'$ or
$db = \kw{entered}~y.f~w.\c{val} \SB de' \FB$. We proceed by

$db = de'$

* By cmd-ty-let we have
$\Gammas \vdash de' : t' \dashv \Gamma''$.

* By the induction hypothesis we have $de' = \Use$, or
$de' = \mathbf{Failure}$ or
$\exists \Eff, de''.~ de' \ComStep{\Eff} de''$. We
proceed by cases.

* If $de' = \Use$, configuration steps by

* If $de' = \mathbf{Failure}$, configuration steps by

* If $de'\ComStep{\Eff}de''$, configuration steps
by cmd-ec.

$db = \kw{entered}~x.f~y.\c{val} \SB de' \FB$

* $\Gammas = \many{\Gamma}'' :: \Gamma' :: \Gamma$

* By cmd-ty-let we have $\many{\Gamma} \vdash \kw{entered}~x.f~y.\c{val} \SB de' \FB : t' \dashv \Gamma''$.

* By the inversion lemma, we have $\many{\Gamma}'' :: \Gamma' \vdash de' : t' \dashv \Gamma_1'$

* By the induction hypothesis we have $de' = \Use$, or
$de' = \mathbf{Failure}$ or
$\exists \Eff, de''.~ de' \ComStep{\Eff} de''$. We
proceed by cases.

* If $de' = \Use$, configuration steps by cmd-ec
with cmd-exit.

* If $de' = \mathbf{Failure}$, configuration steps by
cmd-ec with cmd-ec-fail.

* If $de'\ComStep{\Eff}de''$, configuration steps
by cmd-ec with cmd-ec

§.§ Theorem: Preservation of Command Language

\[
\begin{array}{l}
\many{\Gamma} \vdash \SB de \FB \AN \SB de \FB \ComStep{\Eff} \SB de' \FB \implies\\
\quad \exists \many{\Gamma}'.~ \many{\Gamma}'\vdash \SB de' \FB \AN
\many{\Gamma} \vdash \Eff \dashv \many{\Gamma}'
\end{array}
\]

§.§.§ Proof Sketch

The proof of preservation ensures that stepping preserves
well-formedness and that it produces a well-formed effect. The
former is straightforward since the only changes we make to the
configuration is alpha conversion of subexpressions, introduction
of (well-formed) function bodies, and introduction of entered
blocks from (well-formed) enter blocks.

The latter comes from lifting the rules for expression typing to
the rules for well-formed effects, via the inversion lemma.

§.§.§ Proof of Theorem

We state an alpha conversion property, the observation that we can
change the name of a variable without affecting well-formedness of
an expression: Prove as lemma?

\[
\begin{array}{l}
\Gamma[x : t_1] \vdash e : t \dashv \Gamma'[x : t_2] \AN y~\mathit{fresh} \implies\\
\quad \Gamma[y : t_1] \vdash e[x \mapsto y] : t \dashv \Gamma'[y : t_2]\\\\
\Gamma[x : t_1] \vdash e : t \dashv \Gamma'[x : \Undef] \AN y~\mathit{fresh} \implies\\
\quad \Gamma[y : t_1] \vdash e[x \mapsto y] : t \dashv \Gamma'[y : \Undef]\\
\end{array}
\]

We also note that the type system supports weakening of the typing
context as long as the bound variables in the expression are not
in the domain of the added context.

\[
\begin{array}{l}
\Gamma_1 \vdash e : t \dashv \Gamma_2 \AN \vdash \Gamma, \Gamma_1 \AN \mathbf{BV}(e) \cap \mathbf{dom}(\Gamma) = \emptyset\implies\\
\quad \Gamma, \Gamma_1 \vdash e : t \dashv \Gamma, \Gamma_2
\end{array}
\]

We start the proof of preservation by inversion of well-formedness
of the configuration and get
$\many{\Gamma} \vdash de : t \dashv \Gamma'$.

We proceed by induction over the dynamic typing judgment.

cmd-dyn-ty-failure, $de = \mathbf{Failure}$

Proof holds vacuously as the configuration does not step.

cmd-dyn-ty-expr, $de = e$

* $\many{\Gamma} = \Gamma$

We proceed by induction over the static typing judgment
$\Gamma \vdash de : t \dashv \Gamma'$:

cmd-ty-use-keep, $de = x$

Proof holds vacuously as the configuration does not step.

cmd-ty-use-drop, $de = \kw{drop}~x$

Proof holds vacuously as the configuration does not step.

cmd-ty-typetest, $de = \kw{if}~\kw{typetest}(\Use, t')\{y \c{=>} e_1\}\{y \c{=>} e_2\}$

By cmd-ty-typetest we have

* $\Gamma \vdash \Use : t'' \dashv \Gamma''$ ass:use

* $\Gamma'', y : t' \vdash e_1 : t_1 \dashv \Gamma_1, y : \_$ ass:then

* $\Gamma'', y : t''  \vdash e_2 : t_2 \dashv \Gamma_2, y : \_$ ass:else

There are two rules that step the configuration.

* cmd-if-typetest-true [pf]case:true

* $\Eff = \cast{y', \Use, k~CL}$

* $k~CL <: t'$ ass:sub

* $y'~\mathit{fresh}$

* By the alpha conversion property with ass:then,
we have $\Gamma'', y' : t' \vdash e_1[y \mapsto y'] : t_1 \dashv \Gamma_1, y' : \_$.

* The resulting configuration is well-formed by cmd-dyn-ty-expr.

* The effect is well-formed under $\Gamma$ By wf-eff-cast with ass:use and ass:sub.

* cmd-if-typetest-false

Similar to the above.

cmd-ty-let[pf]case:let, $de = \kw{let}~x=b~\kw{in}~e$

By cmd-ty-let we have

* $\Gamma \vdash b : t' \dashv \Gamma''$ ass:wfb

* $\Gamma'', x : t' \vdash e : t \dashv \Gamma', x : \_$ ass:wfe

There are seven rules that step the configuration.

* cmd-let-eff

* $x'~\mathit{fresh}$

* $\mathbf{effect}(x', b) = \Eff$

* By the alpha conversion property with ass:wfe,
we have
$\Gamma'', x' : t' \vdash e[x \mapsto x'] : t \dashv
\Gamma'', x' : \_$, and the resulting configuration is
well-formed by cmd-dyn-ty-expr.

* Depending on the shape of $b$ there are eleven cases
of $\mathbf{effect}(x', b) = \Eff$:

* $\mathbf{effect}(x', \c{*y.f}) = \load{x, y.f}$

The effect is well-formed by wf-eff-load, by the
inversion lemma with ass:wfb, followed by
induction over the shape of $t'$.

* $\mathbf{effect}(x', \c{*y}) = \load{x, y.val}$

Similar to the previous case.

* $\mathbf{effect}(x', \c{y.f \c{:=} }\Use) = \swap{x, y.f, \Use}$

The effect is well-formed by wf-eff-swap-class, by
the inversion lemma with ass:wfb, followed by
induction over the shape of $t'$.

* $\mathbf{effect}(x', \c{y \c{:=} }\Use) = \swap{x, y.val, \Use}$

Similar to the previous case, but using wf-eff-swap-var.

* $\mathbf{effect}(x', \kw{new}~\Mut~C(\many{\Use})) = \halloc{x, \Mut{}, \#C, \many{\Use}}$

The effect is well-formed by wf-eff-halloc-mut, by
the inversion lemma with ass:wfb. For the typing
of each $\Use$, we use cmd-ty-sub since the
inversion lemma gives us that the arguments are subtypes
of the field types.

* $\mathbf{effect}(x', \kw{new}~\Iso~C(\many{\Use})) = \halloc{x, \Iso{}, \#C, \many{\Use}}$

Similar to the previous case, but using
wf-eff-halloc-iso and without the need for
cmd-ty-sub (note that all the arguments are
or ).

* $\mathbf{effect}(x', \kw{new}~\Tmp~C(\many{\Use})) = \salloc{x, \Tmp{}, \#C, \many{\Use}}$

Similar to the case for $\Mut{}$ allocation, but using

* $\mathbf{effect}(x', \kw{var}~\Use) = \salloc{x, \Var{}, \#\Cell, \Use}$

Similar to the previous case.

* $\mathbf{effect}(x', \kw{freeze}~\Use) = \freeze{x, \Use}$

The effect is well-formed by wf-eff-freeze, by the
inversion lemma with ass:wfb.

* $\mathbf{effect}(x', \kw{merge}~\Use) = \merge{x, \Use}$

The effect is well-formed by wf-eff-merge, by the
inversion lemma with ass:wfb.

* $\mathbf{effect}(x', \Use) = \bind{x = \Use}$

The effect is well-formed by wf-eff-bind with ass:wfb.

* cmd-enter-field, $b = \kw{enter}~y.f~[\many{z=\Use}] \SB w~\c{=>}~e' \FB$

* $w'~\mathit{fresh}$

* $z'_1,...,z'_n~\mathit{fresh}$

* $\Eff = \enter{w', \Tmp{}, y.f, z'_1 = \Use_1, ..., z'_n = \Use_n}$

* $de' = \kw{let}~x = \kw{entered}~y.f~w'.\c{val} \SB e'[w\mapsto w', z_1 \mapsto z'_1, ..., z_n \mapsto z'_1]\FB$

By the inversion lemma with ass:wfb we get

* $\forall i \in [1,n]. \Gamma_i \vdash \Use_i : t_i \dashv \Gamma_{i+1}$ ass:uses

* $\Gamma_{n+1}(y) = t_y$ ass:yty

* $\Kap(\{\Mut, \Tmp, \Var, \Paused\}, t_y)$ ass:open

* $\mathbf{fresult}(t_y, f)) = t_f$ ass:ftype

* $\Kap(\Iso, t_f)$ ass:iso

* $\Gamma' = y_1 : t'_1, ..., y_n : t'_n \text{ where } t'_i =
\begin{cases}
t_i & \text{if } \Kap(\Iso, t_i)\\
\VPA{\Paused}{t_i} & \text{otherwise}
\end{cases}$ ass:gamma

* $t_f' = \mathit{make\_mut}(t_f)$

* $\Kap(\{\Iso, \Imm\}, t')$ ass:ret

* $ t' <: t$ ass:sub

* $\Gamma', z : \Tmp~\Cell[t_f'] \vdash e : t' \dashv \Gamma', z : \Tmp~\Cell[t_f']$ ass:inner

* $\kw{entered}~y.f~w'.\c{val} \SB e'[w\mapsto w', z_1 \mapsto z'_1, ..., z_n \mapsto z'_1]$

is well-formed by induction over the shape of $t_y$. In
the inductive case we use cmd-dyn-ty-split. In the
base case we use the alpha conversion property and
cmd-dyn-ty-entered with ass:open,
ass:ftype, ass:iso, ass:inner and

* $de'$ is well-formed by cmd-dyn-ty-sub with
ass:sub and cmd-dyn-ty-let with the above and

* The effect is well-formed by induction over the shape
of $t_y$. In the inductive case we use wf-eff-split.
In the base case we use wf-eff-enter with
ass:uses, ass:yty , ass:open
and ass:iso, with resulting dynamic context
$(\Gamma', z : \Tmp~\Cell[t_f']) :: \Gamma_{n+1}$.

* cmd-enter-var, $b = \kw{enter}~y~[\many{z=\Use}] \SB w~\c{=>}~e' \FB$

Similar to the previous case.

* cmd-enter-field-fail

* $\Eff = \badenter{y.f}$

* $de' = \mathbf{Failure}$

By the inversion lemma with ass:wfb we get

* $\forall i \in [1,n]. \Gamma_i \vdash \Use_i : t_i \dashv \Gamma_{i+1}$

* $\Gamma_{n+1}(y) = t_y$ fail:ass:yty

* $\Kap(\{\Mut, \Tmp, \Var, \Paused\}, t_y)$ fail:ass:open

* $\mathbf{fresult}(t_y, f)) = t_f$ fail:ass:ftype

* $\Kap(\Iso, t_f)$ fail:ass:iso

* The resulting configuration $\SB \mathbf{Failure} \FB$
is always well-formed.

* The effect is well-formed by induction over the shape
of $t_y$. In the inductive case we use wf-eff-split.
In the base case we use wf-eff-badenter with
fail:ass:yty, fail:ass:open, fail:ass:ftype and

* cmd-enter-var-fail

Similar to the previous case.

* cmd-call, $b = \fnc(\Use_1, ..., \Use_n)$

* $\mathbf{fnclookup}(\fnc) = (x_1, ..., x_n) \rightarrow

* $x'_1, ..., x'_n~\mathit{fresh}$

* $\many{x} = x_1, ..., x_n$

* $\many{x}' = x'_1, ..., x'_n$

* $\Eff = \bind{x'_1 = \Use_1, ..., x'_n = \Use_n}$

By the inversion lemma with ass:wfb we get

* $t'' <: t'$ call:ass:sub

* $\mathbf{fnctype}(\fnc) = (t_1, ..., t_n) \rightarrow t''$

* $\Gamma = \Gamma_1$

* $\forall i \in [1,n]. \Gamma_i \vdash \Use_i : t_i \dashv \Gamma_{i+1}$ ass:wfargs

* $\Gamma'' = \Gamma_{n+1}$

* By assumptions about the function table we have
$x_1 : t_1, ..., x_n : n_n \vdash e : t'' \dashv \Gamma_{res}$.

* By the alpha conversion property we have
$x'_1 : t_1, ..., x'_n : n_n \vdash e[\many{x} \mapsto \many{x'}] : t'' \dashv \Gamma_{res}$.

* By the weakening property (we assume function lookup
dynamically renames all variables to avoid clashes) we
$\Gamma'', x'_1 : t_1, ..., x'_n : n_n \vdash e[\many{x}
\mapsto \many{x'}] : t'' \dashv \Gamma'', \Gamma_{res}$,
and the resulting configuration is well-formed by
cmd-dyn-ty-expr, with cmd-ty-sub with
call:ass:sub and cmd-ty-let.

* The effect is well-formed by wf-eff-bind with ass:wfargs.

* cmd-ec

Preservation holds by cmd-dyn-ty-let with the induction
hypothesis and ass:wfe.

cmd-dyn-ty-let, $de = \kw{let}~x=db~\kw{in}~e$

* $\Gammas = \many{\Gamma}' :: \Gamma$

* $\many{\Gamma}' :: \Gamma \vdash db : t' \dashv \Gamma''$ [pf]ass:wfb

* $\Gamma'', x : t' \vdash e : t \dashv \Gamma', x : \_$ [pf]ass:wfe

We proceed by cases on whether $db$ is in the syntactic category
of $b$ or not.

* If it is, the proof collapses to case [pf]case:let,
since every non-dynamic typing derivation needs to use
cmd-dyn-ty-expr, which requires a singleton $\many{\Gamma}$.

* If it is not, we have either $db = de''$, where $de''$ is
not in $b$, or
$db = \kw{entered}~y.f~w.\c{val} \SB de'' \FB$. We proceed by

$db = de''$

Since $de''$ is not in $b$, there are only two dynamic rules
that apply:

* cmd-ec

Preservation holds by cmd-dyn-ty-let with the
induction hypothesis and [pf]ass:wfe.

* cmd-ec-fail

Preservation holds since the resulting expression
$\SB \mathbf{Failure} \FB$ and the empty effect are
trivially well-formed.

$db = \kw{entered}~y.f~z.\c{val} \SB de'' \FB$

By the inversion lemma with [pf]ass:wfb we get

* $\Gamma = \Gamma_0[y : t_y]$

* $\many{\Gamma} = \many{\Gamma}''::\Gamma_1\underset{y.f}{::}\Gamma$

* $\many{\Gamma}' \vdash de'' : t' \dashv \Gamma_1'$ ass:inner

* $\Kap(\{\Mut, \Tmp, \Var, \Paused\}, t_y)$

* $\mathbf{fresult}(t_y, f) = t_f$

* $\Kap(\Iso{}, t)$ ass:iso

* $\Kap(\{\Iso{}, \Imm{}\}, t')$ ass:isoimm

* $t' <: t$

* $\Gamma_1'(z) = t_z$

* $\mathbf{fresult}(t_z, \c{val}) = t''$

* $\Kap(\Mut{}, t'')$ ass:mut

* $\Kap(\{\Tmp{}, \Var{}\}, t_z)$ass:tmpvar

* $\Gamma' = \Gamma_0[y : t_y']$

* $t_y' =
\begin{cases}
\mathit{make\_cell}(\mathit{make\_iso}(t'')) & \text{if } t_y = \mathit{make\_cell}(\_)\\
t_y & \text{otherwise}
\end{cases}$ ass:cases

There are two rules that step the configuration:

* cmd-exit

* $de'' = \Use$

* $x~\textit{fresh}$

* $de' = e[x\mapsto x']$

* The resulting configuration is well-formed by the
alpha conversion property with [pf]ass:wfe.

* Since the $de''$ is non-dynamic, we have
$\many{\Gamma}'' = \varepsilon$.

* The effect is well-formed by induction over the
shape of $t_z$. In the inductive cases we use
wf-eff-split. In the base case we use
wf-eff-exit with ass:inner,
ass:isoimm, ass:mut, ass:iso,
ass:tmpvar and ass:cases.

* cmd-ec

Preservation holds by induction on the shape of $t_z$. In
the inductive cases we use wf-eff-split. In the base
case we use cmd-dyn-ty-let with
cmd-dyn-ty-entered with the assumptions given by the
inversion lemma.

Note that the induction hypothesis only gives
well-formedness for $\Eff$ for $\many{\Gamma}'$, but
adding $\Gamma'_1$ to the right of $\many{\Gamma}'$
does not affect well-formedness of the effect since the
well-formedness rules for effects looks at the dynamic
typing context from the left.

§.§ Theorem: Progress of Region Semantics

\[
\begin{array}{l}
\vdash \langle\SB de \FB~\langle\RS; H_{op}; H_{cl}; H_{fr}\rangle \land \SB de \FB \xrightarrow{\Eff} \SB de' \FB \implies\\
\quad\exists \Eff', \SB de \FB \xrightarrow{\Eff'} \SB de' \FB ~\land~ \langle\RS; H_{op}; H_{cl}; H_{fr}\rangle \xrightarrow{\Eff'} \langle\RS'; H'_{op}; H'_{cl}; H'_{fr}\rangle
\end{array}
\]

§.§.§ Proof Sketch

The proof of progress ensures that if the command semantics
produces a well-formed effect, there is an effect that steps both
the command semantics and the region semantics. In practice the
two effects will only be different for dynamic type tests, where
the command semantics always allows both effects $\mathit{cast}$
and $\mathit{nocast}$ with any type argument, and when
entering a region, where the command semantics always allows
both the effects $\mathit{enter}$ and $\mathit{badenter}$. The
region semantics is always able to “select” an effect that works
for both semantics.

The rest of the proof is straightforward and comes down to the
fact that looking up a well-defined name in a well-formed state
always succeeds.

§.§.§ Proof of Theorem

Whenever we have a well-formed $\Use$ of a variable, the
corresponding $\Get$ in the region semantics produces a value of
the corresponding type, and looking up that value in the region
stack or heap produces an object of that type. We call this the
well-formed lookup property and it follows from lemmas
<ref>, <ref> and

We will sometimes use the $\CapOK$ property to narrow where we are
looking for an object. For example, we know that a
reference points to an open heap region.

Similarly, an update of an existing object via a $\mathsf{store}$,
$\mathsf{stack\_store}$ or $\mathsf{heap\_store}$ always succeeds.
We call this property well-formed stores.

We start the proof by inversion of tandem-wf and get
$\many{\Gamma} \vdash \SB de \FB$. By preservation of the command
language we get $\many{\Gamma} \vdash \Eff \dashv \many{\Gamma}'$.
We proceed by induction over the well-formed effect judgment.

wf-eff-eps, $\Eff = \epsilon$

The configuration steps trivially by region-eps.

wf-eff-load, $\Eff = \load{x, y.f}$

* $\many{\Gamma} = \Gamma :: \many{\Gamma}_2$ass:gammas

* $x~\mathit{fresh}$ass:fresh

* $\Gamma(y) = k~CL$ass:y

* $\mathbf{ftype}(CL, f) = t$ass:ftype

* $k \neq \Iso{}$ass:niso

* By wf-rs-cons with ass:gammas we have
$\RS = (r, S, F) :: \RS'$.

* By well-formed lookup with ass:y we get
$F(y) = (k, \iota)$.

* Since only  references can point to closed regions
by , by ass:niso and well-formed lookup we have
$\CfgLoad((r, S, F) :: \RS', H_{op} \c{*} H_{fr}, \iota) = o[f
\mapsto v]$.

* The configuration steps with $\Eff$ by region-load with $\Eff$.

wf-eff-swap-class, $\Eff = \swap{x, y.f, \Use}$[pf]case:swap

* $\many{\Gamma} = \Gamma :: \many{\Gamma}_2$ass:gammas

* $x~\mathit{fresh}$ass:fresh

* $\Gamma \vdash \Use : t \dashv \Gamma'$ass:use

* $\Gamma'(y) = k~CL$ass:y

* $\mathbf{ftype}(CL, f) = t$ass:ftype

* $k \in \{\Mut{}, \Tmp{}\}$ass:k

* By wf-rs-cons with ass:gammas we have
$\RS = (r, S, F) :: \RS'$.

* By well-formed lookup with ass:use we get
$\Get(F, \Use) = (v, F')$ with a well-formed $F'$ under

* By well-formed lookup with ass:y we get
$F'(y) = (k, \iota)$.

* We proceed by cases on ass:k

$k = \Mut{}$

* By  $\iota$ points into region $r$ on the heap
and we have $H_{op} = (r, S')$.

* By well-formed lookup we have
$\mathsf{load}(S', \iota) = o[f \mapsto v']$.

* By well-formed stores we have
$\mathsf{store}(S', \iota, o[f \mapsto v]) = S''$.

* The configuration steps by region-swap-heap with $\Eff$.

$k = \Tmp{}$[pf]case:swap_tmp

* By  $\iota$ points into $S$ on the region

* By well-formed lookup we have
$\mathsf{load}(S, \iota) = o[f \mapsto v']$.

* By well-formed stores we have
$\mathsf{store}(S, \iota, o[f \mapsto v]) = S'$.

* The configuration steps by region-swap-temp with $\Eff$.

wf-eff-swap-var, $\Eff = \swap{x, y.\c{val}, \Use}$

Similar to [pf]case:swap going into [pf]case:swap_tmp.

wf-eff-halloc-mut, $\Eff = \halloc{x, \Mut{}, \#C, \Use_1, ..., \Use_n}$[pf]case:halloc_mut

* $\many{\Gamma} = \Gamma_1 :: \many{\Gamma}_2$ass:gammas

* $x~\mathit{fresh}$ass:fresh

* $\mathbf{ftypes}(C) = f_1 : t_1, ..., f_n : t_n$ass:ftypes

* $\forall i \in [1,n]. \Gamma_i \vdash \Use_i : t_i \dashv \Gamma_{i+1}$ ass:args

* By wf-rs-cons with ass:gammas we have
$\RS = (r, S, F_1) :: \RS'$.

* By induction over $n$, and by well-formed lookup we have
$\forall i \in [1,n]. \Get(F_i, \Use_i) = (v_i, F_{i+1})$.

* By ass:ftypes and the assumptions of the class
table we have $\mathbf{fields}(C) = f_1, ..., f_n$.

* The configuration steps by region-alloc-heap-mut with $\Eff$.

wf-eff-halloc-iso, $\Eff = \halloc{x, \Iso{}, \#C, \Use_1, ..., \Use_n}$

Similar to [pf]case:halloc_mut.

wf-eff-salloc, $\Eff = \salloc{x, k, \#CL, \Use_1, ..., \Use_n}$

Similar to [pf]case:halloc_mut, but the allocation happens on
the region stack instead.

wf-eff-freeze, $\Eff = \freeze{x,\Use}$[pf]case:freeze

* $\many{\Gamma} = \Gamma :: \many{\Gamma}_2$ass:gammas

* $x~\mathit{fresh}$ass:fresh

* $\Gamma \vdash \Use : t \dashv \Gamma'$ass:use

* $\Kap(\Iso{}, t)$ass:iso

* By wf-rs-cons with ass:gammas we have
$\RS = (r, S, F) :: \RS'$.

* By well-formed lookup with ass:use we get
$\Get(F, \Use) = ((k, \iota), F')$.

* By  an  reference in a variable, like
$\iota$, must point into a closed region $R$, so that
$H_{cl} = R \c{*} H'_{cl}$.

* By , outgoing references from a closed region
cannot go into an open region. This means that any regions
reachable from $R$ must also be closed, allowing us to write
$H_{cl}$ as $R \c{*} (H \c{*} H''_{cl})$ where
$H = \mathsf{reachable\_regions}(R, (H \c{*} H''_{cl})\c{*}

* The configuration steps by region-freeze with $\Eff$.

wf-eff-merge, $\Eff = \merge{x,\Use}$

Similar to [pf]case:freeze.

wf-eff-bind, $\Eff = \bind{x_1 = \Use_1, ..., x_n = \Use_n}$

* $\many{\Gamma} = \Gamma_1 :: \many{\Gamma}_2$ass:gammas

* $\forall i \in [1,n]. x_i~\mathit{fresh}$ass:fresh

* $\forall i \in [1,n]. \Gamma_i \vdash \Use_i : t_i \dashv \Gamma_{i+1}$ ass:uses

* By wf-rs-cons with ass:gammas we have
$\RS = (r, S, F) :: \RS'$.

* By induction over $n$, and by well-formed lookup we have
$\forall i \in [1,n]. \Get(F_i, \Use_i) = (v_i, F_{i+1})$.

* The configuration steps by region-bind with $\Eff$.

wf-eff-cast, $\Eff = \cast{x, \Use, k~C}$

* $\many{\Gamma} = \Gamma :: \many{\Gamma}_2$ass:gammas

* $x~\mathit{fresh}$ass:fresh

* $\Gamma \vdash \Use : t \dashv \Gamma'$ass:use

* By wf-rs-cons with ass:gammas we have
$\RS = (r, S, F) :: \RS'$.

* By well-formed lookup with ass:use we get
$\Get(F, \Use) = ((k, \iota), F')$ with a well-formed $F'$
under $\Gamma'$.

* By well-formed lookup we get
$\CfgLoad((r, S, F') :: \RS', H_{op} \c{*} H_{cl} \c{*}
H_{fr}, \iota) = (\#C', \_)$.

* We proceed by cases on whether $k C' <: t$ or not

* If $k C' <: t$, the command configuration steps by
cmd-if-typetest-true with effect $\cast{x, \Use, k~C}'$,
and the region configuration steps by region-cast with
the same effect.

* If $k C' \not<: t$, the command configuration steps by
cmd-if-typetest-false with effect
$\nocast{x, \Use, k~C'}$, and the region configuration steps
by region-nocast with the same effect.

wf-eff-nocast, $\Eff = \nocast{x, \Use, k~C}$

Similar to the previous case.

wf-eff-enter, $\Eff = \enter{w, k, y.f, x_1 = \Use_1, ..., x_n = \Use_n}$

* $\many{\Gamma} = \Gamma :: \many{\Gamma}_2$ass:gammas

* $w~\mathit{fresh}$ass:fresh

* $\forall i \in [1,n]. x_i~\mathit{fresh}$ass:freshs

* $\forall i \in [1,n]. \Gamma_i \vdash \Use_i : t_i \dashv \Gamma_{i+1}$ ass:uses

* $\Gamma_{n+1}(y) = k'~CL$ ass:yty

* $k' \in \{\Mut, \Tmp, \Var, \Paused\}$ ass:open

* $\mathbf{ftype}(CL, f)) = t$ ass:ftype

* $\Kap(\Iso, t)$ ass:iso

* $k \in \{\Tmp, \Var\}$ass:k

* By wf-rs-cons with ass:gammas we have
$\RS = (r, S, F) :: \RS'$.

* By induction over $n$, and by well-formed lookup we have
$\forall i \in [1,n]. \Get(F_i, \Use_i) = (v_i, F_{i+1})$.

* By well-formed lookup we have $F_{n+1}(y) = (k', \iota)$.

* By  references which are $\mathbf{open}$ point to an
open region on the stack or heap. By well-formed lookup and by
ass:open we have
$\CfgLoad((r, S, F') :: \RS', H_{op}, \iota) = o[f \mapsto (\_, \iota')]$.

* We proceed by cases on whether $\iota'$ is in the domain
of any closed region.

* If it is, the configuration steps by region-enter-ok.

* If it is not, the configuration steps by region-enter-fail.

Similar to the previous case, noting that any destructive reads
will not have made $y$ undefined, as this would not have been
well-typed in the command semantics.

* $\many{\Gamma} = \Gamma' :: \Gamma[y : k~CL]:: \many{\Gamma}_2$ass:gammas

* $x~\mathit{fresh}$ass:fresh

* $k \in \{\Mut, \Tmp, \Var, \Paused\}$ ass:open

* $\Gamma' \vdash \Use : t \dashv \Gamma''$ ass:use

* $\Gamma''(w) = k'~CL'$ ass:wty

* $\mathbf{ftype}(CL', g)) = t'$ ass:gtype

* By wf-rs-cons with ass:gammas we have
$\RS = (r', S', F') :: (r, S, F) :: \RS'$.

* By well-formed lookup with ass:use we have
$\Get(F', \Use) = (v, F'')$.

* By well-formed lookup with ass:wty we have
$F''(z) = (\_, \iota')$ and
$\mathsf{load}(S', \iota') = o'[f' \mapsto(\_, \iota'')]$.

* By well-formed lookup with ass:gammas we have
$F(y) = (\_, \iota)$.

* Since $y$ is $\mathbf{open}$ by ass:open, by
$\iota$ points to the open heap or the region stack.
We proceed by cases.

* If $\iota$ points to the stack we have
$\mathsf{stack\_load}(r, S, F) :: \RS, \iota = o[f \mapsto
(k, \_)]$, and by well-formed stores
$\mathsf{stack\_store}((r, S, F) :: \RS, \iota, o[f \mapsto
(k, \iota'')]) = (r, S'', F)::\RS'$. The configuration steps
by region-exit-temp.

* If $\iota$ points to the heap we have
$\mathsf{heap\_load}(H_{op}, \iota) = o[f \mapsto
(k, \_)]$, and by well-formed stores that
$\mathsf{heap\_store}(H_{op}, \iota, o[f \mapsto
(k, \iota'')]) = H'_{op}$. The configuration steps by

* $\many{\Gamma} = \many{\Gamma}_0[x : t|t']$

* $\many{\Gamma}_0[x : t] \vdash \Eff \dashv \many{\Gamma}_1$

* $\many{\Gamma}_0[x : t'] \vdash \Eff \dashv \many{\Gamma}_1$

* By wf-vars-cons, the type $t_x$ of the value of $x$
must be a subtype of $t|t'$.

* By the subtyping rules, we must have $t_x <: t$ or
$t_x <: t'$. We proceed by cases.

* Without loss of generality, we assume $t_x <: t$ (the other case is symmetric).

* We have
$\many{\Gamma}_0[x : t] \vdash \langle\RS; H_{op}; H_{cl}; H_{fr}\rangle$

* Progress holds by the induction hypothesis.

§.§ Theorem: Preservation of Region Semantics

The region semantics has a property similar to preservation that we express like

\[
\begin{array}{l}
\many{\Gamma}; \Delta; \Psi \vdash \RCfg \AN
\CapOK(\RCfg) \AN
\TopOK(\RCfg) \AN
\RCfg \RegStep{\Eff} \RCfg' \AN
\many{\Gamma} \vdash \Eff \dashv \many{\Gamma}'
\implies \\
\quad\exists \Delta', \Psi'.\\
\qquad\many{\Gamma}'; \Delta'; \Psi' \vdash \RCfg' \AN
\CapOK(\RCfg') \AN
\TopOK(\RCfg')
\end{array}
\]

§.§.§ Proof Sketch

This is by far the most complex proof for this system. We proceed by induction
on the well-formedness relation for $\Eff$. The main problem here is the base
cases, for which we first prove well-typedness and then the invariants $\capok$ and
$\topok$. The proof of well-typedness is done by a standard induction
argument on the well-typedness relations for each part of the configuration. For
the invariants we argue about the restrictions of each reference in the object
graph, with regards to its capability.

Each step of the region configuration will have a corresponding action
(removal/addition of locations and references) on the region graph. Furthemore,
because of well-typedness we can express this action using only the object graph
$G(\RCfg)$, the region ordering $\rho(\Gammas, \RCfg)$  and $\Eff$. We use this
fact and the constraints imposed by the reference capabilities to argue that the
invariants hold in the resulting configuration.

§.§.§ Proof of Theorem

* $\RCfg \RegStep{\Eff} \RCfg'$

* $\many{\Gamma} \vdash \Eff \dashv \many{\Gamma}'$

* [pf]wf_rcfg$\many{\Gamma}; \Delta; \Psi \vdash \RCfg$

* [pf]capok $\CapOK(\RCfg)$

* [pf]topok $\TopOK(\RCfg)$

We proceed by structural induction on the derivation of $\Gammas \vdash \Eff
\dashv \Gammas'$

From wf-eff-cast we get

* $\Eff = \cast{x, use, k~CL}$

* $\many{\Gamma} = \Gamma :: \many{\Gamma}_0$

* gammausegamma $\Gamma \vdash use : t \dashv \Gamma'$

* $k~C <: t$

* $\many{\Gamma}' = \Gamma', x : t :: \many{\Gamma}_0$

From region-step-cast

* $\RCfg = \RCfglong{(r, S, F)::RS; H_{op}; H_{cl}; H_{fr}}$

* $\Get( \Use, F ) = ((k, \iota), F')$

* $\CfgLoad((r, S, F)::RS, \Hop * \Hcl * \Hfr, \iota) = (C, \_)$

* $F'' = F', x \mapsto (k, \iota)$

* newrcfg $\RCfg' = \RCfglong{(r, S, F'')::RS; \Hop; \Hcl; \Hfr}$

We apply lemma <ref>, and get

* a1 $\Delta; \Gamma' \vdash F'$

* a2 $\iota : \CL \in \Delta$

* a3 $k \CL <: t$

We apply wf-F-cons on a1, a2, a3 to

* $\Delta; \Gamma', x : t \vdash F''$

The rest of the configuraton remains unchanged. Therefore we can conclude that

* $\Gamma' :: \many{\Gamma}_0; \Delta; \Psi \vdash \RCfg'$

We now move to prove $\CapOK(\RCfg')$ and $\TopOK(\RCfg')$. Given that
$G(\RCfg) = \Graph = (\LocSet, \RefSet)$, $G(\RCfg') = \Graph' = (\LocSet', \RefSet')$ it follows
from <ref> that

* $\LocSet' = \LocSet$

* $\Graph' = \begin{cases}
\Graph + (\Root(r) \RefTo{x, k} \Loc_z) & \text{ if } \Use = z \\
\Graph - (\Root(r) \RefTo{z, k} \Loc_z)  +  (\Root(r) \RefTo{x,
k} \Loc_z) & \If \Use = \Drop z
\end{cases}$

* refgraph $\REF_\Graph(\Root(r), z) = (\Root(r) \RefTo{z, k} \Loc_z)$

* $\Loc_\Graph(\iota) = \Loc_z$

By [case]newrcfg, [pf]capok, refgraph

* $\rho = \rho(\Gammas, \RCfg) = \rho(\Gammas, \RCfg')$

* $\Cl = \Closed(\RCfg) = \Closed(\RCfg')$

* $\Fr = \Frozen(\RCfg) = \Frozen(\RCfg')$

* rordold $\RegionOrder1(\rho, \Cl, \Fr, \Root(r) \RefTo{z, k} \Loc_z)$

* locokold $\LocationOK1(\Root(r) \RefTo{z, k} \Loc_z)$

* varuniqold $\VarUnique(G(\RCfg))$

We proceed by cases of the value of $k$

$k = \Mut$

* $\varunique(\Graph')$ because of [pf]obs:varuniq_neq_var.

* $\regionorder(\rho, \Cl, \Fr, \Graph')$ By [case]rordold,
$\RegionOrder1(\rho, \Cl, \Fr, \Root(r)) \RefTo{x,
k} \Loc_z)$. It follows.

* $\locationok(\Graph')$ By [case]locokold,
$\LocationOK1(\Root(r) \RefTo{x, k} \Loc_z)$. It follows.

* $\deepfreeze(\Fr, \Graph')$ since no frozen regions have changed.

* $\topokgraph(\rho, \Fr, \Graph')$ since $k = \mut$ implies
$\rho \vdash \Rid(loc_z) \leq r$.

* $\entrypoints(\rho, \Graph')$ since we are not affecting entry

$k \in \{\Paused, \Tmp\}$ Similar to [case]scasemut.
$k = \Imm$
Similar to [case]scasemut, observing that $\Frozen(\RCfg) =
\Frozen(\RCfg')$ and that $\CapOK(\RCfg)$ implies $\Rid(\Loc_z) \in \Frozen(\RCfg)$.
$k = \Var$
Similar to [case]scasemut, with [pf]obs:varuniq_swap to get
$k = \Iso$
Similar to previous cases, using [pf]obs:topok_swap to get
$\topokgraph(\rho, \Graph')$

wf-eff-nocast Similar to [pf]case_eff_cast.
By rule wf-eff-split

* $\Gammas = \Gammas[x : t | t']$

* $\Gammas[x : t] \vdash \Eff \dashv \Gammas_1$

* $\Gammas[x : t'] \vdash \Eff \dashv \Gammas_2$

* $\Gammas' = \Gammas_1 | \Gammas_2$

By [pf]obs:wf_rcfg_split, and WLOG

* $\Gammas[x : t] \vdash \RCfg$

By induction hypothesis

* gammas1rcfg $\Gammas_1 \vdash \RCfg'$

* $\CapOK(\RCfg')$

* $\TopOK(\RCfg')$

By $\Gammas[x : t] \gammadefincl \Gammas[x : t']$,

* domgammas $\Gammas_1 \gammadefincl \Gammas_2$

By domgammas, gammas1rcfg, [pf]obs:wf_rcfg_gammas_extend

* $\Gammas_1 | \Gammas_2 \vdash \RCfg'$.

By wf-eff-enter

* $\Eff = \enter{w, k, y.f, x_1 = \Use_1, \dots, x_n = \Use_n}$

* $\Gammas = \Gammas_1 :: \Gammas^*$

* $\forall i \in [1, n]. \Gamma_i \vdash \Use_i \dashv \Gamma_{i+1}$

* $\Gamma_{n+1}(y) = k' \CL$

* $\open(k')$

* $\FType(CL, f) = t$

* kapt $\Kap(iso, t)$

* $k \in \{\Tmp, \Var\}$

* $k = \Var \implies k' = \Var$

* $t' = \Hmakemut(t)$

* typevpa
\forall i \in [1,n]. t_i' =
\begin{cases}
t_i & \text{ if } \Kap(iso, t_i) \\
\VPA{\Paused}{t_i} & \text{ otherwise}
\end{cases}

* gammadef $\Gamma = x_1 : t_1', \dots, x_n : t_n'$

* gammapdef $\Gamma' = \Gamma, w : k~\Cell[t']$

* $\Gammas' = \Gamma :: \Gamma_{n+1} :: \Gammas^*$

By region-enter-ok

* $\RCfg = \RCfglong{(r, S, F_1)::\RS; \Hop; (r', S') * \Hcl; \Hfr}$

* $w$ fresh

* $\forall i \in [1,n]. x_i \text{ fresh}$

* $\forall i \in [1,n]. \Get(F, \Use_i) = ((k_i, \iota_i), F_{i+1})$

* valvpa $\forall i \in [1,n] (k_i', \iota_i) =
\begin{cases}
(k_i, \iota_i) & \If k_i = \Iso \\
(\VPA{\Paused}{k_i}, \iota_i)) & \Ow
\end{cases}$

* fdef $F = [x_i \mapsto (k_i', \iota) \suchthat i \in [1, n]]$

* $F_{n+1}(y) = (k_{\mathsf{here}}, \iota)$

* cfgload $\CfgLoad((r, S, F_{n+1})::RS, \Hop, \iota) = o[f \mapsto (k_{\mathsf{bridge}}, \iota')]$

* $\iota' \in \dom(S')$

* $\iota''$ fresh

* $F' = F, w \mapsto (k, \iota'')$

* $RF = (r', [\iota'' \mapsto (\Cell, [\Valfield \mapsto (\Mut,
\iota')])], F')$

* $\RCfg' = \RCfglong{RF::(r, S, F_{n+1})::\RS; (r', S') * \Hop; \Hcl; \Hfr}$

By repeated application of lemma <ref>

* wffn1$\Delta; \Gamma_{n+1} \vdash F_{n+1}$

* $\iota_i : CL \in \Delta$

* deltasubtype $k_i \CL_i <: t_i$

For each $i$ we split into case on $k_i$:

$k = \Iso$ This, [case]deltasubtype, [case]typevpa, and [pf]obs:iso_subtype_implies_vpa_undefined implies that

* $\Kap(\Iso, t_i)$

By [case]typevpa and [case]valvpa,

* a $k_i' = k_i$

* b $t_i' = t_i$

Thus by [case]deltasubtype, a, b

* $k_i' CL <: t_i'$

$k \neq \Iso$ Similarly to first first subcase, [case]deltasubtype,
[case]typevpa, [pf]obs:iso_subtype_implies_vpa_undefined

* a $k_i' = \VPA{\Paused}{k_i}$

* b $t_i' = \VPA{\Paused}{t_i}$

Specifically $t_i'$ is well-defined, and thus, by a, b,
[case]deltasubtype, [pf]obs:vpa_subtype

* $k_i' CL <: t_i'$

We conclude that

* primesubtypes $\forall i \in [1, n]. k_i'~CL <: t_i'$

Starting with the $\Delta; \NilGamma \vdash \NilF$, by repeated application of
wf-F-cons, gammadef, fdef, [case]primesubtypes

* $\Delta; \Gamma \vdash F$

By [pf]obs:expanding_delta

* deltapdef $\Delta' = \Delta, \iota'' : \Cell[t']$

* wffconsrec $\Delta'; \Gamma \vdash F$

By wf-F-cons, wffconsrec, $k~\Cell[t'] <: k~\Cell[t']$

* wfrff $\Delta'; \Gamma' \vdash F'$

By cfgload and well-formedness of $\RCfg$

* $o[f \mapsto (k_{\mathsf{bridge}}, \iota')] = (\CLTag, F^*)$

* $\iota : \CL \in \Delta$

* $\Delta; \FTypes(\CL) \vdash F^*$

* $\iota' : \CL' \in \Delta$

* ref1 $k_{\mathsf{bridge}} \CL' <: t$

By kapt and ref1

* $k_{\mathsf{bridge}} = \Iso$

By ref1, [pf]obs:make_mut_subtype,

* subtypetp $\Mut \CL' <: \Hmakemut(t) = t'$

By deltapdef, cltag-cell, subtypetp

* bunch1$\CellTag \subtag \Cell[t']$

* $\iota'' : \Cell[t'] \in \Delta'$

* $\Delta'; \Valfield : t' \vdash \Valfield \mapsto (\Mut, \iota')$

* bunch2$\Delta; \NilDelta \vdash \NilS$

By bunch1 - bunch2, wf-subheap-cons,

* wfrfs $\Delta; \iota'' : \Cell[t'] \vdash \iota'' \mapsto (\CellTag, \Valfield
\mapsto (\Mut, \iota')$

From wfrfs, wfrff, wffn1, and [pf]wf_rcfg,
it follows that there is $\Delta_\RS, \Psi_\RS$ such that

* $\Gamma' :: \Gammas_1; \Delta'; \Delta_\RS, \iota'' : Cell[t'];  r', \Psi_\RS \vdash \RF :: (r, S, F_{n+1}) :: \RS$

By applying rules for well formedness, we end up with

* $\Gammas'; \Delta'; \Psi \vdash \RCfg'$

Now, we move on to $\CapOK(\RCfg')$.

We write $\Graph = G(\RCfg)$ and $\Graph' = G(\RCfg')$. Because of
well-formedness of $\RCfg$ and $\RCfg'$, these are well-formed.

We write

* $\rho = \rho(\Gammas, \RCfg) = r \rhosepe \rho^*$

* $\rho' = \rho(\Gammas', \RCfg') = r' \rhosep{y.f} r \rhosepe \rho^*$

We let $\Graph_i$ be defined as follows

* $\Graph_0 = \Graph + \ruut(r') + \temp(r', \iota'')$

* $\REF_i = \ruut(r) \refto{z_i, k_i} \loc_i = \REF_{\Graph_i}(\ruut(r), z_i)$

* $\REF_i' = \ruut(r') \refto{x_i, k_i'} \loc_i$

* $k_i' =
\begin{cases}
k_i & \If k_i = \iso \\
\paused \sees k_i & \Ow
\end{cases}

* $\Graph_{i+1} = \Graph_i - \REF_i + \REF_i'$ if $\Use_i = \Drop z_i$.

* $\Graph_{i+1} = \Graph_i + \REF_i'$ if $\Use_i = z_i$.

Then, from lemma <ref>,

* $\Graph' = \Graph_n + \ruut(r') \refto{w, k} \temp(r', \iota'') +
\temp(r', \iota'') \refto{\Valfield, \mut} \heap(r', \iota')$

We make some general observations:

If we have $\Graph, \rho, \Cl, \Fr, r$ such that $\vdash \rho, \Cl \cup \{r\},
\Fr$ and $r \not\in \Cl$

* If

* $\regionorder1(\rho, \Cl \cup \{r \}, \Fr, \Loc_1[r_1] \RefTo{f, k}
\Loc_2[r_2])$

$\RegionOrder1(r :: \rho, \Cl, \Fr, \Loc_1[r_1] \RefTo{f, k} \Loc_2[r_2])$

Follows by

* if $k \neq \Iso$, moving $r$ from the closed set to region stack does
not affect ordering of $r_1$ and $r_2$

* If $k = \Iso$, then either $r_2 = r'$ in which case $\topok(\RCfg)$
implies $r_1 = r$, thus $r :: \rho \vdash r_1 < r_2$.

Otherwise, $r_2 \neq r'$ and region order of $r_1$ and $r_2$ will be

This in turn implies

* If $\regionorder(\rho, \Cl \cup r, \Fr, \Graph)$, then $\regionorder(r :: \rho,
\Cl, \Fr, \Graph)$.

* If

* $\entrypointsok(r :: \rho, \Graph)$

* $r' \not\in r :: \rho$

* $\ruut(r) \refto{y, k_y} \loc_y \in \Graph$

* $\loc_y \refto{f', k_{f}} \Heap(r', \_) \in \Graph$

Then $\entrypointsok(r' \rhosep{y.f} r :: \rho, \Graph)$.

Follows from definition of $\entrypointsok$.

* $\topokgraph(\rho, \Fr, \Graph)$ implies $\topokgraph(r :: \rho, \Fr, \Graph)$.

Follows from that the relation on region ids defined by $\rho
\vdash r1 \leq r2$ is included in the relation defined by $r :: \rho \vdash
r1 \leq r2$.

* [pf]obs:enter_region_order_paused

* $\RegionOrder1(r :: \rho, \Cl, \Fr, \Loc_1[r_1] \RefTo{f, k}
\Loc_2[r_2])$

* $r_1 \in \rho$

* $k \neq \Iso$

Then $\regionorder1(r :: \rho, \Cl, \Fr, \Loc[r] \refto{f', \Paused \sees k}
\loc_2[r_2])$

Follows from case analysis on $k$.

* [pf]obs:enter_region_order_iso

* shit $\RegionOrder(r' :: r :: \rho, \Cl, \Fr, \ruut(r) \RefTo{f, \iso}
\Loc_2[r_2])$

* piss$r_2 \neq r'$

Then $\RegionOrder(r' :: r :: \rho, \Cl, \Fr, \ruut(r') \RefTo{f', \iso}
\Loc_2[r_2])$

Follow by the following argument:
(i) and capability $\iso$ implies that $r_2 \neq r$. Furthermore
$r_2 \neq r'$ by (ii), so we do not have $r' :: r :: \rho \vdash r
< r_2$. Also, $r \not\in \Fr$. Thus $r_2 \in Cl$, and thus the conclusion

* [pf]obs:enter_locationok_paused

* $\locationok1(\loc_1 \refto{f, k} \loc_2)$

* $k \neq \iso$

* $\locationok1(\ruut(r) \refto{f, \paused \sees k} \loc_2)$

Follows from case analysis on $k$.

* [pf]obs:enter_locationok_iso
Similary, if

* $\locationok1(\loc_1 \refto{f, \iso} \loc_2)$

* $\locationok1(\ruut(r) \refto{f, \iso} \loc_2)$

Because of these observations, and since adding locations does not affect
invariants we have

* $\varunique(\Graph_0)$

* $\regionorder(\rho', \Cl', \Fr, \Graph_0)$

* $\locationok(\Graph_0)$

* $\deepfreeze(\Fr, \Graph_0)$

* $\entrypoints(\rho', \Graph_0)$ using well-formedness to get $(\ruut(r)
\refto{y, k'} \loc_y) \in \Graph_0$, $(\loc_y \refto{f, \iso} \heap(r',
\iota')) \in \Graph_0$ and that $\kw{open}(k')$ implies $\Rid(\loc_y) \in \rho$.

* $\topokgraph(\rho', \Fr, \Graph_0)$

By an inductive argument on $i$, by cases on $k_i$:

$k = \var$ Implies $\Use_i = \Drop z_i$, and thus $\Graph_i =
\Graph_{i-1} - \REF_i + \REF_i'$.

* $\varunique(\Graph_i)$ follows from [pf]obs:varuniq_swap.

* $\regionorder(\rho', \Cl', \Fr, \Graph_i)$ follows from [pf]obs:enter_region_order_paused

* $\locationok(\Graph_i)$ follows from

* $\deepfreeze(\Fr, \Graph_i)$ follows from $r' \not\in \Fr$ and $\deepfreeze(\Graph_{i-1})$.

* $\entrypointsok(\rho', \Graph_i)$ since no entry points have changed,

* $\topokgraph(\rho', \Fr, \Graph_i)$ follows from $k_i = \paused$ and $\regionorder(\Graph_i)$

$k = \iso$ Implies $\Use_i = \Drop z_i$, and thus $\Graph_i =
\Graph_{i-1} - \REF_i + \REF_i'$.

* $\varunique(\Graph_i)$ follows from [pf]obs:varuniq_neq_var.

* $\regionorder(\rho', \Cl', \Fr, \Graph_i)$ follows from $\Rid(\loc_i)
\neq r'$
(from $\topokgraph(\rho', \Fr, \Graph_i)$) and

* $\locationok(\Graph_i)$ follows from [pf]obs:enter_locationok_iso

* $\deepfreeze(\Graph_i)$ follows from $r' \not\in \Fr$ and $\deepfreeze(\Graph_{i-1})$.

* $\entrypointsok(\rho', \Graph_i)$ since no entry points have changed,

* $\topokgraph(\rho', \Fr, \Graph_i)$ follows from
[pf]obs:topok_swap and that $\Rid(\loc_i) \in \Cl$ (which
implies that we do not have $\rho' \vdash \rid(\loc_i) \leq r$).

From a simple case analysis on $k$, and the observation that there is no
reference $\REF$ in $\Graph_{n}$ such that $\REF$ points to $\temp(r',
\iota'')$, we have

* $\varunique(\Graph')$

* $\regionorder(\rho', \Cl', \Fr, \Graph')$

* $\locationok(\Graph')$

* $\deepfreeze(\Fr, \Graph')$

* $\topokgraph(\rho', \Cl', \Fr, \Graph')$

* $\capok(\RCfg')$

* $\topok(\RCfg')$

We have

* $\Eff = \swap{x, y.\Valfield, \Use}$

* $\Gammas = \Gamma :: \Gamma^*$

* gammausegammap $\Gamma \vdash \Use : t \dashv \Gamma'[y: \var~\Cell[t']]$

* capnotvar $\Kap(\{ \var \}^c, t)$

* $\Gammas' = \Gamma'[y : \var~\Cell[t]], x : t :: \Gamma^*$

* $\Graph = G(\RCfg)$

* $\rho = \rho(\RCfg)$

* $\Cl = \Closed(\RCfg)$

* $\Fr = \Frozen(\RCfg)$

There are two cases for the dynamic execution of $\Eff$:
region-swap-heap and region-swap-temp. However, the
former is impossible because of well-formedness and $\capok(\RCfg)$,
specifically $\locationok(\Graph)$ and $\regionorder(\rho, \Cl, \Fr, \Graph)$,
which says that $y$ with $\var$ capability must point to the temporary store in
the top region frame.

By region-swap-temp

* $\RCfg = \RCfglong{(r, S, F)::RS; \Hop; \Hcl; \Hfr}$

* $x$ fresh

* $\Get(F, \Use) = ((k, \iota), F')$

* $F'(y) = (k_y, \iota_y)$

* $\load{S, \iota_y} = o[\Valfield \mapsto (k', \iota')]$

* $o' = o[\Valfield \mapsto (k, \iota)]$

* $\store(S, \iota, o') = S'$

* $F'' = F', x \mapsto (k', \iota')$

* $\RCfg' = \RCfglong{(r, S', F'')::RS; \Hop; \Hcl; \Hfr}$

We note that

* $\rho' = \rho(\RCfg') = \rho$

* $\Cl' = \Closed(\RCfg') = \Cl$

* $\Fr' = \Closed(\RCfg') = \Fr$

By well-formedness of $\RCfg$ we have

* deltadeltass$\Delta; \Delta_S \vdash S$

Using lemma <ref>, we know

* deltagammapfp $\Delta; \Gamma'[y : \var~\Cell[t']] \vdash F'$

We argue that there is a $\Delta'$ such that $\Gammas'; \Delta'; \Psi \vdash
\RCfg$.
We know $\iota_y : \Cell[\_]$ is in $\Delta$ since $\RCfg$ is well typed.

* $\Delta = \Delta^*[\iota_y : \Cell[\_]]$

* $\Delta' = \Delta^*[\iota_y : \Cell[t]]$

By induction on the structure of the derivation on deltagammapfp

* deltapgammapfpp $\Delta'; \Gamma'[y : \var~\Cell[t]] \vdash F''$

By induction on the structure of the derivation of deltadeltass

* $\Delta_S = \Delta_S^*[\iota_y : \Cell[\_]]$

* $\Delta_S' = \Delta_S^*[\iota_y : \Cell[t]]$

* deltadeltaspsp $\Delta'; \Delta_S' \vdash S'$

For any frame $(\_, \_, F_1) \in RS$ there is a corresponding $\Gamma_1 \in
\Gammas^*$. By induction on structure of $\Delta; \Gamma_1 \vdash F_1$: if
$x \mapsto (k_x, \iota_x) \in F_1$, and corresponding typing $x : t_x$, then
$\iota_x \neq \iota_y$, since otherwise we would contradict
$\varunique(\Graph)$. We conclude that $\iota_x : \CL \in \Delta \implies
\iota_x : \CL \in \Delta'$ and thus $k_x \CL <: t_x$. Thus by wf-F-cons we
can conclude that

* $\Delta'; \Gamma_1 \vdash F_1$

A analogous argument holds for any $(\CLTag, F_2)$ in $\Hop * \Hcl * \Hfr$,
with rule wf-subheap-cons.

Thus all subheaps and frames are well-formed under $\Gammas'; \Delta'; \Psi$,
allowing us to conclude that

* $\Gammas'; \Delta'; \Psi \vdash \RCfg'$

Letting $\Graph = G(\RCfg)$, by lemma <ref>

* $
\Graph' =
\begin{cases}
\Graph - (\ruut(r) \refto{z, k_z} \loc_z) - (\loc_y \refto{f,
k_f} \loc_f) + (\loc_y \refto{f, k_z} \loc_z) & \If \Use = \Drop
z \\
\Graph - (\loc_y \refto{f, k_f} \loc_f) + (\loc_y \refto{f, k_z}
\loc_z) & \Ow
\end{cases}

* $\varunique(\Graph')$ holds because of [pf]obs:varuniq_neq_var
and [pf]obs:varuniq_swap, because the only way to break the invariant
is if $k_z = \var$. But this implies $\Use = \Drop z$ and thus we remove the
old reference to $\loc_z$.

* $\regionorder(\rho, \Cl, \Fr, \Graph')$ holds because region
$\rid(\ruut(r)) = \rid(\loc_y)$, i.e. the new reference will have the same
relation between start and end region.

* $\locationok(\Graph')$ follows from a case analysis on $k_z$, notin $k_z \neq \var$ by gammausegammap and capnotvar.

* $\deepfreeze(\Fr, \Graph')$ holds since $r \not\in \Fr$.

* $\entrypointsok(\rho, \Graph')$ since no entrypoints have changed.

* $\topokgraph(\rho, \Fr, \Graph')$ holds by case analysis on $k_z$, using
$\regionorder(\rho, \Cl, \Fr, \Graph')$ and [pf]obs:topok_swap.

We have

* $\Eff = \swap{x, y.f, \Use}$

* $\Gammas = \Gamma :: \Gamma^*$

* gammausegammap $\Gamma \vdash \Use : t \dashv \Gamma'$

* capnotvar $\Kap(\{ \var \}^c, t)$

* $\Gamma(y) = k \CL$

* $k \in \{\mut, \tmp\}$

* $\Gammas' = \Gamma'[y : k \CL], x : t :: \Gamma^*$

This case is similar to case [pf]case_eff_swap_var above. One thing to
note is that the case where $k = \mut$ together with $\vdash k \CL$ (from
lemmas <ref>, <ref>) implies that the
reference specified by $\Use$ will be either $\imm, \iso$ or $\mut$, (i.e. a
reference to a closed, frozen or within the same region) which will
allow us to prove $\capok$ and $\topok$.

We have

* $\Eff = \exit{x, \Use, y.f, w.g}$

* $\Gammas = \Gamma' :: \Gamma[y : k \CL] :: \Gammas^*$

* $k \in \{ \var, \tmp, \mut, \paused \}$

* $\Gamma' \vdash \Use : t \dashv \Gamma''$

* $\Kap(\{ \iso, \imm \}, t)$

* $\Gamma''(w) = k' \CL'$

* $\FType(\CL', g) = t'$

* $\Kap(\mut, t')$

* $\Kap(\iso, \FType(\CL, f))$

* $
k'' \CL'' =
\begin{cases}
\var \Cell[\Hmakeiso(t')] & \If k \CL = \var~\Cell[\_] \\
k \CL & \Ow
\end{cases}

* $\Gammas' = \Gamma[y : k'' \CL''], x : t :: \Gammas^*$

For the dynamic rule we have two cases: region-exit-temp and

* $\RCfg = \RCfglong{(r', S', F') :: (r, S, F) :: RS; (r', S_{op}) *
\Hop; \Hcl; \Hfr}$

* $x$ fresh

* $\Get(F', \Use) = ((k_z, \iota_z), F'')$

* $F''(w) = (k_w, \iota')$

* $\sload(S', \iota') = o'[g \mapsto (k_g, \iota'')]$

* $F(y) = (k_y, \iota)$

* $\stackload((r, S, F) :: \RS, \iota) = o[f \mapsto(k_f, \iota_f)]$

* $\stackstore((r, S, F) :: \RS, \iota, o[f \mapsto (k_f, \iota'')]) =
(r, S'', F) :: \RS'$

* $F''' = F, x \mapsto (k_z, \iota_z)$

* $\RCfg' = \RCfglong{(r, S'', F''') :: RS'; \Hop; (r', S_{op}) * \Hcl;
\Hfr}$

* $\RCfg = \RCfglong{(r', S', F') :: (r, S, F) :: RS; (r', S_{op}) *
\Hop; \Hcl; \Hfr}$

* $x$ fresh

* $\Get(F', \Use) = ((k_z, \iota_z), F'')$

* $F''(w) = (k_w, \iota')$

* $\sload(S', \iota') = o'[g \mapsto (k_g, \iota'')]$

* $F(y) = (k_y, \iota)$

* $\heapload(\Hop, \iota) = o[f \mapsto(k_f, \iota_f)]$

* $\heapstore(\Hop, \iota, o[f \mapsto (k_f, \iota'')]) =
\Hop'$

* $F''' = F, x \mapsto (k_z, \iota_z)$

* $\RCfg' = \RCfglong{(r, S, F''') :: RS; \Hop'; (r', S_{op}) * \Hcl;
\Hfr}$

We note

* $\Graph = G(\RCfg)$

* $\rho = \rho(\RCfg) = r' :: r :: \rho^*$

* $\rho' = \rho(\RCfg') = r :: \rho^*$

* $\Fr = \Frozen(\RCfg) = \Frozen(\RCfg')$

* $\Cl = \Closed(\RCfg)$

* $\Cl = \Closed(\RCfg') = \Cl \cup \{ r' \}$

* $\Graph' = G(\RCfg')$

* $\varunique(\Graph)$

* $\regionorder(\rho, \Cl, \Fr, \Graph)$

* $\locationok(\Graph)$

* $\deepfreeze(\Graph)$

* $\entrypoints(\rho, \Graph)$

* $\topokgraph(\rho, \Fr, \Graph)$

We note the similarity between ret and reh, and furthermore note that the
they are similar to a $\swap$, with the extra action of popping a region

$\regionorder(\rho, \Cl, \Fr, \RCfg)$, $\topokgraph(\rho, \Graph)$,
$\locationok(\Graph)$, and $\entrypointsok(\rho, \RCfg)$ implies that the
only reference from another region into $r'$ is $\loc_y \refto{f, \iso}
\heap(r', \_)$. Thus we can construct $\Delta'$ from $\Delta$ by removing all
$\iota^* \in \Delta$ such that $\iota^* \in S'$. By these facts, we can

* $\Gamma[y : k \CL] :: \Gammas^*; \Delta'; \Psi \vdash \RCfglong{(r, S,
F)::RS; \Hop; (r', S_{op}) * \Hcl; \Hfr}$.

From similar reasoning to the swap
effects e.g. [pf]case_eff_swap_var above.

* $\Gammas'; \Delta'; \Psi \vdash \RCfg'$

By lemma <ref>, and well-formedness

* $
\Graph' = \Graph
\begin{aligned}[t]
&- \ruut(r') - \{ \temp(r', \_) \suchthat \temp(r', \_) \in \Graph \} \\
&- \{ \ruut(r') \refto{\_, \_} \_ \suchthat \ruut(r') \refto{\_, \_} \_ \in \Graph \} \\
&- \{ \temp(r', \_) \refto{\_, \_} \_ \suchthat \temp(r', \_) \refto{\_, \_} \_ \in \Graph \} \\
&+ \ruut(r) \refto{x, k_z} \loc_z \\
&- \loc_y \refto{f, \iso} \heap(r', \_) + \loc_y \refto{f, \iso} \heap(r', \iota'')
\end{aligned}

* $\Use = z$ or $\Use = \Drop z$.

* $\REF_\Graph(\ruut(r'), z) = \ruut(r') \refto{z, k_z} \loc_z$

* $\REF_\Graph(\ruut(r), y) = \ruut(r) \refto{y, k_y} \loc_y$

* $\REF_\Graph(\loc_y, f) = \loc_y \refto{f, \iso} \heap(r', \_)$

* kz $k_z \in \{ \imm, \iso \}$

* $k_y \in \{ \mut, \paused, \var, \tmp \}$

* $\REF_\Graph(\ruut(r'), w) = \ruut(r') \refto{w, k_w} \temp(r',
\iota')$

* $k_w \in \{ \tmp, \var \}$

* $\REF_\Graph(\temp(r', \iota'), g) = \temp(r', \iota') \refto{g, \mut}
\heap(r', \iota'')$

* $\varunique(\Graph')$ by applying observation
[pf]obs:subgraph_varuniq, and then using well-formedness and
\FType(\CL, f))$ to get $k_f \neq \var$ and $\Kap(\{\iso, \imm\}, t)$ to get
$k_z \neq \var$, and then applying observation

* $\regionorder(\rho', \Cl', \Fr, \Graph')$ by kz implying
$\Rid(\loc_z) \in \Cl \cup \Fr \subseteq \Cl' \cup \Fr$ thus
$\regionorder1(\rho', \Cl', \Fr, \ruut(r) \refto{x, k_z} \loc_z)$. Furthermore
$r' \in \Cl'$ and so
$\regionorder1(\rho', \Cl', \Fr, \loc_y \refto{f, \iso}
\heap(r', \iota''))$

* $\locationok(\Graph')$ by case analysis on $k_z$.

* $\deepfreeze(\Fr, \Graph')$ since frozen regions are unchanged.

* $\entrypointsok(\rho', \Graph')$ by arguing that all region ids in
$\rho$ are unique (by well-typedness of $\RCfg$) and thus by
$\topokgraph(\rho, \Graph)$ and [pf]obs:entrypoint_objects_disjoint
all entrypoint are disjoint and therefore the swap at $\loc_y$, field $f$,
does not affect any other entrypoint.

* $\topokgraph(\rho', \Fr, \Graph')$ by [pf]obs:topok_swap.

We have

* $\Eff = \freeze(x, \Use)$

* $\Gammas = \Gamma :: \Gammas^*$

* $\Gamma \vdash \Use : t \dashv \Gamma'$

* $\Kap(\iso, t)$

* $\Gammas' = \Gamma', x : \Hmakeimm(t) :: \Gammas^*$

By region-freeze

* $\RCfg = \RCfglong{(r, S, F) :: RS; \Hop; (R * H) * \Hcl; \Hfr}$

* $x$ fresh

* $\Get(F, \Use) = ((k, \iota), F')$

* $\iota \in \dom(R.S)$

* $H = \reachableregions(\iota, \Hop * H * \Hcl)$

* $F'' = F', x \mapsto (\imm, \iota)$

* $\RCfg' = \RCfglong{(r, S, F'') :: RS; \Hop; \Hcl; (R * H) * \Hfr}$

Well-typedness follows by induction on the well-formedness of the top region
frame. We have

* $\Gammas'; \Delta; \Psi \vdash \RCfg'$

We note

* $\rho = \rho(\Gammas, \RCfg) = \rho(\Gammas', \RCfg')$

* $\Cl = \Closed(\RCfg)$

* $\Fr = \Frozen(\RCfg)$

* $\Fr_{new} = \rids(R * H)$

* $\Cl' = \Cl - \Fr_{new} = \Closed(\RCfg')$

* $\Fr' = \Fr + \Fr_{new} = \Frozen(\RCfg')$

* $\Graph = G(\RCfg)$

* $\Graph' = G(\RCfg')$

* $\Use = \Drop z$

By lemma <ref>,

* $\Graph' =
\begin{aligned}[t]
\Graph - (\ruut(r) \refto{z, k_z} \loc_z[r']) + (\ruut(r) \refto{x, \imm} \loc_z[r'])
\end{aligned}

* $k_z = \iso$

* $\varunique(\Graph')$ since we do not handle $\var$ references.

* $\regionorder(\rho, \Cl', \Fr', \Graph')$ by noting that
$\reachableregions$ says that all references between two regions
reachable from $R$ will have both ends in $R * H$, and that $R$ is in $R *

* $\locationok(\Graph')$ noting that $\loc_z[r'] = \heap(r', \_)$ by
$\locationok(\Graph)$ and $k_z = \iso$.

* $\deepfreeze(\Fr', \Graph')$ by similar argument to $\reachableregions$.

* $\topokgraph(\rho, \Fr', \Graph')$ since $\Fr \subseteq \Fr'$ and $r'
\in \Fr'$.

* $\entrypointsok(\rho, \Graph')$ since entrypoints are unaffected.

We have

* $\Eff = \freeze(x, \Use)$

* $\Gammas = \Gamma :: \Gammas^*$

* $\Gamma \vdash \Use : t \dashv \Gamma'$

* $\Kap(\iso, t)$

* $\Gammas' = \Gamma', x : \Hmakeimm(t) :: \Gammas^*$

By region-merge

* $\RCfg = \RCfglong{(r, S, F) :: RS; (r, S') * \Hop; R * \Hcl; \Hfr}$

* $x$ fresh

* $\Get(F, \Use) = ((k, \iota), F')$

* $\iota \in \dom(R.S)$

* $R' = (r, S' \uplus R.S)$

* $F'' = F', x \mapsto (\mut, \iota)$

* $\RCfg' = \RCfglong{(r, S, F'') :: RS; R * \Hop; \Hcl; \Hfr}$

Well-typedness holds by induction on the well-formedness of the top frame and
region configuration heaps.

* $\Gammas'; \Delta; \Psi \RCfg'$

We note

* $\rho = \rho(\Gammas, \RCfg) = \rho(\Gammas', \RCfg')$

* $\Cl = \Closed(\RCfg)$

* $\Fr = \Frozen(\RCfg) = \Frozen(\RCfg')$

* $r' = R.r$

* $\Cl' = \Cl - r$

* $\Graph = G(\RCfg)$

* $\Graph' = G(\RCfg')$

* $\Use = \Drop z$

By lemma <ref>,

* $LOCS = \{ \Loc[r'] \suchthat \Loc[r'] \in \Graph \}$

* $LOCS' = \{ \Loc[r] \suchthat \Loc[r'] \in LOCS \}$

* $REFS = \{ \Loc \refto{f, k} \Loc' \suchthat \Loc \in LOCS \}$

* $REFS' = \left\{ \Loc[r] \refto{f, k} \Loc'[r_2'] \Suchthat \Loc[r'] \refto{f, k}
\Loc'[r_2] \in REFS \AN r_2' = \left[\begin{array}{ll}
r & \If r_2 = r' \\
r_2 & \Ow
\end{array}\right. \right\}$

* $
\Graph' =
\begin{aligned}[t]
\Graph & - LOCS + LOCS' - REFS + REFS' \\
&- (\ruut(r) \refto{z, \iso} \loc_z[r']) + (\ruut(r) \refto{x, \mut} \loc_z[r])
\end{aligned}

Now, we can conclude that

* $\varunique(\Graph')$ since each $\REF \in REFS$ has been replaced with
a corresponding one in $REFS'$.

* $\regionorder(\rho, \Cl', \Fr, \Graph')$ by case analysis on the
capability of the references in $REFS'$ reference $\loc_1[r_1] \refto{f, k}
\loc_2[r_2] \in REFS$, $k = \paused$ would violate $\regionorder(\rho, \Cl,
\Fr, \Graph)$, since $r' \in \Cl$.

* $\locationok(\Graph')$ by same argument as $\varunique$.

* $\deepfreeze(\Fr, \Graph')$ since we have not changed frozen regions.

* $\topokgraph(\rho, \Fr, \Graph')$ since intra-region references have been
converted to intra-region references, and iso-references (i.e. inter-region
references) have been converted to corresponding iso-references.

* $\entrypointsok(\rho, \Graph')$ since we have not touched entry points.

* $\Eff = \halloc{x, \iso, \#C, \Use_1, \dots, \Use_n}$

* $\Gammas = \Gamma_1 :: \Gammas^*$

* $x$ fresh

* $\vdash \iso~C$

* $\FTypes(C) = f_1 : t_1, \dots, f_n : t_n$

* $\forall i \in [1, n]. \Gamma_i \vdash \Use_i : t_i' \dashv \Gamma_{i+1} \AN
\Kap({iso, imm}, t_i) \AN t_i' <: t_i$

* $\Gamma_{n+1}, x : \iso~C :: \Gammas^*$

From region-alloc-heap-iso

* $\RCfg = \RCfglong{(r, S, F_1) :: RS; \Hop; \Hcl; \Hfr}$

* $x$ fresh

* $\forall i \in [1, n]. \Get(F_i, \Use_i) = ((k_i, \iota_i), F_{i+1})$

* $\kw{fields}(C) = f_1, ..., f_n$

* $o = (\#C, [f_1 \mapsto (k_1, \iota_1), ..., f_n \mapsto (k_n,
\iota_n)])$

* $\iota$ fresh

* $r'$ fresh

* $F' = F_{n+1}, x \mapsto (\iso, \iota)$

* $\RCfg = \RCfglong{(r, S, F_1) :: RS; \Hop; (r', [\iota \mapsto o]) *\Hcl; \Hfr}$

Well-typedness follows similarly to case $\swap()$, where we use an inductive
argument to account for the multiple $\Use_1, \dots, \Use_n$. $\capok$ and
$\topok$ follows from the observation that all references originating from the
created object is either $\iso$ or $\imm$, (i.e. $k_i \in \{ \iso, \imm \}$) implying that they point into closed or
frozen regions respectively. The object itself is created in a closed (fresh
region), to which we create an iso reference.

* $\Eff = \halloc{x, \mut, \#C, \Use_1, \dots, \Use_n}$

* $\Gammas = \Gamma_1 :: \Gammas^*$

* $x$ fresh

* $\vdash \mut~C$

* $\FTypes(C) = f_1 : t_1, \dots, f_n : t_n$

* $\forall i \in [1, n]. \Gamma_i \vdash \Use_i : t_i \dashv \Gamma_{i+1}$

* $\Gamma_{n+1}, x : \mut~C :: \Gammas^*$

From region-alloc-heap-mut

* $\RCfg = \RCfglong{(r, S, F_1) :: RS; (r, S') * \Hop; \Hcl; \Hfr}$

* $x$ fresh

* $\forall i \in [1, n]. \Get(F_i, \Use_i) = ((k_i, \iota_i), F_{i+1})$

* $\kw{fields}(C) = f_1, ..., f_n$

* $o = (\#C, [f_1 \mapsto (k_1, \iota_1), ..., f_n \mapsto (k_n,
\iota_n)])$

* $\iota$ fresh

* $S'' = S',\iota \mapsto o$

* $F' = F_{n+1}, x \mapsto (\mut, \iota)$

* $\RCfg = \RCfglong{(r, S, F_1) :: RS; (r, S'') * \Hop; (r', [\iota \mapsto o]) *\Hcl; \Hfr}$

Follows from a similar argument as the $\mut$ case for $\swap{}$, using an
inductive argument to account for the multiple $\Use_i$s.

* $\Eff = \halloc{x, k, \#C, \Use_1, \dots, \Use_n}$

* $\Gammas = \Gamma_1 :: \Gammas^*$

* $x$ fresh

* $k \in \{ \tmp, \var \}$

* $\vdash k~C$

* $\FTypes(C) = f_1 : t_1, \dots, f_n : t_n$

* $\forall i \in [1, n]. \Gamma_i \vdash \Use_i : t_i \dashv \Gamma_{i+1}$

* $\Gamma_{n+1}, x : k~C :: \Gammas^*$

From region-alloc-temp

* $\RCfg = \RCfglong{(r, S, F_1) :: RS; \Hop; \Hcl; \Hfr}$

* $x$ fresh

* $k \in \{ \tmp, \var \}$

* $\forall i \in [1, n]. \Get(F_i, \Use_i) = ((k_i, \iota_i), F_{i+1})$

* $\kw{fields}(C) = f_1, ..., f_n$

* $o = (\#C, [f_1 \mapsto (k_1, \iota_1), ..., f_n \mapsto (k_n,
\iota_n)])$

* $\iota$ fresh

* $S' = S,\iota \mapsto o$

* $F' = F_{n+1}, x \mapsto (k, \iota)$

* $\RCfg = \RCfglong{(r, S', F_1) :: RS; \Hop; (r', [\iota \mapsto o]) *\Hcl; \Hfr}$

Follows from a similar argument as the $\tmp$ or $\var$ case for $\swap{}$, using an
inductive argument to account for the multiple $\Use_i$s.

* $\Gammas = \Gamma :: \Gamma^*$

* $x$ fresh

* $\Gamma(y) = k \CL$

* $\FType(\CL, f) = t$

* $k \neq \iso$

* $\vdash k \sees t$

By region-load

* $\RCfg = \RCfglong{(r, S, F) :: \RS; \Hop; \Hcl; \Hfr}$

* $x$ fresh

* $F(y) = (k_y, \iota_y)$

* $\CfgLoad((r, S, F)::\RS; \Hop * \Hfr, \iota_y) = o[f \mapsto (k_f, \iota_f)$

* $F' = F, x \mapsto (k_y \sees k_f, \iota_f)$

Well-typedness follows from a similar argument to the $swap()$ cases. $\capok$
and $\topok$ follows from observation [pf]obs:graph_add_vpa_ref.

By trivial inductive argument on $\many{x = Use}$.

§.§.§ Observations for Proof

* [pf]obs:subgraph_varuniq
\[\Graph \subseteq \Graph' \AN \VarUnique(\Graph') \implies \VarUnique(\Graph) \]

* [pf]obs:varuniq_neq_var

* $\REF = \Loc_1 \RefTo{f, k} \Loc_2 \in \Graph$

* $k \neq \Var$

* $k' \neq \Var $

* $\VarUnique(\Graph )$

* $\VarUnique(\Graph + (\_ \RefTo{f', k'} \Loc_2))$

* $\VarUnique(\Graph - \REF + (\_ \RefTo{f', k'} \Loc_2))$

Follows from $k \neq \var$ implying that there is no reference $\_
\refto{g, k''} \loc_2$ with $k'' = \var$.

* [pf]obs:varuniq_swap $\VarUnique(\Graph) \AN  (\Loc_1 \RefTo{f,
\Var} \Loc_2) \in \Graph \implies \VarUnique(\Graph - (\Loc_1 \RefTo{f,
\Var} \Loc_2) + (\Loc_3 \RefTo{f', k'} \Loc_2)$

* [pf]obs:topok_swap If $\REF = (\Loc_1[r_1] \RefTo{f, k} \Loc_2[r_2]$),
$\REF' = (\Loc_1'[r_1'] \RefTo{f', k'} \Loc_2[r_2])$, $\REF \in \Graph$,
\vdash r_2 \leq r_1 \implies \rho \vdash r_2 \leq r_1'$ and

\[
\topokgraph(\rho, \Fr, \Graph)
\]

\[
\topokgraph(\rho, \Fr, \Graph - \REF + \REF')
\]

Follows from a simple case analysis on the clauses of $\toppok$.

* [pf]obs:wf_rcfg_gammas_extend

If $\Gammas_1 \gammadefincl \Gammas_2$ and
$\Gammas_1 \vdash \RCfg$, then $\Gammas_1 | \Gammas_2 \vdash \RCfg$.

* [pf]obs:wf_eff_result_subgamma If $\Gammas_1 \gammadefincl \Gammas_2$,
$\Gammas_1 \vdash \Eff \dashv \Gammas_1'$ and $\Gammas_2 \vdash \Eff \dashv
\Gammas_2'$, then $\Gammas_1' \gammadefincl \Gammas_2'$.

Follows by induction on $\Gammas_1 \vdash \Eff \dashv \Gammas_1'$.

* [pf]obs:wf_rcfg_split If $\Gammas[x : t | t'] \vdash \RCfg$, then
$\Gammas[x: t] \vdash \RCfg$ or $\Gammas[x : t'] \vdash \RCfg$

Follows since the actual type of $x$ must be a subtype of $t|t'$, meaning that
the actual type is a subtype of either $t$ or $t'$.

* [pf]obs:vpa_subtype If $t <: t'$, then $\VPA{k}{t} <: \VPA{k}{t'}$

* [pf]obs:iso_subtype_implies_vpa_undefined $t <: t'$ and
$\Kap(iso, t)$ implies that $\VPA{\Paused}{t} = \FUndef$. Follows by
definition of subtyping and view-point adaptation (<ref>).

* [pf]obs:expanding_delta $\Delta; \Gamma \vdash F$, $\iota \not\in
\dom(\Delta)$ then $\Delta, \iota : CL; \Gamma \vdash F$. Follows from that
$\iota \not\in \dom(\Delta)$ implies that $\iota \not\in \mathbf{rng}(F)$

* [pf]obs:make_mut_subtype If $t <: t'$ then $\Hmakemut(t) <:
\Hmakemut(t')$. Follows by induction on structure of $t$.

* [pf]obs:entrypoint_objects_disjoint

* $\entrypointsok(\rho, \Graph)$

* $\topokgraph(\rho, \Fr, \Graph)$

* $\rho$ contains unique region ids

* $\rho = \dots \rhosep{x.f} r' \dots \rhosep{y.g} r'' :: \dots \Nilrho$

* $\REF_\Graph(\ruut(r'), x) = \ruut(r') \refto{x, k_x} \loc_x$

* $\REF_\Graph(\ruut(r''), y) = \ruut(r'') \refto{y, k_y} \loc_y$

* Either $\loc_x \neq \loc_y$ or $f \neq g$.

Follows from uniqueness constraints of $\topokgraph$ and that $\rho$ does not
have repeated region ids.

* [pf]obs:top_iso_ref_closed
$\regionorder1(r :: \rho, \Cl, \Fr, (\ruut(r) \refto{x, \iso} \loc_x[r']))$,
then $r' \in \Cl$.

Follows by definition of $\regionorder1$

* [pf]obs:graph_add_vpa_ref

* $\rho = r :: \rho^*$

* $\vdash \rho, \Cl, \Fr$

* $\varunique(\Graph)$

* $\regionorder(\rho, \Cl, \Fr, \Graph)$

* $\locationok(\Graph)$

* $\deepfreeze(\Fr, \Graph)$

* $\topokgraph(\rho, \Fr, \Graph)$

* $\entrypointsok(\rho, \Graph)$

* $\ruut(r) \refto{x, k_x} \loc_x[r_x] \in \Graph$

* $\loc_x[r_x] \refto{f, k_f} \loc_f \in \Graph$

* $r_x \in \rho$

* $\REF = \ruut(r) \refto{z, k_x \sees k_f} \loc_f$

* $\varunique(\Graph + \REF)$

* $\regionorder(\rho, \Cl, \Fr, \Graph + \REF)$

* $\locationok(\Graph + \REF)$

* $\deepfreeze(\Fr, \Graph + \REF)$

* $\topokgraph(\rho, \Fr, \Graph + \REF)$

* $\entrypointsok(\rho, \Graph + \REF)$

Follows from a case analysis on $k_x, k_f$.

§.§ Theorem: Soundness of the Tandem Semantics

A well formed configuration is either done, is has reached a failed state
(because of failing to enter an already opened region), or can take a step to a
well formed configuration.

\[
\begin{aligned}
\vdash \langle \SB de \FB~\RCfg\rangle \implies de = \Use \OR
de = \mathbf{Failure} \OR \langle \SB de \FB~\RCfg \rangle \rightarrow
\langle \SB de' \FB~\RCfg' \rangle \AN \vdash \langle \SB de' \FB~\RCfg' \rangle
\end{aligned}
\]

§.§.§ Proof of Theorem

Follows from theorems <ref>, <ref>,
<ref>, and <ref>.

§.§ Lemma: Subtyping is Transitive

Subtyping is transitive, i.e. if $t_1 <: t_2$ and $t_2 <: t_3$, then $t_1 <: t_3$.

§.§.§ Proof of Lemma

By strong induction over the subtyping relations.

real proof

§.§ Lemma: get is Total

\[
\begin{array}{l}
\Delta; \Gamma \vdash F \AN \Gamma \vdash use : t \dashv \Gamma' \implies\\
\quad\exists F', k, \iota. \Get(F, use) = ((k, \iota), F')
\end{array}
\]

§.§.§ Proof of Lemma

By induction over the well-formedness judgment of $F$.

real proof

§.§ Lemma: Well-Formedness of

\[
\begin{aligned}
\forall &\Delta, \Gamma, \Gamma', use, F, F', k, \iota. \\
&\Delta; \Gamma \vdash F \AN \\
&\Gamma \vdash use : t \dashv \Gamma' \AN \\
&\Get(F, use) = ((k, \iota), F') \\
&\implies \\
&\Delta; \Gamma' \vdash F' \AN \\
&\iota : CL \in \Delta \AN \\
&k~CL <: t
\end{aligned}
\]

§.§.§ Observations

It is a simple exercise to prove the following observations

*  If $\Delta; \Gamma \vdash F$, then if
$\phi$ is a permutation of the order of the mappings in $\Gamma$ and $F$,
we have $\Delta; \phi(\Gamma) \vdash \phi(F)$.

*  If $t <: t'$, then $t[k/k'] <: t'[k/k']$ for all
capabilities $k, k'$.

§.§.§ Proof of Lemma

In order to prove the lemma we begin by stating the assumptions

* deltagammaf $\Delta; \Gamma \vdash F$

* gammausetgammap $\Gamma \vdash \Use : t \dashv \Gamma'$

* getfuse $\Get(F, \Use) = ((k , \iota), F')$.

By structural induction on $\Delta; \Gamma \vdash F$:

* $\Gamma = \Gamma_1, y : t_y$

* $F = F_1, y \mapsto (k_y, \iota_y)$

* $\Delta; \Gamma_1 \vdash F_1$

* $\iota_y : \CL_y \in \Delta$

* $k_y \CL_y <: t_y$

* $y \not\in \dom(F_1)$

We now split on cases of .

$\Use = z = y$ [pf]subcase:use_eq_z_eq_y

By lemma <ref> we we have

* a $\Kap(\{\Mut, \Tmp, \Paused, \Imm\}, t_y)$

* b $\Gamma' = \Gamma_1, y : t_y$

* c $t_y <: t$

By definition of  $\Get$

* $\Get(y, (F_1, y \mapsto (k_y, \iota_y))) = ((k_y, \iota_y), (F_1, y
\mapsto (k_y, \iota_y)))$

We can thus identify the following

* $k = k_y$

* $\iota = \iota_y$

* $\CL = \CL_y$

* $F' = F_1, y \mapsto (k_y, \iota_y)$

Together with these facts, and with observations
<ref>, <ref>, and lemma
<ref>, it follows that

* $\Delta; \Gamma' \vdash F'$

* $\iota : \CL \in \Delta$, and

* $k \CL <: t$.

$\Use = z \neq y$ [pf]subcase:use_eq_z_neq_y

Follows from definition of $\Get$ and application of induction hypothesis
together with observation <ref>.

$\Use = \kw{drop}~z$, $z = y$

This case is similar to [pf]subcase:use_eq_z_eq_y above .

$\Use = \kw{drop}~z$, $z \neq y$

Similar to [pf]subcase:use_eq_z_neq_y.

We have the assumptions

* $\Gamma = \Gamma_1, y : \Undef$

* $F = F_1, y \mapsto \Undef$

* $\Delta; \Gamma_1 \vdash F_1$

* $\iota_y : \CL_y \in \Delta$

* $k_y \CL_y <: t_y$

* $y \not\in \dom(F_1)$

Because $y$ is undefined in both $\Gamma$ and $F$, looking at the definition
of $\Get$ together with [pf]gammausetgammap, the only possible cases
are $\Use = \kw{drop}~z$ or $\Use = z$, where $z \neq y$. We can thus apply
the induction hypothesis similar to [pf]subcase:use_eq_z_neq_y above.

§.§ Lemma: Well-Formed cfg_load

\[
\begin{array}{l}
\RCfg = \RCfglong{RS; H_{op}; H_{cl}; H_{fr}} \AN
\Gammas; \Delta; \Psi \vdash \RCfg \AN
\iota : CL \in \Delta
\implies \\
\quad\CfgLoad(RS, H_{op} * H_{cl} * H_{fr}) = (CL, F) \AN
\Delta; \FTypes{CL} \vdash F
\end{array}
\]

§.§.§ Proof of Lemma

By induction over the well-formedness rules for $\RS$ and $H$.
Note that every $\iota$ in $\Delta$ maps to exactly
one object in the configuration.

real proof

§.§ Lemma: Well-Formed Environment

If $\Gamma \vdash b : t \dashv \Gamma'$, then $\vdash \Gamma$ and $\vdash
\Gamma'$.

§.§.§ Proof of lemma

By structural induction on $\Gamma \vdash b : t \dashv \Gamma'$.

§.§ Lemma: Well-Formed Type Under Environment

If $\vdash \Gamma$ and $\Gamma(x) = t$, then $\vdash t$.

§.§.§ Proof of lemma

By structural induction on $\vdash \Gamma$.

§.§ Inversion Lemma

Because of subtyping, we cannot invert typing judgments directly
to get useful information. Instead we prove an inversion lemma
that gives us the premises of the corresponding rule, with
subtyping information regarding the result type.

Because some of the type rules are only defined when variables
have types of the shape $k~CL$, we define a helper function for
calculating the type of a field lookup for type unions (this is
the result of typing *̧x̧.̧f̧ when $x$ has type $t$):

\[
\mathbf{fresult}(t, f) =
\begin{cases}
\VPA{k}{\mathbf{ftype}(CL, f)} & \text{if } t = k~CL\\
\mathbf{fresult}(t_1, f)~|~\mathbf{fresult}(t_2, f) & \text{if } t = t_1~|~t_2
\end{cases}
\]

When doing strong updates of ref cells, we need to turn a union of
types into a union of  types:

\[
\begin{array}{rcl}
\mathit{make\_cell}(k~CL) & = & \Var{}~\Cell[k~CL]\\
\mathit{make\_cell}(t_1~|~t_2) & = & \mathit{make\_cell}(t_1) ~|~ \mathit{make\_cell}(t_2)
\end{array}
\]

When freezing a type, we need to change  capabilities to :

\[
\begin{array}{rcl}
\mathit{make\_imm}(k~CL) & = &
\begin{cases}
\Imm~CL & \text{if } k = \Iso\\
k~CL    & \text{otherwise}
\end{cases}\\
\mathit{make\_imm}(t_1~|~t_2) & = & \mathit{make\_imm}(t_1) ~|~ \mathit{make\_imm}(t_2)
\end{array}
\]

The inversion lemma itself is stated as follows:

\[
\begin{array}{rcl}
\Gamma \vdash x : t \dashv \Gamma' & \iff &
\vdash \Gamma \AN \Gamma = \Gamma_1[x : t'] \AN t' <: t \AN
\Kap(\{\Iso, \Var\}^c, t') \AN\\
&    & \Gamma' = \Gamma_1[x : t']\\
\\

\Gamma \vdash \kw{drop}~x : t \dashv \Gamma' & \iff &
\vdash \Gamma \AN \Gamma = \Gamma_1[x : t'] \AN t' <: t \AN \Gamma' = \Gamma_1[x : \mathbf{undef}]\\
\\

\Gamma \vdash \c{*}x.f : t \dashv \Gamma' & \implies &
\Gamma(x) = t_x \AN \mathbf{fresult}(t_x, f) = t' \AN t' <: t\\
&    & \Kap(\{\Iso\}^c, t_x) \AN \forall k~CL\in t_x. \vdash \VPA{k}{t'}\\
\\

\Gamma \vdash \c{*}x : t \dashv \Gamma' & \implies &
\Gamma(x) = t_x \AN \mathbf{fresult}(t_x, \c{val}) = t' \AN t' <: t\\
&    & \Kap(\Var{}, t_x) \AN \vdash \VPA{\Var{}}{t'}\\
\\

\Gamma \vdash x.f~\c{:=}~\Use : t \dashv \Gamma' & \implies &
\Gamma \vdash \Use : t' \dashv \Gamma' \AN \Gamma'(x) = t_x \AN\\
&    & \Kap(\{\Mut{}, \Tmp\}, t_x) \AN \mathbf{fresult}(t_x, f) = t' \AN t' <: t\\
\\

\Gamma \vdash x \c{:=}~\Use : t \dashv \Gamma' & \implies &
\Gamma \vdash \Use : t' \dashv \Gamma''[x : t_x] \AN \Kap(\Var{}, t_x) \AN\\
&    & \mathbf{fresult}(t_x, \c{val}) = t_f \AN t_f <: t \AN\\
&    & \Gamma' = \Gamma''[x : \mathit{make\_cell}[t']] \\
\\

\Gamma_1 \vdash \fnc(\Use_1,...,\Use_n) : t \dashv \Gamma_{n+1} & \implies &
\mathbf{fnctype}(\fnc) = t_1,...,t_n \rightarrow t' \AN t' <: t \AN\\
&   & \forall i \in [1,n]. \Gamma_i \vdash \Use_i : t_i \dashv \Gamma_{i+1}\\
\\

\Gamma \vdash \kw{var}~\Use : t \dashv \Gamma' & \implies &
\Gamma \vdash \Use : t' \dashv \Gamma' \AN \Var{}~\Cell[t'] <: t\\
\\

\Gamma_1 \vdash \kw{new}~k~C(\many{\Use}) : t \dashv \Gamma_{n+1} & \implies &
\vdash \Gamma_1 \AN \vdash k~C \AN k~C <: t \AN k\in\{\Mut, \Tmp, \Iso\} \AN \\
&    & \mathbf{ftypes}(C)= f_1:t_1,...f_n:t_n \AN \many{\Use} = \Use_1, ..., \Use_n \AN\\
&    & \forall i \in [1,n]. (\Gamma_i \vdash \Use_i : t'_i \dashv \Gamma_{i+1} \AN t'_i <: t_i)\\
&    & \quad k=\Iso \implies \Kap(\{\Iso, \Imm\}, t'_i)\\
\\

\Gamma \vdash \kw{freeze}~\Use : t \dashv \Gamma' & \implies &
\Gamma \vdash \Use : t' \dashv \Gamma' \AN \Kap(iso, t') \AN
\mathit{make\_imm}(t') <: t)\\
\\

\Gamma \vdash \kw{merge}~\Use : t \dashv \Gamma' & \implies &
\Gamma \vdash \Use : t' \dashv \Gamma' \AN \Kap(iso, t') \AN
\mathit{make\_mut}(t') <: t\\
\\
\text{Continued on next page...}
\end{array}
\]

\[
\begin{array}{l}
\Gamma_1 \vdash \kw{enter}~x.f~[\many{y=\Use}] \SB z~\c{=>}~e \FB : t \dashv \Gamma_{n+1} \implies\\
\quad\forall i \in [1,n]. \Gamma_i \vdash \Use_i : t_i \dashv \Gamma_{i+1} \AN \Gamma_{n+1}(x) = t_x \AN\\
\quad\Kap(\{\Mut, \Tmp, \Var, \Paused\}, t_x) \AN \\
\quad\mathbf{fresult}(t_x, f)) = t_f \AN \Kap(\Iso, t_f) \AN\\
\quad\Gamma = y_1 : t'_1, ..., y_n : t'_n \\
\quad\quad\text{ where } t'_i =
\begin{cases}
t_i & \text{if } \Kap(\Iso, t_i)\\
\VPA{\Paused}{t_i} & \text{otherwise}
\end{cases} \AN\\
\quad t_f' = \mathit{make\_mut}(t_f) \AN \Kap(\{\Iso, \Imm\}, t') \AN t' <: t \AN\\
\quad \Gamma, z : \Tmp~\Cell[t_f'] \vdash e : t' \dashv \Gamma', z : \Tmp~\Cell[t_f']\\
\\

\Gamma_1 \vdash \kw{enter}~x~[\many{y=\Use}] \SB z~\c{=>}~e \FB : t \dashv \Gamma' \implies\\
\quad \forall i \in [1,n]. \Gamma_i \vdash \Use_i : t_i \dashv \Gamma_{i+1} \AN \Gamma[x : t_x] = \Gamma_{n+1} \AN\\
\quad \Kap(\Var, t_x) \AN \\
\quad \mathbf{fresult}(t_x, \c{val})) = t_f \AN \Kap(\Iso, t_f) \AN\\
\quad \Gamma_y = y_1 : t'_1, ..., y_n : t'_n \\
\quad \quad\text{ where } t'_i =
\begin{cases}
t_i & \text{if } \Kap(\Iso, t_i)\\
\VPA{\Paused}{t_i} & \text{otherwise}
\end{cases} \AN\\
\quad t_z = \mathit{make\_cell}(\mathit{make\_mut}(t_f)) \AN \\
\quad t_z' = \mathit{make\_cell}(t_f') \AN\\
\quad \Gamma_y, z : t_z \vdash e : t' \dashv \Gamma_y', z : t_z' \AN \Kap(\{\Iso, \Imm\}, t') \AN\\
\quad \Kap(\Mut, t_f') \AN t' <: t \AN\\
\quad \Gamma' = \Gamma[x : t_x'] \AN t_x' = \mathit{make\_cell}(\mathit{make\_iso}(t_f'))\\
\end{array}
\]

\[
\begin{array}{l}
\Gammas \vdash \kw{entered}~x.f~y.\c{val} \SB de \FB : t \vdash \Gamma' \implies\\
\quad \Gammas = \many{\Gamma}' :: \Gamma_1 \underset{x.f}{::} \Gamma_0[x : t_x] \AN \\
\quad \Kap(\{\Mut, \Tmp, \Var, \Paused\}, t_x) \AN \mathbf{fresult}(t_x, f) = t_f \AN\\
\quad \Kap(\Iso{}, t) \AN \many{\Gamma}' :: \Gamma_1 \vdash de : t' \dashv \Gamma_1' \AN \Kap(\{\Iso{}, \Imm{}\}, t') \AN\\
\quad t' <: t \AN \Gamma_1'(y) = t_y \AN \mathbf{fresult}(t_y, \c{val}) = t'' \AN\\
\quad \Kap(\Mut{}, t'') \AN \Kap(\{\Tmp{}, \Var{}\}, t_y) \AN \Gamma' = \Gamma_0[x : t_x'] \AN\\
\quad t_x' =
\begin{cases}
\mathit{make\_cell}(\mathit{make\_iso}(t'')) & \text{if } t_x = \mathit{make\_cell}(\_)\\
t_x & \text{otherwise}
\end{cases}\\

\end{array}
\]

§.§.§ Proof of Lemma

We first prove the $\Rightarrow$-cases by induction over the
typing judgments. The only two interesting subcases are using the
rules cmd-ty-sub and cmd-ty-split, which are similar for
all the cases. We show the cases for $x$, $\kw{drop}~x$ and
function call here; the remaining cases are similar. More if
there is time

$\Gamma \vdash x : t \dashv \Gamma'$

* Proof follows immediately from reflexivity of subtyping

A1 $\Gamma \vdash x : t' \dashv \Gamma'$

A2 $t' <: t$

* By the induction hypothesis, we have $\Gamma(x) = t''$
and $t'' <: t'$,

* By transitivity of subtyping, we get $t'' <: t$.

* The remaining obligations follow from the induction

A1 $t = t_{x} | t'_{x}$

A2 $\Gamma = \Gamma_1[y : t_{y1} ~|~ t_{y2}]$

A3 $\Gamma_1[y : t_{y1}] \vdash x : t_{x} \dashv \Gamma_2$

A4 $\Gamma_1[y : t_{y2}] \vdash x : t'_{x} \dashv \Gamma_2'$

A5 $\Gamma' = \Gamma_2 ~|~ \Gamma_2'$

* if $x \neq y$ the proof follows from the induction

* If $x = y$, by the induction hypothesis we have
$t_{y1} <: t_{x}$ and
$t_{y2} <: t'_{x}$, that  is not
in the capabilities of $t_{y1}$ or $t_{y2}$, and that
$\Gamma_2(x) = t_{y1}$ and
$\Gamma_2'(x) = t_{y2}$.

* From the definition of $\Gamma_2 ~|~ \Gamma_2'$, we get
that $\Gamma'(x) = t_{y1}~|~t_{y2}$.

* From the subtyping rules, we get that
$t_{y1}~|~t_{y2} <: t_{x}~|~t'_{x}$.

$\Gamma \vdash \kw{drop}~x : t \dashv \Gamma'$

* Proof follows immediately

A1 $\Gamma \vdash \kw{drop}~x : t' \dashv \Gamma'$

A2 $t' <: t$

* By the induction hypothesis, we have $\Gamma(x) = t''$
and $t'' <: t'$,

* By transitivity of subtyping, we get $t'' <: t$.

* The remaining obligations follow from the induction

A1 $t = t_{x} | t'_{x}$

A2 $\Gamma = \Gamma_1[y : t_{y1} ~|~ t_{y2}]$

A3 $\Gamma_1[y : t_{y1}] \vdash \kw{drop}~x : t_{x} \dashv \Gamma_2$

A4 $\Gamma_1[y : t_{y2}] \vdash \kw{drop}~x : t'_{x} \dashv \Gamma_2'$

A5 $\Gamma' = \Gamma_2 ~|~ \Gamma_2'$

* if $x \neq y$ the proof follows from the induction

* If $x = y$, by the induction hypothesis we have
$t_{y1} <: t_{x}$ and $t_{y2} <: t'_{x}$, and that
$\Gamma_2(x) = \mathbf{undef}$ and
$\Gamma_2'(x) = \mathbf{undef}$.

* From the definition of $\Gamma_2 ~|~ \Gamma_2'$, we get
that $\Gamma'(x) = \mathbf{undef}$.

* From the subtyping rules, we get that
$t_{y1}~|~t_{y2} <: t_{x}~|~t'_{x}$.

$\Gamma \vdash \fnc(use_1,...,use_n) : t \dashv \Gamma'$

* Proof follows immediately from reflexivity of subtyping

A1 $\Gamma \vdash b : t' \dashv \Gamma'$

A2 $t' <: t$

* By the induction hypothesis, we have
$\mathbf{fnctype}(\fnc) = t_1,...,t_n \rightarrow
t''$ and $t'' <: t'$.

* By transitivity of subtyping, we get
$t'' <: t$.

* The rest of the obligations follow from the induction

A1 $t = t_{b1} | t_{b1}'$

A2 $\Gamma = \Gamma_1[x : t_{x1} ~|~ t_{x2}]$

A3 $\Gamma_1[x : t_{x1}] \vdash b : t_{b1} \dashv \Gamma_2$

A4 $\Gamma_1[x : t_{x2}] \vdash b : t_{b1}' \dashv \Gamma_2'$

A5 $\Gamma' = \Gamma_2 ~|~ \Gamma_2'$

* By the induction hypothesis, we have
$\mathbf{fnctype}(\fnc) = t_1,...,t_n \rightarrow
t'$, and $t' <: t_{b1}$ and $t' <: t_{b2}$.

* By the subtyping rules, $t' <: t_{b1} | t_{b1}'$.

* The arguments are typed using the same reasoning as in the
cases for $b = use$, but generalized to a sequence. We note
that a drop of the same variable cannot appear twice in
the same argument list.

We then prove the $\Leftarrow$-cases of $x$ and $\kw{drop}~x$ by
induction on the shape of $t'$.

$t' = k~CL$

$\Gamma_1[x : k~CL] \vdash x : t \dashv \Gamma_1[x : k~CL]$ by
cmd-ty-sub with cmd-ty-use-keep.

$t' = t'_1~|~t'_2$

* By the induction hypothesis, we have
$\Gamma_1[x : t'_1] \vdash x : t \dashv \Gamma_1[x : t'_1]$
$\Gamma_1[x : t'_2] \vdash x : t \dashv \Gamma_1[x : t'_2]$.

* By cmd-ty-split we have
$\Gamma_1[x : t'_1~|~t'_2] \vdash x : t~|~t \dashv \Gamma_1[x : t'_1~|~t'_2]$.

* Since $t~|~t <: t$, by cmd-ty-sub we have
$\Gamma_1[x : t'_1~|~t'_2] \vdash x : t \dashv \Gamma_1[x : t'_1~|~t'_2]$.

No induction is needed. We have
$\Gamma[x : t'] \vdash x : t \dashv \Gamma'[x : \Undef]$ by
cmd-ty-sub with cmd-ty-use-drop.

§.§ Graph Actions

To describe the action of an effect $\Eff$ on the object graph $\Graph$, we
make some basic definitions of what an graph action is. The main idea is
that each effect has some basic action consisting of removal and addition of
locations and references.

Given a configuration $\Gammas \vdash \RCfg$ and $\Gammas \vdash \Eff \dashv
\Gammas'$, the graph $G(\RCfg)$ is well defined and well formed. By progress,
WLOG we can assume that $\RCfg \RegStep{\Eff} \RCfg'$. For such an $\Eff$ we can
calculate a delta $\delta$ such that $G(\RCfg') = G(\RCfg) + \delta$ (this
addition is defined below). $\delta$, called a graph action, is a pair of set
actions, one for locations and one for references. A set action is a pair
of sets, one for removal and one for addition:

\[
\begin{array}{lcll}
\delta & \in & (\delta_\AllLocs, \delta_\AllRefs) & \text{Graph
action for
locations/references} \\
\delta_E & \in & \Pow(E) \times \Pow(E) & \text{Set action: pair of
\emph{remove} and \emph{add} set}
\end{array}
\]

For convenience we define

\[
\Nildelta = (\emptyset, \emptyset).
\]

Addition between a set $E$ and a $\delta = (E_\mathsf{r}, E_\mathsf{a})$ is
defined as

\[
\begin{array}{lcl}
E + (E_{\mathsf{r}}, E_{\mathsf{a}}) &=& (E \setminus E_{\mathsf{r}}) \cupdisj E_{\mathsf{a}}
\end{array}
\]

Given a graph action $\delta = (\delta_l, \delta_r)$ and a graph $\Graph =
(\LocSet, \RefSet)$, we define

\[
\begin{array}{lcl}
\Graph + \delta &=& (\LocSet + \delta_l, \RefSet + \delta_r) \\
\end{array}
\]

Furthermore for convenience, we define the addition of two actions $delta_1 =
(E^{\mathsf{r}}_1, E^{\mathsf{a}}_1)$ and $\delta_2 = (E^{\mathsf{r}}_2, E^{\mathsf{a}}_2)$ as

\[ \delta_1 + \delta_2 = (E^{\mathsf{r}}_1 \cupdisj E^{\mathsf{r}}_2,
E^{\mathsf{a}}_1 \cupdisj E^{\mathsf{a}}_2 ) \]

When not ambiguous, we can write

\[
\begin{array}{lcl}
\Graph + \LocSet &\equiv& \Graph + ((\emptyset, \LocSet), \Nildelta) \\
\Graph - \LocSet &\equiv& \Graph + ((\LocSet, \emptyset), \Nildelta) \\
\Graph + \Loc &\equiv& \Graph + ((\emptyset, \{\Loc\}), \Nildelta) \\
\Graph - \Loc &\equiv& \Graph + ((\{\Loc\}, \emptyset), \Nildelta) \\
\Graph + \RefSet &\equiv& \Graph + (\Nildelta, (\emptyset, \RefSet)) \\
\Graph - \RefSet &\equiv& \Graph + (\Nildelta, (\RefSet, \emptyset)) \\
\Graph + \REF &\equiv& \Graph + (\Nildelta, (\emptyset, \{\REF\})) \\
\Graph - \REF &\equiv& \Graph + (\Nildelta, (\{\REF\}, \emptyset))
\end{array}
\]

Both $+$ and $-$ associate to the left.

§.§ Lemma: Well-Defined Graph Actions

* $\Gammas \vdash \RCfg$

* $\Gammas \vdash \Eff \dashv \Gammas'$

* $\RCfg \RegStep{\Eff} \RCfg'$

then there is a unique $\delta$, such that

\[
G(\RCfg') = G(\RCfg) + \delta
\]

Furthermore, this $\delta$ can be computed using only $G(\RCfg), \rho(\Gammas, \RCfg),
\Eff$, and access to any fresh $\iota$ and $r$ used in the step.

§.§.§ Proof of Lemma

We prove this by defining a partial function, taking a $\rho = \rho(\Gammas, \RCfg)$,
$\Graph = G(\RCfg)$, and $\Eff$:

\[
\delta^*(\rho, \Graph, \Eff) = (\delta_{LOC}, \delta_{REF})
\]

In the cases below, we make statements of the form

\[
\REF_\Graph(\Loc, f) = (\Loc \RefTo{f, k_f} \Loc_f)
\]

These equalities are well-defined because of the well formedness of $\RCfg$ and
$\Eff$. Furthermore, uniqueness of $\delta$ follows from that $\REF_\Graph$ is a
partial function.

$\enter{w, k, y.f, \many{x = \Use}}$

\[
\delta^*(r :: \rho, \Graph, \enter{w, k, y.f, \many{z = \Use}}) = (\delta_{LOC}, \delta_{REF})
\]

Looking at the rule region-enter-ok, the $\enter{}$ effect
adds two new locations: a new $\Root(r')$ for the region $r'$ on the region
stack, and a $\Temp(r', \iota'')$, representing the $\Cell$ holding the entry
(with $\iota''$ a fresh object id). We do not remove any graph locations. I.e.

\[
\delta_{LOC} = (\{\}, \{ \Root(r'), \Temp(r', \iota'') \} ).
\]

As for the references, looking at the rule again, we have the following:

* For each $z_i = \kw{drop}~x_i \in \many{z = \Use}$, we remove the

\[\REF_\Graph(\Root(r), x_i) = (\Root(r) \RefTo{x_i, k_i} \Loc_{x_i}) \]

and add the reference

\[\Root(r') \RefTo{z_i, k} \Loc_{x_i} \]

We also note that well-formedness of the effect and configuration,
$\REF_\Graph(\Root(r), x_i)$ is well defined, and $k_i = \Iso$.

For such an $i$, we let

\[
\delta_{REF}^i = \begin{cases}
(\{\Root(r) \RefTo{x_i, k_i} \Loc_{x_i} \}, \{ \Root(r)
\RefTo{z_i, k_i} \Loc_{x_i} \} ) & \If k_i = \iso \\
(\{\Root(r) \RefTo{x_i, k_i} \Loc_{x_i} \}, \{ \Root(r)
\RefTo{z_i, \paused \sees k_i} \Loc_{x_i} \} )& \Ow
\end{cases}
\]

* For each $z_i = x_i \in \many{z = \Use}$, if

\[\REF_\Graph(\Root(r), x_i) = (\Root(r) \RefTo{x_i, k_i} \Loc_{x_i}), \]

we add the reference

\[\Root(r') \RefTo{z_i, \VPA{\Paused}{k_i}} \Loc_{x_i}. \]

Well-formedness implies that $\REF_\Graph(\Root(r), x_i)$ and
$\VPA{\Paused}{k_i}$ is well defined.

For such an $i$, we let

\[
\delta_{REF}^i = (\emptyset, \{ \Root(r) \RefTo{z_i, k_i} \Loc_{x_i} \} ).
\]

* We finally add a reference from $\Root(r')$ to $\Temp(r', \iota'')$

\[ \Root(r') \RefTo{w, k} \Temp(r', \iota'') \]

(note that b.c. of well-formedness, $k \in \{ \Var, \Temp \}$)
and from $\Temp(r', \iota'')$ to $\Loc_f$:

\[ \Temp(r', \iota'') \RefTo{\Valfield, \Mut} \Loc_f \]

\[
\begin{array}{lcl}
\REF_\Graph(\Root(r), y) &=& (\Root(r) \RefTo{y, k_y}  \Loc_y) \\
\REF_\Graph(\Loc_y, f)   &=& (\Loc_y   \RefTo{f, \Iso} \Loc_f).
\end{array}
\]

These are well defined because of well-formedness.

We let

\[
\delta_{REF}^{\mathsf{entry}} = \left(\emptyset, \left\{(\Root(r') \RefTo{w, k}
\Temp(r', \iota'')), (\Temp(r', \iota'') \RefTo{\Valfield, \Mut}
\Loc_f) \right\} \right)
\]

From the above we conclude that

\[
\delta_{REF} = \sum_{i = 1}^{\Len(\many{z = \Use})}{\delta_{REF}^i} + \delta_{REF}^\mathsf{entry}
\]

The rule region-enter-fail has $\RCfg = \RCfg'$ and we conclude that

\[
\delta^*(\rho, \Graph, \badenter) = (\Nildelta, \Nildelta)
\]

i.e. $\delta_{LOC} = \Nildelta$ and $\delta_{REF} = \Nildelta$.

$\exit{x, \Use, y.f, z.f'}$

\[
\delta^*(r :: \rho, \Graph, \exit{x, \Use, y.f, z.f'}) = (\delta_{LOC}, \delta_{REF})
\]

We must now consider two cases: region-exit-temp and
region-exit-heap. By examining both rules, we see that the top region
frame is popped. We can thus immediately conclude that $\Root(r')$ and
$\Temp$-locations pertaining to the top region $r'$ are removed, i.e.

\[
\begin{aligned}
\delta_{LOC} = (&\{ \Root(r') \} \cupdisj \\ & \{ \Temp(r', \_) ~|~
\Temp(r', \_) \in \Graph \}, \emptyset )
\end{aligned}
\]

For references, since we remove the top region frame all outgoing references
are removed. This corresponds to:

\[
\begin{aligned}
\delta_{REF}^1 = ( &\left\{ \Root(r') \RefTo{\_, \_} \_ ~|~ \Root(r') \RefTo{\_, \_} \_ \in
\Graph  \right \} \cupdisj \\
& \left\{ \Temp(r', \_) \RefTo{\_, \_} \_ ~|~ \Temp(r', \_) \RefTo{\_, \_} \_ \in
\Graph  \right \}, \emptyset )
\end{aligned}
\]

The return value specified by $\Use$ is picked up from the frame being
popped. Assuming $\Use = w$ or $\Use = \kw{drop}~w$, this means that we add
a reference:

\[
\delta_{REF}^2 = (\emptyset, \{\Root(r) \RefTo{x, k_w} \Loc_w \})
\]

\[
\REF_\Graph(\Root(r'), w) = (\Root(r') \RefTo{w, k_w} \Loc_w)
\]

Note that $\REF_\Graph(\Root(r'), z)$ is removed as part of $\delta_{REF}^1$ above.

Lastly, we move the new entrypoint referred to by $z.f'$ in the top frame,
into $y.f$ referred to in the second top frame:

\[
\delta_{REF}^3 = (\{ \Loc_y \RefTo{f, k} \Loc_f \}, \{\Loc_y \RefTo{f,
k} \Loc_{f'} \})
\]

\[
\begin{array}{lcl}
\REF_\Graph(\Root(r), y) &=& (\Root(r) \RefTo{y, k_y} \Loc_y) \\
\REF_\Graph(\Loc_y, f)   &=& (\Loc_y \RefTo{f, k} \Loc_f)  \\
\REF_\Graph(\Root(r'), z)&=& (\Root(r') \RefTo{z, k_z} \Loc_{f'})
\end{array}
\]

In total we get:

\[
\delta_{REF} = \delta_{REF}^1 + \delta_{REF}^2 + \delta_{REF}^3
\]

Note that all of this holds for both region-exit-temp and
region-exit-heap. The only difference between the two cases is the
format of $\Loc_y$.
$\load{x, y.f}$

\[
\delta^*(r::\rho, \Graph, \load{x, y.f}) = (\delta_{LOC}, \delta_{REF})
\]

It is clear from region-load that

\[
\delta_{LOC} = \Nildelta.
\]

Furthermore, we see that the only action on references is adding a
reference from $\Root(r)$ to $\Loc_f$, the location referred to by $y.f$:

\[
\delta_{REF} = (\emptyset, \{ \Root(r) \RefTo{x, \VPA{k}{k'}} \Loc_f \})
\]

\[\begin{array}{lcl}
\REF(\Root(r), y) &=& (\Root(r)\RefTo{y, k} \Loc_y) \\
\REF(\Loc_y, f)   &=& (\Loc_y  \RefTo{f, k'}\Loc_f)
\end{array}\]

$\swap{x, y.f, \Use}$

The two rules for swap are region-swap-temp and region-swap-heap,
which are very similar. We note that $\swap{}$ has no action on the
locations of the graph:

\[
\delta^*(r::\rho, \Graph, \swap{x, y.f, \Use}) = (\Nildelta, \delta_{REF})
\]

We have $\Use = z$ or $\Use = \kw{drop}~z$. If we let

\[
\REF_\Graph(\Root(r), z) = (\Root(r) \RefTo{z, k_z} \Loc_z)
\]

we have two cases:

\[
\delta_{REF}^{\mathsf{drop}} =
\begin{cases}
(\{ \Root(r) \RefTo{z, k_z} \Loc_z \}, \emptyset) & \text{ if } \Use =
\kw{drop}~z \\
\Nildelta & \text{ otherwise}
\end{cases}
\]

The action of the actual swap on the graph is

\[
\delta_{REF}^\mathsf{switch} = (\{ \Loc_y \RefTo{f, k_y} \Loc_f \}, \{\Loc_y
\RefTo{f, k_z} \Loc_z \})
\]

In total we have

\[
\delta_{REF} = \delta_{REF}^\mathsf{drop} + \delta_{REF}^\mathsf{switch}.
\]

Because of the similarity, this holds in both region-swap-tmp and
region-swap-heap. The only difference will be the format of $\Loc_y$.

$\halloc{x, k, \#C, \many{\Use}}$

\[
\delta^*(r::\rho, \Graph, \halloc{x, \#C, k, \many{\Use}}) = (\delta_{LOC}, \delta_{REF}).
\]

By well-formedness, $k = \Mut$ or $k = \Iso$, which corresponds to the two
cases region-halloc-mut and region-halloc-iso respectively. In both cases
the set of locations will be expanded with a new heap location with fresh
object id $\iota$. Its region id will depend on $k$:

\[
r^* =
\begin{cases}
r & \text{ if } k = \Mut \\
r'  & \text{ if } k = \Iso, \text{ where } r' \text{ is fresh}
\end{cases}
\]

\[
\delta_{LOC} = (\emptyset, \{ \Heap(r^*, \iota) \})
\]

Similar to the enter case ([pf]caseenter) above, we have a sequence of $\Use$
to consider. These correspond to the fields of the new object being created.
Letting $\Fnames(C) = f_1, \dots, f_n$:

* For each $\kw{drop}~z_i \in \many{\Use}$,

\[
\REF_\Graph(\Root(r), z_i) = (\Root(r) \RefTo{z_i, k_i} \Loc_i)
\]

\[
\delta_{REF}^i = (\{ \Root(r) \RefTo{z_i, k_i} \Loc_i \},
\{ \Heap(r^*, \iota) \RefTo{f_i, k_i} \Loc_i \})
\]

* For each $z_i \in \many{\Use}$,

\[
\REF_\Graph(\Root(r), z_i) = (\Root(r) \RefTo{z_i, k_i} \Loc_i)
\]

\[
\delta_{REF}^i = (\emptyset, \{ \Heap(r^*, \iota) \RefTo{f_i, k_i} \Loc_i \})
\]

This is all well defined because of well-formedness. In total we have

\[
\delta_{REF} = (\emptyset, \{ \Root(r) \RefTo{x, k} \Heap(r^*, \iota) \}) + \sum_{i = 1}^{\Len(\many{\Use})} \delta_{REF}^i
\]

$\salloc{x, k, \CLTag, \many{\Use}}$

\[
\delta^*(r::\rho, \Graph, \salloc{x, k, C, \many{\Use}}) = (\delta_{LOC}, \delta_{REF}).
\]

By similar reasoning to [pf]casehalloc, for a fresh $\iota$

\[
\delta_{LOC} = (\emptyset, \{ \Temp(r, \iota) \})
\]

Letting $\Fnames(C) = f_1, \dots, f_n$:

* For each $\kw{drop}~z_i \in \many{\Use}$,

\[
\REF_\Graph(\Root(r), z_i) = (\Root(r) \RefTo{z_i, k_i} \Loc_i)
\]

\[
\delta_{REF}^i = (\{ \Root(r) \RefTo{z_i, k_i} \Loc_i \},
\{ \Temp(r, \iota) \RefTo{f_i, k_i} \Loc_i \})
\]

* For each $z_i \in \many{\Use}$,

\[
\REF_\Graph(\Root(r), z_i) = (\Root(r) \RefTo{z_i, k_i} \Loc_i)
\]

\[
\delta_{REF}^i = (\emptyset, \{ \Temp(r, \iota) \RefTo{f_i, k_i} \Loc_i \})
\]

In total:

\[
\delta_{REF} = (\emptyset, \{ \Root(r) \RefTo{x, k} \Temp(r, \iota) \}) + \sum_{i = 1}^{\Len(\many{\Use})} \delta_{REF}^i
\]

We note that $k \in \{ \Tmp, \Var \}$ by well-formedness.

$\freeze{x, \Use}$

By inspecting region-freeze,

\[
\delta^*(r :: rn, \Graph, \freeze{x, \Use}) = (\Nildelta, \delta_{REF})
\]

i.e. $\delta_{LOC} = \Nildelta$.

By well-formedness, $\Use = \kw{drop}~z$ and

\[
\REF_\Graph(\Root(r), z) = (\Root \RefTo{z, \Iso} \Loc_z)
\]

From rule region-freeze we have that this reference is consumed and
converted into a immutable reference:

\[
\delta_{REF} = (\{\Root(r) \RefTo{z, \Iso} \Loc_z\}, \{\Root(r) \RefTo{x,
\Imm} \Loc_z\})
\]

$\merge{x, \Use}$

\[
\delta^*(r :: rn, \Graph, \merge{x, \Use}) = (\delta_{LOC}, \delta_{REF})
\]

By well-formedness, $\Use = \kw{drop}~z$. By region-merge,

\[
\REF_\Graph(\Root(r), z) = (\Root(r) \RefTo{z, \Iso} \Heap(r', \iota'))
\]

The $\delta$s for merging a region is somewhat tricky. In the configuration
semantics, this ammounts to merging the subheap of the region $r'$ into the the
subheap of the currently active region $r$. This means that all locations
$loc[r']$ will be converted to $loc[r]$.

\[
D_{LOC} = \left\{ \Loc[r'] \Suchthat \Loc[r'] \in \Graph \right\}
\]

We write

\[
\delta_{LOC} = (D_{LOC}, D_{LOC}[r'/r])
\]

where $D_{LOC}[r'/r]$ is the set of elements of $D_{LOC}$ but with $r'$
substituted for $r$.

For references we have the analogue

\[
D_{REF} = \left\{ (\Loc_1[r_1] \RefTo{f, k} \Loc_2[r_2]) \Suchthat
(\Loc_1[r_1] \RefTo{f, k} \Loc_2[r_2]) \in \Graph \AN
(r_1 = r' \OR r_2 = r') \right\}
\]

We have

\[
\delta_{REF} = (D_{REF}, D_{REF}[r'/r])
\]

$\cast{x, \Use, k~CL}$

$\Use$ can either be $z$ or $\kw{drop}~z$. From the rule region-cast it is
obvious that

\[
\delta^*(r :: \rho, \Graph, \cast{x, \Use, k~CL}) = (\Nildelta, \delta_{REF})
\]

\[
\delta_{REF} = \delta_{REF}^\mathsf{drop} + (\emptyset, \{ \Root(r) \RefTo{x,
k_z} \Loc_z \}
\]

\[
\begin{array}{lcl}
\REF_\Graph(\Root(r), z) &=& (\Root(r) \RefTo{z, k_z} \Loc_z)\\
\delta_{REF}^\mathsf{drop} &=& \begin{cases}
(\{\Root(r) \RefTo{z, k_z} \Loc_z \},
\emptyset) & \text{ if } \Use = \kw{drop}~z
\\
\Nildelta & \text{ otherwise}
\end{cases}
\end{array}
\]

$\nocast{x, \Use, k~CL}$

By similar reasoning to [pf]casecast, using region-nocast instead:

\[
\delta^*(r :: \rho, \Graph, \nocast{x, \Use, k~CL}) = (\Nildelta, \delta_{REF})
\]

\[
\delta_{REF} = \delta_{REF}^\mathsf{drop} + (\emptyset, \{ \Root(r) \RefTo{x,
k_z} \Loc_z \}
\]

\[
\begin{array}{lcl}
\REF_\Graph(\Root(r), z) &=& (\Root(r) \RefTo{z, k_z} \Loc_z)\\
\delta_{REF}^\mathsf{drop} &=& \begin{cases}
(\{\Root(r) \RefTo{z, k_z} \Loc_z \},
\emptyset) & \text{ if } \Use = \kw{drop}~z
\\
\Nildelta & \text{ otherwise}
\end{cases}
\end{array}
\]

$\bind{\many{x = \Use}}$

Looking at rule region-bind, similarly to $\halloc{}$ and $\salloc{}$
cases ([pf]casehalloc and [pf]casesalloc), we have a sequence of
$\Use$s. Here we instead create references from $\Root(r)$. We get

\[
\delta^*(r::\rho, \Graph, \bind{\many{x = \Use}}) = (\Nildelta, \delta_{REF}).
\]

* For each $x_i = \kw{drop}~z_i \in \many{x = \Use}$,

\[
\REF_\Graph(\Root(r), z_i) = (\Root(r) \RefTo{z_i, k_i} \Loc_i)
\]

\[
\delta_{REF}^i = (\{ \Root(r) \RefTo{z_i, k_i} \Loc_i \},
\{ \Root(r) \RefTo{x_i, k_i} \Loc_i \})
\]

* For each $x_i = z_i \in \many{x = \Use}$,

\[
\REF_\Graph(\Root(r), z_i) = (\Root(r) \RefTo{z_i, k_i} \Loc_i)
\]

\[
\delta_{REF}^i = (\emptyset, \{ \Root(r) \RefTo{x_i, k_i} \Loc_i \})
\]

In total:

\[
\delta_{REF} = \sum_{i = 1}^{\Len(\many{\Use})} \delta_{REF}^i
\]