\overline{\npair[n']{(w_{\mathrm{import}},w_{\mathrm{import}})}} \in \lrv(\purePart{W'})
\end{equation*}

together with <ref> and the fact that $R_W(\addr) \future \purePart{W'}$ (by Lemma <ref>).

Otherwise, $\msdata'(a) = \msdata(a)$ and we know from our assumptions that

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

By Lemma <ref>, it then suffices to prove that

* $\npair[n']{A_{\mathrm{non-linear}}} \in \readCond{\normal,R_W(\addr)}$: follows by Lemma <ref> using the fact that $R_W(a) \future R_W'(a)$ and by definition, using the choice of $W$, $R_W'(\addr)$

* $\npair[n']{A_{\mathrm{non-linear}}} \in \writeCond{\normal,R_W(\addr)}$: follows by Lemma <ref> using the fact that $R_W(a) \future R_W'(a)$ and by definition, using the choice of $W$, $R_W'(\addr)$

* $\npair[n']{A_{\mathrm{own}}(\addr)} \in \readCond{\linear,R_W(\addr)}$: follows by Lemma <ref> using the fact that $R_W(a) \future R_W'(a)$ and by definition, using the choice of $W$, $R_W'(\addr)$

* $\npair[n']{A_{\mathrm{own}}(\addr)} \in \writeCond{\linear,R_W(\addr)}$: follows by Lemma <ref> using the fact that $R_W(a) \future R_W'(a)$ and by definition, using the choice of $W$, $R_W'(\addr)$

* $\pwheap[R_W(\addr)](r_{\mathrm{code}}) = \codereg{\sigrets,\sigcloss,\mscode,\gc}$: follows from the choice of $W$ and $R_W'(\addr)$ and the fact that $R_W(a) \future R_W'(a)$

* $\dom(\mscode) \mathrel{\#} \ta$ or $\dom(\mscode) \subseteq \ta$: by assumption.

* $\npair[n']{(\mspad\uplus\mscode,\mspad\uplus\mscode)} \in  \codereg[\mathrm{code},\square]{\sigrets,\sigcloss,\mscode,\gc}.H~ \xi^{-1}(\purePart{W'})$ for all $n' < n$:
Take $n' < n$.
We take $\trust = \trusted$ if $[\baddr-1,\eaddr+1] \subseteq \ta$ and $\trust =\untrusted$ otherwise.
By definition, we need to prove that:

* $\dom(\code) = [\baddr,\eaddr]$: by assumption.

* $([\baddr-1,\eaddr+1]\subseteq \ta \wedge \trust = \trusted) \vee ([\baddr-1,\eaddr+1]\mathrel{\#} \ta \wedge \sigrets = \emptyset \wedge \trust =\untrusted)$: by assumption and choice of $\trust$.

* $\sigrets,\sigcloss,\ta\vdash_{\mathrm{comp-code}} \code$: by assumption.

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

* $\forall a \in \dom(\code) \ldotp \npair[n']{(\code(a),\code(a))} \in \lrvg{\trust}(\purePart{}(\xi(\xi^{-1}(\purePart{W'}))))$:
Note first that $\purePart{}(\xi(\xi^{-1}(\purePart{W'}))) =\purePart{W'}$.

By Lemma <ref>, it suffices to prove that:

* $\pwheap[W'](r_{\mathrm{code}}) = \codereg{\sigrets,\sigcloss,\mscode,\gc}$: follows by choice of $W$ and the fact that $W' \future W$.

* ($\dom(\mscode) \mathrel{\#} \ta$ and $\trust = \untrusted$) or ($\dom(\mscode) \subseteq \ta$ and $\trust = \trusted$): by assumption and choice of $\trust$

\begin{equation*}
\dom(\codereg[\mathrm{code},\square]{\sigrets,\sigcloss,\mscode,\gc}.H_\sigma) = \sigrets\uplus \sigcloss
\end{equation*}

This follows easily from the definition.

* $\overline{\npair{(w_{\mathrm{export}},w_{\mathrm{export}})}} \in \lrv(\purePart{W'})$:

We know from our assumptions that

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

By Lemma <ref>, it then suffices to prove that

* $\npair{A_{\mathrm{non-linear}}} \in \readCond{}(\normal,\purePart{W'})$: follows by Lemma <ref> using the fact that $R_W(a) \future R_W'(a)$ and by definition, using the choice of $W$, $R_W'(\addr)$

* $\npair{A_{\mathrm{non-linear}}} \in \writeCond{}(\normal,\purePart{W'})$: follows by Lemma <ref> using the fact that $R_W(a) \future R_W'(a)$ and by definition, using the choice of $W$, $R_W'(\addr)$

* $\pwheap[\purePart{W'}](r_{\mathrm{code}}) = \codereg{\sigrets,\sigcloss,\mscode,\gc}$: follows from the choice of $W$ and the fact that $W' \future W$

* $\dom(\mscode) \mathrel{\#} \ta$ or $\dom(\mscode) \subseteq \ta$: by assumption.

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

This follows directly from the fact that $\var{comp}$ is a reasonable component.

* $A_{\mathrm{non-linear}}\mathrel{\#} \ta$:
This follows from the facts that $A_{\mathrm{non-linear}}\subseteq \dom(\msdata) \mathrel{\#} \ta$.

Note: the trusted case of the above lemma can be considered as a compiler correctness result.
The untrusted case can be considered as a back-translation correctness result.

§.§ Related execution configurations

\[
\lrec(W) = \left\{ \npair{\left(
\arraycolsep=0pt\array{l}
(\ms_T,\reg_T)\endarray\right)} \middle|
\begin{array}{l}
\gc = (\ta,\stkb) \tand\\
\exists W_M,W_R,W_\pcreg \ldotp W = W_M \oplus W_R \oplus W_\pcreg \tand\\
\npair{( (\reg_S(\pcreg),\reg_S(\rdata)), (\reg_T(\pcreg),\reg_T(\rdata)) )} \in \lrexj(W_\pcreg) \tand \\
\reg_S(\pcreg) \neq \retptrc(\_) \wedge
\reg_S(\rdata) \neq \retptrd(\_) \wedge \\
\nonExec{\reg_S(\rdata)} \wedge
\nonExec{\reg_T(\rdata)}\\
\memSat{\ms_S,\ms_\stk,\stk,\ms_T}{W_M} \tand\\
\npair{\stpair{\reg}{\reg}} \in \lrr(\{\rdata\})(W_R)
\end{array}
\right\}
\]

TODO 18-07-2018: gc should probably be specified here, so they are not just picked at random.
TODO 18-07-2018: Where is this lemma even used?

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

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

* $\var{comp} \rightsquigarrow \Phi$,

then $\exists W' \future W$ such that for all $n' < n$

* $\npair[n']{(\Phi,\Phi)}\in\lrec(W')$

Take $\var{comp} = ((\mscode, \msdata, \overline{\var{import}}, \overline{\var{export}}, \sigrets, \sigcloss,A_\linear),  c_{\mathrm{main},c}, c_{\mathrm{main},d})$.
Then we know from $\var{comp} \rightsquigarrow \Phi$ that

* $c_{\mathrm{main},c} = \sealed{\sigma_1, c_{\mathrm{main},c}'}$

* $c_{\mathrm{main},d} = \sealed{\sigma_2, c_{\mathrm{main},d}'}$

* $\sigma_1 = \sigma_2$

* $\reg(\pcreg) = c_{\mathrm{main},c}'$

* $\reg(\rdata) = c_{\mathrm{main},d}'$

* $\nonExec{c_{\mathrm{main},d}'}$

* $\src{\reg(\rstk) = \stkptr{\rw,\baddr_\stk,\eaddr_\stk,\eaddr_\stk}}$

* $\trg{\reg(\rstk) = ((\rw,\linear),\baddr_\stk,\eaddr_\stk,\eaddr_\stk)}$

* $\reg(\RegName \setminus \{\pcreg,\rdata,\rstk\}) = 0$

* $\range{\ms_\stk} = \{0\}$

* $\mem = \mscode \uplus \msdata \trg{\;\uplus\; \ms_\stk}$

* $[\baddr_\stk,\eaddr_\stk] = \dom(\ms_\stk )$

* $[\baddr_\stk-1,\eaddr_\stk+1] \mathrel{\#} (\dom(\mscode) \cup \dom(\msdata))$

* $\overline{\var{import}} = \emptyset$

* $\Phi = (\mem, \reg\src{, \emptyset, \ms_\stk})$

From $\npair{(\var{comp},\var{comp})} \in \lrcomp(W)$, we know that

* $\{(\_ \mapsto c_{\mathrm{main},c}), (\_ \mapsto c_{\mathrm{main},d})\}\subseteq \overline{\var{export}}$ and

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

* $\var{comp}_0 = (\mscode, \msdata, \overline{a_{\mathrm{import}}\mapsfrom s_{\mathrm{import}}}, \overline{s_{\mathrm{export}}\mapsto w_{\mathrm{export}}}, \sigrets, \sigcloss,A_\linear)$

From this, it follows that for all  $W' \future W$, if

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

and $\msdata' = \msdata{}[\overline{a_{\mathrm{import}} \mapsto w_{\mathrm{import}}}]$

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

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

Since $\overline{w_{\mathrm{import}}} = \emptyset$, the former holds vacuously, $\msdata' = \msdata$ and the latter two results follow for every $W' \future W$.

Now take $\overline{r_a}$ for $a \in [\baddr_\stk,\eaddr_\stk]$ arbitrary and

\begin{align*}
\pwheap[W_\stk] &= \emptyset\\
\pwpriv[W_\stk] &= \emptyset\\
\dom(\pwfree[W_\stk]) &= \{r_a \mid a \in [\baddr_\stk,\eaddr_\stk]\}\\
\pwfree[W_\stk](r_a) &= \stdreg{\{a\},\gc}{\spatialo}\\
W' &= W \uplus W_\stk\\
W_\pcreg &= \purePart{W'}\\
W_R &= \purePart{W} \uplus W_\stk\\
W_M &= W \uplus \purePart{W_\stk}
\end{align*}

Then $W' = W_M \oplus W_R \oplus W_\pcreg$ (by Lemmas <ref>, <ref>, <ref> and <ref>), $W_M \future W$ (by Lemma <ref>) and $W_\pcreg \future \purePart{W}$ (by Lemma <ref> and <ref>).

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

* $\npair[n']{( (\reg(\pcreg),\reg(\rdata)), (\reg(\pcreg),\reg(\rdata)) )} \in \lrexj(W_\pcreg)$:
Since $W' \future W$, we know from above that:

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

and we have defined $W_\pc = \purePart{W'}$ and we know that $\{c_{\mathrm{main},c}, c_{\mathrm{main},d}\}\subseteq
\overline{c_{\mathrm{export}}}$.
It follows that

\begin{align*}
\npair{(c_{\mathrm{main},c},c_{\mathrm{main},c})} &\in \lrv(W_\pc)\\
\npair{(c_{\mathrm{main},d},c_{\mathrm{main},d})} &\in \lrv(W_\pc)
\end{align*}

Since $W_\pc = \purePart{W'}$, Lemma <ref> tells us that for $n' < n$,

\begin{equation*}
\npair[n']{( (c_{\mathrm{main},c},c_{\mathrm{main},d}), (c_{\mathrm{main},c},c_{\mathrm{main},d}) )} \in \lrexj(W_\pcreg)
\end{equation*}

Since $\reg(\pcreg) = c_{\mathrm{main},c}'$ and $\reg(\rdata) = c_{\mathrm{main},d}'$, this is what we set out to prove.

* $\reg_S(\pcreg) \neq \retptrc(\_)$,

* $\reg_S(\rdata) \neq \retptrd(\_)$,

* $\nonExec{\reg_S(\rdata)}$ and

* $\nonExec{\reg_T(\rdata)}$

This follows from the facts that $\reg(\pcreg) = c_{\mathrm{main},c}'$, $\reg(\rdata) = c_{\mathrm{main},d}'$,
$\nonExec{c_{\mathrm{main},d}'}$, $\{c_{\mathrm{main},c}, c_{\mathrm{main},d}\}\subseteq \overline{c_{\mathrm{export}}}$ and the fact that $\overline{c_{\mathrm{export}}}$ are also valid

* $\memSat[n']{\ms_S,\ms_\stk,\stk,\ms_T}{W_M}$:
Since $W_M \future W$, we have seen above that

\begin{equation*}
\npair{(\sigrets\uplus\sigcloss,\mscode\uplus \msdata, \mscode\uplus\msdata)} \in \lrheap(\pwheap[W_M])(W_M)
\end{equation*}

and by Lemma <ref> also

\begin{equation*}
\npair[n']{(\sigrets\uplus\sigcloss,\mscode\uplus \msdata, \mscode\uplus\msdata)} \in \lrheap(\pwheap[W_M])(W_M)
\end{equation*}

It suffices to prove that also

* $\memSatStack[n']{\emptyset,\emptyset}{\purePart{W_M}}$

* $\memSatFStack[n']{\ms_\stk,\ms_\stk}{\purePart{W_M}}$

The former follows vacuously.
The latter follows by taking $R_\ms(r_a) = (\ms_\stk|_{\{a\}},\ms_\stk|_{\{a\}})$, $R_W(r_a) = \purePart{W_M}$ for $a \in [\baddr_\stk,\eaddr_\stk]$ by Lemma <ref> and <ref> if we can show that:

\begin{equation*}
\npair[n'']{(\ms_\stk|_{\{a\}},\ms_\stk|_{\{a\}})} \in \stdreg{\{a\},\gc}{\spatialo}.H~ \xi^{-1}(\purePart{W_M})
\end{equation*}

for all $n'' < n'$.
By definition, it suffices to show that for all $n'' < n'$, we have that:

\begin{equation*}
\npair[n'']{(\ms_\stk(a),\ms_\stk(a)) \in \lrv(\purePart{W_M})}
\end{equation*}

But $\ms_\stk(a) = 0$, so this follows easily by definition.

* $\npair[n']{(\reg,\reg)} \in \lrr(\{\rdata\})(W_R)$:

We have that $\reg(\RegName \setminus \{\pcreg,\rdata,\rstk\}) = 0$, so by definition, it suffices to prove that

\begin{equation*}
\npair[n']{(\reg(r_\stk),\reg(r_\stk))} \in \lrv(W_R)
\end{equation*}

Since $\src{\reg(\rstk) = \stkptr{\rw,\baddr_\stk,\eaddr_\stk,\eaddr_\stk}}$ and $\trg{\reg(\rstk) = ((\rw,\linear),\baddr_\stk,\eaddr_\stk,\eaddr_\stk)}$, it suffices to prove (by definition) that

\begin{align*}
\npair[n']{[b_\stk,e_\stk]} &\in \stackReadCond{W_R}\\
\npair[n']{[b_\stk,e_\stk]} &\in \stackWriteCond{W_R}
\end{align*}

For both, we can take $S = \dom(\pwfree[W_\stk]) = \{r_a \mid a \in [\baddr_\stk,\eaddr_\stk]\}$, $R(r_\addr) = \{\addr\}$, and then it suffices to prove that for all $r_\addr$, $\pwfree[W_R](r_\addr).H \nsubeq \stdreg{\{\addr\},\gc}{\spatialo}$ resp. $\pwfree[W_R](r_\addr).H \nsupeq \stdreg{\{\addr\},\gc}{\spatialo}$.
Both follow easily since
$\pwfree[W_R](r_a) = \pwfree[W_\stk](r_a) = \stdreg{\{a\},\gc}{\spatialo}$.

* $\npair{\stpair{\Phi}{\Phi}}\in\lrec[\preceq,\gc](W)$

* $i \leq n$

* $\Phi_S \sterm[i]{\gc}$

then $\Phi_T\term$.

Also, if

* $\npair{\stpair{\Phi}{\Phi}}\in\lrec[\succeq,\gc](W)$

* $i \leq n$

* $\Phi_T \term[i]$,

then $\Phi_S\sterm{\gc}$.

First, assume that

* $\npair{\stpair{\Phi}{\Phi}}\in\lrec[\preceq](W)$

* $i \leq n$

* $\Phi_S \sterm[i]{\gc}$

Assume w.l.o.g. that $\Phi_S = (\ms_S,\reg_S,\stk,\ms_\stk)$, $\Phi_T = (\ms_T,\reg_T)$ and $\gc = (\ta,\stkb)$.
Then it follows from $\npair{\stpair{\Phi}{\Phi}}\in\lrec[\preceq](W)$ that there exist $W_M,W_R,W_\pcreg$ such that

* $W = W_M \oplus W_R \oplus W_\pcreg$

* $\npair{( (\reg_S(\pcreg),\reg_S(\rdata)), (\reg_T(\pcreg),\reg_T(\rdata)) )} \in \lrexj[\preceq,\gc](W_\pcreg)$

* $\reg_S(\pcreg) \neq \retptrc(\_)$,

* $\reg_S(\rdata) \neq \retptrd(\_)$,

* $\nonExec{\reg_S(\rdata)}$ and

* $\nonExec{\reg_T(\rdata)}$

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

* $\npair{\stpair{\reg}{\reg}} \in \lrr[\preceq,\gc](\{\rdata\})(W_R)$

We can then instantiate the conditions from $\lrexj$ with the other conditions from this list to obtain $\Phi_S',\Phi_T'$ such that

* $\Phi_S' = \xjumpResult{\reg_S(\pcreg)}{\reg_S(\rdata)}{\Phi_S}$

* $\Phi_T' = \xjumpResult{\reg_T(\pcreg)}{\reg_T(\rdata)}{\Phi_T}$

* $\npair{\left(\Phi_S', \Phi_T' \right)}\in \lrol$

Using the facts that $\reg_S(\pcreg) \neq \retptrc(\_)$, $\reg_S(\rdata) \neq \retptrd(\_)$ and $\nonExec{\reg_S(\rdata)}$, we know (by definition of $\xjumpResult{\_}{\_}{\_}$) that

* $\Phi_S' = \xjumpResult{\reg_S(\pcreg)}{\reg_S(\rdata)}{\Phi_S} = \Phi_S\updReg{\pcreg}{\reg_S(\pcreg)}\updReg{\rdata}{\reg_S(\rdata)} = \Phi_S$

* $\Phi_T' = \xjumpResult{\reg_T(\pcreg)}{\reg_T(\rdata)}{\Phi_T} = \Phi_T\updReg{\pcreg}{\reg_T(\pcreg)}\updReg{\rdata}{\reg_T(\rdata)} = \Phi_T$

From $\npair{\left(\Phi_S, \Phi_T \right)}\in \lrol$, it follows immediately that if $\Phi_S \sterm[i]{\ta,\stkb}$ with $i \le n$, then $\Phi_T \term$ as required.

The proof in the other direction is directly analogous.

If $\npair{\stpair{C}{C}}\in\lrcomp(W_1)$ and $\npair{\stpair{P}{P}} \in \lrcomp(W_2)$, then
$\npair[n']{(\plug{C_S}{P_S},\plug{C_T}{P_T})} \in \lrec(W_1 \uplus W_2)$, for all $n' < n$.

By definition, we have that $C_S \bowtie P_S \rightsquigarrow C_S[P_S]$ and $C_T \bowtie P_T \rightsquigarrow C_T[P_T]$.

The result follows directly from Lemmas <ref> and <ref>.

§ FULL ABSTRACTION

In the source language, we define that $\src{\var{comp}_1 \sconeq \var{comp}_2}$ iff

\begin{equation*}
\forall \src{\context} \ldotp \emptyset \vdash \src{\context} \Rightarrow \src{\plug{\context}{\var{comp}_1} \sterm{\ta[,1],\stkb_1}} \Leftrightarrow \src{\plug{\context}{\var{comp}_2} \sterm{\ta[,2],\stkb_2}}
\end{equation*}

with $\src{\ta[,i]} = \src{\dom(\var{comp}_i.\mscode)}$
06-07-2018: TODO: Dominique, did you resolve this?
and stkbase?

Note that we define source language contextual equivalence with respect to contexts that are not in $\ta$.
This means that they are unable to perform calls.
We believe this fits with the goal of this work: allow programmers (or better: authors of previous compiler passes) to reason about their target language programs under a special perspective, where all calls can be interpreted as calls that actually behave in a well-bracketed way by the operational semantics.
This special perspective is defined by overlaying a different operational semantics on the existing code: the source language semantics.
The fact that source contexts cannot make calls themselves is no problem: authors of previous compiler passes should only be able to take the perspective that their own calls are guaranteed to be well-bracketed.
It does not matter for them whether calls in the rest of the system are guaranteed to be well-bracketed.
Note also that if the trusted code hands out closures, the context can still invoke them with an xjmp, rather than a call.
That xjmp can even be the one in the implementation of call if the context uses that implementation.
This works perfectly fine, except that the context does not get any well-bracketedness guarantees, but that doesn't matter.

In the target language, we define that $\trg{\var{comp}_1 \tconeq \var{comp}_2}$ iff

\begin{equation*}
\forall \trg{\context} \ldotp \emptyset \vdash \trg{\context} \Rightarrow \trg{\plug{\context}{\var{comp}_1} \term} \Leftrightarrow \trg{\plug{\context}{\var{comp}_2} \term}
\end{equation*}

For reasonable, well-formed components $\var{comp}_1$ and $\var{comp}_2$ (with respect to $\ta[,i] = \dom(\var{comp}_i.\mscode)$, respectively), we have

\begin{gather*}
\src{\var{comp}_1} \sconeq \src{\var{comp}_2}\\
\Updownarrow\\
\src{\var{comp}_1} \tconeq \src{\var{comp}_2}
\end{gather*}

* Consider first the upward arrow.
Assume $\src{\var{comp}_1} \tconeq \src{\var{comp}_2}$.

Take a $\src{\context}$ such that $\emptyset \vdash \src{\context}$, take $\src{\ta[,i]}
= \src{\dom(\var{comp}_i.\mscode)}$, $\gsigrets_i = \var{comp}_i.\sigrets$ and
$\gsigcloss_i = \var{comp}_i.\sigcloss$, $\gc_i = (\ta[,i],\stkb_i,\gsigrets_i,\gsigcloss_i)$ and we will prove that
$\src{\plug{\context}{\var{comp}_1} \sterm{\gc_1}} \Leftrightarrow
\src{\plug{\context}{\var{comp}_2} \sterm{\gc_2}}$.

By symmetry, we can assume w.l.o.g. that $\src{\plug{\context}{\var{comp}_1} \sterm{\gc_1}}$ and prove that $\src{\plug{\context}{\var{comp}_2} \sterm{\gc_2}}$.
Note that this implies that $\src{\context}$ is a valid context for both $\src{\var{comp}_1}$ and $\src{\var{comp}_2}$.

First, we show that also $\plug{\context}{\var{comp}_1} \trg{\term}$.
Take $n$ the amount of steps in the termination of $\src{\plug{\context}{\var{comp}_1} \sterm{\gc_1}}$.
It follows from Lemma <ref> that $\npair[n+1]{(\var{comp}_1,\var{comp}_1)} \in \lrcomp[\preceq,\gc_1](W_1)$ for some $W_1$ with $\dom(\pwfree) = \dom(\pwpriv) = \emptyset$.
It also follows from the same Lemma <ref> and Lemma <ref> that $\npair[n+1]{(\context,\context)} \in \lrcomp[\preceq,\gc_1](W_1')$ for some $W_1'$ that we can choose such that $W_1 \uplus W_1'$ is defined.
Lemma <ref> then tells us that $\npair{(\plug{\context}{\var{comp}_1}, \plug{\context}{\var{comp}_1})} \in \lrec[\preceq,\gc_1](W_1\uplus W_1')$
Together with $\src{\plug{\context}{\var{comp}_1} \sterm[n]{\gc_1}}$, Lemma <ref> then tells us that $\plug{\context}{\var{comp}_1} \trg{\term}$.

It follows from $\src{\var{comp}_1} \tconeq \src{\var{comp}_2}$ that also $\plug{\context}{\var{comp}_2} \trg{\term}$.

It now remains to show that also $\src{\plug{\context}{\var{comp}_2} \sterm{\gc_2}}$.
Take $n'$ the amount of steps in the termination of $\plug{\context}{\var{comp}_2} \trg{\term}$.
It follows from Lemma <ref> that $\npair[n'+1]{(\var{comp}_2,\var{comp}_2)} \in \lrcomp[\succeq,\gc_2](W_2)$ for some $W_2$ with $\dom(\pwfree) = \dom(\pwpriv) = \emptyset$.
It also follows from the same Lemma <ref> and Lemma <ref> that $\npair[n'+1]{(\context,\context)} \in \lrcomp[\succeq,\gc_2](W_2')$ for some $W_2'$ that we can choose such that $W_2 \uplus W_2'$ is defined.
Lemma <ref> then tells us that $\npair[n']{(\plug{\context}{\var{comp}_2}, \plug{\context}{\var{comp}_2})} \in \lrec[\succeq,\gc_2](W_2\uplus W_2')$
Together with $\plug{\context}{\var{comp}_2} \trg{\term[n']}$, Lemma <ref> then tells us that $\src{\plug{\context}{\var{comp}_2} \sterm{\gc_2}}$, concluding this direction of the proof.

* The downward arrow is similar.

Assume $\src{\var{comp}_1} \sconeq \src{\var{comp}_2}$.
Take $\src{\ta[,i]} = \src{\dom(\var{comp}_i.\mscode)}$, $\gsigrets_i = \var{comp}_i.\sigrets$ and $\gsigcloss_i = \var{comp}_i.\sigcloss$, $\gc_i = (\ta[,i],\stkb_i,\gsigrets_i,\gsigcloss_i)$.

Take a $\trg{\context}$ such that $\emptyset \vdash \trg{\context}$ and we will prove that
$\trg{\plug{\context}{\var{comp}_1} \term} \Leftrightarrow
\trg{\plug{\context}{\var{comp}_2} \term}$.

By symmetry, we can assume w.l.o.g. that $\trg{\plug{\context}{\var{comp}_1} \term}$ and prove that $\trg{\plug{\context}{\var{comp}_2} \term}$.
Note that this implies that $\trg{\context}$ is a valid context for both $\trg{\var{comp}_1}$ and $\trg{\var{comp}_2}$.

First, we show that also $\plug{\context}{\var{comp}_1} \src{\sterm{\gc_1}}$.
Take $n$ the amount of steps in the termination of $\plug{\context}{\var{comp}_1} \trg{\term}$.
It follows from Lemma <ref> that $\npair[n+1]{(\var{comp}_1,\var{comp}_1)} \in \lrcomp[\succeq,\gc_1](W_1)$ for some $W_1$ with $\dom(\pwfree) = \dom(\pwpriv) = \emptyset$.
It also follows from the same Lemma <ref> and Lemma <ref> that $\npair[n+1]{(\context,\context)} \in \lrcomp[\succeq,\gc_1](W_1')$ for some $W_1'$ that we can choose such that $W_1 \uplus W_1'$ is defined.
Lemma <ref> then tells us that $\npair{(\plug{\context}{\var{comp}_1}, \plug{\context}{\var{comp}_1})} \in \lrec[\succeq,\gc_1](W_1\uplus W_1')$
Together with $\plug{\context}{\var{comp}_1} \trg{\term[n]}$, Lemma <ref> then tells us that $\plug{\context}{\var{comp}_1} \src{\sterm{\gc_1}}$.

It follows from $\src{\var{comp}_1} \sconeq \src{\var{comp}_2}$ that also $\plug{\context}{\var{comp}_2} \src{\sterm{\gc_2}}$.

It now remains to show that also $\plug{\context}{\var{comp}_2} \trg{\term}$.
Take $n'$ the amount of steps in the termination of $\plug{\context}{\var{comp}_2} \src{\sterm{\gc_2}}$.
It follows from Lemma <ref> that $\npair[n'+1]{(\var{comp}_2,\var{comp}_2)} \in \lrcomp[\preceq,\gc_2](W_2)$ for some $W_2$ with $\dom(\pwfree) = \dom(\pwpriv) = \emptyset$.
It also follows from the same Lemma <ref> and Lemma <ref> that $\npair[n'+1]{(\context,\context)} \in \lrcomp[\preceq,\gc_2](W_2')$ for some $W_2'$ that we can choose such that $W_2 \uplus W_2'$ is defined.
Lemma <ref> then tells us that

\begin{equation*}
\npair[n']{(\plug{\context}{\var{comp}_2}, \plug{\context}{\var{comp}_2})} \in \lrec[\preceq,\gc_2](W_2\uplus W_2')
\end{equation*}

Together with $\plug{\context}{\var{comp}_2} \trg{\term[n']}$, Lemma <ref> then tells us that $\plug{\context}{\var{comp}_2} \trg{\term}$, concluding the second direction of the proof.

§ LEMMAS

If $r,r' \in \dom(\pwheap)$ and $\pwheap(r) = (\pure,\_,H_\sigma)$
and $\pwheap(r') = (\pure,\_,H_\sigma')$ and $\sigma \in \dom(H_\sigma)$
and $\sigma \in \dom(H_\sigma')$ and $\memSat{\ms_S,\stk,\ms_\stk,\ms_T}{W}$,

\[
H_\sigma = H_\sigma' \text{ and } r = r'
\]

This follows easily by definition of $\memSat{\ms_S,\stk,\ms_\stk,\ms_T}{W}$ and $\lrheap$.

Why is the below lemma needed?

if $\npair{[\baddr,\eaddr]} \in \stackReadCond{W}$, and
$\npair{[\baddr,\eaddr]} \in \stackWriteCond{W}$, and

$\memSat{\ms_S,\stk,\ms_\stk,\ms_T}{W}$, then

\[
\begin{array}{l}
\exists S \subseteq \addressable{\linear,\pwfree} \ldotp \\
\quad \exists R : S \fun \powerset{\nats} \ldotp \\
\qquad \biguplus R(r) = [\baddr,\eaddr] \wedge \\
\qquad \forall r \in S \ldotp \pwfree(r).H \nequal \stdreg{R(r),\gc}{\pur}.H \wedge \\
\qquad \quad |R(r)| = 1 \wedge \\
\qquad \quad \pwfree(r) \text{ is address-stratified}
\end{array}
\]

By assumption we get

* $S_R \subseteq \addressable{\linear,\pwfree}$

* $R_R : S_R \fun \powerset{\nats}$

* $S_W \subseteq \addressable{\linear,\pwfree}$

* $R_W : S_W \fun \powerset{\nats}$

such that

* $\biguplus R_R(r) = [\baddr,\eaddr]$

* $\forall r \in S_R \ldotp \pwfree(r).H \nsubeq
\stdreg{R_R(r),\gc}{\pur}.H \text{ and } |R_R(r)|=1$

* $\biguplus R_W(r) = [\baddr,\eaddr]$

* $\forall r \in S_W \ldotp \pwfree(r).H \nsupeq
\stdreg{R_W(r),\gc}{\pur}.H \text{ and } |R_R(r)|=1 \text{ and } \pwfree(r)
\text{ is address-stratified}$

Now pick $S = S_R \cup S_W$ and show

\[
\forall r \in S \ldotp R_R(r) = R_W(r)
\]

Assuming for contradiction $\exists r \in S \ldotp R_R(r) \neq R_W(r)$, we have $\pwfree(r).H \nsubeq \stdreg{*,\gc}{\pur}.H$ and $\pwfree(r).H \nsupeq \stdreg{-,\gc}{\pur}.H$ for two distinct singleton sets $*$ and $-$.
Due to the memory satisfaction assumption $\pwfree(r)$ is non-empty and it is trivial to show that so is the standard regions.
From the above, we can conclude that $\pwfree(r)$ should contain some $\ms$
with $\dom(\ms) = *$ and $\dom(\ms) = -$ which contradicts the address
stratification assumption.

Now pick

\[
R = R_R(r) \text{ for $r \in S$}
\]

We first show $\biguplus R(r) \supseteq [\baddr,\eaddr]$.
For $\aaddr \in [\baddr,\eaddr]$ we know that there exists $r_1$ and $r_2$ such that $R_W(r_1) = R_R(r_2) = \{\aaddr\}$.
It suffices to show $r_1 = r_2$.
To this end assume the contrary.
This, the address-stratification assumption on all write regions, the $n$-subset of a standard region for read regions, and memory satisfaction lead to a contradiction as any part of memory only can be governed by one region.
Address-stratification and the singleton requirement follows trivially from
the assumptions from the write region. Finally the $n$-equality follows from Lemma <ref>.

If $\iota.H \nsubeq \stdreg{A,\gc}{v}.H$ and $\iota.H \nsupeq \stdreg{A,\gc}{v}.H$, then $\iota.H \nequal  \stdreg{A,\gc}{v}.H$

By definition.

§ PROOFS

§.§ Lemmas

In this section, I have listed lemmas that seem to be necessary for the FTLR proof.

If $n' \leq n$, then

* If $\npair{A} \in \readCond{\lin,W}$, then $\npair[n']{A} \in \readCond{\lin,W}$.

* If $\npair{A} \in \stackReadCond{\lin,W}$, then $\npair[n']{A} \in \stackReadCond{\lin,W}$.

* If $\npair{A} \in \writeCond{\lin,W}$, then $\npair[n']{A} \in \writeCond{\lin,W}$.

* If $\npair{A} \in \stackWriteCond{\lin,W}$, then $\npair[n']{A} \in \stackWriteCond{\lin,W}$.

* If $\npair{A} \in \execCond{\lin,W}$, then $\npair[n']{A} \in \execCond{\lin,W}$.

* If $\npair{A} \in \xReadCond{W}$, then $\npair[n']{A} \in \xReadCond{W}$.

* If $\npair{(w,w')} \in \lrvg{\trust}(W)$, then $\npair[n']{(w,w')} \in \lrvg{\trust}(W)$.

* If $\npair{(w,w')} \in \lrrg{\trust}(W)$, then $\npair[n']{(w,w')} \in \lrrg{\trust}(W)$.

* If $\memSatFStack{ms_\stk,\ms_T}{W}$, then $\memSatFStack[n']{ms_\stk,\ms_T}{W}$.

* If $\memSatStack{ms_\stk,\ms_T}{W}$, then $\memSatStack[n']{ms_\stk,\ms_T}{W}$.

* If $\npair{(\overline{\sigma},\ms_S,\ms_T)} \in \lrheap{\pwheap}(W)$, then $\npair[n']{(\overline{\sigma},\ms_S,\ms_T)} \in \lrheap{\pwheap}(W)$.

* $\memSat{(\ms_S,\stk,\ms_\stk,\ms_T)}{W}$, then also $\memSat[n']{(\ms_S,\stk,\ms_\stk,\ms_T)}{W}$.

The properties for $\readCond{}$, $\stackReadCond{}$, $\writeCond{}$, $\stackWriteCond{}$, $\execCond{}$, $\xReadCond{}$ follow easily by definition.
The property for $\lrv$ follows from the others and by definition.
The property for $\lrr$ follows directly from the one for $\lrv$.

The property for $\lrheap$, $\memSatFStack{\_,\_}{\_}$, $\memSatStack{\_,\_}{\_}$ follows by their definition from the quantifications over $n' < n$, and the property for $(\_,\_,\_,\_) :_n W$ follows from those.

If $W_1 \nequal W_2$ then

* $\purePart{W_1} \nequal \purePart{W_2}$

* If $W_1' \future W_1$ then there exists a $W_2'$ such that $W_2' \nequal W_1'$ and $W_2' \future W_2$.

* If $W_1' \oplus W_1$ is defined, then there exists a $W_2' \nequal W_1'$ and $W_2' \oplus W_2$ is defined.

* If $W_1 = W_1' \oplus W_1''$ then there exist $W_2' \nequal W_1'$ and $W_2'' \nequal W_1''$ such that $W_2 = W_2' \oplus W_2''$.

* If $W_1' \nequal W_2'$ then $W_1\oplus W_1' \nequal W_2 \oplus W_2'$.

* $\xi^{-1}(W_1) \nequal[n-1] \xi^{-1}(W_2)$

Easy to prove by unfolding definitions and making unsurprising choices for existentially quantified worlds.

If $W \nequal W'$, then

* $\readCond{W} \nequal \readCond{W'}$.

* If $\stackReadCond{\lin,W} \nequal \stackReadCond{\lin,W'}$.

* If $\writeCond{\lin,W} \nequal \writeCond{\lin,W'}$.

* If $\stackWriteCond{\lin,W} \nequal \stackWriteCond{\lin,W'}$

* If $\xReadCond{W} \nequal \xReadCond{W'}$.

* $\lre(W) \nequal \lre(W')$.

* $\lrexj(W) \nequal \lrexj(W')$.

* If $\execCond{\lin,W} \nequal \execCond{\lin,W'}$.

* If $\lrvg{\trust}(W) \nequal \lrvg{\trust}(W')$.

* If $\lrrg{\trust}(W) \nequal \lrrg{\trust}(W')$.

* If $\memSatFStack{ms_\stk,\ms_T}{W}$, then $\memSatFStack{ms_\stk,\ms_T}{W'}$.

* If $\memSatStack{ms_\stk,\ms_T}{W}$, then $\memSatStack{ms_\stk,\ms_T}{W'}$.

* If $\npair{(\overline{\sigma},\ms_S,\ms_T)} \in \lrheap{\pwheap}(W)$, then $\npair{(\overline{\sigma},\ms_S,\ms_T)} \in \lrheap{\pwheap[W']}(W')$.

* $\memSat{(\ms_S,\stk,\ms_\stk,\ms_T)}{W}$ iff $\memSat{(\ms_S,\stk,\ms_\stk,\ms_T)}{W'}$.

The properties for $\readCond{}$, $\stackReadCond{}$, $\writeCond{}$, $\stackWriteCond{}$, $\xReadCond{}$ follow from the fact that these are defined to use the world only for comparing regions using $\nequal$, $\nsubeq$ and $\nsupeq$.

The property for $\lre$ and $\lrexj$ follow from Lemma <ref>.

The property for $\execCond{}$ follows from Lemma <ref> and the property for $\lre$.

The property for $\lrv$ follows from the other properties, by definition, from Lemma <ref>, and non-expansiveness of regions.

The property of $\lrr$ follows from the one for $\lrv$.

The property for $\lrheap$, $\memSatFStack{\_,\_}{\_}$, $\memSatStack{\_,\_}{\_}$ and $(\_,\_,\_,\_) :_n W$ follows from the non-expansiveness of regions in the world and Lemma <ref>.

For all $n$, $W' \future W$, we have that

* If $(w_1,w_2) \in H_\sigma~\sigma~W$, then $(w_1,w_2) \in H_\sigma~\sigma~W'$.
This should hold for any valid $H_\sigma$, but we need to prove it for specific instantiations.

* If $\npair{(w_1,w_2)} \in \lrv(W)$, then $\npair{(w_1,w_2)} \in
\lrv(W')$.

* If $\npair{(\overline{\sigma},\ms_S,\ms_T)} \in \lrheap(\pwheap[W_1])(W)$, then $\npair{(\overline{\sigma},\ms_S,\ms_T)} \in
\lrheap(\pwheap[W_1])(W')$.

Follows from the definitions.
Note: the proof for $\lrheap$ relies on Lemma <ref>.

For all $\Phi_S$, $\Phi_T$, $\Phi_T'$, $j$, $n$, if

\[
\Phi_T \nstep[j]{} \Phi_T' \text{ and } \npair[n-j]{(\Phi_S,\Phi_T')} \in \lror,
\]

\[
\npair{(\Phi_S,\Phi_T)} \in \lror
\]

Special case of Lemma <ref>.

For all $\Phi_S$, $\Phi_T$, $\Phi_T'$, $j$, $n$, if

\[
\Phi_S \nstep[j]{\gc} \Phi_S' \text{ and } \npair[n-j]{(\Phi_S',\Phi_T)} \in \lrol,
\]

\[
\npair{(\Phi_S,\Phi_T)} \in \lrol
\]

Special case of Lemma <ref>.

For all $\Phi_S$, $\Phi_S'$, $\Phi_T$, $\Phi_T'$, $j_S,j_T$, $n$, if

* $\Phi_S \nstep[j_S]{\gc} \Phi_S'$

* $\Phi_T \nstep[j_T]{} \Phi_T'$

* $\npair{(\Phi_S',\Phi_T')} \in \lro$

\[
\npair[n+\min(j_S,j_T)]{(\Phi_S,\Phi_T)} \in \lro
\]

Our two languages are deterministicLemma needed for this, I guess.., so we have that $\Phi_S \sterm{\ta,\stkb}$ iff $\Phi_S \sterm{\ta,\stkb}$ and $\Phi_T \term$ iff $\Phi_T' \term$.
It is also easy to show that if $\Phi_S \sterm[i + \min(j_S,j_T)]{\ta,\stkb}$, then $\Phi_S' \sterm[i]{\ta,\stkb}$ and if $\Phi_T \term[i+\min(j_S,j_T)]$, then $\Phi_T' \term[i]$.
The result then follows easily by definition of $\lro[\preceq,\gc]$ and $\lro[\preceq,\gc]$.

\[
\npair{((\perm,\lin),\baddr,\eaddr,\aaddr),((\perm,\lin),\baddr,\eaddr,\aaddr)} \in \lrvg{\trust}(W)
\]

\[
\npair{((\perm,\lin),\baddr,\eaddr,\aaddr'),((\perm,\lin),\baddr,\eaddr,\aaddr')} \in \lrvg{\trust}(W)
\]

Direct form the definition of $\lrvg{\trust}$.

\[
\npair{((\stkptr{\perm,\baddr,\eaddr,\aaddr},(\perm,\lin),\baddr,\eaddr,\aaddr))} \in \lrvg{\trust}(W)
\]

\[
\npair{(\stkptr{\perm,\baddr,\eaddr,\aaddr'},((\perm,\lin),\baddr,\eaddr,\aaddr'))} \in \lrvg{\trust}(W)
\]

Direct from the definition of $\lrvg{\trust}$.

\[
\npair{(\seal{\sigma_\baddr,\sigma_\eaddr,\sigma},\seal{\sigma_\baddr,\sigma_\eaddr,\sigma})} \in \lrvg{\trust}(W)
\]

\[
\npair{(\seal{\sigma_\baddr,\sigma_\eaddr,\sigma'},\seal{\sigma_\baddr,\sigma_\eaddr,\sigma'})} \in \lrvg{\trust}(W)
\]

Direct from the definition of $\lrvg{\trust}$.

\[
\npair{((\perm,\lin),\baddr,\eaddr,\aaddr),((\perm,\lin),\baddr,\eaddr,\aaddr)} \in \lrvg{\trust}(W)
\]

\[
\perm' \sqsubseteq \perm
\]

\[
\npair{((\perm',\lin),\baddr,\eaddr,\aaddr),((\perm',\lin),\baddr,\eaddr,\aaddr)} \in \lrvg{\trust}(W)
\]

Direct from the definition of $\sqsubseteq$ and $\lrvg{\trust}$.

* $\npair{(c,c)} \in \lrvg{\trust}(W)$

* $c = ((\perm,\lin),\baddr,\eaddr,\aaddr)$

* $b \le s < e$

* $c_1 = ((\perm,\lin),\baddr,s,\aaddr)$

* $c_2 = ((\perm,\lin),s+1,\eaddr,\aaddr)$

* $c_3 = \linCons{c}$

* $\memSat{\ms_S,\stk,\ms_\stk,\ms_T}{W \oplus \purePart{W_1 \oplus W_2 \oplus W_3}}$

then there exist $W_1,W_2$,$W_3$ such that

* $W = W_1 \oplus W_2 \oplus W_3$

* $\npair{(c_1,c_1)} \in \lrvg{\trust}(W_1)$

* $\npair{(c_2,c_2)} \in \lrvg{\trust}(W_2)$

* $\npair{(c_3,c_3)} \in \lrvg{\trust}(W_3)$

If $\lin = \normal$, then we pick $W_3 = W$ and $W_1 = W_2 = \purePart{W_3}$ which easily satisfies $W = W_1 \oplus W_2 \oplus W_3$.

Assuming $\gc = (\ta,\gc,\gsigrets,\gsigcloss)$, we know by assumption $\npair{(c,c)} \in \lrvg{\trust}(W)$ that either

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

* $\ta \# [\addr,\eaddr]$

In the former case, the result follows from Lemma <ref> and Lemma <ref>.

In the latter case, we know that $[\baddr,s],[s+1,\eaddr] \neq \emptyset$ because $b \le s < e$, so the result follows from Lemma <ref> and Lemma <ref>.

If $\lin = \linear$, then
we know from $\npair{(c,c)} \in \lrvg{\trust}(W)$ and w.l.o.g we can assume

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

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

from this, we get $S_{\var{read}} \subseteq \addressable{\linear,\pwheap{W}}$ and
$R_{\var{read}} : S_{\var{read}} \fun \Worlds$ such that

* $\biguplus_{r\in S_{\var{read}}} R_{\var{read}}(r) \supseteq A$

* $\forall r\ldotp |R_{\var{read}}(r)|  = 1$

* $\forall r \in S_{\var{read}} \ldotp \pwheap(r).H \nsubeq \stdreg{R_{\var{read}}(r),\gc}{\pur}.H$

$S_{\var{write}} \subseteq \addressable{\linear,\pwheap{W}}$ and
$R_{\var{write}} : S_{\var{write}} \fun \Worlds$ such that

* $\biguplus_{r\in S_{\var{write}}} R_{\var{write}}(r) \supseteq A$

* $\forall r\ldotp |R_{\var{write}}(r)|  = 1$

* $\forall r \in S_{\var{write}} \ldotp \pwheap(r).H \nsupeq
\stdreg{R_{\var{write}}(r),\gc}{\pur}.H \wedge \pwheap(r) $ is address-stratified

Now we would like to show $R_{\var{read}}^{-1}([\baddr,\eaddr]) = R_{\var{write}}^{-1}([\baddr,\eaddr])$.
We know that the two sets are the same size as both $R$'s map to singleton sets.
This means that there exists $r \neq r'$ s.t. $R_{\var{read}}(r) =
R_{\var{write}}(r') = \{\aaddr'\}$ for $\aaddr' \in [\baddr,\eaddr]$.

By definition of the standard region, we know that for any $\hat{W}$ and any $\ms$ and $\ms'$ where $\npair[n-1]{(\ms,\ms')} \in \pwheap(r)$ we have $\dom(\ms)= \dom(\ms') = \{a'\}$.

By assumption $\pwheap(r)$ is address-stratified which means that for any $\hat{W}$ and any $\ms$ and $\ms'$ where $\npair[n-1]{(\ms,\ms')} \in \pwheap(r)$ we have $\dom(\ms)e= \dom(\ms') = \{a'\}$.

By the memory satisfaction, the memory must be split into disjointed parts that
each satisfy a region. With two regions that require a memory segment pair with
the same domain, we cannot satisfy all the regions, so we must have

Now pick $W_1$ as the world that owns $R_{\var{read}}^{-1}([\baddr,s])$, $W_2$
the world that owns $R_{\var{read}}^{-1}([s+1,\eaddr])$, and $W_3$ as the world
that owns the remaining regions of $W$.

It is clearly the case that $W = W_1 \oplus W_2 \oplus W_3$.

In this case, we need to show

\[
\npair{(0,0)} \in \lrvg{\trust}(W_3)
\]

which is trivially the case.

For the remaining, it suffices to show

* $\npair{[\baddr,s]} \in \readCond{\linear,W_1}$

* $\npair{[\baddr,s]} \in \writeCond{\linear,W_1}$

* $\npair{[s+1,\eaddr]} \in \readCond{\linear,W_2}$

* $\npair{[s+1,\eaddr]} \in \writeCond{\linear,W_2}$

which follows by assumption.

* $\npair{(c_S,c_T)} \in \lrvg{\trust}(W)$

* $c_S = \stkptr{\perm,\baddr,\eaddr,\aaddr}$

* $c_T = ((\perm,\linear),\baddr,\eaddr,\aaddr)$

* $b \le n \le e$

* $c_{1,S} = \stkptr{\perm,\baddr,n,\aaddr}$

* $c_{1,T} = ((\perm,\linear),\baddr,n,\aaddr)$

* $c_{2,S} = \stkptr{\perm,n,\eaddr,\aaddr}$

* $c_{2,T} = ((\perm,\linear),n,\eaddr,\aaddr)$

* $c_3 = 0$

then there exist $W_1,W_2$,$W_3$ such that

* $W = W_1 \oplus W_2 \oplus W_3$

* $\npair{(c_{1,S},c_{1,T})} \in \lrvg{\trust}(W_1)$

* $\npair{(c_{2,S},c_{2,T})} \in \lrvg{\trust}(W_2)$

* $\npair{(c_3,c_3)} \in \lrvg{\trust}(W_3)$

Similar to the proof of Lemma <ref>.

* $\npair{(c_1,c_1)} \in \lrvg{\trust}(W_1)$

* $\npair{(c_2,c_2)} \in \lrvg{\trust}(W_2)$

* $c_1 = ((\perm,\lin),\baddr,m,\aaddr)$

* $c_2 = ((\perm,\lin),m+1,\eaddr,\aaddr)$

* $c = ((\perm,\lin),\baddr,\eaddr,\aaddr)$

* $b \le m \le e$

* $c_1' = \linCons{c_1}$

* $c_2' = \linCons{c_2}$

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

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

then there exist $W_1',W_2',W_3'$ such that

* $W_1 \oplus W_2 = W_1' \oplus W_2' \oplus W_3'$

* $\npair{(c,c)} \in \lrvg{\trust}(W_3')$

* $\npair{(c_1',c_1')} \in \lrvg{\trust}(W_1')$

* $\npair{(c_2',c_2')} \in \lrvg{\trust}(W_2')$

From $\npair{(c_1,c_1)} \in \lrvg{\trust}(W_1)$ and $\npair{(c_2,c_2)} \in \lrvg{\trust}(W_2)$, it follows that either ($[b,m] \mathrel{\#} \ta$ or $[b,m] \subseteq \ta$) and also either ($[m+1,e] \mathrel{\#} \ta$ or $[m+1,e] \subseteq \ta$).

Consider first the case where either $[b,m] \subseteq \ta$ or $[m+1,e]\subseteq \ta$.
Then by definition of $\lrvg{\trust}$, we have that $\lin = \normal$, $\trust = \trusted$ and $\npair{[b,m]} \in \xReadCond{W_1}$ or $\npair{[m+1,e]} \in \xReadCond{W_2}$, respectively.
It follows by definition of $\xReadCond{}$ and $\codereg{}$ that $[\baddr-1,m+1]$ or $[m,\eaddr+1] \subseteq \ta$, respectively, so that it is impossible that $[m+1,\eaddr]\mathrel{\#} \ta$ or $[\baddr,m] \mathrel{\#} \ta$ respectively.
In other words, we must have that both $[b,m] \subseteq \ta$ and $[m+1,e]\subseteq \ta$.

From Lemma <ref>, it follows that also $\npair{[\baddr,\eaddr]}\in\xReadCond{W_1\oplus W_2}$ and from Lemma <ref>, it follows that $\npair{[\baddr,\eaddr]}\in\xReadCond{}(\purePart{W_1\oplus W_2})$.
Finally, we have that $\npair{(c,c)}\in\lrvg{\trust}(\purePart{W_1\oplus W_2})$.
We can take $W_3' = \purePart{W_1\oplus W_2}$, $W_1' = W_1$ and $W_2' = W_2$ and the remaining proof obligations follow by assumption and by Lemma <ref> and <ref>.

Now consider the case that both $[b,m] \mathrel{\#} \ta$ and $[m+1,e]\mathrel{\#} \ta$.
The results now follow by definition of $\lrv$, using Lemma <ref> and <ref>, taking $W_3' = W_1 \oplus W_2$ and $W_1' = \purePart{W_1}$ and $W_2' = \purePart{W_2}$.

* $\npair{(c_{1,S},c_{1,T})} \in \lrvg{\trust}(W_1)$

* $\npair{(c_{2,S},c_{2,T})} \in \lrvg{\trust}(W_2)$

* $b \le m \le e$

* $c_{1,S} = \stkptr{\perm,\baddr,m,\aaddr}$

* $c_{1,T} = ((\perm,\linear),\baddr,m,\aaddr)$

* $c_{2,S} = \stkptr{\perm,m+1,\eaddr,\aaddr}$

* $c_{2,T} = ((\perm,\linear),m+1,\eaddr,\aaddr)$

* $c_S = \stkptr{\perm,\baddr,\eaddr,\aaddr}$

* $c_T = ((\perm,\linear),\baddr,\eaddr,\aaddr)$

then we have that

* $\npair{(c_S,c_T)} \in \lrvg{\trust}(W_1 \oplus W_2)$

This follows easily by definition of $\lrv$ and using Lemma <ref>.

\[
\npair{(\stkptr{\perm,\baddr,\eaddr,\aaddr},((\perm,\lin),\baddr,\eaddr,\aaddr))} \in \lrvg{\trust}(W)
\]

\[
\perm' \sqsubseteq \perm
\]

\[
\npair{(\stkptr{\perm',\baddr,\eaddr,\aaddr},((\perm',\lin),\baddr,\eaddr,\aaddr))} \in \lrvg{\trust}(W)
\]

Follows directly from the definition.

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

* $\npair{(b,e)}\in\readCond{l,W}$

* $a \in [b,e]$

* $W \oplus W_M$ is defined

* $n' < n$

Then $\npair[n']{(\ms_S(a),\ms_T(a))} \in \lrv(W')$ for some $W'$ such that $W_M = W' \oplus W_M'$.
Additionally, if

* $\npair{(b,e)}\in\writeCond{l,W}$

Then $\memSat{(\ms_S[a\mapsto 0],\stk,\ms_\stk,\ms_T[a\mapsto 0])}{W_M'}$.

From $\npair{(b,e)}\in\readCond{l,W}$, we get an $S \subseteq \addressable{\lin,
\pwheap}$, an $R : S \rightarrow \powerset{\nats}$ with $\biguplus_{r \in S} R(r) \supseteq [\baddr,\eaddr]$ and $\pwheap(r).H
\nsubeq \stdreg{R(r),\gc}{\pur}.H$ for all $r \in S$.

Since $a \in [b,e]$, there is a unique $r \in S$ such that $a \in R(r)$.

Since $W \oplus W_M$ is defined, we have that $r \in \dom(\pwheap) =
\dom(\pwheap[W_M])$ and $\pwheap(r) \oplus \pwheap[W_M](r)$ is defined.

From $\memSat{(\ms_S,\stk,\ms_\stk,\ms_T)}{W_M}$, we get that
$\stk = (\opc_0,\ms_0):: \dots :: (\opc_m,\ms_m)$,
$\ms_S \uplus \ms_\stk \uplus \ms_0 \uplus \dots \uplus \ms_m$ is defined,
$W_M = W_{\var{stack}} \oplus W_{\var{free\_stack}} \oplus W_{\var{heap}}$ and
$\exists \ms_\var{T,stack}, \ms_\var{T,free\_stack}, \ms_\var{T,heap}$, $\ms_{T,f}$, $\ms_{S,f}$, $\ms_S'$ such that

* $\ms_S =\ms_{S,f} \uplus \ms_S'$

* $\ms_T = \ms_\var{T,stack} \uplus \ms_\var{T,free\_stack} \uplus
\ms_\var{T,heap} \uplus \ms_{T,f}$

* $\memSatStack{\stk,\ms_\var{T,stack}}{W_{\var{stack}}}$

* $\memSatFStack{\ms_\stk,\ms_\var{T,free\_stack}}{W_{\var{free\_stack}}}$

* $\npair{(\overline{\sigma},\ms_S',\ms_\var{T,heap})} \in \lrheap(W_M)(W_\var{heap})$.

From $\npair{(\overline{\sigma},\ms_S',\ms_\var{T,heap})} \in \lrheap(W_M)(W_\var{heap})$, we get an
$R_\ms : \dom(\activeReg{\pwheap[W_\var{heap}]}) \fun \MemSeg \times \MemSeg$,
$\ms_\var{T,heap} = \biguplus_{r \in \dom(\activeReg{\pwheap[W_\var{heap}]})} \pi_2(R_\ms(r))$,
$\ms_S = \biguplus_{r \in \dom(\activeReg{\pwheap[W_\var{heap}]})} \pi_1(R_\ms(r))$,
$\exists R_W : \dom(\activeReg{\pwheap[W_\var{heap}]}) \fun \World\ldotp$
$W_\var{heap} = \oplus_{r \in \dom(\activeReg{\pwheap[W_\var{heap}]})} R_W(r)$,
$\forall r \in \activeReg{\pwheap[W_M]}$, we have that
$\npair[n']{R_\ms(r)} \in  \pwheap[W_\var{heap}](r).H \; \xi^{-1}(R_W(r))$ for all $n' < n$.
We also get an $R_\var{seal} : \dom(\activeReg{\pwheap}) \fun \powerset{\Seal}$ such that  $\biguplus_{r \in \dom(\activeReg{\pwheap})} R_\var{seal}(r)) \subseteq \overline{\sigma}$ and $\dom(\pwheap(r).H_\sigma) = R_\var{seal}(r)$.

We have that $r \in \addressable{\lin, \pwheap} \subseteq
\activeReg{\pwheap[W_\var{heap}]}$, so $\npair[n']{R_\ms(r)} \in
\pwheap[W_M](r).H \; \xi^{-1}(R_W(r))$.
Because $\pwheap(r).H \nsubeq \stdreg{R(r),\gc}{\pur}.H$ and $W\oplus W_M$ is defined, it follows that
also $\pwheap[W_M](r).H \nsubeq \stdreg{R(r),\gc}{\pur}.H$. This
means that also $\npair[n']{R_\ms(r)} \in
H^{\mathrm{std}}_{R(r)}\; \xi^{-1}(R_W(r))$.

From this, it follows that $\dom(R_\ms(r).1) = \dom(R_\ms(r).2) = R(r)$ and we get a $S : R(r) \fun \World$ with $\xi(\xi^{-1}(R_W(r))) = \oplus_{\aaddr \in R(r)} S(\aaddr)$ and $\forall \aaddr \in R(r) \ldotp \npair[n']{(\ms_S(\aaddr),\ms_T(\aaddr))} \in \lrv(S(\aaddr))$.

Since $\aaddr \in R(r)$, we have that $\npair[n']{(\ms_S(\aaddr),\ms_T(\aaddr))} \in \lrv(S(\aaddr))$ and
we can take $W_M' = W_r' \oplus W_{\var{heap}}' \oplus (W_{\var{stack}} \oplus W_{\var{free\_stack}})$ with $W_r' = \oplus_{\aaddr \in (R(r)\setminus \{\aaddr\})} S(\aaddr)$ and $W_\var{heap}' = \oplus_{r' \in (\dom(\activeReg{\pwheap[W_\var{heap}]})\setminus \{r\})} R_W(r')$, and get

\begin{align*}
S(\aaddr) \oplus W_M'
&=S(\aaddr) \oplus (W_r' \oplus W_\var{heap}'\oplus (W_{\var{stack}} \oplus W_{\var{free\_stack}}))\\
\oplus_{\aaddr \in R(r)} S(\aaddr) \oplus W_{\var{heap}}'\oplus (W_{\var{stack}} \oplus W_{\var{free\_stack}})\\
\xi(\xi^{-1}(R_W(r))) \oplus W_\var{heap}'\oplus (W_{\var{stack}} \oplus W_{\var{free\_stack}})\\
R_W(r) \oplus W_\var{heap}'\oplus (W_{\var{stack}} \oplus W_{\var{free\_stack}})\\
\oplus_{r \in \dom(\activeReg{\pwheap[W_\var{heap}]})} R_W(r)\oplus (W_{\var{stack}} \oplus W_{\var{free\_stack}})\\
W_\var{heap} \oplus (W_{\var{stack}} \oplus W_{\var{free\_stack}})\\
&= W_M
\end{align*}

Additionally, if $\npair{(b,e)}\in\writeCond{l,W}$, then
we get an $S'\subseteq \addressable{\lin, \pwheap} \subseteq \activeReg{\pwheap[W_M]}$, an $R' : S' \fun \powerset{\nats}$ such that $\biguplus_{r \in S'} R'(r) \supseteq [\baddr,\eaddr]$ and
for all $r \in S'$, $\pwheap(r).H \nsupeq \stdreg{R'(r),\gc}{\pur}.H$ and
$\pwheap(r)$ is address-stratified.

Since $a \in [b,e]$, there is an $r' \in S'$ such that $a \in R'(r')$ .

Because $W \oplus W_M$ is defined, it follows that also
$\pwheap[W_M](r').H \nsupeq \stdreg{R'(r'),\gc}{\pur}.H$ and
$\pwheap[W_M](r') $ is address-stratified.

It follows that $r = r'$ because $\dom(R_\ms(r).1) = \dom(R_\ms(r).2) = R(r) \ni a$ and $\dom(R_\ms(r').2) = \dom(R_\ms(r').1) = R'(r') \ni a$ and all the $R_\ms(r).1$ and $R_\ms(r).2$ are disjoint.

We have that $\npair[n']{(R_\ms(r).1\update{a}{0},R_\ms(r).2\update{a}{0})} \in \pwheap[W_\var{heap}](r).H \; \xi^{-1}(W_r')$ for all $n' < n$ because $\pwheap[W_M](r)$ is address-stratified and $\pwheap[W_M](r).H \nsupeq \stdreg{R'(r),\gc}{\pur}.H$.

From this, it follows that $\npair{(\overline{\sigma},\ms_S\update{a}{0},\ms_\var{T,heap}\update{a}{0})} \in \lrheap(W_M)(W_r' \oplus W_\var{heap}')$ and finally

\begin{equation*}
\npair{(\overline{\sigma},\ms_S\update{a}{0},\stk,\ms_\stk,\ms_T\update{a}{0})} \in \lrheap(W_M')(W_r' \oplus W_{\var{heap}}')
\end{equation*}

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

* $\npair{(b,e)}\in\stackReadCond{W}$

* $a \in [b,e]$

* $W \oplus W_M$ is defined

* $n' < n$

Then $\npair[n']{(\ms_\stk(a),\ms_T(a))} \in \lrv(W')$ for some $W'$ such that $W_M = W' \oplus W_M'$.
Additionally, if

* $\npair{(b,e)}\in\stackWriteCond{W}$

Then $\memSat{(\ms_S,\stk,\ms_\stk[a\mapsto 0],\ms_T[a\mapsto 0])}{W_M'}$.

From $\npair{(b,e)}\in\stackReadCond{W}$, we get an $S \subseteq \addressable{\lin,
\pwfree}$, an $R : S \rightarrow \powerset{\nats}$ with $\biguplus_{r \in S} R(r) \supseteq [\baddr,\eaddr]$ and $\pwfree(r).H
\nsubeq \stdreg{R(r),\gc}{\pur}.H$ for all $r \in S$.

Since $a \in [b,e]$, there is a unique $r \in S$ such that $a \in R(r)$.

Since $W \oplus W_M$ is defined, we have that $r \in \dom(\pwfree) =
\dom(\pwfree[W_M])$ and $\pwfree(r) \oplus \pwfree[W_M](r)$ is defined.

From $\memSat{(\ms_S,\stk,\ms_\stk,\ms_T)}{W_M}$, we get that
$\stk = (\opc_0,\ms_0):: \dots :: (\opc_m,\ms_m)$,
$\ms_S \uplus \ms_\stk \uplus \ms_0 \uplus \dots \uplus \ms_m$ is defined,
$W_M = W_{\var{stack}} \oplus W_{\var{free\_stack}} \oplus W_{\var{heap}}$ and
$\exists \ms_\var{T,stack}, \ms_\var{T,free\_stack}, \ms_\var{T,heap}$, $\ms_{T,f}$, $\ms_{S,f}$, $\ms_S'$ such that

* $\ms_S =\ms_{S,f} \uplus \ms_S'$

* $\ms_T = \ms_\var{T,stack} \uplus \ms_\var{T,free\_stack} \uplus
\ms_\var{T,heap} \uplus \ms_{T,f}$

* $\memSatStack{\stk,\ms_\var{T,stack}}{W_{\var{stack}}}$

* $\memSatFStack{\ms_\stk,\ms_\var{T,free\_stack}}{W_{\var{free\_stack}}}$

* $\npair{(\overline{\sigma},\ms_S',\ms_\var{T,heap})}\in\lrheap(\pwheap[W_M])(W_\var{heap})$.

From $\memSatFStack{\ms_\stk,\ms_\var{T,free\_stack}}{W_{\var{free\_stack}}}$, we get an

* $R_\ms : \dom(\activeReg{\pwfree[W_\var{free\_stack}]}) \fun \MemSeg \times \MemSeg$,

* $\ms_\var{T,free\_stack} = \biguplus_{r \in \dom(\activeReg{\pwfree[W_\var{free\_stack}]})} \pi_2(R_\ms(r))$,

* $\ms_\stk = \biguplus_{r \in \dom(\activeReg{\pwfree[W_\var{free\_stack}]})} \pi_1(R_\ms(r))$,

* $\stkb \in \dom(\ms_\var{T,free\_stack}) \wedge \stkb \in \dom(\ms_\stk)$,

* $\exists R_W : \dom(\activeReg{\pwfree[W_\var{free\_stack}]}) \fun \World\ldotp$

* $W_\var{free\_stack} = \oplus_{r \in \dom(\activeReg{\pwfree[W_\var{free\_stack}]})} R_W(r)$

and for all
$r \in \activeReg{\pwfree[W_\var{free\_stack}]}$, we have that
$\npair[n']{R_\ms(r)} \in  \pwfree[W_\var{free\_stack}](r).H \; \xi^{-1}(R_W(r))$ for all $n' < n$.

We have that $r \in \addressable{\lin, \pwfree} \subseteq \activeReg{\pwfree[W_\var{free\_stack}]}$, so $\npair[n']{R_\ms(r)} \in \pwfree[W_\var{free\_stack}](r).H \; \xi^{-1}(R_W(r))$.
Because $\pwfree(r).H \nsubeq \stdreg{R(r),\gc}{\pur}.H$ and $W\oplus W_M = W \oplus (W_\var{free\_stack} \oplus W_\var{free\_stack} \oplus W_\var{stack})$ is defined, it follows that also $\pwfree[W_\var{free\_stack}](r).H \nsubeq \stdreg{R(r),\gc}{\pur}.H$.
This means that also $\npair[n']{R_\ms(r)} \in H^{\mathrm{std}}_{R(r)}\; \xi^{-1}(R_W(r))$.

From this, it follows that $\dom(R_\ms(r).1) = \dom(R_\ms(r).2) = R(r)$ and we get a $S : R(r) \fun \World$ with $\xi(\xi^{-1}(R_W(r))) = \oplus_{\aaddr \in R(r)} S(\aaddr)$ and $\forall \aaddr \in R(r) \ldotp \npair[n']{(\ms_\stk(\aaddr),\ms_T(\aaddr))} \in \lrv(S(\aaddr))$.

Since $\aaddr \in R(r)$, we have that $\npair[n']{(\ms_\stk(\aaddr),\ms_T(\aaddr))} \in \lrv(S(\aaddr))$ and
we can take $W_M' = W_r' \oplus W_{\var{heap}} \oplus (W_{\var{stack}} \oplus W_{\var{free\_stack}}')$ with $W_r' = \oplus_{\aaddr \in (R(r)\setminus \{\aaddr\})} S(\aaddr)$ and $W_\var{free\_stack}' = \oplus_{r' \in (\dom(\activeReg{\pwheap[W_\var{heap}]})\setminus \{r\})} R_W(r')$, and get

\begin{align*}
S(\aaddr) \oplus W_M'
&=S(\aaddr) \oplus (W_r' \oplus W_{\var{free\_stack}}' \oplus (W_{\var{stack}}\oplus W_\var{heap}))\\
\oplus_{\aaddr \in R(r)} S(\aaddr) \oplus W_{\var{free\_stack}}' \oplus (W_{\var{stack}}\oplus W_{\var{heap}})\\
\xi(\xi^{-1}(R_W(r))) \oplus W_{\var{free\_stack}}' \oplus (W_{\var{stack}} \oplus W_\var{heap})\\
R_W(r) \oplus W_{\var{free\_stack}}' \oplus (W_{\var{stack}} \oplus W_\var{heap})\\
\oplus_{r \in \dom(\activeReg{\pwheap[W_\var{free\_stack}]})} R_W(r)\oplus (W_{\var{stack}} \oplus W_{\var{heap}})\\
W_\var{free\_stack} \oplus (W_{\var{stack}} \oplus W_{\var{heap}})\\
&= W_M
\end{align*}

Additionally, if $\npair{(b,e)}\in\stackWriteCond{W}$, then
we get an

\begin{equation*}
S'\subseteq \addressable{\lin, \pwfree} \subseteq \activeReg{\pwheap[W_\var{free\_stack}]} \text{,}
\end{equation*}

and an $R' : S' \fun \powerset{\nats}$ such that $\biguplus_{r \in S'} R'(r) \supseteq [\baddr,\eaddr]$ and
for all $r \in S'$, $\pwfree(r).H \nsupeq \stdreg{R'(r),\gc}{\pur}.H$ and
$\pwfree(r)$ is address-stratified.

Since $a \in [b,e]$, there is an $r' \in S'$ such that $a \in R'(r')$ .

Because $W \oplus W_M$ is defined, it follows that also
$\pwfree[W_\var{free\_stack}](r').H \nsupeq \stdreg{R'(r'),\gc}{\pur}.H$ and
$\pwfree[W_\var{free\_stack}](r')$ is address-stratified.

It follows that $r = r'$ because $\dom(R_\ms(r).1) = \dom(R_\ms(r).2) = R(r) \ni a$ and $ \dom(R_\ms(r').2) = \dom(R_\ms(r').1) = R'(r') \ni a$ and all the $R_\ms(r).1$ and $R_\ms(r).2$ are disjoint.

We have that $\npair[n']{(R_\ms(r).1\update{a}{0},R_\ms(r).2\update{a}{0})} \in \pwfree[W_\var{free\_stack}](r).H \; \xi^{-1}(W_r')$ for all $n' < n$ because $\pwfree[W_\var{free\_stack}](r)$ is address-stratified and $\pwfree[W_\var{free\_stack}](r).H \nsupeq \stdreg{R'(r),\gc}{\pur}.H$.

From this, it follows that $\memSatFStack{\ms_\stk\update{a}{0},\ms_\var{T,heap}\update{a}{0}}{W_r' \oplus W_\var{free\_stack}'}$ and finally $\memSat{(\ms_S,\stk,\ms_\stk\update{a}{0},\ms_T\update{a}{0})}{W_M'}$.

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

* $c = ((\perm,\lin),\baddr,\eaddr,\aaddr)$

* $c' = ((\perm',\lin'),\baddr',\eaddr',\aaddr')$

* $\perm \in \readAllowed{}$, $\perm' \in \readAllowed{}$

* $\npair{(c,c')}\in\lrvg{\trust}(H_\sigma,W)$

* $W \oplus W_M$ is defined

* $n' < n$

* $w_S = \linCons{\ms_S(\aaddr)}$, $w_T = \linCons{\ms_T(\aaddr')}$

* $\linConsPerm{\perm}{\ms_S(\aaddr)}$, $\linConsPerm{\perm'}{\ms_T(\aaddr')}$

* $\aaddr \in [\baddr,\eaddr]$

* $\aaddr' \in [\baddr',\eaddr']$

Then $\exists W', W_M'\ldotp$

* $W_M = W' \oplus W_M'$

* $\memSat[n']{(\ms_S\update{\aaddr}{w_S},\stk,\ms_\stk,\ms_T\update{\aaddr'}{w_T})}{W_M'}$

* $\npair[n']{(\ms_S(\aaddr),\ms_T(\aaddr'))} \in \lrvg{\trust}(W')$

Consider first the case that $\npair{(c,c')}\in\lrv(W)$.

From $\npair{(c,c')}\in\lrv(H_\sigma,W)$ with $c = ((\perm,\lin),\baddr,\eaddr,\aaddr)$, $c' = ((\perm',\lin'),\baddr',\eaddr',\aaddr')$, $\perm \in \readAllowed{}$ and $\perm' \in \readAllowed{}$, we get that $\baddr = \baddr'$, $\eaddr = \eaddr'$ and $\aaddr = \aaddr'$ and $\npair{(\baddr,\eaddr)} \in \readCond{\lin,W}$.

Lemma <ref> then gives us a $W'$ and $W_M'$ such that $W_M = W' \oplus W_M'$ and $\npair[n']{(\ms_S(\aaddr),\ms_T(\aaddr'))} \in \lrv(W')$.

it remains to prove that $\memSat[n']{(\ms_S\update{\aaddr}{w_S},\stk,\ms_\stk,\ms_T\update{\aaddr'}{w_T})}{W_M'}$.
We have to distinguish the case that $\isLinear{\ms_S(\aaddr)}$ and the opposite case.

* case $\isLinear{\ms_S(\aaddr)}$: then $\linCons{\ms_S(\aaddr)} = 0$ and it follows from $\npair[n']{(\ms_S(\aaddr),\ms_T(\aaddr'))}\in\lrv(W)$ that also $\isLinear{\ms_T(\aaddr')}$ and $\linCons{\ms_T(\aaddr')} = 0$.

From $\linConsPerm{\perm}{\ms_S(\aaddr)}$ and $\linConsPerm{\perm'}{\ms_T(\aaddr')}$, we then also get that $\perm,\perm' \in \writeAllowed{}$ and from $\npair{(c,c')}\in\lrv(W)$, it then follows that $\npair{(\baddr,eaddr)} \in \writeCond{\lin,W}$.
From the “Additionally, if..” case in Lemma <ref> with Lemma <ref>, we then get that $\memSat[n']{(\ms_S\update{\aaddr}{w_S},\stk,\ms_\stk,\ms_T\update{\aaddr'}{w_T})}{W_M'}$.

* case $\neg\isLinear{\ms_S(\aaddr)}$: then $\linCons{\ms_S(\aaddr)} = \ms_S(\aaddr)$ and it follows from $\npair[n']{(\ms_S(\aaddr),\ms_T(\aaddr'))}\in\lrv(W)$ that also $\neg\isLinear{\ms_T(\aaddr')}$ Do we need a lemma for this?
and $\linCons{\ms_T(\aaddr')} = \ms_T(\aaddr')$.
The fact that $\memSat[n']{(\ms_S\update{\aaddr}{w_S},\stk,\ms_\stk,\ms_T\update{\aaddr'}{w_T})}{W_M'}$ then follows simply by downwards closure of memory satisfaction, i.e. Lemma <ref>.

Now consider the case that $\npair{(c,c')}\in(\lrvg{\trusted}(W) \setminus \lrv(W))$. then we have that $[b,e] \subseteq \ta$ and $\npair{[b,e]} \in \xReadCond{W}$.
By definition of $\xReadCond{}$, there is an $r_a$ such that $\pwheap(r) \nequal \codereg{\_,\_,\code,\gc}$, $a \in \dom(\code)$.
By definition of $\codereg{}$ and using the fact that $\dom(\code) \ni a \in [b,e] \subseteq \ta$, we know that $\dom(\code) \subseteq \ta$ and $\_,\_\vdash_{\mathrm{comp-code}} \code$.
From the fact that $\memSat{(\ms_S,\stk,\ms_\stk,\ms_T)}{W_M}$, together with the definition of $\codereg{}$, we know that $\npair[n']{(\Phi.\mem(a),\Phi.\mem(a))} \in \lrvg{\trusted}(\purePart{W_M})$ and we have that $\purePart{W_M} = \purePart{W}$ by Lemma <ref>.
From the fact that $\_,\_\vdash_{\mathrm{comp-code}} \code$, we get that $\neg \isLinear{\code(a)}$.

We can then take $W_M' = W_M$, $W' = W$ and get the required results from what we have proven above and using Lemma <ref>.

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

* $c = \stkptr{\perm,\baddr,\eaddr,\aaddr}$

* $c' = ((\perm',\lin'),\baddr',\eaddr',\aaddr')$

* $\perm \in \readAllowed{}$ or $\perm' \in \readAllowed{}$

* $\npair{(c,c')}\in\lrvg{\trust}(H_\sigma,W)$

* $W \oplus W_M$ is defined

* $n' < n$

* ($\aaddr \in [\baddr,\eaddr]$ or $\aaddr' \in [\baddr',\eaddr']$)

* $w_S = \linCons{\ms_S(\aaddr)}$, $w_T = \linCons{\ms_T(\aaddr')}$

* $\linConsPerm{\perm}{\ms_S(\aaddr)}$, $\linConsPerm{\perm'}{\ms_T(\aaddr')}$

Then $\exists W', W_M'\ldotp$

* $W_M = W' \oplus W_M'$

* $\memSat[n']{(\ms_S,\stk,\ms_\stk\update{\aaddr}{w_S},\ms_T\update{\aaddr'}{w_T})}{W_M'}$

* $\npair[n']{(\ms_\stk(a),\ms_T(a))} \in \lrv(W')$

From $\npair{(c,c')}\in\lrv(H_\sigma,W)$ with $c = \stkptr{\perm,\baddr,\eaddr,\aaddr}$, $c' = ((\perm',\lin'),\baddr',\eaddr',\aaddr')$, ($\perm \in \readAllowed{}$ or $\perm' \in \readAllowed{}$), we get that $\perm = \perm'$, $\lin' = \linear$, $\baddr = \baddr'$, $\eaddr = \eaddr'$ and $\aaddr = \aaddr'$ and $\npair{(\baddr,\eaddr)} \in \stackReadCond{W}$.

From Lemma <ref>, we then get that $\npair[n']{(\ms_\stk(a),\ms_T(a))}\in\lrv(W')$ for some $W'$ such that $W_M = W' \oplus W_M'$.

It remains to prove that $\memSat{(\ms_S,\stk,\ms_\stk\update{\aaddr}{w_S},\ms_T\update{\aaddr'}{w_T})}{W_M'}$.
We have to distinguish the case that $\isLinear{\ms_\stk(\aaddr)}$ and the opposite case.

* case $\isLinear{\ms_\stk(\aaddr)}$: then $\linCons{\ms_\stk(\aaddr)} = 0$ and it follows from

\begin{equation*}
\npair[n']{(\ms_\stk(a),\ms_T(a))}\in\lrv(H_\sigma,W)
\end{equation*}

that also $\isLinear{\ms_T(\aaddr')}$ Do we need a lemma for this? and $\linCons{\ms_T(\aaddr')} = 0$.
From $\linConsPerm{\perm}{\ms_S(\aaddr)}$ and $\linConsPerm{\perm'}{\ms_T(\aaddr')}$, we then also get that $\perm = \perm' \in \writeAllowed{}$ and from $\npair{(c,c')}\in\lrvg{\trust}(H_\sigma,W)$, it then follows that $\npair{(\baddr,eaddr)} \in \stackWriteCond{W}$.
From the “Additionally, if..” case in Lemma <ref> with Lemma <ref>, we then get that $\memSat[n']{(\ms_S,\stk,\ms_\stk\update{\aaddr}{0},\ms_T\update{\aaddr'}{0})}{W_M'}$.

* case $\neg\isLinear{\ms_\stk(\aaddr)}$: then $\linCons{\ms_\stk(\aaddr)} = \ms_\stk(\aaddr)$ and it follows from

\begin{equation*}
\npair[n']{(\ms_\stk(a),\ms_T(a))}\in\lrv(H_\sigma,W)
\end{equation*}

that also $\neg\isLinear{\ms_T(\aaddr')}$ Do we need a lemma for this?
and $\linCons{\ms_T(\aaddr')} = \ms_T(\aaddr')$.
The fact that $\memSat[n']{(\ms_S\update{\aaddr}{w_S},\stk,\ms_\stk,\ms_T\update{\aaddr'}{w_T})}{W_M'}$ then follows simply by downwards closure of memory satisfaction, i.e. Lemma <ref>.

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

* $c_1 = ((\perm,\lin),\baddr,\eaddr,\aaddr)$

* $c_1' = ((\perm',\lin'),\baddr',\eaddr',\aaddr')$

* $\perm \in \writeAllowed{}$, $\perm' \in \writeAllowed{}$

* $\aaddr \in [\baddr,\eaddr]$

* $\aaddr' \in [\baddr',\eaddr']$

* $\npair{(c_1,c_1')}\in\lrvg{\trusted}(H_\sigma,W_1)$

* $\npair{(c_2,c_2')}\in\lrv(H_\sigma,W_2)$

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

* $n' < n$

* $c_3 = \linCons{c_2}$, $c_3' = \linCons{c_2'}$

Then $\exists W_2', W_M'\ldotp$

* $W_2 \oplus W_M = W_2' \oplus W_M'$

* $\memSat[n']{(\ms_S\update{\aaddr}{c_2},\stk,\ms_\stk,\ms_T\update{\aaddr'}{c_2'})}{W_M'}$

* $\npair[n']{(c_3,c_3')} \in \lrv(W_2')$

From $\npair{(c_1,c_1')}\in\lrvg{\trusted}(W_1)$ and $\perm \in \writeAllowed{}$, it follows that $c_1 = c_1'$ and $\npair{[b,e]} \in \writeCond{\lin,W_1}$.

We then get a $r$ and $A$, such that $a \in A$, $\pwheap[W_1](r).H \nsupeq \stdreg{A,\gc}{v}.H$ and $\pwheap[W_1](r)$ is address-stratified.

If we decompose the judgement that $\memSat{(\ms_S,\stk,\ms_\stk,\ms_T)}{W_M}$, then we get some $\npair[n-1]{\ms_S|_A, \ms_T|_A} \in \stdreg{A,\gc}{v}.H~W_{M,A}$ for some $W_M = W_{M,A} \oplus W_{M,R}$.
If we define $W_M'$ as $W_M \oplus W_2$ and $W_2' = \purePart{W_2}$, then we can use the properties about $\pwheap[W_1](r)$ above to show that  $\memSat[n']{(\ms_S\update{\aaddr}{c_2},\stk,\ms_\stk,\ms_T\update{\aaddr'}{c_2'})}{W_M'}$.
The fact that $\npair[n']{(c_3,c_3')} \in \lrv(W_2')$ follows from Lemma <ref>.

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

* $c_1 = \stkptr{\perm,\baddr,\eaddr,\aaddr}$

* $c_1' = ((\perm',\linear),\baddr',\eaddr',\aaddr')$

* $\perm \in \writeAllowed{}$, $\perm' \in \writeAllowed{}$

* $\aaddr \in [\baddr,\eaddr]$

* $\aaddr' \in [\baddr',\eaddr']$

* $\npair{(c_1,c_1')}\in\lrvg{\trusted}(H_\sigma,W_1)$

* $\npair{(c_2,c_2')}\in\lrv(H_\sigma,W_2)$

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

* $n' < n$

* $c_3 = \linCons{c_2}$, $c_3' = \linCons{c_2'}$

Then $\exists W_2', W_M'\ldotp$

* $W_2 \oplus W_M = W_2' \oplus W_M'$

* $\memSat[n']{(\ms_S,\stk,\ms_\stk\update{\aaddr}{c_2},\ms_T\update{\aaddr'}{c_2'})}{W_M'}$

* $\npair[n']{(c_3,c_3')} \in \lrv(W_2')$

From $\npair{(c_1,c_1')}\in\lrvg{\trusted}(W_1)$ and $\perm \in \writeAllowed{}$, it follows that $\perm = \perm'$, $\baddr = \baddr'$, $\eaddr = \eaddr'$, $\aaddr = \aaddr'$ and $\npair{[b,e]} \in \stackWriteCond{W_1}$.

We then get a $r$ and $A$, such that $a \in A$, $\pwfree[W_1](r).H \nsupeq \stdreg{A,\gc}{v}.H$ and $\pwfree[W_1](r)$ is address-stratified.

If we decompose the judgement that $\memSat{(\ms_S,\stk,\ms_\stk,\ms_T)}{W_M}$, then we get some $\npair[n-1]{\ms_\stk|_A, \ms_T|_A} \in \stdreg{A,\gc}{v}.H~W_{M,A}$ for some $W_M = W_{M,A} \oplus W_{M,R}$.
If we define $W_M'$ as $W_M \oplus W_2$ and $W_2' = \purePart{W_2}$, then we can use the properties about $\pwfree[W_1](r)$ above to show that  $\memSat[n']{(\ms_S,\stk,\ms_\stk\update{\aaddr}{c_2},\ms_T\update{\aaddr'}{c_2'})}{W_M'}$.
The fact that $\npair[n']{(c_3,c_3')} \in \lrv(W_2')$ follows from Lemma <ref>.

* $\npair{(\sealed{\sigma,\vsc_1},\sealed{\sigma,\vsc_1'})} \in \lrvg{\trust}(W_{R,1})$

* $\npair{(\sealed{\sigma,\vsc_2},\sealed{\sigma,\vsc_2'})} \in \lrvg{\trust}(W_{R,2})$

* $\nonExec{\vsc_1'}$ and $\nonExec{\vsc_2'}$

* $W_{R,1} \oplus W_{R,2} \oplus W_M$ is defined

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

* $\npair[n-1]{(\vsc_1,\vsc_2,\vsc_1',\vsc_2')} \in \lrexj(W_{R,1}\oplus W_{R,2})$

From $\npair{(\sealed{\sigma,\vsc_1},\sealed{\sigma,\vsc_1'})} \in \lrvg{\trust}(W_{R,1})$, we know that

* $(\isLinear{\src{\vsc_1}} \text{ iff } \isLinear{\vsc_1'})$

* $\exists r \in \dom(\pwheap), \sigrets,\sigcloss,\mscode \ldotp$

* $\pwheap[W_{R,1}](r) = (\pure,\_,H_\sigma)$

* $H_\sigma \nequal H^\mathrm{code,\square}_\sigma \; \sigrets \; \sigcloss \; \mscode \; \gc$

* $\npair[n']{\stpair[.]{\vsc_1}{\vsc_1'}} \in H_\sigma \; \sigma \; \xi^{-1}(W_{R,1})$ for all $n' < n$

* If $(\isLinear{\src{\vsc_1}}$ then for all $W' \future W_{R,1}$, $W_o$, $n' < n$, $\npair[n']{\stpair[.]{\vsc_2}{\vsc_2'}} \in H_\sigma \; \sigma \; \xi^{-1}(W_o)$, we have that

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

* If $(\nonLinear{\src{\vsc_1}}$ then for all $W' \future \purePart{W_{R,1}}$, $W_o$, $n' < n$, $\npair[n']{\stpair[.]{\vsc_2}{\vsc_2'}} \in H_\sigma \; \sigma \; \xi^{-1}(W_o)$, we have that

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

From $\npair{(\sealed{\sigma,\vsc_2},\sealed{\sigma,\vsc_2'})} \in \lrvg{\trust}(W_{R,2})$, we know that

* $(\isLinear{\src{\vsc_2}} \text{ iff } \isLinear{\vsc_2'})$

* $\exists r' \in \dom(\pwheap), \sigrets,\sigcloss,\mscode \ldotp$

* $\pwheap[W_{R,2}](r') = (\pure,\_,H_\sigma)$

* $H_\sigma \nequal H^\mathrm{code,\square}_\sigma \; \sigrets \; \sigcloss \; \mscode \; \gc$

* $\npair[n']{\stpair[.]{\vsc_2}{\vsc_2'}} \in H_\sigma \; \sigma \; \xi^{-1}(W_{R,2})$ for all $n' < n$

From $\memSat{\ms_S,\stk,\ms_\stk,\ms_T}{W_M}$, we know that two different regions cannot have $H_\sigma$ defined for the same $\sigma$, so that $r = r'$.
Both when $\isLinear{\vsc_1}$ and when $\nonLinear{\vsc_1}$ (using Lemma <ref>), we know that for all $W' \future W_{R,1}$, $W_o$, $n' < n$, $\vsc_2$, $\vsc_2'$, $\npair[n']{\stpair[.]{\vsc_2}{\vsc_2'}} \in H_\sigma \; \sigma \; \xi^{-1}(W_o)$, we have that

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

We can now instantiate this fact with $W' = W_{R,1}$, $W_o = W_{R,2}$, $n' = n-1$, and the fact that $\npair[n-1]{\stpair[.]{\vsc_2}{\vsc_2'}} \in H_\sigma \; \sigma \; \xi^{-1}(W_{R,2})$ (see above) to conclude

\begin{equation*}
\npair[n-1]{\src{\vsc_1},\src{\vsc_2},\vsc_1',\vsc_2'} \in \lrexj(W_{R,1}\oplus W_{R,2})\text{.}
\end{equation*}

§.§ FTLR proof

* One of the following sets of requirements holds:

* $\trust = \trusted$, $\Phi_S$ is reasonable up to $n$ steps and $[\baddr,\eaddr] \subseteq \ta$

* $\trust = \untrusted$ and $[b,e] \mathrel{\#} \ta$ and $\npair{[\baddr,\eaddr]} \in \readCond{\normal,W_\pcreg}$

* $\Phi_S(\pcreg) = \Phi_T(\pcreg) = ((\rx,\normal),\baddr,\eaddr,a)$

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

* $\npair{(\Phi_S.\reg,\Phi_T.\reg)} \in \lrrg{\trust}(W_R)$

* $\memSat{\Phi_S.\mem,\Phi_S.\stk,\Phi_S.\ms_\stk,\Phi_T.\mem}{W_M}$

* $W_\pcreg \oplus W_R \oplus W_M$ is defined.

* Theorem <ref> holds for all $n' < n$.

\[
\npair{(\Phi_S,\Phi_T)} \in \lro
\]

In the following we will use the following: $\reg_S = \Phi_S.\reg$, $\reg_T = \Phi_T.\reg$, $\ms_S = \Phi_S.\mem$, $\ms_\stk = \Phi_S.\ms_\stk$, and $\stk = \Phi_S.\stk$.

By complete induction on $n$, i.e. we can assume that the lemma already holds for $n' < n$.

In order to prove this, we first, we prove that one of the following holds:

*  $\Phi_S \nstep[j]{\gc} \failed$ and $\Phi_T
\step[i] \failed$ for some $i$,$j$.

*  $\Phi_S \step[\gc] \halted$ and $\Phi_T \step\halted$

*  All of the following hold: (includes simple cases: gettype, geta, getb,
gete, getp, getl, lt, plus, minus, one case of move that can be handled

* $\Phi_S \step[\gc] \Phi_S'$

* $\Phi_T \step \Phi_T'$

* $\Phi_S$ does not point to $\scall{\offpc,\offsigma}{r_1}{r_2}$ or $\txjmp{r_1}{r_2}$

* $\Phi_S' = \updPcAddr{\Phi_S\updReg{r}{z}} \neq \failed$

* $\Phi_T' = \updPcAddr{\Phi_T\updReg{r}{z}} \neq \failed$

* $r \neq \pcreg$

* $z \in \ints$

*  All of the following hold:

* $\callCond{\Phi_S,r_1,r_2,\offpc,\offsigma,\aaddr}$

* $r_1 \neq \rtmp{1}$ and $r_2 \neq \rtmp{1}$

* $\baddr \leq \aaddr \tand \aaddr + \calllen-1 \leq \eaddr$

* $\exec{\Phi_S(\pcreg)}$

* for all $i = 0..\calllen-1$, $\ms_T(\aaddr+i) = \ms_S(\aaddr+i) \in \ints$.

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

* $\Phi_S \step[\gc] \Phi_S' \neq \failed$

* $\Phi_T \step \Phi_T' \neq \failed$

* $\Phi_S(r_1) = \sealed{\sigma,c_1}$

* $\Phi_S(r_2) = \sealed{\sigma,c_2}$

* $\nonExec{c_2}$

* $\Phi_S(\rstk) = \stkptr{\rw, \baddr_\stk, \eaddr_\stk, \aaddr_\stk}$

* $\baddr_\stk < \aaddr_\stk \leq \eaddr_\stk$

* $\Phi_S(\pcreg) = ((\perm,\normal),\baddr,\eaddr,\aaddr)$

* $w_1 = \linCons{c_1}$ and $w_2 = \linCons{c_2}$

\[
\begin{split}
\Phi_S''.\reg = \Phi_S.reg      &[\rstk \mapsto \stkptr{\rw,\baddr_\stk,\aaddr_\stk-1,\aaddr_\stk-1}] \\
&[\rretc \mapsto \sealed{\sigma',\retptrc(\baddr,\eaddr,\aaddr+\calllen)}]\\
&[\rretd \mapsto \sealed{\sigma',\retptrd(\aaddr_\stk,\eaddr_\stk)}] \\
&[r_1,r_2 \mapsto w_1,w_2] \\
&[\rtmp{1} \mapsto 0]
\end{split}
\]

* $\Phi_S''.\mem = \Phi_S.\mem$

* $\ms_{\stk\_\priv,S} = \Phi_S.\ms_\stk |_{[\aaddr_\stk,\eaddr_\stk]}\update{\aaddr_\stk}{42}$

* $\Phi_S''.\stk = ((\aaddr+\calllen),\ms_{\stk\_\priv,S}) :: \Phi_S.\stk$

* $\Phi_S''.\ms_\stk = \Phi_S.\ms_\stk -
\Phi_S.\ms_\stk|_{[\aaddr_\stk,\eaddr_\stk]}$

* $\baddr \leq \aaddr+\offpc \leq \eaddr$

* $\mem(\aaddr+\offpc) = \seal{\sigma_\baddr,\sigma_\eaddr,\sigma_\aaddr}$

* $\sigma' = \sigma_\aaddr + \offsigma$

* $\sigma_\aaddr \leq \sigma' \leq \sigma_\eaddr$

* $\Phi_S' =\var{xjumpResult}\left(c_1,c_2, \Phi_S'' \right)$

*  All of the following hold: (includes cap-manipulation cases: move, cca,
restrict, seta2b, cseal, split, splice, that can be handled mostly

* $\Phi_S \step[\gc] \Phi_S'$

* $\Phi_T \step \Phi_T'$

* $\Phi_S$ does not point to $\scall{\offpc,\offsigma}{r_1}{r_2}$ or $\txjmp{r_1}{r_2}$

* $\Phi_S' = \updPcAddr{\Phi_S\updReg{r_1\cdots r_k}{w_1\cdots w_k}}\neq
\failed$

* $\Phi_T' = \updPcAddr{\Phi_T\updReg{r_1\cdots r_k}{w_1'\cdots w_k'}}
\neq \failed$

* $r_i \neq \pcreg$ for all $i$

* One of the following holds:

*  (restrict,cca,seta2b) $w_1 = ((\perm',\lin),\baddr,\eaddr,\aaddr')$,
$w_1' = ((\perm',\lin),\baddr,\eaddr,\aaddr')$, $\Phi_S(r_1) =
((\perm,\lin),\baddr,\eaddr,\aaddr)$ and $\Phi_T(r_1) =
((\perm,\lin),\baddr,\eaddr,\aaddr)$ and $\perm' \sqsubseteq\perm$, $k =

* (restrict,cca,seta2b)

* $w_1 = \stkptr{\perm',\baddr,\eaddr,\aaddr'}$,

* $w_1' = ((\perm',\linear),\baddr,\eaddr,\aaddr')$,

* $\Phi_S(r_1) = \stkptr{\perm,\baddr,\eaddr,\aaddr}$ and

* $\Phi_T(r_1) = ((\perm,\linear),\baddr,\eaddr,\aaddr)$ and

* $\perm' \sqsubseteq\perm$,

* $k = 1$

* (cca,seta2b) $w_1 = \seal{\sigma_\baddr,\sigma_\eaddr,\sigma'}$,
$w_1' = \seal{\sigma_\baddr,\sigma_\eaddr,\sigma'}$, $\Phi_S(r_1) =
\seal{\sigma_\baddr,\sigma_\eaddr,\sigma}$ and $\Phi_T(r_1) =
\seal{\sigma_\baddr,\sigma_\eaddr,\sigma}$, $k = 1$

* (move) $w_1 = \Phi_S(r_2)$, $w_1' = \Phi_T(r_2)$, and $w_2 = \linCons{w_1}$, $w_2' = \linCons{w_1'}$ and $r_1 \neq r_2$ and $k = 2$.

* (cseal) $w_1 = \sealed{\sigma,\Phi_S(r_1)}$, $w_1' = \sealed{\sigma,\Phi_T(r_1)}$, $\Phi_S(r_2) = \Phi_T(r_2) = \seal{\sigma_\baddr,\sigma_\eaddr,\sigma}$, $\sigma_\baddr \le \sigma \le \sigma_\eaddr$, and $k=1$, and $\Phi_S$ points to $\src{\tcseal{r_1}{r_2}}$.

*  (split) $\Phi_T(r_3) = \Phi_S(r_3) =
((\perm,\lin),\baddr,\eaddr,\aaddr)$, $\baddr \leq s$, $s < \eaddr$,
$w_1 = w_1' = ((\perm,\lin),\baddr,n,\aaddr)$, $w_2 = w_2' =
((\perm,\lin),n+1,\eaddr,\aaddr)$, $w_3 = w_3' = \linCons{\Phi_S(r_3)}$, $k=3$.

*  (split) $\Phi_T(r_3) = \Phi_S(r_3) =
\seal{\sigma_\baddr,\sigma_\eaddr,\sigma}$, $\sigma_\baddr \leq s$, $s <
\sigma_\eaddr$, $w_1 = w_1' = \seal{\sigma_\baddr,s,\sigma}$, $w_2 =
w_2' = \seal{s+1,\sigma_\eaddr,\sigma}$, $k=2$.

*  (split) $\Phi_S(r_3) = \stkptr{\perm,\baddr,\eaddr,\aaddr}$,
$\Phi_T(r_3) = ((\perm,\linear),\baddr,\eaddr,\aaddr)$, $\baddr \leq n$,
$n < \eaddr$, $w_1 = \stkptr{\perm,\baddr,n,\aaddr}$, $w_1' =
((\perm,\linear),\baddr,n,\aaddr)$, $w_2 =
\stkptr{\perm,n+1,\eaddr,\aaddr}$,

$w_2' = ((\perm,\linear),n+1,\eaddr,\aaddr)$, $k=2$.

* (splice) $\Phi_T(r_2) = ((\perm,\linear),\baddr_2,\eaddr_2,\_)$,
$\Phi_S(r_2) = \stkptr{\perm,\baddr_2,\eaddr_2,\_}$, and

$\Phi_T(r_3) =
((\perm,\linear),\eaddr_2+1,\eaddr_3,\aaddr_3)$, $\Phi_S(r_3) =
\stkptr{\perm,\eaddr_2+1,\eaddr_3,\aaddr_3}$, and $\baddr_2 \leq
\eaddr_2$, and $\eaddr_2+1 \leq \eaddr_3$, and
$w_1=((\perm,\linear),\baddr_2,\eaddr_3,\aaddr_3)$, $w_1'=
\stkptr{\perm,\baddr_2,\eaddr_3,\aaddr_3}$, and $w_2 = w_2' = w_3 = w_3'
= 0$, and $k=3$

* (splice)

* $\Phi_T(r_2) = \Phi_S(r_2) = ((\perm,\lin),\baddr_2,\eaddr_2,\_)$,

* $\Phi_T(r_3) = \Phi_S(r_3) =
((\perm,\lin),\eaddr_2+1,\eaddr_3,\aaddr_3)$, and

* $\baddr_2 \leq
\eaddr_2$, and

* $\eaddr_2+1 \leq \eaddr_3$, and

* $w_1=w_1'=((\perm,\lin),\baddr_2,\eaddr_3,\aaddr_3)$, and

* $w_2 = w_2'
= \linCons{\Phi_S(r_2)}$ and

* $w_3 = w_3' = \linCons{\Phi_S(r_3)}$, and

* $k=3$

*  (splice) $\Phi_T(r_2) = \Phi_S(r_2) =
\seal{\sigma_{\baddr,2},\sigma_{\eaddr,2},\_}$, and $\Phi_T(r_3) =
\Phi_S(r_3) =
\seal{\sigma_{\eaddr,2}+1,\sigma_{\eaddr,3},\sigma_{\aaddr,3}}$, and
$\sigma_{\baddr,2} \leq \sigma_{\eaddr,2}$, and $\sigma_{\eaddr,2} + 1
\leq \sigma_{\eaddr,3}$and $w_1 = w_1' = \seal{\sigma_{\baddr,2},
\sigma_{\eaddr,3}, \sigma}$

*  (jnz zero case, noop move) $k = 0$

*  All of the following hold: (includes memory-manipulation cases: store,
load, that can be handled mostly uniformly)

* $\Phi_S \step[\gc] \Phi_S'$

* $\Phi_T \step \Phi_T'$

* $\Phi_S$ does not point to $\scall{\offpc,\offsigma}{r_1}{r_2}$ or $\txjmp{r_1}{r_2}$

* $\Phi_S' =
\updPcAddr{\Phi_S\updReg{r_1,r_2}{w_1,w_2}\update{\mem.\aaddr}{w}}$

* $\Phi_T' =
\updPcAddr{\Phi_T\updReg{r_1',r_2'}{w_1',w_2'}\update{\mem.\aaddr}{w'}}$

* $r_i \neq \pcreg$ for all $i$

* One of the following hold:

* (store) $w_1 = w_1' = \Phi_S(r_1) = \Phi_T(r_1) =
((\perm,\lin),\baddr,\eaddr,\aaddr)$, and $\perm \in \writeAllowed{}$,
$\withinBounds{w_1}$, and

$w = \Phi_S(r_2)$, and $w' = \Phi_T(r_2)$, and $w_2 = \linCons{\Phi_S(r_2)}$, $w_2' = \linCons{\Phi_T(r_2)}$.

* (load) $w_2 = w_2' = \Phi_T(r_2) = \Phi_S(r_2) =
((\perm,\lin),\baddr,\eaddr,\aaddr)$, and $\perm \in \readAllowed{}$,
$\withinBounds{((\perm,\lin),\baddr,\eaddr,\aaddr)}$, and

$w_1 = \Phi_S.\mem(\aaddr)$, and $w_1' = \Phi_T.\mem(\aaddr)$, and

$w = \linCons{w_1}$, $w' = \linCons{w_1'}$, $\linConsPerm{\perm}{w_1}$, $\linConsPerm{\perm}{w_1'}$

*  All of the following hold: (includes memory-manipulation cases: store,
load, that can be handled mostly uniformly (stack))

* $\Phi_S \step[\gc]\Phi_S'$

* $\Phi_T \step \Phi_T'$

* $\Phi_S$ does not point to $\scall{\offpc,\offsigma}{r_1}{r_2}$ or $\txjmp{r_1}{r_2}$

* $\Phi_S' =
\updPcAddr{\Phi_S\updReg{r_1,r_2}{w_1,w_2}\update{\ms_\stk.\aaddr}{w}}$

* $\Phi_T' =
\updPcAddr{\Phi_T\updReg{r_1',r_2'}{w_1',w_2'}\update{\ms_\stk.\aaddr}{w'}}$

* $r_i \neq \pcreg$ for all $i$

* One of the following hold:

* (store) $w_1 = \Phi_T(r_1) =
((\perm,\linear),\baddr,\eaddr,\aaddr)$, $w_1' = \Phi_S(r_1) =
\stkptr{\perm,\baddr,\eaddr,\aaddr}$, and $\perm \in \writeAllowed{}$,
$\withinBounds{w_1}$, and

$w = \Phi_S(r_2)$, and $w' = \Phi_T(r_2)$, and $w_2 = \linCons{\Phi_S(r_2)}$, $w_2' = \linCons{\Phi_T(r_2)}$.

* (load) $w_2' = \Phi_T(r_2) =
((\perm,\linear),\baddr,\eaddr,\aaddr)$, and $w_2 = \Phi_S(r_2) =
\stkptr{\perm,\baddr,\eaddr,\aaddr}$, and $\perm \in \readAllowed{}$,
$\withinBounds{((\perm,\lin),\baddr,\eaddr,\aaddr)}$, and $\aaddr \in
\dom(\Phi.\ms_\stk)$, and $\aaddr \in \dom(\Phi.\ms_\stk)$, and

$w_1 = \Phi_S.\ms_\stk(\aaddr)$, and $w_1' = \Phi_T.\ms_\stk(\aaddr)$, and $w = \linCons{w_1}$, $w' = \linCons{w_1'}$, $\linConsPerm{\perm}{w_1}$ and $\linConsPerm{\perm}{w_1'}$.

*  All of the following hold: (includes control-flow manipulation cases:
jmp, jnz, xjmp, that can be handled mostly uniformly)

* $\Phi_S \step[\gc] \Phi_S'$

* $\Phi_T \step \Phi_T'$

* $\Phi_S$ does not point to $\scall{\offpc,\offsigma}{r_1}{r_2}$ or $\txjmp{r_1}{r_2}$

* One of the following holds

* (jmp,jnz)

* $\Phi_S' = \Phi_S\updReg{\pcreg,r_1}{\Phi_S(r_1),w_1}$ and

* $\Phi_T' = \Phi_T\updReg{\pcreg,r_1'}{\Phi_T(r_1),w_1'}$ and

* $\Phi_S(r_1) = \Phi_T(r_1) = ((\perm_1,\lin_1),\baddr_1,\eaddr_1,\aaddr_1)$,

* $\exec{\Phi_S(r_1)}$,

* $\withinBounds{\Phi_S(r_1)}$,

* $w_1 = \linCons{\Phi_S(r_1)}$ and

* $w_1' = \linCons{\Phi_T(r_1)}$

* (xjmp)

* $\Phi_S(r_1) = \sealed{\sigma,c_1}$ and

* $\Phi_S(r_2) = \sealed{\sigma,c_2}$ and

* $\Phi_T(r_1) = \sealed{\sigma,c_1'}$ and

* $\Phi_T(r_2) = \sealed{\sigma,c_2'}$ and

* $c_1' \neq \retptrc(\_)$ and

* $c_2' \neq \retptrd(\_)$ and

* $\nonExec{\Phi_S(r_2)}$ and

* $\nonExec{\Phi_T(r_2)}$ and

* $\Phi_S'' = \Phi_S\updReg{r_1,r_2}{\linCons{c_1},\linCons{c_2}}$ and

* $\Phi_S' = \xjumpResult{c_1}{c_2}{\Phi_S''}$ and

* $\Phi_T'' = \Phi_T\updReg{r_1,r_2}{\linCons{c_1'},\linCons{c_2'}}$ and

* $\Phi_T' = \xjumpResult{c_1'}{c_2'}{\Phi_T''}$

The above follows from a careful analysis of the cases of the operational semantics, using the following facts:

* $[b,e] \subseteq \ta$ or $[b,e] \mathrel{\#} \ta$ (by assumption of this lemma)

* $\Phi_S.\reg(\pcreg) = \Phi_T.\reg(\pcreg)$ (by assumption of this lemma)

* $\Phi_S.\mem(a) = \Phi_T.\mem(a)$ if $a \in [b,e]$: follows from
$\npair{[\baddr,\eaddr]} \in \xReadCond{W_\pcreg}$, the fact that $W_\pcreg
\oplus W_R \oplus W_M$ is defined and

* $\Phi_S.\mem(a\cdots a+\calllen-1) = \Phi_T.\mem(a \cdots a+\calllen -1)$ if $[a\cdots a+\calllen-1] \subseteq [b,e]$ (follows similarly).

* $\Phi_S.\reg(r) = ((\perm_1,\lin_1),\baddr_1,\eaddr_1,\aaddr_1)$ implies that $\Phi_S.\reg(r) = \Phi_T.\reg(r)$ and $a_1 \in \dom(\Phi_S.\mem)$ (follows from $\npair{(\Phi_S.\reg,\Phi_T.\reg)} \in \lrrg{\trust}(W_R)$).

* $\Phi_S.\reg(r) = z$ implies that $\Phi_S.\reg(r) = \Phi_T.\reg(r)$ (follows from $\npair{(\Phi_S.\reg,\Phi_T.\reg)} \in \lrrg{\trust}(W_R)$).

* $\Phi_S.\reg(r) = \seal{\sigma_b,\sigma_e,\sigma}$ implies that $\Phi_S.\reg(r) = \Phi_T.\reg(r)$ (follows from $\npair{(\Phi_S.\reg,\Phi_T.\reg)} \in \lrrg{\trust}(W_R)$).

* $\Phi_S.\reg(r) = \sealed{\sigma,\vsc}$ implies that $\Phi_T.\reg(r) = \sealed{\sigma,\vsc'}$ (follows from $\npair{(\Phi_S.\reg,\Phi_T.\reg)} \in \lrrg{\trust}(W_R)$).

* $\Phi_S.\reg(r) \neq \retptrd(\_,\_)$ (follows from $\npair{(\Phi_S.\reg,\Phi_T.\reg)} \in \lrrg{\trust}(W_R)$).

* $\Phi_S.\reg(r) \neq \retptrc(\_,\_,\_)$ (follows from $\npair{(\Phi_S.\reg,\Phi_T.\reg)} \in \lrrg{\trust}(W_R)$).

* $\Phi_S.\reg(r) = \stkptr{\perm_1,\baddr_1,\eaddr_1,\aaddr_1}$ implies that $\Phi_T.\reg(r) = ((\perm_1,\linear),b_1,e_1,a_1)$ and $a \in \dom(\Phi_S.\ms_\stk)$ (follows from $\npair{(\Phi_S.\reg,\Phi_T.\reg)} \in \lrrg{\trust}(W_R)$).

* Similar facts about the current address, base and end pointer, permissions and linearity of all register capabilities being equal (follows from $\npair{(\Phi_S.\reg,\Phi_T.\reg)} \in \lrrg{\trust}(W_R)$).

By the above observation, we know that $\Phi_S \step[\gc] \Phi_S'$ and $\Phi_T \step
\Phi_T'$ for some $\Phi_S'$ and $\Phi_T'$.
According to Lemma <ref>, it suffices to show:

\[
\npair[n-1]{(\Phi_S',\Phi_T')} \in \lro
\]

Consider each of the possible cases:

In case <ref>, both executions go to $\failed$.
In this case, the result follows vacuously by definition of $\lro[\preceq,\gc]$ and $\lro[\preceq,\gc]$.

In case <ref>, both source and target configuration halts in 0
steps, so both directions of $\lro$ are trivially satisfied.

In case <ref>, we use the induction hypothesis to conclude

\[
\npair[n-1]{(\Phi_S',\Phi_T')} \in \lro
\]

from the following facts:

* One of the following sets of requirements holds:

* $\trust = \trusted$, $\Phi_S$ is reasonable up to $n-1$ steps and $[\baddr,\eaddr] \subseteq \ta$

* $\trust = \untrusted$ and $[b,e] \mathrel{\#} \ta$ and $\npair[n-1]{[\baddr,\eaddr]} \in \readCond{\normal,W_\pcreg}$

This follows from the corresponding assumption of this lemma, the fact that $\Phi_S \step[\gc] \Phi_S'$ and $\Phi_S$ does not point to $\scall{\offpc,\offsigma}{r_1}{r_2}$ or $\txjmp{r_1}{r_2}$ and <ref>.

* $\Phi_S'(\pcreg) = \Phi_T'(\pcreg) = ((\rx,\normal),\baddr,\eaddr,\_)$:
Follows from the definition of $\updPcAddr{}$ and the assumptions of this case.

* $\npair[n-1]{[\baddr,\eaddr]} \in \xReadCond{W_\pcreg}$:
Follows from the corresponding assumption of this lemma using Lemma <ref>.

* $\npair[n-1]{(\Phi_S.\reg,\Phi_T.\reg)} \in \lrrg{\trust}(W_R)$:
Follows from the corresponding assumption of this lemma using Lemma <ref>, the definition of $\lrr$ and the fact that integers are always in $\lrvg{\trust}$ by definition.

* $\memSat[n-1]{\Phi_S.\mem,\Phi_S.\ms_\stk,\Phi_S.\stk,\Phi_T.\mem}{W_M}$:
Follows from the corresponding assumption of this lemma using Lemma <ref>.

* Theorem <ref> holds for all $n'' < n-1$:
follows from the corresponding assumption of this lemma, since $n - 1 < n$.

In case <ref>, we may assume $r_1 \neq r_2$[If the register contains a data capability, then the execution fails in the step after the jump. If it is an executable capability, then the xjump fails as it does not permit executable capabilities for the data part.] and $r_i \neq \pcreg$ for $i \in \{1,2\}$[The pc is executable which causes the xjump to fail.] as this will cause the execution to fail.
We need to let the target execution catch up.
That is $\Phi_T' \nstep[15]{} \Phi_T''$ for

\[
\Phi_T'' = \Phi_T
\begin{array}[t]{l}
\update{\mem.\aaddr_\stk}{42} \\
\updReg{\rstk}{((\rw,\linear),\baddr_\stk,\aaddr_\stk-1,\aaddr_\stk-1)} \\
\updReg{\rretd}{\sealed{\sigma',((\rw,\linear),\aaddr_\stk,\eaddr_\stk,\aaddr_\stk-1)}} \\
\updReg{\rretc}{\sealed{\sigma',((\perm,\normal),\baddr,\eaddr,\aaddr+\retoffset)}} \\
\updReg{\rtmp{1}}{0}\\
\updReg{r_1,r_2}{\linCons{\Phi_T(r_1)},\linCons{\Phi_T(r_2)}}\\
\updReg{\pcreg}{c_1'}\\
\updReg{\rdata}{c_2'}
\end{array}
\]

where $\Phi_T(r_i) = \sealed{\sigma,c_i'} \text{ for $i\in\{1,2\}$}$ and $\retoffset = 15$ which is the offset to the return code.
Now using Lemma <ref> again, it suffices to show

\[
\npair[n-1]{(\Phi_S',\Phi_T'')} \in \lro
\]

By assumption, we have $\npair[n]{(\reg_S(r_i),\reg_T(r_i))} \in \lrvg{\trust}(W_{R,i})$ for some $W_{R,i}$ with $i \in \{1,2\}$.
We know the capabilities in $r_1$ and $r_2$ are sealed capabilities, and by
Lemma <ref> and the definition of $\lrvg{\trust}$ we get
$\npair[n-1]{(c_2,c_2')} \in H_\sigma \; \sigma \; \xi^{-1}(W_{R,2})$
and w.l.o.g.

\begin{equation}
\forall W' \future W_{R,1}, W_o, n' < n, \npair[n']{(c_2,c_2')} \in H_\sigma \; \sigma \; \xi^{-1}(W_o) \ldotp \npair[n']{c_1,c_2,c_1',c_2'} \in \lrexj(W'\oplus W_o)\label{eq:ftlr:call:sealed-code-assump}
\end{equation}

Now take $W_o = W_{R,2}$, take $n' = n-1$ and construct $W_{R,1}'$ as follows:

By Lemma <ref> and the safety assumption on the register-file, there exists $S \supseteq [\baddr_\stk, \eaddr_\stk]$ such that for some $R : S \fun \powerset{\nats}$ we have $\biguplus_{r \in S} R(r) \supseteq [\baddr_\stk,\eaddr_\stk]$ and for all $r \in S$, $\pwfree[W_{R,1}](r).H \nequal \stdreg{R(r),\gc}{\pur}.H$ and $|R(r)| = 1$ and $\pwfree[W_{R,1}](r)$ is address-stratified.
Now take $r_\var{priv\_stk}$ fresh and define

\[
W_{R,1}' = W_{R,1}[\free.R^{-1}([\aaddr_\stk,\eaddr_\stk]) \mapsto \revoked][\priv.r_\var{priv\_stk} \mapsto (\stareg[(\ms_{\stk\_\priv,S},\Phi_T''.\mem|_{[\aaddr_\stk,\eaddr_\stk]}),\gc]{\spa,\square},\aaddr+\calllen)]
\]

We know $W_{R,1}' \future W_{R,1}$ as the revoked regions must have been $\spatial$ in $W_{R,q}$ (as they are owned by the part of the world assigned to the stack-register in the register-file relation).
The static region for the private stack is an extension of the old world.

Pick this world as $W'$ in Eq <ref>.
Let $W_{R,2}'$ be the same world but with the ownership of $W_{R,2}$ and pick it for $W_o$.
Now observe that also $W_{R,2}' \future W_{R,2}$ and use monotonicity of $H_\sigma$ with the above facts to get

\[
\npair[n-1]{c_1,c_2,c_1',c_2'} \in \lrexj(W_{R,1}'\oplus W_{R,2}')
\]

Now pick register files and memories such that they form $\Phi_S''$ (defined in
the assumptions) and $\Phi_T''$ and for $W_R'$ and $W_M'$ (we define them below) show

*  $W_{R,1}'\oplus W_{R,2}' \oplus W_R' \oplus W_M'$ is defined.

*  $\npair[n-1]{(\Phi_S''.\reg,\Phi_T''.\reg)} \in \lrr(\{\rdata\})(W_R')$

*  $\memSat[n-1]{\Phi_S''.\mem,\Phi_S''.\stk,\Phi_S''.\ms_\stk,\Phi_T''.\mem}{W_M'}$

to get

\[
\npair[n-1]{(\Phi_S',\Phi_T'')} \in \lro
\]

as desired.

It remains to show <ref>-<ref>, but first we note that we can deduce the following: From the assumption $\npair{[\baddr,\eaddr]} \in \xReadCond{W}$ we get $r \in \addressable{\normal, \pwheap}$ and $\mscode$ such that $\dom(\mscode) \supseteq [\baddr,\eaddr]$ and $\pwheap(r) \nequal \codereg{\sigrets',\_,\mscode,\gc}$.
Further by $\memSat{\ms_S,\stk,\ms_\stk,\ms_T}{W}$, we know that

\begin{equation}
\npair{(\mscode\uplus\mspad,\mscode\uplus\mspad)} \in H^{\var{code}} \; \sigrets' \; \sigcloss' \; \mscode \; (\ta,\_,\gsigrets,\gsigcloss)~ W_r\label{eq:ftlr:rretd:Hcode}
\end{equation}

where $\sigma' \in \sigrets'$ and $\dom(\mscode) \supseteq [\baddr,\eaddr]$ and $\aaddr + \offpc \in \dom(\mscode)$ and $W = W_r \oplus \_$.
That is: $\mscode$ contains the call we are considering.
This also entails

\begin{equation}
\label{eq:ftlr:code-comp-jud}
\sigrets',\sigcloss' \vdash_\var{code\_comp} \mscode
\end{equation}

from <ref> we also get

* $\dom(\mscode\uplus\mspad) \subseteq \ta$

Otherwise we would have $\dom(\mscode\uplus\mspad) \# \ta$ which would contradict $\ta\supseteq [b,e] \subseteq\dom(\mscode\uplus\mspad)$

* $\sigrets' \subseteq \gsigrets$

Follows from the above.

TODO: Make the above more precise and possibly put into a lemma (also needed in the next case).

Case <ref>: Pick $W_R'$ and $W_M'$ to have the regions of $W_{R,1}'$, but where $W_R'$ owns $r_\var{priv\_stk}$ and otherwise has the ownership of $W_R$ and $W$ with the exception of the regions owned by $W_{R,1}'$ and $W_{R,2}'$.
$W_M'$ has the ownership of $W_M$.
Case <ref> follows from assumption $W \oplus W_R \oplus W_M$.
The only changes to the worlds is that some ownership has been shifted from $W_R$ to $W_{R,1}$ and $W_{R,2}$ and the ownership for $W$ now belongs to $W_R'$.
In other words, no ownership has been duplicated.

Case <ref>:

First, from reasonability of $\Phi_S$, we get that $\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$.
Lemma <ref> then tells us that
$\npair[n-1]{(\Phi_S.\reg,\Phi_T.\reg)} \in \lrr(W_R)$.

We then need to split the ownership of $W_R'$.
From assumption $\npair[n]{(\Phi_S.reg,\Phi_T.\reg)} \in \lrr(W_R)$, we get a way to split the ownership of $W_R$.
We take this as the starting point, but with the following changes: regions $r_1$ and $r_2$ maps to worlds with no ownership (i.e. $\purePart{W_{R,1}'}$).
region $\rstk$ maps to a world with the same ownership, but of course without the now revoked regions.
Region $\rretd$ maps to a world that owns private $r_\var{priv\_stk}$ region.
Finally, $\rretc$ maps to a world with the ownership of $W$.

we split the world in the same way for the registers that remain unchanged, and we get from Lemma <ref> and <ref> that
$\npair[n-1]{(\Phi_S''.\reg,\Phi_T''.\reg)} \in \lrrg{\trust}(\{\rdata,\rstk,\rtmp{1},r_1,r_2,\rretd,\rretc\})(W_R'')$ for the appropriate $W_R''$.

To obtain $\npair[n-1]{(\Phi_S''.\reg,\Phi_T''.\reg)} \in \lrr(\{\rdata\})(W_R')$, it remains to prove the following cases:

Case $\rstk$: Show:

\[
\npair[n-1]{(\stkptr{\rw,\baddr_\stk,\aaddr_\stk-1,\aaddr_\stk-1},((\rw,\linear),\baddr_\stk,\aaddr_\stk-1,\aaddr_\stk-1))} \in \lrv(W_{R,\rstk}')
\]

We know by Assumption $\npair[n]{(\Phi_S.reg,\Phi_T.\reg)} \in \lrrg{\trust}(W_R)$, we know

\[
\npair[n]{(\stkptr{\rw,\baddr_\stk,\eaddr_\stk,\aaddr_\stk},((\rw, \linear), \baddr_\stk ,\eaddr_\stk, \aaddr_\stk)} \in \lrvg{\trust}(W_{R,\stk})
\]

which by the $\mathit{stackReadCondition}$ gives $S \subseteq \addressable{\linear,\pwfree}$ and $R : S \fun \powerset{\nats}$.
We need to pick an $S'$ to argue

\[
\npair[n-1]{[\baddr_\stk,\aaddr_\stk-1]} \in \stackReadCond{W_{R,\rstk}'}
\]

To this end pick $S' = R^{-1}(\left(\bigcup_{r\in S} R(r) \right) \setminus [\aaddr_\stk,\eaddr_\stk])$ and $R'$ to be $R$ limited to $S'$.
As we exclude all the revoked regions and the ownership otherwise remains the
same in $W_{R,\rstk}'$ as in $W_{R,\rstk}$, the regions in $S'$ are exactly the same in the new world as they were in $W_{R,\rstk}$.
So what we need to show follows immediately from

\[
\npair[n]{[\baddr_\stk,\eaddr_\stk]} \in \stackReadCond{W_{R,\rstk}}
\]

and by Lemma <ref>.

We show

\[
\npair[n-1]{[\baddr_\stk,\aaddr_\stk-1]} \in \stackWriteCond{W_{R,\rstk}'}
\]

in the same way.

Case $\rtmp{1}$: Show:

\[
\npair[n-1]{(0,0)} \in \lrv(W_{R,\rtmp{1}}')
\]

Follows immediately from the definition.

Case $r_1$,$r_2$: The two cases are symmetric, so we just show the $r_1$ case:

\[
\npair[n-1]{(\linCons{c_1},\linCons{\Phi_T(r_1)})} \in \lrv(W_{R,r_1}')
\]

Follows from the related register files assumption and Lemma <ref> and the fact that for sealed capabilities if they are in $\lrvg{\trusted}$, then they are in the $\lrv$ part.

Case $\rretd$: We have to show

\[
\npair[n-1]{(\sealed{\sigma',\retptrd(\aaddr_\stk,\eaddr_\stk)},\sealed{\sigma',((\rw,\linear),\aaddr_\stk,\eaddr_\stk,\aaddr_\stk-1)})} \in \lrv(W_{R,\rretd}')
\]

where $W_{R,\rretd}'$ is the part of $W_R'$ with ownership over $r_\var{priv\_stk}$.

Use the $r=r_{\mscode}$ as the witness.
The $\xReadCond{}$ gives us $\pwheap(r) \nequal \codereg{\_,\_,\mscode,\gc}$.
As it is a pure region, it is also present in the future world we consider.
We now have to show:

* for $n'' < n-1$ we have

\[\npair[n'']{\left(\array{l}\retptrd(\aaddr_\stk,\eaddr_\stk),\\((\rw,\linear),\aaddr_\stk,\eaddr_\stk,\aaddr_\stk-1)\endarray\right)}
\in H^\mathrm{code,\square}_\sigma \; \sigrets' \; \sigcloss' \; \mscode'
\; (\ta,\stkb) \; \sigma' \; \xi^{-1}(W_{R,\rretd}')
\]

First, we already know $\dom(\mscode) \subseteq \ta$ and $\sigrets' \subseteq \gsigrets$.
Now pick $r_\var{priv\_stk}$ as the witness.
We immediately get $\dom(\ms_{\stk\_\priv,S}) = \dom(\Phi_T''.\mem|_{[\aaddr_\stk,\eaddr_\stk]}) = [\aaddr_\stk,\eaddr_\stk]$.
Next, $\decInstr{\mscode'(\aaddr,\aaddr+\calllen-1)} = \overline{\scall{\offpc,\offsigma}{r_1}{r_2}}$ follows from $\callCond{\Phi_S,r_1,r_2,\offpc,\offsigma,\aaddr}$.
Finally, $\ms_\code(\aaddr+\offpc) = \seal{\sigma_\baddr,\sigma_\eaddr}$ with $\sigma' = \sigma_\baddr + \offpc \in \sigrets'$ which follows from $\sigrets',\sigcloss' \vdash_{\mathrm{comp-code}} \mscode$ and the fact that the call is there.

* $\isLinear{\sealed{\sigma',\retptrd(\aaddr_\stk,\eaddr_\stk)}}$ iff

Trivial, both are linear.

\[
\begin{array}{l}
\forall W'' \future \purePart{W_{R,\rretd}'}, W_o, n'' < n-1,\\
\quad\npair[n'']{(\vsc_S',\vsc_T')}
\in  H^\mathrm{code,\square}_\sigma \; \sigrets' \; \sigcloss' \; \mscode'
\; (\ta,\stkb) \; \sigma' \; \xi^{-1}(W_o) \ldotp \\
\qquad\npair[n'']{\retptrd(\aaddr_\stk,\eaddr_\stk),\vsc_S',((\rw,\linear),\aaddr_\stk,\eaddr_\stk,\aaddr_\stk-1),\vsc_T'} \in
\lrexj(W'\oplus W_o))
\end{array}
\]

Trivial as both configurations fails.

Case $\rretc$:
We have to show

\[
\npair[n-1]{\left(\array{l}\sealed{\sigma',\retptrc(\baddr,\eaddr,\aaddr +
\calllen)},\\\sealed{\sigma',((\rx,\normal),\baddr,\eaddr,\aaddr + \retoffset)}\endarray\right)} \in \lrv(W_{R,\rretc}')
\]

where $W_{R,\rretc}'$ has the ownership of $W$.
Just as in the previous case, we know that for some region $r$ there exists an $\mscode$ such that: $\pwheap(r) \nequal \codereg{\sigrets',\_,\mscode,\gc}$ where $\sigma' \in \sigrets'$ and $\dom(\mscode) \supseteq [\baddr,\eaddr]$ and $\aaddr + \offpc \in \dom(\mscode)$ and $\sigrets' \subseteq \gsigrets$.
It follows easily from the definition of $H_\sigma^\var{code}$ that

\begin{equation}
\label{eq:code-caps-in-h-sigma}
\npair[n'']{\left(\array{l}\retptrc(\baddr,\eaddr,\aaddr + \calllen),\\((\rx,\normal),\baddr,\eaddr,\aaddr + \retoffset)\endarray\right)} \in H^\mathrm{code,\square}_\sigma \; \sigrets' \; \sigcloss' \; \mscode \; (\ta,\stkb) \; \sigma' \; \xi^{-1}(W_{R,\rretc}')
\end{equation}

for $n'' < n-1$.
Both capabilities are non-linear, so

\[
\isLinear{\retptrc(\baddr,\eaddr,\aaddr + \calllen)}\text{ iff } \isLinear{((\rx,\normal),\baddr,\eaddr,\aaddr + \retoffset)}
\]

is indeed the case.

Finally we need to show:

\[
\begin{array}{l}
\forall W'' \future \purePart{W_{R,\rretc}'}, W_o, n'' < n-1,\\
\quad  \npair[n'']{(\vsc_S',\vsc'_T)} \in H^\mathrm{code,\square}_\sigma \; \sigrets' \; \sigcloss' \; \mscode \; (\ta,\stkb) \; \sigma' \; \xi^{-1}(W_o) \ldotp \\
\qquad \npair[n'']{\retptrc(\baddr,\eaddr,\aaddr + \calllen),\vsc_S',((\rx,\normal),\baddr,\eaddr,\aaddr + \retoffset),\vsc_T'} \in \lrexj(W''\oplus W_o))
\end{array}
\]

To this end let $W'' \future \purePart{W_{R,\rretc}'}$ and $W_o$ be given s.t. $W'' \oplus W_o$ is defined.
Further, let $\npair[n'']{(\vsc_S',\vsc'_T)} \in H^\mathrm{code,\square}_\sigma \; \sigrets' \; \sigcloss' \; \mscode \; (\ta,\stkb) \; \sigma' \; \xi^{-1}(W_o)$ be given and show

\[
\npair[n'']{\retptrc(\baddr,\eaddr,\aaddr + \calllen),\vsc_S',((\rx,\normal),\baddr,\eaddr,\aaddr + \retoffset),\vsc_T'} \in \lrexj(W''\oplus W_o))
\]

Now let $n''' \leq n''$ be given along with $\reg[3]_S$, $\reg[3]_T$, $\ms^{(3)}_S$, $\ms^{(3)}_T$,$\ms^{(3)}_\stk$, $\stk^{(3)}$, $W_R''$, and $W_M''$ such that

* $W'' \oplus W_o \oplus W_R'' \oplus W_M''$ is defined

* $\memSat[n''']{\ms^{(3)}_S,\ms^{(3)}_\stk, \stk^{(3)}, \ms^{(3)}_T}{W_M''}$

* $\npair[n''']{(\reg[3]_S,\reg[3]_T)} \in \lrr(W_R'')$

Based on $H_\sigma^\var{code}$, there are three possible values for $\vsc_S'$ and $\vsc_T'$.
In the first case, $\vsc_S'$ is a $\retptrc$ and $\vsc_T'$ is a capability with permission $\rx$.
In this case, $\var{xjumpResult}$ will produce failed configurations which are trivially in the observation relation.
In the next case, it is required that $\sigma' \in \sigcloss'$, but this
cannot be the case as $\sigma' \in \sigrets'$ and we have $\sigrets',\sigcloss' \vdash_{\mathrm{comp-code}} \mscode$, which implies that $\sigcloss' \mathrel{\#} \sigrets'$.

This leaves us with one final case, namely $\vsc_S'= \retptrd(\baddr_\stk',\eaddr_\stk')$ and $\vsc_T'=((\rw,\linear),\baddr_\stk',\eaddr_\stk',\baddr_\stk'-1)$.
Further we know

\[
\begin{array}{l}
\exists r \in \addressable{\linear,\pwpriv[W_o]} \ldotp \pwpriv[W_o](r).H \nequal (\stareg[(\ms_{\priv,S}^{(3)},\ms_{\priv,T}^{(3)}),\gc]{\spao,\square}, \aaddr'+\calllen) \tand \\
\quad \dom(\ms_{\priv,S}^{(3)}) = \dom(\ms_{\priv,T}^{(3)}) = [\baddr_\stk',\eaddr_\stk'] \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}
\]

Call this region $r'$.
By the above, the fact that the code capability pair is in $H_\sigma^\var{code}$ (<ref>) and Lemma <ref>, we get $\aaddr' = \aaddr$.
This means that $W_M''$ and $W_R''$ have this region.

We know that the two register-files are related which in particular means that the values in register $\rstk$ are related.
Now consider the following cases:

* $\reg_S^{(3)}(\rstk) \neq \stkptr{\_,\_,\_,\_}$

In this case due to $\reg[3]_S$ being related to $\reg[3]_T$, there are three cases we need to consider.
In all cases, the source configuration will fail because the value in the stack register is not a stack capability.
If we can argue that the target configuration will also fail, then the two are in the observation relation.
First, if $\reg[3]_T = \sealed{\sigma_\var{ret\_\stk},\vsc_T''}$, then the return code will fail when the base address (a sealed capability has no base address, so the instruction returns $-1$) is compared to $\stkb$.
Second, if $\reg[3]_T = \seal{\_,\_,\_}$, then the target execution fails when it attempts to splice this seal with $\vsc_T'$ (which we know is not a $\seal{}$ capability).
Finally, $\reg[3]_T = ((\perm_\var{ret\_\stk},\lin_\var{ret\_\stk}),\baddr_\var{ret\_\stk},\eaddr_\var{ret\_\stk},\_)$ and $\npair[n''']{[\baddr_\var{ret\_\stk},\eaddr_\var{ret\_\stk}]} \in \readCond{\lin_\var{ret\_\stk},W_{R,\rstk}''}$ is satisfied.
This means that it is satisfied by some heap region, but by the memory satisfaction assumption $\stkb$ must be in the free stack part of the world.
This means that the execution will fail that $\stkb$ check.

* $\reg_S^{(3)}(\rstk) = \stkptr{\perm_\var{ret\_\stk},\baddr_\var{ret\_\stk},\_,\_}$ and $\baddr_\var{ret\_\stk} \neq \stkb$

Here the source side will fail the xjmp as the base address is not $\stkb$.
Similarly on the target side, the return code will fail the $\stkb$ check.

* $\reg_S^{(3)}(\rstk) = \stkptr{\_,\baddr_\var{ret\_\stk},\eaddr_\var{ret\_\stk},\_}$ and $\baddr_\var{ret\_\stk} = \stkb$ and either $\eaddr_\var{ret\_\stk} +1 \neq \baddr_\stk' $ or $\perm_\var{ret\_\stk} \neq \rw$ or
$\baddr_\var{ret\_\stk} > \eaddr_\var{ret\_\stk}$.

In this case, the source configuration will fail as one of the conditions in $\var{xjumpResult}$ will not be met.
On the target side, the splice will fail as either the two capabilities being spliced don't line up, the permissions don't match, or the range of authority is empty, respectively.

* $\reg_S^{(3)}(\rstk) = \stkptr{\perm_\var{ret\_\stk},\baddr_\var{ret\_\stk},\eaddr_\var{ret\_\stk},\_}$ and $\baddr_\var{ret\_\stk} = \stkb$ and $\eaddr_\var{ret\_\stk} +1 = \baddr_\stk' $ and $\perm_\var{ret\_\stk} = \rw$ and $\baddr_\var{ret\_\stk} \leq \eaddr_\var{ret\_\stk}$.

We would like to show that $\ms_{\priv,S}^{(3)}$ is the top most stack frame and that $r'$ governs it.
By the memory satisfaction assumption and the presence of $r'$ in $W_M''$ we know that $\stk^{(3)}$ is non-empty.
By the memory satisfaction on the private stack, the following must be the case:

\[
\begin{array}{l}
\stk^{(3)} = (\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')\\
\end{array}
\]

Assume for contradiction $\ms_{\priv,S}^{(3)}$ is not the top frame. In that
case $\dom(\ms_0) \neq \emptyset$ and $\forall a \in \dom(\ms_0) \ldotp
\ldotp \stkb < a < b_\stk$ at the same time, we know

\[
\npair[n'']{(\stkptr{\rw,\stkb,\eaddr_\var{ret\_\stk},\_},((\rw,\linear),\stkb,\eaddr_\var{ret\_\stk},\_))}
\in \lrv(W_{R,\rstk}'')
\]

which means that the free stack part of the world contains a region that at least governs $[\stkb,\eaddr_\var{ret\_\stk}]$.
Combine this with $\eaddr_\var{ret\_\stk} +1 = \baddr_\stk' $, we can conclude that no such address can exist in $\ms_0$, so it must be empty, but this cannot be the case either.
Therefore, the top stack frame must contain $\ms_{\priv,S}^{(3)}$.

Further, due to the disjointedness required by memory satisfaction, it must be $r'$ that governs this stack frame.
This also means that we have $\opc_0 =  \aaddr+\calllen$.
With this, we have all the requirements for $\var{xjumpResult}$ satisfied on
both sides which allows us to pick the necessary configurations:

\begin{multline*}
\Phi^{(4)}_S=\xjumpResult{r_1}{r_2}{(\ms_S^{(3)},\reg[3]_S,(\ms_{\priv,S}^{(3)},\aaddr+\calllen)
:: \stk^{(3)}_\var{rest},\ms_\stk^{(3)})} =\\
\arraycolsep=0pt
\begin{array}[t]{l}
\updReg{\pcreg}{((\rx,\normal),\baddr,\eaddr,\aaddr+\calllen)} \\
\updReg{\rdata}{0} \\
\updReg{\rstk}{\stkptr{\rw,\stkb,e_\stk',\eaddr_\var{ret\_stk}+1}} \\
\updReg{\rtmp{1}}{0} \\
\updReg{\rtmp{2}}{0}
\end{array}
,\stk^{(3)}_\var{rest},\ms_{\priv,S}^{(3)} \uplus \ms_\stk^{(3)})
\end{multline*}

\begin{multline*}
\Phi^{(4)}_T=\xjumpResult{r_1}{r_2}{(\ms_T^{(3)},\reg[3]_T)} =\\
\arraycolsep=0pt
\begin{array}[t]{l}
\updReg{\pcreg}{((\rx,\normal),\baddr,\eaddr,\aaddr+\retoffset)} \\
\updReg{\rdata}{((\rw,\linear),\stkb,\eaddr_\var{ret\_stk})}
\end{array})
\end{multline*}

It now remains to show

\[
\npair[n''']{(\Phi^{(4)}_S,\Phi^{(4)}_T)} \in \lro
\]

Use Lemma <ref> by which it suffices to show the
following two things:

\[
\Phi^{(4)}_T \step[l] \Phi^{(5)}_T = (\ms_T^{(3)},\reg[3]_S
\arraycolsep=0pt
\begin{array}[t]{l}
\updReg{\pcreg}{((\rx,\normal),\baddr,\eaddr,\aaddr+\calllen)} \\
\updReg{\rdata}{0} \\
\updReg{\rstk}{((\rw,\linear),\stkb,e_\stk',\eaddr_\var{ret\_stk}+1)} \\
\updReg{\rtmp{1}}{0} \\
\updReg{\rtmp{2}}{0}
\end{array})
\]

for some number of steps $l$. This follows immediately from the
operational semantics.

\[
\npair[n''']{(\Phi^{(4)}_S,\Phi^{(5)}_T)} \in \lro
\]

For fresh $r_{b_\stk'}\dots r_{e_\stk'}$ and $W'''$ defined as

\[
W''' = W''[\priv.r' \mapsto \revoked,\free.r_{b_\stk'}\dots r_{e_\stk'}\mapsto \stdreg{\{b_\stk'\},\gc}{\spa} \dots \stdreg{\{e_\stk'\},\gc}{\spa}]
\]

and $W'''_R$ the same as $W'''$, but with the ownership of $W''_R$ as well as for the regions $r_{b_\stk'}\dots r_{e_\stk'}$,
and $W'''_M$ the same as $W'''$ but with the ownership of $W''_M$,
we show the following:

* $\npair[n''']{(\Phi_S^{(4)}.\reg,\Phi_T^{(5)}.\reg)} \in \lrr(W'''_R)$

* $\memSat[n''']{\Phi_S^{(4)}.\mem,\Phi_S^{(4)}.\stk,\Phi_S^{(4)}.\ms_\stk,\Phi_T^{(5)}.\mem}{W'''_M}$

* $W''' \oplus W'''_R \oplus W'''_M$ defined

Assuming the above, we use our assumption that Theorem <ref> holds for all $n' < n$ to get

\[
\npair[n''']{(((\rx,\normal),\baddr,\eaddr,\aaddr+\calllen),((\rx,\normal),\baddr,\eaddr,\aaddr+\calllen))} \in \lre(W''')
\]

Note that from assumption “$\Phi_S$ reasonable up to $n$ steps” and Lemma <ref> and $n''' \le n'' < n - 1$ we get “$\Phi_S$ reasonable up to $n'''+1$ steps” from which it follows that “$\Phi_S(\pcreg) + \calllen$ reasonable up to $n'''$ steps”.
Using this along with the register-file safety and memory satisfaction,
we get

\[
\npair[n''']{(\Phi^{(4)}_S,\Phi^{(5)}_T)} \in \lro
\]

as desired. We need to show the three things we skipped:

\[
\npair[n''']{(\Phi_S^{(4)}.\reg,\Phi_T^{(5)}.\reg)} \in \lrr(W'''_R)
\]

We will split the world like in $\npair[n''']{(\reg_S^{(3)},\reg_T^{(3)})} \in \lrr(W)$, but where $r_\stk$ also get the ownership of $r_{b_\stk'}\dots r_{e_\stk'}$.
We need to show the following

* Case $\rdata$, $\rtmp{1}$, $\rtmp{2}$:

* Case $r \not\in \{\rdata,\rtmp{1},\rtmp{2},\pcreg,\rstk\}$:

We have $\Phi^{(4)}_S.\reg(r) = \reg^{(3)}_S(r)$ and $\Phi^{(5)}_T.\reg(r) = \reg^{(3)}_T(r)$.
We already know:

\[\npair[n''']{(\reg^{(3)}_S(r),\reg^{(3)}_T(r))} \in \lrr(W''_{R,r}),\]

This is true for some $W_{R,r}''$ which does not have the ownership of the regions that are revoked in $W_R'''$, so that we can take the corresponding $W_{R,r}'''$ and have $W_{R,r}''' \future W_{R,r}''$.
From Lemma <ref>, we then get

\[
\npair[n''']{(\reg^{(3)}_S(r),\reg^{(3)}_T(r))} \in \lrr(W'''_{R,r})
\]

as desired.

* Case $\rstk$:

For this case, we need to show

\[
\npair[n''']{[\stkb,e_\stk']} \in \stackReadCond{W'''_{R,\rstk}}
\]

\[
\npair[n''']{[\stkb,e_\stk']} \in \stackWriteCond{W'''_{R,\rstk}}
\]

For $W'''_{R,\rstk}$ that owns the same as $W''_{R,\rstk}$ as well as $r_{b_\stk'},\dots,r_{e_\stk'}$.

For the first part, we use $\npair[n''']{(\reg_S^{(3)}(\rstk),\reg_T^{(3)}(\rstk))} \in \lrv(W_{R,\rstk}'')$ and the fact that the stack capability must have $\rw$ permission from which it follows that

\[
\npair[n''']{[\stkb,e_\var{ret\_stk}]} \in \stackReadCond{W''_{R,\rstk}}
\]

which gives us $S_\free \subseteq \addressable{\linear,\pwfree}$ and $R_\free : S_\free \fun \powerset{\nats}$ such that

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

* $\biguplus_{r \in S_\free} R(r) \subseteq [\stkb,e_\var{ret\_stk}]$

* $\forall r \in S_\free \ldotp \pwfree(r) \nsupeq \stdreg{R(r),\gc}{\spao}$

Now pick $S_\var{read} = S_\free \cup \{r_{b_\stk'},\dots,r_{e_\stk'}\}$ and

\[
R_\var{read}(r) =
\begin{cases}
R_\var{read}(r) & r \in S_\var{read} \\
\{a\} & r \in \{r_{b_\stk'},\dots,r_{e_\stk'}\} \wedge r = r_a
\end{cases}
\]

It is clearly the case that $\forall r \in S_\var{read} \ldotp |R_\var{read}(r)| = 1$ and $\biguplus_{r \in S_\var{read}} R(r) \subseteq [\stkb,e_\var{ret\_stk}]$.
For $\forall r \in S_\var{free} \ldotp \pwfree(r) \nsupeq \stdreg{R(r),\gc}{\spao}$ it follows from $\forall r \in S_\free \ldotp \pwfree(r) \nsupeq \stdreg{R(r),\gc}{\spao}$ and $\pwfree(r) = \stdreg{R(r),\gc}{\spao}$ for $r \in \{r_{b_\stk'},\dots,r_{e_\stk'}\}$.

The $\var{stackReadCondition}$ is shown in the same way, but we also use Lemma <ref> to argue that the new regions are address-stratified.

\begin{equation}
\memSat[n''']{\ms^{(3)}_S,\Phi_S^{(4)}.\stk,\ms_\stk^{(3)} \uplus \ms_{\priv,S}^{(3)} ,\ms^{(3)}_T}{W'''_M}\label{eq:ftlr:case:last-mem-sat}
\end{equation}

From the assumption $\memSat[n''']{\ms^{(3)}_S,\ms^{(3)}_\stk, \stk^{(3)}, \ms^{(3)}_T}{W_M''}$, we know

* $\stk = (\addr + \calllen,\ms_{\priv,S}^{(3)})::(\opc_1,\ms_1):: \dots :: (\opc_m,\ms_m)$

* $\ms^{(3)}_S \uplus \ms^{(3)}_\stk \uplus \ms_{\priv,S}^{(3)} \uplus \ms_1 \uplus \dots \uplus \ms_m  \text{ is defined}$

* $W''_M = W_{\var{stack}}'' \oplus W_{\var{free\_stack}}'' \oplus W_{\var{heap}}''$

* $\ms_\var{T,stack}, \ms_\var{T,free\_stack}, \ms_\var{T,heap}, \ms_{T,f}, \ms_{S,f}, \ms_S',\overline{\sigma}$ such that

* $\ms^{(3)}_S = \ms_{f,S} \uplus \ms_S'$

* $\ms^{(3)}_T = \ms_\var{T,stack} \uplus \ms_\var{T,free\_stack} \uplus \ms_\var{T,heap} \uplus \ms_{T,f}$

* $\memSatStack[n''']{\stk,\ms_\var{T,stack}}{W_{\var{stack}}''}$

* $\memSatFStack[n''']{\ms^{(3)}_\stk,\ms_\var{T,free\_stack}}{W_{\var{free\_stack}}''}$

* $\npair[n''']{(\overline{\sigma},\ms_S',\ms_\var{T,heap})} \in \lrheap(\pwheap)(W_{\var{heap}}'')$

We will pick the same things to show <ref> with a few changes.
We have to show

* $\Phi_S^{(4)}.\stk = (\opc_1,\ms_1):: \dots :: (\opc_m,\ms_m)$

By the memory satisfaction assumption and the change to the stack.

* $\ms^{(3)}_S \uplus \ms^{(3)}_\stk \uplus \ms_{\priv,S}^{(3)} \uplus \ms_1 \uplus \dots \uplus \ms_m \text{ is defined}$

By the memory satisfaction assumption.

* $W'''_M = W_{\var{stack}}''' \oplus W_{\var{free\_stack}}''' \oplus W_{\var{heap}}'''$

Define the new worlds to have the ownership of their $W_M''$ counterparts except $W_{\var{stack}}'''$ does not take ownership of the regions used for the safety of addresses $b_\stk',\dots,e_\stk'$.
This ownership goes to $W_{\var{free\_stack}}'''$ instead.

* We need to pick partitions of $\ms^{(3)}_T$ and a frame for $\ms^{(3)}_S$.
We pick the same as we get from the memory satisfaction assumption except we pick the free stack partition of the target memory to be $\ms_\var{T,free\_stack} \uplus \ms_{\priv,S}^{(3)}$ and the stack partition to be $\ms_\var{T,stack}\setminus \ms_\var{T,stack} | _{\dom(\ms_{\priv,S}^{(3)})}$

* $\ms^{(3)}_S = \ms_{f,S} \uplus \ms_S'$

By assumption.

* $\ms^{(3)}_T = \ms_\var{T,stack} \uplus \ms_\var{T,free\_stack} \uplus \ms_\var{T,heap} \uplus \ms_{T,f}$

By assumption and the fact that the only change is that we moved part of the stack to the free stack.

* $\memSatStack[n''']{(\opc_1,\ms_1):: \dots :: (\opc_m,\ms_m),\ms_\var{T,stack}\setminus \ms_\var{T,stack} | _{\dom(\ms_{\priv,S}^{(3)})}}{W_{\var{stack}}'''}$

Follows easily from the private stack satisfaction assumption.
The distribution functions from the assumption are simply limited to forget about the now revoked region and extend the world partition to be on $W_M'''$, but with the same ownership as in the one we had in the assumption.
All the new partitions are future worlds of the old ones as none of them owned the revoked region (it was owned by $W_R''$).

* $\memSatFStack[n''']{\ms^{(3)}_\stk \uplus \ms_{\priv,S}^{(3)},\ms_\var{T,free\_stack} \uplus \ms_\var{T,stack} | _{\dom(\ms_{\priv,S}^{(3)})}}{W_{\var{free\_stack}}'''}$

From the $\memSatFStack[n''']{\ms^{(3)}_\stk,\ms_\var{T,free\_stack}}{W_{\var{free\_stack}}''}$ assumption we get

* $R_\ms : \dom(\activeReg{W_{\var{free\_stack}}''}) \fun \MemSeg \times \MemSeg$ and

* $R_W : \dom(\activeReg{W_{\var{free\_stack}}''}.\free) \fun \Worlds$

for which

* $\ms^{(3)}_\stk = \biguplus_{r \in \dom(\activeReg{W_{\var{free\_stack}}''.\free})} \pi_1(R_\ms(r))$

* $\ms_\var{T,free\_stack} = \biguplus_{r \in \dom(\activeReg{W_{\var{free\_stack}}''.\free})} \pi_2(R_\ms(r))$

* $\stkb \in \dom(\ms^{(3)}_\stk)$ and $\stkb \in \dom(\ms_\var{T,free\_stack})$

* $W_{\var{free\_stack}}'' \bigoplus_{r \in \dom(\activeReg{W_{\var{free\_stack}}''.\free})} R_W(r)$

* $\forall r \in \dom(\activeReg{W_{\var{free\_stack}}''.\free}), n'''' < n'''\ldotp \npair[n'''']{R_\ms(r)} \in W_{\var{free\_stack}}''.\free(r).H \; \xi^{-1}(R_W(r))$

Now pick

\[
R_\ms'(r) =
\begin{cases}
(\ms_{\priv,S}^{(3)}|_{\{a'\}} , \ms_\var{T,stack}|_{\{a'\}}) & r_{a'} \in \{r_{b_\stk'}\dots r_{e_\stk'}\}\\
R_\ms(r) & \totherwise
\end{cases}
\]

\[
R_W'(r) =
\begin{cases}
W'''_{a'} & r_{a'} \in \{r_{b_\stk'}\dots r_{e_\stk'}\} \\
R_W(r)[\priv.r' \mapsto \revoked,\free.r_{b_\stk'}\dots r_{e_\stk'}\mapsto \stdreg{\{b_\stk'\},\gc}{\spa} \dots \stdreg{\{e_\stk'\},\gc}{\spa}]& \totherwise
\end{cases}
\]

for $W'''_{a'}$ constructed as follows: $W_{\var{stack}}''$ is the part of the world given to the stack judgement in the assumption.
This world is split into a number of parts to satisfy the memory interpretation of each frame.
Say $W_{top,\var{stack}}''$ is used for the top stack frame in the assumption.
The top stack frame is governed by a static region, so by definition it is split into parts that satisfy each of the addresses.
That is for $a' \in \{b_\stk' \dots e_\stk'\}$, $W_{a'}''$ is the part that makes the value in memory satisfy the value relation.
Now let $W_{a'}'''$ be $W'''$ but with the ownership of $W_{a'}''$

It is easy to see that the $R_\ms'$ constructs the two memories, and
from the assumption, we also get that the base stack address is in there.

It remains to show

\[
\forall r \in \dom(\activeReg{W_{\var{free\_stack}}'''.\free}),n'''' < n''' \ldotp \npair[n'''']{R_\ms(r)} \in W_{\var{free\_stack}}'''.\free(r).H \; \xi^{-1}(R_W(r))
\]

for $r \in \dom(\activeReg{W_{\var{free\_stack}}'''.\free}) \setminus \{r_{b_\stk'}\dots r_{e_\stk'}\}$, it follows from monotonicity of the $H$ (memory interpretation) function.
For $r_{a'} \in \{r_{b_\stk'}\dots r_{e_\stk'}\}$ and $n'''' < n'''$, we need to show

\[
\npair[n'''']{(\ms_{\priv,S}^{(3)}(a') , \ms_\var{T,stack}|(a'))} \in \stdreg{\{a\},\gc}{\spa}.H (\xi^{-1}R_W(r_{a'}))
\]

which amounts to showing $\dom(\ms_{\priv,S}^{(3)}|_{\{a'\}}) = \dom(\ms_\var{T,stack}|_{\{a'\}}) \{a'\}$, which is the case, and

\[
\npair[n'''']{(\ms_{\priv,S}^{(3)}(a') , \ms_\var{T,stack}|(a'))} \in \lrv (W_{a'}''')
\]

Which follows from Lemma <ref> and the fact that we have a memory satisfaction assumption in which $\ms_{\priv,S}^{(3)}$ is governed by a standard static region.

* $\npair[n''']{(\overline{\sigma},\ms_S',\ms_\var{T,heap})} \in \lrheap(\pwheap)(W_{\var{heap}}''')$

Follows by Lemma <ref> and the heap satisfaction assumption.

\[
W''' \oplus W'''_R \oplus W'''_M \text{ is defined.}
\]

This follows from the assumption $W'' \oplus W''_R \oplus W''_M$ and the fact that each of the new worlds is constructed from one of the past worlds and only one of them claims the ownership of the new regions.

This concludes case <ref>

Case <ref>:
we need to show:

\[
\memSat[n-1]{\Phi_S''.\mem,\Phi_S''.\stk,\Phi_S''.\ms_\stk,\Phi_T''.\mem}{W_M'}
\]

which amounts to

\[
\memSat[n-1]{\Phi_S.\mem,((\aaddr+\calllen),\ms_{\stk\_\priv,S}) :: \Phi_S,\Phi_S.\ms_\stk - \Phi_S.\ms_\stk|_{[\aaddr_\stk,\eaddr_\stk]},\Phi_T''.\mem}{W_M'}
\]

for $\ms_{\stk\_\priv,S} = \Phi_S.\ms_\stk |_{[\aaddr_\stk,\eaddr_\stk]}\update{\aaddr_\stk}{42}$.

In order to show this, we will first show the following:

* $\baddr_\stk = \stkb$

We know $\Phi_S$ is reasonable up to $n$ steps.
Further, from $\callCond{\Phi_S,r_1,r_2,\offpc,\offsigma,a}$ and $b \leq a$ and $a + \calllen -1 \leq e$ and $[b,e] \subseteq \ta$ we can conclude that $\Phi_S$ points to $\src{\scall{\offpc,\offsigma}{r_1}{r_2}}$ in $\ta$.
By the Guarantee stack base address before call we then know $\Phi_S(r_\stk) = \stkptr{\_,\stkb,\_,\_}$.

By assumption we have
$\memSat{\Phi_S.\mem,\Phi_S.\stk,\Phi_S.\ms_\stk,\Phi_T.\mem}{W_M}$ which
gives us $\ms_\var{T,stack}, \ms_\var{T,free\_stack},$ $\ms_\var{T,heap},
\ms_{T,f}, \ms_{S,f}, \ms_S', W_{M,\var{stack}}, W_{M,\var{free\_stack}},
W_{M,\var{heap}}$ such that:

* $\Phi_S.\stk = (\opc_0, \ms_0) \dots (\opc_m,\ms_m)$

* $\ms_0 \uplus \dots \uplus \ms_m \uplus \Phi_S.\mem \uplus \Phi_S.\ms_\stk$

* $W_M = W_{M,\var{stack}} \oplus W_{M,\var{free\_stack}} \oplus W_{M,\var{heap}}$

* $\Phi_S.\mem = \ms_{f,S} \uplus \ms_S'$

* $\Phi_T.\mem = \ms_\var{T,stack} \uplus \ms_\var{T,free\_stack} \uplus
\ms_\var{T,heap} \uplus \ms_{T,f}$

* $\memSatStack{\Phi_S.\stk,\ms_\var{T,stack}}{W_{M,\var{stack}}}$

* $\memSatFStack{\Phi_S.\ms_\stk,\ms_\var{T,free\_stack}}{W_{M,\var{free\_stack}}}$

* $\npair{(\overline{\sigma},\ms_S',\ms_\var{T,heap})} \in \lrheap(\pwheap[W_M])(W_{M,\var{heap}})$

In order to prove the memory satisfaction, we pick the same memories except for the following changes:

* The target free stack partition: $\ms_\var{T,free\_stack} \setminus \ms_\var{T,free\_stack}|_{[\aaddr_\stk,\eaddr_\stk]}$

* The target private stack partition: $\ms_\var{T,stack} \uplus \ms_\var{T,free\_stack}|_{[\aaddr_\stk,\eaddr_\stk]}\update{\aaddr_\stk}{42}$

and the worlds

* Free stack world: $W_{M,\var{free\_stack}}'$ is $W_{R,1}'$ with the ownership of $W_{M,\var{free\_stack}}$ except that it gives up any ownership that we used for the safety of the addresses $[\aaddr_\stk,\eaddr_\stk]$.

* Private stack world: $W_{M,\var{stack}}'$ is $W_{R,1}'$ with the ownership of $W_{M,\var{stack}}$ except that it takes the ownership that $W_{M,\var{free\_stack}}$ used for the safety of the addresses $[\aaddr_\stk,\eaddr_\stk]$.

* Heap world: $W_{M,\var{heap}}'$ is $W_{R,1}'$ with the ownership of $W_{M,\var{heap}}$ which gives us $W_{M,\var{heap}}' \future W_{M,\var{heap}}$.

We now need to show:

* $\stk = ((\aaddr+\calllen),\ms_{\stk\_\priv,S}) :: (\opc_0, \ms_0) \dots (\opc_m,\ms_m)$

* $\ms_{\stk\_\priv,S} \uplus \ms_0 \uplus \dots \uplus \ms_m \uplus \Phi_S.\mem \uplus \Phi_S.\ms_\stk - \Phi_S.\ms_\stk|_{[\aaddr_\stk,\eaddr_\stk]}$

Follows by assumption and the fact that we have shuffled around some memory[Thanks to the register-file safety assumption we know for sure that the memory we remove from the free stack is actually there.].

* $W_M' = W_{M,\var{stack}}' \oplus W_{M,\var{free\_stack}}' \oplus W_{M,\var{heap}}'$

This follows by assumption and the fact that all ownership we have added to a world has been removed from another.

* $\Phi_S.\mem = \ms_{f,S} \uplus \ms_S'$

By assumption.

* $\Phi_T.\mem = \ms_\var{T,stack} \uplus \ms_\var{T,free\_stack}|_{[\aaddr_\stk,\eaddr_\stk]}\update{\aaddr_\stk}{42} \uplus \ms_\var{T,free\_stack} \setminus \ms_\var{T,free\_stack}|_{[\aaddr_\stk,\eaddr_\stk]} \uplus \ms_\var{T,heap} \uplus \ms_{T,f}$

Follows by assumption and the fact that we have shuffled around some memory[Thanks to the register-file safety assumption we know for sure that the memory we remove from the free stack is actually there.].

* $\memSatStack[n-1]{((\aaddr+\calllen),\ms_{\stk\_\priv,S}) :: \Phi_S,\ms_\var{T,stack} \uplus \ms_\var{T,free\_stack}|_{[\aaddr_\stk,\eaddr_\stk]}\update{\aaddr_\stk}{42}}{W_{M,\var{stack}}'}$:

For most of the conditions, they follow from the previous stack satisfaction assumption.
The only challenge is to argue that the new stack frame satisfies the conditions.
First of all, we know $\ms_{\stk\_\priv,S}$ is non-empty as it at least contains address $\aaddr_\stk$.
Next, we need to argue that

\[
\begin{array}{l}
\forall i \in \{0,\dots,m\} \ldotp \\
\quad \forall a \in \dom(\ms_{\stk\_\priv,S}) \ldotp \forall a' \in \dom(\ms_j) \ldotp \stkb < a < a') \wedge\\
\end{array}
\]

The first bit, $\stkb < a$ for $a \in \dom(\ms_{\stk\_\priv,S})$ follows from the fact that $a_\stk$ is the smallest address of $a \in \dom(\ms_{\stk\_\priv,S})$ and by assumption $\stkb < a_\stk$.

Now assume for contradiction that there exists $a' \in \dom(\ms_j)$ for some $j$ such that $a' \le a$ for some $a \in \dom(\ms_{\stk\_\priv,S})$.
By assumption we have $\stkb < a'$ so $a' \in [\stkb+1,a] \subseteq [\stkb+1,a_\stk] \subseteq [\stkb,e_\stk]$ which means that $a'$ is an address governed by a stack pointer.
By the register-safety assumption this must mean that it is an address of the free part of the stack.
At the same time, it must be an address of the private stack because $\ms_j$ is part of the stack from the original configuration.
This contradicts the initial memory satisfaction assumption as the different parts must be disjointed.

From the stack satisfaction assumption, we get $R_\ms$ and $R_W$. Pick

\[
R_\ms'(r) =
\begin{cases}
(\ms_{\stk\_\priv,S}, (\aaddr+\calllen),\ms_\var{T,free\_stack}|_{[\aaddr_\stk,\eaddr_\stk]}\update{\aaddr_\stk}{42})& \text{for $r = r_\var{priv\_stk}$}\\
R_\ms(r) & \totherwise
\end{cases}
\]

and for $R_W'$ pick

\[
R_W'(r) =
\begin{cases}
\begin{aligned}
W_{M,\var{free\_stack},[\aaddr_\stk,\eaddr_\stk]}&[\free.R^{-1}([\aaddr_\stk,\eaddr_\stk]) \mapsto \revoked]\\
&[\priv.r_\var{priv\_stk} \mapsto (\stareg[(\ms_{\stk\_\priv,S},\Phi_T''.\mem|_{[\aaddr_\stk,\eaddr_\stk]}),\gc]{\spa,\square},\aaddr+\calllen)]
\end{aligned}

& \text{for $r = r_\var{priv\_stk}$} \\
\begin{aligned}
R_W(r)&[\free.R^{-1}([\aaddr_\stk,\eaddr_\stk]) \mapsto \revoked]\\
&[\priv.r_\var{priv\_stk} \mapsto (\stareg[(\ms_{\stk\_\priv,S},\Phi_T''.\mem|_{[\aaddr_\stk,\eaddr_\stk]}),\gc]{\spa,\square},\aaddr+\calllen)]
\end{aligned} &
\end{cases}
\]

where $W_{M,\var{free\_stack},[\aaddr_\stk,\eaddr_\stk]}$ is the world that the free stack assumption uses to satisfy that range of addresses.

Most of the condition trivially holds.

The only one that requires some argumentation is

\[
\npair[n']{(\ms_{\stk\_\priv,S},\ms_\var{T,free\_stack}|_{[\aaddr_\stk,\eaddr_\stk]}\update{\aaddr_\stk}{42})}
\in
\stareg[(\ms_{\stk\_\priv,S},\Phi_T''.\mem|_{[\aaddr_\stk,\eaddr_\stk]}),\gc]{\spa,\square}.H
\; \xi^{-1}(R_W'(r_\var{priv\_stk}))
\]

for all $n' < n-1$.
Where $R_W'(r_\var{priv\_stk})$ is the part of $W_{M,\var{stack}}'$ with the ownership used for addresses $[\aaddr_\stk, \eaddr_\stk]$ in the memory satisfaction assumption.

As we have the safe register-file assumption, we know that the stack capability is safe.
This means that addresses $[\aaddr_\stk,\eaddr_\stk]$ must be part of the free stack.
Further, $\Phi''_T.\mem = \Phi_T.\mem\update{\aaddr_\stk}{42}$ and $\ms_\var{T,free\_stack} \subseteq \Phi_T.\mem$ and $\dom(\ms_\var{T,free\_stack}) \supseteq [\aaddr_\stk,\eaddr_\stk]$ from which it follows that the memories are equal to the one of the static region.

It remains to show

\[
\forall \aaddr \in [\aaddr_\stk,\eaddr_\stk] \ldotp \npair[n']{(\ms_{\stk\_\priv,S}(\aaddr),\ms_\var{T,free\_stack}|_{[\aaddr_\stk,\eaddr_\stk]}\update{\aaddr_\stk}{42}(\aaddr))} \in \lrv(W_{R,\aaddr}')
\]

for $n' < n-1$.
For $\aaddr = \aaddr_\stk$ it is trivial as we have to show

\[
\npair[n-1]{(42,42)} \in \lrv(W_{R,\aaddr_\stk}')
\]

for $\aaddr \in [\aaddr_\stk+1,\eaddr_\stk]$ we need to show

\[
\npair[n']{(\ms_{\stk\_\priv,S}(\aaddr),\ms_\var{T,free\_stack}|_{[\aaddr_\stk,\eaddr_\stk]}\update{\aaddr_\stk}{42}(\aaddr))} \in \lrv(W_{R,\aaddr}')
\]

for $n' < n-1$.
If we can show

\[
\npair[n']{(\Phi_S.\ms_\stk(\aaddr),\ms_\var{T,free\_stack}(\aaddr))} \in \lrv(W_{R,\aaddr})
\]

for $n' < n-1$, then we are done by monotonicity of $\lrv$.

By assumption we know $\npair{(\Phi_S.\reg,\Phi_T.\reg)} \in \lrr(W_R)$ which entails $\npair{(\Phi_S.\reg(\rstk),\Phi_T.\reg(\rstk))} \in \lrr(W_{R,\rstk})$.
We know $\Phi_S.\reg(\rstk) = \stkptr{\rw,\stkb,\eaddr_\stk,\aaddr_\stk}$, so by the definition of $\lrv$ we get

\[
\npair{[\stkb,\eaddr_\stk]} \in \stackReadCond{W_{R,\rstk}}
\]

which in turn gives us $S_{\rstk} \subseteq \addressable{\linear,\pwfree}$ and
$R_{\rstk} : S_{\rstk} \fun \powerset{\nats}$ for which

* $\forall r \in S_{\rstk} \ldotp |R_{\rstk}(r)| = 1$

* $\uplus_{r \in S_{\rstk}} R_{\rstk}(r) \supseteq [\stkb,\eaddr_\stk]$

* $\forall r \in S_{\rstk} \ldotp W_{R,\rstk}(r).H \nsubeq \stdreg{R_{\rstk}(r),\gc}{\spao}$

Further, we know $\memSatFStack{\Phi_S.\ms_\stk,\ms_\var{T,free\_stack}}{W_{M,\var{free\_stack}}.\free}$ which means that we have $R_\ms : \dom(\activeReg{W_{M,\var{free\_stack}}}) \fun MemSeg \times \MemSeg$ and $R_W : \dom(W_{M,\var{free\_stack}}.\free) \fun \Worlds$.
$R_W$ distributes the ownership of $W_{M,\var{free\_stack}}$ and $R_\ms$ partitions the memories.

We know that all regions in $S_{\rstk}$ govern singleton memory segments, so $R_\ms$ must map to singleton memory segment pairs for $r \in S_{\rstk}$.
Further, by definition of the free stack satisfaction for $r \in S_{\rstk}$ we have

\[
\npair[n']{R_\ms(r)} \in W_{R,\rstk}(r).H \; \xi^{-1}(R_W(r))
\]

for $n' < n$
which entails

\[
\npair[n-1]{R_\ms(r)} \in \stdreg{R_{\rstk}(r),\gc}{\spao}.H \; \xi^{-1}(R_W(r))
\]

which entails

\[
\npair[n-1]{R_\ms(r)(a)} \in \lrv (R_W(r))
\]

for $a \in R_{\rstk(r)}$.

Now, using Lemma <ref>, this is exactly what we wanted to show because $R_W(r)$ is what we picked as $W_{R,\aaddr}$.

* $\memSatFStack[n-1]{\Phi_S.\ms_\stk - \Phi_S.\ms_\stk|_{[\aaddr_\stk,\eaddr_\stk]},\ms_\var{T,free\_stack} \setminus \ms_\var{T,free\_stack}|_{[\aaddr_\stk,\eaddr_\stk]}}{W_{M,\var{free\_stack}}'}$:

From the safety assumption on the stack capability, we can deduce a number of things:

* $[\aaddr_\stk,\eaddr_\stk]$ must have been part of the free stack

* for every address in $[\aaddr_\stk,\eaddr_\stk]$ there is a region for that singleton memory segment.

The first part means that we do indeed remove all of the memory we try to subtract.
The latter means that we can reuse the same split of the remaining memory and the world ownership as we get from assumption $\memSatFStack{\Phi_S.\ms_\stk,\ms_\var{T,free\_stack}}{W_{M,\var{free\_stack}}}$.
Using this, the result follows from monotonicity of the $H$ function.

* $\npair[n-1]{(\overline{\sigma},\ms_S',\ms_\var{T,heap})} \in \lrheap(\pwheap[W_M'])(W_{M,\var{heap}}')$:

Follows from Lemma <ref>, Lemma <ref>, the fact that the heap part of the world remains unchanged and $W_{M,\var{heap}}' \future W_{M,\var{heap}}$.

Case <ref>:

First show that

\[
\npair[n-1]{(((\rx,\normal),\baddr,\eaddr,\aaddr),((\rx,\normal),\baddr,\eaddr,\aaddr))} \in \lrvg{\trust}(\purePart{W_R})
\]

First observe that by Lemma <ref> $\purePart{W_R} = \purePart{W_\pcreg}$.
Further, by assumption, Lemma <ref>, Lemma <ref>, and Lemma <ref>, we have

\[
\npair[n-1]{[\baddr,\eaddr]} \in \xReadCond{}(\purePart{W_R})
\]

If $\trust = \trusted$, then by assumption we have $[\baddr,\eaddr] \subseteq \ta$ which means that all the conditions for are met for the capability pair to be in the trusted part of the value relation.

If $\trust = \untrusted$, then we need to show that the capability pair is in the untrusted part of the value relation which means that we need to show:

* $\npair[n-1]{[\baddr,\eaddr]} \in \readCond{}(\normal,\purePart{W_R})$

This follows by assumption, Lemma <ref>, Lemma <ref>, and Lemma <ref>.

* $\npair[n-1]{[\baddr,\eaddr]} \in \xReadCond{}(\purePart{W_R})$

We already showed this.

* $\npair[n-1]{[\baddr,\eaddr]} \in \execCond{}(\purePart{W_R})$

To this end let $W' \future \purePart{W_R}$ and $n' < n-1$ and $\aaddr' \in [\baddr',\eaddr']$ be given, and show

\[
\npair[n']{(((\rx,\normal),\baddr',\eaddr',\aaddr'),((\rx,\normal),\baddr',\eaddr',\aaddr'))} \in \lre(W')
\]

This follows immediately from the FTLR: we know that $[b,e] \mathrel{\#} \ta$ since $\trust = \untrusted$ and we know that $n' < n - 1 < n$.

Now show

\[
\npair[n-1]{(\Phi_S'.\reg,\Phi_T'.\reg)} \in \lrrg{\trust}(W_R)
\]

Note that we know that $\Phi_S.\reg(\pcreg)$ is not linear (which will sometimes help to eliminate some cases).

By assumption we have

\[
\npair[n]{(\Phi_S.\reg,\Phi_T.\reg)} \in \lrrg{\trust}(W_R)
\]

which gives us $R_R : (\RegName \setminus \{\pcreg\}) \fun \World$ such that $W_R = \bigoplus_{r\in \RegName \setminus \{\pcreg\}} R_R(r)$ and for all $r$ in $\RegName \setminus \{\pcreg\}$ we have $\npair[n]{(\Phi_S.\reg(r),\Phi_T.\reg(r))} \in \lrrg{\trust}(R_R(r))$.
To this end, we need to consider each of cases

TODO: check that all the below cases take care of the trusted case.

* Case <ref>:

Pick $R_R$ as the ownership distribution.
For $r \neq r_1$ it follows by assumption and Lemma <ref>.
For $r = r_1$ it also follows by assumption and Lemma <ref>, <ref>, and <ref>.

* Case <ref>:

Pick $R_R$ as the ownership distribution.
For $r \neq r_1$ it follows by assumption and Lemma <ref>.
For $r = r_1$ it also follows by assumption and Lemma <ref>, <ref>, and <ref>.

* Case <ref>:

Pick $R_R$ as the ownership distribution.
For $r \neq r_1$ it follows by assumption and Lemma <ref>.
For $r = r_1$ it also follows by assumption and Lemma <ref> and <ref>.

* Case <ref>:
Pick the ownership distribution based on the linearity of $w_2$: If $\isLinear{w_2}$, then pick

\[
R_R'(r) =
\begin{cases}
R_R(r_2) \oplus R_R(r_1) & r = r_1 \\
\purePart{W_R}         & r = r_2 \\
R_R(r)                 & \totherwise
\end{cases}
\]

if $\neg \isLinear{w_2}$, then pick

\[
R_R'(r) = R_R(r)
\]

In the case where $\isLinear{w_2}$, we may assume $r_2 \neq \pcreg$. We need to show (assuming $r_1 \neq \pcreg$)

\[
\npair[n-1]{(\Phi_S'(r_1),\Phi_T'(r_1))} \in \lrvg{\trust}(R_R(r_2) \oplus R_R(r_1))
\]

which is

\[
\npair[n-1]{(\Phi_S(r_2),\Phi_T(r_2))} \in \lrvg{\trust}(R_R(r_2) \oplus R_R(r_1))
\]

this follows by assumption and Lemma <ref> and <ref>.

We also need to show

\[
\npair[n-1]{(\Phi_S'(r_2),\Phi_T'(r_2))} \in \lrvg{\trust}(\purePart{W_R})
\]

which is trivial as $\Phi_S'(r_2) = \Phi_T'(r_2) = 0$.

Finally for $r \neq r_1,r_2,\pcreg$

\[
\npair[n-1]{(\Phi_S'(r),\Phi_T'(r))} \in \lrvg{\trust}(R_R(r))
\]

Follows by assumption and Lemma <ref>.

In the case where $\neg \isLinear{w_2}$

If $r_2 \neq \pcreg$, then for $r \neq r_1$

\[
\npair[n-1]{(\Phi_S'(r),\Phi_T'(r))} \in \lrvg{\trust}(R_R(r))
\]

Follows by assumption and Lemma <ref>.

For $r \neq r_1,r_2$

\[
\npair[n-1]{(\Phi_S'(r_1),\Phi_T'(r_1))} \in \lrvg{\trust}(R_R(r_1))
\]

amounts to

\[
\npair[n-1]{(\Phi_S(r_2),\Phi_T(r_2))} \in \lrvg{\trust}(R_R(r_1))
\]

By assumption and Lemma <ref> and <ref>.

If $r_2 = \pcreg$, show

\[
\npair[n-1]{(\Phi_S(\pcreg),\Phi_T(\pcreg))} \in \lrvg{\trust}(R_R(r_1))
\]

which follows from Lemma <ref> and <ref> and what we have proven about the pc.

* Case <ref>:

Pick $R_R' = R_R$.
For $r \neq r_1,r_2$, we have

\[
\npair[n-1]{(\Phi_S(r),\Phi_T(r))} \in \lrv(R_R(r))
\]

by assumption and Lemma <ref>.

For $r_1$ use Lemma <ref> and consider the following 2 cases:

* $\ta \# [\baddr,\eaddr]$: by assumption this entails $\trust = \untrusted$.

By assumption we have $\npair{(\Phi_S(r_2),\Phi_T(r_2))} \in \lrvg{\untrusted}(R_R(r_2))$ which gives us the following facts:

* $[\sigma_\baddr,\sigma_\eaddr] \# (\gsigrets \uplus \gsigcloss)$

* $\forall \sigma' \in [\sigma_\baddr,\sigma_\eaddr] \ldotp \exists r \in \pwheap[R_R(r_2)] \ldotp \pwheap[R_R(r_2)](r) = (\pure,\_,H_\sigma) \wedge H_\sigma \; \sigma' \nequal (\lrvg{\untrusted} \circ \xi)$

This means that for $\sigma$ there is a region $r$ for which $\pwheap[R_R(r_2)](r) = (\pure,\_,H_\sigma)$ and $H_\sigma \; \sigma' \nequal (\lrvg{\untrusted} \circ \xi)$.
Pick this as the region in the sealed case and $\sigrets' = \emptyset$,
$\sigcloss = [\sigma_\baddr,\sigma_\eaddr]$, and $\mscode = [\baddr,\eaddr] \mapsto 0$.
We now need to show the following:

* $H_\sigma \; \sigma \nequal H^\mathrm{code,\square}_\sigma \; \sigrets \; \sigcloss \; \mscode \; \gc \; \sigma$

To this end let $\hat{W}$ be given and show

\[
H_\sigma \; \sigma \; \hat{W} \nequal H^\mathrm{code,\square}_\sigma \; \sigrets \; \sigcloss \; \mscode \; \gc \; \sigma \; \hat{W}
\]

By transitivity of $n$-equality it suffices to show $H_\sigma \; \sigma' \; \hat{W} \nequal \lrvg{\untrusted} \circ \xi(\hat{W})$, which follows by assumption and $H^\mathrm{code,\square}_\sigma \; \sigrets \; \sigcloss \; \mscode \; \gc \; \sigma \; \hat{W} \nequal \lrvg{\untrusted} \circ \xi(\hat{W})$ which follows by definition of $H^\mathrm{code,\square}_\sigma$ and the fact that $\sigma \in \sigcloss$ and $\ta \# [\baddr,\eaddr]$.

* $\npair[n']{(\Phi_S(r_1),\Phi_T(r_1))} \in H_\sigma \; \sigma \; \xi^{-1}(R_R(r_1)) \text{ for all $n' < n$}$

which corresponds to showing $\npair[n']{(\Phi_S(r_1),\Phi_T(r_1))} \in \lrvg{\untrusted}(R_R(r_1))$ which is true by assumption and Lemma <ref>.

* $(\isLinear{\vsc_S} \Rightarrow \forall W' \future R_R(r_1), W_o, n' < n-1, \npair[n']{(\vsc_S',\vsc'_T)} \in H_\sigma \; \sigma \; \xi^{-1}(W_o) \ldotp \npair[n']{\vsc_S,\vsc_S',\vsc_T,\vsc_T'} \in \lrexj(W'\oplus W_o))$

Let $W' \future R_R(r_1)$, $W_o$, $n' < n$, $\npair[n']{(\vsc_S',\vsc'_T)} \in \codereg{\sigrets,\sigcloss,\mscode,\gc}.H_\sigma \; \sigma \; \xi^{-1}(W_o)$.
Further let $n'' \le n'$ be given and assume $\npair[n'']{(\reg_S,\reg_T)} \in \lrrg{\untrusted}(\{\rdata\})(W_R)$, $\memSat{\ms_S,\stk,\ms_\stk,\ms_T}{W_M}$.

Now consider the following cases:

* $\exec{\vsc_S'}$:

In this case, pick $\Phi_S' = \Phi_T' = \failed$ (as xjump fails).
It is trivial to show $\npair{\Phi_S',\Phi_T'} \in \lro$.

* $\nonExec{\vsc_S'}$:

In this case consider what $\Phi_S(r_1)$ is:

If $\Phi_S(r_1) = ((\perm,\lin),\baddr,\eaddr,\aaddr)$ and $\perm \in \{\rwx, \rx\}$:

If $\perm = \rwx$, then we have a contradiction with $\npair{(\Phi_S(r_1),\Phi_T(r_1))} \in \lrvg{\untrusted}(R_R(r_1))$.

If $\perm = \rx$, then by Lemma <ref> we have a contradiction with $\isLinear{\Phi_S(r_1)}$.

Otherwise (not $\Phi_S(r_1) = ((\perm,\lin),\baddr,\eaddr,\aaddr)$ and $\perm \in \{\rwx, \rx\}$):

In this case, pick $\Phi_S' = (\ms_S,\reg_S\update{\pcreg}{\Phi_S(r_1)}\update{\rdata}{\vsc_S'},\stk,\ms_\stk)$ and $\Phi_T' = (\ms_T,\reg_T\update{\pcreg}{\Phi_T(r_1)}\update{\rdata}{\vsc_T'})$.
In this case, the next step of execution fails which makes it trivial
to show $\npair{\Phi_S',\Phi_T'} \in \lro$.

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

Let $W' \future \purePart{R_R(r_1)}$, $W_o$, $n' < n$, $\npair[n']{(\vsc_S',\vsc'_T)} \in \codereg{\sigrets,\sigcloss,\mscode,\gc}.H_\sigma \; \sigma \; \xi^{-1}(W_o)$.
Further let $n'' \le n'$ be given and assume that

* $\npair[n'']{(\reg_S,\reg_T)} \in
\lrrg{\untrusted}(\{\rdata\})(W_R)$

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

Now consider the following cases:

* $\exec{\vsc_S'}$:

In this case, pick $\Phi_S' = \Phi_T' = \failed$ (as xjump fails).
It is trivial to show $\npair{\Phi_S',\Phi_T'} \in \lro$.

* $\nonExec{\vsc_S'}$:

In this case consider what $\Phi_S(r_1)$ is.

If $\Phi_S(r_1) = ((\perm',\lin'),\baddr',\eaddr',\aaddr')$ and $\perm' \in \{\rwx, \rx\}$:

If $\perm' = \rwx$, then we have a contradiction with $\npair{(\Phi_S(r_1),\Phi_T(r_1))} \in \lrvg{\untrusted}(R_R(r_1))$.

If $\perm' = \rx$, then the result follows from <ref>.

* $\ta \subseteq [\baddr,\eaddr]$: by assumption this entails $\trust = \trusted$.