{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Cardano.Ledger.Shelley.Rules.Pool (
  ShelleyPOOL,
  PoolEvent (..),
  PoolEnv (..),
  PredicateFailure,
  ShelleyPoolPredFailure (..),
)
where

import Cardano.Crypto.Hash.Class (sizeHash)
import Cardano.Ledger.Address (raNetwork)
import Cardano.Ledger.BaseTypes (
  EpochNo,
  Globals (..),
  Mismatch (..),
  Network,
  Relation (..),
  ShelleyBase,
  addEpochInterval,
  invalidKey,
  networkId,
 )
import Cardano.Ledger.Binary (
  DecCBOR (..),
  EncCBOR (..),
  decodeRecordSum,
  encodeListLen,
 )
import Cardano.Ledger.Binary.Coders (Encode (..), encode, (!>))
import Cardano.Ledger.Coin (Coin)
import Cardano.Ledger.PoolParams (PoolMetadata (..), PoolParams (..))
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.Era (ShelleyEra, ShelleyPOOL)
import qualified Cardano.Ledger.Shelley.HardForks as HardForks
import Cardano.Ledger.Shelley.LedgerState (PState (..), payPoolDeposit)
import qualified Cardano.Ledger.Shelley.SoftForks as SoftForks
import Control.DeepSeq
import Control.Monad (forM_, when)
import Control.Monad.Trans.Reader (asks)
import Control.SetAlgebra (dom, eval, setSingleton, singleton, (∈), (∉), (⋪), (⨃))
import Control.State.Transition (
  STS (..),
  TRC (..),
  TransitionRule,
  judgmentContext,
  liftSTS,
  tellEvent,
  (?!),
 )
import qualified Data.ByteString as BS
import Data.Kind (Type)
import Data.Word (Word8)
import GHC.Generics (Generic)
import Lens.Micro ((^.))
import NoThunks.Class (NoThunks (..))

data PoolEnv era
  = PoolEnv !EpochNo !(PParams era)
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x. Rep (PoolEnv era) x -> PoolEnv era
forall era x. PoolEnv era -> Rep (PoolEnv era) x
$cto :: forall era x. Rep (PoolEnv era) x -> PoolEnv era
$cfrom :: forall era x. PoolEnv era -> Rep (PoolEnv era) x
Generic)

instance EraPParams era => EncCBOR (PoolEnv era) where
  encCBOR :: PoolEnv era -> Encoding
encCBOR (PoolEnv EpochNo
e PParams era
pp) =
    forall (w :: Wrapped) t. Encode w t -> Encoding
encode forall a b. (a -> b) -> a -> b
$
      forall t. t -> Encode ('Closed 'Dense) t
Rec forall era. EpochNo -> PParams era -> PoolEnv era
PoolEnv
        forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To EpochNo
e
        forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To PParams era
pp

deriving instance Show (PParams era) => Show (PoolEnv era)

deriving instance Eq (PParams era) => Eq (PoolEnv era)

instance NFData (PParams era) => NFData (PoolEnv era)

data ShelleyPoolPredFailure era
  = StakePoolNotRegisteredOnKeyPOOL
      !(KeyHash 'StakePool) -- KeyHash which cannot be retired since it is not registered
  | StakePoolRetirementWrongEpochPOOL
      !(Mismatch 'RelGT EpochNo)
      !(Mismatch 'RelLTEQ EpochNo)
  | StakePoolCostTooLowPOOL
      !(Mismatch 'RelGTEQ Coin)
  | WrongNetworkPOOL
      !(Mismatch 'RelEQ Network)
      !(KeyHash 'StakePool) -- Stake Pool ID
  | PoolMedataHashTooBig
      !(KeyHash 'StakePool) -- Stake Pool ID
      !Int -- Size of the metadata hash
  deriving (ShelleyPoolPredFailure era -> ShelleyPoolPredFailure era -> Bool
forall era.
ShelleyPoolPredFailure era -> ShelleyPoolPredFailure era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ShelleyPoolPredFailure era -> ShelleyPoolPredFailure era -> Bool
$c/= :: forall era.
ShelleyPoolPredFailure era -> ShelleyPoolPredFailure era -> Bool
== :: ShelleyPoolPredFailure era -> ShelleyPoolPredFailure era -> Bool
$c== :: forall era.
ShelleyPoolPredFailure era -> ShelleyPoolPredFailure era -> Bool
Eq, Int -> ShelleyPoolPredFailure era -> ShowS
forall era. Int -> ShelleyPoolPredFailure era -> ShowS
forall era. [ShelleyPoolPredFailure era] -> ShowS
forall era. ShelleyPoolPredFailure era -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ShelleyPoolPredFailure era] -> ShowS
$cshowList :: forall era. [ShelleyPoolPredFailure era] -> ShowS
show :: ShelleyPoolPredFailure era -> String
$cshow :: forall era. ShelleyPoolPredFailure era -> String
showsPrec :: Int -> ShelleyPoolPredFailure era -> ShowS
$cshowsPrec :: forall era. Int -> ShelleyPoolPredFailure era -> ShowS
Show, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyPoolPredFailure era) x -> ShelleyPoolPredFailure era
forall era x.
ShelleyPoolPredFailure era -> Rep (ShelleyPoolPredFailure era) x
$cto :: forall era x.
Rep (ShelleyPoolPredFailure era) x -> ShelleyPoolPredFailure era
$cfrom :: forall era x.
ShelleyPoolPredFailure era -> Rep (ShelleyPoolPredFailure era) x
Generic)

type instance EraRuleFailure "POOL" ShelleyEra = ShelleyPoolPredFailure ShelleyEra

instance InjectRuleFailure "POOL" ShelleyPoolPredFailure ShelleyEra

instance NoThunks (ShelleyPoolPredFailure era)

instance NFData (ShelleyPoolPredFailure era)

instance (ShelleyEraTxCert era, EraPParams era) => STS (ShelleyPOOL era) where
  type State (ShelleyPOOL era) = PState era

  type Signal (ShelleyPOOL era) = PoolCert

  type Environment (ShelleyPOOL era) = PoolEnv era

  type BaseM (ShelleyPOOL era) = ShelleyBase
  type PredicateFailure (ShelleyPOOL era) = ShelleyPoolPredFailure era
  type Event (ShelleyPOOL era) = PoolEvent era

  transitionRules :: [TransitionRule (ShelleyPOOL era)]
transitionRules = [forall (ledger :: * -> *) era.
(EraPParams era, Signal (ledger era) ~ PoolCert,
 Environment (ledger era) ~ PoolEnv era,
 State (ledger era) ~ PState era, STS (ledger era),
 Event (ledger era) ~ PoolEvent era,
 BaseM (ledger era) ~ ShelleyBase,
 PredicateFailure (ledger era) ~ ShelleyPoolPredFailure era) =>
TransitionRule (ledger era)
poolDelegationTransition]

data PoolEvent era
  = RegisterPool (KeyHash 'StakePool)
  | ReregisterPool (KeyHash 'StakePool)
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x. Rep (PoolEvent era) x -> PoolEvent era
forall era x. PoolEvent era -> Rep (PoolEvent era) x
$cto :: forall era x. Rep (PoolEvent era) x -> PoolEvent era
$cfrom :: forall era x. PoolEvent era -> Rep (PoolEvent era) x
Generic, PoolEvent era -> PoolEvent era -> Bool
forall era. PoolEvent era -> PoolEvent era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PoolEvent era -> PoolEvent era -> Bool
$c/= :: forall era. PoolEvent era -> PoolEvent era -> Bool
== :: PoolEvent era -> PoolEvent era -> Bool
$c== :: forall era. PoolEvent era -> PoolEvent era -> Bool
Eq)

instance NFData (PoolEvent era)

instance Era era => EncCBOR (ShelleyPoolPredFailure era) where
  encCBOR :: ShelleyPoolPredFailure era -> Encoding
encCBOR = \case
    StakePoolNotRegisteredOnKeyPOOL KeyHash 'StakePool
kh ->
      Word -> Encoding
encodeListLen Word
2 forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
0 :: Word8) forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR KeyHash 'StakePool
kh
    StakePoolRetirementWrongEpochPOOL (Mismatch EpochNo
_ EpochNo
gtExpected) (Mismatch EpochNo
ltSupplied EpochNo
ltExpected) ->
      Word -> Encoding
encodeListLen Word
4
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
1 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR EpochNo
gtExpected
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR EpochNo
ltSupplied
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR EpochNo
ltExpected
    StakePoolCostTooLowPOOL (Mismatch Coin
supplied Coin
expected) ->
      Word -> Encoding
encodeListLen Word
3 forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
3 :: Word8) forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Coin
supplied forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Coin
expected
    WrongNetworkPOOL (Mismatch Network
supplied Network
expected) KeyHash 'StakePool
c ->
      Word -> Encoding
encodeListLen Word
4 forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
4 :: Word8) forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Network
expected forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Network
supplied forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR KeyHash 'StakePool
c
    PoolMedataHashTooBig KeyHash 'StakePool
a Int
b ->
      Word -> Encoding
encodeListLen Word
3 forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
5 :: Word8) forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR KeyHash 'StakePool
a forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Int
b

-- `ShelleyPoolPredFailure` is used in Conway POOL rule, so we need to keep the serialization unchanged
instance Era era => DecCBOR (ShelleyPoolPredFailure era) where
  decCBOR :: forall s. Decoder s (ShelleyPoolPredFailure era)
decCBOR = forall s a. Text -> (Word -> Decoder s (Int, a)) -> Decoder s a
decodeRecordSum Text
"PredicateFailure (POOL era)" forall a b. (a -> b) -> a -> b
$
    \case
      Word
0 -> do
        KeyHash 'StakePool
kh <- forall a s. DecCBOR a => Decoder s a
decCBOR
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era. KeyHash 'StakePool -> ShelleyPoolPredFailure era
StakePoolNotRegisteredOnKeyPOOL KeyHash 'StakePool
kh)
      Word
1 -> do
        EpochNo
gtExpected <- forall a s. DecCBOR a => Decoder s a
decCBOR
        EpochNo
ltSupplied <- forall a s. DecCBOR a => Decoder s a
decCBOR
        EpochNo
ltExpected <- forall a s. DecCBOR a => Decoder s a
decCBOR
        forall (f :: * -> *) a. Applicative f => a -> f a
pure
          ( Int
4
          , forall era.
Mismatch 'RelGT EpochNo
-> Mismatch 'RelLTEQ EpochNo -> ShelleyPoolPredFailure era
StakePoolRetirementWrongEpochPOOL
              (forall (r :: Relation) a. a -> a -> Mismatch r a
Mismatch EpochNo
ltSupplied EpochNo
gtExpected)
              (forall (r :: Relation) a. a -> a -> Mismatch r a
Mismatch EpochNo
ltSupplied EpochNo
ltExpected)
          )
      Word
2 -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"WrongCertificateTypePOOL has been removed as impossible case"
      Word
3 -> do
        Coin
supplied <- forall a s. DecCBOR a => Decoder s a
decCBOR
        Coin
expected <- forall a s. DecCBOR a => Decoder s a
decCBOR
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, forall era. Mismatch 'RelGTEQ Coin -> ShelleyPoolPredFailure era
StakePoolCostTooLowPOOL (forall (r :: Relation) a. a -> a -> Mismatch r a
Mismatch Coin
supplied Coin
expected))
      Word
4 -> do
        Network
expectedNetId <- forall a s. DecCBOR a => Decoder s a
decCBOR
        Network
suppliedNetId <- forall a s. DecCBOR a => Decoder s a
decCBOR
        KeyHash 'StakePool
poolId <- forall a s. DecCBOR a => Decoder s a
decCBOR
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
4, forall era.
Mismatch 'RelEQ Network
-> KeyHash 'StakePool -> ShelleyPoolPredFailure era
WrongNetworkPOOL (forall (r :: Relation) a. a -> a -> Mismatch r a
Mismatch Network
suppliedNetId Network
expectedNetId) KeyHash 'StakePool
poolId)
      Word
5 -> do
        KeyHash 'StakePool
poolID <- forall a s. DecCBOR a => Decoder s a
decCBOR
        Int
s <- forall a s. DecCBOR a => Decoder s a
decCBOR
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, forall era. KeyHash 'StakePool -> Int -> ShelleyPoolPredFailure era
PoolMedataHashTooBig KeyHash 'StakePool
poolID Int
s)
      Word
k -> forall (m :: * -> *) a. MonadFail m => Word -> m a
invalidKey Word
k

poolDelegationTransition ::
  forall (ledger :: Type -> Type) era.
  ( EraPParams era
  , Signal (ledger era) ~ PoolCert
  , Environment (ledger era) ~ PoolEnv era
  , State (ledger era) ~ PState era
  , STS (ledger era)
  , Event (ledger era) ~ PoolEvent era
  , BaseM (ledger era) ~ ShelleyBase
  , PredicateFailure (ledger era) ~ ShelleyPoolPredFailure era
  ) =>
  TransitionRule (ledger era)
poolDelegationTransition :: forall (ledger :: * -> *) era.
(EraPParams era, Signal (ledger era) ~ PoolCert,
 Environment (ledger era) ~ PoolEnv era,
 State (ledger era) ~ PState era, STS (ledger era),
 Event (ledger era) ~ PoolEvent era,
 BaseM (ledger era) ~ ShelleyBase,
 PredicateFailure (ledger era) ~ ShelleyPoolPredFailure era) =>
TransitionRule (ledger era)
poolDelegationTransition = do
  TRC
    ( PoolEnv EpochNo
cEpoch PParams era
pp
      , ps :: State (ledger era)
ps@PState {Map (KeyHash 'StakePool) PoolParams
psStakePoolParams :: forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams :: Map (KeyHash 'StakePool) PoolParams
psStakePoolParams, Map (KeyHash 'StakePool) PoolParams
psFutureStakePoolParams :: forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psFutureStakePoolParams :: Map (KeyHash 'StakePool) PoolParams
psFutureStakePoolParams, Map (KeyHash 'StakePool) EpochNo
psRetiring :: forall era. PState era -> Map (KeyHash 'StakePool) EpochNo
psRetiring :: Map (KeyHash 'StakePool) EpochNo
psRetiring}
      , Signal (ledger era)
poolCert
      ) <-
    forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  case Signal (ledger era)
poolCert of
    RegPool poolParams :: PoolParams
poolParams@PoolParams {KeyHash 'StakePool
ppId :: PoolParams -> KeyHash 'StakePool
ppId :: KeyHash 'StakePool
ppId, RewardAccount
ppRewardAccount :: PoolParams -> RewardAccount
ppRewardAccount :: RewardAccount
ppRewardAccount, StrictMaybe PoolMetadata
ppMetadata :: PoolParams -> StrictMaybe PoolMetadata
ppMetadata :: StrictMaybe PoolMetadata
ppMetadata, Coin
ppCost :: PoolParams -> Coin
ppCost :: Coin
ppCost} -> do
      let pv :: ProtVer
pv = PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) ProtVer
ppProtocolVersionL
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ProtVer -> Bool
HardForks.validatePoolRewardAccountNetID ProtVer
pv) forall a b. (a -> b) -> a -> b
$ do
        Network
actualNetID <- forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> Network
networkId
        let suppliedNetID :: Network
suppliedNetID = RewardAccount -> Network
raNetwork RewardAccount
ppRewardAccount
        Network
actualNetID
          forall a. Eq a => a -> a -> Bool
== Network
suppliedNetID
            forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era.
Mismatch 'RelEQ Network
-> KeyHash 'StakePool -> ShelleyPoolPredFailure era
WrongNetworkPOOL
              Mismatch
                { mismatchSupplied :: Network
mismatchSupplied = Network
suppliedNetID
                , mismatchExpected :: Network
mismatchExpected = Network
actualNetID
                }
              KeyHash 'StakePool
ppId

      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ProtVer -> Bool
SoftForks.restrictPoolMetadataHash ProtVer
pv) forall a b. (a -> b) -> a -> b
$
        forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ StrictMaybe PoolMetadata
ppMetadata forall a b. (a -> b) -> a -> b
$ \PoolMetadata
pmd ->
          let s :: Int
s = ByteString -> Int
BS.length (PoolMetadata -> ByteString
pmHash PoolMetadata
pmd)
           in Int
s
                forall a. Ord a => a -> a -> Bool
<= forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall h (proxy :: * -> *). HashAlgorithm h => proxy h -> Word
sizeHash ([] @HASH))
                  forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era. KeyHash 'StakePool -> Int -> ShelleyPoolPredFailure era
PoolMedataHashTooBig KeyHash 'StakePool
ppId Int
s

      let minPoolCost :: Coin
minPoolCost = PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) Coin
ppMinPoolCostL
      Coin
ppCost
        forall a. Ord a => a -> a -> Bool
>= Coin
minPoolCost
          forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era. Mismatch 'RelGTEQ Coin -> ShelleyPoolPredFailure era
StakePoolCostTooLowPOOL
            Mismatch
              { mismatchSupplied :: Coin
mismatchSupplied = Coin
ppCost
              , mismatchExpected :: Coin
mismatchExpected = Coin
minPoolCost
              }

      if forall s t. Embed s t => Exp t -> s
eval (KeyHash 'StakePool
ppId forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∉ forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom Map (KeyHash 'StakePool) PoolParams
psStakePoolParams)
        then do
          -- register new, Pool-Reg
          forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent forall a b. (a -> b) -> a -> b
$ forall era. KeyHash 'StakePool -> PoolEvent era
RegisterPool KeyHash 'StakePool
ppId
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
            forall era.
EraPParams era =>
KeyHash 'StakePool -> PParams era -> PState era -> PState era
payPoolDeposit KeyHash 'StakePool
ppId PParams era
pp forall a b. (a -> b) -> a -> b
$
              State (ledger era)
ps {psStakePoolParams :: Map (KeyHash 'StakePool) PoolParams
psStakePoolParams = forall s t. Embed s t => Exp t -> s
eval (Map (KeyHash 'StakePool) PoolParams
psStakePoolParams 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)
⨃ forall k v. Ord k => k -> v -> Exp (Single k v)
singleton KeyHash 'StakePool
ppId PoolParams
poolParams)}
        else do
          forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent forall a b. (a -> b) -> a -> b
$ forall era. KeyHash 'StakePool -> PoolEvent era
ReregisterPool KeyHash 'StakePool
ppId
          -- hk is already registered, so we want to reregister it. That means adding it
          -- to the Future pool params (if it is not there already), and overriding the
          -- range with the new 'poolParam', if it is (using ⨃ ). We must also unretire
          -- it, if it has been scheduled for retirement.  The deposit does not
          -- change. One pays the deposit just once. Only if it is fully retired
          -- (i.e. it's deposit has been refunded, and it has been removed from the
          -- registered pools).  does it need to pay a new deposit (at the current deposit
          -- amount). But of course, if that has happened, we cannot be in this branch of
          -- the if statement.
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
            State (ledger era)
ps
              { psFutureStakePoolParams :: Map (KeyHash 'StakePool) PoolParams
psFutureStakePoolParams = forall s t. Embed s t => Exp t -> s
eval (Map (KeyHash 'StakePool) PoolParams
psFutureStakePoolParams 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)
⨃ forall k v. Ord k => k -> v -> Exp (Single k v)
singleton KeyHash 'StakePool
ppId PoolParams
poolParams)
              , psRetiring :: Map (KeyHash 'StakePool) EpochNo
psRetiring = forall s t. Embed s t => Exp t -> s
eval (forall k. Ord k => k -> Exp (Single k ())
setSingleton KeyHash 'StakePool
ppId 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)
⋪ Map (KeyHash 'StakePool) EpochNo
psRetiring)
              }
    RetirePool KeyHash 'StakePool
hk EpochNo
e -> do
      forall s t. Embed s t => Exp t -> s
eval (KeyHash 'StakePool
hk forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∈ forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom Map (KeyHash 'StakePool) PoolParams
psStakePoolParams) forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era. KeyHash 'StakePool -> ShelleyPoolPredFailure era
StakePoolNotRegisteredOnKeyPOOL KeyHash 'StakePool
hk
      let maxEpoch :: EpochInterval
maxEpoch = PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) EpochInterval
ppEMaxL
          limitEpoch :: EpochNo
limitEpoch = EpochNo -> EpochInterval -> EpochNo
addEpochInterval EpochNo
cEpoch EpochInterval
maxEpoch
      (EpochNo
cEpoch forall a. Ord a => a -> a -> Bool
< EpochNo
e Bool -> Bool -> Bool
&& EpochNo
e forall a. Ord a => a -> a -> Bool
<= EpochNo
limitEpoch)
        forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era.
Mismatch 'RelGT EpochNo
-> Mismatch 'RelLTEQ EpochNo -> ShelleyPoolPredFailure era
StakePoolRetirementWrongEpochPOOL
          Mismatch -- 'RelGT - The supplied value should be greater than the current epoch
            { mismatchSupplied :: EpochNo
mismatchSupplied = EpochNo
e
            , mismatchExpected :: EpochNo
mismatchExpected = EpochNo
cEpoch
            }
          Mismatch -- 'RelLTEQ - The supplied value should be less then or equal to ppEMax after the current epoch
            { mismatchSupplied :: EpochNo
mismatchSupplied = EpochNo
e
            , mismatchExpected :: EpochNo
mismatchExpected = EpochNo
limitEpoch
            }
      -- We just schedule it for retirement. When it is retired we refund the deposit (see POOLREAP)
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ State (ledger era)
ps {psRetiring :: Map (KeyHash 'StakePool) EpochNo
psRetiring = forall s t. Embed s t => Exp t -> s
eval (Map (KeyHash 'StakePool) EpochNo
psRetiring 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)
⨃ forall k v. Ord k => k -> v -> Exp (Single k v)
singleton KeyHash 'StakePool
hk EpochNo
e)}