Conventions

As in Core WebAssembly, a validation stage checks that a component is well-formed, and only valid components may be instantiated.

Similarly to Core WebAssembly, a type system over the abstract syntax of a component is used to specify which modules are valid, and the rules governing the validity of a component are given in both prose and formal mathematical notation.

Contexts

Validation rules for individual definitions are interpreted within a particular context, which contains the information about the surrounding component and environment needed to validae a particular definition. The validation contexts used in the component model contain the types of every definition in every index space currently accessible (including the index spaces of parent components, which may be accessed via \(\href{../syntax/components.html#syntax-aliastarget}{\mathsf{outer}}\) aliases).

Concretely, a validation context is defined as a record with the following abstract syntax:

\[\begin{split}\begin{array}{llcl} \def\mathdef4964#1{{}}\mathdef4964{(coretyctx)} & \href{../valid/conventions.html#syntax-coretyctx}{\Gamma_c} &::=& \{ \begin{array}[t]{l@{~}ll} \href{../valid/conventions.html#syntax-coretyctx}{\mathsf{types}} & \href{../valid/types.html#syntax-ecoredeftype}{\mathit{core{:}deftype}_e}^\ast, \\ \href{../valid/conventions.html#syntax-coretyctx}{\mathsf{funcs}} & \href{https://webassembly.github.io/spec/core/syntax/types.html#syntax-functype}{\mathit{core{:}}\mathit{functype}}^\ast, \\ \href{../valid/conventions.html#syntax-coretyctx}{\mathsf{modules}} & \href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}^\ast, \\ \href{../valid/conventions.html#syntax-coretyctx}{\mathsf{instances}} & \href{../valid/types.html#syntax-ecoreinstancetype}{\mathit{core{:}instancetype}_e}^\ast, \\ \href{../valid/conventions.html#syntax-coretyctx}{\mathsf{tables}} & \href{https://webassembly.github.io/spec/core/syntax/types.html#syntax-tabletype}{\mathit{core{:}}\mathit{tabletype}}^\ast, \\ \href{../valid/conventions.html#syntax-coretyctx}{\mathsf{mems}} & \href{https://webassembly.github.io/spec/core/syntax/types.html#syntax-memtype}{\mathit{core{:}}\mathit{memtype}}^\ast, \\ \href{../valid/conventions.html#syntax-coretyctx}{\mathsf{globals}} & \href{https://webassembly.github.io/spec/core/syntax/types.html#syntax-globaltype}{\mathit{core{:}}\mathit{globaltype}}^\ast\} \\ \end{array}\\ \def\mathdef4964#1{{}}\mathdef4964{(tyctx)} & \href{../valid/conventions.html#syntax-tyctx}{\Gamma} &::=& \{ \begin{array}[t]{l@{~}ll} \href{../valid/conventions.html#syntax-tyctx}{\mathsf{parent}} & \href{../valid/conventions.html#syntax-tyctx}{\Gamma}, \\ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}} & \href{../valid/conventions.html#syntax-coretyctx}{\Gamma_c}, \\ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{uvars}} & \href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast, \\ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{evars}} & (\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}, \href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e})^\ast \\ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{rtypes}} & \href{../valid/types.html#syntax-eresourcetype}{\mathit{resourcetype}_e}^\ast, \\ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}} & \href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}^\ast, \\ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{components}} & \href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}^\ast, \\ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}} & {\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}^\dagger}^\ast, \\ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{funcs}} & \href{../valid/types.html#syntax-efunctype}{\mathit{functype}_e}^\ast, \\ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{values}} & \href{../valid/types.html#syntax-evaltypead}{{\mathit{valtype}_e^?}}^\ast, \} \\ \end{array}\\ \end{array}\end{split}\]

Notation

Both the formal and prose notation share a number of constructs:

• When writing a value of the abstract syntax, any component of the abstract syntax which has the form \(\mathit{nonterminal}^n\), \(\mathit{nonterminal}^\ast\), \(\mathit{nonterminal}^{+}\), or \(\mathit{nonterminal}^{?}\), we may write \(\overline{\dots_i}^n\) to mean that this position is filled by a series of \(n\) abstract values, named \(\dots_1\) to \(\dots_n\).