{-# LANGUAGE DataKinds #-} {-# 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.BasicFunctors import Data.SOP.Counting (Exactly (..)) import Data.SOP.Dict (Dict (..)) import Data.SOP.Index import qualified Data.SOP.InPairs as InPairs import Data.SOP.Strict import Ouroboros.Consensus.Block import Ouroboros.Consensus.Config import Ouroboros.Consensus.HardFork.Combinator import qualified Ouroboros.Consensus.HardFork.Combinator.State as State 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 ((.:)) {------------------------------------------------------------------------------- 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' :: forall (f :: * -> *) a b x (xs :: [*]). (Inject f, CanHardFork xs, Coercible a (f x), Coercible b (f (HardForkBlock xs))) => 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 forall a b. Coercible a b => a -> b coerce (f (HardForkBlock xs) -> b) -> (a -> f (HardForkBlock xs)) -> a -> b forall b c a. (b -> c) -> (a -> b) -> a -> c . 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 forall a b. Coercible a b => a -> b coerce {------------------------------------------------------------------------------- Defaults (to ease implementation) -------------------------------------------------------------------------------} injectNestedCtxt_ :: forall f x xs a. Index xs x -> NestedCtxt_ x f a -> NestedCtxt_ (HardForkBlock xs) f a injectNestedCtxt_ :: 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 = case Index xs x idx of Index xs x IZ -> NestedCtxt_ x f a -> NestedCtxt_ (HardForkBlock (x : xs1)) f a forall x (a :: * -> *) b (xs1 :: [*]). NestedCtxt_ x a b -> NestedCtxt_ (HardForkBlock (x : xs1)) a b NCZ NestedCtxt_ x f a nc IS Index xs1 x idx' -> NestedCtxt_ (HardForkBlock xs1) f a -> NestedCtxt_ (HardForkBlock (y : xs1)) f a forall (xs1 :: [*]) (a :: * -> *) b x. NestedCtxt_ (HardForkBlock xs1) a b -> NestedCtxt_ (HardForkBlock (x : xs1)) a b NCS (Index xs1 x -> NestedCtxt_ x f a -> NestedCtxt_ (HardForkBlock xs1) f a forall (f :: * -> *) x (xs :: [*]) a. Index xs x -> NestedCtxt_ x f a -> NestedCtxt_ (HardForkBlock xs) f a injectNestedCtxt_ Index xs1 x idx' NestedCtxt_ x f a nc) injectQuery :: forall x xs result. Index xs x -> BlockQuery x result -> QueryIfCurrent xs result injectQuery :: forall x (xs :: [*]) result. 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 : xs1) result forall x b (xs :: [*]). BlockQuery x b -> QueryIfCurrent (x : xs) b QZ BlockQuery x result q IS Index xs1 x idx' -> QueryIfCurrent xs1 result -> QueryIfCurrent (y : xs1) result forall (xs :: [*]) b x. QueryIfCurrent xs b -> QueryIfCurrent (x : xs) b QS (Index xs1 x -> BlockQuery x result -> QueryIfCurrent xs1 result forall x (xs :: [*]) result. Index xs x -> BlockQuery x result -> QueryIfCurrent xs result injectQuery Index xs1 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 :: forall (f :: * -> *) x (xs :: [*]). 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 :: forall (xs' :: [*]). 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 {k} (f :: k -> *) (x :: k) (g :: k -> *) (xs1 :: [k]). f x -> Telescope g f (x : xs1) TZ (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 xs1 x idx') = K Past x -> Telescope (K Past) (Current f) xs -> Telescope (K Past) (Current f) (x : xs) forall {k} (g :: k -> *) (x :: k) (f :: k -> *) (xs1 :: [k]). g x -> Telescope g f xs1 -> Telescope g f (x : xs1) TS (Past -> K Past x forall k a (b :: k). a -> K a b K 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 xs1 x idx') go (ExactlyCons Bound _ Exactly xs Bound ExactlyNil) (IS Index xs1 x idx') = case Index xs1 x idx' of {} go Exactly xs' Bound ExactlyNil Index xs' x idx' = case Index xs' x idx' of {} {------------------------------------------------------------------------------- Instances -------------------------------------------------------------------------------} instance Inject I where inject :: forall x (xs :: [*]). CanHardFork xs => 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 {k} (f :: k -> *) a b (x :: k) (xs :: [k]). (Coercible a (f x), Coercible b (NS f xs)) => Proxy f -> Index xs x -> a -> b injectNS' (forall {k} (t :: k). Proxy t forall (t :: * -> *). Proxy t Proxy @I) instance Inject Header where inject :: forall x (xs :: [*]). CanHardFork xs => 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 {k} (f :: k -> *) a b (x :: k) (xs :: [k]). (Coercible a (f x), Coercible b (NS f xs)) => Proxy f -> Index xs x -> a -> b injectNS' (forall {k} (t :: k). Proxy t forall (t :: * -> *). Proxy t Proxy @Header) instance Inject SerialisedHeader where inject :: forall x (xs :: [*]). CanHardFork xs => 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 a b c. (a -> b) -> (a, c) -> (b, c) 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 :: forall x (xs :: [*]). CanHardFork xs => 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 (forall {k} (t :: k). Proxy t forall (t :: * -> Constraint). Proxy t Proxy @SingleEraBlock) Index xs x idx of Dict SingleEraBlock x Dict -> HeaderHash (HardForkBlock xs) -> WrapHeaderHash (HardForkBlock xs) 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 forall (proxy :: * -> *). proxy x -> HeaderHash x -> ShortByteString toShortRawHash (forall t. Proxy t 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 :: forall x (xs :: [*]). CanHardFork xs => 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 {k} (f :: k -> *) a b (x :: k) (xs :: [k]). (Coercible a (f x), Coercible b (NS f xs)) => Proxy f -> Index xs x -> a -> b injectNS' (forall {k} (t :: k). Proxy t forall (t :: * -> *). Proxy t Proxy @GenTx) instance Inject WrapGenTxId where inject :: forall x (xs :: [*]). CanHardFork xs => 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 {k} (f :: k -> *) a b (x :: k) (xs :: [k]). (Coercible a (f x), Coercible b (NS f xs)) => Proxy f -> Index xs x -> a -> b injectNS' (forall {k} (t :: k). Proxy t forall (t :: * -> *). Proxy t Proxy @WrapGenTxId) instance Inject WrapApplyTxErr where inject :: forall x (xs :: [*]). CanHardFork xs => Exactly xs Bound -> Index xs x -> WrapApplyTxErr x -> WrapApplyTxErr (HardForkBlock xs) inject Exactly xs Bound _ = (ApplyTxErr (HardForkBlock xs) -> WrapApplyTxErr (HardForkBlock xs) 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 {k} (f :: k -> *) a b (x :: k) (xs :: [k]). (Coercible a (f x), Coercible b (NS f xs)) => Proxy f -> Index xs x -> a -> b injectNS' (forall {k} (t :: k). Proxy t forall (t :: * -> *). Proxy t Proxy @WrapApplyTxErr) instance Inject (SomeSecond BlockQuery) where inject :: forall x (xs :: [*]). CanHardFork xs => 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) (Either (MismatchEraInfo xs) b) -> SomeSecond BlockQuery (HardForkBlock xs) forall {k1} {k2} (f :: k1 -> k2 -> *) (a :: k1) (b :: k2). f a b -> SomeSecond f a SomeSecond (QueryIfCurrent xs b -> BlockQuery (HardForkBlock xs) (Either (MismatchEraInfo xs) b) forall (xs :: [*]) result. QueryIfCurrent xs result -> BlockQuery (HardForkBlock xs) (Either (MismatchEraInfo 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 :: forall x (xs :: [*]). CanHardFork xs => 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 {k} (f :: k -> *) a b (x :: k) (xs :: [k]). (Coercible a (f x), Coercible b (NS f xs)) => Proxy f -> Index xs x -> a -> b injectNS' (forall {k} (t :: k). Proxy t forall (t :: * -> *). Proxy t Proxy @AnnTip) instance Inject LedgerState where inject :: forall x (xs :: [*]). CanHardFork xs => 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 :: forall x (xs :: [*]). CanHardFork xs => 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) forall a b. Coercible a b => a -> b 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 :: forall x (xs :: [*]). CanHardFork xs => 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) headerStateTip :: WithOrigin (AnnTip x) headerStateChainDep :: ChainDepState (BlockProtocol x) headerStateTip :: forall blk. HeaderState blk -> WithOrigin (AnnTip blk) headerStateChainDep :: forall blk. HeaderState blk -> ChainDepState (BlockProtocol blk) ..} = HeaderState { headerStateTip :: WithOrigin (AnnTip (HardForkBlock xs)) headerStateTip = Exactly xs Bound -> Index xs x -> AnnTip x -> AnnTip (HardForkBlock xs) forall x (xs :: [*]). CanHardFork xs => 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 x (xs :: [*]). CanHardFork xs => 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 :: forall x (xs :: [*]). CanHardFork xs => 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 ledgerState :: LedgerState x headerState :: HeaderState x ledgerState :: forall blk. ExtLedgerState blk -> LedgerState blk headerState :: forall blk. ExtLedgerState blk -> HeaderState blk ..} = ExtLedgerState { ledgerState :: LedgerState (HardForkBlock xs) ledgerState = Exactly xs Bound -> Index xs x -> LedgerState x -> LedgerState (HardForkBlock xs) forall x (xs :: [*]). CanHardFork xs => 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 x (xs :: [*]). CanHardFork xs => 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 :: forall x (xs :: [*]). CanHardFork (x : xs) => TopLevelConfig (HardForkBlock (x : xs)) -> ExtLedgerState x -> ExtLedgerState (HardForkBlock (x : xs)) injectInitialExtLedgerState TopLevelConfig (HardForkBlock (x : xs)) cfg ExtLedgerState x extLedgerState0 = 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 (xs :: [*]) (f :: * -> *). SListIN NP xs => (forall a. f a) -> NP f 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