{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# 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,
  ShelleyNewEpochPredFailure (..),
  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.EpochBoundary
import Cardano.Ledger.PoolDistr (PoolDistr (..))
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, ShelleyMirPredFailure)
import Cardano.Ledger.Shelley.Rules.Rupd (RupdEvent (..))
import Cardano.Ledger.Slot (EpochNo (..))
import qualified Cardano.Ledger.Val as Val
import Control.DeepSeq (NFData)
import Control.State.Transition
import Data.Default (Default, def)
import qualified Data.Map.Strict as Map
import Data.Set (Set)
import GHC.Generics (Generic)
import Lens.Micro ((^.))
import NoThunks.Class (NoThunks (..))

data ShelleyNewEpochPredFailure era
  = EpochFailure (PredicateFailure (EraRule "EPOCH" era)) -- Subtransition Failures
  | CorruptRewardUpdate
      !RewardUpdate -- The reward update which violates an invariant
  | MirFailure (PredicateFailure (EraRule "MIR" era)) -- Subtransition Failures
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyNewEpochPredFailure era) x
-> ShelleyNewEpochPredFailure era
forall era x.
ShelleyNewEpochPredFailure era
-> Rep (ShelleyNewEpochPredFailure era) x
$cto :: forall era x.
Rep (ShelleyNewEpochPredFailure era) x
-> ShelleyNewEpochPredFailure era
$cfrom :: forall era x.
ShelleyNewEpochPredFailure era
-> Rep (ShelleyNewEpochPredFailure era) x
Generic)

deriving stock instance
  ( Show (PredicateFailure (EraRule "EPOCH" era))
  , Show (PredicateFailure (EraRule "MIR" era))
  ) =>
  Show (ShelleyNewEpochPredFailure era)

deriving stock instance
  ( Eq (PredicateFailure (EraRule "EPOCH" era))
  , Eq (PredicateFailure (EraRule "MIR" era))
  ) =>
  Eq (ShelleyNewEpochPredFailure era)

instance
  ( NoThunks (PredicateFailure (EraRule "EPOCH" era))
  , NoThunks (PredicateFailure (EraRule "MIR" era))
  ) =>
  NoThunks (ShelleyNewEpochPredFailure era)

instance
  ( NFData (PredicateFailure (EraRule "EPOCH" era))
  , NFData (PredicateFailure (EraRule "MIR" era))
  ) =>
  NFData (ShelleyNewEpochPredFailure era)

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 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
$cto :: forall era x.
Rep (ShelleyNewEpochEvent era) x -> ShelleyNewEpochEvent era
$cfrom :: forall era x.
ShelleyNewEpochEvent era -> Rep (ShelleyNewEpochEvent era) x
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
  , 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) = ShelleyNewEpochPredFailure era
  type Event (ShelleyNEWEPOCH era) = ShelleyNewEpochEvent era

  initialRules :: [InitialRule (ShelleyNEWEPOCH era)]
initialRules =
    [ forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        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 forall k a. Map k a
Map.empty)
          (Map (KeyHash 'StakePool) Natural -> BlocksMade
BlocksMade forall k a. Map k a
Map.empty)
          forall a. Default a => a
def
          forall a. StrictMaybe a
SNothing
          (Map (KeyHash 'StakePool) IndividualPoolStake
-> CompactForm Coin -> PoolDistr
PoolDistr forall k a. Map k a
Map.empty forall a. Monoid a => a
mempty)
          forall a. Default a => a
def
    ]

  transitionRules :: [TransitionRule (ShelleyNEWEPOCH era)]
transitionRules = [forall era.
(EraTxOut era, EraGov 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
  , 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,
 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
    ( Environment (ShelleyNEWEPOCH era)
_
      , src :: State (ShelleyNEWEPOCH era)
src@(NewEpochState EpochNo
eNoL BlocksMade
_ BlocksMade
bcur EpochState era
es StrictMaybe PulsingRewUpdate
ru PoolDistr
_pd StashedAVVMAddresses era
_)
      , Signal (ShelleyNEWEPOCH era)
eNo
      ) <-
    forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  if Signal (ShelleyNEWEPOCH era)
eNo forall a. Eq a => a -> a -> Bool
/= forall a. Enum a => a -> a
succ EpochNo
eNoL
    then forall (f :: * -> *) a. Applicative f => a -> f a
pure State (ShelleyNEWEPOCH era)
src
    else do
      EpochState era
es' <- case StrictMaybe PulsingRewUpdate
ru of
        StrictMaybe PulsingRewUpdate
SNothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure EpochState era
es
        SJust p :: PulsingRewUpdate
p@(Pulsing RewardSnapShot
_ Pulser
_) -> do
          (RewardUpdate
ans, Map (Credential 'Staking) (Set Reward)
event) <- 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)
          forall era (rtype :: RuleType).
(Event (EraRule "RUPD" era) ~ RupdEvent) =>
ShelleyNewEpochEvent era -> Rule (ShelleyNEWEPOCH era) rtype ()
tellReward (forall era. Event (EraRule "RUPD" era) -> ShelleyNewEpochEvent era
DeltaRewardEvent (EpochNo -> Map (Credential 'Staking) (Set Reward) -> RupdEvent
RupdEvent Signal (ShelleyNEWEPOCH era)
eNo Map (Credential 'Staking) (Set Reward)
event))
          forall era.
EraGov era =>
EpochState era
-> EpochNo
-> RewardUpdate
-> Rule (ShelleyNEWEPOCH era) 'Transition (EpochState era)
updateRewards EpochState era
es Signal (ShelleyNEWEPOCH era)
eNo RewardUpdate
ans
        SJust (Complete RewardUpdate
ru') -> forall era.
EraGov era =>
EpochState era
-> EpochNo
-> RewardUpdate
-> Rule (ShelleyNEWEPOCH era) 'Transition (EpochState era)
updateRewards EpochState era
es Signal (ShelleyNEWEPOCH era)
eNo RewardUpdate
ru'
      EpochState era
es'' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "MIR" era) forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC ((), EpochState era
es', ())
      EpochState era
es''' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "EPOCH" era) forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC ((), EpochState era
es'', Signal (ShelleyNEWEPOCH era)
eNo)
      let adaPots :: AdaPots
adaPots = forall era. (EraTxOut era, EraGov era) => EpochState era -> AdaPots
totalAdaPotsES EpochState era
es'''
      forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent forall a b. (a -> b) -> a -> b
$ forall era. AdaPots -> ShelleyNewEpochEvent era
TotalAdaPotsEvent AdaPots
adaPots
      let pd' :: PoolDistr
pd' = SnapShots -> PoolDistr
ssStakeMarkPoolDistr (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.
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        State (ShelleyNEWEPOCH era)
src
          { nesEL :: EpochNo
nesEL = Signal (ShelleyNEWEPOCH era)
eNo
          , nesBprev :: BlocksMade
nesBprev = BlocksMade
bcur
          , nesBcur :: BlocksMade
nesBcur = Map (KeyHash 'StakePool) Natural -> BlocksMade
BlocksMade forall a. Monoid a => a
mempty
          , nesEs :: EpochState era
nesEs = EpochState era
es'''
          , nesRu :: StrictMaybe PulsingRewUpdate
nesRu = forall a. StrictMaybe a
SNothing
          , nesPd :: PoolDistr
nesPd = PoolDistr
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)) | forall k a. Map k a -> Bool
Map.null Map (Credential 'Staking) (Set Reward)
m = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
tellReward ShelleyNewEpochEvent era
x = forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent ShelleyNewEpochEvent era
x

instance
  ( STS (ShelleyEPOCH era)
  , PredicateFailure (EraRule "EPOCH" era) ~ ShelleyEpochPredFailure era
  , Event (EraRule "EPOCH" era) ~ ShelleyEpochEvent era
  ) =>
  Embed (ShelleyEPOCH era) (ShelleyNEWEPOCH era)
  where
  wrapFailed :: PredicateFailure (ShelleyEPOCH era)
-> PredicateFailure (ShelleyNEWEPOCH era)
wrapFailed = forall era.
PredicateFailure (EraRule "EPOCH" era)
-> ShelleyNewEpochPredFailure era
EpochFailure
  wrapEvent :: Event (ShelleyEPOCH era) -> Event (ShelleyNEWEPOCH era)
wrapEvent = forall era. Event (EraRule "EPOCH" era) -> ShelleyNewEpochEvent era
EpochEvent

instance
  ( EraGov era
  , Default (EpochState era)
  , PredicateFailure (EraRule "MIR" era) ~ ShelleyMirPredFailure era
  , Event (EraRule "MIR" era) ~ ShelleyMirEvent era
  ) =>
  Embed (ShelleyMIR era) (ShelleyNEWEPOCH era)
  where
  wrapFailed :: PredicateFailure (ShelleyMIR era)
-> PredicateFailure (ShelleyNEWEPOCH era)
wrapFailed = forall era.
PredicateFailure (EraRule "MIR" era)
-> ShelleyNewEpochPredFailure era
MirFailure
  wrapEvent :: Event (ShelleyMIR era) -> Event (ShelleyNEWEPOCH era)
wrapEvent = forall era. Event (EraRule "MIR" era) -> ShelleyNewEpochEvent era
MirEvent

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

updateRewards ::
  EraGov era =>
  EpochState era ->
  EpochNo ->
  RewardUpdate ->
  Rule (ShelleyNEWEPOCH era) 'Transition (EpochState era)
updateRewards :: forall era.
EraGov 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 forall s a. s -> Getting a s a -> a
^. forall era. EraGov era => Lens' (EpochState era) (PParams era)
prevPParamsEpochStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraPParams era => Lens' (PParams era) ProtVer
ppProtocolVersionL) Map (Credential 'Staking) (Set Reward)
rs_
  forall t. Val t => t -> Bool
Val.isZero (DeltaCoin
dt forall a. Semigroup a => a -> a -> a
<> (DeltaCoin
dr forall a. Semigroup a => a -> a -> a
<> Coin -> DeltaCoin
toDeltaCoin Coin
totRs forall a. Semigroup a => a -> a -> a
<> DeltaCoin
df)) forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era. RewardUpdate -> ShelleyNewEpochPredFailure era
CorruptRewardUpdate RewardUpdate
ru'
  let !(!EpochState era
es', FilteredRewards era
filtered) = forall era.
EraGov era =>
RewardUpdate
-> EpochState era -> (EpochState era, FilteredRewards era)
applyRUpdFiltered RewardUpdate
ru' EpochState era
es
  forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent forall a b. (a -> b) -> a -> b
$ forall era.
EpochNo
-> Map (Credential 'Staking) (Set Reward)
-> Set (Credential 'Staking)
-> ShelleyNewEpochEvent era
RestrainedRewards EpochNo
e (forall era.
FilteredRewards era -> Map (Credential 'Staking) (Set Reward)
frShelleyIgnored FilteredRewards era
filtered) (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).
  forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent forall a b. (a -> b) -> a -> b
$ forall era.
EpochNo
-> Map (Credential 'Staking) (Set Reward)
-> ShelleyNewEpochEvent era
TotalRewardEvent EpochNo
e (forall era.
FilteredRewards era -> Map (Credential 'Staking) (Set Reward)
frRegistered FilteredRewards era
filtered)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure EpochState era
es'