{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

-- | Test properties relating Peras and voting committee types.
module Test.Consensus.Peras.Voting.Committee
  ( tests
  ) where

import Data.Proxy (Proxy (..))
import qualified Ouroboros.Consensus.Committee.Class as Committee
import Ouroboros.Consensus.Committee.EveryoneVotes (EveryoneVotes)
import Ouroboros.Consensus.Committee.WFALS (WFALS)
import qualified Ouroboros.Consensus.Peras.Cert.V1 as V1
import qualified Ouroboros.Consensus.Peras.Vote.V1 as V1
import Ouroboros.Consensus.Peras.Voting.Committee
  ( PerasCertCompatibleWithVotingCommittee (..)
  , PerasVoteCompatibleWithVotingCommittee (..)
  )
import Test.Consensus.Peras.Util
  ( genPerasCert
  , genPerasVote
  , perasCertContainsOnlyPersistentVotes
  , perasVoteIsPersistent
  , tabulatePerasCert
  , tabulatePerasVote
  )
import Test.QuickCheck
  ( Gen
  , Property
  , Testable (..)
  , counterexample
  , forAll
  , frequency
  , tabulate
  , (===)
  )
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.QuickCheck (testProperty)
import Test.Util.TestEnv (adjustQuickCheckTests)

tests :: TestTree
tests :: TestTree
tests =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
"Roundtrip for Peras types via abstract committee types"
    [ (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
$
        TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"Roundtrip for PerasVote via WFALS" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
          Proxy PerasVote
-> Proxy WFALS
-> (PerasVote -> Bool)
-> Gen PerasVote
-> (PerasVote -> Property -> Property)
-> Property
forall vote crypto committee.
(Show vote, Eq vote,
 PerasVoteCompatibleWithVotingCommittee vote crypto committee) =>
Proxy vote
-> Proxy committee
-> (vote -> Bool)
-> Gen vote
-> (vote -> Property -> Property)
-> Property
prop_roundtrip_vote
            (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @V1.PerasVote)
            (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @WFALS)
            -- WFALS supports both persistent and non-persistent of votes
            (Bool -> PerasVote -> Bool
forall a b. a -> b -> a
const Bool
True)
            -- Generate both persistent and non-persistent votes
            (Bool -> Gen PerasVote
genPerasVote Bool
True)
            PerasVote -> Property -> Property
tabulatePerasVote
    , (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
$
        TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"Roundtrip for PerasVote via EveryoneVotes" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
          Proxy PerasVote
-> Proxy EveryoneVotes
-> (PerasVote -> Bool)
-> Gen PerasVote
-> (PerasVote -> Property -> Property)
-> Property
forall vote crypto committee.
(Show vote, Eq vote,
 PerasVoteCompatibleWithVotingCommittee vote crypto committee) =>
Proxy vote
-> Proxy committee
-> (vote -> Bool)
-> Gen vote
-> (vote -> Property -> Property)
-> Property
prop_roundtrip_vote
            (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @V1.PerasVote)
            (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @EveryoneVotes)
            -- EveryoneVotes only supports non-persistent votes
            PerasVote -> Bool
perasVoteIsPersistent
            -- Generate both persistent and non-persistent votes to trigger
            -- conversion errors in a reasonable amount of tests
            (Bool -> Gen PerasVote
genPerasVote (Bool -> Gen PerasVote) -> Gen Bool -> Gen PerasVote
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [(Int, Gen Bool)] -> Gen Bool
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency [(Int
2, Bool -> Gen Bool
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True), (Int
1, Bool -> Gen Bool
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False)])
            PerasVote -> Property -> Property
tabulatePerasVote
    , (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
$
        TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"Roundtrip for PerasCert via WFALS" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
          Proxy PerasCert
-> Proxy WFALS
-> (PerasCert -> Bool)
-> Gen PerasCert
-> (PerasCert -> Property -> Property)
-> Property
forall cert crypto committee.
(Show cert, Eq cert,
 PerasCertCompatibleWithVotingCommittee cert crypto committee) =>
Proxy cert
-> Proxy committee
-> (cert -> Bool)
-> Gen cert
-> (cert -> Property -> Property)
-> Property
prop_roundtrip_cert
            (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @V1.PerasCert)
            (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @WFALS)
            -- WFALS supports certs with both persistent and non-persistent votes
            (Bool -> PerasCert -> Bool
forall a b. a -> b -> a
const Bool
True)
            -- Generate certs with both persistent and non-persistent votes
            (Bool -> Gen PerasCert
genPerasCert Bool
True)
            PerasCert -> Property -> Property
tabulatePerasCert
    , (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
$
        TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"Roundtrip for PerasCert via EveryoneVotes" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
          Proxy PerasCert
-> Proxy EveryoneVotes
-> (PerasCert -> Bool)
-> Gen PerasCert
-> (PerasCert -> Property -> Property)
-> Property
forall cert crypto committee.
(Show cert, Eq cert,
 PerasCertCompatibleWithVotingCommittee cert crypto committee) =>
Proxy cert
-> Proxy committee
-> (cert -> Bool)
-> Gen cert
-> (cert -> Property -> Property)
-> Property
prop_roundtrip_cert
            (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @V1.PerasCert)
            (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @EveryoneVotes)
            -- EveryoneVotes only supports certs with persistent votes
            PerasCert -> Bool
perasCertContainsOnlyPersistentVotes
            -- Only sometimes generate certs with non-persistent votes to
            -- trigger conversion errors in a reasonable amount of tests
            (Bool -> Gen PerasCert
genPerasCert (Bool -> Gen PerasCert) -> Gen Bool -> Gen PerasCert
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [(Int, Gen Bool)] -> Gen Bool
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency [(Int
2, Bool -> Gen Bool
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False), (Int
1, Bool -> Gen Bool
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True)])
            PerasCert -> Property -> Property
tabulatePerasCert
    ]

-- * Properties

-- | Test that converting a concrete Peras vote to an committee vote and back
-- again results in the original Peras vote.
--
-- NOTE: this takes a predicate to determine whether triggering an exception is
-- a test failure or an expected outcome for the given voting committee scheme.
prop_roundtrip_vote ::
  forall vote crypto committee.
  ( Show vote
  , Eq vote
  , PerasVoteCompatibleWithVotingCommittee vote crypto committee
  ) =>
  Proxy vote ->
  Proxy committee ->
  (vote -> Bool) ->
  Gen vote ->
  (vote -> Property -> Property) ->
  Property
prop_roundtrip_vote :: forall vote crypto committee.
(Show vote, Eq vote,
 PerasVoteCompatibleWithVotingCommittee vote crypto committee) =>
Proxy vote
-> Proxy committee
-> (vote -> Bool)
-> Gen vote
-> (vote -> Property -> Property)
-> Property
prop_roundtrip_vote Proxy vote
_ Proxy committee
_ vote -> Bool
shouldPass Gen vote
gen vote -> Property -> Property
tabulateValue =
  Gen vote -> (vote -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll Gen vote
gen ((vote -> Property) -> Property) -> (vote -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \vote
vote -> do
    vote -> Property -> Property
tabulateValue vote
vote (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
      case vote -> Either PerasConversionError (Vote crypto committee)
forall vote crypto committee.
PerasVoteCompatibleWithVotingCommittee vote crypto committee =>
vote -> Either PerasConversionError (Vote crypto committee)
fromPerasVote vote
vote of
        Left PerasConversionError
err
          | vote -> Bool
shouldPass vote
vote ->
              TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
                ( [TestName] -> TestName
unlines
                    [ TestName
"fromPerasVote failed with:"
                    , PerasConversionError -> TestName
forall a. Show a => a -> TestName
show PerasConversionError
err
                    , TestName
"Original vote:"
                    , vote -> TestName
forall a. Show a => a -> TestName
show vote
vote
                    ]
                )
                Bool
False
          | Bool
otherwise ->
              TestName -> Property -> Property
tabulateOutcome TestName
"Fails as expected" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
                Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
        Right (Vote crypto committee
committeeVote :: Committee.Vote crypto committee) ->
          case Vote crypto committee -> Either PerasConversionError vote
forall vote crypto committee.
PerasVoteCompatibleWithVotingCommittee vote crypto committee =>
Vote crypto committee -> Either PerasConversionError vote
toPerasVote Vote crypto committee
committeeVote of
            Left PerasConversionError
err ->
              TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
                ( [TestName] -> TestName
unlines
                    [ TestName
"toPerasVote failed with:"
                    , PerasConversionError -> TestName
forall a. Show a => a -> TestName
show PerasConversionError
err
                    ]
                )
                (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
False
            Right vote
vote' ->
              TestName -> Property -> Property
tabulateOutcome TestName
"Roundtrips successfully"
                (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
                  ( [TestName] -> TestName
unlines
                      [ TestName
"Original vote:"
                      , vote -> TestName
forall a. Show a => a -> TestName
show vote
vote
                      , TestName
"Roundtripped vote:"
                      , vote -> TestName
forall a. Show a => a -> TestName
show vote
vote'
                      ]
                  )
                (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ vote
vote vote -> vote -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== vote
vote'

-- | Test that converting a concrete Peras cert to an committee cert and back
-- again results in the original Peras cert.
--
-- NOTE: this takes a predicate to determine whether triggering an exception is
-- a test failure or an expected outcome for the given voting committee scheme.
prop_roundtrip_cert ::
  forall cert crypto committee.
  ( Show cert
  , Eq cert
  , PerasCertCompatibleWithVotingCommittee cert crypto committee
  ) =>
  Proxy cert ->
  Proxy committee ->
  (cert -> Bool) ->
  Gen cert ->
  (cert -> Property -> Property) ->
  Property
prop_roundtrip_cert :: forall cert crypto committee.
(Show cert, Eq cert,
 PerasCertCompatibleWithVotingCommittee cert crypto committee) =>
Proxy cert
-> Proxy committee
-> (cert -> Bool)
-> Gen cert
-> (cert -> Property -> Property)
-> Property
prop_roundtrip_cert Proxy cert
_ Proxy committee
_ cert -> Bool
shouldPass Gen cert
gen cert -> Property -> Property
tabulateValue =
  Gen cert -> (cert -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll Gen cert
gen ((cert -> Property) -> Property) -> (cert -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \cert
cert -> do
    cert -> Property -> Property
tabulateValue cert
cert (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
      case cert -> Either PerasConversionError (Cert crypto committee)
forall cert crypto committee.
PerasCertCompatibleWithVotingCommittee cert crypto committee =>
cert -> Either PerasConversionError (Cert crypto committee)
fromPerasCert cert
cert of
        Left PerasConversionError
err
          | cert -> Bool
shouldPass cert
cert ->
              TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
                ( [TestName] -> TestName
unlines
                    [ TestName
"fromPerasCert failed with:"
                    , PerasConversionError -> TestName
forall a. Show a => a -> TestName
show PerasConversionError
err
                    , TestName
"Original cert:"
                    , cert -> TestName
forall a. Show a => a -> TestName
show cert
cert
                    ]
                )
                (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
False
          | Bool
otherwise ->
              TestName -> Property -> Property
tabulateOutcome TestName
"Fails as expected" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
                Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
        Right (Cert crypto committee
committeeCert :: Committee.Cert crypto committee) ->
          case Cert crypto committee -> Either PerasConversionError cert
forall cert crypto committee.
PerasCertCompatibleWithVotingCommittee cert crypto committee =>
Cert crypto committee -> Either PerasConversionError cert
toPerasCert Cert crypto committee
committeeCert of
            Left PerasConversionError
err ->
              TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
                ( [TestName] -> TestName
unlines
                    [ TestName
"toPerasCert failed with:"
                    , PerasConversionError -> TestName
forall a. Show a => a -> TestName
show PerasConversionError
err
                    ]
                )
                Bool
False
            Right cert
cert' ->
              TestName -> Property -> Property
tabulateOutcome TestName
"Roundtrips successfully"
                (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
                  ( [TestName] -> TestName
unlines
                      [ TestName
"Original cert:"
                      , cert -> TestName
forall a. Show a => a -> TestName
show cert
cert
                      , TestName
"Roundtripped cert:"
                      , cert -> TestName
forall a. Show a => a -> TestName
show cert
cert'
                      ]
                  )
                (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ cert
cert cert -> cert -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== cert
cert'

tabulateOutcome :: String -> Property -> Property
tabulateOutcome :: TestName -> Property -> Property
tabulateOutcome TestName
outcome = TestName -> [TestName] -> Property -> Property
forall prop.
Testable prop =>
TestName -> [TestName] -> prop -> Property
tabulate TestName
"Outcome" [TestName
outcome]