definitions.tex

\section{Definitions}\label{sec:defs}

In this work we are concerned with ledgers that
record a round with every transaction indicating the time at which
the transaction in question is recorded on the ledger.

\begin{definition}[Temporal Ledger]
  A \emph{temporal ledger} is a finite sequence of pairs $(r, \tx)$ where $\tx$ is
  a transaction, and $r$ is a \emph{round}.
\end{definition}

\begin{definition}[Distributed Temporal Ledger Protocol]
  A \emph{distributed temporal ledger protocol} is a distributed ledger protocol
  in which when \rread is invoked, honest parties output temporal ledgers instead of traditional ledgers.
\end{definition}

The following property of temporal ledgers is central to this work.

\begin{definition}[Timely]\label{def:timely}
  A distributed temporal ledger protocol execution is \emph{timely}$(v)$
  if for all honest parties $P$ and rounds $r_1$ it holds that:

  \begin{enumerate}
    \item The rounds recorded in $\Ledger[][P][r_1]$ are non-decreasing.\label{def:timely-increasing}
    \item The round recorded at $\Ledger[][P][r_1][-1]$ is at most $r_1$.\label{def:timely-past}
    \item For all $r_1 \leq r_2$, the rounds recorded in $\Ledger[][P][r_2][|\Ledger[][P][r_1]|{:}]$ are
          newer than $r_1 - v$.\label{def:timely-chunk}
  \end{enumerate}
\end{definition}

Timeliness is orthogonal to safety and liveness. Protocols can have any
combination\footnote{One live, timely, but not safe protocol includes all transactions
received from the network with the current round.
One live, safe, but not timely protocol records round $1$ for all transactions.
One safe, timely, but not live protocol always reports empty ledgers.}
of the three properties.

If a temporal ledger protocol is timely and live, then the recorded timestamp of a transaction does not deviate much from the time at which the transaction was written to honest parties.

\begin{lemma}
  In a distributed temporal ledger protocol execution that is timely$(v)$ and live$(u)$, if a transaction $\tx$ is written to an honest party at round $r$, then the round recorded for $\tx$ in any honest party's ledger is $r'$ such that $r - v \leq r' \leq r + u$.
\end{lemma}
\begin{proof}
  The round in which $\tx$ is recorded in any honest party's ledger is between $r$ and $r + u$ by liveness. The claim follows from timeliness.
\end{proof}

\begin{definition}[Perfectly Timely]
  We call a protocol execution \emph{perfectly timely} if it is timely with parameter $v = 0$.
\end{definition}

\begin{definition}[Supersafety]
  A distributed ledger protocol execution is \emph{supersafe} if it is sticky and
  for any honest parties $P_1, P_2$ and any round $r$, it holds that
  $\Ledger[][P_1][r] = \Ledger[][P_2][r]$.
\end{definition}

All supersafe protocol executions are safe.