Merge pull request #2448 from input-output-hk/andre/alonzo-audit

Alonzo audit

alonzo/formal-spec/chain.tex

@@ -77,7 +77,7 @@ \subsection{Block Body Transition}
       \fun{bbodyhash}~{txs} = \bhash{bhb}
       \\~\\
       \\
-      \var{slot} \leteq \bslot{bhbh}
+      \var{slot} \leteq \bslot{bhb}
       &
       \var{fSlot} \leteq \fun{firstSlot}~(\epoch{slot})
       \\~\\

alonzo/formal-spec/introduction.tex

@@ -1,7 +1,5 @@
 \section{Introduction}
 
-\TODO{Please run a spell checker over the final document}
-
 This document describes the extensions to the multi-asset formal ledger specification~\cite{shelley_ma_spec} that are
 required for the support of phase two scripts, in particular Plutus Core. This underpins future Plutus development: there should be minimal changes to these ledger rules to support future phase-2 languages (eg. upcoming versions of Plutus).
 %
@@ -43,7 +41,7 @@ \subsection{Phase Two Scripts}
 This may be used, for example, if a more efficient interpreter is produced.
 
 The approach we use to bound execution costs to a pre-determined constant is
-distinct from the usual ``gas'' model~\cite{XX}.\TODO{And this one, please!} in the following notable ways :
+distinct from the usual ``gas'' model in the following notable ways :
 
 \begin{itemize}
   \item The exact budget to run a script is expressed in terms of computational resources,
@@ -79,10 +77,10 @@ \subsection{Phase Two Scripts}
 makes UTxO entries locked by that script unspendable.
 
 We use the terms Plutus, $\PlutusVI$, and ``phase two scripting language'' in this specification
-somewhat interchangably. The reason for this is that while we intend for the infrastructure
+somewhat interchangeably. The reason for this is that while we intend for the infrastructure
 set up in this document to be somewhat language-agnostic (in particular,
 able to support multiple versions of Plutus), it only gives all the details for
-the first and (currenly only) phase-2 script language, $\PlutusVI$,
+the first and (currently only) phase-2 script language, $\PlutusVI$,
 the introduction of which represents the
 start of the Alonzo era.
 

alonzo/formal-spec/properties.tex

@@ -51,7 +51,7 @@ \section{Formal Properties}
   \begin{itemize}
     \item preservation of value property expressed via the $\fun{produced}$ and $\fun{consumed}$
     calculations, applicable for transactions with $\fun{txValTag}~tx~=~\True$, which
-    is specified as in the ShelleMA POV.
+    is specified as in the ShelleyMA POV.
     \item the preservation of value for $\fun{txValTag}~tx~=~\False$, when
     only the collateral fees are collected into the fee pot.
   \end{itemize}
@@ -79,7 +79,7 @@ \section{Formal Properties}
 
   Note that in the $\fun{feesOK}$ function, there is a check that verifies
   that, in the case that there are phase-2 scripts, there are no non-Ada tokens in the UTxOs
-  which the collateral inputs reference, so non-Ada tokens do not get minted, burned, or transfered
+  which the collateral inputs reference, so non-Ada tokens do not get minted, burned, or transferred
   in this case.
 \end{proof}
 \end{property}
@@ -187,15 +187,15 @@ \section{Formal Properties}
   of transitions called in the order $\mathsf{LEDGER}, \mathsf{UTXOW}, \mathsf{UTXO}, \mathsf{UTXOS}$.
 
   The $\mathsf{Scripts{-}Yes}$ rule (i.e. $\fun{txValTag} = \True$)
-  transfers the amount of lovelace in the $\fun{txfee}$ field of the
+  transfers the amount of Lovelace in the $\fun{txfee}$ field of the
   transaction to the fee pot, which is checked to be at least the $\fun{minfee}$
   by $\fun{feesOK}$ in the $\mathsf{UTXO}$ transition. So, we get
 
   \[\field_{fees}~(s')~=~\field_{fees}~(s)~+~\fun{txfee}~{tx}~\geq~\field_{fees}~(s)~+~\fun{minfee}~{tx}\]
 
   The $\mathsf{Scripts{-}No}$ rule (i.e. $\fun{txValTag} = \False$) removes the
   $\fun{collateral}$ inputs from the
-  UTxO, and adds the the balance of these realized inputs to the fee pot.
+  UTxO, and adds the balance of these realized inputs to the fee pot.
 
   \[\field_{fees}~(s')~=~field_{fees}~(s)~+~\fun{ubalance}~(\fun{collateral}~{txb} \restrictdom \var{utxo})\]
 
@@ -417,7 +417,7 @@ \section{Formal Properties}
     The $\fun{collectTwoPhaseScriptInputs}$
     function (see \ref{fig:functions:script2})
     constructs a list where each entry contains a Plutus script
-    and the argumets passed to the interpreter for its evaluation.
+    and the arguments passed to the interpreter for its evaluation.
 
     To show that $\fun{collectTwoPhaseScriptInputs}$ returns a list containing
     the same elements for both $tx$ and $tx'$, we observe that
@@ -454,7 +454,7 @@ \section{Formal Properties}
       (and, by the same argument, the datum hash) are fixed by the inputs in body of the
       transaction, despite not being explicitly contained in it. We then get that
 
-      \[ \fun{scriptsNeeded}~\Utxo(s)~tx = \fun{scriptsNeeded}~\Utxo(u)~tx' \]
+      \[ \fun{scriptsNeeded}~\Utxo(s)~(\txbody{tx}) = \fun{scriptsNeeded}~\Utxo(u)~(\txbody{tx'}) \]
 
       \item $\fun{getDatum}$ : In the case the script purpose
       is of the input type, the datum this function returns is one that
@@ -512,13 +512,13 @@ \section{Formal Properties}
 
         \item $\fun{txInfoValidRange}$ : this field contains the transaction
         validity interval as system time (converted from the slot numbers, which are
-        used to speficy the interval in the transaction body). This conversion is
+        used to specify the interval in the transaction body). This conversion is
         done by a function defined in the consensus layer, and takes two global
         constants in addition to the slot interval itself. Since the slot interval
         conversion function $\fun{epochInfoSlotToUTCTime}$ necessarily
         succeeds if both $tx$ and $tx'$ pass phase-1 validation, the additional
         global constant arguments must be the same (by assumption). The determinism of this conversion
-        is one of the assumptions of this property, and thus gives the same ouput
+        is one of the assumptions of this property, and thus gives the same output
         for both transactions.
 
         \item $\fun{txInfoData}$ : this field is populated with the datums (and their
@@ -574,13 +574,13 @@ \section{Formal Properties}
 
     \begin{itemize}
       \item has no impact on the outcome of script evaluation in the case the script
-      being validated at this step is phase-2, as it is competely ignored, and,
+      being validated at this step is phase-2, as it is completely ignored, and,
 
       \item because $\fun{collectTwoPhaseScriptInputs}$ filters out all phase-1 scripts,
       is, in fact, ignored always.
     \end{itemize}
 
-    The second argument to $\fun{evalScripts}$, ie. the list of scripts and their arguemnts,
+    The second argument to $\fun{evalScripts}$, ie. the list of scripts and their arguments,
     has already been shown to contain the same tuples for both transactions in the lemma above.
     The order of the list does not affect the validation outcome, since the interpreter is run
     on each tuple of a script and its arguments independently of all other tuples in the list.

alonzo/formal-spec/protocol-parameters.tex

@@ -25,7 +25,7 @@ \section{Language Versions and Cost Models}
   $\ExUnits$ &
   $(mem, steps)\in \ExUnits$ is made up of two integer values.
   These represent abstract notions of the relative memory usage and script execution steps,
-  respectively.
+  respectively. We give it the structure of a partially ordered monoid via its product structure, i.e. addition and comparisons are defined point-wise.
   \\
   $\LangDepView$ &
   A pair of two byte strings, where the first represents the serialized language tag (eg. the tag for $\PlutusVI$),
@@ -104,19 +104,19 @@ \subsection{Script Evaluation Cost Model and Prices}
 
 \textbf{Value size limit as a protocol parameter.}
 The new parameter $\var{maxValSize}$ replaces the constant $\mathsf{maxValSize}$
-used (in the ShelleyMA era) to limit the size of the the $\Value$ part of an output in a
+used (in the ShelleyMA era) to limit the size of 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 phase-2 script fails (see Section~\ref{sec:transctions}).
-The term \emph{collateral} refers to the total ada contained in the UTxOs referenced
+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,
+be VKey inputs. The parameter $\var{maxCollateralInputs}$ 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.
 
@@ -158,7 +158,7 @@ \subsection{Script Evaluation Cost Model and Prices}
   %
   \begin{equation*}
       \begin{array}{r@{~\in~}l@{\qquad}r}
-        \var{minUTxOValue} \mapsto \Coin & \PParams & \text{Min. amount of ada each UTxO must contain}
+        \var{minUTxOValue} \mapsto \Coin & \PParams & \text{Min. amount of Ada each UTxO must contain}
       \end{array}
   \end{equation*}
   %
@@ -177,18 +177,19 @@ \subsection{Script Evaluation Cost Model and Prices}
         \var{maxValSize} \mapsto \N & \PParams \\
         % & \text{Max size a value can be}\\
         \var{coinsPerUTxOWord} \mapsto \Coin & \PParams \\
-        % & \text{Min. lovelace per word (8 bytes) a UTxO entry must contain}
+        % & \text{Min. Lovelace 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 \\
+        \var{maxCollateralInputs} \mapsto \N & \PParams \\
         % & \text{Maximum number of VK inputs that can be used to cover collateral}
       \end{array}
   \end{equation*}
   %
   \emph{Accessor Functions}
   %
   \begin{center}
-  \fun{costmdls},~\fun{maxTxExUnits},~\fun{maxBlockExUnits},~\fun{prices}
+    \fun{costmdls},~\fun{prices},~\fun{maxTxExUnits},~\fun{maxBlockExUnits},~\fun{maxValSize},~\fun{coinsPerUTxOWord},\\
+    \fun{collateralPercent},~\fun{maxCollateralInputs}
   \end{center}
   %
   \emph{Helper Functions}

alonzo/formal-spec/transactions.tex

@@ -182,7 +182,7 @@ \section{Transactions}
 \end{figure*}
 
 \textbf{Auxiliary Data. } The auxiliary data in an Alonzo transaction has the same structure as
-in a ShelleMA transaction, but can additionally contain phase-2 scripts.
+in a ShelleyMA transaction, but can additionally contain phase-2 scripts.
 
 \subsection{Witnessing}
 Figure \ref{fig:defs:utxo-shelley-2} defines the witness type, $\TxWitness$.  This contains everything
@@ -206,7 +206,7 @@ \subsection{Witnessing}
   [Hash reference (script/datum object):]
   Scripts and datum objects are referred to explicitly via their hashes,
   which are included in the $\UTxO$ or the transaction. Thus, they can be
-  looked up in the tranasaction without any key in the data structure.
+  looked up in the transaction without any key in the data structure.
 
   \item[No hash reference (redeemers):] For redeemers,
   we use a reverse pointer approach and
@@ -226,7 +226,7 @@ \subsection{Transactions}
     \emph{in case the transaction contains failing phase-2 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.
+    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