{-# 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 era
type Signal (POOL era) = DCert era
type Environment (POOL era) = PoolEnv era
type BaseM (POOL era) = ShelleyBase
type PredicateFailure (POOL era) = PoolPredicateFailure era
initialRules :: [InitialRule (POOL era)]
initialRules = [PState era -> F (Clause (POOL era) 'Initial) (PState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure PState era
forall era. PState era
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 era)
stpools = PState era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
forall era.
PState era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
_pParams State (POOL era)
PState era
ps
case Signal (POOL era)
c of
DCertPool (RegPool poolParam) -> do
let poolCost :: Coin
poolCost = PoolParams era -> Coin
forall era. PoolParams era -> Coin
_poolCost PoolParams 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 era -> KeyHash 'StakePool (Crypto era)
forall era. PoolParams era -> KeyHash 'StakePool (Crypto era)
_poolId PoolParams 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 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 era)
stpools))
then
PState era -> F (Clause (POOL era) 'Transition) (PState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PState era -> F (Clause (POOL era) 'Transition) (PState era))
-> PState era -> F (Clause (POOL era) 'Transition) (PState era)
forall a b. (a -> b) -> a -> b
$
State (POOL era)
PState era
ps
{ _pParams :: Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
_pParams = Exp (Map (KeyHash 'StakePool (Crypto era)) (PoolParams era))
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
forall s t. Embed s t => Exp t -> s
eval (PState era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
forall era.
PState era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
_pParams State (POOL era)
PState era
ps Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
-> Exp (Single (KeyHash 'StakePool (Crypto era)) (PoolParams era))
-> Exp (Map (KeyHash 'StakePool (Crypto era)) (PoolParams 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 era
-> Exp (Single (KeyHash 'StakePool (Crypto era)) (PoolParams era))
forall k v. Ord k => k -> v -> Exp (Single k v)
singleton KeyHash 'StakePool (Crypto era)
hk PoolParams era
poolParam))
}
else do
PState era -> F (Clause (POOL era) 'Transition) (PState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PState era -> F (Clause (POOL era) 'Transition) (PState era))
-> PState era -> F (Clause (POOL era) 'Transition) (PState era)
forall a b. (a -> b) -> a -> b
$
State (POOL era)
PState era
ps
{ _fPParams :: Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
_fPParams = Exp (Map (KeyHash 'StakePool (Crypto era)) (PoolParams era))
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
forall s t. Embed s t => Exp t -> s
eval (PState era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
forall era.
PState era
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
_fPParams State (POOL era)
PState era
ps Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
-> Exp (Single (KeyHash 'StakePool (Crypto era)) (PoolParams era))
-> Exp (Map (KeyHash 'StakePool (Crypto era)) (PoolParams 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 era
-> Exp (Single (KeyHash 'StakePool (Crypto era)) (PoolParams era))
forall k v. Ord k => k -> v -> Exp (Single k v)
singleton KeyHash 'StakePool (Crypto era)
hk PoolParams 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 era -> Map (KeyHash 'StakePool (Crypto era)) EpochNo
forall era.
PState era -> Map (KeyHash 'StakePool (Crypto era)) EpochNo
_retiring State (POOL era)
PState 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 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 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 era -> F (Clause (POOL era) 'Transition) (PState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PState era -> F (Clause (POOL era) 'Transition) (PState era))
-> PState era -> F (Clause (POOL era) 'Transition) (PState era)
forall a b. (a -> b) -> a -> b
$ State (POOL era)
PState 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 era -> Map (KeyHash 'StakePool (Crypto era)) EpochNo
forall era.
PState era -> Map (KeyHash 'StakePool (Crypto era)) EpochNo
_retiring State (POOL era)
PState 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 era -> F (Clause (POOL era) 'Transition) (PState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure State (POOL era)
PState 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 era -> F (Clause (POOL era) 'Transition) (PState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure State (POOL era)
PState 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 era -> F (Clause (POOL era) 'Transition) (PState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure State (POOL era)
PState era
ps