-
Notifications
You must be signed in to change notification settings - Fork 155
/
TestDeleg.hs
135 lines (114 loc) · 4.84 KB
/
TestDeleg.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeSynonymInstances #-}
module Rules.TestDeleg
( credentialMappingAfterDelegation
, credentialRemovedAfterDereg
, rewardZeroAfterReg
, rewardsSumInvariant
)
where
import Data.Map (Map)
import qualified Data.Map.Strict as Map (difference, filter, lookup)
import qualified Data.Maybe as Maybe (maybe)
import Data.Set (Set)
import qualified Data.Set as Set (singleton, size)
import Data.Word (Word64)
import Hedgehog (MonadTest, Property, TestLimit, forAll, property, withTests)
import Address (mkRwdAcnt)
import BaseTypes ((==>))
import Control.State.Transition.Generator (ofLengthAtLeast, trace)
import Control.State.Transition.Trace (SourceSignalTarget, pattern SourceSignalTarget,
signal, source, sourceSignalTargets, target)
import Generator.LedgerTrace ()
import Ledger.Core (dom, range, (∈), (∉), (◁))
import Coin (Coin, pattern Coin)
import LedgerState (_delegations, _rewards, _stKeys)
import MockTypes (DELEG, DState, KeyHash, RewardAcnt, StakeCredential)
import Test.Utils (assertAll)
import TxData (pattern DeRegKey, pattern Delegate, pattern Delegation, pattern RegKey)
-------------------------------
-- helper accessor functions --
-------------------------------
getStDelegs :: DState -> Set StakeCredential
getStDelegs = dom . _stKeys
getRewards :: DState -> Map RewardAcnt Coin
getRewards = _rewards
getDelegations :: DState -> Map StakeCredential KeyHash
getDelegations = _delegations
------------------------------
-- Constants for Properties --
------------------------------
numberOfTests :: TestLimit
numberOfTests = 300
traceLen :: Word64
traceLen = 100
--------------------------
-- Properties for DELEG --
--------------------------
-- | Check that a newly registered key has a reward of 0.
rewardZeroAfterReg
:: MonadTest m
=> [SourceSignalTarget DELEG]
-> m ()
rewardZeroAfterReg tr =
assertAll credNewlyRegisteredAndRewardZero tr
where credNewlyRegisteredAndRewardZero (SourceSignalTarget d d' (RegKey hk)) =
(hk ∉ getStDelegs d) ==>
(hk ∈ getStDelegs d'
&& Maybe.maybe True (== 0) (Map.lookup (mkRwdAcnt hk) (getRewards d')))
credNewlyRegisteredAndRewardZero _ = True
-- | Check that when a stake credential is deregistered, it will not be in the
-- rewards mapping or delegation mapping of the target state.
credentialRemovedAfterDereg :: Property
credentialRemovedAfterDereg = withTests numberOfTests . property $ do
tr <- fmap sourceSignalTargets
$ forAll
$ trace @DELEG traceLen `ofLengthAtLeast` 1
assertAll removedDeregCredential tr
where removedDeregCredential (SourceSignalTarget
{ signal = DeRegKey cred
, target = d'}) =
cred ∉ getStDelegs d'
&& mkRwdAcnt cred ∉ dom (getRewards d')
&& cred ∉ dom (getDelegations d')
removedDeregCredential _ = True
-- |Check that a registered stake credential get correctly delegated when
-- applying a delegation certificate.
credentialMappingAfterDelegation :: Property
credentialMappingAfterDelegation = withTests (fromIntegral numberOfTests) . property $ do
tr <- fmap sourceSignalTargets
$ forAll
$ trace @DELEG traceLen `ofLengthAtLeast` 1
assertAll delegatedCredential tr
where delegatedCredential (SourceSignalTarget
{ signal = Delegate (Delegation cred to)
, target = d'}) =
let credImage = range (Set.singleton cred ◁ getDelegations d') in
cred ∈ getStDelegs d'
&& to ∈ credImage
&& Set.size credImage == 1
delegatedCredential _ = True
-- | Check that the sum of rewards does not change and that each element that is
-- either removed or added has a zero balance.
rewardsSumInvariant :: Property
rewardsSumInvariant = withTests (fromIntegral numberOfTests) . property $ do
tr <- fmap sourceSignalTargets
$ forAll
$ trace @DELEG traceLen `ofLengthAtLeast` 1
assertAll rewardsSumZeroDiff tr
where rewardsSumZeroDiff (SourceSignalTarget
{ source = d
, target = d'}) =
let rew = _rewards d
rew' = _rewards d'
sumRew = foldl (+) (Coin 0)
in
-- sum of rewards is not changed
sumRew rew == sumRew rew'
&& -- dropped elements had a zero reward balance
null (Map.filter (/= Coin 0) $ rew `Map.difference` rew')
&& -- added elements have a zero reward balance
null (Map.filter (/= Coin 0) $ rew' `Map.difference` rew)