: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down
to WebAssembly

Zoe Paraskevopoulou

Northeastern University

Michael Fitzgibbons

Northeastern University

Noble Mushtak

Northeastern University

Michelle Thalakottur

Northeastern University

Jose Sulaiman Manzur

Northeastern University

Amal Ahmed

Northeastern University

Safe, shared-memory interoperability between languages with
different type systems and memory-safety guarantees is an intricate problem as
crossing language boundaries may result in memory-safety violations.

In this paper, we present RichWasm, a novel richly typed
intermediate language designed to serve as a compilation target for
typed high-level languages with different memory-safety guarantees.

RichWasm is based on WebAssembly and enables safe shared-memory
interoperability by incorporating a variety of type features
that support fine-grained memory ownership and sharing.

RichWasm is rich enough to serve as a typed compilation target for
both typed garbage-collected languages and languages with an
ownership-based type system and manually managed memory.

We demonstrate this by providing compilers from core ML and
, a type-safe language with strong updates <cit.>, to RichWasm.

RichWasm is compiled to regular Wasm,

§ INTRODUCTION

WebAssembly <cit.> (Wasm) is a portable binary format that enables
almost-native execution speed for a variety of languages.

With around 40 languages compiling to Wasm, the WebAssembly platform
has huge potential to serve as a platform for language interoperability.

This potential has been recognized for some time, but there are two
impediments. The first is that Wasm takes an all-or-nothing approach to sharing
memory. Each Wasm module has its own memory. If it wants to share a data
structure in its memory with another module, that effectively leaves all of
its memory exposed to the other module, potentially allowing adversarial code to
access and modify arbitrary parts of that memory via pointer arithmetic.

The multiple memories proposal <cit.> addresses this by allowing
modules to have multiple independent memories and only share some of them while
keeping others private.

A module can thus protect its private data by placing it in a memory that is not
shared, but this mechanism is too coarse-grained, in both a spatial
and temporal sense: it does not allow fine-grained sharing of only one data
structure in a memory or sharing for only a while and then allowing access to be revoked.

The second impediment is that Wasm has only low-level types (32- and 64-bit
integers and floats), so when modules from different languages need to
communicate, there is a question of how to exchange high-level values. The
Interface Types proposal <cit.> aimed to address this by
introducing a set of high-level “interface types” (e.g., char, list, record,
variant, and more can be encoded) that can be used to communicate across

However, the Interface Types proposal and its successor, the Component Model
proposal <cit.>, support only “shared-nothing” interoperability,
requiring that values be copied across language boundaries when necessary. This
ensures memory safety but comes with runtime overhead for copying.

In this paper, we propose , a richly typed intermediate language (IL)
based on WebAssembly. Unlike existing proposals in the Wasm ecosystem, supports safe, fine-grained, shared-memory interoperability across Wasm modules,
and it is also motivated by a desire to provide a platform atop which language
implementors can easily develop safe FFIs.

A particular goal is to enable statically detecting memory safety violations
that happen across source-language boundaries and thus cannot be detected by the
source type system.

For instance, if we mix a type-safe garbage-collected language such as OCaml
with a type-safe non-GC'd language such as Rust and allow them to share memory,
violations may include Rust freeing some garbage-collected memory passed to it
from OCaml, or OCaml copying a mutable reference from Rust that Rust considers
uniquely owned.

We wish to allow source-language designers to add inter-language communication
through a simple foreign-function interface that requires no changes to the
existing source type systems and minimal changes to the syntax of their

Then the source-language modules are compiled separately to modules. Any
potentially problematic interaction between modules will fail to type
check. Thus, type checking at the level guarantees cross-module type and
memory safety.

Overview of . supports both a garbage-collected memory
and a manually managed memory so we can compile languages with these very
different memory management strategies to and reason about the
highly intricate problems that arise when sharing memory across such languages.

At the core of 's type system are capability
types in the style of  <cit.>, which is a linear language with
locations and safe strong updates. A key idea in was that when we
allocate a new reference and initialize it with a value
of type $\tau$, we get back an existential package $\exists
\rho. \mathsf{!Ptr~}\rho \otimes \mathsf{Cap~}\rho~\tau$ that says that there
exists some location $\rho$ and we now have an unrestricted (copyable) pointer
to that location and we have a linear capability that tells us the type of value
currently stored at that location. This linear capability is essentially an
ownership token required to access the reference — the capability must be
provided to read from, write to, or free the location.
In , we similarly have linear capabilities that represent (allow
access to) uniquely owned memory and support strong updates. But we also have
unrestricted capabilities, which represent (allow access to)
garbage-collected memory and are analogous to ML references in that they only
support type-preserving updates. Unlike , capability types in can
provide either read-only access or read-write access.

Formally, has a substructural type system, realized via two qualifiers,
linear and unrestricted, that annotate pretypes. In addition to capability
pretypes, supports polymorphism, recursive types, variants, structs,
arrays and existential types. Unlike
, which assumes a reference cell can hold a value of any size,
has a low-level memory model like Wasm's, where each memory is simply a
sequence of bytes and we must allocate data structures in the “flat” memory.
[In WebAssembly-speak, what we refer to as “flat” memory, i.e.,
This leads to an important novelty in the type system, which must keep track of
the size of memory slots and disallow strong updates that attempt to store a
larger value in that slot. Hence, capability types in track the size
of the memory slot originally allocated and type variables $\alpha$ must be
annotated with a size bound that indicates the maximum size of the type
that $\alpha$ can be instantiated with.

is rich enough to serve as a typed compilation target for both
typed garbage-collected languages and languages with an
ownership-based type system and manually managed memory.  We
demonstrate this by implementing compilers from core ML and to

can be compiled to regular Wasm, providing a pathway to realistic
use in many environments.

We have formalized in Coq and we have proved type safety
(progress and preservation) for the type system.

Situating . Before we dive into the details of , we
would like to make clear where is sits relative to two other pieces of related
work. The first is the Wasm Component Model, though we've already discussed the
salient difference above, namely “shared-nothing” vs. “fine-grained
shared-memory” interoperability. But there are additional similarities and
differences. The Component Model is intended to be a part of the WebAssembly
ecosystem but not part of the core Wasm spec and the same is true of
RichWasm. The Component Model provides a means to organize
Wasm modules into components and instrument core Wasm modules so they can take
advantage of higher-level types when communicating across components, while
RichWasm supports higher-level types and then compiles (or lowers) them to
Wasm. On the other hand, while the Component Model implementation employs
dynamic techniques to assure safety when it comes to features like resources and
handles, RichWasm uses static enforcement.

The second is recent work on safe FFIs by Patterson et al. <cit.>
who proposed a framework for design and verification of safe FFIs. Their main
insight is that language designers should build a model of source-level types as
sets of
target-level terms. Then for all conversions their FFI permits, from a type in
one language say $\tau_A$ to a type in the other say $\tau_B$, the target-level
glue code they write to implement that conversion can be shown to be sound if:
given target code that behaves like $\tau_A$, the conversion produces target
code that behaves like $\tau_B$.  This is a perfectly reasonable recipe for
designing and verifying safe FFIs between languages that compile directly to
Wasm. However, we would argue that it is a rather heavyweight recipe, one that
requires FFI designers to know how to construct semantic models that would then
guide their thinking. With , we would like to provide support for compiler
writers who don't know how to build semantic models and aren't interested in
doing formal verification of FFIs. To that end, we've developed a richly typed IR
capable of detecting unsafe interoperability via type checking of compiled
code. To take advantage of this, compiler writers must implement type-preserving
compilers to , a much easier task than defining a target-level model of
source-language types. Whenever the language designer wants to support
additional FFI functionality, they simply have to extend their compiler and see
if any additional conversions they allow result in type-checking errors at the

Contributions. Our central contribution is , a typed
IL built on top of WebAssembly that is designed to serve as a
useful platform for safe FFI design.

* supports an advanced substructural type system with capabilities
and size tracking that enables static assurance of safe, fine-grained shared
memory interoperability in a language with a low-level memory model (i.e.,
“flat” memory). The type system allows precisely tracking memory
ownership and sharing, and avoids memory safety violations even when sharing
memory across languages with garbage collection and manual memory management
(<ref> and <ref>).

* We have formalized in Coq and proved type safety.

* We have compilers from core ML and to
and a simple FFI between them that allows us to compile interoperating programs to (<ref>).

* We have a compiler from to WebAssembly that allows us to run
programs in all hosts of WebAssembly (<ref>).

§ OVERVIEW

In this section, we will give an overview of the language,
presenting its types and syntax. Then we will provide an example of
interoperation of and ML show how can statically detect
safety violations.

First, let's consider a small example to get a sense for the sort of errors
can catch.

In Fig. <ref> we have a GC'd program which provides two functions:
an identity function on integer references, which stashes a copy of the reference, and a
function which can return the stashed copy.

Our manually managed program first creates a reference, passes it to the $\tt{stash}$
function, and frees the returned reference.

Next, the linear program retrieves the stashed reference and attempts to free
that, resulting in a double free.

If compiled naively, 's type system will first complain that $\tt{stash}$
requires an unrestricted reference, while it is called with a linear reference.

If $\tt{stash}$ were compiled to take a linear reference, would not admit
the function since it duplicates a linear value.

let c = ref (ref 0) in
fun stash (r : Ref Int) = c := r; r in
fun get_stashed (() : Unit) = !c

garbage collected program

free (ml.stash (new 42));
free (ml.get_stashed ()) (* CRASH *)

manually managed program

Unsafe interoperability

and Wasm. While is coherent
without comparison to Wasm, readers who are familiar with Wasm will note the
parallel structure of the two languages.

Existing constructs from Wasm are extended to support 's new types, while
continuing to fulfill their original purpose.

For instance, Wasm has "local variables": a location which lives for the duration
of a function call and can store one numeric type. has an analagous concept.
However, also has strong tools for reasoning about sizes and linearity.
This allows us to use locals even more effectively, strongly updating them
while guaranteeing that there will be space for any value we
store and that we only duplicate or ignore values which are not linear.

The largest departure from Wasm is in 's treatment of memory. Because we
want to support strong memory invariants, supports a series of structured
memory types, rather than the raw sequence of numeric types present in Wasm.

Wasm's unfettered access to the memory makes it impossible to
guarantee any invariants about one's memory layout when linking with
other code. We no longer support arbitrary memory operations, but
thanks to the same size and linearity reasoning tools that give us
greater control over locals, we still have control over memory layouts
and sharing, without the burden of losing invariants when linking with
other code.

§.§ Syntax

In Fig. <ref> we give a full account of types and
programs. The highlighted constructs are new in and not present
in Wasm.  We start explaining the syntax of the language from the
top-level structures.

abstract syntax

Modules. As in Wasm, the top-level unit of program is a module.
A module consists of code in the form of a list of functions and data in the
form of a list of global declarations that can be mutable or immutable.

Each module also has a table that, as in WebAssembly, stores references to
functions which facilitate indirect calls.

Functions, globals, and tables can be exported, making them visible to
other modules for import.

Functions. Functions are sequences of instructions, taking as input
a sequence of values and returning a sequence of values.

The function type, $\Wfty$, can be polymorphic over various entities
of the type system: memory locations, sizes, qualifiers (which
describe the linearity of a value), and types.

Unlike Wasm, local variables  are not tied to a particular type, so instead they
are defined by their slot size ($\Wsz$) and initialized with an unrestricted
unit value.

Locals may take on linear types during evaluation, and upon use will
be returned to the unrestricted unit type to avoid duplication of a
linear value.

Value types. The types of values consist of a pretype
that is annotated with a qualifier. Concrete qualifiers can be linear
($\Wlin$) or unrestricted ($\Wunr$) and indicate whether a value must
be treated linearly. Qualifiers can also be abstract variables bound in function

Qualifiers are ordered with $\Wunr \Wqualless \Wlin$. This ordering
helps us put restrictions on abstract types bound in polymorphic,
existential, or recursive types.

Simple pretypes include unit, numeric types (32 or 64 bit signed and
unsigned integers and floats), and tuples $\WPgroup{\many{\Wtau}}$.

Next we have references, pointers, and capabilities. Pointers are used
to access a memory location and capabilities provide ownership to a
memory location. References represent the pair of a capability and a
pointer. Capabilities are a type-level reasoning tool and are erased
in programs compiled to Wasm. The ability to split a reference
into a capability and a pointer allows a program to separate its static notion of ownership
from its runtime data layout. If pointers to a location are stashed in
separate parts of a large data strucutre, ownership (in the form of a
capability) can be stored with one of them and then temporarily borrowed
by the other location by moving the capability. Since capabilities will
be erased upon compilation to Wasm, this transfer of ownership
satisifies the type system without incurring any runtime cost.

The type $\WPref{\Wrw}{\Wloc}{\Whty}$ is a reference to a location
$\Wloc$ that contains a heap type $\Whty$ and provides read or
read-write priviledge ($\Wrw$) to it. A capability carries similar
information, while a pointer is annotated only with the location that
it points to.

The type $\WPown{\Wloc}$ is an ownership token that represents
write ownership of a location. A read-write capability can be temporarily
split into a read-only capability and an ownership token and later

In order to represent recursive data structures, has
isorecursive types. The type $\WPrec{\Wqual}{\Wptyvar}{\Wtau}$ is
recursive over $\Wptyvar$. The constraint $q \Wqualless$ asserts that
this recursive type will only be unfolded into locations with qualifiers
greater than or equal to the qualifier $q$. The need for such a constraint
is discussed further below.

To facilitate location abstraction, which is necessary to statically
represent references to memory locations, has existential types
over locations $\WPexists{\Wlocvar}{\Wtau}$. For instance,
$\WPexists{\Wlocvar}{\WPref{\Wrwrw}{\Wlocvar}}{\Whty}$ represents a
read-write reference to a statically unknown location with heap type

Wasm allows "indirect" function calls, using a runtime value to lookup
a function in a table. We use the type $\WPcoderef{\Wfty}$ to
represent a code pointer to some function in that table with type

Lastly, a pretype can be a pretype variable $\Wptyvar$, referring to
a universal, existential, or recursive binding site.

Heap types and memory model. The memory model of consists
of two global flat memories: the linear memory and the unrestricted
memory. The linear memory is manually managed and references to it
must be treated linearly. The unrestricted memory is garbage collected
and stores ML-like references.

Unlike Wasm, where memories are essentially byte arrays, in memories store high-level structured data. Heap types can be variants,
structs, arrays, and existential packages abstracting over types.

A variant type $\WHvariant{\many{\Wtau}}$ describes a heap value
that can contain more than one kind of value, where $\many{\Wtau}$
is a list containing the type for each case of the variant.

An array type $\WHarray{\Wtau}$ is a variable-length array containing
values of type $\Wtau$.

A struct type $\WHstruct{\many{\Wtau,\ \Wsz}}$ is a record type
with the list $\many{\Wtau,\Wsz}$ indicating the type $\Wtau$ and
the size $\Wsz$ of each field.

Keeping the size of each field is necessary to support strong updates.

Strong updates are necessary when consuming linear struct fields, as
the old value must be replaced with a new value in order to prevent duplication.

An existential heap type $\WHstruct{\many{\Wtau,\ \Wsz}}$
abstracts over a pretype $\Wptyvar$ in a type $\Wtau$. The qualifier
$q$ denotes the minimum qualifier that the pretype should have when it
is used inside the type. The size $sz$ denotes an upper bound for the
size of the abstracted type, which is useful when we want to

Locations are natural numbers that refer either to the unrestricted or
linear memory. Since we have location polymorphism, locations can also be

Function types and polymorphism. Function types are arrow types $\many{\Wtau_1} \rightarrow \many{\Wtau_2}$
that indicate that a function consumes values with types
$\many{\Wtau_1}$ from the stack, and leaves values with types
$\many{\Wtau_2}$ on the stack after its execution.

To facilitate polymorphism, function types can quantify over four
different kinds: locations, sizes, qualifiers, and
pretypes. Quantification over sizes, qualifiers, and pretypes can
impose constraints over the abstracted kind.

Location quantification is most straightforward: function declarations
should be polymorphic over locations since concrete locations are only
available at runtime.

Functions can also be polymorphic over sizes. For instance, projecting
a struct field is an operation that should be agnostic to the size of the
field, therefore the size must be abstracted.

Quantification over sizes can also be subject to constraints. In
particular, the size variable $\Wszvar$ can be upper-bounded and
lower-bounded by some sizes, written $\many{\Wsz} \Wszless \Wszvar
\Wszless \many{\Wsz'}$.

Allowing quantification over sizes to be constrained in this way
allows for richer reasoning about location usage. For instance, if a
function takes two arguments of sizes $\Wszvar_1$ and $\Wszvar_2$ and
places a tuple consisting of the two arguments into a local of size
$\Wszvar_3$, it must be known that $ \Wszvar_1 + \Wszvar_2 \Wszless
\Wszvar_3 $.

In order to be able to write functions that operate on both linear and unrestricted data,
functions can also be polymorphic on qualifiers.

Qualifier quantification can also be subject to the same sort of
contraint as size quantification, in this case written $\many{\Wqual}
\Wqualless \Wqualvar \Wqualless \many{\Wqual'}$.

To see why qualifier constraints are necessary, consider a function
that takes two arguments and constructs a tuple.

The qualifier of the tuple must be greater than the qualifiers on the
values inside the tuple. If this were not the case, we could
have a non-linear tuple which can be duplicated, containing a linear
value which should not be duplicated.

Lastly, we have pretype polymoprhism, which is the usual parametric
polymorphism we find in ML programs. The type constraints are $\Wqual
\Wqualless \Wptyvar^{(c^?)} \Wtyless \Wsz$ where $\Wqual$ is a lower bound for
the qualifier of the pretype, $\Wsz$ an upper bound for its size, and the presence
of $^{c}$ denotes whether this type can contain capabilities.

Type variables having an upper bound on size is straightforwardly useful to demonstrate
that they will fit into locations.

A qualifier lower bound is, however, a bit less intuitive. Keep in
mind that we are quantifying over pretypes and not types, so
any location this pretype variable appears will have a qualifier on it. These
bounds provide two guarantees. Firstly, this pretype variable will
only be substituted into positions with qualifiers greater than or
equal to the bound. Secondly, we can only substitute a pretype in for
such a pretype variable if it would be valid at that qualifier.

To see why this is important, consider an attempt to instantiate the variable in the type
$\Wptyvar^{\Wunr}$ with the tuple pretype $\WPgroup{\WPunit^{\Wlin}}$. This instantiation
would leave us with an unrestricted tuple containing a linear value, a type we just
determined would violate the guarantees of our type system. Having quantifier lower bounds
will guarantee that such instantiations never take place.

Whether or not a type contains capabilities is relevant only for garbage collection and
will be discussed below.

Using polymorphism, we can write the type of a function that projects
a linear field of a singleton struct and replaces it with a value of a
new type, performing a strong update:

\[\forall~\Wlocvar~\Wszvar~\Wptyvar_1~(\Wlin\Wqualless\Wptyvar_2^c\Wtyless\Wszvar),~
\Wptyvar_2^{\Wlin}~(\WPref{\Wrwrw}{\Wlocvar}{\WHstruct{(\Wptyvar_1^{\Wlin},\Wszvar)}})^{\Wlin}
\rightarrow
\Wptyvar_1^{\Wlin}~(\WPref{\Wrwrw}{\Wlocvar}{\WHstruct{(\Wptyvar_2^{\Wlin},\Wszvar)}})^{\Wlin}
\]

The function is polymorphic over the actual location of the struct,
$\Wlocvar$, the size of the struct field, $\Wszvar$, the pretype of
the struct field $\Wptyvar_1$, and the pretype of the new value,
$\Wptyvar_2$, that is going to be put in the struct slot.

The constraints over $\Wptyvar_2$ ensure that it will fit into the slot
of size $\Wszvar$ and can be safely stored in the heap. The qualifier
lower bound ensures that this function can be used on types which must
appear in at least linear positions.

Heap values.
Heap values are variants $\WHVvariant{i}{v}$, where $i$ is tag of
the variant, structs $\WHVstruct{\many{v}}$, arrays
$\WHVarray{i}{\many{v}}$, where $i$ is the size of the array, and
existential packages $\WHVpack{\Wpty}{v}{\Whty}$, where
$\Wpty$ is the pretype witness, $\Whty$ the heap type of the existential
package, and $v$ the value that is being packed.

Values and instructions.
Each type has a corresponding value form. For unit, numeric
types, and tuples, these values are straightforward. References and
pointers are annotated with the memory location they point
to. Capabilities and ownership tokens carry no information and are
computationally irrelevant. We have the typical constructor for
isorecursive types ($\WVfold{v}$). Existential location packages
($\WVmempack{\Wloc}{v}$) contain the packed value as well as the
location witness of the package, used to instantiate abstract
locations in instructions once unpacked.

The value form for function references is
$\WVcoderef{i}{j}{\many{\Wk}}$, where $i$ is the index of the module
instance, $j$ is the index of the function in the function table,

New instructions include instructions for folding and
unfolding recursive types, packing and unpacking existential memory
locations, grouping and ungrouping tuples, joining and spliting
capabilties and ownership tokens, joining and spliting capabilities
and pointers to form references, and manipulating heap values (each
type of heap value has its own set of instructions).

Instructions that introduce blocks of instructions, like
$\Wkey{block}$ or $\Wkey{if~then~else}$, are annotated not only with
their type as in Wasm, but also with their local effects,
$\Wleff$. These describe the effect that a list of instructions may
have on the type of their local variable slots: the slot at
position $i$ gets type $\Wtau$.

§.§ Unsafe Interoperability

We extend the languages in the style of linking types <cit.>, which allow
languages to maintain their native reasoning principles while interacting with foreign types
near language boundaries.

gets a type which directs the compiler to make a type $\tau$ linear in , written
$(\tau)^{\Wlin}$. To store linear types, it also has a new construct $\reftolin$ which creates
a reference which can either be empty or contain a linear value of the given type. Normal
$\tt{Ref}$ operations can be used on these references, but compiles them in such a way that
if they are read from or written to twice, they will fail at runtime, as this would violate
linearity and thus not typecheck[In the following example, the code's use of its
reference to a linear value is entirely valid and would not crash on purpose. This program would
result in a true memory safety violation if admitted by .].

, which typically only has capabilities and pointers, gets a new -like $\tt{Ref}$ type.
In order to convert to and from this type at the boundary with an program, it also has two
new constructs $\tt{join}$ and $\tt{split}$.

let c = $\reftolin$ (Ref Int)$^{\Wlin}$ in
fun stash (r : (Ref Int)$^{\Wlin}$) : (Ref Int)$^{\Wlin}$ =
c := r; r
fun get_stashed (() : Unit) = !c

ML program

import (ml.stash :
!(($\exists$ $\ell$. Ref $\ell$ !Int 1) $\multimap$ ($\exists$ $\ell$. Ref $\ell$ !Int 1)))
import (ml.get_stashed :
!(!Unit $\multimap$ ($\exists$ $\ell$. Ref $\ell$ !Int 1)))
free (split (stash (join (new !42 1))));
free (split (get_stashed !())) (* CRASH! *)

Unsafe interoperability

Fig. <ref> shows an example akin to that in Fig. <ref>,
but with syntax more accurate to and .

The key differences are that the programs must use their new extensions to agree on types at
the linking boundary. The problematic function here is still 's $\tt{stash}$, and will not
allow it to typecheck since it duplicates a linear value. If $\tt{stash}$ were to not return the linear
value (and correspondingly were to no longer attempt to free that value, since it's not
returned), this program would type check and 's previously illegal attempt to free
would be safe.

§ DYNAMIC SEMANTICS

Execution in terms closely follows Wasm and it is defined as a
reduction relation. The relation, written
represents a reduction step in module $j$ from one program configuration
$s;\many{v};\many{sz};\many{e}$ to another, where $s$ is the store, $\many{v}$
the local values and $\many{sz}$ the sizes of their slots, and
$\many{e}$ the instructions to be evaluated. Fig. <ref> shows the definition of runtime
objects as well as important rules of the reduction relation.

We elide rules that are identical to Wasm, and we focus on the
reduction rules of new constructs.

dynamic semantics

Store and module instances. A store represents the execution
state. It holds the list of module instances, which is the
dynamic representation of static modules and the global
memory. A module instance consists of a dynamic function table that
holds a list of closures which, as in Wasm, is used for direct
calls, a list of global values, and the dynamic table which is a list
of closures that is used for indirect calls. A closure, in the Wasm
sense, is a dynamic instance of a function that consists of the
code and a pointer to the module that provides the function's

The global memory has two components: the linear memory and the
unrestricted memory. Both memories are maps from locations to
high-level heap values.

Administrative instructions. As in Wasm, some reduction rules
generate instructions that are not part of the syntax of source
programs and represent administrative operations. A $\Wtrap$
instruction signals an execution trap. We add two administrative instructions:
$\Wmalloc{\Wsz}{hv}{\Wqual}$ to allocate memory of size $\Wsz$ holding a value $hv$
in the memory $q$, and $\Wfree$ to deallocate parts of the linear memory, given
a reference. Allocation and deallocation of aggregate types reduces to these
administrative instructions.

The administrative instruction $\Wcallcl{\Wcl}{\many{z}}$ is similar
to Wasm's but along with the closure $cl$, it is annotated with the
concrete instantiation of the polymorphic quantifiers in the
function's type, $\many{z}$.

Control flow.
Much like in Wasm, when running programs, evaluation occurs
within some number of label instructions, each of which corresponds to
a source block of code (introduced by instructions like
$\Wkey{block}$, $\Wkey{if}$, $\Wkey{loop}$). The break instructions
($\Wkey{br}$, $\Wkey{br\_if}$, $\Wkey{br\_table}$) allow programs to
jump to any of the surrounding N locations by specifying how many
labels to jump over. Nested label instructions are represented with
$\emph{local contexts}$. A local context $\locctx^N[\many{e}]$
represents N nested label instructions. A local context has a hole at
its most deep label instruction, where evaluation can occur.

§.§ Reduction relation.

We give an overview of the most important reduction rules
of that are new or different from those in Wasm.

Additional reduction rules can be found in 1 of
the appendix. The full set of rules is encoded in our Coq development.

For space reasons, we drop the store and local variables in all the
rules that leave them unchanged. We may still use the store $s$ in
side conditions where it is relevant, without explicitly mentioning it
in the rule.

Garbage collection.
The reduction relation is equipped with a rule that can be applied at
any point and allows collection of unrestricted locations that are no
longer accessible from the configuration. Therefore, the roots of collection
are the unrestricted locations that appear in reference values in the
instructions, local variables, or the module instances. Any location not
reachable from the roots is collected.

If a reference to linear memory is placed into garbage collected memory,
we say that the garbage collector now owns that memory and is
responsible for collecting it if the unrestricted location, and thus the
only reference to the linear location, should be collected.

Freeing of linear memory is a type-directed operation, and when compiling
to Wasm, we can generate finalizer functions that get called when such
references are collected. But what would we do if a capability to linear
memory were in garbage-collected memory? When compiling to Wasm, capabilities
will be erased, which would leave the garbage collector with no way to reference
the linear memory location it owns at runtime. To resolve this, we require
that capabilities always be paired with a pointer in the form of a reference
when placed in memory.

Function calls. Function calls follow similar
principles with function calls in Wasm. Few differences arise from the
polymorphic types of functions and the way polymorphic binders
are instantiated.

Direct function calls are performed with the $\Wcall{j}{\many{z}}$
instruction, where $j$ is the index of the function in the function
table and $\many{z}$ that concrete instantiations of the polymorphic

The instruction $\Wcall{j}{\many{z}}$ is reduced to the administrative
instruction $\Wcallcl{\mathit{cl}}{\many{z}}$, where $\mathit{cl}$ is
the corresponding closure in the function table.

Indirect function calls are performed with $\Wcallindirect$, whose
argument is a code pointer $\WVcoderef{i}{j}{\many{z}}$ that points to
the $j$th function of the $i$th module instance and $\many{z}$ are the
concrete instantiations of polymorphic indexes.

The administrative call instruction $\Wcallcl{\mathit{cl}}{\many{z}}$,
where $\mathit{cl}$ is a closure containing a module number and function
body, takes as stack arguments the arguments of the function and reduces to
a local frame that performs the necessary substitutions of the
polymorphic indices. For the sizes of local variable slots we use the
metafunction $\sz(\cdot)$ that returns the size of a type.

Heap manipulation.
Let's consider the rules for manipulating 's new heap structures.
All heap data structures have have their own allocation
instruction that reduces to the administrative malloc instruction we saw above.
This malloc instruction then reduces to a reference contained in an
existential package which abstracts the location.

Reduction rules for struct's get, set and swap operations are straightforward,
taking a reference from the stack and perhaps the value to put at the
$i$th field, performing any necessary memory updates, and leaving the
reference back on the stack, together with the read value, if any.

Variants can be used to perform case analysis. The case instruction expects on the
stack the reference to the variant and a list of values expected by the branches,
that have types $\manyn{\Wty_1}{n}$.

If the allocated value is the $i$th case of the variant, then we create
an instruction block using the $i$th element of the list of instruction
blocks $\manyn{(\many{e})}{m}$, written $\manyn{(\many{e})}{m}_{(i)}$.

If the case instruction is anntotated with an unrestricted qualifier, the
reference is returned to the stack for reuse.

If the annotation is linear, then a $\Wfree$ instruction is generated to consume
the reference. In this case the contents of the memory are
replaced with an empty array, so that the linearity invariants of the
type system are preserved.

Existential types can be packed and unpacked. Packing an existential
type triggers the allocation of a $\Wkey{pack}$ heap value.

Much like variants, the unpacking operation is a block instruction
which can optionally free the underlying memory. The unpack operation
additionally needs to substitute the witness pretype in the list of
instructions to be evaluated.

§ TYPE SYSTEM

We now give a technical account of the type system as well as its safety properties.

Typing environments.
Typing environments in (fig. <ref>) are similar to
Wasm, but they also keep track of the new kind variables (types,
sizes, locations, qualifiers) and their constraints.

The local environment keeps track of the type and size of the
local variables of a program configuration. It is a list of a type and
size where the $i$th element corresponds to the size and the type of
local variable $i$.

The function environment is used to give a function type to a
list of an expressions. It has 7 components. As in Wasm, the
$\mathsf{label}$ component keeps track of the return type of all the
available jump locations (i.e., nested labels). In , it additionally
tracks the resulting local environment, as all jumps to a location must
have the same view of the types of locals.

The $\mathsf{return}$ component keeps track of the return type of the
execution of the current block of instructions.

$\mathsf{qual}$, $\mathsf{size}$, $\mathsf{type}$ are partial maps from
the variables in scope to the constraints placed on them, as explained
in <ref>.

The $\mathsf{location}$ component keeps track of declared location

Lastly, the $\mathsf{linear}$ environment contains a list of
qualifiers representing the greatest lower bound of the qualifiers of
the values on the stack between two jump locations. Jumping from the
current evaluation context to an outer label will drop the contents of
that label, including any potentially linear values. The linear
environment can be used to verify that all values dropped when
performing a jumping to a given label are unrestricted.

To update an component of a typing environment we use similar notation
as the WebAssembly paper. For instance, we write $F, \mathsf{linear}~
\Wunr :: F_{\mathsf{linear}}$ to update the linear environment of $F$
by inserting the qualifier $\Wunr$ to the top of the list.

Local Environment (, )
Function Environment{    𝗅𝖺𝖻𝖾𝗅 (, ),    𝗋𝖾𝗍𝗎𝗋𝗇 ()^?,
𝗊𝗎𝖺𝗅 ⇀(, ),
𝗌𝗂𝗓𝖾 ⇀(, ),

𝗍𝗒𝗉𝖾 ⇀(, , hc),
𝗅𝗈𝖼𝖺𝗍𝗂𝗈𝗇 ,    𝗅𝗂𝗇𝖾𝖺𝗋   }

Module Environment
{ 𝖿𝗎𝗇𝖼 ,
𝗀𝗅𝗈𝖻𝖺𝗅 ,
𝗍𝖺𝖻𝗅𝖾   }

Store Typing
{ 𝗂𝗇𝗌𝗍 ,            𝗎𝗇𝗋 ⇀,            𝗅𝗂𝗇 ⇀ }

Typing environments.

The module environment keeps track of the declared functions and globals in
the current module.

Finally, we have the store typing that keeps track of the list of
module instances ($\mathsf{inst}$) and the typing of the linear and unrestricted memories.

The memory typing is a partial map from a memory locations to a pair
of the stored heap type ($\Whty$) and the size of the slot.

The linear memory typing is split across
the typing of the subexpressions in the premises of a rule to ensure
that no linear resource is used twice in the program.

We write $S= S_1 \uplus S_2 $ to denote that the linear memory typing
of $S_{ \mathsf{lin}}$ is the disjoint union of
$(S_1){_\mathsf{lin}}$ and $(S_2){_\mathsf{lin}}$, whereas the other
components are exactly the same in all three store typings.

When typing a base value or instruction that has no linear memory
locations, we require that the

Value Typing. The value typing judgment, written
$\valtype{S}{F}{v}{\Wty}$, asserts that a value $v$ has type $\Wty$
in a store typing $S$ and function environment $F$.

Selected value typing rules are shown in Fig.
<ref>. Numeric constants have the corresponding numeric
type and can have any qualifier.

Tuples have a tuple type consisting of the types of individual values.

The top-level qualifier must be an upper bound for each individual
qualifier $q_i$ of any type $p_i^{q_i}$ inside the list $\many{\Wty}$.

Pointers have type $\WPptr^{\Wqual}$, which is independent of the heap
type of the location, and do not consume a location from the memory
typing as they do not represent memory ownership.

Typing of capabilities and references are similar. We only explain

In the unrestricted case, a reference $\WVref{\Wlocunr}$ has type
$(\WPref{\Wrw}{\Wlocunr}{\Whty})^{\Wqual}$, where $\Whty$ is the type
of $\Wlocunr$ in the unrestricted component of the heap. The qualifier
$q$ must be provably unrestricted in the constraints of
$F_{\mathsf{qual}}$, written $\Wqual \Wquallessctx \Wunr$. The linear
component of the memory typing must be empty.

The linear case is similar. The type $\Whty$ is the type of $\Wloclin$
in the linear component of the heap, which must be a singleton. The
qualifier must be linear.

The value $\WVfold{v}$ has the recursive type
$\WPrec{\Wptyvar}{\Wqual}{\Wpty^\Wqual})^{\Wqual'}$, if the value $v$
has type
where we have substituted $\Wptyvar$ with
$\WPrec{\Wptyvar}{\Wqual}{\Wpty^\Wqual}$, and the qualifier $\Wqual$
is upper bounded by $\Wqual'$.

Next we have existential packages $\WVmempack{\Wloc}{v}$ that have an
existential type $(\WPexists{\Wlocvar}{\Wpty^\Wqual})^{\Wqual'}$ if
the type of value $v$ is $(\Wpty\subst{\Wlocvar}{\Wloc})^{\Wqual'}$
and qualifier $\Wqual$ is upper bounded by $\Wqual'$.

Lastly, we have typing for code references
$\WVcoderef{i}{j}{\many{\Wk'}}$: if $M$ is the $i$th module
instance and $\forall \many{\Wk}. \Waty $ the type of the $j$th
function in the table of $M$, then the code reference has type
$(\Waty\subst{\many{\Wk}}{\many{\Wk'}})^\Wqual$ where
quantifier variables $\Wk$ have been substituted with the indices

S = _i≤nS_i

∀ v_i∈vn _i∈n,  _iv_i_i

∀ _i^_i ∈n,   _i

(i) = M

.𝗍𝖺𝖻𝗅𝖾(j) = ∀.

Value typing.

Heap Typing. The heap typing judgement is written $\heaptype{\storetyp}{\funcctx}{\Whv}{\Whty}$
and asserts that the heap value $\Whv$ has type $\Whty$ in the store
typing $\storetyp$ and function environment $\funcctx$. Complete rules
of heap value typing can be found in the appendix.

Instruction Typing. The core of 's type system is typing of instructions.
The typing judgement, written
asserts that a list of instructions $\many{e}$ has type
$\ftyp$. $\storetyp$, $\modctx$, and $\funcctx$ are the store typing,
module environment and function environment respectively.

$L$ is the local environment that keeps track of the types and sizes
of the local variables, and $L'$ is the typing of the local variables
after execution of $\many{e}$, which might change the types of local
variables. Many rules follow Wasm with the addition that we add the
necessary premises to ensure linearity (i.e., constraints on
qualifiers and linear memory typing). In Fig. <ref>, we
show several important rules of the system.

Instruction typing.

All block-style instructions follow similar principles, so let's examine
the block instruction $\Wblock{\Wty}{\Wleff}{\many{e}}$.

The block instruction is annotated with the type of the inner list of
instructions $\ftyp$ and the local effects $\Wleff$, which prescribe
the effect that this block of instructions has on the local
environment. The premises of the rule first construct the returned
local environment $L'$, by applying the local effects to the initial
local environment, which is written $\Wleff[L]$ and means that the
type of the $i$th slot of $L$ changes to $(\many{\Wtau})_{(i)}$.

Then the premises assert that block of instructions has the expected
type inside a new function environment that we obtain by pushing
$(\Wty_2, L')$ to the $\mathsf{label}$ component and $\Wunr$ to the
$\mathsf{linear}$ component.

The former tracks the return type and local environment of the label
we are creating. The latter gives us a new qualifier with which we
will track linearity of values on the stack inside this new block and
"locks in" the qualifier corresponding to the linearity of the values
on the stack between the previous enclosing block and this new block.
We choose $\Wunr$ becuase upon entering a block there are no linear
values which might be jumped over. The head element of the $\mathsf{linear}$
environment can be increased by the frame rule (not shown), which as in Wasm, allows
typing rules to ignore values lower on the stack. Since break
instructions will not see ingored values, the only way they can know
whether they will be dropping linear values is by consulting this

Let's look at some instructions for manipulating locals.

The $\Wgetlocal{i}{q}$ instruction fetches the value of the $i$th
local slot. If the qualifier of the slot, $q$, is linear, then the
contents of the slot must be updated to ensure linearity. We replace
it with the unit value and update the typing of the slot accordingly.

The $\Wsetlocal{i}$ instruction updates the $i$th local slot,
allowing to update its type as well. It ensures that the previous
value was unrestricted, so it can freely be dropped, and that the
upper bound of the size of the new type $\sizeof{\tau}$, fits into the
size of the slot, written $\sizeof{\tau} \Wszlessctx \Wsz$. The size
function takes the $\mathsf{type}$ environment component as parameter
to lookup the upper bound for the size of type variables. The
$\Wszlessctx$ operation takes as parameter the $\mathsf{size}$
component to take into account the size constraints that are in scope.

Creating an existential package is done with $\Wmempack{\Wloc}$.
It receives a value from the stack containing
a location $\Wloc$ and creates an existential package that hides this

The typing rule for $\Wmemunpack{\Waty}{\Wleff}{\Wlocvar}{\many{e}}$
is more complicated. It combines the typing of instructions that
introduce a new block with unpacking
an existential location. The instruction receives from the stack the
arguments of the instruction block $\many{\Wty_1}$ and a packed value
with an existential location type. Then it puts the location variable
in the $\flocation$ environment component to type the instructions in
the block.

The handling of the $\flabel$ and $\flinear$ components is the same as
in the block instruction.

Next we discuss instructions for manipulation heap values. Each family
of heap values has its own malloc instruction. For example,
the $\Wstructmalloc{\manyn{sz}{n}}{q}$ instruction allocates
space for a struct of $n$ values with sizes $\manyn{sz}{n}$. It
receives from the stack $n$ values of types $\manyn{\Wty}{n}$ and it
returns a reference whose location is abstracted with an existential
type and has the corresponding struct type. We require that the size
of the types fit into the requested sizes of the slots. We also put
the restriction that there are no capabilities in the types, for
the reasons described in <ref>.

Structs have get, set, and swap operations shown in the following
rules. $\Wstructget{i}$ gets the $i$th element of a struct, that must
be an unrestricted value, and $\Wstructset{i}$ sets the $i$th element
with the a value that it finds on the stack. The qualifier of the
previous value that is dropped must be unrestricted. If the reference
holding the stack is linear then the type of the new value can be
arbitrary, otherwise it must be the same as the type of the previous
value, as only linear structs support strong updates.
There is also a check the the new value fits in the size of the slot.

The only way to read and write a linear entry from a struct is with a
$\Wstructswap{i}$ operation that combines set and get by
simultaneously getting and setting a struct cell and therefore ensuring
that neither value is dropped or duplicated.

Variants in the heap can be manipulated with the case analysis
instruction. The instruction
performs case analysis on a variant with type
$\WHvariant{\manyn{\Wty}{n}}$ and, depending on the result, executes
one block of instructions from the branch list
$\manyn{(\many{e})}{n}$. The rule expects $\many{\Wty_1}$ on the stack
and returns $\many{\Wty_2}$. If the qualifier of the instruction is
linear, then the underlying memory will be freed after the case analysis
and the given (linear) reference will not be returned.
Each of the instruction blocks $(\many{e})_i$ are typed in
the updated (in the usual way) function context and are required to
have type ${\Warrow{\many{\Wty_1}~\Wty_{i}}{\many{\Wty_2}}}$,
where $\Wty_{i}$ is the type of the $i$th variant.

The unrestricted case is similar, with the distinction that the reference
is returned onto the stack after the case analysis and the underlying memory
is left intact.

In addition, the second
element of the $\flinear$ component (corresponding to the values outside
this case block, but inside the nearest surrounding block) is switched to
an arbitrary $q'$ that is stricter than both the qualifier of the variant
reference and the previous qualifier of $\flinear$. This ensures that any
jumps beyond this case block will need to consider whether the reference
we're leaving on the stack is linear, as such a jump woudld drop it.

Configuration and store typing. At the top level we have
the typing judgements for stores and program configurations, show in Fig. <ref>.

The spirit is the same as in Wasm, but we have to split the linear
store typing across the typing of different components of the
configuration. First we introduce an auxiliary judgement
that asserts that in the store typing $S$ the configuration
$s;\manyn{v}{n};\manyn{\Wsz}{n};\many{e}$ will result in a stack of type
(or potentially returns) $\many{\Wtau}$. The premises require that
the local values are well-typed with some types $\manyn{\Wty_v}{n}$
and that the size of each (closed) value fits in the size of the
corresponding slot. The instructions have type
$\Wemptyarrow{\many{\Wty}}$ under the empty function context containing
only an optional return type and under the local context
$\manyn{(\Wty_v, sz)}{n}$. The store typing $S$ is the disjoint
union of the store typing used across all typing judgements of the
premises. Furthermore, we require that in the final local environment
there are no linear values, as all of them must be consumed.

The store typing judgement $\vdash s : \storetyp_{\mathit{heap}};
\storetyp_{\mathit{prog}}$ asserts that the store $s$ has typing
$\storetyp_{\mathit{heap}}; \storetyp_{\mathit{prog}}$.  The two store
typings $\storetyp_{\mathit{heap}}$ and $\storetyp_{\mathit{prog}}$
have identical instances and unrestricted memory typings, but disjoint
linear typings.  The linear typing of $\storetyp_{\mathit{prog}}$
contains the surface locations found syntactically in a configration,
i.e., the root pointers, while the linear typing of
$\storetyp_{\mathit{heap}}$ contains the linear locations needed to
type the contents of the memory.

The rule asserts that the domain of the linear memory coincides with
the locations contained in the linear typing of
$\storetyp_{\mathit{heap}}$ and $\storetyp_{\mathit{prog}}$, and the
same for the unrestricted memory.

It also asserts that every pair of location and heap value in the
unrestricted store has the corresponding type prescribed by the
unrestricted memory typing.

For the reasons described previously, it also requires that no capabilities
are present on the heap.

Additionally, $\storetyp_{\mathit{heap}}$ must be the disjoint union
of all the individual store typing components used in typing the heap

Lastly, the rule asserts that the length of the module instances
$|s_{\mathsf{inst}}|$ must coincide with the length of the instance
typings $|S_{\mathsf{inst}}|$ and that each instance in the list has
the corresponding instance typing. We elide the instance typing
judgement from the paper as it is similar to the one of Wasm.

The top level judgement
asserts that the store is well typed in some store typings
$\storetyp_{\mathit{heap}}$ and $\storetyp_{\mathit{proj}}$, and that the
configuration is well typed in the store typing

= _stack ⊎_1 ⊎…⊎_n

∀v_i ∈vn _i ∈n,  _i;_empty ⊢v_i : _v_i ∧ v_i _ϵ _i

= _empty, 𝗋𝖾𝗍𝗎𝗋𝗇 ()^?

_stack(i)(_v, )neϵ→L'

∀(^, ) ∈L',

$\vdash s : \storetyp_{\mathit{heap}}; \storetyp_{\mathit{prog}}$

S = _heap ⊎_prog

𝑑𝑜𝑚 s_𝗅𝗂𝗇 = 𝑑𝑜𝑚

𝑑𝑜𝑚 s_𝗎𝗇𝗋 = 𝑑𝑜𝑚

s_𝗎𝗇𝗋 = { (l__1, __1), …, (l__n, __n) }

s_𝗅𝗂𝗇 = { (l__1, __1), …, (l__m, __m) }

∀ i≤ n, S_𝑢𝑛𝑟_i_empty__i(l__i)

∀ i≤ m, S_𝑙𝑖𝑛_i_empty__i(l__i)  ∧  l__i ∈𝑐𝑜𝑑𝑜𝑚 s_𝗎𝗇𝗋 ⇒𝑛𝑜_𝑐𝑎𝑝𝑠(__i)

_heap = _i ≤n S__i ⊎_i ≤m S__i

|s_𝗂𝗇𝗌𝗍| = |S_𝗂𝗇𝗌𝗍|

∀ i≤𝑙𝑒𝑛,  S_𝗂𝗇𝗌𝗍 ⊢s_𝗂𝗇𝗌𝗍(i) : S_𝗂𝗇𝗌𝗍(i)

⊢s : _ℎ𝑒𝑎𝑝; _𝑝𝑟𝑜𝑔

$\conftype{i}{s}{\many{v, \Wsz}}{\many{e}}{\many{\Wtau}}$

⊢s : _heap; _prog

Configuration typing.

§.§ Type safety

We prove, in Coq, that our language is type safe by proving soundness via progress and preservation.

If a configuration is well-typed
$\conftype{i}{s}{\many{v, \Wsz}}{\many{e}}{\many{\Wtau}}$, then either
$\many{e}$ are all values, or it is a single $\Wtrap$ instruction, or
the configuration can take a step $\Wredi{s}{\many{v}}{\many{\Wsz}}{\many{e}}{s'}{\many{v'}}{\many{e'}}$.

If a well-formed and well-typed configuration,
$\conftype{i}{s}{\many{v, \Wsz}}{\many{e}}{\many{\Wtau}}$, takes a step
then the resulting configuration is well-typed with the same type
$\conftype{i}{s'}{\many{v', \Wsz}}{\many{e'}}{\many{\Wtau}}$

Coq development. We have formalized the language, its static and dynamic semantics,
and the proof of type safety via progress and preservation in Coq.

The effort is substantial, consisting of  14k lines of specifications
(definitions and theorem statements) and  52k lines of proofs, all
directly related to the type system.

We have submitted the proof development as supplemental material.

At the time of the submission we have 4 remaining admitted lemmas,
all related to substitution (among many others that we have fully proved).

We give a more detailed description in the submitted artifact.

§.§ Example

We conclude this section by considering some examples to see how 's fine-grained
memory access might be useful for real programs. Imagine a library for some performance-critical
operation, such as a graphics library. We  want to implement this in a manually managed
source language. Instances of this graphics data structure might take some mutable configuration
state that can change over the course of a program, such as quality settings or dimensions.
Next, we might want to write the higher-level logic of our program in a GC'd language which simply
makes use of this library for graphics. Such a program requires the GC'd code to reference linear
values, which in turn reference some shared mutable state.

For our example, we'll keep this structure, but simplify our library down to a small mutable counter.
The shared runtime state will configure how much counters should increment by. The GC'd portion of
our program will use this linear library, but hide it behind an interface which allows it to use
the library without reasoning about linearity.

\begin{align*}
\textsf{Client} & :=
\WHexists{\Wunr}{\Wptyvar}{64}{\WPgroup{\Wptyvar^{\Wunr}
(\WPcoderef{\forall~\epsilon.~\Wptyvar^{\Wunr} \rightarrow \Wkey{i32}^{\Wunr}})^{\Wunr}}^{\Wunr}} \\
\textsf{$\alpha$} & :=
(\WPexists{\ell}{(\WPref{\ell}{\Wrwrw}{\WHstruct{Counter,~64}})^{\Wunr}})^{\Wunr} \\
\textsf{Counter} & :=
(Config,~64)}})^{\Wlin}})^{\Wlin} \\
\textsf{State} & :=
(\WPexists{\ell}{(\WPref{\ell}{\Wrwrw}{\WHstruct{\Wkey{i32}^{\Wunr},~32}})^{\Wlin}})^{\Wlin} \\
\textsf{Config} & :=
(\WPexists{\ell}{(\WPref{\ell}{\Wrwr}{\WHstruct{\Wkey{i32}^{\Wunr},~32}})^{\Wunr}})^{\Wunr} \\
\\
\end{align*}

Memory layout. (ref = solid blue line) (coderef = dashed pink line) and type definitions.

Fig. <ref> presents a memory layout for such an example.

is the value with which our GC-ed portion will be interacting.

It contains a pair of an abstract value $\Wptyvar$ and a coderef which, given that value,
increments the counter and returns the new count.

The hidden type $\Wptyvar$ contains a struct referencing , the main data
structure provided by our linear library.

contains a pair of references, one which grants write access ($\Wrwrw$)
to its internal mutable state (), and one which grants read access ($\Wrwr$)
to the shared configuration ().

Once this heap is laid out, the GC'd portion of the program can configure and use
the counter without any need to reason about linearity at all.

A program which creates this heap layout is included in our supplemental material.

§ COMPILING TO

In order to demonstrate that provides a reasonable target for a
variety of high-level languages, we implement type-preserving compilers
from a garbage collected language () and a manually managed language
(). In order to demonstrate 's ability to serve as a
platform for interop between languages, we extend and with
the necessary constructs to reference each other's types in a limited
fashion. For these extensions, we follow a linking types <cit.> approach,
which aims to allow users of a source language to link with other types
inexpressible in their own language, without losing native reasoning principles.
Additionally, programs which do not mention any extensions are unaffected
by the extensions' presence in the language.

. Our base supports the standard types: units, ints, references,
variants, products, recursive types, and functions with parametric polymorphism.
Since has similar types, the choice of
representation is quite straightforward.

We also extend with standard constructs for writing multi-module code, such as
function imports and exports and the ability to define global state which exported
functions can close over.

Such extensions provide a good basis for exploring multi-module code in and
eventually interoperability with other languages.

As described in the discussion of Fig. <ref>, we extend with
the ability to direct the compiler to compile particular types as linear and provide
a construct which allows the creation of references containing linear types.

The compiler explicitly does not check whether types annotated as linear are used
linearly, as we can rely on to demonstrate safety. The goal of interoperability
is to allow programmers to use the right language for each task, without burdening them
by turning the type system of their source into something as complex as . Programmers
are still writing , only using these linking types at the boundary between languages.

. We compile the core language with a minor adjustment.

We require that capabilities explicitly track the size of the memory they reference.

Pragmatically, sizes will need to be reasoned about at the level, but also
philosophically, a source language which allows precise reuse of memory should
require a programmer to think about sizes.

While 's ability to perform strong updates is impressive, it must be accompanied
by reasoning about the size of the location being updated to be useful.

As described for the example in Fig. <ref>, we extend with an -like reference
type in order to allow memory interop between the two languages, as well as constructs (, ) to
convert between capability-pointer pairs and references.

Readers familiar with might note that its source programs often put capabilities on
the heap, an operation which is disallowed in the verion of presented in this paper.

While pointers and capabilites can be separated, programs can always place
capabilities on the heap with some pointer in the form of a reference without losing the
performance gains that come from moving raw capabilities around on the stack.

Nonetheless, we've been working on relaxing this restriction in such that capabilities
are only disallowed in the parts of the heap owned by the garbage collector.

We're in the process of updating our formalism, but our prototype compilers and typechecker already support this more relaxed restriction, allowing programmers to write
in their native style.

Compilation to untyped or poorly typed targets requires compiler writers to
expend significant effort on low-level details like data layout, calling
conventions, and bit manipulation. In contrast, compilation to is
largely an exercise in satisfying 's type system. While this is not
entirely straightforward, we have found it to be tractable.

The compiler has three phases of note: typed closure conversion,
annotation, and code generation.

Typed closure conversion is standard in compilers for functional languages.

What is notable is that (after the remaining passes) is going to check
the correctness of this pass, examining the size and qualifier annoations
that we use when generating existential packages to hide the environments of

Since all type variables in have size and qualifier bounds and has
no such notion at the source, we introduce an annotation phase to change the
types of functions appropriately, annotating definitions and call sites with
the appropriate information.

Code generation is overall quite similar to code generation to any stack based

However there are some type-based complications.

For instance, instead of relying on a compiler writer's carefulness when
shuffling values around, requires explanation of one's use of locals
in the form of a local effect annotation on every block of
code, allowing it to check that duplication only occurs when allowed.

is a much lower level language, without the ability to existentially or
universally quantify types. Thus, it is much easier to compile to , and we
can do so in one code generation phase.

To keep things simple and since we've already demonstrated how to do so in , we
don't implement closure conversion in .

§ COMPILING TO WASM

Compilation from to WebAssembly is type directed.
It requires some type information that is implicit in instructions which is provided by the type checker.

The to Wasm compiler takes in the type annotated code produced by the type checker and compiles to WebAssembly 1.0 with the multi-value extension, where, functions and instructions can return more than one value.

Lowering 's Type System.
Every type will be translated to a series of base Wasm numeric types.

Types with no runtime information, such as $\Wkey{unit}$, $\Wkey{cap}$ and $\WPown$, are erased.

Numeric types are translated to the corresponding WebAssembly  type.

$\Wkey{ref}$  and  $\Wkey{ptr}$ are lowered to a single $\Wkey{i32}$ pointer.

Type variables $\Wptyvar$ are annotated with a size bound that indicates the maximum size of the type that the $\Wptyvar$ can be instantiated with.
If this size is concrete or an upper bound for it can be inferred using the constraints, we compile the type into a series of Wasm's numeric types.

If the upper bound is unknown, the $\Wptyvar$ is boxed on the heap and it is translated to an $\Wkey{i32}$ pointer.

To translate recursive types, we just compile the inner type, since gives us an invariant that the recursive type appears only inside a level of indirection.

For existential types, we similarly lower the inner type down to Wasm numeric types.

Operations on local and global variables.
Local variables in can have arbitrary sizes and can have multiple types over their lifetime.
In Wasm, however, local variables can only be one of four numeric types.

Therefore, we lower a local to a series of Wasm locals.

For example, if a local has size 160 it will be stored across three Wasm locals of types $\Wkey{i64}$, $\Wkey{i64}$ and $\Wkey{i32}$.

This sequence of locals might be used to store any type of size up to 160, for example $\WPgroup{\Wkey{i32}~\Wkey{i64}~\Wkey{i64}}$.
Therefore, the first local will store the first $\Wkey{i32}$ component of the tuple and the first half of the second $\Wkey{i64}$ component.

The compilation of $\Wkey{local.set}$ and $\Wkey{local.get}$ needs to perform the correct accesses to fetch the entire value onto the stack, and is informed by the type.

Operations on global variables in is similar to locals.

Memory model and heap types.
In Wasm we use only one flat memory to represent both 's memories.

We use a simple free list allocator to allocate and free pointers in
Wasm memory.

Structs and arrays are encoded in the Wasm memory as a consecutive bytes. Similar to local variables, the representation of a field or an array slot might need to use more than one consecutive memory slot.

Variants are represented in memory as a sequence of bytes containing the numeric tag followed by the corresponding type.

$\Wkey{variant.case}$ instructions are compiled as a switch case for every case in the variant. Switch cases are represented in Wasm using nested blocks, with blocks for every case, and a $\Wkey{br\_table}$ instruction in the innermost block that jumps to the case being executed. At the start of every case, we provide instructions to read data from the heap according to the type of that case.

$\Wkey{exists.pack}$ stores a single value on the heap, and $\Wkey{exists.unpack}$ reads it, with the help of an annotation of the type.

Function calls.
Functions in can be polymorphic on types with unknown size bounds that are represented in Wasm as $\Wkey{i32}$ pointers.

Say that a caller needs to pass an argument of type
$\WPgroup{\Wkey{i64}~\Wkey{i32}}$ to a function that expects a boxed
representation of the same argument as it is polymorphic on its type.

The caller will put an $\Wkey{i64}$ and $\Wkey{i32}$ on the stack.
Then, we need to perform a stack coercion, replacing the $\Wkey{i64}$
and $\Wkey{i32}$ with a pointer to the same data on the heap.  Stack
coersions like this will always be required when functions expect or
return values of boxed $\Wptyvar$ types.

For indirect calls, $\Wkey{coderef}$ instructions compile to an
$\Wkey{i32}$ index into the function table.

To coerce the stack to the shape that the callee expects, we make a
case for each possible shape in the table that could correspond to this call,
and at runtime we jump to the correct case depending on the value of the
index to the table.

Remaining Instructions.
Instructions that have identical counterparts in Wasm are left
unaltered. $\Wrecfold$, $\Wrecunfold$, $\Wmempack{\Wloc}$,
$\Wseqgroup$, $\Wsequngroup$, $\Wcapsplit$, $\Wcapjoin$,
$\Wrefdemote$, $\Wrefsplit$, $\Wrefjoin$, $\Wqualify$, $\Wkey{inst}$ are all erased
since they are type level operations.

§ RELATED WORK

In <ref>, we've already discussed the three most closely related
piece of work: , the Component Model, and Patterson et al.'s semantic
framework for sound interoperability. In a general sense, is also
influenced by work on substructural types, using $\Wunr$ and $\Wlin$ qualifiers
to annotate pretypes as in <cit.>, and by work on
type-preserving compilation and typed low-level
languages <cit.>.

Wasm does not currently support garbage collection natively, but a
proposal to do so is currently working its way through the standardization
process <cit.>. 's heap types are intentionally designed
to be compatible with this proposal, but we believe it lacks one crucial
feature: finalizers. Many languages use finalizers, and for they
are essential to allowing the garbage collector to own, and thus sometimes
free, linear memory. At present, with Wasm's current GC proposal, 's
runtime needs to implement its own garbage collector.

MSWasm <cit.> (Memory-Safe Wasm) is an extension of Wasm designed to
enforce memory-safe execution of unsafe code, e.g., code compiled from C
or C++. MSWasm extends Wasm with language constructs for CHERI-like fine-grained
dynamically checked memory capabilities so code compiled from C will be checked
for memory safety at runtime. In contrast, has static rather than dynamic
capabilities, which have the benefit of zero runtime overhead. But is
meant to be a target for type-safe source
languages; when compiling an unsafe language like C it would be nearly
impossible to produce type-annotated code that is well typed since the
type information and safety guarantees don't exist in the source.

Iris-Wasm <cit.> is a mechanized higher-order separation logic for
modularly verifying Wasm 1.0 programs. The authors have used Iris-Wasm to build
a logical relation for Wasm and prove type safety. By contrast, we have a
mechanized type safety proof for a language with a far richer type system, but
is a typed language not a verification logic.

§ DISCUSSION AND FUTURE WORK

We want to serve as a platform for safe interoperability between a wide range of typed languages, which may require extending its type system.
Our first priority in future work is type-preserving compilation from safe Rust  to . There are two interesting challenges: how to encode lifetime constraints and how to encode immutable borrows in . The latter may require fractioal capabilities so we can create many borrows but when all of these borrows end, we can produce a linear capability to return to the owner.  A further challenge is to compile Rust with concurrency to a concurrent extension of , in turn compiling that to the recent Wasm threads proposal.

Next, we will tackle compiling languages with advanced control effects, e.g., algebraic effect handlers. This will require extending with linearly typed continuations and compiling to Wasm with the recent typed continuations proposal <cit.>. The latter dynamically ensures that continuations are used linearly instead of using linear types, which are expensive to implement as they preclude in-place updates. In , we can statically ensure linear usage of continuations and then have the compiler to Wasm perform the optimization to use in-place updates. We can verify correctness of such optimizations using a logical relation.

Wasm provides custom sections and the ability to implement additional type-checking by examining annotations in custom sections. We can leverage this to keep type information around in Wasm, enabling a rich form of proof-carrying codenecula96,necula97:popl.

Another broad area of future work is designing safe FFIs between practical typed languages that compile to RichWasm.

Beyond that, we would like to support safe interop between type-safe languages compiled to RichWasm and unsafe languages such as C and C++ compiled to Wasm. The simplest solution for safe interop is to use Component Model interface types at the boundary between RichWasm (compiled to Wasm) and Wasm modules, ensuring that safe and unsafe code never mix. If we do want to support memory sharing between RichWasm and Wasm, the interop between more precisely and less precisely typed modules is reminicent of gradual typing <cit.>, but more general since the term languages have differences. This essentially requires tackling gradual typing between a language with linear capability types and one without. We plan to design a -Wasm multilanguage, which would have to identify the static guarantees or dynamic checks we need at boundaries; then we will investigate a combination of type inference and static contract verification to eliminate these static and dynamic checks. Interop of with MSWasm <cit.> would be an easier way of achieving the goal since MSWasm already supports dynamic capability checking,

Missing 'biblatex' package
The bibliography requires the 'biblatex' package.

booktitleInternational Conference on Functional Programming (ICFP)
titleA Step-Indexed Model of Substructural State

journaltitleFundamenta Informaticae
titleL3 : A Linear Language with Locations

titleEffect handlers for WebAssembly

titleComponent Model Design and Specification

titleMulti Memory Proposal for WebAssembly

titleBringing the web up to speed with WebAssembly

booktitleACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI)
titleA Garbage-Collecting Typed Assembly Language

New York, NY, USA

Association for Computing Machinery

journaltitleProc. ACM Program. Lang.
titleMSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code
WebAssembly,Memory-safety,Semantics,Secure Compilation

booktitleACM Symposium on Principles of Programming Languages (POPL), St. Petersburg Beach, Florida
titleTyped Closure Conversion

Springer Berlin Heidelberg

titleL3: A Linear Language with Locations

journaltitleACM Transactions on Programming Languages and Systems
titleFrom System F to Typed Assembly Language

journaltitleJournal of Functional Programming
titleStack-based typed assembly language

Dagstuhl, Germany

Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik

booktitle2nd Summit on Advances in Programming Languages (SNAPL 2017)
seriesLeibniz International Proceedings in Informatics (LIPIcs)
titleLinking Types for Multi-Language Software: Have Your Cake and Eat It Too

San Diego, CA, USA

Association for Computing Machinery

booktitleProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation
seriesPLDI 2022
titleSemantic Soundness for Language Interoperability
semantics,language interoperability,logical relations,type soundness

journaltitleProceedings of the ACM on Programming Languages (PACMPL)
titleContinuing WebAssembly with Effect Handlers

New York, NY, USA

Association for Computing Machinery

journaltitleProc. ACM Program. Lang.
titleIris-Wasm: Robust and Modular Verification of WebAssembly Programs
separation logic,higher-order logic,formal verification,WebAssembly

booktitleScheme and Functional Programming Workshop (Scheme)
titleGradual Typing for Functional Languages

booktitleACM Symposium on Principles of Programming Languages (POPL), St. Petersburg, Florida
titleIs Sound Gradual Typing Dead?

booktitleDynamic Languages Symposium (DLS)
titleInterlanguage Migration: From Scripts to Programs

IEEE Computer Society

abstractCHERI extends a conventional RISC Instruction-Set Architecture, compiler, and operating system to support fine-grained, capability-based memory protection to mitigate memory-related vulnerabilities in C-language TCBs. We describe how CHERI capabilities can also underpin a hardware-software object-capability model for application compartmentalization that can mitigate broader classes of attack. Prototyped as an extension to the open-source 64-bit BERI RISC FPGA soft-core processor, Free BSD operating system, and LLVM compiler, we demonstrate multiple orders-of-magnitude improvement in scalability, simplified programmability, and resulting tangible security benefits as compared to compartmentalization based on pure Memory-Management Unit (MMU) designs. We evaluate incrementally deployable CHERI-based compartmentalization using several real-world UNIX libraries and applications.
booktitleProceedings of the 2015 IEEE Symposium on Security and Privacy
seriesSP '15
titleCHERI: A Hybrid Capability-System Architecture for Scalable Software Compartmentalization
software compartmentalization,CHERI processor,object capabilities,capability system,computer architecture,memory protection