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.

type

The type definition (type rectype) is valid with the defined type sequence dt if:

  • |C.types| is equal to x.

  • The defined type sequence dt is equal to rollx(rectype).

  • Let C be the same context as C, but with the defined type sequence dt appended to the field types.

  • Under the context C, the recursive type rectype is valid with (okx).

x=|C.types|dt=rollx(rectype)C{types dt}rectype:ok(x)Ctype rectype:dt

type

The type definition sequence typeu1 is valid with the defined type sequence dtu1 if:

  • Either:

    • The type definition sequence typeu1 is equal to ϵ.

    • The defined type sequence dtu1 is equal to ϵ.

  • Or:

    • The type definition sequence typeu1 is equal to type1 type.

    • The defined type sequence dtu1 is equal to dt1 dt.

    • The type definition type1 is valid with the defined type sequence dt1.

    • Let C be the same context as C, but with the defined type sequence dt1 appended to the field types.

    • Under the context C, the type definition sequence type is valid with the defined type sequence dt.

Todo

below is the official specification

  • If the sequence is empty, then:

    • The context C must be empty.

    • Then the type sequence is valid.

  • Otherwise:

    • Let the recursive type rectype be the last element in the sequence.

    • The sequence without rectype must be valid for some context C.

    • Let the type index x be the length of C.types, i.e., the first type index free in C.

    • Let the sequence of defined types deftype be the result rollx(rectype) of rolling up into its sequence of defined types.

    • The recursive type rectype must be valid under the context C for type index x.

    • The current context C be the same as C, but with deftype appended to types.

    • Then the type sequence is valid.

Cϵ:ϵCtype1:dt1C{types dt1}type:dtCtype1 type:dt1 dt

Functions

Functions func are classified by defined types that expand to function types of the form func (t1t2).

{type x,locals t,body expr}

The function (func x local expr) is valid with the defined type C.types[x] if:

  • The defined type C.types[x] exists.

  • The expansion of the defined type C.types[x] is the composite type (func t1  t2).

  • |local| is equal to |lct|.

  • For all lt in lt and local in local:

    • The local local is valid with the local type lt.

  • Under the context C[.locals=(set,t1) lt][.labels=t2][.return=t2], the expression expr is valid with the result type t2.

Todo

below is the official specification

  • The defined type C.types[x] must be a function type.

  • Let func [t1][t2] be the expansion of the defined type C.types[x].

  • For each local declared by a value type t in t:

  • Let localtype be the concatenation of all localtypei.

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

    • locals set to the sequence of value types (set t1) localtype, 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 C.types[x].

C.types[x]func (t1t2)(Clocal:lt)C{locals (set t1) lt,labels (t2),return (t2)}expr:t2Cfunc x local expr:C.types[x]

Locals

Locals local are classified with local types.

{type valtype}

The local (local t) is valid with the local type (initu1,t) if:

  • Either:

    • The initialization status initu1 is equal to set.

    • A default value for value type the value type t is defined.

  • Or:

    • The initialization status initu1 is equal to unset.

    • A default value for value type the value type t is not defined.

Todo

below is the official specification

  • The value type valtype must be valid.

  • If valtype is defaultable, then:

    • The local is valid with local type set valtype.

  • Else:

    • The local is valid with local type unset valtype.

defaulttϵClocal t:set tdefaultt=ϵClocal t:unset t

Note

For cases where both rules are applicable, the former yields the more permissable type.

Tables

Tables table are classified by table types.

{type tabletype,init expr}

The table (table tabletype expr) is valid with the table type tabletype if:

  • The table type tt is valid.

  • The table type tabletype is equal to (at,lim,rt).

  • The expression expr is valid with the value type rt.

  • expr is const.

Todo

below is the official specification

Ctt:oktabletype=at lim rtCexpr:rt constCtable tabletype expr:tabletype

Memories

Memories mem are classified by memory types.

{type memtype}

The memory (memory memtype) is valid with the memory type memtype if:

  • The memory type memtype is valid.

Todo

below is the official specification

  • The memory type memtype must be valid.

  • Then the memory definition is valid with type memtype.

Cmemtype:okCmemory memtype:memtype

Globals

Globals global are classified by global types.

Sequences of globals are handled incrementally, such that each definition has access to previous definitions.

{type mut t,init expr}

The global (global globaltype expr) is valid with the global type globaltype if:

  • The global type gt is valid.

  • The global type globaltype is equal to (mut?,t).

  • The expression expr is valid with the value type t.

  • expr is const.

Todo

below is the official specification

Cgt:okglobaltype=mut? tCexpr:t constCglobal globaltype expr:globaltype

global

The global sequence globalu1 is valid with the global type sequence gtu1 if:

  • Either:

    • The global sequence globalu1 is equal to ϵ.

    • The global type sequence gtu1 is equal to ϵ.

  • Or:

    • The global sequence globalu1 is equal to global1 global.

    • The global type sequence gtu1 is equal to gt1 gt.

    • The global global1 is valid with the global type gt1.

    • Let C be the same context as C, but with the global type gt1 appended to the field globals.

    • Under the context C, the global sequence global is valid with the global type sequence gt.

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

    • Let C be the same context as C, but with the global type gt1 apppended to the globals list.

    • Under context C, the remainder of the sequence must be valid with some sequence gt of global types.

    • Then the sequence is valid with the sequence of global types consisting of gt1 prepended to gt.

Cϵ:ϵCglobal1:gt1C{globals gt1}global:gtCglobal1 global:gt1 gt

Tags

Tags tag are classified by their tag type, each containing an index to a function type with empty result.

{type x}

The tag (tag x) is valid with the tag type C.types[x] if:

  • The tag type C.types[x] exists.

  • The expansion of the tag type C.types[x] is the composite type (func functype).

Todo

below is the official specification

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

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

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

C.types[x]func functypeCtag x:C.types[x]

Element Segments

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

{type t,init e,mode elemmode}

The table segment (elem elemtype expr elemmode) is valid with the element type elemtype if:

  • The element type elemtype is valid.

  • For all expr in expr:

    • The expression expr is valid with the element type elemtype.

    • expr is const.

  • The element mode elemmode is valid with the element type elemtype.

Todo

below is the official specification

Celemtype:ok(Cexpr:elemtype const)Celemmode:elemtypeCelem elemtype expr elemmode:elemtype

The element mode elemmodeu1 is valid with the element type rt if:

  • Either:

    • The element mode elemmodeu1 is equal to (active x expr).

    • The table type C.tables[x] exists.

    • The table type C.tables[x] is equal to (at,lim,rt).

    • The element type rt matches the reference type rt.

    • The expression expr is valid with the value type i32.

    • expr is const.

  • Or:

    • The element mode elemmodeu1 is equal to passive.

  • Or:

    • The element mode elemmodeu1 is equal to declare.

Todo

below is the official specification

passive

Cpassive:rt

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]=at lim rtCrtrtCexpr:i32 constCactive x expr:rt

declare

Cdeclare:rt

Data Segments

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

{init b,mode datamode}

The memory segment (data b datamode) is valid with the data type ok if:

  • The data mode datamode is valid with the data type ok.

Todo

below is the official specification

  • The data mode datamode must be valid.

  • Then the data segment is valid.

Cdatamode:okCdata b datamode:ok

The data mode datamodeu1 is valid with the data type ok if:

  • Either:

    • The data mode datamodeu1 is equal to (active x expr).

    • The memory type C.mems[x] exists.

    • The memory type C.mems[x] is equal to mt.

    • The expression expr is valid with the value type i32.

    • expr is const.

  • Or:

    • The data mode datamodeu1 is equal to passive.

Todo

below is the official specification

passive

  • The data mode is valid.

Cpassive:ok

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]=mtCexpr:i32 constCactive x expr:ok

Start Function

Start function declarations start are not classified by any type.

{func x}

The start function (start x) is valid if:

  • The defined type C.funcs[x] exists.

  • The expansion of the defined type C.funcs[x] is the composite type (func ϵ  ϵ).

Todo

below is the official specification

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

  • The expansion of C.funcs[x] must be a function type func [][].

  • Then the start function is valid.

C.funcs[x]func (ϵϵ)Cstart x:ok

Exports

Exports export are classified by their external type.

{name name,desc exportdesc}

The export (export name externidx) is valid with the name name and the external type xt if:

  • The external index externidx is valid with the external type xt.

Todo

below is the official specification

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

  • Then the export is valid with external type externtype.

Cexternidx:xtCexport name externidx:name xt

func x

The external index (func x) is valid with the external type (func dt) if:

  • The defined type C.funcs[x] exists.

  • The defined type C.funcs[x] is equal to dt.

Todo

below is the official specification

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

  • Let dt be the defined type C.funcs[x].

  • Then the export description is valid with external type func dt.

C.funcs[x]=dtCfunc x:func dt

table x

The external index (table x) is valid with the external type (table tt) if:

  • The table type C.tables[x] exists.

  • The table type C.tables[x] is equal to tt.

Todo

below is the official specification

  • 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]=ttCtable x:table tt

mem x

The external index (memory x) is valid with the external type (mem mt) if:

  • The memory type C.mems[x] exists.

  • The memory type C.mems[x] is equal to mt.

Todo

below is the official specification

  • 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]=mtCmemory x:mem mt

global x

The external index (global x) is valid with the external type (global gt) if:

  • The global type C.globals[x] exists.

  • The global type C.globals[x] is equal to gt.

Todo

below is the official specification

  • 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]=gtCglobal x:global gt

tag x

  • The tag C.tags[x] must be defined in the context.

  • Then the export description is valid with external type tag C.tags[x].

C.tags[x]=jtCtag x:tag jt

Imports

Imports import are classified by external types.

{module name1,name name2,desc importdesc}

The import (import name1 name2 xt) is valid with the external type xt if:

  • The external type xt is valid.

Todo

below is the official specification

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

  • Then the import is valid with type externtype.

Cxt:okCimport name1 name2 xt:xt

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.

The external types classifying a module may contain free type indices that refer to types defined within the module.

The module (module type import func global table mem tag elem data start? export) is valid with the module type t if:

  • Under the context {types ϵ,recs ϵ,funcs ϵ,globals ϵ,tables ϵ,mems ϵ,tags ϵ,elems ϵ,datas ϵ,locals ϵ,labels ϵ,return ϵ,refs ϵ}, the type definition sequence type is valid with the defined type sequence dt.

  • |xti| is equal to |import|.

  • For all import in import and xti in xti:

    • Under the context {types dt,recs ϵ,funcs ϵ,globals ϵ,tables ϵ,mems ϵ,tags ϵ,elems ϵ,datas ϵ,locals ϵ,labels ϵ,return ϵ,refs ϵ}, the import import is valid with the external type xti.

  • Under the context C, the global sequence global is valid with the global type sequence gt.

  • |tt| is equal to |table|.

  • For all table in table and tt in tt:

    • Under the context C, the table table is valid with the table type tt.

  • |mt| is equal to |mem|.

  • For all mem in mem and mt in mt:

    • Under the context C, the memory mem is valid with the memory type mt.

  • |tag| is equal to |jt|.

  • For all jt in jt and tag in tag:

    • Under the context C, the tag tag is valid with the tag type jt.

  • |func| is equal to |dt|.

  • For all dt in dt and func in func:

    • The function func is valid with the defined type dt.

  • |rt| is equal to |elem|.

  • For all elem in elem and rt in rt:

    • The table segment elem is valid with the element type rt.

  • |ok| is equal to |data|.

  • For all data in data and ok in ok:

    • The memory segment data is valid with the data type ok.

  • If start is defined, then:

    • The start function start is valid.

  • |nm| is equal to |export|.

  • |xte| is equal to |export|.

  • For all export in export and nm in nm and xte in xte:

    • The export export is valid with the name nm and the external type xte.

  • nm disjoint is equal to true.

  • The context C is equal to C[.globals=gt][.tables=tti tt][.mems=mti mt][.tags=jti jt][.elems=rt][.datas=ok].

  • The context C is equal to {types dt,recs ϵ,funcs dti dt,globals gti,tables ϵ,mems ϵ,tags ϵ,elems ϵ,datas ϵ,locals ϵ,labels ϵ,return ϵ,refs x}.

  • The function index sequence x is equal to funcidx((global,table,mem,elem,data)).

  • The defined type sequence dti is equal to funcs(xti).

  • The global type sequence gti is equal to globals(xti).

  • The table type sequence tti is equal to tables(xti).

  • The memory type sequence mti is equal to mems(xti).

  • The tag type sequence jti is equal to tags(xti).

  • Let t be the module type closC(xti  xte).

Todo

below is the official specification

  • Let module be the module to validate.

  • The types module.types must be valid yielding a context C0.

  • Let C be a context where:

    • C.types is C0.types,

    • C.funcs is funcs(it) concatenated with dt, with the import’s external types it and the internal defined types dt 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.tags is tags(it) concatenated with ht, with the import’s external types it and the internal tag types ht as determined below,

    • C.elems is rt as determined below,

    • C.datas is ok as determined below,

    • 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.types is the same as C.types,

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

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

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

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

    • all other fields are empty.

  • Under the context C:

  • Under the context C:

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

    • For each tagi in module.tags, the definition tagi must be valid with a tag type hti.

    • 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 with data type oki.

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

  • Let dt be the concatenation of the internal function types dti, 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 ht be the concatenation of the internal tag types hti, in index order.

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

  • Let ok be the concatenation of the data types oki, 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.

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

  • All export names exporti.name must be different.

  • Then the module is valid with external types itet.

{}type:dt({types dt}import:xti)Cglobal:gt(Ctable:tt)(Cmem:mt)(Ctag:jt)(Cfunc:dt)(Celem:rt)(Cdata:ok)(Cstart:ok)?(Cexport:nm xte)nm disjointC=C{globals gt,tables tti tt,mems mti mt,tags jti jt,elems rt,datas ok}C={types dt,funcs dti dt,globals gti,refs x}x=funcidx(global table mem elem data)dti=funcs(xti)gti=globals(xti)tti=tables(xti)mti=mems(xti)jti=tags(xti)module type import func global table mem tag elem data start? export:closC(xtixte)

Todo

Check refs; check export names

Note

All functions in a module 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 but evaluated sequentially, such that each constant expressions only has access to imported or previously defined globals.