Merge pull request #2516 from input-output-hk/jc/fix-createRUpd-spec

fix createRUpd in spec, add TICKN to diagram
IntersectMBO · Oct 11, 2021 · 3f2c3fc · 3f2c3fc
2 parents 8ef01f2 + dd7327b
commit 3f2c3fc
Show file tree

Hide file tree

Showing 4 changed files with 10 additions and 3 deletions.
diff --git a/eras/shelley/formal-spec/epoch.tex b/eras/shelley/formal-spec/epoch.tex
@@ -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,~
@@ -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*}

diff --git a/eras/shelley/formal-spec/frontmatter.tex b/eras/shelley/formal-spec/frontmatter.tex
@@ -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}}
@@ -66,6 +69,7 @@ \section*{List of Contributors}
 \label{acknowledgements}
 
 Nicol\'as Arqueros,
+Dan Bornside,
 Nicholas Clarke,
 Duncan Coutts,
 Ruslan Dudin,

diff --git a/eras/shelley/formal-spec/rules.dot b/eras/shelley/formal-spec/rules.dot
@@ -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]

diff --git a/eras/shelley/formal-spec/rules.pdf b/eras/shelley/formal-spec/rules.pdf