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

module Shelley.Spec.Ledger.STS.Pool
  ( POOL,
    PoolEnv (..),
    PredicateFailure,
    PoolPredicateFailure (..),
  )
where

import Cardano.Binary
  ( FromCBOR (..),
    ToCBOR (..),
    encodeListLen,
  )
import Cardano.Ledger.Era (Crypto, Era)
import Control.Monad.Trans.Reader (asks)
import Control.SetAlgebra (dom, eval, setSingleton, singleton, (∈), (∉), (∪), (⋪), (⨃))
import Control.State.Transition
  ( STS (..),
    TRC (..),
    TransitionRule,
    failBecause,
    judgmentContext,
    liftSTS,
    (?!),
  )
import Data.Kind (Type)
import Data.Typeable (Typeable)
import Data.Word (Word64, Word8)
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))
import Shelley.Spec.Ledger.BaseTypes (Globals (..), ShelleyBase, invalidKey)
import Shelley.Spec.Ledger.Coin (Coin)
import Shelley.Spec.Ledger.Keys (KeyHash (..), KeyRole (..))
import Shelley.Spec.Ledger.LedgerState (PState (..), emptyPState)
import Shelley.Spec.Ledger.PParams (PParams, PParams' (..))
import Shelley.Spec.Ledger.Serialization (decodeRecordSum)
import Shelley.Spec.Ledger.Slot (EpochNo (..), SlotNo, epochInfoEpoch)
import Shelley.Spec.Ledger.TxBody
  ( DCert (..),
    PoolCert (..),
    PoolParams (..),
  )

data POOL (era :: Type)

data PoolEnv era
  = PoolEnv SlotNo (PParams era)
  deriving (Int -> PoolEnv era -> ShowS
[PoolEnv era] -> ShowS
PoolEnv era -> String
(Int -> PoolEnv era -> ShowS)
-> (PoolEnv era -> String)
-> ([PoolEnv era] -> ShowS)
-> Show (PoolEnv era)
forall era. Int -> PoolEnv era -> ShowS
forall era. [PoolEnv era] -> ShowS
forall era. PoolEnv era -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PoolEnv era] -> ShowS
$cshowList :: forall era. [PoolEnv era] -> ShowS
show :: PoolEnv era -> String
$cshow :: forall era. PoolEnv era -> String
showsPrec :: Int -> PoolEnv era -> ShowS
$cshowsPrec :: forall era. Int -> PoolEnv era -> ShowS
Show, PoolEnv era -> PoolEnv era -> Bool
(PoolEnv era -> PoolEnv era -> Bool)
-> (PoolEnv era -> PoolEnv era -> Bool) -> Eq (PoolEnv era)
forall era. PoolEnv era -> PoolEnv era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PoolEnv era -> PoolEnv era -> Bool
$c/= :: forall era. PoolEnv era -> PoolEnv era -> Bool
== :: PoolEnv era -> PoolEnv era -> Bool
$c== :: forall era. PoolEnv era -> PoolEnv era -> Bool
Eq)

data PoolPredicateFailure era
  = StakePoolNotRegisteredOnKeyPOOL
      !(KeyHash 'StakePool (Crypto era)) -- KeyHash which cannot be retired since it is not registered
  | StakePoolRetirementWrongEpochPOOL
      !Word64 -- Current Epoch
      !Word64 -- The epoch listed in the Pool Retirement Certificate
      !Word64 -- The first epoch that is too far out for retirement
  | WrongCertificateTypePOOL
      !Word8 -- The disallowed certificate (this case should never happen)
  | StakePoolCostTooLowPOOL
      !Coin -- The stake pool cost listed in the Pool Registration Certificate
      !Coin -- The minimum stake pool cost listed in the protocol parameters
  deriving (Int -> PoolPredicateFailure era -> ShowS
[PoolPredicateFailure era] -> ShowS
PoolPredicateFailure era -> String
(Int -> PoolPredicateFailure era -> ShowS)
-> (PoolPredicateFailure era -> String)
-> ([PoolPredicateFailure era] -> ShowS)
-> Show (PoolPredicateFailure era)
forall era. Int -> PoolPredicateFailure era -> ShowS
forall era. [PoolPredicateFailure era] -> ShowS
forall era. PoolPredicateFailure era -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PoolPredicateFailure era] -> ShowS
$cshowList :: forall era. [PoolPredicateFailure era] -> ShowS
show :: PoolPredicateFailure era -> String
$cshow :: forall era. PoolPredicateFailure era -> String
showsPrec :: Int -> PoolPredicateFailure era -> ShowS
$cshowsPrec :: forall era. Int -> PoolPredicateFailure era -> ShowS
Show, PoolPredicateFailure era -> PoolPredicateFailure era -> Bool
(PoolPredicateFailure era -> PoolPredicateFailure era -> Bool)
-> (PoolPredicateFailure era -> PoolPredicateFailure era -> Bool)
-> Eq (PoolPredicateFailure era)
forall era.
PoolPredicateFailure era -> PoolPredicateFailure era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PoolPredicateFailure era -> PoolPredicateFailure era -> Bool
$c/= :: forall era.
PoolPredicateFailure era -> PoolPredicateFailure era -> Bool
== :: PoolPredicateFailure era -> PoolPredicateFailure era -> Bool
$c== :: forall era.
PoolPredicateFailure era -> PoolPredicateFailure era -> Bool
Eq, (forall x.
 PoolPredicateFailure era -> Rep (PoolPredicateFailure era) x)
-> (forall x.
    Rep (PoolPredicateFailure era) x -> PoolPredicateFailure era)
-> Generic (PoolPredicateFailure era)
forall x.
Rep (PoolPredicateFailure era) x -> PoolPredicateFailure era
forall x.
PoolPredicateFailure era -> Rep (PoolPredicateFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (PoolPredicateFailure era) x -> PoolPredicateFailure era
forall era x.
PoolPredicateFailure era -> Rep (PoolPredicateFailure era) x
$cto :: forall era x.
Rep (PoolPredicateFailure era) x -> PoolPredicateFailure era
$cfrom :: forall era x.
PoolPredicateFailure era -> Rep (PoolPredicateFailure era) x
Generic)

instance NoThunks (PoolPredicateFailure era)

instance Typeable era => STS (POOL era) where
  type State (POOL era) = PState (Crypto era)

  type Signal (POOL era) = DCert (Crypto era)

  type Environment (POOL era) = PoolEnv era

  type BaseM (POOL era) = ShelleyBase
  type PredicateFailure (POOL era) = PoolPredicateFailure era

  initialRules :: [InitialRule (POOL era)]
initialRules = [PState (Crypto era)
-> F (Clause (POOL era) 'Initial) (PState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure PState (Crypto era)
forall crypto. PState crypto
emptyPState]

  transitionRules :: [TransitionRule (POOL era)]
transitionRules = [TransitionRule (POOL era)
forall era. Typeable era => TransitionRule (POOL era)
poolDelegationTransition]

instance
  (Typeable era, Era era) =>
  ToCBOR (PoolPredicateFailure era)
  where
  toCBOR :: PoolPredicateFailure era -> Encoding
toCBOR = \case
    StakePoolNotRegisteredOnKeyPOOL KeyHash 'StakePool (Crypto era)
kh ->
      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
0 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> KeyHash 'StakePool (Crypto era) -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR KeyHash 'StakePool (Crypto era)
kh
    StakePoolRetirementWrongEpochPOOL Word64
ce Word64
e Word64
em ->
      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
<> Word64 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Word64
ce Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word64 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Word64
e Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word64 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Word64
em
    WrongCertificateTypePOOL Word8
ct ->
      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
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Word8
ct
    StakePoolCostTooLowPOOL Coin
pc Coin
mc ->
      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
3 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Coin -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Coin
pc Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Coin -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Coin
mc

instance
  (Era era) =>
  FromCBOR (PoolPredicateFailure era)
  where
  fromCBOR :: Decoder s (PoolPredicateFailure era)
fromCBOR = String
-> (Word -> Decoder s (Int, PoolPredicateFailure era))
-> Decoder s (PoolPredicateFailure era)
forall s a. String -> (Word -> Decoder s (Int, a)) -> Decoder s a
decodeRecordSum String
"PredicateFailure (POOL era)" ((Word -> Decoder s (Int, PoolPredicateFailure era))
 -> Decoder s (PoolPredicateFailure era))
-> (Word -> Decoder s (Int, PoolPredicateFailure era))
-> Decoder s (PoolPredicateFailure era)
forall a b. (a -> b) -> a -> b
$
    \case
      Word
0 -> do
        KeyHash 'StakePool (Crypto era)
kh <- Decoder s (KeyHash 'StakePool (Crypto era))
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, PoolPredicateFailure era)
-> Decoder s (Int, PoolPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, KeyHash 'StakePool (Crypto era) -> PoolPredicateFailure era
forall era.
KeyHash 'StakePool (Crypto era) -> PoolPredicateFailure era
StakePoolNotRegisteredOnKeyPOOL KeyHash 'StakePool (Crypto era)
kh)
      Word
1 -> do
        Word64
ce <- Decoder s Word64
forall a s. FromCBOR a => Decoder s a
fromCBOR
        Word64
e <- Decoder s Word64
forall a s. FromCBOR a => Decoder s a
fromCBOR
        Word64
em <- Decoder s Word64
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, PoolPredicateFailure era)
-> Decoder s (Int, PoolPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
4, Word64 -> Word64 -> Word64 -> PoolPredicateFailure era
forall era. Word64 -> Word64 -> Word64 -> PoolPredicateFailure era
StakePoolRetirementWrongEpochPOOL Word64
ce Word64
e Word64
em)
      Word
2 -> do
        Word8
ct <- Decoder s Word8
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, PoolPredicateFailure era)
-> Decoder s (Int, PoolPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, Word8 -> PoolPredicateFailure era
forall era. Word8 -> PoolPredicateFailure era
WrongCertificateTypePOOL Word8
ct)
      Word
3 -> do
        Coin
pc <- Decoder s Coin
forall a s. FromCBOR a => Decoder s a
fromCBOR
        Coin
mc <- Decoder s Coin
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, PoolPredicateFailure era)
-> Decoder s (Int, PoolPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, Coin -> Coin -> PoolPredicateFailure era
forall era. Coin -> Coin -> PoolPredicateFailure era
StakePoolCostTooLowPOOL Coin
pc Coin
mc)
      Word
k -> Word -> Decoder s (Int, PoolPredicateFailure era)
forall s a. Word -> Decoder s a
invalidKey Word
k

poolDelegationTransition :: Typeable era => TransitionRule (POOL era)
poolDelegationTransition :: TransitionRule (POOL era)
poolDelegationTransition = do
  TRC (PoolEnv slot pp, State (POOL era)
ps, Signal (POOL era)
c) <- F (Clause (POOL era) 'Transition) (TRC (POOL era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  let stpools :: Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
stpools = PState (Crypto era)
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
forall crypto.
PState crypto
-> Map (KeyHash 'StakePool crypto) (PoolParams crypto)
_pParams State (POOL era)
PState (Crypto era)
ps
  case Signal (POOL era)
c of
    DCertPool (RegPool poolParam) -> do
      -- note that pattern match is used instead of cwitness, as in the spec

      let poolCost :: Coin
poolCost = PoolParams (Crypto era) -> Coin
forall crypto. PoolParams crypto -> Coin
_poolCost PoolParams (Crypto era)
poolParam
          minPoolCost :: HKD Identity Coin
minPoolCost = PParams' Identity era -> HKD Identity Coin
forall (f :: * -> *) era. PParams' f era -> HKD f Coin
_minPoolCost PParams' Identity era
pp
      Coin
poolCost Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
>= Coin
HKD Identity Coin
minPoolCost Bool
-> PredicateFailure (POOL era) -> Rule (POOL era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Coin -> Coin -> PoolPredicateFailure era
forall era. Coin -> Coin -> PoolPredicateFailure era
StakePoolCostTooLowPOOL Coin
poolCost Coin
HKD Identity Coin
minPoolCost

      let hk :: KeyHash 'StakePool (Crypto era)
hk = PoolParams (Crypto era) -> KeyHash 'StakePool (Crypto era)
forall crypto. PoolParams crypto -> KeyHash 'StakePool crypto
_poolId PoolParams (Crypto era)
poolParam
      if Exp Bool -> Bool
forall s t. Embed s t => Exp t -> s
eval (KeyHash 'StakePool (Crypto era)
hk KeyHash 'StakePool (Crypto era)
-> Exp (Sett (KeyHash 'StakePool (Crypto era)) ()) -> Exp Bool
forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
 (Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> Exp (Sett (KeyHash 'StakePool (Crypto era)) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
stpools))
        then -- register new, Pool-Reg

          PState (Crypto era)
-> F (Clause (POOL era) 'Transition) (PState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PState (Crypto era)
 -> F (Clause (POOL era) 'Transition) (PState (Crypto era)))
-> PState (Crypto era)
-> F (Clause (POOL era) 'Transition) (PState (Crypto era))
forall a b. (a -> b) -> a -> b
$
            State (POOL era)
PState (Crypto era)
ps
              { _pParams :: Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
_pParams = Exp
  (Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era)))
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
forall s t. Embed s t => Exp t -> s
eval (PState (Crypto era)
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
forall crypto.
PState crypto
-> Map (KeyHash 'StakePool crypto) (PoolParams crypto)
_pParams State (POOL era)
PState (Crypto era)
ps Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> Exp
     (Single
        (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era)))
-> Exp
     (Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era)))
forall k v s1 (f :: * -> * -> *) s2 (g :: * -> * -> *).
(Show k, Show v, Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) =>
s1 -> s2 -> Exp (f k v)
 (KeyHash 'StakePool (Crypto era)
-> PoolParams (Crypto era)
-> Exp
     (Single
        (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era)))
forall k v. Ord k => k -> v -> Exp (Single k v)
singleton KeyHash 'StakePool (Crypto era)
hk PoolParams (Crypto era)
poolParam))
              }
        else do
          PState (Crypto era)
-> F (Clause (POOL era) 'Transition) (PState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PState (Crypto era)
 -> F (Clause (POOL era) 'Transition) (PState (Crypto era)))
-> PState (Crypto era)
-> F (Clause (POOL era) 'Transition) (PState (Crypto era))
forall a b. (a -> b) -> a -> b
$
            State (POOL era)
PState (Crypto era)
ps
              { _fPParams :: Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
_fPParams = Exp
  (Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era)))
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
forall s t. Embed s t => Exp t -> s
eval (PState (Crypto era)
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
forall crypto.
PState crypto
-> Map (KeyHash 'StakePool crypto) (PoolParams crypto)
_fPParams State (POOL era)
PState (Crypto era)
ps Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> Exp
     (Single
        (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era)))
-> Exp
     (Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto 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)
 (KeyHash 'StakePool (Crypto era)
-> PoolParams (Crypto era)
-> Exp
     (Single
        (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era)))
forall k v. Ord k => k -> v -> Exp (Single k v)
singleton KeyHash 'StakePool (Crypto era)
hk PoolParams (Crypto era)
poolParam)),
                _retiring :: Map (KeyHash 'StakePool (Crypto era)) EpochNo
_retiring = Exp (Map (KeyHash 'StakePool (Crypto era)) EpochNo)
-> Map (KeyHash 'StakePool (Crypto era)) EpochNo
forall s t. Embed s t => Exp t -> s
eval (KeyHash 'StakePool (Crypto era)
-> Exp (Single (KeyHash 'StakePool (Crypto era)) ())
forall k. Ord k => k -> Exp (Single k ())
setSingleton KeyHash 'StakePool (Crypto era)
hk Exp (Single (KeyHash 'StakePool (Crypto era)) ())
-> Map (KeyHash 'StakePool (Crypto era)) EpochNo
-> Exp (Map (KeyHash 'StakePool (Crypto era)) EpochNo)
forall k (g :: * -> * -> *) s1 s2 (f :: * -> * -> *) v.
(Ord k, Iter g, HasExp s1 (g k ()), HasExp s2 (f k v)) =>
s1 -> s2 -> Exp (f k v)
 PState (Crypto era)
-> Map (KeyHash 'StakePool (Crypto era)) EpochNo
forall crypto.
PState crypto -> Map (KeyHash 'StakePool crypto) EpochNo
_retiring State (POOL era)
PState (Crypto era)
ps)
              }
    DCertPool (RetirePool hk (EpochNo e)) -> do
      -- note that pattern match is used instead of cwitness, as in the spec
      Exp Bool -> Bool
forall s t. Embed s t => Exp t -> s
eval (KeyHash 'StakePool (Crypto era)
hk KeyHash 'StakePool (Crypto era)
-> Exp (Sett (KeyHash 'StakePool (Crypto era)) ()) -> Exp Bool
forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
 Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> Exp (Sett (KeyHash 'StakePool (Crypto era)) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
stpools) Bool
-> PredicateFailure (POOL era) -> Rule (POOL era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! KeyHash 'StakePool (Crypto era) -> PoolPredicateFailure era
forall era.
KeyHash 'StakePool (Crypto era) -> PoolPredicateFailure era
StakePoolNotRegisteredOnKeyPOOL KeyHash 'StakePool (Crypto era)
hk
      EpochNo Word64
cepoch <- BaseM (POOL era) EpochNo -> Rule (POOL era) 'Transition EpochNo
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (POOL era) EpochNo -> Rule (POOL era) 'Transition EpochNo)
-> BaseM (POOL era) EpochNo -> Rule (POOL 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
      let EpochNo Word64
maxEpoch = PParams' Identity era -> HKD Identity EpochNo
forall (f :: * -> *) era. PParams' f era -> HKD f EpochNo
_eMax PParams' Identity era
pp
      Word64
cepoch Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
< Word64
e Bool -> Bool -> Bool
&& Word64
e Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64
cepoch Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
maxEpoch
        Bool
-> PredicateFailure (POOL era) -> Rule (POOL era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Word64 -> Word64 -> Word64 -> PoolPredicateFailure era
forall era. Word64 -> Word64 -> Word64 -> PoolPredicateFailure era
StakePoolRetirementWrongEpochPOOL Word64
cepoch Word64
e (Word64
cepoch Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
maxEpoch)
      PState (Crypto era)
-> F (Clause (POOL era) 'Transition) (PState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PState (Crypto era)
 -> F (Clause (POOL era) 'Transition) (PState (Crypto era)))
-> PState (Crypto era)
-> F (Clause (POOL era) 'Transition) (PState (Crypto era))
forall a b. (a -> b) -> a -> b
$ State (POOL era)
PState (Crypto era)
ps {_retiring :: Map (KeyHash 'StakePool (Crypto era)) EpochNo
_retiring = Exp (Map (KeyHash 'StakePool (Crypto era)) EpochNo)
-> Map (KeyHash 'StakePool (Crypto era)) EpochNo
forall s t. Embed s t => Exp t -> s
eval (PState (Crypto era)
-> Map (KeyHash 'StakePool (Crypto era)) EpochNo
forall crypto.
PState crypto -> Map (KeyHash 'StakePool crypto) EpochNo
_retiring State (POOL era)
PState (Crypto era)
ps Map (KeyHash 'StakePool (Crypto era)) EpochNo
-> Exp (Single (KeyHash 'StakePool (Crypto era)) EpochNo)
-> Exp (Map (KeyHash 'StakePool (Crypto era)) EpochNo)
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)
 (KeyHash 'StakePool (Crypto era)
-> EpochNo
-> Exp (Single (KeyHash 'StakePool (Crypto era)) EpochNo)
forall k v. Ord k => k -> v -> Exp (Single k v)
singleton KeyHash 'StakePool (Crypto era)
hk (Word64 -> EpochNo
EpochNo Word64
e)))}
    DCertDeleg _ -> do
      PredicateFailure (POOL era) -> Rule (POOL era) 'Transition ()
forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause (PredicateFailure (POOL era) -> Rule (POOL era) 'Transition ())
-> PredicateFailure (POOL era) -> Rule (POOL era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ Word8 -> PoolPredicateFailure era
forall era. Word8 -> PoolPredicateFailure era
WrongCertificateTypePOOL Word8
0
      PState (Crypto era)
-> F (Clause (POOL era) 'Transition) (PState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure State (POOL era)
PState (Crypto era)
ps
    DCertMir _ -> do
      PredicateFailure (POOL era) -> Rule (POOL era) 'Transition ()
forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause (PredicateFailure (POOL era) -> Rule (POOL era) 'Transition ())
-> PredicateFailure (POOL era) -> Rule (POOL era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ Word8 -> PoolPredicateFailure era
forall era. Word8 -> PoolPredicateFailure era
WrongCertificateTypePOOL Word8
1
      PState (Crypto era)
-> F (Clause (POOL era) 'Transition) (PState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure State (POOL era)
PState (Crypto era)
ps
    DCertGenesis _ -> do
      PredicateFailure (POOL era) -> Rule (POOL era) 'Transition ()
forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause (PredicateFailure (POOL era) -> Rule (POOL era) 'Transition ())
-> PredicateFailure (POOL era) -> Rule (POOL era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ Word8 -> PoolPredicateFailure era
forall era. Word8 -> PoolPredicateFailure era
WrongCertificateTypePOOL Word8
2
      PState (Crypto era)
-> F (Clause (POOL era) 'Transition) (PState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure State (POOL era)
PState (Crypto era)
ps