{-# 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 x. PoolEnv era -> Rep (PoolEnv era) x)
-> (forall x. Rep (PoolEnv era) x -> PoolEnv era)
-> Generic (PoolEnv era)
forall x. Rep (PoolEnv era) x -> PoolEnv era
forall x. PoolEnv era -> Rep (PoolEnv era) x
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
$cfrom :: forall era x. PoolEnv era -> Rep (PoolEnv era) x
from :: forall x. PoolEnv era -> Rep (PoolEnv era) x
$cto :: forall era x. Rep (PoolEnv era) x -> PoolEnv era
to :: forall x. Rep (PoolEnv era) x -> PoolEnv era
Generic)

instance EraPParams era => EncCBOR (PoolEnv era) where
  encCBOR :: PoolEnv era -> Encoding
encCBOR (PoolEnv EpochNo
e PParams era
pp) =
    Encode ('Closed 'Dense) (PoolEnv era) -> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode (Encode ('Closed 'Dense) (PoolEnv era) -> Encoding)
-> Encode ('Closed 'Dense) (PoolEnv era) -> Encoding
forall a b. (a -> b) -> a -> b
$
      (EpochNo -> PParams era -> PoolEnv era)
-> Encode ('Closed 'Dense) (EpochNo -> PParams era -> PoolEnv era)
forall t. t -> Encode ('Closed 'Dense) t
Rec EpochNo -> PParams era -> PoolEnv era
forall era. EpochNo -> PParams era -> PoolEnv era
PoolEnv
        Encode ('Closed 'Dense) (EpochNo -> PParams era -> PoolEnv era)
-> Encode ('Closed 'Dense) EpochNo
-> Encode ('Closed 'Dense) (PParams era -> PoolEnv era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> EpochNo -> Encode ('Closed 'Dense) EpochNo
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To EpochNo
e
        Encode ('Closed 'Dense) (PParams era -> PoolEnv era)
-> Encode ('Closed 'Dense) (PParams era)
-> Encode ('Closed 'Dense) (PoolEnv era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> PParams era -> Encode ('Closed 'Dense) (PParams era)
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
(ShelleyPoolPredFailure era -> ShelleyPoolPredFailure era -> Bool)
-> (ShelleyPoolPredFailure era
    -> ShelleyPoolPredFailure era -> Bool)
-> Eq (ShelleyPoolPredFailure era)
forall era.
ShelleyPoolPredFailure era -> ShelleyPoolPredFailure era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall era.
ShelleyPoolPredFailure era -> ShelleyPoolPredFailure era -> Bool
== :: ShelleyPoolPredFailure era -> ShelleyPoolPredFailure era -> Bool
$c/= :: forall era.
ShelleyPoolPredFailure era -> ShelleyPoolPredFailure era -> Bool
/= :: ShelleyPoolPredFailure era -> ShelleyPoolPredFailure era -> Bool
Eq, Int -> ShelleyPoolPredFailure era -> ShowS
[ShelleyPoolPredFailure era] -> ShowS
ShelleyPoolPredFailure era -> String
(Int -> ShelleyPoolPredFailure era -> ShowS)
-> (ShelleyPoolPredFailure era -> String)
-> ([ShelleyPoolPredFailure era] -> ShowS)
-> Show (ShelleyPoolPredFailure era)
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
$cshowsPrec :: forall era. Int -> ShelleyPoolPredFailure era -> ShowS
showsPrec :: Int -> ShelleyPoolPredFailure era -> ShowS
$cshow :: forall era. ShelleyPoolPredFailure era -> String
show :: ShelleyPoolPredFailure era -> String
$cshowList :: forall era. [ShelleyPoolPredFailure era] -> ShowS
showList :: [ShelleyPoolPredFailure era] -> ShowS
Show, (forall x.
 ShelleyPoolPredFailure era -> Rep (ShelleyPoolPredFailure era) x)
-> (forall x.
    Rep (ShelleyPoolPredFailure era) x -> ShelleyPoolPredFailure era)
-> Generic (ShelleyPoolPredFailure era)
forall x.
Rep (ShelleyPoolPredFailure era) x -> ShelleyPoolPredFailure era
forall x.
ShelleyPoolPredFailure era -> Rep (ShelleyPoolPredFailure era) x
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
$cfrom :: forall era x.
ShelleyPoolPredFailure era -> Rep (ShelleyPoolPredFailure era) x
from :: forall x.
ShelleyPoolPredFailure era -> Rep (ShelleyPoolPredFailure era) x
$cto :: forall era x.
Rep (ShelleyPoolPredFailure era) x -> ShelleyPoolPredFailure era
to :: forall x.
Rep (ShelleyPoolPredFailure era) x -> ShelleyPoolPredFailure era
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 = [TransitionRule (ShelleyPOOL era)
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 x. PoolEvent era -> Rep (PoolEvent era) x)
-> (forall x. Rep (PoolEvent era) x -> PoolEvent era)
-> Generic (PoolEvent era)
forall x. Rep (PoolEvent era) x -> PoolEvent era
forall x. PoolEvent era -> Rep (PoolEvent era) x
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
$cfrom :: forall era x. PoolEvent era -> Rep (PoolEvent era) x
from :: forall x. PoolEvent era -> Rep (PoolEvent era) x
$cto :: forall era x. Rep (PoolEvent era) x -> PoolEvent era
to :: forall x. Rep (PoolEvent era) x -> PoolEvent era
Generic, PoolEvent era -> PoolEvent era -> Bool
(PoolEvent era -> PoolEvent era -> Bool)
-> (PoolEvent era -> PoolEvent era -> Bool) -> Eq (PoolEvent era)
forall era. PoolEvent era -> PoolEvent era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall era. PoolEvent era -> PoolEvent era -> Bool
== :: PoolEvent era -> PoolEvent era -> Bool
$c/= :: forall era. PoolEvent era -> PoolEvent era -> Bool
/= :: 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 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
0 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> KeyHash 'StakePool -> Encoding
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
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
1 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> EpochNo -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR EpochNo
gtExpected
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> EpochNo -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR EpochNo
ltSupplied
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> EpochNo -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR EpochNo
ltExpected
    StakePoolCostTooLowPOOL (Mismatch Coin
supplied Coin
expected) ->
      Word -> Encoding
encodeListLen Word
3 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
3 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Coin -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Coin
supplied Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Coin -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Coin
expected
    WrongNetworkPOOL (Mismatch Network
supplied Network
expected) KeyHash 'StakePool
c ->
      Word -> Encoding
encodeListLen Word
4 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
4 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Network -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Network
expected Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Network -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Network
supplied Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> KeyHash 'StakePool -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR KeyHash 'StakePool
c
    PoolMedataHashTooBig KeyHash 'StakePool
a Int
b ->
      Word -> Encoding
encodeListLen Word
3 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
5 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> KeyHash 'StakePool -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR KeyHash 'StakePool
a Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Int -> Encoding
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 = Text
-> (Word -> Decoder s (Int, ShelleyPoolPredFailure era))
-> Decoder s (ShelleyPoolPredFailure era)
forall s a. Text -> (Word -> Decoder s (Int, a)) -> Decoder s a
decodeRecordSum Text
"PredicateFailure (POOL era)" ((Word -> Decoder s (Int, ShelleyPoolPredFailure era))
 -> Decoder s (ShelleyPoolPredFailure era))
-> (Word -> Decoder s (Int, ShelleyPoolPredFailure era))
-> Decoder s (ShelleyPoolPredFailure era)
forall a b. (a -> b) -> a -> b
$
    \case
      Word
0 -> do
        KeyHash 'StakePool
kh <- Decoder s (KeyHash 'StakePool)
forall s. Decoder s (KeyHash 'StakePool)
forall a s. DecCBOR a => Decoder s a
decCBOR
        (Int, ShelleyPoolPredFailure era)
-> Decoder s (Int, ShelleyPoolPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, KeyHash 'StakePool -> ShelleyPoolPredFailure era
forall era. KeyHash 'StakePool -> ShelleyPoolPredFailure era
StakePoolNotRegisteredOnKeyPOOL KeyHash 'StakePool
kh)
      Word
1 -> do
        EpochNo
gtExpected <- Decoder s EpochNo
forall s. Decoder s EpochNo
forall a s. DecCBOR a => Decoder s a
decCBOR
        EpochNo
ltSupplied <- Decoder s EpochNo
forall s. Decoder s EpochNo
forall a s. DecCBOR a => Decoder s a
decCBOR
        EpochNo
ltExpected <- Decoder s EpochNo
forall s. Decoder s EpochNo
forall a s. DecCBOR a => Decoder s a
decCBOR
        (Int, ShelleyPoolPredFailure era)
-> Decoder s (Int, ShelleyPoolPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
          ( Int
4
          , Mismatch 'RelGT EpochNo
-> Mismatch 'RelLTEQ EpochNo -> ShelleyPoolPredFailure era
forall era.
Mismatch 'RelGT EpochNo
-> Mismatch 'RelLTEQ EpochNo -> ShelleyPoolPredFailure era
StakePoolRetirementWrongEpochPOOL
              (EpochNo -> EpochNo -> Mismatch 'RelGT EpochNo
forall (r :: Relation) a. a -> a -> Mismatch r a
Mismatch EpochNo
ltSupplied EpochNo
gtExpected)
              (EpochNo -> EpochNo -> Mismatch 'RelLTEQ EpochNo
forall (r :: Relation) a. a -> a -> Mismatch r a
Mismatch EpochNo
ltSupplied EpochNo
ltExpected)
          )
      Word
2 -> String -> Decoder s (Int, ShelleyPoolPredFailure era)
forall a. String -> Decoder s a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"WrongCertificateTypePOOL has been removed as impossible case"
      Word
3 -> do
        Coin
supplied <- Decoder s Coin
forall s. Decoder s Coin
forall a s. DecCBOR a => Decoder s a
decCBOR
        Coin
expected <- Decoder s Coin
forall s. Decoder s Coin
forall a s. DecCBOR a => Decoder s a
decCBOR
        (Int, ShelleyPoolPredFailure era)
-> Decoder s (Int, ShelleyPoolPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, Mismatch 'RelGTEQ Coin -> ShelleyPoolPredFailure era
forall era. Mismatch 'RelGTEQ Coin -> ShelleyPoolPredFailure era
StakePoolCostTooLowPOOL (Coin -> Coin -> Mismatch 'RelGTEQ Coin
forall (r :: Relation) a. a -> a -> Mismatch r a
Mismatch Coin
supplied Coin
expected))
      Word
4 -> do
        Network
expectedNetId <- Decoder s Network
forall s. Decoder s Network
forall a s. DecCBOR a => Decoder s a
decCBOR
        Network
suppliedNetId <- Decoder s Network
forall s. Decoder s Network
forall a s. DecCBOR a => Decoder s a
decCBOR
        KeyHash 'StakePool
poolId <- Decoder s (KeyHash 'StakePool)
forall s. Decoder s (KeyHash 'StakePool)
forall a s. DecCBOR a => Decoder s a
decCBOR
        (Int, ShelleyPoolPredFailure era)
-> Decoder s (Int, ShelleyPoolPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
4, Mismatch 'RelEQ Network
-> KeyHash 'StakePool -> ShelleyPoolPredFailure era
forall era.
Mismatch 'RelEQ Network
-> KeyHash 'StakePool -> ShelleyPoolPredFailure era
WrongNetworkPOOL (Network -> Network -> Mismatch 'RelEQ Network
forall (r :: Relation) a. a -> a -> Mismatch r a
Mismatch Network
suppliedNetId Network
expectedNetId) KeyHash 'StakePool
poolId)
      Word
5 -> do
        KeyHash 'StakePool
poolID <- Decoder s (KeyHash 'StakePool)
forall s. Decoder s (KeyHash 'StakePool)
forall a s. DecCBOR a => Decoder s a
decCBOR
        Int
s <- Decoder s Int
forall s. Decoder s Int
forall a s. DecCBOR a => Decoder s a
decCBOR
        (Int, ShelleyPoolPredFailure era)
-> Decoder s (Int, ShelleyPoolPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, KeyHash 'StakePool -> Int -> ShelleyPoolPredFailure era
forall era. KeyHash 'StakePool -> Int -> ShelleyPoolPredFailure era
PoolMedataHashTooBig KeyHash 'StakePool
poolID Int
s)
      Word
k -> Word -> Decoder s (Int, ShelleyPoolPredFailure era)
forall a (m :: * -> *). (Typeable 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 :: Map (KeyHash 'StakePool) PoolParams
psStakePoolParams :: forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams, Map (KeyHash 'StakePool) PoolParams
psFutureStakePoolParams :: Map (KeyHash 'StakePool) PoolParams
psFutureStakePoolParams :: forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psFutureStakePoolParams, Map (KeyHash 'StakePool) EpochNo
psRetiring :: Map (KeyHash 'StakePool) EpochNo
psRetiring :: forall era. PState era -> Map (KeyHash 'StakePool) EpochNo
psRetiring}
      , Signal (ledger era)
poolCert
      ) <-
    Rule
  (ledger era) 'Transition (RuleContext 'Transition (ledger era))
F (Clause (ledger era) 'Transition) (TRC (ledger era))
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 :: KeyHash 'StakePool
ppId :: PoolParams -> KeyHash 'StakePool
ppId, RewardAccount
ppRewardAccount :: RewardAccount
ppRewardAccount :: PoolParams -> RewardAccount
ppRewardAccount, StrictMaybe PoolMetadata
ppMetadata :: StrictMaybe PoolMetadata
ppMetadata :: PoolParams -> StrictMaybe PoolMetadata
ppMetadata, Coin
ppCost :: Coin
ppCost :: PoolParams -> Coin
ppCost} -> do
      let pv :: ProtVer
pv = PParams era
pp PParams era -> Getting ProtVer (PParams era) ProtVer -> ProtVer
forall s a. s -> Getting a s a -> a
^. Getting ProtVer (PParams era) ProtVer
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams era) ProtVer
ppProtocolVersionL
      Bool
-> F (Clause (ledger era) 'Transition) ()
-> F (Clause (ledger era) 'Transition) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ProtVer -> Bool
HardForks.validatePoolRewardAccountNetID ProtVer
pv) (F (Clause (ledger era) 'Transition) ()
 -> F (Clause (ledger era) 'Transition) ())
-> F (Clause (ledger era) 'Transition) ()
-> F (Clause (ledger era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ do
        Network
actualNetID <- BaseM (ledger era) Network -> Rule (ledger era) 'Transition Network
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (ledger era) Network
 -> Rule (ledger era) 'Transition Network)
-> BaseM (ledger era) Network
-> Rule (ledger era) 'Transition Network
forall a b. (a -> b) -> a -> b
$ (Globals -> Network) -> ReaderT Globals Identity Network
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
          Network -> Network -> Bool
forall a. Eq a => a -> a -> Bool
== Network
suppliedNetID
            Bool
-> PredicateFailure (ledger era)
-> F (Clause (ledger era) 'Transition) ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Mismatch 'RelEQ Network
-> KeyHash 'StakePool -> ShelleyPoolPredFailure era
forall era.
Mismatch 'RelEQ Network
-> KeyHash 'StakePool -> ShelleyPoolPredFailure era
WrongNetworkPOOL
              Mismatch
                { mismatchSupplied :: Network
mismatchSupplied = Network
suppliedNetID
                , mismatchExpected :: Network
mismatchExpected = Network
actualNetID
                }
              KeyHash 'StakePool
ppId

      Bool
-> F (Clause (ledger era) 'Transition) ()
-> F (Clause (ledger era) 'Transition) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ProtVer -> Bool
SoftForks.restrictPoolMetadataHash ProtVer
pv) (F (Clause (ledger era) 'Transition) ()
 -> F (Clause (ledger era) 'Transition) ())
-> F (Clause (ledger era) 'Transition) ()
-> F (Clause (ledger era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$
        StrictMaybe PoolMetadata
-> (PoolMetadata -> F (Clause (ledger era) 'Transition) ())
-> F (Clause (ledger era) 'Transition) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ StrictMaybe PoolMetadata
ppMetadata ((PoolMetadata -> F (Clause (ledger era) 'Transition) ())
 -> F (Clause (ledger era) 'Transition) ())
-> (PoolMetadata -> F (Clause (ledger era) 'Transition) ())
-> F (Clause (ledger era) 'Transition) ()
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
                Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Word -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([HASH] -> Word
forall h (proxy :: * -> *). HashAlgorithm h => proxy h -> Word
sizeHash ([] @HASH))
                  Bool
-> PredicateFailure (ledger era)
-> F (Clause (ledger era) 'Transition) ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! KeyHash 'StakePool -> Int -> ShelleyPoolPredFailure era
forall era. KeyHash 'StakePool -> Int -> ShelleyPoolPredFailure era
PoolMedataHashTooBig KeyHash 'StakePool
ppId Int
s

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

      if Exp Bool -> Bool
forall s t. Embed s t => Exp t -> s
eval (KeyHash 'StakePool
ppId KeyHash 'StakePool
-> Exp (Sett (KeyHash 'StakePool) ()) -> Exp Bool
forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∉ Map (KeyHash 'StakePool) PoolParams
-> Exp (Sett (KeyHash 'StakePool) ())
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
          Event (ledger era) -> F (Clause (ledger era) 'Transition) ()
forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent (Event (ledger era) -> F (Clause (ledger era) 'Transition) ())
-> Event (ledger era) -> F (Clause (ledger era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ KeyHash 'StakePool -> PoolEvent era
forall era. KeyHash 'StakePool -> PoolEvent era
RegisterPool KeyHash 'StakePool
ppId
          PState era -> F (Clause (ledger era) 'Transition) (PState era)
forall a. a -> F (Clause (ledger era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PState era -> F (Clause (ledger era) 'Transition) (PState era))
-> PState era -> F (Clause (ledger era) 'Transition) (PState era)
forall a b. (a -> b) -> a -> b
$
            KeyHash 'StakePool -> PParams era -> PState era -> PState era
forall era.
EraPParams era =>
KeyHash 'StakePool -> PParams era -> PState era -> PState era
payPoolDeposit KeyHash 'StakePool
ppId PParams era
pp (PState era -> PState era) -> PState era -> PState era
forall a b. (a -> b) -> a -> b
$
              State (ledger era)
ps {psStakePoolParams = eval (psStakePoolParams ⨃ singleton ppId poolParams)}
        else do
          Event (ledger era) -> F (Clause (ledger era) 'Transition) ()
forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent (Event (ledger era) -> F (Clause (ledger era) 'Transition) ())
-> Event (ledger era) -> F (Clause (ledger era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ KeyHash 'StakePool -> PoolEvent era
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.
          PState era -> F (Clause (ledger era) 'Transition) (PState era)
forall a. a -> F (Clause (ledger era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PState era -> F (Clause (ledger era) 'Transition) (PState era))
-> PState era -> F (Clause (ledger era) 'Transition) (PState era)
forall a b. (a -> b) -> a -> b
$
            State (ledger era)
ps
              { psFutureStakePoolParams = eval (psFutureStakePoolParams ⨃ singleton ppId poolParams)
              , psRetiring = eval (setSingleton ppId ⋪ psRetiring)
              }
    RetirePool KeyHash 'StakePool
hk EpochNo
e -> do
      Exp Bool -> Bool
forall s t. Embed s t => Exp t -> s
eval (KeyHash 'StakePool
hk KeyHash 'StakePool
-> Exp (Sett (KeyHash 'StakePool) ()) -> Exp Bool
forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∈ Map (KeyHash 'StakePool) PoolParams
-> Exp (Sett (KeyHash 'StakePool) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom Map (KeyHash 'StakePool) PoolParams
psStakePoolParams) Bool
-> PredicateFailure (ledger era)
-> F (Clause (ledger era) 'Transition) ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! KeyHash 'StakePool -> ShelleyPoolPredFailure era
forall era. KeyHash 'StakePool -> ShelleyPoolPredFailure era
StakePoolNotRegisteredOnKeyPOOL KeyHash 'StakePool
hk
      let maxEpoch :: EpochInterval
maxEpoch = PParams era
pp PParams era
-> Getting EpochInterval (PParams era) EpochInterval
-> EpochInterval
forall s a. s -> Getting a s a -> a
^. Getting EpochInterval (PParams era) EpochInterval
forall era. EraPParams era => Lens' (PParams era) EpochInterval
Lens' (PParams era) EpochInterval
ppEMaxL
          limitEpoch :: EpochNo
limitEpoch = EpochNo -> EpochInterval -> EpochNo
addEpochInterval EpochNo
cEpoch EpochInterval
maxEpoch
      (EpochNo
cEpoch EpochNo -> EpochNo -> Bool
forall a. Ord a => a -> a -> Bool
< EpochNo
e Bool -> Bool -> Bool
&& EpochNo
e EpochNo -> EpochNo -> Bool
forall a. Ord a => a -> a -> Bool
<= EpochNo
limitEpoch)
        Bool
-> PredicateFailure (ledger era)
-> F (Clause (ledger era) 'Transition) ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Mismatch 'RelGT EpochNo
-> Mismatch 'RelLTEQ EpochNo -> ShelleyPoolPredFailure era
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)
      PState era -> F (Clause (ledger era) 'Transition) (PState era)
forall a. a -> F (Clause (ledger era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PState era -> F (Clause (ledger era) 'Transition) (PState era))
-> PState era -> F (Clause (ledger era) 'Transition) (PState era)
forall a b. (a -> b) -> a -> b
$ State (ledger era)
ps {psRetiring = eval (psRetiring ⨃ singleton hk e)}