Embedding¶

A WebAssembly implementation will typically be embedded into a host environment. An embedder implements the connection between such a host environment and the WebAssembly semantics as defined in the main body of this specification. An embedder is expected to interact with the semantics in well-defined ways.

This section defines a suitable interface to the WebAssembly semantics in the form of entry points through which an embedder can access it. The interface is intended to be complete, in the sense that an embedder does not need to reference other functional parts of the WebAssembly specification directly.

Note

On the other hand, an embedder does not need to provide the host environment with access to all functionality defined in this interface. For example, an implementation may not support parsing of the text format.

In the description of the embedder interface, syntactic classes from the abstract syntax and the runtime’s abstract machine are used as names for variables that range over the possible objects from that class. Hence, these syntactic classes can also be interpreted as types.

Failure of an interface operation is indicated by an auxiliary syntactic class:

\[\begin{split}\begin{array}{llll} \def\mathdef117#1{{}}\mathdef117{(error)} & \href{../appendix/embedding.html#embed-error}{\mathit{error}} &::=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} \\ \end{array}\end{split}\]

In addition to the error conditions specified explicitly in this section, implementations may also return errors when specific implementation limitations are reached.

Note

Errors are abstract and unspecific with this definition. Implementations can refine it to carry suitable classifications and diagnostic messages.

Store¶

\(\mathrm{init\_store}() : \href{../exec/runtime.html#syntax-store}{\mathit{store}}\)¶

Return the empty store.

\[\begin{split}\begin{array}{lclll} \mathrm{init\_store}() &=& \{ \href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}~\epsilon,~ \href{../exec/runtime.html#syntax-store}{\mathsf{mems}}~\epsilon,~ \href{../exec/runtime.html#syntax-store}{\mathsf{tables}}~\epsilon,~ \href{../exec/runtime.html#syntax-store}{\mathsf{globals}}~\epsilon \} \\ \end{array}\end{split}\]

Modules¶

\(\mathrm{decode\_module}(\href{../syntax/values.html#syntax-byte}{\mathit{byte}}^\ast) : \href{../syntax/modules.html#syntax-module}{\mathit{module}} ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}}\)¶

If there exists a derivation for the byte sequence \(\href{../syntax/values.html#syntax-byte}{\mathit{byte}}^\ast\) as a \(\href{../binary/modules.html#binary-module}{\mathtt{module}}\) according to the binary grammar for modules, yielding a module \(m\), then return \(m\).
Else, return \(\href{../appendix/embedding.html#embed-error}{\mathsf{error}}\).

\[\begin{split}\begin{array}{lclll} \mathrm{decode\_module}(b^\ast) &=& m && (\mathrel{\mbox{if}} \href{../binary/modules.html#binary-module}{\mathtt{module}} \stackrel\ast\Longrightarrow m{:}b^\ast) \\ \mathrm{decode\_module}(b^\ast) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]

\(\mathrm{parse\_module}(\href{../syntax/values.html#syntax-name}{\mathit{codepoint}}^\ast) : \href{../syntax/modules.html#syntax-module}{\mathit{module}} ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}}\)¶

If there exists a derivation for the source \(\href{../syntax/values.html#syntax-name}{\mathit{codepoint}}^\ast\) as a \(\href{../text/modules.html#text-module}{\mathtt{module}}\) according to the text grammar for modules, yielding a module \(m\), then return \(m\).
Else, return \(\href{../appendix/embedding.html#embed-error}{\mathsf{error}}\).

\[\begin{split}\begin{array}{lclll} \mathrm{parse\_module}(c^\ast) &=& m && (\mathrel{\mbox{if}} \href{../text/modules.html#text-module}{\mathtt{module}} \stackrel\ast\Longrightarrow m{:}c^\ast) \\ \mathrm{parse\_module}(c^\ast) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]

\(\mathrm{validate\_module}(\href{../syntax/modules.html#syntax-module}{\mathit{module}}) : \href{../appendix/embedding.html#embed-error}{\mathit{error}}^?\)¶

If \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) is valid, then return nothing.
Else, return \(\href{../appendix/embedding.html#embed-error}{\mathsf{error}}\).

\[\begin{split}\begin{array}{lclll} \mathrm{validate\_module}(m) &=& \epsilon && (\mathrel{\mbox{if}} {} \href{../valid/modules.html#valid-module}{\vdash} m : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}^\ast \href{../syntax/types.html#syntax-functype}{\rightarrow} {\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}'}^\ast) \\ \mathrm{validate\_module}(m) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]

\(\mathrm{instantiate\_module}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../syntax/modules.html#syntax-module}{\mathit{module}}, \href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast) : (\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}} ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}})\)¶

Try instantiating \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) in \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}\) with external values \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast\) as imports:

If it succeeds with a module instance \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\), then let \(\mathit{result}\) be \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\).

Else, let \(\mathit{result}\) be \(\href{../appendix/embedding.html#embed-error}{\mathsf{error}}\).

Return the new store paired with \(\mathit{result}\).

\[\begin{split}\begin{array}{lclll} \mathrm{instantiate\_module}(S, m, \mathit{ev}^\ast) &=& (S', F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}) && (\mathrel{\mbox{if}} \href{../exec/modules.html#exec-instantiation}{\mathrm{instantiate}}(S, m, \mathit{ev}^\ast) \href{../exec/conventions.html#formal-notation}{\hookrightarrow}^\ast S'; F; \epsilon) \\ \mathrm{instantiate\_module}(S, m, \mathit{ev}^\ast) &=& (S', \href{../appendix/embedding.html#embed-error}{\mathsf{error}}) && (\mathrel{\mbox{if}} \href{../exec/modules.html#exec-instantiation}{\mathrm{instantiate}}(S, m, \mathit{ev}^\ast) \href{../exec/conventions.html#formal-notation}{\hookrightarrow}^\ast S'; F; \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}) \\ \end{array}\end{split}\]

Note

The store may be modified even in case of an error.

\(\mathrm{module\_imports}(\href{../syntax/modules.html#syntax-module}{\mathit{module}}) : (\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}})^\ast\)¶

Assert: \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) is valid with external import types \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}^\ast\) and external export types \({\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}'}^\ast\).
Let \(\href{../syntax/modules.html#syntax-import}{\mathit{import}}^\ast\) be the imports \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{imports}}\).
Assert: the length of \(\href{../syntax/modules.html#syntax-import}{\mathit{import}}^\ast\) equals the length of \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}^\ast\).
For each \(\href{../syntax/modules.html#syntax-import}{\mathit{import}}_i\) in \(\href{../syntax/modules.html#syntax-import}{\mathit{import}}^\ast\) and corresponding \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_i\) in \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}^\ast\), do:

Let \(\mathit{result}_i\) be the triple \((\href{../syntax/modules.html#syntax-import}{\mathit{import}}_i.\href{../syntax/modules.html#syntax-import}{\mathsf{module}}, \href{../syntax/modules.html#syntax-import}{\mathit{import}}_i.\href{../syntax/modules.html#syntax-import}{\mathsf{name}}, \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_i)\).

Return the concatenation of all \(\mathit{result}_i\), in index order.

\[\begin{split}~ \\ \begin{array}{lclll} \mathrm{module\_imports}(m) &=& (\mathit{im}.\href{../syntax/modules.html#syntax-import}{\mathsf{module}}, \mathit{im}.\href{../syntax/modules.html#syntax-import}{\mathsf{name}}, \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}})^\ast \\ && \qquad (\mathrel{\mbox{if}} \mathit{im}^\ast = m.\href{../syntax/modules.html#syntax-module}{\mathsf{imports}} \wedge {} \href{../valid/modules.html#valid-module}{\vdash} m : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}^\ast \href{../syntax/types.html#syntax-functype}{\rightarrow} {\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}'}^\ast) \\ \end{array}\end{split}\]

\(\mathrm{module\_exports}(\href{../syntax/modules.html#syntax-module}{\mathit{module}}) : (\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}})^\ast\)¶

Assert: \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) is valid with external import types \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}^\ast\) and external export types \({\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}'}^\ast\).
Let \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}^\ast\) be the exports \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{exports}}\).
Assert: the length of \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}^\ast\) equals the length of \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}^\ast\).
For each \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i\) in \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}^\ast\) and corresponding \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}'_i\) in \({\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}'}^\ast\), do:

Let \(\mathit{result}_i\) be the pair \((\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i.\href{../syntax/modules.html#syntax-export}{\mathsf{name}}, \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}'_i)\).

Return the concatenation of all \(\mathit{result}_i\), in index order.

\[\begin{split}~ \\ \begin{array}{lclll} \mathrm{module\_exports}(m) &=& (\mathit{ex}.\href{../syntax/modules.html#syntax-export}{\mathsf{name}}, \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}')^\ast \\ && \qquad (\mathrel{\mbox{if}} \mathit{ex}^\ast = m.\href{../syntax/modules.html#syntax-module}{\mathsf{exports}} \wedge {} \href{../valid/modules.html#valid-module}{\vdash} m : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}^\ast \href{../syntax/types.html#syntax-functype}{\rightarrow} {\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}'}^\ast) \\ \end{array}\end{split}\]

Exports¶

\(\mathrm{get\_export}(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}, \href{../syntax/values.html#syntax-name}{\mathit{name}}) : \href{../exec/runtime.html#syntax-externval}{\mathit{externval}} ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}}\)¶

Assert: due to validity of the module instance \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\), all its export names are different.
If there exists an \(\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}_i\) in \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{exports}}\) such that name \(\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}_i.\href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}\) equals \(\href{../syntax/values.html#syntax-name}{\mathit{name}}\), then:
1. Return the external value \(\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}_i.\href{../exec/runtime.html#syntax-exportinst}{\mathsf{value}}\).
Else, return \(\href{../appendix/embedding.html#embed-error}{\mathsf{error}}\).

\[\begin{split}~ \\ \begin{array}{lclll} \mathrm{get\_export}(m, \href{../syntax/values.html#syntax-name}{\mathit{name}}) &=& m.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{exports}}[i].\href{../exec/runtime.html#syntax-exportinst}{\mathsf{value}} && (\mathrel{\mbox{if}} m.\href{../syntax/modules.html#syntax-module}{\mathsf{exports}}[i].\href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}} = \href{../syntax/values.html#syntax-name}{\mathit{name}}) \\ \mathrm{get\_export}(m, \href{../syntax/values.html#syntax-name}{\mathit{name}}) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]

Functions¶

\(\mathrm{alloc\_func}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../syntax/types.html#syntax-functype}{\mathit{functype}}, \href{../exec/runtime.html#syntax-hostfunc}{\mathit{hostfunc}}) : (\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}})\)¶

Let \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}\) be the result of allocating a host function in \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}\) with function type \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\) and host function code \(\href{../exec/runtime.html#syntax-hostfunc}{\mathit{hostfunc}}\).
Return the new store paired with \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}\).

\[\begin{split}\begin{array}{lclll} \mathrm{alloc\_func}(S, \mathit{ft}, \mathit{code}) &=& (S', \mathit{a}) && (\mathrel{\mbox{if}} \href{../exec/modules.html#alloc-hostfunc}{\mathrm{allochostfunc}}(S, \mathit{ft}, \mathit{code}) = S', \mathit{a}) \\ \end{array}\end{split}\]

Note

This operation assumes that \(\href{../exec/runtime.html#syntax-hostfunc}{\mathit{hostfunc}}\) satisfies the pre- and post-conditions required for a function instance with type \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\).

Regular (non-host) function instances can only be created indirectly through module instantiation.

\(\mathrm{type\_func}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}) : \href{../syntax/types.html#syntax-functype}{\mathit{functype}}\)¶

Assert: \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}]\) exists.
Assert: the external value \(\href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}\) is valid with external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\).
Return \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\).

\[\begin{split}\begin{array}{lclll} \mathrm{type\_func}(S, a) &=& \mathit{ft} && (\mathrel{\mbox{if}} S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~a : \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\mathit{ft}) \\ \end{array}\end{split}\]

\(\mathrm{invoke\_func}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}, \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast) : (\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}})\)¶

Assert: \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}]\) exists.
Try invoking the function \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}\) in \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}\) with values \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\) as arguments:

If it succeeds with values \({\href{../exec/runtime.html#syntax-val}{\mathit{val}}'}^\ast\) as results, then let \(\mathit{result}\) be \({\href{../exec/runtime.html#syntax-val}{\mathit{val}}'}^\ast\).

Else it has trapped, hence let \(\mathit{result}\) be \(\href{../appendix/embedding.html#embed-error}{\mathsf{error}}\).

Return the new store paired with \(\mathit{result}\).

\[\begin{split}~ \\ \begin{array}{lclll} \mathrm{invoke\_func}(S, a, v^\ast) &=& (S', {v'}^\ast) && (\mathrel{\mbox{if}} \href{../exec/modules.html#exec-invocation}{\mathrm{invoke}}(S, a, v^\ast) \href{../exec/conventions.html#formal-notation}{\hookrightarrow}^\ast S'; F; {v'}^\ast) \\ \mathrm{invoke\_func}(S, a, v^\ast) &=& (S', \href{../appendix/embedding.html#embed-error}{\mathsf{error}}) && (\mathrel{\mbox{if}} \href{../exec/modules.html#exec-invocation}{\mathrm{invoke}}(S, a, v^\ast) \href{../exec/conventions.html#formal-notation}{\hookrightarrow}^\ast S'; F; \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}) \\ \end{array}\end{split}\]

Note

The store may be modified even in case of an error.

Tables¶

\(\mathrm{alloc\_table}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}) : (\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}})\)¶

Let \(\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}\) be the result of allocating a table in \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}\) with table type \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\).
Return the new store paired with \(\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}\).

\[\begin{split}\begin{array}{lclll} \mathrm{alloc\_table}(S, \mathit{tt}) &=& (S', \mathit{a}) && (\mathrel{\mbox{if}} \href{../exec/modules.html#alloc-table}{\mathrm{alloctable}}(S, \mathit{tt}) = S', \mathit{a}) \\ \end{array}\end{split}\]

\(\mathrm{type\_table}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}) : \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\)¶

Assert: \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}]\) exists.
Assert: the external value \(\href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}\) is valid with external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\).
Return \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\).

\[\begin{split}\begin{array}{lclll} \mathrm{type\_table}(S, a) &=& \mathit{tt} && (\mathrel{\mbox{if}} S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~a : \href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~\mathit{tt}) \\ \end{array}\end{split}\]

\(\mathrm{read\_table}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}, i) : \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}^? ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}}\)¶

Assert: \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}]\) exists.
Assert: \(i\) is a non-negative integer.
Let \(\mathit{ti}\) be the table instance \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}]\).
If \(i\) is larger than or equal to the length if \(\mathit{ti}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}\), then return \(\href{../appendix/embedding.html#embed-error}{\mathsf{error}}\).
Else, return \(\mathit{ti}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}[i]\).

\[\begin{split}\begin{array}{lclll} \mathrm{read\_table}(S, a, i) &=& \mathit{fa}^? && (\mathrel{\mbox{if}} S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}[i] = \mathit{fa}^?) \\ \mathrm{read\_table}(S, a, i) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]

\(\mathrm{write\_table}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}, i, \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}^?) : \href{../exec/runtime.html#syntax-store}{\mathit{store}} ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}}\)¶

Assert: \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}]\) exists.
Assert: \(i\) is a non-negative integer.
Let \(\mathit{ti}\) be the table instance \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}]\).
If \(i\) is larger than or equal to the length if \(\mathit{ti}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}\), then return \(\href{../appendix/embedding.html#embed-error}{\mathsf{error}}\).
Replace \(\mathit{ti}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}[i]\) with the optional function address \(\mathit{fa}^?\).
Return the updated store.

\[\begin{split}\begin{array}{lclll} \mathrm{write\_table}(S, a, i, \mathit{fa}^?) &=& S' && (\mathrel{\mbox{if}} S' = S \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}[i] = \mathit{fa}^?) \\ \mathrm{write\_table}(S, a, i, \mathit{fa}^?) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]

\(\mathrm{size\_table}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}) : \mathit{i32}\)¶

Assert: \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}]\) exists.
Return the length of \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}\).

\[\begin{split}~ \\ \begin{array}{lclll} \mathrm{size\_table}(S, a) &=& n && (\mathrel{\mbox{if}} |S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}| = n) \\ \end{array}\end{split}\]

\(\mathrm{grow\_table}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}, n) : \href{../exec/runtime.html#syntax-store}{\mathit{store}} ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}}\)¶

Assert: \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}]\) exists.
Assert: \(n\) is a non-negative integer.
Try growing the table instance \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}]\) by \(n\) elements:
1. If it succeeds, return the updated store.
2. Else, return \(\href{../appendix/embedding.html#embed-error}{\mathsf{error}}\).

\[\begin{split}~ \\ \begin{array}{lclll} \mathrm{grow\_table}(S, a, n) &=& S' && (\mathrel{\mbox{if}} S' = S \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a] = \href{../exec/modules.html#grow-table}{\mathrm{growtable}}(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a], n)) \\ \mathrm{grow\_table}(S, a, n) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]

Memories¶

\(\mathrm{alloc\_mem}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}) : (\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}})\)¶

Let \(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}\) be the result of allocating a memory in \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}\) with memory type \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\).
Return the new store paired with \(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}\).

\[\begin{split}\begin{array}{lclll} \mathrm{alloc\_mem}(S, \mathit{mt}) &=& (S', \mathit{a}) && (\mathrel{\mbox{if}} \href{../exec/modules.html#alloc-mem}{\mathrm{allocmem}}(S, \mathit{mt}) = S', \mathit{a}) \\ \end{array}\end{split}\]

\(\mathrm{type\_mem}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}) : \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\)¶

Assert: \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}]\) exists.
Assert: the external value \(\href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}\) is valid with external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\).
Return \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\).

\[\begin{split}\begin{array}{lclll} \mathrm{type\_mem}(S, a) &=& \mathit{mt} && (\mathrel{\mbox{if}} S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~a : \href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\mathit{mt}) \\ \end{array}\end{split}\]

\(\mathrm{read\_mem}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}, i) : \href{../syntax/values.html#syntax-byte}{\mathit{byte}} ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}}\)¶

Assert: \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}]\) exists.
Assert: \(i\) is a non-negative integer.
Let \(\mathit{mi}\) be the memory instance \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}]\).
If \(i\) is larger than or equal to the length if \(\mathit{mi}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\), then return \(\href{../appendix/embedding.html#embed-error}{\mathsf{error}}\).
Else, return the byte \(\mathit{mi}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}[i]\).

\[\begin{split}\begin{array}{lclll} \mathrm{read\_mem}(S, a, i) &=& b && (\mathrel{\mbox{if}} S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}[i] = b) \\ \mathrm{read\_mem}(S, a, i) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]

\(\mathrm{write\_mem}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}, i, \href{../syntax/values.html#syntax-byte}{\mathit{byte}}) : \href{../exec/runtime.html#syntax-store}{\mathit{store}} ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}}\)¶

Assert: \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}]\) exists.
Assert: \(i\) is a non-negative integer.
Let \(\mathit{mi}\) be the memory instance \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}]\).
If \(i\) is larger than or equal to the length if \(\mathit{mi}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\), then return \(\href{../appendix/embedding.html#embed-error}{\mathsf{error}}\).
Replace \(\mathit{mi}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}[i]\) with \(\href{../syntax/values.html#syntax-byte}{\mathit{byte}}\).
Return the updated store.

\[\begin{split}\begin{array}{lclll} \mathrm{write\_mem}(S, a, i, b) &=& S' && (\mathrel{\mbox{if}} S' = S \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}[i] = b) \\ \mathrm{write\_mem}(S, a, i, b) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]

\(\mathrm{size\_mem}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}) : \mathit{i32}\)¶

Assert: \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}]\) exists.
Return the length of \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\) divided by the page size.

\[\begin{split}~ \\ \begin{array}{lclll} \mathrm{size\_mem}(S, a) &=& n && (\mathrel{\mbox{if}} |S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}| = n \cdot 64\,\mathrm{Ki}) \\ \end{array}\end{split}\]

\(\mathrm{grow\_mem}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}, n) : \href{../exec/runtime.html#syntax-store}{\mathit{store}} ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}}\)¶

Assert: \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}]\) exists.
Assert: \(n\) is a non-negative integer.
Try growing the memory instance \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}]\) by \(n\) pages:
1. If it succeeds, return the updated store.
2. Else, return \(\href{../appendix/embedding.html#embed-error}{\mathsf{error}}\).

\[\begin{split}~ \\ \begin{array}{lclll} \mathrm{grow\_mem}(S, a, n) &=& S' && (\mathrel{\mbox{if}} S' = S \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a] = \href{../exec/modules.html#grow-mem}{\mathrm{growmem}}(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a], n)) \\ \mathrm{grow\_mem}(S, a, n) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]

Globals¶

\(\mathrm{alloc\_global}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}, \href{../exec/runtime.html#syntax-val}{\mathit{val}}) : (\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}})\)¶

Let \(\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}\) be the result of allocating a global in \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}\) with global type \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\) and initialization value \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}\).
Return the new store paired with \(\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}\).

\[\begin{split}\begin{array}{lclll} \mathrm{alloc\_global}(S, \mathit{gt}, v) &=& (S', \mathit{a}) && (\mathrel{\mbox{if}} \href{../exec/modules.html#alloc-global}{\mathrm{allocglobal}}(S, \mathit{gt}, v) = S', \mathit{a}) \\ \end{array}\end{split}\]

\(\mathrm{type\_global}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}) : \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\)¶

Assert: \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}]\) exists.
Assert: the external value \(\href{../exec/runtime.html#syntax-externval}{\mathsf{global}}~\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}\) is valid with external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\).
Return \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\).

\[\begin{split}\begin{array}{lclll} \mathrm{type\_global}(S, a) &=& \mathit{gt} && (\mathrel{\mbox{if}} S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{global}}~a : \href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\mathit{gt}) \\ \end{array}\end{split}\]

\(\mathrm{read\_global}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}) : \href{../exec/runtime.html#syntax-val}{\mathit{val}}\)¶

Assert: \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}]\) exists.
Let \(\mathit{gi}\) be the global instance \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}]\).
Return the value \(\mathit{gi}.\href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}\).

\[\begin{split}\begin{array}{lclll} \mathrm{read\_global}(S, a) &=& v && (\mathrel{\mbox{if}} S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[a].\href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}} = v) \\ \end{array}\end{split}\]

\(\mathrm{write\_global}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}, \href{../exec/runtime.html#syntax-val}{\mathit{val}}) : \href{../exec/runtime.html#syntax-store}{\mathit{store}} ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}}\)¶

Assert: \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[a]\) exists.
Let \(\mathit{gi}\) be the global instance \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}]\).
If \(\mathit{gi}.\href{../exec/runtime.html#syntax-globalinst}{\mathsf{mut}}\) is not \(\href{../syntax/types.html#syntax-mut}{\mathsf{var}}\), then return \(\href{../appendix/embedding.html#embed-error}{\mathsf{error}}\).
Replace \(\mathit{gi}.\href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}\) with the value \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}\).
Return the updated store.

\[\begin{split}~ \\ \begin{array}{lclll} \mathrm{write\_global}(S, a, v) &=& S' && (\mathrel{\mbox{if}} S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[a].\href{../exec/runtime.html#syntax-globalinst}{\mathsf{mut}} = \href{../syntax/types.html#syntax-mut}{\mathsf{var}} \wedge S' = S \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[a].\href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}} = v) \\ \mathrm{write\_global}(S, a, v) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]