{-# 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.Deleg (
  tests,
)
where

import Cardano.Ledger.Coin
import Cardano.Ledger.Shelley.API (ShelleyDELEG)
import Cardano.Ledger.Shelley.Core
import qualified Cardano.Ledger.Shelley.HardForks as HardForks (allowMIRTransfer)
import Cardano.Ledger.Shelley.LedgerState (
  DState (..),
  InstantaneousRewards (..),
  delegations,
  rewards,
 )
import Cardano.Ledger.Shelley.Rules (DelegEnv (..))
import qualified Cardano.Ledger.UMap as UM
import Control.SetAlgebra (eval, rng, (∈))
import Data.Foldable (fold)
import Data.Foldable as F (foldl')
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)
import Test.Cardano.Ledger.Shelley.Rules.TestChain (
  delegTraceFromBlock,
  forAllChainTrace,
  traceLen,
 )
import Test.Cardano.Ledger.Shelley.Utils (
  ChainProperty,
 )
import Test.Control.State.Transition.Trace (
  SourceSignalTarget (..),
  sourceSignalTargets,
 )
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
  , QC.HasTrace (CHAIN era) (GenEnv era)
  , ChainProperty era
  ) =>
  TestTree
tests :: forall era.
(EraGen era, HasTrace (CHAIN era) (GenEnv era),
 ChainProperty era) =>
TestTree
tests =
  forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"properties of the DELEG 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
      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
chainProp (forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (CHAIN era)
tr)
  where
    delegProp :: DelegEnv era -> SourceSignalTarget (ShelleyDELEG era) -> Property
    delegProp :: DelegEnv era -> SourceSignalTarget (ShelleyDELEG era) -> Property
delegProp DelegEnv era
denv SourceSignalTarget (ShelleyDELEG era)
delegSst =
      forall prop. Testable prop => [prop] -> Property
conjoin
        [ forall era.
ShelleyEraTxCert era =>
SourceSignalTarget (ShelleyDELEG era) -> Property
keyRegistration SourceSignalTarget (ShelleyDELEG era)
delegSst
        , forall era.
ShelleyEraTxCert era =>
SourceSignalTarget (ShelleyDELEG era) -> Property
keyDeRegistration SourceSignalTarget (ShelleyDELEG era)
delegSst
        , forall era.
ShelleyEraTxCert era =>
SourceSignalTarget (ShelleyDELEG era) -> Property
keyDelegation SourceSignalTarget (ShelleyDELEG era)
delegSst
        , forall era. SourceSignalTarget (ShelleyDELEG era) -> Property
rewardsSumInvariant SourceSignalTarget (ShelleyDELEG era)
delegSst
        , forall era.
(EraPParams era, ShelleyEraTxCert era, ProtVerAtMost era 8) =>
DelegEnv era -> SourceSignalTarget (ShelleyDELEG era) -> Property
checkInstantaneousRewards DelegEnv era
denv SourceSignalTarget (ShelleyDELEG era)
delegSst
        ]
    chainProp :: SourceSignalTarget (CHAIN era) -> Property
    chainProp :: SourceSignalTarget (CHAIN era) -> Property
chainProp (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}) =
      let delegInfo :: (DelegEnv era, Trace (ShelleyDELEG era))
delegInfo = forall era.
(ChainProperty era, ShelleyEraTxBody era, EraSegWits era) =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (DelegEnv era, Trace (ShelleyDELEG era))
delegTraceFromBlock State (CHAIN era)
chainSt Signal (CHAIN era)
block
          delegEnv :: DelegEnv era
delegEnv = forall a b. (a, b) -> a
fst (DelegEnv era, Trace (ShelleyDELEG era))
delegInfo
          delegTr :: Trace (ShelleyDELEG era)
delegTr = forall a b. (a, b) -> b
snd (DelegEnv era, Trace (ShelleyDELEG era))
delegInfo
          delegSsts :: [SourceSignalTarget (ShelleyDELEG era)]
delegSsts = forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (ShelleyDELEG era)
delegTr
       in forall prop. Testable prop => [prop] -> Property
conjoin (forall a b. (a -> b) -> [a] -> [b]
map (DelegEnv era -> SourceSignalTarget (ShelleyDELEG era) -> Property
delegProp DelegEnv era
delegEnv) [SourceSignalTarget (ShelleyDELEG era)]
delegSsts)

-- | Check stake key registration
keyRegistration :: ShelleyEraTxCert era => SourceSignalTarget (ShelleyDELEG era) -> Property
keyRegistration :: forall era.
ShelleyEraTxCert era =>
SourceSignalTarget (ShelleyDELEG era) -> Property
keyRegistration
  SourceSignalTarget
    { signal :: forall a. SourceSignalTarget a -> Signal a
signal = RegTxCert StakeCredential
hk
    , target :: forall a. SourceSignalTarget a -> State a
target = State (ShelleyDELEG era)
targetSt
    } =
    forall prop. Testable prop => [prop] -> Property
conjoin
      [ forall prop. Testable prop => TestName -> prop -> Property
counterexample
          TestName
"a newly registered key should have a reward account"
          (forall k v. k -> UView k v -> Bool
UM.member StakeCredential
hk (forall era. DState era -> UView StakeCredential RDPair
rewards State (ShelleyDELEG era)
targetSt))
      , forall prop. Testable prop => TestName -> prop -> Property
counterexample
          TestName
"a newly registered key should have a reward account with 0 balance"
          ((RDPair -> CompactForm Coin
UM.rdReward forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k v. k -> UView k v -> Maybe v
UM.lookup StakeCredential
hk (forall era. DState era -> UView StakeCredential RDPair
rewards State (ShelleyDELEG era)
targetSt)) forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just forall a. Monoid a => a
mempty)
      ]
keyRegistration SourceSignalTarget (ShelleyDELEG era)
_ = forall prop. Testable prop => prop -> Property
property ()

-- | Check stake key de-registration
keyDeRegistration :: ShelleyEraTxCert era => SourceSignalTarget (ShelleyDELEG era) -> Property
keyDeRegistration :: forall era.
ShelleyEraTxCert era =>
SourceSignalTarget (ShelleyDELEG era) -> Property
keyDeRegistration
  SourceSignalTarget
    { signal :: forall a. SourceSignalTarget a -> Signal a
signal = UnRegTxCert StakeCredential
hk
    , target :: forall a. SourceSignalTarget a -> State a
target = State (ShelleyDELEG era)
targetSt
    } =
    forall prop. Testable prop => [prop] -> Property
conjoin
      [ forall prop. Testable prop => TestName -> prop -> Property
counterexample
          TestName
"a deregistered stake key should no longer be in the rewards mapping"
          (forall k v. k -> UView k v -> Bool
UM.notMember StakeCredential
hk (forall era. DState era -> UView StakeCredential RDPair
rewards State (ShelleyDELEG era)
targetSt))
      , forall prop. Testable prop => TestName -> prop -> Property
counterexample
          TestName
"a deregistered stake key should no longer be in the delegations mapping"
          (forall k v. k -> UView k v -> Bool
UM.notMember StakeCredential
hk (forall era.
DState era -> UView StakeCredential (KeyHash 'StakePool)
delegations State (ShelleyDELEG era)
targetSt))
      ]
keyDeRegistration SourceSignalTarget (ShelleyDELEG era)
_ = forall prop. Testable prop => prop -> Property
property ()

-- | Check stake key delegation
keyDelegation :: ShelleyEraTxCert era => SourceSignalTarget (ShelleyDELEG era) -> Property
keyDelegation :: forall era.
ShelleyEraTxCert era =>
SourceSignalTarget (ShelleyDELEG era) -> Property
keyDelegation
  SourceSignalTarget
    { signal :: forall a. SourceSignalTarget a -> Signal a
signal = DelegStakeTxCert StakeCredential
from KeyHash 'StakePool
to
    , target :: forall a. SourceSignalTarget a -> State a
target = State (ShelleyDELEG era)
targetSt
    } =
    let fromImage :: Set (KeyHash 'StakePool)
fromImage = forall s t. Embed s t => Exp t -> s
eval (forall k v s (f :: * -> * -> *).
(Ord k, Ord v, HasExp s (f k v)) =>
s -> Exp (Sett v ())
rng (forall a. a -> Set a
Set.singleton StakeCredential
from forall k v. Set k -> UView k v -> Map k v
`UM.domRestrictedMap` forall era.
DState era -> UView StakeCredential (KeyHash 'StakePool)
delegations State (ShelleyDELEG era)
targetSt))
     in forall prop. Testable prop => [prop] -> Property
conjoin
          [ forall prop. Testable prop => TestName -> prop -> Property
counterexample
              TestName
"a delegated key should have a reward account"
              (forall k v. k -> UView k v -> Bool
UM.member StakeCredential
from (forall era. DState era -> UView StakeCredential RDPair
rewards State (ShelleyDELEG era)
targetSt))
          , forall prop. Testable prop => TestName -> prop -> Property
counterexample
              TestName
"a registered stake credential should be delegated"
              (forall s t. Embed s t => Exp t -> s
eval (KeyHash 'StakePool
to forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∈ Set (KeyHash 'StakePool)
fromImage) :: Bool)
          , forall prop. Testable prop => TestName -> prop -> Property
counterexample
              TestName
"a registered stake credential should be uniquely delegated"
              (forall a. Set a -> Int
Set.size Set (KeyHash 'StakePool)
fromImage forall a. Eq a => a -> a -> Bool
== Int
1)
          ]
keyDelegation SourceSignalTarget (ShelleyDELEG era)
_ = forall prop. Testable prop => prop -> Property
property ()

-- | Check that the sum of rewards does not change and that each element
-- that is either removed or added has a zero balance.
rewardsSumInvariant :: SourceSignalTarget (ShelleyDELEG era) -> Property
rewardsSumInvariant :: forall era. SourceSignalTarget (ShelleyDELEG era) -> Property
rewardsSumInvariant
  SourceSignalTarget {State (ShelleyDELEG era)
source :: State (ShelleyDELEG era)
source :: forall a. SourceSignalTarget a -> State a
source, State (ShelleyDELEG era)
target :: State (ShelleyDELEG era)
target :: forall a. SourceSignalTarget a -> State a
target} =
    let sourceRewards :: Map StakeCredential (CompactForm Coin)
sourceRewards = UMap -> Map StakeCredential (CompactForm Coin)
UM.compactRewardMap (forall era. DState era -> UMap
dsUnified State (ShelleyDELEG era)
source)
        targetRewards :: Map StakeCredential (CompactForm Coin)
targetRewards = UMap -> Map StakeCredential (CompactForm Coin)
UM.compactRewardMap (forall era. DState era -> UMap
dsUnified State (ShelleyDELEG era)
target)
        rewardsSum :: Map StakeCredential (CompactForm Coin) -> CompactForm Coin
rewardsSum = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
F.foldl' forall a. Semigroup a => a -> a -> a
(<>) forall a. Monoid a => a
mempty
     in forall prop. Testable prop => [prop] -> Property
conjoin
          [ forall prop. Testable prop => TestName -> prop -> Property
counterexample
              TestName
"sum of rewards should not change"
              (Map StakeCredential (CompactForm Coin) -> CompactForm Coin
rewardsSum Map StakeCredential (CompactForm Coin)
sourceRewards forall a. Eq a => a -> a -> Bool
== Map StakeCredential (CompactForm Coin) -> CompactForm Coin
rewardsSum Map StakeCredential (CompactForm Coin)
targetRewards)
          , forall prop. Testable prop => TestName -> prop -> Property
counterexample
              TestName
"dropped elements have a zero reward balance"
              (forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (forall a. Eq a => a -> a -> Bool
/= Word64 -> CompactForm Coin
UM.CompactCoin Word64
0) forall a b. (a -> b) -> a -> b
$ Map StakeCredential (CompactForm Coin)
sourceRewards forall k a b. Ord k => Map k a -> Map k b -> Map k a
`Map.difference` Map StakeCredential (CompactForm Coin)
targetRewards))
          , forall prop. Testable prop => TestName -> prop -> Property
counterexample
              TestName
"added elements have a zero reward balance"
              (forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (forall a. Eq a => a -> a -> Bool
/= Word64 -> CompactForm Coin
UM.CompactCoin Word64
0) forall a b. (a -> b) -> a -> b
$ Map StakeCredential (CompactForm Coin)
targetRewards forall k a b. Ord k => Map k a -> Map k b -> Map k a
`Map.difference` Map StakeCredential (CompactForm Coin)
sourceRewards))
          ]

checkInstantaneousRewards ::
  (EraPParams era, ShelleyEraTxCert era, ProtVerAtMost era 8) =>
  DelegEnv era ->
  SourceSignalTarget (ShelleyDELEG era) ->
  Property
checkInstantaneousRewards :: forall era.
(EraPParams era, ShelleyEraTxCert era, ProtVerAtMost era 8) =>
DelegEnv era -> SourceSignalTarget (ShelleyDELEG era) -> Property
checkInstantaneousRewards
  DelegEnv era
denv
  SourceSignalTarget {State (ShelleyDELEG era)
source :: State (ShelleyDELEG era)
source :: forall a. SourceSignalTarget a -> State a
source, Signal (ShelleyDELEG era)
signal :: Signal (ShelleyDELEG era)
signal :: forall a. SourceSignalTarget a -> Signal a
signal, State (ShelleyDELEG era)
target :: State (ShelleyDELEG era)
target :: forall a. SourceSignalTarget a -> State a
target} =
    case Signal (ShelleyDELEG era)
signal of
      MirTxCert (MIRCert MIRPot
ReservesMIR (StakeAddressesMIR Map StakeCredential DeltaCoin
irwd)) ->
        forall prop. Testable prop => [prop] -> Property
conjoin
          [ forall prop. Testable prop => TestName -> prop -> Property
counterexample
              TestName
"a ReservesMIR certificate should add all entries to the `irwd` mapping"
              (forall k a. Map k a -> Set k
Map.keysSet Map StakeCredential DeltaCoin
irwd forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` forall k a. Map k a -> Set k
Map.keysSet (InstantaneousRewards -> Map StakeCredential Coin
iRReserves forall a b. (a -> b) -> a -> b
$ forall era. DState era -> InstantaneousRewards
dsIRewards State (ShelleyDELEG era)
target))
          , forall prop. Testable prop => TestName -> prop -> Property
counterexample
              TestName
"a ReservesMIR certificate should add the total value to the `irwd` map, overwriting any existing entries"
              ( if ProtVer -> Bool
HardForks.allowMIRTransfer forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a s. Getting a s a -> s -> a
view forall era. EraPParams era => Lens' (PParams era) ProtVer
ppProtocolVersionL forall a b. (a -> b) -> a -> b
$ forall era. DelegEnv era -> PParams era
ppDE DelegEnv era
denv
                  then -- In the Alonzo era, repeated fields are added
                    forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (InstantaneousRewards -> Map StakeCredential Coin
iRReserves forall a b. (a -> b) -> a -> b
$ forall era. DState era -> InstantaneousRewards
dsIRewards State (ShelleyDELEG era)
source)
                      Coin -> DeltaCoin -> Coin
`addDeltaCoin` forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map StakeCredential DeltaCoin
irwd
                      forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (InstantaneousRewards -> Map StakeCredential Coin
iRReserves forall a b. (a -> b) -> a -> b
$ forall era. DState era -> InstantaneousRewards
dsIRewards State (ShelleyDELEG era)
target)
                  else -- Prior to the Alonzo era, repeated fields overridden
                    forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (InstantaneousRewards -> Map StakeCredential Coin
iRReserves (forall era. DState era -> InstantaneousRewards
dsIRewards State (ShelleyDELEG era)
source) forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.\\ Map StakeCredential DeltaCoin
irwd)
                      Coin -> DeltaCoin -> Coin
`addDeltaCoin` forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map StakeCredential DeltaCoin
irwd
                      forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (InstantaneousRewards -> Map StakeCredential Coin
iRReserves forall a b. (a -> b) -> a -> b
$ forall era. DState era -> InstantaneousRewards
dsIRewards State (ShelleyDELEG era)
target)
              )
          ]
      MirTxCert (MIRCert MIRPot
TreasuryMIR (StakeAddressesMIR Map StakeCredential DeltaCoin
irwd)) ->
        forall prop. Testable prop => [prop] -> Property
conjoin
          [ forall prop. Testable prop => TestName -> prop -> Property
counterexample
              TestName
"a TreasuryMIR certificate should add all entries to the `irwd` mapping"
              (forall k a. Map k a -> Set k
Map.keysSet Map StakeCredential DeltaCoin
irwd forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` forall k a. Map k a -> Set k
Map.keysSet (InstantaneousRewards -> Map StakeCredential Coin
iRTreasury forall a b. (a -> b) -> a -> b
$ forall era. DState era -> InstantaneousRewards
dsIRewards State (ShelleyDELEG era)
target))
          , forall prop. Testable prop => TestName -> prop -> Property
counterexample
              TestName
"a TreasuryMIR certificate should add* the total value to the `irwd` map"
              ( if ProtVer -> Bool
HardForks.allowMIRTransfer forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a s. Getting a s a -> s -> a
view forall era. EraPParams era => Lens' (PParams era) ProtVer
ppProtocolVersionL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. DelegEnv era -> PParams era
ppDE forall a b. (a -> b) -> a -> b
$ DelegEnv era
denv
                  then -- In the Alonzo era, repeated fields are added
                    forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (InstantaneousRewards -> Map StakeCredential Coin
iRTreasury forall a b. (a -> b) -> a -> b
$ forall era. DState era -> InstantaneousRewards
dsIRewards State (ShelleyDELEG era)
source)
                      Coin -> DeltaCoin -> Coin
`addDeltaCoin` forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map StakeCredential DeltaCoin
irwd
                      forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (InstantaneousRewards -> Map StakeCredential Coin
iRTreasury forall a b. (a -> b) -> a -> b
$ forall era. DState era -> InstantaneousRewards
dsIRewards State (ShelleyDELEG era)
target)
                  else -- Prior to the Alonzo era, repeated fields overridden
                    forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (InstantaneousRewards -> Map StakeCredential Coin
iRTreasury (forall era. DState era -> InstantaneousRewards
dsIRewards State (ShelleyDELEG era)
source) forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.\\ Map StakeCredential DeltaCoin
irwd)
                      Coin -> DeltaCoin -> Coin
`addDeltaCoin` forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map StakeCredential DeltaCoin
irwd
                      forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (InstantaneousRewards -> Map StakeCredential Coin
iRTreasury forall a b. (a -> b) -> a -> b
$ forall era. DState era -> InstantaneousRewards
dsIRewards State (ShelleyDELEG era)
target)
              )
          ]
      Signal (ShelleyDELEG era)
_ -> forall prop. Testable prop => prop -> Property
property ()