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 diverge, throw an exception, or trap).

• 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:

𝐶::={ …,𝗋𝖾𝖼𝗌 subtype∗ }

Types

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

Heap Type 𝖻𝗈𝗍

• The heap type is valid.

𝐶⊢𝖻𝗈𝗍:𝗈𝗄

Heap Type 𝗋𝖾𝖼 𝑖

• The recursive type index 𝑖 must exist in 𝐶.𝗋𝖾𝖼𝗌.

• Then the heap type is valid.

𝐶.𝗋𝖾𝖼𝗌⁡[𝑖]=subtype𝐶⊢𝗋𝖾𝖼 𝑖:𝗈𝗄

Value Type 𝖻𝗈𝗍

• The value type is valid.

𝐶⊢𝖻𝗈𝗍:𝗈𝗄

Recursive Types 𝗋𝖾𝖼 subtype∗

• Let 𝐶′ be the current context 𝐶, but where 𝗋𝖾𝖼𝗌 is subtype∗.

• There must be a type index 𝑥, such that for each sub type subtype𝑖 in subtype∗:

  • Under the context 𝐶′, the sub type subtype𝑖 must be valid for type index 𝑥 +𝑖 and recursive type index 𝑖.

• Then the recursive type is valid for the type index 𝑥.

𝐶,𝗋𝖾𝖼𝗌 subtype∗⊢𝗋𝖾𝖼 subtype∗:𝗈𝗄⁡(𝑥,0)𝐶⊢𝗋𝖾𝖼 subtype∗:𝗈𝗄⁡(𝑥)

𝐶⊢𝗋𝖾𝖼 𝜖:𝗈𝗄⁡(𝑥,𝑖)𝐶⊢subtype:𝗈𝗄⁡(𝑥,𝑖)𝐶⊢𝗋𝖾𝖼 subtype′∗:𝗈𝗄⁡(𝑥+1,𝑖+1)𝐶⊢𝗋𝖾𝖼 subtype subtype′∗:𝗈𝗄⁡(𝑥,𝑖)

Note

These rules are a generalisation of the ones previously given.

Sub types 𝗌𝗎𝖻 𝖿𝗂𝗇𝖺𝗅? ht∗ comptype

• The composite type comptype must be valid.

• The sequence ht∗ may be no longer than 1.

• For every heap type ht𝑘 in ht∗:

  • The heap type ht𝑘 must be ordered before a type index 𝑥 and recursive type index a 𝑖, meaning:

    • Either ht𝑘 is a defined type.

    • Or ht𝑘 is a type index 𝑦𝑘 that is smaller than 𝑥.

    • Or ht𝑘 is a recursive type index 𝗋𝖾𝖼 𝑗𝑘 where 𝑗𝑘 is smaller than 𝑖.

  • Let sub type subtype𝑘 be the unrolling of the heap type ht𝑘, meaning:

    • Either ht𝑘 is a defined type deftype𝑘, then subtype𝑘 must be the unrolling of deftype𝑘.

    • Or ht𝑘 is a type index 𝑦𝑘, then subtype𝑘 must be the unrolling of the defined type 𝐶.𝗍𝗒𝗉𝖾𝗌⁡[𝑦𝑘].

    • Or ht𝑘 is a recursive type index 𝗋𝖾𝖼 𝑗𝑘, then subtype𝑘 must be 𝐶.𝗋𝖾𝖼𝗌⁡[𝑗𝑘].

  • The sub type subtype𝑘 must not contain 𝖿𝗂𝗇𝖺𝗅.

  • Let comptype′𝑘 be the composite type in subtype𝑘.

  • The composite type comptype must match comptype′𝑘.

• Then the sub type is valid for the type index 𝑥 and recursive type index 𝑖.

|ht∗|≤1(ht≺𝑥,𝑖)∗(unroll𝐶⁢(ht)=𝗌𝗎𝖻 ht′∗ comptype′)∗𝐶⊢comptype:𝗈𝗄(𝐶⊢comptype≤comptype′)∗𝐶⊢𝗌𝗎𝖻 𝖿𝗂𝗇𝖺𝗅? ht∗ comptype:𝗈𝗄⁡(𝑥,𝑖)

where:

(deftype≺𝑥,𝑖)=true(𝑦≺𝑥,𝑖)=𝑦<𝑥(𝗋𝖾𝖼 𝑗≺𝑥,𝑖)=𝑗<𝑖[2⁢𝑒⁢𝑥]⁢unroll𝐶⁡(deftype)=unroll⁡(deftype)unroll𝐶⁡(𝑦)=unroll⁡(𝐶.𝗍𝗒𝗉𝖾𝗌⁡[𝑦])unroll𝐶⁡(𝗋𝖾𝖼 𝑗)=𝐶.𝗋𝖾𝖼𝗌⁡[𝑗]

Note

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

Defined types rectype.𝑖

The defined type (rectype . 𝑖) is valid if:

• The recursive type rectype is valid for the type index 𝑥.

• The recursive type rectype is of the form (𝗋𝖾𝖼 subtype𝑛).

• 𝑖 is less than 𝑛.

𝐶⊢rectype:𝗈𝗄⁡(𝑥)rectype=𝗋𝖾𝖼 subtype𝑛𝑖<𝑛𝐶⊢rectype . 𝑖:𝗈𝗄

Subtyping

In a rolled-up recursive type, a recursive type indices 𝗋𝖾𝖼 𝑖 matches another heap type ht if:

• Let 𝗌𝗎𝖻 𝖿𝗂𝗇𝖺𝗅? ht′∗ comptype be the sub type 𝐶.𝗋𝖾𝖼𝗌⁡[𝑖].

• The heap type ht is contained in ht′∗.

𝐶.𝗋𝖾𝖼𝗌⁡[𝑖]=𝗌𝗎𝖻 𝖿𝗂𝗇𝖺𝗅? (ht∗1 ht ht∗2) comptype𝐶⊢𝗋𝖾𝖼 𝑖≤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 val∗

• For each value val𝑖 in val∗:

  • The value val𝑖 is valid with some value type 𝑡𝑖.

• Let 𝑡∗ be the concatenation of all 𝑡𝑖.

• Then the result is valid with result type [𝑡∗].

(𝑆⊢val:𝑡)∗𝑆⊢val∗:[𝑡∗]

Results (𝗋𝖾𝖿.𝖾𝗑𝗇 𝑎) 𝗍𝗁𝗋𝗈𝗐_𝗋𝖾𝖿

• The value 𝗋𝖾𝖿.𝖾𝗑𝗇 𝑎 must be valid.

• Then the result is valid with result type [𝑡∗], for any valid closed result types.

𝑆⊢𝗋𝖾𝖿.𝖾𝗑𝗇 𝑎:𝗋𝖾𝖿 𝖾𝗑𝗇⊢[𝑡∗]:𝗈𝗄𝑆⊢(𝗋𝖾𝖿.𝖾𝗑𝗇 𝑎) 𝗍𝗁𝗋𝗈𝗐_𝗋𝖾𝖿:[𝑡′∗]

Results 𝗍𝗋𝖺𝗉

• The result is valid with result type [𝑡∗], for any valid closed result types.

⊢[𝑡∗]:𝗈𝗄𝑆⊢𝗍𝗋𝖺𝗉:[𝑡∗]

Store Validity

The following typing rules specify when a runtime store 𝑆 is valid. A valid store must consist of tag, global, memory, table, function, data, element, structure, array, exception, and module instances that are themselves valid, relative to 𝑆.

To that end, each kind of instance is classified by a respective tag, global, memory, table, function, or element, type, or just 𝗈𝗄 in the case of data structures, arrays, or exceptions. Module instances are classified by module contexts, which are regular contexts repurposed as module types describing the index spaces defined by a module.

Store 𝑆

• Each tag instance taginst𝑖 in 𝑆.𝗍𝖺𝗀𝗌 must be valid with some tag type tagtype𝑖.

• Each global instance globalinst𝑖 in 𝑆.𝗀𝗅𝗈𝖻𝖺𝗅𝗌 must be valid with some global type globaltype𝑖.

• Each memory instance meminst𝑖 in 𝑆.𝗆𝖾𝗆𝗌 must be valid with some memory type memtype𝑖.

• Each table instance tableinst𝑖 in 𝑆.𝗍𝖺𝖻𝗅𝖾𝗌 must be valid with some table type tabletype𝑖.

• Each function instance funcinst𝑖 in 𝑆.𝖿𝗎𝗇𝖼𝗌 must be valid with some defined type deftype𝑖.

• Each data instance datainst𝑖 in 𝑆.𝖽𝖺𝗍𝖺𝗌 must be valid.

• Each element instance eleminst𝑖 in 𝑆.𝖾𝗅𝖾𝗆𝗌 must be valid with some reference type reftype𝑖.

• Each structure instance structinst𝑖 in 𝑆.𝗌𝗍𝗋𝗎𝖼𝗍𝗌 must be valid.

• Each array instance arrayinst𝑖 in 𝑆.𝖺𝗋𝗋𝖺𝗒𝗌 must be valid.

• Each exception instance exninst𝑖 in 𝑆.𝖾𝗑𝗇𝗌 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 or fields of exception instances.

• 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 or fields of exception instances.

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

• Then the store is valid.

 (𝑆⊢taginst:tagtype)∗(𝑆⊢globalinst:globaltype)∗(𝑆⊢meminst:memtype)∗(𝑆⊢tableinst:tabletype)∗(𝑆⊢funcinst:deftype)∗(𝑆⊢datainst:𝗈𝗄)∗(𝑆⊢eleminst:reftype)∗(𝑆⊢structinst:𝗈𝗄)∗(𝑆⊢arrayinst:𝗈𝗄)∗(𝑆⊢exninst:𝗈𝗄)∗𝑆={𝗍𝖺𝗀𝗌 taginst∗,𝗀𝗅𝗈𝖻𝖺𝗅𝗌 globalinst∗,𝗆𝖾𝗆𝗌 meminst∗,𝗍𝖺𝖻𝗅𝖾𝗌 tableinst∗,𝖿𝗎𝗇𝖼𝗌 funcinst∗,𝖽𝖺𝗍𝖺𝗌 datainst∗,𝖾𝗅𝖾𝗆𝗌 eleminst∗,𝗌𝗍𝗋𝗎𝖼𝗍𝗌 structinst∗,𝖺𝗋𝗋𝖺𝗒𝗌 arrayinst∗,𝖾𝗑𝗇𝗌 exninst∗}(𝑆.𝗌𝗍𝗋𝗎𝖼𝗍𝗌⁡[𝑎s]=structinst)∗((𝗋𝖾𝖿.𝗌𝗍𝗋𝗎𝖼𝗍 𝑎s)≫̸+𝑆(𝗋𝖾𝖿.𝗌𝗍𝗋𝗎𝖼𝗍 𝑎s))∗(𝑆.𝖺𝗋𝗋𝖺𝗒𝗌⁡[𝑎a]=arrayinst)∗((𝗋𝖾𝖿.𝖺𝗋𝗋𝖺𝗒 𝑎a)≫̸+𝑆(𝗋𝖾𝖿.𝖺𝗋𝗋𝖺𝗒 𝑎a))∗(𝑆.𝖾𝗑𝗇𝗌⁡[𝑎e]=exninst)∗((𝗋𝖾𝖿.𝖾𝗑𝗇 𝑎e)≫̸+𝑆(𝗋𝖾𝖿.𝖾𝗑𝗇 𝑎e))∗⊢𝑆:𝗈𝗄

where val1 ≫+𝑆val2 denotes the transitive closure of the following immutable reachability relation on values:

(𝗋𝖾𝖿.𝗌𝗍𝗋𝗎𝖼𝗍 𝑎)≫𝑆𝑆.𝗌𝗍𝗋𝗎𝖼𝗍𝗌⁡[𝑎].𝖿𝗂𝖾𝗅𝖽𝗌⁡[𝑖]ifexpand⁡(𝑆.𝗌𝗍𝗋𝗎𝖼𝗍𝗌⁡[𝑎].𝗍𝗒𝗉𝖾)=𝗌𝗍𝗋𝗎𝖼𝗍 ft𝑖1 st ft∗2(𝗋𝖾𝖿.𝖺𝗋𝗋𝖺𝗒 𝑎)≫𝑆𝑆.𝖺𝗋𝗋𝖺𝗒𝗌⁡[𝑎].𝖿𝗂𝖾𝗅𝖽𝗌⁡[𝑖]ifexpand⁡(𝑆.𝖺𝗋𝗋𝖺𝗒𝗌⁡[𝑎].𝗍𝗒𝗉𝖾)=𝖺𝗋𝗋𝖺𝗒 st(𝗋𝖾𝖿.𝖾𝗑𝗇 𝑎)≫𝑆𝑆.𝖾𝗑𝗇𝗌⁡[𝑎].𝖿𝗂𝖾𝗅𝖽𝗌⁡[𝑖](𝗋𝖾𝖿.𝖾𝗑𝗍𝖾𝗋𝗇 ref)≫𝑆ref

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.

Tag Instances {𝗍𝗒𝗉𝖾 tagtype}

• The tag type tagtype must be valid under the empty context.

• Then the tag instance is valid with tag type tagtype.

⊢tagtype:𝗈𝗄𝑆⊢{𝗍𝗒𝗉𝖾 tagtype}:tagtype

Global Instances {𝗍𝗒𝗉𝖾 mut 𝑡,𝗏𝖺𝗅𝗎𝖾 val}

• The global type mut 𝑡 must be valid under the empty context.

• The value val must be valid with some value type 𝑡′.

• The value type 𝑡′ must match the value type 𝑡.

• Then the global instance is valid with global type mut 𝑡.

⊢mut 𝑡:𝗈𝗄𝑆⊢val:𝑡′⊢𝑡′≤𝑡𝑆⊢{𝗍𝗒𝗉𝖾 mut 𝑡,𝗏𝖺𝗅𝗎𝖾 val}:mut 𝑡

Memory Instances {𝗍𝗒𝗉𝖾 (addrtype limits),𝖻𝗒𝗍𝖾𝗌 𝑏∗}

• The memory type addrtype limits must be valid under the empty context.

• Let limits be [𝑛 .. 𝑚].

• The length of 𝑏∗ must equal 𝑚 multiplied by the page size 64 Ki.

• Then the memory instance is valid with memory type addrtype limits.

⊢addrtype [𝑛..𝑚]:𝗈𝗄|𝑏∗|=𝑛⋅64Ki𝑆⊢{𝗍𝗒𝗉𝖾 (addrtype [𝑛..𝑚]),𝖻𝗒𝗍𝖾𝗌 𝑏∗}:addrtype [𝑛..𝑚]

Table Instances {𝗍𝗒𝗉𝖾 (addrtype limits 𝑡),𝖾𝗅𝖾𝗆 ref∗}

• The table type addrtype limits 𝑡 must be valid under the empty context.

• Let limits be [𝑛 .. 𝑚].

• The length of ref∗ must equal 𝑛.

• For each reference ref𝑖 in the table’s elements ref𝑛:

  • The reference ref𝑖 must be valid with some reference type 𝑡′𝑖.

  • The reference type 𝑡′𝑖 must match the reference type 𝑡.

• Then the table instance is valid with table type addrtype limits 𝑡.

⊢addrtype [𝑛..𝑚] 𝑡:𝗈𝗄|ref∗|=𝑛(𝑆⊢ref:𝑡′)∗(⊢𝑡′≤𝑡)∗𝑆⊢{𝗍𝗒𝗉𝖾 (addrtype [𝑛..𝑚] 𝑡),𝖾𝗅𝖾𝗆 ref∗}:addrtype [𝑛..𝑚] 𝑡

Function Instances {𝗍𝗒𝗉𝖾 deftype,𝗆𝗈𝖽𝗎𝗅𝖾 moduleinst,𝖼𝗈𝖽𝖾 func}

• The defined type deftype must be valid under an empty context.

• The module instance moduleinst must be valid with some context 𝐶.

• Under context 𝐶:

  • The function func must be valid with some defined type deftype′.

  • The defined type deftype′ must match deftype.

• Then the function instance is valid with defined type deftype.

⊢deftype:𝗈𝗄𝑆⊢moduleinst:𝐶𝐶⊢func:deftype′𝐶⊢deftype′≤deftype𝑆⊢{𝗍𝗒𝗉𝖾 deftype,𝗆𝗈𝖽𝗎𝗅𝖾 moduleinst,𝖼𝗈𝖽𝖾 func}:deftype

Host Function Instances {𝗍𝗒𝗉𝖾 deftype,𝗁𝗈𝗌𝗍𝖿𝗎𝗇𝖼 hf}

• The defined type deftype must be valid under an empty context.

• The expansion of defined type deftype must be some function type 𝖿𝗎𝗇𝖼 [𝑡∗1] →[𝑡∗2].

• For every valid store 𝑆1 extending 𝑆 and every sequence val∗ of values whose types coincide with 𝑡∗1:

  • Executing hf in store 𝑆1 with arguments val∗ has a non-empty set of possible outcomes.

  • For every element 𝑅 of this set:

    • Either 𝑅 must be ⊥ (i.e., divergence).

    • Or 𝑅 consists of a valid store 𝑆2 extending 𝑆1 and a result result whose type coincides with [𝑡∗2].

• Then the function instance is valid with defined type deftype.

⊢deftype:𝗈𝗄deftype≈𝖿𝗎𝗇𝖼 [𝑡∗1]→[𝑡∗2]∀𝑆1,val∗, ⊢𝑆1:𝗈𝗄∧⊢𝑆⪯𝑆1∧𝑆1⊢val∗:[𝑡∗1]⟹hf⁡(𝑆1;val∗)⊃∅∧∀𝑅∈hf⁡(𝑆1;val∗), 𝑅=⊥∨∃𝑆2,result, ⊢𝑆2:𝗈𝗄∧⊢𝑆1⪯𝑆2∧𝑆2⊢result:[𝑡∗2]∧𝑅=(𝑆2;result)𝑆⊢{𝗍𝗒𝗉𝖾 deftype,𝗁𝗈𝗌𝗍𝖿𝗎𝗇𝖼 hf}:deftype

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.

Data Instances {𝖻𝗒𝗍𝖾𝗌 𝑏∗}

• The data instance is valid.

𝑆⊢{𝖻𝗒𝗍𝖾𝗌 𝑏∗}:𝗈𝗄

Element Instances {𝗍𝗒𝗉𝖾 𝑡,𝖾𝗅𝖾𝗆 ref∗}

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

• For each reference ref𝑖 in the elements ref𝑛:

  • The reference ref𝑖 must be valid with some reference type 𝑡′𝑖.

  • The reference type 𝑡′𝑖 must match the reference type 𝑡.

• Then the element instance is valid with reference type 𝑡.

⊢𝑡:𝗈𝗄(𝑆⊢ref:𝑡′)∗(⊢𝑡′≤𝑡)∗𝑆⊢{𝗍𝗒𝗉𝖾 𝑡,𝖾𝗅𝖾𝗆 ref∗}:𝑡

Structure Instances {𝗍𝗒𝗉𝖾 deftype,𝖿𝗂𝖾𝗅𝖽𝗌 fieldval∗}

• The defined type deftype must be valid under the empty context.

• The expansion of deftype must be a structure type 𝗌𝗍𝗋𝗎𝖼𝗍 fieldtype∗.

• The length of the sequence of field values fieldval∗ must be the same as the length of the sequence of field types fieldtype∗.

• For each field value fieldval𝑖 in fieldval∗ and corresponding field type fieldtype𝑖 in fieldtype∗:

  • Let fieldtype𝑖 be mut storagetype𝑖.

  • The field value fieldval𝑖 must be valid with storage type storagetype𝑖.

• Then the structure instance is valid.

⊢dt:𝗈𝗄expand⁡(dt)=𝗌𝗍𝗋𝗎𝖼𝗍 (mut st)∗(𝑆⊢fv:st)∗𝑆⊢{𝗍𝗒𝗉𝖾 dt,𝖿𝗂𝖾𝗅𝖽𝗌 fv∗}:𝗈𝗄

Array Instances {𝗍𝗒𝗉𝖾 deftype,𝖿𝗂𝖾𝗅𝖽𝗌 fieldval∗}

• The defined type deftype must be valid under the empty context.

• The expansion of deftype must be an array type 𝖺𝗋𝗋𝖺𝗒 fieldtype.

• Let fieldtype be mut storagetype.

• For each field value fieldval𝑖 in fieldval∗:

  • The field value fieldval𝑖 must be valid with storage type storagetype.

• Then the array instance is valid.

⊢dt:𝗈𝗄expand⁡(dt)=𝖺𝗋𝗋𝖺𝗒 (mut st)(𝑆⊢fv:st)∗𝑆⊢{𝗍𝗒𝗉𝖾 dt,𝖿𝗂𝖾𝗅𝖽𝗌 fv∗}:𝗈𝗄

Field Values fieldval

• If fieldval is a value val, then:

  • The value val must be valid with value type 𝑡.

  • Then the field value is valid with value type 𝑡.

• Else, fieldval is a packed value packval:

  • Let packtype.𝗉𝖺𝖼𝗄 𝑖 be the field value fieldval.

  • Then the field value is valid with packed type packtype.

𝑆⊢pt.𝗉𝖺𝖼𝗄 𝑖:pt

Exception Instances {𝗍𝖺𝗀 𝑎,𝖿𝗂𝖾𝗅𝖽𝗌 val∗}

• The store entry 𝑆.𝗍𝖺𝗀𝗌⁡[𝑎] must exist.

• The expansion of the tag type 𝑆.𝗍𝖺𝗀𝗌⁡[𝑎].𝗍𝗒𝗉𝖾 must be some function type 𝖿𝗎𝗇𝖼 [𝑡∗] →[𝑡′∗].

• The result type [𝑡′∗] must be empty.

• The sequence val𝑎⁢𝑠⁢𝑡 of values must have the same length as the sequence 𝑡∗ of value types.

• For each value val𝑖 in val𝑎⁢𝑠⁢𝑡 and corresponding value type 𝑡𝑖 in 𝑡∗, the value val𝑖 must be valid with type 𝑡𝑖.

• Then the exception instance is valid.

𝑆.𝗍𝖺𝗀𝗌⁡[𝑎].𝗍𝗒𝗉𝖾≈𝖿𝗎𝗇𝖼 [𝑡∗]→[](𝑆⊢val:𝑡)∗𝑆⊢{𝗍𝖺𝗀 𝑎,𝖿𝗂𝖾𝗅𝖽𝗌 val∗}:𝗈𝗄

Export Instances {𝗇𝖺𝗆𝖾 name,𝖺𝖽𝖽𝗋 externaddr}

• The external address externaddr must be valid with some external type externtype.

• Then the export instance is valid.

𝑆⊢externaddr:externtype𝑆⊢{𝗇𝖺𝗆𝖾 name,𝖺𝖽𝖽𝗋 externaddr}:𝗈𝗄

Module Instances moduleinst

• Each defined type deftype𝑖 in moduleinst.𝗍𝗒𝗉𝖾𝗌 must be valid under the empty context.

• For each tag address tagaddr𝑖 in moduleinst.𝗍𝖺𝗀𝗌, the external address 𝗍𝖺𝗀 tagaddr𝑖 must be valid with some external type 𝗍𝖺𝗀 tagtype𝑖.

• For each global address globaladdr𝑖 in moduleinst.𝗀𝗅𝗈𝖻𝖺𝗅𝗌, the external address 𝗀𝗅𝗈𝖻𝖺𝗅 globaladdr𝑖 must be valid with some external type 𝗀𝗅𝗈𝖻𝖺𝗅 globaltype𝑖.

• For each memory address memaddr𝑖 in moduleinst.𝗆𝖾𝗆𝗌, the external address 𝗆𝖾𝗆 memaddr𝑖 must be valid with some external type 𝗆𝖾𝗆 memtype𝑖.

• For each table address tableaddr𝑖 in moduleinst.𝗍𝖺𝖻𝗅𝖾𝗌, the external address 𝗍𝖺𝖻𝗅𝖾 tableaddr𝑖 must be valid with some external type 𝗍𝖺𝖻𝗅𝖾 tabletype𝑖.

• For each function address funcaddr𝑖 in moduleinst.𝖿𝗎𝗇𝖼𝗌, the external address 𝖿𝗎𝗇𝖼 funcaddr𝑖 must be valid with some external type 𝖿𝗎𝗇𝖼 deftype𝖥⁡𝑖.

• For each data address dataaddr𝑖 in moduleinst.𝖽𝖺𝗍𝖺𝗌, the data instance 𝑆.𝖽𝖺𝗍𝖺𝗌⁡[dataaddr𝑖] must be valid with ok𝑖.

• For each element address elemaddr𝑖 in moduleinst.𝖾𝗅𝖾𝗆𝗌, the element instance 𝑆.𝖾𝗅𝖾𝗆𝗌⁡[elemaddr𝑖] must be valid with some reference type reftype𝑖.

• Each export instance exportinst𝑖 in moduleinst.𝖾𝗑𝗉𝗈𝗋𝗍𝗌 must be valid.

• For each export instance exportinst𝑖 in moduleinst.𝖾𝗑𝗉𝗈𝗋𝗍𝗌, the name exportinst𝑖.𝗇𝖺𝗆𝖾 must be different from any other name occurring in moduleinst.𝖾𝗑𝗉𝗈𝗋𝗍𝗌.

• Let deftype∗ be the concatenation of all deftype𝑖 in order.

• Let tagtype∗ be the concatenation of all tagtype𝑖 in order.

• Let globaltype∗ be the concatenation of all globaltype𝑖 in order.

• Let memtype∗ be the concatenation of all memtype𝑖 in order.

• Let tabletype∗ be the concatenation of all tabletype𝑖 in order.

• Let deftype∗𝖥 be the concatenation of all deftype𝖥⁡𝑖 in order.

• Let reftype∗ be the concatenation of all reftype𝑖 in order.

• Let ok∗ be the concatenation of all ok𝑖 in order.

• Let 𝑚 be the length of moduleinst.𝖿𝗎𝗇𝖼𝗌.

• Let 𝑥∗ be the sequence of function indices from 0 to 𝑚 −1.

• Then the module instance is valid with context {𝗍𝗒𝗉𝖾𝗌 deftype∗, 𝗍𝖺𝗀𝗌 tagtype∗, 𝗀𝗅𝗈𝖻𝖺𝗅𝗌 globaltype∗, 𝗆𝖾𝗆𝗌 memtype∗, 𝗍𝖺𝖻𝗅𝖾𝗌 tabletype∗, 𝖿𝗎𝗇𝖼𝗌 deftype∗𝖥, 𝖽𝖺𝗍𝖺𝗌 ok∗, 𝖾𝗅𝖾𝗆𝗌 reftype∗, 𝗋𝖾𝖿𝗌 𝑥∗}.

 (⊢deftype:𝗈𝗄)∗(𝑆⊢𝗍𝖺𝗀 tagaddr:𝗍𝖺𝗀 tagtype)∗(𝑆⊢𝗀𝗅𝗈𝖻𝖺𝗅 globaladdr:𝗀𝗅𝗈𝖻𝖺𝗅 globaltype)∗(𝑆⊢𝖿𝗎𝗇𝖼 funcaddr:𝖿𝗎𝗇𝖼 deftype𝖥)∗(𝑆⊢𝗆𝖾𝗆 memaddr:𝗆𝖾𝗆 memtype)∗(𝑆⊢𝗍𝖺𝖻𝗅𝖾 tableaddr:𝗍𝖺𝖻𝗅𝖾 tabletype)∗(𝑆⊢𝑆.𝖽𝖺𝗍𝖺𝗌⁡[dataaddr]:ok)∗(𝑆⊢𝑆.𝖾𝗅𝖾𝗆𝗌⁡[elemaddr]:reftype)∗(𝑆⊢exportinst:𝗈𝗄)∗(exportinst.𝗇𝖺𝗆𝖾)∗ disjoint𝑆⊢{𝗍𝗒𝗉𝖾𝗌 deftype∗,𝗍𝖺𝗀𝗌 tagaddr∗,𝗀𝗅𝗈𝖻𝖺𝗅𝗌 globaladdr∗,𝗆𝖾𝗆𝗌 memaddr∗,𝗍𝖺𝖻𝗅𝖾𝗌 tableaddr∗,𝖿𝗎𝗇𝖼𝗌 funcaddr∗,𝖽𝖺𝗍𝖺𝗌 dataaddr∗,𝖾𝗅𝖾𝗆𝗌 elemaddr∗,𝖾𝗑𝗉𝗈𝗋𝗍𝗌 exportinst∗ }:{𝗍𝗒𝗉𝖾𝗌 deftype∗,𝗍𝖺𝗀𝗌 tagtype∗,𝗀𝗅𝗈𝖻𝖺𝗅𝗌 globaltype∗,𝗆𝖾𝗆𝗌 memtype∗,𝗍𝖺𝖻𝗅𝖾𝗌 tabletype∗,𝖿𝗎𝗇𝖼𝗌 deftype∗𝖥,𝖽𝖺𝗍𝖺𝗌 ok∗,𝖾𝗅𝖾𝗆𝗌 reftype∗,𝗋𝖾𝖿𝗌 0…(|funcaddr∗|−1) }

Configuration Validity

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

Configurations and threads are classified by their result type. In addition to the store 𝑆, 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 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 𝑆;𝑇

• The store 𝑆 must be valid.

• Under no allowed return type, the thread 𝑇 must be valid with some result type [𝑡∗].

• Then the configuration is valid with the result type [𝑡∗].

⊢𝑆:𝗈𝗄𝑆;𝜖⊢𝑇:[𝑡∗]⊢𝑆;𝑇:[𝑡∗]

Threads 𝐹;instr∗

• Let resulttype? be the current allowed return type.

• The frame 𝐹 must be valid with a context 𝐶.

• Let 𝐶′ be the same context as 𝐶, but with 𝗋𝖾𝗍𝗎𝗋𝗇 set to resulttype?.

• Under context 𝐶′, the instruction sequence instr∗ must be valid with some type [] →[𝑡∗].

• Then the thread is valid with the result type [𝑡∗].

𝑆⊢𝐹:𝐶𝑆;𝐶,𝗋𝖾𝗍𝗎𝗋𝗇 resulttype?⊢instr∗:[]→[𝑡∗]𝑆;resulttype?⊢𝐹;instr∗:[𝑡∗]

Frames {𝗅𝗈𝖼𝖺𝗅𝗌 val∗,𝗆𝗈𝖽𝗎𝗅𝖾 moduleinst}

• The module instance moduleinst must be valid with some module context 𝐶.

• Each value val𝑖 in val∗ must be valid with some value type 𝑡𝑖.

• Let 𝑡∗ be the concatenation of all 𝑡𝑖 in order.

• Let 𝐶′ be the same context as 𝐶, but with the value types 𝑡∗ prepended to the 𝗅𝗈𝖼𝖺𝗅𝗌 list.

• Then the frame is valid with frame context 𝐶′.

𝑆⊢moduleinst:𝐶(𝑆⊢val:𝑡)∗𝑆⊢{𝗅𝗈𝖼𝖺𝗅𝗌 val∗,𝗆𝗈𝖽𝗎𝗅𝖾 moduleinst}:(𝐶,𝗅𝗈𝖼𝖺𝗅𝗌 𝑡∗)

Administrative Instructions

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

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

𝗍𝗋𝖺𝗉

• The instruction is valid with any valid instruction type of the form [𝑡∗1] →[𝑡∗2].

𝐶⊢[𝑡∗1]→[𝑡∗2]:𝗈𝗄𝑆;𝐶⊢𝗍𝗋𝖺𝗉:[𝑡∗1]→[𝑡∗2]

val

• The value val must be valid with value type 𝑡.

• Then it is valid as an instruction with type [] →[𝑡].

𝑆⊢val:𝑡𝑆;𝐶⊢val:[]→[𝑡]

𝗂𝗇𝗏𝗈𝗄𝖾 funcaddr

• The external function address 𝖿𝗎𝗇𝖼 funcaddr must be valid with external function type 𝖿𝗎𝗇𝖼 deftype′.

• The expansion of the defined type deftype must be some function type 𝖿𝗎𝗇𝖼 [𝑡∗1] →[𝑡∗2]).

• Then the instruction is valid with type [𝑡∗1] →[𝑡∗2].

𝑆⊢𝖿𝗎𝗇𝖼 funcaddr:𝖿𝗎𝗇𝖼 deftypedeftype≈𝖿𝗎𝗇𝖼 [𝑡∗1]→[𝑡∗2]𝑆;𝐶⊢𝗂𝗇𝗏𝗈𝗄𝖾 funcaddr:[𝑡∗1]→[𝑡∗2]

𝗅𝖺𝖻𝖾𝗅𝑛⁢{instr∗0} instr∗

• The instruction sequence instr∗0 must be valid with some type [𝑡𝑛1] →𝑥∗[𝑡∗2].

• Let 𝐶′ be the same context as 𝐶, but with the result type [𝑡𝑛1] prepended to the 𝗅𝖺𝖻𝖾𝗅𝗌 list.

• Under context 𝐶′, the instruction sequence instr∗ must be valid with type [] →𝑥′∗[𝑡∗2].

• Then the compound instruction is valid with type [] →[𝑡∗2].

𝑆;𝐶⊢instr∗0:[𝑡𝑛1]→𝑥∗[𝑡∗2]𝑆;𝐶,𝗅𝖺𝖻𝖾𝗅𝗌⁡[𝑡𝑛1]⊢instr∗:[]→𝑥′∗[𝑡∗2]𝑆;𝐶⊢𝗅𝖺𝖻𝖾𝗅𝑛⁢{instr∗0} instr∗:[]→[𝑡∗2]

𝖿𝗋𝖺𝗆𝖾𝑛⁢{𝐹} instr∗

• Under the valid return type [𝑡𝑛], the thread 𝐹;instr∗ must be valid with result type [𝑡𝑛].

• Then the compound instruction is valid with type [] →[𝑡𝑛].

𝐶⊢[𝑡𝑛]:𝗈𝗄𝑆;[𝑡𝑛]⊢𝐹;instr∗:[𝑡𝑛]𝑆;𝐶⊢𝖿𝗋𝖺𝗆𝖾𝑛⁢{𝐹} instr∗:[]→[𝑡𝑛]

𝗁𝖺𝗇𝖽𝗅𝖾𝗋𝑛⁢{catch∗} instr∗

• For every catch clause catch𝑖 in catch∗, catch𝑖 must be valid.

• The instruction sequence instr∗ must be valid with some type [𝑡∗1] →[𝑡∗2].

• Then the compound instruction is valid with type [𝑡∗1] →[𝑡∗2].

(𝐶⊢catch:𝗈𝗄)∗𝑆;𝐶⊢instr∗:[𝑡∗1]→[𝑡∗2]𝑆;𝐶⊢𝗁𝖺𝗇𝖽𝗅𝖾𝗋𝑛⁢{catch∗} instr∗:[𝑡∗1]→[𝑡∗2]

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 𝑆′ extends state 𝑆, written 𝑆 ⪯𝑆′, when the following rules hold.

Note

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

Store 𝑆

• The length of 𝑆.𝗍𝖺𝗀𝗌 must not shrink.

• The length of 𝑆.𝗀𝗅𝗈𝖻𝖺𝗅𝗌 must not shrink.

• The length of 𝑆.𝗆𝖾𝗆𝗌 must not shrink.

• The length of 𝑆.𝗍𝖺𝖻𝗅𝖾𝗌 must not shrink.

• The length of 𝑆.𝖿𝗎𝗇𝖼𝗌 must not shrink.

• The length of 𝑆.𝖽𝖺𝗍𝖺𝗌 must not shrink.

• The length of 𝑆.𝖾𝗅𝖾𝗆𝗌 must not shrink.

• The length of 𝑆.𝗌𝗍𝗋𝗎𝖼𝗍𝗌 must not shrink.

• The length of 𝑆.𝖺𝗋𝗋𝖺𝗒𝗌 must not shrink.

• The length of 𝑆.𝖾𝗑𝗇𝗌 must not shrink.

• For each tag instance taginst𝑖 in the original 𝑆.𝗍𝖺𝗀𝗌, the new tag instance must be an extension of the old.

• For each global instance globalinst𝑖 in the original 𝑆.𝗀𝗅𝗈𝖻𝖺𝗅𝗌, the new global instance must be an extension of the old.

• For each memory instance meminst𝑖 in the original 𝑆.𝗆𝖾𝗆𝗌, the new memory instance must be an extension of the old.

• For each table instance tableinst𝑖 in the original 𝑆.𝗍𝖺𝖻𝗅𝖾𝗌, the new table instance must be an extension of the old.

• For each function instance funcinst𝑖 in the original 𝑆.𝖿𝗎𝗇𝖼𝗌, the new function instance must be an extension of the old.

• For each data instance datainst𝑖 in the original 𝑆.𝖽𝖺𝗍𝖺𝗌, the new data instance must be an extension of the old.

• For each element instance eleminst𝑖 in the original 𝑆.𝖾𝗅𝖾𝗆𝗌, the new element instance must be an extension of the old.

• For each structure instance structinst𝑖 in the original 𝑆.𝗌𝗍𝗋𝗎𝖼𝗍𝗌, the new structure instance must be an extension of the old.

• For each array instance arrayinst𝑖 in the original 𝑆.𝖺𝗋𝗋𝖺𝗒𝗌, the new array instance must be an extension of the old.

• For each exception instance exninst𝑖 in the original 𝑆.𝖾𝗑𝗇𝗌, the new exception instance must be an extension of the old.

𝑆1.𝗍𝖺𝗀𝗌=taginst∗1𝑆2.𝗍𝖺𝗀𝗌=taginst′1∗ taginst∗2(⊢taginst1⪯taginst′1)∗𝑆1.𝗀𝗅𝗈𝖻𝖺𝗅𝗌=globalinst∗1𝑆2.𝗀𝗅𝗈𝖻𝖺𝗅𝗌=globalinst′1∗ globalinst∗2(⊢globalinst1⪯globalinst′1)∗𝑆1.𝗆𝖾𝗆𝗌=meminst∗1𝑆2.𝗆𝖾𝗆𝗌=meminst′1∗ meminst∗2(⊢meminst1⪯meminst′1)∗𝑆1.𝗍𝖺𝖻𝗅𝖾𝗌=tableinst∗1𝑆2.𝗍𝖺𝖻𝗅𝖾𝗌=tableinst′1∗ tableinst∗2(⊢tableinst1⪯tableinst′1)∗𝑆1.𝖿𝗎𝗇𝖼𝗌=funcinst∗1𝑆2.𝖿𝗎𝗇𝖼𝗌=funcinst′1∗ funcinst∗2(⊢funcinst1⪯funcinst′1)∗𝑆1.𝖽𝖺𝗍𝖺𝗌=datainst∗1𝑆2.𝖽𝖺𝗍𝖺𝗌=datainst′1∗ datainst∗2(⊢datainst1⪯datainst′1)∗𝑆1.𝖾𝗅𝖾𝗆𝗌=eleminst∗1𝑆2.𝖾𝗅𝖾𝗆𝗌=eleminst′1∗ eleminst∗2(⊢eleminst1⪯eleminst′1)∗𝑆1.𝗌𝗍𝗋𝗎𝖼𝗍𝗌=structinst∗1𝑆2.𝗌𝗍𝗋𝗎𝖼𝗍𝗌=structinst′1∗ structinst∗2(⊢structinst1⪯structinst′1)∗𝑆1.𝖺𝗋𝗋𝖺𝗒𝗌=arrayinst∗1𝑆2.𝖺𝗋𝗋𝖺𝗒𝗌=arrayinst′1∗ arrayinst∗2(⊢arrayinst1⪯arrayinst′1)∗𝑆1.𝖾𝗑𝗇𝗌=exninst∗1𝑆2.𝖾𝗑𝗇𝗌=exninst′1∗ exninst∗2(⊢exninst1⪯exninst′1)∗⊢𝑆1⪯𝑆2

Tag Instance taginst

• A tag instance must remain unchanged.

⊢taginst⪯taginst

Global Instance globalinst

• The global type globalinst.𝗍𝗒𝗉𝖾 must remain unchanged.

• Let mut 𝑡 be the structure of globalinst.𝗍𝗒𝗉𝖾.

• If mut is empty, then the value globalinst.𝗏𝖺𝗅𝗎𝖾 must remain unchanged.

mut=𝗆𝗎𝗍∨val1=val2⊢{𝗍𝗒𝗉𝖾 (mut 𝑡),𝗏𝖺𝗅𝗎𝖾 val1}⪯{𝗍𝗒𝗉𝖾 (mut 𝑡),𝗏𝖺𝗅𝗎𝖾 val2}

Memory Instance meminst

• The memory type meminst.𝗍𝗒𝗉𝖾 must remain unchanged.

• The length of meminst.𝖻𝗒𝗍𝖾𝗌 must not shrink.

𝑛1≤𝑛2⊢{𝗍𝗒𝗉𝖾 mt,𝖻𝗒𝗍𝖾𝗌 𝑏𝑛11}⪯{𝗍𝗒𝗉𝖾 mt,𝖻𝗒𝗍𝖾𝗌 𝑏𝑛22}

Table Instance tableinst

• The table type tableinst.𝗍𝗒𝗉𝖾 must remain unchanged.

• The length of tableinst.𝖾𝗅𝖾𝗆 must not shrink.

𝑛1≤𝑛2⊢{𝗍𝗒𝗉𝖾 tt,𝖾𝗅𝖾𝗆 (fa?1)𝑛1}⪯{𝗍𝗒𝗉𝖾 tt,𝖾𝗅𝖾𝗆 (fa?2)𝑛2}

Function Instance funcinst

• A function instance must remain unchanged.

⊢funcinst⪯funcinst

Data Instance datainst

• The list datainst.𝖻𝗒𝗍𝖾𝗌 must:

  • either remain unchanged,

  • or shrink to length 0.

⊢{𝖻𝗒𝗍𝖾𝗌 𝑏∗}⪯{𝖻𝗒𝗍𝖾𝗌 𝑏∗}

⊢{𝖻𝗒𝗍𝖾𝗌 𝑏∗}⪯{𝖻𝗒𝗍𝖾𝗌 𝜖}

Element Instance eleminst

• The reference type eleminst.𝗍𝗒𝗉𝖾 must remain unchanged.

• The list eleminst.𝖾𝗅𝖾𝗆 must:

  • either remain unchanged,

  • or shrink to length 0.

⊢{𝗍𝗒𝗉𝖾 𝑡,𝖾𝗅𝖾𝗆 𝑎∗}⪯{𝗍𝗒𝗉𝖾 𝑡,𝖾𝗅𝖾𝗆 𝑎∗}

⊢{𝗍𝗒𝗉𝖾 𝑡,𝖾𝗅𝖾𝗆 𝑎∗}⪯{𝗍𝗒𝗉𝖾 𝑡,𝖾𝗅𝖾𝗆 𝜖}

Structure Instance structinst

• The defined type structinst.𝗍𝗒𝗉𝖾 must remain unchanged.

• Assert: due to store well-formedness, the expansion of structinst.𝗍𝗒𝗉𝖾 is a structure type.

• Let 𝗌𝗍𝗋𝗎𝖼𝗍 fieldtype∗ be the expansion of structinst.𝗍𝗒𝗉𝖾.

• The length of the list structinst.𝖿𝗂𝖾𝗅𝖽𝗌 must remain unchanged.

• Assert: due to store well-formedness, the length of structinst.𝖿𝗂𝖾𝗅𝖽𝗌 is the same as the length of fieldtype∗.

• For each field value fieldval𝑖 in structinst.𝖿𝗂𝖾𝗅𝖽𝗌 and corresponding field type fieldtype𝑖 in fieldtype∗:

  • Let mut𝑖 st𝑖 be the structure of fieldtype𝑖.

  • If mut𝑖 is empty, then the field value fieldval𝑖 must remain unchanged.

(mut=𝗆𝗎𝗍∨fieldval1=fieldval2)∗⊢{𝗍𝗒𝗉𝖾 (mut st)∗,𝖿𝗂𝖾𝗅𝖽𝗌 fieldval∗1}⪯{𝗍𝗒𝗉𝖾 (mut st)∗,𝖿𝗂𝖾𝗅𝖽𝗌 fieldval∗2}

Array Instance arrayinst

• The defined type arrayinst.𝗍𝗒𝗉𝖾 must remain unchanged.

• Assert: due to store well-formedness, the expansion of arrayinst.𝗍𝗒𝗉𝖾 is an array type.

• Let 𝖺𝗋𝗋𝖺𝗒 fieldtype be the expansion of arrayinst.𝗍𝗒𝗉𝖾.

• The length of the list arrayinst.𝖿𝗂𝖾𝗅𝖽𝗌 must remain unchanged.

• Let mut st be the structure of fieldtype.

• If mut is empty, then the sequence of field values arrayinst.𝖿𝗂𝖾𝗅𝖽𝗌 must remain unchanged.

mut=𝗆𝗎𝗍∨fieldval∗1=fieldval∗2⊢{𝗍𝗒𝗉𝖾 (mut st),𝖿𝗂𝖾𝗅𝖽𝗌 fieldval∗1}⪯{𝗍𝗒𝗉𝖾 (mut st),𝖿𝗂𝖾𝗅𝖽𝗌 fieldval∗2}

Exception Instance exninst

• An exception instance must remain unchanged.

⊢exninst⪯exninst

Theorems

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

Theorem (Preservation). If a configuration 𝑆;𝑇 is valid with result type [𝑡∗] (i.e., ⊢𝑆;𝑇 :[𝑡∗]), and steps to 𝑆′;𝑇′ (i.e., 𝑆;𝑇 ↪𝑆′;𝑇′), then 𝑆′;𝑇′ is a valid configuration with the same result type (i.e., ⊢𝑆′;𝑇′ :[𝑡∗]). Furthermore, 𝑆′ is an extension of 𝑆 (i.e., ⊢𝑆 ⪯𝑆′).

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 𝑆;𝑇 is valid (i.e., ⊢𝑆;𝑇 :[𝑡∗] for some result type [𝑡∗]), then either it is terminal, or it can step to some configuration 𝑆′;𝑇′ (i.e., 𝑆;𝑇 ↪𝑆′;𝑇′).

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

Corollary (Soundness). If a configuration 𝑆;𝑇 is valid (i.e., ⊢𝑆;𝑇 :[𝑡∗] for some result type [𝑡∗]), then it either diverges or takes a finite number of steps to reach a terminal configuration 𝑆′;𝑇′ (i.e., 𝑆;𝑇 ↪∗𝑆′;𝑇′) that is valid with the same result type (i.e., ⊢𝑆′;𝑇′ :[𝑡∗]) and where 𝑆′ is an extension of 𝑆 (i.e., ⊢𝑆 ⪯𝑆′).

In other words, every thread in a valid configuration either runs forever, traps, throws an exception, 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 𝗋𝖾𝖿.𝖺𝗌_𝗇𝗈𝗇_𝗇𝗎𝗅𝗅 has the type [(𝗋𝖾𝖿 𝗇𝗎𝗅𝗅 ht)] →[(𝗋𝖾𝖿 ht)] for any choice of valid heap type ht. Moreover, if the input type [(𝗋𝖾𝖿 𝗇𝗎𝗅𝗅 ht)] is already determined, i.e., a specific ht is given, then the output type [(𝗋𝖾𝖿 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:

null::=𝗇𝗎𝗅𝗅? | 𝛼nullheaptype::=… | 𝛼heaptypereftype::=𝗋𝖾𝖿 null heaptypevaltype::=… | 𝛼valtype | 𝛼numvectyperesulttype::=[𝛼?valtype∗ valtype∗]

where each 𝛼xyz ranges over a set of type variables for syntactic class xyz, respectively. The special class numvectype is defined as numtype | vectype | 𝖻𝗈𝗍, and is only needed to handle unannotated 𝗌𝖾𝗅𝖾𝖼𝗍 instructions.

A type is closed when it does not contain any type variables, and open otherwise. A type substitution 𝜎 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 𝛼 from its domain with the respective 𝜎⁡(𝛼).

Theorem (Principal Types). If an instruction sequence instr∗ is valid with some closed instruction type instrtype (i.e., 𝐶 ⊢instr∗ :instrtype), then it is also valid with a possibly open instruction type instrtypemin (i.e., 𝐶 ⊢instr∗ :instrtypemin), such that for every closed type instrtype′ with which instr∗ is valid (i.e., for all 𝐶 ⊢instr∗ :instrtype′), there exists a substitution 𝜎, such that 𝜎⁡(instrtypemin) is a subtype of instrtype′ (i.e., 𝐶 ⊢𝜎⁡(instrtypemin) ≤instrtype′). Furthermore, instrtypemin is unique up to the choice of type variables.

Theorem (Closed Principal Forward Types). If closed input type [𝑡∗1] is given and the instruction sequence instr∗ is valid with instruction type [𝑡∗1] →𝑥∗[𝑡∗2] (i.e., 𝐶 ⊢instr∗ :[𝑡∗1] →𝑥∗[𝑡∗2]), then it is also valid with instruction type [𝑡∗1] →𝑥∗[𝛼valtype∗ 𝑡∗] (i.e., 𝐶 ⊢instr∗ :[𝑡∗1] →𝑥∗[𝛼valtype∗ 𝑡∗]), where all 𝑡∗ are closed, such that for every closed result type [𝑡′2∗] with which instr∗ is valid (i.e., for all 𝐶 ⊢instr∗ :[𝑡∗1] →𝑥∗[𝑡′2∗]), there exists a substitution 𝜎, such that [𝑡′2∗] =[𝜎⁡(𝛼valtype∗) 𝑡∗].

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 𝑡1 and 𝑡2 that are valid (i.e., 𝐶 ⊢𝑡1 :𝗈𝗄 and 𝐶 ⊢𝑡2 :𝗈𝗄), there exists a valid value type 𝑡 that is a subtype of both 𝑡1 and 𝑡2 (i.e., 𝐶 ⊢𝑡 :𝗈𝗄 and 𝐶 ⊢𝑡 ≤𝑡1 and 𝐶 ⊢𝑡 ≤𝑡2), such that every valid value type 𝑡′ that also is a subtype of both 𝑡1 and 𝑡2 (i.e., for all 𝐶 ⊢𝑡′ :𝗈𝗄 and 𝐶 ⊢𝑡′ ≤𝑡1 and 𝐶 ⊢𝑡′ ≤𝑡2), is a subtype of 𝑡 (i.e., 𝐶 ⊢𝑡′ ≤𝑡).

Note

The greatest lower bound of two types may be 𝖻𝗈𝗍.

Theorem (Conditional Least Upper Bounds for Value Types). Any two value types 𝑡1 and 𝑡2 that are valid (i.e., 𝐶 ⊢𝑡1 :𝗈𝗄 and 𝐶 ⊢𝑡2 :𝗈𝗄) either have no common supertype, or there exists a valid value type 𝑡 that is a supertype of both 𝑡1 and 𝑡2 (i.e., 𝐶 ⊢𝑡 :𝗈𝗄 and 𝐶 ⊢𝑡1 ≤𝑡 and 𝐶 ⊢𝑡2 ≤𝑡), such that every valid value type 𝑡′ that also is a supertype of both 𝑡1 and 𝑡2 (i.e., for all 𝐶 ⊢𝑡′ :𝗈𝗄 and 𝐶 ⊢𝑡1 ≤𝑡′ and 𝐶 ⊢𝑡2 ≤𝑡′), is a supertype of 𝑡 (i.e., 𝐶 ⊢𝑡 ≤𝑡′).

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 𝖻𝗈𝗍.

Theorem (Disjoint Subtype Hierarchies). The greatest lower bound of two value types is 𝖻𝗈𝗍 or 𝗋𝖾𝖿 𝖻𝗈𝗍 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 𝖻𝗈𝗍 or 𝗋𝖾𝖿 𝖻𝗈𝗍), 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 instr∗1 and instr∗2 are valid with types [𝑡∗1] →𝑥∗1[𝑡∗] and [𝑡∗] →𝑥∗2[𝑡∗2], respectively (i.e., 𝐶 ⊢instr∗1 :[𝑡∗1] →𝑥∗1[𝑡∗] and 𝐶 ⊢instr∗1 :[𝑡∗] →𝑥∗2[𝑡∗2]), then the concatenated instruction sequence (instr∗1 instr∗2) is valid with type [𝑡∗1] →𝑥∗1𝑥∗2[𝑡∗2] (i.e., 𝐶 ⊢instr∗1 instr∗2 :[𝑡∗1] →𝑥∗1𝑥∗2[𝑡∗2]).

Note

More generally, instead of a shared type [𝑡∗], it suffices if the output type of instr∗1 is a subtype of the input type of instr∗1, 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 instr∗ that is valid with type [𝑡∗1] →𝑥∗[𝑡∗2] (i.e., 𝐶 ⊢instr∗ :[𝑡∗1] →𝑥∗[𝑡∗2]) is split into two instruction sequences instr∗1 and instr∗2 at any point (i.e., instr∗ =instr∗1 instr∗2), then these are separately valid with some types [𝑡∗1] →𝑥∗1[𝑡∗] and [𝑡∗] →𝑥∗2[𝑡∗2], respectively (i.e., 𝐶 ⊢instr∗1 :[𝑡∗1] →𝑥∗1[𝑡∗] and 𝐶 ⊢instr∗1 :[𝑡∗] →𝑥∗2[𝑡∗2]), where 𝑥∗ =𝑥∗1 𝑥∗2.

Note

This property holds because validation is required even for unreachable code. Without that, instr∗2 might not be valid in isolation.