utxo.tex

\section{UTxO}
\label{sec:utxo}

A key constraint that must always be satisfied as a result and precondition of
a valid ledger state transition is called the \textit{general accounting
property}, or the \textit{preservation of value} condition. Every piece of
software that is a part of the implementation of the
Cardano cryptocurrency must function in such a way as to not result in
a violation of this rule.
If this condition is not satisfied, it is an indicator of
incorrect accounting, potentially due to
malicious disruption or a bug.

The preservation of value is expressed as an equality that uses values in
the ledger state and the environment, as well as the values in the body of
the signal transaction.
We have defined the rules of the delegation protocol in a way that should
consistently satisfy the preservation of value.

In this section, we discuss the relevant accounting that needs to be done
as a result of processing a transaction, i.e.~the deposits for all certificates,
transaction fees, transaction withdrawals and refunds for individual
deregistration, so that we may keep track of whether the preservation of
value is satisfied. Stake pool retirement refunds are not triggered by a
transaction (but rather, happen at the epoch boundary) and are therefore
not considered in our state change rules invoked due to a signal transaction.

Note that when a transaction is issued by a wallet to be applied to the ledger
state (i.e.~processed), the rules in this section are defined in such a way that it is impossible to
apply only some parts of a transaction (e.g.~only certain certificates).
Every part of the transaction must be valid and it must be live, otherwise
it is ignored entirely. It is the wallet's responsibility to inform the user
that a transaction failed to be processed.

\subsection{UTxO Transitions}
\label{sec:utxo-trans}

Figure~\ref{fig:functions:utxo} defines functions needed for the UTxO transition system.
See Figure~\ref{fig:defs:utxo-shelley} for most of the definitions used in the transition system.

\begin{itemize}

  \item
    The function $\fun{outs}$ creates unspent outputs generated by a transaction, so that
    they can be added to the ledger state.  For each output in the transaction,
    $\fun{outs}$ maps the transaction id and output index to the output.

  \item
    The $\fun{ubalance}$ function calculates sum total of all the coin in a given UTxO.
  \item
    The $\fun{wbalance}$ function calculates the total sum of all the reward withdrawals in a
    transaction.

  \item The calculation $\fun{consumed}$ gives the value consumed by the
    transaction $\var{tx}$ in the context of the protocol parameters, the
    current UTxO on the ledger and the registered stake credentials. This
    calculation is a sum of all coin in the inputs of $\var{tx}$, reward
    withdrawals and stake credential deposit refunds. Some of the definitions
    used in this function will be defined in Section~\ref{sec:deps-refunds}. In particular,
    $\fun{keyRefunds}$ is defined in Figure~\ref{fig:functions:deposits-refunds}.

  \item The calculation $\fun{produced}$ gives the value produced by the transaction $\var{tx}$
    in the context of the protocol parameters and the registered stake pools.
    This calculation is a sum of all coin in the outputs of $\var{tx}$,
    the transaction fee and all needed deposits.
    Some of the definitions used in this function will be defined in
    Section~\ref{sec:deps-refunds}.
    In particular, $\fun{totalDeposits}$ is defined in Figure~\ref{fig:functions:deposits-refunds}.
\end{itemize}

For a transaction and a given ledger state, the preservation of value property holds
exactly when the results of $\fun{consumed}$ equal the results of $\fun{produced}$.
Moreover, when the property holds, value is only moved between transaction outputs,
the reward accounts, the fee pot and the deposit pot.

Note that the $\fun{produced}$ function takes the registered stake pools ($\var{poolParams}$)
as a parameter only in order to determine which pool registration certificates are
new (and thus require a deposit) and which ones are updates.
Registration will be discussed more in Section~\ref{sec:delegation-shelley}.

\begin{figure}[htb]
  \begin{align*}
    & \fun{outs} \in \TxBody \to \UTxO
    & \text{tx outputs as UTxO} \\
    & \fun{outs} ~ \var{tx} =
        \left\{
          (\fun{txid} ~ \var{tx}, \var{ix}) \mapsto \var{txout} ~
          \middle|
          \var{ix} \mapsto \var{txout} \in \txouts{tx}
        \right\}
    \nextdef
    & \fun{ubalance} \in \UTxO \to \Coin
    & \text{UTxO balance} \\
    & \fun{ubalance} ~ utxo = \sum_{(~\wcard ~ \mapsto (\wcard, ~c)) \in \var{utxo}} c
    \nextdef
    & \fun{wbalance} \in \Wdrl \to \Coin
    & \text{withdrawal balance} \\
    & \fun{wbalance} ~ ws = \sum_{(\wcard\mapsto c)\in\var{ws}} c
    \nextdef
    & \fun{consumed} \in \PParams \to \UTxO \to \TxBody \to \Coin
    & \text{value consumed} \\
    & \consumed{pp}{utxo}{tx} = \\
    & ~~\ubalance{(\txins{tx} \restrictdom \var{utxo})} +
        \fun{wbalance}~(\fun{txwdrls}~{tx}) \\
    & ~~ + \keyRefunds{pp}{tx} \\
    \nextdef
    & \fun{produced} \in \PParams \to (\KeyHash_{pool}\mapsto\PoolParam) \to \TxBody \to \Coin
    & \text{value produced} \\
    & \fun{produced}~\var{pp}~\var{poolParams}~\var{tx} = \\
    &~~\ubalance{(\outs{tx})}
    + \txfee{tx} + \totalDeposits{pp}{poolParams}{(\txcerts{tx})}\\
  \end{align*}

  \caption{Functions used in UTxO rules}
  \label{fig:functions:utxo}
\end{figure}

\clearpage


The types for the UTxO transition are given in Figure~\ref{fig:ts-types:utxo-shelley}.
The environment, $\UTxOEnv$, consists of:

\begin{itemize}
  \item The current slot.
  \item The protocol parameters.
  \item The registered stake pools
    (also explained in Section~\ref{sec:delegation-shelley},
    Figure~\ref{fig:delegation-defs}).
  \item The genesis key delegation mapping.
\end{itemize}
The current slot and registrations are needed for the refund calculations
described in Section~\ref{sec:deps-refunds}.

The state needed for the UTxO transition $\UTxOState$, consists of:

\begin{itemize}
  \item The current UTxO.
  \item The deposit pot.
  \item The fee pot.
  \item Proposed updates (see Section~\ref{sec:update}).
\end{itemize}
The signal for the UTxO transition is a transaction.

\begin{figure}[htb]
  \emph{UTxO environment}
  \begin{equation*}
    \UTxOEnv =
    \left(
      \begin{array}{r@{~\in~}lr}
        \var{slot} & \Slot & \text{current slot}\\
        \var{pp} & \PParams & \text{protocol parameters}\\
        \var{poolParams} & \KeyHash_{pool}\mapsto\PoolParam & \text{stake pools}\\
        \var{genDelegs} & \GenesisDelegation & \text{genesis key delegations} \\
      \end{array}
    \right)
  \end{equation*}
  %
  \emph{UTxO States}
  \begin{equation*}
    \UTxOState =
    \left(
      \begin{array}{r@{~\in~}lr}
        \var{utxo} & \UTxO & \text{UTxO}\\
        \var{deposited} & \Coin & \text{deposits pot}\\
        \var{fees} & \Coin & \text{fee pot}\\
        \var{ppup} & \PPUpdateState & \text{proposed updates}\\
      \end{array}
    \right)
  \end{equation*}
  %
  \emph{UTxO transitions}
  \begin{equation*}
    \_ \vdash
    \var{\_} \trans{utxo}{\_} \var{\_}
    \subseteq \powerset (\UTxOEnv \times \UTxOState \times \Tx \times \UTxOState)
  \end{equation*}
  %
  \caption{UTxO transition-system types}
  \label{fig:ts-types:utxo-shelley}
\end{figure}

The UTxO transition system is given in Figure~\ref{fig:rules:utxo-shelley}.
Rule~\ref{eq:utxo-inductive-shelley} specifies the conditions under which a transaction can
be applied to a particular $\UTxOState$ in environment $\UTxOEnv$:

The transition contains the following predicates:

\begin{itemize}
  \item
    The transaction is live (the current slot is less than its time to live).
  \item
    The transaction has at least one input.
    The global uniqueness of transaction inputs prevents replay attacks.
    By requiring that all transactions spend at least one input,
    the entire transaction is safe from such attacks.
    A delegation certificate by itself, for example, does not have this property.
  \item
    The fee paid by the transaction has to be greater than or equal to the minimum fee,
    which is based on the size of the transaction.
    We leave open the future possibility that transactions with larger fees can be prioritized.
  \item
    Each input spent in the transaction must be in the set of unspent
    outputs.
  \item
    The \textit{preservation of value} property must hold.
    In other words, the amount of value produced by the transaction must be the same as
    the amount consumed.
  \item
    The $\mathsf{PPUP}$ transition is successful.
  \item
    The coin value of each new output must be at least as large as the
    minimum value specified by the protocol parameter $\var{minUTxOValue}$.
  \item
    The transaction size must be below the allowed maximum.
    Note that there is an implicit max transaction size given by the max block size,
    and that if we wished to allow a transaction to be as large as will fit in a block, this
    check would not be needed.
    Being able to limit the size below that of the block, however, gives us some
    control over how transactions will be packed into the blocks.
\end{itemize}
If all the predicates are satisfied, the state is updated as follows:

\begin{itemize}
  \item Update the UTxO:
    \begin{itemize}
      \item Remove from the UTxO all the $(\var{txin}, \var{txout})$ pairs
        associated with the $\var{txins}$'s in the $\var{inputs}$ list of
        the transaction body $\var{txb}$.
      \item Add all the $\var{outputs}$ of $\var{tx}$ to the
        UTxO, associated with the $\fun{txid}$ of the transaction body $\var{txb}$
    \end{itemize}
  \item Add all new deposits to the deposit pot and subtract all deposit refunds.
  \item Add the transaction fee to the fee pot.
  \item Update the current update proposals.
\end{itemize}

The accounting for the reward withdrawals is not done in this transition system.
The rewards are tracked with the delegation state and will
be removed in the final delegation transition, see ~\ref{eq:delegs-base}.

Note here that output entries for both the deposit refunds and the rewards
withdrawals must be included in the body of the transaction
carrying the deregistration certificates (requesting these refunds) and the
reward requests. It is the job
of the wallet to calculate the value of these refunds and withdrawals and
generate the correct outputs to include in the outputs list of $\var{tx}$ such
that applying this transaction results in a
valid ledger update adding correct amounts of coin to the right addresses.

The approach of including refunds and rewards directly in the $outputs$ gives
great flexibility to the management of the coin value obtained from these
accounts, i.e.~it can be directed to any address. However, it means there is no
direct link between the $wdrls$ requests (similarly for the key deregistration
certificate addresses and refund amounts) and the $outputs$. We verify that
the included outputs are correct and authorized through the preservation of value condition
and witnessing the transaction. The combination of the
preservation of value and witnessing, described in Section~\ref{sec:witnesses-shelley},
assures that the ledger state is updated correctly.

The main difference, however, in how rewards and refunds work is that refunds
come from the $\var{deposited}$ pot, which is a single coin value indicating
the sum of all the deposits, while rewards come from individual
accounts where a reward is accumulated to a specific address.

\begin{figure}[htb]
  \begin{equation}\label{eq:utxo-inductive-shelley}
    \inference[UTxO-inductive]
    { \var{txb}\leteq\txbody{tx}
      & \txttl txb \geq \var{slot}
      \\ \txins{txb} \neq \emptyset
      & \minfee{pp}{tx} \leq \txfee{txb}
      & \txins{txb} \subseteq \dom \var{utxo}
      \\
      \consumed{pp}{utxo}~{txb} = \produced{pp}{poolParams}~{txb}
      \\
      ~
      \\
      {
        \begin{array}{r}
          \var{slot} \\
          \var{pp} \\
          \var{genDelegs} \\
        \end{array}
      }
      \vdash \var{ppup} \trans{\hyperref[fig:rules:pp-update]{ppup}}{\fun{txup}~\var{tx}} \var{ppup'}
      \\
      ~
      \\
      \forall (\wcard\mapsto (\wcard,~c)) \in \txouts{txb}, c \geq (\fun{minUTxOValue}~\var{pp})
      \\
      \forall (\wcard\mapsto (a,~\wcard)) \in \txouts{txb}, a \in \AddrBS \Rightarrow \fun{bootstrapAttrsSize}~a \leq 64
      \\
      \forall (\wcard\mapsto (a,~\wcard)) \in \txouts{txb}, \fun{netId}~a =\NetworkId
      \\
      \forall (a\mapsto\wcard) \in \txwdrls{txb}, \fun{netId}~a =\NetworkId
      \\
      \fun{txsize}~{tx}\leq\fun{maxTxSize}~\var{pp}
      \\
      ~
      \\
      \var{refunded} \leteq \keyRefunds{pp}{txb}
      \\
      \var{depositChange} \leteq
        \totalDeposits{pp}{poolParams}{(\txcerts{txb})} - \var{refunded}
    }
    {
      \begin{array}{r}
        \var{slot}\\
        \var{pp}\\
        \var{poolParams}\\
        \var{genDelegs}\\
      \end{array}
      \vdash
      \left(
      \begin{array}{r}
        \var{utxo} \\
        \var{deposited} \\
        \var{fees} \\
        \var{ppup}\\
      \end{array}
      \right)
      \trans{utxo}{tx}
      \left(
      \begin{array}{r}
        \varUpdate{(\txins{txb} \subtractdom \var{utxo}) \cup \outs{txb}}  \\
        \varUpdate{\var{deposited} + \var{depositChange}} \\
        \varUpdate{\var{fees} + \txfee{txb}} \\
        \varUpdate{ppup'}\\
      \end{array}
      \right)
    }
  \end{equation}
  \caption{UTxO inference rules}
  \label{fig:rules:utxo-shelley}
\end{figure}

The UTXO rule has ten predicate failures:
\begin{itemize}
\item In the case of any input not being valid, there is a \emph{BadInput}
  failure.
\item In the case of the current slot being greater than the time-to-live of the
  current transaction, there is an \emph{Expired} failure.
\item In the case that the transaction is too large,
  there is a \emph{MaxTxSize} failure.
\item In the case of an empty input set, there is a \emph{InputSetEmpty} failure,
  in order to prevent replay attacks.
\item If the fees are smaller than the minimal transaction fees, there is a
  \emph{FeeTooSmall} failure.
\item If the transaction does not correctly conserve the balance, there is a
  \emph{ValueNotConserved} failure.
\item If the transaction creates any outputs with the wrong network ID,
  there is a \emph{WrongNetwork} failure.
\item If the transaction contains any withdrawals with the wrong network ID,
  there is a \emph{WrongNetworkWithdrawal} failure.
\item If the transaction creates an output below the allowed minimum value,
  there is a \emph{OutputTooSmall} failure.
\item If the transaction creates any boostrap outputs whose attributes have
  size bigger than 64, there is a \emph{OutputBootAddrAttrsTooBig} failure.
\end{itemize}

\clearpage

\subsection{Deposits and Refunds}
\label{sec:deps-refunds}

Deposits are described in appendix B.2 of the delegation design document
\cite{delegation_design}.  These deposit functions were used above in the UTxO
transition,~\ref{sec:utxo-trans}. Deposits are used for stake credential
registration and pool registration certificates, which will be explained in
Section~\ref{sec:delegation-shelley}.  In particular, the function
$\cwitness{}$, which gets the certificate witness from a certificate, will be
defined later.  Figure~\ref{fig:functions:deposits-refunds} defines the deposit
and refund functions.
\begin{itemize}
  \item The function $\fun{totalDeposits}$ returns the total deposits that have to be
    made by a transaction.  This calculation uses two protocol parameters, namely
    the key deposit value and the pool deposit value.
    Note that those certificates which are
    updates of stake pool parameters of already registered pool keys should not
    (and are, in fact, not allowed to) make a deposit.
  \item The function $\fun{keyRefunds}$, calculates the total amount of returned
    deposits from stake key deregistration certificates.

    Note that $\fun{keyRefunds}$ uses the \textit{current} protocol parameters.
    This means that any deposits made prior to a change in the deposit values
    will be refunded with the current value, not the one originally paid.

    The protocol parameters are not
    expected to change often and using the current ones for the calculation
    is a deliberate simplification choice, which does not introduce any inconsistencies
    into the system rules or properties. In particular, the general accounting
    property is not violated.
\end{itemize}

\begin{figure}[htb]
  \begin{align*}
    & \fun{totalDeposits} \in \PParams \to (\KeyHash_{pool}\mapsto\PoolParam) \\
    & ~~~~\to \seqof{\DCert} \to \Coin
    & \text{total deposits for a tx} \\
    & \totalDeposits{pp}{poolParams}{certs} = \\
    &  ~~~ (\fun{keyDeposit}~pp)\cdot|\var{certs}\cap\DCertRegKey| \\
    &  ~~~~~ + (\fun{poolDeposit}~pp)\cdot|\{\cwitness{c} ~\mid c\in~\var{newPools}\}| \\
    & ~~~\where \\
    &  ~~~~~~~ \var{newPools} = \{c ~\mid~ c\in\var{certs}\cap\DCertRegPool,~\cwitness{c}\notin \var{poolParams}\}
    \nextdef
      & \fun{keyRefunds} \in \PParams \to \TxBody \to \Coin
      & \text{key refunds for a tx} \\
      & \keyRefunds{pp}{tx} = (\fun{keyDeposit}~\var{pp})\cdot|\txcerts{tx} \cap \DCertDeRegKey|\\
      \end{align*}
      \caption{Functions used in Deposits - Refunds}
      \label{fig:functions:deposits-refunds}
  \end{figure}

\clearpage

\subsection{Witnesses}
\label{sec:witnesses-shelley}

The purpose of witnessing is make sure that the intended action is authorized by
the holder of the signing key, providing replay protection as a consequence.
Replay prevention is an inherent property of UTxO type accounting
since transaction IDs are unique and we require all transaction to
consume at least one input.

A transaction is witnessed by a signature and a verification key corresponding
to this signature.  The witnesses, together with the transaction body, form a
full transaction.  Every witness in a transaction signs the transaction body.
Moreover, the witnesses are represented as finite maps from verification keys to
signatures, so that any key that is required to sign a transaction only provides
a single witness.  This means that, for example, a transaction which includes a
delegation certificate and a reward withdrawal corresponding to the same stake
credential still only includes one signature.

Figure~\ref{fig:functions-witnesses} defines the function which
gathers all the (hashes of) verification keys needed to witness a given transaction.
This consists of:
\begin{itemize}
  \item payment keys for outputs being spent
  \item stake credentials for reward withdrawals
  \item stake credentials for delegation certificates (except \DCertMir{} and \DCertRegKey{})
  \item delegates of the genesis keys for any protocol parameter updates
  \item stake credentials for the pool owners in a pool registration certificate
\end{itemize}

\begin{figure}[htb]
  \begin{align*}
    & \fun{propWits} \in \Update \to \GenesisDelegation \to \powerset{\KeyHash}
    & \text{hashkeys for proposals} \\
    & \fun{propWits}~(\var{pup},~\wcard)~\var{genDelegs} = \\
    & ~~\left\{
      \var{kh}
      \mid
      \var{gkh}\mapsto(\var{kh},~\wcard)\in
      \left(\dom{\var{pup}}\restrictdom\var{genDelegs}\right)
      \right\}
  \end{align*}

  \begin{align*}
    & \hspace{-0.8cm}\fun{certWitsNeeded} \Tx \to \powerset{\Credential}
    & \text{certificates with witnesses} \\
    &  \hspace{-0.8cm}\fun{certWitsNeeded}~\var{tx} = \\
    & \bigcup\{\cwitness{c} \mid c \in \txcerts{tx} \setminus (\DCertRegKey\cup\DCertMir)\}
  \end{align*}

  \begin{align*}
    & \hspace{-0.8cm}\fun{witsVKeyNeeded} \in \UTxO \to \Tx \to (\KeyHashGen\mapsto\VKey) \to
      \powerset{\KeyHash}
    & \text{required key hashes} \\
    &  \hspace{-0.8cm}\fun{witsVKeyNeeded}~\var{utxo}~\var{tx}~\var{genDelegs} = \\
    & ~~\{ \fun{paymentHK}~a \mid i \mapsto (a, \wcard) \in \var{utxo},~i\in\fun{txinsVKey}~{tx} \} \\
    \cup & ~~
           \{\fun{stakeCred_r}~a\mid a\mapsto \wcard \in \AddrRWDVKey
      \restrictdom \txwdrls{tx}\}\\
    \cup & ~~(\AddrVKey \cap \fun{certWitsNeeded}~{tx}) \\
    \cup & ~~\fun{propWits}~(\fun{txup}~\var{tx})~\var{genDelegs} \\
    \cup & ~~\bigcup_{\substack{c \in \txcerts{tx} \\ ~c \in\DCertRegPool}} \fun{poolOwners}~{c}
  \end{align*}
  \begin{align*}
    & \hspace{-1cm}\fun{scriptsNeeded} \in \UTxO \to \Tx \to
      \powerset{\HashScr}
    & \text{required script hashes} \\
    &  \hspace{-1cm}\fun{scriptsNeeded}~\var{utxo}~\var{tx} = \\
    & ~~\{ \fun{validatorHash}~a \mid i \mapsto (a, \wcard) \in \var{utxo},\\
    & ~~~~~i\in\fun{txinsScript}~{(\fun{txins~\var{tx}})}~{utxo}\} \\
    \cup & ~~\{ \fun{stakeCred_{r}}~\var{a} \mid a \in \dom (\AddrRWDScr
           \restrictdom \fun{txwdrls}~\var{tx}) \} \\
      \cup & ~~(\AddrScr \cap \fun{certWitsNeeded}~{tx})
  \end{align*}
  \caption{Functions used in witness rule}
  \label{fig:functions-witnesses}
\end{figure}

The UTxOW transition system adds witnessing to the previous UTxO transition system.
Figure~\ref{fig:ts-types:utxow-shelley} defines the type for this transition.

\begin{figure}
  \emph{UTxO with witness transitions}
  \begin{equation*}
    \var{\_} \vdash
    \var{\_} \trans{utxow}{\_} \var{\_}
    \subseteq \powerset (\UTxOEnv \times \UTxOState \times \Tx \times \UTxOState)
  \end{equation*}
  \caption{UTxO with witness transition-system types}
  \label{fig:ts-types:utxow-shelley}
\end{figure}

Figure~\ref{fig:rules:utxow-shelley} defines UTxOW transition.
It has six predicates:
\begin{itemize}
  \item Every signature in the transaction is a valid signature of the transaction body.
  \item The set of (hashes of) verification keys given by the transaction is a subset of
    the set of needed (hashes of) verification keys.
  \item Every multisignature script is valid.
  \item The set of scripts given by the transaction is equal to the set of required scripts.
  \item Any instantaneous reward certificates have quorum agreement from the genesis nodes delegates.
  \item Either the transaction metadata hash and the transaction metadata are both absent,
    or the hash present in the body is actually equal to the hash of the metadata.
\end{itemize}
If the predicates are satisfied, the state is transitioned by the UTxO transition rule.

\begin{figure}
  \begin{equation}
    \label{eq:utxo-witness-inductive-shelley}
    \inference[UTxO-wit]
    {
      (utxo, \wcard, \wcard, \wcard) \leteq \var{utxoSt} \\
      \var{witsKeyHashes} \leteq \{\fun{hashKey}~\var{vk} \vert \var{vk} \in
      \dom (\txwitsVKey{tx}) \}\\~\\
      \forall \var{hs} \mapsto \var{validator} \in \fun{txwitsScript}~{tx},\\
      \fun{hashScript}~\var{validator} = \var{hs} \wedge
      \fun{validateScript}~\var{validator}~\var{tx}\\~\\
      \fun{scriptsNeeded}~\var{utxo}~\var{tx} = \dom (\fun{txwitsScript}~{tx})
      \\~\\
      \var{txbodyHash}\leteq\fun{hash}~(\txbody{tx}) \\
      \forall \var{vk} \mapsto \sigma \in \txwitsVKey{tx},
      \mathcal{V}_{\var{vk}}{\serialised{txbodyHash}}_{\sigma} \\
      \fun{witsVKeyNeeded}~{utxo}~{tx}~{genDelegs} \subseteq witsKeyHashes
      \\~\\
      genSig \leteq
      \left\{
        \var{genDelegate}~\vert~(\var{genDelegate},~\wcard) \in\range{genDelegs}
      \right\}
      \cap
      \var{witsKeyHashes}
      \\
      \left\{
        c\in\txcerts{tx}~\cap\DCertMir
      \right\} \neq\emptyset \implies \vert genSig\vert \geq \Quorum
      \\~\\
      \var{mdh}\leteq\fun{txMDhash}~\var{tx}
      &
      \var{md}\leteq\fun{txMD}~\var{tx}
      \\
      (\var{mdh}=\Nothing \land \var{md}=\Nothing)
      \lor
      (\var{mdh}=\fun{hashMD}~\var{md})
      \\~\\
      {
        \begin{array}{r}
          \var{slot}\\
          \var{pp}\\
          \var{poolParams}\\
          \var{genDelegs}\\
        \end{array}
      }
      \vdash \var{utxoSt} \trans{\hyperref[fig:rules:utxo-shelley]{utxo}}{tx}
      \var{utxoSt'}\\
    }
    {
      \begin{array}{r}
        \var{slot}\\
        \var{pp}\\
        \var{poolParams}\\
        \var{genDelegs}\\
      \end{array}
      \vdash \var{utxoSt} \trans{utxow}{tx} \varUpdate{\var{utxoSt'}}
    }
  \end{equation}
  \caption{UTxO with witnesses inference rules}
  \label{fig:rules:utxow-shelley}
\end{figure}

The UTXOW rule has eight predicate failures:
\begin{itemize}
\item In the case of an incorrect witness,
  there is a \emph{InvalidWitnesses} failure.
\item In the case of a missing witness,
  there is a \emph{MissingVKeyWitnesses} failure.
\item In the case of missing scripts,
  there is a \emph{MissingScriptWitnesses} failure.
\item In the case of an invalid script,
  there is a \emph{ScriptWitnessNotValidating} failure.
\item In the case of a lack of quorum on an instantaneous reward certificate,
  there is a \emph{MIRInsufficientGenesisSigs} failure.
\item In the case the transaction contains metadata,
  but the transaction body does not contain a metadata hash,
  there is a \emph{MissingTxBodyMetadataHash} failure.
\item In the case that the transaction body contains a metadata hash,
  but there is no metadata outside the body,
  there is a \emph{MissingTxMetadata} failure.
\item In the case that the metadata hash in the transaction body
  is not equal to the hash of the metadata outside the body,
  there is a \emph{ConflictingMetadataHash} failure.
\end{itemize}

\clearpage