properties.tex

\section{Transition Systems Properties}
\label{sec:ts-properties}


\subsection{Transition-system traces}
\label{sec:ts-traces}

This section introduces the notion of traces induced by the transition systems
described in \cite{small_step_semantics}.

\begin{definition}[Traces]
  Given a state transition system $L=(S,T,\Sigma, R, \Gamma)$, the set of
  traces of $L$, denoted as $\fun{traces}_L$ is defined as:
  $$
  \{ (e, s, \txs, s') \mid e \in \Gamma,~ s \in S,~ \txs \in \seqof{\Sigma},~ s' \in S\}
  $$

\end{definition}


\begin{definition}[Valid traces]
  Given a state transition system $L=(S,T,\Sigma, R, \Gamma)$, we define the
  notion of valid traces inductively:

  \begin{itemize}
  \item For all $e \in \Gamma$, $s \in S$, $(e, s, \epsilon, s)$ is a valid
    trace of $L$.

  \item If $(e, s, \txs, s')$ is a valid trace, and
    $e \vdash s' \trans{}{\var{t}} s''$ is a valid transition according to the
    rules of $L$, then $(e, s, \txs; t, s'')$ is also a valid trace.
  \end{itemize}

\end{definition}

We denote the set of valid traces of $L$ as $\transtar{L}{}$, and we write
$e \vdash s \transtar{L}{\txs} s'$ as a shorthand for
$(e, s, \txs, s') \in \transtar{L}{}$. Furthermore, when the transition system
name is clear from the context we will omit it from the transition arrow label.

\subsection{Additional notation}
\label{sec:additional-notation}

We describe next additional notation needed in the properties of the transition
systems specified in this document.

\subsubsection{Sequence indexing}
\label{sec:seq-indexing}

Given a sequence $\mathcal{A} \in \seqof{\type{A}}$, and a natural number $i$
such that $0 \leq i < \size{\mathcal{A}}$, $\mathcal{A}_i$ refers to the
$i^{\text{th}}$ element of $\mathcal{A}$.


Given a sequence $\mathcal{A}$, a quantification symbol $\bigoplus$, e.g.
$\forall$ or $\exists$, a range predicate $R$, and a quantification term $T$
(both of which depend on an element of $\mathcal{A}$) we write:
%
$$
\bigoplus \mathcal{A}_i \cdot R~\mathcal{A}_i \cdot T~\mathcal{A}_i
$$
%
as a shorthand notation for:
%
$$
\bigoplus i \cdot 0 \leq i < \size{\mathcal{A}} \wedge R~\mathcal{A}_i \cdot T~\mathcal{A}_i
$$

For instance:
%
$$
\forall \txs_i \cdot \txins{\txs_i} \neq \emptyset
$$
is a shorthand notation for:
$$
\forall i \cdot 0 \leq i < \size{\txs} \Rightarrow \txins{\txs_i} \neq \emptyset
$$
Remember that the range of a universal quantification can be expressed by an
implication, and the range of an existential qualification by a conjunction.

\subsubsection{Quantifying over set operations}
\label{sec:quantifying-over-set-operators}

Given a sequence $\mathcal{A} \in \seqof{A}$, a set $B$, a set operation
$\bigoplus$, e.g. $\cup$ or $\unionoverrideRight$, and a function
$\fun{f} \in \type{A} \to \type{B}$, the term:
%
$$
\underset{\fun{f}}{\bigoplus} \mathcal{A}
$$
is a shorthand notation for:
%
$$
\underset{0 \leq i < \size{\mathcal{A}}}{\bigoplus} \mathcal{A}_i
$$

For instance:
$$
\bigcup_{\txins{}} \txs
$$
denotes the sequence of unions:
$$
\bigcup_{0 \leq i < \size{\txs}} \txins{\txs_i}
$$

In a set operation quantification over a sequence $\mathcal{A}$, the operation
is applied to the elements the order in which they appear in $\mathcal{A}$.
This is crucial in the case of non-commutative operations, such as union
override ($\unionoverrideRight$).

\subsection{UTxO Properties}
\label{sec:utxo-properties}

Property~\ref{prop:no-double-spending} expresses the fact that transaction
inputs cannot be used more than once. This property requires that the starting
UTxO does not contain any future outputs, which is a reasonable constraint.

\begin{property}[No double spending]\label{prop:no-double-spending}
  For all

  $$
  \left(
    \begin{array}{l}
      \var{utxo_0}\\
      \var{reserves_0}
    \end{array}
  \right)
  \transtar{\hyperref[fig:rules:utxo]{utxo}}{\txs}
  \left(
    \begin{array}{l}
      \var{utxo}\\
      \var{reserves}
    \end{array}
  \right)
  $$

  such that

  $$
    \forall \txs_i \cdot \dom~(\txouts{\txs_i}) \cap \dom~(\var{utxo_0}) = \emptyset
  $$

  we have:

  $$
  \forall \txs_i,~\txs_j \cdot i < j \Rightarrow \txins{\txs_i} \cap \txins{\txs_j} = \emptyset
  $$
\end{property}

Property~\ref{prop:utxo-out-min-in} expresses the fact that all inputs and
outputs are accounted for, in such a way that we can reconstruct the final
(UTxO) state by adding all the outputs to the initial state, and removing the
spent outputs.

\begin{property}[UTxO is outputs minus inputs]\label{prop:utxo-out-min-in}
  For all

  $$
  \left(
    \begin{array}{l}
      \var{utxo_0}\\
      \var{reserves_0}
    \end{array}
  \right)
  \transtar{\hyperref[fig:rules:utxo]{utxo}}{\txs}
  \left(
    \begin{array}{l}
      \var{utxo}\\
      \var{reserves}
    \end{array}
  \right)
  $$

  such that

  $$
    \forall \txs_i \cdot \dom~(\txouts{\txs_i}) \cap \dom~(\var{utxo_0}) = \emptyset
  $$

  we have:

  $$
  \bigcup_{\txins{}} \txs \subtractdom (\var{utxo_0} \cup \bigcup_{\txouts{}} \txs) = \var{utxo}
  $$

\end{property}

Property~\ref{prop:utxo-money-supply-cnst} models the fact that the amount of
money in the system (counted as Lovelaces) remains constant.

\begin{property}[Money supply is constant in the system]\label{prop:utxo-money-supply-cnst}
  For all

  $$
  \left(
    \begin{array}{l}
      \var{utxo_0}\\
      \var{reserves_0}
    \end{array}
  \right)
  \transtar{\hyperref[fig:rules:utxo]{utxo}}{\txs}
  \left(
    \begin{array}{l}
      \var{utxo}\\
      \var{reserves}
    \end{array}
  \right)
  $$

  we have:

  $$ \var{reserves} + \balance{utxo} =  \var{reserves_0} + \balance{utxo_0} $$
\end{property}

\subsection{Delegation Properties}
\label{sec:delegation-props}

Property~\ref{prop:no-dcert-replay} states that delegation certificates cannot be replayed. Remember
that $\Delta_i$ is the $i^{\text{th}}$ element of $\Delta$, which is a sequence of sequences of
delegation certificates, so $\Delta_i \in \seqof{\DCert}$ and $\Delta_{i_j} \in \DCert$ (assuming
$j$ is a valid index of $\Delta_i$).

\begin{property}[No replay of delegation certificates]\label{prop:no-dcert-replay}
  For all
  %
  $$
  \left(
    \begin{array}{l}
      \var{delegSt}
    \end{array}
  \right)
  \transtar{\hyperref[fig:rules:delegation-interface]{deleg}}{\Delta}
  \left(
    \begin{array}{l}
      \var{delegSt'}
    \end{array}
  \right)
  $$
  %
  we have:
  %
  $$
  \forall i, j, k, l \cdot j < l \Rightarrow \Delta_{i_j} \neq \Delta_{k_l}
  $$
\end{property}