{-# 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.Keys (KeyRole (Staking))
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.Class (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 (EraCrypto era)) -- 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 (EraCrypto era)) (Set (Reward (EraCrypto era))))
      (Set (Credential 'Staking (EraCrypto era)))
  | TotalRewardEvent
      EpochNo
      (Map.Map (Credential 'Staking (EraCrypto era)) (Set (Reward (EraCrypto era))))
  | 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 c) = ShelleyNewEpochEvent (ShelleyEra c)

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 (EraCrypto era)
  , 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 (EraCrypto era)
-> BlocksMade (EraCrypto era)
-> EpochState era
-> StrictMaybe (PulsingRewUpdate (EraCrypto era))
-> PoolDistr (EraCrypto era)
-> StashedAVVMAddresses era
-> NewEpochState era
NewEpochState
          (Word64 -> EpochNo
EpochNo Word64
0)
          (forall c. Map (KeyHash 'StakePool c) Natural -> BlocksMade c
BlocksMade forall k a. Map k a
Map.empty)
          (forall c. Map (KeyHash 'StakePool c) Natural -> BlocksMade c
BlocksMade forall k a. Map k a
Map.empty)
          forall a. Default a => a
def
          forall a. StrictMaybe a
SNothing
          (forall c.
Map (KeyHash 'StakePool c) (IndividualPoolStake c)
-> CompactForm Coin -> PoolDistr c
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 (EraCrypto era),
 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 (EraCrypto era)
  , 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 (EraCrypto era),
 Default (State (EraRule "PPUP" era))) =>
TransitionRule (ShelleyNEWEPOCH era)
newEpochTransition = do
  TRC
    ( Environment (ShelleyNEWEPOCH era)
_
      , src :: State (ShelleyNEWEPOCH era)
src@(NewEpochState EpochNo
eNoL BlocksMade (EraCrypto era)
_ BlocksMade (EraCrypto era)
bcur EpochState era
es StrictMaybe (PulsingRewUpdate (EraCrypto era))
ru PoolDistr (EraCrypto era)
_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 (EraCrypto era))
ru of
        StrictMaybe (PulsingRewUpdate (EraCrypto era))
SNothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure EpochState era
es
        SJust p :: PulsingRewUpdate (EraCrypto era)
p@(Pulsing RewardSnapShot (EraCrypto era)
_ Pulser (EraCrypto era)
_) -> do
          (RewardUpdate (EraCrypto era)
ans, Map
  (Credential 'Staking (EraCrypto era))
  (Set (Reward (EraCrypto era)))
event) <- forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (forall c.
PulsingRewUpdate c -> ShelleyBase (RewardUpdate c, RewardEvent c)
completeRupd PulsingRewUpdate (EraCrypto era)
p)
          forall era (rtype :: RuleType).
(Event (EraRule "RUPD" era) ~ RupdEvent (EraCrypto era)) =>
ShelleyNewEpochEvent era -> Rule (ShelleyNEWEPOCH era) rtype ()
tellReward (forall era. Event (EraRule "RUPD" era) -> ShelleyNewEpochEvent era
DeltaRewardEvent (forall c.
EpochNo
-> Map (Credential 'Staking c) (Set (Reward c)) -> RupdEvent c
RupdEvent Signal (ShelleyNEWEPOCH era)
eNo Map
  (Credential 'Staking (EraCrypto era))
  (Set (Reward (EraCrypto era)))
event))
          forall era.
EraGov era =>
EpochState era
-> EpochNo
-> RewardUpdate (EraCrypto era)
-> Rule (ShelleyNEWEPOCH era) 'Transition (EpochState era)
updateRewards EpochState era
es Signal (ShelleyNEWEPOCH era)
eNo RewardUpdate (EraCrypto era)
ans
        SJust (Complete RewardUpdate (EraCrypto era)
ru') -> forall era.
EraGov era =>
EpochState era
-> EpochNo
-> RewardUpdate (EraCrypto era)
-> Rule (ShelleyNEWEPOCH era) 'Transition (EpochState era)
updateRewards EpochState era
es Signal (ShelleyNEWEPOCH era)
eNo RewardUpdate (EraCrypto era)
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 (EraCrypto era)
pd' = forall c. SnapShots c -> PoolDistr c
ssStakeMarkPoolDistr (forall era. EpochState era -> SnapShots (EraCrypto era)
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 (EraCrypto era)
nesBprev = BlocksMade (EraCrypto era)
bcur
          , nesBcur :: BlocksMade (EraCrypto era)
nesBcur = forall c. Map (KeyHash 'StakePool c) Natural -> BlocksMade c
BlocksMade forall a. Monoid a => a
mempty
          , nesEs :: EpochState era
nesEs = EpochState era
es'''
          , nesRu :: StrictMaybe (PulsingRewUpdate (EraCrypto era))
nesRu = forall a. StrictMaybe a
SNothing
          , nesPd :: PoolDistr (EraCrypto era)
nesPd = PoolDistr (EraCrypto era)
pd'
          }

-- | tell a RupdEvent as a DeltaRewardEvent only if the map is non-empty
tellReward ::
  Event (EraRule "RUPD" era) ~ RupdEvent (EraCrypto era) =>
  ShelleyNewEpochEvent era ->
  Rule (ShelleyNEWEPOCH era) rtype ()
tellReward :: forall era (rtype :: RuleType).
(Event (EraRule "RUPD" era) ~ RupdEvent (EraCrypto era)) =>
ShelleyNewEpochEvent era -> Rule (ShelleyNEWEPOCH era) rtype ()
tellReward (DeltaRewardEvent (RupdEvent EpochNo
_ Map
  (Credential 'Staking (EraCrypto era))
  (Set (Reward (EraCrypto era)))
m)) | forall k a. Map k a -> Bool
Map.null Map
  (Credential 'Staking (EraCrypto era))
  (Set (Reward (EraCrypto era)))
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 (EraCrypto era) ->
  Rule (ShelleyNEWEPOCH era) 'Transition (EpochState era)
updateRewards :: forall era.
EraGov era =>
EpochState era
-> EpochNo
-> RewardUpdate (EraCrypto era)
-> Rule (ShelleyNEWEPOCH era) 'Transition (EpochState era)
updateRewards EpochState era
es EpochNo
e ru' :: RewardUpdate (EraCrypto era)
ru'@(RewardUpdate DeltaCoin
dt DeltaCoin
dr Map
  (Credential 'Staking (EraCrypto era))
  (Set (Reward (EraCrypto era)))
rs_ DeltaCoin
df NonMyopic (EraCrypto era)
_) = do
  let totRs :: Coin
totRs = forall c.
ProtVer -> Map (Credential 'Staking c) (Set (Reward c)) -> 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 (EraCrypto era))
  (Set (Reward (EraCrypto era)))
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 (EraCrypto era) -> ShelleyNewEpochPredFailure era
CorruptRewardUpdate RewardUpdate (EraCrypto era)
ru'
  let !(!EpochState era
es', FilteredRewards era
filtered) = forall era.
EraGov era =>
RewardUpdate (EraCrypto era)
-> EpochState era -> (EpochState era, FilteredRewards era)
applyRUpdFiltered RewardUpdate (EraCrypto era)
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 (EraCrypto era))
     (Set (Reward (EraCrypto era)))
-> Set (Credential 'Staking (EraCrypto era))
-> ShelleyNewEpochEvent era
RestrainedRewards EpochNo
e (forall era.
FilteredRewards era
-> Map
     (Credential 'Staking (EraCrypto era))
     (Set (Reward (EraCrypto era)))
frShelleyIgnored FilteredRewards era
filtered) (forall era.
FilteredRewards era -> Set (Credential 'Staking (EraCrypto era))
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 (EraCrypto era))
     (Set (Reward (EraCrypto era)))
-> ShelleyNewEpochEvent era
TotalRewardEvent EpochNo
e (forall era.
FilteredRewards era
-> Map
     (Credential 'Staking (EraCrypto era))
     (Set (Reward (EraCrypto era)))
frRegistered FilteredRewards era
filtered)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure EpochState era
es'