{-# 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 (
EpochNo,
Network,
ShelleyBase,
TxIx,
invalidKey,
mkCertIxPartial,
networkId,
)
import Cardano.Ledger.Binary (
DecCBOR (..),
EncCBOR (..),
decodeRecordSum,
encodeListLen,
)
import Cardano.Ledger.Coin (Coin)
import Cardano.Ledger.Core
import Cardano.Ledger.Credential (Credential, Ptr (..))
import Cardano.Ledger.Rules.ValidationMode (Test)
import Cardano.Ledger.Shelley.Era (ShelleyDELEGS, ShelleyEra)
import Cardano.Ledger.Shelley.LedgerState (
AccountState,
CertState (..),
DState (..),
PState (..),
certDState,
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.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 (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
, 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 -> AccountState
delegsAccount :: !AccountState
}
deriving stock instance
( Show (Tx era)
, Show (PParams era)
) =>
Show (DelegsEnv era)
data ShelleyDelegsPredFailure era
=
DelegateeNotRegisteredDELEG
!(KeyHash 'StakePool)
|
WithdrawalsNotInRewardsDELEGS
!(Map RewardAccount Coin)
|
DelplFailure !(PredicateFailure (EraRule "DELPL" era))
deriving (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
$cto :: forall era x.
Rep (ShelleyDelegsPredFailure era) x
-> ShelleyDelegsPredFailure era
$cfrom :: forall era x.
ShelleyDelegsPredFailure era
-> Rep (ShelleyDelegsPredFailure era) x
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 = forall era.
PredicateFailure (EraRule "DELPL" era)
-> ShelleyDelegsPredFailure era
DelplFailure
instance InjectRuleFailure "DELEGS" ShelleyPoolPredFailure ShelleyEra where
injectFailure :: ShelleyPoolPredFailure ShelleyEra
-> EraRuleFailure "DELEGS" ShelleyEra
injectFailure = forall era.
PredicateFailure (EraRule "DELPL" era)
-> ShelleyDelegsPredFailure era
DelplFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall era.
PredicateFailure (EraRule "DELPL" era)
-> ShelleyDelegsPredFailure era
DelplFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 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
$cto :: forall era x.
Rep (ShelleyDelegsEvent era) x -> ShelleyDelegsEvent era
$cfrom :: forall era x.
ShelleyDelegsEvent era -> Rep (ShelleyDelegsEvent era) x
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
, 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 = [forall era.
(EraTx 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
forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
0 :: Word8)
forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR KeyHash 'StakePool
kh
WithdrawalsNotInRewardsDELEGS Map RewardAccount Coin
ws ->
Word -> Encoding
encodeListLen Word
2
forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
1 :: Word8)
forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Map RewardAccount Coin
ws
(DelplFailure PredicateFailure (EraRule "DELPL" era)
a) ->
Word -> Encoding
encodeListLen Word
2
forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
2 :: Word8)
forall a. Semigroup a => a -> a -> a
<> 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 =
forall s a. Text -> (Word -> Decoder s (Int, a)) -> Decoder s a
decodeRecordSum Text
"PredicateFailure" forall a b. (a -> b) -> a -> b
$
\case
Word
0 -> do
KeyHash 'StakePool
kh <- forall a s. DecCBOR a => Decoder s a
decCBOR
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era. KeyHash 'StakePool -> ShelleyDelegsPredFailure era
DelegateeNotRegisteredDELEG KeyHash 'StakePool
kh)
Word
1 -> do
Map RewardAccount Coin
ws <- forall a s. DecCBOR a => Decoder s a
decCBOR
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era. Map RewardAccount Coin -> ShelleyDelegsPredFailure era
WithdrawalsNotInRewardsDELEGS Map RewardAccount Coin
ws)
Word
2 -> do
PredicateFailure (EraRule "DELPL" era)
a <- forall a s. DecCBOR a => Decoder s a
decCBOR
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era.
PredicateFailure (EraRule "DELPL" era)
-> ShelleyDelegsPredFailure era
DelplFailure PredicateFailure (EraRule "DELPL" era)
a)
Word
k -> forall (m :: * -> *) a. MonadFail m => Word -> m a
invalidKey Word
k
delegsTransition ::
forall era.
( EraTx 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, 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 SlotNo
slot EpochNo
epochNo TxIx
txIx PParams era
pp Tx era
tx AccountState
acnt), State (ShelleyDELEGS era)
certState, Signal (ShelleyDELEGS era)
certificates) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
Network
network <- forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS forall a b. (a -> b) -> a -> b
$ 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 = forall era. CertState era -> DState era
certDState State (ShelleyDELEGS era)
certState
withdrawals :: Withdrawals
withdrawals = Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraTxBody era => Lens' (TxBody era) Withdrawals
withdrawalsTxBodyL
forall e sts (ctx :: RuleType).
(e -> PredicateFailure sts)
-> Validation (NonEmpty e) () -> Rule sts ctx ()
validateTrans forall era. Map RewardAccount Coin -> ShelleyDelegsPredFailure era
WithdrawalsNotInRewardsDELEGS forall a b. (a -> b) -> a -> b
$
forall era.
DState era
-> Withdrawals -> Network -> Test (Map RewardAccount Coin)
validateZeroRewards DState era
dState Withdrawals
withdrawals Network
network
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ State (ShelleyDELEGS era)
certState {certDState :: DState era
certDState = 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) forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment (ShelleyDELEGS era)
env, State (ShelleyDELEGS era)
certState, Seq (TxCert era)
gamma)
forall e sts (ctx :: RuleType).
(e -> PredicateFailure sts)
-> Validation (NonEmpty e) () -> Rule sts ctx ()
validateTrans forall era. KeyHash 'StakePool -> ShelleyDelegsPredFailure era
DelegateeNotRegisteredDELEG forall a b. (a -> b) -> a -> b
$
case TxCert era
txCert of
DelegStakeTxCert StakeCredential
_ KeyHash 'StakePool
targetPool ->
forall era.
PState era
-> KeyHash 'StakePool
-> Validation (NonEmpty (KeyHash 'StakePool)) ()
validateStakePoolDelegateeRegistered (forall era. CertState era -> PState era
certPState CertState era
certState') KeyHash 'StakePool
targetPool
TxCert era
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
let ptr :: Ptr
ptr = SlotNo -> TxIx -> CertIx -> Ptr
Ptr SlotNo
slot TxIx
txIx (HasCallStack => Integer -> CertIx
mkCertIxPartial forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> Integer
toInteger forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq (TxCert era)
gamma)
forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "DELPL" era) forall a b. (a -> b) -> a -> b
$
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (forall era.
SlotNo
-> EpochNo -> Ptr -> PParams era -> AccountState -> DelplEnv era
DelplEnv SlotNo
slot EpochNo
epochNo Ptr
ptr PParams era
pp AccountState
acnt, CertState era
certState', TxCert 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 = forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams PState era
pState
in forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (forall s t. Embed s t => Exp t -> s
eval (KeyHash 'StakePool
targetPool forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∈ 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
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
_)) = 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 = 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 forall a. Eq a => a -> a -> Bool
== 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 :: UMap
dsUnified = forall era. DState era -> UView StakeCredential RDPair
rewards DState era
dState forall k v. UView k v -> Map k v -> UMap
UM.⨃ Map StakeCredential RDPair
drainedRewardAccounts}
where
drainedRewardAccounts :: Map StakeCredential RDPair
drainedRewardAccounts =
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey
( \(RewardAccount Network
_ StakeCredential
cred) Coin
_coin ->
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))
)
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 -> Test (Map RewardAccount Coin)
validateZeroRewards DState era
dState (Withdrawals Map RewardAccount Coin
wdrls) Network
network = do
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (Map RewardAccount Coin -> UView StakeCredential RDPair -> Bool
isSubmapOfUM Map RewardAccount Coin
wdrls (forall era. DState era -> UView StakeCredential RDPair
rewards DState era
dState)) forall a b. (a -> b) -> a -> b
$
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 forall a. Eq a => a -> a -> Bool
/= Coin
y then forall a. a -> Maybe a
Just Coin
x else forall a. Maybe a
Nothing)
Map RewardAccount Coin
wdrls
(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 (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 = forall era.
PredicateFailure (EraRule "DELPL" era)
-> ShelleyDelegsPredFailure era
DelplFailure
wrapEvent :: Event (ShelleyDELPL era) -> Event (ShelleyDELEGS era)
wrapEvent = forall era. Event (EraRule "DELPL" era) -> ShelleyDelegsEvent era
DelplEvent