Integers
All integers are encoded using the LEB128 variable-length integer encoding, in either unsigned or signed variant.
Unsigned integers are encoded in unsigned LEB128 format.
As an additional constraint, the total number of bytes encoding a value of type \(\href{../syntax/values.html#syntax-int}{\mathit{u}N}\) must not exceed \(\mathrm{ceil}(N/7)\) bytes.
\[\begin{split}\begin{array}{llclll@{\qquad}l}
\def\mathdef1092#1{{}}\mathdef1092{unsigned integer} & \href{../binary/values.html#binary-int}{\def\mathdef1093#1{{\mathtt{u}#1}}\mathdef1093{N}} &::=&
n{:}\href{../binary/values.html#binary-byte}{\mathtt{byte}} &\Rightarrow& n & (\mathrel{\mbox{if}} n < 2^7 \wedge n < 2^N) \\ &&|&
n{:}\href{../binary/values.html#binary-byte}{\mathtt{byte}}~~m{:}\def\mathdef1133#1{{\mathtt{u}#1}}\mathdef1133{(N\mathtt{-7})} &\Rightarrow&
2^7\cdot m + (n-2^7) & (\mathrel{\mbox{if}} n \geq 2^7 \wedge N > 7) \\
\end{array}\end{split}\]
Signed integers are encoded in signed LEB128 format, which uses a two’s complement representation.
As an additional constraint, the total number of bytes encoding a value of type \(\href{../syntax/values.html#syntax-int}{\mathit{s}N}\) must not exceed \(\mathrm{ceil}(N/7)\) bytes.
\[\begin{split}\begin{array}{llclll@{\qquad}l}
\def\mathdef1092#1{{}}\mathdef1092{signed integer} & \href{../binary/values.html#binary-int}{\def\mathdef1099#1{{\mathtt{s}#1}}\mathdef1099{N}} &::=&
n{:}\href{../binary/values.html#binary-byte}{\mathtt{byte}} &\Rightarrow& n & (\mathrel{\mbox{if}} n < 2^6 \wedge n < 2^{N-1}) \\ &&|&
n{:}\href{../binary/values.html#binary-byte}{\mathtt{byte}} &\Rightarrow& n-2^7 & (\mathrel{\mbox{if}} 2^6 \leq n < 2^7 \wedge n \geq 2^7-2^{N-1}) \\ &&|&
n{:}\href{../binary/values.html#binary-byte}{\mathtt{byte}}~~m{:}\def\mathdef1134#1{{\mathtt{s}#1}}\mathdef1134{(N\mathtt{-7})} &\Rightarrow&
2^7\cdot m + (n-2^7) & (\mathrel{\mbox{if}} n \geq 2^7 \wedge N > 7) \\
\end{array}\end{split}\]
Uninterpreted integers are encoded as signed integers.
\[\begin{array}{llclll@{\qquad\qquad}l}
\def\mathdef1092#1{{}}\mathdef1092{uninterpreted integer} & \href{../binary/values.html#binary-int}{\def\mathdef1104#1{{\mathtt{i}#1}}\mathdef1104{N}} &::=&
n{:}\href{../binary/values.html#binary-int}{\def\mathdef1099#1{{\mathtt{s}#1}}\mathdef1099{N}} &\Rightarrow& i & (\mathrel{\mbox{if}} n = \href{../exec/numerics.html#aux-signed}{\mathrm{signed}}_{\href{../syntax/values.html#syntax-int}{\mathit{i}N}}(i))
\end{array}\]
Note
The side conditions \(N > 7\) in the productions for non-terminal bytes of the \(\def\mathdef1135#1{{\mathit{u#1}}}\mathdef1135{}\) and \(\def\mathdef1136#1{{\mathit{s#1}}}\mathdef1136{}\) encodings restrict the encoding’s length.
However, “trailing zeros” are still allowed within these bounds.
For example, \(\def\mathdef1137#1{\mathtt{0x#1}}\mathdef1137{03}\) and \(\def\mathdef1138#1{\mathtt{0x#1}}\mathdef1138{83}~\def\mathdef1139#1{\mathtt{0x#1}}\mathdef1139{00}\) are both well-formed encodings for the value \(3\) as a \(\href{../syntax/values.html#syntax-int}{\mathit{u8}}\).
Similarly, either of \(\def\mathdef1140#1{\mathtt{0x#1}}\mathdef1140{7e}\) and \(\def\mathdef1141#1{\mathtt{0x#1}}\mathdef1141{FE}~\def\mathdef1142#1{\mathtt{0x#1}}\mathdef1142{7F}\) and \(\def\mathdef1143#1{\mathtt{0x#1}}\mathdef1143{FE}~\def\mathdef1144#1{\mathtt{0x#1}}\mathdef1144{FF}~\def\mathdef1145#1{\mathtt{0x#1}}\mathdef1145{7F}\) are well-formed encodings of the value \(-2\) as a \(\href{../syntax/values.html#syntax-int}{\mathit{s16}}\).
The side conditions on the value \(n\) of terminal bytes further enforce that
any unused bits in these bytes must be \(0\) for positive values and \(1\) for negative ones.
For example, \(\def\mathdef1146#1{\mathtt{0x#1}}\mathdef1146{83}~\def\mathdef1147#1{\mathtt{0x#1}}\mathdef1147{10}\) is malformed as a \(\href{../syntax/values.html#syntax-int}{\mathit{u8}}\) encoding.
Similarly, both \(\def\mathdef1148#1{\mathtt{0x#1}}\mathdef1148{83}~\def\mathdef1149#1{\mathtt{0x#1}}\mathdef1149{3E}\) and \(\def\mathdef1150#1{\mathtt{0x#1}}\mathdef1150{FF}~\def\mathdef1151#1{\mathtt{0x#1}}\mathdef1151{7B}\) are malformed as \(\href{../syntax/values.html#syntax-int}{\mathit{s8}}\) encodings.
Floating-Point
Floating-point values are encoded directly by their IEEE 754-2019 (Section 3.4) bit pattern in little endian byte order:
\[\begin{split}\begin{array}{llclll@{\qquad\qquad}l}
\def\mathdef1092#1{{}}\mathdef1092{floating-point value} & \href{../binary/values.html#binary-float}{\def\mathdef1107#1{{\mathtt{f}#1}}\mathdef1107{N}} &::=&
b^\ast{:\,}\href{../binary/values.html#binary-byte}{\mathtt{byte}}^{N/8} &\Rightarrow& \href{../exec/numerics.html#aux-bytes}{\mathrm{bytes}}_{\href{../syntax/values.html#syntax-float}{\mathit{f}N}}^{-1}(b^\ast) \\
\end{array}\end{split}\]
Names
Names are encoded as a vector of bytes containing the Unicode (Section 3.9) UTF-8 encoding of the name’s character sequence.
\[\begin{split}\begin{array}{llclllll}
\def\mathdef1092#1{{}}\mathdef1092{name} & \href{../binary/values.html#binary-name}{\mathtt{name}} &::=&
b^\ast{:}\href{../binary/conventions.html#binary-vec}{\mathtt{vec}}(\href{../binary/values.html#binary-byte}{\mathtt{byte}}) &\Rightarrow& \href{../syntax/values.html#syntax-name}{\mathit{name}}
&& (\mathrel{\mbox{if}} \href{../binary/values.html#binary-utf8}{\mathrm{utf8}}(\href{../syntax/values.html#syntax-name}{\mathit{name}}) = b^\ast) \\
\end{array}\end{split}\]
The auxiliary \(\href{../binary/values.html#binary-utf8}{\mathrm{utf8}}\) function expressing this encoding is defined as follows:
\[\begin{split}\begin{array}{@{}l@{}}
\begin{array}{@{}lcl@{\qquad}l@{}}
\href{../binary/values.html#binary-utf8}{\mathrm{utf8}}(c^\ast) &=& (\href{../binary/values.html#binary-utf8}{\mathrm{utf8}}(c))^\ast \\[1ex]
\href{../binary/values.html#binary-utf8}{\mathrm{utf8}}(c) &=& b &
(\begin{array}[t]{@{}c@{~}l@{}}
\mathrel{\mbox{if}} & c < \def\mathdef1152#1{\mathrm{U{+}#1}}\mathdef1152{80} \\
\wedge & c = b) \\
\end{array} \\
\href{../binary/values.html#binary-utf8}{\mathrm{utf8}}(c) &=& b_1~b_2 &
(\begin{array}[t]{@{}c@{~}l@{}}
\mathrel{\mbox{if}} & \def\mathdef1153#1{\mathrm{U{+}#1}}\mathdef1153{80} \leq c < \def\mathdef1154#1{\mathrm{U{+}#1}}\mathdef1154{800} \\
\wedge & c = 2^6(b_1-\def\mathdef1155#1{\mathtt{0x#1}}\mathdef1155{C0})+(b_2-\def\mathdef1156#1{\mathtt{0x#1}}\mathdef1156{80})) \\
\end{array} \\
\href{../binary/values.html#binary-utf8}{\mathrm{utf8}}(c) &=& b_1~b_2~b_3 &
(\begin{array}[t]{@{}c@{~}l@{}}
\mathrel{\mbox{if}} & \def\mathdef1157#1{\mathrm{U{+}#1}}\mathdef1157{800} \leq c < \def\mathdef1158#1{\mathrm{U{+}#1}}\mathdef1158{D800} \vee \def\mathdef1159#1{\mathrm{U{+}#1}}\mathdef1159{E000} \leq c < \def\mathdef1160#1{\mathrm{U{+}#1}}\mathdef1160{10000} \\
\wedge & c = 2^{12}(b_1-\def\mathdef1161#1{\mathtt{0x#1}}\mathdef1161{E0})+2^6(b_2-\def\mathdef1162#1{\mathtt{0x#1}}\mathdef1162{80})+(b_3-\def\mathdef1163#1{\mathtt{0x#1}}\mathdef1163{80})) \\
\end{array} \\
\href{../binary/values.html#binary-utf8}{\mathrm{utf8}}(c) &=& b_1~b_2~b_3~b_4 &
(\begin{array}[t]{@{}c@{~}l@{}}
\mathrel{\mbox{if}} & \def\mathdef1164#1{\mathrm{U{+}#1}}\mathdef1164{10000} \leq c < \def\mathdef1165#1{\mathrm{U{+}#1}}\mathdef1165{110000} \\
\wedge & c = 2^{18}(b_1-\def\mathdef1166#1{\mathtt{0x#1}}\mathdef1166{F0})+2^{12}(b_2-\def\mathdef1167#1{\mathtt{0x#1}}\mathdef1167{80})+2^6(b_3-\def\mathdef1168#1{\mathtt{0x#1}}\mathdef1168{80})+(b_4-\def\mathdef1169#1{\mathtt{0x#1}}\mathdef1169{80})) \\
\end{array} \\
\end{array} \\
\mathrel{\mbox{where}} b_2, b_3, b_4 < \def\mathdef1170#1{\mathtt{0x#1}}\mathdef1170{C0} \\
\end{array}\end{split}\]
Note
Unlike in some other formats, name strings are not 0-terminated.
