%% Extended UTXO Specification
\newcommand\version{-1}

\title{The Extended UTXO Ledger Model}

\pagestyle{plain}
\date{11th March 2020}

\author{}

\documentclass[a4paper]{article}

% correct bad hyphenation here
\hyphenation{}

\usepackage{natbib}
\usepackage{url}

% *** MATHS PACKAGES ***
%
\usepackage[cmex10]{amsmath}
\usepackage{amssymb}
\usepackage{stmaryrd}
\usepackage{amsthm}

% *** ALIGNMENT PACKAGES ***
%
\usepackage{array}
\usepackage{float}  %% Try to improve placement of figures.  Doesn't work well with subcaption package.
\usepackage{subcaption}
\usepackage{caption}

\usepackage{subfiles}
\usepackage{geometry}
\usepackage{listings}
\usepackage[dvipsnames]{xcolor}
\usepackage{verbatim}
\usepackage{alltt}

%\usepackage{todonotes}
\usepackage[disable]{todonotes}

% These have to go at the end of the packages.
\usepackage[colorlinks=true,linkcolor=MidnightBlue,citecolor=ForestGreen,urlcolor=Plum]{hyperref}
\usepackage[capitalise, noabbrev]{cleveref}

% Mild hack to get cleveref to refer to things as "Rules": we alias the
% enumerate counters to "rule". This would be annoying if we ever wanted to
% refer to items or lists as something other than "rule", but we don't.
\crefname{rule}{rule}{rules}
\crefname{rule}{Rule}{Rules}
\crefalias{enumi}{rule}
\crefalias{enumii}{rule}

% Stuff for splitting figures over page breaks
%\DeclareCaptionLabelFormat{continued}{#1~#2 (Continued)}
%\captionsetup[ContinuedFloat]{labelformat=continued}

% *** MACROS ***

% A command for making notes with bold titles and an independent
% numbering system.  This is used for a list of notes in the appendix.
\newcounter{note}
\newcommand{\note}[1]{
  \bigskip
  \refstepcounter{note}
  \noindent\textbf{Note \thenote. #1}
}

\newcommand{\todochak}[1]{\todo[inline,color=purple!40,author=chak]{#1}}
\newcommand{\todompj}[1]{\todo[inline,color=yellow!40,author=Michael]{#1}}
\newcommand{\todokwxm}[1]{\todo[inline,color=blue!20,author=kwxm]{#1}}
\newcommand{\todojm}[1]{\todo[inline,color=purple!40,author=Jann]{#1}}

\newcommand{\red}[1]{\textcolor{red}{#1}}
\newcommand{\redfootnote}[1]{\red{\footnote{\red{#1}}}}
\newcommand{\blue}[1]{\textcolor{blue}{#1}}
\newcommand{\bluefootnote}[1]{\blue{\footnote{\blue{#1}}}}

%% A version of ^{\prime} for use in text mode
\makeatletter
\DeclareTextCommand{\textprime}{\encodingdefault}{%
  \mbox{$\m@th'\kern-\scriptspace$}%
}
\makeatother

\renewcommand{\i}{\textit}  % Just to speed up typing: replace these in the final version
\renewcommand{\t}{\texttt}  % Just to speed up typing: replace these in the final version
\newcommand{\s}{\textsf}  % Just to speed up typing: replace these in the final version
\newcommand{\msf}[1]{\ensuremath{\mathsf{#1}}}
\newcommand{\mi}[1]{\ensuremath{\mathit{#1}}}

%% A figure with rules above and below.
\newcommand\rfskip{7pt}
\newenvironment{ruledfigure}[1]{\begin{figure}[#1]\hrule\vspace{\rfskip}}{\vspace{\rfskip}\hrule\end{figure}}

%% Various text macros
\newcommand{\true}{\textsf{true}}
\newcommand{\false}{\textsf{false}}

\newcommand{\hash}[1]{\ensuremath{#1^{\#}}}

\newcommand{\List}[1]{\ensuremath{\s{List}[#1]}}
\newcommand{\Set}[1]{\ensuremath{\s{Set}[#1]}}
\newcommand{\FinSet}[1]{\ensuremath{\s{FinSet}[#1]}}
\newcommand{\Interval}[1]{\ensuremath{\s{Interval}[#1]}}
\newcommand{\FinSup}[2]{\ensuremath{\s{FinSup}[#1,#2]}}
\newcommand{\support}{\msf{support}}

\newcommand{\script}{\ensuremath{\s{Script}}}
\newcommand{\scriptAddr}{\msf{scriptAddr}}
\newcommand{\ctx}{\ensuremath{\s{Context}}}
\newcommand{\toData}{\ensuremath{\s{toData}}}
\newcommand{\mkContext}{\ensuremath{\s{mkContext}}}

% Macros for eutxo things.
\newcommand{\TxId}{\ensuremath{\s{TxId}}}
\newcommand{\txId}{\msf{txId}}
\newcommand{\txrefid}{\mi{id}}
\newcommand{\Address}{\ensuremath{\s{Address}}}
\newcommand{\DataHash}{\ensuremath{\s{DataHash}}}
\newcommand{\hashData}{\msf{dataHash}}
\newcommand{\idx}{\mi{index}}
\newcommand{\inputs}{\mi{inputs}}
\newcommand{\outputs}{\mi{outputs}}
\newcommand{\forge}{\mi{forge}}
\newcommand{\fee}{\mi{fee}}
\newcommand{\addr}{\mi{addr}}
\newcommand{\val}{\mi{value}}  %% \value is already defined

\newcommand{\validator}{\mi{validator}}
\newcommand{\redeemer}{\mi{redeemer}}
\newcommand{\datum}{\mi{datum}}
\newcommand{\datumHash}{\mi{datumHash}}
\newcommand{\datumWits}{\mi{datumWitnesses}}
\newcommand{\Data}{\ensuremath{\s{Data}}}

\newcommand{\outputref}{\mi{outputRef}}
\newcommand{\txin}{\mi{in}}
\newcommand{\id}{\mi{id}}
\newcommand{\lookupTx}{\msf{lookupTx}}
\newcommand{\getSpent}{\msf{getSpentOutput}}

\newcommand{\slotnum}{\ensuremath{\s{SlotNumber}}}
\newcommand{\spent}{\msf{spentOutputs}}
\newcommand{\unspent}{\msf{unspentOutputs}}
\newcommand{\txunspent}{\msf{unspentTxOutputs}}
\newcommand{\eutxotx}{\msf{Tx}}

\newcommand{\qty}{\ensuremath{\s{Quantity}}}
\newcommand{\token}{\ensuremath{\s{Token}}}
\newcommand{\currency}{\ensuremath{\s{CurrencyId}}}
\newcommand{\nativeCur}{\ensuremath{\mathrm{nativeC}}}
\newcommand{\nativeTok}{\ensuremath{\mathrm{nativeT}}}

\newcommand{\qtymap}{\ensuremath{\s{Quantities}}}

\newcommand\B{\ensuremath{\mathbb{B}}}
\newcommand\N{\ensuremath{\mathbb{N}}}
\newcommand\Z{\ensuremath{\mathbb{Z}}}
\renewcommand\H{\ensuremath{\mathbb{H}}}
%% \H is usually the Hungarian double acute accent
\newcommand{\emptyBs}{\ensuremath{\emptyset}}

\newcommand{\emptymap}{\ensuremath{\{\}}}


%% ------------- Start of document ------------- %%

\begin{document}
\maketitle

\section{Introduction: The Extended UTXO Model}
\label{sec:intro}
The Cardano blockchain~\citep{Cardano, Cardano-ledger-spec} uses a
variant of the \textit{Unspent Transaction Output} (UTXO) model used
by Bitcoin.  Transactions consume \textit{unspent outputs} (UTXOs)
from previous transactions and produce new outputs which can be used
as inputs to later transactions.  Unspent outputs are the liquid funds
on the blockchain. Users do not have individual accounts, but rather
have a software \textit{wallet} on a smartphone or PC which manages
UTXOs on the blockchain and can initiate transactions involving UTXOs
owned by the user.  Every core node on the blockchain maintains a
record of all of the currently unspent outputs, the \textit{UTXO set};
when outputs are spent, they are removed from the UTXO set.

This document contains a description of some extensions of the
UTXO model: the main aim of these extensions is to facilitate the
implementation of \textit{smart contracts}, programs which perform
automated and irrevocable transfer of funds on the blockchain, subject
to certain conditions being met.  A smart contract may involve
multiple transactions, and our aim is to define a transaction model
which enables the implementation of highly expressive contracts.

An important feature of our UTXO models is \textit{scripts},
programs which run on the blockchain to check the validity of
transactions.  In Cardano, scripts will be programs in the Plutus Core
language~\citep{Plutus-Core-spec}. The Extended UTXO models are largely
agnostic as to the scripting language.


\subsection{Structure of the document}
\label{sec:doc-structure}
The papers~\citep{Zahnentferner18-Chimeric} and
\citep{Zahnentferner18-UTxO} give a formal specification of a basic
UTXO model. See \cref{note:basic-utxo} for some background on
this model.

\medskip
\noindent This document proposes two extensions of the basic UTXO
model (EUTXO stands for \textit{Extended UTXO}):

\begin{itemize}
  \item \textbf{EUTXO-1} (\cref{sec:eutxo-1}): this extends the
    basic UTXO model with enhanced scripting features, allowing the
    implementation of complex smart contracts.
  \item \textbf{EUTXO-2} (\cref{sec:eutxo-2}): this adds
    multicurrency features to EUTXO-1, allowing users to define
    \textit{custom currencies} and \textit{non-fungible tokens}.
\end{itemize}


\medskip

The rationale for providing two separate extensions is that (1)
introducing the extensions separately clarifies the structure of the
models and makes it easier to explain the relevant design decisions,
and (2) it is possible that a particular blockchain might not need the
full power of EUTXO-2 and so could use the simpler EUTXO-1 model,
perhaps with less computational overhead.

\medskip

For ease of reference we have kept exposition to a minimum in the main
text.  Some aspects of the models are explained in more detail
in \cref{appendix:comments}, with cross-references in the main
text.  Further explanation and many examples are contained in the
book~\citep{Plutus-book}.


\section{Notation}
This section defines some basic notation.  We generally follow the
notation established by \citep{Zahnentferner18-UTxO}, except that we make use
of finitely-supported functions in most places that \citep{Zahnentferner18-UTxO}
use maps.

\subsection{Basic types and operations}
\label{sec:basic-notation}

This section describes some types, notation, and
conventions used in the remainder of the document.

\begin{itemize}
\item Types are typeset in $\mathsf{sans~serif}$.

\item \B{} denotes the type of booleans, $\{\false, \true\}$.
\item \N{} denotes the type of natural numbers, $\{0, 1, 2, \ldots\}$.
\item \Z{} denotes the type of integers, $\{\ldots, -2, -1, 0, 1, 2, \ldots\}$.
\item We regard $\N$ as a subtype of $\Z$ and convert freely between
  natural numbers and non-negative integers.
\item \H{} denotes the type of bytestrings,
  $\bigcup_{n=0}^{\infty}\{0,1\}^{8n}$.

  \emptyBs{} denotes the empty bytestring.

  A bytestring is a sequence of 8-bit bytes: the symbol $\H$ is used because bytestrings are often
  presented as sequences of hexadecimal digits.

\item If a type $M$ is a monoid, we use $+$ for the monoidal operation and $0$
  for the unit of the monoid.

  If $M$ is a commutative monoid, we use $\sum$ for the extension of $+$ to a finite set of elements of
  type $M$.

  If $M$ is a group, we use $-$ for the group
  inverse operation.

  This should never be ambiguous.

\item A record type with fields $\phi_1, \ldots, \phi_n$ of types $T_1,
  \ldots, T_n$ is denoted by $(\phi_1 : T_1, \ldots, \phi_n : T_n)$.

  If $t$ is a value of a record type $T$ and $\phi$ is the name
  of a field of $T$ then $t.\phi$ denotes the value of $\phi$ for
  $t$.

\item If $T$ is a type then $\FinSet{T}$ is the type of finite sets
  with elements of type $T$.

\item A list $l$ of type $\List{T}$ is either the empty list
  $[]$ or a list $e :: l$ with $head$ $e$ of type $T$ and
  $tail$ $l$ of type $\List{T}$. A list has only a finite
  number of elements.  We denote the $i$th element of a list $l$ by
  $l[i]$ and the length of $l$ by $\left|l\right|$.

\item $x \mapsto f(x)$ denotes an anonymous function.

\item A cryptographic collision-resistant hash of a value $c$ is denoted $\hash{c}$.

\item For a type $A$ which forms a total order, $\Interval{A}$ is the
  type of intervals over that type. Intervals may be bounded or
  unbounded, and open or closed at either end. The type $\Interval{A}$
  forms a lattice under inclusion.
\end{itemize}

\subsection {Finitely-supported functions}
\label{sec:fsfs}

Finitely-supported functions are a generalisation of maps to monoidal values.
They always return an answer (which will in all but finitely many cases be
zero), and can be queried for the set of non-zero points in their domain.

For two types $K$ and $V$ where $V$ is a monoid, $\FinSup{K}{V}$ denotes the type of
\textit{finitely-supported functions} from $K$ to $V$. That is, there is a
function $\support : \FinSup{K}{V} \rightarrow \FinSet{K}$ such that
$k \in \support(f) \Leftrightarrow f(k) \neq 0$.

Equality on finitely-supported functions is defined as pointwise equality. Similarly,
if $V$ has a partial order, then a partial order on finitely-supported functions
is also defined pointwise.

If the type $M$ is a monoid then we define the sum of two finitely-supported
functions
$f, g \in \FinSup{K}{M}$ to be the function $f+g \in \FinSup{K}{M}$ given by
\[(f+g)(k) = f(k) + g(k) \]
Note that the type $\FinSup{K}{M}$ is a monoid with this
operation, and the empty function as
identity element.

If the type $M$ is a group, then we can
similarly define the inverse of a finitely-supported function $f$ as
the function $(-f)$ with the same support, given by
\[ (-f)(k) = -f(k) \]
Again, $\FinSup{K}{M}$ is a group with this operation.

See \cref{note:finitely-supported-functions} for discussion of using
finitely-supported functions computationally.

\subsection{The \Data{} type}
We also define a type \Data{} which can be used to pass information
into scripts in a type-safe manner: see \cref{fig:data-defn}. The
definition is given here in EBNF form, but can easily be translated to
a Haskell type, for instance.

\begin{ruledfigure}{H}
\begin{alltt}
  \Data =
      "I" \(\Z\)
    | "B" \(\H\)
    | "Constr" \(\N (\List{\Data})\)
    | "List" \(\List{\Data}\)
    | "Map" \(\List{\Data\times\Data}\)
\end{alltt}
\caption{The \Data{} type}
\label{fig:data-defn}
\end{ruledfigure}

\noindent Thus values of type \Data{} are nested sums and products
built up recursively from the base types of integers and
bytestrings. This allows one to encode a large variety of first-order
data structures: for example, we could encode values of Haskell's
\verb|Maybe Integer| type using \verb|Constr 0 []| to represent
\verb|Nothing| and \verb|Constr 1 [I 41]| to encode \verb|Just 41|.


The \texttt{List} and \texttt{Map} constructors are strictly
redundant, but are included for convenience to allow straightforward
encoding of lists and records.

We assume that the scripting language has the ability to parse values
of type \Data{}, converting them into a suitable internal representation.


\section{EUTXO-1: Enhanced scripting}
\label{sec:eutxo-1}
The EUTXO-1 model adds the following new features to the model
proposed in~\citep{Zahnentferner18-UTxO}:

\begin{itemize}
\item Every transaction has a \textit{validity interval}, of type $\Interval{\slotnum}$.
  A core node will only process the transaction if
  the current slot number lies within the transaction's validity
  interval.

\item The redeemer script of~\citet{Zahnentferner18-UTxO} has been
  replaced with a \textit{redeemer object} (\textit{redeemer} for short) of
  type \Data{}.

\item Each unspent output now has an object of type \Data{} associated
  with it: we call this the output's \textit{datum} (or occasionally
  \emph{datum object}) (see \cref{note:datum}).  Only the hash
  $\datumHash$ of the datum is stored in the output: the full value
  must be provided when the output is spent, much like the validator.

\item Validator scripts make use of information about the pending
  transaction (ie, the transaction which is just about to take place,
  assuming that validation succeeds). This information is contained in
  a structure which we call \ctx{} (see \cref{sec:context} for its
  definition).  We may refer to this information as the
  \textit{validation context} in cases where ambiguity may arise.

\item Validation of an output is performed by running the validator
  with three inputs:
  \begin{enumerate}
  \item the datum,
  \item the redeemer,
  \item the \ctx{} information, encoded as \Data{}.
  \end{enumerate}

\end{itemize}

\todokwxm{There's the issue about whether validators return
  \texttt{true/false} or \texttt{()/Error}. Remember to fix this when things have settled down.}

\subsection{A Formal Description of the EUTXO-1 Model}
\label{section:eutxo-spec}

In this section we give a formal description of the EUTXO-1 model.  The
description is given in a straightforward set-theoretic form, which
(a) admits an almost direct translation into Haskell, and (b) should
easily be amenable to mechanical formalisation.  This will potentially
allow us to argue formally about smart contracts and to develop tools
for automatic contract analysis.

The definitions in this section are essentially the definitions of
UTXO-based cryptocurrencies with scripts from
\citep{Zahnentferner18-UTxO}, except that we have added the new
features mentioned above (the validity interval, the datum
and the \ctx{} structure), changed the type of the redeemer from
\script{} to \Data{}, and used finitely-supported functions in place
of maps.

\Cref{fig:eutxo-1-types} lists the types and operations used in the
the basic EUTXO model. Some of these are defined, the others must be provided by
the ledger.
%%
\begin{ruledfigure}{H}
  \begin{displaymath}
  \begin{array}{rll}
    \multicolumn{3}{l}{\textsc{Ledger primitives}}\\
    \qty{} && \mbox{an amount of currency}\\
    \slotnum && \mbox{a slot number}\\
    \Address && \mbox{the ``address'' of a script in the blockchain}\\
    \DataHash && \mbox{the hash of an object of type \Data{}}\\
    \TxId && \mbox{the identifier of a transaction}\\
    \txId : \eutxotx \rightarrow \TxId && \mbox{a function computing the identifier of a transaction}\\
    \script && \mbox{the (opaque) type of scripts}\\
    \scriptAddr : \script \rightarrow \Address && \mbox{the address of a script}\\
    \hashData : \Data \rightarrow \DataHash && \mbox{the hash of a data object}\\
    \llbracket \cdots \rrbracket : \script \rightarrow \Data \times \Data \times
    \Data \rightarrow \B && \mbox{application of a script to its arguments}\\
    \\
    \multicolumn{3}{l}{\textsc{Defined types}}\\
    \s{Output } &=&(\addr: \Address,\\
                & &\ \val: \qty,\\
                & &\ \datumHash: \DataHash)\\
    \\
    \s{OutputRef } &=&(\txrefid: \TxId, \idx: \s{Int})\\
    \\
    \s{Input } &=&(\outputref: \s{OutputRef},\\
               & &\ \validator: \script,\\
               & &\ \datum: \Data,\\
               & &\ \redeemer: \Data)\\
     \\
     \eutxotx\s{ } &=&(\inputs: \FinSet{\s{Input}},\\
                   & &\ \outputs: \List{\s{Output}},\\
                   & &\ \i{validityInterval}: \Interval{\slotnum},\\
                   & &\ \datumWits: \FinSup{\DataHash}{\Data},\\
                   & &\ \fee: \qty,\\
                   & &\ \forge: \qty) \\
     \\
     \s{Ledger } &=&\!\List{\eutxotx}\\
  \end{array}
  \end{displaymath}
  \caption{Primitives and basic types for the EUTXO-1 model}
  \label{fig:eutxo-1-types}
\end{ruledfigure}

\subsubsection{Remarks}
\paragraph{ETUXO-1 on Cardano.}
The Cardano implementation of EUTXO-1 uses the primitives given in
\cref{fig:eutxo-1-types-cardano}.

\begin{ruledfigure}{H}
  \begin{displaymath}
  \begin{array}{rll}
    \qty{} &=& \Z\\
    \slotnum &=& \N\\
    \Address &=& \H\\
    \DataHash &=& \H\\
    \TxId &=& \H\\
    \txId : \eutxotx \rightarrow \TxId &=& t \mapsto \hash{t}\\
    \script &=& \mbox{a Plutus Core program}\\
    \scriptAddr : \script \rightarrow \Address &=& s \mapsto \hash{s}\\
    \llbracket \cdots \rrbracket : \script \rightarrow \Data \times \Data \times
    \Data \rightarrow \B &=& \mbox{typechecking the program and running}\\
                             &&\mbox{the Plutus Core interpreter}\\
  \end{array}
  \end{displaymath}
  \caption{Cardano primitives for the EUTXO-1 model}
  \label{fig:eutxo-1-types-cardano}
\end{ruledfigure}

\paragraph{Inputs and outputs.} Note that a transaction has a
\textsf{Set} of inputs but a \textsf{List} of outputs. See
\cref{note:inputs-and-outputs} for a discussion of why.

\paragraph{Validator addresses in outputs.} The \textit{addr} field
of an output should contain the address of the validator script for
that output: this requirement is enforced in
\cref{rule:validator-scripts-hash} of
\cref{fig:eutxo-1-validity} below.

\paragraph{Scripts and hashes.} Note that datum objects and validators are
provided as parts of transaction inputs, even though they are
conceptually part of the output being spent.  The reasons for
this are explained in \cref{note:scripts}.

\paragraph{Datum witnesses.} The transaction may include the full
value of the datum for each output that it creates.  See
\cref{note:datum-witnesses} for more discussion.

\paragraph{Fees.}  Users are charged a fee for the on-chain storage
and execution costs of a transaction, and this is included in the
EUTXO models.  The details are not important for the purposes of the
models, but see \cref{note:fees} for some more discussion.

\paragraph{Special types of transaction.} In a practical
implementation it might be useful to include special cases for common
transaction types such as pay-to-pukbey transactions in order to
increase efficiency and decrease storage requirements (and hence
reduce fees).  These have been omitted from this model because it
subsumes all of the other transaction types we're likely to encounter,
and also because it's difficult to give a definitive list of such
special cases.

\paragraph{Ledger structure.} We model a ledger as a simple
list of transactions: a real blockchain ledger will be more complex
than this, but the only property that we really require is that
transactions in the ledger have some kind of address which allows them
to be uniquely identified and retrieved.

\subsubsection{The \ctx{} type}
\label{sec:context}
Recall from the introduction to \cref{sec:eutxo-1} that when a
transaction input is being validated, the validator is supplied
with an object of type \ctx{} which contains information about the
pending transaction.  The \ctx{} type for the current version of
EUTXO-1 is defined in \cref{fig:ptx-1-types}, along with some
related types.

\begin{ruledfigure}{H}
  \begin{displaymath}
  \begin{array}{rll}
    \s{OutputInfo } &=&(\val: \qty,\\
                    & &\ \i{validatorHash}: \Address,\\
                    & &\ \datumHash: \DataHash)\\
    \\
    \s{InputInfo } &=&(\outputref: \s{OutputRef},\\
                   & &\ \i{validatorHash}: \Address,\\
                   & &\ \i{datumHash}: \DataHash,\\
                   & &\ \i{redeemerHash}: \DataHash,\\
                   & &\ \val: \qty)\\
     \\
     \ctx\s{ } &=&(\i{inputInfo}: \List{\s{InputInfo}},\\
               & &\ \i{thisInput}: \N,\\
               & &\ \i{outputInfo}: \List{\s{OutputInfo}},\\
               & &\ \i{validityInterval}: \Interval{\slotnum},\\
               & &\ \datumWits: \FinSup{\DataHash}{\Data},\\
               & &\ \fee: \qty,\\
               & &\ \forge: \qty)\\
     \\
     \mkContext: \eutxotx \times \s{Input} \times \s{Ledger} \rightarrow\\
      \ctx &=& \mbox{\parbox[t]{6cm}{summarises a transaction in the context of an input and a ledger state}}\\
      \\
      %% Without the break after the right arrow, the = sign is well
      %% over halfway across the pages, which is horrible. This makes
      %% it a bit better, but not much.
     \toData: \ctx \rightarrow \Data &=& \mbox{encodes a \ctx{} as \Data}
  \end{array}
  \end{displaymath}
  \caption{The \ctx{} type for the EUTXO-1 model}
  \label{fig:ptx-1-types}
\end{ruledfigure}

\subsection{Remarks}
\paragraph{The contents of \ctx{}.}
The \ctx{} type is essentially a summary of the information contained
in the $\eutxotx$ type in \cref{fig:eutxo-1-types}. The \fee{},
\forge{}, and \i{validityInterval} fields are copied directly from the
pending transaction.  The \i{outputInfo} field contains information
about the outputs which will be produced if the pending transaction
validates successfully: it contains only the address of the relevant
validator, and the hash of the datum.\footnote{See
  \cref{note:datum-objects-in-ptx} for further explanation.}  The
\i{inputInfo} field contains information about the inputs to the
pending transaction, but provides only the hashes of the validators
and redeemers for the inputs.  The \i{thisInput} field
is an index pointing to the element of \i{inputInfo} relating to the
input currently undergoing validation.
% Note: in the code at the moment, the hashes of the validator
% and redeemer scripts in inputInfo are allowed to be absent
% when we have pubkey inputs.  We're ignoring that special case here.

\paragraph{Defining \mkContext{} and \toData.}
Assuming we have an
appropriate hashing function, it is straightforward to define \mkContext.
For the implementation of \toData, note that the $inputs$ field is a
\FinSet{} in \eutxotx{}, but a \List{} in \ctx{}. Therefore \toData{} has to introduce
an ordering of the transaction inputs. Contract authors cannot make
any assumptions about this ordering and therefore should ensure that
their scripts pass or fail regardless of what particular permutation
of transaction inputs they are presented with.

Apart from that, the function \toData{} is implementation-dependent and
we will not discuss it further.

\paragraph{Determinism.}
The information provided in the \ctx{}
structure is sufficiently limited that the validation process
becomes \textit{deterministic},  which has important implications
for fee calculations.  See \cref{note:validation-determinism}
for further discussion.


\subsection{Validity of EUTXO-1 transactions}
\label{sec:eutxo-1-validity}
A number of conditions must be satisfied in order for a transaction
$t$ to be considered valid with respect to a ledger $l$.

\Cref{fig:validation-functions-1} defines some auxiliary functions used in validation.
\begin{ruledfigure}{H}
  \begin{displaymath}
  \begin{array}{lll}
  \multicolumn{3}{l}{\lookupTx : \s{Ledger} \times \TxId \rightarrow \eutxotx{}}\\
  \lookupTx(l,id) &=& \textsf{find}(l, tx \mapsto \txId(tx) = id)\\
  \\
  \multicolumn{3}{l}{\txunspent : \eutxotx \rightarrow \FinSet{\s{OutputRef}}}\\
  \txunspent(t) &=& \{(\txId(t),1), \ldots, (\txId(id),\left|t.outputs\right|)\}\\
  \\
  \multicolumn{3}{l}{\unspent : \s{Ledger} \rightarrow \FinSet{\s{OutputRef}}}\\
  \unspent([]) &=& \emptymap \\
  \unspent(t::l) &=& (\unspent(l) \setminus t.\inputs) \cup \txunspent(t)\\
  \\
  \multicolumn{3}{l}{\getSpent : \s{Input} \times \s{Ledger} \rightarrow \s{Output}}\\
  \getSpent(i,l) &=& l\langle i.\outputref.\id \rangle.\outputs[i.\outputref.\idx]
  \end{array}
  \end{displaymath}
  \caption{Auxiliary functions for EUTXO-1 validation}
  \label{fig:validation-functions-1}
\end{ruledfigure}

\noindent The function $\lookupTx(l,id)$ looks up the unique
transaction $T$ whose $\TxId$ is $id$, and can of course
fail. However, during validation
Rule~\ref{rule:all-inputs-refer-to-unspent-outputs} of
Figure~\ref{fig:eutxo-1-validity} ensures that all of the transaction
inputs refer to existing unspent outputs, and in these circumstances
$\lookupTx$ will always succeed for the transactions of interest.

We can now define what it means for a transaction $t$ of
type $\eutxotx$ to be valid for a ledger $l$ during the slot $\msf{currentSlot}$: see
\cref{fig:eutxo-1-validity}.  Our definition combines
Definitions 6 and 14 from \citep{Zahnentferner18-UTxO}, differing from
the latter in \cref{rule:all-inputs-validate}.
\todokwxm{Check this.}

\begin{ruledfigure}{H}
\begin{enumerate}

\item
  \label{rule:slot-in-range}
  \textbf{The current slot is within the validity interval}
  \begin{displaymath}
    \msf{currentSlot} \in t.\i{validityInterval}
  \end{displaymath}

\item
  \label{rule:all-outputs-are-non-negative}
  \textbf{All outputs have non-negative values}
  \begin{displaymath}
    \textrm{For all } o \in t.\outputs,\ o.\val \geq 0
  \end{displaymath}

\item
  \label{rule:all-inputs-refer-to-unspent-outputs}
  \textbf{All inputs refer to unspent outputs}
  \begin{displaymath}
    \{i.\outputref: i \in t.\inputs \} \subseteq \unspent(l).
  \end{displaymath}

\item
  \label{rule:forging}
  \textbf{Forging} \\
    A transaction with a non-zero \forge{}
    field is only valid if the ledger $l$ is empty (that
    is, if it is the initial transaction).

\item
  \label{rule:value-is-preserved}
  \textbf{Value is preserved}
  \begin{displaymath}
    t.\forge + \sum_{i \in t.\inputs} \getSpent(i, l).\val = t.\fee + \sum_{o \in t.\outputs} o.\val
  \end{displaymath}

\item
  \label{rule:no-double-spending}
  \textbf{No output is double spent}
  \begin{displaymath}
    \textrm{If } i_1, i_2 \in t.\inputs \textrm{ and }  i_1.\outputref = i_2.\outputref
    \textrm{ then } i_1 = i_2.
  \end{displaymath}

\item
  \label{rule:all-inputs-validate}
  \textbf{All inputs validate}
  \begin{displaymath}
    \textrm{For all } i \in t.\inputs,\ \llbracket
    i.\validator\rrbracket (i.\datum,\, i.\redeemer,\,  \toData(\mkContext(t,i,l))) = \true.
  \end{displaymath}

\item
  \label{rule:validator-scripts-hash}
  \textbf{Validator scripts match output addresses}
  \begin{displaymath}
    \textrm{For all } i \in t.\inputs,\ \scriptAddr(i.\validator) = \getSpent(i, l).\addr
  \end{displaymath}

\item
  \label{rule:datum-objects-hash}
  \textbf{Datum objects match output hashes}
  \begin{displaymath}
    \textrm{For all } i \in t.\inputs,\ \hashData(i.\datum) = \getSpent(i, l).\datumHash
  \end{displaymath}
  
\end{enumerate}
\caption{Validity of a transaction $t$ in the EUTXO-1 model}
\label{fig:eutxo-1-validity}
\end{ruledfigure}
\todokwxm{Do we really needs the $\llbracket\cdots\rrbracket$ business?}


\noindent We say that a ledger
$l$ is \textit{valid} if either $l$ is empty or
$l$ is of the form $t::l^{\prime}$ with
$l^{\prime}$ valid and $t$ valid for $l^{\prime}$.

In practice, validity imposes a limit on the sizes of the
$\validator$ \script{}, the $\redeemer$ and
$\datum$ \Data{} fields, and the result of \toData. The validation of a
single transaction must take place within one slot, so the evaluation
of $\llbracket ~ \rrbracket$ cannot take longer than one slot.
\todokwxm{Do we need this $\uparrow$?}

%%\newpage
\section{EUTXO-2: multicurrency support and non-fungible tokens}
\label{sec:eutxo-2}
We now extend the EUTXO-1 model further by introducing features which
allow, among other things, the implementation of new currencies and
\textit{non-fungible tokens} (NFTs).

\paragraph{Multiple currencies.} The EUTXO-2 model allows an unlimited
number of \textit{currencies}.  Each custom currency has a
unique identifier.

\todokwxm{We may wish to implement a DEX to enable exchange of custom
  currencies.  This is a little problematic in Ethereum because the
  Ether currency itself does not conform to ERC-20 and so has to be
  wrapped in another currency before it can participate in DEX trades.
  Will the fact that Ada is treated differently from custom currencies
  in EUTXO cause us difficulties here?}

\paragraph{NFTs.}
A non-fungible token (NFT) is a unique object which can be transferred
to another user, but not duplicated.  NFTs have proven useful in a
number of blockchain applications (see~\citep{ERC-721} for example);
for example, they can represent ownership of some object in a game.
We can implement NFTs as custom currencies whose supply is limited to
a single coin.

\subsection{The definition of EUTXO-2}
In order to support these extensions, we introduce several new types.
Custom currencies are represented by unique \textit{currency
  identifiers} and each currency has a number of \textit{tokens} which
partition each custom currency into a number of sub-currencies.  The
basic idea is that ordinary currencies have a single token whose
sub-currency has an unlimited supply and NFTs have a number of tokens
with the sub-currency for each token limited to a supply of one.

The changes to the basic EUTXO-1 types are now quite simple:
see \cref{fig:eutxo-2-types}.  We change the type of the $\val$ field
in the \s{Output} type to be \qtymap{}, representing values of all currencies;
we also change the type of the \forge{} field on transactions to \qtymap{}, to
allow the creation and destruction of funds in all currencies; the
supply of a currency can be reduced by forging a negative amount of that
currency, as in EUTXO-1.
\begin{ruledfigure}{H}
  \begin{displaymath}
    \begin{array}{rll}
    \multicolumn{3}{l}{\textsc{Ledger primitives}}\\
    \currency  && \mbox{an identifier for a custom currency}\\
    \token     && \mbox{a type consisting of identifiers for individual tokens}\\
    \\
    \multicolumn{3}{l}{\textsc{Defined types}}\\
    \qtymap   &=& \FinSup{\currency}{\FinSup{\token}{\qty}}\\
    \\
    \s{Output}_2 &=&(\addr: \Address,\\
                 & &\ \val: \qtymap\\
                 & &\ \datumHash: \DataHash)\\
    \\
    \s{OutputRef}_2 &= &(\txrefid: \TxId, \idx: \s{Int})\\
    \\
    \s{Input}_2 &=&( \outputref: \sf{OutputRef}_2,\\
                & &\ \validator: \script,\\
                & &\ \datum: \Data,\\
                & &\ \redeemer: \Data)\\
    \\
    \eutxotx_2 &=&(\inputs: \FinSet{\s{Input}_2},\\
               & &\ \outputs: \List{\s{Output}_2},\\
               & &\ \i{validityInterval}: \Interval{\slotnum},\\
               & &\ \datumWits: \FinSup{\DataHash}{\Data},\\
               & &\ \fee: \qtymap,\\
               & &\ \forge: \qtymap)\\
    \\
    \s{Ledger}_2 &=&\!\List{\eutxotx_2}\\
    \end{array}
  \end{displaymath}
  \caption{Extra primitives and basic types for the EUTXO-2 model}
  \label{fig:eutxo-2-types}
\end{ruledfigure}

\subsubsection{Remarks}
\paragraph{ETUXO-2 on Cardano.}
The Cardano implementation of EUTXO-2 uses the primitives given in
\cref{fig:eutxo-2-types-cardano}.

Cardano also defines an \emph{native currency} and \emph{native currency token}.
This allows defining a native currency that behaves as a simple \qty{}. This
is used in Fig~\ref{fig:cardano-fee-validity}.
\begin{ruledfigure}{H}
  \begin{displaymath}
    \begin{array}{rll}
      \currency  &=& \H\\
      \token     &=& \H\\
      \nativeCur &=& \emptyBs\\
      \nativeTok &=& \emptyBs\\
    \end{array}
  \end{displaymath}
  \caption{Cardano primitives for the EUTXO-2 model}
  \label{fig:eutxo-2-types-cardano}
\end{ruledfigure}

\paragraph{\qtymap{}. }
The \qtymap{} type represents a collection of funds from a
number of currencies and their subcurrencies.

\qtymap{} is a finitely-supported function \emph{to} another finitely-supported
function. This is well-defined, since finitely-supported functions form a monoid.

\subsection{The \ctx{} type for EUTXO-2}
\label{sec:pendingtx-2}
The \ctx{} type must be also be updated for the EUTXO-2 model.  All
that is required is to replace \qty{} by \qtymap{} everywhere in
\cref{fig:ptx-1-types} except for the \fee{} field: for reference
the details are given in \cref{fig:ptx-2-types}.
\begin{ruledfigure}{H}
  \begin{displaymath}
  \begin{array}{rll}
    \s{OutputInfo}_2\s{ } &=&(\val: \qtymap,\\
                          & &\ \i{validatorHash}: \Address,\\
                          & &\ \datumHash: \DataHash)\\
    \\
    \s{InputInfo}_2\s{ } &=& (\outputref: \s{OutputRef},\\
                         & &\ \i{validatorHash}: \Address,\\
                         & &\ \i{datumHash}: \DataHash,\\
                         & &\ \i{redeemerHash}: \DataHash),\\
                         & &\ \val: \qtymap)\\
     \\
     \ctx_2\s{ } &=&(\i{inputInfo}: \List{\s{InputInfo}_2},\\
                 & &\ \i{thisInput}: \N,\\
                 & &\ \i{outputInfo}: \List{\s{OutputInfo$_2$}},\\
                 & &\ \i{validityInterval}: \Interval{\slotnum},\\
                 & &\ \datumWits: \FinSup{\DataHash}{\Data},\\
                 & &\ \fee: \qtymap,\\
                 & &\ \forge: \qtymap)\\
    \\
    \mkContext_2: \eutxotx_2 \times \s{Input} \times \s{Ledger} \rightarrow&\\
    
      \ctx_2 &=& \mbox{\parbox[t]{6cm}{summarises a transaction in the context of an input and a ledger state}}\\
     \\
    \toData_2: \ctx_2 \rightarrow \Data &=& \mbox{encodes a $\ctx_2$}
  \end{array}
  \end{displaymath}
  \caption{The \ctx{} type for the EUTXO-2 model}
  \label{fig:ptx-2-types}
\end{ruledfigure}

\subsection{Validity of EUTXO-2 transactions}
\label{sec:eutxo-2-validity}

\bigskip
\noindent The validity conditions from
\cref{fig:eutxo-1-validity} must also be updated to take account
of multiple currencies.

We can now adapt the definition of validity for EUTXO-1
(\cref{fig:eutxo-1-validity}) to obtain a definition of validity for
EUTXO-2: see \cref{fig:eutxo-2-validity}.

\begin{ruledfigure}{H}
\begin{enumerate}

\item
  \label{rule:slot-in-range-2}
  \textbf{The current slot is within the validity interval}
  \begin{displaymath}
    \msf{currentSlot} \in t.\i{validityInterval}
  \end{displaymath}

\item
  \label{rule:all-outputs-are-non-negative-2}
  \textbf{All outputs have non-negative values}
  \begin{displaymath}
    \textrm{For all } o \in t.\outputs,\ o.\val \geq 0
  \end{displaymath}

\item
  \label{rule:all-inputs-refer-to-unspent-outputs-2}
  \textbf{All inputs refer to unspent outputs}
  \begin{displaymath}
    \{i.\outputref: i \in t.\inputs \} \subseteq \unspent(l).
  \end{displaymath}

\item
  \label{rule:forging-2}
  \textbf{Forging}\\
  A transaction with a non-zero \forge{} field is only
  valid if either:
  \begin{enumerate}
    \item the ledger $l$ is empty (that is, if it is the initial transaction).
    \item \label{rule:custom-forge}
      for every key $h \in \support(t.\forge)$, there
      exists $i \in t.\inputs$ with
      $$
      h = \getSpent(i,l).\addr;
      $$
      in other words, some input must spend an output
      whose address is $h$.
  \end{enumerate}

\item
  \label{rule:value-is-preserved-2}
  \textbf{Values are preserved}
  \begin{displaymath}
    t.\forge + \sum_{i \in t.\inputs} \getSpent(i, l) = t.\fee + \sum_{o \in t.\outputs} o.\val
  \end{displaymath}

\item
  \label{rule:no-double-spending-2}
  \textbf{No output is double spent}
  \begin{displaymath}
    \textrm{If } i_1, i_2 \in t.\inputs \textrm{ and }  i_1.\outputref = i_2.\outputref
    \textrm{ then } i_1 = i_2.
  \end{displaymath}

\item
  \label{rule:all-inputs-validate-2}
  \textbf{All inputs validate}
  \begin{displaymath}
    \textrm{For all } i \in t.\inputs,\ \llbracket
    i.\validator\rrbracket(i.\datum,\, i.\redeemer,\, \toData_2(\mkContext_2(t, i, l))) = \true
  \end{displaymath}

\item
  \label{rule:validator-scripts-hash-2}
  \textbf{Validator scripts match output addresses}
  \begin{displaymath}
    \textrm{For all } i \in t.\inputs,\ \scriptAddr(i.\validator) = \getSpent(i, l).\addr
  \end{displaymath}

\item
  \label{rule:datum-objects-hash-2}
  \textbf{Datum objects match output hashes}
  \begin{displaymath}
    \textrm{For all } i \in t.\inputs,\ \hashData(i.\datum) = \getSpent(i, l).\datumHash
  \end{displaymath}
  
\end{enumerate}
\caption{Validity of a transaction $t$ in the EUTXO-2 model}
\label{fig:eutxo-2-validity}
\end{ruledfigure}

\subsection{Remarks}
\paragraph{Monetary policies.} 
Rule~\ref{rule:custom-forge} can be used to enforce monetary policies
for custom currencies: see Note~\ref{note:monetary-policies} for a
detailed explanation.

\paragraph{Preservation of value over \qtymap{}.}
In \cref{rule:value-is-preserved-2},
$+$ and $\sum$ operate over \qtymap{}, which is
a finitely-supported function (which, with their operations,
are defined in \cref{sec:fsfs}). Preservation of value
in this model essentially requires that the
quantities of each of the individual currencies involved in the
transaction are preserved.

\paragraph{Preservation of value and forging.}
Recall that values in $\forge$ can
be negative whereas values in outputs must be non-negative. This allows
currency to be destroyed as well as created. The
\cref{rule:value-is-preserved-2} implies that a
transaction is invalid if it attempts to destroy more of a currency
than is actually available in its inputs.

\paragraph{Validation on Cardano.}
Cardano adds an additional rule in Fig~\ref{fig:cardano-fee-validity}, which
asserts that fees are paid exclusively in the native currency.

\begin{ruledfigure}{H}
  \textbf{Fees are paid in the native currency}
  \begin{displaymath}
    \support(t.\fee) = \{ \nativeCur \} \textrm{ and }
    \support(t.\fee(\nativeCur)) = \{ \nativeTok \}
  \end{displaymath}
  \caption{Validity of a transaction $t$ in the EUTXO-2 model}
  \label{fig:cardano-fee-validity}
\end{ruledfigure}

\subsection{The EUTXO-2 model in practice.}
See~\cite{Plutus-book} for examples of contracts which make use of the
features of the EUTXO-2 model.  See also
\cref{note:monetary-policies,note:eutxo-2-implications,note:eutxo-2-performance}
for comments on some technical aspects of the model.

\appendix
\section{Comments}
\label{appendix:comments}

\note{Computing with finitely-supported functions.}
\label{note:finitely-supported-functions}
We intend that finitely-supported functions are implemented as finite
maps, with a failed map lookup corresponding to returning 0.

However, there are two apparent difficulties:
\begin{enumerate}
  \item The domain of a map does not correspond to the support of the function:
    values may be mapped to zero, thus appearing in the domain but not the support.
  \item Pointwise equality is hard to compute.
\end{enumerate}

However, both of these are easily ameliorated. We say that a set $w$ is a \textit{weak support}
of a finitely-supported function $f$ if $\support(f) \subseteq w$. That is, a
weak support contains all the points that are non-zero, but possibly also some
points that are zero. It is easy to see that the domain of a map is a weak
support for the finitely-supported function it represents.

We can compute the support from the weak support by simply checking the function
at each value and removing those that are zero. This is potentially expensive,
but we only need to do it when we need the support, which we only do during the
computation of \cref{rule:value-is-preserved-2}.

Pointwise equality between two finitely-supported functions $f$ and $g$ is
equivalent to checking pointwise equality only over the union of $\support(f)$
and $\support(g)$; or similarly over the union of a weak support of $f$ and of
$g$. In particular, for finitely-supported functions represented as maps, we can
check pointwise equality over the union of their domains.

The same applies to checking partial ordering pointwise, which can similarly
be done over the union of the weak support.

\note{The Basic UTXO model: Outputs and scripts.}
\label{note:basic-utxo}
There is no well-defined notion of ownership for UTXOs.  In many
transactions an output will accrue to a single user who is then
entitled to spend it at a later date.  However, in general the notion
of ownership is more complex: an output of a transaction might require
the cooperation of several users before it could be spent, or it might
not be spendable until some other condition has been met (for example
a certain period of time may have to pass).  At the extremes, an
output could be spendable by anyone, or by no-one.

In order to deal with this complexity, an output can be locked by a
\textit{script}%
\footnote{In the Cardano setting, scripts are Plutus Core
  programs~\citep{Plutus-Core-spec}.}
which must be supplied with suitable evidence to unlock the output.
In the basic model, each input to a transaction comes with a
\i{validator} script which checks that the transaction is allowed to
spend the output.  In order to spend an output, the transaction
supplies an object of type $\Data$, called the \i{redeemer}, which provides
evidence that the transaction has the authority to do so;\footnote{The
  validator plays a role similar to that of BitCoin's
  \texttt{scriptPubKey} and the redeemer to \texttt{scriptSig}.
} a process called \i{validation} is then performed which checks that
the redeemer satisfies the conditions required by the validator.
Before a transaction can proceed, all inputs must be successfully
validated: if one or more inputs fails to validate then the
transaction is rejected.

A simple example of this is a \i{pay-to-pubkey} script, where the
redeemer consists of a signature for the current transaction produced
using a private key belonging to the owner of the output.  The
validator script (provided by the owner of the output) would check the
signature using a known public key: if the public key corresponds to
the private key then validation succeeds, otherwise it fails.  Thus
the output can only be spent by the owner of the relevant private key

See \cref{note:scripts} for more information about validators in
the EUTXO setting.

\note{Inputs and outputs.}
\label{note:inputs-and-outputs}
A transaction has a \textsf{Set} of inputs but a \textsf{List} of outputs.
This is for two reasons:
\begin{itemize}
  \item We need a way to uniquely identify a transaction output, so
  that it can be referred to by a transaction input that spends it. The pair of
  a transaction id and an output index is sufficient for this, but other schemes
  are conceivable.
  \item Equality of transaction outputs is defined structurally. But that means
    that if we had two outputs paying $X$ to address $A$, then they would be
    equal and therefore if we kept them in a \s{Set} one would be lost.
\end{itemize}

\noindent An alternative design would be to include a unique nonce in transaction outputs
(effectively: their index in the list), and then we could use this to identify
them (and distinguish them from each other), and so we could keep them in a \s{Set} instead.

\note{The datum.}
\label{note:datum}
The introduction of the datum
increases the expressivity of the model considerably. For example,
one can use a datum to propagate state between
transactions, and this can be used to give a contract the structure
of a finite state machine; the fact that the datum is part
of the output and not the transaction means that the state can
change without the transaction changing, which makes it easier to
have an ``identity'' for an ongoing contract.

\note{Fees and Costs.}
\label{note:fees}
Users may have to pay a fee in order to have a transaction executed.
In a public blockchain an important reason for this is to deter
hostile agents from carrying out denial of service attacks by
submitting transactions which take a long time or use excessive
amounts of memory.  The precise details of fees in Cardano are outwith
the scope of this document, and indeed have not been fully decided at
the time of writing. However, we expect that the fee will include a
component based on the size of the transaction (including its
associated scripts), and also a so-called \textit{gas} charge to cover
execution costs.  We will have a model specifying the costs of
individual operations during script execution; costs will be monitored
dynamically during execution, and if the gas consumed ever exceeds the
amount covered by the fee then the transaction will fail.

\note{Scripts and Hashes.}
\label{note:scripts} The spendability of an output is determined by
its validator, and thus the validator for an output must be
known at the time when the output is created (a completely new validator
may be created, or an existing validator may be re-used).

Conceptually the validator is part of the output, so it may be rather
unexpected that \cref{fig:eutxo-1-types} defines the validator
to be part of an \textit{input}, with the output only containing the
address of the validator.  The rationale for this is that a validator
$V$ for an output $O$ is not required until $O$ is actually spent,
which may be some time after $O$ was created. Recall from
\cref{note:fees} that the cost of executing a transaction depends
on the size of transaction, including the associated scripts.  Thus
the transaction that produces the validator only pays for the size of
a hash (32 bytes) and the transaction that runs it pays for the full
size of the script.

This strategy also helps to reduce on-chain
storage requirements, since validators can be stored off-chain until
needed (and the presence of the hash in the output can be used to
check that the correct validator is in fact being used when validation
occurs), but unspent outputs persist on-chain in the UTXO set until
they are eventually spent.

The same strategy applies to datum objects.

\note{Datum witnesses.}
\label{note:datum-witnesses}
Although a datum is only recorded as a hash in a transaction output,
it is useful to be able to record the full value of the datum on the
transaction that \emph{creates} an output: this allows observers to
determine the full datum without it having to be kept in the UTXO set.

This mechanism is \emph{optional}, since it incurs an increase in transaction
size (and hence cost), and some clients may want to transmit the information
off-chain instead to minimize these costs.

Hence there is a $\datumWits$ field on transactions, which \emph{may}
contain mappings from the $\DataHash$es used in the transaction to
their \Data{} values. This information is also present in \ctx{}.

\note{Datum objects in \ctx{}.}
\label{note:datum-objects-in-ptx}
In \cref{fig:ptx-1-types,fig:ptx-2-types} the
\textsf{OutputInfo} does not include the datum attached to the output.
These may be found in $\datumWits$.

Having access to the value of the datum allows a validator to inspect
an outgoing datum, for example to confirm that its contents are
correct in some sense. This can be useful when a datum is used to
propagate information about the state of a contract to later
transactions.  See~\cite{Plutus-book} for examples of this.
\todokwxm{More specific reference?}



\note{Determinism of the validation process.}
\label{note:validation-determinism} The \ctx{} type is the only
information about the ``outside world'' available to a validator
at the time of validation.  Allowing the validator access to
this information gives the EUTXO models a considerable amount of
power, as can be seen from the example contracts
in~\cite{Plutus-book}.  However, it is important not to make too much
information available to the validator.  The choice of the \ctx{} type
above means that the information available to the validator is
essentially independent of the state of the blockchain, and in
particular, it is independent of time (note that the check that the
current slot number is within a transaction's validity range takes
place \textit{before} validation is initiated, and the slot number is
not passed to the validator (although the validity range is)).  This
implies that validation is \textit{determinisitic} and validators can
be run off-chain in order to determine their execution cost before
on-chain validation actually occurs.  This helps users to calculate
transaction fees in advance and avoid the possibility of their
transactions failing due to an insufficient fee having been paid (and
also avoids overpayment due to overestimating the fees).

\todokwxm{This may be a little optimistic.  For example, in the
  crowdfunding contract we don't know in advance how many
  contributions will be made, or whether a campaign will succeed or
  fail.  Thus we won't know how much the final transaction will cost
  until just before it happens.}

\note{Monetary policies for custom currencies.}
\label{note:monetary-policies}
The new \textbf{Forging} rule in
\cref{fig:eutxo-2-validity} enables custom currencies to
implement their own monetary policies: for example, one might wish to
place some limit on the amount of a currency that can be forged, or
restrict the creation of the currency to owners of particular public
keys.

The idea is that a custom currency has a monetary policy which is
defined by some script $H$, and the address $h = \scriptAddr(H)$ is used as the
identifier of the currency.

Whenever a new quantity of the currency is forged,
\cref{rule:custom-forge,rule:all-inputs-validate-2,rule:validator-scripts-hash-2}
imply that $H$ must be executed; $H$ is provided with the \forge{}
field of the transaction via the \ctx{} object, and so it knows how
much of the currency is to be forged and can respond appropriately.

The advantage of this scheme is that custom currencies can be handled
entirely within the smart contract system, without the need to
introduce any extra blockchain infrastructure such as a central
registry of custom currencies.

In practice some refinement of this scheme will be required in order
to (a) allow re-use of a monetary policy for different currencies, and
(b) prevent unauthorised forging of a currency. To deal with (a) we
can make the validator script unique by including a nonce. This still
doesn't prevent unauthorised people from using the script $H$ to
produce currency, but this can be prevented by, for instance,
embedding a reference to an unspent output in the script and
requiring that the currency can only be forged if the referenced
output is spent at the same time, so it can only be forged once.

\smallskip
\todokwxm{Is this exactly what we want?  I think that gives you a
  single opportunity to forge the currency, and then you can't make
  any more. I suppose that you could restrict the ability to forge to
  a particular individual by requiring them to provide something
  signed by their private key when they want to create new money.
  Also, is this a case where an output of value zero would be useful?}

\smallskip
\todokwxm{The use of the term ``forging'' is a bit confusing here,
  since it also means ``counterfeiting''.}

% \todojm{I think there are two different concerns:
%  (1) Using the same monetary policy multiple times;
%   (2) Preventing unauthorised forging of a currency.

% The "referencing an unspent output" trick accomplishes
%   both but is mainly aimed at (2). You could also achieve (1) by
%   embedding any kind of random data in the validator script, like a
%   nonce.
% }


\note{Implications of the EUTXO-2 model.}
\label{note:eutxo-2-implications}
The EUTXO-2 model and the techniques described in
\cref{note:monetary-policies} allow us to implement fungible
(normal) and non-fungible token currencies, as well as ``mixed
states'':
\begin{itemize}
\item Standard (fungible) currencies are implemented by issuing
  currencies with a single \token{}.
\item Non-fungible token currencies are implemented by only ever
  issuing single quantities of many unique \token{}s.
\item Note that there is nothing in this model which enforces
  uniqueness: having multiples of a single \token{} merely means that
  those can be used fungibly. If a currency wants to make sure it only
  issues unique tokens it must track this itself.  These ``mixed'' token
  currencies can have many \token{}s, but these can have more than unit
  quantities in circulation.  These can be useful to model distinct
  categories of thing where there are fungible quantities within
  those, for example share classes.
\end{itemize}

\note{Performance issues for EUTXO-2.}
\label{note:eutxo-2-performance}
The EUTXO-2 model will lose some efficiency in comparison to the EUTXO-1
model, simply because the data structures are more complicated.  This
would even apply to transactions which only involve the native
currency (if there is one), since it would be necessary to check whether the \qtymap{}
contains anything that needs to be processed.  If this is a concern
then one could implement a model with two types of transaction,
essentially just the disjoint union of the EUTXO-1 and EUTXO-2
transaction types. A simple case distinction at the start of a
transaction could then select either a fast native-currency-only
computation or a slower multicurrency computation.  This would be
harder to maintain though.

\smallskip  Another optimisation would be possible if one wished to
implement custom currencies but not NFTs: since in this case every
currency would only have a single token, the tokens could be omitted
and the \qtymap{} replaced with a map from currency ids to quantities.

\smallskip A more significant cost may be that we can no longer use
\verb|{-# UNPACK #-}| when our \qty{} type stops being a simple
combination of wrappers and products around primitives, but this is
again an issue with any multi-currency proposal.

\bibliographystyle{plainnat} %% ... or whatever
\bibliography{extended-utxo-specification}


\end{document}
