{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Cardano.Ledger.Shelley.Rules.Tick
  ( TICK,
    State,
    TickPredicateFailure (..),
    TickEvent (..),
    PredicateFailure,
    adoptGenesisDelegs,
    TICKF,
    TickfPredicateFailure (..),
  )
where

import Cardano.Ledger.BaseTypes (ShelleyBase, StrictMaybe (..), epochInfoPure)
import qualified Cardano.Ledger.Core as Core
import Cardano.Ledger.Era (Crypto, Era)
import Cardano.Ledger.Keys (GenDelegs (..))
import Cardano.Ledger.Shelley.Constraints (UsesTxOut, UsesValue)
import Cardano.Ledger.Shelley.EpochBoundary (SnapShots (_pstakeMark))
import Cardano.Ledger.Shelley.LedgerState
  ( DPState (..),
    DState (..),
    EpochState (..),
    FutureGenDeleg (..),
    LedgerState (..),
    NewEpochState (..),
    PulsingRewUpdate,
  )
import Cardano.Ledger.Shelley.Rules.NewEpoch (NEWEPOCH, NewEpochEvent, NewEpochPredicateFailure)
import Cardano.Ledger.Shelley.Rules.Rupd (RUPD, RupdEnv (..), RupdEvent, RupdPredicateFailure)
import Cardano.Ledger.Slot (EpochNo, SlotNo, epochInfoEpoch)
import Control.Monad.Trans.Reader (asks)
import Control.SetAlgebra (eval, (⨃))
import Control.State.Transition
import qualified Data.Map.Strict as Map
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))

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

data TICK era

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

deriving stock instance
  ( Show (PredicateFailure (Core.EraRule "NEWEPOCH" era)),
    Show (PredicateFailure (Core.EraRule "RUPD" era))
  ) =>
  Show (TickPredicateFailure era)

deriving stock instance
  ( Eq (PredicateFailure (Core.EraRule "NEWEPOCH" era)),
    Eq (PredicateFailure (Core.EraRule "RUPD" era))
  ) =>
  Eq (TickPredicateFailure era)

instance
  ( NoThunks (PredicateFailure (Core.EraRule "NEWEPOCH" era)),
    NoThunks (PredicateFailure (Core.EraRule "RUPD" era))
  ) =>
  NoThunks (TickPredicateFailure era)

data TickEvent era
  = NewEpochEvent (Event (Core.EraRule "NEWEPOCH" era))
  | RupdEvent (Event (Core.EraRule "RUPD" era))
  deriving ((forall x. TickEvent era -> Rep (TickEvent era) x)
-> (forall x. Rep (TickEvent era) x -> TickEvent era)
-> Generic (TickEvent era)
forall x. Rep (TickEvent era) x -> TickEvent era
forall x. TickEvent era -> Rep (TickEvent era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x. Rep (TickEvent era) x -> TickEvent era
forall era x. TickEvent era -> Rep (TickEvent era) x
$cto :: forall era x. Rep (TickEvent era) x -> TickEvent era
$cfrom :: forall era x. TickEvent era -> Rep (TickEvent era) x
Generic)

instance
  ( Era era,
    Embed (Core.EraRule "NEWEPOCH" era) (TICK era),
    Embed (Core.EraRule "RUPD" era) (TICK era),
    State (TICK era) ~ NewEpochState era,
    BaseM (TICK era) ~ ShelleyBase,
    Environment (Core.EraRule "RUPD" era) ~ RupdEnv era,
    State (Core.EraRule "RUPD" era) ~ StrictMaybe (PulsingRewUpdate (Crypto era)),
    Signal (Core.EraRule "RUPD" era) ~ SlotNo,
    Environment (Core.EraRule "NEWEPOCH" era) ~ (),
    State (Core.EraRule "NEWEPOCH" era) ~ NewEpochState era,
    Signal (Core.EraRule "NEWEPOCH" era) ~ EpochNo
  ) =>
  STS (TICK era)
  where
  type
    State (TICK era) =
      NewEpochState era
  type
    Signal (TICK era) =
      SlotNo
  type Environment (TICK era) = ()
  type BaseM (TICK era) = ShelleyBase
  type PredicateFailure (TICK era) = TickPredicateFailure era
  type Event (TICK era) = TickEvent era

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

adoptGenesisDelegs ::
  EpochState era ->
  SlotNo ->
  EpochState era
adoptGenesisDelegs :: 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 :: DPState (Crypto era)
dp = LedgerState era -> DPState (Crypto era)
forall era. LedgerState era -> DPState (Crypto era)
lsDPState LedgerState era
ls
    ds :: DState (Crypto era)
ds = DPState (Crypto era) -> DState (Crypto era)
forall crypto. DPState crypto -> DState crypto
dpsDState DPState (Crypto era)
dp
    fGenDelegs :: Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
fGenDelegs = DState (Crypto era)
-> Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
forall crypto.
DState crypto -> Map (FutureGenDeleg crypto) (GenDelegPair crypto)
_fGenDelegs DState (Crypto era)
ds
    GenDelegs Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
genDelegs = DState (Crypto era) -> GenDelegs (Crypto era)
forall crypto. DState crypto -> GenDelegs crypto
_genDelegs DState (Crypto era)
ds
    (Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
curr, Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
fGenDelegs') = (FutureGenDeleg (Crypto era) -> GenDelegPair (Crypto era) -> Bool)
-> Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
-> (Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era)),
    Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era)))
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey (\(FutureGenDeleg SlotNo
s KeyHash 'Genesis (Crypto era)
_) GenDelegPair (Crypto era)
_ -> SlotNo
s SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
<= SlotNo
slot) Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
fGenDelegs
    latestPerGKey :: FutureGenDeleg crypto
-> b
-> Map (KeyHash 'Genesis crypto) (SlotNo, b)
-> Map (KeyHash 'Genesis crypto) (SlotNo, b)
latestPerGKey (FutureGenDeleg SlotNo
s KeyHash 'Genesis crypto
genKeyHash) b
delegate Map (KeyHash 'Genesis crypto) (SlotNo, b)
latest =
      case KeyHash 'Genesis crypto
-> Map (KeyHash 'Genesis crypto) (SlotNo, b) -> Maybe (SlotNo, b)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KeyHash 'Genesis crypto
genKeyHash Map (KeyHash 'Genesis crypto) (SlotNo, b)
latest of
        Maybe (SlotNo, b)
Nothing -> KeyHash 'Genesis crypto
-> (SlotNo, b)
-> Map (KeyHash 'Genesis crypto) (SlotNo, b)
-> Map (KeyHash 'Genesis crypto) (SlotNo, b)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert KeyHash 'Genesis crypto
genKeyHash (SlotNo
s, b
delegate) Map (KeyHash 'Genesis crypto) (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 crypto
-> (SlotNo, b)
-> Map (KeyHash 'Genesis crypto) (SlotNo, b)
-> Map (KeyHash 'Genesis crypto) (SlotNo, b)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert KeyHash 'Genesis crypto
genKeyHash (SlotNo
s, b
delegate) Map (KeyHash 'Genesis crypto) (SlotNo, b)
latest
            else Map (KeyHash 'Genesis crypto) (SlotNo, b)
latest
    genDelegs' :: Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
genDelegs' = ((SlotNo, GenDelegPair (Crypto era)) -> GenDelegPair (Crypto era))
-> Map
     (KeyHash 'Genesis (Crypto era)) (SlotNo, GenDelegPair (Crypto era))
-> Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (SlotNo, GenDelegPair (Crypto era)) -> GenDelegPair (Crypto era)
forall a b. (a, b) -> b
snd (Map
   (KeyHash 'Genesis (Crypto era)) (SlotNo, GenDelegPair (Crypto era))
 -> Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era)))
-> Map
     (KeyHash 'Genesis (Crypto era)) (SlotNo, GenDelegPair (Crypto era))
-> Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
forall a b. (a -> b) -> a -> b
$ (FutureGenDeleg (Crypto era)
 -> GenDelegPair (Crypto era)
 -> Map
      (KeyHash 'Genesis (Crypto era)) (SlotNo, GenDelegPair (Crypto era))
 -> Map
      (KeyHash 'Genesis (Crypto era))
      (SlotNo, GenDelegPair (Crypto era)))
-> Map
     (KeyHash 'Genesis (Crypto era)) (SlotNo, GenDelegPair (Crypto era))
-> Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
-> Map
     (KeyHash 'Genesis (Crypto era)) (SlotNo, GenDelegPair (Crypto era))
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey FutureGenDeleg (Crypto era)
-> GenDelegPair (Crypto era)
-> Map
     (KeyHash 'Genesis (Crypto era)) (SlotNo, GenDelegPair (Crypto era))
-> Map
     (KeyHash 'Genesis (Crypto era)) (SlotNo, GenDelegPair (Crypto era))
forall crypto b.
FutureGenDeleg crypto
-> b
-> Map (KeyHash 'Genesis crypto) (SlotNo, b)
-> Map (KeyHash 'Genesis crypto) (SlotNo, b)
latestPerGKey Map
  (KeyHash 'Genesis (Crypto era)) (SlotNo, GenDelegPair (Crypto era))
forall k a. Map k a
Map.empty Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
curr
    ds' :: DState (Crypto era)
ds' =
      DState (Crypto era)
ds
        { _fGenDelegs :: Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
_fGenDelegs = Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
fGenDelegs',
          _genDelegs :: GenDelegs (Crypto era)
_genDelegs = Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
-> GenDelegs (Crypto era)
forall crypto.
Map (KeyHash 'Genesis crypto) (GenDelegPair crypto)
-> GenDelegs crypto
GenDelegs (Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
 -> GenDelegs (Crypto era))
-> Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
-> GenDelegs (Crypto era)
forall a b. (a -> b) -> a -> b
$ Exp
  (Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era)))
-> Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
forall s t. Embed s t => Exp t -> s
eval (Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
genDelegs Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
-> Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
-> Exp
     (Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era)))
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 (Crypto era)) (GenDelegPair (Crypto era))
genDelegs')
        }
    dp' :: DPState (Crypto era)
dp' = DPState (Crypto era)
dp {dpsDState :: DState (Crypto era)
dpsDState = DState (Crypto era)
ds'}
    ls' :: LedgerState era
ls' = LedgerState era
ls {lsDPState :: DPState (Crypto era)
lsDPState = DPState (Crypto era)
dp'}
    es' :: EpochState era
es' = EpochState era
es {esLState :: LedgerState era
esLState = LedgerState era
ls'}

-- | This is a limited version of 'bheadTransition' which is suitable for the
-- future ledger view.
validatingTickTransition ::
  forall tick era.
  ( Embed (Core.EraRule "NEWEPOCH" era) (tick era),
    STS (tick era),
    State (tick era) ~ NewEpochState era,
    BaseM (tick era) ~ ShelleyBase,
    Environment (Core.EraRule "NEWEPOCH" era) ~ (),
    State (Core.EraRule "NEWEPOCH" era) ~ NewEpochState era,
    Signal (Core.EraRule "NEWEPOCH" era) ~ EpochNo
  ) =>
  NewEpochState era ->
  SlotNo ->
  TransitionRule (tick era)
validatingTickTransition :: NewEpochState era -> SlotNo -> TransitionRule (tick era)
validatingTickTransition NewEpochState era
nes SlotNo
slot = do
  EpochNo
epoch <- BaseM (tick era) EpochNo -> Rule (tick era) 'Transition EpochNo
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (tick era) EpochNo -> Rule (tick era) 'Transition EpochNo)
-> BaseM (tick era) EpochNo -> Rule (tick era) 'Transition EpochNo
forall a b. (a -> b) -> a -> b
$ do
    EpochInfo Identity
ei <- (Globals -> EpochInfo Identity)
-> ReaderT Globals Identity (EpochInfo Identity)
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> EpochInfo Identity
epochInfoPure
    HasCallStack => EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
epochInfoEpoch EpochInfo Identity
ei SlotNo
slot

  NewEpochState era
nes' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (EraRule "NEWEPOCH" era) super =>
RuleContext rtype (EraRule "NEWEPOCH" era)
-> Rule super rtype (State (EraRule "NEWEPOCH" era))
trans @(Core.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)
epoch)
  let es'' :: EpochState era
es'' = EpochState era -> SlotNo -> EpochState era
forall 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 (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 :: EpochState era
nesEs = EpochState era
es''}

bheadTransition ::
  forall era.
  ( Embed (Core.EraRule "NEWEPOCH" era) (TICK era),
    Embed (Core.EraRule "RUPD" era) (TICK era),
    STS (TICK era),
    State (TICK era) ~ NewEpochState era,
    BaseM (TICK era) ~ ShelleyBase,
    Environment (Core.EraRule "RUPD" era) ~ RupdEnv era,
    State (Core.EraRule "RUPD" era) ~ StrictMaybe (PulsingRewUpdate (Crypto era)),
    Signal (Core.EraRule "RUPD" era) ~ SlotNo,
    Environment (Core.EraRule "NEWEPOCH" era) ~ (),
    State (Core.EraRule "NEWEPOCH" era) ~ NewEpochState era,
    Signal (Core.EraRule "NEWEPOCH" era) ~ EpochNo
  ) =>
  TransitionRule (TICK era)
bheadTransition :: TransitionRule (TICK era)
bheadTransition = do
  TRC ((), nes :: State (TICK era)
nes@(NewEpochState _ bprev _ es _ _ _), Signal (TICK era)
slot) <-
    F (Clause (TICK era) 'Transition) (TRC (TICK era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext

  NewEpochState era
nes' <- NewEpochState era -> SlotNo -> TransitionRule (TICK era)
forall (tick :: * -> *) 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 @TICK State (TICK era)
NewEpochState era
nes SlotNo
Signal (TICK era)
slot

  -- Here we force the evaluation of the mark snapshot.
  -- 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 (Crypto era)
_ = SnapShots (Crypto era) -> SnapShot (Crypto era)
forall crypto. SnapShots crypto -> SnapShot crypto
_pstakeMark (SnapShots (Crypto era) -> SnapShot (Crypto era))
-> (NewEpochState era -> SnapShots (Crypto era))
-> NewEpochState era
-> SnapShot (Crypto era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpochState era -> SnapShots (Crypto era)
forall era. EpochState era -> SnapShots (Crypto era)
esSnapshots (EpochState era -> SnapShots (Crypto era))
-> (NewEpochState era -> EpochState era)
-> NewEpochState era
-> SnapShots (Crypto era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewEpochState era -> EpochState era
forall era. NewEpochState era -> EpochState era
nesEs (NewEpochState era -> SnapShot (Crypto era))
-> NewEpochState era -> SnapShot (Crypto era)
forall a b. (a -> b) -> a -> b
$ NewEpochState era
nes'

  StrictMaybe (PulsingRewUpdate (Crypto era))
ru'' <-
    forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (EraRule "RUPD" era) super =>
RuleContext rtype (EraRule "RUPD" era)
-> Rule super rtype (State (EraRule "RUPD" era))
trans @(Core.EraRule "RUPD" era) (RuleContext 'Transition (EraRule "RUPD" era)
 -> Rule (TICK era) 'Transition (State (EraRule "RUPD" era)))
-> RuleContext 'Transition (EraRule "RUPD" era)
-> Rule (TICK 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 (Crypto era) -> EpochState era -> RupdEnv era
forall era.
BlocksMade (Crypto era) -> EpochState era -> RupdEnv era
RupdEnv BlocksMade (Crypto era)
bprev EpochState era
es, NewEpochState era -> StrictMaybe (PulsingRewUpdate (Crypto era))
forall era.
NewEpochState era -> StrictMaybe (PulsingRewUpdate (Crypto era))
nesRu NewEpochState era
nes', Signal (EraRule "RUPD" era)
Signal (TICK era)
slot)

  let nes'' :: NewEpochState era
nes'' = NewEpochState era
nes' {nesRu :: StrictMaybe (PulsingRewUpdate (Crypto era))
nesRu = StrictMaybe (PulsingRewUpdate (Crypto era))
ru''}
  NewEpochState era
-> F (Clause (TICK era) 'Transition) (NewEpochState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure NewEpochState era
nes''

instance
  ( UsesTxOut era,
    UsesValue era,
    STS (NEWEPOCH era),
    PredicateFailure (Core.EraRule "NEWEPOCH" era) ~ NewEpochPredicateFailure era,
    Event (Core.EraRule "NEWEPOCH" era) ~ NewEpochEvent era
  ) =>
  Embed (NEWEPOCH era) (TICK era)
  where
  wrapFailed :: PredicateFailure (NEWEPOCH era) -> PredicateFailure (TICK era)
wrapFailed = PredicateFailure (NEWEPOCH era) -> PredicateFailure (TICK era)
forall era.
PredicateFailure (EraRule "NEWEPOCH" era)
-> TickPredicateFailure era
NewEpochFailure
  wrapEvent :: Event (NEWEPOCH era) -> Event (TICK era)
wrapEvent = Event (NEWEPOCH era) -> Event (TICK era)
forall era. Event (EraRule "NEWEPOCH" era) -> TickEvent era
NewEpochEvent

instance
  ( Era era,
    STS (RUPD era),
    PredicateFailure (Core.EraRule "RUPD" era) ~ RupdPredicateFailure era,
    Event (Core.EraRule "RUPD" era) ~ RupdEvent (Crypto era)
  ) =>
  Embed (RUPD era) (TICK era)
  where
  wrapFailed :: PredicateFailure (RUPD era) -> PredicateFailure (TICK era)
wrapFailed = PredicateFailure (RUPD era) -> PredicateFailure (TICK era)
forall era.
PredicateFailure (EraRule "RUPD" era) -> TickPredicateFailure era
RupdFailure
  wrapEvent :: Event (RUPD era) -> Event (TICK era)
wrapEvent = Event (RUPD era) -> Event (TICK era)
forall era. Event (EraRule "RUPD" era) -> TickEvent era
RupdEvent

{------------------------------------------------------------------------------
-- 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.
------------------------------------------------------------------------------}

data TICKF era

newtype TickfPredicateFailure era
  = TickfNewEpochFailure (PredicateFailure (Core.EraRule "NEWEPOCH" era)) -- Subtransition Failures
  deriving ((forall x.
 TickfPredicateFailure era -> Rep (TickfPredicateFailure era) x)
-> (forall x.
    Rep (TickfPredicateFailure era) x -> TickfPredicateFailure era)
-> Generic (TickfPredicateFailure era)
forall x.
Rep (TickfPredicateFailure era) x -> TickfPredicateFailure era
forall x.
TickfPredicateFailure era -> Rep (TickfPredicateFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (TickfPredicateFailure era) x -> TickfPredicateFailure era
forall era x.
TickfPredicateFailure era -> Rep (TickfPredicateFailure era) x
$cto :: forall era x.
Rep (TickfPredicateFailure era) x -> TickfPredicateFailure era
$cfrom :: forall era x.
TickfPredicateFailure era -> Rep (TickfPredicateFailure era) x
Generic)

deriving stock instance
  ( Era era,
    Show (PredicateFailure (Core.EraRule "NEWEPOCH" era))
  ) =>
  Show (TickfPredicateFailure era)

deriving stock instance
  ( Era era,
    Eq (PredicateFailure (Core.EraRule "NEWEPOCH" era))
  ) =>
  Eq (TickfPredicateFailure era)

instance
  ( UsesTxOut era,
    UsesValue era,
    NoThunks (PredicateFailure (Core.EraRule "NEWEPOCH" era))
  ) =>
  NoThunks (TickfPredicateFailure era)

newtype TickfEvent era
  = TickfNewEpochEvent (Event (Core.EraRule "NEWEPOCH" era)) -- Subtransition Events

instance
  ( Era era,
    Embed (Core.EraRule "NEWEPOCH" era) (TICKF era),
    Environment (Core.EraRule "NEWEPOCH" era) ~ (),
    State (Core.EraRule "NEWEPOCH" era) ~ NewEpochState era,
    Signal (Core.EraRule "NEWEPOCH" era) ~ EpochNo
  ) =>
  STS (TICKF era)
  where
  type
    State (TICKF era) =
      NewEpochState era
  type
    Signal (TICKF era) =
      SlotNo
  type Environment (TICKF era) = ()
  type BaseM (TICKF era) = ShelleyBase
  type PredicateFailure (TICKF era) = TickfPredicateFailure era
  type Event (TICKF era) = TickfEvent era

  initialRules :: [InitialRule (TICKF era)]
initialRules = []
  transitionRules :: [TransitionRule (TICKF era)]
transitionRules =
    [ do
        TRC ((), State (TICKF era)
nes, Signal (TICKF era)
slot) <- F (Clause (TICKF era) 'Transition) (TRC (TICKF era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        NewEpochState era -> SlotNo -> TransitionRule (TICKF era)
forall (tick :: * -> *) 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 State (TICKF era)
NewEpochState era
nes SlotNo
Signal (TICKF era)
slot
    ]

instance
  ( UsesTxOut era,
    UsesValue era,
    STS (NEWEPOCH era),
    PredicateFailure (Core.EraRule "NEWEPOCH" era) ~ NewEpochPredicateFailure era,
    Event (Core.EraRule "NEWEPOCH" era) ~ NewEpochEvent era
  ) =>
  Embed (NEWEPOCH era) (TICKF era)
  where
  wrapFailed :: PredicateFailure (NEWEPOCH era) -> PredicateFailure (TICKF era)
wrapFailed = PredicateFailure (NEWEPOCH era) -> PredicateFailure (TICKF era)
forall era.
PredicateFailure (EraRule "NEWEPOCH" era)
-> TickfPredicateFailure era
TickfNewEpochFailure
  wrapEvent :: Event (NEWEPOCH era) -> Event (TICKF era)
wrapEvent = Event (NEWEPOCH era) -> Event (TICKF era)
forall era. Event (EraRule "NEWEPOCH" era) -> TickfEvent era
TickfNewEpochEvent