{-# LANGUAGE DataKinds #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# 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 Data.Functor.Product import Data.SOP.BasicFunctors import Data.SOP.Constraint import Data.SOP.Counting import Data.SOP.InPairs (InPairs, Requiring (..)) import qualified Data.SOP.InPairs as InPairs import Data.SOP.Match (Mismatch) import qualified Data.SOP.Match as Match import Data.SOP.NonEmpty import Data.SOP.Strict import Data.SOP.Telescope (Extend (..), Telescope (..)) import qualified Data.SOP.Telescope as Telescope import Ouroboros.Consensus.Block 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.History (Bound (..), EraEnd (..), EraParams (..), EraSummary (..), SafeZone (..)) import qualified Ouroboros.Consensus.HardFork.History as History import Prelude hiding (sequence) {------------------------------------------------------------------------------- Initialization -------------------------------------------------------------------------------} initHardForkState :: f x -> HardForkState f (x ': xs) initHardForkState :: forall (f :: * -> *) x (xs :: [*]). 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 {k} (f :: k -> *) (x :: k) (g :: k -> *) (xs1 :: [k]). f x -> Telescope g f (x : xs1) 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 { 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 :: forall (xs :: [*]) (f :: * -> *). SListI xs => 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 Current f a -> f a 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 :: forall (xs :: [*]) (h :: * -> *) (f :: * -> *). SListI xs => 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 Product h (Current f) a -> Current (Product h f) a 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 :: forall (h :: * -> *) (f :: * -> *) blk. 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 :: forall (f :: * -> *) (m :: * -> *) (xs :: [*]). (SListI xs, Functor m) => 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 Current (m :.: f) a -> (:.:) m (Current f) a 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 :: forall a. Current (m :.: f) a -> (:.:) m (Current f) a 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 :: forall (f :: * -> *) blk. 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 :: forall (h :: * -> *) (xs :: [*]) (f :: * -> *). 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 :: forall (h :: * -> *) (xs' :: [*]) (f :: * -> *). 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 : xs1) forall (f :: * -> *) xs (h :: * -> *) (x :: [*]). Current f xs -> h xs -> Situated h f (xs : x) 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 : xs1) forall (f :: * -> *) xs (h :: * -> *) x (y :: [*]). Current f xs -> h x -> Situated h f (xs : x : y) SituatedNext Current f x cur h x era go (S (S NS h xs1 era)) (TZ Current f x cur) = Current f x -> NS h xs1 -> Situated h f (x : x : xs1) forall (f :: * -> *) xs (h :: * -> *) (x :: [*]) y. Current f xs -> NS h x -> Situated h f (xs : y : x) SituatedFuture Current f x cur NS h xs1 era go (Z h x era) (TS K Past x past Telescope (K Past) (Current f) xs1 _) = K Past x -> h x -> Situated h f (x : xs1) forall xs (h :: * -> *) (f :: * -> *) (x :: [*]). K Past xs -> h xs -> Situated h f (xs : x) SituatedPast K Past x past h x h x era go (S NS h xs1 era) (TS K Past x _ Telescope (K Past) (Current f) xs1 st) = Situated h f xs1 -> Situated h f (x : xs1) forall (h :: * -> *) (f :: * -> *) (xs :: [*]) x. Situated h f xs -> Situated h f (x : xs) SituatedShift (Situated h f xs1 -> Situated h f (x : xs1)) -> Situated h f xs1 -> Situated h f (x : xs1) forall a b. (a -> b) -> a -> b $ NS h xs1 -> Telescope (K Past) (Current f) xs1 -> Situated h f xs1 forall (h :: * -> *) (xs' :: [*]) (f :: * -> *). NS h xs' -> Telescope (K Past) (Current f) xs' -> Situated h f xs' go NS h xs1 era Telescope (K Past) (Current f) xs1 Telescope (K Past) (Current f) xs1 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 :: forall (xs :: [*]) (f :: * -> *) (f' :: * -> *) (f'' :: * -> *). All SingleEraBlock xs => 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} {k1} (h :: k -> *) (f :: k -> k1 -> *) (x :: k) (y :: k1). (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 :: forall blk. (-.->) 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 :: forall blk blk'. 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 { 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 { 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 :: forall (xs :: [*]) (f :: * -> *). 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 :: forall (xs' :: [*]) (f :: * -> *). 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 pastStart :: Past -> Bound pastEnd :: Past -> Bound pastStart :: Bound pastEnd :: Bound ..}) Telescope (K Past) (Current f) xs1 t) = EraSummary -> NonEmpty xs EraSummary -> NonEmpty (x : xs) EraSummary forall a (xs1 :: [*]) x. a -> NonEmpty xs1 a -> NonEmpty (x : xs1) 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) xs1 t go (ExactlyCons EraParams params Exactly xs EraParams ss) (TZ Current{f x Bound currentStart :: forall (f :: * -> *) blk. Current f blk -> Bound currentState :: forall (f :: * -> *) blk. Current f blk -> f blk currentStart :: Bound currentState :: f x ..}) = 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 (xs1 :: [*]) x. a -> NonEmpty xs1 a -> NonEmpty (x : xs1) a NonEmptyCons 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 (xs1 :: [*]). a -> NonEmpty (x : xs1) a NonEmptyOne 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 (xs1 :: [*]). a -> NonEmpty (x : xs1) a NonEmptyOne 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 (xs1 :: [*]). a -> NonEmpty (x : xs1) a NonEmptyOne (EraSummary -> NonEmpty (x : xs) EraSummary) -> EraSummary -> NonEmpty (x : xs) EraSummary forall a b. (a -> b) -> a -> b $ 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 (xs1 :: [*]). a -> NonEmpty (x : xs1) a NonEmptyOne (EraSummary -> NonEmpty (x : xs) EraSummary) -> EraSummary -> NonEmpty (x : xs) EraSummary forall a b. (a -> b) -> a -> b $ 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{EpochSize SlotLength GenesisWindow SafeZone eraEpochSize :: EpochSize eraSlotLength :: SlotLength eraSafeZone :: SafeZone eraGenesisWin :: GenesisWindow eraEpochSize :: EraParams -> EpochSize eraSlotLength :: EraParams -> SlotLength eraSafeZone :: EraParams -> SafeZone eraGenesisWin :: EraParams -> GenesisWindow ..} 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