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