{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Shelley.Spec.Ledger.STS.NewEpoch
  ( NEWEPOCH,
    NewEpochPredicateFailure (..),
    PredicateFailure,
    calculatePoolDistr,
  )
where

import Cardano.Ledger.Era (Crypto)
import Cardano.Ledger.Shelley (ShelleyBased)
import qualified Cardano.Ledger.Val as Val
import Control.State.Transition
import Data.Foldable (fold)
import qualified Data.Map.Strict as Map
import Data.Maybe (catMaybes)
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))
import Shelley.Spec.Ledger.BaseTypes
import Shelley.Spec.Ledger.Coin
import Shelley.Spec.Ledger.Delegation.Certificates
import Shelley.Spec.Ledger.EpochBoundary
import Shelley.Spec.Ledger.LedgerState
import Shelley.Spec.Ledger.STS.Epoch
import Shelley.Spec.Ledger.STS.Mir
import Shelley.Spec.Ledger.Slot
import Shelley.Spec.Ledger.TxBody

data NEWEPOCH era

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

deriving stock instance
  Show (NewEpochPredicateFailure era)

deriving stock instance
  Eq (NewEpochPredicateFailure era)

instance NoThunks (NewEpochPredicateFailure era)

instance ShelleyBased 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) = NewEpochPredicateFailure era

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

  transitionRules :: [TransitionRule (NEWEPOCH era)]
transitionRules = [TransitionRule (NEWEPOCH era)
forall era. ShelleyBased era => TransitionRule (NEWEPOCH era)
newEpochTransition]

newEpochTransition ::
  forall era.
  ( ShelleyBased era
  ) =>
  TransitionRule (NEWEPOCH era)
newEpochTransition :: TransitionRule (NEWEPOCH era)
newEpochTransition = do
  TRC
    ( Environment (NEWEPOCH era)
_,
      src :: State (NEWEPOCH era)
src@(NewEpochState (EpochNo eL) _ bcur es ru _pd),
      e :: Signal (NEWEPOCH era)
e@(EpochNo e_)
      ) <-
    F (Clause (NEWEPOCH era) 'Transition) (TRC (NEWEPOCH era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  if Word64
e_ Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
/= Word64
eL Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1
    then NewEpochState era
-> F (Clause (NEWEPOCH era) 'Transition) (NewEpochState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure State (NEWEPOCH era)
NewEpochState era
src
    else do
      EpochState era
es' <- case StrictMaybe (RewardUpdate era)
ru of
        StrictMaybe (RewardUpdate era)
SNothing -> EpochState era
-> F (Clause (NEWEPOCH era) 'Transition) (EpochState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure EpochState era
es
        SJust RewardUpdate era
ru' -> do
          let RewardUpdate Coin
dt DeltaCoin
dr Map (Credential 'Staking era) Coin
rs_ DeltaCoin
df NonMyopic era
_ = RewardUpdate era
ru'
          Coin -> Bool
forall t. Val t => t -> Bool
Val.isZero (Coin
dt Coin -> DeltaCoin -> Coin
`addDeltaCoin` (DeltaCoin
dr DeltaCoin -> DeltaCoin -> DeltaCoin
forall a. Semigroup a => a -> a -> a
<> (Coin -> DeltaCoin
toDeltaCoin (Coin -> DeltaCoin) -> Coin -> DeltaCoin
forall a b. (a -> b) -> a -> b
$ Map (Credential 'Staking era) Coin -> Coin
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (Credential 'Staking era) Coin
rs_) DeltaCoin -> DeltaCoin -> DeltaCoin
forall a. Semigroup a => a -> a -> a
<> DeltaCoin
df)) Bool
-> PredicateFailure (NEWEPOCH era)
-> Rule (NEWEPOCH era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! RewardUpdate era -> NewEpochPredicateFailure era
forall era. RewardUpdate era -> NewEpochPredicateFailure era
CorruptRewardUpdate RewardUpdate era
ru'
          EpochState era
-> F (Clause (NEWEPOCH era) 'Transition) (EpochState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EpochState era
 -> F (Clause (NEWEPOCH era) 'Transition) (EpochState era))
-> EpochState era
-> F (Clause (NEWEPOCH era) 'Transition) (EpochState era)
forall a b. (a -> b) -> a -> b
$ RewardUpdate era -> EpochState era -> EpochState era
forall era. RewardUpdate era -> EpochState era -> EpochState era
applyRUpd RewardUpdate era
ru' EpochState era
es

      EpochState era
es'' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (MIR era) super =>
RuleContext rtype (MIR era) -> Rule super rtype (State (MIR era))
trans @(MIR era) (RuleContext 'Transition (MIR era)
 -> Rule (NEWEPOCH era) 'Transition (State (MIR era)))
-> RuleContext 'Transition (MIR era)
-> Rule (NEWEPOCH era) 'Transition (State (MIR era))
forall a b. (a -> b) -> a -> b
$ (Environment (MIR era), State (MIR era), Signal (MIR era))
-> TRC (MIR era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC ((), State (MIR era)
EpochState era
es', ())
      EpochState era
es''' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (EPOCH era) super =>
RuleContext rtype (EPOCH era)
-> Rule super rtype (State (EPOCH era))
trans @(EPOCH era) (RuleContext 'Transition (EPOCH era)
 -> Rule (NEWEPOCH era) 'Transition (State (EPOCH era)))
-> RuleContext 'Transition (EPOCH era)
-> Rule (NEWEPOCH era) 'Transition (State (EPOCH era))
forall a b. (a -> b) -> a -> b
$ (Environment (EPOCH era), State (EPOCH era), Signal (EPOCH era))
-> TRC (EPOCH era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC ((), State (EPOCH era)
EpochState era
es'', Signal (EPOCH era)
Signal (NEWEPOCH era)
e)
      let EpochState AccountState
_acnt SnapShots era
ss LedgerState era
_ls PParams era
_pr PParams era
_ NonMyopic era
_ = EpochState era
es'''
          pd' :: PoolDistr (Crypto era)
pd' = SnapShot era -> PoolDistr (Crypto era)
forall era. SnapShot era -> PoolDistr (Crypto era)
calculatePoolDistr (SnapShots era -> SnapShot era
forall era. SnapShots era -> SnapShot era
_pstakeSet SnapShots era
ss)
      NewEpochState era
-> F (Clause (NEWEPOCH era) 'Transition) (NewEpochState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NewEpochState era
 -> F (Clause (NEWEPOCH era) 'Transition) (NewEpochState era))
-> NewEpochState era
-> F (Clause (NEWEPOCH era) 'Transition) (NewEpochState era)
forall a b. (a -> b) -> a -> b
$
        EpochNo
-> BlocksMade era
-> BlocksMade era
-> EpochState era
-> StrictMaybe (RewardUpdate era)
-> PoolDistr (Crypto era)
-> NewEpochState era
forall era.
EpochNo
-> BlocksMade era
-> BlocksMade era
-> EpochState era
-> StrictMaybe (RewardUpdate era)
-> PoolDistr (Crypto era)
-> NewEpochState era
NewEpochState
          EpochNo
Signal (NEWEPOCH era)
e
          BlocksMade era
bcur
          (Map (KeyHash 'StakePool (Crypto era)) Natural -> BlocksMade era
forall era.
Map (KeyHash 'StakePool (Crypto era)) Natural -> BlocksMade era
BlocksMade Map (KeyHash 'StakePool (Crypto era)) Natural
forall k a. Map k a
Map.empty)
          EpochState era
es'''
          StrictMaybe (RewardUpdate era)
forall a. StrictMaybe a
SNothing
          PoolDistr (Crypto era)
pd'

calculatePoolDistr :: SnapShot era -> PoolDistr (Crypto era)
calculatePoolDistr :: SnapShot era -> PoolDistr (Crypto era)
calculatePoolDistr (SnapShot (Stake Map (Credential 'Staking era) Coin
stake) Map (Credential 'Staking era) (KeyHash 'StakePool (Crypto era))
delegs Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
poolParams) =
  let Coin Integer
total = (Coin -> Coin -> Coin)
-> Coin -> Map (Credential 'Staking era) Coin -> Coin
forall a b k. (a -> b -> a) -> a -> Map k b -> a
Map.foldl' Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
(<>) Coin
forall a. Monoid a => a
mempty Map (Credential 'Staking era) Coin
stake
      sd :: Map (KeyHash 'StakePool (Crypto era)) Rational
sd =
        (Rational -> Rational -> Rational)
-> [(KeyHash 'StakePool (Crypto era), Rational)]
-> Map (KeyHash 'StakePool (Crypto era)) Rational
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
(+) ([(KeyHash 'StakePool (Crypto era), Rational)]
 -> Map (KeyHash 'StakePool (Crypto era)) Rational)
-> [(KeyHash 'StakePool (Crypto era), Rational)]
-> Map (KeyHash 'StakePool (Crypto era)) Rational
forall a b. (a -> b) -> a -> b
$
          [Maybe (KeyHash 'StakePool (Crypto era), Rational)]
-> [(KeyHash 'StakePool (Crypto era), Rational)]
forall a. [Maybe a] -> [a]
catMaybes
            [ (,Integer -> Rational
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
c Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ Integer -> Rational
forall a b. (Integral a, Num b) => a -> b
fromIntegral (if Integer
total Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then Integer
1 else Integer
total))
                (KeyHash 'StakePool (Crypto era)
 -> (KeyHash 'StakePool (Crypto era), Rational))
-> Maybe (KeyHash 'StakePool (Crypto era))
-> Maybe (KeyHash 'StakePool (Crypto era), Rational)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential 'Staking era
-> Map (Credential 'Staking era) (KeyHash 'StakePool (Crypto era))
-> Maybe (KeyHash 'StakePool (Crypto era))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Credential 'Staking era
hk Map (Credential 'Staking era) (KeyHash 'StakePool (Crypto era))
delegs -- TODO mgudemann total could be zero (in
                -- particular when shrinking)
              | (Credential 'Staking era
hk, Coin Integer
c) <- Map (Credential 'Staking era) Coin
-> [(Credential 'Staking era, Coin)]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Credential 'Staking era) Coin
stake
            ]
   in Map
  (KeyHash 'StakePool (Crypto era))
  (IndividualPoolStake (Crypto era))
-> PoolDistr (Crypto era)
forall crypto.
Map (KeyHash 'StakePool crypto) (IndividualPoolStake crypto)
-> PoolDistr crypto
PoolDistr (Map
   (KeyHash 'StakePool (Crypto era))
   (IndividualPoolStake (Crypto era))
 -> PoolDistr (Crypto era))
-> Map
     (KeyHash 'StakePool (Crypto era))
     (IndividualPoolStake (Crypto era))
-> PoolDistr (Crypto era)
forall a b. (a -> b) -> a -> b
$ (Rational
 -> Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era)))
 -> IndividualPoolStake (Crypto era))
-> Map (KeyHash 'StakePool (Crypto era)) Rational
-> Map
     (KeyHash 'StakePool (Crypto era))
     (Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era))))
-> Map
     (KeyHash 'StakePool (Crypto era))
     (IndividualPoolStake (Crypto era))
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWith Rational
-> Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era)))
-> IndividualPoolStake (Crypto era)
forall crypto.
Rational
-> Hash crypto (VerKeyVRF crypto) -> IndividualPoolStake crypto
IndividualPoolStake Map (KeyHash 'StakePool (Crypto era)) Rational
sd ((PoolParams era
 -> Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era))))
-> Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
-> Map
     (KeyHash 'StakePool (Crypto era))
     (Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era))))
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map PoolParams era
-> Hash (HASH (Crypto era)) (VerKeyVRF (VRF (Crypto era)))
forall era.
PoolParams era -> Hash (Crypto era) (VerKeyVRF (Crypto era))
_poolVrf Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
poolParams)

instance
  ShelleyBased era =>
  Embed (EPOCH era) (NEWEPOCH era)
  where
  wrapFailed :: PredicateFailure (EPOCH era) -> PredicateFailure (NEWEPOCH era)
wrapFailed = PredicateFailure (EPOCH era) -> PredicateFailure (NEWEPOCH era)
forall era.
PredicateFailure (EPOCH era) -> NewEpochPredicateFailure era
EpochFailure

instance
  ShelleyBased era =>
  Embed (MIR era) (NEWEPOCH era)
  where
  wrapFailed :: PredicateFailure (MIR era) -> PredicateFailure (NEWEPOCH era)
wrapFailed = PredicateFailure (MIR era) -> PredicateFailure (NEWEPOCH era)
forall era.
PredicateFailure (MIR era) -> NewEpochPredicateFailure era
MirFailure