diff --git a/ouroboros-consensus/changelog.d/20250917_101832_thomas.bagrel_peras_cert_db.md b/ouroboros-consensus/changelog.d/20250917_101832_thomas.bagrel_peras_cert_db.md new file mode 100644 index 0000000000..8d348d4575 --- /dev/null +++ b/ouroboros-consensus/changelog.d/20250917_101832_thomas.bagrel_peras_cert_db.md @@ -0,0 +1,24 @@ + + + + + +### Breaking + +- Added modules `Ouroboros.Consensus.Storage.PerasCertDB{,.API,.Impl}`, notably defining the types`PerasCertDB`, `PerasCertSnapshot` (read-only snapshot of certs contained in the DB), and `AddPerasCertResult`; alongside their respectives methods +- Added modules `Test.Ouroboros.Storage.PerasCertDB{,.StateMachine,.Model}` for q-s-m testing of the `PerasCertDB` datatype. The corresponding tests have been included in the test suite defined by `Test.Ouroboros.Storage` diff --git a/ouroboros-consensus/ouroboros-consensus.cabal b/ouroboros-consensus/ouroboros-consensus.cabal index b8097608ed..f66cd91d93 100644 --- a/ouroboros-consensus/ouroboros-consensus.cabal +++ b/ouroboros-consensus/ouroboros-consensus.cabal @@ -264,6 +264,9 @@ library Ouroboros.Consensus.Storage.LedgerDB.V2.Forker Ouroboros.Consensus.Storage.LedgerDB.V2.InMemory Ouroboros.Consensus.Storage.LedgerDB.V2.LedgerSeq + Ouroboros.Consensus.Storage.PerasCertDB + Ouroboros.Consensus.Storage.PerasCertDB.API + Ouroboros.Consensus.Storage.PerasCertDB.Impl Ouroboros.Consensus.Storage.Serialisation Ouroboros.Consensus.Storage.VolatileDB Ouroboros.Consensus.Storage.VolatileDB.API @@ -720,6 +723,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.VolatileDB Test.Ouroboros.Storage.VolatileDB.Mock Test.Ouroboros.Storage.VolatileDB.Model diff --git a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Storage/PerasCertDB.hs b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Storage/PerasCertDB.hs new file mode 100644 index 0000000000..288039b30c --- /dev/null +++ b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Storage/PerasCertDB.hs @@ -0,0 +1,4 @@ +module Ouroboros.Consensus.Storage.PerasCertDB (module X) where + +import Ouroboros.Consensus.Storage.PerasCertDB.API as X +import Ouroboros.Consensus.Storage.PerasCertDB.Impl as X diff --git a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Storage/PerasCertDB/API.hs b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Storage/PerasCertDB/API.hs new file mode 100644 index 0000000000..2d136af38d --- /dev/null +++ b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Storage/PerasCertDB/API.hs @@ -0,0 +1,56 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Ouroboros.Consensus.Storage.PerasCertDB.API + ( PerasCertDB (..) + , AddPerasCertResult (..) + + -- * 'PerasCertSnapshot' + , PerasCertSnapshot (..) + , PerasCertTicketNo + , zeroPerasCertTicketNo + ) where + +import Data.Word (Word64) +import NoThunks.Class +import Ouroboros.Consensus.Block +import Ouroboros.Consensus.Peras.Weight +import Ouroboros.Consensus.Util.IOLike +import Ouroboros.Consensus.Util.STM (WithFingerprint (..)) + +data PerasCertDB m blk = PerasCertDB + { addCert :: ValidatedPerasCert blk -> m AddPerasCertResult + -- ^ Add a Peras certificate to the database. The result indicates whether + -- the certificate was actually added, or if it was already present. + , getWeightSnapshot :: STM m (WithFingerprint (PerasWeightSnapshot blk)) + -- ^ Return the Peras weights in order compare the current selection against + -- potential candidate chains, namely the weights for blocks not older than + -- the current immutable tip. It might contain weights for even older blocks + -- if they have not yet been garbage-collected. + -- + -- The 'Fingerprint' is updated every time a new certificate is added, but it + -- stays the same when certificates are garbage-collected. + , getCertSnapshot :: STM m (PerasCertSnapshot blk) + , garbageCollect :: SlotNo -> m () + -- ^ Garbage-collect state older than the given slot number. + , closeDB :: m () + } + deriving NoThunks via OnlyCheckWhnfNamed "PerasCertDB" (PerasCertDB m blk) + +data AddPerasCertResult = AddedPerasCertToDB | PerasCertAlreadyInDB + deriving stock (Show, Eq) + +data PerasCertSnapshot blk = PerasCertSnapshot + { containsCert :: PerasRoundNo -> Bool + -- ^ Do we have the certificate for this round? + , getCertsAfter :: PerasCertTicketNo -> [(ValidatedPerasCert blk, PerasCertTicketNo)] + } + +newtype PerasCertTicketNo = PerasCertTicketNo Word64 + deriving stock Show + deriving newtype (Eq, Ord, Enum, NoThunks) + +zeroPerasCertTicketNo :: PerasCertTicketNo +zeroPerasCertTicketNo = PerasCertTicketNo 0 diff --git a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Storage/PerasCertDB/Impl.hs b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Storage/PerasCertDB/Impl.hs new file mode 100644 index 0000000000..1837900fef --- /dev/null +++ b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Storage/PerasCertDB/Impl.hs @@ -0,0 +1,297 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneKindSignatures #-} + +module Ouroboros.Consensus.Storage.PerasCertDB.Impl + ( -- * Opening + PerasCertDbArgs (..) + , defaultArgs + , openDB + + -- * Trace types + , TraceEvent (..) + + -- * Exceptions + , PerasCertDbError (..) + ) where + +import Control.Tracer (Tracer, nullTracer, traceWith) +import Data.Functor ((<&>)) +import Data.Kind (Type) +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map +import GHC.Generics (Generic) +import NoThunks.Class +import Ouroboros.Consensus.Block +import Ouroboros.Consensus.Peras.Weight +import Ouroboros.Consensus.Storage.PerasCertDB.API +import Ouroboros.Consensus.Util.Args +import Ouroboros.Consensus.Util.CallStack +import Ouroboros.Consensus.Util.IOLike +import Ouroboros.Consensus.Util.STM + +{------------------------------------------------------------------------------ + Opening the database +------------------------------------------------------------------------------} + +type PerasCertDbArgs :: (Type -> Type) -> (Type -> Type) -> Type -> Type +data PerasCertDbArgs f m blk = PerasCertDbArgs + { pcdbaTracer :: Tracer m (TraceEvent blk) + } + +defaultArgs :: Applicative m => Incomplete PerasCertDbArgs m blk +defaultArgs = + PerasCertDbArgs + { pcdbaTracer = nullTracer + } + +openDB :: + forall m blk. + ( IOLike m + , StandardHash blk + ) => + Complete PerasCertDbArgs m blk -> + m (PerasCertDB m blk) +openDB args = do + pcdbVolatileState <- newTVarIO initialPerasVolatileCertState + let env = + PerasCertDbEnv + { pcdbTracer + , pcdbVolatileState + } + h <- PerasCertDbHandle <$> newTVarIO (PerasCertDbOpen env) + traceWith pcdbTracer OpenedPerasCertDB + pure + PerasCertDB + { addCert = getEnv1 h implAddCert + , getWeightSnapshot = getEnvSTM h implGetWeightSnapshot + , getCertSnapshot = getEnvSTM h implGetCertSnapshot + , garbageCollect = getEnv1 h implGarbageCollect + , closeDB = implCloseDB h + } + where + PerasCertDbArgs + { pcdbaTracer = pcdbTracer + } = args + +{------------------------------------------------------------------------------- + Database state +-------------------------------------------------------------------------------} + +newtype PerasCertDbHandle m blk = PerasCertDbHandle (StrictTVar m (PerasCertDbState m blk)) + +data PerasCertDbState m blk + = PerasCertDbOpen !(PerasCertDbEnv m blk) + | PerasCertDbClosed + deriving stock Generic + deriving anyclass NoThunks + +data PerasCertDbEnv m blk = PerasCertDbEnv + { pcdbTracer :: !(Tracer m (TraceEvent blk)) + , pcdbVolatileState :: !(StrictTVar m (WithFingerprint (PerasVolatileCertState blk))) + -- ^ The 'RoundNo's of all certificates currently in the db. + } + deriving NoThunks via OnlyCheckWhnfNamed "PerasCertDbEnv" (PerasCertDbEnv m blk) + +getEnv :: + (IOLike m, HasCallStack) => + PerasCertDbHandle m blk -> + (PerasCertDbEnv m blk -> m r) -> + m r +getEnv (PerasCertDbHandle varState) f = + readTVarIO varState >>= \case + PerasCertDbOpen env -> f env + PerasCertDbClosed -> throwIO $ ClosedDBError prettyCallStack + +getEnv1 :: + (IOLike m, HasCallStack) => + PerasCertDbHandle m blk -> + (PerasCertDbEnv m blk -> a -> m r) -> + a -> + m r +getEnv1 h f a = getEnv h (\env -> f env a) + +getEnvSTM :: + (IOLike m, HasCallStack) => + PerasCertDbHandle m blk -> + (PerasCertDbEnv m blk -> STM m r) -> + STM m r +getEnvSTM (PerasCertDbHandle varState) f = + readTVar varState >>= \case + PerasCertDbOpen env -> f env + PerasCertDbClosed -> throwIO $ ClosedDBError prettyCallStack + +{------------------------------------------------------------------------------- + API implementation +-------------------------------------------------------------------------------} + +implCloseDB :: IOLike m => PerasCertDbHandle m blk -> m () +implCloseDB (PerasCertDbHandle varState) = + atomically (swapTVar varState PerasCertDbClosed) >>= \case + PerasCertDbOpen PerasCertDbEnv{pcdbTracer} -> do + traceWith pcdbTracer ClosedPerasCertDB + -- DB was already closed. + PerasCertDbClosed -> pure () + +-- TODO: we will need to update this method with non-trivial validation logic +-- see https://github.com/tweag/cardano-peras/issues/120 +implAddCert :: + ( IOLike m + , StandardHash blk + ) => + PerasCertDbEnv m blk -> + ValidatedPerasCert blk -> + m AddPerasCertResult +implAddCert env cert = do + traceWith pcdbTracer $ AddingPerasCert roundNo boostedPt + res <- atomically $ do + WithFingerprint + PerasVolatileCertState + { pvcsCerts + , pvcsWeightByPoint + , pvcsCertsByTicket + , pvcsLastTicketNo + } + fp <- + readTVar pcdbVolatileState + if Map.member roundNo pvcsCerts + then pure PerasCertAlreadyInDB + else do + let pvcsLastTicketNo' = succ pvcsLastTicketNo + writeTVar pcdbVolatileState $ + WithFingerprint + PerasVolatileCertState + { pvcsCerts = + Map.insert roundNo cert pvcsCerts + , -- Note that the same block might be boosted by multiple points. + pvcsWeightByPoint = + addToPerasWeightSnapshot boostedPt (getPerasCertBoost cert) pvcsWeightByPoint + , pvcsCertsByTicket = + Map.insert pvcsLastTicketNo' cert pvcsCertsByTicket + , pvcsLastTicketNo = pvcsLastTicketNo' + } + (succ fp) + pure AddedPerasCertToDB + traceWith pcdbTracer $ case res of + AddedPerasCertToDB -> AddedPerasCert roundNo boostedPt + PerasCertAlreadyInDB -> IgnoredCertAlreadyInDB roundNo boostedPt + pure res + where + PerasCertDbEnv + { pcdbTracer + , pcdbVolatileState + } = env + + boostedPt = getPerasCertBoostedBlock cert + roundNo = getPerasCertRound cert + +implGetWeightSnapshot :: + IOLike m => + PerasCertDbEnv m blk -> STM m (WithFingerprint (PerasWeightSnapshot blk)) +implGetWeightSnapshot PerasCertDbEnv{pcdbVolatileState} = + fmap pvcsWeightByPoint <$> readTVar pcdbVolatileState + +implGetCertSnapshot :: + IOLike m => + PerasCertDbEnv m blk -> STM m (PerasCertSnapshot blk) +implGetCertSnapshot PerasCertDbEnv{pcdbVolatileState} = + readTVar pcdbVolatileState + <&> forgetFingerprint + <&> \PerasVolatileCertState + { pvcsCerts + , pvcsCertsByTicket + } -> + PerasCertSnapshot + { containsCert = \r -> Map.member r pvcsCerts + , getCertsAfter = \ticketNo -> + let (_, certs) = Map.split ticketNo pvcsCertsByTicket + in [(cert, tno) | (tno, cert) <- Map.toAscList certs] + } + +implGarbageCollect :: + forall m blk. + (IOLike m, StandardHash blk) => + PerasCertDbEnv m blk -> SlotNo -> m () +implGarbageCollect PerasCertDbEnv{pcdbVolatileState} slot = + -- No need to update the 'Fingerprint' as we only remove certificates that do + -- not matter for comparing interesting chains. + atomically $ modifyTVar pcdbVolatileState (fmap gc) + where + gc :: PerasVolatileCertState blk -> PerasVolatileCertState blk + gc + PerasVolatileCertState + { pvcsCerts + , pvcsWeightByPoint + , pvcsLastTicketNo + , pvcsCertsByTicket + } = + PerasVolatileCertState + { pvcsCerts = Map.filter keepCert pvcsCerts + , pvcsWeightByPoint = prunePerasWeightSnapshot slot pvcsWeightByPoint + , pvcsCertsByTicket = Map.filter keepCert pvcsCertsByTicket + , pvcsLastTicketNo = pvcsLastTicketNo + } + where + keepCert cert = + pointSlot (getPerasCertBoostedBlock cert) >= NotOrigin slot + +{------------------------------------------------------------------------------- + Implementation-internal types +-------------------------------------------------------------------------------} + +-- | Volatile Peras certificate state, i.e. certificates that could influence +-- chain selection by boosting a volatile block. +data PerasVolatileCertState blk = PerasVolatileCertState + { pvcsCerts :: !(Map PerasRoundNo (ValidatedPerasCert blk)) + -- ^ The boosted blocks by 'RoundNo' of all certificates currently in the db. + , pvcsWeightByPoint :: !(PerasWeightSnapshot blk) + -- ^ The weight of boosted blocks w.r.t. the certificates currently in the db. + -- + -- INVARIANT: In sync with 'pvcsCerts'. + , pvcsCertsByTicket :: !(Map PerasCertTicketNo (ValidatedPerasCert blk)) + -- ^ The certificates by 'PerasCertTicketNo'. + -- + -- INVARIANT: In sync with 'pvcsCerts'. + , pvcsLastTicketNo :: !PerasCertTicketNo + -- ^ The most recent 'PerasCertTicketNo' (or 'zeroPerasCertTicketNo' + -- otherwise). + } + deriving stock (Show, Generic) + deriving anyclass NoThunks + +initialPerasVolatileCertState :: WithFingerprint (PerasVolatileCertState blk) +initialPerasVolatileCertState = + WithFingerprint + PerasVolatileCertState + { pvcsCerts = Map.empty + , pvcsWeightByPoint = emptyPerasWeightSnapshot + , pvcsCertsByTicket = Map.empty + , pvcsLastTicketNo = zeroPerasCertTicketNo + } + (Fingerprint 0) + +{------------------------------------------------------------------------------- + Trace types +-------------------------------------------------------------------------------} + +data TraceEvent blk + = OpenedPerasCertDB + | ClosedPerasCertDB + | AddingPerasCert PerasRoundNo (Point blk) + | AddedPerasCert PerasRoundNo (Point blk) + | IgnoredCertAlreadyInDB PerasRoundNo (Point blk) + deriving stock (Show, Eq, Generic) + +{------------------------------------------------------------------------------- + Exceptions +-------------------------------------------------------------------------------} + +data PerasCertDbError + = ClosedDBError PrettyCallStack + deriving stock Show + deriving anyclass Exception diff --git a/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage.hs b/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage.hs index 419d8872a7..1153457c70 100644 --- a/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage.hs +++ b/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage.hs @@ -5,6 +5,7 @@ module Test.Ouroboros.Storage (tests) where 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.VolatileDB as VolatileDB import Test.Tasty (TestTree, testGroup) @@ -20,4 +21,5 @@ tests = , VolatileDB.tests , LedgerDB.tests , ChainDB.tests + , PerasCertDB.tests ] diff --git a/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/PerasCertDB.hs b/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/PerasCertDB.hs new file mode 100644 index 0000000000..6a3f06bf90 --- /dev/null +++ b/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 + ] diff --git a/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/PerasCertDB/Model.hs b/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/PerasCertDB/Model.hs new file mode 100644 index 0000000000..f6e7f5cb27 --- /dev/null +++ b/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/PerasCertDB/Model.hs @@ -0,0 +1,62 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE UndecidableInstances #-} + +module Test.Ouroboros.Storage.PerasCertDB.Model + ( Model (..) + , initModel + , openDB + , closeDB + , addCert + , getWeightSnapshot + , garbageCollect + ) where + +import Data.Set (Set) +import qualified Data.Set as Set +import GHC.Generics (Generic) +import Ouroboros.Consensus.Block +import Ouroboros.Consensus.Peras.Weight + ( PerasWeightSnapshot + , mkPerasWeightSnapshot + ) + +data Model blk = Model + { certs :: Set (ValidatedPerasCert blk) + , open :: Bool + } + deriving Generic + +deriving instance StandardHash blk => Show (Model blk) + +initModel :: Model blk +initModel = Model{open = False, certs = Set.empty} + +openDB :: Model blk -> Model blk +openDB model = model{open = True} + +closeDB :: Model blk -> Model blk +closeDB _ = Model{open = False, certs = Set.empty} + +addCert :: + StandardHash blk => + Model blk -> ValidatedPerasCert blk -> Model blk +addCert model@Model{certs} cert = + model{certs = Set.insert cert certs} + +getWeightSnapshot :: + StandardHash blk => + Model blk -> PerasWeightSnapshot blk +getWeightSnapshot Model{certs} = + mkPerasWeightSnapshot + [ (getPerasCertBoostedBlock cert, getPerasCertBoost cert) + | cert <- Set.toList certs + ] + +garbageCollect :: StandardHash blk => SlotNo -> Model blk -> Model blk +garbageCollect slot model@Model{certs} = + model{certs = Set.filter keepCert certs} + where + keepCert cert = pointSlot (getPerasCertBoostedBlock cert) >= NotOrigin slot diff --git a/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/PerasCertDB/StateMachine.hs b/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/PerasCertDB/StateMachine.hs new file mode 100644 index 0000000000..cba3925c47 --- /dev/null +++ b/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/PerasCertDB/StateMachine.hs @@ -0,0 +1,147 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedRecordDot #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} + +module Test.Ouroboros.Storage.PerasCertDB.StateMachine (tests) where + +import Control.Monad.State +import Control.Tracer (nullTracer) +import qualified Data.List.NonEmpty as NE +import qualified Data.Set as Set +import Ouroboros.Consensus.Block +import Ouroboros.Consensus.Peras.Weight (PerasWeightSnapshot) +import qualified Ouroboros.Consensus.Storage.PerasCertDB as PerasCertDB +import Ouroboros.Consensus.Storage.PerasCertDB.API (AddPerasCertResult (..), PerasCertDB) +import Ouroboros.Consensus.Util.IOLike +import Ouroboros.Consensus.Util.STM +import qualified Test.Ouroboros.Storage.PerasCertDB.Model as Model +import Test.QuickCheck +import qualified Test.QuickCheck.Monadic as QC +import Test.QuickCheck.StateModel +import Test.Tasty +import Test.Tasty.QuickCheck +import Test.Util.TestBlock (TestBlock, TestHash (..)) +import Test.Util.TestEnv (adjustQuickCheckTests) + +tests :: TestTree +tests = + testGroup + "PerasCertDB" + [ adjustQuickCheckTests (* 100) $ testProperty "q-d" $ prop_qd + ] + +prop_qd :: Actions Model -> Property +prop_qd actions = QC.monadic f $ property () <$ runActions actions + where + f :: StateT (PerasCertDB IO TestBlock) IO Property -> Property + f = ioProperty . flip evalStateT (error "unreachable") + +newtype Model = Model (Model.Model TestBlock) deriving (Show, Generic) + +instance StateModel Model where + data Action Model a where + OpenDB :: Action Model () + CloseDB :: Action Model () + AddCert :: ValidatedPerasCert TestBlock -> Action Model AddPerasCertResult + GetWeightSnapshot :: Action Model (PerasWeightSnapshot TestBlock) + GarbageCollect :: SlotNo -> Action Model () + + arbitraryAction _ (Model model) + | model.open = + frequency + [ (1, pure $ Some CloseDB) + , (20, Some <$> genAddCert) + , (20, pure $ Some GetWeightSnapshot) + , (5, Some . GarbageCollect . SlotNo <$> arbitrary) + ] + | otherwise = pure $ Some OpenDB + where + genAddCert = do + roundNo <- PerasRoundNo <$> arbitrary + boostedBlock <- genPoint + pure $ + AddCert + ValidatedPerasCert + { vpcCert = + PerasCert + { pcCertRound = roundNo + , pcCertBoostedBlock = boostedBlock + } + , vpcCertBoost = boostPerCert + } + + genPoint :: Gen (Point TestBlock) + genPoint = + oneof + [ return GenesisPoint + , BlockPoint <$> (SlotNo <$> arbitrary) <*> genHash + ] + where + genHash = TestHash . NE.fromList . getNonEmpty <$> arbitrary + + initialState = Model Model.initModel + + nextState (Model model) action _ = Model $ case action of + OpenDB -> Model.openDB model + CloseDB -> Model.closeDB model + AddCert cert -> Model.addCert model cert + GetWeightSnapshot -> model + GarbageCollect slot -> Model.garbageCollect slot model + + precondition (Model model) = \case + OpenDB -> not model.open + action -> + model.open && case action of + CloseDB -> True + -- Do not add equivocating certificates. + AddCert cert -> all p model.certs + where + p cert' = getPerasCertRound cert /= getPerasCertRound cert' || cert == cert' + GetWeightSnapshot -> True + GarbageCollect _slot -> True + +deriving stock instance Show (Action Model a) +deriving stock instance Eq (Action Model a) + +instance HasVariables (Action Model a) where + getAllVariables _ = mempty + +instance RunModel Model (StateT (PerasCertDB IO TestBlock) IO) where + perform _ action _ = case action of + OpenDB -> do + perasCertDB <- lift $ PerasCertDB.openDB (PerasCertDB.PerasCertDbArgs nullTracer) + put perasCertDB + CloseDB -> do + perasCertDB <- get + lift $ PerasCertDB.closeDB perasCertDB + AddCert cert -> do + perasCertDB <- get + lift $ PerasCertDB.addCert perasCertDB cert + GetWeightSnapshot -> do + perasCertDB <- get + lift $ atomically $ forgetFingerprint <$> PerasCertDB.getWeightSnapshot perasCertDB + GarbageCollect slot -> do + perasCertDB <- get + lift $ PerasCertDB.garbageCollect perasCertDB slot + + postcondition (Model model, _) (AddCert cert) _ actual = do + let expected + | cert `Set.member` model.certs = PerasCertAlreadyInDB + | otherwise = AddedPerasCertToDB + counterexamplePost $ show expected <> " /= " <> show actual + pure $ expected == actual + postcondition (Model model, _) GetWeightSnapshot _ actual = do + let expected = Model.getWeightSnapshot model + counterexamplePost $ "Model: " <> show expected + counterexamplePost $ "SUT: " <> show actual + pure $ expected == actual + postcondition _ _ _ _ = pure True