app-analysis.tex

\section{Security Analysis with Proofs}\label{app:proofs}

We now prove that PoEM is secure. We begin with our central assumption.

\begin{definition}[Honest Majority Assumption]
  We say that an execution has \emph{honest majority} with \emph{honest advantage parameter}
  $0 < \delta \leq 1$, if the number $t$ of corrupted parties out of
  $n$ parties satisfies $t < (1 - \delta) (n - t)$.
\end{definition}

Consider an execution of the \poem protocol.

We define a random variable $A_{r, i, j}$ as follows.
If at round $r$, the $j$-th query of (honest or adversarial) party $P_i$ is a valid block $B$ (i.e., $H(B) < T$),
then $A_{r, i, j} = \rwork(\rH(B))$.
If no valid block is found, $A_{r, i, j} = 0$.

We define $X_{r} = \max_{j=1}^q \max_{i = 1}^{n - t} A_{r, i, j}$.
If at round $r$ at least one honest party finds a valid block ($X_r > 0$),
we say that round $r$ is a \emph{successful round}.
We let $f = \Pr[X_r > 0] = 1 - (1 - T)^{q(n - t)} \geq q(n - t)T$.
Solving for $T$ we obtain
$f = 1 - (1 - T)^{q(n - t)} \Rightarrow 1 - f = (1 - T)^{q(n - t)} \Rightarrow
(1 - f)^{\frac{1}{q(n - t)}} = 1 - T \Rightarrow T = 1 - (1 - f)^{\frac{1}{q(n - t)}}$.

In our protocol parametrization, we are free to choose how quickly blocks are produced
by honest parties by adjusting the target $T$ parameter, but only some configurations
will yield the desired security results. We will set $T$ such that the following
condition is satisfied.

\begin{definition}[Secure Configuration]
  Given an environment which affords $q (n - t)$ queries per round to
  the honest parties, the secure configuration $f$ of PoEM requires
  $f = \frac{\delta}{6}$. This is achieved by using the secure target
  value $T = 1 - (1 - \frac{\delta}{6})^{\frac{1}{q(n - t)}}$.
\end{definition}

We will prove the PoEM protocol is secure if the above configuration is
followed.

We let $\overline{X}_r = \sum_{i = 1}^{n - t} \sum_{j = 1}^q A_{r,i,j}$ and
\[
  \underbar{X}_r = \begin{cases}
  0 \text{, if there are no $i, j$ with $A_{r,i,j} > 0$; otherwise,}\\
  A_{r,i,j} \text{, where $(i, j)$ are the minimum such $(i, j)$.}
\end{cases}\]
Observe that $\underbar{X}_r \leq X_r \leq \overline{X}_r$
and $\E[\underbar{X}_r] \leq \E[X_r] \leq \E[\overline{X}_r]$.

We define a random variable $Y_r$ as follows.
If at round $r$ exactly one honest party obtains a valid block, then $Y_r = X_r$,
and we call $r$ a \emph{convergence opportunity}. Otherwise, $Y_r = 0$.

We define $Z_{r}$ as the sum of all real intrinsic work generated by all adversarial
party queries during round $r$, namely $Z_{r} = \sum_{i = n - t + 1}^n \sum_{j = 1}^q A_{r, i, j}$.

Given a set of rounds $S$, we define
$X(S) = \sum_{r \in S} X_r$,
$\overline{X}(S) = \sum_{r \in S} \overline{X}_r$,
$\underbar{X}(S) = \sum_{r \in S} \underbar{X}_r$,
$Y(S) = \sum_{r \in S} Y_r$
and $Z(S) = \sum_{r \in S} Z_r$.
Observe $\underbar{X}(S) \leq X(S) \leq \overline{X}(S)$.

\begin{lemma}[Expectation Bounds]\label{lem:expectation-bounds}
  The following bounds hold.
  \begin{enumerate}
    \item $\frac{f}{1 - f} > Tq(n - t)$
    \item $\E[\underbar{X}_r] = \frac{1 - (1 - T)^{q(n - t)}}{\ln2} = \frac{f}{\ln2}
            > \frac{(1 - f)Tq(n - t)}{\ln2}$ \label{eq.ex-underbar-x-bound}
    \item $\E[\overline{X}_r] < \frac{f}{1 - f}\frac{1}{\ln2}$
    \item $\E[Y_r] > \frac{(1 - \frac{\delta}{3})f}{\ln2}$\label{eq.ex-y-bound}
    \item $\E[Z_r] = \frac{tqT}{\ln2} < \frac{t}{n - t} \cdot \frac{f}{1 - f} \cdot \frac{1}{\ln2}  < \left(1 + \frac{\delta}{2}\right)\frac{t}{n - t} \cdot \frac{f}{\ln2}$\label{eq.ex-z-bound}
    \item $\E[Z_r] < \E[X_r]$
  \end{enumerate}
\end{lemma}
\begin{proof}
  Observe that $A_{r, i, j}$ can be expressed in the form $A_{r, i, j} = C_{r, i, j} W_{r, i, j}$,
  with independent boolean random variable $C_{r, i, j} \sim \Bern(T)$ indicating whether the query was successful
  and real random variable $W_{r, i, j} \sim \Exp(\ln2)$ measuring the real work of the block found.
  Concerning expectations, $\E[W_{r, i, j}] = \frac{1}{\ln2}$, and, furthermore,
  $\E[A_{r, i, j}] = \E[A_{r, i, j} | C_{r, i, j} = 0] \Pr[C_{r, i, j} = 0] +
    \E[A_{r, i, j} | C_{r, i, j} = 1] \Pr[C_{r, i, j} = 1] = \E[A_{r, i, j} | C_{r, i, j} = 1] \Pr[C_{r, i, j} = 1] = \frac{T}{\ln2}$.
  The following bounds are similar to~\cite{backbone}.

  \noindent
  \textbf{Bounds for $f$.}
  We note that
  $\frac{f}{1 - f} = \frac{1 - (1 - T)^{q(n - t)}}{(1 - T)^{q(n - t)}} = (1 - T)^{-q(n - t)} - 1 > (1 + T)^{q(n - t)} - 1 > Tq(n - t)$.
  Here, the penultimate inequality stems from $(1 - T)^{-q(n - t)} > (1 + T)^{q(n - t)} \Leftarrow (1 - T)^{-1} > 1 + T \Leftarrow 1 - T^2 < 1 \Leftarrow
  T > 0$. The last inequality stems from Bernoulli's inequality,
  namely $(1 + x)^r \geq 1 + rx$ for integer $r \geq 1$ and real $x \geq -1$.

  \noindent
  \textbf{Bounds for $\E[X]$.}
  The expectation
  $\E[\underbar{X}_r] = \frac{1 - (1 - T)^{q(n - t)}}{\ln2}$
  follows from fact that
  $\underbar{X}_r \sim \Bern(1 - (1 - T)^{q(n - t)}) \Exp(\ln 2)$.
  The bound on $\E[\underbar{X}_r]$ follows from the previous
  bound on $f$.
  The expectation $\E[\overline{X}_r] = \frac{Tq(n - t)}{\ln2} < \frac{f}{1 - f}\frac{1}{\ln2}$
  follows from the fact that $\overline{X}_r$ is the sum of $q(n - t)$ independent
  random variables distributed as $\Bern(T)\Exp(\ln2)$ and the above bounds on $f$.

  \noindent
  \textbf{Bounds for $\E[Y]$.}
  The probability of a convergence opportunity is
  $(n - t) (1 - (1 - T)^q) (1 - T)^{q(n - t - 1)} \geq T q(n - t) (1 - T)^{q(n - t) - 1} >
  T q(n - t) (1 - (q(n - t) - 1)T) > T q(n - t) (1 - T q(n - t))$.
  The first expression is the binomial probability that exactly one, among $n - t$,
  honest party is successful;
  the second is the binomial probability that exactly one, among $q(n - t)$, honest query is successful,
  which implies that exactly one honest party was successful.
  The penultimate inequality is by
  Bernoulli's inequality, namely $(1 + x)^r \geq 1 + rx$ for integer $r \geq 1$ and real $x \geq -1$.

  We have $Y_r \sim \Bern((n - t)(1 - (1 - T)^q)(1 - T)^{q(n - t - 1)}) \Exp(\ln 2)$,
  therefore, $\E[Y_r] > \frac{T q(n - t)(1 - T q(n - t))}{\ln2} \geq \frac{f(1 - f)}{\ln2} > \frac{(1 - \frac{\delta}{3})f}{\ln2}$.
  For the inequality concerning $\E[Y_r]$, the derivation is analogous to~\cite{backbone}.

  \noindent
  \textbf{Bounds for $\E[Z]$.}
  The expectation $\E[Z_r] = \frac{tqT}{\ln2}$ follows from the fact that $Z_r$
  is distributed as a sum of $tq$ independent samples distributed as $\Bern(T) \Exp(\ln2)$.
  For the bound, we have
  $\E[Z_r] < \frac{t}{n - t}\frac{f}{1 - f}\frac{1}{\ln2} < \left(1 + \frac{\delta}{2}\right)\frac{t}{n - t} \cdot \frac{f}{\ln2}$ % \stepcounter{equation}\tag{\theequation}\label{eq.ex-z-bound}$
    % \E[Z(S)] =
    % \E[\sum_{r \in S} Z_r] = \sum_{r \in S} \E[Z_r] = \sum_{r \in S} \sum_{i = 1}^{t}{ \sum_{j = 1}^{q}{ \E[Z_{r, i, j}] } } = tq|S| \E[A_{r, i, j}] =\\
    % \frac{tq|S| T}{\ln2}\,.
  % \end{align*}
  using an analysis completely analogous to the one in~\cite{backbone}.
  \dznote{Write this derivation explicitly}

  For $\E[Z_r] < \E[X_r]$, we have
  $\E[Z_r] < \E[X_r]
  \Leftarrow \E[Z_r] < \E[\underbar{X}_r]
  \Leftarrow \frac{tqT}{\ln2} < \frac{(1 - f)Tq(n - t)}{\ln2}
  \Leftarrow \frac{t}{n - t} < 1 - f
  \Leftarrow 1 - \delta < 1 - f
  \Leftarrow f < \delta$, which follows from
  the secure configuration.
\end{proof}

% TODO: revise based on new "guess" notion in Backbone '24
\begin{definition}[Causality]
  An execution is \emph{causal} if no block (directly or indirectly) extends
  one which is computed at a later or the same random oracle query.
\end{definition}

\begin{definition}[Hash Separation] % TODO: define it the other way around as well
  An execution has Hash Separation if for all two (adversarial or honest) chains
  $C_1, C_2$ appearing in the execution, if $\rwork(C_1) < \rwork(C_2)$, then $\work(C_1) < \work(C_2)$.
\end{definition}

\begin{definition}[\poem Typical Execution]\label{def:typicality}
  An execution of \poem is \emph{($\epsilon,\lambda$)-typical} (or just typical),
  for $\epsilon \in (0,1)$ and integer $\lambda > 4$, if for any set $S$ of at
  least $\lambda$ consecutive rounds, the following hold.
  \begin{itemize}
    \item
    \begin{minipage}{\linewidth}%
      \vspace{-\abovedisplayskip}%
      \begin{align}%
        (1 - \epsilon) \E[\underbar{X}(S)] < X(S) < (1 + \epsilon) \E[\overline{X}(S)] \label{eq.typical-x}%
      \end{align}%
    \end{minipage}

    \item
    \begin{minipage}{\linewidth}%
      \vspace{-\abovedisplayskip}%
      \begin{align}%
        (1 - \epsilon) \E[Y(S)] < Y(S) \label{eq.typical-y}%
      \end{align}%
    \end{minipage}

    \item
    \begin{minipage}{\linewidth}%
      \vspace{-\abovedisplayskip}%
      \begin{align}%
        Z(S) < (1 + \epsilon)\E[Z(S)] \label{eq.typical-z}%
      \end{align}%
    \end{minipage}

    \item It is causal.
    \item It has hash separation.
  \end{itemize}
\end{definition}

In our analysis, we will let $\epsilon = \frac{\delta}{6}$. If the desired
maximum probability of failure is made concrete, this $\epsilon$, together
with the concrete probabilities later calculated in Theorem~\ref{thm:typicality},
will determine the concrete value of $\lambda$, from which the rest of the
concrete protocol parameters follow. In particular, the value $k$
for the ledger stabilization rule is
determined by $\lambda$ and $f$, and $\lambda$ can be calculated from $\epsilon$,
whereas both $f$ and $\epsilon$ can be determined from the desired acceptable
honest advantage $\delta$.

We will now prove that typical executions occur with overwhelming probability.
Towards this purpose, we will need a couple of auxiliary lemmas.

In the following arguments, we connect the \emph{real valued}
random oracle, evaluated using the $\rwork(\rH(B)) \in \mathbb{R}^+$
function (an ideal quantity
unobservable by any Turing Machine, as it cannot process real-valued
inputs), and its $\kappa$-bit \emph{discrete approximation} $\work(H(B))$ (observable by
a Turing Machine). We show the
difference between these two quantities is immaterial for polynomially bound
computations, namely they notably diverge only with negligible probability.
This connection between real-valued and discrete-valued
random variables will allow us to conduct our analysis using \emph{continuous}
random variables and, in particular, random variables distributed according to the
exponential distribution. These distributions lend themselves
to easier tools than conducting a cumbersome analysis in the discrete domain;
for instance, the sum of i.i.d. exponentially distributed variables is the gamma
distribution.
The following lemmas that translate between the continuous and discrete worlds
will allow us to later utilize our continuous results in the discrete
realization of the protocol.

First, we make a few observations about the relationship
between the real and the discrete work of blocks and chains.
Observe that for hash input $A$, we have
$H(A) \leq \rH(A)$ and for block $B$ we have
$\work(H(B)) \geq \rwork(\rH(B))$,
and for blocks $B_1, B_2$ we have
$\rwork(\rH(B_1)) \geq \rwork(\rH(B_2)) \rightarrow \work(H(B_1)) \geq \work(H(B_2))$.

Furthermore, discretizing real works preserves
the order of blocks in the following fashion.

\begin{lemma}\label{lemma:awork-rounding}
  For all $A, B \in (0, 1)$, it holds that
  $\rwork(A) \geq \rwork(B) \rightarrow \work(A) \geq \work(B)$.
\end{lemma}
\begin{proof}
  \begin{align*}
                &\rwork(A) \geq \rwork(B) \Rightarrow -\lg A \geq -\lg B \Rightarrow \lg A \leq \lg B\\
    \Rightarrow &A \leq B \Rightarrow 2^\kappa A \leq 2^\kappa B \Rightarrow \lfloor 2^\kappa A \rfloor \leq \lfloor 2^\kappa B \rfloor \Rightarrow \frac{\lfloor 2^\kappa A \rfloor}{2^\kappa} \leq \frac{\lfloor 2^\kappa B \rfloor}{2^\kappa}\\
    \Rightarrow &\lg \frac{\lfloor 2^\kappa A \rfloor}{2^\kappa} \leq \lg \frac{\lfloor 2^\kappa B \rfloor}{2^\kappa} \Rightarrow -\lg \frac{\lfloor 2^\kappa A \rfloor}{2^\kappa} \geq -\lg \frac{\lfloor 2^\kappa B \rfloor}{2^\kappa}\\
    \Rightarrow &\work(A) \geq \work(B)
  \end{align*}
  \Qed
\end{proof}

Showing that the order of \emph{chains}
is preserved under discretization is a bit more involved,
and we will work towards it next.
Towards this, we observe that the discrete work of a block is
close to its real work.

\begin{lemma}[Block Work Approximation]\label{lem:block-work-approximation}
  In a PoEM execution, consider the event $\CLOSE$ that all blocks $B$
  have $\work(B) - \rwork(B) < 2^{-\kappa/2}$.
  The probability $\Pr[\CLOSE]$ is overwhelming in $\kappa$.
\end{lemma}
\begin{proof}
  Consider the event $E$ in which for all blocks $B$ it holds that
  $\rH(B) > 2^{-(\kappa/2 - 2)}$.
  Let us calculate the probability of $\lnot E$. For $\lnot E$ to happen,
  at least one block must have $\rH(B) \leq 2^{-(\kappa/2 - 2)}$.
  For any block $B$, it holds that $\Pr[\rH(B) \leq 2^{-(\kappa/2 - 2)}] = 2^{-(\kappa/2 - 2)}$ (from the
  uniform distribution of $\rH(B)$ in the interval $(0, 1)$ due to it being a real-valued random oracle).
  Since there are at most $nqL$ blocks in the execution, by applying a union bound, we have
  $\Pr[\lnot E] = \Pr[\exists B: \rH(B) \leq 2^{-(\kappa/2 - 2)}] \leq \sum_B \Pr[\rH(B) \leq 2^{-(\kappa/2 - 2)}] \leq nqL 2^{-(\kappa/2 - 2)}$,
  which is negligible in $\kappa$,
  so $E$ happens with overwhelming probability.

  Consider a block $B$ of the execution, conditioned on the event $E$.
  Then
  \begin{align*}
        &\work(B) - \rwork(B) = -\lg H(B) - (-\lg \rH(B))\\
        \numrel{<}{lem:block-work-approximation-floor}& \lg \rH(B) - \lg\left(\rH(B) - 2^{-\kappa}\right)
        \numrel{<}{lem:block-work-approximation-log-dec} \lg{2^{-(\kappa/2 - 2)}} - \lg\left(2^{-(\kappa/2 - 2)} - 2^{-\kappa}\right)\\
       =& -\left(\frac{\kappa}{2} - 2\right) - \lg(2^{-(\kappa/2 - 2)}(1 - 2^{-(\kappa/2 + 2)})) \\
       =& -\left(\frac{\kappa}{2} - 2\right) + \left(\frac{\kappa}{2} - 2\right) - \lg\left(1 - 2^{-(\kappa/2 + 2)}\right)
       = -\lg\left(1 - 2^{-(\kappa/2 + 2)}\right)\\
       =& -\ln\left(1 - 2^{-(\kappa/2 + 2)}\right) \cdot \frac{1}{\ln2}
    \numrel{\leq}{lem:block-work-approximation-log-ineq} -\frac{-2^{-(\kappa/2 + 2)}}{1 - 2^{-(\kappa/2 + 2)}} \cdot \frac{1}{\ln2} \\
    \leq& \frac{2^{-(\kappa/2 + 2)}}{1 - \frac{1}{2}} \cdot \frac{1}{\ln2}
    = 2^{-(\kappa/2 + 1)} \cdot \frac{1}{\ln2}
    < 2^{-\kappa/2}\,.
  \end{align*}

  Inequality~(\ref{lem:block-work-approximation-floor}) stems from the fact that
  $\rH(B) - 2^{-\kappa} < H(B) \leq \rH(B)$ and the monotonicity of $\lg$.
  Inequality~(\ref{lem:block-work-approximation-log-dec}) stems from
  the fact that the function $\lg x - \lg\left(x - 2^{-\kappa}\right) = \lg \frac{x}{x - 2^{-\kappa}}$ is
  decreasing for $x > 2^{-\kappa}$, remembering our conditioning on
  $\rH(B) > 2^{-(\kappa/2 - 2)} > 2^{-\kappa}$.
  Inequality~(\ref{lem:block-work-approximation-log-ineq}) stems from the standard logarithm
  inequality $\ln(1 + x) \geq \frac{x}{1 + x}$ for all $x > -1$.
  \Qed
\end{proof}

The discrete work of a chain is also close to the real work of a chain.

\begin{corollary}[Chain Work Approximation]\label{cor:chain-work-approximation}
  In a PoEM execution, the probability that all subchains $C^*$
  have $\work(C^*) - \rwork(C^*) < Lqn 2^{-\kappa/2}$
  is overwhelming in $\kappa$.
\end{corollary}
\begin{proof}
  Conditioned on the overwhelming event of Lemma~\ref{lem:block-work-approximation}, for all
  subchains $C^*$ it holds that
  \begin{align*}
     &\work(C^*) - \rwork(C^*) = \sum_{B \in C^*}{\work(B) - \rwork(B)}\\
    <& \sum_{B \in C^*}{2^{-\kappa/2}} = |C*| 2^{-\kappa/2} \leq Lqn 2^{-\kappa/2}\,.
  \end{align*}
  \Qed
\end{proof}

We are now ready to prove a technical lemma which shows that works
of chains do not fall dangerously close to each other.

\begin{lemma}\label{lem:good-ranges}
  Consider a PoEM execution $\mathcal{E}$ with $n$ parties, $q$ queries per round per party,
  and total lifetime $L$.
  Consider the $j$-th random oracle query in this execution.
  If the query is successful, let $B$ indicate its produced block, let
  $\rw = \rwork(B), w = \work(B)$, and let $C$ be the
  chain it extends, let $\rw_1 = \rwork(C), w_1 = \work(C)$, and
  $\rw_1' = \rwork(CB), w_1' = \work(CB)$. Consider any other chain $C_i$ that appears in the
  execution, and let $\rw_2 = \rwork(C_i), w_2 = \work(C_i)$.
  Let $\BADRANGE_{j,i}$ denote the event that both
  $\rw_1 < \rw_2$, and, furthermore, either
  $\rw_2 - \frac{nqL}{2^{\kappa/2}} - \frac{1}{2^{\kappa/2}} \leq \rw_1 + \rw < \rw_2$ or
  $\rw_2 < \rw_1 + \rw \leq \rw_2 + \frac{nqL}{2^{\kappa/2}} + \frac{1}{2^{\kappa/2}}$.
  Let $\BADRANGE$ denote the event that there exists a random oracle query $j$
  and a chain $C_i$ in the execution such that $\BADRANGE_{j,i}$.
  The probability $\Pr[\BADRANGE]$ is negligible in $\kappa$.
\end{lemma}
\begin{proof}
  If the $j$-th query does take place, its $\rw$ is distributed as $\Exp(\ln2)$,
  so for every other chain $C_i$ in the execution for which $\rw_1 < \rw_2$ we have
  \begin{align*}
    \Pr[\rw_2 - \frac{nqL}{2^{\kappa/2}} - \frac{1}{2^{\kappa/2}} \leq \rw_1 + \rw < \rw_2 | \rw_1 < \rw_2] = \\
    \Pr[\rw_2 - \rw_1 - \frac{nqL}{2^{\kappa/2}} - \frac{1}{2^{\kappa/2}} \leq \rw < \rw_2 - \rw_1 | \rw_1 < \rw_2] = \\
    (1 - 2^{-(\rw_2 - \rw_1)}) - (1 - 2^{-\left(\rw_2 - \rw_1 - \frac{nqL}{2^{\kappa/2}} - \frac{1}{2^{\kappa/2}}\right)}) = \\
    2^{-\left(\rw_2 - \rw_1 - \frac{nqL}{2^{\kappa/2}} - \frac{1}{2^{\kappa/2}}\right)} - 2^{-(\rw_2 - \rw_1)} = \\
    2^{-(\rw_2 - \rw_1)} (2^{\frac{nqL}{2^{\kappa/2}} + \frac{1}{2^{\kappa/2}}} - 1) \leq
    2^{\frac{nqL}{2^{\kappa/2}} + \frac{1}{2^{\kappa/2}}} - 1 <
    \frac{nqL}{2^{\kappa/2}} + \frac{1}{2^{\kappa/2}}\,.
  \end{align*}

  The second relation is from the cumulative distribution function of the exponential distribution;
  the fifth relation is from the conditioning on $\rw_1 < \rw_2$, and the last relation is from
  Lemma~\ref{lem:bernoulli}, noting that $0 < \frac{nqL + 1}{2^{\kappa/2}} < 1$.

  Similarly, for the other direction,
  \begin{align*}
    \Pr[\rw_2 < \rw_1 + \rw \leq \rw_2 + \frac{nqL}{2^{\kappa/2}} + \frac{1}{2^{\kappa/2}} | \rw_1 < \rw_2] = \\
    \Pr[\rw_2 - \rw_1 < \rw \leq \rw_2 - \rw_1 + \frac{nqL}{2^{\kappa/2}} + \frac{1}{2^{\kappa/2}} | \rw_1 < \rw_2] = \\
    (1 - 2^{-\left(\rw_2 - \rw_1 + \frac{nqL}{2^{\kappa/2}} + \frac{1}{2^{\kappa/2}}\right)}) - (1 - 2^{-(\rw_2 - \rw_1)}) = \\
    2^{-(\rw_2 - \rw_1)} - 2^{-\left(\rw_2 - \rw_1 + \frac{nqL}{2^{\kappa/2}} + \frac{1}{2^{\kappa/2}}\right)} = \\
    2^{-(\rw_2 - \rw_1)} (1 - 2^{-\frac{nqL}{2^{\kappa/2}} - \frac{1}{2^{\kappa/2}}}) \leq
    1 - 2^{-\frac{nqL}{2^{\kappa/2}} - \frac{1}{2^{\kappa/2}}} <
    \frac{nqL}{2^{\kappa/2}} + \frac{1}{2^{\kappa/2}}\,.
  \end{align*}

  Consequently,
  \begin{align*}
      &\Pr[\BADRANGE_{j,i}]
    = \Pr[\BADRANGE_{j,i}|\rw_1 < \rw_2]\Pr[\rw_1 < \rw_2]\\
    \leq & \Pr[\BADRANGE_{j,i}|\rw_1 < \rw_2]\\
    = &\Pr[\rw_2 - \frac{nqL}{2^{\kappa/2}} - \frac{1}{2^{\kappa/2}} \leq \rw_1 + \rw < \rw_2 | \rw_1 < \rw_2] +\\
      &\Pr[\rw_2 < \rw_1 + \rw \leq \rw_2 + \frac{nqL}{2^{\kappa/2}} + \frac{1}{2^{\kappa/2}} | \rw_1 < \rw_2]\\
    = &2 \frac{nqL + 1}{2^{\kappa/2}}\\
  \end{align*}

  Applying a union bound over all the queries $j$ and chains $i$ of the execution, we obtain
  $\Pr[\BADRANGE] \leq 2 (nqL)^2 \cdot \frac{nqL + 1}{2^{\kappa/2}}$, which is negligible in $\kappa$.
  \Qed
\end{proof}

\begin{lemma}[Hash Separation]\label{lem:hash-separation}
  A causal execution of PoEM has Hash Separation except with negligible
  probability in $\kappa$.
\end{lemma}
\begin{proof}
  % There are at most $Lqn$ random oracle queries in the execution.
  Consider a causal execution of PoEM for which
  the event $\CLOSE$ of Lemma~\ref{lem:block-work-approximation}
  and the event $\lnot \BADRANGE$ of Lemma~\ref{lem:good-ranges}
  both hold.
  Observe that the statement of Corollary~\ref{cor:chain-work-approximation}
  holds in this conditioning.
  From the two lemmas we know $\Pr[\CLOSE]$ and
  $\Pr[\lnot \BADRANGE]$ are both overwhelming, therefore
  $\Pr[\CLOSE \land \lnot \BADRANGE]$ is overwhelming.
  Conditioned on this event, we will
  show that the desired statement holds with probability $1$.

  Let $\HS$ be the event that Hash Separation holds.
  Let $\HS_j$ denote the predicate that $\HS$ holds for all chains appearing
  before, or at, the $j$-th random oracle query, with $j = 0$ indicating
  the beginning of the execution.
  We will use induction on $j$ to show that for all $0 \leq j \leq Lnq$,
  $\HS_j$ holds. We know that $\HS_0$ always holds by definition.

  Now, consider the $j$-th random oracle query and suppose $\HS_{j - 1}$ holds.
  If the query was unsuccessful, then $\HS_j$ holds, and we are done.
  Otherwise, let $C_1$ be the chain
  that the $j$-th random oracle query extends, let $B$ be the block mined on it,
  let $C'_1 = C_1 B$, and let $\rw = \rwork(B), \rw_1 = \rwork(C_1), \rw'_1 = \rwork(C'_1)$
  and $w, w_1, w'_1$ be the respective discrete works.
  Consider any other chain $C_2$ with work $\rw_2 = \rwork(C_2)$
  and discrete work $w_2$
  that has already appeared in the execution,
  and consider the undesirable event $\FLIP_{C_1,C_2}$ that
  $\rw'_1 < \rw_2 \land w'_1 \geq w_2$ or $\rw'_1 > \rw_2 \land w'_1 \leq w_2$.
  If $\rw_1 \geq \rw_2$, then, because $\rw > 0$, therefore $\rw_1 + \rw > \rw_2$ and hence $\rw_1' > \rw_2$.
  Additionally, by $\HS_{j - 1}$ we have $w_1 > w_2$, therefore $w_1 + w > w_2$, and
  $w_1' > w_2$. From this, it follows that $\rw_1 \geq \rw_2$ yields $\lnot \FLIP_{C_1,C_2}$.
  Thus, it suffices to only consider the situation where $\rw_1 < \rw_2$.

  \textbf{Case 1: } $\rw_1 + \rw < \rw_2$.
  From the conditioning on $\lnot \BADRANGE$, we have
  $\rw_1 + \rw < \rw_2 - \frac{nqL}{2^{\kappa/2}} - \frac{1}{2^{\kappa/2}}$,
  therefore
  $
    w_1 - \frac{nqL}{2^{\kappa/2}} + \rw < \rw_2 - \frac{nqL}{2^{\kappa/2}} - \frac{1}{2^{\kappa/2}}\Rightarrow
    w_1 + \rw < \rw_2 - \frac{1}{2^{\kappa/2}}\Rightarrow
    w_1 + w - \frac{1}{2^{\kappa/2}} < \rw_2 - \frac{1}{2^{\kappa/2}}\Rightarrow
    w_1 + w < \rw_2 \Rightarrow
    w'_1 < \rw_2 \leq w_2
  $.
  The first inequality is obtained from the conditioning on $\CLOSE$,
  noting that $w_1 - \frac{nqL}{2^{\kappa/2}} < \rw_1$ follows from
  $w_1 - \rw_1 < Lqn 2^{-\kappa/2}$ (Corollary~\ref{cor:chain-work-approximation}).
  The third inequality is also obtained from the conditioning on $\CLOSE$,
  noting that $w - \frac{1}{2^{\kappa/2}} < \rw$ follows from
  $w - \rw < 2^{-\kappa/2}$ (Lemma~\ref{lem:block-work-approximation}).
  It follows that $\lnot \FLIP_{C_1,C_2}$.

  \textbf{Case 2: } $\rw_1 + \rw > \rw_2$.
  From the conditioning on $\lnot \BADRANGE$, we have
  $\rw_1 + \rw > \rw_2 + \frac{nqL}{2^{\kappa/2}} + \frac{1}{2^{\kappa/2}} > \rw_2 + \frac{nqL}{2^{\kappa/2}}$,
  therefore
  $\rw_1 + \rw > w_2 - \frac{nqL}{2^{\kappa/2}} + \frac{nqL}{2^{\kappa/2}} \Rightarrow \rw_1 + \rw > w_2 \Rightarrow
    w_1 + w > w_2 \Rightarrow w'_1 > w_2$.
  Again, it follows that $\lnot \FLIP_{C_1,C_2}$.

  From this and $\HS_{j-1}$ it follows that $\HS_j$ holds.
  Therefore, by induction, $\HS_{Lnq}$ holds, and hence $\HS$ holds.
  Since our conditioning was on an overwhelming event, the lemma follows.
  \Qed
\end{proof}

\dznote{Handle the case of equality}

\begin{corollary}[Approximate Fork Choice]
  In Hash Separated executions of PoEM, for any two chains $C_1, C_2$
  it holds that $\work(C_1) < \work(C_2) \rightarrow \rwork(C_1) < \rwork(C_2)$.
\end{corollary}
\begin{proof}
  Suppose towards a contradiction $\work(C_1) < \work(C_2)$, but
  $\rwork(C_1) \geq \rwork(C_2)$. From Hash Separation, it follows that
  $\work(C_1) \geq \work(C_2)$, which is a contradiction.
  \Qed
\end{proof}

\begin{theorem}[Typicality]\label{thm:typicality}
  An execution of duration $L$ of \poem is $(\epsilon, \lambda)$-typical with
  probability $1 - e^{-\Omega(\lambda - \log L)} - e^{-\Omega(\kappa - \log L)}$,
  % TODO: The correct probability is $1 - e^{-\Omega(\epsilon^2 \lambda f - \log L)} - e^{-\Omega(\kappa - \log L)}$
  namely, overwhelming in $\lambda$ and $\kappa$.
\end{theorem}
\begin{proof}
  For each $S$ with $|S| = \lambda$,
  \begin{align*}
    \Pr[X(S) < (1 - \epsilon)\E[\underbar{X}(S)]] &\leq\\
    \Pr[\underbar{X}(S) < (1 - \epsilon)\E[\underbar{X}(S)]] &\leq
    e^{-\Omega(\lambda)} \,.\\
    \Pr[X(S) > (1 + \epsilon)\E[\overline{X}(S)]] &\leq\\
    \Pr[\overline{X}(S) > (1 + \epsilon)\E[\overline{X}(S)]] &\leq
    e^{-\Omega(\lambda)} \,.\\
    \Pr[Y(S) < (1 - \epsilon)\E[Y(S)]] \leq e^{-\Omega(\lambda)} &\,.\\
    \Pr[Z(S) > (1 + \epsilon)\E[Z(S)]] \leq e^{-\Omega(\lambda)} &\,.\\
  \end{align*}
  The $e^{-\Omega(\lambda)}$ bounds are obtained by applying
  Lemma~\ref{lem:bern-exp} to each of the random variables
  $\underbar{X}(S), \overline{X}(S), Y(S)$ and $Z(S)$, each
  of which is the sum of $\Theta(\lambda)$ i.i.d. random variables\
  distributed according to $\Bern(p) \times \Exp(\ln2)$ for
  some respective $p \in (0, 1)$.
  Applying a union bound for all $S$ (of which there are $L - \lambda + 1$),
  we obtain that typicality Eq.~\ref{eq.typical-x}, Eq.~\ref{eq.typical-y}
  and Eq.~\ref{eq.typical-z}
  hold with probability $1 - e^{-\Omega(\lambda)+\ln L}$.
  If typicality bounds
  hold for all $S$ with $|S| = \lambda$, then they hold for all $S$ with
  $|S| \geq \lambda$.

  The probability bound for causality follows from the stochastic nature
  of the Random Oracle and is proven in~\cite{backbone}.

  Lastly, Hash Separation follows from Lemma~\ref{lem:hash-separation}.
  \Qed
\end{proof}

\begin{definition}[Block Work Interval]
  A block $B$ of chain $C$ has \emph{work interval}
  $I(B) = \{\xi \geq 0: [\xi] \rlhd C = B\}$.
\end{definition}

\begin{lemma}[Entropic Pairing Lemma] \label{lem:pairing}
  Consider a typical execution of PoEM.
  Suppose a block $B$ of a chain $C$ with work interval $I(B)$
  was computed by an honest party in a convergence opportunity.
  For every $\xi \in I(B)$ and every chain $C'$ of the execution,
  block $B' = [\xi] \lhd C'$ is either $B$ or adversarial,
  as long as $B' \neq \bot$.
\end{lemma}
\begin{proof}
  Consider an execution as in the statement and suppose, towards a contradiction,
  that block $B'$ is not $B$ and is honestly computed.
  Since $B$ was computed in a convergence opportunity, $B$ and $B'$
  cannot have been computed in the same round. Let $r$ be the earliest round
  on which $B$ or $B'$ was computed, and $C$ be the chain whose tip this block is.
  Since it was computed by
  an honest party, at round $r + 1$, every other honest party receives
  a chain with real work greater or equal to $\xi$.

  \textbf{Claim: } Every block computed after round $r$ will be extending a
  chain with real work at least $\xi$. To see this, consider a chain $C^*$ that an honest
  party is extending after $r$. Since the party has adopted $C^*$, by the heaviest
  chain rule, $\work(C^*) \geq \work(C)$. By Hash Separation, $\rwork(C^*) \geq \rwork(C) \geq \xi$.

  If $B$ is computed after round $r$, it holds that $\xi \not \in I$ (noting that $\rwork(B) > 0$).
  If $B'$ is computed after round $r$, it holds that $B' \neq [\xi] \lhd C'$.
  Both lead to a contradiction. \Qed
\end{proof}

% The following conjecture is likely true and will allow us to tighten the analysis:
%
% \begin{conjecture}[Entropic Pairing Conjecture]
%   Consider any block $B$ of chain $C$ with work interval $I(B)$
%   computed by an honest party during a round $r$ such that
%   for every $B'$ which was honestly computed during round $r$,
%   it holds that $\work(B) \geq \work(B')$.
%   Then, for every $\xi \in I(B) \setminus I(B')$ and every chain $C'$ of the execution,
%   block $B' = [\xi] \lhd C'$ is either $B$ or adversarial,
%   as long as $B' \neq \bot$.
% \end{conjecture}

\begin{lemma}[Entropic Chain Growth Lemma]\label{lem:chain-growth}
  Suppose that at round $r_1$ an honest party $P_1$ has a chain which has real work $\rw$.
  Then, at round $r_2 \geq r_1$, every honest party $P_2$
  adopts a chain which has real work at least
  $\rw + \sum_{r = r_1}^{r_2 - 1}{X_r}$.
\end{lemma}
\begin{proof}
  By induction on $r_2$. For the inductive base ($r_2 = r_1$), observe that
  if at round $r_1$ party $P_1$ has a chain $C$ of work $\rw$, then
  $P_1$ broadcasted $C$ at the end or round $r_1 - 1$.
  Party $P_2$ receives $C$ at round $r_1$.
  Consider the chain $C_2$ that $P_2$ adopts at $r_1$.
  Due to the heaviest chain rule, $\work(C_2) \geq \work(C)$,
  therefore, by Hash Separation, $\rwork(C_2) \geq \rw$,
  and the statement follows.

  For the inductive step, note that by the inductive hypothesis,
  every honest party has adopted a chain of real work at least $\rw' = \rw + \sum_{r = r_1}^{r_2 - 2}{X_r}$
  at round $r_2 - 1$. When $X_{r_2 - 1} = 0$ the statement follows directly, so assume
  $X_{r_2 - 1} > 0$. Observe that an honest party $P_3$ successfully queried the random oracle
  at round $r_2 - 1$
  and obtained a chain $C_3$ of real work at least $\rw' + X_{r_2 - 1}$ and broadcasted it to the network.
  At round $r_2$, party $P_2$ receives $C_3$ and
  adopts a chain $C_2$, with $\work(C_2) \geq \work(C_3)$ due to the heaviest chain rule.
  By Hash Separation, $\rwork(C_2) \geq \rwork(C_3) \geq \rw' + X_{r_2 - 1} = \rw + \sum_{r = r_1}^{r_2 - 1}{X_r}$.
  \Qed
\end{proof}

\begin{lemma}[Typical Bounds] \label{lem:typical-bounds}
  In typical PoEM executions, for any set $S$ of at least $\lambda$ consecutive rounds,
  it holds that:

  \begin{enumerate}
    \item $Z(S) < \frac{t}{n - t} \cdot \frac{f}{1 - f} \cdot \frac{|S|}{\ln2} + \epsilon f \frac{|S|}{\ln2} \leq (1 - \frac{2 \delta}{3}) f \frac{|S|}{\ln2}$. \label{eq.typ-bound-z}
    \item $Z(S) < \left(1 + \frac{\delta}{2}\right)\frac{t}{n - t} X(S) + \frac{\epsilon f |S|}{\ln2}$. \label{eq.typ-bound-z-x}
    \item $Z(S) < Y(S)$. \label{eq.typ-bound-y-z}
  \end{enumerate}
\end{lemma}
\begin{proof}
  \textbf{Proposition \ref{eq.typ-bound-z}.}
  \begin{align*}
    Z(S) &< (1 + \epsilon) \E[Z(S)] = (1 + \epsilon) \E[Z_r] |S| \\
         &= \E[Z_r] |S| + \epsilon \E[Z_r] |S|\\
         &< \frac{t}{n - t} \cdot \frac{f}{1 - f} \cdot \frac{|S|}{\ln2} + \epsilon \frac{t}{n - t} \cdot \frac{f}{1 - f} \cdot \frac{|S|}{\ln2} \\
         &< \frac{t}{n - t} \cdot \frac{f}{1 - f} \cdot \frac{|S|}{\ln2} + \epsilon f \frac{|S|}{\ln2} \\
         &= \left(\frac{t}{n - t} \cdot \frac{1}{1 - f} + \epsilon \right) f \frac{|S|}{\ln2}
         \leq \left(1 - \frac{2 \delta}{3}\right) f \frac{|S|}{\ln2}\,.
  \end{align*}

  The first relation follows from Definition~\ref{def:typicality} Eq.~\ref{eq.typical-z},
  the second from the independence of $Z_r$, the fourth from
  the bound in Lemma~\ref{lem:expectation-bounds} Eq.~\ref{eq.ex-z-bound},
  the fifth and the last from the bounds in~\cite[Section 13.2.2]{blockchain-foundations}.

  \textbf{Proposition \ref{eq.typ-bound-z-x}.}
  $
    Z(S) < \frac{t}{n - t} \cdot \frac{f}{1 - f} \cdot \frac{|S|}{\ln2} + \epsilon f \frac{|S|}{\ln2}
        %  &< \left(1 + \frac{\delta}{2}\right) \cdot \frac{t}{n - t} \cdot f \frac{|S|}{\ln2} + \epsilon f \frac{|S|}{\ln2}\\
        %  &= \left(1 + \frac{\delta}{2}\right) \cdot \frac{t}{n - t} \E[\underbar{X}(S)] + \epsilon f \frac{|S|}{\ln2}\\
         < \left(1 + \frac{\delta}{2}\right) \cdot \frac{t}{n - t} X(S) + \frac{\epsilon f |S|}{\ln2}
  $.
  \atnote{Do the math instead of citing backbone.}
  The first relation follows from part~(\ref{eq.typ-bound-z}) of this proof,
  and the second from the bound in \cite[Lemma 11(c)]{backbone}.

  \textbf{Proposition \ref{eq.typ-bound-y-z}.}
  $Y(S) > (1 - \epsilon)\E[Y(S)]
         > \left(1 - \frac{\delta}{3}\right) f \frac{|S|}{\ln2}
         > \left(1 - \frac{2\delta}{3}\right) f \frac{|S|}{\ln2}
         > Z(S)$.
  The first inequality follows from Definition~\ref{def:typicality} Eq.~\ref{eq.typical-y},
  the second from the bound in Lemma~\ref{lem:expectation-bounds} Eq.~\ref{eq.ex-y-bound},
  and the last one from part~(\ref{eq.typ-bound-z}) of this proof.
  \Qed
\end{proof}

% \atnote{Define Chained Work}

\begin{theorem}[Entropic Growth] \label{thm:entropic-growth}
  Typical executions of \poem satisfy the Entropic Growth property
  with $s = \lambda$ and $\tau = (1 - \epsilon)\frac{f}{\ln2}$.
\end{theorem}
\begin{proof}
  Consider a typical \poem execution in which an honest party has a chain $C_1$
  at round $r_1$ and adopts a chain $C_2$ at round $r_2 \geq r_1 + s$.
  Let $S = \{r_1, \ldots, r_2 - 1\}$. Then $|S| \geq s = \lambda$ and,
  applying Definition~\ref{def:typicality} we obtain $X(S) > (1 - \epsilon)\E[\underline{X}(S)]$.
  By
  Lemma~\ref{lem:expectation-bounds}, $\E[\underline{X}(S)] \geq \frac{f}{\ln2}|S|$.
  Hence, $X(S) > (1 - \epsilon)\frac{f}{\ln2}|S|$.
  By Lemma~\ref{lem:chain-growth}, $\rwork(C_2) \geq \rwork(C_1) + X(S)$, as desired.
  \Qed
\end{proof}

\begin{lemma}[Entropic Patience] \label{lem:patience}
  In a typical execution, any chained real work $k \geq 2 \lambda \frac{f}{1 - f} \frac{1}{\ln2} + 8$ is computed
  in more than $\frac{k - 8}{2 \frac{f}{1 - f} \frac{1}{\ln2}} \geq \lambda$ consecutive rounds.
\end{lemma}
\begin{proof}
  Assume, towards a contradiction, there is a set of consecutive rounds $S'$ in which
  the chained real work $k$ was computed and $|S'| \leq \frac{k - 8}{2 \frac{f}{1 - f} \frac{1}{\ln2}}$.
  It holds that $X(S') + Z(S') \geq k$.
  Then, there is a set $S \supseteq S'$ of consecutive rounds with
  $|S| = \ceil*{\frac{k - 8}{2 \frac{f}{1 - f} \frac{1}{\ln2}}} + 1 < \frac{k - 8}{2 \frac{f}{1 - f} \frac{1}{\ln2}} + 2$
  such that $X(S) + Z(S) \geq X(S') + Z(S') \geq k$. However,
  because $|S| > \lambda$, typicality applies and from Lemma~\ref{lem:typical-bounds} we obtain
  $X(S) < (1 + \epsilon) \E[\overline{X}(S)] \leq (1 + \epsilon) \E[\overline{X}_r] |S| <
  (1 + \epsilon) \frac{f}{1 - f} \frac{|S|}{\ln2}$
  and
  $Z(S) < (1 + \epsilon) \E[Z(S)] \leq (1 + \epsilon) \E[Z_r] |S| <
  (1 + \epsilon) \frac{t}{n - t} \frac{f}{1 - f}\frac{|S|}{\ln2} <
  (1 + \epsilon) (1 - \delta) \frac{f}{1 - f}\frac{|S|}{\ln2}$.
  Hence,
  \begin{align*}
    X(S) + Z(S) < (1 + \epsilon) \frac{f}{1 - f} \frac{|S|}{\ln2} (1 + 1 - \delta) <
    2 \frac{f}{1 - f} \frac{|S|}{\ln2} <\\
    2\frac{k - 8}{2 \frac{f}{1 - f} \frac{1}{\ln2}} \frac{f}{1 - f} \frac{1}{\ln2} + 4 \frac{f}{1 - f} \frac{1}{\ln2} =\\
    k - 8 + 4 \frac{f}{1 - f} \frac{1}{\ln2} = k - 4 \left(2 - \frac{f}{1 - f} \frac{1}{\ln2}\right) < k\,.
  \end{align*}
  The second inequality follows from the fact that $\epsilon =\frac{\delta}{6} \Rightarrow (1 + \epsilon)(2 - \delta) < 2$.
  The last inequality follows from $f < \frac{1}{2} \Rightarrow 2 - \frac{f}{1 - f} \frac{1}{\ln2} < 0$.
  \Qed
\end{proof}

\begin{corollary} \label{cor:slicing-work-bound}
  In a typical execution of \poem, for any honest party $P$ and any round $r$ it holds that
  $\rwork([{:}{-k}] \rlhd \Chain[P][][r]) < 2k$.
\end{corollary}
\begin{proof}
  From Entropic Patience (Lemma~\ref{lem:patience}), every block has less than $k$ real work. Therefore,
  $\rwork([-k] \rlhd \Chain[P][][r]) < k$.
  From the definition of the slicing notation ($[{:}]\rlhd$)
  it holds that $\rwork(([-k{:}] \rlhd \Chain[P][][r])[1{:}]) \leq k$. Summing the two constituents,
  we obtain
  \begin{align*}
    \rwork([-k{:}] \rlhd \Chain[P][][r]) =\\
    \rwork(([-k{:}] \rlhd \Chain[P][][r])[1{:}]) + \rwork([-k] \rlhd \Chain[P][][r]) < 2k\,.
  \end{align*}
  \Qed
\end{proof}

\begin{lemma}[Entropic Common Prefix Lemma] \label{lem:common-prefix-lemma}
  For all rounds $r$, and all honest parties $P_1, P_2$, where $P_1$ has $C_1$ and $P_2$ adopts $C_2$ at round $r$
  of a typical PoEM execution, it holds that $[{:}{-k}] \rlhd C_1 \preccurlyeq C_2$ and $[{:}{-k}] \rlhd C_2 \preccurlyeq C_1$
  for $k = 2 \lambda \frac{f}{1 - f} \frac{1}{\ln2} + 8$.
\end{lemma}
\begin{proof}
  Consider an execution as in the statement and suppose,
  towards a contradiction, that $[{:}{-k}] \rlhd C_1 \not \preccurlyeq C_2$
  or $[{:}{-k}] \rlhd C_2 \not \preccurlyeq C_1$.
  Consider the last block $B^*$ with index $i^*$ on the common prefix of
  $C_1$ and $C_2$ that was computed by an honest party and let $r^*$
  be the round at which it was computed; if no such block exists let $r^* = 0$.
  Define the set of rounds $S = \{i: r^* < i < r\}$. We claim that
  $Z(S) \geq Y(S)$.

  We show this by pairing all real work of blocks computed by honest parties during
  convergence opportunities in $S$ with adversarial real work computed during $S$.
  Let $\mathcal{Y}(S)$ be the set of honestly produced blocks in convergence opportunities
  during $S$, and $\Xi = \bigcup \{I(B): B \in \mathcal{Y}(S)\}$.

  Note that, if $\Xi \neq \emptyset$, then $\inf{\Xi} \geq \max{I(B^*)}$
  because the chain ending in block $B^*$
  was diffused at round $r^*$, and all honestly produced blocks after round $r^*$
  are extending a chain with greater or equal real work.
  Also note that $\rwork(C_1) \geq \max{\Xi}$ and $\rwork(C_2) \geq \max{\Xi}$ because
  the honest party that computed the chain with work $\max \Xi$ diffused it and any chain adopted
  by honest parties at any later round should have at least $\max \Xi$ work. % TODO: this is real work, but parties are adopting based on approximate work. Need to use Hash Separation.
  \atnote{Why is $\work(C_1) \geq \max \Xi$?}
  \dznote{I believe this was a mistake in Backbone.}
  Hence, for every $\xi \in \Xi$ it holds that
  $[\xi] \rlhd C_1 \neq \bot$ and $[\xi] \rlhd C_2 \neq \bot$.

  We now argue that for every $\xi \in \Xi$ either block $[\xi] \rlhd C_1$
  or block $[\xi] \rlhd C_2$ is adversarial. If the block lies on the
  common prefix of $C_1$ and $C_2$, namely $[\xi] \rlhd C_1 = [\xi] \rlhd C_2$,
  then it is adversarial by the definition of $B^*$. Otherwise,
  there is one block in $C_1$ and another one in $C_2$, and by
  Lemma~\ref{lem:pairing}, it holds that $[\xi] \rlhd C_1$ and
  $[\xi] \rlhd C_2$ cannot both be honest.
  This completes the proof of the claim $Z(S) \geq Y(S)$.

  All the chained real work $\max(\rwork(C_1[{i^*} {:}]), \rwork(C_2[{i^*} {:}])) \geq k$
  was produced during $S \cup \{r^*\}$.
  Hence, from Lemma~\ref{lem:patience}, $|S \cup \{r^*\}| > \lambda \Rightarrow |S| \geq \lambda$ and
  the properties of a typical execution apply.
  Therefore, by Lemma~\ref{lem:typical-bounds},
  $Z(S) < Y(S)$ which contradicts the previous claim. \Qed
\end{proof}

\begin{theorem}[Entropic Common Prefix] \label{thm:common-prefix}
  Typical executions of \poem satisfy Entropic Common Prefix
  with $k = 2 \lambda \frac{f}{1 - f} \frac{1}{\ln2} + 8$.
\end{theorem}
\begin{proof}
  Consider a typical execution and suppose, towards a contradiction, that Common
  Prefix is violated, and let $r_2$ be the first round during which it is violated.
  At $r_2$ there is an honest party $P_2$ who adopts chain $C_2$
  inconsistent with the chain $C_1$ adopted by an honest party
  $P_1$ at a round $r_1 \leq r_2$, namely $[{:}{-k}] \rlhd C_1 \not\preceq C_2$.

  % TODO: Change algorithm so that has r => adopts r + 1
  \noindent
  \textbf{Case $r_1 < r_2$.}
  At round $r_2$, party $P_1$ has a chain $C$,
  which it adopted at $r_2 - 1$ (not excluding the case
  where $C = C_1$). It holds that $[{:}{-k}] \rlhd C_1 \preceq C$
  due to the minimality of $r_2$ (otherwise, the Common Prefix virtue would
  have been broken at $r_2 - 1$ by chains $C_1$ and $C$).
  Furthermore, $\rwork(C) \geq \rwork(C_1)$ due to the heaviest chain
  rule followed by $P_1$. % TODO: Hash Separation needed for this part?
  Therefore, $[{:}{-k}] \rlhd C_1 \preceq [{:}{-k}] \rlhd C$.
  By the Common Prefix lemma, we have $[{:}{-k}] \rlhd C \preceq C_2$
  (at $r_2$, party $P_1$ has $C$ and party $P_2$ adopts $C_2$).
  By transitivity of $\preceq$, we have $[{:}{-k}] \rlhd C_1 \preceq C_2$,
  which contradicts the violation of Common Prefix.

  \noindent
  \textbf{Case $r_1 = r_2$.}
  Let $C$ be the chain that $P_1$ adopts at $r_1 + 1$ (not excluding the case
  where $C = C_1$).
  By the Common Prefix lemma, we have that
  $[{:}{-k}] \rlhd C_1 \preceq C$ (at $r_1 + 1$, party $P_1$ adopts $C$ and has $C_1$).
  Furthermore, $\rwork(C) \geq \rwork(C_1)$ due to the heaviest chain
  rule followed by $P_1$. % TODO: Hash Separation is needed here too?
  Because $\rwork(C) \geq \rwork(C_1)$, therefore $[{:}{-k}] \rlhd C_1 \preceq [{:}{-k}] \rlhd C$.
  By the Common Prefix lemma, we have that
  $[{:}{-k}] \rlhd C \preceq C_2$ (at $r_1 + 1$, party $P_1$ adopts $C$ and party $P_2$ has $C_2$).
  By transitivity of $\preceq$, we have $[{:}{-k}] \rlhd C_1 \preceq C_2$,
  which contradicts the violation of Common Prefix.
  \Qed
\end{proof}

\begin{theorem}[Entropic Quality] \label{thm:entoropic-quality}
  Typical executions of \poem satisfy the Entropic Quality property
  with $\ell = 2 \lambda \frac{f}{1 - f} \frac{1}{\ln2} + 8$ and
  $\mu = 1 - (1 + \frac{\delta}{2})\frac{t}{n - t} - \frac{\epsilon}{1 - \epsilon}$.
\end{theorem}
\begin{proof}
  Suppose, towards a contradiction, that there is a chain quality violation in a typical
  \poem execution. Then there is an honest party $P$ who adopts a chain $C_3$
  at round $r$ for which chain quality is violated.
  This means there are $u, v$ such that the chain $C_1 = C_3[u{:}v]$
  has $\rwork(C_1) \geq \ell$ and quality lower than $\mu$, namely
  the sum $x$ of works of all honestly generated blocks in $C_1$ is less than
  $\mu \rwork(C_1)$.
  Consider the minimum real work chain $C_2 = C_3[{u'}{:}{v'}]$
  such that $C_1$ is fully included in $C_2$ (i.e., $u' \leq u$ and $v' \geq v$)
  with the following properties:

  \begin{enumerate}
    \item $C_3[u']$ was computed by an honest party $P_1$ (this will exist because $C_3[0]$ is the genesis block, which is honestly generated) at some round $r_1$ (letting $r_1 = 0$ if $u' = 0$).
    \item $C_3[v']$ was the tip of the adopted chain by an honest party $P_2$ at some round $r_2$ (this will exist because $P$ adopts $C_3$).
  \end{enumerate}

  Let $L = \rwork(C_2)$ and $S = \{r_1, \ldots, r_2 - 1\}$. Note that, by causality,
  all the work $L$ was computed in $S$. By the supposition, we have
  $x < \mu \ell \leq \mu L$.

  We have that $Z(S) \geq L - x$. To see this, observe that, by the minimality of $C_2$, all the blocks
  with heights $u', \ldots, u$ as well as the blocks with heights $v, \ldots, v'$ were computed by the adversary, and so the only honest real work computed within $L$ is $x$.

  Additionally, $L \geq X(S)$. To see this, note that at round $r_1$, party $P_1$ produced $C_3[u']$,
  and so every honest party adopts a chain of real work at least $\rwork(C_3[{u'}{:}])$ from round $r_1 + 1$
  onwards. % TODO: Hash Separation is needed to make this argument
  Therefore, by Lemma~\ref{lem:chain-growth}, at round $r_2$, every honest party adopts a chain of real work at least $\rwork(C_3[{u'}{:}]) + X(S)$. But we know that $P_2$ adopts a chain
  of real work $\rwork(C_3[{u'}{:}]) + L$, and so $L \geq X(S)$.

  Therefore,
  \[
    Z(S) \geq L - x > (1 - \mu)L \geq (1 - \mu)X(S) \geq ((1 + \frac{\delta}{2})\cdot\frac{t}{n - t} + \frac{\epsilon}{1 - \epsilon})X(S)\,.
  \]

  The last inequality follows from replacing the value of $\mu$ from the statement.
  By Lemma~\ref{lem:patience}, $|S| > \lambda$ and typical bounds apply. Therefore,
  $X(S) > (1 - \epsilon)\E[\underline{X}(S)] = (1 - \epsilon)\frac{f}{\ln2}$ and,
  from this and the previous inequality,
  $Z(S) \geq (1 + \frac{\delta}{2})\cdot\frac{t}{n - t}X(S) + \epsilon f \frac{|S|}{\ln2}$.
  However, this contradicts the bound in Lemma~\ref{lem:typical-bounds}.
  \Qed
\end{proof}

\begin{lemma}[Confirmation Separation] \label{lem:confirmation-separation}
  For any function $k = k(\kappa)$, it holds that, in a PoEM execution,
  $\Pr[\exists C: [{:}{-k}] \rlhd C \neq [{:}{-k}] \lhd C]$
  is negligible in $\kappa$.
\end{lemma}
\begin{proof}
  Consider the event that there exists a \emph{chain} $C$ with
  $[{:}{-k}] \rlhd C \neq [{:}{-k}] \lhd C$. Since the prefixes
  differ, the suffixes must also differ, namely
  $[{-k}{:}] \rlhd C \neq [{-k}{:}] \lhd C$.
  Let $C^* = [{-k}{:}] \lhd C$.
  By the slicing notation, it directly follows that $\work(C^*) \geq k$.
  Additionally, we observe that $k > \rwork(C^*)$
  (otherwise, $[{-k}{:}] \rlhd C = [{-k}{:}] \lhd C$).
  % TODO: Add figure
  Define $\borderline$ the bad event that there exists some subchain $C^*$
  in the execution such that $\work(C^*) \geq k > \rwork(C^*)$.
  We have shown that $\exists C: [{:}{-k}] \rlhd C \neq [{:}{-k}] \lhd C \rightarrow \borderline$.

  It suffices to show that $\Pr[\borderline]$ is negligible.

  Let $E_1$ be the event that there exists a subchain $C^*$ such that
  $\work(C^*) - \rwork(C^*) \geq Lqn2^{−\kappa/2}$, and let $p_1 = \Pr[E_1]$.
  Let $E_2$ be the event that there exists a subchain $C^*$ such that
  $k - Lqn2^{\kappa/2} \leq \rwork(C^*) < k$, and let $p_2 = \Pr[E_2]$.
  We observe that $\lnot E_1 \land \lnot E_2 \rightarrow \lnot \borderline$,
  hence $\borderline \rightarrow E_1 \lor E_2$.
  Therefore, from the union bound, we have
  \[
  \Pr[E_1] + \Pr[E_2] = p_1 + p_2 \geq \Pr[E_1 \lor E_2] \geq \Pr[\borderline]\~.
  \]

  From Corollary~\ref{cor:chain-work-approximation}, we have that
  $p_1$ is negligible.

  Let us calculate the probability $p_2$. Consider all the, at most $(nqL)^2$, subchains
  $C^*_1, C^*_2, \ldots, C^*_{(nqL)^2}$ appearing in an execution, and consider an aribtrary
  subchain $C^*_i$ among them. Because the work of each
  block $B$ in $C^*_i$ is distributed as $\Exp(\ln2)$,
  the points $(\rwork(C^*_i[{:}{1}]), \rwork(C^*_i[{:}{2}]), \ldots, \rwork(C^*_i))$
  correspond to the initial $\rwork(C^*_i)$ segment of a Poisson stochastic
  process with rate $\ln2$ (do not
  confuse the \emph{work} between blocks, which exactly follows a Poisson process with rate $\ln2$,
  and the \emph{time} between consecutive block generation).
  We are interested in the number of Poisson points that fall within the interval
  $[k - Lqn2^{-\kappa/2}, k)$. This is a random variable distributed as a Poisson
  distribution with rate $Lqn2^{-\kappa/2} \lambda$. Let $F_i$ be the bad event that
  the number of points of the process corresponding to the subchain $C^*_i$ that fall
  within the interval $[k - Lqn2^{-\kappa/2}, k)$ is at least one.
  Using the probability mass function of the Poisson distribution evaluated at $0$
  we have $\Pr[F_i] = 1 - \Pr[\lnot F_i] = 1 - e^{-\lambda Lqn2^{-\kappa/2}}
  = 1 - 2^{-(\lg e) \lambda Lqn2^{-\kappa/2}} < (\lg e) \lambda Lqn2^{-\kappa/2}$,
  where the last inequality follows from Lemma~\ref{lem:bernoulli}.
  Taking a union bound over all subchains, we have
  $p_2 = \Pr[E_2] = \Pr[\bigcup_{i=1}^{(nqL)^2}F_i] \leq \sum_{i = 1}^{(nqL)^2}\Pr[F_i] = (nqL)^2 \Pr[F_i] < (nqL)^3 (\lg e) \lambda 2^{-\kappa/2}$
  which is negligible. Therefore, $\Pr[\borderline]$ is negligible.
  \Qed
\end{proof}


\restateSafety*
\begin{proof}
  Consider any two honest parties $P_1, P_2$ and
  any rounds $r_1, r_2$. Let $C_1, C_2$ be the chains that $P_1, P_2$
  adopt at rounds $r_1, r_2$ respectively.
  From Entropic Common Prefix (Theorem~\ref{thm:common-prefix}), it follows that
  if $r_1 \leq r_2$, then $[{:}{-k}] \rlhd C_1 \preccurlyeq C_2$; and
  if $r_2 \leq r_1$, then $[{:}{-k}] \rlhd C_2 \preccurlyeq C_1$.
  In both cases, it follows that $[{:}{-k}] \rlhd C_1 \sim [{:}{-k}] \rlhd C_2$.
  From Confirmation Separation (Lemma~\ref{lem:confirmation-separation}),
  it follows that $[{:}{-k}] \lhd C_1 \sim [{:}{-k}] \lhd C_2$.
  Therefore, for the ledgers $\Ledger[P_1][][r_1], \Ledger[P_2][][r_2]$ returned when
  \lread is invoked on parties $P_1, P_2$ after rounds $r_1, r_2$ respectively,
  % TODO: \lread uses \lhd, not \rlhd; a Hash Separation is needed
  it holds that $\Ledger[P_1][][r_1] \sim \Ledger[P_2][][r_2]$.
\end{proof}

\restateLiveness*
\begin{proof}
  Consider any round $r$.
  Because $u \geq s$, invoking Entropic Growth($s, \tau$) (Theorem~\ref{thm:entropic-growth}), we conclude that
  for all honest parties $P$ and all rounds $r' \geq r + u$, it holds that
  $\rwork(\Chain[P][][r'][|\Chain[P][][r]|{:}]) \geq u \tau \geq \ell + 2k$.
  From Corollary~\ref{cor:slicing-work-bound}, it follows that
  $\rwork([{:}{-k}] \rlhd \Chain[P][][r'][|\Chain[P][][r]|{:}]) \geq \ell$.
  Invoking Entropic Quality (Theorem~\ref{thm:entoropic-quality}),
  it holds that in the chain segment $[{:}{-k}] \rlhd \Chain[P][][r'][|\Chain[P][][r]|{:}]$,
  there is at least one honestly generated block that was produced after round $r$.

  Now, consider that an honest party attempts to inject a transaction \tx
  at round $r$. At the beginning of round $r + 1$, all honest parties
  receive \tx and include it in their mempool~\cite[Section 5.7]{blockchain-foundations}.
  Hence, all honest blocks produced
  after round $r$ will either include, or extend a chain that includes transaction \tx.
  Because of this and the above, for all honest parties $P$ and rounds $r' \geq r + u$,
  we conclude that $\tx \in \Ledger[P][][r']$.
  \Qed
\end{proof}

\restateSecurity*
\begin{proof}
  Executions are typical with overwhelming probability (Theorem~\ref{thm:typicality}).
  Typical executions are safe (Theorem~\ref{thm:safety}), and live (Theorem~\ref{thm:liveness}), from which
  security follows.
  \Qed
\end{proof}