Values

Bytes

Bytes encode themselves.

\[\begin{split}\begin{array}{llcll@{\qquad}l} \def\mathdef805#1{{}}\mathdef805{byte} & \href{../binary/values.html#binary-byte}{\mathtt{byte}} &::=& \def\mathdef863#1{\mathtt{0x#1}}\mathdef863{00} &\Rightarrow& \def\mathdef864#1{\mathtt{0x#1}}\mathdef864{00} \\ &&|&& \dots \\ &&|& \def\mathdef865#1{\mathtt{0x#1}}\mathdef865{FF} &\Rightarrow& \def\mathdef866#1{\mathtt{0x#1}}\mathdef866{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\mathdef806#1{{\mathit{u}#1}}\mathdef806{N}}\) must not exceed \(\mathrm{ceil}(N/7)\) bytes.

\[\begin{split}\begin{array}{llclll@{\qquad}l} \def\mathdef805#1{{}}\mathdef805{unsigned integer} & \href{../binary/values.html#binary-int}{\def\mathdef828#1{{\mathtt{u}#1}}\mathdef828{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\mathdef867#1{{\mathtt{u}#1}}\mathdef867{(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\mathdef813#1{{\mathit{s}#1}}\mathdef813{N}}\) must not exceed \(\mathrm{ceil}(N/7)\) bytes.

\[\begin{split}\begin{array}{llclll@{\qquad}l} \def\mathdef805#1{{}}\mathdef805{signed integer} & \href{../binary/values.html#binary-int}{\def\mathdef834#1{{\mathtt{s}#1}}\mathdef834{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\mathdef868#1{{\mathtt{s}#1}}\mathdef868{(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\mathdef805#1{{}}\mathdef805{uninterpreted integer} & \href{../binary/values.html#binary-int}{\def\mathdef838#1{{\mathtt{i}#1}}\mathdef838{N}} &::=& n{:}\href{../binary/values.html#binary-int}{\def\mathdef834#1{{\mathtt{s}#1}}\mathdef834{N}} &\Rightarrow& i & (\mathrel{\mbox{if}} n = \href{../exec/numerics.html#aux-signed}{\mathrm{signed}}_{\href{../syntax/values.html#syntax-int}{\def\mathdef819#1{{\mathit{i}#1}}\mathdef819{N}}}(i)) \end{array}\]

Note

The side conditions \(N > 7\) in the productions for non-terminal bytes of the \(\def\mathdef869#1{{\mathit{u}#1}}\mathdef869{}\) and \(\def\mathdef870#1{{\mathit{s}#1}}\mathdef870{}\) encodings restrict the encoding’s length. However, “trailing zeros” are still allowed within these bounds. For example, \(\def\mathdef871#1{\mathtt{0x#1}}\mathdef871{03}\) and \(\def\mathdef872#1{\mathtt{0x#1}}\mathdef872{83}~\def\mathdef873#1{\mathtt{0x#1}}\mathdef873{00}\) are both well-formed encodings for the value \(3\) as a \(\href{../syntax/values.html#syntax-int}{\def\mathdef809#1{{\mathit{u}#1}}\mathdef809{\mathit{8}}}\). Similarly, either of \(\def\mathdef874#1{\mathtt{0x#1}}\mathdef874{7e}\) and \(\def\mathdef875#1{\mathtt{0x#1}}\mathdef875{FE}~\def\mathdef876#1{\mathtt{0x#1}}\mathdef876{7F}\) and \(\def\mathdef877#1{\mathtt{0x#1}}\mathdef877{FE}~\def\mathdef878#1{\mathtt{0x#1}}\mathdef878{FF}~\def\mathdef879#1{\mathtt{0x#1}}\mathdef879{7F}\) are well-formed encodings of the value \(-2\) as a \(\href{../syntax/values.html#syntax-int}{\def\mathdef815#1{{\mathit{s}#1}}\mathdef815{\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\mathdef880#1{\mathtt{0x#1}}\mathdef880{83}~\def\mathdef881#1{\mathtt{0x#1}}\mathdef881{10}\) is malformed as a \(\href{../syntax/values.html#syntax-int}{\def\mathdef809#1{{\mathit{u}#1}}\mathdef809{\mathit{8}}}\) encoding. Similarly, both \(\def\mathdef882#1{\mathtt{0x#1}}\mathdef882{83}~\def\mathdef883#1{\mathtt{0x#1}}\mathdef883{3E}\) and \(\def\mathdef884#1{\mathtt{0x#1}}\mathdef884{FF}~\def\mathdef885#1{\mathtt{0x#1}}\mathdef885{7B}\) are malformed as \(\href{../syntax/values.html#syntax-int}{\def\mathdef814#1{{\mathit{s}#1}}\mathdef814{\mathit{8}}}\) encodings.

Floating-Point

Floating-point values are encoded directly by their IEEE 754 bit pattern in little endian byte order:

\[\begin{split}\begin{array}{llclll@{\qquad\qquad}l} \def\mathdef805#1{{}}\mathdef805{floating-point value} & \href{../binary/values.html#binary-float}{\def\mathdef841#1{{\mathtt{f}#1}}\mathdef841{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\mathdef824#1{{\mathit{f}#1}}\mathdef824{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\mathdef805#1{{}}\mathdef805{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\mathdef886#1{\mathrm{U{+}#1}}\mathdef886{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\mathdef887#1{\mathrm{U{+}#1}}\mathdef887{80} \leq c < \def\mathdef888#1{\mathrm{U{+}#1}}\mathdef888{800} \\ \wedge & c = 2^6(b_1-\def\mathdef889#1{\mathtt{0x#1}}\mathdef889{C0})+(b_2-\def\mathdef890#1{\mathtt{0x#1}}\mathdef890{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\mathdef891#1{\mathrm{U{+}#1}}\mathdef891{800} \leq c < \def\mathdef892#1{\mathrm{U{+}#1}}\mathdef892{10000} \\ \wedge & c = 2^{12}(b_1-\def\mathdef893#1{\mathtt{0x#1}}\mathdef893{C0})+2^6(b_2-\def\mathdef894#1{\mathtt{0x#1}}\mathdef894{80})+(b_3-\def\mathdef895#1{\mathtt{0x#1}}\mathdef895{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\mathdef896#1{\mathrm{U{+}#1}}\mathdef896{10000} \leq c < \def\mathdef897#1{\mathrm{U{+}#1}}\mathdef897{110000} \\ \wedge & c = 2^{18}(b_1-\def\mathdef898#1{\mathtt{0x#1}}\mathdef898{C0})+2^{12}(b_2-\def\mathdef899#1{\mathtt{0x#1}}\mathdef899{80})+2^6(b_3-\def\mathdef900#1{\mathtt{0x#1}}\mathdef900{80})+(b_4-\def\mathdef901#1{\mathtt{0x#1}}\mathdef901{80})) \\ \end{array} \\ \end{array}\end{split}\]