{-# 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.Strict import Data.Typeable (Typeable) import Data.Word import NoThunks.Class (NoThunks) import Ouroboros.Consensus.Block import Ouroboros.Consensus.HeaderValidation import Ouroboros.Consensus.TypeFamilyWrappers import Ouroboros.Consensus.Util (ShowProxy, (.:)) import Ouroboros.Consensus.Util.SOP import Ouroboros.Consensus.HardFork.Combinator.Abstract import Ouroboros.Consensus.HardFork.Combinator.AcrossEras import Ouroboros.Consensus.HardFork.Combinator.Basics import qualified Ouroboros.Consensus.HardFork.Combinator.Util.Match as Match {------------------------------------------------------------------------------- GetHeader -------------------------------------------------------------------------------} newtype instance Header (HardForkBlock xs) = HardForkHeader { 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 showList :: [Header (HardForkBlock xs)] -> ShowS $cshowList :: forall (xs :: [*]). CanHardFork xs => [Header (HardForkBlock xs)] -> ShowS show :: Header (HardForkBlock xs) -> String $cshow :: forall (xs :: [*]). CanHardFork xs => Header (HardForkBlock xs) -> String showsPrec :: Int -> Header (HardForkBlock xs) -> ShowS $cshowsPrec :: forall (xs :: [*]). CanHardFork xs => Int -> 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 showTypeOf :: Proxy (Header (HardForkBlock xs)) -> String $cshowTypeOf :: forall (xs :: [*]). CanHardFork xs => Proxy (Header (HardForkBlock xs)) -> String wNoThunks :: Context -> Header (HardForkBlock xs) -> IO (Maybe ThunkInfo) $cwNoThunks :: forall (xs :: [*]). CanHardFork xs => Context -> Header (HardForkBlock xs) -> IO (Maybe ThunkInfo) noThunks :: Context -> Header (HardForkBlock xs) -> IO (Maybe ThunkInfo) $cnoThunks :: forall (xs :: [*]). CanHardFork xs => Context -> Header (HardForkBlock xs) -> IO (Maybe ThunkInfo) 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 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 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 :: 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 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)) 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 :: Header blk -> HeaderFields (Header (HardForkBlock xs)) getOne Header blk hdr = HeaderFields :: forall b. SlotNo -> BlockNo -> HeaderHash b -> HeaderFields b 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 toShortRawHash (Proxy blk 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{SlotNo BlockNo HeaderHash (Header blk) headerFieldBlockNo :: BlockNo headerFieldBlockNo :: forall b. HeaderFields b -> BlockNo headerFieldSlot :: SlotNo headerFieldSlot :: forall b. HeaderFields b -> SlotNo headerFieldHash :: HeaderHash (Header blk) headerFieldHash :: forall b. HeaderFields b -> HeaderHash b ..} = 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) 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 :: 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 b. ChainHash b GenesisHash BlockHash HeaderHash blk h -> HeaderHash (HardForkBlock xs) -> ChainHash (HardForkBlock xs) forall b. 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 toShortRawHash (Proxy blk 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 :: 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 :: NestedCtxt_ (HardForkBlock xs') Header a -> NestedCtxt_ (HardForkBlock xs') Header b -> Maybe (a :~: b) go (NCZ ctxt) (NCZ ctxt') = 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 ctxt) (NCS 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 :: 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 (x : xs)) a -> a -> DepPair (NestedCtxt Header (HardForkBlock (x : xs))) forall (f :: * -> *) a. f a -> a -> DepPair f DepPair (NestedCtxt_ (HardForkBlock (x : xs)) Header a -> NestedCtxt Header (HardForkBlock (x : xs)) a forall (f :: * -> *) blk a. NestedCtxt_ blk f a -> NestedCtxt f blk a NestedCtxt (NestedCtxt_ x Header a -> NestedCtxt_ (HardForkBlock (x : xs)) Header a forall x (f :: * -> *) a (xs :: [*]). NestedCtxt_ x f a -> NestedCtxt_ (HardForkBlock (x : xs)) f a NCZ NestedCtxt_ x Header a ctxt)) a x' go (S NS Header xs x) = case 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 x of DepPair (NestedCtxt NestedCtxt_ (HardForkBlock xs) Header a ctxt) a x' -> NestedCtxt Header (HardForkBlock (x : xs)) a -> a -> DepPair (NestedCtxt Header (HardForkBlock (x : xs))) forall (f :: * -> *) a. f a -> a -> DepPair f DepPair (NestedCtxt_ (HardForkBlock (x : xs)) Header a -> NestedCtxt Header (HardForkBlock (x : xs)) a forall (f :: * -> *) blk a. NestedCtxt_ blk f a -> NestedCtxt f blk a NestedCtxt (NestedCtxt_ (HardForkBlock xs) Header a -> NestedCtxt_ (HardForkBlock (x : xs)) Header a forall (xs :: [*]) (f :: * -> *) a x. NestedCtxt_ (HardForkBlock xs) f a -> NestedCtxt_ (HardForkBlock (x : xs)) f a NCS NestedCtxt_ (HardForkBlock xs) 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 :: NestedCtxt Header (HardForkBlock xs') a -> a -> NS Header xs' go (NestedCtxt (NCZ ctxt)) a x = Header x -> NS Header (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs) 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 ctxt)) a x = NS Header xs -> NS Header (x : xs) forall a (f :: a -> *) (xs :: [a]) (x :: a). NS f xs -> NS f (x : xs) 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 :: proxy (HardForkBlock xs) -> HeaderHash (HardForkBlock xs) -> ShortByteString toShortRawHash proxy (HardForkBlock xs) _ = HeaderHash (HardForkBlock xs) -> ShortByteString forall k (xs :: [k]). OneEraHash xs -> ShortByteString getOneEraHash fromShortRawHash :: proxy (HardForkBlock xs) -> ShortByteString -> HeaderHash (HardForkBlock xs) fromShortRawHash proxy (HardForkBlock xs) _ = ShortByteString -> HeaderHash (HardForkBlock xs) forall k (xs :: [k]). ShortByteString -> OneEraHash xs OneEraHash hashSize :: 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 hcpure Proxy SingleEraBlock proxySingle forall a. SingleEraBlock a => K Word32 a hashSizeOne hashSizeOne :: forall blk. SingleEraBlock blk => K Word32 blk hashSizeOne :: K Word32 blk 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 hashSize (Proxy blk 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 :: proxy (HardForkBlock xs) -> TipInfo (HardForkBlock xs) -> HeaderHash (HardForkBlock xs) tipInfoHash proxy (HardForkBlock xs) _ = NS (K (OneEraHash xs)) xs -> OneEraHash xs 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 :: 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 toShortRawHash (Proxy blk 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 tipInfoHash (Proxy blk 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 :: AnnTip (HardForkBlock xs) -> NS AnnTip xs distribAnnTip AnnTip{SlotNo BlockNo TipInfo (HardForkBlock xs) annTipInfo :: forall blk. AnnTip blk -> TipInfo blk annTipBlockNo :: forall blk. AnnTip blk -> BlockNo annTipSlotNo :: forall blk. AnnTip blk -> SlotNo annTipInfo :: TipInfo (HardForkBlock xs) annTipBlockNo :: BlockNo annTipSlotNo :: SlotNo ..} = (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 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 :: WrapTipInfo blk -> AnnTip blk 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 :: NS AnnTip xs -> AnnTip (HardForkBlock xs) undistribAnnTip = NS (K (AnnTip (HardForkBlock xs))) xs -> AnnTip (HardForkBlock xs) 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 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 :: Index xs blk -> AnnTip blk -> K (AnnTip (HardForkBlock xs)) blk undistrib Index xs blk index AnnTip{SlotNo BlockNo TipInfo blk annTipInfo :: TipInfo blk annTipBlockNo :: BlockNo annTipSlotNo :: SlotNo annTipInfo :: forall blk. AnnTip blk -> TipInfo blk annTipBlockNo :: forall blk. AnnTip blk -> BlockNo annTipSlotNo :: forall blk. AnnTip blk -> SlotNo ..} = 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 -> OneEraTipInfo xs forall (xs :: [*]). NS WrapTipInfo xs -> OneEraTipInfo xs OneEraTipInfo (NS WrapTipInfo xs -> OneEraTipInfo xs) -> (TipInfo blk -> NS WrapTipInfo xs) -> TipInfo blk -> OneEraTipInfo 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 -> OneEraTipInfo xs) -> TipInfo blk -> OneEraTipInfo xs forall a b. (a -> b) -> a -> b $ TipInfo blk annTipInfo) {------------------------------------------------------------------------------- BasicEnvelopeValidation -------------------------------------------------------------------------------} instance CanHardFork xs => BasicEnvelopeValidation (HardForkBlock xs) where expectedFirstBlockNo :: 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 isNonEmpty (Proxy xs forall k (t :: k). Proxy t Proxy @xs) of ProofNonEmpty Proxy x p Proxy xs _ -> Proxy x -> BlockNo forall blk (proxy :: * -> *). BasicEnvelopeValidation blk => proxy blk -> 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 isNonEmpty (Proxy xs forall k (t :: k). Proxy t Proxy @xs) of ProofNonEmpty Proxy x p Proxy xs _ -> 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 :: proxy (HardForkBlock xs) -> TipInfo (HardForkBlock xs) -> TipInfo (HardForkBlock xs) -> BlockNo -> BlockNo expectedNextBlockNo proxy (HardForkBlock xs) _ (OneEraTipInfo oldTip) (OneEraTipInfo 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 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 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 :: Product WrapTipInfo WrapTipInfo blk -> K BlockNo blk 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 expectedNextBlockNo (Proxy blk 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 :: proxy (HardForkBlock xs) -> TipInfo (HardForkBlock xs) -> TipInfo (HardForkBlock xs) -> SlotNo -> SlotNo minimumNextSlotNo proxy (HardForkBlock xs) _ (OneEraTipInfo oldTip) (OneEraTipInfo 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 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 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 :: Product WrapTipInfo WrapTipInfo blk -> K SlotNo blk 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 minimumNextSlotNo (Proxy blk 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 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 (Proxy Eq forall k (t :: k). Proxy t Proxy @Eq) (\(Pair x 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 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 (Proxy (Compose Eq Header) forall k (t :: k). Proxy t Proxy @(Compose Eq Header)) (\(Pair x 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