utxo.tex

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

\subsection*{UTxO Helper Functions}

\begin{figure}[htb]
  \emph{Type Definition}
  \begin{equation*}
    \begin{array}{r@{~\in~}l@{\qquad=\qquad}lr}
      \var{mest} & \MemoryEstimate & \N
    \end{array}
  \end{equation*}
  %
  \emph{Abstract Helper Function}
  \begin{align*}
    \fun{utxoEntrySize} \in& ~\TxOut \to \MemoryEstimate & \text{Memory estimate for}~\TxOut
  \end{align*}
  %
  \emph{Helper Functions}
  \begin{align*}
    & \fun{ininterval} \in \Slot \to (\Slot^? \times \Slot^?) \to \Bool \\
    & \fun{ininterval}~\var{slot}~(i_s, i_f) ~=~
    \begin{cases}
      \True & (i_s = \Nothing)~\wedge~(i_f = \Nothing) \\
      \var{slot}~<~i_f & (i_s = \Nothing)~\wedge~(i_f \neq \Nothing)\\
      i_s~\leq~\var{slot} & (i_s \neq \Nothing)~\wedge~(i_f = \Nothing) \\
      i_s~\leq~\var{slot}~<~i_f & (i_s \neq \Nothing)~\wedge~(i_f \neq \Nothing)
    \end{cases}
    \nextdef
    & \fun{getCoin} \in \TxOut \to \Coin \\
    & \fun{getCoin}~{(\wcard,~\var{out})} ~=~\fun{coin}~\var{out}
    \nextdef
    & \fun{ubalance} \in \UTxO \to \hldiff{\ValMonoid} \\
    & \fun{ubalance} ~ utxo = \hldiff{\sum_{\wcard\mapsto\var{u}\in~\var{utxo}} \fun{getValue}~\var{u}}
    \nextdef
    & \fun{isAdaOnly} ~\in~ \mathsf{ValType} \to \Bool \\
    & \fun{isAdaOnly}~v = v \in \range \fun{inject}
    \nextdef
    & \fun{scaledMinDeposit} \in \ValMonoid \to \Coin \to \Coin \\
    & \fun{scaledMinDeposit}~\var{v}~\var{mv} ~=~
    \begin{cases}
      \var{mv} & \fun{isAdaOnly}~v \\
      \fun{max}~(\var{mv},~\fun{utxoEntrySize}~{v} * \fun{coinsPerUTxOWord}~mv)) & \text{otherwise}
    \end{cases}
  \end{align*}
  %
  \emph{Produced and Consumed Calculations}
  \begin{align*}
    & \fun{consumed} \in \PParams \to \UTxO \to \TxBody \to \hldiff{\ValMonoid} \\
    & \consumed{pp}{utxo}{txb} = \\
    & ~~\ubalance{(\txins{txb} \restrictdom \var{utxo})} ~+~ \hldiff{\fun{mint}~\var{txb}} \\
    &~~+~\hldiff{\fun{inject}}(\fun{wbalance}~(\fun{txwdrls}~{txb})~+~ \keyRefunds{pp}{txb})
    \nextdef
    & \fun{produced} \in \PParams \to \StakePools \to \TxBody \to \hldiff{\ValMonoid} \\
    & \fun{produced}~\var{pp}~\var{stpools}~\var{txb} = \\
    &~~\ubalance{(\fun{outs}~{txb})} \\
    &~~+ \hldiff{\fun{inject}}(\txfee{txb} + \totalDeposits{pp}{stpools}{(\txcerts{txb})})
  \end{align*}
  \caption{UTxO Calculations}
  \label{fig:functions:utxo}
\end{figure}

Figure~\ref{fig:functions:utxo} defines additional calculations that are needed for the
UTxO transition system with multi-assets:

\begin{itemize}
  \item The $\MemoryEstimate$ type represents the size, in \emph{words} (8 bytes), of
  a term (eg. a transaction input, or output). Note that this estimate is calculated
  according to fomulas we provide in this specification (see Appendix \ref{sec:value-size}),
  as opposed to obtained using an existing function of the programming
  language selected for implementation.

  \item The $\fun{utxoEntrySize}$ function provides a rough estimate of
    the amount of memory the storage of an output will consume, which is used in the UTXO rule.
    Its implementation is described in Appendix \ref{sec:value-size}.

  \item The function $\fun{ininterval}$ returns $\True$ whenever the given slot is
  inside the given interval. If an endpoint of the validity interval
  is $\Nothing$, the comparison of the slot to that endpoint is $\True$ by default.

  \item The function $\fun{getCoin}$ returns the Ada in a given output as a $\Coin$ value.

  \item The $\fun{ubalance}$ function calculates the sum total in a given UTxO.

  \item The $\fun{consumed}$ and $\fun{produced}$ calculations are similar to their Shelley
    counterparts, with the following changes: 1) They return elements of $\ValMonoid$, which
    the administrative fields of type $\Coin$ have to be converted to, via $\fun{inject}$.
    2) $\fun{consumed}$ also contains the $\fun{mint}$ field of the transaction.
    This is explained below.
\end{itemize}

\subsection*{Minting and the Preservation of Value}
What does it mean to preserve the value of non-Ada assets, since they
are put in and taken out of circulation by the users themselves? This
question becomes relevant when we pick a Token algebra that can represent
assets other than Ada.

If a transaction $\var{tx}$ has an empty $\fun{mint}$ field, the preservation
of value condition reduces to the same equality as the POV in Shelley. If a transaction
mints assets, the value of the $\fun{mint}$ field has to reflect exactly
the increase or decrease of the total quantities of the assets being
minted or burned. Note that this means that the
$\fun{mint}$ field can also contain negative quantities in the case assets
are being burned.

To balance the preservation of value equation, the $\fun{mint}$ field
could be included in either $\fun{consumed}$ or $\fun{produced}$, with
the only difference being the sign of the $\fun{mint}$ field. We
include it on the $\fun{consumed}$ side, because this means that
minting a positive quantity increases the total quantity of assets on the
ledger, and minting a negative quantity reduces the total quantity of assets on
the ledger.

Note that the UTXO rule specifically forbids the minting of Ada, and
thus in the case of Ada, the preservation of value equation is exactly
the same as in Shelley.

The minting scripts themselves are not evaluated at part of the UTXO, but instead
as part of witnessing, i.e. in the UTXOW rule, see Figure~\ref{fig:functions-witnesses}.

\subsection*{The UTXO Transition Rule}
In Figure \ref{fig:rules:utxo-shelley}, we give the UTXO transition rule for ShelleyMA.
There are the following changes to the preconditions
of this rule as compared to the original Shelley UTXO rule:

\begin{itemize}
  \item The check that the time-to-live of a transaction is after the current
  slot is replaced with the check that the current slot is inside the validity interval

  \item In the preservation of value calculation (which looks the same as in
  Shelley), the value in the $\fun{mint}$ field is taken into account.

  \item The transaction is not minting any Ada. This condition, in the Allegra
  era, ensures that no assets can ever be minted (since Ada is the only existing
  asset).

  \item The $\ValMonoid$ element in each output is constrained from below by a
    $\ValMonoid$ element that contains some amount of Ada and no other assets.
    The amount of Ada that is contained in this element (and therefore, the output
    element which it constrains) depends on the
    size of the output. To get the minimum Ada amount, the size of the output is multiplied by
    the function $\var{coinsPerUTxOWord}$ applied to protocol parameters
    (see Section~\ref{sec:value-size} for the function definition).
    Note that this check implies that no quantity of any asset appearing in that output can be
    negative.

    In the case that $\ValMonoid = \Coin$, this constraint exactly mimics
    the $\fun{minUTxOValue}$ constraint in Shelley, see \ref{sec:min-value}.

    \item The serialized size of the $\ValMonoid$ element in each output is no greater than $\mathsf{MaxValSize}$
    (specified in Section~\ref{sec:value-size}).
    This ensures that each individual output is never so large that any transaction carrying all the
    witness data (eg. large scripts, etc.) necessary for spending such an output will exceed the transaction size limit.
    See Section~\ref{sec:value-size} for details. Note that this precondition can be assumed to
    hold for the Token algebra $\Coin$, as it is a single integer.
\end{itemize}

Note that updating the $\UTxO$ with the inputs and the outputs of the transaction
looks the same as in the Shelley rule. There is a type-level difference however, as
the outputs of a transaction contain an element of $\ValMonoid$, rather than
$\Coin$.


\begin{figure}[htb]
  \begin{equation}\label{eq:utxo-inductive-shelley}
    \inference[UTxO-inductive]
    { \var{txb}\leteq\txbody{tx}
      & \hldiff{\fun{ininterval}~\var{slot}~(\fun{txvldt}~{tx})}
      \\ \txins{txb} \neq \emptyset
      & \minfee{pp}{tx} \leq \txfee{txb}
      & \txins{txb} \subseteq \dom \var{utxo}
      \\
      \consumed{pp}{utxo}~{txb} = \produced{pp}{stpools}~{txb}
      \\
      ~
      \\
      {
        \begin{array}{r}
          \var{slot} \\
          \var{pp} \\
          \var{genDelegs} \\
        \end{array}
      }
      \vdash \var{pup} \trans{\hyperref[fig:rules:update]{ppup}}{\fun{txup}~\var{tx}} \var{pup'}
      \\
      ~
      \\
      \hldiff{\fun{coin}~(\fun{mint}~txb)~=~0} \\
      ~\\
      \hldiff{\forall txout \in \txouts{txb},} \\
      \hldiff{\fun{getValue}~txout \geq \fun{inject}~(\fun{scaledMinDeposit}~v~(\fun{minUTxOValue}~pp))} \\~
      \\
      \hldiff{\forall txout \in \txouts{txb},} \\
      \hldiff{\fun{serSize}~(\fun{getValue}~txout) ~\leq ~\mathsf{MaxValSize}} \\~\\
      \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}{stpools}{(\txcerts{txb})} - \var{refunded}
    }
    {
      \begin{array}{r}
        \var{slot}\\
        \var{pp}\\
        \var{stpools}\\
        \var{genDelegs}\\
      \end{array}
      \vdash
      \left(
      \begin{array}{r}
        \var{utxo} \\
        \var{deposits} \\
        \var{fees} \\
        \var{pup}\\
      \end{array}
      \right)
      \trans{utxo}{tx}
      \left(
      \begin{array}{r}
        \varUpdate{(\txins{txb} \subtractdom \var{utxo}) \cup \fun{outs}~{txb}}  \\
        \varUpdate{\var{deposits} + \var{depositChange}} \\
        \varUpdate{\var{fees} + \txfee{txb}} \\
        \varUpdate{pup'}\\
      \end{array}
      \right)
    }
  \end{equation}
  \caption{UTxO inference rules}
  \label{fig:rules:utxo-shelley}
\end{figure}


\subsection*{Witnessing}

\begin{figure}[htb]
  \begin{align*}
    \fun{scriptsNeeded} & \in \UTxO \to \Tx \to \powerset{\ScriptHash} \hspace{2cm} \text{required script hashes} \\
    \fun{scriptsNeeded} &~\var{utxo}~\var{tx} = \\
    & ~~\{ \fun{validatorHash}~a \mid i \mapsto (a, \wcard) \in \var{utxo},\\
    & ~~~~~i\in\fun{txinsScript}~{(\fun{txins~\var{txb}})}~{utxo}\} \\
    \cup & ~~\{ \fun{stakeCred_{r}}~\var{a} \mid a \in \dom (\AddrRWDScr
           \restrictdom \fun{txwdrls}~\var{txb}) \} \\
      \cup & ~~(\AddrScr \cap \fun{certWitsNeeded}~{txb}) \\
      \cup & ~~\hldiff{\fun{policies}~(\fun{mint}~{txb})} \\
    & \where \\
    & ~~~~~~~ \var{txb}~=~\txbody{tx}
  \end{align*}
  \caption{Scripts Needed}
  \label{fig:functions-witnesses}
\end{figure}

Figure~\ref{fig:functions-witnesses} contains the changed definition
of the function $\fun{scriptsNeeded}$, which also collects the scripts
necessary for minting.
Recall that in Allegra, no assets can ever be minted, so there are no scripts to run that
validate minting.

The witnessing rule UTXOW only needs a minor change for verifying the metadata hash,
which is replacing the condition $\var{md} = \Nothing$ with $\var{md} = (\emptyset, \Nothing)$.