$$ \tau/_{\_} = \tau \qquad \langle \tau_1, \dots, \tau_n \rangle / \langle p_1, \dots, p_n \rangle = \langle \tau_1 / p_1, \dots, \tau_n / p_n \rangle \\ K_1(\tau_1) + \dots + K_n(\tau_n) / K(p) = K_i(\tau_i / p) $$

<caption>Fig. 15. Type Specialisation</caption>

$$ \tau/_{\_} = \{\_ \mapsto \tau\} \qquad (\pi \text{ as } \hat{\tau})/p = \{p \mapsto (\pi \text{ as } \hat{\tau})\} \\ \langle\{\hat{\tau}_1, \dots, \hat{\tau}_n\}\rangle / p = \left\{ \begin{array}{l} p' \mapsto \langle\{\hat{\tau}'_1, \dots, \hat{\tau}'_n\}\rangle \\ \left| \begin{array}{l} (p_i \mapsto \hat{\tau}'_i) \in \hat{\tau}_i / p \\ p_1 \cap \dots \cap p_n = p' \end{array} \right. \end{array} \right\} \\ \text{split}(\hat{\pi}) \left\{ \begin{array}{l} c_1 \text{ from } P_1 \Rightarrow \hat{\tau}_1 \\ \vdots \text{ from } : \Rightarrow : \\ c_n \text{ from } P_n \Rightarrow \hat{\tau}_n \end{array} \right\} / p = \left\{ \begin{array}{l} \hat{\tau}_i / p \\ \left| \begin{array}{l} p' \in P_i \\ p \subset p' \end{array} \right. \end{array} \right\} $$

<caption>Fig. 16. Layout Specialisation.</caption>

$$ |t| = |\Delta(t)| \qquad |I_t| = \ell \qquad |\_\ell| = \ell \qquad |(c)_\ell| = \ell \qquad |\&\ell(\hat{\tau})| = \ell \qquad \left| \hat{\tau} \supseteq [o_i : \ell_i] : \hat{\tau}_i \right| = |\hat{\tau}| \\ \left| \langle\{\hat{\tau}_1, \dots, \hat{\tau}_n\}\rangle \right| = |\hat{\tau}_1| + \dots + |\hat{\tau}_n| \qquad \left| (\pi \text{ as } \hat{\tau}) \right| = |\hat{\tau}| \\ \left| \text{split}(\hat{\pi}) \left\{ c_i \text{ from } P_i \Rightarrow \hat{\tau}_i \mid 1 \le i \le n \right\} \right| = \max_{1 \le i \le n} |\hat{\tau}_i| $$

<caption>Fig. 17. Size of a memory layout in type environment $\Delta: \text{TyVars} \to \widetilde{\text{Types}}$.</caption>
$$ \tau/_{\_} = \tau \qquad \langle \tau_1, \dots, \tau_n \rangle / \langle p_1, \dots, p_n \rangle = \langle \tau_1 / p_1, \dots, \tau_n / p_n \rangle \\ K_1(\tau_1) + \dots + K_n(\tau_n) / K(p) = K_i(\tau_i / p) $$

<caption>Fig. 15. Type Specialisation</caption>

$$ \tau/_{\_} = \{\_ \mapsto \tau\} \qquad (\pi \text{ as } \hat{\tau})/p = \{p \mapsto (\pi \text{ as } \hat{\tau})\} \\ \langle\{\hat{\tau}_1, \dots, \hat{\tau}_n\}\rangle / p = \left\{ p' \mapsto \langle\{\hat{\tau}'_1, \dots, \hat{\tau}'_n\}\rangle \;\middle|\; \begin{array}{l} (p_i \mapsto \hat{\tau}'_i) \in \hat{\tau}_i / p \\ p_1 \cap \dots \cap p_n = p' \end{array} \right\} \\ \text{split}(\hat{\pi}) \left\{ \begin{array}{l} c_1 \text{ from } P_1 \Rightarrow \hat{\tau}_1 \\ \vdots \text{ from } : \Rightarrow : \\ c_n \text{ from } P_n \Rightarrow \hat{\tau}_n \end{array} \right\} / p = \left\{ \hat{\tau}_i / p \;\middle|\; \begin{array}{l} p' \in P_i \\ p \subset p' \end{array} \right\} $$

<caption>Fig. 16. Layout Specialisation.</caption>

$$ |t| = |\Delta(t)| \qquad |I_t| = \ell \qquad |\_\ell| = \ell \qquad |(c)_\ell| = \ell \qquad |\&\ell(\hat{\tau})| = \ell \qquad \left| \hat{\tau} \mathrel{\substack{\bowtie \\ 0 \le i < n}} [o_i : \ell_i] : \hat{\tau}_i \right| = |\hat{\tau}| \\ \left| \langle\{\hat{\tau}_1, \dots, \hat{\tau}_n\}\rangle \right| = |\hat{\tau}_1| + \dots + |\hat{\tau}_n| \qquad \left| (\pi \text{ as } \hat{\tau}) \right| = |\hat{\tau}| \\ \left| \text{split}(\hat{\pi}) \{c_i \text{ from } P_i \Rightarrow \hat{\tau}_i \mid 1 \le i \le n\} \right| = \max_{1 \le i \le n} |\hat{\tau}_i| $$

<caption>Fig. 17. Size of a memory layout in type environment $\Delta: \text{TyVars} \to \widetilde{\text{Types}}$.</caption>
B RECURSIVE CONSTRUCTORS

We now detail the extension of our algorithm to handle such cases by emitting recursive constructor code. The idea is to replace REBUILD and SEEK with WRAP(REBUILD) and WRAP(SEEK) respectively. The WRAP function, defined in Algorithm 8, hashes arguments to keep track of which calls have already been performed. Each argument hash is associated with a function symbol, and any subsequent call on the same arguments returns a call to this function.

1 **function** WRAP(FUN):
2     H := empty
3     **return** λ(⟨s<sub>in</sub>, τ<sub>in</sub>, τ̂<sub>in</sub>, p<sub>in</sub>⟩, ⟨d<sub>out</sub>, τ<sub>out</sub>, τ̂<sub>out</sub>⟩, π) . {
4         h ← (τ<sub>in</sub>, τ̂<sub>in</sub>, p<sub>in</sub>, τ<sub>out</sub>, τ̂<sub>out</sub>, π)
5     **if** h ∈ dom (H) **then**
6         f ← H(h)
7         **return** call f(s<sub>in</sub>, d<sub>out</sub>); success
8     **else**
9         f, s, d ← fresh symbols
10        H(h) := Declared(f)
11        args'<sub>in</sub> ← ⟨s, τ<sub>in</sub>, τ̂<sub>in</sub>, p<sub>in</sub>⟩
12        args'<sub>out</sub> ← ⟨d, τ<sub>out</sub>, τ̂<sub>out</sub>⟩
13        E<sub>body</sub> ← FUN(args'<sub>in</sub>, args'<sub>out</sub>, π)
14        H(h) := Defined(f, λ(s, d).E<sub>body</sub>)
15        **return** call f(s<sub>in</sub>, d<sub>out</sub>); success
16     **end**
17 }

<caption>**Algorithm 8:** Wrapper for emitting recursive code</caption>
B RECURSIVE CONSTRUCTORS

We now detail the extension of our algorithm to handle such cases by emitting recursive constructor code. The idea is to replace REBUILD and SEEK with WRAP(REBUILD) and WRAP(SEEK) respectively. The WRAP function, defined in Algorithm 8, hashes arguments to keep track of which calls have already been performed. Each argument hash is associated with a function symbol, and any subsequent call on the same arguments returns a call to this function.

1 **function** WRAP(FUN):
2     H := empty
3     **return** λ(⟨s<sub>in</sub>, τ<sub>in</sub>, τ̂<sub>in</sub>, p<sub>in</sub>⟩, ⟨d<sub>out</sub>, τ<sub>out</sub>, τ̂<sub>out</sub>⟩, π) . {
4         h ← (τ<sub>in</sub>, τ̂<sub>in</sub>, p<sub>in</sub>, τ<sub>out</sub>, τ̂<sub>out</sub>, π)
5     **if** h ∈ dom(H) **then**
6         f ← H(h)
7         **return** call f(s<sub>in</sub>, d<sub>out</sub>); success
8     **else**
9         f, s, d ← fresh symbols
10        H(h) := Declared(f)
11        args'<sub>in</sub> ← ⟨s, τ<sub>in</sub>, τ̂<sub>in</sub>, p<sub>in</sub>⟩
12        args'<sub>out</sub> ← ⟨d, τ<sub>out</sub>, τ̂<sub>out</sub>⟩
13        E<sub>body</sub> ← FUN(args'<sub>in</sub>, args'<sub>out</sub>, π)
14        H(h) := Defined(f, λ(s, d).E<sub>body</sub>)
15        **return** call f(s<sub>in</sub>, d<sub>out</sub>); success
16     **end**
17 }

<caption>**Algorithm 8:** Wrapper for emitting recursive code</caption>
# C ASSORTED DEFINITIONS

## C.1 Types and layouts

Agreement criteria define the relationship between a high-level type and its memory layout specification.

**Definition C.1 (Agreement between types and layouts).** Let $\tau$ a high-level type and $\hat{\tau}$ a memory layout. We say that $\hat{\tau}$ represents $\tau$, or agrees with $\tau$, and we write **agree**($\tau, \hat{\tau}$), if either $\tau$ and $\hat{\tau}$ are integer types of the same width (i.e., $\tau = \hat{\tau} = I_\ell$) or the following conditions hold:

**All fragments bind subterms to their valid representation.** (Fragment Coherence)

For all $\hat{\pi}$ such that **focus**($\hat{\pi}, \hat{\tau}$) = ($\pi$ as $\hat{\tau}$), $\tau' = \mathbf{focus}$($\pi, \tau$) is defined and $\hat{\tau}'$ agrees with $\tau'$.

**Split branches are valid representations of high-level subtypes.** (Branch Coherence)

For all $\hat{\pi}$ such that **focus**($\hat{\pi}, \hat{\tau}$) = split($\hat{\tau}$) { $c_i$ from $P_i \Rightarrow \hat{\tau}_i$}, for each $i$ and each $p \in P_i$ such that $p$ is a provenance of type $\tau$, $\hat{\tau}_i$ agrees with $\tau/p$.

**All data from the high-level type is represented within the memory layout.** (Coverage)

For every $\pi$ that leads to a single bit in $\tau$ (i.e., **focus**($\pi, \tau$) = i1), $\hat{\tau}$ covers $\pi$: every memory type $\hat{\tau}' \in \hat{\tau}/\pi$ contains a fragment for a source position $\pi_0$ prefix of $\pi$. More precisely, there exist source and memory paths $\pi_0, \hat{\pi}_0$ such that **focus**($\hat{\pi}_0, \hat{\tau}'$) = ($\pi_0$ as $\hat{\tau}'$) and either $\pi = \pi_0$. $\pi'$ or $\pi = \pi'$. [$o : \ell$], $\pi_0 = \pi'$. [$o_0 : \ell_0$] and $o_0 \le o \le o + \ell \le o_0 + \ell_0$.

**Memory layouts can tell incompatible provenances apart.** (Distinguishability)

For every pair of provenances $p_0, p_1$ of type $\tau$ such that $p_0$ and $p_1$ are incompatible (that is, there exists some position $\pi$ such that **focus**($\pi, p_0$) and **focus**($\pi, p_1$) have different head constructors), $\hat{\tau}$ distinguishes between $p_0$ and $p_1$. More precisely, for any $\hat{\tau}_0 \in \hat{\tau}/p_0$ and $\hat{\tau}_1 \in \hat{\tau}/p_1$, there exists a memory path $\hat{\pi}$ such that **focus**($\hat{\pi}, \hat{\tau}_0$) = ($c_0$)$_\ell$, **focus**($\hat{\pi}, \hat{\tau}_1$) = ($c_1$)$_\ell$ and $c_0 \ne c_1$.

$$ \frac{ (t \mapsto \hat{\tau}) \in \Delta \quad \Delta, \Gamma \vdash e : \tau \text{ as } \hat{\tau} }{ \Delta, \Gamma \vdash e : \tau \text{ as } t } \qquad \frac{ \mathbf{agree}(\tau, \hat{\tau}) \quad \Delta, \Gamma \vdash u : \tau }{ \Delta, \Gamma \vdash (u : \tau \text{ as } \hat{\tau}) : (\tau \text{ as } \hat{\tau}) } \\ \frac{ \Delta, \Gamma \vdash e : \tau \text{ as } \hat{\tau} \quad \Delta, \Gamma \cup \{ (x : \tau \text{ as } \hat{\tau}) \} \vdash e_0 : (\tau_0 \text{ as } \hat{\tau}_0) }{ \Delta, \Gamma \vdash \text{let } x = e \text{ in } e_0 : (\tau_0 \text{ as } \hat{\tau}_0) } $$

$$ \frac{ \Delta, \Gamma \cup \{x : (\tau \text{ as } \hat{\tau})\} \vdash e : (\tau' \text{ as } \hat{\tau}') \qquad \mathbf{agree}(\tau, \hat{\tau}) \qquad \Delta, \Gamma \cup \{f : (\tau \text{ as } \hat{\tau}) \to (\tau' \text{ as } \hat{\tau}')\} \vdash e_0 : (\tau_0 \text{ as } \hat{\tau}_0) }{ \Delta, \Gamma \vdash \mathbf{fun} \ f(x : \tau \text{ as } \hat{\tau}) = e \text{ in } e_0 : (\tau_0 \text{ as } \hat{\tau}_0) } $$

$$ \frac{ (x : (\tau \text{ as } \hat{\tau})) \in \Gamma \qquad (f : (\tau \text{ as } \hat{\tau}) \to (\tau' \text{ as } \hat{\tau}')) \in \Gamma \qquad (x : (\tau \text{ as } \hat{\tau})) \in \Gamma }{ \Delta, \Gamma \vdash x : (\tau \text{ as } \hat{\tau}) } \qquad \Delta, \Gamma \vdash f(x) : (\tau' \text{ as } \hat{\tau}') $$

$$ \frac{ x : \tau \text{ as } \hat{\tau} \in \Gamma \quad \Delta \vdash \text{pat}_i : \tau \quad \Delta, \Gamma \vdash e_i : (\tau' \text{ as } \hat{\tau}') \quad \forall p \in \mathbf{provs\_of}_\Delta(\tau), \exists i, \text{pat}_i \triangleright p }{ \Delta, \Gamma \vdash \text{match}(x)\{\text{pat}_1 \to e_1 \dots \text{pat}_n \to e_n\} : (\tau' \text{ as } \hat{\tau}') } $$

<caption>Fig. 18. Typing judgment for source expressions (grammar in Fig. 8): $\Delta, \Gamma \vdash e : \tau$ as $\hat{\tau}$ with $\Delta : \mathit{TyVars} \to \mathit{Types} \cup \overline{\mathit{Types}}$ and $\Gamma : \mathit{Vars} \to \mathit{Types} \times \overline{\mathit{Types}}$</caption>
# C ASSORTED DEFINITIONS

## C.1 Types and layouts

Agreement criteria define the relationship between a high-level type and its memory layout specification.

**Definition C.1 (Agreement between types and layouts).** Let $\tau$ a high-level type and $\hat{\tau}$ a memory layout. We say that $\hat{\tau}$ represents $\tau$, or agrees with $\tau$, and we write **agree**($\tau, \hat{\tau}$), if either $\tau$ and $\hat{\tau}$ are integer types of the same width (i.e., $\tau = \hat{\tau} = I_\ell$) or the following conditions hold:

**All fragments bind subterms to their valid representation.** (Fragment Coherence)

For all $\hat{\pi}$ such that **focus**($\hat{\pi}, \hat{\tau}$) = ($\pi$ as $\hat{\tau}$), $\tau' = \text{focus}$(π, τ) is defined and $\hat{\tau}'$ agrees with $\tau'$.

**Split branches are valid representations of high-level subtypes.** (Branch Coherence)

For all $\hat{\pi}$ such that **focus**($\hat{\pi}, \hat{\tau}$) = split($\hat{\tau}$) {cᵢ from Pᵢ ⇒ $\hat{\tau}_i$}, for each i and each p ∈ Pᵢ such that p is a provenance of type $\tau, \hat{\tau}_i$ agrees with $\tau/p$.

**All data from the high-level type is represented within the memory layout.** (Coverage)

For every $\pi$ that leads to a single bit in $\tau$ (i.e., **focus**($\pi, \tau$) = i1), $\hat{\tau}$ covers $\pi$: every memory type $\hat{\tau}' \in \hat{\tau}/\pi$ contains a fragment for a source position $\pi_0$ prefix of $\pi$. More precisely, there exist source and memory paths $\pi_0, \hat{\pi}_0$ such that **focus**($\hat{\pi}_0, \hat{\tau}'$) = ($\pi_0$ as $\hat{\tau}'$) and either $\pi = \pi_0$.π' or $\pi = \pi'$.[$o: \ell$], $\pi_0 = \pi'$.[$o_0: \ell_0$] and $o_0 \le o \le o + \ell \le o_0 + \ell_0$.

**Memory layouts can tell incompatible provenances apart.** (Distinguishability)

For every pair of provenances $p_0, p_1$ of type $\tau$ such that $p_0$ and $p_1$ are incompatible (that is, there exists some position $\pi$ such that **focus**($\pi, p_0$) and **focus**($\pi, p_1$) have different head constructors), $\hat{\tau}$ distinguishes between $p_0$ and $p_1$. More precisely, for any $\hat{\tau}_0 \in \hat{\tau}/p_0$ and $\hat{\tau}_1 \in \hat{\tau}/p_1$, there exists a memory path $\hat{\pi}$ such that **focus**($\hat{\pi}, \hat{\tau}_0$) = ($c_0$)$_\ell$, **focus**($\hat{\pi}, \hat{\tau}_1$) = ($c_1$)$_\ell$ and $c_0 \ne c_1$.

$$ \frac{(t \mapsto \hat{\tau}) \in \Delta \quad \Delta, \Gamma \vdash e : \tau \text{ as } \hat{\tau}}{\Delta, \Gamma \vdash e : \tau \text{ as } t} \qquad \frac{\text{agree}(\tau, \hat{\tau}) \quad \Delta, \Gamma \vdash u : \tau}{\Delta, \Gamma \vdash (u : \tau \text{ as } \hat{\tau}) : (\tau \text{ as } \hat{\tau})} \\ \frac{\Delta, \Gamma \vdash e : \tau \text{ as } \hat{\tau} \quad \Delta, \Gamma \cup \{(x : \tau \text{ as } \hat{\tau}) \} \vdash e_0 : (\tau_0 \text{ as } \hat{\tau}_0)}{\Delta, \Gamma \vdash \text{let } x = e \text{ in } e_0 : (\tau_0 \text{ as } \hat{\tau}_0)} $$

$$ \frac{\Delta, \Gamma \cup \{x : (\tau \text{ as } \hat{\tau})\} \vdash e : (\tau' \text{ as } \hat{\tau}')}{\Delta, \Gamma \cup \{f : (\tau \text{ as } \hat{\tau}) \to (\tau' \text{ as } \hat{\tau}' )\} \vdash e_0 : (\tau_0 \text{ as } \hat{\tau}_0)} \qquad \frac{\text{agree}(\tau, \hat{\tau})}{\Delta, \Gamma \vdash \text{fun } f(x : \tau \text{ as } \hat{\tau}) = e \text{ in } e_0 : (\tau_0 \text{ as } \hat{\tau}_0)} $$

$$ \frac{(x : (\tau \text{ as } \hat{\tau})) \in \Gamma}{\Delta, \Gamma \vdash x : (\tau \text{ as } \hat{\tau})} \qquad \frac{(f : (\tau \text{ as } \hat{\tau}) \to (\tau' \text{ as } \hat{\tau}')) \in \Gamma}{\Delta, \Gamma \vdash f(x) : (\tau' \text{ as } \hat{\tau}')} \qquad \frac{(x : (\tau \text{ as } \hat{\tau})) \in \Gamma}{\Delta, \Gamma \vdash (x : (\tau \text{ as } \hat{\tau})) \vdash (\tau' \text{ as } \hat{\tau}')} \\ \frac{x : \tau \text{ as } \hat{\tau} \in \Gamma}{\Delta, \Gamma \vdash \text{pat}_i : \tau} \qquad \Delta, \Gamma \vdash e_i : (\tau' \text{ as } \hat{\tau}') \qquad \forall p \in \textbf{provs\_of}_\Delta(\tau), \exists i, \text{pat}_i \triangleright p \\ \frac{\Delta, \Gamma \vdash \text{match}(x)\{\text{pat}_1 \to e_1 \dots \text{pat}_n \to e_n\} : (\tau' \text{ as } \hat{\tau}')}{} $$

<caption>Fig. 18. Typing judgment for source expressions (grammar in Fig. 8): $\Delta, \Gamma \vdash e : \tau$ as $\hat{\tau}$ with $\Delta : \textit{TyVars} \to \textit{Types} \cup \overline{\textit{Types}}$ and $\Gamma : \textit{Vars} \to \textit{Types} \times \overline{\textit{Types}}$</caption>
## C.2 Memory values and stores

The notion of *memory valuexpressions*, whose grammar is depicted in Fig. 19, abstracts from previously defined memory contents (Fig. 9), and is in our formalism used to capture values halfway during the interpretation process.

### Memory valuexpressions

$$ \begin{array}{l@{\hspace{2em}}r} \hat{u} \in \widehat{\text{ValuExprs}} & \text{(unevaluated representation)} \\ | \quad \underline{\ell} & \text{(opaque word)} \\ | \quad (c)_{\ell} & \text{(constant word)} \\ | \quad \&_{\ell}(\hat{u}) & \text{(addressless pointer)} \\ | \quad \&_{\ell}(a) & \text{(pointer value)} \\ | \quad \hat{u} \mathrel{\substack{\nsim \\ \text{0} \le i < n}} [o_i : \ell_i] : \hat{u}_i & \text{(composite word)} \\ | \quad \{\hat{u}_0, \dots, \hat{u}_{n-1}\} & \text{(struct)} \end{array} $$

### Memory expressions

$$ \begin{array}{l@{\hspace{2em}}r} \hat{e} \in \widehat{\text{Exprs}} & \text{(source expression)} \\ | \quad \hat{u} & \text{(memory valuexpression)} \\ | \quad \text{let } x : \tau \text{ as } \hat{\tau} = \hat{e} \text{ in } e & \text{(let-binding intermediate stage)} \end{array} $$

<caption>Fig. 19. Memory expressions and valuexpressions, representing intermediate stages between source expressions and memory values</caption>

The notion of shape of a memory value $\hat{v}$ according to a store $\zeta : \text{Addrs} \to \widehat{\text{Values}}$ (Fig. 20) is useful to characterise our equivalence notion (Fig. 21)

$$ \begin{array}{l@{\hspace{2em}}r} \mathbf{shape\_of}_{\zeta}\{ & \\ \underline{\ell} & \rightarrow \underline{\ell} \\ (c)_{\ell} & \rightarrow (c)_{\ell} \\ \&_{\ell}(a) & \rightarrow \&_{\ell}(\mathbf{shape\_of}_{\zeta}(\hat{v})) & \text{when } (a \mapsto \hat{v}) \in \zeta \\ \hat{v} \mathrel{\substack{\nsim \\ \text{0} \le i < n}} [o_i : \ell_i] : \hat{v}_i & \rightarrow \mathbf{shape\_of}_{\zeta}(\hat{v}) \mathrel{\substack{\nsim \\ \text{0} \le i < n}} [o_i : \ell_i] : \mathbf{shape\_of}_{\zeta}(\hat{v}_i) \\ \{\hat{v}_0, \dots, \hat{v}_{n-1}\} & \rightarrow \{\mathbf{shape\_of}_{\zeta}(\hat{v}_0), \dots, \mathbf{shape\_of}_{\zeta}(\hat{v}_{n-1})\} \end{array} $$

<caption>Fig. 20. Shape of a memory value $\hat{v}$ in a store $\zeta : \mathbf{shape\_of}_{\zeta}(\hat{v})$</caption>
## C.2 Memory values and stores

The notion of *memory valuexpressions*, whose grammar is depicted in Fig. 19, abstracts from previously defined memory contents (Fig. 9), and is in our formalism used to capture values halfway during the interpretation process.

### Memory valuexpressions

$$ \begin{array}{l@{\hspace{2em}}r} \hat{u} \in \widehat{ValuExprs} ::= & (u : \tau \text{ as } \hat{\tau}) & \text{(unevaluated representation)} \\ & | \underline{\epsilon} & \text{(opaque word)} \\ & | (c)_{\epsilon} & \text{(constant word)} \\ & | \&_{\epsilon} (\hat{u}) & \text{(addressless pointer)} \\ & | \&_{\epsilon} (a) & \text{(pointer value)} \\ & | \hat{u} \mathrel{\substack{\dagger \\ \text{0} \le i < n}} [o_i : \ell_i] : \hat{u}_i & \text{(composite word)} \\ & | \{\hat{u}_0, \dots, \hat{u}_{n-1}\} & \text{(struct)} \end{array} $$

### Memory expressions

$$ \begin{array}{l@{\hspace{2em}}r} \hat{e} \in \widehat{Exprs} ::= & e & \text{(source expression)} \\ & | \hat{u} & \text{(memory valuexpression)} \\ & | \text{let } x : \tau \text{ as } \hat{\tau} = \hat{e} \text{ in } e & \text{(let-binding intermediate stage)} \end{array} $$

<caption>Fig. 19. Memory expressions and valuexpressions, representing intermediate stages between source expressions and memory values</caption>

The notion of shape of a memory value $\hat{v}$ according to a store $\zeta : \text{Addrs} \to \widehat{\text{Values}}$ (Fig. 20) is useful to characterise our equivalence notion (Fig. 21)

$$ \begin{array}{l@{\hspace{2em}}r} \mathbf{shape\_of}_{\zeta} \{ & \underline{\epsilon} \rightarrow \underline{\epsilon} \\ & (c)_{\epsilon} \rightarrow (c)_{\epsilon} \\ & \&_{\epsilon} (a) \rightarrow \&_{\epsilon} (\mathbf{shape\_of}_{\zeta}(\hat{v})) \quad \text{when } (a \mapsto \hat{v}) \in \zeta \\ & \hat{v} \mathrel{\substack{\dagger \\ \text{0} \le i < n}} [o_i : \ell_i] : \hat{v}_i \rightarrow \mathbf{shape\_of}_{\zeta}(\hat{v}) \mathrel{\substack{\dagger \\ \text{0} \le i < n}} [o_i : \ell_i] : \mathbf{shape\_of}_{\zeta}(\hat{v}_i) \\ & \{\hat{v}_0, \dots, \hat{v}_{n-1}\} \rightarrow \{\mathbf{shape\_of}_{\zeta}(\hat{v}_0), \dots, \mathbf{shape\_of}_{\zeta}(\hat{v}_{n-1})\} \end{array} $$

<caption>Fig. 20. Shape of a memory value $\hat{v}$ in a store $\zeta : \mathbf{shape\_of}_{\zeta}(\hat{v})$</caption>
<figure><img src="image_9.png" /><figcaption>Fig. 21. Equivalence between two memory values considered in their stores: $\zeta, \tilde{v} \sim \zeta', \tilde{v}'$ (this is equivalent to $\mathbf{shape\_of}_{\zeta}(\tilde{v}) = \mathbf{shape\_of}_{\zeta'}(\tilde{v}')$)</figcaption></figure>

### C.3 Semantics/Evaluation

In order to state the correctness of our compilation algorithms, we need to define a “memory-aware” small steps semantics for our source language, in Fig. 22 (t LEVEL rules) and Fig. 23 (rules to construct and evaluate values).

The judgment is denoted $\Gamma, \hat{\sigma}, \zeta, \hat{e} \leftrightarrow \Gamma', \hat{\sigma}', \zeta', \hat{e}'$, where:

* $\Gamma: \text{Vars} \to \text{Types} \times \overline{\text{Typesin shape}}$ is a typing environment (assigning both a type and a layout);

* $\hat{\sigma}: \text{Vars} \to \text{Values}$ is a memory value environment (with the same domain as $\Gamma$);

* $\zeta$ is a memory store used to interpret the contents of $\hat{\sigma}$;

* $\hat{e}$ is a memory expression that represents the memory value currently being built. It includes both source expressions and memory values, along with intermediate stages containing both concrete memory structures and unevaluated triples ($u : \tau$ as $\hat{\tau}$).

Normal forms are states where $\hat{e}$ is a memory value. In order to reduce a source expression $e$ to a memory value $\hat{v}$ (along with its store $\zeta$), $\leftrightarrow$ must handle both high-level constructs (e.g., let, match) and memory-level construction of values (i.e., represent some valueexpression $u$ according to a given layout $\hat{\tau}$).

<figure><img src="image_10.png" /><figcaption>Fig. 22. Evaluation judgment for source expressions, high-level rules: $\Gamma, \hat{\sigma}, \zeta, \hat{e} \leftrightarrow \Gamma', \hat{\sigma}', \zeta', \hat{e}'$. $\Delta$ is a global type variable environment and $\Sigma$ a global function definition environment. Environments that are not relevant to a particular rule are displayed in gray. The MATCH rule relies on a memory-level pattern matching evaluation function eval_match which implements the approach presented in [Baudon et al. 2023] and returns the smallest $i$ such that the $i$-th pattern matching branch matches, or $\perp$ if no branch matches.</figcaption></figure>
<figure><img src="image_10.png" /><figcaption>Fig. 21. Equivalence between two memory values considered in their stores: $\zeta, \tilde{v} \sim \zeta', \tilde{v}'$ (this is equivalent to $\mathbf{shape\_of}_{\zeta}(\tilde{v}) = \mathbf{shape\_of}_{\zeta'}(\tilde{v}')$)</figcaption></figure>

### C.3 Semantics/Evaluation

In order to state the correctness of our compilation algorithms, we need to define a “memory-aware” small steps semantics for our source language, in Fig. 22 (tLEVEL rules) and Fig. 23 (rules to construct and evaluate values).

The judgment is denoted $\Gamma, \hat{\sigma}, \zeta, \hat{e} \mapsto \Gamma', \hat{\sigma}', \zeta', \hat{e}'$, where:

* $\Gamma: \mathbf{Vars} \to \mathbf{Types} \times \overline{\mathbf{Typesin shape}}$ is a typing environment (assigning both a type and a layout);

* $\hat{\sigma}: \mathbf{Vars} \to \mathbf{Values}$ is a memory value environment (with the same domain as $\Gamma$);

* $\zeta$ is a memory store used to interpret the contents of $\hat{\sigma}$;

* $\hat{e}$ is a memory expression that represents the memory value currently being built. It includes both source expressions and memory values, along with intermediate stages containing both concrete memory structures and unevaluated triples ($u : \tau$ as $\hat{\tau}$).

Normal forms are states where $\hat{e}$ is a memory value. In order to reduce a source expression $e$ to a memory value $\hat{v}$ (along with its store $\zeta$), $\mapsto$ must handle both high-level constructs (e.g., let, match) and memory-level construction of values (i.e., represent some valueexpression $u$ according to a given layout $\hat{\tau}$).

<figure><img src="image_11.png" /><figcaption>Fig. 22. Evaluation judgment for source expressions, high-level rules: $\Gamma, \hat{\sigma}, \zeta, \hat{e} \mapsto \Gamma', \hat{\sigma}', \zeta', \hat{e}'$. $\Delta$ is a global type variable environment and $\Sigma$ a global function definition environment. Environments that are not relevant to a particular rule are displayed in gray. The MATCH rule relies on a memory-level pattern matching evaluation function eval_match which implements the approach presented in [Baudon et al. 2023] and returns the smallest $i$ such that the $i$-th pattern matching branch matches, or $\perp$ if no branch matches.</figcaption></figure>
It remains to define the semantics of our target representation (see grammar in Fig. 11), in Fig. 24.
It remains to define the semantics of our target representation (see grammar in Fig. 11), in Fig. 24.
$\hat{C}[\Box] ::= \Box | \&_\ell (\hat{C}[\Box]) | \hat{C}[\Box] \bowtie b : \hat{u} | \hat{u} \bowtie b : \hat{C}[\Box] | \{\hat{u}, \dots, \hat{u}, \hat{C}[\Box], \hat{u}, \dots, \hat{u}\} | \text{let } x : \tau \text{ as } \hat{\tau} = \hat{C}[\Box] \text{ in e}$

**SUBSTEP**

$$ \frac{\Delta, \Sigma \vdash \Gamma, \hat{\sigma}, \zeta, \hat{u} \leftrightarrow \Gamma', \hat{\sigma}', \zeta', \hat{u}'}{\Delta, \Sigma \vdash \Gamma, \hat{\sigma}, \zeta, \hat{C}[\hat{u}] \leftrightarrow \Gamma', \hat{\sigma}', \zeta', \hat{C}[\hat{u}']}

**ALLOC**

$$ \frac{a \notin \text{dom}(\zeta)}{\Delta, \Sigma \vdash \Gamma, \hat{\sigma}, \zeta, \&_\ell (\hat{v}) \leftrightarrow \Gamma, \hat{\sigma}, \zeta \cup \{a \mapsto \hat{v}\}, \&_\ell (a)} $$

**TYPEVAR**

$$ \frac{(t \mapsto \hat{\tau}) \in \Delta \qquad \Delta, \Sigma \vdash \Gamma, \hat{\sigma}, \zeta, (u : \tau \text{ as } \hat{\tau}) \leftrightarrow \Gamma', \hat{\sigma}', \zeta', \hat{e}}{\Delta, \Sigma \vdash \Gamma, \hat{\sigma}, \zeta, (u : \tau \text{ as } t) \leftrightarrow \Gamma', \hat{\sigma}', \zeta', \hat{e}} $$

**SPLIT**

$$ \frac{\hat{\tau} = \text{split}(\dots) \qquad P = \{x \mapsto \widehat{\text{prov\_of}}_{\Delta,\zeta}(\hat{\tau}_x, \hat{\sigma}(x)) \mid (x : \tau_x \text{ as } \hat{\tau}_x) \in \Gamma\} \qquad \hat{\tau}/p = \{(p, \hat{\tau}')\}}{p = \text{prov\_of}_{\Delta}(\tau, u) [\dots \text{\textit{\textbf{focus}}}(\pi', P(x)) \mid \text{\textbf{focus}}(\pi, u) = x.\pi'] \qquad \Delta, \Sigma \vdash \Gamma, \hat{\sigma}, \zeta, (u : \tau \text{ as } \hat{\tau}) \leftrightarrow \Gamma, \hat{\sigma}, \zeta, (u : \tau/p \text{ as } \hat{\tau}')} $$

**FRAGMENT**

$$ \Delta \vdash \Gamma, \hat{\sigma}, \zeta, (u : \tau \text{ as } (\pi \text{ as } \hat{\tau})) \leftrightarrow \Gamma, \hat{\sigma}, \zeta, (\text{focus}(\pi, u) : \text{focus}(\pi, \tau) \text{ as } \hat{\tau}) $$

**ATOM**

$$ \Delta \vdash \Gamma, \hat{\sigma}, \zeta, (c : \tau \text{ as } I_\ell) \leftrightarrow \Gamma, \hat{\sigma}, \zeta, (c)_\ell $$

**CONSTANT**

$$ \Delta \vdash \Gamma, \hat{\sigma}, \zeta, (u : \tau \text{ as } (c)_\ell) \leftrightarrow \Gamma, \hat{\sigma}, \zeta, (c)_\ell $$

**WORD**

$$ \Delta \vdash \Gamma, \hat{\sigma}, \zeta, (u : \tau \text{ as } \underline{\phantom{x}}) \leftrightarrow \Gamma, \hat{\sigma}, \zeta, \underline{\phantom{x}} $$

**POINTER**

$$ \Delta \vdash \Gamma, \hat{\sigma}, \zeta, (u : \tau \text{ as } \&_\ell (\hat{\tau})) \leftrightarrow \Gamma, \hat{\sigma}, \zeta, \&_\ell ((u : \tau \text{ as } \hat{\tau})) $$

**BITRANGE**

$$ \Delta \vdash \Gamma, \hat{\sigma}, \zeta, (u : \tau \text{ as } \hat{\tau} \bowtie b : \hat{\tau}') \leftrightarrow \Gamma, \hat{\sigma}, \zeta, (u : \tau \text{ as } \hat{\tau}) \bowtie b : (u : \tau \text{ as } \hat{\tau}') $$

**STRUCT**

$$ \Delta \vdash \Gamma, \hat{\sigma}, \zeta, (u : \tau \text{ as } \{\hat{\tau}_1, \dots, \hat{\tau}_n\}) \leftrightarrow \Gamma, \hat{\sigma}, \zeta, \{\langle u : \tau \text{ as } \hat{\tau}_1 \rangle, \dots, \langle u : \tau \text{ as } \hat{\tau}_n \rangle\} $$

**EXTRACT-LIKE**

$$ \frac{(x : \tau_x \text{ as } \hat{\tau}_x) \in \Gamma \qquad \hat{\tau}_x = \hat{\tau}}{\Delta, \Sigma \vdash \Gamma, \hat{\sigma}, \zeta, (x.\epsilon : \tau \text{ as } \hat{\tau}) \leftrightarrow \Gamma, \hat{\sigma}, \zeta, \hat{\sigma}(x)} $$

**SEEK-LIKE**

$$ \frac{(x : \tau_x \text{ as } \hat{\tau}_x) \in \Gamma \qquad (x \mapsto \hat{v}) \in \hat{\sigma}}{p = \widehat{\text{prov\_of}}_{\Delta,\zeta}(\hat{\tau}_x, \hat{v}) \qquad \hat{\tau}_x / p = \{(p_b, \hat{t}_b)\} \qquad (\hat{\pi} \mapsto \pi_f \text{ as } \hat{\tau}_f) \in \text{Shatter}(\hat{t}_b) \qquad \pi = \pi_f.\pi' \qquad x_f \text{ fresh symbol} \qquad \tau_f = \text{focus}(\pi_f, \tau_x) \qquad \hat{v}_f = \widehat{\text{focus}}_{\zeta}(\hat{\pi}, \hat{v})} \\ \Delta, \Sigma \vdash \Gamma, \hat{\sigma}, \zeta, (x.\pi : \tau \text{ as } \hat{\tau}) \leftrightarrow \Gamma \cup \{x_f : (\tau_f \text{ as } \hat{\tau}_f)\}, \hat{\sigma} \cup \{x_f \mapsto \hat{v}_f\}, \zeta, (x_f.\pi' : \tau \text{ as } \hat{\tau}) $$

<caption>Fig. 23. Evaluation judgment for source expressions, memory value construction. $\widehat{\text{prov\_of}}(\hat{\tau}, \hat{v})$ explores all splits in $\hat{\tau}$ and gathers the branches whose discriminant values are coherent with $\hat{v}$.</caption>
$\hat{C}[\Box] ::= \Box | \&_\ell (\hat{C}[\Box]) | \hat{C}[\Box] \bowtie b : \hat{u} | \hat{u} \bowtie b : \hat{C}[\Box] | \{\hat{u}, \dots, \hat{u}, \hat{C}[\Box], \hat{u}, \dots, \hat{u}\} | \text{let } x : \tau \text{ as } \hat{\tau} = \hat{C}[\Box] \text{ in e}$

**SUBSTEP**
$\Delta, \Sigma \vdash \Gamma, \hat{\sigma}, \zeta, \hat{u} \leftrightarrow \Gamma', \hat{\sigma}', \zeta', \hat{u}'$
$\Delta, \Sigma \vdash \Gamma, \hat{\sigma}, \zeta, \hat{C}[\hat{u}] \leftrightarrow \Gamma', \hat{\sigma}', \zeta', \hat{C}[\hat{u}']$

**ALLOC**
$\underline{a \notin \text{dom } (\zeta)}$
$\Delta, \Sigma \vdash \Gamma, \hat{\sigma}, \zeta, \&_\ell (\hat{v}) \leftrightarrow \Gamma, \hat{\sigma}, \zeta \cup \{a \mapsto \hat{v}\}, \&_\ell (a)$

**TYPEVAR**
$(t \mapsto \hat{\tau}) \in \Delta \qquad \Delta, \Sigma \vdash \Gamma, \hat{\sigma}, \zeta, (u : \tau \text{ as } \hat{\tau}) \leftrightarrow \Gamma', \hat{\sigma}', \zeta', \hat{e}$
$\Delta, \Sigma \vdash \Gamma, \hat{\sigma}, \zeta, (u : \tau \text{ as } t) \leftrightarrow \Gamma', \hat{\sigma}', \zeta', \hat{e}$

**SPLIT**
$\hat{\tau} = \text{split}(\dots) \qquad P = \{x \mapsto \widehat{\text{prov\_of}}_{\Delta,\zeta}(\hat{\tau}_x, \hat{\sigma}(x)) \mid (x : \tau_x \text{ as } \hat{\tau}_x) \in \Gamma\}$
$p = \text{prov\_of}_{\Delta}(\tau, u) [\dots, \text{focus}(\pi', P(x)) | \text{focus}(\pi, u) = x.\pi'] \qquad \hat{\tau}/p = \{(p, \hat{\tau}')\}$
$\Delta, \Sigma \vdash \Gamma, \hat{\sigma}, \zeta, (u : \tau \text{ as } \hat{\tau}) \leftrightarrow \Gamma, \hat{\sigma}, \zeta, (u : \tau/p \text{ as } \hat{\tau}')$

**FRAGMENT**
$\Delta \vdash \Gamma, \hat{\sigma}, \zeta, (u : \tau \text{ as } (\pi \text{ as } \hat{\tau})) \leftrightarrow \Gamma, \hat{\sigma}, \zeta, (\text{focus}(\pi, u) : \text{focus}(\pi, \tau) \text{ as } \hat{\tau})$

**ATOM**
$\Delta \vdash \Gamma, \hat{\sigma}, \zeta, (c : \tau \text{ as } I_\ell) \leftrightarrow \Gamma, \hat{\sigma}, \zeta, (c)_\ell$

**CONSTANT**
$\Delta \vdash \Gamma, \hat{\sigma}, \zeta, (u : \tau \text{ as } (c)_\ell) \leftrightarrow \Gamma, \hat{\sigma}, \zeta, (c)_\ell$

**WORD**
$\Delta \vdash \Gamma, \hat{\sigma}, \zeta, (u : \tau \text{ as } \underline{\phantom{\tau}}) \leftrightarrow \Gamma, \hat{\sigma}, \zeta, \underline{\phantom{\tau}}$

**POINTER**
$\Delta \vdash \Gamma, \hat{\sigma}, \zeta, (u : \tau \text{ as } \&_\ell (\hat{\tau})) \leftrightarrow \Gamma, \hat{\sigma}, \zeta, \&_\ell ((u : \tau \text{ as } \hat{\tau}))$

**BITRANGE**
$\Delta \vdash \Gamma, \hat{\sigma}, \zeta, (u : \tau \text{ as } \hat{\tau} \bowtie b : \hat{\tau}') \leftrightarrow \Gamma, \hat{\sigma}, \zeta, (u : \tau \text{ as } \hat{\tau}) \bowtie b : (u : \tau \text{ as } \hat{\tau}')$

**STRUCT**
$\Delta \vdash \Gamma, \hat{\sigma}, \zeta, (u : \tau \text{ as } \{\hat{\tau}_1, \dots, \hat{\tau}_n\}) \leftrightarrow \Gamma, \hat{\sigma}, \zeta, \{(u : \tau \text{ as } \hat{\tau}_1), \dots, (u : \tau \text{ as } \hat{\tau}_n)\}$

**EXTRACT-LIKE**
$(x : \tau_x \text{ as } \hat{\tau}_x) \in \Gamma \qquad \hat{\tau}_x = \hat{\tau}$
$\Delta, \Sigma \vdash \Gamma, \hat{\sigma}, \zeta, (x.\epsilon : \tau \text{ as } \hat{\tau}) \leftrightarrow \Gamma, \hat{\sigma}, \zeta, \hat{\sigma}(x)$

**SEEK-LIKE**
$(x : \tau_x \text{ as } \hat{\tau}_x) \in \Gamma \qquad (x \mapsto \hat{v}) \in \hat{\sigma}$
$p = \widehat{\text{prov\_of}}_{\Delta,\zeta}(\hat{\tau}_x, \hat{v}) \qquad \hat{\tau}_x / p = \{(p_b, \hat{\tau}_b)\} \qquad (\hat{\pi} \mapsto \pi_f \text{ as } \hat{\tau}_f) \in \text{Shatter}(\hat{\tau}_b)$
$\pi = \pi_f.\pi' \qquad x_f \text{ fresh symbol} \qquad \tau_f = \text{focus}(\pi_f, \tau_x) \qquad \hat{v}_f = \widehat{\text{focus}}_{\zeta}(\hat{\pi}, \hat{v})$
$\Delta, \Sigma \vdash \Gamma, \hat{\sigma}, \zeta, (x.\pi : \tau \text{ as } \hat{\tau}) \leftrightarrow \Gamma \cup \{x_f : (\tau_f \text{ as } \hat{\tau}_f)\}, \hat{\sigma} \cup \{x_f \mapsto \hat{v}_f\}, \zeta, (x_f.\pi' : \tau \text{ as } \hat{\tau})$

<caption>Fig. 23. Evaluation judgment for source expressions, memory value construction. $\widehat{\text{prov\_of}}(\hat{\tau}, \hat{v})$ explores all splits in $\hat{\tau}$ and gathers the branches whose discriminant values are coherent with $\hat{v}$.</caption>
$$
\frac{y \notin \text{dom}(\rho_{\text{in}}) \cup \text{dom}(\rho_{\text{out}}) \quad x \in \text{dom}(\rho_{\text{in}}) \quad \rho_{\text{in}}(x) = a.\hat{\pi}_0}{\rho_{\text{in}}, \rho_{\text{out}}, \zeta, \text{let}_{\text{in}} y = x.\hat{\pi}; \mathcal{E} \rightsquigarrow_T \rho_{\text{in}} \cup \{y \mapsto a.\hat{\pi}_0.\hat{\pi}\}, \rho_{\text{out}}, \zeta, \mathcal{E}}
$$

$$
\frac{y \notin \text{dom}(\rho_{\text{in}}) \cup \text{dom}(\rho_{\text{out}}) \quad x \in \text{dom}(\rho_{\text{out}}) \quad \rho_{\text{out}}(x) = a.\hat{\pi}_0}{\rho_{\text{in}}, \rho_{\text{out}}, \zeta, \text{let}_{\text{out}} y = x.\hat{\pi}; \mathcal{E} \rightsquigarrow_T \rho_{\text{in}}, \rho_{\text{out}} \cup \{y \mapsto a.\hat{\pi}_0.\hat{\pi}\}, \zeta, \mathcal{E}}
$$

$x \notin \text{dom}(\rho_{\text{in}}) \cup \text{dom}(\rho_{\text{out}}) \quad \text{a fresh address}$

$$
\frac{\rho_{\text{in}}, \rho_{\text{out}}, \zeta, \text{let}_{\text{out}} x = \text{alloc}(\ell); \mathcal{E} \rightsquigarrow \rho_{\text{in}}, \rho_{\text{out}} \cup \{x \mapsto a.\epsilon\}, \zeta \cup \{a \mapsto \underline{\ell}\}, \mathcal{E}}{x \in \text{dom}(\rho_{\text{out}})}
$$
$$
\frac{\rho_{\text{in}}, \rho_{\text{out}}, \zeta, x := c; \mathcal{E} \rightsquigarrow \rho_{\text{in}}, \rho_{\text{out}}, \zeta[\rho_{\text{out}}(x) \leftarrow c], \mathcal{E}}{x \mapsto a_0.\hat{\pi}) \in \rho_{\text{out}} \quad |\widehat{\text{focus}}_{\zeta}(\hat{\pi}, \zeta(a_0))| = \ell_0 \quad \text{a fresh address}}
$$
$$
\frac{\rho_{\text{in}}, \rho_{\text{out}}, \zeta, x := \&\text{alloc}(\ell); \mathcal{E} \rightsquigarrow \rho_{\text{in}}, \rho_{\text{out}}, \zeta[a_0.\hat{\pi} \leftarrow \&\ell_0(a)] \cup \{a \mapsto \underline{\ell}\}, \mathcal{E}}{x \in \text{dom}(\rho_{\text{in}}) \quad y \in \text{dom}(\rho_{\text{out}}) \quad \rho_{\text{in}}(x) = a.\hat{\pi} \quad \widehat{\text{focus}}_{\zeta}(\hat{\pi}, \zeta(a)) = \hat{v}}
$$
$$
\frac{\rho_{\text{in}}, \rho_{\text{out}}, \zeta, y := x; \mathcal{E} \rightsquigarrow \rho_{\text{in}}, \rho_{\text{out}}, \zeta[\rho_{\text{out}}(y) \leftarrow \hat{v}], \mathcal{E}}{x \in \text{dom}(\rho_{\text{out}})}
$$

$$
\frac{x \in \text{dom}(\rho_{\text{out}})}{\rho_{\text{in}}, \rho_{\text{out}}, \zeta, \text{freeze}(x); \mathcal{E} \rightsquigarrow \rho_{\text{in}} \cup \{x \mapsto \rho_{\text{out}}(x)\}, \rho_{\text{out}} \setminus x, \zeta, \mathcal{E}}
$$

$$
\frac{x \in \text{dom}(\rho_{\text{out}}) \quad \rho_{\text{out}}(x) = a.\hat{\pi} \quad \widehat{\text{focus}}_{\zeta}(\hat{\pi}, a) = \underline{\ell} \quad \ell = \ell_0 + \ell_1}{\rho_{\text{in}}, \rho_{\text{out}}, \zeta, \text{cast } x \text{ to } \underline{\ell_0} \bowtie r : \underline{\ell_1}; \mathcal{E} \rightsquigarrow \rho_{\text{in}}, \rho_{\text{out}}, \zeta[a.\hat{\pi} \leftarrow \underline{\ell_0} \bowtie r : \underline{\ell_1}], \mathcal{E}}
$$

$$
\frac{x \in \text{dom}(\rho_{\text{out}}) \quad \rho_{\text{out}}(x) = a.\hat{\pi} \quad \widehat{\text{focus}}_{\zeta}(\hat{\pi}, a) = \underline{\ell} \quad \ell = \ell_1 + \dots + \ell_n}{\rho_{\text{in}}, \rho_{\text{out}}, \zeta, \text{cast } x \text{ to } \{\underline{-\ell_1}, \dots, \underline{-\ell_n}\}; \mathcal{E} \rightsquigarrow \rho_{\text{in}}, \rho_{\text{out}}, \zeta[a.\hat{\pi} \leftarrow \underline{-\ell_1}, \dots, \underline{-\ell_n}], \mathcal{E}}
$$

$$
\frac{(x \mapsto a.\hat{\pi}) \in \rho_{\text{in}} \quad (a \mapsto \hat{v}) \in \zeta \quad \widehat{\text{focus}}_{\zeta}(\hat{\pi}, \hat{v}) = (c_i)_{\ell}}{\rho_{\text{in}}, \rho_{\text{out}}, \zeta, \text{switch}(x) \{c_1 \to \mathcal{E}_1 \dots c_n \to \mathcal{E}_n\} \rightsquigarrow_T \rho_{\text{in}}, \rho_{\text{out}}, \zeta, \mathcal{E}_i}
$$

<caption>Fig. 24. Evaluation judgment for target expressions: $\rho_{\text{in}}$, $\rho_{\text{out}}$, $\zeta$, $\mathcal{E} \rightsquigarrow \rho'_{\text{in}}$, $\rho'_{\text{out}}$, $\zeta'$, $\mathcal{E}'$. Steps labelled with $T$ indicate transitions that do not correspond to any $\rightsquigarrow$-step in the simulation used to prove correctness.</caption>
$$ \frac{y \notin \text{dom}(\rho_{\text{in}}) \cup \text{dom}(\rho_{\text{out}}) \quad x \in \text{dom}(\rho_{\text{in}}) \quad \rho_{\text{in}}(x) = a.\hat{\pi}_0}{\rho_{\text{in}}, \rho_{\text{out}}, \zeta, \text{let}_{\text{in}} y = x.\hat{\pi}; \mathcal{E} \rightsquigarrow_T \rho_{\text{in}} \cup \{y \mapsto a.\hat{\pi}_0.\hat{\pi}\}, \rho_{\text{out}}, \zeta, \mathcal{E}} $$
$$ \frac{y \notin \text{dom}(\rho_{\text{in}}) \cup \text{dom}(\rho_{\text{out}}) \quad x \in \text{dom}(\rho_{\text{out}}) \quad \rho_{\text{out}}(x) = a.\hat{\pi}_0}{\rho_{\text{in}}, \rho_{\text{out}}, \zeta, \text{let}_{\text{out}} y = x.\hat{\pi}; \mathcal{E} \rightsquigarrow_T \rho_{\text{in}}, \rho_{\text{out}} \cup \{y \mapsto a.\hat{\pi}_0.\hat{\pi}\}, \zeta, \mathcal{E}} $$
$$ x \notin \text{dom}(\rho_{\text{in}}) \cup \text{dom}(\rho_{\text{out}}) \quad a \text{ fresh address} $$
$$ \rho_{\text{in}}, \rho_{\text{out}}, \zeta, \text{let}_{\text{out}} x = \text{alloc}(\ell); \mathcal{E} \rightsquigarrow \rho_{\text{in}}, \rho_{\text{out}} \cup \{x \mapsto a.\epsilon\}, \zeta \cup \{a \mapsto \underline{\ell}\}, \mathcal{E} $$

$$ \frac{x \in \text{dom}(\rho_{\text{out}})}{\rho_{\text{in}}, \rho_{\text{out}}, \zeta, x := c; \mathcal{E} \rightsquigarrow \rho_{\text{in}}, \rho_{\text{out}}, \zeta[\rho_{\text{out}}(x) \leftarrow c], \mathcal{E}} $$

$$ \frac{(x \mapsto a_0.\hat{\pi}) \in \text{dom}(\rho_{\text{out}}) \quad |\widehat{\text{focus}}_{\zeta}(\hat{\pi}, \zeta(a_0))| = \ell_0 \quad \text{a fresh address}}{\rho_{\text{in}}, \rho_{\text{out}}, \zeta, x := \&\text{alloc}(\ell); \mathcal{E} \rightsquigarrow \rho_{\text{in}}, \rho_{\text{out}}, \zeta[a_0.\hat{\pi} \leftarrow \&\ell_0(a)] \cup \{a \mapsto \underline{\ell}\}, \mathcal{E}} $$
$$ \frac{x \in \text{dom}(\rho_{\text{in}}) \quad y \in \text{dom}(\rho_{\text{out}}) \quad \rho_{\text{in}}(x) = a.\hat{\pi} \quad \widehat{\text{focus}}_{\zeta}(\hat{\pi}, \zeta(a)) = \hat{v}}{\rho_{\text{in}}, \rho_{\text{out}}, \zeta, y := x; \mathcal{E} \rightsquigarrow \rho_{\text{in}}, \rho_{\text{out}}, \zeta[\rho_{\text{out}}(y) \leftarrow \hat{v}], \mathcal{E}} $$

$$ \frac{x \in \text{dom}(\rho_{\text{out}})}{\rho_{\text{in}}, \rho_{\text{out}}, \zeta, \text{freeze}(x); \mathcal{E} \rightsquigarrow \rho_{\text{in}} \cup \{x \mapsto \rho_{\text{out}}(x)\}, \rho_{\text{out}} \setminus x, \zeta, \mathcal{E}} $$

$$ \frac{x \in \text{dom}(\rho_{\text{out}}) \quad \rho_{\text{out}}(x) = a.\hat{\pi} \quad \widehat{\text{focus}}_{\zeta}(\hat{\pi}, a) = \underline{\ell} \quad \ell = \ell_0 + \ell_1}{\rho_{\text{in}}, \rho_{\text{out}}, \zeta, \text{cast } x \text{ to } \underline{\ell_0} \bowtie r : \underline{\ell_1}; \mathcal{E} \rightsquigarrow \rho_{\text{in}}, \rho_{\text{out}}, \zeta[a.\hat{\pi} \leftarrow \underline{\ell_0} \bowtie r : \underline{\ell_1}], \mathcal{E}} $$
$$ \frac{x \in \text{dom}(\rho_{\text{out}}) \quad \rho_{\text{out}}(x) = a.\hat{\pi} \quad \widehat{\text{focus}}_{\zeta}(\hat{\pi}, a) = \underline{\ell} \quad \ell = \ell_1 + \cdots + \ell_n}{\rho_{\text{in}}, \rho_{\text{out}}, \zeta, \text{cast } x \text{ to } \{\underline{-\ell_1}, \ldots, \underline{-\ell_n}\}; \mathcal{E} \rightsquigarrow \rho_{\text{in}}, \rho_{\text{out}}, \zeta[a.\hat{\pi} \leftarrow \{\underline{-\ell_1}, \ldots, \underline{-\ell_n}\}], \mathcal{E}} $$
$$ \frac{(x \mapsto a.\hat{\pi}) \in \rho_{\text{in}} \quad (a \mapsto \hat{v}) \in \zeta \quad \widehat{\text{focus}}_{\zeta}(\hat{\pi}, \hat{v}) = (c_i)_{\ell}}{\rho_{\text{in}}, \rho_{\text{out}}, \zeta, \text{switch}(x) \{c_1 \to \mathcal{E}_1 \ldots c_n \to \mathcal{E}_n\} \rightsquigarrow_T \rho_{\text{in}}, \rho_{\text{out}}, \zeta, \mathcal{E}_i} $$

<caption>Fig. 24. Evaluation judgment for target expressions: $\rho_{\text{in}}, \rho_{\text{out}}, \zeta, \mathcal{E} \rightsquigarrow \rho'_{\text{in}}, \rho'_{\text{out}}, \zeta', \mathcal{E}'$. Steps labelled with $T$ indicate transitions that do not correspond to any $\rightsquigarrow$-step in the simulation used to prove correctness.</caption>