value.tex

\section{Coin and Multi-Asset Tokens}
\label{sec:coin-ma}

This section describes the type $\Value$, the operations required on
it, and its relation to $\Coin$.

When multi-asset support on the ledger is introduced, Bcc is still expected to be
the most common type of token on the ledger.
The $\Coin$ type is used to represent an amount of Bcc.
It is the only
type of token that can be used for all non-UTxO ledger accounting, including deposits,
fees, rewards, treasury, and the proof of stake protocol.

\begin{figure*}[t!]
  \emph{Abstract Types}
  %
  \begin{align*}
    \var{aname} \in& ~\AssetName & \text{Asset Names}
  \end{align*}
  %
  \emph{Derived types}
  %
  \begin{equation*}
    \begin{array}{r@{~\in~}l@{\qquad=\qquad}lr}
      \var{pid} & \PolicyID & \ScriptHash \\
      \var{quan} & \Quantity & \Z \\
      %\text{quantity of a token}\\
      \var{v}, \var{w} & \Value
      & \PolicyID \to_0 ( \AssetName \to_0 \Quantity )
%      & \text{a collection of tokens}
    \end{array}
  \end{equation*}
  %
  \emph{Abstract Functions and Values}
  %
  \begin{align*}
    \mathsf{bccPolicy} \in& ~\PolicyID & \text{Bcc Policy ID} \\
    \mathsf{bccName} \in& ~\AssetName & \text{Bcc Asset Name} \\
    \mathsf{size} \in& ~\Value\to\MemoryEstimate & \text{the size of a Value}
  \end{align*}
  \emph{Helper Functions}
  %
  \begin{align*}
    & \fun{inject} \in \Coin\to \Value \\
    & \fun{inject}~c = \lambda~\var{pid}~\var{aname}.
      \begin{cases}
        c & \var{pid} = \mathsf{bccPolicy}~\text{and}~\var{aname} = \mathsf{bccName} \\
        0 & \text{otherwise}
      \end{cases}
    \nextdef
    & \fun{coin} \in \Value \to \Coin \\
    & \fun{coin}~v = v~\mathsf{bccPolicy}~\mathsf{bccName}
    \nextdef \fun{inject} \circ \fun{coin}
    & \fun{bccOnly} \in \Value \to \Bool \\
    & \fun{bccOnly}~v =
      \begin{cases}
        \True & \fun{inject} \circ \fun{coin} = \fun{id}_{\Value} \\
        \False & \text{otherwise}
      \end{cases}
  \end{align*}
  \caption{Type Definitions and auxiliary functions for Value}
  \label{fig:defs:value}
\end{figure*}

\subsection*{Representing Multi-asset Types and Values}
We will refer to a pair of a $\PolicyID$ and an
$\AssetName$ as an $\AssetID$. The $\AssetID$ for Bcc is $(\mathsf{bccPolicy}, \mathsf{bccName})$.
This is symbolic only, no actual minting policy for Bcc exists.

The set of tokens that are referred to by the underlying monetary
policy represents the coinage that the asset supports. A multi-asset
value, $\Value$ is a finitely supported function of two variables,
$\PolicyID$ and $\AssetName$ to $\Quantity$.

\begin{itemize}
  \item $\PolicyID$ identifies monetary policies. A policy ID $\var{pid}$ is associated with a script
    $s$ such that $\fun{hashScript}~s~=~pid$. When a transaction attempts to create or destroy tokens
    that fall under the policy ID $\var{pid}$,
    $s$ verifies that the transaction
    respects the restrictions that are imposed by the monetary policy.
    See sections \ref{sec:transactions} and \ref{sec:utxo} for details.

  \item $\AssetName$ is a type used to distinguish different tokens with the same $\PolicyID$.
    Each $aname$ identifies a unique kind of token in $\var{pid}$.

  \item $\Quantity$ is an integer type that represents an amount of a specific $\AssetName$. We associate
    a term $q\in\Quantity$ with a specific token to track how much of that token is contained in a given asset value.

  \item $\Value$ is the multi-asset type that is used to represent
    a collection of tokens, including Bcc. If $(\var{pid}, \var{aname})$ is an $\AssetID$ and $v \in \Value$,
    the quantity in $v$ belonging to that $\AssetID$ is $v~\var{pid}~\var{aname}$.
    Tokens are fungible with each other if and only if they belong to the same $\AssetID$,
    i.e. they have the same $\PolicyID$ and $\AssetName$. Terms of type $\Value$ are sometimes also referred to as
    \emph{token bundles}.

  \item $\mathsf{bccPolicy}$ and $\mathsf{bccName}$ are the $\PolicyID$ and $\AssetName$ of Bcc respectively.
    It is not possible to mint any token with the $\PolicyID$ $\mathsf{bccPolicy}$, which means that every
    token in the UTxO belonging to $\mathsf{bccPolicy}$ will have $\AssetName$ $\mathsf{bccName}$.

  \item $\mathsf{size}$ returns the size (in units of memory, eg. bytes or words) of a $\Value$.
  We give this function, alongside implementation-specific constants we have used in it in Section \ref{sec:value-size}.

  \item $\fun{inject}$ and $\fun{coin}$ convert between the two types,
  by building a $\Value$ that only contains Bcc given by the input, and extracting
  the amount of Bcc as (a $\Coin$) from a $\Value$ respectively.
  Note that composed as

  \[\fun{coin} \circ \fun{inject} = \fun{id}_{\Coin}\]

  these functions give the identity on $\Coin$, but composed in the opposite order as

  \[\fun{inject} \circ \fun{coin}\]

  they return a $\Value$ containing only the Bcc tokens contained in the original $\Value$.

  \item $\fun{bccOnly}$ returns $\True$ if a given $\Value$ contains only Bcc.
\end{itemize}

\subsection*{Value Operations and Partial Order}
We require some operations on $\Value$, including equality, addition and $\leq$ comparison.

Addition and binary relations are extended pointwise from $\Coin$ to $\Value$, so if $R$ is a binary relation defined on $\Coin$, like $=$ or $\leq$, and $v, w$ are values, we define

\[ v~R~w :\Leftrightarrow \forall~\var{pid}~\var{aname}, (v~\var{pid}~\var{aname})~R~(w~\var{pid}~\var{aname}) \]
\[ (v + w)~\var{pid}~\var{aname} := (v~\var{pid}~\var{aname}) + (w~\var{pid}~\var{aname}). \]