{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

module Test.Cardano.Ledger.Shelley.Rules.Pool (
  tests,
) where

import Cardano.Ledger.BaseTypes (EpochInterval (..), Network (..))
import Cardano.Ledger.Block (blockHeader)
import Cardano.Ledger.Core
import Cardano.Ledger.Shelley.LedgerState (
  NewEpochState (..),
  curPParamsEpochStateL,
 )
import Cardano.Ledger.Shelley.Rules (ShelleyPOOL)
import Cardano.Ledger.Shelley.State
import Cardano.Ledger.Slot (EpochNo (..))
import Cardano.Protocol.TPraos.BHeader (bhbody, bheaderSlotNo)
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import Lens.Micro.Extras (view)
import Test.Cardano.Ledger.Shelley.ConcreteCryptoTypes (MockCrypto)
import Test.Cardano.Ledger.Shelley.Constants (defaultConstants)
import Test.Cardano.Ledger.Shelley.Generator.Core (GenEnv)
import Test.Cardano.Ledger.Shelley.Generator.EraGen (EraGen (..))
import Test.Cardano.Ledger.Shelley.Generator.ShelleyEraGen ()
import Test.Cardano.Ledger.Shelley.Rules.Chain (CHAIN, ChainState (..))
import Test.Cardano.Ledger.Shelley.Rules.TestChain (
  forAllChainTrace,
  poolTraceFromBlock,
  traceLen,
 )
import Test.Cardano.Ledger.Shelley.Utils (
  ChainProperty,
  epochFromSlotNo,
 )
import Test.Control.State.Transition.Trace (
  SourceSignalTarget (..),
  TraceOrder (OldestFirst),
  sourceSignalTargets,
  traceStates,
 )
import qualified Test.Control.State.Transition.Trace.Generator.QuickCheck as QC
import Test.QuickCheck (
  Property,
  Testable (..),
  conjoin,
  counterexample,
  (===),
 )
import Test.Tasty (TestTree)
import Test.Tasty.QuickCheck (testProperty)

-- | Various properties of the POOL STS Rule, tested on longer traces
-- (double the default length)
tests ::
  forall era.
  ( EraGen era
  , EraStake era
  , ChainProperty era
  , QC.HasTrace (CHAIN era) (GenEnv MockCrypto era)
  ) =>
  TestTree
tests :: forall era.
(EraGen era, EraStake era, ChainProperty era,
 HasTrace (CHAIN era) (GenEnv MockCrypto era)) =>
TestTree
tests =
  String -> Property -> TestTree
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> TestTree
testProperty String
"properties of the POOL STS" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
    forall era prop.
(EraGen era, EraGov era, EraStake era, Testable prop,
 HasTrace (CHAIN era) (GenEnv MockCrypto era)) =>
Word64 -> Constants -> (Trace (CHAIN era) -> prop) -> Property
forAllChainTrace @era Word64
traceLen Constants
defaultConstants ((Trace (CHAIN era) -> Property) -> Property)
-> (Trace (CHAIN era) -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Trace (CHAIN era)
tr -> do
      let ssts :: [SourceSignalTarget (CHAIN era)]
ssts = Trace (CHAIN era) -> [SourceSignalTarget (CHAIN era)]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (CHAIN era)
tr
      [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ([Property] -> Property)
-> ([[Property]] -> [Property]) -> [[Property]] -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Property]] -> [Property]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Property]] -> Property) -> [[Property]] -> Property
forall a b. (a -> b) -> a -> b
$
        [ (SourceSignalTarget (CHAIN era) -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget (CHAIN era) -> Property
forall era.
ChainProperty era =>
SourceSignalTarget (CHAIN era) -> Property
poolRetirement [SourceSignalTarget (CHAIN era)]
ssts
        , (SourceSignalTarget (CHAIN era) -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget (CHAIN era) -> Property
forall era.
ChainProperty era =>
SourceSignalTarget (CHAIN era) -> Property
poolRegistration [SourceSignalTarget (CHAIN era)]
ssts
        , (SourceSignalTarget (CHAIN era) -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget (CHAIN era) -> Property
forall era.
ChainProperty era =>
SourceSignalTarget (CHAIN era) -> Property
poolStateIsInternallyConsistent [SourceSignalTarget (CHAIN era)]
ssts
        ]

-- | Check that a `RetirePool` certificate properly marks a stake pool for
-- retirement.
poolRetirement ::
  ChainProperty era =>
  SourceSignalTarget (CHAIN era) ->
  Property
poolRetirement :: forall era.
ChainProperty era =>
SourceSignalTarget (CHAIN era) -> Property
poolRetirement SourceSignalTarget {source :: forall a. SourceSignalTarget a -> State a
source = State (CHAIN era)
chainSt, signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal (CHAIN era)
block} =
  [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ([Property] -> Property) -> [Property] -> Property
forall a b. (a -> b) -> a -> b
$
    (SourceSignalTarget (ShelleyPOOL era) -> Property)
-> [SourceSignalTarget (ShelleyPOOL era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map (EpochNo
-> EpochInterval
-> SourceSignalTarget (ShelleyPOOL era)
-> Property
forall era.
EpochNo
-> EpochInterval
-> SourceSignalTarget (ShelleyPOOL era)
-> Property
poolRetirementProp EpochNo
currentEpoch EpochInterval
maxEpoch) (Trace (ShelleyPOOL era) -> [SourceSignalTarget (ShelleyPOOL era)]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (ShelleyPOOL era)
poolTr)
  where
    (ChainState era
chainSt', Trace (ShelleyPOOL era)
poolTr) = ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, Trace (ShelleyPOOL era))
forall era.
ChainProperty era =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, Trace (ShelleyPOOL era))
poolTraceFromBlock State (CHAIN era)
ChainState era
chainSt Block (BHeader MockCrypto) era
Signal (CHAIN era)
block
    bhb :: BHBody MockCrypto
bhb = BHeader MockCrypto -> BHBody MockCrypto
forall c. Crypto c => BHeader c -> BHBody c
bhbody (BHeader MockCrypto -> BHBody MockCrypto)
-> BHeader MockCrypto -> BHBody MockCrypto
forall a b. (a -> b) -> a -> b
$ Block (BHeader MockCrypto) era -> BHeader MockCrypto
forall h era. Block h era -> h
blockHeader Block (BHeader MockCrypto) era
Signal (CHAIN era)
block
    currentEpoch :: EpochNo
currentEpoch = (SlotNo -> EpochNo
epochFromSlotNo (SlotNo -> EpochNo)
-> (BHBody MockCrypto -> SlotNo) -> BHBody MockCrypto -> EpochNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BHBody MockCrypto -> SlotNo
forall c. BHBody c -> SlotNo
bheaderSlotNo) BHBody MockCrypto
bhb
    maxEpoch :: EpochInterval
maxEpoch = (Getting EpochInterval (PParams era) EpochInterval
-> PParams era -> EpochInterval
forall a s. Getting a s a -> s -> a
view Getting EpochInterval (PParams era) EpochInterval
forall era. EraPParams era => Lens' (PParams era) EpochInterval
Lens' (PParams era) EpochInterval
ppEMaxL (PParams era -> EpochInterval)
-> (ChainState era -> PParams era)
-> ChainState era
-> EpochInterval
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting (PParams era) (EpochState era) (PParams era)
-> EpochState era -> PParams era
forall a s. Getting a s a -> s -> a
view Getting (PParams era) (EpochState era) (PParams era)
forall era. EraGov era => Lens' (EpochState era) (PParams era)
Lens' (EpochState era) (PParams era)
curPParamsEpochStateL (EpochState era -> PParams era)
-> (ChainState era -> EpochState era)
-> ChainState era
-> PParams era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewEpochState era -> EpochState era
forall era. NewEpochState era -> EpochState era
nesEs (NewEpochState era -> EpochState era)
-> (ChainState era -> NewEpochState era)
-> ChainState era
-> EpochState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChainState era -> NewEpochState era
forall era. ChainState era -> NewEpochState era
chainNes) ChainState era
chainSt'

-- | Check that a newly registered pool key is registered and not
-- in the retiring map.
poolRegistration ::
  ChainProperty era =>
  SourceSignalTarget (CHAIN era) ->
  Property
poolRegistration :: forall era.
ChainProperty era =>
SourceSignalTarget (CHAIN era) -> Property
poolRegistration (SourceSignalTarget {source :: forall a. SourceSignalTarget a -> State a
source = State (CHAIN era)
chainSt, signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal (CHAIN era)
block}) =
  [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ([Property] -> Property) -> [Property] -> Property
forall a b. (a -> b) -> a -> b
$
    (SourceSignalTarget (ShelleyPOOL era) -> Property)
-> [SourceSignalTarget (ShelleyPOOL era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget (ShelleyPOOL era) -> Property
forall era. SourceSignalTarget (ShelleyPOOL era) -> Property
poolRegistrationProp (Trace (ShelleyPOOL era) -> [SourceSignalTarget (ShelleyPOOL era)]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (ShelleyPOOL era)
poolTr)
  where
    (ChainState era
_, Trace (ShelleyPOOL era)
poolTr) = ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, Trace (ShelleyPOOL era))
forall era.
ChainProperty era =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, Trace (ShelleyPOOL era))
poolTraceFromBlock State (CHAIN era)
ChainState era
chainSt Block (BHeader MockCrypto) era
Signal (CHAIN era)
block

-- | Assert that PState maps are in sync with each other after each `Signal
-- POOL` transition.
poolStateIsInternallyConsistent ::
  ChainProperty era =>
  SourceSignalTarget (CHAIN era) ->
  Property
poolStateIsInternallyConsistent :: forall era.
ChainProperty era =>
SourceSignalTarget (CHAIN era) -> Property
poolStateIsInternallyConsistent (SourceSignalTarget {source :: forall a. SourceSignalTarget a -> State a
source = State (CHAIN era)
chainSt, signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal (CHAIN era)
block}) =
  [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ([Property] -> Property) -> [Property] -> Property
forall a b. (a -> b) -> a -> b
$
    (PState era -> Property) -> [PState era] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map PState era -> Property
forall c. PState c -> Property
poolStateIsInternallyConsistentProp (TraceOrder -> Trace (ShelleyPOOL era) -> [State (ShelleyPOOL era)]
forall s. TraceOrder -> Trace s -> [State s]
traceStates TraceOrder
OldestFirst Trace (ShelleyPOOL era)
poolTr)
  where
    (ChainState era
_, Trace (ShelleyPOOL era)
poolTr) = ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, Trace (ShelleyPOOL era))
forall era.
ChainProperty era =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, Trace (ShelleyPOOL era))
poolTraceFromBlock State (CHAIN era)
ChainState era
chainSt Block (BHeader MockCrypto) era
Signal (CHAIN era)
block

poolRegistrationProp :: SourceSignalTarget (ShelleyPOOL era) -> Property
poolRegistrationProp :: forall era. SourceSignalTarget (ShelleyPOOL era) -> Property
poolRegistrationProp
  SourceSignalTarget
    { signal :: forall a. SourceSignalTarget a -> Signal a
signal = RegPool StakePoolParams
stakePoolParams
    , source :: forall a. SourceSignalTarget a -> State a
source = State (ShelleyPOOL era)
sourceSt
    , target :: forall a. SourceSignalTarget a -> State a
target = State (ShelleyPOOL era)
targetSt
    } =
    let hk :: KeyHash StakePool
hk = StakePoolParams -> KeyHash StakePool
sppId StakePoolParams
stakePoolParams
     in case KeyHash StakePool
-> Map (KeyHash StakePool) StakePoolState -> Maybe StakePoolState
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KeyHash StakePool
hk (Map (KeyHash StakePool) StakePoolState -> Maybe StakePoolState)
-> Map (KeyHash StakePool) StakePoolState -> Maybe StakePoolState
forall a b. (a -> b) -> a -> b
$ PState era -> Map (KeyHash StakePool) StakePoolState
forall era. PState era -> Map (KeyHash StakePool) StakePoolState
psStakePools PState era
State (ShelleyPOOL era)
sourceSt of
          Just StakePoolState
_ ->
            [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
              [ String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
                  String
"Pre-existing StakePoolParams must still be registered in pParams"
                  (KeyHash StakePool -> Map (KeyHash StakePool) StakePoolState -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member KeyHash StakePool
hk (PState era -> Map (KeyHash StakePool) StakePoolState
forall era. PState era -> Map (KeyHash StakePool) StakePoolState
psStakePools PState era
State (ShelleyPOOL era)
targetSt) :: Bool)
              , String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
                  String
"New StakePoolParams are registered in future Params map"
                  ( KeyHash StakePool
-> Map (KeyHash StakePool) StakePoolParams -> Maybe StakePoolParams
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KeyHash StakePool
hk (PState era -> Map (KeyHash StakePool) StakePoolParams
forall era. PState era -> Map (KeyHash StakePool) StakePoolParams
psFutureStakePoolParams PState era
State (ShelleyPOOL era)
targetSt)
                      Maybe StakePoolParams -> Maybe StakePoolParams -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== StakePoolParams -> Maybe StakePoolParams
forall a. a -> Maybe a
Just StakePoolParams
stakePoolParams
                  )
              , String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
                  String
"StakePoolParams are removed in 'retiring'"
                  (KeyHash StakePool -> Map (KeyHash StakePool) EpochNo -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.notMember KeyHash StakePool
hk (PState era -> Map (KeyHash StakePool) EpochNo
forall era. PState era -> Map (KeyHash StakePool) EpochNo
psRetiring PState era
State (ShelleyPOOL era)
targetSt) :: Bool)
              ]
          Maybe StakePoolState
Nothing ->
            -- first registration
            [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
              [ String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
                  String
"New StakePoolParams are registered in pParams"
                  ( (KeyHash StakePool -> Network -> StakePoolState -> StakePoolParams
stakePoolStateToStakePoolParams KeyHash StakePool
hk Network
Testnet (StakePoolState -> StakePoolParams)
-> Maybe StakePoolState -> Maybe StakePoolParams
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KeyHash StakePool
-> Map (KeyHash StakePool) StakePoolState -> Maybe StakePoolState
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KeyHash StakePool
hk (PState era -> Map (KeyHash StakePool) StakePoolState
forall era. PState era -> Map (KeyHash StakePool) StakePoolState
psStakePools PState era
State (ShelleyPOOL era)
targetSt))
                      Maybe StakePoolParams -> Maybe StakePoolParams -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== StakePoolParams -> Maybe StakePoolParams
forall a. a -> Maybe a
Just StakePoolParams
stakePoolParams
                  )
              , String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
                  String
"StakePoolParams are not present in 'future pool params'"
                  (KeyHash StakePool
-> Map (KeyHash StakePool) StakePoolParams -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.notMember KeyHash StakePool
hk (PState era -> Map (KeyHash StakePool) StakePoolParams
forall era. PState era -> Map (KeyHash StakePool) StakePoolParams
psFutureStakePoolParams PState era
State (ShelleyPOOL era)
targetSt) :: Bool)
              , String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
                  String
"StakePoolParams are removed in 'retiring'"
                  (KeyHash StakePool -> Map (KeyHash StakePool) EpochNo -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.notMember KeyHash StakePool
hk (PState era -> Map (KeyHash StakePool) EpochNo
forall era. PState era -> Map (KeyHash StakePool) EpochNo
psRetiring PState era
State (ShelleyPOOL era)
targetSt) :: Bool)
              ]
poolRegistrationProp SourceSignalTarget (ShelleyPOOL era)
_ = () -> Property
forall prop. Testable prop => prop -> Property
property ()

poolRetirementProp ::
  EpochNo ->
  EpochInterval ->
  SourceSignalTarget (ShelleyPOOL era) ->
  Property
poolRetirementProp :: forall era.
EpochNo
-> EpochInterval
-> SourceSignalTarget (ShelleyPOOL era)
-> Property
poolRetirementProp
  currentEpoch :: EpochNo
currentEpoch@(EpochNo Word64
ce)
  (EpochInterval Word32
maxEpoch)
  SourceSignalTarget {source :: forall a. SourceSignalTarget a -> State a
source = State (ShelleyPOOL era)
sourceSt, target :: forall a. SourceSignalTarget a -> State a
target = State (ShelleyPOOL era)
targetSt, signal :: forall a. SourceSignalTarget a -> Signal a
signal = RetirePool KeyHash StakePool
hk EpochNo
e} =
    [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
      [ String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
          (String
"epoch must be well formed " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Word64 -> String
forall a. Show a => a -> String
show Word64
ce String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> EpochNo -> String
forall a. Show a => a -> String
show EpochNo
e String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Word32 -> String
forall a. Show a => a -> String
show Word32
maxEpoch)
          (EpochNo
currentEpoch EpochNo -> EpochNo -> Bool
forall a. Ord a => a -> a -> Bool
< EpochNo
e Bool -> Bool -> Bool
&& EpochNo
e EpochNo -> EpochNo -> Bool
forall a. Ord a => a -> a -> Bool
< Word64 -> EpochNo
EpochNo (Word64
ce Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word32 -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
maxEpoch))
      , String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
          String
"hk must be in source stPools"
          (KeyHash StakePool -> Map (KeyHash StakePool) StakePoolState -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member KeyHash StakePool
hk (PState era -> Map (KeyHash StakePool) StakePoolState
forall era. PState era -> Map (KeyHash StakePool) StakePoolState
psStakePools PState era
State (ShelleyPOOL era)
sourceSt) :: Bool)
      , String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
          String
"hk must be in target stPools"
          (KeyHash StakePool -> Map (KeyHash StakePool) StakePoolState -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member KeyHash StakePool
hk (PState era -> Map (KeyHash StakePool) StakePoolState
forall era. PState era -> Map (KeyHash StakePool) StakePoolState
psStakePools PState era
State (ShelleyPOOL era)
targetSt) :: Bool)
      , String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
          String
"hk must be in target's retiring"
          (KeyHash StakePool -> Map (KeyHash StakePool) EpochNo -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member KeyHash StakePool
hk (PState era -> Map (KeyHash StakePool) EpochNo
forall era. PState era -> Map (KeyHash StakePool) EpochNo
psRetiring PState era
State (ShelleyPOOL era)
targetSt) :: Bool)
      ]
poolRetirementProp EpochNo
_ EpochInterval
_ SourceSignalTarget (ShelleyPOOL era)
_ = () -> Property
forall prop. Testable prop => prop -> Property
property ()

poolStateIsInternallyConsistentProp :: PState c -> Property
poolStateIsInternallyConsistentProp :: forall c. PState c -> Property
poolStateIsInternallyConsistentProp PState {psStakePools :: forall era. PState era -> Map (KeyHash StakePool) StakePoolState
psStakePools = Map (KeyHash StakePool) StakePoolState
pParams_, psRetiring :: forall era. PState era -> Map (KeyHash StakePool) EpochNo
psRetiring = Map (KeyHash StakePool) EpochNo
retiring_} = do
  let poolKeys :: Set (KeyHash StakePool)
poolKeys = Map (KeyHash StakePool) StakePoolState -> Set (KeyHash StakePool)
forall k a. Map k a -> Set k
Map.keysSet Map (KeyHash StakePool) StakePoolState
pParams_
      pParamKeys :: Set (KeyHash StakePool)
pParamKeys = Map (KeyHash StakePool) StakePoolState -> Set (KeyHash StakePool)
forall k a. Map k a -> Set k
Map.keysSet Map (KeyHash StakePool) StakePoolState
pParams_
      retiringKeys :: Set (KeyHash StakePool)
retiringKeys = Map (KeyHash StakePool) EpochNo -> Set (KeyHash StakePool)
forall k a. Map k a -> Set k
Map.keysSet Map (KeyHash StakePool) EpochNo
retiring_

  [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
    [ String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
        String
"All pool keys should be in both stPools and pParams"
        (Set (KeyHash StakePool)
poolKeys Set (KeyHash StakePool) -> Set (KeyHash StakePool) -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Set (KeyHash StakePool)
pParamKeys)
    , String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
        String
"A retiring pool should still be registered in `stPools`"
        ((Set (KeyHash StakePool)
retiringKeys Set (KeyHash StakePool) -> Set (KeyHash StakePool) -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set (KeyHash StakePool)
poolKeys) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
True)
    ]