value update to align with code

shelley-ma/formal-spec/chain.tex

@@ -51,8 +51,18 @@ \section{Blockchain layer}
 \newcommand{\ChainState}{\type{ChainState}}
 \newcommand{\ChainSig}{\type{ChainSig}}
 
+No changes to translate data between old and new types within the ledger or chain
+state are required to transition from the
+Shelley era to the Allegra era. Allegra changes are to the rules for
+validating a new type of script, so we do not give a translation function here.
+Note that while the multi-signature scripts are deprecated in the Allegra era,
+the timelock scripts are intended to be encoding-compatible with the MSig ones.
+That means that
+For this reason,
+
 In Figure~\ref{fig:functions:to-ma}, we give the functions that will be used
-to transition from a Shelley chain state into a chain state that provides multi-asset support.
+to transition from an Allegra chain state into a chain state that provides multi-asset support
+(the Mary era).
 The only part of the state that is affected by the transition is the UTxO. For ease of
 reading, we keep the function $\fun{updateChainStateUTxO}$ abstract, which simply transforms the
 UTxO that is nested deeply inside the chain state with the provided function.
@@ -65,20 +75,20 @@ \section{Blockchain layer}
   \emph{Abstract function}
   %
   \begin{align*}
-      & \fun{updateChainStateUTxO} \in (\ShelleyUTxO \to \UTxO) \to \ShelleyChainState \to \ChainState \\
-      & \text{update the UTxO in a Shelley chain state}
+      & \fun{translateEra} \in (\ShelleyUTxO \to \UTxO) \to \ShelleyChainState \to \ChainState \\
+      & \text{update the UTxO in a chain state}
   \end{align*}
   %
   \emph{Chain state update}
   %
   \begin{align*}
-      & \fun{mkUTxO} ~\in~ \ShelleyUTxO  \to \UTxO  \\
+      & \fun{translateEra} ~\in~ \ShelleyUTxO  \to \UTxO  \\
       & \fun{mkUTxO}~\var{utxo} ~=~ \{~ \var{txin} \mapsto (a,\fun{inject}~c) ~\vert~
       \var{txin} \mapsto \var{(a,c)}\in ~\var{utxo}~\}
       \nextdef
       & \fun{toMA} \in ~ \ShelleyChainState \to \ChainState \\
       & \fun{toMA}~cs = \fun{updateChainStateUTxO}~\fun{mkUTxO}
   \end{align*}
-  \caption{Shelley to Multi-Asset Chain State Transtition}
+  \caption{Allegra to Multi-Asset Chain State Transtition}
   \label{fig:functions:to-ma}
 \end{figure}

shelley-ma/formal-spec/introduction.tex

@@ -1,12 +1,69 @@
 \section{Introduction}
 
-The focus of this document is to give a description of the changes
-required to support multi-assets on the Shelley ledger as described in
-\cite{utxo_ma}. These multi-assets are implemented via token bundles,
-given by a type called $\Value$, which replace the type $\Coin$ of the
-Shelley ledger in many (but not all) cases.
+This document gives a specification of the changes
+required to implement a both an Allegra-era and a Mary-era ledger. These ledgers share
+a specification (and can share an implementation), with the exception of
+a difference in one particular type. We abstract over this type and several
+functions specific to it, which allows us to write a single spec for both versions of the
+ledger, to which we refer as a \emph{ShelleyMA ledger spec}.
 
 All aspects of the ledger not given in this document are as specified
-in the Shelley ledger design and implementation~\cite{shelley_spec},
-but if they depend on something that is changed in this version of the
-ledger they must use the definitions from this document.
+in the Shelley ledger design and implementation~\cite{shelley_spec}.
+Only additions and replacements of definitions of Shelley types, functions, rules, and transitions
+are given here. Replacements are always given the same name as the
+original definition in the Shelley spec, eg. the $\mathsf{UTXO}$ rule in the
+Shelley spec is replaced with the $\mathsf{UTXO}$ rule given here.
+
+\subsection{ShelleyMA, Allegra and Mary Eras}
+
+The additional functionality that is introduced in the Allegra and Mary eras
+is as follows :
+
+\begin{itemize}
+  \item \emph{Allegra} : Timelock scripts replace multi-signature scripts as the native
+  ledger-iterpreted script type. This type of script, in addition to the
+  clauses of the m-of-n multi-signature language, has constructors that
+  allow users to constrain the upper and lower slots of the validity of a
+  clause of the script. For example, one may specify that up to a given slot $s$,
+  either key $k$ or $k'$ can sign the transaction for the script to be valid,
+  whereas from $s$ onwards, only $k$'s signature can make the script valid.
+
+  \item \emph{Mary} : Multi-asset support is added to the Allegra ledger, ie.
+  to the Shelley ledger with timelock scripts. This includes changes to
+  ledger accounting to accommodate multiple types of tokens, as well as
+  support for minting and burning of user-defined tokens. This approach
+  taken here was described initially in \cite{utxo_ma}.
+\end{itemize}
+
+Adding both timelock script and multi-asset support is done in a single specification
+of the ShelleyMA ledger, as the transition rules are exactly the same for both
+Mary and Allegra. The difference between the two is that all accounting is
+done in terms of lovelace, ie. $\Coin$, in the Allegra era, whereas the Mary era
+replaces the $\Coin$ type with a type the terms of which are bundles of arbitrary assets
+(user-defined ones, as well as lovelace), which we call $\Value$.
+
+In this specification, we represent all the places where the $\Coin$ type is used in Allegra,
+and the $\Value$ type in Mary, as $\ValClass$. This is not itself a type, but an
+abstraction representing any type that has certain functions defined on its terms,
+such as addition of two terms,
+a size function, etc. (see Section \ref{sec:value} for details). We say that we
+\emph{instantiate} $\ValClass$ with a specific type (eg. $\Coin$) when we interpretet all
+uses of $\ValClass$ in the spec as replaced by the chosen type, and all the functions
+on abstract terms of $\ValClass$ as the versions specific to the type. For example,
+when we instantiate $\ValClass$ with $\Coin$, we specify that
+addition of two terms is the usual addition of two $\Coin$ terms, and use
+the $\Coin$ addition anywhere $\ValClass$ terms are added in the spec.
+
+Introducing the $\ValClass$ abstraction (including the required
+functions)
+\begin{itemize}
+  \item makes this document is a specification for Allegra when $\ValClass$
+  is instantiated to $\Coin$, and therefore transitions rules invoke the $\Coin$-specific functions
+  defining which is required for instantiating $\ValClass$, and
+  \item makes it a specification for Mary when $\ValClass$
+  is instantiated to $\Value$, together with the $\Value$-specific functions required by $\ValClass$.
+\end{itemize}
+
+Note that this spec is for two distinct eras, but we give only one translations, which is
+from Shelley to Mary, see Section \ref{sec:chain}. This is because no changes to
+chain or ledger types are required for Allegra.

shelley-ma/formal-spec/properties.tex

@@ -7,13 +7,13 @@ \section{Properties}
 The properties of this section are modifications and additions to the properties of the Shelley ledger. See \cite{shelley_spec} for definitions used here. We need to amend the definition of $\Val$ to the following:
 
 \begin{equation*}
-    \Val(x \in \Value) = x
+    \Val(x \in \ValClass) = x
 \end{equation*}
 \begin{equation*}
     \Val(x \in \Coin) = \fun{inject}~x
 \end{equation*}
 \begin{equation*}
-    \Val((\wcard\mapsto (y \in \Value))^{*}) = \sum y
+    \Val((\wcard\mapsto (y \in \ValClass))^{*}) = \sum y
 \end{equation*}
 
 \begin{lemma}
@@ -32,7 +32,7 @@ \section{Properties}
   The proof is identical to the corresponding one in the previous
   specification, except that unfolding $\fun{consumed}$ gives an
   additional $\fun{mint}~{txb}$ term and all $\Coin$ quantities have
-  to be converted to $\Value$.
+  to be converted to terms of type $\ValClass$.
 \end{proof}
 
 We also need to track the sum of the $\fun{mint}$ fields of all
@@ -85,4 +85,4 @@ \section{Properties}
   $\fun{coin}(\fun{mint}~tx) = 0$ for all transactions included
   in $b$. This implies $\fun{coin}(\fun{mint}(b)) = 0$, so the
   claim follows by Lemma~\ref{thm:chain-pres-of-value}.
-\end{proof}
+\end{proof}

shelley-ma/formal-spec/shelley-ma.tex

@@ -102,6 +102,7 @@
 \newcommand{\seedOp}{\star}
 \newcommand{\Ppm}{\type{Ppm}}
 \newcommand{\Value}{\type{Value}}
+\newcommand{\ValClass}{\mathcal{Val}}
 \newcommand{\ProtVer}{\ensuremath{\type{ProtVer}}}
 \newcommand{\Language}{\type{Language}}
 \newcommand{\ApName}{\ensuremath{\type{ApName}}}

shelley-ma/formal-spec/transactions.tex

@@ -13,7 +13,7 @@
   %
   \begin{equation*}
     \begin{array}{r@{~\in~}l@{\qquad=\qquad}lr}
-      \var{txout} & \TxOut & \Addr \times \hldiff{\Value} \\
+      \var{txout} & \TxOut & \Addr \times \hldiff{\ValClass} \\
 %      & \text{tx outputs}
       \var{s} & \Script & \hldiff{\ScriptNI \uniondistinct \Timelock}
 %      & \text{scripts}
@@ -29,7 +29,7 @@
       & \powerset{\TxIn} & \fun{txinputs}& \text{inputs}\\
       &\times ~(\Ix \mapsto \TxOut) & \fun{txouts}& \text{outputs}\\
       & \times~ \seqof{\DCert} & \fun{txcerts}& \text{certificates}\\
-       & \times ~\hldiff{\Value}  & \hldiff{\fun{mint}} &\text{value minted}\\
+       & \times ~\hldiff{\ValClass}  & \hldiff{\fun{mint}} &\text{value minted}\\
        & \times ~\Coin & \fun{txfee} &\text{non-script fee}\\
        & \times ~\hldiff{\Slot^? \times \Slot^?} & \hldiff{\fun{txvldt}} & \text{validity interval}\\
        & \times~ \Wdrl  & \fun{txwdrls} &\text{reward withdrawals}\\
@@ -58,7 +58,7 @@
   \emph{Accessor Functions}
   \begin{equation*}
     \begin{array}{r@{~\in~}lr}
-      \fun{getValue} & \TxOut \to \Value & \text{output value} \\
+      \fun{getValue} & \TxOut \to \ValClass & \text{output value} \\
       \fun{getAddr} & \TxOut \to \Addr & \text{output address}
     \end{array}
   \end{equation*}
@@ -69,17 +69,24 @@
 \section{Transactions}
 \label{sec:transactions}
 
-This section describes the changes that are necessary to the
-transaction structure to support native multi-asset (MA) functionality in
-Cardano.
+This section describes the changes that are made to the
+transaction structure to support both timelock script and native multi-asset (MA)
+functionality in the Cardano ledger.
 
 \subsection*{New Output Type}
 
-A key change needed to introduce MA functionality is changing the type of
+A key change needed to introduce MA functionality in the Mary era is changing the type of
 the transaction and UTxO outputs to contain multi-asset values to accommodate
 transacting with these types of assets natively, using the same ledger accounting
-infrastructure as is used for Ada. That is,
-$\TxOut$ now contains a $\Value$ rather than a $\Coin$.
+scheme as is used for Ada. We set up the infrastructure for this
+change in transition system update common to both Allegra and Mary, ie. ShelleyMA. That is,
+$\TxOut$ now contains a term that is a member of the $\ValClass$ type (which
+could be a $\Coin$, $\Value$, or another type, see Section \ref{sec:coin-ma}),
+rather than only $\Coin$.
+
+In the Allegra era, $\ValClass$ is instantiated with $\Coin$, so there is no
+multi-asset support in the UTxO or the transactions. In the Mary era, it
+is changed to $\Value$ in order to add multi-asset support.
 
 \subsection*{New Script Type}
 
@@ -102,9 +109,9 @@ \subsection*{New Script Type}
 
 \subsection*{The Mint Field}
 
-The body of a transaction with multi-asset support contains one additional
+The body of a transaction in the ShelleyMA era contains one additional
 field, the $\fun{mint}$ field.
-The $\fun{mint}$ field is a term of type $\Value$, which contains
+The $\fun{mint}$ field is a term of type $\ValClass$, which contains
 tokens the transaction is putting into or taking out of
 circulation. Here, by "circulation", we mean specifically "the UTxO on the
 ledger". Since the administrative fields cannot contain tokens other than Ada,
@@ -115,19 +122,56 @@ \subsection*{The Mint Field}
 fields $\fun{mint}$ field, and taking tokens out of circulation can be done
 with negative quantities.
 
-A transaction cannot simply mint arbitrary tokens. Restrictions on
-Multi-Asset tokens are imposed, for each asset with ID $\var{pid}$, by a script
-with the hash $\var{pid}$. Whether a given transaction adheres to the restrictions
-prescribed by its script is verified as part of the processing of the transaction.
+A transaction cannot simply mint arbitrary tokens. In the Mary era, restrictions on
+multi-asset tokens are imposed, for each asset with ID $\var{pid}$, by a script
+with the hash $\var{pid}$. Whether a minting transaction adheres to the restrictions
+prescribed by preimage script is verified as part of the processing of the transaction.
 The minting mechanism is detailed in Section~\ref{sec:utxo}.
 
+Note that the $\fun{mint}$ field exists in both Allegra and Mary eras,
+but can only be used in the Mary era, when multi-assets are introduced.
+In Figure \ref{fig:minted} we give two versions of a function $\fun{minted}$,
+which is used to inspect the $\fun{mint}$ field and return the set of hashes
+of scripts that must be run to validate the minting of the tokens therein :
+
+\begin{itemize}
+  \item For the Allegra version of the function, which operates on $\Coin$ as the
+  type with which $\ValClass$ is instantiated, no scripts need to be run
+  to validate minting, since no minting of Ada is ever allowed.
+
+  \item For the Mary version, the set of $\fun{PolicyID}$s of the
+  assets in the $\Value$ term of the $\fun{mint}$ field is returned.
+\end{itemize}
+
+\begin{figure*}[t!]
+  \emph{ShelleyMA Abstract $\fun{minted}$ Field Type}
+  %
+  \begin{align*}
+    \fun{minted}~\in& \TxBody~\to~\powerset{ScriptHash}
+  \end{align*}
+  %
+  \emph{Allegra Instance}
+  %
+  \begin{align*}
+    \fun{minted}~\wcard~=& \emptyset
+  \end{align*}
+  %
+  \emph{Mary Instance}
+  %
+  \begin{align*}
+    \fun{minted}~\var{txb}~=& \supp~(\fun{mint}~{txb})
+  \end{align*}
+  \caption{$\fun{minted}$ Field in ShelleyMA, Allegra, and Mary}
+  \label{fig:minted}
+\end{figure*}
+
 \subsection*{Transaction Body}
 
 The following changes were made to $\TxBody$:
 
 \begin{itemize}
   \item a change in the type of $\TxOut$ --- instead of
-$\Coin$, the transaction outputs now have type $\Value$.
+$\Coin$, the transaction outputs now have type $\ValClass$.
   \item the addition of the $\fun{mint}$ field to the transaction body
   \item the time-to-live slot number (which had the accessor $\fun{txttl}$),
   has been replaced with a validity interval with accessor $\fun{txvldt}$,

shelley-ma/formal-spec/utxo.tex

@@ -30,18 +30,18 @@ \subsection*{UTxO Helper Functions}
     & \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} \in \UTxO \to \hldiff{\ValClass} \\
     & \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} \\
+    & \fun{consumed} \in \PParams \to \UTxO \to \TxBody \to \hldiff{\ValClass} \\
     & \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} \in \PParams \to \StakePools \to \TxBody \to \hldiff{\ValClass} \\
     & \fun{produced}~\var{pp}~\var{stpools}~\var{txb} = \\
     &~~\ubalance{(\fun{outs}~{txb})} \\
     &~~+ \hldiff{\fun{inject}}(\txfee{txb} + \totalDeposits{pp}{stpools}{(\txcerts{txb})})
@@ -73,7 +73,7 @@ \subsection*{UTxO Helper Functions}
   \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 Shelley
-    counterparts, with the following changes: 1) They return elements of $\Value$, which
+    counterparts, with the following changes: 1) They return terms of $\ValClass$, 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.
@@ -121,19 +121,21 @@ \subsection*{The UTXO Transition Rule}
   \item In the preservation of value calculation (which looks the same as in
   Shelley), the value in the $\fun{mint}$ field is taken into account.
 
-  \item The transaction is not minting any Ada.
+  \item The transaction is not minting any Ada. This condition, in the Allegra
+  era, ensures that no assets can ever be minted (since Ada is the only existing
+  asset).
 
-  \item The $\Value$ in each output is constrained from below by a
-    $\Value$ that contains some amount of ada and no other tokens.
-    The amount of ada that is contained in the constraint $\Value$ (and
-    hence the $\Value$ in the output itself must contain at least as much) depends on the
+  \item The $\ValClass$ term in each output is constrained from below by a
+    $\ValClass$ term that contains some amount of ada and no other tokens.
+    The amount of ada that is contained in the constraint $\ValClass$ term (and
+    hence the $\ValClass$ term in the output itself must contain at least as much) depends on the
     size of the output. To get the minimum ada amount, the size of the output is multiplied by
     the function $\var{adaPerUTxOWord}$ 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}$
+    \item The serialized size of the $\ValClass$ term 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.
@@ -142,7 +144,7 @@ \subsection*{The UTXO Transition Rule}
 
 Note that updating the $\UTxO$ with the inputs and the outputs of the transaction
 looks the same as in the Shelley rule. There is a type-level difference however, as
-the outputs of a transaction contain a $\Value$ term, rather than
+the outputs of a transaction contain a $\ValClass$ term, rather than
 $\Coin$.
 
 
@@ -236,7 +238,7 @@ \subsection*{Witnessing}
     \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})} \\
+      \cup & ~~\hldiff{\fun{minted}~\var{txb}} \\
     & \where \\
     & ~~~~~~~ \var{txb}~=~\txbody{tx}
   \end{align*}
@@ -246,7 +248,10 @@ \subsection*{Witnessing}
 
 Figure~\ref{fig:functions-witnesses} contains the changed definition
 of the function $\fun{scriptsNeeded}$, which also collects the scripts
-necessary for minting.
+necessary for minting. See Section \ref{sec:transactions} for the definitions of
+$\fun{minted}$, which are specific to the exact type used to instantiate
+$\ValClass$. Recall that in Allegra, no assets can ever be minted, so there are no scripts to run that
+validate minting.
 
-The witnessing rule UTXOW only needs a minor change for verifying the meta data hash,
+The witnessing rule UTXOW only needs a minor change for verifying the metadata hash,
 which is replacing the condition $\var{md} = \Nothing$ with $\var{md} = (\emptyset, \Nothing)$.