{-# 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 (
  AccountState (..),
  DState (..),
  FutureGenDeleg (..),
  InstantaneousRewards (..),
  availableAfterMIR,
  delegations,
  dsFutureGenDelegs,
  dsGenDelegs,
  dsIRewards,
  rewards,
 )
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 -> AccountState
acnt_ :: !AccountState
  , forall era. DelegEnv era -> PParams era
ppDE :: !(PParams era) -- The protocol parameters are only used for the HardFork mechanism
  }
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x. Rep (DelegEnv era) x -> DelegEnv era
forall era x. DelegEnv era -> Rep (DelegEnv era) x
$cto :: forall era x. Rep (DelegEnv era) x -> DelegEnv era
$cfrom :: forall era x. DelegEnv era -> Rep (DelegEnv era) x
Generic)

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

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

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

data ShelleyDelegPredFailure era
  = StakeKeyAlreadyRegisteredDELEG
      !(Credential 'Staking) -- 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
forall era. Int -> ShelleyDelegPredFailure era -> ShowS
forall era. [ShelleyDelegPredFailure era] -> ShowS
forall era. ShelleyDelegPredFailure era -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ShelleyDelegPredFailure era] -> ShowS
$cshowList :: forall era. [ShelleyDelegPredFailure era] -> ShowS
show :: ShelleyDelegPredFailure era -> String
$cshow :: forall era. ShelleyDelegPredFailure era -> String
showsPrec :: Int -> ShelleyDelegPredFailure era -> ShowS
$cshowsPrec :: forall era. Int -> ShelleyDelegPredFailure era -> ShowS
Show, ShelleyDelegPredFailure era -> ShelleyDelegPredFailure era -> Bool
forall era.
ShelleyDelegPredFailure era -> ShelleyDelegPredFailure era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ShelleyDelegPredFailure era -> ShelleyDelegPredFailure era -> Bool
$c/= :: forall era.
ShelleyDelegPredFailure era -> ShelleyDelegPredFailure era -> Bool
== :: ShelleyDelegPredFailure era -> ShelleyDelegPredFailure era -> Bool
$c== :: forall era.
ShelleyDelegPredFailure era -> ShelleyDelegPredFailure era -> Bool
Eq, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyDelegPredFailure era) x -> ShelleyDelegPredFailure era
forall era x.
ShelleyDelegPredFailure era -> Rep (ShelleyDelegPredFailure era) x
$cto :: forall era x.
Rep (ShelleyDelegPredFailure era) x -> ShelleyDelegPredFailure era
$cfrom :: forall era x.
ShelleyDelegPredFailure era -> Rep (ShelleyDelegPredFailure era) x
Generic)

type instance EraRuleFailure "DELEG" ShelleyEra = ShelleyDelegPredFailure ShelleyEra

instance InjectRuleFailure "DELEG" ShelleyDelegPredFailure ShelleyEra

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

instance NFData (ShelleyDelegEvent era)

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

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

instance NoThunks (ShelleyDelegPredFailure era)

instance NFData (ShelleyDelegPredFailure era)

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

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

delegationTransition ::
  (ShelleyEraTxCert era, EraPParams era, ProtVerAtMost era 8) =>
  TransitionRule (ShelleyDELEG era)
delegationTransition :: forall era.
(ShelleyEraTxCert era, EraPParams era, ProtVerAtMost era 8) =>
TransitionRule (ShelleyDELEG era)
delegationTransition = do
  TRC (DelegEnv SlotNo
slot EpochNo
epochNo Ptr
ptr AccountState
acnt PParams era
pp, State (ShelleyDELEG era)
ds, Signal (ShelleyDELEG era)
c) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  let pv :: ProtVer
pv = PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) ProtVer
ppProtocolVersionL
  case Signal (ShelleyDELEG era)
c of
    RegTxCert Credential 'Staking
hk -> do
      -- (hk ∉ dom (rewards ds))
      forall k v. k -> UView k v -> Bool
UM.notMember Credential 'Staking
hk (forall era. DState era -> UView (Credential 'Staking) RDPair
rewards State (ShelleyDELEG era)
ds) forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era. Credential 'Staking -> ShelleyDelegPredFailure era
StakeKeyAlreadyRegisteredDELEG Credential 'Staking
hk
      let u1 :: UMap
u1 = forall era. DState era -> UMap
dsUnified State (ShelleyDELEG era)
ds
          deposit :: CompactForm Coin
deposit = HasCallStack => Coin -> CompactForm Coin
compactCoinOrError (PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) Coin
ppKeyDepositL)
          u2 :: UMap
u2 = UMap -> UView (Credential 'Staking) RDPair
RewDepUView UMap
u1 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 forall k v. UView k v -> (k, v) -> UMap
UM.∪ (Ptr
ptr, Credential 'Staking
hk)
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (State (ShelleyDELEG era)
ds {dsUnified :: UMap
dsUnified = UMap
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 (forall era. DState era -> UMap
dsUnified State (ShelleyDELEG era)
ds)
          checkStakeKeyHasZeroRewardBalance :: Maybe Coin
checkStakeKeyHasZeroRewardBalance = do
            UM.UMElem (SJust RDPair
rd) Set Ptr
_ StrictMaybe (KeyHash 'StakePool)
_ StrictMaybe DRep
_ <- Maybe UMElem
mUMElem
            forall (f :: * -> *). Alternative f => Bool -> f ()
guard (RDPair -> CompactForm Coin
UM.rdReward RDPair
rd forall a. Eq a => a -> a -> Bool
/= forall a. Monoid a => a
mempty)
            forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Compactible a => CompactForm a -> a
UM.fromCompact (RDPair -> CompactForm Coin
UM.rdReward RDPair
rd)
      forall a. Maybe a -> Bool
isJust Maybe UMElem
mUMElem forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era. Credential 'Staking -> ShelleyDelegPredFailure era
StakeKeyNotRegisteredDELEG Credential 'Staking
cred
      forall a sts (ctx :: RuleType).
Maybe a -> (a -> PredicateFailure sts) -> Rule sts ctx ()
failOnJust Maybe Coin
checkStakeKeyHasZeroRewardBalance forall era. Coin -> ShelleyDelegPredFailure era
StakeKeyNonZeroAccountBalanceDELEG
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ State (ShelleyDELEG era)
ds {dsUnified :: UMap
dsUnified = UMap
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))
      forall k v. k -> UView k v -> Bool
UM.member Credential 'Staking
hk (forall era. DState era -> UView (Credential 'Staking) RDPair
rewards State (ShelleyDELEG era)
ds) forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era. Credential 'Staking -> ShelleyDelegPredFailure era
StakeDelegationImpossibleDELEG Credential 'Staking
hk

      forall (f :: * -> *) a. Applicative f => a -> f a
pure (State (ShelleyDELEG era)
ds {dsUnified :: UMap
dsUnified = forall era.
DState era -> UView (Credential 'Staking) (KeyHash 'StakePool)
delegations State (ShelleyDELEG era)
ds forall k v. UView k v -> Map k v -> UMap
UM.⨃ forall k a. k -> a -> Map k a
Map.singleton Credential 'Staking
hk KeyHash 'StakePool
dpool})
    GenesisDelegTxCert KeyHash 'Genesis
gkh KeyHash 'GenesisDelegate
vkh VRFVerKeyHash 'GenDelegVRF
vrf -> do
      Word64
sp <- forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> Word64
stabilityWindow
      -- note that pattern match is used instead of genesisDeleg, as in the spec
      let s' :: SlotNo
s' = SlotNo
slot SlotNo -> Duration -> SlotNo
+* Word64 -> Duration
Duration Word64
sp
          GenDelegs Map (KeyHash 'Genesis) GenDelegPair
genDelegs = forall era. DState era -> GenDelegs
dsGenDelegs State (ShelleyDELEG era)
ds

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

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

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

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

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

checkSlotNotTooLate ::
  (ShelleyEraTxCert era, EraPParams era, ProtVerAtMost era 8) =>
  SlotNo ->
  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 <- forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> Word64
stabilityWindow
  EpochInfo Identity
ei <- forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> EpochInfo Identity
epochInfoPure
  let firstSlot :: SlotNo
firstSlot = HasCallStack => 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)
  forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent (forall era. EpochNo -> ShelleyDelegEvent era
DelegNewEpoch EpochNo
newEpoch)
  SlotNo
slot forall a. Ord a => a -> a -> Bool
< SlotNo
tooLate forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era. Mismatch 'RelLT SlotNo -> ShelleyDelegPredFailure era
MIRCertificateTooLateinEpochDELEG (forall (r :: Relation) a. a -> a -> Mismatch r a
Mismatch SlotNo
slot SlotNo
tooLate)

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