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

module Cardano.Ledger.Shelley.Rules.Delegs (
  ShelleyDELEGS,
  DelegsEnv (..),
  ShelleyDelegsPredFailure (..),
  ShelleyDelegsEvent (..),
  PredicateFailure,
  validateStakePoolDelegateeRegistered,
) where

import Cardano.Ledger.BaseTypes (
  CertIx (..),
  EpochNo,
  ShelleyBase,
  TxIx (..),
  invalidKey,
  networkId,
 )
import Cardano.Ledger.Binary (
  DecCBOR (..),
  EncCBOR (..),
  decodeRecordSum,
  encodeListLen,
 )
import Cardano.Ledger.Core
import Cardano.Ledger.Credential (Ptr (..), SlotNo32 (..))
import Cardano.Ledger.Rules.ValidationMode (Test)
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.Era (ShelleyDELEGS, ShelleyEra)
import Cardano.Ledger.Shelley.Rules.Deleg (ShelleyDelegPredFailure)
import Cardano.Ledger.Shelley.Rules.Delpl (
  DelplEnv (..),
  ShelleyDELPL,
  ShelleyDelplEvent,
  ShelleyDelplPredFailure,
 )
import Cardano.Ledger.Shelley.Rules.Pool (ShelleyPoolPredFailure)
import Cardano.Ledger.Shelley.State
import Cardano.Ledger.Slot (SlotNo (..))
import Control.DeepSeq
import Control.Monad.Trans.Reader (asks)
import Control.SetAlgebra (dom, eval, (∈))
import Control.State.Transition (
  Embed (..),
  STS (..),
  TRC (..),
  TransitionRule,
  failOnJust,
  judgmentContext,
  liftSTS,
  trans,
  validateTrans,
 )
import Data.Sequence (Seq (..))
import Data.Typeable (Typeable)
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.Generics (Generic)
import Lens.Micro
import NoThunks.Class (NoThunks (..))
import Validation (failureUnless)

data DelegsEnv era = DelegsEnv
  { forall era. DelegsEnv era -> SlotNo
delegsSlotNo :: SlotNo
  , forall era. DelegsEnv era -> EpochNo
delegsEpochNo :: EpochNo
  -- ^ Lazy on purpose, because not all certificates need to know the current EpochNo
  , forall era. DelegsEnv era -> TxIx
delegsIx :: TxIx
  , forall era. DelegsEnv era -> PParams era
delegspp :: PParams era
  , forall era. DelegsEnv era -> Tx era
delegsTx :: Tx era
  , forall era. DelegsEnv era -> ChainAccountState
delegsAccount :: ChainAccountState
  }

deriving stock instance
  ( Show (Tx era)
  , Show (PParams era)
  ) =>
  Show (DelegsEnv era)

data ShelleyDelegsPredFailure era
  = -- | Target pool which is not registered
    DelegateeNotRegisteredDELEG
      (KeyHash 'StakePool)
  | -- | Withdrawals that are missing or do not withdrawal the entire amount
    WithdrawalsNotInRewardsDELEGS
      Withdrawals
  | -- | Subtransition Failures
    DelplFailure (PredicateFailure (EraRule "DELPL" era))
  deriving ((forall x.
 ShelleyDelegsPredFailure era
 -> Rep (ShelleyDelegsPredFailure era) x)
-> (forall x.
    Rep (ShelleyDelegsPredFailure era) x
    -> ShelleyDelegsPredFailure era)
-> Generic (ShelleyDelegsPredFailure era)
forall x.
Rep (ShelleyDelegsPredFailure era) x
-> ShelleyDelegsPredFailure era
forall x.
ShelleyDelegsPredFailure era
-> Rep (ShelleyDelegsPredFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyDelegsPredFailure era) x
-> ShelleyDelegsPredFailure era
forall era x.
ShelleyDelegsPredFailure era
-> Rep (ShelleyDelegsPredFailure era) x
$cfrom :: forall era x.
ShelleyDelegsPredFailure era
-> Rep (ShelleyDelegsPredFailure era) x
from :: forall x.
ShelleyDelegsPredFailure era
-> Rep (ShelleyDelegsPredFailure era) x
$cto :: forall era x.
Rep (ShelleyDelegsPredFailure era) x
-> ShelleyDelegsPredFailure era
to :: forall x.
Rep (ShelleyDelegsPredFailure era) x
-> ShelleyDelegsPredFailure era
Generic)

type instance EraRuleFailure "DELEGS" ShelleyEra = ShelleyDelegsPredFailure ShelleyEra

instance InjectRuleFailure "DELEGS" ShelleyDelegsPredFailure ShelleyEra

instance InjectRuleFailure "DELEGS" ShelleyDelplPredFailure ShelleyEra where
  injectFailure :: ShelleyDelplPredFailure ShelleyEra
-> EraRuleFailure "DELEGS" ShelleyEra
injectFailure = PredicateFailure (EraRule "DELPL" ShelleyEra)
-> ShelleyDelegsPredFailure ShelleyEra
ShelleyDelplPredFailure ShelleyEra
-> EraRuleFailure "DELEGS" ShelleyEra
forall era.
PredicateFailure (EraRule "DELPL" era)
-> ShelleyDelegsPredFailure era
DelplFailure

instance InjectRuleFailure "DELEGS" ShelleyPoolPredFailure ShelleyEra where
  injectFailure :: ShelleyPoolPredFailure ShelleyEra
-> EraRuleFailure "DELEGS" ShelleyEra
injectFailure = PredicateFailure (EraRule "DELPL" ShelleyEra)
-> ShelleyDelegsPredFailure ShelleyEra
ShelleyDelplPredFailure ShelleyEra
-> ShelleyDelegsPredFailure ShelleyEra
forall era.
PredicateFailure (EraRule "DELPL" era)
-> ShelleyDelegsPredFailure era
DelplFailure (ShelleyDelplPredFailure ShelleyEra
 -> ShelleyDelegsPredFailure ShelleyEra)
-> (ShelleyPoolPredFailure ShelleyEra
    -> ShelleyDelplPredFailure ShelleyEra)
-> ShelleyPoolPredFailure ShelleyEra
-> ShelleyDelegsPredFailure ShelleyEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShelleyPoolPredFailure ShelleyEra
-> EraRuleFailure "DELPL" ShelleyEra
ShelleyPoolPredFailure ShelleyEra
-> ShelleyDelplPredFailure ShelleyEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "DELEGS" ShelleyDelegPredFailure ShelleyEra where
  injectFailure :: ShelleyDelegPredFailure ShelleyEra
-> EraRuleFailure "DELEGS" ShelleyEra
injectFailure = PredicateFailure (EraRule "DELPL" ShelleyEra)
-> ShelleyDelegsPredFailure ShelleyEra
ShelleyDelplPredFailure ShelleyEra
-> ShelleyDelegsPredFailure ShelleyEra
forall era.
PredicateFailure (EraRule "DELPL" era)
-> ShelleyDelegsPredFailure era
DelplFailure (ShelleyDelplPredFailure ShelleyEra
 -> ShelleyDelegsPredFailure ShelleyEra)
-> (ShelleyDelegPredFailure ShelleyEra
    -> ShelleyDelplPredFailure ShelleyEra)
-> ShelleyDelegPredFailure ShelleyEra
-> ShelleyDelegsPredFailure ShelleyEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShelleyDelegPredFailure ShelleyEra
-> EraRuleFailure "DELPL" ShelleyEra
ShelleyDelegPredFailure ShelleyEra
-> ShelleyDelplPredFailure ShelleyEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

newtype ShelleyDelegsEvent era = DelplEvent (Event (EraRule "DELPL" era))
  deriving ((forall x.
 ShelleyDelegsEvent era -> Rep (ShelleyDelegsEvent era) x)
-> (forall x.
    Rep (ShelleyDelegsEvent era) x -> ShelleyDelegsEvent era)
-> Generic (ShelleyDelegsEvent era)
forall x. Rep (ShelleyDelegsEvent era) x -> ShelleyDelegsEvent era
forall x. ShelleyDelegsEvent era -> Rep (ShelleyDelegsEvent era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyDelegsEvent era) x -> ShelleyDelegsEvent era
forall era x.
ShelleyDelegsEvent era -> Rep (ShelleyDelegsEvent era) x
$cfrom :: forall era x.
ShelleyDelegsEvent era -> Rep (ShelleyDelegsEvent era) x
from :: forall x. ShelleyDelegsEvent era -> Rep (ShelleyDelegsEvent era) x
$cto :: forall era x.
Rep (ShelleyDelegsEvent era) x -> ShelleyDelegsEvent era
to :: forall x. Rep (ShelleyDelegsEvent era) x -> ShelleyDelegsEvent era
Generic)

deriving instance Eq (Event (EraRule "DELPL" era)) => Eq (ShelleyDelegsEvent era)

instance NFData (Event (EraRule "DELPL" era)) => NFData (ShelleyDelegsEvent era)

deriving stock instance
  Show (PredicateFailure (EraRule "DELPL" era)) =>
  Show (ShelleyDelegsPredFailure era)

deriving stock instance
  Eq (PredicateFailure (EraRule "DELPL" era)) =>
  Eq (ShelleyDelegsPredFailure era)

instance
  NFData (PredicateFailure (EraRule "DELPL" era)) =>
  NFData (ShelleyDelegsPredFailure era)

instance
  ( EraTx era
  , EraCertState era
  , ShelleyEraTxBody era
  , Embed (EraRule "DELPL" era) (ShelleyDELEGS era)
  , Environment (EraRule "DELPL" era) ~ DelplEnv era
  , State (EraRule "DELPL" era) ~ CertState era
  , Signal (EraRule "DELPL" era) ~ TxCert era
  , EraRule "DELEGS" era ~ ShelleyDELEGS era
  ) =>
  STS (ShelleyDELEGS era)
  where
  type State (ShelleyDELEGS era) = CertState era
  type Signal (ShelleyDELEGS era) = Seq (TxCert era)
  type Environment (ShelleyDELEGS era) = DelegsEnv era
  type BaseM (ShelleyDELEGS era) = ShelleyBase
  type
    PredicateFailure (ShelleyDELEGS era) =
      ShelleyDelegsPredFailure era
  type Event (ShelleyDELEGS era) = ShelleyDelegsEvent era

  transitionRules :: [TransitionRule (ShelleyDELEGS era)]
transitionRules = [TransitionRule (ShelleyDELEGS era)
forall era.
(EraTx era, EraCertState era, ShelleyEraTxBody era,
 Embed (EraRule "DELPL" era) (ShelleyDELEGS era),
 Environment (EraRule "DELPL" era) ~ DelplEnv era,
 State (EraRule "DELPL" era) ~ CertState era,
 Signal (EraRule "DELPL" era) ~ TxCert era,
 EraRule "DELEGS" era ~ ShelleyDELEGS era) =>
TransitionRule (ShelleyDELEGS era)
delegsTransition]

instance
  NoThunks (PredicateFailure (EraRule "DELPL" era)) =>
  NoThunks (ShelleyDelegsPredFailure era)

instance
  ( Era era
  , Typeable (Script era)
  , EncCBOR (PredicateFailure (EraRule "DELPL" era))
  ) =>
  EncCBOR (ShelleyDelegsPredFailure era)
  where
  encCBOR :: ShelleyDelegsPredFailure era -> Encoding
encCBOR = \case
    DelegateeNotRegisteredDELEG 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
    WithdrawalsNotInRewardsDELEGS Withdrawals
ws ->
      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
1 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Withdrawals -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Withdrawals
ws
    (DelplFailure PredicateFailure (EraRule "DELPL" era)
a) ->
      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
2 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> PredicateFailure (EraRule "DELPL" era) -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR PredicateFailure (EraRule "DELPL" era)
a

instance
  ( Era era
  , DecCBOR (PredicateFailure (EraRule "DELPL" era))
  , Typeable (Script era)
  ) =>
  DecCBOR (ShelleyDelegsPredFailure era)
  where
  decCBOR :: forall s. Decoder s (ShelleyDelegsPredFailure era)
decCBOR =
    Text
-> (Word -> Decoder s (Int, ShelleyDelegsPredFailure era))
-> Decoder s (ShelleyDelegsPredFailure era)
forall s a. Text -> (Word -> Decoder s (Int, a)) -> Decoder s a
decodeRecordSum Text
"PredicateFailure" ((Word -> Decoder s (Int, ShelleyDelegsPredFailure era))
 -> Decoder s (ShelleyDelegsPredFailure era))
-> (Word -> Decoder s (Int, ShelleyDelegsPredFailure era))
-> Decoder s (ShelleyDelegsPredFailure 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, ShelleyDelegsPredFailure era)
-> Decoder s (Int, ShelleyDelegsPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, KeyHash 'StakePool -> ShelleyDelegsPredFailure era
forall era. KeyHash 'StakePool -> ShelleyDelegsPredFailure era
DelegateeNotRegisteredDELEG KeyHash 'StakePool
kh)
        Word
1 -> do
          Withdrawals
ws <- Decoder s Withdrawals
forall s. Decoder s Withdrawals
forall a s. DecCBOR a => Decoder s a
decCBOR
          (Int, ShelleyDelegsPredFailure era)
-> Decoder s (Int, ShelleyDelegsPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, Withdrawals -> ShelleyDelegsPredFailure era
forall era. Withdrawals -> ShelleyDelegsPredFailure era
WithdrawalsNotInRewardsDELEGS Withdrawals
ws)
        Word
2 -> do
          PredicateFailure (EraRule "DELPL" era)
a <- Decoder s (PredicateFailure (EraRule "DELPL" era))
forall s. Decoder s (PredicateFailure (EraRule "DELPL" era))
forall a s. DecCBOR a => Decoder s a
decCBOR
          (Int, ShelleyDelegsPredFailure era)
-> Decoder s (Int, ShelleyDelegsPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, PredicateFailure (EraRule "DELPL" era)
-> ShelleyDelegsPredFailure era
forall era.
PredicateFailure (EraRule "DELPL" era)
-> ShelleyDelegsPredFailure era
DelplFailure PredicateFailure (EraRule "DELPL" era)
a)
        Word
k -> Word -> Decoder s (Int, ShelleyDelegsPredFailure era)
forall a (m :: * -> *). (Typeable a, MonadFail m) => Word -> m a
invalidKey Word
k

delegsTransition ::
  forall era.
  ( EraTx era
  , EraCertState era
  , ShelleyEraTxBody era
  , Embed (EraRule "DELPL" era) (ShelleyDELEGS era)
  , Environment (EraRule "DELPL" era) ~ DelplEnv era
  , State (EraRule "DELPL" era) ~ CertState era
  , Signal (EraRule "DELPL" era) ~ TxCert era
  , EraRule "DELEGS" era ~ ShelleyDELEGS era
  ) =>
  TransitionRule (ShelleyDELEGS era)
delegsTransition :: forall era.
(EraTx era, EraCertState era, ShelleyEraTxBody era,
 Embed (EraRule "DELPL" era) (ShelleyDELEGS era),
 Environment (EraRule "DELPL" era) ~ DelplEnv era,
 State (EraRule "DELPL" era) ~ CertState era,
 Signal (EraRule "DELPL" era) ~ TxCert era,
 EraRule "DELEGS" era ~ ShelleyDELEGS era) =>
TransitionRule (ShelleyDELEGS era)
delegsTransition = do
  TRC
    (env :: Environment (ShelleyDELEGS era)
env@(DelegsEnv slot :: SlotNo
slot@(SlotNo Word64
slot64) EpochNo
epochNo TxIx
txIx PParams era
pp Tx era
tx ChainAccountState
chainAccountState), State (ShelleyDELEGS era)
certState, Signal (ShelleyDELEGS era)
certificates) <-
    Rule
  (ShelleyDELEGS era)
  'Transition
  (RuleContext 'Transition (ShelleyDELEGS era))
F (Clause (ShelleyDELEGS era) 'Transition)
  (TRC (ShelleyDELEGS era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  Network
network <- BaseM (ShelleyDELEGS era) Network
-> Rule (ShelleyDELEGS era) 'Transition Network
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (ShelleyDELEGS era) Network
 -> Rule (ShelleyDELEGS era) 'Transition Network)
-> BaseM (ShelleyDELEGS era) Network
-> Rule (ShelleyDELEGS 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

  case Signal (ShelleyDELEGS era)
certificates of
    Seq (TxCert era)
Signal (ShelleyDELEGS era)
Empty -> do
      let dState :: DState era
dState = CertState era
State (ShelleyDELEGS era)
certState CertState era
-> Getting (DState era) (CertState era) (DState era) -> DState era
forall s a. s -> Getting a s a -> a
^. Getting (DState era) (CertState era) (DState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL
          withdrawals :: Withdrawals
withdrawals = Tx era
tx Tx era -> Getting Withdrawals (Tx era) Withdrawals -> Withdrawals
forall s a. s -> Getting a s a -> a
^. (TxBody era -> Const Withdrawals (TxBody era))
-> Tx era -> Const Withdrawals (Tx era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL ((TxBody era -> Const Withdrawals (TxBody era))
 -> Tx era -> Const Withdrawals (Tx era))
-> ((Withdrawals -> Const Withdrawals Withdrawals)
    -> TxBody era -> Const Withdrawals (TxBody era))
-> Getting Withdrawals (Tx era) Withdrawals
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Withdrawals -> Const Withdrawals Withdrawals)
-> TxBody era -> Const Withdrawals (TxBody era)
forall era. EraTxBody era => Lens' (TxBody era) Withdrawals
Lens' (TxBody era) Withdrawals
withdrawalsTxBodyL
          accounts :: Accounts era
accounts = DState era
dState DState era
-> Getting (Accounts era) (DState era) (Accounts era)
-> Accounts era
forall s a. s -> Getting a s a -> a
^. Getting (Accounts era) (DState era) (Accounts era)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL
      Maybe Withdrawals
-> (Withdrawals -> PredicateFailure (ShelleyDELEGS era))
-> Rule (ShelleyDELEGS era) 'Transition ()
forall a sts (ctx :: RuleType).
Maybe a -> (a -> PredicateFailure sts) -> Rule sts ctx ()
failOnJust
        (Withdrawals -> Network -> Accounts era -> Maybe Withdrawals
forall era.
EraAccounts era =>
Withdrawals -> Network -> Accounts era -> Maybe Withdrawals
withdrawalsThatDoNotDrainAccounts Withdrawals
withdrawals Network
network Accounts era
accounts)
        Withdrawals -> PredicateFailure (ShelleyDELEGS era)
Withdrawals -> ShelleyDelegsPredFailure era
forall era. Withdrawals -> ShelleyDelegsPredFailure era
WithdrawalsNotInRewardsDELEGS
      CertState era
-> F (Clause (ShelleyDELEGS era) 'Transition) (CertState era)
forall a. a -> F (Clause (ShelleyDELEGS era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CertState era
 -> F (Clause (ShelleyDELEGS era) 'Transition) (CertState era))
-> CertState era
-> F (Clause (ShelleyDELEGS era) 'Transition) (CertState era)
forall a b. (a -> b) -> a -> b
$ CertState era
State (ShelleyDELEGS era)
certState CertState era -> (CertState era -> CertState era) -> CertState era
forall a b. a -> (a -> b) -> b
& (DState era -> Identity (DState era))
-> CertState era -> Identity (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era -> Identity (DState era))
 -> CertState era -> Identity (CertState era))
-> ((Accounts era -> Identity (Accounts era))
    -> DState era -> Identity (DState era))
-> (Accounts era -> Identity (Accounts era))
-> CertState era
-> Identity (CertState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Accounts era -> Identity (Accounts era))
-> DState era -> Identity (DState era)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL ((Accounts era -> Identity (Accounts era))
 -> CertState era -> Identity (CertState era))
-> (Accounts era -> Accounts era) -> CertState era -> CertState era
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ Withdrawals -> Accounts era -> Accounts era
forall era.
EraAccounts era =>
Withdrawals -> Accounts era -> Accounts era
drainAccounts Withdrawals
withdrawals
    Seq (TxCert era)
gamma :|> TxCert era
txCert -> do
      CertState era
certState' <-
        forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(ShelleyDELEGS era) (RuleContext 'Transition (ShelleyDELEGS era)
 -> TransitionRule (ShelleyDELEGS era))
-> RuleContext 'Transition (ShelleyDELEGS era)
-> TransitionRule (ShelleyDELEGS era)
forall a b. (a -> b) -> a -> b
$ (Environment (ShelleyDELEGS era), State (ShelleyDELEGS era),
 Signal (ShelleyDELEGS era))
-> TRC (ShelleyDELEGS era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment (ShelleyDELEGS era)
env, State (ShelleyDELEGS era)
certState, Seq (TxCert era)
Signal (ShelleyDELEGS era)
gamma)
      (KeyHash 'StakePool -> PredicateFailure (ShelleyDELEGS era))
-> Validation (NonEmpty (KeyHash 'StakePool)) ()
-> Rule (ShelleyDELEGS era) 'Transition ()
forall e sts (ctx :: RuleType).
(e -> PredicateFailure sts)
-> Validation (NonEmpty e) () -> Rule sts ctx ()
validateTrans KeyHash 'StakePool -> PredicateFailure (ShelleyDELEGS era)
KeyHash 'StakePool -> ShelleyDelegsPredFailure era
forall era. KeyHash 'StakePool -> ShelleyDelegsPredFailure era
DelegateeNotRegisteredDELEG (Validation (NonEmpty (KeyHash 'StakePool)) ()
 -> Rule (ShelleyDELEGS era) 'Transition ())
-> Validation (NonEmpty (KeyHash 'StakePool)) ()
-> Rule (ShelleyDELEGS era) 'Transition ()
forall a b. (a -> b) -> a -> b
$
        case TxCert era
txCert of
          DelegStakeTxCert StakeCredential
_ KeyHash 'StakePool
targetPool ->
            PState era
-> KeyHash 'StakePool
-> Validation (NonEmpty (KeyHash 'StakePool)) ()
forall era.
PState era
-> KeyHash 'StakePool
-> Validation (NonEmpty (KeyHash 'StakePool)) ()
validateStakePoolDelegateeRegistered (CertState era
certState' CertState era
-> Getting (PState era) (CertState era) (PState era) -> PState era
forall s a. s -> Getting a s a -> a
^. Getting (PState era) (CertState era) (PState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL) KeyHash 'StakePool
targetPool
          TxCert era
_ -> () -> Validation (NonEmpty (KeyHash 'StakePool)) ()
forall a. a -> Validation (NonEmpty (KeyHash 'StakePool)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      -- It is impossible to have 65535 number of certificates in a transaction.
      let certIx :: CertIx
certIx = Word16 -> CertIx
CertIx (forall a b. (Integral a, Num b) => a -> b
fromIntegral @Int @Word16 (Int -> Word16) -> Int -> Word16
forall a b. (a -> b) -> a -> b
$ Seq (TxCert era) -> Int
forall a. Seq a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq (TxCert era)
gamma)
          ptr :: Ptr
ptr = SlotNo32 -> TxIx -> CertIx -> Ptr
Ptr (Word32 -> SlotNo32
SlotNo32 (forall a b. (Integral a, Num b) => a -> b
fromIntegral @Word64 @Word32 Word64
slot64)) TxIx
txIx CertIx
certIx
      forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "DELPL" era) (RuleContext 'Transition (EraRule "DELPL" era)
 -> Rule
      (ShelleyDELEGS era) 'Transition (State (EraRule "DELPL" era)))
-> RuleContext 'Transition (EraRule "DELPL" era)
-> Rule
     (ShelleyDELEGS era) 'Transition (State (EraRule "DELPL" era))
forall a b. (a -> b) -> a -> b
$
        (Environment (EraRule "DELPL" era), State (EraRule "DELPL" era),
 Signal (EraRule "DELPL" era))
-> TRC (EraRule "DELPL" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (SlotNo
-> EpochNo
-> Ptr
-> PParams era
-> ChainAccountState
-> DelplEnv era
forall era.
SlotNo
-> EpochNo
-> Ptr
-> PParams era
-> ChainAccountState
-> DelplEnv era
DelplEnv SlotNo
slot EpochNo
epochNo Ptr
ptr PParams era
pp ChainAccountState
chainAccountState, CertState era
State (EraRule "DELPL" era)
certState', TxCert era
Signal (EraRule "DELPL" era)
txCert)

validateStakePoolDelegateeRegistered ::
  PState era ->
  KeyHash 'StakePool ->
  Test (KeyHash 'StakePool)
validateStakePoolDelegateeRegistered :: forall era.
PState era
-> KeyHash 'StakePool
-> Validation (NonEmpty (KeyHash 'StakePool)) ()
validateStakePoolDelegateeRegistered PState era
pState KeyHash 'StakePool
targetPool =
  let stPools :: Map (KeyHash 'StakePool) PoolParams
stPools = PState era -> Map (KeyHash 'StakePool) PoolParams
forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams PState era
pState
   in Bool
-> KeyHash 'StakePool
-> Validation (NonEmpty (KeyHash 'StakePool)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Exp Bool -> Bool
forall s t. Embed s t => Exp t -> s
eval (KeyHash 'StakePool
targetPool 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
stPools)) KeyHash 'StakePool
targetPool

instance
  ( Era era
  , STS (ShelleyDELPL era)
  , PredicateFailure (EraRule "DELPL" era) ~ ShelleyDelplPredFailure era
  , Event (EraRule "DELPL" era) ~ ShelleyDelplEvent era
  ) =>
  Embed (ShelleyDELPL era) (ShelleyDELEGS era)
  where
  wrapFailed :: PredicateFailure (ShelleyDELPL era)
-> PredicateFailure (ShelleyDELEGS era)
wrapFailed = PredicateFailure (EraRule "DELPL" era)
-> ShelleyDelegsPredFailure era
PredicateFailure (ShelleyDELPL era)
-> PredicateFailure (ShelleyDELEGS era)
forall era.
PredicateFailure (EraRule "DELPL" era)
-> ShelleyDelegsPredFailure era
DelplFailure
  wrapEvent :: Event (ShelleyDELPL era) -> Event (ShelleyDELEGS era)
wrapEvent = Event (EraRule "DELPL" era) -> ShelleyDelegsEvent era
Event (ShelleyDELPL era) -> Event (ShelleyDELEGS era)
forall era. Event (EraRule "DELPL" era) -> ShelleyDelegsEvent era
DelplEvent