Modules¶
Modules are valid when all the components they contain are valid. Furthermore, most definitions are themselves classified with a suitable type.
Types¶
The sequence of types defined in a module is validated incrementally, yielding a sequence of defined types representing them individually.
¶
The type definition
is equal to . The defined type sequence
is equal to . Let
be the same context as , but with the defined type sequence appended to the field . Under the context
, the recursive type is valid with .
¶
The type definition sequence
Either:
The type definition sequence
is equal to . The defined type sequence
is equal to . Or:
The type definition sequence
is equal to . The defined type sequence
is equal to . The type definition
is valid with the defined type sequence . Let
be the same context as , but with the defined type sequence appended to the field . Under the context
, the type definition sequence is valid with the defined type sequence .
Todo
below is the official specification
If the sequence is empty, then:
The context
must be empty.Then the type sequence is valid.
Otherwise:
Let the recursive type
be the last element in the sequence.The sequence without
must be valid for some context .Let the type index
be the length of , i.e., the first type index free in .Let the sequence of defined types
be the result of rolling up into its sequence of defined types.The recursive type
must be valid under the context for type index .The current context
be the same as , but with appended to .Then the type sequence is valid.
Functions¶
Functions
¶
The function
The defined type
exists. The expansion of the defined type
is the composite type .
is equal to . For all
in and in :
The local
is valid with the local type . Under the context
, the expression is valid with the result type .
Todo
below is the official specification
The defined type
must be a function type.Let
be the expansion of the defined type .For each local declared by a value type
in :The local for type
must be valid with local type .
Let
be the concatenation of all .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
.
Locals¶
Locals
¶
The local
Either:
The initialization status
is equal to . A default value for value type the value type
is defined. Or:
The initialization status
is equal to . A default value for value type the value type
is not defined.
Todo
below is the official specification
The value type
must be valid.If
is defaultable, then:The local is valid with local type
.
Else:
The local is valid with local type
.
Note
For cases where both rules are applicable, the former yields the more permissable type.
Tables¶
Tables
¶
The table
The table type
is valid. The table type
is equal to . The expression
is valid with the value type .
is const.
Todo
below is the official specification
The table type
must be valid.Let
be the element reference type of .The expression
must be valid with result type .The expression
must be constant.Then the table definition is valid with type
.
Memories¶
Memories
¶
The memory
The memory type
is valid.
Todo
below is the official specification
The memory type
must be valid.Then the memory definition is valid with type
.
Globals¶
Globals
Sequences of globals are handled incrementally, such that each definition has access to previous definitions.
¶
The global
The global type
is valid. The global type
is equal to . The expression
is valid with the value type .
is const.
Todo
below is the official specification
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
.
¶
The global sequence
Either:
The global sequence
is equal to . The global type sequence
is equal to . Or:
The global sequence
is equal to . The global type sequence
is equal to . The global
is valid with the global type . Let
be the same context as , but with the global type appended to the field . Under the context
, the global sequence is valid with the global type sequence .
Todo
below is the official specification
If the sequence is empty, then it is valid with the empty sequence of global types.
Else:
The first global definition must be valid with some type global type
.Let
be the same context as , but with the global type apppended to the list.Under context
, the remainder of the sequence must be valid with some sequence of global types.Then the sequence is valid with the sequence of global types consisting of
prepended to .
Element Segments¶
Element segments
¶
The table segment
The element type
is valid. For all
in :
The expression
is valid with the element type .
is const. The element mode
is valid with the element type .
Todo
below is the official specification
The reference type
must be valid.For each
in :The expression
must be valid with some result type .The expression
must be constant.
The element mode
must be valid with some reference type .The reference type
must match the reference type .Then the element segment is valid with reference type
.
The element mode
Either:
The element mode
is equal to . The table type
exists. The table type
is equal to . The element type
matches the reference type . The expression
is valid with the value type .
is const. Or:
The element mode
is equal to . Or:
The element mode
is equal to .
Todo
below is the official specification
¶
The element mode is valid with any valid 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 valid reference type.
Data Segments¶
Data segments
¶
The memory segment
The data mode
is valid with the data type .
Todo
below is the official specification
The data mode
must be valid.Then the data segment is valid.
The data mode
Either:
The data mode
is equal to . The memory type
exists. The memory type
is equal to . The expression
is valid with the value type .
is const. Or:
The data mode
is equal to .
Todo
below is the official specification
¶
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 start function
The defined type
exists. The expansion of the defined type
is the composite type .
Todo
below is the official specification
The function
must be defined in the context.The expansion of
must be a function type .Then the start function is valid.
Exports¶
Exports
¶
The export
The external index
is valid with the external type .
Todo
below is the official specification
The export description
must be valid with external type .Then the export is valid with external type
.
¶
The external index
The defined type
exists. The defined type
is equal to .
Todo
below is the official specification
The function
must be defined in the context.Let
be the defined type .Then the export description is valid with external type
.
¶
The external index
The table type
exists. The table type
is equal to .
Todo
below is the official specification
The table
must be defined in the context.Then the export description is valid with external type
.
¶
The external index
The memory type
exists. The memory type
is equal to .
Todo
below is the official specification
The memory
must be defined in the context.Then the export description is valid with external type
.
¶
The external index
The global type
exists. The global type
is equal to .
Todo
below is the official specification
The global
must be defined in the context.Then the export description is valid with external type
.
¶
The tag
must be defined in the context.Then the export description is valid with external type
.
Imports¶
Imports
¶
The import
The external type
is valid.
Todo
below is the official specification
The import description
must be valid with type .Then the import 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
The external types classifying a module may contain free type indices that refer to types defined within the module.
The module
Under the context
, the type definition sequence is valid with the defined type sequence .
is equal to . For all
in and in :
Under the context
, the import is valid with the external type . Under the context
, the global sequence is valid with the global type sequence .
is equal to . For all
in and in :
Under the context
, the table is valid with the table type .
is equal to . For all
in and in :
Under the context
, the memory is valid with the memory type .
is equal to . For all
in and in :
Under the context
, the tag is valid with the tag type .
is equal to . For all
in and in :
The function
is valid with the defined type .
is equal to . For all
in and in :
The table segment
is valid with the element type .
is equal to . For all
in and in :
The memory segment
is valid with the data type . If
is defined, then:
The start function
is valid.
is equal to .
is equal to . For all
in and in and in :
The export
is valid with the name and the external type .
is equal to true. The context
is equal to . The context
is equal to . The function index sequence
is equal to . The defined type sequence
is equal to . The global type sequence
is equal to . The table type sequence
is equal to . The memory type sequence
is equal to . The tag type sequence
is equal to . Let
be the module type .
Todo
below is the official specification
Let
be the module to validate.Let
be a context where: is , is concatenated with , with the import’s external types and the internal defined 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 concatenated with , with the import’s external types and the internal tag types as determined below, is as determined below, is as determined below, 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 , is the same as , is the same as , is the same as ,all other fields are empty.
Under the context
:The sequence
of globals must be valid with a sequence of global types.For each
in , the definition must be valid with a table type .For each
in , the definition must be valid with a memory type .
Under the context
:For each
in , the definition must be valid with a defined type .For each
in , the definition must be valid with a tag type .For each
in , the segment must be valid with reference 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 .
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 internal tag types , in index order.Let
be the concatenation of the reference types , in index order.Let
be the concatenation of the data 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.The length of
must not be larger than .All export names
must be different.Then the module is valid with external types
.
Todo
Check refs; check export names
Note
All functions in a module are mutually recursive.
Consequently, the definition of the context
Globals, however, are not recursive but evaluated sequentially, such that each constant expressions only has access to imported or previously defined globals.