{-# 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.Hashes (GenDelegs (..))
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

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

instance NoThunks VotingPeriod

instance NFData VotingPeriod

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

instance DecCBOR VotingPeriod where
  decCBOR :: forall s. Decoder s VotingPeriod
decCBOR =
    Decoder s Word
forall s. Decoder s Word
decodeWord Decoder s Word
-> (Word -> Decoder s VotingPeriod) -> Decoder s VotingPeriod
forall a b. Decoder s a -> (a -> Decoder s b) -> Decoder s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Word
0 -> VotingPeriod -> Decoder s VotingPeriod
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VotingPeriod
VoteForThisEpoch
      Word
1 -> VotingPeriod -> Decoder s VotingPeriod
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VotingPeriod
VoteForNextEpoch
      Word
k -> Word -> Decoder s VotingPeriod
forall a (m :: * -> *). (Typeable 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)))
  | -- | 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
[ShelleyPpupPredFailure era] -> ShowS
ShelleyPpupPredFailure era -> String
(Int -> ShelleyPpupPredFailure era -> ShowS)
-> (ShelleyPpupPredFailure era -> String)
-> ([ShelleyPpupPredFailure era] -> ShowS)
-> Show (ShelleyPpupPredFailure era)
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
$cshowsPrec :: forall era. Int -> ShelleyPpupPredFailure era -> ShowS
showsPrec :: Int -> ShelleyPpupPredFailure era -> ShowS
$cshow :: forall era. ShelleyPpupPredFailure era -> String
show :: ShelleyPpupPredFailure era -> String
$cshowList :: forall era. [ShelleyPpupPredFailure era] -> ShowS
showList :: [ShelleyPpupPredFailure era] -> ShowS
Show, ShelleyPpupPredFailure era -> ShelleyPpupPredFailure era -> Bool
(ShelleyPpupPredFailure era -> ShelleyPpupPredFailure era -> Bool)
-> (ShelleyPpupPredFailure era
    -> ShelleyPpupPredFailure era -> Bool)
-> Eq (ShelleyPpupPredFailure era)
forall era.
ShelleyPpupPredFailure era -> ShelleyPpupPredFailure era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall era.
ShelleyPpupPredFailure era -> ShelleyPpupPredFailure era -> Bool
== :: ShelleyPpupPredFailure era -> ShelleyPpupPredFailure era -> Bool
$c/= :: forall era.
ShelleyPpupPredFailure era -> ShelleyPpupPredFailure era -> Bool
/= :: ShelleyPpupPredFailure era -> ShelleyPpupPredFailure era -> Bool
Eq, (forall x.
 ShelleyPpupPredFailure era -> Rep (ShelleyPpupPredFailure era) x)
-> (forall x.
    Rep (ShelleyPpupPredFailure era) x -> ShelleyPpupPredFailure era)
-> Generic (ShelleyPpupPredFailure era)
forall x.
Rep (ShelleyPpupPredFailure era) x -> ShelleyPpupPredFailure era
forall x.
ShelleyPpupPredFailure era -> Rep (ShelleyPpupPredFailure era) x
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
$cfrom :: forall era x.
ShelleyPpupPredFailure era -> Rep (ShelleyPpupPredFailure era) x
from :: forall x.
ShelleyPpupPredFailure era -> Rep (ShelleyPpupPredFailure era) x
$cto :: forall era x.
Rep (ShelleyPpupPredFailure era) x -> ShelleyPpupPredFailure era
to :: forall x.
Rep (ShelleyPpupPredFailure era) x -> ShelleyPpupPredFailure era
Generic)

type instance EraRuleFailure "PPUP" ShelleyEra = ShelleyPpupPredFailure ShelleyEra

instance InjectRuleFailure "PPUP" ShelleyPpupPredFailure ShelleyEra

instance NoThunks (ShelleyPpupPredFailure era)

instance NFData (ShelleyPpupPredFailure era)

newtype PpupEvent era = PpupNewEpoch EpochNo
  deriving ((forall x. PpupEvent era -> Rep (PpupEvent era) x)
-> (forall x. Rep (PpupEvent era) x -> PpupEvent era)
-> Generic (PpupEvent era)
forall x. Rep (PpupEvent era) x -> PpupEvent era
forall x. PpupEvent era -> Rep (PpupEvent era) x
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
$cfrom :: forall era x. PpupEvent era -> Rep (PpupEvent era) x
from :: forall x. PpupEvent era -> Rep (PpupEvent era) x
$cto :: forall era x. Rep (PpupEvent era) x -> PpupEvent era
to :: forall x. Rep (PpupEvent era) x -> PpupEvent era
Generic, PpupEvent era -> PpupEvent era -> Bool
(PpupEvent era -> PpupEvent era -> Bool)
-> (PpupEvent era -> PpupEvent era -> Bool) -> Eq (PpupEvent era)
forall era. PpupEvent era -> PpupEvent era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall era. PpupEvent era -> PpupEvent era -> Bool
== :: PpupEvent era -> PpupEvent era -> Bool
$c/= :: forall era. PpupEvent era -> PpupEvent era -> Bool
/= :: 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 = [TransitionRule (ShelleyPPUP era)
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) (Encode 'Open (ShelleyPpupPredFailure era) -> Encoding)
-> (ShelleyPpupPredFailure era
    -> Encode 'Open (ShelleyPpupPredFailure era))
-> ShelleyPpupPredFailure era
-> Encoding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      NonGenesisUpdatePPUP Mismatch 'RelSubset (Set (KeyHash 'Genesis))
mm -> (Mismatch 'RelSubset (Set (KeyHash 'Genesis))
 -> ShelleyPpupPredFailure era)
-> Word
-> Encode
     'Open
     (Mismatch 'RelSubset (Set (KeyHash 'Genesis))
      -> ShelleyPpupPredFailure era)
forall t. t -> Word -> Encode 'Open t
Sum Mismatch 'RelSubset (Set (KeyHash 'Genesis))
-> ShelleyPpupPredFailure era
forall era.
Mismatch 'RelSubset (Set (KeyHash 'Genesis))
-> ShelleyPpupPredFailure era
NonGenesisUpdatePPUP Word
0 Encode
  'Open
  (Mismatch 'RelSubset (Set (KeyHash 'Genesis))
   -> ShelleyPpupPredFailure era)
-> Encode
     ('Closed 'Dense) (Mismatch 'RelSubset (Set (KeyHash 'Genesis)))
-> Encode 'Open (ShelleyPpupPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Mismatch 'RelSubset (Set (KeyHash 'Genesis))
-> Encode
     ('Closed 'Dense) (Mismatch 'RelSubset (Set (KeyHash 'Genesis)))
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Mismatch 'RelSubset (Set (KeyHash 'Genesis))
mm
      PPUpdateWrongEpoch EpochNo
ce EpochNo
e VotingPeriod
vp -> (EpochNo -> EpochNo -> VotingPeriod -> ShelleyPpupPredFailure era)
-> Word
-> Encode
     'Open
     (EpochNo -> EpochNo -> VotingPeriod -> ShelleyPpupPredFailure era)
forall t. t -> Word -> Encode 'Open t
Sum EpochNo -> EpochNo -> VotingPeriod -> ShelleyPpupPredFailure era
forall era.
EpochNo -> EpochNo -> VotingPeriod -> ShelleyPpupPredFailure era
PPUpdateWrongEpoch Word
1 Encode
  'Open
  (EpochNo -> EpochNo -> VotingPeriod -> ShelleyPpupPredFailure era)
-> Encode ('Closed 'Dense) EpochNo
-> Encode
     'Open (EpochNo -> VotingPeriod -> ShelleyPpupPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> EpochNo -> Encode ('Closed 'Dense) EpochNo
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To EpochNo
ce Encode
  'Open (EpochNo -> VotingPeriod -> ShelleyPpupPredFailure era)
-> Encode ('Closed 'Dense) EpochNo
-> Encode 'Open (VotingPeriod -> ShelleyPpupPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> EpochNo -> Encode ('Closed 'Dense) EpochNo
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To EpochNo
e Encode 'Open (VotingPeriod -> ShelleyPpupPredFailure era)
-> Encode ('Closed 'Dense) VotingPeriod
-> Encode 'Open (ShelleyPpupPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> VotingPeriod -> Encode ('Closed 'Dense) VotingPeriod
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To VotingPeriod
vp
      PVCannotFollowPPUP ProtVer
p -> (ProtVer -> ShelleyPpupPredFailure era)
-> Word -> Encode 'Open (ProtVer -> ShelleyPpupPredFailure era)
forall t. t -> Word -> Encode 'Open t
Sum ProtVer -> ShelleyPpupPredFailure era
forall era. ProtVer -> ShelleyPpupPredFailure era
PVCannotFollowPPUP Word
2 Encode 'Open (ProtVer -> ShelleyPpupPredFailure era)
-> Encode ('Closed 'Dense) ProtVer
-> Encode 'Open (ShelleyPpupPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> ProtVer -> Encode ('Closed 'Dense) ProtVer
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 = Decode ('Closed 'Dense) (ShelleyPpupPredFailure era)
-> Decoder s (ShelleyPpupPredFailure era)
forall t (w :: Wrapped) s. Typeable t => Decode w t -> Decoder s t
decode (Decode ('Closed 'Dense) (ShelleyPpupPredFailure era)
 -> Decoder s (ShelleyPpupPredFailure era))
-> ((Word -> Decode 'Open (ShelleyPpupPredFailure era))
    -> Decode ('Closed 'Dense) (ShelleyPpupPredFailure era))
-> (Word -> Decode 'Open (ShelleyPpupPredFailure era))
-> Decoder s (ShelleyPpupPredFailure era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text
-> (Word -> Decode 'Open (ShelleyPpupPredFailure era))
-> Decode ('Closed 'Dense) (ShelleyPpupPredFailure era)
forall t.
Text -> (Word -> Decode 'Open t) -> Decode ('Closed 'Dense) t
Summands Text
"ShelleyPpupPredFailure" ((Word -> Decode 'Open (ShelleyPpupPredFailure era))
 -> Decoder s (ShelleyPpupPredFailure era))
-> (Word -> Decode 'Open (ShelleyPpupPredFailure era))
-> Decoder s (ShelleyPpupPredFailure era)
forall a b. (a -> b) -> a -> b
$ \case
    Word
0 -> (Mismatch 'RelSubset (Set (KeyHash 'Genesis))
 -> ShelleyPpupPredFailure era)
-> Decode
     'Open
     (Mismatch 'RelSubset (Set (KeyHash 'Genesis))
      -> ShelleyPpupPredFailure era)
forall t. t -> Decode 'Open t
SumD Mismatch 'RelSubset (Set (KeyHash 'Genesis))
-> ShelleyPpupPredFailure era
forall era.
Mismatch 'RelSubset (Set (KeyHash 'Genesis))
-> ShelleyPpupPredFailure era
NonGenesisUpdatePPUP Decode
  'Open
  (Mismatch 'RelSubset (Set (KeyHash 'Genesis))
   -> ShelleyPpupPredFailure era)
-> Decode
     ('Closed Any) (Mismatch 'RelSubset (Set (KeyHash 'Genesis)))
-> Decode 'Open (ShelleyPpupPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (Mismatch 'RelSubset (Set (KeyHash 'Genesis)))
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
1 -> (EpochNo -> EpochNo -> VotingPeriod -> ShelleyPpupPredFailure era)
-> Decode
     'Open
     (EpochNo -> EpochNo -> VotingPeriod -> ShelleyPpupPredFailure era)
forall t. t -> Decode 'Open t
SumD EpochNo -> EpochNo -> VotingPeriod -> ShelleyPpupPredFailure era
forall era.
EpochNo -> EpochNo -> VotingPeriod -> ShelleyPpupPredFailure era
PPUpdateWrongEpoch Decode
  'Open
  (EpochNo -> EpochNo -> VotingPeriod -> ShelleyPpupPredFailure era)
-> Decode ('Closed Any) EpochNo
-> Decode
     'Open (EpochNo -> VotingPeriod -> ShelleyPpupPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) EpochNo
forall t (w :: Wrapped). DecCBOR t => Decode w t
From Decode
  'Open (EpochNo -> VotingPeriod -> ShelleyPpupPredFailure era)
-> Decode ('Closed Any) EpochNo
-> Decode 'Open (VotingPeriod -> ShelleyPpupPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) EpochNo
forall t (w :: Wrapped). DecCBOR t => Decode w t
From Decode 'Open (VotingPeriod -> ShelleyPpupPredFailure era)
-> Decode ('Closed Any) VotingPeriod
-> Decode 'Open (ShelleyPpupPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) VotingPeriod
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
2 -> (ProtVer -> ShelleyPpupPredFailure era)
-> Decode 'Open (ProtVer -> ShelleyPpupPredFailure era)
forall t. t -> Decode 'Open t
SumD ProtVer -> ShelleyPpupPredFailure era
forall era. ProtVer -> ShelleyPpupPredFailure era
PVCannotFollowPPUP Decode 'Open (ProtVer -> ShelleyPpupPredFailure era)
-> Decode ('Closed Any) ProtVer
-> Decode 'Open (ShelleyPpupPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) ProtVer
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
k -> Word -> Decode 'Open (ShelleyPpupPredFailure era)
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) GenDelegPair
genDelegs)
      , pps :: State (ShelleyPPUP era)
pps@( ShelleyGovState
                { sgsCurProposals :: forall era. ShelleyGovState era -> ProposedPPUpdates era
sgsCurProposals = ProposedPPUpdates Map (KeyHash 'Genesis) (PParamsUpdate era)
pupS
                , sgsFutureProposals :: forall era. ShelleyGovState era -> ProposedPPUpdates era
sgsFutureProposals = ProposedPPUpdates Map (KeyHash 'Genesis) (PParamsUpdate era)
fpupS
                }
              )
      , Signal (ShelleyPPUP era)
update
      ) <-
    Rule
  (ShelleyPPUP era)
  'Transition
  (RuleContext 'Transition (ShelleyPPUP era))
F (Clause (ShelleyPPUP era) 'Transition) (TRC (ShelleyPPUP era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext

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

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

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

      if SlotNo
slot SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
< SlotNo
tooLate
        then do
          (EpochNo
curEpochNo EpochNo -> EpochNo -> Bool
forall a. Eq a => a -> a -> Bool
== EpochNo
targetEpochNo)
            Bool
-> PredicateFailure (ShelleyPPUP era)
-> Rule (ShelleyPPUP era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! EpochNo -> EpochNo -> VotingPeriod -> ShelleyPpupPredFailure era
forall era.
EpochNo -> EpochNo -> VotingPeriod -> ShelleyPpupPredFailure era
PPUpdateWrongEpoch EpochNo
curEpochNo EpochNo
targetEpochNo VotingPeriod
VoteForThisEpoch
          let curProposals :: ProposedPPUpdates era
curProposals = Map (KeyHash 'Genesis) (PParamsUpdate era) -> ProposedPPUpdates era
forall era.
Map (KeyHash 'Genesis) (PParamsUpdate era) -> ProposedPPUpdates era
ProposedPPUpdates (Exp (Map (KeyHash 'Genesis) (PParamsUpdate era))
-> Map (KeyHash 'Genesis) (PParamsUpdate era)
forall s t. Embed s t => Exp t -> s
eval (Map (KeyHash 'Genesis) (PParamsUpdate era)
pupS Map (KeyHash 'Genesis) (PParamsUpdate era)
-> Map (KeyHash 'Genesis) (PParamsUpdate era)
-> Exp (Map (KeyHash 'Genesis) (PParamsUpdate era))
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) (PParamsUpdate era)
pup))
          !Word64
coreNodeQuorum <- BaseM (ShelleyPPUP era) Word64
-> Rule (ShelleyPPUP era) 'Transition Word64
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (ShelleyPPUP era) Word64
 -> Rule (ShelleyPPUP era) 'Transition Word64)
-> BaseM (ShelleyPPUP era) Word64
-> Rule (ShelleyPPUP era) 'Transition Word64
forall a b. (a -> b) -> a -> b
$ (Globals -> Word64) -> ReaderT Globals Identity Word64
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> Word64
quorum
          ShelleyGovState era
-> F (Clause (ShelleyPPUP era) 'Transition) (ShelleyGovState era)
forall a. a -> F (Clause (ShelleyPPUP era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ShelleyGovState era
 -> F (Clause (ShelleyPPUP era) 'Transition) (ShelleyGovState era))
-> ShelleyGovState era
-> F (Clause (ShelleyPPUP era) 'Transition) (ShelleyGovState era)
forall a b. (a -> b) -> a -> b
$
            State (ShelleyPPUP era)
pps
              { sgsCurProposals = curProposals
              , sgsFutureProposals = ProposedPPUpdates fpupS
              , sgsFuturePParams =
                  PotentialPParamsUpdate $ votedFuturePParams curProposals pp coreNodeQuorum
              }
        else do
          (EpochNo -> EpochNo
forall a. Enum a => a -> a
succ EpochNo
curEpochNo EpochNo -> EpochNo -> Bool
forall a. Eq a => a -> a -> Bool
== EpochNo
targetEpochNo)
            Bool
-> PredicateFailure (ShelleyPPUP era)
-> Rule (ShelleyPPUP era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! EpochNo -> EpochNo -> VotingPeriod -> ShelleyPpupPredFailure era
forall era.
EpochNo -> EpochNo -> VotingPeriod -> ShelleyPpupPredFailure era
PPUpdateWrongEpoch EpochNo
curEpochNo EpochNo
targetEpochNo VotingPeriod
VoteForNextEpoch
          ShelleyGovState era
-> F (Clause (ShelleyPPUP era) 'Transition) (ShelleyGovState era)
forall a. a -> F (Clause (ShelleyPPUP era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ShelleyGovState era
 -> F (Clause (ShelleyPPUP era) 'Transition) (ShelleyGovState era))
-> ShelleyGovState era
-> F (Clause (ShelleyPPUP era) 'Transition) (ShelleyGovState era)
forall a b. (a -> b) -> a -> b
$
            State (ShelleyPPUP era)
pps
              { sgsCurProposals = ProposedPPUpdates pupS
              , sgsFutureProposals = ProposedPPUpdates (eval (fpupS ⨃ 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) (PParamsUpdate era)
pppu) PParams era
pp Word64
quorumN = do
  let votes :: Map (PParamsUpdate era) Word64
votes =
        (PParamsUpdate era
 -> Map (PParamsUpdate era) Word64
 -> Map (PParamsUpdate era) Word64)
-> Map (PParamsUpdate era) Word64
-> Map (KeyHash 'Genesis) (PParamsUpdate era)
-> Map (PParamsUpdate era) Word64
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr
          (\PParamsUpdate era
vote -> (Word64 -> Word64 -> Word64)
-> PParamsUpdate era
-> Word64
-> Map (PParamsUpdate era) Word64
-> Map (PParamsUpdate era) Word64
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
(+) PParamsUpdate era
vote Word64
1)
          (Map (PParamsUpdate era) Word64
forall k a. Map k a
Map.empty :: Map.Map (PParamsUpdate era) Word64)
          Map (KeyHash 'Genesis) (PParamsUpdate era)
pppu
      consensus :: Map (PParamsUpdate era) Word64
consensus = (Word64 -> Bool)
-> Map (PParamsUpdate era) Word64 -> Map (PParamsUpdate era) Word64
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Word64 -> Word64 -> Bool
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] <- [PParamsUpdate era] -> Maybe [PParamsUpdate era]
forall a. a -> Maybe a
Just ([PParamsUpdate era] -> Maybe [PParamsUpdate era])
-> [PParamsUpdate era] -> Maybe [PParamsUpdate era]
forall a b. (a -> b) -> a -> b
$ Map (PParamsUpdate era) Word64 -> [PParamsUpdate era]
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 = PParams era -> PParamsUpdate era -> PParams era
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
  Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$
    Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (PParams era
ppNew PParams era -> Getting Word32 (PParams era) Word32 -> Word32
forall s a. s -> Getting a s a -> a
^. Getting Word32 (PParams era) Word32
forall era. EraPParams era => Lens' (PParams era) Word32
Lens' (PParams era) Word32
ppMaxTxSizeL) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Word16 -> Integer
forall a. Integral a => a -> Integer
toInteger (PParams era
ppNew PParams era -> Getting Word16 (PParams era) Word16 -> Word16
forall s a. s -> Getting a s a -> a
^. Getting Word16 (PParams era) Word16
forall era. EraPParams era => Lens' (PParams era) Word16
Lens' (PParams era) Word16
ppMaxBHSizeL)
      Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (PParams era
ppNew PParams era -> Getting Word32 (PParams era) Word32 -> Word32
forall s a. s -> Getting a s a -> a
^. Getting Word32 (PParams era) Word32
forall era. EraPParams era => Lens' (PParams era) Word32
Lens' (PParams era) Word32
ppMaxBBSizeL)
  PParams era -> Maybe (PParams era)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure PParams era
ppNew