{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}

module Test.Consensus.Committee.WFALS (tests) where

import qualified Cardano.Crypto.DSIGN.Class as SL
import qualified Cardano.Crypto.Seed as SL
import qualified Cardano.Ledger.Keys as SL
import qualified Data.Array as Array
import Data.Bifunctor (Bifunctor (..))
import Data.Either (partitionEithers)
import Data.Function (on)
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import Data.String (IsString (..))
import qualified Ouroboros.Consensus.Committee.Types as WFA
import Ouroboros.Consensus.Committee.WFA (WFATiebreaker (..))
import qualified Ouroboros.Consensus.Committee.WFA as WFA
import Test.Consensus.Committee.Utils (mkPoolId)
import Test.Consensus.Committee.WFALS.Conformance (conformsToRustImplementation)
import Test.Consensus.Committee.WFALS.Model
  ( NumSeats
  , StakeDistr
  , StakeRole (..)
  , StakeType (..)
  )
import qualified Test.Consensus.Committee.WFALS.Model as Model
import qualified Test.Consensus.Committee.WFALS.Model.Tests as Model
import qualified Test.Consensus.Committee.WFALS.Model.Utils as Model
import qualified Test.Consensus.Committee.WFALS.Tests as Impl
import Test.QuickCheck
  ( Property
  , Testable (..)
  , counterexample
  , tabulate
  , (.&&.)
  , (===)
  )
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.QuickCheck (testProperty)
import Test.Util.TestEnv (adjustQuickCheckTests)

tests :: TestTree
tests :: TestTree
tests =
  String -> [TestTree] -> TestTree
testGroup
    String
"WFALS"
    [ TestTree
Model.tests
    , TestTree
Impl.tests
    , TestTree
modelConformsToRustImplementation
    , TestTree
realImplementationConformsToRustImplementation
    , TestTree
modelConformsToRealImplementation
    ]

-- | Check that the model implementation matches the Rust one
modelConformsToRustImplementation :: TestTree
modelConformsToRustImplementation :: TestTree
modelConformsToRustImplementation =
  String
-> (Map String Rational -> Map String (Stake Ledger Global))
-> (Map String (Stake Ledger Global) -> Word64 -> (Word64, Word64))
-> TestTree
forall stakeDistr.
String
-> (Map String Rational -> stakeDistr)
-> (stakeDistr -> Word64 -> (Word64, Word64))
-> TestTree
conformsToRustImplementation
    String
"Model conforms to Rust implementation"
    Map String Rational -> Map String (Stake Ledger Global)
forall {k}. Map k Rational -> Map k (Stake Ledger Global)
mkStakeDistr
    Map String (Stake Ledger Global) -> Word64 -> (Word64, Word64)
forall {p} {a} {b}.
(Integral p, Num a, Num b) =>
Map String (Stake Ledger Global) -> p -> (a, b)
model
 where
  -- NOTE: this is not a good tiebreaker for real-world use, but it is
  -- sufficient here because the actual order of pools with the same stake does
  -- not matter when computing the persistent vs. non-persistent seat /counts/.
  tiebreaker :: String -> String -> Ordering
tiebreaker =
    String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
compare

  mkStakeDistr :: Map k Rational -> Map k (Stake Ledger Global)
mkStakeDistr =
    (Rational -> Stake Ledger Global)
-> Map k Rational -> Map k (Stake Ledger Global)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map Rational -> Stake Ledger Global
forall stake. IsStake stake => Rational -> stake
Model.rationalToStake

  model :: Map String (Stake Ledger Global) -> p -> (a, b)
model Map String (Stake Ledger Global)
stakeDistr p
targetCommitteeSize = do
    let totalSeats :: Natural
totalSeats = p -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral p
targetCommitteeSize
    case (String -> String -> Ordering)
-> NumSeats Global
-> Map String (Stake Ledger Global)
-> Either
     String
     (StakeDistr Weight Persistent, NumSeats Residual,
      StakeDistr Ledger Residual)
Model.weightedFaitAccompliPersistentSeats String -> String -> Ordering
tiebreaker Natural
NumSeats Global
totalSeats Map String (Stake Ledger Global)
stakeDistr of
      Left String
err ->
        String -> (a, b)
forall a. HasCallStack => String -> a
error (String -> (a, b)) -> String -> (a, b)
forall a b. (a -> b) -> a -> b
$ String
"Model implementation failed with error: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String -> String
forall a. Show a => a -> String
show String
err
      Right (StakeDistr Weight Persistent
persistentSeats, NumSeats Residual
numNonPersistentSeats, StakeDistr Ledger Residual
_) ->
        ( Int -> a
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)
        , Natural -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
NumSeats Residual
numNonPersistentSeats
        )

-- | Check that the real implementation matches the Rust one
realImplementationConformsToRustImplementation :: TestTree
realImplementationConformsToRustImplementation :: TestTree
realImplementationConformsToRustImplementation =
  String
-> (Map String Rational -> ExtWFAStakeDistr ())
-> (ExtWFAStakeDistr () -> Word64 -> (Word64, Word64))
-> TestTree
forall stakeDistr.
String
-> (Map String Rational -> stakeDistr)
-> (stakeDistr -> Word64 -> (Word64, Word64))
-> TestTree
conformsToRustImplementation
    String
"Real implementation conforms to Rust implementation"
    Map String Rational -> ExtWFAStakeDistr ()
mkStakeDistr
    ExtWFAStakeDistr () -> Word64 -> (Word64, Word64)
forall {p} {a} {b} {c}.
(Integral p, Num a, Num b) =>
ExtWFAStakeDistr c -> p -> (a, b)
impl
 where
  -- NOTE: this is not a good tiebreaker for real-world use, but it is
  -- sufficient here because the actual order of pools with the same stake does
  -- not matter when computing the persistent vs. non-persistent seat /counts/.
  tiebreaker :: WFATiebreaker
tiebreaker =
    (PoolId -> PoolId -> Ordering) -> WFATiebreaker
WFATiebreaker PoolId -> PoolId -> Ordering
forall a. Ord a => a -> a -> Ordering
compare

  mkStakeDistr :: Map String Rational -> ExtWFAStakeDistr ()
mkStakeDistr =
    (WFAError -> ExtWFAStakeDistr ())
-> Either WFAError (ExtWFAStakeDistr ()) -> ExtWFAStakeDistr ()
forall {t} {t}. (t -> t) -> Either t t -> t
expectRight
      ( \WFAError
err ->
          String -> ExtWFAStakeDistr ()
forall a. HasCallStack => String -> a
error (String
"could not build a stake distribution: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> WFAError -> String
forall a. Show a => a -> String
show WFAError
err)
      )
      (Either WFAError (ExtWFAStakeDistr ()) -> ExtWFAStakeDistr ())
-> (Map String Rational -> Either WFAError (ExtWFAStakeDistr ()))
-> Map String Rational
-> ExtWFAStakeDistr ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WFATiebreaker
-> Map PoolId (LedgerStake, ())
-> Either WFAError (ExtWFAStakeDistr ())
forall a.
WFATiebreaker
-> Map PoolId (LedgerStake, a)
-> Either WFAError (ExtWFAStakeDistr a)
WFA.mkExtWFAStakeDistr WFATiebreaker
tiebreaker
      (Map PoolId (LedgerStake, ())
 -> Either WFAError (ExtWFAStakeDistr ()))
-> (Map String Rational -> Map PoolId (LedgerStake, ()))
-> Map String Rational
-> Either WFAError (ExtWFAStakeDistr ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> PoolId)
-> Map String (LedgerStake, ()) -> Map PoolId (LedgerStake, ())
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys
        ( \String
str ->
            KeyHash StakePool -> PoolId
WFA.PoolId
              (KeyHash StakePool -> PoolId)
-> (String -> KeyHash StakePool) -> String -> PoolId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VKey StakePool -> KeyHash StakePool
forall (kd :: KeyRole). VKey kd -> KeyHash kd
SL.hashKey
              (VKey StakePool -> KeyHash StakePool)
-> (String -> VKey StakePool) -> String -> KeyHash StakePool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerKeyDSIGN DSIGN -> VKey StakePool
forall (kd :: KeyRole). VerKeyDSIGN DSIGN -> VKey kd
SL.VKey
              (VerKeyDSIGN DSIGN -> VKey StakePool)
-> (String -> VerKeyDSIGN DSIGN) -> String -> VKey StakePool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SignKeyDSIGN DSIGN -> VerKeyDSIGN DSIGN
forall v. DSIGNAlgorithm v => SignKeyDSIGN v -> VerKeyDSIGN v
SL.deriveVerKeyDSIGN
              (SignKeyDSIGN DSIGN -> VerKeyDSIGN DSIGN)
-> (String -> SignKeyDSIGN DSIGN) -> String -> VerKeyDSIGN DSIGN
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Seed -> SignKeyDSIGN DSIGN
forall v. DSIGNAlgorithm v => Seed -> SignKeyDSIGN v
SL.genKeyDSIGN
              (Seed -> SignKeyDSIGN DSIGN)
-> (String -> Seed) -> String -> SignKeyDSIGN DSIGN
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Seed
SL.mkSeedFromBytes
              (ByteString -> Seed) -> (String -> ByteString) -> String -> Seed
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ByteString
forall a. IsString a => String -> a
fromString
              (String -> PoolId) -> String -> PoolId
forall a b. (a -> b) -> a -> b
$ String
str
        )
      (Map String (LedgerStake, ()) -> Map PoolId (LedgerStake, ()))
-> (Map String Rational -> Map String (LedgerStake, ()))
-> Map String Rational
-> Map PoolId (LedgerStake, ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rational -> (LedgerStake, ()))
-> Map String Rational -> Map String (LedgerStake, ())
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map
        ( \Rational
stake ->
            (Rational -> LedgerStake
WFA.LedgerStake Rational
stake, ())
        )

  impl :: ExtWFAStakeDistr c -> p -> (a, b)
impl ExtWFAStakeDistr c
stakeDistr p
targetCommitteeSize =
    let
      totalSeats :: TargetCommitteeSize
totalSeats =
        Word64 -> TargetCommitteeSize
WFA.TargetCommitteeSize (p -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral p
targetCommitteeSize)
      (PersistentCommitteeSize
persistentSeats, NonPersistentCommitteeSize
nonPersistentSeats, TotalPersistentStake
_, TotalNonPersistentStake
_) =
        (WFAError
 -> (PersistentCommitteeSize, NonPersistentCommitteeSize,
     TotalPersistentStake, TotalNonPersistentStake))
-> Either
     WFAError
     (PersistentCommitteeSize, NonPersistentCommitteeSize,
      TotalPersistentStake, TotalNonPersistentStake)
-> (PersistentCommitteeSize, NonPersistentCommitteeSize,
    TotalPersistentStake, TotalNonPersistentStake)
forall {t} {t}. (t -> t) -> Either t t -> t
expectRight
          ( \WFAError
err ->
              String
-> (PersistentCommitteeSize, NonPersistentCommitteeSize,
    TotalPersistentStake, TotalNonPersistentStake)
forall a. HasCallStack => String -> a
error (String
"weightedFaitAccompliSplitSeats failed: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> WFAError -> String
forall a. Show a => a -> String
show WFAError
err)
          )
          (Either
   WFAError
   (PersistentCommitteeSize, NonPersistentCommitteeSize,
    TotalPersistentStake, TotalNonPersistentStake)
 -> (PersistentCommitteeSize, NonPersistentCommitteeSize,
     TotalPersistentStake, TotalNonPersistentStake))
-> Either
     WFAError
     (PersistentCommitteeSize, NonPersistentCommitteeSize,
      TotalPersistentStake, TotalNonPersistentStake)
-> (PersistentCommitteeSize, NonPersistentCommitteeSize,
    TotalPersistentStake, TotalNonPersistentStake)
forall a b. (a -> b) -> a -> b
$ ExtWFAStakeDistr c
-> TargetCommitteeSize
-> Either
     WFAError
     (PersistentCommitteeSize, NonPersistentCommitteeSize,
      TotalPersistentStake, TotalNonPersistentStake)
forall c.
ExtWFAStakeDistr c
-> TargetCommitteeSize
-> Either
     WFAError
     (PersistentCommitteeSize, NonPersistentCommitteeSize,
      TotalPersistentStake, TotalNonPersistentStake)
WFA.weightedFaitAccompliSplitSeats ExtWFAStakeDistr c
stakeDistr TargetCommitteeSize
totalSeats
     in
      ( Word64 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (PersistentCommitteeSize -> Word64
WFA.unPersistentCommitteeSize PersistentCommitteeSize
persistentSeats)
      , Word64 -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral (NonPersistentCommitteeSize -> Word64
WFA.unNonPersistentCommitteeSize NonPersistentCommitteeSize
nonPersistentSeats)
      )

  expectRight :: (t -> t) -> Either t t -> t
expectRight t -> t
onLeft = \case
    Left t
err -> t -> t
onLeft t
err
    Right t
a -> t
a

-- | Check that the model implementation conforms to the real implementation
-- using QuickCheck generators
modelConformsToRealImplementation :: TestTree
modelConformsToRealImplementation :: TestTree
modelConformsToRealImplementation =
  (Int -> Int) -> TestTree -> TestTree
adjustQuickCheckTests (Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
10) (TestTree -> TestTree) -> TestTree -> TestTree
forall a b. (a -> b) -> a -> b
$
    String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
      String
"Model conforms to real implementation"
      Property
prop_modelConformsToRealImplementation

-- | Property: the model and real implementations should produce the same
-- number of persistent and non-persistent seats
prop_modelConformsToRealImplementation :: Property
prop_modelConformsToRealImplementation :: Property
prop_modelConformsToRealImplementation =
  (Map String (Stake Ledger Global) -> NumSeats Global -> Property)
-> Property
Model.forAllPossiblyInvalidStakeDistrAndNumSeats ((Map String (Stake Ledger Global) -> NumSeats Global -> Property)
 -> Property)
-> (Map String (Stake Ledger Global)
    -> NumSeats Global -> Property)
-> Property
forall a b. (a -> b) -> a -> b
$ \Map String (Stake Ledger Global)
stakeDistr NumSeats Global
numSeats -> do
    -- NOTE: we use a trivial tiebreaker here because we are not interested in
    -- fairness here. However, the model's tiebreaker needs to be adapted below
    -- to produce the same ordering based on the 'PoolId' we derive from the
    -- string keys in the random stake distribution, so that both
    -- implementations select the same pools as persistent vs. non-persistent.
    let realTiebreaker :: WFA.PoolId -> WFA.PoolId -> Ordering
        realTiebreaker :: PoolId -> PoolId -> Ordering
realTiebreaker = PoolId -> PoolId -> Ordering
forall a. Ord a => a -> a -> Ordering
compare
    -- Run the model
    let modelOutput :: Either
  String
  (StakeDistr Weight Persistent, NumSeats Residual,
   StakeDistr Ledger Residual)
modelOutput =
          (String -> String -> Ordering)
-> NumSeats Global
-> Map String (Stake Ledger Global)
-> Either
     String
     (StakeDistr Weight Persistent, NumSeats Residual,
      StakeDistr Ledger Residual)
Model.weightedFaitAccompliPersistentSeats
            (PoolId -> PoolId -> Ordering
realTiebreaker (PoolId -> PoolId -> Ordering)
-> (String -> PoolId) -> String -> String -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` String -> PoolId
mkPoolId)
            NumSeats Global
numSeats
            Map String (Stake Ledger Global)
stakeDistr
    -- Run the real implementation
    let realOutput :: Either
  WFAError
  (ExtWFAStakeDistr (),
   (PersistentCommitteeSize, NonPersistentCommitteeSize,
    TotalPersistentStake, TotalNonPersistentStake))
realOutput = do
          let mkEntry :: stake -> (LedgerStake, ())
mkEntry stake
stake = (Rational -> LedgerStake
WFA.LedgerStake (stake -> Rational
forall stake. IsStake stake => stake -> Rational
Model.stakeToRational stake
stake), ())
          extWFAStakeDistr <-
            WFATiebreaker
-> Map PoolId (LedgerStake, ())
-> Either WFAError (ExtWFAStakeDistr ())
forall a.
WFATiebreaker
-> Map PoolId (LedgerStake, a)
-> Either WFAError (ExtWFAStakeDistr a)
WFA.mkExtWFAStakeDistr ((PoolId -> PoolId -> Ordering) -> WFATiebreaker
WFATiebreaker PoolId -> PoolId -> Ordering
realTiebreaker)
              (Map PoolId (LedgerStake, ())
 -> Either WFAError (ExtWFAStakeDistr ()))
-> (Map String (Stake Ledger Global)
    -> Map PoolId (LedgerStake, ()))
-> Map String (Stake Ledger Global)
-> Either WFAError (ExtWFAStakeDistr ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> PoolId)
-> Map String (LedgerStake, ()) -> Map PoolId (LedgerStake, ())
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys (\String
str -> String -> PoolId
mkPoolId String
str)
              (Map String (LedgerStake, ()) -> Map PoolId (LedgerStake, ()))
-> (Map String (Stake Ledger Global)
    -> Map String (LedgerStake, ()))
-> Map String (Stake Ledger Global)
-> Map PoolId (LedgerStake, ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Stake Ledger Global -> (LedgerStake, ()))
-> Map String (Stake Ledger Global) -> Map String (LedgerStake, ())
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\Stake Ledger Global
stake -> Stake Ledger Global -> (LedgerStake, ())
forall {stake}. IsStake stake => stake -> (LedgerStake, ())
mkEntry Stake Ledger Global
stake)
              (Map String (Stake Ledger Global)
 -> Either WFAError (ExtWFAStakeDistr ()))
-> Map String (Stake Ledger Global)
-> Either WFAError (ExtWFAStakeDistr ())
forall a b. (a -> b) -> a -> b
$ Map String (Stake Ledger Global)
stakeDistr
          wfaOutput <-
            WFA.weightedFaitAccompliSplitSeats
              extWFAStakeDistr
              (WFA.TargetCommitteeSize (fromIntegral numSeats))
          return (extWFAStakeDistr, wfaOutput)
    -- Compare their results
    Either
  WFAError
  (ExtWFAStakeDistr (),
   (PersistentCommitteeSize, NonPersistentCommitteeSize,
    TotalPersistentStake, TotalNonPersistentStake))
-> Property -> Property
forall err a. Either err a -> Property -> Property
tabulateOutcome Either
  WFAError
  (ExtWFAStakeDistr (),
   (PersistentCommitteeSize, NonPersistentCommitteeSize,
    TotalPersistentStake, TotalNonPersistentStake))
realOutput
      (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map String (Stake Ledger Global)
-> NumSeats Global -> Property -> Property
tabulateMoreSeatsThanNodes Map String (Stake Ledger Global)
stakeDistr NumSeats Global
numSeats
      (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ case (Either
  String
  (StakeDistr Weight Persistent, Natural, StakeDistr Ledger Residual)
modelOutput, Either
  WFAError
  (ExtWFAStakeDistr (),
   (PersistentCommitteeSize, NonPersistentCommitteeSize,
    TotalPersistentStake, TotalNonPersistentStake))
realOutput) of
        -- Both implementations failed (we don't care about the specific error)
        (Left String
_, Left WFAError
_) ->
          Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
        -- Model failed but real implementation succeeded
        (Left String
modelErr, Right (ExtWFAStakeDistr (),
 (PersistentCommitteeSize, NonPersistentCommitteeSize,
  TotalPersistentStake, TotalNonPersistentStake))
_) ->
          String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
            ( String
"Model implementation failed with error: "
                String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String -> String
forall a. Show a => a -> String
show String
modelErr
                String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" but real implementation succeeded with output: "
                String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Either
  WFAError
  (ExtWFAStakeDistr (),
   (PersistentCommitteeSize, NonPersistentCommitteeSize,
    TotalPersistentStake, TotalNonPersistentStake))
-> String
forall a. Show a => a -> String
show Either
  WFAError
  (ExtWFAStakeDistr (),
   (PersistentCommitteeSize, NonPersistentCommitteeSize,
    TotalPersistentStake, TotalNonPersistentStake))
realOutput
            )
            (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
False
        -- Model succeeded but real implementation failed
        (Right (StakeDistr Weight Persistent, Natural, StakeDistr Ledger Residual)
_, Left WFAError
realErr) ->
          String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
            ( String
"Real implementation failed with error: "
                String -> String -> String
forall a. Semigroup a => a -> a -> a
<> WFAError -> String
forall a. Show a => a -> String
show WFAError
realErr
                String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" but model implementation succeeded with output: "
                String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Either
  String
  (StakeDistr Weight Persistent, Natural, StakeDistr Ledger Residual)
-> String
forall a. Show a => a -> String
show Either
  String
  (StakeDistr Weight Persistent, Natural, StakeDistr Ledger Residual)
modelOutput
            )
            (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
False
        -- Both implementations succeeded, compare their outputs
        ( Right
            ( StakeDistr Weight Persistent
modelPersistentStakeDistr
              , Natural
modelNonPersistentSeats
              , StakeDistr Ledger Residual
modelNonPersistentStakeDistr
              )
          , Right
              ( ExtWFAStakeDistr ()
extWFAStakeDistr
                , ( WFA.PersistentCommitteeSize Word64
realPersistentSeats
                    , WFA.NonPersistentCommitteeSize Word64
realNonPersistentSeats
                    , WFA.TotalPersistentStake
                        (WFA.Cumulative (WFA.LedgerStake Rational
realPersistentStake))
                    , WFA.TotalNonPersistentStake
                        (WFA.Cumulative (WFA.LedgerStake Rational
realNonPersistentStake))
                    )
                )
          ) -> do
            let modelPersistentPools :: Set PoolId
modelPersistentPools =
                  (String -> PoolId) -> Set String -> Set PoolId
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map String -> PoolId
mkPoolId (StakeDistr Weight Persistent -> Set String
forall k a. Map k a -> Set k
Map.keysSet StakeDistr Weight Persistent
modelPersistentStakeDistr)
            let modelNonPersistentPools :: Set PoolId
modelNonPersistentPools =
                  (String -> PoolId) -> Set String -> Set PoolId
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map String -> PoolId
mkPoolId (StakeDistr Ledger Residual -> Set String
forall k a. Map k a -> Set k
Map.keysSet StakeDistr Ledger Residual
modelNonPersistentStakeDistr)
            let Model.StakeLedgerResidual Rational
modelNonPersistentStake =
                  [Stake Ledger Residual] -> Stake Ledger Residual
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (StakeDistr Ledger Residual -> [Stake Ledger Residual]
forall k a. Map k a -> [a]
Map.elems StakeDistr Ledger Residual
modelNonPersistentStakeDistr)
            let Model.StakeWeightPersistent Rational
modelPersistentStake =
                  [Stake Weight Persistent] -> Stake Weight Persistent
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (StakeDistr Weight Persistent -> [Stake Weight Persistent]
forall k a. Map k a -> [a]
Map.elems StakeDistr Weight Persistent
modelPersistentStakeDistr)
            let splitPools :: (SeatIndex, (a, b, c, d)) -> Either a a
splitPools (WFA.SeatIndex Word64
i, (a
poolId, b
_, c
_, d
_))
                  | Word64
realPersistentSeats Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
== Word64
0 = a -> Either a a
forall a b. b -> Either a b
Right a
poolId
                  | Word64
i Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
>= Word64
realPersistentSeats = a -> Either a a
forall a b. b -> Either a b
Right a
poolId
                  | Bool
otherwise = a -> Either a a
forall a b. a -> Either a b
Left a
poolId
            let (Set PoolId
realPersistentPools, Set PoolId
realNonPersistentPools) =
                  ([PoolId] -> Set PoolId)
-> ([PoolId] -> Set PoolId)
-> ([PoolId], [PoolId])
-> (Set PoolId, Set PoolId)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap [PoolId] -> Set PoolId
forall a. Ord a => [a] -> Set a
Set.fromList [PoolId] -> Set PoolId
forall a. Ord a => [a] -> Set a
Set.fromList
                    (([PoolId], [PoolId]) -> (Set PoolId, Set PoolId))
-> (ExtWFAStakeDistr () -> ([PoolId], [PoolId]))
-> ExtWFAStakeDistr ()
-> (Set PoolId, Set PoolId)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Either PoolId PoolId] -> ([PoolId], [PoolId])
forall a b. [Either a b] -> ([a], [b])
partitionEithers
                    ([Either PoolId PoolId] -> ([PoolId], [PoolId]))
-> (ExtWFAStakeDistr () -> [Either PoolId PoolId])
-> ExtWFAStakeDistr ()
-> ([PoolId], [PoolId])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SeatIndex, (PoolId, (), LedgerStake, Cumulative LedgerStake))
 -> Either PoolId PoolId)
-> [(SeatIndex, (PoolId, (), LedgerStake, Cumulative LedgerStake))]
-> [Either PoolId PoolId]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SeatIndex, (PoolId, (), LedgerStake, Cumulative LedgerStake))
-> Either PoolId PoolId
forall {a} {b} {c} {d}. (SeatIndex, (a, b, c, d)) -> Either a a
splitPools
                    ([(SeatIndex, (PoolId, (), LedgerStake, Cumulative LedgerStake))]
 -> [Either PoolId PoolId])
-> (ExtWFAStakeDistr ()
    -> [(SeatIndex,
         (PoolId, (), LedgerStake, Cumulative LedgerStake))])
-> ExtWFAStakeDistr ()
-> [Either PoolId PoolId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Array SeatIndex (PoolId, (), LedgerStake, Cumulative LedgerStake)
-> [(SeatIndex, (PoolId, (), LedgerStake, Cumulative LedgerStake))]
forall i e. Ix i => Array i e -> [(i, e)]
Array.assocs
                    (Array SeatIndex (PoolId, (), LedgerStake, Cumulative LedgerStake)
 -> [(SeatIndex,
      (PoolId, (), LedgerStake, Cumulative LedgerStake))])
-> (ExtWFAStakeDistr ()
    -> Array
         SeatIndex (PoolId, (), LedgerStake, Cumulative LedgerStake))
-> ExtWFAStakeDistr ()
-> [(SeatIndex, (PoolId, (), LedgerStake, Cumulative LedgerStake))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtWFAStakeDistr ()
-> Array
     SeatIndex (PoolId, (), LedgerStake, Cumulative LedgerStake)
forall a.
ExtWFAStakeDistr a
-> Array SeatIndex (PoolId, a, LedgerStake, Cumulative LedgerStake)
WFA.unExtWFAStakeDistr
                    (ExtWFAStakeDistr () -> (Set PoolId, Set PoolId))
-> ExtWFAStakeDistr () -> (Set PoolId, Set PoolId)
forall a b. (a -> b) -> a -> b
$ ExtWFAStakeDistr ()
extWFAStakeDistr
            String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
              ( [String] -> String
unlines
                  [ String
"Model persistent pools: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Set PoolId -> String
forall a. Show a => a -> String
show Set PoolId
modelPersistentPools
                  , String
"Model non-persistent pools: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Set PoolId -> String
forall a. Show a => a -> String
show Set PoolId
modelNonPersistentPools
                  , String
"Model persistent stake: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Rational -> String
forall a. Show a => a -> String
show Rational
modelPersistentStake
                  , String
"Model non-persistent stake: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Rational -> String
forall a. Show a => a -> String
show Rational
modelNonPersistentStake
                  , String
"Real persistent pools: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Set PoolId -> String
forall a. Show a => a -> String
show Set PoolId
realPersistentPools
                  , String
"Real non-persistent pools: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Set PoolId -> String
forall a. Show a => a -> String
show Set PoolId
realNonPersistentPools
                  , String
"Real persistent stake: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Rational -> String
forall a. Show a => a -> String
show Rational
realPersistentStake
                  , String
"Real non-persistent stake: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Rational -> String
forall a. Show a => a -> String
show Rational
realNonPersistentStake
                  ]
              )
              (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ (Set PoolId
modelPersistentPools Set PoolId -> Set PoolId -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Set PoolId
realPersistentPools)
                Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. (Set PoolId
modelNonPersistentPools Set PoolId -> Set PoolId -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Set PoolId
realNonPersistentPools)
                Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. (Rational
modelNonPersistentStake Rational -> Rational -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Rational
realNonPersistentStake)
                Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. (Rational
modelPersistentStake Rational -> Rational -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Rational
realPersistentStake)
                Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. (Natural -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
modelNonPersistentSeats Word64 -> Word64 -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Word64
realNonPersistentSeats)

-- * Tabulation helpers

tabulateMoreSeatsThanNodes ::
  StakeDistr Ledger Global ->
  NumSeats Global ->
  Property ->
  Property
tabulateMoreSeatsThanNodes :: Map String (Stake Ledger Global)
-> NumSeats Global -> Property -> Property
tabulateMoreSeatsThanNodes Map String (Stake Ledger Global)
stakeDistr NumSeats Global
numSeats =
  String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate
    String
"More target seats than nodes"
    [ Bool -> String
forall a. Show a => a -> String
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 (Map String (Stake Ledger Global) -> Int
forall k a. Map k a -> Int
Map.size Map String (Stake Ledger Global)
stakeDistr))
    ]

tabulateOutcome ::
  Either err a ->
  Property ->
  Property
tabulateOutcome :: forall err a. Either err a -> Property -> Property
tabulateOutcome Either err a
result =
  String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate
    String
"Outcome"
    [ case Either err a
result of
        Left err
_ -> String
"Failure"
        Right a
_ -> String
"Success"
    ]