document/core/util/macros.def

.. LINK MACROS

.. External Standards
.. ------------------

.. |WasmDraft| replace:: http://webassembly.github.io/spec/core/
.. _WasmDraft: http://webassembly.github.io/spec/core/

.. |WasmIssues| replace:: http://github.com/webassembly/spec/issues/
.. _WasmIssues: http://github.com/webassembly/spec/issues/

.. |IEEE754| replace:: IEEE 754-2019
.. _IEEE754: https://ieeexplore.ieee.org/document/8766229

.. |Unicode| replace:: Unicode
.. _Unicode: http://www.unicode.org/versions/latest/

.. |ASCII| replace:: ASCII
.. _ASCII: http://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

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

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

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

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

.. |I8| mathdef:: \xref{exec/runtime}{syntax-storagetype}{\K{i8}}
.. |I16| mathdef:: \xref{exec/runtime}{syntax-storagetype}{\K{i16}}
.. |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}}

.. |FUNCREF| mathdef:: \xref{syntax/types}{syntax-elemtype}{\K{funcref}}

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

.. |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}}
.. |elemtype| mathdef:: \xref{syntax/types}{syntax-elemtype}{\X{elemtype}}
.. |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}}


.. 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}}
.. |localidx| mathdef:: \xref{syntax/modules}{syntax-localidx}{\X{localidx}}
.. |labelidx| mathdef:: \xref{syntax/modules}{syntax-labelidx}{\X{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}}
.. |MDATA| mathdef:: \xref{syntax/modules}{syntax-module}{\K{data}}
.. |MELEM| mathdef:: \xref{syntax/modules}{syntax-module}{\K{elem}}
.. |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}}

.. |ETABLE| mathdef:: \xref{syntax/modules}{syntax-elem}{\K{table}}
.. |EOFFSET| mathdef:: \xref{syntax/modules}{syntax-elem}{\K{offset}}
.. |EINIT| mathdef:: \xref{syntax/modules}{syntax-elem}{\K{init}}

.. |DMEM| mathdef:: \xref{syntax/modules}{syntax-data}{\K{data}}
.. |DOFFSET| mathdef:: \xref{syntax/modules}{syntax-data}{\K{offset}}
.. |DINIT| mathdef:: \xref{syntax/modules}{syntax-data}{\K{init}}

.. |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/modules}{syntax-typedef}{\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}}
.. |data| mathdef:: \xref{syntax/modules}{syntax-data}{\X{data}}
.. |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}}

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

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


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

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

.. |sx| mathdef:: \xref{syntax/instructions}{syntax-sx}{\X{sx}}
.. |memarg| mathdef:: \xref{syntax/instructions}{syntax-memarg}{\X{memarg}}

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

.. |Bvaltype| mathdef:: \xref{binary/types}{binary-valtype}{\B{valtype}}
.. |Bresulttype| mathdef:: \xref{binary/types}{binary-resulttype}{\B{resulttype}}
.. |Bblocktype| mathdef:: \xref{binary/types}{binary-blocktype}{\B{blocktype}}
.. |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}}
.. |Belemtype| mathdef:: \xref{binary/types}{binary-elemtype}{\B{elemtype}}
.. |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}}
.. |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}}

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

.. |Binstr| mathdef:: \xref{binary/instructions}{binary-instr}{\B{instr}}
.. |Bexpr| mathdef:: \xref{binary/instructions}{binary-expr}{\B{expr}}



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

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

.. |Tvaltype| mathdef:: \xref{text/types}{text-valtype}{\T{valtype}}
.. |Tresulttype| mathdef:: \xref{text/types}{text-resulttype}{\T{resulttype}}
.. |Tblocktype| mathdef:: \xref{text/types}{text-blocktype}{\T{blocktype}}
.. |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}}
.. |Telemtype| mathdef:: \xref{text/types}{text-elemtype}{\T{elemtype}}
.. |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}}
.. |Tlocalidx| mathdef:: \xref{text/modules}{text-localidx}{\T{localidx}}
.. |Tlabelidx| mathdef:: \xref{text/modules}{text-labelidx}{\T{labelidx}}

.. |Ttypebind| mathdef:: \xref{text/modules}{text-typebind}{\T{typebind}}
.. |Tfuncbind| mathdef:: \xref{text/modules}{text-funcbind}{\T{funcbind}}
.. |Ttablebind| mathdef:: \xref{text/modules}{text-tablebind}{\T{tablebind}}
.. |Tmembind| mathdef:: \xref{text/modules}{text-membind}{\T{membind}}
.. |Tglobalbind| mathdef:: \xref{text/modules}{text-globalbind}{\T{globalbind}}
.. |Tlocalbind| mathdef:: \xref{text/modules}{text-localbind}{\T{localbind}}
.. |Tlabelbind| mathdef:: \xref{text/modules}{text-labelbind}{\T{labelbind}}


.. Modules, non-terminals

.. |Tmodule| mathdef:: \xref{text/modules}{text-module}{\T{module}}
.. |Tmodulebody| mathdef:: \xref{text/modules}{text-modulebody}{\T{modulebody}}
.. |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}}
.. |Tcode| mathdef:: \xref{text/modules}{text-code}{\T{code}}
.. |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}}
.. |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}}

.. |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}}
.. |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}}
.. |CLOCALS| mathdef:: \xref{valid/conventions}{context}{\K{locals}}
.. |CLABELS| mathdef:: \xref{valid/conventions}{context}{\K{labels}}
.. |CRETURN| mathdef:: \xref{valid/conventions}{context}{\K{return}}


.. Judgments

.. |vdashlimits| mathdef:: \xref{valid/types}{valid-limits}{\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}
.. |vdashdata| mathdef:: \xref{valid/modules}{valid-data}{\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}


.. Execution
.. ---------

.. Notation

.. |stepto| mathdef:: \xref{exec/conventions}{formal-notation}{\hookrightarrow}
.. |extendsto| mathdef:: \xref{appendix/properties}{extend}{\preceq}
.. |matches| mathdef:: \xref{exec/modules}{match}{\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}}
.. |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}}


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

.. |TIELEM| mathdef:: \xref{exec/runtime}{syntax-tableinst}{\K{elem}}
.. |TIMAX| mathdef:: \xref{exec/runtime}{syntax-tableinst}{\K{max}}

.. |MIDATA| mathdef:: \xref{exec/runtime}{syntax-meminst}{\K{data}}
.. |MIMAX| mathdef:: \xref{exec/runtime}{syntax-meminst}{\K{max}}

.. |GIVALUE| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\K{value}}
.. |GIMUT| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\K{mut}}

.. |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}}
.. |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}}
.. |funcelem| mathdef:: \xref{exec/runtime}{syntax-funcelem}{\X{funcelem}}
.. |meminst| mathdef:: \xref{exec/runtime}{syntax-meminst}{\X{meminst}}
.. |globalinst| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\X{globalinst}}
.. |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}}


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


.. Administrative Instructions, terminals

.. |TRAP| mathdef:: \xref{exec/runtime}{syntax-trap}{\K{trap}}
.. |INVOKE| mathdef:: \xref{exec/runtime}{syntax-invoke}{\K{invoke}}
.. |INITELEM| mathdef:: \xref{exec/runtime}{syntax-init_elem}{\K{init\_elem}}
.. |INITDATA| mathdef:: \xref{exec/runtime}{syntax-init_data}{\K{init\_data}}


.. Values & Results, non-terminals

.. |val| mathdef:: \xref{exec/runtime}{syntax-val}{\X{val}}
.. |result| mathdef:: \xref{exec/runtime}{syntax-result}{\X{result}}


.. 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}}
.. |iand| mathdef:: \xref{exec/numerics}{op-iand}{\F{iand}}
.. |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}}

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

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


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


.. 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{exec/modules}{match-limits}{\vdash}
.. |vdashexterntypematch| mathdef:: \xref{exec/modules}{match-externtype}{\vdash}


.. Soundness
.. ---------

.. Judgements

.. |vdashadmininstr| mathdef:: \xref{appendix/properties}{valid-instr-admin}{\vdash}

.. |vdashval| mathdef:: \xref{appendix/properties}{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}
.. |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}
.. |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}}