notation.md 769 B
Notation
We use superscript$^*$ to denote an arbitrary length ordered array, usually
corresponding to the Vec type in Rust.
$ℕ$ 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.
Use $ℕ2𝔹ⁿ : ℕ₈ₙ → 𝔹ⁿ$ for converting between the integer $ℕ₈ₙ$ to $𝔹ⁿ$
in little-endian order.
$𝔹ᵃ||𝔹ᵇ$ with $a, b ∈ ℕ$ is used for concatenation of arbitrary bytes.
$ℤ₂$ refers to binary bits.
$\t{im}(f)$ denotes the image of a function $f$.
$[n]$ with $n ∈ ℕ$ denotes the sequences of $n$ values starting with 1.