{-# 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 =
  [Char] -> [TestTree] -> TestTree
testGroup
    [Char]
"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 =
  [Char]
-> (Map [Char] (Ratio Integer) -> Map [Char] (Stake Ledger Global))
-> (Map [Char] (Stake Ledger Global) -> Word64 -> (Word64, Word64))
-> TestTree
forall stakeDistr.
[Char]
-> (Map [Char] (Ratio Integer) -> stakeDistr)
-> (stakeDistr -> Word64 -> (Word64, Word64))
-> TestTree
conformsToRustImplementation
    [Char]
"Model conforms to Rust implementation"
    Map [Char] (Ratio Integer) -> Map [Char] (Stake Ledger Global)
forall {k}. Map k (Ratio Integer) -> Map k (Stake Ledger Global)
mkStakeDistr
    Map [Char] (Stake Ledger Global) -> Word64 -> (Word64, Word64)
forall {p} {a} {b}.
(Integral p, Num a, Num b) =>
Map [Char] (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 :: [Char] -> [Char] -> Ordering
tiebreaker =
    [Char] -> [Char] -> Ordering
forall a. Ord a => a -> a -> Ordering
compare

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

  model :: Map [Char] (Stake Ledger Global) -> p -> (a, b)
model Map [Char] (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 ([Char] -> [Char] -> Ordering)
-> NumSeats Global
-> Map [Char] (Stake Ledger Global)
-> Either
     [Char]
     (StakeDistr Weight Persistent, NumSeats Residual,
      StakeDistr Ledger Residual)
Model.weightedFaitAccompliPersistentSeats [Char] -> [Char] -> Ordering
tiebreaker Natural
NumSeats Global
totalSeats Map [Char] (Stake Ledger Global)
stakeDistr of
      Left [Char]
err ->
        [Char] -> (a, b)
forall a. HasCallStack => [Char] -> a
error ([Char] -> (a, b)) -> [Char] -> (a, b)
forall a b. (a -> b) -> a -> b
$ [Char]
"Model implementation failed with error: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char] -> [Char]
forall a. Show a => a -> [Char]
show [Char]
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 =
  [Char]
-> (Map [Char] (Ratio Integer) -> ExtWFAStakeDistr ())
-> (ExtWFAStakeDistr () -> Word64 -> (Word64, Word64))
-> TestTree
forall stakeDistr.
[Char]
-> (Map [Char] (Ratio Integer) -> stakeDistr)
-> (stakeDistr -> Word64 -> (Word64, Word64))
-> TestTree
conformsToRustImplementation
    [Char]
"Real implementation conforms to Rust implementation"
    Map [Char] (Ratio Integer) -> 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 [Char] (Ratio Integer) -> ExtWFAStakeDistr ()
mkStakeDistr =
    (WFAError -> ExtWFAStakeDistr ())
-> Either WFAError (ExtWFAStakeDistr ()) -> ExtWFAStakeDistr ()
forall {t} {t}. (t -> t) -> Either t t -> t
expectRight
      ( \WFAError
err ->
          [Char] -> ExtWFAStakeDistr ()
forall a. HasCallStack => [Char] -> a
error ([Char]
"could not build a stake distribution: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> WFAError -> [Char]
forall a. Show a => a -> [Char]
show WFAError
err)
      )
      (Either WFAError (ExtWFAStakeDistr ()) -> ExtWFAStakeDistr ())
-> (Map [Char] (Ratio Integer)
    -> Either WFAError (ExtWFAStakeDistr ()))
-> Map [Char] (Ratio Integer)
-> 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 [Char] (Ratio Integer) -> Map PoolId (LedgerStake, ()))
-> Map [Char] (Ratio Integer)
-> Either WFAError (ExtWFAStakeDistr ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> PoolId)
-> Map [Char] (LedgerStake, ()) -> Map PoolId (LedgerStake, ())
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys
        ( \[Char]
str ->
            KeyHash StakePool -> PoolId
WFA.PoolId
              (KeyHash StakePool -> PoolId)
-> ([Char] -> KeyHash StakePool) -> [Char] -> 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)
-> ([Char] -> VKey StakePool) -> [Char] -> 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)
-> ([Char] -> VerKeyDSIGN DSIGN) -> [Char] -> 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)
-> ([Char] -> SignKeyDSIGN DSIGN) -> [Char] -> 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)
-> ([Char] -> Seed) -> [Char] -> SignKeyDSIGN DSIGN
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Seed
SL.mkSeedFromBytes
              (ByteString -> Seed) -> ([Char] -> ByteString) -> [Char] -> Seed
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> ByteString
forall a. IsString a => [Char] -> a
fromString
              ([Char] -> PoolId) -> [Char] -> PoolId
forall a b. (a -> b) -> a -> b
$ [Char]
str
        )
      (Map [Char] (LedgerStake, ()) -> Map PoolId (LedgerStake, ()))
-> (Map [Char] (Ratio Integer) -> Map [Char] (LedgerStake, ()))
-> Map [Char] (Ratio Integer)
-> Map PoolId (LedgerStake, ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ratio Integer -> (LedgerStake, ()))
-> Map [Char] (Ratio Integer) -> Map [Char] (LedgerStake, ())
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map
        ( \Ratio Integer
stake ->
            (Ratio Integer -> LedgerStake
WFA.LedgerStake Ratio Integer
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 ->
              [Char]
-> (PersistentCommitteeSize, NonPersistentCommitteeSize,
    TotalPersistentStake, TotalNonPersistentStake)
forall a. HasCallStack => [Char] -> a
error ([Char]
"weightedFaitAccompliSplitSeats failed: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> WFAError -> [Char]
forall a. Show a => a -> [Char]
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
$
    [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty
      [Char]
"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 [Char] (Stake Ledger Global) -> NumSeats Global -> Property)
-> Property
Model.forAllPossiblyInvalidStakeDistrAndNumSeats ((Map [Char] (Stake Ledger Global) -> NumSeats Global -> Property)
 -> Property)
-> (Map [Char] (Stake Ledger Global)
    -> NumSeats Global -> Property)
-> Property
forall a b. (a -> b) -> a -> b
$ \Map [Char] (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
  [Char]
  (StakeDistr Weight Persistent, NumSeats Residual,
   StakeDistr Ledger Residual)
modelOutput =
          ([Char] -> [Char] -> Ordering)
-> NumSeats Global
-> Map [Char] (Stake Ledger Global)
-> Either
     [Char]
     (StakeDistr Weight Persistent, NumSeats Residual,
      StakeDistr Ledger Residual)
Model.weightedFaitAccompliPersistentSeats
            (PoolId -> PoolId -> Ordering
realTiebreaker (PoolId -> PoolId -> Ordering)
-> ([Char] -> PoolId) -> [Char] -> [Char] -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` [Char] -> PoolId
mkPoolId)
            NumSeats Global
numSeats
            Map [Char] (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 = (Ratio Integer -> LedgerStake
WFA.LedgerStake (stake -> Ratio Integer
forall stake. IsStake stake => stake -> Ratio Integer
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 [Char] (Stake Ledger Global)
    -> Map PoolId (LedgerStake, ()))
-> Map [Char] (Stake Ledger Global)
-> Either WFAError (ExtWFAStakeDistr ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> PoolId)
-> Map [Char] (LedgerStake, ()) -> Map PoolId (LedgerStake, ())
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys (\[Char]
str -> [Char] -> PoolId
mkPoolId [Char]
str)
              (Map [Char] (LedgerStake, ()) -> Map PoolId (LedgerStake, ()))
-> (Map [Char] (Stake Ledger Global)
    -> Map [Char] (LedgerStake, ()))
-> Map [Char] (Stake Ledger Global)
-> Map PoolId (LedgerStake, ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Stake Ledger Global -> (LedgerStake, ()))
-> Map [Char] (Stake Ledger Global) -> Map [Char] (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 [Char] (Stake Ledger Global)
 -> Either WFAError (ExtWFAStakeDistr ()))
-> Map [Char] (Stake Ledger Global)
-> Either WFAError (ExtWFAStakeDistr ())
forall a b. (a -> b) -> a -> b
$ Map [Char] (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 [Char] (Stake Ledger Global)
-> NumSeats Global -> Property -> Property
tabulateMoreSeatsThanNodes Map [Char] (Stake Ledger Global)
stakeDistr NumSeats Global
numSeats
      (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ case (Either
  [Char]
  (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 [Char]
_, Left WFAError
_) ->
          Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
        -- Model failed but real implementation succeeded
        (Left [Char]
modelErr, Right (ExtWFAStakeDistr (),
 (PersistentCommitteeSize, NonPersistentCommitteeSize,
  TotalPersistentStake, TotalNonPersistentStake))
_) ->
          [Char] -> Property -> Property
forall prop. Testable prop => [Char] -> prop -> Property
counterexample
            ( [Char]
"Model implementation failed with error: "
                [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char] -> [Char]
forall a. Show a => a -> [Char]
show [Char]
modelErr
                [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" but real implementation succeeded with output: "
                [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Either
  WFAError
  (ExtWFAStakeDistr (),
   (PersistentCommitteeSize, NonPersistentCommitteeSize,
    TotalPersistentStake, TotalNonPersistentStake))
-> [Char]
forall a. Show a => a -> [Char]
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) ->
          [Char] -> Property -> Property
forall prop. Testable prop => [Char] -> prop -> Property
counterexample
            ( [Char]
"Real implementation failed with error: "
                [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> WFAError -> [Char]
forall a. Show a => a -> [Char]
show WFAError
realErr
                [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" but model implementation succeeded with output: "
                [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Either
  [Char]
  (StakeDistr Weight Persistent, Natural, StakeDistr Ledger Residual)
-> [Char]
forall a. Show a => a -> [Char]
show Either
  [Char]
  (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 Ratio Integer
realPersistentStake))
                    , WFA.TotalNonPersistentStake
                        (WFA.Cumulative (WFA.LedgerStake Ratio Integer
realNonPersistentStake))
                    )
                )
          ) -> do
            let modelPersistentPools :: Set PoolId
modelPersistentPools =
                  ([Char] -> PoolId) -> Set [Char] -> Set PoolId
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map [Char] -> PoolId
mkPoolId (StakeDistr Weight Persistent -> Set [Char]
forall k a. Map k a -> Set k
Map.keysSet StakeDistr Weight Persistent
modelPersistentStakeDistr)
            let modelNonPersistentPools :: Set PoolId
modelNonPersistentPools =
                  ([Char] -> PoolId) -> Set [Char] -> Set PoolId
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map [Char] -> PoolId
mkPoolId (StakeDistr Ledger Residual -> Set [Char]
forall k a. Map k a -> Set k
Map.keysSet StakeDistr Ledger Residual
modelNonPersistentStakeDistr)
            let Model.StakeLedgerResidual Ratio Integer
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 Ratio Integer
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
            [Char] -> Property -> Property
forall prop. Testable prop => [Char] -> prop -> Property
counterexample
              ( [[Char]] -> [Char]
unlines
                  [ [Char]
"Model persistent pools: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Set PoolId -> [Char]
forall a. Show a => a -> [Char]
show Set PoolId
modelPersistentPools
                  , [Char]
"Model non-persistent pools: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Set PoolId -> [Char]
forall a. Show a => a -> [Char]
show Set PoolId
modelNonPersistentPools
                  , [Char]
"Model persistent stake: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Ratio Integer -> [Char]
forall a. Show a => a -> [Char]
show Ratio Integer
modelPersistentStake
                  , [Char]
"Model non-persistent stake: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Ratio Integer -> [Char]
forall a. Show a => a -> [Char]
show Ratio Integer
modelNonPersistentStake
                  , [Char]
"Real persistent pools: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Set PoolId -> [Char]
forall a. Show a => a -> [Char]
show Set PoolId
realPersistentPools
                  , [Char]
"Real non-persistent pools: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Set PoolId -> [Char]
forall a. Show a => a -> [Char]
show Set PoolId
realNonPersistentPools
                  , [Char]
"Real persistent stake: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Ratio Integer -> [Char]
forall a. Show a => a -> [Char]
show Ratio Integer
realPersistentStake
                  , [Char]
"Real non-persistent stake: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Ratio Integer -> [Char]
forall a. Show a => a -> [Char]
show Ratio Integer
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
.&&. (Ratio Integer
modelNonPersistentStake Ratio Integer -> Ratio Integer -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Ratio Integer
realNonPersistentStake)
                Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. (Ratio Integer
modelPersistentStake Ratio Integer -> Ratio Integer -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Ratio Integer
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 [Char] (Stake Ledger Global)
-> NumSeats Global -> Property -> Property
tabulateMoreSeatsThanNodes Map [Char] (Stake Ledger Global)
stakeDistr NumSeats Global
numSeats =
  [Char] -> [[Char]] -> Property -> Property
forall prop.
Testable prop =>
[Char] -> [[Char]] -> prop -> Property
tabulate
    [Char]
"More target seats than nodes"
    [ Bool -> [Char]
forall a. Show a => a -> [Char]
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 [Char] (Stake Ledger Global) -> Int
forall k a. Map k a -> Int
Map.size Map [Char] (Stake Ledger Global)
stakeDistr))
    ]

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