{-# 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))
| StakePoolRetirementWrongEpochPOOL
!Word64
!Word64
!Word64
| WrongCertificateTypePOOL
!Word8
| StakePoolCostTooLowPOOL
!Coin
!Coin
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
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
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
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