{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}

module Test.Ouroboros.Consensus.ChainGenerator.Tests.BitVector (tests) where

import           Data.Monoid (Endo (Endo, appEndo))
import qualified Data.Vector.Unboxed as V
import           GHC.Generics (Generic)
import qualified System.Random.Stateful as R
import qualified Test.Ouroboros.Consensus.ChainGenerator.BitVector as BV
import qualified Test.Ouroboros.Consensus.ChainGenerator.Counting as C
import qualified Test.Ouroboros.Consensus.ChainGenerator.Slot as S
import           Test.Ouroboros.Consensus.ChainGenerator.Slot
                     (E (EmptySlotE, SlotE), POL, PreImage, S)
import qualified Test.Ouroboros.Consensus.ChainGenerator.Some as Some
import qualified Test.QuickCheck as QC
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 -> (SomeFindTestSetup -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
TT.testProperty TestName
"prop_findIthEmptyInV" SomeFindTestSetup -> Property
prop_findIthEmptyInV,
    TestName -> (FillInWindowSetup -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
TT.testProperty TestName
"prop_fillInWindow" FillInWindowSetup -> Property
prop_fillInWindow
  ]

-----

data SomeFindTestSetup = forall pol. TestPOL pol => SomeFindTestSetup (FindTestSetup pol)

instance Show SomeFindTestSetup where
    showsPrec :: Int -> SomeFindTestSetup -> ShowS
showsPrec Int
p (SomeFindTestSetup FindTestSetup pol
testSetup) =
        Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11)
      (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ TestName -> ShowS
showString TestName
"SomeFindTestSetup " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> FindTestSetup pol -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 FindTestSetup pol
testSetup

data ProxyPol (pol :: S.Pol) = ProxyPol
  deriving (ProxyPol pol -> ProxyPol pol -> Bool
(ProxyPol pol -> ProxyPol pol -> Bool)
-> (ProxyPol pol -> ProxyPol pol -> Bool) -> Eq (ProxyPol pol)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (pol :: Pol). ProxyPol pol -> ProxyPol pol -> Bool
$c== :: forall (pol :: Pol). ProxyPol pol -> ProxyPol pol -> Bool
== :: ProxyPol pol -> ProxyPol pol -> Bool
$c/= :: forall (pol :: Pol). ProxyPol pol -> ProxyPol pol -> Bool
/= :: ProxyPol pol -> ProxyPol pol -> Bool
Eq)

instance TestPOL pol => Show (ProxyPol pol) where
    showsPrec :: Int -> ProxyPol pol -> ShowS
showsPrec Int
p ProxyPol pol
pol =
        Int -> ShowBuilder (ProxyPol pol) -> ShowS
forall a.
NoFun "runShowsPrec" a (AbsError "runShowsPrec" a) =>
Int -> ShowBuilder a -> ShowS
Some.runShowsPrec Int
p
      (ShowBuilder (ProxyPol pol) -> ShowS)
-> ShowBuilder (ProxyPol pol) -> ShowS
forall a b. (a -> b) -> a -> b
$ ProxyPol pol -> TestName -> ShowBuilder (ProxyPol pol)
forall a. a -> TestName -> ShowBuilder a
Some.showCtor ProxyPol pol
pol (TestName
"ProxyPol :: ProxyPol " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> ProxyPol pol -> TestName
forall (pol :: Pol) (proxy :: Pol -> *).
TestPOL pol =>
proxy pol -> TestName
forall (proxy :: Pol -> *). proxy pol -> TestName
showPol ProxyPol pol
pol)

instance TestPOL pol => Read (ProxyPol pol) where
    readPrec :: ReadPrec (ProxyPol pol)
readPrec =
        ReadBuilder (ProxyPol pol) -> ReadPrec (ProxyPol pol)
forall a.
NoFun "runReadPrec" a (AbsError "runReadPrec" a) =>
ReadBuilder a -> ReadPrec a
Some.runReadPrec
      (ReadBuilder (ProxyPol pol) -> ReadPrec (ProxyPol pol))
-> ReadBuilder (ProxyPol pol) -> ReadPrec (ProxyPol pol)
forall a b. (a -> b) -> a -> b
$ ProxyPol pol -> TestName -> ReadBuilder (ProxyPol pol)
forall a. a -> TestName -> ReadBuilder a
Some.readCtor ProxyPol pol
pol (ProxyPol pol -> TestName
forall a. Show a => a -> TestName
show ProxyPol pol
pol)
      where
        pol :: ProxyPol pol
pol = ProxyPol pol
forall (pol :: Pol). ProxyPol pol
ProxyPol :: ProxyPol pol

data TestB

instance QC.Arbitrary (ProxyPol pol) where
    arbitrary :: Gen (ProxyPol pol)
arbitrary = ProxyPol pol -> Gen (ProxyPol pol)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ProxyPol pol
forall (pol :: Pol). ProxyPol pol
ProxyPol
    shrink :: ProxyPol pol -> [ProxyPol pol]
shrink    = ProxyPol pol -> [ProxyPol pol]
forall a. a -> [a]
QC.shrinkNothing

data SomePol = forall pol. TestPOL pol => SomePol (ProxyPol pol)

deriving instance Show SomePol

data FindTestSetup (pol :: S.Pol) = FindTestSetup {
    forall (pol :: Pol). FindTestSetup pol -> ProxyPol pol
testPol   :: ProxyPol pol
  ,
    -- | INVARIANT @'testIndex' < V.sum (V.map ('countZeros' 'testPol') 'testV')@
    forall (pol :: Pol).
FindTestSetup pol -> Index TestB (PreImage pol 'EmptySlotE)
testIndex :: C.Index TestB (PreImage pol EmptySlotE)
  ,
    forall (pol :: Pol). FindTestSetup pol -> Vector TestB 'SlotE S
testV     :: C.Vector TestB SlotE S
  }
  deriving (FindTestSetup pol -> FindTestSetup pol -> Bool
(FindTestSetup pol -> FindTestSetup pol -> Bool)
-> (FindTestSetup pol -> FindTestSetup pol -> Bool)
-> Eq (FindTestSetup pol)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (pol :: Pol). FindTestSetup pol -> FindTestSetup pol -> Bool
$c== :: forall (pol :: Pol). FindTestSetup pol -> FindTestSetup pol -> Bool
== :: FindTestSetup pol -> FindTestSetup pol -> Bool
$c/= :: forall (pol :: Pol). FindTestSetup pol -> FindTestSetup pol -> Bool
/= :: FindTestSetup pol -> FindTestSetup pol -> Bool
Eq, (forall x. FindTestSetup pol -> Rep (FindTestSetup pol) x)
-> (forall x. Rep (FindTestSetup pol) x -> FindTestSetup pol)
-> Generic (FindTestSetup pol)
forall x. Rep (FindTestSetup pol) x -> FindTestSetup pol
forall x. FindTestSetup pol -> Rep (FindTestSetup pol) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (pol :: Pol) x.
Rep (FindTestSetup pol) x -> FindTestSetup pol
forall (pol :: Pol) x.
FindTestSetup pol -> Rep (FindTestSetup pol) x
$cfrom :: forall (pol :: Pol) x.
FindTestSetup pol -> Rep (FindTestSetup pol) x
from :: forall x. FindTestSetup pol -> Rep (FindTestSetup pol) x
$cto :: forall (pol :: Pol) x.
Rep (FindTestSetup pol) x -> FindTestSetup pol
to :: forall x. Rep (FindTestSetup pol) x -> FindTestSetup pol
Generic, ReadPrec [FindTestSetup pol]
ReadPrec (FindTestSetup pol)
Int -> ReadS (FindTestSetup pol)
ReadS [FindTestSetup pol]
(Int -> ReadS (FindTestSetup pol))
-> ReadS [FindTestSetup pol]
-> ReadPrec (FindTestSetup pol)
-> ReadPrec [FindTestSetup pol]
-> Read (FindTestSetup pol)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall (pol :: Pol). TestPOL pol => ReadPrec [FindTestSetup pol]
forall (pol :: Pol). TestPOL pol => ReadPrec (FindTestSetup pol)
forall (pol :: Pol).
TestPOL pol =>
Int -> ReadS (FindTestSetup pol)
forall (pol :: Pol). TestPOL pol => ReadS [FindTestSetup pol]
$creadsPrec :: forall (pol :: Pol).
TestPOL pol =>
Int -> ReadS (FindTestSetup pol)
readsPrec :: Int -> ReadS (FindTestSetup pol)
$creadList :: forall (pol :: Pol). TestPOL pol => ReadS [FindTestSetup pol]
readList :: ReadS [FindTestSetup pol]
$creadPrec :: forall (pol :: Pol). TestPOL pol => ReadPrec (FindTestSetup pol)
readPrec :: ReadPrec (FindTestSetup pol)
$creadListPrec :: forall (pol :: Pol). TestPOL pol => ReadPrec [FindTestSetup pol]
readListPrec :: ReadPrec [FindTestSetup pol]
Read, Int -> FindTestSetup pol -> ShowS
[FindTestSetup pol] -> ShowS
FindTestSetup pol -> TestName
(Int -> FindTestSetup pol -> ShowS)
-> (FindTestSetup pol -> TestName)
-> ([FindTestSetup pol] -> ShowS)
-> Show (FindTestSetup pol)
forall a.
(Int -> a -> ShowS) -> (a -> TestName) -> ([a] -> ShowS) -> Show a
forall (pol :: Pol).
TestPOL pol =>
Int -> FindTestSetup pol -> ShowS
forall (pol :: Pol). TestPOL pol => [FindTestSetup pol] -> ShowS
forall (pol :: Pol). TestPOL pol => FindTestSetup pol -> TestName
$cshowsPrec :: forall (pol :: Pol).
TestPOL pol =>
Int -> FindTestSetup pol -> ShowS
showsPrec :: Int -> FindTestSetup pol -> ShowS
$cshow :: forall (pol :: Pol). TestPOL pol => FindTestSetup pol -> TestName
show :: FindTestSetup pol -> TestName
$cshowList :: forall (pol :: Pol). TestPOL pol => [FindTestSetup pol] -> ShowS
showList :: [FindTestSetup pol] -> ShowS
Show)

instance QC.Arbitrary SomePol where
    arbitrary :: Gen SomePol
arbitrary = do
        Bool
inverted <- Gen Bool
forall a. Arbitrary a => Gen a
QC.arbitrary
        if Bool
inverted then
          SomePol -> Gen SomePol
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomePol -> Gen SomePol) -> SomePol -> Gen SomePol
forall a b. (a -> b) -> a -> b
$ ProxyPol 'Inverted -> SomePol
forall (pol :: Pol). TestPOL pol => ProxyPol pol -> SomePol
SomePol (ProxyPol 'Inverted
forall (pol :: Pol). ProxyPol pol
ProxyPol :: ProxyPol S.Inverted)
        else
          SomePol -> Gen SomePol
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomePol -> Gen SomePol) -> SomePol -> Gen SomePol
forall a b. (a -> b) -> a -> b
$ ProxyPol 'NotInverted -> SomePol
forall (pol :: Pol). TestPOL pol => ProxyPol pol -> SomePol
SomePol (ProxyPol 'NotInverted
forall (pol :: Pol). ProxyPol pol
ProxyPol :: ProxyPol S.NotInverted)
    shrink :: SomePol -> [SomePol]
shrink    = SomePol -> [SomePol]
forall a. a -> [a]
QC.shrinkNothing

instance QC.Arbitrary SomeFindTestSetup where
    arbitrary :: Gen SomeFindTestSetup
arbitrary = do
        SomePol (ProxyPol pol
_ :: ProxyPol pol) <- Gen SomePol
forall a. Arbitrary a => Gen a
QC.arbitrary
        FindTestSetup pol -> SomeFindTestSetup
forall (pol :: Pol).
TestPOL pol =>
FindTestSetup pol -> SomeFindTestSetup
SomeFindTestSetup (FindTestSetup pol -> SomeFindTestSetup)
-> Gen (FindTestSetup pol) -> Gen SomeFindTestSetup
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Gen (FindTestSetup pol)
forall a. Arbitrary a => Gen a
QC.arbitrary :: QC.Gen (FindTestSetup pol))

    shrink :: SomeFindTestSetup -> [SomeFindTestSetup]
shrink (SomeFindTestSetup FindTestSetup pol
x) = [ FindTestSetup pol -> SomeFindTestSetup
forall (pol :: Pol).
TestPOL pol =>
FindTestSetup pol -> SomeFindTestSetup
SomeFindTestSetup FindTestSetup pol
y | FindTestSetup pol
y <- FindTestSetup pol -> [FindTestSetup pol]
forall a. Arbitrary a => a -> [a]
QC.shrink FindTestSetup pol
x ]

instance TestPOL pol => QC.Arbitrary (FindTestSetup pol) where
    arbitrary :: Gen (FindTestSetup pol)
arbitrary = do
        let testPol :: ProxyPol pol
testPol = ProxyPol pol
forall (pol :: Pol). ProxyPol pol
ProxyPol :: ProxyPol pol

        Vector S
v <- [S] -> Vector S
forall a. Unbox a => [a] -> Vector a
V.fromList ([S] -> Vector S) -> Gen [S] -> Gen (Vector S)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen [S]
forall a. Arbitrary a => Gen a
QC.arbitrary

        let tc :: Int
tc = ProxyPol pol -> Vector S -> Int
forall (pol :: Pol) (proxy :: Pol -> *).
TestPOL pol =>
proxy pol -> Vector S -> Int
targetCount ProxyPol pol
testPol Vector S
v
        Int
i <- if Int
0 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
tc then Gen Int
forall a. a
QC.discard else (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
QC.choose (Int
0, Int
tc Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)

        FindTestSetup pol -> Gen (FindTestSetup pol)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FindTestSetup {
            ProxyPol pol
testPol :: ProxyPol pol
testPol :: ProxyPol pol
testPol
          ,
            testIndex :: Index TestB (PreImage pol 'EmptySlotE)
testIndex = Int -> Index TestB (PreImage pol 'EmptySlotE)
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
i
          ,
            testV :: Vector TestB 'SlotE S
testV     = Vector S -> Vector TestB 'SlotE S
forall {k} {k1} (base :: k) (elem :: k1) a.
Vector a -> Vector base elem a
C.Vector Vector S
v
          }

    shrink :: FindTestSetup pol -> [FindTestSetup pol]
shrink FindTestSetup pol
x =
        [ FindTestSetup pol
y
        | FindTestSetup pol
y <- FindTestSetup pol -> [FindTestSetup pol]
forall a.
(Generic a, RecursivelyShrink (Rep a), GSubterms (Rep a) a) =>
a -> [a]
QC.genericShrink FindTestSetup pol
x
        , let FindTestSetup {Index TestB (PreImage pol 'EmptySlotE)
testIndex :: forall (pol :: Pol).
FindTestSetup pol -> Index TestB (PreImage pol 'EmptySlotE)
testIndex :: Index TestB (PreImage pol 'EmptySlotE)
testIndex, ProxyPol pol
testPol :: forall (pol :: Pol). FindTestSetup pol -> ProxyPol pol
testPol :: ProxyPol pol
testPol, Vector TestB 'SlotE S
testV :: forall (pol :: Pol). FindTestSetup pol -> Vector TestB 'SlotE S
testV :: Vector TestB 'SlotE S
testV} = FindTestSetup pol
y
        , Index TestB (PreImage pol 'EmptySlotE) -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount Index TestB (PreImage pol 'EmptySlotE)
testIndex Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< ProxyPol pol -> Vector S -> Int
forall (pol :: Pol) (proxy :: Pol -> *).
TestPOL pol =>
proxy pol -> Vector S -> Int
targetCount ProxyPol pol
testPol (Vector TestB 'SlotE S -> Vector S
forall {k1} {k2} (base :: k1) (elem :: k2) a.
Vector base elem a -> Vector a
C.getVector Vector TestB 'SlotE S
testV)
        ]

targetCount :: TestPOL pol => proxy pol -> V.Vector S -> Int
targetCount :: forall (pol :: Pol) (proxy :: Pol -> *).
TestPOL pol =>
proxy pol -> Vector S -> Int
targetCount proxy pol
pol = Vector S -> Int
forall a. Unbox a => Vector a -> Int
V.length (Vector S -> Int) -> (Vector S -> Vector S) -> Vector S -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (S -> Bool) -> Vector S -> Vector S
forall a. Unbox a => (a -> Bool) -> Vector a -> Vector a
V.filter (Bool -> Bool
not (Bool -> Bool) -> (S -> Bool) -> S -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. proxy pol -> S -> Bool
forall (pol :: Pol) (proxy :: Pol -> *).
POL pol =>
proxy pol -> S -> Bool
forall (proxy :: Pol -> *). proxy pol -> S -> Bool
S.test proxy pol
pol)

-----

class POL pol => TestPOL (pol :: S.Pol) where showPol :: proxy pol -> String
instance TestPOL S.Inverted             where showPol :: forall (proxy :: Pol -> *). proxy 'Inverted -> TestName
showPol proxy 'Inverted
_pol = TestName
"Inverted"
instance TestPOL S.NotInverted          where showPol :: forall (proxy :: Pol -> *). proxy 'NotInverted -> TestName
showPol proxy 'NotInverted
_pol = TestName
"NotInverted"

-- | Check that when @findIthEmptyInV pol bv i@ yields 'JustFound'
--
-- 1. it yields the index of an inactive slot
-- 2. there are exactly @i@ inactive slots in the preceding slots
--
prop_findIthEmptyInV :: SomeFindTestSetup -> QC.Property
prop_findIthEmptyInV :: SomeFindTestSetup -> Property
prop_findIthEmptyInV SomeFindTestSetup
testSetup = case SomeFindTestSetup
testSetup of
    SomeFindTestSetup FindTestSetup {
        Index TestB (PreImage pol 'EmptySlotE)
testIndex :: forall (pol :: Pol).
FindTestSetup pol -> Index TestB (PreImage pol 'EmptySlotE)
testIndex :: Index TestB (PreImage pol 'EmptySlotE)
testIndex
      ,
        ProxyPol pol
testPol :: forall (pol :: Pol). FindTestSetup pol -> ProxyPol pol
testPol :: ProxyPol pol
testPol
      ,
        Vector TestB 'SlotE S
testV :: forall (pol :: Pol). FindTestSetup pol -> Vector TestB 'SlotE S
testV :: Vector TestB 'SlotE S
testV
      } -> case ProxyPol pol
-> Vector TestB 'SlotE S
-> Index TestB (PreImage pol 'EmptySlotE)
-> MaybeFound TestB
forall (pol :: Pol) (proxy :: Pol -> *) base.
POL pol =>
proxy pol
-> Vector base 'SlotE S
-> Index base (PreImage pol 'EmptySlotE)
-> MaybeFound base
BV.findIthEmptyInV ProxyPol pol
testPol Vector TestB 'SlotE S
testV Index TestB (PreImage pol 'EmptySlotE)
testIndex of
        MaybeFound TestB
BV.NothingFound -> TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample TestName
"NothingFound" Bool
False
        BV.JustFound Index TestB 'SlotE
i  ->
              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 (ProxyPol pol -> TestName
forall (pol :: Pol) (proxy :: Pol -> *).
TestPOL pol =>
proxy pol -> TestName
forall (proxy :: Pol -> *). proxy pol -> TestName
showPol ProxyPol pol
testPol)
            (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample
                (let C.Vector Vector S
v = Vector TestB 'SlotE S
testV
                 in
                 TestName
"v =" TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> (S -> Endo TestName) -> Vector S -> Endo TestName
forall m a. (Monoid m, Unbox a) => (a -> m) -> Vector a -> m
V.foldMap (ShowS -> Endo TestName
forall a. (a -> a) -> Endo a
Endo (ShowS -> Endo TestName) -> (S -> ShowS) -> S -> Endo TestName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. S -> ShowS
S.showS) Vector S
v Endo TestName -> ShowS
forall a. Endo a -> a -> a
`appEndo` TestName
""
                )
            (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (TestName
"i = " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> Index TestB 'SlotE -> TestName
forall a. Show a => a -> TestName
show Index TestB 'SlotE
i)
            (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
               (   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
"i isn't the position of a post-polarization-0 in w!"
                 (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ ProxyPol pol -> Vector TestB 'SlotE S -> Index TestB 'SlotE -> Bool
forall (pol :: Pol) (proxy :: Pol -> *) base.
POL pol =>
proxy pol -> Vector base 'SlotE S -> Index base 'SlotE -> Bool
BV.testV ProxyPol pol
testPol Vector TestB 'SlotE S
testV Index TestB 'SlotE
i Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
QC.=== Bool
False
               )
              Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
QC..&&.
                  (   let targetsInPrecedingWords :: Int
targetsInPrecedingWords =
                              ProxyPol pol -> Vector S -> Int
forall (pol :: Pol) (proxy :: Pol -> *).
TestPOL pol =>
proxy pol -> Vector S -> Int
targetCount ProxyPol pol
testPol (Vector S -> Int) -> Vector S -> Int
forall a b. (a -> b) -> a -> b
$ Int -> Vector S -> Vector S
forall a. Unbox a => Int -> Vector a -> Vector a
V.take (Index TestB 'SlotE -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount Index TestB 'SlotE
i) (Vector S -> Vector S) -> Vector S -> Vector S
forall a b. (a -> b) -> a -> b
$ Vector TestB 'SlotE S -> Vector S
forall {k1} {k2} (base :: k1) (elem :: k2) a.
Vector base elem a -> Vector a
C.getVector Vector TestB 'SlotE S
testV
                      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
"There are not testIndex-many post-polarization-0s preceding i!"
                      (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Int
targetsInPrecedingWords Int -> Int -> Property
forall a. (Eq a, Show a) => a -> a -> Property
QC.=== Index TestB (PreImage pol 'EmptySlotE) -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount Index TestB (PreImage pol 'EmptySlotE)
testIndex
                  )


data FillInWindowSetup =
    FillInWindowSetup
      SomePol
      Int -- ^ k
      Int -- ^ size of the window to fill
      QCGen -- ^ random generator
      (V.Vector S) -- ^ the vector to fill

instance Show FillInWindowSetup where
  showsPrec :: Int -> FillInWindowSetup -> ShowS
showsPrec Int
p (FillInWindowSetup SomePol
spol Int
k Int
szW QCGen
qcGen Vector S
v) =
        Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11)
      (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ TestName -> ShowS
showString TestName
"FillInWindowSetup"
      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestName -> ShowS
showString TestName
"\n  pol = " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomePol -> ShowS
forall a. Show a => a -> ShowS
shows SomePol
spol
      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestName -> ShowS
showString TestName
"\n  k = " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ShowS
forall a. Show a => a -> ShowS
shows Int
k
      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestName -> ShowS
showString TestName
"\n  qcGen = " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QCGen -> ShowS
forall a. Show a => a -> ShowS
shows QCGen
qcGen
      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestName -> ShowS
showString TestName
"\n  szW = " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ShowS
forall a. Show a => a -> ShowS
shows Int
szW
      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestName -> ShowS
showString TestName
"\n  v = " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestName -> ShowS
forall a. Show a => a -> ShowS
shows (Vector S -> TestName
showBitVector Vector S
v)

showBitVector :: V.Vector S -> String
showBitVector :: Vector S -> TestName
showBitVector Vector S
v =
    Int -> ShowS
forall a. Int -> [a] -> [a]
take Int
bvLen [ if Bool
b then Char
'1' else Char
'0' | S
s <- Vector S -> [S]
forall a. Unbox a => Vector a -> [a]
V.toList Vector S
v, let b :: Bool
b = Proxy 'NotInverted -> S -> Bool
forall (pol :: Pol) (proxy :: Pol -> *).
POL pol =>
proxy pol -> S -> Bool
forall (proxy :: Pol -> *). proxy 'NotInverted -> S -> Bool
S.test Proxy 'NotInverted
S.notInverted S
s ]
    TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ if Int
szV Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
bvLen then TestName
"..." else TestName
""
  where
    szV :: Int
szV = Vector S -> Int
forall a. Unbox a => Vector a -> Int
V.length Vector S
v
    bvLen :: Int
bvLen = Int
80

instance QC.Arbitrary FillInWindowSetup where
  arbitrary :: Gen FillInWindowSetup
arbitrary = do
      SomePol
pol <- Gen SomePol
forall a. Arbitrary a => Gen a
QC.arbitrary
      QC.NonNegative Int
k <- Gen (NonNegative Int)
forall a. Arbitrary a => Gen a
QC.arbitrary
      QC.NonNegative Int
k1 <- Gen (NonNegative Int)
forall a. Arbitrary a => Gen a
QC.arbitrary
      QC.NonNegative Int
k2 <- Gen (NonNegative Int)
forall a. Arbitrary a => Gen a
QC.arbitrary
      QCGen
qcGen <- Gen QCGen
forall a. Arbitrary a => Gen a
QC.arbitrary
      let szV :: Int
szV = Int
k1
          szW :: Int
szW = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
k Int
szV Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
k2 -- k <= szW && szV <= szW
      [S]
ss <- Int -> Gen S -> Gen [S]
forall a. Int -> Gen a -> Gen [a]
QC.vectorOf Int
szV Gen S
forall a. Arbitrary a => Gen a
QC.arbitrary
      FillInWindowSetup -> Gen FillInWindowSetup
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FillInWindowSetup -> Gen FillInWindowSetup)
-> FillInWindowSetup -> Gen FillInWindowSetup
forall a b. (a -> b) -> a -> b
$ SomePol -> Int -> Int -> QCGen -> Vector S -> FillInWindowSetup
FillInWindowSetup SomePol
pol Int
k Int
szW QCGen
qcGen ([S] -> Vector S
forall a. Unbox a => [a] -> Vector a
V.fromList [S]
ss)

-- | Check that 'fillInWindow'
--
-- 1. does not decrease the count of active slots in the given window
-- 2. returns exactly the amount of activated slots
-- 3. never leaves less than the requested amount of slots in the given
--    window
--
prop_fillInWindow :: FillInWindowSetup -> QC.Property
prop_fillInWindow :: FillInWindowSetup -> Property
prop_fillInWindow
        (FillInWindowSetup
          (SomePol ProxyPol pol
pol)
          Int
k
          Int
szW
          QCGen
qcGen
          Vector S
v
        ) = QCGen -> (forall {s}. STGenM QCGen s -> ST s Property) -> Property
forall g a.
RandomGen g =>
g -> (forall s. STGenM g s -> ST s a) -> a
R.runSTGen_ QCGen
qcGen ((forall {s}. STGenM QCGen s -> ST s Property) -> Property)
-> (forall {s}. STGenM QCGen s -> ST s Property) -> Property
forall a b. (a -> b) -> a -> b
$ \STGenM QCGen s
g -> do
    MVector s S
vmv <- Vector S -> ST s (MVector (PrimState (ST s)) S)
forall a (m :: * -> *).
(Unbox a, PrimMonad m) =>
Vector a -> m (MVector (PrimState m) a)
V.thaw Vector S
v
    let mv :: MVector Any 'SlotE s S
mv = MVector s S -> MVector Any 'SlotE s S
forall {k} {k1} (base :: k) (elem :: k1) s a.
MVector s a -> MVector base elem s a
C.MVector MVector s S
vmv
        szV :: Int
szV = Vector S -> Int
forall a. Unbox a => Vector a -> Int
V.length Vector S
v
    Int
actives0 <- Count Any (PreImage pol 'ActiveSlotE) Other -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount (Count Any (PreImage pol 'ActiveSlotE) Other -> Int)
-> ST s (Count Any (PreImage pol 'ActiveSlotE) Other) -> ST s Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProxyPol pol
-> MVector Any 'SlotE s S
-> ST s (Count Any (PreImage pol 'ActiveSlotE) Other)
forall (pol :: Pol) (proxy :: Pol -> *) base s.
POL pol =>
proxy pol
-> MVector base 'SlotE s S
-> ST s (Var base (PreImage pol 'ActiveSlotE))
BV.countActivesInMV ProxyPol pol
pol MVector Any 'SlotE s S
mv
    Int
c <- Count Any (PreImage pol 'ActiveSlotE) Other -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount (Count Any (PreImage pol 'ActiveSlotE) Other -> Int)
-> ST s (Count Any (PreImage pol 'ActiveSlotE) Other) -> ST s Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProxyPol pol
-> SomeDensityWindow pol
-> STGenM QCGen s
-> MVector Any 'SlotE s S
-> ST s (Count Any (PreImage pol 'ActiveSlotE) Other)
forall (proxy :: Pol -> *) (pol :: Pol) base g s.
(POL pol, StatefulGen g (ST s)) =>
proxy pol
-> SomeDensityWindow pol
-> g
-> MVector base 'SlotE s S
-> ST s (Var base (PreImage pol 'ActiveSlotE))
BV.fillInWindow ProxyPol pol
pol (Count Any (PreImage pol 'ActiveSlotE) Other
-> Size Any 'SlotE -> SomeDensityWindow pol
forall (pol :: Pol) slidingWindow.
Var slidingWindow (PreImage pol 'ActiveSlotE)
-> Size slidingWindow 'SlotE -> SomeDensityWindow pol
BV.SomeDensityWindow (Int -> Count Any (PreImage pol 'ActiveSlotE) Other
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
k) (Int -> Size Any 'SlotE
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
szW)) STGenM QCGen s
g MVector Any 'SlotE s S
mv
    Int
actives1 <- Count Any (PreImage pol 'ActiveSlotE) Other -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount (Count Any (PreImage pol 'ActiveSlotE) Other -> Int)
-> ST s (Count Any (PreImage pol 'ActiveSlotE) Other) -> ST s Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProxyPol pol
-> MVector Any 'SlotE s S
-> ST s (Count Any (PreImage pol 'ActiveSlotE) Other)
forall (pol :: Pol) (proxy :: Pol -> *) base s.
POL pol =>
proxy pol
-> MVector base 'SlotE s S
-> ST s (Var base (PreImage pol 'ActiveSlotE))
BV.countActivesInMV ProxyPol pol
pol MVector Any 'SlotE s S
mv
    Vector S
mvFrozen <- MVector (PrimState (ST s)) S -> ST s (Vector S)
forall a (m :: * -> *).
(Unbox a, PrimMonad m) =>
MVector (PrimState m) a -> m (Vector a)
V.freeze MVector s S
MVector (PrimState (ST s)) S
vmv
    Property -> ST s Property
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> ST s Property) -> Property -> ST s Property
forall a b. (a -> b) -> a -> b
$
        TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (ProxyPol pol -> TestName
forall (pol :: Pol) (proxy :: Pol -> *).
TestPOL pol =>
proxy pol -> TestName
forall (proxy :: Pol -> *). proxy pol -> TestName
showPol ProxyPol pol
pol) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (TestName
"actives0 = " TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> TestName
forall a. Show a => a -> TestName
show Int
actives0) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (TestName
"actives1 = " TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> TestName
forall a. Show a => a -> TestName
show Int
actives1) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (TestName
"szV = " TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> TestName
forall a. Show a => a -> TestName
show Int
szV) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (TestName
"v = " TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> TestName
show (Vector S -> TestName
showBitVector Vector S
mvFrozen)) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$

        (TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample TestName
"actives0 <= actives1" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Int
actives0 Int -> Int -> Property
forall a. (Ord a, Show a) => a -> a -> Property
`QC.le` Int
actives1)
        Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
QC..&&.
        (TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample TestName
"c == actives1" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Int
c Int -> Int -> Property
forall a. (Eq a, Show a) => a -> a -> Property
QC.=== Int
actives1)
        Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
QC..&&.
        (TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample TestName
"k <= actives1 + szW - szV" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Int
k Int -> Int -> Property
forall a. (Ord a, Show a) => a -> a -> Property
`QC.le` Int
actives1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
szW Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
szV)