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