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.