{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeFamilies #-}

module Shelley.Spec.Ledger.STS.Ppup
  ( PPUP,
    PPUPEnv (..),
    PpupPredicateFailure (..),
    PredicateFailure,
    VotingPeriod (..),
  )
where

import Cardano.Binary
  ( FromCBOR (..),
    ToCBOR (..),
    decodeWord,
    encodeListLen,
  )
import Cardano.Ledger.Era (Crypto, Era)
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 NoThunks.Class (NoThunks (..))
import Shelley.Spec.Ledger.BaseTypes
import Shelley.Spec.Ledger.Keys
import Shelley.Spec.Ledger.LedgerState (PPUPState (..), pvCanFollow)
import Shelley.Spec.Ledger.PParams
import Shelley.Spec.Ledger.Serialization (decodeRecordSum)
import Shelley.Spec.Ledger.Slot

data PPUP era

data PPUPEnv era
  = PPUPEnv SlotNo (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)

instance Typeable era => 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

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

  transitionRules :: [TransitionRule (PPUP era)]
transitionRules = [TransitionRule (PPUP era)
forall era. Typeable era => 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 => 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)) (PParamsUpdate era)
-> ProposedPPUpdates era
forall era.
Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era)
-> ProposedPPUpdates era
ProposedPPUpdates Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era)
pupS) (Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era)
-> ProposedPPUpdates era
forall era.
Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era)
-> ProposedPPUpdates era
ProposedPPUpdates Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate 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)) (PParamsUpdate 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)) (PParamsUpdate 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)) (PParamsUpdate 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)) (PParamsUpdate 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 :: PParamsUpdate era -> Bool
goodPV = ProtVer -> StrictMaybe ProtVer -> Bool
pvCanFollow (PParams' Identity era -> HKD Identity ProtVer
forall (f :: * -> *) era. PParams' f era -> HKD f ProtVer
_protocolVersion PParams' Identity era
pp) (StrictMaybe ProtVer -> Bool)
-> (PParamsUpdate era -> StrictMaybe ProtVer)
-> PParamsUpdate era
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PParamsUpdate era -> StrictMaybe ProtVer
forall (f :: * -> *) era. PParams' f era -> HKD f ProtVer
_protocolVersion
      let badPVs :: Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era)
badPVs = (PParamsUpdate era -> Bool)
-> Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era)
-> Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era)
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Bool -> Bool
not (Bool -> Bool)
-> (PParamsUpdate era -> Bool) -> PParamsUpdate era -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PParamsUpdate era -> Bool
goodPV) Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate 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 ((PParamsUpdate era -> StrictMaybe ProtVer)
-> Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era)
-> Map (KeyHash 'Genesis (Crypto era)) (StrictMaybe ProtVer)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map PParamsUpdate era -> StrictMaybe ProtVer
forall (f :: * -> *) era. PParams' f era -> HKD f ProtVer
_protocolVersion Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate 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 <- BaseM (PPUP era) SlotNo -> Rule (PPUP era) 'Transition SlotNo
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (PPUP era) SlotNo -> Rule (PPUP era) 'Transition SlotNo)
-> BaseM (PPUP era) SlotNo -> Rule (PPUP era) 'Transition SlotNo
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
epochInfo
        EpochNo Word64
e <- HasCallStack => EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
epochInfoEpoch EpochInfo Identity
ei SlotNo
slot
        HasCallStack => EpochInfo Identity -> EpochNo -> ShelleyBase SlotNo
EpochInfo Identity -> EpochNo -> ShelleyBase SlotNo
epochInfoFirst EpochInfo Identity
ei (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)
      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
epochInfo
        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)) (PParamsUpdate era)
-> ProposedPPUpdates era
forall era.
Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era)
-> ProposedPPUpdates era
ProposedPPUpdates (Exp (Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era))
-> Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era)
forall s t. Embed s t => Exp t -> s
eval (Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era)
pupS Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era)
-> Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era)
-> Exp (Map (KeyHash 'Genesis (Crypto era)) (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 (Crypto era)) (PParamsUpdate era)
pup)))
              (Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era)
-> ProposedPPUpdates era
forall era.
Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era)
-> ProposedPPUpdates era
ProposedPPUpdates Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate 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)) (PParamsUpdate era)
-> ProposedPPUpdates era
forall era.
Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era)
-> ProposedPPUpdates era
ProposedPPUpdates Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era)
pupS)
              (Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era)
-> ProposedPPUpdates era
forall era.
Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era)
-> ProposedPPUpdates era
ProposedPPUpdates (Exp (Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era))
-> Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era)
forall s t. Embed s t => Exp t -> s
eval (Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era)
fpupS Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era)
-> Map (KeyHash 'Genesis (Crypto era)) (PParamsUpdate era)
-> Exp (Map (KeyHash 'Genesis (Crypto era)) (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 (Crypto era)) (PParamsUpdate era)
pup)))