From 2601394e423915d75be23de7cfbd1f8da3a398c3 Mon Sep 17 00:00:00 2001
From: Lucy Maya Menon <semiotics@ccs.neu.edu>
Date: Fri, 2 Sep 2022 21:05:18 -0400
Subject: [PATCH] Add draft of the specification of validation
---
LICENSE | 1 +
spec/document/.gitignore | 4 +
spec/document/macros.tex | 286 +++++++++
spec/document/shell.nix | 5 +
spec/document/spec.tex | 21 +
spec/document/syntax/components.tex | 161 +++++
spec/document/syntax/conventions.tex | 47 ++
spec/document/syntax/types.tex | 160 +++++
spec/document/valid/components.tex | 495 +++++++++++++++
spec/document/valid/contexts.tex | 72 +++
spec/document/valid/conventions.tex | 23 +
spec/document/valid/elaboration.tex | 897 +++++++++++++++++++++++++++
spec/document/valid/types.tex | 266 ++++++++
13 files changed, 2438 insertions(+)
create mode 100644 spec/document/.gitignore
create mode 100644 spec/document/macros.tex
create mode 100644 spec/document/shell.nix
create mode 100644 spec/document/spec.tex
create mode 100644 spec/document/syntax/components.tex
create mode 100644 spec/document/syntax/conventions.tex
create mode 100644 spec/document/syntax/types.tex
create mode 100644 spec/document/valid/components.tex
create mode 100644 spec/document/valid/contexts.tex
create mode 100644 spec/document/valid/conventions.tex
create mode 100644 spec/document/valid/elaboration.tex
create mode 100644 spec/document/valid/types.tex
diff --git a/LICENSE b/LICENSE
index c5587c38..5d0eb780 100644
--- a/LICENSE
+++ b/LICENSE
@@ -4,6 +4,7 @@ to that directory and its relative sub-directories.
The relevant directories and licenses are:
design/ - Apache License 2.0
+spec/document/ - W3C Software and Document Notice and License
(Other directories will be added when the [module-linking] repository merges.)
diff --git a/spec/document/.gitignore b/spec/document/.gitignore
new file mode 100644
index 00000000..ef5f7e55
--- /dev/null
+++ b/spec/document/.gitignore
@@ -0,0 +1,4 @@
+*.aux
+*.log
+*.out
+*.pdf
diff --git a/spec/document/macros.tex b/spec/document/macros.tex
new file mode 100644
index 00000000..649fef30
--- /dev/null
+++ b/spec/document/macros.tex
@@ -0,0 +1,286 @@
+\usepackage[hidelinks]{hyperref}
+\usepackage{amssymb}
+\usepackage{amsmath}
+
+\def\K{\mathsf}
+\def\X{\mathit}
+\def\F{\mathrm}
+
+\def\subtypeof{\preccurlyeq}
+\def\ESUBRESOURCE{\K{resource}}
+
+% TODO: xref properly
+\def\name{\X{name}}
+\def\tyvar{\alpha}
+\def\tyvarb{\beta}
+\def\rtidx{\X{rtidx}}
+\def\bool{\X{bool}}
+\def\true{\K{true}}
+\def\false{\K{false}}
+
+\catcode`:=11
+\def\core:type{\X{core{:}type}}
+\def\core:typeidx{\X{core{:}typeidx}}
+\def\core:funcidx{\X{core{:}funcidx}}
+\def\core:memidx{\X{core{:}memidx}}
+\def\core:functype{\X{core{:}functype}}
+\def\core:tabletype{\X{core{:}tabletype}}
+\def\core:memtype{\X{core{:}memtype}}
+\def\core:globaltype{\X{core{:}globaltype}}
+\def\core:import{\X{core{:}import}}
+\def\core:importdesc{\X{core{:}importdesc}}
+\def\core:module{\X{core{:}module}}
+\def\core:IMODULE{\K{module}}
+\def\core:ENAME{\K{name}}
+\def\core:INAME{\K{name}}
+\def\core:EDESC{\K{desc}}
+\def\core:IDESC{\K{desc}}
+
+\makeatletter
+
+\protected\def\u{\afterassignment\@u\count255=}
+\def\@u{\K{u\the\count255}}
+\protected\def\i{\afterassignment\@i\count255=}
+\def\@i{\K{i\the\count255}}
+
+\def\setupPCR{\def\production@cr{\global\let\production@cr=\\}}
+\def\setupSP{%
+ \def\alt{\\&&\mathchar"26A&}%
+ \mathcode`|="8000%
+ \setupPCR%
+}
+\catcode`|=13
+\def|{~\mathchar"26A~}
+\catcode`|=12
+\newenvironment{sum-productions}
+{\[\setupSP\begin{array}{llcl}}
+{\end{array}\]}
+\newenvironment{sum-production}[1]
+{\begin{sum-productions}\production{#1}}
+{\end{sum-productions}}
+\def\production#1{\production@cr&\hypertarget{syntax:#1}{\csname#1\endcsname}&::=&}
+\newenvironment{record-productions}
+{\[\setupPCR\begin{array}{llll}}
+{\end{array}\]}
+\newenvironment{record-production}[1]
+{\begin{record-productions}\production{#1}}
+{\end{record-productions}}
+
+\def\defgrammar@#1#2#3{%
+ \def\currentprefix{#1}%
+ \def\currentgrammar{#2}%
+ \expandafter\def\csname#2\endcsname{{\protect\hyperlink{syntax:#2}{#3}}}%
+}
+\def\defgrammar#1#2{\defgrammar@{#1}{#2}{\X{#2}}}
+\def\defconstr@#1#2{%
+ \expandafter\uppercase\expandafter{\expandafter\expandafter\expandafter\gdef\expandafter\csname\currentprefix#1}\expandafter\endcsname\expandafter{\expandafter{\expandafter\protect\expandafter\hyperlink\expandafter{\expandafter s\expandafter y\expandafter n\expandafter t\expandafter a\expandafter x\expandafter :\currentgrammar}{#2}}}%
+}
+\def\defconstr#1{\defconstr@{#1}{\K{#1}}}
+
+\def\defconstrs#1{\@defconstrs#1,,\relax}
+\def\@defconstrs#1,#2\relax{\defconstr{#1}\if#2,\expandafter\@firstoftwo\else\expandafter\@secondoftwo\fi{}{\@defconstrs#2\relax}}
+\def\defsyntax#1#2#3{\defgrammar{#1}{#2}\defconstrs{#3}}
+
+%%% Surface Type Syntax
+
+\defgrammar{VT}{primvaltype}
+\defconstr{bool}
+\protected\def\VTS{\afterassignment\@VTS\count255=}
+\def\@VTS{\hyperlink{syntax:primvaltype}{\K{s\the\count255}}}
+\protected\def\VTU{\afterassignment\@VTU\count255=}
+\def\@VTU{\hyperlink{syntax:primvaltype}{\K{u\the\count255}}}
+\protected\def\VTFLOAT{\afterassignment\@VTFLOAT\count255=}
+\def\@VTFLOAT{\hyperlink{syntax:primvaltype}{\K{float\the\count255}}}
+\defconstr{char}
+\defconstr{string}
+
+\defgrammar{VT}{defvaltype}
+\defconstr{prim}
+\defconstr{record}
+\defconstr{variant}
+\defconstr{list}
+\defconstr{tuple}
+\defconstr{flags}
+\defconstr{enum}
+\defconstr{union}
+\defconstr{option}
+\defconstr{result}
+\defconstr{own}
+\defconstr{borrow}
+
+\defgrammar{VT}{valtype}
+
+\defgrammar{RF}{recordfield}
+\defconstr{name}
+\defconstr{type}
+
+\defgrammar{VC}{variantcase}
+\defconstr{name}
+\defconstr{type}
+\defconstr{refines}
+
+\defgrammar{RT}{resourcetype}
+\tracingmacros1
+\defconstrs{rep,dtor}
+
+\defsyntax{FT}{functype}{params,results}
+\defsyntax{PL}{paramlist}{type,name}
+\defsyntax{RL}{resultlist}{type,name}
+
+\defsyntax{IT}{instancetype}{}
+\defsyntax{ID}{instancedecl}{alias,type,export}
+\defsyntax{ED}{externdesc}{type,func,value,instance,component}
+\defconstr@{coremodule}{\K{core\_module}}
+\defsyntax{TB}{typebound}{eq,subr}
+\defsyntax{ED}{exportdecl}{name,desc}
+
+\defsyntax{}{componenttype}{}
+\defsyntax{CD}{componentdecl}{import}
+\defsyntax{ID}{importdecl}{name,desc}
+
+\defsyntax{}{deftype}{}
+
+\defgrammar@{}{coredeftype}{\X{core{:}deftype}}
+\defgrammar@{}{coremoduletype}{\X{core{:}moduletype}}
+\defgrammar@{}{coremoduledecl}{\X{core{:}moduledecl}}
+\defgrammar@{}{coreimportdecl}{\X{core{:}importdecl}}
+\defgrammar@{CA}{corealias}{\X{core{:}alias}}
+\defconstrs{sort,target}
+\defgrammar@{CAT}{corealiastarget}{\X{core{:}aliastarget}}
+\defconstrs{outer}
+\defgrammar@{CED}{coreexportdecl}{\X{core{:}exportdecl}}
+\defconstrs{name,desc}
+
+%%% Surface Expression Syntax
+
+\defsyntax{S}{sort}{core,func,value,type,component,instance}
+\defgrammar@{CS}{coresort}{\X{core{:}sort}}
+\defconstrs{instance,module,type,global,memory,table,func}
+
+\defgrammar@{}{coremoduleidx}{\X{core{:}moduleidx}}
+\defgrammar@{}{coreinstanceidx}{\X{core{:}instanceidx}}
+\defgrammar{}{componentidx}
+\defgrammar{}{instanceidx}
+\defgrammar{}{funcidx}
+\defgrammar@{}{corefuncidx}{\X{core{:}funcidx}}
+\defgrammar{}{valueidx}
+\defgrammar{}{typeidx}
+\defgrammar@{}{coretypeidx}{\X{core{:}typeidx}}
+
+\defgrammar@{CSI}{coresortidx}{\X{core{:}sortidx}}
+\defconstrs{sort,idx}
+\defsyntax{SI}{sortidx}{sort,idx}
+
+\defsyntax{D}{definition}{component,instance,alias,type,canon,start,import,export}
+\defconstr@{coremodule}{\K{core\_module}}
+\defconstr@{coreinstance}{\K{core\_instance}}
+\defconstr@{coretype}{\K{core\_type}}
+
+\defgrammar@{CI}{coreinstance}{\X{core{:}instance}}
+\defconstrs{instantiate,exports}
+\defgrammar@{CIA}{coreinstantiatearg}{\X{core{:}instantiatearg}}
+\defconstrs{instance,name}
+\defgrammar@{CE}{coreexport}{\X{core{:}export}}
+\defconstrs{def,name}
+
+\defsyntax{}{component}{}
+
+\defsyntax{I}{instance}{instantiate,exports}
+\defsyntax{IA}{instantiatearg}{name,arg}
+
+\defsyntax{A}{alias}{sort,target}
+\defsyntax{AT}{aliastarget}{export,outer}
+\defconstr@{coreexport}{\K{core\_export}}
+
+\defsyntax{C}{canon}{lift,lower}
+\defconstr@{resourcenew}{\K{resource.new}}
+\defconstr@{resourcedrop}{\K{resource.drop}}
+\defconstr@{resourcerep}{\K{resource.rep}}
+\defsyntax{CO}{canonopt}{memory,realloc,postreturn}
+\defconstr@{stringencodingUTFEIGHT}{\K{string\_encoding\_utf8}}
+\defconstr@{stringencodingUTFSIXTEEN}{\K{string\_encoding\_utf16}}
+\defconstr@{stringencodingLATINONEUTFSIXTEEN}{\K{string\_encoding\_latin1{+}utf16}}
+
+\defsyntax{F}{start}{func,args}
+
+\defsyntax{}{import}{}
+
+\defsyntax{E}{export}{name,def,desc}
+
+%%% Elaborated Type Syntax
+\def\defesyntax#1#2#3{\defgrammar@{E#1}{e#2}{\X{#2}_e}\defconstrs{#3}}
+
+\def\maybedead{{\rlap{$\mathsurround=0pt\dagger$}?}}
+
+\defesyntax{VT}{valtype}{bool,char,list,record,variant,own,ref}
+\protected\def\EVTS{\afterassignment\@EVTS\count255=}
+\def\@EVTS{\hyperlink{syntax:evaltype}{\K{s\the\count255}}}
+\protected\def\EVTU{\afterassignment\@EVTU\count255=}
+\def\@EVTU{\hyperlink{syntax:evaltype}{\K{u\the\count255}}}
+\protected\def\EVTFLOAT{\afterassignment\@EVTFLOAT\count255=}
+\def\@EVTFLOAT{\hyperlink{syntax:evaltype}{\K{float\the\count255}}}
+\defsyntax{RS}{refscope}{call}
+\defgrammar@{}{evaltypead}{{\X{valtype}_e^\maybedead}}
+
+\defesyntax{RF}{recordfield}{name,type}
+\defesyntax{VC}{variantcase}{name,type,refines}
+
+\defesyntax{RT}{resourcetype}{rep,dtor}
+
+\defesyntax{PL}{paramlist}{name,type}
+\defesyntax{RL}{resultlist}{name,type}
+
+\defesyntax{}{functype}{}
+\defesyntax{TB}{typebound}{eq,subr}
+
+\defesyntax{}{instancetype}{}
+\defsyntax{}{boundedtyvar}{}
+\defesyntax{ED}{externdecl}{name,desc}
+\defesyntax{EMD}{externdesc}{func,value,type,instance,component}
+\defconstr@{coremodule}{\K{core\_module}}
+\defgrammar@{}{einstancetypead}{{\X{instancetype}_e^\maybedead}}
+\defgrammar@{}{eexterndeclad}{{\X{externdecl}_e^\maybedead}}
+
+\defesyntax{}{componenttype}{}
+
+\defesyntax{DT}{deftype}{resource}
+
+\defgrammar@{}{ecoreinstancetype}{\X{core{:}instancetype}_e}
+\defgrammar@{}{ecoremoduletype}{\X{core{:}moduletype}_e}
+\defgrammar@{}{ecoredeftype}{\X{core{:}deftype}_e}
+
+%%% Contexts
+
+\defgrammar@{CTC}{coretyctx}{\Gamma_c}
+\defconstrs{types,funcs,tables,mems,globals,modules,instances}
+\defgrammar@{TC}{tyctx}{\Gamma}
+\defconstrs{parent,core,vars,rtypes,types,components,instances,funcs,values}
+\defconstr@{ob}{\K{outer\_boundary}}
+\defconstr@{ld}{\K{locally\_defined}}
+
+\defsyntax{VCC}{vcctx}{ctx,cases}
+\defgrammar@{EVTP}{evaltypepos}{{\pi_v}}
+\defconstrs{result,export}
+\defgrammar@{EDTP}{edeftypepos}{{\pi_d}}
+\defconstr@{export}{extern}
+
+%%% Judgments
+
+
+\def\vdashh!#1!{\mathrel{\hyperref[judgment:#1]{\vdash}}}
+\def\leadstoh!#1!{\mathrel{\hyperref[judgment:#1]{\leadsto}}}
+\def\dashvh!#1!{\mathrel{\hyperref[judgment:#1]{\dashv}}}
+\def\trelh!#1!{\mathrel{\hyperref[judgment:#1]{:}}}
+
+\def\freeVars#1{\mathop{\F{fv}}(#1)}
+\def\subst{\gamma}
+\def\resolveVars#1{\mathop{\F{resolve\_vars}}(#1)}
+\def\length#1{\lVert#1\rVert}
+
+\def\novalues#1{{}\mathrel{\hyperref[judgment:novalues]{\vdash^\mathsf{\mkern-20mu\neg v}}}{#1}}
+
+%\def\EEDtoCtx#1#2#3#4{{#1} \mathrel{\hyperref[judgment:EEDtoCtx]{\oplus}} {#2} \mathrel{\hyperref[judgment:EEDtoCtx]{=}} {#4} \mathrel{\hyperref[judgment:EEDtoCtx]{@}} {#3}}
+%\def\callEITvars#1{\mathop{\hyperref[judgment:EITvars]{\F{unvar\_instance}}}({#1})}
+%\def\EITvars#1#2#3{\callEITvars{#1} = \exists {#2}. {#3}}
+
+\makeatother
diff --git a/spec/document/shell.nix b/spec/document/shell.nix
new file mode 100644
index 00000000..b5a7dacc
--- /dev/null
+++ b/spec/document/shell.nix
@@ -0,0 +1,5 @@
+{ nixpkgs ? import <nixpkgs> {} }: with nixpkgs;
+stdenv.mkDerivation {
+ name = "wasm-components-spec";
+ buildInputs = [ texlive.combined.scheme-full ];
+}
diff --git a/spec/document/spec.tex b/spec/document/spec.tex
new file mode 100644
index 00000000..1749fe11
--- /dev/null
+++ b/spec/document/spec.tex
@@ -0,0 +1,21 @@
+\documentclass{report}
+
+\input{macros}
+
+\begin{document}
+
+\chapter{Introduction}
+
+\chapter{Structure}
+\include{syntax/conventions}
+\include{syntax/types}
+\include{syntax/components}
+
+\chapter{Validation}
+\include{valid/conventions}
+\include{valid/types}
+\include{valid/contexts}
+\include{valid/elaboration}
+\include{valid/components}
+
+\end{document}
diff --git a/spec/document/syntax/components.tex b/spec/document/syntax/components.tex
new file mode 100644
index 00000000..164a0b24
--- /dev/null
+++ b/spec/document/syntax/components.tex
@@ -0,0 +1,161 @@
+\section{Components}
+
+\subsection{Sorts}
+
+A component's definitions define objects, each of which is of one of
+the following \emph{sort}s:
+
+\begin{sum-productions}
+ \production{coresort}
+ \CSFUNC | \CSTABLE | \CSMEMORY | \CSGLOBAL | \CSTYPE | \CSMODULE |
+ \CSINSTANCE
+ \production{sort}
+ \SCORE~\coresort \alt
+ \SFUNC | \SVALUE | \STYPE | \SCOMPONENT | \SINSTANCE
+\end{sum-productions}
+
+\subsection{Indices}
+
+Each object defined by a component exists within an \emph{index space}
+made up of all objects of the same sort. Unlike in Core WebAssembly, a
+component definition may only refer to objects that were defined prior
+to it in the current component. Future definitions refer to past
+definitions by means of an \emph{index} into the appropriate index
+space:
+
+\begin{record-productions}
+ \production{coremoduleidx} \u32
+ \production{coreinstanceidx} \u32
+ \production{componentidx} \u32
+ \production{instanceidx} \u32
+ \production{funcidx} \u32
+ \production{corefuncidx} \u32
+ \production{valueidx} \u32
+ \production{typeidx} \u32
+ \production{coretypeidx} \u32
+\end{record-productions}
+
+\begin{record-productions}
+ \production{coresortidx} \{ \CSISORT~\coresort, \CSIIDX~\u32 \}\\
+ \production{sortidx} \{ \SISORT~\sort, \SIIDX~\u32 \}
+\end{record-productions}
+
+\subsection{Definitions}
+
+\begin{sum-productions}
+ \production{definition}
+ \DCOREMODULE~\core:module \alt
+ \DCOREINSTANCE~\coreinstance \alt
+ \DCORETYPE~\coredeftype \alt
+ \DCOMPONENT~\component \alt
+ \DINSTANCE~\instance \alt
+ \DALIAS~\alias \alt
+ \DTYPE~\deftype \alt
+ \DCANON~\canon \alt
+ \DSTART~\start \alt
+ \DIMPORT~\import \alt
+ \DEXPORT~\export
+\end{sum-productions}
+
+\subsection{Core Instances}
+
+A core instance may be defined either by instantiating a core module
+with other core instances taking the place of its first-level imports,
+or by creating a core instance from whole cloth by combining core
+definitions already present in our index space:
+
+\begin{sum-productions}
+ \production{coreinstance}
+ \CIINSTANTIATE~\coremoduleidx~\coreinstantiatearg^{*} \alt
+ \CIEXPORTS~\coreexport^{*}
+ \production{coreinstantiatearg}
+ \{ \CIANAME~\name, \CIAINSTANCE~\coreinstanceidx \}
+ \production{coreexport} \{ \CENAME~\name, \CEDEF~\coresortidx \}
+\end{sum-productions}
+
+\subsection{Components}
+
+A component is merely a sequence of definitions:
+
+\begin{record-production}{component}
+ \definition^{*}
+\end{record-production}
+
+\subsection{Instances}
+
+Component-level instance declarations are nearly identical to
+core-level instance declarations, with the caveat that more sorts of
+definitions may be supplied as imports:
+
+\begin{sum-productions}
+ \production{instance}
+ \IINSTANTIATE~\componentidx~\instantiatearg^{*}\\&&|&
+ \IEXPORTS~\export^{*}\\
+ \production{instantiatearg}
+ \{ \IANAME~\name, \IAARG~\sortidx \}
+\end{sum-productions}
+
+\subsection{Aliases}
+
+An alias definition copies a definition from some other module,
+component, or instance into an index space of the current component:
+
+\begin{sum-productions}
+ \production{alias} \{ \ASORT~\sort, \ATARGET~\aliastarget \}
+ \production{aliastarget}
+ \ATEXPORT~\instanceidx~\name \alt
+ \ATCOREEXPORT~\coreinstanceidx~\name \alt
+ \ATOUTER~\u32~\u32
+\end{sum-productions}
+
+\subsection{Canonical Definitions}
+
+Canonical definitions are the only way to convert between Core
+WebAssembly functions and component-level shared-nothing functions
+which produce and consume values of type $\valtype$. A \emph{canon
+ lift} definition converts a core WebAssembly function into a
+component-level function which may be exported or used to satisfy the
+imports of another component; a \emph{canon lower} definition converts
+an lifted function (often imported) into a core function.
+
+\begin{sum-productions}
+ \production{canon}
+ \CLIFT~\core:funcidx~\canonopt^{*}~\typeidx \alt
+ \CLOWER~\funcidx~\canonopt^{*}
+ \production{canonopt}
+ \COSTRINGENCODINGUTFEIGHT \alt
+ \COSTRINGENCODINGUTFSIXTEEN \alt
+ \COSTRINGENCODINGLATINONEUTFSIXTEEN \alt
+ \COMEMORY~\core:memidx \alt
+ \COREALLOC~\core:funcidx \alt
+ \COPOSTRETURN~\core:funcidx
+\end{sum-productions}
+
+\subsection{Start definitions}
+
+A start definition specifies a component function which this component
+would like to see called at instantiation type in order to do some
+sort of initialization.
+
+\begin{record-production}{start}
+ \{ \FFUNC~\funcidx, \FARGS~\valueidx^{*} \}
+\end{record-production}
+
+\subsection{Imports}
+
+Since an imported value is described entirely by its type, an actual
+import definition is effectively the same thing as an import
+declaration:
+
+\begin{record-production}{import}
+ \importdecl
+\end{record-production}
+
+\subsection{Exports}
+
+An export definition is simply a name and a reference to another
+definition to export:
+
+\begin{record-production}{export}
+ \{ \ENAME~\name, \EDEF~\sortidx \}
+\end{record-production}
diff --git a/spec/document/syntax/conventions.tex b/spec/document/syntax/conventions.tex
new file mode 100644
index 00000000..65bcf078
--- /dev/null
+++ b/spec/document/syntax/conventions.tex
@@ -0,0 +1,47 @@
+\section{Conventions}
+
+The WebAssembly component specification defines a language for
+specifying components, which, like the WebAssembly core language, may
+be represented by multiple complete representations (e.g. the
+\hyperref[sec:binary-format]{binary format} and the
+\hyperref[sec:text-format]{text format}). In order to avoid
+duplication, the static and dynamic semantics of the WebAssembly
+component model are instead defined over an abstract syntax.
+
+The following conventions are adopted in defining grammar rules for abstract syntax.
+
+\begin{itemize}
+\item Terminal symbols (atoms) are written in sans-serif font:
+ $\K{i32}, \K{end}$.
+
+\item Nonterminal symbols are written in italic font:
+ $\X{valtype}, \X{instr}$.
+
+\item $A^n$ is a sequence of $n\geq 0$ iterations of $A$.
+
+\item $A^\ast$ is a possibly empty sequence of iterations of $A$.
+ (This is a shorthand for $A^n$ used where $n$ is not relevant.)
+
+\item $A^+$ is a non-empty sequence of iterations of $A$. (This is a
+ shorthand for $A^n$ where $n \geq 1$.)
+
+\item $A^?$ is an optional occurrence of $A$. (This is a shorthand for
+ $A^n$ where $n \leq 1$.)
+
+\item Productions are written $\X{sym} ::= A_1 ~|~ \dots ~|~ A_n$.
+
+\item Large productions may be split into multiple definitions,
+ indicated by ending the first one with explicit ellipses,
+ $\X{sym} ::= A_1 ~|~ \dots$, and starting continuations with
+ ellipses, $\X{sym} ::= \dots ~|~ A_2$.
+
+\item Some productions are augmented with side conditions in
+ parentheses, ``$(\iff \X{condition})$'', that provide a shorthand for
+ a combinatorial expansion of the production into many separate
+ cases.
+
+\item If the same meta variable or non-terminal symbol appears
+ multiple times in a production, then all those occurrences must
+ have the same instantiation. (This is a shorthand for a side
+ condition requiring multiple different variables to be equal.)
+\end{itemize}
diff --git a/spec/document/syntax/types.tex b/spec/document/syntax/types.tex
new file mode 100644
index 00000000..6500ca2b
--- /dev/null
+++ b/spec/document/syntax/types.tex
@@ -0,0 +1,160 @@
+\section{Types}
+
+The component model introduces two new kinds of types: value types,
+which are used to classify shared-nothing interface values, and
+defined types, which are used to characterize the core and component
+modules, instances, and functions which form part of a a component's
+interface.
+
+\subsection{Value types}
+
+A \emph{value type} classifies a component-level abstract value.
+Unlike for Core WebAssembly values, no specified abstract syntax of
+component values exist; they serve simply to define the interface of
+lifted component functions (which currently may be produced only via
+canonical definitions).
+
+Value types are further divided into primitive value types, which have
+a compact representation and can be found in most places where types
+are allowed, and defined value types, which must appear in a type
+definition before they can be used (via a $\typeidx$ into the type
+index space):
+
+
+\begin{sum-productions}
+ \production{primvaltype}
+ \VTBOOL \alt
+ \VTS8 | \VTU8 | \VTS16 | \VTU16 | \VTS32 | \VTU32 | \VTS64 | \VTU64 \alt
+ \VTFLOAT32 | \VTFLOAT64 \alt
+ \VTCHAR | \VTSTRING
+
+ \production{defvaltype}
+ \VTPRIM~\primvaltype \alt
+ \VTRECORD~\recordfield^{+} \alt
+ \VTVARIANT~\variantcase^{+} \alt
+ \VTLIST~\valtype \alt
+ \VTTUPLE~\valtype^{*} \alt
+ \VTFLAGS~\name^{*} \alt
+ \VTENUM~\name^{+} \alt
+ \VTUNION~\valtype^{+} \alt
+ \VTOPTION~\valtype \alt
+ \VTRESULT~\valtype^{?}~\valtype^{?} \alt
+ \VTOWN~\typeidx \alt
+ \VTBORROW~\typeidx
+
+ \production{valtype}
+ \primvaltype | \typeidx
+\end{sum-productions}
+
+\begin{record-productions}
+ \production{recordfield}
+ \{ \RFNAME~\name, \RFTYPE~\valtype \}
+ \production{variantcase}
+ \{ \VCNAME~\name, \VCTYPE~\valtype^{?}, \VCREFINES~\u32^? \}
+\end{record-productions}
+
+\subsection{Resource Types}
+
+\begin{record-production}{resourcetype}
+ \{ \RTREP~\i32, \RTDTOR~\funcidx \}
+\end{record-production}
+
+\subsection{Function Types}
+
+A component-level shared-nothing function is classified by the types
+of its parameters and return values. Such a function may take as
+parameters zero or more named values, and will return as results zero
+or more namde values. If a function takes a single parameter, or
+returns a single result, said parameter or result may be unnamed:
+
+\begin{record-production}{functype}
+ \paramlist \to \resultlist
+\end{record-production}
+
+The input or output of a function is classified by a parameter or
+return list:
+
+\begin{sum-productions}
+ \production{paramlist}
+ \{ \PLNAME~\name, \PLTYPE~\valtype \}^{*}
+ \production{resultlist}
+ \valtype \alt
+ \{ \RLNAME~\name, \RLTYPE~\valtype \}^{*}
+\end{sum-productions}
+
+\subsection{Instance Types}
+
+A component instance is conceptually classified by the types of its
+exports. However, an instance's type is concretely represented as a
+series of \emph{declarations} manipulating index spaces (particular to
+the instance type; these index spaces are entirely unrelated to both
+the index spaces of any instance which has this type and those of any
+instance importing or exporting something of this type). This allows
+for better type sharing and, in the future, uses of private types from
+parent components.
+
+\begin{sum-productions}
+ \production{instancetype} \instancedecl^{*}
+ \production{instancedecl}
+ \IDALIAS~\alias \alt
+ \IDTYPE~\deftype \alt
+ \IDEXPORT~\exportdecl
+ \production{externdesc}
+ \EDTYPE~\typebound \alt
+ \EDCOREMODULE~\core:typeidx \alt
+ \EDFUNC~\typeidx \alt
+ \EDVALUE~\valtype \alt
+ \EDINSTANCE~\typeidx \alt
+ \EDCOMPONENT~\typeidx
+ \production{typebound}
+ \TBEQ~\typeidx \alt
+ \TBSUBR\\
+ \production{exportdecl} \{ \EDNAME~\name, \EDDESC~\externdesc \}
+\end{sum-productions}
+
+\subsection{Component Types}
+
+A component is conceptually classified by the types of its imports and
+exports. However, as in the case of instances, this is concretely
+represented as a series of declarations. Component types allow the
+same declarations used in instance types, but also import declarations.
+
+\begin{sum-productions}
+ \production{componenttype} \componentdecl^{*}\\
+ \production{componentdecl}
+ \instancedecl \alt
+ \CDIMPORT~\importdecl
+ \production{importdecl}
+ \{ \IDNAME~\name, \IDDESC~\externdesc \}
+\end{sum-productions}
+
+\subsection{Defined Types}
+
+A type definition may name a value, resource, function, component, or
+instance type:
+
+\begin{sum-production}{deftype}
+ \defvaltype \alt \resourcetype \alt \functype \alt \componenttype
+ \alt \instancetype
+\end{sum-production}
+
+\subsection{Core definition types}
+
+The component module specification also defines an expanded notion of
+what a core type is, which may eventually be subsumed by a core module
+linking extension.
+
+\begin{sum-productions}
+ \production{coredeftype}
+ \core:functype \alt \coremoduletype
+ \production{coremoduletype} \coremoduledecl^{*}
+ \production{coremoduledecl}
+ \coreimportdecl \alt
+ \coredeftype \alt
+ \corealias \alt
+ \coreexportdecl \alt
+ \production{corealias} \{ \CASORT~\coresort, \CATARGET~\corealiastarget \}
+ \production{corealiastarget} \CATOUTER~\u32~\u32
+ \production{coreimportdecl} \core:import
+ \production{coreexportdecl} \{ \CEDNAME~\name, \CEDDESC~\core:importdesc \}
+\end{sum-productions}
diff --git a/spec/document/valid/components.tex b/spec/document/valid/components.tex
new file mode 100644
index 00000000..40f13f3d
--- /dev/null
+++ b/spec/document/valid/components.tex
@@ -0,0 +1,495 @@
+\section{Components}
+
+\subsection{No Live Values In Context}
+\label{judgment:novalues}
+\fbox{$\novalues{\tyctx}$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \novalues\tyctx.\TCPARENT\\
+ \forall i, \exists \evaltype, \tyctx.\TCVALUES[i] = \evaltype^\dagger\\
+ \begin{aligned}\forall i, \exists \overline{\eexterndeclad_j},{}&\tyctx.\TCINSTANCES[i] = \eexterndeclad\\\land{}&{}\forall j, \neg \exists \evaltype, \eexterndeclad_j = \EEMDVALUE~\evaltype\\\end{aligned}\\
+ \end{array}
+ }{
+ \novalues \tyctx
+ }
+\]
+
+\subsection{$\overline{\definition_i}$}
+\label{judgment:CatECT}
+\fbox{$\tyctx \vdashh!CatECT! \component \trelh!CatECT! \ecomponenttype$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \tyctx_0 = \{ \TCPARENT~\tyctx, \TCOB~\true \}\\
+ \forall i, \tyctx_{i-1} \vdashh!CDatECT! \definition_i \trelh!CDatECT! {\ecomponenttype}_i \dashvh!CDatECT! \tyctx_i\\
+ \novalues\tyctx_n\\
+ \ecomponenttype = \bigoplus_i \ecomponenttype_i\\
+ \tyctx_n.\TCVARS \cap \freeVars{\ecomponenttype} = \varnothing\\
+ \end{array}
+ }{
+ \tyctx \vdashh!CatECT! \overline{\definition_i}^n
+ \trelh!CatECT! \ecomponenttype
+ }
+\]
+
+\subsection{Core Sort Indices}
+\label{judgment:CSIatCID}
+\fbox{$\tyctx \vdashh!CSIatCID! \coresortidx \trelh!CSIatCID! \core:importdesc$}
+
+\subsection{Instantiate/Export Arguments}
+\label{judgment:SIatEED}
+\fbox{$\tyctx \vdashh!SIatEED! \sortidx \trelh!SIatEED! \eexterndesc$}
+
+\subsubsection{Core Modules}
+\[
+ \frac{
+ \tyctx \vdash \tyctx.\TCCORE.\CTCMODULES[i] \subtypeof \ecoremoduletype
+ }{
+ \tyctx \vdashh!SIatEED! \{ \SISORT~\SCORE~\CSMODULE, \SIIDX~i \}
+ \trelh!SIatEED! \EEMDCOREMODULE~\ecoremoduletype
+ }
+\]
+
+\subsubsection{Functions}
+\[
+ \frac{
+ \tyctx \vdash \tyctx.\TCFUNCS[i] \subtypeof \efunctype
+ }{
+ \tyctx \vdashh!SIatEED! \{ \SISORT~\SFUNC, \SIIDX~i \}
+ \trelh!SIatEED! \EEMDFUNC~\efunctype
+ }
+\]
+
+\subsubsection{Values}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \tyctx \vdash \tyctx.\TCVALUES[i] \subtypeof \evaltype\\
+ \tyctx \vdashh!EVT! \evaltype\\
+ \end{array}
+ }{
+ \tyctx \vdashh!SIatEED! \{ \SISORT~\SVALUE, \SIIDX~i \}
+ \trelh!SIatEED! \EEMDVALUE~\evaltype
+ }
+\]
+
+\subsubsection{Types}
+\[
+ \frac{
+ \tyctx \vdash \tyctx.\TCTYPES[i] \subtypeof \edeftype
+ }{
+ \tyctx \vdashh!SIatEED! \{ \SISORT~\STYPE, \SIIDX~i \}
+ \trelh!SIatEED! \EEMDTYPE~\edeftype
+ }
+\]
+
+\subsubsection{Instances}
+\[
+ \frac{
+ \tyctx \vdash \tyctx.\TCINSTANCES[i] \subtypeof \einstancetype
+ }{
+ \tyctx \vdashh!SIatEED! \{ \SISORT~\SINSTANCE, \SIIDX~i \}
+ \trelh!SIatEED! \EEMDINSTANCE~\einstancetype
+ }
+\]
+
+\subsubsection{Components}
+\[
+ \frac{
+ \tyctx \vdash \tyctx.\TCCOMPONENTS[i] \subtypeof \ecomponenttype
+ }{
+ \tyctx \vdashh!SIatEED! \{ \SISORT~\SCOMPONENT, \SIIDX~i \}
+ \trelh!SIatEED! \EEMDCOMPONENT~\ecomponenttype
+ }
+\]
+
+\subsection{Start Arguments}
+\label{judgment:VIsatPL}
+\fbox{$\tyctx \vdashh!VIsatPL! \overline{\valueidx_i} \trelh!VIsatPL! \paramlist$}
+\[
+ \frac{
+ \forall i, \tyctx \vdashh!VIsatPL! \valueidx_i \trelh!VIsatPL! {\evaltype}_i
+ }{
+ \tyctx \vdashh!VIsatPL! \overline{\valueidx_i} \trelh!VIsatPL! \overline{\EPLNAME~\name_i, \EPLTYPE~{\evaltype}_i}
+ }
+\]
+
+\subsection{Definitions}
+\label{judgment:CDatECT}
+\fbox{$\tyctx \vdashh!CDatECT! \definition \trelh!CDatECT! \ecomponenttype \dashvh!CDatECT! \tyctx'$}
+
+\subsubsection{$\DCOREMODULE~\core:module$}
+\[
+ \frac{
+ \vdash \core:module : \ecoremoduletype
+ }{
+ \begin{aligned}
+ \tyctx \vdashh!CDatECT!{}&\DCOREMODULE~\core:module\\
+ \trelh!CDatECT!{}&\forall \varnothing. \varnothing \to \exists \varnothing. \varnothing\\
+ \dashvh!CDatECT!{}&\tyctx \oplus \begin{aligned}\{{}&\TCCORE.\CTCMODULES~\ecoremoduletype\\,{}&\TCLD~\{ \SISORT~\SCORE~\CSMODULE, \SIIDX~\length{\tyctx.\TCCORE.\CTCMODULES} \}\}\end{aligned}\\
+ \end{aligned}
+ }
+\]
+
+\subsubsection{$\DCOREINSTANCE~\CIINSTANTIATE~\coremoduleidx~\overline{\coreinstantiatearg_i}$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \tyctx.\TCCORE.\CTCMODULES[\coremoduleidx] = \overline{\coreimportdecl_j} \to \overline{\ecoreinstancetype}\\
+ \begin{aligned}
+ \forall j, \exists i,&\coreinstantiatearg_i.\CIANAME = \coreimportdecl_j.\core:IMODULE\\
+ \land{}& \tyctx.\TCCORE.\CTCINSTANCES[\coreinstantiatearg_i.\CIAINSTANCE] = \overline{\coreexportdecl_l}\\
+ \land{}& {\begin{aligned}[t]
+ \exists l,&\coreexportdecl_l.\core:ENAME = \coreimportdecl_j.\core:INAME\\
+ \land{}&\coreexportdecl_l.\core:EDESC \subtypeof \coreimportdecl_j.\core:IDESC\\
+ \end{aligned}}
+ \end{aligned}\\
+ \forall i,\forall i', \coreinstantiatearg_i.\CIANAME = \coreinstantiatearg_{i'}.\CIANAME \Rightarrow i = i'\\
+ \end{array}
+ }{
+ \begin{aligned}
+ \tyctx \vdashh!CDatECT!{}&\DCOREINSTANCE~\CIINSTANTIATE~\coremoduleidx~\overline{\coreinstantiatearg_i}\\
+ \trelh!CDatECT!{}&\forall\varnothing.\varnothing \to \exists\varnothing.\varnothing\\
+ \dashvh!CDatECT!{}&\tyctx \oplus \begin{aligned}\{{}&\TCCORE.\CTCINSTANCES~\ecoreinstancetype\\,{}&\TCLD~\{\SISORT~\SCORE~\CSINSTANCE, \SIIDX~\length{\tyctx.\TCCORE.\CTCINSTANCES}\}\}\end{aligned}
+ \end{aligned}
+ }
+\]
+
+\subsubsection{$\DCOREINSTANCE~\CIEXPORTS~\overline{\{\CENAME~\name_i, \CEDEF~\coresortidx_i \}}$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \forall i, \tyctx \vdash \coresortidx_i : \core:importdesc_i\\
+ \forall i j, \name_i = \name_j \Rightarrow i = j
+ \end{array}
+ }{
+ \begin{aligned}
+ \tyctx \vdashh!CDatECT!{}& \DCOREINSTANCE~\CIEXPORTS~\overline{\{\CENAME~\name_i, \CEDEF~\coresortidx_i \}}\\
+ \trelh!CDatECT!{}& \forall\varnothing.\varnothing \to \exists\varnothing.\varnothing\\
+ \dashvh!CDatECT!{}& \tyctx \oplus \begin{aligned} \{{}& \TCCORE.\CTCINSTANCES~\overline{\{ \CEDNAME~\name_i, \CEDDESC~\core:importdesc_i\}}\\,{}&\TCLD~\{\SISORT~\SCORE~\CSINSTANCE, \SIIDX~\length{\tyctx.\TCCORE.\CTCINSTANCES} \}\}\end{aligned}\\
+ \end{aligned}
+ }
+\]
+
+\subsubsection{$\DCORETYPE~\coredeftype$}
+\[
+ \frac{
+ \tyctx \vdash \coredeftype \leadsto \ecoredeftype
+ }{
+ \tyctx \vdashh!CDatECT! \DCORETYPE~\coredeftype
+ \trelh!CDatECT! \forall\varnothing.\varnothing \to \exists\varnothing.\varnothing
+ \dashvh!CDatECT! \tyctx \oplus \{ \TCCORE.\CTCTYPES~\ecoredeftype \}
+ }
+\]
+
+\subsubsection{$\DCOMPONENT~\component$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \tyctx = \tyctx_1 \boxplus \tyctx_2\\
+ \tyctx_1 \vdashh!CatECT! \component \trelh!CatECT! \ecomponenttype\\
+ \end{array}
+ }{
+ \tyctx \vdashh!CDatECT! \component
+ \trelh!CDatECT! \forall\varnothing.\varnothing \to \exists\varnothing.\varnothing
+ \dashvh!CDatECT! \tyctx_2 \oplus \begin{aligned} \{{}& \TCCOMPONENTS~\ecomponenttype\\,{}& \TCLD~\{\SISORT~\SCOMPONENT, \SIIDX~\length{\tyctx.\TCCOMPONENTS}\}\}\end{aligned}
+ }
+\]
+
+\subsubsection{$\DINSTANCE~\IINSTANTIATE~\componentidx~\overline{\instantiatearg_i}$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \tyctx.\TCCOMPONENTS[\componentidx] = \forall\overline{\boundedtyvar_j}.\overline{{\eexterndecl}_k} \to \exists\overline{\boundedtyvar_o}. \einstancetype\\
+ \forall j, \exists {\edeftype}_j, {\edeftype}_j \subtypeof \boundedtyvar_j\\
+ \begin{aligned}&\overline{\eexterndecl'}_k\to\exists\overline{\boundedtyvar'_o}.\einstancetype' =\\&\quad (\overline{{\eexterndecl}_k} \to \exists\overline{\boundedtyvar_o}.\einstancetype)[\overline{{\edeftype}_j/\boundedtyvar_j}]\end{aligned}\\
+ \begin{aligned}
+ \forall k, \exists i, &\instantiatearg_i.\IANAME = {\eexterndecl'}_k.\EEDNAME\\\land{}&\tyctx \vdashh!SIatEED! \instantiatearg_i.\IAARG \trelh!SIatEED! {\eexterndecl'}_k.\EEDDESC
+ \end{aligned}\\
+ \forall l, \evaltypead_l = \begin{cases}
+ \tyctx.\TCVALUES[l]^\dagger&\text{if }\begin{aligned}\exists i,{}&\instantiatearg_i.\IAARG.\SISORT = \SVALUE\\\land{}&\instantiatearg_i.\IAARG.\SIIDX = k\\\end{aligned}\\
+ \tyctx.\TCVALUES[l]&\text{otherwise}\\
+ \end{cases}\\
+ \forall m, {\einstancetypead}_m = \begin{cases}
+ \einstancetype'&\text{if }m = \length{\tyctx.\TCINSTANCES}\\
+ \overline{\eexterndecl^\dagger}_n &\text{if }
+ \begin{aligned}
+ \exists i,{}&\instantiatearg_i.\IAARG.\SISORT = \SCOMPONENT\\
+ \land{}&\instantiatearg_i.\IAARG.\SIIDX = m\\
+ \land{}&\tyctx.\TCINSTANCES[m] = \overline{\eexterndeclad_n}\\
+ \end{aligned}\\
+ \tyctx.\TCINSTANCES[m] & \text{otherwise}\\
+ \end{cases}
+ \end{array}
+ }{
+ \begin{aligned}
+ \tyctx \vdashh!CDatECT!{}&\DINSTANCE~\IINSTANTIATE~\componentidx~\overline{\instantiatearg_i}\\
+ \trelh!CDatECT!{}&\forall\varnothing.\varnothing \to \exists\varnothing.\varnothing\\
+ \dashvh!CDatECT!{}&\tyctx' \ominus \{ \TCVALUES, \TCINSTANCES \} \oplus \begin{aligned} \{{}& \TCVARS~\overline{(\boundedtyvar'_o,)}, \TCINSTANCES~\overline{\einstancetypead}_m, \TCVALUES~\overline{\evaltypead_l}\\,{}& \TCLD~\{ \SISORT~\SINSTANCE, \SIIDX~\length{\tyctx.\TCINSTANCES}\}\}\end{aligned}\\
+ \end{aligned}
+ }
+\]
+
+\subsubsection{$\DINSTANCE~\IEXPORTS~\overline{\{ \ENAME~\name_i, \EDEF~\sortidx_i \}}$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \forall i, \tyctx \vdashh!SIatEED! \sortidx_i \trelh!SIatEED! {\eexterndesc}_i\\
+ \forall i j, \name_i = \name_j \Rightarrow i = j\\
+ \forall j, \evaltypead_j = \begin{cases}
+ \tyctx.\TCVALUES[j]^\dagger&\text{if }\begin{aligned}\exists i,{}&\sortidx_i.\SISORT = \SVALUE\\\land{}&\sortidx_i.\SIIDX = j\\\end{aligned}\\
+ \tyctx.\TCVALUES[j]&\text{otherwise}\\
+ \end{cases}\\
+ \einstancetype = \overline{ \EEDNAME~\name_i, \EEDDESC~{\eexterndesc}_i}\\
+ \forall k, \einstancetypead_k = \begin{cases}
+ \einstancetype&\text{if } k = \length{\tyctx.\TCINSTANCES}\\
+ \overline{{\eexterndecl^\dagger}_l}&\text{if }
+ \begin{aligned}
+ \exists i,{}&\sortidx_i.\SISORT = \SINSTANCE\\
+ \land{}&\sortidx_i.\SIIDX = k\\
+ \land{}&\tyctx.\TCINSTANCES[k] = \overline{\eexterndeclad_l}\\
+ \end{aligned}\\
+ \tyctx.\TCINSTANCES[k]&\text{otherwise}
+ \end{cases}
+ \end{array}
+ }{
+ \begin{aligned}
+ \tyctx \vdashh!CDatECT!{}& \DINSTANCE~\IEXPORTS~\overline{\{ \ENAME~\name_i, \EDEF~\sortidx_i \}}\\
+ \trelh!CDatECT!{}& \forall\varnothing.\varnothing \to \exists\varnothing.\varnothing\\
+ \dashvh!CDatECT!{}& \tyctx\ominus\{\TCINSTANCES,\TCVALUES\} \oplus \begin{aligned} \{{}& \TCINSTANCES~\overline{\einstancetypead_k},\TCVALUES~\overline{\evaltypead_j}\\,{}& \TCLD~\{ \SISORT~\SINSTANCE,\SIIDX~\length{\tyctx.\TCINSTANCES}\} \}\end{aligned}
+ \end{aligned}
+ }
+\]
+
+\subsubsection{$\DALIAS~\{ \ASORT~\sort, \ATARGET~\ATEXPORT~\instanceidx~\name \}$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \tyctx.\TCINSTANCES[\instanceidx] = \overline{{\eexterndeclad}_i}\\
+ \exists i, {\eexterndeclad}_i.\EEDNAME = \name\\
+ \forall j, {\eexterndeclad'}_j = \begin{cases}
+ {\eexterndeclad}_j^\dagger&\text{if } (\sort = \SVALUE \lor \sort = \SINSTANCE) \land j = i\\
+ {\eexterndeclad}_j&\text{otherwise}\\
+ \end{cases}\\
+ \end{array}
+ }{
+ \begin{aligned}
+ \tyctx \vdashh!CDatECT!{}& \DALIAS~\{ \ASORT~\sort, \ATARGET~\ATEXPORT~\instanceidx~\name \}\\
+ \trelh!CDatECT!{}& \forall\varnothing.\varnothing \to \exists\varnothing.\varnothing\\
+ \dashvh!CDatECT!{}& \tyctx \oplus \{ \F{index\_space}(\sort)~{\eexterndeclad}_i.\EEDDESC, \TCINSTANCES[i]~\overline{{\eexterndeclad'}_j} \}\\
+ \end{aligned}
+ }
+\]
+
+\subsubsection{$\DALIAS~\{ \ASORT~\sort, \ATARGET~\ATCOREEXPORT~\coreinstanceidx~\name \}$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \sort = \SCORE~\coresort\\
+ \tyctx.\TCCORE.\CTCINSTANCES[\coreinstanceidx] = \overline{\coreexportdecl_i}\\
+ {\coreexportdecl}_i.\CEDNAME~\name\\
+ \end{array}
+ }{
+ \begin{aligned}
+ \tyctx \vdashh!CDatECT!{}& \DALIAS~\{ \ASORT~\sort, \ATARGET~\ATCOREEXPORT~\coreinstanceidx~\name \}\\
+ \trelh!CDatECT!{}& \forall\varnothing.\varnothing \to \exists\varnothing.\varnothing\\
+ \dashvh!CDatECT!{}& \tyctx \oplus \{ \F{index\_space}(\sort)~{\coreexportdecl}_i.\CEDDESC \}
+ \end{aligned}
+ }
+\]
+
+\subsubsection{$\DALIAS~\{ \ASORT~\sort, \ATARGET~\ATOUTER~\u32_o~\u32_i \}$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \sort \in \{ \SCOMPONENT, \SCORE~\CSMODULE, \STYPE, \SCORE~\CSTYPE \}\\
+ \{\SISORT~\sort, \SIIDX~\u32_i\} \in \Gamma.\TCPARENT[\u32_o].\TCLD\\
+ \eexterndesc = \sort~\Gamma.\TCPARENT[\u32_o].\F{index\_space}(\sort)[\u32_i]\\
+ \mathit{boundary} = \bigvee_{j<\u32_o} \tyctx.\TCPARENT[j].\TCOB\\
+ \subst = \begin{cases}\resolveVars{\tyctx.\TCPARENT[\u32_o]} & \text{if } \mathit{boundary}\\\varnothing&\text{otherwise}\end{cases}\\
+ \eexterndesc' = \eexterndesc[\subst]\\
+ \tyctx.\TCPARENT[\u32_o] \vdashh!EED!_{\{\EDTPEXPORT~\true\}} \eexterndesc'\\
+ \mathit{boundary} \Rightarrow \freeVars{\eexterndesc'} = \varnothing\\
+ \end{array}
+ }{
+ \begin{aligned}
+ \tyctx \vdashh!CDatECT!{}& \DALIAS~\{ \ASORT~\sort, \ATARGET~\ATOUTER~\u32_o~\u32_i \}\\
+ \trelh!CDatECT!{}&\forall\varnothing.\varnothing \to \exists\varnothing.\varnothing\\
+ \dashvh!CDatECT!{}&\tyctx \oplus \eexterndesc'\\
+ \end{aligned}
+ }
+\]
+
+\subsubsection{$\DTYPE~\deftype$}
+\[
+ \frac{
+ \tyctx \vdashh!DTtoEDT! \deftype \leadstoh!DTtoEDT! \edeftype\\
+ }{
+ \begin{aligned}
+ \tyctx \vdashh!CDatECT!{}&\DTYPE~\deftype\\
+ \trelh!CDatECT!{}&\forall\varnothing.\varnothing \to \varnothing\\
+ \dashvh!CDatECT!{}&\tyctx \oplus \{ \TCTYPES~\edeftype \}\\
+ \end{aligned}
+ }
+\]
+
+\subsubsection{$\DTYPE~\{ \RTREP~\mathtt{i32}, \RTDTOR~\funcidx \}$}
+\label{rule:CDatECT:DTYPE}
+\[
+ \frac{
+ }{
+ \begin{aligned}
+ \tyctx
+ \vdashh!CDatECT!{}&\DTYPE~\{ \RTREP~\mathtt{i32}, \RTDTOR~\funcidx \}\\
+ \trelh!CDatECT!{}&\forall \varnothing. \varnothing \to \varnothing\\
+ \dashvh!CDatECT!{}&\tyctx \oplus \{ \TCRTYPES~\{ \ERTREP~\mathtt{i32}, \ERTDTOR~\funcidx \}, \TCTYPES~\EDTRESOURCE~\length{\tyctx.\TCRTYPES} \}
+ \end{aligned}
+ }
+\]
+
+\subsubsection{$\DCANON~\CLIFT~\core:funcidx~\overline{\canonopt_i}~\typeidx$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \tyctx.\TCTYPES[\typeidx] = \efunctype\\
+ \tyctx.\TCCORE.\CTCFUNCS[\core:funcidx] = \F{canon\_lower\_type}(\efunctype, \overline{\canonopt_i})\\
+ \end{array}
+ }{
+ \tyctx \vdashh!CDatECT! \DCANON~\CLIFT~\core:funcidx~\overline{\canonopt_i}~\typeidx
+ \trelh!CDatECT! \varnothing \to \varnothing
+ \dashvh!CDatECT! \tyctx \oplus \{ \TCFUNCS~\efunctype \}
+ }
+\]
+
+\subsubsection{$\DCANON~\CLOWER~\funcidx~\overline{\canonopt_i}$}
+\[
+ \frac{
+ }{
+ \begin{aligned}
+ \tyctx \vdashh!CDatECT!{}&\DCANON~\CLOWER~\funcidx~\overline{\canonopt_i}\\
+ \trelh!CDatECT!{}&\forall\varnothing.\varnothing \to \exists\varnothing.\varnothing\\
+ \dashvh!CDatECT!{}&\tyctx \oplus \{ \tyctx.\TCCORE.\CTCFUNCS~\F{canon\_lower\_type}(\tyctx.\TCFUNCS[\funcidx], \overline{\canonopt_i}) \}\\
+ \end{aligned}
+ }
+\]
+
+\subsubsection{$\DCANON~\CRESOURCENEW~\typeidx$}
+% todo core xref for i32
+\[
+ \frac{
+ \tyctx.\TCTYPES[\typeidx] = \EDTRESOURCE~\rtidx\\
+ }{
+ \begin{aligned}
+ \tyctx \vdashh!CDatECT!{}&\DCANON~\CRESOURCENEW~\typeidx\\
+ \trelh!CDatECt!{}&\forall\varnothing.\varnothing\to\exists\varnothing.\varnothing\\
+ \dashvh!CDatECT!{}&\tyctx\oplus\{\tyctx.\TCCORE.\CTCFUNCS~\i32\to\i32\}\\
+ \end{aligned}
+ }
+\]
+
+\subsubsection{$\DCANON~\CRESOURCEDROP~\typeidx$}
+\[
+ \frac{
+ \exists \edeftype, \tyctx.\TCTYPES[\typeidx] = \EVTOWN~\edeftype \lor \tyctx.\TCTYPES[\typeidx] = \EVTREF~\RSCALL~\edeftype
+ }{
+ \begin{aligned}
+ \tyctx \vdashh!CDatECT!{}&\DCANON~\CRESOURCEDROP~\typeidx\\
+ \trelh!CDatECt!{}&\forall\varnothing.\varnothing\to\exists\varnothing.\varnothing\\
+ \dashvh!CDatECT!{}&\tyctx\oplus\{\tyctx.\TCCORE.\CTCFUNCS~\i32\to\varnothing\}\\
+ \end{aligned}
+ }
+\]
+
+\subsubsection{$\DCANON~\CRESOURCEREP~\typeidx$}
+\[
+ \frac{
+ \tyctx.\TCTYPES[\typeidx] = \EDTRESOURCE~\rtidx\\
+ }{
+ \begin{aligned}
+ \tyctx \vdashh!CDatECT!{}&\DCANON~\CRESOURCEREP~\typeidx\\
+ \trelh!CDatECt!{}&\forall\varnothing.\varnothing\to\exists\varnothing.\varnothing\\
+ \dashvh!CDatECT!{}&\tyctx\oplus\{\tyctx.\TCCORE.\CTCFUNCS~\i32\to\i32\}\\
+ \end{aligned}
+ }
+\]
+
+\subsubsection{$\DSTART~\{ \FFUNC~\funcidx, \FARGS~\overline{\valueidx_i} \}$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \tyctx.\TCFUNCS[\funcidx] = \eparamlist \to \eresultlist\\
+ \tyctx \vdashh!VIsatPL! \overline{\valueidx_i} \trelh!VIsatPL! \eparamlist\\
+ n = \F{length}(\tyctx.\TCVALUES)\\
+ \forall j, \evaltypead'_j = \begin{cases}
+ \tyctx.\TCVALUES[j]^\dagger&
+ {\begin{aligned}
+ \text{if }\exists i\,\forall \deftype,{} & j < n \land j = \valueidx_i\\
+ \land {}&{\eparamlist}_i.\EPLTYPE \neq \EVTREF~\RSCALL~\edeftype\\
+ \end{aligned}}\\
+ \tyctx.\TCVALUES[j]&\text{if }j <n\land j \notin \overline{\valueidx_i}\\
+ {\eresultlist}_{j-n}&\text{otherwise}\\
+ \end{cases}\\
+ \end{array}
+ }{
+ \begin{aligned}
+ \tyctx \vdashh!CDatECT!{}&\DSTART~\{ \FFUNC~\funcidx, \FARGS~\overline{\valueidx_i} \}\\
+ \trelh!CDatECT!{}&\forall\varnothing.\varnothing \to \exists\varnothing.\varnothing\\
+ \dashvh!CDatECT!{}&\tyctx \ominus \{ \TCVALUES \} \oplus \{ \TCVALUES~\overline{\evaltypead'_j} \}\\
+ \end{aligned}
+ }
+\]
+
+\subsubsection{$\DIMPORT~\{ \IDNAME~\name, \IDDESC~\externdesc \}$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \tyctx \vdashh!EDtoEED! \externdesc \leadstoh!EDtoEED! \forall\overline{\boundedtyvar_i}.\eexterndesc\\
+ \tyctx' = \tyctx \oplus \{ \TCVARS~\overline{(\boundedtyvar_i,)} \}\\
+ \tyctx' \vdashh!EED!_{\{\EDTPEXPORT~\true\}} \eexterndesc
+ \end{array}
+ }{
+ \begin{aligned}
+ \tyctx \vdashh!CDatECT!{}&\DIMPORT~\{ \IDNAME~\name, \IDDESC~\externdesc \}\\
+ \trelh!CDatECT!{}&\forall\overline{\boundedtyvar_i}.\{ \EEDNAME~\name, \EEDDESC~\eexterndesc \} \to \exists\varnothing.\varnothing\\
+ \dashvh!CDatECT!{}&\tyctx' \oplus \eexterndesc\\
+ \end{aligned}
+ }
+\]
+
+\subsubsection{$\DEXPORT~\{ \ENAME~\name, \EDEF~\sortidx, \EDESC~\externdesc \}$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \tyctx \vdashh!SIatEED! \sortidx \trelh!SIatEED! \eexterndesc\\
+ \tyctx \vdashh!EDtoEED! \externdesc \leadstoh!EDatEED! \forall\overline{\boundedtyvar_i}.\eexterndesc'\\
+ \forall i, \exists \edeftype_i, \edeftype_i \subtypeof \boundedtyvar_i\\
+ \eexterndesc \subtypeof \eexterndesc'[\overline{\edeftype_i/\boundedtyvar_i}]\\
+ \edeftype^? =
+ \begin{cases}
+ \edeftype & \text{if } \eexterndesc = \EEMDTYPE~\edeftype\\
+ \epsilon & \text{otherwise}
+ \end{cases}\\
+ \Gamma' = \Gamma \oplus \{ \TCVARS~\overline{(\boundedtyvar_i,\edeftype^?)} \}\\
+ \Gamma' \vdashh!EED!_{\{\EDTPEXPORT~\true\}} \eexterndesc'\\
+ \forall j, \evaltypead'_j = \begin{cases}
+ \tyctx.\TCVALUES[j]^\dagger&\text{if }\sortidx.\SISORT=\SVALUE\land \sortidx.\SIIDX = j\\
+ \tyctx.\TCVALUES[j]&\text{otherwise}\\
+ \end{cases}\\
+ \forall k, \einstancetypead'_k = \begin{cases}
+ \overline{{\eexterndecl^\dagger}_l}&
+ \begin{aligned}
+ \text{if }&\sortidx.\SISORT = \SCOMPONENT \land \sortidx.\SIIDX = j\\
+ \land{}&\tyctx.\TCINSTANCES[j] = \overline{\eexterndeclad_l}\\
+ \end{aligned}\\
+ \tyctx.\TCINSTANCES[j]&\text{otherwise}\\
+ \end{cases}\\
+ \end{array}
+ }{
+ \begin{aligned}
+ \tyctx \vdashh!CDatECT!{}&\DEXPORT~\{ \ENAME~\name, \EDEF~\sortidx \}\\
+ \trelh!CDatECT!{}&\forall\varnothing.\varnothing \to \exists\varnothing.\{ \EEDNAME~\name, \EEDDESC~\eexterndesc \}\\
+ \dashvh!CDatECT!{}&\tyctx' \ominus \{ \TCVALUES, \TCINSTANCES \} \oplus \{ \TCVALUES~\overline{\evaltypead'_j}, \TCINSTANCES~\overline{\einstancetypead'_k} \} \oplus \eexterndesc'\\
+ \end{aligned}
+ }
+\]
diff --git a/spec/document/valid/contexts.tex b/spec/document/valid/contexts.tex
new file mode 100644
index 00000000..30f0bb47
--- /dev/null
+++ b/spec/document/valid/contexts.tex
@@ -0,0 +1,72 @@
+\section{Contexts}
+
+Validation rules for individual definitions are interpreted within a
+particular \emph{context}, which contains the information about the
+surrounding component and environment needed to validate a particular
+definition. The validation contexts used in the component model
+contain the types of every definition in every index space currently
+accessible.
+
+Notably, this includes the index spaces of parent components, which
+may be accessed via $\ATOUTER$ aliases. Since child components' outer
+aliases are only allowed to access locally-defined components and core
+modules from their parents' index spaces, we record whether or not we
+are in a child component in $\TCOB$, and the set of locally-defined
+index space items in $\TCLD$. We write $\tyctx.\TCPARENT[\u32]$ to
+mean the result of walking up the chain of $\TCPARENT$ members $\u32$
+times.
+
+Concretely, a validation context is defined as a record with the
+following abstract syntax:
+
+\begin{record-productions}
+ \production{coretyctx}
+ \{
+ \begin{array}[t]{l@{~}ll}
+ \CTCTYPES & \ecoredeftype^\ast, \\
+ \CTCFUNCS & \core:functype^\ast, \\
+ \CTCMODULES & \ecoremoduletype^\ast, \\
+ \CTCINSTANCES & \ecoreinstancetype^\ast, \\
+ \CTCTABLES & \core:tabletype^\ast, \\
+ \CTCMEMS & \core:memtype^\ast, \\
+ \CTCGLOBALS & \core:globaltype^\ast\} \\
+ \end{array}\\
+ \production{tyctx}
+ \{
+ \begin{array}[t]{l@{~}ll}
+ \TCPARENT & \tyctx^{?}, \\
+ \TCOB & \bool,\\
+ \TCLD & \sortidx^\ast \\
+ \TCCORE & \coretyctx, \\
+ \TCVARS & (\boundedtyvar, \edeftype^?)^\ast \\
+ \TCRTYPES & \eresourcetype^\ast, \\
+ \TCTYPES & \edeftype^\ast, \\
+ \TCCOMPONENTS & \ecomponenttype^\ast, \\
+ \TCINSTANCES & \einstancetypead^\ast, \\
+ \TCFUNCS & \efunctype^\ast, \\
+ \TCVALUES & \evaltypead^\ast, \} \\
+ \end{array}\\
+\end{record-productions}
+
+\subsection{Resolving type variables}
+
+It is occasionally useful to produce a substitution which eliminates
+all of the variables in a context whose definitions are (locally)
+known. To this end, we define a metafunction $\resolveVars{\Gamma}$,
+which produces such a substitution.
+
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \subst_0 = \varnothing\\
+ \forall i, \subst_i =
+ \begin{cases}
+ \subst_{i-1}[\edeftype_i] & \text{if } \edeftype^?_i = \edeftype_i\\
+ \subst_{i-1}[\edeftype/\alpha] & \text{if } \boundedtyvar_i = (\alpha : \TBEQ~\edeftype)\\
+ \subst_{i-1} & \text{otherwise}
+ \end{cases}
+ \end{array}
+ }{
+ \subst_n \cup \resolveVars{\Gamma} = \resolveVars{\{ \TCPARENT~\Gamma, \TCVARS~\overline{(\boundedtyvar_i, \edeftype^?_i)}^n \}}
+ }
+\]
diff --git a/spec/document/valid/conventions.tex b/spec/document/valid/conventions.tex
new file mode 100644
index 00000000..78cf63e0
--- /dev/null
+++ b/spec/document/valid/conventions.tex
@@ -0,0 +1,23 @@
+\section{Conventions}
+
+As in Core WebAssembly, a \emph{validation} stage checks that a
+component is well-formed, and only valid components may be
+instantiated.
+
+Similarly to Core WebAssembly, a \emph{type system} over the abstract
+syntax of a component is used to specify which modules are valid, and
+the rules governing the validity of a component are given in both
+prose and formal mathematical notation.
+
+\subsection{Notation}
+
+Both the formal and prose notation share a number of constructs:
+
+\begin{itemize}
+\item When writing a value of the abstract syntax, any component of
+ the abstract syntax which has the form $\X{nonterminal}^n$,
+ $\X{nonterminal}^\ast$, $\X{nonterminal}^{+}$, or
+ $\X{nonterminal}^{?}$, we may write $\overline{\dots_i}^n$ to mean
+ that this position is filled by a series of $n$ abstract values,
+ named $\dots_1$ to $\dots_n$.
+\end{itemize}
diff --git a/spec/document/valid/elaboration.tex b/spec/document/valid/elaboration.tex
new file mode 100644
index 00000000..78fab02a
--- /dev/null
+++ b/spec/document/valid/elaboration.tex
@@ -0,0 +1,897 @@
+\section{Type Elaboration}
+
+
+\subsection{Primitive Value Types}
+\label{judgment:PVTtoEVT}
+
+\fbox{$\tyctx \vdashh!PVTtoEVT! \primvaltype \leadstoh!PVTtoEVT! \evaltype$}
+
+Any $\primvaltype$ elaborates to a a $\evaltype$.
+
+\subsubsection{$\VTSTRING$}
+
+\[
+ \frac{
+ }{
+ \tyctx \vdashh!PVTtoEVT! \VTSTRING \leadstoh!PVTtoEVT! \EVTLIST~\EVTCHAR
+ }
+\]
+
+\subsubsection{$\primvaltype$ other than $\VTSTRING$}
+
+\[
+ \frac{
+ \primvaltype \neq \VTSTRING
+ }{
+ \tyctx \vdashh!PVTtoEVT! \primvaltype \leadstoh!PVTtoEVT! \primvaltype
+ }
+\]
+
+\subsection{Record Fields}
+\label{judgment:RFtoERF}
+\fbox{$\tyctx \vdashh!RFtoERF! \recordfield \leadstoh!RFtoERF! \erecordfield$}
+
+
+\[
+ \frac{
+ \tyctx \vdashh!VTtoEVT! \valtype \leadstoh!VTtoEVT! \evaltype
+ }{
+ \tyctx \vdashh!RFtoERF! \{ \RFNAME~\name, \RFTYPE~\valtype \}
+ \leadstoh!RFtoERF! \{ \ERFNAME~\name, \ERFTYPE~\evaltype \}
+ }
+\]
+
+\subsection{Variant Cases}
+\label{judgment:VCtoEVC}
+\fbox{$\vcctx \vdashh!VCtoEVC! \variantcase \leadstoh!VCtoEVC! \evariantcase$}
+
+Because validation must ensure that a variant case which refines
+another case has a compatible type, a variant case elaborates to a
+$\evariantcase$ in a special context $\vcctx$:
+
+\begin{record-production}{vcctx}
+ \{ \VCCCTX~\tyctx, \VCCCASES~\evariantcase^{*} \}
+\end{record-production}
+
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \forall i, \vcctx.\VCCCTX \vdashh!VTtoEVT! \valtype_i \leadstoh!VTtoEVT! {\evaltype}_i\\
+ \forall j, \vcctx.\VCCCASES[\u32_j] = \{ \EVCNAME~\name_j, \EVCTYPE~\overline{{\evaltype'}_k}, \dots \} \land \forall i, {\evaltype}_i \subtypeof {\evaltype'}_i
+ \end{array}
+ }{
+ \vcctx \vdashh!VCtoEVC! \{ \VCNAME~\name, \VCTYPE~\overline{\valtype_i}, \VCREFINES~\overline{\u32_j} \}
+ \leadstoh!VCtoEVC! \{ \EVCNAME~\name, \EVCTYPE~\overline{{\evaltype}_i}, \VCREFINES~\overline{\name_j} \}
+ }
+\]
+
+\subsection{Defined Value Types}
+\label{judgment:DVTtoEVT}
+\fbox{$\tyctx \vdashh!DVTtoEVT! \defvaltype \leadstoh!DVTtoEVT! \evaltype$}
+
+A defined value type elaborates to a $\evaltype$.
+
+\subsubsection{$\VTPRIM~\primvaltype$}
+
+\[
+ \frac{
+ \tyctx \vdashh!PVTtoEVT! \primvaltype \leadstoh!PVTtoEVT! \evaltype
+ }{
+ \tyctx \vdashh!DVTtoEVT! \VTPRIM~\primvaltype \leadstoh!DVTtoEVT! \evaltype
+ }
+\]
+
+\subsubsection{$\VTRECORD~\recordfield^{+}$}
+
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \forall i, \tyctx \vdashh!RFtoERF! \recordfield_i \leadstoh!RFtoERF! {\erecordfield}_i\\
+ \forall i j, {\erecordfield}_i.\ERFNAME = {\erecordfield}_j.\ERFNAME \Rightarrow i = j
+ \end{array}
+ }{
+ \tyctx \vdashh!DVTtoEVT! \VTRECORD~\overline{{\recordfield}_i}^n
+ \leadstoh!DVTtoEVT! \EVTRECORD~\overline{{\erecordfield}_i}^n
+ }
+\]
+
+\subsubsection{$\VTVARIANT~\variantcase^{+}$}
+
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \forall i, \{ \VCCCTX~\Gamma, \VCCCASES~{\evariantcase}_1,\dots,{\evariantcase}_{i-1} \} \vdashh!VCtoEVC! \variantcase_i \leadstoh!VCtoEVC! {\evariantcase}_i\\
+ \forall i, j {\evariantcase}_i.\EVCNAME = {\evariantcase}_j.\EVCNAME \Rightarrow i = j
+ \end{array}
+ }{
+ \tyctx \vdashh!DVTtoEVT! \VTVARIANT~\overline{\variantcase_i}^n
+ \leadstoh!DVTtoEVT! \EVTVARIANT~\overline{{\evariantcase}_i}^n
+ }
+\]
+
+\subsubsection{$\VTLIST~\valtype$}
+\[
+ \frac{
+ \tyctx \vdashh!VTtoEVT! \valtype \leadstoh!VTtoEVT! \evaltype
+ }{
+ \tyctx \vdashh!DVTtoEVT! \VTLIST~\valtype \leadstoh!DVTtoEVT! \EVTLIST~\evaltype
+ }
+\]
+
+\subsubsection{$\VTTUPLE~\overline{\valtype_i}$}
+\[
+ \frac{
+ \forall i, \tyctx \vdashh!VTtoEVT! \valtype_i \leadstoh!VTtoEVT! {\evaltype}_i
+ }{
+ \tyctx \vdashh!DVTtoEVT! \VTTUPLE~\overline{\valtype_i}
+ \leadstoh!DVTtoEVT! \EVTRECORD~\overline{\{\ERFNAME~''i'',\ERFTYPE~{\evaltype}_i\}}
+ }
+\]
+
+\subsubsection{$\VTFLAGS~\overline{\name_i}$}
+\[
+ \frac{
+ }{
+ \tyctx \vdashh!DVTtoEVT! \VTFLAGS~\overline{\name_i}
+ \leadstoh!DVTtoEVT! \EVTRECORD~\overline{\{\ERFNAME~\name_i, \ERFTYPE~\EVTBOOL\}}
+ }
+\]
+
+\subsubsection{$\VTENUM~\overline{\name_i}$}
+
+\[
+ \frac{
+ }{
+ \tyctx \vdashh!DVTtoEVT! \VTENUM~\overline{\name_i}
+ \leadstoh!DVTtoEVT! \VTVARIANT~\overline{\{\EVCNAME~\name_i\}}
+ }
+\]
+
+\subsubsection{$\VTOPTION~\valtype$}
+
+\[
+ \frac{
+ \tyctx \vdashh!VTtoEVT! \valtype \leadstoh!VTtoEVT! \evaltype
+ }{
+ \tyctx \vdashh!DVTtoEVT! \VTOPTION~\valtype
+ \leadstoh!DVTtoEVT! \EVTVARIANT~\{ \EVCNAME~''none'' \}~\{ \EVCNAME~''some'', \EVCTYPE~\evaltype \}
+ }
+\]
+
+\subsubsection{$\VTUNION~\overline{\valtype_i}$}
+\[
+ \frac{
+ \forall i, \tyctx \vdashh!VTtoEVT! \valtype_i \leadstoh!VTtoEVT! {\evaltype}_i
+ }{
+ \tyctx \vdashh!DVTtoEVT! \VTUNION~\overline{\valtype_i}
+ \leadstoh!DVTtoEVT! \EVTVARIANT~\overline{\{\EVCNAME~''i'', \EVCTYPE~{\evaltype}_i\}}
+ }
+\]
+
+\subsubsection{$\VTRESULT~\overline{\valtype_i}~\overline{\valtype'_j}$}
+
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \forall i, \tyctx \vdashh!VTtoEVT! \valtype_i \leadstoh!VTtoEVT! {\evaltype}_i\\
+ \forall j, \tyctx \vdashh!VTtoEVT! \valtype'_j \leadstoh!VTtoEVT! {\evaltype'}_j\\
+ \end{array}
+ }{
+ \begin{aligned}
+ \tyctx\vdash!DVTtoEVT!{}&\VTRESULT~\overline{\valtype_i}~\overline{\valtype'_j}\\
+! \leadstoh!DVTtoEVT!{}&\EVTVARIANT~\{\EVCNAME~''ok'',! \EVCTYPE~\overline{{\evaltype}_i}\}~\{\EVCNAME~''error'', \EVCTYPE~\overline{{\evaltype'}_j}\}\\
+ \end{aligned}
+ }
+\]
+
+\subsubsection{$\VTOWN~\typeidx$}
+
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \tyctx.\TCTYPES[\typeidx] = \edeftype\\
+ \edeftype \subtypeof \ESUBRESOURCE\\
+ \end{array}
+ }{
+ \tyctx \vdashh!DVTtoEVT! \VTOWN~\typeidx \leadstoh!DVTtoEVT! \EVTOWN~\edeftype
+ }
+\]
+
+\subsubsection{$\VTBORROW~\typeidx$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \tyctx.\TCTYPES[\typeidx] = \edeftype\\
+ \edeftype \subtypeof \ESUBRESOURCE\\
+ \end{array}
+ }{
+ \tyctx \vdashh!DVTtoEVT! \VTBORROW~\typeidx \leadstoh!DVTtoEVT! \EVTREF~\RSCALL~\edeftype
+ }
+\]
+
+\subsection{Value Types}
+\label{judgment:VTtoEVT}
+\fbox{$\tyctx \vdashh!VTtoEVT! \valtype \leadstoh!VTtoEVT! \evaltype$}
+
+\subsubsection{$\primvaltype$}
+\[
+ \frac{
+ \tyctx \vdashh!PVTtoEVT! \primvaltype \leadstoh!PVTtoEVT! \evaltype
+ }{
+ \tyctx \vdashh!VTtoEVT! \primvaltype \leadstoh!VTtoEVT! \evaltype
+ }
+\]
+
+\subsubsection{$\typeidx$}
+\[
+ \frac{
+ }{
+ \tyctx \vdashh!VTtoEVT! \typeidx \leadstoh!VTtoEVT! \tyctx.\TCTYPES[\typeidx]
+ }
+\]
+
+\subsection{Value Type Well-formedness}
+\label{judgment:EVT}
+\fbox{$\tyctx \vdashh!EVT!_\evaltypepos \evaltype$}
+
+Since certain value types cannot appear in certain places (notably,
+$\EVTREF~\RSCALL$ may not appear in a function result type), we define
+a family of well-formedness judgments. Each context which may require
+a $\evaltype$ uses one of these well-formedness judgments to ensure
+that it is of correct form.
+
+Note that the variable scoping constraints should already be enforced
+by earlier elaboration stages, which never generate free type
+variables, but they are included here for completeness.
+
+We define a formal syntax of the position parameters which may be
+used. In addition to recording whether or not the present type is a
+function result type, it records whether or not the type is being
+exported, in which case bare resource types are not allowed.
+
+\begin{record-production}{evaltypepos}
+ \{ \EVTPRESULT~\bool, \EVTPEXPORT~\bool \}
+\end{record-production}
+
+\subsubsection{Primitive value types}
+\[
+ \frac{
+ \evaltype \in \{ \EVTBOOL, \EVTS8, \EVTU8, \EVTS16, \EVTU16, \EVTS32, \EVTU32, \EVTS64, \EVTU64, \EVTFLOAT32, \EVTFLOAT64, \EVTCHAR \}
+ }{
+ \tyctx \vdashh!EVT!_\evaltypepos \evaltype
+ }
+\]
+
+\subsubsection{$\EVTLIST~\evaltype$}
+\[
+ \frac{
+ \tyctx \vdashh!EVT!_\evaltypepos \evaltype
+ }{
+ \tyctx \vdashh!EVT!_\evaltypepos \EVTLIST~\evaltype
+ }
+\]
+
+\subsubsection{$\EVTRECORD~\erecordfield^{\ast}$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \forall i j, i \neq j \Rightarrow \name_i \neq name_j\\
+ \forall i, \tyctx \vdashh!EVT!_\evaltypepos {\evaltype}_i\\
+ \end{array}
+ }{
+ \tyctx \vdashh!EVT!_\evaltypepos
+ \EVTRECORD~\overline{\ERFNAME~\name_i, \ERFTYPE~{\evaltype}_i}
+ }
+\]
+
+\subsubsection{$\EVTVARIANT~\evariantcase^{+}$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \forall i j, i \neq j \Rightarrow \name_i \neq \name_j\\
+ \forall i, \forall \evaltype, {\evaltype^?}_i = \evaltype \Rightarrow \tyctx \vdashh!EVT!_\evaltypepos \evaltype\\
+ \end{array}
+ }{
+ \tyctx \vdashh!EVT!_\evaltypepos
+ \EVTVARIANT~\overline{\EVCNAME~\name_i, \EVCTYPE~{\evaltype^?}_i, \EVCREFINES~\u32^?_i}^n
+ }
+\]
+
+\subsubsection{$\EVTOWN~\edeftype$}
+\[
+ \frac{
+ \tyctx \vdashh!EDT!_\evaltypepos \edeftype\\
+ \tyctx \vdash \edeftype \subtypeof \ESUBRESOURCE
+ }{
+ \tyctx \vdashh!EVT!_\evaltypepos \EVTOWN~\edeftype
+ }
+\]
+
+\subsubsection{$\EVTREF~\edeftype$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \neg \evaltypepos.\EVTPRESULT\\
+ \tyctx \vdashh!EVT!_\evaltypepos \EVTOWN~\edeftype
+ \end{array}
+ }{
+ \tyctx \vdashh!EVT!_\evaltypepos \EVTREF~\RSCALL~\edeftype
+ }
+\]
+
+\subsection{Parameter Lists}
+\label{judgment:PLtoEPL}
+\fbox{$\tyctx \vdashh!PLtoEPL! \paramlist \leadstoh!PLtoEPL! \eparamlist$}
+
+Any $\paramlist$ elaborates to a $\eparamlist$.
+
+\subsubsection{$\overline{\{\PLNAME~\name_i, \PLTYPE~\valtype_i\}}$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \forall i, \tyctx \vdashh!VTtoEVT! \valtype_i \leadstoh!VTtoEVT! {\evaltype}_i\\
+ \forall i, \tyctx \vdashh!EVT!_{\{\EVTPRESULT~\false,\EVTPEXPORT~\false\}} {\evaltype}_i\\
+ \end{array}
+ }{
+ \tyctx \vdashh!PLtoEPL! \overline{\{\PLNAME~\name_i,
+ \PLTYPE~\valtype_i\}} \leadstoh!PLtoEPL! \overline{\{\EPLNAME~\name_i,
+ \EPLTYPE~{\evaltype}_i\}}
+ }
+\]
+
+\subsection{Parameter List Well-formedness}
+\label{judgment:EPL}
+\fbox{$\tyctx \vdashh!EPL! \eparamlist$}
+
+We define an analogous well-formedness judgment for parameter lists.
+Since parameter lists may only occur in parameter position, we define
+another syntax of position parameters which does not include the
+information about whether or not the type appears in parameter
+positoin; this version of the syntax will be used for all defined type
+well-formedness judgments, since defined types other than resources
+may not appear inside function parameter or return lists:
+
+\begin{record-production}{edeftypepos}
+ \{ \EDTPEXPORT~\bool \}
+\end{record-production}
+
+\subsubsection{$\overline{\{\EPLNAME~\name_i, \EPLTYPE~\evaltype_i\}}$}
+\[
+ \frac{
+ \forall i, \tyctx \vdashh!EVT!_{\{\EVTPRESULT~\false,\EVTPEXPORT~\edeftypepos.\EDTPEXPORT\}} \evaltype_i
+ }{
+ \tyctx \vdashh!EPL!_\edeftypepos \{\EPLNAME~\name_i, \EPLTYPE~\evaltype_i\}
+ }
+\]
+
+\subsection{Result Lists}
+\label{judgment:RLtoERL}
+\fbox{$\tyctx \vdashh!RLtoERL! \resultlist \leadstoh!RLtoERL! \eparamlist$}
+
+Any $\resultlist$ elaborates to a $\eresultlist$.
+
+\subsubsection{$\valtype$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \tyctx \vdashh!VTtoEVT! \valtype \leadstoh!VTtoEVT! \evaltype\\
+ \tyctx \vdashh!EVT!_{\{\EVTPRESULT~\true,\EVTPEXPORT~\false\}} \evaltype\\
+ \end{array}
+ }{
+ \tyctx \vdashh!RLtoERL! \valtype \leadstoh!RLtoERL! \evaltype
+ }
+\]
+
+\subsubsection{$\overline{\{\RLNAME~\name_i, \RLTYPE~\valtype_i\}}$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \forall i, \tyctx \vdashh!VTtoEVT! \valtype_i \leadstoh!VTtoEVT! {\evaltype}_i\\
+ \forall i, \tyctx \vdashh!EVT!_{\{\EVTPRESULT~\true,\EVTPEXPORT~\false\}} {\evaltype}_i\\
+ \end{array}
+ }{
+ \tyctx \vdashh!RLtoERL! \overline{\{\RLNAME~\name_i,
+ \RLTYPE~\valtype_i\}} \leadstoh!RLtoERL! \overline{\{\ERLNAME~\name_i,
+ \ERLTYPE~{\evaltype}_i\}}
+ }
+\]
+
+\subsection{Result List Well-formedness}
+\label{judgment:ERL}
+
+\subsubsection{$\evaltype$}
+\[
+ \frac{
+ \tyctx \vdashh!EVT!_{\{\EVTPRESULT~\true,\EVTPEXPORT~\edeftypepos.\EDTPEXPORT\}} \evaltype
+ }{
+ \tyctx \vdashh!ERL!_\edeftypepos \evaltype
+ }
+\]
+
+\subsubsection{$\overline{\{\ERLNAME~\name_i, \ERLTYPE~\evaltype_i\}}$}
+\[
+ \frac{
+ \forall i, \tyctx \vdashh!EVT!_{\{\EVTPRESULT~\true,\EVTPEXPORT~\edeftypepos.\EDTPEXPORT\}} \evaltype_i
+ }{
+ \tyctx \vdashh!ERL!_\edeftypepos \{\ERLNAME~\name_i, \ERLTYPE~\evaltype_i\}
+ }
+\]
+
+\subsection{Function types}
+\label{judgment:FTtoEFT}
+\fbox{$\tyctx \vdashh!FTtoEFT! \functype \leadstoh!FTtoEFT! \efunctype$}
+
+Any $\functype$ elaborates to a $\efunctype$.
+
+\subsubsection{$\paramlist \to \resultlist$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \tyctx \vdashh!PLtoEPL! \paramlist \leadstoh!PLtoEPL! \eparamlist\\
+ \tyctx \vdashh!RLtoERL! \resultlist \leadstoh!RLtoERL! \eresultlist\\
+ \end{array}
+ }{
+ \tyctx \vdashh!FTtoEFT! \paramlist\to\resultlist
+ \leadstoh!FTtoEFT! \eparamlist\to\eresultlist
+ }
+\]
+
+\subsection{Type Bounds}
+\label{judgment:TBtoETB}
+\fbox{$\tyctx \vdashh!TBtoETB! \typebound \leadstoh!TBtoETB! \etypebound$}
+
+A type bound elaborates to a $\etypebound$.
+
+\subsubsection{$\TBEQ~\typeidx$}
+\[
+ \frac{
+ }{
+ \tyctx \vdashh!TBtoETB! \TBEQ~\typeidx \leadstoh!TBtoETB! \ETBEQ~\tyctx.\TCTYPES[\typeidx]
+ }
+\]
+
+\subsubsection{$\TBSUBR$}
+\[
+ \frac{
+ }{
+ \tyctx \vdashh!TBtoETB! \TBSUBR \leadstoh!TBtoETB! \ETBSUBR
+ }
+\]
+
+\subsection{Extern Descriptors}
+\label{judgment:EDtoEED}
+\fbox{$\tyctx \vdashh!EDtoEED! \externdesc \leadstoh!EDtoEED! \forall \overline{\boundedtyvar}. \eexterndesc$}
+
+An extern descriptor elaborates to a quantified $\eexterndesc$. The
+quantifiers track type variables that are introduced by the
+$\externdesc$, but which have no place in the $\eexterndesc$; in
+particular, those introduced by type and instance imports/exports.
+
+\subsubsection{$\EDTYPE~\typebound$}
+\[
+ \frac{
+ \tyctx \vdashh!TBtoETB! \typebound \leadstoh!TBtoETB! \etypebound
+ }{
+ \tyctx \vdashh!EDtoEED! \EDTYPE~\typebound \leadstoh!EDtoEED! \forall(\tyvar : \etypebound).\EEMDTYPE~\tyvar
+ }
+\]
+
+\subsubsection{$\EDCOREMODULE~\core:typeidx$}
+\[
+ \frac{
+ \tyctx.\TCCORE.\CTCTYPES[\core:typeidx] = \ecoremoduletype
+ }{
+ \tyctx \vdashh!EDtoEED! \EDCOREMODULE~\core:typeidx \leadstoh!EDtoEED! \forall\varnothing.\EEMDCOREMODULE~\ecoremoduletype
+ }
+\]
+
+\subsubsection{$\EDFUNC~\typeidx$}
+\[
+ \frac{
+ \tyctx.\TCTYPES[\typeidx] = \efunctype
+ }{
+ \tyctx \vdashh!EDtoEED! \EDFUNC~\typeidx \leadstoh!EDtoEED! \forall\varnothing.\EEMDFUNC~\efunctype
+ }
+\]
+
+\subsubsection{$\EDVALUE~\typeidx$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \tyctx.\TCTYPES[\typeidx] = \evaltype\\
+ \tyctx \vdashh!EVT! \evaltype\\
+ \end{array}
+ }{
+ \tyctx \vdashh!EDtoEED! \EDVALUE~\typeidx \leadstoh!EDtoEED! \forall\varnothing.\EEMDVALUE~\evaltype
+ }
+\]
+
+\subsubsection{$\EDINSTANCE~\typeidx$}
+\[
+ \frac{
+ \tyctx.\TCTYPES[typeidx] = \exists\boundedtyvar^\ast.\einstancetype
+ }{
+ \tyctx \vdashh!EDtoEED! \EDINSTANCE~\typeidx \leadstoh!EDtoEED! \forall\boundedtyvar^\ast.\EEMDINSTANCE~\einstancetype
+ }
+\]
+
+\subsubsection{$\EDCOMPONENT~\typeidx$}
+\[
+ \frac{
+ \tyctx.\TCTYPES[\typeidx] = \ecomponenttype
+ }{
+ \tyctx \vdashh!EDtoEED! \EDCOMPONENT~\typeidx \leadstoh!EDtoEED! \forall\varnothing.\EEMDCOMPONENT~\ecomponenttype
+ }
+\]
+
+\subsection{Extern Descriptor Well-formedness}
+\label{judgment:EED}
+\fbox{$\tyctx \vdashh!EED!_\edeftypepos \eexterndesc$}
+
+\subsubsection{$\EEMDCOREMODULE~\ecoremoduletype$}
+\[
+ \frac{
+ }{
+ \tyctx \vdashh!EED!_\edeftypepos \EEMDCOREMODULE~\ecoremoduletype
+ }
+\]
+
+\subsubsection{$\eexterndesc$ other than $\EEMDCOREMODULE$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ K \in \{ \EEMDFUNC, \EEMDVALUE, \EEMDTYPE, \EEMDINSTANCE, \EEMDCOMPONENT \}\\
+ \tyctx \vdashh!EDT!_\edeftypepos \edeftype\\
+ \end{array}
+ }{
+ \tyctx \vdashh!EED!_\edeftypepos K~\edeftype
+ }
+\]
+
+\subsection{Instance Declarators}
+\label{judgment:IDtoEIT}
+\fbox{$\tyctx \vdashh!IDtoEIT! \instancedecl \leadstoh!IDtoEIT! \exists \boundedtyvar^\ast. \einstancetype \dashvh!IDtoEIT! \tyctx'$}
+
+Each instance declarator elaborates to a quantified (partial)
+$\einstancetype$ and an updated context, reflecting the effect of the
+declarator on the component's index spaces.
+
+\subsubsection{$\IDALIAS~\{ \ASORT~\sort, \ATARGET~\ATEXPORT~\instanceidx~\name \}$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \sort \in \{ \STYPE, \SINSTANCE \}\\
+ \tyctx.\TCINSTANCES[\instanceidx] = \overline{{\eexterndeclad}_i}\\
+ \exists i, \eexterndeclad_i.\EEDNAME = \name
+ \end{array}
+ }{
+ \begin{aligned}
+ \tyctx \vdashh!IDtoEIT!{}& \IDALIAS~\{\ASORT~\sort, \ATARGET~\ATEXPORT~\instanceidx~\name \}\\ \leadstoh!IDtoEIT!{}& \exists\varnothing. \varnothing \\\dashvh!IDtoEIT!{}& \tyctx \oplus \{ \F{index\_space}(\sort)~\eexterndeclad_i.\EEDDESC \}
+ \end{aligned}
+ }
+\]
+
+\subsubsection{$\IDALIAS~\{ \ASORT~\sort, \ATARGET~\ATOUTER~\u32_o~\u32_i\}$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \sort = \STYPE\\
+ \edeftype = \tyctx.\TCPARENT[\u32_o].\TCTYPES[\u32_i]\\
+ \mathit{boundary} = \bigvee_{j < \u32_o} \tyctx.\TCPARENT[j].\TCOB\\
+ \subst = \begin{cases}\resolveVars{\tyctx.\TCPARENT[\u32_o]} & \text{if } \mathit{boundary}\\\varnothing&\text{otherwise}\end{cases}\\
+ \edeftype' = \edeftype[\subst]\\
+ \tyctx.\TCPARENT[\u32_o] \vdashh!EDT!_{\{\EDTPEXPORT~\true\}} \edeftype'\\
+ \mathit{boundary} \Rightarrow \freeVars{\edeftype'} = \varnothing
+ \end{array}
+ }{
+ \tyctx \vdashh!IDtoEIT! \IDALIAS~\{\ASORT~\sort, \ATARGET~\ATOUTER~\u32_o~\u32_i\} \leadstoh!IDtoEIT!
+ \exists\varnothing. \varnothing \dashvh!IDtoEIT! \tyctx \oplus \{ \TCTYPES~\edeftype' \}
+ }
+\]
+
+\subsubsection{$\IDTYPE~\deftype$}
+\[
+ \frac{
+ \tyctx \vdashh!DTtoEDT! \deftype \leadstoh!DTtoEDT! \edeftype
+ }{
+ \tyctx \vdashh!IDtoEIT! \IDTYPE~\deftype \leadstoh!IDtoEIT!
+ \exists\varnothing. \varnothing
+ \dashvh!IDtoEIT! \tyctx \oplus \{ \TCTYPES~\edeftype \}
+ }
+\]
+
+\subsubsection{$\IDEXPORT~\exportdecl$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \tyctx \vdashh!EDtoEED! \exportdecl.\EDDESC \leadstoh!EDtoEED! \forall\overline{\boundedtyvar_i}.\eexterndesc\\
+ \tyctx' = \tyctx \oplus \{ \TCVARS~\overline{(\boundedtyvar_i,)}\\
+ \tyctx' \vdashh!EED!_{\{\EDTPEXPORT~\true\}} \eexterndesc\\
+ \end{array}
+ }{
+ \begin{aligned}
+ \tyctx \vdashh!IDtoEIT!{}& \exportdecl\\
+ \leadstoh!IDtoEIT!{}&\exists\overline{\boundedtyvar_i}. \{ \EEDNAME~\exportdecl.\EDNAME, \EEDDESC~\eexterndesc \}\\
+ \dashvh!IDtoEIT!{}& \tyctx' \oplus \eexterndesc
+ \end{aligned}
+ }
+\]
+
+\subsection{Component declarators}
+\label{judgment:CDtoECT}
+\fbox{$\tyctx \vdashh!CDtoECT! \componentdecl \leadstoh!CDtoECT! \ecomponenttype \dashvh!CDtoECT! \tyctx'$}
+
+Each component declarator elaborates to a (partial)
+$\ecomponenttype$ and an updated context, reflecting the effect
+of the declarator on the component's index spaces.
+
+\subsubsection{$\instancedecl$}
+\[
+ \frac{
+ \tyctx \vdashh!IDtoEIT! \instancedecl \leadstoh!IDtoEIT! \exists \boundedtyvar^\ast. \einstancetype \dashvh!IDtoEIT! \tyctx'
+ }{
+ \tyctx \vdashh!CDtoECT! \instancedecl \leadstoh!CDtoECT! \forall\varnothing. \varnothing \to \exists \boundedtyvar^\ast. \einstancetype \dashvh!CDtoECT! \tyctx'
+ }
+\]
+
+\subsubsection{$\importdecl$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \tyctx \vdashh!EDtoEED! \importdecl.\IDDESC \leadstoh!EDtoEED! \forall\overline{\boundedtyvar_i}. \eexterndesc\\
+ \tyctx' = \tyctx \oplus \{ \TCVARS~\overline{(\boundedtyvar_i,)} \}\\
+ \tyctx' \vdashh!EED!_{\{\EDTPEXPORT~\true\}} \eexterndesc\\
+ \end{array}
+ }{
+ \begin{aligned}
+ \tyctx \vdashh!CDtoECT!{}&\importdecl\\
+ \leadstoh!CDtoECT!{}&\forall\overline{\boundedtyvar_i}. \{\EEDNAME~\importdecl.\IDNAME, \EEDDESC~\eexterndesc\} \to \exists \varnothing. \varnothing\\
+ \dashvh!CDtoECT!{}&\tyctx' \oplus \eexterndesc
+ \end{aligned}
+ }
+\]
+
+\subsection{Instance Types}
+\label{judgment:ITtoEIT}
+\fbox{$\tyctx \vdashh!ITtoEIT! \instancetype \leadstoh!ITtoEIT! \einstancetype$}
+
+A surface instance type elaborates to a quantified elaborated instance
+type $\exists \boundedtyvar^\ast. \einstancetype$.
+
+\subsubsection{$\overline{\instancedecl_i}$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \tyctx_0 = \{ \TCPARENT~\tyctx \}\\
+ \forall i, \tyctx_{i-1} \vdashh!IDtoEIT! \instancedecl_i
+ \leadstoh!IDtoEIT! \exists \boundedtyvar^\ast_i. \einstancetype_i \dashvh!IDtoEIT! \tyctx_i\\
+ \einstancetype = \bigoplus_i {\einstancetype}_i \\
+ \tyctx_n.\TCVARS \cap \freeVars{\einstancetype} = \varnothing\\
+ \end{array}
+ }{
+ \tyctx \vdashh!ITtoEIT! \overline{\instancedecl_i}^n
+ \leadstoh!ITtoEIT! \exists \overline{\boundedtyvar^\ast_i}. \einstancetype
+ }
+\]
+
+\subsection{Component Types}
+\label{judgment:CTtoECT}
+\fbox{$\tyctx \vdashh!CTtoECT! \componenttype \leadstoh!CTtoECT! \ecomponenttype$}
+
+\subsubsection{$\overline{\componentdecl_i}$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \tyctx_0 = \{ \TCPARENT~\tyctx \}\\
+ \forall i, \tyctx_{i-1} \vdashh!CDtoECT! \componentdecl_i \leadstoh!CDtoECT! \ecomponenttype_i \dashvh!CDtoECT! \tyctx_i\\
+ \ecomponenttype = \bigoplus_i \ecomponenttype_i\\
+ \tyctx_n.\TCVARS \cap \freeVars{\ecomponenttype} = \varnothing\\
+ \end{array}
+ }{
+ \tyctx \vdashh!CTtoECT! \overline{\componentdecl_i}^n
+ \leadstoh!CTtoECT! \ecomponenttype
+ }
+\]
+
+\subsection{Defined Types}
+\label{judgment:DTtoEDT}
+\fbox{$\tyctx \vdashh!DTtoEDT! \deftype \leadstoh!DTtoEDT! \edeftype$}
+
+A $\deftype$ elaborates to a $\edeftype$.
+
+In general, a $\deftype$ of the form $\resourcetype$ does not
+elaborate to any $\edeftype$; however, the component $\DTYPE$
+declarator \hyperref[rule:CDatECT:DTYPE]{generates} a new context
+entry for the resource in question and produces an appropriate
+$\EDTRESOURCE$ type.
+
+\subsubsection{$\defvaltype$}
+\[
+ \frac{
+ \tyctx \vdashh!DVTtoEVT! \defvaltype \leadstoh!DVTtoEVT! \evaltype
+ }{
+ \tyctx \vdashh!DTtoEDT! \defvaltype \leadstoh!DTtoEDT! \evaltype
+ }
+\]
+
+\subsubsection{$\functype$}
+\[
+ \frac{
+ \tyctx \vdashh!FTtoEFT! \functype \leadstoh!FTtoEFT! \efunctype
+ }{
+ \tyctx \vdashh!DTtoEDT! \functype \leadstoh!DTtoEDT! \efunctype
+ }
+\]
+
+\subsubsection{$\componenttype$}
+\[
+ \frac{
+ \tyctx \vdashh!CTtoECT! \componenttype \leadstoh!CTtoECT! \ecomponenttype
+ }{
+ \tyctx \vdashh!DTtoEDT! \componenttype \leadstoh!DTtoEDT! \ecomponenttype
+ }
+\]
+
+\subsubsection{$\instancetype$}
+\[
+ \frac{
+ \tyctx \vdashh!ITtoEIT! \instancetype \leadstoh!ITtoEIT! \exists \boundedtyvar^\ast. \einstancetype
+ }{
+ \tyctx \vdashh!DTtoEDT! \instancetype \leadstoh!DTtoEDT! \exists \boundedtyvar^\ast. \einstancetype
+ }
+\]
+
+\subsection{Defined Type Well-formedness}
+\label{judgment:EDT}
+\fbox{$\tyctx \vdashh!EDT!_\edeftypepos \edeftype$}
+
+\subsubsection{$\tyvar$}
+\[
+ \frac{
+ \tyvar \in \bigcup_i \tyctx.\TCPARENT[i].\TCVARS
+ }{
+ \tyctx \vdashh!EDT!_\edeftypepos \tyvar
+ }
+\]
+
+\subsubsection{$\EDTRESOURCE~\rtidx$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \neg \edeftypepos.\EVTPEXPORT \\
+ \rtidx \in \tyctx.\TCRTYPES\\
+ \end{array}
+ }{
+ \tyctx \vdashh!EDT!_\edeftypepos \EDTRESOURCE~\rtidx
+ }
+\]
+
+\subsubsection{$\evaltype$}
+\[
+ \frac{
+ \tyctx \vdashh!EVT!_{\{\EVTPRESULT~\false,\EVTPEXPORT~\edeftypepos.\EVTPEXPORT\}} \evaltype
+ }{
+ \tyctx \vdashh!EDT!_\edeftypepos \edeftype
+ }
+\]
+
+\subsubsection{$\efunctype$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \tyctx \vdashh!EPL!_\edeftypepos \eparamlist\\
+ \tyctx \vdashh!ERL!_\edeftypepos \eresultlist\\
+ \end{array}
+ }{
+ \tyctx \vdashh!EDT!_\edeftypepos \eparamlist\to\eresultlist
+ }
+\]
+
+\subsubsection{$\exists \boundedtyvar^\ast. \einstancetype$}
+\[
+ \frac{
+ \forall j, \tyctx \oplus \TCVARS~\overline{(\boundedtyvar_i, )} \vdashh!EED!_\edeftypepos \eexterndecl_j
+ }{
+ \tyctx \vdashh!EDT!_\edeftypepos \exists \overline{\boundedtyvar_i}. \overline{\eexterndecl_j}
+ }
+\]
+
+\subsubsection{$\ecomponenttype$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \forall j, \tyctx \oplus \TCVARS~\overline{(\boundedtyvar_i, )} \vdashh!EED!_\edeftypepos \eexterndecl_j\\
+ \tyctx \oplus \TCVARS~\overline{(\boundedtyvar_i, )} \vdashh!EDT!_\edeftypepos \einstancetype
+ \end{array}
+ }{
+ \tyctx \vdashh!EDT!_\edeftypepos \forall \overline{\boundedtyvar_i}. \overline{\eexterndecl_j} \to \einstancetype
+ }
+\]
+
+\subsection{Core module types}
+\label{judgment:CMTtoECMT}
+\fbox{$\tyctx \vdashh!CMTtoECMT! \coremoduletype \leadstoh!CMTtoECMT! \ecoremoduletype$}
+
+\subsubsection{$\overline{\coremoduledecl_i}$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \tyctx_0 = \{ \TCPARENT~\tyctx \}\\
+ \forall i, \tyctx_{i-1} \vdashh!CMDtoECMT! \coremoduledecl_i
+ \leadstoh!CMDtoECMT! {\ecoremoduletype}_i \dashvh!CMDtoECMT! \tyctx_i
+ \end{array}
+ }{
+ \tyctx \vdashh!CMTtoECMT! \overline{\coremoduledecl_i}
+ \leadstoh!CMTtoECMT! \bigoplus_i {\ecoremoduletype}_i
+ }
+\]
+
+\subsection{Core module declarators}
+\label{judgment:CMDtoECMT}
+\fbox{$\tyctx \vdashh!CMDtoECMT! \coremoduledecl \leadstoh!CMDtoECMT! \ecoremoduletype \dashvh!CMDtoECMT! \tyctx'$}
+
+Each core module declarator elaborates to a (partial)
+$\ecoremoduletype$ and an updated context, reflecting the effect
+of the declarator on the component's index spaces.
+
+\subsubsection{$\coreimportdecl$}
+\[
+ \frac{
+ }{
+ \tyctx \vdashh!CMDtoECMT! \coreimportdecl \leadstoh!CMDtoECMT! \coreimportdecl \to \varnothing \dashvh!CMDtoECMT! \tyctx
+ }
+\]
+
+\subsubsection{$\coredeftype$}
+\[
+ \frac{
+ \tyctx \vdashh!CDTtoECDT! \coredeftype \leadstoh!CDTtoECDT! \ecoredeftype
+ }{
+ \tyctx \vdashh!CMDtoECMT! \coredeftype \leadstoh!CMDtoECMT!
+ \varnothing \to \varnothing \dashvh!CMDtoECMT! \tyctx \oplus \{ \TCCORE.\CTCTYPES~\ecoredeftype \}
+ }
+\]
+
+\subsubsection{$\corealias$}
+\[
+ \frac{
+ \begin{array}{@{}c@{}}
+ \corealias.\CASORT = \CSTYPE\\
+ \corealias.\CATARGET = \CATOUTER~\u32_o~\u32_i\\
+ \end{array}
+ }{
+ \tyctx \vdashh!CMDtoECMT! \alias \leadstoh!CMDtoECMT!
+ \varnothing \to \varnothing \dashvh!CMDtoECMT! \tyctx \oplus \{ \TCCORE.\CTCTYPES~\tyctx.\TCPARENT[\u32_o].\TCCORE.\CTCTYPES[\u32_i] \}
+ }
+\]
+
+\subsubsection{$\coreexportdecl$}
+\[
+ \frac{
+ }{
+ \tyctx \vdashh!CMDtoECMT! \coreexportdecl \leadstoh!CMDtoECMT! \varnothing \to \coreexportdecl \dashvh!CMDtoECMT! \tyctx
+ }
+\]
+
+\subsection{Core definition types}
+\label{judgment:CDTtoECDT}
+\fbox{$\tyctx \vdashh!CDTtoECDT! \coredeftype \leadstoh!CDTtoECDT! \ecoredeftype$}
+
+A core definition type elaborates to a $\ecoredeftype$.
+
+\subsubsection{$\core:functype$}
+\[
+ \frac{
+ }{
+ \tyctx \vdashh!CDTtoECDT! \core:functype \leadstoh!CDTtoECDT! \core:functype
+ }
+\]
+
+\subsubsection{$\coremoduletype$}
+\[
+ \frac{
+ \tyctx \vdashh!CMTtoECMT! \coremoduletype \leadstoh!CMTtoECMT! \ecoremoduletype
+ }{
+ \tyctx \vdashh!CDTtoECDT! \coremoduletype \leadstoh!CDTtoECDT! \ecoremoduletype
+ }
+\]
diff --git a/spec/document/valid/types.tex b/spec/document/valid/types.tex
new file mode 100644
index 00000000..621a193a
--- /dev/null
+++ b/spec/document/valid/types.tex
@@ -0,0 +1,266 @@
+\section{Elaborated Types}
+
+During validation, the abstract syntax types described above are
+\emph{elaborated} into types of a different structure, which are
+easier to work with. Elaborated types are different from the original
+abstract syntax types in three major aspects:
+
+* They do not contain any indirections through type index spaces:
+ since recursive types are explicitly not permitted by the component
+ model, it is possible to simply inline all such indirections.
+
+* Due to the above, instance and component types do not contain any
+ embedded declarations; the type sharing that necesstated the use of
+ type alias declarations is replaced with explicit binders and type
+ variables.
+
+ * Value types have been \emph{despecialised}: the value type
+ constructors $\VTTUPLE$, $\VTFLAGS$, $\VTENUM$, $\VTOPTION$,
+ $\VTUNION$, $\VTRESULT$, and $\VTSTRING$ have been replaced by
+ equivalent types.
+
+This elaboration also ensures that the type definitions themselves
+have valid structures, and so may be considered as validation on
+types.
+
+\subsection{Primitive Value Types}
+
+Any $\primvaltype$, $\defvaltype$, or $\valtype$ elaborates to a a
+$\evaltype$ with the following syntax:
+
+\begin{sum-production}{evaltype}
+ \EVTBOOL \alt
+ \EVTS8 | \EVTU8 | \EVTS16 | \EVTU16 | \EVTS32 | \EVTU32 | \EVTS64 | \EVTU64 \alt
+ \EVTFLOAT32 | \EVTFLOAT64 \alt
+ \EVTCHAR \alt
+ \EVTLIST~\evaltype \alt
+ \EVTRECORD~\erecordfield^{+} \alt
+ \EVTVARIANT~\evariantcase^{+} \alt
+ \EVTOWN~\edeftype \alt
+ \EVTREF~\refscope~\edeftype
+\end{sum-production}
+
+Because values are used linearly, values in the context must be
+associated with information about whether they are alive or dead. This
+is accomplished by assigning them types from $\evaltypead$:
+
+\begin{sum-production}{evaltypead}
+ \evaltype \alt
+ \evaltype^\dagger
+\end{sum-production}
+
+\subsection{Record Fields}
+
+Any $\recordfield$ elaborates to a $\erecordfield$ with the following
+abstract syntax:
+
+\begin{record-production}{erecordfield}
+ \{ \ERFNAME~\name, \ERFTYPE~\evaltype \}
+\end{record-production}
+
+\subsection{Variant Cases}
+
+Any $\variantcase$ elaborates to a $\evariantcase$ with the following
+abstract syntax:
+
+\begin{record-production}{evariantcase}
+ \{ \EVCNAME~\name, \EVCTYPE~\evaltype^?, \EVCREFINES~\u32^? \}
+\end{record-production}
+
+\subsection{Resource Types}
+
+Resource type definitions record the Core representation (which is
+presently fixed as $\i32$) and the destructor for a resource type:
+
+\begin{record-production}{eresourcetype}
+ \{ \ERTREP~\i32, \ERTDTOR~\funcidx \}
+\end{record-production}
+
+\subsection{Parameter Lists}
+
+Any $\paramlist$ elaborates to a $\eparamlist$ with the following
+abstract syntax:
+
+\begin{record-production}{eparamlist}
+ \{ \EPLNAME~\name, \EPLTYPE~\evaltype \}^\ast
+\end{record-production}
+
+\subsection{Result Lists}
+
+Any $\resultlist$ elaborates to a $\eresultlist$ with the following
+abstract syntax:
+
+\begin{sum-production}{eresultlist}
+ \evaltype \alt
+ \{ \ERLNAME~\name, \ERLTYPE~\evaltype \}^\ast
+\end{sum-production}
+
+\subsection{Function types}
+
+Any $\functype$ elaborates to a $\efunctype$ with the following
+abstract syntax:
+
+\begin{record-production}{efunctype}
+ \eparamlist\to\eresultlist
+\end{record-production}
+
+\subsection{Type bound}
+
+Any type bound elaborates to a $\etypebound$ with the following
+abstract syntax:
+
+\begin{sum-production}{etypebound}
+ \ETBEQ~\edeftype \alt
+ \ETBSUBR
+\end{sum-production}
+
+\subsection{Instance Types}
+
+An elaborated instance type is nothing more than a list of its
+exports. An instance type does not contain existential quantifiers for
+its type exports, as they can always be hoisted to a containing
+component type.
+
+\begin{sum-productions}
+ \production{einstancetype} \eexterndecl^{*}
+ \production{eexterndecl} \{ \EEDNAME~\name, \EEDDESC~\eexterndesc \}
+ \production{eexterndesc}
+ \EEMDCOREMODULE~\ecoremoduletype \alt
+ \EEMDFUNC~\efunctype \alt
+ \EEMDVALUE~\evaltype \alt
+ \EEMDTYPE~\edeftype \alt
+ \EEMDINSTANCE~\einstancetype \alt
+ \EEMDCOMPONENT~\ecomponenttype
+\end{sum-productions}
+
+Because instance value exports must be used linearly in the context,
+instances in the contexts are, by analogy with $\evaltypead$, assigned
+types from $\einstancetypead$.
+
+\begin{sum-productions}
+ \production{einstancetypead} \eexterndeclad^{*}
+ \production{eexterndeclad}
+ \eexterndecl \alt
+ \eexterndecl^\dagger
+\end{sum-productions}
+
+\subsubsection{Notational conventions}
+
+\begin{itemize}
+\item We write $\einstancetype \oplus \einstancetype'$ to mean the
+ instance type formed by the concationation of the export
+ declarations of $\einstancetype$ and $\einstancetype'$.
+
+\item We write $\bigoplus_i {\einstancetype}_i$ to mean the instance
+ type formed by
+ ${\einstancetype}_1 \oplus \dots \oplus {\einstancetype}_n$.
+\end{itemize}
+
+\subsection{Component Types}
+
+In a similar manner to instance types above, component types change
+significantly upon elaboration: an elaborated component type is
+described as a mapping from a quantified list of imports to the
+existentially quantified type of the instance that it will produce
+upon instantiation:
+
+\begin{record-productions}
+ \production{ecomponenttype}
+ \forall \boundedtyvar^\ast. \eexterndecl^\ast \to
+ \exists \boundedtyvar^\ast. \einstancetype
+ \production{boundedtyvar} (\tyvar : \etypebound)
+\end{record-productions}
+
+\subsubsection{Notational conventions}
+
+\begin{itemize}
+\item Much like with instance types above, we write
+ $\ecomponenttype \oplus \ecomponenttype'$ to mean the combination of
+ two component types; in this case, the component type whose
+ \begin{itemize}
+ \item universally quantified type variables are the concatenation of
+ the universally quantified type variables of $\ecomponenttype$ and
+ $\ecomponenttype$; and whose
+
+ \item imports are the concatenation of the import lists of
+ $\ecomponenttype$ and $\ecomponenttype'$; and whose
+
+ \item existentially quantified type variables are the concatenation
+ of the existentially quantified type variables of
+ $\ecomponenttype$ and $\ecomponenttype'$; and whose
+
+ \item instantiation result (instance) type is the result of applying
+ $\oplus$ to the instantiation result (instance) types of
+ $\ecomponenttype$ and $\ecomponenttype'$.
+ \end{itemize}
+\end{itemize}
+
+\subsection{Defined Types}
+
+Any $\deftype$ elaborates to a $\edeftype$ with the
+following abstract syntax:
+
+\begin{sum-production}{edeftype}
+ \tyvar \alt
+ \EDTRESOURCE~\rtidx \alt
+ \evaltype \alt
+ \efunctype \alt
+ \ecomponenttype \alt
+ \exists \boundedtyvar^\ast. einstancetype\\
+\end{sum-production}
+
+\subsection{Core Instance Types}
+
+Although there are no core instance types present at the surface
+level, it is useful to define the abstract syntax of (elaborated) core
+instance types, as they will be needed to characterise the results of
+instantiationg core modules. As with a component instance type, an
+(elaborated) core instance type is nothing more than a list of its
+exports:
+
+\begin{record-production}{ecoreinstancetype}
+ \coreexportdecl^\ast
+\end{record-production}
+
+\subsubsection{Notational conventions}
+
+\begin{itemize}
+\item We write $\ecoreinstancetype \oplus \ecoreinstancetype'$ to mean
+ the instance type formed by the concatenation of the export
+ declarations of $\ecoreinstancetype$ and $\ecoreinstancetype'$.
+\end{itemize}
+
+
+\subsection{Core Module Types}
+
+Core module types are defined much like component types above: as a
+mapping from import descriptions to the type of the instance that will
+be produced upon instantiating the module:
+
+
+\begin{record-production}{ecoremoduletype}
+ \coreimportdecl^\ast \to \coreexportdecl^\ast
+\end{record-production}
+
+
+\subsubsection{Notational conventions}
+
+\begin{itemize}
+\item Much like with core instance types above, we write
+ $\ecoremoduletype \oplus \ecoremoduletype'$ to mean the combination
+ of two module types; in this case, the module type whose imports are
+ the concatenation of the import lists of $\ecoremoduletype$ and
+ $\ecoremoduletype'$ and whose instantiation result (instance) type
+ is the result of applying $\oplus$ to the instantiation result
+ (instance) types of $\ecoremoduletype$ and $\ecoremoduletype'$.
+\end{itemize}
+
+\subsection{Core Definition Types}
+
+Any core definition type elaborates to a $\ecoredeftype$ with
+the following abstract syntax:
+
+\begin{sum-production}{ecoredeftype}
+ \core:functype \alt
+ \ecoremoduletype
+\end{sum-production}