ModuleValidator

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*.