{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Cardano.Ledger.Shelley.Rules.NewEpoch (
  NEWEPOCH,
  ShelleyNewEpochEvent (..),
  updateRewards,
) where

import Cardano.Ledger.BaseTypes (
  BlocksMade (BlocksMade),
  ShelleyBase,
  StrictMaybe (SJust, SNothing),
 )
import Cardano.Ledger.Coin (toDeltaCoin)
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.Rewards (Reward)
import Cardano.Ledger.Shelley.AdaPots (AdaPots, totalAdaPotsES)
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.Era (NEWEPOCH, ShelleyEra)
import Cardano.Ledger.Shelley.LedgerState
import Cardano.Ledger.Shelley.Rewards (sumRewards)
import Cardano.Ledger.Shelley.Rules.Epoch
import Cardano.Ledger.Shelley.Rules.Mir (MIR, ShelleyMirEvent)
import Cardano.Ledger.Shelley.Rules.Rupd (RupdEvent (..))
import Cardano.Ledger.Slot (EpochNo (..))
import Cardano.Ledger.State
import qualified Cardano.Ledger.Val as Val
import Control.DeepSeq (NFData)
import Control.Exception (assert)
import Control.State.Transition
import Data.Default (Default, def)
import qualified Data.Map.Strict as Map
import Data.Set (Set)
import Data.Void (Void)
import GHC.Generics (Generic)
import Lens.Micro ((^.))

data ShelleyNewEpochEvent era
  = DeltaRewardEvent (Event (EraRule "RUPD" era))
  | RestrainedRewards
      EpochNo
      (Map.Map (Credential Staking) (Set Reward))
      (Set (Credential Staking))
  | TotalRewardEvent
      EpochNo
      (Map.Map (Credential Staking) (Set Reward))
  | EpochEvent (Event (EraRule "EPOCH" era))
  | MirEvent (Event (EraRule "MIR" era))
  | TotalAdaPotsEvent AdaPots
  deriving ((forall x.
 ShelleyNewEpochEvent era -> Rep (ShelleyNewEpochEvent era) x)
-> (forall x.
    Rep (ShelleyNewEpochEvent era) x -> ShelleyNewEpochEvent era)
-> Generic (ShelleyNewEpochEvent era)
forall x.
Rep (ShelleyNewEpochEvent era) x -> ShelleyNewEpochEvent era
forall x.
ShelleyNewEpochEvent era -> Rep (ShelleyNewEpochEvent era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyNewEpochEvent era) x -> ShelleyNewEpochEvent era
forall era x.
ShelleyNewEpochEvent era -> Rep (ShelleyNewEpochEvent era) x
$cfrom :: forall era x.
ShelleyNewEpochEvent era -> Rep (ShelleyNewEpochEvent era) x
from :: forall x.
ShelleyNewEpochEvent era -> Rep (ShelleyNewEpochEvent era) x
$cto :: forall era x.
Rep (ShelleyNewEpochEvent era) x -> ShelleyNewEpochEvent era
to :: forall x.
Rep (ShelleyNewEpochEvent era) x -> ShelleyNewEpochEvent era
Generic)

deriving instance
  ( Eq (Event (EraRule "EPOCH" era))
  , Eq (Event (EraRule "MIR" era))
  , Eq (Event (EraRule "RUPD" era))
  ) =>
  Eq (ShelleyNewEpochEvent era)

instance
  ( NFData (Event (EraRule "EPOCH" era))
  , NFData (Event (EraRule "MIR" era))
  , NFData (Event (EraRule "RUPD" era))
  ) =>
  NFData (ShelleyNewEpochEvent era)

type instance EraRuleEvent "NEWEPOCH" ShelleyEra = ShelleyNewEpochEvent ShelleyEra

instance
  ( EraTxOut era
  , EraGov era
  , EraStake era
  , EraCertState era
  , Embed (EraRule "MIR" era) (NEWEPOCH era)
  , Embed (EraRule "EPOCH" era) (NEWEPOCH era)
  , Environment (EraRule "MIR" era) ~ ()
  , State (EraRule "MIR" era) ~ EpochState era
  , Signal (EraRule "MIR" era) ~ ()
  , Event (EraRule "RUPD" era) ~ RupdEvent
  , Environment (EraRule "EPOCH" era) ~ ()
  , State (EraRule "EPOCH" era) ~ EpochState era
  , Signal (EraRule "EPOCH" era) ~ EpochNo
  , Default (EpochState era)
  , Default (State (EraRule "PPUP" era))
  , Default (PParams era)
  , Default (StashedAVVMAddresses era)
  ) =>
  STS (NEWEPOCH era)
  where
  type State (NEWEPOCH era) = NewEpochState era

  type Signal (NEWEPOCH era) = EpochNo

  type Environment (NEWEPOCH era) = ()

  type BaseM (NEWEPOCH era) = ShelleyBase
  type PredicateFailure (NEWEPOCH era) = Void
  type Event (NEWEPOCH era) = ShelleyNewEpochEvent era

  initialRules :: [InitialRule (NEWEPOCH era)]
initialRules =
    [ State (NEWEPOCH era) -> InitialRule (NEWEPOCH era)
forall a. a -> F (Clause (NEWEPOCH era) 'Initial) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (State (NEWEPOCH era) -> InitialRule (NEWEPOCH era))
-> State (NEWEPOCH era) -> InitialRule (NEWEPOCH era)
forall a b. (a -> b) -> a -> b
$
        EpochNo
-> BlocksMade
-> BlocksMade
-> EpochState era
-> StrictMaybe PulsingRewUpdate
-> PoolDistr
-> StashedAVVMAddresses era
-> NewEpochState era
forall era.
EpochNo
-> BlocksMade
-> BlocksMade
-> EpochState era
-> StrictMaybe PulsingRewUpdate
-> PoolDistr
-> StashedAVVMAddresses era
-> NewEpochState era
NewEpochState
          (Word64 -> EpochNo
EpochNo Word64
0)
          (Map (KeyHash StakePool) Natural -> BlocksMade
BlocksMade Map (KeyHash StakePool) Natural
forall k a. Map k a
Map.empty)
          (Map (KeyHash StakePool) Natural -> BlocksMade
BlocksMade Map (KeyHash StakePool) Natural
forall k a. Map k a
Map.empty)
          EpochState era
forall a. Default a => a
def
          StrictMaybe PulsingRewUpdate
forall a. StrictMaybe a
SNothing
          PoolDistr
forall a. Default a => a
def
          StashedAVVMAddresses era
forall a. Default a => a
def
    ]

  transitionRules :: [TransitionRule (NEWEPOCH era)]
transitionRules = [TransitionRule (NEWEPOCH era)
forall era.
(EraTxOut era, EraGov era, EraStake era, EraCertState era,
 Embed (EraRule "MIR" era) (NEWEPOCH era),
 Embed (EraRule "EPOCH" era) (NEWEPOCH era),
 Environment (EraRule "MIR" era) ~ (),
 State (EraRule "MIR" era) ~ EpochState era,
 Signal (EraRule "MIR" era) ~ (),
 Environment (EraRule "EPOCH" era) ~ (),
 State (EraRule "EPOCH" era) ~ EpochState era,
 Signal (EraRule "EPOCH" era) ~ EpochNo, Default (PParams era),
 Default (StashedAVVMAddresses era),
 Event (EraRule "RUPD" era) ~ RupdEvent,
 Default (State (EraRule "PPUP" era))) =>
TransitionRule (NEWEPOCH era)
newEpochTransition]

newEpochTransition ::
  forall era.
  ( EraTxOut era
  , EraGov era
  , EraStake era
  , EraCertState era
  , Embed (EraRule "MIR" era) (NEWEPOCH era)
  , Embed (EraRule "EPOCH" era) (NEWEPOCH era)
  , Environment (EraRule "MIR" era) ~ ()
  , State (EraRule "MIR" era) ~ EpochState era
  , Signal (EraRule "MIR" era) ~ ()
  , Environment (EraRule "EPOCH" era) ~ ()
  , State (EraRule "EPOCH" era) ~ EpochState era
  , Signal (EraRule "EPOCH" era) ~ EpochNo
  , Default (PParams era)
  , Default (StashedAVVMAddresses era)
  , Event (EraRule "RUPD" era) ~ RupdEvent
  , Default (State (EraRule "PPUP" era))
  ) =>
  TransitionRule (NEWEPOCH era)
newEpochTransition :: forall era.
(EraTxOut era, EraGov era, EraStake era, EraCertState era,
 Embed (EraRule "MIR" era) (NEWEPOCH era),
 Embed (EraRule "EPOCH" era) (NEWEPOCH era),
 Environment (EraRule "MIR" era) ~ (),
 State (EraRule "MIR" era) ~ EpochState era,
 Signal (EraRule "MIR" era) ~ (),
 Environment (EraRule "EPOCH" era) ~ (),
 State (EraRule "EPOCH" era) ~ EpochState era,
 Signal (EraRule "EPOCH" era) ~ EpochNo, Default (PParams era),
 Default (StashedAVVMAddresses era),
 Event (EraRule "RUPD" era) ~ RupdEvent,
 Default (State (EraRule "PPUP" era))) =>
TransitionRule (NEWEPOCH era)
newEpochTransition = do
  TRC
    ( _
      , src@(NewEpochState eNoL _ bcur es ru _pd _)
      , eNo
      ) <-
    Rule
  (NEWEPOCH era) 'Transition (RuleContext 'Transition (NEWEPOCH era))
F (Clause (NEWEPOCH era) 'Transition) (TRC (NEWEPOCH era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  if eNo /= succ eNoL
    then pure src
    else do
      es' <- case ru of
        StrictMaybe PulsingRewUpdate
SNothing -> EpochState era
-> F (Clause (NEWEPOCH era) 'Transition) (EpochState era)
forall a. a -> F (Clause (NEWEPOCH era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure EpochState era
es
        SJust p :: PulsingRewUpdate
p@(Pulsing RewardSnapShot
_ Pulser
_) -> do
          (ans, event) <- BaseM
  (NEWEPOCH era)
  (RewardUpdate, Map (Credential Staking) (Set Reward))
-> Rule
     (NEWEPOCH era)
     'Transition
     (RewardUpdate, Map (Credential Staking) (Set Reward))
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (PulsingRewUpdate
-> ShelleyBase
     (RewardUpdate, Map (Credential Staking) (Set Reward))
completeRupd PulsingRewUpdate
p)
          tellReward (DeltaRewardEvent (RupdEvent eNo event))
          updateRewards es eNo ans
        SJust (Complete RewardUpdate
ru') -> EpochState era
-> EpochNo
-> RewardUpdate
-> F (Clause (NEWEPOCH era) 'Transition) (EpochState era)
forall era.
(EraGov era, EraCertState era) =>
EpochState era
-> EpochNo
-> RewardUpdate
-> Rule (NEWEPOCH era) 'Transition (EpochState era)
updateRewards EpochState era
es EpochNo
Signal (NEWEPOCH era)
eNo RewardUpdate
ru'
      es'' <- trans @(EraRule "MIR" era) $ TRC ((), es', ())
      es''' <- trans @(EraRule "EPOCH" era) $ TRC ((), es'', eNo)
      let adaPots = EpochState era -> AdaPots
forall era.
(EraTxOut era, EraGov era, EraCertState era) =>
EpochState era -> AdaPots
totalAdaPotsES EpochState era
es'''
      tellEvent $ TotalAdaPotsEvent adaPots
      let pd' = SnapShots -> PoolDistr
ssStakeMarkPoolDistr (EpochState era -> SnapShots
forall era. EpochState era -> SnapShots
esSnapshots EpochState era
es)
      -- The spec sets pd' with:
      -- pd' = calculatePoolDistr (ssStakeSet $ esSnapshots es'''),
      --
      -- This is equivalent to:
      -- pd' = ssStakeMarkPoolDistr (esSnapshots es)
      --
      -- since:
      --
      -- \* SNAP rotates `ssStakeMark` to `ssStakeSet`, so
      -- \* the `ssStakeSet` snapshot in es''' is `ssStakeMark` in es
      -- \* `ssStakeMarkPoolDistr` is computed by calling `calculatePoolDistr`
      --    on the `ssStakeMark` snapshot at the previous epoch boundary.
      -- \* RUPD does not alter `esSnaphots`
      -- \* MIR does not alter `esSnaphots`
      --
      -- This was done to memoize the per-pool stake distribution.
      -- See ADR-7.
      pure $
        src
          { nesEL = eNo
          , nesBprev = bcur
          , nesBcur = BlocksMade mempty
          , nesEs = es'''
          , nesRu = SNothing
          , nesPd = pd'
          }

-- | tell a RupdEvent as a DeltaRewardEvent only if the map is non-empty
tellReward ::
  Event (EraRule "RUPD" era) ~ RupdEvent =>
  ShelleyNewEpochEvent era ->
  Rule (NEWEPOCH era) rtype ()
tellReward :: forall era (rtype :: RuleType).
(Event (EraRule "RUPD" era) ~ RupdEvent) =>
ShelleyNewEpochEvent era -> Rule (NEWEPOCH era) rtype ()
tellReward (DeltaRewardEvent (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 (NEWEPOCH era) rtype) ()
forall a. a -> F (Clause (NEWEPOCH era) rtype) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
tellReward ShelleyNewEpochEvent era
x = Event (NEWEPOCH era) -> F (Clause (NEWEPOCH era) rtype) ()
forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent Event (NEWEPOCH era)
ShelleyNewEpochEvent era
x

instance
  ( STS (EPOCH era)
  , Event (EraRule "EPOCH" era) ~ ShelleyEpochEvent era
  ) =>
  Embed (EPOCH era) (NEWEPOCH era)
  where
  wrapFailed :: PredicateFailure (EPOCH era) -> PredicateFailure (NEWEPOCH era)
wrapFailed = \case {}
  wrapEvent :: Event (EPOCH era) -> Event (NEWEPOCH era)
wrapEvent = Event (EraRule "EPOCH" era) -> ShelleyNewEpochEvent era
Event (EPOCH era) -> Event (NEWEPOCH era)
forall era. Event (EraRule "EPOCH" era) -> ShelleyNewEpochEvent era
EpochEvent

instance
  ( EraGov era
  , EraCertState era
  , Default (EpochState era)
  , Event (EraRule "MIR" era) ~ ShelleyMirEvent era
  ) =>
  Embed (MIR era) (NEWEPOCH era)
  where
  wrapFailed :: PredicateFailure (MIR era) -> PredicateFailure (NEWEPOCH era)
wrapFailed = \case {}
  wrapEvent :: Event (MIR era) -> Event (NEWEPOCH era)
wrapEvent = Event (EraRule "MIR" era) -> ShelleyNewEpochEvent era
Event (MIR era) -> Event (NEWEPOCH era)
forall era. Event (EraRule "MIR" era) -> ShelleyNewEpochEvent era
MirEvent

-- ===========================================

updateRewards ::
  (EraGov era, EraCertState era) =>
  EpochState era ->
  EpochNo ->
  RewardUpdate ->
  Rule (NEWEPOCH era) 'Transition (EpochState era)
updateRewards :: forall era.
(EraGov era, EraCertState era) =>
EpochState era
-> EpochNo
-> RewardUpdate
-> Rule (NEWEPOCH era) 'Transition (EpochState era)
updateRewards EpochState era
es EpochNo
e ru' :: RewardUpdate
ru'@(RewardUpdate DeltaCoin
dt DeltaCoin
dr Map (Credential Staking) (Set Reward)
rs_ DeltaCoin
df NonMyopic
_) = do
  let totRs :: Coin
totRs = ProtVer -> Map (Credential Staking) (Set Reward) -> Coin
sumRewards (EpochState era
es EpochState era
-> Getting ProtVer (EpochState era) ProtVer -> ProtVer
forall s a. s -> Getting a s a -> a
^. (PParams era -> Const ProtVer (PParams era))
-> EpochState era -> Const ProtVer (EpochState era)
forall era. EraGov era => Lens' (EpochState era) (PParams era)
Lens' (EpochState era) (PParams era)
prevPParamsEpochStateL ((PParams era -> Const ProtVer (PParams era))
 -> EpochState era -> Const ProtVer (EpochState era))
-> ((ProtVer -> Const ProtVer ProtVer)
    -> PParams era -> Const ProtVer (PParams era))
-> Getting ProtVer (EpochState era) ProtVer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProtVer -> Const ProtVer ProtVer)
-> PParams era -> Const ProtVer (PParams era)
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams era) ProtVer
ppProtocolVersionL) Map (Credential Staking) (Set Reward)
rs_
   in Bool
-> F (Clause (NEWEPOCH era) 'Transition) ()
-> F (Clause (NEWEPOCH era) 'Transition) ()
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (DeltaCoin -> Bool
forall t. Val t => t -> Bool
Val.isZero (DeltaCoin
dt DeltaCoin -> DeltaCoin -> DeltaCoin
forall a. Semigroup a => a -> a -> a
<> (DeltaCoin
dr DeltaCoin -> DeltaCoin -> DeltaCoin
forall a. Semigroup a => a -> a -> a
<> Coin -> DeltaCoin
toDeltaCoin Coin
totRs DeltaCoin -> DeltaCoin -> DeltaCoin
forall a. Semigroup a => a -> a -> a
<> DeltaCoin
df))) (() -> F (Clause (NEWEPOCH era) 'Transition) ()
forall a. a -> F (Clause (NEWEPOCH era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
  let !(!EpochState era
es', FilteredRewards era
filtered) = RewardUpdate
-> EpochState era -> (EpochState era, FilteredRewards era)
forall era.
(EraGov era, EraCertState era) =>
RewardUpdate
-> EpochState era -> (EpochState era, FilteredRewards era)
applyRUpdFiltered RewardUpdate
ru' EpochState era
es
  Event (NEWEPOCH era) -> F (Clause (NEWEPOCH era) 'Transition) ()
forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent (Event (NEWEPOCH era) -> F (Clause (NEWEPOCH era) 'Transition) ())
-> Event (NEWEPOCH era) -> F (Clause (NEWEPOCH era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ EpochNo
-> Map (Credential Staking) (Set Reward)
-> Set (Credential Staking)
-> ShelleyNewEpochEvent era
forall era.
EpochNo
-> Map (Credential Staking) (Set Reward)
-> Set (Credential Staking)
-> ShelleyNewEpochEvent era
RestrainedRewards EpochNo
e (FilteredRewards era -> Map (Credential Staking) (Set Reward)
forall era.
FilteredRewards era -> Map (Credential Staking) (Set Reward)
frShelleyIgnored FilteredRewards era
filtered) (FilteredRewards era -> Set (Credential Staking)
forall era. FilteredRewards era -> Set (Credential Staking)
frUnregistered FilteredRewards era
filtered)
  -- This event (which is only generated once per epoch) must be generated even if the
  -- map is empty (db-sync depends on it).
  Event (NEWEPOCH era) -> F (Clause (NEWEPOCH era) 'Transition) ()
forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent (Event (NEWEPOCH era) -> F (Clause (NEWEPOCH era) 'Transition) ())
-> Event (NEWEPOCH era) -> F (Clause (NEWEPOCH era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ EpochNo
-> Map (Credential Staking) (Set Reward)
-> ShelleyNewEpochEvent era
forall era.
EpochNo
-> Map (Credential Staking) (Set Reward)
-> ShelleyNewEpochEvent era
TotalRewardEvent EpochNo
e (FilteredRewards era -> Map (Credential Staking) (Set Reward)
forall era.
FilteredRewards era -> Map (Credential Staking) (Set Reward)
frRegistered FilteredRewards era
filtered)
  EpochState era
-> F (Clause (NEWEPOCH era) 'Transition) (EpochState era)
forall a. a -> F (Clause (NEWEPOCH era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure EpochState era
es'