Add draft of the specification of validation

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

spec/document/.gitignore

@@ -0,0 +1,4 @@
+*.aux
+*.log
+*.out
+*.pdf

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

spec/document/shell.nix

@@ -0,0 +1,5 @@
+{ nixpkgs ? import <nixpkgs> {} }: with nixpkgs;
+stdenv.mkDerivation {
+  name = "wasm-components-spec";
+  buildInputs = [ texlive.combined.scheme-full ];
+}

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}