# Notation

The following is the notation used within the descriptions of the state manager and the message routing layer.

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