Skip to content

Commit 2601394

Browse files
pl-semioticspl-semiotics
committed
Add draft of the specification of validation
1 parent 1ddf5d7 commit 2601394

13 files changed

+2438
-0
lines changed

‎LICENSE

+1
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ to that directory and its relative sub-directories.
44
The relevant directories and licenses are:
55

66
design/ - Apache License 2.0
7+
spec/document/ - W3C Software and Document Notice and License
78

89
(Other directories will be added when the [module-linking] repository merges.)
910

‎spec/document/.gitignore

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
*.aux
2+
*.log
3+
*.out
4+
*.pdf

‎spec/document/macros.tex

+286
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,286 @@
1+
\usepackage[hidelinks]{hyperref}
2+
\usepackage{amssymb}
3+
\usepackage{amsmath}
4+
5+
\def\K{\mathsf}
6+
\def\X{\mathit}
7+
\def\F{\mathrm}
8+
9+
\def\subtypeof{\preccurlyeq}
10+
\def\ESUBRESOURCE{\K{resource}}
11+
12+
% TODO: xref properly
13+
\def\name{\X{name}}
14+
\def\tyvar{\alpha}
15+
\def\tyvarb{\beta}
16+
\def\rtidx{\X{rtidx}}
17+
\def\bool{\X{bool}}
18+
\def\true{\K{true}}
19+
\def\false{\K{false}}
20+
21+
\catcode`:=11
22+
\def\core:type{\X{core{:}type}}
23+
\def\core:typeidx{\X{core{:}typeidx}}
24+
\def\core:funcidx{\X{core{:}funcidx}}
25+
\def\core:memidx{\X{core{:}memidx}}
26+
\def\core:functype{\X{core{:}functype}}
27+
\def\core:tabletype{\X{core{:}tabletype}}
28+
\def\core:memtype{\X{core{:}memtype}}
29+
\def\core:globaltype{\X{core{:}globaltype}}
30+
\def\core:import{\X{core{:}import}}
31+
\def\core:importdesc{\X{core{:}importdesc}}
32+
\def\core:module{\X{core{:}module}}
33+
\def\core:IMODULE{\K{module}}
34+
\def\core:ENAME{\K{name}}
35+
\def\core:INAME{\K{name}}
36+
\def\core:EDESC{\K{desc}}
37+
\def\core:IDESC{\K{desc}}
38+
39+
\makeatletter
40+
41+
\protected\def\u{\afterassignment\@u\count255=}
42+
\def\@u{\K{u\the\count255}}
43+
\protected\def\i{\afterassignment\@i\count255=}
44+
\def\@i{\K{i\the\count255}}
45+
46+
\def\setupPCR{\def\production@cr{\global\let\production@cr=\\}}
47+
\def\setupSP{%
48+
\def\alt{\\&&\mathchar"26A&}%
49+
\mathcode`|="8000%
50+
\setupPCR%
51+
}
52+
\catcode`|=13
53+
\def|{~\mathchar"26A~}
54+
\catcode`|=12
55+
\newenvironment{sum-productions}
56+
{\[\setupSP\begin{array}{llcl}}
57+
{\end{array}\]}
58+
\newenvironment{sum-production}[1]
59+
{\begin{sum-productions}\production{#1}}
60+
{\end{sum-productions}}
61+
\def\production#1{\production@cr&\hypertarget{syntax:#1}{\csname#1\endcsname}&::=&}
62+
\newenvironment{record-productions}
63+
{\[\setupPCR\begin{array}{llll}}
64+
{\end{array}\]}
65+
\newenvironment{record-production}[1]
66+
{\begin{record-productions}\production{#1}}
67+
{\end{record-productions}}
68+
69+
\def\defgrammar@#1#2#3{%
70+
\def\currentprefix{#1}%
71+
\def\currentgrammar{#2}%
72+
\expandafter\def\csname#2\endcsname{{\protect\hyperlink{syntax:#2}{#3}}}%
73+
}
74+
\def\defgrammar#1#2{\defgrammar@{#1}{#2}{\X{#2}}}
75+
\def\defconstr@#1#2{%
76+
\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}}}%
77+
}
78+
\def\defconstr#1{\defconstr@{#1}{\K{#1}}}
79+
80+
\def\defconstrs#1{\@defconstrs#1,,\relax}
81+
\def\@defconstrs#1,#2\relax{\defconstr{#1}\if#2,\expandafter\@firstoftwo\else\expandafter\@secondoftwo\fi{}{\@defconstrs#2\relax}}
82+
\def\defsyntax#1#2#3{\defgrammar{#1}{#2}\defconstrs{#3}}
83+
84+
%%% Surface Type Syntax
85+
86+
\defgrammar{VT}{primvaltype}
87+
\defconstr{bool}
88+
\protected\def\VTS{\afterassignment\@VTS\count255=}
89+
\def\@VTS{\hyperlink{syntax:primvaltype}{\K{s\the\count255}}}
90+
\protected\def\VTU{\afterassignment\@VTU\count255=}
91+
\def\@VTU{\hyperlink{syntax:primvaltype}{\K{u\the\count255}}}
92+
\protected\def\VTFLOAT{\afterassignment\@VTFLOAT\count255=}
93+
\def\@VTFLOAT{\hyperlink{syntax:primvaltype}{\K{float\the\count255}}}
94+
\defconstr{char}
95+
\defconstr{string}
96+
97+
\defgrammar{VT}{defvaltype}
98+
\defconstr{prim}
99+
\defconstr{record}
100+
\defconstr{variant}
101+
\defconstr{list}
102+
\defconstr{tuple}
103+
\defconstr{flags}
104+
\defconstr{enum}
105+
\defconstr{union}
106+
\defconstr{option}
107+
\defconstr{result}
108+
\defconstr{own}
109+
\defconstr{borrow}
110+
111+
\defgrammar{VT}{valtype}
112+
113+
\defgrammar{RF}{recordfield}
114+
\defconstr{name}
115+
\defconstr{type}
116+
117+
\defgrammar{VC}{variantcase}
118+
\defconstr{name}
119+
\defconstr{type}
120+
\defconstr{refines}
121+
122+
\defgrammar{RT}{resourcetype}
123+
\tracingmacros1
124+
\defconstrs{rep,dtor}
125+
126+
\defsyntax{FT}{functype}{params,results}
127+
\defsyntax{PL}{paramlist}{type,name}
128+
\defsyntax{RL}{resultlist}{type,name}
129+
130+
\defsyntax{IT}{instancetype}{}
131+
\defsyntax{ID}{instancedecl}{alias,type,export}
132+
\defsyntax{ED}{externdesc}{type,func,value,instance,component}
133+
\defconstr@{coremodule}{\K{core\_module}}
134+
\defsyntax{TB}{typebound}{eq,subr}
135+
\defsyntax{ED}{exportdecl}{name,desc}
136+
137+
\defsyntax{}{componenttype}{}
138+
\defsyntax{CD}{componentdecl}{import}
139+
\defsyntax{ID}{importdecl}{name,desc}
140+
141+
\defsyntax{}{deftype}{}
142+
143+
\defgrammar@{}{coredeftype}{\X{core{:}deftype}}
144+
\defgrammar@{}{coremoduletype}{\X{core{:}moduletype}}
145+
\defgrammar@{}{coremoduledecl}{\X{core{:}moduledecl}}
146+
\defgrammar@{}{coreimportdecl}{\X{core{:}importdecl}}
147+
\defgrammar@{CA}{corealias}{\X{core{:}alias}}
148+
\defconstrs{sort,target}
149+
\defgrammar@{CAT}{corealiastarget}{\X{core{:}aliastarget}}
150+
\defconstrs{outer}
151+
\defgrammar@{CED}{coreexportdecl}{\X{core{:}exportdecl}}
152+
\defconstrs{name,desc}
153+
154+
%%% Surface Expression Syntax
155+
156+
\defsyntax{S}{sort}{core,func,value,type,component,instance}
157+
\defgrammar@{CS}{coresort}{\X{core{:}sort}}
158+
\defconstrs{instance,module,type,global,memory,table,func}
159+
160+
\defgrammar@{}{coremoduleidx}{\X{core{:}moduleidx}}
161+
\defgrammar@{}{coreinstanceidx}{\X{core{:}instanceidx}}
162+
\defgrammar{}{componentidx}
163+
\defgrammar{}{instanceidx}
164+
\defgrammar{}{funcidx}
165+
\defgrammar@{}{corefuncidx}{\X{core{:}funcidx}}
166+
\defgrammar{}{valueidx}
167+
\defgrammar{}{typeidx}
168+
\defgrammar@{}{coretypeidx}{\X{core{:}typeidx}}
169+
170+
\defgrammar@{CSI}{coresortidx}{\X{core{:}sortidx}}
171+
\defconstrs{sort,idx}
172+
\defsyntax{SI}{sortidx}{sort,idx}
173+
174+
\defsyntax{D}{definition}{component,instance,alias,type,canon,start,import,export}
175+
\defconstr@{coremodule}{\K{core\_module}}
176+
\defconstr@{coreinstance}{\K{core\_instance}}
177+
\defconstr@{coretype}{\K{core\_type}}
178+
179+
\defgrammar@{CI}{coreinstance}{\X{core{:}instance}}
180+
\defconstrs{instantiate,exports}
181+
\defgrammar@{CIA}{coreinstantiatearg}{\X{core{:}instantiatearg}}
182+
\defconstrs{instance,name}
183+
\defgrammar@{CE}{coreexport}{\X{core{:}export}}
184+
\defconstrs{def,name}
185+
186+
\defsyntax{}{component}{}
187+
188+
\defsyntax{I}{instance}{instantiate,exports}
189+
\defsyntax{IA}{instantiatearg}{name,arg}
190+
191+
\defsyntax{A}{alias}{sort,target}
192+
\defsyntax{AT}{aliastarget}{export,outer}
193+
\defconstr@{coreexport}{\K{core\_export}}
194+
195+
\defsyntax{C}{canon}{lift,lower}
196+
\defconstr@{resourcenew}{\K{resource.new}}
197+
\defconstr@{resourcedrop}{\K{resource.drop}}
198+
\defconstr@{resourcerep}{\K{resource.rep}}
199+
\defsyntax{CO}{canonopt}{memory,realloc,postreturn}
200+
\defconstr@{stringencodingUTFEIGHT}{\K{string\_encoding\_utf8}}
201+
\defconstr@{stringencodingUTFSIXTEEN}{\K{string\_encoding\_utf16}}
202+
\defconstr@{stringencodingLATINONEUTFSIXTEEN}{\K{string\_encoding\_latin1{+}utf16}}
203+
204+
\defsyntax{F}{start}{func,args}
205+
206+
\defsyntax{}{import}{}
207+
208+
\defsyntax{E}{export}{name,def,desc}
209+
210+
%%% Elaborated Type Syntax
211+
\def\defesyntax#1#2#3{\defgrammar@{E#1}{e#2}{\X{#2}_e}\defconstrs{#3}}
212+
213+
\def\maybedead{{\rlap{$\mathsurround=0pt\dagger$}?}}
214+
215+
\defesyntax{VT}{valtype}{bool,char,list,record,variant,own,ref}
216+
\protected\def\EVTS{\afterassignment\@EVTS\count255=}
217+
\def\@EVTS{\hyperlink{syntax:evaltype}{\K{s\the\count255}}}
218+
\protected\def\EVTU{\afterassignment\@EVTU\count255=}
219+
\def\@EVTU{\hyperlink{syntax:evaltype}{\K{u\the\count255}}}
220+
\protected\def\EVTFLOAT{\afterassignment\@EVTFLOAT\count255=}
221+
\def\@EVTFLOAT{\hyperlink{syntax:evaltype}{\K{float\the\count255}}}
222+
\defsyntax{RS}{refscope}{call}
223+
\defgrammar@{}{evaltypead}{{\X{valtype}_e^\maybedead}}
224+
225+
\defesyntax{RF}{recordfield}{name,type}
226+
\defesyntax{VC}{variantcase}{name,type,refines}
227+
228+
\defesyntax{RT}{resourcetype}{rep,dtor}
229+
230+
\defesyntax{PL}{paramlist}{name,type}
231+
\defesyntax{RL}{resultlist}{name,type}
232+
233+
\defesyntax{}{functype}{}
234+
\defesyntax{TB}{typebound}{eq,subr}
235+
236+
\defesyntax{}{instancetype}{}
237+
\defsyntax{}{boundedtyvar}{}
238+
\defesyntax{ED}{externdecl}{name,desc}
239+
\defesyntax{EMD}{externdesc}{func,value,type,instance,component}
240+
\defconstr@{coremodule}{\K{core\_module}}
241+
\defgrammar@{}{einstancetypead}{{\X{instancetype}_e^\maybedead}}
242+
\defgrammar@{}{eexterndeclad}{{\X{externdecl}_e^\maybedead}}
243+
244+
\defesyntax{}{componenttype}{}
245+
246+
\defesyntax{DT}{deftype}{resource}
247+
248+
\defgrammar@{}{ecoreinstancetype}{\X{core{:}instancetype}_e}
249+
\defgrammar@{}{ecoremoduletype}{\X{core{:}moduletype}_e}
250+
\defgrammar@{}{ecoredeftype}{\X{core{:}deftype}_e}
251+
252+
%%% Contexts
253+
254+
\defgrammar@{CTC}{coretyctx}{\Gamma_c}
255+
\defconstrs{types,funcs,tables,mems,globals,modules,instances}
256+
\defgrammar@{TC}{tyctx}{\Gamma}
257+
\defconstrs{parent,core,vars,rtypes,types,components,instances,funcs,values}
258+
\defconstr@{ob}{\K{outer\_boundary}}
259+
\defconstr@{ld}{\K{locally\_defined}}
260+
261+
\defsyntax{VCC}{vcctx}{ctx,cases}
262+
\defgrammar@{EVTP}{evaltypepos}{{\pi_v}}
263+
\defconstrs{result,export}
264+
\defgrammar@{EDTP}{edeftypepos}{{\pi_d}}
265+
\defconstr@{export}{extern}
266+
267+
%%% Judgments
268+
269+
270+
\def\vdashh!#1!{\mathrel{\hyperref[judgment:#1]{\vdash}}}
271+
\def\leadstoh!#1!{\mathrel{\hyperref[judgment:#1]{\leadsto}}}
272+
\def\dashvh!#1!{\mathrel{\hyperref[judgment:#1]{\dashv}}}
273+
\def\trelh!#1!{\mathrel{\hyperref[judgment:#1]{:}}}
274+
275+
\def\freeVars#1{\mathop{\F{fv}}(#1)}
276+
\def\subst{\gamma}
277+
\def\resolveVars#1{\mathop{\F{resolve\_vars}}(#1)}
278+
\def\length#1{\lVert#1\rVert}
279+
280+
\def\novalues#1{{}\mathrel{\hyperref[judgment:novalues]{\vdash^\mathsf{\mkern-20mu\neg v}}}{#1}}
281+
282+
%\def\EEDtoCtx#1#2#3#4{{#1} \mathrel{\hyperref[judgment:EEDtoCtx]{\oplus}} {#2} \mathrel{\hyperref[judgment:EEDtoCtx]{=}} {#4} \mathrel{\hyperref[judgment:EEDtoCtx]{@}} {#3}}
283+
%\def\callEITvars#1{\mathop{\hyperref[judgment:EITvars]{\F{unvar\_instance}}}({#1})}
284+
%\def\EITvars#1#2#3{\callEITvars{#1} = \exists {#2}. {#3}}
285+
286+
\makeatother

‎spec/document/shell.nix

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

‎spec/document/spec.tex

+21
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
\documentclass{report}
2+
3+
\input{macros}
4+
5+
\begin{document}
6+
7+
\chapter{Introduction}
8+
9+
\chapter{Structure}
10+
\include{syntax/conventions}
11+
\include{syntax/types}
12+
\include{syntax/components}
13+
14+
\chapter{Validation}
15+
\include{valid/conventions}
16+
\include{valid/types}
17+
\include{valid/contexts}
18+
\include{valid/elaboration}
19+
\include{valid/components}
20+
21+
\end{document}

0 commit comments

Comments
 (0)