{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Cardano.Ledger.Shelley.Rules.Deleg
  ( DELEG,
    DelegEnv (..),
    PredicateFailure,
    DelegPredicateFailure (..),
  )
where

import Cardano.Binary
  ( FromCBOR (..),
    ToCBOR (..),
    encodeListLen,
  )
import Cardano.Ledger.BaseTypes (Globals (..), ProtVer, ShelleyBase, epochInfoPure, invalidKey)
import Cardano.Ledger.Coin (Coin (..), DeltaCoin (..), addDeltaCoin, toDeltaCoin)
import qualified Cardano.Ledger.Core as Core
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.Era (Crypto, Era)
import Cardano.Ledger.Keys
  ( GenDelegPair (..),
    GenDelegs (..),
    Hash,
    KeyHash,
    KeyRole (..),
    VerKeyVRF,
  )
import Cardano.Ledger.Serialization (decodeRecordSum)
import Cardano.Ledger.Shelley.HardForks as HardForks
import Cardano.Ledger.Shelley.LedgerState
  ( AccountState (..),
    DState (..),
    FutureGenDeleg (..),
    InstantaneousRewards (..),
    availableAfterMIR,
    delegations,
    rewards,
    _fGenDelegs,
    _genDelegs,
    _irwd,
  )
import Cardano.Ledger.Shelley.TxBody
  ( DCert (..),
    DelegCert (..),
    Delegation (..),
    GenesisDelegCert (..),
    MIRCert (..),
    MIRPot (..),
    MIRTarget (..),
    Ptr,
  )
import Cardano.Ledger.Slot
  ( Duration (..),
    EpochNo (..),
    SlotNo,
    epochInfoEpoch,
    epochInfoFirst,
    (*-),
    (+*),
  )
import Cardano.Ledger.UnifiedMap (View (..))
import Control.Monad.Trans.Reader (asks)
import Control.SetAlgebra (dom, eval, range, singleton, (∈), (∉), (∪), (⨃))
import Control.State.Transition
import Data.Foldable (fold)
import Data.Group (Group (..))
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
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 DELEG era

data DelegEnv era = DelegEnv
  { DelegEnv era -> SlotNo
slotNo :: SlotNo,
    DelegEnv era -> Ptr
ptr_ :: Ptr,
    DelegEnv era -> AccountState
acnt_ :: AccountState,
    DelegEnv era -> PParams era
ppDE :: Core.PParams era -- The protocol parameters are only used for the HardFork mechanism
  }

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

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

data DelegPredicateFailure era
  = StakeKeyAlreadyRegisteredDELEG
      !(Credential 'Staking (Crypto 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 (Crypto era)) -- DEPRECATED, now redundant with StakeKeyAlreadyRegisteredDELEG
  | StakeKeyNotRegisteredDELEG
      !(Credential 'Staking (Crypto era)) -- Credential which is not registered
  | StakeKeyNonZeroAccountBalanceDELEG
      !(Maybe Coin) -- The remaining reward account balance, if it exists
  | StakeDelegationImpossibleDELEG
      !(Credential 'Staking (Crypto era)) -- Credential that is not registered
  | WrongCertificateTypeDELEG -- The DCertPool constructor should not be used by this transition
  | GenesisKeyNotInMappingDELEG
      !(KeyHash 'Genesis (Crypto era)) -- Unknown Genesis KeyHash
  | DuplicateGenesisDelegateDELEG
      !(KeyHash 'GenesisDelegate (Crypto era)) -- Keyhash which is already delegated to
  | InsufficientForInstantaneousRewardsDELEG
      !MIRPot -- which pot the rewards are to be drawn from, treasury or reserves
      !Coin -- amount of rewards to be given out
      !Coin -- size of the pot from which the lovelace is drawn
  | MIRCertificateTooLateinEpochDELEG
      !SlotNo -- current slot
      !SlotNo -- Core.EraRule "MIR" must be submitted before this slot
  | DuplicateGenesisVRFDELEG
      !(Hash (Crypto era) (VerKeyVRF (Crypto era))) -- VRF KeyHash which is already delegated to
  | MIRTransferNotCurrentlyAllowed
  | MIRNegativesNotCurrentlyAllowed
  | InsufficientForTransferDELEG
      !MIRPot -- which pot the rewards are to be drawn from, treasury or reserves
      !Coin -- amount attempted to transfer
      !Coin -- amount available
  | MIRProducesNegativeUpdate
  | MIRNegativeTransfer
      !MIRPot -- which pot the rewards are to be drawn from, treasury or reserves
      !Coin -- amount attempted to transfer
  deriving (Int -> DelegPredicateFailure era -> ShowS
[DelegPredicateFailure era] -> ShowS
DelegPredicateFailure era -> String
(Int -> DelegPredicateFailure era -> ShowS)
-> (DelegPredicateFailure era -> String)
-> ([DelegPredicateFailure era] -> ShowS)
-> Show (DelegPredicateFailure era)
forall era. Int -> DelegPredicateFailure era -> ShowS
forall era. [DelegPredicateFailure era] -> ShowS
forall era. DelegPredicateFailure era -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DelegPredicateFailure era] -> ShowS
$cshowList :: forall era. [DelegPredicateFailure era] -> ShowS
show :: DelegPredicateFailure era -> String
$cshow :: forall era. DelegPredicateFailure era -> String
showsPrec :: Int -> DelegPredicateFailure era -> ShowS
$cshowsPrec :: forall era. Int -> DelegPredicateFailure era -> ShowS
Show, DelegPredicateFailure era -> DelegPredicateFailure era -> Bool
(DelegPredicateFailure era -> DelegPredicateFailure era -> Bool)
-> (DelegPredicateFailure era -> DelegPredicateFailure era -> Bool)
-> Eq (DelegPredicateFailure era)
forall era.
DelegPredicateFailure era -> DelegPredicateFailure era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DelegPredicateFailure era -> DelegPredicateFailure era -> Bool
$c/= :: forall era.
DelegPredicateFailure era -> DelegPredicateFailure era -> Bool
== :: DelegPredicateFailure era -> DelegPredicateFailure era -> Bool
$c== :: forall era.
DelegPredicateFailure era -> DelegPredicateFailure era -> Bool
Eq, (forall x.
 DelegPredicateFailure era -> Rep (DelegPredicateFailure era) x)
-> (forall x.
    Rep (DelegPredicateFailure era) x -> DelegPredicateFailure era)
-> Generic (DelegPredicateFailure era)
forall x.
Rep (DelegPredicateFailure era) x -> DelegPredicateFailure era
forall x.
DelegPredicateFailure era -> Rep (DelegPredicateFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (DelegPredicateFailure era) x -> DelegPredicateFailure era
forall era x.
DelegPredicateFailure era -> Rep (DelegPredicateFailure era) x
$cto :: forall era x.
Rep (DelegPredicateFailure era) x -> DelegPredicateFailure era
$cfrom :: forall era x.
DelegPredicateFailure era -> Rep (DelegPredicateFailure era) x
Generic)

newtype DelegEvent era = NewEpoch EpochNo

instance
  ( Typeable era,
    HasField "_protocolVersion" (Core.PParams era) ProtVer
  ) =>
  STS (DELEG era)
  where
  type State (DELEG era) = DState (Crypto era)
  type Signal (DELEG era) = DCert (Crypto era)
  type Environment (DELEG era) = DelegEnv era
  type BaseM (DELEG era) = ShelleyBase
  type PredicateFailure (DELEG era) = DelegPredicateFailure era
  type Event (DELEG era) = DelegEvent era

  transitionRules :: [TransitionRule (DELEG era)]
transitionRules = [TransitionRule (DELEG era)
forall era.
(Typeable era,
 HasField "_protocolVersion" (PParams era) ProtVer) =>
TransitionRule (DELEG era)
delegationTransition]

instance NoThunks (DelegPredicateFailure era)

instance
  (Typeable era, Era era, Typeable (Core.Script era)) =>
  ToCBOR (DelegPredicateFailure era)
  where
  toCBOR :: DelegPredicateFailure era -> Encoding
toCBOR = \case
    StakeKeyAlreadyRegisteredDELEG Credential 'Staking (Crypto era)
cred ->
      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
<> Credential 'Staking (Crypto era) -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Credential 'Staking (Crypto era)
cred
    StakeKeyNotRegisteredDELEG Credential 'Staking (Crypto era)
cred ->
      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
<> Credential 'Staking (Crypto era) -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Credential 'Staking (Crypto era)
cred
    StakeKeyNonZeroAccountBalanceDELEG Maybe Coin
rewardBalance ->
      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
<> Maybe Coin -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Maybe Coin
rewardBalance
    StakeDelegationImpossibleDELEG Credential 'Staking (Crypto era)
cred ->
      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
3 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Credential 'Staking (Crypto era) -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Credential 'Staking (Crypto era)
cred
    DelegPredicateFailure era
WrongCertificateTypeDELEG ->
      Word -> Encoding
encodeListLen Word
1 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
4 :: Word8)
    GenesisKeyNotInMappingDELEG KeyHash 'Genesis (Crypto era)
gkh ->
      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
5 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> KeyHash 'Genesis (Crypto era) -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR KeyHash 'Genesis (Crypto era)
gkh
    DuplicateGenesisDelegateDELEG KeyHash 'GenesisDelegate (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
6 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> KeyHash 'GenesisDelegate (Crypto era) -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR KeyHash 'GenesisDelegate (Crypto era)
kh
    InsufficientForInstantaneousRewardsDELEG MIRPot
pot Coin
needed Coin
potAmount ->
      Word -> Encoding
encodeListLen Word
4 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
7 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> MIRPot -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR MIRPot
pot
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Coin -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Coin
needed
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Coin -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Coin
potAmount
    MIRCertificateTooLateinEpochDELEG SlotNo
sNow SlotNo
sTooLate ->
      Word -> Encoding
encodeListLen Word
3 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
8 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> SlotNo -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR SlotNo
sNow Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> SlotNo -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR SlotNo
sTooLate
    DuplicateGenesisVRFDELEG Hash (Crypto era) (VerKeyVRF (Crypto era))
vrf ->
      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
9 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Hash (Crypto era) (VerKeyVRF (Crypto era)) -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Hash (Crypto era) (VerKeyVRF (Crypto era))
vrf
    StakeKeyInRewardsDELEG Credential 'Staking (Crypto era)
cred ->
      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
10 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Credential 'Staking (Crypto era) -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Credential 'Staking (Crypto era)
cred
    DelegPredicateFailure era
MIRTransferNotCurrentlyAllowed ->
      Word -> Encoding
encodeListLen Word
1 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
11 :: Word8)
    DelegPredicateFailure era
MIRNegativesNotCurrentlyAllowed ->
      Word -> Encoding
encodeListLen Word
1 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
12 :: Word8)
    InsufficientForTransferDELEG MIRPot
pot Coin
needed Coin
available ->
      Word -> Encoding
encodeListLen Word
4 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
13 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> MIRPot -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR MIRPot
pot
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Coin -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Coin
needed
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Coin -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Coin
available
    DelegPredicateFailure era
MIRProducesNegativeUpdate ->
      Word -> Encoding
encodeListLen Word
1 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
14 :: Word8)
    MIRNegativeTransfer MIRPot
pot Coin
amt ->
      Word -> Encoding
encodeListLen Word
3 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR (Word8
15 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> MIRPot -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR MIRPot
pot
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Coin -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Coin
amt

instance
  (Era era, Typeable (Core.Script era)) =>
  FromCBOR (DelegPredicateFailure era)
  where
  fromCBOR :: Decoder s (DelegPredicateFailure era)
fromCBOR = String
-> (Word -> Decoder s (Int, DelegPredicateFailure era))
-> Decoder s (DelegPredicateFailure era)
forall s a. String -> (Word -> Decoder s (Int, a)) -> Decoder s a
decodeRecordSum String
"PredicateFailure (DELEG era)" ((Word -> Decoder s (Int, DelegPredicateFailure era))
 -> Decoder s (DelegPredicateFailure era))
-> (Word -> Decoder s (Int, DelegPredicateFailure era))
-> Decoder s (DelegPredicateFailure era)
forall a b. (a -> b) -> a -> b
$
    \case
      Word
0 -> do
        Credential 'Staking (Crypto era)
kh <- Decoder s (Credential 'Staking (Crypto era))
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, DelegPredicateFailure era)
-> Decoder s (Int, DelegPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, Credential 'Staking (Crypto era) -> DelegPredicateFailure era
forall era.
Credential 'Staking (Crypto era) -> DelegPredicateFailure era
StakeKeyAlreadyRegisteredDELEG Credential 'Staking (Crypto era)
kh)
      Word
1 -> do
        Credential 'Staking (Crypto era)
kh <- Decoder s (Credential 'Staking (Crypto era))
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, DelegPredicateFailure era)
-> Decoder s (Int, DelegPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, Credential 'Staking (Crypto era) -> DelegPredicateFailure era
forall era.
Credential 'Staking (Crypto era) -> DelegPredicateFailure era
StakeKeyNotRegisteredDELEG Credential 'Staking (Crypto era)
kh)
      Word
2 -> do
        Maybe Coin
b <- Decoder s (Maybe Coin)
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, DelegPredicateFailure era)
-> Decoder s (Int, DelegPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, Maybe Coin -> DelegPredicateFailure era
forall era. Maybe Coin -> DelegPredicateFailure era
StakeKeyNonZeroAccountBalanceDELEG Maybe Coin
b)
      Word
3 -> do
        Credential 'Staking (Crypto era)
kh <- Decoder s (Credential 'Staking (Crypto era))
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, DelegPredicateFailure era)
-> Decoder s (Int, DelegPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, Credential 'Staking (Crypto era) -> DelegPredicateFailure era
forall era.
Credential 'Staking (Crypto era) -> DelegPredicateFailure era
StakeDelegationImpossibleDELEG Credential 'Staking (Crypto era)
kh)
      Word
4 -> do
        (Int, DelegPredicateFailure era)
-> Decoder s (Int, DelegPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
1, DelegPredicateFailure era
forall era. DelegPredicateFailure era
WrongCertificateTypeDELEG)
      Word
5 -> do
        KeyHash 'Genesis (Crypto era)
gkh <- Decoder s (KeyHash 'Genesis (Crypto era))
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, DelegPredicateFailure era)
-> Decoder s (Int, DelegPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, KeyHash 'Genesis (Crypto era) -> DelegPredicateFailure era
forall era.
KeyHash 'Genesis (Crypto era) -> DelegPredicateFailure era
GenesisKeyNotInMappingDELEG KeyHash 'Genesis (Crypto era)
gkh)
      Word
6 -> do
        KeyHash 'GenesisDelegate (Crypto era)
kh <- Decoder s (KeyHash 'GenesisDelegate (Crypto era))
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, DelegPredicateFailure era)
-> Decoder s (Int, DelegPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, KeyHash 'GenesisDelegate (Crypto era) -> DelegPredicateFailure era
forall era.
KeyHash 'GenesisDelegate (Crypto era) -> DelegPredicateFailure era
DuplicateGenesisDelegateDELEG KeyHash 'GenesisDelegate (Crypto era)
kh)
      Word
7 -> do
        MIRPot
pot <- Decoder s MIRPot
forall a s. FromCBOR a => Decoder s a
fromCBOR
        Coin
needed <- Decoder s Coin
forall a s. FromCBOR a => Decoder s a
fromCBOR
        Coin
potAmount <- Decoder s Coin
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, DelegPredicateFailure era)
-> Decoder s (Int, DelegPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
4, MIRPot -> Coin -> Coin -> DelegPredicateFailure era
forall era. MIRPot -> Coin -> Coin -> DelegPredicateFailure era
InsufficientForInstantaneousRewardsDELEG MIRPot
pot Coin
needed Coin
potAmount)
      Word
8 -> do
        SlotNo
sNow <- Decoder s SlotNo
forall a s. FromCBOR a => Decoder s a
fromCBOR
        SlotNo
sTooLate <- Decoder s SlotNo
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, DelegPredicateFailure era)
-> Decoder s (Int, DelegPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, SlotNo -> SlotNo -> DelegPredicateFailure era
forall era. SlotNo -> SlotNo -> DelegPredicateFailure era
MIRCertificateTooLateinEpochDELEG SlotNo
sNow SlotNo
sTooLate)
      Word
9 -> do
        Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era)))
vrf <- Decoder s (Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era))))
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, DelegPredicateFailure era)
-> Decoder s (Int, DelegPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era)))
-> DelegPredicateFailure era
forall era.
Hash (Crypto era) (VerKeyVRF (Crypto era))
-> DelegPredicateFailure era
DuplicateGenesisVRFDELEG Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era)))
vrf)
      Word
10 -> do
        Credential 'Staking (Crypto era)
kh <- Decoder s (Credential 'Staking (Crypto era))
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, DelegPredicateFailure era)
-> Decoder s (Int, DelegPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, Credential 'Staking (Crypto era) -> DelegPredicateFailure era
forall era.
Credential 'Staking (Crypto era) -> DelegPredicateFailure era
StakeKeyInRewardsDELEG Credential 'Staking (Crypto era)
kh)
      Word
11 -> do
        (Int, DelegPredicateFailure era)
-> Decoder s (Int, DelegPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
1, DelegPredicateFailure era
forall era. DelegPredicateFailure era
MIRTransferNotCurrentlyAllowed)
      Word
12 -> do
        (Int, DelegPredicateFailure era)
-> Decoder s (Int, DelegPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
1, DelegPredicateFailure era
forall era. DelegPredicateFailure era
MIRNegativesNotCurrentlyAllowed)
      Word
13 -> do
        MIRPot
pot <- Decoder s MIRPot
forall a s. FromCBOR a => Decoder s a
fromCBOR
        Coin
needed <- Decoder s Coin
forall a s. FromCBOR a => Decoder s a
fromCBOR
        Coin
available <- Decoder s Coin
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, DelegPredicateFailure era)
-> Decoder s (Int, DelegPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
4, MIRPot -> Coin -> Coin -> DelegPredicateFailure era
forall era. MIRPot -> Coin -> Coin -> DelegPredicateFailure era
InsufficientForTransferDELEG MIRPot
pot Coin
needed Coin
available)
      Word
14 -> do
        (Int, DelegPredicateFailure era)
-> Decoder s (Int, DelegPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
1, DelegPredicateFailure era
forall era. DelegPredicateFailure era
MIRProducesNegativeUpdate)
      Word
15 -> do
        MIRPot
pot <- Decoder s MIRPot
forall a s. FromCBOR a => Decoder s a
fromCBOR
        Coin
amt <- Decoder s Coin
forall a s. FromCBOR a => Decoder s a
fromCBOR
        (Int, DelegPredicateFailure era)
-> Decoder s (Int, DelegPredicateFailure era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, MIRPot -> Coin -> DelegPredicateFailure era
forall era. MIRPot -> Coin -> DelegPredicateFailure era
MIRNegativeTransfer MIRPot
pot Coin
amt)
      Word
k -> Word -> Decoder s (Int, DelegPredicateFailure era)
forall s a. Word -> Decoder s a
invalidKey Word
k

delegationTransition ::
  ( Typeable era,
    HasField "_protocolVersion" (Core.PParams era) ProtVer
  ) =>
  TransitionRule (DELEG era)
delegationTransition :: TransitionRule (DELEG era)
delegationTransition = do
  TRC (DelegEnv slot ptr acnt pp, State (DELEG era)
ds, Signal (DELEG era)
c) <- F (Clause (DELEG era) 'Transition) (TRC (DELEG era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  case Signal (DELEG era)
c of
    DCertDeleg (RegKey hk) -> do
      Exp Bool -> Bool
forall s t. Embed s t => Exp t -> s
eval (StakeCredential (Crypto era)
hk StakeCredential (Crypto era)
-> Exp (Sett (StakeCredential (Crypto era)) ()) -> Exp Bool
forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∉ ViewMap (Crypto era) (StakeCredential (Crypto era)) Coin
-> Exp (Sett (StakeCredential (Crypto era)) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom (DState (Crypto era)
-> ViewMap (Crypto era) (StakeCredential (Crypto era)) Coin
forall crypto.
DState crypto -> ViewMap crypto (Credential 'Staking crypto) Coin
rewards State (DELEG era)
DState (Crypto era)
ds)) Bool
-> PredicateFailure (DELEG era) -> Rule (DELEG era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! StakeCredential (Crypto era) -> DelegPredicateFailure era
forall era.
Credential 'Staking (Crypto era) -> DelegPredicateFailure era
StakeKeyAlreadyRegisteredDELEG StakeCredential (Crypto era)
hk
      DState (Crypto era)
-> F (Clause (DELEG era) 'Transition) (DState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DState (Crypto era)
 -> F (Clause (DELEG era) 'Transition) (DState (Crypto era)))
-> DState (Crypto era)
-> F (Clause (DELEG era) 'Transition) (DState (Crypto era))
forall a b. (a -> b) -> a -> b
$
        ( let u1 :: UnifiedMap (Crypto era)
u1 = DState (Crypto era) -> UnifiedMap (Crypto era)
forall crypto. DState crypto -> UnifiedMap crypto
_unified State (DELEG era)
DState (Crypto era)
ds
              u2 :: UnifiedMap (Crypto era)
u2 = (UnifiedMap (Crypto era)
-> ViewMap (Crypto era) (StakeCredential (Crypto era)) Coin
forall coin cr pl ptr.
UMap coin cr pl ptr -> View coin cr pl ptr cr coin
Rewards UnifiedMap (Crypto era)
u1 ViewMap (Crypto era) (StakeCredential (Crypto era)) Coin
-> (StakeCredential (Crypto era), Coin) -> UnifiedMap (Crypto era)
forall cr coin ptr pool k v.
(Ord cr, Monoid coin, Ord ptr) =>
View coin cr pool ptr k v -> (k, v) -> UMap coin cr pool ptr
UM.∪ (StakeCredential (Crypto era)
hk, Coin
forall a. Monoid a => a
mempty))
              u3 :: UnifiedMap (Crypto era)
u3 = (UnifiedMap (Crypto era)
-> View
     Coin
     (StakeCredential (Crypto era))
     (KeyHash 'StakePool (Crypto era))
     Ptr
     Ptr
     (StakeCredential (Crypto era))
forall coin cr pl ptr.
UMap coin cr pl ptr -> View coin cr pl ptr ptr cr
Ptrs UnifiedMap (Crypto era)
u2 View
  Coin
  (StakeCredential (Crypto era))
  (KeyHash 'StakePool (Crypto era))
  Ptr
  Ptr
  (StakeCredential (Crypto era))
-> (Ptr, StakeCredential (Crypto era)) -> UnifiedMap (Crypto era)
forall cr coin ptr pool k v.
(Ord cr, Monoid coin, Ord ptr) =>
View coin cr pool ptr k v -> (k, v) -> UMap coin cr pool ptr
UM.∪ (Ptr
ptr, StakeCredential (Crypto era)
hk))
           in State (DELEG era)
DState (Crypto era)
ds {_unified :: UnifiedMap (Crypto era)
_unified = UnifiedMap (Crypto era)
u3}
        )
    DCertDeleg (DeRegKey hk) -> do
      -- note that pattern match is used instead of cwitness, as in the spec
      Exp Bool -> Bool
forall s t. Embed s t => Exp t -> s
eval (StakeCredential (Crypto era)
hk StakeCredential (Crypto era)
-> Exp (Sett (StakeCredential (Crypto era)) ()) -> Exp Bool
forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∈ ViewMap (Crypto era) (StakeCredential (Crypto era)) Coin
-> Exp (Sett (StakeCredential (Crypto era)) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom (DState (Crypto era)
-> ViewMap (Crypto era) (StakeCredential (Crypto era)) Coin
forall crypto.
DState crypto -> ViewMap crypto (Credential 'Staking crypto) Coin
rewards State (DELEG era)
DState (Crypto era)
ds)) Bool
-> PredicateFailure (DELEG era) -> Rule (DELEG era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! StakeCredential (Crypto era) -> DelegPredicateFailure era
forall era.
Credential 'Staking (Crypto era) -> DelegPredicateFailure era
StakeKeyNotRegisteredDELEG StakeCredential (Crypto era)
hk
      let rewardCoin :: Maybe Coin
rewardCoin = StakeCredential (Crypto era)
-> ViewMap (Crypto era) (StakeCredential (Crypto era)) Coin
-> Maybe Coin
forall cr ptr k coin pool v.
(Ord cr, Ord ptr) =>
k -> View coin cr pool ptr k v -> Maybe v
UM.lookup StakeCredential (Crypto era)
hk (DState (Crypto era)
-> ViewMap (Crypto era) (StakeCredential (Crypto era)) Coin
forall crypto.
DState crypto -> ViewMap crypto (Credential 'Staking crypto) Coin
rewards State (DELEG era)
DState (Crypto era)
ds)
      Maybe Coin
rewardCoin Maybe Coin -> Maybe Coin -> Bool
forall a. Eq a => a -> a -> Bool
== Coin -> Maybe Coin
forall a. a -> Maybe a
Just Coin
forall a. Monoid a => a
mempty Bool
-> PredicateFailure (DELEG era) -> Rule (DELEG era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Maybe Coin -> DelegPredicateFailure era
forall era. Maybe Coin -> DelegPredicateFailure era
StakeKeyNonZeroAccountBalanceDELEG Maybe Coin
rewardCoin

      DState (Crypto era)
-> F (Clause (DELEG era) 'Transition) (DState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DState (Crypto era)
 -> F (Clause (DELEG era) 'Transition) (DState (Crypto era)))
-> DState (Crypto era)
-> F (Clause (DELEG era) 'Transition) (DState (Crypto era))
forall a b. (a -> b) -> a -> b
$
        let u0 :: UnifiedMap (Crypto era)
u0 = DState (Crypto era) -> UnifiedMap (Crypto era)
forall crypto. DState crypto -> UnifiedMap crypto
_unified State (DELEG era)
DState (Crypto era)
ds
            u1 :: UnifiedMap (Crypto era)
u1 = (StakeCredential (Crypto era) -> Set (StakeCredential (Crypto era))
forall a. a -> Set a
Set.singleton StakeCredential (Crypto era)
hk Set (StakeCredential (Crypto era))
-> ViewMap (Crypto era) (StakeCredential (Crypto era)) Coin
-> UnifiedMap (Crypto era)
forall cred ptr k coin pool v.
(Ord cred, Ord ptr) =>
Set k -> View coin cred pool ptr k v -> UMap coin cred pool ptr
UM.⋪ UnifiedMap (Crypto era)
-> ViewMap (Crypto era) (StakeCredential (Crypto era)) Coin
forall coin cr pl ptr.
UMap coin cr pl ptr -> View coin cr pl ptr cr coin
Rewards UnifiedMap (Crypto era)
u0)
            u2 :: UnifiedMap (Crypto era)
u2 = (StakeCredential (Crypto era) -> Set (StakeCredential (Crypto era))
forall a. a -> Set a
Set.singleton StakeCredential (Crypto era)
hk Set (StakeCredential (Crypto era))
-> View
     Coin
     (StakeCredential (Crypto era))
     (KeyHash 'StakePool (Crypto era))
     Ptr
     (StakeCredential (Crypto era))
     (KeyHash 'StakePool (Crypto era))
-> UnifiedMap (Crypto era)
forall cred ptr k coin pool v.
(Ord cred, Ord ptr) =>
Set k -> View coin cred pool ptr k v -> UMap coin cred pool ptr
UM.⋪ UnifiedMap (Crypto era)
-> View
     Coin
     (StakeCredential (Crypto era))
     (KeyHash 'StakePool (Crypto era))
     Ptr
     (StakeCredential (Crypto era))
     (KeyHash 'StakePool (Crypto era))
forall coin cr pl ptr.
UMap coin cr pl ptr -> View coin cr pl ptr cr pl
Delegations UnifiedMap (Crypto era)
u1)
            u3 :: UnifiedMap (Crypto era)
u3 = (UnifiedMap (Crypto era)
-> View
     Coin
     (StakeCredential (Crypto era))
     (KeyHash 'StakePool (Crypto era))
     Ptr
     Ptr
     (StakeCredential (Crypto era))
forall coin cr pl ptr.
UMap coin cr pl ptr -> View coin cr pl ptr ptr cr
Ptrs UnifiedMap (Crypto era)
u2 View
  Coin
  (StakeCredential (Crypto era))
  (KeyHash 'StakePool (Crypto era))
  Ptr
  Ptr
  (StakeCredential (Crypto era))
-> Set (StakeCredential (Crypto era)) -> UnifiedMap (Crypto era)
forall cred ptr coin pool k v.
(Ord cred, Ord ptr, Ord coin, Ord pool) =>
View coin cred pool ptr k v -> Set v -> UMap coin cred pool ptr
UM.⋫ StakeCredential (Crypto era) -> Set (StakeCredential (Crypto era))
forall a. a -> Set a
Set.singleton StakeCredential (Crypto era)
hk)
         in State (DELEG era)
DState (Crypto era)
ds {_unified :: UnifiedMap (Crypto era)
_unified = UnifiedMap (Crypto era)
u3}
    DCertDeleg (Delegate (Delegation hk dpool)) -> do
      -- note that pattern match is used instead of cwitness and dpool, as in the spec
      Exp Bool -> Bool
forall s t. Embed s t => Exp t -> s
eval (StakeCredential (Crypto era)
hk StakeCredential (Crypto era)
-> Exp (Sett (StakeCredential (Crypto era)) ()) -> Exp Bool
forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∈ ViewMap (Crypto era) (StakeCredential (Crypto era)) Coin
-> Exp (Sett (StakeCredential (Crypto era)) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom (DState (Crypto era)
-> ViewMap (Crypto era) (StakeCredential (Crypto era)) Coin
forall crypto.
DState crypto -> ViewMap crypto (Credential 'Staking crypto) Coin
rewards State (DELEG era)
DState (Crypto era)
ds)) Bool
-> PredicateFailure (DELEG era) -> Rule (DELEG era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! StakeCredential (Crypto era) -> DelegPredicateFailure era
forall era.
Credential 'Staking (Crypto era) -> DelegPredicateFailure era
StakeDelegationImpossibleDELEG StakeCredential (Crypto era)
hk

      DState (Crypto era)
-> F (Clause (DELEG era) 'Transition) (DState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (State (DELEG era)
DState (Crypto era)
ds {_unified :: UnifiedMap (Crypto era)
_unified = (DState (Crypto era)
-> View
     Coin
     (StakeCredential (Crypto era))
     (KeyHash 'StakePool (Crypto era))
     Ptr
     (StakeCredential (Crypto era))
     (KeyHash 'StakePool (Crypto era))
forall crypto.
DState crypto
-> ViewMap
     crypto (Credential 'Staking crypto) (KeyHash 'StakePool crypto)
delegations State (DELEG era)
DState (Crypto era)
ds View
  Coin
  (StakeCredential (Crypto era))
  (KeyHash 'StakePool (Crypto era))
  Ptr
  (StakeCredential (Crypto era))
  (KeyHash 'StakePool (Crypto era))
-> Map
     (StakeCredential (Crypto era)) (KeyHash 'StakePool (Crypto era))
-> UnifiedMap (Crypto era)
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.⨃ (StakeCredential (Crypto era)
-> KeyHash 'StakePool (Crypto era)
-> Map
     (StakeCredential (Crypto era)) (KeyHash 'StakePool (Crypto era))
forall k a. k -> a -> Map k a
Map.singleton StakeCredential (Crypto era)
hk KeyHash 'StakePool (Crypto era)
dpool))})
    DCertGenesis (GenesisDelegCert gkh vkh vrf) -> do
      Word64
sp <- BaseM (DELEG era) Word64 -> Rule (DELEG era) 'Transition Word64
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (DELEG era) Word64 -> Rule (DELEG era) 'Transition Word64)
-> BaseM (DELEG era) Word64 -> Rule (DELEG era) 'Transition Word64
forall a b. (a -> b) -> a -> b
$ (Globals -> Word64) -> ReaderT Globals Identity Word64
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 (Crypto era)) (GenDelegPair (Crypto era))
genDelegs) = DState (Crypto era) -> GenDelegs (Crypto era)
forall crypto. DState crypto -> GenDelegs crypto
_genDelegs State (DELEG era)
DState (Crypto era)
ds

      -- gkh ∈ dom genDelegs ?! GenesisKeyNotInMappingDELEG gkh
      (case KeyHash 'Genesis (Crypto era)
-> Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
-> Maybe (GenDelegPair (Crypto era))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KeyHash 'Genesis (Crypto era)
gkh Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
genDelegs of Just GenDelegPair (Crypto era)
_ -> Bool
True; Maybe (GenDelegPair (Crypto era))
Nothing -> Bool
False) Bool
-> PredicateFailure (DELEG era) -> Rule (DELEG era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! KeyHash 'Genesis (Crypto era) -> DelegPredicateFailure era
forall era.
KeyHash 'Genesis (Crypto era) -> DelegPredicateFailure era
GenesisKeyNotInMappingDELEG KeyHash 'Genesis (Crypto era)
gkh

      let cod :: Set (GenDelegPair (Crypto era))
cod =
            Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
-> Set (GenDelegPair (Crypto era))
forall (f :: * -> * -> *) v k. (Basic f, Ord v) => f k v -> Set v
range (Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
 -> Set (GenDelegPair (Crypto era)))
-> Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
-> Set (GenDelegPair (Crypto era))
forall a b. (a -> b) -> a -> b
$
              (KeyHash 'Genesis (Crypto era)
 -> GenDelegPair (Crypto era) -> Bool)
-> Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
-> Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\KeyHash 'Genesis (Crypto era)
g GenDelegPair (Crypto era)
_ -> KeyHash 'Genesis (Crypto era)
g KeyHash 'Genesis (Crypto era)
-> KeyHash 'Genesis (Crypto era) -> Bool
forall a. Eq a => a -> a -> Bool
/= KeyHash 'Genesis (Crypto era)
gkh) Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
genDelegs
          fod :: Set (GenDelegPair (Crypto era))
fod =
            Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
-> Set (GenDelegPair (Crypto era))
forall (f :: * -> * -> *) v k. (Basic f, Ord v) => f k v -> Set v
range (Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
 -> Set (GenDelegPair (Crypto era)))
-> Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
-> Set (GenDelegPair (Crypto era))
forall a b. (a -> b) -> a -> b
$
              (FutureGenDeleg (Crypto era) -> GenDelegPair (Crypto era) -> Bool)
-> Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
-> Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\(FutureGenDeleg SlotNo
_ KeyHash 'Genesis (Crypto era)
g) GenDelegPair (Crypto era)
_ -> KeyHash 'Genesis (Crypto era)
g KeyHash 'Genesis (Crypto era)
-> KeyHash 'Genesis (Crypto era) -> Bool
forall a. Eq a => a -> a -> Bool
/= KeyHash 'Genesis (Crypto era)
gkh) (DState (Crypto era)
-> Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
forall crypto.
DState crypto -> Map (FutureGenDeleg crypto) (GenDelegPair crypto)
_fGenDelegs State (DELEG era)
DState (Crypto era)
ds)
          currentOtherColdKeyHashes :: Set (KeyHash 'GenesisDelegate (Crypto era))
currentOtherColdKeyHashes = (GenDelegPair (Crypto era)
 -> KeyHash 'GenesisDelegate (Crypto era))
-> Set (GenDelegPair (Crypto era))
-> Set (KeyHash 'GenesisDelegate (Crypto era))
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map GenDelegPair (Crypto era) -> KeyHash 'GenesisDelegate (Crypto era)
forall crypto.
GenDelegPair crypto -> KeyHash 'GenesisDelegate crypto
genDelegKeyHash Set (GenDelegPair (Crypto era))
cod
          currentOtherVrfKeyHashes :: Set (Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era))))
currentOtherVrfKeyHashes = (GenDelegPair (Crypto era)
 -> Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era))))
-> Set (GenDelegPair (Crypto era))
-> Set (Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era))))
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map GenDelegPair (Crypto era)
-> Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era)))
forall crypto.
GenDelegPair crypto -> Hash crypto (VerKeyVRF crypto)
genDelegVrfHash Set (GenDelegPair (Crypto era))
cod
          futureOtherColdKeyHashes :: Set (KeyHash 'GenesisDelegate (Crypto era))
futureOtherColdKeyHashes = (GenDelegPair (Crypto era)
 -> KeyHash 'GenesisDelegate (Crypto era))
-> Set (GenDelegPair (Crypto era))
-> Set (KeyHash 'GenesisDelegate (Crypto era))
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map GenDelegPair (Crypto era) -> KeyHash 'GenesisDelegate (Crypto era)
forall crypto.
GenDelegPair crypto -> KeyHash 'GenesisDelegate crypto
genDelegKeyHash Set (GenDelegPair (Crypto era))
fod
          futureOtherVrfKeyHashes :: Set (Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era))))
futureOtherVrfKeyHashes = (GenDelegPair (Crypto era)
 -> Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era))))
-> Set (GenDelegPair (Crypto era))
-> Set (Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era))))
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map GenDelegPair (Crypto era)
-> Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era)))
forall crypto.
GenDelegPair crypto -> Hash crypto (VerKeyVRF crypto)
genDelegVrfHash Set (GenDelegPair (Crypto era))
fod

      Exp Bool -> Bool
forall s t. Embed s t => Exp t -> s
eval (KeyHash 'GenesisDelegate (Crypto era)
vkh KeyHash 'GenesisDelegate (Crypto era)
-> Exp (Sett (KeyHash 'GenesisDelegate (Crypto era)) ())
-> Exp Bool
forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∉ (Set (KeyHash 'GenesisDelegate (Crypto era))
currentOtherColdKeyHashes Set (KeyHash 'GenesisDelegate (Crypto era))
-> Set (KeyHash 'GenesisDelegate (Crypto era))
-> Exp (Sett (KeyHash 'GenesisDelegate (Crypto era)) ())
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 (Crypto era))
futureOtherColdKeyHashes))
        Bool
-> PredicateFailure (DELEG era) -> Rule (DELEG era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! KeyHash 'GenesisDelegate (Crypto era) -> DelegPredicateFailure era
forall era.
KeyHash 'GenesisDelegate (Crypto era) -> DelegPredicateFailure era
DuplicateGenesisDelegateDELEG KeyHash 'GenesisDelegate (Crypto era)
vkh
      Exp Bool -> Bool
forall s t. Embed s t => Exp t -> s
eval (Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era)))
vrf Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era)))
-> Exp
     (Sett (Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era)))) ())
-> Exp Bool
forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∉ (Set (Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era))))
currentOtherVrfKeyHashes Set (Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era))))
-> Set (Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era))))
-> Exp
     (Sett (Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era)))) ())
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 (Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era))))
futureOtherVrfKeyHashes))
        Bool
-> PredicateFailure (DELEG era) -> Rule (DELEG era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era)))
-> DelegPredicateFailure era
forall era.
Hash (Crypto era) (VerKeyVRF (Crypto era))
-> DelegPredicateFailure era
DuplicateGenesisVRFDELEG Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era)))
vrf

      DState (Crypto era)
-> F (Clause (DELEG era) 'Transition) (DState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DState (Crypto era)
 -> F (Clause (DELEG era) 'Transition) (DState (Crypto era)))
-> DState (Crypto era)
-> F (Clause (DELEG era) 'Transition) (DState (Crypto era))
forall a b. (a -> b) -> a -> b
$
        State (DELEG era)
DState (Crypto era)
ds
          { _fGenDelegs :: Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
_fGenDelegs = Exp (Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era)))
-> Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
forall s t. Embed s t => Exp t -> s
eval (DState (Crypto era)
-> Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
forall crypto.
DState crypto -> Map (FutureGenDeleg crypto) (GenDelegPair crypto)
_fGenDelegs State (DELEG era)
DState (Crypto era)
ds Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
-> Exp
     (Single (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era)))
-> Exp
     (Map (FutureGenDeleg (Crypto era)) (GenDelegPair (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)
⨃ FutureGenDeleg (Crypto era)
-> GenDelegPair (Crypto era)
-> Exp
     (Single (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era)))
forall k v. Ord k => k -> v -> Exp (Single k v)
singleton (SlotNo
-> KeyHash 'Genesis (Crypto era) -> FutureGenDeleg (Crypto era)
forall crypto.
SlotNo -> KeyHash 'Genesis crypto -> FutureGenDeleg crypto
FutureGenDeleg SlotNo
s' KeyHash 'Genesis (Crypto era)
gkh) (KeyHash 'GenesisDelegate (Crypto era)
-> Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era)))
-> GenDelegPair (Crypto era)
forall crypto.
KeyHash 'GenesisDelegate crypto
-> Hash crypto (VerKeyVRF crypto) -> GenDelegPair crypto
GenDelegPair KeyHash 'GenesisDelegate (Crypto era)
vkh Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era)))
vrf))
          }
    DCertMir (MIRCert targetPot (StakeAddressesMIR credCoinMap)) -> do
      if PParams era -> Bool
forall pp. HasField "_protocolVersion" pp ProtVer => pp -> Bool
HardForks.allowMIRTransfer PParams era
pp
        then do
          Word64
sp <- BaseM (DELEG era) Word64 -> Rule (DELEG era) 'Transition Word64
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (DELEG era) Word64 -> Rule (DELEG era) 'Transition Word64)
-> BaseM (DELEG era) Word64 -> Rule (DELEG era) 'Transition Word64
forall a b. (a -> b) -> a -> b
$ (Globals -> Word64) -> ReaderT Globals Identity Word64
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> Word64
stabilityWindow
          EpochInfo Identity
ei <- BaseM (DELEG era) (EpochInfo Identity)
-> Rule (DELEG era) 'Transition (EpochInfo Identity)
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (DELEG era) (EpochInfo Identity)
 -> Rule (DELEG era) 'Transition (EpochInfo Identity))
-> BaseM (DELEG era) (EpochInfo Identity)
-> Rule (DELEG era) 'Transition (EpochInfo Identity)
forall a b. (a -> b) -> a -> b
$ (Globals -> EpochInfo Identity)
-> ReaderT Globals Identity (EpochInfo Identity)
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> EpochInfo Identity
epochInfoPure
          EpochNo Word64
currEpoch <- BaseM (DELEG era) EpochNo -> Rule (DELEG era) 'Transition EpochNo
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (DELEG era) EpochNo -> Rule (DELEG era) 'Transition EpochNo)
-> BaseM (DELEG era) EpochNo
-> Rule (DELEG era) 'Transition EpochNo
forall a b. (a -> b) -> a -> b
$ HasCallStack => EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
epochInfoEpoch EpochInfo Identity
ei SlotNo
slot
          let newEpoch :: EpochNo
newEpoch = Word64 -> EpochNo
EpochNo (Word64
currEpoch Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1)
          Event (DELEG era) -> Rule (DELEG era) 'Transition ()
forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent (EpochNo -> DelegEvent era
forall era. EpochNo -> DelegEvent era
NewEpoch EpochNo
newEpoch)
          SlotNo
firstSlot <- BaseM (DELEG era) SlotNo -> Rule (DELEG era) 'Transition SlotNo
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (DELEG era) SlotNo -> Rule (DELEG era) 'Transition SlotNo)
-> BaseM (DELEG era) SlotNo -> Rule (DELEG era) 'Transition SlotNo
forall a b. (a -> b) -> a -> b
$ HasCallStack => EpochInfo Identity -> EpochNo -> ShelleyBase SlotNo
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 SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
< SlotNo
tooLate
            Bool
-> PredicateFailure (DELEG era) -> Rule (DELEG era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! SlotNo -> SlotNo -> DelegPredicateFailure era
forall era. SlotNo -> SlotNo -> DelegPredicateFailure era
MIRCertificateTooLateinEpochDELEG SlotNo
slot SlotNo
tooLate

          let (Coin
potAmount, DeltaCoin
delta, Map (StakeCredential (Crypto era)) Coin
instantaneousRewards) =
                case MIRPot
targetPot of
                  MIRPot
ReservesMIR -> (AccountState -> Coin
_reserves AccountState
acnt, InstantaneousRewards (Crypto era) -> DeltaCoin
forall crypto. InstantaneousRewards crypto -> DeltaCoin
deltaReserves (InstantaneousRewards (Crypto era) -> DeltaCoin)
-> (DState (Crypto era) -> InstantaneousRewards (Crypto era))
-> DState (Crypto era)
-> DeltaCoin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DState (Crypto era) -> InstantaneousRewards (Crypto era)
forall crypto. DState crypto -> InstantaneousRewards crypto
_irwd (DState (Crypto era) -> DeltaCoin)
-> DState (Crypto era) -> DeltaCoin
forall a b. (a -> b) -> a -> b
$ State (DELEG era)
DState (Crypto era)
ds, InstantaneousRewards (Crypto era)
-> Map (StakeCredential (Crypto era)) Coin
forall crypto.
InstantaneousRewards crypto
-> Map (Credential 'Staking crypto) Coin
iRReserves (InstantaneousRewards (Crypto era)
 -> Map (StakeCredential (Crypto era)) Coin)
-> InstantaneousRewards (Crypto era)
-> Map (StakeCredential (Crypto era)) Coin
forall a b. (a -> b) -> a -> b
$ DState (Crypto era) -> InstantaneousRewards (Crypto era)
forall crypto. DState crypto -> InstantaneousRewards crypto
_irwd State (DELEG era)
DState (Crypto era)
ds)
                  MIRPot
TreasuryMIR -> (AccountState -> Coin
_treasury AccountState
acnt, InstantaneousRewards (Crypto era) -> DeltaCoin
forall crypto. InstantaneousRewards crypto -> DeltaCoin
deltaTreasury (InstantaneousRewards (Crypto era) -> DeltaCoin)
-> (DState (Crypto era) -> InstantaneousRewards (Crypto era))
-> DState (Crypto era)
-> DeltaCoin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DState (Crypto era) -> InstantaneousRewards (Crypto era)
forall crypto. DState crypto -> InstantaneousRewards crypto
_irwd (DState (Crypto era) -> DeltaCoin)
-> DState (Crypto era) -> DeltaCoin
forall a b. (a -> b) -> a -> b
$ State (DELEG era)
DState (Crypto era)
ds, InstantaneousRewards (Crypto era)
-> Map (StakeCredential (Crypto era)) Coin
forall crypto.
InstantaneousRewards crypto
-> Map (Credential 'Staking crypto) Coin
iRTreasury (InstantaneousRewards (Crypto era)
 -> Map (StakeCredential (Crypto era)) Coin)
-> InstantaneousRewards (Crypto era)
-> Map (StakeCredential (Crypto era)) Coin
forall a b. (a -> b) -> a -> b
$ DState (Crypto era) -> InstantaneousRewards (Crypto era)
forall crypto. DState crypto -> InstantaneousRewards crypto
_irwd State (DELEG era)
DState (Crypto era)
ds)
              credCoinMap' :: Map (StakeCredential (Crypto era)) Coin
credCoinMap' = (DeltaCoin -> Coin)
-> Map (StakeCredential (Crypto era)) DeltaCoin
-> Map (StakeCredential (Crypto era)) Coin
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\(DeltaCoin Integer
x) -> Integer -> Coin
Coin Integer
x) Map (StakeCredential (Crypto era)) DeltaCoin
credCoinMap
              combinedMap :: Map (StakeCredential (Crypto era)) Coin
combinedMap = (Coin -> Coin -> Coin)
-> Map (StakeCredential (Crypto era)) Coin
-> Map (StakeCredential (Crypto era)) Coin
-> Map (StakeCredential (Crypto era)) Coin
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
(<>) Map (StakeCredential (Crypto era)) Coin
credCoinMap' Map (StakeCredential (Crypto era)) Coin
instantaneousRewards
              requiredForRewards :: Coin
requiredForRewards = Map (StakeCredential (Crypto era)) Coin -> Coin
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (StakeCredential (Crypto era)) Coin
combinedMap
              available :: Coin
available = Coin
potAmount Coin -> DeltaCoin -> Coin
`addDeltaCoin` DeltaCoin
delta

          (Coin -> Bool) -> Map (StakeCredential (Crypto era)) Coin -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
>= Coin
forall a. Monoid a => a
mempty) Map (StakeCredential (Crypto era)) Coin
combinedMap Bool
-> PredicateFailure (DELEG era) -> Rule (DELEG era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure (DELEG era)
forall era. DelegPredicateFailure era
MIRProducesNegativeUpdate

          Coin
requiredForRewards Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
<= Coin
available
            Bool
-> PredicateFailure (DELEG era) -> Rule (DELEG era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! MIRPot -> Coin -> Coin -> DelegPredicateFailure era
forall era. MIRPot -> Coin -> Coin -> DelegPredicateFailure era
InsufficientForInstantaneousRewardsDELEG MIRPot
targetPot Coin
requiredForRewards Coin
available

          case MIRPot
targetPot of
            MIRPot
ReservesMIR -> DState (Crypto era)
-> F (Clause (DELEG era) 'Transition) (DState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DState (Crypto era)
 -> F (Clause (DELEG era) 'Transition) (DState (Crypto era)))
-> DState (Crypto era)
-> F (Clause (DELEG era) 'Transition) (DState (Crypto era))
forall a b. (a -> b) -> a -> b
$ State (DELEG era)
DState (Crypto era)
ds {_irwd :: InstantaneousRewards (Crypto era)
_irwd = (DState (Crypto era) -> InstantaneousRewards (Crypto era)
forall crypto. DState crypto -> InstantaneousRewards crypto
_irwd State (DELEG era)
DState (Crypto era)
ds) {iRReserves :: Map (StakeCredential (Crypto era)) Coin
iRReserves = Map (StakeCredential (Crypto era)) Coin
combinedMap}}
            MIRPot
TreasuryMIR -> DState (Crypto era)
-> F (Clause (DELEG era) 'Transition) (DState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DState (Crypto era)
 -> F (Clause (DELEG era) 'Transition) (DState (Crypto era)))
-> DState (Crypto era)
-> F (Clause (DELEG era) 'Transition) (DState (Crypto era))
forall a b. (a -> b) -> a -> b
$ State (DELEG era)
DState (Crypto era)
ds {_irwd :: InstantaneousRewards (Crypto era)
_irwd = (DState (Crypto era) -> InstantaneousRewards (Crypto era)
forall crypto. DState crypto -> InstantaneousRewards crypto
_irwd State (DELEG era)
DState (Crypto era)
ds) {iRTreasury :: Map (StakeCredential (Crypto era)) Coin
iRTreasury = Map (StakeCredential (Crypto era)) Coin
combinedMap}}
        else do
          Word64
sp <- BaseM (DELEG era) Word64 -> Rule (DELEG era) 'Transition Word64
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (DELEG era) Word64 -> Rule (DELEG era) 'Transition Word64)
-> BaseM (DELEG era) Word64 -> Rule (DELEG era) 'Transition Word64
forall a b. (a -> b) -> a -> b
$ (Globals -> Word64) -> ReaderT Globals Identity Word64
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> Word64
stabilityWindow
          EpochInfo Identity
ei <- BaseM (DELEG era) (EpochInfo Identity)
-> Rule (DELEG era) 'Transition (EpochInfo Identity)
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (DELEG era) (EpochInfo Identity)
 -> Rule (DELEG era) 'Transition (EpochInfo Identity))
-> BaseM (DELEG era) (EpochInfo Identity)
-> Rule (DELEG era) 'Transition (EpochInfo Identity)
forall a b. (a -> b) -> a -> b
$ (Globals -> EpochInfo Identity)
-> ReaderT Globals Identity (EpochInfo Identity)
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> EpochInfo Identity
epochInfoPure
          EpochNo Word64
currEpoch <- BaseM (DELEG era) EpochNo -> Rule (DELEG era) 'Transition EpochNo
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (DELEG era) EpochNo -> Rule (DELEG era) 'Transition EpochNo)
-> BaseM (DELEG era) EpochNo
-> Rule (DELEG era) 'Transition EpochNo
forall a b. (a -> b) -> a -> b
$ HasCallStack => EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
epochInfoEpoch EpochInfo Identity
ei SlotNo
slot
          let newEpoch :: EpochNo
newEpoch = Word64 -> EpochNo
EpochNo (Word64
currEpoch Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1)
          Event (DELEG era) -> Rule (DELEG era) 'Transition ()
forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent (EpochNo -> DelegEvent era
forall era. EpochNo -> DelegEvent era
NewEpoch EpochNo
newEpoch)
          SlotNo
firstSlot <- BaseM (DELEG era) SlotNo -> Rule (DELEG era) 'Transition SlotNo
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (DELEG era) SlotNo -> Rule (DELEG era) 'Transition SlotNo)
-> BaseM (DELEG era) SlotNo -> Rule (DELEG era) 'Transition SlotNo
forall a b. (a -> b) -> a -> b
$ HasCallStack => EpochInfo Identity -> EpochNo -> ShelleyBase SlotNo
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 SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
< SlotNo
tooLate
            Bool
-> PredicateFailure (DELEG era) -> Rule (DELEG era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! SlotNo -> SlotNo -> DelegPredicateFailure era
forall era. SlotNo -> SlotNo -> DelegPredicateFailure era
MIRCertificateTooLateinEpochDELEG SlotNo
slot SlotNo
tooLate

          (DeltaCoin -> Bool)
-> Map (StakeCredential (Crypto era)) DeltaCoin -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (DeltaCoin -> DeltaCoin -> Bool
forall a. Ord a => a -> a -> Bool
>= DeltaCoin
forall a. Monoid a => a
mempty) Map (StakeCredential (Crypto era)) DeltaCoin
credCoinMap Bool
-> PredicateFailure (DELEG era) -> Rule (DELEG era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure (DELEG era)
forall era. DelegPredicateFailure era
MIRNegativesNotCurrentlyAllowed

          let (Coin
potAmount, Map (StakeCredential (Crypto era)) Coin
instantaneousRewards) =
                case MIRPot
targetPot of
                  MIRPot
ReservesMIR -> (AccountState -> Coin
_reserves AccountState
acnt, InstantaneousRewards (Crypto era)
-> Map (StakeCredential (Crypto era)) Coin
forall crypto.
InstantaneousRewards crypto
-> Map (Credential 'Staking crypto) Coin
iRReserves (InstantaneousRewards (Crypto era)
 -> Map (StakeCredential (Crypto era)) Coin)
-> InstantaneousRewards (Crypto era)
-> Map (StakeCredential (Crypto era)) Coin
forall a b. (a -> b) -> a -> b
$ DState (Crypto era) -> InstantaneousRewards (Crypto era)
forall crypto. DState crypto -> InstantaneousRewards crypto
_irwd State (DELEG era)
DState (Crypto era)
ds)
                  MIRPot
TreasuryMIR -> (AccountState -> Coin
_treasury AccountState
acnt, InstantaneousRewards (Crypto era)
-> Map (StakeCredential (Crypto era)) Coin
forall crypto.
InstantaneousRewards crypto
-> Map (Credential 'Staking crypto) Coin
iRTreasury (InstantaneousRewards (Crypto era)
 -> Map (StakeCredential (Crypto era)) Coin)
-> InstantaneousRewards (Crypto era)
-> Map (StakeCredential (Crypto era)) Coin
forall a b. (a -> b) -> a -> b
$ DState (Crypto era) -> InstantaneousRewards (Crypto era)
forall crypto. DState crypto -> InstantaneousRewards crypto
_irwd State (DELEG era)
DState (Crypto era)
ds)
          let credCoinMap' :: Map (StakeCredential (Crypto era)) Coin
credCoinMap' = (DeltaCoin -> Coin)
-> Map (StakeCredential (Crypto era)) DeltaCoin
-> Map (StakeCredential (Crypto era)) Coin
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\(DeltaCoin Integer
x) -> Integer -> Coin
Coin Integer
x) Map (StakeCredential (Crypto era)) DeltaCoin
credCoinMap
              combinedMap :: Map (StakeCredential (Crypto era)) Coin
combinedMap = Map (StakeCredential (Crypto era)) Coin
-> Map (StakeCredential (Crypto era)) Coin
-> Map (StakeCredential (Crypto era)) Coin
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map (StakeCredential (Crypto era)) Coin
credCoinMap' Map (StakeCredential (Crypto era)) Coin
instantaneousRewards
              requiredForRewards :: Coin
requiredForRewards = Map (StakeCredential (Crypto era)) Coin -> Coin
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (StakeCredential (Crypto era)) Coin
combinedMap
          Coin
requiredForRewards Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
<= Coin
potAmount
            Bool
-> PredicateFailure (DELEG era) -> Rule (DELEG era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! MIRPot -> Coin -> Coin -> DelegPredicateFailure era
forall era. MIRPot -> Coin -> Coin -> DelegPredicateFailure era
InsufficientForInstantaneousRewardsDELEG MIRPot
targetPot Coin
requiredForRewards Coin
potAmount

          case MIRPot
targetPot of
            MIRPot
ReservesMIR -> DState (Crypto era)
-> F (Clause (DELEG era) 'Transition) (DState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DState (Crypto era)
 -> F (Clause (DELEG era) 'Transition) (DState (Crypto era)))
-> DState (Crypto era)
-> F (Clause (DELEG era) 'Transition) (DState (Crypto era))
forall a b. (a -> b) -> a -> b
$ State (DELEG era)
DState (Crypto era)
ds {_irwd :: InstantaneousRewards (Crypto era)
_irwd = (DState (Crypto era) -> InstantaneousRewards (Crypto era)
forall crypto. DState crypto -> InstantaneousRewards crypto
_irwd State (DELEG era)
DState (Crypto era)
ds) {iRReserves :: Map (StakeCredential (Crypto era)) Coin
iRReserves = Map (StakeCredential (Crypto era)) Coin
combinedMap}}
            MIRPot
TreasuryMIR -> DState (Crypto era)
-> F (Clause (DELEG era) 'Transition) (DState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DState (Crypto era)
 -> F (Clause (DELEG era) 'Transition) (DState (Crypto era)))
-> DState (Crypto era)
-> F (Clause (DELEG era) 'Transition) (DState (Crypto era))
forall a b. (a -> b) -> a -> b
$ State (DELEG era)
DState (Crypto era)
ds {_irwd :: InstantaneousRewards (Crypto era)
_irwd = (DState (Crypto era) -> InstantaneousRewards (Crypto era)
forall crypto. DState crypto -> InstantaneousRewards crypto
_irwd State (DELEG era)
DState (Crypto era)
ds) {iRTreasury :: Map (StakeCredential (Crypto era)) Coin
iRTreasury = Map (StakeCredential (Crypto era)) Coin
combinedMap}}
    DCertMir (MIRCert targetPot (SendToOppositePotMIR coin)) ->
      if PParams era -> Bool
forall pp. HasField "_protocolVersion" pp ProtVer => pp -> Bool
HardForks.allowMIRTransfer PParams era
pp
        then do
          Word64
sp <- BaseM (DELEG era) Word64 -> Rule (DELEG era) 'Transition Word64
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (DELEG era) Word64 -> Rule (DELEG era) 'Transition Word64)
-> BaseM (DELEG era) Word64 -> Rule (DELEG era) 'Transition Word64
forall a b. (a -> b) -> a -> b
$ (Globals -> Word64) -> ReaderT Globals Identity Word64
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> Word64
stabilityWindow
          EpochInfo Identity
ei <- BaseM (DELEG era) (EpochInfo Identity)
-> Rule (DELEG era) 'Transition (EpochInfo Identity)
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (DELEG era) (EpochInfo Identity)
 -> Rule (DELEG era) 'Transition (EpochInfo Identity))
-> BaseM (DELEG era) (EpochInfo Identity)
-> Rule (DELEG era) 'Transition (EpochInfo Identity)
forall a b. (a -> b) -> a -> b
$ (Globals -> EpochInfo Identity)
-> ReaderT Globals Identity (EpochInfo Identity)
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> EpochInfo Identity
epochInfoPure
          EpochNo Word64
currEpoch <- BaseM (DELEG era) EpochNo -> Rule (DELEG era) 'Transition EpochNo
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (DELEG era) EpochNo -> Rule (DELEG era) 'Transition EpochNo)
-> BaseM (DELEG era) EpochNo
-> Rule (DELEG era) 'Transition EpochNo
forall a b. (a -> b) -> a -> b
$ HasCallStack => EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
epochInfoEpoch EpochInfo Identity
ei SlotNo
slot
          let newEpoch :: EpochNo
newEpoch = Word64 -> EpochNo
EpochNo (Word64
currEpoch Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1)
          Event (DELEG era) -> Rule (DELEG era) 'Transition ()
forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent (EpochNo -> DelegEvent era
forall era. EpochNo -> DelegEvent era
NewEpoch EpochNo
newEpoch)
          SlotNo
firstSlot <- BaseM (DELEG era) SlotNo -> Rule (DELEG era) 'Transition SlotNo
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (DELEG era) SlotNo -> Rule (DELEG era) 'Transition SlotNo)
-> BaseM (DELEG era) SlotNo -> Rule (DELEG era) 'Transition SlotNo
forall a b. (a -> b) -> a -> b
$ HasCallStack => EpochInfo Identity -> EpochNo -> ShelleyBase SlotNo
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 SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
< SlotNo
tooLate
            Bool
-> PredicateFailure (DELEG era) -> Rule (DELEG era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! SlotNo -> SlotNo -> DelegPredicateFailure era
forall era. SlotNo -> SlotNo -> DelegPredicateFailure era
MIRCertificateTooLateinEpochDELEG SlotNo
slot SlotNo
tooLate

          let available :: Coin
available = MIRPot -> AccountState -> InstantaneousRewards (Crypto era) -> Coin
forall crypto.
MIRPot -> AccountState -> InstantaneousRewards crypto -> Coin
availableAfterMIR MIRPot
targetPot AccountState
acnt (DState (Crypto era) -> InstantaneousRewards (Crypto era)
forall crypto. DState crypto -> InstantaneousRewards crypto
_irwd State (DELEG era)
DState (Crypto era)
ds)
          Coin
coin Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
>= Coin
forall a. Monoid a => a
mempty
            Bool
-> PredicateFailure (DELEG era) -> Rule (DELEG era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! MIRPot -> Coin -> DelegPredicateFailure era
forall era. MIRPot -> Coin -> DelegPredicateFailure era
MIRNegativeTransfer MIRPot
targetPot Coin
coin
          Coin
coin Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
<= Coin
available
            Bool
-> PredicateFailure (DELEG era) -> Rule (DELEG era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! MIRPot -> Coin -> Coin -> DelegPredicateFailure era
forall era. MIRPot -> Coin -> Coin -> DelegPredicateFailure era
InsufficientForTransferDELEG MIRPot
targetPot Coin
coin Coin
available

          let ir :: InstantaneousRewards (Crypto era)
ir = DState (Crypto era) -> InstantaneousRewards (Crypto era)
forall crypto. DState crypto -> InstantaneousRewards crypto
_irwd State (DELEG era)
DState (Crypto era)
ds
              dr :: DeltaCoin
dr = InstantaneousRewards (Crypto era) -> DeltaCoin
forall crypto. InstantaneousRewards crypto -> DeltaCoin
deltaReserves InstantaneousRewards (Crypto era)
ir
              dt :: DeltaCoin
dt = InstantaneousRewards (Crypto era) -> DeltaCoin
forall crypto. InstantaneousRewards crypto -> DeltaCoin
deltaTreasury InstantaneousRewards (Crypto era)
ir
          case MIRPot
targetPot of
            MIRPot
ReservesMIR ->
              DState (Crypto era)
-> F (Clause (DELEG era) 'Transition) (DState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DState (Crypto era)
 -> F (Clause (DELEG era) 'Transition) (DState (Crypto era)))
-> DState (Crypto era)
-> F (Clause (DELEG era) 'Transition) (DState (Crypto era))
forall a b. (a -> b) -> a -> b
$
                State (DELEG era)
DState (Crypto era)
ds
                  { _irwd :: InstantaneousRewards (Crypto era)
_irwd =
                      InstantaneousRewards (Crypto era)
ir
                        { deltaReserves :: DeltaCoin
deltaReserves = DeltaCoin
dr DeltaCoin -> DeltaCoin -> DeltaCoin
forall a. Semigroup a => a -> a -> a
<> DeltaCoin -> DeltaCoin
forall m. Group m => m -> m
invert (Coin -> DeltaCoin
toDeltaCoin Coin
coin),
                          deltaTreasury :: DeltaCoin
deltaTreasury = DeltaCoin
dt DeltaCoin -> DeltaCoin -> DeltaCoin
forall a. Semigroup a => a -> a -> a
<> Coin -> DeltaCoin
toDeltaCoin Coin
coin
                        }
                  }
            MIRPot
TreasuryMIR ->
              DState (Crypto era)
-> F (Clause (DELEG era) 'Transition) (DState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DState (Crypto era)
 -> F (Clause (DELEG era) 'Transition) (DState (Crypto era)))
-> DState (Crypto era)
-> F (Clause (DELEG era) 'Transition) (DState (Crypto era))
forall a b. (a -> b) -> a -> b
$
                State (DELEG era)
DState (Crypto era)
ds
                  { _irwd :: InstantaneousRewards (Crypto era)
_irwd =
                      InstantaneousRewards (Crypto era)
ir
                        { deltaReserves :: DeltaCoin
deltaReserves = DeltaCoin
dr DeltaCoin -> DeltaCoin -> DeltaCoin
forall a. Semigroup a => a -> a -> a
<> Coin -> DeltaCoin
toDeltaCoin Coin
coin,
                          deltaTreasury :: DeltaCoin
deltaTreasury = DeltaCoin
dt DeltaCoin -> DeltaCoin -> DeltaCoin
forall a. Semigroup a => a -> a -> a
<> DeltaCoin -> DeltaCoin
forall m. Group m => m -> m
invert (Coin -> DeltaCoin
toDeltaCoin Coin
coin)
                        }
                  }
        else do
          PredicateFailure (DELEG era) -> Rule (DELEG era) 'Transition ()
forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause PredicateFailure (DELEG era)
forall era. DelegPredicateFailure era
MIRTransferNotCurrentlyAllowed
          DState (Crypto era)
-> F (Clause (DELEG era) 'Transition) (DState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure State (DELEG era)
DState (Crypto era)
ds
    DCertPool _ -> do
      PredicateFailure (DELEG era) -> Rule (DELEG era) 'Transition ()
forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause PredicateFailure (DELEG era)
forall era. DelegPredicateFailure era
WrongCertificateTypeDELEG -- this always fails
      DState (Crypto era)
-> F (Clause (DELEG era) 'Transition) (DState (Crypto era))
forall (f :: * -> *) a. Applicative f => a -> f a
pure State (DELEG era)
DState (Crypto era)
ds