Modules

For modules, the execution semantics primarily defines instantiation, which allocates instances for a module and its contained definitions, initializes tables and memories from contained element and data segments, and invokes the start function if present. It also includes invocation of exported functions.

Instantiation depends on a number of auxiliary notions for type-checking imports and allocating instances.

External Typing

For the purpose of checking external values against imports, such values are classified by external types. The following auxiliary typing rules specify this typing relation relative to a store \(S\) in which the referenced instances live.

\(\href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~a\)

• The store entry \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a]\) must be a function instance \(\{\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}, \dots\}\).

• Then \(\href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~a\) is valid with external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\).

\[\frac{ S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a] = \{\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}, \dots\} }{ S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~a : \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}} }\]

\(\href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~a\)

• The store entry \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a]\) must be a table instance \(\{\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~(\mathit{fa}^?)^n, \href{../exec/runtime.html#syntax-tableinst}{\mathsf{max}}~m^?\}\).

• Then \(\href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~a\) is valid with external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~(\{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\}~\href{../syntax/types.html#syntax-elemtype}{\mathsf{funcref}})\).

\[\frac{ S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a] = \{ \href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~(\mathit{fa}^?)^n, \href{../exec/runtime.html#syntax-tableinst}{\mathsf{max}}~m^? \} }{ S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~a : \href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~(\{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\}~\href{../syntax/types.html#syntax-elemtype}{\mathsf{funcref}}) }\]

\(\href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~a\)

• The store entry \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\) must be a memory instance \(\{\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}~b^{n\cdot64\,\mathrm{Ki}}, \href{../exec/runtime.html#syntax-meminst}{\mathsf{max}}~m^?\}\), for some \(n\).

• Then \(\href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~a\) is valid with external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~(\{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\})\).

\[\frac{ S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a] = \{ \href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}~b^{n\cdot64\,\mathrm{Ki}}, \href{../exec/runtime.html#syntax-meminst}{\mathsf{max}}~m^? \} }{ S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~a : \href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\} }\]

\(\href{../exec/runtime.html#syntax-externval}{\mathsf{global}}~a\)

• The store entry \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[a]\) must be a global instance \(\{\href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}~(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c), \href{../exec/runtime.html#syntax-globalinst}{\mathsf{mut}}~\href{../syntax/types.html#syntax-mut}{\mathit{mut}}\}\).

• Then \(\href{../exec/runtime.html#syntax-externval}{\mathsf{global}}~a\) is valid with external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t)\).

\[\frac{ S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[a] = \{ \href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}~(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c), \href{../exec/runtime.html#syntax-globalinst}{\mathsf{mut}}~\href{../syntax/types.html#syntax-mut}{\mathit{mut}} \} }{ S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{global}}~a : \href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t) }\]

Import Matching

When instantiating a module, external values must be provided whose types are matched against the respective external types classifying each import. In some cases, this allows for a simple form of subtyping, as defined below.

Limits

Limits \(\{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n_1, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m_1^? \}\) match limits \(\{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n_2, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m_2^? \}\) if and only if:

• \(n_1\) is larger than or equal to \(n_2\).

• Either:

  • \(m_2^?\) is empty.

• Or:

  • Both \(m_1^?\) and \(m_2^?\) are non-empty.

  • \(m_1\) is smaller than or equal to \(m_2\).

\[\begin{split}~\\[-1ex] \frac{ n_1 \geq n_2 }{ \href{../exec/modules.html#match-limits}{\vdash} \{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n_1, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m_1^? \} \href{../exec/modules.html#match}{\leq} \{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n_2, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~\epsilon \} } \quad \frac{ n_1 \geq n_2 \qquad m_1 \leq m_2 }{ \href{../exec/modules.html#match-limits}{\vdash} \{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n_1, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m_1 \} \href{../exec/modules.html#match}{\leq} \{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n_2, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m_2 \} }\end{split}\]

Functions

An external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_1\) matches \(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_2\) if and only if:

• Both \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_1\) and \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_2\) are the same.

\[\begin{split}~\\[-1ex] \frac{ }{ \href{../exec/modules.html#match-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}} \href{../exec/modules.html#match}{\leq} \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}} }\end{split}\]

Tables

An external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1~\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}_1)\) matches \(\href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2~\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}_2)\) if and only if:

• Limits \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1\) match \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2\).

• Both \(\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}_1\) and \(\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}_2\) are the same.

\[\frac{ \href{../exec/modules.html#match-limits}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1 \href{../exec/modules.html#match}{\leq} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2 }{ \href{../exec/modules.html#match-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1~\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}) \href{../exec/modules.html#match}{\leq} \href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2~\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}) }\]

Memories

An external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1\) matches \(\href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2\) if and only if:

• Limits \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1\) match \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2\).

\[\frac{ \href{../exec/modules.html#match-limits}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1 \href{../exec/modules.html#match}{\leq} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2 }{ \href{../exec/modules.html#match-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1 \href{../exec/modules.html#match}{\leq} \href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2 }\]

Globals

An external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_1\) matches \(\href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_2\) if and only if:

• Both \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_1\) and \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_2\) are the same.

\[\begin{split}~\\[-1ex] \frac{ }{ \href{../exec/modules.html#match-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}} \href{../exec/modules.html#match}{\leq} \href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}} }\end{split}\]

Allocation

New instances of functions, tables, memories, and globals are allocated in a store \(S\), as defined by the following auxiliary functions.

Functions

1. Let \(\href{../syntax/modules.html#syntax-func}{\mathit{func}}\) be the function to allocate and \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\) its module instance.

2. Let \(a\) be the first free function address in \(S\).

3. Let \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\) be the function type \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}[\href{../syntax/modules.html#syntax-func}{\mathit{func}}.\href{../syntax/modules.html#syntax-func}{\mathsf{type}}]\).

4. Let \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}\) be the function instance \(\{ \href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{code}}~\href{../syntax/modules.html#syntax-func}{\mathit{func}} \}\).

5. Append \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}\) to the \(\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}\) of \(S\).

6. Return \(a\).

\[\begin{split}~\\[-1ex] \begin{array}{rlll} \href{../exec/modules.html#alloc-func}{\mathrm{allocfunc}}(S, \href{../syntax/modules.html#syntax-func}{\mathit{func}}, \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}) &=& S', \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} \\[1ex] \mbox{where:} \hfill \\ \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} &=& |S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}| \\ \href{../syntax/types.html#syntax-functype}{\mathit{functype}} &=& \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}[\href{../syntax/modules.html#syntax-func}{\mathit{func}}.\href{../syntax/modules.html#syntax-func}{\mathsf{type}}] \\ \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}} &=& \{ \href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{code}}~\href{../syntax/modules.html#syntax-func}{\mathit{func}} \} \\ S' &=& S \href{../syntax/conventions.html#notation-compose}{\oplus} \{\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}~\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}\} \\ \end{array}\end{split}\]

Host Functions

1. Let \(\href{../exec/runtime.html#syntax-hostfunc}{\mathit{hostfunc}}\) be the host function to allocate and \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\) its function type.

2. Let \(a\) be the first free function address in \(S\).

3. Let \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}\) be the function instance \(\{ \href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{hostcode}}~\href{../exec/runtime.html#syntax-hostfunc}{\mathit{hostfunc}} \}\).

4. Append \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}\) to the \(\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}\) of \(S\).

5. Return \(a\).

\[\begin{split}~\\[-1ex] \begin{array}{rlll} \href{../exec/modules.html#alloc-hostfunc}{\mathrm{allochostfunc}}(S, \href{../syntax/types.html#syntax-functype}{\mathit{functype}}, \href{../exec/runtime.html#syntax-hostfunc}{\mathit{hostfunc}}) &=& S', \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} \\[1ex] \mbox{where:} \hfill \\ \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} &=& |S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}| \\ \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}} &=& \{ \href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{hostcode}}~\href{../exec/runtime.html#syntax-hostfunc}{\mathit{hostfunc}} \} \\ S' &=& S \href{../syntax/conventions.html#notation-compose}{\oplus} \{\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}~\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}\} \\ \end{array}\end{split}\]

Note

Host functions are never allocated by the WebAssembly semantics itself, but may be allocated by the embedder.

Tables

1. Let \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\) be the table type to allocate.

2. Let \((\{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\}~\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}})\) be the structure of table type \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\).

3. Let \(a\) be the first free table address in \(S\).

4. Let \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}\) be the table instance \(\{ \href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~(\epsilon)^n, \href{../exec/runtime.html#syntax-tableinst}{\mathsf{max}}~m^? \}\) with \(n\) empty elements.

5. Append \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}\) to the \(\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}\) of \(S\).

6. Return \(a\).

\[\begin{split}\begin{array}{rlll} \href{../exec/modules.html#alloc-table}{\mathrm{alloctable}}(S, \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}) &=& S', \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}} \\[1ex] \mbox{where:} \hfill \\ \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}} &=& \{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\}~\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}} \\ \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}} &=& |S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}| \\ \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}} &=& \{ \href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~(\epsilon)^n, \href{../exec/runtime.html#syntax-tableinst}{\mathsf{max}}~m^? \} \\ S' &=& S \href{../syntax/conventions.html#notation-compose}{\oplus} \{\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}~\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}\} \\ \end{array}\end{split}\]

Memories

1. Let \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\) be the memory type to allocate.

2. Let \(\{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\}\) be the structure of memory type \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\).

3. Let \(a\) be the first free memory address in \(S\).

4. Let \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}\) be the memory instance \(\{ \href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}~(\def\mathdef1287#1{\mathtt{0x#1}}\mathdef1287{00})^{n \cdot 64\,\mathrm{Ki}}, \href{../exec/runtime.html#syntax-meminst}{\mathsf{max}}~m^? \}\) that contains \(n\) pages of zeroed bytes.

5. Append \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}\) to the \(\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}\) of \(S\).

6. Return \(a\).

\[\begin{split}\begin{array}{rlll} \href{../exec/modules.html#alloc-mem}{\mathrm{allocmem}}(S, \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}) &=& S', \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}} \\[1ex] \mbox{where:} \hfill \\ \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} &=& \{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\} \\ \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}} &=& |S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}| \\ \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}} &=& \{ \href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}~(\def\mathdef1288#1{\mathtt{0x#1}}\mathdef1288{00})^{n \cdot 64\,\mathrm{Ki}}, \href{../exec/runtime.html#syntax-meminst}{\mathsf{max}}~m^? \} \\ S' &=& S \href{../syntax/conventions.html#notation-compose}{\oplus} \{\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}~\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}\} \\ \end{array}\end{split}\]

Globals

1. Let \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\) be the global type to allocate and \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}\) the value to initialize the global with.

2. Let \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t\) be the structure of global type \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\).

3. Let \(a\) be the first free global address in \(S\).

4. Let \(\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}\) be the global instance \(\{ \href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}, \href{../exec/runtime.html#syntax-globalinst}{\mathsf{mut}}~\href{../syntax/types.html#syntax-mut}{\mathit{mut}} \}\).

5. Append \(\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}\) to the \(\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}\) of \(S\).

6. Return \(a\).

\[\begin{split}\begin{array}{rlll} \href{../exec/modules.html#alloc-global}{\mathrm{allocglobal}}(S, \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}, \href{../exec/runtime.html#syntax-val}{\mathit{val}}) &=& S', \href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}} \\[1ex] \mbox{where:} \hfill \\ \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}} &=& \href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t \\ \href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}} &=& |S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}| \\ \href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}} &=& \{ \href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}, \href{../exec/runtime.html#syntax-globalinst}{\mathsf{mut}}~\href{../syntax/types.html#syntax-mut}{\mathit{mut}} \} \\ S' &=& S \href{../syntax/conventions.html#notation-compose}{\oplus} \{\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}~\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}\} \\ \end{array}\end{split}\]

Element segments

1. Let \(\href{../exec/runtime.html#syntax-funcelem}{\mathit{funcelem}}^\ast\) be the vector of function elements to allocate.

2. Let \(a\) be the first free element address in \(S\).

3. Let \(\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}\) be the element instance \(\{ \href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}}~\href{../exec/runtime.html#syntax-funcelem}{\mathit{funcelem}}^\ast \}\).

4. Append \(\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}\) to the \(\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}\) of \(S\).

5. Return \(a\).

\[\begin{split}\begin{array}{rlll} \href{../exec/modules.html#alloc-elem}{\mathrm{allocelem}}(S, \href{../exec/runtime.html#syntax-funcelem}{\mathit{funcelem}}^\ast) &=& S', \href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}} \\[1ex] \mbox{where:} \hfill \\ \href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}} &=& |S.\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}| \\ \href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}} &=& \{ \href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}}~\href{../exec/runtime.html#syntax-funcelem}{\mathit{funcelem}}^\ast \} \\ S' &=& S \href{../syntax/conventions.html#notation-compose}{\oplus} \{\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}~\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}\} \\ \end{array}\end{split}\]

Data segments

1. Let \(\href{../exec/numerics.html#aux-bytes}{\mathrm{bytes}}\) be the vector of bytes to allocate.

2. Let \(a\) be the first free data address in \(S\).

3. Let \(\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}\) be the data instance \(\{ \href{../exec/runtime.html#syntax-datainst}{\mathsf{data}}~\href{../exec/numerics.html#aux-bytes}{\mathrm{bytes}} \}\).

4. Append \(\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}\) to the \(\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}\) of \(S\).

5. Return \(a\).

\[\begin{split}\begin{array}{rlll} \href{../exec/modules.html#alloc-data}{\mathrm{allocdata}}(S, \href{../exec/numerics.html#aux-bytes}{\mathrm{bytes}}) &=& S', \href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}} \\[1ex] \mbox{where:} \hfill \\ \href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}} &=& |S.\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}| \\ \href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}} &=& \{ \href{../exec/runtime.html#syntax-datainst}{\mathsf{data}}~\href{../exec/numerics.html#aux-bytes}{\mathrm{bytes}} \} \\ S' &=& S \href{../syntax/conventions.html#notation-compose}{\oplus} \{\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}~\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}\} \\ \end{array}\end{split}\]

Growing tables

1. Let \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}\) be the table instance to grow and \(n\) the number of elements by which to grow it.

2. Let \(\mathit{len}\) be \(n\) added to the length of \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}\).

3. If \(\mathit{len}\) is larger than or equal to \(2^{32}\), then fail.

4. If \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{max}}\) is not empty and its value is smaller than \(\mathit{len}\), then fail.

5. Append \(n\) empty elements to \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}\).

\[\begin{split}\begin{array}{rllll} \href{../exec/modules.html#grow-table}{\mathrm{growtable}}(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}, n) &=& \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}} \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}} = \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~(\epsilon)^n \\ && ( \begin{array}[t]{@{}r@{~}l@{}} \mathrel{\mbox{if}} & \mathit{len} = n + |\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}| \\ \wedge & \mathit{len} < 2^{32} \\ \wedge & (\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{max}} = \epsilon \vee \mathit{len} \leq \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{max}})) \\ \end{array} \\ \end{array}\end{split}\]

Growing memories

1. Let \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}\) be the memory instance to grow and \(n\) the number of pages by which to grow it.

2. Assert: The length of \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\) is divisible by the page size \(64\,\mathrm{Ki}\).

3. Let \(\mathit{len}\) be \(n\) added to the length of \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\) divided by the page size \(64\,\mathrm{Ki}\).

4. If \(\mathit{len}\) is larger than \(2^{16}\), then fail.

5. If \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{max}}\) is not empty and its value is smaller than \(\mathit{len}\), then fail.

6. Append \(n\) times \(64\,\mathrm{Ki}\) bytes with value \(\def\mathdef1289#1{\mathtt{0x#1}}\mathdef1289{00}\) to \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\).

\[\begin{split}\begin{array}{rllll} \href{../exec/modules.html#grow-mem}{\mathrm{growmem}}(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}, n) &=& \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}} \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../exec/runtime.html#syntax-meminst}{\mathsf{data}} = \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}~(\def\mathdef1290#1{\mathtt{0x#1}}\mathdef1290{00})^{n \cdot 64\,\mathrm{Ki}} \\ && ( \begin{array}[t]{@{}r@{~}l@{}} \mathrel{\mbox{if}} & \mathit{len} = n + |\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}| / 64\,\mathrm{Ki} \\ \wedge & \mathit{len} \leq 2^{16} \\ \wedge & (\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{max}} = \epsilon \vee \mathit{len} \leq \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{max}})) \\ \end{array} \\ \end{array}\end{split}\]

Modules

The allocation function for modules requires a suitable list of external values that are assumed to match the import vector of the module, a list of initialization values for the module’s globals, and list of function element vectors for the module’s element segments.

1. Let \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) be the module to allocate and \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast\) the vector of external values providing the module’s imports, \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\) the initialization values of the module’s globals, and \((\href{../exec/runtime.html#syntax-funcelem}{\mathit{funcelem}}^\ast)^\ast\) the function element vectors of the module’s element segments.

2. For each function \(\href{../syntax/modules.html#syntax-func}{\mathit{func}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{funcs}}\), do:

   1. Let \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}_i\) be the function address resulting from allocating \(\href{../syntax/modules.html#syntax-func}{\mathit{func}}_i\) for the module instance \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\) defined below.

3. For each table \(\href{../syntax/modules.html#syntax-table}{\mathit{table}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{tables}}\), do:

   1. Let \(\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}_i\) be the table address resulting from allocating \(\href{../syntax/modules.html#syntax-table}{\mathit{table}}_i.\href{../syntax/modules.html#syntax-table}{\mathsf{type}}\).

4. For each memory \(\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{mems}}\), do:

   1. Let \(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}_i\) be the memory address resulting from allocating \(\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}_i.\href{../syntax/modules.html#syntax-mem}{\mathsf{type}}\).

5. For each global \(\href{../syntax/modules.html#syntax-global}{\mathit{global}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{globals}}\), do:

   1. Let \(\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}_i\) be the global address resulting from allocating \(\href{../syntax/modules.html#syntax-global}{\mathit{global}}_i.\href{../syntax/modules.html#syntax-global}{\mathsf{type}}\) with initializer value \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast[i]\).

6. For each element segment \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{elems}}\), do:

   1. Let \(\href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}_i\) be the element address resulting from allocating a element instance with contents \((\href{../exec/runtime.html#syntax-funcelem}{\mathit{funcelem}}^\ast)^\ast[i]\).

7. For each data segment \(\href{../syntax/modules.html#syntax-data}{\mathit{data}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{datas}}\), do:

   1. Let \(\href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}_i\) be the data address resulting from allocating a data instance with contents \(\href{../syntax/modules.html#syntax-data}{\mathit{data}}_i.\href{../syntax/modules.html#syntax-data}{\mathsf{init}}\).

8. Let \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}^\ast\) be the the concatenation of the function addresses \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}_i\) in index order.

9. Let \(\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}^\ast\) be the the concatenation of the table addresses \(\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}_i\) in index order.

10. Let \(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}^\ast\) be the the concatenation of the memory addresses \(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}_i\) in index order.

11. Let \(\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}^\ast\) be the the concatenation of the global addresses \(\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}_i\) in index order.

12. Let \(\href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}^\ast\) be the the concatenation of the element addresses \(\href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}_i\) in index order.

13. Let \(\href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}^\ast\) be the the concatenation of the data addresses \(\href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}_i\) in index order.

14. Let \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}_{\mathrm{mod}}^\ast\) be the list of function addresses extracted from \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast\), concatenated with \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}^\ast\).

15. Let \(\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}_{\mathrm{mod}}^\ast\) be the list of table addresses extracted from \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast\), concatenated with \(\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}^\ast\).

16. Let \(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}_{\mathrm{mod}}^\ast\) be the list of memory addresses extracted from \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast\), concatenated with \(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}^\ast\).

17. Let \(\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}_{\mathrm{mod}}^\ast\) be the list of global addresses extracted from \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast\), concatenated with \(\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}^\ast\).

18. For each export \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{exports}}\), do:

    1. If \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i\) is a function export for function index \(x\), then let \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_i\) be the external value \(\href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}_{\mathrm{mod}}^\ast[x])\).

    2. Else, if \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i\) is a table export for table index \(x\), then let \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_i\) be the external value \(\href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~(\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}_{\mathrm{mod}}^\ast[x])\).

    3. Else, if \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i\) is a memory export for memory index \(x\), then let \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_i\) be the external value \(\href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}_{\mathrm{mod}}^\ast[x])\).

    4. Else, if \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i\) is a global export for global index \(x\), then let \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_i\) be the external value \(\href{../exec/runtime.html#syntax-externval}{\mathsf{global}}~(\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}_{\mathrm{mod}}^\ast[x])\).

    5. Let \(\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}_i\) be the export instance \(\{\href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}~(\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i.\href{../syntax/modules.html#syntax-export}{\mathsf{name}}), \href{../exec/runtime.html#syntax-exportinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_i\}\).

19. Let \(\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}^\ast\) be the the concatenation of the export instances \(\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}_i\) in index order.

20. Let \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\) be the module instance \(\{\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}~(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{types}}),\) \(\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}_{\mathrm{mod}}^\ast,\) \(\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}~\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}_{\mathrm{mod}}^\ast,\) \(\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}~\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}_{\mathrm{mod}}^\ast,\) \(\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globaladdrs}}~\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}_{\mathrm{mod}}^\ast,\) \(\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{exports}}~\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}^\ast\}\).

21. Return \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\).

\[\begin{split}~\\ \begin{array}{rlll} \href{../exec/modules.html#alloc-module}{\mathrm{allocmodule}}(S, \href{../syntax/modules.html#syntax-module}{\mathit{module}}, \href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast, \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast, (\href{../exec/runtime.html#syntax-funcelem}{\mathit{funcelem}}^\ast)^\ast) &=& S', \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}} \end{array}\end{split}\]

where:

\[\begin{split}\begin{array}{rlll} \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}} &=& \{~ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}~\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{types}}, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}~\href{../exec/runtime.html#syntax-externval}{\mathrm{funcs}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast)~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}~\href{../exec/runtime.html#syntax-externval}{\mathrm{tables}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast)~\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}~\href{../exec/runtime.html#syntax-externval}{\mathrm{mems}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast)~\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globaladdrs}}~\href{../exec/runtime.html#syntax-externval}{\mathrm{globals}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast)~\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{elemaddrs}}~\href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{dataaddrs}}~\href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{exports}}~\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}^\ast ~\} \end{array} \\[1ex] S_1, \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}^\ast &=& \href{../exec/modules.html#alloc-func}{\mathrm{allocfunc}}^\ast(S, \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{funcs}}, \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}) \\ S_2, \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}^\ast &=& \href{../exec/modules.html#alloc-table}{\mathrm{alloctable}}^\ast(S_1, (\href{../syntax/modules.html#syntax-table}{\mathit{table}}.\href{../syntax/modules.html#syntax-table}{\mathsf{type}})^\ast) \qquad\qquad\qquad~ (\mathrel{\mbox{where}} \href{../syntax/modules.html#syntax-table}{\mathit{table}}^\ast = \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{tables}}) \\ S_3, \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}^\ast &=& \href{../exec/modules.html#alloc-mem}{\mathrm{allocmem}}^\ast(S_2, (\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}.\href{../syntax/modules.html#syntax-mem}{\mathsf{type}})^\ast) \qquad\qquad\qquad~ (\mathrel{\mbox{where}} \href{../syntax/modules.html#syntax-mem}{\mathit{mem}}^\ast = \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{mems}}) \\ S_4, \href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}^\ast &=& \href{../exec/modules.html#alloc-global}{\mathrm{allocglobal}}^\ast(S_3, (\href{../syntax/modules.html#syntax-global}{\mathit{global}}.\href{../syntax/modules.html#syntax-global}{\mathsf{type}})^\ast, \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast) \qquad\quad~ (\mathrel{\mbox{where}} \href{../syntax/modules.html#syntax-global}{\mathit{global}}^\ast = \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{globals}}) \\ S_5, \href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}^\ast &=& \href{../exec/modules.html#alloc-elem}{\mathrm{allocelem}}^\ast(S_4, (\href{../exec/runtime.html#syntax-funcelem}{\mathit{funcelem}}^\ast)^\ast) \\ S', \href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}^\ast &=& \href{../exec/modules.html#alloc-data}{\mathrm{allocdata}}^\ast(S_5, (\href{../syntax/modules.html#syntax-data}{\mathit{data}}.\href{../syntax/modules.html#syntax-data}{\mathsf{init}})^\ast) \qquad\qquad\qquad~ (\mathrel{\mbox{where}} \href{../syntax/modules.html#syntax-data}{\mathit{data}}^\ast = \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{datas}}) \\ \href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}^\ast &=& \{ \href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}~(\href{../syntax/modules.html#syntax-export}{\mathit{export}}.\href{../syntax/modules.html#syntax-export}{\mathsf{name}}), \href{../exec/runtime.html#syntax-exportinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{ex}} \}^\ast \quad (\mathrel{\mbox{where}} \href{../syntax/modules.html#syntax-export}{\mathit{export}}^\ast = \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{exports}}) \\[1ex] \href{../exec/runtime.html#syntax-externval}{\mathrm{funcs}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{ex}}^\ast) &=& (\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}[x])^\ast \qquad~ (\mathrel{\mbox{where}} x^\ast = \href{../syntax/modules.html#syntax-exportdesc}{\mathrm{funcs}}(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{exports}})) \\ \href{../exec/runtime.html#syntax-externval}{\mathrm{tables}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{ex}}^\ast) &=& (\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[x])^\ast \qquad (\mathrel{\mbox{where}} x^\ast = \href{../syntax/modules.html#syntax-exportdesc}{\mathrm{tables}}(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{exports}})) \\ \href{../exec/runtime.html#syntax-externval}{\mathrm{mems}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{ex}}^\ast) &=& (\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[x])^\ast \qquad (\mathrel{\mbox{where}} x^\ast = \href{../syntax/modules.html#syntax-exportdesc}{\mathrm{mems}}(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{exports}})) \\ \href{../exec/runtime.html#syntax-externval}{\mathrm{globals}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{ex}}^\ast) &=& (\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globaladdrs}}[x])^\ast \qquad\!\!\! (\mathrel{\mbox{where}} x^\ast = \href{../syntax/modules.html#syntax-exportdesc}{\mathrm{globals}}(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{exports}})) \\ \end{array}\end{split}\]

Here, the notation \(\mathrm{allocx}^\ast\) is shorthand for multiple allocations of object kind \(X\), defined as follows:

\[\begin{split}\begin{array}{rlll} \mathrm{allocx}^\ast(S_0, X^n, \dots) &=& S_n, a^n \\[1ex] \mbox{where for all $i < n$:} \hfill \\ S_{i+1}, a^n[i] &=& \mathrm{allocx}(S_i, X^n[i], \dots) \end{array}\end{split}\]

Moreover, if the dots \(\dots\) are a sequence \(A^n\) (as for globals), then the elements of this sequence are passed to the allocation function pointwise.

Note

The definition of module allocation is mutually recursive with the allocation of its associated functions, because the resulting module instance \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\) is passed to the function allocator as an argument, in order to form the necessary closures. In an implementation, this recursion is easily unraveled by mutating one or the other in a secondary step.

Instantiation

Given a store \(S\), a module \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) is instantiated with a list of external values \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^n\) supplying the required imports as follows.

Instantiation checks that the module is valid and the provided imports match the declared types, and may fail with an error otherwise. Instantiation can also result in a trap from executing the start function. It is up to the embedder to define how such conditions are reported.

1. If \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) is not valid, then:

   1. Fail.

2. Assert: \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) is valid with external types \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_{\mathrm{im}}^m\) classifying its imports.

3. If the number \(m\) of imports is not equal to the number \(n\) of provided external values, then:

   1. Fail.

4. For each external value \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_i\) in \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^n\) and external type \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}'_i\) in \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_{\mathrm{im}}^n\), do:

   1. If \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_i\) is not valid with an external type \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_i\) in store \(S\), then:

      1. Fail.

   2. If \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_i\) does not match \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}'_i\), then:

      1. Fail.

5. Let \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\) be the vector of global initialization values determined by \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) and \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^n\). These may be calculated as follows.

   1. Let \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}_{\mathrm{im}}\) be the auxiliary module instance \(\{\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globaladdrs}}~\href{../exec/runtime.html#syntax-externval}{\mathrm{globals}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^n)\}\) that only consists of the imported globals.

   2. Let \(F_{\mathrm{im}}\) be the auxiliary frame \(\{ \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}_{\mathrm{im}}, \href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\epsilon \}\).

   3. Push the frame \(F_{\mathrm{im}}\) to the stack.

   4. For each global \(\href{../syntax/modules.html#syntax-global}{\mathit{global}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{globals}}\), do:

      1. Let \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_i\) be the result of evaluating the initializer expression \(\href{../syntax/modules.html#syntax-global}{\mathit{global}}_i.\href{../syntax/modules.html#syntax-global}{\mathsf{init}}\).

   5. Assert: due to validation, the frame \(F_{\mathrm{im}}\) is now on the top of the stack.

   6. Pop the frame \(F_{\mathrm{im}}\) from the stack.

   7. Let \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\) be the conatenation of \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_i\) in index order.

6. Let \((\href{../exec/runtime.html#syntax-funcelem}{\mathit{funcelem}}^\ast)^\ast\) be the list of function element vectors determined by the element segments in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\). These may be calculated as follows.

   1. For each element segment \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{elems}}\), and for each element expression \(\href{../syntax/modules.html#syntax-elemexpr}{\mathit{elemexpr}}_{ij}\) in \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i.\href{../syntax/modules.html#syntax-elem}{\mathsf{init}}\), do:

      1. If \(\href{../syntax/modules.html#syntax-elemexpr}{\mathit{elemexpr}}_{ij}\) is of the form \(\href{../syntax/modules.html#syntax-elemexpr}{\mathsf{ref.null}}\), then let the function element \(\href{../exec/runtime.html#syntax-funcelem}{\mathit{funcelem}}_{ij}\) be \(\epsilon\).

      2. Else, \(\href{../syntax/modules.html#syntax-elemexpr}{\mathit{elemexpr}}_{ij}\) is of the form is \(\href{../syntax/modules.html#syntax-elemexpr}{\mathsf{ref.func}}~\href{../syntax/modules.html#syntax-funcidx}{\mathit{funcidx}}_{ij}\).

      3. Assert: due to validation, \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}[\href{../syntax/modules.html#syntax-funcidx}{\mathit{funcidx}}_{ij}]\) exists.

      4. Let the function element \(\href{../exec/runtime.html#syntax-funcelem}{\mathit{funcelem}}_{ij}\) be the function address \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}[\href{../syntax/modules.html#syntax-funcidx}{\mathit{funcidx}}_{ij}]\).

   2. Let \(\href{../exec/runtime.html#syntax-funcelem}{\mathit{funcelem}}^\ast_i\) be the concatenation of function elements \(\href{../exec/runtime.html#syntax-funcelem}{\mathit{funcelem}}_{ij}\) in order of index \(j\).

   3. Let \((\href{../exec/runtime.html#syntax-funcelem}{\mathit{funcelem}}^\ast)^\ast\) be the concatenation of function element vectors \(\href{../exec/runtime.html#syntax-funcelem}{\mathit{funcelem}}^\ast_i\) in order of index \(i\).

7. Let \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\) be a new module instance allocated from \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) in store \(S\) with imports \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^n\), global initializer values \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\), and element segment contents \((\href{../exec/runtime.html#syntax-funcelem}{\mathit{funcelem}}^\ast)^\ast\), and let \(S'\) be the extended store produced by module allocation.

8. Let \(F\) be the auxiliary frame \(\{ \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}, \href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\epsilon \}\).

9. Push the frame \(F\) to the stack.

10. For each element segment \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{elems}}\) whose mode is of the form \(\href{../syntax/modules.html#syntax-elem}{\mathsf{active}}~\{ \href{../syntax/modules.html#syntax-elem}{\mathsf{table}}~\href{../syntax/modules.html#syntax-tableidx}{\mathit{tableidx}}_i, \href{../syntax/modules.html#syntax-elem}{\mathsf{offset}}~\mathit{einstr}^\ast_i~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \}\), do:

    1. Assert: \(\href{../syntax/modules.html#syntax-tableidx}{\mathit{tableidx}}_i\) is \(0\).

    2. Let \(n\) be the length of the vector \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i.\href{../syntax/modules.html#syntax-elem}{\mathsf{init}}\).

    3. Execute the instruction sequence \(\mathit{einstr}^\ast_i\).

    4. Execute the instruction \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0\).

    5. Execute the instruction \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n\).

    6. Execute the instruction \(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.init}}~i\).

    7. Execute the instruction \(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{elem.drop}}~i\).

11. For each data segment \(\href{../syntax/modules.html#syntax-data}{\mathit{data}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{datas}}\) whose mode is of the form \(\href{../syntax/modules.html#syntax-data}{\mathsf{active}}~\{ \href{../syntax/modules.html#syntax-data}{\mathsf{memory}}~\href{../syntax/modules.html#syntax-memidx}{\mathit{memidx}}_i, \href{../syntax/modules.html#syntax-data}{\mathsf{offset}}~\mathit{dinstr}^\ast_i~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \}\), do:

    1. Assert: \(\href{../syntax/modules.html#syntax-memidx}{\mathit{memidx}}_i\) is \(0\).

    2. Let \(n\) be the length of the vector \(\href{../syntax/modules.html#syntax-data}{\mathit{data}}_i.\href{../syntax/modules.html#syntax-data}{\mathsf{init}}\).

    3. Execute the instruction sequence \(\mathit{dinstr}^\ast_i\).

    4. Execute the instruction \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0\).

    5. Execute the instruction \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n\).

    6. Execute the instruction \(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.init}}~i\).

    7. Execute the instruction \(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{data.drop}}~i\).

12. If the start function \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{start}}\) is not empty, then:

    1. Let \(\href{../syntax/modules.html#syntax-start}{\mathit{start}}\) be the start function \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{start}}\).

    2. Execute the instruction \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call}}~\href{../syntax/modules.html#syntax-start}{\mathit{start}}.\href{../syntax/modules.html#syntax-start}{\mathsf{func}}\).

13. Assert: due to validation, the frame \(F\) is now on the top of the stack.

14. Pop the frame \(F\) from the stack.

\[\begin{split}~\\ \begin{array}{@{}rcll} \href{../exec/modules.html#exec-instantiation}{\mathrm{instantiate}}(S, \href{../syntax/modules.html#syntax-module}{\mathit{module}}, \href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^k) &=& S'; F; \begin{array}[t]{@{}l@{}} \mathrm{runelem}_0(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}^n[0])~\dots~\mathrm{runelem}_{n-1}(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}^n[n-1]) \\ \mathrm{rundata}_0(\href{../syntax/modules.html#syntax-data}{\mathit{data}}^m[0])~\dots~\mathrm{rundata}_{m-1}(\href{../syntax/modules.html#syntax-data}{\mathit{data}}^m[m-1]) \\ (\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call}}~\href{../syntax/modules.html#syntax-start}{\mathit{start}}.\href{../syntax/modules.html#syntax-start}{\mathsf{func}})^? \\ \end{array} \\ &(\mathrel{\mbox{if}} & \href{../valid/modules.html#valid-module}{\vdash} \href{../syntax/modules.html#syntax-module}{\mathit{module}} : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_{\mathrm{im}}^k \href{../syntax/types.html#syntax-functype}{\rightarrow} \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_{\mathrm{ex}}^\ast \\ &\wedge& (S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathit{externval}} : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}})^k \\ &\wedge& (\href{../exec/modules.html#match-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}} \href{../exec/modules.html#match}{\leq} \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_{\mathrm{im}})^k \\[1ex] &\wedge& \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{globals}} = \href{../syntax/modules.html#syntax-global}{\mathit{global}}^\ast \\ &\wedge& \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{elems}} = \href{../syntax/modules.html#syntax-elem}{\mathit{elem}}^n \\ &\wedge& \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{datas}} = \href{../syntax/modules.html#syntax-data}{\mathit{data}}^m \\ &\wedge& \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{start}} = \href{../syntax/modules.html#syntax-start}{\mathit{start}}^? \\[1ex] &\wedge& S', \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}} = \href{../exec/modules.html#alloc-module}{\mathrm{allocmodule}}(S, \href{../syntax/modules.html#syntax-module}{\mathit{module}}, \href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^k, \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast) \\ &\wedge& F = \{ \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}, \href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\epsilon \} \\[1ex] &\wedge& (S'; F; \href{../syntax/modules.html#syntax-global}{\mathit{global}}.\href{../syntax/modules.html#syntax-global}{\mathsf{init}} \href{../exec/conventions.html#formal-notation}{\hookrightarrow}^\ast S'; F; \href{../exec/runtime.html#syntax-val}{\mathit{val}}~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}})^\ast \\ &\wedge& (S'; F; \href{../syntax/modules.html#syntax-elem}{\mathit{elem}}.\href{../syntax/modules.html#syntax-elem}{\mathsf{offset}} \href{../exec/conventions.html#formal-notation}{\hookrightarrow}^\ast S'; F; \href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\mathit{eo}~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}})^\ast \\ &\wedge& (S'; F; \href{../syntax/modules.html#syntax-data}{\mathit{data}}.\href{../syntax/modules.html#syntax-data}{\mathsf{offset}} \href{../exec/conventions.html#formal-notation}{\hookrightarrow}^\ast S'; F; \href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\mathit{do}~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}})^\ast \\[1ex] &\wedge& (\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}} = \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}.\href{../syntax/modules.html#syntax-elem}{\mathsf{table}}])^\ast \\ &\wedge& (\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}} = \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[\href{../syntax/modules.html#syntax-data}{\mathit{data}}.\href{../syntax/modules.html#syntax-data}{\mathsf{memory}}])^\ast \\ &\wedge& (\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} = \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}[\href{../syntax/modules.html#syntax-start}{\mathit{start}}.\href{../syntax/modules.html#syntax-start}{\mathsf{func}}])^?) \end{array}\end{split}\]

where:

\[\begin{split}\begin{array}{@{}l} \mathrm{runelem}_i(\{\href{../syntax/modules.html#syntax-elem}{\mathsf{type}}~\mathit{et}, \href{../syntax/modules.html#syntax-elem}{\mathsf{init}}~\href{../exec/runtime.html#syntax-funcelem}{\mathit{funcelem}}^n, \href{../syntax/modules.html#syntax-elem}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-elem}{\mathsf{passive}}\}) \quad=\quad \epsilon \\ \mathrm{runelem}_i(\{\href{../syntax/modules.html#syntax-elem}{\mathsf{type}}~\mathit{et}, \href{../syntax/modules.html#syntax-elem}{\mathsf{init}}~\href{../exec/runtime.html#syntax-funcelem}{\mathit{funcelem}}^n, \href{../syntax/modules.html#syntax-elem}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-elem}{\mathsf{active}} \{\href{../syntax/modules.html#syntax-elem}{\mathsf{table}}~0, \href{../syntax/modules.html#syntax-elem}{\mathsf{offset}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\}\}) \quad=\\ \qquad \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.init}}~i)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{elem.drop}}~i) \\[1ex] \mathrm{rundata}_i(\{\href{../syntax/modules.html#syntax-data}{\mathsf{init}}~b^n, DMODE~\href{../syntax/modules.html#syntax-data}{\mathsf{passive}}\}) \quad=\quad \epsilon \\ \mathrm{rundata}_i(\{\href{../syntax/modules.html#syntax-data}{\mathsf{init}}~b^n, DMODE~\href{../syntax/modules.html#syntax-data}{\mathsf{active}} \{\href{../syntax/modules.html#syntax-data}{\mathsf{memory}}~0, \href{../syntax/modules.html#syntax-data}{\mathsf{offset}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\}\}) \quad=\\ \qquad \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.init}}~i)~(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{data.drop}}~i) \\ \end{array}\end{split}\]

Note

Module allocation and the evaluation of global initializers are mutually recursive because the global initialization values \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\) are passed to the module allocator but depend on the store \(S'\) and module instance \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\) returned by allocation. However, this recursion is just a specification device. Due to validation, the initialization values can easily be determined from a simple pre-pass that evaluates global initializers in the initial store.

All failure conditions are checked before any observable mutation of the store takes place. Store mutation is not atomic; it happens in individual steps that may be interleaved with other threads.

Evaluation of constant expressions does not affect the store.

Invocation

Once a module has been instantiated, any exported function can be invoked externally via its function address \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}\) in the store \(S\) and an appropriate list \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\) of argument values.

Invocation may fail with an error if the arguments do not fit the function type. Invocation can also result in a trap. It is up to the embedder to define how such conditions are reported.

Note

If the embedder API performs type checks itself, either statically or dynamically, before performing an invocation, then no failure other than traps can occur.

The following steps are performed:

1. Assert: \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}]\) exists.

2. Let \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}\) be the function instance \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}]\).

3. Let \([t_1^n] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^m]\) be the function type \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}.\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}\).

4. If the length \(|\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast|\) of the provided argument values is different from the number \(n\) of expected arguments, then:

   1. Fail.

5. For each value type \(t_i\) in \(t_1^n\) and corresponding value \(val_i\) in \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\), do:

   1. If \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_i\) is not \(t_i.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_i\) for some \(c_i\), then:

      1. Fail.

6. Let \(F\) be the dummy frame \(\{ \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\{\}, \href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\epsilon \}\).

7. Push the frame \(F\) to the stack.

8. Push the values \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\) to the stack.

9. Invoke the function instance at address \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}\).

Once the function has returned, the following steps are executed:

1. Assert: due to validation, \(m\) values are on the top of the stack.

2. Pop \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_{\mathrm{res}}^m\) from the stack.

The values \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_{\mathrm{res}}^m\) are returned as the results of the invocation.

\[\begin{split}~\\[-1ex] \begin{array}{@{}lcl} \href{../exec/modules.html#exec-invocation}{\mathrm{invoke}}(S, \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}, \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n) &=& S; F; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n~(\href{../exec/runtime.html#syntax-invoke}{\mathsf{invoke}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}) \\ &(\mathrel{\mbox{if}} & S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}].\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}} = [t_1^n] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^m] \\ &\wedge& \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n = (t_1.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c)^n \\ &\wedge& F = \{ \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\{\}, \href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\epsilon \}) \\ \end{array}\end{split}\]