Skip to content

Commit 1164efa

Browse files
agustinmistanbacqueytbagrel1
committed
Implement state-machine tests for PerasVoteDB
This commit implements state-machine tests for the PerasVoteDB using quickcheck-dynamic. Notably, we define rather constrained generators to increase the chances of (among others): * Voting for the same target more than once (normal behavior), * Voting more than once per round (PerasVoteAlreadyInDB), * Two voting targets becoming winners (MultipleWinnersInRound) Co-authored-by: Nicolas BACQUEY <[email protected]> Co-authored-by: Thomas BAGREL <[email protected]> Co-authored-by: Agustin Mista <[email protected]>
1 parent f937cb5 commit 1164efa

File tree

7 files changed

+608
-1
lines changed

7 files changed

+608
-1
lines changed

‎ouroboros-consensus/ouroboros-consensus.cabal‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -804,6 +804,9 @@ test-suite storage-test
804804
Test.Ouroboros.Storage.PerasCertDB
805805
Test.Ouroboros.Storage.PerasCertDB.Model
806806
Test.Ouroboros.Storage.PerasCertDB.StateMachine
807+
Test.Ouroboros.Storage.PerasVoteDB
808+
Test.Ouroboros.Storage.PerasVoteDB.Model
809+
Test.Ouroboros.Storage.PerasVoteDB.StateMachine
807810
Test.Ouroboros.Storage.VolatileDB
808811
Test.Ouroboros.Storage.VolatileDB.Mock
809812
Test.Ouroboros.Storage.VolatileDB.Model
@@ -816,6 +819,7 @@ test-suite storage-test
816819
bifunctors,
817820
bytestring,
818821
cardano-binary,
822+
cardano-crypto-class,
819823
cardano-ledger-binary:testlib,
820824
cardano-ledger-core:{cardano-ledger-core, testlib},
821825
cardano-slotting:{cardano-slotting, testlib},

‎ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Storage/PerasVoteDB/API.hs‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@
44
{-# LANGUAGE DerivingVia #-}
55
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
66
{-# LANGUAGE ScopedTypeVariables #-}
7+
{-# LANGUAGE UndecidableInstances #-}
78

89
module Ouroboros.Consensus.Storage.PerasVoteDB.API
910
( PerasVoteDB (..)
@@ -55,7 +56,7 @@ data PerasVoteSnapshot blk = PerasVoteSnapshot
5556

5657
-- | A sequence number, incremented every time we receive a new vote.
5758
newtype PerasVoteTicketNo = PerasVoteTicketNo Word64
58-
deriving stock Show
59+
deriving stock (Generic, Show)
5960
deriving newtype (Eq, Ord, Enum, NoThunks)
6061

6162
zeroPerasVoteTicketNo :: PerasVoteTicketNo

‎ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage.hs‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ import qualified Test.Ouroboros.Storage.ChainDB as ChainDB
66
import qualified Test.Ouroboros.Storage.ImmutableDB as ImmutableDB
77
import qualified Test.Ouroboros.Storage.LedgerDB as LedgerDB
88
import qualified Test.Ouroboros.Storage.PerasCertDB as PerasCertDB
9+
import qualified Test.Ouroboros.Storage.PerasVoteDB as PerasVoteDB
910
import qualified Test.Ouroboros.Storage.VolatileDB as VolatileDB
1011
import Test.Tasty (TestTree, testGroup)
1112

@@ -22,4 +23,5 @@ tests =
2223
, LedgerDB.tests
2324
, ChainDB.tests
2425
, PerasCertDB.tests
26+
, PerasVoteDB.tests
2527
]

‎ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/Orphans.hs‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
{-# LANGUAGE FlexibleInstances #-}
12
{-# LANGUAGE StandaloneDeriving #-}
23
{-# OPTIONS_GHC -Wno-orphans #-}
34

@@ -19,6 +20,7 @@ import Ouroboros.Consensus.Util.CallStack
1920
import System.FS.API.Types (FsError, sameFsError)
2021
import Test.QuickCheck.StateModel (HasVariables)
2122
import Test.QuickCheck.StateModel.Variables (HasVariables (..))
23+
import Cardano.Crypto.Hash.Class (PackedBytes)
2224

2325
{-------------------------------------------------------------------------------
2426
PrettyCallStack
@@ -76,3 +78,17 @@ deriving instance StandardHash blk => Eq (ChainDbError blk)
7678

7779
instance HasVariables NominalDiffTime where
7880
getAllVariables _ = mempty
81+
82+
{-------------------------------------------------------------------------------
83+
Rational
84+
-------------------------------------------------------------------------------}
85+
86+
instance HasVariables Rational where
87+
getAllVariables _ = mempty
88+
89+
{-------------------------------------------------------------------------------
90+
PackedBytes
91+
-------------------------------------------------------------------------------}
92+
93+
instance HasVariables (PackedBytes a) where
94+
getAllVariables _ = mempty

‎ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/PerasVoteDB.hs‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
module Test.Ouroboros.Storage.PerasVoteDB (tests) where
2+
3+
import qualified Test.Ouroboros.Storage.PerasVoteDB.StateMachine as StateMachine
4+
import Test.Tasty (TestTree, testGroup)
5+
6+
--
7+
-- The list of all PerasVoteDB tests
8+
--
9+
10+
tests :: TestTree
11+
tests =
12+
testGroup
13+
"PerasVoteDB"
14+
[ StateMachine.tests
15+
]

‎ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/PerasVoteDB/Model.hs‎

Lines changed: 237 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,237 @@
1+
{-# LANGUAGE DeriveGeneric #-}
2+
3+
module Test.Ouroboros.Storage.PerasVoteDB.Model
4+
( Model (..)
5+
, initModel
6+
, hasVote
7+
, openDB
8+
, closeDB
9+
, addVote
10+
, getVoteSnapshot
11+
, getForgedCertForRound
12+
, garbageCollect
13+
) where
14+
15+
import Data.Map.Strict (Map)
16+
import qualified Data.Map.Strict as Map
17+
import Data.Set (Set)
18+
import qualified Data.Set as Set
19+
import GHC.Generics (Generic)
20+
import Ouroboros.Consensus.Block.Abstract (Point, StandardHash)
21+
import Ouroboros.Consensus.Block.SupportsPeras
22+
( HasPerasVoteBlock (..)
23+
, HasPerasVoteRound (..)
24+
, PerasCert (..)
25+
, PerasCfg
26+
, PerasParams (..)
27+
, PerasQuorumStakeThreshold (unPerasQuorumStakeThreshold)
28+
, PerasRoundNo
29+
, PerasVoteId (..)
30+
, PerasVoteStake (..)
31+
, PerasVoterId
32+
, ValidatedPerasCert (..)
33+
, ValidatedPerasVote
34+
, getPerasCertBoostedBlock
35+
, getPerasVoteStake
36+
, getPerasVoteVoterId
37+
)
38+
import Ouroboros.Consensus.BlockchainTime.WallClock.Types
39+
( WithArrivalTime (..)
40+
)
41+
import Ouroboros.Consensus.Storage.PerasVoteDB.API
42+
( AddPerasVoteResult (..)
43+
, PerasVoteSnapshot (..)
44+
, PerasVoteTicketNo
45+
, zeroPerasVoteTicketNo
46+
)
47+
48+
data Model blk = Model
49+
{ open :: Bool
50+
, params :: PerasParams
51+
, lastTicketNo :: PerasVoteTicketNo
52+
, votes ::
53+
Map
54+
(PerasRoundNo, Point blk)
55+
(Set (WithArrivalTime (ValidatedPerasVote blk), PerasVoteTicketNo))
56+
, voteIds ::
57+
Set (PerasRoundNo, PerasVoterId)
58+
, certs ::
59+
Map
60+
PerasRoundNo
61+
(ValidatedPerasCert blk)
62+
}
63+
deriving (Show, Generic)
64+
65+
initModel :: PerasCfg blk -> Model blk
66+
initModel cfg =
67+
Model
68+
{ open = False
69+
, params = cfg
70+
, lastTicketNo = zeroPerasVoteTicketNo
71+
, votes = Map.empty
72+
, voteIds = Set.empty
73+
, certs = Map.empty
74+
}
75+
76+
hasVote ::
77+
StandardHash blk =>
78+
Model blk ->
79+
WithArrivalTime (ValidatedPerasVote blk) ->
80+
Bool
81+
hasVote model vote =
82+
Set.member vote (Set.map fst existingVotes)
83+
where
84+
roundNo = getPerasVoteRound vote
85+
votedBlock = getPerasVoteBlock vote
86+
existingVotes = Map.findWithDefault Set.empty (roundNo, votedBlock) (votes model)
87+
88+
openDB ::
89+
Model blk ->
90+
Model blk
91+
openDB model =
92+
model
93+
{ open = True
94+
}
95+
96+
closeDB ::
97+
Model blk ->
98+
Model blk
99+
closeDB model =
100+
model
101+
{ open = False
102+
, lastTicketNo = zeroPerasVoteTicketNo
103+
, votes = Map.empty
104+
, voteIds = Set.empty
105+
, certs = Map.empty
106+
}
107+
108+
addVote ::
109+
StandardHash blk =>
110+
WithArrivalTime (ValidatedPerasVote blk) ->
111+
Model blk ->
112+
( Maybe (AddPerasVoteResult blk)
113+
, Model blk
114+
)
115+
addVote vote model
116+
-- This voter has already voted in this round => ignore the vote
117+
| voterAlreadyVotedInRound =
118+
( Just $
119+
PerasVoteAlreadyInDB
120+
, model
121+
)
122+
-- A quorum was reached, but there is another cert already boosting a different
123+
-- block in this round => integrity violation (shouldn't happen in practice)
124+
| reachedQuorum
125+
, Just existingCert <- certAtRound
126+
, getPerasCertBoostedBlock freshCert /= getPerasCertBoostedBlock existingCert =
127+
( Nothing -- Cannot have multiple certs for the same round
128+
, model
129+
)
130+
-- A quorum was reached for the first time (when there is no existing
131+
-- certificate for the given round) => causing a new cert to be generated
132+
| reachedQuorum
133+
, Nothing <- certAtRound =
134+
( Just $
135+
AddedPerasVoteAndGeneratedNewCert freshCert
136+
, model
137+
{ votes =
138+
Map.insert (roundNo, votedBlock) extendedVotes (votes model)
139+
, voteIds =
140+
Set.insert (roundNo, voter) (voteIds model)
141+
, certs =
142+
Map.insert roundNo freshCert (certs model)
143+
, lastTicketNo =
144+
nextTicketNo
145+
}
146+
)
147+
-- Otherwise, just add the vote without generating a new cert
148+
| otherwise =
149+
( Just $
150+
AddedPerasVoteButDidntGenerateNewCert
151+
, model
152+
{ votes =
153+
Map.insert (roundNo, votedBlock) extendedVotes (votes model)
154+
, voteIds =
155+
Set.insert (roundNo, voter) (voteIds model)
156+
, lastTicketNo =
157+
nextTicketNo
158+
}
159+
)
160+
where
161+
roundNo =
162+
getPerasVoteRound vote
163+
votedBlock =
164+
getPerasVoteBlock vote
165+
voter =
166+
getPerasVoteVoterId vote
167+
nextTicketNo =
168+
succ (lastTicketNo model)
169+
voterAlreadyVotedInRound =
170+
Set.member (roundNo, voter) (voteIds model)
171+
existingVotes =
172+
Map.findWithDefault Set.empty (roundNo, votedBlock) (votes model)
173+
extendedVotes =
174+
Set.insert (vote, nextTicketNo) existingVotes
175+
quorumStakeThreshold =
176+
unPerasQuorumStakeThreshold . perasQuorumStakeThreshold . params
177+
getVoteStake =
178+
unPerasVoteStake . getPerasVoteStake . forgetArrivalTime
179+
reachedQuorum =
180+
sum (getVoteStake . fst <$> Set.toList extendedVotes)
181+
>= quorumStakeThreshold model
182+
certAtRound =
183+
Map.lookup roundNo (certs model)
184+
freshCert =
185+
ValidatedPerasCert
186+
{ vpcCert =
187+
PerasCert
188+
{ pcCertRound = getPerasVoteRound vote
189+
, pcCertBoostedBlock = getPerasVoteBlock vote
190+
}
191+
, vpcCertBoost = perasWeight (params model)
192+
}
193+
194+
getVoteSnapshot ::
195+
Model blk ->
196+
PerasVoteSnapshot blk
197+
getVoteSnapshot model =
198+
PerasVoteSnapshot
199+
{ containsVote = \voteId ->
200+
Set.member
201+
(pviRoundNo voteId, pviVoterId voteId)
202+
(voteIds model)
203+
, getVotesAfter = \ticketNo ->
204+
Map.fromList
205+
[ (tn, vote)
206+
| (_, vs) <- Map.toList (votes model)
207+
, (vote, tn) <- Set.toList vs
208+
, tn > ticketNo
209+
]
210+
}
211+
212+
getForgedCertForRound ::
213+
PerasRoundNo ->
214+
Model blk ->
215+
Maybe (ValidatedPerasCert blk)
216+
getForgedCertForRound roundNo model =
217+
Map.lookup roundNo (certs model)
218+
219+
garbageCollect ::
220+
PerasRoundNo ->
221+
Model blk ->
222+
Model blk
223+
garbageCollect roundNo model =
224+
model
225+
{ votes =
226+
Map.filterWithKey
227+
(\(r, _) _ -> r >= roundNo)
228+
(votes model)
229+
, voteIds =
230+
Set.filter
231+
(\(r, _) -> r >= roundNo)
232+
(voteIds model)
233+
, certs =
234+
Map.filterWithKey
235+
(\r _ -> r >= roundNo)
236+
(certs model)
237+
}

0 commit comments

Comments
 (0)