[WIP] set structure for model-based testing for PerasCertDB

Author: tbagrel1

ouroboros-consensus/ouroboros-consensus.cabal

@@ -721,6 +721,9 @@ test-suite storage-test
     Test.Ouroboros.Storage.LedgerDB.V1.DbChangelog
     Test.Ouroboros.Storage.LedgerDB.V1.LMDB
     Test.Ouroboros.Storage.Orphans
+    Test.Ouroboros.Storage.PerasCertDB
+    Test.Ouroboros.Storage.PerasCertDB.Model
+    Test.Ouroboros.Storage.PerasCertDB.StateMachine
     Test.Ouroboros.Storage.TestBlock
     Test.Ouroboros.Storage.VolatileDB
     Test.Ouroboros.Storage.VolatileDB.Mock

ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Block/SupportsPeras.hs

@@ -23,6 +23,7 @@ import Ouroboros.Consensus.Block.Abstract
 
 newtype PerasRoundNo = PerasRoundNo {unPerasRoundNo :: Word64}
   deriving stock Show
+  deriving Generic
   deriving newtype (Eq, Ord, NoThunks)
 
 newtype PerasWeight = PerasWeight {unPerasWeight :: Word64}
@@ -50,7 +51,7 @@ instance StandardHash blk => BlockSupportsPeras blk where
     { pcCertRound :: PerasRoundNo
     , pcCertBoostedBlock :: Point blk
     }
-    deriving stock Generic
+    deriving stock (Generic, Eq, Ord, Show)
     deriving anyclass NoThunks
 
   perasCertRound = pcCertRound

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

@@ -2,6 +2,7 @@
 {-# LANGUAGE DerivingVia #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE DeriveGeneric #-}
 
 module Ouroboros.Consensus.Storage.PerasCertDB.API
   ( PerasCertDB (..)
@@ -17,6 +18,7 @@ import Ouroboros.Consensus.Block
 import Ouroboros.Consensus.Util.IOLike
 import Ouroboros.Network.AnchoredFragment (AnchoredFragment)
 import qualified Ouroboros.Network.AnchoredFragment as AF
+import GHC.Generics (Generic)
 
 data PerasCertDB m blk = PerasCertDB
   { addCert :: PerasCert blk -> m ()
@@ -29,6 +31,7 @@ newtype PerasWeightSnapshot blk = PerasWeightSnapshot
   { getPerasWeightSnapshot :: Map (Point blk) PerasWeight
   }
   deriving stock Show
+  deriving Generic
   deriving newtype NoThunks
 
 boostedWeightForPoint ::

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

@@ -6,6 +6,8 @@ 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.VolatileDB as VolatileDB
+import qualified Test.Ouroboros.Storage.PerasCertDB as PerasCertDB
+
 import Test.Tasty (TestTree, testGroup)
 
 --
@@ -20,4 +22,5 @@ tests =
     , VolatileDB.tests
     , LedgerDB.tests
     , ChainDB.tests
+    , PerasCertDB.tests
     ]

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

@@ -0,0 +1,17 @@
+{-# LANGUAGE CPP #-}
+
+module Test.Ouroboros.Storage.PerasCertDB (tests) where
+
+import qualified Test.Ouroboros.Storage.PerasCertDB.StateMachine as StateMachine
+import Test.Tasty (TestTree, testGroup)
+
+--
+-- The list of all PerasCertDB tests
+--
+
+tests :: TestTree
+tests =
+  testGroup
+    "PerasCertDB"
+    [ StateMachine.tests
+    ]

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

@@ -0,0 +1,60 @@
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE UndecidableInstances #-}
+module Test.Ouroboros.Storage.PerasCertDB.Model
+  ( PerasCertDBModel,
+    initPerasCertDBModel,
+    openDBModel,
+    closeDBModel,
+    addCertModel,
+    getWeightSnapshotModel
+  ) where
+import Ouroboros.Consensus.Block (PerasCert, boostPerCert, perasCertBoostedBlock, StandardHash)
+import Data.Set (Set)
+import GHC.Generics (Generic)
+import Data.Proxy (Proxy)
+import qualified Data.Set as Set
+import Ouroboros.Consensus.Storage.PerasCertDB.API
+import qualified Data.Map as Map
+import Data.Vector.Internal.Check (HasCallStack)
+import Ouroboros.Consensus.Storage.PerasCertDB.Impl (PerasCertDbError(..))
+import Ouroboros.Consensus.Util.CallStack (prettyCallStack)
+
+data PerasCertDBModel blk = PerasCertDBModel
+    {
+        open :: Bool,
+        certs :: Set (PerasCert blk)
+    } deriving Generic
+
+deriving instance (StandardHash blk) => Show (PerasCertDBModel blk)
+
+initPerasCertDBModel :: Proxy blk -> PerasCertDBModel blk
+initPerasCertDBModel _ = PerasCertDBModel
+    { open = False
+    , certs = Set.empty
+    }
+
+openDBModel :: PerasCertDBModel blk -> PerasCertDBModel blk
+openDBModel model = model { open = True }
+
+closeDBModel :: PerasCertDBModel blk -> PerasCertDBModel blk
+closeDBModel model = model { open = False }
+
+addCertModel :: (HasCallStack, StandardHash blk) => PerasCertDBModel blk -> PerasCert blk -> Either PerasCertDbError (PerasCertDBModel blk)
+addCertModel model cert =
+    if open model
+    then Right model { certs = Set.insert cert (certs model) }
+    else Left (ClosedDBError prettyCallStack)
+
+getWeightSnapshotModel :: (HasCallStack, StandardHash blk) => PerasCertDBModel blk -> Either PerasCertDbError (PerasWeightSnapshot blk)
+getWeightSnapshotModel model =
+    if open model
+    then
+        Right $ PerasWeightSnapshot {
+            getPerasWeightSnapshot = Set.fold
+                (\cert acc -> Map.insertWith (<>) (perasCertBoostedBlock cert) boostPerCert acc)
+                Map.empty
+                (certs model)
+        }
+    else Left (ClosedDBError prettyCallStack)

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

@@ -0,0 +1,29 @@
+
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE FlexibleInstances #-}
+module Test.Ouroboros.Storage.PerasCertDB.StateMachine (tests) where
+import Test.Tasty (TestTree)
+import Test.Ouroboros.Storage.TestBlock (TestBlock)
+import Ouroboros.Consensus.Block.SupportsPeras
+import Test.Ouroboros.Storage.PerasCertDB.Model
+import Test.QuickCheck.StateModel
+import Ouroboros.Consensus.Storage.PerasCertDB.API (PerasWeightSnapshot)
+
+tests :: TestTree
+tests = undefined
+
+type Block = TestBlock
+newtype Model = Model (PerasCertDBModel Block) deriving (Show, Generic)
+
+instance StateModel Model where
+  data Action Model a where
+    OpenDB :: Action Model ()
+    CloseDB :: Action Model ()
+    AddCert :: PerasCert Block -> Action Model ()
+    GetWeightSnapshot :: Action Model (PerasWeightSnapshot Block)
+
+  arbitraryAction _ _ = error "arbitraryAction not implemented"
+  initialState = error "initialState not implemented"