Modules¶
Modules are valid when all the components they contain are valid. Furthermore, most definitions are themselves classified with a suitable type.
Functions¶
Functions
¶
The type
must be defined in the context.Let
be the function type .Let
be the same context as , but with: set to the sequence of value types , concatenating parameters and locals, set to the singular sequence containing only result type . set to the result type .
Under the context
, the expression must be valid with type .Then the function definition is valid with type
.
Tables¶
Tables
¶
The table type
must be valid.Then the table definition is valid with type
.
Memories¶
Memories
¶
The memory type
must be valid.Then the memory definition is valid with type
.
Globals¶
Globals
¶
The global type
must be valid.The expression
must be valid with result type .The expression
must be constant.Then the global definition is valid with type
.
Element Segments¶
Element segments
¶
For each
in :The expression
must be valid with some result type .The expression
must be constant.
The element mode
must be valid with reference type .Then the element segment is valid with reference type
.
¶
The element mode is valid with any reference type.
¶
The table
must be defined in the context.Let
be the table type .The expression
must be valid with result type .The expression
must be constant.Then the element mode is valid with reference type
.
¶
The element mode is valid with any reference type.
Data Segments¶
Data segments
¶
The data mode
must be valid.Then the data segment is valid.
¶
The data mode is valid.
¶
The memory
must be defined in the context.The expression
must be valid with result type .The expression
must be constant.Then the data mode is valid.
Start Function¶
Start function declarations
¶
The function
must be defined in the context.The type of
must be .Then the start function is valid.
Exports¶
Exports
¶
The export description
must be valid with external type .Then the export is valid with external type
.
¶
The function
must be defined in the context.Then the export description is valid with external type
.
¶
The table
must be defined in the context.Then the export description is valid with external type
.
¶
The memory
must be defined in the context.Then the export description is valid with external type
.
¶
The global
must be defined in the context.Then the export description is valid with external type
.
Imports¶
Imports
¶
The import description
must be valid with type .Then the import is valid with type
.
¶
The function
must be defined in the context.Let
be the function type .Then the import description is valid with type
.
¶
The table type
must be valid.Then the import description is valid with type
.
¶
The memory type
must be valid.Then the import description is valid with type
.
¶
The global type
must be valid.Then the import description is valid with type
.
Modules¶
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
Let
be the module to validate.Let
be a context where: is , is concatenated with , with the import’s external types and the internal function types as determined below, is concatenated with , with the import’s external types and the internal table types as determined below, is concatenated with , with the import’s external types and the internal memory types as determined below, is concatenated with , with the import’s external types and the internal global types as determined below, is as determined below, is , where is the length of the vector , is empty, is empty, is empty. is the set , i.e., the set of function indices occurring in the module, except in its functions or start function.
Let
be the context where: is the sequence , is the same as , is the same as ,all other fields are empty.
For each
in , the function type must be valid.Under the context
:For each
in , the definition must be valid with a function type .If
is non-empty, then must be valid.For each
in , the segment must be valid with an external type .For each
in , the segment must be valid with external type .
Under the context
:For each
in , the definition must be valid with a table type .For each
in , the definition must be valid with a memory type .For each
in , the definition must be valid with a global type .For each
in , the segment must be valid with reference type .For each
in , the segment must be valid.
The length of
must not be larger than .All export names
must be different.Let
be the concatenation of the internal function types , in index order.Let
be the concatenation of the internal table types , in index order.Let
be the concatenation of the internal memory types , in index order.Let
be the concatenation of the internal global types , in index order.Let
be the concatenation of the reference types , in index order.Let
be the concatenation of external types of the imports, in index order.Let
be the concatenation of external types of the exports, in index order.Then the module is valid with external types
.
Note
Most definitions in a module – particularly functions – are mutually recursive.
Consequently, the definition of the context
Globals, however, are not recursive and not accessible within constant expressions when they are defined locally.
The effect of defining the limited context
Note
The restriction on the number of memories may be lifted in future versions of WebAssembly.