{-# 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.Constraints (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 (Crypto 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 (Crypto era)
-> BlocksMade (Crypto era)
-> EpochState era
-> StrictMaybe (RewardUpdate (Crypto era))
-> PoolDistr (Crypto era)
-> NewEpochState era
forall era.
EpochNo
-> BlocksMade (Crypto era)
-> BlocksMade (Crypto era)
-> EpochState era
-> StrictMaybe (RewardUpdate (Crypto era))
-> PoolDistr (Crypto era)
-> NewEpochState era
NewEpochState
          (Word64 -> EpochNo
EpochNo Word64
0)
          (Map (KeyHash 'StakePool (Crypto era)) Natural
-> BlocksMade (Crypto era)
forall crypto.
Map (KeyHash 'StakePool crypto) Natural -> BlocksMade crypto
BlocksMade Map (KeyHash 'StakePool (Crypto era)) Natural
forall k a. Map k a
Map.empty)
          (Map (KeyHash 'StakePool (Crypto era)) Natural
-> BlocksMade (Crypto era)
forall crypto.
Map (KeyHash 'StakePool crypto) Natural -> BlocksMade crypto
BlocksMade Map (KeyHash 'StakePool (Crypto era)) Natural
forall k a. Map k a
Map.empty)
          EpochState era
forall era. EpochState era
emptyEpochState
          StrictMaybe (RewardUpdate (Crypto 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 (Crypto era))
ru of
        StrictMaybe (RewardUpdate (Crypto 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 (Crypto era)
ru' -> do
          let RewardUpdate DeltaCoin
dt DeltaCoin
dr Map (Credential 'Staking (Crypto era)) Coin
rs_ DeltaCoin
df NonMyopic (Crypto era)
_ = RewardUpdate (Crypto era)
ru'
          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 -> DeltaCoin) -> Coin -> DeltaCoin
forall a b. (a -> b) -> a -> b
$ Map (Credential 'Staking (Crypto era)) Coin -> Coin
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (Credential 'Staking (Crypto 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 (Crypto era) -> NewEpochPredicateFailure era
forall era.
RewardUpdate (Crypto era) -> NewEpochPredicateFailure era
CorruptRewardUpdate RewardUpdate (Crypto 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 (Crypto era) -> EpochState era -> EpochState era
forall era.
RewardUpdate (Crypto era) -> EpochState era -> EpochState era
applyRUpd RewardUpdate (Crypto 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 (Crypto era)
ss LedgerState era
_ls PParams era
_pr PParams era
_ NonMyopic (Crypto era)
_ = EpochState era
es'''
          pd' :: PoolDistr (Crypto era)
pd' = SnapShot (Crypto era) -> PoolDistr (Crypto era)
forall crypto. SnapShot crypto -> PoolDistr crypto
calculatePoolDistr (SnapShots (Crypto era) -> SnapShot (Crypto era)
forall crypto. SnapShots crypto -> SnapShot crypto
_pstakeSet SnapShots (Crypto 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 (Crypto era)
-> BlocksMade (Crypto era)
-> EpochState era
-> StrictMaybe (RewardUpdate (Crypto era))
-> PoolDistr (Crypto era)
-> NewEpochState era
forall era.
EpochNo
-> BlocksMade (Crypto era)
-> BlocksMade (Crypto era)
-> EpochState era
-> StrictMaybe (RewardUpdate (Crypto era))
-> PoolDistr (Crypto era)
-> NewEpochState era
NewEpochState
          EpochNo
Signal (NEWEPOCH era)
e
          BlocksMade (Crypto era)
bcur
          (Map (KeyHash 'StakePool (Crypto era)) Natural
-> BlocksMade (Crypto era)
forall crypto.
Map (KeyHash 'StakePool crypto) Natural -> BlocksMade crypto
BlocksMade Map (KeyHash 'StakePool (Crypto era)) Natural
forall k a. Map k a
Map.empty)
          EpochState era
es'''
          StrictMaybe (RewardUpdate (Crypto era))
forall a. StrictMaybe a
SNothing
          PoolDistr (Crypto era)
pd'

calculatePoolDistr :: SnapShot crypto -> PoolDistr crypto
calculatePoolDistr :: SnapShot crypto -> PoolDistr crypto
calculatePoolDistr (SnapShot (Stake Map (Credential 'Staking crypto) Coin
stake) Map (Credential 'Staking crypto) (KeyHash 'StakePool crypto)
delegs Map (KeyHash 'StakePool crypto) (PoolParams crypto)
poolParams) =
  let Coin Integer
total = (Coin -> Coin -> Coin)
-> Coin -> Map (Credential 'Staking crypto) 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 crypto) Coin
stake
      sd :: Map (KeyHash 'StakePool crypto) Rational
sd =
        (Rational -> Rational -> Rational)
-> [(KeyHash 'StakePool crypto, Rational)]
-> Map (KeyHash 'StakePool crypto) 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, Rational)]
 -> Map (KeyHash 'StakePool crypto) Rational)
-> [(KeyHash 'StakePool crypto, Rational)]
-> Map (KeyHash 'StakePool crypto) Rational
forall a b. (a -> b) -> a -> b
$
          [Maybe (KeyHash 'StakePool crypto, Rational)]
-> [(KeyHash 'StakePool crypto, 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
 -> (KeyHash 'StakePool crypto, Rational))
-> Maybe (KeyHash 'StakePool crypto)
-> Maybe (KeyHash 'StakePool crypto, Rational)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential 'Staking crypto
-> Map (Credential 'Staking crypto) (KeyHash 'StakePool crypto)
-> Maybe (KeyHash 'StakePool crypto)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Credential 'Staking crypto
hk Map (Credential 'Staking crypto) (KeyHash 'StakePool crypto)
delegs -- TODO mgudemann total could be zero (in
                -- particular when shrinking)
              | (Credential 'Staking crypto
hk, Coin Integer
c) <- Map (Credential 'Staking crypto) Coin
-> [(Credential 'Staking crypto, Coin)]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Credential 'Staking crypto) Coin
stake
            ]
   in Map (KeyHash 'StakePool crypto) (IndividualPoolStake crypto)
-> PoolDistr crypto
forall crypto.
Map (KeyHash 'StakePool crypto) (IndividualPoolStake crypto)
-> PoolDistr crypto
PoolDistr (Map (KeyHash 'StakePool crypto) (IndividualPoolStake crypto)
 -> PoolDistr crypto)
-> Map (KeyHash 'StakePool crypto) (IndividualPoolStake crypto)
-> PoolDistr crypto
forall a b. (a -> b) -> a -> b
$ (Rational
 -> Hash (HASH crypto) (VerKeyVRF (VRF crypto))
 -> IndividualPoolStake crypto)
-> Map (KeyHash 'StakePool crypto) Rational
-> Map
     (KeyHash 'StakePool crypto)
     (Hash (HASH crypto) (VerKeyVRF (VRF crypto)))
-> Map (KeyHash 'StakePool crypto) (IndividualPoolStake crypto)
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) (VerKeyVRF (VRF crypto))
-> IndividualPoolStake crypto
forall crypto.
Rational
-> Hash crypto (VerKeyVRF crypto) -> IndividualPoolStake crypto
IndividualPoolStake Map (KeyHash 'StakePool crypto) Rational
sd ((PoolParams crypto -> Hash (HASH crypto) (VerKeyVRF (VRF crypto)))
-> Map (KeyHash 'StakePool crypto) (PoolParams crypto)
-> Map
     (KeyHash 'StakePool crypto)
     (Hash (HASH crypto) (VerKeyVRF (VRF crypto)))
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map PoolParams crypto -> Hash (HASH crypto) (VerKeyVRF (VRF crypto))
forall crypto. PoolParams crypto -> Hash crypto (VerKeyVRF crypto)
_poolVrf Map (KeyHash 'StakePool crypto) (PoolParams crypto)
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