{-# LANGUAGE TypeApplications #-}

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

import Data.List (mapAccumR)
import qualified Data.Map.Strict as Map
import Numeric.Natural (minusNaturalMaybe)
import Test.Consensus.Committee.WFALS.Model
  ( IsStake (..)
  , Stake (..)
  , StakeRole (..)
  , StakeType (..)
  , WFAError
  , adjustStake
  , coerceStake
  , stakeDistrToDecreasingStakes
  , stakeDistrTotalStake
  , weightedFaitAccompliPersistentSeats
  , weightedFaitAccompliThreshold
  )
import Test.Consensus.Committee.WFALS.Model.Utils
  ( forAllValidStakeDistrAndNumSeats
  , genStakeDistr
  , tabulatePersistentToNonPersistentRatio
  , tabulateStakeDistrSize
  , tabulateTargetNumSeats
  )
import Test.QuickCheck
  ( Property
  , Testable (..)
  , counterexample
  , forAll
  , sized
  , (===)
  , (==>)
  )
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.QuickCheck (testProperty)
import Test.Util.TestEnv (adjustQuickCheckTests)

-- * 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 tiebreaker :: String -> String -> Ordering
tiebreaker = String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
compare -- unfair tiebreaker
    let stakes :: [Stake Ledger Global]
stakes = ((String, Stake Ledger Global) -> Stake Ledger Global)
-> [(String, 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 (String, Stake Ledger Global) -> Stake Ledger Global
forall a b. (a, b) -> b
snd ((String -> String -> Ordering)
-> StakeDistr Ledger Global -> [(String, Stake Ledger Global)]
forall (sr :: StakeRole) (st :: StakeType).
IsStake (Stake sr st) =>
(String -> String -> Ordering)
-> StakeDistr sr st -> [(String, Stake sr st)]
stakeDistrToDecreasingStakes String -> String -> Ordering
tiebreaker 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
forAllValidStakeDistrAndNumSeats ((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 tiebreaker :: String -> String -> Ordering
tiebreaker = String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
compare -- unfair tiebreaker
    let (StakeDistr Weight Persistent
persistentSeats, NumSeats Residual
numNonPersistentSeats, StakeDistr Ledger Residual
_) =
          Either
  String
  (StakeDistr Weight Persistent, NumSeats Residual,
   StakeDistr Ledger Residual)
-> (StakeDistr Weight Persistent, NumSeats Residual,
    StakeDistr Ledger Residual)
forall a. Either String a -> a
expectSuccess (Either
   String
   (StakeDistr Weight Persistent, NumSeats Residual,
    StakeDistr Ledger Residual)
 -> (StakeDistr Weight Persistent, NumSeats Residual,
     StakeDistr Ledger Residual))
-> Either
     String
     (StakeDistr Weight Persistent, NumSeats Residual,
      StakeDistr Ledger Residual)
-> (StakeDistr Weight Persistent, NumSeats Residual,
    StakeDistr Ledger Residual)
forall a b. (a -> b) -> a -> b
$
            (String -> String -> Ordering)
-> NumSeats Global
-> StakeDistr Ledger Global
-> Either
     String
     (StakeDistr Weight Persistent, NumSeats Residual,
      StakeDistr Ledger Residual)
weightedFaitAccompliPersistentSeats
              String -> String -> Ordering
tiebreaker
              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
$ String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
        ( [String] -> String
unlines
            [ String
"Total requested seats: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Natural -> String
forall a. Show a => a -> String
show Natural
NumSeats Global
numSeats
            , String
"Number of persistent seats selected: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Natural -> String
forall a. Show a => a -> String
show Natural
numPersistentSeats
            , String
"Persistent seats selected: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> StakeDistr Weight Persistent -> String
forall a. Show a => a -> String
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
forAllValidStakeDistrAndNumSeats ((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 tiebreaker :: String -> String -> Ordering
tiebreaker = String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
compare -- unfair tiebreaker
    let (StakeDistr Weight Persistent
persistentSeats, NumSeats Residual
numNonPersistentSeats, StakeDistr Ledger Residual
residualStakeDistr) =
          Either
  String
  (StakeDistr Weight Persistent, NumSeats Residual,
   StakeDistr Ledger Residual)
-> (StakeDistr Weight Persistent, NumSeats Residual,
    StakeDistr Ledger Residual)
forall a. Either String a -> a
expectSuccess (Either
   String
   (StakeDistr Weight Persistent, NumSeats Residual,
    StakeDistr Ledger Residual)
 -> (StakeDistr Weight Persistent, NumSeats Residual,
     StakeDistr Ledger Residual))
-> Either
     String
     (StakeDistr Weight Persistent, NumSeats Residual,
      StakeDistr Ledger Residual)
-> (StakeDistr Weight Persistent, NumSeats Residual,
    StakeDistr Ledger Residual)
forall a b. (a -> b) -> a -> b
$
            (String -> String -> Ordering)
-> NumSeats Global
-> StakeDistr Ledger Global
-> Either
     String
     (StakeDistr Weight Persistent, NumSeats Residual,
      StakeDistr Ledger Residual)
weightedFaitAccompliPersistentSeats
              String -> String -> Ordering
tiebreaker
              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
. 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
$ String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
        ( [String] -> String
unlines
            [ String
"Persistent seats: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> StakeDistr Weight Persistent -> String
forall a. Show a => a -> String
show StakeDistr Weight Persistent
persistentSeats
            , String
"Residual stake distribution: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> StakeDistr Ledger Residual -> String
forall a. Show a => a -> String
show StakeDistr Ledger Residual
residualStakeDistr
            , String
"Min persistent stake: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Stake Weight Persistent -> String
forall a. Show a => a -> String
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)
            , String
"Max residual stake: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Stake Ledger Residual -> String
forall a. Show a => a -> String
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
forAllValidStakeDistrAndNumSeats ((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 tiebreaker :: String -> String -> Ordering
tiebreaker = String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
compare -- unfair tiebreaker
    let (StakeDistr Weight Persistent
persistentSeats, NumSeats Residual
numNonPersistentSeats, StakeDistr Ledger Residual
residualStakeDistr) =
          Either
  String
  (StakeDistr Weight Persistent, NumSeats Residual,
   StakeDistr Ledger Residual)
-> (StakeDistr Weight Persistent, NumSeats Residual,
    StakeDistr Ledger Residual)
forall a. Either String a -> a
expectSuccess (Either
   String
   (StakeDistr Weight Persistent, NumSeats Residual,
    StakeDistr Ledger Residual)
 -> (StakeDistr Weight Persistent, NumSeats Residual,
     StakeDistr Ledger Residual))
-> Either
     String
     (StakeDistr Weight Persistent, NumSeats Residual,
      StakeDistr Ledger Residual)
-> (StakeDistr Weight Persistent, NumSeats Residual,
    StakeDistr Ledger Residual)
forall a b. (a -> b) -> a -> b
$
            (String -> String -> Ordering)
-> NumSeats Global
-> StakeDistr Ledger Global
-> Either
     String
     (StakeDistr Weight Persistent, NumSeats Residual,
      StakeDistr Ledger Residual)
weightedFaitAccompliPersistentSeats
              String -> String -> Ordering
tiebreaker
              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
. 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
$ String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
        ( [String] -> String
unlines
            [ String
"Total original stake: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Stake Ledger Global -> String
forall a. Show a => a -> String
show Stake Ledger Global
totalOriginalStake
            , String
"Total persistent stake: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Stake Weight Persistent -> String
forall a. Show a => a -> String
show Stake Weight Persistent
totalPersistentStake
            , String
"Total residual stake: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Stake Ledger Residual -> String
forall a. Show a => a -> String
show Stake Ledger Residual
totalResidualStake
            , String
"Total combined stake: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Rational -> String
forall a. Show a => a -> String
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
forAllValidStakeDistrAndNumSeats ((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 tiebreaker :: String -> String -> Ordering
tiebreaker = String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
compare -- unfair tiebreaker
    let (StakeDistr Weight Persistent
persistentSeats, NumSeats Residual
numNonPersistentSeats, StakeDistr Ledger Residual
_) =
          Either
  String
  (StakeDistr Weight Persistent, NumSeats Residual,
   StakeDistr Ledger Residual)
-> (StakeDistr Weight Persistent, NumSeats Residual,
    StakeDistr Ledger Residual)
forall a. Either String a -> a
expectSuccess (Either
   String
   (StakeDistr Weight Persistent, NumSeats Residual,
    StakeDistr Ledger Residual)
 -> (StakeDistr Weight Persistent, NumSeats Residual,
     StakeDistr Ledger Residual))
-> Either
     String
     (StakeDistr Weight Persistent, NumSeats Residual,
      StakeDistr Ledger Residual)
-> (StakeDistr Weight Persistent, NumSeats Residual,
    StakeDistr Ledger Residual)
forall a b. (a -> b) -> a -> b
$
            (String -> String -> Ordering)
-> NumSeats Global
-> StakeDistr Ledger Global
-> Either
     String
     (StakeDistr Weight Persistent, NumSeats Residual,
      StakeDistr Ledger Residual)
weightedFaitAccompliPersistentSeats
              String -> String -> Ordering
tiebreaker
              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
. 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
$ String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
        ( [String] -> String
unlines
            [ String
"Total requested seats: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Natural -> String
forall a. Show a => a -> String
show Natural
NumSeats Global
numSeats
            , String
"Persistent seats selected: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Natural -> String
forall a. Show a => a -> String
show Natural
numPersistentSeats
            , String
"Non-persistent seats to select: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Natural -> String
forall a. Show a => a -> String
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
forAllValidStakeDistrAndNumSeats ((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 tiebreaker :: String -> String -> Ordering
tiebreaker = String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
compare -- unfair tiebreaker
    let (StakeDistr Weight Persistent
persistentSeats, NumSeats Residual
numNonPersistentSeats, StakeDistr Ledger Residual
residualStakeDistr) =
          Either
  String
  (StakeDistr Weight Persistent, NumSeats Residual,
   StakeDistr Ledger Residual)
-> (StakeDistr Weight Persistent, NumSeats Residual,
    StakeDistr Ledger Residual)
forall a. Either String a -> a
expectSuccess (Either
   String
   (StakeDistr Weight Persistent, NumSeats Residual,
    StakeDistr Ledger Residual)
 -> (StakeDistr Weight Persistent, NumSeats Residual,
     StakeDistr Ledger Residual))
-> Either
     String
     (StakeDistr Weight Persistent, NumSeats Residual,
      StakeDistr Ledger Residual)
-> (StakeDistr Weight Persistent, NumSeats Residual,
    StakeDistr Ledger Residual)
forall a b. (a -> b) -> a -> b
$
            (String -> String -> Ordering)
-> NumSeats Global
-> StakeDistr Ledger Global
-> Either
     String
     (StakeDistr Weight Persistent, NumSeats Residual,
      StakeDistr Ledger Residual)
weightedFaitAccompliPersistentSeats
              String -> String -> Ordering
tiebreaker
              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 :: [(String, Stake Ledger Residual, Natural, Stake Ledger Cumulative)]
rightCumulativeDecreasingResidualStakes =
          [(String, Stake Ledger Residual, Natural)]
-> [(String, Stake Ledger Residual, Natural,
     Stake Ledger Cumulative)]
forall {a} {c}.
[(a, Stake Ledger Residual, c)]
-> [(a, Stake Ledger Residual, c, Stake Ledger Cumulative)]
accumStakeR ([(String, Stake Ledger Residual, Natural)]
 -> [(String, Stake Ledger Residual, Natural,
      Stake Ledger Cumulative)])
-> [(String, Stake Ledger Residual, Natural)]
-> [(String, Stake Ledger Residual, Natural,
     Stake Ledger Cumulative)]
forall a b. (a -> b) -> a -> b
$
            [(String, Stake Ledger Residual)]
-> [(String, Stake Ledger Residual, Natural)]
forall {a} {b}. [(a, b)] -> [(a, b, Natural)]
addSeatIndex ([(String, Stake Ledger Residual)]
 -> [(String, Stake Ledger Residual, Natural)])
-> [(String, Stake Ledger Residual)]
-> [(String, Stake Ledger Residual, Natural)]
forall a b. (a -> b) -> a -> b
$
              (String -> String -> Ordering)
-> StakeDistr Ledger Residual -> [(String, Stake Ledger Residual)]
forall (sr :: StakeRole) (st :: StakeType).
IsStake (Stake sr st) =>
(String -> String -> Ordering)
-> StakeDistr sr st -> [(String, Stake sr st)]
stakeDistrToDecreasingStakes String -> String -> Ordering
tiebreaker StakeDistr Ledger Residual
residualStakeDistr

    let judgments :: [(String, Stake Ledger Residual, Natural, Stake Ledger Cumulative,
  Bool)]
judgments =
          ((String, Stake Ledger Residual, Natural, Stake Ledger Cumulative)
 -> (String, Stake Ledger Residual, Natural,
     Stake Ledger Cumulative, Bool))
-> [(String, Stake Ledger Residual, Natural,
     Stake Ledger Cumulative)]
-> [(String, 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
            ( \(String
voterIndex, Stake Ledger Residual
voterStake, Natural
seatIndex, Stake Ledger Cumulative
stakeAccum) ->
                ( String
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
                )
            )
            [(String, 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
. 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
$ String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
        ( [String] -> String
unlines
            [ String
"Persistent seats selected: "
                String -> String -> String
forall a. Semigroup a => a -> a -> a
<> StakeDistr Weight Persistent -> String
forall a. Show a => a -> String
show StakeDistr Weight Persistent
persistentSeats
            , String
"Next persistent seat index: "
                String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Natural -> String
forall a. Show a => a -> String
show Natural
numPersistentSeats
            , String
"Residual stakes with index, cumulative stake, and threshold judgments: "
                String -> String -> String
forall a. Semigroup a => a -> a -> a
<> [(String, Stake Ledger Residual, Natural, Stake Ledger Cumulative,
  Bool)]
-> String
forall a. Show a => a -> String
show [(String, Stake Ledger Residual, Natural, Stake Ledger Cumulative,
  Bool)]
judgments
            ]
        )
      (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ ((String, Stake Ledger Residual, Natural, Stake Ledger Cumulative,
  Bool)
 -> Bool)
-> [(String, Stake Ledger Residual, Natural,
     Stake Ledger Cumulative, Bool)]
-> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all
        (\(String
_, Stake Ledger Residual
_, Natural
_, Stake Ledger Cumulative
_, Bool
aboveThreshold) -> Bool -> Bool
not Bool
aboveThreshold)
        [(String, Stake Ledger Residual, Natural, Stake Ledger Cumulative,
  Bool)]
judgments

expectSuccess :: Either WFAError a -> a
expectSuccess :: forall a. Either String a -> a
expectSuccess Either String a
result =
  case Either String a
result of
    Left String
err -> String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"Model failed unexpectedly: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
err
    Right a
val -> a
val

-- | 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
$
    String -> [TestTree] -> TestTree
testGroup
      String
"Model property tests"
      [ String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
          String
"prop_stakeDistrDecreasingStakes"
          Property
prop_stakeDistrDecreasingStakes
      , String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
          String
"prop_weightedFaitAccompliPersistentSeats_persistentSeatsRespectNumSeats"
          Property
prop_weightedFaitAccompliPersistentSeats_persistentSeatsRespectNumSeats
      , String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
          String
"prop_weightedFaitAccompliPersistentSeats_persistentSeatsHaveLargeStake"
          Property
prop_weightedFaitAccompliPersistentSeats_persistentSeatsHaveLargeStake
      , String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
          String
"prop_weightedFaitAccompliPersistentSeats_totalStakePreserved"
          Property
prop_weightedFaitAccompliPersistentSeats_totalStakePreserved
      , String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
          String
"prop_weightedFaitAccompliPersistentSeats_nonPersistentSeatsCountCorrect"
          Property
prop_weightedFaitAccompliPersistentSeats_nonPersistentSeatsCountCorrect
      , String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
          String
"prop_weightedFaitAccompliPersistentSeats_residualSeatsDoNotQualify"
          Property
prop_weightedFaitAccompliPersistentSeats_residualSeatsDoNotQualify
      ]