Merge pull request #2271 from input-output-hk/polina/collateral

collateral inputs

alonzo/formal-spec/chain.tex

@@ -59,8 +59,8 @@ \subsection{Block Body Transition}
 
 
 Figure~\ref{fig:rules:bbody} includes an additional check that the sum of the
-script fees that are paid by all transactions in a block does not exceed the maximum total fees per
-block (obtained from the protocol parameter).
+execution units of all transactions in a block does not exceed the maximum total units per
+block (specified in a protocol parameter).
 
 \begin{figure}[ht]
   \begin{equation}\label{eq:bbody}
@@ -130,7 +130,8 @@ \subsection{Block Body Transition}
   \emph{Types and Constants}
   %
   \begin{align*}
-      & \NewParams ~=~ (\Language \mapsto \CostMod) \times \Prices \times \ExUnits \times \ExUnits \times \N \times \Coin \\
+      & \NewParams ~=~ (\Language \mapsto \CostMod) \times \Prices \times \ExUnits \times \ExUnits \\
+      & ~~~~~~~~ \times \N \times \Coin \times \N \times \N \\
       & \text{the type of new parameters to add for Goguen}
       \nextdef
       & \var{ivPP} ~\in~ \NewParams \\

alonzo/formal-spec/introduction.tex

@@ -53,24 +53,24 @@ \subsection{Non-Native Scripts}
   contract (eg. their total available funds).
 
   \item The exact total fee a transaction is paying is also specified in the transaction data.
-  For a transaction to be valid, this fee must cover the script-running resource budget at the current price.
+  For a transaction to be valid, this fee must cover the script-running resource budget at the current price,
+  as well as the size-based part of the required fee.
   If the fee is not sufficient to cover the resource budget specified (eg. if the resource price increased),
   the transaction is considered invalid and \emph{will not appear on the ledger (will not be included in a valid block)}.
   No fees will be collected in this case.
   This is in contrast with the gas model, where, if prices go up, a greater fee will be charged - up to
   the maximum available funds, even if they are not sufficient to cover the cost of the execution of the contract.
 
-  \item If a script validates having used less resources than the budget specified by the
-  transaction, the fee for the whole budget is still collected. Unlike the gas model, where
-  the exact fee is not known at the time of transaction submission.
-
-  \item The user specifies the UTxO entries containing funds intended to pay fees.
-  The total amount of funds in entries marked for-fees must cover the specified transaction fee.
-  The UTxO entries may, however, contain more funds than the fee amount. In the case that a script carried by a transaction fails
-  to validate, a larger fee (than the one specified in the transaction) may be collected.
-  The amount of the fee collected is the total funds in all the UTxOs marked for fee payment.
-  This scheme is similar to the upper bound on the transaction fee that is used by the gas model,
-  however, it only applies in the case of script failure in our model.
+  \item The user specifies the UTxO entries containing funds sufficient to cover a percentage
+  (usually $100$ or more) of the total transaction fee.
+  These inputs are only collected \emph{in the case of script validation failure},
+  and are called \emph{collateral inputs}. In the case of
+  script validation success, the fee specified in the fee field of the transaction is collected,
+  but the collateral is not.
+
+  This scheme is different from the gas model in that the exact payment collected in
+  both the case of script validation success and validation failure is known ahead of time,
+  though the collected fees are different in the two cases.
 \end{itemize}
 
 Another important point to make about both native and non-native scripts on Cardano is that

alonzo/formal-spec/ledger.tex

@@ -5,11 +5,11 @@ \section{Ledger State Transition}
 in a transaction successfully validate from the case where there is one or more that does not.
 These two cases are distinguished by the use of the $\IsValidating$ tag.
 %
-Besides fee collection, no side effects should occur when processing a
+Besides collateral collection, no side effects should occur when processing a
 transaction that contains a script that does not validate. That is, no
 delegation or pool state updates, update proposals, or any other observable state change, should be
 applied. The UTxO rule is still applied, however, as this is where the correctness of the
-validation tag is verified, and where script fees are collected.
+validation tag is verified, and where collateral inputs are collected.
 
 \begin{figure}
   \begin{equation}

alonzo/formal-spec/properties.tex

@@ -17,14 +17,14 @@ \section{Formal Properties}
 \item
   \emph{General Accounting.}
   The \emph{general accounting} property\todo{Reference or explain this} holds for any transaction,
-  whether it is fully processed or just paying fees. In particular,
+  whether it is fully processed or just paying collateral. In particular,
   this implies that the total amount of Ada in the system is constant.
 \item
   \emph{Fee Movement.}
-  If a transaction is accepted and marked as paying fees only
+  If a transaction is accepted and marked as paying collateral only
   (i.e. $\fun{isValidating}\, tx = \False$), then the only change to the ledger
-  when processing the transaction is that the inputs marked for paying
-  fees are moved to the fee pot.
+  when processing the transaction is that the collateral inputs
+  are moved to the fee pot.
 \item
   \emph{Transaction Validation.}
   If a Shelley transaction is accepted, it is fully processed.\todo{What does this mean? Is this: Transaction consistency - any transaction that is successfully validated can be executed successfully by the interpreter.}

alonzo/formal-spec/protocol-parameters.tex

@@ -93,6 +93,19 @@ \subsection{Script Evaluation Cost Model and Prices}
 used (in the ShelleyMA era) to limit the size of the the $\Value$ part of an output in a
 serialised transaction.
 
+\textbf{Collateral inputs.}
+Collateral inputs in a transaction are used to cover the transaction fees in the case
+that a non-native script fails (see Section~\ref{sec:transctions}).
+The term \emph{collateral} refers to the total ada contained in the UTxOs referenced 
+by collateral inputs.
+
+The parameter $\var{collateralPercent}$ is used to specify the percentage of
+the total transaction fee its collateral must (at minimum) cover. The
+collateral inputs must not themselves be locked by a script. That is, they must
+be VK inputs. The parameter $\var{maxCollInputs}$ is used to limit, additionally,
+the total number of collateral inputs, and thus the total number of additional
+signatures that must be checked during validation.
+
 \begin{figure*}[htb]
   \emph{Abstract types}
   %
@@ -151,6 +164,10 @@ \subsection{Script Evaluation Cost Model and Prices}
         % & \text{Max size a value can be}\\
         \var{adaPerUTxOWord} \mapsto \Coin & \PParams \\
         % & \text{Min. ada per word (8 bytes) a UTxO entry must contain}
+        \var{collateralPercent} \mapsto \N & \PParams \\
+        % & \text{Percentage of Tx fee which collateral must cover}
+        \var{maxCollInputs} \mapsto \N & \PParams \\
+        % & \text{Maximum number of VK inputs that can be used to cover collateral}
       \end{array}
   \end{equation*}
   %
@@ -164,7 +181,7 @@ \subsection{Script Evaluation Cost Model and Prices}
   %
   \begin{align*}
     & \fun{getLanguageView} \in \PParams \to \Language \to \LangDepView \\
-    & \fun{getLanguageView}~\var{pp}~\PlutusVI = \var{costmdls}~\mapsto~\{\PlutusVI\} \restrictdom \fun{costmdls}~{pp}
+    & \fun{getLanguageView}~\var{pp}~\PlutusVI = \var{costmdls}~\mapsto~ (\fun{costmdls}~{pp}~\{\PlutusVI\})
   \end{align*}
   %
   \caption{Definitions Used in Protocol Parameters}

alonzo/formal-spec/transactions.tex

@@ -57,7 +57,8 @@ \section{Transactions}
 We add the following helper functions:
 
 \begin{itemize}
-  \item $\fun{language}$ selects the language of a non-native script.
+  \item $\fun{language}$ selects the language of a non-native script, and $\Nothing$ in case
+  the script is native.
   \item $\fun{hashData}$ hashes a value of type $\Data$.
   \item $\fun{hashWitnessPPData}$ hashes the protocol parameters and witnesses relevant to script execution.
 \end{itemize}
@@ -113,7 +114,7 @@ \section{Transactions}
   \emph{Helper Functions}
   %
   \begin{align*}
-    \fun{language}& \in \ScriptNonNative \to \Language\\
+    \fun{language}& \in \Script \to \Language^?\\
     \fun{hashData}& \in \Data \to \DataHash
     \nextdef
     \fun{hashWitnessPPData}&\in\PParams \to \powerset{\Language} \to (\RdmrPtr \mapsto \Redeemer \times \ExUnits)\\
@@ -149,11 +150,11 @@ \section{Transactions}
     \begin{array}{r@{~~}l@{~~}l@{\qquad}l}
       \var{txbody} ~\in~ \TxBody ~=~
       & \powerset{\TxIn} & \fun{txinputs}& \text{Inputs}\\
-      & \times \hldiff{\powerset{\TxIn}} & \hldiff{\fun{txinputs_{fee}}}& \text{Fee inputs}\\
-      &\times ~(\Ix \mapsto \TxOut) & \fun{txouts}& \text{Outputs}\\
+      & \times ~\hldiff{\powerset{\TxIn}} & \hldiff{\fun{collateral}} & \text{Collateral inputs}\\
+      & \times ~(\Ix \mapsto \TxOut) & \fun{txouts}& \text{Outputs}\\
       & \times~ \seqof{\DCert} & \fun{txcerts}& \text{Certificates}\\
        & \times ~\Value  & \fun{mint} &\text{A minted value}\\
-       & \times ~\Coin & \fun{txfee} &\text{Non-script fee}\\
+       & \times ~\Coin & \fun{txfee} &\text{Total fee}\\
        & \times ~\ValidityInterval & \fun{txvldt} & \text{Validity interval}\\
        & \times~ \Wdrl  & \fun{txwdrls} &\text{Reward withdrawals}\\
        & \times ~\Update^?  & \fun{txUpdates} & \text{Update proposals}\\
@@ -221,14 +222,23 @@ \subsection{Witnessing}
 \end{description}
 
 \subsection{Transactions}
+\label{sec:transctions}
 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 The new field $\fun{collateral}$ is used to specify the \emph{collateral inputs}
+    that are collected (into the fee pot) to cover a percentage of
+    transaction fees (usually $100$ percent or more)
+    \emph{in case the transaction contains failing non-native scripts}. They are not collected otherwise.
+    The purpose of these is to cover the resource use costs incurred by block producers running not only
+    scripts that validate, but the failing one also. Only the inputs that are locked by VKeys can
+    be used for collateral, and they must only contain ada.
+
+    It is permitted to use the same inputs as both collateral and a regular inputs, as exactly
+    one set of inputs is ever collected : collateral ones in the case of script failure, and regular inputs
+    in the case when all scripts validate.
+
   \item There is a new field called $\fun{reqSignerHashes}$ that is used to specify a set of signers (via the
     hashes of their VKeys) that the scripts a transaction is carrying expect to have signed the transaction.
     These signatures are required in addition to the ones required by VKey addresses, and
@@ -250,7 +260,7 @@ \subsection{Transactions}
 \begin{enumerate}
   \item the transaction body,
   \item all the information that is needed to witness transactions,
-  \item the $\IsValidating$ tag, which indicates whether all scripts with all inputs
+  \item the $\IsValidating$ tag, which indicates whether all scripts
   that are executed during the script execution phase validate.
   The correctness of the tag is verified as part of the ledger rules, and the block is
   deemed to be invalid if it is applied incorrectly.
@@ -283,25 +293,3 @@ \subsection{Additional Role of Signatures on TxBody}
 script interpreters are included in the body of the transaction. In the future, other parts of the ledger
 state may also need to be included in this hash, if they are passed as
 arguments to new script interpreter.
-
-The owner of any tokens that are spent as part of a given transaction
-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 transaction body.
-
-\subsection{Fee charges in the event of script validation failure}
-
-We have considered two ways to prevent all the Ada that exists in the transaction outputs from being transferred to
-the fee pot if script validation fails:
-%
-\begin{enumerate}
-  \item programmatically select the inputs that will be used to pay fees;
-  \item allow the user to decide which inputs will be used to pay fees.
-\end{enumerate}
-%
-In order to maximise flexibility, we have chosen to use the second option.
-This also allows users to provide their own programmatic solutions to choosing the inputs that are used to pay fees.
-
-Only the inputs that are locked by VKeys or native scripts can
-be used to pay fees.