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

module Cardano.Ledger.Shelley.Rules.Delegs
  ( DELEGS,
    DelegsEnv (..),
    DelegsPredicateFailure (..),
    DelegsEvent (..),
    PredicateFailure,
  )
where

import Cardano.Binary
  ( FromCBOR (..),
    ToCBOR (..),
    encodeListLen,
  )
import Cardano.Ledger.Address (mkRwdAcnt)
import Cardano.Ledger.BaseTypes
  ( ShelleyBase,
    TxIx,
    invalidKey,
    mkCertIxPartial,
    networkId,
  )
import Cardano.Ledger.Coin (Coin)
import qualified Cardano.Ledger.Core as Core
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.Era (Crypto, Era)
import Cardano.Ledger.Keys (KeyHash, KeyRole (..))
import Cardano.Ledger.Serialization
  ( decodeRecordSum,
    mapFromCBOR,
    mapToCBOR,
  )
import Cardano.Ledger.Shelley.LedgerState
  ( AccountState,
    DPState (..),
    RewardAccounts,
    dpsDState,
    rewards,
    _pParams,
    _unified,
  )
import Cardano.Ledger.Shelley.Rules.Delpl (DELPL, DelplEnv (..), DelplEvent, DelplPredicateFailure)
import Cardano.Ledger.Shelley.TxBody
  ( DCert (..),
    DelegCert (..),
    Delegation (..),
    Ptr (..),
    RewardAcnt (..),
    Wdrl (..),
  )
import Cardano.Ledger.Slot (SlotNo)
import Cardano.Ledger.UnifiedMap (Trip (..), UMap (..), View (..), ViewMap)
import Control.Monad.Trans.Reader (asks)
import Control.SetAlgebra (dom, eval, (∈))
import Control.State.Transition
  ( Embed (..),
    STS (..),
    TRC (..),
    TransitionRule,
    judgmentContext,
    liftSTS,
    trans,
    (?!),
    (?!:),
  )
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 qualified Data.UMap as UM
import Data.Word (Word8)
import GHC.Generics (Generic)
import GHC.Records (HasField (..))
import NoThunks.Class (NoThunks (..))

data DELEGS era

data DelegsEnv era = DelegsEnv
  { DelegsEnv era -> SlotNo
delegsSlotNo :: !SlotNo,
    DelegsEnv era -> TxIx
delegsIx :: !TxIx,
    DelegsEnv era -> PParams era
delegspp :: !(Core.PParams era),
    DelegsEnv era -> Tx era
delegsTx :: !(Core.Tx era),
    DelegsEnv era -> AccountState
delegsAccount :: !AccountState
  }

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

data DelegsPredicateFailure era
  = DelegateeNotRegisteredDELEG
      !(KeyHash 'StakePool (Crypto era)) -- target pool which is not registered
  | WithdrawalsNotInRewardsDELEGS
      !(Map (RewardAcnt (Crypto era)) Coin) -- withdrawals that are missing or do not withdrawl the entire amount
  | DelplFailure (PredicateFailure (Core.EraRule "DELPL" era)) -- Subtransition Failures
  deriving ((forall x.
 DelegsPredicateFailure era -> Rep (DelegsPredicateFailure era) x)
-> (forall x.
    Rep (DelegsPredicateFailure era) x -> DelegsPredicateFailure era)
-> Generic (DelegsPredicateFailure era)
forall x.
Rep (DelegsPredicateFailure era) x -> DelegsPredicateFailure era
forall x.
DelegsPredicateFailure era -> Rep (DelegsPredicateFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (DelegsPredicateFailure era) x -> DelegsPredicateFailure era
forall era x.
DelegsPredicateFailure era -> Rep (DelegsPredicateFailure era) x
$cto :: forall era x.
Rep (DelegsPredicateFailure era) x -> DelegsPredicateFailure era
$cfrom :: forall era x.
DelegsPredicateFailure era -> Rep (DelegsPredicateFailure era) x
Generic)

newtype DelegsEvent era = DelplEvent (Event (Core.EraRule "DELPL" era))

deriving stock instance
  ( Show (PredicateFailure (Core.EraRule "DELPL" era))
  ) =>
  Show (DelegsPredicateFailure era)

deriving stock instance
  ( Eq (PredicateFailure (Core.EraRule "DELPL" era))
  ) =>
  Eq (DelegsPredicateFailure era)

instance
  ( Era era,
    HasField "wdrls" (Core.TxBody era) (Wdrl (Crypto era)),
    Embed (Core.EraRule "DELPL" era) (DELEGS era),
    Environment (Core.EraRule "DELPL" era) ~ DelplEnv era,
    State (Core.EraRule "DELPL" era) ~ DPState (Crypto era),
    Signal (Core.EraRule "DELPL" era) ~ DCert (Crypto era)
  ) =>
  STS (DELEGS era)
  where
  type State (DELEGS era) = DPState (Crypto era)
  type Signal (DELEGS era) = Seq (DCert (Crypto era))
  type Environment (DELEGS era) = DelegsEnv era
  type BaseM (DELEGS era) = ShelleyBase
  type
    PredicateFailure (DELEGS era) =
      DelegsPredicateFailure era
  type Event _ = DelegsEvent era

  transitionRules :: [TransitionRule (DELEGS era)]
transitionRules = [TransitionRule (DELEGS era)
forall era.
(Era era, HasField "wdrls" (TxBody era) (Wdrl (Crypto era)),
 Embed (EraRule "DELPL" era) (DELEGS era),
 Environment (EraRule "DELPL" era) ~ DelplEnv era,
 State (EraRule "DELPL" era) ~ DPState (Crypto era),
 Signal (EraRule "DELPL" era) ~ DCert (Crypto era)) =>
TransitionRule (DELEGS era)
delegsTransition]

instance
  ( NoThunks (PredicateFailure (Core.EraRule "DELPL" era))
  ) =>
  NoThunks (DelegsPredicateFailure era)

instance
  ( Era era,
    Typeable (Core.Script era),
    ToCBOR (PredicateFailure (Core.EraRule "DELPL" era))
  ) =>
  ToCBOR (DelegsPredicateFailure era)
  where
  toCBOR :: DelegsPredicateFailure era -> Encoding
toCBOR = \case
    DelegateeNotRegisteredDELEG 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
    WithdrawalsNotInRewardsDELEGS Map (RewardAcnt (Crypto era)) Coin
ws ->
      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
1 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Map (RewardAcnt (Crypto era)) Coin -> Encoding
forall a b. (ToCBOR a, ToCBOR b) => Map a b -> Encoding
mapToCBOR Map (RewardAcnt (Crypto era)) 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. ToCBOR a => a -> Encoding
toCBOR (Word8
2 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> PredicateFailure (EraRule "DELPL" era) -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR PredicateFailure (EraRule "DELPL" era)
a

instance
  ( Era era,
    FromCBOR (PredicateFailure (Core.EraRule "DELPL" era)),
    Typeable (Core.Script era)
  ) =>
  FromCBOR (DelegsPredicateFailure era)
  where
  fromCBOR :: Decoder s (DelegsPredicateFailure era)
fromCBOR =
    String
-> (Word -> Decoder s (Int, DelegsPredicateFailure era))
-> Decoder s (DelegsPredicateFailure era)
forall s a. String -> (Word -> Decoder s (Int, a)) -> Decoder s a
decodeRecordSum String
"PredicateFailure" ((Word -> Decoder s (Int, DelegsPredicateFailure era))
 -> Decoder s (DelegsPredicateFailure era))
-> (Word -> Decoder s (Int, DelegsPredicateFailure era))
-> Decoder s (DelegsPredicateFailure 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, DelegsPredicateFailure era)
-> Decoder s (Int, DelegsPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, KeyHash 'StakePool (Crypto era) -> DelegsPredicateFailure era
forall era.
KeyHash 'StakePool (Crypto era) -> DelegsPredicateFailure era
DelegateeNotRegisteredDELEG KeyHash 'StakePool (Crypto era)
kh)
        Word
1 -> do
          Map (RewardAcnt (Crypto era)) Coin
ws <- Decoder s (Map (RewardAcnt (Crypto era)) Coin)
forall a b s.
(Ord a, FromCBOR a, FromCBOR b) =>
Decoder s (Map a b)
mapFromCBOR
          (Int, DelegsPredicateFailure era)
-> Decoder s (Int, DelegsPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, Map (RewardAcnt (Crypto era)) Coin -> DelegsPredicateFailure era
forall era.
Map (RewardAcnt (Crypto era)) Coin -> DelegsPredicateFailure era
WithdrawalsNotInRewardsDELEGS Map (RewardAcnt (Crypto era)) Coin
ws)
        Word
2 -> do
          PredicateFailure (EraRule "DELPL" era)
a <- Decoder s (PredicateFailure (EraRule "DELPL" era))
forall a s. FromCBOR a => Decoder s a
fromCBOR
          (Int, DelegsPredicateFailure era)
-> Decoder s (Int, DelegsPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, PredicateFailure (EraRule "DELPL" era)
-> DelegsPredicateFailure era
forall era.
PredicateFailure (EraRule "DELPL" era)
-> DelegsPredicateFailure era
DelplFailure PredicateFailure (EraRule "DELPL" era)
a)
        Word
k -> Word -> Decoder s (Int, DelegsPredicateFailure era)
forall s a. Word -> Decoder s a
invalidKey Word
k

delegsTransition ::
  forall era.
  ( Era era,
    HasField "wdrls" (Core.TxBody era) (Wdrl (Crypto era)),
    Embed (Core.EraRule "DELPL" era) (DELEGS era),
    Environment (Core.EraRule "DELPL" era) ~ DelplEnv era,
    State (Core.EraRule "DELPL" era) ~ DPState (Crypto era),
    Signal (Core.EraRule "DELPL" era) ~ DCert (Crypto era)
  ) =>
  TransitionRule (DELEGS era)
delegsTransition :: TransitionRule (DELEGS era)
delegsTransition = do
  TRC (env :: Environment (DELEGS era)
env@(DelegsEnv slot txIx pp tx acnt), State (DELEGS era)
dpstate, Signal (DELEGS era)
certificates) <- F (Clause (DELEGS era) 'Transition) (TRC (DELEGS era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  Network
network <- BaseM (DELEGS era) Network -> Rule (DELEGS era) 'Transition Network
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (DELEGS era) Network
 -> Rule (DELEGS era) 'Transition Network)
-> BaseM (DELEGS era) Network
-> Rule (DELEGS 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 (DELEGS era)
certificates of
    Signal (DELEGS era)
Empty -> do
      let ds :: DState (Crypto era)
ds = DPState (Crypto era) -> DState (Crypto era)
forall crypto. DPState crypto -> DState crypto
dpsDState State (DELEGS era)
DPState (Crypto era)
dpstate
          wdrls_ :: Map (RewardAcnt (Crypto era)) Coin
wdrls_ = Wdrl (Crypto era) -> Map (RewardAcnt (Crypto era)) Coin
forall crypto. Wdrl crypto -> Map (RewardAcnt crypto) Coin
unWdrl (Wdrl (Crypto era) -> Map (RewardAcnt (Crypto era)) Coin)
-> (TxBody era -> Wdrl (Crypto era))
-> TxBody era
-> Map (RewardAcnt (Crypto era)) Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (x :: k) r a. HasField x r a => r -> a
forall r a. HasField "wdrls" r a => r -> a
getField @"wdrls" (TxBody era -> Map (RewardAcnt (Crypto era)) Coin)
-> TxBody era -> Map (RewardAcnt (Crypto era)) Coin
forall a b. (a -> b) -> a -> b
$ Tx era -> TxBody era
forall k (x :: k) r a. HasField x r a => r -> a
getField @"body" Tx era
tx
          rewards' :: ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
rewards' = DState (Crypto era)
-> ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
forall crypto.
DState crypto -> ViewMap crypto (Credential 'Staking crypto) Coin
rewards DState (Crypto era)
ds
      Map (RewardAcnt (Crypto era)) Coin
-> ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
-> Bool
forall crypto.
Map (RewardAcnt (Crypto era)) Coin
-> ViewMap (Crypto era) (Credential 'Staking crypto) Coin -> Bool
isSubmapOf Map (RewardAcnt (Crypto era)) Coin
wdrls_ ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
rewards' -- wdrls_ ⊆ rewards
        Bool
-> PredicateFailure (DELEGS era)
-> Rule (DELEGS era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Map (RewardAcnt (Crypto era)) Coin -> DelegsPredicateFailure era
forall era.
Map (RewardAcnt (Crypto era)) Coin -> DelegsPredicateFailure era
WithdrawalsNotInRewardsDELEGS
          ( (Coin -> Coin -> Maybe Coin)
-> Map (RewardAcnt (Crypto era)) Coin
-> Map (RewardAcnt (Crypto era)) Coin
-> Map (RewardAcnt (Crypto era)) 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 (RewardAcnt (Crypto era)) Coin
wdrls_
              ((Credential 'Staking (Crypto era) -> RewardAcnt (Crypto era))
-> Map (Credential 'Staking (Crypto era)) Coin
-> Map (RewardAcnt (Crypto era)) Coin
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys (Network
-> Credential 'Staking (Crypto era) -> RewardAcnt (Crypto era)
forall crypto.
Network -> Credential 'Staking crypto -> RewardAcnt crypto
mkRwdAcnt Network
network) (ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
-> Map (Credential 'Staking (Crypto era)) Coin
forall coin cred pool ptr k v.
View coin cred pool ptr k v -> Map k v
UM.unUnify ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
rewards'))
          )

      let wdrls_' :: RewardAccounts (Crypto era)
          wdrls_' :: Map (Credential 'Staking (Crypto era)) Coin
wdrls_' =
            (RewardAcnt (Crypto era)
 -> Coin
 -> Map (Credential 'Staking (Crypto era)) Coin
 -> Map (Credential 'Staking (Crypto era)) Coin)
-> Map (Credential 'Staking (Crypto era)) Coin
-> Map (RewardAcnt (Crypto era)) Coin
-> Map (Credential 'Staking (Crypto era)) Coin
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey
              ( \(RewardAcnt Network
_ Credential 'Staking (Crypto era)
cred) Coin
_coin ->
                  Credential 'Staking (Crypto era)
-> Coin
-> Map (Credential 'Staking (Crypto era)) Coin
-> Map (Credential 'Staking (Crypto era)) Coin
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Credential 'Staking (Crypto era)
cred Coin
forall a. Monoid a => a
mempty
              )
              Map (Credential 'Staking (Crypto era)) Coin
forall k a. Map k a
Map.empty
              Map (RewardAcnt (Crypto era)) Coin
wdrls_
          unified' :: UMap
  Coin
  (Credential 'Staking (Crypto era))
  (KeyHash 'StakePool (Crypto era))
  Ptr
unified' = ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
rewards' ViewMap (Crypto era) (Credential 'Staking (Crypto era)) Coin
-> Map (Credential 'Staking (Crypto era)) Coin
-> UMap
     Coin
     (Credential 'Staking (Crypto era))
     (KeyHash 'StakePool (Crypto era))
     Ptr
forall cr coin ptr pool k v.
(Ord cr, Monoid coin, Ord ptr) =>
View coin cr pool ptr k v -> Map k v -> UMap coin cr pool ptr
UM.⨃ Map (Credential 'Staking (Crypto era)) Coin
wdrls_'
      DPState (Crypto era)
-> F (Clause (DELEGS era) 'Transition) (DPState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DPState (Crypto era)
 -> F (Clause (DELEGS era) 'Transition) (DPState (Crypto era)))
-> DPState (Crypto era)
-> F (Clause (DELEGS era) 'Transition) (DPState (Crypto era))
forall a b. (a -> b) -> a -> b
$ State (DELEGS era)
DPState (Crypto era)
dpstate {dpsDState :: DState (Crypto era)
dpsDState = DState (Crypto era)
ds {_unified :: UMap
  Coin
  (Credential 'Staking (Crypto era))
  (KeyHash 'StakePool (Crypto era))
  Ptr
_unified = UMap
  Coin
  (Credential 'Staking (Crypto era))
  (KeyHash 'StakePool (Crypto era))
  Ptr
unified'}}
    gamma :|> c -> do
      DPState (Crypto era)
dpstate' <-
        forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (DELEGS era) super =>
RuleContext rtype (DELEGS era)
-> Rule super rtype (State (DELEGS era))
trans @(DELEGS era) (RuleContext 'Transition (DELEGS era)
 -> TransitionRule (DELEGS era))
-> RuleContext 'Transition (DELEGS era)
-> TransitionRule (DELEGS era)
forall a b. (a -> b) -> a -> b
$ (Environment (DELEGS era), State (DELEGS era), Signal (DELEGS era))
-> TRC (DELEGS era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment (DELEGS era)
env, State (DELEGS era)
dpstate, Seq (DCert (Crypto era))
Signal (DELEGS era)
gamma)

      let isDelegationRegistered :: Either (DelegsPredicateFailure era) ()
isDelegationRegistered = case DCert (Crypto era)
c of
            DCertDeleg (Delegate Delegation (Crypto era)
deleg) ->
              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 (PState (Crypto era)
 -> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era)))
-> PState (Crypto era)
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams (Crypto era))
forall a b. (a -> b) -> a -> b
$ DPState (Crypto era) -> PState (Crypto era)
forall crypto. DPState crypto -> PState crypto
dpsPState DPState (Crypto era)
dpstate'
                  targetPool :: KeyHash 'StakePool (Crypto era)
targetPool = Delegation (Crypto era) -> KeyHash 'StakePool (Crypto era)
forall crypto. Delegation crypto -> KeyHash 'StakePool crypto
_delegatee Delegation (Crypto era)
deleg
               in case Exp Bool -> Bool
forall s t. Embed s t => Exp t -> s
eval (KeyHash 'StakePool (Crypto era)
targetPool 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_) of
                    Bool
True -> () -> Either (DelegsPredicateFailure era) ()
forall a b. b -> Either a b
Right ()
                    Bool
False -> DelegsPredicateFailure era
-> Either (DelegsPredicateFailure era) ()
forall a b. a -> Either a b
Left (DelegsPredicateFailure era
 -> Either (DelegsPredicateFailure era) ())
-> DelegsPredicateFailure era
-> Either (DelegsPredicateFailure era) ()
forall a b. (a -> b) -> a -> b
$ KeyHash 'StakePool (Crypto era) -> DelegsPredicateFailure era
forall era.
KeyHash 'StakePool (Crypto era) -> DelegsPredicateFailure era
DelegateeNotRegisteredDELEG KeyHash 'StakePool (Crypto era)
targetPool
            DCert (Crypto era)
_ -> () -> Either (DelegsPredicateFailure era) ()
forall a b. b -> Either a b
Right ()
      Either (DelegsPredicateFailure era) ()
isDelegationRegistered Either (DelegsPredicateFailure era) ()
-> (DelegsPredicateFailure era -> PredicateFailure (DELEGS era))
-> Rule (DELEGS era) 'Transition ()
forall e sts (ctx :: RuleType).
Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
?!: DelegsPredicateFailure era -> PredicateFailure (DELEGS era)
forall a. a -> a
id

      -- It is impossible to have 4294967295 number of certificates in a
      -- transaction, therefore partial function is justified.
      let ptr :: Ptr
ptr = SlotNo -> TxIx -> CertIx -> Ptr
Ptr SlotNo
slot TxIx
txIx (HasCallStack => Integer -> CertIx
Integer -> CertIx
mkCertIxPartial (Integer -> CertIx) -> Integer -> CertIx
forall a b. (a -> b) -> a -> b
$ Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ Seq (DCert (Crypto era)) -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq (DCert (Crypto era))
gamma)
      forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (EraRule "DELPL" era) super =>
RuleContext rtype (EraRule "DELPL" era)
-> Rule super rtype (State (EraRule "DELPL" era))
trans @(Core.EraRule "DELPL" era) (RuleContext 'Transition (EraRule "DELPL" era)
 -> Rule (DELEGS era) 'Transition (State (EraRule "DELPL" era)))
-> RuleContext 'Transition (EraRule "DELPL" era)
-> Rule (DELEGS 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 -> Ptr -> PParams era -> AccountState -> DelplEnv era
forall era.
SlotNo -> Ptr -> PParams era -> AccountState -> DelplEnv era
DelplEnv SlotNo
slot Ptr
ptr PParams era
pp AccountState
acnt, State (EraRule "DELPL" era)
DPState (Crypto era)
dpstate', Signal (EraRule "DELPL" era)
DCert (Crypto era)
c)
  where
    -- @wdrls_@ is small and @rewards@ big, better to transform the former
    -- than the latter into the right shape so we can call 'Map.isSubmapOf'.
    isSubmapOf ::
      Map (RewardAcnt (Crypto era)) Coin ->
      ViewMap (Crypto era) (Credential 'Staking crypto) Coin ->
      Bool
    isSubmapOf :: Map (RewardAcnt (Crypto era)) Coin
-> ViewMap (Crypto era) (Credential 'Staking crypto) Coin -> Bool
isSubmapOf Map (RewardAcnt (Crypto era)) Coin
wdrls_ (Rewards (UnifiedMap Map
  (Credential 'Staking (Crypto era))
  (Trip Coin Ptr (KeyHash 'StakePool (Crypto era)))
tripmap Map Ptr (Credential 'Staking (Crypto era))
_)) = (Coin -> Trip Coin Ptr (KeyHash 'StakePool (Crypto era)) -> Bool)
-> Map (Credential 'Staking (Crypto era)) Coin
-> Map
     (Credential 'Staking (Crypto era))
     (Trip Coin Ptr (KeyHash 'StakePool (Crypto era)))
-> Bool
forall k a b.
Ord k =>
(a -> b -> Bool) -> Map k a -> Map k b -> Bool
Map.isSubmapOfBy Coin -> Trip Coin Ptr (KeyHash 'StakePool (Crypto era)) -> Bool
forall a ptr pool. Eq a => a -> Trip a ptr pool -> Bool
f Map (Credential 'Staking (Crypto era)) Coin
withdrawalMap Map
  (Credential 'Staking (Crypto era))
  (Trip Coin Ptr (KeyHash 'StakePool (Crypto era)))
tripmap
      where
        withdrawalMap :: Map (Credential 'Staking (Crypto era)) Coin
withdrawalMap =
          [(Credential 'Staking (Crypto era), Coin)]
-> Map (Credential 'Staking (Crypto era)) Coin
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
            [ (Credential 'Staking (Crypto era)
cred, Coin
coin)
              | (RewardAcnt Network
_ Credential 'Staking (Crypto era)
cred, Coin
coin) <- Map (RewardAcnt (Crypto era)) Coin
-> [(RewardAcnt (Crypto era), Coin)]
forall k a. Map k a -> [(k, a)]
Map.toList Map (RewardAcnt (Crypto era)) Coin
wdrls_
            ]
        f :: a -> Trip a ptr pool -> Bool
f a
coin1 (Triple (SJust a
coin2) Set ptr
_ StrictMaybe pool
_) = a
coin1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
coin2
        f a
_ Trip a ptr pool
_ = Bool
False

instance
  ( Era era,
    STS (DELPL era),
    PredicateFailure (Core.EraRule "DELPL" era) ~ DelplPredicateFailure era,
    Event (Core.EraRule "DELPL" era) ~ DelplEvent era
  ) =>
  Embed (DELPL era) (DELEGS era)
  where
  wrapFailed :: PredicateFailure (DELPL era) -> PredicateFailure (DELEGS era)
wrapFailed = PredicateFailure (DELPL era) -> PredicateFailure (DELEGS era)
forall era.
PredicateFailure (EraRule "DELPL" era)
-> DelegsPredicateFailure era
DelplFailure
  wrapEvent :: Event (DELPL era) -> Event (DELEGS era)
wrapEvent = Event (DELPL era) -> Event (DELEGS era)
forall era. Event (EraRule "DELPL" era) -> DelegsEvent era
DelplEvent