{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# OPTIONS_GHC -Wno-orphans #-} module Ouroboros.Consensus.HardFork.Combinator.Node.DiffusionPipelining () where import Data.Functor.Product import Data.Proxy import Data.SOP.BasicFunctors import qualified Data.SOP.Match as Match import Data.SOP.NonEmpty import Data.SOP.Strict import Ouroboros.Consensus.Block.SupportsDiffusionPipelining import Ouroboros.Consensus.HardFork.Combinator.Abstract import Ouroboros.Consensus.HardFork.Combinator.AcrossEras import Ouroboros.Consensus.HardFork.Combinator.Basics import Ouroboros.Consensus.HardFork.Combinator.Block import Ouroboros.Consensus.TypeFamilyWrappers import Ouroboros.Consensus.Util -- | The 'BlockSupportsDiffusionPipelining' instance for the HFC is -- compositional: -- -- - @'TentativeHeaderState' ('HardForkBlock' xs)@ is -- 'OneEraTentativeHeaderState', the n-ary sum of per-era -- 'TentativeHeaderState's. The 'initialTentativeHeaderState' is the one for -- the first era. -- -- - Similarly, @'TentativeHeaderView' ('HardForkBlock' xs)@ is -- 'OneEraTentativeHeaderView', the n-ary sum of per-era -- 'TentativeHeaderView's, and 'tentativeHeaderView' delegates to the -- era-specific 'tentativeHeaderView'. -- -- - @'applyTentativeHeaderView' 'Proxy' thv st@ works like this: -- -- - If @thv@ and @st@ are in the same era, we call the corresponding -- era-specific 'applyTentativeHeaderView'. -- -- - If @thv@ is in a later era than @st@, we replace @st@ with the -- 'initialTentativeHeaderState' for the era of @thv@, and then proceed -- like in the previous step. -- -- - If @thv@ is in an earlier era than @st@, we return 'Nothing' to -- disallow pipelining. -- -- This behavior guarantees the "Consistent validity under subsequences" -- requirement if it is satisfied for every era. -- -- Note that at an era boundary, the tip of the selection might switch multiple -- times between two adjacent eras. Compared to the scenario where the -- pipelining criteria in both eras are compatible and make sense even across -- eras, this might lead to unnecessarily strict/relaxed diffusion pipelining. -- However, the tip switching between different eras is rare and rather short, -- so there is no direct need to address this, so we rather avoid the extra -- complexity for now. -- -- Still, a possible future refinement would be to allow custom logic for -- "upgrading" the 'TentativeHeaderState' to a new era. instance CanHardFork xs => BlockSupportsDiffusionPipelining (HardForkBlock xs) where type TentativeHeaderState (HardForkBlock xs) = OneEraTentativeHeaderState xs type TentativeHeaderView (HardForkBlock xs) = OneEraTentativeHeaderView xs initialTentativeHeaderState :: Proxy (HardForkBlock xs) -> TentativeHeaderState (HardForkBlock xs) initialTentativeHeaderState Proxy (HardForkBlock xs) _ | ProofNonEmpty Proxy x proxyHead Proxy xs1 _ <- 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) = NS WrapTentativeHeaderState (x : xs1) -> OneEraTentativeHeaderState (x : xs1) forall (xs :: [*]). NS WrapTentativeHeaderState xs -> OneEraTentativeHeaderState xs OneEraTentativeHeaderState (NS WrapTentativeHeaderState (x : xs1) -> OneEraTentativeHeaderState (x : xs1)) -> NS WrapTentativeHeaderState (x : xs1) -> OneEraTentativeHeaderState (x : xs1) forall a b. (a -> b) -> a -> b $ WrapTentativeHeaderState x -> NS WrapTentativeHeaderState (x : xs1) forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]). f x -> NS f (x : xs1) Z (WrapTentativeHeaderState x -> NS WrapTentativeHeaderState (x : xs1)) -> WrapTentativeHeaderState x -> NS WrapTentativeHeaderState (x : xs1) forall a b. (a -> b) -> a -> b $ TentativeHeaderState x -> WrapTentativeHeaderState x forall blk. TentativeHeaderState blk -> WrapTentativeHeaderState blk WrapTentativeHeaderState (TentativeHeaderState x -> WrapTentativeHeaderState x) -> TentativeHeaderState x -> WrapTentativeHeaderState x forall a b. (a -> b) -> a -> b $ Proxy x -> TentativeHeaderState x forall blk. BlockSupportsDiffusionPipelining blk => Proxy blk -> TentativeHeaderState blk initialTentativeHeaderState Proxy x proxyHead tentativeHeaderView :: BlockConfig (HardForkBlock xs) -> Header (HardForkBlock xs) -> TentativeHeaderView (HardForkBlock xs) tentativeHeaderView (HardForkBlockConfig (PerEraBlockConfig NP BlockConfig xs bcfg)) (HardForkHeader (OneEraHeader NS Header xs hdr)) = NS WrapTentativeHeaderView xs -> TentativeHeaderView (HardForkBlock xs) NS WrapTentativeHeaderView xs -> OneEraTentativeHeaderView xs forall (xs :: [*]). NS WrapTentativeHeaderView xs -> OneEraTentativeHeaderView xs OneEraTentativeHeaderView (NS WrapTentativeHeaderView xs -> TentativeHeaderView (HardForkBlock xs)) -> (NS Header xs -> NS WrapTentativeHeaderView xs) -> NS Header xs -> TentativeHeaderView (HardForkBlock xs) forall b c a. (b -> c) -> (a -> b) -> a -> c . Proxy SingleEraBlock -> (forall a. SingleEraBlock a => BlockConfig a -> Header a -> WrapTentativeHeaderView a) -> Prod NS BlockConfig xs -> NS Header xs -> NS WrapTentativeHeaderView xs forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *) (f'' :: k -> *). (AllN (Prod h) c xs, HAp h, HAp (Prod h)) => proxy c -> (forall (a :: k). c a => f a -> f' a -> f'' a) -> Prod h f xs -> h f' xs -> h f'' xs hcliftA2 Proxy SingleEraBlock proxySingle (TentativeHeaderView a -> WrapTentativeHeaderView a forall blk. TentativeHeaderView blk -> WrapTentativeHeaderView blk WrapTentativeHeaderView (TentativeHeaderView a -> WrapTentativeHeaderView a) -> (BlockConfig a -> Header a -> TentativeHeaderView a) -> BlockConfig a -> Header a -> WrapTentativeHeaderView a forall y z x0 x1. (y -> z) -> (x0 -> x1 -> y) -> x0 -> x1 -> z .: BlockConfig a -> Header a -> TentativeHeaderView a forall blk. BlockSupportsDiffusionPipelining blk => BlockConfig blk -> Header blk -> TentativeHeaderView blk tentativeHeaderView) Prod NS BlockConfig xs NP BlockConfig xs bcfg (NS Header xs -> TentativeHeaderView (HardForkBlock xs)) -> NS Header xs -> TentativeHeaderView (HardForkBlock xs) forall a b. (a -> b) -> a -> b $ NS Header xs hdr applyTentativeHeaderView :: Proxy (HardForkBlock xs) -> TentativeHeaderView (HardForkBlock xs) -> TentativeHeaderState (HardForkBlock xs) -> Maybe (TentativeHeaderState (HardForkBlock xs)) applyTentativeHeaderView Proxy (HardForkBlock xs) Proxy (OneEraTentativeHeaderView NS WrapTentativeHeaderView xs thv) (OneEraTentativeHeaderState NS WrapTentativeHeaderState xs st) = (NS WrapTentativeHeaderState xs -> OneEraTentativeHeaderState xs) -> Maybe (NS WrapTentativeHeaderState xs) -> Maybe (OneEraTentativeHeaderState xs) forall a b. (a -> b) -> Maybe a -> Maybe b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap NS WrapTentativeHeaderState xs -> OneEraTentativeHeaderState xs forall (xs :: [*]). NS WrapTentativeHeaderState xs -> OneEraTentativeHeaderState xs OneEraTentativeHeaderState (Maybe (NS WrapTentativeHeaderState xs) -> Maybe (OneEraTentativeHeaderState xs)) -> (NS (Product WrapTentativeHeaderView WrapTentativeHeaderState) xs -> Maybe (NS WrapTentativeHeaderState xs)) -> NS (Product WrapTentativeHeaderView WrapTentativeHeaderState) xs -> Maybe (OneEraTentativeHeaderState xs) forall b c a. (b -> c) -> (a -> b) -> a -> c . NS (Maybe :.: WrapTentativeHeaderState) xs -> Maybe (NS WrapTentativeHeaderState xs) forall {k} (xs :: [k]) (f :: * -> *) (g :: k -> *). Functor f => NS (f :.: g) xs -> f (NS g xs) sequence_NS' (NS (Maybe :.: WrapTentativeHeaderState) xs -> Maybe (NS WrapTentativeHeaderState xs)) -> (NS (Product WrapTentativeHeaderView WrapTentativeHeaderState) xs -> NS (Maybe :.: WrapTentativeHeaderState) xs) -> NS (Product WrapTentativeHeaderView WrapTentativeHeaderState) xs -> Maybe (NS WrapTentativeHeaderState xs) forall b c a. (b -> c) -> (a -> b) -> a -> c . Proxy SingleEraBlock -> (forall a. SingleEraBlock a => Product WrapTentativeHeaderView WrapTentativeHeaderState a -> (:.:) Maybe WrapTentativeHeaderState a) -> NS (Product WrapTentativeHeaderView WrapTentativeHeaderState) xs -> NS (Maybe :.: WrapTentativeHeaderState) 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 WrapTentativeHeaderView WrapTentativeHeaderState a -> (:.:) Maybe WrapTentativeHeaderState a forall blk. BlockSupportsDiffusionPipelining blk => Product WrapTentativeHeaderView WrapTentativeHeaderState blk -> (:.:) Maybe WrapTentativeHeaderState blk forall a. SingleEraBlock a => Product WrapTentativeHeaderView WrapTentativeHeaderState a -> (:.:) Maybe WrapTentativeHeaderState a updateSt (NS (Product WrapTentativeHeaderView WrapTentativeHeaderState) xs -> Maybe (OneEraTentativeHeaderState xs)) -> Maybe (NS (Product WrapTentativeHeaderView WrapTentativeHeaderState) xs) -> Maybe (OneEraTentativeHeaderState xs) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b =<< case NS WrapTentativeHeaderView xs -> NS WrapTentativeHeaderState xs -> Either (Mismatch WrapTentativeHeaderView WrapTentativeHeaderState xs) (NS (Product WrapTentativeHeaderView WrapTentativeHeaderState) 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 WrapTentativeHeaderView xs thv NS WrapTentativeHeaderState xs st of Right NS (Product WrapTentativeHeaderView WrapTentativeHeaderState) xs thvSt -> NS (Product WrapTentativeHeaderView WrapTentativeHeaderState) xs -> Maybe (NS (Product WrapTentativeHeaderView WrapTentativeHeaderState) xs) forall a. a -> Maybe a Just NS (Product WrapTentativeHeaderView WrapTentativeHeaderState) xs thvSt Left Mismatch WrapTentativeHeaderView WrapTentativeHeaderState xs mismatch -> Mismatch WrapTentativeHeaderView WrapTentativeHeaderState xs -> Maybe (NS (Product WrapTentativeHeaderView WrapTentativeHeaderState) xs) fromMismatch Mismatch WrapTentativeHeaderView WrapTentativeHeaderState xs mismatch where updateSt :: forall blk. BlockSupportsDiffusionPipelining blk => Product WrapTentativeHeaderView WrapTentativeHeaderState blk -> (Maybe :.: WrapTentativeHeaderState) blk updateSt :: forall blk. BlockSupportsDiffusionPipelining blk => Product WrapTentativeHeaderView WrapTentativeHeaderState blk -> (:.:) Maybe WrapTentativeHeaderState blk updateSt (Pair (WrapTentativeHeaderView TentativeHeaderView blk thv') (WrapTentativeHeaderState TentativeHeaderState blk st')) = Maybe (WrapTentativeHeaderState blk) -> (:.:) Maybe WrapTentativeHeaderState blk forall l k (f :: l -> *) (g :: k -> l) (p :: k). f (g p) -> (:.:) f g p Comp (Maybe (WrapTentativeHeaderState blk) -> (:.:) Maybe WrapTentativeHeaderState blk) -> Maybe (WrapTentativeHeaderState blk) -> (:.:) Maybe WrapTentativeHeaderState blk forall a b. (a -> b) -> a -> b $ (TentativeHeaderState blk -> WrapTentativeHeaderState blk) -> Maybe (TentativeHeaderState blk) -> Maybe (WrapTentativeHeaderState blk) forall a b. (a -> b) -> Maybe a -> Maybe b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap TentativeHeaderState blk -> WrapTentativeHeaderState blk forall blk. TentativeHeaderState blk -> WrapTentativeHeaderState blk WrapTentativeHeaderState (Maybe (TentativeHeaderState blk) -> Maybe (WrapTentativeHeaderState blk)) -> Maybe (TentativeHeaderState blk) -> Maybe (WrapTentativeHeaderState blk) forall a b. (a -> b) -> a -> b $ Proxy blk -> TentativeHeaderView blk -> TentativeHeaderState blk -> Maybe (TentativeHeaderState blk) forall blk. BlockSupportsDiffusionPipelining blk => Proxy blk -> TentativeHeaderView blk -> TentativeHeaderState blk -> Maybe (TentativeHeaderState blk) applyTentativeHeaderView (forall t. Proxy t forall {k} (t :: k). Proxy t Proxy @blk) TentativeHeaderView blk thv' TentativeHeaderState blk st' -- If the mismatch indicates that the tentative header view is in a later -- era than the 'TentativeHeaderState', pair the view with the -- 'initialTentativeHeaderState' of its era. fromMismatch :: Match.Mismatch WrapTentativeHeaderView WrapTentativeHeaderState xs -> Maybe (NS (Product WrapTentativeHeaderView WrapTentativeHeaderState) xs) fromMismatch :: Mismatch WrapTentativeHeaderView WrapTentativeHeaderState xs -> Maybe (NS (Product WrapTentativeHeaderView WrapTentativeHeaderState) xs) fromMismatch Mismatch WrapTentativeHeaderView WrapTentativeHeaderState xs mismatch | ProofNonEmpty Proxy x _ Proxy xs1 _ <- 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) = case Mismatch WrapTentativeHeaderView WrapTentativeHeaderState (x : xs1) -> Either (NS WrapTentativeHeaderView xs1) (NS WrapTentativeHeaderState xs1) forall {k} (f :: k -> *) (g :: k -> *) (x :: k) (xs :: [k]). Mismatch f g (x : xs) -> Either (NS f xs) (NS g xs) Match.mismatchNotFirst Mismatch WrapTentativeHeaderView WrapTentativeHeaderState xs Mismatch WrapTentativeHeaderView WrapTentativeHeaderState (x : xs1) mismatch of -- The @thv@ is in an earlier era compared to the @st@, so it does -- not satisfy the HFC pipelining criterion. Right NS WrapTentativeHeaderState xs1 _ -> Maybe (NS (Product WrapTentativeHeaderView WrapTentativeHeaderState) xs) forall a. Maybe a Nothing -- The @thv@ is in a later era compared to the @st@. Left NS WrapTentativeHeaderView xs1 thv' -> NS (Product WrapTentativeHeaderView WrapTentativeHeaderState) xs -> Maybe (NS (Product WrapTentativeHeaderView WrapTentativeHeaderState) xs) forall a. a -> Maybe a Just (NS (Product WrapTentativeHeaderView WrapTentativeHeaderState) xs -> Maybe (NS (Product WrapTentativeHeaderView WrapTentativeHeaderState) xs)) -> NS (Product WrapTentativeHeaderView WrapTentativeHeaderState) xs -> Maybe (NS (Product WrapTentativeHeaderView WrapTentativeHeaderState) xs) forall a b. (a -> b) -> a -> b $ Proxy SingleEraBlock -> (forall a. SingleEraBlock a => WrapTentativeHeaderView a -> Product WrapTentativeHeaderView WrapTentativeHeaderState a) -> NS WrapTentativeHeaderView xs -> NS (Product WrapTentativeHeaderView WrapTentativeHeaderState) 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 WrapTentativeHeaderView a -> Product WrapTentativeHeaderView WrapTentativeHeaderState a forall blk. BlockSupportsDiffusionPipelining blk => WrapTentativeHeaderView blk -> Product WrapTentativeHeaderView WrapTentativeHeaderState blk forall a. SingleEraBlock a => WrapTentativeHeaderView a -> Product WrapTentativeHeaderView WrapTentativeHeaderState a withInitialSt (NS WrapTentativeHeaderView xs1 -> NS WrapTentativeHeaderView (x : xs1) forall {k} (f :: k -> *) (xs1 :: [k]) (x :: k). NS f xs1 -> NS f (x : xs1) S NS WrapTentativeHeaderView xs1 thv') where withInitialSt :: forall blk. BlockSupportsDiffusionPipelining blk => WrapTentativeHeaderView blk -> Product WrapTentativeHeaderView WrapTentativeHeaderState blk withInitialSt :: forall blk. BlockSupportsDiffusionPipelining blk => WrapTentativeHeaderView blk -> Product WrapTentativeHeaderView WrapTentativeHeaderState blk withInitialSt WrapTentativeHeaderView blk v = WrapTentativeHeaderView blk -> WrapTentativeHeaderState blk -> Product WrapTentativeHeaderView WrapTentativeHeaderState blk forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> g a -> Product f g a Pair WrapTentativeHeaderView blk v (TentativeHeaderState blk -> WrapTentativeHeaderState blk forall blk. TentativeHeaderState blk -> WrapTentativeHeaderState blk WrapTentativeHeaderState TentativeHeaderState blk initialSt) where initialSt :: TentativeHeaderState blk initialSt = Proxy blk -> TentativeHeaderState blk forall blk. BlockSupportsDiffusionPipelining blk => Proxy blk -> TentativeHeaderState blk initialTentativeHeaderState (forall t. Proxy t forall {k} (t :: k). Proxy t Proxy @blk)