{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-} module Ouroboros.Consensus.HardFork.Combinator.Block ( -- * Type family instances Header (..) , NestedCtxt_ (..) -- * AnnTip , distribAnnTip , undistribAnnTip ) where import Data.Function (on) import Data.Functor.Product import Data.Kind (Type) import Data.SOP.BasicFunctors import Data.SOP.Constraint import Data.SOP.Index import qualified Data.SOP.Match as Match import Data.SOP.Strict import Data.Typeable (Typeable) import Data.Word import NoThunks.Class (NoThunks) import Ouroboros.Consensus.Block import Ouroboros.Consensus.HardFork.Combinator.Abstract import Ouroboros.Consensus.HardFork.Combinator.AcrossEras import Ouroboros.Consensus.HardFork.Combinator.Basics import Ouroboros.Consensus.HeaderValidation import Ouroboros.Consensus.TypeFamilyWrappers import Ouroboros.Consensus.Util (ShowProxy, (.:)) {------------------------------------------------------------------------------- GetHeader -------------------------------------------------------------------------------} newtype instance Header (HardForkBlock xs) = HardForkHeader { forall (xs :: [*]). Header (HardForkBlock xs) -> OneEraHeader xs getHardForkHeader :: OneEraHeader xs } deriving (Int -> Header (HardForkBlock xs) -> ShowS [Header (HardForkBlock xs)] -> ShowS Header (HardForkBlock xs) -> String (Int -> Header (HardForkBlock xs) -> ShowS) -> (Header (HardForkBlock xs) -> String) -> ([Header (HardForkBlock xs)] -> ShowS) -> Show (Header (HardForkBlock xs)) forall (xs :: [*]). CanHardFork xs => Int -> Header (HardForkBlock xs) -> ShowS forall (xs :: [*]). CanHardFork xs => [Header (HardForkBlock xs)] -> ShowS forall (xs :: [*]). CanHardFork xs => Header (HardForkBlock xs) -> String forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a $cshowsPrec :: forall (xs :: [*]). CanHardFork xs => Int -> Header (HardForkBlock xs) -> ShowS showsPrec :: Int -> Header (HardForkBlock xs) -> ShowS $cshow :: forall (xs :: [*]). CanHardFork xs => Header (HardForkBlock xs) -> String show :: Header (HardForkBlock xs) -> String $cshowList :: forall (xs :: [*]). CanHardFork xs => [Header (HardForkBlock xs)] -> ShowS showList :: [Header (HardForkBlock xs)] -> ShowS Show, Context -> Header (HardForkBlock xs) -> IO (Maybe ThunkInfo) Proxy (Header (HardForkBlock xs)) -> String (Context -> Header (HardForkBlock xs) -> IO (Maybe ThunkInfo)) -> (Context -> Header (HardForkBlock xs) -> IO (Maybe ThunkInfo)) -> (Proxy (Header (HardForkBlock xs)) -> String) -> NoThunks (Header (HardForkBlock xs)) forall (xs :: [*]). CanHardFork xs => Context -> Header (HardForkBlock xs) -> IO (Maybe ThunkInfo) forall (xs :: [*]). CanHardFork xs => Proxy (Header (HardForkBlock xs)) -> String forall a. (Context -> a -> IO (Maybe ThunkInfo)) -> (Context -> a -> IO (Maybe ThunkInfo)) -> (Proxy a -> String) -> NoThunks a $cnoThunks :: forall (xs :: [*]). CanHardFork xs => Context -> Header (HardForkBlock xs) -> IO (Maybe ThunkInfo) noThunks :: Context -> Header (HardForkBlock xs) -> IO (Maybe ThunkInfo) $cwNoThunks :: forall (xs :: [*]). CanHardFork xs => Context -> Header (HardForkBlock xs) -> IO (Maybe ThunkInfo) wNoThunks :: Context -> Header (HardForkBlock xs) -> IO (Maybe ThunkInfo) $cshowTypeOf :: forall (xs :: [*]). CanHardFork xs => Proxy (Header (HardForkBlock xs)) -> String showTypeOf :: Proxy (Header (HardForkBlock xs)) -> String NoThunks) instance Typeable xs => ShowProxy (Header (HardForkBlock xs)) where instance CanHardFork xs => GetHeader (HardForkBlock xs) where getHeader :: HardForkBlock xs -> Header (HardForkBlock xs) getHeader = OneEraHeader xs -> Header (HardForkBlock xs) forall (xs :: [*]). OneEraHeader xs -> Header (HardForkBlock xs) HardForkHeader (OneEraHeader xs -> Header (HardForkBlock xs)) -> (HardForkBlock xs -> OneEraHeader xs) -> HardForkBlock xs -> Header (HardForkBlock xs) forall b c a. (b -> c) -> (a -> b) -> a -> c . OneEraBlock xs -> OneEraHeader xs forall (xs :: [*]). CanHardFork xs => OneEraBlock xs -> OneEraHeader xs oneEraBlockHeader (OneEraBlock xs -> OneEraHeader xs) -> (HardForkBlock xs -> OneEraBlock xs) -> HardForkBlock xs -> OneEraHeader xs forall b c a. (b -> c) -> (a -> b) -> a -> c . HardForkBlock xs -> OneEraBlock xs forall (xs :: [*]). HardForkBlock xs -> OneEraBlock xs getHardForkBlock blockMatchesHeader :: Header (HardForkBlock xs) -> HardForkBlock xs -> Bool blockMatchesHeader = \Header (HardForkBlock xs) hdr HardForkBlock xs blk -> case NS Header xs -> NS I xs -> Either (Mismatch Header I xs) (NS (Product Header I) xs) forall {k} (f :: k -> *) (xs :: [k]) (g :: k -> *). NS f xs -> NS g xs -> Either (Mismatch f g xs) (NS (Product f g) xs) Match.matchNS (OneEraHeader xs -> NS Header xs forall (xs :: [*]). OneEraHeader xs -> NS Header xs getOneEraHeader (Header (HardForkBlock xs) -> OneEraHeader xs forall (xs :: [*]). Header (HardForkBlock xs) -> OneEraHeader xs getHardForkHeader Header (HardForkBlock xs) hdr)) (OneEraBlock xs -> NS I xs forall (xs :: [*]). OneEraBlock xs -> NS I xs getOneEraBlock (HardForkBlock xs -> OneEraBlock xs forall (xs :: [*]). HardForkBlock xs -> OneEraBlock xs getHardForkBlock HardForkBlock xs blk)) of Left Mismatch Header I xs _ -> Bool False Right NS (Product Header I) xs hdrAndBlk -> NS (K Bool) xs -> CollapseTo NS Bool forall (xs :: [*]) a. SListIN NS xs => NS (K a) xs -> CollapseTo NS a forall k l (h :: (k -> *) -> l -> *) (xs :: l) a. (HCollapse h, SListIN h xs) => h (K a) xs -> CollapseTo h a hcollapse (NS (K Bool) xs -> CollapseTo NS Bool) -> NS (K Bool) xs -> CollapseTo NS Bool forall a b. (a -> b) -> a -> b $ Proxy SingleEraBlock -> (forall a. SingleEraBlock a => Product Header I a -> K Bool a) -> NS (Product Header I) xs -> NS (K Bool) xs forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *). (AllN (Prod h) c xs, HAp h) => proxy c -> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs hcliftA Proxy SingleEraBlock proxySingle Product Header I a -> K Bool a forall blk. GetHeader blk => Product Header I blk -> K Bool blk forall a. SingleEraBlock a => Product Header I a -> K Bool a matchesSingle NS (Product Header I) xs hdrAndBlk where matchesSingle :: GetHeader blk => Product Header I blk -> K Bool blk matchesSingle :: forall blk. GetHeader blk => Product Header I blk -> K Bool blk matchesSingle (Pair Header blk hdr (I blk blk)) = Bool -> K Bool blk forall k a (b :: k). a -> K a b K (Header blk -> blk -> Bool forall blk. GetHeader blk => Header blk -> blk -> Bool blockMatchesHeader Header blk hdr blk blk) headerIsEBB :: Header (HardForkBlock xs) -> Maybe EpochNo headerIsEBB = NS (K (Maybe EpochNo)) xs -> Maybe EpochNo NS (K (Maybe EpochNo)) xs -> CollapseTo NS (Maybe EpochNo) forall (xs :: [*]) a. SListIN NS xs => NS (K a) xs -> CollapseTo NS a forall k l (h :: (k -> *) -> l -> *) (xs :: l) a. (HCollapse h, SListIN h xs) => h (K a) xs -> CollapseTo h a hcollapse (NS (K (Maybe EpochNo)) xs -> Maybe EpochNo) -> (Header (HardForkBlock xs) -> NS (K (Maybe EpochNo)) xs) -> Header (HardForkBlock xs) -> Maybe EpochNo forall b c a. (b -> c) -> (a -> b) -> a -> c . Proxy SingleEraBlock -> (forall a. SingleEraBlock a => Header a -> K (Maybe EpochNo) a) -> NS Header xs -> NS (K (Maybe EpochNo)) xs forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *). (AllN (Prod h) c xs, HAp h) => proxy c -> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs hcmap Proxy SingleEraBlock proxySingle (Maybe EpochNo -> K (Maybe EpochNo) a forall k a (b :: k). a -> K a b K (Maybe EpochNo -> K (Maybe EpochNo) a) -> (Header a -> Maybe EpochNo) -> Header a -> K (Maybe EpochNo) a forall b c a. (b -> c) -> (a -> b) -> a -> c . Header a -> Maybe EpochNo forall blk. GetHeader blk => Header blk -> Maybe EpochNo headerIsEBB) (NS Header xs -> NS (K (Maybe EpochNo)) xs) -> (Header (HardForkBlock xs) -> NS Header xs) -> Header (HardForkBlock xs) -> NS (K (Maybe EpochNo)) xs forall b c a. (b -> c) -> (a -> b) -> a -> c . OneEraHeader xs -> NS Header xs forall (xs :: [*]). OneEraHeader xs -> NS Header xs getOneEraHeader (OneEraHeader xs -> NS Header xs) -> (Header (HardForkBlock xs) -> OneEraHeader xs) -> Header (HardForkBlock xs) -> NS Header xs forall b c a. (b -> c) -> (a -> b) -> a -> c . Header (HardForkBlock xs) -> OneEraHeader xs forall (xs :: [*]). Header (HardForkBlock xs) -> OneEraHeader xs getHardForkHeader {------------------------------------------------------------------------------- HasHeader -------------------------------------------------------------------------------} instance CanHardFork xs => StandardHash (HardForkBlock xs) instance CanHardFork xs => HasHeader (HardForkBlock xs) where getHeaderFields :: HardForkBlock xs -> HeaderFields (HardForkBlock xs) getHeaderFields = HardForkBlock xs -> HeaderFields (HardForkBlock xs) forall blk. GetHeader blk => blk -> HeaderFields blk getBlockHeaderFields instance CanHardFork xs => HasHeader (Header (HardForkBlock xs)) where getHeaderFields :: Header (HardForkBlock xs) -> HeaderFields (Header (HardForkBlock xs)) getHeaderFields = NS (K (HeaderFields (Header (HardForkBlock xs)))) xs -> HeaderFields (Header (HardForkBlock xs)) NS (K (HeaderFields (Header (HardForkBlock xs)))) xs -> CollapseTo NS (HeaderFields (Header (HardForkBlock xs))) forall (xs :: [*]) a. SListIN NS xs => NS (K a) xs -> CollapseTo NS a forall k l (h :: (k -> *) -> l -> *) (xs :: l) a. (HCollapse h, SListIN h xs) => h (K a) xs -> CollapseTo h a hcollapse (NS (K (HeaderFields (Header (HardForkBlock xs)))) xs -> HeaderFields (Header (HardForkBlock xs))) -> (Header (HardForkBlock xs) -> NS (K (HeaderFields (Header (HardForkBlock xs)))) xs) -> Header (HardForkBlock xs) -> HeaderFields (Header (HardForkBlock xs)) forall b c a. (b -> c) -> (a -> b) -> a -> c . Proxy SingleEraBlock -> (forall a. SingleEraBlock a => Header a -> K (HeaderFields (Header (HardForkBlock xs))) a) -> NS Header xs -> NS (K (HeaderFields (Header (HardForkBlock xs)))) xs forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *). (AllN (Prod h) c xs, HAp h) => proxy c -> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs hcmap Proxy SingleEraBlock proxySingle (HeaderFields (Header (HardForkBlock xs)) -> K (HeaderFields (Header (HardForkBlock xs))) a forall k a (b :: k). a -> K a b K (HeaderFields (Header (HardForkBlock xs)) -> K (HeaderFields (Header (HardForkBlock xs))) a) -> (Header a -> HeaderFields (Header (HardForkBlock xs))) -> Header a -> K (HeaderFields (Header (HardForkBlock xs))) a forall b c a. (b -> c) -> (a -> b) -> a -> c . Header a -> HeaderFields (Header (HardForkBlock xs)) forall blk. SingleEraBlock blk => Header blk -> HeaderFields (Header (HardForkBlock xs)) getOne) (NS Header xs -> NS (K (HeaderFields (Header (HardForkBlock xs)))) xs) -> (Header (HardForkBlock xs) -> NS Header xs) -> Header (HardForkBlock xs) -> NS (K (HeaderFields (Header (HardForkBlock xs)))) xs forall b c a. (b -> c) -> (a -> b) -> a -> c . OneEraHeader xs -> NS Header xs forall (xs :: [*]). OneEraHeader xs -> NS Header xs getOneEraHeader (OneEraHeader xs -> NS Header xs) -> (Header (HardForkBlock xs) -> OneEraHeader xs) -> Header (HardForkBlock xs) -> NS Header xs forall b c a. (b -> c) -> (a -> b) -> a -> c . Header (HardForkBlock xs) -> OneEraHeader xs forall (xs :: [*]). Header (HardForkBlock xs) -> OneEraHeader xs getHardForkHeader where getOne :: forall blk. SingleEraBlock blk => Header blk -> HeaderFields (Header (HardForkBlock xs)) getOne :: forall blk. SingleEraBlock blk => Header blk -> HeaderFields (Header (HardForkBlock xs)) getOne Header blk hdr = HeaderFields { headerFieldHash :: HeaderHash (Header (HardForkBlock xs)) headerFieldHash = ShortByteString -> OneEraHash xs forall k (xs :: [k]). ShortByteString -> OneEraHash xs OneEraHash (ShortByteString -> OneEraHash xs) -> ShortByteString -> OneEraHash xs forall a b. (a -> b) -> a -> b $ Proxy blk -> HeaderHash blk -> ShortByteString forall blk (proxy :: * -> *). ConvertRawHash blk => proxy blk -> HeaderHash blk -> ShortByteString forall (proxy :: * -> *). proxy blk -> HeaderHash blk -> ShortByteString toShortRawHash (forall t. Proxy t forall {k} (t :: k). Proxy t Proxy @blk) HeaderHash blk HeaderHash (Header blk) headerFieldHash , headerFieldSlot :: SlotNo headerFieldSlot = SlotNo headerFieldSlot , headerFieldBlockNo :: BlockNo headerFieldBlockNo = BlockNo headerFieldBlockNo } where HeaderFields{BlockNo SlotNo HeaderHash (Header blk) headerFieldHash :: forall k (b :: k). HeaderFields b -> HeaderHash b headerFieldHash :: HeaderHash (Header blk) headerFieldSlot :: forall k (b :: k). HeaderFields b -> SlotNo headerFieldSlot :: SlotNo headerFieldBlockNo :: forall k (b :: k). HeaderFields b -> BlockNo headerFieldBlockNo :: BlockNo ..} = Header blk -> HeaderFields (Header blk) forall b. HasHeader b => b -> HeaderFields b getHeaderFields Header blk hdr instance CanHardFork xs => GetPrevHash (HardForkBlock xs) where headerPrevHash :: Header (HardForkBlock xs) -> ChainHash (HardForkBlock xs) headerPrevHash = NS (K (ChainHash (HardForkBlock xs))) xs -> ChainHash (HardForkBlock xs) NS (K (ChainHash (HardForkBlock xs))) xs -> CollapseTo NS (ChainHash (HardForkBlock xs)) forall (xs :: [*]) a. SListIN NS xs => NS (K a) xs -> CollapseTo NS a forall k l (h :: (k -> *) -> l -> *) (xs :: l) a. (HCollapse h, SListIN h xs) => h (K a) xs -> CollapseTo h a hcollapse (NS (K (ChainHash (HardForkBlock xs))) xs -> ChainHash (HardForkBlock xs)) -> (Header (HardForkBlock xs) -> NS (K (ChainHash (HardForkBlock xs))) xs) -> Header (HardForkBlock xs) -> ChainHash (HardForkBlock xs) forall b c a. (b -> c) -> (a -> b) -> a -> c . Proxy SingleEraBlock -> (forall a. SingleEraBlock a => Header a -> K (ChainHash (HardForkBlock xs)) a) -> NS Header xs -> NS (K (ChainHash (HardForkBlock xs))) xs forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *). (AllN (Prod h) c xs, HAp h) => proxy c -> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs hcmap Proxy SingleEraBlock proxySingle (ChainHash (HardForkBlock xs) -> K (ChainHash (HardForkBlock xs)) a forall k a (b :: k). a -> K a b K (ChainHash (HardForkBlock xs) -> K (ChainHash (HardForkBlock xs)) a) -> (Header a -> ChainHash (HardForkBlock xs)) -> Header a -> K (ChainHash (HardForkBlock xs)) a forall b c a. (b -> c) -> (a -> b) -> a -> c . Header a -> ChainHash (HardForkBlock xs) forall blk. SingleEraBlock blk => Header blk -> ChainHash (HardForkBlock xs) getOnePrev) (NS Header xs -> NS (K (ChainHash (HardForkBlock xs))) xs) -> (Header (HardForkBlock xs) -> NS Header xs) -> Header (HardForkBlock xs) -> NS (K (ChainHash (HardForkBlock xs))) xs forall b c a. (b -> c) -> (a -> b) -> a -> c . OneEraHeader xs -> NS Header xs forall (xs :: [*]). OneEraHeader xs -> NS Header xs getOneEraHeader (OneEraHeader xs -> NS Header xs) -> (Header (HardForkBlock xs) -> OneEraHeader xs) -> Header (HardForkBlock xs) -> NS Header xs forall b c a. (b -> c) -> (a -> b) -> a -> c . Header (HardForkBlock xs) -> OneEraHeader xs forall (xs :: [*]). Header (HardForkBlock xs) -> OneEraHeader xs getHardForkHeader where getOnePrev :: forall blk. SingleEraBlock blk => Header blk -> ChainHash (HardForkBlock xs) getOnePrev :: forall blk. SingleEraBlock blk => Header blk -> ChainHash (HardForkBlock xs) getOnePrev Header blk hdr = case Header blk -> ChainHash blk forall blk. GetPrevHash blk => Header blk -> ChainHash blk headerPrevHash Header blk hdr of ChainHash blk GenesisHash -> ChainHash (HardForkBlock xs) forall {k} (b :: k). ChainHash b GenesisHash BlockHash HeaderHash blk h -> HeaderHash (HardForkBlock xs) -> ChainHash (HardForkBlock xs) forall {k} (b :: k). HeaderHash b -> ChainHash b BlockHash (ShortByteString -> OneEraHash xs forall k (xs :: [k]). ShortByteString -> OneEraHash xs OneEraHash (ShortByteString -> OneEraHash xs) -> ShortByteString -> OneEraHash xs forall a b. (a -> b) -> a -> b $ Proxy blk -> HeaderHash blk -> ShortByteString forall blk (proxy :: * -> *). ConvertRawHash blk => proxy blk -> HeaderHash blk -> ShortByteString forall (proxy :: * -> *). proxy blk -> HeaderHash blk -> ShortByteString toShortRawHash (forall t. Proxy t forall {k} (t :: k). Proxy t Proxy @blk) HeaderHash blk h) {------------------------------------------------------------------------------- NestedContent -------------------------------------------------------------------------------} data instance NestedCtxt_ (HardForkBlock xs) :: (Type -> Type) -> (Type -> Type) where NCZ :: !(NestedCtxt_ x f a) -> NestedCtxt_ (HardForkBlock (x ': xs)) f a NCS :: !(NestedCtxt_ (HardForkBlock xs) f a) -> NestedCtxt_ (HardForkBlock (x ': xs)) f a deriving instance All SingleEraBlock xs => Show (NestedCtxt_ (HardForkBlock xs) Header a) instance CanHardFork xs => SameDepIndex (NestedCtxt_ (HardForkBlock xs) Header) where sameDepIndex :: forall a b. NestedCtxt_ (HardForkBlock xs) Header a -> NestedCtxt_ (HardForkBlock xs) Header b -> Maybe (a :~: b) sameDepIndex = NestedCtxt_ (HardForkBlock xs) Header a -> NestedCtxt_ (HardForkBlock xs) Header b -> Maybe (a :~: b) forall (xs' :: [*]) a b. All SingleEraBlock xs' => NestedCtxt_ (HardForkBlock xs') Header a -> NestedCtxt_ (HardForkBlock xs') Header b -> Maybe (a :~: b) go where go :: All SingleEraBlock xs' => NestedCtxt_ (HardForkBlock xs') Header a -> NestedCtxt_ (HardForkBlock xs') Header b -> Maybe (a :~: b) go :: forall (xs' :: [*]) a b. All SingleEraBlock xs' => NestedCtxt_ (HardForkBlock xs') Header a -> NestedCtxt_ (HardForkBlock xs') Header b -> Maybe (a :~: b) go (NCZ NestedCtxt_ x Header a ctxt) (NCZ NestedCtxt_ x Header b ctxt') = NestedCtxt_ x Header a -> NestedCtxt_ x Header b -> Maybe (a :~: b) forall a b. NestedCtxt_ x Header a -> NestedCtxt_ x Header b -> Maybe (a :~: b) forall (f :: * -> *) a b. SameDepIndex f => f a -> f b -> Maybe (a :~: b) sameDepIndex NestedCtxt_ x Header a ctxt NestedCtxt_ x Header b NestedCtxt_ x Header b ctxt' go (NCS NestedCtxt_ (HardForkBlock xs) Header a ctxt) (NCS NestedCtxt_ (HardForkBlock xs) Header b ctxt') = NestedCtxt_ (HardForkBlock xs) Header a -> NestedCtxt_ (HardForkBlock xs) Header b -> Maybe (a :~: b) forall (xs' :: [*]) a b. All SingleEraBlock xs' => NestedCtxt_ (HardForkBlock xs') Header a -> NestedCtxt_ (HardForkBlock xs') Header b -> Maybe (a :~: b) go NestedCtxt_ (HardForkBlock xs) Header a ctxt NestedCtxt_ (HardForkBlock xs) Header b NestedCtxt_ (HardForkBlock xs) Header b ctxt' go NestedCtxt_ (HardForkBlock xs') Header a _ NestedCtxt_ (HardForkBlock xs') Header b _ = Maybe (a :~: b) forall a. Maybe a Nothing instance CanHardFork xs => HasNestedContent Header (HardForkBlock xs) where unnest :: Header (HardForkBlock xs) -> DepPair (NestedCtxt Header (HardForkBlock xs)) unnest = NS Header xs -> DepPair (NestedCtxt Header (HardForkBlock xs)) forall (xs' :: [*]). All SingleEraBlock xs' => NS Header xs' -> DepPair (NestedCtxt Header (HardForkBlock xs')) go (NS Header xs -> DepPair (NestedCtxt Header (HardForkBlock xs))) -> (Header (HardForkBlock xs) -> NS Header xs) -> Header (HardForkBlock xs) -> DepPair (NestedCtxt Header (HardForkBlock xs)) forall b c a. (b -> c) -> (a -> b) -> a -> c . OneEraHeader xs -> NS Header xs forall (xs :: [*]). OneEraHeader xs -> NS Header xs getOneEraHeader (OneEraHeader xs -> NS Header xs) -> (Header (HardForkBlock xs) -> OneEraHeader xs) -> Header (HardForkBlock xs) -> NS Header xs forall b c a. (b -> c) -> (a -> b) -> a -> c . Header (HardForkBlock xs) -> OneEraHeader xs forall (xs :: [*]). Header (HardForkBlock xs) -> OneEraHeader xs getHardForkHeader where go :: All SingleEraBlock xs' => NS Header xs' -> DepPair (NestedCtxt Header (HardForkBlock xs')) go :: forall (xs' :: [*]). All SingleEraBlock xs' => NS Header xs' -> DepPair (NestedCtxt Header (HardForkBlock xs')) go (Z Header x x) = case Header x -> DepPair (NestedCtxt Header x) forall (f :: * -> *) blk. HasNestedContent f blk => f blk -> DepPair (NestedCtxt f blk) unnest Header x x of DepPair (NestedCtxt NestedCtxt_ x Header a ctxt) a x' -> NestedCtxt Header (HardForkBlock xs') a -> a -> DepPair (NestedCtxt Header (HardForkBlock xs')) forall (f :: * -> *) a. f a -> a -> DepPair f DepPair (NestedCtxt_ (HardForkBlock xs') Header a -> NestedCtxt Header (HardForkBlock xs') a forall (f :: * -> *) blk a. NestedCtxt_ blk f a -> NestedCtxt f blk a NestedCtxt (NestedCtxt_ x Header a -> NestedCtxt_ (HardForkBlock (x : xs1)) Header a forall xs (f :: * -> *) a (x :: [*]). NestedCtxt_ xs f a -> NestedCtxt_ (HardForkBlock (xs : x)) f a NCZ NestedCtxt_ x Header a ctxt)) a x' go (S NS Header xs1 x) = case NS Header xs1 -> DepPair (NestedCtxt Header (HardForkBlock xs1)) forall (xs' :: [*]). All SingleEraBlock xs' => NS Header xs' -> DepPair (NestedCtxt Header (HardForkBlock xs')) go NS Header xs1 x of DepPair (NestedCtxt NestedCtxt_ (HardForkBlock xs1) Header a ctxt) a x' -> NestedCtxt Header (HardForkBlock xs') a -> a -> DepPair (NestedCtxt Header (HardForkBlock xs')) forall (f :: * -> *) a. f a -> a -> DepPair f DepPair (NestedCtxt_ (HardForkBlock xs') Header a -> NestedCtxt Header (HardForkBlock xs') a forall (f :: * -> *) blk a. NestedCtxt_ blk f a -> NestedCtxt f blk a NestedCtxt (NestedCtxt_ (HardForkBlock xs1) Header a -> NestedCtxt_ (HardForkBlock (x : xs1)) Header a forall (xs :: [*]) (f :: * -> *) a x. NestedCtxt_ (HardForkBlock xs) f a -> NestedCtxt_ (HardForkBlock (x : xs)) f a NCS NestedCtxt_ (HardForkBlock xs1) Header a ctxt)) a x' nest :: DepPair (NestedCtxt Header (HardForkBlock xs)) -> Header (HardForkBlock xs) nest = \(DepPair NestedCtxt Header (HardForkBlock xs) a ctxt a hdr) -> OneEraHeader xs -> Header (HardForkBlock xs) forall (xs :: [*]). OneEraHeader xs -> Header (HardForkBlock xs) HardForkHeader (OneEraHeader xs -> Header (HardForkBlock xs)) -> (NS Header xs -> OneEraHeader xs) -> NS Header xs -> Header (HardForkBlock xs) forall b c a. (b -> c) -> (a -> b) -> a -> c . NS Header xs -> OneEraHeader xs forall (xs :: [*]). NS Header xs -> OneEraHeader xs OneEraHeader (NS Header xs -> Header (HardForkBlock xs)) -> NS Header xs -> Header (HardForkBlock xs) forall a b. (a -> b) -> a -> b $ NestedCtxt Header (HardForkBlock xs) a -> a -> NS Header xs forall (xs' :: [*]) a. All SingleEraBlock xs' => NestedCtxt Header (HardForkBlock xs') a -> a -> NS Header xs' go NestedCtxt Header (HardForkBlock xs) a ctxt a hdr where go :: All SingleEraBlock xs' => NestedCtxt Header (HardForkBlock xs') a -> a -> NS Header xs' go :: forall (xs' :: [*]) a. All SingleEraBlock xs' => NestedCtxt Header (HardForkBlock xs') a -> a -> NS Header xs' go (NestedCtxt (NCZ NestedCtxt_ x Header a ctxt)) a x = Header x -> NS Header (x : xs) forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]). f x -> NS f (x : xs1) Z (DepPair (NestedCtxt Header x) -> Header x forall (f :: * -> *) blk. HasNestedContent f blk => DepPair (NestedCtxt f blk) -> f blk nest (NestedCtxt Header x a -> a -> DepPair (NestedCtxt Header x) forall (f :: * -> *) a. f a -> a -> DepPair f DepPair (NestedCtxt_ x Header a -> NestedCtxt Header x a forall (f :: * -> *) blk a. NestedCtxt_ blk f a -> NestedCtxt f blk a NestedCtxt NestedCtxt_ x Header a ctxt) a x)) go (NestedCtxt (NCS NestedCtxt_ (HardForkBlock xs) Header a ctxt)) a x = NS Header xs -> NS Header (x : xs) forall {k} (f :: k -> *) (xs1 :: [k]) (x :: k). NS f xs1 -> NS f (x : xs1) S (NestedCtxt Header (HardForkBlock xs) a -> a -> NS Header xs forall (xs' :: [*]) a. All SingleEraBlock xs' => NestedCtxt Header (HardForkBlock xs') a -> a -> NS Header xs' go (NestedCtxt_ (HardForkBlock xs) Header a -> NestedCtxt Header (HardForkBlock xs) a forall (f :: * -> *) blk a. NestedCtxt_ blk f a -> NestedCtxt f blk a NestedCtxt NestedCtxt_ (HardForkBlock xs) Header a ctxt) a x) {------------------------------------------------------------------------------- ConvertRawHash -------------------------------------------------------------------------------} instance CanHardFork xs => ConvertRawHash (HardForkBlock xs) where toShortRawHash :: forall (proxy :: * -> *). proxy (HardForkBlock xs) -> HeaderHash (HardForkBlock xs) -> ShortByteString toShortRawHash proxy (HardForkBlock xs) _ = HeaderHash (HardForkBlock xs) -> ShortByteString OneEraHash xs -> ShortByteString forall k (xs :: [k]). OneEraHash xs -> ShortByteString getOneEraHash fromShortRawHash :: forall (proxy :: * -> *). proxy (HardForkBlock xs) -> ShortByteString -> HeaderHash (HardForkBlock xs) fromShortRawHash proxy (HardForkBlock xs) _ = ShortByteString -> HeaderHash (HardForkBlock xs) ShortByteString -> OneEraHash xs forall k (xs :: [k]). ShortByteString -> OneEraHash xs OneEraHash hashSize :: forall (proxy :: * -> *). proxy (HardForkBlock xs) -> Word32 hashSize proxy (HardForkBlock xs) _ = NP (K Word32) xs -> Word32 forall {k} (xs :: [k]) a. (IsNonEmpty xs, Eq a, SListI xs, HasCallStack) => NP (K a) xs -> a getSameValue NP (K Word32) xs hashSizes where hashSizes :: NP (K Word32) xs hashSizes :: NP (K Word32) xs hashSizes = Proxy SingleEraBlock -> (forall a. SingleEraBlock a => K Word32 a) -> NP (K Word32) xs forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *). (HPure h, AllN h c xs) => proxy c -> (forall (a :: k). c a => f a) -> h f xs forall (c :: * -> Constraint) (xs :: [*]) (proxy :: (* -> Constraint) -> *) (f :: * -> *). AllN NP c xs => proxy c -> (forall a. c a => f a) -> NP f xs hcpure Proxy SingleEraBlock proxySingle K Word32 a forall a. SingleEraBlock a => K Word32 a hashSizeOne hashSizeOne :: forall blk. SingleEraBlock blk => K Word32 blk hashSizeOne :: forall a. SingleEraBlock a => K Word32 a hashSizeOne = Word32 -> K Word32 blk forall k a (b :: k). a -> K a b K (Word32 -> K Word32 blk) -> Word32 -> K Word32 blk forall a b. (a -> b) -> a -> b $ Proxy blk -> Word32 forall blk (proxy :: * -> *). ConvertRawHash blk => proxy blk -> Word32 forall (proxy :: * -> *). proxy blk -> Word32 hashSize (forall t. Proxy t forall {k} (t :: k). Proxy t Proxy @blk) {------------------------------------------------------------------------------- HasAnnTip -------------------------------------------------------------------------------} instance CanHardFork xs => HasAnnTip (HardForkBlock xs) where type TipInfo (HardForkBlock xs) = OneEraTipInfo xs getTipInfo :: Header (HardForkBlock xs) -> TipInfo (HardForkBlock xs) getTipInfo = NS WrapTipInfo xs -> OneEraTipInfo xs forall (xs :: [*]). NS WrapTipInfo xs -> OneEraTipInfo xs OneEraTipInfo (NS WrapTipInfo xs -> OneEraTipInfo xs) -> (Header (HardForkBlock xs) -> NS WrapTipInfo xs) -> Header (HardForkBlock xs) -> OneEraTipInfo xs forall b c a. (b -> c) -> (a -> b) -> a -> c . Proxy SingleEraBlock -> (forall a. SingleEraBlock a => Header a -> WrapTipInfo a) -> NS Header xs -> NS WrapTipInfo xs forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *). (AllN (Prod h) c xs, HAp h) => proxy c -> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs hcmap Proxy SingleEraBlock proxySingle (TipInfo a -> WrapTipInfo a forall blk. TipInfo blk -> WrapTipInfo blk WrapTipInfo (TipInfo a -> WrapTipInfo a) -> (Header a -> TipInfo a) -> Header a -> WrapTipInfo a forall b c a. (b -> c) -> (a -> b) -> a -> c . Header a -> TipInfo a forall blk. HasAnnTip blk => Header blk -> TipInfo blk getTipInfo) (NS Header xs -> NS WrapTipInfo xs) -> (Header (HardForkBlock xs) -> NS Header xs) -> Header (HardForkBlock xs) -> NS WrapTipInfo xs forall b c a. (b -> c) -> (a -> b) -> a -> c . OneEraHeader xs -> NS Header xs forall (xs :: [*]). OneEraHeader xs -> NS Header xs getOneEraHeader (OneEraHeader xs -> NS Header xs) -> (Header (HardForkBlock xs) -> OneEraHeader xs) -> Header (HardForkBlock xs) -> NS Header xs forall b c a. (b -> c) -> (a -> b) -> a -> c . Header (HardForkBlock xs) -> OneEraHeader xs forall (xs :: [*]). Header (HardForkBlock xs) -> OneEraHeader xs getHardForkHeader tipInfoHash :: forall (proxy :: * -> *). proxy (HardForkBlock xs) -> TipInfo (HardForkBlock xs) -> HeaderHash (HardForkBlock xs) tipInfoHash proxy (HardForkBlock xs) _ = NS (K (OneEraHash xs)) xs -> CollapseTo NS (OneEraHash xs) NS (K (OneEraHash xs)) xs -> OneEraHash xs forall (xs :: [*]) a. SListIN NS xs => NS (K a) xs -> CollapseTo NS a forall k l (h :: (k -> *) -> l -> *) (xs :: l) a. (HCollapse h, SListIN h xs) => h (K a) xs -> CollapseTo h a hcollapse (NS (K (OneEraHash xs)) xs -> OneEraHash xs) -> (OneEraTipInfo xs -> NS (K (OneEraHash xs)) xs) -> OneEraTipInfo xs -> OneEraHash xs forall b c a. (b -> c) -> (a -> b) -> a -> c . Proxy SingleEraBlock -> (forall a. SingleEraBlock a => WrapTipInfo a -> K (OneEraHash xs) a) -> NS WrapTipInfo xs -> NS (K (OneEraHash xs)) xs forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *). (AllN (Prod h) c xs, HAp h) => proxy c -> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs hcmap Proxy SingleEraBlock proxySingle (OneEraHash xs -> K (OneEraHash xs) a forall k a (b :: k). a -> K a b K (OneEraHash xs -> K (OneEraHash xs) a) -> (WrapTipInfo a -> OneEraHash xs) -> WrapTipInfo a -> K (OneEraHash xs) a forall b c a. (b -> c) -> (a -> b) -> a -> c . WrapTipInfo a -> OneEraHash xs forall blk. SingleEraBlock blk => WrapTipInfo blk -> OneEraHash xs tipInfoOne) (NS WrapTipInfo xs -> NS (K (OneEraHash xs)) xs) -> (OneEraTipInfo xs -> NS WrapTipInfo xs) -> OneEraTipInfo xs -> NS (K (OneEraHash xs)) xs forall b c a. (b -> c) -> (a -> b) -> a -> c . OneEraTipInfo xs -> NS WrapTipInfo xs forall (xs :: [*]). OneEraTipInfo xs -> NS WrapTipInfo xs getOneEraTipInfo where tipInfoOne :: forall blk. SingleEraBlock blk => WrapTipInfo blk -> OneEraHash xs tipInfoOne :: forall blk. SingleEraBlock blk => WrapTipInfo blk -> OneEraHash xs tipInfoOne = ShortByteString -> OneEraHash xs forall k (xs :: [k]). ShortByteString -> OneEraHash xs OneEraHash (ShortByteString -> OneEraHash xs) -> (WrapTipInfo blk -> ShortByteString) -> WrapTipInfo blk -> OneEraHash xs forall b c a. (b -> c) -> (a -> b) -> a -> c . Proxy blk -> HeaderHash blk -> ShortByteString forall blk (proxy :: * -> *). ConvertRawHash blk => proxy blk -> HeaderHash blk -> ShortByteString forall (proxy :: * -> *). proxy blk -> HeaderHash blk -> ShortByteString toShortRawHash (forall t. Proxy t forall {k} (t :: k). Proxy t Proxy @blk) (HeaderHash blk -> ShortByteString) -> (WrapTipInfo blk -> HeaderHash blk) -> WrapTipInfo blk -> ShortByteString forall b c a. (b -> c) -> (a -> b) -> a -> c . Proxy blk -> TipInfo blk -> HeaderHash blk forall blk (proxy :: * -> *). HasAnnTip blk => proxy blk -> TipInfo blk -> HeaderHash blk forall (proxy :: * -> *). proxy blk -> TipInfo blk -> HeaderHash blk tipInfoHash (forall t. Proxy t forall {k} (t :: k). Proxy t Proxy @blk) (TipInfo blk -> HeaderHash blk) -> (WrapTipInfo blk -> TipInfo blk) -> WrapTipInfo blk -> HeaderHash blk forall b c a. (b -> c) -> (a -> b) -> a -> c . WrapTipInfo blk -> TipInfo blk forall blk. WrapTipInfo blk -> TipInfo blk unwrapTipInfo distribAnnTip :: SListI xs => AnnTip (HardForkBlock xs) -> NS AnnTip xs distribAnnTip :: forall (xs :: [*]). SListI xs => AnnTip (HardForkBlock xs) -> NS AnnTip xs distribAnnTip AnnTip{BlockNo SlotNo TipInfo (HardForkBlock xs) annTipSlotNo :: SlotNo annTipBlockNo :: BlockNo annTipInfo :: TipInfo (HardForkBlock xs) annTipSlotNo :: forall blk. AnnTip blk -> SlotNo annTipBlockNo :: forall blk. AnnTip blk -> BlockNo annTipInfo :: forall blk. AnnTip blk -> TipInfo blk ..} = (forall a. WrapTipInfo a -> AnnTip a) -> NS WrapTipInfo xs -> NS AnnTip 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 WrapTipInfo a -> AnnTip a forall a. WrapTipInfo a -> AnnTip a distrib (OneEraTipInfo xs -> NS WrapTipInfo xs forall (xs :: [*]). OneEraTipInfo xs -> NS WrapTipInfo xs getOneEraTipInfo TipInfo (HardForkBlock xs) OneEraTipInfo xs annTipInfo) where distrib :: WrapTipInfo blk -> AnnTip blk distrib :: forall a. WrapTipInfo a -> AnnTip a distrib (WrapTipInfo TipInfo blk info) = SlotNo -> BlockNo -> TipInfo blk -> AnnTip blk forall blk. SlotNo -> BlockNo -> TipInfo blk -> AnnTip blk AnnTip SlotNo annTipSlotNo BlockNo annTipBlockNo TipInfo blk info undistribAnnTip :: SListI xs => NS AnnTip xs -> AnnTip (HardForkBlock xs) undistribAnnTip :: forall (xs :: [*]). SListI xs => NS AnnTip xs -> AnnTip (HardForkBlock xs) undistribAnnTip = NS (K (AnnTip (HardForkBlock xs))) xs -> CollapseTo NS (AnnTip (HardForkBlock xs)) NS (K (AnnTip (HardForkBlock xs))) xs -> AnnTip (HardForkBlock xs) forall (xs :: [*]) a. SListIN NS xs => NS (K a) xs -> CollapseTo NS a forall k l (h :: (k -> *) -> l -> *) (xs :: l) a. (HCollapse h, SListIN h xs) => h (K a) xs -> CollapseTo h a hcollapse (NS (K (AnnTip (HardForkBlock xs))) xs -> AnnTip (HardForkBlock xs)) -> (NS AnnTip xs -> NS (K (AnnTip (HardForkBlock xs))) xs) -> NS AnnTip xs -> AnnTip (HardForkBlock xs) forall b c a. (b -> c) -> (a -> b) -> a -> c . (forall a. Index xs a -> AnnTip a -> K (AnnTip (HardForkBlock xs)) a) -> NS AnnTip xs -> NS (K (AnnTip (HardForkBlock xs))) xs forall {k} (h :: (k -> *) -> [k] -> *) (xs :: [k]) (f1 :: k -> *) (f2 :: k -> *). (HAp h, SListI xs, Prod h ~ NP) => (forall (a :: k). Index xs a -> f1 a -> f2 a) -> h f1 xs -> h f2 xs himap Index xs a -> AnnTip a -> K (AnnTip (HardForkBlock xs)) a forall (xs :: [*]) blk. Index xs blk -> AnnTip blk -> K (AnnTip (HardForkBlock xs)) blk forall a. Index xs a -> AnnTip a -> K (AnnTip (HardForkBlock xs)) a undistrib where undistrib :: Index xs blk -> AnnTip blk -> K (AnnTip (HardForkBlock xs)) blk undistrib :: forall (xs :: [*]) blk. Index xs blk -> AnnTip blk -> K (AnnTip (HardForkBlock xs)) blk undistrib Index xs blk index AnnTip{BlockNo SlotNo TipInfo blk annTipSlotNo :: forall blk. AnnTip blk -> SlotNo annTipBlockNo :: forall blk. AnnTip blk -> BlockNo annTipInfo :: forall blk. AnnTip blk -> TipInfo blk annTipSlotNo :: SlotNo annTipBlockNo :: BlockNo annTipInfo :: TipInfo blk ..} = AnnTip (HardForkBlock xs) -> K (AnnTip (HardForkBlock xs)) blk forall k a (b :: k). a -> K a b K (AnnTip (HardForkBlock xs) -> K (AnnTip (HardForkBlock xs)) blk) -> AnnTip (HardForkBlock xs) -> K (AnnTip (HardForkBlock xs)) blk forall a b. (a -> b) -> a -> b $ SlotNo -> BlockNo -> TipInfo (HardForkBlock xs) -> AnnTip (HardForkBlock xs) forall blk. SlotNo -> BlockNo -> TipInfo blk -> AnnTip blk AnnTip SlotNo annTipSlotNo BlockNo annTipBlockNo (NS WrapTipInfo xs -> TipInfo (HardForkBlock xs) NS WrapTipInfo xs -> OneEraTipInfo xs forall (xs :: [*]). NS WrapTipInfo xs -> OneEraTipInfo xs OneEraTipInfo (NS WrapTipInfo xs -> TipInfo (HardForkBlock xs)) -> (TipInfo blk -> NS WrapTipInfo xs) -> TipInfo blk -> TipInfo (HardForkBlock xs) forall b c a. (b -> c) -> (a -> b) -> a -> c . Index xs blk -> WrapTipInfo blk -> NS WrapTipInfo xs forall {k} (f :: k -> *) (x :: k) (xs :: [k]). Index xs x -> f x -> NS f xs injectNS Index xs blk index (WrapTipInfo blk -> NS WrapTipInfo xs) -> (TipInfo blk -> WrapTipInfo blk) -> TipInfo blk -> NS WrapTipInfo xs forall b c a. (b -> c) -> (a -> b) -> a -> c . TipInfo blk -> WrapTipInfo blk forall blk. TipInfo blk -> WrapTipInfo blk WrapTipInfo (TipInfo blk -> TipInfo (HardForkBlock xs)) -> TipInfo blk -> TipInfo (HardForkBlock xs) forall a b. (a -> b) -> a -> b $ TipInfo blk annTipInfo) {------------------------------------------------------------------------------- BasicEnvelopeValidation -------------------------------------------------------------------------------} instance CanHardFork xs => BasicEnvelopeValidation (HardForkBlock xs) where expectedFirstBlockNo :: forall (proxy :: * -> *). proxy (HardForkBlock xs) -> BlockNo expectedFirstBlockNo proxy (HardForkBlock xs) _ = case Proxy xs -> ProofNonEmpty xs forall {a} (xs :: [a]) (proxy :: [a] -> *). IsNonEmpty xs => proxy xs -> ProofNonEmpty xs forall (proxy :: [*] -> *). proxy xs -> ProofNonEmpty xs isNonEmpty (forall (t :: [*]). Proxy t forall {k} (t :: k). Proxy t Proxy @xs) of ProofNonEmpty Proxy x p Proxy xs1 _ -> Proxy x -> BlockNo forall blk (proxy :: * -> *). BasicEnvelopeValidation blk => proxy blk -> BlockNo forall (proxy :: * -> *). proxy x -> BlockNo expectedFirstBlockNo Proxy x p minimumPossibleSlotNo :: Proxy (HardForkBlock xs) -> SlotNo minimumPossibleSlotNo Proxy (HardForkBlock xs) _ = case Proxy xs -> ProofNonEmpty xs forall {a} (xs :: [a]) (proxy :: [a] -> *). IsNonEmpty xs => proxy xs -> ProofNonEmpty xs forall (proxy :: [*] -> *). proxy xs -> ProofNonEmpty xs isNonEmpty (forall (t :: [*]). Proxy t forall {k} (t :: k). Proxy t Proxy @xs) of ProofNonEmpty Proxy x p Proxy xs1 _ -> Proxy x -> SlotNo forall blk. BasicEnvelopeValidation blk => Proxy blk -> SlotNo minimumPossibleSlotNo Proxy x p -- TODO: If the block is from a different era as the current tip, we just -- expect @succ b@. This may not be sufficient: if we ever transition /to/ -- an era with EBBs, this is not correct. expectedNextBlockNo :: forall (proxy :: * -> *). proxy (HardForkBlock xs) -> TipInfo (HardForkBlock xs) -> TipInfo (HardForkBlock xs) -> BlockNo -> BlockNo expectedNextBlockNo proxy (HardForkBlock xs) _ (OneEraTipInfo NS WrapTipInfo xs oldTip) (OneEraTipInfo NS WrapTipInfo xs newBlock) BlockNo b = case NS WrapTipInfo xs -> NS WrapTipInfo xs -> Either (Mismatch WrapTipInfo WrapTipInfo xs) (NS (Product WrapTipInfo WrapTipInfo) xs) forall {k} (f :: k -> *) (xs :: [k]) (g :: k -> *). NS f xs -> NS g xs -> Either (Mismatch f g xs) (NS (Product f g) xs) Match.matchNS NS WrapTipInfo xs oldTip NS WrapTipInfo xs newBlock of Right NS (Product WrapTipInfo WrapTipInfo) xs matched -> NS (K BlockNo) xs -> CollapseTo NS BlockNo forall (xs :: [*]) a. SListIN NS xs => NS (K a) xs -> CollapseTo NS a forall k l (h :: (k -> *) -> l -> *) (xs :: l) a. (HCollapse h, SListIN h xs) => h (K a) xs -> CollapseTo h a hcollapse (NS (K BlockNo) xs -> CollapseTo NS BlockNo) -> NS (K BlockNo) xs -> CollapseTo NS BlockNo forall a b. (a -> b) -> a -> b $ Proxy SingleEraBlock -> (forall a. SingleEraBlock a => Product WrapTipInfo WrapTipInfo a -> K BlockNo a) -> NS (Product WrapTipInfo WrapTipInfo) xs -> NS (K BlockNo) xs forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *). (AllN (Prod h) c xs, HAp h) => proxy c -> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs hcmap Proxy SingleEraBlock proxySingle Product WrapTipInfo WrapTipInfo a -> K BlockNo a forall a. SingleEraBlock a => Product WrapTipInfo WrapTipInfo a -> K BlockNo a aux NS (Product WrapTipInfo WrapTipInfo) xs matched Left Mismatch WrapTipInfo WrapTipInfo xs _mismatch -> BlockNo -> BlockNo forall a. Enum a => a -> a succ BlockNo b where aux :: forall blk. SingleEraBlock blk => Product WrapTipInfo WrapTipInfo blk -> K BlockNo blk aux :: forall a. SingleEraBlock a => Product WrapTipInfo WrapTipInfo a -> K BlockNo a aux (Pair (WrapTipInfo TipInfo blk old) (WrapTipInfo TipInfo blk new)) = BlockNo -> K BlockNo blk forall k a (b :: k). a -> K a b K (BlockNo -> K BlockNo blk) -> BlockNo -> K BlockNo blk forall a b. (a -> b) -> a -> b $ Proxy blk -> TipInfo blk -> TipInfo blk -> BlockNo -> BlockNo forall blk (proxy :: * -> *). BasicEnvelopeValidation blk => proxy blk -> TipInfo blk -> TipInfo blk -> BlockNo -> BlockNo forall (proxy :: * -> *). proxy blk -> TipInfo blk -> TipInfo blk -> BlockNo -> BlockNo expectedNextBlockNo (forall t. Proxy t forall {k} (t :: k). Proxy t Proxy @blk) TipInfo blk old TipInfo blk new BlockNo b -- TODO: If the block is from a different era as the current tip, we just -- expect @succ s@. This may not be sufficient: if we ever transition /to/ -- an era with EBBs, this is not correct. minimumNextSlotNo :: forall (proxy :: * -> *). proxy (HardForkBlock xs) -> TipInfo (HardForkBlock xs) -> TipInfo (HardForkBlock xs) -> SlotNo -> SlotNo minimumNextSlotNo proxy (HardForkBlock xs) _ (OneEraTipInfo NS WrapTipInfo xs oldTip) (OneEraTipInfo NS WrapTipInfo xs newBlock) SlotNo s = case NS WrapTipInfo xs -> NS WrapTipInfo xs -> Either (Mismatch WrapTipInfo WrapTipInfo xs) (NS (Product WrapTipInfo WrapTipInfo) xs) forall {k} (f :: k -> *) (xs :: [k]) (g :: k -> *). NS f xs -> NS g xs -> Either (Mismatch f g xs) (NS (Product f g) xs) Match.matchNS NS WrapTipInfo xs oldTip NS WrapTipInfo xs newBlock of Right NS (Product WrapTipInfo WrapTipInfo) xs matched -> NS (K SlotNo) xs -> CollapseTo NS SlotNo forall (xs :: [*]) a. SListIN NS xs => NS (K a) xs -> CollapseTo NS a forall k l (h :: (k -> *) -> l -> *) (xs :: l) a. (HCollapse h, SListIN h xs) => h (K a) xs -> CollapseTo h a hcollapse (NS (K SlotNo) xs -> CollapseTo NS SlotNo) -> NS (K SlotNo) xs -> CollapseTo NS SlotNo forall a b. (a -> b) -> a -> b $ Proxy SingleEraBlock -> (forall a. SingleEraBlock a => Product WrapTipInfo WrapTipInfo a -> K SlotNo a) -> NS (Product WrapTipInfo WrapTipInfo) xs -> NS (K SlotNo) xs forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *). (AllN (Prod h) c xs, HAp h) => proxy c -> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs hcmap Proxy SingleEraBlock proxySingle Product WrapTipInfo WrapTipInfo a -> K SlotNo a forall a. SingleEraBlock a => Product WrapTipInfo WrapTipInfo a -> K SlotNo a aux NS (Product WrapTipInfo WrapTipInfo) xs matched Left Mismatch WrapTipInfo WrapTipInfo xs _mismatch -> SlotNo -> SlotNo forall a. Enum a => a -> a succ SlotNo s where aux :: forall blk. SingleEraBlock blk => Product WrapTipInfo WrapTipInfo blk -> K SlotNo blk aux :: forall a. SingleEraBlock a => Product WrapTipInfo WrapTipInfo a -> K SlotNo a aux (Pair (WrapTipInfo TipInfo blk old) (WrapTipInfo TipInfo blk new)) = SlotNo -> K SlotNo blk forall k a (b :: k). a -> K a b K (SlotNo -> K SlotNo blk) -> SlotNo -> K SlotNo blk forall a b. (a -> b) -> a -> b $ Proxy blk -> TipInfo blk -> TipInfo blk -> SlotNo -> SlotNo forall blk (proxy :: * -> *). BasicEnvelopeValidation blk => proxy blk -> TipInfo blk -> TipInfo blk -> SlotNo -> SlotNo forall (proxy :: * -> *). proxy blk -> TipInfo blk -> TipInfo blk -> SlotNo -> SlotNo minimumNextSlotNo (forall t. Proxy t forall {k} (t :: k). Proxy t Proxy @blk) TipInfo blk old TipInfo blk new SlotNo s {------------------------------------------------------------------------------- Other instances (primarily for the benefit of tests) -------------------------------------------------------------------------------} instance All Eq xs => Eq (HardForkBlock xs) where == :: HardForkBlock xs -> HardForkBlock xs -> Bool (==) = (Either (Mismatch I I xs) (NS (Product I I) xs) -> Bool aux (Either (Mismatch I I xs) (NS (Product I I) xs) -> Bool) -> (NS I xs -> NS I xs -> Either (Mismatch I I xs) (NS (Product I I) xs)) -> NS I xs -> NS I xs -> Bool forall y z x0 x1. (y -> z) -> (x0 -> x1 -> y) -> x0 -> x1 -> z .: NS I xs -> NS I xs -> Either (Mismatch I I xs) (NS (Product I I) xs) forall {k} (f :: k -> *) (xs :: [k]) (g :: k -> *). NS f xs -> NS g xs -> Either (Mismatch f g xs) (NS (Product f g) xs) Match.matchNS) (NS I xs -> NS I xs -> Bool) -> (HardForkBlock xs -> NS I xs) -> HardForkBlock xs -> HardForkBlock xs -> Bool forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c `on` (OneEraBlock xs -> NS I xs forall (xs :: [*]). OneEraBlock xs -> NS I xs getOneEraBlock (OneEraBlock xs -> NS I xs) -> (HardForkBlock xs -> OneEraBlock xs) -> HardForkBlock xs -> NS I xs forall b c a. (b -> c) -> (a -> b) -> a -> c . HardForkBlock xs -> OneEraBlock xs forall (xs :: [*]). HardForkBlock xs -> OneEraBlock xs getHardForkBlock) where aux :: Either (Match.Mismatch I I xs) (NS (Product I I) xs) -> Bool aux :: Either (Mismatch I I xs) (NS (Product I I) xs) -> Bool aux (Left Mismatch I I xs _) = Bool False aux (Right NS (Product I I) xs m) = NS (K Bool) xs -> CollapseTo NS Bool forall (xs :: [*]) a. SListIN NS xs => NS (K a) xs -> CollapseTo NS a forall k l (h :: (k -> *) -> l -> *) (xs :: l) a. (HCollapse h, SListIN h xs) => h (K a) xs -> CollapseTo h a hcollapse (NS (K Bool) xs -> CollapseTo NS Bool) -> NS (K Bool) xs -> CollapseTo NS Bool forall a b. (a -> b) -> a -> b $ Proxy Eq -> (forall a. Eq a => Product I I a -> K Bool a) -> NS (Product I I) xs -> NS (K Bool) xs forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *). (AllN (Prod h) c xs, HAp h) => proxy c -> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs hcmap (forall {k} (t :: k). Proxy t forall (t :: * -> Constraint). Proxy t Proxy @Eq) (\(Pair I a x I a y) -> Bool -> K Bool a forall k a (b :: k). a -> K a b K (Bool -> K Bool a) -> Bool -> K Bool a forall a b. (a -> b) -> a -> b $ I a x I a -> I a -> Bool forall a. Eq a => a -> a -> Bool == I a y) NS (Product I I) xs m instance All (Compose Eq Header) xs => Eq (Header (HardForkBlock xs)) where == :: Header (HardForkBlock xs) -> Header (HardForkBlock xs) -> Bool (==) = (Either (Mismatch Header Header xs) (NS (Product Header Header) xs) -> Bool aux (Either (Mismatch Header Header xs) (NS (Product Header Header) xs) -> Bool) -> (NS Header xs -> NS Header xs -> Either (Mismatch Header Header xs) (NS (Product Header Header) xs)) -> NS Header xs -> NS Header xs -> Bool forall y z x0 x1. (y -> z) -> (x0 -> x1 -> y) -> x0 -> x1 -> z .: NS Header xs -> NS Header xs -> Either (Mismatch Header Header xs) (NS (Product Header Header) xs) forall {k} (f :: k -> *) (xs :: [k]) (g :: k -> *). NS f xs -> NS g xs -> Either (Mismatch f g xs) (NS (Product f g) xs) Match.matchNS) (NS Header xs -> NS Header xs -> Bool) -> (Header (HardForkBlock xs) -> NS Header xs) -> Header (HardForkBlock xs) -> Header (HardForkBlock xs) -> Bool forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c `on` (OneEraHeader xs -> NS Header xs forall (xs :: [*]). OneEraHeader xs -> NS Header xs getOneEraHeader (OneEraHeader xs -> NS Header xs) -> (Header (HardForkBlock xs) -> OneEraHeader xs) -> Header (HardForkBlock xs) -> NS Header xs forall b c a. (b -> c) -> (a -> b) -> a -> c . Header (HardForkBlock xs) -> OneEraHeader xs forall (xs :: [*]). Header (HardForkBlock xs) -> OneEraHeader xs getHardForkHeader) where aux :: Either (Match.Mismatch Header Header xs) (NS (Product Header Header) xs) -> Bool aux :: Either (Mismatch Header Header xs) (NS (Product Header Header) xs) -> Bool aux (Left Mismatch Header Header xs _) = Bool False aux (Right NS (Product Header Header) xs m) = NS (K Bool) xs -> CollapseTo NS Bool forall (xs :: [*]) a. SListIN NS xs => NS (K a) xs -> CollapseTo NS a forall k l (h :: (k -> *) -> l -> *) (xs :: l) a. (HCollapse h, SListIN h xs) => h (K a) xs -> CollapseTo h a hcollapse (NS (K Bool) xs -> CollapseTo NS Bool) -> NS (K Bool) xs -> CollapseTo NS Bool forall a b. (a -> b) -> a -> b $ Proxy (Compose Eq Header) -> (forall a. Compose Eq Header a => Product Header Header a -> K Bool a) -> NS (Product Header Header) xs -> NS (K Bool) xs forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *). (AllN (Prod h) c xs, HAp h) => proxy c -> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs hcmap (forall {k} (t :: k). Proxy t forall (t :: * -> Constraint). Proxy t Proxy @(Compose Eq Header)) (\(Pair Header a x Header a y) -> Bool -> K Bool a forall k a (b :: k). a -> K a b K (Bool -> K Bool a) -> Bool -> K Bool a forall a b. (a -> b) -> a -> b $ Header a x Header a -> Header a -> Bool forall a. Eq a => a -> a -> Bool == Header a y) NS (Product Header Header) xs m