{-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-} module Ouroboros.Consensus.HardFork.Combinator.State.Types ( -- * Main types Current (..) , HardForkState (..) , Past (..) , sequenceHardForkState -- * Supporting types , CrossEraForecaster (..) , TransitionInfo (..) , Translate (..) ) where import Control.Monad.Except import Data.SOP.BasicFunctors import Data.SOP.Constraint import Data.SOP.Strict import Data.SOP.Telescope (Telescope) import qualified Data.SOP.Telescope as Telescope import GHC.Generics (Generic) import NoThunks.Class (NoThunks (..)) import Ouroboros.Consensus.Block import Ouroboros.Consensus.Forecast import Ouroboros.Consensus.HardFork.History (Bound) import Prelude {------------------------------------------------------------------------------- Types -------------------------------------------------------------------------------} -- | Generic hard fork state -- -- This is used both for the consensus state and the ledger state. -- -- By using a telescope with @f ~ LedgerState@, we will keep track of 'Past' -- information for eras before the current one: -- -- > TZ currentByronState -- > TZ pastByronState $ TZ currentShelleyState -- > TZ pastByronState $ TS pastShelleyState $ TZ currentAllegraState -- > ... -- -- These are some intuitions on how the Telescope operations behave for this -- type: -- -- = @extend@ -- -- Suppose we have a telescope containing the ledger state. The "how to extend" -- argument would take, say, the final Byron state to the initial Shelley state; -- and "where to extend from" argument would indicate when we want to extend: -- when the current slot number has gone past the end of the Byron era. -- -- = @retract@ -- -- Suppose we have a telescope containing the consensus state. When we rewind -- the consensus state, we might cross a hard fork transition point. So we first -- /retract/ the telescope /to/ the era containing the slot number that we want -- to rewind to, and only then call 'rewindChainDepState' on that era. Of course, -- retraction may fail (we might not /have/ past consensus state to rewind to -- anymore); this failure would require a choice for a particular monad @m@. -- -- = @align@ -- -- Suppose we have one telescope containing the already-ticked ledger state, and -- another telescope containing the consensus state. Since the ledger state has -- already been ticked, it might have been advanced to the next era. If this -- happens, we should then align the consensus state with the ledger state, -- moving /it/ also to the next era, before we can do the consensus header -- validation check. Note that in this particular example, the ledger state will -- always be ahead of the consensus state, never behind; 'alignExtend' can be -- used in this case. newtype HardForkState f xs = HardForkState { forall (f :: * -> *) (xs :: [*]). HardForkState f xs -> Telescope (K Past) (Current f) xs getHardForkState :: Telescope (K Past) (Current f) xs } -- | Information about the current era data Current f blk = Current { forall (f :: * -> *) blk. Current f blk -> Bound currentStart :: !Bound , forall (f :: * -> *) blk. Current f blk -> f blk currentState :: !(f blk) } deriving ((forall x. Current f blk -> Rep (Current f blk) x) -> (forall x. Rep (Current f blk) x -> Current f blk) -> Generic (Current f blk) forall x. Rep (Current f blk) x -> Current f blk forall x. Current f blk -> Rep (Current f blk) x forall a. (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a forall (f :: * -> *) blk x. Rep (Current f blk) x -> Current f blk forall (f :: * -> *) blk x. Current f blk -> Rep (Current f blk) x $cfrom :: forall (f :: * -> *) blk x. Current f blk -> Rep (Current f blk) x from :: forall x. Current f blk -> Rep (Current f blk) x $cto :: forall (f :: * -> *) blk x. Rep (Current f blk) x -> Current f blk to :: forall x. Rep (Current f blk) x -> Current f blk Generic) -- | Information about a past era data Past = Past { Past -> Bound pastStart :: !Bound , Past -> Bound pastEnd :: !Bound } deriving (Past -> Past -> Bool (Past -> Past -> Bool) -> (Past -> Past -> Bool) -> Eq Past forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a $c== :: Past -> Past -> Bool == :: Past -> Past -> Bool $c/= :: Past -> Past -> Bool /= :: Past -> Past -> Bool Eq, Int -> Past -> ShowS [Past] -> ShowS Past -> String (Int -> Past -> ShowS) -> (Past -> String) -> ([Past] -> ShowS) -> Show Past forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a $cshowsPrec :: Int -> Past -> ShowS showsPrec :: Int -> Past -> ShowS $cshow :: Past -> String show :: Past -> String $cshowList :: [Past] -> ShowS showList :: [Past] -> ShowS Show, (forall x. Past -> Rep Past x) -> (forall x. Rep Past x -> Past) -> Generic Past forall x. Rep Past x -> Past forall x. Past -> Rep Past x forall a. (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a $cfrom :: forall x. Past -> Rep Past x from :: forall x. Past -> Rep Past x $cto :: forall x. Rep Past x -> Past to :: forall x. Rep Past x -> Past Generic, Context -> Past -> IO (Maybe ThunkInfo) Proxy Past -> String (Context -> Past -> IO (Maybe ThunkInfo)) -> (Context -> Past -> IO (Maybe ThunkInfo)) -> (Proxy Past -> String) -> NoThunks Past forall a. (Context -> a -> IO (Maybe ThunkInfo)) -> (Context -> a -> IO (Maybe ThunkInfo)) -> (Proxy a -> String) -> NoThunks a $cnoThunks :: Context -> Past -> IO (Maybe ThunkInfo) noThunks :: Context -> Past -> IO (Maybe ThunkInfo) $cwNoThunks :: Context -> Past -> IO (Maybe ThunkInfo) wNoThunks :: Context -> Past -> IO (Maybe ThunkInfo) $cshowTypeOf :: Proxy Past -> String showTypeOf :: Proxy Past -> String NoThunks) -- | Thin wrapper around 'Telescope.sequence' sequenceHardForkState :: forall m f xs. (All Top xs, Functor m) => HardForkState (m :.: f) xs -> m (HardForkState f xs) sequenceHardForkState :: forall (m :: * -> *) (f :: * -> *) (xs :: [*]). (All Top xs, Functor m) => HardForkState (m :.: f) xs -> m (HardForkState f xs) sequenceHardForkState (HardForkState Telescope (K Past) (Current (m :.: f)) xs tel) = (Telescope (K Past) (Current f) xs -> HardForkState f xs) -> m (Telescope (K Past) (Current f) xs) -> m (HardForkState f xs) forall a b. (a -> b) -> m a -> m b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap Telescope (K Past) (Current f) xs -> HardForkState f xs forall (f :: * -> *) (xs :: [*]). Telescope (K Past) (Current f) xs -> HardForkState f xs HardForkState (m (Telescope (K Past) (Current f) xs) -> m (HardForkState f xs)) -> m (Telescope (K Past) (Current f) xs) -> m (HardForkState f xs) forall a b. (a -> b) -> a -> 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 (Telescope (K Past) (m :.: Current f) xs -> m (Telescope (K Past) (Current f) xs)) -> Telescope (K Past) (m :.: Current f) xs -> m (Telescope (K Past) (Current f) xs) forall a b. (a -> b) -> a -> b $ (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 sequenceCurrent Telescope (K Past) (Current (m :.: f)) xs tel where sequenceCurrent :: Current (m :.: f) a -> (m :.: Current f) a sequenceCurrent :: forall a. Current (m :.: f) a -> (:.:) m (Current f) a sequenceCurrent (Current Bound start (:.:) m f a state) = m (Current f a) -> (:.:) m (Current f) a forall l k (f :: l -> *) (g :: k -> l) (p :: k). f (g p) -> (:.:) f g p Comp (m (Current f a) -> (:.:) m (Current f) a) -> m (Current f a) -> (:.:) m (Current f) a forall a b. (a -> b) -> a -> b $ Bound -> f a -> Current f a forall (f :: * -> *) blk. Bound -> f blk -> Current f blk Current Bound start (f a -> Current f a) -> m (f a) -> m (Current f a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> (:.:) m f a -> m (f a) forall {l} {k} (f :: l -> *) (g :: k -> l) (p :: k). (:.:) f g p -> f (g p) unComp (:.:) m f a state {------------------------------------------------------------------------------- Supporting types -------------------------------------------------------------------------------} -- | Translate @f x@ to @f y@ across an era transition -- -- Typically @f@ will be 'LedgerState' or 'WrapChainDepState'. newtype Translate f x y = Translate { forall (f :: * -> *) x y. Translate f x y -> EpochNo -> f x -> f y translateWith :: EpochNo -> f x -> f y } -- | Forecast a @view y@ from a @state x@ across an era transition. -- -- In addition to the 'Bound' of the transition, this is also told the -- 'SlotNo' we're constructing a forecast for. This enables the translation -- function to take into account any scheduled changes that the final ledger -- view in the preceding era might have. newtype CrossEraForecaster state view x y = CrossEraForecaster { forall (state :: * -> *) (view :: * -> *) x y. CrossEraForecaster state view x y -> Bound -> SlotNo -> state x -> Except OutsideForecastRange (view y) crossEraForecastWith :: Bound -- 'Bound' of the transition (start of the new era) -> SlotNo -- 'SlotNo' we're constructing a forecast for -> state x -> Except OutsideForecastRange (view y) } -- | Knowledge in a particular era of the transition to the next era data TransitionInfo = -- | No transition is yet known for this era -- We instead record the ledger tip (which must be in /this/ era) -- -- NOTE: If we are forecasting, this will be set to the slot number of the -- (past) ledger state in which the forecast was created. This means that -- when we construct an 'EpochInfo' using a 'HardForkLedgerView', the -- range of that 'EpochInfo' will extend a safe zone from that /past/ -- ledger state. TransitionUnknown !(WithOrigin SlotNo) -- | Transition to the next era is known to happen at this 'EpochNo' | TransitionKnown !EpochNo -- | The transition is impossible -- -- This can be due to one of two reasons: -- -- * We are in the final era -- * This era has not actually begun yet (we are forecasting). In this case, -- we cannot look past the safe zone of this era and hence, by definition, -- the transition to the /next/ era cannot happen. | TransitionImpossible deriving (Int -> TransitionInfo -> ShowS [TransitionInfo] -> ShowS TransitionInfo -> String (Int -> TransitionInfo -> ShowS) -> (TransitionInfo -> String) -> ([TransitionInfo] -> ShowS) -> Show TransitionInfo forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a $cshowsPrec :: Int -> TransitionInfo -> ShowS showsPrec :: Int -> TransitionInfo -> ShowS $cshow :: TransitionInfo -> String show :: TransitionInfo -> String $cshowList :: [TransitionInfo] -> ShowS showList :: [TransitionInfo] -> ShowS Show, (forall x. TransitionInfo -> Rep TransitionInfo x) -> (forall x. Rep TransitionInfo x -> TransitionInfo) -> Generic TransitionInfo forall x. Rep TransitionInfo x -> TransitionInfo forall x. TransitionInfo -> Rep TransitionInfo x forall a. (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a $cfrom :: forall x. TransitionInfo -> Rep TransitionInfo x from :: forall x. TransitionInfo -> Rep TransitionInfo x $cto :: forall x. Rep TransitionInfo x -> TransitionInfo to :: forall x. Rep TransitionInfo x -> TransitionInfo Generic, Context -> TransitionInfo -> IO (Maybe ThunkInfo) Proxy TransitionInfo -> String (Context -> TransitionInfo -> IO (Maybe ThunkInfo)) -> (Context -> TransitionInfo -> IO (Maybe ThunkInfo)) -> (Proxy TransitionInfo -> String) -> NoThunks TransitionInfo forall a. (Context -> a -> IO (Maybe ThunkInfo)) -> (Context -> a -> IO (Maybe ThunkInfo)) -> (Proxy a -> String) -> NoThunks a $cnoThunks :: Context -> TransitionInfo -> IO (Maybe ThunkInfo) noThunks :: Context -> TransitionInfo -> IO (Maybe ThunkInfo) $cwNoThunks :: Context -> TransitionInfo -> IO (Maybe ThunkInfo) wNoThunks :: Context -> TransitionInfo -> IO (Maybe ThunkInfo) $cshowTypeOf :: Proxy TransitionInfo -> String showTypeOf :: Proxy TransitionInfo -> String NoThunks)