{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDeriving #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# 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,
  ShelleyTickEvent (..),
  PredicateFailure,
  adoptGenesisDelegs,
  ShelleyTICKF,
  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)
import Cardano.Ledger.Shelley.Rules.Rupd (
  RupdEnv (..),
  RupdEvent,
  ShelleyRUPD,
 )
import Cardano.Ledger.Shelley.Rules.Upec (ShelleyUPEC, UpecState (..))
import Cardano.Ledger.Slot (EpochNo, SlotNo, getTheSlotOfNoReturn)
import Cardano.Ledger.State (EraCertState (..), SnapShots (ssStakeMark, ssStakeMarkPoolDistr))
import Control.DeepSeq (NFData)
import Control.State.Transition
import qualified Data.Map.Strict as Map
import Data.Void (Void)
import GHC.Generics (Generic)
import Lens.Micro ((%~), (&), (.~), (^.))

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

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) = Void
  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 GenesisRole) 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 GenesisRole
_) GenDelegPair
_ -> SlotNo
s SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
<= SlotNo
slot) Map FutureGenDeleg GenDelegPair
fGenDelegs
    latestPerGKey :: FutureGenDeleg
-> b
-> Map (KeyHash GenesisRole) (SlotNo, b)
-> Map (KeyHash GenesisRole) (SlotNo, b)
latestPerGKey (FutureGenDeleg SlotNo
s KeyHash GenesisRole
genKeyHash) b
delegate Map (KeyHash GenesisRole) (SlotNo, b)
latest =
      case KeyHash GenesisRole
-> Map (KeyHash GenesisRole) (SlotNo, b) -> Maybe (SlotNo, b)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KeyHash GenesisRole
genKeyHash Map (KeyHash GenesisRole) (SlotNo, b)
latest of
        Maybe (SlotNo, b)
Nothing -> KeyHash GenesisRole
-> (SlotNo, b)
-> Map (KeyHash GenesisRole) (SlotNo, b)
-> Map (KeyHash GenesisRole) (SlotNo, b)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert KeyHash GenesisRole
genKeyHash (SlotNo
s, b
delegate) Map (KeyHash GenesisRole) (SlotNo, b)
latest
        Just (SlotNo
t, b
_) ->
          if SlotNo
s SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
> SlotNo
t
            then KeyHash GenesisRole
-> (SlotNo, b)
-> Map (KeyHash GenesisRole) (SlotNo, b)
-> Map (KeyHash GenesisRole) (SlotNo, b)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert KeyHash GenesisRole
genKeyHash (SlotNo
s, b
delegate) Map (KeyHash GenesisRole) (SlotNo, b)
latest
            else Map (KeyHash GenesisRole) (SlotNo, b)
latest
    genDelegs' :: Map (KeyHash GenesisRole) GenDelegPair
genDelegs' = ((SlotNo, GenDelegPair) -> GenDelegPair)
-> Map (KeyHash GenesisRole) (SlotNo, GenDelegPair)
-> Map (KeyHash GenesisRole) 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 GenesisRole) (SlotNo, GenDelegPair)
 -> Map (KeyHash GenesisRole) GenDelegPair)
-> Map (KeyHash GenesisRole) (SlotNo, GenDelegPair)
-> Map (KeyHash GenesisRole) GenDelegPair
forall a b. (a -> b) -> a -> b
$ (FutureGenDeleg
 -> GenDelegPair
 -> Map (KeyHash GenesisRole) (SlotNo, GenDelegPair)
 -> Map (KeyHash GenesisRole) (SlotNo, GenDelegPair))
-> Map (KeyHash GenesisRole) (SlotNo, GenDelegPair)
-> Map FutureGenDeleg GenDelegPair
-> Map (KeyHash GenesisRole) (SlotNo, GenDelegPair)
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey FutureGenDeleg
-> GenDelegPair
-> Map (KeyHash GenesisRole) (SlotNo, GenDelegPair)
-> Map (KeyHash GenesisRole) (SlotNo, GenDelegPair)
forall {b}.
FutureGenDeleg
-> b
-> Map (KeyHash GenesisRole) (SlotNo, b)
-> Map (KeyHash GenesisRole) (SlotNo, b)
latestPerGKey Map (KeyHash GenesisRole) (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 $ Map.union 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
  (curEpochNo, slotOfNoReturn, _) <- HasCallStack => SlotNo -> ShelleyBase (EpochNo, SlotNo, EpochNo)
SlotNo -> ShelleyBase (EpochNo, SlotNo, EpochNo)
getTheSlotOfNoReturn SlotNo
slot
  pure
    ( curEpochNo
    , if slot < slotOfNoReturn
        then nes
        else nes & newEpochStateGovStateL . futurePParamsGovStateL %~ 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
  (curEpochNo, 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

  nes' <- trans @(EraRule "NEWEPOCH" era) $ TRC ((), nes, curEpochNo)
  let 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

  pure $ 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.

  (curEpochNo, 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 = NewEpochState era -> EpochState era
forall era. NewEpochState era -> EpochState era
nesEs NewEpochState era
nes
      ss = EpochState era -> SnapShots
forall era. EpochState era -> SnapShots
esSnapshots EpochState era
es

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

  -- note that the genesis delegates are updated not only on the epoch boundary.
  if curEpochNo /= succ (nesEL nes)
    then pure $ 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 = 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 = EpochState era -> LedgerState era
forall era. EpochState era -> LedgerState era
esLState EpochState era
es
          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 pp' _ <-
        trans @(EraRule "UPEC" era) $
          TRC (ls, UpecState pp updates, ())
      let 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'

      pure $!
        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@(NewEpochState _ bprev _ es _ _ _), 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

  nes1 <- validatingTickTransition @ShelleyTICK nes0 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 !_ = ssStakeMark . esSnapshots . nesEs $ nes1
      !_ = ssStakeMarkPoolDistr . esSnapshots . nesEs $ nes1

  ru'' <-
    trans @(EraRule "RUPD" era) $
      TRC (RupdEnv bprev es, nesRu nes1, slot)

  let nes2 = NewEpochState era
nes1 {nesRu = ru''}
  pure nes2

instance
  ( STS (ShelleyNEWEPOCH era)
  , Event (EraRule "NEWEPOCH" era) ~ ShelleyNewEpochEvent era
  ) =>
  Embed (ShelleyNEWEPOCH era) (ShelleyTICK era)
  where
  wrapFailed :: PredicateFailure (ShelleyNEWEPOCH era)
-> PredicateFailure (ShelleyTICK era)
wrapFailed = \case {}
  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)
  , Event (EraRule "RUPD" era) ~ RupdEvent
  ) =>
  Embed (ShelleyRUPD era) (ShelleyTICK era)
  where
  wrapFailed :: PredicateFailure (ShelleyRUPD era)
-> PredicateFailure (ShelleyTICK era)
wrapFailed = \case {}
  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 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) = Void
  type Event (ShelleyTICKF era) = ShelleyTickfEvent era

  initialRules :: [InitialRule (ShelleyTICKF era)]
initialRules = []
  transitionRules :: [TransitionRule (ShelleyTICKF era)]
transitionRules =
    [ do
        TRC ((), nes, 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
        validatingTickTransitionFORECAST nes slot
    ]

instance
  ( Era era
  , STS (ShelleyUPEC era)
  , Event (EraRule "UPEC" era) ~ Void
  ) =>
  Embed (ShelleyUPEC era) (ShelleyTICKF era)
  where
  wrapFailed :: PredicateFailure (ShelleyUPEC era)
-> PredicateFailure (ShelleyTICKF era)
wrapFailed = \case {}
  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