For modules, the execution semantics primarily defines :ref:`instantiation <exec-instantiation>`, which :ref:`allocates <alloc>` instances for a module and its contained definitions, initializes :ref:`tables <syntax-table>` and :ref:`memories <syntax-mem>` from contained :ref:`element <syntax-elem>` and :ref:`data <syntax-data>` segments, and invokes the :ref:`start function <syntax-start>` if present. It also includes :ref:`invocation <exec-invocation>` of exported functions.

Instantiation depends on a number of auxiliary notions for :ref:`type-checking imports <exec-import>` and :ref:`allocating <alloc>` instances.

.. index:: external value, external type, validation, import, store

For the purpose of checking :ref:`external values <syntax-externval>` against :ref:`imports <syntax-import>`, such values are classified by :ref:`external types <syntax-externtype>`. The following auxiliary typing rules specify this typing relation relative to a :ref:`store <syntax-store>` S in which the referenced instances live.

.. index:: function type, function address

• The store entry S.\SFUNCS[a] must exist.
• Then \EVFUNC~a is valid with :ref:`external type <syntax-externtype>` \ETFUNC~S.\SFUNCS[a].\FITYPE.

\frac{
}{
  S \vdashexternval \EVFUNC~a : \ETFUNC~S.\SFUNCS[a].\FITYPE
}

.. index:: table type, table address

• The store entry S.\STABLES[a] must exist.
• Then \EVTABLE~a is valid with :ref:`external type <syntax-externtype>` \ETTABLE~S.\STABLES[a].\TITYPE.

\frac{
}{
  S \vdashexternval \EVTABLE~a : \ETTABLE~S.\STABLES[a].\TITYPE
}

.. index:: memory type, memory address

• The store entry S.\SMEMS[a] must exist.
• Then \EVMEM~a is valid with :ref:`external type <syntax-externtype>` \ETMEM~S.\SMEMS[a].\MITYPE.

\frac{
}{
  S \vdashexternval \EVMEM~a : \ETMEM~S.\SMEMS[a].\MITYPE
}

.. index:: global type, global address, value type, mutability

• The store entry S.\SGLOBALS[a] must exist.
• Then \EVGLOBAL~a is valid with :ref:`external type <syntax-externtype>` \ETGLOBAL~S.\SGLOBALS[a].\GITYPE.

\frac{
}{
  S \vdashexternval \EVGLOBAL~a : \ETGLOBAL~S.\SGLOBALS[a].\GITYPE
}

.. index:: value, value type, validation

For the purpose of checking argument :ref:`values <syntax-externval>` against the parameter types of exported :ref:`functions <syntax-func>`, values are classified by :ref:`value types <syntax-valtype>`. The following auxiliary typing rules specify this typing relation relative to a :ref:`store <syntax-store>` S in which possibly referenced addresses live.

• The value is valid with :ref:`number type <syntax-numtype>` t.

\frac{
}{
  S \vdashval t.\CONST~c : t
}

• The value is valid with :ref:`reference type <syntax-reftype>` t.

\frac{
}{
  S \vdashval \REFNULL~t : t
}

• The :ref:`external value <syntax-externval>` \EVFUNC~a must be :ref:`valid <valid-externval>`.
• Then the value is valid with :ref:`reference type <syntax-reftype>` \FUNCREF.

\frac{
  S \vdashexternval \EVFUNC~a : \ETFUNC~\functype
}{
  S \vdashval \REFFUNCADDR~a : \FUNCREF
}

• The value is valid with :ref:`reference type <syntax-reftype>` \EXTERNREF.

\frac{
}{
  S \vdashval \REFEXTERNADDR~a : \EXTERNREF
}

.. index:: ! allocation, store, address

New instances of :ref:`functions <syntax-funcinst>`, :ref:`tables <syntax-tableinst>`, :ref:`memories <syntax-meminst>`, and :ref:`globals <syntax-globalinst>` are allocated in a :ref:`store <syntax-store>` S, as defined by the following auxiliary functions.

.. index:: function, function instance, function address, module instance, function type

1. Let \func be the :ref:`function <syntax-func>` to allocate and \moduleinst its :ref:`module instance <syntax-moduleinst>`.
2. Let a be the first free :ref:`function address <syntax-funcaddr>` in S.
3. Let \functype be the :ref:`function type <syntax-functype>` \moduleinst.\MITYPES[\func.\FTYPE].
4. Let \funcinst be the :ref:`function instance <syntax-funcinst>` \{ \FITYPE~\functype, \FIMODULE~\moduleinst, \FICODE~\func \}.
5. Append \funcinst to the |SFUNCS| of S.
6. Return a.

~\\[-1ex]
\begin{array}{rlll}
\allocfunc(S, \func, \moduleinst) &=& S', \funcaddr \\[1ex]
\mbox{where:} \hfill \\
\funcaddr &=& |S.\SFUNCS| \\
\functype &=& \moduleinst.\MITYPES[\func.\FTYPE] \\
\funcinst &=& \{ \FITYPE~\functype, \FIMODULE~\moduleinst, \FICODE~\func \} \\
S' &=& S \compose \{\SFUNCS~\funcinst\} \\
\end{array}

.. index:: host function, function instance, function address, function type

1. Let \hostfunc be the :ref:`host function <syntax-hostfunc>` to allocate and \functype its :ref:`function type <syntax-functype>`.
2. Let a be the first free :ref:`function address <syntax-funcaddr>` in S.
3. Let \funcinst be the :ref:`function instance <syntax-funcinst>` \{ \FITYPE~\functype, \FIHOSTCODE~\hostfunc \}.
4. Append \funcinst to the |SFUNCS| of S.
5. Return a.

~\\[-1ex]
\begin{array}{rlll}
\allochostfunc(S, \functype, \hostfunc) &=& S', \funcaddr \\[1ex]
\mbox{where:} \hfill \\
\funcaddr &=& |S.\SFUNCS| \\
\funcinst &=& \{ \FITYPE~\functype, \FIHOSTCODE~\hostfunc \} \\
S' &=& S \compose \{\SFUNCS~\funcinst\} \\
\end{array}

.. index:: table, table instance, table address, table type, limits

1. Let \tabletype be the :ref:`table type <syntax-tabletype>` to allocate and \reff the initialization value.
2. Let (\{\LMIN~n, \LMAX~m^?\}~\reftype) be the structure of :ref:`table type <syntax-tabletype>` \tabletype.
3. Let a be the first free :ref:`table address <syntax-tableaddr>` in S.
4. Let \tableinst be the :ref:`table instance <syntax-tableinst>` \{ \TITYPE~\tabletype, \TIELEM~\reff^n \} with n elements set to \reff.
5. Append \tableinst to the |STABLES| of S.
6. Return a.

\begin{array}{rlll}
\alloctable(S, \tabletype, \reff) &=& S', \tableaddr \\[1ex]
\mbox{where:} \hfill \\
\tabletype &=& \{\LMIN~n, \LMAX~m^?\}~\reftype \\
\tableaddr &=& |S.\STABLES| \\
\tableinst &=& \{ \TITYPE~\tabletype, \TIELEM~\reff^n \} \\
S' &=& S \compose \{\STABLES~\tableinst\} \\
\end{array}

.. index:: memory, memory instance, memory address, memory type, limits, byte

1. Let \memtype be the :ref:`memory type <syntax-memtype>` to allocate.
2. Let \{\LMIN~n, \LMAX~m^?\} be the structure of :ref:`memory type <syntax-memtype>` \memtype.
3. Let a be the first free :ref:`memory address <syntax-memaddr>` in S.
4. Let \meminst be the :ref:`memory instance <syntax-meminst>` \{ \MITYPE~\memtype, \MIDATA~(\hex{00})^{n \cdot 64\,\F{Ki}} \} that contains n pages of zeroed :ref:`bytes <syntax-byte>`.
5. Append \meminst to the |SMEMS| of S.
6. Return a.

\begin{array}{rlll}
\allocmem(S, \memtype) &=& S', \memaddr \\[1ex]
\mbox{where:} \hfill \\
\memtype &=& \{\LMIN~n, \LMAX~m^?\} \\
\memaddr &=& |S.\SMEMS| \\
\meminst &=& \{ \MITYPE~\memtype, \MIDATA~(\hex{00})^{n \cdot 64\,\F{Ki}} \} \\
S' &=& S \compose \{\SMEMS~\meminst\} \\
\end{array}

.. index:: global, global instance, global address, global type, value type, mutability, value

1. Let \globaltype be the :ref:`global type <syntax-globaltype>` to allocate and \val the :ref:`value <syntax-val>` to initialize the global with.
2. Let a be the first free :ref:`global address <syntax-globaladdr>` in S.
3. Let \globalinst be the :ref:`global instance <syntax-globalinst>` \{ \GITYPE~\globaltype, \GIVALUE~\val \}.
4. Append \globalinst to the |SGLOBALS| of S.
5. Return a.

\begin{array}{rlll}
\allocglobal(S, \globaltype, \val) &=& S', \globaladdr \\[1ex]
\mbox{where:} \hfill \\
\globaladdr &=& |S.\SGLOBALS| \\
\globalinst &=& \{ \GITYPE~\globaltype, \GIVALUE~\val \} \\
S' &=& S \compose \{\SGLOBALS~\globalinst\} \\
\end{array}

.. index:: element, element instance, element address

1. Let \reftype be the elements' type and \reff^\ast the vector of :ref:`references <syntax-ref>` to allocate.
2. Let a be the first free :ref:`element address <syntax-elemaddr>` in S.
3. Let \eleminst be the :ref:`element instance <syntax-eleminst>` \{ \EITYPE~t, \EIELEM~\reff^\ast \}.
4. Append \eleminst to the |SELEMS| of S.
5. Return a.

\begin{array}{rlll}
\allocelem(S, \reftype, \reff^\ast) &=& S', \elemaddr \\[1ex]
\mbox{where:} \hfill \\
\elemaddr &=& |S.\SELEMS| \\
\eleminst &=& \{ \EITYPE~\reftype, \EIELEM~\reff^\ast \} \\
S' &=& S \compose \{\SELEMS~\eleminst\} \\
\end{array}

.. index:: data, data instance, data address

1. Let \bytes be the vector of :ref:`bytes <syntax-byte>` to allocate.
2. Let a be the first free :ref:`data address <syntax-dataaddr>` in S.
3. Let \datainst be the :ref:`data instance <syntax-datainst>` \{ \DIDATA~\bytes \}.
4. Append \datainst to the |SDATAS| of S.
5. Return a.

\begin{array}{rlll}
\allocdata(S, \bytes) &=& S', \dataaddr \\[1ex]
\mbox{where:} \hfill \\
\dataaddr &=& |S.\SDATAS| \\
\datainst &=& \{ \DIDATA~\bytes \} \\
S' &=& S \compose \{\SDATAS~\datainst\} \\
\end{array}

.. index:: table, table instance, table address, grow, limits

1. Let \tableinst be the :ref:`table instance <syntax-tableinst>` to grow, n the number of elements by which to grow it, and \reff the initialization value.
2. Let \X{len} be n added to the length of \tableinst.\TIELEM.
3. If \X{len} is larger than or equal to 2^{32}, then fail.
4. Let \limits~t be the structure of :ref:`table type <syntax-tabletype>` \tableinst.\TITYPE.
5. Let \limits' be \limits with \LMIN updated to \X{len}.
6. If \limits' is not :ref:`valid <valid-limits>`, then fail.
7. Append \reff^n to \tableinst.\TIELEM.
8. Set \tableinst.\TITYPE to the :ref:`table type <syntax-tabletype>` \limits'~t.

\begin{array}{rllll}
\growtable(\tableinst, n, \reff) &=& \tableinst \with \TITYPE = \limits'~t \with \TIELEM = \tableinst.\TIELEM~\reff^n \\
  && (
    \begin{array}[t]{@{}r@{~}l@{}}
    \iff & \X{len} = n + |\tableinst.\TIELEM| \\
    \wedge & \X{len} < 2^{32} \\
    \wedge & \limits~t = \tableinst.\TITYPE \\
    \wedge & \limits' = \limits \with \LMIN = \X{len} \\
    \wedge & \vdashlimits \limits' \ok \\
    \end{array} \\
\end{array}

.. index:: memory, memory instance, memory address, grow, limits

1. Let \meminst be the :ref:`memory instance <syntax-meminst>` to grow and n the number of :ref:`pages <page-size>` by which to grow it.
2. Assert: The length of \meminst.\MIDATA is divisible by the :ref:`page size <page-size>` 64\,\F{Ki}.
3. Let \X{len} be n added to the length of \meminst.\MIDATA divided by the :ref:`page size <page-size>` 64\,\F{Ki}.
4. If \X{len} is larger than 2^{16}, then fail.
5. Let \limits be the structure of :ref:`memory type <syntax-memtype>` \meminst.\MITYPE.
6. Let \limits' be \limits with \LMIN updated to \X{len}.
7. If \limits' is not :ref:`valid <valid-limits>`, then fail.
8. Append n times 64\,\F{Ki} :ref:`bytes <syntax-byte>` with value \hex{00} to \meminst.\MIDATA.
9. Set \meminst.\MITYPE to the :ref:`memory type <syntax-memtype>` \limits'.

\begin{array}{rllll}
\growmem(\meminst, n) &=& \meminst \with \MITYPE = \limits' \with \MIDATA = \meminst.\MIDATA~(\hex{00})^{n \cdot 64\,\F{Ki}} \\
  && (
    \begin{array}[t]{@{}r@{~}l@{}}
    \iff & \X{len} = n + |\meminst.\MIDATA| / 64\,\F{Ki} \\
    \wedge & \X{len} \leq 2^{16} \\
    \wedge & \limits = \meminst.\MITYPE \\
    \wedge & \limits' = \limits \with \LMIN = \X{len} \\
    \wedge & \vdashlimits \limits' \ok \\
    \end{array} \\
\end{array}

.. index:: module, module instance, function instance, table instance, memory instance, global instance, export instance, function address, table address, memory address, global address, function index, table index, memory index, global index, type, function, table, memory, global, import, export, external value, external type, matching

The allocation function for :ref:`modules <syntax-module>` requires a suitable list of :ref:`external values <syntax-externval>` that are assumed to :ref:`match <match-externtype>` the :ref:`import <syntax-import>` vector of the module, a list of initialization :ref:`values <syntax-val>` for the module's :ref:`globals <syntax-global>`, and list of :ref:`reference <syntax-ref>` vectors for the module's :ref:`element segments <syntax-elem>`.

1. Let \module be the :ref:`module <syntax-module>` to allocate and \externval_{\F{im}}^\ast the vector of :ref:`external values <syntax-externval>` providing the module's imports, \val^\ast the initialization :ref:`values <syntax-val>` of the module's :ref:`globals <syntax-global>`, and (\reff^\ast)^\ast the :ref:`reference <syntax-ref>` vectors of the module's :ref:`element segments <syntax-elem>`.

2. For each :ref:`function <syntax-func>` \func_i in \module.\MFUNCS, do:

   1. Let \funcaddr_i be the :ref:`function address <syntax-funcaddr>` resulting from :ref:`allocating <alloc-func>` \func_i for the :ref:`\module instance <syntax-moduleinst>` \moduleinst defined below.

3. For each :ref:`table <syntax-table>` \table_i in \module.\MTABLES, do:

   1. Let \limits_i~t_i be the :ref:`table type <syntax-tabletype>` \table_i.\TTYPE.

   b. Let \tableaddr_i be the :ref:`table address <syntax-tableaddr>` resulting from :ref:`allocating <alloc-table>` \table_i.\TTYPE with initialization value \REFNULL~t_i.

4. For each :ref:`memory <syntax-mem>` \mem_i in \module.\MMEMS, do:

   1. Let \memaddr_i be the :ref:`memory address <syntax-memaddr>` resulting from :ref:`allocating <alloc-mem>` \mem_i.\MTYPE.

5. For each :ref:`global <syntax-global>` \global_i in \module.\MGLOBALS, do:

   1. Let \globaladdr_i be the :ref:`global address <syntax-globaladdr>` resulting from :ref:`allocating <alloc-global>` \global_i.\GTYPE with initializer value \val^\ast[i].

6. For each :ref:`element segment <syntax-elem>` \elem_i in \module.\MELEMS, do:

   1. Let \elemaddr_i be the :ref:`element address <syntax-elemaddr>` resulting from :ref:`allocating <alloc-elem>` a :ref:`element instance <syntax-eleminst>` of :ref:`reference type <syntax-reftype>` \elem_i.\ETYPE with contents (\reff^\ast)^\ast[i].

7. For each :ref:`data segment <syntax-data>` \data_i in \module.\MDATAS, do:

   1. Let \dataaddr_i be the :ref:`data address <syntax-dataaddr>` resulting from :ref:`allocating <alloc-data>` a :ref:`data instance <syntax-datainst>` with contents \data_i.\DINIT.

8. Let \funcaddr^\ast be the concatenation of the :ref:`function addresses <syntax-funcaddr>` \funcaddr_i in index order.

9. Let \tableaddr^\ast be the concatenation of the :ref:`table addresses <syntax-tableaddr>` \tableaddr_i in index order.

10. Let \memaddr^\ast be the concatenation of the :ref:`memory addresses <syntax-memaddr>` \memaddr_i in index order.

11. Let \globaladdr^\ast be the concatenation of the :ref:`global addresses <syntax-globaladdr>` \globaladdr_i in index order.

12. Let \elemaddr^\ast be the concatenation of the :ref:`element addresses <syntax-elemaddr>` \elemaddr_i in index order.

13. Let \dataaddr^\ast be the concatenation of the :ref:`data addresses <syntax-dataaddr>` \dataaddr_i in index order.

14. Let \funcaddr_{\F{mod}}^\ast be the list of :ref:`function addresses <syntax-funcaddr>` extracted from \externval_{\F{im}}^\ast, concatenated with \funcaddr^\ast.

15. Let \tableaddr_{\F{mod}}^\ast be the list of :ref:`table addresses <syntax-tableaddr>` extracted from \externval_{\F{im}}^\ast, concatenated with \tableaddr^\ast.

16. Let \memaddr_{\F{mod}}^\ast be the list of :ref:`memory addresses <syntax-memaddr>` extracted from \externval_{\F{im}}^\ast, concatenated with \memaddr^\ast.

17. Let \globaladdr_{\F{mod}}^\ast be the list of :ref:`global addresses <syntax-globaladdr>` extracted from \externval_{\F{im}}^\ast, concatenated with \globaladdr^\ast.

18. For each :ref:`export <syntax-export>` \export_i in \module.\MEXPORTS, do:

    1. If \export_i is a function export for :ref:`function index <syntax-funcidx>` x, then let \externval_i be the :ref:`external value <syntax-externval>` \EVFUNC~(\funcaddr_{\F{mod}}^\ast[x]).
    2. Else, if \export_i is a table export for :ref:`table index <syntax-tableidx>` x, then let \externval_i be the :ref:`external value <syntax-externval>` \EVTABLE~(\tableaddr_{\F{mod}}^\ast[x]).
    3. Else, if \export_i is a memory export for :ref:`memory index <syntax-memidx>` x, then let \externval_i be the :ref:`external value <syntax-externval>` \EVMEM~(\memaddr_{\F{mod}}^\ast[x]).
    4. Else, if \export_i is a global export for :ref:`global index <syntax-globalidx>` x, then let \externval_i be the :ref:`external value <syntax-externval>` \EVGLOBAL~(\globaladdr_{\F{mod}}^\ast[x]).
    5. Let \exportinst_i be the :ref:`export instance <syntax-exportinst>` \{\EINAME~(\export_i.\ENAME), \EIVALUE~\externval_i\}.

19. Let \exportinst^\ast be the concatenation of the :ref:`export instances <syntax-exportinst>` \exportinst_i in index order.

20. Let \moduleinst be the :ref:`module instance <syntax-moduleinst>` \{\MITYPES~(\module.\MTYPES), \MIFUNCS~\funcaddr_{\F{mod}}^\ast, \MITABLES~\tableaddr_{\F{mod}}^\ast, \MIMEMS~\memaddr_{\F{mod}}^\ast, \MIGLOBALS~\globaladdr_{\F{mod}}^\ast, \MIEXPORTS~\exportinst^\ast\}.

21. Return \moduleinst.

~\\
\begin{array}{rlll}
\allocmodule(S, \module, \externval_{\F{im}}^\ast, \val^\ast, (\reff^\ast)^\ast) &=& S', \moduleinst
\end{array}

where:

\begin{array}{@{}rlll@{}}
\table^\ast &=& \module.\MTABLES \\
\mem^\ast &=& \module.\MMEMS \\
\global^\ast &=& \module.\MGLOBALS \\
\elem^\ast &=& \module.\MELEMS \\
\data^\ast &=& \module.\MDATAS \\
\export^\ast &=& \module.\MEXPORTS \\[1ex]
\moduleinst &=& \{~
  \begin{array}[t]{@{}l@{}}
  \MITYPES~\module.\MTYPES, \\
  \MIFUNCS~\evfuncs(\externval_{\F{im}}^\ast)~\funcaddr^\ast, \\
  \MITABLES~\evtables(\externval_{\F{im}}^\ast)~\tableaddr^\ast, \\
  \MIMEMS~\evmems(\externval_{\F{im}}^\ast)~\memaddr^\ast, \\
  \MIGLOBALS~\evglobals(\externval_{\F{im}}^\ast)~\globaladdr^\ast, \\
  \MIELEMS~\elemaddr^\ast, \\
  \MIDATAS~\dataaddr^\ast, \\
  \MIEXPORTS~\exportinst^\ast ~\}
  \end{array} \\[1ex]
S_1, \funcaddr^\ast &=&
  \allocfunc^\ast(S, \module.\MFUNCS, \moduleinst) \\
S_2, \tableaddr^\ast &=&
  \alloctable^\ast(S_1, (\table.\TTYPE)^\ast, (\REFNULL~t)^\ast)
  \quad (\where (\table.\TTYPE)^\ast = (\limits~t)^\ast) \\
S_3, \memaddr^\ast &=&
  \allocmem^\ast(S_2, (\mem.\MTYPE)^\ast) \\
S_4, \globaladdr^\ast &=&
  \allocglobal^\ast(S_3, (\global.\GTYPE)^\ast, \val^\ast) \\
S_5, \elemaddr^\ast &=&
  \allocelem^\ast(S_4, (\elem.\ETYPE)^\ast, (\reff^\ast)^\ast) \\
S', \dataaddr^\ast &=&
  \allocdata^\ast(S_5, (\data.\DINIT)^\ast) \\
\exportinst^\ast &=&
  \{ \EINAME~(\export.\ENAME), \EIVALUE~\externval_{\F{ex}} \}^\ast \\[1ex]
\evfuncs(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIFUNCS[x])^\ast
  \qquad~ (\where x^\ast = \edfuncs(\export^\ast)) \\
\evtables(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MITABLES[x])^\ast
  \qquad (\where x^\ast = \edtables(\export^\ast)) \\
\evmems(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIMEMS[x])^\ast
  \qquad (\where x^\ast = \edmems(\export^\ast)) \\
\evglobals(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIGLOBALS[x])^\ast
  \qquad\!\!\! (\where x^\ast = \edglobals(\export^\ast)) \\
\end{array}

Here, the notation \F{allocx}^\ast is shorthand for multiple :ref:`allocations <alloc>` of object kind X, defined as follows:

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

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

.. index:: ! instantiation, module, instance, store, trap

Given a :ref:`store <syntax-store>` S, a :ref:`module <syntax-module>` \module is instantiated with a list of :ref:`external values <syntax-externval>` \externval^n supplying the required imports as follows.

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

1. If \module is not :ref:`valid <valid-module>`, then:
   1. Fail.
2. Assert: \module is :ref:`valid <valid-module>` with :ref:`external types <syntax-externtype>` \externtype_{\F{im}}^m classifying its :ref:`imports <syntax-import>`.
3. If the number m of :ref:`imports <syntax-import>` is not equal to the number n of provided :ref:`external values <syntax-externval>`, then:
   1. Fail.
4. For each :ref:`external value <syntax-externval>` \externval_i in \externval^n and :ref:`external type <syntax-externtype>` \externtype'_i in \externtype_{\F{im}}^n, do:
   1. If \externval_i is not :ref:`valid <valid-externval>` with an :ref:`external type <syntax-externtype>` \externtype_i in store S, then:
      1. Fail.
   2. If \externtype_i does not :ref:`match <match-externtype>` \externtype'_i, then:
      1. Fail.

5. Let \moduleinst_{\F{init}} be the auxiliary module :ref:`instance <syntax-moduleinst>` \{\MIGLOBALS~\evglobals(\externval^n), \MIFUNCS~\moduleinst.\MIFUNCS\} that only consists of the imported globals and the imported and allocated functions from the final module instance \moduleinst, defined below.

6. Let F_{\F{init}} be the auxiliary :ref:`frame <syntax-frame>` \{ \AMODULE~\moduleinst_{\F{init}}, \ALOCALS~\epsilon \}.

7. Push the frame F_{\F{init}} to the stack.

8. Let \val^\ast be the vector of :ref:`global <syntax-global>` initialization :ref:`values <syntax-val>` determined by \module and \externval^n. These may be calculated as follows.

   1. For each :ref:`global <syntax-global>` \global_i in \module.\MGLOBALS, do:
      1. Let \val_i be the result of :ref:`evaluating <exec-expr>` the initializer expression \global_i.\GINIT.
   2. Assert: due to :ref:`validation <valid-module>`, the frame F_{\F{init}} is now on the top of the stack.
   3. Let \val^\ast be the concatenation of \val_i in index order.

9. Let (\reff^\ast)^\ast be the list of :ref:`reference <syntax-ref>` vectors determined by the :ref:`element segments <syntax-elem>` in \module. These may be calculated as follows.

   1. For each :ref:`element segment <syntax-elem>` \elem_i in \module.\MELEMS, and for each element :ref:`expression <syntax-expr>` \expr_{ij} in \elem_i.\EINIT, do:
      1. Let \reff_{ij} be the result of :ref:`evaluating <exec-expr>` the initializer expression \expr_{ij}.
   2. Let \reff^\ast_i be the concatenation of function elements \reff_{ij} in order of index j.
   3. Let (\reff^\ast)^\ast be the concatenation of function element vectors \reff^\ast_i in order of index i.

10. Pop the frame F_{\F{init}} from the stack.

11. Let \moduleinst be a new module instance :ref:`allocated <alloc-module>` from \module in store S with imports \externval^n, global initializer values \val^\ast, and element segment contents (\reff^\ast)^\ast, and let S' be the extended store produced by module allocation.

12. Let F be the auxiliary :ref:`frame <syntax-frame>` \{ \AMODULE~\moduleinst, \ALOCALS~\epsilon \}.

13. Push the frame F to the stack.

14. For each :ref:`element segment <syntax-elem>` \elem_i in \module.\MELEMS whose :ref:`mode <syntax-elemmode>` is of the form \EACTIVE~\{ \ETABLE~\tableidx_i, \EOFFSET~\X{einstr}^\ast_i~\END \}, do:

    1. Let n be the length of the vector \elem_i.\EINIT.
    2. :ref:`Execute <exec-instr-seq>` the instruction sequence \X{einstr}^\ast_i.
    3. :ref:`Execute <exec-const>` the instruction \I32.\CONST~0.
    4. :ref:`Execute <exec-const>` the instruction \I32.\CONST~n.
    5. :ref:`Execute <exec-table.init>` the instruction \TABLEINIT~\tableidx_i~i.
    6. :ref:`Execute <exec-elem.drop>` the instruction \ELEMDROP~i.

15. For each :ref:`data segment <syntax-data>` \data_i in \module.\MDATAS whose :ref:`mode <syntax-datamode>` is of the form \DACTIVE~\{ \DMEM~\memidx_i, \DOFFSET~\X{dinstr}^\ast_i~\END \}, do:

    1. Assert: \memidx_i is 0.
    2. Let n be the length of the vector \data_i.\DINIT.
    3. :ref:`Execute <exec-instr-seq>` the instruction sequence \X{dinstr}^\ast_i.
    4. :ref:`Execute <exec-const>` the instruction \I32.\CONST~0.
    5. :ref:`Execute <exec-const>` the instruction \I32.\CONST~n.
    6. :ref:`Execute <exec-memory.init>` the instruction \MEMORYINIT~i.
    7. :ref:`Execute <exec-data.drop>` the instruction \DATADROP~i.

16. If the :ref:`start function <syntax-start>` \module.\MSTART is not empty, then:

    1. Let \start be the :ref:`start function <syntax-start>` \module.\MSTART.
    2. :ref:`Execute <exec-call>` the instruction \CALL~\start.\SFUNC.

17. Assert: due to :ref:`validation <valid-module>`, the frame F is now on the top of the stack.

18. Pop the frame F from the stack.

~\\
\begin{array}{@{}rcll}
\instantiate(S, \module, \externval^k) &=& S'; F;
  \begin{array}[t]{@{}l@{}}
  \F{runelem}_0(\elem^n[0])~\dots~\F{runelem}_{n-1}(\elem^n[n-1]) \\
  \F{rundata}_0(\data^m[0])~\dots~\F{rundata}_{m-1}(\data^m[m-1]) \\
  (\CALL~\start.\SFUNC)^? \\
  \end{array} \\
&(\iff
  & \vdashmodule \module : \externtype_{\F{im}}^k \to \externtype_{\F{ex}}^\ast \\
  &\wedge& (S \vdashexternval \externval : \externtype)^k \\
  &\wedge& (\vdashexterntypematch \externtype \matchesexterntype \externtype_{\F{im}})^k \\[1ex]
  &\wedge& \module.\MGLOBALS = \global^\ast \\
  &\wedge& \module.\MELEMS = \elem^n \\
  &\wedge& \module.\MDATAS = \data^m \\
  &\wedge& \module.\MSTART = \start^? \\
  &\wedge& (\expr_{\F{g}} = \global.GINIT)^\ast \\
  &\wedge& (\expr_{\F{e}}^\ast = \elem.EINIT)^n \\[1ex]
  &\wedge& S', \moduleinst = \allocmodule(S, \module, \externval^k, \val^\ast, (\reff^\ast)^n) \\
  &\wedge& F = \{ \AMODULE~\moduleinst, \ALOCALS~\epsilon \} \\[1ex]
  &\wedge& (S'; F; \expr_{\F{g}} \stepto^\ast S'; F; \val~\END)^\ast \\
  &\wedge& ((S'; F; \expr_{\F{e}} \stepto^\ast S'; F; \reff~\END)^\ast)^n \\
  &\wedge& (\tableaddr = \moduleinst.\MITABLES[\elem.\ETABLE])^\ast \\
  &\wedge& (\memaddr = \moduleinst.\MIMEMS[\data.\DMEM])^\ast \\
  &\wedge& (\funcaddr = \moduleinst.\MIFUNCS[\start.\SFUNC])^?)
\end{array}

where:

\begin{array}{@{}l}
\F{runelem}_i(\{\ETYPE~\X{et}, \EINIT~\reff^n, \EMODE~\EPASSIVE\}) \quad=\quad \epsilon \\
\F{runelem}_i(\{\ETYPE~\X{et}, \EINIT~\reff^n, \EMODE~\EACTIVE \{\ETABLE~0, \EOFFSET~\instr^\ast~\END\}\}) \quad=\\ \qquad
  \instr^\ast~(\I32.\CONST~0)~(\I32.\CONST~n)~(\TABLEINIT~i)~(\ELEMDROP~i) \\
\F{runelem}_i(\{\ETYPE~\X{et}, \EINIT~\reff^n, \EMODE~\EDECLARATIVE\}) \quad=\\ \qquad
  (\ELEMDROP~i) \\[1ex]
\F{rundata}_i(\{\DINIT~b^n, DMODE~\DPASSIVE\}) \quad=\quad \epsilon \\
\F{rundata}_i(\{\DINIT~b^n, DMODE~\DACTIVE \{\DMEM~0, \DOFFSET~\instr^\ast~\END\}\}) \quad=\\ \qquad
  \instr^\ast~(\I32.\CONST~0)~(\I32.\CONST~n)~(\MEMORYINIT~i)~(\DATADROP~i) \\
\end{array}

.. index:: ! invocation, module, module instance, function, export, function address, function instance, function type, value, stack, trap, store

Once a :ref:`module <syntax-module>` has been :ref:`instantiated <exec-instantiation>`, any exported function can be invoked externally via its :ref:`function address <syntax-funcaddr>` \funcaddr in the :ref:`store <syntax-store>` S and an appropriate list \val^\ast of argument :ref:`values <syntax-val>`.

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

The following steps are performed:

1. Assert: S.\SFUNCS[\funcaddr] exists.
2. Let \funcinst be the :ref:`function instance <syntax-funcinst>` S.\SFUNCS[\funcaddr].
3. Let [t_1^n] \to [t_2^m] be the :ref:`function type <syntax-functype>` \funcinst.\FITYPE.
4. If the length |\val^\ast| of the provided argument values is different from the number n of expected arguments, then:
   1. Fail.
5. For each :ref:`value type <syntax-valtype>` t_i in t_1^n and corresponding :ref:`value <syntax-val>` val_i in \val^\ast, do:
   1. If \val_i is not :ref:`valid <valid-val>` with value type t_i, then:
      1. Fail.
6. Let F be the dummy :ref:`frame <syntax-frame>` \{ \AMODULE~\{\}, \ALOCALS~\epsilon \}.
7. Push the frame F to the stack.
8. Push the values \val^\ast to the stack.
9. :ref:`Invoke <exec-invoke>` the function instance at address \funcaddr.

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

1. Assert: due to :ref:`validation <valid-func>`, m :ref:`values <syntax-val>` are on the top of the stack.
2. Pop \val_{\F{res}}^m from the stack.

The values \val_{\F{res}}^m are returned as the results of the invocation.

~\\[-1ex]
\begin{array}{@{}lcl}
\invoke(S, \funcaddr, \val^n) &=& S; F; \val^n~(\INVOKE~\funcaddr) \\
  &(\iff & S.\SFUNCS[\funcaddr].\FITYPE = [t_1^n] \to [t_2^m] \\
  &\wedge& (S \vdashval \val : t_1)^n \\
  &\wedge& F = \{ \AMODULE~\{\}, \ALOCALS~\epsilon \}) \\
\end{array}