ch:capability-region-types: ch:capability-region-types

Choose outer ${\rho }_0$ and fresh local $\rho$, and annotate $$\mathsf{letregion}\rho \mathsf{in}\mathsf{let}x=1\mathsf{at}\rho \mathsf{in}2\mathsf{at}{\rho }_0\mathsf{end}\mathsf{end}.$$ The body effect is $\{\mathsf{put}(\rho ),\mathsf{put}({\rho }_0)\}$. The result is an integer at ${\rho }_0$, and the empty initial $\mathit{TE}$ does not mention $\rho$. Those are RI-Letregion’s freshness facts. The rule removes the local put effect, leaving $\{\mathsf{put}({\rho }_0)\}$; it has no continuation-effect premise.

Deleting the outer ${\pi }_0$ from $e_{\mathsf{pairFirst}}$ returns the allocated pair, whose result type is $⟨\mathsf{int},\mathsf{int}⟩\mathsf{at}\rho$. Hence $\rho \in \mathrm{ftv}(\tau )$, violating R-Letregion. Without that premise, evaluation could remove $\rho$ and return an address into it.

Initially $M=\mathrm{\Psi }=\{\}$ and $C=\varnothing$. A fresh-region step chooses $\nu$, yielding $M(\nu )=\{\}$, $\mathrm{\Psi }(\nu )=\{\}$, and $C=\{{\nu }^1\}$. Pair allocation adds a fresh label $\ell$ with tuple type to $\mathrm{\Psi }(\nu )$, but retains the unique capability. Projection uses the tuple entry and authority for $\nu$. Deallocation consumes $\{{\nu }^1\}$ and removes $\nu$ from $M$ and $\mathrm{\Psi }$, returning $C$ to empty. A later projection cannot establish either the location typing $\nu .\ell :\tau$ or capability satisfiability for $\nu$.

Take a well-typed terminating run and its terminal state. Preservation keeps the terminal state well typed. Progress says a terminal expression is $\mathsf{halt}v$ for a word value $v:\mathsf{int}$. Cap-Halt requires its current capability equal to $\varnothing$. Capability cardinality preservation ensures that equality cannot erase a unique occurrence of a live region. Satisfiability then implies that the memory typing has no live region names. Canonical memory typing says a concrete memory realizing the empty memory typing is itself empty. Hence the terminal state is $(\{\},\mathsf{halt}v)$.

Write the body of $e_{\mathsf{pairFirst}}$ as $e$, the outer meta-level continuation as $k=⟨x_k;e_k⟩$, and the body’s result parameter as $x^{\prime }$. The essential target shape is $$\mathsf{let}\mathsf{newrgn}\rho ,x_{\rho }\mathsf{in}\mathsf{CPS}(e;⟨x^{\prime };\mathsf{let}\mathsf{freergn}{x}_{\rho }\mathsf{in}\mathsf{apply}(k,x^{\prime })⟩).$$ Immediately after $\mathsf{newrgn}$, the translation environment’s current capability and bound contain $\{{\rho }^1\}$. The body effect translates to an absorbable capability under that bound. The continuation receives the body’s value while unique $\rho$ is still available, consumes it at $\mathsf{freergn}$, and invokes $k$ under the old bound. The displayed equation with $\mathsf{CapOf}(\psi )$ remains true after deleting the discharged singleton; the fresh-region premise prevents $k$’s type or capability from mentioning $\rho$.

L${}^3$ allocation returns an existential package containing $\mathsf{Cap}\rho \mathsf{int}$ and a duplicable pointer. Its swap step replaces that capability by $\mathsf{Cap}\rho (\mathsf{int}\times \mathsf{int})$ and returns the old integer; free consumes the repackaged capability and pointer. This is the card that owns strong update. Linear-region allocation extends $\psi$ and returns a linear capability plus unrestricted handle; accesses thread the capability and $\mathsf{freergn}$ consumes it, as covered by target safety. Monadic $\mathsf{runRGN}$ pushes an empty region stack, allocates and reads within it, discards it, and returns $7$. Its rank-2 result type cannot mention the fresh region, so this card owns lifetime hiding. None of the latter two claims imports L${}^3$’s strong-update theorem.