{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Cardano.Ledger.Shelley.Rules.Deleg (
  ShelleyDELEG,
  DelegEnv (..),
  PredicateFailure,
  ShelleyDelegPredFailure (..),
  ShelleyDelegEvent (..),
)
where

import Cardano.Ledger.BaseTypes (
  Globals (..),
  Mismatch (..),
  Relation (..),
  ShelleyBase,
  StrictMaybe (..),
  epochInfoPure,
  invalidKey,
 )
import Cardano.Ledger.Binary (
  DecCBOR (..),
  EncCBOR (..),
  decodeRecordSum,
  encodeListLen,
 )
import Cardano.Ledger.Coin (Coin (..), DeltaCoin (..), addDeltaCoin, toDeltaCoin)
import Cardano.Ledger.Credential (Credential, Ptr)
import Cardano.Ledger.Keys (
  GenDelegPair (..),
  GenDelegs (..),
  KeyHash,
  KeyRole (..),
  KeyRoleVRF (..),
  VRFVerKeyHash,
 )
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.Era (ShelleyDELEG, ShelleyEra)
import Cardano.Ledger.Shelley.HardForks as HardForks (allowMIRTransfer)
import Cardano.Ledger.Shelley.LedgerState (
  AccountState (..),
  DState (..),
  FutureGenDeleg (..),
  InstantaneousRewards (..),
  availableAfterMIR,
  delegations,
  dsFutureGenDelegs,
  dsGenDelegs,
  dsIRewards,
  rewards,
 )
import Cardano.Ledger.Slot (
  Duration (..),
  EpochNo (..),
  SlotNo,
  epochInfoEpoch,
  epochInfoFirst,
  (*-),
  (+*),
 )
import Cardano.Ledger.UMap (RDPair (..), UView (..), compactCoinOrError)
import qualified Cardano.Ledger.UMap as UM
import Control.DeepSeq
import Control.Monad (guard)
import Control.Monad.Trans.Reader (asks)
import Control.SetAlgebra (eval, range, singleton, (∉), (∪), (⨃))
import Control.State.Transition
import Data.Foldable (fold)
import Data.Group (Group (..))
import qualified Data.Map.Strict as Map
import Data.Maybe (isJust)
import qualified Data.Set as Set
import Data.Typeable (Typeable)
import Data.Word (Word8)
import GHC.Generics (Generic)
import Lens.Micro ((^.))
import NoThunks.Class (NoThunks (..))

data DelegEnv era = DelegEnv
  { forall era. DelegEnv era -> SlotNo
slotNo :: !SlotNo
  , forall era. DelegEnv era -> Ptr
ptr_ :: !Ptr
  , forall era. DelegEnv era -> AccountState
acnt_ :: !AccountState
  , forall era. DelegEnv era -> PParams era
ppDE :: !(PParams era) -- The protocol parameters are only used for the HardFork mechanism
  }
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x. Rep (DelegEnv era) x -> DelegEnv era
forall era x. DelegEnv era -> Rep (DelegEnv era) x
$cto :: forall era x. Rep (DelegEnv era) x -> DelegEnv era
$cfrom :: forall era x. DelegEnv era -> Rep (DelegEnv era) x
Generic)

deriving instance Show (PParams era) => Show (DelegEnv era)

deriving instance Eq (PParams era) => Eq (DelegEnv era)

instance NFData (PParams era) => NFData (DelegEnv era)

data ShelleyDelegPredFailure era
  = StakeKeyAlreadyRegisteredDELEG
      !(Credential 'Staking (EraCrypto era)) -- Credential which is already registered
  | -- | Indicates that the stake key is somehow already in the rewards map.
    --   This error is now redundant with StakeKeyAlreadyRegisteredDELEG.
    --   We should remove it and replace its one use with StakeKeyAlreadyRegisteredDELEG.
    StakeKeyInRewardsDELEG
      !(Credential 'Staking (EraCrypto era)) -- DEPRECATED, now redundant with StakeKeyAlreadyRegisteredDELEG
  | StakeKeyNotRegisteredDELEG
      !(Credential 'Staking (EraCrypto era)) -- Credential which is not registered
  | StakeKeyNonZeroAccountBalanceDELEG
      !(Maybe Coin) -- The remaining reward account balance, if it exists
  | StakeDelegationImpossibleDELEG
      !(Credential 'Staking (EraCrypto era)) -- Credential that is not registered
  | WrongCertificateTypeDELEG -- The TxCertPool constructor should not be used by this transition
  | GenesisKeyNotInMappingDELEG
      !(KeyHash 'Genesis (EraCrypto era)) -- Unknown Genesis KeyHash
  | DuplicateGenesisDelegateDELEG
      !(KeyHash 'GenesisDelegate (EraCrypto era)) -- Keyhash which is already delegated to
  | InsufficientForInstantaneousRewardsDELEG
      !MIRPot -- which pot the rewards are to be drawn from, treasury or reserves
      !(Mismatch 'RelLTEQ Coin)
  | MIRCertificateTooLateinEpochDELEG
      !(Mismatch 'RelLT SlotNo)
  | DuplicateGenesisVRFDELEG
      !(VRFVerKeyHash 'GenDelegVRF (EraCrypto era)) -- VRF KeyHash which is already delegated to
  | MIRTransferNotCurrentlyAllowed
  | MIRNegativesNotCurrentlyAllowed
  | InsufficientForTransferDELEG
      !MIRPot -- which pot the rewards are to be drawn from, treasury or reserves
      !(Mismatch 'RelLTEQ Coin)
  | MIRProducesNegativeUpdate
  | MIRNegativeTransfer
      !MIRPot -- which pot the rewards are to be drawn from, treasury or reserves
      !Coin -- amount attempted to transfer
  deriving (Int -> ShelleyDelegPredFailure era -> ShowS
forall era. Int -> ShelleyDelegPredFailure era -> ShowS
forall era. [ShelleyDelegPredFailure era] -> ShowS
forall era. ShelleyDelegPredFailure era -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ShelleyDelegPredFailure era] -> ShowS
$cshowList :: forall era. [ShelleyDelegPredFailure era] -> ShowS
show :: ShelleyDelegPredFailure era -> String
$cshow :: forall era. ShelleyDelegPredFailure era -> String
showsPrec :: Int -> ShelleyDelegPredFailure era -> ShowS
$cshowsPrec :: forall era. Int -> ShelleyDelegPredFailure era -> ShowS
Show, ShelleyDelegPredFailure era -> ShelleyDelegPredFailure era -> Bool
forall era.
ShelleyDelegPredFailure era -> ShelleyDelegPredFailure era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ShelleyDelegPredFailure era -> ShelleyDelegPredFailure era -> Bool
$c/= :: forall era.
ShelleyDelegPredFailure era -> ShelleyDelegPredFailure era -> Bool
== :: ShelleyDelegPredFailure era -> ShelleyDelegPredFailure era -> Bool
$c== :: forall era.
ShelleyDelegPredFailure era -> ShelleyDelegPredFailure era -> Bool
Eq, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyDelegPredFailure era) x -> ShelleyDelegPredFailure era
forall era x.
ShelleyDelegPredFailure era -> Rep (ShelleyDelegPredFailure era) x
$cto :: forall era x.
Rep (ShelleyDelegPredFailure era) x -> ShelleyDelegPredFailure era
$cfrom :: forall era x.
ShelleyDelegPredFailure era -> Rep (ShelleyDelegPredFailure era) x
Generic)

type instance EraRuleFailure "DELEG" (ShelleyEra c) = ShelleyDelegPredFailure (ShelleyEra c)

instance InjectRuleFailure "DELEG" ShelleyDelegPredFailure (ShelleyEra c)

newtype ShelleyDelegEvent era = DelegNewEpoch EpochNo
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyDelegEvent era) x -> ShelleyDelegEvent era
forall era x.
ShelleyDelegEvent era -> Rep (ShelleyDelegEvent era) x
$cto :: forall era x.
Rep (ShelleyDelegEvent era) x -> ShelleyDelegEvent era
$cfrom :: forall era x.
ShelleyDelegEvent era -> Rep (ShelleyDelegEvent era) x
Generic, ShelleyDelegEvent era -> ShelleyDelegEvent era -> Bool
forall era. ShelleyDelegEvent era -> ShelleyDelegEvent era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ShelleyDelegEvent era -> ShelleyDelegEvent era -> Bool
$c/= :: forall era. ShelleyDelegEvent era -> ShelleyDelegEvent era -> Bool
== :: ShelleyDelegEvent era -> ShelleyDelegEvent era -> Bool
$c== :: forall era. ShelleyDelegEvent era -> ShelleyDelegEvent era -> Bool
Eq)

instance NFData (ShelleyDelegEvent era)

instance (EraPParams era, ShelleyEraTxCert era, ProtVerAtMost era 8) => STS (ShelleyDELEG era) where
  type State (ShelleyDELEG era) = DState era
  type Signal (ShelleyDELEG era) = TxCert era
  type Environment (ShelleyDELEG era) = DelegEnv era
  type BaseM (ShelleyDELEG era) = ShelleyBase
  type PredicateFailure (ShelleyDELEG era) = ShelleyDelegPredFailure era
  type Event (ShelleyDELEG era) = ShelleyDelegEvent era

  transitionRules :: [TransitionRule (ShelleyDELEG era)]
transitionRules = [forall era.
(ShelleyEraTxCert era, EraPParams era, ProtVerAtMost era 8) =>
TransitionRule (ShelleyDELEG era)
delegationTransition]

instance NoThunks (ShelleyDelegPredFailure era)

instance NFData (ShelleyDelegPredFailure era)

instance
  (Era era, Typeable (Script era)) =>
  EncCBOR (ShelleyDelegPredFailure era)
  where
  encCBOR :: ShelleyDelegPredFailure era -> Encoding
encCBOR = \case
    StakeKeyAlreadyRegisteredDELEG Credential 'Staking (EraCrypto era)
cred ->
      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 Credential 'Staking (EraCrypto era)
cred
    StakeKeyNotRegisteredDELEG Credential 'Staking (EraCrypto era)
cred ->
      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 Credential 'Staking (EraCrypto era)
cred
    StakeKeyNonZeroAccountBalanceDELEG Maybe Coin
rewardBalance ->
      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 Maybe Coin
rewardBalance
    StakeDelegationImpossibleDELEG Credential 'Staking (EraCrypto era)
cred ->
      Word -> Encoding
encodeListLen Word
2 forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
3 :: Word8) forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Credential 'Staking (EraCrypto era)
cred
    ShelleyDelegPredFailure era
WrongCertificateTypeDELEG ->
      Word -> Encoding
encodeListLen Word
1 forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
4 :: Word8)
    GenesisKeyNotInMappingDELEG KeyHash 'Genesis (EraCrypto era)
gkh ->
      Word -> Encoding
encodeListLen Word
2 forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
5 :: Word8) forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR KeyHash 'Genesis (EraCrypto era)
gkh
    DuplicateGenesisDelegateDELEG KeyHash 'GenesisDelegate (EraCrypto era)
kh ->
      Word -> Encoding
encodeListLen Word
2 forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
6 :: Word8) forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR KeyHash 'GenesisDelegate (EraCrypto era)
kh
    InsufficientForInstantaneousRewardsDELEG MIRPot
pot Mismatch 'RelLTEQ Coin
m ->
      Word -> Encoding
encodeListLen Word
3
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
7 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR MIRPot
pot
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Mismatch 'RelLTEQ Coin
m
    MIRCertificateTooLateinEpochDELEG Mismatch 'RelLT SlotNo
m ->
      Word -> Encoding
encodeListLen Word
2 forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
8 :: Word8) forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Mismatch 'RelLT SlotNo
m
    DuplicateGenesisVRFDELEG VRFVerKeyHash 'GenDelegVRF (EraCrypto era)
vrf ->
      Word -> Encoding
encodeListLen Word
2 forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
9 :: Word8) forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR VRFVerKeyHash 'GenDelegVRF (EraCrypto era)
vrf
    StakeKeyInRewardsDELEG Credential 'Staking (EraCrypto era)
cred ->
      Word -> Encoding
encodeListLen Word
2 forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
10 :: Word8) forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Credential 'Staking (EraCrypto era)
cred
    ShelleyDelegPredFailure era
MIRTransferNotCurrentlyAllowed ->
      Word -> Encoding
encodeListLen Word
1 forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
11 :: Word8)
    ShelleyDelegPredFailure era
MIRNegativesNotCurrentlyAllowed ->
      Word -> Encoding
encodeListLen Word
1 forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
12 :: Word8)
    InsufficientForTransferDELEG MIRPot
pot Mismatch 'RelLTEQ Coin
m ->
      Word -> Encoding
encodeListLen Word
3
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
13 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR MIRPot
pot
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Mismatch 'RelLTEQ Coin
m
    ShelleyDelegPredFailure era
MIRProducesNegativeUpdate ->
      Word -> Encoding
encodeListLen Word
1 forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
14 :: Word8)
    MIRNegativeTransfer MIRPot
pot Coin
amt ->
      Word -> Encoding
encodeListLen Word
3
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
15 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR MIRPot
pot
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR Coin
amt

instance
  (Era era, Typeable (Script era)) =>
  DecCBOR (ShelleyDelegPredFailure era)
  where
  decCBOR :: forall s. Decoder s (ShelleyDelegPredFailure era)
decCBOR = forall s a. Text -> (Word -> Decoder s (Int, a)) -> Decoder s a
decodeRecordSum Text
"ShelleyDelegPredFailure" forall a b. (a -> b) -> a -> b
$
    \case
      Word
0 -> do
        Credential 'Staking (EraCrypto era)
kh <- forall a s. DecCBOR a => Decoder s a
decCBOR
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era.
Credential 'Staking (EraCrypto era) -> ShelleyDelegPredFailure era
StakeKeyAlreadyRegisteredDELEG Credential 'Staking (EraCrypto era)
kh)
      Word
1 -> do
        Credential 'Staking (EraCrypto era)
kh <- forall a s. DecCBOR a => Decoder s a
decCBOR
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era.
Credential 'Staking (EraCrypto era) -> ShelleyDelegPredFailure era
StakeKeyNotRegisteredDELEG Credential 'Staking (EraCrypto era)
kh)
      Word
2 -> do
        Maybe Coin
b <- forall a s. DecCBOR a => Decoder s a
decCBOR
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era. Maybe Coin -> ShelleyDelegPredFailure era
StakeKeyNonZeroAccountBalanceDELEG Maybe Coin
b)
      Word
3 -> do
        Credential 'Staking (EraCrypto era)
kh <- forall a s. DecCBOR a => Decoder s a
decCBOR
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era.
Credential 'Staking (EraCrypto era) -> ShelleyDelegPredFailure era
StakeDelegationImpossibleDELEG Credential 'Staking (EraCrypto era)
kh)
      Word
4 -> do
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
1, forall era. ShelleyDelegPredFailure era
WrongCertificateTypeDELEG)
      Word
5 -> do
        KeyHash 'Genesis (EraCrypto era)
gkh <- forall a s. DecCBOR a => Decoder s a
decCBOR
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era.
KeyHash 'Genesis (EraCrypto era) -> ShelleyDelegPredFailure era
GenesisKeyNotInMappingDELEG KeyHash 'Genesis (EraCrypto era)
gkh)
      Word
6 -> do
        KeyHash 'GenesisDelegate (EraCrypto era)
kh <- forall a s. DecCBOR a => Decoder s a
decCBOR
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era.
KeyHash 'GenesisDelegate (EraCrypto era)
-> ShelleyDelegPredFailure era
DuplicateGenesisDelegateDELEG KeyHash 'GenesisDelegate (EraCrypto era)
kh)
      Word
7 -> do
        MIRPot
pot <- forall a s. DecCBOR a => Decoder s a
decCBOR
        Mismatch 'RelLTEQ Coin
m <- forall a s. DecCBOR a => Decoder s a
decCBOR
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, forall era.
MIRPot -> Mismatch 'RelLTEQ Coin -> ShelleyDelegPredFailure era
InsufficientForInstantaneousRewardsDELEG MIRPot
pot Mismatch 'RelLTEQ Coin
m)
      Word
8 -> do
        Mismatch 'RelLT SlotNo
m <- forall a s. DecCBOR a => Decoder s a
decCBOR
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era. Mismatch 'RelLT SlotNo -> ShelleyDelegPredFailure era
MIRCertificateTooLateinEpochDELEG Mismatch 'RelLT SlotNo
m)
      Word
9 -> do
        VRFVerKeyHash 'GenDelegVRF (EraCrypto era)
vrf <- forall a s. DecCBOR a => Decoder s a
decCBOR
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era.
VRFVerKeyHash 'GenDelegVRF (EraCrypto era)
-> ShelleyDelegPredFailure era
DuplicateGenesisVRFDELEG VRFVerKeyHash 'GenDelegVRF (EraCrypto era)
vrf)
      Word
10 -> do
        Credential 'Staking (EraCrypto era)
kh <- forall a s. DecCBOR a => Decoder s a
decCBOR
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era.
Credential 'Staking (EraCrypto era) -> ShelleyDelegPredFailure era
StakeKeyInRewardsDELEG Credential 'Staking (EraCrypto era)
kh)
      Word
11 -> do
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
1, forall era. ShelleyDelegPredFailure era
MIRTransferNotCurrentlyAllowed)
      Word
12 -> do
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
1, forall era. ShelleyDelegPredFailure era
MIRNegativesNotCurrentlyAllowed)
      Word
13 -> do
        MIRPot
pot <- forall a s. DecCBOR a => Decoder s a
decCBOR
        Mismatch 'RelLTEQ Coin
m <- forall a s. DecCBOR a => Decoder s a
decCBOR
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, forall era.
MIRPot -> Mismatch 'RelLTEQ Coin -> ShelleyDelegPredFailure era
InsufficientForTransferDELEG MIRPot
pot Mismatch 'RelLTEQ Coin
m)
      Word
14 -> do
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
1, forall era. ShelleyDelegPredFailure era
MIRProducesNegativeUpdate)
      Word
15 -> do
        MIRPot
pot <- forall a s. DecCBOR a => Decoder s a
decCBOR
        Coin
amt <- forall a s. DecCBOR a => Decoder s a
decCBOR
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, forall era. MIRPot -> Coin -> ShelleyDelegPredFailure era
MIRNegativeTransfer MIRPot
pot Coin
amt)
      Word
k -> forall (m :: * -> *) a. MonadFail m => Word -> m a
invalidKey Word
k

delegationTransition ::
  (ShelleyEraTxCert era, EraPParams era, ProtVerAtMost era 8) =>
  TransitionRule (ShelleyDELEG era)
delegationTransition :: forall era.
(ShelleyEraTxCert era, EraPParams era, ProtVerAtMost era 8) =>
TransitionRule (ShelleyDELEG era)
delegationTransition = do
  TRC (DelegEnv SlotNo
slot Ptr
ptr AccountState
acnt PParams era
pp, State (ShelleyDELEG era)
ds, Signal (ShelleyDELEG era)
c) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  let pv :: ProtVer
pv = PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) ProtVer
ppProtocolVersionL
  case Signal (ShelleyDELEG era)
c of
    RegTxCert Credential 'Staking (EraCrypto era)
hk -> do
      -- (hk ∉ dom (rewards ds))
      forall k c v. k -> UView c k v -> Bool
UM.notMember Credential 'Staking (EraCrypto era)
hk (forall era.
DState era
-> UView
     (EraCrypto era) (Credential 'Staking (EraCrypto era)) RDPair
rewards State (ShelleyDELEG era)
ds) forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era.
Credential 'Staking (EraCrypto era) -> ShelleyDelegPredFailure era
StakeKeyAlreadyRegisteredDELEG Credential 'Staking (EraCrypto era)
hk
      let u1 :: UMap (EraCrypto era)
u1 = forall era. DState era -> UMap (EraCrypto era)
dsUnified State (ShelleyDELEG era)
ds
          deposit :: CompactForm Coin
deposit = HasCallStack => Coin -> CompactForm Coin
compactCoinOrError (PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) Coin
ppKeyDepositL)
          u2 :: UMap (EraCrypto era)
u2 = forall c. UMap c -> UView c (Credential 'Staking c) RDPair
RewDepUView UMap (EraCrypto era)
u1 forall c k v. UView c k v -> (k, v) -> UMap c
UM.∪ (Credential 'Staking (EraCrypto era)
hk, CompactForm Coin -> CompactForm Coin -> RDPair
RDPair (Word64 -> CompactForm Coin
UM.CompactCoin Word64
0) CompactForm Coin
deposit)
          u3 :: UMap (EraCrypto era)
u3 = forall c. UMap c -> UView c Ptr (Credential 'Staking c)
PtrUView UMap (EraCrypto era)
u2 forall c k v. UView c k v -> (k, v) -> UMap c
UM.∪ (Ptr
ptr, Credential 'Staking (EraCrypto era)
hk)
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (State (ShelleyDELEG era)
ds {dsUnified :: UMap (EraCrypto era)
dsUnified = UMap (EraCrypto era)
u3})
    UnRegTxCert Credential 'Staking (EraCrypto era)
cred -> do
      -- (hk ∈ dom (rewards ds))
      let (Maybe (UMElem (EraCrypto era))
mUMElem, UMap (EraCrypto era)
umap) = forall c.
Credential 'Staking c -> UMap c -> (Maybe (UMElem c), UMap c)
UM.extractStakingCredential Credential 'Staking (EraCrypto era)
cred (forall era. DState era -> UMap (EraCrypto era)
dsUnified State (ShelleyDELEG era)
ds)
          checkStakeKeyHasZeroRewardBalance :: Maybe Coin
checkStakeKeyHasZeroRewardBalance = do
            UM.UMElem (SJust RDPair
rd) Set Ptr
_ StrictMaybe (KeyHash 'StakePool (EraCrypto era))
_ StrictMaybe (DRep (EraCrypto era))
_ <- Maybe (UMElem (EraCrypto era))
mUMElem
            forall (f :: * -> *). Alternative f => Bool -> f ()
guard (RDPair -> CompactForm Coin
UM.rdReward RDPair
rd forall a. Eq a => a -> a -> Bool
/= forall a. Monoid a => a
mempty)
            forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Compactible a => CompactForm a -> a
UM.fromCompact (RDPair -> CompactForm Coin
UM.rdReward RDPair
rd)
      forall a. Maybe a -> Bool
isJust Maybe (UMElem (EraCrypto era))
mUMElem forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era.
Credential 'Staking (EraCrypto era) -> ShelleyDelegPredFailure era
StakeKeyNotRegisteredDELEG Credential 'Staking (EraCrypto era)
cred
      forall a sts (ctx :: RuleType).
Maybe a -> (a -> PredicateFailure sts) -> Rule sts ctx ()
failOnJust Maybe Coin
checkStakeKeyHasZeroRewardBalance (forall era. Maybe Coin -> ShelleyDelegPredFailure era
StakeKeyNonZeroAccountBalanceDELEG forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just)
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ State (ShelleyDELEG era)
ds {dsUnified :: UMap (EraCrypto era)
dsUnified = UMap (EraCrypto era)
umap}
    DelegStakeTxCert Credential 'Staking (EraCrypto era)
hk KeyHash 'StakePool (EraCrypto era)
dpool -> do
      -- note that pattern match is used instead of cwitness and dpool, as in the spec
      -- (hk ∈ dom (rewards ds))
      forall k c v. k -> UView c k v -> Bool
UM.member Credential 'Staking (EraCrypto era)
hk (forall era.
DState era
-> UView
     (EraCrypto era) (Credential 'Staking (EraCrypto era)) RDPair
rewards State (ShelleyDELEG era)
ds) forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era.
Credential 'Staking (EraCrypto era) -> ShelleyDelegPredFailure era
StakeDelegationImpossibleDELEG Credential 'Staking (EraCrypto era)
hk

      forall (f :: * -> *) a. Applicative f => a -> f a
pure (State (ShelleyDELEG era)
ds {dsUnified :: UMap (EraCrypto era)
dsUnified = forall era.
DState era
-> UView
     (EraCrypto era)
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era))
delegations State (ShelleyDELEG era)
ds forall c k v. UView c k v -> Map k v -> UMap c
UM.⨃ forall k a. k -> a -> Map k a
Map.singleton Credential 'Staking (EraCrypto era)
hk KeyHash 'StakePool (EraCrypto era)
dpool})
    GenesisDelegTxCert KeyHash 'Genesis (EraCrypto era)
gkh KeyHash 'GenesisDelegate (EraCrypto era)
vkh VRFVerKeyHash 'GenDelegVRF (EraCrypto era)
vrf -> do
      Word64
sp <- 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 -> Word64
stabilityWindow
      -- note that pattern match is used instead of genesisDeleg, as in the spec
      let s' :: SlotNo
s' = SlotNo
slot SlotNo -> Duration -> SlotNo
+* Word64 -> Duration
Duration Word64
sp
          GenDelegs Map
  (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
genDelegs = forall era. DState era -> GenDelegs (EraCrypto era)
dsGenDelegs State (ShelleyDELEG era)
ds

      -- gkh ∈ dom genDelegs ?! GenesisKeyNotInMappingDELEG gkh
      forall a. Maybe a -> Bool
isJust (forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KeyHash 'Genesis (EraCrypto era)
gkh Map
  (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
genDelegs) forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era.
KeyHash 'Genesis (EraCrypto era) -> ShelleyDelegPredFailure era
GenesisKeyNotInMappingDELEG KeyHash 'Genesis (EraCrypto era)
gkh

      let cod :: Set (GenDelegPair (EraCrypto era))
cod = forall (f :: * -> * -> *) v k. (Basic f, Ord v) => f k v -> Set v
range forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Map k a
Map.delete KeyHash 'Genesis (EraCrypto era)
gkh Map
  (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
genDelegs
          fod :: Set (GenDelegPair (EraCrypto era))
fod =
            forall (f :: * -> * -> *) v k. (Basic f, Ord v) => f k v -> Set v
range forall a b. (a -> b) -> a -> b
$
              forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\(FutureGenDeleg SlotNo
_ KeyHash 'Genesis (EraCrypto era)
g) GenDelegPair (EraCrypto era)
_ -> KeyHash 'Genesis (EraCrypto era)
g forall a. Eq a => a -> a -> Bool
/= KeyHash 'Genesis (EraCrypto era)
gkh) (forall era.
DState era
-> Map
     (FutureGenDeleg (EraCrypto era)) (GenDelegPair (EraCrypto era))
dsFutureGenDelegs State (ShelleyDELEG era)
ds)
          currentOtherColdKeyHashes :: Set (KeyHash 'GenesisDelegate (EraCrypto era))
currentOtherColdKeyHashes = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map forall c. GenDelegPair c -> KeyHash 'GenesisDelegate c
genDelegKeyHash Set (GenDelegPair (EraCrypto era))
cod
          currentOtherVrfKeyHashes :: Set (VRFVerKeyHash 'GenDelegVRF (EraCrypto era))
currentOtherVrfKeyHashes = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map forall c. GenDelegPair c -> VRFVerKeyHash 'GenDelegVRF c
genDelegVrfHash Set (GenDelegPair (EraCrypto era))
cod
          futureOtherColdKeyHashes :: Set (KeyHash 'GenesisDelegate (EraCrypto era))
futureOtherColdKeyHashes = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map forall c. GenDelegPair c -> KeyHash 'GenesisDelegate c
genDelegKeyHash Set (GenDelegPair (EraCrypto era))
fod
          futureOtherVrfKeyHashes :: Set (VRFVerKeyHash 'GenDelegVRF (EraCrypto era))
futureOtherVrfKeyHashes = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map forall c. GenDelegPair c -> VRFVerKeyHash 'GenDelegVRF c
genDelegVrfHash Set (GenDelegPair (EraCrypto era))
fod

      forall s t. Embed s t => Exp t -> s
eval (KeyHash 'GenesisDelegate (EraCrypto era)
vkh forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∉ (Set (KeyHash 'GenesisDelegate (EraCrypto era))
currentOtherColdKeyHashes forall k v s1 (f :: * -> * -> *) s2 (g :: * -> * -> *).
(Show k, Show v, Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) =>
s1 -> s2 -> Exp (f k v)
∪ Set (KeyHash 'GenesisDelegate (EraCrypto era))
futureOtherColdKeyHashes))
        forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era.
KeyHash 'GenesisDelegate (EraCrypto era)
-> ShelleyDelegPredFailure era
DuplicateGenesisDelegateDELEG KeyHash 'GenesisDelegate (EraCrypto era)
vkh
      forall s t. Embed s t => Exp t -> s
eval (VRFVerKeyHash 'GenDelegVRF (EraCrypto era)
vrf forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∉ (Set (VRFVerKeyHash 'GenDelegVRF (EraCrypto era))
currentOtherVrfKeyHashes forall k v s1 (f :: * -> * -> *) s2 (g :: * -> * -> *).
(Show k, Show v, Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) =>
s1 -> s2 -> Exp (f k v)
∪ Set (VRFVerKeyHash 'GenDelegVRF (EraCrypto era))
futureOtherVrfKeyHashes))
        forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era.
VRFVerKeyHash 'GenDelegVRF (EraCrypto era)
-> ShelleyDelegPredFailure era
DuplicateGenesisVRFDELEG VRFVerKeyHash 'GenDelegVRF (EraCrypto era)
vrf

      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        State (ShelleyDELEG era)
ds
          { dsFutureGenDelegs :: Map (FutureGenDeleg (EraCrypto era)) (GenDelegPair (EraCrypto era))
dsFutureGenDelegs =
              forall s t. Embed s t => Exp t -> s
eval (forall era.
DState era
-> Map
     (FutureGenDeleg (EraCrypto era)) (GenDelegPair (EraCrypto era))
dsFutureGenDelegs State (ShelleyDELEG era)
ds 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)
⨃ forall k v. Ord k => k -> v -> Exp (Single k v)
singleton (forall c. SlotNo -> KeyHash 'Genesis c -> FutureGenDeleg c
FutureGenDeleg SlotNo
s' KeyHash 'Genesis (EraCrypto era)
gkh) (forall c.
KeyHash 'GenesisDelegate c
-> VRFVerKeyHash 'GenDelegVRF c -> GenDelegPair c
GenDelegPair KeyHash 'GenesisDelegate (EraCrypto era)
vkh VRFVerKeyHash 'GenDelegVRF (EraCrypto era)
vrf))
          }
    RegPoolTxCert PoolParams (EraCrypto era)
_ -> do
      forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause forall era. ShelleyDelegPredFailure era
WrongCertificateTypeDELEG -- this always fails
      forall (f :: * -> *) a. Applicative f => a -> f a
pure State (ShelleyDELEG era)
ds
    Signal (ShelleyDELEG era)
_ | Just (MIRCert MIRPot
targetPot MIRTarget (EraCrypto era)
mirTarget) <- forall era.
(ShelleyEraTxCert era, ProtVerAtMost era 8) =>
TxCert era -> Maybe (MIRCert (EraCrypto era))
getMirTxCert Signal (ShelleyDELEG era)
c -> do
      forall era.
(ShelleyEraTxCert era, EraPParams era, ProtVerAtMost era 8) =>
SlotNo -> Rule (ShelleyDELEG era) 'Transition ()
checkSlotNotTooLate SlotNo
slot
      case MIRTarget (EraCrypto era)
mirTarget of
        StakeAddressesMIR Map (Credential 'Staking (EraCrypto era)) DeltaCoin
credCoinMap -> do
          let (Coin
potAmount, DeltaCoin
delta, Map (Credential 'Staking (EraCrypto era)) Coin
instantaneousRewards) =
                case MIRPot
targetPot of
                  MIRPot
ReservesMIR ->
                    (AccountState -> Coin
asReserves AccountState
acnt, forall c. InstantaneousRewards c -> DeltaCoin
deltaReserves forall a b. (a -> b) -> a -> b
$ forall era. DState era -> InstantaneousRewards (EraCrypto era)
dsIRewards State (ShelleyDELEG era)
ds, forall c.
InstantaneousRewards c -> Map (Credential 'Staking c) Coin
iRReserves forall a b. (a -> b) -> a -> b
$ forall era. DState era -> InstantaneousRewards (EraCrypto era)
dsIRewards State (ShelleyDELEG era)
ds)
                  MIRPot
TreasuryMIR ->
                    (AccountState -> Coin
asTreasury AccountState
acnt, forall c. InstantaneousRewards c -> DeltaCoin
deltaTreasury forall a b. (a -> b) -> a -> b
$ forall era. DState era -> InstantaneousRewards (EraCrypto era)
dsIRewards State (ShelleyDELEG era)
ds, forall c.
InstantaneousRewards c -> Map (Credential 'Staking c) Coin
iRTreasury forall a b. (a -> b) -> a -> b
$ forall era. DState era -> InstantaneousRewards (EraCrypto era)
dsIRewards State (ShelleyDELEG era)
ds)
          let credCoinMap' :: Map (Credential 'Staking (EraCrypto era)) Coin
credCoinMap' = forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\(DeltaCoin Integer
x) -> Integer -> Coin
Coin Integer
x) Map (Credential 'Staking (EraCrypto era)) DeltaCoin
credCoinMap
          (Map (Credential 'Staking (EraCrypto era)) Coin
combinedMap, Coin
available) <-
            if ProtVer -> Bool
HardForks.allowMIRTransfer ProtVer
pv
              then do
                let cm :: Map (Credential 'Staking (EraCrypto era)) Coin
cm = forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith forall a. Semigroup a => a -> a -> a
(<>) Map (Credential 'Staking (EraCrypto era)) Coin
credCoinMap' Map (Credential 'Staking (EraCrypto era)) Coin
instantaneousRewards
                forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Ord a => a -> a -> Bool
>= forall a. Monoid a => a
mempty) Map (Credential 'Staking (EraCrypto era)) Coin
cm forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era. ShelleyDelegPredFailure era
MIRProducesNegativeUpdate
                forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map (Credential 'Staking (EraCrypto era)) Coin
cm, Coin
potAmount Coin -> DeltaCoin -> Coin
`addDeltaCoin` DeltaCoin
delta)
              else do
                forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Ord a => a -> a -> Bool
>= forall a. Monoid a => a
mempty) Map (Credential 'Staking (EraCrypto era)) DeltaCoin
credCoinMap forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era. ShelleyDelegPredFailure era
MIRNegativesNotCurrentlyAllowed
                forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map (Credential 'Staking (EraCrypto era)) Coin
credCoinMap' Map (Credential 'Staking (EraCrypto era)) Coin
instantaneousRewards, Coin
potAmount)
          forall era.
MIRPot
-> Map (Credential 'Staking (EraCrypto era)) Coin
-> Coin
-> DState era
-> Rule (ShelleyDELEG era) 'Transition (DState era)
updateReservesAndTreasury MIRPot
targetPot Map (Credential 'Staking (EraCrypto era)) Coin
combinedMap Coin
available State (ShelleyDELEG era)
ds
        SendToOppositePotMIR Coin
coin ->
          if ProtVer -> Bool
HardForks.allowMIRTransfer ProtVer
pv
            then do
              let available :: Coin
available = forall c. MIRPot -> AccountState -> InstantaneousRewards c -> Coin
availableAfterMIR MIRPot
targetPot AccountState
acnt (forall era. DState era -> InstantaneousRewards (EraCrypto era)
dsIRewards State (ShelleyDELEG era)
ds)
              Coin
coin forall a. Ord a => a -> a -> Bool
>= forall a. Monoid a => a
mempty forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era. MIRPot -> Coin -> ShelleyDelegPredFailure era
MIRNegativeTransfer MIRPot
targetPot Coin
coin
              Coin
coin forall a. Ord a => a -> a -> Bool
<= Coin
available forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era.
MIRPot -> Mismatch 'RelLTEQ Coin -> ShelleyDelegPredFailure era
InsufficientForTransferDELEG MIRPot
targetPot (forall (r :: Relation) a. a -> a -> Mismatch r a
Mismatch Coin
coin Coin
available)

              let ir :: InstantaneousRewards (EraCrypto era)
ir = forall era. DState era -> InstantaneousRewards (EraCrypto era)
dsIRewards State (ShelleyDELEG era)
ds
                  dr :: DeltaCoin
dr = forall c. InstantaneousRewards c -> DeltaCoin
deltaReserves InstantaneousRewards (EraCrypto era)
ir
                  dt :: DeltaCoin
dt = forall c. InstantaneousRewards c -> DeltaCoin
deltaTreasury InstantaneousRewards (EraCrypto era)
ir
              case MIRPot
targetPot of
                MIRPot
ReservesMIR ->
                  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
                    State (ShelleyDELEG era)
ds
                      { dsIRewards :: InstantaneousRewards (EraCrypto era)
dsIRewards =
                          InstantaneousRewards (EraCrypto era)
ir
                            { deltaReserves :: DeltaCoin
deltaReserves = DeltaCoin
dr forall a. Semigroup a => a -> a -> a
<> forall m. Group m => m -> m
invert (Coin -> DeltaCoin
toDeltaCoin Coin
coin)
                            , deltaTreasury :: DeltaCoin
deltaTreasury = DeltaCoin
dt forall a. Semigroup a => a -> a -> a
<> Coin -> DeltaCoin
toDeltaCoin Coin
coin
                            }
                      }
                MIRPot
TreasuryMIR ->
                  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
                    State (ShelleyDELEG era)
ds
                      { dsIRewards :: InstantaneousRewards (EraCrypto era)
dsIRewards =
                          InstantaneousRewards (EraCrypto era)
ir
                            { deltaReserves :: DeltaCoin
deltaReserves = DeltaCoin
dr forall a. Semigroup a => a -> a -> a
<> Coin -> DeltaCoin
toDeltaCoin Coin
coin
                            , deltaTreasury :: DeltaCoin
deltaTreasury = DeltaCoin
dt forall a. Semigroup a => a -> a -> a
<> forall m. Group m => m -> m
invert (Coin -> DeltaCoin
toDeltaCoin Coin
coin)
                            }
                      }
            else do
              forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause forall era. ShelleyDelegPredFailure era
MIRTransferNotCurrentlyAllowed
              forall (f :: * -> *) a. Applicative f => a -> f a
pure State (ShelleyDELEG era)
ds
    Signal (ShelleyDELEG era)
_ -> do
      -- The impossible case
      forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause forall era. ShelleyDelegPredFailure era
WrongCertificateTypeDELEG -- this always fails
      forall (f :: * -> *) a. Applicative f => a -> f a
pure State (ShelleyDELEG era)
ds

checkSlotNotTooLate ::
  (ShelleyEraTxCert era, EraPParams era, ProtVerAtMost era 8) =>
  SlotNo ->
  Rule (ShelleyDELEG era) 'Transition ()
checkSlotNotTooLate :: forall era.
(ShelleyEraTxCert era, EraPParams era, ProtVerAtMost era 8) =>
SlotNo -> Rule (ShelleyDELEG era) 'Transition ()
checkSlotNotTooLate SlotNo
slot = do
  Word64
sp <- 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 -> Word64
stabilityWindow
  EpochInfo Identity
ei <- 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 -> EpochInfo Identity
epochInfoPure
  EpochNo Word64
currEpoch <- forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS forall a b. (a -> b) -> a -> b
$ HasCallStack => EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
epochInfoEpoch EpochInfo Identity
ei SlotNo
slot
  let newEpoch :: EpochNo
newEpoch = Word64 -> EpochNo
EpochNo (Word64
currEpoch forall a. Num a => a -> a -> a
+ Word64
1)
  forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent (forall era. EpochNo -> ShelleyDelegEvent era
DelegNewEpoch EpochNo
newEpoch)
  SlotNo
firstSlot <- forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS forall a b. (a -> b) -> a -> b
$ HasCallStack => EpochInfo Identity -> EpochNo -> ShelleyBase SlotNo
epochInfoFirst EpochInfo Identity
ei EpochNo
newEpoch
  let tooLate :: SlotNo
tooLate = SlotNo
firstSlot SlotNo -> Duration -> SlotNo
*- Word64 -> Duration
Duration Word64
sp
  SlotNo
slot forall a. Ord a => a -> a -> Bool
< SlotNo
tooLate forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era. Mismatch 'RelLT SlotNo -> ShelleyDelegPredFailure era
MIRCertificateTooLateinEpochDELEG (forall (r :: Relation) a. a -> a -> Mismatch r a
Mismatch SlotNo
slot SlotNo
tooLate)

updateReservesAndTreasury ::
  MIRPot ->
  Map.Map (Credential 'Staking (EraCrypto era)) Coin ->
  Coin ->
  DState era ->
  Rule (ShelleyDELEG era) 'Transition (DState era)
updateReservesAndTreasury :: forall era.
MIRPot
-> Map (Credential 'Staking (EraCrypto era)) Coin
-> Coin
-> DState era
-> Rule (ShelleyDELEG era) 'Transition (DState era)
updateReservesAndTreasury MIRPot
targetPot Map (Credential 'Staking (EraCrypto era)) Coin
combinedMap Coin
available DState era
ds = do
  let requiredForRewards :: Coin
requiredForRewards = forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (Credential 'Staking (EraCrypto era)) Coin
combinedMap
  Coin
requiredForRewards
    forall a. Ord a => a -> a -> Bool
<= Coin
available
      forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era.
MIRPot -> Mismatch 'RelLTEQ Coin -> ShelleyDelegPredFailure era
InsufficientForInstantaneousRewardsDELEG
        MIRPot
targetPot
        Mismatch
          { mismatchSupplied :: Coin
mismatchSupplied = Coin
requiredForRewards
          , mismatchExpected :: Coin
mismatchExpected = Coin
available
          }
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
    case MIRPot
targetPot of
      MIRPot
ReservesMIR -> DState era
ds {dsIRewards :: InstantaneousRewards (EraCrypto era)
dsIRewards = (forall era. DState era -> InstantaneousRewards (EraCrypto era)
dsIRewards DState era
ds) {iRReserves :: Map (Credential 'Staking (EraCrypto era)) Coin
iRReserves = Map (Credential 'Staking (EraCrypto era)) Coin
combinedMap}}
      MIRPot
TreasuryMIR -> DState era
ds {dsIRewards :: InstantaneousRewards (EraCrypto era)
dsIRewards = (forall era. DState era -> InstantaneousRewards (EraCrypto era)
dsIRewards DState era
ds) {iRTreasury :: Map (Credential 'Staking (EraCrypto era)) Coin
iRTreasury = Map (Credential 'Staking (EraCrypto era)) Coin
combinedMap}}