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

The number value \(({\mathit{nt}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c)\) is valid with the number type \({\mathit{nt}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ s \href{../exec/values.html#valid-num}{\vdash} {\mathit{nt}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c : {\mathit{nt}} } \qquad \end{array}\]

Vector Values

The vector value \(({\mathit{vt}}{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c)\) is valid with the vector type \({\mathit{vt}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ s \href{../exec/values.html#valid-vec}{\vdash} {\mathit{vt}}{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c : {\mathit{vt}} } \qquad \end{array}\]

Null References

The reference value \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}null}}\) is valid with the reference type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../valid/conventions.html#syntax-valtype-ext}{\mathsf{bot}})\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ s \href{../exec/values.html#valid-ref}{\vdash} \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}null}} : (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../valid/conventions.html#syntax-valtype-ext}{\mathsf{bot}}) } \qquad \end{array}\]

Scalar References

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

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ s \href{../exec/values.html#valid-ref}{\vdash} \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}i\scriptstyle31}}~i : (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{i\scriptstyle31}}) } \qquad \end{array}\]

Structure References

The reference value \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}struct}}~a)\) is valid with the reference type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\mathit{dt}})\) if:

• The structure instance \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{structs}}{}[a]\) exists.

• The defined type \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{structs}}{}[a]{.}\href{../exec/runtime.html#syntax-structinst}{\mathsf{type}}\) is of the form \({\mathit{dt}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{structs}}{}[a]{.}\href{../exec/runtime.html#syntax-structinst}{\mathsf{type}} = {\mathit{dt}} }{ s \href{../exec/values.html#valid-ref}{\vdash} \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}struct}}~a : (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\mathit{dt}}) } \qquad \end{array}\]

Array References

The reference value \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a)\) is valid with the reference type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\mathit{dt}})\) if:

• The array instance \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}{}[a]\) exists.

• The defined type \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}{}[a]{.}\href{../exec/runtime.html#syntax-arrayinst}{\mathsf{type}}\) is of the form \({\mathit{dt}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}{}[a]{.}\href{../exec/runtime.html#syntax-arrayinst}{\mathsf{type}} = {\mathit{dt}} }{ s \href{../exec/values.html#valid-ref}{\vdash} \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a : (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\mathit{dt}}) } \qquad \end{array}\]

Exception References

The reference value \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}exn}}~a)\) is valid with the reference type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{exn}})\) if:

• The exception instance \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{exns}}{}[a]\) exists.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{exns}}{}[a] = {\mathit{exn}} }{ s \href{../exec/values.html#valid-ref}{\vdash} \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}exn}}~a : (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{exn}}) } \qquad \end{array}\]

Function References

The reference value \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}func}}~a)\) is valid with the reference type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\mathit{dt}})\) if:

• The function instance \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}{}[a]\) exists.

• The defined type \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}{}[a]{.}\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}\) is of the form \({\mathit{dt}}\).

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

Host References

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

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ s \href{../exec/values.html#valid-ref}{\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}}) } \qquad \end{array}\]

Note

A bare host reference is considered internalized.

External References

The reference value \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}extern}}~{\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}})\) is valid with the reference type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{extern}})\) if:

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

• The reference value \({\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}\) is not of the form \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}null}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ s \href{../exec/values.html#valid-ref}{\vdash} {\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}} : (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{any}}) \qquad {\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}} \neq \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}null}} }{ s \href{../exec/values.html#valid-ref}{\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-heaptype}{\mathsf{extern}}) } \qquad \end{array}\]

Subsumption

The reference value \({\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}\) is valid with the reference type \({\mathit{rt}}\) if:

• The reference value \({\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}\) is valid with the reference type \({\mathit{rt}'}\).

• The reference type \({\mathit{rt}'}\) matches the reference type \({\mathit{rt}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ s \href{../exec/values.html#valid-ref}{\vdash} {\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}} : {\mathit{rt}'} \qquad \{ \} \href{../valid/matching.html#match-reftype}{\vdash} {\mathit{rt}'} \href{../valid/matching.html#match-reftype}{\leq} {\mathit{rt}} }{ s \href{../exec/values.html#valid-ref}{\vdash} {\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}} : {\mathit{rt}} } \qquad \end{array}\]

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.

Functions

The external address \((\href{../exec/runtime.html#syntax-externaddr}{\mathsf{func}}~a)\) is valid with the external type \((\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~{\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}}{.}\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}})\) if:

• The function instance \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}{}[a]\) exists.

• The function instance \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}{}[a]\) is of the form \({\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}{}[a] = {\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}} }{ s \href{../exec/values.html#valid-externaddr}{\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}\]

Tables

The external address \((\href{../exec/runtime.html#syntax-externaddr}{\mathsf{table}}~a)\) is valid with the external type \((\href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~{\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}}{.}\href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}})\) if:

• The table instance \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}{}[a]\) exists.

• The table instance \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}{}[a]\) is of the form \({\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}{}[a] = {\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}} }{ s \href{../exec/values.html#valid-externaddr}{\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}\]

Memories

The external address \((\href{../exec/runtime.html#syntax-externaddr}{\mathsf{mem}}~a)\) is valid with the external type \((\href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~{\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}}{.}\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}})\) if:

• The memory instance \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}{}[a]\) exists.

• The memory instance \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}{}[a]\) is of the form \({\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}{}[a] = {\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}} }{ s \href{../exec/values.html#valid-externaddr}{\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}\]

Globals

The external address \((\href{../exec/runtime.html#syntax-externaddr}{\mathsf{global}}~a)\) is valid with the external type \((\href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~{\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}}{.}\href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}})\) if:

• The global instance \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}{}[a]\) exists.

• The global instance \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}{}[a]\) is of the form \({\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}{}[a] = {\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}} }{ s \href{../exec/values.html#valid-externaddr}{\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}\]

Tags

The external address \((\href{../exec/runtime.html#syntax-externaddr}{\mathsf{tag}}~a)\) is valid with the external type \((\href{../syntax/types.html#syntax-externtype}{\mathsf{tag}}~{\href{../exec/runtime.html#syntax-taginst}{\mathit{taginst}}}{.}\href{../exec/runtime.html#syntax-taginst}{\mathsf{type}})\) if:

• The tag instance \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{tags}}{}[a]\) exists.

• The tag instance \(s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{tags}}{}[a]\) is of the form \({\href{../exec/runtime.html#syntax-taginst}{\mathit{taginst}}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{tags}}{}[a] = {\href{../exec/runtime.html#syntax-taginst}{\mathit{taginst}}} }{ s \href{../exec/values.html#valid-externaddr}{\vdash} \href{../exec/runtime.html#syntax-externaddr}{\mathsf{tag}}~a : \href{../syntax/types.html#syntax-externtype}{\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 \({\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}\) is valid with the external type \({\mathit{xt}}\) if:

• The external address \({\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}\) is valid with the external type \({\mathit{xt}'}\).

• The external type \({\mathit{xt}'}\) matches the external type \({\mathit{xt}}\).

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