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{\Value} \\
    & \fun{ubalance} ~ utxo = \hldiff{\sum_{\wcard\mapsto\var{u}\in~\var{utxo}} \fun{getValue}~\var{u}}
  \end{align*}
  %
  \emph{Produced and Consumed Calculations}
  \begin{align*}
    & \fun{consumed} \in \PParams \to \UTxO \to \TxBody \to \hldiff{\Value} \\
    & \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{\Value} \\
    & \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 Bcc 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 Sophie
    counterparts, with the following changes: 1) They return elements of $\Value$, 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-Bcc tokens, since they
are put in and taken out of circulation by the users themselves?

For the following discussion, we focus on a single arbitrary
$\var{pid}$ that is not $\mathsf{bccPolicy}$. If a transaction $\var{tx}$
does not mint any tokens with policy ID $\var{pid}$, the preservation
of value reduces to an equation that the sum of inputs and the sum of
outputs are equal, which is exactly the same condition as for Sophie,
except that there are no administrative fields. If a transactions
mints tokens of that policy ID, then the sum of inputs and the sum of
outputs will differ, and that difference has to be exactly the value
of the $\fun{mint}$ field. Note that this means that the
$\fun{mint}$ field can also contain negative quantities.

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 amount of tokens on the
ledger, and minting a negative quantity reduces the amount of tokens on
the ledger.

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

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-sophie}, we give the UTXO transition rule,
updated for multi-asset support. There are the following changes to the preconditions
of this rule as compared to the original Sophie 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
  Sophie), the value in the $\fun{mint}$ field is taken into account.

  \item The transaction is not minting any Bcc.

  \item The $\Value$ in each output is constrained from below by a
    $\Value$ that contains some amount of bcc and no other tokens.
    The amount of bcc that is contained in the constraint $\Value$ (and
    hence the $\Value$ in the output itself must contain at least as much) depends on the
    size of the output. To get the minimum bcc amount, the size of the output is multiplied by
    the function $\var{bccPerUTxOWord}$ applied to protocol parameters
    (see Section~\ref{sec:value-size} for the function definition).
    Note that this check implies that no quantity of any token appearing in that output can be
    negative.

    \item The serialized size of the $\Value$ 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.
\end{itemize}

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


\begin{figure}[htb]
  \begin{equation}\label{eq:utxo-inductive-sophie}
    \inference[UTxO-inductive]
    { \var{txb}\leteq\txbody{tx}
      & \hldiff{\fun{ininterval}~\var{slot}~(\fun{txvld}{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{\mathsf{bccPolicy}~\notin \supp{\fun{mint}~txb}} \\
      ~\\
      \hldiff{\forall txout \in \txouts{txb},} \\
      \hldiff{\fun{getValue}~txout \geq} \\
      \hldiff{\fun{inject}~(\fun{max}~(\var{minUTxOValue}~pp,~\fun{utxoEntrySize}~{txout} * \fun{bccPerUTxOWord}~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-sophie}
\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{\supp~(\fun{mint}~\var{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.

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