Notation

[math]\displaystyle{ v : τ }[/math] means value [math]\displaystyle{ v }[/math] has type [math]\displaystyle{ τ }[/math].
[math]\displaystyle{ X = a }[/math] means that a type or a value [math]\displaystyle{ X }[/math] is an alias for [math]\displaystyle{ a }[/math].
[math]\displaystyle{ X := \text{[something]} }[/math] means that [math]\displaystyle{ X }[/math] is defined to be [math]\displaystyle{ \text{[something]} }[/math]
A percent sign % preceded only by spaces starts a line comment % [comment]
We use [math]\displaystyle{ \cdot }[/math] to denote that we do not care about the value some variable takes. For example, when quantifying over a set of tuples of the form [math]\displaystyle{ (x, y) }[/math] we may use a [math]\displaystyle{ (x, \cdot) }[/math] to express that we do not care about the value [math]\displaystyle{ y }[/math] takes in each of the tuples.
Let [math]\displaystyle{ X }[/math] be a set or a sequence. We use [math]\displaystyle{ |X| }[/math] to denote the size/length of the set/sequence.
Let [math]\displaystyle{ X }[/math] be a sequence. We use [math]\displaystyle{ X[i] }[/math] to access the element in [math]\displaystyle{ X }[/math] at index [math]\displaystyle{ i }[/math] and [math]\displaystyle{ X[u…v] }[/math] to refer to a slice of the sequence starting at index [math]\displaystyle{ u }[/math] and ending at index [math]\displaystyle{ v }[/math]. For example, for a sequence [math]\displaystyle{ X := (a, b, c, d) }[/math], the [math]\displaystyle{ slice X[2…3] = (b, c) }[/math].
We define the concatenation of two ordered sequences [math]\displaystyle{ a := (x_1, …, x_m) }[/math] and [math]\displaystyle{ b := (y_1, …, y_n) }[/math] as [math]\displaystyle{ (x_1, …, x_m, y_1, …, y_n) }[/math].
We often work with partial maps [math]\displaystyle{ M: X \mapsto Y }[/math], which we write as [math]\displaystyle{ \{ (x_1 \mapsto y_1), \dots, (x_n \mapsto y_n) \} }[/math], where [math]\displaystyle{ \forall~ i, 1 \leq i \leq n : x_i \in X \land y_i \in Y }[/math] and [math]\displaystyle{ \nexists~ i, j, 1 \leq i, j \leq n: x_i = x_j \land i \neq j }[/math]. We note that partial maps can be nested, i.e., the set [math]\displaystyle{ Y }[/math] could again be a partial map
We use square brackets to index into a partial map, for example [math]\displaystyle{ M[x] = y }[/math] if [math]\displaystyle{ (x \mapsto y) \in M }[/math]
In case we work with nested partial maps, such as [math]\displaystyle{ M: X \mapsto (Y \mapsto Z) }[/math], for example, we usually write them as a single map [math]\displaystyle{ M: (X \times Y) \mapsto Z }[/math], i.e., [math]\displaystyle{ \{ ((x_1, y_1) \mapsto z_1), … ((x_m, y_n) \mapsto z_{mn}) \} }[/math].
Let [math]\displaystyle{ X }[/math] be a set. We define [math]\displaystyle{ \min(X) := \{ i | i \in X \land \nexists j \in X : j \lt i \} }[/math] and [math]\displaystyle{ \max(X) := \{ i | i \in X \land \nexists j \in X : j \gt i \} }[/math]. Note that a set can contain multiple incomparable elements in which case [math]\displaystyle{ |\min(X)| }[/math] or [math]\displaystyle{ |\max(X)| }[/math] could be greater than 1.
For partial maps [math]\displaystyle{ M : X \mapsto Y }[/math], we define the function [math]\displaystyle{ \text{dom}(M) := \{ i | (i ↦ ·) \in M \} }[/math].
We define the map merge operator [math]\displaystyle{ A \cup B }[/math] on partial maps [math]\displaystyle{ A: X \mapsto Y }[/math] and [math]\displaystyle{ B: X \mapsto Y }[/math] as [math]\displaystyle{ (x \mapsto y) \in A \cup B }[/math] iff [math]\displaystyle{ (x \mapsto y) \in A \lor (x \mapsto y) \in B }[/math]. The operation fails if the domains of A and B are not disjoint.
We define the [math]\displaystyle{ \text{merge}(S) }[/math] operator, which, for a set of partial maps S : Set<X ↦ Y> is defined as [math]\displaystyle{ \text{merge}(\{ M_1, …, M_n \}) := M_1 ∪ … ∪ M_n }[/math].
When working with sets of types with multiple fields, e.g., set [math]\displaystyle{ S = \{ t_1, …, t_n \} }[/math] of type Set<T> where [math]\displaystyle{ T }[/math] has a field [math]\displaystyle{ A }[/math] of type [math]\displaystyle{ T_A }[/math] we use [math]\displaystyle{ S.A }[/math] to denote the set [math]\displaystyle{ \{ t_1.A, …, t_n.A \} }[/math] of type Set<T_A>.
We do the same for nested partial maps where the innermost partial map is a type with multiple fields. For example, for a map [math]\displaystyle{ M : X \mapsto Y \mapsto T }[/math] we use [math]\displaystyle{ M.A }[/math] to denote the map [math]\displaystyle{ \{ (x \mapsto y \mapsto a) | (x \mapsto y \mapsto t) \in M \land a = t.A \} }[/math] of type [math]\displaystyle{ X ↦ Y ↦ T_A }[/math].
Sometimes we need to drop the property of (nested) partial maps that each key maps to a unique value in which case we use the same notation, but replace the [math]\displaystyle{ \mapsto }[/math] with a [math]\displaystyle{ \times }[/math] in the type definition, i.e., use sets of key-value tuples of type Set((X × … × Y) × V) tuples. We will use the same notational conventions as defined for partial maps above.
We sometimes use FAIL IF: p for some predicate p before function definitions in pseudocode. The semantic of this is that whenever p evaluates to false the actual implementation should fail, while the implementation given in the specification does not fail.
We say that a function [math]\displaystyle{ H: X \rightarrow Y }[/math] is collision resistant, if—for practical purposes—it it will never happen that one comes up with two values [math]\displaystyle{ x, x' \in X }[/math] so that [math]\displaystyle{ x \neq x' }[/math] and [math]\displaystyle{ H(x) = H(x') }[/math].