Skip to content

Commit

Permalink
TEMP: remove d from the shelley spec
Browse files Browse the repository at this point in the history
  • Loading branch information
@WhatisRT
WhatisRT committed Sep 29, 2021
1 parent c6c4be1 commit c09df2d
Show file tree
Hide file tree
Showing 3 changed files with 12 additions and 260 deletions.
254 changes: 8 additions & 246 deletions eras/shelley/formal-spec/chain.tex
View file
Expand Up @@ -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}

Expand All @@ -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)
Expand Down Expand Up @@ -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})
\\~\\
{
Expand All @@ -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
Expand Down Expand Up @@ -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}
Expand Down Expand Up @@ -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}
Expand Down Expand Up @@ -1812,9 +1576,7 @@ \subsection{Chain Transition}
}\\~\\~\\
{
{\begin{array}{c}
(\fun{d}~\var{pp}) \\
\var{pd} \\
\var{genDelegs} \\
\eta_0' \\
\end{array}}
\vdash
Expand Down
16 changes: 4 additions & 12 deletions eras/shelley/formal-spec/epoch.tex
View file
Expand Up @@ -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}}

Expand Down Expand Up @@ -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*}
Expand Down Expand Up @@ -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\{
Expand Down Expand Up @@ -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 \\
Expand Down
2 changes: 0 additions & 2 deletions eras/shelley/formal-spec/protocol-parameters.tex
View file
Expand Up @@ -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}\\
Expand All @@ -112,7 +111,6 @@ \subsection{Updatable Protocol Parameters}
\fun{influence},
\fun{tau},
\fun{rho},
\fun{d},
\fun{extraEntropy},
\fun{pv},
\fun{minUTxOValue},
Expand Down

0 comments on commit c09df2d

Please sign in to comment.