Modules

Modules are valid when all the components they contain are valid. Furthermore, most definitions are themselves classified with a suitable type.

Functions

Functions func are classified by function types of the form [t1][t2].

{type x,locals t,body expr}

  • The type C.types[x] must be defined in the context.

  • Let [t1][t2] 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 t1 t, concatenating parameters and locals,

    • labels set to the singular sequence containing only result type [t2].

    • return set to the result type [t2].

  • Under the context C, the expression expr must be valid with type [t2].

  • Then the function definition is valid with type [t1][t2].

C.types[x]=[t1][t2]C,localst1 t,labels [t2],return [t2]expr:[t2]C{type x,locals t,body expr}:[t1][t2]

Tables

Tables table are classified by table types.

{type tabletype}

  • The table type tabletype must be valid.

  • Then the table definition is valid with type tabletype.

tabletypeokC{type tabletype}:tabletype

Memories

Memories mem are classified by memory types.

{type memtype}

  • The memory type memtype must be valid.

  • Then the memory definition is valid with type memtype.

memtypeokC{type memtype}:memtype

Globals

Globals global are classified by global types of the form mut t.

{type mut t,init expr}

mut tokCexpr:[t]CexprconstC{type mut t,init expr}:mut t

Element Segments

Element segments elem are classified by the reference type of their elements.

{type t,init e,mode elemmode}

(Ce:[t])(Ceconst)Celemmode:tC{type t,init e,mode elemmode}:t

passive

Cpassive:reftype

active {table x,offset expr}

  • The table C.tables[x] must be defined in the context.

  • Let limits t be the table type C.tables[x].

  • The expression expr must be valid with result type [i32].

  • The expression expr must be constant.

  • Then the element mode is valid with reference type t.

C.tables[x]=limits tCexpr:[i32]CexprconstCactive {table x,offset expr}:t

declarative

Cdeclarative:reftype

Data Segments

Data segments data are not classified by any type but merely checked for well-formedness.

{init b,mode datamode}

  • The data mode datamode must be valid.

  • Then the data segment is valid.

CdatamodeokC{init b,mode datamode}ok

passive

  • The data mode is valid.

Cpassiveok

active {memory x,offset expr}

  • 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 mode is valid.

C.mems[x]=limitsCexpr:[i32]CexprconstCactive {memory x,offset expr}ok

Start Function

Start function declarations start are not classified by any type.

{func x}

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

C.funcs[x]=[][]C{func x}ok

Exports

Exports export and export descriptions exportdesc are classified by their external type.

{name name,desc exportdesc}

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

  • Then the export is valid with external type externtype.

Cexportdesc:externtypeC{name name,desc exportdesc}:externtype

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

C.funcs[x]=functypeCfunc x:func functype

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

C.tables[x]=tabletypeCtable x:table tabletype

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

C.mems[x]=memtypeCmem x:mem memtype

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

C.globals[x]=globaltypeCglobal x:global globaltype

Imports

Imports import and import descriptions importdesc are classified by external types.

{module name1,name name2,desc importdesc}

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

  • Then the import is valid with type externtype.

Cimportdesc:externtypeC{module name1,name name2,desc importdesc}:externtype

func x

  • The function C.types[x] must be defined in the context.

  • Let [t1][t2] be the function type C.types[x].

  • Then the import description is valid with type func [t1][t2].

C.types[x]=[t1][t2]Cfunc x:func [t1][t2]

table tabletype

  • The table type tabletype must be valid.

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

tabletypeokCtable tabletype:table tabletype

mem memtype

  • The memory type memtype must be valid.

  • Then the import description is valid with type mem memtype.

memtypeokCmem memtype:mem memtype

global globaltype

  • The global type globaltype must be valid.

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

globaltypeokCglobal globaltype:global globaltype

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 C for validation of the module’s content is constructed from the definitions in the module.

  • 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.elems is rt as determined below,

    • C.datas is okn, where n is the length of the vector module.datas,

    • C.locals is empty,

    • C.labels is empty,

    • C.return is empty.

    • C.refs is the set funcidx(modulewithfuncs=ϵwithstart=ϵ), i.e., the set of function indices occurring in the module, except in its functions or start function.

  • Let C be the context where:

    • C.globals is the sequence globals(it),

    • C.funcs is the same as C.funcs,

    • C.refs is the same as C.refs,

    • all other fields are empty.

  • For each functypei in module.types, the function type functypei must be valid.

  • Under the context C:

    • For each funci in module.funcs, the definition funci must be valid with a function type fti.

    • If module.start is non-empty, then module.start must be valid.

    • For each importi in module.imports, the segment importi must be valid with an external type iti.

    • For each exporti in module.exports, the segment exporti must be valid with external type eti.

  • Under the context C:

    • For each tablei in module.tables, the definition tablei must be valid with a table type tti.

    • For each memi in module.mems, the definition memi must be valid with a memory type mti.

    • For each globali in module.globals, the definition globali must be valid with a global type gti.

    • For each elemi in module.elems, the segment elemi must be valid with reference type rti.

    • For each datai in module.datas, the segment datai must be valid.

  • The length of C.mems must not be larger than 1.

  • All export names exporti.name must be different.

  • Let ft be the concatenation of the internal function types fti, in index order.

  • Let tt be the concatenation of the internal table types tti, in index order.

  • Let mt be the concatenation of the internal memory types mti, in index order.

  • Let gt be the concatenation of the internal global types gti, in index order.

  • Let rt be the concatenation of the reference types rti, in index order.

  • Let it be the concatenation of external types iti of the imports, in index order.

  • Let et be the concatenation of external types eti of the exports, in index order.

  • Then the module is valid with external types itet.

(typeok)(Cfunc:ft)(Ctable:tt)(Cmem:mt)(Cglobal:gt)(Celem:rt)(Cdataok)n(Cstartok)?(Cimport:it)(Cexport:et)ift=funcs(it)itt=tables(it)imt=mems(it)igt=globals(it)x=funcidx(modulewithfuncs=ϵwithstart=ϵ)C={types type,funcs iftft,tables itttt,mems imtmt,globals igtgt,elems rt,datas okn,refs x}C={globals igt,funcs (C.funcs),refs (C.refs)}|C.mems|1(export.name) disjointmodule={types type,funcs func,tables table,mems mem,globals global,elems elem,datas datan,start start?,imports import,exports export}module:itet

Note

Most definitions in a module – particularly functions – are mutually recursive. Consequently, the definition of the context C in this rule is recursive: it depends on the outcome of validation of the function, table, memory, and global definitions contained in the module, which itself depends on C. However, this recursion is just a specification device. All types needed to construct C can easily be determined from a simple pre-pass over the module that does not perform any actual validation.

Globals, however, are not recursive and not accessible within constant expressions when they are defined locally. The effect of defining the limited context C for validating certain definitions is that they can only access functions and imported globals and nothing else.

Note

The restriction on the number of memories may be lifted in future versions of WebAssembly.