streamlet-proof.tex

\subsection{Streamlet is Timely}

We now prove that the Partially Synchronous Streamlet Protocol is timely,
in the partially synchronous setting, after GST.
We work in the same model as the Streamlet paper~\cite{streamlet},
in particular assuming a PKI.

First, we turn Streamlet into a temporal blockchain protocol.
Recall Streamlet proceeds in epochs of duration $2\Delta$ rounds.
\emph{Temporal Streamlet} is the Streamlet protocol with the
following additions: Honest block producers record the first round of the current epoch as the block's recorded round.
Blocks with decreasing recorded rounds or recorded rounds in the future are not accepted.
Temporal Streamlet remains safe---in the language of \cite{streamlet}, \emph{consistent}---and live($u$) for some $u$
if $\frac{t}{n} < \frac{1}{3}$. Furthermore, it has consistent recorded rounds.

Honest party $P$, at the beginning of round $r$, and
before performing any other action, checks the network and
outputs the longest confirmed chain $\Chain[][P][r]$.
Let $G(e)$ be the predicate indicating that epochs $e-3,e-2,e-1,e,e+1$ have honest leaders (this predicate is used to prove liveness in \cite{streamlet}).
Before proving freshness, we first show the maximum interval between two epochs satisfying $G(e)$ is bounded.

\begin{definition}[Temporal Streamlet Typical Execution]
  Consider an execution of the Temporal Streamlet protocol with duration
  of $E$ epochs, $n$ total number of parties and $t$ number of corrupt parties.
  Let $J = \{0,E\} \cup \{0 < e < E: G(e)\}$.
  The execution is \emph{typical} if for all
  $d \geq 5\frac{\kappa + \lg \floor*{\frac{E}{5}}}{- \lg \left(1 - \left(\frac{n - t}{n}\right)^5\right)}$:
  $\max_{e \in J}(\min_{\substack{e' > e \\ e' \in J}}(e' - e)) \leq d$.
\end{definition}

\begin{lemma}[Temporal Streamlet Typicality] \label{lem:honest-quintuple}
  A Temporal Streamlet execution is typical, except with negligible probability in $\kappa$.
\end{lemma}
\begin{proof}
  We let $K = \{0, E\} \cup \{e \in \{5, 10, 15, \ldots, 5\floor*{\frac{E}{5}}\}: G(e)\}$.
  It holds that
  $\max_{e \in J}(\min_{\substack{e' > e \\ e' \in J}}(e' - e)) \leq \max_{e \in K}(\min_{\substack{e' > e \\ e' \in K}}(e' - e))$.
  Therefore:

  \begin{gather*}
      \Pr [\max_{e \in J}(\min_{\substack{e' > e \\ e' \in J}}(e' - e)) > d] \leq \\
      \Pr [\max_{e \in K}(\min_{\substack{e' > e \\ e' \in K}}(e' - e)) > d] \leq \\
      \floor*{\frac{E}{5}} \left(1 - \left(\frac{n - t}{n}\right)^5\right)^{\frac{d}{5}}
  \end{gather*}

  For the second inequality, we observe that each chunk is a Bernoulli trial and we
  apply a union bound.
  Letting $F = \left(1 - \left(\frac{n - t}{n}\right)^5\right)$, we obtain
  $\floor*{\frac{E}{5}} F^{\frac{d}{5}} \leq 2^{-\kappa} \Rightarrow
   \frac{d}{5} \lg F \leq -\kappa - \lg \floor*{\frac{E}{5}} \Rightarrow
   d \geq 5\frac{\kappa + \lg \floor*{\frac{E}{5}}}{- \lg F}
  $.
  \Qed
\end{proof}

\begin{theorem}[Streamlet Recency] \label{thm.streamlet-recency}
  A typical execution of Temporal Streamlet is recent with parameter $w = 2\Delta (d + 1) - 1$.
\end{theorem}
\begin{proof}
  Let $r$ be the current round of the current epoch $e$.
  Let $e' = \max(\{\hat e \leq e: G(\hat e)\} \cup \{0\})$.
  From typicality, it holds that $e - e' \leq d$.
  From the proof of Streamlet liveness~\cite[Theorem 6]{streamlet}, epoch $e'$ contains
  a confirmed honest block produced at round $r' = 2\Delta (e' - 1) + 1$.
  Therefore, $e - e' \leq d
  %\Rightarrow (2 \Delta e) - (2\Delta e' - 2\Delta + 1) \leq 2\Delta d + 2\Delta - 1
  \Rightarrow r - r' \leq 2\Delta (d + 1) - 1$.
  \Qed
\end{proof}

\begin{corollary}[Streamlet Timeliness]
  A typical execution of Temporal Streamlet is timely with parameter $v = 2\Delta (d + 1) - 1$.
\end{corollary}
\begin{proof}
  From Theorems~\ref{thm.streamlet-recency} and~\ref{thm.recency-to-freshness},
  the execution is fresh($2\Delta (d + 1) - 1$).
  From this, safety~\cite[Theorem 3]{streamlet},
  recorded round consistency, and Theorem~\ref{thm:freshness-to-timeliness},
  timeliness with $v = 2\Delta (d + 1) - 1$ follows.
  \Qed
\end{proof}