{-# 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 #-}
#if __GLASGOW_HASKELL__ >= 908
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
#endif

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.EpochBoundary (SnapShots (ssStakeMark, ssStakeMarkPoolDistr))
import Cardano.Ledger.Keys (GenDelegs (..))
import Cardano.Ledger.Shelley.Era (ShelleyEra, ShelleyTICK, ShelleyTICKF)
import Cardano.Ledger.Shelley.Governance
import Cardano.Ledger.Shelley.LedgerState (
  CertState (..),
  DState (..),
  EpochState (..),
  FutureGenDeleg (..),
  LedgerState (..),
  NewEpochState (..),
  PulsingRewUpdate,
  UTxOState (..),
  curPParamsEpochStateL,
  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 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 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
$cto :: forall era x.
Rep (ShelleyTickPredFailure era) x -> ShelleyTickPredFailure era
$cfrom :: forall era x.
ShelleyTickPredFailure era -> Rep (ShelleyTickPredFailure era) x
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 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
$cto :: forall era x. Rep (ShelleyTickEvent era) x -> ShelleyTickEvent era
$cfrom :: forall era x. ShelleyTickEvent era -> Rep (ShelleyTickEvent era) x
Generic)

type instance EraRuleEvent "TICK" (ShelleyEra c) = ShelleyTickEvent (ShelleyEra c)

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
  , 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 (EraCrypto era))
  , 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 = [forall era.
(EraGov era, Embed (EraRule "NEWEPOCH" era) (ShelleyTICK era),
 Embed (EraRule "RUPD" era) (ShelleyTICK era),
 STS (ShelleyTICK era), State (ShelleyTICK era) ~ NewEpochState era,
 BaseM (ShelleyTICK era) ~ ShelleyBase,
 Environment (EraRule "RUPD" era) ~ RupdEnv era,
 State (EraRule "RUPD" era)
 ~ StrictMaybe (PulsingRewUpdate (EraCrypto era)),
 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 ::
  EpochState era ->
  SlotNo ->
  EpochState era
adoptGenesisDelegs :: forall era. EpochState era -> SlotNo -> EpochState era
adoptGenesisDelegs EpochState era
es SlotNo
slot = EpochState era
es'
  where
    ls :: LedgerState era
ls = forall era. EpochState era -> LedgerState era
esLState EpochState era
es
    dp :: CertState era
dp = forall era. LedgerState era -> CertState era
lsCertState LedgerState era
ls
    ds :: DState era
ds = forall era. CertState era -> DState era
certDState CertState era
dp
    fGenDelegs :: Map (FutureGenDeleg (EraCrypto era)) (GenDelegPair (EraCrypto era))
fGenDelegs = forall era.
DState era
-> Map
     (FutureGenDeleg (EraCrypto era)) (GenDelegPair (EraCrypto era))
dsFutureGenDelegs DState era
ds
    GenDelegs Map
  (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
genDelegs = forall era. DState era -> GenDelegs (EraCrypto era)
dsGenDelegs DState era
ds
    (Map (FutureGenDeleg (EraCrypto era)) (GenDelegPair (EraCrypto era))
curr, Map (FutureGenDeleg (EraCrypto era)) (GenDelegPair (EraCrypto era))
fGenDelegs') = forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey (\(FutureGenDeleg SlotNo
s KeyHash 'Genesis (EraCrypto era)
_) GenDelegPair (EraCrypto era)
_ -> SlotNo
s forall a. Ord a => a -> a -> Bool
<= SlotNo
slot) Map (FutureGenDeleg (EraCrypto era)) (GenDelegPair (EraCrypto era))
fGenDelegs
    latestPerGKey :: FutureGenDeleg c
-> b
-> Map (KeyHash 'Genesis c) (SlotNo, b)
-> Map (KeyHash 'Genesis c) (SlotNo, b)
latestPerGKey (FutureGenDeleg SlotNo
s KeyHash 'Genesis c
genKeyHash) b
delegate Map (KeyHash 'Genesis c) (SlotNo, b)
latest =
      case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KeyHash 'Genesis c
genKeyHash Map (KeyHash 'Genesis c) (SlotNo, b)
latest of
        Maybe (SlotNo, b)
Nothing -> forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert KeyHash 'Genesis c
genKeyHash (SlotNo
s, b
delegate) Map (KeyHash 'Genesis c) (SlotNo, b)
latest
        Just (SlotNo
t, b
_) ->
          if SlotNo
s forall a. Ord a => a -> a -> Bool
> SlotNo
t
            then forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert KeyHash 'Genesis c
genKeyHash (SlotNo
s, b
delegate) Map (KeyHash 'Genesis c) (SlotNo, b)
latest
            else Map (KeyHash 'Genesis c) (SlotNo, b)
latest
    genDelegs' :: Map
  (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
genDelegs' = forall a b k. (a -> b) -> Map k a -> Map k b
Map.map forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey forall {c} {b}.
FutureGenDeleg c
-> b
-> Map (KeyHash 'Genesis c) (SlotNo, b)
-> Map (KeyHash 'Genesis c) (SlotNo, b)
latestPerGKey forall k a. Map k a
Map.empty Map (FutureGenDeleg (EraCrypto era)) (GenDelegPair (EraCrypto era))
curr
    ds' :: DState era
ds' =
      DState era
ds
        { dsFutureGenDelegs :: Map (FutureGenDeleg (EraCrypto era)) (GenDelegPair (EraCrypto era))
dsFutureGenDelegs = Map (FutureGenDeleg (EraCrypto era)) (GenDelegPair (EraCrypto era))
fGenDelegs'
        , dsGenDelegs :: GenDelegs (EraCrypto era)
dsGenDelegs = forall c. Map (KeyHash 'Genesis c) (GenDelegPair c) -> GenDelegs c
GenDelegs forall a b. (a -> b) -> a -> b
$ forall s t. Embed s t => Exp t -> s
eval (Map
  (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
genDelegs forall k s1 (f :: * -> * -> *) v s2 (g :: * -> * -> *).
(Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) =>
s1 -> s2 -> Exp (f k v)
⨃ Map
  (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
genDelegs')
        }
    dp' :: CertState era
dp' = CertState era
dp {certDState :: DState era
certDState = DState era
ds'}
    ls' :: LedgerState era
ls' = LedgerState era
ls {lsCertState :: CertState era
lsCertState = CertState era
dp'}
    es' :: EpochState era
es' = EpochState era
es {esLState :: LedgerState era
esLState = LedgerState era
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)
getTheSlotOfNoReturn SlotNo
slot
  forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( EpochNo
curEpochNo
    , if SlotNo
slot forall a. Ord a => a -> a -> Bool
< SlotNo
slotOfNoReturn
        then NewEpochState era
nes
        else NewEpochState era
nes forall a b. a -> (a -> b) -> b
& forall era. Lens' (NewEpochState era) (GovState era)
newEpochStateGovStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraGov era => Lens' (GovState era) (FuturePParams era)
futurePParamsGovStateL forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ 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
  , 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, 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) <- forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS forall a b. (a -> b) -> a -> b
$ 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) forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC ((), NewEpochState era
nes, EpochNo
curEpochNo)
  let es'' :: EpochState era
es'' = forall era. EpochState era -> SlotNo -> EpochState era
adoptGenesisDelegs (forall era. NewEpochState era -> EpochState era
nesEs NewEpochState era
nes') SlotNo
slot

  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ NewEpochState era
nes' {nesEs :: EpochState era
nesEs = EpochState era
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
  ) =>
  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) =>
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) <- forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS forall a b. (a -> b) -> a -> b
$ forall era.
EraGov era =>
NewEpochState era
-> SlotNo -> ShelleyBase (EpochNo, NewEpochState era)
solidifyNextEpochPParams NewEpochState era
nes0 SlotNo
slot

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

  -- the relevant 'NEWEPOCH' logic
  let pd' :: PoolDistr (EraCrypto era)
pd' = forall c. SnapShots c -> PoolDistr c
ssStakeMarkPoolDistr SnapShots (EraCrypto era)
ss

  -- note that the genesis delegates are updated not only on the epoch boundary.
  if EpochNo
curEpochNo forall a. Eq a => a -> a -> Bool
/= forall a. Enum a => a -> a
succ (forall era. NewEpochState era -> EpochNo
nesEL NewEpochState era
nes)
    then forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ NewEpochState era
nes {nesEs :: EpochState era
nesEs = forall era. EpochState era -> SlotNo -> EpochState era
adoptGenesisDelegs EpochState era
es SlotNo
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 forall s a. s -> Getting a s a -> a
^. forall era. EraGov era => Lens' (EpochState era) (PParams era)
curPParamsEpochStateL
          ls :: LedgerState era
ls = forall era. EpochState era -> LedgerState era
esLState EpochState era
es
          updates :: GovState era
updates = forall era. UTxOState era -> GovState era
utxosGovState forall a b. (a -> b) -> a -> b
$ 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) forall a b. (a -> b) -> a -> b
$
          forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (LedgerState era
ls, forall era. PParams era -> ShelleyGovState era -> UpecState era
UpecState PParams era
pp GovState era
updates, ())
      let es' :: EpochState era
es' =
            forall era. EpochState era -> SlotNo -> EpochState era
adoptGenesisDelegs EpochState era
es SlotNo
slot
              forall a b. a -> (a -> b) -> b
& forall era. EraGov era => Lens' (EpochState era) (PParams era)
curPParamsEpochStateL forall s t a b. ASetter s t a b -> b -> s -> t
.~ PParams era
pp'

      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$!
        NewEpochState era
nes
          { nesPd :: PoolDistr (EraCrypto era)
nesPd = PoolDistr (EraCrypto era)
pd'
          , nesEs :: EpochState era
nesEs = EpochState era
es'
          }

bheadTransition ::
  forall era.
  ( EraGov era
  , Embed (EraRule "NEWEPOCH" era) (ShelleyTICK era)
  , Embed (EraRule "RUPD" era) (ShelleyTICK era)
  , STS (ShelleyTICK era)
  , State (ShelleyTICK era) ~ NewEpochState era
  , BaseM (ShelleyTICK era) ~ ShelleyBase
  , Environment (EraRule "RUPD" era) ~ RupdEnv era
  , State (EraRule "RUPD" era) ~ StrictMaybe (PulsingRewUpdate (EraCrypto era))
  , 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, Embed (EraRule "NEWEPOCH" era) (ShelleyTICK era),
 Embed (EraRule "RUPD" era) (ShelleyTICK era),
 STS (ShelleyTICK era), State (ShelleyTICK era) ~ NewEpochState era,
 BaseM (ShelleyTICK era) ~ ShelleyBase,
 Environment (EraRule "RUPD" era) ~ RupdEnv era,
 State (EraRule "RUPD" era)
 ~ StrictMaybe (PulsingRewUpdate (EraCrypto era)),
 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 (EraCrypto era)
bprev BlocksMade (EraCrypto era)
_ EpochState era
es StrictMaybe (PulsingRewUpdate (EraCrypto era))
_ PoolDistr (EraCrypto era)
_ StashedAVVMAddresses era
_), Signal (ShelleyTICK era)
slot) <-
    forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext

  NewEpochState era
nes1 <- forall (tick :: * -> *) era.
(EraGov 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)
nes0 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 (EraCrypto era)
_ = forall c. SnapShots c -> SnapShot c
ssStakeMark forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EpochState era -> SnapShots (EraCrypto era)
esSnapshots forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. NewEpochState era -> EpochState era
nesEs forall a b. (a -> b) -> a -> b
$ NewEpochState era
nes1
      !PoolDistr (EraCrypto era)
_ = forall c. SnapShots c -> PoolDistr c
ssStakeMarkPoolDistr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EpochState era -> SnapShots (EraCrypto era)
esSnapshots forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. NewEpochState era -> EpochState era
nesEs forall a b. (a -> b) -> a -> b
$ NewEpochState era
nes1

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

  let nes2 :: NewEpochState era
nes2 = NewEpochState era
nes1 {nesRu :: StrictMaybe (PulsingRewUpdate (EraCrypto era))
nesRu = StrictMaybe (PulsingRewUpdate (EraCrypto era))
ru''}
  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 = forall era.
PredicateFailure (EraRule "NEWEPOCH" era)
-> ShelleyTickPredFailure era
NewEpochFailure
  wrapEvent :: Event (ShelleyNEWEPOCH era) -> Event (ShelleyTICK era)
wrapEvent = 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 (EraCrypto era)
  ) =>
  Embed (ShelleyRUPD era) (ShelleyTICK era)
  where
  wrapFailed :: PredicateFailure (ShelleyRUPD era)
-> PredicateFailure (ShelleyTICK era)
wrapFailed = forall era.
PredicateFailure (EraRule "RUPD" era) -> ShelleyTickPredFailure era
RupdFailure
  wrapEvent :: Event (ShelleyRUPD era) -> Event (ShelleyTICK era)
wrapEvent = 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 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
$cto :: forall era x.
Rep (ShelleyTickfPredFailure era) x -> ShelleyTickfPredFailure era
$cfrom :: forall era x.
ShelleyTickfPredFailure era -> Rep (ShelleyTickfPredFailure era) x
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
  , 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) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        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) =>
NewEpochState era -> SlotNo -> TransitionRule (tick era)
validatingTickTransitionFORECAST State (ShelleyTICKF era)
nes 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 = forall era.
PredicateFailure (EraRule "UPEC" era)
-> ShelleyTickfPredFailure era
TickfUpecFailure
  wrapEvent :: Event (ShelleyUPEC era) -> Event (ShelleyTICKF era)
wrapEvent = forall era. Event (EraRule "UPEC" era) -> ShelleyTickfEvent era
TickfUpecEvent