sync formal spec and implementation in EPOCH rule

shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/Genesis.hs

@@ -30,6 +30,7 @@ import Data.Aeson (FromJSON (..), ToJSON (..), (.!=), (.:), (.:?), (.=))
 import qualified Data.Aeson as Aeson
 import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
+import Data.Maybe (catMaybes)
 import Data.Proxy (Proxy (..))
 import Data.Scientific (Scientific)
 import Data.Text (Text)
@@ -210,6 +211,7 @@ initialFundsPseudoTxIn addr =
 data ValidationErr
   = EpochNotLongEnough EpochSize Word64 Rational EpochSize
   | MaxKESEvolutionsUnsupported Word64 Word
+  | QuorumTooSmall Word64 Word64 Word64
   deriving (Eq, Show)
 
 describeValidationErr :: ValidationErr -> Text
@@ -234,6 +236,17 @@ describeValidationErr (MaxKESEvolutionsUnsupported reqKES supportedKES) =
       " but the algorithm supports a maximum of ",
       Text.pack (show supportedKES)
     ]
+describeValidationErr (QuorumTooSmall q maxTooSmal nodes) =
+  mconcat
+    [ "You have specified an 'updateQuorum' which is",
+      " too small compared to the number of genesis nodes.",
+      " You requested ",
+      Text.pack (show q),
+      ", but given ",
+      Text.pack (show nodes),
+      " genesis nodes 'updateQuorum' must be greater than ",
+      Text.pack (show maxTooSmal)
+    ]
 
 -- | Do some basic sanity checking on the Shelley genesis file.
 validateGenesis ::
@@ -246,16 +259,19 @@ validateGenesis
     { sgEpochLength,
       sgActiveSlotsCoeff,
       sgMaxKESEvolutions,
-      sgSecurityParam
+      sgSecurityParam,
+      sgUpdateQuorum,
+      sgGenDelegs
     } =
-    case [ x
-           | Just cel <- [checkEpochLength],
-             Just cke <- [checkKesEvolutions],
-             x <- [cel, cke]
-         ] of
+    case catMaybes errors of
       [] -> Right ()
       xs -> Left xs
     where
+      errors =
+        [ checkEpochLength,
+          checkKesEvolutions,
+          checkQuorumSize
+        ]
       checkEpochLength =
         let minLength =
               EpochSize . ceiling $
@@ -278,3 +294,9 @@ validateGenesis
               MaxKESEvolutionsUnsupported
                 sgMaxKESEvolutions
                 (totalPeriodsKES (Proxy @(KES c)))
+      checkQuorumSize =
+        let numGenesisNodes = fromIntegral $ length sgGenDelegs
+            maxTooSmal = numGenesisNodes `div` 2
+         in if numGenesisNodes == 0 || sgUpdateQuorum > maxTooSmal
+              then Nothing
+              else Just $ QuorumTooSmall sgUpdateQuorum maxTooSmal numGenesisNodes

shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/LedgerState.hs

@@ -427,7 +427,7 @@ data EpochState crypto = EpochState
     esLState :: !(LedgerState crypto),
     esPrevPp :: !PParams,
     esPp :: !PParams,
-    esNonMyopic :: !(NonMyopic crypto)
+    esNonMyopic :: !(NonMyopic crypto) -- TODO document this in the formal spec, see github #1319
   }
   deriving (Show, Eq, Generic)
 

shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Epoch.hs

@@ -77,21 +77,29 @@ initialEpoch =
       emptyPParams
       emptyNonMyopic
 
-votedValuePParams ::
+votedValue ::
   ProposedPPUpdates crypto ->
   PParams ->
   Int ->
   Maybe PParams
-votedValuePParams (ProposedPPUpdates ppup) pps quorumN =
+votedValue (ProposedPPUpdates pup) pps quorumN =
   let incrTally vote tally = 1 + Map.findWithDefault 0 vote tally
       votes =
         Map.foldr
           (\vote tally -> Map.insert vote (incrTally vote tally) tally)
           (Map.empty :: Map PParamsUpdate Int)
-          ppup
+          pup
       consensus = Map.filter (>= quorumN) votes
    in case length consensus of
+        -- NOTE that `quorumN` is a global constant, and that we require
+        -- it to be strictly greater than half the number of genesis nodes.
+        -- The keys in the `pup` correspond to the genesis nodes,
+        -- and therefore either:
+        --   1) `consensus` is empty, or
+        --   2) `consensus` has exactly one element.
         1 -> (Just . updatePParams pps . fst . head . Map.toList) consensus
+        -- NOTE that `updatePParams` corresponds to the union override right
+        -- operation in the formal spec.
         _ -> Nothing
 
 epochTransition ::
@@ -129,8 +137,8 @@ epochTransition = do
 
   coreNodeQuorum <- liftSTS $ asks quorum
 
-  let ppup = proposals . _ppups $ utxoSt
-  let ppNew = votedValuePParams ppup pp (fromIntegral coreNodeQuorum)
+  let pup = proposals . _ppups $ utxoSt'
+  let ppNew = votedValue pup pp (fromIntegral coreNodeQuorum)
   NewppState utxoSt'' acnt'' pp' <-
     trans @(NEWPP crypto) $
       TRC (NewppEnv dstate' pstate'', NewppState utxoSt' acnt' pp, ppNew)

shelley/chain-and-ledger/formal-spec/epoch.tex

@@ -766,7 +766,7 @@ \subsection{Complete Epoch Boundary Transition}
 The transition uses a helper function $\fun{votedValue}$ which returns
 the consensus value of update proposals in the event that consensus is met.
 \textbf{Note that} $\fun{votedValue}$
-\textbf{is only well-defined if } $\Quorum$
+\textbf{is only well-defined if } $\var{quorum}$
 \textbf{is greater than half the number of core nodes, i.e.}
 $\Quorum > |\var{genDelegs}|/2$ \textbf{.}
 
@@ -805,12 +805,13 @@ \subsection{Complete Epoch Boundary Transition}
   %
   \emph{Helper Functions}
   \begin{align*}
-      & \fun{votedValue} \in (\KeyHashGen\mapsto\PParamsUpdate) \to \PParamsUpdate^?\\
-      & \fun{votedValue}~\var{vs} =
-        \begin{cases}
-          p & \exists p\in\range{vs}~(|vs\restrictrange p|\geq \Quorum) \\
-          \Nothing & \text{otherwise} \\
-        \end{cases}
+      & \fun{votedValue} \in (\KeyHashGen\mapsto\PParamsUpdate) \to \PParams \to \N \to \PParamsUpdate^?\\
+      & \fun{votedValue}~\var{pup}~\var{pps}~\var{quorum} =
+      \begin{cases}
+        \var{pps}\unionoverrideRight\var{p}
+          & \exists! p\in\range{vs}~(|vs\restrictrange p|\geq \var{quorum}) \\
+        \Nothing & \text{otherwise} \\
+      \end{cases}
   \end{align*}
   %
   \caption{Epoch transition-system types}
@@ -881,7 +882,7 @@ \subsection{Complete Epoch Boundary Transition}
       \\~\\~\\
       \var{(\wcard,~\wcard,~\wcard,~(\var{pup},\wcard))}\leteq\var{utxoSt'}\\
       \var{pp_{new}}\leteq\var{pp}\unionoverrideRight
-      \fun{votedValue}~\var{pup}\\
+      \fun{votedValue}~\var{pup}~\var{pps}~\Quorum\\
       {
         \begin{array}{r}
           \var{dstate'}\\