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}}
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$ and the protocol parameters $\var{pp}$. 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 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 (\Seed\times\Seed\times\Seed)
+
               \times \Slot
+
               \times (\Seed\times\Seed\times\Seed)
+
              )
  \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 \var{s} is the first slot
+
of an epoch, 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.

                      
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).

                      
\begin{figure}[ht]
+
   \begin{equation}\label{eq:update-all}
+
    \inference[Update-All]
+
    {
+
      s = \firstSlot{(\epoch{s})}
+
    }
+
    {
+
      {\begin{array}{c}
+
         \eta \\
+
         \var{pp}
+
       \end{array}}
+
      \vdash
+
      {\left(\begin{array}{c}
+
            \eta_0 \\
+
            \eta_v \\
+
            \eta_c \\
+
      \end{array}\right)}
+
      \trans{updn}{\var{s}}
+
      {\left(\begin{array}{c}
+
            \varUpdate{\eta_c \seedOp \fun{extraEntropy}~\var{pp}} \\
+
            \varUpdate{\eta_v\seedOp\eta} \\
+
            \varUpdate{\eta_v\seedOp\eta} \\
+
      \end{array}\right)}
+
    }
+
  \end{equation}
+

                      
+
  \nextdef
+

                      
  \begin{equation}\label{eq:update-both}
    \inference[Update-Both]
    {
+
      s > \firstSlot{(\epoch{s})} \\
      s < \firstSlot{((\epoch{s}) + 1) - \SlotsPrior}