Skip to content
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

small edits from 20190503 review #451

Merged
merged 1 commit into from
May 7, 2019
Merged

small edits from 20190503 review #451

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
109 changes: 59 additions & 50 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 @@ -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}}
Expand All @@ -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}}
Expand Down Expand Up @@ -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}
Expand Down Expand Up @@ -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\\
Expand Down Expand Up @@ -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}}
Expand Down Expand Up @@ -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}

Expand Down Expand Up @@ -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}}.
Expand All @@ -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}}.
Expand All @@ -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}}
\\~\\
Expand All @@ -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}
Expand Down Expand Up @@ -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}
\\~\\
Expand Down Expand Up @@ -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}
Expand All @@ -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} \\
Expand All @@ -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]
Expand Down Expand Up @@ -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}'} \\
Expand Down Expand Up @@ -1029,16 +1036,16 @@ \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}'} \\
\end{array}\right)}
}
\end{equation}

\caption{DSlider rules}
\label{fig:rules:decent-slider}
\caption{Overlay rules}
\label{fig:rules:overlay}
\end{figure}

\subsection{Block Body Transition}
Expand Down Expand Up @@ -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}
Expand Down Expand Up @@ -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' \\
Expand Down Expand Up @@ -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}}
Expand All @@ -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}' \\
Expand Down Expand Up @@ -1604,7 +1613,7 @@ \subsection{Byron to Shelley Transition}
\Nothing \\
\emptyset \\
\emptyset \\
\dom{dms} \\
\dom{(\fun{dms}~\var{ds})} \\
\end{array}
\right)
\end{align*}
Expand Down
6 changes: 3 additions & 3 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 @@ -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}

Expand Down Expand Up @@ -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*}
Expand Down