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

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

import Cardano.Ledger.BaseTypes (EpochInterval (..))
import Cardano.Ledger.Block (
  bheader,
 )
import Cardano.Ledger.Core
import Cardano.Ledger.PoolParams (ppId)
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.LedgerState (
  NewEpochState (..),
  PState (..),
  curPParamsEpochStateL,
  psFutureStakePoolParams,
  psStakePoolParams,
 )
import Cardano.Ledger.Shelley.Rules (ShelleyPOOL)
import Cardano.Ledger.Slot (EpochNo (..))
import Cardano.Protocol.TPraos.BHeader (
  bhbody,
  bheaderSlotNo,
 )
import Control.SetAlgebra (dom, eval, (∈), (∉))
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import Lens.Micro.Extras (view)
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.Control.State.Transition.Trace (
  SourceSignalTarget (..),
  TraceOrder (OldestFirst),
  sourceSignalTargets,
  traceStates,
 )
import qualified Test.Control.State.Transition.Trace.Generator.QuickCheck as QC
import Test.QuickCheck (Property, conjoin, counterexample, (===))

import Test.Cardano.Ledger.Shelley.Rules.TestChain (
  forAllChainTrace,
  poolTraceFromBlock,
  traceLen,
 )
import Test.Cardano.Ledger.Shelley.Utils (
  ChainProperty,
  epochFromSlotNo,
 )
import Test.QuickCheck (
  Testable (..),
 )
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
  , ChainProperty era
  , QC.HasTrace (CHAIN era) (GenEnv era)
  ) =>
  TestTree
tests :: forall era.
(EraGen era, ChainProperty era,
 HasTrace (CHAIN era) (GenEnv era)) =>
TestTree
tests =
  forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"properties of the POOL STS" forall a b. (a -> b) -> a -> b
$
    forall era prop.
(Testable prop, EraGen era, HasTrace (CHAIN era) (GenEnv era),
 EraGov era) =>
Word64 -> Constants -> (Trace (CHAIN era) -> prop) -> Property
forAllChainTrace @era Word64
traceLen Constants
defaultConstants forall a b. (a -> b) -> a -> b
$ \Trace (CHAIN era)
tr -> do
      let ssts :: [SourceSignalTarget (CHAIN era)]
ssts = forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (CHAIN era)
tr
      forall prop. Testable prop => [prop] -> Property
conjoin forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$
        [ forall a b. (a -> b) -> [a] -> [b]
map forall era.
(ChainProperty era, EraSegWits era, ShelleyEraTxBody era) =>
SourceSignalTarget (CHAIN era) -> Property
poolRetirement [SourceSignalTarget (CHAIN era)]
ssts
        , forall a b. (a -> b) -> [a] -> [b]
map forall era.
(ChainProperty era, EraSegWits era, ShelleyEraTxBody era) =>
SourceSignalTarget (CHAIN era) -> Property
poolRegistration [SourceSignalTarget (CHAIN era)]
ssts
        , forall a b. (a -> b) -> [a] -> [b]
map forall era.
(ChainProperty era, EraSegWits era, ShelleyEraTxBody 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
  , EraSegWits era
  , ShelleyEraTxBody era
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
poolRetirement :: forall era.
(ChainProperty era, EraSegWits era, ShelleyEraTxBody 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} =
  forall prop. Testable prop => [prop] -> Property
conjoin forall a b. (a -> b) -> a -> b
$
    forall a b. (a -> b) -> [a] -> [b]
map (forall era.
EpochNo
-> EpochInterval
-> SourceSignalTarget (ShelleyPOOL era)
-> Property
poolRetirementProp EpochNo
currentEpoch EpochInterval
maxEpoch) (forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (ShelleyPOOL era)
poolTr)
  where
    (ChainState era
chainSt', Trace (ShelleyPOOL era)
poolTr) = forall era.
(ChainProperty era, ShelleyEraTxBody era, EraSegWits era) =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, Trace (ShelleyPOOL era))
poolTraceFromBlock State (CHAIN era)
chainSt Signal (CHAIN era)
block
    bhb :: BHBody MockCrypto
bhb = forall c. Crypto c => BHeader c -> BHBody c
bhbody forall a b. (a -> b) -> a -> b
$ forall h era. Block h era -> h
bheader Signal (CHAIN era)
block
    currentEpoch :: EpochNo
currentEpoch = (SlotNo -> EpochNo
epochFromSlotNo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c. BHBody c -> SlotNo
bheaderSlotNo) BHBody MockCrypto
bhb
    maxEpoch :: EpochInterval
maxEpoch = (forall a s. Getting a s a -> s -> a
view forall era. EraPParams era => Lens' (PParams era) EpochInterval
ppEMaxL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a s. Getting a s a -> s -> a
view forall era. EraGov era => Lens' (EpochState era) (PParams era)
curPParamsEpochStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. NewEpochState era -> EpochState era
nesEs forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
  , EraSegWits era
  , ShelleyEraTxBody era
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
poolRegistration :: forall era.
(ChainProperty era, EraSegWits era, ShelleyEraTxBody 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}) =
  forall prop. Testable prop => [prop] -> Property
conjoin forall a b. (a -> b) -> a -> b
$
    forall a b. (a -> b) -> [a] -> [b]
map forall era. SourceSignalTarget (ShelleyPOOL era) -> Property
poolRegistrationProp (forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (ShelleyPOOL era)
poolTr)
  where
    (ChainState era
_, Trace (ShelleyPOOL era)
poolTr) = forall era.
(ChainProperty era, ShelleyEraTxBody era, EraSegWits era) =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, Trace (ShelleyPOOL era))
poolTraceFromBlock State (CHAIN era)
chainSt Signal (CHAIN era)
block

-- | Assert that PState maps are in sync with each other after each `Signal
-- POOL` transition.
poolStateIsInternallyConsistent ::
  ( ChainProperty era
  , EraSegWits era
  , ShelleyEraTxBody era
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
poolStateIsInternallyConsistent :: forall era.
(ChainProperty era, EraSegWits era, ShelleyEraTxBody 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}) =
  forall prop. Testable prop => [prop] -> Property
conjoin forall a b. (a -> b) -> a -> b
$
    forall a b. (a -> b) -> [a] -> [b]
map forall c. PState c -> Property
poolStateIsInternallyConsistentProp (forall s. TraceOrder -> Trace s -> [State s]
traceStates TraceOrder
OldestFirst Trace (ShelleyPOOL era)
poolTr)
  where
    (ChainState era
_, Trace (ShelleyPOOL era)
poolTr) = forall era.
(ChainProperty era, ShelleyEraTxBody era, EraSegWits era) =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, Trace (ShelleyPOOL era))
poolTraceFromBlock State (CHAIN era)
chainSt 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 PoolParams
poolParams
    , 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 = PoolParams -> KeyHash 'StakePool
ppId PoolParams
poolParams
        reRegistration :: Bool
reRegistration = forall s t. Embed s t => Exp t -> s
eval (KeyHash 'StakePool
hk forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∈ forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom (forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams State (ShelleyPOOL era)
sourceSt))
     in if Bool
reRegistration
          then
            forall prop. Testable prop => [prop] -> Property
conjoin
              [ forall prop. Testable prop => TestName -> prop -> Property
counterexample
                  TestName
"Pre-existing PoolParams must still be registered in pParams"
                  (forall s t. Embed s t => Exp t -> s
eval (KeyHash 'StakePool
hk forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∈ forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom (forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams State (ShelleyPOOL era)
targetSt)) :: Bool)
              , forall prop. Testable prop => TestName -> prop -> Property
counterexample
                  TestName
"New PoolParams are registered in future Params map"
                  (forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KeyHash 'StakePool
hk (forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psFutureStakePoolParams State (ShelleyPOOL era)
targetSt) forall a. (Eq a, Show a) => a -> a -> Property
=== forall a. a -> Maybe a
Just PoolParams
poolParams)
              , forall prop. Testable prop => TestName -> prop -> Property
counterexample
                  TestName
"PoolParams are removed in 'retiring'"
                  (forall s t. Embed s t => Exp t -> s
eval (KeyHash 'StakePool
hk forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∉ forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom (forall era. PState era -> Map (KeyHash 'StakePool) EpochNo
psRetiring State (ShelleyPOOL era)
targetSt)) :: Bool)
              ]
          else -- first registration
            forall prop. Testable prop => [prop] -> Property
conjoin
              [ forall prop. Testable prop => TestName -> prop -> Property
counterexample
                  TestName
"New PoolParams are registered in pParams"
                  (forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KeyHash 'StakePool
hk (forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams State (ShelleyPOOL era)
targetSt) forall a. (Eq a, Show a) => a -> a -> Property
=== forall a. a -> Maybe a
Just PoolParams
poolParams)
              , forall prop. Testable prop => TestName -> prop -> Property
counterexample
                  TestName
"PoolParams are not present in 'future pool params'"
                  (forall s t. Embed s t => Exp t -> s
eval (KeyHash 'StakePool
hk forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∉ forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom (forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psFutureStakePoolParams State (ShelleyPOOL era)
targetSt)) :: Bool)
              , forall prop. Testable prop => TestName -> prop -> Property
counterexample
                  TestName
"PoolParams are removed in 'retiring'"
                  (forall s t. Embed s t => Exp t -> s
eval (KeyHash 'StakePool
hk forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∉ forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom (forall era. PState era -> Map (KeyHash 'StakePool) EpochNo
psRetiring State (ShelleyPOOL era)
targetSt)) :: Bool)
              ]
poolRegistrationProp SourceSignalTarget (ShelleyPOOL era)
_ = 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} =
    forall prop. Testable prop => [prop] -> Property
conjoin
      [ forall prop. Testable prop => TestName -> prop -> Property
counterexample
          (TestName
"epoch must be well formed " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> TestName
show Word64
ce forall a. Semigroup a => a -> a -> a
<> TestName
" " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> TestName
show EpochNo
e forall a. Semigroup a => a -> a -> a
<> TestName
" " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> TestName
show Word32
maxEpoch)
          (EpochNo
currentEpoch forall a. Ord a => a -> a -> Bool
< EpochNo
e Bool -> Bool -> Bool
&& EpochNo
e forall a. Ord a => a -> a -> Bool
< Word64 -> EpochNo
EpochNo (Word64
ce forall a. Num a => a -> a -> a
+ forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
maxEpoch))
      , forall prop. Testable prop => TestName -> prop -> Property
counterexample
          TestName
"hk must be in source stPools"
          (forall s t. Embed s t => Exp t -> s
eval (KeyHash 'StakePool
hk forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∈ forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom (forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams State (ShelleyPOOL era)
sourceSt)) :: Bool)
      , forall prop. Testable prop => TestName -> prop -> Property
counterexample
          TestName
"hk must be in target stPools"
          (forall s t. Embed s t => Exp t -> s
eval (KeyHash 'StakePool
hk forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∈ forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom (forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams State (ShelleyPOOL era)
targetSt)) :: Bool)
      , forall prop. Testable prop => TestName -> prop -> Property
counterexample
          TestName
"hk must be in target's retiring"
          (forall s t. Embed s t => Exp t -> s
eval (KeyHash 'StakePool
hk forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∈ forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom (forall era. PState era -> Map (KeyHash 'StakePool) EpochNo
psRetiring State (ShelleyPOOL era)
targetSt)) :: Bool)
      ]
poolRetirementProp EpochNo
_ EpochInterval
_ SourceSignalTarget (ShelleyPOOL era)
_ = forall prop. Testable prop => prop -> Property
property ()

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

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