Types¶

Simple types, such as number types are universally valid. However, restrictions apply to most other types, such as reference types, function types, as well as the limits of table types and memory types, which must be checked during validation.

Moreover, block types are converted to plain function types for ease of processing.

Number Types¶

Number types are always valid.

\[\frac{ }{ C \href{../valid/types.html#valid-numtype}{\vdash} \href{../syntax/types.html#syntax-numtype}{\mathit{numtype}} \mathrel{\mbox{ok}} }\]

Vector Types¶

Vector types are always valid.

\[\frac{ }{ C \href{../valid/types.html#valid-vectype}{\vdash} \href{../syntax/types.html#syntax-vectype}{\mathit{vectype}} \mathrel{\mbox{ok}} }\]

Heap Types¶

Concrete Heap types are only valid when the type index is.

\(\href{../syntax/types.html#syntax-heaptype}{\mathsf{func}}\)¶

The heap type is valid.

\[\frac{ }{ C \href{../valid/types.html#valid-heaptype}{\vdash} \href{../syntax/types.html#syntax-heaptype}{\mathsf{func}} \mathrel{\mbox{ok}} }\]

\(\href{../syntax/types.html#syntax-heaptype}{\mathsf{extern}}\)¶

The heap type is valid.

\[\frac{ }{ C \href{../valid/types.html#valid-heaptype}{\vdash} \href{../syntax/types.html#syntax-heaptype}{\mathsf{extern}} \mathrel{\mbox{ok}} }\]

\(\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}\)¶

The type \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}]\) must be defined in the context.
Then the heap type is valid.

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{types}}[\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}] = \href{../syntax/types.html#syntax-deftype}{\mathit{deftype}} }{ C \href{../valid/types.html#valid-heaptype}{\vdash} \href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}} \mathrel{\mbox{ok}} }\]

\(\href{../syntax/types.html#syntax-valtype}{\mathsf{bot}}\)¶

The heap type is valid.

\[\frac{ }{ C \href{../valid/types.html#valid-heaptype}{\vdash} \href{../syntax/types.html#syntax-valtype}{\mathsf{bot}} \mathrel{\mbox{ok}} }\]

Reference Types¶

Reference types are valid when the referenced heap type is.

\(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}^?~\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}\)¶

The heap type \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}\) must be valid.
Then the reference type is valid.

\[\frac{ C \href{../valid/types.html#valid-reftype}{\vdash} \href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}} \mathrel{\mbox{ok}} }{ C \href{../valid/types.html#valid-reftype}{\vdash} \href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}^?~\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}} \mathrel{\mbox{ok}} }\]

Value Types¶

Valid value types are either valid number type, reference type, or the bottom type.

\(\href{../syntax/types.html#syntax-valtype}{\mathsf{bot}}\)¶

The value type is valid.

\[\frac{ }{ C \href{../valid/types.html#valid-valtype}{\vdash} \href{../syntax/types.html#syntax-valtype}{\mathsf{bot}} \mathrel{\mbox{ok}} }\]

Block Types¶

Block types may be expressed in one of two forms, both of which are converted to instruction types by the following rules.

\(\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}\)¶

The type \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}]\) must be defined in the context.
Let \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\) be the function type \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}]\).
Then the block type is valid as instruction type \([t_1^\ast] \href{../syntax/types.html#syntax-instrtype}{\rightarrow} [t_2^\ast]\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{types}}[\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}] = [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] }{ C \href{../valid/types.html#valid-blocktype}{\vdash} \href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}} : [t_1^\ast] \href{../syntax/types.html#syntax-instrtype}{\rightarrow} [t_2^\ast] }\]

\([\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}^?]\)¶

The value type \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}\) must either be absent, or valid.
Then the block type is valid as instruction type \([] \href{../syntax/types.html#syntax-instrtype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}^?]\).

\[\frac{ (C \href{../valid/types.html#valid-valtype}{\vdash} \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}} \mathrel{\mbox{ok}})^? }{ C \href{../valid/types.html#valid-blocktype}{\vdash} [\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}^?] : [] \href{../syntax/types.html#syntax-instrtype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}^?] }\]

Result Types¶

\([t^\ast]\)¶

Each value type \(t_i\) in the type sequence \(t^\ast\) must be valid.
Then the result type is valid.

\[\frac{ (C \href{../valid/types.html#valid-valtype}{\vdash} t \mathrel{\mbox{ok}})^\ast }{ C \href{../valid/types.html#valid-resulttype}{\vdash} [t^\ast] \mathrel{\mbox{ok}} }\]

Instruction Types¶

\([t_1^\ast] \rightarrow_{x^\ast} [t_2^\ast]\)¶

The result type \([t_1^\ast]\) must be valid.
The result type \([t_2^\ast]\) must be valid.
Each local index \(x_i\) in \(x^\ast\) must be defined in the context.
Then the instruction type is valid.

\[\frac{ C \href{../valid/types.html#valid-valtype}{\vdash} [t_1^\ast] \mathrel{\mbox{ok}} \qquad C \href{../valid/types.html#valid-valtype}{\vdash} [t_2^\ast] \mathrel{\mbox{ok}} \qquad (C.\href{../valid/conventions.html#context}{\mathsf{locals}}[x] = \href{../syntax/types.html#syntax-localtype}{\mathit{localtype}})^\ast }{ C \href{../valid/types.html#valid-functype}{\vdash} [t_1^\ast] \def\mathdef4406#1{\rightarrow_{#1}}\mathdef4406{x^\ast} [t_2^\ast] \mathrel{\mbox{ok}} }\]

Function Types¶

\([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\)¶

The result type \([t_1^\ast]\) must be valid.
The result type \([t_2^\ast]\) must be valid.
Then the function type is valid.

\[\frac{ C \href{../valid/types.html#valid-valtype}{\vdash} [t_1^\ast] \mathrel{\mbox{ok}} \qquad C \href{../valid/types.html#valid-valtype}{\vdash} [t_2^\ast] \mathrel{\mbox{ok}} }{ C \href{../valid/types.html#valid-functype}{\vdash} [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] \mathrel{\mbox{ok}} }\]

Limits¶

Limits must have meaningful bounds that are within a given range.

\(\{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^? \}\)¶

The value of \(n\) must not be larger than \(k\).
If the maximum \(m^?\) is not empty, then:
- Its value must not be larger than \(k\).
- Its value must not be smaller than \(n\).
Then the limit is valid within range \(k\).

\[\frac{ n \leq k \qquad (m \leq k)^? \qquad (n \leq m)^? }{ C \href{../valid/types.html#valid-limits}{\vdash} \{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^? \} : k }\]

Table Types¶

\(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}\)¶

The limits \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\) must be valid within range \(2^{32}-1\).
The reference type \(\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}\) must be valid.
Then the table type is valid.

\[\frac{ C \href{../valid/types.html#valid-limits}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}} : 2^{32} - 1 \qquad C \href{../valid/types.html#valid-reftype}{\vdash} \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}} \mathrel{\mbox{ok}} }{ C \href{../valid/types.html#valid-tabletype}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}~\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}} \mathrel{\mbox{ok}} }\]

Memory Types¶

\(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\)¶

The limits \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\) must be valid within range \(2^{16}\).
Then the memory type is valid.

\[\frac{ C \href{../valid/types.html#valid-limits}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}} : 2^{16} }{ C \href{../valid/types.html#valid-memtype}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}} \mathrel{\mbox{ok}} }\]

Global Types¶

\(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}\)¶

The value type \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}\) must be valid.
Then the global type is valid.

\[\frac{ C \href{../valid/types.html#valid-reftype}{\vdash} \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}} \mathrel{\mbox{ok}} }{ C \href{../valid/types.html#valid-globaltype}{\vdash} \href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}} \mathrel{\mbox{ok}} }\]

External Types¶

\(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}\)¶

The function type \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\) must be defined in the context.
Then the external type is valid.

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{types}}[x] = \href{../syntax/types.html#syntax-functype}{\mathit{functype}} }{ C \href{../valid/types.html#valid-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~x }\]

\(\href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\)¶

The table type \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\) must be valid.
Then the external type is valid.

\[\frac{ C \href{../valid/types.html#valid-tabletype}{\vdash} \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}} \mathrel{\mbox{ok}} }{ C \href{../valid/types.html#valid-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}} \mathrel{\mbox{ok}} }\]

\(\href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\)¶

The memory type \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\) must be valid.
Then the external type is valid.

\[\frac{ C \href{../valid/types.html#valid-memtype}{\vdash} \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} \mathrel{\mbox{ok}} }{ C \href{../valid/types.html#valid-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} \mathrel{\mbox{ok}} }\]

\(\href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\)¶

The global type \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\) must be valid.
Then the external type is valid.

\[\frac{ C \href{../valid/types.html#valid-globaltype}{\vdash} \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}} \mathrel{\mbox{ok}} }{ C \href{../valid/types.html#valid-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}} \mathrel{\mbox{ok}} }\]

Defaultable Types¶

A type is defaultable if it has a default value for initialization.

Value Types¶

A defaultable value type \(t\) must be:
- either a number type,
- or a vector type,
- or a nullable reference type.

\[\frac{ }{ C \href{../valid/types.html#valid-defaultable}{\vdash} \href{../syntax/types.html#syntax-numtype}{\mathit{numtype}} \href{../valid/types.html#valid-defaultable}{\mathrel{\mbox{defaultable}}} }\]

\[\frac{ }{ C \href{../valid/types.html#valid-defaultable}{\vdash} \href{../syntax/types.html#syntax-vectype}{\mathit{vectype}} \href{../valid/types.html#valid-defaultable}{\mathrel{\mbox{defaultable}}} }\]

\[\frac{ }{ C \href{../valid/types.html#valid-defaultable}{\vdash} (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}) \href{../valid/types.html#valid-defaultable}{\mathrel{\mbox{defaultable}}} }\]