IntersectMBO · polinavino · Mar 18, 2021 · Mar 9, 2021
@@ -1,10 +1,8 @@
 \section{Introduction}
 
 \TODO{Please run a spell checker over the final document}
-\TODO{Please fix up all missing references}
-\TODO{Take care to distinguish validation succeeding, and validation returning true.  I think you ALWAYS mean validation is true (a script is valid) NOT validation is successful (it has completed, but may have returned false)}
 
-This document describes the extensions to the multi-asset formal ledger specification~\ref{XX} \TODO{Fix this reference} that are
+This document describes the extensions to the multi-asset formal ledger specification~\cite{shelley_ma_spec} that are
 required for the support of non-native scripts, in particular Plutus Core. This underpins future Plutus development: there should be minimal changes to these ledger rules to support future non-native languages.
 %
 The two major extensions that are described here are:
@@ -17,7 +15,7 @@ \section{Introduction}
   constructs (the ``extended UTxO'' model).
 \end{inparaenum}
 This document defines these extensions as changes to the multi-asset structured transition system,
-using the same notation and conventions that were used for the multi-asset specification~\cite{XX}.\TODO{Add this reference!!}
+using the same notation and conventions that were used for the multi-asset specification~\cite{shelley_ma_spec}.
 As with the multi-asset formal specification, these rules will be implemented in the form of an executable ledger specification that will then be
 integrated with the Cardano node.
 
@@ -31,7 +29,7 @@ \subsection{Non-Native Scripts}
 
 In contrast, \emph{non-native} scripts can perform arbitrary
 (and, in principle, Turing-complete) computations.
-In order to bound execution costs to a pre-determined constant, we use a standard ``fuel'' approach~\cite{XX}.\TODO{And this one, please!}
+In order to bound execution costs to a pre-determined constant, we use a standard ``fuel'' approach.
 We require transactions that use non-native scripts
 to have a budget in terms of a number of abstract $\ExUnits$.
 This budget gives a quantitative bound on resource usage in terms of a number of specific metrics, including memory usage or abstract execution steps.

@@ -2,13 +2,13 @@ \section{Language Versions and Cost Models}
 \label{sec:protocol-parameters}
 
 We require the following types (see Figure~\ref{fig:defs:protocol-parameters})
-in addition to those that are already defined in the Shelley specification~\cite{XX}. \TODO{Add the citation}
+in addition to those that are already defined in the Shelley specification~\cite{shelley_spec}.
 
 \vspace{12pt}
 \begin{tabular}{lp{5in}}
   $\Language$ &
-  This represents the language name/tag (including the
-  version number).
+  This represents the language name/tag, including the
+  version number.
   \\
   $\ExUnits$ &
   A term of this type contains two integer values,
@@ -24,18 +24,10 @@ \section{Language Versions and Cost Models}
   \\
   $\Prices$ &
   A term of this type comprises two integer values that correspond to the components of $\ExUnits$,
-  $\var{pr_{mem}, pr_{steps})}$:
+  $\var{(pr_{mem}, pr_{steps})}$:
   $pr_{mem}$ is the price (in Ada) per unit of memory, and $pr_{steps}$ is the price (in Ada) per
   reduction step. This is used to calculate the Ada cost for a specific script execution.
 \end{tabular}
-\vspace{12pt}
-
-We also need a number of additional protocol parameters and accessor functions: ...\todo{List these.}
-
-\begin{tabular}{||l|l||}
-  \textbf{Item} & \textbf{Use} \\
-  \
-  \end{tabular}
 
 \subsection{Language Versions and Backwards Compatibility Requirements}
 \label{sec:versions}
@@ -47,7 +39,7 @@ \subsection{Language Versions and Backwards Compatibility Requirements}
 It is necessary for the ledger to be capable of executing scripts in languages it ever supported.
 This implies that it is necessary to maintain all forms of ledger
 data that is needed by any past or current language, which constrains future ledger designs.
-Introducing a new language will require a major protocol version update, since the datatypes need to support the new language and the ledger rules must be updated to use the new interpreter.
+Introducing a new language will require a protocol version update, since the datatypes need to support the new language and the ledger rules must be updated to use the new interpreter.
 
 \subsection{Determinism of Script Evaluation}
 \label{sec:determinism}
@@ -60,7 +52,7 @@ \subsection{Determinism of Script Evaluation}
 submission and completion of the script processing.
 %
 In order to achieve this,
-any data that is passed to the interpreter must be determined by the transaction itself.
+any data that is passed to the interpreter must be determined by the transaction body itself.
 The transaction therefore includes a hash of any data that is not determined by the transaction or the UTXO.
 When the transaction is processed, as part of the UTXOW rule, this hash is compared with a hash of the data that is passed to the interpreter. This
 ensures that scripts are only executed if they have been provided with the intended data.
@@ -93,7 +85,7 @@ \subsection{Script Evaluation Cost Model and Prices}
   \emph{Abstract types}
   %
   \begin{equation*}
-    \begin{array}{r@{~\in~}l@{\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad}r}
+    \begin{array}{r@{~\in~}l@{\qquad\qquad\qquad}r}
       \var{cm} & \CostMod & \text{Coefficients for the cost model} \\
       \var{ldv} & \LangDepView & \text{Language-dependent view of the protocol parameters}
     \end{array}
@@ -107,7 +99,7 @@ \subsection{Script Evaluation Cost Model and Prices}
       & \{\Plutus, \dotsb\}
       & \text{Script Language}
       \\
-      \var{pr_{mem}, pr_{steps})}
+      \var{(pr_{mem}, pr_{steps})}
       & \Prices
       & \Coin \times \Coin
       & \text {Coefficients for $\ExUnits$ prices}

@@ -52,6 +52,14 @@ @misc{shelley_spec
   url = {https://github.com/input-output-hk/cardano-ledger-specs/tree/master/shelley/chain-and-ledger/formal-spec/ledger-spec.tex}
 }
 
+@misc{shelley_ma_spec,
+  label = {CdoLedger},
+  author = {{Formal Methods Team, IOHK}},
+  title  = {{A Formal Specification of the Cardano Ledger with a Native Multi-Asset Implementation}},
+  year   = {2019},
+  url = {https://github.com/input-output-hk/cardano-ledger-specs/tree/master/shelley-ma/formal-spec/shelley-ma.tex}
+}
+
 @misc{ouroboros,
     label = {CdoProt},
     author = {Aggelos Kiayias and Alexander Russell and Bernardo David and Roman Oliynykov},

@@ -6,7 +6,7 @@ \section{Transactions}
 the minting of tokens, spending outputs, verifying certificates, and
 verifying withdrawals.
 %
-Figure \ref{fig:defs:utxo-shelley-1} gives the modified transaction types.
+Figure \ref{fig:defs:utxo-shelley-1} gives the modified transaction types and helper functions.
 We make the following changes and additions:
 
 \begin{itemize}
@@ -19,7 +19,7 @@ \section{Transactions}
 
   \item $\Data$ is a type for communicating data to script.  It is kept abstract here.
 
-  \item $\Script$ is a sum type covering all possible scripts, both native and non-native.
+  \item $\Script$ is the type of all scripts, both native and non-native.
 
   \item $\IsValidating$ is a tag that indicates that a transaction
   expects that all its non-native scripts will be validated.
@@ -48,12 +48,20 @@ \section{Transactions}
 
 \end{itemize}
 
+We add the following helper functions:
+
+\begin{itemize}
+  \item $\fun{language}$ selects the language of a non-native script.
+  \item $\fun{hashData}$ hashes a value of type $\Data$.
+  \item $\fun{hashWitnessPPData}$ hashes the protocol parameters and witnesses relevant to script execution.
+\end{itemize}
+
 \begin{figure*}[htb]
   \emph{Abstract types}
   %
   \begin{equation*}
     \begin{array}{r@{~\in~}l@{\quad\quad\quad\quad}r}
-      \var{sdh} &\WitnessPPDataHash & \text{Script data hash}\\
+      \var{wph} &\WitnessPPDataHash & \text{Script data hash}\\
       \var{plc} & \ScriptPlutus & \text{Plutus core scripts} \\
       \var{d} & \Data & \text{Generic script data}
     \end{array}
@@ -99,7 +107,7 @@ \section{Transactions}
     \fun{hashWitnessPPData}&~{pp}~{langs}~{rdmrs}~=~ \\
                           &\begin{cases}
                             \Nothing & rdmrs~=~\emptyset \land langs~=~\emptyset \\
-                            \fun{hash} (rdmrs, \{ \fun{hashLanguagePP}~pp~l \mid l \in langs \}) & \text{otherwise}
+                            \fun{hash} (rdmrs, \{ \fun{getLanguageView}~pp~l \mid l \in langs \}) & \text{otherwise}
                           \end{cases}
     \nextdef
     \fun{getCoin}& \in \TxOut \to \Coin \\
@@ -135,6 +143,7 @@ \section{Transactions}
        & \times ~\Slot^? \times \Slot^? & \fun{txvldt} & \text{Validity interval}\\
        & \times~ \Wdrl  & \fun{txwdrls} &\text{Reward withdrawals}\\
        & \times ~\Update^?  & \fun{txUpdates} & \text{Update proposals}\\
+       & \times ~\hldiff{\powerset{\VKey}} & \hldiff{\fun{extraKeys}} & \text{VKeys passed to scripts}\\
        & \times ~\hldiff{\WitnessPPDataHash^?} & \hldiff{\fun{wppHash}} & \text{Hash of script-related data}\\
        & \times ~\AuxiliaryDataHash^? & \fun{txADhash} & \text{Auxiliary data hash}\\
     \end{array}
@@ -190,16 +199,22 @@ \subsection{Witnessing}
   For details on how a script finds its redeemer, see Section~\ref{sec:scripts-inputs}.
 \end{description}
 
-\subsection{Goguen transactions}
+\subsection{Transactions}
 We have also made the following changes to
 the body of the transaction:
 
 \begin{itemize}
+  \item There is a set of \emph{fee inputs} that is used to cover transaction fees
+    \emph{in case the transaction contains non-native scripts}. In case the same itput is mentioned both as
+    a regular and a fee input, it still counts as being spent just once, so there is no need to prevent this.
+    It is in the transaction creator's best interest to keep the two sets of inputs disjoint, to minimize fees.
+  \item There is a new field called $\fun{extraKeys}$ that is used to specify a set of signers that are passed
+    to scripts, in addition to the ones required by VKey addresses. The keys included also need to sign the transaction.
   \item We include a hash of some script-related data, specifically the redeemers and protocol parameters,
-    with accessor $\fun{sdHash}$.
+    with accessor $\fun{wppHash}$.
 \end{itemize}
 
-A complete Goguen transaction comprises:
+A complete transaction comprises:
 
 \begin{enumerate}
   \item the transaction body,
@@ -235,7 +250,7 @@ \subsection{Additional Role of Signatures on TxBody}
 must sign the transaction body. This means that
 the owners of tokens that are spent by the transaction will have
 signed their selection of the inputs that will be put in the fee pot in case of script validation failure, and
-thus have had the opportunity to check the outcome of those scripts before signing the body.
+thus have had the opportunity to check the outcome of those scripts before signing the transaction body.
 
 \subsection{Fee charges in the event of script validation failure}