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.

Types¶

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.

For numeric parameters, notation like \(n:\href{../syntax/values.html#syntax-int}{\mathit{u32}}\) is used to specify a symbolic name in addition to the respective value range.

Errors¶

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

\[\begin{split}\begin{array}{llll} \def\mathdef77#1{{}}\mathdef77{(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.

Pre- and Post-Conditions¶

Some operations state pre-conditions about their arguments or post-conditions about their results. It is the embedder’s responsibility to meet the pre-conditions. If it does, the post conditions are guaranteed by the semantics.

In addition to pre- and post-conditions explicitly stated with each operation, the specification adopts the following conventions for runtime objects (\(store\), \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\), \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}\), addresses):

Every runtime object passed as a parameter must be valid per an implicit pre-condition.
Every runtime object returned as a result is valid per an implicit post-condition.

Note

As long as an embedder treats runtime objects as abstract and only creates and manipulates them through the interface defined here, all implicit pre-conditions are automatically met.

Store¶

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

Return the empty store.

\[\begin{split}\begin{array}{lclll} \mathrm{store\_init}() &=& \{ \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{module\_decode}(\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{module\_decode}(b^\ast) &=& m && (\mathrel{\mbox{if}} \href{../binary/modules.html#binary-module}{\mathtt{module}} \stackrel\ast\Longrightarrow m{:}b^\ast) \\ \mathrm{module\_decode}(b^\ast) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]

\(\mathrm{module\_parse}(\href{../syntax/values.html#syntax-name}{\mathit{char}}^\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{char}}^\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{module\_parse}(c^\ast) &=& m && (\mathrel{\mbox{if}} \href{../text/modules.html#text-module}{\mathtt{module}} \stackrel\ast\Longrightarrow m{:}c^\ast) \\ \mathrm{module\_parse}(c^\ast) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]

\(\mathrm{module\_validate}(\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{module\_validate}(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{module\_validate}(m) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]

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

Pre-condition: \(\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.
Post-condition: each \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_i\) is valid.

\[\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\)¶

Pre-condition: \(\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.
Post-condition: each \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}'_i\) is valid.

\[\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}\]

Module Instances¶

\(\mathrm{instance\_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{instance\_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{instance\_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{func\_alloc}(\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}})\)¶

Pre-condition: \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\) is \(valid <valid-functype>\).
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{func\_alloc}(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{func\_type}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}) : \href{../syntax/types.html#syntax-functype}{\mathit{functype}}\)¶

Return \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a].\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}\).
Post-condition: the returned function type is valid.

\[\begin{split}\begin{array}{lclll} \mathrm{func\_type}(S, a) &=& S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a].\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}} \\ \end{array}\end{split}\]

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

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{func\_invoke}(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{func\_invoke}(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{table\_alloc}(\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}}, \href{../exec/runtime.html#syntax-ref}{\mathit{ref}})\)¶

Pre-condition: \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\) is \(valid <valid-tabletype>\).
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}}\) and initialization value \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}\).
Return the new store paired with \(\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}\).

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

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

Return \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}\).
Post-condition: the returned table type is \(valid <valid-tabletype>\).

\[\begin{split}\begin{array}{lclll} \mathrm{table\_type}(S, a) &=& S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}} \\ \end{array}\end{split}\]

\(\mathrm{table\_read}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}, i:\href{../syntax/values.html#syntax-int}{\mathit{u32}}) : \href{../exec/runtime.html#syntax-ref}{\mathit{ref}} ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}}\)¶

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 of \(\mathit{ti}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}\), then return \(\href{../appendix/embedding.html#embed-error}{\mathsf{error}}\).
Else, return the reference value \(\mathit{ti}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}[i]\).

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

\(\mathrm{table\_write}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}, i:\href{../syntax/values.html#syntax-int}{\mathit{u32}}, \href{../exec/runtime.html#syntax-ref}{\mathit{ref}}) : \href{../exec/runtime.html#syntax-store}{\mathit{store}} ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}}\)¶

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 of \(\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 reference value \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}\).
Return the updated store.

\[\begin{split}\begin{array}{lclll} \mathrm{table\_write}(S, a, i, r) &=& 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] = r) \\ \mathrm{table\_write}(S, a, i, r) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]

\(\mathrm{table\_size}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}) : \href{../syntax/values.html#syntax-int}{\mathit{u32}}\)¶

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{table\_size}(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{table\_grow}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}, n:\href{../syntax/values.html#syntax-int}{\mathit{u32}}, \href{../exec/runtime.html#syntax-ref}{\mathit{ref}}) : \href{../exec/runtime.html#syntax-store}{\mathit{store}} ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}}\)¶

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 with initialization value \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}\):
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{table\_grow}(S, a, n, r) &=& 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, r)) \\ \mathrm{table\_grow}(S, a, n, r) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]

Memories¶

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

Pre-condition: \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\) is \(valid <valid-memtype>\).
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{mem\_alloc}(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{mem\_type}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}) : \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\)¶

Return \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a].\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}\).
Post-condition: the returned memory type is \(valid <valid-memtype>\).

\[\begin{split}\begin{array}{lclll} \mathrm{mem\_type}(S, a) &=& S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a].\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}} \\ \end{array}\end{split}\]

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

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 of \(\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{mem\_read}(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{mem\_read}(S, a, i) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]

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

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 \(\href{../syntax/values.html#syntax-int}{\mathit{u32}}\) is larger than or equal to the length of \(\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{mem\_write}(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{mem\_write}(S, a, i, b) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]

\(\mathrm{mem\_size}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}) : \href{../syntax/values.html#syntax-int}{\mathit{u32}}\)¶

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{mem\_size}(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{mem\_grow}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}, n:\href{../syntax/values.html#syntax-int}{\mathit{u32}}) : \href{../exec/runtime.html#syntax-store}{\mathit{store}} ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}}\)¶

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{mem\_grow}(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{mem\_grow}(S, a, n) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]

Globals¶

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

Pre-condition: \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\) is \(valid <valid-globaltype>\).
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{global\_alloc}(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{global\_type}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}) : \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\)¶

Return \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[a].\href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}}\).
Post-condition: the returned global type is \(valid <valid-globaltype>\).

\[\begin{split}\begin{array}{lclll} \mathrm{global\_type}(S, a) &=& S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[a].\href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}} \\ \end{array}\end{split}\]

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

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

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}}]\).
Let \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t\) be the structure of the global type \(\mathit{gi}.\href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}}\).
If \(\href{../syntax/types.html#syntax-mut}{\mathit{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{global\_write}(S, a, v) &=& S' && (\mathrel{\mbox{if}} S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[a].\href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}} = \href{../syntax/types.html#syntax-mut}{\mathsf{var}}~t \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{global\_write}(S, a, v) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]