Modules¶
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 \(I\).
\[\begin{split}\begin{array}{llcllllllll}
\def\mathdef3294#1{{}}\mathdef3294{type index} & \href{../text/modules.html#text-typeidx}{\mathtt{typeidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef3319#1{{\mathtt{u}#1}}\mathdef3319{\mathtt{32}}} &\Rightarrow& x \\&&|&
v{:}\href{../text/values.html#text-id}{\mathtt{id}} &\Rightarrow& x & (\mathrel{\mbox{if}} I.\href{../text/conventions.html#text-context}{\mathsf{types}}[x] = v) \\
\def\mathdef3294#1{{}}\mathdef3294{function index} & \href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef3319#1{{\mathtt{u}#1}}\mathdef3319{\mathtt{32}}} &\Rightarrow& x \\&&|&
v{:}\href{../text/values.html#text-id}{\mathtt{id}} &\Rightarrow& x & (\mathrel{\mbox{if}} I.\href{../text/conventions.html#text-context}{\mathsf{funcs}}[x] = v) \\
\def\mathdef3294#1{{}}\mathdef3294{table index} & \href{../text/modules.html#text-tableidx}{\mathtt{tableidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef3319#1{{\mathtt{u}#1}}\mathdef3319{\mathtt{32}}} &\Rightarrow& x \\&&|&
v{:}\href{../text/values.html#text-id}{\mathtt{id}} &\Rightarrow& x & (\mathrel{\mbox{if}} I.\href{../text/conventions.html#text-context}{\mathsf{tables}}[x] = v) \\
\def\mathdef3294#1{{}}\mathdef3294{memory index} & \href{../text/modules.html#text-memidx}{\mathtt{memidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef3319#1{{\mathtt{u}#1}}\mathdef3319{\mathtt{32}}} &\Rightarrow& x \\&&|&
v{:}\href{../text/values.html#text-id}{\mathtt{id}} &\Rightarrow& x & (\mathrel{\mbox{if}} I.\href{../text/conventions.html#text-context}{\mathsf{mems}}[x] = v) \\
\def\mathdef3294#1{{}}\mathdef3294{global index} & \href{../text/modules.html#text-globalidx}{\mathtt{globalidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef3319#1{{\mathtt{u}#1}}\mathdef3319{\mathtt{32}}} &\Rightarrow& x \\&&|&
v{:}\href{../text/values.html#text-id}{\mathtt{id}} &\Rightarrow& x & (\mathrel{\mbox{if}} I.\href{../text/conventions.html#text-context}{\mathsf{globals}}[x] = v) \\
\def\mathdef3294#1{{}}\mathdef3294{element index} & \href{../text/modules.html#text-elemidx}{\mathtt{elemidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef3319#1{{\mathtt{u}#1}}\mathdef3319{\mathtt{32}}} &\Rightarrow& x \\&&|&
v{:}\href{../text/values.html#text-id}{\mathtt{id}} &\Rightarrow& x & (\mathrel{\mbox{if}} I.\href{../text/conventions.html#text-context}{\mathsf{elem}}[x] = v) \\
\def\mathdef3294#1{{}}\mathdef3294{data index} & \href{../text/modules.html#text-dataidx}{\mathtt{dataidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef3319#1{{\mathtt{u}#1}}\mathdef3319{\mathtt{32}}} &\Rightarrow& x \\&&|&
v{:}\href{../text/values.html#text-id}{\mathtt{id}} &\Rightarrow& x & (\mathrel{\mbox{if}} I.\href{../text/conventions.html#text-context}{\mathsf{data}}[x] = v) \\
\def\mathdef3294#1{{}}\mathdef3294{local index} & \href{../text/modules.html#text-localidx}{\mathtt{localidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef3319#1{{\mathtt{u}#1}}\mathdef3319{\mathtt{32}}} &\Rightarrow& x \\&&|&
v{:}\href{../text/values.html#text-id}{\mathtt{id}} &\Rightarrow& x & (\mathrel{\mbox{if}} I.\href{../text/conventions.html#text-context}{\mathsf{locals}}[x] = v) \\
\def\mathdef3294#1{{}}\mathdef3294{label index} & \href{../text/modules.html#text-labelidx}{\mathtt{labelidx}}_I &::=&
l{:}\href{../text/values.html#text-int}{\def\mathdef3319#1{{\mathtt{u}#1}}\mathdef3319{\mathtt{32}}} &\Rightarrow& l \\&&|&
v{:}\href{../text/values.html#text-id}{\mathtt{id}} &\Rightarrow& l & (\mathrel{\mbox{if}} I.\href{../text/conventions.html#text-context}{\mathsf{labels}}[l] = v) \\
\end{array}\end{split}\]
Types¶
Type definitions can bind a symbolic type identifier.
\[\begin{split}\begin{array}{llclll}
\def\mathdef3294#1{{}}\mathdef3294{type definition} & \href{../text/modules.html#text-typedef}{\mathtt{type}}_I &::=&
\def\mathdef3333#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3333{(}~\def\mathdef3334#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3334{type}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{ft}{:}\href{../text/types.html#text-functype}{\mathtt{functype}}_I~\def\mathdef3335#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3335{)}
&\Rightarrow& \mathit{ft} \\
\end{array}\end{split}\]
Type Uses¶
A type use is a reference to a type definition. It may optionally be augmented by explicit inlined parameter and result declarations. That allows binding symbolic identifiers to name the local indices of parameters. If inline declarations are given, then their types must match the referenced function type.
\[\begin{split}\begin{array}{llcllll}
\def\mathdef3294#1{{}}\mathdef3294{type use} & \href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}_I &::=&
\def\mathdef3336#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3336{(}~\def\mathdef3337#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3337{type}~~x{:}\href{../text/modules.html#text-typeidx}{\mathtt{typeidx}}_I~\def\mathdef3338#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3338{)}
\quad\Rightarrow\quad x, I' \\ &&& \qquad
(\mathrel{\mbox{if}} \begin{array}[t]{@{}l@{}}
I.\href{../text/conventions.html#text-context}{\mathsf{typedefs}}[x] = [t_1^n] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] \wedge
I' = \{\href{../text/conventions.html#text-context}{\mathsf{locals}}~(\epsilon)^n\}) \\
\end{array} \\[1ex] &&|&
\def\mathdef3339#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3339{(}~\def\mathdef3340#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3340{type}~~x{:}\href{../text/modules.html#text-typeidx}{\mathtt{typeidx}}_I~\def\mathdef3341#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3341{)}
~~(t_1{:}\href{../text/types.html#text-functype}{\mathtt{param}})^\ast~~(t_2{:}\href{../text/types.html#text-functype}{\mathtt{result}})^\ast
\quad\Rightarrow\quad x, I' \\ &&& \qquad
(\mathrel{\mbox{if}} \begin{array}[t]{@{}l@{}}
I.\href{../text/conventions.html#text-context}{\mathsf{typedefs}}[x] = [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] \wedge
I' = \{\href{../text/conventions.html#text-context}{\mathsf{locals}}~\mathrm{id}(\href{../text/types.html#text-functype}{\mathtt{param}})^\ast\} ~\href{../text/conventions.html#text-context-wf}{\mbox{well-formed}}) \\
\end{array} \\
\end{array}\end{split}\]
The synthesized attribute of a \(\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}\) is a pair consisting of both the used type index and the updated identifier context including possible parameter identifiers. The following auxiliary function extracts optional identifiers from parameters:
\[\begin{split}\begin{array}{lcl@{\qquad\qquad}l}
\mathrm{id}(\def\mathdef3342#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3342{(}~\def\mathdef3343#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3343{param}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3344#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3344{)}) &=& \href{../text/values.html#text-id}{\mathtt{id}}^? \\
\end{array}\end{split}\]
Note
Both productions overlap for the case that the function type is \([] \href{../syntax/types.html#syntax-functype}{\rightarrow} []\). However, in that case, they also produce the same results, so that the choice is immaterial.
The well-formedness condition on \(I'\) ensures that the parameters do not contain duplicate identifier.
Abbreviations¶
A \(\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}\) may also be replaced entirely by inline parameter and result declarations. In that case, a type index is automatically inserted:
\[\begin{split}\begin{array}{llclll}
\def\mathdef3294#1{{}}\mathdef3294{type use} &
(t_1{:}\href{../text/types.html#text-functype}{\mathtt{param}})^\ast~~(t_2{:}\href{../text/types.html#text-functype}{\mathtt{result}})^\ast &\equiv&
\def\mathdef3345#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3345{(}~\def\mathdef3346#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3346{type}~~x~\def\mathdef3347#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3347{)}~~\href{../text/types.html#text-functype}{\mathtt{param}}^\ast~~\href{../text/types.html#text-functype}{\mathtt{result}}^\ast \\
\end{array}\end{split}\]
where \(x\) is the smallest existing type index whose definition in the current module is the function type \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\). If no such index exists, then a new type definition of the form
\[\def\mathdef3348#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3348{(}~\def\mathdef3349#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3349{type}~~\def\mathdef3350#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3350{(}~\def\mathdef3351#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3351{func}~~\href{../text/types.html#text-functype}{\mathtt{param}}^\ast~~\href{../text/types.html#text-functype}{\mathtt{result}}^\ast~\def\mathdef3352#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3352{)}~\def\mathdef3353#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3353{)}\]
is inserted at the end of the module.
Abbreviations are expanded in the order they appear, such that previously inserted type definitions are reused by consecutive expansions.
Imports¶
The descriptors in imports can bind a symbolic function, table, memory, or global identifier.
\[\begin{split}\begin{array}{llclll}
\def\mathdef3294#1{{}}\mathdef3294{import} & \href{../text/modules.html#text-import}{\mathtt{import}}_I &::=&
\def\mathdef3354#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3354{(}~\def\mathdef3355#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3355{import}~~\mathit{mod}{:}\href{../text/values.html#text-name}{\mathtt{name}}~~\mathit{nm}{:}\href{../text/values.html#text-name}{\mathtt{name}}~~d{:}\href{../text/modules.html#text-importdesc}{\mathtt{importdesc}}_I~\def\mathdef3356#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3356{)} \\ &&& \qquad
\Rightarrow\quad \{ \href{../syntax/modules.html#syntax-import}{\mathsf{module}}~\mathit{mod}, \href{../syntax/modules.html#syntax-import}{\mathsf{name}}~\mathit{nm}, \href{../syntax/modules.html#syntax-import}{\mathsf{desc}}~d \} \\[1ex]
\def\mathdef3294#1{{}}\mathdef3294{import description} & \href{../text/modules.html#text-importdesc}{\mathtt{importdesc}}_I &::=&
\def\mathdef3357#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3357{(}~\def\mathdef3358#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3358{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~x,I'{:}\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}_I~\def\mathdef3359#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3359{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{func}}~x \\ &&|&
\def\mathdef3360#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3360{(}~\def\mathdef3361#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3361{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{tt}{:}\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}_I~\def\mathdef3362#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3362{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{table}}~\mathit{tt} \\ &&|&
\def\mathdef3363#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3363{(}~\def\mathdef3364#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3364{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{mt}{:}\href{../text/types.html#text-memtype}{\mathtt{memtype}}_I~\def\mathdef3365#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3365{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{mem}}~~\mathit{mt} \\ &&|&
\def\mathdef3366#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3366{(}~\def\mathdef3367#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3367{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{gt}{:}\href{../text/types.html#text-globaltype}{\mathtt{globaltype}}_I~\def\mathdef3368#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3368{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{global}}~\mathit{gt} \\
\end{array}\end{split}\]
Abbreviations¶
As an abbreviation, imports may also be specified inline with function, table, memory, or global definitions; see the respective sections.
Functions¶
Function definitions can bind a symbolic function identifier, and local identifiers for its parameters and locals.
\[\begin{split}\begin{array}{llclll}
\def\mathdef3294#1{{}}\mathdef3294{function} & \href{../text/modules.html#text-func}{\mathtt{func}}_I &::=&
\def\mathdef3369#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3369{(}~\def\mathdef3370#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3370{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~x,I'{:}\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}_I~~
(t{:}\href{../text/modules.html#text-local}{\mathtt{local}}_I)^\ast~~(\mathit{in}{:}\href{../text/instructions.html#text-instr}{\mathtt{instr}}_{I''})^\ast~\def\mathdef3371#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3371{)} \\ &&& \qquad
\Rightarrow\quad \{ \href{../syntax/modules.html#syntax-func}{\mathsf{type}}~x, \href{../syntax/modules.html#syntax-func}{\mathsf{locals}}~t^\ast, \href{../syntax/modules.html#syntax-func}{\mathsf{body}}~\mathit{in}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \} \\ &&& \qquad\qquad\qquad
(\mathrel{\mbox{if}} I'' = I' \href{../syntax/conventions.html#notation-compose}{\oplus} \{\href{../text/conventions.html#text-context}{\mathsf{locals}}~\mathrm{id}(\href{../text/modules.html#text-local}{\mathtt{local}})^\ast\} ~\href{../text/conventions.html#text-context-wf}{\mbox{well-formed}}) \\[1ex]
\def\mathdef3294#1{{}}\mathdef3294{local} & \href{../text/modules.html#text-local}{\mathtt{local}}_I &::=&
\def\mathdef3372#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3372{(}~\def\mathdef3373#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3373{local}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~t{:}\href{../text/types.html#text-valtype}{\mathtt{valtype}}_I~\def\mathdef3374#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3374{)}
\quad\Rightarrow\quad t \\
\end{array}\end{split}\]
The definition of the local identifier context \(I''\) uses the following auxiliary function to extract optional identifiers from locals:
\[\begin{split}\begin{array}{lcl@{\qquad\qquad}l}
\mathrm{id}(\def\mathdef3375#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3375{(}~\def\mathdef3376#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3376{local}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3377#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3377{)}) &=& \href{../text/values.html#text-id}{\mathtt{id}}^? \\
\end{array}\end{split}\]
Note
The well-formedness condition on \(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}{llclll}
\def\mathdef3294#1{{}}\mathdef3294{local} &
\def\mathdef3378#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3378{(}~~\def\mathdef3379#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3379{local}~~\href{../text/types.html#text-valtype}{\mathtt{valtype}}^\ast~~\def\mathdef3380#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3380{)} &\equiv&
(\def\mathdef3381#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3381{(}~~\def\mathdef3382#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3382{local}~~\href{../text/types.html#text-valtype}{\mathtt{valtype}}~~\def\mathdef3383#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3383{)})^\ast \\
\end{array}\end{split}\]
Functions can be defined as imports or exports inline:
\[\begin{split}\begin{array}{llclll}
\def\mathdef3294#1{{}}\mathdef3294{module field} &
\def\mathdef3384#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3384{(}~\def\mathdef3385#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3385{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3386#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3386{(}~\def\mathdef3387#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3387{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef3388#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3388{)}~~\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}~\def\mathdef3389#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3389{)} \quad\equiv \\ & \qquad
\def\mathdef3390#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3390{(}~\def\mathdef3391#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3391{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef3392#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3392{(}~\def\mathdef3393#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3393{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}~\def\mathdef3394#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3394{)}~\def\mathdef3395#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3395{)} \\[1ex] &
\def\mathdef3396#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3396{(}~\def\mathdef3397#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3397{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3398#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3398{(}~\def\mathdef3399#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3399{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef3400#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3400{)}~~\dots~\def\mathdef3401#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3401{)} \quad\equiv \\ & \qquad
\def\mathdef3402#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3402{(}~\def\mathdef3403#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3403{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef3404#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3404{(}~\def\mathdef3405#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3405{func}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3406#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3406{)}~\def\mathdef3407#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3407{)}~~
\def\mathdef3408#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3408{(}~\def\mathdef3409#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3409{func}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef3410#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3410{)}
\\ & \qquad\qquad
(\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \vee \href{../text/values.html#text-id}{\mathtt{id}}^? = \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}) \\
\end{array}\end{split}\]
The latter abbreviation can be applied repeatedly, with “\(\dots\)” containing another import or export.
Tables¶
Table definitions can bind a symbolic table identifier.
\[\begin{split}\begin{array}{llclll}
\def\mathdef3294#1{{}}\mathdef3294{table} & \href{../text/modules.html#text-table}{\mathtt{table}}_I &::=&
\def\mathdef3411#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3411{(}~\def\mathdef3412#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3412{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{tt}{:}\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}_I~\def\mathdef3413#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3413{)}
&\Rightarrow& \{ \href{../syntax/modules.html#syntax-table}{\mathsf{type}}~\mathit{tt} \} \\
\end{array}\end{split}\]
Abbreviations¶
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}{llclll}
\def\mathdef3294#1{{}}\mathdef3294{module field} &
\def\mathdef3414#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3414{(}~\def\mathdef3415#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3415{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~~\def\mathdef3416#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3416{(}~\def\mathdef3417#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3417{elem}~~\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}^n{:}\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-elemexpr}{\mathtt{elemexpr}})~\def\mathdef3418#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3418{)}~~\def\mathdef3419#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3419{)} \quad\equiv \\ & \qquad
\def\mathdef3420#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3420{(}~\def\mathdef3421#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3421{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~n~~n~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~\def\mathdef3422#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3422{)} \\ & \qquad
\def\mathdef3423#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3423{(}~\def\mathdef3424#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3424{elem}~~\def\mathdef3425#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3425{(}~\def\mathdef3426#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3426{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3427#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3427{)}~~\def\mathdef3428#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3428{(}~\def\mathdef3429#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3429{i32.const}~~\def\mathdef3430#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3430{0}~\def\mathdef3431#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3431{)}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-elemexpr}{\mathtt{elemexpr}})~\def\mathdef3432#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3432{)}
\\ & \qquad\qquad
(\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \vee \href{../text/values.html#text-id}{\mathtt{id}}^? = \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}) \\
\end{array}\end{split}\]
\[\begin{split}\begin{array}{llclll}
\def\mathdef3294#1{{}}\mathdef3294{module field} &
\def\mathdef3433#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3433{(}~\def\mathdef3434#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3434{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~~\def\mathdef3435#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3435{(}~\def\mathdef3436#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3436{elem}~~x^n{:}\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}})~\def\mathdef3437#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3437{)} \quad\equiv \\ & \qquad
\def\mathdef3438#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3438{(}~\def\mathdef3439#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3439{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~n~~n~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~\def\mathdef3440#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3440{)} \\ & \qquad
\def\mathdef3441#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3441{(}~\def\mathdef3442#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3442{elem}~~\def\mathdef3443#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3443{(}~\def\mathdef3444#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3444{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3445#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3445{)}~~\def\mathdef3446#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3446{(}~\def\mathdef3447#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3447{i32.const}~~\def\mathdef3448#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3448{0}~\def\mathdef3449#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3449{)}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}})~\def\mathdef3450#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3450{)}
\\ & \qquad\qquad
(\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \vee \href{../text/values.html#text-id}{\mathtt{id}}^? = \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}) \\
\end{array}\end{split}\]
Tables can be defined as imports or exports inline:
\[\begin{split}\begin{array}{llclll}
\def\mathdef3294#1{{}}\mathdef3294{module field} &
\def\mathdef3451#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3451{(}~\def\mathdef3452#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3452{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3453#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3453{(}~\def\mathdef3454#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3454{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef3455#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3455{)}~~\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}~\def\mathdef3456#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3456{)} \quad\equiv \\ & \qquad
\def\mathdef3457#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3457{(}~\def\mathdef3458#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3458{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef3459#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3459{(}~\def\mathdef3460#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3460{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}~\def\mathdef3461#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3461{)}~\def\mathdef3462#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3462{)} \\[1ex] &
\def\mathdef3463#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3463{(}~\def\mathdef3464#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3464{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3465#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3465{(}~\def\mathdef3466#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3466{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef3467#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3467{)}~~\dots~\def\mathdef3468#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3468{)} \quad\equiv \\ & \qquad
\def\mathdef3469#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3469{(}~\def\mathdef3470#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3470{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef3471#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3471{(}~\def\mathdef3472#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3472{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3473#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3473{)}~\def\mathdef3474#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3474{)}~~
\def\mathdef3475#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3475{(}~\def\mathdef3476#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3476{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef3477#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3477{)}
\\ & \qquad\qquad
(\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \vee \href{../text/values.html#text-id}{\mathtt{id}}^? = \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}) \\
\end{array}\end{split}\]
The latter abbreviation can be applied repeatedly, with “\(\dots\)” containing another import or export or an inline elements segment.
Memories¶
Memory definitions can bind a symbolic memory identifier.
\[\begin{split}\begin{array}{llclll}
\def\mathdef3294#1{{}}\mathdef3294{memory} & \href{../text/modules.html#text-mem}{\mathtt{mem}}_I &::=&
\def\mathdef3478#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3478{(}~\def\mathdef3479#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3479{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{mt}{:}\href{../text/types.html#text-memtype}{\mathtt{memtype}}_I~\def\mathdef3480#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3480{)}
&\Rightarrow& \{ \href{../syntax/modules.html#syntax-mem}{\mathsf{type}}~\mathit{mt} \} \\
\end{array}\end{split}\]
Abbreviations¶
A data segment can be given inline with a memory definition, in which case its offset is \(0\) the limits of the memory type are inferred from the length of the data, rounded up to page size:
\[\begin{split}\begin{array}{llclll}
\def\mathdef3294#1{{}}\mathdef3294{module field} &
\def\mathdef3481#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3481{(}~\def\mathdef3482#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3482{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3483#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3483{(}~\def\mathdef3484#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3484{data}~~b^n{:}\href{../text/modules.html#text-datastring}{\mathtt{datastring}}~\def\mathdef3485#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3485{)}~~\def\mathdef3486#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3486{)} \quad\equiv \\ & \qquad
\def\mathdef3487#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3487{(}~\def\mathdef3488#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3488{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~m~~m~\def\mathdef3489#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3489{)} \\ & \qquad
\def\mathdef3490#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3490{(}~\def\mathdef3491#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3491{data}~~\def\mathdef3492#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3492{(}~\def\mathdef3493#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3493{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3494#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3494{)}~~\def\mathdef3495#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3495{(}~\def\mathdef3496#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3496{i32.const}~~\def\mathdef3497#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3497{0}~\def\mathdef3498#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3498{)}~~\href{../text/modules.html#text-datastring}{\mathtt{datastring}}~\def\mathdef3499#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3499{)}
\\ & \qquad\qquad
(\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \vee \href{../text/values.html#text-id}{\mathtt{id}}^? = \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}, m = \mathrm{ceil}(n / 64\mathrm{Ki})) \\
\end{array}\end{split}\]
Memories can be defined as imports or exports inline:
\[\begin{split}\begin{array}{llclll}
\def\mathdef3294#1{{}}\mathdef3294{module field} &
\def\mathdef3500#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3500{(}~\def\mathdef3501#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3501{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3502#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3502{(}~\def\mathdef3503#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3503{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef3504#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3504{)}~~\href{../text/types.html#text-memtype}{\mathtt{memtype}}~\def\mathdef3505#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3505{)} \quad\equiv \\ & \qquad
\def\mathdef3506#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3506{(}~\def\mathdef3507#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3507{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef3508#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3508{(}~\def\mathdef3509#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3509{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-memtype}{\mathtt{memtype}}~\def\mathdef3510#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3510{)}~\def\mathdef3511#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3511{)}
\\[1ex] &
\def\mathdef3512#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3512{(}~\def\mathdef3513#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3513{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3514#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3514{(}~\def\mathdef3515#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3515{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef3516#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3516{)}~~\dots~\def\mathdef3517#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3517{)} \quad\equiv \\ & \qquad
\def\mathdef3518#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3518{(}~\def\mathdef3519#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3519{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef3520#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3520{(}~\def\mathdef3521#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3521{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3522#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3522{)}~\def\mathdef3523#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3523{)}~~
\def\mathdef3524#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3524{(}~\def\mathdef3525#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3525{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef3526#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3526{)}
\\ & \qquad\qquad
(\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \vee \href{../text/values.html#text-id}{\mathtt{id}}^? = \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}) \\
\end{array}\end{split}\]
The latter abbreviation can be applied repeatedly, with “\(\dots\)” containing another import or export or an inline data segment.
Globals¶
Global definitions can bind a symbolic global identifier.
\[\begin{split}\begin{array}{llclll}
\def\mathdef3294#1{{}}\mathdef3294{global} & \href{../text/modules.html#text-global}{\mathtt{global}}_I &::=&
\def\mathdef3527#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3527{(}~\def\mathdef3528#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3528{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{gt}{:}\href{../text/types.html#text-globaltype}{\mathtt{globaltype}}_I~~e{:}\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef3529#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3529{)}
&\Rightarrow& \{ \href{../syntax/modules.html#syntax-global}{\mathsf{type}}~\mathit{gt}, \href{../syntax/modules.html#syntax-global}{\mathsf{init}}~e \} \\
\end{array}\end{split}\]
Abbreviations¶
Globals can be defined as imports or exports inline:
\[\begin{split}\begin{array}{llclll}
\def\mathdef3294#1{{}}\mathdef3294{module field} &
\def\mathdef3530#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3530{(}~\def\mathdef3531#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3531{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3532#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3532{(}~\def\mathdef3533#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3533{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef3534#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3534{)}~~\href{../text/types.html#text-globaltype}{\mathtt{globaltype}}~\def\mathdef3535#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3535{)} \quad\equiv \\ & \qquad
\def\mathdef3536#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3536{(}~\def\mathdef3537#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3537{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef3538#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3538{(}~\def\mathdef3539#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3539{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-globaltype}{\mathtt{globaltype}}~\def\mathdef3540#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3540{)}~\def\mathdef3541#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3541{)}
\\[1ex] &
\def\mathdef3542#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3542{(}~\def\mathdef3543#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3543{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3544#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3544{(}~\def\mathdef3545#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3545{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef3546#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3546{)}~~\dots~\def\mathdef3547#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3547{)} \quad\equiv \\ & \qquad
\def\mathdef3548#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3548{(}~\def\mathdef3549#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3549{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef3550#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3550{(}~\def\mathdef3551#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3551{global}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3552#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3552{)}~\def\mathdef3553#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3553{)}~~
\def\mathdef3554#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3554{(}~\def\mathdef3555#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3555{global}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef3556#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3556{)}
\\ & \qquad\qquad
(\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \vee \href{../text/values.html#text-id}{\mathtt{id}}^? = \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}) \\
\end{array}\end{split}\]
The latter abbreviation can be applied repeatedly, with “\(\dots\)” containing another import or export.
Exports¶
The syntax for exports mirrors their abstract syntax directly.
\[\begin{split}\begin{array}{llclll}
\def\mathdef3294#1{{}}\mathdef3294{export} & \href{../text/modules.html#text-export}{\mathtt{export}}_I &::=&
\def\mathdef3557#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3557{(}~\def\mathdef3558#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3558{export}~~\mathit{nm}{:}\href{../text/values.html#text-name}{\mathtt{name}}~~d{:}\href{../text/modules.html#text-exportdesc}{\mathtt{exportdesc}}_I~\def\mathdef3559#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3559{)}
&\Rightarrow& \{ \href{../syntax/modules.html#syntax-export}{\mathsf{name}}~\mathit{nm}, \href{../syntax/modules.html#syntax-export}{\mathsf{desc}}~d \} \\
\def\mathdef3294#1{{}}\mathdef3294{export description} & \href{../text/modules.html#text-exportdesc}{\mathtt{exportdesc}}_I &::=&
\def\mathdef3560#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3560{(}~\def\mathdef3561#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3561{func}~~x{:}\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I~\def\mathdef3562#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3562{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{func}}~x \\ &&|&
\def\mathdef3563#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3563{(}~\def\mathdef3564#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3564{table}~~x{:}\href{../text/modules.html#text-tableidx}{\mathtt{tableidx}}_I~\def\mathdef3565#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3565{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{table}}~x \\ &&|&
\def\mathdef3566#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3566{(}~\def\mathdef3567#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3567{memory}~~x{:}\href{../text/modules.html#text-memidx}{\mathtt{memidx}}_I~\def\mathdef3568#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3568{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{mem}}~x \\ &&|&
\def\mathdef3569#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3569{(}~\def\mathdef3570#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3570{global}~~x{:}\href{../text/modules.html#text-globalidx}{\mathtt{globalidx}}_I~\def\mathdef3571#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3571{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{global}}~x \\
\end{array}\end{split}\]
Abbreviations¶
As an abbreviation, exports may also be specified inline with function, table, memory, or global definitions; see the respective sections.
Start Function¶
A start function is defined in terms of its index.
\[\begin{split}\begin{array}{llclll}
\def\mathdef3294#1{{}}\mathdef3294{start function} & \href{../text/modules.html#text-start}{\mathtt{start}}_I &::=&
\def\mathdef3572#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3572{(}~\def\mathdef3573#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3573{start}~~x{:}\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I~\def\mathdef3574#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3574{)}
&\Rightarrow& \{ \href{../syntax/modules.html#syntax-start}{\mathsf{func}}~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.
Element Segments¶
Element segments allow for an optional table index to identify the table to initialize.
\[\begin{split}\begin{array}{llclll}
\def\mathdef3294#1{{}}\mathdef3294{element segment} & \href{../text/modules.html#text-elem}{\mathtt{elem}}_I &::=&
\def\mathdef3575#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3575{(}~\def\mathdef3576#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3576{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~(et, y^\ast){:}\href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}_I~\def\mathdef3577#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3577{)} \\ &&& \qquad
\Rightarrow\quad \{ \href{../syntax/modules.html#syntax-elem}{\mathsf{type}}~et, \href{../syntax/modules.html#syntax-elem}{\mathsf{init}}~y^\ast, \href{../syntax/modules.html#syntax-elem}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-elemmode}{\mathsf{passive}} \} \\ &&|&
\def\mathdef3578#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3578{(}~\def\mathdef3579#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3579{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~x{:}\href{../text/modules.html#text-tableuse}{\mathtt{tableuse}}_I~~\def\mathdef3580#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3580{(}~\def\mathdef3581#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3581{offset}~~e{:}\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef3582#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3582{)}~~(et, y^\ast){:}\href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}_I~\def\mathdef3583#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3583{)} \\ &&& \qquad
\Rightarrow\quad \{ \href{../syntax/modules.html#syntax-elem}{\mathsf{type}}~et, \href{../syntax/modules.html#syntax-elem}{\mathsf{init}}~y^\ast, \href{../syntax/modules.html#syntax-elem}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-elemmode}{\mathsf{active}}~\{ \href{../syntax/modules.html#syntax-elem}{\mathsf{table}}~x, \href{../syntax/modules.html#syntax-elem}{\mathsf{offset}}~e \} \} \\ &&&
\def\mathdef3584#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3584{(}~\def\mathdef3585#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3585{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3586#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3586{declare}~~(et, y^\ast){:}\href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}_I~\def\mathdef3587#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3587{)} \\ &&& \qquad
\Rightarrow\quad \{ \href{../syntax/modules.html#syntax-elem}{\mathsf{type}}~et, \href{../syntax/modules.html#syntax-elem}{\mathsf{init}}~y^\ast, \href{../syntax/modules.html#syntax-elem}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-elemmode}{\mathsf{declarative}} \} \\
\def\mathdef3294#1{{}}\mathdef3294{element list} & \href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}_I &::=&
t{:}\href{../text/types.html#text-reftype}{\mathtt{reftype}}_I~~y^\ast{:}\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-elemexpr}{\mathtt{elemexpr}}_I) \qquad\Rightarrow\quad ( \href{../syntax/modules.html#syntax-elem}{\mathsf{type}}~t, \href{../syntax/modules.html#syntax-elem}{\mathsf{init}}~y^\ast ) \\
\def\mathdef3294#1{{}}\mathdef3294{element expression} & \href{../text/modules.html#text-elemexpr}{\mathtt{elemexpr}}_I &::=&
\def\mathdef3588#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3588{(}~\def\mathdef3589#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3589{item}~~e{:}\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef3590#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3590{)}
\quad\Rightarrow\quad e \\
\def\mathdef3294#1{{}}\mathdef3294{table use} & \href{../text/modules.html#text-tableuse}{\mathtt{tableuse}}_I &::=&
\def\mathdef3591#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3591{(}~\def\mathdef3592#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3592{table}~~x{:}\href{../text/modules.html#text-tableidx}{\mathtt{tableidx}}_I ~\def\mathdef3593#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3593{)}
\quad\Rightarrow\quad x \\
\end{array}\end{split}\]
Abbreviations¶
As an abbreviation, a single instruction may occur in place of the offset of an active element segment or as an element expression:
\[\begin{split}\begin{array}{llcll}
\def\mathdef3294#1{{}}\mathdef3294{element offset} &
\def\mathdef3594#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3594{(}~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef3595#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3595{)} &\equiv&
\def\mathdef3596#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3596{(}~\def\mathdef3597#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3597{offset}~~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef3598#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3598{)} \\
\def\mathdef3294#1{{}}\mathdef3294{element item} &
\def\mathdef3599#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3599{(}~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef3600#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3600{)} &\equiv&
\def\mathdef3601#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3601{(}~\def\mathdef3602#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3602{item}~~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef3603#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3603{)} \\
\end{array}\end{split}\]
Also, the element list may be written as just a sequence of function indices:
\[\begin{array}{llcll}
\def\mathdef3294#1{{}}\mathdef3294{element list} &
\def\mathdef3604#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3604{func}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I) &\equiv&
\def\mathdef3605#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3605{funcref}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\def\mathdef3606#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3606{(}~\def\mathdef3607#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3607{ref.func}~~\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I~\def\mathdef3608#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3608{)})
\end{array}\]
A table use can be omitted, defaulting to \(\mathtt{0}\). Furthermore, for backwards compatibility with earlier versions of WebAssembly, if the table use is omitted, the \(\def\mathdef3609#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3609{func}\) keyword can be omitted as well.
\[\begin{split}\begin{array}{llclll}
\def\mathdef3294#1{{}}\mathdef3294{table use} &
\epsilon &\equiv& \def\mathdef3610#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3610{(}~\def\mathdef3611#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3611{table}~~\def\mathdef3612#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3612{0}~\def\mathdef3613#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3613{)} \\
\def\mathdef3294#1{{}}\mathdef3294{element segment} &
\def\mathdef3614#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3614{(}~\def\mathdef3615#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3615{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3616#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3616{(}~\def\mathdef3617#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3617{offset}~~\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef3618#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3618{)}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I)~\def\mathdef3619#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3619{)}
&\equiv&
\def\mathdef3620#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3620{(}~\def\mathdef3621#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3621{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3622#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3622{(}~\def\mathdef3623#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3623{table}~~\def\mathdef3624#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3624{0}~\def\mathdef3625#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3625{)}~~\def\mathdef3626#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3626{(}~\def\mathdef3627#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3627{offset}~~\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef3628#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3628{)}~~\def\mathdef3629#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3629{func}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I)~\def\mathdef3630#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3630{)}
\end{array}\end{split}\]
As another abbreviation, element segments may also be specified inline with table definitions; see the respective section.
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}{llclll}
\def\mathdef3294#1{{}}\mathdef3294{data segment} & \href{../text/modules.html#text-data}{\mathtt{data}}_I &::=&
\def\mathdef3631#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3631{(}~\def\mathdef3632#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3632{data}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~b^\ast{:}\href{../text/modules.html#text-datastring}{\mathtt{datastring}}~\def\mathdef3633#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3633{)} \\ &&& \qquad
\Rightarrow\quad \{ \href{../syntax/modules.html#syntax-data}{\mathsf{init}}~b^\ast, \href{../syntax/modules.html#syntax-data}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-datamode}{\mathsf{passive}} \} \\ &&|&
\def\mathdef3634#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3634{(}~\def\mathdef3635#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3635{data}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~x{:}\href{../text/modules.html#text-memuse}{\mathtt{memuse}}_I~~\def\mathdef3636#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3636{(}~\def\mathdef3637#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3637{offset}~~e{:}\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef3638#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3638{)}~~b^\ast{:}\href{../text/modules.html#text-datastring}{\mathtt{datastring}}~\def\mathdef3639#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3639{)} \\ &&& \qquad
\Rightarrow\quad \{ \href{../syntax/modules.html#syntax-data}{\mathsf{init}}~b^\ast, \href{../syntax/modules.html#syntax-data}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-datamode}{\mathsf{active}}~\{ \href{../syntax/modules.html#syntax-data}{\mathsf{memory}}~x', \href{../syntax/modules.html#syntax-data}{\mathsf{offset}}~e \} \} \\
\def\mathdef3294#1{{}}\mathdef3294{data string} & \href{../text/modules.html#text-datastring}{\mathtt{datastring}} &::=&
(b^\ast{:}\href{../text/values.html#text-string}{\mathtt{string}})^\ast \quad\Rightarrow\quad \href{../syntax/conventions.html#notation-concat}{\mathrm{concat}}((b^\ast)^\ast) \\
\def\mathdef3294#1{{}}\mathdef3294{memory use} & \href{../text/modules.html#text-memuse}{\mathtt{memuse}}_I &::=&
\def\mathdef3640#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3640{(}~\def\mathdef3641#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3641{memory}~~x{:}\href{../text/modules.html#text-memidx}{\mathtt{memidx}}_I ~\def\mathdef3642#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3642{)}
\quad\Rightarrow\quad x \\
\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 instruction may occur in place of the offset of an active data segment:
\[\begin{array}{llcll}
\def\mathdef3294#1{{}}\mathdef3294{data offset} &
\def\mathdef3643#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3643{(}~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef3644#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3644{)} &\equiv&
\def\mathdef3645#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3645{(}~\def\mathdef3646#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3646{offset}~~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef3647#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3647{)}
\end{array}\]
Also, a memory use can be omitted, defaulting to \(\mathtt{0}\).
\[\begin{split}\begin{array}{llclll}
\def\mathdef3294#1{{}}\mathdef3294{memory use} &
\epsilon &\equiv& \def\mathdef3648#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3648{(}~\def\mathdef3649#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3649{memory}~~\def\mathdef3650#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3650{0}~\def\mathdef3651#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3651{)} \\
\end{array}\end{split}\]
As another abbreviation, data segments may also be specified inline with memory definitions; see the respective section.
Modules¶
A module consists of a sequence of fields that can occur in any order. All definitions and their respective bound identifiers scope over the entire module, including the text preceding them.
A module 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}{lll}
\def\mathdef3294#1{{}}\mathdef3294{module} & \href{../text/modules.html#text-module}{\mathtt{module}} &
\begin{array}[t]{@{}cllll}
::=&
\def\mathdef3652#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3652{(}~\def\mathdef3653#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3653{module}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~(m{:}\href{../text/modules.html#text-modulefield}{\mathtt{modulefield}}_I)^\ast~\def\mathdef3654#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3654{)}
\quad\Rightarrow\quad \href{../syntax/conventions.html#notation-compose}{\bigoplus} m^\ast \\
&\qquad (\mathrel{\mbox{if}} I = \href{../syntax/conventions.html#notation-compose}{\bigoplus} \mathrm{idc}(\href{../text/modules.html#text-modulefield}{\mathtt{modulefield}})^\ast ~\href{../text/conventions.html#text-context-wf}{\mbox{well-formed}}) \\
\end{array} \\[1ex]
\def\mathdef3294#1{{}}\mathdef3294{module field} & \href{../text/modules.html#text-modulefield}{\mathtt{modulefield}}_I &
\begin{array}[t]{@{}clll}
::=&
\mathit{ty}{:}\href{../text/modules.html#text-typedef}{\mathtt{type}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{types}}~\mathit{ty}\} \\ |&
\mathit{im}{:}\href{../text/modules.html#text-import}{\mathtt{import}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{imports}}~\mathit{im}\} \\ |&
\mathit{fn}{:}\href{../text/modules.html#text-func}{\mathtt{func}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{funcs}}~\mathit{fn}\} \\ |&
\mathit{ta}{:}\href{../text/modules.html#text-table}{\mathtt{table}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{tables}}~\mathit{ta}\} \\ |&
\mathit{me}{:}\href{../text/modules.html#text-mem}{\mathtt{mem}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{mems}}~\mathit{me}\} \\ |&
\mathit{gl}{:}\href{../text/modules.html#text-global}{\mathtt{global}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{globals}}~\mathit{gl}\} \\ |&
\mathit{ex}{:}\href{../text/modules.html#text-export}{\mathtt{export}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{exports}}~\mathit{ex}\} \\ |&
\mathit{st}{:}\href{../text/modules.html#text-start}{\mathtt{start}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{start}}~\mathit{st}\} \\ |&
\mathit{el}{:}\href{../text/modules.html#text-elem}{\mathtt{elem}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{elems}}~\mathit{el}\} \\ |&
\mathit{da}{:}\href{../text/modules.html#text-data}{\mathtt{data}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{datas}}~\mathit{da}\} \\
\end{array}
\end{array}\end{split}\]
The following restrictions are imposed on the composition of modules: \(m_1 \href{../syntax/conventions.html#notation-compose}{\oplus} m_2\) is defined if and only if
\(m_1.\href{../syntax/modules.html#syntax-module}{\mathsf{start}} = \epsilon \vee m_2.\href{../syntax/modules.html#syntax-module}{\mathsf{start}} = \epsilon\)
\(m_1.\href{../syntax/modules.html#syntax-module}{\mathsf{funcs}} = m_1.\href{../syntax/modules.html#syntax-module}{\mathsf{tables}} = m_1.\href{../syntax/modules.html#syntax-module}{\mathsf{mems}} = m_1.\href{../syntax/modules.html#syntax-module}{\mathsf{globals}} = \epsilon \vee m_2.\href{../syntax/modules.html#syntax-module}{\mathsf{imports}} = \epsilon\)
Note
The first condition ensures that there is at most one start function. The second condition enforces that all imports must occur before any regular definition of a function, table, memory, or global, thereby maintaining the ordering of the respective index spaces.
The well-formedness condition on \(I\) in the grammar for \(\href{../text/modules.html#text-module}{\mathtt{module}}\) ensures that no namespace contains duplicate identifiers.
The definition of the initial identifier context \(I\) uses the following auxiliary definition which maps each relevant definition to a singular context with one (possibly empty) identifier:
\[\begin{split}\begin{array}{@{}lcl@{\qquad\qquad}l}
\mathrm{idc}(\def\mathdef3655#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3655{(}~\def\mathdef3656#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3656{type}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\mathit{ft}{:}\href{../text/types.html#text-functype}{\mathtt{functype}}~\def\mathdef3657#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3657{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{types}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?), \href{../text/conventions.html#text-context}{\mathsf{typedefs}}~\mathit{ft}\} \\
\mathrm{idc}(\def\mathdef3658#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3658{(}~\def\mathdef3659#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3659{func}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3660#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3660{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{funcs}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef3661#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3661{(}~\def\mathdef3662#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3662{table}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3663#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3663{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{tables}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef3664#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3664{(}~\def\mathdef3665#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3665{memory}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3666#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3666{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{mems}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef3667#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3667{(}~\def\mathdef3668#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3668{global}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3669#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3669{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{globals}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef3670#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3670{(}~\def\mathdef3671#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3671{elem}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3672#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3672{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{elem}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef3673#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3673{(}~\def\mathdef3674#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3674{data}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3675#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3675{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{data}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef3676#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3676{(}~\def\mathdef3677#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3677{import}~\dots~\def\mathdef3678#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3678{(}~\def\mathdef3679#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3679{func}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3680#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3680{)}~\def\mathdef3681#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3681{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{funcs}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef3682#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3682{(}~\def\mathdef3683#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3683{import}~\dots~\def\mathdef3684#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3684{(}~\def\mathdef3685#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3685{table}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3686#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3686{)}~\def\mathdef3687#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3687{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{tables}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef3688#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3688{(}~\def\mathdef3689#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3689{import}~\dots~\def\mathdef3690#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3690{(}~\def\mathdef3691#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3691{memory}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3692#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3692{)}~\def\mathdef3693#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3693{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{mems}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef3694#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3694{(}~\def\mathdef3695#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3695{import}~\dots~\def\mathdef3696#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3696{(}~\def\mathdef3697#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3697{global}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3698#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3698{)}~\def\mathdef3699#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3699{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{globals}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef3700#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3700{(}~\dots~\def\mathdef3701#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3701{)}) &=&
\{\} \\
\end{array}\end{split}\]
Abbreviations¶
In a source file, the toplevel \(\mathtt{(module}~\dots\mathtt{)}\) surrounding the module body may be omitted.
\[\begin{array}{llcll}
\def\mathdef3294#1{{}}\mathdef3294{module} &
\href{../text/modules.html#text-modulefield}{\mathtt{modulefield}}^\ast &\equiv&
\def\mathdef3702#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3702{(}~\def\mathdef3703#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3703{module}~~\href{../text/modules.html#text-modulefield}{\mathtt{modulefield}}^\ast~\def\mathdef3704#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3704{)}
\end{array}\]