diff --git a/document/core/util/macros.def b/document/core/util/macros.def
new file mode 100644
index 0000000..0436dfd
--- /dev/null
+++ b/document/core/util/macros.def
@@ -0,0 +1,1272 @@
+.. LINK MACROS
+
+.. External Standards
+.. ------------------
+
+.. |WasmDraft| replace:: |pagelink|
+.. _WasmDraft: |pagelink|
+
+.. |WasmIssues| replace:: |issuelink|
+.. _WasmIssues: |issuelink|
+
+.. |IEEE754| replace:: IEEE 754
+.. _IEEE754: https://ieeexplore.ieee.org/document/8766229
+
+.. |Unicode| replace:: Unicode
+.. _Unicode: https://www.unicode.org/versions/latest/
+
+.. |ASCII| replace:: ASCII
+.. _ASCII: https://webstore.ansi.org/RecordDetail.aspx?sku=INCITS+4-1986%5bR2012%5d
+
+
+.. External Definitions
+.. --------------------
+
+.. |LittleEndian| replace:: little endian
+.. _LittleEndian: https://en.wikipedia.org/wiki/Endianness#Little-endian
+
+.. |LEB128| replace:: LEB128
+.. _LEB128: https://en.wikipedia.org/wiki/LEB128
+.. |UnsignedLEB128| replace:: unsigned LEB128
+.. _UnsignedLEB128: https://en.wikipedia.org/wiki/LEB128#Unsigned_LEB128
+.. |SignedLEB128| replace:: signed LEB128
+.. _SignedLEB128: https://en.wikipedia.org/wiki/LEB128#Signed_LEB128
+
+.. |SExpressions| replace:: S-expressions
+.. _SExpressions: https://en.wikipedia.org/wiki/S-expression
+
+.. |MediaType| replace:: Media Type
+.. _MediaType: https://www.iana.org/assignments/media-types/media-types.xhtml
+
+
+.. Literature
+.. ----------
+
+.. |PLDI2017| replace:: Bringing the Web up to Speed with WebAssembly
+.. _PLDI2017: https://dl.acm.org/citation.cfm?doid=3062341.3062363
+
+.. |CPP2018| replace:: Mechanising and Verifying the WebAssembly Specification
+.. _CPP2018: https://dl.acm.org/citation.cfm?id=3167082
+
+.. |FM2021| replace:: Two Mechanisations of WebAssembly 1.0
+.. _FM2021: https://link.springer.com/chapter/10.1007/978-3-030-90870-6_4
+
+.. |TAPL| replace:: Types and Programming Languages
+.. _TAPL: https://www.cis.upenn.edu/~bcpierce/tapl/
+
+
+
+.. MATH MACROS
+
+
+.. Generic Stuff
+.. -------------
+
+.. To comment out stuff
+
+.. |void#1| mathdef:: {}
+
+
+.. Type-setting of names
+.. X - (multi-letter) variables / non-terminals
+.. F - functions
+.. K - keywords / terminals
+.. B - binary grammar non-terminals
+.. T - textual grammar non-terminals
+
+.. |X| mathdef:: \mathit
+.. |F| mathdef:: \mathrm
+.. |K| mathdef:: \mathsf
+.. |B| mathdef:: \mathtt
+.. |T| mathdef:: \mathtt
+
+
+.. Notation
+
+.. |mod| mathdef:: \mathbin{\F{mod}}
+
+.. |iff| mathdef:: \mathrel{\mbox{if}}
+.. |otherwise| mathdef:: \mathrel{\mbox{otherwise}}
+.. |where| mathdef:: \mathrel{\mbox{where}}
+
+
+
+.. Grammar & Syntax Notation
+.. -------------------------
+
+.. Notation for grammars
+
+.. |production| mathdef:: \void
+
+
+.. Notation for Sequences & Records
+
+.. |slice| mathdef:: \xref{syntax/conventions}{notation-slice}{\mathrel{\mathbf{:}}}
+.. |with| mathdef:: \xref{syntax/conventions}{notation-replace}{\mathrel{\mbox{with}}}
+.. |concat| mathdef:: \xref{syntax/conventions}{notation-concat}{\F{concat}}
+.. |compose| mathdef:: \xref{syntax/conventions}{notation-compose}{\oplus}
+.. |bigcompose| mathdef:: \xref{syntax/conventions}{notation-compose}{\bigoplus}
+
+
+
+.. Abstract Syntax
+.. ---------------
+
+.. Auxiliary productions
+
+.. |vec| mathdef:: \xref{syntax/conventions}{syntax-vec}{\X{vec}}
+
+
+.. Values, terminals
+
+.. |hex#1| mathdef:: \mathtt{0x#1}
+.. |unicode#1| mathdef:: \mathrm{U{+}#1}
+
+.. |NAN| mathdef:: \xref{syntax/values}{syntax-float}{\K{nan}}
+
+
+.. Values, non-terminals
+
+.. |byte| mathdef:: \xref{syntax/values}{syntax-byte}{\X{byte}}
+
+.. |uX#1| mathdef:: {\X{u#1}}
+.. |sX#1| mathdef:: {\X{s#1}}
+.. |iX#1| mathdef:: {\X{i#1}}
+.. |fX#1| mathdef:: {\X{f#1}}
+.. |vX#1| mathdef:: {\X{v#1}}
+
+.. |uN| mathdef:: \xref{syntax/values}{syntax-int}{\X{u}N}
+.. |uM| mathdef:: \xref{syntax/values}{syntax-int}{\X{u}M}
+.. |u1| mathdef:: \xref{syntax/values}{syntax-int}{\X{u1}}
+.. |u8| mathdef:: \xref{syntax/values}{syntax-int}{\X{u8}}
+.. |u16| mathdef:: \xref{syntax/values}{syntax-int}{\X{u16}}
+.. |u32| mathdef:: \xref{syntax/values}{syntax-int}{\X{u32}}
+.. |u64| mathdef:: \xref{syntax/values}{syntax-int}{\X{u64}}
+
+.. |sN| mathdef:: \xref{syntax/values}{syntax-int}{\X{s}N}
+.. |s8| mathdef:: \xref{syntax/values}{syntax-int}{\X{s8}}
+.. |s16| mathdef:: \xref{syntax/values}{syntax-int}{\X{s16}}
+.. |s32| mathdef:: \xref{syntax/values}{syntax-int}{\X{s32}}
+.. |s64| mathdef:: \xref{syntax/values}{syntax-int}{\X{s64}}
+
+.. |iM| mathdef:: \xref{syntax/values}{syntax-int}{\X{i}M}
+.. |iN| mathdef:: \xref{syntax/values}{syntax-int}{\X{i}N}
+.. |i8| mathdef:: \xref{syntax/values}{syntax-int}{\X{i8}}
+.. |i16| mathdef:: \xref{syntax/values}{syntax-int}{\X{i16}}
+.. |i32| mathdef:: \xref{syntax/values}{syntax-int}{\X{i32}}
+.. |i64| mathdef:: \xref{syntax/values}{syntax-int}{\X{i64}}
+.. |i128| mathdef:: \xref{syntax/values}{syntax-int}{\X{i128}}
+
+.. |fN| mathdef:: \xref{syntax/values}{syntax-float}{\X{f}N}
+.. |fNmag| mathdef:: \xref{syntax/values}{syntax-float}{\X{f}\X{Nmag}}
+.. |f32| mathdef:: \xref{syntax/values}{syntax-float}{\X{f32}}
+.. |f64| mathdef:: \xref{syntax/values}{syntax-float}{\X{f64}}
+
+.. |name| mathdef:: \xref{syntax/values}{syntax-name}{\X{name}}
+.. |char| mathdef:: \xref{syntax/values}{syntax-name}{\X{char}}
+
+
+.. Values, meta functions
+
+.. |canon| mathdef:: \xref{syntax/values}{aux-canon}{\F{canon}}
+.. |significand| mathdef:: \xref{syntax/values}{aux-significand}{\F{signif}}
+.. |exponent| mathdef:: \xref{syntax/values}{aux-exponent}{\F{expon}}
+
+
+.. Types, terminals
+
+.. |to| mathdef:: \xref{syntax/types}{syntax-functype}{\rightarrow}
+
+.. |I32| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{i32}}
+.. |I64| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{i64}}
+.. |F32| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{f32}}
+.. |F64| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{f64}}
+.. |V128| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{v128}}
+.. |IN| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{i}N}
+.. |FN| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{f}N}
+.. |VN| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{v}N}
+.. |I8X16| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{i8x16}}
+.. |I16X8| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{i16x8}}
+.. |I32X4| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{i32x4}}
+.. |I64X2| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{i64x2}}
+.. |F32X4| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{f32x4}}
+.. |F64X2| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{f64x2}}
+
+.. |FUNCREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{funcref}}
+.. |EXTERNREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{externref}}
+
+.. |MVAR| mathdef:: \xref{syntax/types}{syntax-mut}{\K{var}}
+.. |MCONST| mathdef:: \xref{syntax/types}{syntax-mut}{\K{const}}
+
+.. |LMIN| mathdef:: \xref{syntax/types}{syntax-limits}{\K{min}}
+.. |LMAX| mathdef:: \xref{syntax/types}{syntax-limits}{\K{max}}
+
+.. |ETFUNC| mathdef:: \xref{syntax/types}{syntax-externtype}{\K{func}}
+.. |ETTABLE| mathdef:: \xref{syntax/types}{syntax-externtype}{\K{table}}
+.. |ETMEM| mathdef:: \xref{syntax/types}{syntax-externtype}{\K{mem}}
+.. |ETGLOBAL| mathdef:: \xref{syntax/types}{syntax-externtype}{\K{global}}
+
+
+.. Types, non-terminals
+
+.. |numtype| mathdef:: \xref{syntax/types}{syntax-numtype}{\X{numtype}}
+.. |vectype| mathdef:: \xref{syntax/types}{syntax-vectype}{\X{vectype}}
+.. |reftype| mathdef:: \xref{syntax/types}{syntax-reftype}{\X{reftype}}
+.. |valtype| mathdef:: \xref{syntax/types}{syntax-valtype}{\X{valtype}}
+.. |resulttype| mathdef:: \xref{syntax/types}{syntax-resulttype}{\X{resulttype}}
+.. |functype| mathdef:: \xref{syntax/types}{syntax-functype}{\X{functype}}
+
+.. |globaltype| mathdef:: \xref{syntax/types}{syntax-globaltype}{\X{globaltype}}
+.. |tabletype| mathdef:: \xref{syntax/types}{syntax-tabletype}{\X{tabletype}}
+.. |memtype| mathdef:: \xref{syntax/types}{syntax-memtype}{\X{memtype}}
+
+.. |limits| mathdef:: \xref{syntax/types}{syntax-limits}{\X{limits}}
+.. |mut| mathdef:: \xref{syntax/types}{syntax-mut}{\X{mut}}
+
+.. |externtype| mathdef:: \xref{syntax/types}{syntax-externtype}{\X{externtype}}
+
+.. |stacktype| mathdef:: \xref{valid/instructions}{syntax-stacktype}{\X{stacktype}}
+.. |opdtype| mathdef:: \xref{valid/instructions}{syntax-opdtype}{\X{opdtype}}
+
+
+.. Types, meta functions
+
+.. |etfuncs| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{funcs}}
+.. |ettables| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{tables}}
+.. |etmems| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{mems}}
+.. |etglobals| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{globals}}
+
+
+.. Indices, non-terminals
+
+.. |typeidx| mathdef:: \xref{syntax/modules}{syntax-typeidx}{\X{typeidx}}
+.. |funcidx| mathdef:: \xref{syntax/modules}{syntax-funcidx}{\X{funcidx}}
+.. |tableidx| mathdef:: \xref{syntax/modules}{syntax-tableidx}{\X{tableidx}}
+.. |memidx| mathdef:: \xref{syntax/modules}{syntax-memidx}{\X{memidx}}
+.. |globalidx| mathdef:: \xref{syntax/modules}{syntax-globalidx}{\X{globalidx}}
+.. |elemidx| mathdef:: \xref{syntax/modules}{syntax-elemidx}{\X{elemidx}}
+.. |dataidx| mathdef:: \xref{syntax/modules}{syntax-dataidx}{\X{dataidx}}
+.. |localidx| mathdef:: \xref{syntax/modules}{syntax-localidx}{\X{localidx}}
+.. |labelidx| mathdef:: \xref{syntax/modules}{syntax-labelidx}{\X{labelidx}}
+
+
+.. Indices, meta functions
+
+.. |freetypeidx| mathdef:: \xref{syntax/modules}{syntax-typeidx}{\F{typeidx}}
+.. |freefuncidx| mathdef:: \xref{syntax/modules}{syntax-funcidx}{\F{funcidx}}
+.. |freetableidx| mathdef:: \xref{syntax/modules}{syntax-tableidx}{\F{tableidx}}
+.. |freememidx| mathdef:: \xref{syntax/modules}{syntax-memidx}{\F{memidx}}
+.. |freeglobalidx| mathdef:: \xref{syntax/modules}{syntax-globalidx}{\F{globalidx}}
+.. |freeelemidx| mathdef:: \xref{syntax/modules}{syntax-elemidx}{\F{elemidx}}
+.. |freedataidx| mathdef:: \xref{syntax/modules}{syntax-dataidx}{\F{dataidx}}
+.. |freelocalidx| mathdef:: \xref{syntax/modules}{syntax-localidx}{\F{localidx}}
+.. |freelabelidx| mathdef:: \xref{syntax/modules}{syntax-labelidx}{\F{labelidx}}
+
+
+.. Modules, terminals
+
+.. |MTYPES| mathdef:: \xref{syntax/modules}{syntax-module}{\K{types}}
+.. |MFUNCS| mathdef:: \xref{syntax/modules}{syntax-module}{\K{funcs}}
+.. |MTABLES| mathdef:: \xref{syntax/modules}{syntax-module}{\K{tables}}
+.. |MMEMS| mathdef:: \xref{syntax/modules}{syntax-module}{\K{mems}}
+.. |MGLOBALS| mathdef:: \xref{syntax/modules}{syntax-module}{\K{globals}}
+.. |MIMPORTS| mathdef:: \xref{syntax/modules}{syntax-module}{\K{imports}}
+.. |MEXPORTS| mathdef:: \xref{syntax/modules}{syntax-module}{\K{exports}}
+.. |MDATAS| mathdef:: \xref{syntax/modules}{syntax-module}{\K{datas}}
+.. |MELEMS| mathdef:: \xref{syntax/modules}{syntax-module}{\K{elems}}
+.. |MSTART| mathdef:: \xref{syntax/modules}{syntax-module}{\K{start}}
+
+.. |FTYPE| mathdef:: \xref{syntax/modules}{syntax-func}{\K{type}}
+.. |FLOCALS| mathdef:: \xref{syntax/modules}{syntax-func}{\K{locals}}
+.. |FBODY| mathdef:: \xref{syntax/modules}{syntax-func}{\K{body}}
+
+.. |TTYPE| mathdef:: \xref{syntax/modules}{syntax-table}{\K{type}}
+
+.. |MTYPE| mathdef:: \xref{syntax/modules}{syntax-mem}{\K{type}}
+
+.. |GTYPE| mathdef:: \xref{syntax/modules}{syntax-global}{\K{type}}
+.. |GINIT| mathdef:: \xref{syntax/modules}{syntax-global}{\K{init}}
+
+.. |ETYPE| mathdef:: \xref{syntax/modules}{syntax-elem}{\K{type}}
+.. |EINIT| mathdef:: \xref{syntax/modules}{syntax-elem}{\K{init}}
+.. |EMODE| mathdef:: \xref{syntax/modules}{syntax-elem}{\K{mode}}
+.. |EPASSIVE| mathdef:: \xref{syntax/modules}{syntax-elemmode}{\K{passive}}
+.. |EACTIVE| mathdef:: \xref{syntax/modules}{syntax-elemmode}{\K{active}}
+.. |EDECLARATIVE| mathdef:: \xref{syntax/modules}{syntax-elemmode}{\K{declarative}}
+.. |ETABLE| mathdef:: \xref{syntax/modules}{syntax-elem}{\K{table}}
+.. |EOFFSET| mathdef:: \xref{syntax/modules}{syntax-elem}{\K{offset}}
+
+.. |DINIT| mathdef:: \xref{syntax/modules}{syntax-data}{\K{init}}
+.. |DMODE| mathdef:: \xref{syntax/modules}{syntax-data}{\K{mode}}
+.. |DPASSIVE| mathdef:: \xref{syntax/modules}{syntax-datamode}{\K{passive}}
+.. |DACTIVE| mathdef:: \xref{syntax/modules}{syntax-datamode}{\K{active}}
+.. |DMEM| mathdef:: \xref{syntax/modules}{syntax-data}{\K{memory}}
+.. |DOFFSET| mathdef:: \xref{syntax/modules}{syntax-data}{\K{offset}}
+
+.. |SFUNC| mathdef:: \xref{syntax/modules}{syntax-start}{\K{func}}
+
+.. |ENAME| mathdef:: \xref{syntax/modules}{syntax-export}{\K{name}}
+.. |EDESC| mathdef:: \xref{syntax/modules}{syntax-export}{\K{desc}}
+.. |EDFUNC| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\K{func}}
+.. |EDTABLE| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\K{table}}
+.. |EDMEM| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\K{mem}}
+.. |EDGLOBAL| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\K{global}}
+
+.. |IMODULE| mathdef:: \xref{syntax/modules}{syntax-import}{\K{module}}
+.. |INAME| mathdef:: \xref{syntax/modules}{syntax-import}{\K{name}}
+.. |IDESC| mathdef:: \xref{syntax/modules}{syntax-import}{\K{desc}}
+.. |IDFUNC| mathdef:: \xref{syntax/modules}{syntax-importdesc}{\K{func}}
+.. |IDTABLE| mathdef:: \xref{syntax/modules}{syntax-importdesc}{\K{table}}
+.. |IDMEM| mathdef:: \xref{syntax/modules}{syntax-importdesc}{\K{mem}}
+.. |IDGLOBAL| mathdef:: \xref{syntax/modules}{syntax-importdesc}{\K{global}}
+
+
+.. Modules, non-terminals
+
+.. |module| mathdef:: \xref{syntax/modules}{syntax-module}{\X{module}}
+.. |type| mathdef:: \xref{syntax/types}{syntax-functype}{\X{type}}
+.. |func| mathdef:: \xref{syntax/modules}{syntax-func}{\X{func}}
+.. |table| mathdef:: \xref{syntax/modules}{syntax-table}{\X{table}}
+.. |mem| mathdef:: \xref{syntax/modules}{syntax-mem}{\X{mem}}
+.. |global| mathdef:: \xref{syntax/modules}{syntax-global}{\X{global}}
+.. |import| mathdef:: \xref{syntax/modules}{syntax-import}{\X{import}}
+.. |export| mathdef:: \xref{syntax/modules}{syntax-export}{\X{export}}
+.. |importdesc| mathdef:: \xref{syntax/modules}{syntax-importdesc}{\X{importdesc}}
+.. |exportdesc| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\X{exportdesc}}
+.. |elem| mathdef:: \xref{syntax/modules}{syntax-elem}{\X{elem}}
+.. |elemmode| mathdef:: \xref{syntax/modules}{syntax-elemmode}{\X{elemmode}}
+.. |data| mathdef:: \xref{syntax/modules}{syntax-data}{\X{data}}
+.. |datamode| mathdef:: \xref{syntax/modules}{syntax-datamode}{\X{datamode}}
+.. |start| mathdef:: \xref{syntax/modules}{syntax-start}{\X{start}}
+
+
+.. Modules, meta functions
+
+.. |edfuncs| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{funcs}}
+.. |edtables| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{tables}}
+.. |edmems| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{mems}}
+.. |edglobals| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{globals}}
+
+
+.. Instructions, terminals
+
+.. |OFFSET| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{offset}}
+.. |ALIGN| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{align}}
+
+.. |UNREACHABLE| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{unreachable}}
+.. |NOP| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{nop}}
+.. |BLOCK| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{block}}
+.. |LOOP| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{loop}}
+.. |IF| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{if}}
+.. |ELSE| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{else}}
+.. |END| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{end}}
+.. |BR| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br}}
+.. |BRIF| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_if}}
+.. |BRTABLE| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_table}}
+.. |RETURN| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{return}}
+.. |CALL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{call}}
+.. |CALLINDIRECT| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{call\_indirect}}
+
+.. |DROP| mathdef:: \xref{syntax/instructions}{syntax-instr-parametric}{\K{drop}}
+.. |SELECT| mathdef:: \xref{syntax/instructions}{syntax-instr-parametric}{\K{select}}
+
+.. |LOCALGET| mathdef:: \xref{syntax/instructions}{syntax-instr-variable}{\K{local.get}}
+.. |LOCALSET| mathdef:: \xref{syntax/instructions}{syntax-instr-variable}{\K{local.set}}
+.. |LOCALTEE| mathdef:: \xref{syntax/instructions}{syntax-instr-variable}{\K{local.tee}}
+.. |GLOBALGET| mathdef:: \xref{syntax/instructions}{syntax-instr-variable}{\K{global.get}}
+.. |GLOBALSET| mathdef:: \xref{syntax/instructions}{syntax-instr-variable}{\K{global.set}}
+
+.. |TABLEGET| mathdef:: \xref{syntax/instructions}{syntax-instr-table}{\K{table.get}}
+.. |TABLESET| mathdef:: \xref{syntax/instructions}{syntax-instr-table}{\K{table.set}}
+.. |TABLESIZE| mathdef:: \xref{syntax/instructions}{syntax-instr-table}{\K{table.size}}
+.. |TABLEGROW| mathdef:: \xref{syntax/instructions}{syntax-instr-table}{\K{table.grow}}
+.. |TABLEFILL| mathdef:: \xref{syntax/instructions}{syntax-instr-table}{\K{table.fill}}
+.. |TABLECOPY| mathdef:: \xref{syntax/instructions}{syntax-instr-table}{\K{table.copy}}
+.. |TABLEINIT| mathdef:: \xref{syntax/instructions}{syntax-instr-table}{\K{table.init}}
+.. |ELEMDROP| mathdef:: \xref{syntax/instructions}{syntax-instr-table}{\K{elem.drop}}
+
+.. |LOAD| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{load}}
+.. |STORE| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{store}}
+.. |MEMORYSIZE| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{memory.size}}
+.. |MEMORYGROW| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{memory.grow}}
+.. |MEMORYFILL| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{memory.fill}}
+.. |MEMORYCOPY| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{memory.copy}}
+.. |MEMORYINIT| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{memory.init}}
+.. |DATADROP| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{data.drop}}
+
+.. |REFNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}null}}
+.. |REFISNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}is\_null}}
+.. |REFFUNC| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}func}}
+
+.. |CONST| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{const}}
+.. |EQZ| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{eqz}}
+.. |EQ| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{eq}}
+.. |NE| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{ne}}
+.. |LT| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{lt}}
+.. |GT| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{gt}}
+.. |LE| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{le}}
+.. |GE| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{ge}}
+.. |CLZ| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{clz}}
+.. |CTZ| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{ctz}}
+.. |POPCNT| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{popcnt}}
+.. |ABS| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{abs}}
+.. |NEG| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{neg}}
+.. |CEIL| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{ceil}}
+.. |FLOOR| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{floor}}
+.. |TRUNC| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{trunc}}
+.. |NEAREST| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{nearest}}
+.. |SQRT| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{sqrt}}
+.. |ADD| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{add}}
+.. |SUB| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{sub}}
+.. |MUL| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{mul}}
+.. |DIV| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{div}}
+.. |REM| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{rem}}
+.. |FMIN| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{min}}
+.. |FMAX| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{max}}
+.. |AND| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{and}}
+.. |OR| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{or}}
+.. |XOR| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{xor}}
+.. |SHL| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{shl}}
+.. |SHR| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{shr}}
+.. |ROTL| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{rotl}}
+.. |ROTR| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{rotr}}
+.. |COPYSIGN| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{copysign}}
+
+.. |CONVERT| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{convert}}
+.. |EXTEND| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{extend}}
+.. |WRAP| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{wrap}}
+.. |PROMOTE| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{promote}}
+.. |DEMOTE| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{demote}}
+.. |REINTERPRET| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{reinterpret}}
+
+.. |VCONST| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{const}}
+.. |SHUFFLE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{shuffle}}
+.. |SWIZZLE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{swizzle}}
+.. |SPLAT| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{splat}}
+.. |EXTRACTLANE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{extract\_lane}}
+.. |REPLACELANE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{replace\_lane}}
+.. |VNOT| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{not}}
+.. |VAND| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{and}}
+.. |VANDNOT| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{andnot}}
+.. |VOR| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{or}}
+.. |VXOR| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{xor}}
+.. |BITSELECT| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{bitselect}}
+.. |VEQ| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{eq}}
+.. |VNE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{ne}}
+.. |VLT| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{lt}}
+.. |VGT| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{gt}}
+.. |VLE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{le}}
+.. |VGE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{ge}}
+.. |VABS| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{abs}}
+.. |VNEG| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{neg}}
+.. |VCEIL| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{ceil}}
+.. |VFLOOR| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{floor}}
+.. |VTRUNC| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{trunc}}
+.. |VNEAREST| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{nearest}}
+.. |VPOPCNT| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{popcnt}}
+.. |ANYTRUE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{any\_true}}
+.. |ALLTRUE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{all\_true}}
+.. |BITMASK| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{bitmask}}
+.. |VSHL| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{shl}}
+.. |VSHR| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{shr}}
+.. |VSQRT| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{sqrt}}
+.. |VADD| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{add}}
+.. |VSUB| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{sub}}
+.. |VMUL| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{mul}}
+.. |VDIV| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{div}}
+.. |VMIN| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{min}}
+.. |VMAX| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{max}}
+.. |VPMIN| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{pmin}}
+.. |VPMAX| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{pmax}}
+.. |NARROW| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{narrow}}
+.. |VEXTEND| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{extend}}
+.. |AVGR| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{avgr}}
+.. |DOT| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{dot}}
+.. |EXTMUL| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{extmul}}
+.. |VCONVERT| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{convert}}
+.. |Q15MULRSAT| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{q15mulr\_sat}}
+.. |EXTADDPAIRWISE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{extadd\_pairwise}}
+.. |VDEMOTE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{demote}}
+.. |VPROMOTE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{promote}}
+
+
+.. Instructions, non-terminals
+
+.. |unop| mathdef:: \xref{syntax/instructions}{syntax-unop}{\X{unop}}
+.. |binop| mathdef:: \xref{syntax/instructions}{syntax-binop}{\X{binop}}
+.. |testop| mathdef:: \xref{syntax/instructions}{syntax-testop}{\X{testop}}
+.. |relop| mathdef:: \xref{syntax/instructions}{syntax-relop}{\X{relop}}
+.. |cvtop| mathdef:: \xref{syntax/instructions}{syntax-cvtop}{\X{cvtop}}
+
+.. |unopF| mathdef:: \xref{exec/instructions}{exec-instr-numeric}{\X{unop}}
+.. |binopF| mathdef:: \xref{exec/instructions}{exec-instr-numeric}{\X{binop}}
+.. |testopF| mathdef:: \xref{exec/instructions}{exec-instr-numeric}{\X{testop}}
+.. |relopF| mathdef:: \xref{exec/instructions}{exec-instr-numeric}{\X{relop}}
+.. |cvtopF| mathdef:: \xref{exec/instructions}{exec-instr-numeric}{\X{cvtop}}
+
+.. |iunop| mathdef:: \xref{syntax/instructions}{syntax-iunop}{\X{iunop}}
+.. |ibinop| mathdef:: \xref{syntax/instructions}{syntax-ibinop}{\X{ibinop}}
+.. |itestop| mathdef:: \xref{syntax/instructions}{syntax-itestop}{\X{itestop}}
+.. |irelop| mathdef:: \xref{syntax/instructions}{syntax-irelop}{\X{irelop}}
+
+.. |funop| mathdef:: \xref{syntax/instructions}{syntax-funop}{\X{funop}}
+.. |fbinop| mathdef:: \xref{syntax/instructions}{syntax-fbinop}{\X{fbinop}}
+.. |ftestop| mathdef:: \xref{syntax/instructions}{syntax-ftestop}{\X{ftestop}}
+.. |frelop| mathdef:: \xref{syntax/instructions}{syntax-frelop}{\X{frelop}}
+
+.. |ishape| mathdef:: \xref{syntax/instructions}{syntax-shape}{\X{ishape}}
+.. |fshape| mathdef:: \xref{syntax/instructions}{syntax-shape}{\X{fshape}}
+.. |shape| mathdef:: \xref{syntax/instructions}{syntax-shape}{\X{shape}}
+
+.. |vunop| mathdef:: \xref{syntax/instructions}{syntax-vunop}{\X{vunop}}
+.. |vbinop| mathdef:: \xref{syntax/instructions}{syntax-vbinop}{\X{vbinop}}
+.. |vrelop| mathdef:: \xref{syntax/instructions}{syntax-vrelop}{\X{vrelop}}
+.. |vcvtop| mathdef:: \xref{syntax/instructions}{syntax-vcvtop}{\X{vcvtop}}
+
+.. |laneidx| mathdef:: \xref{syntax/instructions}{syntax-laneidx}{\X{laneidx}}
+.. |vvunop| mathdef:: \xref{syntax/instructions}{syntax-vvunop}{\X{vvunop}}
+.. |vvbinop| mathdef:: \xref{syntax/instructions}{syntax-vvbinop}{\X{vvbinop}}
+.. |vvternop| mathdef:: \xref{syntax/instructions}{syntax-vvternop}{\X{vvternop}}
+.. |vvtestop| mathdef:: \xref{syntax/instructions}{syntax-vvtestop}{\X{vvtestop}}
+.. |vishiftop| mathdef:: \xref{syntax/instructions}{syntax-vishiftop}{\X{vishiftop}}
+.. |viunop| mathdef:: \xref{syntax/instructions}{syntax-viunop}{\X{viunop}}
+.. |vibinop| mathdef:: \xref{syntax/instructions}{syntax-vibinop}{\X{vibinop}}
+.. |viminmaxop| mathdef:: \xref{syntax/instructions}{syntax-viminmaxop}{\X{viminmaxop}}
+.. |visatbinop| mathdef:: \xref{syntax/instructions}{syntax-visatbinop}{\X{visatbinop}}
+.. |vfunop| mathdef:: \xref{syntax/instructions}{syntax-vfunop}{\X{vfunop}}
+.. |vfbinop| mathdef:: \xref{syntax/instructions}{syntax-vfbinop}{\X{vfbinop}}
+.. |virelop| mathdef:: \xref{syntax/instructions}{syntax-virelop}{\X{virelop}}
+.. |vfrelop| mathdef:: \xref{syntax/instructions}{syntax-vfrelop}{\X{vfrelop}}
+.. |vitestop| mathdef:: \xref{syntax/instructions}{syntax-vitestop}{\X{vitestop}}
+.. |vtestop| mathdef:: \xref{syntax/instructions}{syntax-vtestop}{\X{vtestop}}
+
+.. |sx| mathdef:: \xref{syntax/instructions}{syntax-sx}{\X{sx}}
+.. |half| mathdef:: \xref{syntax/instructions}{syntax-half}{\X{half}}
+.. |memarg| mathdef:: \xref{syntax/instructions}{syntax-memarg}{\X{memarg}}
+
+.. |blocktype| mathdef:: \xref{syntax/instructions}{syntax-blocktype}{\X{blocktype}}
+
+.. |instr| mathdef:: \xref{syntax/instructions}{syntax-instr}{\X{instr}}
+.. |expr| mathdef:: \xref{syntax/instructions}{syntax-expr}{\X{expr}}
+
+
+
+.. Binary Format
+.. -------------
+
+.. Auxiliary productions
+
+.. |Bvec| mathdef:: \xref{binary/conventions}{binary-vec}{\B{vec}}
+
+
+.. Values, non-terminals
+
+.. |Bbyte| mathdef:: \xref{binary/values}{binary-byte}{\B{byte}}
+
+.. |BuX#1| mathdef:: {\B{u}#1}
+.. |BsX#1| mathdef:: {\B{s}#1}
+.. |BiX#1| mathdef:: {\B{i}#1}
+.. |BfX#1| mathdef:: {\B{f}#1}
+
+.. |BuN| mathdef:: \xref{binary/values}{binary-int}{\BuX{N}}
+.. |Bu1| mathdef:: \xref{binary/values}{binary-int}{\BuX{\B{1}}}
+.. |Bu8| mathdef:: \xref{binary/values}{binary-int}{\BuX{\B{8}}}
+.. |Bu16| mathdef:: \xref{binary/values}{binary-int}{\BuX{\B{16}}}
+.. |Bu32| mathdef:: \xref{binary/values}{binary-int}{\BuX{\B{32}}}
+.. |Bu64| mathdef:: \xref{binary/values}{binary-int}{\BuX{\B{64}}}
+
+.. |BsN| mathdef:: \xref{binary/values}{binary-int}{\BsX{N}}
+.. |Bs7| mathdef:: \xref{binary/values}{binary-int}{\BsX{\B{7}}}
+.. |Bs32| mathdef:: \xref{binary/values}{binary-int}{\BsX{\B{32}}}
+.. |Bs33| mathdef:: \xref{binary/values}{binary-int}{\BsX{\B{33}}}
+.. |Bs64| mathdef:: \xref{binary/values}{binary-int}{\BsX{\B{64}}}
+
+.. |BiN| mathdef:: \xref{binary/values}{binary-int}{\BiX{N}}
+.. |Bi32| mathdef:: \xref{binary/values}{binary-int}{\BiX{\B{32}}}
+.. |Bi64| mathdef:: \xref{binary/values}{binary-int}{\BiX{\B{64}}}
+
+.. |BfN| mathdef:: \xref{binary/values}{binary-float}{\BfX{N}}
+.. |Bf32| mathdef:: \xref{binary/values}{binary-float}{\BfX{\B{32}}}
+.. |Bf64| mathdef:: \xref{binary/values}{binary-float}{\BfX{\B{64}}}
+
+.. |Bname| mathdef:: \xref{binary/values}{binary-name}{\B{name}}
+
+
+.. Values, meta functions
+
+.. |utf8| mathdef:: \xref{binary/values}{binary-utf8}{\F{utf8}}
+
+
+.. Types, non-terminals
+
+.. |Bnumtype| mathdef:: \xref{binary/types}{binary-numtype}{\B{numtype}}
+.. |Bvectype| mathdef:: \xref{binary/types}{binary-vectype}{\B{vectype}}
+.. |Breftype| mathdef:: \xref{binary/types}{binary-reftype}{\B{reftype}}
+.. |Bvaltype| mathdef:: \xref{binary/types}{binary-valtype}{\B{valtype}}
+.. |Bresulttype| mathdef:: \xref{binary/types}{binary-resulttype}{\B{resulttype}}
+.. |Bfunctype| mathdef:: \xref{binary/types}{binary-functype}{\B{functype}}
+.. |Bglobaltype| mathdef:: \xref{binary/types}{binary-globaltype}{\B{globaltype}}
+.. |Btabletype| mathdef:: \xref{binary/types}{binary-tabletype}{\B{tabletype}}
+.. |Bmemtype| mathdef:: \xref{binary/types}{binary-memtype}{\B{memtype}}
+.. |Blimits| mathdef:: \xref{binary/types}{binary-limits}{\B{limits}}
+.. |Bmut| mathdef:: \xref{binary/types}{binary-mut}{\B{mut}}
+
+
+.. Indices, non-terminals
+
+.. |Bidx| mathdef:: \xref{binary/modules}{binary-index}{\B{idx}}
+.. |Btypeidx| mathdef:: \xref{binary/modules}{binary-typeidx}{\B{typeidx}}
+.. |Bfuncidx| mathdef:: \xref{binary/modules}{binary-funcidx}{\B{funcidx}}
+.. |Btableidx| mathdef:: \xref{binary/modules}{binary-tableidx}{\B{tableidx}}
+.. |Bmemidx| mathdef:: \xref{binary/modules}{binary-memidx}{\B{memidx}}
+.. |Bglobalidx| mathdef:: \xref{binary/modules}{binary-globalidx}{\B{globalidx}}
+.. |Belemidx| mathdef:: \xref{binary/modules}{binary-elemidx}{\B{elemidx}}
+.. |Bdataidx| mathdef:: \xref{binary/modules}{binary-dataidx}{\B{dataidx}}
+.. |Blocalidx| mathdef:: \xref{binary/modules}{binary-localidx}{\B{localidx}}
+.. |Blabelidx| mathdef:: \xref{binary/modules}{binary-labelidx}{\B{labelidx}}
+
+
+.. Modules, non-terminals
+
+.. |Bmagic| mathdef:: \xref{binary/modules}{binary-magic}{\B{magic}}
+.. |Bversion| mathdef:: \xref{binary/modules}{binary-version}{\B{version}}
+.. |Bmodule| mathdef:: \xref{binary/modules}{binary-module}{\B{module}}
+
+.. |Bsection| mathdef:: \xref{binary/modules}{binary-section}{\B{section}}
+.. |Bcustomsec| mathdef:: \xref{binary/modules}{binary-customsec}{\B{customsec}}
+.. |Btypesec| mathdef:: \xref{binary/modules}{binary-typesec}{\B{typesec}}
+.. |Bfuncsec| mathdef:: \xref{binary/modules}{binary-funcsec}{\B{funcsec}}
+.. |Bcodesec| mathdef:: \xref{binary/modules}{binary-codesec}{\B{codesec}}
+.. |Btablesec| mathdef:: \xref{binary/modules}{binary-tablesec}{\B{tablesec}}
+.. |Bmemsec| mathdef:: \xref{binary/modules}{binary-memsec}{\B{memsec}}
+.. |Bglobalsec| mathdef:: \xref{binary/modules}{binary-globalsec}{\B{globalsec}}
+.. |Bimportsec| mathdef:: \xref{binary/modules}{binary-importsec}{\B{importsec}}
+.. |Bexportsec| mathdef:: \xref{binary/modules}{binary-exportsec}{\B{exportsec}}
+.. |Belemsec| mathdef:: \xref{binary/modules}{binary-elemsec}{\B{elemsec}}
+.. |Bdatasec| mathdef:: \xref{binary/modules}{binary-datasec}{\B{datasec}}
+.. |Bstartsec| mathdef:: \xref{binary/modules}{binary-startsec}{\B{startsec}}
+.. |Bdatacountsec| mathdef:: \xref{binary/modules}{binary-datacountsec}{\B{datacountsec}}
+
+.. |Bcustom| mathdef:: \xref{binary/modules}{binary-customsec}{\B{custom}}
+.. |Btype| mathdef:: \xref{binary/modules}{binary-typedef}{\B{type}}
+.. |Bfunc| mathdef:: \xref{binary/modules}{binary-func}{\B{func}}
+.. |Btable| mathdef:: \xref{binary/modules}{binary-table}{\B{table}}
+.. |Bmem| mathdef:: \xref{binary/modules}{binary-mem}{\B{mem}}
+.. |Bglobal| mathdef:: \xref{binary/modules}{binary-global}{\B{global}}
+.. |Bimport| mathdef:: \xref{binary/modules}{binary-import}{\B{import}}
+.. |Bexport| mathdef:: \xref{binary/modules}{binary-export}{\B{export}}
+.. |Bimportdesc| mathdef:: \xref{binary/modules}{binary-importdesc}{\B{importdesc}}
+.. |Bexportdesc| mathdef:: \xref{binary/modules}{binary-exportdesc}{\B{exportdesc}}
+.. |Belem| mathdef:: \xref{binary/modules}{binary-elem}{\B{elem}}
+.. |Belemkind| mathdef:: \xref{binary/modules}{binary-elemkind}{\B{elemkind}}
+.. |Bcode| mathdef:: \xref{binary/modules}{binary-code}{\B{code}}
+.. |Blocal| mathdef:: \xref{binary/modules}{binary-local}{\B{local}}
+.. |Blocals| mathdef:: \xref{binary/modules}{binary-local}{\B{locals}}
+.. |Bdata| mathdef:: \xref{binary/modules}{binary-data}{\B{data}}
+.. |Bstart| mathdef:: \xref{binary/modules}{binary-start}{\B{start}}
+
+
+.. Instructions, non-terminals
+
+.. |Bmemarg| mathdef:: \xref{binary/instructions}{binary-memarg}{\B{memarg}}
+.. |Bblocktype| mathdef:: \xref{binary/instructions}{binary-blocktype}{\B{blocktype}}
+
+.. |Binstr| mathdef:: \xref{binary/instructions}{binary-instr}{\B{instr}}
+.. |Bexpr| mathdef:: \xref{binary/instructions}{binary-expr}{\B{expr}}
+
+.. |Blaneidx| mathdef:: \xref{binary/instructions}{binary-laneidx}{\B{laneidx}}
+
+
+.. Text Format
+.. -----------
+
+.. Auxiliary productions
+
+.. |Tvec| mathdef:: \xref{text/conventions}{text-vec}{\T{vec}}
+
+
+.. Lexical grammar, terminals
+
+.. |textl| mathdef:: \mbox{‘}
+.. |textr| mathdef:: \mbox{’}
+.. |text#1| mathdef:: \textl\mathtt{#1}\textr
+
+.. |Tcommentl| mathdef:: \text{{(}{;}}
+.. |Tcommentr| mathdef:: \text{{;}{)}}
+.. |Tcommentd| mathdef:: \text{{;}{;}}
+
+
+.. Lexical grammar, non-terminals
+
+.. |Tsource| mathdef:: \xref{text/lexical}{text-source}{\T{source}}
+.. |Tchar| mathdef:: \xref{text/lexical}{text-char}{\T{char}}
+.. |Tspace| mathdef:: \xref{text/lexical}{text-space}{\T{space}}
+.. |Tformat| mathdef:: \xref{text/lexical}{text-format}{\T{format}}
+.. |Tnewline| mathdef:: \xref{text/lexical}{text-newline}{\T{newline}}
+
+.. |Ttoken| mathdef:: \xref{text/lexical}{text-token}{\T{token}}
+.. |Tkeyword| mathdef:: \xref{text/lexical}{text-keyword}{\T{keyword}}
+.. |Treserved| mathdef:: \xref{text/lexical}{text-reserved}{\T{reserved}}
+
+.. |Tcomment| mathdef:: \xref{text/lexical}{text-comment}{\T{comment}}
+.. |Tlinecomment| mathdef:: \xref{text/lexical}{text-comment}{\T{linecomment}}
+.. |Tblockcomment| mathdef:: \xref{text/lexical}{text-comment}{\T{blockcomment}}
+.. |Tlinechar| mathdef:: \xref{text/lexical}{text-comment}{\T{linechar}}
+.. |Tblockchar| mathdef:: \xref{text/lexical}{text-comment}{\T{blockchar}}
+
+
+.. Values, non-terminals
+
+.. |Tsign| mathdef:: \xref{text/values}{text-sign}{\T{sign}}
+.. |Tdigit| mathdef:: \xref{text/values}{text-digit}{\T{digit}}
+.. |Thexdigit| mathdef:: \xref{text/values}{text-hexdigit}{\T{hexdigit}}
+.. |Tnum| mathdef:: \xref{text/values}{text-num}{\T{num}}
+.. |Thexnum| mathdef:: \xref{text/values}{text-hexnum}{\T{hexnum}}
+.. |Tfrac| mathdef:: \xref{text/values}{text-frac}{\T{frac}}
+.. |Thexfrac| mathdef:: \xref{text/values}{text-hexfrac}{\T{hexfrac}}
+.. |Tfloat| mathdef:: \xref{text/values}{text-float}{\T{float}}
+.. |Thexfloat| mathdef:: \xref{text/values}{text-hexfloat}{\T{hexfloat}}
+
+.. |TuX#1| mathdef:: {\T{u}#1}
+.. |TsX#1| mathdef:: {\T{s}#1}
+.. |TiX#1| mathdef:: {\T{i}#1}
+.. |TfX#1| mathdef:: {\T{f}#1}
+
+.. |TuN| mathdef:: \xref{text/values}{text-int}{\TuX{N}}
+.. |Tu1| mathdef:: \xref{text/values}{text-int}{\TuX{\T{1}}}
+.. |Tu8| mathdef:: \xref{text/values}{text-int}{\TuX{\T{8}}}
+.. |Tu16| mathdef:: \xref{text/values}{text-int}{\TuX{\T{16}}}
+.. |Tu32| mathdef:: \xref{text/values}{text-int}{\TuX{\T{32}}}
+.. |Tu64| mathdef:: \xref{text/values}{text-int}{\TuX{\T{64}}}
+
+.. |TsN| mathdef:: \xref{text/values}{text-int}{\TsX{N}}
+.. |Ts32| mathdef:: \xref{text/values}{text-int}{\TsX{\T{32}}}
+.. |Ts64| mathdef:: \xref{text/values}{text-int}{\TsX{\T{64}}}
+
+.. |TiN| mathdef:: \xref{text/values}{text-int}{\TiX{N}}
+.. |Ti8| mathdef:: \xref{text/values}{text-int}{\TiX{\T{8}}}
+.. |Ti16| mathdef:: \xref{text/values}{text-int}{\TiX{\T{16}}}
+.. |Ti32| mathdef:: \xref{text/values}{text-int}{\TiX{\T{32}}}
+.. |Ti64| mathdef:: \xref{text/values}{text-int}{\TiX{\T{64}}}
+
+.. |TfN| mathdef:: \xref{text/values}{text-float}{\TfX{N}}
+.. |TfNmag| mathdef:: \xref{text/values}{text-float}{\TfX{N}\T{mag}}
+.. |Tf32| mathdef:: \xref{text/values}{text-float}{\TfX{\T{32}}}
+.. |Tf64| mathdef:: \xref{text/values}{text-float}{\TfX{\T{64}}}
+
+.. |Tstring| mathdef:: \xref{text/values}{text-string}{\T{string}}
+.. |Tstringelem| mathdef:: \xref{text/values}{text-string}{\T{stringelem}}
+.. |Tstringchar| mathdef:: \xref{text/values}{text-string}{\T{stringchar}}
+.. |Tname| mathdef:: \xref{text/values}{text-name}{\T{name}}
+
+.. |Tid| mathdef:: \xref{text/values}{text-id}{\T{id}}
+.. |Tidchar| mathdef:: \xref{text/values}{text-idchar}{\T{idchar}}
+
+
+.. Types, non-terminals
+
+.. |Tnumtype| mathdef:: \xref{text/types}{text-numtype}{\T{numtype}}
+.. |Tvectype| mathdef:: \xref{text/types}{text-vectype}{\T{vectype}}
+.. |Treftype| mathdef:: \xref{text/types}{text-reftype}{\T{reftype}}
+.. |Theaptype| mathdef:: \xref{text/types}{text-heaptype}{\T{heaptype}}
+.. |Tvaltype| mathdef:: \xref{text/types}{text-valtype}{\T{valtype}}
+.. |Tfunctype| mathdef:: \xref{text/types}{text-functype}{\T{functype}}
+
+.. |Tglobaltype| mathdef:: \xref{text/types}{text-globaltype}{\T{globaltype}}
+.. |Ttabletype| mathdef:: \xref{text/types}{text-tabletype}{\T{tabletype}}
+.. |Tmemtype| mathdef:: \xref{text/types}{text-memtype}{\T{memtype}}
+.. |Tlimits| mathdef:: \xref{text/types}{text-limits}{\T{limits}}
+
+.. |Tparam| mathdef:: \xref{text/types}{text-functype}{\T{param}}
+.. |Tresult| mathdef:: \xref{text/types}{text-functype}{\T{result}}
+
+
+.. Indices, non-terminals
+
+.. |Ttypeidx| mathdef:: \xref{text/modules}{text-typeidx}{\T{typeidx}}
+.. |Tfuncidx| mathdef:: \xref{text/modules}{text-funcidx}{\T{funcidx}}
+.. |Ttableidx| mathdef:: \xref{text/modules}{text-tableidx}{\T{tableidx}}
+.. |Tmemidx| mathdef:: \xref{text/modules}{text-memidx}{\T{memidx}}
+.. |Tglobalidx| mathdef:: \xref{text/modules}{text-globalidx}{\T{globalidx}}
+.. |Telemidx| mathdef:: \xref{text/modules}{text-elemidx}{\T{elemidx}}
+.. |Tdataidx| mathdef:: \xref{text/modules}{text-dataidx}{\T{dataidx}}
+.. |Tlocalidx| mathdef:: \xref{text/modules}{text-localidx}{\T{localidx}}
+.. |Tlabelidx| mathdef:: \xref{text/modules}{text-labelidx}{\T{labelidx}}
+
+
+.. Modules, non-terminals
+
+.. |Tmodule| mathdef:: \xref{text/modules}{text-module}{\T{module}}
+.. |Tmodulefield| mathdef:: \xref{text/modules}{text-modulefield}{\T{modulefield}}
+.. |Ttype| mathdef:: \xref{text/modules}{text-typedef}{\T{type}}
+.. |Ttypeuse| mathdef:: \xref{text/modules}{text-typeuse}{\T{typeuse}}
+.. |Tfunc| mathdef:: \xref{text/modules}{text-func}{\T{func}}
+.. |Ttable| mathdef:: \xref{text/modules}{text-table}{\T{table}}
+.. |Tmem| mathdef:: \xref{text/modules}{text-mem}{\T{mem}}
+.. |Tglobal| mathdef:: \xref{text/modules}{text-global}{\T{global}}
+.. |Timport| mathdef:: \xref{text/modules}{text-import}{\T{import}}
+.. |Texport| mathdef:: \xref{text/modules}{text-export}{\T{export}}
+.. |Timportdesc| mathdef:: \xref{text/modules}{text-importdesc}{\T{importdesc}}
+.. |Texportdesc| mathdef:: \xref{text/modules}{text-exportdesc}{\T{exportdesc}}
+.. |Telem| mathdef:: \xref{text/modules}{text-elem}{\T{elem}}
+.. |Telemlist| mathdef:: \xref{text/modules}{text-elemlist}{\T{elemlist}}
+.. |Telemexpr| mathdef:: \xref{text/modules}{text-elemexpr}{\T{elemexpr}}
+.. |Ttableuse| mathdef:: \xref{text/modules}{text-tableuse}{\T{tableuse}}
+.. |Tlocal| mathdef:: \xref{text/modules}{text-local}{\T{local}}
+.. |Tlocals| mathdef:: \xref{text/modules}{text-local}{\T{locals}}
+.. |Tdata| mathdef:: \xref{text/modules}{text-data}{\T{data}}
+.. |Tdatastring| mathdef:: \xref{text/modules}{text-datastring}{\T{datastring}}
+.. |Tmemuse| mathdef:: \xref{text/modules}{text-memuse}{\T{memuse}}
+.. |Tstart| mathdef:: \xref{text/modules}{text-start}{\T{start}}
+
+
+.. Instructions, non-terminals
+
+.. |Tmemarg| mathdef:: \xref{text/instructions}{text-memarg}{\T{memarg}}
+.. |Talign| mathdef:: \xref{text/instructions}{text-memarg}{\T{align}}
+.. |Toffset| mathdef:: \xref{text/instructions}{text-memarg}{\T{offset}}
+
+.. |Tblocktype| mathdef:: \xref{text/instructions}{text-blocktype}{\T{blocktype}}
+
+.. |Tlabel| mathdef:: \xref{text/instructions}{text-label}{\T{label}}
+.. |Tinstr| mathdef:: \xref{text/instructions}{text-instr}{\T{instr}}
+.. |Tplaininstr| mathdef:: \xref{text/instructions}{text-plaininstr}{\T{plaininstr}}
+.. |Tblockinstr| mathdef:: \xref{text/instructions}{text-blockinstr}{\T{blockinstr}}
+.. |Tfoldedinstr| mathdef:: \xref{text/instructions}{text-foldedinstr}{\T{foldedinstr}}
+.. |Texpr| mathdef:: \xref{text/instructions}{text-expr}{\T{expr}}
+
+
+
+.. Parsing
+.. -------
+
+.. Contexts
+
+.. |ITYPEDEFS| mathdef:: \xref{text/conventions}{text-context}{\K{typedefs}}
+.. |ITYPES| mathdef:: \xref{text/conventions}{text-context}{\K{types}}
+.. |IFUNCS| mathdef:: \xref{text/conventions}{text-context}{\K{funcs}}
+.. |ITABLES| mathdef:: \xref{text/conventions}{text-context}{\K{tables}}
+.. |IMEMS| mathdef:: \xref{text/conventions}{text-context}{\K{mems}}
+.. |IGLOBALS| mathdef:: \xref{text/conventions}{text-context}{\K{globals}}
+.. |IELEM| mathdef:: \xref{text/conventions}{text-context}{\K{elem}}
+.. |IDATA| mathdef:: \xref{text/conventions}{text-context}{\K{data}}
+.. |ILOCALS| mathdef:: \xref{text/conventions}{text-context}{\K{locals}}
+.. |ILABELS| mathdef:: \xref{text/conventions}{text-context}{\K{labels}}
+
+
+.. Meta Functions
+
+.. |idfresh| mathdef:: ~\xref{text/values}{text-id-fresh}{\mbox{fresh}}
+.. |idcwellformed| mathdef:: ~\xref{text/conventions}{text-context-wf}{\mbox{well-formed}}
+
+
+
+
+.. Validation
+.. ----------
+
+.. Notation
+
+.. |ok| mathdef:: \mathrel{\mbox{ok}}
+.. |const| mathdef:: \xref{valid/instructions}{valid-constant}{\mathrel{\mbox{const}}}
+
+
+.. Contexts
+
+.. |CTYPES| mathdef:: \xref{valid/conventions}{context}{\K{types}}
+.. |CFUNCS| mathdef:: \xref{valid/conventions}{context}{\K{funcs}}
+.. |CTABLES| mathdef:: \xref{valid/conventions}{context}{\K{tables}}
+.. |CMEMS| mathdef:: \xref{valid/conventions}{context}{\K{mems}}
+.. |CGLOBALS| mathdef:: \xref{valid/conventions}{context}{\K{globals}}
+.. |CELEMS| mathdef:: \xref{valid/conventions}{context}{\K{elems}}
+.. |CDATAS| mathdef:: \xref{valid/conventions}{context}{\K{datas}}
+.. |CLOCALS| mathdef:: \xref{valid/conventions}{context}{\K{locals}}
+.. |CLABELS| mathdef:: \xref{valid/conventions}{context}{\K{labels}}
+.. |CRETURN| mathdef:: \xref{valid/conventions}{context}{\K{return}}
+.. |CREFS| mathdef:: \xref{valid/conventions}{context}{\K{refs}}
+
+
+.. Judgments
+
+.. |vdashlimits| mathdef:: \xref{valid/types}{valid-limits}{\vdash}
+.. |vdashblocktype| mathdef:: \xref{valid/types}{valid-blocktype}{\vdash}
+.. |vdashfunctype| mathdef:: \xref{valid/types}{valid-functype}{\vdash}
+.. |vdashtabletype| mathdef:: \xref{valid/types}{valid-tabletype}{\vdash}
+.. |vdashmemtype| mathdef:: \xref{valid/types}{valid-memtype}{\vdash}
+.. |vdashglobaltype| mathdef:: \xref{valid/types}{valid-globaltype}{\vdash}
+.. |vdashexterntype| mathdef:: \xref{valid/types}{valid-externtype}{\vdash}
+
+.. |vdashinstr| mathdef:: \xref{valid/instructions}{valid-instr}{\vdash}
+.. |vdashinstrseq| mathdef:: \xref{valid/instructions}{valid-instr-seq}{\vdash}
+.. |vdashexpr| mathdef:: \xref{valid/instructions}{valid-expr}{\vdash}
+.. |vdashexprconst| mathdef:: \xref{valid/instructions}{valid-constant}{\vdash}
+.. |vdashinstrconst| mathdef:: \xref{valid/instructions}{valid-constant}{\vdash}
+
+.. |vdashfunc| mathdef:: \xref{valid/modules}{valid-func}{\vdash}
+.. |vdashtable| mathdef:: \xref{valid/modules}{valid-table}{\vdash}
+.. |vdashmem| mathdef:: \xref{valid/modules}{valid-mem}{\vdash}
+.. |vdashglobal| mathdef:: \xref{valid/modules}{valid-global}{\vdash}
+.. |vdashelem| mathdef:: \xref{valid/modules}{valid-elem}{\vdash}
+.. |vdashelemmode| mathdef:: \xref{valid/modules}{valid-elemmode}{\vdash}
+.. |vdashdata| mathdef:: \xref{valid/modules}{valid-data}{\vdash}
+.. |vdashdatamode| mathdef:: \xref{valid/modules}{valid-datamode}{\vdash}
+.. |vdashstart| mathdef:: \xref{valid/modules}{valid-start}{\vdash}
+.. |vdashexport| mathdef:: \xref{valid/modules}{valid-export}{\vdash}
+.. |vdashexportdesc| mathdef:: \xref{valid/modules}{valid-exportdesc}{\vdash}
+.. |vdashimport| mathdef:: \xref{valid/modules}{valid-import}{\vdash}
+.. |vdashimportdesc| mathdef:: \xref{valid/modules}{valid-importdesc}{\vdash}
+.. |vdashmodule| mathdef:: \xref{valid/modules}{valid-module}{\vdash}
+
+.. |unpacked| mathdef:: \xref{valid/instructions}{aux-unpacked}{\F{unpacked}}
+.. |dim| mathdef:: \xref{valid/instructions}{aux-dim}{\F{dim}}
+
+
+.. Execution
+.. ---------
+
+.. Notation
+
+.. |stepto| mathdef:: \xref{exec/conventions}{exec-notation}{\hookrightarrow}
+.. |extendsto| mathdef:: \xref{appendix/properties}{extend}{\preceq}
+.. |matchesexterntype| mathdef:: \xref{valid/types}{match-externtype}{\leq}
+.. |matcheslimits| mathdef:: \xref{valid/types}{match-limits}{\leq}
+
+
+.. Allocation
+
+.. |allocfunc| mathdef:: \xref{exec/modules}{alloc-func}{\F{allocfunc}}
+.. |allochostfunc| mathdef:: \xref{exec/modules}{alloc-hostfunc}{\F{allochostfunc}}
+.. |alloctable| mathdef:: \xref{exec/modules}{alloc-table}{\F{alloctable}}
+.. |allocmem| mathdef:: \xref{exec/modules}{alloc-mem}{\F{allocmem}}
+.. |allocglobal| mathdef:: \xref{exec/modules}{alloc-global}{\F{allocglobal}}
+.. |allocelem| mathdef:: \xref{exec/modules}{alloc-elem}{\F{allocelem}}
+.. |allocdata| mathdef:: \xref{exec/modules}{alloc-data}{\F{allocdata}}
+.. |allocmodule| mathdef:: \xref{exec/modules}{alloc-module}{\F{allocmodule}}
+
+.. |growtable| mathdef:: \xref{exec/modules}{grow-table}{\F{growtable}}
+.. |growmem| mathdef:: \xref{exec/modules}{grow-mem}{\F{growmem}}
+
+
+.. Addresses, non-terminals
+
+.. |addr| mathdef:: \xref{exec/runtime}{syntax-addr}{\X{addr}}
+.. |funcaddr| mathdef:: \xref{exec/runtime}{syntax-funcaddr}{\X{funcaddr}}
+.. |tableaddr| mathdef:: \xref{exec/runtime}{syntax-tableaddr}{\X{tableaddr}}
+.. |memaddr| mathdef:: \xref{exec/runtime}{syntax-memaddr}{\X{memaddr}}
+.. |globaladdr| mathdef:: \xref{exec/runtime}{syntax-globaladdr}{\X{globaladdr}}
+.. |elemaddr| mathdef:: \xref{exec/runtime}{syntax-elemaddr}{\X{elemaddr}}
+.. |dataaddr| mathdef:: \xref{exec/runtime}{syntax-dataaddr}{\X{dataaddr}}
+.. |externaddr| mathdef:: \xref{exec/runtime}{syntax-externaddr}{\X{externaddr}}
+
+.. Instances, terminals
+
+.. |FITYPE| mathdef:: \xref{exec/runtime}{syntax-funcinst}{\K{type}}
+.. |FIMODULE| mathdef:: \xref{exec/runtime}{syntax-funcinst}{\K{module}}
+.. |FICODE| mathdef:: \xref{exec/runtime}{syntax-funcinst}{\K{code}}
+.. |FIHOSTCODE| mathdef:: \xref{exec/runtime}{syntax-funcinst}{\K{hostcode}}
+
+.. |TITYPE| mathdef:: \xref{exec/runtime}{syntax-tableinst}{\K{type}}
+.. |TIELEM| mathdef:: \xref{exec/runtime}{syntax-tableinst}{\K{elem}}
+
+.. |MITYPE| mathdef:: \xref{exec/runtime}{syntax-meminst}{\K{type}}
+.. |MIDATA| mathdef:: \xref{exec/runtime}{syntax-meminst}{\K{data}}
+
+.. |GITYPE| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\K{type}}
+.. |GIVALUE| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\K{value}}
+
+.. |EITYPE| mathdef:: \xref{exec/runtime}{syntax-eleminst}{\K{type}}
+.. |EIELEM| mathdef:: \xref{exec/runtime}{syntax-eleminst}{\K{elem}}
+
+.. |DIDATA| mathdef:: \xref{exec/runtime}{syntax-datainst}{\K{data}}
+
+.. |EINAME| mathdef:: \xref{exec/runtime}{syntax-exportinst}{\K{name}}
+.. |EIVALUE| mathdef:: \xref{exec/runtime}{syntax-exportinst}{\K{value}}
+
+.. |EVFUNC| mathdef:: \xref{exec/runtime}{syntax-externval}{\K{func}}
+.. |EVTABLE| mathdef:: \xref{exec/runtime}{syntax-externval}{\K{table}}
+.. |EVMEM| mathdef:: \xref{exec/runtime}{syntax-externval}{\K{mem}}
+.. |EVGLOBAL| mathdef:: \xref{exec/runtime}{syntax-externval}{\K{global}}
+
+.. |MITYPES| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{types}}
+.. |MIFUNCS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{funcaddrs}}
+.. |MITABLES| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{tableaddrs}}
+.. |MIMEMS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{memaddrs}}
+.. |MIGLOBALS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{globaladdrs}}
+.. |MIELEMS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{elemaddrs}}
+.. |MIDATAS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{dataaddrs}}
+.. |MIEXPORTS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{exports}}
+
+
+.. Instances, non-terminals
+
+.. |externval| mathdef:: \xref{exec/runtime}{syntax-externval}{\X{externval}}
+
+.. |moduleinst| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\X{moduleinst}}
+.. |funcinst| mathdef:: \xref{exec/runtime}{syntax-funcinst}{\X{funcinst}}
+.. |tableinst| mathdef:: \xref{exec/runtime}{syntax-tableinst}{\X{tableinst}}
+.. |meminst| mathdef:: \xref{exec/runtime}{syntax-meminst}{\X{meminst}}
+.. |globalinst| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\X{globalinst}}
+.. |eleminst| mathdef:: \xref{exec/runtime}{syntax-eleminst}{\X{eleminst}}
+.. |datainst| mathdef:: \xref{exec/runtime}{syntax-datainst}{\X{datainst}}
+.. |exportinst| mathdef:: \xref{exec/runtime}{syntax-exportinst}{\X{exportinst}}
+
+.. |hostfunc| mathdef:: \xref{exec/runtime}{syntax-hostfunc}{\X{hostfunc}}
+
+
+.. Instances, meta functions
+
+.. |evfuncs| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{funcs}}
+.. |evtables| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{tables}}
+.. |evmems| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{mems}}
+.. |evglobals| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{globals}}
+
+
+.. Store, terminals
+
+.. |SFUNCS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{funcs}}
+.. |STABLES| mathdef:: \xref{exec/runtime}{syntax-store}{\K{tables}}
+.. |SMEMS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{mems}}
+.. |SGLOBALS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{globals}}
+.. |SELEMS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{elems}}
+.. |SDATAS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{datas}}
+
+.. Store, non-terminals
+
+.. |store| mathdef:: \xref{exec/runtime}{syntax-store}{\X{store}}
+
+
+.. Stack, terminals
+
+.. |LABEL| mathdef:: \xref{exec/runtime}{syntax-label}{\K{label}}
+.. |FRAME| mathdef:: \xref{exec/runtime}{syntax-frame}{\K{frame}}
+
+.. |ALOCALS| mathdef:: \xref{exec/runtime}{syntax-frame}{\K{locals}}
+.. |AMODULE| mathdef:: \xref{exec/runtime}{syntax-frame}{\K{module}}
+
+
+.. Stack, non-terminals
+
+.. |label| mathdef:: \xref{exec/runtime}{syntax-label}{\X{label}}
+.. |frame| mathdef:: \xref{exec/runtime}{syntax-frame}{\X{frame}}
+.. |framestate| mathdef:: \xref{exec/runtime}{syntax-framestate}{\X{framestate}}
+
+
+.. Stack, meta functions
+
+.. |expand| mathdef:: \xref{exec/runtime}{exec-expand}{\F{expand}}
+
+
+.. Administrative Instructions, terminals
+
+.. |REFFUNCADDR| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref}}
+.. |REFEXTERNADDR| mathdef:: \xref{exec/runtime}{syntax-ref.extern}{\K{ref{.}extern}}
+.. |TRAP| mathdef:: \xref{exec/runtime}{syntax-trap}{\K{trap}}
+.. |INVOKE| mathdef:: \xref{exec/runtime}{syntax-invoke}{\K{invoke}}
+
+
+.. Values & Results, non-terminals
+
+.. |num| mathdef:: \xref{exec/runtime}{syntax-num}{\X{num}}
+.. |vecc| mathdef:: \xref{exec/runtime}{syntax-vecc}{\X{vec}}
+.. |reff| mathdef:: \xref{exec/runtime}{syntax-ref}{\X{ref}}
+.. |val| mathdef:: \xref{exec/runtime}{syntax-val}{\X{val}}
+.. |result| mathdef:: \xref{exec/runtime}{syntax-result}{\X{result}}
+
+
+.. Values, meta-functions
+
+.. |default| mathdef:: \xref{exec/runtime}{default-val}{\F{default}}
+
+
+.. Administrative Instructions, non-terminals
+
+.. |XB| mathdef:: \xref{exec/runtime}{syntax-ctxt-block}{B}
+
+
+.. Configurations, non-terminals
+
+.. |config| mathdef:: \xref{exec/runtime}{syntax-config}{\X{config}}
+.. |thread| mathdef:: \xref{exec/runtime}{syntax-thread}{\X{thread}}
+
+
+.. Numerics, operators
+
+.. |iadd| mathdef:: \xref{exec/numerics}{op-iadd}{\F{iadd}}
+.. |isub| mathdef:: \xref{exec/numerics}{op-isub}{\F{isub}}
+.. |imul| mathdef:: \xref{exec/numerics}{op-imul}{\F{imul}}
+.. |idivu| mathdef:: \xref{exec/numerics}{op-idiv_u}{\F{idiv\_u}}
+.. |idivs| mathdef:: \xref{exec/numerics}{op-idiv_s}{\F{idiv\_s}}
+.. |iremu| mathdef:: \xref{exec/numerics}{op-irem_u}{\F{irem\_u}}
+.. |irems| mathdef:: \xref{exec/numerics}{op-irem_s}{\F{irem\_s}}
+.. |inot| mathdef:: \xref{exec/numerics}{op-inot}{\F{inot}}
+.. |iand| mathdef:: \xref{exec/numerics}{op-iand}{\F{iand}}
+.. |iandnot| mathdef:: \xref{exec/numerics}{op-iandnot}{\F{iandnot}}
+.. |ior| mathdef:: \xref{exec/numerics}{op-ior}{\F{ior}}
+.. |ixor| mathdef:: \xref{exec/numerics}{op-ixor}{\F{ixor}}
+.. |ishl| mathdef:: \xref{exec/numerics}{op-ishl}{\F{ishl}}
+.. |ishru| mathdef:: \xref{exec/numerics}{op-ishr_u}{\F{ishr\_u}}
+.. |ishrs| mathdef:: \xref{exec/numerics}{op-ishr_s}{\F{ishr\_s}}
+.. |irotl| mathdef:: \xref{exec/numerics}{op-irotl}{\F{irotl}}
+.. |irotr| mathdef:: \xref{exec/numerics}{op-irotr}{\F{irotr}}
+.. |iclz| mathdef:: \xref{exec/numerics}{op-iclz}{\F{iclz}}
+.. |ictz| mathdef:: \xref{exec/numerics}{op-ictz}{\F{ictz}}
+.. |ipopcnt| mathdef:: \xref{exec/numerics}{op-ipopcnt}{\F{ipopcnt}}
+.. |ieqz| mathdef:: \xref{exec/numerics}{op-ieqz}{\F{ieqz}}
+.. |ieq| mathdef:: \xref{exec/numerics}{op-ieq}{\F{ieq}}
+.. |ine| mathdef:: \xref{exec/numerics}{op-ine}{\F{ine}}
+.. |iltu| mathdef:: \xref{exec/numerics}{op-ilt_u}{\F{ilt\_u}}
+.. |ilts| mathdef:: \xref{exec/numerics}{op-ilt_s}{\F{ilt\_s}}
+.. |igtu| mathdef:: \xref{exec/numerics}{op-igt_u}{\F{igt\_u}}
+.. |igts| mathdef:: \xref{exec/numerics}{op-igt_s}{\F{igt\_s}}
+.. |ileu| mathdef:: \xref{exec/numerics}{op-ile_u}{\F{ile\_u}}
+.. |iles| mathdef:: \xref{exec/numerics}{op-ile_s}{\F{ile\_s}}
+.. |igeu| mathdef:: \xref{exec/numerics}{op-ige_u}{\F{ige\_u}}
+.. |iges| mathdef:: \xref{exec/numerics}{op-ige_s}{\F{ige\_s}}
+.. |iextendMs| mathdef:: \xref{exec/numerics}{op-iextendn_s}{\F{iextend}M\F{\_s}}
+.. |ibitselect| mathdef:: \xref{exec/numerics}{op-ibitselect}{\F{ibitselect}}
+.. |iabs| mathdef:: \xref{exec/numerics}{op-iabs}{\F{iabs}}
+.. |ineg| mathdef:: \xref{exec/numerics}{op-ineg}{\F{ineg}}
+.. |iminu| mathdef:: \xref{exec/numerics}{op-imin_u}{\F{imin\_u}}
+.. |imins| mathdef:: \xref{exec/numerics}{op-imin_s}{\F{imin\_s}}
+.. |imaxu| mathdef:: \xref{exec/numerics}{op-imax_u}{\F{imax\_u}}
+.. |imaxs| mathdef:: \xref{exec/numerics}{op-imax_s}{\F{imax\_s}}
+.. |iaddsatu| mathdef:: \xref{exec/numerics}{op-iadd_sat_u}{\F{iadd\_sat\_u}}
+.. |iaddsats| mathdef:: \xref{exec/numerics}{op-iadd_sat_s}{\F{iadd\_sat\_s}}
+.. |isubsatu| mathdef:: \xref{exec/numerics}{op-isub_sat_u}{\F{isub\_sat\_u}}
+.. |isubsats| mathdef:: \xref{exec/numerics}{op-isub_sat_s}{\F{isub\_sat\_s}}
+.. |iavgru| mathdef:: \xref{exec/numerics}{op-iavgr_u}{\F{iavgr\_u}}
+.. |iq15mulrsats| mathdef:: \xref{exec/numerics}{op-iq15mulrsat_s}{\F{iq15mulrsat\_s}}
+
+.. |fadd| mathdef:: \xref{exec/numerics}{op-fadd}{\F{fadd}}
+.. |fsub| mathdef:: \xref{exec/numerics}{op-fsub}{\F{fsub}}
+.. |fmul| mathdef:: \xref{exec/numerics}{op-fmul}{\F{fmul}}
+.. |fdiv| mathdef:: \xref{exec/numerics}{op-fdiv}{\F{fdiv}}
+.. |fmin| mathdef:: \xref{exec/numerics}{op-fmin}{\F{fmin}}
+.. |fmax| mathdef:: \xref{exec/numerics}{op-fmax}{\F{fmax}}
+.. |fcopysign| mathdef:: \xref{exec/numerics}{op-fcopysign}{\F{fcopysign}}
+.. |fabs| mathdef:: \xref{exec/numerics}{op-fabs}{\F{fabs}}
+.. |fneg| mathdef:: \xref{exec/numerics}{op-fneg}{\F{fneg}}
+.. |fsqrt| mathdef:: \xref{exec/numerics}{op-fsqrt}{\F{fsqrt}}
+.. |fceil| mathdef:: \xref{exec/numerics}{op-fceil}{\F{fceil}}
+.. |ffloor| mathdef:: \xref{exec/numerics}{op-ffloor}{\F{ffloor}}
+.. |ftrunc| mathdef:: \xref{exec/numerics}{op-ftrunc}{\F{ftrunc}}
+.. |fnearest| mathdef:: \xref{exec/numerics}{op-fnearest}{\F{fnearest}}
+.. |feq| mathdef:: \xref{exec/numerics}{op-feq}{\F{feq}}
+.. |fne| mathdef:: \xref{exec/numerics}{op-fne}{\F{fne}}
+.. |flt| mathdef:: \xref{exec/numerics}{op-flt}{\F{flt}}
+.. |fgt| mathdef:: \xref{exec/numerics}{op-fgt}{\F{fgt}}
+.. |fle| mathdef:: \xref{exec/numerics}{op-fle}{\F{fle}}
+.. |fge| mathdef:: \xref{exec/numerics}{op-fge}{\F{fge}}
+.. |fpmin| mathdef:: \xref{exec/numerics}{op-fpmin}{\F{fpmin}}
+.. |fpmax| mathdef:: \xref{exec/numerics}{op-fpmax}{\F{fpmax}}
+
+.. |extend| mathdef:: \xref{exec/numerics}{op-extend_u}{\F{extend}}
+.. |extendu| mathdef:: \xref{exec/numerics}{op-extend_u}{\F{extend}^{\K{u}}}
+.. |extends| mathdef:: \xref{exec/numerics}{op-extend_s}{\F{extend}^{\K{s}}}
+.. |wrap| mathdef:: \xref{exec/numerics}{op-wrap}{\F{wrap}}
+.. |truncu| mathdef:: \xref{exec/numerics}{op-trunc_u}{\F{trunc}^{\K{u}}}
+.. |truncs| mathdef:: \xref{exec/numerics}{op-trunc_s}{\F{trunc}^{\K{s}}}
+.. |truncsatu| mathdef:: \xref{exec/numerics}{op-trunc_sat_u}{\F{trunc\_sat\_u}}
+.. |truncsats| mathdef:: \xref{exec/numerics}{op-trunc_sat_s}{\F{trunc\_sat\_s}}
+.. |promote| mathdef:: \xref{exec/numerics}{op-promote}{\F{promote}}
+.. |demote| mathdef:: \xref{exec/numerics}{op-demote}{\F{demote}}
+.. |convertu| mathdef:: \xref{exec/numerics}{op-convert_u}{\F{convert}^{\K{u}}}
+.. |converts| mathdef:: \xref{exec/numerics}{op-convert_s}{\F{convert}^{\K{s}}}
+.. |reinterpret| mathdef:: \xref{exec/numerics}{op-reinterpret}{\F{reinterpret}}
+.. |narrow| mathdef:: \xref{exec/numerics}{op-narrow_u}{\F{narrow}}
+.. |narrowu| mathdef:: \xref{exec/numerics}{op-narrow_u}{\F{narrow}^{\K{u}}}
+.. |narrows| mathdef:: \xref{exec/numerics}{op-narrow_s}{\F{narrow}^{\K{s}}}
+
+
+.. Numerics, meta functions
+
+.. |bits| mathdef:: \xref{exec/numerics}{aux-bits}{\F{bits}}
+.. |ibits| mathdef:: \xref{exec/numerics}{aux-ibits}{\F{ibits}}
+.. |fbits| mathdef:: \xref{exec/numerics}{aux-fbits}{\F{fbits}}
+.. |fsign| mathdef:: \xref{exec/numerics}{aux-fsign}{\F{fsign}}
+.. |fbias| mathdef:: \xref{exec/numerics}{aux-fbias}{\F{fbias}}
+.. |bytes| mathdef:: \xref{exec/numerics}{aux-bytes}{\F{bytes}}
+.. |littleendian| mathdef:: \xref{exec/numerics}{aux-littleendian}{\F{littleendian}}
+.. |signed| mathdef:: \xref{exec/numerics}{aux-signed}{\F{signed}}
+.. |bool| mathdef:: \xref{exec/numerics}{aux-bool}{\F{bool}}
+
+.. |ieee| mathdef:: \xref{exec/numerics}{aux-ieee}{\F{float}}
+.. |nans| mathdef:: \xref{exec/numerics}{aux-nans}{\F{nans}}
+.. |trunc| mathdef:: \xref{exec/numerics}{aux-trunc}{\F{trunc}}
+.. |satu| mathdef:: \xref{exec/numerics}{aux-sat_u}{\F{sat\_u}}
+.. |sats| mathdef:: \xref{exec/numerics}{aux-sat_s}{\F{sat\_s}}
+
+.. |lanes| mathdef:: \xref{exec/numerics}{aux-lanes}{\F{lanes}}
+
+
+.. Other meta functions
+
+.. |instantiate| mathdef:: \xref{exec/modules}{exec-instantiation}{\F{instantiate}}
+.. |invoke| mathdef:: \xref{exec/modules}{exec-invocation}{\F{invoke}}
+
+
+.. Judgements
+
+.. |vdashexternval| mathdef:: \xref{exec/modules}{valid-externval}{\vdash}
+
+.. |vdashlimitsmatch| mathdef:: \xref{valid/types}{match-limits}{\vdash}
+.. |vdashexterntypematch| mathdef:: \xref{valid/types}{match-externtype}{\vdash}
+
+
+.. Soundness
+.. ---------
+
+.. Judgements
+
+.. |vdashadmininstr| mathdef:: \xref{appendix/properties}{valid-instr-admin}{\vdash}
+
+.. |vdashval| mathdef:: \xref{exec/modules}{valid-val}{\vdash}
+.. |vdashresult| mathdef:: \xref{appendix/properties}{valid-result}{\vdash}
+
+.. |vdashfuncinst| mathdef:: \xref{appendix/properties}{valid-funcinst}{\vdash}
+.. |vdashtableinst| mathdef:: \xref{appendix/properties}{valid-tableinst}{\vdash}
+.. |vdashmeminst| mathdef:: \xref{appendix/properties}{valid-meminst}{\vdash}
+.. |vdashglobalinst| mathdef:: \xref{appendix/properties}{valid-globalinst}{\vdash}
+.. |vdasheleminst| mathdef:: \xref{appendix/properties}{valid-eleminst}{\vdash}
+.. |vdashdatainst| mathdef:: \xref{appendix/properties}{valid-datainst}{\vdash}
+.. |vdashexportinst| mathdef:: \xref{appendix/properties}{valid-exportinst}{\vdash}
+.. |vdashmoduleinst| mathdef:: \xref{appendix/properties}{valid-moduleinst}{\vdash}
+
+.. |vdashstore| mathdef:: \xref{appendix/properties}{valid-store}{\vdash}
+.. |vdashconfig| mathdef:: \xref{appendix/properties}{valid-config}{\vdash}
+.. |vdashthread| mathdef:: \xref{appendix/properties}{valid-thread}{\vdash}
+.. |vdashframe| mathdef:: \xref{appendix/properties}{valid-frame}{\vdash}
+
+.. |vdashfuncinstextends| mathdef:: \xref{appendix/properties}{extend-funcinst}{\vdash}
+.. |vdashtableinstextends| mathdef:: \xref{appendix/properties}{extend-tableinst}{\vdash}
+.. |vdashmeminstextends| mathdef:: \xref{appendix/properties}{extend-meminst}{\vdash}
+.. |vdashglobalinstextends| mathdef:: \xref{appendix/properties}{extend-globalinst}{\vdash}
+.. |vdasheleminstextends| mathdef:: \xref{appendix/properties}{extend-eleminst}{\vdash}
+.. |vdashdatainstextends| mathdef:: \xref{appendix/properties}{extend-datainst}{\vdash}
+.. |vdashstoreextends| mathdef:: \xref{appendix/properties}{extend-store}{\vdash}
+
+
+.. Custom Sections
+.. ---------------
+
+.. Name section, non-terminals
+
+.. |Bnamesec| mathdef:: \xref{appendix/custom}{binary-namesubsection}{\B{namesec}}
+.. |Bnamedata| mathdef:: \xref{appendix/custom}{binary-namesubsection}{\B{namedata}}
+.. |Bnamesubsection| mathdef:: \xref{appendix/custom}{binary-namesubsection}{\B{namesubsection}}
+
+.. |Bnamemap| mathdef:: \xref{appendix/custom}{binary-namemap}{\B{namemap}}
+.. |Bnameassoc| mathdef:: \xref{appendix/custom}{binary-namemap}{\B{nameassoc}}
+.. |Bindirectnamemap| mathdef:: \xref{appendix/custom}{binary-indirectnamemap}{\B{indirectnamemap}}
+.. |Bindirectnameassoc| mathdef:: \xref{appendix/custom}{binary-indirectnamemap}{\B{indirectnameassoc}}
+
+.. |Bmodulenamesubsec| mathdef:: \xref{appendix/custom}{binary-modulenamesec}{\B{modulenamesubsec}}
+.. |Bfuncnamesubsec| mathdef:: \xref{appendix/custom}{binary-funcnamesec}{\B{funcnamesubsec}}
+.. |Blocalnamesubsec| mathdef:: \xref{appendix/custom}{binary-localnamesec}{\B{localnamesubsec}}
+
+
+.. Embedding
+.. ---------
+
+.. |error| mathdef:: \xref{appendix/embedding}{embed-error}{\X{error}}
+.. |ERROR| mathdef:: \xref{appendix/embedding}{embed-error}{\K{error}}
\ No newline at end of file