Merge pull request #1521 from michaelpj/imp/eutxo-outputs-positivity

EUTXO spec: allow negative values in the representation

extended-utxo-spec/extended-utxo-specification.tex

@@ -133,16 +133,13 @@
 \newcommand{\eutxotx}{\msf{Tx}}
 
 \newcommand{\qty}{\ensuremath{\s{Quantity}}}
-\newcommand{\qtypm}{\ensuremath{\s{Quantity}^{\pm}}}
-\newcommand{\newqtytype}{\ensuremath{\s{Quantity}^{\prime}}}
 \newcommand{\token}{\ensuremath{\s{Token}}}
 \newcommand{\currency}{\ensuremath{\s{CurrencyId}}}
 \newcommand{\nativeCur}{\ensuremath{\mathrm{nativeC}}}
 \newcommand{\nativeTok}{\ensuremath{\mathrm{nativeT}}}
 \newcommand{\injectNative}{\ensuremath{\mathrm{inject}}}
 
-\newcommand{\qtymap}{\ensuremath{\s{QuantityMap}}}
-\newcommand{\qtymappm}{\ensuremath{\s{QuantityMap}^{\pm}}}
+\newcommand{\qtymap}{\ensuremath{\s{Quantities}}}
 
 \newcommand\B{\ensuremath{\mathbb{B}}}
 \newcommand\N{\ensuremath{\mathbb{N}}}
@@ -423,8 +420,7 @@ \subsection{A Formal Description of the EUTXO-1 Model}
   \begin{displaymath}
   \begin{array}{rll}
     \multicolumn{3}{l}{\textsc{Ledger primitives}}\\
-    \qty{} && \mbox{an amount of currency, always non-negative}\\
-    \qtypm && \mbox{a possibly negative amount of currency}\\
+    \qty{} && \mbox{an amount of currency}\\
     \slotnum && \mbox{a slot number}\\
     \Address && \mbox{the address of an object in the blockchain}\\
     \TxId && \mbox{the identifier of a transaction}\\
@@ -466,8 +462,7 @@ \subsubsection{Remarks}
 \begin{ruledfigure}{H}
   \begin{displaymath}
   \begin{array}{rll}
-    \qty{} &=& \N\\
-    \qtypm &=& \Z\\
+    \qty{} &=& \Z\\
     \slotnum &=& \N\\
     \Address &=& \H\\
     \TxId &=& \H\\
@@ -483,11 +478,6 @@ \subsubsection{Remarks}
   \label{fig:eutxo-1-types-cardano}
 \end{ruledfigure}
 
-\paragraph{Quantities. }
-The \qty{} type represents a non-negative quantity of funds.  The \qtypm{} type
-is similar, but negative quantities are allowed.  As with \N{} and \Z{}, we regard
-\qty{} as a subtype of \qtypm{} and convert freely between them.
-
 \paragraph{Inputs and outputs. } Note that a transaction has a
 \textsf{Set} of inputs but a \textsf{List} of outputs. See
 note~\ref{note:inputs-and-outputs} for a discussion of why.
@@ -636,6 +626,13 @@ \subsection{Validity of EUTXO-1 transactions}
 \begin{ruledfigure}{H}
 \begin{enumerate}
 
+\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}
@@ -669,15 +666,15 @@ \subsection{Validity of EUTXO-1 transactions}
   \label{rule:all-inputs-validate}
   \textbf{All inputs validate}
   \begin{displaymath}
-    \textrm{For all } i \in t.\inputs,\enspace \llbracket
+    \textrm{For all } i \in t.\inputs,\ \llbracket
     i.\validator\rrbracket (\getSpent(i, l).\valdata,\, i.\redeemer,\,  \delta(\tau(t,i))) = \true.
   \end{displaymath}
 
 \item
   \label{rule:validator-scripts-hash}
   \textbf{Validator scripts match output addresses}
   \begin{displaymath}
-    \textrm{For all } i \in t.\inputs,\enspace \scriptAddr(i.\validator) = \getSpent(i, l).\addr
+    \textrm{For all } i \in t.\inputs,\ \scriptAddr(i.\validator) = \getSpent(i, l).\addr
   \end{displaymath}
 
 \end{enumerate}
@@ -743,7 +740,7 @@ \subsection{The definition of EUTXO-2}
 The changes to the basic EUTXO-1 types are now quite simple:
 see Figure~\ref{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 \qtymappm{}, to
+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.
@@ -758,7 +755,6 @@ \subsection{The definition of EUTXO-2}
     \\
     \multicolumn{3}{l}{\textsc{Defined types}}\\
     \qtymap   &=& \FinSup{\currency}{\FinSup{\token}{\qty}}\\
-    \qtymappm &=& \FinSup{\currency}{\FinSup{\token}{\qtypm}}\\
     \\
     \s{Output}_2 &=&(\addr: \Address,\\
                  & &\ \val: \qtymap\\
@@ -774,7 +770,7 @@ \subsection{The definition of EUTXO-2}
                & &\ \outputs: \List{\s{Output}_2},\\
                & &\ \i{validityInterval}: \Interval{\extended{\slotnum}},\\
                & &\ \fee: \qty,\\
-               & &\ \forge: \qtymap^{\pm})\\
+               & &\ \forge: \qtymap)\\
     \\
     \s{Ledger}_2 &=&\!\List{\eutxotx_2}\\
     \end{array}
@@ -800,12 +796,9 @@ \subsubsection{Remarks}
   \label{fig:eutxo-2-types-cardano}
 \end{ruledfigure}
 
-\paragraph{Quantity maps. }
+\paragraph{\qtymap{}. }
 The \qtymap{} type represents a collection of funds from a
-number of currencies and their subcurrencies, with all quantities
-being non-negative.  The \qtymappm{} type is similar, but
-negative quantities are allowed.  As with \qty{} and \qtypm{}, we regard
-\qtymap{} as a subtype of \qtymappm{} and convert freely between them.
+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.
@@ -887,6 +880,13 @@ \subsection{Validity of EUTXO-2 transactions}
 \begin{ruledfigure}{H}
 \begin{enumerate}
 
+\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}
@@ -927,15 +927,15 @@ \subsection{Validity of EUTXO-2 transactions}
   \label{rule:all-inputs-validate-2}
   \textbf{All inputs validate}
   \begin{displaymath}
-    \textrm{For all } i \in t.\inputs,\enspace \llbracket
+    \textrm{For all } i \in t.\inputs,\ \llbracket
     i.\validator\rrbracket(\getSpent(i,l).\valdata,\, i.\redeemer,\, \delta_2(\tau_2(t, i))) = \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,\enspace \scriptAddr(i.\validator) = \getSpent(i, l).\addr
+    \textrm{For all } i \in t.\inputs,\ \scriptAddr(i.\validator) = \getSpent(i, l).\addr
   \end{displaymath}
 
 \end{enumerate}
@@ -946,8 +946,8 @@ \subsection{Validity of EUTXO-2 transactions}
 \subsection{Remarks}
 \paragraph{Preservation of value over \qtymap{}s.}
 In rule~\ref{rule:value-is-preserved-2},
-$+$ and $\sum$ operate over \qtymap{}s, which are
-finitely-supported functions (which, with their operations,
+$+$ and $\sum$ operate over \qtymap{}, which is
+a finitely-supported function (which, with their operations,
 are defined in Section~\ref{sec:fsfs}). Preservation of value
 in this model essentially requires that the
 quantities of each of the individual currencies involved in the