View on GitHub
File Changes
\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}}

                      
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$.
+
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 \PParams)
-
               \times (\Seed\times\Seed\times\Seed)
+
    \powerset ((\Seed \times \PParams \times \Bool)
+
               \times \UpdateNonceState
               \times \Slot
-
               \times (\Seed\times\Seed\times\Seed)
+
               \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
-
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.
+
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]
-
    {
-
      s = \firstSlot{(\epoch{s})}
-
    }
+
    { }
    {
      {\begin{array}{c}
         \eta \\
-
         \var{pp}
+
         \var{pp} \\
+
         \mathsf{True}
       \end{array}}
      \vdash
      {\left(\begin{array}{c}
  \begin{equation}\label{eq:update-both}
    \inference[Update-Both]
    {
-
      s > \firstSlot{(\epoch{s})} \\
      s < \firstSlot{((\epoch{s}) + 1) - \SlotsPrior}
    }
    {
      {\begin{array}{c}
         \eta \\
-
         \var{pp}
+
         \var{pp} \\
+
         \mathsf{False}
       \end{array}}
      \vdash
      {\left(\begin{array}{c}
    {
      {\begin{array}{c}
         \eta \\
-
         \var{pp}
+
         \var{pp} \\
+
         \mathsf{False}
       \end{array}}
      \vdash
      {\left(\begin{array}{c}

                      
The environments for this transition are:
\begin{itemize}
-
  \item The overlay environment $\var{oe}$.
+
  \item The protocol parameters $\var{pp}$.
+
  \item A mapping $\var{osched}$ of slots to an optional genesis key.
+
    In the terminology of \cite{delegation_design},
+
    the slots in $\var{osched}$ are the ``OBFT slots''.
+
    A slot in this map with a value of $\Nothing$ is a non-active slot,
+
    otherwise it is an active slot and its value designates the genesis key
+
    responsible for producing the block.
+
  \item The stake pool stake distribution $\var{pd}$.
+
  \item The mapping $\var{genDelegs}$ of genesis keys to their cold keys.
  \item The current slot (as determined by wall-clock).
+
  \item A marker indicating whether we are in a new epoch $\var{ne}$.
\end{itemize}

                      
The states for this transition consists of:
      {
        {\left(\begin{array}{c}
        \eta \\
-
        \var{pp}
+
        \var{pp} \\
+
        \var{ne}
        \end{array}\right)}
        \vdash
        {\left(\begin{array}{c}
         \var{pd} \\
         \var{dms} \\
         \var{s_{now}} \\
+
         \var{ne}
       \end{array}}
      \vdash
      {\left(\begin{array}{c}

                      
\begin{itemize}
  \item The epoch specific state $\var{nes}$.
+
  \item The epoch nonce $\eta_0$.
  \item The evolving nonce $\eta_v$.
  \item The candidate nonce $\eta_c$.
  \item The last header hash \var{h}.
    \left(
      \begin{array}{[email protected]{~\in~}lr}
        \var{nes} & \NewEpochState & \text{epoch specific state} \\
+
        ~\eta_0 & \Seed & \text{epoch nonce} \\
        ~\eta_v & \Seed & \text{evolving nonce} \\
        ~\eta_c & \Seed & \text{candidate nonce} \\
        \var{h} & \HashHeader & \text{latest header hash} \\
         \end{array}}
        \vdash\var{nes}\trans{\hyperref[fig:rules:bhead]{bhead}}{\var{bh}}\var{nes'}
      } \\~\\
-
      (\wcard,~\wcard,~\var{b_{cur}},~\var{es},~\wcard,~\var{pd},\var{osched})
+
      (\var{e_1},~\wcard,~\wcard,~\wcard,~\wcard,~\wcard,\wcard)
+
        \leteq\var{nes} \\
+
      (\var{e_2},~\wcard,~\var{b_{cur}},~\var{es},~\wcard,~\var{pd},\var{osched})
        \leteq\var{nes'} \\
        (\var{acnt},~\wcard,\var{ls},~\var{pp})\leteq\var{es}\\
        ( \wcard,
          ( (\wcard,~\wcard,~\wcard,~\wcard,~\wcard,~\var{genDelegs}),~
          (\wcard,~\wcard,~\wcard,~\var{cs})))\leteq\var{ls}\\
          (\wcard, reserves) \leteq \var{acnt}\\
+
          \var{ne} \leteq  \var{e_1} \neq \var{e_2}\\
      {
        {\begin{array}{c}
-
           \begin{array}{c}
-
             \var{pp} \\
-
             \var{osched} \\
-
             \var{pd} \\
-
             \var{genDelegs} \\
-
           \end{array}\\
-
           \var{s_{now}} \\
+
            \var{pp} \\
+
            \var{osched} \\
+
            \var{pd} \\
+
            \var{genDelegs} \\
+
            \var{s_{now}} \\
+
            \var{ne}
         \end{array}}
        \vdash
        {\left(\begin{array}{c}
              \var{cs} \\