diff --git a/document/core/binary/instructions.rst b/document/core/binary/instructions.rst index 151e7e591e..0e3840cfca 100644 --- a/document/core/binary/instructions.rst +++ b/document/core/binary/instructions.rst @@ -510,7 +510,7 @@ The |VCONST| instruction is followed by 16 immediate bytes, which are converted \begin{array}{llclll} \production{instruction} & \Binstr &::=& \dots \\&&|& \hex{FD}~~12{:}\Bu32~~(b{:}\Bbyte)^{16} &\Rightarrow& \V128.\VCONST~ - bytes_{\K{i128}}^{-1}(b_{0}~\dots~b_{15}) \\ + \bytes_{\K{i128}}^{-1}(b_{0}~\dots~b_{15}) \\ \end{array} .. _binary-vternop: diff --git a/document/core/binary/modules.rst b/document/core/binary/modules.rst index 818c19e767..f20bd0749c 100644 --- a/document/core/binary/modules.rst +++ b/document/core/binary/modules.rst @@ -325,7 +325,7 @@ It decodes into a vector of :ref:`element segments ` that represent .. math:: \begin{array}{llclll} \production{element section} & \Belemsec &::=& - \X{seg}^\ast{:}\Bsection_9(\Bvec(\Belem)) &\Rightarrow& \X{seg} \\ + \X{seg}^\ast{:}\Bsection_9(\Bvec(\Belem)) &\Rightarrow& \X{seg}^\ast \\ \production{element segment} & \Belem &::=& 0{:}\Bu32~~e{:}\Bexpr~~y^\ast{:}\Bvec(\Bfuncidx) &\Rightarrow& \\&&&\quad @@ -406,7 +406,7 @@ denoting *count* locals of the same value type. &\Rightarrow& \X{code} & (\iff \X{size} = ||\Bfunc||) \\ \production{function} & \Bfunc &::=& (t^\ast)^\ast{:}\Bvec(\Blocals)~~e{:}\Bexpr - &\Rightarrow& \concat((t^\ast)^\ast), e^\ast + &\Rightarrow& \concat((t^\ast)^\ast), e & (\iff |\concat((t^\ast)^\ast)| < 2^{32}) \\ \production{locals} & \Blocals &::=& n{:}\Bu32~~t{:}\Bvaltype &\Rightarrow& t^n \\ @@ -438,7 +438,7 @@ It decodes into a vector of :ref:`data segments ` that represent th .. math:: \begin{array}{llclll} \production{data section} & \Bdatasec &::=& - \X{seg}^\ast{:}\Bsection_{11}(\Bvec(\Bdata)) &\Rightarrow& \X{seg} \\ + \X{seg}^\ast{:}\Bsection_{11}(\Bvec(\Bdata)) &\Rightarrow& \X{seg}^\ast \\ \production{data segment} & \Bdata &::=& 0{:}\Bu32~~e{:}\Bexpr~~b^\ast{:}\Bvec(\Bbyte) &\Rightarrow& \{ \DINIT~b^\ast, \DMODE~\DACTIVE~\{ \DMEM~0, \DOFFSET~e \} \} \\ &&|& @@ -504,7 +504,7 @@ All sections can be empty. The lengths of vectors produced by the (possibly empty) :ref:`function ` and :ref:`code ` section must match up. Similarly, the optional data count must match the length of the :ref:`data segment ` vector. -Furthermore, it must be present if any :math:`data index ` occurs in the code section. +Furthermore, it must be present if any :ref:`data index ` occurs in the code section. .. math:: \begin{array}{llcllll} diff --git a/document/core/binary/types.rst b/document/core/binary/types.rst index 4850573544..4df6618393 100644 --- a/document/core/binary/types.rst +++ b/document/core/binary/types.rst @@ -91,7 +91,7 @@ Value Types Result Types ~~~~~~~~~~~~ -:ref:`Result types ` are encoded by the respective :ref:`vectors ` of :ref:`value types ``. +:ref:`Result types ` are encoded by the respective :ref:`vectors ` of :ref:`value types `. .. math:: \begin{array}{llclll@{\qquad\qquad}l} diff --git a/document/core/binary/values.rst b/document/core/binary/values.rst index c626862489..93699749bc 100644 --- a/document/core/binary/values.rst +++ b/document/core/binary/values.rst @@ -66,7 +66,7 @@ As an additional constraint, the total number of bytes encoding a value of type .. math:: \begin{array}{llclll@{\qquad\qquad}l} \production{uninterpreted integer} & \BiN &::=& - n{:}\BsN &\Rightarrow& i & (\iff n = \signed_{\iN}(i)) + n{:}\BsN &\Rightarrow& i & (\iff n = \signed_N(i)) \end{array} .. note:: diff --git a/document/core/text/instructions.rst b/document/core/text/instructions.rst index ea3b683f26..1081b608c7 100644 --- a/document/core/text/instructions.rst +++ b/document/core/text/instructions.rst @@ -239,17 +239,17 @@ Table Instructions Abbreviations ............. -For backwards compatibility, all :math:`table indices ` may be omitted from table instructions, defaulting to :math:`0`. +For backwards compatibility, all :ref:`table indices ` may be omitted from table instructions, defaulting to :math:`0`. .. math:: - \begin{array}{llclll} + \begin{array}{llcl} \production{instruction} & - \text{table.get} &\equiv& \text{table.get}~~\text{0} \\ &&|& - \text{table.set} &\equiv& \text{table.set}~~\text{0} \\ &&|& - \text{table.size} &\equiv& \text{table.size}~~\text{0} \\ &&|& - \text{table.grow} &\equiv& \text{table.grow}~~\text{0} \\ &&|& - \text{table.fill} &\equiv& \text{table.fill}~~\text{0} \\ &&|& - \text{table.copy} &\equiv& \text{table.copy}~~\text{0}~~\text{0} \\ &&|& + \text{table.get} &\equiv& \text{table.get}~~\text{0} \\ & + \text{table.set} &\equiv& \text{table.set}~~\text{0} \\ & + \text{table.size} &\equiv& \text{table.size}~~\text{0} \\ & + \text{table.grow} &\equiv& \text{table.grow}~~\text{0} \\ & + \text{table.fill} &\equiv& \text{table.fill}~~\text{0} \\ & + \text{table.copy} &\equiv& \text{table.copy}~~\text{0}~~\text{0} \\ & \text{table.init}~~x{:}\Telemidx_I &\equiv& \text{table.init}~~\text{0}~~x{:}\Telemidx_I \\ \end{array} @@ -968,7 +968,7 @@ Such a folded instruction can appear anywhere a regular instruction can. \text{(}~\text{loop}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~\text{)} &\equiv\quad \text{loop}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~~\text{end} \\ & \text{(}~\text{if}~~\Tlabel~~\Tblocktype~~\Tfoldedinstr^\ast - &\hspace{-3ex} \text{(}~\text{then}~~\Tinstr_1^\ast~\text{)}~~\text{(}~\text{else}~~\Tinstr_2^\ast~\text{)}^?~~\text{)} + &\hspace{-3ex} \text{(}~\text{then}~~\Tinstr_1^\ast~\text{)}~~(\text{(}~\text{else}~~\Tinstr_2^\ast~\text{)})^?~~\text{)} \quad\equiv \\ &\qquad \Tfoldedinstr^\ast~~\text{if}~~\Tlabel~~\Tblocktype &\hspace{-1ex} \Tinstr_1^\ast~~\text{else}~~(\Tinstr_2^\ast)^?~\text{end} \\ \end{array}