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{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~{\mathit{ht}})\) is valid with the reference type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~{\mathit{ht}'})\) if:

• The heap type \({\mathit{ht}'}\) matches the heap type \({\mathit{ht}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ \{ \begin{array}[t]{@{}l@{}} \}\end{array} \href{../valid/matching.html#match-heaptype}{\vdash} {\mathit{ht}'} \href{../valid/matching.html#match-heaptype}{\leq} {\mathit{ht}} }{ s \href{../exec/values.html#valid-ref}{\vdash} \href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~{\mathit{ht}} : (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~{\mathit{ht}'}) } \qquad \end{array}\]

Note

A null reference can be typed with any smaller type. In particular, that allows it to be typed with the least type in its respective hierarchy. That ensures that the value is compatible with any nullable type in that hierarchy.

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.

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

\[\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-addrref}{\mathit{addrref}}})\) is valid with the reference type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{extern}})\) if:

• Under the context \(s\), the reference value \({\href{../exec/runtime.html#syntax-addrref}{\mathit{addrref}}}\) 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-addrref}{\mathit{addrref}}} : (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{any}}) }{ s \href{../exec/values.html#valid-ref}{\vdash} \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}extern}}~{\href{../exec/runtime.html#syntax-addrref}{\mathit{addrref}}} : (\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:

• Under the context \(s\), 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 \{ \begin{array}[t]{@{}l@{}} \}\end{array} \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:

• Under the context \(s\), 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 \{ \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 \href{../exec/values.html#valid-externaddr}{\vdash} {\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}} : {\mathit{xt}} } \qquad \end{array}\]