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

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

import Test.Cardano.Ledger.Shelley.Rules.TestChain (
  chainSstWithTick,
  forAllChainTrace,
  traceLen,
 )

import Cardano.Ledger.Block (
  Block (..),
 )
import Cardano.Ledger.Keys (KeyHash, KeyRole (StakePool))
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.LedgerState (
  CertState (..),
  EpochState (..),
  LedgerState (..),
  NewEpochState (..),
  PState (..),
  psStakePoolParams,
 )
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 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.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.
  ( ChainProperty era
  , EraGen era
  , QC.HasTrace (CHAIN era) (GenEnv era)
  ) =>
  TestTree
tests :: forall era.
(ChainProperty era, EraGen era,
 HasTrace (CHAIN era) (GenEnv era)) =>
TestTree
tests =
  forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"pool is removed from stake pool and retiring maps" 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 Word64
traceLen Constants
defaultConstants forall a b. (a -> b) -> a -> b
$ \Trace (CHAIN era)
tr ->
      forall prop. Testable prop => [prop] -> Property
conjoin forall a b. (a -> b) -> a -> b
$
        forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget (CHAIN era) -> Property
removedAfterPoolreap_ forall a b. (a -> b) -> a -> b
$
          forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. SourceSignalTarget (CHAIN era) -> Bool
sameEpoch) (forall era.
ChainProperty era =>
Trace (CHAIN era) -> [SourceSignalTarget (CHAIN era)]
chainSstWithTick Trace (CHAIN era)
tr)
  where
    poolState :: ChainState era -> PState era
poolState = forall era. CertState era -> PState era
certPState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. LedgerState era -> CertState era
lsCertState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EpochState era -> LedgerState era
esLState 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

    removedAfterPoolreap_ :: SourceSignalTarget (CHAIN era) -> Property
    removedAfterPoolreap_ :: SourceSignalTarget (CHAIN era) -> Property
removedAfterPoolreap_ (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, signal :: forall a. SourceSignalTarget a -> Signal a
signal = (UnserialisedBlock BHeader (EraCrypto era)
bh TxSeq era
_)}) =
      let e :: EpochNo
e = (SlotNo -> EpochNo
epochFromSlotNo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c. BHBody c -> SlotNo
bheaderSlotNo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c. Crypto c => BHeader c -> BHBody c
bhbody) BHeader (EraCrypto era)
bh
       in forall era. PState era -> PState era -> EpochNo -> Property
removedAfterPoolreap (forall {era}. ChainState era -> PState era
poolState State (CHAIN era)
source) (forall {era}. ChainState era -> PState era
poolState State (CHAIN 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 =
  forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$
    forall s t. Embed s t => Exp t -> s
eval (Set (KeyHash 'StakePool (EraCrypto era))
retire 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
⊆ forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
stp)
      Bool -> Bool -> Bool
&& forall a. Set a -> Bool
Set.null (forall s t. Embed s t => Exp t -> s
eval (Set (KeyHash 'StakePool (EraCrypto era))
retire 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 ())
∩ forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
stp'))
      Bool -> Bool -> Bool
&& forall a. Set a -> Bool
Set.null (forall s t. Embed s t => Exp t -> s
eval (Set (KeyHash 'StakePool (EraCrypto era))
retire 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 ())
∩ forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom Map (KeyHash 'StakePool (EraCrypto era)) EpochNo
retiring'))
  where
    stp :: Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
stp = forall era.
PState era
-> Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
psStakePoolParams PState era
p
    stp' :: Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
stp' = forall era.
PState era
-> Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
psStakePoolParams PState era
p'
    retiring :: Map (KeyHash 'StakePool (EraCrypto era)) EpochNo
retiring = forall era.
PState era -> Map (KeyHash 'StakePool (EraCrypto era)) EpochNo
psRetiring PState era
p
    retiring' :: Map (KeyHash 'StakePool (EraCrypto era)) EpochNo
retiring' = forall era.
PState era -> Map (KeyHash 'StakePool (EraCrypto era)) EpochNo
psRetiring PState era
p'
    retire :: Set.Set (KeyHash 'StakePool (EraCrypto era)) -- This declaration needed to disambiguate 'eval'
    retire :: Set (KeyHash 'StakePool (EraCrypto era))
retire = forall s t. Embed s t => Exp t -> s
eval (forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom (Map (KeyHash 'StakePool (EraCrypto era)) EpochNo
retiring 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)
▷ 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 :: 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} =
  forall {era}. ChainState era -> EpochNo
epoch State (CHAIN era)
source forall a. Eq a => a -> a -> Bool
== forall {era}. ChainState era -> EpochNo
epoch State (CHAIN era)
target
  where
    epoch :: ChainState era -> EpochNo
epoch = forall era. NewEpochState era -> EpochNo
nesEL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. ChainState era -> NewEpochState era
chainNes