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}}})\)

1. 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}\).

2. Let \(a\) be the length of \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}\).

3. Append \({\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}}\) to \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}\).

4. 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}}})\)

1. 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}\).

2. Let \(a\) be the length of \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}\).

3. Append \({\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}}\) to \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}\).

4. 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}})\)

1. 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}\).

2. Let \(a\) be the length of \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}\).

3. Append \({\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}}\) to \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}\).

4. 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}}})\)

1. 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}\).

2. Let \(a\) be the length of \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{tags}}\).

3. Append \({\href{../exec/runtime.html#syntax-taginst}{\mathit{taginst}}}\) to \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{tags}}\).

4. 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}}})\)

1. 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}\).

2. Let \(a\) be the length of \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}\).

3. Append \({\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}}\) to \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}\).

4. 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})\)

1. 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}\).

2. Let \(a\) be the length of \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}\).

3. Append \({\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}}\) to \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}\).

4. 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})\)

1. 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}\).

2. Let \(a\) be the length of \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}\).

3. Append \({\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}}\) to \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}\).

4. 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)\)

1. 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}}}\).

2. If \({|{{r'}^\ast}|} + n > j\), then:

   1. Fail.

3. Let \({i'}\) be \({|{{r'}^\ast}|} + n\).

4. 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}\).

5. 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)\)

1. 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}}}\).

2. If \({|{b^\ast}|} / (64 \, {\mathrm{Ki}}) + n > j\), then:

   1. Fail.

3. Let \({i'}\) be \({|{b^\ast}|} / (64 \, {\mathrm{Ki}}) + n\).

4. 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}\).

5. 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})\)

1. 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}}}\).

2. Let \({{\mathit{fa}}_{\mathsf{i}}^\ast}\) be \({\href{../exec/runtime.html#syntax-externaddr}{\mathrm{funcs}}}({{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast})\).

3. Let \({{\mathit{ga}}_{\mathsf{i}}^\ast}\) be \({\href{../exec/runtime.html#syntax-externaddr}{\mathrm{globals}}}({{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast})\).

4. Let \({{\mathit{aa}}_{\mathsf{i}}^\ast}\) be \({\href{../exec/runtime.html#syntax-externaddr}{\mathrm{tags}}}({{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast})\).

5. Let \({{\mathit{ma}}_{\mathsf{i}}^\ast}\) be \({\href{../exec/runtime.html#syntax-externaddr}{\mathrm{mems}}}({{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast})\).

6. Let \({{\mathit{ta}}_{\mathsf{i}}^\ast}\) be \({\href{../exec/runtime.html#syntax-externaddr}{\mathrm{tables}}}({{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast})\).

7. Let \({{\mathit{fa}}^\ast}\) be \({({|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}|} + i_{\mathsf{f}})^{i_{\mathsf{f}}<{|{{\href{../syntax/modules.html#syntax-func}{\mathit{func}}}^\ast}|}}}\).

8. Let \({{\mathit{ga}}^\ast}\) be \({({|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}|} + i_{\mathsf{g}})^{i_{\mathsf{g}}<{|{{\href{../syntax/modules.html#syntax-global}{\mathit{global}}}^\ast}|}}}\).

9. Let \({{\mathit{ta}}^\ast}\) be \({({|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}|} + i_{\mathsf{t}})^{i_{\mathsf{t}}<{|{{\href{../syntax/modules.html#syntax-table}{\mathit{table}}}^\ast}|}}}\).

10. Let \({{\mathit{aa}}^\ast}\) be \({({|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{tags}}|} + i_{\mathsf{a}})^{i_{\mathsf{a}}<{|{{\href{../syntax/modules.html#syntax-tag}{\mathit{tag}}}^\ast}|}}}\).

11. Let \({{\mathit{ma}}^\ast}\) be \({({|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}|} + i_{\mathsf{m}})^{i_{\mathsf{m}}<{|{{\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}}^\ast}|}}}\).

12. Let \({{\mathit{ea}}^\ast}\) be \({({|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}|} + i_{\mathsf{e}})^{i_{\mathsf{e}}<{|{{\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}}^\ast}|}}}\).

13. Let \({{\mathit{da}}^\ast}\) be \({({|s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}|} + i_{\mathsf{d}})^{i_{\mathsf{d}}<{|{{\href{../syntax/modules.html#syntax-data}{\mathit{data}}}^\ast}|}}}\).

14. 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}\).

15. Let \({{\mathit{dt}}^\ast}\) be \({{{\href{../exec/modules.html#alloc-type}{\mathrm{alloctype}}}^\ast}}{({{\href{../syntax/types.html#syntax-rectype}{\mathit{type}}}^\ast})}\).

16. Let \({(\href{../syntax/modules.html#syntax-tag}{\mathsf{tag}}~y)^\ast}\) be \({{\href{../syntax/modules.html#syntax-tag}{\mathit{tag}}}^\ast}\).

17. 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}\).

18. 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}\).

19. 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}\).

20. 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}\).

21. 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}\).

22. 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})}\).

23. 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}\).

24. 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}|}}})}\).

25. Assert: Due to validation, \({{\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}}_0^\ast} = {{\mathit{fa}}^\ast}\).

26. 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})}\).

27. Assert: Due to validation, \({{\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}}_0^\ast} = {{\mathit{ga}}^\ast}\).

28. 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})}\).

29. Assert: Due to validation, \({{\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}}_0^\ast} = {{\mathit{ta}}^\ast}\).

30. 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})}\).

31. Assert: Due to validation, \({{\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}}_0^\ast} = {{\mathit{ma}}^\ast}\).

32. 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})}\).

33. Assert: Due to validation, \({{\href{../exec/runtime.html#syntax-tagaddr}{\mathit{tagaddr}}}_0^\ast} = {{\mathit{aa}}^\ast}\).

34. 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})}\).

35. Assert: Due to validation, \({{\href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}}_0^\ast} = {{\mathit{ea}}^\ast}\).

36. 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})}\).

37. Assert: Due to validation, \({{\href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}}_0^\ast} = {{\mathit{da}}^\ast}\).

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

Todo

Prose for Allocmodule was being skipped due to indentation error, which is fixed by now. Needs to check if the generated prose seems good.

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

1. Let \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) be the module to allocate and \(\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}_{\mathrm{im}}^\ast\) the list of external addresses providing the module’s imports, \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_{\mathrm{g}}^\ast\) the initialization values of the module’s globals, \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}_{\mathrm{t}}^\ast\) the initializer reference of the module’s tables, and \((\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}_{\mathrm{e}}^\ast)^\ast\) the reference lists of the module’s element segments.

2. Let \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}^\ast\) be the sequence of defined types obtained by allocating the types from \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{types}}\).

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

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

4. 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{../syntax/types.html#syntax-limits}{\mathit{limits}}_i~t_i\) be the table type obtained by instantiating \(\href{../syntax/modules.html#syntax-table}{\mathit{table}}_i.\href{../syntax/modules.html#syntax-table}{\mathsf{type}}\) in \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\) defined below.

   2. Let \(\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}_i\) be the table address resulting from allocating \(\href{../syntax/modules.html#syntax-table}{\mathit{table}}_i.\href{../syntax/modules.html#syntax-table}{\mathsf{type}}\) with initialization value \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}_{\mathrm{t}}^\ast[i]\).

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

   1. Let \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}_i\) be the memory type obtained by instantiating \(\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}_i.\href{../syntax/modules.html#syntax-mem}{\mathsf{type}}\) in \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\) defined below.

   2. Let \(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}_i\) be the memory address resulting from allocating \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}_i\).

6. 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{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_i\) be the global type obtained by instantiating \(\href{../syntax/modules.html#syntax-global}{\mathit{global}}_i.\href{../syntax/modules.html#syntax-global}{\mathsf{type}}\) in \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\) defined below.

   2. Let \(\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}_i\) be the global address resulting from allocating \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_i\) with initializer value \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_{\mathrm{g}}^\ast[i]\).

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

   1. Let \(\href{../valid/conventions.html#syntax-tagtype}{\mathit{tagtype}}\) be the tag type \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{types}}[\href{../syntax/modules.html#syntax-tag}{\mathit{tag}}_i.\href{../syntax/modules.html#syntax-tag}{\mathsf{type}}]\).

   2. Let \(\href{../exec/runtime.html#syntax-tagaddr}{\mathit{tagaddr}}_i\) be the tag address resulting from allocating \(\href{../valid/conventions.html#syntax-tagtype}{\mathit{tagtype}}\).

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

   1. Let \(\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}_i\) be the element reference type obtained by instantiating \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i.\href{../syntax/modules.html#syntax-elem}{\mathsf{type}}\) in \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\) defined below.

   2. Let \(\href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}_i\) be the element address resulting from allocating a element instance of reference type \(\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}_i\) with contents \((\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}_{\mathrm{e}}^\ast)^\ast[i]\).

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

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

10. Let \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}^\ast\) be the concatenation of the defined types \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}_i\) in index order.

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

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

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

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

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

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

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

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

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

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

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

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

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

    1. Let \(\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}_i\) be the export instance resulting from allocating \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i\).

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

25. Let \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\) be the module instance \(\{\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}^\ast,\) \(\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcs}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}_{\mathrm{mod}}^\ast,\) \(\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tables}}~\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}_{\mathrm{mod}}^\ast,\) \(\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{mems}}~\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}_{\mathrm{mod}}^\ast,\) \(\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globals}}~\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}_{\mathrm{mod}}^\ast,\) \(\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tags}}~\href{../exec/runtime.html#syntax-tagaddr}{\mathit{tagaddr}}_{\mathrm{mod}}^\ast\), \(\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{elems}}~\href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}^\ast,\) \(\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{datas}}~\href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}^\ast,\) \(\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{exports}}~\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}^\ast\}\).

26. 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})}\)

1. If \({{\href{../syntax/types.html#syntax-rectype}{\mathit{type}}''}^\ast} = \epsilon\), then:

   1. Return \(\epsilon\).

2. 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}\).

3. 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}}}\).

4. 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})}\).

5. Let \(x\) be the length of \({{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}'}^\ast}\).

6. 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} ]}\).

7. 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}}})\)

1. If \({\href{../syntax/modules.html#syntax-externidx}{\mathit{externidx}}}\) is some \(\href{../syntax/modules.html#syntax-externidx}{\mathsf{func}}\), 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}\).

2. If \({\href{../syntax/modules.html#syntax-externidx}{\mathit{externidx}}}\) is some \(\href{../syntax/modules.html#syntax-externidx}{\mathsf{global}}\), 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}\).

3. If \({\href{../syntax/modules.html#syntax-externidx}{\mathit{externidx}}}\) is some \(\href{../syntax/modules.html#syntax-externidx}{\mathsf{table}}\), 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}\).

4. If \({\href{../syntax/modules.html#syntax-externidx}{\mathit{externidx}}}\) is some \(\href{../syntax/modules.html#syntax-externidx}{\mathsf{memory}}\), 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}\).

5. Assert: Due to validation, \({\href{../syntax/modules.html#syntax-externidx}{\mathit{externidx}}}\) is some \(\href{../syntax/modules.html#syntax-externidx}{\mathsf{tag}}\).

6. Let \((\href{../syntax/modules.html#syntax-externidx}{\mathsf{tag}}~x)\) be the destructuring of \({\href{../syntax/modules.html#syntax-externidx}{\mathit{externidx}}}\).

7. 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})\)

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

   1. Fail.

2. 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}}}\).

3. 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}}}\).

4. If \({|{{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}^\ast}|} \neq {|{{\mathit{xt}}_{\mathsf{i}}^\ast}|}\), then:

   1. Fail.

5. For all \({\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}\), and \({\mathit{xt}}_{\mathsf{i}}\) in \({({\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}, {\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.

6. 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}|}}}\).

7. 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}|}}}\).

8. Let \({(\href{../syntax/modules.html#syntax-start}{\mathsf{start}}~x)^?}\) be \({{\href{../syntax/modules.html#syntax-start}{\mathit{start}}}^?}\).

9. 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}\).

10. 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}\).

11. 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}\).

12. 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}\).

13. Let \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathsf{s}}^?}\) be \({(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call}}~x)^?}\).

14. 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})\).

15. Let F be the \(\mathsf{frame}\) \(z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{frame}}\).

16. Push the \(\mathsf{frame}\) F.

17. 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})}\).

18. Pop the \(\mathsf{frame}\) F from the stack.

19. Let F be the \(\mathsf{frame}\) \(f\).

20. Push the \(\mathsf{frame}\) F.

21. 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\).

22. Pop the \(\mathsf{frame}\) F from the stack.

23. Let F be the \(\mathsf{frame}\) \(f\).

24. Push the \(\mathsf{frame}\) F.

25. 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\).

26. Pop the \(\mathsf{frame}\) F from the stack.

27. 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})\).

28. 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}\).

29. Let F be the \(\mathsf{frame}\) \(f\).

30. Push the \(\mathsf{frame}\) F.

31. Execute the sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathsf{e}}^\ast}\).

32. Execute the sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathsf{d}}^\ast}\).

33. 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\).

34. Pop the \(\mathsf{frame}\) F from the stack.

35. Return \(f{.}\mathsf{module}\).

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

   1. Fail.

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

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

   1. Fail.

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

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

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

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

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

10. 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\).

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

12. 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\).

13. 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\).

14. 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\).

15. 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}}\).

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

17. 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})}\)

1. 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\).

2. Assert: Due to validation, \({|{{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}''}^\ast}|} \geq 1\).

3. 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}\).

4. Assert: Due to validation, \({|{{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}^\ast}|} \geq 1\).

5. Let \({\mathit{gt}}~{{\mathit{gt}'}^\ast}\) be \({{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}^\ast}\).

6. Let \((s, f)\) be the destructuring of \(z\).

7. 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\).

8. Let \(a\) be \({\href{../exec/modules.html#alloc-global}{\mathrm{allocglobal}}}(s, {\mathit{gt}}, {\href{../exec/runtime.html#syntax-val}{\mathit{val}}})\).

9. Append \(a\) to \(f{.}\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}{.}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globals}}\).

10. 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})}\).

11. 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}}})\)

1. If \({\href{../syntax/modules.html#syntax-elemmode}{\mathit{elemmode}}} = \href{../syntax/modules.html#syntax-elemmode}{\mathsf{passive}}\), then:

   1. Return \(\epsilon\).

2. 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)\).

3. Assert: Due to validation, \({\href{../syntax/modules.html#syntax-elemmode}{\mathit{elemmode}}}\) is some \(\href{../syntax/modules.html#syntax-elemmode}{\mathsf{active}}\).

4. 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}}}\).

5. 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}}})\)

1. If \({\href{../syntax/modules.html#syntax-datamode}{\mathit{datamode}}} = \href{../syntax/modules.html#syntax-datamode}{\mathsf{passive}}\), then:

   1. Return \(\epsilon\).

2. Assert: Due to validation, \({\href{../syntax/modules.html#syntax-datamode}{\mathit{datamode}}}\) is some \(\href{../syntax/modules.html#syntax-datamode}{\mathsf{active}}\).

3. 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}}}\).

4. 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})\)

1. 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}}\).

2. 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}}\).

3. 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\).

4. 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}\).

5. If \({|{t_1^\ast}|} \neq {|{{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^\ast}|}\), then:

   1. Fail.

6. For all \(t_1\), and \({\href{../exec/runtime.html#syntax-val}{\mathit{val}}}\) in \({(t_1, {\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.

7. Let \(k\) be the length of \({t_2^\ast}\).

8. Let F be the \(\mathsf{frame}\) \(f\) whose arity is \(k\).

9. Push the \(\mathsf{frame}\) F.

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

11. Push the value \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}func}}~{\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}})\) to the stack.

12. 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}})\).

13. Pop the values \({{\href{../exec/runtime.html#syntax-val}{\mathit{val}}'}^{k}}\) from the stack.

14. Pop the \(\mathsf{frame}\) F from the stack.

15. 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:

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

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

3. Let \(\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}})\).

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

   1. Fail.

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

   1. If \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_i\) is not valid with value type \(t_i\), then:

      1. Fail.

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

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

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

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

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

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

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

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

4. 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}} \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}\]