{-# 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.Keys (KeyHash, KeyRole (StakePool))
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 Control.SetAlgebra (dom, eval, setSingleton, (∩), (⊆), (▷))
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 =
  TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"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
    poolState :: ChainState era -> PState era
poolState 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 TxSeq 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
poolState 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
poolState 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
e =
  Bool -> Property
forall prop. Testable prop => prop -> Property
property (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$
    Exp Bool -> Bool
forall s t. Embed s t => Exp t -> s
eval (Set (KeyHash 'StakePool)
retire Set (KeyHash 'StakePool)
-> Exp (Sett (KeyHash 'StakePool) ()) -> Exp Bool
forall k (f :: * -> * -> *) (g :: * -> * -> *) s1 v s2 u.
(Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) =>
s1 -> s2 -> Exp Bool
⊆ Map (KeyHash 'StakePool) PoolParams
-> Exp (Sett (KeyHash 'StakePool) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom Map (KeyHash 'StakePool) PoolParams
stp)
      Bool -> Bool -> Bool
&& Set (KeyHash 'StakePool) -> Bool
forall a. Set a -> Bool
Set.null (Exp (Sett (KeyHash 'StakePool) ()) -> Set (KeyHash 'StakePool)
forall s t. Embed s t => Exp t -> s
eval (Set (KeyHash 'StakePool)
retire Set (KeyHash 'StakePool)
-> Exp (Sett (KeyHash 'StakePool) ())
-> Exp (Sett (KeyHash 'StakePool) ())
forall k (f :: * -> * -> *) (g :: * -> * -> *) s1 v s2 u.
(Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) =>
s1 -> s2 -> Exp (Sett k ())
∩ Map (KeyHash 'StakePool) PoolParams
-> Exp (Sett (KeyHash 'StakePool) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom Map (KeyHash 'StakePool) PoolParams
stp'))
      Bool -> Bool -> Bool
&& Set (KeyHash 'StakePool) -> Bool
forall a. Set a -> Bool
Set.null (Exp (Sett (KeyHash 'StakePool) ()) -> Set (KeyHash 'StakePool)
forall s t. Embed s t => Exp t -> s
eval (Set (KeyHash 'StakePool)
retire Set (KeyHash 'StakePool)
-> Exp (Sett (KeyHash 'StakePool) ())
-> Exp (Sett (KeyHash 'StakePool) ())
forall k (f :: * -> * -> *) (g :: * -> * -> *) s1 v s2 u.
(Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) =>
s1 -> s2 -> Exp (Sett k ())
∩ Map (KeyHash 'StakePool) EpochNo
-> Exp (Sett (KeyHash 'StakePool) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom Map (KeyHash 'StakePool) EpochNo
retiring'))
  where
    stp :: Map (KeyHash 'StakePool) PoolParams
stp = PState era -> Map (KeyHash 'StakePool) PoolParams
forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams PState era
p
    stp' :: Map (KeyHash 'StakePool) PoolParams
stp' = PState era -> Map (KeyHash 'StakePool) PoolParams
forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams 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.Set (KeyHash 'StakePool) -- This declaration needed to disambiguate 'eval'
    retire :: Set (KeyHash 'StakePool)
retire = Exp (Sett (KeyHash 'StakePool) ()) -> Set (KeyHash 'StakePool)
forall s t. Embed s t => Exp t -> s
eval (Exp (Map (KeyHash 'StakePool) EpochNo)
-> Exp (Sett (KeyHash 'StakePool) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom (Map (KeyHash 'StakePool) EpochNo
retiring Map (KeyHash 'StakePool) EpochNo
-> Exp (Single EpochNo ())
-> Exp (Map (KeyHash 'StakePool) EpochNo)
forall k (g :: * -> * -> *) v s1 (f :: * -> * -> *) s2.
(Ord k, Iter g, Ord v, HasExp s1 (f k v), HasExp s2 (g v ())) =>
s1 -> s2 -> Exp (f k v)
▷ EpochNo -> Exp (Single EpochNo ())
forall k. Ord k => k -> Exp (Single k ())
setSingleton EpochNo
e))

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