<figure><img src="image_1.png" /></figure>

HAL
open science

# Compiling Morphisms of Algebraic Data Types

Thaïs Baudon, Gabriel Radanne, Laure Gonnord

► To cite this version:

Thaïs Baudon, Gabriel Radanne, Laure Gonnord. Compiling Morphisms of Algebraic Data Types. 2024. hal-04601882

HAL Id: hal-04601882

https://hal.science/hal-04601882

Preprint submitted on 5 Jun 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.
# Compiling Morphisms of Algebraic Data Types

Thaïs Baudon, Gabriel Radanne, Laure Gonnord

► To cite this version:

Thaïs Baudon, Gabriel Radanne, Laure Gonnord. Compiling Morphisms of Algebraic Data Types. 2024. [https://hal.science/hal-04601882v1](https://hal.science/hal-04601882v1)

HAL Id: hal-04601882

[https://hal.science/hal-04601882v1](https://hal.science/hal-04601882v1)

Preprint submitted on 5 Jun 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Compiling Morphisms of Algebraic Data Types

THAÏS BAUDON, EnsL, UCBL, CNRS, Inria, LIP, France

GABRIEL RADANNE, Inria, EnsL, UCBL, CNRS, LIP, France

LAURE GONNORD, UGA, Grenoble INP, France, LCIS, France, and LIP, France

Now integrated in mainstream languages, Algebraic Data Types (ADTs) have established themselves as a nice way to reason about data structures and their manipulation using *pattern matching*. However, their use in low-level programming remains limited despite efforts, notably from the Rust community. Recently, Baudon et al. [2023] propose to let programmers express the precise memory layout of a given Algebraic Data Type, while still enjoying high-level programming constructs. Their compilation procedure covers efficient pattern matching, but leaves out constructors and struggles with arbitrarily mangled memory layouts.

So far, the literature on ADT compilation rarely mentions constructors, which are indeed a non-issue on simple memory layouts. However, when data pieces are broken and scattered in memory, this task becomes particularly challenging. Even simple accessors might require constructing new values. This is the case for many low-level representations such as network packets, instruction sets, database data-structures, or aggressively packed representations.

In this article, we go one step further, by enabling optimized compilation of any morphisms between ADTs for arbitrary mangled memory representations. We also provide full synthesis of bijections between memory representations of the same type. We subsume existing compilation algorithms, and extend them to emit CFG-style programs with explicit memory allocation and full support for recursive types.

Additional Key Words and Phrases: Algebraic Data Types, Pattern Matching, Compilation, Data Layouts

# 1 INTRODUCTION

Algebraic Data Types (ADTs) have proven themselves to be an essential tool for high-level programming: they allow to concisely model data thanks to sums, which indicate potential alternatives, and products, which group different pieces of data together. Thanks to their declarative nature, they let programmers manipulate data unbothered by the nitty-gritty details of its actual memory representation. That declarative nature allows compilers to verify and optimise code manipulating algebraic data, notably through pattern matching [Augustsson 1985; Maranget 2008, 2007]. This versatility and simplicity has allowed them to gain popularity, from their original grounds in functional programming languages [Burstall et al. 1980] like OCaml and Haskell, to mainstream languages such as Typescript, Python, and most recently Java.

Unfortunately, low-level programmers have so far not reaped the benefits of ADTs: they must often fall back to manual handling of memory layout to implement their data manipulation code, even in languages such as Rust which offer both ADTs and low-level programming. One main reason is that memory layouts for low-level data structures are indisputably *weird*: Red-Black Trees in the Linux kernel leverage low bits in aligned pointers to store information using the now classic bit-stealing technique [Torvalds 2023]; high-performance code regularly uses AoS (array of structs), SoA or AoSoA representations to mangle data collections for better locality [*AoS and SoA 2023*]; binary representations of data such as instruction sets and network packets regularly cut data into tiny pieces to minimise overall memory size. The general mold of Algebraic Data Types does not provide enough control over memory layout to model such mangled representations. As one might

Authors' addresses: Thaïs Baudon, EnsL, UCBL, CNRS, Inria, LIP, Lyon, France, thais.baudon@ens-lyon.fr; Gabriel Radanne, Inria, EnsL, UCBL, CNRS, LIP, Lyon, France, gabriel.radanne@inria.fr; Laure Gonnord, UGA, Grenoble INP, Grenoble, France and LCIS, Valence, France and LIP, Lyon, France, laure.gonnord@grenoble-inp.fr.

2024. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record was published in , https://doi.org/10.1145/nnnnnnn.nnnnnnn.
Compiling Morphisms of Algebraic Data Types

THAÏS BAUDON, EnsL, UCBL, CNRS, Inria, LIP, France

GABRIEL RADANNE, Inria, EnsL, UCBL, CNRS, LIP, France

LAURE GONNORD, UGA, Grenoble INP, France, LCIS, France, and LIP, France

Now integrated in mainstream languages, Algebraic Data Types (ADTs) have established themselves as a nice way to reason about data structures and their manipulation using *pattern matching*. However, their use in low-level programming remains limited despite efforts, notably from the Rust community. Recently, Baudon et al. [2023] propose to let programmers express the precise memory layout of a given Algebraic Data Type, while still enjoying high-level programming constructs. Their compilation procedure covers efficient pattern matching, but leaves out constructors and struggles with arbitrarily mangled memory layouts.

So far, the literature on ADT compilation rarely mentions constructors, which are indeed a non-issue on simple memory layouts. However, when data pieces are broken and scattered in memory, this task becomes particularly challenging. Even simple accessors might require constructing new values. This is the case for many low-level representations such as network packets, instruction sets, database data-structures, or aggressively packed representations.

In this article, we go one step further, by enabling optimized compilation of any morphisms between ADTs for arbitrary mangled memory representations. We also provide full synthesis of bijections between memory representations of the same type. We subsume existing compilation algorithms, and extend them to emit CFG-style programs with explicit memory allocation and full support for recursive types.

Additional Key Words and Phrases: Algebraic Data Types, Pattern Matching, Compilation, Data Layouts

# 1 INTRODUCTION

Algebraic Data Types (ADTs) have proven themselves to be an essential tool for high-level programming: they allow to concisely model data thanks to sums, which indicate potential alternatives, and products, which group different pieces of data together. Thanks to their declarative nature, they let programmers manipulate data unbothered by the nitty-gritty details of its actual memory representation. That declarative nature allows compilers to verify and optimise code manipulating algebraic data, notably through pattern matching [Augustsson 1985; Maranget 2008, 2007]. This versatility and simplicity has allowed them to gain popularity, from their original grounds in functional programming languages [Burstall et al. 1980] like OCaml and Haskell, to mainstream languages such as Typescript, Python, and most recently Java.

Unfortunately, low-level programmers have so far not reaped the benefits of ADTs: they must often fall back to manual handling of memory layout to implement their data manipulation code, even in languages such as Rust which offer both ADTs and low-level programming. One main reason is that memory layouts for low-level data structures are indisputably *weird*: Red-Black Trees in the Linux kernel leverage low bits in aligned pointers to store information using the now classic bit-stealing technique [Torvalds 2023]; high-performance code regularly uses AoS (array of structs), SoA or AoSoA representations to mangle data collections for better locality [*AoS and SoA 2023*]; binary representations of data such as instruction sets and network packets regularly cut data into tiny pieces to minimise overall memory size. The general mold of Algebraic Data Types does not provide enough control over memory layout to model such mangled representations. As one might

Authors' addresses: Thaïs Baudon, EnsL, UCBL, CNRS, Inria, LIP, Lyon, France, thais.baudon@ens-lyon.fr; Gabriel Radanne, Inria, EnsL, UCBL, CNRS, LIP, Lyon, France, gabriel.radanne@inria.fr; Laure Gonnord, UGA, Grenoble INP, Grenoble, France and LCIS, Valence, France and LIP, Lyon, France, laure.gonnord@grenoble-inp.fr.

2024. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record was published in , https://doi.org/10.1145/nnnnnnn.nnnnnnn.
imagine, the code required to manipulate such memory layouts is complex, error-prone, and hard to automatically verify and optimise.

Our goal is to provide high-level data-modelling constructs via ADTs, specify their precise
memory layout, and obtain low-level efficient code conforming to that layout. Some works have
attempted to bridge this gap. Dargent [Chen et al. 2023] lets programmers give high-level layout
descriptions and generates certified C accessors and constructors. It however doesn't provide full
language constructs like pattern matching. LoCal [Vollmer et al. 2019] and Gibbon [Koparkar et al.
2021] provide efficient compilation specialised for code operating on serialised and dense data
representations. More generally, many programming languages such as Rust or Haskell provide
both low-level vector types and high-level ADTs in separate manners, forcing programmers to
resort to low-level code when they want to fine-tune their memory layout.

More recently, RIBBIT [Baudon et al. 2023] proposes a dual-view compilation approach: a high-level type is paired with a low-level memory layout. A compilation algorithm then takes high-level pattern matching to low-level code respecting the layout. Their layout specification is expressive, allowing to specify many of the examples we just highlighted and scaling to fairly complex real-world examples. Their compilation algorithm, however, suffers from one crucial drawback: it can only access and deconstruct values. More formally, it only handles surjective morphisms between ADT representations. This not only limits the kind of code that can be compiled, but in fact also limits the choice of representations themselves, as highly mangled layouts might need data to be deconstructed, reshaped, and rebuilt differently. This is the case for aggressive struct packing, flattening or AoS/SoA transformations. To better understand this limitation, let us study two real-world examples of ADTs with complex layouts: the RISC-V instruction set with its binary representation, and optimised arithmetic expressions.

## 2 MOTIVATION

To demonstrate the complexity of real-world memory layouts for ADTs, we first consider a
restricted version of the 32-bit RISC-V assembly language consisting of four instructions (add,
addi, sw, and jal) in Fig. 1. We will use RIBBIT’s DSL to specify as a memory layout the encoding
described in the instruction set (ISA) documentation [Waterman et al. 2019]. A RISC-V machine
has 32 registers, x0 to x31 (encoded on 5 bits). As shown in Fig. 1a, RISC-V 32-bit instructions have
different formats based on their addressing mode. Further characteristics of our four instructions
are in Fig. 1b.

Already, we see complications: in general, instruction characteristics (type, instruction name, in-
volved registers, ...) are spread over opcode, funct3 and funct7, which are stored non-consecutively.
Moreover, the latter two are sometimes not present in the 32-bit instruction value. Immediates
are particularly mangled, and cannot be readily extracted from the binary representation. For our
particular (simple) subset: (i) the four instructions are distinguishable from their opcode *only*,
stored in bits 0 to 7 inclusive; (ii) the destination registers of add and addi are at the same location,
bits 7 to 11; (iii) the immediate value (imm) for the sw instruction is split and stored in two bit ranges:
bits 7 to 11 and 25 to 31; (iv) the 20-bit immediate value for the jal instruction can be recovered
from bits 12 to 31 but we need to *rebuild* this immediate from four separate bit ranges.

We demonstrate the modelling of RISC-V registers and instructions with ADTs in Figs. 1c and 1d,
using RIBBIT [Baudon et al. 2023] syntax. Additionally, all examples in this article can be tried
interactively at https://ribbit.gitlabpages.inria.fr/ribbit/. In addition to ADTs, RIBBIT lets us define
their *memory layouts*, which describe how concrete values are encoded in memory. Registers are
encoded on 5 bits, similar to a C enum (e.g., x2 is the 5-bit integer “3”). Instructions (Op32 type) are
encoded on 32 bits (w32). The split construct, on Line 3, allows to distinguish between the four
possible cases using the 7 lowest bits (opcode). We only showcase the Sw and Addi branches of this
imagine, the code required to manipulate such memory layouts is complex, error-prone, and hard to automatically verify and optimise.

Our goal is to provide high-level data-modelling constructs via ADTs, specify their precise
memory layout, and obtain low-level efficient code conforming to that layout. Some works have
attempted to bridge this gap. Dargent [Chen et al. 2023] lets programmers give high-level layout
descriptions and generates certified C accessors and constructors. It however doesn't provide full
language constructs like pattern matching. LoCal [Vollmer et al. 2019] and Gibbon [Koparkar et al.
2021] provide efficient compilation specialised for code operating on serialised and dense data
representations. More generally, many programming languages such as Rust or Haskell provide
both low-level vector types and high-level ADTs in separate manners, forcing programmers to
resort to low-level code when they want to fine-tune their memory layout.

More recently, RIBBIT [Baudon et al. 2023] proposes a dual-view compilation approach: a high-level type is paired with a low-level memory layout. A compilation algorithm then takes high-level pattern matching to low-level code respecting the layout. Their layout specification is expressive, allowing to specify many of the examples we just highlighted and scaling to fairly complex real-world examples. Their compilation algorithm, however, suffers from one crucial drawback: it can only access and deconstruct values. More formally, it only handles surjective morphisms between ADT representations. This not only limits the kind of code that can be compiled, but in fact also limits the choice of representations themselves, as highly mangled layouts might need data to be deconstructed, reshaped, and rebuilt differently. This is the case for aggressive struct packing, flattening or AoS/SoA transformations. To better understand this limitation, let us study two real-world examples of ADTs with complex layouts: the RISC-V instruction set with its binary representation, and optimised arithmetic expressions.

## 2 MOTIVATION

To demonstrate the complexity of real-world memory layouts for ADTs, we first consider a
restricted version of the 32-bit RISC-V assembly language consisting of four instructions (add,
addi, sw, and jal) in Fig. 1. We will use RIBBIT’s DSL to specify as a memory layout the encoding
described in the instruction set (ISA) documentation [Waterman et al. 2019]. A RISC-V machine
has 32 registers, x0 to x31 (encoded on 5 bits). As shown in Fig. 1a, RISC-V 32-bit instructions have
different formats based on their addressing mode. Further characteristics of our four instructions
are in Fig. 1b.

Already, we see complications: in general, instruction characteristics (type, instruction name, in-
volved registers, ...) are spread over opcode, funct3 and funct7, which are stored non-consecutively.
Moreover, the latter two are sometimes not present in the 32-bit instruction value. Immediates
are particularly mangled, and cannot be readily extracted from the binary representation. For our
particular (simple) subset: (i) the four instructions are distinguishable from their opcode *only*,
stored in bits 0 to 7 inclusive; (ii) the destination registers of add and addi are at the same location,
bits 7 to 11; (iii) the immediate value (imm) for the sw instruction is split and stored in two bit ranges:
bits 7 to 11 and 25 to 31; (iv) the 20-bit immediate value for the jal instruction can be recovered
from bits 12 to 31 but we need to rebuild this immediate from four separate bit ranges.

We demonstrate the modelling of RISC-V registers and instructions with ADTs in Figs. 1c and 1d,
using RIBBIT [Baudon et al. 2023] syntax. Additionally, all examples in this article can be tried
interactively at https://ribbit.gitlabpages.inria.fr/ribbit/. In addition to ADTs, RIBBIT lets us define
their *memory layouts*, which describe how concrete values are encoded in memory. Registers are
encoded on 5 bits, similar to a C enum (e.g., x2 is the 5-bit integer “3”). Instructions (Op32 type) are
encoded on 32 bits (w32). The split construct, on Line 3, allows to distinguish between the four
possible cases using the 7 lowest bits (opcode). We only showcase the Sw and Addi branches of this
split. For `sw`, Line 13 specifies that the opcode value is `0x23` (see Fig. 1b). The immediate operand is broken down into two parts, which are encoded on bits 7 to 11 inclusive (Line 15) and 25 to 31 (Line 20) within the 32-bit word representing the full instruction.

## 2.1 Compilation of Constructors and Destructors

Now that types and layouts have been defined, high-level data manipulation constructs can be compiled to code which directly manipulates memory. For instance, Fig. 2 represents `sw(x1, x2, imm)` in memory. From a high-level perspective, this is a simple constructor: a typical representation for such a value would simply allocate an adequate amount of memory, and encode `x1`, `x2` and `imm` as integers at their assigned positions. Our representation, however, is not so straightforward: since `imm` is stored non-consecutively, we need to break it down into two pieces. In essence, we need to synthesize code manifesting the *isomorphism* between the previous representation of `imm` (here, a straight `i12`) and the representation embedded in `Op32` (two pieces at positions `[25:7]` and `[7:5]`). Such implicit recombination of subterms is common in the context of embedded and low-level memory representations. A simple struct flattening and reordering already exhibits a similar behavior. Baudon et al. [2023]'s algorithm is unable to synthesize code that properly manipulates such representations.

<table><thead><tr><th>31</th><th>25</th><th>24</th><th></th><th>19</th><th>15</th><th>14</th><th>12</th><th>11</th><th>7</th><th>6</th><th>0</th></tr></thead><tbody><tr><td>funct7</td><td></td><td></td><td>rs2</td><td>rs1</td><td>funct3</td><td></td><td>rd</td><td></td><td>SELF</td><td></td><td></td></tr><tr><td></td><td></td><td></td><td>imm[0:12]</td><td>rs1</td><td>funct3</td><td></td><td>rd</td><td></td><td>SELF</td><td></td><td></td></tr><tr><td>imm[5:7]</td><td></td><td></td><td>rs2</td><td>rs1</td><td>funct3</td><td>imm[0:5]</td><td></td><td></td><td>SELF</td><td></td><td></td></tr><tr><td>imm[20]</td><td></td><td></td><td>imm[1:10]</td><td></td><td>imm[11]</td><td>imm[12:7]</td><td></td><td></td><td>SELF</td><td></td><td></td></tr></tbody></table>

(a) RISCV Core instruction format, excerpt. “rs1,2” are source registers, “rd” a destination register. “imm[n]” denotes the n-th bit of imm. “imm[0:7]” means “7 bits starting from 0 in the binary representation of imm”.

<table><thead><tr><th>Inst</th><th>Name</th><th>Type</th><th>Opcode</th><th>funct3</th><th>funct7</th><th>Description (in C)</th></tr></thead><tbody><tr><td>add</td><td>Add</td><td>R</td><td>0x33</td><td>0</td><td>0</td><td>rd = rs1 + rs2</td></tr><tr><td>addi</td><td>Add Immediate</td><td>I</td><td>0x13</td><td>0</td><td>-</td><td>rd = rs1 + imm</td></tr><tr><td>sw</td><td>Store Word</td><td>S</td><td>0x23</td><td>2</td><td>-</td><td>*(rs1+imm) = rs2</td></tr><tr><td>jal</td><td>Jump And Link</td><td>J</td><td>0x6F</td><td>-</td><td>-</td><td>rd = PC+4; PC += imm</td></tr></tbody></table>

(b) Instruction semantics and encoding, excerpt.

1 `enum Reg { X0, X1, X2, X3, ... } // cut`

2 `represented by C`

3

4 `enum Op32 {`

5 `Add(Reg, Reg, Reg), // add rd, rs1, rs2`

6 `Addi(Reg, Reg, i12), // addi rd, rs1, imm12`

7 `Jal(Reg, i20), // jal rd, imm20`

8 `Sw(Reg, Reg, i12), // sw rs1, rs2, imm12`

9 }

(c) Algebraic Data Types for 32-bit RISC-V instructions. iN types are predefined as “integers on N bits”.

<caption>Fig. 1. 32-bit RISC-V instructions – Specification, Type and Memory Layout in RIBBIT</caption>

1 `let out o = alloc(32);`

2 `o.[12:+3] := 2; o.[0:+5] := 0x23; // funct3, opcode`

3 `o.[15:+5] := 1; o.[20:+5] := 2; // rs1 = X1, rs2 = X2`

4 `o.[25:+7] := imm.[5:+7]; o.[7:+5] := imm.[0:+5]; // imm`

Fig. 2. Code building the memory representation of `Sw(X1, X2, imm)` in the root memory location `o`.

1 `Op32 represented as`

2 // discriminant in the 7 lowest bits

3 `split .[0:7] {`

4 `| 0x13 from Addi =>`

w32

5 `with .[0:7] = 0x13 // opcode`

6 `with .[7:5] : (_Addi.0 as Reg32)`

7 `with .[12:3] = 0`

8 `with .[15:5] : (_Addi.1 as Reg32)`

9 `with .[20:12] : (_Addi.2 as w12)`

10 `| 0x23 from Sw =>`

w32

13 `with .[0:7] = 0x23 // opcode`

14 // 5 lowest bits from imm

15 `with .[7:5]:(_Sw.2.[0:5] as w5)`

16 `with .[12:3] = 2 // funct3`

17 `with .[15:5]:(_Sw.0 as Reg32) // rs1`

18 `with .[20:5]:(_Sw.1 as Reg32) // rs2`

19 // 7 highest bits from imm

20 `with .[25:7]:(_Sw.2.[5:7] as w7)`

21 `| // other cases cut for readability`

(d) RIBBIT modelling for RISC-V instructions. wN types are predefined as “words on N bits”. Bit ranges consist of a left bound and a size.
split. For `sw`, Line 13 specifies that the opcode value is `0x23` (see Fig. 1b). The immediate operand is broken down into two parts, which are encoded on bits 7 to 11 inclusive (Line 15) and 25 to 31 (Line 20) within the 32-bit word representing the full instruction.

## 2.1 Compilation of Constructors and Destructors

Now that types and layouts have been defined, high-level data manipulation constructs can be compiled to code which directly manipulates memory. For instance, Fig. 2 represents `sw(x1, x2, imm)` in memory. From a high-level perspective, this is a simple constructor: a typical representation for such a value would simply allocate an adequate amount of memory, and encode `x1`, `x2` and `imm` as integers at their assigned positions. Our representation, however, is not so straightforward: since `imm` is stored non-consecutively, we need to break it down into two pieces. In essence, we need to synthesize code manifesting the *isomorphism* between the previous representation of `imm` (here, a straight `i12`) and the representation embedded in `Op32` (two pieces at positions `[25:7]` and `[7:5]`). Such implicit recombination of subterms is common in the context of embedded and low-level memory representations. A simple struct flattening and reordering already exhibits a similar behavior. Baudon et al. [2023]'s algorithm is unable to synthesize code that properly manipulates such representations.

<table><thead><tr><th>31</th><th>25</th><th>24</th><th></th><th>19</th><th>15</th><th>14</th><th>12</th><th>11</th><th>7</th><th>6</th><th>0</th></tr></thead><tbody><tr><td>funct7</td><td></td><td></td><td>rs2</td><td>rs1</td><td>funct3</td><td></td><td>rd</td><td></td><td>SELF</td><td></td><td></td></tr><tr><td></td><td></td><td></td><td>imm[0:12]</td><td>rs1</td><td>funct3</td><td></td><td>rd</td><td></td><td>SELF</td><td></td><td></td></tr><tr><td>imm[5:7]</td><td></td><td></td><td>rs2</td><td>rs1</td><td>funct3</td><td>imm[0:5]</td><td></td><td></td><td>SELF</td><td></td><td></td></tr><tr><td>imm[20]</td><td></td><td></td><td>imm[1:10]</td><td></td><td>imm[11]</td><td>imm[12:7]</td><td></td><td></td><td>SELF</td><td></td><td></td></tr></tbody></table>

(a) RISCV Core instruction format, excerpt. “rs1,2” are source registers, “rd” a destination register. “imm[n]” denotes the n-th bit of imm. “imm[0:7]” means “7 bits starting from 0 in the binary representation of imm”.

<table><thead><tr><th>Inst</th><th>Name</th><th>Type</th><th>Opcode</th><th>funct3</th><th>funct7</th><th>Description (in C)</th></tr></thead><tbody><tr><td>add</td><td>Add</td><td>R</td><td>0x33</td><td>0</td><td>0</td><td>rd = rs1 + rs2</td></tr><tr><td>addi</td><td>Add Immediate</td><td>I</td><td>0x13</td><td>0</td><td>—</td><td>rd = rs1 + imm</td></tr><tr><td>sw</td><td>Store Word</td><td>S</td><td>0x23</td><td>2</td><td>—</td><td>*(rs1+imm) = rs2</td></tr><tr><td>jal</td><td>Jump And Link</td><td>J</td><td>0x6F</td><td>—</td><td>—</td><td>rd = PC+4; PC += imm</td></tr></tbody></table>

(b) Instruction semantics and encoding, excerpt.

1. `enum Reg { X0, X1, X2, X3, ... } // cut`

2. `represented by C`

3.

4. `enum Op32 {`

5. `Add(Reg, Reg, Reg), // add rd, rs1, rs2`

6. `Addi(Reg, Reg, i12), // addi rd, rs1, imm12`

7. `Jal(Reg, i20), // jal rd, imm20`

8. `Sw(Reg, Reg, i12), // sw rs1, rs2, imm12`

9. `}`

(c) Algebraic Data Types for 32-bit RISC-V instructions. `iN` types are predefined as “integers on N bits”.

<caption>Fig. 1. 32-bit RISC-V instructions – Specification, Type and Memory Layout in RIBBIT</caption>

1. `let out o = alloc(32);`

2. `o.[12:+3] := 2; o.[0:+5] := 0x23; // funct3, opcode`

3. `o.[15:+5] := 1; o.[20:+5] := 2; // rs1 = X1, rs2 = X2`

4. `o.[25:+7] := imm.[5:+7]; o.[7:+5] := imm.[0:+5]; // imm`

Fig. 2. Code building the memory representation of `Sw(X1, X2, imm)` in the root memory location `o`.

1. `Op32 represented as`

2. `// discriminant in the 7 lowest bits`

3. `split .[0:7] {`

4. `| 0x13 from Addi =>`

w32

5. `with .[0:7] = 0x13 // opcode`

6. `with .[7:5] : (_Addi.0 as Reg32)`

7. `with .[12:3] = 0`

8. `with .[15:5] : (_Addi.1 as Reg32)`

9. `with .[20:12] : (_Addi.2 as w12)`

10. `| 0x23 from Sw =>`

w32

11. `with .[0:7] = 0x23 // opcode`

12. `// 5 lowest bits from imm`

13. `with .[7:5]:(_Sw.2.[0:5] as w5)`

14. `with .[12:3] = 2 // funct3`

15. `with .[15:5]:(_Sw.0 as Reg32) // rs1`

16. `with .[20:5]:(_Sw.1 as Reg32) // rs2`

17. `// 7 highest bits from imm`

18. `with .[25:7]:(_Sw.2.[5:7] as w7)`

19. `| // other cases cut for readability`

(d) RIBBIT modelling for RISC-V instructions. `wN` types are predefined as “words on N bits”. Bit ranges consist of a left bound and a size.
```R
fn is_compressible(o: Op32) -> Bool {
    match o {
        Jal(X1, off) => off < 4096,
        Add rd, rs1, rs2) => rd == rs1 && rs1 != X0 && !(rs2 == X0),
        Addi rd, rs, imm) => rd == rs && rs != X0 && imm < 64,
        Sw(rbase, roff, imm) =>
            X8 <= rbase && rbase <= X15 && X8 <= roff && roff <= X15 && (imm & 0b110000011111) == 0,
        _ => False,
    }
}
```

<figure><img src="image_2.png" /><figcaption>Fig. 4. Simplified CFG for `is_compressible`. From the input `i`, it identifies the head constructor using the 7 lowest bits, then extracts subterms such as destination and source registers for `Add` or the 12-bit `imm` for `Sw` (in bold), and finally stores the result in `dest`.</figcaption></figure>

Such transformations can also be necessary when *destroying* values. Figure 3 defines a function that determines whether a given 32-bit RISC-V instruction can be compressed into a 16-bit RISC-V instruction. However, again, we can not immediately bind the `imm` value during pattern matching compilation and need to first find all needed pieces and combine them together. Baudon et al. [2023]'s algorithm is thus not capable of compiling the `is_compressible` function.
```R
fn is_compressible(o : Op32) -> Bool {
    match o {
        Jal(X1, off) => off < 4096,
        Add rd, rs1, rs2) => rd == rs1 && rs1 != X0 && !(rs2 == X0),
        Addi rd, rs, imm) => rd == rs && rs != X0 && imm < 64,
        Sw(rbase, roff, imm) =>
            X8 <= rbase && rbase <= X15 && X8 <= roff && roff <= X15 && (imm & 0b110000011111) == 0,
        _ => False,
    }
}
```

<figure><img src="image_2.png" /><figcaption>Fig. 4. Simplified CFG for `is_compressible`. From the input `i`, it identifies the head constructor using the 7 lowest bits, then extracts subterms such as destination and source registers for `Add` or the 12-bit `imm` for `Sw` (in bold), and finally stores the result in `dest`.</figcaption></figure>

Such transformations can also be necessary when *destroying* values. Figure 3 defines a function that determines whether a given 32-bit RISC-V instruction can be compressed into a 16-bit RISC-V instruction. However, again, we can not immediately bind the `imm` value during pattern matching compilation and need to first find all needed pieces and combine them together. Baudon et al. [2023]'s algorithm is thus not capable of compiling the `is_compressible` function.
Our compilation procedure is capable of emitting the control flow graph depicted in Fig. 4, which:

* *inspects* the internal representation of an input Op32 value to determine its head constructor (Add, Addi, Jal or Sw), as well as the nested register constructor in Jal;

* *extracts* from this representation all subterms that are bound to variables in the matched pattern. For instance, in the *Sw case*, the parts of the immediate *imm* are combined in *simm* in order to reconstruct a value that can be used in a mask;

* *allocates* and *initialises* memory to represent the appropriate values. For instance, the *imm* value just mentioned is first allocated as *dimm*, filled, then promoted to a read-only value *simm* before being used.

## 2.2 Morphisms of Complex Types

So far, the type we had to transform, while having an intricate representation, consisted of fairly flat simple structures. Let us consider a richer example with simple arithmetic expressions over 32-bit integers in Fig. 5. As described by the Exp type, arithmetic expressions consist of variable names, 32-bit integer constants and operations with two arguments (for simplicity of the example, we only have additions here). The host machine is assumed to be a 64-bit architecture. A naive representation of operands would be a pointer to a 3-word structure: a first word containing a few bits (here, 32) representing the operation, followed by two 64-bit-wide aligned pointers to the operands. However, in cases such as Plus(I(12), ...), this is wasteful: we could simply pack the 32-bit operator with the left operand, and use one less memory word. In Fig. 5a, we define this optimized memory layout. Integer terms are boxed in a 64-bit word when isolated (Line 13), but are inlined (i.e., directly represented as their 32-bit integer value) when they appear as operands of a binary operation (Line 7). While this reduces memory usage and indirections compared to a naive, uniform layout, it pervasively impacts the compilation process. Since the very structure (pointers/indirections, struct shapes) of the memory representation of an integer expression is different depending on the context in which it appears, some seemingly simple constructs – pattern matching and value construction – require complex code to properly manipulate data. For all these reasons, such optimizations are only done by programmers when absolutely necessary (such as extremely performance-sensitive code). As we will see, our approach can compile any valid program given its layout, making such complex layouts completely transparent to client code.

The eval function (shown in Fig. 5b), reduces all arithmetic expressions which can be evaluated. When both operands are integers, it reduces further (Fig. 5b, Line 5). Figure 5c shows the normalized program representation we use in the rest of this article, and Fig. 5d shows the final compiled version, using a Control Flow Graph in Destination Passing Style [Shaikhha et al. 2017] with segregated input (read-only) and output (write only) memory locations, allowing fine control over memory. Corresponding elements of eval in normalized source and final target code are colorized accordingly.

Consider the code which extracts both operands of Plus (on **Line 4**). Given the complex layout, this is not a straight-up pointer dereference: we need to reconstruct values fitting the type Exp to be used as arguments to eval. In other words, we need to synthesize an isomorphism between the stored memory representation of .Plus.0 (inlined integer), and the desired representation (a standard Exp). The generated code creates two destinations to receive contents, inspects the inner tag (tag2, stored in x. * .0) to determine which operands, if any, are inlined integers, and emits code to fill them. As we can see, a simple accessor at the source level might require us to emit code that rebuild values.

Consider now the final code returning Plus(e1', e2') (on **Line 13**). It is naturally split in three cases: depending on whether e1' and e2' are I constructors or not. Note that this decision is factorized
Our compilation procedure is capable of emitting the control flow graph depicted in Fig. 4, which:

* *inspects* the internal representation of an input Op32 value to determine its head constructor (Add, Addi, Jal or Sw), as well as the nested register constructor in Jal;

* *extracts* from this representation all subterms that are bound to variables in the matched pattern. For instance, in the *Sw case*, the parts of the immediate *imm* are combined in *simm* in order to reconstruct a value that can be used in a mask;

* *allocates* and *initialises* memory to represent the appropriate values. For instance, the *imm* value just mentioned is first allocated as *dimm*, filled, then promoted to a read-only value *simm* before being used.

## 2.2 Morphisms of Complex Types

So far, the type we had to transform, while having an intricate representation, consisted of fairly flat simple structures. Let us consider a richer example with simple arithmetic expressions over 32-bit integers in Fig. 5. As described by the Exp type, arithmetic expressions consist of variable names, 32-bit integer constants and operations with two arguments (for simplicity of the example, we only have additions here). The host machine is assumed to be a 64-bit architecture. A naive representation of operands would be a pointer to a 3-word structure: a first word containing a few bits (here, 32) representing the operation, followed by two 64-bit-wide aligned pointers to the operands. However, in cases such as Plus(I(12), ...), this is wasteful: we could simply pack the 32-bit operator with the left operand, and use one less memory word. In Fig. 5a, we define this optimized memory layout. Integer terms are boxed in a 64-bit word when isolated (Line 13), but are inlined (i.e., directly represented as their 32-bit integer value) when they appear as operands of a binary operation (Line 7). While this reduces memory usage and indirections compared to a naive, uniform layout, it pervasively impacts the compilation process. Since the very structure (pointers/indirections, struct shapes) of the memory representation of an integer expression is different depending on the context in which it appears, some seemingly simple constructs – pattern matching and value construction – require complex code to properly manipulate data. For all these reasons, such optimizations are only done by programmers when absolutely necessary (such as extremely performance-sensitive code). As we will see, our approach can compile any valid program given its layout, making such complex layouts completely transparent to client code.

The eval function (shown in Fig. 5b), reduces all arithmetic expressions which can be evaluated. When both operands are integers, it reduces further (Fig. 5b, Line 5). Figure 5c shows the normalized program representation we use in the rest of this article, and Fig. 5d shows the final compiled version, using a Control Flow Graph in Destination Passing Style [Shaikhha et al. 2017] with segregated input (read-only) and output (write only) memory locations, allowing fine control over memory. Corresponding elements of eval in normalized source and final target code are colorized accordingly.

Consider the code which extracts both operands of Plus (on **Line 4**). Given the complex layout, this is not a straight-up pointer dereference: we need to reconstruct values fitting the type Exp to be used as arguments to eval. In other words, we need to synthesize an isomorphism between the stored memory representation of .Plus.0 (inlined integer), and the desired representation (a standard Exp). The generated code creates two destinations to receive contents, inspects the inner tag (tag2, stored in x. * .0) to determine which operands, if any, are inlined integers, and emits code to fill them. As we can see, a simple accessor at the source level might require us to emit code that rebuild values.

Consider now the final code returning Plus(e1', e2') (on **Line 13**). It is naturally split in three cases: depending on whether e1' and e2' are I constructors or not. Note that this decision is factorized
```R
1 enum Exp { V(String), I(i32), Plus(Exp, Exp) }
2 represented as
3 split .[0, 2] {
4 | 0 from Plus =>
5 &<64, 2>(split .0 {
6 | 0 from Plus(I,_) =>
7 | {{w32, _Plus.0.I as w32, _Plus.1 as Exp}}
8 | 1 from Plus(Plus|V, I) =>
9 | {{w32, _Plus.1.I as w32, _Plus.0 as Exp}}
10 | 2 from (Plus(Plus|V,Plus|V)) =>
11 | {{w32, _32, _Plus.0 as Exp, _Plus.1 as Exp}}
12 })
13 | 1 from I => w64 with .[32, 32] : (_I as w32)
14 | 2 from V => &<64, 2>(._V as String)
15 }
```

(a) Arithmetic expressions and their representation. On the first layer, this representation stores the tag distinguishing between V, I, and Plus in the two lowest bits. This potentially leverages bit-stealing in pointer alignment bits. For Plus constructors, we use a struct whose first field indicates the more precise layout. Some space could be used to store an operator (MULT, ...) as well. Fields are arranged to keep pointers in aligned positions.

```R
1 fn eval(x:Exp) => Exp {
2   match x {
3     I(_)| V(_)=> x,
4     Plus(e1,e2)=> match eval(e1), eval(e2) {
5       I(x1), I(x2)=> I(x1+x2),
6       e1', e2' => Plus(e1', e2')
7   }}}
```

(b) User implementation of eval.

```R
1 fn eval(x: Exp) : Exp {
2   match x {
3     Plus(_,_)=>
4       let e1:Exp = x.Plus.0; let e2:Exp = x.Plus.1;
5       let e1':Exp = eval(e1); let e2':Exp = eval(e2);
6     match e1', e2' {
7       I(_), I(_)=>
8         let x1 : i32 = e1'.I;
9         let x2 : i32 = e2'.I;
10        let i : i32 = ADD(x1, x2);
11        I(i),
12        _ , _ =>
13         Plus(e1', e2'),
14     },
15   }=> x,
16 }}
```

(c) Normalized representation of eval. Explicitly typed A-Normal Form version of the code, where patterns have no variables, and accesses are made through paths instead. For instance x.Plus.0 is the first operand under a Plus constructor in x. Such accesses are only valid under the right pre-conditions.

<figure><img src="image_3.png" /></figure>

(d) Simplified CFG of eval. For pedagogic and readability purposes, code has been simplified (block sinking, variable renaming, simple constant propagation).

<caption>Fig. 5. Arithmetic expressions, their representation, and the eval function in RIBBIT. Full interactive example available at https://ribbit.gitlabpages.inria.fr/ribbit/#arith_expr_icfp.rbt.</caption>
```R
1 enum Exp { V(String), I(i32), Plus(Exp, Exp) }
2 represented as
3 split .[0, 2] {
4 | 0 from Plus =>
5 &<64, 2>(split .0 {
6 | 0 from Plus(I,_) =>
7 | {{w32, _Plus.0.I as w32, _Plus.1 as Exp}}
8 | 1 from Plus(Plus|V, I) =>
9 | {{w32, _Plus.1.I as w32, _Plus.0 as Exp}}
10 | 2 from (Plus(Plus|V,Plus|V)) =>
11 | {{w32, _32, _Plus.0 as Exp, _Plus.1 as Exp}}
12 })
13 | 1 from I => w64 with .[32, 32] : (_I as w32)
14 | 2 from V => &<64, 2>(._V as String)
15 }
```

(a) Arithmetic expressions and their representation. On the first layer, this representation stores the tag distinguishing between V, I, and Plus in the two lowest bits. This potentially leverages bit-stealing in pointer alignment bits. For Plus constructors, we use a struct whose first field indicates the more precise layout. Some space could be used to store an operator (MULT, ...) as well. Fields are arranged to keep pointers in aligned positions.

```R
1 fn eval(x:Exp) => Exp {
2   match x {
3     I(_)| V(_)=> x,
4     Plus(e1,e2)=> match eval(e1), eval(e2) {
5       I(x1), I(x2)=> I(x1+x2),
6       e1', e2' => Plus(e1', e2')
7   }}}
```

(b) User implementation of eval.

```R
1 fn eval(x: Exp) : Exp {
2   match x {
3     Plus(_,_)=>
4       let e1:Exp = x.Plus.0; let e2:Exp = x.Plus.1;
5       let e1':Exp = eval(e1); let e2':Exp = eval(e2);
6     match e1', e2' {
7       I(_), I(_)=>
8         let x1 : i32 = e1'.I;
9         let x2 : i32 = e2'.I;
10        let i : i32 = ADD(x1, x2);
11        I(i),
12        _ , _ =>
13         Plus(e1', e2'),
14     },
15   }=> x,
16 }}
```

(c) Normalized representation of eval. Explicitly typed A-Normal Form version of the code, where patterns have no variables, and accesses are made through paths instead. For instance x.Plus.0 is the first operand under a Plus constructor in x. Such accesses are only valid under the right pre-conditions.

<figure><img src="image_3.png" /></figure>

(d) Simplified CFG of eval. For pedagogic and readability purposes, code has been simplified (block sinking, variable renaming, simple constant propagation).

<caption>Fig. 5. Arithmetic expressions, their representation, and the eval function in RIBBIT. Full interactive example available at https://ribbit.gitlabpages.inria.fr/ribbit/#arith_expr_icfp.rbt.</caption>
with the pattern matching above. Again, in all cases, the emitted code allocates and places every bit in memory. Again, we had to synthesize a morphism between the memory representation of the present pieces (*e1'* and *e2') and the one contained inside a Plus constructor.

Naturally, to reap the full power of our tweaked representation, one would need to unroll the eval function, allowing to completely skip some intermediary products. We consider such transformations orthogonal to our contribution, and focus on emitting straightforward code that is easily optimized by existing state-of-the-art transformations (here, unrolling and constant propagation).

As shown here, in order to properly compile programs manipulating complex representations, RIBBIT can generate morphisms: code converting between different memory representations of the same source type. In fact, programmers themselves can also leverage that feature! For instance, given a naive AST-style representation of arithmetic expressions ExpAST and our optimised version Exp, both sharing the same source definition, we can readily write the following function:

```h
fn convert(x:ExpAST) -> Exp {x}
```

Our approach will readily generate the full (recursive!) code that manifests the isomorphism between these two structures.

All these behaviors, and all examples developed in this article, can be experimented upon interactively on https://ribbit.gitlabpages.inria.fr/ribbit/. Our prototype online implementation can verify validity of types, memory layouts and programs; compile programs to our intermediate representation, show the obtained programs, and run them. In addition, it will verify correction of the obtained compiled code against a reference source interpreter.

## 2.3 Contribution and Outline

In this article, we define a general procedure which compiles (potentially nested) accessors, constructors, pattern matching, and both together, without introducing superfluous work.

Our approach works for rich and custom memory representations in the style of Baudon et al. [2023], and is able to compile any well-typed high-level ADT-manipulating program, including in the presence of recursive types and recursive code emission. For this purpose, our approach can synthesise, when necessary, the code manifesting any isomorphism between memory representations of compatible types. We emit low-level code with precise memory manipulation thanks to the use of a destination passing intermediary representation [Shaikhha et al. 2017]. We also state the correctness of our algorithms against a source-level semantics. Finally, we implemented our algorithm (an online version can be found at https://ribbit.gitlabpages.inria.fr/ribbit/), evaluated it on numerous examples, and tested the correctness of our compilation procedure against a reference interpreter.

Section 3 describes our input language based on types and memory layouts from Baudon et al. [2023]. Section 4 presents our target intermediate representation. Our approach relies on existing pattern matching compilation techniques, which we detail in Section 5. From a first partial algorithm, in Section 6, working on simple (not "intricate") representations, we then derive our main contribution, detailed in Section 7: a complete compilation algorithm for expressions constructing ADT values according to custom memory layouts. Finally, we sketch the metatheoretic properties of our algorithms in Section 8.

## 3 ALGEBRAIC DATA TYPES AND THEIR LAYOUTS

We first present our input language. From the type perspective, as highlighted in Section 2, we use a two-tiered view: *algebraic data types* used for programming and *memory layouts* detailing how to represent them in memory. The formal presentation of these types and layouts extends Baudon et al. [2023] with most of its limitations lifted. In addition, we introduce a complete expression language to both destruct and construct values of such types.
with the pattern matching above. Again, in all cases, the emitted code allocates and places every bit in memory. Again, we had to synthesize a morphism between the memory representation of the present pieces (*e1'* and *e2'* ) and the one contained inside a Plus constructor.

Naturally, to reap the full power of our tweaked representation, one would need to unroll the eval function, allowing to completely skip some intermediary products. We consider such transfor- mations orthogonal to our contribution, and focus on emitting straightforward code that is easily optimized by existing state-of-the-art transformations (here, unrolling and constant propagation).

As shown here, in order to properly compile programs manipulating complex representations, RIBBIT can generate morphisms: code converting between different memory representations of the same source type. In fact, programmers themselves can also leverage that feature! For instance, given a naive AST-style representation of arithmetic expressions ExpAST and our optimised version Exp, both sharing the same source definition, we can readily write the following function:

1 fn convert(x:ExpAST) -> Exp {x}

Our approach will readily generate the full (recursive!) code that manifests the isomorphism between these two structures.

All these behaviors, and all examples developed in this article, can be experimented upon interactively on https://ribbit.gitlabpages.inria.fr/ribbit/. Our prototype online implementation can verify validity of types, memory layouts and programs; compile programs to our intermediate representation, show the obtained programs, and run them. In addition, it will verify correction of the obtained compiled code against a reference source interpreter.

2.3 Contribution and Outline

In this article, we define a general procedure which compiles (potentially nested) accessors, con-
STRUCTORS, pattern matching, and *both* together, without introducing superfluous work.

Our approach works for rich and custom memory representations in the style of Baudon et al. [2023], and is able to compile any well-typed high-level ADT-manipulating program, including in the presence of recursive types and recursive code emission. For this purpose, our approach can synthesise, when necessary, the code manifesting any isomorphism between memory representations of compatible types. We emit low-level code with precise memory manipulation thanks to the use of a destination passing intermediary representation [Shaikhha et al. 2017]. We also state the correctness of our algorithms against a source-level semantics. Finally, we implemented our algorithm (an online version can be found at https://ribbit.gitlabpages.inria.fr/ribbit/), evaluated it on numerous examples, and tested the correctness of our compilation procedure against a reference interpreter.

Section 3 describes our input language based on types and memory layouts from Baudon et al. [2023]. Section 4 presents our target intermediate representation. Our approach relies on existing pattern matching compilation techniques, which we detail in Section 5. From a first partial algorithm, in Section 6, working on simple (not “intricate”) representations, we then derive our main contribution, detailed in Section 7: a complete compilation algorithm for expressions constructing ADT values according to custom memory layouts. Finally, we sketch the metatheoretic properties of our algorithms in Section 8.

3 ALGEBRAIC DATA TYPES AND THEIR LAYOUTS

We first present our input language. From the type perspective, as highlighted in Section 2, we use
a two-tiered view: *algebraic data types* used for programming and *memory layouts* detailing how to
represent them in memory. The formal presentation of these types and layouts extends Baudon
et al. [2023] with most of its limitations lifted. In addition, we introduce a complete expression
language to both destruct and construct values of such types.
$$
\begin{array}{l@{\hspace{2em}}l@{\hspace{2em}}l}
\tau \in \mathit{Types} ::= t \in \mathit{TyVars} & \text{(variables)} & p \in P \subseteq \mathit{Provs} ::= \_ | \langle p_0, \dots, p_{n-1} \rangle | K(p) \\
\phantom{\tau \in \mathit{Types} ::=} | I_l & \text{($l$-bit wide integers)} & \text{(provenances and their sets)} \\
\phantom{\tau \in \mathit{Types} ::=} | \langle \tau_0, \dots, \tau_{n-1} \rangle & \text{(tuples)} & \pi \in \mathit{Paths} ::= \epsilon \quad \text{(empty path)} \\
\phantom{\tau \in \mathit{Types} ::=} | K_1(\tau_1)' |' \dots |' K_n(\tau_n) & \text{(sums)} & | \pi.[o : l] \quad \text{($l$ bits at offset $o$)} \\
v \in \mathit{Values} ::= c | \langle v_0, \dots, v_{n-1} \rangle | K(v) & \text{(values)} & | \pi.i \quad \text{(field access)} \\
& & | \pi.K \quad \text{(constructor access)}
\end{array}
$$

<caption>Fig. 6. Algebraic Data Types and other high-level objects</caption>

As general meta-syntactic conventions:

* Syntactic categories are in *italics* (TyVars, Exps, ...).

* Each syntactic category has a dedicated meta-syntactic letter (e for elements of Exps, ...) and a capital for sets (E for sets of Exps elements, ...)

* Lists, sets and maps are indicated either *in-extenso* ($\tau_0, \dots, \tau_{n-1}$), with a Python-like notation ($\{e_i | 0 \le i < n\}$), or with a sequence-like notation ($\langle x_i \rangle_{1 \le i \le n}$).

## 3.1 Algebraic Data Types

The grammar for Algebraic Data Types is presented in Fig. 6. We denote types using $\tau$ and type variables with $t \in \mathit{TyVars}$. Primitive types consist of fixed-width signed integers, denoted $I_t$. We denote all tuples with angle brackets, for instance $\langle I_{32}, I_{32} \rangle$ for pairs of 32-bit integers. Constructors of sums are marked with a capital letter and separated from each other with vertical bars, for instance “None | Some($t$)” is an option type. In examples, we use $K$ as shortcut for $K(\langle\rangle)$ and $K(\tau_1, \dots, \tau_n)$ for $K(\langle\tau_1, \dots, \tau_n\rangle)$. *Values* of Algebraic Data Types, dubbed “high-level values”, consist of integer constants denoted $c$, tuples and constructors.

We now define two related constructs: *provenances* and *paths*. Provenances give partial information on what a value looks like: a tuple, a head constructor with nested provenances, or anything (wildcard: `_`). Paths precisely indicate the position of a subterm in a given type, value or provenance, using position accesses `i` to deconstruct tuples, head constructors `.K` for constructor values and bit ranges `[o : l]` consisting of an offset $o$ and a width $l$ for integers.

**Focusing and specialisation.** We also define two accompanying operations, which will be demonstrated on examples below. The *focusing* operation, denoted **focus** ($\pi, \theta$) where $\theta \in \mathit{Types} \cup \mathit{Values} \cup \mathit{Provs} \cup \mathit{Paths}$ is a high-level object (type, value, provenance or path), accesses the subterm of $\theta$ located at $\pi$. It follows the syntax to extract the subterm at position $\pi$. The *specialisation* operation on ADTs, denoted $\tau/p$, restricts a type $\tau$ to values that match a given provenance $p$. It syntactically filters irrelevant constructors. The full definitions for both can be found in Appendix A.

**Example 3.1 (High-level types and values).** Our high-level type for RISC-V 32-bit instructions is a sum type with four constructors:

$$ \tau_{\text{RISC-V}} = \text{Add}(\tau_{\text{reg}}, \tau_{\text{reg}}, \tau_{\text{reg}}) | \text{Addi}(\tau_{\text{reg}}, \tau_{\text{reg}}, I_{12}) | \text{Jal}(\tau_{\text{reg}}, I_{20}) | \text{Sw}(\tau_{\text{reg}}, \tau_{\text{reg}}, I_{12}) $$

where $\tau_{\text{reg}}$ is a simple sum type enumerating the 32 available RISC-V registers: $\tau_{\text{reg}} = X_0 | \dots | X_{31}$.

Given this definition, the high-level value Addi($X_2, X_2, 3$) of type $\tau_{\text{RISC-V}}$ represents the instruction `addi x2, x2, 3`. The path `Addi.0` designates the first argument of any `addi` instruction, namely its destination register. We can focus on “the part that is relevant to `Addi.0`” in the type $\tau_{\text{RISC-V}}$:

$$ \mathbf{focus} (.\text{Addi.0}, \tau_{\text{RISC-V}}) = \mathbf{focus} (.\text{Addi.0}, \text{Addi}(\tau_{\text{reg}}, \tau_{\text{reg}}, I_{12})) = \tau_{\text{reg}} $$
<figure><img src="image_4.png" /><figcaption>Fig. 6. Algebraic Data Types and other high-level objects</figcaption></figure>

As general meta-syntactic conventions:

* Syntactic categories are in *italics* (TyVars, Exps, ...).

* Each syntactic category has a dedicated meta-syntactic letter (e for elements of Exps, ...) and a capital for sets (E for sets of Exps elements, ...)

* Lists, sets and maps are indicated either *in-extenso* ($\tau_0, \dots, \tau_{n-1}$), with a Python-like notation ($\{e_i | 0 \le i < n\}$), or with a sequence-like notation ($\langle x_i \rangle_{1 \le i \le n}$).

## 3.1 Algebraic Data Types

The grammar for Algebraic Data Types is presented in Fig. 6. We denote types using $\tau$ and type variables with $t \in TyVars$. Primitive types consist of fixed-width signed integers, denoted $I_t$. We denote all tuples with angle brackets, for instance $\langle I_{32}, I_{32} \rangle$ for pairs of 32-bit integers. Constructors of sums are marked with a capital letter and separated from each other with vertical bars, for instance "None | Some(t)" is an option type. In examples, we use $K$ as shortcut for $K(\langle \rangle)$ and $K(\tau_1, \dots, \tau_n)$ for $K(\langle \tau_1, \dots, \tau_n \rangle)$. *Values* of Algebraic Data Types, dubbed "high-level values", consist of integer constants denoted $c$, tuples and constructors.

We now define two related constructs: *provenances* and *paths*. Provenances give partial information on what a value looks like: a tuple, a head constructor with nested provenances, or anything (wildcard: `=`). Paths precisely indicate the position of a subterm in a given type, value or provenance, using position accesses `i` to deconstruct tuples, head constructors `.K` for constructor values and bit ranges `[o : l]` consisting of an offset $o$ and a width $l$ for integers.

**Focusing and specialisation.** We also define two accompanying operations, which will be demonstrated on examples below. The *focusing* operation, denoted **focus** ($\pi, \theta$) where $\theta \in \text{Types} \cup \text{Values} \cup \text{Provs} \cup \text{Paths}$ is a high-level object (type, value, provenance or path), accesses the subterm of $\theta$ located at $\pi$. It follows the syntax to extract the subterm at position $\pi$. The *specialisation* operation on ADTs, denoted $\tau/p$, restricts a type $\tau$ to values that match a given provenance $p$. It syntactically filters irrelevant constructors. The full definitions for both can be found in Appendix A.

**Example 3.1 (High-level types and values).** Our high-level type for RISC-V 32-bit instructions is a sum type with four constructors:

$$ \tau_{\text{RISC-V}} = \text{Add}(\tau_{\text{reg}}, \tau_{\text{reg}}, \tau_{\text{reg}}) \mid \text{Addi}(\tau_{\text{reg}}, \tau_{\text{reg}}, I_{12}) \mid \text{Jal}(\tau_{\text{reg}}, I_{20}) \mid \text{Sw}(\tau_{\text{reg}}, \tau_{\text{reg}}, I_{12}) $$

where $\tau_{\text{reg}}$ is a simple sum type enumerating the 32 available RISC-V registers: $\tau_{\text{reg}} = X_0 | \dots | X_{31}$.

Given this definition, the high-level value Addi($X_2, X_2, 3$) of type $\tau_{\text{RISC-V}}$ represents the instruction `addi x2, x2, 3`. The path `Addi.0` designates the first argument of any `addi` instruction, namely its destination register. We can focus on "the part that is relevant to `Addi.0`" in the type $\tau_{\text{RISC-V}}$:

$$ \textbf{focus} (.\text{Addi.0}, \tau_{\text{RISC-V}}) = \textbf{focus} (.\text{Addi.0}, \text{Addi}(\tau_{\text{reg}}, \tau_{\text{reg}}, I_{12})) = \tau_{\text{reg}} $$
<figure><img src="image_4.png" /><figcaption>Fig. 7. Memory layouts and paths</figcaption></figure>

and similarly, in our high-level value: **focus** (.Addi.0, Addi($X_2$, $X_2$, 3)) = $X_2$. The provenance $\text{Sw}(X_2, \_, \_)$ matches sw instructions whose destination register is x2. The specialisation of $\tau_{\text{RISC-V}}$ for this provenance is the following type: $\tau_{\text{RISC-V}}/\text{Sw}(X_2, \_, \_) = \text{Sw}(X_2, \tau_{\text{reg}}, I_{12}) \triangle$

## 3.2 Memory Layouts

Each ADT is associated with a *memory layout* which specifies how its values should be represented in memory. As a general convention, memory elements are distinguished with a hat. Memory layouts, denoted $\hat{\tau}$ and defined in Fig. 7, feature two types of constructs: some describe concrete memory structures, others refer back to the represented high-level type. Concrete memory structures consist of opaque words $\underline{\ell}$ representing $\ell$ unused contiguous bits, fixed-width integer constants and pointers, or structs aggregating several fields together. Finally, composite words, denoted $\hat{\tau} \bowtie_{0 \le i < n} [o_i : \ell_i] : \hat{\tau}_i$, specify the contents of $n$ unused bit ranges within a word type $\hat{\tau}$. Unused bits include all parts of opaque words and architecture/implementation-dependent locations such as address alignment bits in pointers. In any case, the $n$ bit ranges must not overlap. Constructs that refer back to the represented high-level type consist of fixed-width encodings $I_\ell$ for values of integer types (the precise encoding used is implementation-dependent), and of two more complex constructs: fragments and splits.

Fragments refer to subterms within the high-level type and indicate their layout: the fragment $(\pi$ as $\hat{\tau})$ stands for the representation according to the layout $\hat{\tau}$ of the subterm located at $\pi$ within the high-level value being represented. Fragments may refer to arbitrarily nested subterms.

Splits create disjunctions between different possible layouts by designating a position in memory as a *discriminant*: split $(\hat{\pi}) \{c_i \text{ from } P_i \Rightarrow \hat{\tau}_i \mid 1 \le i \le n\}$ indicates that if the contents of memory at position $\hat{\pi}$ are equal to $c_i$, then the memory value under scrutiny follows the layout $\hat{\tau}_i$ and represents a high-level value whose provenance belongs to the set $P_i$. The validity of a split construct depends on each $\hat{\tau}_i$ actually containing the value $c_i$ (specified as a constant $(c_i)_\ell$) at position $\hat{\pi}$: it ensures
<figure><img src="image_5.png" /><figcaption>Fig. 7. Memory layouts and paths</figcaption></figure>

and similarly, in our high-level value: **focus** (.Addi.0, Addi($X_2$, $X_2$, 3)) = $X_2$. The provenance $\text{Sw}(X_2, \_\_)$ matches sw instructions whose destination register is x2. The specialisation of $\tau_{\text{RISC-V}}$ for this provenance is the following type: $\tau_{\text{RISC-V}}/\text{Sw}(X_2, \_, \_) = \text{Sw}(X_2, \tau_{\text{reg}}, I_{12}) \triangle$

## 3.2 Memory Layouts

Each ADT is associated with a *memory layout* which specifies how its values should be represented in memory. As a general convention, memory elements are distinguished with a hat. Memory layouts, denoted $\hat{\tau}$ and defined in Fig. 7, feature two types of constructs: some describe concrete memory structures, others refer back to the represented high-level type. Concrete memory structures consist of opaque words $\_\ell$ representing $\ell$ unused contiguous bits, fixed-width integer constants and pointers, or structs aggregating several fields together. Finally, composite words, denoted $\hat{\tau} \bowtie_{0\le i<n} [o_i : \ell_i] : \hat{\tau}_i$, specify the contents of $n$ unused bit ranges within a word type $\hat{\tau}$. Unused bits include all parts of opaque words and architecture/implementation-dependent locations such as address alignment bits in pointers. In any case, the $n$ bit ranges must not overlap. Constructs that refer back to the represented high-level type consist of fixed-width encodings $I_\ell$ for values of integer types (the precise encoding used is implementation-dependent), and of two more complex constructs: fragments and splits.

Fragments refer to subterms within the high-level type and indicate their layout: the fragment $(\pi$ as $\hat{\tau})$ stands for the representation according to the layout $\hat{\tau}$ of the subterm located at $\pi$ within the high-level value being represented. Fragments may refer to arbitrarily nested subterms.

Splits create disjunctions between different possible layouts by designating a position in memory as a *discriminant*: split $(\hat{\pi}) \{c_i \text{ from } P_i \Rightarrow \hat{\tau}_i \mid 1 \le i \le n\}$ indicates that if the contents of memory at position $\hat{\pi}$ are equal to $c_i$, then the memory value under scrutiny follows the layout $\hat{\tau}_i$ and represents a high-level value whose provenance belongs to the set $P_i$. The validity of a split construct depends on each $\hat{\tau}_i$ actually containing the value $c_i$ (specified as a constant $(c_i)_\ell$) at position $\hat{\pi}$: it ensures
that it is possible to retrieve the provenance of any value from its representation only, by inspecting its contents at $\hat{\pi}$.

**Example 3.2 (Memory layout for RISC-V).** Here are the layouts of the types from Example 3.1:

$$ \hat{\tau}_{\text{reg}} = \text{split}(\epsilon) \left\{ \begin{array}{l} 0 \text{ from } X_0 \Rightarrow (0)_5 \\ \vdots \\ 31 \text{ from } X_{31} \Rightarrow (31)_5 \end{array} \right\} \quad \hat{\tau}_{\text{RISC-V}} = \text{split}(.[0:7]) \left\{ \begin{array}{l} 0 \times 33 \text{ from Add}(\_, \_, \_) \Rightarrow \hat{\tau}_{\text{Add}} \\ 0 \times 13 \text{ from Addi}(\_, \_, \_) \Rightarrow \hat{\tau}_{\text{Addi}} \\ 0 \times 6F \text{ from Jal}(\_, \_, \_) \Rightarrow \hat{\tau}_{\text{Jal}} \\ 0 \times 23 \text{ from Sw}(\_, \_, \_) \Rightarrow \hat{\tau}_{\text{Sw}} \end{array} \right\} $$

The split describes how to distinguish between instructions, by inspecting the 7 lowest bits (0xXX are fixed constants). Layouts for individual instructions (e.g., Sw) are built from an opaque 32-bit word _32 whose contents are specified by constraints on subranges of bits:

$$ \hat{\tau}_{\text{Sw}} = _{32} \bowtie [0:7] : (0 \times 23)_7 \bowtie [12:3] : (2)_3 \quad (\text{opcode and funct3 const}) $$

$$ \bowtie [15:5] : (.\text{Sw.0 as } \hat{\tau}_{\text{reg}}) \bowtie [20:5] : (.\text{Sw.1 as } \hat{\tau}_{\text{reg}}) \quad (\text{registers rs1 and rs2}) $$

$$ \bowtie [7:5] : (.\text{Sw.2.} [0:5] \text{ as } I_5) \bowtie [25:7] : (.\text{Sw.2.} [5:7] \text{ as } I_7) \quad (\text{imm in split ranges}) $$

For instance, the fragment (.Sw.0 as $\hat{\tau}_{\text{reg}}$) expresses that bits 15 to 19 inclusive contain the representation of the first argument of Sw (base register, rs1) according to the $\hat{\tau}_{\text{reg}}$ layout. $\Delta$

**Example 3.3 (Memory layout for lists).** Consider lists of 32-bit integers $\tau = \text{Nil} | \text{Cons}(I_{32}, \tau)$, and a packed layout with up to two elements per level of indirection, with three branches: empty or a singleton list – both immediately encoded – or a pointer to a block of two integers and a list:

$$ \begin{array}{l} \hat{\tau}_p = \text{split}(.[0:2]) \{ \\ \quad 0 \text{ from } \text{Nil} \Rightarrow _{-64} \\ \quad 1 \text{ from } \text{Cons}(\_, \text{Nil}) \Rightarrow _{-64} \bowtie [2:32] : (.\text{Cons.0 as } I_{32}) \\ \quad 2 \text{ from } \text{Cons}(\_, \text{Cons}(\_, \_)) \Rightarrow \\ \quad \quad \&_{64} (\{ (.\text{Cons.0 as } I_{32}), (.\text{Cons.1.Const.0 as } I_{32}), (.\text{Cons.1.Const.1 as } \hat{\tau}_p) \}) \\ \} \end{array} $$

$\Delta$

**Memory Paths and Focusing.** Similarly to high-level types, we define paths, provenances and focusing for memory layouts. Memory paths, denoted $\hat{\pi}$ (see Fig. 7), indicate positions in layouts. Memory path operations consist of struct field accesses, pointer dereference, and two operations that deconstruct composite words: bit range extraction to focus on the contents of a specific bit range and bitwise “and” to discard ranges that lie outside of a bit mask. Similarly to high-level paths, we define the memory focus operation $\widehat{\text{focus}}$ ($\hat{\pi}, \hat{\tau}$) that extracts the subterm at position $\hat{\pi}$ within $\hat{\tau}$ (it is undefined on fragments and splits; the full definition is in Appendix A).

**Example 3.4 (Paths and Focusing for $\hat{\tau}_{\text{RISC-V}}$).** The memory path .[15:5] denotes the 5 bits starting from offset 15 (included) within a word. Focusing on this path in $\hat{\tau}_{\text{Sw}}$ yields the fragment corresponding to the base register of a sw instruction: $\widehat{\text{focus}}$ (.[15:5], $\hat{\tau}_{\text{Sw}}$) = (.Sw.0 as $\hat{\tau}_{\text{reg}}$). $\Delta$

## 3.3 Input Programs

We can now define high-level programs that manipulate ADT values according to a given memory layout specification. Our general goal is to compile such programs to low-level programs that operate on memory directly, with respect to the specified memory layout. Our input language consists of expressions, denoted e and defined in Fig. 8. For presentation purposes, we consider an explicitly-typed, already simplified input language, corresponding to the internal representation
that it is possible to retrieve the provenance of any value from its representation only, by inspecting
its contents at $\hat{\pi}$.

**Example 3.2 (Memory layout for RISC-V).** Here are the layouts of the types from Example 3.1:

$$ \hat{\tau}_{\text{reg}} = \text{split}(\epsilon) \left\{ \begin{array}{l} 0 \text{ from } X_0 \Rightarrow (0)_5 \\ \vdots \\ 31 \text{ from } X_{31} \Rightarrow (31)_5 \end{array} \right\} \quad \hat{\tau}_{\text{RISC-V}} = \text{split}(.[0:7]) \left\{ \begin{array}{l} 0 \times 33 \text{ from Add}(\_, \_, \_) \Rightarrow \hat{\tau}_{\text{Add}} \\ 0 \times 13 \text{ from Addi}(\_, \_, \_) \Rightarrow \hat{\tau}_{\text{Addi}} \\ 0 \times 6F \text{ from Jal}(\_, \_, \_) \Rightarrow \hat{\tau}_{\text{Jal}} \\ 0 \times 23 \text{ from Sw}(\_, \_, \_) \Rightarrow \hat{\tau}_{\text{Sw}} \end{array} \right\} $$

The split describes how to distinguish between instructions, by inspecting the 7 lowest bits (θxXX are fixed constants). Layouts for individual instructions (e.g., Sw) are built from an opaque 32-bit word _32 whose contents are specified by constraints on subranges of bits:

$$ \hat{\tau}_{\text{Sw}} = _{32} \bowtie [0:7] : (0 \times 23)_7 \bowtie [12:3] : (2)_3 \quad (\text{opcode and funct3 const}) $$

$$ \bowtie [15:5] : (.\text{Sw.0 as } \hat{\tau}_{\text{reg}}) \bowtie [20:5] : (.\text{Sw.1 as } \hat{\tau}_{\text{reg}}) \quad (\text{registers rs1 and rs2}) $$

$$ \bowtie [7:5] : (.\text{Sw.2.}[0:5] \text{ as } I_5) \bowtie [25:7] : (.\text{Sw.2.}[5:7] \text{ as } I_7) \quad (\text{imm in split ranges}) $$

For instance, the fragment (.Sw.0 as $\hat{\tau}_{\text{reg}}$) expresses that bits 15 to 19 inclusive contain the representation of the first argument of Sw (base register, rs1) according to the $\hat{\tau}_{\text{reg}}$ layout. $\Delta$

**Example 3.3 (Memory layout for lists).** Consider lists of 32-bit integers $\tau = \text{Nil} | \text{Cons}(I_{32}, \tau)$, and a packed layout with up to two elements per level of indirection, with three branches: empty or a singleton list – both immediately encoded – or a pointer to a block of two integers and a list:

$$ \begin{array}{l} \hat{\tau}_p = \text{split}(.[0:2]) \{ \\ \quad 0 \text{ from } \text{Nil} \Rightarrow _{-64} \\ \quad 1 \text{ from } \text{Cons}(\_, \text{Nil}) \Rightarrow _{-64} \bowtie [2:32] : (.\text{Cons.0 as } I_{32}) \\ \quad 2 \text{ from } \text{Cons}(\_, \text{Cons}(\_, \_)) \Rightarrow \\ \quad \quad \&_{64} (\{ (.\text{Cons.0 as } I_{32}), (.\text{Cons.1.Const.0 as } I_{32}), (.\text{Cons.1.Const.1 as } \hat{\tau}_p) \}) \\ \} \end{array} $$

$\Delta$

*Memory Paths and Focusing.* Similarly to high-level types, we define paths, provenances and focusing for memory layouts. Memory paths, denoted $\hat{\pi}$ (see Fig. 7), indicate positions in layouts. Memory path operations consist of struct field accesses, pointer dereference, and two operations that deconstruct composite words: bit range extraction to focus on the contents of a specific bit range and bitwise “and” to discard ranges that lie outside of a bit mask. Similarly to high-level paths, we define the *memory focus* operation $\widehat{\text{focus}}$ ($\hat{\pi}, \hat{\tau}$) that extracts the subterm at position $\hat{\pi}$ within $\hat{\tau}$ (it is undefined on fragments and splits; the full definition is in Appendix A).

**Example 3.4 (Paths and Focusing for $\hat{\tau}_{\text{RISC-V}}$).** The memory path `[15:5]` denotes the 5 bits starting from offset 15 (included) within a word. Focusing on this path in $\hat{\tau}_{\text{Sw}}$ yields the fragment corresponding to the base register of a sw instruction: $\widehat{\text{focus}}(.[15:5], \hat{\tau}_{\text{Sw}}) = (.\text{Sw.0 as } \hat{\tau}_{\text{reg}})$. $\Delta$

## 3.3 Input Programs

We can now define high-level programs that manipulate ADT values according to a given memory layout specification. Our general goal is to compile such programs to low-level programs that operate on memory directly, with respect to the specified memory layout. Our input language consists of expressions, denoted e and defined in Fig. 8. For presentation purposes, we consider an explicitly-typed, already simplified input language, corresponding to the internal representation
$$
\begin{array}{l@{\qquad}l@{\qquad}l}
u \in \mathbf{ValuExprs} ::= x.\pi & \text{(variable accessor)} & e \in \mathbf{Exprs} ::= u & \text{(value building)} \\
| c & \text{(integer constant)} & | \text{let } x : \tau \text{ as } \hat{\tau} = e \text{ in } e' & \\
| \langle u_0, \dots, u_{n-1} \rangle & \text{(tuple)} & & \text{(let-binding)} \\
| K(u) & \text{(constructor)} & | \text{match}(x)\{p_1 \to e_1 | \dots | p_n \to e_n\} & \\
& & & \text{(pattern matching)}
\end{array}
$$

<caption>Fig. 8. Program syntax.</caption>

$$
\begin{align*}
& a \in \mathit{Addr}s \qquad \zeta : \mathit{Addr}s \to \widehat{\mathit{Values}} \tag{addresses and stores} \\
& \hat{v} \in \widehat{\mathit{Values}} ::= \underline{\ell} \mid (c)_\ell \mid \&_\ell (a) \mid \hat{v} \underset{0 \le i < n}{\bowtie} [o_i : \ell_i] : \hat{v}_i \mid \{\hat{v}_0, \dots, \hat{v}_{n-1}\} \tag{memory values} \\
& \hat{p} \in \widehat{\mathit{Provs}} ::= \underline{\ell} \mid (c)_\ell \mid \&_\ell (\hat{p}) \mid \hat{p} \underset{0 \le i < n}{\bowtie} [o_i : \ell_i] : \hat{p}_i \mid \{\hat{p}_0, \dots, \hat{p}_{n-1}\} \tag{memory shapes}
\end{align*}
$$

<caption>Fig. 9. Memory contents and shapes.</caption>

from Fig. 5c. Expressions are in A-normal form: every value is let-bound to a variable. Programs
manipulate ADT values through *pattern matching* to destruct values, and *value-building expressions*
to construct values according to a given memory layout.

A pattern-matching expression contains a list of *cases* of the form *p* → *e*, each consisting of a
provenance on the left-hand side and an expression on the right-hand side. Note that provenances
contain no variables. In some of our examples, we will use *or-patterns* such as *p*₁ | *p*₂ → *e*.

*Value expressions*, denoted *u*, allow to define values with reference to other already-bound values, using accessors of the form *x*.π. Such accessors designate subterms at position *π* within an existing value bound to *x*.

Example 3.5 (Value xpression). The valuenxpression u = Jal(x.Jal.0, 42) builds a jal instruc-
tion using the same destination register as another jal instruction bound to x, and the con-
stant immediate 42. Note that focusing on a valuenpr does not evaluate accessors: we have
focus (.Jal.0, u) = x.Jal.0.

Δ

Example 3.6 (RISC-V destination register binding). The following program extracts the destination register of a RISC-V instruction if it exists, and returns X₀ otherwise:

$$
\text{get\_dest}(x : \tau_{\text{RISC-V}} \text{ as } \hat{\tau}_{\text{RISC-V}}) : \tau_{\text{reg}} \text{ as } \hat{\tau}_{\text{reg}} = \text{match}(x) \quad \begin{array}{@{}c@{}} \left\{ \begin{array}{@{}l@{}} \text{Add}(..., ..., ...) \rightarrow x.\text{Add}.0 \\ \text{Addi}(..., ..., ...) \rightarrow x.\text{Addi}.0 \\ \text{Jal}(..., ...) \rightarrow x.\text{Jal}.0 \\ \text{Sw}(..., ..., ...) \rightarrow X_0 \end{array} \right\} \\ \Delta \end{array}
$$

**3.4 Memory Model**

We model memory contents with values and stores, defined in Fig. 7. Memory values, denoted
$\hat{v}$, follow roughly the same syntax as layouts, excluding constructs that do not relate to concrete
memory contents (integer encodings, fragments and splits). The main difference is that pointers do
not directly contain the pointee memory value, but refer to it with an address *a*. Interpretation of
memory values therefore relies on a store, denoted $\zeta$, which maps addresses to memory values.

Example 3.7 (RISC-V memory values). Consider the high-level value *v* = Sw(*X*₂, *X*₂, 3), of type τ<sub>RISC-V</sub>. The memory value representing *X*₂ according to τ<sub>reg</sub> is (2)₅. We can similarly follow the layout τ<sub>RISC-V</sub> to represent *v*, by instantiating each split, fragment and non-constant integer with *v* contents, and get the following memory value (which corresponds to the “assembled” version of
$$
\begin{array}{l@{\qquad}l@{\qquad}l}
u \in \mathbf{ValuExprs} ::= x.\pi & \text{(variable accessor)} & e \in \mathbf{Exprs} ::= u & \text{(value building)} \\
| c & \text{(integer constant)} & | \text{let } x : \tau \text{ as } \hat{\tau} = e \text{ in } e' & \\
| \langle u_0, \dots, u_{n-1} \rangle & \text{(tuple)} & & \text{(let-binding)} \\
| K(u) & \text{(constructor)} & | \text{match}(x)\{p_1 \to e_1 | \dots | p_n \to e_n\} & \\
& & & \text{(pattern matching)}
\end{array}
$$

<caption>Fig. 8. Program syntax.</caption>

$$
\begin{align*}
& a \in \mathit{Addr}s \qquad \zeta : \mathit{Addr}s \rightarrow \widehat{\mathit{Values}} \tag{addresses and stores} \\
& \hat{v} \in \widehat{\mathit{Values}} ::= \underline{\ell} \mid (c)_\ell \mid \&_\ell (a) \mid \hat{v} \underset{0 \le i < n}{\bowtie} [o_i : \ell_i] : \hat{v}_i \mid \{\hat{v}_0, \dots, \hat{v}_{n-1}\} \tag{memory values} \\
& \hat{p} \in \widehat{\mathit{Provs}} ::= \underline{\ell} \mid (c)_\ell \mid \&_\ell (\hat{p}) \mid \hat{p} \underset{0 \le i < n}{\bowtie} [o_i : \ell_i] : \hat{p}_i \mid \{\hat{p}_0, \dots, \hat{p}_{n-1}\} \tag{memory shapes}
\end{align*}
$$

<caption>Fig. 9. Memory contents and shapes.</caption>

from Fig. 5c. Expressions are in A-normal form: every value is let-bound to a variable. Programs manipulate ADT values through *pattern matching* to destruct values, and *value-building expressions* to construct values according to a given memory layout.

A pattern-matching expression contains a list of *cases* of the form $p \to e$, each consisting of a provenance on the left-hand side and an expression on the right-hand side. Note that provenances contain no variables. In some of our examples, we will use *or-patterns* such as $p_1 | p_2 \to e$.

*Value expressions*, denoted *u*, allow to define values with reference to other already-bound values, using accessors of the form *x*.π. Such accessors designate subterms at position π within an existing value bound to *x*.

*Example 3.5 (Valueexpression)*. The valueexpression *u* = *Jal*(*x*.Jal.0, 42) builds a *jal* instruc-
tion using the same destination register as another *jal* instruction bound to *x*, and the con-
stant immediate 42. Note that focusing on a valueexpr does *not* evaluate accessors: we have
**focus** (*Jal*.0, *u*) = *x*.Jal.0.

Δ

*Example 3.6 (RISC-V destination register binding)*. The following program extracts the destination register of a RISC-V instruction if it exists, and returns *X*₀ otherwise:

$$
\text{get\_dest}(x : \tau_{\text{RISC-V}} \text{ as } \hat{\tau}_{\text{RISC-V}}) : \tau_{\text{reg}} \text{ as } \hat{\tau}_{\text{reg}} = \text{match}(x) \quad \begin{array}{@{}c@{}} \left\{ \begin{array}{@{}l@{}} \text{Add}(..., ..., ...) \rightarrow x.\text{Add}.0 \\ \text{Addi}(..., ..., ...) \rightarrow x.\text{Addi}.0 \\ \text{Jal}(..., ...) \rightarrow x.\text{Jal}.0 \\ \text{Sw}(..., ..., ...) \rightarrow X_0 \end{array} \right\} \\ \Delta \end{array}
$$

**3.4 Memory Model**

We model memory contents with values and stores, defined in Fig. 7. Memory values, denoted $\hat{v}$, follow roughly the same syntax as layouts, excluding constructs that do not relate to concrete memory contents (integer encodings, fragments and splits). The main difference is that pointers do not directly contain the pointee memory value, but refer to it with an address *a*. Interpretation of memory values therefore relies on a store, denoted $\zeta$, which maps addresses to memory values.

*Example 3.7 (RISC-V memory values)*. Consider the high-level value *v* = *Sw*(*X*₂, *X*₂, 3), of type *τ*<sub>RISC-V</sub>. The memory value representing *X*₂ according to *τ*<sub>reg</sub> is (2)₅. We can similarly follow the layout *τ*<sub>RISC-V</sub> to represent *v*, by instantiating each split, fragment and non-constant integer with *v* contents, and get the following memory value (which corresponds to the “assembled” version of
<figure><img src="image_5.png" /><figcaption>Fig. 10. Translation from layouts to shapes in type environment $\Delta: TyVars \to \widetilde{Types}$</figcaption></figure>

the instruction):

$$ \hat{v} = \begin{aligned}[t] & -32 \llbracket 0 : 7 \rbracket : (\theta \times 23)_7 \llbracket 7 : 5 \rbracket : (3)_5 \llbracket 12 : 3 \rbracket : (2)_3 \llbracket 15 : 5 \rbracket : (2)_5 \\ & \qquad \llbracket 20 : 5 \rbracket : (2)_5 \llbracket 25 : 7 \rbracket : (0)_7 \end{aligned} \quad \Delta $$

*Memory shapes.* Finally, we formalize the notion of a memory value “fitting” a given layout with *memory shapes*, denoted $\hat{p}$ and defined in Fig. 9. A shape exactly describes the “concrete” part of a memory type. The function **shape_of** in Fig. 10 is a conservative, best-effort translation from memory layouts to shapes used to gather static knowledge about memory layout. It uses a notion of size, which is defined in Appendix A. Here, the shape of a split is an opaque word large enough to contain any of its branches. However, a more precise definition is also possible, and even desirable, as we will see later.

*Example 3.8 (Shapes for RISC-V).* The shape of the layout used for RISC-V instructions in our running example (Example 3.2), considered in an empty type environment, depends on the size of each split branch. The layout in each of these branches is a composite word based on a 32-bit opaque word, hence $|\hat{\tau}_{Add}| = |\hat{\tau}_{Addi}| = |\hat{\tau}_{Jal}| = |\hat{\tau}_{Sw}|$ and **shape_of**($\hat{\tau}_{RISC-V}$) = $-32$. Similarly, we have **shape_of**($\hat{\tau}_{reg}$) = $-5$. The shape of the layout used for *sw* instructions follows its composite word structure and includes all of its fixed immediates:

$$ \mathbf{shape\_of}(\hat{\tau}_{\mathrm{Sw}}) = \begin{aligned}[t] & -32 \llbracket 0 : 7 \rbracket : (\theta \times 23)_7 \llbracket 7 : 5 \rbracket : -5 \llbracket 12 : 3 \rbracket : (2)_3 \llbracket 15 : 5 \rbracket : -5 \\ & \qquad \llbracket 20 : 5 \rbracket : -5 \llbracket 25 : 7 \rbracket : -7 \end{aligned} \quad \Delta $$

# 4 TARGET IN DESTINATION PASSING STYLE

Before formally defining our target intermediate representation, let us illustrate it on a first example.

*Example 4.1 (Target IR for RISC-V destination register binding).* The program from Example 3.6 reads from an input location $x_{in}$ representing a high-level value of type $\tau_{RISC-V}$ using the layout $\hat{\tau}_{RISC-V}$, and writes its result of type $\tau_{reg}$ to an output location $x_{out}$ using the layout $\hat{\tau}_{reg}$. Its compiled
<figure><img src="image_6.png" /><figcaption>Fig. 10. Translation from layouts to shapes in type environment $\Delta: TyVars \rightarrow \widetilde{Types}$</figcaption></figure>

the instruction):

$$ \hat{v} = _{-32} \bowtie [0 : 7] : (\theta \times 23)_7 \bowtie [7 : 5] : (3)_5 \bowtie [12 : 3] : (2)_3 \bowtie [15 : 5] : (2)_5 \\ \qquad \bowtie [20 : 5] : (2)_5 \bowtie [25 : 7] : (0)_7 \qquad \Delta $$

*Memory shapes.* Finally, we formalize the notion of a memory value “fitting” a given layout with *memory shapes*, denoted $\hat{p}$ and defined in Fig. 9. A shape exactly describes the “concrete” part of a memory type. The function **shape_of** in Fig. 10 is a conservative, best-effort translation from memory layouts to shapes used to gather static knowledge about memory layout. It uses a notion of size, which is defined in Appendix A. Here, the shape of a split is an opaque word large enough to contain any of its branches. However, a more precise definition is also possible, and even desirable, as we will see later.

*Example 3.8 (Shapes for RISC-V).* The shape of the layout used for RISC-V instructions in our running example (Example 3.2), considered in an empty type environment, depends on the size of each split branch. The layout in each of these branches is a composite word based on a 32-bit opaque word, hence $|\hat{\tau}_{Add}| = |\hat{\tau}_{Addi}| = |\hat{\tau}_{Jal}| = |\hat{\tau}_{Sw}|$ and **shape_of**($\hat{\tau}_{RISC-V}$) = _-32. Similarly, we have **shape_of**($\hat{\tau}_{reg}$) = _-5. The shape of the layout used for *sw* instructions follows its composite word structure and includes all of its fixed immediates:

$$ \mathbf{shape\_of}(\hat{\tau}_{\text{Sw}}) = _{-32} \bowtie [0 : 7] : (\theta \times 23)_7 \bowtie [7 : 5] : _{-5} \bowtie [12 : 3] : (2)_3 \bowtie [15 : 5] : _{-5} \\ \qquad \bowtie [20 : 5] : _{-5} \bowtie [25 : 7] : _{-7} \qquad \Delta $$

# 4 TARGET IN DESTINATION PASSING STYLE

Before formally defining our target intermediate representation, let us illustrate it on a first example.

*Example 4.1 (Target IR for RISC-V destination register binding).* The program from Example 3.6 reads from an input location $x_{in}$ representing a high-level value of type $\tau_{RISC-V}$ using the layout $\hat{\tau}_{RISC-V}$, and writes its result of type $\tau_{reg}$ to an output location $x_{out}$ using the layout $\hat{\tau}_{reg}$. Its compiled
**Data:** $x_1, \dots, x_n$ the input locations

**Data:** $\hat{\tau}_1, \dots, \hat{\tau}_n \in \overline{\text{Types}}$ the input memory layouts

**Data:** $m = \{p_{i,1}, \dots, p_{i,n} \to \mathcal{E}_i \mid 1 \le i \le N\}$ a matching problem whose branches map provenances to target expressions

**Result:** Target code corresponding to the decision DAG computed by Baudon et al. [2023]

1 function `DESTRUCT`((x₁: $\hat{\tau}_1$, . . ., xₙ: $\hat{\tau}_n$), m) : $\mathcal{E}$

**Algorithm 1:** `DESTRUCT` interface.

`alloc(l)`. This memory is then filled using write instructions, with several kinds of contents: constants denoted `c`, the contents of an input location, or the address of newly allocated memory of a given size denoted `&alloc(l)`.

Traditional control flow relies on the `switch` construct with a default branch marked by `"_"`, along with `success` and `fail` return statements which do not return any value.

Finally, in the context of `RIBBIT`, switching on a location reveals information about values, notably details about their concrete shapes. To materialize this in the IR, we introduce `cast` instructions which refine the shape of a given output location to a more precise shape.

In the rest of this article, target expressions will be displayed with a **plain frame** around them. Let us finally point out that sharing is not explicit in the IR, even though we use a control-flow-graph style representation underneath.

*Example 4.2 (Target IR on a program with lists)*. Using the memory type defined in Example 3.3, the following function captures and returns the first element of a list, 0 if empty.

$$ \text{get\_value}(x : \tau \text{ as } \tau_p) : I_{32} = \text{match}(x) \begin{cases} \text{Nil} & \to 0_{(32)} \\ \text{Cons}(\_, \_) & \to x.\text{Cons}.0 \end{cases} $$

will be compiled as:

$$ \text{get\_value}(x_{\text{in}} : \hat{\tau}_p, x_{\text{out}} : I_{32}) = \left[ \begin{array}{l} \text{let}_{\text{in}} x = x_{\text{in}}.[0:2]; \\ \text{switch}(x) \begin{cases} 0 \to x_{\text{out}} := 0; & \text{success} \\ 1 \to \text{let}_{\text{in}} x' = x_{\text{in}}.[2:32]; & x_{\text{out}} := x'; \text{ success} \\ 2 \to \text{let}_{\text{in}} x' = x_{\text{in}}.*.0; & x_{\text{out}} := x'; \text{ success} \end{cases} \end{array} \right. \Delta $$

# 5 COMPILATION OF DESTRUCTORS: A PRIMER

Looking at the compilation of our expression language described in Section 3.3, one important task is to compile pattern matching. This is a well-studied topic [Maranget 2008; Sestoft 1996] with several general procedures which take as input a list of patterns – usually with no variables nor right-hand-side expressions – and produce a nest of “switch” nodes, either following an automaton or a DAG. In the context of customizable memory layouts like the ones we consider, Baudon et al. [2023] provides a layout-aware compilation procedure emitting decision DAGs. As our goal is to consider such a compilation procedure in a full language, we will reuse their compilation algorithm, which already accommodates nested provenances.

The `DESTRUCT` algorithm, whose interface is described in Algorithm 1, takes as argument an input location to inspect, its memory type, and a matching problem. It emits code that inspects the *memory representation* of the value at the given memory location, to determine which provenance in the list, if any, matches the *original high-level value*. As a side effect, it also copies the right-hand side expressions of the pattern matching problem.
**Data:** $x_1, \dots, x_n$ the input locations

**Data:** $\hat{\tau}_1, \dots, \hat{\tau}_n \in \overline{\text{Types}}$ the input memory layouts

**Data:** $m = \{p_{i,1}, \dots, p_{i,n} \to \mathcal{E}_i \mid 1 \le i \le N\}$ a matching problem whose branches map provenances to target expressions

**Result:** Target code corresponding to the decision DAG computed by Baudon et al. [2023]

1 function `DESTRUCT`((x₁: $\hat{\tau}_1$, . . . , xₙ: $\hat{\tau}_n$), m) : $\mathcal{E}$

**Algorithm 1:** `DESTRUCT` interface.

`alloc(l)`. This memory is then filled using write instructions, with several kinds of contents: constants denoted `c`, the contents of an input location, or the address of newly allocated memory of a given size denoted `&alloc(l)`.

Traditional control flow relies on the `switch` construct with a default branch marked by `"_"`, along with `success` and `fail` return statements which do not return any value.

Finally, in the context of `RIBBIT`, switching on a location reveals information about values, notably details about their concrete shapes. To materialize this in the IR, we introduce `cast` instructions which refine the shape of a given output location to a more precise shape.

In the rest of this article, target expressions will be displayed with a **plain frame** around them. Let us finally point out that sharing is not explicit in the IR, even though we use a control-flow-graph style representation underneath.

*Example 4.2 (Target IR on a program with lists)*. Using the memory type defined in Example 3.3, the following function captures and returns the first element of a list, 0 if empty.

$$ \text{get\_value}(x : \tau \text{ as } \tau_p) : I_{32} = \text{match}(x) \begin{cases} \text{Nil} & \to 0_{(32)} \\ \text{Cons}(\_, \_) & \to x.\text{Cons}.0 \end{cases} $$

will be compiled as:

$$ \text{get\_value}(x_{\text{in}} : \hat{\tau}_p, x_{\text{out}} : I_{32}) = \left[ \begin{array}{l} \text{let}_{\text{in}} x = x_{\text{in}}.[0:2]; \\ \text{switch}(x) \begin{cases} 0 \to x_{\text{out}} := 0; & \text{success} \\ 1 \to \text{let}_{\text{in}} x' = x_{\text{in}}.[2:32]; & x_{\text{out}} := x'; \text{ success} \\ 2 \to \text{let}_{\text{in}} x' = x_{\text{in}}.*.0; & x_{\text{out}} := x'; \text{ success} \end{cases} \end{array} \right. \Delta $$

# 5 COMPILATION OF DESTRUCTORS: A PRIMER

Looking at the compilation of our expression language described in Section 3.3, one important task is to compile pattern matching. This is a well-studied topic [Maranget 2008; Sestoft 1996] with several general procedures which take as input a list of patterns – usually with no variables nor right-hand-side expressions – and produce a nest of “switch” nodes, either following an automaton or a DAG. In the context of customizable memory layouts like the ones we consider, Baudon et al. [2023] provides a layout-aware compilation procedure emitting decision DAGs. As our goal is to consider such a compilation procedure in a full language, we will reuse their compilation algorithm, which already accommodates nested provenances.

The `DESTRUCT` algorithm, whose interface is described in Algorithm 1, takes as argument an input location to inspect, its memory type, and a matching problem. It emits code that inspects the *memory representation* of the value at the given memory location, to determine which provenance in the list, if any, matches the *original high-level value*. As a side effect, it also copies the right-hand side expressions of the pattern matching problem.
**Example 5.1 (Matching Compilation for lists).** We consider the “matching part” of the function defined in Example 4.2, on which we apply DESTRUCT:

$$ \texttt{DESTRUCT}((x : \hat{\tau}_p), \left\{ \begin{array}{l} \texttt{Nil} \\ \texttt{Cons}(_ , _ ) \end{array} \right\} \Rightarrow \mathcal{E}_1 \Rightarrow \mathcal{E}_2) = \left[ \texttt{let}_{\texttt{in}} x' = x.[0 : 2]; \texttt{switch}(x') \left\{ \begin{array}{l} 0 \rightarrow \mathcal{E}_1 \\ 1 \rightarrow \mathcal{E}_2 \\ 2 \rightarrow \mathcal{E}_2 \end{array} \right\} \right] \Delta $$

*Some remarks about our adaptation.* We adapt the original algorithm in the following ways. The original algorithm emits decision trees, whose translation to our target IR is straightforward (it is sufficient to bind intermediate input locations for switches). DESTRUCT takes a list of provenances with their target expressions $\mathcal{E}$, which are placed at the leaves of the decision tree. The original algorithm by Baudon et al. [2023] attempts to handle binders in patterns, albeit in an incomplete way. We ignore this aspect, and will instead handle memory accesses in a more general way.

# 6 COMPILATION OF PATHS: A FIRST ATTEMPT

Considering compilation of our input language, another thorny construction remains: value-expressions, which combine constructors, variables, and path-based accessors. We now make a first (unsuccessful, as we will see) attempt at a simple compilation procedure for path-based accessors, and take this opportunity to introduce some tooling required for the full compilation procedure.

## 6.1 Exploring Layouts with Focus and Specialise

To compile high-level expressions in a way that fits a given memory layout, we need a way to explore both a type and its layout conjointly. Indeed, the full inner structure is only revealed when considering both the type, which defines nested terms and subterms, and the layout, which describes the exact operations required to access those subterms, represented as fragments. Let us consider a simple example demonstrating this idea.

**Example 6.1 (Branch-dependent layout on the list example).** Following our list example from Example 3.3, consider the following pattern matching branch: $\text{Cons}(_ , _ ) \rightarrow \dots x.\text{Cons}.0 \dots$.

How to compile the accessor $x.\text{Cons}.0$ to a memory access? This requires locating the associated fragment in the memory layout $\hat{\tau}_p$. However, the location of this fragment depends on other values in memory because of a split in $\hat{\tau}_p$. We thus need to explore several possibilities, indexed by various provenances of $x$. For instance, if $x$ matches $\text{Cons}(_ , \text{Nil})$, it will be at position $x.[2 : 32]$ in memory. If $x$ matches $\text{Cons}(_ , \text{Cons}(_ , _))$ however, it will be at position $x. * .0$ in memory. This distinction between provenances will appear in our generated code, as shown in Example 4.2. $\Delta$

The **Explore** function defined in this section takes as input an already-known provenance $p$, a type $\tau$ and a layout $\hat{\tau}$, and returns the list of branches, i.e. possible versions of $\tau$ represented as $\hat{\tau}$ which are “compatible” with $p$. Semantically, a branch characterises the parts of $\tau$ that match the provenance $p$. A branch is thus defined as quadruplet $(p_i, \tau_i, \hat{\tau}_i, \text{frags}_i)$ consisting of the provenance, type and layout refined for that specific branch, and of a list of fragments contained therein.

**Example 6.2 (Explore the list type (Example 3.3)).** We can explore $\hat{\tau}_p$ with the provenance $\text{Cons}(_ , _)$:

$$ \textbf{Explore}(\text{Cons}(_ , _), \tau_{\text{list}}, \hat{\tau}_p) = \left\{ \begin{array}{l} (\text{Cons}(_ , \text{Nil}) , \text{Cons}(I_{32}, \text{Nil}) , \hat{\tau}_{C1}, F_1) \\ (\text{Cons}(_ , \text{Cons}(_ , _)) , \text{Cons}(I_{32}, \text{Cons}(I_{32}, \tau_{\text{list}})) , \hat{\tau}_{C2}, F_2) \end{array} \right\} $$

$$ \text{where } F_1 = [ .[2 : 32] \mapsto (.\text{Cons}.0 \text{ as } I_{32}) ] \text{ and } F_2 = [ . * .0 \mapsto (.\text{Cons}.0 \text{ as } I_{32}) \\ . * .1 \mapsto (.\text{Cons}.1.\text{Cons}.0 \text{ as } I_{32}) \\ . * .2 \mapsto (.\text{Cons}.1.\text{Cons}.1 \text{ as } \hat{\tau}_p) ] $$

Note that the types and layouts of branches are *refined* according to their provenance. $\Delta$

To precisely define **Explore**, we need a new operation to refine layouts: specialisation.
**Example 5.1 (Matching Compilation for lists).** We consider the “matching part” of the function defined in Example 4.2, on which we apply DESTRUCT:

$$ \text{DESTRUCT}((x : \hat{\tau}_p), \left\{ \begin{array}{rcl} \text{Nil} & \Rightarrow & \mathcal{E}_1 \\ \text{Cons}(..., ...) & \Rightarrow & \mathcal{E}_2 \end{array} \right\}) = \left[ \text{let}_\text{in } x' = x.[0:2]; \text{switch}(x') \left\{ \begin{array}{rcl} 0 & \Rightarrow & \mathcal{E}_1 \\ 1 & \Rightarrow & \mathcal{E}_2 \\ 2 & \Rightarrow & \mathcal{E}_2 \end{array} \right\} \right] \Delta $$

*Some remarks about our adaptation.* We adapt the original algorithm in the following ways. The original algorithm emits decision trees, whose translation to our target IR is straightforward (it is sufficient to bind intermediate input locations for switches). DESTRUCT takes a list of provenances with their target expressions $\mathcal{E}$, which are placed at the leaves of the decision tree. The original algorithm by Baudon et al. [2023] attempts to handle binders in patterns, albeit in an incomplete way. We ignore this aspect, and will instead handle memory accesses in a more general way.

# 6 COMPILATION OF PATHS: A FIRST ATTEMPT

Considering compilation of our input language, another thorny construction remains: value-expressions, which combine constructors, variables, and path-based accessors. We now make a first (unsuccessful, as we will see) attempt at a simple compilation procedure for path-based accessors, and take this opportunity to introduce some tooling required for the full compilation procedure.

## 6.1 Exploring Layouts with Focus and Specialise

To compile high-level expressions in a way that fits a given memory layout, we need a way to explore both a type and its layout conjointly. Indeed, the full inner structure is only revealed when considering both the type, which defines nested terms and subterms, and the layout, which describes the exact operations required to access those subterms, represented as fragments. Let us consider a simple example demonstrating this idea.

**Example 6.1 (Branch-dependent layout on the list example).** Following our list example from Example 3.3, consider the following pattern matching branch: $\text{Cons}(..., ...) \rightarrow \dots x.\text{Cons}.0\dots$.

How to compile the accessor $x.\text{Cons}.0$ to a memory access? This requires locating the associated fragment in the memory layout $\hat{\tau}_p$. However, the location of this fragment depends on other values in memory because of a split in $\hat{\tau}_p$. We thus need to explore several possibilities, indexed by various provenances of $x$. For instance, if $x$ matches $\text{Cons}(..., \text{Nil})$, it will be at position $x.[2:32]$ in memory. If $x$ matches $\text{Cons}(..., \text{Cons}(..., ...))$ however, it will be at position $x.\ast.0$ in memory. This distinction between provenances will appear in our generated code, as shown in Example 4.2. $\Delta$

The **Explore** function defined in this section takes as input an already-known provenance $p$, a type $\tau$ and a layout $\hat{\tau}$, and returns the list of branches, i.e. possible versions of $\tau$ represented as $\hat{\tau}$ which are “compatible” with $p$. Semantically, a branch characterises the parts of $\tau$ that match the provenance $p$. A branch is thus defined as quadruplet $(p_i, \tau_i, \hat{\tau}_i, \text{frags}_i)$ consisting of the provenance, type and layout refined for that specific branch, and of a list of fragments contained therein.

**Example 6.2 (Explore the list type (Example 3.3)).** We can explore $\hat{\tau}_p$ with the provenance $\text{Cons}(..., ...)$:

$$ \text{Explore}(\text{Cons}(..., ...), \tau_{\text{list}}, \hat{\tau}_p) = \left\{ \begin{array}{l} \left( \text{Cons}(..., \text{Nil}), \text{Cons}(I_{32}, \text{Nil}), \dots, \hat{\tau}_{C1}, F_1 \right) \\ \left( \text{Cons}(..., \text{Cons}(..., ...)), \text{Cons}(I_{32}, \text{Cons}(I_{32}, \tau_{\text{list}})), \hat{\tau}_{C2}, F_2 \right) \end{array} \right\} \\ \text{where } F_1 = [ ...[2:32] \mapsto (.\text{Cons}.0 \text{ as } I_{32}) ] \text{ and } F_2 = [ \begin{array}{l} \ast.0 \mapsto (.\text{Cons}.0 \text{ as } I_{32}) \\ \ast.1 \mapsto (.\text{Cons}.1.\text{Cons}.0 \text{ as } I_{32}) \\ \ast.2 \mapsto (.\text{Cons}.1.\text{Cons}.1 \text{ as } \hat{\tau}_p) \end{array} ] $$

Note that the types and layouts of branches are *refined* according to their provenance. $\Delta$

To precisely define **Explore**, we need a new operation to refine layouts: specialisation.
1 function **Explore**($p_0 \in Provs, \tau_0 \in Types, \hat{\tau}_0 \in \overline{Types}$):

2 for ($p, \hat{\tau}$) $\in \hat{\tau}_0/p_0$ do

3 $\tau \leftarrow \tau_0/p$
4 fragments $\leftarrow \{(\hat{\pi} \mapsto \pi \text{ as } \hat{\tau}) \mid \textbf{focus} (\hat{\pi}, \hat{\tau}) = (\pi \text{ as } \hat{\tau'})\}$

5 **yield** ($p, \tau, \hat{\tau}, \text{frags}$)

**Algorithm 2: Explore.**

*Layout Specialisation.* Similar to type specialisation, layout specialisation, denoted $\hat{\tau}/p$, filters a layout $\hat{\tau}$ to exclude parts which are incompatible with a given provenance $p$. It removes all splits from $\hat{\tau}$ (up to fragments) by filtering out branches whose provenance set excludes $p$. It returns a list of pairs of the form $(p', \hat{\tau}')$, where $p'$ is a refined version of $p$ and $\hat{\tau}'$ is the restriction of $\hat{\tau}$ to values that match $p'$. We demonstrate it on an example, the full definition is in Appendix A, Fig. 14.

*Example 6.3 (Layout specialisation).* For instance:

$$ \hat{\tau}_p / \text{Cons}(\_, \_) = \left\{ \begin{array}{l} \text{Cons}(\_, \text{Nil}), \_64 \bowtie [0:2] = 1 \bowtie [2:32] : (\text{Cons}.0 \text{ as } I_{32}) \\ (\text{Cons}(\_, \text{Cons}(\_, \_)), \_64 \dots \bowtie [0:2] = 2 \end{array} \right\} \Delta $$

*Explore.* We are now ready to properly define **Explore**, in Algorithm 2. Given an initial provenance $p_0$, type $\tau_0$ and layout $\hat{\tau}_0$, it returns the list of all branches of $\hat{\tau}_0$ that represent $\tau_0$ values matching $p_0$. **Explore**, and many of the algorithms described in this article, uses Python-style generators using the “yield” keyword, and “for-each” style loops.

Using the specialisation $\hat{\tau}_0/p_0$, we gather all refinements pairs of $\hat{\tau}_0$ compatible with $p_0$. Each pair consists of a more precise provenance $p$ and a specialised layout $\hat{\tau}$. We then derive all information relevant to this case from $p$ and $\hat{\tau}$: the refined type $\tau_0/p$, and a list of the form $(\hat{\pi}' \mapsto \pi'$ as $\hat{\tau}')$ containing every position $\hat{\pi}'$ such that $\hat{\tau}$ contains a fragment at $\hat{\pi}'$. From these results, we construct a branch.

## 6.2 A Naive Compilation Algorithm for Accessors

An intuitive idea to compile accessors would be to find “the right memory path” corresponding to a given high-level path. It would proceed as follows: given a variable $x$, its type $\tau$, layout $\hat{\tau}$, and a path-based accessor $x.\pi$, we can explore all branches of $\hat{\tau}$ and for each possible layout, return the memory path that leads to a fragment corresponding to the high-level path $\pi$.

The **EXTRACT** procedure, defined in Algorithm 3, implements this idea. It takes a description $(x, \tau, \hat{\tau}, p \triangleleft f : \text{as } o)$ the input value, an output location $y$ and a path $\pi$. It emits code to store in $y$ the representation of the subterm located at $\pi$ within the input value. Here, we are looking for “the right memory path”, as such, there should exist a fragment within $\hat{\tau}$ that exactly corresponds to the (high-level) subterm $\pi$. All we have to do now is to find where.

* In the base case (Line 2), if $\pi = \epsilon$, then we simply copy input contents into the output location.

* As we have seen, the location of the fragment might depend on other parts of the layout, hence the need for **Explore**. For this purpose, we gather all branches (Line 5) and generate code that dynamically determines the appropriate branch by inspecting the input value. We can readily reuse the pattern matching compilation algorithm **DESTRUCT** for this purpose (Line 12).

* For each branch of the input layout, we round up all fragments that appear in its layout and their positions, then focus into the one that represents a parent of the target subterm $(\pi_f \le \pi)$ (Line 8) to recursively look for $\pi$ (Line 9).

* If no such fragment exists, we fail.

*Example 6.4 (EXTRACT on the list example– Algorithm 3).* Let us consider again the first integer element of a (non empty) list, at position .Cons.0. Let $x_{\text{out}}$ a fresh output location and $x$ an input location
1 function **Explore**($p_0 \in Provs, \tau_0 \in Types, \hat{\tau}_0 \in \overline{Types}$):

2 for ($p, \hat{\tau}$) $\in \hat{\tau}_0/p_0$ do

3 $\tau \leftarrow \tau_0/p$
4 fragments $\leftarrow \{ (\hat{\pi} \mapsto \pi \text{ as } \hat{\tau}) \mid \textbf{focus} (\hat{\pi}, \hat{\tau}) = (\pi \text{ as } \hat{\tau}) \}$

5 **yield** ($p, \tau, \hat{\tau}, \text{frags}$)

**Algorithm 2: Explore.**

*Layout Specialisation.* Similar to type specialisation, layout specialisation, denoted $\hat{\tau}/p$, filters a layout $\hat{\tau}$ to exclude parts which are incompatible with a given provenance $p$. It removes all splits from $\hat{\tau}$ (up to fragments) by filtering out branches whose provenance set excludes $p$. It returns a list of pairs of the form $(p', \hat{\tau}')$, where $p'$ is a refined version of $p$ and $\hat{\tau}'$ is the restriction of $\hat{\tau}$ to values that match $p'$. We demonstrate it on an example, the full definition is in Appendix A, Fig. 14.

*Example 6.3 (Layout specialisation).* For instance:

$$ \hat{\tau}_p / \text{Cons}(\_, \_) = \left\{ \begin{array}{@{}l@{}} \text{Cons}(\_, \text{Nil}), \_64 \bowtie [0:2] = 1 \bowtie [2:32] : (\text{Cons}.0 \text{ as } I_{32}) \\ (\text{Cons}(\_, \text{Cons}(\_, \_)), \_64 \dots \bowtie [0:2] = 2 \end{array} \right\} \Delta $$

*Explore.* We are now ready to properly define **Explore**, in Algorithm 2. Given an initial provenance $p_0$, type $\tau_0$ and layout $\hat{\tau}_0$, it returns the list of all branches of $\hat{\tau}_0$ that represent $\tau_0$ values matching $p_0$. **Explore**, and many of the algorithms described in this article, uses Python-style generators using the “yield” keyword, and “for-each” style loops.

Using the specialisation $\hat{\tau}_0/p_0$, we gather all refinements pairs of $\hat{\tau}_0$ compatible with $p_0$. Each pair consists of a more precise provenance $p$ and a specialised layout $\hat{\tau}$. We then derive all information relevant to this case from $p$ and $\hat{\tau}$: the refined type $\tau_0/p$, and a list of the form $(\hat{\pi}' \mapsto \pi'$ as $\hat{\tau}')$ containing every position $\hat{\pi}'$ such that $\hat{\tau}$ contains a fragment at $\hat{\pi}'$. From these results, we construct a branch.

## 6.2 A Naive Compilation Algorithm for Accessors

An intuitive idea to compile accessors would be to find “the right memory path” corresponding to a given high-level path. It would proceed as follows: given a variable $x$, its type $\tau$, layout $\hat{\tau}$, and a path-based accessor $x.\pi$, we can explore all branches of $\hat{\tau}$ and for each possible layout, return the memory path that leads to a fragment corresponding to the high-level path $\pi$.

The **EXTRACT** procedure, defined in Algorithm 3, implements this idea. It takes a description $(x, \tau, \hat{\tau}, p \triangleleft f : \text{as } o)$ the input value, an output location $y$ and a path $\pi$. It emits code to store in $y$ the representation of the subterm located at $\pi$ within the input value. Here, we are looking for “the right memory path”, as such, there should exist a fragment within $\hat{\tau}$ that exactly corresponds to the (high-level) subterm $\pi$. All we have to do now is to find where.

* In the base case (Line 2), if $\pi = \epsilon$, then we simply copy input contents into the output location.

* As we have seen, the location of the fragment might depend on other parts of the layout, hence the need for **Explore**. For this purpose, we gather all branches (Line 5) and generate code that dynamically determines the appropriate branch by inspecting the input value. We can readily reuse the pattern matching compilation algorithm **DESTRUCT** for this purpose (Line 12).

* For each branch of the input layout, we round up all fragments that appear in its layout and their positions, then focus into the one that represents a parent of the target subterm $(\pi_f \le \pi)$ (Line 8) to recursively look for $\pi$ (Line 9).

* If no such fragment exists, we fail.

*Example 6.4 (EXTRACT on the list example– Algorithm 3).* Let us consider again the first integer element of a (non empty) list, at position .Cons.0. Let $x_{\text{out}}$ a fresh output location and $x$ an input location
**Data:** $(x \triangleleft p : \tau \text{ as } \hat{\tau})$ the input description

**Data:** $y$ the output location

**Data:** $\pi$ the path in the input to the desired value

**Result:** Code binding $y$ to the representation of the subterm at position $\pi$ in the input

1 function `EXTRACT((x \triangleleft p : \tau \text{ as } \hat{\tau}), y, \pi):`

2 if $\pi = \epsilon$ then

3 return $y := x; \text{ success}$

4 else

<figure><img src="image_6.png" /><figcaption>**Algorithm 3: EXTRACT:** Naive Path compilation algorithm.</figcaption></figure>

assumed to contain the representation of a Cons. `EXTRACT((x \triangleleft Cons($_, \_): \tau_{list}$ as $\hat{\tau}_p$), x_{out}, .Cons.0)` starts by exploring $\hat{\tau}_p$. Following Example 6.2, we have two branches:

* The first branch is `(Cons($_, \text{Nil}), \tau_{C1}, \hat{\tau}_{C1}, F_1)` where $F_1 = [.[2:32] \mapsto (.\text{Cons}.0 \text{ as } I_{32})]$. The fragment at `[2:32]` covers `.Cons.0`. We can now focus on it and proceed to the (first) recursive call. Let $x'$ a fresh symbol. By focusing, we obtain the recursive arguments $\tau' = \text{focus} (.\text{Cons}.0, \tau_{C1}) = I_{32}, p' = \_` and $\pi' = \epsilon$, leading to `EXTRACT((x' \triangleleft p' : \tau' \text{ as } I_{32}), x_{out}, \pi') = [x_{out} := x'; \text{ success}]$. We finally obtain $\mathcal{E}_1 = [\text{let}_{\text{in}} x' = x.[2:32]; y := x'; \text{ success}]$ and yield `(Cons($_, \text{Nil}), \mathcal{E}_1)`.

* The second branch is `(Cons($_, \text{Cons}($_, \_)), \tau_{C2}, \hat{\tau}_{C2}, F_2)` with `(. * .0 \mapsto .\text{Cons}.0 \text{ as } I_{32}) \in F_2`. We proceed similarly, with a recursive call to get a target expression $\mathcal{E}_2$, yielding the pair `(Cons($_, \text{Cons}($_, \_)), \mathcal{E}_2)`.

We finally emit the following code, which is coherent with Example 4.2:

`DESTRUCT((x_0 : \hat{\tau}_{\text{list}}), {(Cons($_, \text{Nil}) \mapsto \mathcal{E}_1), (Cons($_, \text{Cons}($_, \_)) \mapsto \mathcal{E}_2)}) =`

<figure><img src="image_7.png" /></figure>

To implement `EXTRACT`, we assumed that, once we have narrowed down the layout to a single branch, any given source path can be translated to a single memory path. While this is true for “simple” layouts, it is not the case in general. For instance, the immediate at `.Sw.2` in the RISC-V layout (Fig. 1d and Example 3.2) is broken into two pieces, which need to be assembled to get a whole integer. Similarly, the arithmetic expression (Fig. 5a) at position `.Plus.1` in the case `Plus($_, I($_))` doesn't even exist in memory anymore as only the inner integer is stored: we need to rebox it to get an expression. Finally, in our list example (Example 3.3), if we had to implement `tail`, we would have to reconstruct a new list from `Cons.1`, which does not exist either: `Nil` is implicit in the case `Cons($_, \text{Nil})` and the tail list is broken up in the pointed struct in the case `Cons($_, \text{Cons}($_, \_))`.
**Data:** $(x \triangleleft p : \tau \text{ as } \hat{\tau})$ the input description

**Data:** $y$ the output location

**Data:** $\pi$ the path in the input to the desired value

**Result:** Code binding $y$ to the representation of the subterm at position $\pi$ in the input

1 function `EXTRACT((x \triangleleft p : \tau \text{ as } \hat{\tau}), y, \pi):`

2 if $\pi = \epsilon$ then

3 return $y := x; \text{ success}$

4 else

<figure><img src="image_7.png" /><figcaption>**Algorithm 3: EXTRACT:** Naive Path compilation algorithm.</figcaption></figure>

assumed to contain the representation of a Cons. `EXTRACT((x \triangleleft Cons($_, \_): \tau_{list}$ as $\hat{\tau}_p$), x_{out}, .Cons.0)` starts by exploring $\hat{\tau}_p$. Following Example 6.2, we have two branches:

* The first branch is `(Cons($_, \text{Nil}), \tau_{C1}, \hat{\tau}_{C1}, F_1)` where $F_1 = [.[2:32] \mapsto (.\text{Cons}.0 \text{ as } I_{32})]$. The fragment at `[2:32]` covers `.Cons.0`. We can now focus on it and proceed to the (first) recursive call. Let $x'$ a fresh symbol. By focusing, we obtain the recursive arguments $\tau' = \text{focus} (.\text{Cons}.0, \tau_{C1}) = I_{32}, p' = \_` and $\pi' = \epsilon$, leading to `EXTRACT((x' \triangleleft p' : \tau' \text{ as } I_{32}), x_{out}, \pi') = [x_{out} := x'; \text{ success}]$. We finally obtain $\mathcal{E}_1 = [\text{let}_{\text{in}} x' = x.[2:32]; y := x'; \text{ success}]$ and yield `(Cons($_, \text{Nil}), \mathcal{E}_1)`.

* The second branch is `(Cons($_, \text{Cons}($_, \_)), \tau_{C2}, \hat{\tau}_{C2}, F_2)` with `(. * .0 \mapsto .\text{Cons}.0 \text{ as } I_{32}) \in F_2`. We proceed similarly, with a recursive call to get a target expression $\mathcal{E}_2$, yielding the pair `(Cons($_, \text{Cons}($_, \_)), \mathcal{E}_2)`.

We finally emit the following code, which is coherent with Example 4.2:

`DESTRUCT((x_0 : \hat{\tau}_{\text{list}}), {(Cons($_, \text{Nil}) \mapsto \mathcal{E}_1), (Cons($_, \text{Cons}($_, \_)) \mapsto \mathcal{E}_2)}) =`

<figure><img src="image_8.png" /></figure>

To implement `EXTRACT`, we assumed that, once we have narrowed down the layout to a single branch, any given source path can be translated to a single memory path. While this is true for “simple” layouts, it is not the case in general. For instance, the immediate at `.Sw.2` in the RISC-V layout (Fig. 1d and Example 3.2) is broken into two pieces, which need to be assembled to get a whole integer. Similarly, the arithmetic expression (Fig. 5a) at position `.Plus.1` in the case `Plus($_, I($_))` doesn't even exist in memory anymore as only the inner integer is stored: we need to rebox it to get an expression. Finally, in our list example (Example 3.3), if we had to implement `tail`, we would have to reconstruct a new list from `Cons.1`, which does not exist either: `Nil` is implicit in the case `Cons($_, \text{Nil})` and the tail list is broken up in the pointed struct in the case `Cons($_, \text{Cons}($_, \_))`.
Nevertheless, the **EXTRACT** procedure demonstrates how focusing, specialisation and **Explore** can be combined to design fairly complex compilation procedures. In fact, **EXTRACT** already subsumes the subset of binders handled by Baudon et al. [2023], in only 12 lines of code. We can now use these tools to develop a full compilation procedure for our language.

# 7 FULL COMPILATION

We are, at last, ready to present our main contribution: a general procedure, implemented into **RIBBIT**, which can compile both pattern matching and value-building expressions in a unified manner for arbitrary memory layouts. As we have seen, in the presence of complex layouts, it is necessary to destruct and reconstruct values, making it necessary to treat compilation of accessors and constructors conjointly. Before going any further, let us look at the toplevel compilation process for full expressions.

## 7.1 Compilation of Expressions

Our main compilation algorithm is presented in **Algorithm 4**. It takes as input a collection of binders $\Gamma$, an output triplet $(x_{\text{out}} : \tau_{\text{out}} \text{ as } \hat{\tau}_{\text{out}})$, and an expression $e$. $\Gamma$ contains binders of the form $(x \triangleleft p : \tau \text{ as } \hat{\tau})$ indicating that $x$ is an available input memory location which represents a value of type $\tau$ with the layout $\hat{\tau}$ and which is known to match the provenance $p$. In each case, **COMPILE** delegates emission of code for given tasks to several sub-procedures. First off, compilation of pattern matching is immediately delegated to **DESTRUCT**, as previously described in Section 5. The other procedures are described in the upcoming subsections, and comprise the following tasks:

* **SEEK** (Section 7.2) a path $\pi$ within the memory representation of its parent input value $x$ to produce a piece of data corresponding to the accessor $x.\pi$. **SEEK** extends **EXTRACT** to handle arbitrary memory layout combinations, including those where the desired subterm is broken into multiple pieces scattered over the parent representation.

* Assemble these pieces to **REBUILD** (Section 7.3) the representation of the valueexpression $u$.

* **REFINE** (Section 7.4) the contents of a memory location to allocate all necessary pieces and set constants.

* Finally, Section 7.6 describes how to ensure termination of our algorithm and emit recursive code when necessary.

## 7.2 Seek a path

**SEEK**, in **Algorithm 5**, compiles an accessor $x.\pi$ to target code. We consider the memory representation of the value bound to $x$ (which is already built and read-only at execution time) as the *input value* and identify it with the quadruple $(x_{\text{in}} \triangleleft p_{\text{in}} : \tau_{\text{in}} \text{ as } \hat{\tau}_{\text{in}})$, composed of its input location, type, layout and provenance respectively. That is, at execution time, $x_{\text{in}}$ is expected to contain the memory representation according to $\hat{\tau}_{\text{in}}$ of some value of type $\tau_{\text{in}}$ matching the provenance $p_{\text{in}}$. Similarly, we refer to the memory representation of the desired subterm (which is the piece of data currently being built) as the *output value* and identify it with the triple $(x_{\text{out}} : \tau_{\text{out}} \text{ as } \hat{\tau}_{\text{out}})$ composed of its output location, type and layout respectively. Our goal is to emit code that, given an input location $x_{\text{in}}$ containing the memory representation of $v$ following the layout $\hat{\tau}_{\text{in}}$ and an output location $x_{\text{out}}$, stores in $x_{\text{out}}$ the representation of **focus** $(\pi, v)$ following the layout $\hat{\tau}_{\text{out}}$.

**SEEK** is similar to the **EXTRACT** procedure presented in Section 6.2. The differences are highlighted in **orange**. As we have seen, there are some cases where there is no single fragment that covers the desired path. Alternatively, we might reach $\pi = \epsilon$, but $\hat{\tau}_{\text{in}} \neq \hat{\tau}_{\text{out}}$, indicating that we should exhibit an isomorphism between $\hat{\tau}_{\text{in}}$ and $\hat{\tau}_{\text{out}}$ to get the desired value. In both cases, we need to
Nevertheless, the **EXTRACT** procedure demonstrates how focusing, specialisation and **Explore** can be combined to design fairly complex compilation procedures. In fact, **EXTRACT** already subsumes the subset of binders handled by Baudon et al. [2023], in only 12 lines of code. We can now use these tools to develop a full compilation procedure for our language.

# 7 FULL COMPILATION

We are, at last, ready to present our main contribution: a general procedure, implemented into **RIBBIT**, which can compile both pattern matching and value-building expressions in a unified manner for arbitrary memory layouts. As we have seen, in the presence of complex layouts, it is necessary to destruct and reconstruct values, making it necessary to treat compilation of accessors and constructors conjointly. Before going any further, let us look at the toplevel compilation process for full expressions.

## 7.1 Compilation of Expressions

Our main compilation algorithm is presented in **Algorithm 4**. It takes as input a collection of binders $\Gamma$, an output triplet $(x_{\text{out}} : \tau_{\text{out}} \text{ as } \hat{\tau}_{\text{out}})$, and an expression $e$. $\Gamma$ contains binders of the form $(x \triangleleft p : \tau \text{ as } \hat{\tau})$ indicating that $x$ is an available input memory location which represents a value of type $\tau$ with the layout $\hat{\tau}$ and which is known to match the provenance $p$. In each case, **COMPILE** delegates emission of code for given tasks to several sub-procedures. First off, compilation of pattern matching is immediately delegated to **DESTRUCT**, as previously described in Section 5. The other procedures are described in the upcoming subsections, and comprise the following tasks:

* **SEEK** (Section 7.2) a path $\pi$ within the memory representation of its parent input value $x$ to produce a piece of data corresponding to the accessor $x.\pi$. **SEEK** extends **EXTRACT** to handle arbitrary memory layout combinations, including those where the desired subterm is broken into multiple pieces scattered over the parent representation.

* Assemble these pieces to **REBUILD** (Section 7.3) the representation of the valueexpression $u$.

* **REFINE** (Section 7.4) the contents of a memory location to allocate all necessary pieces and set constants.

* Finally, Section 7.6 describes how to ensure termination of our algorithm and emit recursive code when necessary.

## 7.2 Seek a path

**SEEK**, in **Algorithm 5**, compiles an accessor $x.\pi$ to target code. We consider the memory representation of the value bound to $x$ (which is already built and read-only at execution time) as the *input value* and identify it with the quadruple $(x_{\text{in}} \triangleleft p_{\text{in}} : \tau_{\text{in}} \text{ as } \hat{\tau}_{\text{in}})$, composed of its input location, type, layout and provenance respectively. That is, at execution time, $x_{\text{in}}$ is expected to contain the memory representation according to $\hat{\tau}_{\text{in}}$ of some value of type $\tau_{\text{in}}$ matching the provenance $p_{\text{in}}$. Similarly, we refer to the memory representation of the desired subterm (which is the piece of data currently being built) as the *output value* and identify it with the triple $(x_{\text{out}} : \tau_{\text{out}} \text{ as } \hat{\tau}_{\text{out}})$ composed of its output location, type and layout respectively. Our goal is to emit code that, given an input location $x_{\text{in}}$ containing the memory representation of $v$ following the layout $\hat{\tau}_{\text{in}}$ and an output location $x_{\text{out}}$, stores in $x_{\text{out}}$ the representation of **focus** $(\pi, v)$ following the layout $\hat{\tau}_{\text{out}}$.

**SEEK** is similar to the **EXTRACT** procedure presented in Section 6.2. The differences are highlighted in **orange**. As we have seen, there are some cases where there is no single fragment that covers the desired path. Alternatively, we might reach $\pi = \epsilon$, but $\hat{\tau}_{\text{in}} \neq \hat{\tau}_{\text{out}}$, indicating that we should exhibit an isomorphism between $\hat{\tau}_{\text{in}}$ and $\hat{\tau}_{\text{out}}$ to get the desired value. In both cases, we need to
**Data:** $\Gamma = (x_i \triangleleft p_i : \tau_i \text{ as } \hat{\tau}_i)_{0 \le i < n}$ a set of input descriptions

**Data:** *e* the input expression

**Data:** $(x_{\text{out}} : \tau_{\text{out}} \text{ as } \hat{\tau}_{\text{out}})$ the output description

**Result:** Code computing the value of the expression *e*

**function COMPILE(Γ, (x_{out} : τ_{out} as $\hat{\tau}_{out}$), e) = case(e){**

$$
\begin{array}{rcl}
\text{match}(y) \{ & & \text{ Delegate pattern matching compilation to DESTRUCT (Section 5)} \\
& p_i \to e_i \mid (0 \le i < n) & \to \\
\} & & \quad (y \triangleleft p : \tau \text{ as } \hat{\tau}) \in \Gamma \\
& & \quad \forall i. \mathcal{E}_i \leftarrow \text{COMPILE}(\Gamma, (x_{\text{out}} : \tau_{\text{out}} \text{ as } \hat{\tau}_{\text{out}}), e_i) \\
& & \quad \text{DESTRUCT}((y : \hat{\tau}), \{p_i \to \mathcal{E}_i \mid 1 \le i \le n\})
\end{array}
$$

$$
y.\pi \quad \rightarrow \quad \text{SEEK}(\Gamma(y), (x_{\text{out}} : \tau_{\text{out}} \text{ as } \hat{\tau}_{\text{out}}), \pi) \quad \text{// SEEK the path } \pi \text{ in } y \text{ (Section 7.2)}
$$

$$
u \rightarrow \begin{array}{@{}l@{}}
\text{REBUILD}(\Gamma, (x_{\text{out}} : \tau_{\text{out}} \text{ as } \hat{\tau}_{\text{out}}), u) \text{ // REBUILD constructor } u \text{ (Section 7.3)} \\
\text{ } y_{\text{out}} \text{ fresh.}
\end{array}
$$

$$
\[
\left.
\begin{array}{@{}l@{}}
  \text{ // Allocate new memory location for } e_1 \text{ with REFINE (Section 7.4)} \\
  \text{let}_{\text{out}} y_{\text{out}} = \text{alloc}(|\hat{\tau}|); \text{REFINE}(y_{\text{out}}, -|\hat{\tau}|, \mathbf{shape\_of}(\hat{\tau})); \\
  \text{COMPILE}(\Gamma, (y_{\text{out}} : \tau \text{ as } \hat{\tau}), e_1) \text{ // Emit } e_1 \\
  \text{let}_{\text{in}} y = \text{freeze}(y_{\text{out}}); \\
  \text{COMPILE}(\Gamma \cup (y \triangleleft : \tau \text{ as } \hat{\tau}), (x_{\text{out}} : \tau_{\text{out}} \text{ as } \hat{\tau}_{\text{out}}), e_2) \text{ // Emit } e_2
\end{array}
\right\}
\]
$$

**Algorithm 4:** COMPILE – Compile the expression *e* given the environment *Γ*.

break up the value even more in order to reconstruct it differently. This task is precisely done on
*Line 11* via our next procedure: **REBUILD**.

7.3 Rebuild constructors

REBUILD (Algorithm 6) compiles an arbitrary valueexpression *u* to target code that constructs it.
Whereas SEEK retrieves a (possibly mangled) relevant fragment from a single input value, REBUILD
inspects the shape of the output value to assemble its constituent pieces, which include constant
parts of the memory layout as well as fragments extracted from multiple input values. It reuses
the general structure of SEEK (and EXTRACT), but considers *n* input values described by quadruples
(*x*ᵢ ≺ pᵢ : τᵢ as ̂τᵢ) with 1 ≤ *i* ≤ *n*.

Firstly, when *u* is a constant integer and the output layout is a fixed-width integer encoding, we simply write this constant to the output location (Line 3). In other cases, we operate in a similar manner as in other procedures: we **Explore** the various branches (Line 6), whose code we will eventually combine with **DESTRUCT** (Line 18).

A first subtlety appears: both algorithms need to maintain a precise description of the current case under scrutiny, and to distinguish between all possible subcases. Indeed, after a few recursive calls, we might be exploring deep into input and output layouts. This is done by maintaining the already determined provenances $p_{in}$ through recursive calls. This is essential to emit code that respects invariants stemming from previous branch choices. For the output, however, we do not have a ready-made provenance. We obtain one in Line 5 via the **prov_of** function, which is a simple syntactic translation from expressions to provenances. We can then use the obtained provenance $p_{out}$ in **Explore** to only obtain branches that are relevant to *u*.

Conversely, while exploring a branch characterised by $p_b$, we must perform a similar maneuver
in the opposite direction. Indeed, at execution time, the only way to determine the right branch
of $\hat{\tau}_{\text{out}}$ is to examine input values. By definition, the only variable parts of $p_{\text{out}}$ are those at the
**Data:** $\Gamma = (x_i \triangleleft p_i : \tau_i \text{ as } \hat{\tau}_i)_{0 \le i < n}$ a set of input descriptions

**Data:** *e* the input expression

**Data:** $(x_{\text{out}} : \tau_{\text{out}} \text{ as } \hat{\tau}_{\text{out}})$ the output description

**Result:** Code computing the value of the expression *e*

**function COMPILE(Γ, (x_{out} : τ_{out} as $\hat{\tau}_{out}$), e) = case(e){**

$$
\begin{array}{l@{\quad}l}
\text{match}(y) \{ & \text{ Delegate pattern matching compilation to DESTRUCT (Section 5)} \\
\quad p_i \to e_i \mid (0 \le i < n) \to & (y \triangleleft p : \tau \text{ as } \hat{\tau}) \in \Gamma \\
& \forall i. \mathcal{E}_i \leftarrow \text{COMPILE}(\Gamma, (x_{\text{out}} : \tau_{\text{out}} \text{ as } \hat{\tau}_{\text{out}}), e_i) \\
& \qquad \text{DESTRUCT}((y : \hat{\tau}), \{p_i \to \mathcal{E}_i \mid 1 \le i \le n\})
\end{array}
$$

$$
y.\pi \rightarrow \text{SEEK}(\Gamma(y), (x_{\text{out}} : \tau_{\text{out}} \text{ as } \hat{\tau}_{\text{out}}), \pi) \text{ // SEEK the path } \pi \text{ in } y \text{ (Section 7.2)}
$$

$$
u \rightarrow \begin{array}{@{}l@{}}
\text{REBUILD}(\Gamma, (x_{\text{out}} : \tau_{\text{out}} \text{ as } \hat{\tau}_{\text{out}}), u) \text{ // REBUILD constructor } u \text{ (Section 7.3)} \\
\qquad y_{\text{out}} \text{ fresh.}
\end{array}
$$

$$
\[
\left.
\begin{array}{@{}l@{}}
  \text{Allocate new memory location for } e_1 \text{ with REFINE (Section 7.4)} \\
  \text{let}_{\text{out}} y_{\text{out}} = \text{alloc}(|\hat{\tau}|); \text{REFINE}(y_{\text{out}}, -|\hat{\tau}|, \mathbf{shape\_of}(\hat{\tau})); \\
  \text{COMPILE}(\Gamma, (y_{\text{out}} : \tau \text{ as } \hat{\tau}), e_1) \text{ // Emit } e_1 \\
  \text{let}_{\text{in}} y = \text{freeze}(y_{\text{out}}); \\
  \text{COMPILE}(\Gamma \cup (y \triangleleft : \tau \text{ as } \hat{\tau}), (x_{\text{out}} : \tau_{\text{out}} \text{ as } \hat{\tau}_{\text{out}}), e_2) \text{ // Emit } e_2
\end{array}
\right\}
\]
$$

**Algorithm 4:** COMPILE – Compile the expression *e* given the environment *Γ*.

break up the value even more in order to reconstruct it differently. This task is precisely done on
*Line 11* via our next procedure: **REBUILD**.

7.3 Rebuild constructors

REBUILD (Algorithm 6) compiles an arbitrary valueexpression *u* to target code that constructs it.
Whereas SEEK retrieves a (possibly mangled) relevant fragment from a single input value, REBUILD
inspects the shape of the output value to assemble its constituent pieces, which include constant
parts of the memory layout as well as fragments extracted from multiple input values. It reuses
the general structure of SEEK (and EXTRACT), but considers *n* input values described by quadruples
(*x*ᵢ ≺ pᵢ : τᵢ as ̂τᵢ) with 1 ≤ *i* ≤ *n*.

Firstly, when *u* is a constant integer and the output layout is a fixed-width integer encoding, we simply write this constant to the output location (Line 3). In other cases, we operate in a similar manner as in other procedures: we **Explore** the various branches (Line 6), whose code we will eventually combine with **DESTRUCT** (Line 18).

A first subtlety appears: both algorithms need to maintain a precise description of the current case under scrutiny, and to distinguish between all possible subcases. Indeed, after a few recursive calls, we might be exploring deep into input and output layouts. This is done by maintaining the already determined provenances $p_{in}$ through recursive calls. This is essential to emit code that respects invariants stemming from previous branch choices. For the output, however, we do not have a ready-made provenance. We obtain one in Line 5 via the **prov_of** function, which is a simple syntactic translation from expressions to provenances. We can then use the obtained provenance $p_{out}$ in **Explore** to only obtain branches that are relevant to *u*.

Conversely, while exploring a branch characterised by $p_b$, we must perform a similar maneuver
in the opposite direction. Indeed, at execution time, the only way to determine the right branch
of $\hat{\tau}_{\text{out}}$ is to examine input values. By definition, the only variable parts of $p_{\text{out}}$ are those at the
**Data:** $(x_{in} \triangleleft p_{in} : \tau_{in}$ as $\hat{\tau}_{in}$) the input description

**Data:** $(x_{out} : \tau_{out}$ as $\hat{\tau}_{out}$) the output description

**Data:** $\pi$ the path in the input to the desired subterm

**Result:** Code binding the memory value at position $\pi$ in the input

1 **function** `SEEK((x_{in} \triangleleft p_{in} : \tau_{in}$ as $\hat{\tau}_{in}), (x_{out} : \tau_{out}$ as $\hat{\tau}_{out}), \pi):`
// Invariant: $\pi$ and $p_{in}$ are compatible

2 `if $\pi = \epsilon \land \hat{\tau}_{in} = \hat{\tau}_{out}$ then // Input and output representations are the same, we return.`

3 `return $x_{out} := x_{in}; \text{ success}$`

4 `else // Otherwise, Explore all cases.`

5 $B \leftarrow \textbf{for } p_b, \tau_b, \hat{\tau}_b, \text{frags}_b \in \textbf{Explore}(p_{in}, \tau_{in}, \hat{\tau}_{in}) \textbf{ do}$
// Seek a fragment containing the piece of data at $\pi$.

6 `if $\exists(\hat{\pi}_f \mapsto \pi_f \text{ as } \hat{\tau}_f) \in \text{frags}_b, \exists \pi', \pi = \pi_f. \pi' \text{ then // Found one. Focus and search inside.}$`

7 $x' \leftarrow \text{fresh symbol}$

8 $\tau', p' \leftarrow \textbf{focus} (\pi_f, \tau_b), \textbf{focus} (\pi_f, p_b)$

9 `$\mathcal{E} \leftarrow \text{let}_{in} x' = x.\hat{\pi}_f; \text{SEEK}((x' \triangleleft p' : \tau' \text{ as } \hat{\tau}_f), (x_{out} : \tau_{out} \text{ as } \hat{\tau}_{out}), \pi')$`

10 `else // If none exists, Rebuild from smaller pieces.`

11 `$\mathcal{E} \leftarrow \text{REBUILD}((x_{in} \triangleleft p_{in} : \tau_{in} \text{ as } \hat{\tau}_{in}), (x_{out} : \tau_{out} \text{ as } \hat{\tau}_{out}), x_{in}.\pi)$`

12 `yield $(p_b, \mathcal{E})$`

13 `return $\text{DESTRUCT}((x_{in} : \hat{\tau}_{in}), B) // \text{Assemble the code of these branches via a decision tree.}$`

<caption>**Algorithm 5:** `SEEK` – Seek the memory location representing $\pi$ in $x_{in}$.</caption>

positions of accessors in $u$: there is a bijection between the possible cases of $p_{out}$ and the possible combinations of $p_i$ subcases. At Line 8, we derive a new provenance $p'_i$ for each input, which is at least as precise as $p_i$ and also integrates information from the considered output subcase $p_b$. We use these refined input provenances to emit code that inspects the $n$ input values to determine the right branch of $\hat{\tau}_{out}$, at Line 18.

For each branch, we need two categories of code: how to define the constant part of the value, and how to fill variable parts depending on input arguments. Let us first focus on variable parts. Each variable part exactly corresponds to a fragment. On Line 12, we look for a fragment ($\pi_f$ as $\hat{\tau}_f$) available in the current branch. If there is an accessor $x.\pi$ linked to an input readily available at a corresponding position in $u$, it is sufficient to `SEEK` our desired piece in $x$ (Line 13). If the fragment corresponds to no existing input argument, we need to break it down further, by calling `REBUILD` again (Line 16). While we have found all variable pieces, we have not yet allocated the surrounding memory in which to assemble them! This is done Line 7 via the `REFINE` procedure.

## 7.4 Refine memory locations

So far, we implicitly assumed that the code emitted by a `SEEK` or `REBUILD` call would always be executed in a context where the output location $x_{out}$ contains a memory value of the same shape as $\hat{\tau}_{out}$. This section focuses on the task of emitting allocation and cast instructions to maintain this invariant. We must ensure that whenever the output shape becomes more precise – by replacing a split or fragment in $\hat{\tau}_{out}$ with a concrete layout – the shape of $x_{out}$ is *refined* accordingly by allocating, casting and initializing memory at this position to match the new shape.

The intuition behind our shape refinement procedure is as follows: for both `SEEK` and `REBUILD`, we know that the contents of the output location $x_{out}$ conform to the shape `shape_of(\hat{\tau}_{out})`. This shape might be *opaque* (of the form `_t`), for instance if $\hat{\tau}_{out}$ is a split. In `REBUILD`, we **Explore** the
**Data:** $(x_{in} \triangleleft p_{in} : \tau_{in}$ as $\hat{\tau}_{in}$) the input description

**Data:** $(x_{out} : \tau_{out}$ as $\hat{\tau}_{out}$) the output description

**Data:** $\pi$ the path in the input to the desired subterm

**Result:** Code binding the memory value at position $\pi$ in the input

**1 function** `SEEK((x_{in} \triangleleft p_{in} : \tau_{in}$ as $\hat{\tau}_{in}$), (x_{out} : \tau_{out}$ as $\hat{\tau}_{out}), \pi):`
// Invariant: $\pi$ and $p_{in}$ are compatible

2 `if $\pi = \epsilon \land \hat{\tau}_{in} = \hat{\tau}_{out}$ then // Input and output representations are the same, we return.`

3 `return $x_{out} := x_{in}; \text{ success}$`

4 `else // Otherwise, Explore all cases.`

5 $B \leftarrow \textbf{for } p_b, \tau_b, \hat{\tau}_b, \text{frags}_b \in \textbf{Explore}(p_{in}, \tau_{in}, \hat{\tau}_{in}) \textbf{ do}$
// Seek a fragment containing the piece of data at $\pi$.

6 `if $\exists(\hat{\pi}_f \mapsto \pi_f \text{ as } \hat{\tau}_f) \in \text{frags}_b, \exists \pi', \pi = \pi_f. \pi' \text{ then // Found one. Focus and search inside.}$`

7 $x' \leftarrow \text{fresh symbol}$

8 $\tau', p' \leftarrow \text{focus } (\pi_f, \tau_b), \text{focus } (\pi_f, p_b)$

9 `$\mathcal{E} \leftarrow \text{let}_{in} x' = x. \hat{\pi}_f; \text{SEEK}((x' \triangleleft p' : \tau' \text{ as } \hat{\tau}_f), (x_{out} : \tau_{out} \text{ as } \hat{\tau}_{out}), \pi')$

10 `else // If none exists, Rebuild from smaller pieces.`

11 `$\mathcal{E} \leftarrow \text{REBUILD}((x_{in} \triangleleft p_{in} : \tau_{in} \text{ as } \hat{\tau}_{in}), (x_{out} : \tau_{out} \text{ as } \hat{\tau}_{out}), x_{in}.\pi)$`

12 `yield $(p_b, \mathcal{E})$`

13 `return $\text{DESTRUCT}((x_{in} : \hat{\tau}_{in}), B) // \text{Assemble the code of these branches via a decision tree.}$`

<caption>**Algorithm 5:** `SEEK` – Seek the memory location representing $\pi$ in $x_{in}$.</caption>

positions of accessors in $u$: there is a bijection between the possible cases of $p_{out}$ and the possible combinations of $p_i$ subcases. At Line 8, we derive a new provenance $p'_i$ for each input, which is at least as precise as $p_i$ and also integrates information from the considered output subcase $p_b$. We use these refined input provenances to emit code that inspects the $n$ input values to determine the right branch of $\hat{\tau}_{out}$, at Line 18.

For each branch, we need two categories of code: how to define the constant part of the value, and how to fill variable parts depending on input arguments. Let us first focus on variable parts. Each variable part exactly corresponds to a fragment. On Line 12, we look for a fragment ($\pi_f$ as $\hat{\tau}_f$) available in the current branch. If there is an accessor $x.\pi$ linked to an input readily available at a corresponding position in $u$, it is sufficient to `SEEK` our desired piece in $x$ (Line 13). If the fragment corresponds to no existing input argument, we need to break it down further, by calling `REBUILD` again (Line 16). While we have found all variable pieces, we have not yet allocated the surrounding memory in which to assemble them! This is done Line 7 via the `REFINE` procedure.

## 7.4 Refine memory locations

So far, we implicitly assumed that the code emitted by a `SEEK` or `REBUILD` call would always be executed in a context where the output location $x_{out}$ contains a memory value of the same shape as $\hat{\tau}_{out}$. This section focuses on the task of emitting allocation and cast instructions to maintain this invariant. We must ensure that whenever the output shape becomes more precise – by replacing a split or fragment in $\hat{\tau}_{out}$ with a concrete layout – the shape of $x_{out}$ is *refined* accordingly by allocating, casting and initializing memory at this position to match the new shape.

The intuition behind our shape refinement procedure is as follows: for both `SEEK` and `REBUILD`, we know that the contents of the output location $x_{out}$ conform to the shape `shape_of(\hat{\tau}_{out})`. This shape might be *opaque* (of the form `_t`), for instance if $\hat{\tau}_{out}$ is a split. In `REBUILD`, we **Explore** the
**Data:** $(x_i \triangleleft p_i : \tau_i \text{ as } \hat{\tau}_i)_{1 \le i \le n}$ the $n$ input descriptions

**Data:** $(x_{\text{out}} : \tau_{\text{out}} \text{ as } \hat{\tau}_{\text{out}})$ the output description

**Data:** $u$ the desired value expr

**Result:** Code constructing the memory value corresponding to expression $u$

1 **function** REBUILD((x_i \triangleleft p_i : \tau_i \text{ as } \hat{\tau}_i)_{1 \le i \le n}, (x_{\text{out}} : \tau_{\text{out}} \text{ as } \hat{\tau}_{\text{out}}), u):

2 **if** $u = c \land \hat{\tau}_{\text{out}} = I_t$ **then** // Target value is a constant encoded in an immediate type.

3 **return** $x_{\text{out}} := c; \text{ success}$

4 **else** // Otherwise, Explore all cases.

5 $p_{\text{out}} \leftarrow \text{prov\_of}(\tau_{\text{out}}, u)$

6 $B \leftarrow \text{for } p_b, \tau_b, \hat{\tau}_b, \text{frags}_b \in \text{Explore}(p_{\text{out}}, \tau_{\text{out}}, \hat{\tau}_{\text{out}})$ do

// Allocate memory, cast and fill in constant parts of the target memory layout to fit its shape.

7 $\mathcal{E}_{\text{conssts}} \leftarrow \text{REFINE}(x_{\text{out}}, \text{shape\_of}(\hat{\tau}_{\text{out}}), \text{shape\_of}(\hat{\tau}_b))$

// Rebuild target fragments from input values, which we specialize for the current branch.

8 $\forall i, p'_i \leftarrow p_i$ [$\text{ at } \pi_{\text{in}} \cdot \pi \leftarrow \text{focus}(\pi_{\text{out}} \cdot \pi, p_b)$ | **focus**($\pi_{\text{out}}, u) = x_i \cdot \pi_{\text{in}$

9 $\mathcal{E}_{\text{frags}} \leftarrow \text{for } (\hat{\pi}_f \mapsto \pi_f \text{ as } \hat{\tau}_f) \in \text{frags}_b$ **do**

10 $x'_{\text{out}} \leftarrow \text{fresh symbol}$

11 $\tau_f \leftarrow \text{focus}(\pi_f, \tau_b)$

// Look at the subterm containing $\pi_f$ in $u$

12 **if** $\exists i, \pi, \pi_{\text{in}}, \pi_{\text{out}} \text{focus}(\pi_{\text{out}}, u) = x_i \cdot \pi_{\text{in}} \land \pi_{\text{out}} \cdot \pi = \pi_f$ **then** // Found an input path $x_i \cdot \pi_{\text{in}} \cdot \pi$

13 **yield** $\text{let out } x'_{\text{out}} = x_{\text{out}} \cdot \hat{\pi}_f$; **SEEK** $((x_i \triangleleft p'_i : \tau_i \text{ as } \hat{\tau}_i), (x'_{\text{out}} : \tau_f \text{ as } \hat{\tau}_f), \pi_{\text{in}} \cdot \pi)$

14 **else** // Otherwise, break it down further.

15 $u' \leftarrow \text{focus}(\pi_f, u)$

16 **yield** $\text{let out } x'_{\text{out}} = x_{\text{out}} \cdot \hat{\pi}_f$; REBUILD $((x_i \triangleleft p'_i : \tau_i \text{ as } \hat{\tau}_i)_{1 \le i \le n}, (x'_{\text{out}} : \tau_f \text{ as } \hat{\tau}_f), u')$

17 **yield** $((x_i \triangleleft p'_i)_{1 \le i \le n}, \mathcal{E}_{\text{conssts}}; \mathcal{E}_{\text{frags}})$

18 **return** **DESTRUCT** $((x_i : \hat{\tau}_i)_{1 \le i \le n}, B)$ // Assemble these branches into a decision tree.

<caption>**Algorithm 6:** REBUILD – Rebuild the value in memory representing $u$ from the $x_i$s.</caption>

output type and layout, yielding a more precise layout $\hat{\tau}_b$. This is precisely the time at which we might need to allocate: if we discover that $\hat{\tau}_b$ contains a pointer to new structures, we should allocate them for future use. REFINE creates a skeleton that will be filled later on. This can happens either while rebuilding values, on Line 7 in Algorithm 6, or while compiling let-bindings, in Algorithm 4.

This leads us to define REFINE (Algorithm 7), which takes an output location $x$, an imprecise shape $\hat{p}_{\text{old}}$ and a more precise shape $\hat{p}_{\text{new}}$, and emits a piece of code that allocates memory and initializes constants everywhere $\hat{p}_{\text{new}}$ is more precise than $\hat{p}_{\text{old}}$. For instance, when discovering a new pointer, we allocate a new address to fill $x$. Furthermore, we explore recursively the shapes to fill out all the pieces, for instance in the case of structs. Note that refining composite words $\hat{p} \succsim_{0 \le i < n} [o_i : \ell_i] : \hat{p}'_i$ takes peculiar care: indeed, $\hat{p}$ could yield a new pointer, which should be masked appropriately to not overwrite values obtained by the right hand sides. For this purpose, we craft a new mask using the **mask**$_t$ functions to generate $t$-bit masks that precisely focus on the leftmost/base layout of a composite word.

Note that our refinement procedure is directly linked to the precision of the **shape\_of** function (Fig. 10): a more precise shape analysis, for instance that inspects inside pointers, would yield earlier, easily factorised, memory allocations.
**Data:** $(x_i \triangleleft p_i : \tau_i \text{ as } \hat{\tau}_i)_{1 \le i \le n}$ the $n$ input descriptions

**Data:** $(x_{\text{out}} : \tau_{\text{out}} \text{ as } \hat{\tau}_{\text{out}})$ the output description

**Data:** $u$ the desired value expr

**Result:** Code constructing the memory value corresponding to expression $u$

1 function REBUILD((x_i \triangleleft p_i : \tau_i \text{ as } \hat{\tau}_i)_{1 \le i \le n}, (x_{\text{out}} : \tau_{\text{out}} \text{ as } \hat{\tau}_{\text{out}}), u):

2 if $u = c \land \hat{\tau}_{\text{out}} = I_t$ then // Target value is a constant encoded in an immediate type.

3 return $x_{\text{out}} := c; \text{ success}$

4 else // Otherwise, Explore all cases.

5 $p_{\text{out}} \leftarrow \text{prov\_of}(\tau_{\text{out}}, u)$

6 $B \leftarrow \text{for } p_b, \tau_b, \hat{\tau}_b, \text{frags}_b \in \text{Explore}(p_{\text{out}}, \tau_{\text{out}}, \hat{\tau}_{\text{out}})$ do

// Allocate memory, cast and fill in constant parts of the target memory layout to fit its shape.

7 $\mathcal{E}_{\text{conssts}} \leftarrow \text{REFINE}(x_{\text{out}}, \text{shape\_of}(\hat{\tau}_{\text{out}}), \text{shape\_of}(\hat{\tau}_b))$

// Rebuild target fragments from input values, which we specialize for the current branch.

8 $\forall i, p'_i \leftarrow p_i$ at $\pi_{\text{in}} \cdot \pi \leftarrow \text{focus}(\pi_{\text{out}} \cdot \pi, p_b)$ | $\text{focus}(\pi_{\text{out}}, u) = x_i \cdot \pi_{\text{in}}$

9 $\mathcal{E}_{\text{frags}} \leftarrow \text{for } (\hat{\pi}_f \mapsto \pi_f \text{ as } \hat{\tau}_f) \in \text{frags}_b$ do

10 $x'_{\text{out}} \leftarrow \text{fresh symbol}$

11 $\tau_f \leftarrow \text{focus}(\pi_f, \tau_b)$

// Look at the subterm containing $\pi_f$ in $u$

12 if $\exists i, \pi, \pi_{\text{in}}, \pi_{\text{out}} \text{focus}(\pi_{\text{out}}, u) = x_i \cdot \pi_{\text{in}} \land \pi_{\text{out}} \cdot \pi = \pi_f$ then // Found an input path $x_i \cdot \pi_{\text{in}} \cdot \pi$

13 $\text{yield} \text{letout } x'_{\text{out}} = x_{\text{out}} \cdot \hat{\pi}_f$; \text{SEEK} $((x_i \triangleleft p'_i : \tau_i \text{ as } \hat{\tau}_i), (x'_{\text{out}} : \tau_f \text{ as } \hat{\tau}_f), \pi_{\text{in}} \cdot \pi)$

14 else // Otherwise, break it down further.

15 $u' \leftarrow \text{focus}(\pi_f, u)$

16 $\text{yield} \text{letout } x'_{\text{out}} = x_{\text{out}} \cdot \hat{\pi}_f$; \text{REBUILD} $((x_i \triangleleft p'_i : \tau_i \text{ as } \hat{\tau}_i)_{1 \le i \le n}, (x'_{\text{out}} : \tau_f \text{ as } \hat{\tau}_f), u')$

17 $\text{yield} ((x_i \triangleleft p'_i)_{1 \le i \le n}, \mathcal{E}_{\text{conssts}}; \mathcal{E}_{\text{frags}})$

18 $\text{return} \text{DESTRUCT}((x_i : \hat{\tau}_i)_{1 \le i \le n}, B)$ // Assemble these branches into a decision tree.

<caption>**Algorithm 6:** REBUILD – Rebuild the value in memory representing $u$ from the $x_i$s.</caption>

output type and layout, yielding a more precise layout $\hat{\tau}_b$. This is precisely the time at which we might need to allocate: if we discover that $\hat{\tau}_b$ contains a pointer to new structures, we should allocate them for future use. REFINE creates a skeleton that will be filled later on. This can happens either while rebuilding values, on Line 7 in Algorithm 6, or while compiling let-bindings, in Algorithm 4.

This leads us to define REFINE (Algorithm 7), which takes an output location $x$, an imprecise shape $\hat{p}_{\text{old}}$ and a more precise shape $\hat{p}_{\text{new}}$, and emits a piece of code that allocates memory and initializes constants everywhere $\hat{p}_{\text{new}}$ is more precise than $\hat{p}_{\text{old}}$. For instance, when discovering a new pointer, we allocate a new address to fill $x$. Furthermore, we explore recursively the shapes to fill out all the pieces, for instance in the case of structs. Note that refining composite words $\hat{p} \succsim_{0 \le i < n} [o_i : \ell_i] : \hat{p}'_i$ takes peculiar care: indeed, $\hat{p}$ could yield a new pointer, which should be masked appropriately to not overwrite values obtained by the right hand sides. For this purpose, we craft a new mask using the **mask**$_t$ functions to generate $t$-bit masks that precisely focus on the leftmost/base layout of a composite word.

Note that our refinement procedure is directly linked to the precision of the **shape\_of** function (Fig. 10): a more precise shape analysis, for instance that inspects inside pointers, would yield earlier, easily factorised, memory allocations.
- **fragment** (.*.0 $\mapsto$ .Cons.0 as $I_{32}$) where **focus** (Cons.0, $u$) = $h'$ and $\underline{letout}$ $d_{f0} = d.*.0$
  call $\mathcal{E}'_{f1} = \text{SEEK}(\Gamma(h'), (d_{f0}: I_{32} \text{ as } I_{32}), \epsilon) = \underline{d_{f0} := h'}$ (**base case**)

- **fragment** (.*.1 $\mapsto$ $\pi_l$ = .Cons.1.Cons.0 as $I_{32}$) where **focus** ($\pi_l, u$) = $x.\pi_l$ and $\underline{letout}$ $d_{f1} = d.*.1$
  call $\mathcal{E}'_{f1} = \text{SEEK}(\Gamma(x), (d_{f1}: I_{32} \text{ as } I_{32}), \pi_l) = \underline{\text{let}_\text{in} s_{f1} = x.\text{Cons.0.Cons.1}; d_{f1} := s_{f1}}$

- **fragment** (.*.2 $\mapsto$ $\pi_r$ = .Cons.1.Cons.1 as $\hat{\tau}_p$) where **focus** ($\pi_r, u$) = $x.\pi_r$ and $\underline{letout}$ $d_{f2} = d.*.2$
  call $\mathcal{E}'_{f1} = \text{SEEK}(\Gamma(x), (d_{f2}: I_{32} \text{ as } I_{32}), \pi_r) = \underline{\text{let}_\text{in} s_{f2} = x.\text{Cons.1.Cons.1}; d_{f2} := s_{f2}}$

yield (Cons($_\cdot$, Cons($_\cdot$, $_\cdot$), $\underline{\mathcal{E}'_c; \mathcal{E}'_{f1}; \mathcal{E}'_{f2}; \mathcal{E}'_{f3}}$)

return **DESTRUCT** $((x : \hat{\tau}_p), \{\text{(Cons}($_\cdot$, Nil), $\underline{\mathcal{E}_c; \mathcal{E}_f}$), \text{(Cons}($_\cdot$, Cons($_\cdot$, $_\cdot$), $\underline{\mathcal{E}'_c; \mathcal{E}'_{f1}; \mathcal{E}'_{f2}; \mathcal{E}'_{f3}})$\})}$

## 7.6 Recursive Constructors

Although the algorithm presented so far is sufficient to handle most situations, it does not necessarily terminate in the presence of recursive types and layouts. Let us consider an example.

**Example 7.1 (Recursive rebuilding of linked lists).** Consider simply-linked lists of 32-bit integers $\tau = \text{Nil}$ | Cons($I_{32}$, $\tau$) with two possible layouts. $\hat{\tau}_l$ is a traditional “pointers and blocks” layout with a pointer for each element. $\hat{\tau}_p$ is the packed layout already shown in **Example 3.3**. We can ask **REBUILD** to emit conversion code that transforms inputs of type $\tau$ with representation $\hat{\tau}_l$ into an output of type $\tau$ with representation $\hat{\tau}_p$: **REBUILD**((x $\triangleleft$ $_\cdot$: $\tau$ as $\hat{\tau}_l$), (y: $\tau$ as $\hat{\tau}_p$), $\epsilon$).

Naturally, such conversion code is not so simple: it requires recursive code that walks the structure and fuse blocks two by two. Our current algorithms will not terminate, as it tries to **REBUILD** each block in the list, infinitely. $\Delta$

To properly handle such cases, we must emit **recursive constructor code**. Naturally, we could also refuse to emit such code (in contexts when recursion is not acceptable). In both cases, we need to detect recursion. We now sketch the main idea; full details are available in **Appendix B**. Intuitively, a call to **SEEK** or **REBUILD** leads to infinite recursion if it attempts to recursively rebuild an output value with the same type, layout and relative position from an input value with the same type, layout and provenance. This indicates that the output value contains a subterm which must be rebuilt in the exact same way: the only way to emit correct code is to introduce an explicit recursive node and emit recursive calls at this position. For this purpose, we **memoise** **SEEK** and **REBUILD** on their **anonymized** arguments, i.e. the arguments without any input or output memory locations. For instance, **prov_of(u)** is kept instead of u. We record when we enter one of the algorithms, and generate a fresh function symbol f. If we enter this function again, we emit a call call f(x, y) with the appropriate arguments. Afterwards, we can use simple deforestation to get rid of extra functions. Note that, on top of emitting recursive code, this also improves sharing.

**Example 7.2 (Linked lists, cont'd).** Using memoisation, the **REBUILD** call from our previous example terminates and emits recursive code. We explore $\hat{\tau}_p$ and get three branches from its split. The first two branch with the provenances Nil and Cons($_\cdot$, Nil) are straightforward. The third branch Cons($_\cdot$, Cons($_\cdot$, $_\cdot$)) requires rebuilding the fragment (.*.2 $\mapsto$ .Cons.1.Cons.1 as $\hat{\tau}_p$), which is more involved. Indeed, the position .Cons.1.Cons.1 in the original list type $\hat{\tau}_l$ represents itself a tail of type $\hat{\tau}_l$. Eventually, we try to **REBUILD** a piece of type $\tau$ represented as $\hat{\tau}_p$ from the same piece represented as $\hat{\tau}_l$, i.e., the same task as the initial **REBUILD** call. Thanks to memoisation, this task is now associated with a function symbol f and we finally emit the target code in Fig. 12. $\Delta$
- **fragment** (.*.0 $\mapsto$ .Cons.0 as $I_{32}$) where **focus** (Cons.0, $u$) = $h'$ and $\underline{letout}$ $d_{f0} = d.*.0$
  call $\mathcal{E}'_{f1} = \text{SEEK}(\Gamma(h'), (d_{f0}: I_{32} \text{ as } I_{32}), \epsilon) = \underline{d_{f0} := h'}$ (**base case**)

- **fragment** (.*.1 $\mapsto$ $\pi_l$ = .Cons.1.Cons.0 as $I_{32}$) where **focus** ($\pi_l, u$) = $x.\pi_l$ and $\underline{letout}$ $d_{f1} = d.*.1$
  call $\mathcal{E}'_{f1} = \text{SEEK}(\Gamma(x), (d_{f1}: I_{32} \text{ as } I_{32}), \pi_l) = \underline{\text{let}_\text{in} s_{f1} = x.\text{Cons.0.Cons.1}; d_{f1} := s_{f1}}$

- **fragment** (.*.2 $\mapsto$ $\pi_r$ = .Cons.1.Cons.1 as $\hat{\tau}_p$) where **focus** ($\pi_r, u$) = $x.\pi_r$ and $\underline{letout}$ $d_{f2} = d.*.2$
  call $\mathcal{E}'_{f1} = \text{SEEK}(\Gamma(x), (d_{f2}: I_{32} \text{ as } I_{32}), \pi_r) = \underline{\text{let}_\text{in} s_{f2} = x.\text{Cons.1.Cons.1}; d_{f2} := s_{f2}}$

yield (Cons($_\cdot$, Cons($_\cdot$, $_\cdot$), $\underline{\mathcal{E}'_c; \mathcal{E}'_{f1}; \mathcal{E}'_{f2}; \mathcal{E}'_{f3}}$)

return **DESTRUCT** $((x : \hat{\tau}_p), \{\text{(Cons}($_\cdot$, \text{Nil}), \underline{\mathcal{E}_c; \mathcal{E}_f}\}), \text{(Cons}($_\cdot$, Cons($_\cdot$, $_\cdot$), \underline{\mathcal{E}'_c; \mathcal{E}'_{f1}; \mathcal{E}'_{f2}; \mathcal{E}'_{f3}})\})$)

7.6 Recursive Constructors

Although the algorithm presented so far is sufficient to handle most situations, it does not necessarily
terminate in the presence of recursive types and layouts. Let us consider an example.

Example 7.1 (Recursive rebuilding of linked lists). Consider simply-linked lists of 32-bit integers $\tau = \text{Nil}$ | $\text{Cons}(I_{32}, \tau)$ with two possible layouts. $\hat{\tau}_l$ is a traditional “pointers and blocks” layout with a pointer for each element. $\hat{\tau}_p$ is the packed layout already shown in Example 3.3. We can ask REBUILD to emit conversion code that transforms inputs of type $\tau$ with representation $\hat{\tau}_l$ into an output of type $\tau$ with representation $\hat{\tau}_p$: REBUILD((x $\triangleleft$ $_{-}$: $\tau$ as $\hat{\tau}_l$), (y: $\tau$ as $\hat{\tau}_p$), $\epsilon$).

Naturally, such conversion code is not so simple: it requires recursive code that walks the
structure and fuse blocks two by two. Our current algorithms will not terminate, as it tries to
REBUILD each block in the list, infinitely.

$\Delta$

To properly handle such cases, we must emit recursive constructor code. Naturally, we could also
refuse to emit such code (in contexts when recursion is not acceptable). In both cases, we need to
detect recursion. We now sketch the main idea; full details are available in Appendix B. Intuitively,
a call to `SEEK` or `REBUILD` leads to infinite recursion if it attempts to recursively rebuild an output
value with the same type, layout and relative position from an input value with the same type,
layout and provenance. This indicates that the output value contains a subterm which must be
rebuilt in the exact same way: the only way to emit correct code is to introduce an explicit recursive
node and emit recursive calls at this position. For this purpose, we memoise `SEEK` and `REBUILD` on
their anonymized arguments, i.e. the arguments without any input or output memory locations.
For instance, `prov_of(u)` is kept instead of `u`. We record when we enter one of the algorithms,
and generate a fresh function symbol `f`. If we enter this function again, we emit a call `call f(x, y)`
with the appropriate arguments. Afterwards, we can use simple deforestation to get rid of extra
functions. Note that, on top of emitting recursive code, this also improves sharing.

Example 7.2 (Linked lists, cont’d). Using memoisation, the REBUILD call from our previous example terminates and emits recursive code. We explore $\hat{\tau}_p$ and get three branches from its split. The first two branch with the provenances Nil and Cons($_\cdot$, Nil) are straightforward. The third branch Cons($_\cdot$, Cons($_\cdot$, $_\cdot$)) requires rebuilding the fragment (.*.2 $\mapsto$ .Cons.1.Cons.1 as $\hat{\tau}_p$), which is more involved. Indeed, the position .Cons.1.Cons.1 in the original list type $\hat{\tau}_l$ represents itself a tail of type $\hat{\tau}_l$. Eventually, we try to REBUILD a piece of type $\tau$ represented as $\hat{\tau}_p$ from the same piece represented as $\hat{\tau}_l$, i.e., the same task as the initial REBUILD call. Thanks to memoisation, this task is now associated with a function symbol `f` and we finally emit the target code in Fig. 12. $\Delta$
<figure><img src="image_8.png" /><figcaption>Fig. 12. Generated code for rebuilding linked lists $s$ is the entry list and $d$ the destination name.</figcaption></figure>

# 8 METATHEORY

We now briefly sketch the semantics of our source and target languages and state the correctness of our compilation approach. Most of the definitions are delegated to the Appendix.

First, let us specify valid programs. We define a source typing judgement, denoted $\Gamma \vdash e : \tau$. This typing judgement is a straightforward monomorphic type system with ADTs. Additionally, we follow Baudon et al. [2023] by defining the *agreement* between a type and its layout, denoted **agree**($\tau, \hat{\tau}$). This agreement for instance, ensures that paths are coherent, branches are all represented, etc. Both are defined in Appendix C.1. We define the shape of a memory value in a store, denoted **shape_of**<sub>ζ</sub>(v̂), in a similar way to the shape of a memory layout (Appendix C, Fig. 20). The equivalence judgment between store/memory value pairs, denoted ζ, v̂_ζ ~ ζ', v̂_ζ', holds if and only if v̂_ζ and v̂_ζ' are identical up to address renaming. Both are defined in Appendix C.2.

In order to give a precise account of our semantics, and be able to compare between source and compiled programs, we provide a semantic for the source language which precisely account for the state of memory, following the specified memory layout. For this purpose, we define a small-step evaluation judgment for our source language, denoted $\Gamma, \hat{\sigma}, \zeta, \hat{e} \leftrightarrow \Gamma', \sigma', \zeta', \hat{e}'$, where:

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

* $\hat{\sigma}: \mathit{Vars} \to \widehat{\mathit{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. Its full grammar is given in Appendix C.2 (Fig. 19); 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 $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}$). Its full definition is available in Appendix C.2 (Figs. 22 and 23); here, we quickly demonstrate it on an example.
<figure><img src="image_9.png" /><figcaption>Fig. 12. Generated code for rebuilding linked lists $s$ is the entry list and $d$ the destination name.</figcaption></figure>

# 8 METATHEORY

We now briefly sketch the semantics of our source and target languages and state the correctness of our compilation approach. Most of the definitions are delegated to the Appendix.

First, let us specify valid programs. We define a source typing judgement, denoted $\Gamma \vdash e : \tau$. This typing judgement is a straightforward monomorphic type system with ADTs. Additionally, we follow Baudon et al. [2023] by defining the *agreement* between a type and its layout, denoted **agree**($\tau, \hat{\tau}$). This agreement for instance, ensures that paths are coherent, branches are all represented, etc. Both are defined in Appendix C.1. We define the shape of a memory value in a store, denoted **shape_of**<sub>ζ</sub>(v̂), in a similar way to the shape of a memory layout (Appendix C, Fig. 20). The equivalence judgment between store/memory value pairs, denoted ζ, v̂ = ζ', v̂', holds if and only if v̂ and v̂' are identical up to address renaming. Both are defined in Appendix C.2.

In order to give a precise account of our semantics, and be able to compare between source and compiled programs, we provide a semantic for the source language which precisely account for the state of memory, following the specified memory layout. For this purpose, we define a small-step evaluation judgment for our source language, denoted $\Gamma, \hat{\sigma}, \zeta, \hat{e} \mapsto \Gamma', \sigma', \zeta', \hat{e}'$, where:

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

* $\hat{\sigma}: \mathit{Vars} \to \widehat{\mathit{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. Its full grammar is given in Appendix C.2 (Fig. 19); 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 $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}$). Its full definition is available in Appendix C.2 (Figs. 22 and 23); here, we quickly demonstrate it on an example.
**Example 8.1 (Source semantics on lists).** Let us recall our list example with layout $\hat{\tau}_p$ from Example 3.3, and evaluate the following expression in initially empty environments and store (environments $\Gamma$ and $\hat{\sigma}$ are merged for conciseness): $e = \text{let } x : \tau_{\text{list}} \text{ as } \hat{\tau}_p = \text{Cons}(42, \text{Nil}) \text{ in } x.\text{Cons}(0 : I_{32} \text{ as } I_{32})$

$\emptyset, \emptyset, \text{let } x : \tau_{\text{list}} \text{ as } \hat{\tau}_p = \text{Cons}(42, \text{Nil}) \text{ in } (x.\text{Cons}.0 : I_{32} \text{ as } I_{32})$

$\leftrightarrow \emptyset, \emptyset, \text{let } x : \tau_{\text{list}} \text{ as } \hat{\tau}_p = \underline{-64} \bowtie \underline{[0:2]} : (1)_2 \bowtie \underline{[2:32]} : \underline{(42 : I_{32} \text{ as } I_{32})} \text{ in } (x.\text{Cons}.0 : I_{32} \text{ as } I_{32})$

$\leftrightarrow \emptyset, \emptyset, \text{let } x : \tau_{\text{list}} \text{ as } \hat{\tau}_p = \underline{-64} \bowtie \underline{[0:2]} : (1)_2 \bowtie \underline{[2:32]} : \underline{(42)_{32}} \text{ in } (x.\text{Cons}.0 : I_{32} \text{ as } I_{32})$

$\leftrightarrow \{x : \tau_{\text{list}} \text{ as } \hat{\tau}_p \mapsto a.\epsilon\}, \{a \mapsto \underline{-64} \bowtie \underline{[0:2]} : (1)_2 \bowtie \underline{[2:32]} : \underline{(42)_{32}}\}, (x.\text{Cons}.0 : I_{32} \text{ as } I_{32})$

$\leftrightarrow \{\dots, x' : I_{32} \text{ as } I_{32} \mapsto a.[2:32]\}, \{\dots\}, (x'.\epsilon : I_{32} \text{ as } I_{32})$

$\leftrightarrow \{\dots\}, \{\dots\}, (42)_{32}$

Δ

For the target IR, we use a more standard small step semantics with a store modeling the content of the memory. Our target evaluation judgement is denoted $\rho_{\text{in}}, \rho_{\text{out}}, \zeta, \mathcal{E} \rightsquigarrow \rho'_{\text{in}}, \rho'_{\text{out}}, \zeta', \mathcal{E}'$, where:

* $\rho_{\text{in}}$ and $\rho_{\text{out}}$ map input and output location identifiers to concrete locations, which consist of an address and a memory path (i.e., unaligned pointers);

* $\zeta$ is a memory store used to interpret the contents of $\rho_{\text{in}}$ and $\rho_{\text{out}}$;

* $\mathcal{E}$ is the target expression to evaluate.

Normal forms are states where $\mathcal{E}$ is a return statement (success or fail). The location environments $\rho_{\text{in}}$ and $\rho_{\text{out}}$ enforce a distinction between input and output locations, and directly reflect the effects of let in and let out instructions; for instance, we evaluate $\text{let}_{\text{in}} x' = x.\hat{\pi}$ by looking up $x$ in $\rho_{\text{in}}$, appending $\hat{\pi}$ to $\rho_{\text{in}}(x)$ and binding the result to $x'$ in $\rho_{\text{in}}$. The store $\zeta$ is only used by instructions that allocate memory or perform actual reads/writes, such as switches and writes. The full judgment is available in appendix (Fig. 24).

We can now state our main result: given a source expression and its compiled target expression, their evaluation eventually yields identical memory contents.

**THEOREM 8.2 (SOUNDNESS).** Let $\tau$ a type, $\hat{\tau}$ a layout and $e$ a source expression such that $\hat{\tau}$ agrees with $\tau$ and $\Gamma \vdash e : \tau$. Let $x$ free in $e$ and $a$ a fresh address. Finally, let $\zeta_0$ and $\hat{v}_0$ the initial memory store and value where $\hat{v}_0$ is compatible with $\hat{\tau}$, i.e. $\text{shape\_of}_{\zeta_0}(\hat{v}_0) = \text{shape\_of}(\hat{\tau})$.

The following conditions hold:

* `COMPILE` (Ø, $(x : \tau \text{ as } \hat{\tau})$, e) succeeds and yields a target expression $\mathcal{E}$;

* the source evaluation reaches a normal form: Ø, Ø, Ø, e $\leftrightarrow^* \Gamma, \hat{\sigma}, \zeta_s, \hat{v}_s$;

* the target evaluation reaches a successful state: Ø, {$x \mapsto a.\epsilon$}, $\zeta_0 \cup \{a \mapsto \hat{v}_0\}$, $\mathcal{E} \rightsquigarrow^* \rho_{\text{in}}, \rho_{\text{out}}, \zeta_t$, success with $(x \mapsto a.\epsilon) \in \rho_{\text{out}}$ and there exists $\hat{v}_t$ such that $(a \mapsto \hat{v}_t) \in \zeta_t$;

* the results of source and target evaluation are equivalent: $\zeta_s, \hat{\sigma}_s \sim \zeta_t, \hat{v}_t$.

# 9 RELATED WORK

*Algebraic Data Types and low-level programming.* ADTs, pattern matching compilation and compact memory representations all have long histories. We summarise the work directly related to low-level programming.

Our approach directly extends (and subsumes) [Baudon et al. 2023]. In particular, their “regular” case is covered by our initial naive algorithm in Section 6.2. Our full procedure covers all possible cases, including the so-called “irregular” ones which they only sketch.

Many of the links between ADTs and low-level programming were initially made for verification. Notably, Dargent [Chen et al. 2023] allows to specify memory representations in an external DSL which outputs C code for accessors, and Isabelle/HOL theorems; with the aim of formally verifying embedded systems. Swamy et al. [2022] propose a similar approach to formally verify binary format parsers in $F^*$. These approaches are precise, leveraging their host proof assistant, but do not provide
**Example 8.1 (Source semantics on lists).** Let us recall our list example with layout $\hat{\tau}_p$ from Example 3.3, and evaluate the following expression in initially empty environments and store (environments $\Gamma$ and $\hat{\sigma}$ are merged for conciseness): $e = \text{let } x : \tau_{\text{list}} \text{ as } \hat{\tau}_p = \text{Cons}(42, \text{Nil}) \text{ in } x.\text{Cons}(0 : I_{32} \text{ as } I_{32})$

$\emptyset, \emptyset, \text{ let } x : \tau_{\text{list}} \text{ as } \hat{\tau}_p = \text{Cons}(42, \text{Nil}) \text{ in } (x.\text{Cons}.0 : I_{32} \text{ as } I_{32})$

$\leftrightarrow \emptyset, \emptyset, \text{ let } x : \tau_{\text{list}} \text{ as } \hat{\tau}_p = \underline{-64} \bowtie \underline{[0:2]} : (1)_2 \bowtie \underline{[2:32]} : \underline{(42 : I_{32} \text{ as } I_{32})} \text{ in } (x.\text{Cons}.0 : I_{32} \text{ as } I_{32})$

$\leftrightarrow \emptyset, \emptyset, \text{ let } x : \tau_{\text{list}} \text{ as } \hat{\tau}_p = \underline{-64} \bowtie \underline{[0:2]} : (1)_2 \bowtie \underline{[2:32]} : \underline{(42)_{32}} \text{ in } (x.\text{Cons}.0 : I_{32} \text{ as } I_{32})$

$\leftrightarrow \{x : \tau_{\text{list}} \text{ as } \hat{\tau}_p \mapsto a.\epsilon\}, \{a \mapsto \underline{-64} \bowtie \underline{[0:2]} : (1)_2 \bowtie \underline{[2:32]} : \underline{(42)_{32}}\}, (x.\text{Cons}.0 : I_{32} \text{ as } I_{32})$

$\leftrightarrow \{\dots, x' : I_{32} \text{ as } I_{32} \mapsto a.\underline{[2:32]}\}, \{\dots\}, (x'.\epsilon : I_{32} \text{ as } I_{32})$

$\leftrightarrow \{\dots\}, \{\dots\}, (42)_{32}$

Δ

For the target IR, we use a more standard small step semantics with a store modeling the content of the memory. Our target evaluation judgement is denoted $\rho_{\text{in}}, \rho_{\text{out}}, \zeta, \mathcal{E} \rightsquigarrow \rho'_{\text{in}}, \rho'_{\text{out}}, \zeta', \mathcal{E}'$, where:

* $\rho_{\text{in}}$ and $\rho_{\text{out}}$ map input and output location identifiers to concrete locations, which consist of an address and a memory path (i.e., unaligned pointers);

* $\zeta$ is a memory store used to interpret the contents of $\rho_{\text{in}}$ and $\rho_{\text{out}}$;

* $\mathcal{E}$ is the target expression to evaluate.

Normal forms are states where $\mathcal{E}$ is a return statement (success or fail). The location environments $\rho_{\text{in}}$ and $\rho_{\text{out}}$ enforce a distinction between input and output locations, and directly reflect the effects of `let in` and `let out` instructions; for instance, we evaluate `let_{in} x' = x.\hat{\pi}` by looking up $x$ in $\rho_{\text{in}}$, appending $\hat{\pi}$ to $\rho_{\text{in}}(x)$ and binding the result to $x'$ in $\rho_{\text{in}}$. The store $\zeta$ is only used by instructions that allocate memory or perform actual reads/writes, such as switches and writes. The full judgment is available in appendix (Fig. 24).

We can now state our main result: given a source expression and its compiled target expression, their evaluation eventually yields identical memory contents.

**THEOREM 8.2 (SOUNDNESS).** Let $\tau$ a type, $\hat{\tau}$ a layout and $e$ a source expression such that $\hat{\tau}$ agrees with $\tau$ and $\Gamma \vdash e : \tau$. Let $x$ free in $e$ and $a$ a fresh address. Finally, let $\zeta_0$ and $\hat{v}_0$ the initial memory store and value where $\hat{v}_0$ is compatible with $\hat{\tau}$, i.e. $\text{shape\_of}_{\zeta_0}(\hat{v}_0) = \text{shape\_of}(\hat{\tau})$.

The following conditions hold:

* `COMPILE` ($\emptyset, (x : \tau \text{ as } \hat{\tau}), e$) succeeds and yields a target expression $\mathcal{E}$;

* the source evaluation reaches a normal form: $\emptyset, \emptyset, \emptyset, e \leftrightarrow^* \Gamma, \hat{\sigma}, \zeta_s, \hat{v}_s$;

* the target evaluation reaches a successful state: $\emptyset, \{x \mapsto a.\epsilon\}, \zeta_0 \cup \{a \mapsto \hat{v}_0\}, \mathcal{E} \leftrightarrow^* \rho_{\text{in}}, \rho_{\text{out}}, \zeta_t$, success with $(x \mapsto a.\epsilon) \in \rho_{\text{out}}$ and there exists $\hat{v}_t$ such that $(a \mapsto \hat{v}_t) \in \zeta_t$;

* the results of source and target evaluation are equivalent: $\zeta_s, \hat{\sigma}_s \sim \zeta_t, \hat{v}_t$.

# 9 RELATED WORK

*Algebraic Data Types and low-level programming.* ADTs, pattern matching compilation and compact memory representations all have long histories. We summarise the work directly related to low-level programming.

Our approach directly extends (and subsumes) [Baudon et al. 2023]. In particular, their “regular” case is covered by our initial naive algorithm in Section 6.2. Our full procedure covers all possible cases, including the so-called “irregular” ones which they only sketch.

Many of the links between ADTs and low-level programming were initially made for verification. Notably, Dargent [Chen et al. 2023] allows to specify memory representations in an external DSL which outputs C code for accessors, and Isabelle/HOL theorems; with the aim of formally verifying embedded systems. Swamy et al. [2022] propose a similar approach to formally verify binary format parsers in $F^*$. These approaches are precise, leveraging their host proof assistant, but do not provide
language-integrated constructs such as pattern matching. They also provide far less optimisations
than what we propose.

LoCal [Vollmer et al. 2019] and Gibbon [Koparkar et al. 2021], on the other hand, provide
DSLs tailored to describe and manipulate low-level and serialised representations. Their memory
layouts are less flexible than what we presented, making it impossible to provide truly customised
representations, but allowing them numerous powerful optimisations we do not provide, such as
leveraging parallelism. We hope to combine our approaches in the future.

Finally, some general-purpose languages provide ways to improve data layout. Rust's niches [RFC: Alignment niches for references types 2021] provide semi-automatic layout optimisations, but are quite limited. Unboxed constructors [Colin et al. 2018; Keller et al. 2010] allow for manual optimisations, but prevent the use of nice high-level constructs, falling back to a C-like programming style. By contrast, our approach allows using only a high-level view, while giving full control over memory layout.

*Intermediate Representation.* We use a Destination-Passing Style [Shaikhha et al. 2017] representation in *A-normal form* [2023]. This provides us precise control over memory management and input/output arguments, and could enable further memory improvements, such as using stack allocation when appropriate and applying tail-call modulo cons [Bour et al. 2021]. Another avenue would naturally be to use Continuation-Passing Style [Appel 1992], notably to simplify handling of recursive calls in Section 7.6. This is in line with numerous compilers for functional languages [Hall et al. 1992; Vincent Laviron 2023] and easily allows moving to SSA representations such as Rust's MIR and LLVM.

CONCLUSION

We presented a unified compilation procedure for constructors and destructors of Algebraic Data Types using a Destination-Passing Style intermediate representation. Our work allows providing arbitrary memory layouts for ADTs and compiles high-level code to low-level programs accordingly. In the future, we hope to investigate memory management strategies, for instance following Lorenzen et al. [2023].
language-integrated constructs such as pattern matching. They also provide far less optimisations
than what we propose.

LoCal [Vollmer et al. 2019] and Gibbon [Koparkar et al. 2021], on the other hand, provide
DSLs tailored to describe and manipulate low-level and serialised representations. Their memory
layouts are less flexible than what we presented, making it impossible to provide truly customised
representations, but allowing them numerous powerful optimisations we do not provide, such as
leveraging parallelism. We hope to combine our approaches in the future.

Finally, some general-purpose languages provide ways to improve data layout. Rust's niches [RFC: Alignment niches for references types 2021] provide semi-automatic layout optimisations, but are quite limited. Unboxed constructors [Colin et al. 2018; Keller et al. 2010] allow for manual optimisations, but prevent the use of nice high-level constructs, falling back to a C-like programming style. By contrast, our approach allows using only a high-level view, while giving full control over memory layout.

*Intermediate Representation.* We use a Destination-Passing Style [Shaikhha et al. 2017] representation in *A-normal form* [2023]. This provides us precise control over memory management and input/output arguments, and could enable further memory improvements, such as using stack allocation when appropriate and applying tail-call modulo cons [Bour et al. 2021]. Another avenue would naturally be to use Continuation-Passing Style [Appel 1992], notably to simplify handling of recursive calls in Section 7.6. This is in line with numerous compilers for functional languages [Hall et al. 1992; Vincent Laviron 2023] and easily allows moving to SSA representations such as Rust's MIR and LLVM.

CONCLUSION

We presented a unified compilation procedure for constructors and destructors of Algebraic Data Types using a Destination-Passing Style intermediate representation. Our work allows providing arbitrary memory layouts for ADTs and compiles high-level code to low-level programs accordingly. In the future, we hope to investigate memory management strategies, for instance following Lorenzen et al. [2023].
## REFERENCES

* A-normal form. https://en.wikipedia.org/w/index.php?title=A-normal_form&oldid=1121147927. [Online; accessed 19-February-2023]. (2023).

* AoS and SoA. https://en.wikipedia.org/w/index.php?title=AoS_and_SoA&oldid=1068565041. [Online; accessed 22-February-2023]. (2023).

* Andrew W. Appel. 1992. *Compiling with Continuations*. Cambridge University Press. ISBN: 0-521-41695-7.

* Lennart Augustsson. 1985. "Compiling pattern matching". In: *Functional Programming Languages and Computer Architecture*. Ed. by Jean-Pierre Jouannaud. Springer Berlin Heidelberg, Berlin, Heidelberg, 368–381. ISBN: 978-3-540-39677-2.

* Thais Baudon, Gabriel Radanne, and Laure Gonnord. Aug. 2023. "Bit-Stealing Made Legal: Compilation for Custom Memory Representations of Algebraic Data Types". Proc. ACM Program. Lang., 7, ICFP, (Aug. 2023). DOI: 10.1145/3607858.

* Frédéric Bour, Basile Clément, and Gabriel Scherer. 2021. "Tail Modulo Cons". CoRR, abs/2102.09823. https://arxiv.org/abs/2102.09823 arXiv: 2102.09823.

* Rod M. Burstall, David B. MacQueen, and Donald Sannella. 1980. "HOPE: An Experimental Applicative Language". In: *Proceedings of the 1980 LISP Conference, Stanford, California, USA, August 25-27, 1980*. ACM, 136–143. DOI: 10.1145/800087.802799.

* Zilin Chen, Ambroise Lafont, Liam O'Connor, Gabriele Keller, Craig McLaughlin, Vincent Jackson, and Christine Rizkallah. Jan. 2023. "Dargent: A Silver Bullet for Verified Data Layout Refinement". Proc. ACM Program. Lang., 7, POPL, (Jan. 2023). DOI: 10.1145/3571240.

* Simon Colin, Rodolphe Lepigre, and Gabriel Scherer. 2018. "Unboxing Mutually Recursive Type Definitions in OCaml". arXiv preprint arXiv:1811.02300.

* Cordelia V. Hall, Kevin Hammond, Will Partain, Simon L. Peyton Jones, and Philip Wadler. 1992. "The Glasgow Haskell Compiler: A Retrospective". In: *Functional Programming, Glasgow 1992, Proceedings of the 1992 Glasgow Workshop on Functional Programming, Ayr, Scotland, UK, 6-8 July 1992* (Workshops in Computing). Ed. by John Launchbury and Patrick M. Sansom. Springer, 62–71. DOI: 10.1007/978-1-4471-3215-8_6.

* Gabriele Keller, Manuel M. T. Chakravarty, Roman Leshchinskiy, Simon L. Peyton Jones, and Ben Lippmeier. 2010. "Regular, shape-polymorphic, parallel arrays in Haskell". In: *Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010*. Ed. by Paul Hudak and Stephanie Weirich. ACM, 261–272. DOI: 10.1145/1863543.1863582.

* Chaitanya Koparkar, Mike Rainey, Michael Vollmer, Milind Kulkarni, and Ryan R. Newton. 2021. "Efficient Tree-Traversals: Reconciling Parallelism and Dense Data Representations". Proc. ACM Program. Lang., 5, ICFP. DOI: 10.1145/3473596.

* Anton Lorenzen, Daan Leijen, and Wouter Swierstra. Aug. 2023. "FP²: Fully in-Place Functional Programming". Proc. ACM Program. Lang., 7, ICFP, (Aug. 2023). DOI: 10.1145/3607840.

* Luc Maranget. 2008. "Compiling pattern matching to good decision trees". In: *Proceedings of the ACM Workshop on ML, 2008, Victoria, BC, Canada, September 21, 2008*. Ed. by Eijiro Sumii. ACM, 35–46. DOI: 10.1145/1411304.1411311.

* Luc Maranget. 2007. "Warnings for pattern matching". J. Funct. Program., 17, 3, 387–421. DOI: 10.1017/S0956796807006223. RFC: Alignment niches for references types. https://github.com/rust-lang/rfcs/pull/3204. (2021).

* Peter Sestoft. 1996. "ML pattern match compilation and partial evaluation". In: *Partial Evaluation*. Springer, 446–464.

* Amir Shaikhha, Andrew Fitzgibbon, Simon Peyton Jones, and Dimitrios Vytiniotis. 2017. "Destination-Passing Style for Efficient Memory Management". In: *Proceedings of the 6th ACM SIGPLAN International Workshop on Functional High-Performance Computing (FHPC 2017)*. Association for Computing Machinery, Oxford, UK, 12–23. ISBN: 9781450351812. DOI: 10.1145/3122948.3122949.

* Nikhil Swamy et al. 2022. "Hardening attack surfaces with formally proven binary format parsers". In: *PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13-17, 2022*. Ed. by Ranjit Jhala and Isil Dillig. ACM, 31–45. DOI: 10.1145/3519939.3523708.

* [SW exc.] Linus Torvalds, "Red-Black Trees in Linux", from *The Linux Kernel* version 6.2, 2023. LIC: GPL-2.0 WITH Linux-syscall-note. URL: https://github.com/torvalds/linux, SWHID: (swh:1:cnt:45b6ecde3665aa744f790cd915445fe07595181c;origin=https://github.com/torvalds/linux;visit=swh:1:snp:de81d8ff32247a7edaa935cf0468bf16237d25c5;anchor=swh:1:rel:32758e7a720e4752a824c6062e75f107314e5598;path=/include/linux/rbtree_types.h).

* Mark Shinwell Vincent Laviron Pierre Chambart. 2023. "Efficient OCaml Compilation with Flambda 2". OCaml. https://icfp23.sigplan.org/details/ocaml-2023-papers/8/Efficient-OCaml-compilation-with-Flambda-2.

* Michael Vollmer, Chaitanya Koparkar, Mike Rainey, Laith Sakka, Milind Kulkarni, and Ryan R. Newton. 2019. "LoCal: a language for programs operating on serialized data". In: *Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019*. Ed. by Kathryn S. McKinley and Kathleen Fisher. ACM, 48–62. DOI: 10.1145/3314221.3314631.

* Andrew Waterman, Yunsup Lee, David A. Patterson, and Krste Asanović. Dec. 2019. *The RISC-V Instruction Set Manual, Volume I: User-Level ISA, Version 20191213*. Tech. rep. RISCV fundation, (Dec. 2019).
REFERENCES

A-normal form. https://en.wikipedia.org/w/index.php?title=A-normal_form&oldid=1121147927. [Online; accessed 19-February-2023]. (2023).

AoS and SoA. https://en.wikipedia.org/w/index.php?title=AoS_and_SoA&oldid=1068565041. [Online; accessed 22-February-2023]. (2023).

Andrew W. Appel. 1992. *Compiling with Continuations*. Cambridge University Press. ISBN: 0-521-41695-7.

Lennart Augustsson. 1985. "Compiling pattern matching". In: *Functional Programming Languages and Computer Architecture*. Ed. by Jean-Pierre Jouannaud. Springer Berlin Heidelberg, Berlin, Heidelberg, 368–381. ISBN: 978-3-540-39677-2.

Thais Baudon, Gabriel Radanne, and Laure Gonnord. Aug. 2023. "Bit-Stealing Made Legal: Compilation for Custom Memory Representations of Algebraic Data Types". Proc. ACM Program. Lang., 7, ICFP, (Aug. 2023). DOI: 10.1145/3607858.

Frédéric Bour, Basile Clément, and Gabriel Scherer. 2021. "Tail Modulo Cons". CoRR, abs/2102.09823. https://arxiv.org/abs/2102.09823 arXiv: 2102.09823.

Rod M. Burstall, David B. MacQueen, and Donald Sannella. 1980. "HOPE: An Experimental Applicative Language". In: *Proceedings of the 1980 LISP Conference, Stanford, California, USA, August 25-27, 1980*. ACM, 136–143. DOI: 10.1145/800087.802799.

Zilin Chen, Ambroise Lafont, Liam O'Connor, Gabriele Keller, Craig McLaughlin, Vincent Jackson, and Christine Rizkallah. Jan. 2023. "Dargent: A Silver Bullet for Verified Data Layout Refinement". Proc. ACM Program. Lang., 7, POPL, (Jan. 2023). DOI: 10.1145/3571240.

Simon Colin, Rodolphe Lepigre, and Gabriel Scherer. 2018. "Unboxing Mutually Recursive Type Definitions in OCaml". *arXiv preprint arXiv:1811.02300*.

Cordelia V. Hall, Kevin Hammond, Will Partain, Simon L. Peyton Jones, and Philip Wadler. 1992. "The Glasgow Haskell Compiler: A Retrospective". In: *Functional Programming, Glasgow 1992, Proceedings of the 1992 Glasgow Workshop on Functional Programming, Ayr, Scotland, UK, 6-8 July 1992* (Workshops in Computing). Ed. by John Launchbury and Patrick M. Sansom. Springer, 62–71. DOI: 10.1007/978-1-4471-3215-8_6.

Gabriele Keller, Manuel M. T. Chakravarty, Roman Leshchinskiy, Simon L. Peyton Jones, and Ben Lippmeier. 2010. "Regular, shape-polymorphic, parallel arrays in Haskell". In: *Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010*. Ed. by Paul Hudak and Stephanie Weirich. ACM, 261–272. DOI: 10.1145/1863543.1863582.

Chaitanya Koparkar, Mike Rainey, Michael Vollmer, Milind Kulkarni, and Ryan R. Newton. 2021. "Efficient Tree-Traversals: Reconciling Parallelism and Dense Data Representations". Proc. ACM Program. Lang., 5, ICFP. DOI: 10.1145/3473596.

Anton Lorenzen, Daan Leijen, and Wouter Swierstra. Aug. 2023. "FP²: Fully in-Place Functional Programming". Proc. ACM Program. Lang., 7, ICFP, (Aug. 2023). DOI: 10.1145/3607840.

Luc Maranget. 2008. "Compiling pattern matching to good decision trees". In: *Proceedings of the ACM Workshop on ML, 2008, Victoria, BC, Canada, September 21, 2008*. Ed. by Eijiro Sumii. ACM, 35–46. DOI: 10.1145/1411304.1411311.

Luc Maranget. 2007. "Warnings for pattern matching". J. Funct. Program., 17, 3, 387–421. DOI: 10.1017/S0956796807006223. RFC: Alignment niches for references types. https://github.com/rust-lang/rfcs/pull/3204. (2021).

Peter Sestoft. 1996. "ML pattern match compilation and partial evaluation". In: *Partial Evaluation*. Springer, 446–464.

Amir Shaikhha, Andrew Fitzgibbon, Simon Peyton Jones, and Dimitrios Vytiniotis. 2017. "Destination-Passing Style for Efficient Memory Management". In: *Proceedings of the 6th ACM SIGPLAN International Workshop on Functional High-Performance Computing (FHPC 2017)*. Association for Computing Machinery, Oxford, UK, 12–23. ISBN: 9781450351812. DOI: 10.1145/3122948.3122949.

Nikhil Swamy et al. 2022. "Hardening attack surfaces with formally proven binary format parsers". In: *PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13-17, 2022*. Ed. by Ranjit Jhala and Isil Dillig. ACM, 31–45. DOI: 10.1145/3519939.3523708.

[SW exc.] Linus Torvalds, "Red-Black Trees in Linux", from *The Linux Kernel* version 6.2, 2023. LIC: GPL-2.0 WITH Linux-syscall-note. URL: https://github.com/torvalds/linux, SWHID: (swh:1:cnt:45b6ecde3665aa744f790cd915445fe07595181c;origin=https://github.com/torvalds/linux;visit=swh:1:snp:de81d8ff32247a7edaa935cf0468bf16237d25c5;anchor=swh:1:rel:32758e7a720e4752a824c6062e75f107314e5598;path=/include/linux/rbtree_types.h).

Mark Shinwell Vincent Laviron Pierre Chambart. 2023. "Efficient OCaml Compilation with Flambda 2". OCaml. https://icfp23.sigplan.org/details/ocaml-2023-papers/8/Efficient-OCaml-compilation-with-Flambda-2.

Michael Vollmer, Chaitanya Koparkar, Mike Rainey, Laith Sakka, Milind Kulkarni, and Ryan R. Newton. 2019. "LoCal: a language for programs operating on serialized data". In: *Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019*. Ed. by Kathryn S. McKinley and Kathleen Fisher. ACM, 48–62. DOI: 10.1145/3314221.3314631.

Andrew Waterman, Yunsup Lee, David A. Patterson, and Krste Asanović. Dec. 2019. *The RISC-V Instruction Set Manual, Volume I: User-Level ISA, Version 20191213*. Tech. rep. RISCV fundation, (Dec. 2019).
# A FOCUSING AND SPECIALISATION

We now give full details of the definition of focusing and specialisation.

Focusing in Types and Layouts. “Focusing”, defined in Fig. 13 allows to focus on a specific part of a type or layout, according to a given path. Focus in the high-level language is denoted **focus** ($\pi, \theta$) where $\theta$ is a type, an expression, a provenance, or another path, and returns an object of the same kind. It simply follows the syntax to extract the subterm at position $\pi$. For instance, we can consider “the part that is relevant to .Sw.0” in the type $\tau_{\text{RISC-V}}$(Example 3.1):

$$ \mathbf{focus} (.Sw.0, \tau_{\text{RISC-V}}) = \mathbf{focus} (.Sw.0, \text{Sw}(\tau_{\text{reg}}, \tau_{\text{reg}}, I_{12})) = \tau_{\text{reg}} $$

Layout focusing (Fig. 14), denoted $\widehat{\mathbf{focus}} (\hat{\pi}, \hat{\tau})$, similarly extracts the layout located at position $\hat{\pi}$ within the parent layout $\hat{\tau}$. It is undefined on splits. For instance, $\widehat{\mathbf{focus}} (.[7 : 5], \hat{\tau}_{\text{Sw}}) = (.\text{Sw}.0 \text{ as } \hat{\tau}_{\text{reg}})$.

$$ \mathbf{focus} (\epsilon, x) = x $$

$$ \mathbf{focus} (.i, \langle x_1, \dots, x_n \rangle) = x_i $$

$$ \mathbf{focus} (\pi, \_) = \_ $$

$$ \mathbf{focus} (.K_i, K_1(x_1) + \dots + K_n(x_n)) = x_i $$

<caption>Fig. 13. Type Focusing.</caption>

$$ \widehat{\mathbf{focus}} (\epsilon, \widehat{\tau}) = \widehat{\tau} $$

$$ \widehat{\mathbf{focus}} (.i, \{\widehat{\tau}_1, \dots, \widehat{\tau}_n\}) = \widehat{\tau}_i $$

$$ \widehat{\mathbf{focus}} (.[o_k : \ell_k], \_ \bowtie 1 \le i \le n [o_i : \ell_i] : \widehat{\tau}_i) = \widehat{\tau}_k $$

$$ \widehat{\mathbf{focus}} (.[o_k : \ell_k], \&_l (\widehat{\tau}) \bowtie 1 \le i \le n [o_i : \ell_i] : \widehat{\tau}_i) = \widehat{\tau}_k $$

$$ \widehat{\mathbf{focus}} (\*, \&_l (\widehat{\tau}) \bowtie 1 \le i \le n [o_i : \ell_i] : \widehat{\tau}_i) = \widehat{\tau} $$

<caption>Fig. 14. Layout Focusing.</caption>

Layout and Type Specialisation. “Specialisation”, defined in Fig. 15 filters a type or a layout to exclude parts which are incompatible with a given provenance. Type specialisation, denoted $\tau/p$, is a simple syntactic filter that discards irrelevant constructors. For instance,

$$ \tau_{\text{RISC-V}} / \text{Sw}(\_, \_, \_) = \text{Sw}(\tau_{\text{reg}}, \tau_{\text{reg}}, I_{12}). $$

Layout specialisation, denoted $\widehat{\tau}/p$ (Fig. 16), is more complex: it removes all splits from $\widehat{\tau}$ (up to fragments) by filtering out branches whose provenance set excludes $p$. It returns a list of pairs of the form $(p' \mapsto \widehat{\tau}')$, where $p'$ is a refined version of $p$ and $\widehat{\tau}'$ is the restriction of $\widehat{\tau}$ to values that match $p'$. For instance, $\widehat{\tau}_{\text{RISC-V}} / \text{Sw}(\_, \_, \_)$ returns a single pair $(\text{Sw}(\_, \_, \_) \mapsto \widehat{\tau}_{\text{Sw}})$, and specialisation according to the wildcard provenance lists all possible refinement pairs of a layout:

$$ \widehat{\tau}_{\text{RISC-V}} / \_ = \left\{ \begin{array}{l} (\text{Sw}(\_, \_, \_) \mapsto \widehat{\tau}_{\text{Sw}}), (\text{Add}(\_, \_, \_) \mapsto \widehat{\tau}_{\text{Add}}), \\ (\text{Addi}(\_, \_, \_) \mapsto \widehat{\tau}_{\text{Addi}}), (\text{Jal}(\_, \_, \_) \mapsto \widehat{\tau}_{\text{Jal}}) \end{array} \right\} $$
# A FOCUSING AND SPECIALISATION

We now give full details of the definition of focusing and specialisation.

Focusing in Types and Layouts. “Focusing”, defined in Fig. 13 allows to focus on a specific part of a type or layout, according to a given path. Focus in the high-level language is denoted **focus** ($\pi, \theta$) where $\theta$ is a type, an expression, a provenance, or another path, and returns an object of the same kind. It simply follows the syntax to extract the subterm at position $\pi$. For instance, we can consider “the part that is relevant to .Sw.0” in the type $\tau_{\text{RISC-V}}$(Example 3.1):

$$ \mathbf{focus} (.Sw.0, \tau_{\text{RISC-V}}) = \mathbf{focus} (.Sw.0, \text{Sw}(\tau_{\text{reg}}, \tau_{\text{reg}}, I_{12})) = \tau_{\text{reg}} $$

Layout focusing (Fig. 14), denoted $\widehat{\mathbf{focus}} (\hat{\pi}, \hat{\tau})$, similarly extracts the layout located at position $\hat{\pi}$ within the parent layout $\hat{\tau}$. It is undefined on splits. For instance, $\widehat{\mathbf{focus}} (.[7:5], \hat{\tau}_{\text{Sw}}) = (.\text{Sw}.0 \text{ as } \hat{\tau}_{\text{reg}})$.

$$ \mathbf{focus} (\epsilon, x) = x $$

$$ \mathbf{focus} (.i, \langle x_1, \dots, x_n \rangle) = x_i $$

$$ \mathbf{focus} (\pi, \_) = \_ $$

$$ \mathbf{focus} (.K_i, K_1(x_1) + \dots + K_n(x_n)) = x_i $$

<caption>Fig. 13. Type Focusing.</caption>

$$ \widehat{\mathbf{focus}} (\epsilon, \widehat{\tau}) = \widehat{\tau} $$

$$ \widehat{\mathbf{focus}} (.i, \{\widehat{\tau}_1, \dots, \widehat{\tau}_n\}) = \widehat{\tau}_i $$

$$ \widehat{\mathbf{focus}} (.[o_k : \ell_k], \_ \widehat{\perp} 1 \le i \le n [o_i : \ell_i] : \widehat{\tau}_i) = \widehat{\tau}_k $$

$$ \widehat{\mathbf{focus}} (.[o_k : \ell_k], \&_l (\widehat{\tau}) \widehat{\perp} 1 \le i \le n [o_i : \ell_i] : \widehat{\tau}_i) = \widehat{\tau}_k $$

$$ \widehat{\mathbf{focus}} (\*, \&_l (\widehat{\tau}) \widehat{\perp} 1 \le i \le n [o_i : \ell_i] : \widehat{\tau}_i) = \widehat{\tau} $$

<caption>Fig. 14. Layout Focusing.</caption>

Layout and Type Specialisation. “Specialisation”, defined in Fig. 15 filters a type or a layout to exclude parts which are incompatible with a given provenance. Type specialisation, denoted $\tau/p$, is a simple syntactic filter that discards irrelevant constructors. For instance,

$$ \tau_{\text{RISC-V}} / \text{Sw}(\_, \_, \_) = \text{Sw}(\tau_{\text{reg}}, \tau_{\text{reg}}, I_{12}). $$

Layout specialisation, denoted $\widehat{\tau}/p$ (Fig. 16), is more complex: it removes all splits from $\widehat{\tau}$ (up to fragments) by filtering out branches whose provenance set excludes $p$. It returns a list of pairs of the form $(p' \mapsto \widehat{\tau}')$, where $p'$ is a refined version of $p$ and $\widehat{\tau}'$ is the restriction of $\widehat{\tau}$ to values that match $p'$. For instance, $\widehat{\tau}_{\text{RISC-V}} / \text{Sw}(\_, \_, \_) \text{ returns a single pair } (\text{Sw}(\_, \_, \_) \mapsto \widehat{\tau}_{\text{Sw}})$, and specialisation according to the wildcard provenance lists all possible refinement pairs of a layout:

$$ \widehat{\tau}_{\text{RISC-V}} / \_ = \left\{ \begin{array}{l} (\text{Sw}(\_, \_, \_) \mapsto \widehat{\tau}_{\text{Sw}}), (\text{Add}(\_, \_, \_) \mapsto \widehat{\tau}_{\text{Add}}), \\ (\text{Addi}(\_, \_, \_) \mapsto \widehat{\tau}_{\text{Addi}}), (\text{Jal}(\_, \_, \_) \mapsto \widehat{\tau}_{\text{Jal}}) \end{array} \right\} $$