Merge pull request #2623 from input-output-hk/jc/fix-shelley-spec-new…

…-pools-count Fix error in Shelley Spec regarding new pool count
IntersectMBO · Jan 26, 2022 · b63d046 · b63d046
2 parents 75377d5 + 9d3c329
commit b63d046
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 11 deletions.
diff --git a/eras/shelley/formal-spec/epoch.tex b/eras/shelley/formal-spec/epoch.tex
@@ -571,13 +571,11 @@ \subsection{Pool Reaping Transition}
                  & \{\var{hk}\mapsto \fun{poolRAcnt}~\var{pool} \mid
                    \var{hk}\mapsto\var{pool} \in \var{retired}\restrictdom\var{poolParams} \} \\
         \var{rewardAcnts'} & \left\{
-                        a \mapsto c
-                        \mathrel{\Bigg|}
-                        \begin{array}{r@{~\in~}l}
-                          \var{hk} \mapsto c & \var{pr}, \\
-                          \var{hk}\mapsto\var{a} & \var{rewardAcnts} \\
-                        \end{array}
-                      \right\} \\
+                               a \mapsto
+                               \sum\var{pr}(\var{rewardAcnts}^{-1}(a))
+                               \mathrel{\Big|}
+                               a\in\range{rewardAcnts}
+                             \right\} \\
         \var{refunds} & \dom{rewards}\restrictdom\var{rewardAcnts'} \\
         \var{mRefunds} & \dom{rewards}\subtractdom\var{rewardAcnts'} \\
         \var{refunded} & \sum\limits_{\wcard\mapsto c\in\var{refunds}} c \\

diff --git a/eras/shelley/formal-spec/frontmatter.tex b/eras/shelley/formal-spec/frontmatter.tex
@@ -40,6 +40,7 @@
           The TICKN rule was missing from the dependency diagram.}
         \change{2021/11/08}{Jared Corduan}{FM (IOHK)}{Fixed typo in the description of variable length encodings.}
         \change{2021/12/13}{Jared Corduan}{FM (IOHK)}{Re-wrote the MIR transitions to be more compact.}
+        \change{2022/1/20}{Jared Corduan}{FM (IOHK)}{Fixed error in counting new pools for deposits and an error in the POOLREAP rule.}
       \end{changelog}
       \clearpage%
 \renewcommand{\thepage}{\arabic{page}}

diff --git a/eras/shelley/formal-spec/utxo.tex b/eras/shelley/formal-spec/utxo.tex
@@ -398,15 +398,15 @@ \subsection{Deposits and Refunds}
   \begin{align*}
     & \fun{totalDeposits} \in \PParams \to (\KeyHash_{pool}\mapsto\PoolParam) \\
     & ~~~~\to \seqof{\DCert} \to \Coin
-    & \text{total deposits for transaction} \\
+    & \text{total deposits for a tx} \\
     & \totalDeposits{pp}{poolParams}{certs} = \\
     &  ~~~ (\fun{keyDeposit}~pp)\cdot|\var{certs}\cap\DCertRegKey| \\
-    &  ~~~~~ + (\fun{poolDeposit}~pp)\cdot|\var{newPools}| \\
+    &  ~~~~~ + (\fun{poolDeposit}~pp)\cdot|\{\cwitness{c} ~\mid c\in~\var{newPools}\}| \\
     & ~~~\where \\
-    &  ~~~~~~~ \var{newPools} = \{\var{certs}\cap\DCertRegPool ~\mid~ \cwitness{c}\notin \var{poolParams}\}
+    &  ~~~~~~~ \var{newPools} = \{c ~\mid~ c\in\var{certs}\cap\DCertRegPool,~\cwitness{c}\notin \var{poolParams}\}
     \nextdef
       & \fun{keyRefunds} \in \PParams \to \TxBody \to \Coin
-      & \text{key refunds for a transaction} \\
+      & \text{key refunds for a tx} \\
       & \keyRefunds{pp}{tx} = (\fun{keyDeposit}~\var{pp})\cdot|\txcerts{tx} \cap \DCertDeRegKey|\\
       \end{align*}
       \caption{Functions used in Deposits - Refunds}