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.

Allocation¶

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

Functions ¶

\({\href{../exec/modules.html#alloc-func}{\mathrm{allocfunc}}}(s, {\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}, {{\href{../exec/runtime.html#syntax-funcinst}{\mathit{code}}}}, {\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}})\)¶

Let \({\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}}\) be the function instance \(\{ \begin{array}[t]{@{}l@{}}\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}},\; \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{../exec/runtime.html#syntax-funcinst}{\mathit{code}}}} \}\end{array}\).
Let \(a\) be the length of \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}\).
Append \({\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}}\) to \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}\).
Return \(a\).

\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}} {\href{../exec/modules.html#alloc-func}{\mathrm{allocfunc}}}(s, {\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}, {{\href{../exec/runtime.html#syntax-funcinst}{\mathit{code}}}}, {\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}) & = & (s \oplus \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}~{\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}} \}\end{array}, {|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}|}) & \\ \multicolumn{4}{@{}l@{}}{\quad \quad \mbox{if}~ {\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}} = \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}},\; \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{../exec/runtime.html#syntax-funcinst}{\mathit{code}}}} \}\end{array} } \\ \end{array}\end{split}\]

Tables ¶

\({\href{../exec/modules.html#alloc-table}{\mathrm{alloctable}}}(s, {\mathit{at}}~{}[ i \href{../syntax/types.html#syntax-limits}{\,{..}\,} j ]~{\mathit{rt}}, {\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}})\)¶

Let \({\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}}\) be the table instance \(\{ \begin{array}[t]{@{}l@{}}\href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}~({\mathit{at}}~{}[ i \href{../syntax/types.html#syntax-limits}{\,{..}\,} j ]~{\mathit{rt}}),\; \href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~{{\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}^{i}} \}\end{array}\).
Let \(a\) be the length of \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}\).
Append \({\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}}\) to \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}\).
Return \(a\).

\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}} {\href{../exec/modules.html#alloc-table}{\mathrm{alloctable}}}(s, {\mathit{at}}~{}[ i \href{../syntax/types.html#syntax-limits}{\,{..}\,} j ]~{\mathit{rt}}, {\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}) & = & (s \oplus \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-store}{\mathsf{tables}}~{\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}} \}\end{array}, {|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}|}) & \\ \multicolumn{4}{@{}l@{}}{\quad \quad \mbox{if}~ {\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}} = \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}~({\mathit{at}}~{}[ i \href{../syntax/types.html#syntax-limits}{\,{..}\,} j ]~{\mathit{rt}}),\; \href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~{{\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}^{i}} \}\end{array} } \\ \end{array}\end{split}\]

Memories ¶

\({\href{../exec/modules.html#alloc-mem}{\mathrm{allocmem}}}(s, {\mathit{at}}~{}[ i \href{../syntax/types.html#syntax-limits}{\,{..}\,} j ]~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}})\)¶

Let \({\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}}\) be the memory instance \(\{ \begin{array}[t]{@{}l@{}}\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}~({\mathit{at}}~{}[ i \href{../syntax/types.html#syntax-limits}{\,{..}\,} j ]~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}}),\; \href{../exec/runtime.html#syntax-meminst}{\mathsf{bytes}}~{\mathtt{0x00}^{i \cdot 64 \, {\mathrm{Ki}}}} \}\end{array}\).
Let \(a\) be the length of \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}\).
Append \({\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}}\) to \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}\).
Return \(a\).

\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}} {\href{../exec/modules.html#alloc-mem}{\mathrm{allocmem}}}(s, {\mathit{at}}~{}[ i \href{../syntax/types.html#syntax-limits}{\,{..}\,} j ]~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}}) & = & (s \oplus \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-store}{\mathsf{mems}}~{\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}} \}\end{array}, {|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}|}) & \\ \multicolumn{4}{@{}l@{}}{\quad \quad \mbox{if}~ {\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}} = \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}~({\mathit{at}}~{}[ i \href{../syntax/types.html#syntax-limits}{\,{..}\,} j ]~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}}),\; \href{../exec/runtime.html#syntax-meminst}{\mathsf{bytes}}~{(\mathtt{0x00})^{i \cdot 64 \, {\mathrm{Ki}}}} \}\end{array} } \\ \end{array}\end{split}\]

Tags ¶

\({\href{../exec/modules.html#alloc-tag}{\mathrm{alloctag}}}(s, {\href{../valid/conventions.html#syntax-tagtype}{\mathit{tagtype}}})\)¶

Let \({\href{../exec/runtime.html#syntax-taginst}{\mathit{taginst}}}\) be the tag instance \(\{ \begin{array}[t]{@{}l@{}}\href{../exec/runtime.html#syntax-taginst}{\mathsf{type}}~{\href{../valid/conventions.html#syntax-tagtype}{\mathit{tagtype}}} \}\end{array}\).
Let \(a\) be the length of \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{tags}}\).
Append \({\href{../exec/runtime.html#syntax-taginst}{\mathit{taginst}}}\) to \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{tags}}\).
Return \(a\).

\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}} {\href{../exec/modules.html#alloc-tag}{\mathrm{alloctag}}}(s, {\href{../valid/conventions.html#syntax-tagtype}{\mathit{tagtype}}}) & = & (s \oplus \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-store}{\mathsf{tags}}~{\href{../exec/runtime.html#syntax-taginst}{\mathit{taginst}}} \}\end{array}, {|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{tags}}|}) & \\ \multicolumn{4}{@{}l@{}}{\quad \quad \mbox{if}~ {\href{../exec/runtime.html#syntax-taginst}{\mathit{taginst}}} = \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-taginst}{\mathsf{type}}~{\href{../valid/conventions.html#syntax-tagtype}{\mathit{tagtype}}} \}\end{array} } \\ \end{array}\end{split}\]

Globals ¶

\({\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}}})\)¶

Let \({\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}}\) be the global instance \(\{ \begin{array}[t]{@{}l@{}}\href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}}~{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}},\; \href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}~{\href{../exec/runtime.html#syntax-val}{\mathit{val}}} \}\end{array}\).
Let \(a\) be the length of \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}\).
Append \({\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}}\) to \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}\).
Return \(a\).

\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}} {\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 \oplus \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-store}{\mathsf{globals}}~{\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}} \}\end{array}, {|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}|}) & \\ \multicolumn{4}{@{}l@{}}{\quad \quad \mbox{if}~ {\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}} = \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}}~{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}},\; \href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}~{\href{../exec/runtime.html#syntax-val}{\mathit{val}}} \}\end{array} } \\ \end{array}\end{split}\]

Element segments ¶

\({\href{../exec/modules.html#alloc-elem}{\mathrm{allocelem}}}(s, {\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}}, {{\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}^\ast})\)¶

Let \({\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}}\) be the element instance \(\{ \begin{array}[t]{@{}l@{}}\href{../exec/runtime.html#syntax-eleminst}{\mathsf{type}}~{\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}},\; \href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}}~{{\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}^\ast} \}\end{array}\).
Let \(a\) be the length of \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}\).
Append \({\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}}\) to \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}\).
Return \(a\).

\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}} {\href{../exec/modules.html#alloc-elem}{\mathrm{allocelem}}}(s, {\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}}, {{\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}^\ast}) & = & (s \oplus \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-store}{\mathsf{elems}}~{\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}} \}\end{array}, {|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}|}) & \\ \multicolumn{4}{@{}l@{}}{\quad \quad \mbox{if}~ {\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}} = \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-eleminst}{\mathsf{type}}~{\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}},\; \href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}}~{{\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}^\ast} \}\end{array} } \\ \end{array}\end{split}\]

Data segments ¶

\({\href{../exec/modules.html#alloc-data}{\mathrm{allocdata}}}(s, \href{../valid/modules.html#valid-data}{\mathsf{ok}}, {{\href{../syntax/values.html#syntax-byte}{\mathit{byte}}}^\ast})\)¶

Let \({\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}}\) be the data instance \(\{ \begin{array}[t]{@{}l@{}}\href{../exec/runtime.html#syntax-datainst}{\mathsf{bytes}}~{{\href{../syntax/values.html#syntax-byte}{\mathit{byte}}}^\ast} \}\end{array}\).
Let \(a\) be the length of \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}\).
Append \({\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}}\) to \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}\).
Return \(a\).

\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}} {\href{../exec/modules.html#alloc-data}{\mathrm{allocdata}}}(s, \href{../valid/modules.html#valid-data}{\mathsf{ok}}, {{\href{../syntax/values.html#syntax-byte}{\mathit{byte}}}^\ast}) & = & (s \oplus \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-store}{\mathsf{datas}}~{\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}} \}\end{array}, {|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}|}) & \\ \multicolumn{4}{@{}l@{}}{\quad \quad \mbox{if}~ {\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}} = \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-datainst}{\mathsf{bytes}}~{{\href{../syntax/values.html#syntax-byte}{\mathit{byte}}}^\ast} \}\end{array} } \\ \end{array}\end{split}\]

Growing tables ¶

\({\href{../exec/modules.html#grow-table}{\mathrm{growtable}}}({\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}}, n, r)\)¶

Let \(\{ \begin{array}[t]{@{}l@{}}\href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}~({\mathit{at}}~{}[ i \href{../syntax/types.html#syntax-limits}{\,{..}\,} j ]~{\mathit{rt}}),\; \href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~{{r'}^\ast} \}\end{array}\) be the destructuring of \({\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}}\).
If \({|{{r'}^\ast}|} + n > j\), then:
1. Fail.
Let \({i'}\) be \({|{{r'}^\ast}|} + n\).
Let \({\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}'}\) be the table instance \(\{ \begin{array}[t]{@{}l@{}}\href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}~({\mathit{at}}~{}[ {i'} \href{../syntax/types.html#syntax-limits}{\,{..}\,} j ]~{\mathit{rt}}),\; \href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~{{r'}^\ast}~{r^{n}} \}\end{array}\).
Return \({\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}'}\).

\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}} {\href{../exec/modules.html#grow-table}{\mathrm{growtable}}}({\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}}, n, r) & = & {\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}'} & \quad \begin{array}[t]{@{}l@{}} \mbox{if}~ {\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}} = \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}~({\mathit{at}}~{}[ i \href{../syntax/types.html#syntax-limits}{\,{..}\,} j ]~{\mathit{rt}}),\; \href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~{{r'}^\ast} \}\end{array} \\ {\land}~ {\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}'} = \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}~({\mathit{at}}~{}[ {i'} \href{../syntax/types.html#syntax-limits}{\,{..}\,} j ]~{\mathit{rt}}),\; \href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~{{r'}^\ast}~{r^{n}} \}\end{array} \\ {\land}~ {i'} = {|{{r'}^\ast}|} + n \leq j \\ \end{array} \\ \end{array}\end{split}\]

Growing memories ¶

\({\href{../exec/modules.html#grow-mem}{\mathrm{growmem}}}({\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}}, n)\)¶

Let \(\{ \begin{array}[t]{@{}l@{}}\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}~({\mathit{at}}~{}[ i \href{../syntax/types.html#syntax-limits}{\,{..}\,} j ]~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}}),\; \href{../exec/runtime.html#syntax-meminst}{\mathsf{bytes}}~{b^\ast} \}\end{array}\) be the destructuring of \({\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}}\).
If \({|{b^\ast}|} / (64 \, {\mathrm{Ki}}) + n > j\), then:
1. Fail.
Let \({i'}\) be \({|{b^\ast}|} / (64 \, {\mathrm{Ki}}) + n\).
Let \({\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}'}\) be the memory instance \(\{ \begin{array}[t]{@{}l@{}}\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}~({\mathit{at}}~{}[ {i'} \href{../syntax/types.html#syntax-limits}{\,{..}\,} j ]~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}}),\; \href{../exec/runtime.html#syntax-meminst}{\mathsf{bytes}}~{b^\ast}~{\mathtt{0x00}^{n \cdot 64 \, {\mathrm{Ki}}}} \}\end{array}\).
Return \({\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}'}\).

\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}} {\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}}'} & \quad \begin{array}[t]{@{}l@{}} \mbox{if}~ {\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}} = \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}~({\mathit{at}}~{}[ i \href{../syntax/types.html#syntax-limits}{\,{..}\,} j ]~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}}),\; \href{../exec/runtime.html#syntax-meminst}{\mathsf{bytes}}~{b^\ast} \}\end{array} \\ {\land}~ {\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}'} = \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}~({\mathit{at}}~{}[ {i'} \href{../syntax/types.html#syntax-limits}{\,{..}\,} j ]~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}}),\; \href{../exec/runtime.html#syntax-meminst}{\mathsf{bytes}}~{b^\ast}~{(\mathtt{0x00})^{n \cdot 64 \, {\mathrm{Ki}}}} \}\end{array} \\ {\land}~ {i'} = {|{b^\ast}|} / (64 \, {\mathrm{Ki}}) + n \leq j \\ \end{array} \\ \end{array}\end{split}\]

Modules ¶

\({\href{../exec/modules.html#alloc-module}{\mathrm{allocmodule}}}(s, {\href{../syntax/modules.html#syntax-module}{\mathit{module}}}, {{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast}, {{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}_{\mathsf{g}}^\ast}, {{\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}_{\mathsf{t}}^\ast}, {{{\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}_{\mathsf{e}}^\ast}^\ast})\)¶

Let \((\href{../syntax/modules.html#syntax-module}{\mathsf{module}}~{{\href{../syntax/types.html#syntax-rectype}{\mathit{type}}}^\ast}~{{\href{../syntax/modules.html#syntax-import}{\mathit{import}}}^\ast}~{{\href{../syntax/modules.html#syntax-func}{\mathit{func}}}^\ast}~{{\href{../syntax/modules.html#syntax-global}{\mathit{global}}}^\ast}~{{\href{../syntax/modules.html#syntax-table}{\mathit{table}}}^\ast}~{{\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}}^\ast}~{{\href{../syntax/modules.html#syntax-tag}{\mathit{tag}}}^\ast}~{{\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}}^\ast}~{{\href{../syntax/modules.html#syntax-data}{\mathit{data}}}^\ast}~{{\href{../syntax/modules.html#syntax-start}{\mathit{start}}}^?}~{{\href{../syntax/modules.html#syntax-export}{\mathit{export}}}^\ast})\) be the destructuring of \({\href{../syntax/modules.html#syntax-module}{\mathit{module}}}\).
Let \({{\mathit{fa}}_{\mathsf{i}}^\ast}\) be \({\href{../exec/runtime.html#syntax-externaddr}{\mathrm{funcs}}}({{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast})\).
Let \({{\mathit{ga}}_{\mathsf{i}}^\ast}\) be \({\href{../exec/runtime.html#syntax-externaddr}{\mathrm{globals}}}({{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast})\).
Let \({{\mathit{aa}}_{\mathsf{i}}^\ast}\) be \({\href{../exec/runtime.html#syntax-externaddr}{\mathrm{tags}}}({{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast})\).
Let \({{\mathit{ma}}_{\mathsf{i}}^\ast}\) be \({\href{../exec/runtime.html#syntax-externaddr}{\mathrm{mems}}}({{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast})\).
Let \({{\mathit{ta}}_{\mathsf{i}}^\ast}\) be \({\href{../exec/runtime.html#syntax-externaddr}{\mathrm{tables}}}({{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast})\).
Let \({{\mathit{fa}}^\ast}\) be \({|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}|} + i_{\mathsf{f}}\) for all \(i_{\mathsf{f}}\) from \(0\) to \({|{{\href{../syntax/modules.html#syntax-func}{\mathit{func}}}^\ast}|} - 1\).
Let \({{\mathit{ga}}^\ast}\) be \({|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}|} + i_{\mathsf{g}}\) for all \(i_{\mathsf{g}}\) from \(0\) to \({|{{\href{../syntax/modules.html#syntax-global}{\mathit{global}}}^\ast}|} - 1\).
Let \({{\mathit{ta}}^\ast}\) be \({|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}|} + i_{\mathsf{t}}\) for all \(i_{\mathsf{t}}\) from \(0\) to \({|{{\href{../syntax/modules.html#syntax-table}{\mathit{table}}}^\ast}|} - 1\).
Let \({{\mathit{aa}}^\ast}\) be \({|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{tags}}|} + i_{\mathsf{a}}\) for all \(i_{\mathsf{a}}\) from \(0\) to \({|{{\href{../syntax/modules.html#syntax-tag}{\mathit{tag}}}^\ast}|} - 1\).
Let \({{\mathit{ma}}^\ast}\) be \({|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}|} + i_{\mathsf{m}}\) for all \(i_{\mathsf{m}}\) from \(0\) to \({|{{\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}}^\ast}|} - 1\).
Let \({{\mathit{ea}}^\ast}\) be \({|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}|} + i_{\mathsf{e}}\) for all \(i_{\mathsf{e}}\) from \(0\) to \({|{{\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}}^\ast}|} - 1\).
Let \({{\mathit{da}}^\ast}\) be \({|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}|} + i_{\mathsf{d}}\) for all \(i_{\mathsf{d}}\) from \(0\) to \({|{{\href{../syntax/modules.html#syntax-data}{\mathit{data}}}^\ast}|} - 1\).
Let \({(\href{../syntax/modules.html#syntax-mem}{\mathsf{memory}}~{\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}})^\ast}\) be \({{\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}}^\ast}\).
Let \({{\mathit{dt}}^\ast}\) be \({{{\href{../exec/modules.html#alloc-type}{\mathrm{alloctype}}}^\ast}}{({{\href{../syntax/types.html#syntax-rectype}{\mathit{type}}}^\ast})}\).
Let \({(\href{../syntax/modules.html#syntax-tag}{\mathsf{tag}}~y)^\ast}\) be \({{\href{../syntax/modules.html#syntax-tag}{\mathit{tag}}}^\ast}\).
Let \({(\href{../syntax/modules.html#syntax-data}{\mathsf{data}}~{{\href{../syntax/values.html#syntax-byte}{\mathit{byte}}}^\ast}~{\href{../syntax/modules.html#syntax-datamode}{\mathit{datamode}}})^\ast}\) be \({{\href{../syntax/modules.html#syntax-data}{\mathit{data}}}^\ast}\).
Let \({(\href{../syntax/modules.html#syntax-global}{\mathsf{global}}~{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}~{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}_{\mathsf{g}})^\ast}\) be \({{\href{../syntax/modules.html#syntax-global}{\mathit{global}}}^\ast}\).
Let \({(\href{../syntax/modules.html#syntax-table}{\mathsf{table}}~{\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}}~{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}_{\mathsf{t}})^\ast}\) be \({{\href{../syntax/modules.html#syntax-table}{\mathit{table}}}^\ast}\).
Let \({(\href{../syntax/modules.html#syntax-elem}{\mathsf{elem}}~{\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}}~{{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}_{\mathsf{e}}^\ast}~{\href{../syntax/modules.html#syntax-elemmode}{\mathit{elemmode}}})^\ast}\) be \({{\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}}^\ast}\).
Let \({(\href{../syntax/modules.html#syntax-func}{\mathsf{func}}~x~{{\href{../syntax/modules.html#syntax-local}{\mathit{local}}}^\ast}~{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}_{\mathsf{f}})^\ast}\) be \({{\href{../syntax/modules.html#syntax-func}{\mathit{func}}}^\ast}\).
Let \({{\mathit{xi}}^\ast}\) be \({{{\href{../exec/modules.html#alloc-export}{\mathrm{allocexport}}}^\ast}}{(\{ \begin{array}[t]{@{}l@{}}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcs}}~{{\mathit{fa}}_{\mathsf{i}}^\ast}~{{\mathit{fa}}^\ast},\; \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globals}}~{{\mathit{ga}}_{\mathsf{i}}^\ast}~{{\mathit{ga}}^\ast},\; \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tables}}~{{\mathit{ta}}_{\mathsf{i}}^\ast}~{{\mathit{ta}}^\ast},\; \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{mems}}~{{\mathit{ma}}_{\mathsf{i}}^\ast}~{{\mathit{ma}}^\ast},\; \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tags}}~{{\mathit{aa}}_{\mathsf{i}}^\ast}~{{\mathit{aa}}^\ast} \}\end{array}, {{\href{../syntax/modules.html#syntax-export}{\mathit{export}}}^\ast})}\).
Let \({\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}\) be the module instance \(\{ \begin{array}[t]{@{}l@{}}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}~{{\mathit{dt}}^\ast},\; \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcs}}~{{\mathit{fa}}_{\mathsf{i}}^\ast}~{{\mathit{fa}}^\ast},\; \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globals}}~{{\mathit{ga}}_{\mathsf{i}}^\ast}~{{\mathit{ga}}^\ast},\; \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tables}}~{{\mathit{ta}}_{\mathsf{i}}^\ast}~{{\mathit{ta}}^\ast},\; \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{mems}}~{{\mathit{ma}}_{\mathsf{i}}^\ast}~{{\mathit{ma}}^\ast},\; \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tags}}~{{\mathit{aa}}_{\mathsf{i}}^\ast}~{{\mathit{aa}}^\ast},\; \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{elems}}~{{\mathit{ea}}^\ast},\; \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{datas}}~{{\mathit{da}}^\ast},\; \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{exports}}~{{\mathit{xi}}^\ast} \}\end{array}\).
Let \({{\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}}_0^\ast}\) be \({{{\href{../exec/modules.html#alloc-func}{\mathrm{allocfunc}}}^\ast}}{(s, {{{\mathit{dt}}^\ast}{}[x]^\ast}, {(\href{../syntax/modules.html#syntax-func}{\mathsf{func}}~x~{{\href{../syntax/modules.html#syntax-local}{\mathit{local}}}^\ast}~{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}_{\mathsf{f}})^\ast}, {{\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}^{{|{{\href{../syntax/modules.html#syntax-func}{\mathit{func}}}^\ast}|}}})}\).
Assert: Due to validation, \({{\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}}_0^\ast} = {{\mathit{fa}}^\ast}\).
Let \({{\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}}_0^\ast}\) be \({{{\href{../exec/modules.html#alloc-global}{\mathrm{allocglobal}}}^\ast}}{(s, {{{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}}{{}[ {\href{../valid/conventions.html#notation-subst}{\mathrel{:=}}}\, {{\mathit{dt}}^\ast} ]}^\ast}, {{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}_{\mathsf{g}}^\ast})}\).
Assert: Due to validation, \({{\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}}_0^\ast} = {{\mathit{ga}}^\ast}\).
Let \({{\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}}_0^\ast}\) be \({{{\href{../exec/modules.html#alloc-table}{\mathrm{alloctable}}}^\ast}}{(s, {{{\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}}}{{}[ {\href{../valid/conventions.html#notation-subst}{\mathrel{:=}}}\, {{\mathit{dt}}^\ast} ]}^\ast}, {{\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}_{\mathsf{t}}^\ast})}\).
Assert: Due to validation, \({{\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}}_0^\ast} = {{\mathit{ta}}^\ast}\).
Let \({{\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}}_0^\ast}\) be \({{{\href{../exec/modules.html#alloc-mem}{\mathrm{allocmem}}}^\ast}}{(s, {{{\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}}}{{}[ {\href{../valid/conventions.html#notation-subst}{\mathrel{:=}}}\, {{\mathit{dt}}^\ast} ]}^\ast})}\).
Assert: Due to validation, \({{\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}}_0^\ast} = {{\mathit{ma}}^\ast}\).
Let \({{\href{../exec/runtime.html#syntax-tagaddr}{\mathit{tagaddr}}}_0^\ast}\) be \({{{\href{../exec/modules.html#alloc-tag}{\mathrm{alloctag}}}^\ast}}{(s, {{{\mathit{dt}}^\ast}{}[y]^\ast})}\).
Assert: Due to validation, \({{\href{../exec/runtime.html#syntax-tagaddr}{\mathit{tagaddr}}}_0^\ast} = {{\mathit{aa}}^\ast}\).
Let \({{\href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}}_0^\ast}\) be \({{{\href{../exec/modules.html#alloc-elem}{\mathrm{allocelem}}}^\ast}}{(s, {{{\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}}}{{}[ {\href{../valid/conventions.html#notation-subst}{\mathrel{:=}}}\, {{\mathit{dt}}^\ast} ]}^\ast}, {{{\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}_{\mathsf{e}}^\ast}^\ast})}\).
Assert: Due to validation, \({{\href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}}_0^\ast} = {{\mathit{ea}}^\ast}\).
Let \({{\href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}}_0^\ast}\) be \({{{\href{../exec/modules.html#alloc-data}{\mathrm{allocdata}}}^\ast}}{(s, {\href{../valid/modules.html#valid-data}{\mathsf{ok}}^{{|{{\href{../syntax/modules.html#syntax-data}{\mathit{data}}}^\ast}|}}}, {{{\href{../syntax/values.html#syntax-byte}{\mathit{byte}}}^\ast}^\ast})}\).
Assert: Due to validation, \({{\href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}}_0^\ast} = {{\mathit{da}}^\ast}\).
Return \({\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}\).

\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}} {\href{../exec/modules.html#alloc-module}{\mathrm{allocmodule}}}(s, {\href{../syntax/modules.html#syntax-module}{\mathit{module}}}, {{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast}, {{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}_{\mathsf{g}}^\ast}, {{\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}_{\mathsf{t}}^\ast}, {({{\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}_{\mathsf{e}}^\ast})^\ast}) & = & (s_7, {\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}) & \\ \multicolumn{4}{@{}l@{}}{\quad \quad \begin{array}[t]{@{}l@{}} \mbox{if}~ {\href{../syntax/modules.html#syntax-module}{\mathit{module}}} = \href{../syntax/modules.html#syntax-module}{\mathsf{module}}~{{\href{../syntax/types.html#syntax-rectype}{\mathit{type}}}^\ast}~{{\href{../syntax/modules.html#syntax-import}{\mathit{import}}}^\ast}~{{\href{../syntax/modules.html#syntax-func}{\mathit{func}}}^\ast}~{{\href{../syntax/modules.html#syntax-global}{\mathit{global}}}^\ast}~{{\href{../syntax/modules.html#syntax-table}{\mathit{table}}}^\ast}~{{\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}}^\ast}~{{\href{../syntax/modules.html#syntax-tag}{\mathit{tag}}}^\ast}~{{\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}}^\ast}~{{\href{../syntax/modules.html#syntax-data}{\mathit{data}}}^\ast}~{{\href{../syntax/modules.html#syntax-start}{\mathit{start}}}^?}~{{\href{../syntax/modules.html#syntax-export}{\mathit{export}}}^\ast} \\ {\land}~ {{\href{../syntax/modules.html#syntax-func}{\mathit{func}}}^\ast} = {(\href{../syntax/modules.html#syntax-func}{\mathsf{func}}~x~{{\href{../syntax/modules.html#syntax-local}{\mathit{local}}}^\ast}~{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}_{\mathsf{f}})^\ast} \\ {\land}~ {{\href{../syntax/modules.html#syntax-global}{\mathit{global}}}^\ast} = {(\href{../syntax/modules.html#syntax-global}{\mathsf{global}}~{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}~{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}_{\mathsf{g}})^\ast} \\ {\land}~ {{\href{../syntax/modules.html#syntax-table}{\mathit{table}}}^\ast} = {(\href{../syntax/modules.html#syntax-table}{\mathsf{table}}~{\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}}~{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}_{\mathsf{t}})^\ast} \\ {\land}~ {{\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}}^\ast} = {(\href{../syntax/modules.html#syntax-mem}{\mathsf{memory}}~{\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}})^\ast} \\ {\land}~ {{\href{../syntax/modules.html#syntax-tag}{\mathit{tag}}}^\ast} = {(\href{../syntax/modules.html#syntax-tag}{\mathsf{tag}}~y)^\ast} \\ {\land}~ {{\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}}^\ast} = {(\href{../syntax/modules.html#syntax-elem}{\mathsf{elem}}~{\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}}~{{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}_{\mathsf{e}}^\ast}~{\href{../syntax/modules.html#syntax-elemmode}{\mathit{elemmode}}})^\ast} \\ {\land}~ {{\href{../syntax/modules.html#syntax-data}{\mathit{data}}}^\ast} = {(\href{../syntax/modules.html#syntax-data}{\mathsf{data}}~{{\href{../syntax/values.html#syntax-byte}{\mathit{byte}}}^\ast}~{\href{../syntax/modules.html#syntax-datamode}{\mathit{datamode}}})^\ast} \\ {\land}~ {{\mathit{fa}}_{\mathsf{i}}^\ast} = {\href{../exec/runtime.html#syntax-externaddr}{\mathrm{funcs}}}({{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast}) \\ {\land}~ {{\mathit{ga}}_{\mathsf{i}}^\ast} = {\href{../exec/runtime.html#syntax-externaddr}{\mathrm{globals}}}({{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast}) \\ {\land}~ {{\mathit{ta}}_{\mathsf{i}}^\ast} = {\href{../exec/runtime.html#syntax-externaddr}{\mathrm{tables}}}({{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast}) \\ {\land}~ {{\mathit{ma}}_{\mathsf{i}}^\ast} = {\href{../exec/runtime.html#syntax-externaddr}{\mathrm{mems}}}({{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast}) \\ {\land}~ {{\mathit{aa}}_{\mathsf{i}}^\ast} = {\href{../exec/runtime.html#syntax-externaddr}{\mathrm{tags}}}({{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast}) \\ {\land}~ {{\mathit{fa}}^\ast} = {({|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}|} + i_{\mathsf{f}})^{i_{\mathsf{f}}<{|{{\href{../syntax/modules.html#syntax-func}{\mathit{func}}}^\ast}|}}} \\ {\land}~ {{\mathit{ga}}^\ast} = {({|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}|} + i_{\mathsf{g}})^{i_{\mathsf{g}}<{|{{\href{../syntax/modules.html#syntax-global}{\mathit{global}}}^\ast}|}}} \\ {\land}~ {{\mathit{ta}}^\ast} = {({|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}|} + i_{\mathsf{t}})^{i_{\mathsf{t}}<{|{{\href{../syntax/modules.html#syntax-table}{\mathit{table}}}^\ast}|}}} \\ {\land}~ {{\mathit{aa}}^\ast} = {({|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{tags}}|} + i_{\mathsf{a}})^{i_{\mathsf{a}}<{|{{\href{../syntax/modules.html#syntax-tag}{\mathit{tag}}}^\ast}|}}} \\ {\land}~ {{\mathit{ma}}^\ast} = {({|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}|} + i_{\mathsf{m}})^{i_{\mathsf{m}}<{|{{\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}}^\ast}|}}} \\ {\land}~ {{\mathit{ea}}^\ast} = {({|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}|} + i_{\mathsf{e}})^{i_{\mathsf{e}}<{|{{\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}}^\ast}|}}} \\ {\land}~ {{\mathit{da}}^\ast} = {({|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}|} + i_{\mathsf{d}})^{i_{\mathsf{d}}<{|{{\href{../syntax/modules.html#syntax-data}{\mathit{data}}}^\ast}|}}} \\ {\land}~ {{\mathit{dt}}^\ast} = {{{\href{../exec/modules.html#alloc-type}{\mathrm{alloctype}}}^\ast}}{({{\href{../syntax/types.html#syntax-rectype}{\mathit{type}}}^\ast})} \\ {\land}~ (s_1, {{\mathit{fa}}^\ast}) = {{{\href{../exec/modules.html#alloc-func}{\mathrm{allocfunc}}}^\ast}}{(s, {{{\mathit{dt}}^\ast}{}[x]^\ast}, {(\href{../syntax/modules.html#syntax-func}{\mathsf{func}}~x~{{\href{../syntax/modules.html#syntax-local}{\mathit{local}}}^\ast}~{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}_{\mathsf{f}})^\ast}, {{\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}^{{|{{\href{../syntax/modules.html#syntax-func}{\mathit{func}}}^\ast}|}}})} \\ {\land}~ (s_2, {{\mathit{ga}}^\ast}) = {{{\href{../exec/modules.html#alloc-global}{\mathrm{allocglobal}}}^\ast}}{(s_1, {{{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}}{{}[ {\href{../valid/conventions.html#notation-subst}{\mathrel{:=}}}\, {{\mathit{dt}}^\ast} ]}^\ast}, {{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}_{\mathsf{g}}^\ast})} \\ {\land}~ (s_3, {{\mathit{ta}}^\ast}) = {{{\href{../exec/modules.html#alloc-table}{\mathrm{alloctable}}}^\ast}}{(s_2, {{{\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}}}{{}[ {\href{../valid/conventions.html#notation-subst}{\mathrel{:=}}}\, {{\mathit{dt}}^\ast} ]}^\ast}, {{\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}_{\mathsf{t}}^\ast})} \\ {\land}~ (s_4, {{\mathit{ma}}^\ast}) = {{{\href{../exec/modules.html#alloc-mem}{\mathrm{allocmem}}}^\ast}}{(s_3, {{{\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}}}{{}[ {\href{../valid/conventions.html#notation-subst}{\mathrel{:=}}}\, {{\mathit{dt}}^\ast} ]}^\ast})} \\ {\land}~ (s_5, {{\mathit{aa}}^\ast}) = {{{\href{../exec/modules.html#alloc-tag}{\mathrm{alloctag}}}^\ast}}{(s_4, {{{\mathit{dt}}^\ast}{}[y]^\ast})} \\ {\land}~ (s_6, {{\mathit{ea}}^\ast}) = {{{\href{../exec/modules.html#alloc-elem}{\mathrm{allocelem}}}^\ast}}{(s_5, {{{\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}}}{{}[ {\href{../valid/conventions.html#notation-subst}{\mathrel{:=}}}\, {{\mathit{dt}}^\ast} ]}^\ast}, {({{\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}_{\mathsf{e}}^\ast})^\ast})} \\ {\land}~ (s_7, {{\mathit{da}}^\ast}) = {{{\href{../exec/modules.html#alloc-data}{\mathrm{allocdata}}}^\ast}}{(s_6, {\href{../valid/modules.html#valid-data}{\mathsf{ok}}^{{|{{\href{../syntax/modules.html#syntax-data}{\mathit{data}}}^\ast}|}}}, {({{\href{../syntax/values.html#syntax-byte}{\mathit{byte}}}^\ast})^\ast})} \\ {\land}~ {{\mathit{xi}}^\ast} = {{{\href{../exec/modules.html#alloc-export}{\mathrm{allocexport}}}^\ast}}{(\{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcs}}~{{\mathit{fa}}_{\mathsf{i}}^\ast}~{{\mathit{fa}}^\ast},\; \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globals}}~{{\mathit{ga}}_{\mathsf{i}}^\ast}~{{\mathit{ga}}^\ast},\; \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tables}}~{{\mathit{ta}}_{\mathsf{i}}^\ast}~{{\mathit{ta}}^\ast},\; \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{mems}}~{{\mathit{ma}}_{\mathsf{i}}^\ast}~{{\mathit{ma}}^\ast},\; \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tags}}~{{\mathit{aa}}_{\mathsf{i}}^\ast}~{{\mathit{aa}}^\ast} \}\end{array}, {{\href{../syntax/modules.html#syntax-export}{\mathit{export}}}^\ast})} \\ {\land}~ {\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}} = \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}~{{\mathit{dt}}^\ast},\; \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcs}}~{{\mathit{fa}}_{\mathsf{i}}^\ast}~{{\mathit{fa}}^\ast},\; \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globals}}~{{\mathit{ga}}_{\mathsf{i}}^\ast}~{{\mathit{ga}}^\ast},\; \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tables}}~{{\mathit{ta}}_{\mathsf{i}}^\ast}~{{\mathit{ta}}^\ast},\; \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{mems}}~{{\mathit{ma}}_{\mathsf{i}}^\ast}~{{\mathit{ma}}^\ast},\; \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tags}}~{{\mathit{aa}}_{\mathsf{i}}^\ast}~{{\mathit{aa}}^\ast},\; \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{elems}}~{{\mathit{ea}}^\ast},\; \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{datas}}~{{\mathit{da}}^\ast},\; \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{exports}}~{{\mathit{xi}}^\ast} \}\end{array} \\ \end{array} } \\ \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}[t]{@{}lcl@{}l@{}} {{{\mathrm{allocX}}^\ast}}{(s, \epsilon, \epsilon)} & = & (s, \epsilon) \\ {{{\mathrm{allocX}}^\ast}}{(s, X~{{X'}^\ast}, Y~{{Y'}^\ast})} & = & (s_2, a~{{a'}^\ast}) & \quad \begin{array}[t]{@{}l@{}} \mbox{if}~ (s_1, a) = {\mathrm{allocX}}(X, Y, s, X, Y) \\ {\land}~ (s_2, {{a'}^\ast}) = {{{\mathrm{allocX}}^\ast}}{(s_1, {{X'}^\ast}, {{Y'}^\ast})} \\ \end{array} \\ \end{array}\end{split}\]

For types, however, allocation is defined in terms of rolling and substitution of all preceding types to produce a list of closed defined types:

\({{{\href{../exec/modules.html#alloc-type}{\mathrm{alloctype}}}^\ast}}{({{\href{../syntax/types.html#syntax-rectype}{\mathit{type}}''}^\ast})}\)¶

If \({{\href{../syntax/types.html#syntax-rectype}{\mathit{type}}''}^\ast} = \epsilon\), then:
1. Return \(\epsilon\).
Let \({{\href{../syntax/types.html#syntax-rectype}{\mathit{type}}'}^\ast}~{\href{../syntax/types.html#syntax-rectype}{\mathit{type}}}\) be \({{\href{../syntax/types.html#syntax-rectype}{\mathit{type}}''}^\ast}\).
Let \((\href{../syntax/modules.html#syntax-type}{\mathsf{type}}~{\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}})\) be the destructuring of \({\href{../syntax/types.html#syntax-rectype}{\mathit{type}}}\).
Let \({{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}'}^\ast}\) be \({{{\href{../exec/modules.html#alloc-type}{\mathrm{alloctype}}}^\ast}}{({{\href{../syntax/types.html#syntax-rectype}{\mathit{type}}'}^\ast})}\).
Let \(x\) be the length of \({{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}'}^\ast}\).
Let \({{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}^\ast}\) be \({{{{{\href{../valid/conventions.html#aux-roll-deftype}{\mathrm{roll}}}}_{x}^\ast}}{({\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}})}}{{}[ {\href{../valid/conventions.html#notation-subst}{\mathrel{:=}}}\, {{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}'}^\ast} ]}\).
Return \({{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}'}^\ast}~{{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}^\ast}\).

\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}} {{{\href{../exec/modules.html#alloc-type}{\mathrm{alloctype}}}^\ast}}{(\epsilon)} & = & \epsilon \\ {{{\href{../exec/modules.html#alloc-type}{\mathrm{alloctype}}}^\ast}}{({{\href{../syntax/types.html#syntax-rectype}{\mathit{type}}'}^\ast}~{\href{../syntax/types.html#syntax-rectype}{\mathit{type}}})} & = & {{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}'}^\ast}~{{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}^\ast} & \quad \begin{array}[t]{@{}l@{}} \mbox{if}~ {{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}'}^\ast} = {{{\href{../exec/modules.html#alloc-type}{\mathrm{alloctype}}}^\ast}}{({{\href{../syntax/types.html#syntax-rectype}{\mathit{type}}'}^\ast})} \\ {\land}~ {\href{../syntax/types.html#syntax-rectype}{\mathit{type}}} = \href{../syntax/modules.html#syntax-type}{\mathsf{type}}~{\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}} \\ {\land}~ {{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}^\ast} = {{{{{\href{../valid/conventions.html#aux-roll-deftype}{\mathrm{roll}}}}_{x}^\ast}}{({\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}})}}{{}[ {\href{../valid/conventions.html#notation-subst}{\mathrel{:=}}}\, {{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}'}^\ast} ]} \\ {\land}~ x = {|{{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}'}^\ast}|} \\ \end{array} \\ \end{array}\end{split}\]

Finally, export instances are produced with the help of the following definition:

\({\href{../exec/modules.html#alloc-export}{\mathrm{allocexport}}}({\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}, \href{../syntax/modules.html#syntax-export}{\mathsf{export}}~{\href{../syntax/values.html#syntax-name}{\mathit{name}}}~{\href{../syntax/modules.html#syntax-externidx}{\mathit{externidx}}})\)¶

If \({\href{../syntax/modules.html#syntax-externidx}{\mathit{externidx}}}\) is some \(\href{../syntax/modules.html#syntax-externidx}{\mathsf{func}}\) \({\href{../syntax/modules.html#syntax-funcidx}{\mathit{funcidx}}}\), then:
1. Let \((\href{../syntax/modules.html#syntax-externidx}{\mathsf{func}}~x)\) be the destructuring of \({\href{../syntax/modules.html#syntax-externidx}{\mathit{externidx}}}\).
2. Return \(\{ \begin{array}[t]{@{}l@{}}\href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}~{\href{../syntax/values.html#syntax-name}{\mathit{name}}},\; \href{../exec/runtime.html#syntax-exportinst}{\mathsf{addr}}~(\href{../exec/runtime.html#syntax-externaddr}{\mathsf{func}}~{\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}{.}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcs}}{}[x]) \}\end{array}\).
If \({\href{../syntax/modules.html#syntax-externidx}{\mathit{externidx}}}\) is some \(\href{../syntax/modules.html#syntax-externidx}{\mathsf{global}}\) \({\href{../syntax/modules.html#syntax-globalidx}{\mathit{globalidx}}}\), then:
1. Let \((\href{../syntax/modules.html#syntax-externidx}{\mathsf{global}}~x)\) be the destructuring of \({\href{../syntax/modules.html#syntax-externidx}{\mathit{externidx}}}\).
2. Return \(\{ \begin{array}[t]{@{}l@{}}\href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}~{\href{../syntax/values.html#syntax-name}{\mathit{name}}},\; \href{../exec/runtime.html#syntax-exportinst}{\mathsf{addr}}~(\href{../exec/runtime.html#syntax-externaddr}{\mathsf{global}}~{\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}{.}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globals}}{}[x]) \}\end{array}\).
If \({\href{../syntax/modules.html#syntax-externidx}{\mathit{externidx}}}\) is some \(\href{../syntax/modules.html#syntax-externidx}{\mathsf{table}}\) \({\href{../syntax/modules.html#syntax-tableidx}{\mathit{tableidx}}}\), then:
1. Let \((\href{../syntax/modules.html#syntax-externidx}{\mathsf{table}}~x)\) be the destructuring of \({\href{../syntax/modules.html#syntax-externidx}{\mathit{externidx}}}\).
2. Return \(\{ \begin{array}[t]{@{}l@{}}\href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}~{\href{../syntax/values.html#syntax-name}{\mathit{name}}},\; \href{../exec/runtime.html#syntax-exportinst}{\mathsf{addr}}~(\href{../exec/runtime.html#syntax-externaddr}{\mathsf{table}}~{\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}{.}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tables}}{}[x]) \}\end{array}\).
If \({\href{../syntax/modules.html#syntax-externidx}{\mathit{externidx}}}\) is some \(\href{../syntax/modules.html#syntax-externidx}{\mathsf{memory}}\) \({\href{../syntax/modules.html#syntax-memidx}{\mathit{memidx}}}\), then:
1. Let \((\href{../syntax/modules.html#syntax-externidx}{\mathsf{memory}}~x)\) be the destructuring of \({\href{../syntax/modules.html#syntax-externidx}{\mathit{externidx}}}\).
2. Return \(\{ \begin{array}[t]{@{}l@{}}\href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}~{\href{../syntax/values.html#syntax-name}{\mathit{name}}},\; \href{../exec/runtime.html#syntax-exportinst}{\mathsf{addr}}~(\href{../exec/runtime.html#syntax-externaddr}{\mathsf{mem}}~{\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}{.}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{mems}}{}[x]) \}\end{array}\).
Assert: Due to validation, \({\href{../syntax/modules.html#syntax-externidx}{\mathit{externidx}}}\) is some \(\href{../syntax/modules.html#syntax-externidx}{\mathsf{tag}}\) \({\href{../syntax/modules.html#syntax-tagidx}{\mathit{tagidx}}}\).
Let \((\href{../syntax/modules.html#syntax-externidx}{\mathsf{tag}}~x)\) be the destructuring of \({\href{../syntax/modules.html#syntax-externidx}{\mathit{externidx}}}\).
Return \(\{ \begin{array}[t]{@{}l@{}}\href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}~{\href{../syntax/values.html#syntax-name}{\mathit{name}}},\; \href{../exec/runtime.html#syntax-exportinst}{\mathsf{addr}}~(\href{../exec/runtime.html#syntax-externaddr}{\mathsf{tag}}~{\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}{.}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tags}}{}[x]) \}\end{array}\).

\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}} {\href{../exec/modules.html#alloc-export}{\mathrm{allocexport}}}({\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}, \href{../syntax/modules.html#syntax-export}{\mathsf{export}}~{\href{../syntax/values.html#syntax-name}{\mathit{name}}}~(\href{../syntax/modules.html#syntax-externidx}{\mathsf{func}}~x)) & = & \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}~{\href{../syntax/values.html#syntax-name}{\mathit{name}}},\; \href{../exec/runtime.html#syntax-exportinst}{\mathsf{addr}}~(\href{../exec/runtime.html#syntax-externaddr}{\mathsf{func}}~{\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}{.}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcs}}{}[x]) \}\end{array} \\ {\href{../exec/modules.html#alloc-export}{\mathrm{allocexport}}}({\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}, \href{../syntax/modules.html#syntax-export}{\mathsf{export}}~{\href{../syntax/values.html#syntax-name}{\mathit{name}}}~(\href{../syntax/modules.html#syntax-externidx}{\mathsf{global}}~x)) & = & \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}~{\href{../syntax/values.html#syntax-name}{\mathit{name}}},\; \href{../exec/runtime.html#syntax-exportinst}{\mathsf{addr}}~(\href{../exec/runtime.html#syntax-externaddr}{\mathsf{global}}~{\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}{.}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globals}}{}[x]) \}\end{array} \\ {\href{../exec/modules.html#alloc-export}{\mathrm{allocexport}}}({\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}, \href{../syntax/modules.html#syntax-export}{\mathsf{export}}~{\href{../syntax/values.html#syntax-name}{\mathit{name}}}~(\href{../syntax/modules.html#syntax-externidx}{\mathsf{table}}~x)) & = & \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}~{\href{../syntax/values.html#syntax-name}{\mathit{name}}},\; \href{../exec/runtime.html#syntax-exportinst}{\mathsf{addr}}~(\href{../exec/runtime.html#syntax-externaddr}{\mathsf{table}}~{\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}{.}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tables}}{}[x]) \}\end{array} \\ {\href{../exec/modules.html#alloc-export}{\mathrm{allocexport}}}({\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}, \href{../syntax/modules.html#syntax-export}{\mathsf{export}}~{\href{../syntax/values.html#syntax-name}{\mathit{name}}}~(\href{../syntax/modules.html#syntax-externidx}{\mathsf{memory}}~x)) & = & \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}~{\href{../syntax/values.html#syntax-name}{\mathit{name}}},\; \href{../exec/runtime.html#syntax-exportinst}{\mathsf{addr}}~(\href{../exec/runtime.html#syntax-externaddr}{\mathsf{mem}}~{\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}{.}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{mems}}{}[x]) \}\end{array} \\ {\href{../exec/modules.html#alloc-export}{\mathrm{allocexport}}}({\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}, \href{../syntax/modules.html#syntax-export}{\mathsf{export}}~{\href{../syntax/values.html#syntax-name}{\mathit{name}}}~(\href{../syntax/modules.html#syntax-externidx}{\mathsf{tag}}~x)) & = & \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}~{\href{../syntax/values.html#syntax-name}{\mathit{name}}},\; \href{../exec/runtime.html#syntax-exportinst}{\mathsf{addr}}~(\href{../exec/runtime.html#syntax-externaddr}{\mathsf{tag}}~{\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}{.}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tags}}{}[x]) \}\end{array} \\ \end{array}\end{split}\]

Note

The definition of module allocation is mutually recursive with the allocation of its associated functions, because the resulting module instance is passed to the allocators 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 \({\href{../syntax/modules.html#syntax-module}{\mathit{module}}}\) is instantiated with a list of external addresses \({{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast}\) 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 an exception or trap when initializing a table or memory from an active segment or when executing the start function. It is up to the embedder to define how such conditions are reported.

\({\href{../exec/modules.html#exec-instantiation}{\mathrm{instantiate}}}(s, {\href{../syntax/modules.html#syntax-module}{\mathit{module}}}, {{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast})\)¶

If \({\href{../syntax/modules.html#syntax-module}{\mathit{module}}}\) is not valid, then:
1. Fail.
Let \({{\mathit{xt}}_{\mathsf{i}}^\ast}~\mathrel{\href{../valid/modules.html#syntax-moduletype}{\rightarrow}}~{{\mathit{xt}}_{\mathsf{e}}^\ast}\) be the destructuring of the type of \({\href{../syntax/modules.html#syntax-module}{\mathit{module}}}\).
Let \((\href{../syntax/modules.html#syntax-module}{\mathsf{module}}~{{\href{../syntax/types.html#syntax-rectype}{\mathit{type}}}^\ast}~{{\href{../syntax/modules.html#syntax-import}{\mathit{import}}}^\ast}~{{\href{../syntax/modules.html#syntax-func}{\mathit{func}}}^\ast}~{{\href{../syntax/modules.html#syntax-global}{\mathit{global}}}^\ast}~{{\href{../syntax/modules.html#syntax-table}{\mathit{table}}}^\ast}~{{\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}}^\ast}~{{\href{../syntax/modules.html#syntax-tag}{\mathit{tag}}}^\ast}~{{\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}}^\ast}~{{\href{../syntax/modules.html#syntax-data}{\mathit{data}}}^\ast}~{{\href{../syntax/modules.html#syntax-start}{\mathit{start}}}^?}~{{\href{../syntax/modules.html#syntax-export}{\mathit{export}}}^\ast})\) be the destructuring of \({\href{../syntax/modules.html#syntax-module}{\mathit{module}}}\).
If \({|{{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast}|} \neq {|{{\mathit{xt}}_{\mathsf{i}}^\ast}|}\), then:
1. Fail.
For all \({\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}\) in \({{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast}\), and corresponding \({\mathit{xt}}_{\mathsf{i}}\) in \({{\mathit{xt}}_{\mathsf{i}}^\ast}\):
1. If \({\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}\) is not valid with type \({\mathit{xt}}_{\mathsf{i}}\), then:
  1. Fail.
Let \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathsf{d}}^\ast}\) be the concatenation of \({{{\href{../exec/modules.html#aux-rundata}{\mathrm{rundata}}}}_{i_{\mathsf{d}}}({{\href{../syntax/modules.html#syntax-data}{\mathit{data}}}^\ast}{}[i_{\mathsf{d}}])^{i_{\mathsf{d}}<{|{{\href{../syntax/modules.html#syntax-data}{\mathit{data}}}^\ast}|}}}\).
Let \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathsf{e}}^\ast}\) be the concatenation of \({{{\href{../exec/modules.html#aux-runelem}{\mathrm{runelem}}}}_{i_{\mathsf{e}}}({{\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}}^\ast}{}[i_{\mathsf{e}}])^{i_{\mathsf{e}}<{|{{\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}}^\ast}|}}}\).
Let \({(\href{../syntax/modules.html#syntax-start}{\mathsf{start}}~x)^?}\) be \({{\href{../syntax/modules.html#syntax-start}{\mathit{start}}}^?}\).
Let \({\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}_0\) be the module instance \(\{ \begin{array}[t]{@{}l@{}}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}~{{{\href{../exec/modules.html#alloc-type}{\mathrm{alloctype}}}^\ast}}{({{\href{../syntax/types.html#syntax-rectype}{\mathit{type}}}^\ast})},\; \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcs}}~{\href{../exec/runtime.html#syntax-externaddr}{\mathrm{funcs}}}({{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast})~{({|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}|} + i_{\mathsf{f}})^{i_{\mathsf{f}}<{|{{\href{../syntax/modules.html#syntax-func}{\mathit{func}}}^\ast}|}}},\; \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globals}}~{\href{../exec/runtime.html#syntax-externaddr}{\mathrm{globals}}}({{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast}) \}\end{array}\).
Let \({(\href{../syntax/modules.html#syntax-table}{\mathsf{table}}~{\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}}~{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}_{\mathsf{t}})^\ast}\) be \({{\href{../syntax/modules.html#syntax-table}{\mathit{table}}}^\ast}\).
Let \({(\href{../syntax/modules.html#syntax-global}{\mathsf{global}}~{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}~{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}_{\mathsf{g}})^\ast}\) be \({{\href{../syntax/modules.html#syntax-global}{\mathit{global}}}^\ast}\).
Let \({(\href{../syntax/modules.html#syntax-elem}{\mathsf{elem}}~{\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}}~{{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}_{\mathsf{e}}^\ast}~{\href{../syntax/modules.html#syntax-elemmode}{\mathit{elemmode}}})^\ast}\) be \({{\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}}^\ast}\).
Let \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathsf{s}}^?}\) be \({(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call}}~x)^?}\).
Let \(z\) be the state \((s, \{ \begin{array}[t]{@{}l@{}}\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~{\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}_0 \}\end{array})\).
Let F be the \(\mathsf{frame}\) \(z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{frame}}\).
Push the \(\mathsf{frame}\) F.
Let \({{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}_{\mathsf{g}}^\ast}\) be \({{{\href{../exec/modules.html#eval-globals}{\mathrm{evalglobal}}}^\ast}}{(z, {{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}^\ast}, {{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}_{\mathsf{g}}^\ast})}\).
Pop the \(\mathsf{frame}\) F from the stack.
Let F be the \(\mathsf{frame}\) \(f\).
Push the \(\mathsf{frame}\) F.
Let \({{\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}_{\mathsf{t}}^\ast}\) be the result of evaluating \({{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}_{\mathsf{t}}^\ast}\) with state \(z\).
Pop the \(\mathsf{frame}\) F from the stack.
Let F be the \(\mathsf{frame}\) \(f\).
Push the \(\mathsf{frame}\) F.
Let \({{{\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}_{\mathsf{e}}^\ast}^\ast}\) be the result of evaluating \({{{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}_{\mathsf{e}}^\ast}^\ast}\) with state \(z\).
Pop the \(\mathsf{frame}\) F from the stack.
Let \({\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}\) be \({\href{../exec/modules.html#alloc-module}{\mathrm{allocmodule}}}(s, {\href{../syntax/modules.html#syntax-module}{\mathit{module}}}, {{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast}, {{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}_{\mathsf{g}}^\ast}, {{\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}_{\mathsf{t}}^\ast}, {{{\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}_{\mathsf{e}}^\ast}^\ast})\).
Let \(f\) be the frame \(\{ \begin{array}[t]{@{}l@{}}\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~{\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}} \}\end{array}\).
Let F be the \(\mathsf{frame}\) \(f\).
Push the \(\mathsf{frame}\) F.
Execute the sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathsf{e}}^\ast}\).
Execute the sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathsf{d}}^\ast}\).
If \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathsf{s}}^?}\) is defined, then:
1. Let \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_0\) be \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathsf{s}}^?}\).
2. Execute the instruction \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_0\).
Pop the \(\mathsf{frame}\) F from the stack.
Return \(f{.}\mathsf{module}\).

If \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) is not valid, then:
1. Fail.
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.
If the number \(m\) of imports is not equal to the number \(n\) of provided external addresses, then:
1. Fail.
For each external address \(\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}_i\) in \(\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}^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-externaddr}{\mathit{externaddr}}_i\) is not valid with an external type \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_i\) in store \(S\), then:
  1. Fail.
2. Let \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}''_i\) be the external type obtained by instantiating \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}'_i\) in \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\) defined below.
3. 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.

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 \}\), that consists of the final module instance \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\), defined below.
Push the frame \(F\) to the stack.
Let \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_{\mathrm{g}}^\ast\) be the list of global initialization values determined by \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) and \(\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}^n\). These may be calculated as follows.
1. 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}}_{\mathrm{g}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}}\).
2. Assert: due to validation, the frame \(F\) is now on the top of the stack.
3. Let \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_{\mathrm{g}}^\ast\) be the concatenation of \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_{\mathrm{g}i}\) in index order.
Let \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}_{\mathrm{t}}^\ast\) be the list of table initialization references determined by \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) and \(\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}^n\). These may be calculated as follows.
1. 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-val}{\mathit{val}}_{\mathrm{t}i}\) be the result of evaluating the initializer expression \(\href{../syntax/modules.html#syntax-table}{\mathit{table}}_i.\href{../syntax/modules.html#syntax-table}{\mathsf{init}}\).
  2. Assert: due to validation, \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_{\mathrm{t}i}\) is a reference.
  3. Let \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}_{\mathrm{t}i}\) be the reference \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_{\mathrm{t}i}\).
2. Assert: due to validation, the frame \(F\) is now on the top of the stack.
3. Let \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}_{\mathrm{t}}^\ast\) be the concatenation of \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}_{ti}\) in index order.
Let \((\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}_{\mathrm{e}}^\ast)^\ast\) be the list of reference lists 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/instructions.html#syntax-expr}{\mathit{expr}}_{ij}\) in \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i.\href{../syntax/modules.html#syntax-elem}{\mathsf{init}}\), do:
  1. Let \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}_{ij}\) be the result of evaluating the initializer expression \(\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}_{ij}\).
2. Let \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast_i\) be the concatenation of function elements \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}_{ij}\) in order of index \(j\).
3. Let \((\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}_{\mathrm{e}}^\ast)^\ast\) be the concatenation of function element lists \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast_i\) in order of index \(i\).
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-externaddr}{\mathit{externaddr}}^n\), global initializer values \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_{\mathrm{g}}^\ast\), table initializer values \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}_{\mathrm{t}}^\ast\), and element segment contents \((\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}_{\mathrm{e}}^\ast)^\ast\), and let \(S'\) be the extended store produced by module allocation.
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-elemmode}{\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. Let \(n\) be the length of the list \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i.\href{../syntax/modules.html#syntax-elem}{\mathsf{init}}\).
2. Execute the instruction sequence \(\mathit{einstr}^\ast_i\).
3. Execute the instruction \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0\).
4. Execute the instruction \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n\).
5. Execute the instruction \(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table{.}init}}~\href{../syntax/modules.html#syntax-tableidx}{\mathit{tableidx}}_i~i\).
6. Execute the instruction \(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{elem{.}drop}}~i\).
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-elemmode}{\mathsf{declare}}\), do:
1. Execute the instruction \(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{elem{.}drop}}~i\).
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-datamode}{\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. Let \(n\) be the length of the list \(\href{../syntax/modules.html#syntax-data}{\mathit{data}}_i.\href{../syntax/modules.html#syntax-data}{\mathsf{init}}\).
2. Execute the instruction sequence \(\mathit{dinstr}^\ast_i\).
3. Execute the instruction \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0\).
4. Execute the instruction \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n\).
5. Execute the instruction \(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory{.}init}}~i\).
6. Execute the instruction \(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{data{.}drop}}~i\).
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}}\).
Assert: due to validation, the frame \(F\) is now on the top of the stack.
Pop the frame \(F\) from the stack.

\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}} {\href{../exec/modules.html#exec-instantiation}{\mathrm{instantiate}}}(s, {\href{../syntax/modules.html#syntax-module}{\mathit{module}}}, {{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast}) & = & {s'} ; f ; {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathsf{e}}^\ast}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathsf{d}}^\ast}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathsf{s}}^?} & \\ \multicolumn{4}{@{}l@{}}{\quad \quad \begin{array}[t]{@{}l@{}} \mbox{if}~ {\href{../valid/modules.html#valid-module}{\vdash}}\, {\href{../syntax/modules.html#syntax-module}{\mathit{module}}} : {{\mathit{xt}}_{\mathsf{i}}^\ast} \mathrel{\href{../valid/modules.html#syntax-moduletype}{\rightarrow}} {{\mathit{xt}}_{\mathsf{e}}^\ast} \\ {\land}~ (s \href{../exec/values.html#valid-externaddr}{\vdash} {\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}} : {\mathit{xt}}_{\mathsf{i}})^\ast \\[0.8ex] {\land}~ {\href{../syntax/modules.html#syntax-module}{\mathit{module}}} = \href{../syntax/modules.html#syntax-module}{\mathsf{module}}~{{\href{../syntax/types.html#syntax-rectype}{\mathit{type}}}^\ast}~{{\href{../syntax/modules.html#syntax-import}{\mathit{import}}}^\ast}~{{\href{../syntax/modules.html#syntax-func}{\mathit{func}}}^\ast}~{{\href{../syntax/modules.html#syntax-global}{\mathit{global}}}^\ast}~{{\href{../syntax/modules.html#syntax-table}{\mathit{table}}}^\ast}~{{\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}}^\ast}~{{\href{../syntax/modules.html#syntax-tag}{\mathit{tag}}}^\ast}~{{\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}}^\ast}~{{\href{../syntax/modules.html#syntax-data}{\mathit{data}}}^\ast}~{{\href{../syntax/modules.html#syntax-start}{\mathit{start}}}^?}~{{\href{../syntax/modules.html#syntax-export}{\mathit{export}}}^\ast} \\ {\land}~ {{\href{../syntax/modules.html#syntax-global}{\mathit{global}}}^\ast} = {(\href{../syntax/modules.html#syntax-global}{\mathsf{global}}~{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}~{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}_{\mathsf{g}})^\ast} \\ {\land}~ {{\href{../syntax/modules.html#syntax-table}{\mathit{table}}}^\ast} = {(\href{../syntax/modules.html#syntax-table}{\mathsf{table}}~{\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}}~{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}_{\mathsf{t}})^\ast} \\ {\land}~ {{\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}}^\ast} = {(\href{../syntax/modules.html#syntax-elem}{\mathsf{elem}}~{\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}}~{{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}_{\mathsf{e}}^\ast}~{\href{../syntax/modules.html#syntax-elemmode}{\mathit{elemmode}}})^\ast} \\ {\land}~ {{\href{../syntax/modules.html#syntax-data}{\mathit{data}}}^\ast} = {(\href{../syntax/modules.html#syntax-data}{\mathsf{data}}~{{\href{../syntax/values.html#syntax-byte}{\mathit{byte}}}^\ast}~{\href{../syntax/modules.html#syntax-datamode}{\mathit{datamode}}})^\ast} \\ {\land}~ {{\href{../syntax/modules.html#syntax-start}{\mathit{start}}}^?} = {(\href{../syntax/modules.html#syntax-start}{\mathsf{start}}~x)^?} \\ {\land}~ {\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}_0 = \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}~{{{\href{../exec/modules.html#alloc-type}{\mathrm{alloctype}}}^\ast}}{({{\href{../syntax/types.html#syntax-rectype}{\mathit{type}}}^\ast})},\; \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcs}}~{\href{../exec/runtime.html#syntax-externaddr}{\mathrm{funcs}}}({{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast})~{({|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}|} + i_{\mathsf{f}})^{i_{\mathsf{f}}<{|{{\href{../syntax/modules.html#syntax-func}{\mathit{func}}}^\ast}|}}},\; \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globals}}~{\href{../exec/runtime.html#syntax-externaddr}{\mathrm{globals}}}({{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast}) \}\end{array} \\ {\land}~ z = s ; \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~{\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}_0 \}\end{array} \\ {\land}~ ({z'}, {{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}_{\mathsf{g}}^\ast}) = {{{\href{../exec/modules.html#eval-globals}{\mathrm{evalglobal}}}^\ast}}{(z, {{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}^\ast}, {{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}_{\mathsf{g}}^\ast})} \\ {\land}~ ({z'} ; {\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}_{\mathsf{t}} \href{../exec/conventions.html#exec-notation}{\hookrightarrow^\ast} {z'} ; {\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}_{\mathsf{t}})^\ast \\ {\land}~ {({z'} ; {\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}_{\mathsf{e}} \href{../exec/conventions.html#exec-notation}{\hookrightarrow^\ast} {z'} ; {\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}_{\mathsf{e}})^\ast}^\ast \\ {\land}~ ({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-externaddr}{\mathit{externaddr}}}^\ast}, {{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}_{\mathsf{g}}^\ast}, {{\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}_{\mathsf{t}}^\ast}, {({{\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}_{\mathsf{e}}^\ast})^\ast}) \\ {\land}~ f = \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~{\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}} \}\end{array} \\ {\land}~ {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathsf{e}}^\ast} = {\href{../syntax/conventions.html#notation-concat}{\bigoplus}}\, {{{\href{../exec/modules.html#aux-runelem}{\mathrm{runelem}}}}_{i_{\mathsf{e}}}({{\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}}^\ast}{}[i_{\mathsf{e}}])^{i_{\mathsf{e}}<{|{{\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}}^\ast}|}}} \\ {\land}~ {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathsf{d}}^\ast} = {\href{../syntax/conventions.html#notation-concat}{\bigoplus}}\, {{{\href{../exec/modules.html#aux-rundata}{\mathrm{rundata}}}}_{i_{\mathsf{d}}}({{\href{../syntax/modules.html#syntax-data}{\mathit{data}}}^\ast}{}[i_{\mathsf{d}}])^{i_{\mathsf{d}}<{|{{\href{../syntax/modules.html#syntax-data}{\mathit{data}}}^\ast}|}}} \\ {\land}~ {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathsf{s}}^?} = {(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call}}~x)^?} \\ \end{array} } \\ \end{array}\end{split}\]

where:

\({{{\href{../exec/modules.html#eval-globals}{\mathrm{evalglobal}}}^\ast}}{(z, {{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}^\ast}, {{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}''}^\ast})}\)¶

If \({{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}^\ast} = \epsilon\) and \({{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}''}^\ast} = \epsilon\), then:
1. Return \(\epsilon\).
Assert: Due to validation, \({|{{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}''}^\ast}|} \geq 1\).
Let \({\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}~{{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}'}^\ast}\) be \({{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}''}^\ast}\).
Assert: Due to validation, \({|{{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}^\ast}|} \geq 1\).
Let \({\mathit{gt}}~{{\mathit{gt}'}^\ast}\) be \({{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}^\ast}\).
Let \((s, f)\) be the destructuring of \(z\).
Let \({\href{../exec/runtime.html#syntax-val}{\mathit{val}}}\) be the result of evaluating \({\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}\) with state \(z\).
Let \(a\) be \({\href{../exec/modules.html#alloc-global}{\mathrm{allocglobal}}}(s, {\mathit{gt}}, {\href{../exec/runtime.html#syntax-val}{\mathit{val}}})\).
Append \(a\) to \(f{.}\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}{.}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globals}}\).
Let \({{\href{../exec/runtime.html#syntax-val}{\mathit{val}}'}^\ast}\) be \({{{\href{../exec/modules.html#eval-globals}{\mathrm{evalglobal}}}^\ast}}{((s, f), {{\mathit{gt}'}^\ast}, {{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}'}^\ast})}\).
Return \({\href{../exec/runtime.html#syntax-val}{\mathit{val}}}~{{\href{../exec/runtime.html#syntax-val}{\mathit{val}}'}^\ast}\).

\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}} {{{\href{../exec/modules.html#eval-globals}{\mathrm{evalglobal}}}^\ast}}{(z, \epsilon, \epsilon)} & = & (z, \epsilon) \\ {{{\href{../exec/modules.html#eval-globals}{\mathrm{evalglobal}}}^\ast}}{(z, {\mathit{gt}}~{{\mathit{gt}'}^\ast}, {\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}~{{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}'}^\ast})} & = & ({z'}, {\href{../exec/runtime.html#syntax-val}{\mathit{val}}}~{{\href{../exec/runtime.html#syntax-val}{\mathit{val}}'}^\ast}) & \\ && \multicolumn{2}{@{}l@{}}{\quad \quad \begin{array}[t]{@{}l@{}} \mbox{if}~ z ; {\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}} \href{../exec/conventions.html#exec-notation}{\hookrightarrow^\ast} z ; {\href{../exec/runtime.html#syntax-val}{\mathit{val}}} \\ {\land}~ z = s ; f \\ {\land}~ ({s'}, a) = {\href{../exec/modules.html#alloc-global}{\mathrm{allocglobal}}}(s, {\mathit{gt}}, {\href{../exec/runtime.html#syntax-val}{\mathit{val}}}) \\ {\land}~ ({z'}, {{\href{../exec/runtime.html#syntax-val}{\mathit{val}}'}^\ast}) = {{{\href{../exec/modules.html#eval-globals}{\mathrm{evalglobal}}}^\ast}}{(({s'} ; f{}[{.}\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}{.}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globals}} \mathrel{{=}{\oplus}} a]), {{\mathit{gt}'}^\ast}, {{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}'}^\ast})} \\ \end{array} } \\ \end{array}\end{split}\]

\({{\href{../exec/modules.html#aux-runelem}{\mathrm{runelem}}}}_{x}(\href{../syntax/modules.html#syntax-elem}{\mathsf{elem}}~{\mathit{rt}}~{e^{n}}~{\href{../syntax/modules.html#syntax-elemmode}{\mathit{elemmode}}})\)¶

If \({\href{../syntax/modules.html#syntax-elemmode}{\mathit{elemmode}}} = \href{../syntax/modules.html#syntax-elemmode}{\mathsf{passive}}\), then:
1. Return \(\epsilon\).
If \({\href{../syntax/modules.html#syntax-elemmode}{\mathit{elemmode}}} = \href{../syntax/modules.html#syntax-elemmode}{\mathsf{declare}}\), then:
1. Return \((\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{elem{.}drop}}~x)\).
Assert: Due to validation, \({\href{../syntax/modules.html#syntax-elemmode}{\mathit{elemmode}}}\) is some \(\href{../syntax/modules.html#syntax-elemmode}{\mathsf{active}}\) \({\href{../syntax/modules.html#syntax-tableidx}{\mathit{tableidx}}}\) \({\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}\).
Let \((\href{../syntax/modules.html#syntax-elemmode}{\mathsf{active}}~y~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast})\) be the destructuring of \({\href{../syntax/modules.html#syntax-elemmode}{\mathit{elemmode}}}\).
Return \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}~(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0)~(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table{.}init}}~y~x)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{elem{.}drop}}~x)\).

\({{\href{../exec/modules.html#aux-rundata}{\mathrm{rundata}}}}_{x}(\href{../syntax/modules.html#syntax-data}{\mathsf{data}}~{b^{n}}~{\href{../syntax/modules.html#syntax-datamode}{\mathit{datamode}}})\)¶

If \({\href{../syntax/modules.html#syntax-datamode}{\mathit{datamode}}} = \href{../syntax/modules.html#syntax-datamode}{\mathsf{passive}}\), then:
1. Return \(\epsilon\).
Assert: Due to validation, \({\href{../syntax/modules.html#syntax-datamode}{\mathit{datamode}}}\) is some \(\href{../syntax/modules.html#syntax-datamode}{\mathsf{active}}\) \({\href{../syntax/modules.html#syntax-memidx}{\mathit{memidx}}}\) \({\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}\).
Let \((\href{../syntax/modules.html#syntax-datamode}{\mathsf{active}}~y~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast})\) be the destructuring of \({\href{../syntax/modules.html#syntax-datamode}{\mathit{datamode}}}\).
Return \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}~(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0)~(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory{.}init}}~y~x)~(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{data{.}drop}}~x)\).

\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}} {{\href{../exec/modules.html#aux-runelem}{\mathrm{runelem}}}}_{x}(\href{../syntax/modules.html#syntax-elem}{\mathsf{elem}}~{\mathit{rt}}~{e^{n}}~(\href{../syntax/modules.html#syntax-elemmode}{\mathsf{passive}})) & = & \epsilon \\ {{\href{../exec/modules.html#aux-runelem}{\mathrm{runelem}}}}_{x}(\href{../syntax/modules.html#syntax-elem}{\mathsf{elem}}~{\mathit{rt}}~{e^{n}}~(\href{../syntax/modules.html#syntax-elemmode}{\mathsf{declare}})) & = & (\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{elem{.}drop}}~x) \\ {{\href{../exec/modules.html#aux-runelem}{\mathrm{runelem}}}}_{x}(\href{../syntax/modules.html#syntax-elem}{\mathsf{elem}}~{\mathit{rt}}~{e^{n}}~(\href{../syntax/modules.html#syntax-elemmode}{\mathsf{active}}~y~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast})) & = & & \\ \multicolumn{4}{@{}l@{}}{\quad \begin{array}[t]{@{}l@{}} {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}~(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0)~(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table{.}init}}~y~x)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{elem{.}drop}}~x) \\ \end{array} } \\[0.8ex] {{\href{../exec/modules.html#aux-rundata}{\mathrm{rundata}}}}_{x}(\href{../syntax/modules.html#syntax-data}{\mathsf{data}}~{b^{n}}~(\href{../syntax/modules.html#syntax-datamode}{\mathsf{passive}})) & = & \epsilon \\ {{\href{../exec/modules.html#aux-rundata}{\mathrm{rundata}}}}_{x}(\href{../syntax/modules.html#syntax-data}{\mathsf{data}}~{b^{n}}~(\href{../syntax/modules.html#syntax-datamode}{\mathsf{active}}~y~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast})) & = & & \\ \multicolumn{4}{@{}l@{}}{\quad \begin{array}[t]{@{}l@{}} {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}~(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0)~(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory{.}init}}~y~x)~(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{data{.}drop}}~x) \\ \end{array} } \\ \end{array}\end{split}\]

Note

Checking import types assumes that the module instance has already been allocated to compute the respective closed defined types. However, this forward reference merely is a way to simplify the specification. In practice, implementations will likely allocate or canonicalize types beforehand, when compiling a module, in a stage before instantiation and before imports are checked.

Similarly, module allocation and the evaluation of global and table initializers as well as element segments are mutually recursive because the global initialization values \({{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}_{\mathsf{g}}^\ast}\), \({\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}_{\mathsf{t}}\), and element segment contents \({{{\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}_{\mathsf{e}}^\ast}^\ast}\) are passed to the module allocator while depending on the module instance \({\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}\) and store \({s'}\) returned by allocation. Again, this recursion is just a specification device. In practice, the initialization values can be determined beforehand by staging module allocation such that first, the module’s own function instances are pre-allocated in the store, then the initializer expressions are evaluated in order, allocating globals on the way, then the rest of the module instance is allocated, and finally the new function instances’ \(\mathsf{module}\) fields are set to that module instance. This is possible because validation ensures that initialization expressions cannot actually call a function, only take their reference.

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¶

\({\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}}}^\ast})\)¶

Assert: Due to validation, the expansion of \(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}}\) is some \(\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}\) \({\href{../syntax/types.html#syntax-functype}{\mathit{functype}}}\).
Let \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{\href{../syntax/types.html#syntax-functype}{\mathit{functype}}}_0)\) be the destructuring of the expansion of \(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}}\).
Let \({t_1^\ast}~\href{../syntax/types.html#syntax-functype}{\rightarrow}~{t_2^\ast}\) be the destructuring of \({\href{../syntax/types.html#syntax-functype}{\mathit{functype}}}_0\).
Let \(f\) be the frame \(\{ \begin{array}[t]{@{}l@{}}\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\{ \begin{array}[t]{@{}l@{}} \}\end{array} \}\end{array}\).
If \({|{t_1^\ast}|} \neq {|{{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^\ast}|}\), then:
1. Fail.
For all \(t_1\) in \({t_1^\ast}\), and corresponding \({\href{../exec/runtime.html#syntax-val}{\mathit{val}}}\) in \({{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^\ast}\):
1. If \({\href{../exec/runtime.html#syntax-val}{\mathit{val}}}\) is not valid with type \(t_1\), then:
  1. Fail.
Let \(k\) be the length of \({t_2^\ast}\).
Let F be the \(\mathsf{frame}\) \(f\) whose arity is \(k\).
Push the \(\mathsf{frame}\) F.
Push the values \({{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^\ast}\) to the stack.
Push the value \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}func}}~{\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}})\) to the stack.
Execute the instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call\_ref}}~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}})\).
Pop the values \({{\href{../exec/runtime.html#syntax-val}{\mathit{val}}'}^{k}}\) from the stack.
Pop the \(\mathsf{frame}\) F from the stack.
Return \({{\href{../exec/runtime.html#syntax-val}{\mathit{val}}'}^{k}}\).

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 an exception or 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 or exceptions can occur.

The following steps are performed:

Assert: \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}]\) exists.
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}}]\).
Let \(\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~[t_1^n] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^m]\) be the composite type \(\href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}.\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}})\).
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.
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 valid with value type \(t_i\), then:
  1. Fail.
Let \(F\) be the dummy frame \(\{ \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\{\}, \href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\epsilon \}\).
Push the frame \(F\) to the stack.
Push the values \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\) to the stack.
Invoke the function instance at address \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}\).

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

Assert: due to validation, \(m\) values are on the top of the stack.
Pop \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_{\mathrm{res}}^m\) from the stack.
Assert: due to validation, the frame \(F\) is now on the top of the stack.
Pop the frame \(F\) from the stack.

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

\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}} {\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}}}^\ast}) & = & s ; f ; {{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^\ast}~(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}func}}~{\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}})~(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call\_ref}}~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}}) & \\ \multicolumn{4}{@{}l@{}}{\quad \quad \begin{array}[t]{@{}l@{}} \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}} \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~({t_1^\ast} \href{../syntax/types.html#syntax-functype}{\rightarrow} {t_2^\ast}) \\ {\land}~ (s \href{../exec/values.html#valid-val}{\vdash} {\href{../exec/runtime.html#syntax-val}{\mathit{val}}} : t_1)^\ast \\ {\land}~ f = \{ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\{ \begin{array}[t]{@{}l@{}} \}\end{array} \}\end{array} \\ \end{array} } \\ \end{array}\end{split}\]

Modules¶

Allocation¶

\({\href{../exec/modules.html#alloc-func}{\mathrm{allocfunc}}}(s, {\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}, {{\href{../exec/runtime.html#syntax-funcinst}{\mathit{code}}}}, {\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}})\)¶

\({\href{../exec/modules.html#alloc-table}{\mathrm{alloctable}}}(s, {\mathit{at}}~{}[ i \href{../syntax/types.html#syntax-limits}{\,{..}\,} j ]~{\mathit{rt}}, {\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}})\)¶

\({\href{../exec/modules.html#alloc-mem}{\mathrm{allocmem}}}(s, {\mathit{at}}~{}[ i \href{../syntax/types.html#syntax-limits}{\,{..}\,} j ]~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}})\)¶

\({\href{../exec/modules.html#alloc-tag}{\mathrm{alloctag}}}(s, {\href{../valid/conventions.html#syntax-tagtype}{\mathit{tagtype}}})\)¶

\({\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}}})\)¶

\({\href{../exec/modules.html#alloc-elem}{\mathrm{allocelem}}}(s, {\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}}, {{\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}^\ast})\)¶

\({\href{../exec/modules.html#alloc-data}{\mathrm{allocdata}}}(s, \href{../valid/modules.html#valid-data}{\mathsf{ok}}, {{\href{../syntax/values.html#syntax-byte}{\mathit{byte}}}^\ast})\)¶

Growing tables¶

\({\href{../exec/modules.html#grow-table}{\mathrm{growtable}}}({\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}}, n, r)\)¶

Growing memories¶

\({\href{../exec/modules.html#grow-mem}{\mathrm{growmem}}}({\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}}, n)\)¶

\({{{\href{../exec/modules.html#alloc-type}{\mathrm{alloctype}}}^\ast}}{({{\href{../syntax/types.html#syntax-rectype}{\mathit{type}}''}^\ast})}\)¶

Instantiation¶

\({\href{../exec/modules.html#exec-instantiation}{\mathrm{instantiate}}}(s, {\href{../syntax/modules.html#syntax-module}{\mathit{module}}}, {{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast})\)¶

\({{{\href{../exec/modules.html#eval-globals}{\mathrm{evalglobal}}}^\ast}}{(z, {{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}^\ast}, {{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}''}^\ast})}\)¶

\({{\href{../exec/modules.html#aux-runelem}{\mathrm{runelem}}}}_{x}(\href{../syntax/modules.html#syntax-elem}{\mathsf{elem}}~{\mathit{rt}}~{e^{n}}~{\href{../syntax/modules.html#syntax-elemmode}{\mathit{elemmode}}})\)¶

\({{\href{../exec/modules.html#aux-rundata}{\mathrm{rundata}}}}_{x}(\href{../syntax/modules.html#syntax-data}{\mathsf{data}}~{b^{n}}~{\href{../syntax/modules.html#syntax-datamode}{\mathit{datamode}}})\)¶

Invocation¶

\({\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}}}^\ast})\)¶

Growing tables ¶

Growing memories ¶