{-# LANGUAGE TypeApplications #-}

-- | Test properties for the weighted Fait-Accompli committee selection model
module Test.Consensus.Committee.WFALS.Model.Test (tests) where

import Data.List (mapAccumR)
import qualified Data.Map.Strict as Map
import Data.Ratio ((%))
import qualified Data.Set as Set
import Data.Word (Word64)
import Numeric.Natural (minusNaturalMaybe)
import Test.Consensus.Committee.WFALS.Model
  ( IsStake (..)
  , NumSeats
  , Stake (..)
  , StakeDistr
  , StakeRole (..)
  , StakeType (..)
  , VoterId
  , adjustStake
  , coerceStake
  , stakeDistrToDecreasingStakes
  , stakeDistrTotalStake
  , weightedFaitAccompliPersistentSeats
  , weightedFaitAccompliThreshold
  )
import Test.QuickCheck
  ( Arbitrary (..)
  , Gen
  , Positive (..)
  , Property
  , Testable (..)
  , choose
  , counterexample
  , forAll
  , sized
  , tabulate
  , vectorOf
  , (===)
  , (==>)
  )
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.QuickCheck (testProperty)
import Test.Util.TestEnv (adjustQuickCheckTests)

-- * Property tests

-- ** Generators

-- | Generate a random stake as a Rational number
genStake :: Gen (Stake Ledger Global)
genStake :: Gen (Stake Ledger Global)
genStake = do
  Positive num <- Gen (Positive Integer)
forall a. Arbitrary a => Gen a
arbitrary
  Positive den <- arbitrary
  pure (StakeLedgerGlobal (num % den))

-- | Generate a non-empty list of unique voter IDs of a given size.
genUniqueVoterIds :: Int -> Gen [VoterId]
genUniqueVoterIds :: Int -> Gen [VoterId]
genUniqueVoterIds Int
size =
  (Word64 -> VoterId) -> [Word64] -> [VoterId]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Word64 -> VoterId
forall a. Show a => a -> VoterId
show ([Word64] -> [VoterId]) -> Gen [Word64] -> Gen [VoterId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Set Word64 -> Gen [Word64]
forall {t}. (Eq t, Num t) => t -> Set Word64 -> Gen [Word64]
go Int
size Set Word64
forall a. Set a
Set.empty
 where
  go :: t -> Set Word64 -> Gen [Word64]
go t
0 Set Word64
acc =
    [Word64] -> Gen [Word64]
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set Word64 -> [Word64]
forall a. Set a -> [a]
Set.toList Set Word64
acc)
  go t
k Set Word64
acc = do
    voterId <- (Word64, Word64) -> Gen Word64
forall a. Random a => (a, a) -> Gen a
choose (Word64
0, Word64
forall a. Bounded a => a
maxBound :: Word64)
    if voterId `Set.member` acc
      then
        go k acc
      else do
        rest <- go (k - 1) (Set.insert voterId acc)
        pure (voterId : rest)

-- | Generate a non-empty random stake distribution of a given size
--
-- NOTE: the size is shifted up by one to ensure non-emptiness.
genStakeDistr :: Int -> Gen (StakeDistr Ledger Global)
genStakeDistr :: Int -> Gen (StakeDistr Ledger Global)
genStakeDistr Int
size = do
  ids <- Int -> Gen [VoterId]
genUniqueVoterIds (Int -> Int
forall a. Enum a => a -> a
succ Int
size)
  stakes <- vectorOf (succ size) genStake
  pure (Map.fromList (zip ids stakes))

-- * Property helpers

-- | Helper to generate stake distributions along with a number of seats that
-- could possibly exceed the number of nodes in the stake distribution.
forAllStakeDistrAndNumSeats ::
  (StakeDistr Ledger Global -> NumSeats Global -> Property) ->
  Property
forAllStakeDistrAndNumSeats :: (StakeDistr Ledger Global -> NumSeats Global -> Property)
-> Property
forAllStakeDistrAndNumSeats StakeDistr Ledger Global -> NumSeats Global -> Property
p =
  Gen (StakeDistr Ledger Global)
-> (StakeDistr Ledger Global -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ((Int -> Gen (StakeDistr Ledger Global))
-> Gen (StakeDistr Ledger Global)
forall a. (Int -> Gen a) -> Gen a
sized Int -> Gen (StakeDistr Ledger Global)
genStakeDistr) ((StakeDistr Ledger Global -> Property) -> Property)
-> (StakeDistr Ledger Global -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \StakeDistr Ledger Global
stakeDistr -> do
    let numNodes :: Integer
numNodes = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (StakeDistr Ledger Global -> Int
forall k a. Map k a -> Int
Map.size StakeDistr Ledger Global
stakeDistr)
    -- generate a number of seats that could possibly exceed the number of nodes
    let genNumSeats :: Gen Natural
genNumSeats = Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Integer -> Natural) -> Gen Integer -> Gen Natural
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer, Integer) -> Gen Integer
forall a. Random a => (a, a) -> Gen a
choose (Integer
1, Integer
numNodes Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)
    Gen Natural -> (Natural -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll Gen Natural
genNumSeats ((Natural -> Property) -> Property)
-> (Natural -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Natural
numSeats -> StakeDistr Ledger Global -> NumSeats Global -> Property
p StakeDistr Ledger Global
stakeDistr Natural
NumSeats Global
numSeats

-- | Tabulate the target number of seats
tabulateTargetNumSeats :: NumSeats Global -> Property -> Property
tabulateTargetNumSeats :: NumSeats Global -> Property -> Property
tabulateTargetNumSeats NumSeats Global
numSeats =
  VoterId -> [VoterId] -> Property -> Property
forall prop.
Testable prop =>
VoterId -> [VoterId] -> prop -> Property
tabulate VoterId
"Target number of seats" [VoterId
bucket]
 where
  -- Divide in buckets of 10
  bucket :: VoterId
bucket
    | Natural
lower Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
upper = Natural -> VoterId
forall a. Show a => a -> VoterId
show Natural
lower
    | Bool
otherwise = Natural -> VoterId
forall a. Show a => a -> VoterId
show Natural
lower VoterId -> VoterId -> VoterId
forall a. Semigroup a => a -> a -> a
<> VoterId
"-" VoterId -> VoterId -> VoterId
forall a. Semigroup a => a -> a -> a
<> Natural -> VoterId
forall a. Show a => a -> VoterId
show Natural
upper
  lower :: Natural
lower = (Natural
NumSeats Global
numSeats Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`div` Natural
10) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
10
  upper :: Natural
upper = Natural
lower Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
9

-- | Tabulate the size of a stake distribution
tabulateStakeDistrSize :: StakeDistr Ledger Global -> Property -> Property
tabulateStakeDistrSize :: StakeDistr Ledger Global -> Property -> Property
tabulateStakeDistrSize StakeDistr Ledger Global
stakeDistr =
  VoterId -> [VoterId] -> Property -> Property
forall prop.
Testable prop =>
VoterId -> [VoterId] -> prop -> Property
tabulate VoterId
"Stake distribution size" [VoterId
bucket]
 where
  -- Divide in buckets of 10
  bucket :: VoterId
bucket
    | Int
lower Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
upper = Int -> VoterId
forall a. Show a => a -> VoterId
show Int
lower
    | Bool
otherwise = Int -> VoterId
forall a. Show a => a -> VoterId
show Int
lower VoterId -> VoterId -> VoterId
forall a. Semigroup a => a -> a -> a
<> VoterId
"-" VoterId -> VoterId -> VoterId
forall a. Semigroup a => a -> a -> a
<> Int -> VoterId
forall a. Show a => a -> VoterId
show Int
upper
  lower :: Int
lower = (Int
size Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
10) Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
10
  upper :: Int
upper = Int
lower Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
9
  size :: Int
size = StakeDistr Ledger Global -> Int
forall k a. Map k a -> Int
Map.size StakeDistr Ledger Global
stakeDistr

-- | Tabulate whether we are asking for more seats than nodes in the stake
-- distribution or not
tabulateMoreSeatsThanNodes ::
  StakeDistr Ledger Global ->
  NumSeats Global ->
  Property ->
  Property
tabulateMoreSeatsThanNodes :: StakeDistr Ledger Global -> NumSeats Global -> Property -> Property
tabulateMoreSeatsThanNodes StakeDistr Ledger Global
stakeDistr NumSeats Global
numSeats =
  VoterId -> [VoterId] -> Property -> Property
forall prop.
Testable prop =>
VoterId -> [VoterId] -> prop -> Property
tabulate
    VoterId
"More target seats than nodes"
    [ Bool -> VoterId
forall a. Show a => a -> VoterId
show (Natural
NumSeats Global
numSeats Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (StakeDistr Ledger Global -> Int
forall k a. Map k a -> Int
Map.size StakeDistr Ledger Global
stakeDistr))
    ]

-- | Tabulate the ratio of persistent to non-persistent seats as the percentage
-- of persistent seats out of the total number of seats.
tabulatePersistentToNonPersistentRatio ::
  NumSeats Global ->
  NumSeats Global ->
  Property ->
  Property
tabulatePersistentToNonPersistentRatio :: NumSeats Global -> NumSeats Global -> Property -> Property
tabulatePersistentToNonPersistentRatio
  NumSeats Global
numPersistentSeats
  NumSeats Global
numNonPersistentSeats =
    VoterId -> [VoterId] -> Property -> Property
forall prop.
Testable prop =>
VoterId -> [VoterId] -> prop -> Property
tabulate VoterId
"Persistent to non-persistent seat ratio" [VoterId
bucket]
   where
    -- Divide buckets in 10% increments
    bucket :: VoterId
bucket
      | Natural
lower Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
upper = Natural -> VoterId
forall a. Show a => a -> VoterId
show Natural
lower VoterId -> VoterId -> VoterId
forall a. Semigroup a => a -> a -> a
<> VoterId
"%"
      | Bool
otherwise = Natural -> VoterId
forall a. Show a => a -> VoterId
show Natural
lower VoterId -> VoterId -> VoterId
forall a. Semigroup a => a -> a -> a
<> VoterId
"%-" VoterId -> VoterId -> VoterId
forall a. Semigroup a => a -> a -> a
<> Natural -> VoterId
forall a. Show a => a -> VoterId
show Natural
upper VoterId -> VoterId -> VoterId
forall a. Semigroup a => a -> a -> a
<> VoterId
"%"
    lower :: Natural
lower = (Natural
NumSeats Global
numPersistentSeats Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
100) Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`div` Natural
totalSeats Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`div` Natural
10 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
10
    upper :: Natural
upper = Natural -> Natural -> Natural
forall a. Ord a => a -> a -> a
min Natural
100 (Natural
lower Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
10)
    totalSeats :: Natural
totalSeats = Natural
NumSeats Global
numPersistentSeats Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
NumSeats Global
numNonPersistentSeats

-- ** Properties

-- | Stakes returned by 'stakeDistrToDecreasingStakes' are non-increasing
prop_stakeDistrDecreasingStakes :: Property
prop_stakeDistrDecreasingStakes :: Property
prop_stakeDistrDecreasingStakes =
  Gen (StakeDistr Ledger Global)
-> (StakeDistr Ledger Global -> Bool) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ((Int -> Gen (StakeDistr Ledger Global))
-> Gen (StakeDistr Ledger Global)
forall a. (Int -> Gen a) -> Gen a
sized Int -> Gen (StakeDistr Ledger Global)
genStakeDistr) ((StakeDistr Ledger Global -> Bool) -> Property)
-> (StakeDistr Ledger Global -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ \StakeDistr Ledger Global
stakeDistr -> do
    let stakes :: [Stake Ledger Global]
stakes = ((VoterId, Stake Ledger Global) -> Stake Ledger Global)
-> [(VoterId, Stake Ledger Global)] -> [Stake Ledger Global]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (VoterId, Stake Ledger Global) -> Stake Ledger Global
forall a b. (a, b) -> b
snd (StakeDistr Ledger Global -> [(VoterId, Stake Ledger Global)]
forall (sr :: StakeRole) (st :: StakeType).
IsStake (Stake sr st) =>
StakeDistr sr st -> [(VoterId, Stake sr st)]
stakeDistrToDecreasingStakes StakeDistr Ledger Global
stakeDistr)
    case [Stake Ledger Global]
stakes of
      [] -> Bool
True -- vacuously true for empty stake distributions
      (Stake Ledger Global
_ : [Stake Ledger Global]
rest) -> [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((Stake Ledger Global -> Stake Ledger Global -> Bool)
-> [Stake Ledger Global] -> [Stake Ledger Global] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Stake Ledger Global -> Stake Ledger Global -> Bool
forall a. Ord a => a -> a -> Bool
(>=) [Stake Ledger Global]
stakes [Stake Ledger Global]
rest)

-- | Persistent seats returned by 'weightedFaitAccompliPersistentSeats' never
-- exceed the requested number of seats.
prop_weightedFaitAccompliPersistentSeats_persistentSeatsRespectNumSeats :: Property
prop_weightedFaitAccompliPersistentSeats_persistentSeatsRespectNumSeats :: Property
prop_weightedFaitAccompliPersistentSeats_persistentSeatsRespectNumSeats =
  (StakeDistr Ledger Global -> NumSeats Global -> Property)
-> Property
forAllStakeDistrAndNumSeats ((StakeDistr Ledger Global -> NumSeats Global -> Property)
 -> Property)
-> (StakeDistr Ledger Global -> NumSeats Global -> Property)
-> Property
forall a b. (a -> b) -> a -> b
$ \StakeDistr Ledger Global
stakeDistr NumSeats Global
numSeats -> do
    let (StakeDistr Weight Persistent
persistentSeats, NumSeats Residual
numNonPersistentSeats, StakeDistr Ledger Residual
_) =
          NumSeats Global
-> StakeDistr Ledger Global
-> (StakeDistr Weight Persistent, NumSeats Residual,
    StakeDistr Ledger Residual)
weightedFaitAccompliPersistentSeats NumSeats Global
numSeats StakeDistr Ledger Global
stakeDistr
    let numPersistentSeats :: Natural
numPersistentSeats = Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (StakeDistr Weight Persistent -> Int
forall k a. Map k a -> Int
Map.size StakeDistr Weight Persistent
persistentSeats)
    NumSeats Global -> Property -> Property
tabulateTargetNumSeats NumSeats Global
numSeats
      (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StakeDistr Ledger Global -> Property -> Property
tabulateStakeDistrSize StakeDistr Ledger Global
stakeDistr
      (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NumSeats Global -> NumSeats Global -> Property -> Property
tabulatePersistentToNonPersistentRatio Natural
NumSeats Global
numPersistentSeats Natural
NumSeats Global
numNonPersistentSeats
      (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ VoterId -> Bool -> Property
forall prop. Testable prop => VoterId -> prop -> Property
counterexample
        ( [VoterId] -> VoterId
unlines
            [ VoterId
"Total requested seats: " VoterId -> VoterId -> VoterId
forall a. Semigroup a => a -> a -> a
<> Natural -> VoterId
forall a. Show a => a -> VoterId
show Natural
NumSeats Global
numSeats
            , VoterId
"Number of persistent seats selected: " VoterId -> VoterId -> VoterId
forall a. Semigroup a => a -> a -> a
<> Natural -> VoterId
forall a. Show a => a -> VoterId
show Natural
numPersistentSeats
            , VoterId
"Persistent seats selected: " VoterId -> VoterId -> VoterId
forall a. Semigroup a => a -> a -> a
<> StakeDistr Weight Persistent -> VoterId
forall a. Show a => a -> VoterId
show StakeDistr Weight Persistent
persistentSeats
            ]
        )
      (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ Natural
numPersistentSeats Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= Natural
NumSeats Global
numSeats

-- | The stake of a persistent seat returned by
-- 'weightedFaitAccompliPersistentSeats' is never smaller than the stake of any
-- of the remaining the nodes in the residual stake distribution.
prop_weightedFaitAccompliPersistentSeats_persistentSeatsHaveLargeStake :: Property
prop_weightedFaitAccompliPersistentSeats_persistentSeatsHaveLargeStake :: Property
prop_weightedFaitAccompliPersistentSeats_persistentSeatsHaveLargeStake =
  (StakeDistr Ledger Global -> NumSeats Global -> Property)
-> Property
forAllStakeDistrAndNumSeats ((StakeDistr Ledger Global -> NumSeats Global -> Property)
 -> Property)
-> (StakeDistr Ledger Global -> NumSeats Global -> Property)
-> Property
forall a b. (a -> b) -> a -> b
$ \StakeDistr Ledger Global
stakeDistr NumSeats Global
numSeats -> do
    let (StakeDistr Weight Persistent
persistentSeats, NumSeats Residual
numNonPersistentSeats, StakeDistr Ledger Residual
residualStakeDistr) =
          NumSeats Global
-> StakeDistr Ledger Global
-> (StakeDistr Weight Persistent, NumSeats Residual,
    StakeDistr Ledger Residual)
weightedFaitAccompliPersistentSeats NumSeats Global
numSeats StakeDistr Ledger Global
stakeDistr
    let numPersistentSeats :: Natural
numPersistentSeats = Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (StakeDistr Weight Persistent -> Int
forall k a. Map k a -> Int
Map.size StakeDistr Weight Persistent
persistentSeats)
    let persistentStakes :: [Stake Weight Persistent]
persistentStakes = StakeDistr Weight Persistent -> [Stake Weight Persistent]
forall k a. Map k a -> [a]
Map.elems StakeDistr Weight Persistent
persistentSeats
    let residualStakes :: [Stake Ledger Residual]
residualStakes = StakeDistr Ledger Residual -> [Stake Ledger Residual]
forall k a. Map k a -> [a]
Map.elems StakeDistr Ledger Residual
residualStakeDistr
    StakeDistr Ledger Global -> Property -> Property
tabulateStakeDistrSize StakeDistr Ledger Global
stakeDistr
      (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NumSeats Global -> Property -> Property
tabulateTargetNumSeats NumSeats Global
numSeats
      (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StakeDistr Ledger Global -> NumSeats Global -> Property -> Property
tabulateMoreSeatsThanNodes StakeDistr Ledger Global
stakeDistr NumSeats Global
numSeats
      (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NumSeats Global -> NumSeats Global -> Property -> Property
tabulatePersistentToNonPersistentRatio Natural
NumSeats Global
numPersistentSeats Natural
NumSeats Global
numNonPersistentSeats
      (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ VoterId -> Property -> Property
forall prop. Testable prop => VoterId -> prop -> Property
counterexample
        ( [VoterId] -> VoterId
unlines
            [ VoterId
"Persistent seats: " VoterId -> VoterId -> VoterId
forall a. Semigroup a => a -> a -> a
<> StakeDistr Weight Persistent -> VoterId
forall a. Show a => a -> VoterId
show StakeDistr Weight Persistent
persistentSeats
            , VoterId
"Residual stake distribution: " VoterId -> VoterId -> VoterId
forall a. Semigroup a => a -> a -> a
<> StakeDistr Ledger Residual -> VoterId
forall a. Show a => a -> VoterId
show StakeDistr Ledger Residual
residualStakeDistr
            , VoterId
"Min persistent stake: " VoterId -> VoterId -> VoterId
forall a. Semigroup a => a -> a -> a
<> Stake Weight Persistent -> VoterId
forall a. Show a => a -> VoterId
show ([Stake Weight Persistent] -> Stake Weight Persistent
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [Stake Weight Persistent]
persistentStakes)
            , VoterId
"Max residual stake: " VoterId -> VoterId -> VoterId
forall a. Semigroup a => a -> a -> a
<> Stake Ledger Residual -> VoterId
forall a. Show a => a -> VoterId
show ([Stake Ledger Residual] -> Stake Ledger Residual
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Stake Ledger Residual]
residualStakes)
            ]
        )
      (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not ([Stake Weight Persistent] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Stake Weight Persistent]
persistentStakes)
        Bool -> Bool -> Bool
&& Bool -> Bool
not ([Stake Ledger Residual] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Stake Ledger Residual]
residualStakes)
      Bool -> Bool -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> [Rational] -> Rational
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum (Stake Weight Persistent -> Rational
forall stake. IsStake stake => stake -> Rational
stakeToRational (Stake Weight Persistent -> Rational)
-> [Stake Weight Persistent] -> [Rational]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Stake Weight Persistent]
persistentStakes)
        Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
>= [Rational] -> Rational
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Stake Ledger Residual -> Rational
forall stake. IsStake stake => stake -> Rational
stakeToRational (Stake Ledger Residual -> Rational)
-> [Stake Ledger Residual] -> [Rational]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Stake Ledger Residual]
residualStakes)

-- | The total stake for the persistent are residual stake distributions
-- returned by 'weightedFaitAccompliPersistentSeats' adds up to the original
-- total stake.
prop_weightedFaitAccompliPersistentSeats_totalStakePreserved :: Property
prop_weightedFaitAccompliPersistentSeats_totalStakePreserved :: Property
prop_weightedFaitAccompliPersistentSeats_totalStakePreserved =
  (StakeDistr Ledger Global -> NumSeats Global -> Property)
-> Property
forAllStakeDistrAndNumSeats ((StakeDistr Ledger Global -> NumSeats Global -> Property)
 -> Property)
-> (StakeDistr Ledger Global -> NumSeats Global -> Property)
-> Property
forall a b. (a -> b) -> a -> b
$ \StakeDistr Ledger Global
stakeDistr NumSeats Global
numSeats -> do
    let (StakeDistr Weight Persistent
persistentSeats, NumSeats Residual
numNonPersistentSeats, StakeDistr Ledger Residual
residualStakeDistr) =
          NumSeats Global
-> StakeDistr Ledger Global
-> (StakeDistr Weight Persistent, NumSeats Residual,
    StakeDistr Ledger Residual)
weightedFaitAccompliPersistentSeats NumSeats Global
numSeats StakeDistr Ledger Global
stakeDistr
    let numPersistentSeats :: Natural
numPersistentSeats = Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (StakeDistr Weight Persistent -> Int
forall k a. Map k a -> Int
Map.size StakeDistr Weight Persistent
persistentSeats)
    let totalOriginalStake :: Stake Ledger Global
totalOriginalStake = StakeDistr Ledger Global -> Stake Ledger Global
forall (sr :: StakeRole) (st :: StakeType).
IsStake (Stake sr st) =>
StakeDistr sr st -> Stake sr st
stakeDistrTotalStake StakeDistr Ledger Global
stakeDistr
    let totalPersistentStake :: Stake Weight Persistent
totalPersistentStake = StakeDistr Weight Persistent -> Stake Weight Persistent
forall (sr :: StakeRole) (st :: StakeType).
IsStake (Stake sr st) =>
StakeDistr sr st -> Stake sr st
stakeDistrTotalStake StakeDistr Weight Persistent
persistentSeats
    let totalResidualStake :: Stake Ledger Residual
totalResidualStake = StakeDistr Ledger Residual -> Stake Ledger Residual
forall (sr :: StakeRole) (st :: StakeType).
IsStake (Stake sr st) =>
StakeDistr sr st -> Stake sr st
stakeDistrTotalStake StakeDistr Ledger Residual
residualStakeDistr
    let totalCombinedStake :: Rational
totalCombinedStake =
          Stake Weight Persistent -> Rational
forall stake. IsStake stake => stake -> Rational
stakeToRational Stake Weight Persistent
totalPersistentStake
            Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ Stake Ledger Residual -> Rational
forall stake. IsStake stake => stake -> Rational
stakeToRational Stake Ledger Residual
totalResidualStake
    StakeDistr Ledger Global -> Property -> Property
tabulateStakeDistrSize StakeDistr Ledger Global
stakeDistr
      (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NumSeats Global -> Property -> Property
tabulateTargetNumSeats NumSeats Global
numSeats
      (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StakeDistr Ledger Global -> NumSeats Global -> Property -> Property
tabulateMoreSeatsThanNodes StakeDistr Ledger Global
stakeDistr NumSeats Global
numSeats
      (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NumSeats Global -> NumSeats Global -> Property -> Property
tabulatePersistentToNonPersistentRatio Natural
NumSeats Global
numPersistentSeats Natural
NumSeats Global
numNonPersistentSeats
      (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ VoterId -> Property -> Property
forall prop. Testable prop => VoterId -> prop -> Property
counterexample
        ( [VoterId] -> VoterId
unlines
            [ VoterId
"Total original stake: " VoterId -> VoterId -> VoterId
forall a. Semigroup a => a -> a -> a
<> Stake Ledger Global -> VoterId
forall a. Show a => a -> VoterId
show Stake Ledger Global
totalOriginalStake
            , VoterId
"Total persistent stake: " VoterId -> VoterId -> VoterId
forall a. Semigroup a => a -> a -> a
<> Stake Weight Persistent -> VoterId
forall a. Show a => a -> VoterId
show Stake Weight Persistent
totalPersistentStake
            , VoterId
"Total residual stake: " VoterId -> VoterId -> VoterId
forall a. Semigroup a => a -> a -> a
<> Stake Ledger Residual -> VoterId
forall a. Show a => a -> VoterId
show Stake Ledger Residual
totalResidualStake
            , VoterId
"Total combined stake: " VoterId -> VoterId -> VoterId
forall a. Semigroup a => a -> a -> a
<> Rational -> VoterId
forall a. Show a => a -> VoterId
show Rational
totalCombinedStake
            ]
        )
      (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Stake Ledger Global -> Rational
forall stake. IsStake stake => stake -> Rational
stakeToRational Stake Ledger Global
totalOriginalStake Rational -> Rational -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Rational
totalCombinedStake

-- | The number of non-persistent seats to be selected from the residual stake
-- distribution returned by 'weightedFaitAccompliPersistentSeats' adds up to the
-- original number of seats minus the number of persistent seats.
prop_weightedFaitAccompliPersistentSeats_nonPersistentSeatsCountCorrect :: Property
prop_weightedFaitAccompliPersistentSeats_nonPersistentSeatsCountCorrect :: Property
prop_weightedFaitAccompliPersistentSeats_nonPersistentSeatsCountCorrect =
  (StakeDistr Ledger Global -> NumSeats Global -> Property)
-> Property
forAllStakeDistrAndNumSeats ((StakeDistr Ledger Global -> NumSeats Global -> Property)
 -> Property)
-> (StakeDistr Ledger Global -> NumSeats Global -> Property)
-> Property
forall a b. (a -> b) -> a -> b
$ \StakeDistr Ledger Global
stakeDistr NumSeats Global
numSeats -> do
    let (StakeDistr Weight Persistent
persistentSeats, NumSeats Residual
numNonPersistentSeats, StakeDistr Ledger Residual
_) =
          NumSeats Global
-> StakeDistr Ledger Global
-> (StakeDistr Weight Persistent, NumSeats Residual,
    StakeDistr Ledger Residual)
weightedFaitAccompliPersistentSeats NumSeats Global
numSeats StakeDistr Ledger Global
stakeDistr
    let numPersistentSeats :: Natural
numPersistentSeats = Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (StakeDistr Weight Persistent -> Int
forall k a. Map k a -> Int
Map.size StakeDistr Weight Persistent
persistentSeats)
    StakeDistr Ledger Global -> Property -> Property
tabulateStakeDistrSize StakeDistr Ledger Global
stakeDistr
      (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NumSeats Global -> Property -> Property
tabulateTargetNumSeats NumSeats Global
numSeats
      (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StakeDistr Ledger Global -> NumSeats Global -> Property -> Property
tabulateMoreSeatsThanNodes StakeDistr Ledger Global
stakeDistr NumSeats Global
numSeats
      (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NumSeats Global -> NumSeats Global -> Property -> Property
tabulatePersistentToNonPersistentRatio Natural
NumSeats Global
numPersistentSeats Natural
NumSeats Global
numNonPersistentSeats
      (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ VoterId -> Property -> Property
forall prop. Testable prop => VoterId -> prop -> Property
counterexample
        ( [VoterId] -> VoterId
unlines
            [ VoterId
"Total requested seats: " VoterId -> VoterId -> VoterId
forall a. Semigroup a => a -> a -> a
<> Natural -> VoterId
forall a. Show a => a -> VoterId
show Natural
NumSeats Global
numSeats
            , VoterId
"Persistent seats selected: " VoterId -> VoterId -> VoterId
forall a. Semigroup a => a -> a -> a
<> Natural -> VoterId
forall a. Show a => a -> VoterId
show Natural
numPersistentSeats
            , VoterId
"Non-persistent seats to select: " VoterId -> VoterId -> VoterId
forall a. Semigroup a => a -> a -> a
<> Natural -> VoterId
forall a. Show a => a -> VoterId
show Natural
numNonPersistentSeats
            ]
        )
      (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ case Natural -> Natural -> Maybe Natural
minusNaturalMaybe Natural
NumSeats Global
numSeats Natural
numPersistentSeats of
        Just Natural
n -> Natural
n Natural -> Natural -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Natural
numNonPersistentSeats
        Maybe Natural
Nothing -> Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
False

-- | None of the stakes in the residual stake distribution returned by
-- 'weightedFaitAccompliPersistentSeats' should qualify for the next persistent
-- seat according to the weighted Fait Accompli threshold.
prop_weightedFaitAccompliPersistentSeats_residualSeatsDoNotQualify :: Property
prop_weightedFaitAccompliPersistentSeats_residualSeatsDoNotQualify :: Property
prop_weightedFaitAccompliPersistentSeats_residualSeatsDoNotQualify =
  (StakeDistr Ledger Global -> NumSeats Global -> Property)
-> Property
forAllStakeDistrAndNumSeats ((StakeDistr Ledger Global -> NumSeats Global -> Property)
 -> Property)
-> (StakeDistr Ledger Global -> NumSeats Global -> Property)
-> Property
forall a b. (a -> b) -> a -> b
$ \StakeDistr Ledger Global
stakeDistr NumSeats Global
numSeats -> do
    let (StakeDistr Weight Persistent
persistentSeats, NumSeats Residual
numNonPersistentSeats, StakeDistr Ledger Residual
residualStakeDistr) =
          NumSeats Global
-> StakeDistr Ledger Global
-> (StakeDistr Weight Persistent, NumSeats Residual,
    StakeDistr Ledger Residual)
weightedFaitAccompliPersistentSeats NumSeats Global
numSeats StakeDistr Ledger Global
stakeDistr
    let numPersistentSeats :: Natural
numPersistentSeats =
          Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (StakeDistr Weight Persistent -> Int
forall k a. Map k a -> Int
Map.size StakeDistr Weight Persistent
persistentSeats)
    let addSeatIndex :: [(a, b)] -> [(a, b, Natural)]
addSeatIndex =
          ((Natural -> (a, b) -> (a, b, Natural))
 -> [Natural] -> [(a, b)] -> [(a, b, Natural)])
-> [Natural]
-> (Natural -> (a, b) -> (a, b, Natural))
-> [(a, b)]
-> [(a, b, Natural)]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Natural -> (a, b) -> (a, b, Natural))
-> [Natural] -> [(a, b)] -> [(a, b, Natural)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith [Natural
numPersistentSeats ..] ((Natural -> (a, b) -> (a, b, Natural))
 -> [(a, b)] -> [(a, b, Natural)])
-> (Natural -> (a, b) -> (a, b, Natural))
-> [(a, b)]
-> [(a, b, Natural)]
forall a b. (a -> b) -> a -> b
$
            \Natural
seatIndex (a
voterId, b
voterStake) ->
              (a
voterId, b
voterStake, Natural
seatIndex)
    let accumStakeR :: [(a, Stake Ledger Residual, c)]
-> [(a, Stake Ledger Residual, c, Stake Ledger Cumulative)]
accumStakeR =
          ((Stake Ledger Cumulative,
  [(a, Stake Ledger Residual, c, Stake Ledger Cumulative)])
 -> [(a, Stake Ledger Residual, c, Stake Ledger Cumulative)])
-> ([(a, Stake Ledger Residual, c)]
    -> (Stake Ledger Cumulative,
        [(a, Stake Ledger Residual, c, Stake Ledger Cumulative)]))
-> [(a, Stake Ledger Residual, c)]
-> [(a, Stake Ledger Residual, c, Stake Ledger Cumulative)]
forall a b.
(a -> b)
-> ([(a, Stake Ledger Residual, c)] -> a)
-> [(a, Stake Ledger Residual, c)]
-> b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Stake Ledger Cumulative,
 [(a, Stake Ledger Residual, c, Stake Ledger Cumulative)])
-> [(a, Stake Ledger Residual, c, Stake Ledger Cumulative)]
forall a b. (a, b) -> b
snd (([(a, Stake Ledger Residual, c)]
  -> (Stake Ledger Cumulative,
      [(a, Stake Ledger Residual, c, Stake Ledger Cumulative)]))
 -> [(a, Stake Ledger Residual, c)]
 -> [(a, Stake Ledger Residual, c, Stake Ledger Cumulative)])
-> ([(a, Stake Ledger Residual, c)]
    -> (Stake Ledger Cumulative,
        [(a, Stake Ledger Residual, c, Stake Ledger Cumulative)]))
-> [(a, Stake Ledger Residual, c)]
-> [(a, Stake Ledger Residual, c, Stake Ledger Cumulative)]
forall a b. (a -> b) -> a -> b
$
            ((Stake Ledger Cumulative
  -> (a, Stake Ledger Residual, c)
  -> (Stake Ledger Cumulative,
      (a, Stake Ledger Residual, c, Stake Ledger Cumulative)))
 -> Stake Ledger Cumulative
 -> [(a, Stake Ledger Residual, c)]
 -> (Stake Ledger Cumulative,
     [(a, Stake Ledger Residual, c, Stake Ledger Cumulative)]))
-> Stake Ledger Cumulative
-> (Stake Ledger Cumulative
    -> (a, Stake Ledger Residual, c)
    -> (Stake Ledger Cumulative,
        (a, Stake Ledger Residual, c, Stake Ledger Cumulative)))
-> [(a, Stake Ledger Residual, c)]
-> (Stake Ledger Cumulative,
    [(a, Stake Ledger Residual, c, Stake Ledger Cumulative)])
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Stake Ledger Cumulative
 -> (a, Stake Ledger Residual, c)
 -> (Stake Ledger Cumulative,
     (a, Stake Ledger Residual, c, Stake Ledger Cumulative)))
-> Stake Ledger Cumulative
-> [(a, Stake Ledger Residual, c)]
-> (Stake Ledger Cumulative,
    [(a, Stake Ledger Residual, c, Stake Ledger Cumulative)])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumR Stake Ledger Cumulative
0 ((Stake Ledger Cumulative
  -> (a, Stake Ledger Residual, c)
  -> (Stake Ledger Cumulative,
      (a, Stake Ledger Residual, c, Stake Ledger Cumulative)))
 -> [(a, Stake Ledger Residual, c)]
 -> (Stake Ledger Cumulative,
     [(a, Stake Ledger Residual, c, Stake Ledger Cumulative)]))
-> (Stake Ledger Cumulative
    -> (a, Stake Ledger Residual, c)
    -> (Stake Ledger Cumulative,
        (a, Stake Ledger Residual, c, Stake Ledger Cumulative)))
-> [(a, Stake Ledger Residual, c)]
-> (Stake Ledger Cumulative,
    [(a, Stake Ledger Residual, c, Stake Ledger Cumulative)])
forall a b. (a -> b) -> a -> b
$
              \Stake Ledger Cumulative
stakeAccR (a
voterId, Stake Ledger Residual
voterStake, c
seatIndex) ->
                let
                  stakeAccR' :: Stake Ledger Cumulative
stakeAccR' =
                    (Rational -> Rational)
-> Stake Ledger Cumulative -> Stake Ledger Cumulative
forall stake' stake.
(IsStake stake, IsStake stake') =>
(Rational -> Rational) -> stake -> stake'
adjustStake (Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ Stake Ledger Residual -> Rational
forall stake. IsStake stake => stake -> Rational
stakeToRational Stake Ledger Residual
voterStake) Stake Ledger Cumulative
stakeAccR
                 in
                  ( Stake Ledger Cumulative
stakeAccR'
                  ,
                    ( a
voterId
                    , Stake Ledger Residual
voterStake
                    , c
seatIndex
                    , Stake Ledger Cumulative
stakeAccR'
                    )
                  )
    let rightCumulativeDecreasingResidualStakes :: [(VoterId, Stake Ledger Residual, Natural,
  Stake Ledger Cumulative)]
rightCumulativeDecreasingResidualStakes =
          [(VoterId, Stake Ledger Residual, Natural)]
-> [(VoterId, Stake Ledger Residual, Natural,
     Stake Ledger Cumulative)]
forall {a} {c}.
[(a, Stake Ledger Residual, c)]
-> [(a, Stake Ledger Residual, c, Stake Ledger Cumulative)]
accumStakeR ([(VoterId, Stake Ledger Residual, Natural)]
 -> [(VoterId, Stake Ledger Residual, Natural,
      Stake Ledger Cumulative)])
-> [(VoterId, Stake Ledger Residual, Natural)]
-> [(VoterId, Stake Ledger Residual, Natural,
     Stake Ledger Cumulative)]
forall a b. (a -> b) -> a -> b
$
            [(VoterId, Stake Ledger Residual)]
-> [(VoterId, Stake Ledger Residual, Natural)]
forall {a} {b}. [(a, b)] -> [(a, b, Natural)]
addSeatIndex ([(VoterId, Stake Ledger Residual)]
 -> [(VoterId, Stake Ledger Residual, Natural)])
-> [(VoterId, Stake Ledger Residual)]
-> [(VoterId, Stake Ledger Residual, Natural)]
forall a b. (a -> b) -> a -> b
$
              StakeDistr Ledger Residual -> [(VoterId, Stake Ledger Residual)]
forall (sr :: StakeRole) (st :: StakeType).
IsStake (Stake sr st) =>
StakeDistr sr st -> [(VoterId, Stake sr st)]
stakeDistrToDecreasingStakes StakeDistr Ledger Residual
residualStakeDistr

    let judgments :: [(VoterId, Stake Ledger Residual, Natural, Stake Ledger Cumulative,
  Bool)]
judgments =
          ((VoterId, Stake Ledger Residual, Natural, Stake Ledger Cumulative)
 -> (VoterId, Stake Ledger Residual, Natural,
     Stake Ledger Cumulative, Bool))
-> [(VoterId, Stake Ledger Residual, Natural,
     Stake Ledger Cumulative)]
-> [(VoterId, Stake Ledger Residual, Natural,
     Stake Ledger Cumulative, Bool)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
            ( \(VoterId
voterIndex, Stake Ledger Residual
voterStake, Natural
seatIndex, Stake Ledger Cumulative
stakeAccum) ->
                ( VoterId
voterIndex
                , Stake Ledger Residual
voterStake
                , Natural
seatIndex
                , Stake Ledger Cumulative
stakeAccum
                , NumSeats Global
-> Natural
-> Stake Ledger Global
-> Stake Ledger Cumulative
-> Bool
weightedFaitAccompliThreshold
                    NumSeats Global
numSeats
                    Natural
seatIndex
                    -- Here we cast the stake from Residual to Global since
                    -- the Fait-Accompli threshold is supposed to be computed
                    -- on global stakes:
                    (forall stake' stake.
(IsStake stake, IsStake stake') =>
stake -> stake'
coerceStake @(Stake Ledger Global) Stake Ledger Residual
voterStake)
                    Stake Ledger Cumulative
stakeAccum
                )
            )
            [(VoterId, Stake Ledger Residual, Natural,
  Stake Ledger Cumulative)]
rightCumulativeDecreasingResidualStakes
    StakeDistr Ledger Global -> Property -> Property
tabulateStakeDistrSize StakeDistr Ledger Global
stakeDistr
      (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NumSeats Global -> Property -> Property
tabulateTargetNumSeats NumSeats Global
numSeats
      (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StakeDistr Ledger Global -> NumSeats Global -> Property -> Property
tabulateMoreSeatsThanNodes StakeDistr Ledger Global
stakeDistr NumSeats Global
numSeats
      (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NumSeats Global -> NumSeats Global -> Property -> Property
tabulatePersistentToNonPersistentRatio Natural
NumSeats Global
numPersistentSeats Natural
NumSeats Global
numNonPersistentSeats
      (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ VoterId -> Bool -> Property
forall prop. Testable prop => VoterId -> prop -> Property
counterexample
        ( [VoterId] -> VoterId
unlines
            [ VoterId
"Persistent seats selected: "
                VoterId -> VoterId -> VoterId
forall a. Semigroup a => a -> a -> a
<> StakeDistr Weight Persistent -> VoterId
forall a. Show a => a -> VoterId
show StakeDistr Weight Persistent
persistentSeats
            , VoterId
"Next persistent seat index: "
                VoterId -> VoterId -> VoterId
forall a. Semigroup a => a -> a -> a
<> Natural -> VoterId
forall a. Show a => a -> VoterId
show Natural
numPersistentSeats
            , VoterId
"Residual stakes with index, cumulative stake, and threshold judgments: "
                VoterId -> VoterId -> VoterId
forall a. Semigroup a => a -> a -> a
<> [(VoterId, Stake Ledger Residual, Natural, Stake Ledger Cumulative,
  Bool)]
-> VoterId
forall a. Show a => a -> VoterId
show [(VoterId, Stake Ledger Residual, Natural, Stake Ledger Cumulative,
  Bool)]
judgments
            ]
        )
      (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ ((VoterId, Stake Ledger Residual, Natural, Stake Ledger Cumulative,
  Bool)
 -> Bool)
-> [(VoterId, Stake Ledger Residual, Natural,
     Stake Ledger Cumulative, Bool)]
-> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all
        (\(VoterId
_, Stake Ledger Residual
_, Natural
_, Stake Ledger Cumulative
_, Bool
aboveThreshold) -> Bool -> Bool
not Bool
aboveThreshold)
        [(VoterId, Stake Ledger Residual, Natural, Stake Ledger Cumulative,
  Bool)]
judgments

-- | Test suite
tests :: TestTree
tests :: TestTree
tests =
  (Int -> Int) -> TestTree -> TestTree
adjustQuickCheckTests (Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
100) (TestTree -> TestTree) -> TestTree -> TestTree
forall a b. (a -> b) -> a -> b
$
    VoterId -> [TestTree] -> TestTree
testGroup
      VoterId
"weighted Fait-Accompli committee selection model property tests"
      [ VoterId -> Property -> TestTree
forall a. Testable a => VoterId -> a -> TestTree
testProperty
          VoterId
"prop_stakeDistrDecreasingStakes"
          Property
prop_stakeDistrDecreasingStakes
      , VoterId -> Property -> TestTree
forall a. Testable a => VoterId -> a -> TestTree
testProperty
          VoterId
"prop_weightedFaitAccompliPersistentSeats_persistentSeatsRespectNumSeats"
          Property
prop_weightedFaitAccompliPersistentSeats_persistentSeatsRespectNumSeats
      , VoterId -> Property -> TestTree
forall a. Testable a => VoterId -> a -> TestTree
testProperty
          VoterId
"prop_weightedFaitAccompliPersistentSeats_persistentSeatsHaveLargeStake"
          Property
prop_weightedFaitAccompliPersistentSeats_persistentSeatsHaveLargeStake
      , VoterId -> Property -> TestTree
forall a. Testable a => VoterId -> a -> TestTree
testProperty
          VoterId
"prop_weightedFaitAccompliPersistentSeats_totalStakePreserved"
          Property
prop_weightedFaitAccompliPersistentSeats_totalStakePreserved
      , VoterId -> Property -> TestTree
forall a. Testable a => VoterId -> a -> TestTree
testProperty
          VoterId
"prop_weightedFaitAccompliPersistentSeats_nonPersistentSeatsCountCorrect"
          Property
prop_weightedFaitAccompliPersistentSeats_nonPersistentSeatsCountCorrect
      , VoterId -> Property -> TestTree
forall a. Testable a => VoterId -> a -> TestTree
testProperty
          VoterId
"prop_weightedFaitAccompliPersistentSeats_residualSeatsDoNotQualify"
          Property
prop_weightedFaitAccompliPersistentSeats_residualSeatsDoNotQualify
      ]