Skip to content

add VRF keyhashes to genesis delegation mapping #1501

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
May 29, 2020
Merged

add VRF keyhashes to genesis delegation mapping #1501

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
97 changes: 67 additions & 30 deletions shelley/chain-and-ledger/formal-spec/chain.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -888,7 +888,7 @@ \subsection{Chain Tick Transition}
\\
& ~~~~~~~~~~\var{curr}\leteq
\{
(\var{s},~\var{gkh})\mapsto\var{vkh}\in\var{fGenDelegs}
(\var{s},~\var{gkh})\mapsto(\var{vkh},~\var{vrf})\in\var{fGenDelegs}
~\mid~
\var{s}\leq\var{slot}
\}
Expand All @@ -898,11 +898,11 @@ \subsection{Chain Tick Transition}
\\
& ~~~~~~~~~~\var{genDelegs'}\leteq
\left\{
\var{gkh}\mapsto\var{vkh}
\var{gkh}\mapsto(\var{vkh},~\var{vrf})
~\mathrel{\Bigg|}~
{
\begin{array}{l}
(\var{s},~\var{gkh})\mapsto\var{vkh}\in\var{curr}\\
(\var{s},~\var{gkh})\mapsto(\var{vkh},~\var{vrf})\in\var{curr}\\
\var{s}=\max\{s'~\mid~(s',~\var{gkh})\in\dom{\var{curr}}\}
\end{array}
}
Expand Down Expand Up @@ -1125,25 +1125,42 @@ \subsection{Verifiable Random Function}
\begin{figure}
\emph{VRF helper function}
\begin{align*}
& \fun{vrfChecks} \in \Seed \to \PoolDistr \to \unitInterval \to \BHBody \to \Bool \\
& \fun{vrfChecks}~\eta_0~\var{pd}~\var{f}~\var{bhb} = \\
& \fun{vrfChecks} \in \Seed \to \BHBody \to \Bool \\
& \fun{vrfChecks}~\eta_0~\var{bhb} = \\
& \begin{array}{cl}
~~~~ & \var{hk}\mapsto (\sigma,~\var{hk_{vrf}})\in\var{pd} \\
~~~~ \land &
~~~~ &
\verifyVrf{\Seed}{\var{vrfVk}}{((\eta_0\seedOp ss)\seedOp\Seede)}
{(\bprfn{bhb},~\bnonce{bhb}}) \\
~~~~ \land &
\verifyVrf{\unitInterval}{\var{vrfVk}}{((\eta_0\seedOp ss)\seedOp\Seedl)}
{(\bprfl{bhb},~\bleader{bhb}}) \\
~~~~ \land &
\fun{bleader}~\var{bhb} < 1 - (1 - f)^{\sigma} \\
\end{array} \\
& ~~~~\where \\
& ~~~~~~~~~~\var{hk} \leteq \hashKey{(\bvkcold bhb)} \\
& ~~~~~~~~~~\var{hk_{vrf}} \leteq \hashKey{vrfVk} \\
& ~~~~~~~~~~\var{ss} \leteq \slotToSeed{(\bslot{bhb})} \\
& ~~~~~~~~~~\var{vrfVk} \leteq \fun{bvkvrf}~\var{bhb} \\
\end{align*}
%
\begin{align*}
& \fun{praosVrfChecks} \in \Seed \to \PoolDistr \to \unitInterval \to \BHBody \to \Bool \\
& \fun{praosVrfChecks}~\eta_0~\var{pd}~\var{f}~\var{bhb} = \\
& \begin{array}{cl}
~~~~ & \var{hk}\mapsto (\sigma,~\var{hk_{vrf}})\in\var{pd} \\
~~~~ \land & \fun{vrfChecks}~\eta_0~\var{bhb} \\
~~~~ \land & \fun{bleader}~\var{bhb} < 1 - (1 - f)^{\sigma} \\
\end{array} \\
& ~~~~\where \\
& ~~~~~~~~~~\var{hk} \leteq \hashKey{(\bvkcold bhb)} \\
& ~~~~~~~~~~\var{hk_{vrf}} \leteq \hashKey{(\fun{bvkvrf}~\var{bhb})} \\
\end{align*}
%
\begin{align*}
& \fun{pbftVrfChecks} \in \KeyHash_{vrf} \to \Seed \to \BHBody \to \Bool \\
& \fun{pbftVrfChecks}~\var{vrfh}~\eta_0~~\var{bhb} = \\
& \begin{array}{cl}
~~~~ & \var{vrfh} = \hashKey{(\fun{bvkvrf}~\var{bhb})} \\
~~~~ \land & \fun{vrfChecks}~\eta_0~\var{bhb} \\
\end{array} \\
\end{align*}
\label{fig:vrf-checks}
\end{figure}

Expand Down Expand Up @@ -1171,14 +1188,16 @@ \subsection{Overlay Schedule}
responsible for producing the block.
\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.
\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 in Equation~\ref{eq:decentralized} closely.
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}$.
Expand All @@ -1189,12 +1208,16 @@ \subsection{Overlay Schedule}
\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{vrfChecks}$ returns true, then we know that the cold key in the block header was a
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}
Expand All @@ -1205,7 +1228,7 @@ \subsection{Overlay Schedule}
\var{osched} & \Slot\mapsto\KeyHashGen^? & \text{OBFT overlay schedule} \\
\eta_0 & \Seed & \text{epoch nonce} \\
\var{pd} & \PoolDistr & \text{pool stake distribution} \\
\var{genDelegs} & \KeyHashGen\mapsto\KeyHash & \text{genesis key delegations} \\
\var{genDelegs} & \GenesisDelegation & \text{genesis key delegations} \\
\end{array}
\right)
\end{equation*}
Expand All @@ -1232,7 +1255,9 @@ \subsection{Overlay Schedule}
\\
\bslot bhb \mapsto \var{gkh}\in\var{osched}
&
\var{gkh}\mapsto\var{vkh}\in\var{genDelegs}
\var{gkh}\mapsto(\var{vkh},~\var{vrfh})\in\var{genDelegs}
\\~\\
\fun{pbftVrfChecks}~\var{vrfh}~\eta_0~\var{bhb}
\\~\\
{
{\begin{array}{c}
Expand Down Expand Up @@ -1270,7 +1295,7 @@ \subsection{Overlay Schedule}
\vdash\var{cs}\trans{\hyperref[fig:rules:ocert]{ocert}}{\var{bh}}\var{cs'}
}
\\~\\
\fun{vrfChecks}~\eta_0~\var{pd}~\ActiveSlotCoeff~\var{bhb}
\fun{praosVrfChecks}~\eta_0~\var{pd}~\ActiveSlotCoeff~\var{bhb}
}
{
{\begin{array}{c}
Expand All @@ -1290,18 +1315,31 @@ \subsection{Overlay Schedule}
\label{fig:rules:overlay}
\end{figure}

The OVERLAY rule has four predicate failures:
The OVERLAY rule has nine predicate failures:
\begin{itemize}
\item In the case of the slot not being part of a OBFT schedule, if the VRF
leader check does not verify, there is a \emph{NotPraosLeader} failure.
\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 key, but this key is not in the genesis delegation map, there is a
\emph{NoGenesisStaking} 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{NoGenesisColdKey} failure.
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
Expand Down Expand Up @@ -1892,7 +1930,7 @@ \subsection{Byron to Shelley Transition}
%
\begin{align*}
& \fun{initialShelleyState} \in \LastAppliedBlock^? \to \Epoch \to \UTxO
\to \Coin \to (\KeyHashGen \mapsto \KeyHash) \\
\to \Coin \to \GenesisDelegation \\
& ~~~ \to (\Slot\mapsto\KeyHashGen^?)
\to \PParams \to \Seed \to \ChainState \\
& \fun{initialShelleyState}~
Expand Down Expand Up @@ -1985,7 +2023,7 @@ \subsection{Byron to Shelley Transition}
\var{lab} \\
\end{array}
\right) \\
& ~~~~\where cs = \{\var{hk}\mapsto 0~\mid~\var{hk}\in\range{genDelegs}\} \\
& ~~~~\where cs = \{\var{hk}\mapsto 0~\mid~(\var{hk},~\wcard)\in\range{genDelegs}\} \\
\end{align*}

\caption{Initial Shelley States}
Expand All @@ -1999,18 +2037,18 @@ \subsection{Byron to Shelley Transition}
\emph{Byron to Shelley Transition}
%
\begin{align*}
& \fun{toShelley} \in \CEState \to \BlockNo \to \ChainState \\
& \fun{toShelley} \in \CEState \to \GenesisDelegation \to \BlockNo \to \ChainState \\
& \fun{toShelley}~
\left(
\begin{array}{c}
\var{s_{last}} \\
\wcard \\
\var{h} \\
(\var{utxo},~\var{reserves}) \\
\var{ds} \\
\wcard \\
\var{us}
\end{array}
\right)~\var{bn}
\right)~\var{bn}~\var{gd}
=
\fun{initialShelleyState}~
\left(
Expand All @@ -2028,7 +2066,6 @@ \subsection{Byron to Shelley Transition}
\right) \\
& ~~~~\where \\
& ~~~~~~~~~e = \epoch{s_{last}} \\
& ~~~~~~~~~gd = \fun{dms}~\var{ds} \\
& ~~~~~~~~~pp = \pps{us} \\
\end{align*}

Expand Down
33 changes: 24 additions & 9 deletions shelley/chain-and-ledger/formal-spec/delegation.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -166,7 +166,7 @@ \subsection{Delegation Definitions}
\fun{retire} & \DCertRetirePool \to \Epoch
& \text{epoch of pool retirement}
\\
\fun{genesisDeleg} & \DCertGen \to (\KeyHashGen,~\KeyHash)
\fun{genesisDeleg} & \DCertGen \to (\KeyHashGen,~\KeyHash,~\KeyHash_{vrf})
& \text{genesis delegation}
\\
\fun{moveRewards} & \DCertMir \to (\StakeCredential \mapsto \Coin)
Expand Down Expand Up @@ -270,6 +270,8 @@ \subsection{Delegation Transitions}
\begin{array}{r@{~\in~}l@{\qquad=\qquad}lr}
\var{stakeCred} & \StakeCredential & (\KeyHash_{stake} \uniondistinct
\HashScr) \\
\var{fGenDelegs} & \FutGenesisDelegation
& (\Slot\times\KeyHashGen)\mapsto(\KeyHash\times\KeyHash_{vrf}) \\
\end{array}
\end{equation*}
%
Expand All @@ -283,8 +285,8 @@ \subsection{Delegation Transitions}
\var{rewards} & \AddrRWD \mapsto \Coin & \text{rewards}\\
\var{delegations} & \StakeCredential \mapsto \KeyHash_{pool} & \text{delegations}\\
\var{ptrs} & \Ptr \mapsto \StakeCredential & \text{pointer to stake credential}\\
\var{fGenDelegs} & (\Slot\times\KeyHashGen) \mapsto \KeyHash & \text{future genesis key delegations}\\
\var{genDelegs} & \KeyHashGen \mapsto \KeyHash & \text{genesis key delegations}\\
\var{fGenDelegs} & \FutGenesisDelegation & \text{future genesis key delegations}\\
\var{genDelegs} & \GenesisDelegation & \text{genesis key delegations}\\
\var{i_{rwd}} & \StakeCredential \mapsto \Coin & \text{instantaneous rewards}\\
\end{array}
\right)
Expand Down Expand Up @@ -534,11 +536,23 @@ \subsection{Delegation Rules}
\inference[Deleg-Gen]
{
\var{c}\in \DCertGen
& (\var{gkh},~\var{vkh})\leteq\fun{genesisDeleg}~{c}
& (\var{gkh},~\var{vkh},~\var{vrf})\leteq\fun{genesisDeleg}~{c}
\\
s'\leteq\var{slot}+\StabilityWindow
& \var{gkh}\in\dom{genDelegs}
& \var{vkh}\notin\range{genDelegs}
\\~\\
{
\begin{array}{ l @{~\leteq~\{} c @{~\mid~} r @{\mapsto} l @{,~\var{g}\neq\var{gkh}\}} }
\var{currentOtherColdKeyHashes} & \var{k} & \var{g} & (\var{k},~\wcard) \\
\var{currentOtherVrfKeyHashes} & \var{v} & \var{g} & (\wcard,~\var{v}) \\
\var{futureOtherColdKeyHashes} & \var{k} & (\var{g},~\wcard) & (\var{k},~\wcard) \\
\var{futureOtherVrfKeyHashe} & \var{v} & (\var{g},~\wcard) & (\wcard,~\var{v}) \\
\end{array}
}
\\
\var{vkh}\notin\var{currentOtherColdKeyHashes}\union\var{futureOtherColdKeyHashes} \\
\var{vrf}\notin\var{currentOtherVrfKeyHashes}\union\var{futureOtherVrfKeyHashe} \\
\var{fdeleg}\leteq\{(\var{s'},~\var{gkh}) \mapsto (\var{vkh},~\var{vrf})\}
}
{
\begin{array}{r}
Expand All @@ -565,8 +579,9 @@ \subsection{Delegation Rules}
\var{rewards} \\
\var{delegations} \\
\var{ptrs} \\
\varUpdate{\var{fGenDelegs}} & \varUpdate{\unionoverrideRight}
& \varUpdate{\{(\var{s'},~\var{gkh}) \mapsto \var{vkh}\}} \\
\varUpdate{\var{fGenDelegs}}
& \varUpdate{\unionoverrideRight}
& \varUpdate{fdeleg} \\
\var{genDelegs} \\
\var{i_{rwd}}
\end{array}
Expand Down Expand Up @@ -667,7 +682,7 @@ \subsection{Stake Pool Rules}
\item The pool's parameters are stored.
\end{itemize}
\item Stake pool parameter updates are handled by \cref{eq:pool-rereg}.
This rules, which also matches on the certificate type $\type{DCertRegPool}$,
This rule, which also matches on the certificate type $\type{DCertRegPool}$,
is distinguished from \cref{eq:pool-reg} by the requirement that the pool be registered.

Unlike the initial stake pool registrations, the pool parameters will not change
Expand Down Expand Up @@ -742,7 +757,7 @@ \subsection{Stake Pool Rules}
}
\end{equation}

\begin{equation}\label{eq:pool-rereg-late}
\begin{equation}\label{eq:pool-rereg}
\inference[Pool-reReg]
{
\var{c}\in\DCertRegPool
Expand Down
2 changes: 2 additions & 0 deletions shelley/chain-and-ledger/formal-spec/epoch.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -555,6 +555,7 @@ \subsection{Pool Reaping Transition}
\var{delegations} \\
\var{ptrs} \\
\var{genDelegs} \\
\var{fGenDelegs} \\
\var{i_{rwd}} \\
~ \\
\var{stpools} \\
Expand All @@ -580,6 +581,7 @@ \subsection{Pool Reaping Transition}
\varUpdate{\var{delegations}} & \varUpdate{\subtractrange} & \varUpdate{\var{retired}} \\
\var{ptrs} \\
\var{genDelegs} \\
\var{fGenDelegs} \\
\var{i_{rwd}}\\
~ \\
\varUpdate{\var{retired}} & \varUpdate{\subtractdom} & \varUpdate{\var{stpools}} \\
Expand Down
2 changes: 2 additions & 0 deletions shelley/chain-and-ledger/formal-spec/ledger-spec.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -98,6 +98,8 @@
\newcommand{\MetaDataHash}{\ensuremath{\type{MetaDataHash}}}
\newcommand{\PPUpdate}{\type{PPUpdate}}
\newcommand{\Update}{\type{Update}}
\newcommand{\GenesisDelegation}{\type{GenesisDelegation}}
\newcommand{\FutGenesisDelegation}{\type{FutGenesisDelegation}}

\newcommand{\DCert}{\type{DCert}}
\newcommand{\DCertRegKey}{\type{DCert_{regkey}}}
Expand Down
Loading