-
Notifications
You must be signed in to change notification settings - Fork 155
/
PropertyTests.hs
146 lines (142 loc) · 5.59 KB
/
PropertyTests.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
136
137
138
139
140
141
142
143
144
145
146
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
module Test.Shelley.Spec.Ledger.PropertyTests (propertyTests, minimalPropertyTests) where
import Test.Shelley.Spec.Ledger.Address.Bootstrap
( bootstrapHashTest,
)
import Test.Shelley.Spec.Ledger.Rules.ClassifyTraces
( onlyValidChainSignalsAreGenerated,
onlyValidLedgerSignalsAreGenerated,
relevantCasesAreCovered,
)
import Test.Shelley.Spec.Ledger.Rules.TestChain
( adaPreservationChain,
constantSumPots,
nonNegativeDeposits,
removedAfterPoolreap,
rewardStkCredSync,
)
import Test.Shelley.Spec.Ledger.Rules.TestLedger
( consumedEqualsProduced,
credentialMappingAfterDelegation,
credentialRemovedAfterDereg,
eliminateTxInputs,
feesNonDecreasing,
newEntriesAndUniqueTxIns,
noDoubleSpend,
pStateIsInternallyConsistent,
poolIsMarkedForRetirement,
poolRetireInEpoch,
potsSumIncreaseWdrls,
preserveBalance,
preserveBalanceRestricted,
preserveOutputsTx,
prop_MIRValuesEndUpInMap,
prop_MIRentriesEndUpInMap,
registeredPoolIsAdded,
rewardZeroAfterRegKey,
rewardZeroAfterRegPool,
rewardsDecreasesByWithdrawals,
rewardsSumInvariant,
)
import Test.Tasty (TestTree, testGroup)
import qualified Test.Tasty.QuickCheck as TQC
minimalPropertyTests :: TestTree
minimalPropertyTests =
testGroup
"Minimal Property Tests"
[ TQC.testProperty "Chain and Ledger traces cover the relevant cases" relevantCasesAreCovered,
TQC.testProperty "total amount of Ada is preserved (Chain)" adaPreservationChain,
TQC.testProperty "reward and stake credential maps stay in sync" rewardStkCredSync,
TQC.testProperty "Only valid CHAIN STS signals are generated" onlyValidChainSignalsAreGenerated,
bootstrapHashTest
]
-- | 'TestTree' of property-based testing properties.
propertyTests :: TestTree
propertyTests =
testGroup
"Property-Based Testing"
[ testGroup
"Classify Traces"
[TQC.testProperty "Chain and Ledger traces cover the relevant cases" relevantCasesAreCovered],
testGroup
"STS Rules - Delegation Properties"
[ TQC.testProperty "newly registered key has a reward of 0" rewardZeroAfterRegKey,
TQC.testProperty "deregistered key's credential is removed" credentialRemovedAfterDereg,
TQC.testProperty "registered stake credential is correctly delegated" credentialMappingAfterDelegation,
TQC.testProperty "sum of rewards does not change" rewardsSumInvariant,
TQC.testProperty "rewards pot decreases by the sum of tx withdrawals" rewardsDecreasesByWithdrawals
],
testGroup
"STS Rules - Utxo Properties"
[ TQC.testProperty "the value consumed by UTXO is equal to the value produced in DELEGS" consumedEqualsProduced,
TQC.testProperty "transaction fees are non-decreasing" feesNonDecreasing,
TQC.testProperty "sum of circulation, deposits and fees increases by the sum of tx withdrawals" potsSumIncreaseWdrls,
TQC.testProperty "preserve the balance in a transaction" preserveBalance,
TQC.testProperty "preserve tx balance restricted to TxIns and TxOuts" preserveBalanceRestricted,
TQC.testProperty "preserve transaction outputs" preserveOutputsTx,
TQC.testProperty "consumed inputs are eliminated" eliminateTxInputs,
TQC.testProperty "new tx entries are included and all txIds are new" newEntriesAndUniqueTxIns,
TQC.testProperty "no double spend" noDoubleSpend
],
testGroup
"STS Rules - Pool Properties"
[ TQC.testProperty
"newly registered stake pool is added to \
\appropriate state mappings"
registeredPoolIsAdded,
TQC.testProperty
"newly registered pool key is not in the retiring map"
rewardZeroAfterRegPool,
TQC.testProperty
"retired stake pool is removed from \
\appropriate state mappings and marked \
\ for retiring"
poolIsMarkedForRetirement,
TQC.testProperty
"pool state is internally consistent"
pStateIsInternallyConsistent,
TQC.testProperty
"executing a pool retirement certificate adds to 'retiring'"
poolRetireInEpoch
],
testGroup
"STS Rules - Poolreap Properties"
[ TQC.testProperty
"circulation+deposits+fees+treasury+rewards+reserves is constant."
constantSumPots,
TQC.testProperty
"deposits are always non-negative"
nonNegativeDeposits,
TQC.testProperty
"pool is removed from stake pool and retiring maps"
removedAfterPoolreap
],
testGroup
"STS Rules - NewEpoch Properties"
[ TQC.testProperty
"total amount of Ada is preserved"
adaPreservationChain
],
testGroup
"STS Rules - MIR certificates"
[ TQC.testProperty
"entries of MIR certificate are added to\
\ irwd mapping"
prop_MIRentriesEndUpInMap,
TQC.testProperty
"coin values of entries of a MIR certificate\
\ are added to the irwd mapping"
prop_MIRValuesEndUpInMap
],
testGroup
"Properties of Trace generators"
[ TQC.testProperty
"Only valid LEDGER STS signals are generated"
onlyValidLedgerSignalsAreGenerated,
TQC.testProperty
"Only valid CHAIN STS signals are generated"
onlyValidChainSignalsAreGenerated
]
]