{-# 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 (
  ShelleyNEWEPOCH,
  ShelleyNewEpochEvent (..),
  PredicateFailure,
  updateRewards,
  calculatePoolDistr,
  calculatePoolDistr',
) where

import Cardano.Ledger.BaseTypes (
  BlocksMade (BlocksMade),
  ShelleyBase,
  StrictMaybe (SJust, SNothing),
 )
import Cardano.Ledger.Coin (toDeltaCoin)
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.Shelley.AdaPots (AdaPots, totalAdaPotsES)
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.Era (ShelleyEra, ShelleyNEWEPOCH)
import Cardano.Ledger.Shelley.LedgerState
import Cardano.Ledger.Shelley.Rewards (sumRewards)
import Cardano.Ledger.Shelley.Rules.Epoch
import Cardano.Ledger.Shelley.Rules.Mir (ShelleyMIR, 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) (ShelleyNEWEPOCH era)
  , Embed (EraRule "EPOCH" era) (ShelleyNEWEPOCH 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 (ShelleyNEWEPOCH era)
  where
  type State (ShelleyNEWEPOCH era) = NewEpochState era

  type Signal (ShelleyNEWEPOCH era) = EpochNo

  type Environment (ShelleyNEWEPOCH era) = ()

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

  initialRules :: [InitialRule (ShelleyNEWEPOCH era)]
initialRules =
    [ State (ShelleyNEWEPOCH era) -> InitialRule (ShelleyNEWEPOCH era)
forall a. a -> F (Clause (ShelleyNEWEPOCH era) 'Initial) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (State (ShelleyNEWEPOCH era) -> InitialRule (ShelleyNEWEPOCH era))
-> State (ShelleyNEWEPOCH era) -> InitialRule (ShelleyNEWEPOCH 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
          (Map (KeyHash StakePool) IndividualPoolStake
-> CompactForm Coin -> PoolDistr
PoolDistr Map (KeyHash StakePool) IndividualPoolStake
forall k a. Map k a
Map.empty CompactForm Coin
forall a. Monoid a => a
mempty)
          StashedAVVMAddresses era
forall a. Default a => a
def
    ]

  transitionRules :: [TransitionRule (ShelleyNEWEPOCH era)]
transitionRules = [TransitionRule (ShelleyNEWEPOCH era)
forall era.
(EraTxOut era, EraGov era, EraStake era, EraCertState era,
 Embed (EraRule "MIR" era) (ShelleyNEWEPOCH era),
 Embed (EraRule "EPOCH" era) (ShelleyNEWEPOCH 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 (ShelleyNEWEPOCH era)
newEpochTransition]

newEpochTransition ::
  forall era.
  ( EraTxOut era
  , EraGov era
  , EraStake era
  , EraCertState era
  , Embed (EraRule "MIR" era) (ShelleyNEWEPOCH era)
  , Embed (EraRule "EPOCH" era) (ShelleyNEWEPOCH 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 (ShelleyNEWEPOCH era)
newEpochTransition :: forall era.
(EraTxOut era, EraGov era, EraStake era, EraCertState era,
 Embed (EraRule "MIR" era) (ShelleyNEWEPOCH era),
 Embed (EraRule "EPOCH" era) (ShelleyNEWEPOCH 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 (ShelleyNEWEPOCH era)
newEpochTransition = do
  TRC
    ( _
      , src@(NewEpochState eNoL _ bcur es ru _pd _)
      , eNo
      ) <-
    Rule
  (ShelleyNEWEPOCH era)
  'Transition
  (RuleContext 'Transition (ShelleyNEWEPOCH era))
F (Clause (ShelleyNEWEPOCH era) 'Transition)
  (TRC (ShelleyNEWEPOCH 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 (ShelleyNEWEPOCH era) 'Transition) (EpochState era)
forall a. a -> F (Clause (ShelleyNEWEPOCH 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
  (ShelleyNEWEPOCH era)
  (RewardUpdate, Map (Credential Staking) (Set Reward))
-> Rule
     (ShelleyNEWEPOCH 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 (ShelleyNEWEPOCH era) 'Transition) (EpochState era)
forall era.
(EraGov era, EraCertState era) =>
EpochState era
-> EpochNo
-> RewardUpdate
-> Rule (ShelleyNEWEPOCH era) 'Transition (EpochState era)
updateRewards EpochState era
es EpochNo
Signal (ShelleyNEWEPOCH 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 (ShelleyNEWEPOCH era) rtype ()
tellReward :: forall era (rtype :: RuleType).
(Event (EraRule "RUPD" era) ~ RupdEvent) =>
ShelleyNewEpochEvent era -> Rule (ShelleyNEWEPOCH 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 (ShelleyNEWEPOCH era) rtype) ()
forall a. a -> F (Clause (ShelleyNEWEPOCH era) rtype) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
tellReward ShelleyNewEpochEvent era
x = Event (ShelleyNEWEPOCH era)
-> F (Clause (ShelleyNEWEPOCH era) rtype) ()
forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent Event (ShelleyNEWEPOCH era)
ShelleyNewEpochEvent era
x

instance
  ( STS (ShelleyEPOCH era)
  , Event (EraRule "EPOCH" era) ~ ShelleyEpochEvent era
  ) =>
  Embed (ShelleyEPOCH era) (ShelleyNEWEPOCH era)
  where
  wrapFailed :: PredicateFailure (ShelleyEPOCH era)
-> PredicateFailure (ShelleyNEWEPOCH era)
wrapFailed = \case {}
  wrapEvent :: Event (ShelleyEPOCH era) -> Event (ShelleyNEWEPOCH era)
wrapEvent = Event (EraRule "EPOCH" era) -> ShelleyNewEpochEvent era
Event (ShelleyEPOCH era) -> Event (ShelleyNEWEPOCH 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 (ShelleyMIR era) (ShelleyNEWEPOCH era)
  where
  wrapFailed :: PredicateFailure (ShelleyMIR era)
-> PredicateFailure (ShelleyNEWEPOCH era)
wrapFailed = \case {}
  wrapEvent :: Event (ShelleyMIR era) -> Event (ShelleyNEWEPOCH era)
wrapEvent = Event (EraRule "MIR" era) -> ShelleyNewEpochEvent era
Event (ShelleyMIR era) -> Event (ShelleyNEWEPOCH era)
forall era. Event (EraRule "MIR" era) -> ShelleyNewEpochEvent era
MirEvent

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

updateRewards ::
  (EraGov era, EraCertState era) =>
  EpochState era ->
  EpochNo ->
  RewardUpdate ->
  Rule (ShelleyNEWEPOCH era) 'Transition (EpochState era)
updateRewards :: forall era.
(EraGov era, EraCertState era) =>
EpochState era
-> EpochNo
-> RewardUpdate
-> Rule (ShelleyNEWEPOCH 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 (ShelleyNEWEPOCH era) 'Transition) ()
-> F (Clause (ShelleyNEWEPOCH 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 (ShelleyNEWEPOCH era) 'Transition) ()
forall a. a -> F (Clause (ShelleyNEWEPOCH 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 (ShelleyNEWEPOCH era)
-> F (Clause (ShelleyNEWEPOCH era) 'Transition) ()
forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent (Event (ShelleyNEWEPOCH era)
 -> F (Clause (ShelleyNEWEPOCH era) 'Transition) ())
-> Event (ShelleyNEWEPOCH era)
-> F (Clause (ShelleyNEWEPOCH 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 (ShelleyNEWEPOCH era)
-> F (Clause (ShelleyNEWEPOCH era) 'Transition) ()
forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent (Event (ShelleyNEWEPOCH era)
 -> F (Clause (ShelleyNEWEPOCH era) 'Transition) ())
-> Event (ShelleyNEWEPOCH era)
-> F (Clause (ShelleyNEWEPOCH 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 (ShelleyNEWEPOCH era) 'Transition) (EpochState era)
forall a. a -> F (Clause (ShelleyNEWEPOCH era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure EpochState era
es'