{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Cardano.Ledger.Shelley.Rules.Pool
  ( POOL,
    PoolEvent (..),
    PoolEnv (..),
    PredicateFailure,
    PoolPredicateFailure (..),
  )
where

import Cardano.Binary
  ( FromCBOR (..),
    ToCBOR (..),
    encodeListLen,
  )
import Cardano.Crypto.Hash.Class (sizeHash)
import Cardano.Ledger.BaseTypes
  ( Globals (..),
    Network,
    ProtVer,
    ShelleyBase,
    StrictMaybe (..),
    epochInfoPure,
    invalidKey,
    networkId,
  )
import Cardano.Ledger.Coin (Coin)
import qualified Cardano.Ledger.Core as Core
import qualified Cardano.Ledger.Crypto as CC (Crypto (HASH))
import Cardano.Ledger.Era (Crypto, Era)
import Cardano.Ledger.Keys (KeyHash (..), KeyRole (..))
import Cardano.Ledger.Serialization (decodeRecordSum)
import qualified Cardano.Ledger.Shelley.HardForks as HardForks
import Cardano.Ledger.Shelley.LedgerState (PState (..))
import qualified Cardano.Ledger.Shelley.SoftForks as SoftForks
import Cardano.Ledger.Shelley.TxBody
  ( DCert (..),
    PoolCert (..),
    PoolMetadata (..),
    PoolParams (..),
    getRwdNetwork,
  )
import Cardano.Ledger.Slot (EpochNo (..), SlotNo, epochInfoEpoch)
import Control.Monad (when)
import Control.Monad.Trans.Reader (asks)
import Control.SetAlgebra (dom, eval, setSingleton, singleton, (∈), (∉), (∪), (⋪), (⨃))
import Control.State.Transition
  ( STS (..),
    TRC (..),
    TransitionRule,
    failBecause,
    judgmentContext,
    liftSTS,
    tellEvent,
    (?!),
  )
import qualified Data.ByteString as BS
import Data.Kind (Type)
import Data.Typeable (Typeable)
import Data.Word (Word64, Word8)
import GHC.Generics (Generic)
import GHC.Records (HasField (getField))
import NoThunks.Class (NoThunks (..))

data POOL (era :: Type)

data PoolEnv era
  = PoolEnv SlotNo (Core.PParams era)

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

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

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
  | WrongNetworkPOOL
      !Network -- Actual Network ID
      !Network -- Network ID listed in Pool Registration Certificate
      !(KeyHash 'StakePool (Crypto era)) -- Stake Pool ID
  | PoolMedataHashTooBig
      !(KeyHash 'StakePool (Crypto era)) -- Stake Pool ID
      !Int -- Size of the metadata hash
  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
  ( Era era,
    HasField "_minPoolCost" (Core.PParams era) Coin,
    HasField "_eMax" (Core.PParams era) EpochNo,
    HasField "_protocolVersion" (Core.PParams era) ProtVer
  ) =>
  STS (POOL era)
  where
  type State (POOL era) = PState (Crypto era)

  type Signal (POOL era) = DCert (Crypto era)

  type Environment (POOL era) = PoolEnv era

  type BaseM (POOL era) = ShelleyBase
  type PredicateFailure (POOL era) = PoolPredicateFailure era
  type Event (POOL era) = PoolEvent era

  transitionRules :: [TransitionRule (POOL era)]
transitionRules = [TransitionRule (POOL era)
forall era.
(Era era, HasField "_minPoolCost" (PParams era) Coin,
 HasField "_eMax" (PParams era) EpochNo,
 HasField "_protocolVersion" (PParams era) ProtVer) =>
TransitionRule (POOL era)
poolDelegationTransition]

data PoolEvent era
  = RegisterPool (KeyHash 'StakePool (Crypto era))
  | ReregisterPool (KeyHash 'StakePool (Crypto era))

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
    WrongNetworkPOOL Network
a Network
b KeyHash 'StakePool (Crypto era)
c ->
      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
4 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Network -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Network
a Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Network -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Network
b 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)
c
    PoolMedataHashTooBig KeyHash 'StakePool (Crypto era)
a Int
b ->
      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
5 :: 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)
a Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Int -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Int
b

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
4 -> do
        Network
actualNetID <- Decoder s Network
forall a s. FromCBOR a => Decoder s a
fromCBOR
        Network
suppliedNetID <- Decoder s Network
forall a s. FromCBOR a => Decoder s a
fromCBOR
        KeyHash 'StakePool (Crypto era)
poolID <- 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
4, Network
-> Network
-> KeyHash 'StakePool (Crypto era)
-> PoolPredicateFailure era
forall era.
Network
-> Network
-> KeyHash 'StakePool (Crypto era)
-> PoolPredicateFailure era
WrongNetworkPOOL Network
actualNetID Network
suppliedNetID KeyHash 'StakePool (Crypto era)
poolID)
      Word
5 -> do
        KeyHash 'StakePool (Crypto era)
poolID <- Decoder s (KeyHash 'StakePool (Crypto era))
forall a s. FromCBOR a => Decoder s a
fromCBOR
        Int
s <- Decoder s Int
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, KeyHash 'StakePool (Crypto era) -> Int -> PoolPredicateFailure era
forall era.
KeyHash 'StakePool (Crypto era) -> Int -> PoolPredicateFailure era
PoolMedataHashTooBig KeyHash 'StakePool (Crypto era)
poolID Int
s)
      Word
k -> Word -> Decoder s (Int, PoolPredicateFailure era)
forall s a. Word -> Decoder s a
invalidKey Word
k

poolDelegationTransition ::
  forall era.
  ( Era era,
    HasField "_minPoolCost" (Core.PParams era) Coin,
    HasField "_eMax" (Core.PParams era) EpochNo,
    HasField "_protocolVersion" (Core.PParams era) ProtVer
  ) =>
  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 (Crypto era))
stpools = PState (Crypto era)
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
forall crypto.
PState crypto
-> Map (KeyHash 'StakePool crypto) (PoolParams crypto)
_pParams State (POOL era)
PState (Crypto 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

      Bool
-> F (Clause (POOL era) 'Transition) ()
-> F (Clause (POOL era) 'Transition) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (PParams era -> Bool
forall pp. HasField "_protocolVersion" pp ProtVer => pp -> Bool
HardForks.validatePoolRewardAccountNetID PParams era
pp) (F (Clause (POOL era) 'Transition) ()
 -> F (Clause (POOL era) 'Transition) ())
-> F (Clause (POOL era) 'Transition) ()
-> F (Clause (POOL era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ do
        Network
actualNetID <- BaseM (POOL era) Network -> Rule (POOL era) 'Transition Network
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (POOL era) Network -> Rule (POOL era) 'Transition Network)
-> BaseM (POOL era) Network -> Rule (POOL 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 = RewardAcnt (Crypto era) -> Network
forall crypto. RewardAcnt crypto -> Network
getRwdNetwork (PoolParams (Crypto era) -> RewardAcnt (Crypto era)
forall crypto. PoolParams crypto -> RewardAcnt crypto
_poolRAcnt PoolParams (Crypto era)
poolParam)
        Network
actualNetID Network -> Network -> Bool
forall a. Eq a => a -> a -> Bool
== Network
suppliedNetID
          Bool
-> PredicateFailure (POOL era)
-> F (Clause (POOL era) 'Transition) ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Network
-> Network
-> KeyHash 'StakePool (Crypto era)
-> PoolPredicateFailure era
forall era.
Network
-> Network
-> KeyHash 'StakePool (Crypto era)
-> PoolPredicateFailure era
WrongNetworkPOOL Network
actualNetID Network
suppliedNetID (PoolParams (Crypto era) -> KeyHash 'StakePool (Crypto era)
forall crypto. PoolParams crypto -> KeyHash 'StakePool crypto
_poolId PoolParams (Crypto era)
poolParam)

      Bool
-> F (Clause (POOL era) 'Transition) ()
-> F (Clause (POOL era) 'Transition) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (PParams era -> Bool
forall pp. HasField "_protocolVersion" pp ProtVer => pp -> Bool
SoftForks.restrictPoolMetadataHash PParams era
pp) (F (Clause (POOL era) 'Transition) ()
 -> F (Clause (POOL era) 'Transition) ())
-> F (Clause (POOL era) 'Transition) ()
-> F (Clause (POOL era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ do
        case PoolParams (Crypto era) -> StrictMaybe PoolMetadata
forall crypto. PoolParams crypto -> StrictMaybe PoolMetadata
_poolMD PoolParams (Crypto era)
poolParam of
          StrictMaybe PoolMetadata
SNothing -> () -> F (Clause (POOL era) 'Transition) ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          SJust PoolMetadata
pmd ->
            let s :: Int
s = ByteString -> Int
BS.length (PoolMetadata -> ByteString
_poolMDHash 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 (Crypto era)] -> Word
forall h (proxy :: * -> *). HashAlgorithm h => proxy h -> Word
sizeHash ([] @(CC.HASH (Crypto era))))
                  Bool
-> PredicateFailure (POOL era)
-> F (Clause (POOL era) 'Transition) ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! KeyHash 'StakePool (Crypto era) -> Int -> PoolPredicateFailure era
forall era.
KeyHash 'StakePool (Crypto era) -> Int -> PoolPredicateFailure era
PoolMedataHashTooBig (PoolParams (Crypto era) -> KeyHash 'StakePool (Crypto era)
forall crypto. PoolParams crypto -> KeyHash 'StakePool crypto
_poolId PoolParams (Crypto era)
poolParam) Int
s

      let poolCost :: Coin
poolCost = PoolParams (Crypto era) -> Coin
forall crypto. PoolParams crypto -> Coin
_poolCost PoolParams (Crypto era)
poolParam
          minPoolCost :: Coin
minPoolCost = PParams era -> Coin
forall k (x :: k) r a. HasField x r a => r -> a
getField @"_minPoolCost" PParams era
pp
      Coin
poolCost Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
>= Coin
minPoolCost Bool
-> PredicateFailure (POOL era)
-> F (Clause (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
minPoolCost

      let hk :: KeyHash 'StakePool (Crypto era)
hk = PoolParams (Crypto era) -> KeyHash 'StakePool (Crypto era)
forall crypto. PoolParams crypto -> KeyHash 'StakePool crypto
_poolId PoolParams (Crypto 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 (Crypto 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 (Crypto era))
stpools)
        then do
          -- register new, Pool-Reg
          Event (POOL era) -> F (Clause (POOL era) 'Transition) ()
forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent (Event (POOL era) -> F (Clause (POOL era) 'Transition) ())
-> Event (POOL era) -> F (Clause (POOL era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ KeyHash 'StakePool (Crypto era) -> PoolEvent era
forall era. KeyHash 'StakePool (Crypto era) -> PoolEvent era
RegisterPool KeyHash 'StakePool (Crypto era)
hk
          PState (Crypto era)
-> F (Clause (POOL era) 'Transition) (PState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PState (Crypto era)
 -> F (Clause (POOL era) 'Transition) (PState (Crypto era)))
-> PState (Crypto era)
-> F (Clause (POOL era) 'Transition) (PState (Crypto era))
forall a b. (a -> b) -> a -> b
$
            State (POOL era)
PState (Crypto era)
ps
              { _pParams :: Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
_pParams = Exp
  (Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era)))
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
forall s t. Embed s t => Exp t -> s
eval (PState (Crypto era)
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
forall crypto.
PState crypto
-> Map (KeyHash 'StakePool crypto) (PoolParams crypto)
_pParams State (POOL era)
PState (Crypto era)
ps Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> Exp
     (Single
        (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era)))
-> Exp
     (Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto 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 (Crypto era)
-> Exp
     (Single
        (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era)))
forall k v. Ord k => k -> v -> Exp (Single k v)
singleton KeyHash 'StakePool (Crypto era)
hk PoolParams (Crypto era)
poolParam)
              }
        else do
          Event (POOL era) -> F (Clause (POOL era) 'Transition) ()
forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent (Event (POOL era) -> F (Clause (POOL era) 'Transition) ())
-> Event (POOL era) -> F (Clause (POOL era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ KeyHash 'StakePool (Crypto era) -> PoolEvent era
forall era. KeyHash 'StakePool (Crypto era) -> PoolEvent era
ReregisterPool KeyHash 'StakePool (Crypto era)
hk
          PState (Crypto era)
-> F (Clause (POOL era) 'Transition) (PState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PState (Crypto era)
 -> F (Clause (POOL era) 'Transition) (PState (Crypto era)))
-> PState (Crypto era)
-> F (Clause (POOL era) 'Transition) (PState (Crypto era))
forall a b. (a -> b) -> a -> b
$
            State (POOL era)
PState (Crypto era)
ps
              { _fPParams :: Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
_fPParams = Exp
  (Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era)))
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
forall s t. Embed s t => Exp t -> s
eval (PState (Crypto era)
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
forall crypto.
PState crypto
-> Map (KeyHash 'StakePool crypto) (PoolParams crypto)
_fPParams State (POOL era)
PState (Crypto era)
ps Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
-> Exp
     (Single
        (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era)))
-> Exp
     (Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto 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 (Crypto era)
-> Exp
     (Single
        (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era)))
forall k v. Ord k => k -> v -> Exp (Single k v)
singleton KeyHash 'StakePool (Crypto era)
hk PoolParams (Crypto 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 (Crypto era)
-> Map (KeyHash 'StakePool (Crypto era)) EpochNo
forall crypto.
PState crypto -> Map (KeyHash 'StakePool crypto) EpochNo
_retiring State (POOL era)
PState (Crypto 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 (Crypto 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 (Crypto era))
stpools) Bool
-> PredicateFailure (POOL era)
-> F (Clause (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
epochInfoPure
        HasCallStack => EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
epochInfoEpoch EpochInfo Identity
ei SlotNo
slot
      let EpochNo Word64
maxEpoch = PParams era -> EpochNo
forall k (x :: k) r a. HasField x r a => r -> a
getField @"_eMax" PParams 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)
-> F (Clause (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 (Crypto era)
-> F (Clause (POOL era) 'Transition) (PState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PState (Crypto era)
 -> F (Clause (POOL era) 'Transition) (PState (Crypto era)))
-> PState (Crypto era)
-> F (Clause (POOL era) 'Transition) (PState (Crypto era))
forall a b. (a -> b) -> a -> b
$ State (POOL era)
PState (Crypto 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 (Crypto era)
-> Map (KeyHash 'StakePool (Crypto era)) EpochNo
forall crypto.
PState crypto -> Map (KeyHash 'StakePool crypto) EpochNo
_retiring State (POOL era)
PState (Crypto 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) -> F (Clause (POOL era) 'Transition) ()
forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause (PredicateFailure (POOL era)
 -> F (Clause (POOL era) 'Transition) ())
-> PredicateFailure (POOL era)
-> F (Clause (POOL era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ Word8 -> PoolPredicateFailure era
forall era. Word8 -> PoolPredicateFailure era
WrongCertificateTypePOOL Word8
0
      PState (Crypto era)
-> F (Clause (POOL era) 'Transition) (PState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure State (POOL era)
PState (Crypto era)
ps
    DCertMir _ -> do
      PredicateFailure (POOL era) -> F (Clause (POOL era) 'Transition) ()
forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause (PredicateFailure (POOL era)
 -> F (Clause (POOL era) 'Transition) ())
-> PredicateFailure (POOL era)
-> F (Clause (POOL era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ Word8 -> PoolPredicateFailure era
forall era. Word8 -> PoolPredicateFailure era
WrongCertificateTypePOOL Word8
1
      PState (Crypto era)
-> F (Clause (POOL era) 'Transition) (PState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure State (POOL era)
PState (Crypto era)
ps
    DCertGenesis _ -> do
      PredicateFailure (POOL era) -> F (Clause (POOL era) 'Transition) ()
forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause (PredicateFailure (POOL era)
 -> F (Clause (POOL era) 'Transition) ())
-> PredicateFailure (POOL era)
-> F (Clause (POOL era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ Word8 -> PoolPredicateFailure era
forall era. Word8 -> PoolPredicateFailure era
WrongCertificateTypePOOL Word8
2
      PState (Crypto era)
-> F (Clause (POOL era) 'Transition) (PState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure State (POOL era)
PState (Crypto era)
ps