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}{\def\mathdef1229#1{{\mathit{u}#1}}\mathdef1229{N}} must not exceed \mathrm{ceil}(N/7) bytes.
\begin{split}\begin{array}{llclll@{\qquad}l}
\def\mathdef1228#1{{}}\mathdef1228{unsigned integer} & \href{../binary/values.html#binary-int}{\def\mathdef1250#1{{\mathtt{u}#1}}\mathdef1250{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\mathdef1289#1{{\mathtt{u}#1}}\mathdef1289{(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}{\def\mathdef1236#1{{\mathit{s}#1}}\mathdef1236{N}} must not exceed \mathrm{ceil}(N/7) bytes.
\begin{split}\begin{array}{llclll@{\qquad}l}
\def\mathdef1228#1{{}}\mathdef1228{signed integer} & \href{../binary/values.html#binary-int}{\def\mathdef1256#1{{\mathtt{s}#1}}\mathdef1256{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\mathdef1290#1{{\mathtt{s}#1}}\mathdef1290{(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\mathdef1228#1{{}}\mathdef1228{uninterpreted integer} & \href{../binary/values.html#binary-int}{\def\mathdef1260#1{{\mathtt{i}#1}}\mathdef1260{N}} &::=&
n{:}\href{../binary/values.html#binary-int}{\def\mathdef1256#1{{\mathtt{s}#1}}\mathdef1256{N}} &\Rightarrow& i & (\mathrel{\mbox{if}} n = \href{../exec/numerics.html#aux-signed}{\mathrm{signed}}_{\href{../syntax/values.html#syntax-int}{\def\mathdef1241#1{{\mathit{i}#1}}\mathdef1241{N}}}(i))
\end{array}
Note
The side conditions N > 7 in the productions for non-terminal bytes of the \def\mathdef1291#1{{\mathit{u}#1}}\mathdef1291{} and \def\mathdef1292#1{{\mathit{s}#1}}\mathdef1292{} encodings restrict the encoding’s length.
However, “trailing zeros” are still allowed within these bounds.
For example, \def\mathdef1293#1{\mathtt{0x#1}}\mathdef1293{03} and \def\mathdef1294#1{\mathtt{0x#1}}\mathdef1294{83}~\def\mathdef1295#1{\mathtt{0x#1}}\mathdef1295{00} are both well-formed encodings for the value 3 as a \href{../syntax/values.html#syntax-int}{\def\mathdef1232#1{{\mathit{u}#1}}\mathdef1232{\mathit{8}}}.
Similarly, either of \def\mathdef1296#1{\mathtt{0x#1}}\mathdef1296{7e} and \def\mathdef1297#1{\mathtt{0x#1}}\mathdef1297{FE}~\def\mathdef1298#1{\mathtt{0x#1}}\mathdef1298{7F} and \def\mathdef1299#1{\mathtt{0x#1}}\mathdef1299{FE}~\def\mathdef1300#1{\mathtt{0x#1}}\mathdef1300{FF}~\def\mathdef1301#1{\mathtt{0x#1}}\mathdef1301{7F} are well-formed encodings of the value -2 as a \href{../syntax/values.html#syntax-int}{\def\mathdef1238#1{{\mathit{s}#1}}\mathdef1238{\mathit{16}}}.
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\mathdef1302#1{\mathtt{0x#1}}\mathdef1302{83}~\def\mathdef1303#1{\mathtt{0x#1}}\mathdef1303{10} is malformed as a \href{../syntax/values.html#syntax-int}{\def\mathdef1232#1{{\mathit{u}#1}}\mathdef1232{\mathit{8}}} encoding.
Similarly, both \def\mathdef1304#1{\mathtt{0x#1}}\mathdef1304{83}~\def\mathdef1305#1{\mathtt{0x#1}}\mathdef1305{3E} and \def\mathdef1306#1{\mathtt{0x#1}}\mathdef1306{FF}~\def\mathdef1307#1{\mathtt{0x#1}}\mathdef1307{7B} are malformed as \href{../syntax/values.html#syntax-int}{\def\mathdef1237#1{{\mathit{s}#1}}\mathdef1237{\mathit{8}}} encodings.
Floating-Point
Floating-point values are encoded directly by their IEEE 754-2008 bit pattern in little endian byte order:
\begin{split}\begin{array}{llclll@{\qquad\qquad}l}
\def\mathdef1228#1{{}}\mathdef1228{floating-point value} & \href{../binary/values.html#binary-float}{\def\mathdef1263#1{{\mathtt{f}#1}}\mathdef1263{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}{\def\mathdef1246#1{{\mathit{f}#1}}\mathdef1246{N}}}^{-1}(b^\ast) \\
\end{array}\end{split}
Names
Names are encoded as a vector of bytes containing the Unicode UTF-8 encoding of the name’s code point sequence.
\begin{split}\begin{array}{llclllll}
\def\mathdef1228#1{{}}\mathdef1228{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}{@{}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\mathdef1308#1{\mathrm{U{+}#1}}\mathdef1308{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\mathdef1309#1{\mathrm{U{+}#1}}\mathdef1309{80} \leq c < \def\mathdef1310#1{\mathrm{U{+}#1}}\mathdef1310{800} \\
\wedge & c = 2^6(b_1-\def\mathdef1311#1{\mathtt{0x#1}}\mathdef1311{C0})+(b_2-\def\mathdef1312#1{\mathtt{0x#1}}\mathdef1312{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\mathdef1313#1{\mathrm{U{+}#1}}\mathdef1313{800} \leq c < \def\mathdef1314#1{\mathrm{U{+}#1}}\mathdef1314{10000} \\
\wedge & c = 2^{12}(b_1-\def\mathdef1315#1{\mathtt{0x#1}}\mathdef1315{C0})+2^6(b_2-\def\mathdef1316#1{\mathtt{0x#1}}\mathdef1316{80})+(b_3-\def\mathdef1317#1{\mathtt{0x#1}}\mathdef1317{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\mathdef1318#1{\mathrm{U{+}#1}}\mathdef1318{10000} \leq c < \def\mathdef1319#1{\mathrm{U{+}#1}}\mathdef1319{110000} \\
\wedge & c = 2^{18}(b_1-\def\mathdef1320#1{\mathtt{0x#1}}\mathdef1320{C0})+2^{12}(b_2-\def\mathdef1321#1{\mathtt{0x#1}}\mathdef1321{80})+2^6(b_3-\def\mathdef1322#1{\mathtt{0x#1}}\mathdef1322{80})+(b_4-\def\mathdef1323#1{\mathtt{0x#1}}\mathdef1323{80})) \\
\end{array} \\
\end{array}\end{split}
