audit issue #1751

IntersectMBO · Aug 11, 2020 · a0c9371 · a0c9371
1 parent cf48f29
commit a0c9371
Show file tree

Hide file tree

Showing 4 changed files with 22 additions and 17 deletions.
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Deleg.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Deleg.hs
@@ -246,16 +246,16 @@ delegationTransition = do
       -- gkh ∈ dom genDelegs ?! GenesisKeyNotInpMappingDELEG gkh
       (case Map.lookup gkh genDelegs of Just _ -> True; Nothing -> False) ?! GenesisKeyNotInpMappingDELEG gkh
 
-      let currentOtherDelegations =
+      let cod =
             range $
-              Map.filterWithKey (\k _ -> k /= gkh) genDelegs
-          futureOtherDelegations =
+              Map.filterWithKey (\g _ -> g /= gkh) genDelegs
+          fod =
             range $
-              Map.filterWithKey (\(FutureGenDeleg _ k) _ -> k /= gkh) (_fGenDelegs ds)
-          currentOtherColdKeyHashes = Set.map genDelegKeyHash currentOtherDelegations
-          futureOtherColdKeyHashes = Set.map genDelegKeyHash futureOtherDelegations
-          currentOtherVrfKeyHashes = Set.map genDelegVrfHash currentOtherDelegations
-          futureOtherVrfKeyHashes = Set.map genDelegVrfHash futureOtherDelegations
+              Map.filterWithKey (\(FutureGenDeleg _ g) _ -> g /= gkh) (_fGenDelegs ds)
+          currentOtherColdKeyHashes = Set.map genDelegKeyHash cod
+          currentOtherVrfKeyHashes = Set.map genDelegVrfHash cod
+          futureOtherColdKeyHashes = Set.map genDelegKeyHash fod
+          futureOtherVrfKeyHashes = Set.map genDelegVrfHash fod
 
       eval (vkh ∉ (currentOtherColdKeyHashes `Set.union` futureOtherColdKeyHashes))
         ?! DuplicateGenesisDelegateDELEG vkh

diff --git a/shelley/chain-and-ledger/formal-spec/delegation.tex b/shelley/chain-and-ledger/formal-spec/delegation.tex
@@ -106,7 +106,6 @@ \subsection{Delegation Definitions}
   \begin{equation*}
     \begin{array}{r@{~\in~}lr}
       \var{url} & \URL & \text{a url}\\
-      \var{pmd} & \PoolMD & \text{pool metadata}\\
       \var{mp} & \MIRPot & \text{either $\ReservesMIR$ or $\TreasuryMIR$}\\
     \end{array}
   \end{equation*}
@@ -530,16 +529,23 @@ \subsection{Delegation Rules}
       & \var{gkh}\in\dom{genDelegs}
       \\~\\
       {
-        \begin{array}{ l @{~\leteq~\{} c @{~\mid~} r @{\mapsto} l @{,~\var{g}\neq\var{gkh}\}} }
-          \var{currentOtherColdKeyHashes} & \var{k}  & \var{g} & (\var{k},~\wcard) \\
-          \var{currentOtherVrfKeyHashes}  & \var{v} & \var{g} & (\wcard,~\var{v}) \\
-          \var{futureOtherColdKeyHashes}  & \var{k}  & (\var{g},~\wcard) & (\var{k},~\wcard) \\
-          \var{futureOtherVrfKeyHashe}    & \var{v} & (\var{g},~\wcard) & (\wcard,~\var{v}) \\
+        \begin{array}{ l @{\leteq \{(k,~v) ~\mid~(} c @{\mapsto(k,~v))\in~} l @{,~\var{g}\neq\var{gkh}\}} }
+          \var{cod} & \var{g} & \var{genDelegs} \\
+          \var{fod} & (\wcard,~\var{g}) & \var{fGenDelegs}
+        \end{array}
+      }
+      \\~\\
+      {
+        \begin{array}{ l @{~\leteq~\{} c @{~\mid~\wcard\mapsto} c @{\in~} l @{\}}}
+          \var{currentOtherColdKeyHashes} & \var{k} & (\var{k},~\wcard) & \var{cod}\\
+          \var{currentOtherVrfKeyHashes}  & \var{v} & (\wcard,~\var{v}) & \var{cod}\\
+          \var{futureOtherColdKeyHashes}  & \var{k} & (\var{k},~\wcard) & \var{fod}\\
+          \var{futureOtherVrfKeyHashes}   & \var{v} & (\wcard,~\var{v}) & \var{fod}\\
       \end{array}
       }
       \\
       \var{vkh}\notin\var{currentOtherColdKeyHashes}\union\var{futureOtherColdKeyHashes} \\
-      \var{vrf}\notin\var{currentOtherVrfKeyHashes}\union\var{futureOtherVrfKeyHashe} \\
+      \var{vrf}\notin\var{currentOtherVrfKeyHashes}\union\var{futureOtherVrfKeyHashes} \\
       \var{fdeleg}\leteq\{(\var{s'},~\var{gkh}) \mapsto (\var{vkh},~\var{vrf})\}
     }
     {

diff --git a/shelley/chain-and-ledger/formal-spec/ledger-spec.tex b/shelley/chain-and-ledger/formal-spec/ledger-spec.tex
@@ -97,7 +97,6 @@
 \newcommand{\MetaDatum}{\ensuremath{\type{MetaDatum}}}
 \newcommand{\MetaData}{\ensuremath{\type{MetaData}}}
 \newcommand{\MetaDataHash}{\ensuremath{\type{MetaDataHash}}}
-\newcommand{\PPUpdate}{\type{PPUpdate}}
 \newcommand{\Update}{\type{Update}}
 \newcommand{\GenesisDelegation}{\type{GenesisDelegation}}
 \newcommand{\FutGenesisDelegation}{\type{FutGenesisDelegation}}

diff --git a/shelley/chain-and-ledger/formal-spec/transactions.tex b/shelley/chain-and-ledger/formal-spec/transactions.tex
@@ -94,7 +94,7 @@ \section{Transactions}
     \begin{array}{r@{~\in~}l@{\qquad=\qquad}lr}
       \var{pup}
       & \ProposedPPUpdates
-      & \KeyHashGen \mapsto \PPUpdate
+      & \KeyHashGen \mapsto \PParamsUpdate
       & \text{proposed updates}
       \\
       \var{up}