View on GitHub
File Changes
\newcommand{\bleader}[1]{\fun{bleader}~\var{#1}}
\newcommand{\hBbsize}[1]{\fun{hBbsize}~\var{#1}}
\newcommand{\bbodyhash}[1]{\fun{bbodyhash}~\var{#1}}
-
\newcommand{\overlaySchedule}[4]{\fun{overlaySchedule}~\var{#1}~\var{#2}~{#3}~\var{#4}}
+
\newcommand{\overlaySchedule}[3]{\fun{overlaySchedule}~\var{#1}~\var{#2}~\var{#3}}

                      
\newcommand{\PrtclState}{\type{PrtclState}}
\newcommand{\PrtclEnv}{\type{PrtclEnv}}
\newcommand{\OverlayEnv}{\type{OverlayEnv}}
\newcommand{\VRFState}{\type{VRFState}}
\newcommand{\NewEpochEnv}{\type{NewEpochEnv}}
\newcommand{\NewEpochState}{\type{NewEpochState}}
+
\newcommand{\UpdateNonceState}{\type{UpdateNonceState}}
\newcommand{\PoolDistr}{\type{PoolDistr}}
\newcommand{\BBodyEnv}{\type{BBodyEnv}}
\newcommand{\BBodyState}{\type{BBodyState}}
given in Figure~\ref{fig:ts-types:newepoch}, it consists of

                      
\begin{itemize}
-
\item The epoch nonce.
\item The current slot.
\item The set of genesis keys.
\end{itemize}

                      
\begin{itemize}
\item The number of the last epoch.
-
\item The old epoch nonce.
\item The information about produced blocks for each stake pool during the previous epoch.
\item The information about produced blocks for each stake pool during the current epoch.
\item The old epoch state.
    \NewEpochEnv =
    \left(
      \begin{array}{[email protected]{~\in~}lr}
-
        \eta_1 & \Seed & \text{epoch nonce} \\
        \var{s} & \Slot & \text{current slot} \\
        \var{gkeys} & \powerset{\KeyHashGen} & \text{genesis key hashes} \\
      \end{array}
    \left(
      \begin{array}{[email protected]{~\in~}lr}
        \var{e_\ell} & \Epoch & \text{last epoch} \\
-
        \eta_0 & \Seed & \text{epoch nonce} \\
        \var{b_{prev}} & \BlocksMade & \text{blocks made last epoch} \\
        \var{b_{cur}} & \BlocksMade & \text{blocks made this epoch} \\
        \var{es} & \EpochState & \text{epoch state} \\
  %
  \emph{Abstract pseudorandom schedule function}
  \begin{align*}
-
    & \fun{overlaySchedule} \in \Epoch \to \powerset{\KeyHashGen} \to \Seed \to \PParams
+
    & \fun{overlaySchedule} \in \Epoch \to \powerset{\KeyHashGen} \to \PParams
        \to (\Slot\mapsto\KeyHashGen^?) \\
  \end{align*}
  %
  \emph{Constraints}
  \begin{align*}
-
    \text{ given: }~\var{osched}\leteq\overlaySchedule{e}{gkeys}{\eta}{pp} \\
+
    \text{ given: }~\var{osched}\leteq\overlaySchedule{e}{gkeys}{pp} \\
    \range{osched}\subseteq\var{gkeys} \\
    |\var{osched}| = \floor{(\fun{d}~\var{pp})\cdot\SlotsPerEpoch} \\
    |\{s\mapsto k\in\var{osched}~\mid~k\neq\Nothing\}| =

                      
\begin{itemize}
\item The epoch is set to the new epoch $e$.
-
\item The epoch nonce is replaced with the combination of the new one from the
-
  environment and any extra entropy present in the UTxO state.
\item The mapping for the blocks produced by each stake pool for the previous epoch
  is set to the current such mapping.
\item The mapping for the blocks produced by each stake pool for the current epoch
              \end{array}
            }
            \right\}\\
-
          \var{osched'} & \overlaySchedule{e}{gkeys}{\eta_1}{pp} \\
-
          \eta_e & \fun{extraEntropy}~\var{pp} \\
+
          \var{osched'} & \overlaySchedule{e}{gkeys}{pp} \\
          \var{es''} & (\var{acnt},
                       ~\var{ss},
                       ~\var{ls},
    }
    {
      {\begin{array}{c}
-
         \eta_1 \\
         \var{s} \\
         \var{gkeys} \\
       \end{array}}
      \vdash
      {\left(\begin{array}{c}
            \var{e_\ell} \\
-
            \eta_0 \\
            \var{b_{prev}} \\
            \var{b_{cur}} \\
            \var{es} \\
      \trans{newepoch}{\var{e}}
      {\left(\begin{array}{c}
            \varUpdate{\var{e}} \\
-
            \varUpdate{\eta_1\seedOp\eta_e} \\
            \varUpdate{\var{b_{cur}}} \\
            \varUpdate{\emptyset} \\
            \varUpdate{\var{es}''} \\
    }
    {
      {\begin{array}{c}
-
         \eta_1 \\
         \var{s} \\
         \var{gkeys} \\
       \end{array}}
      \vdash
      {\left(\begin{array}{c}
            \var{e_\ell} \\
-
            \eta_0 \\
            \var{b_{prev}} \\
            \var{b_{cur}} \\
            \var{es} \\
      \trans{newepoch}{\var{e}}
      {\left(\begin{array}{c}
            \var{e_\ell} \\
-
            \eta_0 \\
            \var{b_{prev}} \\
            \var{b_{cur}} \\
            \var{es} \\
\subsection{Update Nonce Transition}
\label{sec:update-nonces-trans}

                      
-
The Update Nonce Transition updates the nonces until the randomness gets
-
fixed. The environment is shown in Figure~\ref{fig:ts-types:updnonce} and
-
consists of the epoch nonce $\eta$. The update nonce state is shown in
-
Figure~\ref{fig:rules:update-nonce} and consists of the candidate nonce
-
$\eta_c$ and the evolving nonce $\eta_v$.
+
The Update Nonce Transition updates the nonces until the randomness gets fixed.
+
The environment is shown in Figure~\ref{fig:ts-types:updnonce} and consists of
+
the block nonce $\eta$, the protocol parameters $\var{pp}$ and a marker
+
$\var{ne}$ determining whether we are in a new epoch. The update nonce state is
+
shown in Figure~\ref{fig:rules:update-nonce} and consists of the epoch nonce
+
$\eta_0$, the candidate nonce $\eta_c$ and the evolving nonce $\eta_v$.

                      
\begin{figure}
+
  \emph{Update Nonce states}
+
  \begin{equation*}
+
    \UpdateNonceState =
+
    \left(
+
      \begin{array}{[email protected]{~\in~}lr}
+
        \eta_0 & \Seed & \text{epoch nonce} \\
+
        \eta_c & \Seed & \text{candidate nonce} \\
+
        \eta_v & \Seed & \text{evolving nonce} \\
+
      \end{array}
+
    \right)
+
  \end{equation*}
+
  %
  \emph{Update Nonce Transitions}
  \begin{equation*}
    \_ \vdash \var{\_} \trans{updn}{\_} \var{\_} \subseteq
-
    \powerset (\Seed \times (\Seed\times\Seed) \times \Slot \times (\Seed\times\Seed))
+
    \powerset ((\Seed \times \PParams \times \Bool)
+
               \times \UpdateNonceState
+
               \times \Slot
+
               \times \UpdateNonceState
+
              )
  \end{equation*}
  \caption{UpdNonce transition-system types}
  \label{fig:ts-types:updnonce}
\end{figure}

                      
-
The transition rule $\mathsf{UPDN}$ takes the slot \var{s} as signal.
-
There are two different cases for $\mathsf{UPDN}$, one where \var{s} is not yet
-
\SlotsPrior{} slots from the beginning of the next epoch and one where \var{s} is at least
-
\SlotsPrior{} slots after the first slot of the epoch.
+
The transition rule $\mathsf{UPDN}$ takes the slot \var{s} as signal. There are
+
three different cases for $\mathsf{UPDN}$: one where we are in a new epoch, one
+
where \var{s} is not yet \SlotsPrior{} slots from the beginning of the next
+
epoch and one where \var{s} is less than \SlotsPrior{} slots until the start of
+
the next epoch.
+

                      
+
This does assume that the first block in an epoch will occur before
+
\SlotsPrior{} slots before the beginning of the next epoch.

                      
Note that in \ref{eq:update-both}, the nonce candidate $\eta_c$ transitions to
-
$\eta_v\star\eta$, not $\eta_c\star\eta$. The reason for this is that even though the nonce
-
candidate is frozen sometime during the epoch, we want the two nonces to again be equal at the
-
start of a new epoch (so that the entropy added near the end of the epoch is not discarded).
+
$\eta_v\star\eta$, not $\eta_c\star\eta$. The reason for this is that even
+
though the nonce candidate is frozen sometime during the epoch, we want the two
+
nonces to again be equal at the start of a new epoch (so that the entropy added
+
near the end of the epoch is not discarded).

                      
\begin{figure}[ht]
+
   \begin{equation}\label{eq:update-all}
+
    \inference[Update-All]
+
    { }
+
    {