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}}\).

Todo

below is the official specification

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

\[\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}}\).

Todo

below is the official specification

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

\[\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}}\).

Todo

below is the official specification

• 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\).

\[\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}})\).

Todo

below is the official specification

• The value is valid with 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}}\).

Todo

below is the official specification

• 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}})\).

\[\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}}\).

Todo

below is the official specification

• 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}})\).

\[\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}}\).

Todo

below is the official specification

• 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}}\).

\[\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}}\).

Todo

below is the official specification

• 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}})\).

\[\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}})\).

Todo

below is the official specification

• The value is valid with 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}})\).

Todo

below is the official specification

• 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}})\).

\[\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}}\).

Todo

below is the official specification

• 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'\).

\[\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}}}\).

Todo

below is the official specification

• 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 \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}}}\).

Todo

below is the official specification

• 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 \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}}}\).

Todo

below is the official specification

• 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 \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}}}\).

Todo

below is the official specification

• 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 \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}}}\).

Todo

below is the official specification

• The store entry \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tags}}[a]\) must exist.

• Let \(\href{../valid/conventions.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-externtype}{\mathsf{tag}}~\href{../valid/conventions.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 \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}}\).

Todo

below is the official specification

• 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 \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}\]