{-# 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 qualified Cardano.Ledger.Crypto as CC (Crypto (HASH))
import Cardano.Ledger.Keys (KeyHash (..), KeyRole (..))
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 (EraCrypto era)) -- 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 (EraCrypto era)) -- Stake Pool ID
  | PoolMedataHashTooBig
      !(KeyHash 'StakePool (EraCrypto era)) -- 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 c) = ShelleyPoolPredFailure (ShelleyEra c)

instance InjectRuleFailure "POOL" ShelleyPoolPredFailure (ShelleyEra c)

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 (EraCrypto era)

  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 (EraCrypto era),
 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 (EraCrypto era))
  | ReregisterPool (KeyHash 'StakePool (EraCrypto era))
  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 (EraCrypto era)
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 (EraCrypto era)
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 (EraCrypto era)
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 (EraCrypto era)
c
    PoolMedataHashTooBig KeyHash 'StakePool (EraCrypto era)
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 (EraCrypto era)
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 (EraCrypto era)
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 (EraCrypto era) -> ShelleyPoolPredFailure era
StakePoolNotRegisteredOnKeyPOOL KeyHash 'StakePool (EraCrypto era)
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 (EraCrypto era)
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 (EraCrypto era) -> ShelleyPoolPredFailure era
WrongNetworkPOOL (forall (r :: Relation) a. a -> a -> Mismatch r a
Mismatch Network
suppliedNetId Network
expectedNetId) KeyHash 'StakePool (EraCrypto era)
poolId)
      Word
5 -> do
        KeyHash 'StakePool (EraCrypto era)
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 (EraCrypto era)
-> Int -> ShelleyPoolPredFailure era
PoolMedataHashTooBig KeyHash 'StakePool (EraCrypto era)
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 (EraCrypto era)
  , 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 (EraCrypto era),
 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 (EraCrypto era)) (PoolParams (EraCrypto era))
psStakePoolParams :: forall era.
PState era
-> Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
psStakePoolParams :: Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
psStakePoolParams, Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
psFutureStakePoolParams :: forall era.
PState era
-> Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
psFutureStakePoolParams :: Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
psFutureStakePoolParams, Map (KeyHash 'StakePool (EraCrypto era)) EpochNo
psRetiring :: forall era.
PState era -> Map (KeyHash 'StakePool (EraCrypto era)) EpochNo
psRetiring :: Map (KeyHash 'StakePool (EraCrypto era)) 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 (EraCrypto era)
poolParams@PoolParams {KeyHash 'StakePool (EraCrypto era)
ppId :: forall c. PoolParams c -> KeyHash 'StakePool c
ppId :: KeyHash 'StakePool (EraCrypto era)
ppId, RewardAccount (EraCrypto era)
ppRewardAccount :: forall c. PoolParams c -> RewardAccount c
ppRewardAccount :: RewardAccount (EraCrypto era)
ppRewardAccount, StrictMaybe PoolMetadata
ppMetadata :: forall c. PoolParams c -> StrictMaybe PoolMetadata
ppMetadata :: StrictMaybe PoolMetadata
ppMetadata, Coin
ppCost :: forall c. PoolParams c -> 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 = forall c. RewardAccount c -> Network
raNetwork RewardAccount (EraCrypto era)
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 (EraCrypto era) -> ShelleyPoolPredFailure era
WrongNetworkPOOL
              Mismatch
                { mismatchSupplied :: Network
mismatchSupplied = Network
suppliedNetID
                , mismatchExpected :: Network
mismatchExpected = Network
actualNetID
                }
              KeyHash 'StakePool (EraCrypto era)
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 ([] @(CC.HASH (EraCrypto era))))
                  forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era.
KeyHash 'StakePool (EraCrypto era)
-> Int -> ShelleyPoolPredFailure era
PoolMedataHashTooBig KeyHash 'StakePool (EraCrypto era)
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 (EraCrypto era)
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 (EraCrypto era)) (PoolParams (EraCrypto era))
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 (EraCrypto era) -> PoolEvent era
RegisterPool KeyHash 'StakePool (EraCrypto era)
ppId
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
            forall era.
EraPParams era =>
KeyHash 'StakePool (EraCrypto era)
-> PParams era -> PState era -> PState era
payPoolDeposit KeyHash 'StakePool (EraCrypto era)
ppId PParams era
pp forall a b. (a -> b) -> a -> b
$
              State (ledger era)
ps {psStakePoolParams :: Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
psStakePoolParams = forall s t. Embed s t => Exp t -> s
eval (Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
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 (EraCrypto era)
ppId PoolParams (EraCrypto era)
poolParams)}
        else do
          forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent forall a b. (a -> b) -> a -> b
$ forall era. KeyHash 'StakePool (EraCrypto era) -> PoolEvent era
ReregisterPool KeyHash 'StakePool (EraCrypto era)
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 (EraCrypto era)) (PoolParams (EraCrypto era))
psFutureStakePoolParams = forall s t. Embed s t => Exp t -> s
eval (Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
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 (EraCrypto era)
ppId PoolParams (EraCrypto era)
poolParams)
              , psRetiring :: Map (KeyHash 'StakePool (EraCrypto era)) EpochNo
psRetiring = forall s t. Embed s t => Exp t -> s
eval (forall k. Ord k => k -> Exp (Single k ())
setSingleton KeyHash 'StakePool (EraCrypto era)
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 (EraCrypto era)) EpochNo
psRetiring)
              }
    RetirePool KeyHash 'StakePool (EraCrypto era)
hk EpochNo
e -> do
      forall s t. Embed s t => Exp t -> s
eval (KeyHash 'StakePool (EraCrypto era)
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 (EraCrypto era)) (PoolParams (EraCrypto era))
psStakePoolParams) forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era.
KeyHash 'StakePool (EraCrypto era) -> ShelleyPoolPredFailure era
StakePoolNotRegisteredOnKeyPOOL KeyHash 'StakePool (EraCrypto era)
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 (EraCrypto era)) EpochNo
psRetiring = forall s t. Embed s t => Exp t -> s
eval (Map (KeyHash 'StakePool (EraCrypto era)) 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 (EraCrypto era)
hk EpochNo
e)}