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 {} }: 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