Type Soundness

The type system of WebAssembly is sound, implying both type safety and memory safety with respect to the WebAssembly semantics. For example:

• All types declared and derived during validation are respected at run time; e.g., every local or global variable will only contain type-correct values, every instruction will only be applied to operands of the expected type, and every function invocation always evaluates to a result of the right type (if it does not trap or diverge).

• No memory location will be read or written except those explicitly defined by the program, i.e., as a local, a global, an element in a table, or a location within a linear memory.

• There is no undefined behavior, i.e., the execution rules cover all possible cases that can occur in a valid program, and the rules are mutually consistent.

Soundness also is instrumental in ensuring additional properties, most notably, encapsulation of function and module scopes: no locals can be accessed outside their own function and no module components can be accessed outside their own module unless they are explicitly exported or imported.

The typing rules defining WebAssembly validation only cover the static components of a WebAssembly program. In order to state and prove soundness precisely, the typing rules must be extended to the dynamic components of the abstract runtime, that is, the store, configurations, and administrative instructions. [1]

Contexts

In order to check rolled up recursive types, the context is locally extended with an additional component that records the sub type corresponding to each recursive type index within the current recursive type:

$$\begin{array}{r}\begin{array}{llll}& C& ::=& \{\dots ,\mathsf{recs}{\mathit{subtype}}^{\ast }\}\end{array}\end{array}$$

Types

Well-formedness for extended type forms is defined as follows.

Heap Type $\mathsf{bot}$

• The heap type is valid.

$$\frac{}{C⊢\mathsf{bot}\text{ok}}$$

Heap Type $\mathsf{rec}i$

• The recursive type index $i$ must exist in $C.\mathsf{recs}$.

• Then the heap type is valid.

$$\frac{C.\mathsf{recs}[i]=\mathit{subtype}}{C⊢\mathsf{rec}i\text{ok}}$$

Value Type $\mathsf{bot}$

• The value type is valid.

$$\frac{}{C⊢\mathsf{bot}\text{ok}}$$

Recursive Types $\mathsf{rec}{\mathit{subtype}}^{\ast }$

• Let $C^{\prime }$ be the current context $C$, but where $\mathsf{recs}$ is ${\mathit{subtype}}^{\ast }$.

• There must be a type index $x$, such that for each sub type ${\mathit{subtype}}_i$ in ${\mathit{subtype}}^{\ast }$:

  • Under the context $C^{\prime }$, the sub type ${\mathit{subtype}}_i$ must be valid for type index $x+i$ and recursive type index $i$.

• Then the recursive type is valid for the type index $x$.

$$\frac{C,\mathsf{recs}{\mathit{subtype}}^{\ast }⊢\mathsf{rec}{\mathit{subtype}}^{\ast }\text{ok}(x,0)}{C⊢\mathsf{rec}{\mathit{subtype}}^{\ast }\text{ok}(x)}$$

$$\frac{}{C⊢\mathsf{rec}ϵ\text{ok}(x,i)}\frac{C⊢\mathit{subtype}\text{ok}(x,i)C⊢\mathsf{rec}{{\mathit{subtype}}^{\prime }}^{\ast }\text{ok}(x+1,i+1)}{C⊢\mathsf{rec}\mathit{subtype}{{\mathit{subtype}}^{\prime }}^{\ast }\text{ok}(x,i)}$$

Note

These rules are a generalisation of the ones previously given.

Sub types $\mathsf{sub}{\mathsf{final}}^{?}{\mathit{ht}}^{\ast }\mathit{comptype}$

• The composite type $\mathit{comptype}$ must be valid.

• The sequence ${\mathit{ht}}^{\ast }$ may be no longer than $1$.

• For every heap type ${\mathit{ht}}_k$ in ${\mathit{ht}}^{\ast }$:

  • The heap type ${\mathit{ht}}_k$ must be ordered before a type index $x$ and recursive type index a $i$, meaning:

    • Either ${\mathit{ht}}_k$ is a defined type.

    • Or ${\mathit{ht}}_k$ is a type index $y_k$ that is smaller than $x$.

    • Or ${\mathit{ht}}_k$ is a recursive type index $\mathsf{rec}{j}_k$ where $j_k$ is smaller than $i$.

  • Let sub type ${\mathit{subtype}}_k$ be the unrolling of the heap type ${\mathit{ht}}_k$, meaning:

    • Either ${\mathit{ht}}_k$ is a defined type ${\mathit{deftype}}_k$, then ${\mathit{subtype}}_k$ must be the unrolling of ${\mathit{deftype}}_k$.

    • Or ${\mathit{ht}}_k$ is a type index $y_k$, then ${\mathit{subtype}}_k$ must be the unrolling of the defined type $C.\mathsf{types}[y_k]$.

    • Or ${\mathit{ht}}_k$ is a recursive type index $\mathsf{rec}{j}_k$, then ${\mathit{subtype}}_k$ must be $C.\mathsf{recs}[j_k]$.

  • The sub type ${\mathit{subtype}}_k$ must not contain $\mathsf{final}$.

  • Let ${\mathit{comptype}}_k^{\prime }$ be the composite type in ${\mathit{subtype}}_k$.

  • The composite type $\mathit{comptype}$ must match ${\mathit{comptype}}_k^{\prime }$.

• Then the sub type is valid for the type index $x$ and recursive type index $i$.

$$\begin{array}{r}\frac{\begin{array}{c}|{\mathit{ht}}^{\ast }|\le 1(\mathit{ht}\prec x,i{)}^{\ast }({\mathrm{unroll}}_C(\mathit{ht})=\mathsf{sub}{{\mathit{ht}}^{\prime }}^{\ast }{\mathit{comptype}}^{\prime }{)}^{\ast }\\ C⊢\mathit{comptype}\text{ok}(C⊢\mathit{comptype}\le {\mathit{comptype}}^{\prime }{)}^{\ast }\end{array}}{C⊢\mathsf{sub}{\mathsf{final}}^{?}{\mathit{ht}}^{\ast }\mathit{comptype}\text{ok}(x,i)}\end{array}$$

where:

$$\begin{array}{r}\begin{array}{lll}(\mathit{deftype}\prec x,i)& =& \mathrm{true}\\ (y\prec x,i)& =& y<x\\ (\mathsf{rec}j\prec x,i)& =& j<i\\ [2ex]{\mathrm{unroll}}_C(\mathit{deftype})& =& \mathrm{unroll}(\mathit{deftype})\\ {\mathrm{unroll}}_C(y)& =& \mathrm{unroll}(C.\mathsf{types}[y])\\ {\mathrm{unroll}}_C(\mathsf{rec}j)& =& C.\mathsf{recs}[j]\end{array}\end{array}$$

Note

This rule is a generalisation of the ones previously given, which only allowed type indices as supertypes.

Subtyping

In a rolled-up recursive type, a recursive type indices $\mathsf{rec}i$ matches another heap type $\mathit{ht}$ if:

• Let $\mathsf{sub}{\mathsf{final}}^{?}{{\mathit{ht}}^{\prime }}^{\ast }\mathit{comptype}$ be the sub type $C.\mathsf{recs}[i]$.

• The heap type $\mathit{ht}$ is contained in ${{\mathit{ht}}^{\prime }}^{\ast }$.

$$\frac{C.\mathsf{recs}[i]=\mathsf{sub}{\mathsf{final}}^{?}({\mathit{ht}}_1^{\ast }\mathit{ht}{\mathit{ht}}_2^{\ast })\mathit{comptype}}{C⊢\mathsf{rec}i\le \mathit{ht}}$$

Note

This rule is only invoked when checking validity of rolled-up recursive types.

Results

Results can be classified by result types as follows.

Results ${\mathit{val}}^{\ast }$

• For each value ${\mathit{val}}_i$ in ${\mathit{val}}^{\ast }$:

  • The value ${\mathit{val}}_i$ is valid with some value type $t_i$.

• Let $t^{\ast }$ be the concatenation of all $t_i$.

• Then the result is valid with result type $[t^{\ast }]$.

$$\frac{(S⊢\mathit{val}:t{)}^{\ast }}{S⊢{\mathit{val}}^{\ast }:[t^{\ast }]}$$

Results $\mathsf{trap}$

• The result is valid with result type $[t^{\ast }]$, for any valid closed result types.

$$\frac{⊢[t^{\ast }]\text{ok}}{S⊢\mathsf{trap}:[t^{\ast }]}$$

Store Validity

The following typing rules specify when a runtime store $S$ is valid. A valid store must consist of function, table, memory, global, and module instances that are themselves valid, relative to $S$.

To that end, each kind of instance is classified by a respective function, table, memory, or global type. Module instances are classified by module contexts, which are regular contexts repurposed as module types describing the index spaces defined by a module.

Store $S$

• Each function instance ${\mathit{funcinst}}_i$ in $S.\mathsf{funcs}$ must be valid with some function type ${\mathit{functype}}_i$.

• Each table instance ${\mathit{tableinst}}_i$ in $S.\mathsf{tables}$ must be valid with some table type ${\mathit{tabletype}}_i$.

• Each memory instance ${\mathit{meminst}}_i$ in $S.\mathsf{mems}$ must be valid with some memory type ${\mathit{memtype}}_i$.

• Each global instance ${\mathit{globalinst}}_i$ in $S.\mathsf{globals}$ must be valid with some global type ${\mathit{globaltype}}_i$.

• Each element instance ${\mathit{eleminst}}_i$ in $S.\mathsf{elems}$ must be valid with some reference type ${\mathit{reftype}}_i$.

• Each data instance ${\mathit{datainst}}_i$ in $S.\mathsf{datas}$ must be valid.

• Each structure instance ${\mathit{structinst}}_i$ in $S.\mathsf{structs}$ must be valid.

• Each array instance ${\mathit{arrayinst}}_i$ in $S.\mathsf{arrays}$ must be valid.

• No reference to a bound structure address must be reachable from itself through a path consisting only of indirections through immutable structure or array fields.

• No reference to a bound array address must be reachable from itself through a path consisting only of indirections through immutable structure or array fields.

• Then the store is valid.

$$\begin{array}{r}\\ \frac{\begin{array}{c}(S⊢\mathit{funcinst}:\mathit{deftype}{)}^{\ast }(S⊢\mathit{tableinst}:\mathit{tabletype}{)}^{\ast }\\ (S⊢\mathit{meminst}:\mathit{memtype}{)}^{\ast }(S⊢\mathit{globalinst}:\mathit{globaltype}{)}^{\ast }\\ (S⊢\mathit{eleminst}:\mathit{reftype}{)}^{\ast }(S⊢\mathit{datainst}\text{ok}{)}^{\ast }\\ (S⊢\mathit{structinst}\text{ok}{)}^{\ast }(S⊢\mathit{arrayinst}\text{ok}{)}^{\ast }\\ S=\{\begin{array}{l}\mathsf{funcs}{\mathit{funcinst}}^{\ast },\mathsf{globals}{\mathit{globalinst}}^{\ast },\mathsf{tables}{\mathit{tableinst}}^{\ast },\mathsf{mems}{\mathit{meminst}}^{\ast },\\ \mathsf{elems}{\mathit{eleminst}}^{\ast },\mathsf{datas}{\mathit{datainst}}^{\ast },\mathsf{structs}{\mathit{structinst}}^{\ast },\mathsf{arrays}{\mathit{arrayinst}}^{\ast }\}\end{array}\\ (S.\mathsf{structs}[a_{\mathrm{s}}]=\mathit{structinst}{)}^{\ast }((\mathsf{ref}\mathsf{.}\mathsf{struct}{a}_{\mathrm{s}}){\gg ̸}_S^{+}(\mathsf{ref}\mathsf{.}\mathsf{struct}{a}_{\mathrm{s}}){)}^{\ast }\\ (S.\mathsf{arrays}[a_{\mathrm{a}}]=\mathit{arrayinst}{)}^{\ast }((\mathsf{ref}\mathsf{.}\mathsf{array}{a}_{\mathrm{a}}){\gg ̸}_S^{+}(\mathsf{ref}\mathsf{.}\mathsf{array}{a}_{\mathrm{a}}){)}^{\ast }\end{array}}{⊢S\text{ok}}\end{array}$$

where ${\mathit{val}}_1{\gg }_S^{+}{\mathit{val}}_2$ denotes the transitive closure of the following reachability relation on values:

$$\begin{array}{r}\begin{array}{lcll}(\mathsf{ref}\mathsf{.}\mathsf{struct}a)& {\gg }_S& S.\mathsf{structs}[a].\mathsf{fields}[i]& \text{if}\mathrm{expand}(S.\mathsf{structs}[a].\mathsf{type})=\mathsf{struct}{\mathit{ft}}_1^i(\mathsf{const}\mathit{st}){\mathit{ft}}_2^{\ast }\\ (\mathsf{ref}\mathsf{.}\mathsf{array}a)& {\gg }_S& S.\mathsf{arrays}[a].\mathsf{fields}[i]& \text{if}\mathrm{expand}(S.\mathsf{arrays}[a].\mathsf{type})=\mathsf{array}(\mathsf{const}\mathit{st})\\ (\mathsf{ref}\mathsf{.}\mathsf{extern}\mathit{ref})& {\gg }_S& \mathit{ref}\end{array}\end{array}$$

Note

The constraint on reachability through immutable fields prevents the presence of cyclic data structures that can not be constructed in the language. Cycles can only be formed using mutation.

Function Instances $\{\mathsf{type}\mathit{functype},\mathsf{module}\mathit{moduleinst},\mathsf{code}\mathit{func}\}$

• The function type $\mathit{functype}$ must be valid under an empty context.

• The module instance $\mathit{moduleinst}$ must be valid with some context $C$.

• Under context $C$:

  • The function $\mathit{func}$ must be valid with some function type ${\mathit{functype}}^{\prime }$.

  • The function type ${\mathit{functype}}^{\prime }$ must match $\mathit{functype}$.

• Then the function instance is valid with function type $\mathit{functype}$.

$$\begin{array}{r}\frac{\begin{array}{c}⊢\mathit{functype}\text{ok}S⊢\mathit{moduleinst}:C\\ C⊢\mathit{func}:{\mathit{functype}}^{\prime }C⊢{\mathit{functype}}^{\prime }\le \mathit{functype}\end{array}}{S⊢\{\mathsf{type}\mathit{functype},\mathsf{module}\mathit{moduleinst},\mathsf{code}\mathit{func}\}:\mathit{functype}}\end{array}$$

Host Function Instances $\{\mathsf{type}\mathit{functype},\mathsf{hostcode}\mathit{hf}\}$

• The function type $\mathit{functype}$ must be valid under an empty context.

• Let $[t_1^{\ast }]\to [t_2^{\ast }]$ be the function type $\mathit{functype}$.

• For every valid store $S_1$ extending $S$ and every sequence ${\mathit{val}}^{\ast }$ of values whose types coincide with $t_1^{\ast }$:

  • Executing $\mathit{hf}$ in store $S_1$ with arguments ${\mathit{val}}^{\ast }$ has a non-empty set of possible outcomes.

  • For every element $R$ of this set:

    • Either $R$ must be $\mathrm{\perp }$ (i.e., divergence).

    • Or $R$ consists of a valid store $S_2$ extending $S_1$ and a result $\mathit{result}$ whose type coincides with $[t_2^{\ast }]$.

• Then the function instance is valid with function type $\mathit{functype}$.

$$\begin{array}{r}\frac{\begin{array}{l}⊢[t_1^{\ast }]\to [t_2^{\ast }]\text{ok}\end{array}\begin{array}{l}\mathrm{\forall }{S}_1,{\mathit{val}}^{\ast },⊢S_1\text{ok}\wedge ⊢S⪯S_1\wedge S_1⊢{\mathit{val}}^{\ast }:[t_1^{\ast }]⟹\\ \mathit{hf}(S_1;{\mathit{val}}^{\ast })\supset \mathrm{\varnothing }\wedge \\ \mathrm{\forall }R\in \mathit{hf}(S_1;{\mathit{val}}^{\ast }),R=\mathrm{\perp }\vee \\ \mathrm{\exists }{S}_2,\mathit{result},⊢S_2\text{ok}\wedge ⊢S_1⪯S_2\wedge S_2⊢\mathit{result}:[t_2^{\ast }]\wedge R=(S_2;\mathit{result})\end{array}}{S⊢\{\mathsf{type}[t_1^{\ast }]\to [t_2^{\ast }],\mathsf{hostcode}\mathit{hf}\}:[t_1^{\ast }]\to [t_2^{\ast }]}\end{array}$$

Note

This rule states that, if appropriate pre-conditions about store and arguments are satisfied, then executing the host function must satisfy appropriate post-conditions about store and results. The post-conditions match the ones in the execution rule for invoking host functions.

Any store under which the function is invoked is assumed to be an extension of the current store. That way, the function itself is able to make sufficient assumptions about future stores.

Table Instances $\{\mathsf{type}(\mathit{limits}t),\mathsf{elem}{\mathit{ref}}^{\ast }\}$

• The table type $\mathit{limits}t$ must be valid under the empty context.

• The length of ${\mathit{ref}}^{\ast }$ must equal $\mathit{limits}.\mathsf{min}$.

• For each reference ${\mathit{ref}}_i$ in the table’s elements ${\mathit{ref}}^n$:

  • The reference ${\mathit{ref}}_i$ must be valid with some reference type $t_i^{\prime }$.

  • The reference type $t_i^{\prime }$ must match the reference type $t$.

• Then the table instance is valid with table type $\mathit{limits}t$.

$$\frac{⊢\mathit{limits}t\text{ok}n=\mathit{limits}.\mathsf{min}(S⊢\mathit{ref}:t^{\prime }{)}^n(⊢t^{\prime }\le t{)}^n}{S⊢\{\mathsf{type}(\mathit{limits}t),\mathsf{elem}{\mathit{ref}}^n\}:\mathit{limits}t}$$

Memory Instances $\{\mathsf{type}\mathit{limits},\mathsf{data}{b}^{\ast }\}$

• The memory type $\mathit{limits}$ must be valid under the empty context.

• The length of $b^{\ast }$ must equal $\mathit{limits}.\mathsf{min}$ multiplied by the page size $64\mathrm{Ki}$.

• Then the memory instance is valid with memory type $\mathit{limits}$.

$$\frac{⊢\mathit{limits}\text{ok}n=\mathit{limits}.\mathsf{min}\cdot 64\mathrm{Ki}}{S⊢\{\mathsf{type}\mathit{limits},\mathsf{data}{b}^n\}:\mathit{limits}}$$

Global Instances $\{\mathsf{type}(\mathit{mut}t),\mathsf{value}\mathit{val}\}$

• The global type $\mathit{mut}t$ must be valid under the empty context.

• The value $\mathit{val}$ must be valid with some value type $t^{\prime }$.

• The value type $t^{\prime }$ must match the value type $t$.

• Then the global instance is valid with global type $\mathit{mut}t$.

$$\frac{⊢\mathit{mut}t\text{ok}S⊢\mathit{val}:t^{\prime }⊢t^{\prime }\le t}{S⊢\{\mathsf{type}(\mathit{mut}t),\mathsf{value}\mathit{val}\}:\mathit{mut}t}$$

Element Instances $\{\mathsf{type}t,\mathsf{elem}{\mathit{ref}}^{\ast }\}$

• The reference type $t$ must be valid under the empty context.

• For each reference ${\mathit{ref}}_i$ in the elements ${\mathit{ref}}^n$:

  • The reference ${\mathit{ref}}_i$ must be valid with some reference type $t_i^{\prime }$.

  • The reference type $t_i^{\prime }$ must match the reference type $t$.

• Then the element instance is valid with reference type $t$.

$$\frac{⊢t\text{ok}(S⊢\mathit{ref}:t^{\prime }{)}^{\ast }(⊢t^{\prime }\le t{)}^{\ast }}{S⊢\{\mathsf{type}t,\mathsf{elem}{\mathit{ref}}^{\ast }\}:t}$$

Data Instances $\{\mathsf{data}{b}^{\ast }\}$

• The data instance is valid.

$$\frac{}{S⊢\{\mathsf{data}{b}^{\ast }\}\text{ok}}$$

Structure Instances $\{\mathsf{type}\mathit{deftype},\mathsf{fields}{\mathit{fieldval}}^{\ast }\}$

• The defined type $\mathit{deftype}$ must be valid.

• The expansion of $\mathit{deftype}$ must be a structure type $\mathsf{struct}{\mathit{fieldtype}}^{\ast }$.

• The length of the sequence of field values ${\mathit{fieldval}}^{\ast }$ must be the same as the length of the sequence of field types ${\mathit{fieldtype}}^{\ast }$.

• For each field value ${\mathit{fieldval}}_i$ in ${\mathit{fieldval}}^{\ast }$ and corresponding field type ${\mathit{fieldtype}}_i$ in ${\mathit{fieldtype}}^{\ast }$:

  • Let ${\mathit{fieldtype}}_i$ be $\mathit{mut}{\mathit{storagetype}}_i$.

  • The field value ${\mathit{fieldval}}_i$ must be valid with storage type ${\mathit{storagetype}}_i$.

• Then the structure instance is valid.

$$\frac{⊢\mathit{dt}\text{ok}\mathrm{expand}(\mathit{dt})=\mathsf{struct}(\mathit{mut}\mathit{st}{)}^{\ast }(S⊢\mathit{fv}:\mathit{st}{)}^{\ast }}{S⊢\{\mathsf{type}\mathit{dt},\mathsf{fields}{\mathit{fv}}^{\ast }\}\text{ok}}$$

Array Instances $\{\mathsf{type}\mathit{deftype},\mathsf{fields}{\mathit{fieldval}}^{\ast }\}$

• The defined type $\mathit{deftype}$ must be valid.

• The expansion of $\mathit{deftype}$ must be an array type $\mathsf{array}\mathit{fieldtype}$.

• Let $\mathit{fieldtype}$ be $\mathit{mut}\mathit{storagetype}$.

• For each field value ${\mathit{fieldval}}_i$ in ${\mathit{fieldval}}^{\ast }$:

  • The field value ${\mathit{fieldval}}_i$ must be valid with storage type $\mathit{storagetype}$.

• Then the array instance is valid.

$$\frac{⊢\mathit{dt}\text{ok}\mathrm{expand}(\mathit{dt})=\mathsf{array}(\mathit{mut}\mathit{st})(S⊢\mathit{fv}:\mathit{st}{)}^{\ast }}{S⊢\{\mathsf{type}\mathit{dt},\mathsf{fields}{\mathit{fv}}^{\ast }\}\text{ok}}$$

Field Values $\mathit{fieldval}$

• If $\mathit{fieldval}$ is a value $\mathit{val}$, then:

  • The value $\mathit{val}$ must be valid with value type $t$.

  • Then the field value is valid with value type $t$.

• Else, $\mathit{fieldval}$ is a packed value $\mathit{packedval}$:

  • Let $\mathit{packedtype}.\mathsf{pack}i$ be the field value $\mathit{fieldval}$.

  • Then the field value is valid with packed type $\mathit{packedtype}$.

$$\frac{}{S⊢\mathit{pt}.\mathsf{pack}i:\mathit{pt}}$$

Export Instances $\{\mathsf{name}\mathit{name},\mathsf{value}\mathit{externval}\}$

• The external value $\mathit{externval}$ must be valid with some external type $\mathit{externtype}$.

• Then the export instance is valid.

$$\frac{S⊢\mathit{externval}:\mathit{externtype}}{S⊢\{\mathsf{name}\mathit{name},\mathsf{value}\mathit{externval}\}\text{ok}}$$

Module Instances $\mathit{moduleinst}$

• Each defined type ${\mathit{deftype}}_i$ in $\mathit{moduleinst}.\mathsf{types}$ must be valid under the empty context.

• For each function address ${\mathit{funcaddr}}_i$ in $\mathit{moduleinst}.\mathsf{funcaddrs}$, the external value $\mathsf{func}{\mathit{funcaddr}}_i$ must be valid with some external type $\mathsf{func}{\mathit{functype}}_i$.

• For each table address ${\mathit{tableaddr}}_i$ in $\mathit{moduleinst}.\mathsf{tableaddrs}$, the external value $\mathsf{table}{\mathit{tableaddr}}_i$ must be valid with some external type $\mathsf{table}{\mathit{tabletype}}_i$.

• For each memory address ${\mathit{memaddr}}_i$ in $\mathit{moduleinst}.\mathsf{memaddrs}$, the external value $\mathsf{mem}{\mathit{memaddr}}_i$ must be valid with some external type $\mathsf{mem}{\mathit{memtype}}_i$.

• For each global address ${\mathit{globaladdr}}_i$ in $\mathit{moduleinst}.\mathsf{globaladdrs}$, the external value $\mathsf{global}{\mathit{globaladdr}}_i$ must be valid with some external type $\mathsf{global}{\mathit{globaltype}}_i$.

• For each element address ${\mathit{elemaddr}}_i$ in $\mathit{moduleinst}.\mathsf{elemaddrs}$, the element instance $S.\mathsf{elems}[{\mathit{elemaddr}}_i]$ must be valid with some reference type ${\mathit{reftype}}_i$.

• For each data address ${\mathit{dataaddr}}_i$ in $\mathit{moduleinst}.\mathsf{dataaddrs}$, the data instance $S.\mathsf{datas}[{\mathit{dataaddr}}_i]$ must be valid.

• Each export instance ${\mathit{exportinst}}_i$ in $\mathit{moduleinst}.\mathsf{exports}$ must be valid.

• For each export instance ${\mathit{exportinst}}_i$ in $\mathit{moduleinst}.\mathsf{exports}$, the name ${\mathit{exportinst}}_i.\mathsf{name}$ must be different from any other name occurring in $\mathit{moduleinst}.\mathsf{exports}$.

• Let ${\mathit{deftype}}^{\ast }$ be the concatenation of all ${\mathit{deftype}}_i$ in order.

• Let ${\mathit{functype}}^{\ast }$ be the concatenation of all ${\mathit{functype}}_i$ in order.

• Let ${\mathit{tabletype}}^{\ast }$ be the concatenation of all ${\mathit{tabletype}}_i$ in order.

• Let ${\mathit{memtype}}^{\ast }$ be the concatenation of all ${\mathit{memtype}}_i$ in order.

• Let ${\mathit{globaltype}}^{\ast }$ be the concatenation of all ${\mathit{globaltype}}_i$ in order.

• Let ${\mathit{reftype}}^{\ast }$ be the concatenation of all ${\mathit{reftype}}_i$ in order.

• Let $m$ be the length of $\mathit{moduleinst}.\mathsf{funcaddrs}$.

• Let $n$ be the length of $\mathit{moduleinst}.\mathsf{dataaddrs}$.

• Let $x^{\ast }$ be the sequence of function indices from $0$ to $m-1$.

• Then the module instance is valid with context $\{\mathsf{types}{\mathit{deftype}}^{\ast },$ $\mathsf{funcs}{\mathit{functype}}^{\ast },$ $\mathsf{tables}{\mathit{tabletype}}^{\ast },$ $\mathsf{mems}{\mathit{memtype}}^{\ast },$ $\mathsf{globals}{\mathit{globaltype}}^{\ast },$ $\mathsf{elems}{\mathit{reftype}}^{\ast },$ $\mathsf{datas}{\text{ok}}^n,$ $\mathsf{refs}{x}^{\ast }\}$.

$$\begin{array}{r}\\ \frac{\begin{array}{c}(⊢\mathit{deftype}\text{ok}{)}^{\ast }\\ (S⊢\mathsf{func}\mathit{funcaddr}:\mathsf{func}\mathit{functype}{)}^{\ast }(S⊢\mathsf{table}\mathit{tableaddr}:\mathsf{table}\mathit{tabletype}{)}^{\ast }\\ (S⊢\mathsf{mem}\mathit{memaddr}:\mathsf{mem}\mathit{memtype}{)}^{\ast }(S⊢\mathsf{global}\mathit{globaladdr}:\mathsf{global}\mathit{globaltype}{)}^{\ast }\\ (S⊢S.\mathsf{elems}[\mathit{elemaddr}]:\mathit{reftype}{)}^{\ast }(S⊢S.\mathsf{datas}[\mathit{dataaddr}]\text{ok}{)}^n\\ (S⊢\mathit{exportinst}\text{ok}{)}^{\ast }(\mathit{exportinst}.\mathsf{name}{)}^{\ast }\text{disjoint}\end{array}}{S⊢\{\begin{array}{ll}\mathsf{types}& {\mathit{deftype}}^{\ast },\\ \mathsf{funcaddrs}& {\mathit{funcaddr}}^{\ast },\\ \mathsf{tableaddrs}& {\mathit{tableaddr}}^{\ast },\\ \mathsf{memaddrs}& {\mathit{memaddr}}^{\ast },\\ \mathsf{globaladdrs}& {\mathit{globaladdr}}^{\ast },\\ \mathsf{elemaddrs}& {\mathit{elemaddr}}^{\ast },\\ \mathsf{dataaddrs}& {\mathit{dataaddr}}^n,\\ \mathsf{exports}& {\mathit{exportinst}}^{\ast }\}:\{\begin{array}{ll}\mathsf{types}& {\mathit{deftype}}^{\ast },\\ \mathsf{funcs}& {\mathit{functype}}^{\ast },\\ \mathsf{tables}& {\mathit{tabletype}}^{\ast },\\ \mathsf{mems}& {\mathit{memtype}}^{\ast },\\ \mathsf{globals}& {\mathit{globaltype}}^{\ast },\\ \mathsf{elems}& {\mathit{reftype}}^{\ast },\\ \mathsf{datas}& {\text{ok}}^n,\\ \mathsf{refs}& 0\dots (|{\mathit{funcaddr}}^{\ast }|-1)\}\end{array}\end{array}}\end{array}$$

Configuration Validity

To relate the WebAssembly type system to its execution semantics, the typing rules for instructions must be extended to configurations $S;T$, which relates the store to execution threads.

Configurations and threads are classified by their result type. In addition to the store $S$, threads are typed under a return type ${\mathit{resulttype}}^{?}$, which controls whether and with which type a $\mathsf{return}$ instruction is allowed. This type is absent ($ϵ$) except for instruction sequences inside an administrative $\mathsf{frame}$ instruction.

Finally, frames are classified with frame contexts, which extend the module contexts of a frame’s associated module instance with the locals that the frame contains.

Configurations $S;T$

• The store $S$ must be valid.

• Under no allowed return type, the thread $T$ must be valid with some result type $[t^{\ast }]$.

• Then the configuration is valid with the result type $[t^{\ast }]$.

$$\frac{⊢S\text{ok}S;ϵ⊢T:[t^{\ast }]}{⊢S;T:[t^{\ast }]}$$

Threads $F;{\mathit{instr}}^{\ast }$

• Let ${\mathit{resulttype}}^{?}$ be the current allowed return type.

• The frame $F$ must be valid with a context $C$.

• Let $C^{\prime }$ be the same context as $C$, but with $\mathsf{return}$ set to ${\mathit{resulttype}}^{?}$.

• Under context $C^{\prime }$, the instruction sequence ${\mathit{instr}}^{\ast }$ must be valid with some type $[]\to [t^{\ast }]$.

• Then the thread is valid with the result type $[t^{\ast }]$.

$$\frac{S⊢F:CS;C,\mathsf{return}{\mathit{resulttype}}^{?}⊢{\mathit{instr}}^{\ast }:[]\to [t^{\ast }]}{S;{\mathit{resulttype}}^{?}⊢F;{\mathit{instr}}^{\ast }:[t^{\ast }]}$$

Frames $\{\mathsf{locals}{\mathit{val}}^{\ast },\mathsf{module}\mathit{moduleinst}\}$

• The module instance $\mathit{moduleinst}$ must be valid with some module context $C$.

• Each value ${\mathit{val}}_i$ in ${\mathit{val}}^{\ast }$ must be valid with some value type $t_i$.

• Let $t^{\ast }$ be the concatenation of all $t_i$ in order.

• Let $C^{\prime }$ be the same context as $C$, but with the value types $t^{\ast }$ prepended to the $\mathsf{locals}$ vector.

• Then the frame is valid with frame context $C^{\prime }$.

$$\frac{S⊢\mathit{moduleinst}:C(S⊢\mathit{val}:t{)}^{\ast }}{S⊢\{\mathsf{locals}{\mathit{val}}^{\ast },\mathsf{module}\mathit{moduleinst}\}:(C,\mathsf{locals}{t}^{\ast })}$$

Administrative Instructions

Typing rules for administrative instructions are specified as follows. In addition to the context $C$, typing of these instructions is defined under a given store $S$.

To that end, all previous typing judgements $C⊢\mathit{prop}$ are generalized to include the store, as in $S;C⊢\mathit{prop}$, by implicitly adding $S$ to all rules – $S$ is never modified by the pre-existing rules, but it is accessed in the extra rules for administrative instructions given below.

$\mathsf{trap}$

• The instruction is valid with any valid instruction type of the form $[t_1^{\ast }]\to [t_2^{\ast }]$.

$$\frac{C⊢[t_1^{\ast }]\to [t_2^{\ast }]\text{ok}}{S;C⊢\mathsf{trap}:[t_1^{\ast }]\to [t_2^{\ast }]}$$

$\mathit{val}$

• The value $\mathit{val}$ must be valid with value type $t$.

• Then it is valid as an instruction with type $[]\to [t]$.

$$\frac{S⊢\mathit{val}:t}{S;C⊢\mathit{val}:[]\to [t]}$$

$\mathsf{invoke}\mathit{funcaddr}$

• The external function value $\mathsf{func}\mathit{funcaddr}$ must be valid with external function type $\mathsf{func}{\mathit{functype}}^{\prime }$.

• Let $[t_1^{\ast }]\to [t_2^{\ast }])$ be the function type $\mathit{functype}$.

• Then the instruction is valid with type $[t_1^{\ast }]\to [t_2^{\ast }]$.

$$\frac{S⊢\mathsf{func}\mathit{funcaddr}:\mathsf{func}[t_1^{\ast }]\to [t_2^{\ast }]}{S;C⊢\mathsf{invoke}\mathit{funcaddr}:[t_1^{\ast }]\to [t_2^{\ast }]}$$

${\mathsf{label}}_n\{{\mathit{instr}}_0^{\ast }\}{\mathit{instr}}^{\ast }\mathsf{end}$

• The instruction sequence ${\mathit{instr}}_0^{\ast }$ must be valid with some type $[t_1^n]{\to }_{x^{\ast }}[t_2^{\ast }]$.

• Let $C^{\prime }$ be the same context as $C$, but with the result type $[t_1^n]$ prepended to the $\mathsf{labels}$ vector.

• Under context $C^{\prime }$, the instruction sequence ${\mathit{instr}}^{\ast }$ must be valid with type $[]{\to }_{{x^{\prime }}^{\ast }}[t_2^{\ast }]$.

• Then the compound instruction is valid with type $[]\to [t_2^{\ast }]$.

$$\frac{S;C⊢{\mathit{instr}}_0^{\ast }:[t_1^n]{\to }_{x^{\ast }}[t_2^{\ast }]S;C,\mathsf{labels}[t_1^n]⊢{\mathit{instr}}^{\ast }:[]{\to }_{{x^{\prime }}^{\ast }}[t_2^{\ast }]}{S;C⊢{\mathsf{label}}_n\{{\mathit{instr}}_0^{\ast }\}{\mathit{instr}}^{\ast }\mathsf{end}:[]\to [t_2^{\ast }]}$$

${\mathsf{frame}}_n\{F\}{\mathit{instr}}^{\ast }\mathsf{end}$

• Under the valid return type $[t^n]$, the thread $F;{\mathit{instr}}^{\ast }$ must be valid with result type $[t^n]$.

• Then the compound instruction is valid with type $[]\to [t^n]$.

$$\frac{C⊢[t^n]\text{ok}S;[t^n]⊢F;{\mathit{instr}}^{\ast }:[t^n]}{S;C⊢{\mathsf{frame}}_n\{F\}{\mathit{instr}}^{\ast }\mathsf{end}:[]\to [t^n]}$$

Store Extension

Programs can mutate the store and its contained instances. Any such modification must respect certain invariants, such as not removing allocated instances or changing immutable definitions. While these invariants are inherent to the execution semantics of WebAssembly instructions and modules, host functions do not automatically adhere to them. Consequently, the required invariants must be stated as explicit constraints on the invocation of host functions. Soundness only holds when the embedder ensures these constraints.

The necessary constraints are codified by the notion of store extension: a store state $S^{\prime }$ extends state $S$, written $S⪯S^{\prime }$, when the following rules hold.

Note

Extension does not imply that the new store is valid, which is defined separately above.

Store $S$

• The length of $S.\mathsf{funcs}$ must not shrink.

• The length of $S.\mathsf{tables}$ must not shrink.

• The length of $S.\mathsf{mems}$ must not shrink.

• The length of $S.\mathsf{globals}$ must not shrink.

• The length of $S.\mathsf{elems}$ must not shrink.

• The length of $S.\mathsf{datas}$ must not shrink.

• The length of $S.\mathsf{structs}$ must not shrink.

• The length of $S.\mathsf{arrays}$ must not shrink.

• For each function instance ${\mathit{funcinst}}_i$ in the original $S.\mathsf{funcs}$, the new function instance must be an extension of the old.

• For each table instance ${\mathit{tableinst}}_i$ in the original $S.\mathsf{tables}$, the new table instance must be an extension of the old.

• For each memory instance ${\mathit{meminst}}_i$ in the original $S.\mathsf{mems}$, the new memory instance must be an extension of the old.

• For each global instance ${\mathit{globalinst}}_i$ in the original $S.\mathsf{globals}$, the new global instance must be an extension of the old.

• For each element instance ${\mathit{eleminst}}_i$ in the original $S.\mathsf{elems}$, the new element instance must be an extension of the old.

• For each data instance ${\mathit{datainst}}_i$ in the original $S.\mathsf{datas}$, the new data instance must be an extension of the old.

• For each structure instance ${\mathit{structinst}}_i$ in the original $S.\mathsf{structs}$, the new structure instance must be an extension of the old.

• For each array instance ${\mathit{arrayinst}}_i$ in the original $S.\mathsf{arrays}$, the new array instance must be an extension of the old.

$$\begin{array}{r}\frac{\begin{array}{ccc}{S}_1.\mathsf{funcs}={\mathit{funcinst}}_1^{\ast }& S_2.\mathsf{funcs}={{\mathit{funcinst}}_1^{\prime }}^{\ast }{\mathit{funcinst}}_2^{\ast }& (⊢{\mathit{funcinst}}_1⪯{\mathit{funcinst}}_1^{\prime }{)}^{\ast }\\ S_1.\mathsf{tables}={\mathit{tableinst}}_1^{\ast }& S_2.\mathsf{tables}={{\mathit{tableinst}}_1^{\prime }}^{\ast }{\mathit{tableinst}}_2^{\ast }& (⊢{\mathit{tableinst}}_1⪯{\mathit{tableinst}}_1^{\prime }{)}^{\ast }\\ S_1.\mathsf{mems}={\mathit{meminst}}_1^{\ast }& S_2.\mathsf{mems}={{\mathit{meminst}}_1^{\prime }}^{\ast }{\mathit{meminst}}_2^{\ast }& (⊢{\mathit{meminst}}_1⪯{\mathit{meminst}}_1^{\prime }{)}^{\ast }\\ S_1.\mathsf{globals}={\mathit{globalinst}}_1^{\ast }& S_2.\mathsf{globals}={{\mathit{globalinst}}_1^{\prime }}^{\ast }{\mathit{globalinst}}_2^{\ast }& (⊢{\mathit{globalinst}}_1⪯{\mathit{globalinst}}_1^{\prime }{)}^{\ast }\\ S_1.\mathsf{elems}={\mathit{eleminst}}_1^{\ast }& S_2.\mathsf{elems}={{\mathit{eleminst}}_1^{\prime }}^{\ast }{\mathit{eleminst}}_2^{\ast }& (⊢{\mathit{eleminst}}_1⪯{\mathit{eleminst}}_1^{\prime }{)}^{\ast }\\ S_1.\mathsf{datas}={\mathit{datainst}}_1^{\ast }& S_2.\mathsf{datas}={{\mathit{datainst}}_1^{\prime }}^{\ast }{\mathit{datainst}}_2^{\ast }& (⊢{\mathit{datainst}}_1⪯{\mathit{datainst}}_1^{\prime }{)}^{\ast }\\ S_1.\mathsf{structs}={\mathit{structinst}}_1^{\ast }& S_2.\mathsf{structs}={{\mathit{structinst}}_1^{\prime }}^{\ast }{\mathit{structinst}}_2^{\ast }& (⊢{\mathit{structinst}}_1⪯{\mathit{structinst}}_1^{\prime }{)}^{\ast }\\ S_1.\mathsf{arrays}={\mathit{arrayinst}}_1^{\ast }& S_2.\mathsf{arrays}={{\mathit{arrayinst}}_1^{\prime }}^{\ast }{\mathit{arrayinst}}_2^{\ast }& (⊢{\mathit{arrayinst}}_1⪯{\mathit{arrayinst}}_1^{\prime }{)}^{\ast }\end{array}}{⊢S_1⪯S_2}\end{array}$$

Function Instance $\mathit{funcinst}$

• A function instance must remain unchanged.

$$\frac{}{⊢\mathit{funcinst}⪯\mathit{funcinst}}$$

Table Instance $\mathit{tableinst}$

• The table type $\mathit{tableinst}.\mathsf{type}$ must remain unchanged.

• The length of $\mathit{tableinst}.\mathsf{elem}$ must not shrink.

$$\frac{n_1\le n_2}{⊢\{\mathsf{type}\mathit{tt},\mathsf{elem}({\mathit{fa}}_1^{?}{)}^{n_1}\}⪯\{\mathsf{type}\mathit{tt},\mathsf{elem}({\mathit{fa}}_2^{?}{)}^{n_2}\}}$$

Memory Instance $\mathit{meminst}$

• The memory type $\mathit{meminst}.\mathsf{type}$ must remain unchanged.

• The length of $\mathit{meminst}.\mathsf{data}$ must not shrink.

$$\frac{n_1\le n_2}{⊢\{\mathsf{type}\mathit{mt},\mathsf{data}{b}_1^{n_1}\}⪯\{\mathsf{type}\mathit{mt},\mathsf{data}{b}_2^{n_2}\}}$$

Global Instance $\mathit{globalinst}$

• The global type $\mathit{globalinst}.\mathsf{type}$ must remain unchanged.

• Let $\mathit{mut}t$ be the structure of $\mathit{globalinst}.\mathsf{type}$.

• If $\mathit{mut}$ is $\mathsf{const}$, then the value $\mathit{globalinst}.\mathsf{value}$ must remain unchanged.

$$\frac{\mathit{mut}=\mathsf{var}\vee {\mathit{val}}_1={\mathit{val}}_2}{⊢\{\mathsf{type}(\mathit{mut}t),\mathsf{value}{\mathit{val}}_1\}⪯\{\mathsf{type}(\mathit{mut}t),\mathsf{value}{\mathit{val}}_2\}}$$

Element Instance $\mathit{eleminst}$

• The reference type $\mathit{eleminst}.\mathsf{type}$ must remain unchanged.

• The vector $\mathit{eleminst}.\mathsf{elem}$ must:

  • either remain unchanged,

  • or shrink to length $0$.

$$\frac{}{⊢\{\mathsf{type}t,\mathsf{elem}{a}^{\ast }\}⪯\{\mathsf{type}t,\mathsf{elem}{a}^{\ast }\}}$$

$$\frac{}{⊢\{\mathsf{type}t,\mathsf{elem}{a}^{\ast }\}⪯\{\mathsf{type}t,\mathsf{elem}ϵ\}}$$

Data Instance $\mathit{datainst}$

• The vector $\mathit{datainst}.\mathsf{data}$ must:

  • either remain unchanged,

  • or shrink to length $0$.

$$\frac{}{⊢\{\mathsf{data}{b}^{\ast }\}⪯\{\mathsf{data}{b}^{\ast }\}}$$

$$\frac{}{⊢\{\mathsf{data}{b}^{\ast }\}⪯\{\mathsf{data}ϵ\}}$$

Structure Instance $\mathit{structinst}$

• The defined type $\mathit{structinst}.\mathsf{type}$ must remain unchanged.

• Assert: due to store well-formedness, the expansion of $\mathit{structinst}.\mathsf{type}$ is a structure type.

• Let $\mathsf{struct}{\mathit{fieldtype}}^{\ast }$ be the expansion of $\mathit{structinst}.\mathsf{type}$.

• The length of the vector $\mathit{structinst}.\mathsf{fields}$ must remain unchanged.

• Assert: due to store well-formedness, the length of $\mathit{structinst}.\mathsf{fields}$ is the same as the length of ${\mathit{fieldtype}}^{\ast }$.

• For each field value ${\mathit{fieldval}}_i$ in $\mathit{structinst}.\mathsf{fields}$ and corresponding field type ${\mathit{fieldtype}}_i$ in ${\mathit{fieldtype}}^{\ast }$:

  • Let ${\mathit{mut}}_i{\mathit{st}}_i$ be the structure of ${\mathit{fieldtype}}_i$.

  • If ${\mathit{mut}}_i$ is $\mathsf{const}$, then the field value ${\mathit{fieldval}}_i$ must remain unchanged.

$$\frac{(\mathit{mut}=\mathsf{var}\vee {\mathit{fieldval}}_1={\mathit{fieldval}}_2{)}^{\ast }}{⊢\{\mathsf{type}(\mathit{mut}\mathit{st}{)}^{\ast },\mathsf{fields}{\mathit{fieldval}}_1^{\ast }\}⪯\{\mathsf{type}(\mathit{mut}\mathit{st}{)}^{\ast },\mathsf{fields}{\mathit{fieldval}}_2^{\ast }\}}$$

Array Instance $\mathit{arrayinst}$

• The defined type $\mathit{arrayinst}.\mathsf{type}$ must remain unchanged.

• Assert: due to store well-formedness, the expansion of $\mathit{arrayinst}.\mathsf{type}$ is an array type.

• Let $\mathsf{array}\mathit{fieldtype}$ be the expansion of $\mathit{arrayinst}.\mathsf{type}$.

• The length of the vector $\mathit{arrayinst}.\mathsf{fields}$ must remain unchanged.

• Let $\mathit{mut}\mathit{st}$ be the structure of $\mathit{fieldtype}$.

• If $\mathit{mut}$ is $\mathsf{const}$, then the sequence of field values $\mathit{arrayinst}.\mathsf{fields}$ must remain unchanged.

$$\frac{\mathit{mut}=\mathsf{var}\vee {\mathit{fieldval}}_1^{\ast }={\mathit{fieldval}}_2^{\ast }}{⊢\{\mathsf{type}(\mathit{mut}\mathit{st}),\mathsf{fields}{\mathit{fieldval}}_1^{\ast }\}⪯\{\mathsf{type}(\mathit{mut}\mathit{st}),\mathsf{fields}{\mathit{fieldval}}_2^{\ast }\}}$$

Theorems

Given the definition of valid configurations, the standard soundness theorems hold. [2] [3]

Theorem (Preservation). If a configuration $S;T$ is valid with result type $[t^{\ast }]$ (i.e., $⊢S;T:[t^{\ast }]$), and steps to $S^{\prime };T^{\prime }$ (i.e., $S;T\hookrightarrow S^{\prime };T^{\prime }$), then $S^{\prime };T^{\prime }$ is a valid configuration with the same result type (i.e., $⊢S^{\prime };T^{\prime }:[t^{\ast }]$). Furthermore, $S^{\prime }$ is an extension of $S$ (i.e., $⊢S⪯S^{\prime }$).

A terminal thread is one whose sequence of instructions is a result. A terminal configuration is a configuration whose thread is terminal.

Theorem (Progress). If a configuration $S;T$ is valid (i.e., $⊢S;T:[t^{\ast }]$ for some result type $[t^{\ast }]$), then either it is terminal, or it can step to some configuration $S^{\prime };T^{\prime }$ (i.e., $S;T\hookrightarrow S^{\prime };T^{\prime }$).

From Preservation and Progress the soundness of the WebAssembly type system follows directly.

Corollary (Soundness). If a configuration $S;T$ is valid (i.e., $⊢S;T:[t^{\ast }]$ for some result type $[t^{\ast }]$), then it either diverges or takes a finite number of steps to reach a terminal configuration $S^{\prime };T^{\prime }$ (i.e., $S;T{\hookrightarrow }^{\ast }{S}^{\prime };T^{\prime }$) that is valid with the same result type (i.e., $⊢S^{\prime };T^{\prime }:[t^{\ast }]$) and where $S^{\prime }$ is an extension of $S$ (i.e., $⊢S⪯S^{\prime }$).

In other words, every thread in a valid configuration either runs forever, traps, or terminates with a result that has the expected type. Consequently, given a valid store, no computation defined by instantiation or invocation of a valid module can “crash” or otherwise (mis)behave in ways not covered by the execution semantics given in this specification.

[1]

The formalization and theorems are 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]

A machine-verified version of the formalization and soundness proof of the PLDI 2017 paper is described in the following article: Conrad Watt. Mechanising and Verifying the WebAssembly Specification. Proceedings of the 7th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2018). ACM 2018.

[3]

Machine-verified formalizations and soundness proofs of the semantics from the official specification are described in the following article: Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, Philippa Gardner. Two Mechanisations of WebAssembly 1.0. Proceedings of the 24th International Symposium on Formal Methods (FM 2021). Springer 2021.

Type System Properties

Principal Types

The type system of WebAssembly features both subtyping and simple forms of polymorphism for instruction types. That has the effect that every instruction or instruction sequence can be classified with multiple different instruction types.

However, the typing rules still allow deriving principal types for instruction sequences. That is, every valid instruction sequence has one particular type scheme, possibly containing some unconstrained place holder type variables, that is a subtype of all its valid instruction types, after substituting its type variables with suitable specific types.

Moreover, when deriving an instruction type in a “forward” manner, i.e., the input of the instruction sequence is already fixed to specific types, then it has a principal output type expressible without type variables, up to a possibly polymorphic stack bottom representable with one single variable. In other words, “forward” principal types are effectively closed.

Note

For example, in isolation, the instruction $\mathsf{ref}\mathsf{.}\mathsf{as}\mathsf{\_}\mathsf{non}\mathsf{\_}\mathsf{null}$ has the type $[(\mathsf{ref}\mathsf{null}\mathit{ht})]\to [(\mathsf{ref}\mathit{ht})]$ for any choice of valid heap type $\mathit{ht}$. Moreover, if the input type $[(\mathsf{ref}\mathsf{null}\mathit{ht})]$ is already determined, i.e., a specific $\mathit{ht}$ is given, then the output type $[(\mathsf{ref}\mathit{ht})]$ is fully determined as well.

The implication of the latter property is that a validator for complete instruction sequences (as they occur in valid modules) can be implemented with a simple left-to-right algorithm that does not require the introduction of type variables.

A typing algorithm capable of handling partial instruction sequences (as might be considered for program analysis or program manipulation) needs to introduce type variables and perform substitutions, but it does not need to perform backtracking or record any non-syntactic constraints on these type variables.

Technically, the syntax of heap, value, and result types can be enriched with type variables as follows:

$$\begin{array}{r}\begin{array}{llll}& \mathit{null}& ::=& {\mathsf{null}}^{?}|{\alpha }_{\mathit{null}}\\ & \mathit{heaptype}& ::=& \dots |{\alpha }_{\mathit{heaptype}}\\ & \mathit{reftype}& ::=& \mathsf{ref}\mathit{null}\mathit{heaptype}\\ & \mathit{valtype}& ::=& \dots |{\alpha }_{\mathit{valtype}}|{\alpha }_{\mathit{numvectype}}\\ & \mathit{resulttype}& ::=& [{\alpha }_{{\mathit{valtype}}^{\ast }}^{?}{\mathit{valtype}}^{\ast }]\end{array}\end{array}$$

where each ${\alpha }_{\mathit{xyz}}$ ranges over a set of type variables for syntactic class $\mathit{xyz}$, respectively. The special class $\mathit{numvectype}$ is defined as $\mathit{numtype}|\mathit{vectype}|\mathsf{bot}$, and is only needed to handle unannotated $\mathsf{select}$ instructions.

A type is closed when it does not contain any type variables, and open otherwise. A type substitution $\sigma$ is a finite mapping from type variables to closed types of the respective syntactic class. When applied to an open type, it replaces the type variables $\alpha$ from its domain with the respective $\sigma (\alpha )$.

Theorem (Principal Types). If an instruction sequence ${\mathit{instr}}^{\ast }$ is valid with some closed instruction type $\mathit{instrtype}$ (i.e., $C⊢{\mathit{instr}}^{\ast }:\mathit{instrtype}$), then it is also valid with a possibly open instruction type ${\mathit{instrtype}}_{min}$ (i.e., $C⊢{\mathit{instr}}^{\ast }:{\mathit{instrtype}}_{min}$), such that for every closed type ${\mathit{instrtype}}^{\prime }$ with which ${\mathit{instr}}^{\ast }$ is valid (i.e., for all $C⊢{\mathit{instr}}^{\ast }:{\mathit{instrtype}}^{\prime }$), there exists a substitution $\sigma$, such that $\sigma ({\mathit{instrtype}}_{min})$ is a subtype of ${\mathit{instrtype}}^{\prime }$ (i.e., $C⊢\sigma ({\mathit{instrtype}}_{min})\le {\mathit{instrtype}}^{\prime }$). Furthermore, ${\mathit{instrtype}}_{min}$ is unique up to the choice of type variables.

Theorem (Closed Principal Forward Types). If closed input type $[t_1^{\ast }]$ is given and the instruction sequence ${\mathit{instr}}^{\ast }$ is valid with instruction type $[t_1^{\ast }]{\to }_{x^{\ast }}[t_2^{\ast }]$ (i.e., $C⊢{\mathit{instr}}^{\ast }:[t_1^{\ast }]{\to }_{x^{\ast }}[t_2^{\ast }]$), then it is also valid with instruction type $[t_1^{\ast }]{\to }_{x^{\ast }}[{\alpha }_{{\mathit{valtype}}^{\ast }}{t}^{\ast }]$ (i.e., $C⊢{\mathit{instr}}^{\ast }:[t_1^{\ast }]{\to }_{x^{\ast }}[{\alpha }_{{\mathit{valtype}}^{\ast }}{t}^{\ast }]$), where all $t^{\ast }$ are closed, such that for every closed result type $[{t_2^{\prime }}^{\ast }]$ with which ${\mathit{instr}}^{\ast }$ is valid (i.e., for all $C⊢{\mathit{instr}}^{\ast }:[t_1^{\ast }]{\to }_{x^{\ast }}[{t_2^{\prime }}^{\ast }]$), there exists a substitution $\sigma$, such that $[{t_2^{\prime }}^{\ast }]=[\sigma ({\alpha }_{{\mathit{valtype}}^{\ast }})t^{\ast }]$.

Type Lattice

The Principal Types property depends on the existence of a greatest lower bound for any pair of types.

Theorem (Greatest Lower Bounds for Value Types). For any two value types $t_1$ and $t_2$ that are valid (i.e., $C⊢t_1\text{ok}$ and $C⊢t_2\text{ok}$), there exists a valid value type $t$ that is a subtype of both $t_1$ and $t_2$ (i.e., $C⊢t\text{ok}$ and $C⊢t\le t_1$ and $C⊢t\le t_2$), such that every valid value type $t^{\prime }$ that also is a subtype of both $t_1$ and $t_2$ (i.e., for all $C⊢t^{\prime }\text{ok}$ and $C⊢t^{\prime }\le t_1$ and $C⊢t^{\prime }\le t_2$), is a subtype of $t$ (i.e., $C⊢t^{\prime }\le t$).

Note

The greatest lower bound of two types may be $\mathsf{bot}$.

Theorem (Conditional Least Upper Bounds for Value Types). Any two value types $t_1$ and $t_2$ that are valid (i.e., $C⊢t_1\text{ok}$ and $C⊢t_2\text{ok}$) either have no common supertype, or there exists a valid value type $t$ that is a supertype of both $t_1$ and $t_2$ (i.e., $C⊢t\text{ok}$ and $C⊢t_1\le t$ and $C⊢t_2\le t$), such that every valid value type $t^{\prime }$ that also is a supertype of both $t_1$ and $t_2$ (i.e., for all $C⊢t^{\prime }\text{ok}$ and $C⊢t_1\le t^{\prime }$ and $C⊢t_2\le t^{\prime }$), is a supertype of $t$ (i.e., $C⊢t\le t^{\prime }$).

Note

If a top type was added to the type system, a least upper bound would exist for any two types.

Corollary (Type Lattice). Assuming the addition of a provisional top type, value types form a lattice with respect to their subtype relation.

Finally, value types can be partitioned into multiple disjoint hierarchies that are not related by subtyping, except through $\mathsf{bot}$.

Theorem (Disjoint Subtype Hierarchies). The greatest lower bound of two value types is $\mathsf{bot}$ or $\mathsf{ref}\mathsf{bot}$ if and only if they do not have a least upper bound.

In other words, types that do not have common supertypes, do not have common subtypes either (other than $\mathsf{bot}$ or $\mathsf{ref}\mathsf{bot}$), and vice versa.

Note

Types from disjoint hierarchies can safely be represented in mutually incompatible ways in an implementation, because their values can never flow to the same place.

Compositionality

Valid instruction sequences can be freely composed, as long as their types match up.

Theorem (Composition). If two instruction sequences ${\mathit{instr}}_1^{\ast }$ and ${\mathit{instr}}_2^{\ast }$ are valid with types $[t_1^{\ast }]{\to }_{x_1^{\ast }}[t^{\ast }]$ and $[t^{\ast }]{\to }_{x_2^{\ast }}[t_2^{\ast }]$, respectively (i.e., $C⊢{\mathit{instr}}_1^{\ast }:[t_1^{\ast }]{\to }_{x_1^{\ast }}[t^{\ast }]$ and $C⊢{\mathit{instr}}_1^{\ast }:[t^{\ast }]{\to }_{x_2^{\ast }}[t_2^{\ast }]$), then the concatenated instruction sequence $({\mathit{instr}}_1^{\ast }{\mathit{instr}}_2^{\ast })$ is valid with type $[t_1^{\ast }]{\to }_{x_1^{\ast }{x}_2^{\ast }}[t_2^{\ast }]$ (i.e., $C⊢{\mathit{instr}}_1^{\ast }{\mathit{instr}}_2^{\ast }:[t_1^{\ast }]{\to }_{x_1^{\ast }{x}_2^{\ast }}[t_2^{\ast }]$).

Note

More generally, instead of a shared type $[t^{\ast }]$, it suffices if the output type of ${\mathit{instr}}_1^{\ast }$ is a subtype of the input type of ${\mathit{instr}}_1^{\ast }$, since the subtype can always be weakened to its supertype by subsumption.

Inversely, valid instruction sequences can also freely be decomposed, that is, splitting them anywhere produces two instruction sequences that are both valid.

Theorem (Decomposition). If an instruction sequence ${\mathit{instr}}^{\ast }$ that is valid with type $[t_1^{\ast }]{\to }_{x^{\ast }}[t_2^{\ast }]$ (i.e., $C⊢{\mathit{instr}}^{\ast }:[t_1^{\ast }]{\to }_{x^{\ast }}[t_2^{\ast }]$) is split into two instruction sequences ${\mathit{instr}}_1^{\ast }$ and ${\mathit{instr}}_2^{\ast }$ at any point (i.e., ${\mathit{instr}}^{\ast }={\mathit{instr}}_1^{\ast }{\mathit{instr}}_2^{\ast }$), then these are separately valid with some types $[t_1^{\ast }]{\to }_{x_1^{\ast }}[t^{\ast }]$ and $[t^{\ast }]{\to }_{x_2^{\ast }}[t_2^{\ast }]$, respectively (i.e., $C⊢{\mathit{instr}}_1^{\ast }:[t_1^{\ast }]{\to }_{x_1^{\ast }}[t^{\ast }]$ and $C⊢{\mathit{instr}}_1^{\ast }:[t^{\ast }]{\to }_{x_2^{\ast }}[t_2^{\ast }]$), where $x^{\ast }=x_1^{\ast }{x}_2^{\ast }$.

Note

This property holds because validation is required even for unreachable code. Without that, ${\mathit{instr}}_2^{\ast }$ might not be valid in isolation.