{-# 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 (
  EpochInterval (..),
  Globals (..),
  Mismatch (..),
  Relation (..),
  ShelleyBase,
  StrictMaybe (..),
  addEpochInterval,
  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.Hashes (GenDelegPair (..), GenDelegs (..))
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 (availableAfterMIR)
import Cardano.Ledger.Shelley.State
import Cardano.Ledger.Slot (
  Duration (..),
  EpochNo (..),
  SlotNo,
  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 -> EpochNo
deCurEpochNo :: EpochNo
  -- ^ Lazy on purpose, because not all certificates need to know the current EpochNo
  , forall era. DelegEnv era -> Ptr
ptr_ :: Ptr
  , forall era. DelegEnv era -> ChainAccountState
deChainAccountState :: ChainAccountState
  , forall era. DelegEnv era -> PParams era
ppDE :: PParams era -- The protocol parameters are only used for the HardFork mechanism
  }
  deriving ((forall x. DelegEnv era -> Rep (DelegEnv era) x)
-> (forall x. Rep (DelegEnv era) x -> DelegEnv era)
-> Generic (DelegEnv era)
forall x. Rep (DelegEnv era) x -> DelegEnv era
forall x. DelegEnv era -> Rep (DelegEnv era) x
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
$cfrom :: forall era x. DelegEnv era -> Rep (DelegEnv era) x
from :: forall x. DelegEnv era -> Rep (DelegEnv era) x
$cto :: forall era x. Rep (DelegEnv era) x -> DelegEnv era
to :: forall x. Rep (DelegEnv era) x -> DelegEnv era
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) -- Credential which is already registered
  | StakeKeyNotRegisteredDELEG
      (Credential 'Staking) -- Credential which is not registered
  | StakeKeyNonZeroAccountBalanceDELEG
      Coin -- The remaining reward account balance
  | StakeDelegationImpossibleDELEG
      (Credential 'Staking) -- Credential that is not registered
  | WrongCertificateTypeDELEG -- The TxCertPool constructor should not be used by this transition
  | GenesisKeyNotInMappingDELEG
      (KeyHash 'Genesis) -- Unknown Genesis KeyHash
  | DuplicateGenesisDelegateDELEG
      (KeyHash 'GenesisDelegate) -- 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) -- 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
[ShelleyDelegPredFailure era] -> ShowS
ShelleyDelegPredFailure era -> String
(Int -> ShelleyDelegPredFailure era -> ShowS)
-> (ShelleyDelegPredFailure era -> String)
-> ([ShelleyDelegPredFailure era] -> ShowS)
-> Show (ShelleyDelegPredFailure era)
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
$cshowsPrec :: forall era. Int -> ShelleyDelegPredFailure era -> ShowS
showsPrec :: Int -> ShelleyDelegPredFailure era -> ShowS
$cshow :: forall era. ShelleyDelegPredFailure era -> String
show :: ShelleyDelegPredFailure era -> String
$cshowList :: forall era. [ShelleyDelegPredFailure era] -> ShowS
showList :: [ShelleyDelegPredFailure era] -> ShowS
Show, ShelleyDelegPredFailure era -> ShelleyDelegPredFailure era -> Bool
(ShelleyDelegPredFailure era
 -> ShelleyDelegPredFailure era -> Bool)
-> (ShelleyDelegPredFailure era
    -> ShelleyDelegPredFailure era -> Bool)
-> Eq (ShelleyDelegPredFailure era)
forall era.
ShelleyDelegPredFailure era -> ShelleyDelegPredFailure era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall era.
ShelleyDelegPredFailure era -> ShelleyDelegPredFailure era -> Bool
== :: ShelleyDelegPredFailure era -> ShelleyDelegPredFailure era -> Bool
$c/= :: forall era.
ShelleyDelegPredFailure era -> ShelleyDelegPredFailure era -> Bool
/= :: ShelleyDelegPredFailure era -> ShelleyDelegPredFailure era -> Bool
Eq, (forall x.
 ShelleyDelegPredFailure era -> Rep (ShelleyDelegPredFailure era) x)
-> (forall x.
    Rep (ShelleyDelegPredFailure era) x -> ShelleyDelegPredFailure era)
-> Generic (ShelleyDelegPredFailure era)
forall x.
Rep (ShelleyDelegPredFailure era) x -> ShelleyDelegPredFailure era
forall x.
ShelleyDelegPredFailure era -> Rep (ShelleyDelegPredFailure era) x
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
$cfrom :: forall era x.
ShelleyDelegPredFailure era -> Rep (ShelleyDelegPredFailure era) x
from :: forall x.
ShelleyDelegPredFailure era -> Rep (ShelleyDelegPredFailure era) x
$cto :: forall era x.
Rep (ShelleyDelegPredFailure era) x -> ShelleyDelegPredFailure era
to :: forall x.
Rep (ShelleyDelegPredFailure era) x -> ShelleyDelegPredFailure era
Generic)

type instance EraRuleFailure "DELEG" ShelleyEra = ShelleyDelegPredFailure ShelleyEra

instance InjectRuleFailure "DELEG" ShelleyDelegPredFailure ShelleyEra

newtype ShelleyDelegEvent era = DelegNewEpoch EpochNo
  deriving ((forall x. ShelleyDelegEvent era -> Rep (ShelleyDelegEvent era) x)
-> (forall x.
    Rep (ShelleyDelegEvent era) x -> ShelleyDelegEvent era)
-> Generic (ShelleyDelegEvent era)
forall x. Rep (ShelleyDelegEvent era) x -> ShelleyDelegEvent era
forall x. ShelleyDelegEvent era -> Rep (ShelleyDelegEvent era) x
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
$cfrom :: forall era x.
ShelleyDelegEvent era -> Rep (ShelleyDelegEvent era) x
from :: forall x. ShelleyDelegEvent era -> Rep (ShelleyDelegEvent era) x
$cto :: forall era x.
Rep (ShelleyDelegEvent era) x -> ShelleyDelegEvent era
to :: forall x. Rep (ShelleyDelegEvent era) x -> ShelleyDelegEvent era
Generic, ShelleyDelegEvent era -> ShelleyDelegEvent era -> Bool
(ShelleyDelegEvent era -> ShelleyDelegEvent era -> Bool)
-> (ShelleyDelegEvent era -> ShelleyDelegEvent era -> Bool)
-> Eq (ShelleyDelegEvent era)
forall era. ShelleyDelegEvent era -> ShelleyDelegEvent era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall era. ShelleyDelegEvent era -> ShelleyDelegEvent era -> Bool
== :: ShelleyDelegEvent era -> ShelleyDelegEvent era -> Bool
$c/= :: forall era. ShelleyDelegEvent era -> ShelleyDelegEvent era -> Bool
/= :: 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 = [TransitionRule (ShelleyDELEG era)
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
cred ->
      Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
0 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Credential 'Staking -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Credential 'Staking
cred
    StakeKeyNotRegisteredDELEG Credential 'Staking
cred ->
      Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
1 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Credential 'Staking -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Credential 'Staking
cred
    StakeKeyNonZeroAccountBalanceDELEG Coin
rewardBalance ->
      Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
2 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Coin -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Coin
rewardBalance
    StakeDelegationImpossibleDELEG Credential 'Staking
cred ->
      Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
3 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Credential 'Staking -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Credential 'Staking
cred
    ShelleyDelegPredFailure era
WrongCertificateTypeDELEG ->
      Word -> Encoding
encodeListLen Word
1 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
4 :: Word8)
    GenesisKeyNotInMappingDELEG KeyHash 'Genesis
gkh ->
      Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
5 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> KeyHash 'Genesis -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR KeyHash 'Genesis
gkh
    DuplicateGenesisDelegateDELEG KeyHash 'GenesisDelegate
kh ->
      Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
6 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> KeyHash 'GenesisDelegate -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR KeyHash 'GenesisDelegate
kh
    InsufficientForInstantaneousRewardsDELEG MIRPot
pot Mismatch 'RelLTEQ Coin
m ->
      Word -> Encoding
encodeListLen Word
3
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
7 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> MIRPot -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR MIRPot
pot
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Mismatch 'RelLTEQ Coin -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Mismatch 'RelLTEQ Coin
m
    MIRCertificateTooLateinEpochDELEG Mismatch 'RelLT SlotNo
m ->
      Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
8 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Mismatch 'RelLT SlotNo -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Mismatch 'RelLT SlotNo
m
    DuplicateGenesisVRFDELEG VRFVerKeyHash 'GenDelegVRF
vrf ->
      Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
9 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> VRFVerKeyHash 'GenDelegVRF -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR VRFVerKeyHash 'GenDelegVRF
vrf
    ShelleyDelegPredFailure era
MIRTransferNotCurrentlyAllowed ->
      Word -> Encoding
encodeListLen Word
1 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
11 :: Word8)
    ShelleyDelegPredFailure era
MIRNegativesNotCurrentlyAllowed ->
      Word -> Encoding
encodeListLen Word
1 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
12 :: Word8)
    InsufficientForTransferDELEG MIRPot
pot Mismatch 'RelLTEQ Coin
m ->
      Word -> Encoding
encodeListLen Word
3
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
13 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> MIRPot -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR MIRPot
pot
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Mismatch 'RelLTEQ Coin -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Mismatch 'RelLTEQ Coin
m
    ShelleyDelegPredFailure era
MIRProducesNegativeUpdate ->
      Word -> Encoding
encodeListLen Word
1 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (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. EncCBOR a => a -> Encoding
encCBOR (Word8
15 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> MIRPot -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR MIRPot
pot
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Coin -> Encoding
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 = Text
-> (Word -> Decoder s (Int, ShelleyDelegPredFailure era))
-> Decoder s (ShelleyDelegPredFailure era)
forall s a. Text -> (Word -> Decoder s (Int, a)) -> Decoder s a
decodeRecordSum Text
"ShelleyDelegPredFailure" ((Word -> Decoder s (Int, ShelleyDelegPredFailure era))
 -> Decoder s (ShelleyDelegPredFailure era))
-> (Word -> Decoder s (Int, ShelleyDelegPredFailure era))
-> Decoder s (ShelleyDelegPredFailure era)
forall a b. (a -> b) -> a -> b
$
    \case
      Word
0 -> do
        Credential 'Staking
kh <- Decoder s (Credential 'Staking)
forall s. Decoder s (Credential 'Staking)
forall a s. DecCBOR a => Decoder s a
decCBOR
        (Int, ShelleyDelegPredFailure era)
-> Decoder s (Int, ShelleyDelegPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, Credential 'Staking -> ShelleyDelegPredFailure era
forall era. Credential 'Staking -> ShelleyDelegPredFailure era
StakeKeyAlreadyRegisteredDELEG Credential 'Staking
kh)
      Word
1 -> do
        Credential 'Staking
kh <- Decoder s (Credential 'Staking)
forall s. Decoder s (Credential 'Staking)
forall a s. DecCBOR a => Decoder s a
decCBOR
        (Int, ShelleyDelegPredFailure era)
-> Decoder s (Int, ShelleyDelegPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, Credential 'Staking -> ShelleyDelegPredFailure era
forall era. Credential 'Staking -> ShelleyDelegPredFailure era
StakeKeyNotRegisteredDELEG Credential 'Staking
kh)
      Word
2 -> do
        Coin
b <- Decoder s Coin
forall s. Decoder s Coin
forall a s. DecCBOR a => Decoder s a
decCBOR
        (Int, ShelleyDelegPredFailure era)
-> Decoder s (Int, ShelleyDelegPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, Coin -> ShelleyDelegPredFailure era
forall era. Coin -> ShelleyDelegPredFailure era
StakeKeyNonZeroAccountBalanceDELEG Coin
b)
      Word
3 -> do
        Credential 'Staking
kh <- Decoder s (Credential 'Staking)
forall s. Decoder s (Credential 'Staking)
forall a s. DecCBOR a => Decoder s a
decCBOR
        (Int, ShelleyDelegPredFailure era)
-> Decoder s (Int, ShelleyDelegPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, Credential 'Staking -> ShelleyDelegPredFailure era
forall era. Credential 'Staking -> ShelleyDelegPredFailure era
StakeDelegationImpossibleDELEG Credential 'Staking
kh)
      Word
4 -> do
        (Int, ShelleyDelegPredFailure era)
-> Decoder s (Int, ShelleyDelegPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
1, ShelleyDelegPredFailure era
forall era. ShelleyDelegPredFailure era
WrongCertificateTypeDELEG)
      Word
5 -> do
        KeyHash 'Genesis
gkh <- Decoder s (KeyHash 'Genesis)
forall s. Decoder s (KeyHash 'Genesis)
forall a s. DecCBOR a => Decoder s a
decCBOR
        (Int, ShelleyDelegPredFailure era)
-> Decoder s (Int, ShelleyDelegPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, KeyHash 'Genesis -> ShelleyDelegPredFailure era
forall era. KeyHash 'Genesis -> ShelleyDelegPredFailure era
GenesisKeyNotInMappingDELEG KeyHash 'Genesis
gkh)
      Word
6 -> do
        KeyHash 'GenesisDelegate
kh <- Decoder s (KeyHash 'GenesisDelegate)
forall s. Decoder s (KeyHash 'GenesisDelegate)
forall a s. DecCBOR a => Decoder s a
decCBOR
        (Int, ShelleyDelegPredFailure era)
-> Decoder s (Int, ShelleyDelegPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, KeyHash 'GenesisDelegate -> ShelleyDelegPredFailure era
forall era. KeyHash 'GenesisDelegate -> ShelleyDelegPredFailure era
DuplicateGenesisDelegateDELEG KeyHash 'GenesisDelegate
kh)
      Word
7 -> do
        MIRPot
pot <- Decoder s MIRPot
forall s. Decoder s MIRPot
forall a s. DecCBOR a => Decoder s a
decCBOR
        Mismatch 'RelLTEQ Coin
m <- Decoder s (Mismatch 'RelLTEQ Coin)
forall s. Decoder s (Mismatch 'RelLTEQ Coin)
forall a s. DecCBOR a => Decoder s a
decCBOR
        (Int, ShelleyDelegPredFailure era)
-> Decoder s (Int, ShelleyDelegPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, MIRPot -> Mismatch 'RelLTEQ Coin -> ShelleyDelegPredFailure era
forall era.
MIRPot -> Mismatch 'RelLTEQ Coin -> ShelleyDelegPredFailure era
InsufficientForInstantaneousRewardsDELEG MIRPot
pot Mismatch 'RelLTEQ Coin
m)
      Word
8 -> do
        Mismatch 'RelLT SlotNo
m <- Decoder s (Mismatch 'RelLT SlotNo)
forall s. Decoder s (Mismatch 'RelLT SlotNo)
forall a s. DecCBOR a => Decoder s a
decCBOR
        (Int, ShelleyDelegPredFailure era)
-> Decoder s (Int, ShelleyDelegPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, Mismatch 'RelLT SlotNo -> ShelleyDelegPredFailure era
forall era. Mismatch 'RelLT SlotNo -> ShelleyDelegPredFailure era
MIRCertificateTooLateinEpochDELEG Mismatch 'RelLT SlotNo
m)
      Word
9 -> do
        VRFVerKeyHash 'GenDelegVRF
vrf <- Decoder s (VRFVerKeyHash 'GenDelegVRF)
forall s. Decoder s (VRFVerKeyHash 'GenDelegVRF)
forall a s. DecCBOR a => Decoder s a
decCBOR
        (Int, ShelleyDelegPredFailure era)
-> Decoder s (Int, ShelleyDelegPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, VRFVerKeyHash 'GenDelegVRF -> ShelleyDelegPredFailure era
forall era.
VRFVerKeyHash 'GenDelegVRF -> ShelleyDelegPredFailure era
DuplicateGenesisVRFDELEG VRFVerKeyHash 'GenDelegVRF
vrf)
      Word
11 -> do
        (Int, ShelleyDelegPredFailure era)
-> Decoder s (Int, ShelleyDelegPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
1, ShelleyDelegPredFailure era
forall era. ShelleyDelegPredFailure era
MIRTransferNotCurrentlyAllowed)
      Word
12 -> do
        (Int, ShelleyDelegPredFailure era)
-> Decoder s (Int, ShelleyDelegPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
1, ShelleyDelegPredFailure era
forall era. ShelleyDelegPredFailure era
MIRNegativesNotCurrentlyAllowed)
      Word
13 -> do
        MIRPot
pot <- Decoder s MIRPot
forall s. Decoder s MIRPot
forall a s. DecCBOR a => Decoder s a
decCBOR
        Mismatch 'RelLTEQ Coin
m <- Decoder s (Mismatch 'RelLTEQ Coin)
forall s. Decoder s (Mismatch 'RelLTEQ Coin)
forall a s. DecCBOR a => Decoder s a
decCBOR
        (Int, ShelleyDelegPredFailure era)
-> Decoder s (Int, ShelleyDelegPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, MIRPot -> Mismatch 'RelLTEQ Coin -> ShelleyDelegPredFailure era
forall era.
MIRPot -> Mismatch 'RelLTEQ Coin -> ShelleyDelegPredFailure era
InsufficientForTransferDELEG MIRPot
pot Mismatch 'RelLTEQ Coin
m)
      Word
14 -> do
        (Int, ShelleyDelegPredFailure era)
-> Decoder s (Int, ShelleyDelegPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
1, ShelleyDelegPredFailure era
forall era. ShelleyDelegPredFailure era
MIRProducesNegativeUpdate)
      Word
15 -> do
        MIRPot
pot <- Decoder s MIRPot
forall s. Decoder s MIRPot
forall a s. DecCBOR a => Decoder s a
decCBOR
        Coin
amt <- Decoder s Coin
forall s. Decoder s Coin
forall a s. DecCBOR a => Decoder s a
decCBOR
        (Int, ShelleyDelegPredFailure era)
-> Decoder s (Int, ShelleyDelegPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
3, MIRPot -> Coin -> ShelleyDelegPredFailure era
forall era. MIRPot -> Coin -> ShelleyDelegPredFailure era
MIRNegativeTransfer MIRPot
pot Coin
amt)
      Word
k -> Word -> Decoder s (Int, ShelleyDelegPredFailure era)
forall a (m :: * -> *). (Typeable 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 EpochNo
epochNo Ptr
ptr ChainAccountState
chainAccountState PParams era
pp, State (ShelleyDELEG era)
ds, Signal (ShelleyDELEG era)
c) <- Rule
  (ShelleyDELEG era)
  'Transition
  (RuleContext 'Transition (ShelleyDELEG era))
F (Clause (ShelleyDELEG era) 'Transition) (TRC (ShelleyDELEG era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  let pv :: ProtVer
pv = PParams era
pp PParams era -> Getting ProtVer (PParams era) ProtVer -> ProtVer
forall s a. s -> Getting a s a -> a
^. Getting ProtVer (PParams era) ProtVer
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams era) ProtVer
ppProtocolVersionL
  case Signal (ShelleyDELEG era)
c of
    RegTxCert Credential 'Staking
hk -> do
      -- (hk ∉ dom (rewards ds))
      Credential 'Staking -> UView (Credential 'Staking) RDPair -> Bool
forall k v. k -> UView k v -> Bool
UM.notMember Credential 'Staking
hk (DState era -> UView (Credential 'Staking) RDPair
forall era. DState era -> UView (Credential 'Staking) RDPair
rewards DState era
State (ShelleyDELEG era)
ds) Bool
-> PredicateFailure (ShelleyDELEG era)
-> Rule (ShelleyDELEG era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Credential 'Staking -> ShelleyDelegPredFailure era
forall era. Credential 'Staking -> ShelleyDelegPredFailure era
StakeKeyAlreadyRegisteredDELEG Credential 'Staking
hk
      let u1 :: UMap
u1 = DState era -> UMap
forall era. DState era -> UMap
dsUnified DState era
State (ShelleyDELEG era)
ds
          deposit :: CompactForm Coin
deposit = HasCallStack => Coin -> CompactForm Coin
Coin -> CompactForm Coin
compactCoinOrError (PParams era
pp PParams era -> Getting Coin (PParams era) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (PParams era) Coin
forall era. EraPParams era => Lens' (PParams era) Coin
Lens' (PParams era) Coin
ppKeyDepositL)
          u2 :: UMap
u2 = UMap -> UView (Credential 'Staking) RDPair
RewDepUView UMap
u1 UView (Credential 'Staking) RDPair
-> (Credential 'Staking, RDPair) -> UMap
forall k v. UView k v -> (k, v) -> UMap
UM.∪ (Credential 'Staking
hk, CompactForm Coin -> CompactForm Coin -> RDPair
RDPair (Word64 -> CompactForm Coin
UM.CompactCoin Word64
0) CompactForm Coin
deposit)
          u3 :: UMap
u3 = UMap -> UView Ptr (Credential 'Staking)
PtrUView UMap
u2 UView Ptr (Credential 'Staking)
-> (Ptr, Credential 'Staking) -> UMap
forall k v. UView k v -> (k, v) -> UMap
UM.∪ (Ptr
ptr, Credential 'Staking
hk)
      DState era
-> F (Clause (ShelleyDELEG era) 'Transition) (DState era)
forall a. a -> F (Clause (ShelleyDELEG era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (State (ShelleyDELEG era)
ds {dsUnified = u3})
    UnRegTxCert Credential 'Staking
cred -> do
      -- (hk ∈ dom (rewards ds))
      let (Maybe UMElem
mUMElem, UMap
umap) = Credential 'Staking -> UMap -> (Maybe UMElem, UMap)
UM.extractStakingCredential Credential 'Staking
cred (DState era -> UMap
forall era. DState era -> UMap
dsUnified DState era
State (ShelleyDELEG era)
ds)
          checkStakeKeyHasZeroRewardBalance :: Maybe Coin
checkStakeKeyHasZeroRewardBalance = do
            UM.UMElem (SJust RDPair
rd) Set Ptr
_ StrictMaybe (KeyHash 'StakePool)
_ StrictMaybe DRep
_ <- Maybe UMElem
mUMElem
            Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (RDPair -> CompactForm Coin
UM.rdReward RDPair
rd CompactForm Coin -> CompactForm Coin -> Bool
forall a. Eq a => a -> a -> Bool
/= CompactForm Coin
forall a. Monoid a => a
mempty)
            Coin -> Maybe Coin
forall a. a -> Maybe a
Just (Coin -> Maybe Coin) -> Coin -> Maybe Coin
forall a b. (a -> b) -> a -> b
$ CompactForm Coin -> Coin
forall a. Compactible a => CompactForm a -> a
UM.fromCompact (RDPair -> CompactForm Coin
UM.rdReward RDPair
rd)
      Maybe UMElem -> Bool
forall a. Maybe a -> Bool
isJust Maybe UMElem
mUMElem Bool
-> PredicateFailure (ShelleyDELEG era)
-> Rule (ShelleyDELEG era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Credential 'Staking -> ShelleyDelegPredFailure era
forall era. Credential 'Staking -> ShelleyDelegPredFailure era
StakeKeyNotRegisteredDELEG Credential 'Staking
cred
      Maybe Coin
-> (Coin -> PredicateFailure (ShelleyDELEG era))
-> Rule (ShelleyDELEG era) 'Transition ()
forall a sts (ctx :: RuleType).
Maybe a -> (a -> PredicateFailure sts) -> Rule sts ctx ()
failOnJust Maybe Coin
checkStakeKeyHasZeroRewardBalance Coin -> PredicateFailure (ShelleyDELEG era)
Coin -> ShelleyDelegPredFailure era
forall era. Coin -> ShelleyDelegPredFailure era
StakeKeyNonZeroAccountBalanceDELEG
      DState era
-> F (Clause (ShelleyDELEG era) 'Transition) (DState era)
forall a. a -> F (Clause (ShelleyDELEG era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DState era
 -> F (Clause (ShelleyDELEG era) 'Transition) (DState era))
-> DState era
-> F (Clause (ShelleyDELEG era) 'Transition) (DState era)
forall a b. (a -> b) -> a -> b
$ State (ShelleyDELEG era)
ds {dsUnified = umap}
    DelegStakeTxCert Credential 'Staking
hk KeyHash 'StakePool
dpool -> do
      -- note that pattern match is used instead of cwitness and dpool, as in the spec
      -- (hk ∈ dom (rewards ds))
      Credential 'Staking -> UView (Credential 'Staking) RDPair -> Bool
forall k v. k -> UView k v -> Bool
UM.member Credential 'Staking
hk (DState era -> UView (Credential 'Staking) RDPair
forall era. DState era -> UView (Credential 'Staking) RDPair
rewards DState era
State (ShelleyDELEG era)
ds) Bool
-> PredicateFailure (ShelleyDELEG era)
-> Rule (ShelleyDELEG era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Credential 'Staking -> ShelleyDelegPredFailure era
forall era. Credential 'Staking -> ShelleyDelegPredFailure era
StakeDelegationImpossibleDELEG Credential 'Staking
hk

      DState era
-> F (Clause (ShelleyDELEG era) 'Transition) (DState era)
forall a. a -> F (Clause (ShelleyDELEG era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (State (ShelleyDELEG era)
ds {dsUnified = delegations ds UM.⨃ Map.singleton hk dpool})
    GenesisDelegTxCert KeyHash 'Genesis
gkh KeyHash 'GenesisDelegate
vkh VRFVerKeyHash 'GenDelegVRF
vrf -> do
      Word64
sp <- BaseM (ShelleyDELEG era) Word64
-> Rule (ShelleyDELEG era) 'Transition Word64
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (ShelleyDELEG era) Word64
 -> Rule (ShelleyDELEG era) 'Transition Word64)
-> BaseM (ShelleyDELEG era) Word64
-> Rule (ShelleyDELEG 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) GenDelegPair
genDelegs = DState era -> GenDelegs
forall era. DState era -> GenDelegs
dsGenDelegs DState era
State (ShelleyDELEG era)
ds

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

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

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

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

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

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

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