Notation

We use superscript${}^{\ast }$ to denote an arbitrary length ordered array, usually corresponding to the Vec type in Rust.

$N$ denotes the non-negative integers. $N_{64}$ denotes $N$ restricted to the range corresponding to u64 in Rust of $[0,2^{64})$.

$\mathbb{B}$ denotes a single byte $[0,2^8)$ corresponding to u8 in Rust. We use ${\mathbb{B}}^{\ast }$ for an arbitrary sequence of bytes. Use $N2{\mathbb{B}}^n:N_{8n}\to {\mathbb{B}}^n$ for converting between the integer $N_{8n}$ to ${\mathbb{B}}^n$ in little-endian order.

${\mathbb{B}}^a||{\mathbb{B}}^b$ with $a,b\in N$ is used for concatenation of arbitrary bytes.

$Z_2$ refers to binary bits.

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

$[n]$ with $n\in N$ denotes the sequences of $n$ values starting with 1.