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

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

import Cardano.Ledger.Block (Block (..))
import Cardano.Ledger.Shelley.LedgerState (
  NewEpochState (..),
  esLStateL,
  lsCertStateL,
  nesEsL,
 )
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 ((^.))
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 (
  chainSstWithTick,
  forAllChainTrace,
  traceLen,
 )
import Test.Cardano.Ledger.Shelley.Utils (
  ChainProperty,
  epochFromSlotNo,
 )
import Test.Control.State.Transition.Trace (
  SourceSignalTarget (..),
 )
import qualified Test.Control.State.Transition.Trace.Generator.QuickCheck as QC
import Test.QuickCheck (
  Property,
  Testable (..),
  conjoin,
 )
import Test.Tasty (TestTree)
import Test.Tasty.QuickCheck (testProperty)

----------------------------------------------------------------------
-- Properties for PoolReap (using the CHAIN Trace) --
----------------------------------------------------------------------

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
"pool is removed from stake pool and retiring maps" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
    Word64 -> Constants -> (Trace (CHAIN era) -> Property) -> Property
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 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 ->
      [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ([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
removedAfterPoolreap_ ([SourceSignalTarget (CHAIN era)] -> [Property])
-> [SourceSignalTarget (CHAIN era)] -> [Property]
forall a b. (a -> b) -> a -> b
$
          (SourceSignalTarget (CHAIN era) -> Bool)
-> [SourceSignalTarget (CHAIN era)]
-> [SourceSignalTarget (CHAIN era)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (SourceSignalTarget (CHAIN era) -> Bool)
-> SourceSignalTarget (CHAIN era)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceSignalTarget (CHAIN era) -> Bool
forall era. SourceSignalTarget (CHAIN era) -> Bool
sameEpoch) (Trace (CHAIN era) -> [SourceSignalTarget (CHAIN era)]
forall era.
ChainProperty era =>
Trace (CHAIN era) -> [SourceSignalTarget (CHAIN era)]
chainSstWithTick Trace (CHAIN era)
tr)
  where
    stakePools :: ChainState era -> PState era
stakePools ChainState era
target = (ChainState era -> NewEpochState era
forall era. ChainState era -> NewEpochState era
chainNes ChainState era
target) NewEpochState era
-> Getting (PState era) (NewEpochState era) (PState era)
-> PState era
forall s a. s -> Getting a s a -> a
^. (EpochState era -> Const (PState era) (EpochState era))
-> NewEpochState era -> Const (PState era) (NewEpochState era)
forall era (f :: * -> *).
Functor f =>
(EpochState era -> f (EpochState era))
-> NewEpochState era -> f (NewEpochState era)
nesEsL ((EpochState era -> Const (PState era) (EpochState era))
 -> NewEpochState era -> Const (PState era) (NewEpochState era))
-> ((PState era -> Const (PState era) (PState era))
    -> EpochState era -> Const (PState era) (EpochState era))
-> Getting (PState era) (NewEpochState era) (PState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LedgerState era -> Const (PState era) (LedgerState era))
-> EpochState era -> Const (PState era) (EpochState era)
forall era (f :: * -> *).
Functor f =>
(LedgerState era -> f (LedgerState era))
-> EpochState era -> f (EpochState era)
esLStateL ((LedgerState era -> Const (PState era) (LedgerState era))
 -> EpochState era -> Const (PState era) (EpochState era))
-> ((PState era -> Const (PState era) (PState era))
    -> LedgerState era -> Const (PState era) (LedgerState era))
-> (PState era -> Const (PState era) (PState era))
-> EpochState era
-> Const (PState era) (EpochState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CertState era -> Const (PState era) (CertState era))
-> LedgerState era -> Const (PState era) (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL ((CertState era -> Const (PState era) (CertState era))
 -> LedgerState era -> Const (PState era) (LedgerState era))
-> ((PState era -> Const (PState era) (PState era))
    -> CertState era -> Const (PState era) (CertState era))
-> (PState era -> Const (PState era) (PState era))
-> LedgerState era
-> Const (PState era) (LedgerState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PState era -> Const (PState era) (PState era))
-> CertState era -> Const (PState era) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL

    removedAfterPoolreap_ :: SourceSignalTarget (CHAIN era) -> Property
    removedAfterPoolreap_ :: SourceSignalTarget (CHAIN era) -> Property
removedAfterPoolreap_ (SourceSignalTarget {State (CHAIN era)
source :: State (CHAIN era)
source :: forall a. SourceSignalTarget a -> State a
source, State (CHAIN era)
target :: State (CHAIN era)
target :: forall a. SourceSignalTarget a -> State a
target, signal :: forall a. SourceSignalTarget a -> Signal a
signal = (Block BHeader MockCrypto
bh BlockBody era
_)}) =
      let e :: EpochNo
e = (SlotNo -> EpochNo
epochFromSlotNo (SlotNo -> EpochNo)
-> (BHeader MockCrypto -> SlotNo) -> BHeader MockCrypto -> EpochNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BHBody MockCrypto -> SlotNo
forall c. BHBody c -> SlotNo
bheaderSlotNo (BHBody MockCrypto -> SlotNo)
-> (BHeader MockCrypto -> BHBody MockCrypto)
-> BHeader MockCrypto
-> SlotNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BHeader MockCrypto -> BHBody MockCrypto
forall c. Crypto c => BHeader c -> BHBody c
bhbody) BHeader MockCrypto
bh
       in PState era -> PState era -> EpochNo -> Property
forall era. PState era -> PState era -> EpochNo -> Property
removedAfterPoolreap (ChainState era -> PState era
forall {era}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 EraCertState era) =>
ChainState era -> PState era
stakePools State (CHAIN era)
ChainState era
source) (ChainState era -> PState era
forall {era}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 EraCertState era) =>
ChainState era -> PState era
stakePools State (CHAIN era)
ChainState era
target) EpochNo
e

-- | Check that after a POOLREAP certificate transition the pool is removed from
-- the stake pool and retiring maps.
removedAfterPoolreap ::
  forall era.
  PState era ->
  PState era ->
  EpochNo ->
  Property
removedAfterPoolreap :: forall era. PState era -> PState era -> EpochNo -> Property
removedAfterPoolreap PState era
p PState era
p' EpochNo
epoch =
  Bool -> Property
forall prop. Testable prop => prop -> Property
property (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$
    (Set (KeyHash StakePool)
retire Set (KeyHash StakePool) -> Set (KeyHash StakePool) -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` (Map (KeyHash StakePool) StakePoolState -> Set (KeyHash StakePool)
forall k a. Map k a -> Set k
Map.keysSet Map (KeyHash StakePool) StakePoolState
stp))
      Bool -> Bool -> Bool
&& Set (KeyHash StakePool) -> Bool
forall a. Set a -> Bool
Set.null (Set (KeyHash StakePool)
-> Set (KeyHash StakePool) -> Set (KeyHash StakePool)
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set (KeyHash StakePool)
retire (Map (KeyHash StakePool) StakePoolState -> Set (KeyHash StakePool)
forall k a. Map k a -> Set k
Map.keysSet Map (KeyHash StakePool) StakePoolState
stp'))
      Bool -> Bool -> Bool
&& Set (KeyHash StakePool) -> Bool
forall a. Set a -> Bool
Set.null (Set (KeyHash StakePool)
-> Set (KeyHash StakePool) -> Set (KeyHash StakePool)
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set (KeyHash StakePool)
retire (Map (KeyHash StakePool) EpochNo -> Set (KeyHash StakePool)
forall k a. Map k a -> Set k
Map.keysSet Map (KeyHash StakePool) EpochNo
retiring'))
  where
    stp :: Map (KeyHash StakePool) StakePoolState
stp = PState era -> Map (KeyHash StakePool) StakePoolState
forall era. PState era -> Map (KeyHash StakePool) StakePoolState
psStakePools PState era
p
    stp' :: Map (KeyHash StakePool) StakePoolState
stp' = PState era -> Map (KeyHash StakePool) StakePoolState
forall era. PState era -> Map (KeyHash StakePool) StakePoolState
psStakePools PState era
p'
    retiring :: Map (KeyHash StakePool) EpochNo
retiring = PState era -> Map (KeyHash StakePool) EpochNo
forall era. PState era -> Map (KeyHash StakePool) EpochNo
psRetiring PState era
p
    retiring' :: Map (KeyHash StakePool) EpochNo
retiring' = PState era -> Map (KeyHash StakePool) EpochNo
forall era. PState era -> Map (KeyHash StakePool) EpochNo
psRetiring PState era
p'
    retire :: Set (KeyHash StakePool)
retire = Map (KeyHash StakePool) EpochNo -> Set (KeyHash StakePool)
forall k a. Map k a -> Set k
Map.keysSet (Map (KeyHash StakePool) EpochNo -> Set (KeyHash StakePool))
-> Map (KeyHash StakePool) EpochNo -> Set (KeyHash StakePool)
forall a b. (a -> b) -> a -> b
$ (EpochNo -> Bool)
-> Map (KeyHash StakePool) EpochNo
-> Map (KeyHash StakePool) EpochNo
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (EpochNo
epoch EpochNo -> EpochNo -> Bool
forall a. Eq a => a -> a -> Bool
==) Map (KeyHash StakePool) EpochNo
retiring

sameEpoch ::
  forall era.
  SourceSignalTarget (CHAIN era) ->
  Bool
sameEpoch :: forall era. SourceSignalTarget (CHAIN era) -> Bool
sameEpoch SourceSignalTarget {State (CHAIN era)
source :: forall a. SourceSignalTarget a -> State a
source :: State (CHAIN era)
source, State (CHAIN era)
target :: forall a. SourceSignalTarget a -> State a
target :: State (CHAIN era)
target} =
  ChainState era -> EpochNo
forall {era}. ChainState era -> EpochNo
epoch State (CHAIN era)
ChainState era
source EpochNo -> EpochNo -> Bool
forall a. Eq a => a -> a -> Bool
== ChainState era -> EpochNo
forall {era}. ChainState era -> EpochNo
epoch State (CHAIN era)
ChainState era
target
  where
    epoch :: ChainState era -> EpochNo
epoch = NewEpochState era -> EpochNo
forall era. NewEpochState era -> EpochNo
nesEL (NewEpochState era -> EpochNo)
-> (ChainState era -> NewEpochState era)
-> ChainState era
-> EpochNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChainState era -> NewEpochState era
forall era. ChainState era -> NewEpochState era
chainNes