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.
  • 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 behaviour, 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 as well as module instructions. [1]

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 \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}_i\) in \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}\) must be valid with some function type \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_i\).
  • Each table instance \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}_i\) in \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}\) must be valid with some table type \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}_i\).
  • Each memory instance \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}_i\) in \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}\) must be valid with some memory type \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}_i\).
  • Each global instance \(\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}_i\) in \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}\) must be valid with some optional global type \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_i^?\).
  • Then the store is valid.
\[\begin{split}~\\[-1ex] \frac{ \begin{array}{@{}c@{}} (S \href{../appendix/properties.html#valid-funcinst}{\vdash} \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}} : \href{../syntax/types.html#syntax-functype}{\mathit{functype}})^\ast \qquad (S \href{../appendix/properties.html#valid-tableinst}{\vdash} \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}} : \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}})^\ast \\ (S \href{../appendix/properties.html#valid-meminst}{\vdash} \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}} : \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}})^\ast \qquad (S \href{../appendix/properties.html#valid-globalinst}{\vdash} \href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}} : \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}^?)^\ast \\ S = \{ \href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}~\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}^\ast, \href{../exec/runtime.html#syntax-store}{\mathsf{tables}}~\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}^\ast, \href{../exec/runtime.html#syntax-store}{\mathsf{mems}}~\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}^\ast, \href{../exec/runtime.html#syntax-store}{\mathsf{globals}}~\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}^\ast \} \end{array} }{ \href{../appendix/properties.html#valid-store}{\vdash} S \mathrel{\mbox{ok}} }\end{split}\]

Function Instance \(\{\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{code}}~\href{../syntax/modules.html#syntax-func}{\mathit{func}}\}\)

  • The function type \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\) must be valid.
  • The module instance \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\) must be valid with some context \(C\).
  • Under context \(C\), the function \(\href{../syntax/modules.html#syntax-func}{\mathit{func}}\) must be valid with function type \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\).
  • Then the function instance is valid with function type \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\).
\[\frac{ \href{../valid/types.html#valid-functype}{\vdash} \href{../syntax/types.html#syntax-functype}{\mathit{functype}} \mathrel{\mbox{ok}} \qquad S \href{../appendix/properties.html#valid-moduleinst}{\vdash} \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}} : C \qquad C \href{../valid/modules.html#valid-func}{\vdash} \href{../syntax/modules.html#syntax-func}{\mathit{func}} : \href{../syntax/types.html#syntax-functype}{\mathit{functype}} }{ S \href{../appendix/properties.html#valid-funcinst}{\vdash} \{\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{code}}~\href{../syntax/modules.html#syntax-func}{\mathit{func}}\} : \href{../syntax/types.html#syntax-functype}{\mathit{functype}} }\]

Table Instance \(\{ \href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~(\mathit{fa}^?)^n, \href{../exec/runtime.html#syntax-tableinst}{\mathsf{max}}~m^? \}\)

  • For each optional function address \(\mathit{fa}^?_i\) in the table elements \((\mathit{fa}^?)^n\):
    • Either \(\mathit{fa}^?_i\) is empty.
    • Or the external value \(\href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~\mathit{fa}\) must be valid with some external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\mathit{ft}\).
  • The limits \(\{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\}\) must be valid.
  • Then the table instance is valid with table type \(\{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\}~\href{../syntax/types.html#syntax-elemtype}{\mathsf{anyfunc}}\).
\[\frac{ ((S \vdash \href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~\mathit{fa} : \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}})^?)^n \qquad \href{../valid/types.html#valid-limits}{\vdash} \{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\} \mathrel{\mbox{ok}} }{ S \href{../appendix/properties.html#valid-tableinst}{\vdash} \{ \href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~(\mathit{fa}^?)^n, \href{../exec/runtime.html#syntax-tableinst}{\mathsf{max}}~m^? \} : \{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\}~\href{../syntax/types.html#syntax-elemtype}{\mathsf{anyfunc}} }\]

Memory Instance \(\{ \href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}~b^n, \href{../exec/runtime.html#syntax-meminst}{\mathsf{max}}~m^? \}\)

  • The limits \(\{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\}\) must be valid.
  • Then the memory instance is valid with memory type \(\{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\}\).
\[\frac{ \href{../valid/types.html#valid-limits}{\vdash} \{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\} \mathrel{\mbox{ok}} }{ S \href{../appendix/properties.html#valid-meminst}{\vdash} \{ \href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}~b^n, \href{../exec/runtime.html#syntax-meminst}{\mathsf{max}}~m^? \} : \{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\} }\]

Global Instance \(\{ \href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}~(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c), \href{../exec/runtime.html#syntax-globalinst}{\mathsf{mut}}~\href{../syntax/types.html#syntax-mut}{\mathit{mut}} \}\)

  • The global instance is valid with global type \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t\).
\[\frac{ }{ S \href{../appendix/properties.html#valid-globalinst}{\vdash} \{ \href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}~(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c), \href{../exec/runtime.html#syntax-globalinst}{\mathsf{mut}}~\href{../syntax/types.html#syntax-mut}{\mathit{mut}} \} : \href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t }\]

Export Instance \(\{ \href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../exec/runtime.html#syntax-exportinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-externval}{\mathit{externval}} \}\)

  • The external value \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}\) must be valid with some external type \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}\).
  • Then the export instance is valid.
\[\frac{ S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathit{externval}} : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}} }{ S \href{../appendix/properties.html#valid-exportinst}{\vdash} \{ \href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../exec/runtime.html#syntax-exportinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-externval}{\mathit{externval}} \} \mathrel{\mbox{ok}} }\]

Module Instance \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\)

  • Each function type \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_i\) in \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}\) must be valid.
  • For each function address \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}_i\) in \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}\), the external value \(\href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}_i\) must be valid with some external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}'_i\).
  • For each table address \(\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}_i\) in \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}\), the external value \(\href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}_i\) must be valid with some external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}_i\).
  • For each memory address \(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}_i\) in \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}\), the external value \(\href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}_i\) must be valid with some external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}_i\).
  • For each global address \(\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}_i\) in \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globaladdrs}}\), the external value \(\href{../exec/runtime.html#syntax-externval}{\mathsf{global}}~\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}_i\) must be valid with some external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_i\).
  • Each export instance \(\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}_i\) in \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{exports}}\) must be valid.
  • For each export instance \(\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}_i\) in \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{exports}}\), the name \(\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}_i.\href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}\) must be different from any other name occurring in \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{exports}}\).
  • Let \({\href{../syntax/types.html#syntax-functype}{\mathit{functype}}'}^\ast\) be the concatenation of all \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}'_i\) in order.
  • Let \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}^\ast\) be the concatenation of all \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}_i\) in order.
  • Let \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}^\ast\) be the concatenation of all \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}_i\) in order.
  • Let \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}^\ast\) be the concatenation of all \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_i\) in order.
  • Then the module instance is valid with context \(\{\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\}\).
\[\begin{split}~\\[-1ex] \frac{ \begin{array}{@{}c@{}} (\href{../valid/types.html#valid-functype}{\vdash} \href{../syntax/types.html#syntax-functype}{\mathit{functype}} \mathrel{\mbox{ok}})^\ast \\ (S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} : \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}')^\ast \qquad (S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}} : \href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}})^\ast \\ (S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}} : \href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}})^\ast \qquad (S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{global}}~\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}} : \href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}})^\ast \\ (S \href{../appendix/properties.html#valid-exportinst}{\vdash} \href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}} \mathrel{\mbox{ok}})^\ast \qquad (\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}.\href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}})^\ast ~\mbox{disjoint} \end{array} }{ S \href{../appendix/properties.html#valid-moduleinst}{\vdash} \{ \begin{array}[t]{@{}l@{~}l@{}} \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}} & \href{../syntax/types.html#syntax-functype}{\mathit{functype}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}} & \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}} & \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}} & \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globaladdrs}} & \href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}^\ast \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{exports}} & \href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}^\ast ~\} : \{ \begin{array}[t]{@{}l@{~}l@{}} \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 ~\} \end{array} \end{array} }\end{split}\]

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.

Threads may either be regular threads executing sequences of instructions, or module threads executing module instructions that represent an ongoing module instantiation. Regular threads are classified by their result type. Module threads on the other hand have no result, not even an empty one. Consequently, threads and configurations are cumutavily classified by an optional result type, where \(\epsilon\) classifies the thread as a module computation.

In addition to the store \(S\), threads are typed under a return type \(\href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}^?\), which controls whether and with which type a \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{return}}\) instruction is allowed. This type is \(\epsilon\), except for instruction sequences inside an administrative \(\href{../exec/runtime.html#syntax-frame}{\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\)

\[\frac{ \href{../appendix/properties.html#valid-store}{\vdash} S \mathrel{\mbox{ok}} \qquad S; \epsilon \href{../appendix/properties.html#valid-thread}{\vdash} T : [t^?]^? }{ \href{../appendix/properties.html#valid-config}{\vdash} S; T : [t^?]^? }\]

Threads \(F;\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\)

  • Let \(\href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}^?\) be the current allowed return type.
  • The frame \(F\) must be valid with a context \(C\).
  • Let \(C'\) be the same context as \(C\), but with \(\href{../valid/conventions.html#context}{\mathsf{return}}\) set to \(\href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}^?\).
  • Under context \(C'\), the instruction sequence \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\) must be valid with some type \([] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t^?]\).
  • Then the thread is valid with the result type \([t^?]\).
\[\frac{ S \href{../appendix/properties.html#valid-frame}{\vdash} F : C \qquad S; C,\href{../valid/conventions.html#context}{\mathsf{return}}~\href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}^? \href{../valid/instructions.html#valid-instr-seq}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t^?] }{ S; \href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}^? \href{../appendix/properties.html#valid-thread}{\vdash} F; \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : [t^?] }\]

Threads \(\href{../exec/runtime.html#syntax-moduleinstr}{\mathit{moduleinstr}}^\ast\)

  • The current allowed return type must be empty.
  • Each module instruction \(\href{../exec/runtime.html#syntax-moduleinstr}{\mathit{moduleinstr}}_i\) in \(\href{../exec/runtime.html#syntax-moduleinstr}{\mathit{moduleinstr}}^\ast\) must be valid.
  • Then the thread is valid with no result type.
\[\frac{ (S \href{../appendix/properties.html#valid-moduleinstr}{\vdash} \href{../exec/runtime.html#syntax-moduleinstr}{\mathit{moduleinstr}} \mathrel{\mbox{ok}})^\ast }{ S; \epsilon \href{../appendix/properties.html#valid-thread}{\vdash} \href{../exec/runtime.html#syntax-moduleinstr}{\mathit{moduleinstr}}^\ast : \epsilon }\]

Frames \(\{\href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast, \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\}\)

  • The module instance \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\) must be valid with some module context \(C\).
  • Each value \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_i\) in \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\) must be valid with some value type \(t_i\).
  • Let \(t^\ast\) the concatenation of all \(t_i\) in order.
  • Let \(C'\) be the same context as \(C\), but with the value types \(t^\ast\) prepended to the \(\href{../valid/conventions.html#context}{\mathsf{locals}}\) vector.
  • Then the frame is valid with frame context \(C'\).
\[\frac{ S \href{../appendix/properties.html#valid-moduleinst}{\vdash} \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}} : C \qquad (\href{../appendix/properties.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-val}{\mathit{val}} : t)^\ast }{ S \href{../appendix/properties.html#valid-frame}{\vdash} \{\href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast, \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\} : (C, \href{../valid/conventions.html#context}{\mathsf{locals}}~t^\ast) }\]

Values \(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c\)

\[\frac{ }{ \href{../appendix/properties.html#valid-val}{\vdash} t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c : t }\]

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 \vdash \mathit{prop}\) are generalized to include the store, as in \(S; C \vdash \mathit{prop}\), by implicitly adding \(S\) to all rules – \(S\) is never modified by the pre-existing rules, but it is accessed in the new rules for administrative instructions and module instructions given below.

\(\href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}\)

  • The instruction is valid with type \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\), for any sequences of value types \(t_1^\ast\) and \(t_2^\ast\).
\[\frac{ }{ S; C \href{../appendix/properties.html#valid-instr-admin}{\vdash} \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} : [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] }\]

\(\href{../exec/runtime.html#syntax-invoke}{\mathsf{invoke}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}\)

  • The external function value \(\href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}\) must be valid with external function type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}} ([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast])\).
  • Then the instruction is valid with type \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\).
\[\frac{ S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} : \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~[t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] }{ S; C \href{../appendix/properties.html#valid-instr-admin}{\vdash} \href{../exec/runtime.html#syntax-invoke}{\mathsf{invoke}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} : [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] }\]

\(\href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_0^\ast\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\)

  • The instruction sequence \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_0^\ast\) must be valid with some type \([t_1^n] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^?]\).
  • Let \(C'\) be the same context as \(C\), but with the result type \([t_1^n]\) prepended to the \(\href{../valid/conventions.html#context}{\mathsf{labels}}\) vector.
  • Under context \(C'\), the instruction sequence \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\) must be valid with type \([] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^?]\).
  • Then the compound instruction is valid with type \([] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^?]\).
\[\frac{ S; C \href{../valid/instructions.html#valid-instr-seq}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_0^\ast : [t_1^n] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^?] \qquad S; C,\href{../valid/conventions.html#context}{\mathsf{labels}}\,[t_1^n] \href{../valid/instructions.html#valid-instr-seq}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^?] }{ S; C \href{../appendix/properties.html#valid-instr-admin}{\vdash} \href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_0^\ast\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} : [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^?] }\]

\(\href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}_n\{F\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\)

  • Under the return type \([t^n]\), the thread \(F; \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\) must be valid with result type \([t^n]\).
  • Then the compound instruction is valid with type \([] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t^n]\).
\[\frac{ S; [t^n] \href{../valid/instructions.html#valid-instr-seq}{\vdash} F; \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : [t^n] }{ S; C \href{../appendix/properties.html#valid-instr-admin}{\vdash} \href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}_n\{F\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} : [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t^n] }\]

Module Instructions

Typing rules for module instructions are specified as follows. Unlike regular instructions, module instructions do not use the operand stack, and consequently, are not classified by a type.

\(\href{../exec/runtime.html#syntax-instantiate}{\mathsf{instantiate}}~\href{../syntax/modules.html#syntax-module}{\mathit{module}}~\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast\)

  • Each external value \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_i\) in \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast\) must be valid with some external type \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_i\).
  • Then the module instruction is valid.
\[\frac{ (S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathit{externval}} : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}})^\ast }{ S \href{../appendix/properties.html#valid-moduleinstr}{\vdash} \href{../exec/runtime.html#syntax-instantiate}{\mathsf{instantiate}}~\href{../syntax/modules.html#syntax-module}{\mathit{module}}~\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast \mathrel{\mbox{ok}} }\]

\(\href{../exec/runtime.html#syntax-init-elem}{\mathsf{init\_elem}}~\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}~o~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}~x^n\)

  • The external table value \(\href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}\) must be valid with some external table type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~\href{../syntax/types.html#syntax-elemtype}{\mathsf{anyfunc}}\).
  • The index \(o + n\) must be smaller than or equal to \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}.\href{../syntax/types.html#syntax-limits}{\mathsf{min}}\).
  • The module instance \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\) must be valid with some context \(C\).
  • Each function index \(x_i\) in \(x^n\) must be defined in the context \(C\).
  • Then the module instruction is valid.
\[\begin{split}\frac{ \begin{array}{@{}rl@{}} S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}} : \href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~\href{../syntax/types.html#syntax-elemtype}{\mathsf{anyfunc}} \qquad& o + n \leq \href{../syntax/types.html#syntax-limits}{\mathit{limits}}.\href{../syntax/types.html#syntax-limits}{\mathsf{min}} \\ S \href{../appendix/properties.html#valid-moduleinst}{\vdash} \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}} : C \qquad& (C.\href{../valid/conventions.html#context}{\mathsf{funcs}}[x] = \href{../syntax/types.html#syntax-functype}{\mathit{functype}})^n \end{array} }{ S \href{../appendix/properties.html#valid-moduleinstr}{\vdash} \href{../exec/runtime.html#syntax-init-elem}{\mathsf{init\_elem}}~\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}~o~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}~x^n \mathrel{\mbox{ok}} }\end{split}\]

\(\href{../exec/runtime.html#syntax-init-data}{\mathsf{init\_data}}~\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}~o~b^n\)

  • The external memory value \(\href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}\) must be valid with some external memory type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\).
  • The index \(o + n\) must be smaller than or equal to \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}.\href{../syntax/types.html#syntax-limits}{\mathsf{min}}\) divided by the page size \(64\,\mathrm{Ki}\).
  • Then the module instruction is valid.
\[\frac{ S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}} : \href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}} \qquad o + n \leq \href{../syntax/types.html#syntax-limits}{\mathit{limits}}.\href{../syntax/types.html#syntax-limits}{\mathsf{min}} \cdot 64\,\mathrm{Ki} }{ S \href{../appendix/properties.html#valid-moduleinstr}{\vdash} \href{../exec/runtime.html#syntax-init-data}{\mathsf{init\_data}}~\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}~o~b^n \mathrel{\mbox{ok}} }\]

\(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}\)

  • Under an empty context, the instruction \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}\) must be valid with type \([] \href{../syntax/types.html#syntax-functype}{\rightarrow} []\).
  • Then the instruction is valid as a module instruction.
\[\frac{ S; \{\} \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}} : [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [] }{ S \href{../appendix/properties.html#valid-moduleinstr}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}} \mathrel{\mbox{ok}} }\]

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'\) extends state \(S\), written \(S \href{../appendix/properties.html#extend}{\preceq} S'\), when the following rules hold.

Note

Extension does not imply that the new store is valid, which is defined :ref:separately above <valid-store>.

Store \(S\)

  • The length of \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}\) must not shrink.
  • The length of \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}\) must not shrink.
  • The length of \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}\) must not shrink.
  • The length of \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}\) must not shrink.
  • For each function instance \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}_i\) in the original \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}\), the new function instance must be an extension of the old.
  • For each table instance \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}_i\) in the original \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}\), the new table instance must be an extension of the old.
  • For each memory instance \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}_i\) in the original \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}\), the new memory instance must be an extension of the old.
  • For each global instance \(\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}_i\) in the original \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}\), the new global instance must be an extension of the old.
\[\begin{split}\frac{ \begin{array}{@{}ccc@{}} S_1.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}} = \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}_1^\ast & S_2.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}} = {\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}'_1}^\ast~\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}_2^\ast & (\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}'_1)^\ast \\ S_1.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}} = \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}_1^\ast & S_2.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}} = {\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}'_1}^\ast~\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}_2^\ast & (\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}'_1)^\ast \\ S_1.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}} = \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}_1^\ast & S_2.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}} = {\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}'_1}^\ast~\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}_2^\ast & (\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}'_1)^\ast \\ S_1.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}} = \href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}_1^\ast & S_2.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}} = {\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}'_1}^\ast~\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}_2^\ast & (\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}'_1)^\ast \\ \end{array} }{ \href{../appendix/properties.html#extend-store}{\vdash} S_1 \href{../appendix/properties.html#extend}{\preceq} S_2 }\end{split}\]

Function Instance \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}\)

  • A function instance must remain unchanged.
\[\frac{ }{ \href{../appendix/properties.html#extend-funcinst}{\vdash} \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}} \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}} }\]

Table Instance \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}\)

  • The length of \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}\) must not shrink.
  • The value of \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{max}}\) must remain unchanged.
\[\frac{ n_1 \leq n_2 }{ \href{../appendix/properties.html#extend-tableinst}{\vdash} \{\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~(\mathit{fa}_1^?)^{n_1}, \href{../exec/runtime.html#syntax-tableinst}{\mathsf{max}}~m\} \href{../appendix/properties.html#extend}{\preceq} \{\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~(\mathit{fa}_2^?)^{n_2}, \href{../exec/runtime.html#syntax-tableinst}{\mathsf{max}}~m\} }\]

Memory Instance \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}\)

  • The length of \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\) must not shrink.
  • The value of \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{max}}\) must remain unchanged.
\[\frac{ n_1 \leq n_2 }{ \href{../appendix/properties.html#extend-meminst}{\vdash} \{\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}~b_1^{n_1}, \href{../exec/runtime.html#syntax-meminst}{\mathsf{max}}~m\} \href{../appendix/properties.html#extend}{\preceq} \{\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}~b_2^{n_2}, \href{../exec/runtime.html#syntax-meminst}{\mathsf{max}}~m\} }\]

Global Instance \(\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}\)

  • The mutability \(\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}.\href{../exec/runtime.html#syntax-globalinst}{\mathsf{mut}}\) must remain unchanged.
  • The value type of the value \(\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}.\href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}\) must remain unchanged.
  • If \(\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}.\href{../exec/runtime.html#syntax-globalinst}{\mathsf{mut}}\) is \(\href{../syntax/types.html#syntax-mut}{\mathsf{const}}\), then the value \(\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}.\href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}\) must remain unchanged.
\[\frac{ \href{../syntax/types.html#syntax-mut}{\mathit{mut}} = \href{../syntax/types.html#syntax-mut}{\mathsf{var}} \vee c_1 = c_2 }{ \href{../appendix/properties.html#extend-globalinst}{\vdash} \{\href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}~(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_1), \href{../exec/runtime.html#syntax-globalinst}{\mathsf{mut}}~\href{../syntax/types.html#syntax-mut}{\mathit{mut}}\} \href{../appendix/properties.html#extend}{\preceq} \{\href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}~(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_2), \href{../exec/runtime.html#syntax-globalinst}{\mathsf{mut}}~\href{../syntax/types.html#syntax-mut}{\mathit{mut}}\} }\]

Theorems

Given the definition of valid configurations, the standard soundness theorems hold.

Theorem (Preservation). If the configuration \(S;T\) is valid with optional result type \([t^\ast]^?\) (i.e., \(\href{../appendix/properties.html#valid-config}{\vdash} S;T : [t^\ast]^?\)), and steps to \(S';T'\) (i.e., \(S;T \href{../exec/conventions.html#formal-notation}{\hookrightarrow} S';T'\)), then \(S';T'\) is a valid configuration with the same optional resulttype (i.e., \(\href{../appendix/properties.html#valid-config}{\vdash} S';T' : [t^\ast]^?\)). Furthermore, \(S'\) is an extension of \(S\) (i.e., \(\href{../appendix/properties.html#extend-store}{\vdash} S \href{../appendix/properties.html#extend}{\preceq} S'\)).

A terminal thread is either an empty sequence of module instructions, a \(\href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}\) instruction, or a sequence \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\) of values (paired with a frame). A terminal configuration is a configuration whose thread is terminal.

Theorem (Progress). If the configuration \(S;T\) is valid (i.e., \(\href{../appendix/properties.html#valid-config}{\vdash} S;T : [t^\ast]^?\) with some optional result type \([t^\ast]^?\)), then either it is terminal, or it can step to some configuration \(S';T'\) (i.e., \(S;T \href{../exec/conventions.html#formal-notation}{\hookrightarrow} S';T'\)).

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

Corollary (Soundness). 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.