Skip to content

Commit 3669032

Browse files
amesgenamesgen
committed
Pairing
1 parent 95bb58e commit 3669032

File tree

4 files changed

+160
-73
lines changed

4 files changed

+160
-73
lines changed

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ module Ouroboros.Consensus.Block.SupportsPeras
1313
, PerasWeight (..)
1414
, boostPerCert
1515
, BlockSupportsPeras (..)
16+
, PerasCert (..)
1617
) where
1718

1819
import Data.Monoid (Sum (..))

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
{-# LANGUAGE DataKinds #-}
2+
{-# LANGUAGE DeriveGeneric #-}
23
{-# LANGUAGE DerivingVia #-}
34
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
45
{-# LANGUAGE ScopedTypeVariables #-}
5-
{-# LANGUAGE DeriveGeneric #-}
66

77
module Ouroboros.Consensus.Storage.PerasCertDB.API
88
( PerasCertDB (..)
@@ -13,12 +13,12 @@ module Ouroboros.Consensus.Storage.PerasCertDB.API
1313

1414
import Data.Map.Strict (Map)
1515
import qualified Data.Map.Strict as Map
16+
import GHC.Generics (Generic)
1617
import NoThunks.Class
1718
import Ouroboros.Consensus.Block
1819
import Ouroboros.Consensus.Util.IOLike
1920
import Ouroboros.Network.AnchoredFragment (AnchoredFragment)
2021
import qualified Ouroboros.Network.AnchoredFragment as AF
21-
import GHC.Generics (Generic)
2222

2323
data PerasCertDB m blk = PerasCertDB
2424
{ addCert :: PerasCert blk -> m ()
@@ -30,7 +30,7 @@ data PerasCertDB m blk = PerasCertDB
3030
newtype PerasWeightSnapshot blk = PerasWeightSnapshot
3131
{ getPerasWeightSnapshot :: Map (Point blk) PerasWeight
3232
}
33-
deriving stock Show
33+
deriving stock (Show, Eq)
3434
deriving Generic
3535
deriving newtype NoThunks
3636

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

Lines changed: 51 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -1,60 +1,58 @@
11
{-# LANGUAGE DeriveGeneric #-}
2-
{-# LANGUAGE StandaloneDeriving #-}
32
{-# LANGUAGE FlexibleContexts #-}
3+
{-# LANGUAGE NamedFieldPuns #-}
4+
{-# LANGUAGE StandaloneDeriving #-}
45
{-# LANGUAGE UndecidableInstances #-}
6+
57
module Test.Ouroboros.Storage.PerasCertDB.Model
6-
( PerasCertDBModel,
7-
initPerasCertDBModel,
8-
openDBModel,
9-
closeDBModel,
10-
addCertModel,
11-
getWeightSnapshotModel
8+
( Model (..)
9+
, initModel
10+
, openDB
11+
, closeDB
12+
, addCert
13+
, getWeightSnapshot
1214
) where
13-
import Ouroboros.Consensus.Block (PerasCert, boostPerCert, perasCertBoostedBlock, StandardHash)
15+
16+
import qualified Data.Map as Map
1417
import Data.Set (Set)
15-
import GHC.Generics (Generic)
16-
import Data.Proxy (Proxy)
1718
import qualified Data.Set as Set
18-
import Ouroboros.Consensus.Storage.PerasCertDB.API
19-
import qualified Data.Map as Map
20-
import Data.Vector.Internal.Check (HasCallStack)
21-
import Ouroboros.Consensus.Storage.PerasCertDB.Impl (PerasCertDbError(..))
22-
import Ouroboros.Consensus.Util.CallStack (prettyCallStack)
23-
24-
data PerasCertDBModel blk = PerasCertDBModel
25-
{
26-
open :: Bool,
27-
certs :: Set (PerasCert blk)
28-
} deriving Generic
29-
30-
deriving instance (StandardHash blk) => Show (PerasCertDBModel blk)
31-
32-
initPerasCertDBModel :: Proxy blk -> PerasCertDBModel blk
33-
initPerasCertDBModel _ = PerasCertDBModel
34-
{ open = False
35-
, certs = Set.empty
36-
}
37-
38-
openDBModel :: PerasCertDBModel blk -> PerasCertDBModel blk
39-
openDBModel model = model { open = True }
40-
41-
closeDBModel :: PerasCertDBModel blk -> PerasCertDBModel blk
42-
closeDBModel model = model { open = False }
43-
44-
addCertModel :: (HasCallStack, StandardHash blk) => PerasCertDBModel blk -> PerasCert blk -> Either PerasCertDbError (PerasCertDBModel blk)
45-
addCertModel model cert =
46-
if open model
47-
then Right model { certs = Set.insert cert (certs model) }
48-
else Left (ClosedDBError prettyCallStack)
49-
50-
getWeightSnapshotModel :: (HasCallStack, StandardHash blk) => PerasCertDBModel blk -> Either PerasCertDbError (PerasWeightSnapshot blk)
51-
getWeightSnapshotModel model =
52-
if open model
53-
then
54-
Right $ PerasWeightSnapshot {
55-
getPerasWeightSnapshot = Set.fold
56-
(\cert acc -> Map.insertWith (<>) (perasCertBoostedBlock cert) boostPerCert acc)
57-
Map.empty
58-
(certs model)
59-
}
60-
else Left (ClosedDBError prettyCallStack)
19+
import GHC.Generics (Generic)
20+
import Ouroboros.Consensus.Block (PerasCert, StandardHash, boostPerCert, perasCertBoostedBlock)
21+
import Ouroboros.Consensus.Storage.PerasCertDB.API (PerasWeightSnapshot (..))
22+
23+
data Model blk = Model
24+
{ certs :: Set (PerasCert blk)
25+
, open :: Bool
26+
}
27+
deriving Generic
28+
29+
deriving instance StandardHash blk => Show (Model blk)
30+
31+
initModel :: Model blk
32+
initModel = Model{open = False, certs = Set.empty}
33+
34+
openDB :: Model blk -> Model blk
35+
openDB model = model{open = True}
36+
37+
closeDB :: Model blk -> Model blk
38+
closeDB _ = Model{open = False, certs = Set.empty}
39+
40+
addCert ::
41+
StandardHash blk =>
42+
Model blk -> PerasCert blk -> Model blk
43+
addCert model@Model{certs} cert =
44+
model{certs = Set.insert cert certs}
45+
46+
getWeightSnapshot ::
47+
StandardHash blk =>
48+
Model blk -> PerasWeightSnapshot blk
49+
getWeightSnapshot Model{certs} = snap
50+
where
51+
snap =
52+
PerasWeightSnapshot
53+
{ getPerasWeightSnapshot =
54+
Set.fold
55+
(\cert acc -> Map.insertWith (<>) (perasCertBoostedBlock cert) boostPerCert acc)
56+
Map.empty
57+
certs
58+
}

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

Lines changed: 105 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -1,36 +1,124 @@
1-
2-
{-# LANGUAGE TypeFamilies #-}
3-
{-# LANGUAGE GADTs #-}
41
{-# LANGUAGE DeriveGeneric #-}
5-
{-# LANGUAGE StandaloneDeriving #-}
2+
{-# LANGUAGE DerivingStrategies #-}
3+
{-# LANGUAGE FlexibleContexts #-}
64
{-# LANGUAGE FlexibleInstances #-}
5+
{-# LANGUAGE GADTs #-}
6+
{-# LANGUAGE LambdaCase #-}
7+
{-# LANGUAGE MultiParamTypeClasses #-}
8+
{-# LANGUAGE NamedFieldPuns #-}
9+
{-# LANGUAGE OverloadedRecordDot #-}
10+
{-# LANGUAGE OverloadedStrings #-}
11+
{-# LANGUAGE StandaloneDeriving #-}
12+
{-# LANGUAGE TypeFamilies #-}
13+
{-# LANGUAGE UndecidableInstances #-}
14+
{-# OPTIONS_GHC -Wno-orphans #-}
15+
716
module Test.Ouroboros.Storage.PerasCertDB.StateMachine (tests) where
8-
import Test.Tasty (TestTree)
9-
import Test.Ouroboros.Storage.TestBlock (TestBlock)
10-
import Ouroboros.Consensus.Block.SupportsPeras
11-
import Test.Ouroboros.Storage.PerasCertDB.Model
17+
18+
import Control.Monad.State
19+
import Control.Tracer (nullTracer)
20+
import qualified Data.List.NonEmpty as NE
21+
import Ouroboros.Consensus.Block
22+
import qualified Ouroboros.Consensus.Storage.PerasCertDB as PerasCertDB
23+
import Ouroboros.Consensus.Storage.PerasCertDB.API (PerasCertDB, PerasWeightSnapshot)
24+
import Ouroboros.Consensus.Util.IOLike
25+
import qualified Test.Ouroboros.Storage.PerasCertDB.Model as Model
26+
import Test.QuickCheck
27+
import qualified Test.QuickCheck.Monadic as QC
1228
import Test.QuickCheck.StateModel
13-
import Ouroboros.Consensus.Storage.PerasCertDB.API (PerasWeightSnapshot)
14-
import Ouroboros.Consensus.Storage.PerasCertDB (PerasCertDbError)
29+
import Test.Tasty
30+
import Test.Tasty.QuickCheck
31+
import Test.Util.TestBlock (TestBlock, TestHash (..))
32+
import Test.Util.TestEnv (adjustQuickCheckTests)
1533

1634
tests :: TestTree
17-
tests = undefined
35+
tests =
36+
testGroup
37+
"PerasCertDB"
38+
[ adjustQuickCheckTests (* 100) $ testProperty "q-d" $ prop_qd
39+
]
40+
41+
prop_qd :: Actions Model -> Property
42+
prop_qd actions = QC.monadic f $ property () <$ runActions actions
43+
where
44+
f :: StateT (PerasCertDB IO TestBlock) IO Property -> Property
45+
f = ioProperty . flip evalStateT (error "unreachable")
1846

1947
type Block = TestBlock
20-
newtype Model = Model (PerasCertDBModel Block) deriving (Show, Generic)
48+
newtype Model = Model (Model.Model Block) deriving (Show, Generic)
2149

2250
instance StateModel Model where
2351
data Action Model a where
2452
OpenDB :: Action Model ()
2553
CloseDB :: Action Model ()
26-
AddCert :: PerasCert Block -> Action Model (Either PerasCertDbError ())
27-
GetWeightSnapshot :: Action Model (Either PerasCertDbError (PerasWeightSnapshot Block))
54+
AddCert :: PerasCert Block -> Action Model ()
55+
GetWeightSnapshot :: Action Model (PerasWeightSnapshot Block)
56+
57+
arbitraryAction _ (Model model)
58+
| model.open =
59+
frequency
60+
[ (1, pure $ Some CloseDB)
61+
, (20, Some <$> genAddCert)
62+
, (20, pure $ Some GetWeightSnapshot)
63+
]
64+
| otherwise = pure $ Some OpenDB
65+
where
66+
genAddCert = do
67+
pcCertRound <- PerasRoundNo <$> arbitrary
68+
pcCertBoostedBlock <- arbitrary
69+
pure $ AddCert PerasCert{pcCertRound, pcCertBoostedBlock}
70+
71+
initialState = Model Model.initModel
2872

29-
arbitraryAction _ _ = error "arbitraryAction not implemented"
30-
initialState = error "initialState not implemented"
73+
nextState (Model model) action _ = Model $ case action of
74+
OpenDB -> Model.openDB model
75+
CloseDB -> Model.closeDB model
76+
AddCert cert -> Model.addCert model cert
77+
GetWeightSnapshot -> model
3178

32-
deriving instance Show (Action Model a)
79+
precondition (Model model) = \case
80+
OpenDB -> not model.open
81+
action ->
82+
model.open && case action of
83+
CloseDB -> True
84+
AddCert cert -> all p model.certs
85+
where
86+
p cert' = perasCertRound cert /= perasCertRound cert' || cert == cert'
87+
GetWeightSnapshot -> True
88+
89+
deriving stock instance Show (Action Model a)
90+
deriving stock instance Eq (Action Model a)
3391

3492
instance HasVariables (Action Model a) where
3593
getAllVariables _ = mempty
3694

95+
instance RunModel Model (StateT (PerasCertDB IO TestBlock) IO) where
96+
perform _ action _ = case action of
97+
OpenDB -> do
98+
perasCertDB <- lift $ PerasCertDB.openDB (PerasCertDB.PerasCertDbArgs nullTracer)
99+
put perasCertDB
100+
CloseDB -> do
101+
perasCertDB <- get
102+
lift $ PerasCertDB.closeDB perasCertDB
103+
AddCert cert -> do
104+
perasCertDB <- get
105+
lift $ PerasCertDB.addCert perasCertDB cert
106+
GetWeightSnapshot -> do
107+
perasCertDB <- get
108+
lift $ atomically $ PerasCertDB.getWeightSnapshot perasCertDB
109+
110+
-- TODO: check open state consistency
111+
postcondition (Model model, _) GetWeightSnapshot _ actual = do
112+
let expected = Model.getWeightSnapshot model
113+
counterexamplePost $ "Model: " <> show expected
114+
counterexamplePost $ "SUT: " <> show actual
115+
pure $ expected == actual
116+
postcondition _ _ _ _ = pure True
117+
118+
-- TODO very ugly
119+
instance Arbitrary (Point TestBlock) where
120+
arbitrary =
121+
oneof
122+
[ return GenesisPoint
123+
, BlockPoint <$> (SlotNo <$> arbitrary) <*> (TestHash . NE.fromList . getNonEmpty <$> arbitrary)
124+
]

0 commit comments

Comments
 (0)