Skip to content

fix createRUpd in spec, add TICKN to diagram #2516

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
Oct 11, 2021
Merged

fix createRUpd in spec, add TICKN to diagram #2516

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
6 changes: 3 additions & 3 deletions eras/shelley/formal-spec/epoch.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1432,8 +1432,8 @@ \subsection{Reward Update Calculation}
\Delta t_1,-~\Delta r_1+\Delta r_2,~\var{rs},~-\var{feeSS}\right) \\
& ~~~\where \\
& ~~~~~~~(\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,~\wcard,~\var{pstake_{go}},~\var{feeSS}) = \var{ss}\\
& ~~~~~~~(\var{stake},~\var{delegs},~\var{poolParams}) = \var{pstate_{go}} \\
& ~~~~~~~(\wcard,~\var{reserves}) = \var{acnt} \\
& ~~~~~~~\left(
\wcard,~
Expand All @@ -1456,7 +1456,7 @@ \subsection{Reward Update Calculation}
& ~~~~~~~\var{R} = \var{rewardPot} - \Delta t_1 \\
& ~~~~~~~\var{circulation} = \var{total} - \var{reserves} \\
& ~~~~~~~\var{rs}
= \reward{prevPp}{b}{R}{(\dom{rewards})}{poolsSS}{stake}{delegs}{circulation} \\
= \reward{prevPp}{b}{R}{(\dom{rewards})}{poolParams}{stake}{delegs}{circulation} \\
& ~~~~~~~\Delta r_{2} = R - \left(\sum\limits_{\_\mapsto c\in\var{rs}}c\right) \\
& ~~~~~~~blocksMade = \sum_{\wcard \mapsto m \in b}m
\end{align*}
Expand Down
4 changes: 4 additions & 0 deletions eras/shelley/formal-spec/frontmatter.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,9 @@
remove all mentions of deposit decay, sync varibale names with code.}
\change{2021/08/27}{Jared Corduan}{FM (IOHK)}{Fixed definitions in the header-only validation properties.
CHAIN transition did not need to use previous protocol parameters.}
\change{2021/10/08}{Jared Corduan}{FM (IOHK)}{The function createRUpd
should get the pool parameters from the go snapshot.
The TICKN rule was missing from the dependency diagram.}
\end{changelog}
\clearpage%
\renewcommand{\thepage}{\arabic{page}}
Expand Down Expand Up @@ -66,6 +69,7 @@ \section*{List of Contributors}
\label{acknowledgements}

Nicol\'as Arqueros,
Dan Bornside,
Nicholas Clarke,
Duncan Coutts,
Ruslan Dudin,
Expand Down
3 changes: 3 additions & 0 deletions eras/shelley/formal-spec/rules.dot
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,9 @@ digraph STS {
CHAIN -> BBODY
CHAIN -> PRTCL
CHAIN -> TICK
CHAIN -> TICKN
TICKN -> PRTCL [style=dotted]

BBODY -> PRTCL [style=dotted]
BBODY -> TICK [style=dotted]
PRTCL -> TICK [style=dotted]
Expand Down
Binary file modified eras/shelley/formal-spec/rules.pdf
View file
Open in desktop
Binary file not shown.