{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Cardano.Ledger.Shelley.Rules.Ppup
  ( PPUP,
    PPUPEnv (..),
    PpupPredicateFailure (..),
    PpupEvent (..),
    PredicateFailure,
    VotingPeriod (..),
  )
where

import Cardano.Binary
  ( FromCBOR (..),
    ToCBOR (..),
    decodeWord,
    encodeListLen,
  )
import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Core (PParamsDelta)
import qualified Cardano.Ledger.Core as Core
import Cardano.Ledger.Era (Crypto, Era)
import Cardano.Ledger.Keys
import Cardano.Ledger.Serialization (decodeRecordSum)
import Cardano.Ledger.Shelley.LedgerState (PPUPState (..), pvCanFollow)
import Cardano.Ledger.Shelley.PParams
import Cardano.Ledger.Slot
import Control.Monad.Trans.Reader (asks)
import Control.SetAlgebra (dom, eval, (⊆), (⨃))
import Control.State.Transition
import qualified Data.Map.Strict as Map
import Data.Set (Set)
import Data.Typeable (Typeable)
import Data.Word (Word8)
import GHC.Generics (Generic)
import GHC.Records
import NoThunks.Class (NoThunks (..))

data PPUP era

data PPUPEnv era
  = PPUPEnv SlotNo (Core.PParams era) (GenDelegs (Crypto era))

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
showList :: [VotingPeriod] -> ShowS
$cshowList :: [VotingPeriod] -> ShowS
show :: VotingPeriod -> String
$cshow :: VotingPeriod -> String
showsPrec :: Int -> VotingPeriod -> ShowS
$cshowsPrec :: Int -> VotingPeriod -> ShowS
Show, VotingPeriod -> VotingPeriod -> Bool
(VotingPeriod -> VotingPeriod -> Bool)
-> (VotingPeriod -> VotingPeriod -> Bool) -> Eq VotingPeriod
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. 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
$cto :: forall x. Rep VotingPeriod x -> VotingPeriod
$cfrom :: forall x. VotingPeriod -> Rep VotingPeriod x
Generic)

instance NoThunks VotingPeriod

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

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

data PpupPredicateFailure era
  = NonGenesisUpdatePPUP
      !(Set (KeyHash 'Genesis (Crypto era))) -- KeyHashes which are voting
      !(Set (KeyHash 'Genesis (Crypto era))) -- KeyHashes which should be voting
  | PPUpdateWrongEpoch
      !EpochNo -- current epoch
      !EpochNo -- intended epoch of update
      !VotingPeriod -- voting period within the epoch
  | PVCannotFollowPPUP
      !ProtVer -- the first bad protocol version
  deriving (Int -> PpupPredicateFailure era -> ShowS
[PpupPredicateFailure era] -> ShowS
PpupPredicateFailure era -> String
(Int -> PpupPredicateFailure era -> ShowS)
-> (PpupPredicateFailure era -> String)
-> ([PpupPredicateFailure era] -> ShowS)
-> Show (PpupPredicateFailure era)
forall era. Int -> PpupPredicateFailure era -> ShowS
forall era. [PpupPredicateFailure era] -> ShowS
forall era. PpupPredicateFailure era -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PpupPredicateFailure era] -> ShowS
$cshowList :: forall era. [PpupPredicateFailure era] -> ShowS
show :: PpupPredicateFailure era -> String
$cshow :: forall era. PpupPredicateFailure era -> String
showsPrec :: Int -> PpupPredicateFailure era -> ShowS
$cshowsPrec :: forall era. Int -> PpupPredicateFailure era -> ShowS
Show, PpupPredicateFailure era -> PpupPredicateFailure era -> Bool
(PpupPredicateFailure era -> PpupPredicateFailure era -> Bool)
-> (PpupPredicateFailure era -> PpupPredicateFailure era -> Bool)
-> Eq (PpupPredicateFailure era)
forall era.
PpupPredicateFailure era -> PpupPredicateFailure era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PpupPredicateFailure era -> PpupPredicateFailure era -> Bool
$c/= :: forall era.
PpupPredicateFailure era -> PpupPredicateFailure era -> Bool
== :: PpupPredicateFailure era -> PpupPredicateFailure era -> Bool
$c== :: forall era.
PpupPredicateFailure era -> PpupPredicateFailure era -> Bool
Eq, (forall x.
 PpupPredicateFailure era -> Rep (PpupPredicateFailure era) x)
-> (forall x.
    Rep (PpupPredicateFailure era) x -> PpupPredicateFailure era)
-> Generic (PpupPredicateFailure era)
forall x.
Rep (PpupPredicateFailure era) x -> PpupPredicateFailure era
forall x.
PpupPredicateFailure era -> Rep (PpupPredicateFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (PpupPredicateFailure era) x -> PpupPredicateFailure era
forall era x.
PpupPredicateFailure era -> Rep (PpupPredicateFailure era) x
$cto :: forall era x.
Rep (PpupPredicateFailure era) x -> PpupPredicateFailure era
$cfrom :: forall era x.
PpupPredicateFailure era -> Rep (PpupPredicateFailure era) x
Generic)

instance NoThunks (PpupPredicateFailure era)

newtype PpupEvent era = NewEpoch EpochNo

instance
  ( Typeable era,
    HasField "_protocolVersion" (Core.PParams era) ProtVer,
    HasField "_protocolVersion" (PParamsDelta era) (StrictMaybe ProtVer)
  ) =>
  STS (PPUP era)
  where
  type State (PPUP era) = PPUPState era
  type Signal (PPUP era) = Maybe (Update era)
  type Environment (PPUP era) = PPUPEnv era
  type BaseM (PPUP era) = ShelleyBase
  type PredicateFailure (PPUP era) = PpupPredicateFailure era
  type Event (PPUP era) = PpupEvent era

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

  transitionRules :: [TransitionRule (PPUP era)]
transitionRules = [TransitionRule (PPUP era)
forall era.
(Typeable era, HasField "_protocolVersion" (PParams era) ProtVer,
 HasField
   "_protocolVersion" (PParamsDelta era) (StrictMaybe ProtVer)) =>
TransitionRule (PPUP era)
ppupTransitionNonEmpty]

instance
  (Typeable era, Era era) =>
  ToCBOR (PpupPredicateFailure era)
  where
  toCBOR :: PpupPredicateFailure era -> Encoding
toCBOR = \case
    (NonGenesisUpdatePPUP Set (KeyHash 'Genesis (Crypto era))
a Set (KeyHash 'Genesis (Crypto era))
b) ->
      Word -> Encoding
encodeListLen Word
3
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
0 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Set (KeyHash 'Genesis (Crypto era)) -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Set (KeyHash 'Genesis (Crypto era))
a
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Set (KeyHash 'Genesis (Crypto era)) -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Set (KeyHash 'Genesis (Crypto era))
b
    PPUpdateWrongEpoch EpochNo
ce EpochNo
e VotingPeriod
vp ->
      Word -> Encoding
encodeListLen Word
4 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
1 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> EpochNo -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR EpochNo
ce Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> EpochNo -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR EpochNo
e Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> VotingPeriod -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR VotingPeriod
vp
    PVCannotFollowPPUP ProtVer
p -> Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
2 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> ProtVer -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR ProtVer
p

instance
  (Era era) =>
  FromCBOR (PpupPredicateFailure era)
  where
  fromCBOR :: Decoder s (PpupPredicateFailure era)
fromCBOR = String
-> (Word -> Decoder s (Int, PpupPredicateFailure era))
-> Decoder s (PpupPredicateFailure era)
forall s a. String -> (Word -> Decoder s (Int, a)) -> Decoder s a
decodeRecordSum String
"PredicateFailure (PPUP era)" ((Word -> Decoder s (Int, PpupPredicateFailure era))
 -> Decoder s (PpupPredicateFailure era))
-> (Word -> Decoder s (Int, PpupPredicateFailure era))
-> Decoder s (PpupPredicateFailure era)
forall a b. (a -> b) -> a -> b
$
    \case
      Word
0 -> do
        Set (KeyHash 'Genesis (Crypto era))
a <- Decoder s (Set (KeyHash 'Genesis (Crypto era)))
forall a s. FromCBOR a => Decoder s a
fromCBOR
        Set (KeyHash 'Genesis (Crypto era))
b <- Decoder s (Set (KeyHash 'Genesis (Crypto era)))
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, PpupPredicateFailure era)
-> Decoder s (Int, PpupPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, Set (KeyHash 'Genesis (Crypto era))
-> Set (KeyHash 'Genesis (Crypto era)) -> PpupPredicateFailure era
forall era.
Set (KeyHash 'Genesis (Crypto era))
-> Set (KeyHash 'Genesis (Crypto era)) -> PpupPredicateFailure era
NonGenesisUpdatePPUP Set (KeyHash 'Genesis (Crypto era))
a Set (KeyHash 'Genesis (Crypto era))
b)
      Word
1 -> do
        EpochNo
a <- Decoder s EpochNo
forall a s. FromCBOR a => Decoder s a
fromCBOR
        EpochNo
b <- Decoder s EpochNo
forall a s. FromCBOR a => Decoder s a
fromCBOR
        VotingPeriod
c <- Decoder s VotingPeriod
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, PpupPredicateFailure era)
-> Decoder s (Int, PpupPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
4, EpochNo -> EpochNo -> VotingPeriod -> PpupPredicateFailure era
forall era.
EpochNo -> EpochNo -> VotingPeriod -> PpupPredicateFailure era
PPUpdateWrongEpoch EpochNo
a EpochNo
b VotingPeriod
c)
      Word
2 -> do
        ProtVer
p <- Decoder s ProtVer
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, PpupPredicateFailure era)
-> Decoder s (Int, PpupPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, ProtVer -> PpupPredicateFailure era
forall era. ProtVer -> PpupPredicateFailure era
PVCannotFollowPPUP ProtVer
p)
      Word
k -> Word -> Decoder s (Int, PpupPredicateFailure era)
forall s a. Word -> Decoder s a
invalidKey Word
k

ppupTransitionNonEmpty ::
  ( Typeable era,
    HasField "_protocolVersion" (Core.PParams era) ProtVer,
    HasField "_protocolVersion" (PParamsDelta era) (StrictMaybe ProtVer)
  ) =>
  TransitionRule (PPUP era)
ppupTransitionNonEmpty :: TransitionRule (PPUP era)
ppupTransitionNonEmpty = do
  TRC
    ( PPUPEnv slot pp (GenDelegs _genDelegs),
      PPUPState (ProposedPPUpdates pupS) (ProposedPPUpdates fpupS),
      Signal (PPUP era)
up
      ) <-
    F (Clause (PPUP era) 'Transition) (TRC (PPUP era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext

  case Signal (PPUP era)
up of
    Signal (PPUP era)
Nothing -> PPUPState era -> F (Clause (PPUP era) 'Transition) (PPUPState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PPUPState era
 -> F (Clause (PPUP era) 'Transition) (PPUPState era))
-> PPUPState era
-> F (Clause (PPUP era) 'Transition) (PPUPState era)
forall a b. (a -> b) -> a -> b
$ ProposedPPUpdates era -> ProposedPPUpdates era -> PPUPState era
forall era.
ProposedPPUpdates era -> ProposedPPUpdates era -> PPUPState era
PPUPState (Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
-> ProposedPPUpdates era
forall era.
Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
-> ProposedPPUpdates era
ProposedPPUpdates Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
pupS) (Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
-> ProposedPPUpdates era
forall era.
Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
-> ProposedPPUpdates era
ProposedPPUpdates Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
fpupS)
    Just (Update (ProposedPPUpdates pup) te) -> do
      Exp Bool -> Bool
forall s t. Embed s t => Exp t -> s
eval (Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
-> Exp (Sett (KeyHash 'Genesis (Crypto era)) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
pup Exp (Sett (KeyHash 'Genesis (Crypto era)) ())
-> Exp (Sett (KeyHash 'Genesis (Crypto era)) ()) -> 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 (Crypto era)) (GenDelegPair (Crypto era))
-> Exp (Sett (KeyHash 'Genesis (Crypto era)) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
_genDelegs) Bool
-> PredicateFailure (PPUP era) -> Rule (PPUP era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Set (KeyHash 'Genesis (Crypto era))
-> Set (KeyHash 'Genesis (Crypto era)) -> PpupPredicateFailure era
forall era.
Set (KeyHash 'Genesis (Crypto era))
-> Set (KeyHash 'Genesis (Crypto era)) -> PpupPredicateFailure era
NonGenesisUpdatePPUP (Exp (Sett (KeyHash 'Genesis (Crypto era)) ())
-> Set (KeyHash 'Genesis (Crypto era))
forall s t. Embed s t => Exp t -> s
eval (Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
-> Exp (Sett (KeyHash 'Genesis (Crypto era)) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
pup)) (Exp (Sett (KeyHash 'Genesis (Crypto era)) ())
-> Set (KeyHash 'Genesis (Crypto era))
forall s t. Embed s t => Exp t -> s
eval (Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
-> Exp (Sett (KeyHash 'Genesis (Crypto era)) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
_genDelegs))

      let goodPV :: PParamsDelta era -> Bool
goodPV =
            ProtVer -> StrictMaybe ProtVer -> Bool
pvCanFollow (PParams era -> ProtVer
forall k (x :: k) r a. HasField x r a => r -> a
getField @"_protocolVersion" PParams era
pp)
              (StrictMaybe ProtVer -> Bool)
-> (PParamsDelta era -> StrictMaybe ProtVer)
-> PParamsDelta era
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (x :: k) r a. HasField x r a => r -> a
forall r a. HasField "_protocolVersion" r a => r -> a
getField @"_protocolVersion"
      let badPVs :: Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
badPVs = (PParamsDelta era -> Bool)
-> Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
-> Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Bool -> Bool
not (Bool -> Bool)
-> (PParamsDelta era -> Bool) -> PParamsDelta era -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PParamsDelta era -> Bool
goodPV) Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
pup
      case Map (KeyHash 'Genesis (Crypto era)) (StrictMaybe ProtVer)
-> [(KeyHash 'Genesis (Crypto era), StrictMaybe ProtVer)]
forall k a. Map k a -> [(k, a)]
Map.toList ((PParamsDelta era -> StrictMaybe ProtVer)
-> Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
-> Map (KeyHash 'Genesis (Crypto era)) (StrictMaybe ProtVer)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (forall k (x :: k) r a. HasField x r a => r -> a
forall r a. HasField "_protocolVersion" r a => r -> a
getField @"_protocolVersion") Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
badPVs) of
        ((KeyHash 'Genesis (Crypto era)
_, SJust ProtVer
pv) : [(KeyHash 'Genesis (Crypto era), StrictMaybe ProtVer)]
_) -> PredicateFailure (PPUP era) -> Rule (PPUP era) 'Transition ()
forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause (PredicateFailure (PPUP era) -> Rule (PPUP era) 'Transition ())
-> PredicateFailure (PPUP era) -> Rule (PPUP era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ ProtVer -> PpupPredicateFailure era
forall era. ProtVer -> PpupPredicateFailure era
PVCannotFollowPPUP ProtVer
pv
        [(KeyHash 'Genesis (Crypto era), StrictMaybe ProtVer)]
_ -> () -> Rule (PPUP era) 'Transition ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

      Word64
sp <- BaseM (PPUP era) Word64 -> Rule (PPUP era) 'Transition Word64
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (PPUP era) Word64 -> Rule (PPUP era) 'Transition Word64)
-> BaseM (PPUP era) Word64 -> Rule (PPUP 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
stabilityWindow
      SlotNo
firstSlotNextEpoch <- do
        EpochInfo Identity
ei <- BaseM (PPUP era) (EpochInfo Identity)
-> Rule (PPUP era) 'Transition (EpochInfo Identity)
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (PPUP era) (EpochInfo Identity)
 -> Rule (PPUP era) 'Transition (EpochInfo Identity))
-> BaseM (PPUP era) (EpochInfo Identity)
-> Rule (PPUP era) 'Transition (EpochInfo Identity)
forall a b. (a -> b) -> a -> b
$ (Globals -> EpochInfo Identity)
-> ReaderT Globals Identity (EpochInfo Identity)
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> EpochInfo Identity
epochInfoPure
        EpochNo Word64
e <- BaseM (PPUP era) EpochNo -> Rule (PPUP era) 'Transition EpochNo
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (PPUP era) EpochNo -> Rule (PPUP era) 'Transition EpochNo)
-> BaseM (PPUP era) EpochNo -> Rule (PPUP era) 'Transition EpochNo
forall a b. (a -> b) -> a -> b
$ HasCallStack => EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
epochInfoEpoch EpochInfo Identity
ei SlotNo
slot
        let newEpochNo :: EpochNo
newEpochNo = Word64 -> EpochNo
EpochNo (Word64 -> EpochNo) -> Word64 -> EpochNo
forall a b. (a -> b) -> a -> b
$ Word64
e Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1
        Event (PPUP era) -> Rule (PPUP era) 'Transition ()
forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent (Event (PPUP era) -> Rule (PPUP era) 'Transition ())
-> Event (PPUP era) -> Rule (PPUP era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ EpochNo -> PpupEvent era
forall era. EpochNo -> PpupEvent era
NewEpoch EpochNo
newEpochNo
        BaseM (PPUP era) SlotNo -> F (Clause (PPUP era) 'Transition) SlotNo
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (PPUP era) SlotNo
 -> F (Clause (PPUP era) 'Transition) SlotNo)
-> BaseM (PPUP era) SlotNo
-> F (Clause (PPUP era) 'Transition) SlotNo
forall a b. (a -> b) -> a -> b
$ HasCallStack => EpochInfo Identity -> EpochNo -> ShelleyBase SlotNo
EpochInfo Identity -> EpochNo -> ShelleyBase SlotNo
epochInfoFirst EpochInfo Identity
ei EpochNo
newEpochNo
      let tooLate :: SlotNo
tooLate = SlotNo
firstSlotNextEpoch SlotNo -> Duration -> SlotNo
*- Word64 -> Duration
Duration (Word64
2 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* Word64
sp)

      EpochNo
currentEpoch <- BaseM (PPUP era) EpochNo -> Rule (PPUP era) 'Transition EpochNo
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (PPUP era) EpochNo -> Rule (PPUP era) 'Transition EpochNo)
-> BaseM (PPUP era) EpochNo -> Rule (PPUP era) 'Transition EpochNo
forall a b. (a -> b) -> a -> b
$ do
        EpochInfo Identity
ei <- (Globals -> EpochInfo Identity)
-> ReaderT Globals Identity (EpochInfo Identity)
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> EpochInfo Identity
epochInfoPure
        HasCallStack => EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
epochInfoEpoch EpochInfo Identity
ei SlotNo
slot

      if SlotNo
slot SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
< SlotNo
tooLate
        then do
          EpochNo
currentEpoch EpochNo -> EpochNo -> Bool
forall a. Eq a => a -> a -> Bool
== EpochNo
te Bool
-> PredicateFailure (PPUP era) -> Rule (PPUP era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! EpochNo -> EpochNo -> VotingPeriod -> PpupPredicateFailure era
forall era.
EpochNo -> EpochNo -> VotingPeriod -> PpupPredicateFailure era
PPUpdateWrongEpoch EpochNo
currentEpoch EpochNo
te VotingPeriod
VoteForThisEpoch
          PPUPState era -> F (Clause (PPUP era) 'Transition) (PPUPState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PPUPState era
 -> F (Clause (PPUP era) 'Transition) (PPUPState era))
-> PPUPState era
-> F (Clause (PPUP era) 'Transition) (PPUPState era)
forall a b. (a -> b) -> a -> b
$
            ProposedPPUpdates era -> ProposedPPUpdates era -> PPUPState era
forall era.
ProposedPPUpdates era -> ProposedPPUpdates era -> PPUPState era
PPUPState
              (Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
-> ProposedPPUpdates era
forall era.
Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
-> ProposedPPUpdates era
ProposedPPUpdates (Exp (Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era))
-> Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
forall s t. Embed s t => Exp t -> s
eval (Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
pupS Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
-> Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
-> Exp (Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta 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 (Crypto era)) (PParamsDelta era)
pup)))
              (Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
-> ProposedPPUpdates era
forall era.
Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
-> ProposedPPUpdates era
ProposedPPUpdates Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
fpupS)
        else do
          EpochNo
currentEpoch EpochNo -> EpochNo -> EpochNo
forall a. Num a => a -> a -> a
+ EpochNo
1 EpochNo -> EpochNo -> Bool
forall a. Eq a => a -> a -> Bool
== EpochNo
te Bool
-> PredicateFailure (PPUP era) -> Rule (PPUP era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! EpochNo -> EpochNo -> VotingPeriod -> PpupPredicateFailure era
forall era.
EpochNo -> EpochNo -> VotingPeriod -> PpupPredicateFailure era
PPUpdateWrongEpoch EpochNo
currentEpoch EpochNo
te VotingPeriod
VoteForNextEpoch
          PPUPState era -> F (Clause (PPUP era) 'Transition) (PPUPState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PPUPState era
 -> F (Clause (PPUP era) 'Transition) (PPUPState era))
-> PPUPState era
-> F (Clause (PPUP era) 'Transition) (PPUPState era)
forall a b. (a -> b) -> a -> b
$
            ProposedPPUpdates era -> ProposedPPUpdates era -> PPUPState era
forall era.
ProposedPPUpdates era -> ProposedPPUpdates era -> PPUPState era
PPUPState
              (Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
-> ProposedPPUpdates era
forall era.
Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
-> ProposedPPUpdates era
ProposedPPUpdates Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
pupS)
              (Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
-> ProposedPPUpdates era
forall era.
Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
-> ProposedPPUpdates era
ProposedPPUpdates (Exp (Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era))
-> Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
forall s t. Embed s t => Exp t -> s
eval (Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
fpupS Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
-> Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta era)
-> Exp (Map (KeyHash 'Genesis (Crypto era)) (PParamsDelta 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 (Crypto era)) (PParamsDelta era)
pup)))