{-# LANGUAGE DataKinds #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} module Ouroboros.Consensus.HardFork.Combinator.State.Infra ( -- * Initialization initHardForkState -- * Lifting 'Telescope' operations , fromTZ , match , sequence , tip -- * Situated , Situated (..) , situate -- * Aligning , align -- * EpochInfo/Summary , reconstructSummary ) where import Prelude hiding (sequence) import Data.Functor.Product import Data.SOP.Strict hiding (shape) import Ouroboros.Consensus.Block import Ouroboros.Consensus.HardFork.History (Bound (..), EraEnd (..), EraParams (..), EraSummary (..), SafeZone (..)) import qualified Ouroboros.Consensus.HardFork.History as History import Ouroboros.Consensus.Util.Counting import Ouroboros.Consensus.HardFork.Combinator.Abstract.SingleEraBlock import Ouroboros.Consensus.HardFork.Combinator.State.Lift import Ouroboros.Consensus.HardFork.Combinator.State.Types import Ouroboros.Consensus.HardFork.Combinator.Util.InPairs (InPairs, Requiring (..)) import qualified Ouroboros.Consensus.HardFork.Combinator.Util.InPairs as InPairs import Ouroboros.Consensus.HardFork.Combinator.Util.Match (Mismatch) import qualified Ouroboros.Consensus.HardFork.Combinator.Util.Match as Match import Ouroboros.Consensus.HardFork.Combinator.Util.Telescope (Extend (..), Telescope (..)) import qualified Ouroboros.Consensus.HardFork.Combinator.Util.Telescope as Telescope {------------------------------------------------------------------------------- Initialization -------------------------------------------------------------------------------} initHardForkState :: f x -> HardForkState f (x ': xs) initHardForkState :: f x -> HardForkState f (x : xs) initHardForkState f x st = Telescope (K Past) (Current f) (x : xs) -> HardForkState f (x : xs) forall (f :: * -> *) (xs :: [*]). Telescope (K Past) (Current f) xs -> HardForkState f xs HardForkState (Telescope (K Past) (Current f) (x : xs) -> HardForkState f (x : xs)) -> Telescope (K Past) (Current f) (x : xs) -> HardForkState f (x : xs) forall a b. (a -> b) -> a -> b $ Current f x -> Telescope (K Past) (Current f) (x : xs) forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]). f x -> Telescope g f (x : xs) TZ (Current f x -> Telescope (K Past) (Current f) (x : xs)) -> Current f x -> Telescope (K Past) (Current f) (x : xs) forall a b. (a -> b) -> a -> b $ Current :: forall (f :: * -> *) blk. Bound -> f blk -> Current f blk Current { currentStart :: Bound currentStart = Bound History.initBound , currentState :: f x currentState = f x st } {------------------------------------------------------------------------------- Lift telescope operations -------------------------------------------------------------------------------} tip :: SListI xs => HardForkState f xs -> NS f xs tip :: HardForkState f xs -> NS f xs tip (HardForkState Telescope (K Past) (Current f) xs st) = (forall a. Current f a -> f a) -> NS (Current f) xs -> NS f xs forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *) (f' :: k -> *). (SListIN (Prod h) xs, HAp h) => (forall (a :: k). f a -> f' a) -> h f xs -> h f' xs hmap forall a. Current f a -> f a forall (f :: * -> *) blk. Current f blk -> f blk currentState (NS (Current f) xs -> NS f xs) -> NS (Current f) xs -> NS f xs forall a b. (a -> b) -> a -> b $ Telescope (K Past) (Current f) xs -> NS (Current f) xs forall k (g :: k -> *) (f :: k -> *) (xs :: [k]). Telescope g f xs -> NS f xs Telescope.tip Telescope (K Past) (Current f) xs st match :: SListI xs => NS h xs -> HardForkState f xs -> Either (Mismatch h (Current f) xs) (HardForkState (Product h f) xs) match :: NS h xs -> HardForkState f xs -> Either (Mismatch h (Current f) xs) (HardForkState (Product h f) xs) match NS h xs ns (HardForkState Telescope (K Past) (Current f) xs t) = Telescope (K Past) (Current (Product h f)) xs -> HardForkState (Product h f) xs forall (f :: * -> *) (xs :: [*]). Telescope (K Past) (Current f) xs -> HardForkState f xs HardForkState (Telescope (K Past) (Current (Product h f)) xs -> HardForkState (Product h f) xs) -> (Telescope (K Past) (Product h (Current f)) xs -> Telescope (K Past) (Current (Product h f)) xs) -> Telescope (K Past) (Product h (Current f)) xs -> HardForkState (Product h f) xs forall b c a. (b -> c) -> (a -> b) -> a -> c . (forall a. Product h (Current f) a -> Current (Product h f) a) -> Telescope (K Past) (Product h (Current f)) xs -> Telescope (K Past) (Current (Product h f)) xs forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *) (f' :: k -> *). (SListIN (Prod h) xs, HAp h) => (forall (a :: k). f a -> f' a) -> h f xs -> h f' xs hmap forall a. Product h (Current f) a -> Current (Product h f) a forall (h :: * -> *) (f :: * -> *) blk. Product h (Current f) blk -> Current (Product h f) blk distrib (Telescope (K Past) (Product h (Current f)) xs -> HardForkState (Product h f) xs) -> Either (Mismatch h (Current f) xs) (Telescope (K Past) (Product h (Current f)) xs) -> Either (Mismatch h (Current f) xs) (HardForkState (Product h f) xs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> NS h xs -> Telescope (K Past) (Current f) xs -> Either (Mismatch h (Current f) xs) (Telescope (K Past) (Product h (Current f)) xs) forall k (h :: k -> *) (xs :: [k]) (g :: k -> *) (f :: k -> *). NS h xs -> Telescope g f xs -> Either (Mismatch h f xs) (Telescope g (Product h f) xs) Match.matchTelescope NS h xs ns Telescope (K Past) (Current f) xs t where distrib :: Product h (Current f) blk -> Current (Product h f) blk distrib :: Product h (Current f) blk -> Current (Product h f) blk distrib (Pair h blk x (Current Bound start f blk y)) = Bound -> Product h f blk -> Current (Product h f) blk forall (f :: * -> *) blk. Bound -> f blk -> Current f blk Current Bound start (h blk -> f blk -> Product h f blk forall k (f :: k -> *) (g :: k -> *) (a :: k). f a -> g a -> Product f g a Pair h blk x f blk y) sequence :: forall f m xs. (SListI xs, Functor m) => HardForkState (m :.: f) xs -> m (HardForkState f xs) sequence :: HardForkState (m :.: f) xs -> m (HardForkState f xs) sequence = \(HardForkState Telescope (K Past) (Current (m :.: f)) xs st) -> Telescope (K Past) (Current f) xs -> HardForkState f xs forall (f :: * -> *) (xs :: [*]). Telescope (K Past) (Current f) xs -> HardForkState f xs HardForkState (Telescope (K Past) (Current f) xs -> HardForkState f xs) -> m (Telescope (K Past) (Current f) xs) -> m (HardForkState f xs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Telescope (K Past) (m :.: Current f) xs -> m (Telescope (K Past) (Current f) xs) forall k (m :: * -> *) (g :: k -> *) (f :: k -> *) (xs :: [k]). Functor m => Telescope g (m :.: f) xs -> m (Telescope g f xs) Telescope.sequence ((forall a. Current (m :.: f) a -> (:.:) m (Current f) a) -> Telescope (K Past) (Current (m :.: f)) xs -> Telescope (K Past) (m :.: Current f) xs forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *) (f' :: k -> *). (SListIN (Prod h) xs, HAp h) => (forall (a :: k). f a -> f' a) -> h f xs -> h f' xs hmap forall a. Current (m :.: f) a -> (:.:) m (Current f) a distrib Telescope (K Past) (Current (m :.: f)) xs st) where distrib :: Current (m :.: f) blk -> (m :.: Current f) blk distrib :: Current (m :.: f) blk -> (:.:) m (Current f) blk distrib (Current Bound start (:.:) m f blk st) = m (Current f blk) -> (:.:) m (Current f) blk forall l k (f :: l -> *) (g :: k -> l) (p :: k). f (g p) -> (:.:) f g p Comp (m (Current f blk) -> (:.:) m (Current f) blk) -> m (Current f blk) -> (:.:) m (Current f) blk forall a b. (a -> b) -> a -> b $ Bound -> f blk -> Current f blk forall (f :: * -> *) blk. Bound -> f blk -> Current f blk Current Bound start (f blk -> Current f blk) -> m (f blk) -> m (Current f blk) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> (:.:) m f blk -> m (f blk) forall l k (f :: l -> *) (g :: k -> l) (p :: k). (:.:) f g p -> f (g p) unComp (:.:) m f blk st fromTZ :: HardForkState f '[blk] -> f blk fromTZ :: HardForkState f '[blk] -> f blk fromTZ = Current f blk -> f blk forall (f :: * -> *) blk. Current f blk -> f blk currentState (Current f blk -> f blk) -> (HardForkState f '[blk] -> Current f blk) -> HardForkState f '[blk] -> f blk forall b c a. (b -> c) -> (a -> b) -> a -> c . Telescope (K Past) (Current f) '[blk] -> Current f blk forall k (g :: k -> *) (f :: k -> *) (x :: k). Telescope g f '[x] -> f x Telescope.fromTZ (Telescope (K Past) (Current f) '[blk] -> Current f blk) -> (HardForkState f '[blk] -> Telescope (K Past) (Current f) '[blk]) -> HardForkState f '[blk] -> Current f blk forall b c a. (b -> c) -> (a -> b) -> a -> c . HardForkState f '[blk] -> Telescope (K Past) (Current f) '[blk] forall (f :: * -> *) (xs :: [*]). HardForkState f xs -> Telescope (K Past) (Current f) xs getHardForkState {------------------------------------------------------------------------------- Situated -------------------------------------------------------------------------------} -- | A @h@ situated in time data Situated h f xs where SituatedCurrent :: Current f x -> h x -> Situated h f (x ': xs) SituatedNext :: Current f x -> h y -> Situated h f (x ': y ': xs) SituatedFuture :: Current f x -> NS h xs -> Situated h f (x ': y ': xs) SituatedPast :: K Past x -> h x -> Situated h f (x ': xs) SituatedShift :: Situated h f xs -> Situated h f (x ': xs) situate :: NS h xs -> HardForkState f xs -> Situated h f xs situate :: NS h xs -> HardForkState f xs -> Situated h f xs situate NS h xs ns = NS h xs -> Telescope (K Past) (Current f) xs -> Situated h f xs forall (h :: * -> *) (xs' :: [*]) (f :: * -> *). NS h xs' -> Telescope (K Past) (Current f) xs' -> Situated h f xs' go NS h xs ns (Telescope (K Past) (Current f) xs -> Situated h f xs) -> (HardForkState f xs -> Telescope (K Past) (Current f) xs) -> HardForkState f xs -> Situated h f xs forall b c a. (b -> c) -> (a -> b) -> a -> c . HardForkState f xs -> Telescope (K Past) (Current f) xs forall (f :: * -> *) (xs :: [*]). HardForkState f xs -> Telescope (K Past) (Current f) xs getHardForkState where go :: NS h xs' -> Telescope (K Past) (Current f) xs' -> Situated h f xs' go :: NS h xs' -> Telescope (K Past) (Current f) xs' -> Situated h f xs' go (Z h x era) (TZ Current f x cur) = Current f x -> h x -> Situated h f (x : xs) forall (f :: * -> *) x (h :: * -> *) (xs :: [*]). Current f x -> h x -> Situated h f (x : xs) SituatedCurrent Current f x cur h x h x era go (S (Z h x era)) (TZ Current f x cur) = Current f x -> h x -> Situated h f (x : x : xs) forall (f :: * -> *) x (h :: * -> *) y (x :: [*]). Current f x -> h y -> Situated h f (x : y : x) SituatedNext Current f x cur h x era go (S (S NS h xs era)) (TZ Current f x cur) = Current f x -> NS h xs -> Situated h f (x : x : xs) forall (f :: * -> *) x (h :: * -> *) (xs :: [*]) y. Current f x -> NS h xs -> Situated h f (x : y : xs) SituatedFuture Current f x cur NS h xs era go (Z h x era) (TS K Past x past Telescope (K Past) (Current f) xs _) = K Past x -> h x -> Situated h f (x : xs) forall x (h :: * -> *) (f :: * -> *) (xs :: [*]). K Past x -> h x -> Situated h f (x : xs) SituatedPast K Past x past h x h x era go (S NS h xs era) (TS K Past x _ Telescope (K Past) (Current f) xs st) = Situated h f xs -> Situated h f (x : xs) forall (h :: * -> *) (f :: * -> *) (xs :: [*]) x. Situated h f xs -> Situated h f (x : xs) SituatedShift (Situated h f xs -> Situated h f (x : xs)) -> Situated h f xs -> Situated h f (x : xs) forall a b. (a -> b) -> a -> b $ NS h xs -> Telescope (K Past) (Current f) xs -> Situated h f xs forall (h :: * -> *) (xs' :: [*]) (f :: * -> *). NS h xs' -> Telescope (K Past) (Current f) xs' -> Situated h f xs' go NS h xs era Telescope (K Past) (Current f) xs Telescope (K Past) (Current f) xs st {------------------------------------------------------------------------------- Aligning -------------------------------------------------------------------------------} align :: forall xs f f' f''. All SingleEraBlock xs => InPairs (Translate f) xs -> NP (f' -.-> f -.-> f'') xs -> HardForkState f' xs -- ^ State we are aligning with -> HardForkState f xs -- ^ State we are aligning -> HardForkState f'' xs align :: InPairs (Translate f) xs -> NP (f' -.-> (f -.-> f'')) xs -> HardForkState f' xs -> HardForkState f xs -> HardForkState f'' xs align InPairs (Translate f) xs fs NP (f' -.-> (f -.-> f'')) xs updTip (HardForkState Telescope (K Past) (Current f') xs alignWith) (HardForkState Telescope (K Past) (Current f) xs toAlign) = Telescope (K Past) (Current f'') xs -> HardForkState f'' xs forall (f :: * -> *) (xs :: [*]). Telescope (K Past) (Current f) xs -> HardForkState f xs HardForkState (Telescope (K Past) (Current f'') xs -> HardForkState f'' xs) -> (I (Telescope (K Past) (Current f'') xs) -> Telescope (K Past) (Current f'') xs) -> I (Telescope (K Past) (Current f'') xs) -> HardForkState f'' xs forall b c a. (b -> c) -> (a -> b) -> a -> c . I (Telescope (K Past) (Current f'') xs) -> Telescope (K Past) (Current f'') xs forall a. I a -> a unI (I (Telescope (K Past) (Current f'') xs) -> HardForkState f'' xs) -> I (Telescope (K Past) (Current f'') xs) -> HardForkState f'' xs forall a b. (a -> b) -> a -> b $ InPairs (Requiring (K Past) (Extend I (K Past) (Current f))) xs -> NP (Current f' -.-> (Current f -.-> Current f'')) xs -> Telescope (K Past) (Current f') xs -> Telescope (K Past) (Current f) xs -> I (Telescope (K Past) (Current f'') xs) forall k (m :: * -> *) (g' :: k -> *) (g :: k -> *) (f :: k -> *) (xs :: [k]) (f' :: k -> *) (f'' :: k -> *). (Monad m, HasCallStack) => InPairs (Requiring g' (Extend m g f)) xs -> NP (f' -.-> (f -.-> f'')) xs -> Telescope g' f' xs -> Telescope g f xs -> m (Telescope g f'' xs) Telescope.alignExtend ((forall x y. Translate f x y -> Requiring (K Past) (Extend I (K Past) (Current f)) x y) -> InPairs (Translate f) xs -> InPairs (Requiring (K Past) (Extend I (K Past) (Current f))) xs forall k (xs :: [k]) (f :: k -> k -> *) (g :: k -> k -> *). SListI xs => (forall (x :: k) (y :: k). f x y -> g x y) -> InPairs f xs -> InPairs g xs InPairs.hmap (\Translate f x y f -> (K Past x -> Extend I (K Past) (Current f) x y) -> Requiring (K Past) (Extend I (K Past) (Current f)) x y forall k k (h :: k -> *) (f :: k -> k -> *) (x :: k) (y :: k). (h x -> f x y) -> Requiring h f x y Require ((K Past x -> Extend I (K Past) (Current f) x y) -> Requiring (K Past) (Extend I (K Past) (Current f)) x y) -> (K Past x -> Extend I (K Past) (Current f) x y) -> Requiring (K Past) (Extend I (K Past) (Current f)) x y forall a b. (a -> b) -> a -> b $ \K Past x past -> (Current f x -> I (K Past x, Current f y)) -> Extend I (K Past) (Current f) x y forall k (m :: * -> *) (g :: k -> *) (f :: k -> *) (x :: k) (y :: k). (f x -> m (g x, f y)) -> Extend m g f x y Extend ((Current f x -> I (K Past x, Current f y)) -> Extend I (K Past) (Current f) x y) -> (Current f x -> I (K Past x, Current f y)) -> Extend I (K Past) (Current f) x y forall a b. (a -> b) -> a -> b $ \Current f x cur -> (K Past x, Current f y) -> I (K Past x, Current f y) forall a. a -> I a I ((K Past x, Current f y) -> I (K Past x, Current f y)) -> (K Past x, Current f y) -> I (K Past x, Current f y) forall a b. (a -> b) -> a -> b $ Translate f x y -> K Past x -> Current f x -> (K Past x, Current f y) forall blk blk'. Translate f blk blk' -> K Past blk -> Current f blk -> (K Past blk, Current f blk') newCurrent Translate f x y f K Past x past Current f x cur) InPairs (Translate f) xs fs) ((forall a. (-.->) f' (f -.-> f'') a -> (-.->) (Current f') (Current f -.-> Current f'') a) -> NP (f' -.-> (f -.-> f'')) xs -> NP (Current f' -.-> (Current f -.-> Current f'')) xs forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *) (f' :: k -> *). (SListIN (Prod h) xs, HAp h) => (forall (a :: k). f a -> f' a) -> h f xs -> h f' xs hmap ((Current f' a -> Current f a -> Current f'' a) -> (-.->) (Current f') (Current f -.-> Current f'') a forall k (f :: k -> *) (a :: k) (f' :: k -> *) (f'' :: k -> *). (f a -> f' a -> f'' a) -> (-.->) f (f' -.-> f'') a fn_2 ((Current f' a -> Current f a -> Current f'' a) -> (-.->) (Current f') (Current f -.-> Current f'') a) -> ((-.->) f' (f -.-> f'') a -> Current f' a -> Current f a -> Current f'' a) -> (-.->) f' (f -.-> f'') a -> (-.->) (Current f') (Current f -.-> Current f'') a forall b c a. (b -> c) -> (a -> b) -> a -> c . (-.->) f' (f -.-> f'') a -> Current f' a -> Current f a -> Current f'' a forall blk. (-.->) f' (f -.-> f'') blk -> Current f' blk -> Current f blk -> Current f'' blk liftUpdTip) NP (f' -.-> (f -.-> f'')) xs updTip) Telescope (K Past) (Current f') xs alignWith Telescope (K Past) (Current f) xs toAlign where liftUpdTip :: (f' -.-> f -.-> f'') blk -> Current f' blk -> Current f blk -> Current f'' blk liftUpdTip :: (-.->) f' (f -.-> f'') blk -> Current f' blk -> Current f blk -> Current f'' blk liftUpdTip (-.->) f' (f -.-> f'') blk f = (f blk -> f'' blk) -> Current f blk -> Current f'' blk forall (f :: * -> *) blk (f' :: * -> *). (f blk -> f' blk) -> Current f blk -> Current f' blk lift ((f blk -> f'' blk) -> Current f blk -> Current f'' blk) -> (Current f' blk -> f blk -> f'' blk) -> Current f' blk -> Current f blk -> Current f'' blk forall b c a. (b -> c) -> (a -> b) -> a -> c . (-.->) f f'' blk -> f blk -> f'' blk forall k (f :: k -> *) (g :: k -> *) (a :: k). (-.->) f g a -> f a -> g a apFn ((-.->) f f'' blk -> f blk -> f'' blk) -> (Current f' blk -> (-.->) f f'' blk) -> Current f' blk -> f blk -> f'' blk forall b c a. (b -> c) -> (a -> b) -> a -> c . (-.->) f' (f -.-> f'') blk -> f' blk -> (-.->) f f'' blk forall k (f :: k -> *) (g :: k -> *) (a :: k). (-.->) f g a -> f a -> g a apFn (-.->) f' (f -.-> f'') blk f (f' blk -> (-.->) f f'' blk) -> (Current f' blk -> f' blk) -> Current f' blk -> (-.->) f f'' blk forall b c a. (b -> c) -> (a -> b) -> a -> c . Current f' blk -> f' blk forall (f :: * -> *) blk. Current f blk -> f blk currentState newCurrent :: Translate f blk blk' -> K Past blk -> Current f blk -> (K Past blk, Current f blk') newCurrent :: Translate f blk blk' -> K Past blk -> Current f blk -> (K Past blk, Current f blk') newCurrent Translate f blk blk' f (K Past past) Current f blk curF = ( Past -> K Past blk forall k a (b :: k). a -> K a b K Past :: Bound -> Bound -> Past Past { pastStart :: Bound pastStart = Current f blk -> Bound forall (f :: * -> *) blk. Current f blk -> Bound currentStart Current f blk curF , pastEnd :: Bound pastEnd = Bound curEnd } , Current :: forall (f :: * -> *) blk. Bound -> f blk -> Current f blk Current { currentStart :: Bound currentStart = Bound curEnd , currentState :: f blk' currentState = Translate f blk blk' -> EpochNo -> f blk -> f blk' forall (f :: * -> *) x y. Translate f x y -> EpochNo -> f x -> f y translateWith Translate f blk blk' f (Bound -> EpochNo boundEpoch Bound curEnd) (Current f blk -> f blk forall (f :: * -> *) blk. Current f blk -> f blk currentState Current f blk curF) } ) where curEnd :: Bound curEnd :: Bound curEnd = Past -> Bound pastEnd Past past {------------------------------------------------------------------------------- Summary/EpochInfo -------------------------------------------------------------------------------} reconstructSummary :: History.Shape xs -> TransitionInfo -- ^ At the tip -> HardForkState f xs -> History.Summary xs reconstructSummary :: Shape xs -> TransitionInfo -> HardForkState f xs -> Summary xs reconstructSummary (History.Shape Exactly xs EraParams shape) TransitionInfo transition (HardForkState Telescope (K Past) (Current f) xs st) = NonEmpty xs EraSummary -> Summary xs forall (xs :: [*]). NonEmpty xs EraSummary -> Summary xs History.Summary (NonEmpty xs EraSummary -> Summary xs) -> NonEmpty xs EraSummary -> Summary xs forall a b. (a -> b) -> a -> b $ Exactly xs EraParams -> Telescope (K Past) (Current f) xs -> NonEmpty xs EraSummary forall (xs' :: [*]) (f :: * -> *). Exactly xs' EraParams -> Telescope (K Past) (Current f) xs' -> NonEmpty xs' EraSummary go Exactly xs EraParams shape Telescope (K Past) (Current f) xs st where go :: Exactly xs' EraParams -> Telescope (K Past) (Current f) xs' -> NonEmpty xs' EraSummary go :: Exactly xs' EraParams -> Telescope (K Past) (Current f) xs' -> NonEmpty xs' EraSummary go Exactly xs' EraParams ExactlyNil Telescope (K Past) (Current f) xs' t = case Telescope (K Past) (Current f) xs' t of {} go (ExactlyCons EraParams params Exactly xs EraParams ss) (TS (K Past{Bound pastEnd :: Bound pastStart :: Bound pastEnd :: Past -> Bound pastStart :: Past -> Bound ..}) Telescope (K Past) (Current f) xs t) = EraSummary -> NonEmpty xs EraSummary -> NonEmpty (x : xs) EraSummary forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a NonEmptyCons (Bound -> EraEnd -> EraParams -> EraSummary EraSummary Bound pastStart (Bound -> EraEnd EraEnd Bound pastEnd) EraParams params) (NonEmpty xs EraSummary -> NonEmpty (x : xs) EraSummary) -> NonEmpty xs EraSummary -> NonEmpty (x : xs) EraSummary forall a b. (a -> b) -> a -> b $ Exactly xs EraParams -> Telescope (K Past) (Current f) xs -> NonEmpty xs EraSummary forall (xs' :: [*]) (f :: * -> *). Exactly xs' EraParams -> Telescope (K Past) (Current f) xs' -> NonEmpty xs' EraSummary go Exactly xs EraParams ss Telescope (K Past) (Current f) xs Telescope (K Past) (Current f) xs t go (ExactlyCons EraParams params Exactly xs EraParams ss) (TZ Current{f x Bound currentState :: f x currentStart :: Bound currentState :: forall (f :: * -> *) blk. Current f blk -> f blk currentStart :: forall (f :: * -> *) blk. Current f blk -> Bound ..}) = case TransitionInfo transition of TransitionKnown EpochNo epoch -> -- We haven't reached the next era yet, but the transition is -- already known. The safe zone applies from the start of the -- next era. let currentEnd :: Bound currentEnd = HasCallStack => EraParams -> Bound -> EpochNo -> Bound EraParams -> Bound -> EpochNo -> Bound History.mkUpperBound EraParams params Bound currentStart EpochNo epoch nextStart :: Bound nextStart = Bound currentEnd in case Exactly xs EraParams ss of ExactlyCons EraParams nextParams Exactly xs EraParams _ -> EraSummary -> NonEmpty (x : xs) EraSummary -> NonEmpty (x : x : xs) EraSummary forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a NonEmptyCons EraSummary :: Bound -> EraEnd -> EraParams -> EraSummary EraSummary { eraStart :: Bound eraStart = Bound currentStart , eraParams :: EraParams eraParams = EraParams params , eraEnd :: EraEnd eraEnd = Bound -> EraEnd EraEnd Bound currentEnd } (NonEmpty (x : xs) EraSummary -> NonEmpty (x : x : xs) EraSummary) -> NonEmpty (x : xs) EraSummary -> NonEmpty (x : x : xs) EraSummary forall a b. (a -> b) -> a -> b $ EraSummary -> NonEmpty (x : xs) EraSummary forall a x (xs :: [*]). a -> NonEmpty (x : xs) a NonEmptyOne EraSummary :: Bound -> EraEnd -> EraParams -> EraSummary EraSummary { eraStart :: Bound eraStart = Bound nextStart , eraParams :: EraParams eraParams = EraParams nextParams , eraEnd :: EraEnd eraEnd = EraParams -> Bound -> SlotNo -> EraEnd applySafeZone EraParams nextParams Bound nextStart (Bound -> SlotNo boundSlot Bound nextStart) } Exactly xs EraParams ExactlyNil -> -- HOWEVER, this code doesn't know what that next era is! This -- can arise when a node has not updated its code despite an -- imminent hard fork. -- -- In the specific case of 'ShelleyBlock' and 'CardanoBlock', a -- lot would have to go wrong in the PR review process for -- 'TransitionKnown' to arise during the last known era in the -- code. The 'ShelleyBlock' 'singleEraTransition' method leads -- to 'TransitionKnown' here only based on the -- 'shelleyTriggerHardFork' field of its ledger config, which is -- statically set by a quite obvious pattern in -- 'protocolInfoCardano', which is passed concrete arguments by -- a similarly obvious pattern in -- 'mkSomeConsensusProtocolCardano' defined in the -- @cardano-node@ repo. EraSummary -> NonEmpty '[x] EraSummary forall a x (xs :: [*]). a -> NonEmpty (x : xs) a NonEmptyOne EraSummary :: Bound -> EraEnd -> EraParams -> EraSummary EraSummary { eraStart :: Bound eraStart = Bound currentStart , eraParams :: EraParams eraParams = EraParams params , eraEnd :: EraEnd eraEnd = Bound -> EraEnd EraEnd Bound currentEnd } TransitionUnknown WithOrigin SlotNo ledgerTip -> EraSummary -> NonEmpty (x : xs) EraSummary forall a x (xs :: [*]). a -> NonEmpty (x : xs) a NonEmptyOne (EraSummary -> NonEmpty (x : xs) EraSummary) -> EraSummary -> NonEmpty (x : xs) EraSummary forall a b. (a -> b) -> a -> b $ EraSummary :: Bound -> EraEnd -> EraParams -> EraSummary EraSummary { eraStart :: Bound eraStart = Bound currentStart , eraParams :: EraParams eraParams = EraParams params , eraEnd :: EraEnd eraEnd = EraParams -> Bound -> SlotNo -> EraEnd applySafeZone EraParams params Bound currentStart -- Even if the safe zone is 0, the first slot at -- which the next era could begin is the /next/ (WithOrigin SlotNo -> SlotNo next WithOrigin SlotNo ledgerTip) } -- 'TransitionImpossible' is used in one of two cases: we are in the -- final era this chain will ever have (handled by the corresponding -- 'UnsafeIndefiniteSafeZone' case within 'applySafeZone' below) or -- this era is a future era that hasn't begun yet, in which case the -- safe zone must start at the beginning of this era. TransitionInfo TransitionImpossible -> EraSummary -> NonEmpty (x : xs) EraSummary forall a x (xs :: [*]). a -> NonEmpty (x : xs) a NonEmptyOne (EraSummary -> NonEmpty (x : xs) EraSummary) -> EraSummary -> NonEmpty (x : xs) EraSummary forall a b. (a -> b) -> a -> b $ EraSummary :: Bound -> EraEnd -> EraParams -> EraSummary EraSummary { eraStart :: Bound eraStart = Bound currentStart , eraParams :: EraParams eraParams = EraParams params , eraEnd :: EraEnd eraEnd = EraParams -> Bound -> SlotNo -> EraEnd applySafeZone EraParams params Bound currentStart (Bound -> SlotNo boundSlot Bound currentStart) } -- Apply safe zone from the specified 'SlotNo' -- -- All arguments must be referring to or in the same era. applySafeZone :: EraParams -> Bound -> SlotNo -> EraEnd applySafeZone :: EraParams -> Bound -> SlotNo -> EraEnd applySafeZone params :: EraParams params@EraParams{SlotLength EpochSize SafeZone eraSafeZone :: EraParams -> SafeZone eraSlotLength :: EraParams -> SlotLength eraEpochSize :: EraParams -> EpochSize eraSafeZone :: SafeZone eraSlotLength :: SlotLength eraEpochSize :: EpochSize ..} Bound start = case SafeZone eraSafeZone of SafeZone UnsafeIndefiniteSafeZone -> EraEnd -> SlotNo -> EraEnd forall a b. a -> b -> a const EraEnd EraUnbounded StandardSafeZone Word64 safeFromTip -> Bound -> EraEnd EraEnd (Bound -> EraEnd) -> (SlotNo -> Bound) -> SlotNo -> EraEnd forall b c a. (b -> c) -> (a -> b) -> a -> c . HasCallStack => EraParams -> Bound -> EpochNo -> Bound EraParams -> Bound -> EpochNo -> Bound History.mkUpperBound EraParams params Bound start (EpochNo -> Bound) -> (SlotNo -> EpochNo) -> SlotNo -> Bound forall b c a. (b -> c) -> (a -> b) -> a -> c . EraParams -> Bound -> SlotNo -> EpochNo History.slotToEpochBound EraParams params Bound start (SlotNo -> EpochNo) -> (SlotNo -> SlotNo) -> SlotNo -> EpochNo forall b c a. (b -> c) -> (a -> b) -> a -> c . Word64 -> SlotNo -> SlotNo History.addSlots Word64 safeFromTip next :: WithOrigin SlotNo -> SlotNo next :: WithOrigin SlotNo -> SlotNo next WithOrigin SlotNo Origin = Word64 -> SlotNo SlotNo Word64 0 next (NotOrigin SlotNo s) = SlotNo -> SlotNo forall a. Enum a => a -> a succ SlotNo s