Conventions¶

Validation checks that a WebAssembly module is well-formed. Only valid modules can be instantiated.

Validity is defined by a type system over the abstract syntax of a module and its contents. For each piece of abstract syntax, there is a typing rule that specifies the constraints that apply to it. All rules are given in two equivalent forms:

In prose, describing the meaning in intuitive form.
In formal notation, describing the rule in mathematical form. 1

Note

The prose and formal rules are equivalent, so that understanding of the formal notation is not required to read this specification. The formalism offers a more concise description in notation that is used widely in programming languages semantics and is readily amenable to mathematical proof.

In both cases, the rules are formulated in a declarative manner. That is, they only formulate the constraints, they do not define an algorithm. The skeleton of a sound and complete algorithm for type-checking instruction sequences according to this specification is provided in the appendix.

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 \(C\) with abstract syntax:

\[\begin{split}\begin{array}{llll} \def\mathdef2564#1{{}}\mathdef2564{(context)} & C &::=& \begin{array}[t]{l@{~}ll} \{ & \href{../valid/conventions.html#context}{\mathsf{types}} & \href{../syntax/types.html#syntax-functype}{\mathit{functype}}^\ast, \\ & \href{../valid/conventions.html#context}{\mathsf{funcs}} & \href{../syntax/types.html#syntax-functype}{\mathit{functype}}^\ast, \\ & \href{../valid/conventions.html#context}{\mathsf{tables}} & \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}^\ast, \\ & \href{../valid/conventions.html#context}{\mathsf{mems}} & \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}^\ast, \\ & \href{../valid/conventions.html#context}{\mathsf{globals}} & \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}^\ast, \\ & \href{../valid/conventions.html#context}{\mathsf{locals}} & \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}^\ast, \\ & \href{../valid/conventions.html#context}{\mathsf{labels}} & \href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}^\ast, \\ & \href{../valid/conventions.html#context}{\mathsf{return}} & \href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}^? ~\} \\ \end{array} \end{array}\end{split}\]

In addition to field access written \(C.\mathsf{field}\) the following notation is adopted for manipulating contexts:

When spelling out a context, empty fields are omitted.
\(C,\mathsf{field}\,A^\ast\) denotes the same context as \(C\) but with the elements \(A^\ast\) prepended to its \(\mathsf{field}\) component sequence.

Note

We use indexing notation like \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}[i]\) to look up indices in their respective index space in the context. Context extension notation \(C,\mathsf{field}\,A\) is primarily used to locally extend relative index spaces, such as label indices. Accordingly, the notation is defined to append at the front of the respective sequence, introducing a new relative index \(0\) and shifting the existing ones.

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 \(A\) is said to be “valid with type \(T\)” if and only if all constraints expressed by the respective rules are met. The form of \(T\) depends on what \(A\) is.

Note

For example, if \(A\) is a function, then \(T\) is a function type; for an \(A\) that is a global, \(T\) is a global type; and so on.
The rules implicitly assume a given context \(C\).
In some places, this context is locally extended to a context \(C'\) with additional entries. The formulation “Under context \(C'\), … statement …” is adopted to express that the following statement must apply under the assumptions embodied in the extended context.

Formal Notation¶

Note

This section gives a brief explanation of the notation for specifying typing rules formally. For the interested reader, a more thorough introduction can be found in respective text books. 2

The proposition that a phrase \(A\) has a respective type \(T\) is written \(A : T\). In general, however, typing is dependent on a context \(C\). To express this explicitly, the complete form is a judgement \(C \vdash A : T\), which says that \(A : T\) holds under the assumptions encoded in \(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:

\[\frac{ \mathit{premise}_1 \qquad \mathit{premise}_2 \qquad \dots \qquad \mathit{premise}_n }{ \mathit{conclusion} }\]

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 \(C \vdash A : T\), and there is one respective rule for each relevant construct \(A\) of the abstract syntax.

Note

For example, the typing rule for the \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}}\) instruction can be given as an axiom:

\[\frac{ }{ C \vdash \href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] }\]

The instruction is always valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\)] (saying that it consumes two \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\) values and produces one), independent of any side conditions.

An instruction like \(\href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{local.get}}\) can be typed as follows:

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{locals}}[x] = t }{ C \vdash \href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{local.get}}~x : [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t] }\]

Here, the premise enforces that the immediate local index \(x\) exists in the context. The instruction produces a value of its respective type \(t\) (and does not consume any values). If \(C.\href{../valid/conventions.html#context}{\mathsf{locals}}[x]\) does not exist then the premise does not hold, and the instruction is ill-typed.

Finally, a structured instruction requires a recursive rule, where the premise is itself a typing judgement:

\[\frac{ C \vdash \href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}} : [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] \qquad C,\href{../exec/runtime.html#syntax-label}{\mathsf{label}}\,[t_2^\ast] \vdash \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] }{ C \vdash \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}~\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} : [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] }\]

A \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}\) instruction is only valid when the instruction sequence in its body is. Moreover, the result type must match the block’s annotation \(\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}}\). If so, then the \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}\) instruction has the same type as the body. Inside the body an additional label of the corresponding result type is available, which is expressed by extending the context \(C\) with the additional label information for the premise.

1: The semantics is derived from the following article: Andreas Haas, Andreas Rossberg, Derek Schuff, Ben Titzer, Dan Gohman, Luke Wagner, Alon Zakai, JF Bastien, Michael Holman. Bringing the Web up to Speed with WebAssembly. Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017). ACM 2017.
2: For example: Benjamin Pierce. Types and Programming Languages. The MIT Press 2002