Merge pull request #1918 from input-output-hk/jc/audit-issue-1907

Formal Spec - correct chainChecks and positional arguments in NewEpochState and EpochState
IntersectMBO · Oct 19, 2020 · c6508ab · c6508ab
2 parents 4068b9b + e8f39be
commit c6508ab
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 14 deletions.
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/LedgerState.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/LedgerState.hs
@@ -430,7 +430,11 @@ data EpochState era = EpochState
     esLState :: !(LedgerState era),
     esPrevPp :: !(PParams era),
     esPp :: !(PParams era),
-    esNonMyopic :: !(NonMyopic era) -- TODO document this in the formal spec, see github #1319
+    -- | This field, esNonMyopic, does not appear in the formal spec
+    -- and is not a part of the protocol. It is only used for providing
+    -- data to the stake pool ranking calculation @getNonMyopicMemberRewards@.
+    -- See https://hydra.iohk.io/job/Cardano/cardano-ledger-specs/specs.pool-ranking/latest/download-by-type/doc-pdf/pool-ranking
+    esNonMyopic :: !(NonMyopic era)
   }
   deriving (Generic)
 

diff --git a/shelley/chain-and-ledger/formal-spec/chain.tex b/shelley/chain-and-ledger/formal-spec/chain.tex
@@ -1809,10 +1809,10 @@ \subsection{Chain Transition}
       &
       \begin{array}{lr@{~=~}l}
         \where
-          & (\wcard,~\wcard,~\wcard,~\wcard,~\var{es},~\wcard,~\wcard)
+          & (\wcard,~\wcard,~\wcard,~\var{es},~\wcard,~\wcard)
           & \var{nes}
           \\
-          & (\wcard,~\wcard,~\var{ls},~\wcard)
+          & (\wcard,~\wcard,~\var{ls},~\wcard,~\wcard)
           & \var{es}
           \\
           & (\wcard,~((\wcard,~\wcard,~\wcard,~\wcard,~\var{genDelegs},~\wcard),~\wcard))
@@ -1823,21 +1823,21 @@ \subsection{Chain Transition}
   \begin{align*}
       & \fun{updateNES} \in \NewEpochState \to \BlocksMade \to \LState \to \NewEpochState \\
       & \fun{updateNES}~
-      (\var{e_\ell},~\var{b_{prev}},~\wcard,~(\var{acnt},~\var{ss},~\wcard,~\var{pp}),
+      (\var{e_\ell},~\var{b_{prev}},~\wcard,~(\var{acnt},~\var{ss},~\wcard,~\var{prevPp},~\var{pp}),
        ~\var{ru},~\var{pd})
           ~\var{b_{cur}}~\var{ls} = \\
       & ~~~~
       (\var{e_\ell},~\var{b_{prev}},~\var{b_{cur}},
-       ~(\var{acnt},~\var{ss},~\var{ls},~\var{pp}),~\var{ru},~\var{pd})
+       ~(\var{acnt},~\var{ss},~\var{ls},~\var{prevPp},~\var{pp}),~\var{ru},~\var{pd})
   \end{align*}
   %
   \begin{align*}
-      & \fun{chainChecks} \in \PParams \to \BHeader \to \Bool \\
-      & \fun{chainChecks}~\var{pp}~\var{bh} = \\
-      & ~~~~ m \leq \MaxMajorPV \\
-      & ~~~~ \land~\bHeaderSize{bh} \leq \fun{maxHeaderSize}~\var{pp} \\
-      & ~~~~ \land~\hBbsize{(\bhbody{bh})} \leq \fun{maxBlockSize}~\var{pp} \\
-      & ~~~~ \where (m,~\wcard)\leteq\fun{pv}~\var{pp}
+      & \fun{chainChecks} \in \N \to (\N,\N, \ProtVer) \to \BHeader \to \Bool \\
+      & \fun{chainChecks}~\var{maxpv}~(\var{maxBHSize},~\var{maxBBSize},~\var{protocolVersion})~\var{bh} = \\
+      & ~~~~ m \leq \var{maxpv} \\
+      & ~~~~ \land~\bHeaderSize{bh} \leq \var{maxBHSize} \\
+      & ~~~~ \land~\hBbsize{(\bhbody{bh})} \leq \var{maxBBSize} \\
+      & ~~~~ \where (m,~\wcard)\leteq\var{protocolVersion}
   \end{align*}
   %
   \begin{align*}
@@ -1884,17 +1884,19 @@ \subsection{Chain Transition}
       &
       \var{s} \leteq \bslot{bhb}
       \\
-      (\wcard,~\wcard,~\wcard,~(\wcard,~\wcard,~\wcard,~\var{pp}),~\wcard,~\wcard) \leteq \var{nes}
+      (\wcard,~\wcard,~\wcard,~(\wcard,~\wcard,~\wcard,~\wcard,~\var{pp}),~\wcard,~\wcard) \leteq \var{nes}
       \\~\\
       \fun{prtlSeqChecks}~\var{lab}~\var{bh}\\
-      \fun{chainChecks}~\var{pp}~\var{bh}
+      \fun{chainChecks}~
+        \MaxMajorPV~(\fun{maxHeaderSize}~\var{pp},~\fun{maxBlockSize}~\var{pp},~\fun{pv}~\var{pp})~
+        \var{bh}
       \\~\\
       {
         \vdash\var{nes}\trans{\hyperref[fig:rules:tick]{tick}}{\var{s}}\var{nes'}
       } \\~\\
       (\var{e_1},~\wcard,~\wcard,~\wcard,~\wcard,~\wcard)
         \leteq\var{nes} \\
-      (\var{e_2},~\wcard,~\var{b_{cur}},~\var{es},~\wcard,~\var{pd})
+      (\var{e_2},~\wcard,~\var{b_{cur}},~\var{es},~\wcard,~\wcard,~\var{pd})
         \leteq\var{nes'} \\
         (\var{acnt},~\wcard,\var{ls},~\wcard,~\var{pp'})\leteq\var{es}\\
         ( \wcard,