{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE EmptyDataDeriving #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Cardano.Ledger.Shelley.Rules.Rupd (
ShelleyRUPD,
RupdEnv (..),
PredicateFailure,
epochInfoRange,
PulsingRewUpdate (..),
startStep,
pulseStep,
completeStep,
lift,
Identity (..),
RupdEvent (..),
) where
import Cardano.Ledger.BaseTypes (
BlocksMade,
ShelleyBase,
StrictMaybe (..),
activeSlotCoeff,
epochInfoPure,
maxLovelaceSupply,
randomnessStabilisationWindow,
securityParameter,
)
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Core
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.Shelley.Era (ShelleyRUPD)
import Cardano.Ledger.Shelley.Governance (EraGov)
import Cardano.Ledger.Shelley.LedgerState (
EpochState,
PulsingRewUpdate (..),
completeStep,
pulseStep,
startStep,
)
import Cardano.Ledger.Slot (
Duration (..),
EpochNo (..),
SlotNo,
epochInfoEpoch,
epochInfoFirst,
epochInfoSize,
(+*),
)
import Cardano.Ledger.State (EraCertState)
import Cardano.Slotting.EpochInfo.API (epochInfoRange)
import Control.DeepSeq (NFData)
import Control.Monad.Identity (Identity (..))
import Control.Monad.Trans (lift)
import Control.Monad.Trans.Reader (asks)
import Control.State.Transition (
Rule,
STS (..),
TRC (..),
TransitionRule,
judgmentContext,
liftSTS,
tellEvent,
)
import qualified Data.Map.Strict as Map
import Data.Set (Set)
import Data.Void (Void)
import GHC.Generics (Generic)
data RupdEnv era
= RupdEnv BlocksMade (EpochState era)
instance
( Era era
, EraGov era
, EraCertState era
) =>
STS (ShelleyRUPD era)
where
type State (ShelleyRUPD era) = StrictMaybe PulsingRewUpdate
type Signal (ShelleyRUPD era) = SlotNo
type Environment (ShelleyRUPD era) = RupdEnv era
type BaseM (ShelleyRUPD era) = ShelleyBase
type PredicateFailure (ShelleyRUPD era) = Void
type Event (ShelleyRUPD era) = RupdEvent
initialRules :: [InitialRule (ShelleyRUPD era)]
initialRules = [StrictMaybe PulsingRewUpdate
-> F (Clause (ShelleyRUPD era) 'Initial)
(StrictMaybe PulsingRewUpdate)
forall a. a -> F (Clause (ShelleyRUPD era) 'Initial) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure StrictMaybe PulsingRewUpdate
forall a. StrictMaybe a
SNothing]
transitionRules :: [TransitionRule (ShelleyRUPD era)]
transitionRules = [TransitionRule (ShelleyRUPD era)
forall era.
(EraGov era, EraCertState era) =>
TransitionRule (ShelleyRUPD era)
rupdTransition]
data RupdEvent
= RupdEvent
!EpochNo
!(Map.Map (Credential Staking) (Set Reward))
deriving ((forall x. RupdEvent -> Rep RupdEvent x)
-> (forall x. Rep RupdEvent x -> RupdEvent) -> Generic RupdEvent
forall x. Rep RupdEvent x -> RupdEvent
forall x. RupdEvent -> Rep RupdEvent x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. RupdEvent -> Rep RupdEvent x
from :: forall x. RupdEvent -> Rep RupdEvent x
$cto :: forall x. Rep RupdEvent x -> RupdEvent
to :: forall x. Rep RupdEvent x -> RupdEvent
Generic, RupdEvent -> RupdEvent -> Bool
(RupdEvent -> RupdEvent -> Bool)
-> (RupdEvent -> RupdEvent -> Bool) -> Eq RupdEvent
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: RupdEvent -> RupdEvent -> Bool
== :: RupdEvent -> RupdEvent -> Bool
$c/= :: RupdEvent -> RupdEvent -> Bool
/= :: RupdEvent -> RupdEvent -> Bool
Eq)
instance NFData RupdEvent
tellRupd :: String -> RupdEvent -> Rule (ShelleyRUPD era) rtype ()
tellRupd :: forall era (rtype :: RuleType).
String -> RupdEvent -> Rule (ShelleyRUPD era) rtype ()
tellRupd String
_ (RupdEvent EpochNo
_ Map (Credential Staking) (Set Reward)
m) | Map (Credential Staking) (Set Reward) -> Bool
forall k a. Map k a -> Bool
Map.null Map (Credential Staking) (Set Reward)
m = () -> F (Clause (ShelleyRUPD era) rtype) ()
forall a. a -> F (Clause (ShelleyRUPD era) rtype) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
tellRupd String
_message RupdEvent
x = Event (ShelleyRUPD era) -> F (Clause (ShelleyRUPD era) rtype) ()
forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent Event (ShelleyRUPD era)
RupdEvent
x
data RewardTiming = RewardsTooEarly | RewardsJustRight | RewardsTooLate
determineRewardTiming :: SlotNo -> SlotNo -> SlotNo -> RewardTiming
determineRewardTiming :: SlotNo -> SlotNo -> SlotNo -> RewardTiming
determineRewardTiming SlotNo
currentSlot SlotNo
startAfterSlot SlotNo
endSlot
| SlotNo
currentSlot SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
> SlotNo
endSlot = RewardTiming
RewardsTooLate
| SlotNo
currentSlot SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
<= SlotNo
startAfterSlot = RewardTiming
RewardsTooEarly
| Bool
otherwise = RewardTiming
RewardsJustRight
rupdTransition :: (EraGov era, EraCertState era) => TransitionRule (ShelleyRUPD era)
rupdTransition :: forall era.
(EraGov era, EraCertState era) =>
TransitionRule (ShelleyRUPD era)
rupdTransition = do
TRC (RupdEnv b es, ru, s) <- Rule
(ShelleyRUPD era)
'Transition
(RuleContext 'Transition (ShelleyRUPD era))
F (Clause (ShelleyRUPD era) 'Transition) (TRC (ShelleyRUPD era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
(slotsPerEpoch, slot, slotForce, maxLL, asc, k, e) <- liftSTS $ do
ei <- asks epochInfoPure
sr <- asks randomnessStabilisationWindow
let e = HasCallStack => EpochInfo Identity -> SlotNo -> EpochNo
EpochInfo Identity -> SlotNo -> EpochNo
epochInfoEpoch EpochInfo Identity
ei SlotNo
Signal (ShelleyRUPD era)
s
slotsPerEpoch = HasCallStack => EpochInfo Identity -> EpochNo -> EpochSize
EpochInfo Identity -> EpochNo -> EpochSize
epochInfoSize EpochInfo Identity
ei EpochNo
e
slot = HasCallStack => EpochInfo Identity -> EpochNo -> SlotNo
EpochInfo Identity -> EpochNo -> SlotNo
epochInfoFirst EpochInfo Identity
ei EpochNo
e SlotNo -> Duration -> SlotNo
+* Word64 -> Duration
Duration Word64
sr
maxLL <- asks maxLovelaceSupply
asc <- asks activeSlotCoeff
k <- asks securityParameter
return (slotsPerEpoch, slot, slot +* Duration sr, maxLL, asc, k, e)
let maxsupply = Integer -> Coin
Coin (Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
maxLL)
case determineRewardTiming s slot slotForce of
RewardTiming
RewardsTooEarly -> StrictMaybe PulsingRewUpdate
-> F (Clause (ShelleyRUPD era) 'Transition)
(StrictMaybe PulsingRewUpdate)
forall a. a -> F (Clause (ShelleyRUPD era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure StrictMaybe PulsingRewUpdate
forall a. StrictMaybe a
SNothing
RewardTiming
RewardsJustRight ->
case State (ShelleyRUPD era)
ru of
StrictMaybe PulsingRewUpdate
State (ShelleyRUPD era)
SNothing ->
(StrictMaybe PulsingRewUpdate
-> F (Clause (ShelleyRUPD era) 'Transition)
(StrictMaybe PulsingRewUpdate)
forall a. a -> F (Clause (ShelleyRUPD era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StrictMaybe PulsingRewUpdate
-> F (Clause (ShelleyRUPD era) 'Transition)
(StrictMaybe PulsingRewUpdate))
-> (PulsingRewUpdate -> StrictMaybe PulsingRewUpdate)
-> PulsingRewUpdate
-> F (Clause (ShelleyRUPD era) 'Transition)
(StrictMaybe PulsingRewUpdate)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PulsingRewUpdate -> StrictMaybe PulsingRewUpdate
forall a. a -> StrictMaybe a
SJust) (EpochSize
-> BlocksMade
-> EpochState era
-> Coin
-> ActiveSlotCoeff
-> NonZero Word64
-> PulsingRewUpdate
forall era.
(EraGov era, EraCertState era) =>
EpochSize
-> BlocksMade
-> EpochState era
-> Coin
-> ActiveSlotCoeff
-> NonZero Word64
-> PulsingRewUpdate
startStep EpochSize
slotsPerEpoch BlocksMade
b EpochState era
es Coin
maxsupply ActiveSlotCoeff
asc NonZero Word64
k)
(SJust p :: PulsingRewUpdate
p@(Pulsing RewardSnapShot
_ Pulser
_)) -> do
(ans, event) <- BaseM
(ShelleyRUPD era)
(PulsingRewUpdate, Map (Credential Staking) (Set Reward))
-> Rule
(ShelleyRUPD era)
'Transition
(PulsingRewUpdate, Map (Credential Staking) (Set Reward))
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM
(ShelleyRUPD era)
(PulsingRewUpdate, Map (Credential Staking) (Set Reward))
-> Rule
(ShelleyRUPD era)
'Transition
(PulsingRewUpdate, Map (Credential Staking) (Set Reward)))
-> BaseM
(ShelleyRUPD era)
(PulsingRewUpdate, Map (Credential Staking) (Set Reward))
-> Rule
(ShelleyRUPD era)
'Transition
(PulsingRewUpdate, Map (Credential Staking) (Set Reward))
forall a b. (a -> b) -> a -> b
$ PulsingRewUpdate
-> ShelleyBase
(PulsingRewUpdate, Map (Credential Staking) (Set Reward))
pulseStep PulsingRewUpdate
p
tellRupd "Pulsing Rupd" (RupdEvent (succ e) event)
pure (SJust ans)
(SJust p :: PulsingRewUpdate
p@(Complete RewardUpdate
_)) -> StrictMaybe PulsingRewUpdate
-> F (Clause (ShelleyRUPD era) 'Transition)
(StrictMaybe PulsingRewUpdate)
forall a. a -> F (Clause (ShelleyRUPD era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PulsingRewUpdate -> StrictMaybe PulsingRewUpdate
forall a. a -> StrictMaybe a
SJust PulsingRewUpdate
p)
RewardTiming
RewardsTooLate ->
case State (ShelleyRUPD era)
ru of
StrictMaybe PulsingRewUpdate
State (ShelleyRUPD era)
SNothing -> do
let pulser :: PulsingRewUpdate
pulser = EpochSize
-> BlocksMade
-> EpochState era
-> Coin
-> ActiveSlotCoeff
-> NonZero Word64
-> PulsingRewUpdate
forall era.
(EraGov era, EraCertState era) =>
EpochSize
-> BlocksMade
-> EpochState era
-> Coin
-> ActiveSlotCoeff
-> NonZero Word64
-> PulsingRewUpdate
startStep EpochSize
slotsPerEpoch BlocksMade
b EpochState era
es Coin
maxsupply ActiveSlotCoeff
asc NonZero Word64
k
(reward, event) <- BaseM
(ShelleyRUPD era)
(PulsingRewUpdate, Map (Credential Staking) (Set Reward))
-> Rule
(ShelleyRUPD era)
'Transition
(PulsingRewUpdate, Map (Credential Staking) (Set Reward))
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM
(ShelleyRUPD era)
(PulsingRewUpdate, Map (Credential Staking) (Set Reward))
-> Rule
(ShelleyRUPD era)
'Transition
(PulsingRewUpdate, Map (Credential Staking) (Set Reward)))
-> BaseM
(ShelleyRUPD era)
(PulsingRewUpdate, Map (Credential Staking) (Set Reward))
-> Rule
(ShelleyRUPD era)
'Transition
(PulsingRewUpdate, Map (Credential Staking) (Set Reward))
forall a b. (a -> b) -> a -> b
$ PulsingRewUpdate
-> ShelleyBase
(PulsingRewUpdate, Map (Credential Staking) (Set Reward))
completeStep PulsingRewUpdate
pulser
tellRupd "Starting too late" (RupdEvent (succ e) event)
pure (SJust reward)
SJust p :: PulsingRewUpdate
p@(Pulsing RewardSnapShot
_ Pulser
_) -> do
(reward, event) <- BaseM
(ShelleyRUPD era)
(PulsingRewUpdate, Map (Credential Staking) (Set Reward))
-> Rule
(ShelleyRUPD era)
'Transition
(PulsingRewUpdate, Map (Credential Staking) (Set Reward))
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM
(ShelleyRUPD era)
(PulsingRewUpdate, Map (Credential Staking) (Set Reward))
-> Rule
(ShelleyRUPD era)
'Transition
(PulsingRewUpdate, Map (Credential Staking) (Set Reward)))
-> BaseM
(ShelleyRUPD era)
(PulsingRewUpdate, Map (Credential Staking) (Set Reward))
-> Rule
(ShelleyRUPD era)
'Transition
(PulsingRewUpdate, Map (Credential Staking) (Set Reward))
forall a b. (a -> b) -> a -> b
$ PulsingRewUpdate
-> ShelleyBase
(PulsingRewUpdate, Map (Credential Staking) (Set Reward))
completeStep PulsingRewUpdate
p
tellRupd "Completing too late" (RupdEvent (succ e) event)
pure (SJust reward)
complete :: State (ShelleyRUPD era)
complete@(SJust (Complete RewardUpdate
_)) -> StrictMaybe PulsingRewUpdate
-> F (Clause (ShelleyRUPD era) 'Transition)
(StrictMaybe PulsingRewUpdate)
forall a. a -> F (Clause (ShelleyRUPD era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure StrictMaybe PulsingRewUpdate
State (ShelleyRUPD era)
complete