ledger.tex

\section{Ledger State Transition}
\label{sec:ledger-trans}

Figure~\ref{fig:rules:ledger} separates the case where all the scripts
in a transaction successfully validate from the case where there is one or more that does not.
These two cases are distinguished by the use of the $\IsValid$ tag.
%
Besides collateral collection, no side effects should occur when processing a
transaction that contains a script that does not validate. That is, no
delegation or pool state updates, update proposals, or any other observable state change, should be
applied. The UTxO rule is still applied, however, as this is where the correctness of the
validation tag is verified, and where collateral inputs are collected.

\begin{figure}
  \begin{equation}
    \label{eq:ledger}
    \inference[ledger-V]
    {
      \fun{isValid}~{tx} = \True \\~\\
      {
        \begin{array}{c}
          \var{slot} \\
          \var{txIx} \\
          \var{pp} \\
          \var{tx}\\
          \var{acnt}
        \end{array}
      }
      \vdash
      dpstate \trans{\hyperref[fig:rules:delegation-sequence]{delegs}}{
                     \fun{txcerts}~(\txbody{tx})} dpstate'
      \\~\\
      (\var{dstate}, \var{pstate}) \leteq \var{dpstate} \\
      (\_, \_, \_, \_, \_, \var{genDelegs}, \_) \leteq \var{dstate} \\
      (\var{poolParams}, \_, \_) \leteq \var{pstate} \\
      \\~\\
      {
        \begin{array}{c}
        \var{slot} \\
        \var{pp} \\
        \var{poolParams} \\
        \var{genDelegs} \\
        \end{array}
      }
      \vdash \var{utxoSt} \trans{\hyperref[fig:rules:utxow-shelley]{utxow}}{tx} \var{utxoSt'}
    }
    {
      \begin{array}{c}
        \var{slot} \\
        \var{txIx} \\
        \var{pp} \\
        \var{acnt}
      \end{array}
      \vdash
      \left(
        \begin{array}{ll}
          \var{utxoSt} \\
          \var{dpstate} \\
        \end{array}
      \right)
      \trans{ledger}{tx}
      \left(
        \begin{array}{ll}
          \varUpdate{utxoSt'} \\
          \varUpdate{dpstate'} \\
        \end{array}
      \right)
    }
  \end{equation}
  %
  \nextdef
  %
  \begin{equation}
    \label{eq:ledger}
    \inference[ledger-NV]
    {
      \fun{isValid}~{tx} = \False \\~\\
      (\var{dstate}, \var{pstate}) \leteq \var{dpstate} \\
      (\_, \_, \_, \_, \_, \var{genDelegs}, \_) \leteq \var{dstate} \\
      (\var{poolParams}, \_, \_) \leteq \var{pstate} \\
      \\~\\
      {
        \begin{array}{c}
        \var{slot} \\
        \var{pp} \\
        \var{poolParams} \\
        \var{genDelegs} \\
        \end{array}
      }
      \vdash \var{utxoSt} \trans{\hyperref[fig:rules:utxow-shelley]{utxow}}{tx} \var{utxoSt'}
    }
    {
      \begin{array}{c}
        \var{slot} \\
        \var{txIx} \\
        \var{pp} \\
        \var{acnt}
      \end{array}
      \vdash
      \left(
        \begin{array}{ll}
          \var{utxoSt} \\
          \var{dpstate} \\
        \end{array}
      \right)
      \trans{ledger}{tx}
      \left(
        \begin{array}{ll}
          \varUpdate{utxoSt'} \\
          \var{dpstate} \\
        \end{array}
      \right)
    }
  \end{equation}
  \caption{Ledger inference rules}
  \label{fig:rules:ledger}
\end{figure}

\clearpage