1.1.1. Design Goals

The design goals of WebAssembly are the following:

• Fast, safe, and portable semantics:
  • Fast: executes with near native code performance, taking advantage of capabilities common to all contemporary hardware.
  • Safe: code is validated and executes in a memory-safe [2], sandboxed environment preventing data corruption or security breaches.
  • Well-defined: fully and precisely defines valid programs and their behavior in a way that is easy to reason about informally and formally.
  • Hardware-independent: can be compiled on all modern architectures, desktop or mobile devices and embedded systems alike.
  • Language-independent: does not privilege any particular language, programming model, or object model.
  • Platform-independent: can be embedded in browsers, run as a stand-alone VM, or integrated in other environments.
  • Open: programs can interoperate with their environment in a simple and universal manner.
• Efficient and portable representation:
  • Compact: has a binary format that is fast to transmit by being smaller than typical text or native code formats.
  • Modular: programs can be split up in smaller parts that can be transmitted, cached, and consumed separately.
  • Efficient: can be decoded, validated, and compiled in a fast single pass, equally with either just-in-time (JIT) or ahead-of-time (AOT) compilation.
  • Streamable: allows decoding, validation, and compilation to begin as soon as possible, before all data has been seen.
  • Parallelizable: allows decoding, validation, and compilation to be split into many independent parallel tasks.
  • Portable: makes no architectural assumptions that are not broadly supported across modern hardware.

WebAssembly code is also intended to be easy to inspect and debug, especially in environments like web browsers, but such features are beyond the scope of this specification.

1.1.2. Scope

At its core, WebAssembly is a virtual instruction set architecture (virtual ISA). As such, it has many use cases and can be embedded in many different environments. To encompass their variety and enable maximum reuse, the WebAssembly specification is split and layered into several documents.

This document is concerned with the core ISA layer of WebAssembly. It defines the instruction set, binary encoding, validation, and execution semantics, as well as a textual representation. It does not, however, define how WebAssembly programs can interact with a specific environment they execute in, nor how they are invoked from such an environment.

Instead, this specification is complemented by additional documents defining interfaces to specific embedding environments such as the Web. These will each define a WebAssembly application programming interface (API) suitable for a given environment.

1.2.1. Dependencies

WebAssembly depends on two existing standards:

• [IEEE-754-2019], for the representation of floating-point data and the semantics of respective numeric operations.
• [UNICODE], for the representation of import/export names and the text format.

However, to make this specification self-contained, relevant aspects of the aforementioned standards are defined and formalized as part of this specification, such as the binary representation and rounding of floating-point values, and the value range and UTF-8 encoding of Unicode characters.

1.3.1. Concepts

WebAssembly encodes a low-level, assembly-like programming language. This language is structured around the following concepts.

Values

WebAssembly provides only four basic value types. These are integers and [IEEE-754-2019] numbers, each in 32 and 64 bit width. 32 bit integers also serve as Booleans and as memory addresses. The usual operations on these types are available, including the full matrix of conversions between them. There is no distinction between signed and unsigned integer types. Instead, integers are interpreted by respective operations as either unsigned or signed in two’s complement representation.

Instructions

The computational model of WebAssembly is based on a stack machine. Code consists of sequences of instructions that are executed in order. Instructions manipulate values on an implicit operand stack [1] and fall into two main categories. Simple instructions perform basic operations on data. They pop arguments from the operand stack and push results back to it. Control instructions alter control flow. Control flow is structured, meaning it is expressed with well-nested constructs such as blocks, loops, and conditionals. Branches can only target such constructs.

Traps

Under some conditions, certain instructions may produce a trap, which immediately aborts execution. Traps cannot be handled by WebAssembly code, but are reported to the outside environment, where they typically can be caught.

Functions

Code is organized into separate functions. Each function takes a sequence of values as parameters and returns a sequence of values as results. [2] Functions can call each other, including recursively, resulting in an implicit call stack that cannot be accessed directly. Functions may also declare mutable local variables that are usable as virtual registers.

Tables

A table is an array of opaque values of a particular element type. It allows programs to select such values indirectly through a dynamic index operand. Currently, the only available element type is an untyped function reference. Thereby, a program can call functions indirectly through a dynamic index into a table. For example, this allows emulating function pointers by way of table indices.

Linear Memory

A linear memory is a contiguous, mutable array of raw bytes. Such a memory is created with an initial size but can be grown dynamically. A program can load and store values from/to a linear memory at any byte address (including unaligned). Integer loads and stores can specify a storage size which is smaller than the size of the respective value type. A trap occurs if an access is not within the bounds of the current memory size.

Modules

A WebAssembly binary takes the form of a module that contains definitions for functions, tables, and linear memories, as well as mutable or immutable global variables. Definitions can also be imported, specifying a module/name pair and a suitable type. Each definition can optionally be exported under one or more names. In addition to definitions, modules can define initialization data for their memories or tables that takes the form of segments copied to given offsets. They can also define a start function that is automatically executed.

Embedder

A WebAssembly implementation will typically be embedded into a host environment. This environment defines how loading of modules is initiated, how imports are provided (including host-side definitions), and how exports can be accessed. However, the details of any particular embedding are beyond the scope of this specification, and will instead be provided by complementary, environment-specific API definitions.

1.3.2. Semantic Phases

Conceptually, the semantics of WebAssembly is divided into three phases. For each part of the language, the specification specifies each of them.

Decoding

WebAssembly modules are distributed in a binary format. Decoding processes that format and converts it into an internal representation of a module. In this specification, this representation is modelled by abstract syntax, but a real implementation could compile directly to machine code instead.

Validation

A decoded module has to be valid. Validation checks a number of well-formedness conditions to guarantee that the module is meaningful and safe. In particular, it performs type checking of functions and the instruction sequences in their bodies, ensuring for example that the operand stack is used consistently.

Execution

Finally, a valid module can be executed. Execution can be further divided into two phases:

Instantiation. A module instance is the dynamic representation of a module, complete with its own state and execution stack. Instantiation executes the module body itself, given definitions for all its imports. It initializes globals, memories and tables and invokes the module’s start function if defined. It returns the instances of the module’s exports.

Invocation. Once instantiated, further WebAssembly computations can be initiated by invoking an exported function on a module instance. Given the required arguments, that executes the respective function and returns its results.

Instantiation and invocation are operations within the embedding environment.

2.1.1. Grammar Notation

The following conventions are adopted in defining grammar rules for abstract syntax.

• Terminal symbols (atoms) are written in sans-serif font: $$\mathsf{i}32,\mathsf{e}\mathsf{n}\mathsf{d}$$.
• Nonterminal symbols are written in italic font: $$valtype,instr$$.
• $${\mathrm{A}}^{\mathrm{n}}$$ is a sequence of $$\mathrm{n}\ge 0$$ iterations of $$\mathrm{A}$$.
• $${\mathrm{A}}^{\ast }$$ is a possibly empty sequence of iterations of $$\mathrm{A}$$. (This is a shorthand for $${\mathrm{A}}^{\mathrm{n}}$$ used where $$\mathrm{n}$$ is not relevant.)
• $${\mathrm{A}}^{+}$$ is a non-empty sequence of iterations of $$\mathrm{A}$$. (This is a shorthand for $${\mathrm{A}}^{\mathrm{n}}$$ where $$\mathrm{n}\ge 1$$.)
• $${\mathrm{A}}^{?}$$ is an optional occurrence of $$\mathrm{A}$$. (This is a shorthand for $${\mathrm{A}}^{\mathrm{n}}$$ where $$\mathrm{n}\le 1$$.)
• Productions are written $$sym::={\mathrm{A}}_1|\dots |{\mathrm{A}}_{\mathrm{n}}$$.
• Large productions may be split into multiple definitions, indicated by ending the first one with explicit ellipses, $$sym::={\mathrm{A}}_1|\dots$$, and starting continuations with ellipses, $$sym::=\dots |{\mathrm{A}}_2$$.
• Some productions are augmented with side conditions in parentheses, “$$(\text{if}condition)$$”, that provide a shorthand for a combinatorial expansion of the production into many separate cases.

2.1.2. Auxiliary Notation

When dealing with syntactic constructs the following notation is also used:

• $$ϵ$$ denotes the empty sequence.
• $$|\mathrm{s}|$$ denotes the length of a sequence $$\mathrm{s}$$.
• $$\mathrm{s}[\mathrm{i}]$$ denotes the $$\mathrm{i}$$-th element of a sequence $$\mathrm{s}$$, starting from $$0$$.
• $$\mathrm{s}[\mathrm{i}:\mathrm{n}]$$ denotes the sub-sequence $$\mathrm{s}[\mathrm{i}]\dots \mathrm{s}[\mathrm{i}+\mathrm{n}-1]$$ of a sequence $$\mathrm{s}$$.
• $$\mathrm{s}\text{with}[\mathrm{i}]=\mathrm{A}$$ denotes the same sequence as $$\mathrm{s}$$, except that the $$\mathrm{i}$$-th element is replaced with $$\mathrm{A}$$.
• $$\mathrm{s}\text{with}[\mathrm{i}:\mathrm{n}]={\mathrm{A}}^{\mathrm{n}}$$ denotes the same sequence as $$\mathrm{s}$$, except that the sub-sequence $$\mathrm{s}[\mathrm{i}:\mathrm{n}]$$ is replaced with $${\mathrm{A}}^{\mathrm{n}}$$.
• $$\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{c}\mathrm{a}\mathrm{t}({\mathrm{s}}^{\ast })$$ denotes the flat sequence formed by concatenating all sequences $${\mathrm{s}}_{\mathrm{i}}$$ in $${\mathrm{s}}^{\ast }$$.

Moreover, the following conventions are employed:

• The notation $${\mathrm{x}}^{\mathrm{n}}$$, where $$\mathrm{x}$$ is a non-terminal symbol, is treated as a meta variable ranging over respective sequences of $$\mathrm{x}$$ (similarly for $${\mathrm{x}}^{\ast }$$, $${\mathrm{x}}^{+}$$, $${\mathrm{x}}^{?}$$).
• When given a sequence $${\mathrm{x}}^{\mathrm{n}}$$, then the occurrences of $$\mathrm{x}$$ in a sequence written $$({\mathrm{A}}_1\mathrm{x}{\mathrm{A}}_2{)}^{\mathrm{n}}$$ are assumed to be in point-wise correspondence with $${\mathrm{x}}^{\mathrm{n}}$$ (similarly for $${\mathrm{x}}^{\ast }$$, $${\mathrm{x}}^{+}$$, $${\mathrm{x}}^{?}$$). This implicitly expresses a form of mapping syntactic constructions over a sequence.

Productions of the following form are interpreted as records that map a fixed set of fields $${\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}}_{\mathrm{i}}$$ to “values” $${\mathrm{A}}_{\mathrm{i}}$$, respectively:

The following notation is adopted for manipulating such records:

• $$\mathrm{r}.\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}$$ denotes the contents of the $$\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}$$ component of $$\mathrm{r}$$.

• $$\mathrm{r}\text{with}\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}=\mathrm{A}$$ denotes the same record as $$\mathrm{r}$$, except that the contents of the $$\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}$$ component is replaced with $$\mathrm{A}$$.

• $${\mathrm{r}}_1\oplus {\mathrm{r}}_2$$ denotes the composition of two records with the same fields of sequences by appending each sequence point-wise:

  $$\{{\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}}_1{\mathrm{A}}_1^{\ast },{\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}}_2{\mathrm{A}}_2^{\ast },\dots \}\oplus \{{\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}}_1{\mathrm{B}}_1^{\ast },{\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}}_2{\mathrm{B}}_2^{\ast },\dots \}=\{{\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}}_1{\mathrm{A}}_1^{\ast }{\mathrm{B}}_1^{\ast },{\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}}_2{\mathrm{A}}_2^{\ast }{\mathrm{B}}_2^{\ast },\dots \}$$

• $$⨁{\mathrm{r}}^{\ast }$$ denotes the composition of a sequence of records, respectively; if the sequence is empty, then all fields of the resulting record are empty.

The update notation for sequences and records generalizes recursively to nested components accessed by “paths” $$pth::=([\dots ]|.\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}{)}^{+}$$:

• $$\mathrm{s}\text{with}[\mathrm{i}]pth=\mathrm{A}$$ is short for $$\mathrm{s}\text{with}[\mathrm{i}]=(\mathrm{s}[\mathrm{i}]\text{with}pth=\mathrm{A})$$.
• $$\mathrm{r}\text{with}\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}pth=\mathrm{A}$$ is short for $$\mathrm{r}\text{with}\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}=(\mathrm{r}.\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}\text{with}pth=\mathrm{A})$$.

where $$\mathrm{r}\text{with}.\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}=\mathrm{A}$$ is shortened to $$\mathrm{r}\text{with}\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}=\mathrm{A}$$.

2.1.3. Vectors

Vectors are bounded sequences of the form $${\mathrm{A}}^{\mathrm{n}}$$ (or $${\mathrm{A}}^{\ast }$$), where the $$\mathrm{A}$$ can either be values or complex constructions. A vector can have at most $$2^{32}-1$$ elements.

2.2.1. Bytes

The simplest form of value are raw uninterpreted bytes. In the abstract syntax they are represented as hexadecimal literals.

2.2.2. Integers

Different classes of integers with different value ranges are distinguished by their bit width $$\mathrm{N}$$ and by whether they are unsigned or signed.

The latter class defines uninterpreted integers, whose signedness interpretation can vary depending on context. In the abstract syntax, they are represented as unsigned values. However, some operations convert them to signed based on a two’s complement interpretation.

2.2.3. Floating-Point

Floating-point data represents 32 or 64 bit values that correspond to the respective binary formats of the [IEEE-754-2019] standard (Section 3.3).

Every value has a sign and a magnitude. Magnitudes can either be expressed as normal numbers of the form $${\mathrm{m}}_0.{\mathrm{m}}_1{\mathrm{m}}_2\dots {\mathrm{m}}_{\mathrm{M}}\cdot 2^{\mathrm{e}}$$, where $$\mathrm{e}$$ is the exponent and $$\mathrm{m}$$ is the significand whose most signifcant bit $${\mathrm{m}}_0$$ is $$1$$, or as a subnormal number where the exponent is fixed to the smallest possible value and $${\mathrm{m}}_0$$ is $$0$$; among the subnormals are positive and negative zero values. Since the significands are binary values, normals are represented in the form $$(1+\mathrm{m}\cdot 2^{-\mathrm{M}})\cdot 2^{\mathrm{e}}$$, where $$\mathrm{M}$$ is the bit width of $$\mathrm{m}$$; similarly for subnormals.

Possible magnitudes also include the special values $$\infty$$ (infinity) and $$\mathsf{n}\mathsf{a}\mathsf{n}$$ (NaN, not a number). NaN values have a payload that describes the mantissa bits in the underlying binary representation. No distinction is made between signalling and quiet NaNs.

where $$\mathrm{M}=\mathrm{s}\mathrm{i}\mathrm{g}\mathrm{n}\mathrm{i}\mathrm{f}(\mathrm{N})$$ and $$\mathrm{E}=\mathrm{e}\mathrm{x}\mathrm{p}\mathrm{o}\mathrm{n}(\mathrm{N})$$ with

A canonical NaN is a floating-point value $$\pm \mathsf{n}\mathsf{a}\mathsf{n}({\mathrm{c}\mathrm{a}\mathrm{n}\mathrm{o}\mathrm{n}}_{\mathrm{N}})$$ where $${\mathrm{c}\mathrm{a}\mathrm{n}\mathrm{o}\mathrm{n}}_{\mathrm{N}}$$ is a payload whose most significant bit is $$1$$ while all others are $$0$$:

An arithmetic NaN is a floating-point value $$\pm \mathsf{n}\mathsf{a}\mathsf{n}(\mathrm{n})$$ with $$\mathrm{n}\ge {\mathrm{c}\mathrm{a}\mathrm{n}\mathrm{o}\mathrm{n}}_{\mathrm{N}}$$, such that the most significant bit is $$1$$ while all others are arbitrary.

2.2.4. Names

Names are sequences of characters, which are scalar values as defined by [UNICODE] (Section 2.4).

Due to the limitations of the binary format, the length of a name is bounded by the length of its UTF-8 encoding.

2.3.1. Value Types

Value types classify the individual values that WebAssembly code can compute with and the values that a variable accepts.

The types $$\mathsf{i}32$$ and $$\mathsf{i}64$$ classify 32 and 64 bit integers, respectively. Integers are not inherently signed or unsigned, their interpretation is determined by individual operations.

The types $$\mathsf{f}32$$ and $$\mathsf{f}64$$ classify 32 and 64 bit floating-point data, respectively. They correspond to the respective binary floating-point representations, also known as single and double precision, as defined by the [IEEE-754-2019] standard (Section 3.3).

2.3.2. Result Types

Result types classify the result of executing instructions or blocks, which is a sequence of values written with brackets.

2.3.3. Function Types

Function types classify the signature of functions, mapping a vector of parameters to a vector of results, written as follows.

2.3.4. Limits

Limits classify the size range of resizeable storage associated with memory types and table types.

If no maximum is given, the respective storage can grow to any size.

2.3.5. Memory Types

Memory types classify linear memories and their size range.

The limits constrain the minimum and optionally the maximum size of a memory. The limits are given in units of page size.

2.3.6. Table Types

Table types classify tables over elements of element types within a size range.

Like memories, tables are constrained by limits for their minimum and optionally maximum size. The limits are given in numbers of entries.

The element type $$\mathsf{f}\mathsf{u}\mathsf{n}\mathsf{c}\mathsf{r}\mathsf{e}\mathsf{f}$$ is the infinite union of all function types. A table of that type thus contains references to functions of heterogeneous type.

2.3.7. Global Types

Global types classify global variables, which hold a value and can either be mutable or immutable.

2.3.8. External Types

External types classify imports and external values with their respective types.

2.4.1. Numeric Instructions

Numeric instructions provide basic operations over numeric values of specific type. These operations closely match respective operations available in hardware.

Numeric instructions are divided by value type. For each type, several subcategories can be distinguished:

• Constants: return a static constant.
• Unary Operators: consume one operand and produce one result of the respective type.
• Binary Operators: consume two operands and produce one result of the respective type.
• Tests: consume one operand of the respective type and produce a Boolean integer result.
• Comparisons: consume two operands of the respective type and produce a Boolean integer result.
• Conversions: consume a value of one type and produce a result of another (the source type of the conversion is the one after the “$$\_$$”).

Some integer instructions come in two flavors, where a signedness annotation $$sx$$ distinguishes whether the operands are to be interpreted as unsigned or signed integers. For the other integer instructions, the use of two’s complement for the signed interpretation means that they behave the same regardless of signedness.

2.4.2. Parametric Instructions

Instructions in this group can operate on operands of any value type.

The $$\mathsf{d}\mathsf{r}\mathsf{o}\mathsf{p}$$ operator simply throws away a single operand.

The $$\mathsf{s}\mathsf{e}\mathsf{l}\mathsf{e}\mathsf{c}\mathsf{t}$$ operator selects one of its first two operands based on whether its third operand is zero or not.

2.4.3. Variable Instructions

Variable instructions are concerned with access to local or global variables.

These instructions get or set the values of variables, respectively. The $$\mathsf{l}\mathsf{o}\mathsf{c}\mathsf{a}\mathsf{l}.\mathsf{t}\mathsf{e}\mathsf{e}$$ instruction is like $$\mathsf{l}\mathsf{o}\mathsf{c}\mathsf{a}\mathsf{l}.\mathsf{s}\mathsf{e}\mathsf{t}$$ but also returns its argument.

2.4.4. Memory Instructions

Instructions in this group are concerned with linear memory.

Memory is accessed with $$\mathsf{l}\mathsf{o}\mathsf{a}\mathsf{d}$$ and $$\mathsf{s}\mathsf{t}\mathsf{o}\mathsf{r}\mathsf{e}$$ instructions for the different value types. They all take a memory immediate $$memarg$$ that contains an address offset and the expected alignment (expressed as the exponent of a power of 2). Integer loads and stores can optionally specify a storage size that is smaller than the bit width of the respective value type. In the case of loads, a sign extension mode $$sx$$ is then required to select appropriate behavior.

The static address offset is added to the dynamic address operand, yielding a 33 bit effective address that is the zero-based index at which the memory is accessed. All values are read and written in little endian byte order. A trap results if any of the accessed memory bytes lies outside the address range implied by the memory’s current size.

The $$\mathsf{m}\mathsf{e}\mathsf{m}\mathsf{o}\mathsf{r}\mathsf{y}.\mathsf{s}\mathsf{i}\mathsf{z}\mathsf{e}$$ instruction returns the current size of a memory. The $$\mathsf{m}\mathsf{e}\mathsf{m}\mathsf{o}\mathsf{r}\mathsf{y}.\mathsf{g}\mathsf{r}\mathsf{o}\mathsf{w}$$ instruction grows memory by a given delta and returns the previous size, or $$-1$$ if enough memory cannot be allocated. Both instructions operate in units of page size.

2.4.5. Control Instructions

Instructions in this group affect the flow of control.

The $$\mathsf{n}\mathsf{o}\mathsf{p}$$ instruction does nothing.

The $$\mathsf{u}\mathsf{n}\mathsf{r}\mathsf{e}\mathsf{a}\mathsf{c}\mathsf{h}\mathsf{a}\mathsf{b}\mathsf{l}\mathsf{e}$$ instruction causes an unconditional trap.

The $$\mathsf{b}\mathsf{l}\mathsf{o}\mathsf{c}\mathsf{k}$$, $$\mathsf{l}\mathsf{o}\mathsf{o}\mathsf{p}$$ and $$\mathsf{i}\mathsf{f}$$ instructions are structured instructions. They bracket nested sequences of instructions, called blocks, terminated with, or separated by, $$\mathsf{e}\mathsf{n}\mathsf{d}$$ or $$\mathsf{e}\mathsf{l}\mathsf{s}\mathsf{e}$$ pseudo-instructions. As the grammar prescribes, they must be well-nested. A structured instruction can produce a value as described by the annotated result type.

Each structured control instruction introduces an implicit label. Labels are targets for branch instructions that reference them with label indices. Unlike with other index spaces, indexing of labels is relative by nesting depth, that is, label $$0$$ refers to the innermost structured control instruction enclosing the referring branch instruction, while increasing indices refer to those farther out. Consequently, labels can only be referenced from within the associated structured control instruction. This also implies that branches can only be directed outwards, “breaking” from the block of the control construct they target. The exact effect depends on that control construct. In case of $$\mathsf{b}\mathsf{l}\mathsf{o}\mathsf{c}\mathsf{k}$$ or $$\mathsf{i}\mathsf{f}$$ it is a forward jump, resuming execution after the matching $$\mathsf{e}\mathsf{n}\mathsf{d}$$. In case of $$\mathsf{l}\mathsf{o}\mathsf{o}\mathsf{p}$$ it is a backward jump to the beginning of the loop.

Branch instructions come in several flavors: $$\mathsf{b}\mathsf{r}$$ performs an unconditional branch, $$\mathsf{b}\mathsf{r}\_\mathsf{i}\mathsf{f}$$ performs a conditional branch, and $$\mathsf{b}\mathsf{r}\_\mathsf{t}\mathsf{a}\mathsf{b}\mathsf{l}\mathsf{e}$$ performs an indirect branch through an operand indexing into the label vector that is an immediate to the instruction, or to a default target if the operand is out of bounds. The $$\mathsf{r}\mathsf{e}\mathsf{t}\mathsf{u}\mathsf{r}\mathsf{n}$$ instruction is a shortcut for an unconditional branch to the outermost block, which implicitly is the body of the current function. Taking a branch unwinds the operand stack up to the height where the targeted structured control instruction was entered. However, forward branches that target a control instruction with a non-empty result type consume matching operands first and push them back on the operand stack after unwinding, as a result for the terminated structured instruction.

The $$\mathsf{c}\mathsf{a}\mathsf{l}\mathsf{l}$$ instruction invokes another function, consuming the necessary arguments from the stack and returning the result values of the call. The $$\mathsf{c}\mathsf{a}\mathsf{l}\mathsf{l}\_\mathsf{i}\mathsf{n}\mathsf{d}\mathsf{i}\mathsf{r}\mathsf{e}\mathsf{c}\mathsf{t}$$ instruction calls a function indirectly through an operand indexing into a table. Since tables may contain function elements of heterogeneous type $$\mathsf{f}\mathsf{u}\mathsf{n}\mathsf{c}\mathsf{r}\mathsf{e}\mathsf{f}$$, the callee is dynamically checked against the function type indexed by the instruction’s immediate, and the call aborted with a trap if it does not match.

2.4.6. Expressions

Function bodies, initialization values for globals, and offsets of element or data segments are given as expressions, which are sequences of instructions terminated by an $$\mathsf{e}\mathsf{n}\mathsf{d}$$ marker.

In some places, validation restricts expressions to be constant, which limits the set of allowable instructions.

2.5.1. Indices

Definitions are referenced with zero-based indices. Each class of definition has its own index space, as distinguished by the following classes.

The index space for functions, tables, memories and globals includes respective imports declared in the same module. The indices of these imports precede the indices of other definitions in the same index space.

The index space for locals is only accessible inside a function and includes the parameters of that function, which precede the local variables.

Label indices reference structured control instructions inside an instruction sequence.

2.5.2. Types

The $$\mathsf{t}\mathsf{y}\mathsf{p}\mathsf{e}\mathsf{s}$$ component of a module defines a vector of function types.

All function types used in a module must be defined in this component. They are referenced by type indices.

2.5.3. Functions

The $$\mathsf{f}\mathsf{u}\mathsf{n}\mathsf{c}\mathsf{s}$$ component of a module defines a vector of functions with the following structure:

The $$\mathsf{t}\mathsf{y}\mathsf{p}\mathsf{e}$$ of a function declares its signature by reference to a type defined in the module. The parameters of the function are referenced through 0-based local indices in the function’s body; they are mutable.

The $$\mathsf{l}\mathsf{o}\mathsf{c}\mathsf{a}\mathsf{l}\mathsf{s}$$ declare a vector of mutable local variables and their types. These variables are referenced through local indices in the function’s body. The index of the first local is the smallest index not referencing a parameter.

The $$\mathsf{b}\mathsf{o}\mathsf{d}\mathsf{y}$$ is an instruction sequence that upon termination must produce a stack matching the function type’s result type.

Functions are referenced through function indices, starting with the smallest index not referencing a function import.

2.5.4. Tables

The $$\mathsf{t}\mathsf{a}\mathsf{b}\mathsf{l}\mathsf{e}\mathsf{s}$$ component of a module defines a vector of tables described by their table type:

A table is a vector of opaque values of a particular table element type. The $$\mathsf{m}\mathsf{i}\mathsf{n}$$ size in the limits of the table type specifies the initial size of that table, while its $$\mathsf{m}\mathsf{a}\mathsf{x}$$, if present, restricts the size to which it can grow later.

Tables can be initialized through element segments.

Tables are referenced through table indices, starting with the smallest index not referencing a table import. Most constructs implicitly reference table index $$0$$.

2.5.5. Memories

The $$\mathsf{m}\mathsf{e}\mathsf{m}\mathsf{s}$$ component of a module defines a vector of linear memories (or memories for short) as described by their memory type:

A memory is a vector of raw uninterpreted bytes. The $$\mathsf{m}\mathsf{i}\mathsf{n}$$ size in the limits of the memory type specifies the initial size of that memory, while its $$\mathsf{m}\mathsf{a}\mathsf{x}$$, if present, restricts the size to which it can grow later. Both are in units of page size.

Memories can be initialized through data segments.

Memories are referenced through memory indices, starting with the smallest index not referencing a memory import. Most constructs implicitly reference memory index $$0$$.

2.5.6. Globals

The $$\mathsf{g}\mathsf{l}\mathsf{o}\mathsf{b}\mathsf{a}\mathsf{l}\mathsf{s}$$ component of a module defines a vector of global variables (or globals for short):

Each global stores a single value of the given global type. Its $$\mathsf{t}\mathsf{y}\mathsf{p}\mathsf{e}$$ also specifies whether a global is immutable or mutable. Moreover, each global is initialized with an $$\mathsf{i}\mathsf{n}\mathsf{i}\mathsf{t}$$ value given by a constant initializer expression.

Globals are referenced through global indices, starting with the smallest index not referencing a global import.

2.5.7. Element Segments

The initial contents of a table is uninitialized. The $$\mathsf{e}\mathsf{l}\mathsf{e}\mathsf{m}$$ component of a module defines a vector of element segments that initialize a subrange of a table, at a given offset, from a static vector of elements.

The $$\mathsf{o}\mathsf{f}\mathsf{f}\mathsf{s}\mathsf{e}\mathsf{t}$$ is given by a constant expression.

2.5.8. Data Segments

The initial contents of a memory are zero-valued bytes. The $$\mathsf{d}\mathsf{a}\mathsf{t}\mathsf{a}$$ component of a module defines a vector of data segments that initialize a range of memory, at a given offset, with a static vector of bytes.

The $$\mathsf{o}\mathsf{f}\mathsf{f}\mathsf{s}\mathsf{e}\mathsf{t}$$ is given by a constant expression.

2.5.9. Start Function

The $$\mathsf{s}\mathsf{t}\mathsf{a}\mathsf{r}\mathsf{t}$$ component of a module declares the function index of a start function that is automatically invoked when the module is instantiated, after tables and memories have been initialized.

2.5.10. Exports

The $$\mathsf{e}\mathsf{x}\mathsf{p}\mathsf{o}\mathsf{r}\mathsf{t}\mathsf{s}$$ component of a module defines a set of exports that become accessible to the host environment once the module has been instantiated.

Each export is labeled by a unique name. Exportable definitions are functions, tables, memories, and globals, which are referenced through a respective descriptor.

2.5.11. Imports

The $$\mathsf{i}\mathsf{m}\mathsf{p}\mathsf{o}\mathsf{r}\mathsf{t}\mathsf{s}$$ component of a module defines a set of imports that are required for instantiation.

Each import is labeled by a two-level name space, consisting of a $$\mathsf{m}\mathsf{o}\mathsf{d}\mathsf{u}\mathsf{l}\mathsf{e}$$ name and a $$\mathsf{n}\mathsf{a}\mathsf{m}\mathsf{e}$$ for an entity within that module. Importable definitions are functions, tables, memories, and globals. Each import is specified by a descriptor with a respective type that a definition provided during instantiation is required to match.

Every import defines an index in the respective index space. In each index space, the indices of imports go before the first index of any definition contained in the module itself.

3.1.1. Contexts

Validity of an individual definition is specified relative to a context, which collects relevant information about the surrounding module and the definitions in scope:

• Types: the list of types defined in the current module.
• Functions: the list of functions declared in the current module, represented by their function type.
• Tables: the list of tables declared in the current module, represented by their table type.
• Memories: the list of memories declared in the current module, represented by their memory type.
• Globals: the list of globals declared in the current module, represented by their global type.
• Locals: the list of locals declared in the current function (including parameters), represented by their value type.
• Labels: the stack of labels accessible from the current position, represented by their result type.
• Return: the return type of the current function, represented as an optional result type that is absent when no return is allowed, as in free-standing expressions.

In other words, a context contains a sequence of suitable types for each index space, describing each defined entry in that space. Locals, labels and return type are only used for validating instructions in function bodies, and are left empty elsewhere. The label stack is the only part of the context that changes as validation of an instruction sequence proceeds.

More concretely, contexts are defined as records $$\mathrm{C}$$ with abstract syntax:

In addition to field access written $$\mathrm{C}.\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}$$ the following notation is adopted for manipulating contexts:

• When spelling out a context, empty fields are omitted.
• $$\mathrm{C},\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}{\mathrm{A}}^{\ast }$$ denotes the same context as $$\mathrm{C}$$ but with the elements $${\mathrm{A}}^{\ast }$$ prepended to its $$\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}$$ component sequence.

3.1.2. Prose Notation

Validation is specified by stylised rules for each relevant part of the abstract syntax. The rules not only state constraints defining when a phrase is valid, they also classify it with a type. The following conventions are adopted in stating these rules.

• A phrase $$\mathrm{A}$$ is said to be “valid with type $$\mathrm{T}$$” if and only if all constraints expressed by the respective rules are met. The form of $$\mathrm{T}$$ depends on what $$\mathrm{A}$$ is.

  Note

  For example, if $$\mathrm{A}$$ is a function, then $$\mathrm{T}$$ is a function type; for an $$\mathrm{A}$$ that is a global, $$\mathrm{T}$$ is a global type; and so on.

• The rules implicitly assume a given context $$\mathrm{C}$$.

• In some places, this context is locally extended to a context $${\mathrm{C}}^{\prime }$$ with additional entries. The formulation “Under context $${\mathrm{C}}^{\prime }$$, … statement …” is adopted to express that the following statement must apply under the assumptions embodied in the extended context.

3.1.3. Formal Notation

The proposition that a phrase $$\mathrm{A}$$ has a respective type $$\mathrm{T}$$ is written $$\mathrm{A}:\mathrm{T}$$. In general, however, typing is dependent on a context $$\mathrm{C}$$. To express this explicitly, the complete form is a judgement $$\mathrm{C}⊢\mathrm{A}:\mathrm{T}$$, which says that $$\mathrm{A}:\mathrm{T}$$ holds under the assumptions encoded in $$\mathrm{C}$$.

The formal typing rules use a standard approach for specifying type systems, rendering them into deduction rules. Every rule has the following general form:

Such a rule is read as a big implication: if all premises hold, then the conclusion holds. Some rules have no premises; they are axioms whose conclusion holds unconditionally. The conclusion always is a judgment $$\mathrm{C}⊢\mathrm{A}:\mathrm{T}$$, and there is one respective rule for each relevant construct $$\mathrm{A}$$ of the abstract syntax.

3.2.1. Limits

Limits must have meaningful bounds that are within a given range.

3.2.2. Function Types

Function types may not specify more than one result.