{-# 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 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
      -- note that pattern match is used instead of cwitness, as in the spec

      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 -- register new, Pool-Reg

          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
      -- 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 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