{-# 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)