This document is a technical report accompanying a paper by the same title and authors, published at POPL 2019.
It contains proofs and details that were omitted from the paper for space and presentation reasons.

Disclaimer: While the proofs in this technical report are done, the text can be lacklustre and from time to time out of date.
We will make the technical report up to date as soon as possible.
Further, the use of coloring in the later parts of this document has not always been done with as much care as it ought to. This means that not all source specific things are colored blue, but it should be evident from the context that they belong to the source language.

§ THE TWO CAPABILITY MACHINES

§.§ Domains

\[
\begin{array}{rrcl}
\addrbnf,\basebnf \in & \Addr & \defeq & \nats \\
\sealbasebnf, \sigma \in & \Seal & \defeq & \nats \\
w \in &\Word & \defeq & \ints \uplus \Caps\\
\permbnf \in& \Perm & \defbnf & \dots \\
&\linbnf & \defbnf & \linear \mid \normal \\
&\aendbnf & \in & \Addr \uplus \{\infty \} \\
&\sealendbnf & \in & \Seal \uplus \{\infty \} \\
\scbnf \in &\SealableCaps&\defbnf & ((\permbnf,\linbnf),\basebnf,\aendbnf,\addrbnf) \mid \seal{\sealbasebnf,\sealendbnf,\sigma}\\
& & & {\sourcecolor{} \mid \stkptr{\permbnf,\basebnf,\aendbnf,\addrbnf}}\\
& & & {\sourcecolor{} \; \mid \retptrd(\basebnf,\aendbnf) \mid \retptrc(\basebnf,\aendbnf,\addrbnf)}\\
\cbnf \in&\Caps& \defbnf &  \scbnf \mid \sealed{\sigma,\scbnf}\\
\rbnf \in & \RegName & \defbnf &\pcreg \mid \rretd \mid \rretc \mid \rstk \mid \rdata \mid \rtmp{1} \mid \rtmp{2} \mid \dots \\
&\Reg & \defeq & \RegName \fun \Word\\
&\Mem & \defeq & \Addr \fun \Word \\
&\MemSeg & \defeq & \Addr \parfun \Word \\
{\sourcecolor \sstkframe \in} & {\sourcecolor \StkFrame} & {\sourcecolor \defeq} & {\sourcecolor \Addr \times \MemSeg}\\
\src{\sstk \in}& \src{ \Stack} & \src{ \defeq} & \src{ \StkFrame^*} \\
\Phi \in & \ExecConf & \defeq & \Mem \times \Reg {\sourcecolor{} \; \times \; \Stack \times \MemSeg }\\
&\Conf & \defeq & \ExecConf \uplus \{\failed\} \uplus \{\halted\}
\end{array}
\]

The target language domains are all the non blue parts in the above. The source language domains are the black and blue parts in the above. Further

* $\linbnf$ defines domain $\Linear$

* $\scbnf$ defines domain $\SealableCaps$

* $\cbnf$ defines domain $\Caps$

* $\rbnf$ defines the finite set $\RegName$.

* $\Perm$ is defined as the set of permissions in Figure <ref>.

In the source language, $\src{\Stack}$ is a call stack that contains the data for each call. The call stack consists of a number of $\src{\StkFrame}$'s that contains 1) the old pc and 2) caller's private stack.

In both languages, the base address of the stack is known (the stack grows downwards in memory, so the base address marks the end of the stack). In the target language, this will be the base address of some linear capability. The base address can be any address on the machine, but it will have to remain the same during all of execution. We write this constant as

\[
\stkb
\]

§.§.§ Useful definitions

For a capability $c=((\_,\_),\baddr,\eaddr,\_)$ we say it has range $[\baddr,\eaddr]$ and we define

\[
\range{c} = [\baddr,\eaddr]
\]

Similarly for seals and stack pointers:

\[
\range{\seal{\sigma_\baddr,\sigma_\eaddr,\_}} = [\sigma_\baddr,\sigma_\eaddr]
\]

\[
\src{\range{\stkptr{\_,\baddr,\eaddr,\_}} = [\baddr,\eaddr]}
\]

§.§ Syntax

The target machine is a simple capability machine with memory capabilities and sealed capabilities[In previous work, we used enter capabilities but for this the complexity introduced by mixing writable and executable memory is difficult to handle.] (inspired by CHERI). The syntax of the instructions of the target machine is defined as follows:

\[
\begin{array}{rcl}
n &\in & \ints \\
\com{r} &\in &  \tRegName \\
\com{\rn} &\defbnf &  \com{r} \mid n \\
\com{i} &\defbnf & \tfail \mid \thalt \mid \tjmp{\com{r}} \mid \tjnz{\com{r}}{\com{\rn}} \mid \tisptr{\com{r}}{\com{r}} \mid \tgeta{\com{r}}{\com{r}} \mid \tgetb{\com{r}}{\com{r}} \mid \\
& &  \tgete{\com{r}}{\com{r}}\mid \tgetp{\com{r}}{\com{r}} \mid \tgetlin{\com{r}}{\com{r}} \mid \tmove{\com{r}}{\com{\rn}} \mid \tstore{\com{r}}{\com{r}} \mid\\
& &  \tload{\com{r}}{\com{r}} \mid \tcca{\com{r}}{\com{\rn}} \mid \trestrict{\com{r}}{\com{\rn}} \mid \tlt{\com{r}}{\com{\rn}}{\com{\rn}} \mid \\
& & \tplus{\com{r}}{\com{\rn}}{\com{\rn}} \mid \tminus{\com{r}}{\com{\rn}}{\com{\rn}} \mid \tsetatob{\com{r}} \mid \txjmp{\com{r}}{\com{r}} \mid \tcseal{\com{r}}{\com{r}} \mid \\
& &   \tsplit{\com{r}}{\com{r}}{\com{r}}{\com{\rn}} \mid\tsplice{\com{r}}{\com{r}}{\com{r}}
\end{array}
\]

$i$ defines the set $\Instr$

The source machine is also a capability machine with memory capabilities and sealed capabilities. Unlike the target machine, the source machine has a built in stack along with special stack and return tokens used in place of the actual capabilities. The syntax of the source machine language is as follows:

\[
\begin{array}{rcl}
\offpc,\offsigma & \in & \nats \\
\src{i} & \defbnf &  \com{i} \mid \scall{\offpc,\offsigma}{r}{r}
\end{array}
\]

There is one syntactic difference between the source language and the target language, namely the target language has an extra instruction in the $\scall{\offpc,\offsigma}{}{}$ instruction (the $o$ refers to the seal it uses, namely the offset in the seals made available by linking).

The source machine allows for variable length instructions which we utilise for $\scall{\offpc,\offsigma}{}{}$. In other words, when $\scall{\offpc,\offsigma}{}{}$ is decoded, a series of addresses in memory must contain what corresponds to the call instruction (and be within the range of the pc capability). This is described in more detail when we present the decoding function.

§.§ Permissions

[main node/.style=]
[main node] (rwx) $\rwx$;
[main node] (rx) [below right of=rwx] $\rx$;

[main node] (rw) [below left of=rwx,] $\rw$;
[main node] (r) [below right of=rw] $\readonly$;
[main node] (0) [below of=r] $\noperm$;

[every node/.style=font=]

(rw) edge (r)
(r) edge (0)

(rwx) edge (rx)

(rw) edge (rwx)
(r) edge (rx);

Permission hierarchy

13-09-2017: Note that most of the discussion below is now captured in Section <ref>
01-09-2017: For now, I will add the linear capabilities such that a linear capability stays linear. It does, however, seem like it would be okay to have linear capabilities become non-linear (I at least don't see anything that would break down completely). One draw back would be that one could “ruin” the stack capability by making it non-linear.
7-9-2017: Err... you mean that we could allow non-linear capabilities to be made linear, right?  We definitely do not want to allow the stack or return capability to be made non-linear, as we want to prevent it from being aliased.
07-09-2017: I actually did mean linear to non-linear (non-linear to linear does not make sense because the non-linear capability may have aliases). The operation that makes a linear capability non-linear would have to clear said capability. If a linear capability has been made non-linear, then someone who expects a linear capability can observe this difference and behave accordingly, i.e., fail the execution. It will, however, remain an invariant that there are no aliases for linear capabilities.
07-09-2017: I had forgotten that return capabilities probably need to be linear. This would call for a “load from offset” operation to be able to load an in code stored seal (see the figure I drew about linking/seals).

We assume functions $\decPerm{}$ and $\encPerm{}$.
15-09-2017: TODO, write more about these. Should be like in the local cap setting.

§.§ Operational Semantics

The source machine is parameterized with a set of trusted addresses $\ta$. $\ta$ are the only addresses from which the $\scall{}{}{}$ will be interpreted. The source machine represents a virtual intermediate machine which we use to argue well-bracketedness and local state encapsulation. It is not meant to be the machine that the actual code is executed on. Further, it is the well-bracketedness and local state encapsulation of the compiled code, not the context we are concerned with. On the other hand, the target machine is not parameterized with $\ta$ as all the instructions on the target machine is available to the adversary.

§.§.§ Notes

* Linear capabilities are cleared when they move around in memory.

Source language:

* Variable length instructions that match the length of the compiled instructions

* This is needed for correctness.

* It is only used for the call instruction.

27-09-2017: I think we need to do something about tail calls in the source language?
27-09-2017: In what sense? Do you want to allow them (I do not think they are allowed at the moment?)
8-11-2017: Yes, I would like to support them.  I think it would be a strength of our calling convention that we can support them (as I expect we can) and it would be good to demonstrate this.

Target language:

§.§.§ Helpful functions, sets, and conventions

\[
\pi_\baddr(\vsc) =
\begin{cases}
\baddr & \text{if $\vsc = ((\_,\_),\baddr,\_,\_)$} \\
\pi_\baddr(c) & \text{if $\vsc = \sealed{\_,c}$} \\
\src{\baddr} & \src{\text{if $\vsc = \stkptr{\_,\baddr,\_,\_}$}} \\
\src{\baddr} & \src{\text{if $\vsc = \retptrd(\baddr,\_)$}} \\
\src{\baddr} & \src{\text{if $\vsc = \retptrc(\baddr,\_,\_)$}}
\end{cases}
\]

\[
\pi_\eaddr(\vsc) =
\begin{cases}
\eaddr & \text{if $\vsc = ((\_,\_),\_,\eaddr,\_)$} \\
\pi_\eaddr(c) & \text{if $\vsc = \sealed{\_,c}$} \\
\src{\eaddr} & \src{\text{if $\vsc = \stkptr{\_,\_,\eaddr,\_}$}} \\
\src{\eaddr} & \src{\text{if $\vsc = \retptrd(\_,\eaddr)$}} \\
\src{\eaddr} & \src{\text{if $\vsc = \retptrc(\_,\eaddr,\_)$}}
\end{cases}
\]

\[
\pi_\lin(\vsc) =
\begin{cases}
\lin & \text{if $\vsc = ((\_,\_),\_,\eaddr,\_)$} \\
\pi_\lin(c) & \text{if $\vsc = \sealed{\_,c}$} \\
\src{\linear} & \src{\text{if $\vsc = \stkptr{\_,\_,\eaddr,\_}$}} \\
\src{\linear} & \src{\text{if $\vsc = \retptrd(\_,\_)$}} \\
\src{\normal} & \src{\text{if $\vsc = \retptrc(\_,\_,\_)$}}
\end{cases}
\]

4-12-2017: what about $\pi_a$?
12-12-2017: I have added them as I needed them in the LR. I have not needed $\pi_a$ yet.

\[
\updPcAddr{\Phi} \defeq
\begin{cases}
\Phi\update{\pcreg}{((\perm,\lin),\baddr,\eaddr,\aaddr+1)} & \text{if $\Phi(\pcreg) = ((\perm,\lin),\baddr,\eaddr,\aaddr)$}\\
\failed & \totherwise
\end{cases}
\]

\[
\readAllowed{} \defeq \{ \rwx,\rw,\rx,\ro \}
\]

\[
\writeAllowed{} \defeq \{ \rwx, \rw \}
\]

\[
\isLinear{c} \defeq
\begin{cases}
\top &
\arraycolsep=0pt
\begin{array}[t]{l}
c = ((\_,\linear),\_,\_,\_) \tor\\
c = \sealed{\_,\cb'} \tand \isLinear{\cb'}
\end{array}\\
\src{\top} &
\sourcecolor\left.
\arraycolsep=0pt
\begin{array}[t]{l}
c = \stkptr{\_,\_,\_,\_}\\
c = \retptrd(\_,\_)\\
\end{array}\right.\\
\bot & \totherwise
\end{cases}
\]

We now define

\[
\nonLinear{\cb} \defeq \neg \isLinear{\cb}
\]

\[
\linCons{w} \defeq
\begin{cases}
0 & \isLinear{w} \\
w & \totherwise
\end{cases}
\]

\[
\linConsPerm{\perm}{w} \defeq
\begin{cases}
\perm \in \writeAllowed{} & \isLinear{w} \\
\mathrm{true} & \totherwise
\end{cases}
\]

\[
\exec{\cb} \defeq
\cb = ((\perm, \_), \_, \_, \_) \tand \perm \in \{\rwx,\rx\}
\]

\[
\nonExec{\cb} \defeq \neg \exec{\cb}
\]

\[
\withinBounds{\vsc} \defeq
\begin{cases}
\baddr \leq \aaddr \leq \eaddr &
\arraycolsep=0pt
\begin{array}[t]{l}
\vsc = ((\_,\_),\baddr,\eaddr,\aaddr) \src{\tor}\\
\src{\vsc = \stkptr{\_,\baddr,\eaddr,\aaddr}}
\end{array}\\
\sigma_\baddr \leq \sigma_\aaddr \leq \sigma_\eaddr & \vsc = \seal{\sigma_\baddr,\sigma_\eaddr,\sigma} \\
\bot & \totherwise
\end{cases}
\]

\[
\nonZero{w} \defeq
\begin{cases}
\bot & w \in \ints \tand w = 0 \\
\top & \totherwise
\end{cases}
\]

For convenience, we introduce the following notation:

\[
\begin{array}{rcl}
\Phi(r) & \defeq & \Phi.\reg(r)
\end{array}
\]

where $r\in \RegName$.

For $\rn$ which can be a register or an integer, we take

\[
\Phi(\rn) = n
\]

to mean

\[
\text{either $n = \rn$ or $n = \Phi.\reg(\rn)$ and in either case $n \in \ints$}
\]

§.§.§ Step relations

Decode and encode functions
We assume functions $\decInstr{} : \Word \fun \Instr$ and $\encInstr{} : \Instr \fun \ints$ where $\Instr$ is the set of target level instructions.

The $\decInstr{}$ function must be surjective and injective for all non-$\tfail$ instructions.
For any $c \in \Caps$, we have that $\decInstr{c} = \tfail$.
The $\encInstr{}$ function must be injective.
Further $\decInstr{}$ must be the left inverse of $\encInstr{}$ that is for all $i \in \Instr$

\[
\decInstr{}(\encInstr{i}) = i
\]

These functions are used for both the target and source level machine. When we write instructions in places where words are required, we will assume that $\encInstr{}$ is implicit.

Step relation
The instruction $\scall{\offpc,\offsigma}{}{}$ has length $\calllen$ which means that it does not fit in one memory address. In fact, $\scall{\offpc,\offsigma}{}{}$ should be seen as a different way of interpreting a series of instruction rather than an instruction on its own. We therefore introduce $\scall[0]{\offpc,\offsigma}{r_1}{r_2},\dots,\scall[\calllen-1]{\offpc,\offsigma}{r_1}{r_2}$ as aliases for the instructions that constitute $\scall{\offpc,\offsigma}{r_1}{r_2}$ (see Paragraph <ref> for details). We define the following condition that indicates that $\aaddr$ is the first address of a $\scall{\offpc,\offsigma}{r_1}{r_2}$ instruction in the configuration $\Phi$:

\[
\sourcecolor\left.
\callCond{\Phi,r_1,r_2,\offpc,\offsigma,\aaddr} = \left\{
\begin{array}{l}
\Phi.\mem(\aaddr) = \scall[0]{\offpc,\offsigma}{r_1}{r_2} \tand\\
\vdots \\
\Phi.\mem(\addr+\calllen-1) = \scall[\calllen-1]{\offpc,\offsigma}{r_1}{r_2}
\end{array}
\right.
\right.
\]

We use the following step relation:
RESOLVED: Add $\ta$ to the source step.
RESOLVED: Add $\stkb$ to source term and everything else where it is necessary. Consider how $\stkb$ and $\ta$ can be added without passing around these values in LR and source semantics (solution to parameterize both with it, so they need to be provided only once.)

\begin{align*}
\src{\Phi} & \; \src{\step[\src{\ta,\stkb}] \sem{\scall{\offpc,\offsigma}{r_1}{r_2}}(\Phi)} &  &\sourcecolor\left.\arraycolsep=0pt
\begin{array}[t]{l}
\text{if }\Phi(\pcreg)
= ((\perm,\_),\baddr,\eaddr,\aaddr) \tand \\
\callCond{\Phi,r_1,r_2,\offpc,\offsigma,\aaddr} \tand\\
\lbrack \aaddr ,\aaddr + \calllen - 1\rbrack \subseteq \ta \tand \\
\lbrack\aaddr,\aaddr + \calllen-1\rbrack \subseteq [\baddr,\eaddr] \tand \\
\exec{\Phi(\pcreg)}
\end{array}\right.\\
\Phi & \step[\src{\ta,\stkb}] \sem{\decInstr{\Phi.\mem(\aaddr)}}(\Phi) & &\left.\arraycolsep=0pt
\begin{array}[t]{l}
\text{if }\Phi(\pcreg) = ((\perm,\_),\baddr,\eaddr,\aaddr) \tand \\
\src{(\neg\callCond{\Phi,r_1,r_2,\offpc,\offsigma,\aaddr} \tor}\\
\src{\eaddr < \aaddr + \calllen-1) \tand} \\
\withinBounds{\Phi(\pcreg)} \tand \\
\exec{\Phi(\pcreg)}
\end{array}\right.\\
\Phi& \step[\src{\ta,\stkb}] \failed & & \totherwise
\end{align*}

On the source machine, the instruction interpretation also takes $\gc$, the global constants.
It does, however, just pass it around and never makes changes to it, so we will leave it implicit.

Note: The above does not allow executing code that is on the stack in the source machine, while this is in principle allowed in the target.
This is probably fine if we make sure a stack pointer can never be executable.

Terminating computations
We use the following notation to write that a configuration $\Phi$ successfully terminates:

\[
\Phi\sterm[i]{\src{\ta,\stkb}} \defeq \Phi \nstep[i]{\src{\ta,\stkb}} \halted
\]

if we just know $\Phi$ terminates in some number of steps, then we write

\[
\Phi\sterm{\src{\ta,\stkb}} \defeq \exists i \ldotp \sterm[i]{\src{\ta,\stkb}}
\]

Call implementation

This paragraph contains the implementation of $\scall{\offpc,\offsigma}{}{}$. That is each of the instructions in the implementation corresponds to $\scall[1]{\offpc,\offsigma}{r_1}{r_2} \dots \scall[\calllen-1]{\offpc,\offsigma}{r_1}{r_2}$, respectively.

16-10-2017: Implementation of $\scall{\offpc,\offsigma}{}{}$ may need registers for temporary registers - we should update the semantics accordingly.

\[
\begin{array}{l}
\text{// push 42 on the stack (so it is non-empty).}\\
\tmove{\rtmp{1}}{42}\\
\tstore{\rstk}{\rtmp{1}}\\
\tcca{\rstk}{(-1)}\\
\text{// split the stack at its current address - rstk done.}\\
\tgeta{\rtmp{1}}{\rstk}\\
\tsplit{\rstk}{\rretd}{\rstk}{\rtmp{1}}\\
\text{// load the seal for the return pointer through the pc capability.}\\
\tmove{\rtmp{1}}{\pcreg}\\
\tcca{\rtmp{1}}{(\offpc - 5)} \text{ // $\offpc$ is the offset from pc to the location of the seal for this code. \footnote{-5 is the offset from the previous instruction where the $\pcreg$ was moved to $\rtmp{1}$ to the first instruction of the call implementation.}}\\
\tload{\rtmp{1}}{\rtmp{1}}\\
\tcca{\rtmp{1}}{\offsigma}\text{ // $\offsigma$ is the offset for the seal used by this call.}\\
\text{// seal the used stack frame as the data part of the return pointer pair.}\\
\tcseal{\rretd}{\rtmp{1}}\\
\text{// obtain the code part of the return pointer pair and seal it too.}\\
\tmove{\rretc}{\pcreg}\\
\tcca{\rretc}{5} \text{ //magic number is offset to return code}\\
\tcseal{\rretc}{\rtmp{1}}\\
\text{// now clear temporary register and jump to the adversary.}\\
\tmove{\rtmp{1}}{0}\\
\txjmp{r_1}{r_2}\\

\text{// the following is the return code}\\
\text{// check that the stack pointer is the same we handed out.}\\
\tgetb{\rtmp{1}}{\rstk}\\
\tminus{\rtmp{1}}{\rtmp{1}}{\stkb} \text{ //$\stkb$ is the stack base constant} \\
\tmove{\rtmp{2}}{\pcreg}\\
\tcca{\rtmp{2}}{5} \text{ //magic number is the offset to fail} \\
\tjnz{\rtmp{2}}{\rtmp{1}} \\
\tcca{\rtmp{2}}{1} \text{ //magic number is the offset to after fail} \\
\tjmp{\rtmp{2}} \\
\tfail \\
\text{// join our stored private stack frame with the rest of the stack (this also finishes the stack pointer check).}\\
\tsplice{\rstk}{\rstk}{\rdata} \\
\text{// pop the magic number 42}\\
\tcca{\rstk}{1}\\
\text{// clear temporary registers used}\\
\tmove{\rtmp{2}}{0}\\
\text{// continue program after invocation.}
\end{array}
\]

Return code could be simplified if we had jz in addition to jnz.

The call code does the following:

* Store 42 (it could be anything) to the stack (this ensures the stack is non-empty), and decrement the pointer according to convention.

* Get the current address of the stack pointer and split according to it.

* Retrieve the seal of the program.

* cca the seal, so the seal to be used is active

* seal our private part of the stack capability.

* Move the pc out of the pc register, adjust it to point to the first address of the return code, and seal it.

* clear the temporary register.

* cross jump to the two specified registers.

* Upon return:

* get the base of the stack and check that it matches up with the global base of the stack.If not, fail.

* splice the returned stack pointer and the stack pointer for our private stack.

* adjust stack pointer to first empty address (the address with the end address is considered free)

* clear the temporary registers. (Note that $\rtmp{1}$ is not cleared with 0 as it already contains 0 after the $\stkb$ check. If it didn't contain 0, then the execution would have failed.)

For convenience, we will add the convention that the memory update $\update{\mem.a}{\scall{\offpc,\offsigma}{r_1}{r_2}}$ corresponds to

\[
\begin{array}{l}
\update{\mem.a}{\scall[0]{\offpc,\offsigma}{r_1}{r_2}}\\
\update{\mem.a+1}{\scall[1]{\offpc,\offsigma}{r_1}{r_2}}\\
\dots\\
\update{\mem.a+\calllen-1}{\scall[\calllen-1]{\offpc,\offsigma}{r_1}{r_2}}\\
\end{array}
\]

§.§.§ Instruction Interpretation

We have unified the two languages in the below definitions. Everything written in black is common for both source and target language. Everything written in blue is specific to the source language.

fail and halt

\begin{align*}
\sem{\tfail}(\Phi) = & \; \failed \\
\sem{\thalt}(\Phi) = & \; \halted
\end{align*}

jmp and jnz

\begin{align*}
\sem{\tjmp{r}}(\Phi) = &
\begin{cases}
\Phi\updReg{r}{w}\updReg{\pcreg}{\Phi(r)} & w = \linCons{\Phi(r)}
\end{cases}
\end{align*}

\begin{align*}
\sem{\tjnz{r}{\rn}}(\Phi) = &
\begin{cases}
\arraycolsep=0pt
\begin{array}[t]{rl}
\Phi&\updReg{r}{w}\\
\end{array}
& w = \linCons{\Phi(r)} \tand \nonZero{\Phi(\rn)}\\
\updPcAddr{\Phi} & \totherwise
\end{cases}
\end{align*}

In the definitions of the semantics below, we use a function $\encType{} : \Word \rightarrow \ints$. This is an encoding function for which the specific implementation does not matter. As the words of the two machines differ, we really need two functions which we call $\encType{}_{\var{src}}$ and $\encType{}_{\var{trg}}$. These two functions need to be related in the following way:

* $\encType{}(((\_,\_),\_,\_,\_))$, $\encType{}(\seal{\_,\_,\_})$, $\encType{}(\sealed{\_,\_})$, and $\encType{}(i)$ where $i\in\ints$ are all distinct.

* For all $w \in \SealableCaps$ (only the words on the target machine), $\encType{}_{\var{trg}}(w) = \encType{}_{\var{src}}(w)$.

* Finally,

\[
\encType{}_{\var{src}}(\src{\stkptr{\_,\_,\_,\_}}) = \encType{}_{\var{trg}}(((\_,\_),\_,\_,\_))
\]

\[
\encType{}_{\var{src}}(\src{\retptrd(\_,\_)}) = \encType{}_{\var{src}}(\src{\retptrc(\_,\_,\_)}) = \encType{}_{\var{trg}}(((\_,\_),\_,\_,\_))
\]

In English this means that each type of word is represented by a distinct value and that the tokens on the source machine has the type of the capability they represent on the target machine.

\begin{align*}
\sem{\tisptr{r_1}{r_2}}(\Phi) = & \; \updPcAddr{}(\Phi\updReg{r_1}{\encType{\Phi(r_2)}})
\end{align*}

geta, getb, gete, getp, and getl

We assume functions to encode and decode permissions as well as a function to encode linearity. The functions are used implicitly when a permission or linearity is used in a place where they need to be a word.

Specifically for the permission function, $\encPerm{} : \Perm \fun \ints$ and $\decPerm{} : \ints \fun \Perm $ encodes and decodes permissions, respectively. Where $\decPerm{}$ is the left inverse of $\encPerm{}$, $\encPerm{}$ is injective and for all $\perm \in \Perm$ $\encPerm{\perm} \neq -1$ (as this is used as an error value). $\decPerm{}$ is surjective.

For the linearity encoding, we make similar assumptions: $\encLin{} : \Linear \fun \ints$ encodes linearity. $\encLin{}$ is injective and for all $\lin \in \Linear$ $\encPerm{\lin} \neq -1$ (as this is used as an error value). As a capabilities linearity stays the same, we do not need a decoding function for linearity.

\begin{align*}
\sem{\tgeta{r_1}{r_2}}(\Phi) = &
\begin{cases}
\updPcAddr{\Phi\updReg{r_1}{\aaddr}} &
\arraycolsep=0pt
\begin{array}[t]{l}
\Phi(r_2) = ((\_,\_),\_,\_,\aaddr) \\
\quad \tor \Phi(r_2) = \seal{\_,\_,\aaddr} \\
\quad \src{\tor \Phi(r_2) = \stkptr{\_,\_,\_,\aaddr} } \\
\end{array} \\
\updPcAddr{\Phi\updReg{r_1}{-1}} & \totherwise
\end{cases}
\end{align*}

\begin{align*}
\sem{\tgetb{r_1}{r_2}}(\Phi) = &
\begin{cases}
\updPcAddr{\Phi\updReg{r_1}{\baddr}} &
\arraycolsep=0pt
\begin{array}[t]{l}
\Phi(r_2) = ((\_,\_),\baddr,\_,\_) \\
\quad \tor \Phi(r_2) = \seal{\baddr,\_,\_} \\
\quad \src{\tor \Phi(r_2) = \stkptr{\_,\baddr,\_,\_} } \\
\end{array} \\
\updPcAddr{\Phi\updReg{r_1}{-1}} & \totherwise
\end{cases}
\end{align*}

\begin{align*}
\sem{\tgete{r_1}{r_2}}(\Phi) = &
\begin{cases}
\updPcAddr{\Phi\updReg{r_1}{\eaddr}} &
\arraycolsep=0pt
\begin{array}[t]{l}
\Phi(r_2) = ((\_,\_),\_,\eaddr,\_) \\
\quad \tor \Phi(r_2) = \seal{\_,\eaddr,\_} \\
\quad \src{\tor \Phi(r_2) = \stkptr{\_,\_,\eaddr,\_} } \\
\end{array} \\
\updPcAddr{\Phi\updReg{r_1}{-1}} & \totherwise
\end{cases}
\end{align*}

15-09-2017: Should gete and getb do something for seals?
4-12-2017: doesn't matter, I think.

\begin{align*}
\sem{\tgetp{r_1}{r_2}}(\Phi) = &
\begin{cases}
\updPcAddr{\Phi\updReg{r_1}{\perm}} &
\arraycolsep=0pt
\begin{array}[t]{l}
\Phi(r_2) = ((\perm,\_),\_,\_,\_) \\
\quad \src{\tor \Phi(r_2) = \stkptr{\perm,\_,\_,\_} } \\
\end{array} \\
\updPcAddr{\Phi\updReg{r_1}{-1}} & \totherwise
\end{cases}
\end{align*}

\begin{align*}
\sem{\tgetlin{r_1}{r_2}}(\Phi) = &
\begin{cases}
\updPcAddr{\Phi\updReg{r_1}{\linear}} &
\arraycolsep=0pt
\begin{array}[t]{l}
\isLinear{\Phi(r_2)}
\end{array} \\
\updPcAddr{\Phi\updReg{r_1}{\normal}} & \nonLinear{\Phi(r_2)}
\end{cases}
\end{align*}

19-12-2017: Resolved the comments below. Seals are all normal and we allow linearity of sealed capabilities to be retrieved as it is observable anyway.
15-09-2017: Should getl do something for seals?
4-12-2017: doesn't matter, I think.
15-09-2017: Do we want to allow getl and getp to work on sealed capabilities?
Linearity of sealed caps is already observable anyway, so no point in hiding it.  Permissions of the sealed capability should be hidden, I think, mostly out of conservativity (hide as much as possible!).

4-12-2017: Couldn't the definitions above use $\pi_b$, $\pi_e$, $\pi_l$ and $\pi_a$ and $\pi_p$ (the latter two to be added) ?
12-12-2017: $\pi_\_$ also projects from sealed capabilities, so the case of sealed capabilities would have to be explicitly excluded (with getl as the exception).

\begin{align*}
\sem{\tmove{r}{\rn}}(\Phi) = &
\begin{cases}
\updPcAddr{\Phi\updReg{r}{\rn}} & r \neq \pcreg \wedge \rn \in \ints \\
\updPcAddr{\Phi\updReg{\rn}{w}\updReg{r}{\Phi(\rn)}} & r \neq \pcreg \wedge w = \linCons{\Phi(\rn)}\\
\failed & \totherwise
\end{cases}
\end{align*}

(Notice that in the case where we are moving a linear capability and $r = \rn$ the order of the updates matter.)

\begin{align*}
\sem{\tstore{r_1}{r_2}}(\Phi) = &
\begin{cases}
\updPcAddr{}\left(
\arraycolsep=0pt
\begin{array}{rl}
\Phi&\updReg{r_2}{w_2}\\
\end{array}
\right) &
\arraycolsep=0pt
\begin{array}[t]{l}
\Phi(r_1) = ((\perm,\lin),\baddr,\eaddr,\aaddr) \tand \\
\perm \in \writeAllowed{} \tand\\
\withinBounds{\Phi(r_1)} \tand \\
w_2 = \linCons{\Phi(r_2)} \tand r_2 \neq \pcreg\\
\src{\aaddr \in \dom(\Phi.\mem)}
\end{array}
\\
\sourcecolor\left.
\updPcAddr{}\left(
\arraycolsep=0pt
\begin{array}{rl}
\Phi&\updReg{r_2}{w_2}\\
\end{array}
\right) \right.&
\sourcecolor\left.
\arraycolsep=0pt
\begin{array}[t]{l}
\Phi(r_1) = \stkptr{\perm,\baddr,\eaddr,\aaddr} \tand \\
\perm \in \writeAllowed{} \tand \\
\withinBounds{\Phi(r_1)} \tand \\
\aaddr \in \dom(\Phi.\ms_\stk) \tand \\
w_2 = \linCons{\Phi(r_2)} \tand r_2 \neq \pcreg
\end{array}\right.\\
\failed & \totherwise
\end{cases}
\end{align*}

\begin{align*}
\sem{\tload{r_1}{r_2}}(\Phi) = &
\begin{cases}
\updPcAddr{}\left(
\arraycolsep=0pt
\begin{array}{rl}
\Phi&\update{\mem.a}{w_2}\\
\end{array}\right)&
\arraycolsep=0pt
\begin{array}[t]{l}
\Phi(r_2) = ((\perm,\lin),\baddr,\eaddr,\aaddr) \tand \\
\perm \in \readAllowed{} \tand\\
\withinBounds{\Phi(r_2)} \tand \\
w = \Phi.\mem(a) \tand r_1 \neq \pcreg \tand \\
w_2 = \linCons{w} \tand
\linConsPerm{\perm}{w}
\end{array}
\\
\sourcecolor\left.
\updPcAddr{}\left(
\arraycolsep=0pt
\begin{array}{rl}
\Phi& \update{\ms_\stk.a}{w_2}\\
\end{array}\right)\right.
\sourcecolor\left.
\arraycolsep=0pt
\begin{array}[t]{l}
\Phi(r_2) = \stkptr{\perm,\baddr,\eaddr,\aaddr} \tand \\
\perm \in \readAllowed{} \tand \\
\withinBounds{\Phi(r_2)} \tand \\
\aaddr \in \dom(\Phi.\ms_\stk) \tand \\ % Lau: this condition seems odd as there should never be a capability for a piece of memory that is unreachable.
w = \Phi.\ms_\stk(a) \tand r_1 \neq \pcreg \tand \\
w_2 = \linCons{w} \tand
\linConsPerm{\perm}{w}
\end{array}\right.
\\
\failed & \totherwise
\end{cases}
\end{align*}

Change Current Address

15-09-2017: This is the old lea. I changed the name, so it actually reflects what the instruction does. We might also want to add a real lea at some point.

\begin{align*}
\sem{\tcca{r}{\rn}}(\Phi) = &
\begin{cases}
\updPcAddr{\Phi\updReg{r}{c}} &
\arraycolsep=0pt
\begin{array}[t]{l}
\Phi(\rn) = n \tand \\
\Phi(r) = ((\perm,\lin),\baddr,\eaddr,\aaddr) \tand \\
c = ((\perm,\lin),\baddr,\eaddr,\aaddr + n) \tand\\
r \neq \pcreg
\end{array}
\\
\updPcAddr{\Phi\updReg{r}{s}} &
\arraycolsep=0pt
\begin{array}[t]{l}
\Phi(\rn) = n \tand \\
\Phi(r) = \seal{\sigma_\baddr,\sigma_\eaddr,\sigma} \tand \\
s = \seal{\sigma_\baddr,\sigma_\eaddr,\sigma + n}
\end{array}
\\
\src{\updPcAddr{\Phi\updReg{r}{c}}} &
\sourcecolor\left.
\arraycolsep=0pt
\begin{array}[t]{l}
\Phi(\rn) = n\tand \\
\Phi(r) = \stkptr{\perm,\baddr,\eaddr,\aaddr} \tand \\
c = \stkptr{\perm,\baddr,\eaddr,\aaddr + n}
\end{array}\right.
\\
\failed & \totherwise
\end{cases}
\end{align*}

This instruction uses the $\decPerm{}$ function.

\begin{align*}
\sem{\trestrict{r_1}{\rn}}(\Phi) = &
\begin{cases}
\updPcAddr{}\left(
\arraycolsep=0pt
\begin{array}{rl}
\Phi &\updReg{r_1}{c}
\end{array} \right)
\arraycolsep=0pt
\begin{array}[t]{l}
\Phi(r_1) = ((\perm,\lin),\baddr,\eaddr,\aaddr) \tand \\
\Phi(\rn) = n \tand\\
\decPerm{n} \sqsubseteq \perm \tand \\
c = ((\decPerm{n},\lin),\baddr,\eaddr,\aaddr) \tand\\
r_1 \neq \pcreg
\end{array}
\\
\sourcecolor\left.
\updPcAddr{}\left(
\arraycolsep=0pt
\begin{array}{rl}
\Phi &\updReg{r_1}{c}
\end{array}\right)\right.
\sourcecolor\left.
\arraycolsep=0pt
\begin{array}[t]{l}
\Phi(r_1) = \stkptr{\perm,\baddr,\eaddr,\aaddr} \tand \\
\Phi(\rn) = n \tand\\
\decPerm{n} \sqsubseteq \perm \tand \\
c = \stkptr{\decPerm{n},\baddr,\eaddr,\aaddr}
\end{array}\right.
\\
\failed & \totherwise
\end{cases}
\end{align*}

\begin{align*}
\sem{\tlt{r_0}{\rn_1}{\rn_2}}(\Phi) = &
\begin{cases}
\updPcAddr{\Phi\updReg{r_0}{1}} &
\arraycolsep=0pt
\begin{array}[t]{l}
\text{if for $i \in \{1,2\}$}\\
\quad\Phi(\rn_i) = n_i \tand\\
\quad n_1 < n_2
\end{array}\\
\updPcAddr{\Phi\updReg{r_0}{0}} &
\arraycolsep=0pt
\begin{array}[t]{l}
\text{if for $i \in \{1,2\}$}\\
\quad \Phi(\rn_i) = n_i \tand \\
\quad n_1 \not< n_2\\
\end{array}\\
\failed & \text{otherwise}
\end{cases}
\end{align*}

plus and minus

\begin{align*}
\sem{\tplus{r_0}{\rn_1}{\rn_2}}(\Phi) = &
\begin{cases}
\updPcAddr{\Phi\updReg{r_0}{n_1+n_2}} &
\arraycolsep=0pt
\begin{array}[t]{l}
\text{if for $i \in \{1,2\}$}\\
\quad \Phi(\rn_i) = n_i\\
\end{array}\\
\failed & \text{otherwise}
\end{cases}
\end{align*}

\begin{align*}
\sem{\tminus{r_0}{\rn_1}{\rn_2}}(\Phi) = &
\begin{cases}
\updPcAddr{\Phi\updReg{r_0}{n_1-n_2}} &
\arraycolsep=0pt
\begin{array}[t]{l}
\text{if for $i \in \{1,2\}$}\\
\quad\Phi(\rn_i) = n_i\\
\end{array}\\
\failed & \text{otherwise}
\end{cases}
\end{align*}

\begin{align*}
\sem{\tsetatob{r_1}}(\Phi) = &
\begin{cases}
\updPcAddr{}\left(
\Phi \updReg{r_1}{c}
\right)
\arraycolsep=0pt
\begin{array}[t]{l}
\Phi(r_1) = ((\perm,\lin),\baddr,\eaddr,\_) \tand \\
c = ((\perm,\lin),\baddr,\eaddr,\baddr) \tand\\
r_1 \neq \pcreg
\end{array} \\
\updPcAddr{}\left(
\Phi \updReg{r_1}{c}
\right)
\arraycolsep=0pt
\begin{array}[t]{l}
\Phi(r_1) = \seal{\sigma_\baddr,\sigma_\eaddr,\_} \tand \\
c = \seal{\sigma_\baddr,\sigma_\eaddr,\sigma_\baddr}
\end{array} \\
\sourcecolor\left.
\updPcAddr{}\left(
\Phi\updReg{r_1}{c}
\right)
\right.
\sourcecolor\left.
\arraycolsep=0pt
\begin{array}[t]{l}
\Phi(r_1) = \stkptr{\perm,\baddr,\eaddr,\_} \tand \\
c = \stkptr{\perm,\baddr,\eaddr,\baddr}
\end{array}\right. \\
\failed & \totherwise
\end{cases}
\end{align*}

22-09-2017: Can we allow the callee to return any stack pointer? At the moment, it is not possible to create an empty stack pointer which may be a saving grace. If we at some point change this, so you can split capabilities into empty ones, then we need to consider whether it is safe for callees to return empty stacks (I think it is okay as long as we always have some stack usage).

\begin{align*}
\sem{\txjmp{r_1}{r_2}}(\Phi) = &
\begin{cases}
\Phi''
\begin{array}[t]{l}
\Phi(r_1) = \sealed{\sigma_1,c_1} \tand
\Phi(r_2) = \sealed{\sigma_2,c_2} \tand\\
\sigma_1 = \sigma_2 \tand \\
w_1 = \linCons{c_1} \tand \\
w_2 = \linCons{c_2} \tand \\
\Phi' = \Phi \updReg{r_1}{w_1} \updReg{r_2}{w_2} \tand\\
\Phi'' = \xjumpResult{c_1}{c_2}{\Phi'}
\end{array}\\
\failed & \totherwise
\end{cases}
\end{align*}

\begin{align*}
\xjumpResult{c_1}{c_2}{\Phi} =
\begin{cases}
\arraycolsep=0pt
\begin{array}[t]{rl}
\Phi & \updReg{\pcreg}{c_1}\\
& \updReg{\rdata}{c_2}
\end{array} &
\begin{array}[t]{l}
\src{c_1 \neq \retptrc(\_) \tand} \\
\src{c_2 \neq \retptrd(\_) \tand} \\
\nonExec{c_2}
\end{array}
\\&\\
\sourcecolor\left.
\arraycolsep=0pt
\begin{array}[t]{rl}
\Phi' & \updReg{\pcreg}{c_\opc}\\
& \updReg{\rdata}{0}\\
& \updReg{\rstk}{c_\stk}\\
& \updReg{\rtmp{1}}{0}\\
& \updReg{\rtmp{2}}{0}
\end{array}\right.&
\sourcecolor\left.
\begin{array}[t]{l}
c_1 = \retptrc(\baddr,\eaddr,\aaddr) \tand \\
c_2 = \retptrd(\aaddr_\stk,\eaddr_{\stk,\priv}) \tand \\
\Phi(\rstk) = \stkptr{\rw,\stkb,\eaddr_\stk,\_} \tand \\
\stkb \leq \eaddr_\stk \tand\\
\Phi = (\mem,\reg,\stkf::\stk,\ms_\stk) \tand \\
\stkf = (\opc,\ms_{\stk,\priv}) \tand \\
\opc = \aaddr \tand \\
c_\opc = ((\rx,\normal),\baddr,\eaddr,\opc) \tand \\
\dom(\ms_{\stk,\priv}) = [\eaddr_\stk+1,\eaddr_{\stk,\priv}] \tand\\
e_\stk + 1 = a_\stk \tand\\
c_\stk = \stkptr{\rw,\stkb,\eaddr_{\stk,\priv},\aaddr_\stk} \tand\\
\Phi' = (\mem,\reg,\stk,\ms_{\stk,\priv} \uplus \ms_\stk)
\end{array}\right.
\\
\failed & \totherwise
\end{cases}
\end{align*}

\begin{align*}
\sem{\tcseal{r_1}{r_2}}(\Phi) = &
\begin{cases}
\updPcAddr{}\left(
\arraycolsep=0pt
\begin{array}{rl}
\Phi&\updReg{r_1}{\vsc}
\end{array}\right)
\arraycolsep=0pt
\begin{array}[t]{l}
\Phi(r_1) \in \SealableCaps \tand \\
\Phi(r_2) = \seal{\sigma_\baddr, \sigma_\eaddr,\sigma} \tand \\
\sigma_\baddr \le \sigma \le \sigma_\eaddr \tand \\
\vsc = \sealed{\sigma,\Phi(r_1)}
\end{array}
\\
\failed & \totherwise
\end{cases}
\end{align*}

split and splice

We would like splice and split to have following properties

* No authority amplification - splitting or splicing capabilities should give you no more authority than you already had.

* Split should be dual to splice in the sense that a split on a capability followed by a splice of the two resulting capabilities should yield the same capability.

* Take the addresses governed by a linear capability to be a multiset. If this capability is split, then the union of the two multisets of addresses governed by the resulting capabilities should be the same as the first multiset. In other words, splice and split should not break linearity.

Split cannot create “empty capabilities” (a capability that governs no segment of the memory, i.e. a capability where the base address is greater than the end address). We partly do not allow this out of convenience as it makes the implementation of call simpler. We do not need empty capabilities as they have no semantic value in the sense that they allow you to do essentially the same as a piece of data.

\begin{align*}
\sem{\tsplit{r_1}{r_2}{r_3}{\rn_4}}(\Phi) = &
\begin{cases}
\updPcAddr{}\left(
\arraycolsep=0pt
\begin{array}{rl}
\Phi&\updReg{r_3}{w}\\
\end{array}\right)
\arraycolsep=0pt
\begin{array}[t]{l}
\Phi(r_3) = ((\perm,\lin),\baddr,\eaddr,\aaddr) \tand \\
\Phi(\rn_4) = n \tand\\
\baddr \leq n \tand n < \eaddr \tand \\
c_1 = ((\perm,\lin),\baddr,n,\aaddr) \tand \\
c_2 = ((\perm,\lin),n+1,\eaddr,\aaddr) \tand \\
w = \linCons{\Phi(r_3)} \tand \\
r_1,r_2,r_3 \neq \pcreg
\end{array}\\
\updPcAddr{} \left(
\arraycolsep=0pt
\begin{array}{rl}
\Phi&\updReg{r_1}{c_1}\\
\end{array} \right)
\arraycolsep=0pt
\begin{array}[t]{l}
\Phi(r_3) = \seal{\sigma_\baddr,\sigma_\eaddr,\sigma} \tand \\
\Phi(\rn_4) = n \tand\\
\sigma_\baddr \leq n \tand n < \sigma_\eaddr \tand \\
c_1 = \seal{\sigma_\baddr,n,\sigma} \tand \\
c_2 = \seal{n+1,\sigma_\eaddr,\sigma}
\end{array}\\
\sourcecolor\left.
\updPcAddr{}\left(
\arraycolsep=0pt
\begin{array}{rl}
\Phi&\updReg{r_3}{0}\\
\end{array} \right)\right.
\sourcecolor\left.
\arraycolsep=0pt
\begin{array}[t]{l}
\Phi(r_3) = \stkptr{\perm,\baddr,\eaddr,\aaddr} \tand \\
\Phi(\rn_4) = n \tand \\
\baddr \leq n \tand n < \eaddr \tand \\
c_1 = \stkptr{\perm,\baddr,n,\aaddr} \tand \\
c_2 = \stkptr{\perm,n+1,\eaddr,\aaddr}
\end{array} \right.\\
\failed & \totherwise
\end{cases}
\end{align*}

Two important points about $\tsplice{}{}{}$ related to the calling convention: (1) Splice fails if two capabilities are not adjacent.
This means that if a caller tries to use a return pointer with a stack that is not immediately adjacent to the private stack, then it fails.
(2) Splice prohibit splicing with an empty capability!
This means that a callee cannot return an empty stack (this also means that it is impossible to make a call when all of the stack is used - this may indeed be undesirable, but without this restriction we need to handle other things).
Note: because $\tsplice{}{}{}$ does not allow empty stacks, it is not “left inverse” to $\tsplit{}{}{}{}$ (because of the empty case).
Intuitively, it is weird that a $\tsplit{}{}{}{}$ followed by a $\tsplice{}{}{}$ does not yield the same capability.

\begin{align*}
\sem{\tsplice{r_1}{r_2}{r_3}}(\Phi) = &
\begin{cases}
\updPcAddr{}\left(
\arraycolsep=0pt
\begin{array}{r l}
\Phi&\updReg{r_2}{w_2}\\
\end{array}\right)
\arraycolsep=0pt
\begin{array}[t]{l}
\Phi(r_2) = ((\perm,\lin),\baddr_2,\eaddr_2,\_) \tand \\
\Phi(r_3) = ((\perm,\lin),\baddr_3,\eaddr_3,\aaddr_3) \tand \\
\eaddr_2 + 1 = \baddr_3 \tand \baddr_2 \leq \eaddr_2 \tand \baddr_3 \leq \eaddr_3 \tand \\
c = ((\perm,\lin),\baddr_2,\eaddr_3,\aaddr_3) \tand\\
w_2 = \linCons{\Phi(r_2)} \tand \\
w_3 = \linCons{\Phi(r_3)}  \tand \\
r_1,r_2,r_3 \neq \pcreg\\
\end{array}\\
\updPcAddr{}\left(
\arraycolsep=0pt
\begin{array}{r l}
\Phi&\updReg{r_1}{c}
\end{array}\right)
\arraycolsep=0pt
\begin{array}[t]{l}
\Phi(r_2) = \seal{\sigma_{\baddr,2},\sigma_{\eaddr,2},\_} \tand \\
\Phi(r_3) = \seal{\sigma_{\baddr,3},\sigma_{\eaddr,3},\sigma} \tand \\
\sigma_{\eaddr,2}+1 = \sigma_{\baddr,3} \tand \sigma_{\baddr,2} \leq \sigma_{\eaddr,2} \tand\\
\sigma_{\baddr,3} \leq \sigma_{\eaddr,3} \tand \\
c = \seal{\sigma_{\baddr,2},\sigma_{\eaddr,3},\sigma}
\end{array}\\
\sourcecolor\left.
\updPcAddr{}\left(
\arraycolsep=0pt
\begin{array}{r l}
\Phi&\updReg{r_2}{0}\\
\end{array}\right)\right.
\sourcecolor
\arraycolsep=0pt
\begin{array}[t]{l}
\Phi(r_2) = \stkptr{\perm,\baddr_2,\eaddr_2,\_} \tand \\
\Phi(r_3) = \stkptr{\perm,\baddr_3,\eaddr_3,\aaddr_3} \tand \\
\eaddr_2 + 1 = \baddr_3 \tand \baddr_2 \leq \eaddr_2 \tand \baddr_3 \leq \eaddr_3 \tand \\
c = \stkptr{\perm,\baddr_2,\eaddr_3,\aaddr_3} \\
\end{array}\\
\failed & \totherwise
\end{cases}
\end{align*}

\begin{multline*}
\sem{\scall{\offpc,\offsigma}{\src{r_1}}{\src{r_2}}}(\Phi) = \\
\begin{cases}
\mathit{xjumpResult}\left(c_1,c_2,
\arraycolsep=0pt
\array[]{rl}
\Phi'&\updReg{r_1}{w_1} \\
&\updReg{r_2}{w_2} \\
\endarray
\right)
& \arraycolsep=0pt
\begin{array}[t]{l}
r_1 \neq \rtmp{1} \tand r_2 \neq \rtmp{1} \tand\\
\Phi(r_1) = \sealed{\sigma_1,c_1} \tand \\
\Phi(r_2) = \sealed{\sigma_2,c_2} \tand \\
\sigma_1 = \sigma_2 \tand \\
\nonExec{c_2} \tand\\
\Phi = (\mem,\reg,\stk,\ms_\stk) \tand\\
\Phi(\rstk) = \stkptr{\rw,\baddr_\stk,\eaddr_\stk,\aaddr_\stk} \tand \\
\baddr_\stk < \aaddr_\stk \leq \eaddr_\stk \tand \\
\ms_{\stk,\priv} = \ms_\stk |_{[\aaddr_\stk,\eaddr_\stk]}\update{\aaddr_\stk}{42} \tand\\
\ms_{\stk,\var{rest}} = \ms_\stk - \ms_\stk |_{[\aaddr_\stk,\eaddr_\stk]} \tand \\
c_\stk = \stkptr{\rw,\baddr_\stk,\aaddr_\stk-1,\aaddr_\stk-1} \tand \\
c_\var{priv\_data} = \retptrd(\aaddr_\stk,\eaddr_\stk) \tand \\
\Phi(\pcreg) = ((\_,\_),\baddr,\eaddr,\aaddr) \tand \\
\opc = \aaddr + \calllen \tand \\
c_\opc = \retptrc(\baddr,\eaddr,\aaddr+\calllen) \tand \\
\stk' = (\opc,\ms_{\stk,\priv}) :: \stk \tand\\
\Phi' = (\mem,\reg,\stk',\ms_{\stk,\var{rest}})\tand\\
\mem(\aaddr+\offpc) = \seal{\sigma_\baddr,\sigma_\eaddr,\sigma_\aaddr}\tand\\
\baddr \leq  \aaddr+\offpc \leq \eaddr \tand \\
\sigma_? = \sigma_\aaddr + \offsigma \tand\\
\sigma_\baddr \leq \sigma_? \leq \sigma_\eaddr \tand\\
w_1 = \linCons{\Phi(r_1)} \tand \\
w_2 = \linCons{\Phi(r_2)}
\end{array}\\
\failed & \totherwise
\end{cases}
\end{multline*}

Note: the caller may have split part of the stack pointer off and even pass the fragments split off to the callee in registers.
This behavior is in principle fine.
Source semantics will define that only the non-split-off part will be encapsulated.
The parts that were split off and passed to the adversary are not protected, as expected.

§.§ Components

A component can be either a component with a main (i.e. a program that still needs to be linked with library implementations) or one without (i.e. a library implementation that will be used by other components).
It contains code memory, data memory a list of imported symbols, a list of exported symbols, a list of seals used for producing return capability pairs and a list of seals used for producing closures.

We define a component as follows:

\begin{align*}
s &\in \Symbol\\
\var{import} &\mathrel{::=} a \mapsfrom s\\
\var{export} &\mathrel{::=} s \mapsto w\\
\var{comp}_0 &\mathrel{::=} (\mscode,\msdata,\overline{\var{import}},\overline{\var{export}},\sigrets,\sigcloss,A_\linear)\\
\var{comp} &\mathrel{::=} \var{comp}_0\\
&\mid  (\var{comp}_0,c_{\mathrm{main},c}, c_{\mathrm{main},d})
\end{align*}

We define inductively when a component is valid ($\ta \vdash \var{comp}$) by the below inference rules:

(a) = σ_,σ_,σ_     [σ_,σ_] = (∪)

,[owned],,⊢_comp-code ,a

(a) ∈

([a ⋯a + -1] ⊆∧([a ⋯a + -1]) = [0..-1],r_1r_2)
((a+) = σ_,σ_,σ_ ∧σ_+∈[owned])

,[owned],,⊢_comp-code ,a

$\mscode$ has no hidden calls

∃d_σ: () → = _a ∈() d_σ(a)

∀a ∈() ,d_σ(a),,⊢_comp-code ,a

∃a (a) = σ_,σ_,_ ∧[σ_,σ_] ≠∅

A_code,A_own,A_non-linear,,⊢_comp-value z

= ⇒∅⊂[,] ⊆A_own
= ⇒[,] ⊆A_non-linear

A_code,A_own,A_non-linear,,⊢_comp-value ((,),,,)

A_code,A_own,A_non-linear,,⊢_comp-value σ,

[,] ⊆A_code
A_code,A_non-linear,,⊢_comp-export s ↦σ,((,),,,)

A_code,∅,A_non-linear,,⊢_comp-value w

A_code,A_non-linear,,⊢_comp-export s ↦w

() = [,]
[-1,+1] # ()

= [-1↦0] ⊎[+1 ↦0]

∃A_own : () →()     () = A_non-linear ⊎A_

A_= _a ∈() A_own(a)

∀a ∈()(),A_own(a),A_non-linear,,⊢_comp-value (a)

export = s_export ↦w_export     import = a_import s_import    {a_import} ⊆()

(), A_non-linear, ,⊢_comp-export w_export

s_import # s_export     (∅≠() ⊆) ∨(() # ∧= ∅)
() #

comp_0 = (,,import,export,,,A_)

⊢comp_0     (_ ↦c_main,c), (_ ↦c_main,d) ∈export

⊢(comp_0,c_main,c, c_main,d)

where the following definition is used

We say that a memory segment $\mscode$ has no hidden calls iff

\[
\begin{array}{l}
\forall \aaddr \in \dom(\mscode) \ldotp \\
\quad \forall i \in [0,\calllen - 1] \\
\qquad \mscode(a + i) = \scall[i]{\offpc,\offsigma}{r_1}{r_2} \Rightarrow \\
\qquad \quad (\dom(\mscode) \supseteq [\aaddr-i,\aaddr + \calllen - i - 1]
\wedge \mscode([\aaddr-i,\aaddr + \calllen - i -1]) =
\scall[0..\calllen-1]{\offpc,\offsigma}{r_1}{r_2}) \vee\\
\qquad \quad \exists j \in [\aaddr-i,\aaddr + \calllen - i -1] \cap \dom(\mscode) \ldotp \mscode(j) \neq  \scall[j-\aaddr-i]{\offpc,\offsigma}{r_1}{r_2}
\end{array}
\]

§.§ Linking

comp_1 = ([1], [1], import_1, export_1, [1], [1],A_,1)

comp_2 = ([2], [2], import_2, export_2, [2], [2],A_,2)

comp_3 = ([3], [3], import_3, export_3, [3], [3],A_,3)

[3] = [1] ⊎[2]

[3] = ([1] ⊎[2])[a ↦w |(a s) ∈(import_1 ∪import_2), (s ↦w) ∈export_3]

export_3 = export_1 ∪export_2
import_3 = { a s ∈(import_1 ∪import_2) |s ↦_ ∉export_3 }

[3] = [1] ⊎[2]
[3] = [1] ⊎[2]
A_,3 = A_,1 ⊎A_,2

([3]) # ([3])     [3] # [3]

comp_3 = comp_1 ⋈comp_2

comp_0” = comp_0 ⋈comp_0'

(comp_0”,c_main,c, c_main,d) = comp_0 ⋈(comp_0',c_main,c, c_main,d)

comp_0” = comp_0 ⋈comp_0'

(comp_0”,c_main,c, c_main,d) = (comp_0,c_main,c, c_main,d) ⋈comp_0'

§.§ Programs, contexts, initial execution configuration

A program is intuitively a component that is ready to be executed, i.e. it must have an empty import list and a pair of capabilities to be used as main.
A context for a given component is any other component that can be linked with it to produce a program.

We define a program to be a component $(\var{comp}_0,c_{\mathrm{main},c}, c_{\mathrm{main},d})$ with an empty import list.

A context for a component $\var{comp}$ is another component $\var{comp}'$ such that $\var{comp} \bowtie \var{comp}'$ is a program.

c_main,c = σ_1, c_main,c'
c_main,d = σ_2, c_main,d'
σ_1 = σ_2

() = c_main,c'
() = c_main,d'

() = ,_,_,_
() = ((,),_,_,_)

(∖{,,}) = 0

_ = {0}
= ⊎ ⊎  _ ⊎_frame

[_,_] = (_)
[_-1,_+1]# (() ∪())
import = ∅
((, , import, export, , ,A_),  c_main,c, c_main,d) ⇝(, , ∅, _)

07-07-2018: TODO why don't the above definition care about the stack base?

When $\var{comp'}$ is a context for component $\var{comp}$ and $\var{comp}' \bowtie \var{comp} \rightsquigarrow \Phi$,
then we write $\plug{\var{comp'}}{\var{comp}}$ for the execution configuration $\Phi$.

For components $\context$ and $\comp$,

* $\emptyset \vdash \context$

* $\dom(\comp.\mscode) \vdash \comp$

* $\plug{\context}{\comp}$ is defined

\[
\dom(\comp.\mscode) \vdash \context
\]

Follows by definition.

§ COMPILER

The compiler is the identity.

§ LOGICAL RELATION

In the following definitions, blue is used to indicate values related to the source machine. This is unlike previous definitions, where blue was used to indicate source language specific parts of definitions.

§.§ Worlds

There exists a c.o.f.e. $\Wor$ and preorder $\future$ such that $(\Wor,\future)$ and there exists an isomorphism $\xi$ such that

\[
\xi : \Wor \cong \blater (\Worldh \times \Worlds \times \Worldfs)
\]

and for $\hat{W},\hat{W}' \in \Wor$

\[
\hat{W'} \future \hat{W}\text{ iff }\xi(\hat{W'}) \future \xi(\hat{W})
\]

Where $\Worlds$, $\Worldh$, and $\Worldfs$ are defined as follows

\[
\Worldh = \RegionName \parfun (\Regions + \Regionh)
\]

\[
\Worlds = \RegionName \parfun (\Regions \times \Addr)
\]

\[
\Worldfs = \RegionName \parfun \Regions
\]

where $\RegionName = \nats$.

\begin{multline*}
\Regionh =
\{\pure \} \times (\Wor \monnefun \URel{\MemSeg^2}) \times \\
(\Seal \parfun \Wor \monnefun \URel{\SealableCaps \times \SealableCaps})
\end{multline*}

\[
\Regions = \left\{
\begin{array}{l}
\{\spatial \} \times (\Wor \monnefun \URel{\MemSeg^2}) \uplus \\
\{\spatialo \} \times (\Wor \monnefun \URel{\MemSeg^2})\uplus \\
\{\revoked\}
\end{array} \right.
\]

where $\spatial$ and $\spatialo$ are regions governing segments of memory addressed by linear capabilities.
$\spatialo$ signifies that this region is addressable.
$\spatial$ signifies that the region is not owned and can thus not be addressed.
At the same time it signifies that if something else addresses it, it is a $\linear$ capability.
Finally, $\pure$ signifies that the region is only addressed by non-linear capabilities.
Notice that no region allows for both linear and non-linear capabilities to address it.
Notice also that $\pure$ regions have an additional component that allows them to claim ownership of part of the address space of seals and impose a relational invariant on everything signed with those seals.

I suppose you are thinking of $\nequal$ for UPreds?
The way I have seen it before, it is defined as “up to $n-1$ (including)”.
More precisely: Define the $k$-cut of $p \in \UPred{A}$ to be

\[
\kcut{p} = \{ (j,a) \in p | j < k \}.
\]

We use this to define a family of equivalences $(\nequal)_{n=0}^{\infty}$ to be, for $p$ and $q$ in $\UPred{A}$

\[
p \nequal q \textit{ iff } \kcut[n]{p} = \kcut[n]{q}
\]

If we pick a different definition, we should check that it is indeed a well-defined $n$-equality (for instance, it should be the total relation for $\nequal[0]$).

We introduce a bit of notation for projecting out each part of the world:

\[
\begin{array}{l}
\pwheap = \pi_1(W)\\
\pwpriv = \pi_2(W)\\
\pwfree = \pi_3(W)
\end{array}
\]

as well as projections for the regions:

\[
\begin{array}{l}
\prv{(v,s,\phi_\pub,\phi,H)} = v \\
\prv{\revoked} = \revoked
\end{array}
\]

We define erasure for worlds as follows:

\[
\erase{(W_{\mathrm{heap}},W_{\mathrm{priv}},W_{\mathrm{free}})}{S} =
\left( \erase{W_{\mathrm{heap}}}{S},\erase{W_{\mathrm{priv}}}{S},\erase{W_{\mathrm{free}}}{S} \right)
\]

where erasure for each part of a world is defined as follows:

\[
\erase{W_{\mathrm{heap}}}{S} = \lambda r \ldotp \left\{
\begin{array}{l}
\prv{W_{\mathrm{heap}}(r)} \in S\\
\bot
\end{array}
\right.
\]

\[
\erase{W_{\mathrm{priv}}}{S} = \lambda r \ldotp \left\{
\begin{array}{l}
\prv{\pregion{W_{\mathrm{priv}}(r)}} \in S \\
\bot
\end{array}
\right.
\]

\[
\erase{W_{\mathrm{free}}}{S} = \lambda r \ldotp \left\{
\begin{array}{l}
\prv{W_{\mathrm{free}}(r)} \in S\\
\bot
\end{array}
\right.
\]

The $\activeReg{}$ function takes a world and filters away all the revoked regions, so

\[
\activeReg{W} = \erase{W}{\spatial,\spatialo,\pure}
\]

Disjoint union of worlds. Joins together two alike worlds with strictly disjoint ownership over $\spatialo$-regions. Two worlds can be joined together if all of their three parts agree on the region names and each of their regions can be joined together.

\[
W_1 \oplus W_2 = W
\text{ iff }
\begin{array}[t]{l}
\dom(\pwheap) = \dom(\pwheap[W_1]) = \dom(\pwheap[W_2]) \tand \\
\dom(\pwfree) = \dom(\pwfree[W_1]) = \dom(\pwfree[W_2]) \tand \\
\dom(\pwpriv) = \dom(\pwpriv[W_1]) = \dom(\pwpriv[W_2]) \tand \\
\forall r \in \dom(\pwheap) \ldotp \pwheap(r) = \pwheap[W_1](r) \oplus \pwheap[W_2](r) \tand \\
\forall r \in \dom(\pwfree) \ldotp \pwfree(r) = \pwfree[W_1](r) \oplus \pwfree[W_2](r) \tand \\
\forall r \in \dom(\pwpriv) \ldotp \pi_1(\pwpriv(r)) = \pi_1(\pwpriv[W_1](r)) \oplus \pi_1(\pwpriv[W_2](r))
\end{array}
\]

$\oplus$ on regions is defined as follows

\begin{align*}
(\pure,H,H_\sigma) \oplus (\pure,H,H_\sigma) =  & \; (\pure,H,H_\sigma) \\
(\spatial,H) \oplus (\spatial,H) =  & \; (\spatial,H) \\
(\spatialo,H) \oplus (\spatial,H) = & \; (\spatial,H) \oplus (\spatialo,H)\\
=  & \; (\spatialo,H)
\end{align*}

and for all other cases $\oplus$ is undefined. Specifically, $\oplus$ is not defined when both sides are a $\spatialo$-region. It is further not defined if the two sides do not agree on region type or heap or sealed value relations.

$\oplus$ is associative and commutative.
Also, left-hand sides in the commutativity and associativity laws are defined whenever the right-hand sides are defined and vice versa.

Follows easily from the definitions.

If $W' \future W_1 \oplus W_2$, then there exist $W_1',W_2'$ such that $W' = W_1' \oplus W_2'$ and $W_1' \future W_1$ and $W_2' \future W_2$.

We define $W_1'$ and $W_2'$ to have the same regions as $W'$ with a possibly different visibility.
For regions that are present in $W_1$ and $W_2$, we give them the same visibility in $W_1'$ and $W_2'$ respectively.
For regions that are new in $W'$, we make them $\pure$ or $\spatial$ in both $W_1'$ and $W_2'$ if they are in $W'$ and we make them $\spatialo$ in $W_1'$ but $\spatial$ in $W_2'$ if they are spatial in $W'$.
It is then easy to check that the required equations hold.

We also define a second disjoint union operator of worlds:

\[
W_1 \uplus W_2 = W
\text{ iff }
\begin{array}[t]{l}
\dom(\pwheap) = \dom(\pwheap[W_1]) \uplus \dom(\pwheap[W_2]) \tand \\
\dom(\pwfree) = \dom(\pwfree[W_1]) \uplus \dom(\pwfree[W_2]) \tand \\
\dom(\pwpriv) = \dom(\pwpriv[W_1]) \uplus \dom(\pwpriv[W_2]) \\
\end{array}
\]

The two operators $\uplus$ and $\oplus$ are quite different.
The difference is most clear in the treatment of pure regions: $\uplus$ allows both worlds to have the same pure region, while $\oplus$ forbids this.
To understand this different treatment ($W_1 \uplus W_2$ and $W_1 \oplus W_2$), you should understand that the two are intended for different usages of worlds.
The $W_1 \oplus W_2$ operator treats the worlds as specifications of authority: taking the disjoint union of worlds specifying non-exclusive ownership of a block of memory is allowed and produces a new world that also specifies non-exclusive ownership of world.
The $W_1 \uplus W_2$  operator treats worlds as specifications of memory contents: taking the disjoint union of worlds specifying the presence of the same memory range is not allowed.
The latter operator is used in the logical relation for components which specifies (among other things) that the world should specify the presence of the component's data memory.
Linking two components then produces a new component with both components' data memory.
The linked component is then valid in a world that has the combined memory presence specifications, not the combined authority.
In other words, $\oplus$ specifies disjoint authority distribution, while $\uplus$ specifies disjoint memory allocation.

Note also that this picture is further complicated by our usage of non-authority-carrying $\spatial$ regions.
They are really only there in a world $W$ as a shadow copy of a $\spatialo$ region in another world $W'$ that $W$ will be combined with.
The shadow copy is used for specifying when a memory satisfies a world: the memory should contain all memory ranges that anyone has authority over, not just the ones whose authority belongs to the memory itself.
For example, if a register contains a linear pointer to a range of memory, then the register file will be valid in a world where the corresponding region is $\spatialo$, while the memory will be valid in a world with the corresponding region only $\spatial$.
However, for the memory to satisfy the world, the block of memory needs to be there, i.e. the memory should contain blocks of memory satisfying every region that is $\spatialo$, $\pure$, but also just $\spatial$ (because it may be $\spatialo$ in, for example, the register file's world).

$\uplus$ is associative and commutative.

Follows easily from the definitions.

\begin{equation*}
(W_1\oplus W_2) \uplus (W_3 \oplus W_4) = (W_1 \uplus W_3) \oplus (W_2 \uplus W_4)
\end{equation*}

Also, the left expression is defined iff the right expression is.

Follows by definition-chasing.

§.§ Future world

The future world relation becomes:

for $i \in \{\mathrm{heap},\mathrm{free},\mathrm{priv} \}$
∃m_i : ,  injective(W'.i) ⊇(m_i(W.i)) ∧∀r ∈(W.i)W'.i(m_i(r)) W.i(r)
W' W

Future regions allow $\spatial$ regions to become $\revoked$.
Also: the future region relation allows $\spatial$ regions to become $\spatialo$, which expresses that our system is affine, rather than linear.
22-3-2018: TODO need extra rules for regions with seal interpretations

(,H) (,H)
(,H) (,H)
(,H) (,H)

For any world $W$, we define

\begin{align*}
\purePart{W} &\defeq (\purePart{\pwheap},\purePart{\pwpriv},\purePart{\pwfree})\\
\purePart{W_\var{heap}} &\defeq
\begin{cases}
W_{\var{heap}}(r) & \text{if } W_\var{heap}(r) = (pure,\var{sm})\\
(\spatial,\var{sm}) & \text{if } W_\var{heap}(r) = (\spatial,\var{sm})\\
(\spatial,\var{sm}) & \text{if } W_\var{heap}(r) = (\spatialo,\var{sm})\\
\revoked & \text{if } W_\var{heap}(r) = \revoked\\
\end{cases}\\
\purePart{W_\var{priv}} &\defeq
\begin{cases}
((\spatial,\var{sm}),\opc) & \text{if } W_\var{priv}(r) = ((\spatial,\var{sm}),\opc)\\
((\spatial,\var{sm}),\opc) & \text{if } W_\var{priv}(r) = ((\spatialo,\var{sm}),\opc)\\
(\revoked,\opc) & \text{if } W_\var{priv}(r) = (\revoked,\opc)\\
\end{cases}\\
\purePart{W_\var{free}} &\defeq
\begin{cases}
W_{\var{free}}(r) & \text{if } W_{\var{free}}(r) = (pure,\var{sm})\\
(\spatial,\var{sm}) & \text{if } W_{\var{free}}(r) = (\spatial,\var{sm})\\
(\spatial,\var{sm}) & \text{if } W_{\var{free}}(r) = (\spatialo,\var{sm})\\
\revoked & \text{if } W_{\var{free}}(r) = \revoked\\
\end{cases}
\end{align*}

For all $W$, we have that $W = W \oplus \purePart{W}$.

Follows from the definition of $\purePart{}$ and $\oplus$.

For all $W$, we have that $\purePart{W} = \purePart{}(\purePart{W})$ and $\purePart{W} = \purePart{W} \oplus \purePart{W}$.

The first part follows easily from the definition.
The second statement follows from the first, together with Lemma <ref>.

For all $W_1,W_2$, we have that $\purePart{W_1\oplus W_2} = \purePart{W_1} \oplus \purePart{W_2} = \purePart{W_1} = \purePart{W_2}$.
Also, all worlds in the equations above are defined when $W_1\oplus W_2$ is defined (but not necessarily vice versa).

Follows from the definition of $\purePart{}$ and $\oplus$.

For all $W'\future W$, we have that $\purePart{W'} \future \purePart{W}$.

Follows easily from the definition of $\purePart{}$ and $\future$.

For all $W_1,W_2$, we have that:
$W_1 \oplus W_2 \future W_1$

Follows easily from the definitions.

For all $W_1,W_2$, we have that:
$W_1 \uplus W_2 \future W_1$

Follows easily from the definitions.

For all $W$, we have that $W \future \purePart{W}$.

Consequence of Lemmas <ref>
and <ref>.

If $W = W_1 \oplus W_2$, then $W_1 \future \purePart{W}$.

Follows easily from the definitions.

§.§ Memory satisfaction

14-02-2018: No matter what the memory satisfaction ends up looking like, remember to handle the revoked case.

RESOLVED add frame to memory satisfaction and remove it from observation relation.
Memory satisfaction for new worlds:

\[
\memSat{\ms_S,\ms_\stk,\stk,\ms_T}{W} \text{ iff }
\left\{
\begin{array}{l}
\stk = (\opc_0,\ms_0):: \dots :: (\opc_m,\ms_m) \wedge \\
\ms_S \uplus \ms_\stk \uplus \ms_0 \uplus \dots \uplus \ms_m  \text{ is defined} \wedge\\
W = W_{\var{stack}} \oplus W_{\var{free\_stack}} \oplus W_{\var{heap}} \wedge\\
\exists \ms_\var{T,stack}, \ms_\var{T,free\_stack}, \ms_\var{T,heap}, \ms_{T,f}, \ms_{S,f}, \ms_S',\overline{\sigma}\ldotp \\
\quad \ms_S = \ms_{f,S} \uplus \ms_S' \wedge \\
\quad \ms_T = \ms_\var{T,stack} \uplus \ms_\var{T,free\_stack} \uplus \ms_\var{T,heap} \uplus \ms_{T,f} \wedge \\
\quad \dom(\ms_{\var{T,stack}} \uplus \var{T,free\_stack}) = [\baddr_\stk,\eaddr_\stk] \wedge \\
\quad \{\baddr_\stk -1,\eaddr_\stk + 1\} \in \dom(\ms_{T,f}) \wedge \\
\quad \memSatStack{\stk,\ms_\var{T,stack}}{W_{\var{stack}}} \wedge \\
\quad \memSatFStack{\ms_\stk,\ms_\var{T,free\_stack}}{W_{\var{free\_stack}}} \wedge \\
\quad \npair{(\overline{\sigma},\ms_S',\ms_\var{T,heap})} \in \lrheap(\pwheap)(W_{\var{heap}})
\end{array}
\right.
\]

\[
\memSatStack{\stk,\ms_T}{W} \text{ iff }
\left\{
\begin{array}{l}
W_\var{stack} = \pwpriv \wedge \\
\stk = (\opc_0,\ms_0), \dots (\opc_m,\ms_m) \wedge \\
\forall i \in \{0,\dots,m\} \ldotp (\dom(\ms_i) \neq \emptyset \wedge\\
\quad \forall i < j \ldotp \forall a \in \dom(\ms_i) \ldotp \forall a' \in \dom(\ms_j) \ldotp \stkb < a < a') \wedge\\
\exists R_\ms : \dom(\activeReg{W_\var{stack}}) \fun \MemSeg \times \Addr \times \MemSeg \ldotp \\
\quad \ms_T = \biguplus_{r \in \dom(\activeReg{W_\var{stack}})} \pi_3(R_\ms(r)) \wedge \\
\quad \ms_0 \uplus \dots \uplus \ms_m = \biguplus_{r \in \dom(\activeReg{W_\var{stack}})} \pi_1(R_\ms(r)) \wedge \\
\quad \exists R_W : \dom(\activeReg{W_\var{stack}}) \fun \World \ldotp \\
\qquad W = \bigoplus_{r \in \dom(\activeReg{W_\var{stack}})} R_W(r) \wedge \\
\qquad \forall r \in \dom(\activeReg{W_\var{stack}}), n' < n\ldotp \\
\qquad \quad \npair[n']{(\pi_1(R_\ms(r)),\pi_3(R_\ms(r))} \in W_\var{stack}(r).H \; \xi^{-1}(R_W(r)) \wedge\\
\qquad \quad \pi_2(R_\ms(r)) = W_\var{stack}(r).\opc \wedge\\
\qquad \quad \exists i \ldotp \opc_i = W_\var{stack}(r).\opc \wedge \ms_i = \pi_1 (R_\ms(r))
\end{array}
\right.
\]

\[
\memSatFStack{ms_\stk,\ms_T}{W} \text{ iff }
\left\{
\begin{array}{l}
W_\var{stack} = \pwfree \wedge \\
\exists R_\ms : \dom(\activeReg{W_\var{stack}}) \fun \MemSeg \times \MemSeg \wedge \\
\quad \ms_T = \biguplus_{r \in \dom(\activeReg{W_\var{stack}})} \pi_2(R_\ms(r)) \wedge \\
\quad \ms_\stk = \biguplus_{r \in \dom(\activeReg{W_\var{stack}})} \pi_1(R_\ms(r)) \wedge \\
\quad \stkb \in \dom(\ms_T) \wedge \stkb \in \dom(\ms_\stk) \wedge \\
\quad \exists R_W : \dom(\activeReg{W_\var{stack}}) \fun \World\ldotp\\
\qquad W = \oplus_{r \in \dom(\activeReg{W_\var{stack}})} R_W(r) \wedge\\
\qquad \forall r \in \dom(\activeReg{W_\var{stack}}),n' < n \ldotp \\
\qquad \quad \npair[n']{R_\ms(r)} \in  W_\var{stack}(r).H \; \xi^{-1}(R_W(r))
\end{array}
\right.
\]

\[
\lrheap(\pwheap)(W') =
\left\{
\npair{(\overline{\sigma},ms,\ms_T)} \middle|
\begin{array}{l}
\exists R_\ms : \dom(\activeReg{\pwheap}) \fun \MemSeg \times \MemSeg \wedge \\
\quad \ms_T = \biguplus_{r \in \dom(\activeReg{\pwheap})} \pi_2(R_\ms(r)) \wedge \\
\quad \ms = \biguplus_{r \in \dom(\activeReg{\pwheap})} \pi_1(R_\ms(r)) \wedge \\
\quad \exists R_W : \dom(\activeReg{\pwheap}) \fun \World\ldotp\\
\qquad W' = \oplus_{r \in \dom(\activeReg{\pwheap})} R_W(r) \wedge\\
\qquad \forall r \in \dom(\activeReg{\pwheap}), n' < n \ldotp \\
\qquad \quad \npair[n']{R_\ms(r)} \in  \pwheap(r).H \; \xi^{-1}(R_W(r)) \wedge\\
\exists R_\var{seal} : \dom(\activeReg{\pwheap}) \fun \powerset{\Seal} \wedge\\
\quad \biguplus_{r \in \dom(\activeReg{\pwheap})} R_\var{seal}(r)) \subseteq \overline{\sigma} \wedge\\
\quad \dom(\pwheap(r).H_\sigma) = R_\var{seal}(r)
\end{array}
\right.
\]

If $\npair{(\overline{\sigma_1},ms_{S,1},\ms_{T,1})}\in\lrheap(\pwheap[W_1])(W)$ and $\npair{(\overline{\sigma_2},ms_{S,2},\ms_{T,2})} \in \lrheap(\pwheap[W_2])(W)$, then $\npair{(\overline{\sigma_1}\uplus\overline{\sigma_2},ms_{S,1}\uplus \ms_{S,2},\ms_{T,1}\uplus \ms_{T,2})} \in \lrheap(\pwheap[W_1 \uplus W_2])(W)$.

Unfolding the definitions, it's easy to construct the memory and seal partitions $R_{\ms,3}$ and $R_{\var{seal},3}$ and $R_{W,3}$ from the corresponding partitions of the separate memories, seals and worlds.

§.§ Relation

Two expression relations: one for sealed code-data pairs being jumped to and one for capabilities being jumped to in the regular way.
The argument for having one relation relate pairs of pairs of capabilities and the other relate pairs of capabilities is that that is how xjump and regular jumps work: xjump takes pairs while regular jumps take single capabilities.

\begin{align*}
\lrexj(W) &= \left\{ \npair{\stpair[.]{v_{c,S},v_{d,S}}{v_{c,T},v_{d,T}}} \middle|
\begin{array}{l}
\forall n' \leq n, \src{\reg_S}, \reg_T, \src{\ms_S}, \ms_T, \src{\ms_\stk}, \src{\stk} \ldotp\\
\quad \forall W_\lrrs , W_\lrm \ldotp \\
\qquad\npair[n']{\stpair{\reg}{\reg}} \in \lrr(\{\rdata\}) (W_\lrrs ) \wedge\\
\qquad\memSat[n']{\stpair[.]{\ms_S,\stk,\ms_\stk}{\ms_T}}{W_\lrm} \wedge \\
\qquad\Phi_S = \src{(\ms_S,\reg_S,\stk, \ms_\stk)}\wedge\\
\qquad\Phi_T = (\ms_T,\reg_T) \wedge\\
\qquad W \oplus W_\lrrs \oplus W_\lrm \text{ is defined }\\
\qquad\Rightarrow \exists \Phi_S',\Phi_T'\ldotp\\
\quad\qquad \Phi_S' = \xjumpResult{v_{c,S}}{v_{d,S}}{\Phi_S} \tand\\
\quad\qquad\Phi_T' = \xjumpResult{v_{c,T}}{v_{d,T}}{\Phi_T}\tand\\
\quad\qquad\npair[n']{\left(\Phi_S', \Phi_T' \right)}\in \lro
\end{array}
\right\}\\
\lre(W) &= \left\{ \npair{\stpair[.]{v_{c,S}}{v_{c,T}}} \middle|
\begin{array}{l}
\forall n' \leq n, \src{\reg_S}, \reg_T, \src{\ms_S}, \ms_T, \src{\ms_\stk}, \src{\stk} \ldotp\\
\quad \forall W_\lrrs , W_\lrm \ldotp \\
\qquad\npair[n']{\stpair{\reg}{\reg}} \in \lrr(W_\lrrs ) \wedge\\
\qquad\memSat[n']{\stpair[.]{\ms_S,\stk,\ms_\stk}{\ms_T}}{W_\lrm} \\
\qquad\Phi_S = \src{(\ms_S,\reg_S,\stk, \ms_\stk)}\\
\qquad \Phi_S' = \Phi_S \updReg{\pcreg}{v_{c,S}}\\
\qquad\Phi_T = (\ms_T,\reg_T)\\
\qquad\Phi_T' = \Phi_T\updReg{\pcreg}{v_{c,T}}\\
\qquad W \oplus W_\lrrs \oplus W_\lrm\\
\qquad\Rightarrow\npair[n']{\left(\Phi_S', \Phi_T' \right)}\in \lro
\end{array}
\right\}
\end{align*}

09-07-2018: Fix these definitions' formatting like in paper

\[
\lro[\preceq,(\ta,\stkb,\_,\_)] = \left\{ \npair{\left(\array{l}\src{(\ms_S,\reg_S,\stk_S,\ms_{\stk,S})},\\(\ms_T,\reg_T)\endarray\right)} \middle|
\begin{array}{l}
\forall i \leq n \ldotp \\
\quad \src{(\ms_S,\reg_S,\stk_S,\ms_{\stk,S})} \sterm[i]{\ta,\stkb} \\\qquad\Rightarrow (\ms_T,\reg_T) \term\\
\end{array}
\right\}
\]

\[
\lro[\succeq,(\ta,\stkb,\_,\_)] = \left\{ \npair{\left(\array{l}\src{(\ms_S,\reg_S,\stk_S,\ms_{\stk,S})},\\(\ms_T,\reg_T)\endarray\right)} \middle|
\begin{array}{l}
\forall i \leq n \ldotp \\
\quad (\ms_T ,\reg_T) \term[i] \\\qquad\Rightarrow \src{(\ms_S,\reg_S,\stk_S,\ms_{\stk,S})} \sterm{\ta,\stkb}
\end{array}
\right\}
\]

\[
\lrrg{\trust}(R)(W) = \left\{ \npair{\stpair{\reg}{\reg}} \middle|
\begin{array}{l}
\exists S : (\RegName \setminus (\{\pcreg \} \cup R))\fun \World \ldotp \\
\quad W = \bigoplus_{r \in (\RegName\setminus (\{\pcreg,\rdata \} \cup R))} S(r) \wedge \\
\quad \forall r \in \RegName \setminus (\{\pcreg \} \cup R)\ldotp\\
\qquad\npair{\stpair[.]{\src{\reg_S(r)}}{\reg_T(r)}} \in \lrvg{\trust}(S(r))
\end{array}
\right\}
\]

We write $\lrr(W)$ to mean $\lrr(\emptyset)(W)$. That is, if we do not need to exclude extra registers, then we simply omit that argument.
RESOLVED check what conditions need to have a “square” i.e. need approximation

\[
\lrv(W) =
\begin{array}[t]{l}
\left\{ \npair{\stpair[.]{i}{i}} \;\middle|\; i \in \ints \right\}\cup \\
\hspace{-2cm}\left\{ \npair{\left(\arraycolsep=0pt\array{l}\src{\sealed{\sigma,\vsc_S}},\\ \sealed{\sigma,\vsc_T} \endarray\right)} \;\middle| \;
\begin{array}{l}
(\isLinear{\src{\vsc_S}} \text{ iff } \isLinear{\vsc_T}) \wedge\\
\exists r \in \dom(\pwheap), \sigrets,\sigcloss,\mscode \ldotp \pwheap(r) = (\pure,\_,H_\sigma) \tand \\
\quad H_\sigma \; \sigma \nequal H^\mathrm{code,\square}_\sigma \; \sigrets \; \sigcloss \; \mscode \; \gc \; \sigma \tand \\
\quad \npair[n']{\stpair[.]{\vsc_S}{\vsc_T}} \in H_\sigma \; \sigma \; \xi^{-1}(W) \text{ for all $n' < n$}\wedge\\
\quad (\isLinear{\src{\vsc_S}} \Rightarrow \\
\qquad\forall W' \future W, W_o, n' < n, \npair[n']{\stpair[.]{\vsc_S'}{\vsc'_T}} \in H_\sigma \; \sigma \; \xi^{-1}(W_o) \ldotp \\
\qquad \quad \npair[n']{\src{\vsc_S},\src{\vsc_S'},\vsc_T,\vsc_T'} \in \lrexj(W'\oplus W_o)) \wedge \\
\quad (\nonLinear{\src{\vsc_S}} \Rightarrow \\
\qquad \forall W' \future \purePart{W}, W_o, n' < n, \npair[n']{\stpair[.]{\vsc_S'}{\vsc'_T}} \in H_\sigma \; \sigma \; \xi^{-1}(W_o) \ldotp \\
\qquad \quad \npair[n']{\src{\vsc_S},\src{\vsc_S'},\vsc_T,\vsc_T'} \in \lrexj(W'\oplus W_o))

% This case was never used (?) so it is not necessary.
% \wedge \\
% \quad \npair[n']{\src{\vsc_S'},\src{\vsc_S},\vsc_T',\vsc_T} \in \lrexj(W' \oplus W_o)
\end{array}
\right\}\cup\\
\hspace{-2cm}\left\{ \npair{\left(\arraycolsep=0pt\array{l} \src{\seal{\sigma_\baddr,\sigma_\eaddr,\sigma}},\\ \seal{\sigma_\baddr,\sigma_\eaddr,\sigma} \endarray \right)}
\; \middle| \;
\begin{array}{l}
[\sigma_\baddr,\sigma_\eaddr] \mathrel{\#} (\gsigrets \cup \gsigcloss) \tand\\
\forall \sigma' \in [\sigma_\baddr,\sigma_\eaddr] \ldotp \exists r \in \dom(\pwheap) \ldotp \\
\quad \pwheap(r) = (\pure,\_,H_\sigma) \tand H_\sigma \; \sigma' \nequal (\lrv \circ \xi)
\end{array}
\right\} \cup \\
\hspace{-2cm}\left\{ \npair{\left(\arraycolsep=0pt\array{l} \src{\stkptr{\perm,\baddr,\eaddr,\aaddr}},\\ ((\perm,\linear),\baddr,\eaddr,\aaddr) \endarray \right)} \;\middle|\;
\begin{array}{l}
\begin{array}{r l l}
\perm \not\in \{\rx,\rwx\} \wedge\\
% \perm = \noperm & \Rightarrow & \npair{(\linear,\baddr,\eaddr)} \in \lrp(W) \wedge \\
\perm \in \readAllowed{} &\Rightarrow& \npair{[\baddr,\eaddr]} \in \stackReadCond{W} \wedge \\
\perm \in \writeAllowed{} &\Rightarrow& \npair{[\baddr,\eaddr]} \in \stackWriteCond{W}
\end{array}
\end{array}
\right\} \cup \\
\hspace{-2cm}\left\{ \npair{\left(\arraycolsep=0pt\array{l} \src{((\perm,\lin),\baddr,\eaddr,\aaddr)},\\ ((\perm,\lin),\baddr,\eaddr,\aaddr) \endarray \right)} \;\middle|\;
\begin{array}{l}
[b,e] \mathrel{\#} \ta \tand\\
\begin{array}{r l l }
% \perm = \noperm & \Rightarrow & \npair{(\lin,\baddr,\eaddr)} \in \lrp(W) \wedge \\
\perm \in \readAllowed{} &\Rightarrow& \npair{[\baddr,\eaddr]} \in \readCond{\lin,W} \wedge\\
\perm \in \writeAllowed{} &\Rightarrow& \npair{[\baddr,\eaddr]} \in \writeCond{\lin,W} \wedge\\
% we are excluding rwx pointers.
\perm \neq \rwx \wedge \\
% \perm = \rwx &\Rightarrow& \array[t]{l}\npair{(\{\rwx,\rx\},\baddr,\eaddr)} \in \execCond{\lin,W} \wedge \\
%                            \npair{(\baddr,\eaddr)} \in \xReadCond{\lin,W} \endarray\\
\perm = \rx &\Rightarrow& \array[t]{l}\npair{[\baddr,\eaddr]} \in \execCond{W} \wedge\\
\npair{[\baddr,\eaddr]} \in \xReadCond{W} \wedge \\
\lin = \normal \\ \endarray
\end{array}
\end{array}
\right\}
\end{array}
\]

\[
\lrvtrusted[\square,\gc](W) =
\begin{array}[t]{l}
\lrv(W)\cup \\
\left\{ \npair{\left(\arraycolsep=0pt\array{l} \src{\seal{\sigma_\baddr,\sigma_\eaddr,\sigma}},\\ \seal{\sigma_\baddr,\sigma_\eaddr,\sigma} \endarray \right)}
\; \middle| \;
\begin{array}{l}
\gc = (\ta,\stkb,\gsigrets,\gsigcloss)  \wedge \\
\exists r \in \dom(\pwheap) \ldotp \\
\quad \pwheap(r) \nequal \codereg{\sigrets,\sigcloss,\code,(\ta,\stkb,\gsigrets,\gsigcloss)} \wedge\\
\quad \dom(\code) \subseteq \ta \wedge [\sigma_\baddr,\sigma_\eaddr] \subseteq (\sigrets\cup\sigcloss) \wedge\\
\quad \sigrets \subseteq \gsigrets \wedge \sigcloss \subseteq \gsigcloss
\end{array}
\right\} \cup \\
\left\{ \npair{\left(\arraycolsep=0pt\array{l} \src{((\perm,\normal),\baddr,\eaddr,\aaddr)},\\ ((\perm,\normal),\baddr,\eaddr,\aaddr) \endarray \right)} \;\middle|\;
\begin{array}{l}
\perm \sqsubseteq \rx \wedge \\
\gc = (\ta,\stkb,\gsigrets,\gsigcloss)  \wedge \\
{} [\baddr,\eaddr] \subseteq \ta \wedge\\
\npair{[\baddr,\eaddr]} \in \xReadCond[\square,\gc]{W}
\end{array}
\right\}
\end{array}
\]

* $\lrvtrusted(W) \supseteq \lrv(W)$

* $\lrrtrusted(W) \supseteq \lrr(W)$

Follows easily by definition.

Note: the case for sub-$\rx$ capabilities in the trusted value relation allows for pointers to trusted code blocks.
Such pointers will not satisfy the read condition, which requires the standard region, which is defined in terms of the untrusted value relation.
Trusted code blocks contain trusted seal capabilities which do not satisfy the untrusted code relation.
An alternative might be to introduce a trust parameter to the readcondition and standard region and merge the case with the regular case for rx capabilities.

§.§ Permission based conditions

28-02-2018: These definitions need to be updated to fit with the new worlds.

\[
\addressable{\lin,W} =
\begin{cases}
\{ r \mid W(r) = (\pure,\_) \} & \text{if $\lin = \normal$} \\
\{ r \mid W(r) = (\spatialo,\_) \}  & \text{otherwise (i.e. $\lin = \linear$)} \\
\end{cases}
\]

\[
\readCond{\lin,W} = \left\{ \npair{A} \middle|
\begin{array}{l}
\exists S \subseteq \addressable{\lin, \pwheap} \ldotp \\
\quad \exists R : S \fun \powerset{\nats} \ldotp\\
\qquad \biguplus_{r\in S} R(r) \supseteq A \wedge\\
\qquad (\lin = \linear \Rightarrow \forall r\ldotp |R(r)|  = 1) \wedge\\
\qquad \forall r \in S \ldotp \pwheap(r).H \nsubeq \stdreg{R(r),\gc}{\pur}.H
\end{array}
\right\}
\]

RESOLVED: Make this condition require a set of adjacent regions. Check whether needed for the stack condition.
where $\iota_A$ is a standard region defined in Section <ref>.

\[
\stackReadCond{W} = \left\{ \npair{A} \middle|
\begin{array}{l}
\exists S \subseteq \addressable{\linear, \pwfree} \ldotp \\
\quad \exists R : S \fun \powerset{\nats} \ldotp\\
\qquad \forall r \in S \ldotp |R(r)| = 1\\
\qquad \biguplus_{r\in S} R(r) \supseteq A \wedge \\
\qquad \forall r \in S \ldotp \pwfree(r).H \nsubeq \stdreg{R(r),\gc}{\pur}.H
\end{array}
\right\}
\]

where $\iota_A$ is a standard region defined in Section <ref>.

\[
\xReadCond{W} = \left\{ \npair{A} \middle|
\begin{array}{l}
\exists r \in \addressable{\normal, \pwheap} \ldotp \\
\qquad \pwheap(r) \nequal \codereg{\_,\_,\code,\gc}\wedge\\
\qquad \dom(\code) \supseteq A
\end{array}
\right\}
\]

We say that a region $\iota = (\_,H,\_)$ is address stratified iff

\[
\begin{array}{l}
\forall n, \src{\ms_S},\ms_T,\src{\ms_S'},\ms_T',s,\hat{W}\ldotp \\
\quad \npair{\stpair{\ms}{\ms}}, \npair{\stpair[.]{\ms_S'}{\ms_T'}} \in H \; \hat{W} \wedge \\
\quad \dom(\src{\ms_S}) = \dom(\ms_T) = \dom(\src{\ms_S'}) = \dom(\ms_T') \\
\quad \Rightarrow \\
\qquad \forall \aaddr \in \dom(\ms_S) \ldotp \npair{(\src{\ms_S}\update{\aaddr}{\src{\ms_S'}(\aaddr)},\ms_T\update{\aaddr}{\ms_T'(\aaddr)})} \in H \; \hat{W}
\end{array}
\]

\[
\writeCond{\lin,W} = \left\{ \npair{A} \middle|
\begin{array}{l}
\exists S \subseteq \addressable{\lin, \pwheap} \ldotp \\
\quad \exists R : S \fun \powerset{\nats} \\
\qquad \biguplus_{r\in S} R(r) \supseteq A \wedge\\
\qquad (\lin = \linear \Rightarrow \forall r\ldotp |R(r)|  = 1) \wedge\\
\qquad \forall r \in S \ldotp \pwheap(r).H \nsupeq \stdreg{R(r),\gc}{\pur}.H \wedge\\
\qquad \quad \pwheap(r) \text{ is address-stratified}
\end{array}
\right\}
\]

where $\iota_A$ is a standard region defined in Section <ref>.

\[
\stackWriteCond{W} = \left\{ \npair{A}) \middle|
\begin{array}{l}
\exists S \subseteq \addressable{\linear, \pwfree} \ldotp \\
\quad \exists R : S \fun \powerset{\nats} \\
\qquad \biguplus_{r\in S} R(r) \supseteq A \wedge \\
\qquad \forall r \in S \ldotp |R(r)| = 1 \wedge \\
\qquad \forall r \in S \ldotp \pwfree(r).H \nsupeq \stdreg{R(r),\gc}{\pur}.H \wedge\\
\qquad \quad \pwfree(r) \text{ is address-stratified}
\end{array}
\right\}
\]

where $\iota_A$ is a standard region defined in Section <ref>.
22-6-2018: address-stratified is useless for length-one regions.
Note: this new version of execCond uses the expression relation for regular jumps since it expresses the validity of jumping to an address pointed to by an executable capability.

\begin{align*}
\execCond{W} &=
\left\{ \npair{A} \middle|
\begin{array}{l}
\forall n' < n, W' \future \purePart{W}, \aaddr \in [\baddr',\eaddr'] \subseteq A \ldotp\\
\quad \npair[n']{\stpair[.]{((\rx,\normal),\baddr',\eaddr',\aaddr)}{((\rx,\normal),\baddr',\eaddr',\aaddr)}} \in \lre(W')
\end{array}
\right\}
\end{align*}

§.§ Standard regions

Standard region:

\[
\stdreg{A,\gc}{v} \defeq (v,H_A^{\mathrm{std},\square} \; \gc) , v \in \{\spa,\spao\}
\]

for readability, we use $\spao$ short for $\spatialo$, $\spa$ short for $\spatial$, and $\pur$ as short for $\pure$.

\[
\stdreg{A,\gc}{\pur} \defeq (\pur,H_A^{\mathrm{std},\square} \; \gc, \lambda \_ \; \_ \ldotp \emptyset)
\]

where $H^{\mathrm{std},\square}_A$ is defined as follows:

\[
H_A^{\mathrm{std},\square} \; \gc \; \hat{W} \defeq \left\{ \npair{\ms_S,\ms_T} \middle|
\begin{array}{l}
\dom(\ms_S) = \dom(\ms_T) = A \wedge \\
\exists S : A \fun \World \ldotp \xi(\hat{W}) = \oplus_{\aaddr \in A} S(\aaddr) \wedge\\
\quad \forall \aaddr \in A \ldotp \npair{(\ms_S(\aaddr),\ms_T(\aaddr))} \in \lrv(S(\aaddr))
\end{array}
\right\}
\]

\[
\stareg[\stpair{\ms}{\ms},\gc]{v,\square} = (v,H^\mathrm{sta,\square}_{\stpair{\ms}{\ms}} \; \gc)
\]

\[
H^\mathrm{sta,\square}_{\stpair{\ms}{\ms}} \; \gc = \left\{ \npair{\stpair{\ms}{\ms}} \middle|
\begin{array}{l}
\exists S : \dom(\ms) \fun \World \ldotp \xi(W) = \oplus_{\aaddr \in \dom(\ms)} S(\aaddr) \wedge\\
\quad \forall \aaddr \in \dom(\ms) \ldotp \npair{(\ms_S(\aaddr),\ms_T(\aaddr))} \in \lrv(S(\aaddr))
\end{array}
\right\}
\]

\[
\codereg{\sigrets,\sigcloss,\code,\gc} \defeq (\pure,
H^\mathrm{code,\square} \; \sigrets \; \sigcloss \; \code \; \gc,
H^\mathrm{code}_\sigma \; \sigrets \; \sigcloss \; \code \; \gc)
\]

\begin{multline*}
H^\mathrm{code} \; \sigrets \; \sigcloss \; \code \; (\ta,\_,\gsigrets,\gsigcloss) \; \hat{W} =\\
\left\{\npair{\arraycolsep=0pt\left(\array{l}\code \uplus \mspad,\\ \code \uplus \mspad\endarray\right)} \middle|
\begin{array}{l}
\dom(\code) = [\baddr,\eaddr] \wedge \\
([\baddr - 1, \eaddr + 1] \subseteq \ta \wedge \sigrets \subseteq \gsigrets \wedge \sigcloss \subseteq \gsigcloss \wedge \trust = \trusted) \vee \\
\quad ([\baddr-1,\eaddr+1]\mathrel{\#} \ta \wedge \sigrets = \emptyset \wedge \trust =\untrusted) \wedge \\
\mspad = [\baddr-1 \mapsto 0] \uplus [\eaddr + 1 \mapsto 0]\wedge\\
\sigrets,\sigcloss,\ta \vdash_{\mathrm{comp-code}} \code \wedge\\
\forall a \in \dom(\code)\ldotp\\
\quad\npair{(\code(a),\code(a))} \in \lrvg{\trust}(\purePart{\xi(\hat{W})})
\end{array}
\right\}
\end{multline*}

\begin{multline*}
H^\mathrm{code,\square}_\sigma \; \sigrets \; \sigcloss \; \code \;
(\ta,\stkb) \; \sigma \; \hat{W}= \\
\begin{array}[t]{l}
\left\{
\begin{array}{l}
\left. \npair{\arraycolsep=0pt\left(\array{l}\retptrc(\baddr,\eaddr,\aaddr'+\calllen),\\((\rx,\normal),\baddr,\eaddr,\aaddr)\endarray\right)} \middle| \right. \\
\begin{array}{l}
\sigrets \subseteq \gsigrets \tand \\
\dom(\code) \subseteq \ta \tand\\
\decInstr{\code([\aaddr',\aaddr' + \calllen-1])} = \overline{\scall{\offpc,\offsigma}{r_1}{r_2}} \tand \\
\aaddr = \aaddr' + \retoffset \tand \\
\code(\aaddr'+\offpc) = \seal{\sigma_b,\sigma_e,\sigma_b} \tand \sigma = \sigma_b + \offsigma \in \sigrets \tand\\
\lbrack \aaddr',\aaddr' + \calllen -1 \rbrack \subseteq \lbrack \baddr, \eaddr \rbrack
\end{array}
\end{array}
\right\} \uplus \\
\left\{
\begin{array}{l}
\left. \npair{\arraycolsep=0pt\left(\array{l}\retptrd(\baddr,\eaddr),\\((\rw,\linear),\baddr,\eaddr,\baddr-1)\endarray\right)} \middle| \right. \\
\begin{array}{l}
\sigrets \subseteq \gsigrets \tand \\
\dom(\code) \subseteq \ta \tand\\
\exists r \in \addressable{\linear,\pwpriv[\xi(\hat{W})]} \ldotp \pwpriv[\xi(\hat{W})](r).H \nequal (\stareg[(\ms_S,\ms_T),(\ta,\stkb)]{\spao,\square}, \aaddr'+\calllen) \tand \\
\quad \dom(\ms_S) = \dom(\ms_T) = [\baddr,\eaddr] \tand\\
\quad \decInstr{\code([\aaddr',\aaddr' + \calllen-1])} = \overline{\scall{\offpc,\offsigma}{r_1}{r_2}} \tand \\
\quad \code(\aaddr'+\offpc) = \seal{\sigma_b,\sigma_e,\sigma_b} \tand \sigma = \sigma_b + \offsigma \in \sigrets
\end{array}
\end{array}
\right\} \\
\end{array}\\
\text{ if } \sigma \in \sigrets\\
\end{multline*}

\begin{multline*}
H^\mathrm{code,\square}_\sigma \; \sigrets \; \sigcloss \; \code \;
(\ta,\stkb) \; \sigma \; \hat{W}= \\
\left\{
\begin{array}{l}
\left. \npair{(\vsc, \vsc' )} \middle| \right. \\
\begin{array}{l}
(\dom(\code) \mathrel{\#} \ta \tand \npair{(\vsc,\vsc')} \in \lrv \; \xi(\hat{W})) \tor\\
(\dom(\code) \subseteq \ta \tand \sigcloss \subseteq \gsigcloss \tand \sigrets \subseteq \gsigrets \tand \\
\quad((\exec{\vsc} \wedge \npair{(\vsc,\vsc')} \in \lrvtrusted \; \xi(\hat{W})) \vee\\
\quad\ (\nonExec{\vsc} \wedge\npair{(\vsc,\vsc')} \in \lrv \; \xi(\hat{W}))))
\end{array}
\end{array}
\right\}\\
\text{ if } \sigma \in \sigcloss
\end{multline*}

§.§ Reasonable Components

Take a set of trusted addresses $\ta$ and sets of return pointer and closure seals $\gsigrets$ and $\sigcloss$.
We define that a word $w$ is reasonable up to $n$ steps in memory $\ms$ and
free stack $\ms_\stk$ if $n=0$
or the following implications hold.

* If $w = \seal{\sigma_\baddr,\sigma_\eaddr,\_}$, then
$[\sigma_\baddr,\sigma_\eaddr] \mathrel{\#} (\gsigrets \cup \gsigcloss)$

* If $w = ((\perm,\_),\baddr,\eaddr,\_)$, then $[\baddr,\eaddr] \# \dom(\ta)$

* If $w = \sealed{\sigma,\vsc}$ and $\sigma \not\in (\gsigrets\cup
\gsigcloss)$ then $\vsc$ is reasonable up to $n - 1$ steps.

* If $w = ((\perm,\_),\baddr,\eaddr,\_)$ and $\perm \in \readAllowed{}$
and $n > 0$, then $\ms(\aaddr)$ is reasonable up to $n - 1$ steps for all
$\aaddr \in ([\baddr,\eaddr] \setminus \ta)$

* If $w = \stkptr{\perm,\baddr,\eaddr,\_}$ and $\perm \in \readAllowed{}$
and $n > 0$, then $\ms_\stk(\aaddr)$ is reasonable up to $n - 1$ steps for
all $\aaddr \in [\baddr,\eaddr]$

We say that an execution configuration $\Phi$ is reasonable up to $n$ steps with $(\ta,\stkb,\gsigrets,\gsigcloss)$
iff for $n' \leq n$:

* Guarantee stack base address before call If

* $\Phi$ points to $\src{\scall{\offpc,\offsigma}{r_1}{r_2}}$ in $\ta$
for some $\src{r_1}$ and $\src{r_2}$

Then all of the following hold:

* $\src{\Phi}(\src{r_\stk}) =
\src{\stkptr{\_,\stkb,\_,\_}}$

* $r_1 \neq \rtmp{1}$

* $n' = 0$ or $\Phi(\pcreg) + \calllen$ behaves reasonably up to $n'-1$ steps

* Use return seals only for calls, use closure seals appropriately If

* $\src{\Phi}$ points to $\src{\tcseal{r_1}{r_2}}$ in $\ta$ and $\Phi(r_2) = \seal{\sigma_\baddr,\sigma_\eaddr,\sigma}$

Then one of the following holds:

* $\src{\Phi}$ is inside $\src{\scall{\offpc,\offsigma}{r_1'}{r_2'}}$ and $\sigma \in \gsigrets$

* $\sigma \in \gsigcloss$ and one of the following holds:

* $\exec{\Phi(r_1)}$ and $n' = 0$ or $\Phi(r_1)$ behaves reasonably up to $n' - 1$ steps.

* $\nonExec{\Phi(r_1)}$ and $n' = 0$ or $\Phi(r_1)$ is reasonable up to $n' - 1$ steps in memory $\Phi.\ms$ and free stack $\Phi.\ms_\stk$.

* Don't store private stuff... If

* $\src{\Phi}$ points to $\src{\tstore{r_1}{r_2}}$ in $\ta$, then

Then $n' = 0$ or $\Phi.\reg(r_2)$ is reasonable in memory $\Phi.\mem$ up to $n' -1$ steps.

* Don't leak private stuff... If

* $\Phi \step[\ta,\stkb] \Phi'$

Then one of the following holds:

* All of the following hold:

* $\Phi'.\reg(\pcreg) =
((\perm,\lin),\baddr,\eaddr,\aaddr')$ and $\Phi.\reg(\pcreg) =

* $\Phi$ does not point to $\src{\txjmp{r_1}{r_2}}$ for some $\src{r_1}$ and $\src{r_2}$

* $\Phi$ does not point to $\src{\scall{\offpc,\offsigma}{r_1}{r_2}}$ for some $\src{r_1}$ and $\src{r_2}$, $\offpc$, $\offsigma$

* $n' = 0$ or $\Phi'$ is reasonable up to $n'-1$ steps

* $\Phi$ points to $\src{\scall{\offpc,\offsigma}{r_1}{r_2}}$ for some $\src{r_1}$ and $\src{r_2}$

* $n' = 0$ or $\Phi.\reg(r)$ is reasonable in memory $\Phi.\mem$ and free stack $\Phi.\ms_\stk$ up to $n'-1$ steps for all $r \neq \pcreg$

* $\Phi$ points to $\src{\txjmp{r_1}{r_2}}$ for some $\src{r_1}$ and $\src{r_2}$

* $n' = 0$ or $\Phi.\reg(r)$ is reasonable in memory $\Phi.\mem$ and free stack $\Phi.\ms_\stk$ up to $n'-1$ steps for all $r \neq \pcreg$

For all $n' \le n$ if

* $\Phi$ is reasonable up to $n$ steps

* $\Phi$ is reasonable up to $n'$ steps

Follows from the definition.

We say that an executable capability $c =
((\perm,\normal),\baddr,\eaddr,\aaddr)$ behaves reasonably up to $n$ steps
if for any $\Phi$ such that

* $\Phi.\reg(\pcreg) = c$

* $\Phi.\reg(r)$ is reasonable up to $n$ steps in memory $\Phi.\mem$ and
free stack $\Phi.\ms_\stk$ for all $r \neq \pcreg$

* $\Phi.\mem$, $\Phi.\ms_\stk$ and $\Phi.\stk$ are all disjoint

We have that $\Phi$ is reasonable up to $n$ steps.

We say that a component
is reasonable if the following hold: For all $(s \mapsto \sealed{\sigma,\vsc}) \in
\overline{c_{\mathrm{export}}}$, with $\exec{\vsc}$, we have that $\vsc$
behaves reasonably up to any number of steps $n$.

We say that a component
$(\var{comp}_0,c_{\mathrm{main},c}, c_{\mathrm{main},d})$ is reasonable if $\var{comp}_0$ is reasonable.

If $\pwheap(r_\code) \nequal \codereg{\sigrets,\sigcloss,\code,\gc}$ and
$\memSat{\ms_S,\stk,\ms_\stk,\ms_T}{W}$, then there exists $W''$
and $W'$ such that $W = W' \oplus W''$ and
$\npair[n']{(\code,\code)} \in H^\mathrm{code} \; \sigrets \; \sigcloss \; \code \; \gc \; \xi^{-1}(W')$ for all $n' < n$

By definition of $\memSat{\ms_S,\stk,\ms_\stk,\ms_T}{W}$, we get that $W = W_{\var{stack}} \oplus W_{\var{free\_stack}} \oplus W_{\var{heap}}$ and

\begin{equation*}
\npair{(\overline{\sigma},\ms_S',\ms_\var{T,heap})} \in
\lrheap(\pwheap)(W_{\var{heap}})
\end{equation*}

for some $\ms_S' \subseteq \ms_S$ and $\ms_{T,\var{heap}}\subseteq \ms_T$.

By definition of $\npair{(\overline{\sigma},\ms_S',\ms_\var{T,heap})} \in
\lrheap(\pwheap)(W_{\var{heap}})$, we get an
$R_\ms : \dom(\activeReg{\pwheap}) \fun \MemSeg \times \MemSeg$ and $\exists R_W : \dom(\activeReg{\pwheap}) \fun \World$ such that

* $W' = \oplus_{r \in \dom(\activeReg{\pwheap})} R_W(r)$ and

* $\npair[n']{R_\ms(r_{\var{code}})} \in \pwheap(r_{\var{code}}).H \; \xi^{-1}(R_W(r_{\var{code}}))$ for all $n' < n$

Since $\pwheap(r_\code) \nequal \codereg{\sigrets,\sigcloss,\code,\gc}$, this implies that also $\npair[n']{R_\ms(r_{\var{code}})} \in  \codereg{\sigrets,\sigcloss,\code,\gc}.H~ \xi^{-1}(R_W(r_{\var{code}}))$, i.e. $\npair[n']{R_\ms(r_{\var{code}})} \in  H^\mathrm{code} \; \sigrets \; \sigcloss \; \code \; \gc~ \xi^{-1}(R_W(r_{\var{code}}))$ as required.

* $\gc = (\ta,\stkb,\gsigrets,\gsigcloss)$

* $\npair{(w,\_)} \in \lrv(W_w)$

* $\memSat{\ms_S,\stk,\ms_\stk,\_}{W_M}$

* $\purePart{W_w} \oplus \purePart{W_M}$ is defined

then, with respect to $\ta,\gsigrets,\gsigcloss$, $w$ is reasonable up to $n$ steps in memory $\ms_S$ and free stack $\ms_\stk$.

Induction over $n$.
For $n=0$ all words are reasonable.
For $n>0$, we need to prove four implications:

* If $w = \seal{\sigma_\baddr,\sigma_\eaddr,\_}$, then $[\sigma_\baddr,\sigma_\eaddr] \mathrel{\#} (\gsigrets \cup \gsigcloss)$:

This follows directly from $\npair{(w,\_)} \in \lrv(W_w)$ by definition of $\lrv$.

* If $w = ((\perm,\_),\baddr,\eaddr,\_)$, then $[\baddr,\eaddr] \# \ta$:

This follows directly from $\npair{(w,\_)} \in \lrv(W_w)$ by definition of $\lrv$.

* If $w = \sealed{\sigma,\vsc}$ and $\sigma \not\in (\gsigrets\cup \gsigcloss)$ then $\vsc$ is reasonable for $n-1$ steps:

By $\npair{(w,\_)} \in \lrv(W_w)$, we get some region $r \in \dom(\pwheap)$ and a set of return seals, a set of closure seals and a code memory: $\sigrets,\sigcloss,\mscode$ such that $\pwheap(r) = (\pure,\_,H_\sigma)$ and $H_\sigma \nequal H^\mathrm{code,\square}_\sigma \; \sigrets \; \sigcloss \; \mscode \; \gc)$ and $\npair[n']{(\sealed{\sigma,\vsc},\_)} \in H_\sigma \; \sigma \; \xi^{-1}(W)$ for all $n' < n$, so in particular for $n' = n-1$.
It follows easily from the above that also $\npair[n-1]{(\vsc,\_)} \in H^\mathrm{code,\square}_\sigma \; \sigrets \; \sigcloss \; \mscode \; \gc \; \sigma \; \xi^{-1}(W)$.

This gives us three cases for $\vsc$.
The two first cases $\vsc = \retptrd(\_,\_)$ and $\vsc = \retptrc(\_,\_,\_)$ are easily discharged as the reasonability definition puts no requirements on return pointers.
For the final case, $\sigma \in \sigcloss$ and either

* $\dom(\mscode) \mathrel{\#} \ta \tand \npair[n-1]{(\vsc,\_)} \in \lrv (W)$; or

* $\dom(\mscode) \subseteq \ta$, $\sigcloss \subseteq \gsigcloss$, and $\npair{(\vsc,\_)} \in \lrvg{\trust}(W)$ for $\trust = \untrusted$ iff $\nonExec{\vsc}$.

In the first case, the result follows from the induction hypothesis.
In the second case, we have a contradiction with $\sigma \not\in (\gsigrets\cup \gsigcloss)$.

* If $w = ((\perm,\_),\baddr,\eaddr,\_)$ and $\perm \in \readAllowed{}$ and $n > 0$, then $\ms_S(\aaddr)$ is reasonable up to $n - 1$ steps for all $\aaddr \in ([\baddr,\eaddr] \setminus \ta)$:

From $\npair{(w,\_)} \in \lrv(W_w)$, we get $\npair[n]{[b,e]} \in \readCond{\perm,\lin}$.

From $\npair[n]{[b,e]} \in \readCond{\perm,\lin}$ we get $S\subseteq \addressable{\lin,\pwheap}$ and $R : S \fun \powerset{\nats}$ such that

* $\biguplus_{r\in S} R(r) \supseteq [b,e]$

* $(\lin = \linear \Rightarrow \forall r\ldotp |R(r)|  = 1)$

* $\forall r \in S \ldotp \pwheap(r).H \nsubeq \stdreg{R(r),\gc}{\pur}.H$

given $a \in [b,e]$ we know by the above that there exists $r$ such that $a
\in R(r)$.

By $\memSat{\ms_S,\stk,\ms_\stk,\_}{W_M}$, we get $R_\ms : \dom(\activeReg{\pwheap}) \fun \MemSeg \times \MemSeg$ such that $\ms_S = \biguplus_{r \in \dom(\activeReg{\pwheap})} \pi_1(R_\ms(r))$.

Further, we get $R_W : \dom(\activeReg{\pwheap}) \fun \World$ such that $W' = \oplus_{r \in \dom(\activeReg{\pwheap})} R_W(r)$ and $\forall r \in \dom(\activeReg{\pwheap}) \ldotp \npair{R_\ms(r)} \in \pwheap(r).H \; \xi^{-1}(R_W(r))$.
For $W_M = W' \oplus W''$ for some $W''$.

In particular, we have $\npair{R_\ms(r)} \in \pwheap(r).H \; \xi^{-1}(R_W(r))$.

We know $\pwheap(r).H \nsubeq \stdreg{R(r),\gc}{\pur}.H$, so $\npair[n']{R_\ms(r)} \in \stdreg{R(r),\gc}{\pur}.H(\xi^{-1}(R_W(r)))$ for $n' < n$.
This gives us $\npair[n']{(\pi_1(R_\ms(r))(a),\_)} \in \lrv(R_W'(a))$ where $R_W' : [b,e] \fun \World$ such that $\biguplus_{a \in \dom(\pi_1(R_\ms(r)))} R_W'(a) = R_W(r)$.

At this point we apply the induction hypothesis which is possible as we have
the following:

* $\npair[n-1]{(\pi_1(R_\ms(r))(a),\_)} \in \lrv(R_W'(a))$

We get this by the above.

* $\memSat[n-1]{\ms_S,\stk,\ms_\stk,\_}{W_M}$

This follows by assumption and Lemma <ref>

* $\purePart{R_W'(a)} \oplus \purePart{W_M}$

Which follows by definition of $\purePart{}$ and the fact that $R_W'(a)$ is $W_M$ with part of its ownership, but $\purePart{}$ strips away the ownership making the two compatible.

which gives us that, with respect to $\ta,\gsigrets,\gsigcloss$, $\pi_1(R_\ms(r))(a)$ is reasonable up to $n-1$ steps in memory $\ms_S$ and free stack $\ms_\stk$.
Which is what we wanted as $\pi_1(R_\ms(r))(a) = \ms_S(a)$.

* If $w = \stkptr{\perm,\baddr,\eaddr,\_}$ and $\perm \in \readAllowed{}$ and $n > 0$, then $\ms_\stk(\aaddr)$ is reasonable up to $n - 1$ steps for all $\aaddr \in [\baddr,\eaddr]$:

This case is proven in the same way the previous case was.
The main difference is that the free part of the world is used instead of the heap part:

From $\npair{(w,\_)} \in \lrv(W_w)$ and $\perm \in \readAllowed{}$, we get $\npair{[b,e]} \in \stackReadCond{\perm}$.

From $\npair{[b,e]} \in \stackReadCond{\perm}$ we get $S\subseteq
\addressable{\linear,\pwfree}$ and $R : S \fun \powerset{\nats}$ such that

* $\biguplus_{r\in S} R(r) \supseteq [b,e]$

* $\forall r\ldotp |R(r)|  = 1$

* $\forall r \in S \ldotp \pwheap(r).H \nsubeq \stdreg{R(r),\gc}{\pur}.H$

given $a \in [b,e]$ we know by the above that there exists $r$ such that $a \in R(r)$.

By $\memSat{\ms_S,\stk,\ms_\stk,\_}{W_M}$, we get $R_\ms : \dom(\activeReg{\pwfree}) \fun \MemSeg \times \MemSeg$ such that $\ms_\stk = \biguplus_{r \in \dom(\activeReg{\pwfree})} \pi_1(R_\ms(r))$.

Further, we get $R_W : \dom(\activeReg{\pwfree}) \fun \World$ such that $W' = \oplus_{r \in \dom(\activeReg{\pwfree})} R_W(r)$ and $\forall r \in \dom(\activeReg{\pwfree}) \ldotp \npair{R_\ms(r)} \in \pwfree(r).H \; \xi^{-1}(R_W(r))$.
For $W_M = W' \oplus W''$ for some $W''$.

In particular, we have $\npair{R_\ms(r)} \in \pwfree(r).H \; \xi^{-1}(R_W(r))$.

We know $\pwfree(r).H \nsubeq \stdreg{R(r),\gc}{\pur}.H$, so $\npair[n']{R_\ms(r)} \in \stdreg{R(r),\gc}{\pur}.H(\xi^{-1}(R_W(r)))$ for $n' < n$.
This gives us $\npair[n']{(\pi_1(R_\ms(r))(a),\_)} \in \lrv(R_W'(a))$ where $R_W' : [b,e] \fun \World$ such that $\biguplus_{a \in \dom(\pi_1(R_\ms(r)))} R_W'(a) = R_W(r)$.

At this point we apply the induction hypothesis which is possible as we have
the following:

* $\npair[n-1]{(\pi_1(R_\ms(r))(a),\_)} \in \lrv(R_W'(a))$

We get this by the above.

* $\memSat[n-1]{\ms_S,\stk,\ms_\stk,\_}{W_M}$

This follows by assumption and Lemma <ref>

* $\purePart{R_W'(a)} \oplus \purePart{W_M}$

Which follows by definition of $\purePart{}$ and the fact that $R_W'(a)$ is $W_M$ with part of its ownership, but $\purePart{}$ strips away the ownership making the two compatible.

which gives us that, with respect to $\ta,\gsigrets,\gsigcloss$, $\pi_1(R_\ms(r))(a)$ is reasonable up to $n-1$ steps in memory $\ms_S$ and free stack $\ms_\stk$.
Which is what we wanted as $\pi_1(R_\ms(r))(a) = \ms_\stk(a)$.

* $\gc = (\ta,\stkb,\gsigrets,\gsigcloss)$

* $\npair{(\reg_S,\_)} \in \lrr(W_w)$

* $\memSat{\ms_S,\stk,\ms_\stk,\_}{W_M}$

* $\purePart{W_w} \oplus \purePart{W_M}$ is defined

then, with respect to $\ta,\gsigrets,\gsigcloss$,

* $\reg_S(r)$ is reasonable up to $n$ steps in memory $\ms_S$ and free stack $\ms_\stk$ for all $r \not\in \{\pcreg\}$

* $\ms_S$, $\ms_\stk$ and $\stk$ are all disjoint

We prove the two results separately:

* $\reg_S(r)$ is reasonable up to $n$ steps in memory $\ms_S$ and free stack $\ms_\stk$ for all $r \not\in \{\pcreg\}$:

We have that $W_w = \bigoplus_{r \in \RegName \setminus \{\pcreg\}} S(r)$ and $\npair{(\reg_S(r),\reg_T(r))} \in \lrv(S(r))$ for all $r \not\in \{\pcreg\}$.

For all $r \neq \pcreg$, we have that $\purePart{S(r)} \oplus \purePart{W_M}$ is defined by Lemmas <ref> and <ref>.

The result then follows directly from Lemma <ref>.

* $\ms_S$, $\ms_\stk$ and $\stk$ are all disjoint:

This follows from $\memSat{\ms_S,\stk,\ms_\stk,\_}{W_M}$.

* $\npair{(w,w')} \in \lrvg{\trusted}(W_w)$

* $w$ is reasonable up to $n$ steps in memory $\ms_S$ and free stack $\ms_\stk$, with respect to $\code,\ta,\gsigrets,\gsigcloss$.

* $n > 0$

* Theorem <ref> holds up to $n$ steps.
Note: I mention this assumption explicitly to avoid cyclic reasoning in the FTLR proof.

* $\npair{(w,w')} \in \lrv(W_w)$

Assume that $\npair{(w,w_T)} \in \lrvg{\trusted}(W_w)$

By definition of $\lrvg{\trusted}$, it is clear that also $\npair{(w,w_T)} \in \lrv(W_w)$, except in the following two cases:

* $w = \src{\seal{\sigma,\sigma_\baddr,\sigma_\eaddr}}$

* $w_T = \seal{\sigma,\sigma_\baddr,\sigma_\eaddr}$

* $r \in \dom(\pwheap)$

* $\pwheap(r) \nequal \codereg{\sigrets,\sigcloss,\code,(\ta,\stkb,\gsigrets,\gsigcloss)}$

* $\dom(\code) \subseteq \ta$

* $[\sigma_\baddr,\sigma_\eaddr] \subseteq (\sigrets\cup\sigcloss)$

* $\sigrets \subseteq \gsigrets$

* $\sigcloss \subseteq \gsigcloss$

By definition of reasonability, we get immediately that $[\sigma_b,\sigma_e]\mathrel{\#} (\gsigrets\cup \gsigcloss)$, contradicting the last three facts above.

* $w = \src{((\perm,\normal),\baddr,\eaddr,\aaddr)}$,

* $w_T =

* $\perm \sqsubseteq \rx$

* $\gc = (\ta,\stkb,\gsigrets,\gsigcloss)$

* $\npair{[\baddr,\eaddr]} \in \xReadCond[\square,\gc]{W}$

If $\perm = \noperm$, then $\npair{(w,w_T)} \in \lrv(W_w)$ follows directly.

If $\perm \neq \noperm$, then by definition of reasonability, we get immediately that $[b,e] \mathrel{\#} \ta$.

By definition of $\lrv$, it suffices to show that $\npair{[b,e]} \in \readCond{\normal,W}$ and $\npair{[b,e]} \in \execCond{\normal,W}$.
The former follows directly from Lemma <ref>.
The latter follows by Theorem <ref>, Lemmas <ref> and <ref> and definition of $\execCond{}$.

§.§ Fundamental Theorem of Logical Relations

For all $n,W,\lin,\baddr,\eaddr,\aaddr$,

* $\npair{[\baddr,\eaddr]} \in \xReadCond{W}$

and one of the following sets of requirements holds:

* $[\baddr,\eaddr] \subseteq \ta$

* $({((\rx,\normal),\baddr,\eaddr,\aaddr)}$ behaves reasonably up to $n$ steps.

* $[\baddr,\eaddr] \mathrel{\#} \ta$

\[
\npair{\left(\arraycolsep=0pt\array{l}((\rx,\normal),\baddr,\eaddr,\aaddr),\\
((\rx,\normal),\baddr,\eaddr,\aaddr)\endarray\right)} \in \lre(W)
\]

Note: we don't require the readcondition in the trusted case because trusted code pointers point to trusted code blocks which may require seals for trusted seals which are not in the untrusted value relation.

* $\npair{(w_1,w_1')} \in \lre(W_1)$ or ($\nonExec{w_1}$ and $\nonExec{w_1'}$)

* $w_1 \neq \retptrc(\_)$

* $\npair{(w_2,w_2')} \in \lrv(W_2)$ or ($\exec{w_2}$ and $\exec{w_2'}$)

* $\npair{((w_1,w_2),(w_1',w_2'))} \in \lrexj(W_1 \oplus W_2)$

Take $n' \leq n$, $\src{\reg_S}, \reg_T, \src{\ms_S}, \ms_T, \src{\ms_\stk}, \src{\stk}$, $W_\lrrs , W_\lrm$ and assume

* $\npair[n']{\stpair{\reg}{\reg}} \in \lrr(\{\rdata\}) (W_\lrrs )$

* $\memSat[n']{\stpair[.]{\ms_S,\stk,\ms_\stk}{\ms_T}}{W_\lrm}$

* $\Phi_S = \src{(\ms_S,\reg_S,\stk, \ms_\stk)}$

* $\Phi_T = (\ms_T,\reg_T)$

* $W_1 \oplus W_2 \oplus W_\lrrs \oplus W_\lrm$ is defined

Then we need to prove that for $\Phi_S'$,$\Phi_T'$

* $\Phi_S' = \xjumpResult{w_1}{w_2}{\Phi_S}$

* $\Phi_T' = \xjumpResult{w_1'}{w_2'}{\Phi_T}$

* $\npair[n']{\left(\Phi_S', \Phi_T' \right)}\in \lro$

Using the fact that $w_1 \neq \retptrc(\_)$, we know by definition of $\xjumpResult{w_1}{w_2}{\Phi_S}$ that we must be in one of the following two cases:

* $w_1 \neq \retptrc(\_)$, $w_2 \neq \retptrd(\_)$, $\nonExec{w_2}$ and
$\Phi_S' = \Phi_S \updReg{\pcreg}{w_1}\updReg{\rdata}{w_2}$.

From $\nonExec{w_2}$ and $\npair{(w_2,w_2')} \in \lrv(W_2)$ or $\exec{w_2}$, it follows that also $\nonExec{w_2'}$ and $\Phi_T' = \Phi_T \updReg{\pcreg}{w_1'}\updReg{\rdata}{w_2'}$

We can now combine $\npair[n']{\stpair{\reg}{\reg}} \in \lrr(\{\rdata\}) (W_\lrrs )$ and $\npair{(w_2,w_2')} \in \lrv(W_2)$ into $\npair[n']{(\reg_S\update{\rdata}{w_2},\reg_T\update{\rdata}{w_2'})} \in \lrr (W_\lrrs \oplus W_2)$, using Lemmas <ref>, <ref>, <ref>, and <ref>.

With our other assumptions above, $\npair{(w_1,w_1')} \in \lre(W_1)$ then gives us that $\npair[n']{(\Phi_S',\Phi_T')}\in \lro$, as required.
On the other hand, if $\nonExec{w_1}$ and $\nonExec{w_1'}$, then $\Phi_S' \step[\gc] \failed$ and $\Phi_T' \step \failed$ and the result follows by definition of $\lrol$ and $\lror$.

* Otherwise: $\Phi_S' = \failed$.

From $w_1 \neq \retptrc(\_)$ and ($\npair{(w_2,w_2')} \in \lrv(W_2)$ or ($\exec{w_2}$ and $\exec{w_2'}$)), the only way we can get to this case is that $\exec{w_2}$ and $\exec{w_2'}$.

It follows that $\Phi_T' = \failed$.

The result follows by definition of $\lrol$ and $\lror$.

* $\npair{(w_1,w_1')} \in \lrv(W_1)$

* $\npair[n']{(w_2,w_2')} \in \lrv(W_2)$ or ($\exec{w_2}$ and $\exec{w_2'}$)

* $n' < n$

* $\npair[n']{((w_1,w_2),(w_1',w_2'))} \in \lrexj(W_1 \oplus W_2)$

By Lemma <ref>, it suffices to prove the following:

* $\npair[n']{(w_1,w_1')} \in \lre(W_1)$ or ($\nonExec{w_1}$ and $\nonExec{w_1'}$)

* $w_1 \neq \retptrc(\_)$.

The latter follows immediately from $\npair{(w_1,w_1')} \in \lrv(W_1)$ by definition.
It also follows that either ($\nonExec{w_1}$ and $\nonExec{w_1'}$) or $w_1 = w_1' = ((\perm,\normal),\baddr,\eaddr,\aaddr)$ and $\npair{[\baddr,\eaddr]} \in \execCond{W_1}$.
In the latter case, it follows by definition of $\execCond{}$ that $\npair[n']{(w_1,w_1')} \in \lre(W_1)$ as required.

§.§ Related components

\begin{align*}
\lrcomp(W) &=
\left\{\begin{aligned}
&\npair{\var{comp},\var{comp}} \;\mid \;\\
&\qquad\var{comp} = (\mscode,\msdata,\overline{a_{\mathrm{import}} \mapsfrom s_{\mathrm{import}}},\overline{s_{\mathrm{export}} \mapsto w_{\mathrm{export}}},\sigrets,\sigcloss) \tand \\
&\qquad\text{For all } W' \future W \ldotp \\
&\qquad\quad\text{If } \overline{\npair[n']{(w_{\mathrm{import}},w_{\mathrm{import}})}} \in \lrv(\purePart{W'}) \text{ for all $n' < n$}\\
&\qquad\quad\text{and } \msdata' = \msdata{}[\overline{a_{\mathrm{import}} \mapsto w_{\mathrm{import}}}] \\
&\qquad\quad\text{then } \npair{(\sigrets\uplus\sigcloss,\mscode\uplus \msdata', \mscode\uplus\msdata')} \in \lrheap(\pwheap)(W') \tand\\
&\qquad\quad\overline{\npair{(w_{\mathrm{export}},w_{\mathrm{export}})}} \in \lrv(\purePart{W'})
\end{aligned}
\right\}\\
&\cup \left\{
\begin{multlined}
\npair{(\var{comp}_0,c_{\mathrm{main},c}, c_{\mathrm{main},d}),(\var{comp}_0,c_{\mathrm{main},c}, c_{\mathrm{main},d})} \;\mid \;\\
\npair{(\var{comp}_0,\var{comp}_0)} \in \lrcomp(W) \tand\\
\{(\_ \mapsto c_{\mathrm{main},c}),(\_ \mapsto c_{\mathrm{main},d})\} \subseteq \overline{w_{\mathrm{export}}}
\end{multlined}
\right\}
\end{align*}

* $\npair{(\var{comp}_1,\var{comp}_1)} \in \lrcomp(W_1)$

* $\npair{(\var{comp}_2,\var{comp}_2)} \in \lrcomp(W_2)$

* $\npair{(\var{comp}_1 \bowtie \var{comp}_2,\var{comp}_1\bowtie\var{comp}_2)} \in \lrcomp(W_1 \uplus W_2)$.

First consider the case where one of the two pairs of components have a pair of “main” capabilities.
By the definition of $\lrcomp$, these capabilities have to be part of that components' export list.
It is then easy to see that the other component cannot have “main” capabilities (otherwise linking is not defined) and it is sufficient to prove the result for the underlying components (without the “main” capabilities).
Therefore, we can restrict ourselves to the case where both pairs of components are of the form $\var{comp}_0$, i.e. no “main” capabilities.

By definition of $\bowtie$, we have that the following hold:

* $\var{comp}_1 = (\mscode[1], \msdata[1], \overline{\var{import}_1}, \overline{\var{export}_1}, \sigrets[1], \sigcloss[1],A_{\linear,1})$

* $\var{comp}_2 = (\mscode[2], \msdata[2], \overline{\var{import}_2}, \overline{\var{export}_2}, \sigrets[2], \sigcloss[2],A_{\linear,2})$

* $\var{comp}_3 = (\mscode[3], \msdata[3], \overline{\var{import}_3}, \overline{\var{export}_3}, \sigrets[3], \sigcloss[3],A_{\linear,3})$

* $\mscode[3] = \mscode[1] \uplus \mscode[2]$

* $\msdata[3] = (\msdata[1] \uplus \msdata[2])[a \mapsto w \mid (a \mapsfrom s) \in (\overline{\var{import}_1} \cup \overline{\var{import}_2}), (s \mapsto w) \in \overline{\var{export}}_3]$

* $\overline{\var{export}_3} = \overline{\var{export}_1} \cup \overline{\var{export}_2}$

* $\overline{\var{import}_3} = \{ a \mapsfrom s \in (\overline{\var{import}_1} \cup \overline{\var{import}_2}) \mid s \mapsto \_ \not\in \overline{\var{export}_3} \}$

* $\sigrets[3] = \sigrets[1] \uplus \sigrets[2]$

* $\sigcloss[3] = \sigcloss[1] \uplus \sigcloss[2]$

* $A_{\linear,3} = A_{\linear,1} \uplus A_{\linear,2}$

* $\dom(\mscode[3]) \mathrel{\#} \dom(\msdata[3])$

* $\sigrets[3] \mathrel{\#} \sigcloss[3]$

Now take $W' \future (W_1\uplus W_2)$ and assume that $\overline{\npair[n']{(w_{\mathrm{import},3},w_{\mathrm{import},3})}} \in \lrv(\purePart{W'})$ for all $n' < n$.
Take $\overline{\var{import}_3} = \overline{a_{\mathrm{import},3} \mapsfrom s_{\mathrm{import},3}}$.
Take $\msdata[3]' = \msdata[3]{}[\overline{a_{\mathrm{import},3} \mapsto w_{\mathrm{import}}}]$
Then it remains to show that

\begin{equation*}
\npair{(\sigrets[3]\uplus\sigcloss[3],\mscode[3]\uplus \msdata[3]', \mscode[3]\uplus\msdata[3]')} \in \lrheap(\pwheap[(W_1\uplus W_2)])(W')
\end{equation*}

\begin{equation*}
\overline{\npair{(c_{\mathrm{export},3},c_{\mathrm{export},3})}} \in \lrv(\purePart{W'})
\end{equation*}

We do this by complete induction on $n$, so that we can assume that $\overline{\npair[n']{(c_{\mathrm{export},3},c_{\mathrm{export},3})}} \in \lrv(\purePart{W'})$ for all $n' < n$.

First, note that

\begin{align*}
\msdata[3]' &= \msdata[3]{}[\overline{a_{\mathrm{import},3} \mapsto w_{\mathrm{import}}}]\\
&=(\msdata[1] \uplus \msdata[2])[a \mapsto w \mid (a \mapsfrom s) \in (\overline{\var{import}_1} \cup \overline{\var{import}_2}), (s \mapsto w) \in \overline{\var{export}}_3]\\
&\hspace{4cm}[\overline{a_{\mathrm{import},3} \mapsto w_{\mathrm{import}}}]\\
&= \msdata[1][a \mapsto w \mid (a \mapsfrom s) \in \overline{\var{import}_1}, (s \mapsto w) \in \overline{\var{export}}_2][\overline{a_{\mathrm{import},3} \mapsto w_{\mathrm{import},3}} \mid \overline{a_{\mathrm{import},3}\mapsfrom \_} \in \overline{\var{import}_1}]\\
&\uplus \msdata[2][a \mapsto w \mid (a \mapsfrom s) \in \overline{\var{import}_2}, (s \mapsto w) \in \overline{\var{export}}_1][\overline{a_{\mathrm{import},3} \mapsto w_{\mathrm{import},3}} \mid \overline{a_{\mathrm{import},3}\mapsfrom \_} \in \overline{\var{import}_2}]\\
&= \msdata[1]' \uplus \msdata[2]'
\end{align*}

First, we prove that for all substituted values $w$ in the equations above, we have that

\begin{equation*}
\overline{\npair[n']{(w,w)}} \in \lrv(\purePart{W'})
\end{equation*}

for all $n' < n$.
We know by assumption that this is true for the $\overline{w_{\mathrm{import}}}$ such that $\overline{a_{\mathrm{import},3}\mapsfrom \_} \in \overline{\var{import}_1}$ or $\overline{a_{\mathrm{import},3}\mapsfrom \_} \in \overline{\var{import}_2}$.
On the other hand, we know by induction that this is true for the $w$ such that $(s \mapsto w) \in \overline{\var{export}}_1$ or $(s \mapsto w) \in \overline{\var{export}}_2$.

Then, it follows from our assumptions ($\npair{(\var{comp}_1,\var{comp}_1)} \in \lrcomp(W_1)$ and $\npair{(\var{comp}_2,\var{comp}_2)} \in \lrcomp(W_2)$), and using Lemma <ref> that

\begin{align*}
\npair{(\sigrets[1]\uplus\sigcloss[1],\mscode[1]\uplus \msdata[1]', \mscode[1]\uplus\msdata[1]')} &\in \lrheap(\pwheap[W_1])(W')\\
\npair{(\sigrets[2]\uplus\sigcloss[2],\mscode[2]\uplus \msdata[2]', \mscode[2]\uplus\msdata[2]')} &\in \lrheap(\pwheap[W_2])(W')
\end{align*}

It follows by Lemma <ref> that

\begin{equation*}
\npair{(\sigrets[3]\uplus\sigcloss[3],\mscode[3]\uplus \msdata[3]', \mscode[3]\uplus\msdata[3]')} \in \lrheap(\pwheap[(W_1\uplus W_2)])(W')
\end{equation*}

Finally, for each

\begin{equation*}
\npair{(c_{\mathrm{export}},c_{\mathrm{export}})} \in \overline{\npair{(c_{\mathrm{export},3},c_{\mathrm{export},3})}}
\end{equation*}

we have that $\npair{(c_{\mathrm{export}},c_{\mathrm{export}})}$ is either in $\overline{\npair{(c_{\mathrm{export},1},c_{\mathrm{export},1})}}$ or $\overline{\npair{(c_{\mathrm{export},2},c_{\mathrm{export},2})}}$.
By unfolding $\npair{(\var{comp}_1,\var{comp}_1)} \in \lrcomp(W_1)$ and $\npair{(\var{comp}_2,\var{comp}_2)} \in \lrcomp(W_2)$ and using Lemma <ref>, this follows from the results above.

§.§ FTLR for components

* $\dom(\code) \mathrel{\#} \ta$

* $\sigma \in \sigcloss$

\begin{equation*}
H^\mathrm{code,\square}_\sigma \; \sigrets \; \sigcloss \; \code \; (\ta,\stkb) \; \sigma \nequal \lrv
\end{equation*}

Follows easily by definition.

* $\dom(\mscode) \mathrel{\#} \ta$

then $\codereg{\sigrets,\sigcloss,\mscode,\gc}.H \nsubeq \stdreg{\dom(\mscode),\gc}{\pur}.H$

Take $\hat{W}$, then we need to prove that

\begin{equation*}
H^\mathrm{code}\;\sigrets\;\sigcloss\;\mscode\;\gc \; \hat{W} \nsubeq H_{\dom(\mscode)}^{\mathrm{std},\square}\;\hat{W}
\end{equation*}

So take $\npair{\ms_S,\ms_T} \in H^\mathrm{code}\;\sigrets\;\sigcloss\;\mscode\;\gc \; \hat{W}$, then we know that

* $\ms_S = \ms_T = \mscode\uplus\mspad$

* $\dom(\mscode) =[\baddr,\eaddr]$

* $[\baddr-1,\eaddr+1] \subseteq \ta \vee ([\baddr-1,\eaddr+1]\mathrel{\#} \ta \wedge \sigrets = \emptyset)$, but we know that $\dom(\mscode) \mathrel{\#} \ta$, so we get that $\sigrets = \emptyset$.

* For all $a \in \dom(\code)$, $\npair{(\code(a),\code(a))} \in \lrv(\purePart{\xi(\hat{W})})$

By definition of $H_{\dom(\mscode)}^{\mathrm{std},\square}\;\hat{W}$, we need to prove that

* $\dom(\mscode) = \dom(\mscode) = \dom(\mscode)$

* there exists a $S : \dom(\mscode) \fun \World$ with $\xi(\hat{W}) = \oplus_{\aaddr\in\dom(\mscode)} S(\aaddr)$ and for all $\aaddr \in \dom(\mscode)$, we have that $\npair{(\ms_S(\aaddr),\ms_T(\aaddr))} \in \lrv(S(\aaddr))$

We take $S$ to map every address to $\purePart{\hat{W}}$, except for a single one that we map to $\hat{W}$.
The result then follows by Lemmas <ref>, <ref> and <ref> and the above fact that for all $a \in \dom(\code)$, $\npair{(\code(a),\code(a))} \in \lrv(\purePart{\xi(\hat{W})})$.

* $\dom(\mscode) \mathrel{\#} \ta$

* $\pwheap(r_{\mathrm{code}}) = \codereg{\sigrets,\sigcloss,\mscode,\gc}$

* $A \subseteq \dom(\mscode)$,

we have that $\npair{A} \in \readCond{\normal,W}$.

Follows by defintion of $\readCond{}$ from Lemma <ref>.

* $A \mathrel{\#} \ta$

* $\npair{A} \in \xReadCond{W}$

we have that $\npair{A} \in \readCond{\normal,W}$.

Follows by defintion of $\readCond{}$ and $\xReadCond{}$ from Lemma <ref>.

* $\emptyset\neq\dom(\mscode) \mathrel{\#} \ta$

* $\sigma \in \sigcloss$

then $\codereg{\sigrets,\sigcloss,\mscode,\gc}.H_\sigma \sigma \nequal \lrv$ for all $n$

The result follows easily by definition of $\codereg{}$ and $H^\mathrm{code,\square}_\sigma$.

* If $\npair{A} \in \readCond{\normal,W}$, then $\npair{A} \in \readCond{}(\normal, \purePart{W} )$.

* If $\npair{A} \in \writeCond{\normal,W}$, then $\npair{A} \in \writeCond{}(\normal,\purePart{W})$

* If $\npair{A} \in \execCond{W}$, then $\npair{A} \in \execCond{}(\purePart{W})$

* If $\npair{A} \in \xReadCond{W}$, then $\npair{A} \in \xReadCond{}(\purePart{W} )$.

* If $\npair{(w_1,w_2)} \in \lrv(W)$ and ($\nonLinear{w_1}$ or
$\nonLinear{w_2}$), then
$\npair{(w_1,w_2)} \in \lrv(\purePart{W})$.

Follows easily by inspecting the definitions of $\lrv$, $\readCond[]{}$, $\addressable{}$, $\writeCond[]{}$, $\execCond[]{}$ and $\xReadCond[]{}$ and using Lemma <ref>.

* If $\npair{A} \in \readCond{\lin,W}$  and $\emptyset \neq A' \subseteq A$, then
$\npair{A'} \in \readCond{\lin,W}$.

* If $\npair{A} \in \writeCond{\lin,W}$  and $\emptyset \neq A' \subseteq A$, then
$\npair{A'} \in \writeCond{\lin,W}$.

* If $\npair{A} \in \xReadCond{W}$  and $A' \subseteq A$, then
$\npair{A'} \in \xReadCond{W}$.

* If $\npair{A} \in \execCond{W}$  and $\emptyset \neq A' \subseteq A$, then
$\npair{A'} \in \execCond{W}$.

Follows easily from the definitions.
In the case for $\execCond{}$ where $\lin = \linear$, we have a partition of the world into $W = \oplus_{a \in A} W_a(a)$ that we need to convert into a partition $W = \oplus_{a \in A'} W_a'(a)$.
It suffices construct new $W_a'$ by taking $W_a$ but adding $\oplus_{a\in(A\setminus A')}$ to an $W_a(a)$ for an arbitrary $a \in A'$ to make this work.

If $A = [\baddr_1,\eaddr_1] \uplus [\baddr_2,\eaddr_2]$, then

* If $\npair{A} \in \readCond{\lin,W}$, then there exists $W_1, W_2$ such that $W = W_1\oplus W_2$ such that $\npair{[\baddr_1,\eaddr_1]} \in \readCond{\lin,W_1}$ and $\npair{[\baddr_2,\eaddr_2]} \in \readCond{\lin,W_2}$.

* If $\npair{A} \in \writeCond{\lin,W}$, then there exists $W_1, W_2$ such that $W = W_1\oplus W_2$ such that $\npair{[\baddr_1,\eaddr_1]} \in \writeCond{\lin,W_1}$ and $\npair{[\baddr_2,\eaddr_2]} \in \writeCond{\lin,W_2}$.

* If $\npair{A} \in \execCond{W}$, then there exists $W_1, W_2$ such that $W = W_1\oplus W_2$ such that $\npair{[\baddr_1,\eaddr_1]} \in \execCond{W_1}$ and $\npair{[\baddr_2,\eaddr_2]} \in \execCond{W_2}$.

If $\lin = \normal$, then Lemma <ref> tells us that it suffices to consider pure worlds $W = \purePart{W}$ and Lemma <ref> tells us that then $W = W \oplus W$.
The results then follow from the previous Lemma <ref>.

As such, we can limit ourselves to the case where $\lin = \linear$.

The read- and write-conditions then require separate islands for each individual address in $A$ and we can distribute ownership of those islands according to whether those addresses are in $[\baddr_1,\eaddr_1]$ or $[\baddr_2,\eaddr_2]$, i.e. make the island $\pwheap(r)$ with $R(r) = \{a\}$ $\spatialo$ in $W_1$ and $\spatial$ in $W_2$ if $a \in [\baddr_1,\eaddr_1]$ and vice versa.
It is then easy to check that our results hold.

For the execute condition, we get a partition of the world into $W = \oplus_{a \in A} W_a(a)$ and we can define $W_1 = \oplus_{a\in[\baddr_1,\eaddr_1]} W_a(a)$ and likewise for $W_2$.
The results then follow easily from the definitions.

* $[\baddr,\eaddr] = [\baddr_1,\eaddr_1] \uplus [\baddr_2,\eaddr_2]$

* $[\baddr,\eaddr]\mathrel{\#} \ta$

* $W_1\oplus W_2$ is defined.

* If $\npair{[\baddr_1,\eaddr_1]} \in \readCond{\lin,W_1}$ and $\npair{[\baddr_2,\eaddr_2]} \in \readCond{\lin,W_2}$, then $\npair{[\baddr,\eaddr]} \in \readCond{\lin,W_1 \oplus W_2}$

* If $\npair{[\baddr_1,\eaddr_1]} \in \writeCond{\lin,W_1}$ and $\npair{[\baddr_2,\eaddr_2]} \in \writeCond{\lin,W_2}$, then $\npair{[\baddr,\eaddr]} \in \writeCond{\lin,W_1 \oplus W_2}$.

* If $\npair{[\baddr_1,\eaddr_1]} \in \execCond{W_1}$ and $\npair{[\baddr_2,\eaddr_2]} \in \execCond{W_2}$, then $\npair{[\baddr,\eaddr]} \in \execCond{W_1 \oplus W_2}$.

* $[\baddr,\eaddr] = [\baddr_1,\eaddr_1] \uplus [\baddr_2,\eaddr_2]$

* $W_1\oplus W_2 \oplus W_M$ is defined.

* $\memSat{\ms_S,\stk,\ms_\stk,\ms_T}{W_M}$

* If $\npair{[\baddr_1,\eaddr_1]} \in \xReadCond{\lin,W_1}$ and
$\npair{[\baddr_2,\eaddr_2]} \in \xReadCond{\lin,W_2}$, then
$\npair{[\baddr,\eaddr]} \in \xReadCond{\lin,W_1 \oplus W_2}$

If $[\baddr,\eaddr] = [\baddr_1,\eaddr_1] \uplus [\baddr_2,\eaddr_2]$, then

* If $\npair{[\baddr_1,\eaddr_1]} \in \stackReadCond{W_1}$ and $\npair{[\baddr_2,\eaddr_2]} \in \stackReadCond{W_2}$, then $\npair{[\baddr,\eaddr]} \in \stackReadCond{W_1 \oplus W_2}$

* If $\npair{[\baddr_1,\eaddr_1]} \in \stackWriteCond{W_1}$ and $\npair{[\baddr_2,\eaddr_2]} \in \stackWriteCond{W_2}$, then $\npair{[\baddr,\eaddr]} \in \stackWriteCond{W_1 \oplus W_2}$.

The results for $\readCond{}$, $\writeCond{}$, $\stackReadCond{}$ and $\stackWriteCond{}$ follow by taking the union of the two sets $S$, and the union of $R$ for every $r$.

The result for $\execCond{}$ follows easily by definition and using Lemmas <ref> and <ref>.

For $\xReadCond{}$, we get $r_i \in \addressable{\normal,W_i}$ such that $\pwheap[W_i](r_i) \nequal \codereg{\_,\_,\code_i,\gc}$ such that $\dom(\code_i)\supseteq [\baddr_i,\eaddr_i]$.
From $\memSat{\ms_S,\stk,\ms_\stk,\ms_T}{W_M}$, it follows that $\code_i = [\baddr_i',\eaddr_i']$ and if $r_1 \neq r_2$, then $[\baddr_1'-1,\eaddr_1+1] \mathrel{\#} [\baddr_2'-1,\eaddr_2'+1]$.
Because $[\baddr,\eaddr] = [\baddr_1,\eaddr_1] \uplus [\baddr_2,\eaddr_2]$ and $[\baddr_i',\eaddr_i'] = \dom(\code_i)\supseteq [\baddr_i,\eaddr_i]$, we can derive that $r_1= r_2$.
The result then follows by definition of $\xReadCond{}$.

* $\npair{\dom(\mscode)}\in\xReadCond{W}$

* ($\trust = \untrusted$ and $\dom(\mscode \mathrel{\#} \ta)$) or ($\trust = \trusted$ and $\dom(\mscode) \subseteq \ta$)

* $w = ((\rx,\normal),\baddr,\eaddr,\aaddr)$

* $[\baddr,\eaddr]\subseteq \dom(\mscode)$

then $\npair{(w,w)} \in \lrvg{\trust}(W)$.

We distinguish two cases:

* $\trust = \untrusted$ and $\dom(\mscode) \mathrel{\#} \ta$:
By definition of $\lrv(W)$, it suffices to show that:

* $[b,e] \mathrel{\#} \ta$: follows directly from $[\baddr,\eaddr]\subseteq \dom(\mscode)$ and $\dom(\mscode) \mathrel{\#} \ta$.

* $\npair{[b,e]}\in\readCond{\normal,W}$:
this follows from Lemma <ref>.

* $\npair{[b,e]}\in\xReadCond{W}$:
by assumption and Lemma <ref>.

* $\npair{[b,e]}\in\execCond{W}$:
take $n' < n$, $W' \future \purePart{W}$, $\aaddr' \in [\baddr',\eaddr'] \subseteq [\baddr,\eaddr]$ and $w' = ((\rx,\normal),\baddr',\eaddr',\aaddr')$.
Then we need to show that $\npair[n']{(w',w')} \in \lre(W')$.
This now follows immediately from the (regular) FTLR (Theorem <ref>), using the two above points, Lemma <ref> and Lemma <ref>.

* $\trust = \trusted$ and $\dom(\mscode) \subseteq \ta$:
By definition of $\lrvg{\trusted}(W)$ and Lemma <ref> with the assumption that $\npair{\dom(\mscode)}\in\xReadCond{W}$.

\begin{equation*}
\sigrets,\sigrets[\mathrm{owned}],\sigcloss,\ta\vdash_{\mathrm{comp-code}} w
\end{equation*}

* $\sigrets \subseteq \gsigrets$ and $\sigcloss \subseteq \gsigcloss$

* $\pwheap(r_{\mathrm{code}}) = \codereg{\sigrets,\sigcloss,\mscode,\gc}$

* ($\dom(\mscode) \mathrel{\#} \ta$ and $\trust = \untrusted$) or ($\dom(\mscode) \subseteq \ta$ and $\trust = \trusted$)

then $\npair{(w,w)} \in \lrvg{\trust}(W)$

By induction on

\begin{equation*}
\sigrets,\sigrets[\mathrm{owned}],\sigcloss,\ta\vdash_{\mathrm{comp-code}} w
\end{equation*}

There are two cases to consider:

* $\mscode(a) = \seal{\sigma_\baddr,\sigma_\eaddr,\sigma_\baddr}$ and $[\sigma_\baddr,\sigma_\eaddr] \subseteq (\sigrets \cup \sigcloss)$:

We distinguish two cases:

* $\trust = \trusted$:

By definition of $\lrvg{\trusted}$, it suffices to prove that
$\pwheap(r_{\mathrm{code}}) = \codereg{\sigrets,\sigcloss,\mscode,\gc}$, $\dom(\code)\subseteq \ta$ and $[\sigma_\baddr,\sigma_\eaddr] \subseteq (\sigrets \cup \sigcloss)$, all of which follow by assumption.

* $\trust = \untrusted$:

In this case, we know that $\sigrets=\emptyset$.

By definition of $\lrv$, it suffices to prove that

\begin{equation*}
\forall \sigma' \in [\sigma_\baddr,\sigma_\eaddr] \ldotp \exists r \in \dom(\pwheap) \ldotp \pwheap(r) = (\pure,\_,H_\sigma) \tand H_\sigma \; \sigma' \nequal \lrv
\end{equation*}

We take $r = r_{\var{code}}$ and the result then follows from Lemma <ref>.

* $\mscode(a) \in \ints$ and

\begin{multline*}
([a \cdots a + \calllen-1] \subseteq \ta \wedge\mscode([a \cdots a + \calllen-1]) = \scall[0..\calllen-1]{\offpc,\offsigma}{r_1}{r_2}) \Rightarrow\\ (\mscode(a+\offpc) = \seal{\sigma_\baddr,\sigma_\eaddr,\sigma_\baddr} \wedge \sigma_\baddr+\offsigma \in \sigrets[\mathrm{owned}])
\end{multline*}

Using $\mscode(a) \in \ints$, the result follows easily by definition.

\begin{equation*}
\dom(\mscode), A_{\mathrm{own}}, A_{\mathrm{non-linear}}, \sigrets,\sigcloss \vdash_{\mathrm{comp-value}} w
\end{equation*}

* $\npair{A_{\mathrm{non-linear}}} \in \readCond{\normal,W}$

* $\npair{A_{\mathrm{non-linear}}} \in \writeCond{\normal,W}$

* $\npair{A_{\mathrm{own}}} \in \readCond{\linear,W}$

* $\npair{A_{\mathrm{own}}} \in \writeCond{\linear,W}$

* $\pwheap(r_{\mathrm{code}}) = \codereg{\sigrets,\sigcloss,\mscode,\gc}$

* $\dom(\mscode) \mathrel{\#} \ta$ or $\dom(\mscode) \subseteq \ta$

* $(A_{\mathrm{own}} \cup A_{\mathrm{non-linear}}) \mathrel{\#} \ta$

then $\npair{(w,w)} \in \lrv(W)$

By induction on the judgement

\begin{equation*}
\dom(\mscode), A_{\mathrm{own}}, A_{\mathrm{non-linear}}, \sigrets,\sigcloss \vdash_{\mathrm{comp-value}} w
\end{equation*}

We have the following cases:

* $w = z$: result follows trivially

* $w = ((\perm,\lin),\baddr,\eaddr,\aaddr)$,
$\permbnf \sqsubseteq \rw$,
$\lin = \linear \Rightarrow \emptyset \subset [\baddr,\eaddr] \subseteq A_{\mathrm{own}}$ and
$\lin = \normal \Rightarrow [\baddr,\eaddr] \subseteq A_{\mathrm{non-linear}}$:

By definition of $\lrv$, it suffices to prove that $[b,e] \mathrel{\#} \ta$, $\npair{[\baddr,\eaddr]} \in \readCond{\lin,W}$ and $\npair{[\baddr,\eaddr]}\in\writeCond{\lin,W}$.
The result then follows easily from the assumptions, with Lemma <ref>.

* $w = \sealed{\sigma,\vsc}$ and

\begin{equation*}
\dom(\mscode),A_{\mathrm{own}},A_{\mathrm{non-linear}},\sigrets,\sigcloss \vdash_{\mathrm{comp-value}} \vsc
\end{equation*}

and $\sigma \in \sigcloss$:

First, we have by induction that $\npair{(\vsc,\vsc)} \in \lrv (W)$.

By definition of $\lrv$ and by choosing island $r = r_{\mathrm{code}}$, it suffices to prove that

* $\npair[n']{(\vsc,\vsc)} \in H_\sigma \; \sigma \; \xi^{-1}(W)$ for all $n' < n$:

By definition of $\codereg{\sigrets,\sigcloss,\mscode,\gc}$ and $H^\mathrm{code,\square}_\sigma$ and because we know that $\sigma\in\sigcloss$, it suffices to prove that
one of the following holds:

* $(\dom(\code) \mathrel{\#} \ta$ and $\npair[n']{(\vsc,\vsc)} \in \lrv \; \xi(\xi^{-1}(W))$

* $(\dom(\code) \subseteq \ta$ and $\npair[n']{(\vsc,\vsc)} \in \lrvtrusted \; \xi(\xi^{-1}(W))$

Both follow since $\xi(\xi^{-1}(W)) = W$ and $\lrv \; W \subseteq \lrvtrusted \; W$, $\dom(\mscode \mathrel{\#} \ta)$ or $\dom(\mscode) \subseteq \ta$, and the above fact that $\npair{(\vsc,\vsc)} \in \lrv (W)$ and Lemma <ref>.

* $(\isLinear{\vsc} \text{ iff } \isLinear{\vsc})$: trivially fine

* If $\isLinear{\vsc}$, then
for all $W' \future W$, $W_o$, $n' < n$ and $\npair[n']{\stpair[.]{\vsc_S'}{\vsc'_T}} \in H_\sigma \; \sigma \; \xi^{-1}(W_o)$, we have that

\begin{equation*}
\npair[n']{(\vsc,\vsc_S',\vsc,\vsc_T')} \in \lrexj(W'\oplus W_o))
\end{equation*}

By definition of $\codereg{\sigrets,\sigcloss,\mscode,\gc}$ and $H^\mathrm{code,\square}_\sigma$ and because we know that $\sigma\in\sigcloss$, we know that
one of the following holds:

* $(\dom(\code) \mathrel{\#} \ta$ and $\npair[n']{(\vsc_S',\vsc_T')} \in \lrv \; \xi(\xi^{-1}(W_o))$

* $(\dom(\code) \subseteq \ta$ and $\sigcloss\subseteq \gsigcloss$ and $\sigrets \subseteq \gsigrets$ and $\npair[n']{(\vsc_S',\vsc_T')} \in \lrvg{\trust} \; \xi(\xi^{-1}(W_o))$ with $\trust = \trusted$ iff $\exec{\vsc_S'}$.

Lemma <ref> now allows us to conclude (using Lemma <ref>) that:

\begin{equation*}
\npair[n']{(\vsc,\vsc_S',\vsc,\vsc_T')} \in \lrexj(W'\oplus W_o))
\end{equation*}

* If $\nonLinear{\src{\vsc_S}}$ then for all $W' \future \purePart{W}$, $W_o$, $n' < n$, $\npair[n']{(\vsc_S',\vsc'_T)} \in H_\sigma \; \sigma \; \xi^{-1}(W_o)$, we have that

\begin{equation*}
\npair[n']{(\vsc,\src{\vsc_S'},\vsc,\vsc_T')} \in \lrexj(W'\oplus W_o))
\end{equation*}

By definition of $\codereg{\sigrets,\sigcloss,\mscode,\gc}$ and $H^\mathrm{code,\square}_\sigma$ and because we know that $\sigma\in\sigcloss$, we know that
one of the following holds:

* $(\dom(\code) \mathrel{\#} \ta$ and $\npair[n']{(\vsc_S',\vsc_T')} \in \lrv \; \xi(\xi^{-1}(W_o))$

* $(\dom(\code) \subseteq \ta$ and $\sigcloss\subseteq \gsigcloss$ and $\sigrets \subseteq \gsigrets$ and $\npair[n']{(\vsc_S',\vsc_T')} \in \lrvg{\trust} \; \xi(\xi^{-1}(W_o))$ with $\trust = \trusted$ iff $\exec{\vsc_S'}$.

First, Lemma <ref> allows us to conclude that also $\npair{(\vsc,\vsc)} \in \lrv (\purePart{W})$.

Next, Lemma <ref> now allows us to conclude (using Lemma <ref>) that:

\begin{equation*}
\npair[n']{(\vsc,\vsc_S',\vsc,\vsc_T')} \in \lrexj(W'\oplus W_o))
\end{equation*}

\begin{equation*}
\dom(\mscode), A_{\mathrm{non-linear}}, \sigrets,\sigcloss \vdash_{\mathrm{comp-export}} w
\end{equation*}

* $\npair{A_{\mathrm{non-linear}}} \in \readCond{\normal,W}$

* $\npair{A_{\mathrm{non-linear}}} \in \writeCond{\normal,W}$

* $\pwheap(r_{\mathrm{code}}) = \codereg{\sigrets,\sigcloss,\mscode,\gc}$

* $\dom(\mscode) \mathrel{\#} \ta$ or $\dom(\mscode) \subseteq \ta$

* If $w = \sealed{\sigma,\vsc}$ with $\dom(\mscode) \subseteq \ta$, $\sigma \in \sigcloss$ and $\exec{\vsc}$, then
$\vsc$ behaves reasonably up to $n$ steps.

* $A_{\mathrm{non-linear}}\mathrel{\#} \ta$

then $\npair{(w,w)} \in \lrv(W)$

By induction on the judgement

\begin{equation*}
\dom(\mscode), A_{\mathrm{non-linear}}, \sigrets,\sigcloss \vdash_{\mathrm{comp-export}} w
\end{equation*}

We have the following cases:

* $w = \sealed{\sigma,\vsc}$, $\vsc = ((\rx,\normal),\baddr,\eaddr,\aaddr)$, $[\baddr,\eaddr]\subseteq \dom(\mscode)$, $\sigma \in \sigcloss$:

By definition of $\lrv$ and by choosing island $r = r_{\mathrm{code}}$, it suffices to prove that

* $\npair[n']{(\vsc,\vsc)} \in H^\mathrm{code,\square}_\sigma \; \sigrets \; \sigcloss \; \code \; \gc \; \sigma \; \xi^{-1}(W)$ for all $n' < n$:

By definition of $\codereg{\sigrets,\sigcloss,\mscode,\gc}$ and $H^\mathrm{code,\square}_\sigma$ and because we know that $\sigma\in\sigcloss$, it suffices to prove that one of the following holds:

* $(\dom(\code) \mathrel{\#} \ta$ and $\npair[n']{(\vsc,\vsc)} \in \lrv \; \xi(\xi^{-1}(W))$

* $(\dom(\code) \subseteq \ta$ and $\npair[n']{(\vsc,\vsc)} \in \lrvtrusted \; \xi(\xi^{-1}(W))$ and $\exec{\vsc}$

Take $\trust = \untrusted$ iff $\dom(\mscode \mathrel{\#} \ta)$ and $\trust = \trusted$ iff $\dom(\mscode) \subseteq \ta$.
Since $\xi(\xi^{-1}(W)) = W$ and because we know by assumption that $\dom(\mscode \mathrel{\#} \ta)$ or $\dom(\mscode) \subseteq \ta$, it suffices to prove that $\npair[n']{(\vsc,\vsc)} \in \lrvg{\trust}(W)$.

This last fact follows from Lemma <ref>, using Lemma <ref> and the definition of $\xReadCond{}$ with the assumption that $\pwheap(r_{\mathrm{code}}) = \codereg{\sigrets,\sigcloss,\mscode,\gc}$.

* $(\isLinear{\vsc} \text{ iff } \isLinear{\vsc})$: trivially fine

* For all $W' \future \purePart{W}$, $W_o$, $n' < n$, $\npair[n']{(\vsc_S',\vsc'_T)} \in H^\mathrm{code,\square}_\sigma \; \sigrets \; \sigcloss \; \code \; \gc \; \sigma \; \xi^{-1}(W_o)$, we have that

\begin{equation*}
\npair[n']{(\vsc,\src{\vsc_S'},\vsc,\vsc_T')} \in \lrexj(W'\oplus W_o))
\end{equation*}

From one of our assumptions, we know that $\vsc$ behaves reasonably up to $n$ steps if $\dom(\mscode)\subseteq \ta$.

Theorem <ref> now tells us that $\npair{(\vsc,\vsc)} \in \lre(\purePart{W})$, using the definition of $\xReadCond{}$ and the assumption that $\pwheap(r_{\mathrm{code}}) = \codereg{\sigrets,\sigcloss,\mscode,\gc}$.

Since $\sigma\in\sigcloss$, it follows from $\npair[n']{(\vsc_S',\vsc'_T)} \in H^\mathrm{code,\square}_\sigma \; \sigrets \; \sigcloss \; \code \; \gc \; \sigma \; \xi^{-1}(W_o)$ that

\begin{equation*}
\npair[n']{(\vsc_S',\vsc'_T)} \in \lrvg{\trust}(W_o)
\end{equation*}

with $\trust = \untrusted$ iff ($\dom(\code \mathrel{\#} \ta)$ or $\nonExec{\vsc_S'}$) and $\trust = \trusted$ iff ($\dom(\code) \subseteq \ta$ and $\exec{\vsc_S'}$).

The result now follows from Lemma <ref>.

\begin{equation*}
\dom(\mscode),\emptyset,A_{\mathrm{non-linear}},\sigrets,\sigcloss \vdash_{\mathrm{comp-value}} w
\end{equation*}

In this case, the result follows from Lemma <ref>, using the fact that $\readCond$ and $\writeCond$ follow trivially for the empty $A_{\mathrm{own}}$ and a similar observation about the empty imports.

* $\gc = (\ta,\stkb,\gsigrets,\gsigcloss)$

* $\var{comp}$ is a well-formed component, i.e. $\ta \vdash \var{comp}$

* One of the following holds:

* $\dom(\var{comp}.\mscode) \subseteq \ta$ and $\var{comp}$ is a reasonable component (see Section <ref>)

* $\dom(\var{comp}.\mscode) \mathrel{\#} \ta$

* $\sigrets \subseteq \gsigrets$ and $\sigcloss \subseteq \gsigcloss$

Then there exists a $W$ such that

* $\npair{(\var{comp},\var{comp})} \in \lrcomp(W)$

* $\dom(\pwheap)$ can be chosen to not include any finite set of region names

* $\dom(\pwfree) =
\dom(\pwpriv)=\emptyset$

If $\var{comp}$ is of the form $(\var{comp}_0,c_{\mathrm{main},c}, c_{\mathrm{main},d})$, then we have (by definition of component well-formedness) that $c_{\mathrm{main},c}, c_{\mathrm{main},d} \subseteq \var{comp}_0.\overline{c_{\mathrm{export}}}$, as required by $\lrcomp(W)$.
Hence, we can restrict our attention to components of the form $\var{comp}_0$.

\begin{equation*}
\var{comp} = (\mscode\uplus\mspad,\msdata,\overline{\var{import}},\overline{\var{export}},\sigrets,\sigcloss,A_\linear)
\end{equation*}

Note that confusingly, $\var{comp}.\mscode = \mscode\uplus\mspad$, so the assumption about $\dom(\var{comp}.\mscode)$ should be interpreted properly.
We then know from $\ta \vdash \var{comp}$ that

* $\dom(\mscode) = [\baddr,\eaddr]$

* $[\baddr-1,\eaddr+1] \mathrel{\#} \dom(\msdata)$

* $\mspad = [\baddr-1\mapsto 0] \uplus [\eaddr+1 \mapsto 0]$

* $\sigrets,\sigcloss,\ta\vdash_{\mathrm{comp-code}} \mscode$

* $\exists A_\mathrm{own} : \dom(\msdata) \rightarrow \powerset{\dom(\msdata)}$

* $\dom(\msdata) = A_{\mathrm{non-linear}} \uplus A_\linear$

* $A_\linear = \biguplus_{a \in \dom(\msdata)} A_{\mathrm{own}}(a)$

\begin{equation*}
\forall a \in \dom(\msdata)\ldotp \dom(\mscode),A_{\mathrm{own}}(a),A_{\mathrm{non-linear}},\sigrets,\sigcloss \vdash_{\mathrm{comp-value}} \msdata(a)
\end{equation*}

\begin{equation*}
\overline{\dom(\mscode), A_{\mathrm{non-linear}}, \sigrets,\sigcloss \vdash_{\mathrm{comp-export}} c_{\mathrm{export}}}
\end{equation*}

* $(\dom(\mscode) \subseteq \ta) \vee (\dom(\mscode) \mathrel{\#} \ta \wedge \sigrets = \emptyset)$

* $\dom(\msdata) \mathrel{\#} \ta$

Take $\overline{\var{import}} = \overline{a_{\mathrm{import}} \mapsfrom s_{\mathrm{import}}}$.

Now take $W$ such that

* $\dom(\pwfree) = \dom(\pwpriv) = \emptyset$

* $\pwheap(r_\code) =  \codereg[\mathrm{code},\square]{\sigrets,\sigcloss,\mscode,\gc}$

* there exist $r_{\mathrm{addr}} : \dom(\msdata) \mapsto \dom(\pwheap)$ such that

* For all $\aaddr\in\dom(\msdata)$, $\pwheap(r_{\mathrm{addr}}(\aaddr)) = \stdreg{\{\aaddr\},\gc}{\lin}$ with ($\lin = \pure$ if $\aaddr\not\in A_\linear$) and ($\lin = \spatialo$ if $\aaddr\in A_\linear$)

with $r_{\mathrm{code}}$ and $r_a$ chosen according to the given restriction.

It now remains to prove that $\npair{(\var{comp},\var{comp})} \in \lrcomp{W}$.
Take $W' \future W$ and assume that

\begin{equation*}
\overline{\npair[n']{(w_{\mathrm{import}},w_{\mathrm{import}})}} \in \lrv(\purePart{W'}) \text{ for all $n' < n$}\\
\end{equation*}

\begin{equation*}
\msdata' = \msdata{}[\overline{a_{\mathrm{import}} \mapsto w_{\mathrm{import}}}] \\
\end{equation*}

We need to show that

\begin{equation*}
\npair{(\sigrets\uplus\sigcloss,\mspad\uplus\mscode\uplus \msdata', \mspad\uplus\mscode\uplus\msdata')} \in \lrheap(\pwheap)(W')
\end{equation*}

Take $R_\ms : \dom(\activeReg{\pwheap}) \fun \MemSeg \times \MemSeg$ such that

* $R_\ms(r_\addr) = (\msdata|_{\{a\}}, \msdata|_{\{a\}})$.

* $R_\ms(r_\var{code}) = (\mspad\uplus\mscode,\mspad\uplus\mscode)$

Take $R_W' : \dom(\activeReg{\pwheap}) \fun \World$ such that

* $R_W'(r_\addr) = \purePart{W}[\var{heap}.r_{\addr'}\mapsto \stdreg{\{\aaddr\},\gc}{\spatialo}]_{\addr' \in A_\var{own}(\addr)}$

* $R_W'(r_\var{code}) = \purePart{W}$

Since then $W = \oplus_{r \in \dom(\activeReg{\pwheap})} R_W'(r)$, we can use Lemma <ref> to construct an $R_W$ with

\begin{equation*}
W' = \oplus_{r \in \dom(\activeReg{\pwheap})} R_W(r)
\end{equation*}

and $R_W(r) \future R_W'(r)$ for all $r$.
Finally, take $R_\var{seal} : \dom(\activeReg{\pwheap}) \fun \powerset{\Seal}$ to satisfy

* $R_\var{seal}(r_\addr) = \emptyset$

* $R_\var{seal}(r_\var{code}) = \sigrets\uplus \sigcloss$.

We then need to prove that

* $\npair[n']{(\msdata'|_{\{\addr\}},\msdata'|_{\{\addr\}})} \in \stdreg{\{\aaddr\},\gc}{\lin}.H~ \xi^{-1}(R_W(r_\addr))$ for all $n' < n$:
Take $n' < n$.
By definition, it suffices to prove that,
$\npair[n']{(\msdata'(\addr),\msdata'(\addr))} \in \lrv(R_W(r_\addr))$.

If $(a \mapsfrom \_) \in \overline{\var{import}}$, then we know that $\msdata'(a)$ is the corresponding $w_{\mathrm{import}}$ and the result is fine by the assumption that

\begin{equation*}