{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Cardano.Ledger.Shelley.Rules.Ppup (
  ShelleyPPUP,
  PpupEnv (..),
  ShelleyPpupPredFailure (..),
  ShelleyGovState (..),
  PpupEvent (..),
  PredicateFailure,
  VotingPeriod (..),
  votedFuturePParams,
)
where

import Cardano.Ledger.BaseTypes (
  Globals (quorum),
  Mismatch (..),
  ProtVer,
  Relation (..),
  ShelleyBase,
  StrictMaybe (..),
 )
import Cardano.Ledger.Binary (
  DecCBOR (..),
  EncCBOR (..),
  decodeWord,
 )
import Cardano.Ledger.Binary.Coders
import Cardano.Ledger.Core
import Cardano.Ledger.Keys (GenDelegs (GenDelegs), KeyHash, KeyRole (Genesis))
import Cardano.Ledger.Shelley.Era (ShelleyEra, ShelleyPPUP)
import Cardano.Ledger.Shelley.Governance
import Cardano.Ledger.Shelley.PParams (
  ProposedPPUpdates (ProposedPPUpdates),
  Update (..),
  hasLegalProtVerUpdate,
 )
import Cardano.Ledger.Slot (
  EpochNo (..),
  SlotNo,
  getTheSlotOfNoReturn,
 )
import Control.DeepSeq (NFData)
import Control.Monad (guard)
import Control.Monad.Trans.Reader (asks)
import Control.SetAlgebra (dom, eval, (⊆), (⨃))
import Control.State.Transition
import qualified Data.Foldable as F (find)
import qualified Data.Map as Map
import Data.Set (Set)
import Data.Word (Word64, Word8)
import GHC.Generics (Generic)
import Lens.Micro ((^.))
import NoThunks.Class (NoThunks (..))

data PpupEnv era
  = PPUPEnv SlotNo (PParams era) (GenDelegs (EraCrypto era))

data VotingPeriod = VoteForThisEpoch | VoteForNextEpoch
  deriving (Int -> VotingPeriod -> ShowS
[VotingPeriod] -> ShowS
VotingPeriod -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [VotingPeriod] -> ShowS
$cshowList :: [VotingPeriod] -> ShowS
show :: VotingPeriod -> String
$cshow :: VotingPeriod -> String
showsPrec :: Int -> VotingPeriod -> ShowS
$cshowsPrec :: Int -> VotingPeriod -> ShowS
Show, VotingPeriod -> VotingPeriod -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: VotingPeriod -> VotingPeriod -> Bool
$c/= :: VotingPeriod -> VotingPeriod -> Bool
== :: VotingPeriod -> VotingPeriod -> Bool
$c== :: VotingPeriod -> VotingPeriod -> Bool
Eq, forall x. Rep VotingPeriod x -> VotingPeriod
forall x. VotingPeriod -> Rep VotingPeriod x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep VotingPeriod x -> VotingPeriod
$cfrom :: forall x. VotingPeriod -> Rep VotingPeriod x
Generic)

instance NoThunks VotingPeriod

instance NFData VotingPeriod

instance EncCBOR VotingPeriod where
  encCBOR :: VotingPeriod -> Encoding
encCBOR VotingPeriod
VoteForThisEpoch = forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
0 :: Word8)
  encCBOR VotingPeriod
VoteForNextEpoch = forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
1 :: Word8)

instance DecCBOR VotingPeriod where
  decCBOR :: forall s. Decoder s VotingPeriod
decCBOR =
    forall s. Decoder s Word
decodeWord forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Word
0 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure VotingPeriod
VoteForThisEpoch
      Word
1 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure VotingPeriod
VoteForNextEpoch
      Word
k -> forall (m :: * -> *) a. MonadFail m => Word -> m a
invalidKey Word
k

data ShelleyPpupPredFailure era
  = -- | An update was proposed by a key hash that is not one of the genesis keys.
    --  `mismatchSupplied` ~ key hashes which were a part of the update.
    --  `mismatchExpected` ~ key hashes of the genesis keys.
    NonGenesisUpdatePPUP
      !(Mismatch 'RelSubset (Set (KeyHash 'Genesis (EraCrypto era))))
  | -- | An update was proposed for the wrong epoch.
    --  The first 'EpochNo' is the current epoch.
    --  The second 'EpochNo' is the epoch listed in the update.
    --  The last parameter indicates if the update was intended
    --  for the current or the next epoch.
    PPUpdateWrongEpoch
      !EpochNo
      !EpochNo
      !VotingPeriod
  | -- | An update was proposed which contains an invalid protocol version.
    --  New protocol versions must either increase the major
    --  number by exactly one and set the minor version to zero,
    --  or keep the major version the same and increase the minor
    --  version by exactly one.
    PVCannotFollowPPUP
      !ProtVer
  deriving (Int -> ShelleyPpupPredFailure era -> ShowS
forall era. Int -> ShelleyPpupPredFailure era -> ShowS
forall era. [ShelleyPpupPredFailure era] -> ShowS
forall era. ShelleyPpupPredFailure era -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ShelleyPpupPredFailure era] -> ShowS
$cshowList :: forall era. [ShelleyPpupPredFailure era] -> ShowS
show :: ShelleyPpupPredFailure era -> String
$cshow :: forall era. ShelleyPpupPredFailure era -> String
showsPrec :: Int -> ShelleyPpupPredFailure era -> ShowS
$cshowsPrec :: forall era. Int -> ShelleyPpupPredFailure era -> ShowS
Show, ShelleyPpupPredFailure era -> ShelleyPpupPredFailure era -> Bool
forall era.
ShelleyPpupPredFailure era -> ShelleyPpupPredFailure era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ShelleyPpupPredFailure era -> ShelleyPpupPredFailure era -> Bool
$c/= :: forall era.
ShelleyPpupPredFailure era -> ShelleyPpupPredFailure era -> Bool
== :: ShelleyPpupPredFailure era -> ShelleyPpupPredFailure era -> Bool
$c== :: forall era.
ShelleyPpupPredFailure era -> ShelleyPpupPredFailure era -> Bool
Eq, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyPpupPredFailure era) x -> ShelleyPpupPredFailure era
forall era x.
ShelleyPpupPredFailure era -> Rep (ShelleyPpupPredFailure era) x
$cto :: forall era x.
Rep (ShelleyPpupPredFailure era) x -> ShelleyPpupPredFailure era
$cfrom :: forall era x.
ShelleyPpupPredFailure era -> Rep (ShelleyPpupPredFailure era) x
Generic)

type instance EraRuleFailure "PPUP" (ShelleyEra c) = ShelleyPpupPredFailure (ShelleyEra c)

instance InjectRuleFailure "PPUP" ShelleyPpupPredFailure (ShelleyEra c)

instance NoThunks (ShelleyPpupPredFailure era)

instance NFData (ShelleyPpupPredFailure era)

newtype PpupEvent era = PpupNewEpoch EpochNo
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x. Rep (PpupEvent era) x -> PpupEvent era
forall era x. PpupEvent era -> Rep (PpupEvent era) x
$cto :: forall era x. Rep (PpupEvent era) x -> PpupEvent era
$cfrom :: forall era x. PpupEvent era -> Rep (PpupEvent era) x
Generic, PpupEvent era -> PpupEvent era -> Bool
forall era. PpupEvent era -> PpupEvent era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PpupEvent era -> PpupEvent era -> Bool
$c/= :: forall era. PpupEvent era -> PpupEvent era -> Bool
== :: PpupEvent era -> PpupEvent era -> Bool
$c== :: forall era. PpupEvent era -> PpupEvent era -> Bool
Eq)

instance NFData (PpupEvent era)

instance (EraPParams era, ProtVerAtMost era 8) => STS (ShelleyPPUP era) where
  type State (ShelleyPPUP era) = ShelleyGovState era
  type Signal (ShelleyPPUP era) = StrictMaybe (Update era)
  type Environment (ShelleyPPUP era) = PpupEnv era
  type BaseM (ShelleyPPUP era) = ShelleyBase
  type PredicateFailure (ShelleyPPUP era) = ShelleyPpupPredFailure era
  type Event (ShelleyPPUP era) = PpupEvent era

  initialRules :: [InitialRule (ShelleyPPUP era)]
initialRules = []

  transitionRules :: [TransitionRule (ShelleyPPUP era)]
transitionRules = [forall era.
(EraPParams era, ProtVerAtMost era 8) =>
TransitionRule (ShelleyPPUP era)
ppupTransitionNonEmpty]

instance Era era => EncCBOR (ShelleyPpupPredFailure era) where
  encCBOR :: ShelleyPpupPredFailure era -> Encoding
encCBOR =
    forall (w :: Wrapped) t. Encode w t -> Encoding
encode @_ @(ShelleyPpupPredFailure era) forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      NonGenesisUpdatePPUP Mismatch 'RelSubset (Set (KeyHash 'Genesis (EraCrypto era)))
mm -> forall t. t -> Word -> Encode 'Open t
Sum forall era.
Mismatch 'RelSubset (Set (KeyHash 'Genesis (EraCrypto era)))
-> ShelleyPpupPredFailure era
NonGenesisUpdatePPUP Word
0 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Mismatch 'RelSubset (Set (KeyHash 'Genesis (EraCrypto era)))
mm
      PPUpdateWrongEpoch EpochNo
ce EpochNo
e VotingPeriod
vp -> forall t. t -> Word -> Encode 'Open t
Sum forall era.
EpochNo -> EpochNo -> VotingPeriod -> ShelleyPpupPredFailure era
PPUpdateWrongEpoch Word
1 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To EpochNo
ce forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To EpochNo
e forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To VotingPeriod
vp
      PVCannotFollowPPUP ProtVer
p -> forall t. t -> Word -> Encode 'Open t
Sum forall era. ProtVer -> ShelleyPpupPredFailure era
PVCannotFollowPPUP Word
2 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To ProtVer
p

instance Era era => DecCBOR (ShelleyPpupPredFailure era) where
  decCBOR :: forall s. Decoder s (ShelleyPpupPredFailure era)
decCBOR = forall (w :: Wrapped) t s. Decode w t -> Decoder s t
decode forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t.
Text -> (Word -> Decode 'Open t) -> Decode ('Closed 'Dense) t
Summands Text
"ShelleyPpupPredFailure" forall a b. (a -> b) -> a -> b
$ \case
    Word
0 -> forall t. t -> Decode 'Open t
SumD forall era.
Mismatch 'RelSubset (Set (KeyHash 'Genesis (EraCrypto era)))
-> ShelleyPpupPredFailure era
NonGenesisUpdatePPUP forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
1 -> forall t. t -> Decode 'Open t
SumD forall era.
EpochNo -> EpochNo -> VotingPeriod -> ShelleyPpupPredFailure era
PPUpdateWrongEpoch forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
2 -> forall t. t -> Decode 'Open t
SumD forall era. ProtVer -> ShelleyPpupPredFailure era
PVCannotFollowPPUP forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
k -> forall (w :: Wrapped) t. Word -> Decode w t
Invalid Word
k

ppupTransitionNonEmpty :: (EraPParams era, ProtVerAtMost era 8) => TransitionRule (ShelleyPPUP era)
ppupTransitionNonEmpty :: forall era.
(EraPParams era, ProtVerAtMost era 8) =>
TransitionRule (ShelleyPPUP era)
ppupTransitionNonEmpty = do
  TRC
    ( PPUPEnv SlotNo
slot PParams era
pp (GenDelegs Map
  (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
genDelegs)
      , pps :: State (ShelleyPPUP era)
pps@( ShelleyGovState
                { sgsCurProposals :: forall era. ShelleyGovState era -> ProposedPPUpdates era
sgsCurProposals = ProposedPPUpdates Map (KeyHash 'Genesis (EraCrypto era)) (PParamsUpdate era)
pupS
                , sgsFutureProposals :: forall era. ShelleyGovState era -> ProposedPPUpdates era
sgsFutureProposals = ProposedPPUpdates Map (KeyHash 'Genesis (EraCrypto era)) (PParamsUpdate era)
fpupS
                }
              )
      , Signal (ShelleyPPUP era)
update
      ) <-
    forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext

  case Signal (ShelleyPPUP era)
update of
    StrictMaybe (Update era)
Signal (ShelleyPPUP era)
SNothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure State (ShelleyPPUP era)
pps
    SJust (Update (ProposedPPUpdates Map (KeyHash 'Genesis (EraCrypto era)) (PParamsUpdate era)
pup) EpochNo
targetEpochNo) -> do
      forall s t. Embed s t => Exp t -> s
eval (forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom Map (KeyHash 'Genesis (EraCrypto era)) (PParamsUpdate era)
pup forall k (f :: * -> * -> *) (g :: * -> * -> *) s1 v s2 u.
(Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) =>
s1 -> s2 -> Exp Bool
⊆ forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom Map
  (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
genDelegs)
        forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era.
Mismatch 'RelSubset (Set (KeyHash 'Genesis (EraCrypto era)))
-> ShelleyPpupPredFailure era
NonGenesisUpdatePPUP
          Mismatch
            { mismatchSupplied :: Set (KeyHash 'Genesis (EraCrypto era))
mismatchSupplied = forall s t. Embed s t => Exp t -> s
eval forall a b. (a -> b) -> a -> b
$ forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom Map (KeyHash 'Genesis (EraCrypto era)) (PParamsUpdate era)
pup
            , mismatchExpected :: Set (KeyHash 'Genesis (EraCrypto era))
mismatchExpected = forall s t. Embed s t => Exp t -> s
eval forall a b. (a -> b) -> a -> b
$ forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom Map
  (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
genDelegs
            }

      let firstIllegalProtVerUpdate :: Maybe ProtVer
firstIllegalProtVerUpdate = do
            PParamsUpdate era
ppu <- forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
F.find (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
(ProtVerAtMost era 8, EraPParams era) =>
PParams era -> PParamsUpdate era -> Bool
hasLegalProtVerUpdate PParams era
pp) Map (KeyHash 'Genesis (EraCrypto era)) (PParamsUpdate era)
pup
            -- SNothing is considered legal
            SJust ProtVer
newBadProtVer <- forall a. a -> Maybe a
Just (PParamsUpdate era
ppu forall s a. s -> Getting a s a -> a
^. forall era.
(EraPParams era, ProtVerAtMost era 8) =>
Lens' (PParamsUpdate era) (StrictMaybe ProtVer)
ppuProtocolVersionL)
            forall a. a -> Maybe a
Just ProtVer
newBadProtVer
      forall a sts (ctx :: RuleType).
Maybe a -> (a -> PredicateFailure sts) -> Rule sts ctx ()
failOnJust Maybe ProtVer
firstIllegalProtVerUpdate forall era. ProtVer -> ShelleyPpupPredFailure era
PVCannotFollowPPUP

      (EpochNo
curEpochNo, SlotNo
tooLate, EpochNo
nextEpochNo) <- forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS forall a b. (a -> b) -> a -> b
$ HasCallStack => SlotNo -> ShelleyBase (EpochNo, SlotNo, EpochNo)
getTheSlotOfNoReturn SlotNo
slot
      forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent forall a b. (a -> b) -> a -> b
$ forall era. EpochNo -> PpupEvent era
PpupNewEpoch EpochNo
nextEpochNo

      if SlotNo
slot forall a. Ord a => a -> a -> Bool
< SlotNo
tooLate
        then do
          (EpochNo
curEpochNo forall a. Eq a => a -> a -> Bool
== EpochNo
targetEpochNo)
            forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era.
EpochNo -> EpochNo -> VotingPeriod -> ShelleyPpupPredFailure era
PPUpdateWrongEpoch EpochNo
curEpochNo EpochNo
targetEpochNo VotingPeriod
VoteForThisEpoch
          let curProposals :: ProposedPPUpdates era
curProposals = forall era.
Map (KeyHash 'Genesis (EraCrypto era)) (PParamsUpdate era)
-> ProposedPPUpdates era
ProposedPPUpdates (forall s t. Embed s t => Exp t -> s
eval (Map (KeyHash 'Genesis (EraCrypto era)) (PParamsUpdate era)
pupS forall k s1 (f :: * -> * -> *) v s2 (g :: * -> * -> *).
(Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) =>
s1 -> s2 -> Exp (f k v)
⨃ Map (KeyHash 'Genesis (EraCrypto era)) (PParamsUpdate era)
pup))
          !Word64
coreNodeQuorum <- forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> Word64
quorum
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
            State (ShelleyPPUP era)
pps
              { sgsCurProposals :: ProposedPPUpdates era
sgsCurProposals = ProposedPPUpdates era
curProposals
              , sgsFutureProposals :: ProposedPPUpdates era
sgsFutureProposals = forall era.
Map (KeyHash 'Genesis (EraCrypto era)) (PParamsUpdate era)
-> ProposedPPUpdates era
ProposedPPUpdates Map (KeyHash 'Genesis (EraCrypto era)) (PParamsUpdate era)
fpupS
              , sgsFuturePParams :: FuturePParams era
sgsFuturePParams =
                  forall era. Maybe (PParams era) -> FuturePParams era
PotentialPParamsUpdate forall a b. (a -> b) -> a -> b
$ forall era.
EraPParams era =>
ProposedPPUpdates era
-> PParams era -> Word64 -> Maybe (PParams era)
votedFuturePParams ProposedPPUpdates era
curProposals PParams era
pp Word64
coreNodeQuorum
              }
        else do
          (forall a. Enum a => a -> a
succ EpochNo
curEpochNo forall a. Eq a => a -> a -> Bool
== EpochNo
targetEpochNo)
            forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era.
EpochNo -> EpochNo -> VotingPeriod -> ShelleyPpupPredFailure era
PPUpdateWrongEpoch EpochNo
curEpochNo EpochNo
targetEpochNo VotingPeriod
VoteForNextEpoch
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
            State (ShelleyPPUP era)
pps
              { sgsCurProposals :: ProposedPPUpdates era
sgsCurProposals = forall era.
Map (KeyHash 'Genesis (EraCrypto era)) (PParamsUpdate era)
-> ProposedPPUpdates era
ProposedPPUpdates Map (KeyHash 'Genesis (EraCrypto era)) (PParamsUpdate era)
pupS
              , sgsFutureProposals :: ProposedPPUpdates era
sgsFutureProposals = forall era.
Map (KeyHash 'Genesis (EraCrypto era)) (PParamsUpdate era)
-> ProposedPPUpdates era
ProposedPPUpdates (forall s t. Embed s t => Exp t -> s
eval (Map (KeyHash 'Genesis (EraCrypto era)) (PParamsUpdate era)
fpupS forall k s1 (f :: * -> * -> *) v s2 (g :: * -> * -> *).
(Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) =>
s1 -> s2 -> Exp (f k v)
⨃ Map (KeyHash 'Genesis (EraCrypto era)) (PParamsUpdate era)
pup))
              }

-- | If at least @n@ nodes voted to change __the same__ protocol parameters to
-- __the same__ values, return the given protocol parameters updated to these
-- values. Here @n@ is the quorum needed.
votedFuturePParams ::
  forall era.
  EraPParams era =>
  ProposedPPUpdates era ->
  -- | Protocol parameters to which the change will be applied.
  PParams era ->
  -- | Quorum needed to change the protocol parameters.
  Word64 ->
  Maybe (PParams era)
votedFuturePParams :: forall era.
EraPParams era =>
ProposedPPUpdates era
-> PParams era -> Word64 -> Maybe (PParams era)
votedFuturePParams (ProposedPPUpdates Map (KeyHash 'Genesis (EraCrypto era)) (PParamsUpdate era)
pppu) PParams era
pp Word64
quorumN = do
  let votes :: Map (PParamsUpdate era) Word64
votes =
        forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr
          (\PParamsUpdate era
vote -> forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith forall a. Num a => a -> a -> a
(+) PParamsUpdate era
vote Word64
1)
          (forall k a. Map k a
Map.empty :: Map.Map (PParamsUpdate era) Word64)
          Map (KeyHash 'Genesis (EraCrypto era)) (PParamsUpdate era)
pppu
      consensus :: Map (PParamsUpdate era) Word64
consensus = forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (forall a. Ord a => a -> a -> Bool
>= Word64
quorumN) Map (PParamsUpdate era) Word64
votes
  -- 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.
  [PParamsUpdate era
ppu] <- forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
Map.keys Map (PParamsUpdate era) Word64
consensus
  -- NOTE that `applyPPUpdates` corresponds to the union override right
  -- operation in the formal spec.
  let ppNew :: PParams era
ppNew = forall era.
EraPParams era =>
PParams era -> PParamsUpdate era -> PParams era
applyPPUpdates PParams era
pp PParamsUpdate era
ppu
  -- TODO: Remove this incorrect check from the code and the spec. It is incorrect because
  -- block header size is not part of the block body size, therefore this relation makes
  -- no sense. My hypothesis is that at initial design phase there was a block size that
  -- included the block header size, which later got changed to block body size. See
  -- relevant spec ticket: https://github.com/IntersectMBO/cardano-ledger/issues/4251
  forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$
    forall a. Integral a => a -> Integer
toInteger (PParams era
ppNew forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) Word32
ppMaxTxSizeL) forall a. Num a => a -> a -> a
+ forall a. Integral a => a -> Integer
toInteger (PParams era
ppNew forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) Word16
ppMaxBHSizeL)
      forall a. Ord a => a -> a -> Bool
< forall a. Integral a => a -> Integer
toInteger (PParams era
ppNew forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) Word32
ppMaxBBSizeL)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure PParams era
ppNew