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

module Shelley.Spec.Ledger.STS.Delegs
  ( DELEGS,
    DelegsEnv (..),
    DelegsPredicateFailure (..),
    PredicateFailure,
  )
where

import Cardano.Binary
  ( FromCBOR (..),
    ToCBOR (..),
    encodeListLen,
  )
import qualified Cardano.Ledger.Core as Core
import Cardano.Ledger.Era (Crypto, Era)
import Cardano.Ledger.Shelley.Constraints (ShelleyBased)
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.Sequence (Seq (..))
import Data.Typeable (Typeable)
import Data.Word (Word8)
import GHC.Generics (Generic)
import GHC.Records (HasField (..))
import NoThunks.Class (NoThunks (..))
import Shelley.Spec.Ledger.Address (mkRwdAcnt)
import Shelley.Spec.Ledger.BaseTypes
  ( ShelleyBase,
    invalidKey,
    networkId,
  )
import Shelley.Spec.Ledger.Coin (Coin)
import Shelley.Spec.Ledger.Keys (KeyHash, KeyRole (..))
import Shelley.Spec.Ledger.LedgerState
  ( AccountState,
    DPState (..),
    RewardAccounts,
    emptyDelegation,
    _dstate,
    _pParams,
    _rewards,
  )
import Shelley.Spec.Ledger.PParams (PParams)
import Shelley.Spec.Ledger.STS.Delpl (DELPL, DelplEnv (..))
import Shelley.Spec.Ledger.Serialization
  ( decodeRecordSum,
    mapFromCBOR,
    mapToCBOR,
  )
import Shelley.Spec.Ledger.Slot (SlotNo)
import Shelley.Spec.Ledger.Tx (Tx (..))
import Shelley.Spec.Ledger.TxBody
  ( DCert (..),
    DelegCert (..),
    Delegation (..),
    Ix,
    Ptr (..),
    RewardAcnt (..),
    Wdrl (..),
  )

data DELEGS era

data DelegsEnv era = DelegsEnv
  { DelegsEnv era -> SlotNo
delegsSlotNo :: SlotNo,
    DelegsEnv era -> Ix
delegsIx :: Ix,
    DelegsEnv era -> PParams era
delegspp :: PParams era,
    DelegsEnv era -> Tx era
delegsTx :: Tx era,
    DelegsEnv era -> AccountState
delegsAccount :: AccountState
  }

deriving stock instance
  ShelleyBased 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 (DELPL era)) -- Subtransition Failures
  deriving (Int -> DelegsPredicateFailure era -> ShowS
[DelegsPredicateFailure era] -> ShowS
DelegsPredicateFailure era -> String
(Int -> DelegsPredicateFailure era -> ShowS)
-> (DelegsPredicateFailure era -> String)
-> ([DelegsPredicateFailure era] -> ShowS)
-> Show (DelegsPredicateFailure era)
forall era. Int -> DelegsPredicateFailure era -> ShowS
forall era. [DelegsPredicateFailure era] -> ShowS
forall era. DelegsPredicateFailure era -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DelegsPredicateFailure era] -> ShowS
$cshowList :: forall era. [DelegsPredicateFailure era] -> ShowS
show :: DelegsPredicateFailure era -> String
$cshow :: forall era. DelegsPredicateFailure era -> String
showsPrec :: Int -> DelegsPredicateFailure era -> ShowS
$cshowsPrec :: forall era. Int -> DelegsPredicateFailure era -> ShowS
Show, DelegsPredicateFailure era -> DelegsPredicateFailure era -> Bool
(DelegsPredicateFailure era -> DelegsPredicateFailure era -> Bool)
-> (DelegsPredicateFailure era
    -> DelegsPredicateFailure era -> Bool)
-> Eq (DelegsPredicateFailure era)
forall era.
DelegsPredicateFailure era -> DelegsPredicateFailure era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DelegsPredicateFailure era -> DelegsPredicateFailure era -> Bool
$c/= :: forall era.
DelegsPredicateFailure era -> DelegsPredicateFailure era -> Bool
== :: DelegsPredicateFailure era -> DelegsPredicateFailure era -> Bool
$c== :: forall era.
DelegsPredicateFailure era -> DelegsPredicateFailure era -> Bool
Eq, (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)

instance
  ( Era era,
    ShelleyBased era,
    HasField "wdrls" (Core.TxBody era) (Wdrl (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

  initialRules :: [InitialRule (DELEGS era)]
initialRules = [DPState (Crypto era)
-> F (Clause (DELEGS era) 'Initial) (DPState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure DPState (Crypto era)
forall crypto. DPState crypto
emptyDelegation]
  transitionRules :: [TransitionRule (DELEGS era)]
transitionRules = [TransitionRule (DELEGS era)
forall era.
(ShelleyBased era,
 HasField "wdrls" (TxBody era) (Wdrl (Crypto era)),
 Embed (DELPL era) (DELEGS era)) =>
TransitionRule (DELEGS era)
delegsTransition]

instance NoThunks (DelegsPredicateFailure era)

instance
  (Typeable era, Era era, Typeable (Core.Script 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 (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
<> DelplPredicateFailure era -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR PredicateFailure (DELPL era)
DelplPredicateFailure era
a

instance
  (Era 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
            DelplPredicateFailure era
a <- Decoder s (DelplPredicateFailure 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 (DELPL era) -> DelegsPredicateFailure era
forall era.
PredicateFailure (DELPL era) -> DelegsPredicateFailure era
DelplFailure PredicateFailure (DELPL era)
DelplPredicateFailure era
a)
          Word
k -> Word -> Decoder s (Int, DelegsPredicateFailure era)
forall s a. Word -> Decoder s a
invalidKey Word
k
      )

delegsTransition ::
  forall era.
  ( ShelleyBased era,
    HasField "wdrls" (Core.TxBody era) (Wdrl (Crypto era)),
    Embed (DELPL era) (DELEGS 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
_dstate 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)
-> Wdrl (Crypto era) -> Map (RewardAcnt (Crypto era)) Coin
forall a b. (a -> b) -> a -> b
$ TxBody era -> Wdrl (Crypto era)
forall k (x :: k) r a. HasField x r a => r -> a
getField @"wdrls" (Tx era
-> (TxBodyConstraints era, ToCBOR (AuxiliaryData era)) =>
   TxBody era
forall era.
Tx era
-> (TxBodyConstraints era, ToCBOR (AuxiliaryData era)) =>
   TxBody era
_body Tx era
tx)
          rewards :: RewardAccounts (Crypto era)
rewards = DState (Crypto era) -> RewardAccounts (Crypto era)
forall crypto. DState crypto -> RewardAccounts crypto
_rewards DState (Crypto era)
ds

      Map (RewardAcnt (Crypto era)) Coin
-> RewardAccounts (Crypto era) -> Bool
isSubmapOf Map (RewardAcnt (Crypto era)) Coin
wdrls_ RewardAccounts (Crypto era)
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))
-> RewardAccounts (Crypto era)
-> 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) RewardAccounts (Crypto era)
rewards)
          )

      let wdrls_' :: RewardAccounts (Crypto era)
          wdrls_' :: RewardAccounts (Crypto era)
wdrls_' =
            (RewardAcnt (Crypto era)
 -> Coin
 -> RewardAccounts (Crypto era)
 -> RewardAccounts (Crypto era))
-> RewardAccounts (Crypto era)
-> Map (RewardAcnt (Crypto era)) Coin
-> RewardAccounts (Crypto era)
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
-> RewardAccounts (Crypto era)
-> RewardAccounts (Crypto era)
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
              )
              RewardAccounts (Crypto era)
forall k a. Map k a
Map.empty
              Map (RewardAcnt (Crypto era)) Coin
wdrls_
          rewards' :: RewardAccounts (Crypto era)
rewards' = Exp (RewardAccounts (Crypto era)) -> RewardAccounts (Crypto era)
forall s t. Embed s t => Exp t -> s
eval (RewardAccounts (Crypto era)
rewards RewardAccounts (Crypto era)
-> RewardAccounts (Crypto era) -> Exp (RewardAccounts (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)
 RewardAccounts (Crypto era)
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 {_dstate :: DState (Crypto era)
_dstate = DState (Crypto era)
ds {_rewards :: RewardAccounts (Crypto era)
_rewards = RewardAccounts (Crypto era)
rewards'}}
    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
_pstate 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

      let ptr :: Ptr
ptr = SlotNo -> Ix -> Ix -> Ptr
Ptr SlotNo
slot Ix
txIx (Int -> Ix
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Ix) -> Int -> Ix
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 (DELPL era) super =>
RuleContext rtype (DELPL era)
-> Rule super rtype (State (DELPL era))
trans @(DELPL era) (RuleContext 'Transition (DELPL era)
 -> Rule (DELEGS era) 'Transition (State (DELPL era)))
-> RuleContext 'Transition (DELPL era)
-> Rule (DELEGS era) 'Transition (State (DELPL era))
forall a b. (a -> b) -> a -> b
$
        (Environment (DELPL era), State (DELPL era), Signal (DELPL era))
-> TRC (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 (DELPL era)
DPState (Crypto era)
dpstate', Signal (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 -> RewardAccounts (Crypto era) -> Bool
    isSubmapOf :: Map (RewardAcnt (Crypto era)) Coin
-> RewardAccounts (Crypto era) -> Bool
isSubmapOf Map (RewardAcnt (Crypto era)) Coin
wdrls_ RewardAccounts (Crypto era)
rewards = RewardAccounts (Crypto era)
wdrls_' RewardAccounts (Crypto era) -> RewardAccounts (Crypto era) -> Bool
forall k a. (Ord k, Eq a) => Map k a -> Map k a -> Bool
`Map.isSubmapOf` RewardAccounts (Crypto era)
rewards
      where
        wdrls_' :: RewardAccounts (Crypto era)
wdrls_' =
          [(Credential 'Staking (Crypto era), Coin)]
-> RewardAccounts (Crypto era)
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_
            ]

instance
  ( Era era,
    ShelleyBased era,
    HasField "wdrls" (Core.TxBody era) (Wdrl (Crypto era))
  ) =>
  Embed (DELPL era) (DELEGS era)
  where
  wrapFailed :: PredicateFailure (DELPL era) -> PredicateFailure (DELEGS era)
wrapFailed = PredicateFailure (DELPL era) -> PredicateFailure (DELEGS era)
forall era.
PredicateFailure (DELPL era) -> DelegsPredicateFailure era
DelplFailure