# Values¶

## Bytes¶

Bytes encode themselves.

$\begin{split}\begin{array}{llcll@{\qquad}l} \def\mathdef1228#1{{}}\mathdef1228{byte} & \href{../binary/values.html#binary-byte}{\mathtt{byte}} &::=& \def\mathdef1285#1{\mathtt{0x#1}}\mathdef1285{00} &\Rightarrow& \def\mathdef1286#1{\mathtt{0x#1}}\mathdef1286{00} \\ &&|&& \dots \\ &&|& \def\mathdef1287#1{\mathtt{0x#1}}\mathdef1287{FF} &\Rightarrow& \def\mathdef1288#1{\mathtt{0x#1}}\mathdef1288{FF} \\ \end{array}\end{split}$

## 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}$