# Notation

$ℕ$ denotes the non-negative integers. $ℕ₆₄$ denotes $ℕ$ restricted to the range
corresponding to `u64` in Rust of $[0, 2⁶⁴)$.

$𝔹$ denotes a single byte $[0, 2⁸)$ corresponding to `u8` in Rust.
We use $𝔹^*$ for an arbitrary sequence of bytes.

$\t{im}(f)$ denotes the image of a function $f$.