Modules¶
Modules consist of a sequence of declarations. The grammar rules for each declaration construct produce a pair, consisting of not just the abstract syntax representing the respective declaration, but also an identifier context recording the new symbolic identifiers bound by the construct, for use in the remainder of the module.
Indices¶
Indices can be given either in raw numeric form or as symbolic identifiers when bound by a respective construct. Such identifiers are looked up in the suitable space of the identifier context \({\href{../text/conventions.html#text-context}{I}}\).
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {{\href{../text/modules.html#text-idx}{\mathtt{idx}}}}_{{\mathit{ids}}} & ::= & x{:}{\href{../text/values.html#text-int}{\mathtt{u32}}} & \quad\Rightarrow\quad{} & x \\
& & | & {\mathit{id}}{:}{\href{../text/values.html#text-id}{\mathtt{id}}} & \quad\Rightarrow\quad{} & x & \quad \mbox{if}~ {\mathit{ids}}{}[x] = {\mathit{id}} \\[0.8ex]
& {{\href{../text/modules.html#text-typeidx}{\mathtt{typeidx}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & {{\href{../text/modules.html#text-idx}{\mathtt{idx}}}}_{{\href{../text/conventions.html#text-context}{I}}{.}\href{../text/conventions.html#text-context}{\mathsf{types}}} \\
& {{\href{../text/modules.html#text-tagidx}{\mathtt{tagidx}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & {{\href{../text/modules.html#text-idx}{\mathtt{idx}}}}_{{\href{../text/conventions.html#text-context}{I}}{.}\href{../text/conventions.html#text-context}{\mathsf{tags}}} \\
& {{\href{../text/modules.html#text-globalidx}{\mathtt{globalidx}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & {{\href{../text/modules.html#text-idx}{\mathtt{idx}}}}_{{\href{../text/conventions.html#text-context}{I}}{.}\href{../text/conventions.html#text-context}{\mathsf{globals}}} \\
& {{\href{../text/modules.html#text-memidx}{\mathtt{memidx}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & {{\href{../text/modules.html#text-idx}{\mathtt{idx}}}}_{{\href{../text/conventions.html#text-context}{I}}{.}\href{../text/conventions.html#text-context}{\mathsf{mems}}} \\
& {{\href{../text/modules.html#text-tableidx}{\mathtt{tableidx}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & {{\href{../text/modules.html#text-idx}{\mathtt{idx}}}}_{{\href{../text/conventions.html#text-context}{I}}{.}\href{../text/conventions.html#text-context}{\mathsf{tables}}} \\
& {{\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & {{\href{../text/modules.html#text-idx}{\mathtt{idx}}}}_{{\href{../text/conventions.html#text-context}{I}}{.}\href{../text/conventions.html#text-context}{\mathsf{funcs}}} \\
& {{\href{../text/modules.html#text-dataidx}{\mathtt{dataidx}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & {{\href{../text/modules.html#text-idx}{\mathtt{idx}}}}_{{\href{../text/conventions.html#text-context}{I}}{.}\href{../text/conventions.html#text-context}{\mathsf{datas}}} \\
& {{\href{../text/modules.html#text-elemidx}{\mathtt{elemidx}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & {{\href{../text/modules.html#text-idx}{\mathtt{idx}}}}_{{\href{../text/conventions.html#text-context}{I}}{.}\href{../text/conventions.html#text-context}{\mathsf{elems}}} \\
& {{\href{../text/modules.html#text-localidx}{\mathtt{localidx}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & {{\href{../text/modules.html#text-idx}{\mathtt{idx}}}}_{{\href{../text/conventions.html#text-context}{I}}{.}\href{../text/conventions.html#text-context}{\mathsf{locals}}} \\
& {{\href{../text/modules.html#text-labelidx}{\mathtt{labelidx}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & {{\href{../text/modules.html#text-idx}{\mathtt{idx}}}}_{{\href{../text/conventions.html#text-context}{I}}{.}\href{../text/conventions.html#text-context}{\mathsf{labels}}} \\
& {{\href{../text/modules.html#text-fieldidx}{\mathtt{fieldidx}}}}_{{\href{../text/conventions.html#text-context}{I}}, x} & ::= & {{\href{../text/modules.html#text-idx}{\mathtt{idx}}}}_{{\href{../text/conventions.html#text-context}{I}}{.}\href{../text/conventions.html#text-context}{\mathsf{fields}}{}[x]} \\
\end{array}\end{split}\]
Types¶
A type definition consists of a recursive type. The identifier context produced for the local bindings is further extended with the respective sequence of defined types that the recursive type generates.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {{\href{../text/types.html#text-type}{\mathtt{type}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & ({\mathit{qt}}, {\href{../text/conventions.html#text-context}{I}'}){:}{{\href{../text/types.html#text-rectype}{\mathtt{rectype}}}}_{{\href{../text/conventions.html#text-context}{I}}} & \quad\Rightarrow\quad{} & (\href{../syntax/modules.html#syntax-type}{\mathsf{type}}~{\mathit{qt}}, {\href{../text/conventions.html#text-context}{I}'} \oplus {\href{../text/conventions.html#text-context}{I}''}) & \quad
\begin{array}[t]{@{}l@{}}
\mbox{if}~ {\mathit{qt}} = \href{../syntax/types.html#syntax-rectype}{\mathsf{rec}}~{{\mathit{st}}^{n}} \\
{\land}~ {\href{../text/conventions.html#text-context}{I}''} = \{ \href{../text/conventions.html#text-context}{\mathsf{typedefs}}~{({\mathit{qt}}~{.}~i)^{i<n}} \} \\
\end{array} \\
\end{array}\end{split}\]
Globals¶
Global definitions can bind a symbolic global identifier.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {{\href{../text/modules.html#text-global}{\mathtt{global}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{global}’}~~{{\mathit{id}}^?}{:}{{\href{../text/values.html#text-id}{\mathtt{id}}}^?}~~{\mathit{gt}}{:}{{\href{../text/types.html#text-globaltype}{\mathtt{globaltype}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~e{:}{{\href{../text/instructions.html#text-expr}{\mathtt{expr}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} & \quad\Rightarrow\quad{} & (\href{../syntax/modules.html#syntax-global}{\mathsf{global}}~{\mathit{gt}}~e, \{ \href{../text/conventions.html#text-context}{\mathsf{globals}}~({{\mathit{id}}^?}) \}) \\
\end{array}\end{split}\]
Abbreviations¶
Globals can be defined as imports or exports inline:
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {{\href{../text/modules.html#text-import}{\mathtt{import}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \dots \\
& & | & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{global}’}~~{{\href{../text/values.html#text-id}{\mathtt{id}}}^?}~~\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{import}’}~~{{\href{../text/values.html#text-name}{\mathtt{name}}}^{2}}~~\mbox{‘\texttt{{)}}’}~~{{\href{../text/types.html#text-globaltype}{\mathtt{globaltype}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} & \quad\equiv\quad{} & & \\
&&& \multicolumn{4}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}}
\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{import}’}~~{{\href{../text/values.html#text-name}{\mathtt{name}}}^{2}}~~\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{global}’}~~{{\href{../text/values.html#text-id}{\mathtt{id}}}^?}~~{{\href{../text/types.html#text-globaltype}{\mathtt{globaltype}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’}~~\mbox{‘\texttt{{)}}’} \\
\end{array}
} \\[0.8ex]
& {{\href{../text/modules.html#text-export}{\mathtt{export}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{global}’}~~{{\mathit{id}}^?}{:}{{\href{../text/values.html#text-id}{\mathtt{id}}}^?}~~\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{export}’}~~{\href{../text/values.html#text-name}{\mathtt{name}}}~~\mbox{‘\texttt{{)}}’}~~\dots~~\mbox{‘\texttt{{)}}’} & \quad\equiv\quad{} & & \\
&&& \multicolumn{4}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}l@{}l@{}}
\begin{array}[t]{@{}l@{}} \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{global}’}~~{\mathit{id}'}{:}{\href{../text/values.html#text-id}{\mathtt{id}}}~~\dots~~\mbox{‘\texttt{{)}}’} \\
\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{export}’}~~{\href{../text/values.html#text-name}{\mathtt{name}}}~~\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{global}’}~~{\href{../text/values.html#text-id}{\mathtt{id}}}~~\mbox{‘\texttt{{)}}’}~~\mbox{‘\texttt{{)}}’} \end{array} & & \\
\multicolumn{3}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}}
\quad \mbox{if}~ {{\mathit{id}}^?} = {\mathit{id}'} \lor {{\mathit{id}}^?} = \epsilon \land {\mathit{id}'} \notin {\href{../text/conventions.html#text-context}{I}}{.}\href{../text/conventions.html#text-context}{\mathsf{globals}} \\
\end{array}
} \\
\end{array}
} \\
\end{array}\end{split}\]
Note
The latter abbreviation can be applied repeatedly, if “\(\dots\)” contains additional export clauses. Consequently, a global declaration can contain any number of exports, possibly followed by an import.
Memories¶
Memory definitions can bind a symbolic memory identifier.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {{\href{../text/modules.html#text-mem}{\mathtt{mem}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{memory}’}~~{{\mathit{id}}^?}{:}{{\href{../text/values.html#text-id}{\mathtt{id}}}^?}~~{\mathit{mt}}{:}{{\href{../text/types.html#text-memtype}{\mathtt{memtype}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} & \quad\Rightarrow\quad{} & (\href{../syntax/modules.html#syntax-mem}{\mathsf{memory}}~{\mathit{mt}}, \{ \href{../text/conventions.html#text-context}{\mathsf{mems}}~({{\mathit{id}}^?}) \}) \\
\end{array}\end{split}\]
Abbreviations¶
A data segment can be given inline with a memory definition, in which case its offset is \(0\) and the limits of the memory type are inferred from the length of the data, rounded up to page size:
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {{\href{../text/modules.html#text-mem}{\mathtt{mem}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{memory}’}~~{{\mathit{id}}^?}{:}{{\href{../text/values.html#text-id}{\mathtt{id}}}^?}~~{{\mathit{at}}^?}{:}{{\href{../text/types.html#text-addrtype}{\mathtt{addrtype}}}^?}~~\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{data}’}~~{b^\ast}{:}{\href{../text/modules.html#text-datastring}{\mathtt{datastring}}}~~\mbox{‘\texttt{{)}}’}~~\mbox{‘\texttt{{)}}’} & \quad\equiv\quad{} & & \\
&&& \multicolumn{4}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}l@{}l@{}}
\begin{array}[t]{@{}l@{}} \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{memory}’}~~{\mathit{id}'}{:}{\href{../text/values.html#text-id}{\mathtt{id}}}~~{{\mathit{at}}^?}{:}{{\href{../text/types.html#text-addrtype}{\mathtt{addrtype}}}^?}~~n{:}{\href{../text/values.html#text-int}{\mathtt{u64}}}~~n{:}{\href{../text/values.html#text-int}{\mathtt{u64}}}~~\mbox{‘\texttt{{)}}’} \\
\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{data}’}~~\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{memory}’}~~{\mathit{id}'}{:}{\href{../text/values.html#text-id}{\mathtt{id}}}~~\mbox{‘\texttt{{)}}’}~~\mbox{‘\texttt{{(}}’}~~{\mathit{at}'}{:}{\href{../text/types.html#text-addrtype}{\mathtt{addrtype}}}~~\mbox{‘\texttt{.const}’}~~\mbox{‘\texttt{0}’}~~\mbox{‘\texttt{{)}}’}~~{\href{../text/modules.html#text-datastring}{\mathtt{datastring}}}~~\mbox{‘\texttt{{)}}’} \end{array} & & \\
\multicolumn{3}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}}
\quad
\begin{array}[t]{@{}l@{}}
\mbox{if}~ {{\mathit{id}}^?} = {\mathit{id}'} \lor {{\mathit{id}}^?} = \epsilon \land {\mathit{id}'} \notin {\href{../text/conventions.html#text-context}{I}}{.}\href{../text/conventions.html#text-context}{\mathsf{mems}} \\
{\land}~ {{\mathit{at}}^?} = {\mathit{at}'} \lor {{\mathit{at}}^?} = \epsilon \land {\mathit{at}'} = \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \\
{\land}~ n = {\mathrm{ceil}}({|{b^\ast}|} / 64 \cdot {\mathrm{Ki}}) \\
\end{array} \\
\end{array}
} \\
\end{array}
} \\
\end{array}\end{split}\]
Memories can be defined as imports or exports inline:
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {{\href{../text/modules.html#text-import}{\mathtt{import}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \dots \\
& & | & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{memory}’}~~{{\href{../text/values.html#text-id}{\mathtt{id}}}^?}~~\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{import}’}~~{{\href{../text/values.html#text-name}{\mathtt{name}}}^{2}}~~\mbox{‘\texttt{{)}}’}~~{{\href{../text/types.html#text-memtype}{\mathtt{memtype}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} & \quad\equiv\quad{} & & \\
&&& \multicolumn{4}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}}
\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{import}’}~~{{\href{../text/values.html#text-name}{\mathtt{name}}}^{2}}~~\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{memory}’}~~{{\href{../text/values.html#text-id}{\mathtt{id}}}^?}~~{{\href{../text/types.html#text-memtype}{\mathtt{memtype}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’}~~\mbox{‘\texttt{{)}}’} \\
\end{array}
} \\[0.8ex]
& {{\href{../text/modules.html#text-export}{\mathtt{export}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{memory}’}~~{{\mathit{id}}^?}{:}{{\href{../text/values.html#text-id}{\mathtt{id}}}^?}~~\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{export}’}~~{\href{../text/values.html#text-name}{\mathtt{name}}}~~\mbox{‘\texttt{{)}}’}~~\dots~~\mbox{‘\texttt{{)}}’} & \quad\equiv\quad{} & & \\
&&& \multicolumn{4}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}l@{}l@{}}
\begin{array}[t]{@{}l@{}} \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{memory}’}~~{\mathit{id}'}{:}{\href{../text/values.html#text-id}{\mathtt{id}}}~~\dots~~\mbox{‘\texttt{{)}}’} \\
\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{export}’}~~{\href{../text/values.html#text-name}{\mathtt{name}}}~~\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{memory}’}~~{\href{../text/values.html#text-id}{\mathtt{id}}}~~\mbox{‘\texttt{{)}}’}~~\mbox{‘\texttt{{)}}’} \end{array} & & \\
\multicolumn{3}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}}
\quad \mbox{if}~ {{\mathit{id}}^?} = {\mathit{id}'} \lor {{\mathit{id}}^?} = \epsilon \land {\mathit{id}'} \notin {\href{../text/conventions.html#text-context}{I}}{.}\href{../text/conventions.html#text-context}{\mathsf{mems}} \\
\end{array}
} \\
\end{array}
} \\
\end{array}\end{split}\]
Note
The latter abbreviation can be applied repeatedly, if “\(\dots\)” contains additional export clauses. Consequently, a memory declaration can contain any number of exports, possibly followed by an import.
Tables¶
Table definitions can bind a symbolic table identifier.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {{\href{../text/modules.html#text-table}{\mathtt{table}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{table}’}~~{{\mathit{id}}^?}{:}{{\href{../text/values.html#text-id}{\mathtt{id}}}^?}~~{\mathit{tt}}{:}{{\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~e{:}{{\href{../text/instructions.html#text-expr}{\mathtt{expr}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} & \quad\Rightarrow\quad{} & (\href{../syntax/modules.html#syntax-table}{\mathsf{table}}~{\mathit{tt}}~e, \{ \href{../text/conventions.html#text-context}{\mathsf{tables}}~({{\mathit{id}}^?}) \}) \\
\end{array}\end{split}\]
Abbreviations¶
A table’s initialization expression can be omitted, in which case it defaults to \(\mathsf{ref{.}null}\):
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {{\href{../text/modules.html#text-table}{\mathtt{table}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \dots \\
& & | & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{table}’}~~{{\href{../text/values.html#text-id}{\mathtt{id}}}^?}~~{\mathit{tt}}{:}{{\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} & \quad\equiv\quad{} & & \\
&&& \multicolumn{4}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}l@{}l@{}}
\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{table}’}~~{{\href{../text/values.html#text-id}{\mathtt{id}}}^?}~~{\mathit{tt}}{:}{{\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{ref.null}’}~~{\mathit{ht}}{:}{{\href{../text/types.html#text-heaptype}{\mathtt{heaptype}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’}~~\mbox{‘\texttt{{)}}’} & & \\
\multicolumn{3}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}}
\quad \mbox{if}~ {\mathit{tt}} = {\mathit{at}}~{\mathit{lim}}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}^?}~{\mathit{ht}}) \\
\end{array}
} \\
\end{array}
} \\
\end{array}\end{split}\]
An element segment can be given inline with a table definition, in which case its offset is \(0\) and the limits of the table type are inferred from the length of the given segment:
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {{\href{../text/modules.html#text-table}{\mathtt{table}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{table}’}~~{{\mathit{id}}^?}{:}{{\href{../text/values.html#text-id}{\mathtt{id}}}^?}~~{{\mathit{at}}^?}{:}{{\href{../text/types.html#text-addrtype}{\mathtt{addrtype}}}^?}~~{{\href{../text/types.html#text-reftype}{\mathtt{reftype}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{elem}’}~~({\mathit{rt}}, {e^\ast}){:}{{\href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’}~~\mbox{‘\texttt{{)}}’} & \quad\equiv\quad{} & & \\
&&& \multicolumn{4}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}l@{}l@{}}
\begin{array}[t]{@{}l@{}} \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{table}’}~~{\mathit{id}'}{:}{\href{../text/values.html#text-id}{\mathtt{id}}}~~{{\mathit{at}}^?}{:}{{\href{../text/types.html#text-addrtype}{\mathtt{addrtype}}}^?}~~n{:}{\href{../text/values.html#text-int}{\mathtt{u64}}}~~n{:}{\href{../text/values.html#text-int}{\mathtt{u64}}}~~{{\href{../text/types.html#text-reftype}{\mathtt{reftype}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} \\
\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{elem}’}~~\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{table}’}~~{\mathit{id}'}{:}{\href{../text/values.html#text-id}{\mathtt{id}}}~~\mbox{‘\texttt{{)}}’}~~\mbox{‘\texttt{{(}}’}~~{\mathit{at}'}{:}{\href{../text/types.html#text-addrtype}{\mathtt{addrtype}}}~~\mbox{‘\texttt{.const}’}~~\mbox{‘\texttt{0}’}~~\mbox{‘\texttt{{)}}’}~~{{\href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} \end{array} & & \\
\multicolumn{3}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}}
\quad
\begin{array}[t]{@{}l@{}}
\mbox{if}~ {{\mathit{id}}^?} = {\mathit{id}'} \lor {{\mathit{id}}^?} = \epsilon \land {\mathit{id}'} \notin {\href{../text/conventions.html#text-context}{I}}{.}\href{../text/conventions.html#text-context}{\mathsf{tables}} \\
{\land}~ {{\mathit{at}}^?} = {\mathit{at}'} \lor {{\mathit{at}}^?} = \epsilon \land {\mathit{at}'} = \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \\
{\land}~ n = {|{e^\ast}|} \\
\end{array} \\
\end{array}
} \\
\end{array}
} \\
\end{array}\end{split}\]
Tables can be defined as imports or exports inline:
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {{\href{../text/modules.html#text-import}{\mathtt{import}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \dots \\
& & | & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{table}’}~~{{\href{../text/values.html#text-id}{\mathtt{id}}}^?}~~\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{import}’}~~{{\href{../text/values.html#text-name}{\mathtt{name}}}^{2}}~~\mbox{‘\texttt{{)}}’}~~{{\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} & \quad\equiv\quad{} & & \\
&&& \multicolumn{4}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}}
\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{import}’}~~{{\href{../text/values.html#text-name}{\mathtt{name}}}^{2}}~~\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{table}’}~~{{\href{../text/values.html#text-id}{\mathtt{id}}}^?}~~{{\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’}~~\mbox{‘\texttt{{)}}’} \\
\end{array}
} \\[0.8ex]
& {{\href{../text/modules.html#text-export}{\mathtt{export}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{table}’}~~{{\mathit{id}}^?}{:}{{\href{../text/values.html#text-id}{\mathtt{id}}}^?}~~\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{export}’}~~{\href{../text/values.html#text-name}{\mathtt{name}}}~~\mbox{‘\texttt{{)}}’}~~\dots~~\mbox{‘\texttt{{)}}’} & \quad\equiv\quad{} & & \\
&&& \multicolumn{4}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}l@{}l@{}}
\begin{array}[t]{@{}l@{}} \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{table}’}~~{\mathit{id}'}{:}{\href{../text/values.html#text-id}{\mathtt{id}}}~~\dots~~\mbox{‘\texttt{{)}}’} \\
\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{export}’}~~{\href{../text/values.html#text-name}{\mathtt{name}}}~~\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{table}’}~~{\href{../text/values.html#text-id}{\mathtt{id}}}~~\mbox{‘\texttt{{)}}’}~~\mbox{‘\texttt{{)}}’} \end{array} & & \\
\multicolumn{3}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}}
\quad \mbox{if}~ {{\mathit{id}}^?} = {\mathit{id}'} \lor {{\mathit{id}}^?} = \epsilon \land {\mathit{id}'} \notin {\href{../text/conventions.html#text-context}{I}}{.}\href{../text/conventions.html#text-context}{\mathsf{tables}} \\
\end{array}
} \\
\end{array}
} \\
\end{array}\end{split}\]
Note
The latter abbreviation can be applied repeatedly, if “\(\dots\)” contains additional export clauses. Consequently, a table declaration can contain any number of exports, possibly followed by an import.
Functions¶
Function definitions can bind a symbolic function identifier, and local identifiers for its parameters and locals.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {{\href{../text/modules.html#text-func}{\mathtt{func}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{func}’}~~{{\mathit{id}}^?}{:}{{\href{../text/values.html#text-id}{\mathtt{id}}}^?}~~(x, {\href{../text/conventions.html#text-context}{I}}_1){:}{{\href{../text/types.html#text-typeuse}{\mathtt{typeuse}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~{(({{\mathit{loc}}^\ast}, {\href{../text/conventions.html#text-context}{I}}_2){:}{{\href{../text/modules.html#text-local}{\mathtt{local}}}}_{{\href{../text/conventions.html#text-context}{I}}})^\ast}~~e{:}{{\href{../text/instructions.html#text-expr}{\mathtt{expr}}}}_{{\href{../text/conventions.html#text-context}{I}'}}~~\mbox{‘\texttt{{)}}’} & \quad\Rightarrow\quad{} & & \\
&&& \multicolumn{4}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}l@{}l@{}}
(\href{../syntax/modules.html#syntax-func}{\mathsf{func}}~x~({\href{../syntax/conventions.html#notation-concat}{\bigoplus}}\, {{{\mathit{loc}}^\ast}^\ast})~e, \{ \href{../text/conventions.html#text-context}{\mathsf{funcs}}~({{\mathit{id}}^?}) \}) & & \\
\multicolumn{3}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}}
\quad
\begin{array}[t]{@{}l@{}}
\mbox{if}~ {\href{../text/conventions.html#text-context}{I}'} = {\href{../text/conventions.html#text-context}{I}} \oplus {\href{../text/conventions.html#text-context}{I}}_1 \oplus {\href{../syntax/conventions.html#notation-concat}{\bigoplus}}\, {{\href{../text/conventions.html#text-context}{I}}_2^\ast} \\
{\land}~ {\vdash}\, {\href{../text/conventions.html#text-context}{I}'} : \mathsf{ok} \\
\end{array} \\
\end{array}
} \\
\end{array}
} \\
\end{array}\end{split}\]
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {{\href{../text/modules.html#text-local}{\mathtt{local}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{local}’}~~{{\mathit{id}}^?}{:}{{\href{../text/values.html#text-id}{\mathtt{id}}}^?}~~t{:}{{\href{../text/types.html#text-valtype}{\mathtt{valtype}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} & \quad\Rightarrow\quad{} & & \\
&&& \multicolumn{4}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}}
(\href{../syntax/modules.html#syntax-local}{\mathsf{local}}~t, \{ \href{../text/conventions.html#text-context}{\mathsf{locals}}~({{\mathit{id}}^?}) \}) \\
\end{array}
} \\
\end{array}\end{split}\]
Note
The well-formedness condition on \({\href{../text/conventions.html#text-context}{I}'}\) ensures that parameters and locals do not contain duplicate identifiers.
Abbreviations¶
Multiple anonymous locals may be combined into a single declaration:
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {{\href{../text/modules.html#text-local}{\mathtt{local}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \dots ~~|~~ \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{local}’}~~t{:}{{{\href{../text/types.html#text-valtype}{\mathtt{valtype}}}}_{{\href{../text/conventions.html#text-context}{I}}}^\ast}~~\mbox{‘\texttt{{)}}’} & \quad\equiv\quad{} & {(\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{local}’}~~t{:}{{\href{../text/types.html#text-valtype}{\mathtt{valtype}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’})^\ast} \\
\end{array}\end{split}\]
Functions can be defined as imports or exports inline:
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {{\href{../text/modules.html#text-import}{\mathtt{import}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \dots \\
& & | & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{func}’}~~{{\href{../text/values.html#text-id}{\mathtt{id}}}^?}~~\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{import}’}~~{{\href{../text/values.html#text-name}{\mathtt{name}}}^{2}}~~\mbox{‘\texttt{{)}}’}~~{{\href{../text/types.html#text-typeuse}{\mathtt{typeuse}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} & \quad\equiv\quad{} & & \\
&&& \multicolumn{4}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}}
\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{import}’}~~{{\href{../text/values.html#text-name}{\mathtt{name}}}^{2}}~~\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{func}’}~~{{\href{../text/values.html#text-id}{\mathtt{id}}}^?}~~{{\href{../text/types.html#text-typeuse}{\mathtt{typeuse}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’}~~\mbox{‘\texttt{{)}}’} \\
\end{array}
} \\[0.8ex]
& {{\href{../text/modules.html#text-export}{\mathtt{export}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{func}’}~~{{\mathit{id}}^?}{:}{{\href{../text/values.html#text-id}{\mathtt{id}}}^?}~~\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{export}’}~~{\href{../text/values.html#text-name}{\mathtt{name}}}~~\mbox{‘\texttt{{)}}’}~~\dots~~\mbox{‘\texttt{{)}}’} & \quad\equiv\quad{} & & \\
&&& \multicolumn{4}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}l@{}l@{}}
\begin{array}[t]{@{}l@{}} \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{func}’}~~{\mathit{id}'}{:}{\href{../text/values.html#text-id}{\mathtt{id}}}~~\dots~~\mbox{‘\texttt{{)}}’} \\
\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{export}’}~~{\href{../text/values.html#text-name}{\mathtt{name}}}~~\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{func}’}~~{\href{../text/values.html#text-id}{\mathtt{id}}}~~\mbox{‘\texttt{{)}}’}~~\mbox{‘\texttt{{)}}’} \end{array} & & \\
\multicolumn{3}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}}
\quad \mbox{if}~ {{\mathit{id}}^?} = {\mathit{id}'} \lor {{\mathit{id}}^?} = \epsilon \land {\mathit{id}'} \notin {\href{../text/conventions.html#text-context}{I}}{.}\href{../text/conventions.html#text-context}{\mathsf{funcs}} \\
\end{array}
} \\
\end{array}
} \\
\end{array}\end{split}\]
Note
The latter abbreviation can be applied repeatedly, if “\(\dots\)” contains additional export clauses. Consequently, a function declaration can contain any number of exports, possibly followed by an import.
Data Segments¶
Data segments allow for an optional memory index to identify the memory to initialize. The data is written as a string, which may be split up into a possibly empty sequence of individual string literals.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {{\href{../text/modules.html#text-data}{\mathtt{data}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{data}’}~~{{\mathit{id}}^?}{:}{{\href{../text/values.html#text-id}{\mathtt{id}}}^?}~~{b^\ast}{:}{\href{../text/modules.html#text-datastring}{\mathtt{datastring}}}~~\mbox{‘\texttt{{)}}’} & \quad\Rightarrow\quad{} & & \\
&&& \multicolumn{4}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}}
(\href{../syntax/modules.html#syntax-data}{\mathsf{data}}~{b^\ast}~\href{../syntax/modules.html#syntax-datamode}{\mathsf{passive}}, \{ \href{../text/conventions.html#text-context}{\mathsf{datas}}~({{\mathit{id}}^?}) \}) \\
\end{array}
} \\
& & | & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{data}’}~~{{\mathit{id}}^?}{:}{{\href{../text/values.html#text-id}{\mathtt{id}}}^?}~~x{:}{{\href{../text/modules.html#text-memuse}{\mathtt{memuse}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~e{:}{{\href{../text/instructions.html#text-memarg}{\mathtt{offset}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~{b^\ast}{:}{\href{../text/modules.html#text-datastring}{\mathtt{datastring}}}~~\mbox{‘\texttt{{)}}’} & \quad\Rightarrow\quad{} & & \\
&&& \multicolumn{4}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}}
(\href{../syntax/modules.html#syntax-data}{\mathsf{data}}~{b^\ast}~(\href{../syntax/modules.html#syntax-datamode}{\mathsf{active}}~x~e), \{ \href{../text/conventions.html#text-context}{\mathsf{datas}}~({{\mathit{id}}^?}) \}) \\
\end{array}
} \\[0.8ex]
& {\href{../text/modules.html#text-datastring}{\mathtt{datastring}}} & ::= & {{b^\ast}^\ast}{:}{{\href{../text/values.html#text-string}{\mathtt{string}}}^\ast} & \quad\Rightarrow\quad{} & {\href{../syntax/conventions.html#notation-concat}{\bigoplus}}\, {{b^\ast}^\ast} \\[0.8ex]
& {{\href{../text/modules.html#text-memuse}{\mathtt{memuse}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{memory}’}~~x{:}{{\href{../text/modules.html#text-memidx}{\mathtt{memidx}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} & \quad\Rightarrow\quad{} & x \\
& {{\href{../text/instructions.html#text-memarg}{\mathtt{offset}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{offset}’}~~e{:}{{\href{../text/instructions.html#text-expr}{\mathtt{expr}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} & \quad\Rightarrow\quad{} & e \\
\end{array}\end{split}\]
Note
In the current version of WebAssembly, the only valid memory index is 0 or a symbolic memory identifier resolving to the same value.
Abbreviations¶
As an abbreviation, a single folded instruction may occur in place of the offset of an active segment:
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {{\href{../text/instructions.html#text-memarg}{\mathtt{offset}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \dots ~~|~~ {{\href{../text/instructions.html#text-foldedinstr}{\mathtt{foldedinstr}}}}_{{\href{../text/conventions.html#text-context}{I}}} & \quad\equiv\quad{} & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{offset}’}~~{{\href{../text/instructions.html#text-foldedinstr}{\mathtt{foldedinstr}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} \\
\end{array}\end{split}\]
Also, a memory use can be omitted, defaulting to \(0\).
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {{\href{../text/modules.html#text-memuse}{\mathtt{memuse}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \dots ~~|~~ \epsilon & \quad\equiv\quad{} & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{memory}’}~~\mbox{‘\texttt{0}’}~~\mbox{‘\texttt{{)}}’} \\
\end{array}\end{split}\]
As another abbreviation, data segments may also be specified inline with memory definitions; see the respective section.
Element Segments¶
Element segments allow for an optional table index to identify the table to initialize.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {{\href{../text/modules.html#text-elem}{\mathtt{elem}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{elem}’}~~{{\mathit{id}}^?}{:}{{\href{../text/values.html#text-id}{\mathtt{id}}}^?}~~({\mathit{rt}}, {e^\ast}){:}{{\href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} & \quad\Rightarrow\quad{} & & \\
&&& \multicolumn{4}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}}
(\href{../syntax/modules.html#syntax-elem}{\mathsf{elem}}~{\mathit{rt}}~{e^\ast}~\href{../syntax/modules.html#syntax-elemmode}{\mathsf{passive}}, \{ \href{../text/conventions.html#text-context}{\mathsf{elems}}~({{\mathit{id}}^?}) \}) \\
\end{array}
} \\
& & | & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{elem}’}~~{{\mathit{id}}^?}{:}{{\href{../text/values.html#text-id}{\mathtt{id}}}^?}~~x{:}{{\href{../text/modules.html#text-tableuse}{\mathtt{tableuse}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~{e'}{:}{{\href{../text/instructions.html#text-memarg}{\mathtt{offset}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~({\mathit{rt}}, {e^\ast}){:}{{\href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} & \quad\Rightarrow\quad{} & & \\
&&& \multicolumn{4}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}}
(\href{../syntax/modules.html#syntax-elem}{\mathsf{elem}}~{\mathit{rt}}~{e^\ast}~(\href{../syntax/modules.html#syntax-elemmode}{\mathsf{active}}~x~{e'}), \{ \href{../text/conventions.html#text-context}{\mathsf{elems}}~({{\mathit{id}}^?}) \}) \\
\end{array}
} \\
& & | & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{elem}’}~~{{\mathit{id}}^?}{:}{{\href{../text/values.html#text-id}{\mathtt{id}}}^?}~~\mbox{‘\texttt{declare}’}~~({\mathit{rt}}, {e^\ast}){:}{{\href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} & \quad\Rightarrow\quad{} & & \\
&&& \multicolumn{4}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}}
(\href{../syntax/modules.html#syntax-elem}{\mathsf{elem}}~{\mathit{rt}}~{e^\ast}~\href{../syntax/modules.html#syntax-elemmode}{\mathsf{declare}}, \{ \href{../text/conventions.html#text-context}{\mathsf{elems}}~({{\mathit{id}}^?}) \}) \\
\end{array}
} \\[0.8ex]
& {{\href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & {\mathit{rt}}{:}{{\href{../text/types.html#text-reftype}{\mathtt{reftype}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~{e^\ast}{:}{\href{../text/conventions.html#text-list}{\mathtt{list}}}({{\href{../text/instructions.html#text-expr}{\mathtt{expr}}}}_{{\href{../text/conventions.html#text-context}{I}}}) & \quad\Rightarrow\quad{} & ({\mathit{rt}}, {e^\ast}) \\
& {{\href{../text/modules.html#text-elemexpr}{\mathtt{elemexpr}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{item}’}~~e{:}{{\href{../text/instructions.html#text-expr}{\mathtt{expr}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} & \quad\Rightarrow\quad{} & e \\[0.8ex]
& {{\href{../text/modules.html#text-tableuse}{\mathtt{tableuse}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{table}’}~~x{:}{{\href{../text/modules.html#text-tableidx}{\mathtt{tableidx}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} & \quad\Rightarrow\quad{} & x \\
\end{array}\end{split}\]
Abbreviations¶
As an abbreviation, a single folded instruction may occur in place of the offset of an active element segment or as an element expression:
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {{\href{../text/modules.html#text-elemexpr}{\mathtt{elemexpr}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \dots ~~|~~ {{\href{../text/instructions.html#text-foldedinstr}{\mathtt{foldedinstr}}}}_{{\href{../text/conventions.html#text-context}{I}}} & \quad\equiv\quad{} & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{item}’}~~{{\href{../text/instructions.html#text-foldedinstr}{\mathtt{foldedinstr}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} \\
\end{array}\end{split}\]
Also, the element list may be written as just a sequence of function indices:
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {{\href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \dots ~~|~~ \mbox{‘\texttt{func}’}~~{x^\ast}{:}{{{\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}}}_{{\href{../text/conventions.html#text-context}{I}}}^\ast} & \quad\equiv\quad{} & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{ref}’}~~\mbox{‘\texttt{func}’}~~\mbox{‘\texttt{{)}}’}~~{(\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{ref.func}’}~~{{\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’})^\ast} \\
\end{array}\end{split}\]
A table use can be omitted, defaulting to \(0\).
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {{\href{../text/modules.html#text-tableuse}{\mathtt{tableuse}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \dots ~~|~~ \epsilon & \quad\equiv\quad{} & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{table}’}~~\mbox{‘\texttt{0}’}~~\mbox{‘\texttt{{)}}’} \\
\end{array}\end{split}\]
Furthermore, for backwards compatibility with earlier versions of WebAssembly, if the table use is omitted, the \(\mbox{‘\texttt{func}’}\) keyword can be omitted as well.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {{\href{../text/modules.html#text-elem}{\mathtt{elem}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \dots \\
& & | & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{elem}’}~~{e'}{:}{{\href{../text/instructions.html#text-memarg}{\mathtt{offset}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~{\href{../text/conventions.html#text-list}{\mathtt{list}}}({{\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}}}_{{\href{../text/conventions.html#text-context}{I}}})~~\mbox{‘\texttt{{)}}’} & \quad\equiv\quad{} & & \\
&&& \multicolumn{4}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}}
\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{elem}’}~~{e'}{:}{{\href{../text/instructions.html#text-memarg}{\mathtt{offset}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{func}’}~~{\href{../text/conventions.html#text-list}{\mathtt{list}}}({{\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}}}_{{\href{../text/conventions.html#text-context}{I}}})~~\mbox{‘\texttt{{)}}’} \\
\end{array}
} \\
\end{array}\end{split}\]
As yet another abbreviation, element segments may also be specified inline with table definitions; see the respective section.
Start Function¶
A start function is defined in terms of its index.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {{\href{../text/modules.html#text-start}{\mathtt{start}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{start}’}~~x{:}{{\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} & \quad\Rightarrow\quad{} & (\href{../syntax/modules.html#syntax-start}{\mathsf{start}}~x, \{ \}) \\
\end{array}\end{split}\]
Note
At most one start function may occur in a module, which is ensured by a suitable side condition on the \({\href{../text/modules.html#text-module}{\mathtt{module}}}\) grammar.
Imports¶
The external type in imports can bind a symbolic tag, global, memory, or function identifier.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {{\href{../text/modules.html#text-import}{\mathtt{import}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{import}’}~~{\mathit{nm}}_1{:}{\href{../text/values.html#text-name}{\mathtt{name}}}~~{\mathit{nm}}_2{:}{\href{../text/values.html#text-name}{\mathtt{name}}}~~({\mathit{xt}}, {\href{../text/conventions.html#text-context}{I}'}){:}{{\href{../text/types.html#text-externtype}{\mathtt{externtype}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} & \quad\Rightarrow\quad{} & (\href{../syntax/modules.html#syntax-import}{\mathsf{import}}~{\mathit{nm}}_1~{\mathit{nm}}_2~{\mathit{xt}}, {\href{../text/conventions.html#text-context}{I}'}) \\
\end{array}\end{split}\]
Abbreviations¶
As an abbreviation, imports may also be specified inline with tag, global, memory, table, or function definitions; see the respective sections.
Exports¶
The syntax for exports mirrors their abstract syntax directly.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {{\href{../text/modules.html#text-export}{\mathtt{export}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{export}’}~~{\mathit{nm}}{:}{\href{../text/values.html#text-name}{\mathtt{name}}}~~{\mathit{xx}}{:}{{\href{../text/modules.html#text-externidx}{\mathtt{externidx}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} & \quad\Rightarrow\quad{} & (\href{../syntax/modules.html#syntax-export}{\mathsf{export}}~{\mathit{nm}}~{\mathit{xx}}, \{ \}) \\[0.8ex]
& {{\href{../text/modules.html#text-externidx}{\mathtt{externidx}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{tag}’}~~x{:}{{\href{../text/modules.html#text-tagidx}{\mathtt{tagidx}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} & \quad\Rightarrow\quad{} & \href{../syntax/modules.html#syntax-externidx}{\mathsf{tag}}~x \\
& & | & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{global}’}~~x{:}{{\href{../text/modules.html#text-globalidx}{\mathtt{globalidx}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} & \quad\Rightarrow\quad{} & \href{../syntax/modules.html#syntax-externidx}{\mathsf{global}}~x \\
& & | & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{memory}’}~~x{:}{{\href{../text/modules.html#text-memidx}{\mathtt{memidx}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} & \quad\Rightarrow\quad{} & \href{../syntax/modules.html#syntax-externidx}{\mathsf{memory}}~x \\
& & | & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{table}’}~~x{:}{{\href{../text/modules.html#text-tableidx}{\mathtt{tableidx}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} & \quad\Rightarrow\quad{} & \href{../syntax/modules.html#syntax-externidx}{\mathsf{table}}~x \\
& & | & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{func}’}~~x{:}{{\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}}}_{{\href{../text/conventions.html#text-context}{I}}}~~\mbox{‘\texttt{{)}}’} & \quad\Rightarrow\quad{} & \href{../syntax/modules.html#syntax-externidx}{\mathsf{func}}~x \\
\end{array}\end{split}\]
Abbreviations¶
As an abbreviation, exports may also be specified inline with tag, global, memory, table, or function definitions; see the respective sections.
Modules¶
A module consists of a sequence of declarations that can occur in any order.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}}
& {\href{../text/modules.html#syntax-decl}{\mathit{decl}}} & ::= & {\href{../syntax/types.html#syntax-rectype}{\mathit{type}}} ~~|~~ {\href{../syntax/modules.html#syntax-import}{\mathit{import}}} ~~|~~ {\href{../syntax/modules.html#syntax-tag}{\mathit{tag}}} ~~|~~ {\href{../syntax/modules.html#syntax-global}{\mathit{global}}} ~~|~~ {\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}} ~~|~~ {\href{../syntax/modules.html#syntax-table}{\mathit{table}}} ~~|~~ {\href{../syntax/modules.html#syntax-func}{\mathit{func}}} ~~|~~ {\href{../syntax/modules.html#syntax-data}{\mathit{data}}} ~~|~~ {\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}} ~~|~~ {\href{../syntax/modules.html#syntax-start}{\mathit{start}}} ~~|~~ {\href{../syntax/modules.html#syntax-export}{\mathit{export}}} \\
\end{array}\end{split}\]
All declarations and their respective bound identifiers scope over the entire module, including the text preceding them. A module itself may optionally bind an identifier that names the module. The name serves a documentary role only.
Note
Tools may include the module name in the name section of the binary format.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {{\href{../text/modules.html#text-decl}{\mathtt{decl}}}}_{{\href{../text/conventions.html#text-context}{I}}} & ::= & {{\href{../text/types.html#text-type}{\mathtt{type}}}}_{{\href{../text/conventions.html#text-context}{I}}} ~~|~~ {{\href{../text/modules.html#text-import}{\mathtt{import}}}}_{{\href{../text/conventions.html#text-context}{I}}} ~~|~~ {{\href{../text/modules.html#text-tag}{\mathtt{tag}}}}_{{\href{../text/conventions.html#text-context}{I}}} ~~|~~ {{\href{../text/modules.html#text-global}{\mathtt{global}}}}_{{\href{../text/conventions.html#text-context}{I}}} ~~|~~ {{\href{../text/modules.html#text-mem}{\mathtt{mem}}}}_{{\href{../text/conventions.html#text-context}{I}}} ~~|~~ {{\href{../text/modules.html#text-table}{\mathtt{table}}}}_{{\href{../text/conventions.html#text-context}{I}}} \\
& & | & {{\href{../text/modules.html#text-func}{\mathtt{func}}}}_{{\href{../text/conventions.html#text-context}{I}}} ~~|~~ {{\href{../text/modules.html#text-data}{\mathtt{data}}}}_{{\href{../text/conventions.html#text-context}{I}}} ~~|~~ {{\href{../text/modules.html#text-elem}{\mathtt{elem}}}}_{{\href{../text/conventions.html#text-context}{I}}} ~~|~~ {{\href{../text/modules.html#text-start}{\mathtt{start}}}}_{{\href{../text/conventions.html#text-context}{I}}} ~~|~~ {{\href{../text/modules.html#text-export}{\mathtt{export}}}}_{{\href{../text/conventions.html#text-context}{I}}} \\
\end{array}\end{split}\]
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {\href{../text/modules.html#text-module}{\mathtt{module}}} & ::= & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{module}’}~~{{\href{../text/values.html#text-id}{\mathtt{id}}}^?}~~{({\href{../text/modules.html#syntax-decl}{\mathit{decl}}}, {\href{../text/conventions.html#text-context}{I}})^\ast}{:}{{{\href{../text/modules.html#text-decl}{\mathtt{decl}}}}_{{\href{../text/conventions.html#text-context}{I}'}}^\ast}~~\mbox{‘\texttt{{)}}’} & \quad\Rightarrow\quad{} & & \\
&&& \multicolumn{4}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}l@{}l@{}}
\href{../syntax/modules.html#syntax-module}{\mathsf{module}}~{{\href{../syntax/types.html#syntax-rectype}{\mathit{type}}}^\ast}~{{\href{../syntax/modules.html#syntax-import}{\mathit{import}}}^\ast}~{{\href{../syntax/modules.html#syntax-tag}{\mathit{tag}}}^\ast}~{{\href{../syntax/modules.html#syntax-global}{\mathit{global}}}^\ast}~{{\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}}^\ast}~{{\href{../syntax/modules.html#syntax-table}{\mathit{table}}}^\ast}~{{\href{../syntax/modules.html#syntax-func}{\mathit{func}}}^\ast}~{{\href{../syntax/modules.html#syntax-data}{\mathit{data}}}^\ast}~{{\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}}^\ast}~{{\href{../syntax/modules.html#syntax-start}{\mathit{start}}}^?}~{{\href{../syntax/modules.html#syntax-export}{\mathit{export}}}^\ast} & & \\
\multicolumn{3}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}}
\quad
\begin{array}[t]{@{}l@{}}
\mbox{if}~ {\href{../text/conventions.html#text-context}{I}'} = {\href{../syntax/conventions.html#notation-concat}{\bigoplus}}\, {{\href{../text/conventions.html#text-context}{I}}^\ast} \\
{\land}~ {\vdash}\, {\href{../text/conventions.html#text-context}{I}'} : \mathsf{ok} \\
{\land}~ {{\href{../syntax/types.html#syntax-rectype}{\mathit{type}}}^\ast} = {\href{../text/modules.html#syntax-decl}{\mathrm{types}}}({{\href{../text/modules.html#syntax-decl}{\mathit{decl}}}^\ast}) \\
{\land}~ {{\href{../syntax/modules.html#syntax-import}{\mathit{import}}}^\ast} = {\href{../text/modules.html#syntax-decl}{\mathrm{imports}}}({{\href{../text/modules.html#syntax-decl}{\mathit{decl}}}^\ast}) \\
{\land}~ {{\href{../syntax/modules.html#syntax-tag}{\mathit{tag}}}^\ast} = {\href{../text/modules.html#syntax-decl}{\mathrm{tags}}}({{\href{../text/modules.html#syntax-decl}{\mathit{decl}}}^\ast}) \\
{\land}~ {{\href{../syntax/modules.html#syntax-global}{\mathit{global}}}^\ast} = {\href{../text/modules.html#syntax-decl}{\mathrm{globals}}}({{\href{../text/modules.html#syntax-decl}{\mathit{decl}}}^\ast}) \\
{\land}~ {{\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}}^\ast} = {\href{../text/modules.html#syntax-decl}{\mathrm{mems}}}({{\href{../text/modules.html#syntax-decl}{\mathit{decl}}}^\ast}) \\
{\land}~ {{\href{../syntax/modules.html#syntax-table}{\mathit{table}}}^\ast} = {\href{../text/modules.html#syntax-decl}{\mathrm{tables}}}({{\href{../text/modules.html#syntax-decl}{\mathit{decl}}}^\ast}) \\
{\land}~ {{\href{../syntax/modules.html#syntax-func}{\mathit{func}}}^\ast} = {\href{../text/modules.html#syntax-decl}{\mathrm{funcs}}}({{\href{../text/modules.html#syntax-decl}{\mathit{decl}}}^\ast}) \\
{\land}~ {{\href{../syntax/modules.html#syntax-data}{\mathit{data}}}^\ast} = {\href{../text/modules.html#syntax-decl}{\mathrm{datas}}}({{\href{../text/modules.html#syntax-decl}{\mathit{decl}}}^\ast}) \\
{\land}~ {{\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}}^\ast} = {\href{../text/modules.html#syntax-decl}{\mathrm{elems}}}({{\href{../text/modules.html#syntax-decl}{\mathit{decl}}}^\ast}) \\
{\land}~ {{\href{../syntax/modules.html#syntax-start}{\mathit{start}}}^?} = {\href{../text/modules.html#syntax-decl}{\mathrm{starts}}}({{\href{../text/modules.html#syntax-decl}{\mathit{decl}}}^\ast}) \\
{\land}~ {{\href{../syntax/modules.html#syntax-export}{\mathit{export}}}^\ast} = {\href{../text/modules.html#syntax-decl}{\mathrm{exports}}}({{\href{../text/modules.html#syntax-decl}{\mathit{decl}}}^\ast}) \\
{\land}~ {\href{../text/modules.html#aux-ordered}{\mathrm{ordered}}}({{\href{../text/modules.html#syntax-decl}{\mathit{decl}}}^\ast}) \\
\end{array} \\
\end{array}
} \\
\end{array}
} \\
\end{array}\end{split}\]
where \({\mathrm{types}}({{\href{../text/modules.html#syntax-decl}{\mathit{decl}}}^\ast})\), \({\mathrm{imports}}({{\href{../text/modules.html#syntax-decl}{\mathit{decl}}}^\ast})\), \({\mathrm{tags}}({{\href{../text/modules.html#syntax-decl}{\mathit{decl}}}^\ast})\), etc., extract the sequence of types, imports, tags, etc., contained in \({{\href{../text/modules.html#syntax-decl}{\mathit{decl}}}^\ast}\), respectively. The auxiliary predicate \({\href{../text/modules.html#aux-ordered}{\mathrm{ordered}}}\) checks that no imports occur after the first definition of a tag, global, memory, table, or function in a sequence of declarations:
\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}}
{\href{../text/modules.html#aux-ordered}{\mathrm{ordered}}}({{\href{../text/modules.html#syntax-decl}{\mathit{decl}}'}^\ast}) & = & \mathsf{true} & \quad \mbox{if}~ {\href{../text/modules.html#syntax-decl}{\mathrm{imports}}}({{\href{../text/modules.html#syntax-decl}{\mathit{decl}}'}^\ast}) = \epsilon \\
{\href{../text/modules.html#aux-ordered}{\mathrm{ordered}}}({{\href{../text/modules.html#syntax-decl}{\mathit{decl}}}_1^\ast}~{\href{../syntax/modules.html#syntax-import}{\mathit{import}}}~{{\href{../text/modules.html#syntax-decl}{\mathit{decl}}}_2^\ast}) & = & & \\
\multicolumn{4}{@{}l@{}}{\quad
\begin{array}[t]{@{}l@{}}
{\href{../text/modules.html#syntax-decl}{\mathrm{imports}}}({{\href{../text/modules.html#syntax-decl}{\mathit{decl}}}_1^\ast}) = \epsilon \land {\href{../text/modules.html#syntax-decl}{\mathrm{tags}}}({{\href{../text/modules.html#syntax-decl}{\mathit{decl}}}_1^\ast}) = \epsilon \land {\href{../text/modules.html#syntax-decl}{\mathrm{globals}}}({{\href{../text/modules.html#syntax-decl}{\mathit{decl}}}_1^\ast}) = \epsilon \land {\href{../text/modules.html#syntax-decl}{\mathrm{mems}}}({{\href{../text/modules.html#syntax-decl}{\mathit{decl}}}_1^\ast}) = \epsilon \land {\href{../text/modules.html#syntax-decl}{\mathrm{tables}}}({{\href{../text/modules.html#syntax-decl}{\mathit{decl}}}_1^\ast}) = \epsilon \land {\href{../text/modules.html#syntax-decl}{\mathrm{funcs}}}({{\href{../text/modules.html#syntax-decl}{\mathit{decl}}}_1^\ast}) = \epsilon \\
\end{array}
} \\
\end{array}\end{split}\]
Abbreviations¶
In a source file, the toplevel \(\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{module}’}~~{\mathtt{decldots}}~~\mbox{‘\texttt{{)}}’}\) surrounding the module body may be omitted.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}l@{}l@{}}
& {\href{../text/modules.html#text-module}{\mathtt{module}}} & ::= & \dots ~~|~~ {{{\href{../text/modules.html#text-decl}{\mathtt{decl}}}}_{{\href{../text/conventions.html#text-context}{I}}}^\ast} & \quad\equiv\quad{} & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{module}’}~~{{{\href{../text/modules.html#text-decl}{\mathtt{decl}}}}_{{\href{../text/conventions.html#text-context}{I}}}^\ast}~~\mbox{‘\texttt{{)}}’} \\
\end{array}\end{split}\]