properties.rst

! soundness, type system

Soundness

The type system <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 <syntax-local> or global <syntax-global> variable will only contain type-correct values, every instruction <syntax-instr> will only be applied to operands of the expected type, and every function <syntax-func> invocation <exec-invocation> always evaluates to a result of the right type (if it does not trap <trap> or diverge).
• No memory location will be read or written except those explicitly defined by the program, i.e., as a local <syntax-local>, a global <syntax-global>, an element in a table <syntax-table>, or a location within a linear memory <syntax-mem>.
• There is no undefined behavior, i.e., the execution rules <exec> cover all possible cases that can occur in a valid <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 <syntax-local> can be accessed outside their own function and no module <syntax-module> components can be accessed outside their own module unless they are explicitly exported <syntax-export> or imported <syntax-import>.

The typing rules defining WebAssembly validation <valid> 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 <syntax-runtime>, that is, the store <syntax-store>, configurations <syntax-config>, and administrative instructions <syntax-instr-admin>.¹

value, value type, result, result type, trap

Results

Results <syntax-result> can be classified by result types <syntax-resulttype> as follows.

Results <syntax-result> $\val^\ast$

• For each value <syntax-val> $\val_i$ in $\val^\ast$:
  • The value $\val_i$ is valid <valid-val> with some value type <syntax-valtype> t_i.
• Let t^* be the concatenation of all t_i.
• Then the result is valid with result type <syntax-resulttype> [t^*].

$$\frac{ (S \vdashval \val : t)^\ast }{ S \vdashresult \val^\ast : [t^\ast] }$$

Results <syntax-result> $\TRAP$

• The result is valid with result type <syntax-resulttype> [t^*], for any sequence t^* of value types <syntax-valtype>.

$$\frac{ }{ S \vdashresult \TRAP : [t^\ast] }$$

Store Validity

The following typing rules specify when a runtime store <syntax-store> S is valid. A valid store must consist of function <syntax-funcinst>, table <syntax-tableinst>, memory <syntax-meminst>, global <syntax-globalinst>, and module <syntax-moduleinst> instances that are themselves valid, relative to S.

To that end, each kind of instance is classified by a respective function <syntax-functype>, table <syntax-tabletype>, memory <syntax-memtype>, or global <syntax-globaltype> type. Module instances are classified by module contexts, which are regular contexts <context> repurposed as module types describing the index spaces <syntax-index> defined by a module.

store, function instance, table instance, memory instance, global instance, function type, table type, memory type, global type

Store <syntax-store> S

• Each function instance <syntax-funcinst> $\funcinst_i$ in $S.\SFUNCS$ must be valid <valid-funcinst> with some function type <syntax-functype> $\functype_i$.
• Each table instance <syntax-tableinst> $\tableinst_i$ in $S.\STABLES$ must be valid <valid-tableinst> with some table type <syntax-tabletype> $\tabletype_i$.
• Each memory instance <syntax-meminst> $\meminst_i$ in $S.\SMEMS$ must be valid <valid-meminst> with some memory type <syntax-memtype> $\memtype_i$.
• Each global instance <syntax-globalinst> $\globalinst_i$ in $S.\SGLOBALS$ must be valid <valid-globalinst> with some global type <syntax-globaltype> $\globaltype_i$.
• Each element instance <syntax-eleminst> $\eleminst_i$ in $S.\SELEMS$ must be valid <valid-eleminst>.
• Each data instance <syntax-datainst> $\datainst_i$ in $S.\SDATAS$ must be valid <valid-datainst>.
• Then the store is valid.

$$\begin{aligned} ~\\[-1ex] \frac{ \begin{array}{@{}c@{}} (S \vdashfuncinst \funcinst : \functype)^\ast \qquad (S \vdashtableinst \tableinst : \tabletype)^\ast \\\ (S \vdashmeminst \meminst : \memtype)^\ast \qquad (S \vdashglobalinst \globalinst : \globaltype)^\ast \\\ (S \vdasheleminst \eleminst \ok)^\ast \qquad (S \vdashdatainst \datainst \ok)^\ast \\\ S = \{ \SFUNCS~\funcinst^\ast, \STABLES~\tableinst^\ast, \SMEMS~\meminst^\ast, \SGLOBALS~\globalinst^\ast, \SELEMS~\eleminst^\ast, \SDATAS~\datainst^\ast \} \end{array} }{ \vdashstore S \ok } \end{aligned}$$

function type, function instance

Function Instances <syntax-funcinst> $\{\FITYPE~\functype, \FIMODULE~\moduleinst, \FICODE~\func\}$

• The function type <syntax-functype> $\functype$ must be valid <valid-functype>.
• The module instance <syntax-moduleinst> $\moduleinst$ must be valid <valid-moduleinst> with some context <context> C.
• Under context <context> C, the function <syntax-func> $\func$ must be valid <valid-func> with function type <syntax-functype> $\functype$.
• Then the function instance is valid with function type <syntax-functype> $\functype$.

$$\frac{ \vdashfunctype \functype \ok \qquad S \vdashmoduleinst \moduleinst : C \qquad C \vdashfunc \func : \functype }{ S \vdashfuncinst \{\FITYPE~\functype, \FIMODULE~\moduleinst, \FICODE~\func\} : \functype }$$

function type, function instance, host function

Host Function Instances <syntax-funcinst> $\{\FITYPE~\functype, \FIHOSTCODE~\X{hf}\}$

• The function type <syntax-functype> $\functype$ must be valid <valid-functype>.
• Let [t₁^*] → [t₂^*] be the function type <syntax-functype> $\functype$.
• For every valid <valid-store> store <syntax-store> S₁ extending <extend-store> S and every sequence $\val^\ast$ of values <syntax-val> whose types <valid-val> coincide with t₁^*:
  • Executing <exec-invoke-host> $\X{hf}$ in store S₁ with arguments $\val^\ast$ has a non-empty set of possible outcomes.
  • For every element R of this set:
    • Either R must be ⊥ (i.e., divergence).
    • Or R consists of a valid <valid-store> store <syntax-store> S₂ extending <extend-store> S₁ and a result <syntax-result> $\result$ whose type <valid-result> coincides with [t₂^*].
• Then the function instance is valid with function type <syntax-functype> $\functype$.

$$\begin{aligned} \frac{ \begin{array}[b]{@{}l@{}} \vdashfunctype [t_1^\ast] \to [t_2^\ast] \ok \\\ \end{array} \quad \begin{array}[b]{@{}l@{}} \forall S_1, \val^\ast,~ {\vdashstore S_1 \ok} \wedge {\vdashstoreextends S \extendsto S_1} \wedge {S_1 \vdashresult \val^\ast : [t_1^\ast]} \Longrightarrow {} \\ \qquad \X{hf}(S_1; \val^\ast) \supset \emptyset \wedge {} \\ \qquad \forall R \in \X{hf}(S_1; \val^\ast),~ R = \bot \vee {} \\ \qquad\qquad \exists S_2, \result,~ {\vdashstore S_2 \ok} \wedge {\vdashstoreextends S_1 \extendsto S_2} \wedge {S_2 \vdashresult \result : [t_2^\ast]} \wedge R = (S_2; \result) \end{array} }{ S \vdashfuncinst \{\FITYPE~[t_1^\ast] \to [t_2^\ast], \FIHOSTCODE~\X{hf}\} : [t_1^\ast] \to [t_2^\ast] } \end{aligned}$$

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 <exec-invoke-host> 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 type, table instance, limits, function address

Table Instances <syntax-tableinst> $\{ \TITYPE~(\limits~t), \TIELEM~\reff^\ast \}$

• The table type <syntax-tabletype> $\limits~t$ must be valid <valid-tabletype>.
• The length of $\reff^\ast$ must equal $\limits.\LMIN$.
• For each reference <syntax-ref> $\reff_i$ in the table's elements $\reff^n$:
  • The reference <syntax-ref> $\reff_i$ must be valid <valid-ref> with reference type <syntax-reftype> t.
• Then the table instance is valid with table type <syntax-tabletype> $\limits~t$.

$$\frac{ \vdashtabletype \limits~t \ok \qquad n = \limits.\LMIN \qquad (S \vdash \reff : t)^n }{ S \vdashtableinst \{ \TITYPE~(\limits~t), \TIELEM~\reff^n \} : \limits~t }$$

memory type, memory instance, limits, byte

Memory Instances <syntax-meminst> $\{ \MITYPE~\limits, \MIDATA~b^\ast \}$

• The memory type <syntax-memtype> $\{\LMIN~n, \LMAX~m^?\}$ must be valid <valid-memtype>.
• The length of b^* must equal $\limits.\LMIN$ multiplied by the page size <page-size> $64\,\F{Ki}$.
• Then the memory instance is valid with memory type <syntax-memtype> $\limits$.

$$\frac{ \vdashmemtype \limits \ok \qquad n = \limits.\LMIN \cdot 64\,\F{Ki} }{ S \vdashmeminst \{ \MITYPE~\limits, \MIDATA~b^n \} : \limits }$$

global type, global instance, value, mutability

Global Instances <syntax-globalinst> $\{ \GITYPE~(\mut~t), \GIVALUE~\val \}$

• The global type <syntax-globaltype> $\mut~t$ must be valid <valid-globaltype>.
• The value <syntax-val> $\val$ must be valid <valid-val> with value type <syntax-valtype> t.
• Then the global instance is valid with global type <syntax-globaltype> $\mut~t$.

$$\frac{ \vdashglobaltype \mut~t \ok \qquad S \vdashval \val : t }{ S \vdashglobalinst \{ \GITYPE~(\mut~t), \GIVALUE~\val \} : \mut~t }$$

element instance, reference

Element Instances <syntax-eleminst> $\{ \EIELEM~\X{fa}^\ast \}$

• For each reference <syntax-ref> $\reff_i$ in the elements $\reff^n$:
  • The reference <syntax-ref> $\reff_i$ must be valid <valid-ref> with reference type <syntax-reftype> t.
• Then the table instance is valid.

$$\frac{ (S \vdash \reff : t)^\ast }{ S \vdasheleminst \{ \EITYPE~t, \EIELEM~\reff^\ast \} \ok }$$

data instance, byte

Data Instances <syntax-eleminst> $\{ \DIDATA~b^\ast \}$

• The data instance is valid.

$$\frac{ }{ S \vdashdatainst \{ \DIDATA~b^\ast \} \ok }$$

external type, export instance, name, external value

Export Instances <syntax-exportinst> $\{ \EINAME~\name, \EIVALUE~\externval \}$

• The external value <syntax-externval> $\externval$ must be valid <valid-externval> with some external type <syntax-externtype> $\externtype$.
• Then the export instance is valid.

$$\frac{ S \vdashexternval \externval : \externtype }{ S \vdashexportinst \{ \EINAME~\name, \EIVALUE~\externval \} \ok }$$

module instance, context

Module Instances <syntax-moduleinst> $\moduleinst$

• Each function type <syntax-functype> $\functype_i$ in $\moduleinst.\MITYPES$ must be valid <valid-functype>.
• For each function address <syntax-funcaddr> $\funcaddr_i$ in $\moduleinst.\MIFUNCS$, the external value <syntax-externval> $\EVFUNC~\funcaddr_i$ must be valid <valid-externval-func> with some external type <syntax-externtype> $\ETFUNC~\functype'_i$.
• For each table address <syntax-tableaddr> $\tableaddr_i$ in $\moduleinst.\MITABLES$, the external value <syntax-externval> $\EVTABLE~\tableaddr_i$ must be valid <valid-externval-table> with some external type <syntax-externtype> $\ETTABLE~\tabletype_i$.
• For each memory address <syntax-memaddr> $\memaddr_i$ in $\moduleinst.\MIMEMS$, the external value <syntax-externval> $\EVMEM~\memaddr_i$ must be valid <valid-externval-mem> with some external type <syntax-externtype> $\ETMEM~\memtype_i$.
• For each global address <syntax-globaladdr> $\globaladdr_i$ in $\moduleinst.\MIGLOBALS$, the external value <syntax-externval> $\EVGLOBAL~\globaladdr_i$ must be valid <valid-externval-global> with some external type <syntax-externtype> $\ETGLOBAL~\globaltype_i$.
• For each element address <syntax-elemaddr> $\elemaddr_i$ in $\moduleinst.\MIELEMS$, the element instance <syntax-eleminst> $S.\SELEMS[\elemaddr_i]$ must be valid <valid-eleminst>.
• For each data address <syntax-dataaddr> $\dataaddr_i$ in $\moduleinst.\MIDATAS$, the data instance <syntax-datainst> $S.\SDATAS[\dataaddr_i]$ must be valid <valid-datainst>.
• Each export instance <syntax-exportinst> $\exportinst_i$ in $\moduleinst.\MIEXPORTS$ must be valid <valid-exportinst>.
• For each export instance <syntax-exportinst> $\exportinst_i$ in $\moduleinst.\MIEXPORTS$, the name <syntax-name> $\exportinst_i.\EINAME$ must be different from any other name occurring in $\moduleinst.\MIEXPORTS$.
• Let ${\functype'}^\ast$ be the concatenation of all $\functype'_i$ in order.
• Let $\tabletype^\ast$ be the concatenation of all $\tabletype_i$ in order.
• Let $\memtype^\ast$ be the concatenation of all $\memtype_i$ in order.
• Let $\globaltype^\ast$ be the concatenation of all $\globaltype_i$ in order.
• Then the module instance is valid with context <context> $\{\CTYPES~\functype^\ast, \CFUNCS~{\functype'}^\ast, \CTABLES~\tabletype^\ast, \CMEMS~\memtype^\ast, \CGLOBALS~\globaltype^\ast\}$.

$$\begin{aligned} ~\\[-1ex] \frac{ \begin{array}{@{}c@{}} (\vdashfunctype \functype \ok)^\ast \\\ (S \vdashexternval \EVFUNC~\funcaddr : \ETFUNC~\functype')^\ast \qquad (S \vdashexternval \EVTABLE~\tableaddr : \ETTABLE~\tabletype)^\ast \\\ (S \vdashexternval \EVMEM~\memaddr : \ETMEM~\memtype)^\ast \qquad (S \vdashexternval \EVGLOBAL~\globaladdr : \ETGLOBAL~\globaltype)^\ast \\\ (S \vdasheleminst S.\SELEMS[\elemaddr] \ok)^\ast \qquad (S \vdashdatainst S.\SDATAS[\dataaddr] \ok)^\ast \\\ (S \vdashexportinst \exportinst \ok)^\ast \qquad (\exportinst.\EINAME)^\ast ~\mbox{disjoint} \end{array} }{ S \vdashmoduleinst \{ \begin{array}[t]{@{}l@{~}l@{}} \MITYPES & \functype^\ast, \\\ \MIFUNCS & \funcaddr^\ast, \\\ \MITABLES & \tableaddr^\ast, \\\ \MIMEMS & \memaddr^\ast, \\\ \MIGLOBALS & \globaladdr^\ast, \\\ \MIELEMS & \elemaddr^\ast, \\\ \MIDATAS & \dataaddr^\ast, \\\ \MIEXPORTS & \exportinst^\ast ~\} : \{ \begin{array}[t]{@{}l@{~}l@{}} \CTYPES & \functype^\ast, \\\ \CFUNCS & {\functype'}^\ast, \\\ \CTABLES & \tabletype^\ast, \\\ \CMEMS & \memtype^\ast, \\\ \CGLOBALS & \globaltype^\ast ~\} \end{array} \end{array} } \end{aligned}$$

configuration, administrative instruction, store, frame

Configuration Validity

To relate the WebAssembly type system <valid> to its execution semantics <exec>, the typing rules for instructions <valid-instr> must be extended to configurations <syntax-config> S; T, which relates the store <syntax-store> to execution threads <syntax-thread>.

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

Finally, frames <syntax-frame> are classified with frame contexts, which extend the module contexts <module-context> of a frame's associated module instance <syntax-moduleinst> with the locals <syntax-local> that the frame contains.

result type, thread

Configurations <syntax-config> S; T

• The store <syntax-store> S must be valid <valid-store>.
• Under no allowed return type, the thread <syntax-thread> T must be valid <valid-thread> with some result type <syntax-resulttype> [t^?].
• Then the configuration is valid with the result type <syntax-resulttype> [t^?].

$$\frac{ \vdashstore S \ok \qquad S; \epsilon \vdashthread T : [t^?] }{ \vdashconfig S; T : [t^?] }$$

thread, frame, instruction, result type, context

Threads <syntax-thread> $F;\instr^\ast$

• Let $\resulttype^?$ be the current allowed return type.
• The frame <syntax-frame> F must be valid <valid-frame> with a context <context> C.
• Let C′ be the same context <context> as C, but with set to $\resulttype^?$.
• Under context C′, the instruction sequence $\instr^\ast$ must be valid <valid-instr-seq> with some type [] → [t^?].
• Then the thread is valid with the result type <syntax-resulttype> [t^?].

$$\frac{ S \vdashframe F : C \qquad S; C,\CRETURN~\resulttype^? \vdashinstrseq \instr^\ast : [] \to [t^?] }{ S; \resulttype^? \vdashthread F; \instr^\ast : [t^?] }$$

frame, local, module instance, value, value type, context

Frames <syntax-frame> $\{\ALOCALS~\val^\ast, \AMODULE~\moduleinst\}$

• The module instance <syntax-moduleinst> $\moduleinst$ must be valid <valid-moduleinst> with some module context <module-context> C.
• Each value <syntax-val> $\val_i$ in $\val^\ast$ must be valid <valid-val> with some value type <syntax-valtype> t_i.
• Let t^* the concatenation of all t_i in order.
• Let C′ be the same context <context> as C, but with the value types <syntax-valtype> t^* prepended to the vector.
• Then the frame is valid with frame context <frame-context> C′.

$$\frac{ S \vdashmoduleinst \moduleinst : C \qquad (S \vdashval \val : t)^\ast }{ S \vdashframe \{\ALOCALS~\val^\ast, \AMODULE~\moduleinst\} : (C, \CLOCALS~t^\ast) }$$

administrative instruction, value type, context, store

Administrative Instructions

Typing rules for administrative instructions <syntax-instr-admin> are specified as follows. In addition to the context <context> C, typing of these instructions is defined under a given store <syntax-store> S. To that end, all previous typing judgements $C \vdash \X{prop}$ are generalized to include the store, as in $S; C \vdash \X{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 <valid-instr-admin> given below.

trap

$\TRAP$

• The instruction is valid with type [t₁^*] → [t₂^*], for any sequences of value types <syntax-valtype> t₁^* and t₂^*.

$$\frac{ }{ S; C \vdashadmininstr \TRAP : [t_1^\ast] \to [t_2^\ast] }$$

extern address

$\REFEXTERNADDR~\externaddr$

• The instruction is valid with type $[] \to [\EXTERNREF]$.

$$\frac{ }{ S; C \vdashadmininstr \REFEXTERNADDR~\externaddr : [] \to [\EXTERNREF] }$$

function address, extern value, extern type, function type

$\REFFUNCADDR~\funcaddr$

• The external function value <syntax-externval> $\EVFUNC~\funcaddr$ must be valid <valid-externval-func> with external function type <syntax-externtype> $\ETFUNC \functype$.
• Then the instruction is valid with type $[] \to [\FUNCREF]$.

$$\frac{ S \vdashexternval \EVFUNC~\funcaddr : \ETFUNC~\functype }{ S; C \vdashadmininstr \REFFUNCADDR~\funcaddr : [] \to [\FUNCREF] }$$

function address, extern value, extern type, function type

$\INVOKE~\funcaddr$

• The external function value <syntax-externval> $\EVFUNC~\funcaddr$ must be valid <valid-externval-func> with external function type <syntax-externtype> $\ETFUNC ([t_1^\ast] \to [t_2^\ast])$.
• Then the instruction is valid with type [t₁^*] → [t₂^*].

$$\frac{ S \vdashexternval \EVFUNC~\funcaddr : \ETFUNC~[t_1^\ast] \to [t_2^\ast] }{ S; C \vdashadmininstr \INVOKE~\funcaddr : [t_1^\ast] \to [t_2^\ast] }$$

label, instruction, result type

$\LABEL_n\{\instr_0^\ast\}~\instr^\ast~\END$

• The instruction sequence $\instr_0^\ast$ must be valid <valid-instr-seq> with some type [t₁ⁿ] → [t₂^?].
• Let C′ be the same context <context> as C, but with the result type <syntax-resulttype> [t₁ⁿ] prepended to the vector.
• Under context C′, the instruction sequence $\instr^\ast$ must be valid <valid-instr-seq> with type [] → [t₂^?].
• Then the compound instruction is valid with type [] → [t₂^?].

$$\frac{ S; C \vdashinstrseq \instr_0^\ast : [t_1^n] \to [t_2^?] \qquad S; C,\CLABELS\,[t_1^n] \vdashinstrseq \instr^\ast : [] \to [t_2^?] }{ S; C \vdashadmininstr \LABEL_n\{\instr_0^\ast\}~\instr^\ast~\END : [] \to [t_2^?] }$$

frame, instruction, result type

$\FRAME_n\{F\}~\instr^\ast~\END$

• Under the return type [tⁿ], the thread <syntax-frame> $F; \instr^\ast$ must be valid <valid-frame> with result type <syntax-resulttype> [tⁿ].
• Then the compound instruction is valid with type [] → [tⁿ].

$$\frac{ S; [t^n] \vdashinstrseq F; \instr^\ast : [t^n] }{ S; C \vdashadmininstr \FRAME_n\{F\}~\instr^\ast~\END : [] \to [t^n] }$$

! store extension, store

Store Extension

Programs can mutate the store <syntax-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 <exec-instr> and modules <exec-instantiation>, host functions <syntax-hostfunc> do not automatically adhere to them. Consequently, the required invariants must be stated as explicit constraints on the invocation <exec-invoke-host> of host functions. Soundness only holds when the embedder <embedder> ensures these constraints.

The necessary constraints are codified by the notion of store extension: a store state S′ extends state S, written $S \extendsto S'$, when the following rules hold.

Note

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

store, function instance, table instance, memory instance, global instance

Store <syntax-store> S

• The length of $S.\SFUNCS$ must not shrink.
• The length of $S.\STABLES$ must not shrink.
• The length of $S.\SMEMS$ must not shrink.
• The length of $S.\SGLOBALS$ must not shrink.
• The length of $S.\SELEMS$ must not shrink.
• The length of $S.\SDATAS$ must not shrink.
• For each function instance <syntax-funcinst> $\funcinst_i$ in the original $S.\SFUNCS$, the new function instance must be an extension <extend-funcinst> of the old.
• For each table instance <syntax-tableinst> $\tableinst_i$ in the original $S.\STABLES$, the new table instance must be an extension <extend-tableinst> of the old.
• For each memory instance <syntax-meminst> $\meminst_i$ in the original $S.\SMEMS$, the new memory instance must be an extension <extend-meminst> of the old.
• For each global instance <syntax-globalinst> $\globalinst_i$ in the original $S.\SGLOBALS$, the new global instance must be an extension <extend-globalinst> of the old.
• For each element instance <syntax-eleminst> $\eleminst_i$ in the original $S.\SELEMS$, the new global instance must be an extension <extend-eleminst> of the old.
• For each data instance <syntax-datainst> $\datainst_i$ in the original $S.\SDATAS$, the new global instance must be an extension <extend-datainst> of the old.

$$\begin{aligned} \frac{ \begin{array}{@{}ccc@{}} S_1.\SFUNCS = \funcinst_1^\ast & S_2.\SFUNCS = {\funcinst'_1}^\ast~\funcinst_2^\ast & (\vdashfuncinstextends \funcinst_1 \extendsto \funcinst'_1)^\ast \\\ S_1.\STABLES = \tableinst_1^\ast & S_2.\STABLES = {\tableinst'_1}^\ast~\tableinst_2^\ast & (\vdashtableinstextends \tableinst_1 \extendsto \tableinst'_1)^\ast \\\ S_1.\SMEMS = \meminst_1^\ast & S_2.\SMEMS = {\meminst'_1}^\ast~\meminst_2^\ast & (\vdashmeminstextends \meminst_1 \extendsto \meminst'_1)^\ast \\\ S_1.\SGLOBALS = \globalinst_1^\ast & S_2.\SGLOBALS = {\globalinst'_1}^\ast~\globalinst_2^\ast & (\vdashglobalinstextends \globalinst_1 \extendsto \globalinst'_1)^\ast \\\ S_1.\SELEMS = \eleminst_1^\ast & S_2.\SELEMS = {\eleminst'_1}^\ast~\eleminst_2^\ast & (\vdasheleminstextends \eleminst_1 \extendsto \eleminst'_1)^\ast \\\ S_1.\SDATAS = \datainst_1^\ast & S_2.\SDATAS = {\datainst'_1}^\ast~\datainst_2^\ast & (\vdashdatainstextends \datainst_1 \extendsto \datainst'_1)^\ast \\\ \end{array} }{ \vdashstoreextends S_1 \extendsto S_2 } \end{aligned}$$

function instance

Function Instance <syntax-funcinst> $\funcinst$

• A function instance must remain unchanged.

$$\frac{ }{ \vdashfuncinstextends \funcinst \extendsto \funcinst }$$

table instance

Table Instance <syntax-tableinst> $\tableinst$

• The table type <syntax-tabletype> $\tableinst.\TITYPE$ must remain unchanged.
• The length of $\tableinst.\TIELEM$ must not shrink.

$$\frac{ n_1 \leq n_2 }{ \vdashtableinstextends \{\TITYPE~\X{tt}, \TIELEM~(\X{fa}_1^?)^{n_1}\} \extendsto \{\TITYPE~\X{tt}, \TIELEM~(\X{fa}_2^?)^{n_2}\} }$$

memory instance

Memory Instance <syntax-meminst> $\meminst$

• The memory type <syntax-memtype> $\meminst.\MITYPE$ must remain unchanged.
• The length of $\meminst.\MIDATA$ must not shrink.

$$\frac{ n_1 \leq n_2 }{ \vdashmeminstextends \{\MITYPE~\X{mt}, \MIDATA~b_1^{n_1}\} \extendsto \{\MITYPE~\X{mt}, \MIDATA~b_2^{n_2}\} }$$

global instance, value, mutability

Global Instance <syntax-globalinst> $\globalinst$

• The global type <syntax-globaltype> $\globalinst.\GITYPE$ must remain unchanged.
• Let $\mut~t$ be the structure of $\globalinst.\GITYPE$.
• If $\mut$ is , then the value <syntax-val> $\globalinst.\GIVALUE$ must remain unchanged.

$$\frac{ \mut = \MVAR \vee \val_1 = \val_2 }{ \vdashglobalinstextends \{\GITYPE~(\mut~t), \GIVALUE~\val_1\} \extendsto \{\GITYPE~(\mut~t), \GIVALUE~\val_2\} }$$

element instance

Element Instance <syntax-eleminst> $\eleminst$

• The vector $\eleminst.\EIELEM$ must either remain unchanged or shrink to length 0.

$$\frac{ \X{fa}_1^\ast = \X{fa}_2^\ast \vee \X{fa}_2^\ast = \epsilon }{ \vdasheleminstextends \{\EIELEM~\X{fa}_1^\ast\} \extendsto \{\EIELEM~\X{fa}_2^\ast\} }$$

data instance

Data Instance <syntax-datainst> $\datainst$

• The vector $\datainst.\DIDATA$ must either remain unchanged or shrink to length 0.

$$\frac{ b_1^\ast = b_2^\ast \vee b_2^\ast = \epsilon }{ \vdashdatainstextends \{\DIDATA~b_1^\ast\} \extendsto \{\DIDATA~b_2^\ast\} }$$

! preservation, ! progress, soundness, configuration, thread, terminal configuration, instantiation, invocation, validity, module

Theorems

Given the definition of valid configurations <valid-config>, the standard soundness theorems hold.²

Theorem (Preservation). If a configuration <syntax-config> S; T is valid <valid-config> with result type <syntax-resulttype> [t^*] (i.e., $\vdashconfig S;T : [t^\ast]$), and steps to S′; T′ (i.e., $S;T \stepto S';T'$), then S′; T′ is a valid configuration with the same result type (i.e., $\vdashconfig S';T' : [t^\ast]$). Furthermore, S′ is an extension <extend-store> of S (i.e., $\vdashstoreextends S \extendsto S'$).

A terminal thread <syntax-thread> is one whose sequence of instructions <syntax-instr> is a result <syntax-result>. A terminal configuration is a configuration whose thread is terminal.

Theorem (Progress). If a configuration <syntax-config> S; T is valid <valid-config> (i.e., $\vdashconfig S;T : [t^\ast]$ for some result type <syntax-resulttype> [t^*]), then either it is terminal, or it can step to some configuration S′; T′ (i.e., $S;T \stepto S';T'$).

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

Corollary (Soundness). If a configuration <syntax-config> S; T is valid <valid-config> (i.e., $\vdashconfig S;T : [t^\ast]$ for some result type <syntax-resulttype> [t^*]), then it either diverges or takes a finite number of steps to reach a terminal configuration S′; T′ (i.e., $S;T \stepto^\ast S';T'$) that is valid with the same result type (i.e., $\vdashconfig S';T' : [t^\ast]$) and where S′ is an extension <extend-store> of S (i.e., $\vdashstoreextends S \extendsto S'$).

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 <valid-store>, no computation defined by instantiation <exec-instantiation> or invocation <exec-invocation> of a valid module can "crash" or otherwise (mis)behave in ways not covered by the execution <exec> 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. _. 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 is described in the following article: Conrad Watt. _. Proceedings of the 7th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2018). ACM 2018.↩