{-# 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,
  validateZeroRewards,
  validateStakePoolDelegateeRegistered,
  drainWithdrawals,
) where

import Cardano.Ledger.BaseTypes (
  CertIx (..),
  EpochNo,
  Network,
  ShelleyBase,
  TxIx (..),
  invalidKey,
  networkId,
 )
import Cardano.Ledger.Binary (
  DecCBOR (..),
  EncCBOR (..),
  decodeRecordSum,
  encodeListLen,
 )
import Cardano.Ledger.Coin (Coin)
import Cardano.Ledger.Core
import Cardano.Ledger.Credential (Credential, Ptr (..), SlotNo32 (..))
import Cardano.Ledger.Rules.ValidationMode (Test)
import Cardano.Ledger.Shelley.Era (ShelleyDELEGS, ShelleyEra)
import Cardano.Ledger.Shelley.LedgerState (
  ChainAccountState,
  DState (..),
  PState (..),
  psStakePoolParams,
  rewards,
 )
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.TxBody (
  RewardAccount (..),
  ShelleyEraTxBody (..),
  Withdrawals (..),
 )
import Cardano.Ledger.Shelley.TxCert (pattern DelegStakeTxCert)
import Cardano.Ledger.Slot (SlotNo (..))
import Cardano.Ledger.State (EraCertState (..))
import Cardano.Ledger.UMap (UMElem (..), UMap (..), UView (..), fromCompact)
import qualified Cardano.Ledger.UMap as UM
import Control.DeepSeq
import Control.Monad.Trans.Reader (asks)
import Control.SetAlgebra (dom, eval, (∈))
import Control.State.Transition (
  Embed (..),
  STS (..),
  TRC (..),
  TransitionRule,
  judgmentContext,
  liftSTS,
  trans,
  validateTrans,
 )
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe.Strict (StrictMaybe (..))
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
      (Map RewardAccount Coin)
  | -- | 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 Map RewardAccount Coin
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
<> Map RewardAccount Coin -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Map RewardAccount Coin
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
          Map RewardAccount Coin
ws <- Decoder s (Map RewardAccount Coin)
forall s. Decoder s (Map RewardAccount Coin)
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, Map RewardAccount Coin -> ShelleyDelegsPredFailure era
forall era. Map RewardAccount Coin -> ShelleyDelegsPredFailure era
WithdrawalsNotInRewardsDELEGS Map RewardAccount Coin
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
      (Map RewardAccount Coin -> PredicateFailure (ShelleyDELEGS era))
-> Validation (NonEmpty (Map RewardAccount Coin)) ()
-> Rule (ShelleyDELEGS era) 'Transition ()
forall e sts (ctx :: RuleType).
(e -> PredicateFailure sts)
-> Validation (NonEmpty e) () -> Rule sts ctx ()
validateTrans Map RewardAccount Coin -> PredicateFailure (ShelleyDELEGS era)
Map RewardAccount Coin -> ShelleyDelegsPredFailure era
forall era. Map RewardAccount Coin -> ShelleyDelegsPredFailure era
WithdrawalsNotInRewardsDELEGS (Validation (NonEmpty (Map RewardAccount Coin)) ()
 -> Rule (ShelleyDELEGS era) 'Transition ())
-> Validation (NonEmpty (Map RewardAccount Coin)) ()
-> Rule (ShelleyDELEGS era) 'Transition ()
forall a b. (a -> b) -> a -> b
$
        DState era
-> Withdrawals
-> Network
-> Validation (NonEmpty (Map RewardAccount Coin)) ()
forall era.
DState era
-> Withdrawals
-> Network
-> Validation (NonEmpty (Map RewardAccount Coin)) ()
validateZeroRewards DState era
dState Withdrawals
withdrawals Network
network
      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))
-> DState era -> CertState era -> CertState era
forall s t a b. ASetter s t a b -> b -> s -> t
.~ DState era -> Withdrawals -> DState era
forall era. DState era -> Withdrawals -> DState era
drainWithdrawals DState era
dState 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

-- @withdrawals_@ is small and @rewards@ big, better to transform the former
-- than the latter into the right shape so we can call 'Map.isSubmapOf'.
isSubmapOfUM ::
  Map RewardAccount Coin ->
  UView (Credential 'Staking) UM.RDPair ->
  Bool
isSubmapOfUM :: Map RewardAccount Coin -> UView StakeCredential RDPair -> Bool
isSubmapOfUM Map RewardAccount Coin
ws (RewDepUView (UMap Map StakeCredential UMElem
tripmap Map Ptr StakeCredential
_)) = (Coin -> UMElem -> Bool)
-> Map StakeCredential Coin -> Map StakeCredential UMElem -> Bool
forall k a b.
Ord k =>
(a -> b -> Bool) -> Map k a -> Map k b -> Bool
Map.isSubmapOfBy Coin -> UMElem -> Bool
f Map StakeCredential Coin
withdrawalMap Map StakeCredential UMElem
tripmap
  where
    withdrawalMap :: Map.Map (Credential 'Staking) Coin
    withdrawalMap :: Map StakeCredential Coin
withdrawalMap = (RewardAccount -> StakeCredential)
-> Map RewardAccount Coin -> Map StakeCredential Coin
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys (\(RewardAccount Network
_ StakeCredential
cred) -> StakeCredential
cred) Map RewardAccount Coin
ws
    f :: Coin -> UMElem -> Bool
    f :: Coin -> UMElem -> Bool
f Coin
coin1 (UMElem (SJust (UM.RDPair CompactForm Coin
coin2 CompactForm Coin
_)) Set Ptr
_ StrictMaybe (KeyHash 'StakePool)
_ StrictMaybe DRep
_) = Coin
coin1 Coin -> Coin -> Bool
forall a. Eq a => a -> a -> Bool
== CompactForm Coin -> Coin
forall a. Compactible a => CompactForm a -> a
fromCompact CompactForm Coin
coin2
    f Coin
_ UMElem
_ = Bool
False

drainWithdrawals :: DState era -> Withdrawals -> DState era
drainWithdrawals :: forall era. DState era -> Withdrawals -> DState era
drainWithdrawals DState era
dState (Withdrawals Map RewardAccount Coin
wdrls) =
  DState era
dState {dsUnified = rewards dState UM.⨃ drainedRewardAccounts}
  where
    drainedRewardAccounts :: Map StakeCredential RDPair
drainedRewardAccounts =
      (RewardAccount
 -> Coin
 -> Map StakeCredential RDPair
 -> Map StakeCredential RDPair)
-> Map StakeCredential RDPair
-> Map RewardAccount Coin
-> Map StakeCredential RDPair
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey
        ( \(RewardAccount Network
_ StakeCredential
cred) Coin
_coin ->
            StakeCredential
-> RDPair
-> Map StakeCredential RDPair
-> Map StakeCredential RDPair
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert StakeCredential
cred (CompactForm Coin -> CompactForm Coin -> RDPair
UM.RDPair (Word64 -> CompactForm Coin
UM.CompactCoin Word64
0) (Word64 -> CompactForm Coin
UM.CompactCoin Word64
0))
            -- Note that the deposit (CompactCoin 0) will be ignored.
        )
        Map StakeCredential RDPair
forall k a. Map k a
Map.empty
        Map RewardAccount Coin
wdrls

validateZeroRewards ::
  forall era.
  DState era ->
  Withdrawals ->
  Network ->
  Test (Map RewardAccount Coin)
validateZeroRewards :: forall era.
DState era
-> Withdrawals
-> Network
-> Validation (NonEmpty (Map RewardAccount Coin)) ()
validateZeroRewards DState era
dState (Withdrawals Map RewardAccount Coin
wdrls) Network
network = do
  Bool
-> Map RewardAccount Coin
-> Validation (NonEmpty (Map RewardAccount Coin)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Map RewardAccount Coin -> UView StakeCredential RDPair -> Bool
isSubmapOfUM Map RewardAccount Coin
wdrls (DState era -> UView StakeCredential RDPair
forall era. DState era -> UView StakeCredential RDPair
rewards DState era
dState)) (Map RewardAccount Coin
 -> Validation (NonEmpty (Map RewardAccount Coin)) ())
-> Map RewardAccount Coin
-> Validation (NonEmpty (Map RewardAccount Coin)) ()
forall a b. (a -> b) -> a -> b
$ -- withdrawals_ ⊆ rewards
    (Coin -> Coin -> Maybe Coin)
-> Map RewardAccount Coin
-> Map RewardAccount Coin
-> Map RewardAccount Coin
forall k a b.
Ord k =>
(a -> b -> Maybe a) -> Map k a -> Map k b -> Map k a
Map.differenceWith
      (\Coin
x Coin
y -> if Coin
x Coin -> Coin -> Bool
forall a. Eq a => a -> a -> Bool
/= Coin
y then Coin -> Maybe Coin
forall a. a -> Maybe a
Just Coin
x else Maybe Coin
forall a. Maybe a
Nothing)
      Map RewardAccount Coin
wdrls
      ((StakeCredential -> RewardAccount)
-> Map StakeCredential Coin -> Map RewardAccount Coin
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys (Network -> StakeCredential -> RewardAccount
RewardAccount Network
network) (UMap -> Map StakeCredential Coin
UM.rewardMap (DState era -> UMap
forall era. DState era -> UMap
dsUnified DState era
dState)))

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