Values¶

Value Typing¶

For the purpose of checking argument values against the parameter types of exported functions, values are classified by value types. The following auxiliary typing rules specify this typing relation relative to a store \(S\) in which possibly referenced addresses live.

Numeric Values \(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c\)¶

The value is valid with number type \(t\).

\[\frac{ }{ S \href{../exec/values.html#valid-val}{\vdash} t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c : t }\]

Vector Values \(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c\)¶

The value is valid with vector type \(t\).

\[\frac{ }{ S \href{../exec/values.html#valid-val}{\vdash} t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c : t }\]

Null References \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~t\)¶

The heap type must be valid under the empty context.
Then the value is valid with reference type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~t')\), where the heap type \(t'\) is the least type that matches \(t\).

\[\frac{ \href{../valid/types.html#valid-heaptype}{\vdash} t : \href{../valid/types.html#valid-heaptype}{\mathsf{ok}} \qquad t' \in \{\href{../syntax/types.html#syntax-heaptype}{\mathsf{none}}, \href{../syntax/types.html#syntax-heaptype}{\mathsf{nofunc}}, \href{../syntax/types.html#syntax-heaptype}{\mathsf{noextern}}\} \qquad \href{../valid/matching.html#match-heaptype}{\vdash} t' \href{../valid/matching.html#match-heaptype}{\leq} t }{ S \href{../exec/values.html#valid-val}{\vdash} \href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~t : (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~t') }\]

Note

A null reference is typed with the least type in its respective hierarchy. That ensures that it is compatible with any nullable type in that hierarchy.

Scalar References \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}i31}}~i\)¶

The value is valid with reference type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{i\scriptstyle31}})\).

\[\frac{ }{ S \href{../exec/values.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}i31}}~i : \href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{i\scriptstyle31}} }\]

Structure References \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}struct}}~a\)¶

The structure address \(a\) must exist in the store.
Let \(\href{../exec/runtime.html#syntax-structinst}{\mathit{structinst}}\) be the structure instance \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{structs}}[a]\).
Let \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}\) be the defined type \(\href{../exec/runtime.html#syntax-structinst}{\mathit{structinst}}.\href{../exec/runtime.html#syntax-structinst}{\mathsf{type}}\).
The expansion of \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}\) must be a struct type.
Then the value is valid with reference type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}})\).

\[\frac{ \href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}} = S.\href{../exec/runtime.html#syntax-store}{\mathsf{structs}}[a].\href{../exec/runtime.html#syntax-structinst}{\mathsf{type}} \qquad \href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}) = \href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~\href{../syntax/types.html#syntax-structtype}{\mathit{structtype}} }{ S \href{../exec/values.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}struct}}~a : \href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}} }\]

Array References \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a\)¶

The array address \(a\) must exist in the store.
Let \(\href{../exec/runtime.html#syntax-arrayinst}{\mathit{arrayinst}}\) be the array instance \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}[a]\).
Let \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}\) be the defined type \(\href{../exec/runtime.html#syntax-arrayinst}{\mathit{arrayinst}}.\href{../exec/runtime.html#syntax-arrayinst}{\mathsf{type}}\).
The expansion of \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}\) must be an array type.
Then the value is valid with reference type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-arraytype}{\mathit{arraytype}})\).

\[\frac{ \href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}} = S.\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}[a].\href{../exec/runtime.html#syntax-arrayinst}{\mathsf{type}} \qquad \href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}) = \href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~\href{../syntax/types.html#syntax-arraytype}{\mathit{arraytype}} }{ S \href{../exec/values.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a : \href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}} }\]

Exception References \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}exn}}~a\)¶

The store entry \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{exns}}[a]\) must exist.
Then the value is valid with reference type \(\href{../syntax/types.html#syntax-reftype}{\mathsf{exnref}}\).

\[\frac{ S.\href{../exec/runtime.html#syntax-store}{\mathsf{exns}}[a] = \href{../exec/runtime.html#syntax-exninst}{\mathit{exninst}} }{ S \href{../exec/values.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}exn}} : \href{../syntax/types.html#syntax-reftype}{\mathsf{exnref}} }\]

Function References \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}func}}~a\)¶

The function address \(a\) must exist in the store.
Let \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}\) be the function instance \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a]\).
Let \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}\) be the defined type \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}.\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}\).
The expansion of \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}\) must be a function type.
Then the value is valid with reference type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}})\).

\[\frac{ \href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}} = S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a].\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}} \qquad \href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}) = \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}} }{ S \href{../exec/values.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}func}}~a : \href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}} }\]

Host References \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}host}}~a\)¶

The value is valid with reference type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{any}})\).

\[\frac{ }{ S \href{../exec/values.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}host}}~a : \href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{any}} }\]

Note

A host reference is considered internalized by this rule.

External References \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}extern}}~\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}\)¶

The reference value \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}\) must be valid with some reference type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}^?~t)\).
The heap type \(t\) must match the heap type \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{any}}\).
Then the value is valid with reference type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}^?~\href{../syntax/types.html#syntax-heaptype}{\mathsf{extern}})\).

\[\frac{ S \href{../exec/values.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-ref}{\mathit{ref}} : \href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}^?~t \qquad \href{../valid/matching.html#match-heaptype}{\vdash} t \href{../valid/matching.html#match-heaptype}{\leq} \href{../syntax/types.html#syntax-heaptype}{\mathsf{any}} }{ S \href{../exec/values.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}extern}}~\href{../exec/runtime.html#syntax-ref}{\mathit{ref}} : \href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}^?~\href{../syntax/types.html#syntax-heaptype}{\mathsf{extern}} }\]

Subsumption¶

The value must be valid with some value type \(t\).
The value type \(t\) matches another valid type \(t'\).
Then the value is valid with type \(t'\).

\[\frac{ S \href{../exec/values.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-val}{\mathit{val}} : t \qquad \href{../valid/types.html#valid-valtype}{\vdash} t' : \href{../valid/types.html#valid-valtype}{\mathsf{ok}} \qquad \href{../valid/matching.html#match-valtype}{\vdash} t \href{../valid/matching.html#match-valtype}{\leq} t' }{ S \href{../exec/values.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-val}{\mathit{val}} : t' }\]

External Typing¶

For the purpose of checking external address against imports, such values are classified by external types. The following auxiliary typing rules specify this typing relation relative to a store \(S\) in which the referenced instances live.

\(\href{../exec/runtime.html#syntax-externaddr}{\mathsf{func}}~a\)¶

The store entry \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a]\) must exist.
Then \(\href{../exec/runtime.html#syntax-externaddr}{\mathsf{func}}~a\) is valid with external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a].\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}{}[a] = {\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}} }{ s \vdash \href{../exec/runtime.html#syntax-externaddr}{\mathsf{func}}~a : \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~{\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}}{.}\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}} } \qquad \end{array}\]

\(\href{../exec/runtime.html#syntax-externaddr}{\mathsf{table}}~a\)¶

The store entry \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a]\) must exist.
Then \(\href{../exec/runtime.html#syntax-externaddr}{\mathsf{table}}~a\) is valid with external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}{}[a] = {\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}} }{ s \vdash \href{../exec/runtime.html#syntax-externaddr}{\mathsf{table}}~a : \href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~{\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}}{.}\href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}} } \qquad \end{array}\]

\(\href{../exec/runtime.html#syntax-externaddr}{\mathsf{mem}}~a\)¶

The store entry \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\) must exist.
Then \(\href{../exec/runtime.html#syntax-externaddr}{\mathsf{mem}}~a\) is valid with external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a].\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}{}[a] = {\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}} }{ s \vdash \href{../exec/runtime.html#syntax-externaddr}{\mathsf{mem}}~a : \href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~{\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}}{.}\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}} } \qquad \end{array}\]

\(\href{../exec/runtime.html#syntax-externaddr}{\mathsf{global}}~a\)¶

The store entry \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[a]\) must exist.
Then \(\href{../exec/runtime.html#syntax-externaddr}{\mathsf{global}}~a\) is valid with external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[a].\href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}{}[a] = {\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}} }{ s \vdash \href{../exec/runtime.html#syntax-externaddr}{\mathsf{global}}~a : \href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~{\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}}{.}\href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}} } \qquad \end{array}\]

\(\href{../exec/runtime.html#syntax-externaddr}{\mathsf{tag}}~a\)¶

The store entry \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tags}}[a]\) must exist.
Let \(\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}\) be the function type \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tags}}[a].\href{../exec/runtime.html#syntax-taginst}{\mathsf{type}}\).
Then \(\href{../exec/runtime.html#syntax-externaddr}{\mathsf{tag}}~a\) is valid with external type \(\href{../syntax/types.html#syntax-tagtype}{\mathsf{tag}}~\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{tags}}{}[a] = {\href{../exec/runtime.html#syntax-taginst}{\mathit{taginst}}} }{ s \vdash \href{../exec/runtime.html#syntax-externaddr}{\mathsf{tag}}~a : \href{../syntax/types.html#syntax-tagtype}{\mathsf{tag}}~{\href{../exec/runtime.html#syntax-taginst}{\mathit{taginst}}}{.}\href{../exec/runtime.html#syntax-taginst}{\mathsf{type}} } \qquad \end{array}\]

Subsumption¶

The external address must be valid with some external type \(\mathit{et}\).
The external type \(\mathit{et}\) matches another valid type \(\mathit{et'}\).
Then the external address is valid with type \(\mathit{et'}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ s \vdash {\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}} : {\mathit{xt}'} \qquad \{ \begin{array}[t]{@{}l@{}} \}\end{array} \href{../valid/matching.html#match-externtype}{\vdash} {\mathit{xt}'} \href{../valid/matching.html#match-externtype}{\leq} {\mathit{xt}} }{ s \vdash {\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}} : {\mathit{xt}} } \qquad \end{array}\]