{-# 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)
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 (EraCrypto era)) 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)
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 (EraCrypto era)
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 c v. k -> UView c k v -> Bool
UM.member StakeCredential (EraCrypto era)
hk (forall era.
DState era
-> UView
(EraCrypto era) (Credential 'Staking (EraCrypto era)) 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 c v. k -> UView c k v -> Maybe v
UM.lookup StakeCredential (EraCrypto era)
hk (forall era.
DState era
-> UView
(EraCrypto era) (Credential 'Staking (EraCrypto era)) 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 ()
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 (EraCrypto era)
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 c v. k -> UView c k v -> Bool
UM.notMember StakeCredential (EraCrypto era)
hk (forall era.
DState era
-> UView
(EraCrypto era) (Credential 'Staking (EraCrypto era)) 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 c v. k -> UView c k v -> Bool
UM.notMember StakeCredential (EraCrypto era)
hk (forall era.
DState era
-> UView
(EraCrypto era)
(Credential 'Staking (EraCrypto era))
(KeyHash 'StakePool (EraCrypto era))
delegations State (ShelleyDELEG era)
targetSt))
]
keyDeRegistration SourceSignalTarget (ShelleyDELEG era)
_ = forall prop. Testable prop => prop -> Property
property ()
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 Credential 'Staking (EraCrypto era)
from KeyHash 'StakePool (EraCrypto era)
to
, target :: forall a. SourceSignalTarget a -> State a
target = State (ShelleyDELEG era)
targetSt
} =
let fromImage :: Set (KeyHash 'StakePool (EraCrypto era))
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 Credential 'Staking (EraCrypto era)
from forall k c v. Set k -> UView c k v -> Map k v
`UM.domRestrictedMap` forall era.
DState era
-> UView
(EraCrypto era)
(Credential 'Staking (EraCrypto era))
(KeyHash 'StakePool (EraCrypto era))
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 c v. k -> UView c k v -> Bool
UM.member Credential 'Staking (EraCrypto era)
from (forall era.
DState era
-> UView
(EraCrypto era) (Credential 'Staking (EraCrypto era)) 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 (EraCrypto era)
to forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∈ Set (KeyHash 'StakePool (EraCrypto era))
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 (EraCrypto era))
fromImage forall a. Eq a => a -> a -> Bool
== Int
1)
]
keyDelegation SourceSignalTarget (ShelleyDELEG era)
_ = forall prop. Testable prop => prop -> Property
property ()
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 (Credential 'Staking (EraCrypto era)) (CompactForm Coin)
sourceRewards = forall c. UMap c -> Map (Credential 'Staking c) (CompactForm Coin)
UM.compactRewardMap (forall era. DState era -> UMap (EraCrypto era)
dsUnified State (ShelleyDELEG era)
source)
targetRewards :: Map (Credential 'Staking (EraCrypto era)) (CompactForm Coin)
targetRewards = forall c. UMap c -> Map (Credential 'Staking c) (CompactForm Coin)
UM.compactRewardMap (forall era. DState era -> UMap (EraCrypto era)
dsUnified State (ShelleyDELEG era)
target)
rewardsSum :: Map (Credential 'Staking (EraCrypto era)) (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 (Credential 'Staking (EraCrypto era)) (CompactForm Coin)
-> CompactForm Coin
rewardsSum Map (Credential 'Staking (EraCrypto era)) (CompactForm Coin)
sourceRewards forall a. Eq a => a -> a -> Bool
== Map (Credential 'Staking (EraCrypto era)) (CompactForm Coin)
-> CompactForm Coin
rewardsSum Map (Credential 'Staking (EraCrypto era)) (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 (Credential 'Staking (EraCrypto era)) (CompactForm Coin)
sourceRewards forall k a b. Ord k => Map k a -> Map k b -> Map k a
`Map.difference` Map (Credential 'Staking (EraCrypto era)) (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 (Credential 'Staking (EraCrypto era)) (CompactForm Coin)
targetRewards forall k a b. Ord k => Map k a -> Map k b -> Map k a
`Map.difference` Map (Credential 'Staking (EraCrypto era)) (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 (Credential 'Staking (EraCrypto era)) 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 (Credential 'Staking (EraCrypto era)) DeltaCoin
irwd forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` forall k a. Map k a -> Set k
Map.keysSet (forall c.
InstantaneousRewards c -> Map (Credential 'Staking c) Coin
iRReserves forall a b. (a -> b) -> a -> b
$ forall era. DState era -> InstantaneousRewards (EraCrypto era)
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
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (forall c.
InstantaneousRewards c -> Map (Credential 'Staking c) Coin
iRReserves forall a b. (a -> b) -> a -> b
$ forall era. DState era -> InstantaneousRewards (EraCrypto era)
dsIRewards State (ShelleyDELEG era)
source)
Coin -> DeltaCoin -> Coin
`addDeltaCoin` forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (Credential 'Staking (EraCrypto era)) DeltaCoin
irwd
forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (forall c.
InstantaneousRewards c -> Map (Credential 'Staking c) Coin
iRReserves forall a b. (a -> b) -> a -> b
$ forall era. DState era -> InstantaneousRewards (EraCrypto era)
dsIRewards State (ShelleyDELEG era)
target)
else
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (forall c.
InstantaneousRewards c -> Map (Credential 'Staking c) Coin
iRReserves (forall era. DState era -> InstantaneousRewards (EraCrypto era)
dsIRewards State (ShelleyDELEG era)
source) forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.\\ Map (Credential 'Staking (EraCrypto era)) DeltaCoin
irwd)
Coin -> DeltaCoin -> Coin
`addDeltaCoin` forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (Credential 'Staking (EraCrypto era)) DeltaCoin
irwd
forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (forall c.
InstantaneousRewards c -> Map (Credential 'Staking c) Coin
iRReserves forall a b. (a -> b) -> a -> b
$ forall era. DState era -> InstantaneousRewards (EraCrypto era)
dsIRewards State (ShelleyDELEG era)
target)
)
]
MirTxCert (MIRCert MIRPot
TreasuryMIR (StakeAddressesMIR Map (Credential 'Staking (EraCrypto era)) 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 (Credential 'Staking (EraCrypto era)) DeltaCoin
irwd forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` forall k a. Map k a -> Set k
Map.keysSet (forall c.
InstantaneousRewards c -> Map (Credential 'Staking c) Coin
iRTreasury forall a b. (a -> b) -> a -> b
$ forall era. DState era -> InstantaneousRewards (EraCrypto era)
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
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (forall c.
InstantaneousRewards c -> Map (Credential 'Staking c) Coin
iRTreasury forall a b. (a -> b) -> a -> b
$ forall era. DState era -> InstantaneousRewards (EraCrypto era)
dsIRewards State (ShelleyDELEG era)
source)
Coin -> DeltaCoin -> Coin
`addDeltaCoin` forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (Credential 'Staking (EraCrypto era)) DeltaCoin
irwd
forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (forall c.
InstantaneousRewards c -> Map (Credential 'Staking c) Coin
iRTreasury forall a b. (a -> b) -> a -> b
$ forall era. DState era -> InstantaneousRewards (EraCrypto era)
dsIRewards State (ShelleyDELEG era)
target)
else
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (forall c.
InstantaneousRewards c -> Map (Credential 'Staking c) Coin
iRTreasury (forall era. DState era -> InstantaneousRewards (EraCrypto era)
dsIRewards State (ShelleyDELEG era)
source) forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.\\ Map (Credential 'Staking (EraCrypto era)) DeltaCoin
irwd)
Coin -> DeltaCoin -> Coin
`addDeltaCoin` forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (Credential 'Staking (EraCrypto era)) DeltaCoin
irwd
forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (forall c.
InstantaneousRewards c -> Map (Credential 'Staking c) Coin
iRTreasury forall a b. (a -> b) -> a -> b
$ forall era. DState era -> InstantaneousRewards (EraCrypto era)
dsIRewards State (ShelleyDELEG era)
target)
)
]
Signal (ShelleyDELEG era)
_ -> forall prop. Testable prop => prop -> Property
property ()