chap01-sec01.tex

% !TEX root = ../zeth-protocol-specification.tex

\section{Data structures and representation}\label{preliminaries:structured-data}

\newcommand{\STR}{\mathsf{STR}}

\subsection{Structured data}\label{preliminaries:data-types:formulation}

When describing the operations to be performed and the data to be manipulated as part of the protocol, we commonly employ tuples of related data where each element of the tuple has some associated semantic meaning and which must often satisfy some conditions. In this section, we develop a framework to reason about such \emph{structured} data, where a single datum may consist of one or more logical parts (called \emph{fields}). The framework is built on top of simple mathematical concepts such as sets, and mappings between them, ensuring that we can always reason about structured data in a rigorous way. We also define notation to aid the specification of structured data, and to refer to specific components of a datum. This will be used extensively in the specification of the protocol.

As a simple motivating example, consider a protocol that processes data relating to individual people. This fictional system may send and receive data such as \emph{name}, \emph{age} and \emph{address} for a single person, grouping this data into a logical unit. Further, each piece of data must satisfy specific conditions (\emph{name} must be a series of characters from some alphabet, \emph{age} must be a positive integer, etc.) We shall make use of this example several times during the formulation below.

In what follows, let $\STR = \smallset{a, b, \ldots, y, z}^{*}$ (the Kleene star of the \emph{Roman alphabet}). In our formulation, field names $f_i$ will be elements in this set.

\begin{remark}
  Note that a similar formulation could be made using an arbitrary set, such as the same alphabet augmented with specific symbols, or the alphabet of a different language. Our choice of $\STR{}$ here is for simplicity.
\end{remark}

We begin by defining a data type as a set of values called ``fields'', each with a ``name'' from $\STR$. Abstract sets are used to constrain the values of each field.

\begin{definition}[Structured Data Type]\label{preliminaries:def:datatype}
  Let $f_0, \ldots, f_{n-1}$ be $n$ distinct elements of $\STR$ and let $V_0, \ldots, V_{n-1}$ be sets, for some $n \in \NN$. We define \emph{the structured data type $\datatypestyle{T}$ with fields $\smallset{(f_i, V_i)}_{i \in [n]}$} to be a set of values:
  \[
    \datatypestyle{T} = V_0 \times \cdots \times V_{n-1}
  \]
  with associated post-fix ``dot'' operators $.f_i : \datatypestyle{T} \to V_i$ for $i = 0, \ldots, n-1$, acting on values $\mathbf{x} \in \datatypestyle{T}$ to extract the individual elements:
  \[
    \mathbf{x}.f_i = v_i \text{, where } \mathbf{x} = (v_0, \ldots, v_{n-1}) \in \datatypestyle{T}
  \]

  Here, we say that the $i$-th field has \emph{field name} $f_i$, with \emph{value set} $V_i$. Each ``dot'' operator $.f_i$ \emph{extracts} the $i$-th component, or the \emph{value with field name $f_i$}.
\end{definition}

\begin{example}\label{preliminaries:eg:datatype-person}
  Consider our example protocol that processes information about people. A potentially useful structured data type $\datatypestyle{Person}$ may be defined with fields:
  \[
    \smallset{ (\varstyle{name}, \STR), (\varstyle{age}, \NN), (\varstyle{height}, \RR^+) }
  \]
  Values $\mathbf{p}$ in $\datatypestyle{Person}$ are simply tuples in $\STR{} \times \NN \times \RR^+$, with semantic meaning (name, age, height) assigned to each component of $\mathbf{p}$.

  Examples of valid elements in $\datatypestyle{Person}$ include $\mathbf{a} = (\varstyle{alice}, 28, 1.65)$ and $\mathbf{b} = (\varstyle{bob}, 31, 1.74)$, where the following equalities hold:
  \begin{align*}
    \mathbf{a}.\varstyle{name} &= \varstyle{alice}, \\
    \mathbf{b}.\varstyle{age} &= 31, \\
    \mathbf{b}.\varstyle{height} &= 1.74;
  \end{align*}
\end{example}

For clarity, structured data types may be specified using tables of names, descriptions and value sets, rather than sets of the form $\smallset{(f_i, V_i)}_{i \in [n]}$. Similarly, it is frequently convenient to include the \emph{field names} alongside values when specifying structured data values.

\begin{example}\label{preliminaries:eg:datatype-person-table}
  $\datatypestyle{Person}$ from \cref{preliminaries:eg:datatype-person} might be described in table-form as follows:
  \begin{table}[H]
    \centering
    \begin{tabular}{cp{15em}c}
      Field                & Description        & Data type \\ \toprule
      $\varstyle{name}$   & Name of the person & $\STR{}$ \\ \midrule
      $\varstyle{age}$    & Age in years       & $\NN$ \\ \midrule
      $\varstyle{height}$ & Height in meters   & $\RR^+$ \\ \midrule
    \end{tabular}
  \end{table}
\end{example}

\begin{example}\label{preliminaries:eg:datatype-person-value-with-field-names}
  The values $\mathbf{a}$ and $\mathbf{b}$ in \cref{preliminaries:eg:datatype-person} might be written as follows:
  \begin{align*}
    \mathbf{a} &=
    \{\varstyle{name}:\: \varstyle{alice}, \; \varstyle{age}:\: 28, \; \varstyle{height}:\: 1.65\} \\
    \mathbf{b} &=
    \{\varstyle{name}:\: \varstyle{bob}, \; \varstyle{age}:\: 31, \; \varstyle{height}:\: 1.74\}
  \end{align*}
\end{example}

\begin{remark}[``dot'' operators in assignment]\label{preliminaries:rem:dot-assignment}
  The ``dot'' operators may be used in algorithm descriptions to indicate \emph{assignment to a specific component}. For example $\mathbf{a}.\varstyle{age} \gets 29$ means that the value of the $\varstyle{age}$ field of $\mathbf{a}$ is replaced by the value $29$.

  Formally, for a structured data type $\datatypestyle{T}$ with fields $\smallset{(f_i, V_i)}_{i \in [n]}$ where $\mathbf{x} = (v_0, \ldots, v_{n-1}) \in \datatypestyle{T}$ and $v_i^\prime \in V_i$:
  \[
    \mathbf{x}.f_i \gets v_i^\prime
  \]
  is equivalent to:
  \[
    \mathbf{x} \gets (v_0, \ldots, v_{i-1}, v_i^\prime, v_{i+1}, \ldots, v_{n-1})
  \]
\end{remark}

We define one further operator and related assignment notation, convenient in cases where $V_i = X^m$ for sets $X$ and $m \in \NN$.
\begin{definition}[Square bracket operator]\label{def:squareb-operator}
  For $m \in \NN$ and set $X$, define the operator $[\ ] : X^m \times [m] \to X$ as:
  \[
    \mathbf{x}[i] = x_i \text{ where } \mathbf{x} = (x_0, \ldots, x_m)
  \]
  For the set $X^*$, the operator takes the form $[\ ] : X^* \times \NN \to X$, defined as:
  \[
    \mathbf{x}[i] =
    \begin{cases}
        x_i & \text{ if } \len{\mathbf{x}} > i \text{ where } \mathbf{x} = (x_0, \ldots) \\
        \bot & \text{otherwise}
    \end{cases}
  \]
\end{definition}

\begin{remark}[Square bracket operators in assignment]
  Similarly to \cref{preliminaries:rem:dot-assignment}, we develop assignment notation for the square bracket operator $[\ ]$.
  Let $\mathbf{x} = (x_0, \ldots, x_{m-1})$ be a member of $X^m$, and $x_i^\prime$ be some element in $X$. The statement:
  \[
    \mathbf{x}[i] \gets x_i^\prime
  \]
  is equivalent to:
  \[
    \mathbf{x} \gets (x_0, \ldots, x_{i-1}, x_i^\prime, x_{x+1}, \ldots, x_{m-1})
  \]
  Informally, this can be interpreted as replacing the $i$-th component of $\mathbf{x}$ with $x_i^\prime$.
\end{remark}

\begin{remark}[Deep structures and chained ``dot'' operators]
Consider the case of structured data $\datatypestyle{T}$ with fields $\{(f_i, V_i)\}_{i \in [n]}$ for $n \in \NN$. Let $\datatypestyle{T^\prime}$ be another structured data type with fields $\{(f^\prime_i, V^\prime_i)\}_{i \in [n^\prime]}$ for $n^\prime \in \NN$, and assume that $V_j = \datatypestyle{T^\prime}$ for some $j \in [n]$. Informally, the values of the $j$-th field of elements of $\datatypestyle{T}$ are themselves structured data of type $\datatypestyle{T^\prime}$.

In this case, ``dot'' operators may be \emph{chained}, so that $\mathbf{x}.f_j.f^\prime_k$ refers to the $k$-th field $v^\prime_k$ of the $j$-th field $v_j$ of $\mathbf{x} \in \datatypestyle{T}$.
\end{remark}

\begin{example}\label{preliminaries:eg:datatype-person-deep}
  Define a structured data type $\datatypestyle{Address}$ with fields $(\varstyle{country}, \STR{}), (\varstyle{zipcode}, \STR{})$. We redefine the structured data type $\datatypestyle{Person}$ from \cref{preliminaries:eg:datatype-person}, with an extra field $\varstyle{address}$ of type $\datatypestyle{Address}$. That is, $\datatypestyle{Person}$ is the structured data type with fields:
  \begin{table}[H]
    \centering
    \begin{tabular}{cp{15em}c}
      Field                 & Description           & Data type \\ \toprule
      $\varstyle{name}$    & Name of the person    & $\STR{}$ \\ \midrule
      $\varstyle{age}$     & Age in years          & $\NN$ \\ \midrule
      $\varstyle{height}$  & Height in meters      & $\RR^+$ \\ \midrule
      $\varstyle{address}$ & Address of the person & $\datatypestyle{Address}$ \\ \midrule
    \end{tabular}
  \end{table}
  An example element $\mathbf{a}$ in $\datatypestyle{Person}$ is:
  \begin{align*}
    \mathbf{a} =
    \{ &\\
       & \varstyle{name}:\: \varstyle{alice}, \\
       & \varstyle{age}:\: 28, \\
       & \varstyle{height}:\: 1.65, \\
       & \varstyle{address}:\: (\varstyle{country}:\: \varstyle{UK}, \varstyle{zipcode}:\: \varstyle{SW1A})\\
    \}
  \end{align*}
  In this case, the following equalities using the dot and square bracket operators all hold:
  \begin{align*}
    & \mathbf{a}.\varstyle{name} = \varstyle{alice} \\
    & \mathbf{a}.\varstyle{height} = 1.65 \\
    & \mathbf{a}.\varstyle{address}.\varstyle{country} = \varstyle{UK} \\
    & \mathbf{a}.\varstyle{address}.\varstyle{zipcode} = \varstyle{SW1A} \\
    & \mathbf{a}.\varstyle{address}.\varstyle{country}[1] = \varstyle{K}
  \end{align*}
\end{example}

\subsection{Representations}\label{preliminaries:data-types:representation}

The binary alphabet $\bin$, denoted $\BB$, is used to represent the presence or absence of an electrical signal in a computer. In fact, every piece of information in a computer is represented as a string of bits.
We assume the existence of an efficient binary representation for some set of primitive datatypes (such as the natural numbers $\NN$, or alphanumeric characters). Structured data types built up from primitive types (as described above) can then recursively be assigned similarly efficient representations.
This is used to define the following functions to \emph{encode} data to its bit-string representation, and to \emph{decode} such bit-strings back to elements of the original type.

\begin{definition}
  For a set $X$ of values which are to be represented as bit strings, we define functions:
  \begin{align*}
    \encode{}{X} &: X \to \BB^* \\
    \decode{}{X} &: \BB^* \to X \cup \bot
  \end{align*}
  satisfying
  \[
    \decode{\encode{x}{X}}{X} = x\ \forall x \in X
  \]
  to be the functions which encode (resp.~decode) elements of $X$ into (resp.~from) the bit-string representations chosen above.
  We note that $\decode{}{X}$ may return $\bot$ in the case that the input bit-string is malformed.
\end{definition}

Without ambiguity, we overload the functions $\encode{}{}$ and $\decode{}{}$ to mean $\encode{}{X}$ and $\decode{}{X}$ where the set $X$ is clear from context.

In the following sections, we assume that elements of $\NN$ are encoded as big-endian binary numbers in the natural way. We denote by $\NN_{b}$ the set of natural numbers that can be uniquely encoded in this way using $b$ bits (possibly with padding). In other words,
\[
  \NN_{b} = \smallset{x \in \NN\ \suchthat\ \encode{x}{\NN} \in \BB^{b}}
\]