Skip to content

Commit

Permalink
removing application versions
Browse files Browse the repository at this point in the history
  • Loading branch information
@JaredCorduan
JaredCorduan committed Mar 24, 2020
1 parent 06f0e47 commit 30ae1be
Show file tree
Hide file tree
Showing 10 changed files with 119 additions and 634 deletions.
28 changes: 12 additions & 16 deletions shelley/chain-and-ledger/formal-spec/chain.tex
View file
Expand Up @@ -288,13 +288,15 @@ \subsection{MIR Transition}
\var{acnt} \\
\var{ss} \\
(\var{us},~(\var{ds},~\var{ps})) \\
\var{prevPP} \\
\var{pp} \\
\end{array}\right)}
\trans{mir}{}
{\left(\begin{array}{c}
\varUpdate{\var{acnt'}} \\
\var{ss} \\
(\var{us},~(\varUpdate{\var{ds'}},~\var{ps})) \\
\var{prevPP} \\
\var{pp} \\
\end{array}\right)}
}
Expand Down Expand Up @@ -326,13 +328,15 @@ \subsection{MIR Transition}
\var{acnt} \\
\var{ss} \\
(\var{us},~(\var{ds},~\var{ps})) \\
\var{prevPP} \\
\var{pp} \\
\end{array}\right)}
\trans{mir}{}
{\left(\begin{array}{c}
\var{acnt} \\
\var{ss} \\
(\var{us},~(\varUpdate{\var{ds'}},~\var{ps})) \\
\var{prevPP} \\
\var{pp} \\
\end{array}\right)}
}
Expand Down Expand Up @@ -481,7 +485,7 @@ \subsection{New Epoch Transition}
}
\\~\\
{\begin{array}{r@{~\leteq~}l}
(\var{acnt},~\var{ss},~\var{ls}, \var{pp}) & \var{es'''} \\
(\var{acnt},~\var{ss},~\var{ls},~\wcard,~\var{pp}) & \var{es'''} \\
(\wcard,~\var{pstake_{set}},~\wcard,~\wcard) & \var{ss} \\
(\var{stake},~\var{delegs},~\var{poolPrms}) & \var{pstake_{set}} \\
total & \sum_{\_ \mapsto c\in\var{stake}} c \\
Expand Down Expand Up @@ -1704,7 +1708,7 @@ \subsection{Chain Transition}
\leteq\var{nes} \\
(\var{e_2},~\wcard,~\var{b_{cur}},~\var{es},~\wcard,~\var{pd},\var{osched})
\leteq\var{nes'} \\
(\var{acnt},~\wcard,\var{ls},~\var{pp'})\leteq\var{es}\\
(\var{acnt},~\wcard,\var{ls},~\wcard,~\var{pp'})\leteq\var{es}\\
( \wcard,
( (\wcard,~\wcard,~\wcard,~\wcard,~\wcard,~\var{genDelegs}),~
(\wcard,~\wcard,~\wcard)))\leteq\var{ls}\\
Expand Down Expand Up @@ -1826,7 +1830,8 @@ \subsection{Byron to Shelley Transition}
\begin{align*}
& \fun{initialShelleyState} \in \Slot \to \BlockNo \to \Epoch \to\HashHeader \to \UTxO
\to \Coin \\
& ~~~ \to (\KeyHashGen \mapsto \KeyHash) \to (\Slot\mapsto\KeyHashGen^?) \to \Applications \to \PParams \to \ChainState \\
& ~~~ \to (\KeyHashGen \mapsto \KeyHash) \to (\Slot\mapsto\KeyHashGen^?)
\to \PParams \to \ChainState \\
& \fun{initialShelleyState}~
\left(
\begin{array}{c}
Expand All @@ -1838,7 +1843,6 @@ \subsection{Byron to Shelley Transition}
\var{reserves} \\
\var{genDelegs} \\
\var{os} \\
\var{apps} \\
\var{pp} \\
\end{array}
\right)
Expand Down Expand Up @@ -1875,14 +1879,7 @@ \subsection{Byron to Shelley Transition}
\var{utxo} \\
0 \\
0 \\
\left(
\begin{array}{c}
\emptyset \\
\emptyset \\
\emptyset \\
\var{apps}\\
\end{array}
\right) \\
\emptyset \\
\end{array}
\right) \\
\left(
Expand All @@ -1909,6 +1906,7 @@ \subsection{Byron to Shelley Transition}
\end{array}
\right) \\
\var{pp} \\
\var{pp} \\
\end{array}
\right) \\
\\
Expand Down Expand Up @@ -1941,7 +1939,7 @@ \subsection{Byron to Shelley Transition}
\emph{Byron to Shelley Transition}
%
\begin{align*}
& \fun{toShelley} \in \CEState \to \ChainState \\
& \fun{toShelley} \in \CEState \to \BlockNo \to \ChainState \\
& \fun{toShelley}~
\left(
\begin{array}{c}
Expand All @@ -1952,7 +1950,7 @@ \subsection{Byron to Shelley Transition}
\var{ds} \\
\var{us}
\end{array}
\right)
\right)~\var{bn}
=
\fun{initialShelleyState}~
\left(
Expand All @@ -1965,13 +1963,11 @@ \subsection{Byron to Shelley Transition}
\var{reserves} \\
\var{gd} \\
\overlaySchedule{e}{(\dom{gd})}{pp} \\
\fun{avs}~\var{us} \\
\var{pp} \\
\end{array}
\right) \\
& ~~~~\where \\
& ~~~~~~~~~e = \epoch{s_{last}} \\
& ~~~~~~~~~bn = \mathsf{TODO} \\
& ~~~~~~~~~gd = \fun{dms}~\var{ds} \\
& ~~~~~~~~~pp = \pps{us} \\
\end{align*}
Expand Down
46 changes: 36 additions & 10 deletions shelley/chain-and-ledger/formal-spec/epoch.tex
View file
Expand Up @@ -436,7 +436,7 @@ \subsection{Snapshot Transition}
\var{utxo} \\
\var{deposits} \\
\var{fees} \\
\var{up} \\
\var{pup} \\
\end{array}
\right)
\trans{snap}{e}
Expand All @@ -450,7 +450,7 @@ \subsection{Snapshot Transition}
\var{utxo} \\
\varUpdate{\var{oblg}} \\
\varUpdate{\var{fees} + \var{decayed}} \\
\var{up} \\
\var{pup} \\
\end{array}
\right)
}
Expand Down Expand Up @@ -804,6 +804,12 @@ \subsection{Complete Epoch Boundary Transition}
The transition has no evironment.
The state is made up of the the accounting state, the snapshots, the ledger state and the
protocol parameters.
The transition uses a helper function $\fun{votedValue}$ which returns
the consensus value of update proposals in the event that consensus it met.
\textbf{Note that} $\fun{votedValue}$
\textbf{is only well-defined if } $\Quorum$
\textbf{is greater than half the number of core nodes, i.e.}
$\Quorum > |\var{genDelegs}|/2$ \textbf{.}

%%
%% Figure - Epoch Defs
Expand All @@ -817,6 +823,7 @@ \subsection{Complete Epoch Boundary Transition}
\var{acnt} & \Acnt & \text{accounting}\\
\var{ss} & \Snapshots & \text{snapshots}\\
\var{ls} & \LState & \text{ledger state}\\
\var{prevPp} & \PParams & \text{previous protocol parameters}\\
\var{pp} & \PParams & \text{protocol parameters}\\
\end{array}
\right)
Expand All @@ -837,13 +844,25 @@ \subsection{Complete Epoch Boundary Transition}
\end{array}
\end{equation*}
%
\emph{Helper Functions}
\begin{align*}
& \fun{votedValue} \in (\KeyHashGen\mapsto\PParamsUpdate) \to \PParamsUpdate^?\\
& \fun{votedValue}~\var{vs} =
\begin{cases}
p & \exists p\in\range{vs}~(|vs\restrictrange p|\geq \Quorum) \\
\Nothing & \text{otherwise} \\
\end{cases}
\end{align*}
%
\caption{Epoch transition-system types}
\label{fig:ts-types:epoch}
\end{figure}


The epoch transition rule calls $\mathsf{SNAP}$, $\mathsf{POOLREAP}$ and $\mathsf{NEWPP}$
in sequence.
in sequence. It also store the previous protocol parameters in $\var{prevPp}$.
The previous protocol parameters will be used for the reward calculation in the upcoming epoch,
note that they correspond to the epoch for which the reward are being calculated.
The ordering of these rules is important.
The stake pools which will be reaped during the $\mathsf{POOLREAP}$ transition must still be a
part of the new snapshot, and so $\mathsf{SNAP}$ must occur before $\mathsf{POOLREAP}$.
Expand Down Expand Up @@ -913,9 +932,9 @@ \subsection{Complete Epoch Boundary Transition}
}
\right)
\\~\\~\\
\var{(\wcard,~\wcard,~\wcard,~(\var{ppup},~\wcard,~\wcard,~\wcard))}\leteq\var{utxoSt'}\\
\var{(\wcard,~\wcard,~\wcard,~\var{pup})}\leteq\var{utxoSt'}\\
\var{pp_{new}}\leteq\var{pp}\unionoverrideRight
\fun{votedValue_{(\Ppm\to\mathsf{T_{ppm}})}}~\var{ppup}\\
\fun{votedValue}~\var{pup}\\
{
\begin{array}{r}
\var{pp_{new}}\\
Expand Down Expand Up @@ -953,6 +972,7 @@ \subsection{Complete Epoch Boundary Transition}
\var{acnt} \\
\var{ss} \\
\var{ls} \\
\var{prevPp} \\
\var{pp} \\
\end{array}
\right)
Expand All @@ -962,6 +982,7 @@ \subsection{Complete Epoch Boundary Transition}
\varUpdate{\var{acnt''}} \\
\varUpdate{\var{ss'}} \\
\varUpdate{\var{ls'}} \\
\varUpdate{\var{pp}} \\
\varUpdate{\var{pp'}} \\
\end{array}
\right)
Expand Down Expand Up @@ -1290,6 +1311,9 @@ \subsection{Reward Update Calculation}

The $\fun{createRUpd}$ function does the following:
\begin{itemize}
\item Note that for all the calculations below, we use the previous protocol parameters
$\var{prevPp}$, which correspondings the the parameters during the epoch for which we
are being created for.
\item First we calculate the change to the reserves,
as determined by the $\rho$ protocol parameter.
\item Next we calculate $\var{rewardPot}$, the total amount of coin available for rewards this
Expand Down Expand Up @@ -1339,7 +1363,7 @@ \subsection{Reward Update Calculation}
& \createRUpd{b}{es}{total} = \left(
\Delta t_1+\Delta t_2,-~\Delta r,~\var{rs},~-\var{feeSS}\right) \\
& ~~~\where \\
& ~~~~~~~(\var{acnt},~\var{ss},~\var{ls},~\var{pp}) = \var{es} \\
& ~~~~~~~(\var{acnt},~\var{ss},~\var{ls},~\var{prevPp},~\wcard) = \var{es} \\
& ~~~~~~~(\wcard,~\wcard,~\var{pstake_{go}},~\var{poolsSS},~\var{feeSS}) = \var{ss}\\
& ~~~~~~~(\var{stake},~\var{delegs}) = \var{pstate_{go}} \\
& ~~~~~~~(\wcard,~\var{reserves}) = \var{acnt} \\
Expand All @@ -1350,15 +1374,15 @@ \subsection{Reward Update Calculation}
\wcard
\right)
\right) = \var{ls} \\
& ~~~~~~~\Delta r = \floor*{\min(1,\eta) \cdot (\fun{rho}~{pp}) \cdot
& ~~~~~~~\Delta r = \floor*{\min(1,\eta) \cdot (\fun{rho}~\var{prevPp}) \cdot
\var{reserves}}
\\
& ~~~~~~~\eta = \frac{blocksMade}{\SlotsPerEpoch \cdot \fun{activeSlotCoeff}~{pp}} \\
& ~~~~~~~\eta = \frac{blocksMade}{\SlotsPerEpoch \cdot \fun{activeSlotCoeff}~\var{prevPp}} \\
& ~~~~~~~\var{rewardPot} = \var{feeSS} + \Delta r \\
& ~~~~~~~\Delta t_1 = \floor*{(\fun{tau}~{pp}) \cdot \var{rewardPot}} \\
& ~~~~~~~\Delta t_1 = \floor*{(\fun{tau}~\var{prevPp}) \cdot \var{rewardPot}} \\
& ~~~~~~~\var{R} = \var{rewardPot} - \Delta t_1 \\
& ~~~~~~~\var{rs}
= \reward{pp}{b}{R}{(\dom{rewards})}{poolsSS}{stake}{delegs}{total} \\
= \reward{prevPp}{b}{R}{(\dom{rewards})}{poolsSS}{stake}{delegs}{total} \\
& ~~~~~~~\Delta t_{2} = R - \left(\sum\limits_{\_\mapsto c\in\var{rs}}c\right) \\
& ~~~~~~~blocksMade = \sum_{\wcard \mapsto m \in b}m
\end{align*}
Expand Down Expand Up @@ -1402,6 +1426,7 @@ \subsection{Reward Update Calculation}
\var{fees} \\
\var{up} \\
~ \\
\var{prevPp} \\
\var{pp} \\
\end{array}
\right)
Expand All @@ -1427,6 +1452,7 @@ \subsection{Reward Update Calculation}
\varUpdate{\var{fees}+\Delta f} \\
\var{up} \\
~ \\
\var{prevPp} \\
\var{pp} \\
\end{array}
\right)
Expand Down
13 changes: 2 additions & 11 deletions shelley/chain-and-ledger/formal-spec/ledger-spec.tex
View file
Expand Up @@ -72,6 +72,8 @@
\newcommand{\Wdrl}{\type{Wdrl}}
\newcommand{\Coin}{\type{Coin}}
\newcommand{\PParams}{\type{PParams}}
\newcommand{\PParamsUpdate}{\type{PParamsUpdate}}
\newcommand{\ProposedPPUpdates}{\type{ProposedPPUpdates}}
\newcommand{\Slot}{\type{Slot}}
\newcommand{\SlotsPrior}{\ensuremath{\mathsf{SlotsPrior}}}
\newcommand{\SlotsPerEpoch}{\mathsf{SlotsPerEpoch}}
Expand All @@ -89,17 +91,10 @@
\newcommand{\seedOp}{\star}
\newcommand{\Ppm}{\type{Ppm}}
\newcommand{\ProtVer}{\ensuremath{\type{ProtVer}}}
\newcommand{\ApName}{\ensuremath{\type{ApName}}}
\newcommand{\ApVer}{\ensuremath{\type{ApVer}}}
\newcommand{\SystemTag}{\ensuremath{\type{SystemTag}}}
\newcommand{\InstallerHash}{\ensuremath{\type{InstallerHash}}}
\newcommand{\MetaDatum}{\ensuremath{\type{MetaDatum}}}
\newcommand{\MetaData}{\ensuremath{\type{MetaData}}}
\newcommand{\MetaDataHash}{\ensuremath{\type{MetaDataHash}}}
\newcommand{\Metadata}{\ensuremath{\type{Mdt}}}
\newcommand{\PPUpdate}{\type{PPUpdate}}
\newcommand{\Applications}{\type{Applications}}
\newcommand{\AVUpdate}{\type{AVUpdate}}
\newcommand{\Update}{\type{Update}}

\newcommand{\DCert}{\type{DCert}}
Expand Down Expand Up @@ -181,10 +176,6 @@
\newcommand{\Block}{\type{Block}}
\newcommand{\SlotId}{\type{SlotId}}
\newcommand{\PPUpdateEnv}{\type{PPUpdateEnv}}
\newcommand{\AVUpdateEnv}{\type{AVUpdateEnv}}
\newcommand{\AVUpdateState}{\type{AVUpdateState}}
\newcommand{\UpdateEnv}{\type{UpdateEnv}}
\newcommand{\UpdateState}{\type{UpdateState}}
\newcommand{\UTxOEnv}{\type{UTxOEnv}}
\newcommand{\CEEnv}{\type{CEEnv}}
\newcommand{\CEState}{\type{CEState}}
Expand Down
10 changes: 9 additions & 1 deletion shelley/chain-and-ledger/formal-spec/protocol-parameters.tex
View file
Expand Up @@ -12,6 +12,9 @@ \section{Protocol Parameters}
indexed by their names.
We will explain the significance of each parameter as it comes up in
the calculations used in transition rules.
The type $\PParamsUpdate$ is similar to $\PParams$, but is
a partial mapping of the protocol parameters. It is used in the update
system explained in Section~\ref{sec:update}.

The type $\Coin$ is defined as an alias for the integers.
Negative values will not be allowed in UTxO outputs or reward accounts,
Expand Down Expand Up @@ -76,8 +79,13 @@ \section{Protocol Parameters}
\begin{array}{r@{~\in~}l@{\qquad=\qquad}lr}
\var{pp}
& \PParams
& \Ppm \to \mathsf{T_{ppm}}
& \text{protocol parameters}
\\
\var{ppup}
& \PParamsUpdate
& \Ppm \mapsto \mathsf{T_{ppm}}
& \text{protocol parameter map}
& \text{protocol parameter update}
\\
\var{coin}
& \Coin
Expand Down
5 changes: 1 addition & 4 deletions shelley/chain-and-ledger/formal-spec/rules.dot
View file
Expand Up @@ -8,10 +8,7 @@ digraph STS {

UTXOW -> UTXO
UTXOW -> DELEGS [style=dotted]
UTXO -> UP

UP -> PPUP
UP -> AVUP
UTXO -> PPUP

DELEGS -> DELPL
DELEGS -> DELEGS
Expand Down
Binary file modified shelley/chain-and-ledger/formal-spec/rules.pdf
View file
Binary file not shown.

0 comments on commit 30ae1be

Please sign in to comment.