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

                      
+
\newcommand{\OCertEnv}{\type{OCertEnv}}
\newcommand{\PrtclState}{\type{PrtclState}}
\newcommand{\PrtclEnv}{\type{PrtclEnv}}
\newcommand{\OverlayEnv}{\type{OverlayEnv}}
\subsection{Operational Certificate Transition}
\label{sec:oper-cert-trans}

                      
-
The Operational Certificate Transition contains no environments, and its state is the mapping of
-
operation certificate issue numbers.  Its signal is a block header.
+
The Operational Certificate Transition environment consists of the genesis key
+
delegation map $\var{genDelegs}$ and the set of stake pools $\var{stpools}$. Its state
+
is the mapping of operation certificate issue numbers.  Its signal is a block
+
header.

                      
\begin{figure}
+
  \emph{Operational Certificate environments}
+
  \begin{equation*}
+
    \OCertEnv =
+
    \left(
+
      \begin{array}{[email protected]{~\in~}lr}
+
        \var{stpools} & \powerset{\type{KeyHash}} & \text{stake pools} \\
+
        \var{genDelegs} & \powerset{\type{KeyHash}} & \text{genesis key delegates}\\
+
      \end{array}
+
    \right)
+
  \end{equation*}
+
  %
  \emph{Operational Certificate Transitions}
  \begin{equation*}
-
    \vdash \var{\_} \trans{ocert}{\_} \var{\_} \subseteq
-
    \powerset (\KeyHash_{pool} \mapsto \N \times \BHeader \times \KeyHash_{pool} \mapsto \N)
+
    \var{\_} \vdash \var{\_} \trans{ocert}{\_} \var{\_} \subseteq
+
    \powerset (\OCertEnv \times \KeyHash_{pool} \mapsto \N \times \BHeader \times \KeyHash_{pool} \mapsto \N)
  \end{equation*}
+
  %
+
  \emph{Operational Certificate helper function}
+
  \begin{align*}
+
      & \fun{currentIssueNo} \in \OCertEnv \to (\KeyHash_{pool} \to \N)
+
                                           \to \KeyHash_{pool}
+
                                           \to \N^? \\
+
      & \fun{currentIssueNo}~(\var{stpools}, \var{genDelegs})~ \var{cs} ~\var{hk} \\
+
      & \begin{array}{ccl}
+
        ~~~~ & | & \var{hk}\mapsto \var{n} \in \var{cs} = n \\
+
        ~~~~ & | & \var{hk} \in \var{stpools} = 0 \\
+
        ~~~~ & | & \var{hk} \in \var{genDelegs} = 0 \\
+
        ~~~~ & | & \text{otherwise} = \Nothing
+
      \end{array}
+
  \end{align*}
  \caption{OCert transition-system types}
  \label{fig:ts-types:ocert}
\end{figure}
      \\~\\
      c_0 \leq \kesPeriod{s} < c_0 + \MaxKESEvo
      \\
-
      \var{hk}\mapsto m\in\var{cs}
+
      \fun{currentIssueNo} ~ \var{oce} ~ \var{cs} ~ \var{hk} = m
      &
      m \leq n
      \\~\\
      \\
    }
    {
-
      \vdash\var{cs}
+
      \var{oce}\vdash\var{cs}
      \trans{ocert}{\var{bh}}\varUpdate{\var{cs}\unionoverrideRight\{\var{hk}\mapsto n\}}
    }
  \end{equation}
      \var{gkh}\mapsto\var{vkh}\in\var{genDelegs}
      \\~\\
      {
+
        {\begin{array}{c}
+
         \dom \var{pd} \\
+
         \dom \var{genDelegs} \\
+
         \end{array}
+
        }
        \vdash\var{cs}\trans{\hyperref[fig:rules:ocert]{ocert}}{\var{bh}}\var{cs'}
      }
    }

                      
\begin{itemize}
  \item The epoch specific state $\var{nes}$.
+
  \item The operational certificate issue number map $\var{cs}$.
  \item The epoch nonce $\eta_0$.
  \item The evolving nonce $\eta_v$.
  \item The candidate nonce $\eta_c$.
    \left(
      \begin{array}{[email protected]{~\in~}lr}
        \var{nes} & \NewEpochState & \text{epoch specific state} \\
+
        \var{cs} & \KeyHash_{pool} \mapsto \N & \text{operaional certificate issue numbers} \\
        ~\eta_0 & \Seed & \text{epoch nonce} \\
        ~\eta_v & \Seed & \text{evolving nonce} \\
        ~\eta_c & \Seed & \text{candidate nonce} \\
      \end{array}
  \end{align*}
  %
-
  \begin{align*}
-
      & \fun{setIssueNumbers} \in \LState \to (\KeyHash_{pool}\to\N) \to \LState \\
-
      & \fun{setIssueNumbers}~
-
          (\var{utxoSt},
-
          ~(\var{dstate},~(\var{stpools},~\var{poolParams},~\var{retiring},~\wcard)))
-
          ~\var{cs} = \\
-
      & ~~~~
-
          (\var{utxoSt},
-
          ~(\var{dstate},~(\var{stpools},~\var{poolParams},~\var{retiring},~\var{cs})))
-
  \end{align*}
-
  %
  \begin{align*}
      & \fun{updateNES} \in \NewEpochState \to \BlocksMade \to \LState \to \NewEpochState \\
      & \fun{updateNES}~
        (\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,~\wcard,~\wcard)))\leteq\var{ls}\\
          (\wcard, reserves) \leteq \var{acnt}\\
          \var{ne} \leteq  \var{e_1} \neq \var{e_2}\\
      {
              \eta_c' \\
        \end{array}\right)}
      } \\~\\~\\
-
      \var{ls'}\leteq\fun{setIssueNumbers}~\var{ls}~\var{cs'} \\~\\
      {
        {\begin{array}{c}
                 \dom{osched} \\
        \end{array}}
        \vdash
        {\left(\begin{array}{c}
-
              \var{ls}' \\
+
              \var{ls} \\
              \var{b_{cur}} \\
        \end{array}\right)}
        \trans{\hyperref[fig:rules:bbody]{bbody}}{\var{block}}
        {\left(\begin{array}{c}
-
              \var{ls}'' \\
+
              \var{ls}' \\
              \var{b_{cur}'} \\
        \end{array}\right)}
      }\\~\\
-
      \var{nes''}\leteq\fun{updateNES}~\var{nes'}~\var{b_{cur}'},~\var{ls''} \\
+
      \var{nes''}\leteq\fun{updateNES}~\var{nes'}~\var{b_{cur}'},~\var{ls'} \\
    }
    {
      \var{s_{now}}
      \vdash
      {\left(\begin{array}{c}
            \var{nes} \\
+
            \var{cs} \\
            \eta_0 \\
            \eta_v \\
            \eta_c \\
      \trans{chain}{\var{block}}
      {\left(\begin{array}{c}
            \varUpdate{\var{nes}''} \\
+
            \varUpdate{\var{cs}'} \\
            \varUpdate{\eta_0'} \\
            \varUpdate{\eta_v'} \\
            \varUpdate{\eta_c'} \\
        their costs and margin.
      \item $\var{retiring}$ tracks stake pool retirements, using a map from hashkeys to
        the epoch in which it will retire.
-
      \item $\var{cs}$ stores the latest operational certificate issues numbers used for each pool.
-
        The numbers are used in the operation certificate transition
-
        in Figure~\ref{fig:rules:ocert}.
    \end{itemize}
\end{itemize}

                      
      \var{poolParams} & \KeyHash_{pool} \mapsto \PoolParam
        & \text{registered pools to pool parameters}\\
      \var{retiring} & \KeyHash_{pool} \mapsto \Epoch & \text{retiring stake pools}\\
-
      \var{cs} & \KeyHash_{pool} \mapsto \N & \text{certificate issue numbers}\\
    \end{array}\right)
    \end{array}
  \end{equation*}
    \begin{itemize}
      \item The key is added to the set of registered stake pools.
      \item The pool's parameters are stored.
-
      \item The pool's operational certificate counter is set to zero.
    \end{itemize}
  \item Stake pool parameter updates are handled by \cref{eq:pool-rereg}.
    This rule, which also matches on the certificate type $\type{DCertRegPool}$,
        \var{stpools} \\
        \var{poolParams} \\
        \var{retiring} \\
-
        \var{cs} \\
      \end{array}
      \right)
      \trans{pool}{c}
        \varUpdate{\var{poolParams}} & \varUpdate{\union}
                                    & \varUpdate{\{\var{hk} \mapsto \poolParam{c}\}} \\
       \var{retiring} \\
-
       \varUpdate{\var{cs}} & \varUpdate{\union}
-
                            & \varUpdate{\{\var{hk} \mapsto 0\}} \\
      \end{array}
      \right)
    }
        \var{stpools} \\
        \var{poolParams} \\
        \var{retiring} \\
-
        \var{cs} \\
      \end{array}
      \right)
      \trans{pool}{c}
        \varUpdate{\var{poolParams}} & \varUpdate{\unionoverrideRight}
                                  & \varUpdate{\{\var{hk} \mapsto \poolParam{c}\}}\\
        \varUpdate{\{\var{hk}\}} & \varUpdate{\subtractdom} & \varUpdate{\var{retiring}} \\
-
        \var{cs} \\
      \end{array}
      \right)
    }
        \var{stpools} \\
        \var{poolParams} \\
        \var{retiring} \\
-
        \var{cs} \\
      \end{array}
    \right)
    \trans{pool}{c}
        \var{poolParams} \\
        \varUpdate{\var{retiring}} & \varUpdate{\unionoverrideRight}
                                   & \varUpdate{\{\var{hk} \mapsto \var{e}\}} \\
-
        \var{cs} \\
      \end{array}
    \right)
  }
          \var{stpools} \\
          \var{poolParams} \\
          \var{retiring} \\
-
          \var{cs} \\
        \end{array}
        \right) \\
      \end{array}
          \var{stpools} \\
          \var{poolParams} \\
          \var{retiring} \\
-
          \var{cs} \\
        \end{array}
        \right) \\
      \end{array}
    \inference[Seq-ledger-base]
    {
      ((\var{utxo},~\var{deposits},~\var{fees},~\var{us})
-
      ,~(\var{ds},~\var{ps}))
+
      ,~(\var{ds}, \var{ps}))
      \leteq\var{ls}
      \\
      (\var{pup},~\var{aup},~\var{favs},~\var{avs}) \leteq\var{us}
      \\
      (\var{stkeys},~\var{rewards},~\var{delegations}, ~\var{ptrs},~\var{fGenDelegs},~\var{genDelegs})
      \leteq\var{ds}
-
      \\
-
      (\var{stpools},~\var{poolParams},~\var{retiring},~\var{cs})\leteq\var{ps}
      \\~\\
      {\begin{array}{[email protected]{~\leteq~}l}
        \var{favs'} & \{\var{s}\mapsto\var{v}\in\var{favs} ~\mid~ s>\var{slot}\}
      (\var{stkeys},~\var{rewards},~\var{delegations},~\var{ptrs},
      ~\var{fGenDelegs}\setminus\var{curr},~\var{genDelegs}\unionoverrideRight\var{genDelegs'})
      \\
-
      \var{oldGenDelegs}\leteq\range((\dom\var{genDelegs'})\restrictdom\var{genDelegs})
-
      \\
-
      \var{cs'}\leteq(\var{oldGenDelegs}\subtractdom\var{cs})\unionoverrideRight
-
      \{\var{hk}\mapsto 0~\mid~\var{hk}\in\range{genDelegs'}\}
-
      \\
-
      \var{ps'}\leteq(\var{stpools},~\var{poolParams},~\var{retiring},~\var{cs'})
-
      \\
-
      \var{ls'}\leteq((\var{utxo},~\var{deposits},~\var{fees},~\var{us'}),~(\var{ds'},~\var{ps'}))
+
      \var{ls'}\leteq((\var{utxo},~\var{deposits},~\var{fees},~\var{us'}),~(\var{ds'}, \var{ps}))
    }
    {
      \begin{array}{r}