diff --git a/alonzo/formal-spec/chain.tex b/alonzo/formal-spec/chain.tex index 0d05eb2f16..24bfd35966 100644 --- a/alonzo/formal-spec/chain.tex +++ b/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}) \\~\\ diff --git a/alonzo/formal-spec/introduction.tex b/alonzo/formal-spec/introduction.tex index cf5a6c5063..2b621adeb3 100644 --- a/alonzo/formal-spec/introduction.tex +++ b/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. diff --git a/alonzo/formal-spec/properties.tex b/alonzo/formal-spec/properties.tex index d1d8b9eba7..dcd2913d01 100644 --- a/alonzo/formal-spec/properties.tex +++ b/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,7 +187,7 @@ \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 @@ -195,7 +195,7 @@ \section{Formal Properties} 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. diff --git a/alonzo/formal-spec/protocol-parameters.tex b/alonzo/formal-spec/protocol-parameters.tex index 028d91e432..c72581b9d5 100644 --- a/alonzo/formal-spec/protocol-parameters.tex +++ b/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,10 +177,10 @@ \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*} @@ -188,7 +188,8 @@ \subsection{Script Evaluation Cost Model and Prices} \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} diff --git a/alonzo/formal-spec/transactions.tex b/alonzo/formal-spec/transactions.tex index 1d9f86fa89..8bf71f39df 100644 --- a/alonzo/formal-spec/transactions.tex +++ b/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 diff --git a/alonzo/formal-spec/utxo.tex b/alonzo/formal-spec/utxo.tex index 2a0c0c50b7..436e00a47d 100644 --- a/alonzo/formal-spec/utxo.tex +++ b/alonzo/formal-spec/utxo.tex @@ -8,23 +8,26 @@ \section{UTxO} & \fun{isTwoPhaseScriptAddress} \in \Tx \to \Addr \to \Bool \\ & \fun{isTwoPhaseScriptAddress}~tx~a = \\ &\quad\begin{cases} - s \in \ScriptPhTwo & a \in \AddrScr \land \fun{validatorHash}~a \mapsto s \in \fun{txscripts} (\fun{txwits}~tx) \\ + \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}~\var{tx} = \sum_{\wcard \mapsto (\wcard, ~eu) \in \fun{txrdmrs}~(\fun{txwits}~tx)} eu + & \fun{totExUnits} \in \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}~\var{pp}~tx~utxo~= \\ &~~ \minfee{pp}~{tx} \leq \txfee{txb} \wedge (\fun{txrdmrs}~tx \neq \Nothing \Rightarrow \\ - &~~~~~~((\forall (a, \wcard, \_) \in \fun{range}~(\fun{collateral}~{txb} \restrictdom \var{utxo}), \fun{paymentHK}~a \in \AddrVKey) \\ + &~~~~~~((\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~ \fun{collateral}~{tx}~ \neq~\{\}) \\ &~~ \where \\ & ~~~~~~~ \var{txb}~=~\txbody{tx} \\ - & ~~~~~~~ \var{balance}~=~\fun{ubalance}~(\fun{collateral}~{txb} \restrictdom \var{utxo}) \\ + & ~~~~~~~ \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}) \nextdef & \fun{txscriptfee} \in \Prices \to \ExUnits \to \Coin \\ & \fun{txscriptfee}~(pr_{mem}, pr_{steps})~ (\var{mem, steps}) @@ -99,7 +102,7 @@ \subsection{Combining Scripts with Their Inputs} \begin{itemize} \item certificates in the $\DCert$ list are indexed in the order in which they arranged in the (full, unfiltered) list of certificates inside the transaction - \item the index of a reward account $\var{ract}$ in the the reward withdrawals map is + \item the index of a reward account $\var{ract}$ in the reward withdrawals map is the index of $\var{ract}$ as a key in the (unfiltered) map. The keys of the $\Wdrl$ map are arranged in the order defined on the $\RewardAcnt$ type, which is a lexicographical (abbrv. lex) order @@ -157,10 +160,10 @@ \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} \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^? \end{align*} % \emph{Indexing functions} @@ -168,18 +171,19 @@ \subsection{Combining Scripts with Their Inputs} &\fun{indexedRdmrs} \in \Tx \to \ScriptPurpose \to (\Redeemer~\times~\ExUnits)^?\\ &\fun{indexedRdmrs}~tx~sp = \begin{cases} - (d, \var{eu}) & (\fun{rdptr}~txb~sp)~ \mapsto (\var{d}, \var{eu}) \in \fun{txrdmrs}~(\fun{txwits}~{tx}) \} \\ + r & (\fun{rdptr}~txb~sp)~ \mapsto r \in \fun{txrdmrs}~(\fun{txwits}~{tx}) \} \\ \Nothing & \text{otherwise} \end{cases} \\ & ~~\where \\ & ~~\quad \var{txb} = \txbody{tx} \nextdef - &\fun{rdptr} ~\in~\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 + &\fun{rdptr} ~\in~\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 \end{cases} \end{align*} \caption{Indexing script and data objects} @@ -215,7 +219,7 @@ \subsection{Plutus Script Validation} \item $\fun{valContext}$ constructs the \emph{validation context}. A validation context is a $\Data$ term which encodes both the summary of the transaction and ledger information - (this is supplied by the $\fun{txInfo}$ summarization function), and the script purpose. + (this is supplied by the $\fun{txInfo}$ summarizing function), and the script purpose. \item $\fun{runPLCScript}$ validates Plutus scripts. It takes the following @@ -320,12 +324,12 @@ \subsection{Plutus Script Validation} % \begin{align*} &\fun{epochInfoSlotToUTCTime} \in \EpochInfo \to \SystemStart \to \Slot \to \UTCTime^? \\ - &\text{Translate slot number to system time or fail} \\~\\ + &\text{Translate slot number to system time (via consensus) or fail} \\~\\ &\fun{txInfo} \in \Language \to \UTxO \to \Tx \to \TxInfo \\ &\text{Summarizes transaction data} \\~\\ &\fun{valContext} \in \TxInfo \to \ScriptPurpose \to \Data \\ &\text{Pairs transaction data with a script purpose} \\~\\ - &\fun{runPLCScript} \in \ScriptPlutus \to \seqof{\Data} \to \ExUnits \to \CostMod \to + &\fun{runPLCScript} \in \CostMod \to \ScriptPlutus \to \ExUnits \to \seqof{\Data} \to \IsValid \\ &\text{Validate a Plutus script, taking resource limits into account} \end{align*} @@ -347,7 +351,7 @@ \subsection{Plutus Script Validation} \begin{itemize} \item $\fun{getDatum}$ looks for a datum associated with a given script purpose. Note that only an $\TxIn$-type script purpose can result in finding an associated datum hash. - In no datum is found, an empty list is returned. A list containing the found datum + If no datum is found, an empty list is returned. A list containing the found datum is returned otherwise. \item $\fun{collectTwoPhaseScriptInputs}$ builds a list of scripts, paired with their @@ -392,7 +396,7 @@ \subsection{Plutus Script Validation} \begin{figure}[htb] \begin{align*} - & \fun{getDatum} \in \Tx \to \UTxO \to \ScriptPurpose \to \seqof{\Data} \\ + & \fun{getDatum} \in \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) \\ @@ -403,7 +407,7 @@ \subsection{Plutus Script Validation} & ~~~~ \seqof{(\Script \times \seqof{\Data} \times \ExUnits \times \CostMod)} \\ & \fun{collectTwoPhaseScriptInputs} ~\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}~{tx}, \\ + & ~~~~(\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}, \\ @@ -605,7 +609,7 @@ \subsection{The UTXOS transition system} \begin{array}{r} \varUpdate{\var{\fun{collateral}~{txb} \subtractdom \var{utxo}}} \\ \var{deposits} \\ - \varUpdate{\var{fees} + \fun{ubalance}~(\fun{collateral}~{txb}\restrictdom \var{utxo})} \\ + \varUpdate{\var{fees} + \fun{cbalance}~(\fun{collateral}~{txb}\restrictdom \var{utxo})} \\ \var{pup} \\ \end{array} \right) @@ -620,7 +624,7 @@ \subsection{The UTXOS transition system} This rule has the following changes: \begin{enumerate} - \item The transaction pays fees and supplies collateral ada correctly, as defined above; + \item The transaction pays fees and supplies collateral Ada correctly, as defined above; \item The end of the transaction validity interval is translatable into system time (ie. within the consensus's forecast window). This is checked @@ -659,7 +663,7 @@ \subsection{The UTXOS transition system} \var{txb}\leteq\txbody{tx} & \fun{ininterval}~\var{slot}~(\fun{txvldt}~{tx}) & \hldiff{\var{(\wcard, i_f)}\leteq\fun{txvldt}~{tx}} \\~\\ - \hldiff{\fun{txrdmrs}~\var{tx}\neq \Nothing ~\Rightarrow~ \fun{epochInfoSlotToUTCTime}~\mathsf{epochInfo}~\mathsf{systemTime}~i_f \neq \Nothing} \\ + \hldiff{\Nothing \notin \{\fun{txrdmrs}~\var{tx}, i_f\} ~\Rightarrow~ \fun{epochInfoSlotToUTCTime}~\mathsf{epochInfo}~\mathsf{systemTime}~i_f \neq \Nothing} \\ \txins{txb} \neq \emptyset & \hldiff{\fun{feesOK}~pp~tx~utxo} & \txins{txb}~\cup~\fun{collateral}~{txb}~ \subseteq~ \dom \var{utxo} @@ -680,7 +684,7 @@ \subsection{The UTXOS transition system} \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{maxCollInputs}~{pp}} + \hldiff{\fun{totExunits}~{tx} \leq \fun{maxTxExUnits}~{pp}} & \hldiff{\| \fun{collateral}~{tx} \| \leq \fun{maxCollateralInputs}~{pp}} \\ ~ \\ @@ -776,27 +780,23 @@ \subsection{Witnessing} \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} \} \\ + & ~~\{ \fun{paymentHK}~a \mid i \mapsto (a, \wcard) \in \var{utxo},~i\in\fun{txinsVKey}~{tx} \cup \hldiff{\fun{collateral}~{tx}} \} \\ \cup & ~~ \{\fun{stakeCred_r}~a\mid a\mapsto \wcard \in \AddrRWDVKey \restrictdom \txwdrls{tx}\}\\ \cup & ~~(\AddrVKey \cap \fun{certWitsNeeded}~{tx}) \\ \cup & ~~\fun{propWits}~(\fun{txup}~\var{tx})~\var{genDelegs} \\ \cup & ~~\bigcup_{\substack{c \in \txcerts{tx} \\ ~c \in\DCertRegPool}} \fun{poolOwners}~{c} \\ - \cup & ~~\hldiff{\{ \fun{paymentHK}~a \mid i \mapsto (a, \wcard) \in \var{utxo},~i\in\fun{collateral}~{tx} \}} \\ \cup & ~~\hldiff{\fun{reqSignerHashes}~\var{tx}} \nextdef - & \hspace{-1cm}\fun{scriptsNeeded} \in \UTxO \to \Tx \to \powerset (\ScriptPurpose \times \ScriptHash) \\ - & \hspace{-1cm}\fun{scriptsNeeded}~\var{utxo}~\var{tx} = \\ - & ~~\{ (\var{i}, \fun{validatorHash}~a) \mid i \mapsto (a, \wcard, \wcard) \in \var{utxo}, - i\in\fun{txinsScript}~{(\fun{txins~\var{txb}})}~{utxo}\} \\ + & \hspace{-1cm}\fun{scriptsNeeded} \in \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 \restrictdom \fun{txwdrls}~\var{txb}) \} \\ - \cup & ~~\{ (\var{cert}, \var{c}) \mid \var{cert} \in (\DCertDeleg \cup \DCertDeRegKey)\cap\fun{txcerts}~(\txbody{tx}), \\ + \cup & ~~\{ (\var{cert}, \var{c}) \mid \var{cert} \in (\DCertDeleg \cup \DCertDeRegKey)\cap\fun{txcerts}~txb, \\ & ~~~~~~\var{c} \in \cwitness{cert} \cap \AddrScr\} \\ - \cup & ~~\{ (\var{pid}, \var{pid}) \mid \var{pid} \in \supp~(\fun{mint}~\var{txb}) \} \\ - & \where \\ - & ~~~~~~~ \var{txb}~=~\txbody{tx} + \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}~=~ @@ -878,12 +878,12 @@ \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}~\var{tx}\} = \dom (\fun{txscripts}~{txw})} \\~\\ + \hldiff{\{ h \mid (\_, h) \in \fun{scriptsNeeded}~\var{utxo}~(\txbody{tx})\} = \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}\}} + \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}~\var{tx}, } \\ + \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}, @@ -910,7 +910,9 @@ \subsection{Witnessing} \lor (\var{adh}=\fun{hashAD}~\var{ad}) \\~\\ - \hldiff{\fun{scriptIntegrityHash}~{txb}~=~\fun{hashScriptIntegrity}~\var{pp}~(\fun{languages}~{txw})~(\fun{txrdmrs}~{txw})~(\fun{txdats}~{txw})} + \hldiff{\fun{languages}~{txw} \subseteq \dom(\fun{costmdls}~tx)} \\ + \hldiff{\fun{scriptIntegrityHash}~{txb}~=~ + \fun{hashScriptIntegrity}~\var{pp}~(\fun{languages}~{txw})~(\fun{txrdmrs}~{txw})~(\fun{txdats}~{txw})} \\~\\ { \begin{array}{r} diff --git a/shelley-ma/formal-spec/utxo.tex b/shelley-ma/formal-spec/utxo.tex index 80c0161d5e..b156f26f89 100644 --- a/shelley-ma/formal-spec/utxo.tex +++ b/shelley-ma/formal-spec/utxo.tex @@ -178,7 +178,7 @@ \subsection*{The UTXO Transition Rule} \\ \hldiff{\forall txout \in \txouts{txb},} \\ \hldiff{\fun{serSize}~(\fun{getValue}~txout) ~\leq ~\mathsf{MaxValSize}} \\~\\ - \forall (\wcard\mapsto (a,~\wcard)) \in \txouts{txb}, a \in \AddrBS \to \fun{bootstrapAttrsSize}~a \leq 64 + \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 \\ diff --git a/shelley/chain-and-ledger/formal-spec/chain.tex b/shelley/chain-and-ledger/formal-spec/chain.tex index e7ebb91e79..c7269e93b9 100644 --- a/shelley/chain-and-ledger/formal-spec/chain.tex +++ b/shelley/chain-and-ledger/formal-spec/chain.tex @@ -1559,7 +1559,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}) \\~\\ diff --git a/shelley/chain-and-ledger/formal-spec/utxo.tex b/shelley/chain-and-ledger/formal-spec/utxo.tex index 06ec389dc1..843eb16149 100644 --- a/shelley/chain-and-ledger/formal-spec/utxo.tex +++ b/shelley/chain-and-ledger/formal-spec/utxo.tex @@ -292,7 +292,7 @@ \subsection{UTxO Transitions} \\ \forall (\wcard\mapsto (\wcard,~c)) \in \txouts{txb}, c \geq (\fun{minUTxOValue}~\var{pp}) \\ - \forall (\wcard\mapsto (a,~\wcard)) \in \txouts{txb}, a \in \AddrBS \to \fun{bootstrapAttrsSize}~a \leq 64 + \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 \\