From c09df2d8af7393ab312b028633636acdc56c51c6 Mon Sep 17 00:00:00 2001 From: whatisRT Date: Wed, 29 Sep 2021 17:46:36 +0200 Subject: [PATCH] TEMP: remove d from the shelley spec --- eras/shelley/formal-spec/chain.tex | 254 +----------------- eras/shelley/formal-spec/epoch.tex | 16 +- .../formal-spec/protocol-parameters.tex | 2 - 3 files changed, 12 insertions(+), 260 deletions(-) diff --git a/eras/shelley/formal-spec/chain.tex b/eras/shelley/formal-spec/chain.tex index c7269e93b98..cd5df4fa625 100644 --- a/eras/shelley/formal-spec/chain.tex +++ b/eras/shelley/formal-spec/chain.tex @@ -1122,233 +1122,6 @@ \subsection{Verifiable Random Function} \clearpage -\subsection{Overlay Schedule} -\label{sec:overlay-schedule} - -The transition from the bootstrap era to a fully decentralized network is explained in -section 3.9.2 of~\cite{delegation_design}. -Key to this transition is a protocol parameter $d$ which controls how many slots are governed by -the genesis nodes via OBFT, and which slots are open to any registered stake pool. -The transition system introduced in this section, $\type{OVERLAY}$, covers this mechanism. - -This transition is responsible for validating the protocol for both the OBFT blocks -and the Praos blocks, depending on the overlay schedule. - -The actual overlay schedule itself it determined by two functions, -$\fun{isOverlaySlot}$ and $\fun{classifyOverlaySlot}$, -which are defined in Figure~\ref{fig:rules:overlay}. -The function $\fun{isOverlaySlot}$ determines if the current slot -is reserved for the OBFT nodes. -In particular, it looks at the current relative slot to -see if the next multiple of $d$ (the decentralization protocol parameter) -raises the ceiling. -If a slot is indeed in the overlay schedule, -the function $\fun{classifyOverlaySlot}$ determines if the current slot -should be a silent slot (no block is allowed) or which core node -is responsible for the block. -The non-silent blocks are the multiples of $1/\ActiveSlotCoeff$, -and the responsible core node are determined by -taking turns according the lexicographic ordering of the core node keyhashes. -\textbf{Note} that $1/\ActiveSlotCoeff$ needs to be natural number, -otherwise the multilples of $\lfloor 1/\ActiveSlotCoeff \rfloor$ -will yield a different proportion of active slots than the Praos blocks. - -The environments for the overlay schedule transition are: -\begin{itemize} - \item The decentralization parameter $d$. - \item The epoch nonce $\eta_0$. - \item The stake pool stake distribution $\var{pd}$. - \item The mapping $\var{genDelegs}$ of genesis keys to their cold keys and vrf keys. -\end{itemize} - -The states for this transition consist only of the mapping of certificate issue numbers. - -This transition establishes that a block producer is in fact authorized. -Since there are three key pairs involved (cold keys, VRF keys, and hot KES keys) -it is worth examining the interaction closely. -First we look at the regular Praos/decentralized setting, -which is given by Equation~\ref{eq:decentralized}. - -\begin{itemize} - \item First we check the operational certificate with $\mathsf{OCERT}$. - This uses the cold verification key given in the block header. - We do not yet trust that this key is a registered pool key. - If this transition is successful, we know that the cold key in the block header has authorized - the block. -\item Next, in the $\fun{vrfChecks}$ predicate, we check that the hash of this cold key is in the - mapping $\var{pd}$, and that it maps to $(\sigma,~\var{hk_{vrf}})$, where - $(\sigma,~\var{hk_{vrf}})$ is the hash of the VRF key in the header. - If $\fun{praosVrfChecks}$ returns true, then we know that the cold key in the block header was a - registered stake pool at the beginning of the previous epoch, and that it is indeed registered - with the VRF key listed in the header. -\item Finally, we use the VRF verification key in the header, along with the VRF proofs in the - header, to check that the operator is allowed to produce the block. -\end{itemize} -The situation for the overlay schedule, given by Equation~\ref{eq:active-pbft}, is similar. -The difference is that we check the overlay schedule to see what core node is -supposed to make a block, and then use the genesis delegation mapping to -check the correct cold key hash and vrf key hash. - -\begin{figure} - \emph{Overlay environments} - \begin{equation*} - \OverlayEnv = - \left( - \begin{array}{r@{~\in~}lr} - \var{d} & \{0,~1/100,~2/100,~\ldots,~1\} & \text{decentralization parameter} \\ - \var{pd} & \PoolDistr & \text{pool stake distribution} \\ - \var{genDelegs} & \GenesisDelegation & \text{genesis key delegations} \\ - \eta_0 & \Seed & \text{epoch nonce} \\ - \end{array} - \right) - \end{equation*} - % - \emph{Overlay Transitions} - \begin{equation*} - \_ \vdash \var{\_} \trans{overlay}{\_} \var{\_} \subseteq - \powerset (\OverlayEnv \times (\KeyHash_{pool} \mapsto \N) \times \BHeader \times - (\KeyHash_{pool} \mapsto \N)) - \end{equation*} - % - \emph{Overlay Schedule helper functions} - \begin{align*} - & \fun{isOverlaySlot} \in \Slot \to \unitInterval \to \Slot \to \Bool \\ - & \isOverlaySlot{fSlot}{dval}{slot} = \lceil s\cdot dval \rceil < \lceil (s+1)\cdot dval \rceil \\ - & ~~~~ \where s\leteq\slotminus{slot}{fslot} - \end{align*} - % - \begin{align*} - & \fun{classifyOverlaySlot} \in \Slot \to \powerset{\KeyHashGen} \to \unitInterval - \to \unitIntervalNonNull \to \Slot \to \Bool \\ - & \classifyOverlaySlot{fSlot}{gkeys}{dval}{asc}{slot} = \\ - & ~~~\begin{cases} - \fun{elemAt}~\left( \frac{\var{position}}{\var{ascInv}} \bmod |\var{gkeys}| \right)~\var{gkeys} - & - \text{if } \var{position} \equiv 0 \pmod{\var{ascInv}} \\ - \Nothing - & - \text{otherwise} - \end{cases} \\ - & ~~~~ \where \\ - & ~~~~~~~ \var{ascInv}\leteq\lfloor 1/\var{asc}\rfloor \\ - & ~~~~~~~ \var{position}\leteq \lceil (\slotminus{slot}{fSlot})\cdot dval \rceil \\ - & ~~~~~~~ \fun{elemAt}~i~\var{set}\leteq i'\text{th lexicographic element of }\var{set} - \end{align*} - % - \caption{Overlay transition-system types} - \label{fig:ts-types:overlay} -\end{figure} - -\begin{figure}[ht] - \begin{equation}\label{eq:active-pbft} - \inference[Active-OBFT] - { - \var{bhb}\leteq\bheader{bh} - & - \var{vk}\leteq\bvkcold{bhb} - & - \var{vkh}\leteq\hashKey{vk} - \\ - \var{slot} \leteq \bslot{bhb} - & - \var{fSlot} \leteq \fun{firstSlot}~(\epoch{slot}) - \\ - \var{gkh}\mapsto(\var{vkh},~\var{vrfh})\in\var{genDelegs} - \\ - \isOverlaySlot{fSlot}{(\dom{genDelegs})}{slot}\\ - \classifyOverlaySlot{fSlot}{(\dom{genDelegs})}{d}{\ActiveSlotCoeff}{slot} = \var{ghk} - \\~\\ - \fun{pbftVrfChecks}~\var{vrfh}~\eta_0~\var{bhb} - \\~\\ - { - {\begin{array}{c} - \dom{\var{pd}} \\ - \range{\var{genDelegs}} \\ - \end{array} - } - \vdash\var{cs}\trans{\hyperref[fig:rules:ocert]{ocert}}{\var{bh}}\var{cs'} - } - } - { - {\begin{array}{c} - \var{d} \\ - \eta_0 \\ - \var{pd} \\ - \var{genDelegs} \\ - \end{array}} - \vdash - \var{cs} - \trans{overlay}{\var{bh}} - \varUpdate{\var{cs}'} - } - \end{equation} - - \nextdef - - \begin{equation}\label{eq:decentralized} - \inference[Decentralized] - { - \var{bhb}\leteq\bheader{bh} - & - \var{slot} \leteq \bslot{bhb} - & - \var{fSlot} \leteq \fun{firstSlot}~(\epoch{slot}) - \\ - \neg\isOverlaySlot{fSlot}{(\dom{genDelegs})}{slot}\\ - \\~\\ - { - \vdash\var{cs}\trans{\hyperref[fig:rules:ocert]{ocert}}{\var{bh}}\var{cs'} - } - \\~\\ - \fun{praosVrfChecks}~\eta_0~\var{pd}~\ActiveSlotCoeff~\var{bhb} - } - { - {\begin{array}{c} - \var{d} \\ - \eta_0 \\ - \var{pd} \\ - \var{genDelegs} \\ - \end{array}} - \vdash - \var{cs} - \trans{overlay}{\var{bh}} - \varUpdate{\var{cs}'} - } - \end{equation} - - \caption{Overlay rules} - \label{fig:rules:overlay} -\end{figure} - -The OVERLAY rule has nine predicate failures: -\begin{itemize} -\item If in the decentralized case the VRF key is not in the pool distribution, - there is a \emph{VRFKeyUnknown} failure. -\item If in the decentralized case the VRF key hash does not match the one - listed in the block header, there is a \emph{VRFKeyWrongVRFKey} failure. -\item If the VRF generated nonce in the block header does not validate - against the VRF certificate, there is a \emph{VRFKeyBadNonce} failure. -\item If the VRF generated leader value in the block header does not validate - against the VRF certificate, there is a \emph{VRFKeyBadLeaderValue} failure. -\item If the VRF generated leader value in the block header is too large - compared to the relative stake of the pool, there is a \emph{VRFLeaderValueTooBig} failure. -\item In the case of the slot being in the OBFT schedule, but without genesis - key (i.e., $Nothing$), there is a \emph{NotActiveSlot} failure. -\item In the case of the slot being in the OBFT schedule, if there is a - specified genesis key which is not the same key as in the bock header body, - there is a \emph{WrongGenesisColdKey} failure. -\item In the case of the slot being in the OBFT schedule, if the hash of the - VRF key in block header does not match the hash in the genesis delegation mapping, - there is a \emph{WrongGenesisVRFKey} failure. -\item In the case of the slot being in the OBFT schedule, if the genesis delegate - keyhash is not in the genesis delegation mapping, - there is a \emph{UnknownGenesisKey} failure. - This case should never happen, and represents a logic error. - -\end{itemize} - -\clearpage - \subsection{Protocol Transition} \label{sec:protocol-trans} @@ -1362,9 +1135,7 @@ \subsection{Protocol Transition} \PrtclEnv = \left( \begin{array}{r@{~\in~}lr} - \var{d} & \{0,~1/100,~2/100,~\ldots,~1\} & \text{decentralization parameter} \\ \var{pd} & \PoolDistr & \text{pool stake distribution} \\ - \var{dms} & \KeyHashGen\mapsto\KeyHash & \text{genesis key delegations} \\ \eta_0 & \Seed & \text{epoch nonce} \\ \end{array} \right) @@ -1410,6 +1181,7 @@ \subsection{Protocol Transition} \begin{equation}\label{eq:prtcl} \inference[PRTCL] { + \var{bhb}\leteq\bheader{bh} & \eta\leteq\fun{bnonce}~(\bhbody{bhb}) \\~\\ { @@ -1424,23 +1196,16 @@ \subsection{Protocol Transition} \eta_v' \\ \eta_c' \\ \end{array}\right)} - }\\~\\ + }\\~\\ { - {\begin{array}{c} - \var{d} \\ - \var{pd} \\ - \var{dms} \\ - \eta_0 \\ - \end{array} - } - \vdash \var{cs}\trans{\hyperref[fig:rules:overlay]{overlay}}{\var{bh}} \var{cs}' + \vdash\var{cs}\trans{\hyperref[fig:rules:ocert]{ocert}}{\var{bh}}\var{cs'} } + \\~\\ + \fun{praosVrfChecks}~\eta_0~\var{pd}~\ActiveSlotCoeff~\var{bhb} } { {\begin{array}{c} - \var{d} \\ \var{pd} \\ - \var{dms} \\ \eta_0 \\ \end{array}} \vdash @@ -1509,11 +1274,10 @@ \subsection{Block Body Transition} % \emph{BBody helper function} \begin{align*} - & \fun{incrBlocks} \in \Bool \to \KeyHash_{pool} \to + & \fun{incrBlocks} \in \KeyHash_{pool} \to \BlocksMade \to \BlocksMade \\ - & \fun{incrBlocks}~\var{isOverlay}~\var{hk}~\var{b} = + & \fun{incrBlocks}~\var{hk}~\var{b} = \begin{cases} - b & \text{if }\var{isOverlay} \\ b\cup\{\var{hk}\mapsto 1\} & \text{if }\var{hk}\notin\dom{b} \\ b\unionoverrideRight\{\var{hk}\mapsto n+1\} & \text{if }\var{hk}\mapsto n\in b \\ \end{cases} @@ -1588,7 +1352,7 @@ \subsection{Block Body Transition} \trans{bbody}{\var{block}} {\left(\begin{array}{c} \varUpdate{\var{ls}'} \\ - \varUpdate{\fun{incrBlocks}~{\left(\isOverlaySlot{fSlot}{(\fun{d}~pp)}{slot}\right)}~{hk}~{b}} \\ + \varUpdate{\fun{incrBlocks}~{hk}~{b}} \\ \end{array}\right)} } \end{equation} @@ -1812,9 +1576,7 @@ \subsection{Chain Transition} }\\~\\~\\ { {\begin{array}{c} - (\fun{d}~\var{pp}) \\ \var{pd} \\ - \var{genDelegs} \\ \eta_0' \\ \end{array}} \vdash diff --git a/eras/shelley/formal-spec/epoch.tex b/eras/shelley/formal-spec/epoch.tex index 4aa2fef70b0..3b48919cfe4 100644 --- a/eras/shelley/formal-spec/epoch.tex +++ b/eras/shelley/formal-spec/epoch.tex @@ -24,7 +24,7 @@ \section{Rewards and the Epoch Boundary} \newcommand{\stakeDistr}[3]{\fun{stakeDistr}~ \var{#1}~ \var{#2}~ \var{#3}} \newcommand{\lReward}[4]{\fun{r_{operator}}~ \var{#1}~ \var{#2}~ \var{#3}~ {#4}} \newcommand{\mReward}[4]{\fun{r_{member}}~ \var{#1}~ \var{#2}~ \var{#3}~ {#4}} -\newcommand{\mkApparentPerformance}[4]{\fun{mkApparentPerformance}~\var{#1}~{#2}~\var{#3}~\var{#4}} +\newcommand{\mkApparentPerformance}[3]{\fun{mkApparentPerformance}~{#1}~\var{#2}~\var{#3}} \newcommand{\createRUpd}[4]{\fun{createRUpd}~\var{#1}~\var{#2}~\var{#3}~\var{#4}} \newcommand{\getIR}[1]{\fun{getIR}~\var{#1}} @@ -1099,11 +1099,7 @@ \subsection{Rewards Distribution Calculation} % \begin{align*} & \fun{mkApparentPerformance} \in \unitInterval \to \unitInterval \to \N \to \N \to \Q \\ - & \mkApparentPerformance{d}{\sigma}{n}{\overline{N}} = - \begin{cases} - \frac{\beta}{\sigma} & \text{if } d < 0.8 \\ - 1 & \text{otherwise} - \end{cases} \\ + & \mkApparentPerformance{\sigma}{n}{\overline{N}} = \frac{\beta}{\sigma} \\ & ~~~\where \\ & ~~~~~~~\beta = \frac{n}{\max(1, \overline{N})} \\ \end{align*} @@ -1217,7 +1213,7 @@ \subsection{Rewards Distribution Calculation} \var{pledge} \leq \var{ostake}\\ 0 & \text{otherwise.} \end{cases} \\ - & ~~~~~~~\var{appPerf} = \mkApparentPerformance{(\fun{d}~pp)}{\sigma_a}{n}{\overline{N}} \\ + & ~~~~~~~\var{appPerf} = \mkApparentPerformance{\sigma_a}{n}{\overline{N}} \\ & ~~~~~~~\var{poolR} = \floor{\var{appPerf}\cdot\var{maxP}} \\ & ~~~~~~~\var{mRewards} = \\ & ~~~~~~~~~~\left\{ @@ -1446,11 +1442,7 @@ \subsection{Reward Update Calculation} \var{reserves}} \\ & ~~~~~~~\eta = - \begin{cases} - 1 & (\fun{d}~\var{prevPp})\geq 0.8 \\ - \frac{blocksMade}{\floor{(1-\fun{d}~\var{prevPp})\cdot\var{slotsPerEpoch} \cdot \ActiveSlotCoeff}} - & \text{otherwise} \\ - \end{cases} \\ + \frac{blocksMade}{\floor{{slotsPerEpoch} \cdot \ActiveSlotCoeff}} \\ & ~~~~~~~\var{rewardPot} = \var{feeSS} + \Delta r_1 \\ & ~~~~~~~\Delta t_1 = \floor*{(\fun{tau}~\var{prevPp}) \cdot \var{rewardPot}} \\ & ~~~~~~~\var{R} = \var{rewardPot} - \Delta t_1 \\ diff --git a/eras/shelley/formal-spec/protocol-parameters.tex b/eras/shelley/formal-spec/protocol-parameters.tex index 34cd6486ae4..35dfb6ae30e 100644 --- a/eras/shelley/formal-spec/protocol-parameters.tex +++ b/eras/shelley/formal-spec/protocol-parameters.tex @@ -89,7 +89,6 @@ \subsection{Updatable Protocol Parameters} \var{a_0} \mapsto \nonnegReals & \PParams & \text{pool influence}\\ \tau \mapsto \unitInterval & \PParams & \text{treasury expansion}\\ \rho \mapsto \unitInterval & \PParams & \text{monetary expansion}\\ - \var{d} \mapsto \{0,~1/100,~2/100,~\ldots,~1\} & \PParams & \text{decentralization parameter}\\ \var{extraEntropy} \mapsto \Seed & \PParams & \text{extra entropy}\\ \var{pv} \mapsto \ProtVer & \PParams & \text{protocol version}\\ \var{minUTxOValue} \mapsto \Coin & \PParams & \text{minimum allowed value of a new \TxOut}\\ @@ -112,7 +111,6 @@ \subsection{Updatable Protocol Parameters} \fun{influence}, \fun{tau}, \fun{rho}, - \fun{d}, \fun{extraEntropy}, \fun{pv}, \fun{minUTxOValue},