Matching

On most types, a notion of subtyping is defined that is applicable in validation rules, during module instantiation when checking the types of imports, or during execution, when performing casts.

Number Types

A number type ${\mathit{numtype}}_1$ matches a number type ${\mathit{numtype}}_2$ if and only if:

• Both ${\mathit{numtype}}_1$ and ${\mathit{numtype}}_2$ are the same.

$$\begin{array}{r}\\ \frac{}{C⊢\mathit{numtype}\le \mathit{numtype}}\end{array}$$

Vector Types

A vector type ${\mathit{vectype}}_1$ matches a vector type ${\mathit{vectype}}_2$ if and only if:

• Both ${\mathit{vectype}}_1$ and ${\mathit{vectype}}_2$ are the same.

$$\begin{array}{r}\\ \frac{}{C⊢\mathit{vectype}\le \mathit{vectype}}\end{array}$$

Heap Types

A heap type ${\mathit{heaptype}}_1$ matches a heap type ${\mathit{heaptype}}_2$ if and only if:

• Either both ${\mathit{heaptype}}_1$ and ${\mathit{heaptype}}_2$ are the same.

• Or there exists a valid heap type ${\mathit{heaptype}}^{\prime }$, such that ${\mathit{heaptype}}_1$ matches ${\mathit{heaptype}}^{\prime }$ and ${\mathit{heaptype}}^{\prime }$ matches ${\mathit{heaptype}}_2$.

• Or $heaptyp{e}_1$ is $\mathsf{eq}$ and ${\mathit{heaptype}}_2$ is $\mathsf{any}$.

• Or ${\mathit{heaptype}}_1$ is one of $\mathsf{i}\mathsf{31}$, $\mathsf{struct}$, or $\mathsf{array}$ and $heaptyp{e}_2$ is $\mathsf{eq}$.

• Or ${\mathit{heaptype}}_1$ is a defined type which expands to a structure type and ${\mathit{heaptype}}_2$ is $\mathsf{struct}$.

• Or ${\mathit{heaptype}}_1$ is a defined type which expands to an array type and ${\mathit{heaptype}}_2$ is $\mathsf{array}$.

• Or ${\mathit{heaptype}}_1$ is a defined type which expands to a function type and ${\mathit{heaptype}}_2$ is $\mathsf{func}$.

• Or ${\mathit{heaptype}}_1$ is a defined type ${\mathit{deftype}}_1$ and ${\mathit{heaptype}}_2$ is a defined type ${\mathit{deftype}}_2$, and ${\mathit{deftype}}_1$ matches ${\mathit{deftype}}_2$.

• Or ${\mathit{heaptype}}_1$ is a type index $x_1$, and the defined type $C.\mathsf{types}[x_1]$ matches ${\mathit{heaptype}}_2$.

• Or ${\mathit{heaptype}}_2$ is a type index $x_2$, and ${\mathit{heaptype}}_1$ matches the defined type $C.\mathsf{types}[x_2]$.

• Or ${\mathit{heaptype}}_1$ is $\mathsf{none}$ and ${\mathit{heaptype}}_2$ matches $\mathsf{any}$.

• Or ${\mathit{heaptype}}_1$ is $\mathsf{nofunc}$ and ${\mathit{heaptype}}_2$ matches $\mathsf{func}$.

• Or ${\mathit{heaptype}}_1$ is $\mathsf{noextern}$ and ${\mathit{heaptype}}_2$ matches $\mathsf{extern}$.

• Or ${\mathit{heaptype}}_1$ is $\mathsf{bot}$.

$$\begin{array}{r}\\ \frac{}{C⊢\mathit{heaptype}\le \mathit{heaptype}}\frac{C⊢{\mathit{heaptype}}^{\prime }\text{ok}C⊢{\mathit{heaptype}}_1\le {\mathit{heaptype}}^{\prime }C⊢{\mathit{heaptype}}^{\prime }\le {\mathit{heaptype}}_2}{C⊢{\mathit{heaptype}}_1\le {\mathit{heaptype}}_2}\end{array}$$

$$\begin{array}{r}\\ \frac{}{C⊢\mathsf{eq}\le \mathsf{any}}\frac{}{C⊢\mathsf{i}\mathsf{31}\le \mathsf{eq}}\frac{}{C⊢\mathsf{struct}\le \mathsf{eq}}\frac{}{C⊢\mathsf{array}\le \mathsf{eq}}\end{array}$$

$$\begin{array}{r}\\ \frac{\mathrm{expand}(\mathit{deftype})=\mathsf{struct}\mathit{st}}{C⊢\mathit{deftype}\le \mathsf{struct}}\frac{\mathrm{expand}(\mathit{deftype})=\mathsf{array}\mathit{at}}{C⊢\mathit{deftype}\le \mathsf{array}}\frac{\mathrm{expand}(\mathit{deftype})=\mathsf{func}\mathit{ft}}{C⊢\mathit{deftype}\le \mathsf{func}}\end{array}$$

$$\begin{array}{r}\\ \frac{C⊢C.\mathsf{types}[{\mathit{typeidx}}_1]\le {\mathit{heaptype}}_2}{C⊢{\mathit{typeidx}}_1\le {\mathit{heaptype}}_2}\frac{C⊢{\mathit{heaptype}}_1\le C.\mathsf{types}[{\mathit{typeidx}}_2]}{C⊢{\mathit{heaptype}}_1\le {\mathit{typeidx}}_2}\end{array}$$

$$\begin{array}{r}\\ \frac{C⊢\mathit{ht}\le \mathsf{any}}{C⊢\mathsf{none}\le \mathit{ht}}\frac{C⊢\mathit{ht}\le \mathsf{func}}{C⊢\mathsf{nofunc}\le \mathit{ht}}\frac{C⊢\mathit{ht}\le \mathsf{extern}}{C⊢\mathsf{noextern}\le \mathit{ht}}\end{array}$$

$$\begin{array}{r}\\ \frac{}{C⊢\mathsf{bot}\le \mathit{heaptype}}\end{array}$$

Reference Types

A reference type $\mathsf{ref}{\mathsf{null}}_1^{?}heaptyp{e}_1$ matches a reference type $\mathsf{ref}{\mathsf{null}}_2^{?}heaptyp{e}_2$ if and only if:

• The heap type ${\mathit{heaptype}}_1$ matches ${\mathit{heaptype}}_2$.

• ${\mathsf{null}}_1$ is absent or ${\mathsf{null}}_2$ is present.

$$\begin{array}{r}\\ \frac{C⊢{\mathit{heaptype}}_1\le {\mathit{heaptype}}_2}{C⊢\mathsf{ref}{\mathit{heaptype}}_1\le \mathsf{ref}{\mathit{heaptype}}_2}\frac{C⊢{\mathit{heaptype}}_1\le {\mathit{heaptype}}_2}{C⊢\mathsf{ref}{\mathsf{null}}^{?}{\mathit{heaptype}}_1\le \mathsf{ref}\mathsf{null}{\mathit{heaptype}}_2}\end{array}$$

Value Types

A value type ${\mathit{valtype}}_1$ matches a value type ${\mathit{valtype}}_2$ if and only if:

• Either both ${\mathit{valtype}}_1$ and ${\mathit{valtype}}_2$ are number types and ${\mathit{valtype}}_1$ matches ${\mathit{valtype}}_2$.

• Or both ${\mathit{valtype}}_1$ and ${\mathit{valtype}}_2$ are reference types and ${\mathit{valtype}}_1$ matches ${\mathit{valtype}}_2$.

• Or ${\mathit{valtype}}_1$ is $\mathsf{bot}$.

$$\begin{array}{r}\\ \frac{}{C⊢\mathsf{bot}\le \mathit{valtype}}\end{array}$$

Result Types

Subtyping is lifted to result types in a pointwise manner. That is, a result type $[t_1^{\ast }]$ matches a result type $[t_2^{\ast }]$ if and only if:

• Every value type $t_1$ in $[t_1^{\ast }]$ matches the corresponding value type $t_2$ in $[t_2^{\ast }]$.

$$\begin{array}{r}\\ \frac{(C⊢t_1\le t_2{)}^{\ast }}{C⊢[t_1^{\ast }]\le [t_2^{\ast }]}\end{array}$$

Instruction Types

Subtyping is further lifted to instruction types. An instruction type $[t_{11}^{\ast }]{\to }_{x_1^{\ast }}[t_{12}^{\ast }]$ matches a type $[t_{21}^{a}st]{\to }_{x_2^{\ast }}[t_{22}^{\ast }]$ if and only if:

• There is a common sequence of value types $t^{\ast }$ such that $t_{21}^{\ast }$ equals $t^{\ast }{t_{21}^{\prime }}^{\ast }$ and $t_{22}^{\ast }$ equals $t^{\ast }{t_{22}^{\prime }}^{\ast }$.

• The result type $[{t_{21}^{\prime }}^{\ast }]$ matches $[t_{11}^{\ast }]$.

• The result type $[t_{12}^{\ast }]$ matches $[{t_{22}^{\prime }}^{\ast }]$.

• For every local index $x$ that is in $x_2^{\ast }$ but not in $x_1^{\ast }$, the local type $C.\mathsf{locals}[x]$ is $\mathsf{set}{t}_x$ for some value type $t_x$.

$$\begin{array}{r}\\ \frac{\begin{array}{cl}C⊢[t_{21}^{\ast }]\le [t_{11}^{\ast }]& \{x^{\ast }\}=\{x_2^{\ast }\}\setminus \{x_1^{\ast }\}\\ C⊢[t_{12}^{\ast }]\le [t_{22}^{\ast }]& (C.\mathsf{locals}[x]=\mathsf{set}{t}_x{)}^{\ast }\end{array}}{C⊢[t_{11}^{\ast }]{\to }_{x_1^{\ast }}[t_{12}^{\ast }]\le [t^{\ast }{t}_{21}^{\ast }]{\to }_{x_2^{\ast }}[t^{\ast }{t}_{22}^{\ast }]}\end{array}$$

Note

Instruction types are contravariant in their input and covariant in their output. Subtyping also incorporates a sort of “frame” condition, which allows adding arbitrary invariant stack elements on both sides in the super type.

Finally, the supertype may ignore variables from the init set $x_1^{\ast }$. It may also add variables to the init set, provided these are already set in the context, i.e., are vacuously initialized.

Function Types

A function type $[t_{11}^{\ast }]\to [t_{12}^{\ast }]$ matches a type $[t_{21}^{a}st]\to [t_{22}^{\ast }]$ if and only if:

• The result type $[t_{21}^{\ast }]$ matches $[t_{11}^{\ast }]$.

• The result type $[t_{12}^{\ast }]$ matches $[t_{22}^{\ast }]$.

$$\begin{array}{r}\\ \frac{C⊢[t_{21}^{\ast }]\le [t_{11}^{\ast }]C⊢[t_{12}^{\ast }]\le [t_{22}^{\ast }]}{C⊢[t_{11}^{\ast }]\to [t_{12}^{\ast }]\le [t_{21}^{\ast }]\to [t_{22}^{\ast }]}\end{array}$$

Composite Types

A composite type ${\mathit{comptype}}_1$ matches a type ${\mathit{comptype}}_2$ if and only if:

• Either the composite type ${\mathit{comptype}}_1$ is $\mathsf{func}{\mathit{functype}}_1$ and ${\mathit{comptype}}_2$ is $\mathsf{func}{\mathit{functype}}_2$ and:

  • The function type ${\mathit{functype}}_1$ matches ${\mathit{functype}}_2$.

• Or the composite type ${\mathit{comptype}}_1$ is $\mathsf{struct}{\mathit{fieldtype}}_1^{n_1}$ and ${\mathit{comptype}}_2$ is $\mathsf{struct}{\mathit{fieldtype}}_2$ and:

  • The arity $n_1$ is greater than or equal to $n_2$.

  • For every field type ${\mathit{fieldtype}}_{2i}$ in ${\mathit{fieldtype}}_2^{n_2}$ and corresponding ${\mathit{fieldtype}}_{1i}$ in ${\mathit{fieldtype}}_1^{n_1}$

    • The field type ${\mathit{fieldtype}}_{1i}$ matches ${\mathit{fieldtype}}_{2i}$.

• Or the composite type ${\mathit{comptype}}_1$ is $\mathsf{array}{\mathit{fieldtype}}_1$ and ${\mathit{comptype}}_2$ is $\mathsf{array}{\mathit{fieldtype}}_2$ and:

  • The field type ${\mathit{fieldtype}}_1$ matches ${\mathit{fieldtype}}_2$.

$$\begin{array}{r}\\ \frac{C⊢{\mathit{functype}}_1\le {\mathit{functype}}_2}{C⊢\mathsf{func}{\mathit{functype}}_1\le \mathsf{func}{\mathit{functype}}_2}\end{array}$$

$$\begin{array}{r}\\ \frac{(C⊢{\mathit{fieldtype}}_1\le {\mathit{fieldtype}}_2{)}^{\ast }}{C⊢\mathsf{struct}{\mathit{fieldtype}}_1^{\ast }{{\mathit{fieldtype}}^{\prime }}_1^{\ast }\le \mathsf{struct}{\mathit{fieldtype}}_2^{\ast }}\end{array}$$

$$\begin{array}{r}\\ \frac{C⊢{\mathit{fieldtype}}_1\le {\mathit{fieldtype}}_2}{C⊢\mathsf{array}{\mathit{fieldtype}}_1\le \mathsf{array}{\mathit{fieldtype}}_2}\end{array}$$

Field Types

A field type ${\mathit{mut}}_1{\mathit{storagetype}}_1$ matches a type ${\mathit{mut}}_2{\mathit{storagetype}}_2$ if and only if:

• Storage type ${\mathit{storagetype}}_1$ matches ${\mathit{storagetype}}_2$.

• Either both ${\mathit{mut}}_1$ and ${\mathit{mut}}_2$ are $\mathsf{const}$.

• Or both ${\mathit{mut}}_1$ and ${\mathit{mut}}_2$ are $\mathsf{var}$ and ${\mathit{storagetype}}_2$ matches ${\mathit{storagetype}}_1$ as well.

$$\begin{array}{r}\\ \frac{C⊢{\mathit{storagetype}}_1\le {\mathit{storagetype}}_2}{C⊢\mathsf{const}{\mathit{storagetype}}_1\le \mathsf{const}{\mathit{storagetype}}_2}\frac{\begin{array}{c}C⊢{\mathit{storagetype}}_1\le {\mathit{storagetype}}_2\\ C⊢{\mathit{storagetype}}_2\le {\mathit{storagetype}}_1\end{array}}{C⊢\mathsf{var}{\mathit{storagetype}}_1\le \mathsf{var}{\mathit{storagetype}}_2}\end{array}$$

A storage type ${\mathit{storagetype}}_1$ matches a type ${\mathit{storagetype}}_2$ if and only if:

• Either ${\mathit{storagetype}}_1$ is a value type ${\mathit{valtype}}_1$ and ${\mathit{storagetype}}_2$ is a value type ${\mathit{valtype}}_2$ and ${\mathit{valtype}}_1$ matches ${\mathit{valtype}}_2$.

• Or ${\mathit{storagetype}}_1$ is a packed type ${\mathit{packedtype}}_1$ and ${\mathit{storagetype}}_2$ is a packed type ${\mathit{packedtype}}_2$ and ${\mathit{packedtype}}_1$ matches ${\mathit{packedtype}}_2$.

A packed type ${\mathit{packedtype}}_1$ matches a type ${\mathit{packedtype}}_2$ if and only if:

• The packed type ${\mathit{packedtype}}_1$ is the same as ${\mathit{packedtype}}_2$.

$$\begin{array}{r}\\ \frac{}{C⊢\mathit{packedtype}\le \mathit{packedtype}}\end{array}$$

Defined Types

A defined type ${\mathit{deftype}}_1$ matches a type ${\mathit{deftype}}_2$ if and only if:

• Either ${\mathit{deftype}}_1$ and ${\mathit{deftype}}_2$ are equal when closed under context $C$.

• Or:

  • Let the sub type $\mathsf{sub}{\mathsf{final}}^{?}{\mathit{heaptype}}^{\ast }\mathit{comptype}$ be the result of unrolling ${\mathit{deftype}}_1$.

  • Then there must exist a heap type ${\mathit{heaptype}}_i$ in ${\mathit{heaptype}}^{\ast }$ that matches ${\mathit{deftype}}_2$.

$$\begin{array}{r}\\ \frac{{\mathsf{clos}}_C({\mathit{deftype}}_1)={\mathsf{clos}}_C({\mathit{deftype}}_2)}{C⊢{\mathit{deftype}}_1\le {\mathit{deftype}}_2}\end{array}$$

$$\begin{array}{r}\\ \frac{\mathrm{unroll}({\mathit{deftype}}_1)=\mathsf{sub}{\mathsf{final}}^{?}{\mathit{heaptype}}^{\ast }\mathit{comptype}C⊢{\mathit{heaptype}}^{\ast }[i]\le {\mathit{deftype}}_2}{C⊢{\mathit{deftype}}_1\le {\mathit{deftype}}_2}\end{array}$$

Note

Note that there is no explicit definition of type _equivalence_, since it coincides with syntactic equality, as used in the premise of the former rule above.

Limits

Limits $\{\mathsf{min}{n}_1,\mathsf{max}{m}_1^{?}\}$ match limits $\{\mathsf{min}{n}_2,\mathsf{max}{m}_2^{?}\}$ if and only if:

• $n_1$ is larger than or equal to $n_2$.

• Either:

  • $m_2^{?}$ is empty.

• Or:

  • Both $m_1^{?}$ and $m_2^{?}$ are non-empty.

  • $m_1$ is smaller than or equal to $m_2$.

$$\begin{array}{r}\\ \frac{n_1\ge n_2}{C⊢\{\mathsf{min}{n}_1,\mathsf{max}{m}_1^{?}\}\le \{\mathsf{min}{n}_2,\mathsf{max}ϵ\}}\frac{n_1\ge n_2{m}_1\le m_2}{C⊢\{\mathsf{min}{n}_1,\mathsf{max}{m}_1\}\le \{\mathsf{min}{n}_2,\mathsf{max}{m}_2\}}\end{array}$$

Table Types

A table type $({\mathit{limits}}_1{\mathit{reftype}}_1)$ matches $({\mathit{limits}}_2{\mathit{reftype}}_2)$ if and only if:

• Limits ${\mathit{limits}}_1$ match ${\mathit{limits}}_2$.

• The reference type ${\mathit{reftype}}_1$ matches ${\mathit{reftype}}_2$, and vice versa.

$$\begin{array}{r}\\ \frac{C⊢{\mathit{limits}}_1\le {\mathit{limits}}_{2}C⊢{\mathit{reftype}}_1\le {\mathit{reftype}}_{2}C⊢{\mathit{reftype}}_2\le {\mathit{reftype}}_1}{C⊢{\mathit{limits}}_1{\mathit{reftype}}_1\le {\mathit{limits}}_2{\mathit{reftype}}_2}\end{array}$$

Memory Types

A memory type ${\mathit{limits}}_1$ matches ${\mathit{limits}}_2$ if and only if:

• Limits ${\mathit{limits}}_1$ match ${\mathit{limits}}_2$.

$$\begin{array}{r}\\ \frac{C⊢{\mathit{limits}}_1\le {\mathit{limits}}_2}{C⊢{\mathit{limits}}_1\le {\mathit{limits}}_2}\end{array}$$

Global Types

A global type $({\mathit{mut}}_1{t}_1)$ matches $({\mathit{mut}}_2{t}_2)$ if and only if:

• Either both ${\mathit{mut}}_1$ and ${\mathit{mut}}_2$ are $\mathsf{var}$ and $t_1$ matches $t_2$ and vice versa.

• Or both ${\mathit{mut}}_1$ and ${\mathit{mut}}_2$ are $\mathsf{const}$ and $t_1$ matches $t_2$.

$$\begin{array}{r}\\ \frac{C⊢t_1\le t_{2}C⊢t_2\le t_1}{C⊢\mathsf{var}{t}_1\le \mathsf{var}{t}_2}\frac{C⊢t_1\le t_2}{C⊢\mathsf{const}{t}_1\le \mathsf{const}{t}_2}\end{array}$$

Tag Types

A tag type ${\mathit{tagtype}}_1$ matches ${\mathit{tagtype}}_2$ if and only if they are the same.

$$\frac{}{C⊢\mathit{tagtype}\le \mathit{tagtype}}$$

External Types

Functions

An external type $\mathsf{func}{\mathit{deftype}}_1$ matches $\mathsf{func}{\mathit{deftype}}_2$ if and only if:

• The defined type ${\mathit{deftype}}_1$ matches ${\mathit{deftype}}_2$.

$$\begin{array}{r}\\ \frac{C⊢{\mathit{deftype}}_1\le {\mathit{deftype}}_2}{C⊢\mathsf{func}{\mathit{deftype}}_1\le \mathsf{func}{\mathit{deftype}}_2}\end{array}$$

Tables

An external type $\mathsf{table}{\mathit{tabletype}}_1$ matches $\mathsf{table}{\mathit{tabletype}}_2$ if and only if:

• Table type ${\mathit{tabletype}}_1$ matches ${\mathit{tabletype}}_2$.

$$\begin{array}{r}\\ \frac{C⊢{\mathit{tabletype}}_1\le {\mathit{tabletype}}_2}{C⊢\mathsf{table}{\mathit{tabletype}}_1\le \mathsf{table}{\mathit{tabletype}}_2}\end{array}$$

Memories

An external type $\mathsf{mem}{\mathit{memtype}}_1$ matches $\mathsf{mem}{\mathit{memtype}}_2$ if and only if:

• Memory type ${\mathit{memtype}}_1$ matches ${\mathit{memtype}}_2$.

$$\begin{array}{r}\\ \frac{C⊢{\mathit{memtype}}_1\le {\mathit{memtype}}_2}{C⊢\mathsf{mem}{\mathit{memtype}}_1\le \mathsf{mem}{\mathit{memtype}}_2}\end{array}$$

Globals

An external type $\mathsf{global}{\mathit{globaltype}}_1$ matches $\mathsf{global}{\mathit{globaltype}}_2$ if and only if:

• Global type ${\mathit{globaltype}}_1$ matches ${\mathit{globaltype}}_2$.

$$\begin{array}{r}\\ \frac{C⊢{\mathit{globaltype}}_1\le {\mathit{globaltype}}_2}{C⊢\mathsf{global}{\mathit{globaltype}}_1\le \mathsf{global}{\mathit{globaltype}}_2}\end{array}$$

Tags

An external type $\mathsf{tag}{\mathit{tagtype}}_1$ matches $\mathsf{tag}{\mathit{tagtype}}_2$ if and only if:

• Tag type ${\mathit{tagtype}}_1$ matches ${\mathit{tagtype}}_2$.

$$\frac{C⊢{\mathit{tagtype}}_1\le {\mathit{tagtype}}_2}{C⊢\mathsf{tag}{\mathit{tagtype}}_1\le \mathsf{tag}{\mathit{tagtype}}_2}$$