No live values in context: \(\href{../valid/types.html#auxiliary-novalues}{\vdash^\mathsf{\mkern-20mu\neg v}}\href{../valid/conventions.html#syntax-tyctx}{\Gamma}\)
There must be no live values in \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{parent}}\).
Every type in \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{values}}\) must be of the form
\(\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}^\dagger\).
For each instance in \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}\), every extern
declaration which is not dead must have a descriptor which is not of
the form \(\href{../valid/types.html#syntax-eexterndesc}{\mathsf{value}}~\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\).
Then there are no live values in the context \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}\).
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\href{../valid/types.html#auxiliary-novalues}{\vdash^\mathsf{\mkern-20mu\neg v}}\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{parent}}\\
\forall i, \exists \href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}, \href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{values}}[i] = \href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}^\dagger\\
\begin{aligned}\forall i, \exists \overline{\href{../valid/types.html#syntax-eexterndeclad}{{\mathit{externdecl}_e^?}}_j},{}&\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{values}}[i] = \href{../valid/types.html#syntax-eexterndeclad}{{\mathit{externdecl}_e^?}}\\\land{}&{}\forall j, \neg \exists \href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}, \href{../valid/types.html#syntax-eexterndeclad}{{\mathit{externdecl}_e^?}}_j = \href{../valid/types.html#syntax-eexterndesc}{\mathsf{value}}~\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\\\end{aligned}\\
\end{array}
}{
\href{../valid/types.html#auxiliary-novalues}{\vdash^\mathsf{\mkern-20mu\neg v}} \href{../valid/conventions.html#syntax-tyctx}{\Gamma}
}\end{split}\]
Instantiate/export arguments: \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \vdash \href{../syntax/components.html#syntax-sortidx}{\mathit{sortidx}} : \href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e}\).
Core modules
If the type \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{modules}}[i]\) exists in the
context and is a subtype of \(\href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}\), then
\(\{\href{../syntax/components.html#syntax-sortidx}{\mathsf{sort}}~\href{../syntax/components.html#syntax-sort}{\mathsf{core}}~\href{../syntax/components.html#syntax-coresort}{\mathsf{module}}, \href{../syntax/components.html#syntax-sortidx}{\mathsf{idx}}~i\}\) is valid with respect
to extern descriptor \(\href{../valid/types.html#syntax-eexterndesc}{\mathsf{core\_module}}~\href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}\).
\[\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \vdash \href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{modules}}[i] \preccurlyeq \href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-siateed}{\vdash}} \{ \href{../syntax/components.html#syntax-sortidx}{\mathsf{sort}}~\href{../syntax/components.html#syntax-sort}{\mathsf{core}}~\href{../syntax/components.html#syntax-coresort}{\mathsf{module}}, \href{../syntax/components.html#syntax-sortidx}{\mathsf{idx}}~i \}
\mathrel{\href{../valid/components.html#elaborate-siateed}{:}} \href{../valid/types.html#syntax-eexterndesc}{\mathsf{core\_module}}~\href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}
}\]
Functions
If the type \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{funcs}}[i]\) exists in the context and is
a subtype of \(\href{../valid/types.html#syntax-efunctype}{\mathit{functype}_e}\), then \(\{\href{../syntax/components.html#syntax-sortidx}{\mathsf{sort}}~\href{../syntax/components.html#syntax-sort}{\mathsf{func}},
\href{../syntax/components.html#syntax-sortidx}{\mathsf{idx}}~i\}\) is valid with respect to extern descriptor
\(\href{../valid/types.html#syntax-eexterndesc}{\mathsf{func}}~\href{../valid/types.html#syntax-efunctype}{\mathit{functype}_e}\).
\[\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \vdash \href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{funcs}}[i] \preccurlyeq \href{../valid/types.html#syntax-efunctype}{\mathit{functype}_e}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-siateed}{\vdash}} \{ \href{../syntax/components.html#syntax-sortidx}{\mathsf{sort}}~\href{../syntax/components.html#syntax-sort}{\mathsf{func}}, \href{../syntax/components.html#syntax-sortidx}{\mathsf{idx}}~i \}
\mathrel{\href{../valid/components.html#elaborate-siateed}{:}} \href{../valid/types.html#syntax-eexterndesc}{\mathsf{func}}~\href{../valid/types.html#syntax-efunctype}{\mathit{functype}_e}
}\]
Values
If the type \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{values}}[i]\) exists in the context and is
a subtype of \(\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\)
And \(\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\) is well-formed.
Then \(\{ \href{../syntax/components.html#syntax-sortidx}{\mathsf{sort}}~\href{../syntax/components.html#syntax-sort}{\mathsf{value}}, \href{../syntax/components.html#syntax-sortidx}{\mathsf{idx}}~i \}\) is valid with respect
to extern descriptor \(\href{../valid/types.html#syntax-eexterndesc}{\mathsf{value}}~\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\).
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \vdash \href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{values}}[i] \preccurlyeq \href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\\
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-evt}{\vdash}} \href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}\\
\end{array}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-siateed}{\vdash}} \{ \href{../syntax/components.html#syntax-sortidx}{\mathsf{sort}}~\href{../syntax/components.html#syntax-sort}{\mathsf{value}}, \href{../syntax/components.html#syntax-sortidx}{\mathsf{idx}}~i \}
\mathrel{\href{../valid/components.html#elaborate-siateed}{:}} \href{../valid/types.html#syntax-eexterndesc}{\mathsf{value}}~\href{../valid/types.html#syntax-evaltype}{\mathit{valtype}_e}
}\end{split}\]
Types
If the type \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[i]\) exists in the context and is
a subtype of \(\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}\), then \(\{\href{../syntax/components.html#syntax-sortidx}{\mathsf{sort}}~\href{../syntax/components.html#syntax-sort}{\mathsf{type}},
\href{../syntax/components.html#syntax-sortidx}{\mathsf{idx}}~i\}\) is valid with respect to extern descriptor
\(\href{../valid/types.html#syntax-eexterndesc}{\mathsf{type}}~\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}\).
\[\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \vdash \href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}} \preccurlyeq \href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-siateed}{\vdash}} \{ \href{../syntax/components.html#syntax-sortidx}{\mathsf{sort}}~\href{../syntax/components.html#syntax-sort}{\mathsf{type}}, \href{../syntax/components.html#syntax-sortidx}{\mathsf{idx}}~i \}
\mathrel{\href{../valid/components.html#elaborate-siateed}{:}} \href{../valid/types.html#syntax-eexterndesc}{\mathsf{type}}~\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}
}\]
Instances
If the type \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}[i]\) exists in the context and
is a subtype of \(\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}\), then
\(\{\href{../syntax/components.html#syntax-sortidx}{\mathsf{sort}}~\href{../syntax/components.html#syntax-sort}{\mathsf{instance}}, \href{../syntax/components.html#syntax-sortidx}{\mathsf{idx}}~i\}\) is valid with respect to
extern descriptor \(\href{../valid/types.html#syntax-eexterndesc}{\mathsf{instance}}~\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}\).
\[\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \vdash \href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}[i] \preccurlyeq \href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-siateed}{\vdash}} \{ \href{../syntax/components.html#syntax-sortidx}{\mathsf{sort}}~\href{../syntax/components.html#syntax-sort}{\mathsf{instance}}, \href{../syntax/components.html#syntax-sortidx}{\mathsf{idx}}~i \}
\mathrel{\href{../valid/components.html#elaborate-siateed}{:}} \href{../valid/types.html#syntax-eexterndesc}{\mathsf{instance}}~\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}
}\]
Components
If the type \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{components}}[i]\) exists in the context
and is a subtype of \(\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}\), then
\(\{\href{../syntax/components.html#syntax-sortidx}{\mathsf{sort}}~\href{../syntax/components.html#syntax-sort}{\mathsf{component}}, \href{../syntax/components.html#syntax-sortidx}{\mathsf{idx}}~i\}\) is valid with respect to
extern descriptor \(\href{../valid/types.html#syntax-eexterndesc}{\mathsf{component}}~\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}\).
\[\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \vdash \href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{components}}[i] \preccurlyeq \href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-siateed}{\vdash}} \{ \href{../syntax/components.html#syntax-sortidx}{\mathsf{sort}}~\href{../syntax/components.html#syntax-sort}{\mathsf{component}}, \href{../syntax/components.html#syntax-sortidx}{\mathsf{idx}}~i \}
\mathrel{\href{../valid/components.html#elaborate-siateed}{:}} \href{../valid/types.html#syntax-eexterndesc}{\mathsf{component}}~\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}
}\]
Definitions
\(\href{../syntax/components.html#syntax-definition}{\mathsf{core\_module}}~\href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-module}{\mathit{core{:}}\mathit{module}}\)
The core module \(\href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-module}{\mathit{core{:}}\mathit{module}}\) must be valid (as per Core
WebAssembly) with respect to the elaborated core module type
\(\href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}\).
Then \(\href{../syntax/components.html#syntax-definition}{\mathsf{core\_module}}~\href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-module}{\mathit{core{:}}\mathit{module}}\) is valid with respect to the
empty component type, and sets \(\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{modules}}\) in the
context to the orginal \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{modules}}\) followed
by \(\href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}\).
\[\begin{split}\frac{
\vdash \href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-module}{\mathit{core{:}}\mathit{module}} : \href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e}
}{
\begin{aligned}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-cdatect}{\vdash}}{}&\href{../syntax/components.html#syntax-definition}{\mathsf{core\_module}}~\href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-module}{\mathit{core{:}}\mathit{module}}\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{:}}{}&\forall \varnothing. \varnothing \to \exists \varnothing. \varnothing\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{\dashv}}{}&\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \oplus \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{modules}}~\href{../valid/types.html#syntax-ecoremoduletype}{\mathit{core{:}moduletype}_e} \}\\
\end{aligned}
}\end{split}\]
\(\href{../syntax/components.html#syntax-definition}{\mathsf{core\_instance}}~\href{../syntax/components.html#syntax-coreinstance}{\mathsf{instantiate}}~\href{../syntax/components.html#syntax-coremoduleidx}{\mathit{core{:}moduleidx}}~\overline{\href{../syntax/components.html#syntax-coreinstantiatearg}{\mathit{core{:}instantiatearg}}_i}\)
No two instantiate arguments may have identical \(\href{../syntax/components.html#syntax-coreinstantiatearg}{\mathsf{name}}\) members.
The type \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{modules}}[\href{../syntax/components.html#syntax-coremoduleidx}{\mathit{core{:}moduleidx}}]\) must
exist in the context, and for each \(\href{../syntax/types.html#syntax-coreimportdecl}{\mathit{core{:}importdecl}}\) in that type:
There must exist an instantiate argument whose \(\href{../syntax/components.html#syntax-coreinstantiatearg}{\mathsf{name}}\)
member matches its \(\href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-import}{\def\mathdef81#1{\mathsf{core{:}#1}}\mathdef81{module}}\) member, such that:
If the argument’s \(\href{../syntax/components.html#syntax-coreinstantiatearg}{\mathsf{instance}}\) member is
\(\href{../syntax/components.html#syntax-coreinstanceidx}{\mathit{core{:}instanceidx}}\), then the type
\(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{instances}}[\href{../syntax/components.html#syntax-coreinstanceidx}{\mathit{core{:}instanceidx}}]\) must
exist in the context, and furthermore, must contain an export
whose \(\href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-export}{\def\mathdef75#1{\mathsf{core{:}#1}}\mathdef75{name}}\) member matches the import declarations
\(\href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-import}{\def\mathdef82#1{\mathsf{core{:}#1}}\mathdef82{name}}\) member, and whose \(\href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-export}{\def\mathdef76#1{\mathsf{core{:}#1}}\mathdef76{desc}}\) member
is a subtype of the import declaration’s \(\href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-import}{\def\mathdef83#1{\mathsf{core{:}#1}}\mathdef83{desc}}\) member.
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{modules}}[\href{../syntax/components.html#syntax-coremoduleidx}{\mathit{core{:}moduleidx}}] = \overline{\href{../syntax/types.html#syntax-coreimportdecl}{\mathit{core{:}importdecl}}_j} \to \overline{\href{../valid/types.html#syntax-ecoreinstancetype}{\mathit{core{:}instancetype}_e}}\\
\begin{aligned}
\forall j, \exists i,&\href{../syntax/components.html#syntax-coreinstantiatearg}{\mathit{core{:}instantiatearg}}_i.\href{../syntax/components.html#syntax-coreinstantiatearg}{\mathsf{name}} = \href{../syntax/types.html#syntax-coreimportdecl}{\mathit{core{:}importdecl}}_j.\href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-import}{\def\mathdef81#1{\mathsf{core{:}#1}}\mathdef81{module}}\\
\land{}& \href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{instances}}[\href{../syntax/components.html#syntax-coreinstantiatearg}{\mathit{core{:}instantiatearg}}_i.\href{../syntax/components.html#syntax-coreinstantiatearg}{\mathsf{instance}}] = \overline{\href{../syntax/types.html#syntax-coreexportdecl}{\mathit{core{:}exportdecl}}_l}\\
\land{}& {\begin{aligned}[t]
\exists l,&\href{../syntax/types.html#syntax-coreexportdecl}{\mathit{core{:}exportdecl}}_l.\href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-export}{\def\mathdef75#1{\mathsf{core{:}#1}}\mathdef75{name}} = \href{../syntax/types.html#syntax-coreimportdecl}{\mathit{core{:}importdecl}}_j.\href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-import}{\def\mathdef82#1{\mathsf{core{:}#1}}\mathdef82{name}}\\
\land{}&\href{../syntax/types.html#syntax-coreexportdecl}{\mathit{core{:}exportdecl}}_l.\href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-export}{\def\mathdef76#1{\mathsf{core{:}#1}}\mathdef76{desc}} \preccurlyeq \href{../syntax/types.html#syntax-coreimportdecl}{\mathit{core{:}importdecl}}_j.\href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-import}{\def\mathdef83#1{\mathsf{core{:}#1}}\mathdef83{desc}}\\
\end{aligned}}
\end{aligned}\\
\forall i,\forall i', \href{../syntax/components.html#syntax-coreinstantiatearg}{\mathit{core{:}instantiatearg}}_i.\href{../syntax/components.html#syntax-coreinstantiatearg}{\mathsf{name}} = \href{../syntax/components.html#syntax-coreinstantiatearg}{\mathit{core{:}instantiatearg}}_{i'}.\href{../syntax/components.html#syntax-coreinstantiatearg}{\mathsf{name}} \Rightarrow i = i'\\
\end{array}
}{
\begin{aligned}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-cdatect}{\vdash}}{}&\href{../syntax/components.html#syntax-definition}{\mathsf{core\_instance}}~\href{../syntax/components.html#syntax-coreinstance}{\mathsf{instantiate}}~\href{../syntax/components.html#syntax-coremoduleidx}{\mathit{core{:}moduleidx}}~\overline{\href{../syntax/components.html#syntax-coreinstantiatearg}{\mathit{core{:}instantiatearg}}_i}\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{:}}{}&\forall\varnothing.\varnothing \to \exists\varnothing.\varnothing\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{\dashv}}{}&\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \oplus \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{instances}}~\href{../valid/types.html#syntax-ecoreinstancetype}{\mathit{core{:}instancetype}_e} \}
\end{aligned}
}\end{split}\]
\(\href{../syntax/components.html#syntax-definition}{\mathsf{core\_instance}}~\href{../syntax/components.html#syntax-coreinstance}{\mathsf{exports}}~\overline{\{\href{../syntax/components.html#syntax-coreexport}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}_i, \href{../syntax/components.html#syntax-coreexport}{\mathsf{def}}~\href{../syntax/components.html#syntax-coresortidx}{\mathit{core{:}sortidx}}_i \}}\)
Each \(\href{../syntax/values.html#syntax-name}{\mathit{name}}_i\) must be distinct.
Each \(\href{../syntax/components.html#syntax-coresortidx}{\mathit{core{:}sortidx}}_i\) must be valid with respect to some
\(\href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-importdesc}{\mathit{core{:}}\mathit{importdesc}}_i\).
Then \(\href{../syntax/components.html#syntax-definition}{\mathsf{core\_instance}}~\href{../syntax/components.html#syntax-coreinstance}{\mathsf{exports}}~\overline{\{\href{../syntax/components.html#syntax-coreexport}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}_i,
\href{../syntax/components.html#syntax-coreexport}{\mathsf{def}}~\href{../syntax/components.html#syntax-coresortidx}{\mathit{core{:}sortidx}}_i \}}\) is valid with respect to the empty module
type, and sets \(\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{instances}}\) in the context to the
original \(\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{instances}}\) followed by
\(\overline{\{ \href{../syntax/types.html#syntax-coreexportdecl}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}_i,
\href{../syntax/types.html#syntax-coreexportdecl}{\mathsf{desc}}~\href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-importdesc}{\mathit{core{:}}\mathit{importdesc}}_i\}}\).
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\forall i, \href{../valid/conventions.html#syntax-tyctx}{\Gamma} \vdash \href{../syntax/components.html#syntax-coresortidx}{\mathit{core{:}sortidx}}_i : \href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-importdesc}{\mathit{core{:}}\mathit{importdesc}}_i\\
\forall i j, \href{../syntax/values.html#syntax-name}{\mathit{name}}_i = \href{../syntax/values.html#syntax-name}{\mathit{name}}_j \Rightarrow i = j
\end{array}
}{
\begin{aligned}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-cdatect}{\vdash}}{}& \href{../syntax/components.html#syntax-definition}{\mathsf{core\_instance}}~\href{../syntax/components.html#syntax-coreinstance}{\mathsf{exports}}~\overline{\{\href{../syntax/components.html#syntax-coreexport}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}_i, \href{../syntax/components.html#syntax-coreexport}{\mathsf{def}}~\href{../syntax/components.html#syntax-coresortidx}{\mathit{core{:}sortidx}}_i \}}\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{:}}{}& \forall\varnothing.\varnothing \to \exists\varnothing.\varnothing\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{\dashv}}{}& \href{../valid/conventions.html#syntax-tyctx}{\Gamma} \oplus \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{instances}}~\overline{\{ \href{../syntax/types.html#syntax-coreexportdecl}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}_i, \href{../syntax/types.html#syntax-coreexportdecl}{\mathsf{desc}}~\href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-importdesc}{\mathit{core{:}}\mathit{importdesc}}_i\}} \}\\
\end{aligned}
}\end{split}\]
\(\href{../syntax/components.html#syntax-definition}{\mathsf{core\_type}}~\href{../syntax/types.html#syntax-coredeftype}{\mathit{core{:}deftype}}\)
The type \(\href{../syntax/types.html#syntax-coredeftype}{\mathit{core{:}deftype}}\) must elaborate to some \(\href{../valid/types.html#syntax-ecoredeftype}{\mathit{core{:}deftype}_e}\).
Then the definition \(\href{../syntax/components.html#syntax-definition}{\mathsf{core\_type}}~\href{../syntax/types.html#syntax-coredeftype}{\mathit{core{:}deftype}}\) is valid with
respect to the empty module type, and sets \(\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{types}}\)
in the context to the original \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{types}}\)
followed by \(\href{../valid/types.html#syntax-ecoredeftype}{\mathit{core{:}deftype}_e}\).
\[\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \vdash \href{../syntax/types.html#syntax-coredeftype}{\mathit{core{:}deftype}} \leadsto \href{../valid/types.html#syntax-ecoredeftype}{\mathit{core{:}deftype}_e}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-cdatect}{\vdash}} \href{../syntax/components.html#syntax-definition}{\mathsf{core\_type}}~\href{../syntax/types.html#syntax-coredeftype}{\mathit{core{:}deftype}}
\mathrel{\href{../valid/components.html#elaborate-cdatect}{:}} \forall\varnothing.\varnothing \to \exists\varnothing.\varnothing
\mathrel{\href{../valid/components.html#elaborate-cdatect}{\dashv}} \href{../valid/conventions.html#syntax-tyctx}{\Gamma} \oplus \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{types}}~\href{../valid/types.html#syntax-ecoredeftype}{\mathit{core{:}deftype}_e} \}
}\]
\(\href{../syntax/components.html#syntax-definition}{\mathsf{component}}~\href{../syntax/components.html#syntax-component}{\mathit{component}}\)
It must be possible to split the context \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}\) such that
the component \(\href{../syntax/components.html#syntax-component}{\mathit{component}}\) is valid for some type
\(\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}\) in the first portion of the context
Then the definition \(\href{../syntax/components.html#syntax-definition}{\mathsf{component}}~\href{../syntax/components.html#syntax-component}{\mathit{component}}\) is valid with
respect to the empty component type, and sets the context to the
second portion of the aforementioned split of the context, further
updated by setting \(\href{../valid/conventions.html#syntax-tyctx}{\mathsf{components}}\) to the original
\(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}_2.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{components}}\) followed by \(\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}\).
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} = \href{../valid/conventions.html#syntax-tyctx}{\Gamma}_1 \boxplus \href{../valid/conventions.html#syntax-tyctx}{\Gamma}_2\\
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}_1 \mathrel{\href{../valid/components.html#elaborate-catect}{\vdash}} \href{../syntax/components.html#syntax-component}{\mathit{component}} \mathrel{\href{../valid/components.html#elaborate-catect}{:}} \href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e}\\
\end{array}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-cdatect}{\vdash}} \href{../syntax/components.html#syntax-component}{\mathit{component}}
\mathrel{\href{../valid/components.html#elaborate-cdatect}{:}} \forall\varnothing.\varnothing \to \exists\varnothing.\varnothing
\mathrel{\href{../valid/components.html#elaborate-cdatect}{\dashv}} \href{../valid/conventions.html#syntax-tyctx}{\Gamma}_2 \oplus \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{components}}~\href{../valid/types.html#syntax-ecomponenttype}{\mathit{componenttype}_e} \}
}\end{split}\]
\(\href{../syntax/components.html#syntax-definition}{\mathsf{instance}}~\href{../syntax/components.html#syntax-instance}{\mathsf{instantiate}}~\href{../syntax/components.html#syntax-componentidx}{\mathit{componentidx}}~\overline{\href{../syntax/components.html#syntax-instantiatearg}{\mathit{instantiatearg}}_i}\)
The type \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{components}}[\href{../syntax/components.html#syntax-componentidx}{\mathit{componentidx}}]\) must exist in
the context, and for each \(\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}\) in that type:
Then
\(\href{../syntax/components.html#syntax-definition}{\mathsf{instance}}~\href{../syntax/components.html#syntax-instance}{\mathsf{instantiate}}~\href{../syntax/components.html#syntax-componentidx}{\mathit{componentidx}}~\overline{\href{../syntax/components.html#syntax-instantiatearg}{\mathit{instantiatearg}}_i}\)
is valid with respect to the empty module type, and sets
\(\href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}\) in the context to the original
\(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}\) followed by \(\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}\) of
\(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{components}}[\href{../syntax/components.html#syntax-componentidx}{\mathit{componentidx}}]\), and marks as dead in the
context any values present in \(\overline{\href{../syntax/components.html#syntax-instantiatearg}{\mathit{instantiatearg}}_i}\).
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{components}}[\href{../syntax/components.html#syntax-componentidx}{\mathit{componentidx}}] = \forall\overline{\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}_j}.\overline{{\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}}_k} \to \href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}\\
\forall j, \exists {\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}}_j, {\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}}_j \preccurlyeq \href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}_j\\
\overline{\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}'}_k\to\exists\overline{\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}'_o}\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}' = (\overline{{\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}}_k} \to \href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e})[\overline{{\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}}_j/\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}_j}]\\
\begin{aligned}
\forall k, \exists i, &\href{../syntax/components.html#syntax-instantiatearg}{\mathit{instantiatearg}}_i.\href{../syntax/components.html#syntax-instantiatearg}{\mathsf{name}} = {\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}'}_k.\href{../valid/types.html#syntax-eexportdecl}{\mathsf{name}}\\\land{}&\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-siateed}{\vdash}} \href{../syntax/components.html#syntax-instantiatearg}{\mathit{instantiatearg}}_i.\href{../syntax/components.html#syntax-instantiatearg}{\mathsf{arg}} \mathrel{\href{../valid/components.html#elaborate-siateed}{:}} {\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}'}_k.\href{../valid/types.html#syntax-eexportdecl}{\mathsf{desc}}
\end{aligned}\\
\forall l, \href{../valid/types.html#syntax-evaltypead}{{\mathit{valtype}_e^?}}_l = \begin{cases}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{values}}[l]^\dagger&\text{if }\begin{aligned}\exists i,{}&\href{../syntax/components.html#syntax-instantiatearg}{\mathit{instantiatearg}}_i.\href{../syntax/components.html#syntax-instantiatearg}{\mathsf{arg}}.\href{../syntax/components.html#syntax-sortidx}{\mathsf{sort}} = \href{../syntax/components.html#syntax-sort}{\mathsf{value}}\\\land{}&\href{../syntax/components.html#syntax-instantiatearg}{\mathit{instantiatearg}}_i.\href{../syntax/components.html#syntax-instantiatearg}{\mathsf{arg}}.\href{../syntax/components.html#syntax-sortidx}{\mathsf{idx}} = k\\\end{aligned}\\
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{values}}[l]&\text{otherwise}\\
\end{cases}\\
\forall m, {\href{../valid/types.html#syntax-einstancetypead}{{\mathit{instancetype}_e^?}}}_m = \begin{cases}
\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}'&\text{if }m = \def\mathdef452#1{\lVert#1\rVert}\mathdef452{\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}}\\
\exists\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast.\overline{\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}^\dagger}_n &\text{if }
\begin{aligned}
\exists i,{}&\href{../syntax/components.html#syntax-instantiatearg}{\mathit{instantiatearg}}_i.\href{../syntax/components.html#syntax-instantiatearg}{\mathsf{arg}}.\href{../syntax/components.html#syntax-sortidx}{\mathsf{sort}} = \href{../syntax/components.html#syntax-sort}{\mathsf{component}}\\
\land{}&\href{../syntax/components.html#syntax-instantiatearg}{\mathit{instantiatearg}}_i.\href{../syntax/components.html#syntax-instantiatearg}{\mathsf{arg}}.\href{../syntax/components.html#syntax-sortidx}{\mathsf{idx}} = m\\
\land{}&\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}[m] = \exists\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast. \overline{\href{../valid/types.html#syntax-eexterndeclad}{{\mathit{externdecl}_e^?}}_n}\\
\end{aligned}\\
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}[m] & \text{otherwise}\\
\end{cases}
\end{array}
}{
\begin{aligned}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-cdatect}{\vdash}}{}&\href{../syntax/components.html#syntax-definition}{\mathsf{instance}}~\href{../syntax/components.html#syntax-instance}{\mathsf{instantiate}}~\href{../syntax/components.html#syntax-componentidx}{\mathit{componentidx}}~\overline{\href{../syntax/components.html#syntax-instantiatearg}{\mathit{instantiatearg}}_i}\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{:}}{}&\forall\varnothing.\varnothing \to \exists\varnothing.\varnothing\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{\dashv}}{}&\href{../valid/conventions.html#syntax-tyctx}{\Gamma}' \ominus \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{values}}, \href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}} \} \oplus \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{uvars}}~\overline{\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}'_o}, \href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}~\overline{\href{../valid/types.html#syntax-einstancetypead}{{\mathit{instancetype}_e^?}}}_m, \href{../valid/conventions.html#syntax-tyctx}{\mathsf{values}}~\overline{\href{../valid/types.html#syntax-evaltypead}{{\mathit{valtype}_e^?}}_l} \}\\
\end{aligned}
}\end{split}\]
\(\href{../syntax/components.html#syntax-definition}{\mathsf{instance}}~\href{../syntax/components.html#syntax-instance}{\mathsf{exports}}~\overline{\{ \href{../syntax/components.html#syntax-export}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}_i, \href{../syntax/components.html#syntax-export}{\mathsf{def}}~\href{../syntax/components.html#syntax-sortidx}{\mathit{sortidx}}_i \}}\)
Each \(\href{../syntax/values.html#syntax-name}{\mathit{name}}_i\) must be distinct.
Each \(\href{../syntax/components.html#syntax-sortidx}{\mathit{sortidx}}_i\) must be valid with respect to some
\({\href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e}}_i\).
Then \(\href{../syntax/components.html#syntax-definition}{\mathsf{instance}}~\href{../syntax/components.html#syntax-instance}{\mathsf{exports}}~\overline{\{ \href{../syntax/components.html#syntax-export}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}_i,
\href{../syntax/components.html#syntax-export}{\mathsf{def}}~\href{../syntax/components.html#syntax-sortidx}{\mathit{sortidx}}_i \}}\) is valid with respect to the empty module
type, and sets \(\href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}\) in the context to the original
\(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}\) followed by \(\href{../valid/types.html#auxiliary-ifinalize}{\langle\mkern-5mu\langle}
\overline{\exists(\Gamma.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{evars}}). \href{../valid/types.html#syntax-eexportdecl}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}_i,
\href{../valid/types.html#syntax-eexportdecl}{\mathsf{desc}}~{\href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e}}_i}\href{../valid/types.html#auxiliary-ifinalize}{\rangle\mkern-5mu\rangle}\), and marks as dead in the
context any values present in \(\overline{\href{../syntax/components.html#syntax-sortidx}{\mathit{sortidx}}_i}\).
TODO: What is the right way to choose which type variables to put
into the existential here?
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\forall i, \href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-siateed}{\vdash}} \href{../syntax/components.html#syntax-sortidx}{\mathit{sortidx}}_i \mathrel{\href{../valid/components.html#elaborate-siateed}{:}} {\href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e}}_i\\
\forall i j, \href{../syntax/values.html#syntax-name}{\mathit{name}}_i = \href{../syntax/values.html#syntax-name}{\mathit{name}}_j \Rightarrow i = j\\
\forall j, \href{../valid/types.html#syntax-evaltypead}{{\mathit{valtype}_e^?}}_j = \begin{cases}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{values}}[j]^\dagger&\text{if }\begin{aligned}\exists i,{}&\href{../syntax/components.html#syntax-sortidx}{\mathit{sortidx}}_i.\href{../syntax/components.html#syntax-sortidx}{\mathsf{sort}} = \href{../syntax/components.html#syntax-sort}{\mathsf{value}}\\\land{}&\href{../syntax/components.html#syntax-sortidx}{\mathit{sortidx}}_i.\href{../syntax/components.html#syntax-sortidx}{\mathsf{idx}} = j\\\end{aligned}\\
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{values}}[j]&\text{otherwise}\\
\end{cases}\\
\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e} = \href{../valid/types.html#auxiliary-ifinalize}{\langle\mkern-5mu\langle}\exists(\Gamma.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{evars}}).\overline{ \href{../valid/types.html#syntax-eexportdecl}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}_i, \href{../valid/types.html#syntax-eexportdecl}{\mathsf{desc}}~{\href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e}}_i}\href{../valid/types.html#auxiliary-ifinalize}{\rangle\mkern-5mu\rangle}\\
\forall k, \href{../valid/types.html#syntax-einstancetypead}{{\mathit{instancetype}_e^?}}_k = \begin{cases}
\href{../valid/types.html#syntax-einstancetype}{\mathit{instancetype}_e}&\text{if } k = \def\mathdef453#1{\lVert#1\rVert}\mathdef453{\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}}\\
\exists\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast.\overline{{\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}^\dagger}_l}&\text{if }
\begin{aligned}
\exists i,{}&\href{../syntax/components.html#syntax-sortidx}{\mathit{sortidx}}_i.\href{../syntax/components.html#syntax-sortidx}{\mathsf{sort}} = \href{../syntax/components.html#syntax-sort}{\mathsf{instance}}\\
\land{}&\href{../syntax/components.html#syntax-sortidx}{\mathit{sortidx}}_i.\href{../syntax/components.html#syntax-sortidx}{\mathsf{idx}} = k\\
\land{}&\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}[k] = \forall\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast. \overline{\href{../valid/types.html#syntax-eexterndeclad}{{\mathit{externdecl}_e^?}}_l}\\
\end{aligned}\\
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}[k]&\text{otherwise}
\end{cases}
\end{array}
}{
\begin{aligned}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-cdatect}{\vdash}}{}& \href{../syntax/components.html#syntax-definition}{\mathsf{instance}}~\href{../syntax/components.html#syntax-instance}{\mathsf{exports}}~\overline{\{ \href{../syntax/components.html#syntax-export}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}_i, \href{../syntax/components.html#syntax-export}{\mathsf{def}}~\href{../syntax/components.html#syntax-sortidx}{\mathit{sortidx}}_i \}}\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{:}}{}& \forall\varnothing.\varnothing \to \exists\varnothing.\varnothing\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{\dashv}}{}& \href{../valid/conventions.html#syntax-tyctx}{\Gamma}\ominus\{\href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}},\href{../valid/conventions.html#syntax-tyctx}{\mathsf{values}}\} \oplus \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}~\overline{\href{../valid/types.html#syntax-einstancetypead}{{\mathit{instancetype}_e^?}}_k},\href{../valid/conventions.html#syntax-tyctx}{\mathsf{values}}~\overline{\href{../valid/types.html#syntax-evaltypead}{{\mathit{valtype}_e^?}}_j} \}
\end{aligned}
}\end{split}\]
\(\href{../syntax/components.html#syntax-definition}{\mathsf{alias}}~\{ \href{../syntax/types.html#syntax-alias}{\mathsf{sort}}~\href{../syntax/components.html#syntax-sort}{\mathit{sort}}, \href{../syntax/types.html#syntax-alias}{\mathsf{target}}~\href{../syntax/components.html#syntax-aliastarget}{\mathsf{export}}~\href{../syntax/components.html#syntax-instanceidx}{\mathit{instanceidx}}~\href{../syntax/values.html#syntax-name}{\mathit{name}} \}\)
This rule applies of \(\href{../syntax/components.html#syntax-sort}{\mathit{sort}} \neq \href{../syntax/components.html#syntax-sort}{\mathsf{instance}}\).
The type \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}[\href{../syntax/components.html#syntax-instanceidx}{\mathit{instanceidx}}]\) must exist in the
context.
Some extern descriptor with a matching \(\href{../syntax/values.html#syntax-name}{\mathit{name}}\) and some desc
\(\href{../valid/types.html#syntax-desc}{\mathit{desc}}\) must exist within \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}[\href{../syntax/components.html#syntax-instanceidx}{\mathit{instanceidx}}]\).
Then \(\href{../syntax/components.html#syntax-definition}{\mathsf{alias}}~\{ \href{../syntax/types.html#syntax-alias}{\mathsf{sort}}~\href{../syntax/components.html#syntax-sort}{\mathit{sort}},
\href{../syntax/types.html#syntax-alias}{\mathsf{target}}~\href{../syntax/components.html#syntax-aliastarget}{\mathsf{export}}~\href{../syntax/components.html#syntax-instanceidx}{\mathit{instanceidx}}~\href{../syntax/values.html#syntax-name}{\mathit{name}} \}\) is valid with respect to
the empty component type, and sets \(\mathrm{index\_space}(\href{../syntax/components.html#syntax-sort}{\mathit{sort}})\)
to the original \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\mathrm{index\_space}(\href{../syntax/components.html#syntax-sort}{\mathit{sort}})\) followed by
\(\href{../valid/types.html#syntax-desc}{\mathit{desc}}\).
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}[\href{../syntax/components.html#syntax-instanceidx}{\mathit{instanceidx}}] = \overline{{\href{../valid/types.html#syntax-eexterndeclad}{{\mathit{externdecl}_e^?}}}_i}\\
\exists i, {\href{../valid/types.html#syntax-eexterndeclad}{{\mathit{externdecl}_e^?}}}_i.\href{../valid/types.html#syntax-eexportdecl}{\mathsf{name}} = \href{../syntax/values.html#syntax-name}{\mathit{name}}\\
\forall j, {\href{../valid/types.html#syntax-eexterndeclad}{{\mathit{externdecl}_e^?}}'}_j = \begin{cases}
{\href{../valid/types.html#syntax-eexterndeclad}{{\mathit{externdecl}_e^?}}}_j^\dagger&\text{if } \href{../syntax/components.html#syntax-sort}{\mathit{sort}} = \href{../syntax/components.html#syntax-sort}{\mathsf{value}} \land j = i\\
{\href{../valid/types.html#syntax-eexterndeclad}{{\mathit{externdecl}_e^?}}}_j&\text{otherwise}\\
\end{cases}\\
\end{array}
}{
\begin{aligned}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-cdatect}{\vdash}}{}& \href{../syntax/components.html#syntax-definition}{\mathsf{alias}}~\{ \href{../syntax/types.html#syntax-alias}{\mathsf{sort}}~\href{../syntax/components.html#syntax-sort}{\mathit{sort}}, \href{../syntax/types.html#syntax-alias}{\mathsf{target}}~\href{../syntax/components.html#syntax-aliastarget}{\mathsf{export}}~\href{../syntax/components.html#syntax-instanceidx}{\mathit{instanceidx}}~\href{../syntax/values.html#syntax-name}{\mathit{name}} \}\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{:}}{}& \forall\varnothing.\varnothing \to \exists\varnothing.\varnothing\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{\dashv}}{}& \href{../valid/conventions.html#syntax-tyctx}{\Gamma} \oplus \{ \mathrm{index\_space}(\href{../syntax/components.html#syntax-sort}{\mathit{sort}})~{\href{../valid/types.html#syntax-eexterndeclad}{{\mathit{externdecl}_e^?}}}_i.\href{../valid/types.html#syntax-eexportdecl}{\mathsf{desc}}, \href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}[i]~\overline{{\href{../valid/types.html#syntax-eexterndeclad}{{\mathit{externdecl}_e^?}}'}_j} \}\\
\end{aligned}
}\end{split}\]
\(\href{../syntax/components.html#syntax-definition}{\mathsf{alias}}~\{ \href{../syntax/types.html#syntax-alias}{\mathsf{sort}}~\href{../syntax/components.html#syntax-sort}{\mathsf{instance}}, \href{../syntax/types.html#syntax-alias}{\mathsf{target}}~\href{../syntax/components.html#syntax-aliastarget}{\mathsf{export}}~\href{../syntax/components.html#syntax-instanceidx}{\mathit{instanceidx}}~\href{../syntax/values.html#syntax-name}{\mathit{name}} \}\)
The type \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}[\href{../syntax/components.html#syntax-instanceidx}{\mathit{instanceidx}}]\) must exist in the
context.
Some extern descriptor with a matching \(\href{../syntax/values.html#syntax-name}{\mathit{name}}\) and a
\(\href{../valid/types.html#syntax-desc}{\mathit{desc}}\) of the form
\(\href{../syntax/types.html#syntax-externdesc}{\mathsf{instance}}~\forall\overline{\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}_l}.
\overline{{\href{../valid/types.html#syntax-eexterndeclad}{{\mathit{externdecl}_e^?}}}_m}w\) must exist within
\(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}[\href{../syntax/components.html#syntax-instanceidx}{\mathit{instanceidx}}]\).
Then \(\href{../syntax/components.html#syntax-definition}{\mathsf{alias}}~\{ \href{../syntax/types.html#syntax-alias}{\mathsf{sort}}~\href{../syntax/components.html#syntax-sort}{\mathsf{instance}},
\href{../syntax/types.html#syntax-alias}{\mathsf{target}}~\href{../syntax/components.html#syntax-aliastarget}{\mathsf{export}}~\href{../syntax/components.html#syntax-instanceidx}{\mathit{instanceidx}}~\href{../syntax/values.html#syntax-name}{\mathit{name}} \}\) is valid with respect to
the empty component type, and sets \(\href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}\) to the
original \(\href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}\) followed by
:\(\overline{{\href{../valid/types.html#syntax-eexterndeclad}{{\mathit{externdecl}_e^?}}}_m}\), and sets \(\href{../valid/conventions.html#syntax-tyctx}{\mathsf{uvars}}\) to
the original \(\href{../valid/conventions.html#syntax-tyctx}{\mathsf{uvars}}\) followed by
\(\overline{\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}_l}\).
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}[\href{../syntax/components.html#syntax-instanceidx}{\mathit{instanceidx}}] = \overline{{\href{../valid/types.html#syntax-eexterndeclad}{{\mathit{externdecl}_e^?}}}_i}\\
\exists i, {\href{../valid/types.html#syntax-eexterndeclad}{{\mathit{externdecl}_e^?}}}_i.\href{../valid/types.html#syntax-eexportdecl}{\mathsf{name}} = \href{../syntax/values.html#syntax-name}{\mathit{name}}\\
{\href{../valid/types.html#syntax-eexterndeclad}{{\mathit{externdecl}_e^?}}}_i.\href{../valid/types.html#syntax-eexportdecl}{\mathsf{desc}} = \href{../syntax/types.html#syntax-externdesc}{\mathsf{instance}}~\forall\overline{\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}_l}.
\overline{{\href{../valid/types.html#syntax-eexterndeclad}{{\mathit{externdecl}_e^?}}}_m}\\
\forall j, {\href{../valid/types.html#syntax-eexterndeclad}{{\mathit{externdecl}_e^?}}'}_j = \begin{cases}
\forall\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast.\overline{{\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}}_k^\dagger}&
{\begin{aligned}
\text{if }&j = i\\
\land{}&\href{../valid/types.html#syntax-eexterndeclad}{{\mathit{externdecl}_e^?}} = \forall\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast.\overline{\href{../valid/types.html#syntax-eexterndeclad}{{\mathit{externdecl}_e^?}}_k}\\
\end{aligned}}\\
{\href{../valid/types.html#syntax-eexterndeclad}{{\mathit{externdecl}_e^?}}}_j&\text{otherwise}\\
\end{cases}\\
\end{array}
}{
\begin{aligned}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-cdatect}{\vdash}}{}& \href{../syntax/components.html#syntax-definition}{\mathsf{alias}}~\{ \href{../syntax/types.html#syntax-alias}{\mathsf{sort}}~\href{../syntax/components.html#syntax-sort}{\mathit{sort}}, \href{../syntax/types.html#syntax-alias}{\mathsf{target}}~\href{../syntax/components.html#syntax-aliastarget}{\mathsf{export}}~\href{../syntax/components.html#syntax-instanceidx}{\mathit{instanceidx}}~\href{../syntax/values.html#syntax-name}{\mathit{name}} \}\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{:}}{}& \forall\varnothing.\varnothing \to \exists\varnothing.\varnothing\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{\dashv}}{}& \href{../valid/conventions.html#syntax-tyctx}{\Gamma} \oplus \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{uvars}}~\overline{\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}_l} \href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}[i]~\overline{{\href{../valid/types.html#syntax-eexterndeclad}{{\mathit{externdecl}_e^?}}'}_j~\overline{{\href{../valid/types.html#syntax-eexterndeclad}{{\mathit{externdecl}_e^?}}}_m}} \}\\
\end{aligned}
}\end{split}\]
\(\href{../syntax/components.html#syntax-definition}{\mathsf{alias}}~\{ \href{../syntax/types.html#syntax-alias}{\mathsf{sort}}~\href{../syntax/components.html#syntax-sort}{\mathit{sort}}, \href{../syntax/types.html#syntax-alias}{\mathsf{target}}~\href{../syntax/components.html#syntax-aliastarget}{\mathsf{core\_export}}~\href{../syntax/components.html#syntax-coreinstanceidx}{\mathit{core{:}instanceidx}}~\href{../syntax/values.html#syntax-name}{\mathit{name}} \}\)
The type \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{instances}}[\href{../syntax/components.html#syntax-coreinstanceidx}{\mathit{core{:}instanceidx}}]\)
must exist in the context.
\(\href{../syntax/components.html#syntax-sort}{\mathit{sort}}\) must be \(\href{../syntax/components.html#syntax-sort}{\mathsf{core}}~\href{../syntax/components.html#syntax-coresort}{\mathit{core{:}sort}}\).
Some export declarator with a matching \(\href{../syntax/values.html#syntax-name}{\mathit{name}}\) and some desc
\(\href{../valid/types.html#syntax-desc}{\mathit{desc}}\) must exist within
\(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}[\href{../syntax/components.html#syntax-instanceidx}{\mathit{instanceidx}}]\).
Then \(\href{../syntax/components.html#syntax-definition}{\mathsf{alias}}~\{ \href{../syntax/types.html#syntax-alias}{\mathsf{sort}}~\href{../syntax/components.html#syntax-sort}{\mathit{sort}},
\href{../syntax/types.html#syntax-alias}{\mathsf{target}}~\href{../syntax/components.html#syntax-aliastarget}{\mathsf{core\_export}}~\href{../syntax/components.html#syntax-coreinstanceidx}{\mathit{core{:}instanceidx}}~\href{../syntax/values.html#syntax-name}{\mathit{name}} \}\) is valid with
respect to the empty component type, and sets
\(\mathrm{index\_space}(sort)\) to the original
\(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\mathrm{index\_space}(\href{../syntax/components.html#syntax-sort}{\mathit{sort}})\) followed by \(\href{../valid/types.html#syntax-desc}{\mathit{desc}}\).
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\href{../syntax/components.html#syntax-sort}{\mathit{sort}} = \href{../syntax/components.html#syntax-sort}{\mathsf{core}}~\href{../syntax/components.html#syntax-coresort}{\mathit{core{:}sort}}\\
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{instances}}[\href{../syntax/components.html#syntax-coreinstanceidx}{\mathit{core{:}instanceidx}}] = \overline{\href{../syntax/types.html#syntax-coreexportdecl}{\mathit{core{:}exportdecl}}_i}\\
{\href{../syntax/types.html#syntax-coreexportdecl}{\mathit{core{:}exportdecl}}}_i.\href{../syntax/types.html#syntax-coreexportdecl}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}\\
\end{array}
}{
\begin{aligned}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-cdatect}{\vdash}}{}& \href{../syntax/components.html#syntax-definition}{\mathsf{alias}}~\{ \href{../syntax/types.html#syntax-alias}{\mathsf{sort}}~\href{../syntax/components.html#syntax-sort}{\mathit{sort}}, \href{../syntax/types.html#syntax-alias}{\mathsf{target}}~\href{../syntax/components.html#syntax-aliastarget}{\mathsf{core\_export}}~\href{../syntax/components.html#syntax-coreinstanceidx}{\mathit{core{:}instanceidx}}~\href{../syntax/values.html#syntax-name}{\mathit{name}} \}\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{:}}{}& \forall\varnothing.\varnothing \to \exists\varnothing.\varnothing\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{\dashv}}{}& \href{../valid/conventions.html#syntax-tyctx}{\Gamma} \oplus \{ \mathrm{index\_space}(\href{../syntax/components.html#syntax-sort}{\mathit{sort}})~{\href{../syntax/types.html#syntax-coreexportdecl}{\mathit{core{:}exportdecl}}}_i.\href{../syntax/types.html#syntax-coreexportdecl}{\mathsf{desc}} \}
\end{aligned}
}\end{split}\]
\(\href{../syntax/components.html#syntax-definition}{\mathsf{alias}}~\{ \href{../syntax/types.html#syntax-alias}{\mathsf{sort}}~\href{../syntax/components.html#syntax-sort}{\mathit{sort}}, \href{../syntax/types.html#syntax-alias}{\mathsf{target}}~\href{../syntax/components.html#syntax-aliastarget}{\mathsf{outer}}~\href{../syntax/values.html#syntax-int}{\mathit{u32}}_o~\href{../syntax/values.html#syntax-int}{\mathit{u32}}_i \}\)
\(\href{../syntax/components.html#syntax-sort}{\mathit{sort}}\) must be one of \(\href{../syntax/components.html#syntax-sort}{\mathsf{component}}\),
\(\href{../syntax/components.html#syntax-sort}{\mathsf{core}}~\href{../syntax/components.html#syntax-coresort}{\mathsf{module}}\), \(\href{../syntax/components.html#syntax-sort}{\mathsf{type}}\), or
\(\href{../syntax/components.html#syntax-sort}{\mathsf{core}}~\href{../syntax/components.html#syntax-coresort}{\mathsf{type}}\).
\(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{parent}}[\href{../syntax/values.html#syntax-int}{\mathit{u32}}_o].\mathrm{index\_space}(\href{../syntax/components.html#syntax-sort}{\mathit{sort}})[\href{../syntax/values.html#syntax-int}{\mathit{u32}}_i]\) must
exist in the context.
If \(\href{../syntax/components.html#syntax-sort}{\mathit{sort}}\) is STYPE, then
\(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{parent}}[\href{../syntax/values.html#syntax-int}{\mathit{u32}}_o].\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/values.html#syntax-int}{\mathit{u32}}_i]\) must not be of the
form \(\href{../valid/types.html#syntax-edeftype}{\mathsf{resource}}~i\) for any \(i\).
Then \(\href{../syntax/components.html#syntax-definition}{\mathsf{alias}}~\{ \href{../syntax/types.html#syntax-alias}{\mathsf{sort}}~\href{../syntax/components.html#syntax-sort}{\mathit{sort}}, \href{../syntax/types.html#syntax-alias}{\mathsf{target}}~\href{../syntax/components.html#syntax-aliastarget}{\mathsf{outer}}~\href{../syntax/values.html#syntax-int}{\mathit{u32}}_o~\href{../syntax/values.html#syntax-int}{\mathit{u32}}_i
\}\) is valid with respect to the empty component type, and sets
\(\mathrm{index\_space}(\href{../syntax/components.html#syntax-sort}{\mathit{sort}})\) in the context to the original
\(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\mathrm{index\_space}(\href{../syntax/components.html#syntax-sort}{\mathit{sort}})\) followed by
\(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{parent}}[\href{../syntax/values.html#syntax-int}{\mathit{u32}}_o].\mathrm{index\_space}(\href{../syntax/components.html#syntax-sort}{\mathit{sort}})[\href{../syntax/values.html#syntax-int}{\mathit{u32}}_i]\).
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\href{../syntax/components.html#syntax-sort}{\mathit{sort}} \in \{ \href{../syntax/components.html#syntax-sort}{\mathsf{component}}, \href{../syntax/components.html#syntax-sort}{\mathsf{core}}~\href{../syntax/components.html#syntax-coresort}{\mathsf{module}}, \href{../syntax/components.html#syntax-sort}{\mathsf{type}}, \href{../syntax/components.html#syntax-sort}{\mathsf{core}}~\href{../syntax/components.html#syntax-coresort}{\mathsf{type}} \}\\
\href{../syntax/components.html#syntax-sort}{\mathit{sort}} = \href{../syntax/components.html#syntax-sort}{\mathsf{type}} \Rightarrow \forall i. \href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{parent}}[\href{../syntax/values.html#syntax-int}{\mathit{u32}}_o].\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/values.html#syntax-int}{\mathit{u32}}_i] \neq \href{../valid/types.html#syntax-edeftype}{\mathsf{resource}}~i\\
\end{array}
}{
\begin{aligned}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-cdatect}{\vdash}}{}& \href{../syntax/components.html#syntax-definition}{\mathsf{alias}}~\{ \href{../syntax/types.html#syntax-alias}{\mathsf{sort}}~\href{../syntax/components.html#syntax-sort}{\mathit{sort}}, \href{../syntax/types.html#syntax-alias}{\mathsf{target}}~\href{../syntax/components.html#syntax-aliastarget}{\mathsf{outer}}~\href{../syntax/values.html#syntax-int}{\mathit{u32}}_o~\href{../syntax/values.html#syntax-int}{\mathit{u32}}_i \}\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{:}}{}&\forall\varnothing.\varnothing \to \exists\varnothing.\varnothing\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{\dashv}}{}&\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \oplus \{ \mathrm{index\_space}(\href{../syntax/components.html#syntax-sort}{\mathit{sort}})~\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{parent}}[\href{../syntax/values.html#syntax-int}{\mathit{u32}}_o].\mathrm{index\_space}(sort)[\href{../syntax/values.html#syntax-int}{\mathit{u32}}_i] \}\\
\end{aligned}
}\end{split}\]
\(\href{../syntax/components.html#syntax-definition}{\mathsf{type}}~\href{../syntax/types.html#syntax-deftype}{\mathit{deftype}}\)
The type \(\href{../syntax/types.html#syntax-deftype}{\mathit{deftype}}\) must elaborate to some \(\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}\).
Then \(\href{../syntax/components.html#syntax-definition}{\mathsf{type}}~\href{../syntax/types.html#syntax-deftype}{\mathit{deftype}}\) is valid with respect to the empty
component type, and sets \(\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}\) in the context to the
original \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}\) followed by \(\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}\).
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-dttoedt}{\vdash}} \href{../syntax/types.html#syntax-deftype}{\mathit{deftype}} \mathrel{\href{../valid/types.html#elaborate-dttoedt}{\leadsto}} \href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}\\
\mathrm{fresh}(\alpha)\\
\end{array}
}{
\begin{aligned}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-cdatect}{\vdash}}{}&\href{../syntax/components.html#syntax-definition}{\mathsf{type}}~\href{../syntax/types.html#syntax-deftype}{\mathit{deftype}}\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{:}}{}&\forall\varnothing.\varnothing \to \varnothing\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{\dashv}}{}&\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \oplus \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}~\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e} \}\\
\end{aligned}
}\end{split}\]
\(\href{../syntax/components.html#syntax-definition}{\mathsf{type}}~\{ \href{../syntax/types.html#syntax-resourcetype}{\mathsf{rep}}~\mathtt{i32}, \href{../syntax/types.html#syntax-resourcetype}{\mathsf{dtor}}~\href{../syntax/components.html#syntax-funcidx}{\mathit{funcidx}} \}\)
\(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{funcs}}[\href{../syntax/components.html#syntax-funcidx}{\mathit{funcidx}}]\) must exist.
Then \(\href{../syntax/components.html#syntax-definition}{\mathsf{type}}~\{ \href{../syntax/types.html#syntax-resourcetype}{\mathsf{rep}}~\mathtt{i32}, \href{../syntax/types.html#syntax-resourcetype}{\mathsf{dtor}}~\href{../syntax/components.html#syntax-funcidx}{\mathit{funcidx}} \}\) is
valid with respect to the empty component type, and appends
\(\{ \href{../syntax/types.html#syntax-resourcetype}{\mathsf{rep}}~\mathtt{i32}, \href{../syntax/types.html#syntax-resourcetype}{\mathsf{dtor}}~\href{../syntax/components.html#syntax-funcidx}{\mathit{funcidx}} \}\) to
\(\href{../valid/conventions.html#syntax-tyctx}{\mathsf{rtypes}}\) in the context, and sets \(\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}\) in the
context to the original \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}\) followed by
\(\href{../valid/types.html#syntax-edeftype}{\mathsf{resource}}~\mathrm{length}(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{rtypes}})\).
\[\frac{
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}
\mathrel{\href{../valid/components.html#elaborate-cdatect}{\vdash}} \href{../syntax/components.html#syntax-definition}{\mathsf{type}}~\{ \href{../syntax/types.html#syntax-resourcetype}{\mathsf{rep}}~\mathtt{i32}, \href{../syntax/types.html#syntax-resourcetype}{\mathsf{dtor}}~\href{../syntax/components.html#syntax-funcidx}{\mathit{funcidx}} \}
\mathrel{\href{../valid/components.html#elaborate-cdatect}{:}} \forall \varnothing. \varnothing \to \varnothing
\mathrel{\href{../valid/components.html#elaborate-cdatect}{\dashv}} \href{../valid/conventions.html#syntax-tyctx}{\Gamma} \oplus \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{rtypes}}~\{ \href{../syntax/types.html#syntax-resourcetype}{\mathsf{rep}}~\mathtt{i32}, \href{../syntax/types.html#syntax-resourcetype}{\mathsf{dtor}}~\href{../syntax/components.html#syntax-funcidx}{\mathit{funcidx}} \}, \href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}~\href{../valid/types.html#syntax-edeftype}{\mathsf{resource}}~\mathrm{length}(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{rtypes}}) \}
}\]
\(\href{../syntax/components.html#syntax-definition}{\mathsf{canon}}~\href{../syntax/components.html#syntax-canon}{\mathsf{lift}}~\href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-funcidx}{\mathit{core{:}}\mathit{funcidx}}~\overline{\href{../syntax/components.html#syntax-canonopt}{\mathit{canonopt}}_i}~\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}\)
\(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}]\) must exist and be a
\(\href{../valid/types.html#syntax-efunctype}{\mathit{functype}_e}\).
\(\mathrm{canon\_lower\_type}(\href{../valid/types.html#syntax-efunctype}{\mathit{functype}_e}, \overline{\href{../syntax/components.html#syntax-canonopt}{\mathit{canonopt}}_i})\) must
be equal to \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{funcs}}[\href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-funcidx}{\mathit{core{:}}\mathit{funcidx}}]\).
Then
\(\href{../syntax/components.html#syntax-definition}{\mathsf{canon}}~\href{../syntax/components.html#syntax-canon}{\mathsf{lift}}~\href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-funcidx}{\mathit{core{:}}\mathit{funcidx}}~\overline{\href{../syntax/components.html#syntax-canonopt}{\mathit{canonopt}}_i}~\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}\)
is valid with respect to the empty component type, and sets
\(\href{../valid/conventions.html#syntax-tyctx}{\mathsf{funcs}}\) in the context to the original
\(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{funcs}}\) followed by \(\href{../valid/types.html#syntax-efunctype}{\mathit{functype}_e}\).
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}] = \href{../valid/types.html#syntax-efunctype}{\mathit{functype}_e}\\
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{funcs}}[\href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-funcidx}{\mathit{core{:}}\mathit{funcidx}}] = \mathrm{canon\_lower\_type}(\href{../valid/types.html#syntax-efunctype}{\mathit{functype}_e}, \overline{\href{../syntax/components.html#syntax-canonopt}{\mathit{canonopt}}_i})\\
\end{array}
}{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-cdatect}{\vdash}} \href{../syntax/components.html#syntax-definition}{\mathsf{canon}}~\href{../syntax/components.html#syntax-canon}{\mathsf{lift}}~\href{https://webassembly.github.io/spec/core/syntax/modules.html#syntax-funcidx}{\mathit{core{:}}\mathit{funcidx}}~\overline{\href{../syntax/components.html#syntax-canonopt}{\mathit{canonopt}}_i}~\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}
\mathrel{\href{../valid/components.html#elaborate-cdatect}{:}} \varnothing \to \varnothing
\mathrel{\href{../valid/components.html#elaborate-cdatect}{\dashv}} \href{../valid/conventions.html#syntax-tyctx}{\Gamma} \oplus \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{funcs}}~\href{../valid/types.html#syntax-efunctype}{\mathit{functype}_e} \}
}\end{split}\]
\(\href{../syntax/components.html#syntax-definition}{\mathsf{canon}}~\href{../syntax/components.html#syntax-canon}{\mathsf{lower}}~\href{../syntax/components.html#syntax-funcidx}{\mathit{funcidx}}~\overline{\href{../syntax/components.html#syntax-canonopt}{\mathit{canonopt}}_i}\)
The type \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{funcs}}[\href{../syntax/components.html#syntax-funcidx}{\mathit{funcidx}}]\) must exist in the context.
\(\mathrm{canon\_lower\_type}(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{funcs}}[\href{../syntax/components.html#syntax-funcidx}{\mathit{funcidx}}],
\overline{\href{../syntax/components.html#syntax-canonopt}{\mathit{canonopt}}_i})\) must be defined (to be some
\(\href{https://webassembly.github.io/spec/core/syntax/types.html#syntax-functype}{\mathit{core{:}}\mathit{functype}}\).
Then \(\href{../syntax/components.html#syntax-definition}{\mathsf{canon}}~\href{../syntax/components.html#syntax-canon}{\mathsf{lower}}~\href{../syntax/components.html#syntax-funcidx}{\mathit{funcidx}}~\overline{\href{../syntax/components.html#syntax-canonopt}{\mathit{canonopt}}_i}\) is
valid with respect to the empty component type, and sets
\(\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{funcs}}\) in the context to the original
\(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{funcs}}\) followed by that
\(\href{https://webassembly.github.io/spec/core/syntax/types.html#syntax-functype}{\mathit{core{:}}\mathit{functype}}\).
\[\begin{split}\frac{
}{
\begin{aligned}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-cdatect}{\vdash}}{}&\href{../syntax/components.html#syntax-definition}{\mathsf{canon}}~\href{../syntax/components.html#syntax-canon}{\mathsf{lower}}~\href{../syntax/components.html#syntax-funcidx}{\mathit{funcidx}}~\overline{\href{../syntax/components.html#syntax-canonopt}{\mathit{canonopt}}_i}\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{:}}{}&\forall\varnothing.\varnothing \to \exists\varnothing.\varnothing\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{\dashv}}{}&\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \oplus \{ \href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{core}}.\href{../valid/conventions.html#syntax-coretyctx}{\mathsf{funcs}}~\mathrm{canon\_lower\_type}(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{funcs}}[\href{../syntax/components.html#syntax-funcidx}{\mathit{funcidx}}], \overline{\href{../syntax/components.html#syntax-canonopt}{\mathit{canonopt}}_i}) \}\\
\end{aligned}
}\end{split}\]
\(\href{../syntax/components.html#syntax-definition}{\mathsf{start}}~\{ \href{../syntax/components.html#syntax-start}{\mathsf{func}}~\href{../syntax/components.html#syntax-funcidx}{\mathit{funcidx}}, \href{../syntax/components.html#syntax-start}{\mathsf{args}}~\overline{\href{../syntax/components.html#syntax-valueidx}{\mathit{valueidx}}_i} \}\)
The type \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{funcs}}[\href{../syntax/components.html#syntax-funcidx}{\mathit{funcidx}}]\) must be defined in the context.
The arguments \(\overline{\href{../syntax/components.html#syntax-valueidx}{\mathit{valueidx}}_i}\) must be valid with
respect to the parameter list of the function.
Then \(\href{../syntax/components.html#syntax-definition}{\mathsf{start}}~\{ \href{../syntax/components.html#syntax-start}{\mathsf{func}}~\href{../syntax/components.html#syntax-funcidx}{\mathit{funcidx}},
\href{../syntax/components.html#syntax-start}{\mathsf{args}}~\overline{\href{../syntax/components.html#syntax-valueidx}{\mathit{valueidx}}_i} \}\) is valid with respect to the empty
component type, and sets \(\href{../valid/conventions.html#syntax-tyctx}{\mathsf{values}}\) in the context to the
original \(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{values}}\) followed by the types of the
return values of the function.
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{funcs}}[\href{../syntax/components.html#syntax-funcidx}{\mathit{funcidx}}] = \href{../valid/types.html#syntax-eresulttype}{\mathit{resulttype}_e} \to \href{../valid/types.html#syntax-eresulttype}{\mathit{resulttype}_e}'\\
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-visatrt}{\vdash}} \overline{\href{../syntax/components.html#syntax-valueidx}{\mathit{valueidx}}_i} \mathrel{\href{../valid/components.html#elaborate-visatrt}{:}} \href{../valid/types.html#syntax-eresulttype}{\mathit{resulttype}_e}\\
n = \mathrm{length}(\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{values}})\\
\forall j, \href{../valid/types.html#syntax-evaltypead}{{\mathit{valtype}_e^?}}'_j = \begin{cases}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{values}}[j]^\dagger&
{\begin{aligned}
\text{if }\exists i\,\forall \href{../syntax/types.html#syntax-deftype}{\mathit{deftype}},{} & j < n \land j = \href{../syntax/components.html#syntax-valueidx}{\mathit{valueidx}}_i\\
\land {}&{\href{../valid/types.html#syntax-eresulttype}{\mathit{resulttype}_e}}_i.\href{../valid/types.html#syntax-eresulttype}{\mathsf{type}} \neq \href{../valid/types.html#syntax-evaltype2}{\mathsf{ref}}~\href{../valid/types.html#syntax-refscope}{\mathsf{call}}~\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}\\
\end{aligned}}\\
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{values}}[j]&\text{if }j <n\land j \notin \overline{\href{../syntax/components.html#syntax-valueidx}{\mathit{valueidx}}_i}\\
{\href{../valid/types.html#syntax-eresulttype}{\mathit{resulttype}_e}}'_{j-n}&\text{otherwise}\\
\end{cases}\\
\end{array}
}{
\begin{aligned}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-cdatect}{\vdash}}{}&\href{../syntax/components.html#syntax-definition}{\mathsf{start}}~\{ \href{../syntax/components.html#syntax-start}{\mathsf{func}}~\href{../syntax/components.html#syntax-funcidx}{\mathit{funcidx}}, \href{../syntax/components.html#syntax-start}{\mathsf{args}}~\overline{\href{../syntax/components.html#syntax-valueidx}{\mathit{valueidx}}_i} \}\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{:}}{}&\forall\varnothing.\varnothing \to \exists\varnothing.\varnothing\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{\dashv}}{}&\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \ominus \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{values}} \} \oplus \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{values}}~\overline{\href{../valid/types.html#syntax-evaltypead}{{\mathit{valtype}_e^?}}'_j} \}\\
\end{aligned}
}\end{split}\]
\(\href{../syntax/components.html#syntax-definition}{\mathsf{import}}~\{ \href{../syntax/types.html#syntax-importdecl}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../syntax/types.html#syntax-importdecl}{\mathsf{desc}}~\href{../syntax/types.html#syntax-externdesc}{\mathit{externdesc}} \}\)
The \(\href{../syntax/types.html#syntax-externdesc}{\mathit{externdesc}}\) must elaborate to some \(\forall\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast.\href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e}\).
Then the definition \(\href{../syntax/components.html#syntax-definition}{\mathsf{import}}~\{ \href{../syntax/types.html#syntax-importdecl}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}},
\href{../syntax/types.html#syntax-importdecl}{\mathsf{desc}}~\href{../syntax/types.html#syntax-externdesc}{\mathit{externdesc}} \}\) is valid with respect to the component type
whose export list is empty and whose import list is the singleton
containing \(\{ \href{../valid/types.html#syntax-eexportdecl}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../valid/types.html#syntax-eexportdecl}{\mathsf{desc}}~\href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e} \}\), and
updates the context with \(\href{../valid/types.html#syntax-eexportdecl}{\mathsf{desc}}\).
\[\begin{split}\frac{
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/types.html#elaborate-edtoeed}{\vdash}} \href{../syntax/types.html#syntax-externdesc}{\mathit{externdesc}} \mathrel{\href{../valid/types.html#elaborate-edtoeed}{\leadsto}} \forall\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast.\href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e}
}{
\begin{aligned}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-cdatect}{\vdash}}{}&\href{../syntax/components.html#syntax-definition}{\mathsf{import}}~\{ \href{../syntax/types.html#syntax-importdecl}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../syntax/types.html#syntax-importdecl}{\mathsf{desc}}~\href{../syntax/types.html#syntax-externdesc}{\mathit{externdesc}} \}\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{:}}{}&\forall\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast.\{ \href{../valid/types.html#syntax-eexportdecl}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../valid/types.html#syntax-eexportdecl}{\mathsf{desc}}~\href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e} \} \to \varnothing\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{\dashv}}{}&\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \oplus \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{uvars}}~\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast, \href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e} \}\\
\end{aligned}
}\end{split}\]
\(\href{../syntax/components.html#syntax-definition}{\mathsf{export}}~\{ \href{../syntax/components.html#syntax-export}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../syntax/components.html#syntax-export}{\mathsf{def}}~\href{../syntax/components.html#syntax-sortidx}{\mathit{sortidx}} \}\)
This rule applies when when \(\href{../syntax/components.html#syntax-sortidx}{\mathit{sortidx}}.\href{../syntax/components.html#syntax-sortidx}{\mathsf{sort}}\) is not STYPE.
The \(\href{../syntax/components.html#syntax-sortidx}{\mathit{sortidx}}\) must be valid with respect to some
\(\href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e}\).
Then the definition \(\href{../syntax/components.html#syntax-definition}{\mathsf{export}}~\{ \href{../syntax/components.html#syntax-export}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../syntax/components.html#syntax-export}{\mathsf{def}}~\href{../syntax/components.html#syntax-sortidx}{\mathit{sortidx}}
\}\) is valid with respect to the component type whose import list is
empty and whose export list is the singleton containing \(\{
\href{../valid/types.html#syntax-eexportdecl}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../valid/types.html#syntax-eexportdecl}{\mathsf{desc}}~\href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e} \}\)
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\href{../syntax/components.html#syntax-sortidx}{\mathit{sortidx}}.\href{../syntax/components.html#syntax-sortidx}{\mathsf{sort}} \neq \href{../syntax/components.html#syntax-sort}{\mathsf{type}}\\
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-siateed}{\vdash}} \href{../syntax/components.html#syntax-sortidx}{\mathit{sortidx}} \mathrel{\href{../valid/components.html#elaborate-siateed}{:}} \href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e}\\
\forall j, \href{../valid/types.html#syntax-evaltypead}{{\mathit{valtype}_e^?}}'_j = \begin{cases}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{values}}[j]^\dagger&\text{if }\href{../syntax/components.html#syntax-sortidx}{\mathit{sortidx}}.\href{../syntax/components.html#syntax-sortidx}{\mathsf{sort}}=\href{../syntax/components.html#syntax-sort}{\mathsf{value}}\land \href{../syntax/components.html#syntax-sortidx}{\mathit{sortidx}}.\href{../syntax/components.html#syntax-sortidx}{\mathsf{idx}} = j\\
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{values}}[j]&\text{otherwise}\\
\end{cases}\\
\forall k, \href{../valid/types.html#syntax-einstancetypead}{{\mathit{instancetype}_e^?}}'_k = \begin{cases}
\forall\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast.\overline{{\href{../valid/types.html#syntax-eexportdecl}{\mathit{externdecl}_e}^\dagger}_l}&
\begin{aligned}
\text{if }&\href{../syntax/components.html#syntax-sortidx}{\mathit{sortidx}}.\href{../syntax/components.html#syntax-sortidx}{\mathsf{sort}} = \href{../syntax/components.html#syntax-sort}{\mathsf{component}} \land \href{../syntax/components.html#syntax-sortidx}{\mathit{sortidx}}.\href{../syntax/components.html#syntax-sortidx}{\mathsf{idx}} = j\\
\land{}&\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}[j] = \forall\href{../valid/types.html#syntax-boundedtyvar}{\mathit{boundedtyvar}}^\ast.\overline{\href{../valid/types.html#syntax-eexterndeclad}{{\mathit{externdecl}_e^?}}_l}\\
\end{aligned}\\
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}[j]&\text{otherwise}\\
\end{cases}\\
\end{array}
}{
\begin{aligned}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-cdatect}{\vdash}}{}&\href{../syntax/components.html#syntax-definition}{\mathsf{export}}~\{ \href{../syntax/components.html#syntax-export}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../syntax/components.html#syntax-export}{\mathsf{def}}~\href{../syntax/components.html#syntax-sortidx}{\mathit{sortidx}} \}\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{:}}{}&\forall\varnothing.\varnothing \to \exists\varnothing.\{ \href{../valid/types.html#syntax-eexportdecl}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../valid/types.html#syntax-eexportdecl}{\mathsf{desc}}~\href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e} \}\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{\dashv}}{}&\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \ominus \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{values}}, \href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}} \} \oplus \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{values}}~\overline{\href{../valid/types.html#syntax-evaltypead}{{\mathit{valtype}_e^?}}'_j}, \href{../valid/conventions.html#syntax-tyctx}{\mathsf{instances}}~\overline{\href{../valid/types.html#syntax-einstancetypead}{{\mathit{instancetype}_e^?}}'_k} \}\\
\end{aligned}
}\end{split}\]
\(\href{../syntax/components.html#syntax-definition}{\mathsf{export}}~\{ \href{../syntax/components.html#syntax-export}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../syntax/components.html#syntax-export}{\mathsf{def}}~\{ \href{../syntax/components.html#syntax-sortidx}{\mathsf{sort}}~\href{../syntax/components.html#syntax-sort}{\mathsf{type}}, \href{../syntax/components.html#syntax-sortidx}{\mathsf{idx}}~\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}} \} \}\)
Then the definition \(\href{../syntax/components.html#syntax-definition}{\mathsf{export}}~\{ \href{../syntax/components.html#syntax-export}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../syntax/components.html#syntax-export}{\mathsf{def}}~\href{../syntax/components.html#syntax-sortidx}{\mathit{sortidx}}
\}\) is valid with respect to the component type whose import list is
empty and whose export list is the singleton containing \(\{
\href{../valid/types.html#syntax-eexportdecl}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../valid/types.html#syntax-eexportdecl}{\mathsf{desc}}~\href{../valid/types.html#syntax-eexterndesc}{\mathit{externdesc}_e} \}\)
\[\begin{split}\frac{
\begin{array}{@{}c@{}}
\href{../syntax/components.html#syntax-sortidx}{\mathit{sortidx}}.\href{../syntax/components.html#syntax-sortidx}{\mathsf{sort}} \neq \href{../syntax/components.html#syntax-sort}{\mathsf{type}}\\
\mathrm{fresh}(\alpha)\\
\href{../valid/conventions.html#syntax-tyctx}{\Gamma}.\href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}[\href{../syntax/components.html#syntax-typeidx}{\mathit{typeidx}}] = \href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}\\
\href{../valid/types.html#syntax-etypebound}{\mathit{typebound}_e} = \begin{cases}
\href{../valid/types.html#syntax-etypebound}{\mathsf{sub~resource}}~&\text{if }\exists i, \href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e} = \href{../valid/types.html#syntax-edeftype}{\mathsf{resource}}~i\\
\href{../valid/types.html#syntax-etypebound}{\mathsf{eq}}~\href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}&\text{otherwise}\\
\end{cases}\\
\end{array}
}{
\begin{aligned}
\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \mathrel{\href{../valid/components.html#elaborate-cdatect}{\vdash}}{}&\href{../syntax/components.html#syntax-definition}{\mathsf{export}}~\{ \href{../syntax/components.html#syntax-export}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../syntax/components.html#syntax-export}{\mathsf{def}}~\href{../syntax/components.html#syntax-sortidx}{\mathit{sortidx}} \}\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{:}}{}&\forall\varnothing.\varnothing \to \exists(\alpha : \href{../valid/types.html#syntax-etypebound}{\mathit{typebound}_e}).\{ \href{../valid/types.html#syntax-eexportdecl}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../valid/types.html#syntax-eexportdecl}{\mathsf{desc}}~\href{../valid/types.html#syntax-eexterndesc}{\mathsf{type}}~\alpha \}\\
\mathrel{\href{../valid/components.html#elaborate-cdatect}{\dashv}}{}&\href{../valid/conventions.html#syntax-tyctx}{\Gamma} \oplus \{ \href{../valid/conventions.html#syntax-tyctx}{\mathsf{evars}}~(\alpha : \href{../valid/types.html#syntax-etypebound}{\mathit{typebound}_e}, \href{../valid/types.html#syntax-edeftype}{\mathit{deftype}_e}), \href{../valid/conventions.html#syntax-tyctx}{\mathsf{types}}~\alpha \}\\
\end{aligned}
}\end{split}\]