{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module Test.Ouroboros.Consensus.DiffusionPipelining (prop_diffusionPipeliningSubsequenceConsistency) where

import           Control.Exception (assert)
import           Data.Either (isRight)
import           Data.Proxy
import           Ouroboros.Consensus.Block
import           Test.QuickCheck

-- | See /Consistent validity under subsequences/ in
-- 'BlockSupportsDiffusionPipelining'.
prop_diffusionPipeliningSubsequenceConsistency ::
     forall blk.
     BlockSupportsDiffusionPipelining blk
  => Proxy blk
  -> [TentativeHeaderView blk]
     -- ^ Have to satisfy the pipelining criterion.
  -> Property
prop_diffusionPipeliningSubsequenceConsistency :: forall blk.
BlockSupportsDiffusionPipelining blk =>
Proxy blk -> [TentativeHeaderView blk] -> Property
prop_diffusionPipeliningSubsequenceConsistency Proxy blk
_ [TentativeHeaderView blk]
thvs =
    Bool -> Property -> Property
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Either ([TentativeHeaderView blk], TentativeHeaderState blk) ()
-> Bool
forall a b. Either a b -> Bool
isRight (Either ([TentativeHeaderView blk], TentativeHeaderState blk) ()
 -> Bool)
-> Either ([TentativeHeaderView blk], TentativeHeaderState blk) ()
-> Bool
forall a b. (a -> b) -> a -> b
$ [TentativeHeaderView blk]
-> Either ([TentativeHeaderView blk], TentativeHeaderState blk) ()
satisfyPipeliningCriterion [TentativeHeaderView blk]
thvs) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    Gen [TentativeHeaderView blk]
-> ([TentativeHeaderView blk] -> [[TentativeHeaderView blk]])
-> ([TentativeHeaderView blk] -> Property)
-> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
forAllShrink ([TentativeHeaderView blk] -> Gen [TentativeHeaderView blk]
forall a. [a] -> Gen [a]
sublistOf [TentativeHeaderView blk]
thvs) ((TentativeHeaderView blk -> [TentativeHeaderView blk])
-> [TentativeHeaderView blk] -> [[TentativeHeaderView blk]]
forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList ([TentativeHeaderView blk]
-> TentativeHeaderView blk -> [TentativeHeaderView blk]
forall a b. a -> b -> a
const [])) (([TentativeHeaderView blk] -> Property) -> Property)
-> ([TentativeHeaderView blk] -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \[TentativeHeaderView blk]
thvs' ->
      case [TentativeHeaderView blk]
-> Either ([TentativeHeaderView blk], TentativeHeaderState blk) ()
satisfyPipeliningCriterion [TentativeHeaderView blk]
thvs' of
        Right () -> () -> Property
forall prop. Testable prop => prop -> Property
property ()
        Left ([TentativeHeaderView blk]
hdrs'', TentativeHeaderState blk
st) ->
            String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"tentative header view subsequence: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> [TentativeHeaderView blk] -> String
forall a. Show a => a -> String
show [TentativeHeaderView blk]
hdrs'')
          (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"last state: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> TentativeHeaderState blk -> String
forall a. Show a => a -> String
show TentativeHeaderState blk
st)
          (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ String -> () -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"unexpected violation of pipelining criterion!"
            ()
  where
    satisfyPipeliningCriterion ::
         [TentativeHeaderView blk]
      -> Either ([TentativeHeaderView blk], TentativeHeaderState blk) ()
    satisfyPipeliningCriterion :: [TentativeHeaderView blk]
-> Either ([TentativeHeaderView blk], TentativeHeaderState blk) ()
satisfyPipeliningCriterion [TentativeHeaderView blk]
allThvs =
        Int
-> TentativeHeaderState blk
-> [TentativeHeaderView blk]
-> Either ([TentativeHeaderView blk], TentativeHeaderState blk) ()
go Int
1 (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)) [TentativeHeaderView blk]
allThvs
      where
        go :: Int
-> TentativeHeaderState blk
-> [TentativeHeaderView blk]
-> Either ([TentativeHeaderView blk], TentativeHeaderState blk) ()
go Int
ix TentativeHeaderState blk
st = \case
          [] -> ()
-> Either ([TentativeHeaderView blk], TentativeHeaderState blk) ()
forall a b. b -> Either a b
Right ()
          TentativeHeaderView blk
thv : [TentativeHeaderView blk]
thvs' -> case 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 of
            Just TentativeHeaderState blk
st' -> Int
-> TentativeHeaderState blk
-> [TentativeHeaderView blk]
-> Either ([TentativeHeaderView blk], TentativeHeaderState blk) ()
go (Int
ix Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) TentativeHeaderState blk
st' [TentativeHeaderView blk]
thvs'
            Maybe (TentativeHeaderState blk)
Nothing  -> ([TentativeHeaderView blk], TentativeHeaderState blk)
-> Either ([TentativeHeaderView blk], TentativeHeaderState blk) ()
forall a b. a -> Either a b
Left (Int -> [TentativeHeaderView blk] -> [TentativeHeaderView blk]
forall a. Int -> [a] -> [a]
take Int
ix [TentativeHeaderView blk]
allThvs, TentativeHeaderState blk
st)