From ed5a6d3f27325a8b863edd65feac68309f0967f6 Mon Sep 17 00:00:00 2001 From: whatisRT Date: Tue, 12 Oct 2021 16:24:42 +0200 Subject: [PATCH 1/2] Address issues pointed out in the audit and other cleanup --- eras/alonzo/formal-spec/alonzo-changes.tex | 3 +- eras/alonzo/formal-spec/chain.tex | 24 ++-- eras/alonzo/formal-spec/introduction.tex | 19 +-- .../formal-spec/protocol-parameters.tex | 47 ++++---- eras/alonzo/formal-spec/transactions.tex | 73 ++++++------ eras/alonzo/formal-spec/utxo.tex | 108 +++++++++--------- 6 files changed, 128 insertions(+), 146 deletions(-) diff --git a/eras/alonzo/formal-spec/alonzo-changes.tex b/eras/alonzo/formal-spec/alonzo-changes.tex index de1965f30cf..9f986c411c1 100644 --- a/eras/alonzo/formal-spec/alonzo-changes.tex +++ b/eras/alonzo/formal-spec/alonzo-changes.tex @@ -379,8 +379,6 @@ \include{chain} -\include{value-size} - %\include{constants} @@ -390,6 +388,7 @@ \begin{appendix} \include{txinfo} + \include{value-size} \include{properties} \end{appendix} diff --git a/eras/alonzo/formal-spec/chain.tex b/eras/alonzo/formal-spec/chain.tex index 24bfd359660..bc3470b8725 100644 --- a/eras/alonzo/formal-spec/chain.tex +++ b/eras/alonzo/formal-spec/chain.tex @@ -117,35 +117,35 @@ \subsection{Block Body Transition} \end{figure} We have also defined a function that transforms the Shelley ledger state into -the corresponding Goguen one, see Figure~\ref{fig:functions:to-shelley}. We -refer to the Shelley-era protocol parameter type as $\ShelleyPParams$, and the corresponding Goguen +the corresponding Alonzo one, see Figure~\ref{fig:functions:to-shelley}. We +refer to the Shelley-era protocol parameter type as $\ShelleyPParams$, and the corresponding Alonzo type as $\PParams$. We use the notation $\var{chainstate}_{x}$ to represent variable $x$ in the chain state. We do not specify the variables that remain unchanged during the transition. %% -%% Figure - Shelley to Goguen Transition +%% Figure - Shelley to Alonzo Transition %% \begin{figure}[htb] \emph{Types and Constants} % \begin{align*} - & \NewParams ~=~ (\Language \mapsto \CostMod) \times \Prices \times \ExUnits \times \ExUnits \\ + & \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} + & \text{the type of new parameters to add for Alonzo} \nextdef - & \var{ivPP} ~\in~ \NewParams \\ - & \text{the initial values for new Goguen parameters} + & \var{ivPP} \in \NewParams \\ + & \text{the initial values for new Alonzo parameters} \end{align*} - \emph{Shelley to Goguen Transition Functions} + \emph{Shelley to Alonzo Transition Functions} % \begin{align*} - & \fun{toGoguen} \in \ShelleyChainState \to \ChainState \\ - & \fun{toGoguen}~\var{chainstate} =~\var{chainstate'} \\ + & \fun{toAlonzo} : \ShelleyChainState \to \ChainState \\ + & \fun{toAlonzo}~\var{chainstate} =~\var{chainstate'} \\ &~~\where \\ &~~~~\var{chainstate'}_{pparams}~=~(\var{pp}\cup \var{ivPP})~ - ~\var{minUTxOValue}\\ - & \text{transform Shelley chain state to Goguen state} + & \text{transform Shelley chain state to Alonzo state} \end{align*} - \caption{Shelley to Goguen State Transtition} + \caption{Shelley to Alonzo State Transtition} \label{fig:functions:to-shelley} \end{figure} diff --git a/eras/alonzo/formal-spec/introduction.tex b/eras/alonzo/formal-spec/introduction.tex index 2b621adeb31..a0f1c9df6b3 100644 --- a/eras/alonzo/formal-spec/introduction.tex +++ b/eras/alonzo/formal-spec/introduction.tex @@ -44,21 +44,14 @@ \subsection{Phase Two Scripts} 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, - and included in the transaction data. This resource budget can be computed before submitting a transaction. - In contrast with the gas model, where the budget is expressed indirectly, - in terms of an upper bound on the fee the author is willing to pay for execution of the + \item The budget to run a script is expressed in terms of computational resources, + and included in the transaction data. The \emph{exact} resource budget required can + be computed before submitting a transaction, since script execution is deterministic. + See Section \ref{sec:determinism}. + In the gas model, the budget is expressed indirectly as an upper bound + on the fee the submitter is willing to pay for execution of the 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, - 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 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}, diff --git a/eras/alonzo/formal-spec/protocol-parameters.tex b/eras/alonzo/formal-spec/protocol-parameters.tex index c72581b9d5f..267a317e7c0 100644 --- a/eras/alonzo/formal-spec/protocol-parameters.tex +++ b/eras/alonzo/formal-spec/protocol-parameters.tex @@ -6,27 +6,26 @@ \section{Language Versions and Cost Models} \vspace{12pt} \begin{tabular}{lp{5in}} + $\ExUnits$ & + $\ExUnits$ is made up of two integer values, representing abstract notions of the + relative memory usage and script execution steps respectively. + We give it the structure of a partially ordered monoid via its product structure, + i.e. addition and comparisons are defined point-wise. + \\ + $\Prices$ & + $\Prices$ consists of two rational numbers that correspond to the components of $\ExUnits$: + the price per unit of memory and price per reduction step. + \\ $\CostMod$ & - $c\in\CostMod$ is the vector of coefficients that are used to compute - a value $exu\in\ExUnits$ given a vector of some resource primitives. The mapping is defined - concretely by the specific version of the Plutus interpreter that is associated with $\Language$. + A cost model is a vector of coefficients that are used to compute + the execution units required to execute a script. Its specifics depend on + specific versions of the Plutus interpreter it is used with. We keep this type as abstract in the specification, see \cite{plutuscore} and \cite{plutustech} for details. \\ $\Language$ & This represents phase-2 language types. Currently there is only $\PlutusVI$. \\ - $\Prices$ & - $\var{(pr_{mem}, pr_{steps})}\in \Prices$ consists of two rational numbers - that correspond to the components of $\ExUnits$: - $pr_{mem}$ is the price per unit of memory, and $pr_{steps}$ is the price per - reduction step. This is used to calculate the cost for a specific script execution. - \\ - $\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. 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$), and the second, the protocol parameters that must be fixed (by the transaction) when carrying a phase-2 script @@ -124,31 +123,27 @@ \subsection{Script Evaluation Cost Model and Prices} \emph{Abstract types} % \begin{equation*} - \begin{array}{r@{~\in~}l@{\qquad\qquad\qquad}r} - \var{cm} & \CostMod & \text{Coefficients for the cost model} + \begin{array}{l@{\qquad\qquad\qquad}r} + \CostMod & \text{Coefficients for the cost model} \end{array} \end{equation*} % \emph{Derived types} \begin{equation*} - \begin{array}{r@{~\in~}l@{\quad=\quad}l@{\qquad}r} - \var{lg} - & \Language + \begin{array}{l@{\quad=\quad}l@{\qquad}r} + \Language & \{\PlutusVI, \dotsb\} & \text{Script Language} \\ - \var{(pr_{mem}, pr_{steps})} - & \Prices + \Prices & \mathsf{Rational} \times \mathsf{Rational} & \text {Coefficients for $\ExUnits$ prices} \\ - \var{(mem, steps)} - & \ExUnits + \ExUnits & \N \times \N & \text{Abstract execution units} \\ - \var{ldv} - & \LangDepView + \LangDepView & \ByteString~\times~\ByteString & \text{Language Tag and PParams view} \end{array} @@ -195,7 +190,7 @@ \subsection{Script Evaluation Cost Model and Prices} \emph{Helper Functions} % \begin{align*} - & \fun{getLanguageView} \in \PParams \to \Language \to \LangDepView \\ + & \fun{getLanguageView} : \PParams \to \Language \to \LangDepView \\ & \fun{getLanguageView}~\var{pp}~\PlutusVI = (\fun{serialize}~\PlutusVI, ~ (\fun{serialize}~(\fun{costmdls}~{pp}~\{\PlutusVI\}))) \end{align*} \caption{Definitions Used in Protocol Parameters} diff --git a/eras/alonzo/formal-spec/transactions.tex b/eras/alonzo/formal-spec/transactions.tex index 8bf71f39df7..feab8e710db 100644 --- a/eras/alonzo/formal-spec/transactions.tex +++ b/eras/alonzo/formal-spec/transactions.tex @@ -68,66 +68,59 @@ \section{Transactions} \emph{Abstract types} % \begin{equation*} - \begin{array}{r@{~\in~}l@{\quad\quad\quad\quad}r} - \var{wph} &\ScriptIntegrityHash & \text{Script data hash}\\ - \var{plc} & \ScriptPlutus & \text{Plutus core scripts} \\ - \var{d} & \Data & \text{Generic script data} + \begin{array}{l@{\quad\quad\quad\quad}r} + \ScriptIntegrityHash & \text{Script data hash}\\ + \ScriptPlutus & \text{Plutus core scripts} \\ + \Data & \text{Generic script data} \end{array} \end{equation*} % \emph{Script types} % \begin{equation*} - \begin{array}{r@{~\in~}l@{\qquad=\qquad}lr} - \var{sc} & \ScriptPhTwo & \ScriptPlutus \\ - \var{sc} & \Script & \ScriptPhOne \uniondistinct \ScriptPhTwo \\ - \var{isv} & \IsValid & \Bool \\ - \var{d} & \Datum & \Data \\ - \var{r} & \Redeemer & \Data + \begin{array}{l@{\qquad=\qquad}lr} + \ScriptPhTwo & \ScriptPlutus \\ + \Script & \ScriptPhOne \uniondistinct \ScriptPhTwo \\ + \IsValid & \Bool \\ + \Datum & \Data \\ + \Redeemer & \Data \end{array} \end{equation*} % \emph{Derived types} % \begin{equation*} - \begin{array}{r@{~\in~}l@{\qquad=\qquad}lr} - \var{vi} - & \ValidityInterval + \begin{array}{l@{\qquad=\qquad}lr} + \ValidityInterval & \Slot^? \times \Slot^? -% & \text{validity interval} \\ - \var{txout} - & \TxOut + \TxOut & \Addr \times \Value \times \hldiff{\DataHash^?} -% & \text{transaction outputs in a transaction} \\ - \var{tag} - & \Tag + \Tag & \{\mathsf{Spend},~\mathsf{Mint},~\mathsf{Cert},~\mathsf{Rewrd}\} \\ - \var{rdptr} - & \RdmrPtr + \RdmrPtr & \Tag \times \Ix -% & \text{reverse pointer to thing dv is for} \end{array} \end{equation*} % \emph{Helper Functions} % \begin{align*} - \fun{language}& \in \Script \to \Language^?\\ - \fun{hashData}& \in \Data \to \DataHash + \fun{language}& : \Script \to \Language^?\\ + \fun{hashData}& : \Data \to \DataHash \nextdef - \fun{getCoin}& \in \TxOut \to \Coin \\ - \fun{getCoin}&~\hldiff{{(\_, \var{v}, \_)}} ~=~\fun{valueToCoin}~{v} + \fun{getCoin}& : \TxOut \to \Coin \\ + \fun{getCoin}&~\hldiff{{(\_, \var{v}, \_)}} = \fun{valueToCoin}~{v} \end{align*} % \begin{align*} - &\fun{hashScriptIntegrity} \in\PParams \to \powerset{\Language} \to (\RdmrPtr \mapsto \Redeemer \times \ExUnits) \\ + &\fun{hashScriptIntegrity} : \PParams \to \powerset{\Language} \to (\RdmrPtr \mapsto \Redeemer \times \ExUnits) \\ &~~~~ \to (\DataHash \mapsto \Datum) \to \ScriptIntegrityHash^? \\ - &\fun{hashScriptIntegrity}~{pp}~{langs}~{rdmrs}~{dats}~=~ \\ + &\fun{hashScriptIntegrity}~{pp}~{langs}~{rdmrs}~{dats} = \\ &~~~~ \begin{cases} - \Nothing & rdmrs~=~\emptyset \land langs~=~\emptyset \land dats~=~\emptyset \\ + \Nothing & rdmrs = \emptyset \land langs = \emptyset \land dats = \emptyset \\ \fun{hash} (rdmrs, dats, \{ \fun{getLanguageView}~pp~l \mid l \in langs \}) & \text{otherwise} \end{cases} \end{align*} @@ -141,18 +134,18 @@ \section{Transactions} % \begin{equation*} \begin{array}{r@{~~}l@{~~}l@{\qquad}l} - \var{wits} ~\in~ \TxWitness ~=~ + \TxWitness = & (\VKey \mapsto \Sig) & \fun{txwitsVKey} & \text{VKey signatures}\\ & \times ~(\ScriptHash \mapsto \Script) & \fun{txscripts} & \text{All scripts}\\ & \times~ \hldiff{(\DataHash \mapsto \Datum)} & \hldiff{\fun{txdats}} & \text{All datum objects}\\ - & \times ~\hldiff{(\RdmrPtr \mapsto \Redeemer \times \ExUnits)}& \hldiff{\fun{txrdmrs}}& \text{Redeemers/budget}\\ + & \times ~\hldiff{(\RdmrPtr \mapsto \Redeemer \times \ExUnits)}& \hldiff{\fun{txrdmrs}}& \text{Redeemers/budget} \end{array} \end{equation*} % \begin{equation*} \begin{array}{r@{~~}l@{~~}l@{\qquad}l} - \var{txbody} ~\in~ \TxBody ~=~ - & \powerset{\TxIn} & \fun{txinputs}& \text{Inputs}\\ + \TxBody = + & \powerset{\TxIn} & \fun{txins}& \text{Inputs}\\ & \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}\\ @@ -170,7 +163,7 @@ \section{Transactions} % \begin{equation*} \begin{array}{r@{~~}l@{~~}l@{\qquad}l} - \var{tx} ~\in~ \Tx ~=~ + \Tx = & \TxBody & \fun{txbody} & \text{Body}\\ & \times ~\TxWitness & \fun{txwits} & \text{Witnesses}\\ & \times ~\hldiff{\IsValid} & \hldiff{\fun{isValid}}&\text{Validation tag}\\ @@ -224,12 +217,14 @@ \subsection{Transactions} 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 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. + The purpose of the collateral is to cover the resource use costs + incurred by block producers running scripts that do not validate. + + Collateral inputs behave like regular inputs, except that they + must be VKey locked and can only contain Ada. See \ref{fig:functions:utxo}. 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 + 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 hashes @@ -261,7 +256,7 @@ \subsection{Transactions} 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. - If it is set to $\False$, then the block can be re-applied without script re-validation. + It can be used to re-apply blocks without script re-validation. This tag cannot be signed, since it is applied by the block producer. \item any auxiliary data. \end{enumerate} diff --git a/eras/alonzo/formal-spec/utxo.tex b/eras/alonzo/formal-spec/utxo.tex index 575c3a7bca9..e5d55020f30 100644 --- a/eras/alonzo/formal-spec/utxo.tex +++ b/eras/alonzo/formal-spec/utxo.tex @@ -5,35 +5,35 @@ \section{UTxO} \emph{Functions} % \begin{align*} - & \fun{isTwoPhaseScriptAddress} \in \Tx \to \Addr \to \Bool \\ + & \fun{isTwoPhaseScriptAddress} : \Tx \to \Addr \to \Bool \\ & \fun{isTwoPhaseScriptAddress}~tx~a = \\ &\quad\begin{cases} \True & a \in \AddrScr \land \fun{validatorHash}~a \mapsto s \in \fun{txscripts} (\fun{txwits}~tx) \land s \in \ScriptPhTwo \\ \False & \text{otherwise} \end{cases} \nextdef - & \fun{totExUnits} \in \Tx \to \ExUnits \\ + & \fun{totExUnits} : \Tx \to \ExUnits \\ & \fun{totExUnits}~\var{tx} = \sum_{r \in \fun{txrdmrs}~tx} \fun{exunits}~r \nextdef - & \fun{feesOK} \in \PParams \to \Tx \to \UTxO \to \Bool \\ + & \fun{feesOK} : \PParams \to \Tx \to \UTxO \to \Bool \\ & \fun{feesOK}~\var{pp}~tx~utxo~= \\ - &~~ \minfee{pp}~{tx} \leq \txfee{txb} \wedge (\fun{txrdmrs}~tx \neq \Nothing \Rightarrow \\ + &~~ \minfee{pp}~{tx} \leq \txfee{txb} \wedge (\fun{txrdmrs}~tx \neq \emptyset \Rightarrow \\ &~~~~~~((\forall (a, \wcard, \_) \in \fun{range}~(\fun{collateral}~{txb} \restrictdom \var{utxo}), a \in \AddrVKey) \\ &~~~~~~\wedge~ \fun{adaOnly}~\var{balance} \\ - &~~~~~~\wedge~ \var{balance}~*~100 \geq \txfee~{txb} * (\fun{collateralPercent}~pp))) \\ - &~~~~~~\wedge~ \fun{collateral}~{tx}~ \neq~\{\}) \\ + &~~~~~~\wedge~ \var{balance}*100 \geq \txfee{txb} * (\fun{collateralPercent}~pp))) \\ + &~~~~~~\wedge~ \fun{collateral}~{tx} \neq \emptyset) \\ &~~ \where \\ - & ~~~~~~~ \var{txb}~=~\txbody{tx} \\ - & ~~~~~~~ \var{balance}~=~\fun{ubalance}~(\fun{collateral}~{txb} \restrictdom \var{utxo}) + & ~~~~~~~ \var{txb} = \txbody{tx} \\ + & ~~~~~~~ \var{balance} = \fun{ubalance}~(\fun{collateral}~{txb} \restrictdom \var{utxo}) \nextdef - & \fun{cbalance} \in \UTxO \to \Coin \\ - & \fun{cbalance}~\var{utxo}~=~ \fun{valueToCoin}~(\fun{ubalance}~\var{utxo}) + & \fun{cbalance} : \UTxO \to \Coin \\ + & \fun{cbalance}~\var{utxo} = \fun{valueToCoin}~(\fun{ubalance}~\var{utxo}) \nextdef - & \fun{txscriptfee} \in \Prices \to \ExUnits \to \Coin \\ + & \fun{txscriptfee} : \Prices \to \ExUnits \to \Coin \\ & \fun{txscriptfee}~(pr_{mem}, pr_{steps})~ (\var{mem, steps}) = \fun{ceiling}~(\var{pr_{mem}}*\var{mem} + \var{pr_{steps}}*\var{steps}) \nextdef - &\fun{minfee} \in \PParams \to \Tx \to \Coin \\ + &\fun{minfee} : \PParams \to \Tx \to \Coin \\ &\fun{minfee}~\var{pp}~\var{tx} = \\ &~~(\fun{a}~\var{pp}) \cdot \fun{txSize}~\var{tx} + (\fun{b}~\var{pp}) + \hldiff{\fun{txscriptfee}~(\fun{prices}~{pp})~(\fun{totExunits}~(\fun{txbody}~{tx}))} @@ -165,15 +165,15 @@ \subsection{Combining Scripts with Their Inputs} % \emph{Abstract functions} \begin{align*} - &\fun{indexOf} \in \DCert \to \seqof{\DCert} \to \Ix^?\\ - &\fun{indexOf} \in \AddrRWD \to \Wdrl \to \Ix^?\\ - &\fun{indexOf} \in \TxIn \to \powerset{\TxIn} \to \Ix^?\\ - &\fun{indexOf} \in \PolicyID \to \powerset{\PolicyID} \to \Ix^? + &\fun{indexOf} : \DCert \to \seqof{\DCert} \to \Ix^?\\ + &\fun{indexOf} : \AddrRWD \to \Wdrl \to \Ix^?\\ + &\fun{indexOf} : \TxIn \to \powerset{\TxIn} \to \Ix^?\\ + &\fun{indexOf} : \PolicyID \to \powerset{\PolicyID} \to \Ix^? \end{align*} % \emph{Indexing functions} \begin{align*} - &\fun{indexedRdmrs} \in \Tx \to \ScriptPurpose \to (\Redeemer~\times~\ExUnits)^?\\ + &\fun{indexedRdmrs} : \Tx \to \ScriptPurpose \to (\Redeemer~\times~\ExUnits)^?\\ &\fun{indexedRdmrs}~tx~sp = \begin{cases} r & (\fun{rdptr}~txb~sp)~ \mapsto r \in \fun{txrdmrs}~(\fun{txwits}~{tx}) \} \\ @@ -182,13 +182,13 @@ \subsection{Combining Scripts with Their Inputs} & ~~\where \\ & ~~\quad \var{txb} = \txbody{tx} \nextdef - &\fun{rdptr} ~\in~\TxBody~\to~\ScriptPurpose~ \to~ \RdmrPtr^? \\ - &\fun{rdptr}~txb~sp~ =~ + &\fun{rdptr} :\TxBody~\to~\ScriptPurpose~ \to~ \RdmrPtr^? \\ + &\fun{rdptr}~txb~sp~ = \begin{cases} - (\mathsf{Cert},\fun{indexOf}~\var{sp}~(\fun{txcerts}~{txb})) & \var{sp}~\in~\DCert \\ - (\mathsf{Rewrd},\fun{indexOf}~\var{sp}~(\fun{txwdrls}~{txb})) & \var{sp}~\in~\AddrRWD \\ - (\mathsf{Mint},\fun{indexOf}~\var{sp}~(\dom (\fun{mint}~{txb}))) & \var{sp}~\in~\PolicyID \\ - (\mathsf{Spend},\fun{indexOf}~\var{sp}~(\fun{txinputs}~{txb})) & \var{sp}~\in~\TxIn + (\mathsf{Cert},\fun{indexOf}~\var{sp}~(\fun{txcerts}~{txb})) & \var{sp} \in \DCert \\ + (\mathsf{Rewrd},\fun{indexOf}~\var{sp}~(\fun{txwdrls}~{txb})) & \var{sp} \in \AddrRWD \\ + (\mathsf{Mint},\fun{indexOf}~\var{sp}~(\dom (\fun{mint}~{txb}))) & \var{sp} \in \PolicyID \\ + (\mathsf{Spend},\fun{indexOf}~\var{sp}~(\fun{txinputs}~{txb})) & \var{sp} \in \TxIn \end{cases} \end{align*} \caption{Indexing script and data objects} @@ -207,7 +207,7 @@ \subsection{Plutus Script Validation} \begin{itemize} \item $\fun{epochInfoSlotToUTCTime}$ translates a slot number to system time if possible. This translation is implemented by the consensus algorithm (not the ledger), and requires -two additional parameters to do this. +two additional parameters to do this. Note that this does not depend on the clock of the node. If it is not possible to do this translation, $\Nothing$ is returned. The reason it may not be possible to translate is that the slot number @@ -309,9 +309,9 @@ \subsection{Plutus Script Validation} \emph{Abstract Script Validation Functions} % \begin{align*} - &\fun{epochInfoSlotToUTCTime} \in \EpochInfo \to \SystemStart \to \Slot \to \UTCTime^? \\ + &\fun{epochInfoSlotToUTCTime} : \EpochInfo \to \SystemStart \to \Slot \to \UTCTime^? \\ &\text{Translate slot number to system time or fail} \\~\\ - &\fun{runPLCScript} \in \CostMod \to \ScriptPlutus \to \ExUnits \to \seqof{\Data} \to + &\fun{runPLCScript} : \CostMod \to \ScriptPlutus \to \ExUnits \to \seqof{\Data} \to \IsValid \\ &\text{Validate a Plutus script, taking resource limits into account} \end{align*} @@ -365,8 +365,8 @@ \subsection{Plutus Script Validation} it evaluates them paired with all their inputs by calling the phase-2 script validator function, $\fun{runPLCScript}$ (see \ref{sec:txinfo} for details). - For phase-1 (timelock) scripts, it calls $\fun{evalTimelock}$. Note that although this - case is covered in the $\fun{evalScripts}$ definition, it should never be used, as + For phase-1 (timelock) scripts, it calls $\fun{evalTimelock}$. This case + is unused though, as the list of scripts and inputs that gets passed to the this function is constructed to contain only Plutus scripts. So, phase-1 scripts do not get evaluated twice. \end{itemize} @@ -378,26 +378,26 @@ \subsection{Plutus Script Validation} \begin{figure}[htb] \begin{align*} - & \fun{getDatum} \in \Tx \to \UTxO \to \ScriptPurpose \to \seqof{\Datum} \\ - & \fun{getDatum}~{tx}~{utxo}~{sp}~=~ + & \fun{getDatum} : \Tx \to \UTxO \to \ScriptPurpose \to \seqof{\Datum} \\ + & \fun{getDatum}~{tx}~{utxo}~{sp} = \begin{cases} [\var{d}] & \var{sp} \mapsto (\_, \_, h_d) \in \var{utxo}, \var{h_d}\mapsto \var{d} \in \fun{txdats}~(\fun{txwits}~tx) \\ \epsilon & \text{otherwise} \end{cases} \nextdef - & \fun{collectTwoPhaseScriptInputs} \in \EpochInfo \to \SystemStart \to \PParams \to \Tx \to \UTxO \to \\ + & \fun{collectTwoPhaseScriptInputs} : \EpochInfo \to \SystemStart \to \PParams \to \Tx \to \UTxO \to \\ & ~~~~ \seqof{(\Script \times \seqof{\Data} \times \ExUnits \times \CostMod)} \\ - & \fun{collectTwoPhaseScriptInputs} ~\var{ei}~\var{sysSt}~\var{pp}~\var{tx}~ \var{utxo} ~=~ \\ - & ~~\fun{toList} \{ (\var{script}, (\fun{getDatum}~tx~utxo~sp~++~[~\var{rdmr};~\fun{valContext}~\var{txinfo}~\var{sp}~]), \var{eu}, \var{cm}) \mid \\ + & \fun{collectTwoPhaseScriptInputs} ~\var{ei}~\var{sysSt}~\var{pp}~\var{tx}~ \var{utxo} = \\ + & ~~\fun{toList} \{ (\var{script}, (\fun{getDatum}~tx~utxo~sp ; \var{rdmr};\fun{valContext}~\var{txinfo}~\var{sp}), \var{eu}, \var{cm}) \mid \\ & ~~~~(\var{sp}, \var{scriptHash}) \in \fun{scriptsNeeded}~{utxo}~{(\txbody{tx})}, \\ & ~~~~\var{scriptHash}\mapsto \var{script}\in \fun{txscripts}~(\fun{txwits}~tx), \\ & ~~~~(\var{rdmr}, \var{eu}) := \fun{indexedRdmrs}~tx~sp, \\ & ~~~~\fun{language}~{script} \mapsto \var{cm} \in \fun{costmdls}~{pp}, \\ & ~~~~\var{script} \in \ScriptPhTwo \} \\ & \where \\ - & ~~~~~~~ \var{txinfo}~=~\fun{txInfo}~\var{ei}~\var{sysSt}~(\fun{language}~{script})~{pp}~\var{utxo}~\var{tx} \\ + & ~~~~~~~ \var{txinfo} = \fun{txInfo}~\var{ei}~\var{sysSt}~(\fun{language}~{script})~{pp}~\var{utxo}~\var{tx} \nextdef - & \fun{evalScripts} \in \Tx \times \seqof{(\Script \times \seqof{\Data} \times \ExUnits \times \CostMod)} \to \IsValid \\ + & \fun{evalScripts} : \Tx \times \seqof{(\Script \times \seqof{\Data} \times \ExUnits \times \CostMod)} \to \IsValid \\ & \fun{evalScripts}~\var{tx}~\epsilon = \True \\ & \fun{evalScripts}~\var{tx}~((\var{sc}, \var{d}, \var{eu}, \var{cm});\Gamma) = \\ & \begin{cases} @@ -465,7 +465,7 @@ \subsection{The UTXOS transition system} \label{sec:utxo-state-trans} We have defined a separate transition system, UTXOS, to represent the two distinct -UTxO state changes: i) when all the scripts in a transaction validating; and +UTxO state changes: i) when all the scripts in a transaction validate; and ii) when at least one fails to validate. Its transition types are identical to the UTXO transition (Figure \ref{fig:ts-types:utxo-scripts}). @@ -552,7 +552,7 @@ \subsection{The UTXOS transition system} \trans{utxos}{tx} \left( \begin{array}{r} - \varUpdate{\var{(\txins{txb} \subtractdom \var{utxo}) \cup \outs~{txb}}} \\ + \varUpdate{\var{(\txins{txb} \subtractdom \var{utxo}) \cup \outs{txb}}} \\ \varUpdate{\var{deposits} + \var{depositChange}} \\ \varUpdate{\var{fees} + \txfee{txb}} \\ \varUpdate{\var{pup'}} \\ @@ -643,27 +643,27 @@ \subsection{The UTXOS transition system} \inference[UTxO-inductive] { \var{txb}\leteq\txbody{tx} & - \fun{ininterval}~\var{slot}~(\fun{txvldt}~{tx}) & + \fun{ininterval}~\var{slot}~(\fun{txvldt}~{txb}) & \hldiff{\var{(\wcard, i_f)}\leteq\fun{txvldt}~{tx}} \\~\\ - \hldiff{\Nothing \notin \{\fun{txrdmrs}~\var{tx}, i_f\} ~\Rightarrow~ \fun{epochInfoSlotToUTCTime}~\mathsf{EI}~\mathsf{SysSt}~i_f \neq \Nothing} \\ + \hldiff{\Nothing \notin \{\fun{txrdmrs}~\var{tx}, i_f\} \Rightarrow \fun{epochInfoSlotToUTCTime}~\mathsf{EI}~\mathsf{SysSt}~i_f \neq \Nothing} \\ \txins{txb} \neq \emptyset & \hldiff{\fun{feesOK}~pp~tx~utxo} & \txins{txb}~\cup~\fun{collateral}~{txb}~ \subseteq~ \dom \var{utxo} \\ - \consumed{pp}{utxo}{txb} = ~\produced{pp}{poolParams}~{txb} + \consumed{pp}{utxo}{txb} = \produced{pp}{poolParams}~{txb} \\~\\ \mathsf{adaID}\notin \supp {\fun{mint}~tx} \\~\\ \forall txout \in \txouts{txb}, \\ \fun{getValue}~txout \geq \fun{inject}~(\hldiff{\fun{utxoEntrySize}~{txout} * \fun{coinsPerUTxOWord}~pp)} \\~ \\ \forall txout \in \txouts{txb},\\ - \hldiff{\fun{serSize}~(\fun{getValue}~txout) ~\leq ~ \fun{maxValSize}~pp} \\~ + \fun{serSize}~(\fun{getValue}~txout) \leq \hldiff{\fun{maxValSize}~pp} \\~ \\ \forall (\wcard\mapsto (a,~\wcard)) \in \txouts{txb}, a \in \AddrBS \Rightarrow \fun{bootstrapAttrsSize}~a \leq 64 \\ \forall (\wcard\mapsto (a,~\wcard)) \in \txouts{txb}, \fun{netId}~a = \NetworkId \\ \forall (a\mapsto\wcard) \in \txwdrls{txb}, \fun{netId}~a = \NetworkId \\ - \hldiff{(\fun{txnetworkid}~\var{txb}~=~\NetworkId) ~\vee~(\fun{txnetworkid}~\var{txb}~=~\Nothing)} + \hldiff{(\fun{txnetworkid}~\var{txb} = \NetworkId) \vee (\fun{txnetworkid}~\var{txb} = \Nothing)} \\~\\ \fun{txsize}~{tx}\leq\fun{maxTxSize}~\var{pp} \\~\\ \hldiff{\fun{totExunits}~{tx} \leq \fun{maxTxExUnits}~{pp}} & \hldiff{\| \fun{collateral}~{tx} \| \leq \fun{maxCollateralInputs}~{pp}} @@ -758,9 +758,8 @@ \subsection{Witnessing} \begin{figure}[htb] \begin{align*} - & \hspace{-0.8cm}\fun{witsVKeyNeeded} \in \UTxO \to \Tx \to (\KeyHashGen\mapsto\VKey) \to + & \hspace{-0.8cm}\fun{witsVKeyNeeded} : \UTxO \to \Tx \to (\KeyHashGen\mapsto\VKey) \to \powerset{\KeyHash} \\ - & \text{required key hashes} \\ & \hspace{-0.8cm}\fun{witsVKeyNeeded}~\var{utxo}~\var{tx}~\var{genDelegs} = \\ & ~~\{ \fun{paymentHK}~a \mid i \mapsto (a, \wcard) \in \var{utxo},~i\in\fun{txinsVKey}~{tx} \cup \hldiff{\fun{collateral}~{tx}} \} \\ \cup & ~~ @@ -771,7 +770,7 @@ \subsection{Witnessing} \cup & ~~\bigcup_{\substack{c \in \txcerts{tx} \\ ~c \in\DCertRegPool}} \fun{poolOwners}~{c} \\ \cup & ~~\hldiff{\fun{reqSignerHashes}~\var{tx}} \nextdef - & \hspace{-1cm}\fun{scriptsNeeded} \in \UTxO \to \TxBody \to \powerset (\ScriptPurpose \times \ScriptHash) \\ + & \hspace{-1cm}\fun{scriptsNeeded} : \UTxO \to \TxBody \to \powerset (\ScriptPurpose \times \ScriptHash) \\ & \hspace{-1cm}\fun{scriptsNeeded}~\var{utxo}~\var{txb} = \\ & ~~\{ (\var{i}, \fun{validatorHash}~a) \mid i\in\fun{txinsScript}~{(\fun{txins~\var{txb}})}~{utxo}, i \mapsto (a, \wcard, \wcard) \in \var{utxo} \} \\ \cup & ~~\{ (\var{a}, \fun{stakeCred_{r}}~\var{a}) \mid a \in \dom (\AddrRWDScr @@ -780,8 +779,8 @@ \subsection{Witnessing} & ~~~~~~\var{c} \in \cwitness{cert} \cap \AddrScr\} \\ \cup & ~~\{ (\var{pid}, \var{pid}) \mid \var{pid} \in \supp~(\fun{mint}~\var{txb}) \} \nextdef - & \hspace{-1cm}\fun{languages} \in \TxWitness \to \powerset{\Language} \\ - & \hspace{-1cm}\fun{languages}~\var{txw}~=~ + & \hspace{-1cm}\fun{languages} : \TxWitness \to \powerset{\Language} \\ + & \hspace{-1cm}\fun{languages}~\var{txw} = \{\fun{language}~s \mid s \in \range (\fun{txscripts}~{txw}) \cap \ScriptPhTwo\} \end{align*} \caption{UTXOW helper functions} @@ -860,17 +859,18 @@ \subsection{Witnessing} \hldiff{\var{inputHashes}\leteq \{ h \mid (\_ \mapsto (a, \_, h)) \in \txins{txb} \restrictdom \var{utxo}, \fun{isTwoPhaseScriptAddress}~{tx}~{a}\}} \\~\\ \hldiff{\forall \var{s} \in \range (\fun{txscripts}~{txw}) \cap \ScriptPhOne, \fun{validateScript}~\var{s}~\var{tx}}\\~\\ - \hldiff{\{ h \mid (\_, h) \in \fun{scriptsNeeded}~\var{utxo}~(\txbody{tx})\} = \dom (\fun{txscripts}~{txw})} \\~\\ + \hldiff{\{ h \mid (\_, h) \in \fun{scriptsNeeded}~\var{utxo}~txb\} = \dom (\fun{txscripts}~{txw})} \\~\\ \hldiff{\var{inputHashes} \subseteq \dom (\fun{txdats}~{txw})} \\~\\ \hldiff{\dom (\fun{txdats}~{txw}) \subseteq \var{inputHashes} \cup \{h~\mid~ (\wcard, \wcard, h)\in\fun{txouts}~{tx}\}} \\~\\ - \hldiff{\ \dom (\fun{txrdmrs}~tx) ~=~\{~\fun{rdptr}~txb~sp~ - \vert~ (sp,h)~\in~\fun{scriptsNeeded}~\var{utxo}~(\txbody{tx}), } \\ - \hldiff{h\mapsto s~\in~\fun{txscripts}~{txw}, s~\in~\ScriptPhTwo \}} + \hldiff{\ \dom (\fun{txrdmrs}~tx) = \{~\fun{rdptr}~txb~sp~ + \vert~ (sp,h) \in \fun{scriptsNeeded}~\var{utxo}~(\txbody{tx}), } \\ + \hldiff{h\mapsto s \in \fun{txscripts}~{txw}, s \in \ScriptPhTwo \}} \\~\\ - \forall \var{vk} \mapsto \sigma \in \txwitsVKey{txw}, + \var{txbodyHash}\leteq\fun{hash}~(\txbody{tx}) \\ + \forall \var{vk} \mapsto \sigma \in \txwitsVKey{tx}, \mathcal{V}_{\var{vk}}{\serialised{txbodyHash}}_{\sigma} \\ - \fun{witsVKeyNeeded}~{utxo}~{tx}~{genDelegs} \subseteq \var{witsKeyHashes} + \fun{witsVKeyNeeded}~{utxo}~{tx}~{genDelegs} \subseteq witsKeyHashes \\~\\ genSig \leteq \left\{ @@ -893,7 +893,7 @@ \subsection{Witnessing} (\var{adh}=\fun{hashAD}~\var{ad}) \\~\\ \hldiff{\fun{languages}~{txw} \subseteq \dom(\fun{costmdls}~tx)} \\ - \hldiff{\fun{scriptIntegrityHash}~{txb}~=~ + \hldiff{\fun{scriptIntegrityHash}~{txb} = \fun{hashScriptIntegrity}~\var{pp}~(\fun{languages}~{txw})~(\fun{txrdmrs}~{txw})~(\fun{txdats}~{txw})} \\~\\ { From 539fdaea2231cd9307154233b455454b297b50ca Mon Sep 17 00:00:00 2001 From: whatisRT Date: Wed, 10 Nov 2021 16:22:48 +0100 Subject: [PATCH 2/2] Small fixes --- eras/alonzo/formal-spec/transactions.tex | 20 +++++++++----------- 1 file changed, 9 insertions(+), 11 deletions(-) diff --git a/eras/alonzo/formal-spec/transactions.tex b/eras/alonzo/formal-spec/transactions.tex index feab8e710db..40304d46ac3 100644 --- a/eras/alonzo/formal-spec/transactions.tex +++ b/eras/alonzo/formal-spec/transactions.tex @@ -257,17 +257,15 @@ \subsection{Transactions} 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. It can be used to re-apply blocks without script re-validation. - This tag cannot be signed, since it is applied by the block producer. + Since this tag is not part of the body, i.e. it is not signed, the block producer can + (and must) choose the correct value. \item any auxiliary data. \end{enumerate} - -Note that unlike in Shelley or ShelleyMA eras, transactions inside blocks and transactions -a user submits are now of different types. A transaction inside a block is composed of -the user-submitted transaction paired with the $\IsValid$ tag, which is -added by the block producer. The user cannot -add their own tag because of how this tag is used in transaction validation, see -Section~\ref{sec:two-phase}. - +\begin{note} + In the implementation the $\IsValid$ tag is part of a user-submitted + transaction, but it is ignored and re-computed by the block + producer. +\end{note} \subsection{Additional Role of Signatures on TxBody} The transaction body and the UTxO must uniquely determine all the data @@ -282,14 +280,14 @@ \subsection{Additional Role of Signatures on TxBody} certificates, minting policies, and reward addresses do not need to be signed. The optional datum objects, however, could be stripped from the transaction without making it invalid. The optional datums are stored in the same map the required ones, so, -for this reason, we do include all datum objects in the witness and PP hash calculation. +for this reason, we do include all datum objects in the script integrity hash calculation. % The hash of the indexed redeemer structure and the protocol parameters that are used by script interpreters are included in the body of the transaction, as these are composed by the transaction author rather than fixed via a hash on the ledger. 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. +arguments to a new script interpreter. \subsection{Data required for script validation.} \label{sec:script-data}