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, and globals are allocated in a store $S$, as defined by the following auxiliary functions.

Functions

1. Let $\mathit{func}$ be the function to allocate and $\mathit{moduleinst}$ its module instance.

2. Let $\mathit{deftype}$ be the defined type $\mathit{moduleinst}.\mathsf{types}[\mathit{func}.\mathsf{type}]$.

3. Let $a$ be the first free function address in $S$.

4. Let $\mathit{funcinst}$ be the function instance $\{\mathsf{type}\mathit{deftype},\mathsf{module}\mathit{moduleinst},\mathsf{code}\mathit{func}\}$.

6. Append $\mathit{funcinst}$ to the $\mathsf{funcs}$ of $S$.

7. Return $a$.

$$\begin{array}{r}\\ \begin{array}{rll}\mathrm{allocfunc}(S,\mathit{func},\mathit{moduleinst})& =& S^{\prime },\mathit{funcaddr}\\ \text{where:}\hfill \\ \mathit{deftype}& =& \mathit{moduleinst}.\mathsf{types}[\mathit{func}.\mathsf{type}]\\ \mathit{funcaddr}& =& |S.\mathsf{funcs}|\\ \mathit{funcinst}& =& \{\mathsf{type}\mathit{deftype},\mathsf{module}\mathit{moduleinst},\mathsf{code}\mathit{func}\}\\ S^{\prime }& =& S\oplus \{\mathsf{funcs}\mathit{funcinst}\}\end{array}\end{array}$$

Host Functions

1. Let $\mathit{hostfunc}$ be the host function to allocate and $\mathit{deftype}$ its defined type.

2. Let $a$ be the first free function address in $S$.

3. Let $\mathit{funcinst}$ be the function instance $\{\mathsf{type}\mathit{deftype},\mathsf{hostcode}\mathit{hostfunc}\}$.

4. Append $\mathit{funcinst}$ to the $\mathsf{funcs}$ of $S$.

5. Return $a$.

$$\begin{array}{r}\\ \begin{array}{rll}\mathrm{allochostfunc}(S,\mathit{deftype},\mathit{hostfunc})& =& S^{\prime },\mathit{funcaddr}\\ \text{where:}\hfill \\ \mathit{funcaddr}& =& |S.\mathsf{funcs}|\\ \mathit{funcinst}& =& \{\mathsf{type}\mathit{deftype},\mathsf{hostcode}\mathit{hostfunc}\}\\ S^{\prime }& =& S\oplus \{\mathsf{funcs}\mathit{funcinst}\}\end{array}\end{array}$$

Note

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

Tables

1. Let $\mathit{tabletype}$ be the table type of the table to allocate and $\mathit{ref}$ the initialization value.

2. Let $(\{\mathsf{min}n,\mathsf{max}{m}^{?}\}\mathit{reftype})$ be the structure of table type $\mathit{tabletype}$.

3. Let $a$ be the first free table address in $S$.

4. Let $\mathit{tableinst}$ be the table instance $\{\mathsf{type}{\mathit{tabletype}}^{\prime },\mathsf{elem}{\mathit{ref}}^n\}$ with $n$ elements set to $\mathit{ref}$.

5. Append $\mathit{tableinst}$ to the $\mathsf{tables}$ of $S$.

6. Return $a$.

$$\begin{array}{r}\begin{array}{rll}\mathrm{alloctable}(S,\mathit{tabletype},\mathit{ref})& =& S^{\prime },\mathit{tableaddr}\\ \text{where:}\hfill \\ \mathit{tabletype}& =& \{\mathsf{min}n,\mathsf{max}{m}^{?}\}\mathit{reftype}\\ \mathit{tableaddr}& =& |S.\mathsf{tables}|\\ \mathit{tableinst}& =& \{\mathsf{type}\mathit{tabletype},\mathsf{elem}{\mathit{ref}}^n\}\\ S^{\prime }& =& S\oplus \{\mathsf{tables}\mathit{tableinst}\}\end{array}\end{array}$$

Memories

1. Let $\mathit{memtype}$ be the memory type of the memory to allocate.

2. Let $\{\mathsf{min}n,\mathsf{max}{m}^{?}\}$ be the structure of memory type $\mathit{memtype}$.

3. Let $a$ be the first free memory address in $S$.

4. Let $\mathit{meminst}$ be the memory instance $\{\mathsf{type}\mathit{memtype},\mathsf{data}(\mathtt{0}\mathtt{x}\mathtt{00}{)}^{n\cdot 64\mathrm{Ki}}\}$ that contains $n$ pages of zeroed bytes.

5. Append $\mathit{meminst}$ to the $\mathsf{mems}$ of $S$.

6. Return $a$.

$$\begin{array}{r}\begin{array}{rll}\mathrm{allocmem}(S,\mathit{memtype})& =& S^{\prime },\mathit{memaddr}\\ \text{where:}\hfill \\ \mathit{memtype}& =& \{\mathsf{min}n,\mathsf{max}{m}^{?}\}\\ \mathit{memaddr}& =& |S.\mathsf{mems}|\\ \mathit{meminst}& =& \{\mathsf{type}\mathit{memtype},\mathsf{data}(\mathtt{0}\mathtt{x}\mathtt{00}{)}^{n\cdot 64\mathrm{Ki}}\}\\ S^{\prime }& =& S\oplus \{\mathsf{mems}\mathit{meminst}\}\end{array}\end{array}$$

Globals

1. Let $\mathit{globaltype}$ be the global type of the global to allocate and $\mathit{val}$ its initialization value.

2. Let $a$ be the first free global address in $S$.

3. Let $\mathit{globalinst}$ be the global instance $\{\mathsf{type}\mathit{globaltype},\mathsf{value}\mathit{val}\}$.

4. Append $\mathit{globalinst}$ to the $\mathsf{globals}$ of $S$.

5. Return $a$.

$$\begin{array}{r}\begin{array}{rll}\mathrm{allocglobal}(S,\mathit{globaltype},\mathit{val})& =& S^{\prime },\mathit{globaladdr}\\ \text{where:}\hfill \\ \mathit{globaladdr}& =& |S.\mathsf{globals}|\\ \mathit{globalinst}& =& \{\mathsf{type}\mathit{globaltype},\mathsf{value}\mathit{val}\}\\ S^{\prime }& =& S\oplus \{\mathsf{globals}\mathit{globalinst}\}\end{array}\end{array}$$

Element segments

1. Let $\mathit{reftype}$ be the elements’ type and ${\mathit{ref}}^{\ast }$ the vector of references to allocate.

2. Let $a$ be the first free element address in $S$.

3. Let $\mathit{eleminst}$ be the element instance $\{\mathsf{type}\mathit{reftype},\mathsf{elem}{\mathit{ref}}^{\ast }\}$.

4. Append $\mathit{eleminst}$ to the $\mathsf{elems}$ of $S$.

5. Return $a$.

$$\begin{array}{r}\begin{array}{rll}\mathrm{allocelem}(S,\mathit{reftype},{\mathit{ref}}^{\ast })& =& S^{\prime },\mathit{elemaddr}\\ \text{where:}\hfill \\ \mathit{elemaddr}& =& |S.\mathsf{elems}|\\ \mathit{eleminst}& =& \{\mathsf{type}\mathit{reftype},\mathsf{elem}{\mathit{ref}}^{\ast }\}\\ S^{\prime }& =& S\oplus \{\mathsf{elems}\mathit{eleminst}\}\end{array}\end{array}$$

Data segments

1. Let $b^{\ast }$ be the vector of bytes to allocate.

2. Let $a$ be the first free data address in $S$.

3. Let $\mathit{datainst}$ be the data instance $\{\mathsf{data}{b}^{\ast }\}$.

4. Append $\mathit{datainst}$ to the $\mathsf{datas}$ of $S$.

5. Return $a$.

$$\begin{array}{r}\begin{array}{rll}\mathrm{allocdata}(S,b^{\ast })& =& S^{\prime },\mathit{dataaddr}\\ \text{where:}\hfill \\ \mathit{dataaddr}& =& |S.\mathsf{datas}|\\ \mathit{datainst}& =& \{\mathsf{data}{b}^{\ast }\}\\ S^{\prime }& =& S\oplus \{\mathsf{datas}\mathit{datainst}\}\end{array}\end{array}$$

Growing tables

1. Let $\mathit{tableinst}$ be the table instance to grow, $n$ the number of elements by which to grow it, and $\mathit{ref}$ the initialization value.

2. Let $\mathit{len}$ be $n$ added to the length of $\mathit{tableinst}.\mathsf{elem}$.

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

4. Let $\mathit{limits}t$ be the structure of table type $\mathit{tableinst}.\mathsf{type}$.

5. Let ${\mathit{limits}}^{\prime }$ be $\mathit{limits}$ with $\mathsf{min}$ updated to $\mathit{len}$.

6. If ${\mathit{limits}}^{\prime }$ is not valid, then fail.

7. Append ${\mathit{ref}}^n$ to $\mathit{tableinst}.\mathsf{elem}$.

8. Set $\mathit{tableinst}.\mathsf{type}$ to the table type ${\mathit{limits}}^{\prime }t$.

$$\begin{array}{r}\begin{array}{rll}\mathrm{growtable}(\mathit{tableinst},n,\mathit{ref})& =& \mathit{tableinst}\text{with}\mathsf{type}={\mathit{limits}}^{\prime }t\text{with}\mathsf{elem}=\mathit{tableinst}.\mathsf{elem}{\mathit{ref}}^n\\ & & (\begin{array}{rl}\text{if}& \mathit{len}=n+|\mathit{tableinst}.\mathsf{elem}|\\ \wedge & \mathit{len}<2^{32}\\ \wedge & \mathit{limits}t=\mathit{tableinst}.\mathsf{type}\\ \wedge & {\mathit{limits}}^{\prime }=\mathit{limits}\text{with}\mathsf{min}=\mathit{len}\\ \wedge & ⊢{\mathit{limits}}^{\prime }\text{ok})\end{array}\end{array}\end{array}$$

Growing memories

1. Let $\mathit{meminst}$ be the memory instance to grow and $n$ the number of pages by which to grow it.

2. Assert: The length of $\mathit{meminst}.\mathsf{data}$ is divisible by the page size $64\mathrm{Ki}$.

3. Let $\mathit{len}$ be $n$ added to the length of $\mathit{meminst}.\mathsf{data}$ divided by the page size $64\mathrm{Ki}$.

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

5. Let $\mathit{limits}$ be the structure of memory type $\mathit{meminst}.\mathsf{type}$.

6. Let ${\mathit{limits}}^{\prime }$ be $\mathit{limits}$ with $\mathsf{min}$ updated to $\mathit{len}$.

7. If ${\mathit{limits}}^{\prime }$ is not valid, then fail.

8. Append $n$ times $64\mathrm{Ki}$ bytes with value $\mathtt{0}\mathtt{x}\mathtt{00}$ to $\mathit{meminst}.\mathsf{data}$.

9. Set $\mathit{meminst}.\mathsf{type}$ to the memory type ${\mathit{limits}}^{\prime }$.

$$\begin{array}{r}\begin{array}{rll}\mathrm{growmem}(\mathit{meminst},n)& =& \mathit{meminst}\text{with}\mathsf{type}={\mathit{limits}}^{\prime }\text{with}\mathsf{data}=\mathit{meminst}.\mathsf{data}(\mathtt{0}\mathtt{x}\mathtt{00}{)}^{n\cdot 64\mathrm{Ki}}\\ & & (\begin{array}{rl}\text{if}& \mathit{len}=n+|\mathit{meminst}.\mathsf{data}|/64\mathrm{Ki}\\ \wedge & \mathit{len}\le 2^{16}\\ \wedge & \mathit{limits}=\mathit{meminst}.\mathsf{type}\\ \wedge & {\mathit{limits}}^{\prime }=\mathit{limits}\text{with}\mathsf{min}=\mathit{len}\\ \wedge & ⊢{\mathit{limits}}^{\prime }\text{ok})\end{array}\end{array}\end{array}$$

Modules

Todo

update prose for types

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

1. Let $\mathit{module}$ be the module to allocate and ${\mathit{externval}}_{\mathrm{im}}^{\ast }$ the vector of external values providing the module’s imports, ${\mathit{val}}_{\mathrm{g}}^{\ast }$ the initialization values of the module’s globals, ${\mathit{ref}}_{\mathrm{t}}^{\ast }$ the initializer reference of the module’s tables, and $({\mathit{ref}}_{\mathrm{e}}^{\ast }{)}^{\ast }$ the reference vectors of the module’s element segments.

2. For each defined type ${\mathit{deftype}}_i^{\prime }$ in $\mathit{module}.\mathsf{types}$, do:

   1. Let ${\mathit{deftype}}_i$ be the instantiation ${\mathit{deftype}}_i^{\prime }$ in $\mathit{moduleinst}$ defined below.

3. For each function ${\mathit{func}}_i$ in $\mathit{module}.\mathsf{funcs}$, do:

   1. Let ${\mathit{funcaddr}}_i$ be the function address resulting from allocating ${\mathit{func}}_i$ for the module instance $\mathit{moduleinst}$ defined below.

4. For each table ${\mathit{table}}_i$ in $\mathit{module}.\mathsf{tables}$, do:

   1. Let ${\mathit{limits}}_i{t}_i$ be the table type obtained by instantiating ${\mathit{table}}_i.\mathsf{type}$ in $\mathit{moduleinst}$ defined below.

   2. Let ${\mathit{tableaddr}}_i$ be the table address resulting from allocating ${\mathit{table}}_i.\mathsf{type}$ with initialization value ${\mathit{ref}}_{\mathrm{t}}^{\ast }[i]$.

5. For each memory ${\mathit{mem}}_i$ in $\mathit{module}.\mathsf{mems}$, do:

   1. Let ${\mathit{memtype}}_i$ be the memory type obtained by insantiating ${\mathit{mem}}_i.\mathsf{type}$ in $\mathit{moduleinst}$ defined below.

   2. Let ${\mathit{memaddr}}_i$ be the memory address resulting from allocating ${\mathit{memtype}}_i$.

6. For each global ${\mathit{global}}_i$ in $\mathit{module}.\mathsf{globals}$, do:

   1. Let ${\mathit{globaltype}}_i$ be the global type obtained by instantiating ${\mathit{global}}_i.\mathsf{type}$ in $\mathit{moduleinst}$ defined below.

   2. Let ${\mathit{globaladdr}}_i$ be the global address resulting from allocating ${\mathit{globaltype}}_i$ with initializer value ${\mathit{val}}_{\mathrm{g}}^{\ast }[i]$.

7. For each element segment ${\mathit{elem}}_i$ in $\mathit{module}.\mathsf{elems}$, do:

   1. Let ${\mathit{reftype}}_i$ be the element reference type obtained by instantiating <type-inst> ${\mathit{elem}}_i.\mathsf{type}$ in $\mathit{moduleinst}$ defined below.

   2. Let ${\mathit{elemaddr}}_i$ be the element address resulting from allocating a element instance of reference type ${\mathit{reftype}}_i$ with contents $({\mathit{ref}}_{\mathrm{e}}^{\ast }{)}^{\ast }[i]$.

8. For each data segment ${\mathit{data}}_i$ in $\mathit{module}.\mathsf{datas}$, do:

   1. Let ${\mathit{dataaddr}}_i$ be the data address resulting from allocating a data instance with contents ${\mathit{data}}_i.\mathsf{init}$.

9. Let ${\mathit{deftype}}^{\ast }$ be the concatenation of the defined types ${\mathit{deftype}}_i$ in index order.

10. Let ${\mathit{funcaddr}}^{\ast }$ be the concatenation of the function addresses ${\mathit{funcaddr}}_i$ in index order.

11. Let ${\mathit{tableaddr}}^{\ast }$ be the concatenation of the table addresses ${\mathit{tableaddr}}_i$ in index order.

12. Let ${\mathit{memaddr}}^{\ast }$ be the concatenation of the memory addresses ${\mathit{memaddr}}_i$ in index order.

13. Let ${\mathit{globaladdr}}^{\ast }$ be the concatenation of the global addresses ${\mathit{globaladdr}}_i$ in index order.

14. Let ${\mathit{elemaddr}}^{\ast }$ be the concatenation of the element addresses ${\mathit{elemaddr}}_i$ in index order.

15. Let ${\mathit{dataaddr}}^{\ast }$ be the concatenation of the data addresses ${\mathit{dataaddr}}_i$ in index order.

16. Let ${\mathit{funcaddr}}_{\mathrm{mod}}^{\ast }$ be the list of function addresses extracted from ${\mathit{externval}}_{\mathrm{im}}^{\ast }$, concatenated with ${\mathit{funcaddr}}^{\ast }$.

17. Let ${\mathit{tableaddr}}_{\mathrm{mod}}^{\ast }$ be the list of table addresses extracted from ${\mathit{externval}}_{\mathrm{im}}^{\ast }$, concatenated with ${\mathit{tableaddr}}^{\ast }$.

18. Let ${\mathit{memaddr}}_{\mathrm{mod}}^{\ast }$ be the list of memory addresses extracted from ${\mathit{externval}}_{\mathrm{im}}^{\ast }$, concatenated with ${\mathit{memaddr}}^{\ast }$.

19. Let ${\mathit{globaladdr}}_{\mathrm{mod}}^{\ast }$ be the list of global addresses extracted from ${\mathit{externval}}_{\mathrm{im}}^{\ast }$, concatenated with ${\mathit{globaladdr}}^{\ast }$.

20. For each export ${\mathit{export}}_i$ in $\mathit{module}.\mathsf{exports}$, do:

    1. If ${\mathit{export}}_i$ is a function export for function index $x$, then let ${\mathit{externval}}_i$ be the external value $\mathsf{func}({\mathit{funcaddr}}_{\mathrm{mod}}^{\ast }[x])$.

    2. Else, if ${\mathit{export}}_i$ is a table export for table index $x$, then let ${\mathit{externval}}_i$ be the external value $\mathsf{table}({\mathit{tableaddr}}_{\mathrm{mod}}^{\ast }[x])$.

    3. Else, if ${\mathit{export}}_i$ is a memory export for memory index $x$, then let ${\mathit{externval}}_i$ be the external value $\mathsf{mem}({\mathit{memaddr}}_{\mathrm{mod}}^{\ast }[x])$.

    4. Else, if ${\mathit{export}}_i$ is a global export for global index $x$, then let ${\mathit{externval}}_i$ be the external value $\mathsf{global}({\mathit{globaladdr}}_{\mathrm{mod}}^{\ast }[x])$.

    5. Let ${\mathit{exportinst}}_i$ be the export instance $\{\mathsf{name}({\mathit{export}}_i.\mathsf{name}),\mathsf{value}{\mathit{externval}}_i\}$.

21. Let ${\mathit{exportinst}}^{\ast }$ be the concatenation of the export instances ${\mathit{exportinst}}_i$ in index order.

22. Let $\mathit{moduleinst}$ be the module instance $\{\mathsf{types}{\mathit{deftype}}^{\ast },$ $\mathsf{funcaddrs}{\mathit{funcaddr}}_{\mathrm{mod}}^{\ast },$ $\mathsf{tableaddrs}{\mathit{tableaddr}}_{\mathrm{mod}}^{\ast },$ $\mathsf{memaddrs}{\mathit{memaddr}}_{\mathrm{mod}}^{\ast },$ $\mathsf{globaladdrs}{\mathit{globaladdr}}_{\mathrm{mod}}^{\ast },$ $\mathsf{exports}{\mathit{exportinst}}^{\ast }\}$.

23. Return $\mathit{moduleinst}$.

$$\begin{array}{r}\\ \begin{array}{rll}\mathrm{allocmodule}(S,\mathit{module},{\mathit{externval}}_{\mathrm{im}}^{\ast },{\mathit{val}}_{\mathrm{g}}^{\ast },{\mathit{ref}}_{\mathrm{t}}^{\ast },({\mathit{ref}}_{\mathrm{e}}^{\ast }{)}^{\ast })& =& S^{\prime },\mathit{moduleinst}\end{array}\end{array}$$

where:

$$\begin{array}{r}\begin{array}{rll}{\mathit{table}}^{\ast }& =& \mathit{module}.\mathsf{tables}\\ {\mathit{mem}}^{\ast }& =& \mathit{module}.\mathsf{mems}\\ {\mathit{global}}^{\ast }& =& \mathit{module}.\mathsf{globals}\\ {\mathit{elem}}^{\ast }& =& \mathit{module}.\mathsf{elems}\\ {\mathit{data}}^{\ast }& =& \mathit{module}.\mathsf{datas}\\ {\mathit{export}}^{\ast }& =& \mathit{module}.\mathsf{exports}\\ \mathit{moduleinst}& =& \{\begin{array}{c}\mathsf{types}{\mathit{deftype}}^{\ast },\\ \mathsf{funcaddrs}\mathrm{funcs}({\mathit{externval}}_{\mathrm{im}}^{\ast }){\mathit{funcaddr}}^{\ast },\\ \mathsf{tableaddrs}\mathrm{tables}({\mathit{externval}}_{\mathrm{im}}^{\ast }){\mathit{tableaddr}}^{\ast },\\ \mathsf{memaddrs}\mathrm{mems}({\mathit{externval}}_{\mathrm{im}}^{\ast }){\mathit{memaddr}}^{\ast },\\ \mathsf{globaladdrs}\mathrm{globals}({\mathit{externval}}_{\mathrm{im}}^{\ast }){\mathit{globaladdr}}^{\ast },\\ \mathsf{elemaddrs}{\mathit{elemaddr}}^{\ast },\\ \mathsf{dataaddrs}{\mathit{dataaddr}}^{\ast },\\ \mathsf{exports}{\mathit{exportinst}}^{\ast }\}\end{array}\\ {\mathit{deftype}}^{\ast }& =& {\mathrm{alloctype}}^{\ast }(\mathit{module}.\mathsf{types})\\ S_1,{\mathit{funcaddr}}^{\ast }& =& {\mathrm{allocfunc}}^{\ast }(S,\mathit{module}.\mathsf{funcs},\mathit{moduleinst})\\ S_2,{\mathit{tableaddr}}^{\ast }& =& {\mathrm{alloctable}}^{\ast }(S_1,{\mathrm{clos}}_{\mathit{moduleinst}}(\mathit{table}.\mathsf{type}{)}^{\ast },{\mathit{ref}}_{\mathrm{t}}^{\ast })(\text{where}(\mathit{table}.\mathsf{type}{)}^{\ast }=(\mathit{limits}t{)}^{\ast })\\ S_3,{\mathit{memaddr}}^{\ast }& =& {\mathrm{allocmem}}^{\ast }(S_2,{\mathrm{clos}}_{\mathit{moduleinst}}(\mathit{mem}.\mathsf{type}{)}^{\ast })\\ S_4,{\mathit{globaladdr}}^{\ast }& =& {\mathrm{allocglobal}}^{\ast }(S_3,{\mathrm{clos}}_{\mathit{moduleinst}}(\mathit{global}.\mathsf{type}{)}^{\ast },{\mathit{val}}_{\mathrm{g}}^{\ast })\\ S_5,{\mathit{elemaddr}}^{\ast }& =& {\mathrm{allocelem}}^{\ast }(S_4,{\mathrm{clos}}_{\mathit{moduleinst}}(\mathit{elem}.\mathsf{type}{)}^{\ast },({\mathit{ref}}_{\mathrm{e}}^{\ast }{)}^{\ast })\\ S^{\prime },{\mathit{dataaddr}}^{\ast }& =& {\mathrm{allocdata}}^{\ast }(S_5,\mathit{data}.{\mathsf{init}}^{\ast })\\ {\mathit{exportinst}}^{\ast }& =& \{\mathsf{name}(\mathit{export}.\mathsf{name}),\mathsf{value}{\mathit{externval}}_{\mathrm{ex}}{\}}^{\ast }\\ \mathrm{funcs}({\mathit{externval}}_{\mathrm{ex}}^{\ast })& =& (\mathit{moduleinst}.\mathsf{funcaddrs}[x]{)}^{\ast }(\text{where}{x}^{\ast }=\mathrm{funcs}({\mathit{export}}^{\ast }))\\ \mathrm{tables}({\mathit{externval}}_{\mathrm{ex}}^{\ast })& =& (\mathit{moduleinst}.\mathsf{tableaddrs}[x]{)}^{\ast }(\text{where}{x}^{\ast }=\mathrm{tables}({\mathit{export}}^{\ast }))\\ \mathrm{mems}({\mathit{externval}}_{\mathrm{ex}}^{\ast })& =& (\mathit{moduleinst}.\mathsf{memaddrs}[x]{)}^{\ast }(\text{where}{x}^{\ast }=\mathrm{mems}({\mathit{export}}^{\ast }))\\ \mathrm{globals}({\mathit{externval}}_{\mathrm{ex}}^{\ast })& =& (\mathit{moduleinst}.\mathsf{globaladdrs}[x]{)}^{\ast }(\text{where}{x}^{\ast }=\mathrm{globals}({\mathit{export}}^{\ast }))\end{array}\end{array}$$

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

$$\begin{array}{r}\begin{array}{rll}{\mathrm{allocx}}^{\ast }(S_0,X^n,\dots )& =& S_n,a^n\\ \text{where for all }i<n\text{:}\hfill \\ S_{i+1},a^n[i]& =& \mathrm{allocx}(S_i,X^n[i],\dots )\end{array}\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.

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

$$\begin{array}{r}\begin{array}{r}{\mathrm{alloctype}}^{\ast }({\mathit{rectype}}^n)={\mathit{deftype}}^{\ast }\\ \text{where for all }i<n\text{:}\hfill \\ {\mathit{rectype}}^n[i]& =& \mathsf{rec}{\mathit{subtype}}_i^{m_i}\\ {\mathit{deftype}}^{\ast }[x_i\mathbf{:}{m}_i]& =& {\mathrm{roll}}_{x_i}^{\ast }(\mathsf{rec}{\mathit{subtype}}_i^{m_i})[\mathbf{:=}{\mathit{deftype}}^{\ast }[0\mathbf{:}{x}_i]]\\ x_{i+1}& =& x_i+m_i\\ x_n& =& |{\mathit{deftype}}^{\ast }|\end{array}\end{array}$$

Note

The definition of module allocation is mutually recursive with the allocation of its associated functions, because the resulting module instance $\mathit{moduleinst}$ 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 module $\mathit{module}$ is instantiated with a list of external values ${\mathit{externval}}^n$ supplying the required imports as follows.

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

1. If $\mathit{module}$ is not valid, then:

   1. Fail.

2. Assert: $\mathit{module}$ is valid with external types ${\mathit{externtype}}_{\mathrm{im}}^m$ classifying its imports.

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

   1. Fail.

4. For each external value ${\mathit{externval}}_i$ in ${\mathit{externval}}^n$ and external type ${\mathit{externtype}}_i^{\prime }$ in ${\mathit{externtype}}_{\mathrm{im}}^n$, do:

   1. If ${\mathit{externval}}_i$ is not valid with an external type ${\mathit{externtype}}_i$ in store $S$, then:

      1. Fail.

   2. Let ${\mathit{externtype}}_i^{″}$ be the external type obtained by instantiating ${\mathit{externtype}}_i^{\prime }$ in $\mathit{moduleinst}$ defined below.

   3. If ${\mathit{externtype}}_i$ does not match ${\mathit{externtype}}_i^{″}$, then:

      1. Fail.

6. Let $F$ be the auxiliary frame $\{\mathsf{module}\mathit{moduleinst},\mathsf{locals}ϵ\}$, that consists of the final module instance $\mathit{moduleinst}$, defined below.

7. Push the frame $F$ to the stack.

8. Let ${\mathit{val}}_{\mathrm{g}}^{\ast }$ be the vector of global initialization values determined by $\mathit{module}$ and ${\mathit{externval}}^n$. These may be calculated as follows.

   1. For each global ${\mathit{global}}_i$ in $\mathit{module}.\mathsf{globals}$, do:

      1. Let ${\mathit{val}}_{\mathrm{g}i}$ be the result of evaluating the initializer expression ${\mathit{global}}_i.\mathsf{init}$.

   2. Assert: due to validation, the frame $F$ is now on the top of the stack.

   3. Let ${\mathit{val}}_{\mathrm{g}}^{\ast }$ be the concatenation of ${\mathit{val}}_{\mathrm{g}i}$ in index order.

9. Let ${\mathit{ref}}_{\mathrm{t}}^{\ast }$ be the vector of table initialization references determined by $\mathit{module}$ and ${\mathit{externval}}^n$. These may be calculated as follows.

   1. For each table ${\mathit{table}}_i$ in $\mathit{module}.\mathsf{tables}$, do:

      1. Let ${\mathit{val}}_{\mathrm{t}i}$ be the result of evaluating the initializer expression ${\mathit{table}}_i.\mathsf{init}$.

      2. Assert: due to validation, ${\mathit{val}}_{\mathrm{t}i}$ is a reference.

      3. Let ${\mathit{ref}}_{\mathrm{t}i}$ be the reference ${\mathit{val}}_{\mathrm{t}i}$.

   2. Assert: due to validation, the frame $F$ is now on the top of the stack.

   3. Let ${\mathit{ref}}_{\mathrm{t}}^{\ast }$ be the concatenation of ${\mathit{ref}}_{ti}$ in index order.

10. Let $({\mathit{ref}}_{\mathrm{e}}^{\ast }{)}^{\ast }$ be the list of reference vectors determined by the element segments in $\mathit{module}$. These may be calculated as follows.

    1. For each element segment ${\mathit{elem}}_i$ in $\mathit{module}.\mathsf{elems}$, and for each element expression ${\mathit{expr}}_{ij}$ in ${\mathit{elem}}_i.\mathsf{init}$, do:

       1. Let ${\mathit{ref}}_{ij}$ be the result of evaluating the initializer expression ${\mathit{expr}}_{ij}$.

    2. Let ${\mathit{ref}}_i^{\ast }$ be the concatenation of function elements ${\mathit{ref}}_{ij}$ in order of index $j$.

    3. Let $({\mathit{ref}}_{\mathrm{e}}^{\ast }{)}^{\ast }$ be the concatenation of function element vectors ${\mathit{ref}}_i^{\ast }$ in order of index $i$.

11. Let $\mathit{moduleinst}$ be a new module instance allocated from $\mathit{module}$ in store $S$ with imports ${\mathit{externval}}^n$, global initializer values ${\mathit{val}}_{\mathrm{g}}^{\ast }$, table initializer values ${\mathit{ref}}_{\mathrm{t}}^{\ast }$, and element segment contents $({\mathit{ref}}_{\mathrm{e}}^{\ast }{)}^{\ast }$, and let $S^{\prime }$ be the extended store produced by module allocation.

12. For each element segment ${\mathit{elem}}_i$ in $\mathit{module}.\mathsf{elems}$ whose mode is of the form $\mathsf{active}\{\mathsf{table}{\mathit{tableidx}}_i,\mathsf{offset}{\mathit{einstr}}_i^{\ast }\mathsf{end}\}$, do:

    1. Let $n$ be the length of the vector ${\mathit{elem}}_i.\mathsf{init}$.

    2. Execute the instruction sequence ${\mathit{einstr}}_i^{\ast }$.

    3. Execute the instruction $\mathsf{i}\mathsf{32}.\mathsf{const}0$.

    4. Execute the instruction $\mathsf{i}\mathsf{32}.\mathsf{const}n$.

    5. Execute the instruction $\mathsf{table}\mathsf{.}\mathsf{init}{\mathit{tableidx}}_{i}i$.

    6. Execute the instruction $\mathsf{elem}\mathsf{.}\mathsf{drop}i$.

13. For each element segment ${\mathit{elem}}_i$ in $\mathit{module}.\mathsf{elems}$ whose mode is of the form $\mathsf{declarative}$, do:

    1. Execute the instruction $\mathsf{elem}\mathsf{.}\mathsf{drop}i$.

14. For each data segment ${\mathit{data}}_i$ in $\mathit{module}.\mathsf{datas}$ whose mode is of the form $\mathsf{active}\{\mathsf{memory}{\mathit{memidx}}_i,\mathsf{offset}{\mathit{dinstr}}_i^{\ast }\mathsf{end}\}$, do:

    1. Assert: ${\mathit{memidx}}_i$ is $0$.

    2. Let $n$ be the length of the vector ${\mathit{data}}_i.\mathsf{init}$.

    3. Execute the instruction sequence ${\mathit{dinstr}}_i^{\ast }$.

    4. Execute the instruction $\mathsf{i}\mathsf{32}.\mathsf{const}0$.

    5. Execute the instruction $\mathsf{i}\mathsf{32}.\mathsf{const}n$.

    6. Execute the instruction $\mathsf{memory}\mathsf{.}\mathsf{init}i$.

    7. Execute the instruction $\mathsf{data}\mathsf{.}\mathsf{drop}i$.

15. If the start function $\mathit{module}.\mathsf{start}$ is not empty, then:

    1. Let $\mathit{start}$ be the start function $\mathit{module}.\mathsf{start}$.

    2. Execute the instruction $\mathsf{call}\mathit{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{array}{r}\\ \begin{array}{rcl}\mathrm{instantiate}(S,\mathit{module},{\mathit{externval}}^k)& =& S^{\prime };F;\begin{array}{c}{\mathrm{runelem}}_0({\mathit{elem}}^n[0])\dots {\mathrm{runelem}}_{n-1}({\mathit{elem}}^n[n-1])\\ {\mathrm{rundata}}_0({\mathit{data}}^m[0])\dots {\mathrm{rundata}}_{m-1}({\mathit{data}}^m[m-1])\\ (\mathsf{call}\mathit{start}.\mathsf{func}{)}^{?}\end{array}\\ & (\text{if}& ⊢\mathit{module}:{\mathit{externtype}}_{\mathrm{im}}^k\to {\mathit{externtype}}_{\mathrm{ex}}^{\ast }\\ & \wedge & (S^{\prime }⊢\mathit{externval}:\mathit{externtype}{)}^k\\ & \wedge & (S^{\prime }⊢\mathit{externtype}\le {\mathrm{clos}}_{\mathit{moduleinst}}({\mathit{externtype}}_{\mathrm{im}}){)}^k\\ & \wedge & \mathit{module}.\mathsf{globals}={\mathit{global}}^{\ast }\\ & \wedge & \mathit{module}.\mathsf{elems}={\mathit{elem}}^n\\ & \wedge & \mathit{module}.\mathsf{datas}={\mathit{data}}^m\\ & \wedge & \mathit{module}.\mathsf{start}={\mathit{start}}^{?}\\ & \wedge & ({\mathit{expr}}_{\mathrm{g}}=\mathit{global}.\mathsf{init}{)}^{\ast }\\ & \wedge & ({\mathit{expr}}_{\mathrm{t}}=\mathit{table}.\mathsf{init}{)}^{\ast }\\ & \wedge & ({\mathit{expr}}_{\mathrm{e}}^{\ast }=\mathit{elem}.\mathsf{init}{)}^n\\ & \wedge & S^{\prime },\mathit{moduleinst}=\mathrm{allocmodule}(S,\mathit{module},{\mathit{externval}}^k,{\mathit{val}}^{\ast },({\mathit{ref}}^{\ast }{)}^n)\\ & \wedge & F=\{\mathsf{module}\mathit{moduleinst},\mathsf{locals}ϵ\}\\ & \wedge & (S^{\prime };F;{\mathit{expr}}_{\mathrm{g}}{\hookrightarrow }^{\ast }{S}^{\prime };F;{\mathit{val}}_{\mathrm{g}}\mathsf{end}{)}^{\ast }\\ & \wedge & (S^{\prime };F;{\mathit{expr}}_{\mathrm{t}}{\hookrightarrow }^{\ast }{S}^{\prime };F;{\mathit{ref}}_{\mathrm{t}}\mathsf{end}{)}^{\ast }\\ & \wedge & ((S^{\prime };F;{\mathit{expr}}_{\mathrm{e}}{\hookrightarrow }^{\ast }{S}^{\prime };F;{\mathit{ref}}_{\mathrm{e}}\mathsf{end}{)}^{\ast }{)}^n)\end{array}\end{array}$$

where:

$$\begin{array}{r}\begin{array}{l}{\mathrm{runelem}}_i(\{\mathsf{type}\mathit{et},\mathsf{init}{\mathit{expr}}^n,\mathsf{mode}\mathsf{passive}\})=ϵ\\ {\mathrm{runelem}}_i(\{\mathsf{type}\mathit{et},\mathsf{init}{\mathit{expr}}^n,\mathsf{mode}\mathsf{active}\{\mathsf{table}x,\mathsf{offset}{\mathit{instr}}^{\ast }\mathsf{end}\}\})=\\ {\mathit{instr}}^{\ast }(\mathsf{i}\mathsf{32}.\mathsf{const}0)(\mathsf{i}\mathsf{32}.\mathsf{const}n)(\mathsf{table}\mathsf{.}\mathsf{init}xi)(\mathsf{elem}\mathsf{.}\mathsf{drop}i)\\ {\mathrm{runelem}}_i(\{\mathsf{type}\mathit{et},\mathsf{init}{\mathit{expr}}^n,\mathsf{mode}\mathsf{declarative}\})=\\ (\mathsf{elem}\mathsf{.}\mathsf{drop}i)\\ {\mathrm{rundata}}_i(\{\mathsf{init}{b}^n,\mathsf{mode}\mathsf{passive}\})=\\ ϵ\\ {\mathrm{rundata}}_i(\{\mathsf{init}{b}^n,\mathsf{mode}\mathsf{active}\{\mathsf{memory}0,\mathsf{offset}{\mathit{instr}}^{\ast }\mathsf{end}\}\})=\\ {\mathit{instr}}^{\ast }(\mathsf{i}\mathsf{32}.\mathsf{const}0)(\mathsf{i}\mathsf{32}.\mathsf{const}n)(\mathsf{memory}\mathsf{.}\mathsf{init}i)(\mathsf{data}\mathsf{.}\mathsf{drop}i)\end{array}\end{array}$$

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 ${\mathit{val}}_{\mathrm{g}}^{\ast }$, ${\mathit{ref}}_{\mathrm{t}}$, and element segment contents $({\mathit{ref}}^{\ast }{)}^{\ast }$ are passed to the module allocator while depending on the module instance $\mathit{moduleinst}$ and store $S^{\prime }$ 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

Once a module has been instantiated, any exported function can be invoked externally via its function address $\mathit{funcaddr}$ in the store $S$ and an appropriate list ${\mathit{val}}^{\ast }$ of argument values.

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

Note

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

The following steps are performed:

1. Assert: $S.\mathsf{funcs}[\mathit{funcaddr}]$ exists.

2. Let $\mathit{funcinst}$ be the function instance $S.\mathsf{funcs}[\mathit{funcaddr}]$.

3. Let $\mathsf{func}[t_1^n]\to [t_2^m]$ be the composite type $\mathrm{expand}(\mathit{funcinst}.\mathsf{type})$.

4. If the length $|{\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 $va{l}_i$ in ${\mathit{val}}^{\ast }$, do:

   1. If ${\mathit{val}}_i$ is not valid with value type $t_i$, then:

      1. Fail.

6. Let $F$ be the dummy frame $\{\mathsf{module}\{\},\mathsf{locals}ϵ\}$.

7. Push the frame $F$ to the stack.

8. Push the values ${\mathit{val}}^{\ast }$ to the stack.

9. Invoke the function instance at address $\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 ${\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 ${\mathit{val}}_{\mathrm{res}}^m$ are returned as the results of the invocation.

$$\begin{array}{r}\\ \begin{array}{lcl}\mathrm{invoke}(S,\mathit{funcaddr},{\mathit{val}}^n)& =& S;F;{\mathit{val}}^n(\mathsf{invoke}\mathit{funcaddr})\\ & (\text{if}& \mathrm{expand}(S.\mathsf{funcs}[\mathit{funcaddr}].\mathsf{type})=\mathsf{func}[t_1^n]\to [t_2^m]\\ & \wedge & (S⊢\mathit{val}:t_1{)}^n\\ & \wedge & F=\{\mathsf{module}\{\},\mathsf{locals}ϵ\})\end{array}\end{array}$$