{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE TypeApplications #-}

#if __GLASGOW_HASKELL__ >= 908
{-# OPTIONS_GHC -Wno-x-partial         #-}
#endif

module Test.Ouroboros.Consensus.ChainGenerator.Tests.Adversarial (
    SomeTestAdversarial (..)
  , TestAdversarial (..)
  , tests
  ) where

import           Control.Applicative ((<|>))
import qualified Control.Monad.Except as Exn
import           Data.Functor ((<&>))
import           Data.Functor.Identity (runIdentity)
import           Data.IORef (modifyIORef', newIORef, readIORef, writeIORef)
import           Data.Proxy (Proxy (Proxy))
import qualified System.Random as R
import qualified System.Timeout as IO (timeout)
import qualified Test.Ouroboros.Consensus.ChainGenerator.Adversarial as A
import           Test.Ouroboros.Consensus.ChainGenerator.Adversarial
                     (genPrefixBlockCount)
import qualified Test.Ouroboros.Consensus.ChainGenerator.BitVector as BV
import qualified Test.Ouroboros.Consensus.ChainGenerator.Counting as C
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)
import qualified Test.Ouroboros.Consensus.ChainGenerator.RaceIterator as RI
import qualified Test.Ouroboros.Consensus.ChainGenerator.Slot as S
import           Test.Ouroboros.Consensus.ChainGenerator.Slot (E (SlotE))
import qualified Test.Ouroboros.Consensus.ChainGenerator.Some as Some
import qualified Test.Ouroboros.Consensus.ChainGenerator.Tests.Honest as H
import qualified Test.QuickCheck as QC
import           Test.QuickCheck.Extras (unsafeMapSuchThatJust)
import           Test.QuickCheck.Random (QCGen)
import qualified Test.Tasty as TT
import qualified Test.Tasty.QuickCheck as TT
import qualified Test.Util.QuickCheck as QC

-----

tests :: [TT.TestTree]
tests :: [TestTree]
tests = [
    TestName -> (SomeTestAdversarial -> QCGen -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
TT.testProperty TestName
"k+1 blocks after the intersection" SomeTestAdversarial -> QCGen -> Property
prop_kPlus1BlocksAfterIntersection
  ,
    TestName -> (SomeTestAdversarial -> QCGen -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
TT.testProperty TestName
"Adversarial chains lose density and race comparisons" SomeTestAdversarial -> QCGen -> Property
prop_adversarialChain
  ,
    QuickCheckMaxSize -> TestTree -> TestTree
forall v. IsOption v => v -> TestTree -> TestTree
TT.localOption (Int -> QuickCheckMaxSize
TT.QuickCheckMaxSize Int
6) (TestTree -> TestTree) -> TestTree -> TestTree
forall a b. (a -> b) -> a -> b
$ TestName
-> (SomeTestAdversarialMutation -> QCGen -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
TT.testProperty TestName
"Adversarial chains win if checked with relaxed parameters" SomeTestAdversarialMutation -> QCGen -> Property
prop_adversarialChainMutation
  ]

-----

data SomeTestAdversarial =
    forall base hon.
    SomeTestAdversarial
        !(Proxy base)
        !(Proxy hon)
        !(TestAdversarial base hon)

instance Show SomeTestAdversarial where
    showsPrec :: Int -> SomeTestAdversarial -> ShowS
showsPrec Int
p (SomeTestAdversarial Proxy base
base Proxy hon
hon TestAdversarial base hon
test) =
        Int -> ShowBuilder SomeTestAdversarial -> ShowS
forall a.
NoFun "runShowsPrec" a (AbsError "runShowsPrec" a) =>
Int -> ShowBuilder a -> ShowS
Some.runShowsPrec Int
p
      (ShowBuilder SomeTestAdversarial -> ShowS)
-> ShowBuilder SomeTestAdversarial -> ShowS
forall a b. (a -> b) -> a -> b
$ (Proxy base
 -> Proxy hon -> TestAdversarial base hon -> SomeTestAdversarial)
-> TestName
-> ShowBuilder
     (Proxy base
      -> Proxy hon -> TestAdversarial base hon -> SomeTestAdversarial)
forall a. a -> TestName -> ShowBuilder a
Some.showCtor Proxy base
-> Proxy hon -> TestAdversarial base hon -> SomeTestAdversarial
forall base hon.
Proxy base
-> Proxy hon -> TestAdversarial base hon -> SomeTestAdversarial
SomeTestAdversarial TestName
"SomeTestAdversarial"
            ShowBuilder
  (Proxy base
   -> Proxy hon -> TestAdversarial base hon -> SomeTestAdversarial)
-> Proxy base
-> ShowBuilder
     (Proxy hon -> TestAdversarial base hon -> SomeTestAdversarial)
forall a b. Show a => ShowBuilder (a -> b) -> a -> ShowBuilder b
`Some.showArg` Proxy base
base
            ShowBuilder
  (Proxy hon -> TestAdversarial base hon -> SomeTestAdversarial)
-> Proxy hon
-> ShowBuilder (TestAdversarial base hon -> SomeTestAdversarial)
forall a b. Show a => ShowBuilder (a -> b) -> a -> ShowBuilder b
`Some.showArg` Proxy hon
hon
            ShowBuilder (TestAdversarial base hon -> SomeTestAdversarial)
-> TestAdversarial base hon -> ShowBuilder SomeTestAdversarial
forall a b. Show a => ShowBuilder (a -> b) -> a -> ShowBuilder b
`Some.showArg` TestAdversarial base hon
test

instance Read SomeTestAdversarial where
    readPrec :: ReadPrec SomeTestAdversarial
readPrec =
        ReadBuilder SomeTestAdversarial -> ReadPrec SomeTestAdversarial
forall a.
NoFun "runReadPrec" a (AbsError "runReadPrec" a) =>
ReadBuilder a -> ReadPrec a
Some.runReadPrec
      (ReadBuilder SomeTestAdversarial -> ReadPrec SomeTestAdversarial)
-> ReadBuilder SomeTestAdversarial -> ReadPrec SomeTestAdversarial
forall a b. (a -> b) -> a -> b
$ (Proxy Any
 -> Proxy Any -> TestAdversarial Any Any -> SomeTestAdversarial)
-> TestName
-> ReadBuilder
     (Proxy Any
      -> Proxy Any -> TestAdversarial Any Any -> SomeTestAdversarial)
forall a. a -> TestName -> ReadBuilder a
Some.readCtor Proxy Any
-> Proxy Any -> TestAdversarial Any Any -> SomeTestAdversarial
forall base hon.
Proxy base
-> Proxy hon -> TestAdversarial base hon -> SomeTestAdversarial
SomeTestAdversarial TestName
"SomeTestAdversarial"
            ReadBuilder
  (Proxy Any
   -> Proxy Any -> TestAdversarial Any Any -> SomeTestAdversarial)
-> ReadBuilder (Proxy Any)
-> ReadBuilder
     (Proxy Any -> TestAdversarial Any Any -> SomeTestAdversarial)
forall a b. ReadBuilder (a -> b) -> ReadBuilder a -> ReadBuilder b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReadBuilder (Proxy Any)
forall a. Read a => ReadBuilder a
Some.readArg
            ReadBuilder
  (Proxy Any -> TestAdversarial Any Any -> SomeTestAdversarial)
-> ReadBuilder (Proxy Any)
-> ReadBuilder (TestAdversarial Any Any -> SomeTestAdversarial)
forall a b. ReadBuilder (a -> b) -> ReadBuilder a -> ReadBuilder b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReadBuilder (Proxy Any)
forall a. Read a => ReadBuilder a
Some.readArg
            ReadBuilder (TestAdversarial Any Any -> SomeTestAdversarial)
-> ReadBuilder (TestAdversarial Any Any)
-> ReadBuilder SomeTestAdversarial
forall a b. ReadBuilder (a -> b) -> ReadBuilder a -> ReadBuilder b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReadBuilder (TestAdversarial Any Any)
forall a. Read a => ReadBuilder a
Some.readArg

data TestAdversarial base hon = TestAdversarial {
    forall base hon. TestAdversarial base hon -> Asc
testAscA     :: !Asc
  ,
    forall base hon. TestAdversarial base hon -> Asc
testAscH     :: !Asc
  ,
    forall base hon.
TestAdversarial base hon -> AdversarialRecipe base hon
testRecipeA  :: !(A.AdversarialRecipe base hon)
  ,
    forall base hon.
TestAdversarial base hon -> SomeCheckedAdversarialRecipe base hon
testRecipeA' :: !(A.SomeCheckedAdversarialRecipe base hon)
  ,
    forall base hon. TestAdversarial base hon -> HonestRecipe
testRecipeH  :: !H.HonestRecipe
  ,
    forall base hon.
TestAdversarial base hon -> CheckedHonestRecipe base hon
testRecipeH' :: !(H.CheckedHonestRecipe base hon)
  ,
    forall base hon. TestAdversarial base hon -> QCGen
testSeedH    :: !QCGen
  }
  deriving (ReadPrec [TestAdversarial base hon]
ReadPrec (TestAdversarial base hon)
Int -> ReadS (TestAdversarial base hon)
ReadS [TestAdversarial base hon]
(Int -> ReadS (TestAdversarial base hon))
-> ReadS [TestAdversarial base hon]
-> ReadPrec (TestAdversarial base hon)
-> ReadPrec [TestAdversarial base hon]
-> Read (TestAdversarial base hon)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall base hon. ReadPrec [TestAdversarial base hon]
forall base hon. ReadPrec (TestAdversarial base hon)
forall base hon. Int -> ReadS (TestAdversarial base hon)
forall base hon. ReadS [TestAdversarial base hon]
$creadsPrec :: forall base hon. Int -> ReadS (TestAdversarial base hon)
readsPrec :: Int -> ReadS (TestAdversarial base hon)
$creadList :: forall base hon. ReadS [TestAdversarial base hon]
readList :: ReadS [TestAdversarial base hon]
$creadPrec :: forall base hon. ReadPrec (TestAdversarial base hon)
readPrec :: ReadPrec (TestAdversarial base hon)
$creadListPrec :: forall base hon. ReadPrec [TestAdversarial base hon]
readListPrec :: ReadPrec [TestAdversarial base hon]
Read, Int -> TestAdversarial base hon -> ShowS
[TestAdversarial base hon] -> ShowS
TestAdversarial base hon -> TestName
(Int -> TestAdversarial base hon -> ShowS)
-> (TestAdversarial base hon -> TestName)
-> ([TestAdversarial base hon] -> ShowS)
-> Show (TestAdversarial base hon)
forall a.
(Int -> a -> ShowS) -> (a -> TestName) -> ([a] -> ShowS) -> Show a
forall base hon. Int -> TestAdversarial base hon -> ShowS
forall base hon. [TestAdversarial base hon] -> ShowS
forall base hon. TestAdversarial base hon -> TestName
$cshowsPrec :: forall base hon. Int -> TestAdversarial base hon -> ShowS
showsPrec :: Int -> TestAdversarial base hon -> ShowS
$cshow :: forall base hon. TestAdversarial base hon -> TestName
show :: TestAdversarial base hon -> TestName
$cshowList :: forall base hon. [TestAdversarial base hon] -> ShowS
showList :: [TestAdversarial base hon] -> ShowS
Show)

instance QC.Arbitrary SomeTestAdversarial where
    arbitrary :: Gen SomeTestAdversarial
arbitrary = Gen (Maybe SomeTestAdversarial) -> Gen SomeTestAdversarial
forall a. Gen (Maybe a) -> Gen a
unsafeMapSuchThatJust (Gen (Maybe SomeTestAdversarial) -> Gen SomeTestAdversarial)
-> Gen (Maybe SomeTestAdversarial) -> Gen SomeTestAdversarial
forall a b. (a -> b) -> a -> b
$ do
        H.TestHonest {
            H.testAsc     = testAscH
          ,
            H.testRecipe  = testRecipeH
          ,
            H.testRecipe' = someTestRecipeH'
          } <- Gen TestHonest
forall a. Arbitrary a => Gen a
QC.arbitrary

        H.SomeCheckedHonestRecipe Proxy Proxy testRecipeH' <- pure someTestRecipeH'

        testSeedH <- QC.arbitrary

        let arHonest = 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
testAscH) CheckedHonestRecipe base hon
testRecipeH' QCGen
testSeedH

        testSeedPrefix <- QC.arbitrary @QCGen

        let arPrefix = HonestRecipe
-> QCGen -> ChainSchema base hon -> Var hon 'ActiveSlotE
forall g base hon.
RandomGen g =>
HonestRecipe -> g -> ChainSchema base hon -> Var hon 'ActiveSlotE
genPrefixBlockCount HonestRecipe
testRecipeH QCGen
testSeedPrefix ChainSchema base hon
arHonest

            H.HonestRecipe kcp scg delta _len = testRecipeH

            testRecipeA = A.AdversarialRecipe {
                Var hon 'ActiveSlotE
arPrefix :: Var hon 'ActiveSlotE
arPrefix :: Var hon 'ActiveSlotE
A.arPrefix
              ,
                arParams :: (Kcp, Scg, Delta)
A.arParams = (Kcp
kcp, Scg
scg, Delta
delta)
              ,
                ChainSchema base hon
arHonest :: ChainSchema base hon
arHonest :: ChainSchema base hon
A.arHonest
              }

        testAscA <- genAsc

        case Exn.runExcept $ A.checkAdversarialRecipe testRecipeA of
            Left NoSuchAdversarialChainSchema
e -> case NoSuchAdversarialChainSchema
e of
                NoSuchAdversarialChainSchema
A.NoSuchAdversarialBlock -> Maybe SomeTestAdversarial -> Gen (Maybe SomeTestAdversarial)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe SomeTestAdversarial
forall a. Maybe a
Nothing
                NoSuchAdversarialChainSchema
A.NoSuchCompetitor       -> TestName -> Gen (Maybe SomeTestAdversarial)
forall a. HasCallStack => TestName -> a
error (TestName -> Gen (Maybe SomeTestAdversarial))
-> TestName -> Gen (Maybe SomeTestAdversarial)
forall a b. (a -> b) -> a -> b
$ TestName
"impossible! " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> NoSuchAdversarialChainSchema -> TestName
forall a. Show a => a -> TestName
show NoSuchAdversarialChainSchema
e
                NoSuchAdversarialChainSchema
A.NoSuchIntersection     -> TestName -> Gen (Maybe SomeTestAdversarial)
forall a. HasCallStack => TestName -> a
error (TestName -> Gen (Maybe SomeTestAdversarial))
-> TestName -> Gen (Maybe SomeTestAdversarial)
forall a b. (a -> b) -> a -> b
$ TestName
"impossible! " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> NoSuchAdversarialChainSchema -> TestName
forall a. Show a => a -> TestName
show NoSuchAdversarialChainSchema
e

            Right SomeCheckedAdversarialRecipe base hon
testRecipeA' -> do
                Maybe SomeTestAdversarial -> Gen (Maybe SomeTestAdversarial)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe SomeTestAdversarial -> Gen (Maybe SomeTestAdversarial))
-> Maybe SomeTestAdversarial -> Gen (Maybe SomeTestAdversarial)
forall a b. (a -> b) -> a -> b
$ SomeTestAdversarial -> Maybe SomeTestAdversarial
forall a. a -> Maybe a
Just (SomeTestAdversarial -> Maybe SomeTestAdversarial)
-> SomeTestAdversarial -> Maybe SomeTestAdversarial
forall a b. (a -> b) -> a -> b
$ Proxy base
-> Proxy hon -> TestAdversarial base hon -> SomeTestAdversarial
forall base hon.
Proxy base
-> Proxy hon -> TestAdversarial base hon -> SomeTestAdversarial
SomeTestAdversarial Proxy base
forall {k} (t :: k). Proxy t
Proxy Proxy hon
forall {k} (t :: k). Proxy t
Proxy (TestAdversarial base hon -> SomeTestAdversarial)
-> TestAdversarial base hon -> SomeTestAdversarial
forall a b. (a -> b) -> a -> b
$ TestAdversarial {
                    Asc
testAscA :: Asc
testAscA :: Asc
testAscA
                  ,
                    Asc
testAscH :: Asc
testAscH :: Asc
testAscH
                  ,
                    AdversarialRecipe base hon
testRecipeA :: AdversarialRecipe base hon
testRecipeA :: AdversarialRecipe base hon
testRecipeA
                  ,
                    SomeCheckedAdversarialRecipe base hon
testRecipeA' :: SomeCheckedAdversarialRecipe base hon
testRecipeA' :: SomeCheckedAdversarialRecipe base hon
testRecipeA'
                  ,
                    HonestRecipe
testRecipeH :: HonestRecipe
testRecipeH :: HonestRecipe
testRecipeH
                  ,
                    CheckedHonestRecipe base hon
testRecipeH' :: CheckedHonestRecipe base hon
testRecipeH' :: CheckedHonestRecipe base hon
testRecipeH'
                  ,
                    QCGen
testSeedH :: QCGen
testSeedH :: QCGen
testSeedH
                  }

-- | Both the honest and the alternative schema have k+1 blocks after the
-- intersection.
prop_kPlus1BlocksAfterIntersection :: SomeTestAdversarial -> QCGen -> QC.Property
prop_kPlus1BlocksAfterIntersection :: SomeTestAdversarial -> QCGen -> Property
prop_kPlus1BlocksAfterIntersection SomeTestAdversarial
someTestAdversarial QCGen
testSeedA = Identity Property -> Property
forall a. Identity a -> a
runIdentity (Identity Property -> Property) -> Identity Property -> Property
forall a b. (a -> b) -> a -> b
$ do
    SomeTestAdversarial Proxy Proxy TestAdversarial {
        testAscA
      ,
        testRecipeA
      ,
        testRecipeA'
      } <- SomeTestAdversarial -> Identity SomeTestAdversarial
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SomeTestAdversarial
someTestAdversarial
    A.SomeCheckedAdversarialRecipe Proxy recipeA' <- pure testRecipeA'

    let A.AdversarialRecipe { A.arHonest = schedH } = testRecipeA
        schedA = Maybe Asc
-> CheckedAdversarialRecipe base hon adv
-> QCGen
-> ChainSchema base adv
forall g base hon adv.
RandomGen g =>
Maybe Asc
-> CheckedAdversarialRecipe base hon adv
-> g
-> ChainSchema base adv
A.uniformAdversarialChain (Asc -> Maybe Asc
forall a. a -> Maybe a
Just Asc
testAscA) CheckedAdversarialRecipe base hon adv
recipeA' QCGen
testSeedA
        H.ChainSchema winA vA = schedA
        H.ChainSchema _winH vH = schedH
        A.AdversarialRecipe { A.arParams = (Kcp k, scg, _delta) } = testRecipeA

    C.SomeWindow Proxy stabWin <- do
        pure $ calculateStability scg schedA

    pure $
      QC.counterexample (unlines $
                            H.prettyChainSchema schedH "H"
                            ++ H.prettyChainSchema schedA "A"
                          )
      $ QC.counterexample ("arPrefix = " <> show (A.arPrefix testRecipeA))
      $ QC.counterexample ("stabWin  = " <> show stabWin)
      $ QC.counterexample ("stabWin' = " <> show (C.joinWin winA stabWin))
      $ QC.counterexample ("The honest chain should have k+1 blocks after the intersection")
          (BV.countActivesInV S.notInverted vH
            `QC.ge` C.toSize (C.Count (k + 1) + A.arPrefix testRecipeA)
          )
        QC..&&.
          QC.counterexample ("The alternative chain should have k+1 blocks after the intersection")
            (BV.countActivesInV S.notInverted vA `QC.ge` C.Count (k + 1))

-- | No seed exists such that each 'A.checkAdversarialChain' rejects the result of 'A.uniformAdversarialChain'
prop_adversarialChain :: SomeTestAdversarial -> QCGen -> QC.Property
prop_adversarialChain :: SomeTestAdversarial -> QCGen -> Property
prop_adversarialChain SomeTestAdversarial
someTestAdversarial QCGen
testSeedA = Identity Property -> Property
forall a. Identity a -> a
runIdentity (Identity Property -> Property) -> Identity Property -> Property
forall a b. (a -> b) -> a -> b
$ do
    SomeTestAdversarial Proxy Proxy TestAdversarial {
        testAscA
      ,
        testRecipeA
      ,
        testRecipeA'
      } <- SomeTestAdversarial -> Identity SomeTestAdversarial
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SomeTestAdversarial
someTestAdversarial
    A.SomeCheckedAdversarialRecipe Proxy recipeA' <- pure testRecipeA'

    let A.AdversarialRecipe { A.arHonest = schedH } = testRecipeA

        schedA = Maybe Asc
-> CheckedAdversarialRecipe base hon adv
-> QCGen
-> ChainSchema base adv
forall g base hon adv.
RandomGen g =>
Maybe Asc
-> CheckedAdversarialRecipe base hon adv
-> g
-> ChainSchema base adv
A.uniformAdversarialChain (Asc -> Maybe Asc
forall a. a -> Maybe a
Just Asc
testAscA) CheckedAdversarialRecipe base hon adv
recipeA' QCGen
testSeedA

    let H.ChainSchema winA _vA = schedA

    C.SomeWindow Proxy stabWin <- do
        let A.AdversarialRecipe { A.arParams = (_kcp, scg, _delta) } = testRecipeA
        pure $ calculateStability scg schedA

    pure $ case Exn.runExcept $ A.checkAdversarialChain testRecipeA schedA of
        Right () -> () -> Property
forall prop. Testable prop => prop -> Property
QC.property ()
        Left AdversarialViolation hon adv
e   -> case AdversarialViolation hon adv
e of
            A.BadAnchor{} -> TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (AdversarialViolation hon adv -> TestName
forall a. Show a => a -> TestName
show AdversarialViolation hon adv
e) Bool
False
            A.BadCount{}  -> TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (AdversarialViolation hon adv -> TestName
forall a. Show a => a -> TestName
show AdversarialViolation hon adv
e) Bool
False
            A.BadDensity{}  -> TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (AdversarialViolation hon adv -> TestName
forall a. Show a => a -> TestName
show AdversarialViolation hon adv
e) Bool
False
            A.BadRace RaceViolation hon adv
rv  -> case RaceViolation hon adv
rv of
                A.AdversaryWonRace {
                    rvAdv :: forall hon adv. RaceViolation hon adv -> Race adv
A.rvAdv = RI.Race (C.SomeWindow Proxy skolem
Proxy Contains 'SlotE adv (Win RaceLbl skolem)
rAdv)
                  ,
                    rvHon :: forall hon adv. RaceViolation hon adv -> Race hon
A.rvHon = RI.Race (C.SomeWindow Proxy skolem
Proxy Contains 'SlotE hon (Win RaceLbl skolem)
rHon)
                  } -> 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 (ChainSchema base hon
-> ChainSchema base adv
-> Contains 'SlotE base adv
-> Contains 'SlotE adv (Win AdvStabLbl skolem)
-> RaceViolation hon adv
-> TestName
forall base hon adv stab.
ChainSchema base hon
-> ChainSchema base adv
-> Contains 'SlotE base adv
-> Contains 'SlotE adv stab
-> RaceViolation hon adv
-> TestName
advCounterexample ChainSchema base hon
schedH ChainSchema base adv
schedA Contains 'SlotE base adv
winA Contains 'SlotE adv (Win AdvStabLbl skolem)
stabWin RaceViolation hon adv
rv)
                    (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (TestName
"arPrefix = " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> Var hon 'ActiveSlotE -> TestName
forall a. Show a => a -> TestName
show (AdversarialRecipe base hon -> Var hon 'ActiveSlotE
forall base hon. AdversarialRecipe base hon -> Var hon 'ActiveSlotE
A.arPrefix AdversarialRecipe base hon
testRecipeA))
                    (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (TestName
"rvAdv    = " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> Contains 'SlotE adv (Win RaceLbl skolem) -> TestName
forall a. Show a => a -> TestName
show Contains 'SlotE adv (Win RaceLbl skolem)
rAdv)
                    (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (TestName
"rvAdv'   = " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> Contains 'SlotE base (Win RaceLbl skolem) -> TestName
forall a. Show a => a -> TestName
show (Contains 'SlotE base adv
-> Contains 'SlotE adv (Win RaceLbl skolem)
-> Contains 'SlotE base (Win RaceLbl skolem)
forall {kelem} (elem :: kelem) outer mid inner.
Contains elem outer mid
-> Contains elem mid inner -> Contains elem outer inner
C.joinWin Contains 'SlotE base adv
winA Contains 'SlotE adv (Win RaceLbl skolem)
rAdv))
                    (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (TestName
"rvHon    = " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> Contains 'SlotE hon (Win RaceLbl skolem) -> TestName
forall a. Show a => a -> TestName
show Contains 'SlotE hon (Win RaceLbl skolem)
rHon)
                    (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (TestName
"stabWin  = " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> Contains 'SlotE adv (Win AdvStabLbl skolem) -> TestName
forall a. Show a => a -> TestName
show Contains 'SlotE adv (Win AdvStabLbl skolem)
stabWin)
                    (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (TestName
"stabWin' = " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> Contains 'SlotE base (Win AdvStabLbl skolem) -> TestName
forall a. Show a => a -> TestName
show (Contains 'SlotE base adv
-> Contains 'SlotE adv (Win AdvStabLbl skolem)
-> Contains 'SlotE base (Win AdvStabLbl skolem)
forall {kelem} (elem :: kelem) outer mid inner.
Contains elem outer mid
-> Contains elem mid inner -> Contains elem outer inner
C.joinWin Contains 'SlotE base adv
winA Contains 'SlotE adv (Win AdvStabLbl skolem)
stabWin))
                    (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (AdversarialViolation hon adv -> TestName
forall a. Show a => a -> TestName
show AdversarialViolation hon adv
e)
                    (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ Bool
False

data AdvStabLbl

-- | Calculate the interval in which the adversary can not yet have accelerated
calculateStability :: Scg -> H.ChainSchema base adv -> C.SomeWindow AdvStabLbl adv SlotE
calculateStability :: forall base adv.
Scg -> ChainSchema base adv -> SomeWindow AdvStabLbl adv 'SlotE
calculateStability (Scg Int
s) ChainSchema base adv
schedA =
    Size adv 'SlotE
-> Lbl AdvStabLbl
-> Index adv 'SlotE
-> Size Any 'SlotE
-> SomeWindow AdvStabLbl adv 'SlotE
forall {kelem} {klbl} outer (elem :: kelem) (lbl :: klbl) x.
Size outer elem
-> Lbl lbl
-> Index outer elem
-> Size x elem
-> SomeWindow lbl outer elem
C.withWindow (Contains 'SlotE base adv -> Size adv 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Size inner elem
C.windowSize Contains 'SlotE base adv
winA) (forall lbl. Lbl lbl
forall {k} (lbl :: k). Lbl lbl
C.Lbl @AdvStabLbl) (Int -> Index adv 'SlotE
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
0) (Int -> Size Any 'SlotE
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count (Int -> Size Any 'SlotE) -> Int -> Size Any 'SlotE
forall a b. (a -> b) -> a -> b
$ Int
firstActive Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
theBlockItself Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
s)
  where
    H.ChainSchema Contains 'SlotE base adv
winA Vector adv 'SlotE S
vA = ChainSchema base adv
schedA

    C.Count Int
firstActive = case Proxy 'Inverted
-> Vector adv 'SlotE S
-> Index adv (PreImage 'Inverted 'EmptySlotE)
-> MaybeFound adv
forall (pol :: Pol) (proxy :: Pol -> *) base.
POL pol =>
proxy pol
-> Vector base 'SlotE S
-> Index base (PreImage pol 'EmptySlotE)
-> MaybeFound base
BV.findIthEmptyInV Proxy 'Inverted
S.inverted Vector adv 'SlotE S
vA (Int -> Count adv 'ActiveSlotE Preds
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
0) of
            BV.JustFound Index adv 'SlotE
x  -> Index adv 'SlotE
x
            MaybeFound adv
BV.NothingFound -> TestName -> Index adv 'SlotE
forall a. HasCallStack => TestName -> a
error (TestName -> Index adv 'SlotE) -> TestName -> Index adv 'SlotE
forall a b. (a -> b) -> a -> b
$ TestName
"impossible! " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> [TestName] -> TestName
H.unlines' (ChainSchema base adv -> TestName -> [TestName]
forall base inner. ChainSchema base inner -> TestName -> [TestName]
H.prettyChainSchema ChainSchema base adv
schedA TestName
"A")
    theBlockItself :: Int
theBlockItself = Int
1

-- | A nice rendering for failures of 'prop_adversarialChain'
advCounterexample ::
     A.ChainSchema base hon
  -> A.ChainSchema base adv
  -> C.Contains 'SlotE base adv
  -> C.Contains 'SlotE adv stab
  -> A.RaceViolation hon adv
  -> String
advCounterexample :: forall base hon adv stab.
ChainSchema base hon
-> ChainSchema base adv
-> Contains 'SlotE base adv
-> Contains 'SlotE adv stab
-> RaceViolation hon adv
-> TestName
advCounterexample ChainSchema base hon
schedH ChainSchema base adv
schedA Contains 'SlotE base adv
winA Contains 'SlotE adv stab
stabWin RaceViolation hon adv
rv =
    case RaceViolation hon adv
rv of
        A.AdversaryWonRace {
            rvAdv :: forall hon adv. RaceViolation hon adv -> Race adv
A.rvAdv = RI.Race (C.SomeWindow Proxy skolem
Proxy Contains 'SlotE adv (Win RaceLbl skolem)
rAdv)
          ,
            rvHon :: forall hon adv. RaceViolation hon adv -> Race hon
A.rvHon = RI.Race (C.SomeWindow Proxy skolem
Proxy Contains 'SlotE hon (Win RaceLbl skolem)
rHon)
          } ->
            [TestName] -> TestName
H.unlines' ([TestName] -> TestName) -> [TestName] -> TestName
forall a b. (a -> b) -> a -> b
$ []
             [TestName] -> [TestName] -> [TestName]
forall a. Semigroup a => a -> a -> a
<> [Contains 'SlotE hon (Win RaceLbl skolem) -> ShowS
forall base inner. Contains 'SlotE base inner -> ShowS
H.prettyWindow Contains 'SlotE hon (Win RaceLbl skolem)
rHon TestName
"rHon"]
             [TestName] -> [TestName] -> [TestName]
forall a. Semigroup a => a -> a -> a
<> [TestName] -> [TestName]
forall a. [a] -> [a]
reverse (ChainSchema base hon -> TestName -> [TestName]
forall base inner. ChainSchema base inner -> TestName -> [TestName]
H.prettyChainSchema ChainSchema base hon
schedH TestName
"H")
             [TestName] -> [TestName] -> [TestName]
forall a. Semigroup a => a -> a -> a
<> ChainSchema base adv -> TestName -> [TestName]
forall base inner. ChainSchema base inner -> TestName -> [TestName]
H.prettyChainSchema ChainSchema base adv
schedA TestName
"A"
             [TestName] -> [TestName] -> [TestName]
forall a. Semigroup a => a -> a -> a
<> [Contains 'SlotE base (Win RaceLbl skolem) -> ShowS
forall base inner. Contains 'SlotE base inner -> ShowS
H.prettyWindow (Contains 'SlotE base adv
-> Contains 'SlotE adv (Win RaceLbl skolem)
-> Contains 'SlotE base (Win RaceLbl skolem)
forall {kelem} (elem :: kelem) outer mid inner.
Contains elem outer mid
-> Contains elem mid inner -> Contains elem outer inner
C.joinWin Contains 'SlotE base adv
winA Contains 'SlotE adv (Win RaceLbl skolem)
rAdv) TestName
"rAdv'"]
             [TestName] -> [TestName] -> [TestName]
forall a. Semigroup a => a -> a -> a
<> [Contains 'SlotE base stab -> ShowS
forall base inner. Contains 'SlotE base inner -> ShowS
H.prettyWindow (Contains 'SlotE base adv
-> Contains 'SlotE adv stab -> Contains 'SlotE base stab
forall {kelem} (elem :: kelem) outer mid inner.
Contains elem outer mid
-> Contains elem mid inner -> Contains elem outer inner
C.joinWin Contains 'SlotE base adv
winA Contains 'SlotE adv stab
stabWin) TestName
"stabWin'"]

-----

-- | A mutation that causes some honest Race Windows to end one slot sooner
data AdversarialMutation =
    -- | Increasing 'Delta' by the given amount may cause the adversary to win a race
    AdversarialMutateDelta Int
  |
    -- | Decreasing 'Kcp' by one may cause the adversary to win a race
    AdversarialMutateKcp
{-
  |
    -- | Decreasing 'Scg' by one may case the adversary to win a (conservative) race
    AdversarialMutateScgNeg
  |
    -- | Increasing 'Scg' by one may case the adversary to accelerate prematurely
    AdversarialMutateScgPos
-}
  deriving (AdversarialMutation -> AdversarialMutation -> Bool
(AdversarialMutation -> AdversarialMutation -> Bool)
-> (AdversarialMutation -> AdversarialMutation -> Bool)
-> Eq AdversarialMutation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AdversarialMutation -> AdversarialMutation -> Bool
== :: AdversarialMutation -> AdversarialMutation -> Bool
$c/= :: AdversarialMutation -> AdversarialMutation -> Bool
/= :: AdversarialMutation -> AdversarialMutation -> Bool
Eq, ReadPrec [AdversarialMutation]
ReadPrec AdversarialMutation
Int -> ReadS AdversarialMutation
ReadS [AdversarialMutation]
(Int -> ReadS AdversarialMutation)
-> ReadS [AdversarialMutation]
-> ReadPrec AdversarialMutation
-> ReadPrec [AdversarialMutation]
-> Read AdversarialMutation
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS AdversarialMutation
readsPrec :: Int -> ReadS AdversarialMutation
$creadList :: ReadS [AdversarialMutation]
readList :: ReadS [AdversarialMutation]
$creadPrec :: ReadPrec AdversarialMutation
readPrec :: ReadPrec AdversarialMutation
$creadListPrec :: ReadPrec [AdversarialMutation]
readListPrec :: ReadPrec [AdversarialMutation]
Read, Int -> AdversarialMutation -> ShowS
[AdversarialMutation] -> ShowS
AdversarialMutation -> TestName
(Int -> AdversarialMutation -> ShowS)
-> (AdversarialMutation -> TestName)
-> ([AdversarialMutation] -> ShowS)
-> Show AdversarialMutation
forall a.
(Int -> a -> ShowS) -> (a -> TestName) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AdversarialMutation -> ShowS
showsPrec :: Int -> AdversarialMutation -> ShowS
$cshow :: AdversarialMutation -> TestName
show :: AdversarialMutation -> TestName
$cshowList :: [AdversarialMutation] -> ShowS
showList :: [AdversarialMutation] -> ShowS
Show)

data TestAdversarialMutation base hon =
    TestAdversarialMutation
        !H.HonestRecipe
        !(H.CheckedHonestRecipe          base hon)
        !(A.AdversarialRecipe            base hon)
        !(A.SomeCheckedAdversarialRecipe base hon)
        !AdversarialMutation
  deriving (ReadPrec [TestAdversarialMutation base hon]
ReadPrec (TestAdversarialMutation base hon)
Int -> ReadS (TestAdversarialMutation base hon)
ReadS [TestAdversarialMutation base hon]
(Int -> ReadS (TestAdversarialMutation base hon))
-> ReadS [TestAdversarialMutation base hon]
-> ReadPrec (TestAdversarialMutation base hon)
-> ReadPrec [TestAdversarialMutation base hon]
-> Read (TestAdversarialMutation base hon)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall base hon. ReadPrec [TestAdversarialMutation base hon]
forall base hon. ReadPrec (TestAdversarialMutation base hon)
forall base hon. Int -> ReadS (TestAdversarialMutation base hon)
forall base hon. ReadS [TestAdversarialMutation base hon]
$creadsPrec :: forall base hon. Int -> ReadS (TestAdversarialMutation base hon)
readsPrec :: Int -> ReadS (TestAdversarialMutation base hon)
$creadList :: forall base hon. ReadS [TestAdversarialMutation base hon]
readList :: ReadS [TestAdversarialMutation base hon]
$creadPrec :: forall base hon. ReadPrec (TestAdversarialMutation base hon)
readPrec :: ReadPrec (TestAdversarialMutation base hon)
$creadListPrec :: forall base hon. ReadPrec [TestAdversarialMutation base hon]
readListPrec :: ReadPrec [TestAdversarialMutation base hon]
Read, Int -> TestAdversarialMutation base hon -> ShowS
[TestAdversarialMutation base hon] -> ShowS
TestAdversarialMutation base hon -> TestName
(Int -> TestAdversarialMutation base hon -> ShowS)
-> (TestAdversarialMutation base hon -> TestName)
-> ([TestAdversarialMutation base hon] -> ShowS)
-> Show (TestAdversarialMutation base hon)
forall a.
(Int -> a -> ShowS) -> (a -> TestName) -> ([a] -> ShowS) -> Show a
forall base hon. Int -> TestAdversarialMutation base hon -> ShowS
forall base hon. [TestAdversarialMutation base hon] -> ShowS
forall base hon. TestAdversarialMutation base hon -> TestName
$cshowsPrec :: forall base hon. Int -> TestAdversarialMutation base hon -> ShowS
showsPrec :: Int -> TestAdversarialMutation base hon -> ShowS
$cshow :: forall base hon. TestAdversarialMutation base hon -> TestName
show :: TestAdversarialMutation base hon -> TestName
$cshowList :: forall base hon. [TestAdversarialMutation base hon] -> ShowS
showList :: [TestAdversarialMutation base hon] -> ShowS
Show)

data SomeTestAdversarialMutation =
    forall base hon.
    SomeTestAdversarialMutation
        !(Proxy base)
        !(Proxy hon)
        !(TestAdversarialMutation base hon)

instance Show SomeTestAdversarialMutation where
    showsPrec :: Int -> SomeTestAdversarialMutation -> ShowS
showsPrec Int
p (SomeTestAdversarialMutation Proxy base
base Proxy hon
hon TestAdversarialMutation base hon
testMut) =
        Int -> ShowBuilder SomeTestAdversarialMutation -> ShowS
forall a.
NoFun "runShowsPrec" a (AbsError "runShowsPrec" a) =>
Int -> ShowBuilder a -> ShowS
Some.runShowsPrec Int
p
      (ShowBuilder SomeTestAdversarialMutation -> ShowS)
-> ShowBuilder SomeTestAdversarialMutation -> ShowS
forall a b. (a -> b) -> a -> b
$ (Proxy base
 -> Proxy hon
 -> TestAdversarialMutation base hon
 -> SomeTestAdversarialMutation)
-> TestName
-> ShowBuilder
     (Proxy base
      -> Proxy hon
      -> TestAdversarialMutation base hon
      -> SomeTestAdversarialMutation)
forall a. a -> TestName -> ShowBuilder a
Some.showCtor Proxy base
-> Proxy hon
-> TestAdversarialMutation base hon
-> SomeTestAdversarialMutation
forall base hon.
Proxy base
-> Proxy hon
-> TestAdversarialMutation base hon
-> SomeTestAdversarialMutation
SomeTestAdversarialMutation TestName
"SomeTestAdversarialMutation"
            ShowBuilder
  (Proxy base
   -> Proxy hon
   -> TestAdversarialMutation base hon
   -> SomeTestAdversarialMutation)
-> Proxy base
-> ShowBuilder
     (Proxy hon
      -> TestAdversarialMutation base hon -> SomeTestAdversarialMutation)
forall a b. Show a => ShowBuilder (a -> b) -> a -> ShowBuilder b
`Some.showArg` Proxy base
base
            ShowBuilder
  (Proxy hon
   -> TestAdversarialMutation base hon -> SomeTestAdversarialMutation)
-> Proxy hon
-> ShowBuilder
     (TestAdversarialMutation base hon -> SomeTestAdversarialMutation)
forall a b. Show a => ShowBuilder (a -> b) -> a -> ShowBuilder b
`Some.showArg` Proxy hon
hon
            ShowBuilder
  (TestAdversarialMutation base hon -> SomeTestAdversarialMutation)
-> TestAdversarialMutation base hon
-> ShowBuilder SomeTestAdversarialMutation
forall a b. Show a => ShowBuilder (a -> b) -> a -> ShowBuilder b
`Some.showArg` TestAdversarialMutation base hon
testMut

instance Read SomeTestAdversarialMutation where
    readPrec :: ReadPrec SomeTestAdversarialMutation
readPrec =
        ReadBuilder SomeTestAdversarialMutation
-> ReadPrec SomeTestAdversarialMutation
forall a.
NoFun "runReadPrec" a (AbsError "runReadPrec" a) =>
ReadBuilder a -> ReadPrec a
Some.runReadPrec
      (ReadBuilder SomeTestAdversarialMutation
 -> ReadPrec SomeTestAdversarialMutation)
-> ReadBuilder SomeTestAdversarialMutation
-> ReadPrec SomeTestAdversarialMutation
forall a b. (a -> b) -> a -> b
$ (Proxy Any
 -> Proxy Any
 -> TestAdversarialMutation Any Any
 -> SomeTestAdversarialMutation)
-> TestName
-> ReadBuilder
     (Proxy Any
      -> Proxy Any
      -> TestAdversarialMutation Any Any
      -> SomeTestAdversarialMutation)
forall a. a -> TestName -> ReadBuilder a
Some.readCtor Proxy Any
-> Proxy Any
-> TestAdversarialMutation Any Any
-> SomeTestAdversarialMutation
forall base hon.
Proxy base
-> Proxy hon
-> TestAdversarialMutation base hon
-> SomeTestAdversarialMutation
SomeTestAdversarialMutation TestName
"SomeTestAdversarialMutation"
            ReadBuilder
  (Proxy Any
   -> Proxy Any
   -> TestAdversarialMutation Any Any
   -> SomeTestAdversarialMutation)
-> ReadBuilder (Proxy Any)
-> ReadBuilder
     (Proxy Any
      -> TestAdversarialMutation Any Any -> SomeTestAdversarialMutation)
forall a b. ReadBuilder (a -> b) -> ReadBuilder a -> ReadBuilder b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReadBuilder (Proxy Any)
forall a. Read a => ReadBuilder a
Some.readArg
            ReadBuilder
  (Proxy Any
   -> TestAdversarialMutation Any Any -> SomeTestAdversarialMutation)
-> ReadBuilder (Proxy Any)
-> ReadBuilder
     (TestAdversarialMutation Any Any -> SomeTestAdversarialMutation)
forall a b. ReadBuilder (a -> b) -> ReadBuilder a -> ReadBuilder b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReadBuilder (Proxy Any)
forall a. Read a => ReadBuilder a
Some.readArg
            ReadBuilder
  (TestAdversarialMutation Any Any -> SomeTestAdversarialMutation)
-> ReadBuilder (TestAdversarialMutation Any Any)
-> ReadBuilder SomeTestAdversarialMutation
forall a b. ReadBuilder (a -> b) -> ReadBuilder a -> ReadBuilder b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReadBuilder (TestAdversarialMutation Any Any)
forall a. Read a => ReadBuilder a
Some.readArg

mutateAdversarial :: A.AdversarialRecipe base hon -> AdversarialMutation -> A.AdversarialRecipe base hon
mutateAdversarial :: forall base hon.
AdversarialRecipe base hon
-> AdversarialMutation -> AdversarialRecipe base hon
mutateAdversarial AdversarialRecipe base hon
recipe AdversarialMutation
mut =
    A.AdversarialRecipe { ChainSchema base hon
arHonest :: ChainSchema base hon
arHonest :: ChainSchema base hon
A.arHonest, arParams :: (Kcp, Scg, Delta)
A.arParams = (Int -> Kcp
Kcp Int
k', Int -> Scg
Scg Int
s', Int -> Delta
Delta Int
d'), Var hon 'ActiveSlotE
arPrefix :: Var hon 'ActiveSlotE
arPrefix :: Var hon 'ActiveSlotE
A.arPrefix }
  where
    A.AdversarialRecipe { ChainSchema base hon
arHonest :: forall base hon. AdversarialRecipe base hon -> ChainSchema base hon
arHonest :: ChainSchema base hon
A.arHonest, arParams :: forall base hon. AdversarialRecipe base hon -> (Kcp, Scg, Delta)
A.arParams = (Kcp Int
k,  Scg Int
s,  Delta Int
d ), Var hon 'ActiveSlotE
arPrefix :: forall base hon. AdversarialRecipe base hon -> Var hon 'ActiveSlotE
arPrefix :: Var hon 'ActiveSlotE
A.arPrefix } = AdversarialRecipe base hon
recipe

    (Int
k', Int
s', Int
d') = case AdversarialMutation
mut of
        AdversarialMutateDelta Int
dInc -> (Int
k,     Int
s,     Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
dInc)
        AdversarialMutation
AdversarialMutateKcp        -> (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1, Int
s,     Int
d       )
--        AdversarialMutateScgNeg -> (k,     s - 1, d    )
--        AdversarialMutateScgPos -> (k,     s + 1, d    )

instance QC.Arbitrary SomeTestAdversarialMutation where
    arbitrary :: Gen SomeTestAdversarialMutation
arbitrary = do
        Gen (Maybe SomeTestAdversarialMutation)
-> Gen SomeTestAdversarialMutation
forall a. Gen (Maybe a) -> Gen a
unsafeMapSuchThatJust (Gen (Maybe SomeTestAdversarialMutation)
 -> Gen SomeTestAdversarialMutation)
-> Gen (Maybe SomeTestAdversarialMutation)
-> Gen SomeTestAdversarialMutation
forall a b. (a -> b) -> a -> b
$ do
            recipeH@(H.HonestRecipe kcp scg delta len) <- Gen HonestRecipe
H.genHonestRecipe

            someTestRecipeH' <- case Exn.runExcept $ H.checkHonestRecipe recipeH 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
recipeH, NoSuchHonestChainSchema
e)
                Right SomeCheckedHonestRecipe
x -> SomeCheckedHonestRecipe -> Gen SomeCheckedHonestRecipe
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SomeCheckedHonestRecipe
x

            H.SomeCheckedHonestRecipe Proxy Proxy recipeH' <- pure someTestRecipeH'

            seedH <- QC.arbitrary @QCGen

            let arHonest = 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
recipeH' QCGen
seedH

            testSeedPrefix <- QC.arbitrary @QCGen

            let arPrefix = HonestRecipe
-> QCGen -> ChainSchema base hon -> Var hon 'ActiveSlotE
forall g base hon.
RandomGen g =>
HonestRecipe -> g -> ChainSchema base hon -> Var hon 'ActiveSlotE
genPrefixBlockCount HonestRecipe
recipeH QCGen
testSeedPrefix ChainSchema base hon
arHonest

            let recipeA = A.AdversarialRecipe {
                    Var hon 'ActiveSlotE
arPrefix :: Var hon 'ActiveSlotE
arPrefix :: Var hon 'ActiveSlotE
A.arPrefix
                  ,
                    arParams :: (Kcp, Scg, Delta)
A.arParams = (Kcp
kcp, Scg
scg, Delta
delta)
                  ,
                    ChainSchema base hon
arHonest :: ChainSchema base hon
arHonest :: ChainSchema base hon
A.arHonest
                  }

            case Exn.runExcept $ A.checkAdversarialRecipe recipeA of
                Left NoSuchAdversarialChainSchema
e -> Maybe SomeTestAdversarialMutation
-> Gen (Maybe SomeTestAdversarialMutation)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe SomeTestAdversarialMutation
 -> Gen (Maybe SomeTestAdversarialMutation))
-> Maybe SomeTestAdversarialMutation
-> Gen (Maybe SomeTestAdversarialMutation)
forall a b. (a -> b) -> a -> b
$ case NoSuchAdversarialChainSchema
e of
                    NoSuchAdversarialChainSchema
A.NoSuchAdversarialBlock -> Maybe SomeTestAdversarialMutation
forall a. Maybe a
Nothing
                    NoSuchAdversarialChainSchema
A.NoSuchCompetitor       -> TestName -> Maybe SomeTestAdversarialMutation
forall a. HasCallStack => TestName -> a
error (TestName -> Maybe SomeTestAdversarialMutation)
-> TestName -> Maybe SomeTestAdversarialMutation
forall a b. (a -> b) -> a -> b
$ TestName
"impossible! " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> NoSuchAdversarialChainSchema -> TestName
forall a. Show a => a -> TestName
show NoSuchAdversarialChainSchema
e
                    NoSuchAdversarialChainSchema
A.NoSuchIntersection     -> TestName -> Maybe SomeTestAdversarialMutation
forall a. HasCallStack => TestName -> a
error (TestName -> Maybe SomeTestAdversarialMutation)
-> TestName -> Maybe SomeTestAdversarialMutation
forall a b. (a -> b) -> a -> b
$ TestName
"impossible! " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> NoSuchAdversarialChainSchema -> TestName
forall a. Show a => a -> TestName
show NoSuchAdversarialChainSchema
e

                Right SomeCheckedAdversarialRecipe base hon
recipeA' -> do
                  let dInc :: Int
dInc = SomeCheckedAdversarialRecipe base hon -> Int
forall {base} {hon}. SomeCheckedAdversarialRecipe base hon -> Int
deltaIncrementFromRecipe SomeCheckedAdversarialRecipe base hon
recipeA'
                  mut <- [AdversarialMutation] -> Gen AdversarialMutation
forall a. HasCallStack => [a] -> Gen a
QC.elements [AdversarialMutation
AdversarialMutateKcp, Int -> AdversarialMutation
AdversarialMutateDelta Int
dInc]
                  pure $ case Exn.runExcept $ A.checkAdversarialRecipe $ mutateAdversarial recipeA mut of
                    Left{} -> Maybe SomeTestAdversarialMutation
forall a. Maybe a
Nothing

                    Right (A.SomeCheckedAdversarialRecipe Proxy adv
Proxy CheckedAdversarialRecipe base hon adv
mutRecipeA)
                        -- no mutation matters if the adversary doesn't even
                        -- have k+1 slots of any kind, let alone active slots
                      | let A.UnsafeCheckedAdversarialRecipe {
                                carParams :: forall base hon adv.
CheckedAdversarialRecipe base hon adv -> (Kcp, Scg, Delta)
A.carParams = (Kcp Int
k', Scg
_scg', Delta
_delta')
                              ,
                                Contains 'SlotE hon adv
carWin :: Contains 'SlotE hon adv
carWin :: forall base hon adv.
CheckedAdversarialRecipe base hon adv -> Contains 'SlotE hon adv
A.carWin
                              } = CheckedAdversarialRecipe base hon adv
mutRecipeA
                      , Count adv 'SlotE Total -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount (Contains 'SlotE hon adv -> Count adv 'SlotE Total
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Size inner elem
C.windowSize Contains 'SlotE hon adv
carWin) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
k' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
                      -> Maybe SomeTestAdversarialMutation
forall a. Maybe a
Nothing

                      -- ASSUMPTION: the adversary has k blocks in the first race.
                      --
                      -- If there's no slot after the first race, then the
                      -- increment of delta cannot make a difference.
                      --
                      -- If there are not at least k+1 slots in the honest schema,
                      -- then decreasing k cannot make the schema check fail.
                      | let H.ChainSchema Contains 'SlotE base hon
_winH Vector hon 'SlotE S
vH = ChainSchema base hon
arHonest
                      , let Len Int
l   = Len
len
                      , let (Kcp Int
k', Scg
_scg', Delta Int
d') = CheckedAdversarialRecipe base hon adv -> (Kcp, Scg, Delta)
forall base hon adv.
CheckedAdversarialRecipe base hon adv -> (Kcp, Scg, Delta)
A.carParams CheckedAdversarialRecipe base hon adv
mutRecipeA
                        -- slot of the k+1 honest active
                      , Int
endOfFirstRace <- case Proxy 'Inverted
-> Vector hon 'SlotE S
-> Index hon (PreImage 'Inverted 'EmptySlotE)
-> MaybeFound hon
forall (pol :: Pol) (proxy :: Pol -> *) base.
POL pol =>
proxy pol
-> Vector base 'SlotE S
-> Index base (PreImage pol 'EmptySlotE)
-> MaybeFound base
BV.findIthEmptyInV Proxy 'Inverted
S.inverted Vector hon 'SlotE S
vH (Var hon 'ActiveSlotE -> Index hon 'ActiveSlotE
forall {kelem} base (elem :: kelem).
Var base elem -> Index base elem
C.toIndex Var hon 'ActiveSlotE
arPrefix Index hon 'ActiveSlotE -> Int -> Index hon 'ActiveSlotE
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int -> Count base elem which
C.+ Int
k') of
                            BV.NothingFound{} -> Int
l
                            BV.JustFound Index hon 'SlotE
x    -> Index hon 'SlotE -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount Index hon 'SlotE
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
d'
                      , Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
endOfFirstRace
                      -> Maybe SomeTestAdversarialMutation
forall a. Maybe a
Nothing

                      | Bool
otherwise ->
                        SomeTestAdversarialMutation -> Maybe SomeTestAdversarialMutation
forall a. a -> Maybe a
Just
                      (SomeTestAdversarialMutation -> Maybe SomeTestAdversarialMutation)
-> SomeTestAdversarialMutation -> Maybe SomeTestAdversarialMutation
forall a b. (a -> b) -> a -> b
$ Proxy base
-> Proxy hon
-> TestAdversarialMutation base hon
-> SomeTestAdversarialMutation
forall base hon.
Proxy base
-> Proxy hon
-> TestAdversarialMutation base hon
-> SomeTestAdversarialMutation
SomeTestAdversarialMutation Proxy base
forall {k} (t :: k). Proxy t
Proxy Proxy hon
forall {k} (t :: k). Proxy t
Proxy
                      (TestAdversarialMutation base hon -> SomeTestAdversarialMutation)
-> TestAdversarialMutation base hon -> SomeTestAdversarialMutation
forall a b. (a -> b) -> a -> b
$ HonestRecipe
-> CheckedHonestRecipe base hon
-> AdversarialRecipe base hon
-> SomeCheckedAdversarialRecipe base hon
-> AdversarialMutation
-> TestAdversarialMutation base hon
forall base hon.
HonestRecipe
-> CheckedHonestRecipe base hon
-> AdversarialRecipe base hon
-> SomeCheckedAdversarialRecipe base hon
-> AdversarialMutation
-> TestAdversarialMutation base hon
TestAdversarialMutation
                            HonestRecipe
recipeH
                            CheckedHonestRecipe base hon
recipeH'
                            AdversarialRecipe base hon
recipeA
                            SomeCheckedAdversarialRecipe base hon
recipeA'
                            AdversarialMutation
mut
      where
        -- | The increment of delta depends on what the honest schema is
        -- in the first stability window after the intersection.
        --
        -- If the stability window has more than k+1 slots. Incrementing
        -- delta by 1 should cause verification to fail for some adversarial
        -- schema. For instance if s=4, k=1, d=0, the intersection is Genesis
        -- and the honest schema is
        --
        -- > 0111 0101
        --
        -- then the following adversarial schema fails to validate with d=1.
        --
        -- > 0101 0011
        --
        -- However, if the stability window has exactly k+1 slots, then we
        -- need a higher increment for delta. Suppose the honest schema is
        --
        -- > 0110 0111
        --
        -- with the same parameters as before. In this situation, the
        -- adversarial schemas are constrained to have only one slot
        -- in the first stability window, and therefore it is impossible
        -- for the adversary to win a race to the k+1st active slot.
        --
        -- We compute the needed increment as the distance from the
        -- k+1st slot after the intersection to the first slot after the
        -- first stability window after the intersection. In our example,
        -- the increment is 2, and therefore with d=2 we can find the
        -- following alternative schema that fails validation.
        --
        -- > 0100 1000
        --
        deltaIncrementFromRecipe :: SomeCheckedAdversarialRecipe base hon -> Int
deltaIncrementFromRecipe (A.SomeCheckedAdversarialRecipe Proxy adv
_ CheckedAdversarialRecipe base hon adv
r) =
          let H.ChainSchema Contains 'SlotE base hon
_ Vector hon 'SlotE S
v = CheckedAdversarialRecipe base hon adv -> ChainSchema base hon
forall base hon adv.
CheckedAdversarialRecipe base hon adv -> ChainSchema base hon
A.carHonest CheckedAdversarialRecipe base hon adv
r
              sv :: Vector adv 'SlotE S
sv = Contains 'SlotE hon adv
-> Vector hon 'SlotE S -> Vector adv 'SlotE S
forall {k} a (elem :: k) outer inner.
Unbox a =>
Contains elem outer inner
-> Vector outer elem a -> Vector inner elem a
C.sliceV (CheckedAdversarialRecipe base hon adv -> Contains 'SlotE hon adv
forall base hon adv.
CheckedAdversarialRecipe base hon adv -> Contains 'SlotE hon adv
A.carWin CheckedAdversarialRecipe base hon adv
r) Vector hon 'SlotE S
v
              (Kcp Int
k, Scg Int
s, Delta
_) = CheckedAdversarialRecipe base hon adv -> (Kcp, Scg, Delta)
forall base hon adv.
CheckedAdversarialRecipe base hon adv -> (Kcp, Scg, Delta)
A.carParams CheckedAdversarialRecipe base hon adv
r
              kPlus1st :: Int
kPlus1st = case Proxy 'Inverted
-> Vector adv 'SlotE S
-> Index adv (PreImage 'Inverted 'EmptySlotE)
-> MaybeFound adv
forall (pol :: Pol) (proxy :: Pol -> *) base.
POL pol =>
proxy pol
-> Vector base 'SlotE S
-> Index base (PreImage pol 'EmptySlotE)
-> MaybeFound base
BV.findIthEmptyInV Proxy 'Inverted
S.inverted Vector adv 'SlotE S
sv (Int -> Count adv 'ActiveSlotE Preds
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
k) of
                MaybeFound adv
BV.NothingFound -> Int
1
                BV.JustFound Index adv 'SlotE
i  -> Index adv 'SlotE -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount Index adv 'SlotE
i
           in
              case Proxy 'Inverted
-> Vector adv 'SlotE S
-> Index adv (PreImage 'Inverted 'EmptySlotE)
-> MaybeFound adv
forall (pol :: Pol) (proxy :: Pol -> *) base.
POL pol =>
proxy pol
-> Vector base 'SlotE S
-> Index base (PreImage pol 'EmptySlotE)
-> MaybeFound base
BV.findIthEmptyInV Proxy 'Inverted
S.inverted Vector adv 'SlotE S
sv (Int -> Count adv 'ActiveSlotE Preds
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)) of
                BV.JustFound Index adv 'SlotE
i | Index adv 'SlotE -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount Index adv 'SlotE
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
s -> Int
1
                MaybeFound adv
_                                 -> Int
s Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
kPlus1st

-- | There exists a seed such that each 'TestAdversarialMutation' causes
-- 'A.checkAdversarialChain' to reject the result of 'A.uniformAdversarialChain'
--
-- TODO this did fail after >500,000 tests. Is that amount of flakiness acceptable?
prop_adversarialChainMutation :: SomeTestAdversarialMutation -> QCGen -> QC.Property
prop_adversarialChainMutation :: SomeTestAdversarialMutation -> QCGen -> Property
prop_adversarialChainMutation (SomeTestAdversarialMutation Proxy base
Proxy Proxy hon
Proxy TestAdversarialMutation base hon
testAdversarialMut) QCGen
testSeedAsSeed0 =
  IO Property -> Property
forall prop. Testable prop => IO prop -> Property
QC.ioProperty (IO Property -> Property) -> IO Property -> Property
forall a b. (a -> b) -> a -> b
$ do
    A.SomeCheckedAdversarialRecipe Proxy recipeA' <- SomeCheckedAdversarialRecipe base hon
-> IO (SomeCheckedAdversarialRecipe base hon)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SomeCheckedAdversarialRecipe base hon
someRecipeA'

    counter <- newIORef @Int 0
    catch   <- newIORef @(QCGen, [String]) (undefined, [])

    -- we're willing to wait up to 20s to find a failure for each 'TestHonestMutation'
    IO.timeout
        (20 * 10^(6::Int))
        (go catch counter recipeA' testSeedAsSeed0) >>= \case
            Just Property
prop -> Property -> IO Property
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Property
prop
            Maybe Property
Nothing   ->    -- did not find a failure caused by the mutation
                ((,) ((QCGen, [TestName]) -> Int -> ((QCGen, [TestName]), Int))
-> IO (QCGen, [TestName]) -> IO (Int -> ((QCGen, [TestName]), Int))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef (QCGen, [TestName]) -> IO (QCGen, [TestName])
forall a. IORef a -> IO a
readIORef IORef (QCGen, [TestName])
catch IO (Int -> ((QCGen, [TestName]), Int))
-> IO Int -> IO ((QCGen, [TestName]), Int)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef IORef Int
counter) IO ((QCGen, [TestName]), Int)
-> (((QCGen, [TestName]), Int) -> Property) -> IO Property
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \((QCGen
seedA, [TestName]
schedA'), Int
n) -> 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
"n = " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> TestName
forall a. Show a => a -> TestName
show Int
n)
                  (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample
                        (TestAdversarialMutation base hon
-> AdversarialRecipe base hon -> [TestName] -> QCGen -> TestName
forall base hon.
TestAdversarialMutation base hon
-> AdversarialRecipe base hon -> [TestName] -> QCGen -> TestName
advMutCounterexample TestAdversarialMutation base hon
testAdversarialMut AdversarialRecipe base hon
mutatedRecipe [TestName]
schedA' QCGen
seedA)
                  (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ Bool
False
  where
    TestAdversarialMutation HonestRecipe
recipeH CheckedHonestRecipe base hon
_recipeH' AdversarialRecipe base hon
recipeA SomeCheckedAdversarialRecipe base hon
someRecipeA' AdversarialMutation
mut = TestAdversarialMutation base hon
testAdversarialMut

    H.HonestRecipe Kcp
_kcp Scg
scg Delta
_delta Len
_len = HonestRecipe
recipeH

    mutatedRecipe :: AdversarialRecipe base hon
mutatedRecipe = AdversarialRecipe base hon
-> AdversarialMutation -> AdversarialRecipe base hon
forall base hon.
AdversarialRecipe base hon
-> AdversarialMutation -> AdversarialRecipe base hon
mutateAdversarial AdversarialRecipe base hon
recipeA AdversarialMutation
mut

    go :: IORef (QCGen, [TestName])
-> IORef a
-> CheckedAdversarialRecipe base hon inner
-> QCGen
-> IO Property
go IORef (QCGen, [TestName])
catch IORef a
counter CheckedAdversarialRecipe base hon inner
recipeA' QCGen
testSeedAsSeed = do
        IORef a -> (a -> a) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef a
counter (a -> a -> a
forall a. Num a => a -> a -> a
+a
1)
        let -- TODO is this a low quality random stream? Why is there no @'R.Random' 'QCGen'@ instance?
            (QCGen
testSeedA, QCGen
testSeedAsSeed') = QCGen -> (QCGen, QCGen)
forall g. RandomGen g => g -> (g, g)
R.split QCGen
testSeedAsSeed

            schedA :: ChainSchema base inner
schedA = Maybe Asc
-> CheckedAdversarialRecipe base hon inner
-> QCGen
-> ChainSchema base inner
forall g base hon adv.
RandomGen g =>
Maybe Asc
-> CheckedAdversarialRecipe base hon adv
-> g
-> ChainSchema base adv
A.uniformAdversarialChain Maybe Asc
forall a. Maybe a
Nothing CheckedAdversarialRecipe base hon inner
recipeA' (QCGen
testSeedA :: QCGen)
            m :: Except (AdversarialViolation hon inner) ()
m      = AdversarialRecipe base hon
-> ChainSchema base inner
-> Except (AdversarialViolation hon inner) ()
forall base hon adv.
AdversarialRecipe base hon
-> ChainSchema base adv -> Except (AdversarialViolation hon adv) ()
A.checkAdversarialChain AdversarialRecipe base hon
mutatedRecipe ChainSchema base inner
schedA
        -- We discard tests where the first race ends past the acceleration bound
        -- as these race windows are unconstrained
        case Except (AdversarialViolation hon inner) ()
-> Either (AdversarialViolation hon inner) ()
forall e a. Except e a -> Either e a
Exn.runExcept Except (AdversarialViolation hon inner) ()
m of
            Right () -> do
                let A.UnsafeCheckedAdversarialRecipe { Contains 'SlotE hon inner
carWin :: forall base hon adv.
CheckedAdversarialRecipe base hon adv -> Contains 'SlotE hon adv
carWin :: Contains 'SlotE hon inner
A.carWin } = CheckedAdversarialRecipe base hon inner
recipeA'
                    pretty :: [TestName]
pretty = case Scg -> ChainSchema base inner -> SomeWindow AdvStabLbl inner 'SlotE
forall base adv.
Scg -> ChainSchema base adv -> SomeWindow AdvStabLbl adv 'SlotE
calculateStability Scg
scg ChainSchema base inner
schedA of
                        C.SomeWindow Proxy skolem
Proxy Contains 'SlotE inner (Win AdvStabLbl skolem)
win ->
                            [Contains 'SlotE hon (Win AdvStabLbl skolem) -> ShowS
forall base inner. Contains 'SlotE base inner -> ShowS
H.prettyWindow (Contains 'SlotE hon inner
-> Contains 'SlotE inner (Win AdvStabLbl skolem)
-> Contains 'SlotE hon (Win AdvStabLbl skolem)
forall {kelem} (elem :: kelem) outer mid inner.
Contains elem outer mid
-> Contains elem mid inner -> Contains elem outer inner
C.joinWin Contains 'SlotE hon inner
carWin Contains 'SlotE inner (Win AdvStabLbl skolem)
win) TestName
"no accel"]
                         [TestName] -> [TestName] -> [TestName]
forall a. Semigroup a => a -> a -> a
<> [Size inner 'ActiveSlotE -> TestName
forall a. Show a => a -> TestName
show (ChainSchema base inner -> Size inner 'ActiveSlotE
forall base inner.
ChainSchema base inner -> Size inner 'ActiveSlotE
H.countChainSchema ChainSchema base inner
schedA)]
                IORef (QCGen, [TestName]) -> (QCGen, [TestName]) -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (QCGen, [TestName])
catch (QCGen
testSeedA,  ChainSchema base inner -> TestName -> [TestName]
forall base inner. ChainSchema base inner -> TestName -> [TestName]
H.prettyChainSchema ChainSchema base inner
schedA TestName
"A" [TestName] -> [TestName] -> [TestName]
forall a. Semigroup a => a -> a -> a
<> [TestName]
pretty)
                IORef (QCGen, [TestName])
-> IORef a
-> CheckedAdversarialRecipe base hon inner
-> QCGen
-> IO Property
go IORef (QCGen, [TestName])
catch IORef a
counter CheckedAdversarialRecipe base hon inner
recipeA' QCGen
testSeedAsSeed'
            Left AdversarialViolation hon inner
e   -> case AdversarialViolation hon inner
e of
                A.BadAnchor{}  -> TestName -> IO Property
forall a. HasCallStack => TestName -> a
error (TestName -> IO Property) -> TestName -> IO Property
forall a b. (a -> b) -> a -> b
$ TestName
"impossible! " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> AdversarialViolation hon inner -> TestName
forall a. Show a => a -> TestName
show AdversarialViolation hon inner
e
                A.BadCount{}   -> TestName -> IO Property
forall a. HasCallStack => TestName -> a
error (TestName -> IO Property) -> TestName -> IO Property
forall a b. (a -> b) -> a -> b
$ TestName
"impossible! " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> AdversarialViolation hon inner -> TestName
forall a. Show a => a -> TestName
show AdversarialViolation hon inner
e
                A.BadDensity{} -> Property -> IO Property
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ () -> Property
forall prop. Testable prop => prop -> Property
QC.property ()
                A.BadRace{}    -> Property -> IO Property
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ () -> Property
forall prop. Testable prop => prop -> Property
QC.property ()

-----

-- | A nice rendering for failures of 'prop_adversarialChainMutation'
advMutCounterexample ::
     TestAdversarialMutation base hon
  -> A.AdversarialRecipe base hon
  -> [String]
  -> QCGen
  -> String
advMutCounterexample :: forall base hon.
TestAdversarialMutation base hon
-> AdversarialRecipe base hon -> [TestName] -> QCGen -> TestName
advMutCounterexample TestAdversarialMutation base hon
testAdversarialMut AdversarialRecipe base hon
mutatedRecipe [TestName]
schedA' QCGen
seedA =
    [TestName] -> TestName
H.unlines' ([TestName] -> TestName) -> [TestName] -> TestName
forall a b. (a -> b) -> a -> b
$ []
     [TestName] -> [TestName] -> [TestName]
forall a. Semigroup a => a -> a -> a
<> [QCGen -> TestName
forall a. Show a => a -> TestName
show QCGen
seedA]
     [TestName] -> [TestName] -> [TestName]
forall a. Semigroup a => a -> a -> a
<> [Size hon 'ActiveSlotE -> TestName
forall a. Show a => a -> TestName
show Size hon 'ActiveSlotE
ch TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> TestName
" - " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> Var hon 'ActiveSlotE -> TestName
forall a. Show a => a -> TestName
show Var hon 'ActiveSlotE
arPrefix TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> TestName
" = " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> Var hon 'ActiveSlotE -> TestName
forall a. Show a => a -> TestName
show (Size hon 'ActiveSlotE -> Var hon 'ActiveSlotE
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Var base elem
C.toVar Size hon 'ActiveSlotE
ch Var hon 'ActiveSlotE
-> Var hon 'ActiveSlotE -> Var hon 'ActiveSlotE
forall a. Num a => a -> a -> a
- Var hon 'ActiveSlotE
arPrefix) TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> TestName
"   vs " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> (Kcp, AdversarialMutation) -> TestName
forall a. Show a => a -> TestName
show (Kcp
kcp, AdversarialMutation
mut)]
     [TestName] -> [TestName] -> [TestName]
forall a. Semigroup a => a -> a -> a
<> [TestName]
schedH'
     [TestName] -> [TestName] -> [TestName]
forall a. Semigroup a => a -> a -> a
<> [TestName]
schedA'
     [TestName] -> [TestName] -> [TestName]
forall a. Semigroup a => a -> a -> a
<> Maybe (Bool, Race hon) -> [TestName]
go' (((,) Bool
False (Race hon -> (Bool, Race hon))
-> Maybe (Race hon) -> Maybe (Bool, Race hon)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Kcp -> Vector hon 'SlotE S -> Maybe (Race hon)
forall base. Kcp -> Vector base 'SlotE S -> Maybe (Race base)
RI.init Kcp
kcp' Vector hon 'SlotE S
vH) Maybe (Bool, Race hon)
-> Maybe (Bool, Race hon) -> Maybe (Bool, Race hon)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Bool, Race hon) -> Maybe (Bool, Race hon)
forall a. a -> Maybe a
Just (Bool
True, Vector hon 'SlotE S -> Race hon
forall base. Vector base 'SlotE S -> Race base
RI.initConservative Vector hon 'SlotE S
vH))
  where
    TestAdversarialMutation HonestRecipe
recipeH CheckedHonestRecipe base hon
_recipeH' AdversarialRecipe base hon
recipeA SomeCheckedAdversarialRecipe base hon
someRecipeA' AdversarialMutation
mut = TestAdversarialMutation base hon
testAdversarialMut

    H.HonestRecipe Kcp
kcp Scg
_scg Delta
_delta Len
_len = HonestRecipe
recipeH

    A.AdversarialRecipe { ChainSchema base hon
arHonest :: forall base hon. AdversarialRecipe base hon -> ChainSchema base hon
arHonest :: ChainSchema base hon
A.arHonest, Var hon 'ActiveSlotE
arPrefix :: forall base hon. AdversarialRecipe base hon -> Var hon 'ActiveSlotE
arPrefix :: Var hon 'ActiveSlotE
A.arPrefix } = AdversarialRecipe base hon
recipeA

    H.ChainSchema Contains 'SlotE base hon
_winH Vector hon 'SlotE S
vH = ChainSchema base hon
arHonest

    A.AdversarialRecipe { arParams :: forall base hon. AdversarialRecipe base hon -> (Kcp, Scg, Delta)
A.arParams = (Kcp
kcp', Scg
_scg', Delta
_delta') } = AdversarialRecipe base hon
mutatedRecipe

    schedH' :: [TestName]
schedH' = ChainSchema base hon -> TestName -> [TestName]
forall base inner. ChainSchema base inner -> TestName -> [TestName]
H.prettyChainSchema ChainSchema base hon
arHonest TestName
"H"

    ch :: Size hon 'ActiveSlotE
ch = ChainSchema base hon -> Size hon 'ActiveSlotE
forall base inner.
ChainSchema base inner -> Size inner 'ActiveSlotE
H.countChainSchema ChainSchema base hon
arHonest

    next :: Race hon -> Maybe (Bool, Race hon)
next Race hon
iter =
            ((,) Bool
False (Race hon -> (Bool, Race hon))
-> Maybe (Race hon) -> Maybe (Bool, Race hon)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector hon 'SlotE S -> Race hon -> Maybe (Race hon)
forall base. Vector base 'SlotE S -> Race base -> Maybe (Race base)
RI.next Vector hon 'SlotE S
vH Race hon
iter)
        Maybe (Bool, Race hon)
-> Maybe (Bool, Race hon) -> Maybe (Bool, Race hon)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
            ((,) Bool
True (Race hon -> (Bool, Race hon))
-> Maybe (Race hon) -> Maybe (Bool, Race hon)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector hon 'SlotE S -> Race hon -> Maybe (Race hon)
forall base. Vector base 'SlotE S -> Race base -> Maybe (Race base)
RI.nextConservative Vector hon 'SlotE S
vH Race hon
iter)

    go' :: Maybe (Bool, Race hon) -> [TestName]
go' = \case
        Maybe (Bool, Race hon)
Nothing -> []
        Just (Bool
cons, iter :: Race hon
iter@(RI.Race (C.SomeWindow Proxy skolem
Proxy Contains 'SlotE hon (Win RaceLbl skolem)
win)))
          | A.SomeCheckedAdversarialRecipe Proxy adv
Proxy CheckedAdversarialRecipe base hon adv
recipeA' <- SomeCheckedAdversarialRecipe base hon
someRecipeA'
          , A.UnsafeCheckedAdversarialRecipe { Contains 'SlotE hon adv
carWin :: forall base hon adv.
CheckedAdversarialRecipe base hon adv -> Contains 'SlotE hon adv
carWin :: Contains 'SlotE hon adv
A.carWin } <- CheckedAdversarialRecipe base hon adv
recipeA'
          , Contains 'SlotE hon (Win RaceLbl skolem) -> Index hon 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index outer elem
C.windowStart Contains 'SlotE hon (Win RaceLbl skolem)
win Index hon 'SlotE -> Index hon 'SlotE -> Bool
forall a. Ord a => a -> a -> Bool
< Contains 'SlotE hon adv -> Index hon 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index outer elem
C.windowStart Contains 'SlotE hon adv
carWin
          -> Maybe (Bool, Race hon) -> [TestName]
go' (Race hon -> Maybe (Bool, Race hon)
next Race hon
iter)

          | Bool
otherwise ->
              TestName
""
            TestName -> [TestName] -> [TestName]
forall a. a -> [a] -> [a]
: [TestName] -> TestName
forall a. HasCallStack => [a] -> a
head ([TestName] -> [TestName]
forall a. HasCallStack => [a] -> [a]
tail [TestName]
schedH')
            TestName -> [TestName] -> [TestName]
forall a. a -> [a] -> [a]
: Contains 'SlotE hon (Win RaceLbl skolem) -> ShowS
forall base inner. Contains 'SlotE base inner -> ShowS
H.prettyWindow Contains 'SlotE hon (Win RaceLbl skolem)
win (TestName
"raceH" TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> if Bool
cons then TestName
" (conservative)" else TestName
"")
            TestName -> [TestName] -> [TestName]
forall a. a -> [a] -> [a]
: Int -> [TestName] -> [TestName]
forall a. Int -> [a] -> [a]
take Int
2 ([TestName] -> [TestName]
forall a. HasCallStack => [a] -> [a]
tail [TestName]
schedA')