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

module Shelley.Spec.Ledger.STS.Deleg
  ( DELEG,
    DelegEnv (..),
    PredicateFailure,
    DelegPredicateFailure (..),
  )
where

import Cardano.Binary
  ( FromCBOR (..),
    ToCBOR (..),
    encodeListLen,
  )
import qualified Cardano.Ledger.Core as Core
import Cardano.Ledger.Era (Crypto, Era)
import Control.Monad.Trans.Reader (asks)
import Control.SetAlgebra (dom, eval, range, setSingleton, singleton, (∈), (∉), (∪), (⋪), (⋫), (⨃))
import Control.State.Transition
import Data.Foldable (fold)
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import Data.Typeable (Typeable)
import Data.Word (Word8)
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))
import Shelley.Spec.Ledger.BaseTypes
  ( Globals (..),
    ShelleyBase,
    invalidKey,
  )
import Shelley.Spec.Ledger.Coin (Coin (..))
import Shelley.Spec.Ledger.Credential (Credential)
import Shelley.Spec.Ledger.Keys
  ( GenDelegPair (..),
    GenDelegs (..),
    Hash,
    KeyHash,
    KeyRole (..),
    VerKeyVRF,
  )
import Shelley.Spec.Ledger.LedgerState
  ( AccountState (..),
    DState,
    FutureGenDeleg (..),
    InstantaneousRewards (..),
    emptyDState,
    _delegations,
    _fGenDelegs,
    _genDelegs,
    _irwd,
    _ptrs,
    _rewards,
  )
import Shelley.Spec.Ledger.Serialization (decodeRecordSum)
import Shelley.Spec.Ledger.Slot
  ( Duration (..),
    EpochNo (..),
    SlotNo,
    epochInfoEpoch,
    epochInfoFirst,
    (*-),
    (+*),
  )
import Shelley.Spec.Ledger.TxBody
  ( DCert (..),
    DelegCert (..),
    Delegation (..),
    GenesisDelegCert (..),
    MIRCert (..),
    MIRPot (..),
    Ptr,
  )

data DELEG era

data DelegEnv = DelegEnv
  { DelegEnv -> SlotNo
slotNo :: SlotNo,
    DelegEnv -> Ptr
ptr_ :: Ptr,
    DelegEnv -> AccountState
acnt_ :: AccountState
  }
  deriving (Int -> DelegEnv -> ShowS
[DelegEnv] -> ShowS
DelegEnv -> String
(Int -> DelegEnv -> ShowS)
-> (DelegEnv -> String) -> ([DelegEnv] -> ShowS) -> Show DelegEnv
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DelegEnv] -> ShowS
$cshowList :: [DelegEnv] -> ShowS
show :: DelegEnv -> String
$cshow :: DelegEnv -> String
showsPrec :: Int -> DelegEnv -> ShowS
$cshowsPrec :: Int -> DelegEnv -> ShowS
Show, DelegEnv -> DelegEnv -> Bool
(DelegEnv -> DelegEnv -> Bool)
-> (DelegEnv -> DelegEnv -> Bool) -> Eq DelegEnv
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DelegEnv -> DelegEnv -> Bool
$c/= :: DelegEnv -> DelegEnv -> Bool
== :: DelegEnv -> DelegEnv -> Bool
$c== :: DelegEnv -> DelegEnv -> Bool
Eq)

data DelegPredicateFailure era
  = StakeKeyAlreadyRegisteredDELEG
      !(Credential 'Staking 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 era) -- DEPRECATED, now redundant with StakeKeyAlreadyRegisteredDELEG
  | StakeKeyNotRegisteredDELEG
      !(Credential 'Staking era) -- Credential which is not registered
  | StakeKeyNonZeroAccountBalanceDELEG
      !(Maybe Coin) -- The remaining reward account balance, if it exists
  | StakeDelegationImpossibleDELEG
      !(Credential 'Staking 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 -- MIR must be submitted before this slot
  | DuplicateGenesisVRFDELEG
      !(Hash (Crypto era) (VerKeyVRF (Crypto era))) --VRF KeyHash which is already delegated to
  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)

instance Typeable era => STS (DELEG era) where
  type State (DELEG era) = DState era
  type Signal (DELEG era) = DCert era
  type Environment (DELEG era) = DelegEnv
  type BaseM (DELEG era) = ShelleyBase
  type PredicateFailure (DELEG era) = DelegPredicateFailure era

  initialRules :: [InitialRule (DELEG era)]
initialRules = [DState era -> F (Clause (DELEG era) 'Initial) (DState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure DState era
forall era. DState era
emptyDState]
  transitionRules :: [TransitionRule (DELEG era)]
transitionRules = [TransitionRule (DELEG era)
forall era. Typeable era => 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 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 era -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Credential 'Staking era
cred
    StakeKeyInRewardsDELEG Credential 'Staking 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 era -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Credential 'Staking era
cred
    StakeKeyNotRegisteredDELEG Credential 'Staking 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 era -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Credential 'Staking 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 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 era -> Encoding
forall a. ToCBOR a => a -> Encoding
toCBOR Credential 'Staking 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

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 era
kh <- Decoder s (Credential 'Staking 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 era -> DelegPredicateFailure era
forall era. Credential 'Staking era -> DelegPredicateFailure era
StakeKeyAlreadyRegisteredDELEG Credential 'Staking era
kh)
      Word
10 -> do
        Credential 'Staking era
kh <- Decoder s (Credential 'Staking 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 era -> DelegPredicateFailure era
forall era. Credential 'Staking era -> DelegPredicateFailure era
StakeKeyInRewardsDELEG Credential 'Staking era
kh)
      Word
1 -> do
        Credential 'Staking era
kh <- Decoder s (Credential 'Staking 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 era -> DelegPredicateFailure era
forall era. Credential 'Staking era -> DelegPredicateFailure era
StakeKeyNotRegisteredDELEG Credential 'Staking 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 era
kh <- Decoder s (Credential 'Staking 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 era -> DelegPredicateFailure era
forall era. Credential 'Staking era -> DelegPredicateFailure era
StakeDelegationImpossibleDELEG Credential 'Staking 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
k -> Word -> Decoder s (Int, DelegPredicateFailure era)
forall s a. Word -> Decoder s a
invalidKey Word
k

delegationTransition ::
  Typeable era =>
  TransitionRule (DELEG era)
delegationTransition :: TransitionRule (DELEG era)
delegationTransition = do
  TRC (DelegEnv slot ptr acnt, 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 era
hk StakeCredential era
-> Exp (Sett (StakeCredential era) ()) -> Exp Bool
forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∉ RewardAccounts era -> Exp (Sett (StakeCredential era) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom (DState era -> RewardAccounts era
forall era. DState era -> RewardAccounts era
_rewards State (DELEG era)
DState era
ds)) Bool
-> PredicateFailure (DELEG era) -> Rule (DELEG era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! StakeCredential era -> DelegPredicateFailure era
forall era. Credential 'Staking era -> DelegPredicateFailure era
StakeKeyAlreadyRegisteredDELEG StakeCredential era
hk

      DState era -> F (Clause (DELEG era) 'Transition) (DState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DState era -> F (Clause (DELEG era) 'Transition) (DState era))
-> DState era -> F (Clause (DELEG era) 'Transition) (DState era)
forall a b. (a -> b) -> a -> b
$
        State (DELEG era)
DState era
ds
          { _rewards :: RewardAccounts era
_rewards = Exp (RewardAccounts era) -> RewardAccounts era
forall s t. Embed s t => Exp t -> s
eval (DState era -> RewardAccounts era
forall era. DState era -> RewardAccounts era
_rewards State (DELEG era)
DState era
ds RewardAccounts era
-> Exp (Single (StakeCredential era) Coin)
-> Exp (RewardAccounts 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)
∪ (StakeCredential era
-> Coin -> Exp (Single (StakeCredential era) Coin)
forall k v. Ord k => k -> v -> Exp (Single k v)
singleton StakeCredential era
hk Coin
forall a. Monoid a => a
mempty)),
            _ptrs :: Bimap Ptr (StakeCredential era)
_ptrs = Exp (Bimap Ptr (StakeCredential era))
-> Bimap Ptr (StakeCredential era)
forall s t. Embed s t => Exp t -> s
eval (DState era -> Bimap Ptr (StakeCredential era)
forall era. DState era -> Bimap Ptr (Credential 'Staking era)
_ptrs State (DELEG era)
DState era
ds Bimap Ptr (StakeCredential era)
-> Exp (Single Ptr (StakeCredential era))
-> Exp (Bimap Ptr (StakeCredential 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)
∪ (Ptr
-> StakeCredential era -> Exp (Single Ptr (StakeCredential era))
forall k v. Ord k => k -> v -> Exp (Single k v)
singleton Ptr
ptr StakeCredential era
hk))
          }
    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 era
hk StakeCredential era
-> Exp (Sett (StakeCredential era) ()) -> Exp Bool
forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∈ RewardAccounts era -> Exp (Sett (StakeCredential era) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom (DState era -> RewardAccounts era
forall era. DState era -> RewardAccounts era
_rewards State (DELEG era)
DState era
ds)) Bool
-> PredicateFailure (DELEG era) -> Rule (DELEG era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! StakeCredential era -> DelegPredicateFailure era
forall era. Credential 'Staking era -> DelegPredicateFailure era
StakeKeyNotRegisteredDELEG StakeCredential era
hk

      let rewardCoin :: Maybe Coin
rewardCoin = StakeCredential era -> RewardAccounts era -> Maybe Coin
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup StakeCredential era
hk (DState era -> RewardAccounts era
forall era. DState era -> RewardAccounts era
_rewards State (DELEG era)
DState 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 era -> F (Clause (DELEG era) 'Transition) (DState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DState era -> F (Clause (DELEG era) 'Transition) (DState era))
-> DState era -> F (Clause (DELEG era) 'Transition) (DState era)
forall a b. (a -> b) -> a -> b
$
        State (DELEG era)
DState era
ds
          { _rewards :: RewardAccounts era
_rewards = Exp (RewardAccounts era) -> RewardAccounts era
forall s t. Embed s t => Exp t -> s
eval (StakeCredential era -> Exp (Single (StakeCredential era) ())
forall k. Ord k => k -> Exp (Single k ())
setSingleton StakeCredential era
hk Exp (Single (StakeCredential era) ())
-> RewardAccounts era -> Exp (RewardAccounts era)
forall k (g :: * -> * -> *) s1 s2 (f :: * -> * -> *) v.
(Ord k, Iter g, HasExp s1 (g k ()), HasExp s2 (f k v)) =>
s1 -> s2 -> Exp (f k v)
⋪ DState era -> RewardAccounts era
forall era. DState era -> RewardAccounts era
_rewards State (DELEG era)
DState era
ds),
            _delegations :: Map (StakeCredential era) (KeyHash 'StakePool (Crypto era))
_delegations = Exp (Map (StakeCredential era) (KeyHash 'StakePool (Crypto era)))
-> Map (StakeCredential era) (KeyHash 'StakePool (Crypto era))
forall s t. Embed s t => Exp t -> s
eval (StakeCredential era -> Exp (Single (StakeCredential era) ())
forall k. Ord k => k -> Exp (Single k ())
setSingleton StakeCredential era
hk Exp (Single (StakeCredential era) ())
-> Map (StakeCredential era) (KeyHash 'StakePool (Crypto era))
-> Exp
     (Map (StakeCredential era) (KeyHash 'StakePool (Crypto era)))
forall k (g :: * -> * -> *) s1 s2 (f :: * -> * -> *) v.
(Ord k, Iter g, HasExp s1 (g k ()), HasExp s2 (f k v)) =>
s1 -> s2 -> Exp (f k v)
⋪ DState era
-> Map (StakeCredential era) (KeyHash 'StakePool (Crypto era))
forall era.
DState era
-> Map (Credential 'Staking era) (KeyHash 'StakePool (Crypto era))
_delegations State (DELEG era)
DState era
ds),
            _ptrs :: Bimap Ptr (StakeCredential era)
_ptrs = Exp (Bimap Ptr (StakeCredential era))
-> Bimap Ptr (StakeCredential era)
forall s t. Embed s t => Exp t -> s
eval (DState era -> Bimap Ptr (StakeCredential era)
forall era. DState era -> Bimap Ptr (Credential 'Staking era)
_ptrs State (DELEG era)
DState era
ds Bimap Ptr (StakeCredential era)
-> Exp (Single (StakeCredential era) ())
-> Exp (Bimap Ptr (StakeCredential era))
forall k (g :: * -> * -> *) v s1 (f :: * -> * -> *) s2.
(Ord k, Iter g, Ord v, HasExp s1 (f k v), HasExp s2 (g v ())) =>
s1 -> s2 -> Exp (f k v)
⋫ StakeCredential era -> Exp (Single (StakeCredential era) ())
forall k. Ord k => k -> Exp (Single k ())
setSingleton StakeCredential era
hk)
          }
    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 era
hk StakeCredential era
-> Exp (Sett (StakeCredential era) ()) -> Exp Bool
forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∈ RewardAccounts era -> Exp (Sett (StakeCredential era) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom (DState era -> RewardAccounts era
forall era. DState era -> RewardAccounts era
_rewards State (DELEG era)
DState era
ds)) Bool
-> PredicateFailure (DELEG era) -> Rule (DELEG era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! StakeCredential era -> DelegPredicateFailure era
forall era. Credential 'Staking era -> DelegPredicateFailure era
StakeDelegationImpossibleDELEG StakeCredential era
hk

      DState era -> F (Clause (DELEG era) 'Transition) (DState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DState era -> F (Clause (DELEG era) 'Transition) (DState era))
-> DState era -> F (Clause (DELEG era) 'Transition) (DState era)
forall a b. (a -> b) -> a -> b
$
        State (DELEG era)
DState era
ds
          { _delegations :: Map (StakeCredential era) (KeyHash 'StakePool (Crypto era))
_delegations = Exp (Map (StakeCredential era) (KeyHash 'StakePool (Crypto era)))
-> Map (StakeCredential era) (KeyHash 'StakePool (Crypto era))
forall s t. Embed s t => Exp t -> s
eval (DState era
-> Map (StakeCredential era) (KeyHash 'StakePool (Crypto era))
forall era.
DState era
-> Map (Credential 'Staking era) (KeyHash 'StakePool (Crypto era))
_delegations State (DELEG era)
DState era
ds Map (StakeCredential era) (KeyHash 'StakePool (Crypto era))
-> Exp
     (Single (StakeCredential era) (KeyHash 'StakePool (Crypto era)))
-> Exp
     (Map (StakeCredential era) (KeyHash 'StakePool (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)
⨃ (StakeCredential era
-> KeyHash 'StakePool (Crypto era)
-> Exp
     (Single (StakeCredential era) (KeyHash 'StakePool (Crypto era)))
forall k v. Ord k => k -> v -> Exp (Single k v)
singleton StakeCredential 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 era -> GenDelegs (Crypto era)
forall era. DState era -> GenDelegs (Crypto era)
_genDelegs State (DELEG era)
DState 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 era
-> Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
forall era.
DState era
-> Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
_fGenDelegs State (DELEG era)
DState 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 era -> F (Clause (DELEG era) 'Transition) (DState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DState era -> F (Clause (DELEG era) 'Transition) (DState era))
-> DState era -> F (Clause (DELEG era) 'Transition) (DState era)
forall a b. (a -> b) -> a -> b
$
        State (DELEG era)
DState 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 era
-> Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
forall era.
DState era
-> Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
_fGenDelegs State (DELEG era)
DState 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 credCoinMap) -> 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
      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
$ do
        EpochInfo Identity
ei <- (Globals -> EpochInfo Identity)
-> ReaderT Globals Identity (EpochInfo Identity)
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> EpochInfo Identity
epochInfo
        EpochNo Word64
currEpoch <- HasCallStack => EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
epochInfoEpoch EpochInfo Identity
ei SlotNo
slot
        HasCallStack => EpochInfo Identity -> EpochNo -> ShelleyBase SlotNo
EpochInfo Identity -> EpochNo -> ShelleyBase SlotNo
epochInfoFirst EpochInfo Identity
ei (EpochNo -> ShelleyBase SlotNo) -> EpochNo -> ShelleyBase SlotNo
forall a b. (a -> b) -> a -> b
$ Word64 -> EpochNo
EpochNo (Word64
currEpoch Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1)
      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, RewardAccounts era
instantaneousRewards) =
            case MIRPot
targetPot of
              MIRPot
ReservesMIR -> (AccountState -> Coin
_reserves AccountState
acnt, InstantaneousRewards era -> RewardAccounts era
forall era.
InstantaneousRewards era -> Map (Credential 'Staking era) Coin
iRReserves (InstantaneousRewards era -> RewardAccounts era)
-> InstantaneousRewards era -> RewardAccounts era
forall a b. (a -> b) -> a -> b
$ DState era -> InstantaneousRewards era
forall era. DState era -> InstantaneousRewards era
_irwd State (DELEG era)
DState era
ds)
              MIRPot
TreasuryMIR -> (AccountState -> Coin
_treasury AccountState
acnt, InstantaneousRewards era -> RewardAccounts era
forall era.
InstantaneousRewards era -> Map (Credential 'Staking era) Coin
iRTreasury (InstantaneousRewards era -> RewardAccounts era)
-> InstantaneousRewards era -> RewardAccounts era
forall a b. (a -> b) -> a -> b
$ DState era -> InstantaneousRewards era
forall era. DState era -> InstantaneousRewards era
_irwd State (DELEG era)
DState era
ds)
      let combinedMap :: RewardAccounts era
combinedMap = RewardAccounts era -> RewardAccounts era -> RewardAccounts era
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union RewardAccounts era
credCoinMap RewardAccounts era
instantaneousRewards
          requiredForRewards :: Coin
requiredForRewards = RewardAccounts era -> Coin
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold RewardAccounts era
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 era -> F (Clause (DELEG era) 'Transition) (DState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DState era -> F (Clause (DELEG era) 'Transition) (DState era))
-> DState era -> F (Clause (DELEG era) 'Transition) (DState era)
forall a b. (a -> b) -> a -> b
$ State (DELEG era)
DState era
ds {_irwd :: InstantaneousRewards era
_irwd = (DState era -> InstantaneousRewards era
forall era. DState era -> InstantaneousRewards era
_irwd State (DELEG era)
DState era
ds) {iRReserves :: RewardAccounts era
iRReserves = RewardAccounts era
combinedMap}}
        MIRPot
TreasuryMIR -> DState era -> F (Clause (DELEG era) 'Transition) (DState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DState era -> F (Clause (DELEG era) 'Transition) (DState era))
-> DState era -> F (Clause (DELEG era) 'Transition) (DState era)
forall a b. (a -> b) -> a -> b
$ State (DELEG era)
DState era
ds {_irwd :: InstantaneousRewards era
_irwd = (DState era -> InstantaneousRewards era
forall era. DState era -> InstantaneousRewards era
_irwd State (DELEG era)
DState era
ds) {iRTreasury :: RewardAccounts era
iRTreasury = RewardAccounts era
combinedMap}}
    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 era -> F (Clause (DELEG era) 'Transition) (DState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure State (DELEG era)
DState era
ds