From 0e3022496382b333708abd7ebbf740a7f411e9ab Mon Sep 17 00:00:00 2001 From: Jared Corduan Date: Mon, 6 May 2019 13:08:38 -0400 Subject: [PATCH] small edits from 20190503 review --- .../chain-and-ledger/formal-spec/chain.tex | 109 ++++++++++-------- .../formal-spec/delegation.tex | 6 +- 2 files changed, 62 insertions(+), 53 deletions(-) diff --git a/shelley/chain-and-ledger/formal-spec/chain.tex b/shelley/chain-and-ledger/formal-spec/chain.tex index 2946bcd2426..81077dd9f41 100644 --- a/shelley/chain-and-ledger/formal-spec/chain.tex +++ b/shelley/chain-and-ledger/formal-spec/chain.tex @@ -30,7 +30,7 @@ \section{Blockchain layer} \newcommand{\hsig}[1]{\fun{hsig}~\var{#1}} \newcommand{\bprev}[1]{\fun{bprev}~\var{#1}} \newcommand{\bhash}[1]{\fun{bhash}~\var{#1}} -\newcommand{\bissuer}[1]{\fun{bissuer}~\var{#1}} +\newcommand{\bvkcold}[1]{\fun{bvkcold}~\var{#1}} \newcommand{\bseedl}[1]{\fun{bseed}_{\ell}~\var{#1}} \newcommand{\bprfn}[1]{\fun{bprf}_{n}~\var{#1}} \newcommand{\bseedn}[1]{\fun{bseed}_{n}~\var{#1}} @@ -44,7 +44,7 @@ \section{Blockchain layer} \newcommand{\BHeaderEnv}{\type{BHeaderEnv}} \newcommand{\BHeaderState}{\type{BHeaderState}} \newcommand{\VRFEnv}{\type{VRFEnv}} -\newcommand{\DSliderEnv}{\type{DSliderEnv}} +\newcommand{\OverlayEnv}{\type{OverlayEnv}} \newcommand{\VRFState}{\type{VRFState}} \newcommand{\OCertState}{\type{OCertState}} \newcommand{\NewEpochEnv}{\type{NewEpochEnv}} @@ -140,7 +140,8 @@ \subsection{Block Definitions} \left( \begin{array}{r@{~\in~}lr} \var{vk_{hot}} & \VKeyEv & \text{operational (hot) key}\\ - \var{n} & \N & \text{counter}\\ + \var{vk_{cold}} & \VKey & \text{cold key}\\ + \var{n} & \N & \text{certificate issue number}\\ c_0 & \KESPeriod & \text{start KES period}\\ \sigma & \Sig & \text{cold key signature}\\ \end{array} @@ -202,8 +203,8 @@ \subsection{Block Definitions} \fun{bhbody} & \BHeader \to \BHBody \\ \fun{hsig} & \BHeader \to \Sig\\ \fun{bbody} & \Block \to \seqof{\Tx} \\ + \fun{bvkcold} & \BHBody \to \VKey\\ \fun{bprev} & \BHBody \to \HashHeader\\ - \fun{bissuer} & \BHBody \to \VKey\\ \fun{bslot} & \BHBody \to \Slot\\ \fun{bnonce} & \BHBody \to \Seed\\ \fun{\bprfn{}} & \BHBody \to \Proof\\ @@ -360,11 +361,11 @@ \subsection{New Epoch Transition} (\wcard,~\var{pstake_{set}},~\wcard,~\wcard,~\wcard,~\wcard) & \var{ss} \\ (\var{stake}, \var{delegs}) & \var{pstake_{set}} \\ total & \sum_{\_ \mapsto c\in\var{stake}} c \\ - \var{pd'} & \fun{aggregate_{+}}~\var{delegs}^{-1}\circ + \var{pd'} & \fun{aggregate_{+}}~\left(\var{delegs}^{-1}\circ \left\{ (\var{hk}, \frac{\var{c}}{\var{total}}) \vert (\var{hk}, \var{c}) \in \var{stake} - \right\} \\ + \right\}\right) \\ \var{osched'} & \fun{overlaySchedule}~\eta_1~(\activeSlotCoeff{pp})~(\fun{d}~{pp})\\ \var{es''} & \var{es'}\unionoverrideRight\{us'\} \end{array}} @@ -527,7 +528,7 @@ \subsection{Operational Certificate Transition} \item The stake pools map \var{stpools}. \item The pool parameters \var{poolParams}. \item The map of retiring stake pools to epochs \var{retiring}. -\item The mapping \var{cs} of operational certificate counters. +\item The mapping \var{cs} of certificate issue numbers. \item The mapping of genesis keys to operational keys. \end{itemize} @@ -557,8 +558,8 @@ \subsection{Operational Certificate Transition} header body \var{bhb} we first extract the following: \begin{itemize} -\item The operational certificate, consisting of the hot key \var{vk_{hot}}, the - KES period number \var{n}, the KES period start \var{c_0} and the cold key + \item The operational certificate, consisting of the hot key \var{vk_{hot}}, the cold key + \var{vk_{cold}}, the KES period number \var{n}, the KES period start \var{c_0} and the cold key signature. \item The block header issuer verification key \var{vk_{cold}}. \item The hash \var{hk} of \var{vk_{cold}}. @@ -570,7 +571,7 @@ \subsection{Operational Certificate Transition} \begin{itemize} \item The KES period start \var{c_0} is greater than or equal to the KES period of the slot of the block header body and less than 90 KES periods after \var{c_0}. -\item \var{hk} exists as key in the mapping of certificate counters to a KES +\item \var{hk} exists as key in the mapping of certificate issues numbers to a KES period \var{m} and that period is less than or equal to \var{n}. \item The signature $sigma$ can be verified with the cold verification key \var{vk_{cold}}. @@ -586,9 +587,7 @@ \subsection{Operational Certificate Transition} \begin{equation}\label{eq:ocert} \inference[OCert] { - (\var{vk_{hot}},~n,~c_{0},~\sigma) \leteq \bocert{bhb} - & - \var{vk_{cold}} \leteq \bissuer{bhb} + (\var{vk_{hot}},~\var{vk_{cold}},~n,~c_{0},~\sigma) \leteq \bocert{bhb} & \var{hk} \leteq \hashKey{vk_{cold}} \\~\\ @@ -606,22 +605,30 @@ \subsection{Operational Certificate Transition} \var{gkeys} \vdash \left( - \begin{array}{r} - \var{stpools} \\ - \var{poolParams} \\ - \var{retiring} \\ - \var{cs} \\ + \begin{array}{c} + \left( + \begin{array}{c} + \var{stpools} \\ + \var{poolParams} \\ + \var{retiring} \\ + \var{cs} \\ + \end{array} + \right)\\ \\ \var{dms} \\ \end{array} \right) \trans{ocert}{\var{bhb}} \left( - \begin{array}{rcl} - \var{stpools} \\ - \var{poolParams} \\ - \var{retiring} \\ - \varUpdate{\var{cs}\unionoverrideRight\{\var{hk}\mapsto n\}} \\ + \begin{array}{c} + \left( + \begin{array}{c} + \var{stpools} \\ + \var{poolParams} \\ + \var{retiring} \\ + \varUpdate{\var{cs}\unionoverrideRight\{\var{hk}\mapsto n\}} \\ + \end{array} + \right)\\ \\ \varUpdate{\var{dms}\unionoverrideRight d} \\ \end{array} @@ -834,9 +841,9 @@ \subsection{Verifiable Random Function} & f \leteq \activeSlotCoeff{pp} \\ - \var{vk} \leteq \bissuer bhb + \var{vk} \leteq \bvkcold bhb & - \var{ss} \leteq \slotToSeed{\bslot{bhb}} + \var{ss} \leteq \slotToSeed{(\bslot{bhb})} & \var{hk} \leteq \hashKey{vk} \\~\\ @@ -900,14 +907,14 @@ \subsection{Verifiable Random Function} \clearpage -\subsection{Decentralization Slider} -\label{sec:decentralization-slider} +\subsection{Overlay Schedule} +\label{sec:overlay-schedule} The transition from the boostrap 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{DSLIDE}$, covers this mechanism. +The transition system introduced in this section, $\type{OVERLAY}$, covers this mechanism. The environments for this transition is: \begin{itemize} @@ -921,9 +928,9 @@ \subsection{Decentralization Slider} \end{itemize} \begin{figure} - \emph{DSlider environments} + \emph{Overlay environments} \begin{equation*} - \DSliderEnv = + \OverlayEnv = \left( \begin{array}{r@{~\in~}lr} \var{ve} & \VRFEnv & \text{VRF environment} \\ @@ -932,13 +939,13 @@ \subsection{Decentralization Slider} \right) \end{equation*} % - \emph{DSlider Transitions} + \emph{Overlay Transitions} \begin{equation*} - \_ \vdash \var{\_} \trans{dslider}{\_} \var{\_} \subseteq - \powerset (\DSliderEnv \times \BHeaderState \times \BHeader \times \BHeaderState) + \_ \vdash \var{\_} \trans{overlay}{\_} \var{\_} \subseteq + \powerset (\OverlayEnv \times \BHeaderState \times \BHeader \times \BHeaderState) \end{equation*} - \caption{DSlider transition-system types} - \label{fig:ts-types:decent-slider} + \caption{Overlay transition-system types} + \label{fig:ts-types:overlay} \end{figure} \begin{figure}[ht] @@ -985,7 +992,7 @@ \subsection{Decentralization Slider} \var{h} \\ \var{s_\ell} \\ \end{array}\right)} - \trans{dslider}{\var{bh}} + \trans{overlay}{\var{bh}} {\left(\begin{array}{c} \varUpdate{\var{h}'} \\ \varUpdate{\var{s_\ell}'} \\ @@ -1029,7 +1036,7 @@ \subsection{Decentralization Slider} \var{h} \\ \var{s_\ell} \\ \end{array}\right)} - \trans{dslider}{\var{bh}} + \trans{overlay}{\var{bh}} {\left(\begin{array}{c} \varUpdate{\var{h}'} \\ \varUpdate{\var{s_\ell}'} \\ @@ -1037,8 +1044,8 @@ \subsection{Decentralization Slider} } \end{equation} - \caption{DSlider rules} - \label{fig:rules:decent-slider} + \caption{Overlay rules} + \label{fig:rules:overlay} \end{figure} \subsection{Block Body Transition} @@ -1130,14 +1137,12 @@ \subsection{Block Body Transition} & \var{bhb} \leteq \bhbody\bheader{block} & - \var{hk} \leteq \hashKey\bissuer{bhb} + \var{hk} \leteq \hashKey\bvkcold{bhb} \\~\\ \bBodySize{txs} = \hBbsize{bhb} & \fun{hash}~{txs} = \bbodyhash{bhb} \\~\\ - \var{hk}\mapsto n\in (b \unionoverrideLeft \{\var{kh}\mapsto 0\}) - \\~\\ { \left( {\begin{array}{c} @@ -1378,7 +1383,7 @@ \subsection{Chain Transition} \var{pd} \\ \var{osched} \\ \end{array}\right)} - \trans{newepoch}{\var{e}} + \trans{newepoch}{\epoch{s}} {\left(\begin{array}{c} \var{e_\ell}' \\ \eta_0' \\ @@ -1422,11 +1427,15 @@ \subsection{Chain Transition} { \left( {\begin{array}{c} - \var{s_{now}} \\ - \var{pp}' \\ - \eta_0' \\ - \var{pd}' \\ - \var{stpools} \\ + \left( + {\begin{array}{c} + \var{s_{now}} \\ + \var{pp}' \\ + \eta_0' \\ + \var{pd}' \\ + \var{stpools} \\ + \end{array}} + \right) \\ \var{osched'} \\ \end{array}} @@ -1436,7 +1445,7 @@ \subsection{Chain Transition} \var{h} \\ \var{s_\ell} \\ \end{array}\right)} - \trans{dslider}{\var{bh}} + \trans{overlay}{\var{bh}} {\left(\begin{array}{c} \var{h}' \\ \var{s_\ell}' \\ @@ -1604,7 +1613,7 @@ \subsection{Byron to Shelley Transition} \Nothing \\ \emptyset \\ \emptyset \\ - \dom{dms} \\ + \dom{(\fun{dms}~\var{ds})} \\ \end{array} \right) \end{align*} diff --git a/shelley/chain-and-ledger/formal-spec/delegation.tex b/shelley/chain-and-ledger/formal-spec/delegation.tex index b77ded2030d..0d30ae64d7f 100644 --- a/shelley/chain-and-ledger/formal-spec/delegation.tex +++ b/shelley/chain-and-ledger/formal-spec/delegation.tex @@ -193,8 +193,8 @@ \subsection{Delegation Transitions} their costs and margin. \item $\var{retiring}$ tracks stake pool retirements, using a map from hashkeys to the epoch in which it will retire. - \item $\var{cs}$ stores the latest operational certificate counter used for each pool. - The counters are used the operation certificate transition in Figure~\ref{fig:rules:ocert}. + \item $\var{cs}$ stores the latest operational certificate issues numbers used for each pool. + The numbers are used the operation certificate transition in Figure~\ref{fig:rules:ocert}. \end{itemize} \end{itemize} @@ -226,7 +226,7 @@ \subsection{Delegation Transitions} \var{poolParams} & \HashKey_{pool} \mapsto \PoolParam & \text{registered pools to pool parameters}\\ \var{retiring} & \HashKey_{pool} \mapsto \Epoch & \text{retiring stake pools}\\ - \var{cs} & \HashKey_{pool} \mapsto \N & \text{operational certificate counters}\\ + \var{cs} & \HashKey_{pool} \mapsto \N & \text{certificate issue numbers}\\ \end{array}\right) \end{array} \end{equation*}