GeezerVisonThe World Wide Web, restored to 800 pixels of glory. |
| Home|About|Gaming cabinet|Archives|How it works|Starter sites |
GeezerVison is showing webassembly.github.io — Type Soundness — WebAssembly 3.0 (2026-11-04) Type Soundness¶The type system of WebAssembly is sound, implying both type safety and memory safety with respect to the WebAssembly semantics. For example:
Soundness also is instrumental in ensuring additional properties, most notably, encapsulation of function and module scopes: no locals can be accessed outside their own function and no module components can be accessed outside their own module unless they are explicitly exported or imported. The typing rules defining WebAssembly validation only cover the static components of a WebAssembly program. In order to state and prove soundness precisely, the typing rules must be extended to the dynamic components of the abstract runtime, that is, the store, configurations, and administrative instructions. [1] Contexts¶In order to check rolled up recursive types, the context is locally extended with an additional component that records the sub type corresponding to each recursive type index within the current group of recursive types:
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}}
& {\href{../valid/conventions.html#context}{\mathit{context}}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}}
\dots , \href{../appendix/properties.html#context-ext}{\mathsf{recs}}~{{\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}^\ast} \} \\
\end{array} \\
\end{array}\end{split}\]
Types¶Well-formedness for extended type forms is defined as follows. The type use \((\href{../syntax/types.html#syntax-heaptype}{\mathsf{rec}} {.} i)\) is valid if:
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
C{.}\href{../appendix/properties.html#context-ext}{\mathsf{recs}}{}[i] = {\mathit{st}}
}{
C \href{../valid/types.html#valid-typeuse}{\vdash} \href{../syntax/types.html#syntax-heaptype}{\mathsf{rec}} {.} i : \href{../valid/types.html#valid-typeuse}{\mathsf{ok}}
}
\qquad
\end{array}\]
The heap type \(\href{../valid/conventions.html#syntax-valtype-ext}{\mathsf{bot}}\) is always valid.
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
}{
C \href{../valid/types.html#valid-heaptype}{\vdash} \href{../valid/conventions.html#syntax-valtype-ext}{\mathsf{bot}} : \href{../valid/types.html#valid-heaptype}{\mathsf{ok}}
}
\qquad
\end{array}\]
The value type \(\href{../valid/conventions.html#syntax-valtype-ext}{\mathsf{bot}}\) is always valid.
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
}{
C \href{../valid/types.html#valid-valtype}{\vdash} \href{../valid/conventions.html#syntax-valtype-ext}{\mathsf{bot}} : \href{../valid/types.html#valid-valtype}{\mathsf{ok}}
}
\qquad
\end{array}\]
The recursive type \((\href{../syntax/types.html#syntax-rectype}{\mathsf{rec}}~{{\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}^\ast})\) is valid for \(i\) if:
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
}{
C \href{../valid/types.html#valid-rectype}{\vdash} \href{../syntax/types.html#syntax-rectype}{\mathsf{rec}}~\epsilon : {\href{../valid/types.html#valid-subtype}{\mathsf{ok}}}{(i)}
}
\qquad
\frac{
C \href{../valid/types.html#valid-subtype}{\vdash} {\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}_1 : {\href{../valid/types.html#valid-subtype}{\mathsf{ok}}}{(i)}
\qquad
C \href{../valid/types.html#valid-rectype}{\vdash} \href{../syntax/types.html#syntax-rectype}{\mathsf{rec}}~{{\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}^\ast} : {\href{../valid/types.html#valid-subtype}{\mathsf{ok}}}{(i + 1)}
}{
C \href{../valid/types.html#valid-rectype}{\vdash} \href{../syntax/types.html#syntax-rectype}{\mathsf{rec}}~({\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}_1~{{\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}^\ast}) : {\href{../valid/types.html#valid-subtype}{\mathsf{ok}}}{(i)}
}
\qquad
\end{array}\]
The sub type \((\href{../syntax/types.html#syntax-subtype}{\mathsf{sub}}~{\href{../syntax/types.html#syntax-subtype}{\mathsf{final}}^?}~{{\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}}^\ast}~{\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}})\) is valid for \(i\) if:
\[\begin{split}\begin{array}{@{}c@{}}\displaystyle
\frac{
\begin{array}{@{}c@{}}
{|{{\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}}^\ast}|} \leq 1
\qquad
(C \href{../valid/types.html#valid-typeuse}{\vdash} {\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}} : \href{../valid/types.html#valid-typeuse}{\mathsf{ok}})^\ast
\qquad
({\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}} \prec i)^\ast
\\
({{\href{../appendix/properties.html#aux-unroll-heaptype}{\mathrm{unroll}}}}_{C}({\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}}) = \href{../syntax/types.html#syntax-subtype}{\mathsf{sub}}~{{\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}'}^\ast}~{\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}'})^\ast
\\
C \href{../valid/types.html#valid-comptype}{\vdash} {\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}} : \href{../valid/types.html#valid-comptype}{\mathsf{ok}}
\qquad
(C \href{../valid/matching.html#match-comptype}{\vdash} {\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}} \href{../valid/matching.html#match-comptype}{\leq} {\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}'})^\ast
\end{array}
}{
C \href{../valid/types.html#valid-subtype}{\vdash} \href{../syntax/types.html#syntax-subtype}{\mathsf{sub}}~{\href{../syntax/types.html#syntax-subtype}{\mathsf{final}}^?}~{{\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}}^\ast}~{\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}} : {\href{../valid/types.html#valid-subtype}{\mathsf{ok}}}{(i)}
}
\qquad
\end{array}\end{split}\]
where:
\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}}
{{\href{../appendix/properties.html#aux-unroll-heaptype}{\mathrm{unroll}}}}_{C}({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}) & = & {\href{../valid/conventions.html#aux-unroll-deftype}{\mathrm{unroll}}}({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}) \\
{{\href{../appendix/properties.html#aux-unroll-heaptype}{\mathrm{unroll}}}}_{C}({\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}}) & = & {\href{../valid/conventions.html#aux-unroll-deftype}{\mathrm{unroll}}}(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[{\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}}]) \\
{{\href{../appendix/properties.html#aux-unroll-heaptype}{\mathrm{unroll}}}}_{C}(\href{../syntax/types.html#syntax-heaptype}{\mathsf{rec}} {.} i) & = & C{.}\href{../appendix/properties.html#context-ext}{\mathsf{recs}}{}[i] \\[0.8ex]
\href{../syntax/types.html#syntax-heaptype}{\mathsf{rec}} {.} j \prec i & = & j < i \\
{\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}} \prec i & = & \mathsf{true} & \quad \mbox{otherwise} \\
\end{array}\end{split}\]
Note The new rules for recursive types and sub types complement the ones previously given, which only allowed regular type indices as supertypes. They define validity of rolled-up recursive types, like they occur in defined types, in turn needed to define validity of contexts. None of these rules are needed in the implementation of a validator. The defined type \(({\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}} {.} i)\) is valid if:
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
C, \href{../appendix/properties.html#context-ext}{\mathsf{recs}}~{{\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}^{n}} \href{../valid/types.html#valid-rectype}{\vdash} {\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}} : {\href{../valid/types.html#valid-subtype}{\mathsf{ok}}}{(0)}
\qquad
{\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}} = \href{../syntax/types.html#syntax-rectype}{\mathsf{rec}}~{{\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}^{n}}
\qquad
i < n
}{
C \href{../appendix/properties.html#valid-deftype}{\vdash} {\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}} {.} i : \href{../appendix/properties.html#valid-deftype}{\mathsf{ok}}
}
\qquad
\end{array}\]
Subtyping¶Inside a rolled-up recursive type, a recursive type index can match another heap type.
\[\begin{split}\begin{array}{@{}c@{}}\displaystyle
\frac{
C{.}\href{../appendix/properties.html#context-ext}{\mathsf{recs}}{}[i] = \href{../syntax/types.html#syntax-subtype}{\mathsf{sub}}~{\href{../syntax/types.html#syntax-subtype}{\mathsf{final}}^?}~(\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~{{\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}}^\ast})
}{
C \href{../valid/matching.html#match-heaptype}{\vdash} \href{../syntax/types.html#syntax-heaptype}{\mathsf{rec}} {.} i \href{../valid/matching.html#match-heaptype}{\leq} \href{../syntax/types.html#syntax-heaptype}{\mathsf{struct}}
}
\\[3ex]\displaystyle
\frac{
C{.}\href{../appendix/properties.html#context-ext}{\mathsf{recs}}{}[i] = \href{../syntax/types.html#syntax-subtype}{\mathsf{sub}}~{\href{../syntax/types.html#syntax-subtype}{\mathsf{final}}^?}~(\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~{\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}})
}{
C \href{../valid/matching.html#match-heaptype}{\vdash} \href{../syntax/types.html#syntax-heaptype}{\mathsf{rec}} {.} i \href{../valid/matching.html#match-heaptype}{\leq} \href{../syntax/types.html#syntax-heaptype}{\mathsf{array}}
}
\\[3ex]\displaystyle
\frac{
C{.}\href{../appendix/properties.html#context-ext}{\mathsf{recs}}{}[i] = \href{../syntax/types.html#syntax-subtype}{\mathsf{sub}}~{\href{../syntax/types.html#syntax-subtype}{\mathsf{final}}^?}~(\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast} \href{../syntax/types.html#syntax-comptype}{\rightarrow} {t_2^\ast})
}{
C \href{../valid/matching.html#match-heaptype}{\vdash} \href{../syntax/types.html#syntax-heaptype}{\mathsf{rec}} {.} i \href{../valid/matching.html#match-heaptype}{\leq} \href{../syntax/types.html#syntax-heaptype}{\mathsf{func}}
}
\\[3ex]\displaystyle
\frac{
C{.}\href{../appendix/properties.html#context-ext}{\mathsf{recs}}{}[i] = \href{../syntax/types.html#syntax-subtype}{\mathsf{sub}}~{\href{../syntax/types.html#syntax-subtype}{\mathsf{final}}^?}~{{\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}}^\ast}~{\mathit{ct}}
}{
C \href{../valid/matching.html#match-heaptype}{\vdash} \href{../syntax/types.html#syntax-heaptype}{\mathsf{rec}} {.} i \href{../valid/matching.html#match-heaptype}{\leq} {{\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}}^\ast}{}[j]
}
\qquad
\end{array}\end{split}\]
Note These rules complement the previously given rules for matching heap types. They are only invoked when checking validity of rolled-up recursive types. Results¶Results can be classified by result types as follows. Results \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\)¶
\[\frac{
(S \href{../exec/values.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-val}{\mathit{val}} : t)^\ast
}{
S \href{../appendix/properties.html#valid-result}{\vdash} \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast : [t^\ast]
}\]
Results \((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}exn}}~a)~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{throw\_ref}}\)¶
\[\frac{
S \href{../exec/values.html#valid-val}{\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
\href{../valid/types.html#valid-resulttype}{\vdash} [t^\ast] : \href{../valid/types.html#valid-resulttype}{\mathsf{ok}}
}{
S \href{../appendix/properties.html#valid-result}{\vdash} (\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}exn}}~a)~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{throw\_ref}} : [t^\ast]
}\]
Results \(\href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}\)¶
\[\frac{
\href{../valid/types.html#valid-resulttype}{\vdash} [t^\ast] : \href{../valid/types.html#valid-resulttype}{\mathsf{ok}}
}{
S \href{../appendix/properties.html#valid-result}{\vdash} \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} : [t^\ast]
}\]
Store Validity¶The following typing rules specify when a runtime store \(S\) is valid. A valid store must consist of tag, global, memory, table, function, data, element, structure, array, exception, and module instances that are themselves valid, relative to \(S\). To that end, each kind of instance is classified by a respective tag, global, memory, table, function, or element, type, or just \(\mathsf{ok}\) in the case of data structures, arrays, or exceptions. Module instances are classified by module contexts, which are regular contexts repurposed as module types describing the index spaces defined by a module. Store \(S\)¶
\[\begin{split}~\\[-1ex]
\frac{
\begin{array}{@{}c@{}}
(S \href{../appendix/properties.html#valid-taginst}{\vdash} \href{../exec/runtime.html#syntax-taginst}{\mathit{taginst}} : \href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}})^\ast
\qquad
(S \href{../appendix/properties.html#valid-globalinst}{\vdash} \href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}} : \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}})^\ast
\\
(S \href{../appendix/properties.html#valid-meminst}{\vdash} \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}} : \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}})^\ast
\qquad
(S \href{../appendix/properties.html#valid-tableinst}{\vdash} \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}} : \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}})^\ast
\\
(S \href{../appendix/properties.html#valid-funcinst}{\vdash} \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}} : \href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}})^\ast
\qquad
(S \href{../appendix/properties.html#valid-datainst}{\vdash} \href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}} : \href{../appendix/properties.html#valid-datainst}{\mathsf{ok}})^\ast
\qquad
(S \href{../appendix/properties.html#valid-eleminst}{\vdash} \href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}} : \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}})^\ast
\\
(S \href{../appendix/properties.html#valid-structinst}{\vdash} \href{../exec/runtime.html#syntax-structinst}{\mathit{structinst}} : \href{../appendix/properties.html#valid-structinst}{\mathsf{ok}})^\ast
\qquad
(S \href{../appendix/properties.html#valid-arrayinst}{\vdash} \href{../exec/runtime.html#syntax-arrayinst}{\mathit{arrayinst}} : \href{../appendix/properties.html#valid-arrayinst}{\mathsf{ok}})^\ast
\qquad
(S \href{../appendix/properties.html#valid-exninst}{\vdash} \href{../exec/runtime.html#syntax-exninst}{\mathit{exninst}} : \href{../appendix/properties.html#valid-exninst}{\mathsf{ok}})^\ast
\\
S = \{
\begin{array}[t]{@{}l@{}}
\href{../exec/runtime.html#syntax-store}{\mathsf{tags}}~\href{../exec/runtime.html#syntax-taginst}{\mathit{taginst}}^\ast,
\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}~\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}^\ast,
\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}~\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}^\ast,
\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}~\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}^\ast,
\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}~\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}^\ast, \\
\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}~\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}^\ast,
\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}~\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}^\ast,
\href{../exec/runtime.html#syntax-store}{\mathsf{structs}}~\href{../exec/runtime.html#syntax-structinst}{\mathit{structinst}}^\ast,
\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}~\href{../exec/runtime.html#syntax-arrayinst}{\mathit{arrayinst}}^\ast,
\href{../exec/runtime.html#syntax-store}{\mathsf{exns}}~\href{../exec/runtime.html#syntax-exninst}{\mathit{exninst}}^\ast \}
\end{array}
\\
(S.\href{../exec/runtime.html#syntax-store}{\mathsf{structs}}[a_{\mathrm{s}}] = \href{../exec/runtime.html#syntax-structinst}{\mathit{structinst}})^\ast
\qquad
((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}struct}}~a_{\mathrm{s}}) \not\gg^+_S (\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}struct}}~a_{\mathrm{s}}))^\ast
\\
(S.\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}[a_{\mathrm{a}}] = \href{../exec/runtime.html#syntax-arrayinst}{\mathit{arrayinst}})^\ast
\qquad
((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a_{\mathrm{a}}) \not\gg^+_S (\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a_{\mathrm{a}}))^\ast
\\
(S.\href{../exec/runtime.html#syntax-store}{\mathsf{exns}}[a_{\mathrm{e}}] = \href{../exec/runtime.html#syntax-exninst}{\mathit{exninst}})^\ast
\qquad
((\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}exn}}~a_{\mathrm{e}}) \not\gg^+_S (\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}exn}}~a_{\mathrm{e}}))^\ast
\end{array}
}{
\href{../appendix/properties.html#valid-store}{\vdash} S : \href{../appendix/properties.html#valid-store}{\mathsf{ok}}
}\end{split}\]
where \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_1 \gg^+_S \href{../exec/runtime.html#syntax-val}{\mathit{val}}_2\) denotes the transitive closure of the following immutable reachability relation on values:
\[\begin{split}\begin{array}{@{}lcll@{}}
(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}struct}}~a) &\gg_S& S.\href{../exec/runtime.html#syntax-store}{\mathsf{structs}}[a].\href{../exec/runtime.html#syntax-structinst}{\mathsf{fields}}[i]
& \mathrel{\mbox{if}} \href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}(S.\href{../exec/runtime.html#syntax-store}{\mathsf{structs}}[a].\href{../exec/runtime.html#syntax-structinst}{\mathsf{type}}) = \href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~\mathit{ft}_1^i~\mathit{st}~\mathit{ft}_2^\ast \\
(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~a) &\gg_S& S.\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}[a].\href{../exec/runtime.html#syntax-arrayinst}{\mathsf{fields}}[i]
& \mathrel{\mbox{if}} \href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}(S.\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}[a].\href{../exec/runtime.html#syntax-arrayinst}{\mathsf{type}}) = \href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~\mathit{st} \\
(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}exn}}~a) &\gg_S& S.\href{../exec/runtime.html#syntax-store}{\mathsf{exns}}[a].\href{../exec/runtime.html#syntax-exninst}{\mathsf{fields}}[i] \\
(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}extern}}~\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}) &\gg_S& \href{../exec/runtime.html#syntax-ref}{\mathit{ref}} \\
\end{array}\end{split}\]
Note The constraint on reachability through immutable fields prevents the presence of cyclic data structures that can not be constructed in the language. Cycles can only be formed using mutation. Tag Instances \(\{ \href{../exec/runtime.html#syntax-taginst}{\mathsf{type}}~\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}} \}\)¶
\[\frac{
\href{../valid/types.html#valid-tagtype}{\vdash} \href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}} : \href{../valid/types.html#valid-tagtype}{\mathsf{ok}}
}{
S \href{../appendix/properties.html#valid-taginst}{\vdash} \{ \href{../exec/runtime.html#syntax-taginst}{\mathsf{type}}~\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}} \} : \href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}
}\]
Global Instances \(\{ \href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}}~\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t, \href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}} \}\)¶
\[\frac{
\href{../valid/types.html#valid-globaltype}{\vdash} \href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t : \href{../valid/types.html#valid-globaltype}{\mathsf{ok}}
\qquad
S \href{../exec/values.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-val}{\mathit{val}} : t'
\qquad
\href{../valid/matching.html#match-valtype}{\vdash} t' \href{../valid/matching.html#match-valtype}{\leq} t
}{
S \href{../appendix/properties.html#valid-globalinst}{\vdash} \{ \href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}}~\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t, \href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}} \} : \href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t
}\]
Memory Instances \(\{ \href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}~(\href{../syntax/types.html#syntax-addrtype}{\mathit{addrtype}}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}), \href{../exec/runtime.html#syntax-meminst}{\mathsf{bytes}}~b^\ast \}\)¶
\[\frac{
\href{../valid/types.html#valid-memtype}{\vdash} \href{../syntax/types.html#syntax-addrtype}{\mathit{addrtype}}~[n\,{..}\,m] : \href{../valid/types.html#valid-memtype}{\mathsf{ok}}
\qquad
|b^\ast| = n \cdot 64\,\mathrm{Ki}
}{
S \href{../appendix/properties.html#valid-meminst}{\vdash} \{ \href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}~(\href{../syntax/types.html#syntax-addrtype}{\mathit{addrtype}}~[n\,{..}\,m]), \href{../exec/runtime.html#syntax-meminst}{\mathsf{bytes}}~b^\ast \} : \href{../syntax/types.html#syntax-addrtype}{\mathit{addrtype}}~[n\,{..}\,m]
}\]
Table Instances \(\{ \href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}~(\href{../syntax/types.html#syntax-addrtype}{\mathit{addrtype}}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t), \href{../exec/runtime.html#syntax-tableinst}{\mathsf{refs}}~\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast \}\)¶
\[\frac{
\href{../valid/types.html#valid-tabletype}{\vdash} \href{../syntax/types.html#syntax-addrtype}{\mathit{addrtype}}~[n\,{..}\,m]~t : \href{../valid/types.html#valid-tabletype}{\mathsf{ok}}
\qquad
|\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast| = n
\qquad
(S \vdash \href{../exec/runtime.html#syntax-ref}{\mathit{ref}} : t')^\ast
\qquad
(\href{../valid/matching.html#match-reftype}{\vdash} t' \href{../valid/matching.html#match-valtype}{\leq} t)^\ast
}{
S \href{../appendix/properties.html#valid-tableinst}{\vdash} \{ \href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}~(\href{../syntax/types.html#syntax-addrtype}{\mathit{addrtype}}~[n\,{..}\,m]~t), \href{../exec/runtime.html#syntax-tableinst}{\mathsf{refs}}~\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast \} : \href{../syntax/types.html#syntax-addrtype}{\mathit{addrtype}}~[n\,{..}\,m]~t
}\]
Function Instances \(\{\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{code}}~\href{../syntax/modules.html#syntax-func}{\mathit{func}}\}\)¶
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\href{../appendix/properties.html#valid-deftype}{\vdash} \href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}} : \href{../appendix/properties.html#valid-deftype}{\mathsf{ok}}
\qquad
S \href{../appendix/properties.html#valid-moduleinst}{\vdash} \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}} : C
\\
C \href{../valid/modules.html#valid-func}{\vdash} \href{../syntax/modules.html#syntax-func}{\mathit{func}} : \href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}'
\qquad
C \href{../valid/matching.html#match-deftype}{\vdash} \href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}' \href{../valid/matching.html#match-deftype}{\leq} \href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}
\end{array}
}{
S \href{../appendix/properties.html#valid-funcinst}{\vdash} \{\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{code}}~\href{../syntax/modules.html#syntax-func}{\mathit{func}}\} : \href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}
}\end{split}\]
Host Function Instances \(\{\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{hostfunc}}~\mathit{hf}\}\)¶
\[\begin{split}\frac{
\begin{array}[b]{@{}r@{}}
\href{../appendix/properties.html#valid-deftype}{\vdash} \href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}} : \href{../appendix/properties.html#valid-deftype}{\mathsf{ok}}
\\
\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}} \approx \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~ [t_1^\ast] \href{../syntax/types.html#syntax-comptype}{\rightarrow} [t_2^\ast]
\end{array}
\quad
\begin{array}[b]{@{}l@{}}
\forall S_1, \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast,~
{\href{../appendix/properties.html#valid-store}{\vdash} S_1 : \href{../appendix/properties.html#valid-store}{\mathsf{ok}}} \wedge
{\href{../appendix/properties.html#extend-store}{\vdash} S \href{../appendix/properties.html#extend}{\preceq} S_1} \wedge
{S_1 \href{../appendix/properties.html#valid-result}{\vdash} \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast : [t_1^\ast]}
\Longrightarrow {} \\ \qquad
\mathit{hf}(S_1; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast) \supset \emptyset \wedge {} \\ \qquad
\forall R \in \mathit{hf}(S_1; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast),~
R = \bot \vee {} \\ \qquad\qquad
\exists S_2, \href{../exec/runtime.html#syntax-result}{\mathit{result}},~
{\href{../appendix/properties.html#valid-store}{\vdash} S_2 : \href{../appendix/properties.html#valid-store}{\mathsf{ok}}} \wedge
{\href{../appendix/properties.html#extend-store}{\vdash} S_1 \href{../appendix/properties.html#extend}{\preceq} S_2} \wedge
{S_2 \href{../appendix/properties.html#valid-result}{\vdash} \href{../exec/runtime.html#syntax-result}{\mathit{result}} : [t_2^\ast]} \wedge
R = (S_2; \href{../exec/runtime.html#syntax-result}{\mathit{result}})
\end{array}
}{
S \href{../appendix/properties.html#valid-funcinst}{\vdash} \{\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{hostfunc}}~\mathit{hf}\} : \href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}
}\end{split}\]
Note This rule states that, if appropriate pre-conditions about store and arguments are satisfied, then executing the host function must satisfy appropriate post-conditions about store and results. The post-conditions match the ones in the execution rule for invoking host functions. Any store under which the function is invoked is assumed to be an extension of the current store. That way, the function itself is able to make sufficient assumptions about future stores. Data Instances \(\{ \href{../exec/runtime.html#syntax-datainst}{\mathsf{bytes}}~b^\ast \}\)¶
\[\frac{
}{
S \href{../appendix/properties.html#valid-datainst}{\vdash} \{ \href{../exec/runtime.html#syntax-datainst}{\mathsf{bytes}}~b^\ast \} : \href{../appendix/properties.html#valid-datainst}{\mathsf{ok}}
}\]
Element Instances \(\{ \href{../exec/runtime.html#syntax-eleminst}{\mathsf{type}}~t, \href{../exec/runtime.html#syntax-eleminst}{\mathsf{refs}}~\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast \}\)¶
\[\frac{
\href{../valid/types.html#valid-reftype}{\vdash} t : \href{../valid/types.html#valid-reftype}{\mathsf{ok}}
\qquad
(S \href{../exec/values.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-ref}{\mathit{ref}} : t')^\ast
\qquad
(\href{../valid/matching.html#match-reftype}{\vdash} t' \href{../valid/matching.html#match-valtype}{\leq} t)^\ast
}{
S \href{../appendix/properties.html#valid-eleminst}{\vdash} \{ \href{../exec/runtime.html#syntax-eleminst}{\mathsf{type}}~t, \href{../exec/runtime.html#syntax-eleminst}{\mathsf{refs}}~\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast \} : t
}\]
Structure Instances \(\{ \href{../exec/runtime.html#syntax-structinst}{\mathsf{type}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}, \href{../exec/runtime.html#syntax-structinst}{\mathsf{fields}}~\href{../exec/runtime.html#syntax-fieldval}{\mathit{fieldval}}^\ast \}\)¶
\[\frac{
\href{../appendix/properties.html#valid-deftype}{\vdash} \mathit{dt} : \href{../appendix/properties.html#valid-deftype}{\mathsf{ok}}
\qquad
\href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}(\mathit{dt}) = \href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\mathit{st})^\ast
\qquad
(S \href{../appendix/properties.html#valid-fieldval}{\vdash} \mathit{fv} : \mathit{st})^\ast
}{
S \href{../appendix/properties.html#valid-structinst}{\vdash} \{ \href{../exec/runtime.html#syntax-structinst}{\mathsf{type}}~\mathit{dt}, \href{../exec/runtime.html#syntax-structinst}{\mathsf{fields}}~\mathit{fv}^\ast \} : \href{../appendix/properties.html#valid-structinst}{\mathsf{ok}}
}\]
Array Instances \(\{ \href{../exec/runtime.html#syntax-arrayinst}{\mathsf{type}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}, \href{../exec/runtime.html#syntax-arrayinst}{\mathsf{fields}}~\href{../exec/runtime.html#syntax-fieldval}{\mathit{fieldval}}^\ast \}\)¶
\[\frac{
\href{../appendix/properties.html#valid-deftype}{\vdash} \mathit{dt} : \href{../appendix/properties.html#valid-deftype}{\mathsf{ok}}
\qquad
\href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}(\mathit{dt}) = \href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\mathit{st})
\qquad
(S \href{../appendix/properties.html#valid-fieldval}{\vdash} \mathit{fv} : \mathit{st})^\ast
}{
S \href{../appendix/properties.html#valid-arrayinst}{\vdash} \{ \href{../exec/runtime.html#syntax-arrayinst}{\mathsf{type}}~\mathit{dt}, \href{../exec/runtime.html#syntax-arrayinst}{\mathsf{fields}}~\mathit{fv}^\ast \} : \href{../appendix/properties.html#valid-arrayinst}{\mathsf{ok}}
}\]
Field Values \(\href{../exec/runtime.html#syntax-fieldval}{\mathit{fieldval}}\)¶
\[\frac{
}{
S \href{../appendix/properties.html#valid-packval}{\vdash} \mathit{pt}.\href{../exec/runtime.html#syntax-packval}{\mathsf{pack}}~i : \mathit{pt}
}\]
Exception Instances \(\{ \href{../exec/runtime.html#syntax-exninst}{\mathsf{tag}}~a, \href{../exec/runtime.html#syntax-exninst}{\mathsf{fields}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast \}\)¶
\[\frac{
S.\href{../exec/runtime.html#syntax-store}{\mathsf{tags}}[a].\href{../exec/runtime.html#syntax-taginst}{\mathsf{type}} \approx \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~ [t^\ast] \href{../syntax/types.html#syntax-comptype}{\rightarrow} []
\qquad
(S \href{../exec/values.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-val}{\mathit{val}} : t)^\ast
}{
S \href{../appendix/properties.html#valid-exninst}{\vdash} \{ \href{../exec/runtime.html#syntax-exninst}{\mathsf{tag}}~a, \href{../exec/runtime.html#syntax-exninst}{\mathsf{fields}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast \} : \href{../appendix/properties.html#valid-exninst}{\mathsf{ok}}
}\]
Export Instances \(\{ \href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../exec/runtime.html#syntax-exportinst}{\mathsf{addr}}~\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}} \}\)¶
\[\frac{
S \href{../exec/values.html#valid-externaddr}{\vdash} \href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}} : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}
}{
S \href{../appendix/properties.html#valid-exportinst}{\vdash} \{ \href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../exec/runtime.html#syntax-exportinst}{\mathsf{addr}}~\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}} \} : \href{../appendix/properties.html#valid-exportinst}{\mathsf{ok}}
}\]
Module Instances \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\)¶
\[\begin{split}~\\[-1ex]
\frac{
\begin{array}{@{}c@{}}
(\href{../appendix/properties.html#valid-deftype}{\vdash} \href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}} : \href{../appendix/properties.html#valid-deftype}{\mathsf{ok}})^\ast
\qquad
(S \href{../exec/values.html#valid-externaddr}{\vdash} \href{../exec/runtime.html#syntax-externaddr}{\mathsf{tag}}~\href{../exec/runtime.html#syntax-tagaddr}{\mathit{tagaddr}} : \href{../syntax/types.html#syntax-externtype}{\mathsf{tag}}~\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}})^\ast
\\
(S \href{../exec/values.html#valid-externaddr}{\vdash} \href{../exec/runtime.html#syntax-externaddr}{\mathsf{global}}~\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}} : \href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}})^\ast
\qquad
(S \href{../exec/values.html#valid-externaddr}{\vdash} \href{../exec/runtime.html#syntax-externaddr}{\mathsf{func}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} : \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}_{\mathsf{F}})^\ast
\\
(S \href{../exec/values.html#valid-externaddr}{\vdash} \href{../exec/runtime.html#syntax-externaddr}{\mathsf{mem}}~\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}} : \href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}})^\ast
\qquad
(S \href{../exec/values.html#valid-externaddr}{\vdash} \href{../exec/runtime.html#syntax-externaddr}{\mathsf{table}}~\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}} : \href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}})^\ast
\\
(S \href{../appendix/properties.html#valid-datainst}{\vdash} S.\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}[\href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}] : \mathit{ok})^\ast
\qquad
(S \href{../appendix/properties.html#valid-eleminst}{\vdash} S.\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}[\href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}] : \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}})^\ast
\\
(S \href{../appendix/properties.html#valid-exportinst}{\vdash} \href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}} : \href{../appendix/properties.html#valid-exportinst}{\mathsf{ok}})^\ast
\qquad
(\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}.\href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}})^\ast ~\mbox{disjoint}
\\
k \le |\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}^\ast|
\end{array}
}{
S \href{../appendix/properties.html#valid-moduleinst}{\vdash} \{
\begin{array}[t]{@{}l@{~}l@{}}
\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}} & \href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}^\ast, \\
\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tags}} & \href{../exec/runtime.html#syntax-tagaddr}{\mathit{tagaddr}}^\ast, \\
\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globals}} & \href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}^\ast, \\
\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{mems}} & \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}^\ast, \\
\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tables}} & \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}^\ast, \\
\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcs}} & \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}^\ast, \\
\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{datas}} & \href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}^\ast, \\
\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{elems}} & \href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}^\ast, \\
\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{exports}} & \href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}^\ast ~\} : \{
\begin{array}[t]{@{}l@{~}l@{}}
\href{../valid/conventions.html#context}{\mathsf{types}} & \href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}^\ast, \\
\href{../valid/conventions.html#context}{\mathsf{tags}} & \href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}^\ast, \\
\href{../valid/conventions.html#context}{\mathsf{globals}} & \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}^\ast, \\
\href{../valid/conventions.html#context}{\mathsf{mems}} & \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}^\ast, \\
\href{../valid/conventions.html#context}{\mathsf{tables}} & \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}^\ast, \\
\href{../valid/conventions.html#context}{\mathsf{funcs}} & \href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}_{\mathsf{F}}^\ast, \\
\href{../valid/conventions.html#context}{\mathsf{datas}} & \mathit{ok}^\ast, \\
\href{../valid/conventions.html#context}{\mathsf{elems}} & \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}^\ast, \\
\href{../valid/conventions.html#context}{\mathsf{refs}} & 0 \dots k-1 ~\}
\end{array}
\end{array}
}\end{split}\]
Note The field \(C{.}\mathsf{refs}\) from the resulting context is meant to be constructed to contain all function indices from the module. However, modules and their instances can contain more than \({2^{32}}\) functions (at most \({2^{32}}\) definitions plus \({2^{32}}\) imports), while the highest representable function index is \({2^{32}} - 1\). The variable \(k\) in the rule hence allows picking an upper limit for \(C{.}\mathsf{refs}\) that is smaller than the total number of functions, in case that is necessary for \(C{.}\mathsf{refs}\) to be syntactically well-formed. In practice, \(k = {\min}({|{{\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}}^\ast}|}, {2^{32}})\) always is the maximally permissive choice. Configuration Validity¶To relate the WebAssembly type system to its execution semantics, the typing rules for instructions must be extended to configurations \(S;T\), which relates the store to execution threads. Configurations and threads are classified by their result type. In addition to the store \(S\), threads are typed under a return type \(\href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}^?\), which controls whether and with which type a \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{return}}\) instruction is allowed. This type is absent (\(\epsilon\)) except for instruction sequences inside an administrative \(\href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}\) instruction. Finally, frames are classified with frame contexts, which extend the module contexts of a frame’s associated module instance with the locals that the frame contains. Configurations \(S;T\)¶
\[\frac{
\href{../appendix/properties.html#valid-store}{\vdash} S : \href{../appendix/properties.html#valid-store}{\mathsf{ok}}
\qquad
S; \epsilon \href{../appendix/properties.html#valid-thread}{\vdash} T : [t^\ast]
}{
\href{../appendix/properties.html#valid-config}{\vdash} S; T : [t^\ast]
}\]
Threads \(F;\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\)¶
\[\frac{
S \href{../appendix/properties.html#valid-frame}{\vdash} F : C
\qquad
S; C,\href{../valid/conventions.html#context}{\mathsf{return}}~\href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}^? \href{../valid/instructions.html#valid-instrs}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : [] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t^\ast]
}{
S; \href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}^? \href{../appendix/properties.html#valid-thread}{\vdash} F; \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : [t^\ast]
}\]
Frames \(\{\href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast, \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\}\)¶
\[\frac{
S \href{../appendix/properties.html#valid-moduleinst}{\vdash} \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}} : C
\qquad
(S \href{../exec/values.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-val}{\mathit{val}} : t)^\ast
}{
S \href{../appendix/properties.html#valid-frame}{\vdash} \{\href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast, \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\} : (C, \href{../valid/conventions.html#context}{\mathsf{locals}}~t^\ast)
}\]
Administrative Instructions¶Typing rules for administrative instructions are specified as follows. In addition to the context \(C\), typing of these instructions is defined under a given store \(S\). To that end, all previous typing judgements \(C \vdash \mathit{prop}\) are generalized to include the store, as in \(S; C \vdash \mathit{prop}\), by implicitly adding \(S\) to all rules – \(S\) is never modified by the pre-existing rules, but it is accessed in the extra rules for administrative instructions given below. \(\href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}\)¶
\[\frac{
C \href{../valid/types.html#valid-instrtype}{\vdash} [t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t_2^\ast] : \href{../valid/types.html#valid-instrtype}{\mathsf{ok}}
}{
S; C \href{../appendix/properties.html#valid-instr-admin}{\vdash} \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} : [t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t_2^\ast]
}\]
\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}\)¶
\[\frac{
S \href{../exec/values.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-val}{\mathit{val}} : t
}{
S; C \href{../appendix/properties.html#valid-instr-admin}{\vdash} \href{../exec/runtime.html#syntax-val}{\mathit{val}} : [] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t]
}\]
\(\href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_0^\ast\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\)¶
\[\frac{
S; C \href{../valid/instructions.html#valid-instrs}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_0^\ast : [t_1^n] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x^\ast} [t_2^*]
\qquad
S; C,\href{../valid/conventions.html#context}{\mathsf{labels}}\,[t_1^n] \href{../valid/instructions.html#valid-instrs}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : [] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{{x'}^\ast} [t_2^*]
}{
S; C \href{../appendix/properties.html#valid-instr-admin}{\vdash} \href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_0^\ast\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : [] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t_2^*]
}\]
\(\href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}_n\{F\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\)¶
\[\frac{
\{\} \href{../valid/types.html#valid-resulttype}{\vdash} [t^n] : \href{../valid/types.html#valid-resulttype}{\mathsf{ok}}
\qquad
S; [t^n] \href{../valid/instructions.html#valid-instrs}{\vdash} F; \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : [t^n]
}{
S; C \href{../appendix/properties.html#valid-instr-admin}{\vdash} \href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}_n\{F\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : [] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t^n]
}\]
\(\href{../exec/runtime.html#syntax-handler}{\mathsf{handler}}_n\{\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}^\ast\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\)¶
\[\begin{split}\frac{
\begin{array}{c}
(C \href{../valid/instructions.html#valid-catch}{\vdash} \href{../syntax/instructions.html#syntax-catch}{\mathit{catch}} : \href{../valid/instructions.html#valid-catch}{\mathsf{ok}})^\ast
\qquad
S; C \href{../valid/instructions.html#valid-instrs}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : [] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t^\ast] \\
\end{array}
}{
S; C \href{../appendix/properties.html#valid-instr-admin}{\vdash} \href{../exec/runtime.html#syntax-handler}{\mathsf{handler}}_n\{\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}^\ast\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : [] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t^\ast]
}\end{split}\]
Store Extension¶Programs can mutate the store and its contained instances. Any such modification must respect certain invariants, such as not removing allocated instances or changing immutable definitions. While these invariants are inherent to the execution semantics of WebAssembly instructions and modules, host functions do not automatically adhere to them. Consequently, the required invariants must be stated as explicit constraints on the invocation of host functions. Soundness only holds when the embedder ensures these constraints. The necessary constraints are codified by the notion of store extension: a store state \(S'\) extends state \(S\), written \(S \href{../appendix/properties.html#extend}{\preceq} S'\), when the following rules hold. Note Extension does not imply that the new store is valid, which is defined separately above. Store \(S\)¶
\[\begin{split}\frac{
\begin{array}{@{}ccc@{}}
S_1.\href{../exec/runtime.html#syntax-store}{\mathsf{tags}} = \href{../exec/runtime.html#syntax-taginst}{\mathit{taginst}}_1^\ast &
S_2.\href{../exec/runtime.html#syntax-store}{\mathsf{tags}} = {\href{../exec/runtime.html#syntax-taginst}{\mathit{taginst}}'_1}^\ast~\href{../exec/runtime.html#syntax-taginst}{\mathit{taginst}}_2^\ast &
(\href{../appendix/properties.html#extend-taginst}{\vdash} \href{../exec/runtime.html#syntax-taginst}{\mathit{taginst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-taginst}{\mathit{taginst}}'_1)^\ast
\\
S_1.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}} = \href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}_1^\ast &
S_2.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}} = {\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}'_1}^\ast~\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}_2^\ast &
(\href{../appendix/properties.html#extend-globalinst}{\vdash} \href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}'_1)^\ast
\\
S_1.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}} = \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}_1^\ast &
S_2.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}} = {\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}'_1}^\ast~\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}_2^\ast &
(\href{../appendix/properties.html#extend-meminst}{\vdash} \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}'_1)^\ast
\\
S_1.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}} = \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}_1^\ast &
S_2.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}} = {\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}'_1}^\ast~\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}_2^\ast &
(\href{../appendix/properties.html#extend-tableinst}{\vdash} \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}'_1)^\ast \\
S_1.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}} = \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}_1^\ast &
S_2.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}} = {\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}'_1}^\ast~\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}_2^\ast &
(\href{../appendix/properties.html#extend-funcinst}{\vdash} \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}'_1)^\ast
\\
S_1.\href{../exec/runtime.html#syntax-store}{\mathsf{datas}} = \href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}_1^\ast &
S_2.\href{../exec/runtime.html#syntax-store}{\mathsf{datas}} = {\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}'_1}^\ast~\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}_2^\ast &
(\href{../appendix/properties.html#extend-datainst}{\vdash} \href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}'_1)^\ast
\\
S_1.\href{../exec/runtime.html#syntax-store}{\mathsf{elems}} = \href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}_1^\ast &
S_2.\href{../exec/runtime.html#syntax-store}{\mathsf{elems}} = {\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}'_1}^\ast~\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}_2^\ast &
(\href{../appendix/properties.html#extend-eleminst}{\vdash} \href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}'_1)^\ast
\\
S_1.\href{../exec/runtime.html#syntax-store}{\mathsf{structs}} = \href{../exec/runtime.html#syntax-structinst}{\mathit{structinst}}_1^\ast &
S_2.\href{../exec/runtime.html#syntax-store}{\mathsf{structs}} = {\href{../exec/runtime.html#syntax-structinst}{\mathit{structinst}}'_1}^\ast~\href{../exec/runtime.html#syntax-structinst}{\mathit{structinst}}_2^\ast &
(\href{../appendix/properties.html#extend-structinst}{\vdash} \href{../exec/runtime.html#syntax-structinst}{\mathit{structinst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-structinst}{\mathit{structinst}}'_1)^\ast
\\
S_1.\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}} = \href{../exec/runtime.html#syntax-arrayinst}{\mathit{arrayinst}}_1^\ast &
S_2.\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}} = {\href{../exec/runtime.html#syntax-arrayinst}{\mathit{arrayinst}}'_1}^\ast~\href{../exec/runtime.html#syntax-arrayinst}{\mathit{arrayinst}}_2^\ast &
(\href{../appendix/properties.html#extend-arrayinst}{\vdash} \href{../exec/runtime.html#syntax-arrayinst}{\mathit{arrayinst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-arrayinst}{\mathit{arrayinst}}'_1)^\ast
\\
S_1.\href{../exec/runtime.html#syntax-store}{\mathsf{exns}} = \href{../exec/runtime.html#syntax-exninst}{\mathit{exninst}}_1^\ast &
S_2.\href{../exec/runtime.html#syntax-store}{\mathsf{exns}} = {\href{../exec/runtime.html#syntax-exninst}{\mathit{exninst}}'_1}^\ast~\href{../exec/runtime.html#syntax-exninst}{\mathit{exninst}}_2^\ast &
(\href{../appendix/properties.html#extend-exninst}{\vdash} \href{../exec/runtime.html#syntax-exninst}{\mathit{exninst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-exninst}{\mathit{exninst}}'_1)^\ast
\\
\end{array}
}{
\href{../appendix/properties.html#extend-store}{\vdash} S_1 \href{../appendix/properties.html#extend}{\preceq} S_2
}\end{split}\]
Tag Instance \(\href{../exec/runtime.html#syntax-taginst}{\mathit{taginst}}\)¶
\[\frac{
}{
\href{../appendix/properties.html#extend-taginst}{\vdash} \href{../exec/runtime.html#syntax-taginst}{\mathit{taginst}} \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-taginst}{\mathit{taginst}}
}\]
Global Instance \(\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}\)¶
\[\frac{
\href{../syntax/types.html#syntax-mut}{\mathit{mut}} = \href{../syntax/types.html#syntax-mut}{\mathsf{mut}} \vee \href{../exec/runtime.html#syntax-val}{\mathit{val}}_1 = \href{../exec/runtime.html#syntax-val}{\mathit{val}}_2
}{
\href{../appendix/properties.html#extend-globalinst}{\vdash} \{\href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}}~(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t), \href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}_1\} \href{../appendix/properties.html#extend}{\preceq} \{\href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}}~(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t), \href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}_2\}
}\]
Memory Instance \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}\)¶
\[\frac{
n_1 \leq n_2
}{
\href{../appendix/properties.html#extend-meminst}{\vdash} \{\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}~\mathit{mt}, \href{../exec/runtime.html#syntax-meminst}{\mathsf{bytes}}~b_1^{n_1}\} \href{../appendix/properties.html#extend}{\preceq} \{\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}~\mathit{mt}, \href{../exec/runtime.html#syntax-meminst}{\mathsf{bytes}}~b_2^{n_2}\}
}\]
Table Instance \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}\)¶
\[\frac{
n_1 \leq n_2
}{
\href{../appendix/properties.html#extend-tableinst}{\vdash} \{\href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}~\mathit{tt}, \href{../exec/runtime.html#syntax-tableinst}{\mathsf{refs}}~(\mathit{fa}_1^?)^{n_1}\} \href{../appendix/properties.html#extend}{\preceq} \{\href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}~\mathit{tt}, \href{../exec/runtime.html#syntax-tableinst}{\mathsf{refs}}~(\mathit{fa}_2^?)^{n_2}\}
}\]
Function Instance \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}\)¶
\[\frac{
}{
\href{../appendix/properties.html#extend-funcinst}{\vdash} \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}} \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}
}\]
Data Instance \(\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}\)¶
\[\frac{
}{
\href{../appendix/properties.html#extend-datainst}{\vdash} \{\href{../exec/runtime.html#syntax-datainst}{\mathsf{bytes}}~b^\ast\} \href{../appendix/properties.html#extend}{\preceq} \{\href{../exec/runtime.html#syntax-datainst}{\mathsf{bytes}}~b^\ast\}
}\]
\[\frac{
}{
\href{../appendix/properties.html#extend-datainst}{\vdash} \{\href{../exec/runtime.html#syntax-datainst}{\mathsf{bytes}}~b^\ast\} \href{../appendix/properties.html#extend}{\preceq} \{\href{../exec/runtime.html#syntax-datainst}{\mathsf{bytes}}~\epsilon\}
}\]
Element Instance \(\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}\)¶
\[\frac{
}{
\href{../appendix/properties.html#extend-eleminst}{\vdash} \{\href{../exec/runtime.html#syntax-eleminst}{\mathsf{type}}~t, \href{../exec/runtime.html#syntax-eleminst}{\mathsf{refs}}~a^\ast\} \href{../appendix/properties.html#extend}{\preceq} \{\href{../exec/runtime.html#syntax-eleminst}{\mathsf{type}}~t, \href{../exec/runtime.html#syntax-eleminst}{\mathsf{refs}}~a^\ast\}
}\]
\[\frac{
}{
\href{../appendix/properties.html#extend-eleminst}{\vdash} \{\href{../exec/runtime.html#syntax-eleminst}{\mathsf{type}}~t, \href{../exec/runtime.html#syntax-eleminst}{\mathsf{refs}}~a^\ast\} \href{../appendix/properties.html#extend}{\preceq} \{\href{../exec/runtime.html#syntax-eleminst}{\mathsf{type}}~t, \href{../exec/runtime.html#syntax-eleminst}{\mathsf{refs}}~\epsilon\}
}\]
Structure Instance \(\href{../exec/runtime.html#syntax-structinst}{\mathit{structinst}}\)¶
\[\frac{
(\href{../syntax/types.html#syntax-mut}{\mathit{mut}} = \href{../syntax/types.html#syntax-mut}{\mathsf{mut}} \vee \href{../exec/runtime.html#syntax-fieldval}{\mathit{fieldval}}_1 = \href{../exec/runtime.html#syntax-fieldval}{\mathit{fieldval}}_2)^\ast
}{
\href{../appendix/properties.html#extend-structinst}{\vdash} \{\href{../exec/runtime.html#syntax-structinst}{\mathsf{type}}~(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\mathit{st})^\ast, \href{../exec/runtime.html#syntax-structinst}{\mathsf{fields}}~\href{../exec/runtime.html#syntax-fieldval}{\mathit{fieldval}}_1^\ast\} \href{../appendix/properties.html#extend}{\preceq} \{\href{../exec/runtime.html#syntax-structinst}{\mathsf{type}}~(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\mathit{st})^\ast, \href{../exec/runtime.html#syntax-structinst}{\mathsf{fields}}~\href{../exec/runtime.html#syntax-fieldval}{\mathit{fieldval}}_2^\ast\}
}\]
Array Instance \(\href{../exec/runtime.html#syntax-arrayinst}{\mathit{arrayinst}}\)¶
\[\frac{
\href{../syntax/types.html#syntax-mut}{\mathit{mut}} = \href{../syntax/types.html#syntax-mut}{\mathsf{mut}} \vee \href{../exec/runtime.html#syntax-fieldval}{\mathit{fieldval}}_1^\ast = \href{../exec/runtime.html#syntax-fieldval}{\mathit{fieldval}}_2^\ast
}{
\href{../appendix/properties.html#extend-arrayinst}{\vdash} \{\href{../exec/runtime.html#syntax-arrayinst}{\mathsf{type}}~(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\mathit{st}), \href{../exec/runtime.html#syntax-arrayinst}{\mathsf{fields}}~\href{../exec/runtime.html#syntax-fieldval}{\mathit{fieldval}}_1^\ast\} \href{../appendix/properties.html#extend}{\preceq} \{\href{../exec/runtime.html#syntax-arrayinst}{\mathsf{type}}~(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\mathit{st}), \href{../exec/runtime.html#syntax-arrayinst}{\mathsf{fields}}~\href{../exec/runtime.html#syntax-fieldval}{\mathit{fieldval}}_2^\ast\}
}\]
Exception Instance \(\href{../exec/runtime.html#syntax-exninst}{\mathit{exninst}}\)¶
\[\frac{
}{
\href{../appendix/properties.html#extend-exninst}{\vdash} \href{../exec/runtime.html#syntax-exninst}{\mathit{exninst}} \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-exninst}{\mathit{exninst}}
}\]
Theorems¶Given the definition of valid configurations, the standard soundness theorems hold. [2] [3] Theorem (Preservation). If a configuration \(S;T\) is valid with result type \([t^\ast]\) (i.e., \(\href{../appendix/properties.html#valid-config}{\vdash} S;T : [t^\ast]\)), and steps to \(S';T'\) (i.e., \(S;T \href{../exec/conventions.html#exec-notation}{\hookrightarrow} S';T'\)), then \(S';T'\) is a valid configuration with the same result type (i.e., \(\href{../appendix/properties.html#valid-config}{\vdash} S';T' : [t^\ast]\)). Furthermore, \(S'\) is an extension of \(S\) (i.e., \(\href{../appendix/properties.html#extend-store}{\vdash} S \href{../appendix/properties.html#extend}{\preceq} S'\)). A terminal thread is one whose sequence of instructions is a result. A terminal configuration is a configuration whose thread is terminal. Theorem (Progress). If a configuration \(S;T\) is valid (i.e., \(\href{../appendix/properties.html#valid-config}{\vdash} S;T : [t^\ast]\) for some result type \([t^\ast]\)), then either it is terminal, or it can step to some configuration \(S';T'\) (i.e., \(S;T \href{../exec/conventions.html#exec-notation}{\hookrightarrow} S';T'\)). From Preservation and Progress the soundness of the WebAssembly type system follows directly. Corollary (Soundness). If a configuration \(S;T\) is valid (i.e., \(\href{../appendix/properties.html#valid-config}{\vdash} S;T : [t^\ast]\) for some result type \([t^\ast]\)), then it either diverges or takes a finite number of steps to reach a terminal configuration \(S';T'\) (i.e., \(S;T \href{../exec/conventions.html#exec-notation}{\hookrightarrow}^\ast S';T'\)) that is valid with the same result type (i.e., \(\href{../appendix/properties.html#valid-config}{\vdash} S';T' : [t^\ast]\)) and where \(S'\) is an extension of \(S\) (i.e., \(\href{../appendix/properties.html#extend-store}{\vdash} S \href{../appendix/properties.html#extend}{\preceq} S'\)). In other words, every thread in a valid configuration either runs forever, traps, throws an exception, or terminates with a result that has the expected type. Consequently, given a valid store, no computation defined by instantiation or invocation of a valid module can “crash” or otherwise (mis)behave in ways not covered by the execution semantics given in this specification. Type System Properties¶Principal Types¶The type system of WebAssembly features both subtyping and simple forms of polymorphism for instruction types. That has the effect that every instruction or instruction sequence can be classified with multiple different instruction types. However, the typing rules still allow deriving principal types for instruction sequences. That is, every valid instruction sequence has one particular type scheme, possibly containing some unconstrained place holder type variables, that is a subtype of all its valid instruction types, after substituting its type variables with suitable specific types. Moreover, when deriving an instruction type in a “forward” manner, i.e., the input of the instruction sequence is already fixed to specific types, then it has a principal output type expressible without type variables, up to a possibly polymorphic stack bottom representable with one single variable. In other words, “forward” principal types are effectively closed. Note For example, in isolation, the instruction \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}as\_non\_null}}\) has the type \([(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\mathit{ht})] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathit{ht})]\) for any choice of valid heap type \(\mathit{ht}\). Moreover, if the input type \([(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\mathit{ht})]\) is already determined, i.e., a specific \(\mathit{ht}\) is given, then the output type \([(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathit{ht})]\) is fully determined as well. The implication of the latter property is that a validator for complete instruction sequences (as they occur in valid modules) can be implemented with a simple left-to-right algorithm that does not require the introduction of type variables. A typing algorithm capable of handling partial instruction sequences (as might be considered for program analysis or program manipulation) needs to introduce type variables and perform substitutions, but it does not need to perform backtracking or record any non-syntactic constraints on these type variables. Technically, the syntax of heap, value, and result types can be enriched with type variables as follows:
\[\begin{split}\begin{array}{llll}
\def\mathdef1460#1{{}}\mathdef1460{nullability} & \mathit{null} &::=&
\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}^? ~|~ \alpha_{\mathit{null}} \\
\def\mathdef1460#1{{}}\mathdef1460{heap type} & \href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}} &::=&
\dots ~|~ \alpha_{\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}} \\
\def\mathdef1460#1{{}}\mathdef1460{reference type} & \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}} &::=&
\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathit{null}~\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}} \\
\def\mathdef1460#1{{}}\mathdef1460{value type} & \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}} &::=&
\dots ~|~ \alpha_{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}} ~|~ \alpha_{\mathit{numvectype}} \\
\def\mathdef1460#1{{}}\mathdef1460{result type} & \href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}} &::=&
[\alpha_{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}^\ast}^?~\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}^\ast] \\
\end{array}\end{split}\]
where each \(\alpha_{\mathit{xyz}}\) ranges over a set of type variables for syntactic class \(\mathit{xyz}\), respectively. The special class \(\mathit{numvectype}\) is defined as \(\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}} ~|~ \href{../syntax/types.html#syntax-vectype}{\mathit{vectype}} ~|~ \href{../valid/conventions.html#syntax-valtype-ext}{\mathsf{bot}}\), and is only needed to handle unannotated \(\href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{select}}\) instructions. A type is closed when it does not contain any type variables, and open otherwise. A type substitution \(\sigma\) is a finite mapping from type variables to closed types of the respective syntactic class. When applied to an open type, it replaces the type variables \(\alpha\) from its domain with the respective \(\sigma(\alpha)\). Theorem (Principal Types). If an instruction sequence \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\) is valid with some closed instruction type \(\href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}\) (i.e., \(C \href{../valid/instructions.html#valid-instrs}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : \href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}\)), then it is also valid with a possibly open instruction type \(\href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}_{\min}\) (i.e., \(C \href{../valid/instructions.html#valid-instrs}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : \href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}_{\min}\)), such that for every closed type \(\href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}'\) with which \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\) is valid (i.e., for all \(C \href{../valid/instructions.html#valid-instrs}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : \href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}'\)), there exists a substitution \(\sigma\), such that \(\sigma(\href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}_{\min})\) is a subtype of \(\href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}'\) (i.e., \(C \href{../valid/matching.html#match-instrtype}{\vdash} \sigma(\href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}_{\min}) \href{../valid/matching.html#match-instrtype}{\leq} \href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}'\)). Furthermore, \(\href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}_{\min}\) is unique up to the choice of type variables. Theorem (Closed Principal Forward Types). If closed input type \([t_1^\ast]\) is given and the instruction sequence \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\) is valid with instruction type \([t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x^\ast} [t_2^\ast]\) (i.e., \(C \href{../valid/instructions.html#valid-instrs}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : [t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x^\ast} [t_2^\ast]\)), then it is also valid with instruction type \([t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x^\ast} [\alpha_{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}^\ast}~t^\ast]\) (i.e., \(C \href{../valid/instructions.html#valid-instrs}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : [t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x^\ast} [\alpha_{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}^\ast}~t^\ast]\)), where all \(t^\ast\) are closed, such that for every closed result type \([{t'_2}^\ast]\) with which \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\) is valid (i.e., for all \(C \href{../valid/instructions.html#valid-instrs}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : [t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x^\ast} [{t'_2}^\ast]\)), there exists a substitution \(\sigma\), such that \([{t'_2}^\ast] = [\sigma(\alpha_{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}^\ast})~t^\ast]\). Type Lattice¶The Principal Types property depends on the existence of a greatest lower bound for any pair of types. Theorem (Greatest Lower Bounds for Value Types). For any two value types \(t_1\) and \(t_2\) that are valid (i.e., \(C \href{../valid/types.html#valid-valtype}{\vdash} t_1 : \href{../valid/types.html#valid-valtype}{\mathsf{ok}}\) and \(C \href{../valid/types.html#valid-valtype}{\vdash} t_2 : \href{../valid/types.html#valid-valtype}{\mathsf{ok}}\)), there exists a valid value type \(t\) that is a subtype of both \(t_1\) and \(t_2\) (i.e., \(C \href{../valid/types.html#valid-valtype}{\vdash} t : \href{../valid/types.html#valid-valtype}{\mathsf{ok}}\) and \(C \href{../valid/matching.html#match-valtype}{\vdash} t \href{../valid/matching.html#match-valtype}{\leq} t_1\) and \(C \href{../valid/matching.html#match-valtype}{\vdash} t \href{../valid/matching.html#match-valtype}{\leq} t_2\)), such that every valid value type \(t'\) that also is a subtype of both \(t_1\) and \(t_2\) (i.e., for all \(C \href{../valid/types.html#valid-valtype}{\vdash} t' : \href{../valid/types.html#valid-valtype}{\mathsf{ok}}\) and \(C \href{../valid/matching.html#match-valtype}{\vdash} t' \href{../valid/matching.html#match-valtype}{\leq} t_1\) and \(C \href{../valid/matching.html#match-valtype}{\vdash} t' \href{../valid/matching.html#match-valtype}{\leq} t_2\)), is a subtype of \(t\) (i.e., \(C \href{../valid/matching.html#match-valtype}{\vdash} t' \href{../valid/matching.html#match-valtype}{\leq} t\)). Note The greatest lower bound of two types may be \(\href{../valid/conventions.html#syntax-valtype-ext}{\mathsf{bot}}\). Theorem (Conditional Least Upper Bounds for Value Types). Any two value types \(t_1\) and \(t_2\) that are valid (i.e., \(C \href{../valid/types.html#valid-valtype}{\vdash} t_1 : \href{../valid/types.html#valid-valtype}{\mathsf{ok}}\) and \(C \href{../valid/types.html#valid-valtype}{\vdash} t_2 : \href{../valid/types.html#valid-valtype}{\mathsf{ok}}\)) either have no common supertype, or there exists a valid value type \(t\) that is a supertype of both \(t_1\) and \(t_2\) (i.e., \(C \href{../valid/types.html#valid-valtype}{\vdash} t : \href{../valid/types.html#valid-valtype}{\mathsf{ok}}\) and \(C \href{../valid/matching.html#match-valtype}{\vdash} t_1 \href{../valid/matching.html#match-valtype}{\leq} t\) and \(C \href{../valid/matching.html#match-valtype}{\vdash} t_2 \href{../valid/matching.html#match-valtype}{\leq} t\)), such that every valid value type \(t'\) that also is a supertype of both \(t_1\) and \(t_2\) (i.e., for all \(C \href{../valid/types.html#valid-valtype}{\vdash} t' : \href{../valid/types.html#valid-valtype}{\mathsf{ok}}\) and \(C \href{../valid/matching.html#match-valtype}{\vdash} t_1 \href{../valid/matching.html#match-valtype}{\leq} t'\) and \(C \href{../valid/matching.html#match-valtype}{\vdash} t_2 \href{../valid/matching.html#match-valtype}{\leq} t'\)), is a supertype of \(t\) (i.e., \(C \href{../valid/matching.html#match-valtype}{\vdash} t \href{../valid/matching.html#match-valtype}{\leq} t'\)). Note If a top type was added to the type system, a least upper bound would exist for any two types. Corollary (Type Lattice). Assuming the addition of a provisional top type, value types form a lattice with respect to their subtype relation. Finally, value types can be partitioned into multiple disjoint hierarchies that are not related by subtyping, except through \(\href{../valid/conventions.html#syntax-valtype-ext}{\mathsf{bot}}\). Theorem (Disjoint Subtype Hierarchies). The greatest lower bound of two value types is \(\href{../valid/conventions.html#syntax-valtype-ext}{\mathsf{bot}}\) or \(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../valid/conventions.html#syntax-valtype-ext}{\mathsf{bot}}\) if and only if they do not have a least upper bound. In other words, types that do not have common supertypes, do not have common subtypes either (other than \(\href{../valid/conventions.html#syntax-valtype-ext}{\mathsf{bot}}\) or \(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../valid/conventions.html#syntax-valtype-ext}{\mathsf{bot}}\)), and vice versa. Note Types from disjoint hierarchies can safely be represented in mutually incompatible ways in an implementation, because their values can never flow to the same place. Compositionality¶Valid instruction sequences can be freely composed, as long as their types match up. Theorem (Composition). If two instruction sequences \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast\) and \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_2^\ast\) are valid with types \([t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x_1^\ast} [t^\ast]\) and \([t^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x_2^\ast} [t_2^\ast]\), respectively (i.e., \(C \href{../valid/instructions.html#valid-instrs}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast : [t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x_1^\ast} [t^\ast]\) and \(C \href{../valid/instructions.html#valid-instrs}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast : [t^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x_2^\ast} [t_2^\ast]\)), then the concatenated instruction sequence \((\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast\;\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_2^\ast)\) is valid with type \([t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x_1^\ast\,x_2^\ast} [t_2^\ast]\) (i.e., \(C \href{../valid/instructions.html#valid-instrs}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast\;\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_2^\ast : [t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x_1^\ast\,x_2^\ast} [t_2^\ast]\)). Note More generally, instead of a shared type \([t^\ast]\), it suffices if the output type of \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast\) is a subtype of the input type of \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast\), since the subtype can always be weakened to its supertype by subsumption. Inversely, valid instruction sequences can also freely be decomposed, that is, splitting them anywhere produces two instruction sequences that are both valid. Theorem (Decomposition). If an instruction sequence \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\) that is valid with type \([t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x^\ast} [t_2^\ast]\) (i.e., \(C \href{../valid/instructions.html#valid-instrs}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : [t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x^\ast} [t_2^\ast]\)) is split into two instruction sequences \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast\) and \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_2^\ast\) at any point (i.e., \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast = \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast\;\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_2^\ast\)), then these are separately valid with some types \([t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x_1^\ast} [t^\ast]\) and \([t^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x_2^\ast} [t_2^\ast]\), respectively (i.e., \(C \href{../valid/instructions.html#valid-instrs}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast : [t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x_1^\ast} [t^\ast]\) and \(C \href{../valid/instructions.html#valid-instrs}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast : [t^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x_2^\ast} [t_2^\ast]\)), where \(x^\ast = x_1^\ast\;x_2^\ast\). Note This property holds because validation is required even for unreachable code. Without that, \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_2^\ast\) might not be valid in isolation.
©2017-2025, WebAssembly Community Group.
|
| You are visitor 01402503 — GeezerVison does not store the pages you look up. Best viewed with Netscape Navigator 4.7 or Internet Explorer 6 at 800×600. No cookies required. |