Kwasm.validation.module

Validator of DataSegment nodes.

From the docs:

• The memory C.mems[x] must be defined in the context.
• The expression expr must be valid with result type [i32].
• The expression expr must be constant.
• Then the data segment is valid.

Validator of ElementSegment nodes.

From the docs:

• The table C.tables[x] must be defined in the context.
• Let limits elemtype be the table type C.tables[x].
• The element type elemtype must be funcref.
• The expression expr must be valid with result type [i32].
• The expression expr must be constant.
• For each y_i in y*, the function C.funcs[y] must be defined in the context.
• Then the element segment is valid.

Validator of Export nodes.

From the docs:

• The export description exportdesc must be valid with external type externtype.
• Then the export is valid with external type externtype.

Validator of ExportDescriptor nodes.

From the docs:

func x

• The function C.funcs[x] must be defined in the context.
• Then the export description is valid with external type func C.funcs[x].

table x

• The table C.tables[x] must be defined in the context.
• Then the export description is valid with external type table C.tables[x].

mem x

• The memory C.mems[x] must be defined in the context.
• Then the export description is valid with external type mem C.mems[x].

global x

• The global C.globals\[x] must be defined in the context.
• Then the export description is valid with external type global C.globals\[x].

Validator of Global nodes.

From the docs:

• The global type mut t must be valid.
• The expression expr must be valid with result type [t].
• The expression expr must be constant.
• Then the global definition is valid with type mut t.

Validator of Import nodes.

From the docs:

• The import description importdesc must be valid with type externtype.
• Then the import is valid with type externtype.

Validator of ImportDescriptor nodes.

From the docs:

func x

• The function C.types[x] must be defined in the context.
• Let [t*^1] => [t*^2] be the function type C.types[x].
• Then the import description is valid with type func [t*^1] => [t*^2].

table tabletype

• The table type tabletype must be valid.
• Then the import description is valid with type table tabletype.

mem memtype

• The memory type memtype must be valid.
• Then the import description is valid with type mem memtype.

global globaltype

• The global type globaltype must be valid.
• Then the import description is valid with type global globaltype.

Validator of Memory nodes.

From the docs:

• The memory type memtype must be valid.
• Then the memory definition is valid with type memtype.

Validator of WasmModules.

From the docs:

Modules are classified by their mapping from the external types of their imports to those of their exports.

A module is entirely closed, that is, its components can only refer to definitions that appear in the module itself. Consequently, no initial context is required. Instead, the context C for validation of the module’s content is constructed from the definitions in the module.

KWasm Note: The validation context will be passed to the ModuleValidator

• Let module be the module to validate.

• Let C be a context where:

  • C.types is module.types,
  • C.funcs is funcs(it*) concatenated with ft*, with the import’s external types it* and the internal function types ft* as determined below,
  • C.tables is tables(it*) concatenated with tt*, with the import’s external types it* and the internal table types tt* as determined below,
  • C.mems is mems(it*) concatenated with mt*, with the import’s external types it* and the internal memory types mt* as determined below,
  • C.globals is globals(it*) concatenated with gt*, with the import’s external types it* and the internal global types gt* as determined below,
  • C.locals is empty,
  • C.labels is empty,
  • C.return is empty.
• Let C′ be the context where C′.globals is the sequence globals(it*) and all other fields are empty.
• Under the context C:
• For each functype_i in module.types, the function type functype_i must be valid.
• For each func_i in module.funcs, the definition func_i must be valid with a function type ft_i.
• For each table_i in module.tables, the definition table_i must be valid with a table type tt_i.
• For each mem_i in module.mems, the definition mem_i must be valid with a memory type mt_i.
• For each global_i in module.globals: Under the context C′, the definition global_i must be valid with a global type gt_i.
• For each elem_i in module.elem, the segment elem_i must be valid.
• For each data_i in module.data, the segment data_i must be valid.
• If module.start is non-empty, then module.start must be valid.
• For each import_i in module.imports, the segment import_i must be valid with an external type it_i.
• For each export_i in module.exports, the segment export_i must be valid with external type et_i.
• The length of C.tables must not be larger than 1.
• The length of C.mems must not be larger than 1.
• All export names export_i.name must be different.
• Let ft* be the concatenation of the internal function types ft_i, in index order.
• Let tt* be the concatenation of the internal table types tt_i, in index order.
• Let mt* be the concatenation of the internal memory types mt_i, in index order.
• Let gt* be the concatenation of the internal global types gt_i, in index order.
• Let it* be the concatenation of external types it_i of the imports, in index order.
• Let et* be the concatenation of external types et_i of the exports, in index order.
• Then the module is valid with external types it* => et*.

Validator of StartFunction nodes.

From the docs:

• The function C.funcs[x] must be defined in the context.
• The type of C.funcs[x] must be [] => [].
• Then the start function is valid.

Validator of Table nodes.

From the docs:

• The table type tabletype must be valid.
• Then the table definition is valid with type tabletype.

Validator of WasmFunction nodes.

From the docs:

• The type C.types[x] must be defined in the context.
• Let [t*^1] => [t?^2] be the function type C.types[x].

• Let C′ be the same context as C, but with:

  • locals set to the sequence of value types t*^1 t*, concatenating parameters and locals,
  • labels set to the singular sequence containing only result type [t?^2].
  • return set to the result type [t?^2].
• Under the context C′, the expression expr must be valid with type t?^2.
• Then the function definition is valid with type [t*^1] => [t?^2].