scripts-multicurrency.tex

\documentclass[11pt,a4paper]{article}
\usepackage[margin=2.5cm]{geometry}
\usepackage{microtype}
\usepackage{mathpazo} % nice fonts
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{latexsym}
\usepackage{mathtools}
\usepackage{stmaryrd}
\usepackage{extarrows}
\usepackage{slashed}
\usepackage[colon]{natbib}
\usepackage[colorinlistoftodos,prependcaption,textsize=tiny]{todonotes}
\usepackage[unicode=true,pdftex,pdfa]{hyperref}
\usepackage[capitalise,noabbrev,nameinlink]{cleveref}
\hypersetup{
  pdftitle={A Formal Specification of a UTxO Ledger with Scripts and Multi-Currency},
  breaklinks=true,
  colorlinks=false,
  linkcolor={blue},
  citecolor={blue},
  urlcolor={blue},
  linkbordercolor={white},
  citebordercolor={white},
  urlbordercolor={white}
}
\usepackage{float}
\floatstyle{boxed}
\restylefloat{figure}

%%
%% Package `semantic` can be used for writing inference rules.
%%
\usepackage{semantic}
%% Setup for the semantic package
\setpremisesspace{20pt}

\DeclareMathOperator{\dom}{dom}
\DeclareMathOperator{\range}{range}

%%
%% TODO: we should package this
%%
\newcommand{\powerset}[1]{\mathbb{P}~#1}
\newcommand{\restrictdom}{\lhd}
\newcommand{\subtractdom}{\mathbin{\slashed{\restrictdom}}}
\newcommand{\restrictrange}{\rhd}
\newcommand{\union}{\cup}
\newcommand{\unionoverride}{\mathbin{\underrightarrow\cup}}
\newcommand{\uniondistinct}{\uplus}
\newcommand{\var}[1]{\mathit{#1}}
\newcommand{\fun}[1]{\mathsf{#1}}
\newcommand{\type}[1]{\mathsf{#1}}
\newcommand{\signed}[2]{\llbracket #1 \rrbracket_{#2}}
\newcommand{\size}[1]{\left| #1 \right|}
\newcommand{\trans}[2]{\xlongrightarrow[\textsc{#1}]{#2}}
\newcommand{\seqof}[1]{#1^{*}}
\newcommand{\nextdef}{\\[1em]}

%%
%% Types
%%
\newcommand{\Bool}{\type{Bool}}
\newcommand{\Slot}{\type{Slot}}
\newcommand{\Script}{\type{Script}}
\newcommand{\TxId}{\type{TxId}}
\newcommand{\Ix}{\type{Ix}}
\newcommand{\Addr}{\type{Addr}}
\newcommand{\Currency}{\type{Currency}}
\newcommand{\Quantity}{\type{Quantity}}
\newcommand{\Value}{\type{Value}}
\newcommand{\TxIn}{\type{TxIn}}
\newcommand{\OutRef}{\type{OutRef}}
\newcommand{\TxOut}{\type{TxOut}}
\newcommand{\UTxO}{\type{UTxO}}
\newcommand{\Create}{\type{Create}}
\newcommand{\Forge}{\type{Forge}}
\newcommand{\TxBody}{\type{TxBody}}
\newcommand{\Tx}{\type{Tx}}

%%
% Scripts
%%
\newcommand{\ScriptEval}[1]{[\![ #1 ]\!]}

%%
%% Functions
%%
\newcommand{\scriptValidate}[3]{\fun{scriptValidate} ~ \var{#1} ~ \var{#2} ~ \var{#3}}
\newcommand{\txid}[1]{\fun{txid}\ \var{#1}}
\newcommand{\inputAddr}[1]{\fun{inputAddr}\ \var{#1}}
\newcommand{\txins}[1]{\fun{txins}\ \var{#1}}
\newcommand{\txouts}[1]{\fun{txouts}\ \var{#1}}
\newcommand{\hash}[1]{\fun{hash}\ \var{#1}}
\newcommand{\forged}[1]{\fun{forged}\ \var{#1}}
\newcommand{\forgeReedemers}[1]{\fun{forgeReedemers}\ \var{#1}}
\newcommand{\fee}[1]{\fun{fee}\ \var{#1}}
\newcommand{\created}[1]{\fun{created}\ \var{#1}}
\newcommand{\outRefs}[1]{\fun{outRefs}\ \var{#1}}

\begin{document}

\title{A Formal Specification of a \\
       UTxO Ledger with Scripts and Multi-Currency}

\author{}

%\date{}

\maketitle

\begin{abstract}
This documents specifies the rules for a multi-currency UTxO ledger with scripts,
as described in \cite{multi_currency} and \cite{utxo_scripts}.
\end{abstract}

\tableofcontents
\listoffigures

\section{Introduction}

A model of a UTxO ledger utilizing an abstract authorization mechanism is
described in \cite{utxo_scripts}.  The authorization mechanism involves a
scripting language, which we leave unspecified and refer to as $\Script$.
This model is an extension of the model described in \cite{chimeric},
which includes account based transactions in addition to UTxO transactions.
We do not include account transactions in this specification.

The model described in \cite{utxo_scripts} was further generalized in
\cite{multi_currency} to support using multiple currencies on the same ledger.

In what follows, we describe the multi-currency UTxO ledger model using
mostly set theory, we state validation rules that determine whether a transaction
is valid for a given ledger state and finally we define the state transformation
that a valid transaction has on the state.

\section{Scripts}

We use an abstract scripting language $\Script$ to generalize authorization
mechanisms such as pay-to-pubkey-hash.
In pay-to-pubkey-hash, an address is the hash of a public key.
UTxO held by that address are authorized by providing the public key
and a digital signature.
Similarly, in the generalized script model, an address
is the hash of a verification script and the redeemer script
plays the role of the digital signature.
UTxO held by script addresses are authorized by providing both the validator
and redeemer script.  Analogously to checking a digital signature,
the authorization succeeds if the redeemer scripts provides evidence to
that causes the validator script to return true.
This is made precise in \cref{fig:scripts}.

\todo[inline]{These scripts probably also need to take some of the data
from the validating transaction}

\begin{figure}
\emph{Scripts}
%
\begin{equation*}
\begin{array}{r@{~\in~}l@{~,~}r@{~:~}l}
  \var{validator}
& \Script
& \ScriptEval{validator}
& \type{LedgerState} \mapsto \type{R} \mapsto \Bool
\\
  \var{redeemer}
& \Script
& \ScriptEval{redeemer}
& \type{LedgerState} \mapsto \type{R}
\end{array}
\end{equation*}
~ ~ ~ \text{where $\ScriptEval{script}$ is the pure function denoted
by $script\in\Script$,}

~ ~ ~ \text{and $\type{R}$ is an arbitrary type, but must be the
same for each validator/redeemer pair.}
\\
\\
\emph{Script Operations}
\begin{align*}
& \fun{scriptValidate} \in
  \type{LedgerState} \mapsto \Script \mapsto \Script \mapsto \Bool \\
& \scriptValidate{st}{validator}{redeemer} =
\ScriptEval{validator} ~ state \left(\ScriptEval{redeemer} state\right)
\end{align*}

\caption{Scripts}
\label{fig:scripts}
\end{figure}
\section{Multi-Currency}

Multi-currency is explained in detail in \cite{multi_currency}, but here we give some
brief details. The main idea is to replace the currency quantity type with a (finite)
mapping from currency names to quantity. The understanding is that currencies not in
a given mapping are assumed to have value 0 (the additive identity). Previous operations
on the quantity type, such as addition and less-than, are now performed coordinate-wise
on the new type. We write $\vec{0}$ for the empty map/value.

\section{Basic Types and Operations}

The basic types and operations for this specification are given
in \cref{fig:basic_definitions}.  Transaction inputs are references to
previous unspent outputs, together with the scripts needed to authorize it.
Outputs are the pair of an address (the hash of a validator script) and a
multi-currency value. A transaction is a collection of inputs and outputs,
together with other data for creating new currencies, minting currency,
and paying fees. Currency is authorized to be minted using the same
mechanism of validator and redeemer scripts.
Other needed operations on transactions and UTxO are given in
\cref{fig:auxiliary_ops}.

\begin{figure}

\emph{Primitive types}
%
\begin{equation*}
\begin{array}{r@{~\in~}lr}
  \var{txid}
& \TxId
& \text{transaction id}
\\
  ix
& \Ix
& \text{index}
\\
  \var{addr}
& Addr
& \text{address}
\\
  curr
& \Currency
& \text{currency identifier}
\\
  qty
& \Quantity
& \text{currency quantity}
\end{array}
\end{equation*}

%
\emph{Derived types}
%
\begin{equation*}
\begin{array}{r@{~=~}lc@{}r@{~\in~}l}
  \Value
& \Currency \mapsto \Quantity
&
& (\var{curr}, \var{qty})
& \Value
\\
  \TxIn
& \TxId \times \Ix \times \Script \times \Script
&
& (\var{txid}, \var{ix}, \var{validator}, \var{redeemer})
& \TxIn
\\
  \OutRef
& \TxId \times \Ix
&
& (\var{txid}, \var{ix})
& \OutRef
\\
  \TxOut
& \Addr \times \Value
&
& (\var{addr}, v)
& \TxOut
\\
  \UTxO
& \OutRef \mapsto \TxOut
&
& \var{outRef} \mapsto \var{txout} \in \var{utxo}
& \UTxO
\\
  \Create
& \type{Optional} (\Currency \times \Script)
&
& (\var{currency}, \var{validator})
& \Create
\\
  \Forge
& \Value \times (\Currency \mapsto \Script)
&
& (\var{value}, \var{curr} \mapsto \var{redeemer})
& \Forge
\\
  \TxBody
& \powerset{\TxIn} \times (\Ix \mapsto \TxOut)
&
& (\var{txins}, \var{txouts})
& \TxBody
\\
  \Tx
& \TxBody \times \Forge \times \Value \times \Create
&
& (\var{txbody}, \var{forge}, \var{fee}, \var{create})
& \Tx
\end{array}
\end{equation*}
%
\emph{Functions}
%
\begin{equation*}
\begin{array}{lr}
  \fun{txid} \in \Tx \to \TxId
& \text{compute transaction id}
\\
  \fun{hash} \in \Script \to \Addr
& \text{compute script address}
\end{array}
\end{equation*}

\caption{Basic Definitions}
\label{fig:basic_definitions}
\end{figure}


\begin{figure}
\begin{align*}
& \fun{txins} \in \Tx \to \powerset{\TxIn}
& \text{transaction inputs} \\
& \fun{txins} ~ ((\var{txins}, \_), \_, \_, \_) = \var{txins}
\\[1em]
& \fun{txouts} \in \Tx \to \UTxO
& \text{transaction outputs as UTxO} \\
& \fun{txouts} ~ \var{tx} =
  \left\{ (\fun{txid} ~ \var{tx}, \var{ix}) \mapsto \var{txout} ~
  \middle| \begin{array}{l@{~}c@{~}l}
             ((\_, \var{txouts}),\_, \_, \_) & = & \var{tx} \\
             \var{ix} \mapsto \var{txout} & \in & \var{txouts}
           \end{array}
  \right\}
\\[1em]
& \fun{outRefs} \in \Tx \to \powerset({\TxId \times \Ix})
& \text{Output References} \\
& \fun{outRefs} ~ ((\var{txins}, \_), \_, \_, \_)
= \left\{ (id, ix) \middle| (id, ix, \_, \_) \in txins\right\}
\\[1em]
& \fun{balance} \in \UTxO \to \Value
& \text{UTxO balance} \\
& \fun{balance} ~ utxo = \sum_{(\_ ~ \mapsto (\_, v)) \in \var{utxo}} v
\\[1em]
& \fun{created} \in \Tx \to \Create
& \text{created currency} \\
& \fun{created} ~ (\_, \_, \_, create) = \var{create}
\\[1em]
& \fun{forged} \in \Tx \to \Value
& \text{the forged multi-currency} \\
& \fun{forged} ~ (\_, (value, \_), \_, \_) = \var{value}
\\[1em]
& \fun{forgeReedemers} \in \Tx \to \Script
& \text{redeemer scripts for forging} \\
& \fun{forgeReedemers} ~ ( \_, (\_, \var{redeemers}), \_, \_) = reedemers
\\[1em]
& \fun{fee} \in \Tx \to \Value
& \text{the fees in a transaction} \\
& \fun{fee} ~ (\_, \_, fee, \_) = \var{fee}
\end{align*}
\caption{Operations on transactions and UTxOs}
\label{fig:auxiliary_ops}
\end{figure}

\section{Validation and Ledger State}

Validation is the determination that a transaction is permitted to be appended
to the ledger and hence manipulate the state of the ledger.
The data in the ledger state is given by \cref{fig:ledger_state}.
Though $\var{totalMinted}$ and $\var{slot}$ do not appear to be used in this specification,
they are important since they are used by the validator scripts.
For example, expirations can be implemented using $\var{slot}$ and a currency's
policy may depend on $\var{totalMinted}$.

The ledger state is defined inductively.
The initial state is defined in \cref{fig:ledger_state}.
\todo{Should we hard code $\mathsf{ADA}$ and the corresponding
monetary policy into the initial ledger state?}
Given a transaction and a ledger state, first we check that
the transaction is valid.
To be valid, it must pass every test given in \cref{fig:validation_rules}.
Note that these rules depend only on the transaction and the ledger state.
If a transaction is valid for a given ledger state, it is then
applied using the state transformation rule given in \cref{fig:state_transition}.
\todo[inline]{There is a subtlety here involving in the order in which these rules are applied.
If the UTxO update rule (\cref{eq:utxo-update}) is applied to a transaction before the
currency creation rule (\cref{eq:create-currency}),
then a currency cannot be both created and forged in the same transaction.}

Note that two rules from \cite{multi_currency} do not appear in \cref{fig:validation_rules},
namely ``creator has enough money" and ``fee is non-negative".
In a model without account transactions, as we have here, we do not need additive
inverses and can assume that all quantities are nonnegative.

\begin{figure}
\emph{Valid-Inputs}
%
\begin{equation*}
\outRefs{tx} \subseteq \dom \var{utxo}
\end{equation*}

\emph{Preservation-of-Value}
%
\begin{equation*}
balance (\txouts tx) + (\fee tx)
  = balance (\outRefs tx \restrictdom utxo) + (\forged tx)
\end{equation*}

\emph{No-Double-Spend}
%
\begin{equation*}
\lvert \txins tx \rvert = \lvert \outRefs tx\rvert
\end{equation*}

\emph{Scripts-Validate}
%
\begin{equation*}
\forall (\_, \_, validator, redeemer)\in(\txins tx),
~ \scriptValidate{state}{validator}{redeemer}
\end{equation*}

\emph{Authorized}
%
\begin{equation*}
\begin{array}{c}
  \forall i\in(\txins tx),\\
    i = (txid, ix, validator, \_)
    \land ((txid, ix) \mapsto (addr, \_)) \in \var{utxo}
    \land \hash validator = addr
\end{array}
\end{equation*}

\emph{Forge-Obeys-Policy}
%
\begin{equation*}
\begin{array}{c}
\forall c\in(\forged tx), \\
\exists policy, (c \mapsto policy) \in \var{currencies} \\
\exists reedemer, (c \mapsto reedemer) \in \forgeReedemers tx \\
\scriptValidate{state}{policy}{redeemer}
\end{array}
\end{equation*}

\emph{Create-Only-New-Currencies}
%
\begin{equation*}
\created tx = (curr, policy), curr \notin \dom currencies
\end{equation*}

\caption{Validation Rules}
\label{fig:validation_rules}
\end{figure}


\begin{figure}

\emph{Ledger State}
%
\begin{equation*}
\begin{array}{r@{~\in~}lr}
utxo & \UTxO & \text{unspent outputs}
\\
currencies & \Currency \mapsto \Script
  & \text{currencies with policies}
\\
totalMinted & \Value & \text{total currency minted}
\\
slot & \Slot & \text{current slot}

\end{array}
\end{equation*}
\emph{Initial Ledger State}
%
\begin{equation*}
\begin{array}{llllll}
utxo = \emptyset
  & currencies = \emptyset
  & totalMinted = \vec{0}
  & slot = 0
\end{array}
\end{equation*}

\caption{Ledger State}
\label{fig:ledger_state}
\end{figure}

\begin{figure}
  \centering
  \begin{equation}\label{eq:utxo-update}
    \inference[update-UTxO]
    {
      \text{Valid-Inputs} & \text{Preservation-of-Value} & \text{No-Double-Spend} \\
      \text{Scripts-Validate} & \text{Authorized} & \text{Forge-Obeys-Policy}
    }
    {
      \begin{array}{rcl}
        \var{utxo} & & (\outRefs tx \subtractdom \var{utxo}) \union \txouts tx \\
        \var{totalMinted} & \trans{}{tx} & \var{totalMinted} + (\forged tx)\\
      \end{array}
    }
  \end{equation}

  \begin{equation}\label{eq:create-currency}
    \inference[create-currency]
    {
      \text{Create-Only-New-Currencies}
    }
    {
      \var{currencies} \trans{}{tx} \var{currencies} \union (\created tx)
    }
  \end{equation}

  \caption{State Transitions}
  \label{fig:state_transition}
\end{figure}

\section{Disabling Multi-Currency}

If we want to disable multi-currency, we can remove the ``Forge Obeys Policy" rule and
add \cref{fig:only_ada_rule}
\begin{figure}
\emph{Only ADA}
%
\begin{equation*}
\created tx = (curr, policy), curr = \mathsf{ADA}
\end{equation*}

\caption{Only ADA Rule}
\label{fig:only_ada_rule}
\end{figure}

\todo[inline]{We need to think carefully about how to handle similar names,
like ``ada", ``Ada" and ``ADA". Allow only uppercase (lowercase)? No unicode?}

\section{Disabling Scripts}

WIP - We should probably make two types of addresses, pay-to-pubkey addresses and script addresses.
The pay-to-pubkey addresses will work similarly to the validation rules defined above, with the
following changes:

"Scripts Validate" becomes a specific validator/redeemer pair, where $\mathsf{validator}$ checks a
digital signature and $\mathsf{redeemer}$ is the constant function returning a signature of the
part of transaction (perhaps $\outRefs tx$?).

``Authorized" is nearly the same, except we hash the stake key instead of the validator script.

``No Double Spend" is no longer needed.

\section{Extended UTxO}

The main documentation is \href{https://github.com/input-output-hk/plutus/blob/master/extended-utxo-spec/extended-utxo-specification.tex}{here}.
We need to add the data script to TxOut:
$$ \TxOut = \Addr \times \Value \times \Script $$
We also need to provide the validator script with more information.  Is the $\TxBody$ enough?
How is this more expressive than what we already have?

\addcontentsline{toc}{section}{References}
\bibliographystyle{plainnat}
\bibliography{references}

\end{document}