[Peras 15] State-machine tests for PerasVoteDB

ouroboros-consensus/changelog.d/20251231_104054_agustin.mista_vote_db_tests.md

@@ -0,0 +1,23 @@
+<!--
+A new scriv changelog fragment.
+
+Uncomment the section that is right (remove the HTML comment wrapper).
+For top level release notes, leave all the headers commented out.
+-->
+
+<!--
+### Patch
+
+- A bullet item for the Patch category.
+
+-->
+### Non-Breaking
+
+- Add state machine tests for PerasVoteDB using quickcheck-dynamic.
+
+<!--
+### Breaking
+
+- A bullet item for the Breaking category.
+
+-->

ouroboros-consensus/ouroboros-consensus.cabal

@@ -804,6 +804,9 @@ test-suite storage-test
     Test.Ouroboros.Storage.PerasCertDB
     Test.Ouroboros.Storage.PerasCertDB.Model
     Test.Ouroboros.Storage.PerasCertDB.StateMachine
+    Test.Ouroboros.Storage.PerasVoteDB
+    Test.Ouroboros.Storage.PerasVoteDB.Model
+    Test.Ouroboros.Storage.PerasVoteDB.StateMachine
     Test.Ouroboros.Storage.VolatileDB
     Test.Ouroboros.Storage.VolatileDB.Mock
     Test.Ouroboros.Storage.VolatileDB.Model
@@ -816,6 +819,7 @@ test-suite storage-test
     bifunctors,
     bytestring,
     cardano-binary,
+    cardano-crypto-class,
     cardano-ledger-binary:testlib,
     cardano-ledger-core:{cardano-ledger-core, testlib},
     cardano-slotting:{cardano-slotting, testlib},

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

@@ -55,7 +55,7 @@ data PerasVoteSnapshot blk = PerasVoteSnapshot
 
 -- | A sequence number, incremented every time we receive a new vote.
 newtype PerasVoteTicketNo = PerasVoteTicketNo Word64
-  deriving stock Show
+  deriving stock (Generic, Show)
   deriving newtype (Eq, Ord, Enum, NoThunks)
 
 zeroPerasVoteTicketNo :: PerasVoteTicketNo

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

@@ -6,6 +6,7 @@ import qualified Test.Ouroboros.Storage.ChainDB as ChainDB
 import qualified Test.Ouroboros.Storage.ImmutableDB as ImmutableDB
 import qualified Test.Ouroboros.Storage.LedgerDB as LedgerDB
 import qualified Test.Ouroboros.Storage.PerasCertDB as PerasCertDB
+import qualified Test.Ouroboros.Storage.PerasVoteDB as PerasVoteDB
 import qualified Test.Ouroboros.Storage.VolatileDB as VolatileDB
 import Test.Tasty (TestTree, testGroup)
 
@@ -22,4 +23,5 @@ tests =
     , LedgerDB.tests
     , ChainDB.tests
     , PerasCertDB.tests
+    , PerasVoteDB.tests
     ]

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

@@ -1,3 +1,4 @@
+{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
@@ -19,6 +20,7 @@ import Ouroboros.Consensus.Util.CallStack
 import System.FS.API.Types (FsError, sameFsError)
 import Test.QuickCheck.StateModel (HasVariables)
 import Test.QuickCheck.StateModel.Variables (HasVariables (..))
+import Cardano.Crypto.Hash.Class (PackedBytes)
 
 {-------------------------------------------------------------------------------
   PrettyCallStack
@@ -76,3 +78,17 @@ deriving instance StandardHash blk => Eq (ChainDbError blk)
 
 instance HasVariables NominalDiffTime where
   getAllVariables _ = mempty
+
+{-------------------------------------------------------------------------------
+  Rational
+-------------------------------------------------------------------------------}
+
+instance HasVariables Rational where
+  getAllVariables _ = mempty
+
+{-------------------------------------------------------------------------------
+  PackedBytes
+-------------------------------------------------------------------------------}
+
+instance HasVariables (PackedBytes a) where
+  getAllVariables _ = mempty

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

@@ -0,0 +1,15 @@
+module Test.Ouroboros.Storage.PerasVoteDB (tests) where
+
+import qualified Test.Ouroboros.Storage.PerasVoteDB.StateMachine as StateMachine
+import Test.Tasty (TestTree, testGroup)
+
+--
+-- The list of all PerasVoteDB tests
+--
+
+tests :: TestTree
+tests =
+  testGroup
+    "PerasVoteDB"
+    [ StateMachine.tests
+    ]

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

@@ -0,0 +1,265 @@
+{-# LANGUAGE DeriveGeneric #-}
+
+module Test.Ouroboros.Storage.PerasVoteDB.Model
+  ( Model (..)
+  , initModel
+  , openDB
+  , closeDB
+  , addVote
+  , getVoteSnapshot
+  , getForgedCertForRound
+  , garbageCollect
+  ) where
+
+import Data.Map.Strict (Map)
+import qualified Data.Map.Strict as Map
+import Data.Set (Set)
+import qualified Data.Set as Set
+import GHC.Generics (Generic)
+import Ouroboros.Consensus.Block.Abstract (StandardHash)
+import Ouroboros.Consensus.Block.SupportsPeras
+  ( HasPerasVoteBlock (..)
+  , HasPerasVoteRound (..)
+  , PerasCert (..)
+  , PerasCfg
+  , PerasParams (..)
+  , PerasQuorumStakeThreshold (unPerasQuorumStakeThreshold)
+  , PerasRoundNo
+  , PerasVoteId (..)
+  , PerasVoteStake (..)
+  , PerasVoteTarget (..)
+  , PerasVoterId
+  , ValidatedPerasCert (..)
+  , ValidatedPerasVote
+  , getPerasCertBoostedBlock
+  , getPerasVoteStake
+  , getPerasVoteVoterId
+  )
+import Ouroboros.Consensus.BlockchainTime.WallClock.Types
+  ( WithArrivalTime (..)
+  )
+import Ouroboros.Consensus.Storage.PerasVoteDB.API
+  ( AddPerasVoteResult (..)
+  , PerasVoteSnapshot (..)
+  , PerasVoteTicketNo
+  , zeroPerasVoteTicketNo
+  )
+
+data VoteEntry blk = VoteEntry
+  { veTicketNo :: PerasVoteTicketNo
+  -- ^ The ticket number assigned to this vote
+  , veVoter :: PerasVoterId
+  -- ^ The voter ID
+  , veVote :: WithArrivalTime (ValidatedPerasVote blk)
+  -- ^ The vote itself
+  }
+  deriving (Show, Eq, Ord, Generic)
+
+data Model blk = Model
+  { open :: Bool
+  -- ^ Is the database open?
+  , params :: PerasParams
+  -- ^ Configuration parameters
+  , lastTicketNo :: PerasVoteTicketNo
+  -- ^ The last issued ticket number
+  , votes :: Map (PerasVoteTarget blk) (Set (VoteEntry blk))
+  -- ^ Collection of votes indexed by target (round number, boosted block)
+  , certs :: Map PerasRoundNo (ValidatedPerasCert blk)
+  -- ^ Forged certificates indexed by round number
+  }
+  deriving (Show, Generic)
+
+initModel :: PerasCfg blk -> Model blk
+initModel cfg =
+  Model
+    { open = False
+    , params = cfg
+    , lastTicketNo = zeroPerasVoteTicketNo
+    , votes = Map.empty
+    , certs = Map.empty
+    }
+
+-- | Check whether a given voter has already voted in a given round
+--
+-- NOTE: while this is an innefficient traversal, it allows the model to be as
+-- trivial as possible. The actual PerasVoteDB implementation uses a separate
+-- collection to track this information efficienty, at the cost of added
+-- complexity.
+hasVote ::
+  PerasVoteId blk ->
+  Model blk ->
+  Bool
+hasVote voteId model =
+  Set.member voteId voteIds
+ where
+  voteIds =
+    Set.unions $
+      [ Set.map
+          ( \ve ->
+              PerasVoteId
+                { pviRoundNo = pvtRoundNo voteTarget
+                , pviVoterId = veVoter ve
+                }
+          )
+          votesForTarget
+      | (voteTarget, votesForTarget) <- Map.toList (votes model)
+      ]
+
+openDB ::
+  Model blk ->
+  Model blk
+openDB model =
+  model
+    { open = True
+    }
+
+closeDB ::
+  Model blk ->
+  Model blk
+closeDB model =
+  model
+    { open = False
+    , lastTicketNo = zeroPerasVoteTicketNo
+    , votes = Map.empty
+    , certs = Map.empty
+    }
+
+addVote ::
+  StandardHash blk =>
+  WithArrivalTime (ValidatedPerasVote blk) ->
+  Model blk ->
+  ( Maybe (AddPerasVoteResult blk)
+  , Model blk
+  )
+addVote vote model
+  -- This voter has already voted in this round => ignore the vote
+  | voterAlreadyVotedInRound =
+      ( Just $
+          PerasVoteAlreadyInDB
+      , model
+      )
+  -- A quorum was reached, but there is another cert already boosting a different
+  -- block in this round => integrity violation (shouldn't happen in practice)
+  | reachedQuorum
+  , Just existingCert <- certAtRound
+  , getPerasCertBoostedBlock freshCert /= getPerasCertBoostedBlock existingCert =
+      ( Nothing -- Cannot have multiple certs for the same round
+      , model
+      )
+  -- A quorum was reached for the first time (when there is no existing
+  -- certificate for the given round) => causing a new cert to be generated
+  | reachedQuorum
+  , Nothing <- certAtRound =
+      ( Just $
+          AddedPerasVoteAndGeneratedNewCert freshCert
+      , model
+          { votes =
+              Map.insert voteTarget extendedVotes (votes model)
+          , certs =
+              Map.insert roundNo freshCert (certs model)
+          , lastTicketNo =
+              nextTicketNo
+          }
+      )
+  -- Otherwise, just add the vote without generating a new cert
+  | otherwise =
+      ( Just $
+          AddedPerasVoteButDidntGenerateNewCert
+      , model
+          { votes =
+              Map.insert voteTarget extendedVotes (votes model)
+          , lastTicketNo =
+              nextTicketNo
+          }
+      )
+ where
+  -- Extract relevant information from the vote
+  roundNo =
+    getPerasVoteRound vote
+  votedBlock =
+    getPerasVoteBlock vote
+  voter =
+    getPerasVoteVoterId vote
+  -- Compute the next ticket number associated to this vote
+  nextTicketNo =
+    succ (lastTicketNo model)
+  -- Prepare various data structures needed to update the model
+  voteId =
+    PerasVoteId{pviRoundNo = roundNo, pviVoterId = voter}
+  voteTarget =
+    PerasVoteTarget{pvtRoundNo = roundNo, pvtBlock = votedBlock}
+  voteEntry =
+    VoteEntry{veTicketNo = nextTicketNo, veVoter = voter, veVote = vote}
+  -- Has this  voter already voted in this round?
+  voterAlreadyVotedInRound =
+    hasVote voteId model
+
+  -- The existing votes for this round and block
+  existingVotes =
+    Map.findWithDefault Set.empty voteTarget (votes model)
+  -- The extended set of votes including the new one
+  extendedVotes =
+    Set.insert voteEntry existingVotes
+  -- Did we reach the quorum threshold with this new vote?
+  reachedQuorum =
+    sum (getVoteStake . veVote <$> Set.toList extendedVotes)
+      >= quorumStakeThreshold model
+   where
+    quorumStakeThreshold =
+      unPerasQuorumStakeThreshold . perasQuorumStakeThreshold . params
+    getVoteStake =
+      unPerasVoteStake . getPerasVoteStake . forgetArrivalTime
+  -- The existing certificate (if any) for this round
+  certAtRound =
+    Map.lookup roundNo (certs model)
+  -- The fresh certificate that would be generated if a quorum is reached
+  freshCert =
+    ValidatedPerasCert
+      { vpcCert =
+          PerasCert
+            { pcCertRound = getPerasVoteRound vote
+            , pcCertBoostedBlock = getPerasVoteBlock vote
+            }
+      , vpcCertBoost = perasWeight (params model)
+      }
+
+getVoteSnapshot ::
+  Model blk ->
+  PerasVoteSnapshot blk
+getVoteSnapshot model =
+  PerasVoteSnapshot
+    { containsVote = \voteId ->
+        hasVote
+          voteId
+          model
+    , getVotesAfter = \ticketNo ->
+        Map.fromList
+          [ (tn, vote)
+          | (_, vs) <- Map.toList (votes model)
+          , VoteEntry{veTicketNo = tn, veVote = vote} <- Set.toList vs
+          , tn > ticketNo
+          ]
+    }
+
+getForgedCertForRound ::
+  PerasRoundNo ->
+  Model blk ->
+  Maybe (ValidatedPerasCert blk)
+getForgedCertForRound roundNo model =
+  Map.lookup roundNo (certs model)
+
+garbageCollect ::
+  PerasRoundNo ->
+  Model blk ->
+  Model blk
+garbageCollect roundNo model =
+  model
+    { votes =
+        Map.filterWithKey
+          (\voteTarget _ -> pvtRoundNo voteTarget >= roundNo)
+          (votes model)
+    , certs =
+        Map.filterWithKey
+          (\r _ -> r >= roundNo)
+          (certs model)
+    }