diff --git a/shelley/chain-and-ledger/formal-spec/chain.tex b/shelley/chain-and-ledger/formal-spec/chain.tex index f288a8dec96..bd5e8617971 100644 --- a/shelley/chain-and-ledger/formal-spec/chain.tex +++ b/shelley/chain-and-ledger/formal-spec/chain.tex @@ -288,6 +288,7 @@ \subsection{MIR Transition} \var{acnt} \\ \var{ss} \\ (\var{us},~(\var{ds},~\var{ps})) \\ + \var{prevPP} \\ \var{pp} \\ \end{array}\right)} \trans{mir}{} @@ -295,6 +296,7 @@ \subsection{MIR Transition} \varUpdate{\var{acnt'}} \\ \var{ss} \\ (\var{us},~(\varUpdate{\var{ds'}},~\var{ps})) \\ + \var{prevPP} \\ \var{pp} \\ \end{array}\right)} } @@ -326,6 +328,7 @@ \subsection{MIR Transition} \var{acnt} \\ \var{ss} \\ (\var{us},~(\var{ds},~\var{ps})) \\ + \var{prevPP} \\ \var{pp} \\ \end{array}\right)} \trans{mir}{} @@ -333,6 +336,7 @@ \subsection{MIR Transition} \var{acnt} \\ \var{ss} \\ (\var{us},~(\varUpdate{\var{ds'}},~\var{ps})) \\ + \var{prevPP} \\ \var{pp} \\ \end{array}\right)} } @@ -481,7 +485,7 @@ \subsection{New Epoch Transition} } \\~\\ {\begin{array}{r@{~\leteq~}l} - (\var{acnt},~\var{ss},~\var{ls}, \var{pp}) & \var{es'''} \\ + (\var{acnt},~\var{ss},~\var{ls},~\wcard,~\var{pp}) & \var{es'''} \\ (\wcard,~\var{pstake_{set}},~\wcard,~\wcard) & \var{ss} \\ (\var{stake},~\var{delegs},~\var{poolPrms}) & \var{pstake_{set}} \\ total & \sum_{\_ \mapsto c\in\var{stake}} c \\ @@ -1704,7 +1708,7 @@ \subsection{Chain Transition} \leteq\var{nes} \\ (\var{e_2},~\wcard,~\var{b_{cur}},~\var{es},~\wcard,~\var{pd},\var{osched}) \leteq\var{nes'} \\ - (\var{acnt},~\wcard,\var{ls},~\var{pp'})\leteq\var{es}\\ + (\var{acnt},~\wcard,\var{ls},~\wcard,~\var{pp'})\leteq\var{es}\\ ( \wcard, ( (\wcard,~\wcard,~\wcard,~\wcard,~\wcard,~\var{genDelegs}),~ (\wcard,~\wcard,~\wcard)))\leteq\var{ls}\\ @@ -1826,7 +1830,8 @@ \subsection{Byron to Shelley Transition} \begin{align*} & \fun{initialShelleyState} \in \Slot \to \BlockNo \to \Epoch \to\HashHeader \to \UTxO \to \Coin \\ - & ~~~ \to (\KeyHashGen \mapsto \KeyHash) \to (\Slot\mapsto\KeyHashGen^?) \to \Applications \to \PParams \to \ChainState \\ + & ~~~ \to (\KeyHashGen \mapsto \KeyHash) \to (\Slot\mapsto\KeyHashGen^?) + \to \PParams \to \ChainState \\ & \fun{initialShelleyState}~ \left( \begin{array}{c} @@ -1838,7 +1843,6 @@ \subsection{Byron to Shelley Transition} \var{reserves} \\ \var{genDelegs} \\ \var{os} \\ - \var{apps} \\ \var{pp} \\ \end{array} \right) @@ -1875,14 +1879,7 @@ \subsection{Byron to Shelley Transition} \var{utxo} \\ 0 \\ 0 \\ - \left( - \begin{array}{c} - \emptyset \\ - \emptyset \\ - \emptyset \\ - \var{apps}\\ - \end{array} - \right) \\ + \emptyset \\ \end{array} \right) \\ \left( @@ -1909,6 +1906,7 @@ \subsection{Byron to Shelley Transition} \end{array} \right) \\ \var{pp} \\ + \var{pp} \\ \end{array} \right) \\ \\ @@ -1941,7 +1939,7 @@ \subsection{Byron to Shelley Transition} \emph{Byron to Shelley Transition} % \begin{align*} - & \fun{toShelley} \in \CEState \to \ChainState \\ + & \fun{toShelley} \in \CEState \to \BlockNo \to \ChainState \\ & \fun{toShelley}~ \left( \begin{array}{c} @@ -1952,7 +1950,7 @@ \subsection{Byron to Shelley Transition} \var{ds} \\ \var{us} \end{array} - \right) + \right)~\var{bn} = \fun{initialShelleyState}~ \left( @@ -1965,13 +1963,11 @@ \subsection{Byron to Shelley Transition} \var{reserves} \\ \var{gd} \\ \overlaySchedule{e}{(\dom{gd})}{pp} \\ - \fun{avs}~\var{us} \\ \var{pp} \\ \end{array} \right) \\ & ~~~~\where \\ & ~~~~~~~~~e = \epoch{s_{last}} \\ - & ~~~~~~~~~bn = \mathsf{TODO} \\ & ~~~~~~~~~gd = \fun{dms}~\var{ds} \\ & ~~~~~~~~~pp = \pps{us} \\ \end{align*} diff --git a/shelley/chain-and-ledger/formal-spec/epoch.tex b/shelley/chain-and-ledger/formal-spec/epoch.tex index e472d32d58b..9dbbf3b8c98 100644 --- a/shelley/chain-and-ledger/formal-spec/epoch.tex +++ b/shelley/chain-and-ledger/formal-spec/epoch.tex @@ -436,7 +436,7 @@ \subsection{Snapshot Transition} \var{utxo} \\ \var{deposits} \\ \var{fees} \\ - \var{up} \\ + \var{pup} \\ \end{array} \right) \trans{snap}{e} @@ -450,7 +450,7 @@ \subsection{Snapshot Transition} \var{utxo} \\ \varUpdate{\var{oblg}} \\ \varUpdate{\var{fees} + \var{decayed}} \\ - \var{up} \\ + \var{pup} \\ \end{array} \right) } @@ -804,6 +804,12 @@ \subsection{Complete Epoch Boundary Transition} The transition has no evironment. The state is made up of the the accounting state, the snapshots, the ledger state and the protocol parameters. +The transition uses a helper function $\fun{votedValue}$ which returns +the consensus value of update proposals in the event that consensus it met. +\textbf{Note that} $\fun{votedValue}$ +\textbf{is only well-defined if } $\Quorum$ +\textbf{is greater than half the number of core nodes, i.e.} +$\Quorum > |\var{genDelegs}|/2$ \textbf{.} %% %% Figure - Epoch Defs @@ -817,6 +823,7 @@ \subsection{Complete Epoch Boundary Transition} \var{acnt} & \Acnt & \text{accounting}\\ \var{ss} & \Snapshots & \text{snapshots}\\ \var{ls} & \LState & \text{ledger state}\\ + \var{prevPp} & \PParams & \text{previous protocol parameters}\\ \var{pp} & \PParams & \text{protocol parameters}\\ \end{array} \right) @@ -837,13 +844,25 @@ \subsection{Complete Epoch Boundary Transition} \end{array} \end{equation*} % + \emph{Helper Functions} + \begin{align*} + & \fun{votedValue} \in (\KeyHashGen\mapsto\PParamsUpdate) \to \PParamsUpdate^?\\ + & \fun{votedValue}~\var{vs} = + \begin{cases} + p & \exists p\in\range{vs}~(|vs\restrictrange p|\geq \Quorum) \\ + \Nothing & \text{otherwise} \\ + \end{cases} + \end{align*} + % \caption{Epoch transition-system types} \label{fig:ts-types:epoch} \end{figure} The epoch transition rule calls $\mathsf{SNAP}$, $\mathsf{POOLREAP}$ and $\mathsf{NEWPP}$ -in sequence. +in sequence. It also store the previous protocol parameters in $\var{prevPp}$. +The previous protocol parameters will be used for the reward calculation in the upcoming epoch, +note that they correspond to the epoch for which the reward are being calculated. The ordering of these rules is important. The stake pools which will be reaped during the $\mathsf{POOLREAP}$ transition must still be a part of the new snapshot, and so $\mathsf{SNAP}$ must occur before $\mathsf{POOLREAP}$. @@ -913,9 +932,9 @@ \subsection{Complete Epoch Boundary Transition} } \right) \\~\\~\\ - \var{(\wcard,~\wcard,~\wcard,~(\var{ppup},~\wcard,~\wcard,~\wcard))}\leteq\var{utxoSt'}\\ + \var{(\wcard,~\wcard,~\wcard,~\var{pup})}\leteq\var{utxoSt'}\\ \var{pp_{new}}\leteq\var{pp}\unionoverrideRight - \fun{votedValue_{(\Ppm\to\mathsf{T_{ppm}})}}~\var{ppup}\\ + \fun{votedValue}~\var{pup}\\ { \begin{array}{r} \var{pp_{new}}\\ @@ -953,6 +972,7 @@ \subsection{Complete Epoch Boundary Transition} \var{acnt} \\ \var{ss} \\ \var{ls} \\ + \var{prevPp} \\ \var{pp} \\ \end{array} \right) @@ -962,6 +982,7 @@ \subsection{Complete Epoch Boundary Transition} \varUpdate{\var{acnt''}} \\ \varUpdate{\var{ss'}} \\ \varUpdate{\var{ls'}} \\ + \varUpdate{\var{pp}} \\ \varUpdate{\var{pp'}} \\ \end{array} \right) @@ -1290,6 +1311,9 @@ \subsection{Reward Update Calculation} The $\fun{createRUpd}$ function does the following: \begin{itemize} + \item Note that for all the calculations below, we use the previous protocol parameters + $\var{prevPp}$, which correspondings the the parameters during the epoch for which we + are being created for. \item First we calculate the change to the reserves, as determined by the $\rho$ protocol parameter. \item Next we calculate $\var{rewardPot}$, the total amount of coin available for rewards this @@ -1339,7 +1363,7 @@ \subsection{Reward Update Calculation} & \createRUpd{b}{es}{total} = \left( \Delta t_1+\Delta t_2,-~\Delta r,~\var{rs},~-\var{feeSS}\right) \\ & ~~~\where \\ - & ~~~~~~~(\var{acnt},~\var{ss},~\var{ls},~\var{pp}) = \var{es} \\ + & ~~~~~~~(\var{acnt},~\var{ss},~\var{ls},~\var{prevPp},~\wcard) = \var{es} \\ & ~~~~~~~(\wcard,~\wcard,~\var{pstake_{go}},~\var{poolsSS},~\var{feeSS}) = \var{ss}\\ & ~~~~~~~(\var{stake},~\var{delegs}) = \var{pstate_{go}} \\ & ~~~~~~~(\wcard,~\var{reserves}) = \var{acnt} \\ @@ -1350,15 +1374,15 @@ \subsection{Reward Update Calculation} \wcard \right) \right) = \var{ls} \\ - & ~~~~~~~\Delta r = \floor*{\min(1,\eta) \cdot (\fun{rho}~{pp}) \cdot + & ~~~~~~~\Delta r = \floor*{\min(1,\eta) \cdot (\fun{rho}~\var{prevPp}) \cdot \var{reserves}} \\ - & ~~~~~~~\eta = \frac{blocksMade}{\SlotsPerEpoch \cdot \fun{activeSlotCoeff}~{pp}} \\ + & ~~~~~~~\eta = \frac{blocksMade}{\SlotsPerEpoch \cdot \fun{activeSlotCoeff}~\var{prevPp}} \\ & ~~~~~~~\var{rewardPot} = \var{feeSS} + \Delta r \\ - & ~~~~~~~\Delta t_1 = \floor*{(\fun{tau}~{pp}) \cdot \var{rewardPot}} \\ + & ~~~~~~~\Delta t_1 = \floor*{(\fun{tau}~\var{prevPp}) \cdot \var{rewardPot}} \\ & ~~~~~~~\var{R} = \var{rewardPot} - \Delta t_1 \\ & ~~~~~~~\var{rs} - = \reward{pp}{b}{R}{(\dom{rewards})}{poolsSS}{stake}{delegs}{total} \\ + = \reward{prevPp}{b}{R}{(\dom{rewards})}{poolsSS}{stake}{delegs}{total} \\ & ~~~~~~~\Delta t_{2} = R - \left(\sum\limits_{\_\mapsto c\in\var{rs}}c\right) \\ & ~~~~~~~blocksMade = \sum_{\wcard \mapsto m \in b}m \end{align*} @@ -1402,6 +1426,7 @@ \subsection{Reward Update Calculation} \var{fees} \\ \var{up} \\ ~ \\ + \var{prevPp} \\ \var{pp} \\ \end{array} \right) @@ -1427,6 +1452,7 @@ \subsection{Reward Update Calculation} \varUpdate{\var{fees}+\Delta f} \\ \var{up} \\ ~ \\ + \var{prevPp} \\ \var{pp} \\ \end{array} \right) diff --git a/shelley/chain-and-ledger/formal-spec/ledger-spec.tex b/shelley/chain-and-ledger/formal-spec/ledger-spec.tex index 0a9c335a32f..821043a5412 100644 --- a/shelley/chain-and-ledger/formal-spec/ledger-spec.tex +++ b/shelley/chain-and-ledger/formal-spec/ledger-spec.tex @@ -72,6 +72,8 @@ \newcommand{\Wdrl}{\type{Wdrl}} \newcommand{\Coin}{\type{Coin}} \newcommand{\PParams}{\type{PParams}} +\newcommand{\PParamsUpdate}{\type{PParamsUpdate}} +\newcommand{\ProposedPPUpdates}{\type{ProposedPPUpdates}} \newcommand{\Slot}{\type{Slot}} \newcommand{\SlotsPrior}{\ensuremath{\mathsf{SlotsPrior}}} \newcommand{\SlotsPerEpoch}{\mathsf{SlotsPerEpoch}} @@ -89,17 +91,10 @@ \newcommand{\seedOp}{\star} \newcommand{\Ppm}{\type{Ppm}} \newcommand{\ProtVer}{\ensuremath{\type{ProtVer}}} -\newcommand{\ApName}{\ensuremath{\type{ApName}}} -\newcommand{\ApVer}{\ensuremath{\type{ApVer}}} -\newcommand{\SystemTag}{\ensuremath{\type{SystemTag}}} -\newcommand{\InstallerHash}{\ensuremath{\type{InstallerHash}}} \newcommand{\MetaDatum}{\ensuremath{\type{MetaDatum}}} \newcommand{\MetaData}{\ensuremath{\type{MetaData}}} \newcommand{\MetaDataHash}{\ensuremath{\type{MetaDataHash}}} -\newcommand{\Metadata}{\ensuremath{\type{Mdt}}} \newcommand{\PPUpdate}{\type{PPUpdate}} -\newcommand{\Applications}{\type{Applications}} -\newcommand{\AVUpdate}{\type{AVUpdate}} \newcommand{\Update}{\type{Update}} \newcommand{\DCert}{\type{DCert}} @@ -181,10 +176,6 @@ \newcommand{\Block}{\type{Block}} \newcommand{\SlotId}{\type{SlotId}} \newcommand{\PPUpdateEnv}{\type{PPUpdateEnv}} -\newcommand{\AVUpdateEnv}{\type{AVUpdateEnv}} -\newcommand{\AVUpdateState}{\type{AVUpdateState}} -\newcommand{\UpdateEnv}{\type{UpdateEnv}} -\newcommand{\UpdateState}{\type{UpdateState}} \newcommand{\UTxOEnv}{\type{UTxOEnv}} \newcommand{\CEEnv}{\type{CEEnv}} \newcommand{\CEState}{\type{CEState}} diff --git a/shelley/chain-and-ledger/formal-spec/protocol-parameters.tex b/shelley/chain-and-ledger/formal-spec/protocol-parameters.tex index 55c09d96799..cbfff71c602 100644 --- a/shelley/chain-and-ledger/formal-spec/protocol-parameters.tex +++ b/shelley/chain-and-ledger/formal-spec/protocol-parameters.tex @@ -12,6 +12,9 @@ \section{Protocol Parameters} indexed by their names. We will explain the significance of each parameter as it comes up in the calculations used in transition rules. +The type $\PParamsUpdate$ is similar to $\PParams$, but is +a partial mapping of the protocol parameters. It is used in the update +system explained in Section~\ref{sec:update}. The type $\Coin$ is defined as an alias for the integers. Negative values will not be allowed in UTxO outputs or reward accounts, @@ -76,8 +79,13 @@ \section{Protocol Parameters} \begin{array}{r@{~\in~}l@{\qquad=\qquad}lr} \var{pp} & \PParams + & \Ppm \to \mathsf{T_{ppm}} + & \text{protocol parameters} + \\ + \var{ppup} + & \PParamsUpdate & \Ppm \mapsto \mathsf{T_{ppm}} - & \text{protocol parameter map} + & \text{protocol parameter update} \\ \var{coin} & \Coin diff --git a/shelley/chain-and-ledger/formal-spec/rules.dot b/shelley/chain-and-ledger/formal-spec/rules.dot index dd899533d66..064a79d8de8 100644 --- a/shelley/chain-and-ledger/formal-spec/rules.dot +++ b/shelley/chain-and-ledger/formal-spec/rules.dot @@ -8,10 +8,7 @@ digraph STS { UTXOW -> UTXO UTXOW -> DELEGS [style=dotted] - UTXO -> UP - - UP -> PPUP - UP -> AVUP + UTXO -> PPUP DELEGS -> DELPL DELEGS -> DELEGS diff --git a/shelley/chain-and-ledger/formal-spec/rules.pdf b/shelley/chain-and-ledger/formal-spec/rules.pdf index 458f6583a22..6fb1475e5b6 100644 Binary files a/shelley/chain-and-ledger/formal-spec/rules.pdf and b/shelley/chain-and-ledger/formal-spec/rules.pdf differ diff --git a/shelley/chain-and-ledger/formal-spec/software-updates.tex b/shelley/chain-and-ledger/formal-spec/software-updates.tex index 1b302b13af7..8c311ebf68c 100644 --- a/shelley/chain-and-ledger/formal-spec/software-updates.tex +++ b/shelley/chain-and-ledger/formal-spec/software-updates.tex @@ -1,61 +1,25 @@ \section{Software Updates} \label{sec:software-updates} - -The distinction between protocol parameter and application updates is as -follows: \newline - -\noindent \textbf{Protocol parameters} -\begin{itemize} - \item All parameters excluding $\ProtVer$: constants -currently used in ledger calculations performed according to the rules described -in this document -\begin{itemize} -\item[$\circ$] Updated only at epoch boundary -\item[$\circ$] All nodes automatically adopt new values (this mechanism is an explicit - part of the ledger rules, and is included in the epoch boundary transition) -\item[$\circ$] Has no effect on the logic of the ledger transition rules -\end{itemize} -\item Protocol version parameter ($\ProtVer$): a special value which -corresponds to a specific version of the \textit{ledger rules} -\begin{itemize} -\item[$\circ$] I.e. if $\var{pv}$ changes, this document may have to be updated with -the new rules and types if there is a change in the logic -\item[$\circ$] E.g. the change may be that the new rules now allow \textit{all} nodes -to vote on update proposals -\item[$\circ$] Whether the $\var{pv}$ must change with any change of protocol -parameters when the \textit{rules do not change} is to be decided -\item[$\circ$] Mechanism for updating is inherited from the general protocol -parameter update and voting rules -\item[$\circ$] If there is a change in transition rules, nodes must have +Updates to the software will include increasing the protocol version. +An increase in the major version indicates a hard fork, and the minor version a soft fork +(meaning old software can validate but not produce new blocks). + +The current protocol version ($\ProtVer$) is a member of the protocol parameters. +It represents a specific version of the \textit{ledger rules}. +If $\var{pv}$ changes, this document may have to be updated with +the new rules and types if there is a change in the logic. +If there is a change in the transition rules, nodes must have software installed that can implement these rules at the epoch boundary -when the protocol parameter adoption occurs -\item[$\circ$] Switching to using these new rules is mandatory in the sense that +when the protocol parameter adoption occurs. +Switching to using these new rules is mandatory in the sense that if the nodes do not have the applications implementing them, this -will prevent a user from reading and -writing to the ledger -\end{itemize} -\end{itemize} -\textbf{Applications} The version of the software the nodes run, -as well as the related system tags and metadata -\begin{itemize} -\item[$\circ$] We cannot force the users to actually upgrade their software -\item[$\circ$] Any application version that is capable of implementing the protocol version -currently on the ledger can be used by a node -\item[$\circ$] Users can update applications as soon as update is agreed upon, and should -do so before their current application becomes incompatible with the -current protocol version (due to the update), however -\item[$\circ$] A voted on application version update has a recommended adoption date, -which applications will automatically follow -\end{itemize} +will prevent a user from reading and writing to the ledger. Applications must sometimes support \textit{several different versions} -of ledger rules in order to accommodate the timely switch of the $\ProtVer$ at the -epoch boundary. Usually, the currently accepted protocol version, and next the -version they are ready to upgrade to (that their application versions can -implement). -The newest protocol version a node is ready to use is included in the block -header of the blocks it produces, see \ref{sec:defs-blocks}. This is either +of ledger rules in order to accommodate the timely switch of the $\ProtVer$ at the epoch boundary. +In this situation, the newest protocol version a node is ready to use is included in the block +header of the blocks it produces, see \ref{sec:defs-blocks}. This is either: \begin{itemize} \item the current version (if there is no protocol version update pending or the node @@ -66,36 +30,14 @@ \section{Software Updates} ledger has not been updated yet). \end{itemize} -So, users have some agency in the process of adoption of +Stake pools have some agency in the process of adoption of new protocol versions. They may refuse to download and install updates. Since software updates cannot be \textit{forced} on the users, if the majority of -users do not perform an update which allows to switch to the next $\ProtVer$, +users do not perform an update which allows the switch to the next $\ProtVer$, it cannot happen. -There is no data in blocks or transactions that says what application -versions a user has, or what protocol version they are using (this always has to -be the version recorded on the ledger). -Having the wrong version of an application -may potentially become problematic (when it is not able to follow the current -ledger rules dictated by $\ProtVer$), however, the update mechanism implemented -in the node software should -ensure this does not happen often. -The process of upgrading the system a new version consists of: - -\begin{enumerate} - \item New software is ready for downloading. - \item The core nodes propose changing - the application version to this - new software. The the voting and proposal of application version updates is discussed - in Section \ref{sec:update}. - \item If there is concensus, this application version becomes the current application version, - see Section \ref{sec:ledger-trans}. - \item All nodes see a new application version on the ledger and update their - software. -\end{enumerate} - -Note that if there is a \textit{new protocol version} implemented by this new -software, the core nodes monitor how many nodes are ready to use the new +Note that if there is a \textit{new protocol version} implemented by new +software, the core nodes can monitor how many nodes are ready to use the new protocol version via the block headers. Once enough nodes are ready for the new protocol version, this may now be updated as well (by the mechanism in described in diff --git a/shelley/chain-and-ledger/formal-spec/transactions.tex b/shelley/chain-and-ledger/formal-spec/transactions.tex index 5b9d45db504..f0116d55a41 100644 --- a/shelley/chain-and-ledger/formal-spec/transactions.tex +++ b/shelley/chain-and-ledger/formal-spec/transactions.tex @@ -21,7 +21,7 @@ \section{Transactions} that error messages can be precise about why a transaction is invalid. For reward calculation rules, see Section \ref{sec:reward-overview}, and for the rule for collecting rewards, see Section \ref{sec:utxo-trans}. - \item Update proposals for protocol parameters and software. + \item An optional update proposals for the protocol parameters. The update system will be explained in Section \ref{sec:update}. \item An optional metadata hash. \end{itemize} @@ -54,9 +54,6 @@ \section{Transactions} \var{gkey} & \VKeyGen & \text{genesis public keys}\\ \var{gkh} & \KeyHashGen & \text{genesis key hash}\\ \var{txid} & \TxId & \text{transaction id}\\ - \var{an} & \ApName & \text{application name}\\ - \var{st} & \SystemTag & \text{system tag}\\ - \var{ih} & \InstallerHash & \text{update data}\\ \var{m} & \MetaDatum & \text{metadatum}\\ \var{mdh} & \MetaDataHash & \text{hash of transaction metadata}\\ \end{array} @@ -96,33 +93,13 @@ \section{Transactions} \begin{equation*} \begin{array}{r@{~\in~}l@{\qquad=\qquad}lr} \var{pup} - & \PPUpdate - & \KeyHashGen \mapsto \Ppm \mapsto \mathsf{T_{ppm}} - & \text{protocol parameter update} - \\ - \var{av} - & \ApVer - & \N - & \text{application versions} - \\ - \var{md} - & \Metadata - & \SystemTag\mapsto\InstallerHash - & \text{application metadata} - \\ - \var{apps} - & \Applications - & \ApName \mapsto (\ApVer \times \Metadata) - & \text{application versions} - \\ - \var{aup} - & \AVUpdate - & \KeyHashGen \mapsto \Applications - & \text{application update} + & \ProposedPPUpdates + & \KeyHashGen \mapsto \PPUpdate + & \text{proposed updates} \\ \var{up} & \Update - & \PPUpdate \times \AVUpdate \times \Epoch^? + & \ProposedPPUpdates \times \Epoch & \text{update proposal} \end{array} \end{equation*} @@ -136,7 +113,7 @@ \section{Transactions} & \begin{array}{l} \powerset{\TxIn} \times (\Ix \mapsto \TxOut) \times \seqof{\DCert} \times \Coin \times \Slot \times \Wdrl - \\ ~~~~\times \Update \times \MetaDataHash^? + \\ ~~~~\times \Update^? \times \MetaDataHash^? \end{array} \\ \var{wit} & \TxWitness & (\VKey \mapsto \Sig) \times (\HashScr \mapsto \Script) @@ -159,8 +136,8 @@ \section{Transactions} \fun{txbody} & \Tx \to \TxBody & \text{transaction body}\\ \fun{txwitsVKey} & \Tx \to (\VKey \mapsto \Sig) & \text{VKey witnesses} \\ \fun{txwitsScript} & \Tx \to (\HashScr \mapsto \Script) & \text{script witnesses}\\ - \fun{txup} & \Tx \to \Update & \text{protocol parameter update}\\ - \fun{txMD} & \Tx \to \MetaData & \text{metadata}\\ + \fun{txup} & \Tx \to \Update^? & \text{protocol parameter update}\\ + \fun{txMD} & \Tx \to \MetaData^? & \text{metadata}\\ \fun{txMDhash} & \Tx \to \MetaDataHash & \text{metadata hash}\\ \end{array} \end{equation*} diff --git a/shelley/chain-and-ledger/formal-spec/update.tex b/shelley/chain-and-ledger/formal-spec/update.tex index c790e478c87..fdfda247ccc 100644 --- a/shelley/chain-and-ledger/formal-spec/update.tex +++ b/shelley/chain-and-ledger/formal-spec/update.tex @@ -4,22 +4,19 @@ \section{Update Proposal Mechanism} The $\mathsf{UPDATE}$ transition is responsible for the federated governance model in Shelley. The governance process includes a mechanism for core nodes to propose and vote on -updates. In this chapter we -outline rules for genesis keys \textit{proposing} both protocol parameter -and application version updates, as well as voting on whether a particular -software update is an acceptable future option. +protocol parameter updates. In this chapter we +outline rules for genesis keys \textit{proposing} protocol parameter updates. For rules regarding the \textit{adoption} of protocol -parameter updates, see Section~\ref{sec:pparam-update}. For rules regarding -adoption of new software versions see \ref{sec:software-updates}. +parameter updates, see Section~\ref{sec:pparam-update}. This chapter does not discuss authentication of update proposals. The signature for the keys in the proposal will be checked in the $\mathsf{UTXOW}$ transition, which checks all the necessary witnesses for a transaction, see Section\ref{sec:witnesses-shelley}. -\textbf{Genesis Key Delegations.} The environment for both protocol parameter -and application version updates contains -the value $\var{genDelegs}$, which is a finite map indexed by genesis key hashes. +\textbf{Genesis Key Delegations.} The environment for the protocol parameter +update transition contains the value $\var{genDelegs}$, +which is a finite map indexed by genesis key hashes. This is the genesis key delegations. During the Byron era, they are all already delegated to some $\KeyHash$, and these delegations are inherited through the Byron-Shelley transition (see Section~\ref{sec:byron-to-shelley}). @@ -27,32 +24,11 @@ \section{Update Proposal Mechanism} but there is no mechanism for them to un-delegate or for the keys to which they delegate to retire (unlike regular stake pools). -Because the protocol parameter and application version update mechanisms are different, the -update proposals for these are handled by separate sets of rules. The main -difference is that the current application version on the ledger is updated -several slots ($\SlotsPrior$-slots) after concensus is reached, whereas protocol -parameter updates must happen at an epoch boundary. -For transparency in both voting mechanisms, the votes and proposals for updates -are stored -on the ledger in addition to the currently accepted protocol parameters and -application versions. - -\subsection{Descriptions of the Data} -\label{sec:update-types} - -The types were defined in Figure~\ref{fig:defs:utxo-shelley}. -In the derived types, $\Metadata$ and $\Applications$ are values -that contain versions of current and next versions of applications. -The $\ApName$ uniquely identifies a specific kind of application (e.g. -the wallet), and the associated $\ApVer$ is the specific version of that -application. The associated $\Metadata$ value gives the \textit{next possible} -versions of the given application. It is a mapping of system tags to hashes of -installer binaries, and is needed for the update mechanism. -The update proposal type $\Update$ is a pair of $\PPUpdate$ and $\AVUpdate$. -$\PPUpdate$ allows for changing protocol parameters, -and $\AVUpdate$ allows for updating the software versions. - -Note that both of these finite maps are indexed by the hashes of the keys of +The types $\ProposedPPUpdates$ and $\Update$ were defined in +Figure~\ref{fig:defs:utxo-shelley}. +The update proposal type $\Update$ is a pair of $\ProposedPPUpdates$ and $\Epoch$. +The epoch in the update specifies the epoch in which the proposal is valid. +$\ProposedPPUpdates$ is a finite maps which is indexed by the hashes of the keys of entities proposing the given updates, $\KeyHashGen$. We use the abstract type $\KeyHashGen$ to represent hashes of genesis (public verification) keys, which have type $\VKeyGen$. @@ -75,11 +51,7 @@ \subsection{Protocol Parameter Update Proposals} The transition type $\mathsf{PPUP}$ is for proposing updates to protocol parameters, see Figure \ref{fig:ts-types:pp-update} (for the corresponding rules, see Figure \ref{fig:rules:pp-update}). -The signal for this transition is a pair consisting of a finite map of -proposed updates (indexed by genesis keys) and an optional epoch -(the epoch must be specified if the mapping is nonempty). -The purpose of the $\Seed$ type in the $\PPUpdate$ derived type is explained -in the protocol parameter adoption rules. +The signal for this transition is an optional update. Protocol updates are only allowed up until ($2\cdot\SlotsPrior$)-many slots before the end of the epoch. The reason for this involves how we safely predict hard forks. @@ -87,11 +59,11 @@ \subsection{Protocol Parameter Update Proposals} entire stability period between when we know that a hard fork will necessarily happen and when the current epoch ends. +The transition $\mathsf{PPUP}$ has two rules: \begin{itemize} - \item PP-Update-Empty : no new updates were proposed, do nothing - \item PP-Update-Nonempty : some new updates $\var{pup}$ were proposed - Add these to - the existing proposals using a right override. That is, if a genesis key + \item PP-Update-Empty : No new updates were proposed, do nothing. + \item PP-Update-Nonempty : Some new updates $\var{up}$ were proposed. + Add these to the existing proposals using a right override. That is, if a genesis key has previously submitted an update proposal, replace it with its new proposal in $\var{pup}$. \end{itemize} @@ -102,26 +74,16 @@ \subsection{Protocol Parameter Update Proposals} \item In the case of \var{slot} being greater than or equal to $\fun{firstSlot}~((\epoch{slot}) + 1) - 2\cdot\fun{SlotsPrior}$, there is a \emph{PPUpdateTooLate} failure. -\item In the case that the epoch number in the signal is not the current epoch, - there is a \emph{PPUpdateNoEpoch} failure. +\item In the case that the epoch number in the signal does not match the current epoch, + there is a \emph{PPUpdateWrongEpoch} failure. \item In the case of \var{pup} being non-empty, if the check $\dom pup \subseteq \dom genDelegs$ fails, there is a \emph{NonGenesisUpdate} failure as only genesis keys can be used in the protocol parameter update. \item If a protocol parameter update in \var{pup} cannot follow the current protocol parameter, there is a \emph{PVCannotFollow} failure. + Note that $\fun{pvCanFollow}$ is defined in Figure~\ref{fig:funcs:helper-updates}. \end{enumerate} -Note that $\fun{pvCanFollow}$ -is defined in Figure~\ref{fig:funcs:helper-updates}. -is used in defining the blockchain layer functionality (specifically, -properties of header validation), -and is explained in detail in the paper \cite{byron_chain_spec}. -It is used in this document in -Section \ref{sec:chain}. -Because of the header validation requirements, a protocol parameter proposal -must be submitted with at least $\SlotsPrior$-slots before the end of an epoch, -and will be rejected otherwise. - \begin{figure}[htb] \emph{Protocol Parameter Update environment} \begin{equation*} @@ -140,7 +102,7 @@ \subsection{Protocol Parameter Update Proposals} \_ \vdash \var{\_} \trans{ppup}{\_} \var{\_} \subseteq \powerset ( - \PPUpdateEnv \times \PPUpdate \times (\PPUpdate\times\Epoch^?) \times \PPUpdate) + \PPUpdateEnv \times \ProposedPPUpdates \times \Update^? \times \ProposedPPUpdates) \end{equation*} % \caption{Protocol Parameter Update Transition System Types} @@ -151,7 +113,7 @@ \subsection{Protocol Parameter Update Proposals} \begin{equation}\label{eq:pp-update-Empty} \inference[PP-Update-Empty] { - \var{pup} = \emptyset + \var{up} = \Nothing } { \begin{array}{r} @@ -159,7 +121,7 @@ \subsection{Protocol Parameter Update Proposals} \var{pp}\\ \var{genDelegs}\\ \end{array} - \vdash \var{pup_s}\trans{ppup}{(pup,~e)}\var{pup_s} + \vdash \var{pup_s}\trans{ppup}{up}\var{pup_s} } \end{equation} @@ -168,7 +130,7 @@ \subsection{Protocol Parameter Update Proposals} \begin{equation}\label{eq:update-nonempty} \inference[PP-Update-Nonempty] { - \var{pup}\neq\emptyset + (\var{pup},~\var{e})\leteq\var{up} & \dom{pup}\subseteq\dom{genDelegs} \\ @@ -187,7 +149,7 @@ \subsection{Protocol Parameter Update Proposals} \end{array} \vdash \var{pup_s} - \trans{ppup}{(pup,~e)} + \trans{ppup}{up} \varUpdate{pup_s\unionoverrideRight pup} } \end{equation} @@ -198,420 +160,6 @@ \subsection{Protocol Parameter Update Proposals} \clearpage -Figure~\ref{fig:funcs:helper-updates} gives some helper functions for the -application version update transition. -The function $\fun{votedValue_T}$ returns -the consensus value of update proposals in the event that at least five -genesis keys agree (see the document~\cite{delegation_design}). Note that this is greater -than majority (there are seven core nodes), so there can -be \text{at most one value} with five or more votes. -This function will also be used for the protocol parameters later in Section~\ref{sec:epoch}. -Note that $\type{T}$ is an arbitrary type. The specific choice of this type -determines what is being voted on, e.g. the application version. -Recall here that $\type{T}^?$ is the option type, see Section~\ref{sec:notation-shelley}, -and a term of this type can have a value of type $\type{T}$ or no value. - -The function $\fun{newAVs}$ adds the most recent valid application -versions to a finite map of applications using right override. -This helper function will be used in the ledger update. - -\textbf{Note that} $\fun{votedValue}$ -\textbf{is only well-defined if } $\Quorum$ -\textbf{is greater than half the number of core nodes, i.e.} -$\Quorum > |\var{genDelegs}|/2$ \textbf{.} -%% -%% Figure - Helper Function for Consensus of Update Proposals -%% -\begin{figure}[htb] - \begin{align*} - & \fun{votedValue_T} \in (\KeyHashGen\mapsto\type{T}) \to \type{T}^?\\ - & \fun{votedValue_T}~\var{vs} = - \begin{cases} - t & \exists t\in\range{vs}~(|vs\restrictrange t|\geq \Quorum) \\ - \Nothing & \text{otherwise} \\ - \end{cases} - \end{align*} - - \begin{align*} - & \fun{maxVer} \in \ApName \to \Applications \to (\Slot\mapsto\Applications) - \to (\ApVer, \Metadata)\\ - & \fun{maxVer}~\var{an}~\var{avs}~\var{favs} = \\ - & ~~~~\fun{max_{first}} \Bigg( - \Big\{(0, \emptyset)\Big\} - \cup - \range{avs} - \cup - \bigcup_{\var{fav}\in\var{favs}} - \range{favs} - \Bigg) - \end{align*} - - \begin{align*} - & \fun{pvCanFollow} \in \ProtVer \to \ProtVer \to \Bool \\ - & \fun{pvCanFollow}~\var{(m,~n)}~\var{(m', n')} = \\ - & ~~~~ (m', n') = (m+1,~0) \lor (m', n') = (m,~n+1) \\ - \end{align*} - - \begin{align*} - & \fun{svCanFollow} \in \Applications \to (\Slot\mapsto\Applications) - \to \ApName \to \ApVer \to \Bool\\ - & \fun{svCanFollow}~\var{avs}~\var{favs}~\var{an}~\var{av}= av = 1 + v' \\ - & ~~~~\where (v',~\wcard) = \fun{maxVer}~\var{an}~\var{avs}~\var{favs} - \end{align*} - - \begin{align*} - & \fun{newAVs} \in \Applications \to (\Slot\mapsto\Applications) \to \Applications \\ - & \fun{newAVs}~\var{avs}~\var{favs} = \\ - & ~~~~\Bigg\{\var{an}\mapsto\fun{maxVer}~\var{an}~\var{avs}~\var{favs} - ~\mid~ - \var{an}\in\Big(\dom{avs}\cup\bigcup_{\var{fav}\in\var{favs}}\dom{fav}\Big) - \Bigg\} - \end{align*} - - \caption{Epoch Helper Functions} - \label{fig:funcs:helper-updates} -\end{figure} - -\subsection{Application Version Update Proposals} -\label{sec:app-proposals} - -The application (or software) version update is defined by the $\mathsf{AVUP}$ -transition type (see Figure \ref{fig:ts-types:av-update}), and the rules in -Figure \ref{fig:rules:av-update}. -The state contains a finite map of update proposals -$\var{aup} \in \AVUpdate$ ($= \VKeyGen \mapsto \Applications$) that the genesis keys have -made previously. -The \textit{voting} and \textit{proposing an application version update} is done through the same -mechanism - the $\var{aup}$ signal carried by a transaction. The difference -is that a proposal is not in the -range of the $\var{aup}$, but a vote is for an existing proposal -in $\var{aup}$. - -Recall here that a single application version update proposal can be -proposing changes to multiple parts of the Cardano system software simultaneously. -This is why it is stored as the finite map $\Applications$, associating the -specific bit of software (referred to by name) with the proposed version. -A proposal for several versions of the same application cannot be made in -a single transaction by the same genesis key. - -The ledger state variable $\var{avs}$ stores the current application version -that the users \textit{should} be running. -Now, the state variable $\var{favs}$ contains update proposals that -were voted on by at least five genesis keys. -The particular update $\var{favs} = s \mapsto ap$ will become -the current application version at slot $s$. -Updating the current application version is part of the rules in the ledger transitionn, -see Section \ref{sec:ledger-trans}. - -At most one application version update -can be selected for a given slot, and some slots do not have any -updates selected by voting - either because none were proposed, or the vote -did not reach a concensus. Finally, the $\var{avs}$ variable stores -the versions of the software that are currently in use. The update -proposal rules are as follows: - -\begin{itemize} - \item AV-Update-Empty: rule represents an update with -and empty set of application version proposals, when nothing happens. - \item AV-Update-No-Consensus: rule -is for the case where a voting consensus was not reached on a proposed software -update after combining the set of new (signal) and existing (state) proposals -by a right override. In this case, we simply use this combined new value -of update proposal (votes) as the state UP value. - \item AV-Update-Consensus: applies when voting on update proposals by genesis keys -reaches consensus. This update is stored associated with a slot which is -$\SlotsPrior$ in the future from the current one, because this is when -this update will become the current AV. -All other update proposals are scrapped. -\end{itemize} - -The AVUP rule has two predicate failures: -\begin{itemize} -\item In the case of \var{aup} being non-empty, if the check $\dom aup \subseteq - \dom genDelegs$ fails, there is a \emph{NonGenesisUpdate} failure as only genesis keys - can be used in the application version update. -\item In the case of \var{aup} being non-empty, if any of the application versions - in the proposal are not exactly one more than the greatest version for the given - application name in the current application versions or the future application - versions, there is a \emph{CannotFollow} failure. -\end{itemize} - -\begin{figure}[htb] - \emph{Application Version Update environment} - \begin{equation*} - \AVUpdateEnv = - \left( - \begin{array}{r@{~\in~}lr} - \var{slot} & \Slot & \text{current slot}\\ - \var{genDelegs} & \KeyHashGen\mapsto\KeyHash & \text{genesis key delegations} \\ - \end{array} - \right) - \end{equation*} - % - \emph{Application Version Update states} - \begin{equation*} - \AVUpdateState = - \left( - \begin{array}{r@{~\in~}lr} - \var{aup} & \AVUpdate & \text{application versions proposals} \\ - \var{favs} & \Slot\mapsto\Applications & \text{future application versions} \\ - \var{avs} & \Applications & \text{current application versions} \\ - \end{array} - \right) - \end{equation*} - % - \emph{Application Version Update transitions} - \begin{equation*} - \_ \vdash - \var{\_} \trans{avup}{\_} \var{\_} - \subseteq \powerset (\AVUpdateEnv \times \AVUpdateState \times \AVUpdate \times \AVUpdateState) - \end{equation*} - % - \caption{Application Version Update transition-system types} - \label{fig:ts-types:av-update} -\end{figure} - -\begin{figure}[htb] - \begin{equation}\label{eq:av-update-Empty} - \inference[AV-Update-Empty] - { - \var{aup} = \emptyset - } - { - \begin{array}{l} - \var{slot}\\ - \var{genDelegs}\\ - \end{array} - \vdash - \left( - \begin{array}{l} - \var{aup_s}\\ - \var{favs}\\ - \var{avs}\\ - \end{array} - \right) - \trans{avup}{aup} - \left( - \begin{array}{l} - \var{aup_s}\\ - \var{favs}\\ - \var{avs}\\ - \end{array} - \right) - } - \end{equation} - - \nextdef - - \begin{equation}\label{eq:update-no-consensus} - \inference[AV-Update-No-Consensus] - { - \var{aup}\neq\emptyset - & - \dom{\var{aup}}\subseteq\dom{\var{genDelegs}} - \\ - \forall \wcard\mapsto\var{vote}\in\var{aup},\forall n\mapsto(v,~\wcard)\in\var{vote},~ - \fun{svCanFollow}~\var{avs}~\var{favs}~\var{n}~\var{v} - \\ - \var{aup'}\leteq\var{aup_s}\unionoverrideRight\var{aup} - \\ - \var{fav}\leteq\fun{votedValue_{Applications}}~\var{aup'} - & - \var{fav}=\Nothing - } - { - \begin{array}{l} - \var{slot}\\ - \var{genDelegs}\\ - \end{array} - \vdash - \left( - \begin{array}{l} - \var{aup_s}\\ - \var{favs}\\ - \var{avs}\\ - \end{array} - \right) - \trans{avup}{aup} - \left( - \begin{array}{l} - \varUpdate{\var{aup'}}\\ - \var{favs}\\ - \var{avs}\\ - \end{array} - \right) - } - \end{equation} - - \nextdef - - \begin{equation}\label{eq:update-consensus} - \inference[AV-Update-Consensus] - { - \var{aup}\neq\emptyset - & - \dom{\var{aup}}\subseteq\dom{\var{genDelegs}} - \\ - \forall \wcard\mapsto\var{vote}\in\var{aup},\forall n\mapsto(v,~\wcard)\in\var{vote},~ - \fun{svCanFollow}~\var{avs}~\var{favs}~\var{n}~\var{v} - \\ - \var{aup'}\leteq\var{aup_s}\unionoverrideRight\var{aup} - \\ - \var{fav}\leteq\fun{votedValue_{Applications}}~\var{aup'} - & - \var{fav}\neq\Nothing - \\ - s\leteq\var{slot}+\SlotsPrior - } - { - \begin{array}{l} - \var{slot}\\ - \var{genDelegs}\\ - \end{array} - \vdash - \left( - \begin{array}{l} - \var{aup_s}\\ - \var{favs}\\ - \var{avs}\\ - \end{array} - \right) - \trans{avup}{aup} - \left( - \begin{array}{l} - \varUpdate{\emptyset}\\ - \varUpdate{\var{favs}\unionoverrideRight\{\var{s}\mapsto\var{fav}\}}\\ - \var{avs}\\ - \end{array} - \right) - } - \end{equation} - - \caption{Application Version Update inference rules} - \label{fig:rules:av-update} -\end{figure} -\clearpage - -The $\mathsf{UP}$ transition type combines processing update -proposals for protocol parameters and applications. The signal for this -transition is a pair of update proposals for parameters and applications, -and each of these is a signal for updating the corresponding data structure. -Both get updated simultaneously by this rule according to a relevant -update rules for each. - -\begin{figure}[htb] - \emph{Update environment} - \begin{equation*} - \UpdateEnv = - \left( - \begin{array}{r@{~\in~}lr} - \var{slot} & \Slot & \text{current slot}\\ - \var{pp} & \PParams & \text{protocol parameters}\\ - \var{genDelegs} & \KeyHashGen\mapsto\KeyHash & \text{genesis key delegations} \\ - \end{array} - \right) - \end{equation*} - % - \emph{Update states} - \begin{equation*} - \UpdateState = - \left( - \begin{array}{r@{~\in~}lr} - \var{pup} & \PPUpdate & \text{protocol parameter proposals} \\ - \var{aup} & \AVUpdate & \text{application versions proposals} \\ - \var{favs} & \Slot\mapsto\Applications & \text{future application versions} \\ - \var{avs} & \Applications & \text{current application versions} \\ - \end{array} - \right) - \end{equation*} - % - \emph{Update transitions} - \begin{equation*} - \_ \vdash - \var{\_} \trans{up}{\_} \var{\_} - \subseteq \powerset (\UpdateEnv \times \UpdateState \times \Update \times \UpdateState) - \end{equation*} - % - \caption{Application Version Update transition-system types} - \label{fig:ts-types:update} -\end{figure} - -\begin{figure}[htb] - \begin{equation}\label{eq:update} - \inference[Update] - { - (\var{pup_{u}},~\var{aup_{u}},~e)\leteq\var{up} - \\~\\ - { - \begin{array}{r} - \var{slot} \\ - \var{pp} \\ - \var{genDelegs} \\ - \end{array} - } - \vdash - \left(\var{pup}\right) - \trans{\hyperref[fig:rules:pp-update]{ppup}}{(\var{pup_{u}},~e)} - \left(\var{pup'}\right) - & - { - \begin{array}{r} - \var{slot} \\ - \var{genDelegs} \\ - \end{array} - } - \vdash - { - \left( - \begin{array}{r} - \var{aup}\\ - \var{favs}\\ - \var{avs}\\ - \end{array} - \right) - } - \trans{\hyperref[fig:rules:av-update]{avup}}{\var{aup_{u}}} - { - \left( - \begin{array}{r} - \var{aup'}\\ - \var{favs'}\\ - \var{avs'}\\ - \end{array} - \right) - } - } - { - \begin{array}{r} - \var{slot}\\ - \var{pp} \\ - \var{genDelegs}\\ - \end{array} - \vdash - \left( - \begin{array}{l} - \var{pup}\\ - \var{aup}\\ - \var{favs}\\ - \var{avs}\\ - \end{array} - \right) - \trans{up}{up} - \left( - \begin{array}{l} - \varUpdate{\var{pup}'} \\ - \varUpdate{\var{aup}'} \\ - \varUpdate{\var{favs}'} \\ - \varUpdate{\var{avs}'} \\ - \end{array} - \right) - } - \end{equation} - - \caption{Update inference rules} - \label{fig:rules:update} -\end{figure} - %%% Local Variables: %%% mode: latex %%% TeX-master: t diff --git a/shelley/chain-and-ledger/formal-spec/utxo.tex b/shelley/chain-and-ledger/formal-spec/utxo.tex index f205a3af91b..8389cda57ab 100644 --- a/shelley/chain-and-ledger/formal-spec/utxo.tex +++ b/shelley/chain-and-ledger/formal-spec/utxo.tex @@ -145,7 +145,7 @@ \subsection{UTxO Transitions} \item The current UTxO. \item The deposit pot. \item The fee pot. - \item The update state (see Figure~\ref{fig:ts-types:update}). + \item Proposed updates (see Section~\ref{sec:update}). \end{itemize} The signal for the UTxO transition is a transaction. @@ -172,7 +172,7 @@ \subsection{UTxO Transitions} \var{utxo} & \UTxO & \text{UTxO}\\ \var{deposits} & \Coin & \text{deposits pot}\\ \var{fees} & \Coin & \text{fee pot}\\ - \var{ups} & \UpdateState & \text{update state}\\ + \var{pup} & \ProposedPPUpdates & \text{proposed updates}\\ \end{array} \right) \end{equation*} @@ -216,7 +216,7 @@ \subsection{UTxO Transitions} In other words, the amount of value produced by the transaction must be the same as the amount consumed. \item - The $\mathsf{UPDATE}$ transition is successful. + The $\mathsf{PPUP}$ transition is successful. \item The coin value of each new output must be non-negative. \item @@ -308,7 +308,7 @@ \subsection{UTxO Transitions} \var{genDelegs} \\ \end{array} } - \vdash \var{ups} \trans{\hyperref[fig:rules:update]{up}}{\fun{txup}~\var{tx}} \var{ups'} + \vdash \var{pup} \trans{\hyperref[fig:rules:pp-update]{ppup}}{\fun{txup}~\var{tx}} \var{pup'} \\ ~ \\ @@ -339,7 +339,7 @@ \subsection{UTxO Transitions} \var{utxo} \\ \var{deposits} \\ \var{fees} \\ - \var{ups}\\ + \var{pup}\\ \end{array} \right) \trans{utxo}{tx} @@ -348,7 +348,7 @@ \subsection{UTxO Transitions} \varUpdate{(\txins{txb} \subtractdom \var{utxo}) \cup \outs{txb}} \\ \varUpdate{\var{deposits} + \var{depositChange}} \\ \varUpdate{\var{fees} + \txfee{txb} + \var{decayed}} \\ - \varUpdate{ups'}\\ + \varUpdate{pup'}\\ \end{array} \right) } @@ -573,12 +573,12 @@ \subsection{Witnesses} \begin{align*} & \fun{propWits} \in \Update \to (\KeyHashGen\mapsto\VKey) \to \powerset{\KeyHash} & \text{hashkeys for proposals} \\ - & \fun{propWits}~(\var{pup},~\var{aup})~\var{genDelegs} = \\ + & \fun{propWits}~(\var{pup},~\wcard)~\var{genDelegs} = \\ & ~~\left\{ \hashKey{vkey} \mid \var{gkey}\mapsto\var{vkey}\in - \left(\left(\dom{\var{pup}}\cup\dom{\var{aup}}\right)\restrictdom\var{genDelegs}\right) + \left(\dom{\var{pup}}\restrictdom\var{genDelegs}\right) \right\} \end{align*}