{-# LANGUAGE DataKinds #-} {-# LANGUAGE DisambiguateRecordFields #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} module Ouroboros.Consensus.HardFork.Combinator.Embed.Nary ( Inject (..) , inject' -- * Defaults , injectHardForkState , injectNestedCtxt_ , injectQuery -- * Initial 'ExtLedgerState' , injectInitialExtLedgerState ) where import Data.Bifunctor (first) import Data.Coerce (Coercible, coerce) import Data.SOP.Dict (Dict (..)) import Data.SOP.Strict import Ouroboros.Consensus.Block import Ouroboros.Consensus.Config import qualified Ouroboros.Consensus.HardFork.History as History import Ouroboros.Consensus.HeaderValidation (AnnTip, HeaderState (..), genesisHeaderState) import Ouroboros.Consensus.Ledger.Extended (ExtLedgerState (..)) import Ouroboros.Consensus.Storage.Serialisation import Ouroboros.Consensus.TypeFamilyWrappers import Ouroboros.Consensus.Util ((.:)) import Ouroboros.Consensus.Util.Counting (Exactly (..)) import Ouroboros.Consensus.Util.SOP import Ouroboros.Consensus.HardFork.Combinator import qualified Ouroboros.Consensus.HardFork.Combinator.State as State import qualified Ouroboros.Consensus.HardFork.Combinator.Util.InPairs as InPairs {------------------------------------------------------------------------------- Injection for a single block into a HardForkBlock -------------------------------------------------------------------------------} class Inject f where inject :: forall x xs. CanHardFork xs => Exactly xs History.Bound -- ^ Start bound of each era -> Index xs x -> f x -> f (HardForkBlock xs) inject' :: forall f a b x xs. ( Inject f , CanHardFork xs , Coercible a (f x) , Coercible b (f (HardForkBlock xs)) ) => Proxy f -> Exactly xs History.Bound -> Index xs x -> a -> b inject' :: Proxy f -> Exactly xs Bound -> Index xs x -> a -> b inject' Proxy f _ Exactly xs Bound startBounds Index xs x idx = f (HardForkBlock xs) -> b coerce (f (HardForkBlock xs) -> b) -> (a -> f (HardForkBlock xs)) -> a -> b forall b c a. (b -> c) -> (a -> b) -> a -> c . Exactly xs Bound -> Index xs x -> f x -> f (HardForkBlock xs) forall (f :: * -> *) x (xs :: [*]). (Inject f, CanHardFork xs) => Exactly xs Bound -> Index xs x -> f x -> f (HardForkBlock xs) inject @f Exactly xs Bound startBounds Index xs x idx (f x -> f (HardForkBlock xs)) -> (a -> f x) -> a -> f (HardForkBlock xs) forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> f x coerce {------------------------------------------------------------------------------- Defaults (to ease implementation) -------------------------------------------------------------------------------} injectNestedCtxt_ :: forall f x xs a. Index xs x -> NestedCtxt_ x f a -> NestedCtxt_ (HardForkBlock xs) f a injectNestedCtxt_ :: Index xs x -> NestedCtxt_ x f a -> NestedCtxt_ (HardForkBlock xs) f a injectNestedCtxt_ Index xs x idx NestedCtxt_ x f a nc = case Index xs x idx of Index xs x IZ -> NestedCtxt_ x f a -> NestedCtxt_ (HardForkBlock (x : xs)) f a forall x (f :: * -> *) a (xs :: [*]). NestedCtxt_ x f a -> NestedCtxt_ (HardForkBlock (x : xs)) f a NCZ NestedCtxt_ x f a nc IS Index xs x idx' -> NestedCtxt_ (HardForkBlock xs) f a -> NestedCtxt_ (HardForkBlock (y : xs)) f a forall (xs :: [*]) (f :: * -> *) a x. NestedCtxt_ (HardForkBlock xs) f a -> NestedCtxt_ (HardForkBlock (x : xs)) f a NCS (Index xs x -> NestedCtxt_ x f a -> NestedCtxt_ (HardForkBlock xs) f a forall (f :: * -> *) x (xs :: [*]) a. Index xs x -> NestedCtxt_ x f a -> NestedCtxt_ (HardForkBlock xs) f a injectNestedCtxt_ Index xs x idx' NestedCtxt_ x f a nc) injectQuery :: forall x xs result. Index xs x -> BlockQuery x result -> QueryIfCurrent xs result injectQuery :: Index xs x -> BlockQuery x result -> QueryIfCurrent xs result injectQuery Index xs x idx BlockQuery x result q = case Index xs x idx of Index xs x IZ -> BlockQuery x result -> QueryIfCurrent (x : xs) result forall x result (xs :: [*]). BlockQuery x result -> QueryIfCurrent (x : xs) result QZ BlockQuery x result q IS Index xs x idx' -> QueryIfCurrent xs result -> QueryIfCurrent (y : xs) result forall (xs :: [*]) result x. QueryIfCurrent xs result -> QueryIfCurrent (x : xs) result QS (Index xs x -> BlockQuery x result -> QueryIfCurrent xs result forall x (xs :: [*]) result. Index xs x -> BlockQuery x result -> QueryIfCurrent xs result injectQuery Index xs x idx' BlockQuery x result q) injectHardForkState :: forall f x xs. Exactly xs History.Bound -- ^ Start bound of each era -> Index xs x -> f x -> HardForkState f xs injectHardForkState :: Exactly xs Bound -> Index xs x -> f x -> HardForkState f xs injectHardForkState Exactly xs Bound startBounds Index xs x idx f x x = 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) -> Telescope (K Past) (Current f) xs -> HardForkState f xs forall a b. (a -> b) -> a -> b $ Exactly xs Bound -> Index xs x -> Telescope (K Past) (Current f) xs forall (xs' :: [*]). Exactly xs' Bound -> Index xs' x -> Telescope (K Past) (Current f) xs' go Exactly xs Bound startBounds Index xs x idx where go :: Exactly xs' History.Bound -> Index xs' x -> Telescope (K State.Past) (State.Current f) xs' go :: Exactly xs' Bound -> Index xs' x -> Telescope (K Past) (Current f) xs' go (ExactlyCons Bound start Exactly xs Bound _) Index xs' x IZ = 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 :: forall (f :: * -> *) blk. Bound -> f blk -> Current f blk State.Current { currentStart :: Bound currentStart = Bound start, currentState :: f x currentState = f x x }) go (ExactlyCons Bound start startBounds' :: Exactly xs Bound startBounds'@(ExactlyCons Bound nextStart Exactly xs Bound _)) (IS Index xs x idx') = K Past x -> Telescope (K Past) (Current f) xs -> Telescope (K Past) (Current f) (x : xs) forall a (g :: a -> *) (x :: a) (f :: a -> *) (xs :: [a]). g x -> Telescope g f xs -> Telescope g f (x : xs) TS (Past -> K Past x forall k a (b :: k). a -> K a b K Past :: Bound -> Bound -> Past State.Past { pastStart :: Bound pastStart = Bound start, pastEnd :: Bound pastEnd = Bound nextStart }) (Exactly xs Bound -> Index xs x -> Telescope (K Past) (Current f) xs forall (xs' :: [*]). Exactly xs' Bound -> Index xs' x -> Telescope (K Past) (Current f) xs' go Exactly xs Bound startBounds' Index xs x Index xs x idx') go (ExactlyCons Bound _ Exactly xs Bound ExactlyNil) (IS Index xs x idx') = case Index xs x idx' of {} {------------------------------------------------------------------------------- Instances -------------------------------------------------------------------------------} instance Inject I where inject :: Exactly xs Bound -> Index xs x -> I x -> I (HardForkBlock xs) inject Exactly xs Bound _ = Proxy I -> Index xs x -> I x -> I (HardForkBlock xs) forall a1 (f :: a1 -> *) a2 b (x :: a1) (xs :: [a1]). (Coercible a2 (f x), Coercible b (NS f xs)) => Proxy f -> Index xs x -> a2 -> b injectNS' (Proxy I forall k (t :: k). Proxy t Proxy @I) instance Inject Header where inject :: Exactly xs Bound -> Index xs x -> Header x -> Header (HardForkBlock xs) inject Exactly xs Bound _ = Proxy Header -> Index xs x -> Header x -> Header (HardForkBlock xs) forall a1 (f :: a1 -> *) a2 b (x :: a1) (xs :: [a1]). (Coercible a2 (f x), Coercible b (NS f xs)) => Proxy f -> Index xs x -> a2 -> b injectNS' (Proxy Header forall k (t :: k). Proxy t Proxy @Header) instance Inject SerialisedHeader where inject :: Exactly xs Bound -> Index xs x -> SerialisedHeader x -> SerialisedHeader (HardForkBlock xs) inject Exactly xs Bound _ Index xs x idx = (SomeSecond (NestedCtxt Header) (HardForkBlock xs), ByteString) -> SerialisedHeader (HardForkBlock xs) forall blk. (SomeSecond (NestedCtxt Header) blk, ByteString) -> SerialisedHeader blk serialisedHeaderFromPair ((SomeSecond (NestedCtxt Header) (HardForkBlock xs), ByteString) -> SerialisedHeader (HardForkBlock xs)) -> (SerialisedHeader x -> (SomeSecond (NestedCtxt Header) (HardForkBlock xs), ByteString)) -> SerialisedHeader x -> SerialisedHeader (HardForkBlock xs) forall b c a. (b -> c) -> (a -> b) -> a -> c . (SomeSecond (NestedCtxt Header) x -> SomeSecond (NestedCtxt Header) (HardForkBlock xs)) -> (SomeSecond (NestedCtxt Header) x, ByteString) -> (SomeSecond (NestedCtxt Header) (HardForkBlock xs), ByteString) forall (p :: * -> * -> *) a b c. Bifunctor p => (a -> b) -> p a c -> p b c first ((forall a. NestedCtxt_ x Header a -> NestedCtxt_ (HardForkBlock xs) Header a) -> SomeSecond (NestedCtxt Header) x -> SomeSecond (NestedCtxt Header) (HardForkBlock xs) forall blk (f :: * -> *) blk' (f' :: * -> *). (forall a. NestedCtxt_ blk f a -> NestedCtxt_ blk' f' a) -> SomeSecond (NestedCtxt f) blk -> SomeSecond (NestedCtxt f') blk' mapSomeNestedCtxt (Index xs x -> NestedCtxt_ x Header a -> NestedCtxt_ (HardForkBlock xs) Header a forall (f :: * -> *) x (xs :: [*]) a. Index xs x -> NestedCtxt_ x f a -> NestedCtxt_ (HardForkBlock xs) f a injectNestedCtxt_ Index xs x idx)) ((SomeSecond (NestedCtxt Header) x, ByteString) -> (SomeSecond (NestedCtxt Header) (HardForkBlock xs), ByteString)) -> (SerialisedHeader x -> (SomeSecond (NestedCtxt Header) x, ByteString)) -> SerialisedHeader x -> (SomeSecond (NestedCtxt Header) (HardForkBlock xs), ByteString) forall b c a. (b -> c) -> (a -> b) -> a -> c . SerialisedHeader x -> (SomeSecond (NestedCtxt Header) x, ByteString) forall blk. SerialisedHeader blk -> (SomeSecond (NestedCtxt Header) blk, ByteString) serialisedHeaderToPair instance Inject WrapHeaderHash where inject :: Exactly xs Bound -> Index xs x -> WrapHeaderHash x -> WrapHeaderHash (HardForkBlock xs) inject Exactly xs Bound _ (Index xs x idx :: Index xs x) = case Proxy SingleEraBlock -> Index xs x -> Dict SingleEraBlock x forall k (c :: k -> Constraint) (xs :: [k]) (x :: k). All c xs => Proxy c -> Index xs x -> Dict c x dictIndexAll (Proxy SingleEraBlock forall k (t :: k). Proxy t Proxy @SingleEraBlock) Index xs x idx of Dict SingleEraBlock x Dict -> OneEraHash xs -> WrapHeaderHash (HardForkBlock xs) forall blk. HeaderHash blk -> WrapHeaderHash blk WrapHeaderHash (OneEraHash xs -> WrapHeaderHash (HardForkBlock xs)) -> (WrapHeaderHash x -> OneEraHash xs) -> WrapHeaderHash x -> WrapHeaderHash (HardForkBlock xs) forall b c a. (b -> c) -> (a -> b) -> a -> c . ShortByteString -> OneEraHash xs forall k (xs :: [k]). ShortByteString -> OneEraHash xs OneEraHash (ShortByteString -> OneEraHash xs) -> (WrapHeaderHash x -> ShortByteString) -> WrapHeaderHash x -> OneEraHash xs forall b c a. (b -> c) -> (a -> b) -> a -> c . Proxy x -> HeaderHash x -> ShortByteString forall blk (proxy :: * -> *). ConvertRawHash blk => proxy blk -> HeaderHash blk -> ShortByteString toShortRawHash (Proxy x forall k (t :: k). Proxy t Proxy @x) (HeaderHash x -> ShortByteString) -> (WrapHeaderHash x -> HeaderHash x) -> WrapHeaderHash x -> ShortByteString forall b c a. (b -> c) -> (a -> b) -> a -> c . WrapHeaderHash x -> HeaderHash x forall blk. WrapHeaderHash blk -> HeaderHash blk unwrapHeaderHash instance Inject GenTx where inject :: Exactly xs Bound -> Index xs x -> GenTx x -> GenTx (HardForkBlock xs) inject Exactly xs Bound _ = Proxy GenTx -> Index xs x -> GenTx x -> GenTx (HardForkBlock xs) forall a1 (f :: a1 -> *) a2 b (x :: a1) (xs :: [a1]). (Coercible a2 (f x), Coercible b (NS f xs)) => Proxy f -> Index xs x -> a2 -> b injectNS' (Proxy GenTx forall k (t :: k). Proxy t Proxy @GenTx) instance Inject WrapGenTxId where inject :: Exactly xs Bound -> Index xs x -> WrapGenTxId x -> WrapGenTxId (HardForkBlock xs) inject Exactly xs Bound _ = Proxy WrapGenTxId -> Index xs x -> WrapGenTxId x -> WrapGenTxId (HardForkBlock xs) forall a1 (f :: a1 -> *) a2 b (x :: a1) (xs :: [a1]). (Coercible a2 (f x), Coercible b (NS f xs)) => Proxy f -> Index xs x -> a2 -> b injectNS' (Proxy WrapGenTxId forall k (t :: k). Proxy t Proxy @WrapGenTxId) instance Inject WrapApplyTxErr where inject :: Exactly xs Bound -> Index xs x -> WrapApplyTxErr x -> WrapApplyTxErr (HardForkBlock xs) inject Exactly xs Bound _ = (HardForkApplyTxErr xs -> WrapApplyTxErr (HardForkBlock xs) forall blk. ApplyTxErr blk -> WrapApplyTxErr blk WrapApplyTxErr (HardForkApplyTxErr xs -> WrapApplyTxErr (HardForkBlock xs)) -> (OneEraApplyTxErr xs -> HardForkApplyTxErr xs) -> OneEraApplyTxErr xs -> WrapApplyTxErr (HardForkBlock xs) forall b c a. (b -> c) -> (a -> b) -> a -> c . OneEraApplyTxErr xs -> HardForkApplyTxErr xs forall (xs :: [*]). OneEraApplyTxErr xs -> HardForkApplyTxErr xs HardForkApplyTxErrFromEra) (OneEraApplyTxErr xs -> WrapApplyTxErr (HardForkBlock xs)) -> (Index xs x -> WrapApplyTxErr x -> OneEraApplyTxErr xs) -> Index xs x -> WrapApplyTxErr x -> WrapApplyTxErr (HardForkBlock xs) forall y z x0 x1. (y -> z) -> (x0 -> x1 -> y) -> x0 -> x1 -> z .: Proxy WrapApplyTxErr -> Index xs x -> WrapApplyTxErr x -> OneEraApplyTxErr xs forall a1 (f :: a1 -> *) a2 b (x :: a1) (xs :: [a1]). (Coercible a2 (f x), Coercible b (NS f xs)) => Proxy f -> Index xs x -> a2 -> b injectNS' (Proxy WrapApplyTxErr forall k (t :: k). Proxy t Proxy @WrapApplyTxErr) instance Inject (SomeSecond BlockQuery) where inject :: Exactly xs Bound -> Index xs x -> SomeSecond BlockQuery x -> SomeSecond BlockQuery (HardForkBlock xs) inject Exactly xs Bound _ Index xs x idx (SomeSecond BlockQuery x b q) = BlockQuery (HardForkBlock xs) (HardForkQueryResult xs b) -> SomeSecond BlockQuery (HardForkBlock xs) forall (f :: * -> * -> *) a b. f a b -> SomeSecond f a SomeSecond (QueryIfCurrent xs b -> BlockQuery (HardForkBlock xs) (HardForkQueryResult xs b) forall (xs :: [*]) result. QueryIfCurrent xs result -> BlockQuery (HardForkBlock xs) (HardForkQueryResult xs result) QueryIfCurrent (Index xs x -> BlockQuery x b -> QueryIfCurrent xs b forall x (xs :: [*]) result. Index xs x -> BlockQuery x result -> QueryIfCurrent xs result injectQuery Index xs x idx BlockQuery x b q)) instance Inject AnnTip where inject :: Exactly xs Bound -> Index xs x -> AnnTip x -> AnnTip (HardForkBlock xs) inject Exactly xs Bound _ = NS AnnTip xs -> AnnTip (HardForkBlock xs) forall (xs :: [*]). SListI xs => NS AnnTip xs -> AnnTip (HardForkBlock xs) undistribAnnTip (NS AnnTip xs -> AnnTip (HardForkBlock xs)) -> (Index xs x -> AnnTip x -> NS AnnTip xs) -> Index xs x -> AnnTip x -> AnnTip (HardForkBlock xs) forall y z x0 x1. (y -> z) -> (x0 -> x1 -> y) -> x0 -> x1 -> z .: Proxy AnnTip -> Index xs x -> AnnTip x -> NS AnnTip xs forall a1 (f :: a1 -> *) a2 b (x :: a1) (xs :: [a1]). (Coercible a2 (f x), Coercible b (NS f xs)) => Proxy f -> Index xs x -> a2 -> b injectNS' (Proxy AnnTip forall k (t :: k). Proxy t Proxy @AnnTip) instance Inject LedgerState where inject :: Exactly xs Bound -> Index xs x -> LedgerState x -> LedgerState (HardForkBlock xs) inject Exactly xs Bound startBounds Index xs x idx = HardForkState LedgerState xs -> LedgerState (HardForkBlock xs) forall (xs :: [*]). HardForkState LedgerState xs -> LedgerState (HardForkBlock xs) HardForkLedgerState (HardForkState LedgerState xs -> LedgerState (HardForkBlock xs)) -> (LedgerState x -> HardForkState LedgerState xs) -> LedgerState x -> LedgerState (HardForkBlock xs) forall b c a. (b -> c) -> (a -> b) -> a -> c . Exactly xs Bound -> Index xs x -> LedgerState x -> HardForkState LedgerState xs forall (f :: * -> *) x (xs :: [*]). Exactly xs Bound -> Index xs x -> f x -> HardForkState f xs injectHardForkState Exactly xs Bound startBounds Index xs x idx instance Inject WrapChainDepState where inject :: Exactly xs Bound -> Index xs x -> WrapChainDepState x -> WrapChainDepState (HardForkBlock xs) inject Exactly xs Bound startBounds Index xs x idx = HardForkState WrapChainDepState xs -> WrapChainDepState (HardForkBlock xs) coerce (HardForkState WrapChainDepState xs -> WrapChainDepState (HardForkBlock xs)) -> (WrapChainDepState x -> HardForkState WrapChainDepState xs) -> WrapChainDepState x -> WrapChainDepState (HardForkBlock xs) forall b c a. (b -> c) -> (a -> b) -> a -> c . Exactly xs Bound -> Index xs x -> WrapChainDepState x -> HardForkState WrapChainDepState xs forall (f :: * -> *) x (xs :: [*]). Exactly xs Bound -> Index xs x -> f x -> HardForkState f xs injectHardForkState Exactly xs Bound startBounds Index xs x idx instance Inject HeaderState where inject :: Exactly xs Bound -> Index xs x -> HeaderState x -> HeaderState (HardForkBlock xs) inject Exactly xs Bound startBounds Index xs x idx HeaderState {WithOrigin (AnnTip x) ChainDepState (BlockProtocol x) headerStateChainDep :: forall blk. HeaderState blk -> ChainDepState (BlockProtocol blk) headerStateTip :: forall blk. HeaderState blk -> WithOrigin (AnnTip blk) headerStateChainDep :: ChainDepState (BlockProtocol x) headerStateTip :: WithOrigin (AnnTip x) ..} = HeaderState :: forall blk. WithOrigin (AnnTip blk) -> ChainDepState (BlockProtocol blk) -> HeaderState blk HeaderState { headerStateTip :: WithOrigin (AnnTip (HardForkBlock xs)) headerStateTip = Exactly xs Bound -> Index xs x -> AnnTip x -> AnnTip (HardForkBlock xs) forall (f :: * -> *) x (xs :: [*]). (Inject f, CanHardFork xs) => Exactly xs Bound -> Index xs x -> f x -> f (HardForkBlock xs) inject Exactly xs Bound startBounds Index xs x idx (AnnTip x -> AnnTip (HardForkBlock xs)) -> WithOrigin (AnnTip x) -> WithOrigin (AnnTip (HardForkBlock xs)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> WithOrigin (AnnTip x) headerStateTip , headerStateChainDep :: ChainDepState (BlockProtocol (HardForkBlock xs)) headerStateChainDep = WrapChainDepState (HardForkBlock xs) -> ChainDepState (BlockProtocol (HardForkBlock xs)) forall blk. WrapChainDepState blk -> ChainDepState (BlockProtocol blk) unwrapChainDepState (WrapChainDepState (HardForkBlock xs) -> ChainDepState (BlockProtocol (HardForkBlock xs))) -> WrapChainDepState (HardForkBlock xs) -> ChainDepState (BlockProtocol (HardForkBlock xs)) forall a b. (a -> b) -> a -> b $ Exactly xs Bound -> Index xs x -> WrapChainDepState x -> WrapChainDepState (HardForkBlock xs) forall (f :: * -> *) x (xs :: [*]). (Inject f, CanHardFork xs) => Exactly xs Bound -> Index xs x -> f x -> f (HardForkBlock xs) inject Exactly xs Bound startBounds Index xs x idx (WrapChainDepState x -> WrapChainDepState (HardForkBlock xs)) -> WrapChainDepState x -> WrapChainDepState (HardForkBlock xs) forall a b. (a -> b) -> a -> b $ ChainDepState (BlockProtocol x) -> WrapChainDepState x forall blk. ChainDepState (BlockProtocol blk) -> WrapChainDepState blk WrapChainDepState ChainDepState (BlockProtocol x) headerStateChainDep } instance Inject ExtLedgerState where inject :: Exactly xs Bound -> Index xs x -> ExtLedgerState x -> ExtLedgerState (HardForkBlock xs) inject Exactly xs Bound startBounds Index xs x idx ExtLedgerState {LedgerState x HeaderState x headerState :: forall blk. ExtLedgerState blk -> HeaderState blk ledgerState :: forall blk. ExtLedgerState blk -> LedgerState blk headerState :: HeaderState x ledgerState :: LedgerState x ..} = ExtLedgerState :: forall blk. LedgerState blk -> HeaderState blk -> ExtLedgerState blk ExtLedgerState { ledgerState :: LedgerState (HardForkBlock xs) ledgerState = Exactly xs Bound -> Index xs x -> LedgerState x -> LedgerState (HardForkBlock xs) forall (f :: * -> *) x (xs :: [*]). (Inject f, CanHardFork xs) => Exactly xs Bound -> Index xs x -> f x -> f (HardForkBlock xs) inject Exactly xs Bound startBounds Index xs x idx LedgerState x ledgerState , headerState :: HeaderState (HardForkBlock xs) headerState = Exactly xs Bound -> Index xs x -> HeaderState x -> HeaderState (HardForkBlock xs) forall (f :: * -> *) x (xs :: [*]). (Inject f, CanHardFork xs) => Exactly xs Bound -> Index xs x -> f x -> f (HardForkBlock xs) inject Exactly xs Bound startBounds Index xs x idx HeaderState x headerState } {------------------------------------------------------------------------------- Initial ExtLedgerState -------------------------------------------------------------------------------} -- | Inject the first era's initial 'ExtLedgerState' and trigger any -- translations that should take place in the very first slot. -- -- Performs any hard forks scheduled via 'TriggerHardForkAtEpoch'. -- -- Note: we can translate across multiple eras when computing the initial ledger -- state, but we do not support translation across multiple eras in general; -- extending 'applyChainTick' to translate across more than one era is not -- problematic, but extending 'ledgerViewForecastAt' is a lot more subtle; see -- @forecastNotFinal@. injectInitialExtLedgerState :: forall x xs. CanHardFork (x ': xs) => TopLevelConfig (HardForkBlock (x ': xs)) -> ExtLedgerState x -> ExtLedgerState (HardForkBlock (x ': xs)) injectInitialExtLedgerState :: TopLevelConfig (HardForkBlock (x : xs)) -> ExtLedgerState x -> ExtLedgerState (HardForkBlock (x : xs)) injectInitialExtLedgerState TopLevelConfig (HardForkBlock (x : xs)) cfg ExtLedgerState x extLedgerState0 = ExtLedgerState :: forall blk. LedgerState blk -> HeaderState blk -> ExtLedgerState blk ExtLedgerState { ledgerState :: LedgerState (HardForkBlock (x : xs)) ledgerState = LedgerState (HardForkBlock (x : xs)) targetEraLedgerState , headerState :: HeaderState (HardForkBlock (x : xs)) headerState = HeaderState (HardForkBlock (x : xs)) targetEraHeaderState } where cfgs :: NP TopLevelConfig (x ': xs) cfgs :: NP TopLevelConfig (x : xs) cfgs = EpochInfo (Except PastHorizonException) -> TopLevelConfig (HardForkBlock (x : xs)) -> NP TopLevelConfig (x : xs) forall (xs :: [*]). All SingleEraBlock xs => EpochInfo (Except PastHorizonException) -> TopLevelConfig (HardForkBlock xs) -> NP TopLevelConfig xs distribTopLevelConfig (HardForkLedgerConfig (x : xs) -> HardForkState LedgerState (x : xs) -> EpochInfo (Except PastHorizonException) forall (xs :: [*]). All SingleEraBlock xs => HardForkLedgerConfig xs -> HardForkState LedgerState xs -> EpochInfo (Except PastHorizonException) State.epochInfoLedger (TopLevelConfig (HardForkBlock (x : xs)) -> LedgerConfig (HardForkBlock (x : xs)) forall blk. TopLevelConfig blk -> LedgerConfig blk configLedger TopLevelConfig (HardForkBlock (x : xs)) cfg) (LedgerState (HardForkBlock (x : xs)) -> HardForkState LedgerState (x : xs) forall (xs :: [*]). LedgerState (HardForkBlock xs) -> HardForkState LedgerState xs hardForkLedgerStatePerEra LedgerState (HardForkBlock (x : xs)) targetEraLedgerState)) TopLevelConfig (HardForkBlock (x : xs)) cfg targetEraLedgerState :: LedgerState (HardForkBlock (x ': xs)) targetEraLedgerState :: LedgerState (HardForkBlock (x : xs)) targetEraLedgerState = HardForkState LedgerState (x : xs) -> LedgerState (HardForkBlock (x : xs)) forall (xs :: [*]). HardForkState LedgerState xs -> LedgerState (HardForkBlock xs) HardForkLedgerState (HardForkState LedgerState (x : xs) -> LedgerState (HardForkBlock (x : xs))) -> HardForkState LedgerState (x : xs) -> LedgerState (HardForkBlock (x : xs)) forall a b. (a -> b) -> a -> b $ -- We can immediately extend it to the right slot, executing any -- scheduled hard forks in the first slot HardForkLedgerConfig (x : xs) -> SlotNo -> HardForkState LedgerState (x : xs) -> HardForkState LedgerState (x : xs) forall (xs :: [*]). CanHardFork xs => HardForkLedgerConfig xs -> SlotNo -> HardForkState LedgerState xs -> HardForkState LedgerState xs State.extendToSlot (TopLevelConfig (HardForkBlock (x : xs)) -> LedgerConfig (HardForkBlock (x : xs)) forall blk. TopLevelConfig blk -> LedgerConfig blk configLedger TopLevelConfig (HardForkBlock (x : xs)) cfg) (Word64 -> SlotNo SlotNo Word64 0) (LedgerState x -> HardForkState LedgerState (x : xs) forall (f :: * -> *) x (xs :: [*]). f x -> HardForkState f (x : xs) initHardForkState (ExtLedgerState x -> LedgerState x forall blk. ExtLedgerState blk -> LedgerState blk ledgerState ExtLedgerState x extLedgerState0)) firstEraChainDepState :: HardForkChainDepState (x ': xs) firstEraChainDepState :: HardForkChainDepState (x : xs) firstEraChainDepState = WrapChainDepState x -> HardForkChainDepState (x : xs) forall (f :: * -> *) x (xs :: [*]). f x -> HardForkState f (x : xs) initHardForkState (WrapChainDepState x -> HardForkChainDepState (x : xs)) -> WrapChainDepState x -> HardForkChainDepState (x : xs) forall a b. (a -> b) -> a -> b $ ChainDepState (BlockProtocol x) -> WrapChainDepState x forall blk. ChainDepState (BlockProtocol blk) -> WrapChainDepState blk WrapChainDepState (ChainDepState (BlockProtocol x) -> WrapChainDepState x) -> ChainDepState (BlockProtocol x) -> WrapChainDepState x forall a b. (a -> b) -> a -> b $ HeaderState x -> ChainDepState (BlockProtocol x) forall blk. HeaderState blk -> ChainDepState (BlockProtocol blk) headerStateChainDep (HeaderState x -> ChainDepState (BlockProtocol x)) -> HeaderState x -> ChainDepState (BlockProtocol x) forall a b. (a -> b) -> a -> b $ ExtLedgerState x -> HeaderState x forall blk. ExtLedgerState blk -> HeaderState blk headerState ExtLedgerState x extLedgerState0 targetEraChainDepState :: HardForkChainDepState (x ': xs) targetEraChainDepState :: HardForkChainDepState (x : xs) targetEraChainDepState = -- Align the 'ChainDepState' with the ledger state of the target era. InPairs (Translate WrapChainDepState) (x : xs) -> NP (LedgerState -.-> (WrapChainDepState -.-> WrapChainDepState)) (x : xs) -> HardForkState LedgerState (x : xs) -> HardForkChainDepState (x : xs) -> HardForkChainDepState (x : xs) 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 State.align (NP WrapConsensusConfig (x : xs) -> InPairs (RequiringBoth WrapConsensusConfig (Translate WrapChainDepState)) (x : xs) -> InPairs (Translate WrapChainDepState) (x : xs) forall k (h :: k -> *) (xs :: [k]) (f :: k -> k -> *). NP h xs -> InPairs (RequiringBoth h f) xs -> InPairs f xs InPairs.requiringBoth ((forall a. TopLevelConfig a -> WrapConsensusConfig a) -> NP TopLevelConfig (x : xs) -> NP WrapConsensusConfig (x : 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 (ConsensusConfig (BlockProtocol a) -> WrapConsensusConfig a forall blk. ConsensusConfig (BlockProtocol blk) -> WrapConsensusConfig blk WrapConsensusConfig (ConsensusConfig (BlockProtocol a) -> WrapConsensusConfig a) -> (TopLevelConfig a -> ConsensusConfig (BlockProtocol a)) -> TopLevelConfig a -> WrapConsensusConfig a forall b c a. (b -> c) -> (a -> b) -> a -> c . TopLevelConfig a -> ConsensusConfig (BlockProtocol a) forall blk. TopLevelConfig blk -> ConsensusConfig (BlockProtocol blk) configConsensus) NP TopLevelConfig (x : xs) cfgs) (EraTranslation (x : xs) -> InPairs (RequiringBoth WrapConsensusConfig (Translate WrapChainDepState)) (x : xs) forall (xs :: [*]). EraTranslation xs -> InPairs (RequiringBoth WrapConsensusConfig (Translate WrapChainDepState)) xs translateChainDepState EraTranslation (x : xs) forall (xs :: [*]). CanHardFork xs => EraTranslation xs hardForkEraTranslation)) ((forall a. (-.->) LedgerState (WrapChainDepState -.-> WrapChainDepState) a) -> NP (LedgerState -.-> (WrapChainDepState -.-> WrapChainDepState)) (x : xs) forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *). (HPure h, SListIN h xs) => (forall (a :: k). f a) -> h f xs hpure ((LedgerState a -> WrapChainDepState a -> WrapChainDepState a) -> (-.->) LedgerState (WrapChainDepState -.-> WrapChainDepState) a forall k (f :: k -> *) (a :: k) (f' :: k -> *) (f'' :: k -> *). (f a -> f' a -> f'' a) -> (-.->) f (f' -.-> f'') a fn_2 (\LedgerState a _ WrapChainDepState a st -> WrapChainDepState a st))) (LedgerState (HardForkBlock (x : xs)) -> HardForkState LedgerState (x : xs) forall (xs :: [*]). LedgerState (HardForkBlock xs) -> HardForkState LedgerState xs hardForkLedgerStatePerEra LedgerState (HardForkBlock (x : xs)) targetEraLedgerState) HardForkChainDepState (x : xs) firstEraChainDepState targetEraHeaderState :: HeaderState (HardForkBlock (x ': xs)) targetEraHeaderState :: HeaderState (HardForkBlock (x : xs)) targetEraHeaderState = ChainDepState (BlockProtocol (HardForkBlock (x : xs))) -> HeaderState (HardForkBlock (x : xs)) forall blk. ChainDepState (BlockProtocol blk) -> HeaderState blk genesisHeaderState ChainDepState (BlockProtocol (HardForkBlock (x : xs))) HardForkChainDepState (x : xs) targetEraChainDepState