# 5.2 Values¶

## 5.2.1 Bytes¶

Bytes encode themselves.

$\begin{split}\begin{array}{llcll@{\qquad}l} \def\mathdef1869#1{{}}\mathdef1869{byte} & \href{../binary/values.html#binary-byte}{\mathtt{byte}} &::=& \def\mathdef1908#1{\mathtt{0x#1}}\mathdef1908{00} &\Rightarrow& \def\mathdef1909#1{\mathtt{0x#1}}\mathdef1909{00} \\ &&|&& \dots \\ &&|& \def\mathdef1910#1{\mathtt{0x#1}}\mathdef1910{FF} &\Rightarrow& \def\mathdef1911#1{\mathtt{0x#1}}\mathdef1911{FF} \\ \end{array}\end{split}$

## 5.2.2 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\mathdef1869#1{{}}\mathdef1869{unsigned integer} & \href{../binary/values.html#binary-int}{\def\mathdef1870#1{{\mathtt{u}#1}}\mathdef1870{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\mathdef1912#1{{\mathtt{u}#1}}\mathdef1912{(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\mathdef1869#1{{}}\mathdef1869{signed integer} & \href{../binary/values.html#binary-int}{\def\mathdef1876#1{{\mathtt{s}#1}}\mathdef1876{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\mathdef1913#1{{\mathtt{s}#1}}\mathdef1913{(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\mathdef1869#1{{}}\mathdef1869{uninterpreted integer} & \href{../binary/values.html#binary-int}{\def\mathdef1881#1{{\mathtt{i}#1}}\mathdef1881{N}} &::=& n{:}\href{../binary/values.html#binary-int}{\def\mathdef1876#1{{\mathtt{s}#1}}\mathdef1876{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\mathdef1914#1{{\mathit{u#1}}}\mathdef1914{}$$ and $$\def\mathdef1915#1{{\mathit{s#1}}}\mathdef1915{}$$ encodings restrict the encoding’s length. However, “trailing zeros” are still allowed within these bounds. For example, $$\def\mathdef1916#1{\mathtt{0x#1}}\mathdef1916{03}$$ and $$\def\mathdef1917#1{\mathtt{0x#1}}\mathdef1917{83}~\def\mathdef1918#1{\mathtt{0x#1}}\mathdef1918{00}$$ are both well-formed encodings for the value $$3$$ as a $$\href{../syntax/values.html#syntax-int}{\mathit{u8}}$$. Similarly, either of $$\def\mathdef1919#1{\mathtt{0x#1}}\mathdef1919{7e}$$ and $$\def\mathdef1920#1{\mathtt{0x#1}}\mathdef1920{FE}~\def\mathdef1921#1{\mathtt{0x#1}}\mathdef1921{7F}$$ and $$\def\mathdef1922#1{\mathtt{0x#1}}\mathdef1922{FE}~\def\mathdef1923#1{\mathtt{0x#1}}\mathdef1923{FF}~\def\mathdef1924#1{\mathtt{0x#1}}\mathdef1924{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\mathdef1925#1{\mathtt{0x#1}}\mathdef1925{83}~\def\mathdef1926#1{\mathtt{0x#1}}\mathdef1926{10}$$ is malformed as a $$\href{../syntax/values.html#syntax-int}{\mathit{u8}}$$ encoding. Similarly, both $$\def\mathdef1927#1{\mathtt{0x#1}}\mathdef1927{83}~\def\mathdef1928#1{\mathtt{0x#1}}\mathdef1928{3E}$$ and $$\def\mathdef1929#1{\mathtt{0x#1}}\mathdef1929{FF}~\def\mathdef1930#1{\mathtt{0x#1}}\mathdef1930{7B}$$ are malformed as $$\href{../syntax/values.html#syntax-int}{\mathit{s8}}$$ encodings.

## 5.2.3 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\mathdef1869#1{{}}\mathdef1869{floating-point value} & \href{../binary/values.html#binary-float}{\def\mathdef1884#1{{\mathtt{f}#1}}\mathdef1884{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}$

## 5.2.4 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\mathdef1869#1{{}}\mathdef1869{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\mathdef1931#1{\mathrm{U{+}#1}}\mathdef1931{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\mathdef1932#1{\mathrm{U{+}#1}}\mathdef1932{80} \leq c < \def\mathdef1933#1{\mathrm{U{+}#1}}\mathdef1933{800} \\ \wedge & c = 2^6(b_1-\def\mathdef1934#1{\mathtt{0x#1}}\mathdef1934{C0})+(b_2-\def\mathdef1935#1{\mathtt{0x#1}}\mathdef1935{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\mathdef1936#1{\mathrm{U{+}#1}}\mathdef1936{800} \leq c < \def\mathdef1937#1{\mathrm{U{+}#1}}\mathdef1937{D800} \vee \def\mathdef1938#1{\mathrm{U{+}#1}}\mathdef1938{E000} \leq c < \def\mathdef1939#1{\mathrm{U{+}#1}}\mathdef1939{10000} \\ \wedge & c = 2^{12}(b_1-\def\mathdef1940#1{\mathtt{0x#1}}\mathdef1940{E0})+2^6(b_2-\def\mathdef1941#1{\mathtt{0x#1}}\mathdef1941{80})+(b_3-\def\mathdef1942#1{\mathtt{0x#1}}\mathdef1942{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\mathdef1943#1{\mathrm{U{+}#1}}\mathdef1943{10000} \leq c < \def\mathdef1944#1{\mathrm{U{+}#1}}\mathdef1944{110000} \\ \wedge & c = 2^{18}(b_1-\def\mathdef1945#1{\mathtt{0x#1}}\mathdef1945{F0})+2^{12}(b_2-\def\mathdef1946#1{\mathtt{0x#1}}\mathdef1946{80})+2^6(b_3-\def\mathdef1947#1{\mathtt{0x#1}}\mathdef1947{80})+(b_4-\def\mathdef1948#1{\mathtt{0x#1}}\mathdef1948{80})) \\ \end{array} \\ \end{array} \\ \mathrel{\mbox{where}} b_2, b_3, b_4 < \def\mathdef1949#1{\mathtt{0x#1}}\mathdef1949{C0} \\ \end{array}\end{split}$

Note

Unlike in some other formats, name strings are not 0-terminated.