{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE EmptyDataDeriving #-}
{-# 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.Tick (
  ShelleyTICK,
  State,
  ShelleyTickPredFailure (..),
  ShelleyTickEvent (..),
  PredicateFailure,
  adoptGenesisDelegs,
  ShelleyTICKF,
  ShelleyTickfPredFailure,
  validatingTickTransition,
  validatingTickTransitionFORECAST,
  solidifyNextEpochPParams,
) where

import Cardano.Ledger.BaseTypes (ShelleyBase, StrictMaybe (..))
import Cardano.Ledger.Core
import Cardano.Ledger.Keys (GenDelegs (..))
import Cardano.Ledger.Shelley.Era (ShelleyEra, ShelleyTICK, ShelleyTICKF)
import Cardano.Ledger.Shelley.Governance
import Cardano.Ledger.Shelley.LedgerState (
  DState (..),
  EpochState (..),
  FutureGenDeleg (..),
  LedgerState (..),
  NewEpochState (..),
  PulsingRewUpdate,
  UTxOState (..),
  curPParamsEpochStateL,
  lsCertStateL,
  newEpochStateGovStateL,
 )
import Cardano.Ledger.Shelley.Rules.NewEpoch (
  ShelleyNEWEPOCH,
  ShelleyNewEpochEvent,
  ShelleyNewEpochPredFailure,
 )
import Cardano.Ledger.Shelley.Rules.Rupd (
  RupdEnv (..),
  RupdEvent,
  ShelleyRUPD,
  ShelleyRupdPredFailure,
 )
import Cardano.Ledger.Shelley.Rules.Upec (ShelleyUPEC, ShelleyUpecPredFailure, UpecState (..))
import Cardano.Ledger.Slot (EpochNo, SlotNo, getTheSlotOfNoReturn)
import Cardano.Ledger.State (EraCertState (..), SnapShots (ssStakeMark, ssStakeMarkPoolDistr))
import Control.DeepSeq (NFData)
import Control.SetAlgebra (eval, (⨃))
import Control.State.Transition
import qualified Data.Map.Strict as Map
import Data.Void (Void)
import GHC.Generics (Generic)
import Lens.Micro ((%~), (&), (.~), (^.))
import NoThunks.Class (NoThunks (..))

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

data ShelleyTickPredFailure era
  = NewEpochFailure (PredicateFailure (EraRule "NEWEPOCH" era)) -- Subtransition Failures
  | RupdFailure (PredicateFailure (EraRule "RUPD" era)) -- Subtransition Failures
  deriving ((forall x.
 ShelleyTickPredFailure era -> Rep (ShelleyTickPredFailure era) x)
-> (forall x.
    Rep (ShelleyTickPredFailure era) x -> ShelleyTickPredFailure era)
-> Generic (ShelleyTickPredFailure era)
forall x.
Rep (ShelleyTickPredFailure era) x -> ShelleyTickPredFailure era
forall x.
ShelleyTickPredFailure era -> Rep (ShelleyTickPredFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyTickPredFailure era) x -> ShelleyTickPredFailure era
forall era x.
ShelleyTickPredFailure era -> Rep (ShelleyTickPredFailure era) x
$cfrom :: forall era x.
ShelleyTickPredFailure era -> Rep (ShelleyTickPredFailure era) x
from :: forall x.
ShelleyTickPredFailure era -> Rep (ShelleyTickPredFailure era) x
$cto :: forall era x.
Rep (ShelleyTickPredFailure era) x -> ShelleyTickPredFailure era
to :: forall x.
Rep (ShelleyTickPredFailure era) x -> ShelleyTickPredFailure era
Generic)

deriving stock instance
  ( Show (PredicateFailure (EraRule "NEWEPOCH" era))
  , Show (PredicateFailure (EraRule "RUPD" era))
  ) =>
  Show (ShelleyTickPredFailure era)

deriving stock instance
  ( Eq (PredicateFailure (EraRule "NEWEPOCH" era))
  , Eq (PredicateFailure (EraRule "RUPD" era))
  ) =>
  Eq (ShelleyTickPredFailure era)

instance
  ( NoThunks (PredicateFailure (EraRule "NEWEPOCH" era))
  , NoThunks (PredicateFailure (EraRule "RUPD" era))
  ) =>
  NoThunks (ShelleyTickPredFailure era)

instance
  ( NFData (PredicateFailure (EraRule "NEWEPOCH" era))
  , NFData (PredicateFailure (EraRule "RUPD" era))
  ) =>
  NFData (ShelleyTickPredFailure era)

data ShelleyTickEvent era
  = TickNewEpochEvent (Event (EraRule "NEWEPOCH" era))
  | TickRupdEvent (Event (EraRule "RUPD" era))
  deriving ((forall x. ShelleyTickEvent era -> Rep (ShelleyTickEvent era) x)
-> (forall x. Rep (ShelleyTickEvent era) x -> ShelleyTickEvent era)
-> Generic (ShelleyTickEvent era)
forall x. Rep (ShelleyTickEvent era) x -> ShelleyTickEvent era
forall x. ShelleyTickEvent era -> Rep (ShelleyTickEvent era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x. Rep (ShelleyTickEvent era) x -> ShelleyTickEvent era
forall era x. ShelleyTickEvent era -> Rep (ShelleyTickEvent era) x
$cfrom :: forall era x. ShelleyTickEvent era -> Rep (ShelleyTickEvent era) x
from :: forall x. ShelleyTickEvent era -> Rep (ShelleyTickEvent era) x
$cto :: forall era x. Rep (ShelleyTickEvent era) x -> ShelleyTickEvent era
to :: forall x. Rep (ShelleyTickEvent era) x -> ShelleyTickEvent era
Generic)

type instance EraRuleEvent "TICK" ShelleyEra = ShelleyTickEvent ShelleyEra

deriving instance
  ( Eq (Event (EraRule "NEWEPOCH" era))
  , Eq (Event (EraRule "RUPD" era))
  ) =>
  Eq (ShelleyTickEvent era)

instance
  ( NFData (Event (EraRule "NEWEPOCH" era))
  , NFData (Event (EraRule "RUPD" era))
  ) =>
  NFData (ShelleyTickEvent era)

instance
  ( EraGov era
  , EraCertState era
  , Embed (EraRule "NEWEPOCH" era) (ShelleyTICK era)
  , Embed (EraRule "RUPD" era) (ShelleyTICK era)
  , State (ShelleyTICK era) ~ NewEpochState era
  , BaseM (ShelleyTICK era) ~ ShelleyBase
  , Environment (EraRule "RUPD" era) ~ RupdEnv era
  , State (EraRule "RUPD" era) ~ StrictMaybe PulsingRewUpdate
  , Signal (EraRule "RUPD" era) ~ SlotNo
  , Environment (EraRule "NEWEPOCH" era) ~ ()
  , State (EraRule "NEWEPOCH" era) ~ NewEpochState era
  , Signal (EraRule "NEWEPOCH" era) ~ EpochNo
  ) =>
  STS (ShelleyTICK era)
  where
  type State (ShelleyTICK era) = NewEpochState era
  type Signal (ShelleyTICK era) = SlotNo
  type Environment (ShelleyTICK era) = ()
  type BaseM (ShelleyTICK era) = ShelleyBase
  type PredicateFailure (ShelleyTICK era) = ShelleyTickPredFailure era
  type Event (ShelleyTICK era) = ShelleyTickEvent era

  initialRules :: [InitialRule (ShelleyTICK era)]
initialRules = []
  transitionRules :: [TransitionRule (ShelleyTICK era)]
transitionRules = [TransitionRule (ShelleyTICK era)
forall era.
(EraGov era, EraCertState era,
 Embed (EraRule "NEWEPOCH" era) (ShelleyTICK era),
 Embed (EraRule "RUPD" era) (ShelleyTICK era),
 STS (ShelleyTICK era),
 Environment (EraRule "RUPD" era) ~ RupdEnv era,
 State (EraRule "RUPD" era) ~ StrictMaybe PulsingRewUpdate,
 Signal (EraRule "RUPD" era) ~ SlotNo,
 Environment (EraRule "NEWEPOCH" era) ~ (),
 State (EraRule "NEWEPOCH" era) ~ NewEpochState era,
 Signal (EraRule "NEWEPOCH" era) ~ EpochNo) =>
TransitionRule (ShelleyTICK era)
bheadTransition]

adoptGenesisDelegs ::
  EraCertState era =>
  EpochState era ->
  SlotNo ->
  EpochState era
adoptGenesisDelegs :: forall era.
EraCertState era =>
EpochState era -> SlotNo -> EpochState era
adoptGenesisDelegs EpochState era
es SlotNo
slot = EpochState era
es'
  where
    ls :: LedgerState era
ls = EpochState era -> LedgerState era
forall era. EpochState era -> LedgerState era
esLState EpochState era
es
    dp :: CertState era
dp = LedgerState era -> CertState era
forall era. LedgerState era -> CertState era
lsCertState LedgerState era
ls
    ds :: DState era
ds = CertState era
dp CertState era
-> Getting (DState era) (CertState era) (DState era) -> DState era
forall s a. s -> Getting a s a -> a
^. Getting (DState era) (CertState era) (DState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL
    fGenDelegs :: Map FutureGenDeleg GenDelegPair
fGenDelegs = DState era -> Map FutureGenDeleg GenDelegPair
forall era. DState era -> Map FutureGenDeleg GenDelegPair
dsFutureGenDelegs DState era
ds
    GenDelegs Map (KeyHash 'Genesis) GenDelegPair
genDelegs = DState era -> GenDelegs
forall era. DState era -> GenDelegs
dsGenDelegs DState era
ds
    (Map FutureGenDeleg GenDelegPair
curr, Map FutureGenDeleg GenDelegPair
fGenDelegs') = (FutureGenDeleg -> GenDelegPair -> Bool)
-> Map FutureGenDeleg GenDelegPair
-> (Map FutureGenDeleg GenDelegPair,
    Map FutureGenDeleg GenDelegPair)
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey (\(FutureGenDeleg SlotNo
s KeyHash 'Genesis
_) GenDelegPair
_ -> SlotNo
s SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
<= SlotNo
slot) Map FutureGenDeleg GenDelegPair
fGenDelegs
    latestPerGKey :: FutureGenDeleg
-> b
-> Map (KeyHash 'Genesis) (SlotNo, b)
-> Map (KeyHash 'Genesis) (SlotNo, b)
latestPerGKey (FutureGenDeleg SlotNo
s KeyHash 'Genesis
genKeyHash) b
delegate Map (KeyHash 'Genesis) (SlotNo, b)
latest =
      case KeyHash 'Genesis
-> Map (KeyHash 'Genesis) (SlotNo, b) -> Maybe (SlotNo, b)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KeyHash 'Genesis
genKeyHash Map (KeyHash 'Genesis) (SlotNo, b)
latest of
        Maybe (SlotNo, b)
Nothing -> KeyHash 'Genesis
-> (SlotNo, b)
-> Map (KeyHash 'Genesis) (SlotNo, b)
-> Map (KeyHash 'Genesis) (SlotNo, b)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert KeyHash 'Genesis
genKeyHash (SlotNo
s, b
delegate) Map (KeyHash 'Genesis) (SlotNo, b)
latest
        Just (SlotNo
t, b
_) ->
          if SlotNo
s SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
> SlotNo
t
            then KeyHash 'Genesis
-> (SlotNo, b)
-> Map (KeyHash 'Genesis) (SlotNo, b)
-> Map (KeyHash 'Genesis) (SlotNo, b)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert KeyHash 'Genesis
genKeyHash (SlotNo
s, b
delegate) Map (KeyHash 'Genesis) (SlotNo, b)
latest
            else Map (KeyHash 'Genesis) (SlotNo, b)
latest
    genDelegs' :: Map (KeyHash 'Genesis) GenDelegPair
genDelegs' = ((SlotNo, GenDelegPair) -> GenDelegPair)
-> Map (KeyHash 'Genesis) (SlotNo, GenDelegPair)
-> Map (KeyHash 'Genesis) GenDelegPair
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (SlotNo, GenDelegPair) -> GenDelegPair
forall a b. (a, b) -> b
snd (Map (KeyHash 'Genesis) (SlotNo, GenDelegPair)
 -> Map (KeyHash 'Genesis) GenDelegPair)
-> Map (KeyHash 'Genesis) (SlotNo, GenDelegPair)
-> Map (KeyHash 'Genesis) GenDelegPair
forall a b. (a -> b) -> a -> b
$ (FutureGenDeleg
 -> GenDelegPair
 -> Map (KeyHash 'Genesis) (SlotNo, GenDelegPair)
 -> Map (KeyHash 'Genesis) (SlotNo, GenDelegPair))
-> Map (KeyHash 'Genesis) (SlotNo, GenDelegPair)
-> Map FutureGenDeleg GenDelegPair
-> Map (KeyHash 'Genesis) (SlotNo, GenDelegPair)
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey FutureGenDeleg
-> GenDelegPair
-> Map (KeyHash 'Genesis) (SlotNo, GenDelegPair)
-> Map (KeyHash 'Genesis) (SlotNo, GenDelegPair)
forall {b}.
FutureGenDeleg
-> b
-> Map (KeyHash 'Genesis) (SlotNo, b)
-> Map (KeyHash 'Genesis) (SlotNo, b)
latestPerGKey Map (KeyHash 'Genesis) (SlotNo, GenDelegPair)
forall k a. Map k a
Map.empty Map FutureGenDeleg GenDelegPair
curr
    ds' :: DState era
ds' =
      DState era
ds
        { dsFutureGenDelegs = fGenDelegs'
        , dsGenDelegs = GenDelegs $ eval (genDelegs ⨃ genDelegs')
        }
    dp' :: CertState era
dp' = CertState era
dp CertState era -> (CertState era -> CertState era) -> CertState era
forall a b. a -> (a -> b) -> b
& (DState era -> Identity (DState era))
-> CertState era -> Identity (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era -> Identity (DState era))
 -> CertState era -> Identity (CertState era))
-> DState era -> CertState era -> CertState era
forall s t a b. ASetter s t a b -> b -> s -> t
.~ DState era
ds'
    ls' :: LedgerState era
ls' = LedgerState era
ls LedgerState era
-> (LedgerState era -> LedgerState era) -> LedgerState era
forall a b. a -> (a -> b) -> b
& (CertState era -> Identity (CertState era))
-> LedgerState era -> Identity (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL ((CertState era -> Identity (CertState era))
 -> LedgerState era -> Identity (LedgerState era))
-> CertState era -> LedgerState era -> LedgerState era
forall s t a b. ASetter s t a b -> b -> s -> t
.~ CertState era
dp'
    es' :: EpochState era
es' = EpochState era
es {esLState = ls'}

-- | This action ensures that once the current slot number is at the point of no return we
-- mark the future PParams to be updated at the next epoch boundary. Also returns the
-- current epoch number for convenience.
solidifyNextEpochPParams ::
  EraGov era =>
  NewEpochState era ->
  SlotNo ->
  ShelleyBase (EpochNo, NewEpochState era)
solidifyNextEpochPParams :: forall era.
EraGov era =>
NewEpochState era
-> SlotNo -> ShelleyBase (EpochNo, NewEpochState era)
solidifyNextEpochPParams NewEpochState era
nes SlotNo
slot = do
  (EpochNo
curEpochNo, SlotNo
slotOfNoReturn, EpochNo
_) <- HasCallStack => SlotNo -> ShelleyBase (EpochNo, SlotNo, EpochNo)
SlotNo -> ShelleyBase (EpochNo, SlotNo, EpochNo)
getTheSlotOfNoReturn SlotNo
slot
  (EpochNo, NewEpochState era)
-> ShelleyBase (EpochNo, NewEpochState era)
forall a. a -> ReaderT Globals Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( EpochNo
curEpochNo
    , if SlotNo
slot SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
< SlotNo
slotOfNoReturn
        then NewEpochState era
nes
        else NewEpochState era
nes NewEpochState era
-> (NewEpochState era -> NewEpochState era) -> NewEpochState era
forall a b. a -> (a -> b) -> b
& (GovState era -> Identity (GovState era))
-> NewEpochState era -> Identity (NewEpochState era)
forall era (f :: * -> *).
Functor f =>
(GovState era -> f (GovState era))
-> NewEpochState era -> f (NewEpochState era)
newEpochStateGovStateL ((GovState era -> Identity (GovState era))
 -> NewEpochState era -> Identity (NewEpochState era))
-> ((FuturePParams era -> Identity (FuturePParams era))
    -> GovState era -> Identity (GovState era))
-> (FuturePParams era -> Identity (FuturePParams era))
-> NewEpochState era
-> Identity (NewEpochState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FuturePParams era -> Identity (FuturePParams era))
-> GovState era -> Identity (GovState era)
forall era. EraGov era => Lens' (GovState era) (FuturePParams era)
Lens' (GovState era) (FuturePParams era)
futurePParamsGovStateL ((FuturePParams era -> Identity (FuturePParams era))
 -> NewEpochState era -> Identity (NewEpochState era))
-> (FuturePParams era -> FuturePParams era)
-> NewEpochState era
-> NewEpochState era
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ FuturePParams era -> FuturePParams era
forall era. FuturePParams era -> FuturePParams era
solidifyFuturePParams
    )

-- | This is a limited version of 'bheadTransition' which is suitable for the
-- future ledger view.
validatingTickTransition ::
  forall tick era.
  ( EraGov era
  , EraCertState era
  , Embed (EraRule "NEWEPOCH" era) (tick era)
  , STS (tick era)
  , State (tick era) ~ NewEpochState era
  , BaseM (tick era) ~ ShelleyBase
  , Environment (EraRule "NEWEPOCH" era) ~ ()
  , State (EraRule "NEWEPOCH" era) ~ NewEpochState era
  , Signal (EraRule "NEWEPOCH" era) ~ EpochNo
  ) =>
  NewEpochState era ->
  SlotNo ->
  TransitionRule (tick era)
validatingTickTransition :: forall (tick :: * -> *) era.
(EraGov era, EraCertState era,
 Embed (EraRule "NEWEPOCH" era) (tick era), STS (tick era),
 State (tick era) ~ NewEpochState era,
 BaseM (tick era) ~ ShelleyBase,
 Environment (EraRule "NEWEPOCH" era) ~ (),
 State (EraRule "NEWEPOCH" era) ~ NewEpochState era,
 Signal (EraRule "NEWEPOCH" era) ~ EpochNo) =>
NewEpochState era -> SlotNo -> TransitionRule (tick era)
validatingTickTransition NewEpochState era
nes0 SlotNo
slot = do
  (EpochNo
curEpochNo, NewEpochState era
nes) <- BaseM (tick era) (EpochNo, NewEpochState era)
-> Rule (tick era) 'Transition (EpochNo, NewEpochState era)
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (tick era) (EpochNo, NewEpochState era)
 -> Rule (tick era) 'Transition (EpochNo, NewEpochState era))
-> BaseM (tick era) (EpochNo, NewEpochState era)
-> Rule (tick era) 'Transition (EpochNo, NewEpochState era)
forall a b. (a -> b) -> a -> b
$ NewEpochState era
-> SlotNo -> ShelleyBase (EpochNo, NewEpochState era)
forall era.
EraGov era =>
NewEpochState era
-> SlotNo -> ShelleyBase (EpochNo, NewEpochState era)
solidifyNextEpochPParams NewEpochState era
nes0 SlotNo
slot

  NewEpochState era
nes' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "NEWEPOCH" era) (RuleContext 'Transition (EraRule "NEWEPOCH" era)
 -> Rule (tick era) 'Transition (State (EraRule "NEWEPOCH" era)))
-> RuleContext 'Transition (EraRule "NEWEPOCH" era)
-> Rule (tick era) 'Transition (State (EraRule "NEWEPOCH" era))
forall a b. (a -> b) -> a -> b
$ (Environment (EraRule "NEWEPOCH" era),
 State (EraRule "NEWEPOCH" era), Signal (EraRule "NEWEPOCH" era))
-> TRC (EraRule "NEWEPOCH" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC ((), State (EraRule "NEWEPOCH" era)
NewEpochState era
nes, EpochNo
Signal (EraRule "NEWEPOCH" era)
curEpochNo)
  let es'' :: EpochState era
es'' = EpochState era -> SlotNo -> EpochState era
forall era.
EraCertState era =>
EpochState era -> SlotNo -> EpochState era
adoptGenesisDelegs (NewEpochState era -> EpochState era
forall era. NewEpochState era -> EpochState era
nesEs NewEpochState era
nes') SlotNo
slot

  NewEpochState era
-> F (Clause (tick era) 'Transition) (NewEpochState era)
forall a. a -> F (Clause (tick era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NewEpochState era
 -> F (Clause (tick era) 'Transition) (NewEpochState era))
-> NewEpochState era
-> F (Clause (tick era) 'Transition) (NewEpochState era)
forall a b. (a -> b) -> a -> b
$ NewEpochState era
nes' {nesEs = es''}

-- | This is a limited version of 'validatingTickTransition' which is only suitable
-- for the future ledger view.
validatingTickTransitionFORECAST ::
  forall tick era.
  ( State (tick era) ~ NewEpochState era
  , BaseM (tick era) ~ ShelleyBase
  , State (EraRule "UPEC" era) ~ UpecState era
  , Signal (EraRule "UPEC" era) ~ ()
  , Environment (EraRule "UPEC" era) ~ LedgerState era
  , Embed (EraRule "UPEC" era) (tick era)
  , STS (tick era)
  , GovState era ~ ShelleyGovState era
  , EraGov era
  , EraCertState era
  ) =>
  NewEpochState era ->
  SlotNo ->
  TransitionRule (tick era)
validatingTickTransitionFORECAST :: forall (tick :: * -> *) era.
(State (tick era) ~ NewEpochState era,
 BaseM (tick era) ~ ShelleyBase,
 State (EraRule "UPEC" era) ~ UpecState era,
 Signal (EraRule "UPEC" era) ~ (),
 Environment (EraRule "UPEC" era) ~ LedgerState era,
 Embed (EraRule "UPEC" era) (tick era), STS (tick era),
 GovState era ~ ShelleyGovState era, EraGov era,
 EraCertState era) =>
NewEpochState era -> SlotNo -> TransitionRule (tick era)
validatingTickTransitionFORECAST NewEpochState era
nes0 SlotNo
slot = do
  -- This whole function is a specialization of an inlined 'NEWEPOCH'.
  --
  -- The ledger view, 'LedgerView', is built entirely from the 'nesPd' and 'esPp' and
  -- 'dsGenDelegs', so the correctness of 'validatingTickTransitionFORECAST' only
  -- depends on getting these three fields correct.

  (EpochNo
curEpochNo, NewEpochState era
nes) <- BaseM (tick era) (EpochNo, NewEpochState era)
-> Rule (tick era) 'Transition (EpochNo, NewEpochState era)
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (tick era) (EpochNo, NewEpochState era)
 -> Rule (tick era) 'Transition (EpochNo, NewEpochState era))
-> BaseM (tick era) (EpochNo, NewEpochState era)
-> Rule (tick era) 'Transition (EpochNo, NewEpochState era)
forall a b. (a -> b) -> a -> b
$ NewEpochState era
-> SlotNo -> ShelleyBase (EpochNo, NewEpochState era)
forall era.
EraGov era =>
NewEpochState era
-> SlotNo -> ShelleyBase (EpochNo, NewEpochState era)
solidifyNextEpochPParams NewEpochState era
nes0 SlotNo
slot

  let es :: EpochState era
es = NewEpochState era -> EpochState era
forall era. NewEpochState era -> EpochState era
nesEs NewEpochState era
nes
      ss :: SnapShots
ss = EpochState era -> SnapShots
forall era. EpochState era -> SnapShots
esSnapshots EpochState era
es

  -- the relevant 'NEWEPOCH' logic
  let pd' :: PoolDistr
pd' = SnapShots -> PoolDistr
ssStakeMarkPoolDistr SnapShots
ss

  -- note that the genesis delegates are updated not only on the epoch boundary.
  if EpochNo
curEpochNo EpochNo -> EpochNo -> Bool
forall a. Eq a => a -> a -> Bool
/= EpochNo -> EpochNo
forall a. Enum a => a -> a
succ (NewEpochState era -> EpochNo
forall era. NewEpochState era -> EpochNo
nesEL NewEpochState era
nes)
    then NewEpochState era
-> F (Clause (tick era) 'Transition) (NewEpochState era)
forall a. a -> F (Clause (tick era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NewEpochState era
 -> F (Clause (tick era) 'Transition) (NewEpochState era))
-> NewEpochState era
-> F (Clause (tick era) 'Transition) (NewEpochState era)
forall a b. (a -> b) -> a -> b
$ NewEpochState era
nes {nesEs = adoptGenesisDelegs es slot}
    else do
      -- We can skip 'SNAP'; we already have the equivalent pd'.

      -- We can skip 'MIR' and 'POOLREAP';
      -- we don't need to do the checks:
      -- if the checks would fail, then the node will fail in the 'TICK' rule
      -- if it ever then node tries to validate blocks for which the
      -- return value here was used to validate their headers.

      let pp :: PParams era
pp = EpochState era
es EpochState era
-> Getting (PParams era) (EpochState era) (PParams era)
-> PParams era
forall s a. s -> Getting a s a -> a
^. Getting (PParams era) (EpochState era) (PParams era)
forall era. EraGov era => Lens' (EpochState era) (PParams era)
Lens' (EpochState era) (PParams era)
curPParamsEpochStateL
          ls :: LedgerState era
ls = EpochState era -> LedgerState era
forall era. EpochState era -> LedgerState era
esLState EpochState era
es
          updates :: GovState era
updates = UTxOState era -> GovState era
forall era. UTxOState era -> GovState era
utxosGovState (UTxOState era -> GovState era) -> UTxOState era -> GovState era
forall a b. (a -> b) -> a -> b
$ LedgerState era -> UTxOState era
forall era. LedgerState era -> UTxOState era
lsUTxOState LedgerState era
ls
      UpecState PParams era
pp' ShelleyGovState era
_ <-
        forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "UPEC" era) (RuleContext 'Transition (EraRule "UPEC" era)
 -> Rule (tick era) 'Transition (State (EraRule "UPEC" era)))
-> RuleContext 'Transition (EraRule "UPEC" era)
-> Rule (tick era) 'Transition (State (EraRule "UPEC" era))
forall a b. (a -> b) -> a -> b
$
          (Environment (EraRule "UPEC" era), State (EraRule "UPEC" era),
 Signal (EraRule "UPEC" era))
-> TRC (EraRule "UPEC" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment (EraRule "UPEC" era)
LedgerState era
ls, PParams era -> ShelleyGovState era -> UpecState era
forall era. PParams era -> ShelleyGovState era -> UpecState era
UpecState PParams era
pp GovState era
ShelleyGovState era
updates, ())
      let es' :: EpochState era
es' =
            EpochState era -> SlotNo -> EpochState era
forall era.
EraCertState era =>
EpochState era -> SlotNo -> EpochState era
adoptGenesisDelegs EpochState era
es SlotNo
slot
              EpochState era
-> (EpochState era -> EpochState era) -> EpochState era
forall a b. a -> (a -> b) -> b
& (PParams era -> Identity (PParams era))
-> EpochState era -> Identity (EpochState era)
forall era. EraGov era => Lens' (EpochState era) (PParams era)
Lens' (EpochState era) (PParams era)
curPParamsEpochStateL ((PParams era -> Identity (PParams era))
 -> EpochState era -> Identity (EpochState era))
-> PParams era -> EpochState era -> EpochState era
forall s t a b. ASetter s t a b -> b -> s -> t
.~ PParams era
pp'

      NewEpochState era
-> F (Clause (tick era) 'Transition) (NewEpochState era)
forall a. a -> F (Clause (tick era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NewEpochState era
 -> F (Clause (tick era) 'Transition) (NewEpochState era))
-> NewEpochState era
-> F (Clause (tick era) 'Transition) (NewEpochState era)
forall a b. (a -> b) -> a -> b
$!
        NewEpochState era
nes
          { nesPd = pd'
          , nesEs = es'
          }

bheadTransition ::
  forall era.
  ( EraGov era
  , EraCertState era
  , Embed (EraRule "NEWEPOCH" era) (ShelleyTICK era)
  , Embed (EraRule "RUPD" era) (ShelleyTICK era)
  , STS (ShelleyTICK era)
  , Environment (EraRule "RUPD" era) ~ RupdEnv era
  , State (EraRule "RUPD" era) ~ StrictMaybe PulsingRewUpdate
  , Signal (EraRule "RUPD" era) ~ SlotNo
  , Environment (EraRule "NEWEPOCH" era) ~ ()
  , State (EraRule "NEWEPOCH" era) ~ NewEpochState era
  , Signal (EraRule "NEWEPOCH" era) ~ EpochNo
  ) =>
  TransitionRule (ShelleyTICK era)
bheadTransition :: forall era.
(EraGov era, EraCertState era,
 Embed (EraRule "NEWEPOCH" era) (ShelleyTICK era),
 Embed (EraRule "RUPD" era) (ShelleyTICK era),
 STS (ShelleyTICK era),
 Environment (EraRule "RUPD" era) ~ RupdEnv era,
 State (EraRule "RUPD" era) ~ StrictMaybe PulsingRewUpdate,
 Signal (EraRule "RUPD" era) ~ SlotNo,
 Environment (EraRule "NEWEPOCH" era) ~ (),
 State (EraRule "NEWEPOCH" era) ~ NewEpochState era,
 Signal (EraRule "NEWEPOCH" era) ~ EpochNo) =>
TransitionRule (ShelleyTICK era)
bheadTransition = do
  TRC ((), nes0 :: State (ShelleyTICK era)
nes0@(NewEpochState EpochNo
_ BlocksMade
bprev BlocksMade
_ EpochState era
es StrictMaybe PulsingRewUpdate
_ PoolDistr
_ StashedAVVMAddresses era
_), Signal (ShelleyTICK era)
slot) <-
    Rule
  (ShelleyTICK era)
  'Transition
  (RuleContext 'Transition (ShelleyTICK era))
F (Clause (ShelleyTICK era) 'Transition) (TRC (ShelleyTICK era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext

  NewEpochState era
nes1 <- forall (tick :: * -> *) era.
(EraGov era, EraCertState era,
 Embed (EraRule "NEWEPOCH" era) (tick era), STS (tick era),
 State (tick era) ~ NewEpochState era,
 BaseM (tick era) ~ ShelleyBase,
 Environment (EraRule "NEWEPOCH" era) ~ (),
 State (EraRule "NEWEPOCH" era) ~ NewEpochState era,
 Signal (EraRule "NEWEPOCH" era) ~ EpochNo) =>
NewEpochState era -> SlotNo -> TransitionRule (tick era)
validatingTickTransition @ShelleyTICK State (ShelleyTICK era)
NewEpochState era
nes0 SlotNo
Signal (ShelleyTICK era)
slot

  -- Here we force the evaluation of the mark snapshot
  -- and the per-pool stake distribution.
  -- We do NOT force it in the TICKF and TICKN rule
  -- so that it can remain a thunk when the consensus
  -- layer computes the ledger view across the epoch boundary.
  let !SnapShot
_ = SnapShots -> SnapShot
ssStakeMark (SnapShots -> SnapShot)
-> (NewEpochState era -> SnapShots)
-> NewEpochState era
-> SnapShot
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpochState era -> SnapShots
forall era. EpochState era -> SnapShots
esSnapshots (EpochState era -> SnapShots)
-> (NewEpochState era -> EpochState era)
-> NewEpochState era
-> SnapShots
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewEpochState era -> EpochState era
forall era. NewEpochState era -> EpochState era
nesEs (NewEpochState era -> SnapShot) -> NewEpochState era -> SnapShot
forall a b. (a -> b) -> a -> b
$ NewEpochState era
nes1
      !PoolDistr
_ = SnapShots -> PoolDistr
ssStakeMarkPoolDistr (SnapShots -> PoolDistr)
-> (NewEpochState era -> SnapShots)
-> NewEpochState era
-> PoolDistr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpochState era -> SnapShots
forall era. EpochState era -> SnapShots
esSnapshots (EpochState era -> SnapShots)
-> (NewEpochState era -> EpochState era)
-> NewEpochState era
-> SnapShots
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewEpochState era -> EpochState era
forall era. NewEpochState era -> EpochState era
nesEs (NewEpochState era -> PoolDistr) -> NewEpochState era -> PoolDistr
forall a b. (a -> b) -> a -> b
$ NewEpochState era
nes1

  StrictMaybe PulsingRewUpdate
ru'' <-
    forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "RUPD" era) (RuleContext 'Transition (EraRule "RUPD" era)
 -> Rule (ShelleyTICK era) 'Transition (State (EraRule "RUPD" era)))
-> RuleContext 'Transition (EraRule "RUPD" era)
-> Rule (ShelleyTICK era) 'Transition (State (EraRule "RUPD" era))
forall a b. (a -> b) -> a -> b
$
      (Environment (EraRule "RUPD" era), State (EraRule "RUPD" era),
 Signal (EraRule "RUPD" era))
-> TRC (EraRule "RUPD" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (BlocksMade -> EpochState era -> RupdEnv era
forall era. BlocksMade -> EpochState era -> RupdEnv era
RupdEnv BlocksMade
bprev EpochState era
es, NewEpochState era -> StrictMaybe PulsingRewUpdate
forall era. NewEpochState era -> StrictMaybe PulsingRewUpdate
nesRu NewEpochState era
nes1, Signal (EraRule "RUPD" era)
Signal (ShelleyTICK era)
slot)

  let nes2 :: NewEpochState era
nes2 = NewEpochState era
nes1 {nesRu = ru''}
  NewEpochState era
-> F (Clause (ShelleyTICK era) 'Transition) (NewEpochState era)
forall a. a -> F (Clause (ShelleyTICK era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure NewEpochState era
nes2

instance
  ( STS (ShelleyNEWEPOCH era)
  , PredicateFailure (EraRule "NEWEPOCH" era) ~ ShelleyNewEpochPredFailure era
  , Event (EraRule "NEWEPOCH" era) ~ ShelleyNewEpochEvent era
  ) =>
  Embed (ShelleyNEWEPOCH era) (ShelleyTICK era)
  where
  wrapFailed :: PredicateFailure (ShelleyNEWEPOCH era)
-> PredicateFailure (ShelleyTICK era)
wrapFailed = PredicateFailure (EraRule "NEWEPOCH" era)
-> ShelleyTickPredFailure era
PredicateFailure (ShelleyNEWEPOCH era)
-> PredicateFailure (ShelleyTICK era)
forall era.
PredicateFailure (EraRule "NEWEPOCH" era)
-> ShelleyTickPredFailure era
NewEpochFailure
  wrapEvent :: Event (ShelleyNEWEPOCH era) -> Event (ShelleyTICK era)
wrapEvent = Event (EraRule "NEWEPOCH" era) -> ShelleyTickEvent era
Event (ShelleyNEWEPOCH era) -> Event (ShelleyTICK era)
forall era. Event (EraRule "NEWEPOCH" era) -> ShelleyTickEvent era
TickNewEpochEvent

instance
  ( Era era
  , STS (ShelleyRUPD era)
  , PredicateFailure (EraRule "RUPD" era) ~ ShelleyRupdPredFailure era
  , Event (EraRule "RUPD" era) ~ RupdEvent
  ) =>
  Embed (ShelleyRUPD era) (ShelleyTICK era)
  where
  wrapFailed :: PredicateFailure (ShelleyRUPD era)
-> PredicateFailure (ShelleyTICK era)
wrapFailed = PredicateFailure (EraRule "RUPD" era) -> ShelleyTickPredFailure era
PredicateFailure (ShelleyRUPD era)
-> PredicateFailure (ShelleyTICK era)
forall era.
PredicateFailure (EraRule "RUPD" era) -> ShelleyTickPredFailure era
RupdFailure
  wrapEvent :: Event (ShelleyRUPD era) -> Event (ShelleyTICK era)
wrapEvent = Event (EraRule "RUPD" era) -> ShelleyTickEvent era
Event (ShelleyRUPD era) -> Event (ShelleyTICK era)
forall era. Event (EraRule "RUPD" era) -> ShelleyTickEvent era
TickRupdEvent

{------------------------------------------------------------------------------
-- TICKF transition

-- This is a variant on the TICK transition called only by the consensus layer
to tick the ledger state to a future slot.
------------------------------------------------------------------------------}

newtype ShelleyTickfPredFailure era
  = TickfUpecFailure (PredicateFailure (EraRule "UPEC" era)) -- Subtransition Failures
  deriving ((forall x.
 ShelleyTickfPredFailure era -> Rep (ShelleyTickfPredFailure era) x)
-> (forall x.
    Rep (ShelleyTickfPredFailure era) x -> ShelleyTickfPredFailure era)
-> Generic (ShelleyTickfPredFailure era)
forall x.
Rep (ShelleyTickfPredFailure era) x -> ShelleyTickfPredFailure era
forall x.
ShelleyTickfPredFailure era -> Rep (ShelleyTickfPredFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyTickfPredFailure era) x -> ShelleyTickfPredFailure era
forall era x.
ShelleyTickfPredFailure era -> Rep (ShelleyTickfPredFailure era) x
$cfrom :: forall era x.
ShelleyTickfPredFailure era -> Rep (ShelleyTickfPredFailure era) x
from :: forall x.
ShelleyTickfPredFailure era -> Rep (ShelleyTickfPredFailure era) x
$cto :: forall era x.
Rep (ShelleyTickfPredFailure era) x -> ShelleyTickfPredFailure era
to :: forall x.
Rep (ShelleyTickfPredFailure era) x -> ShelleyTickfPredFailure era
Generic)

deriving stock instance
  ( Era era
  , Show (PredicateFailure (EraRule "UPEC" era))
  ) =>
  Show (ShelleyTickfPredFailure era)

deriving stock instance
  ( Era era
  , Eq (PredicateFailure (EraRule "UPEC" era))
  ) =>
  Eq (ShelleyTickfPredFailure era)

instance
  NoThunks (PredicateFailure (EraRule "UPEC" era)) =>
  NoThunks (ShelleyTickfPredFailure era)

newtype ShelleyTickfEvent era
  = TickfUpecEvent (Event (EraRule "UPEC" era)) -- Subtransition Events

instance
  ( EraGov era
  , EraCertState era
  , GovState era ~ ShelleyGovState era
  , State (EraRule "PPUP" era) ~ ShelleyGovState era
  , Signal (EraRule "UPEC" era) ~ ()
  , State (EraRule "UPEC" era) ~ UpecState era
  , Environment (EraRule "UPEC" era) ~ LedgerState era
  , Embed (EraRule "UPEC" era) (ShelleyTICKF era)
  ) =>
  STS (ShelleyTICKF era)
  where
  type State (ShelleyTICKF era) = NewEpochState era
  type Signal (ShelleyTICKF era) = SlotNo
  type Environment (ShelleyTICKF era) = ()
  type BaseM (ShelleyTICKF era) = ShelleyBase
  type PredicateFailure (ShelleyTICKF era) = ShelleyTickfPredFailure era
  type Event (ShelleyTICKF era) = ShelleyTickfEvent era

  initialRules :: [InitialRule (ShelleyTICKF era)]
initialRules = []
  transitionRules :: [TransitionRule (ShelleyTICKF era)]
transitionRules =
    [ do
        TRC ((), State (ShelleyTICKF era)
nes, Signal (ShelleyTICKF era)
slot) <- Rule
  (ShelleyTICKF era)
  'Transition
  (RuleContext 'Transition (ShelleyTICKF era))
F (Clause (ShelleyTICKF era) 'Transition) (TRC (ShelleyTICKF era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        NewEpochState era -> SlotNo -> TransitionRule (ShelleyTICKF era)
forall (tick :: * -> *) era.
(State (tick era) ~ NewEpochState era,
 BaseM (tick era) ~ ShelleyBase,
 State (EraRule "UPEC" era) ~ UpecState era,
 Signal (EraRule "UPEC" era) ~ (),
 Environment (EraRule "UPEC" era) ~ LedgerState era,
 Embed (EraRule "UPEC" era) (tick era), STS (tick era),
 GovState era ~ ShelleyGovState era, EraGov era,
 EraCertState era) =>
NewEpochState era -> SlotNo -> TransitionRule (tick era)
validatingTickTransitionFORECAST State (ShelleyTICKF era)
NewEpochState era
nes SlotNo
Signal (ShelleyTICKF era)
slot
    ]

instance
  ( Era era
  , STS (ShelleyUPEC era)
  , PredicateFailure (EraRule "UPEC" era) ~ ShelleyUpecPredFailure era
  , Event (EraRule "UPEC" era) ~ Void
  ) =>
  Embed (ShelleyUPEC era) (ShelleyTICKF era)
  where
  wrapFailed :: PredicateFailure (ShelleyUPEC era)
-> PredicateFailure (ShelleyTICKF era)
wrapFailed = PredicateFailure (EraRule "UPEC" era)
-> ShelleyTickfPredFailure era
PredicateFailure (ShelleyUPEC era)
-> PredicateFailure (ShelleyTICKF era)
forall era.
PredicateFailure (EraRule "UPEC" era)
-> ShelleyTickfPredFailure era
TickfUpecFailure
  wrapEvent :: Event (ShelleyUPEC era) -> Event (ShelleyTICKF era)
wrapEvent = Event (EraRule "UPEC" era) -> ShelleyTickfEvent era
Event (ShelleyUPEC era) -> Event (ShelleyTICKF era)
forall era. Event (EraRule "UPEC" era) -> ShelleyTickfEvent era
TickfUpecEvent