{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}

module Test.Ouroboros.Consensus.ChainGenerator.Tests.Honest (
    -- * Re-use
    TestHonest (TestHonest, testAsc, testRecipe, testRecipe')
  , unlines'
    -- * Tests
  , tests
  ) where

import qualified Control.Exception as IO (evaluate)
import qualified Control.Monad.Except as Exn
import           Data.Functor ((<&>))
import           Data.Functor.Identity (runIdentity)
import           Data.List (intercalate)
import           Data.Proxy (Proxy (Proxy))
import qualified System.Random as R
import qualified System.Timeout as IO (timeout)
import qualified Test.Ouroboros.Consensus.ChainGenerator.Honest as H
import           Test.Ouroboros.Consensus.ChainGenerator.Params (Asc,
                     Delta (Delta), Kcp (Kcp), Len (Len), Scg (Scg), genAsc,
                     genKSD)
import qualified Test.QuickCheck as QC
import           Test.QuickCheck.Extras (sized1, unsafeMapSuchThatJust)
import           Test.QuickCheck.Random (QCGen)
import qualified Test.Tasty as TT
import qualified Test.Tasty.QuickCheck as TT

-----

tests :: [TT.TestTree]
tests :: [TestTree]
tests = [
    TestName -> (TestHonest -> QCGen -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
TT.testProperty TestName
"prop_honestChain" TestHonest -> QCGen -> Property
prop_honestChain
  ,
    TestName -> (TestHonestMutation -> QCGen -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
TT.testProperty TestName
"prop_honestChainMutation" TestHonestMutation -> QCGen -> Property
prop_honestChainMutation
  ]

-----

data TestHonest = TestHonest {
    TestHonest -> Asc
testAsc     :: !Asc
  ,
    TestHonest -> HonestRecipe
testRecipe  :: !H.HonestRecipe
  ,
    TestHonest -> SomeCheckedHonestRecipe
testRecipe' :: !H.SomeCheckedHonestRecipe
  }
  deriving (ReadPrec [TestHonest]
ReadPrec TestHonest
Int -> ReadS TestHonest
ReadS [TestHonest]
(Int -> ReadS TestHonest)
-> ReadS [TestHonest]
-> ReadPrec TestHonest
-> ReadPrec [TestHonest]
-> Read TestHonest
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS TestHonest
readsPrec :: Int -> ReadS TestHonest
$creadList :: ReadS [TestHonest]
readList :: ReadS [TestHonest]
$creadPrec :: ReadPrec TestHonest
readPrec :: ReadPrec TestHonest
$creadListPrec :: ReadPrec [TestHonest]
readListPrec :: ReadPrec [TestHonest]
Read, Int -> TestHonest -> ShowS
[TestHonest] -> ShowS
TestHonest -> TestName
(Int -> TestHonest -> ShowS)
-> (TestHonest -> TestName)
-> ([TestHonest] -> ShowS)
-> Show TestHonest
forall a.
(Int -> a -> ShowS) -> (a -> TestName) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TestHonest -> ShowS
showsPrec :: Int -> TestHonest -> ShowS
$cshow :: TestHonest -> TestName
show :: TestHonest -> TestName
$cshowList :: [TestHonest] -> ShowS
showList :: [TestHonest] -> ShowS
Show)

instance QC.Arbitrary TestHonest where
    arbitrary :: Gen TestHonest
arbitrary = do
        testAsc <- Gen Asc
genAsc
        testRecipe <- H.genHonestRecipe

        testRecipe' <- case Exn.runExcept $ H.checkHonestRecipe testRecipe of
            Left NoSuchHonestChainSchema
e  -> TestName -> Gen SomeCheckedHonestRecipe
forall a. HasCallStack => TestName -> a
error (TestName -> Gen SomeCheckedHonestRecipe)
-> TestName -> Gen SomeCheckedHonestRecipe
forall a b. (a -> b) -> a -> b
$ TestName
"impossible! " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> (HonestRecipe, NoSuchHonestChainSchema) -> TestName
forall a. Show a => a -> TestName
show (HonestRecipe
testRecipe, NoSuchHonestChainSchema
e)
            Right SomeCheckedHonestRecipe
x -> SomeCheckedHonestRecipe -> Gen SomeCheckedHonestRecipe
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SomeCheckedHonestRecipe
x

        pure TestHonest {
            testAsc
          ,
            testRecipe
          ,
            testRecipe'
          }

-- | No seed exists such that each 'H.checkHonestChain' rejects the result of 'H.uniformTheHonestChain'
prop_honestChain :: TestHonest -> QCGen -> QC.Property
prop_honestChain :: TestHonest -> QCGen -> Property
prop_honestChain TestHonest
testHonest QCGen
testSeed = Identity Property -> Property
forall a. Identity a -> a
runIdentity (Identity Property -> Property) -> Identity Property -> Property
forall a b. (a -> b) -> a -> b
$ do
    H.SomeCheckedHonestRecipe Proxy Proxy recipe' <- SomeCheckedHonestRecipe -> Identity SomeCheckedHonestRecipe
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SomeCheckedHonestRecipe
testRecipe'

    let sched = Maybe Asc
-> CheckedHonestRecipe base hon -> QCGen -> ChainSchema base hon
forall base hon g.
RandomGen g =>
Maybe Asc
-> CheckedHonestRecipe base hon -> g -> ChainSchema base hon
H.uniformTheHonestChain (Asc -> Maybe Asc
forall a. a -> Maybe a
Just Asc
testAsc) CheckedHonestRecipe base hon
recipe' QCGen
testSeed

    QC.counterexample (unlines' $ H.prettyChainSchema sched "H") <$> do
        pure $ case Exn.runExcept $ H.checkHonestChain testRecipe sched of
            Right () -> () -> Property
forall prop. Testable prop => prop -> Property
QC.property ()
            Left HonestChainViolation hon
e   -> case HonestChainViolation hon
e of
                H.BadCount{}      -> TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (HonestChainViolation hon -> TestName
forall a. Show a => a -> TestName
show HonestChainViolation hon
e) Bool
False
                H.BadLength{}     -> TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (HonestChainViolation hon -> TestName
forall a. Show a => a -> TestName
show HonestChainViolation hon
e) Bool
False
                H.BadScgWindow ScgViolation hon
v ->
                    let str :: TestName
str = case ScgViolation hon
v of
                            H.ScgViolation {
                                scgvWindow :: ()
H.scgvWindow = Contains 'SlotE hon (Win ScgLbl skolem)
win
                              } -> Contains 'SlotE hon (Win ScgLbl skolem) -> ShowS
forall base inner. Contains 'SlotE base inner -> ShowS
H.prettyWindow Contains 'SlotE hon (Win ScgLbl skolem)
win TestName
"SCGV"
                    in
                        Property -> Property
forall a. a -> a
id
                      (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample TestName
str
                      (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (HonestChainViolation hon -> TestName
forall a. Show a => a -> TestName
show HonestChainViolation hon
e)
                      (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ Bool
False
  where
    TestHonest {
        Asc
testAsc :: TestHonest -> Asc
testAsc :: Asc
testAsc
      ,
        HonestRecipe
testRecipe :: TestHonest -> HonestRecipe
testRecipe :: HonestRecipe
testRecipe
      ,
        SomeCheckedHonestRecipe
testRecipe' :: TestHonest -> SomeCheckedHonestRecipe
testRecipe' :: SomeCheckedHonestRecipe
testRecipe'
      } = TestHonest
testHonest

-- 'unlines' adds a trailing newline, this function never does
unlines' :: [String] -> String
unlines' :: [TestName] -> TestName
unlines' = TestName -> [TestName] -> TestName
forall a. [a] -> [[a]] -> [a]
intercalate TestName
"\n"

-----

-- | A mutation that minimally increases the threshold density of an 'H.HonestRecipe''s SCG constraint
data HonestMutation =
    -- | Increasing 'Kcp' by one increases the SCG numerator
    HonestMutateKcp
  |
    -- | Decreasing 'Scg' by one decreases the SCG denominator
    HonestMutateScg
  deriving (HonestMutation -> HonestMutation -> Bool
(HonestMutation -> HonestMutation -> Bool)
-> (HonestMutation -> HonestMutation -> Bool) -> Eq HonestMutation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HonestMutation -> HonestMutation -> Bool
== :: HonestMutation -> HonestMutation -> Bool
$c/= :: HonestMutation -> HonestMutation -> Bool
/= :: HonestMutation -> HonestMutation -> Bool
Eq, ReadPrec [HonestMutation]
ReadPrec HonestMutation
Int -> ReadS HonestMutation
ReadS [HonestMutation]
(Int -> ReadS HonestMutation)
-> ReadS [HonestMutation]
-> ReadPrec HonestMutation
-> ReadPrec [HonestMutation]
-> Read HonestMutation
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS HonestMutation
readsPrec :: Int -> ReadS HonestMutation
$creadList :: ReadS [HonestMutation]
readList :: ReadS [HonestMutation]
$creadPrec :: ReadPrec HonestMutation
readPrec :: ReadPrec HonestMutation
$creadListPrec :: ReadPrec [HonestMutation]
readListPrec :: ReadPrec [HonestMutation]
Read, Int -> HonestMutation -> ShowS
[HonestMutation] -> ShowS
HonestMutation -> TestName
(Int -> HonestMutation -> ShowS)
-> (HonestMutation -> TestName)
-> ([HonestMutation] -> ShowS)
-> Show HonestMutation
forall a.
(Int -> a -> ShowS) -> (a -> TestName) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> HonestMutation -> ShowS
showsPrec :: Int -> HonestMutation -> ShowS
$cshow :: HonestMutation -> TestName
show :: HonestMutation -> TestName
$cshowList :: [HonestMutation] -> ShowS
showList :: [HonestMutation] -> ShowS
Show)

data TestHonestMutation =
    TestHonestMutation
        !H.HonestRecipe
        !H.SomeCheckedHonestRecipe
        !HonestMutation
  deriving (ReadPrec [TestHonestMutation]
ReadPrec TestHonestMutation
Int -> ReadS TestHonestMutation
ReadS [TestHonestMutation]
(Int -> ReadS TestHonestMutation)
-> ReadS [TestHonestMutation]
-> ReadPrec TestHonestMutation
-> ReadPrec [TestHonestMutation]
-> Read TestHonestMutation
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS TestHonestMutation
readsPrec :: Int -> ReadS TestHonestMutation
$creadList :: ReadS [TestHonestMutation]
readList :: ReadS [TestHonestMutation]
$creadPrec :: ReadPrec TestHonestMutation
readPrec :: ReadPrec TestHonestMutation
$creadListPrec :: ReadPrec [TestHonestMutation]
readListPrec :: ReadPrec [TestHonestMutation]
Read, Int -> TestHonestMutation -> ShowS
[TestHonestMutation] -> ShowS
TestHonestMutation -> TestName
(Int -> TestHonestMutation -> ShowS)
-> (TestHonestMutation -> TestName)
-> ([TestHonestMutation] -> ShowS)
-> Show TestHonestMutation
forall a.
(Int -> a -> ShowS) -> (a -> TestName) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TestHonestMutation -> ShowS
showsPrec :: Int -> TestHonestMutation -> ShowS
$cshow :: TestHonestMutation -> TestName
show :: TestHonestMutation -> TestName
$cshowList :: [TestHonestMutation] -> ShowS
showList :: [TestHonestMutation] -> ShowS
Show)

mutateHonest :: H.HonestRecipe -> HonestMutation -> H.HonestRecipe
mutateHonest :: HonestRecipe -> HonestMutation -> HonestRecipe
mutateHonest HonestRecipe
recipe HonestMutation
mut =
    Kcp -> Scg -> Delta -> Len -> HonestRecipe
H.HonestRecipe (Int -> Kcp
Kcp Int
k') (Int -> Scg
Scg Int
s') (Int -> Delta
Delta Int
d') Len
len
  where
    H.HonestRecipe (Kcp Int
k) (Scg Int
s) (Delta Int
d) Len
len = HonestRecipe
recipe

    (Int
k', Int
s', Int
d') = case HonestMutation
mut of
        HonestMutation
HonestMutateKcp -> (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Int
s,     Int
d    )
        HonestMutation
HonestMutateScg -> (Int
k,     Int
s Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1, Int
d    )

instance QC.Arbitrary TestHonestMutation where
    arbitrary :: Gen TestHonestMutation
arbitrary = (Int -> Gen TestHonestMutation) -> Gen TestHonestMutation
forall a. (Int -> Gen a) -> Gen a
sized1 ((Int -> Gen TestHonestMutation) -> Gen TestHonestMutation)
-> (Int -> Gen TestHonestMutation) -> Gen TestHonestMutation
forall a b. (a -> b) -> a -> b
$ \Int
sz -> Gen (Maybe TestHonestMutation) -> Gen TestHonestMutation
forall a. Gen (Maybe a) -> Gen a
unsafeMapSuchThatJust (Gen (Maybe TestHonestMutation) -> Gen TestHonestMutation)
-> Gen (Maybe TestHonestMutation) -> Gen TestHonestMutation
forall a b. (a -> b) -> a -> b
$ do
        (kcp, Scg s, delta) <- Gen (Kcp, Scg, Delta)
genKSD
        l <- (+ s) <$> QC.choose (0, 5 * sz)

        let testRecipe = Kcp -> Scg -> Delta -> Len -> HonestRecipe
H.HonestRecipe Kcp
kcp (Int -> Scg
Scg Int
s) Delta
delta (Int -> Len
Len Int
l)

        testRecipe' <- case Exn.runExcept $ H.checkHonestRecipe testRecipe of
            Left NoSuchHonestChainSchema
e  -> TestName -> Gen SomeCheckedHonestRecipe
forall a. HasCallStack => TestName -> a
error (TestName -> Gen SomeCheckedHonestRecipe)
-> TestName -> Gen SomeCheckedHonestRecipe
forall a b. (a -> b) -> a -> b
$ TestName
"impossible! " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> (HonestRecipe, NoSuchHonestChainSchema) -> TestName
forall a. Show a => a -> TestName
show (HonestRecipe
testRecipe, NoSuchHonestChainSchema
e)
            Right SomeCheckedHonestRecipe
x -> SomeCheckedHonestRecipe -> Gen SomeCheckedHonestRecipe
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SomeCheckedHonestRecipe
x

        mut <- QC.elements [HonestMutateKcp, HonestMutateScg]

        pure $ case Exn.runExcept $ H.checkHonestRecipe $ mutateHonest testRecipe mut of
            Left{}  -> Maybe TestHonestMutation
forall a. Maybe a
Nothing
            Right{} -> TestHonestMutation -> Maybe TestHonestMutation
forall a. a -> Maybe a
Just (TestHonestMutation -> Maybe TestHonestMutation)
-> TestHonestMutation -> Maybe TestHonestMutation
forall a b. (a -> b) -> a -> b
$ HonestRecipe
-> SomeCheckedHonestRecipe -> HonestMutation -> TestHonestMutation
TestHonestMutation HonestRecipe
testRecipe SomeCheckedHonestRecipe
testRecipe' HonestMutation
mut

-- | There exists a seed such that each 'TestHonestMutation' causes
-- 'H.checkHonestChain' to reject the result of 'H.uniformTheHonestChain'
prop_honestChainMutation :: TestHonestMutation -> QCGen -> QC.Property
prop_honestChainMutation :: TestHonestMutation -> QCGen -> Property
prop_honestChainMutation TestHonestMutation
testHonestMut QCGen
testSeedsSeed0 = IO Bool -> Property
forall prop. Testable prop => IO prop -> Property
QC.ioProperty (IO Bool -> Property) -> IO Bool -> Property
forall a b. (a -> b) -> a -> b
$ do
    H.SomeCheckedHonestRecipe Proxy Proxy recipe' <- SomeCheckedHonestRecipe -> IO SomeCheckedHonestRecipe
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SomeCheckedHonestRecipe
someRecipe'

    -- we're willing to wait up to 500ms to find a failure for each 'TestHonestMutation'
    IO.timeout
        (5 * 10^(5::Int))
        (IO.evaluate $ go recipe' testSeedsSeed0) <&> \case
            Maybe Bool
Nothing   -> Bool
False   -- did not find a failure caused by the mutation
            Just Bool
bool -> Bool
bool
  where
    TestHonestMutation HonestRecipe
recipe SomeCheckedHonestRecipe
someRecipe' HonestMutation
mut = TestHonestMutation
testHonestMut

    mutatedRecipe :: HonestRecipe
mutatedRecipe = HonestRecipe -> HonestMutation -> HonestRecipe
mutateHonest HonestRecipe
recipe HonestMutation
mut

    go :: CheckedHonestRecipe base hon -> QCGen -> Bool
go CheckedHonestRecipe base hon
recipe' QCGen
testSeedsSeed =
        let -- TODO is this a low quality random stream? Why is there no @'R.Random' 'QCGen'@ instance?
            (QCGen
testSeed, QCGen
testSeedsSeed') = QCGen -> (QCGen, QCGen)
forall g. RandomGen g => g -> (g, g)
R.split QCGen
testSeedsSeed

            sched :: ChainSchema base hon
sched = Maybe Asc
-> CheckedHonestRecipe base hon -> QCGen -> ChainSchema base hon
forall base hon g.
RandomGen g =>
Maybe Asc
-> CheckedHonestRecipe base hon -> g -> ChainSchema base hon
H.uniformTheHonestChain Maybe Asc
forall a. Maybe a
Nothing CheckedHonestRecipe base hon
recipe' (QCGen
testSeed :: QCGen)
            m :: Except (HonestChainViolation hon) ()
m     = HonestRecipe
-> ChainSchema base hon -> Except (HonestChainViolation hon) ()
forall base hon.
HonestRecipe
-> ChainSchema base hon -> Except (HonestChainViolation hon) ()
H.checkHonestChain HonestRecipe
mutatedRecipe ChainSchema base hon
sched
        in
        case Except (HonestChainViolation hon) ()
-> Either (HonestChainViolation hon) ()
forall e a. Except e a -> Either e a
Exn.runExcept Except (HonestChainViolation hon) ()
m of
            Right () -> CheckedHonestRecipe base hon -> QCGen -> Bool
go CheckedHonestRecipe base hon
recipe' QCGen
testSeedsSeed'
            Left HonestChainViolation hon
e   -> case HonestChainViolation hon
e of
                H.BadCount{}     -> TestName -> Bool
forall a. HasCallStack => TestName -> a
error (TestName -> Bool) -> TestName -> Bool
forall a b. (a -> b) -> a -> b
$ TestName
"impossible! " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> HonestChainViolation hon -> TestName
forall a. Show a => a -> TestName
show HonestChainViolation hon
e
                H.BadScgWindow{} -> Bool
True
                H.BadLength{}    -> TestName -> Bool
forall a. HasCallStack => TestName -> a
error (TestName -> Bool) -> TestName -> Bool
forall a b. (a -> b) -> a -> b
$ TestName
"impossible! " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> HonestChainViolation hon -> TestName
forall a. Show a => a -> TestName
show HonestChainViolation hon
e