{-# 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.SetAlgebra (eval, (⨃))
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 $ 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
  (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