{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wno-orphans -Wno-incomplete-uni-patterns #-}

-- | Tests of properties of the chain DB model
--
-- The model for the chain DB (@Test.Ouroboros.Storage.ChainDB.Model@) contains
-- a quite a bit of info, but that is primarily because it needs to support
-- stateful APIs such as followers (that follow the tip of the chain) and
-- iterators (which stream a chunk of the chain). The main part of the model is
-- it's model of the volatile DB and the immutable DB, which is again satisfyingly
-- simple: the volatile DB is modelled simply as a set of blocks, and the
-- immutable DB is modelled simply as a list of blocks (i.e., a chain).
--
-- Nonetheless, the implementation of the operations on that model is subtle.
-- In particular, the chain DB is responsible for chain selection, and so the
-- model must too. So we have a few properties checking some aspects of the model;
-- in particular, we verify that no matter in which order we add blocks to the
-- chain DB, we always pick the most preferred chain.
module Test.Ouroboros.Storage.ChainDB.Model.Test (tests) where

import Cardano.Ledger.BaseTypes (unNonZero)
import GHC.Stack
import Ouroboros.Consensus.Block
import Ouroboros.Consensus.Config
import Ouroboros.Consensus.Ledger.Tables
import Ouroboros.Consensus.Storage.ChainDB.API
  ( LoE (..)
  , StreamFrom (..)
  , StreamTo (..)
  )
import qualified Ouroboros.Consensus.Util.AnchoredFragment as AF
import qualified Ouroboros.Network.AnchoredFragment as AF
import qualified Ouroboros.Network.Mock.Chain as Chain
import Test.Ouroboros.Storage.ChainDB.Model (ModelSupportsBlock)
import qualified Test.Ouroboros.Storage.ChainDB.Model as M
import Test.QuickCheck
import Test.Tasty
import Test.Tasty.QuickCheck
import Test.Util.Orphans.Arbitrary ()
import Test.Util.TestBlock

tests :: TestTree
tests :: TestTree
tests =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
"Model"
    [ TestName
-> (LoE () -> BlockTree -> Permutation -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"getBlock_addBlock" LoE () -> BlockTree -> Permutation -> Property
prop_getBlock_addBlock
    , TestName -> (BlockChain -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"getChain_addChain" BlockChain -> Property
prop_getChain_addChain
    , TestName -> (BlockTree -> Permutation -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"alwaysPickPreferredChain" BlockTree -> Permutation -> Property
prop_alwaysPickPreferredChain
    , TestName -> (LoE () -> BlockTree -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"between_currentChain" LoE () -> BlockTree -> Property
prop_between_currentChain
    ]

addBlocks :: LoE () -> [TestBlock] -> M.Model TestBlock
addBlocks :: LoE () -> [TestBlock] -> Model TestBlock
addBlocks LoE ()
loe [TestBlock]
blks = TopLevelConfig TestBlock
-> [TestBlock] -> Model TestBlock -> Model TestBlock
forall blk.
(LedgerSupportsProtocol blk,
 LedgerTablesAreTrivial (ExtLedgerState blk)) =>
TopLevelConfig blk -> [blk] -> Model blk -> Model blk
M.addBlocks TopLevelConfig TestBlock
cfg [TestBlock]
blks (LoE () -> ExtLedgerState TestBlock EmptyMK -> Model TestBlock
forall blk.
HasHeader blk =>
LoE () -> ExtLedgerState blk EmptyMK -> Model blk
M.empty LoE ()
loe (ExtLedgerState TestBlock ValuesMK
-> ExtLedgerState TestBlock EmptyMK
forall (mk :: MapKind) (mk' :: MapKind).
ExtLedgerState TestBlock mk -> ExtLedgerState TestBlock mk'
forall (l :: LedgerStateKind) (mk :: MapKind) (mk' :: MapKind).
LedgerTablesAreTrivial l =>
l mk -> l mk'
convertMapKind ExtLedgerState TestBlock ValuesMK
testInitExtLedger))
 where
  cfg :: TopLevelConfig TestBlock
cfg = TopLevelConfig TestBlock
singleNodeTestConfig

prop_getBlock_addBlock :: LoE () -> BlockTree -> Permutation -> Property
prop_getBlock_addBlock :: LoE () -> BlockTree -> Permutation -> Property
prop_getBlock_addBlock LoE ()
loe BlockTree
bt Permutation
p =
  HeaderHash TestBlock -> Model TestBlock -> Maybe TestBlock
forall blk.
HasHeader blk =>
HeaderHash blk -> Model blk -> Maybe blk
M.getBlock (TestBlock -> HeaderHash TestBlock
forall b. HasHeader b => b -> HeaderHash b
blockHash TestBlock
newBlock) (TopLevelConfig TestBlock
-> TestBlock -> Model TestBlock -> Model TestBlock
forall blk.
(LedgerSupportsProtocol blk,
 LedgerTablesAreTrivial (ExtLedgerState blk)) =>
TopLevelConfig blk -> blk -> Model blk -> Model blk
M.addBlock TopLevelConfig TestBlock
singleNodeTestConfig TestBlock
newBlock Model TestBlock
model)
    Maybe TestBlock -> Maybe TestBlock -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== if BlockNo -> WithOrigin BlockNo
forall t. t -> WithOrigin t
NotOrigin (TestBlock -> BlockNo
forall b. HasHeader b => b -> BlockNo
blockNo TestBlock
newBlock) WithOrigin BlockNo -> WithOrigin BlockNo -> Bool
forall a. Ord a => a -> a -> Bool
> SecurityParam -> Model TestBlock -> WithOrigin BlockNo
forall blk.
HasHeader blk =>
SecurityParam -> Model blk -> WithOrigin BlockNo
M.immutableBlockNo SecurityParam
secParam Model TestBlock
model
      then TestBlock -> Maybe TestBlock
forall a. a -> Maybe a
Just TestBlock
newBlock
      else Maybe TestBlock
forall a. Maybe a
Nothing
 where
  (TestBlock
newBlock : [TestBlock]
initBlocks) = Permutation -> [TestBlock] -> [TestBlock]
forall a. Permutation -> [a] -> [a]
permute Permutation
p ([TestBlock] -> [TestBlock]) -> [TestBlock] -> [TestBlock]
forall a b. (a -> b) -> a -> b
$ BlockTree -> [TestBlock]
treeToBlocks BlockTree
bt
  model :: Model TestBlock
model = LoE () -> [TestBlock] -> Model TestBlock
addBlocks LoE ()
loe [TestBlock]
initBlocks
  secParam :: SecurityParam
secParam = TopLevelConfig TestBlock -> SecurityParam
forall blk.
ConsensusProtocol (BlockProtocol blk) =>
TopLevelConfig blk -> SecurityParam
configSecurityParam TopLevelConfig TestBlock
singleNodeTestConfig

-- | Test that, for any chain @bc@, adding its blocks to an empty model causes
-- the selection to be @bc@. This is only true with LoE disabled.
prop_getChain_addChain :: BlockChain -> Property
prop_getChain_addChain :: BlockChain -> Property
prop_getChain_addChain BlockChain
bc =
  TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"model: " TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ Model TestBlock -> TestName
forall a. Show a => a -> TestName
show Model TestBlock
model) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    BlockChain -> Chain TestBlock
blockChain BlockChain
bc Chain TestBlock -> Chain TestBlock -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Model TestBlock -> Chain TestBlock
forall blk. Model blk -> Chain blk
M.currentChain Model TestBlock
model
 where
  blocks :: [TestBlock]
blocks = BlockChain -> [TestBlock]
chainToBlocks BlockChain
bc
  model :: Model TestBlock
model = LoE () -> [TestBlock] -> Model TestBlock
addBlocks LoE ()
forall a. LoE a
LoEDisabled [TestBlock]
blocks

-- | Test that, no matter in which order we add blocks to the chain DB, we
-- always pick the most preferred chain. This is only true with LoE disabled.
prop_alwaysPickPreferredChain :: BlockTree -> Permutation -> Property
prop_alwaysPickPreferredChain :: BlockTree -> Permutation -> Property
prop_alwaysPickPreferredChain BlockTree
bt Permutation
p =
  TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"blocks: " TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ [TestBlock] -> TestName
forall a. Show a => a -> TestName
show [TestBlock]
blocks) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"invalid: " TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ Map TestHash (ExtValidationError TestBlock, SlotNo) -> TestName
forall a. Show a => a -> TestName
show (Model TestBlock -> InvalidBlocks TestBlock
forall blk. Model blk -> InvalidBlocks blk
M.invalid Model TestBlock
model)) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
      [Bool] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
        [ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Chain TestBlock -> Bool
preferCandidate' Chain TestBlock
candidate
        | Chain TestBlock
candidate <- BlockTree -> [Chain TestBlock]
treeToChains BlockTree
bt
        ]
 where
  blocks :: [TestBlock]
blocks = Permutation -> [TestBlock] -> [TestBlock]
forall a. Permutation -> [a] -> [a]
permute Permutation
p ([TestBlock] -> [TestBlock]) -> [TestBlock] -> [TestBlock]
forall a b. (a -> b) -> a -> b
$ BlockTree -> [TestBlock]
treeToBlocks BlockTree
bt
  model :: Model TestBlock
model = LoE () -> [TestBlock] -> Model TestBlock
addBlocks LoE ()
forall a. LoE a
LoEDisabled [TestBlock]
blocks
  current :: Chain TestBlock
current = Model TestBlock -> Chain TestBlock
forall blk. Model blk -> Chain blk
M.currentChain Model TestBlock
model

  curFragment :: AnchoredFragment (Header TestBlock)
curFragment = Chain (Header TestBlock) -> AnchoredFragment (Header TestBlock)
forall block.
HasHeader block =>
Chain block -> AnchoredFragment block
Chain.toAnchoredFragment (TestBlock -> Header TestBlock
forall blk. GetHeader blk => blk -> Header blk
getHeader (TestBlock -> Header TestBlock)
-> Chain TestBlock -> Chain (Header TestBlock)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Chain TestBlock
current)

  SecurityParam NonZero Word64
k = TopLevelConfig TestBlock -> SecurityParam
forall blk.
ConsensusProtocol (BlockProtocol blk) =>
TopLevelConfig blk -> SecurityParam
configSecurityParam TopLevelConfig TestBlock
singleNodeTestConfig

  bcfg :: BlockConfig TestBlock
bcfg = TopLevelConfig TestBlock -> BlockConfig TestBlock
forall blk. TopLevelConfig blk -> BlockConfig blk
configBlock TopLevelConfig TestBlock
singleNodeTestConfig

  preferCandidate' :: Chain TestBlock -> Bool
preferCandidate' Chain TestBlock
candidate =
    BlockConfig TestBlock
-> AnchoredFragment (Header TestBlock)
-> AnchoredFragment (Header TestBlock)
-> Bool
forall blk (h :: * -> *) (h' :: * -> *).
(BlockSupportsProtocol blk, HasCallStack, GetHeader1 h,
 GetHeader1 h', HeaderHash (h blk) ~ HeaderHash (h' blk),
 HasHeader (h blk), HasHeader (h' blk)) =>
BlockConfig blk
-> AnchoredFragment (h blk) -> AnchoredFragment (h' blk) -> Bool
AF.preferAnchoredCandidate BlockConfig TestBlock
bcfg AnchoredFragment (Header TestBlock)
curFragment AnchoredFragment (Header TestBlock)
candFragment
      Bool -> Bool -> Bool
&& Word64
-> AnchoredFragment (Header TestBlock)
-> AnchoredFragment (Header TestBlock)
-> Bool
forall b.
HasHeader b =>
Word64 -> AnchoredFragment b -> AnchoredFragment b -> Bool
AF.forksAtMostKBlocks (NonZero Word64 -> Word64
forall a. NonZero a -> a
unNonZero NonZero Word64
k) AnchoredFragment (Header TestBlock)
curFragment AnchoredFragment (Header TestBlock)
candFragment
   where
    candFragment :: AnchoredFragment (Header TestBlock)
candFragment = Chain (Header TestBlock) -> AnchoredFragment (Header TestBlock)
forall block.
HasHeader block =>
Chain block -> AnchoredFragment block
Chain.toAnchoredFragment (TestBlock -> Header TestBlock
forall blk. GetHeader blk => blk -> Header blk
getHeader (TestBlock -> Header TestBlock)
-> Chain TestBlock -> Chain (Header TestBlock)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Chain TestBlock
candidate)

-- TODO add properties about forks too
prop_between_currentChain :: LoE () -> BlockTree -> Property
prop_between_currentChain :: LoE () -> BlockTree -> Property
prop_between_currentChain LoE ()
loe BlockTree
bt =
  [TestBlock] -> Either (UnknownRange TestBlock) [TestBlock]
forall a b. b -> Either a b
Right (AnchoredSeq (WithOrigin SlotNo) (Anchor TestBlock) TestBlock
-> [TestBlock]
forall v a b. AnchoredSeq v a b -> [b]
AF.toOldestFirst (AnchoredSeq (WithOrigin SlotNo) (Anchor TestBlock) TestBlock
 -> [TestBlock])
-> AnchoredSeq (WithOrigin SlotNo) (Anchor TestBlock) TestBlock
-> [TestBlock]
forall a b. (a -> b) -> a -> b
$ Chain TestBlock
-> AnchoredSeq (WithOrigin SlotNo) (Anchor TestBlock) TestBlock
forall block.
HasHeader block =>
Chain block -> AnchoredFragment block
Chain.toAnchoredFragment (Chain TestBlock
 -> AnchoredSeq (WithOrigin SlotNo) (Anchor TestBlock) TestBlock)
-> Chain TestBlock
-> AnchoredSeq (WithOrigin SlotNo) (Anchor TestBlock) TestBlock
forall a b. (a -> b) -> a -> b
$ Model TestBlock -> Chain TestBlock
forall blk. Model blk -> Chain blk
M.currentChain Model TestBlock
model)
    Either (UnknownRange TestBlock) [TestBlock]
-> Either (UnknownRange TestBlock) [TestBlock] -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== SecurityParam
-> StreamFrom TestBlock
-> StreamTo TestBlock
-> Model TestBlock
-> Either (UnknownRange TestBlock) [TestBlock]
forall blk.
GetPrevHash blk =>
SecurityParam
-> StreamFrom blk
-> StreamTo blk
-> Model blk
-> Either (UnknownRange blk) [blk]
M.between SecurityParam
secParam StreamFrom TestBlock
forall {blk}. StreamFrom blk
from StreamTo TestBlock
to Model TestBlock
model
 where
  blocks :: [TestBlock]
blocks = BlockTree -> [TestBlock]
treeToBlocks BlockTree
bt
  model :: Model TestBlock
model = LoE () -> [TestBlock] -> Model TestBlock
addBlocks LoE ()
loe [TestBlock]
blocks
  from :: StreamFrom blk
from = Point blk -> StreamFrom blk
forall blk. Point blk -> StreamFrom blk
StreamFromExclusive Point blk
forall {k} (block :: k). Point block
GenesisPoint
  to :: StreamTo TestBlock
to = RealPoint TestBlock -> StreamTo TestBlock
forall blk. RealPoint blk -> StreamTo blk
StreamToInclusive (RealPoint TestBlock -> StreamTo TestBlock)
-> RealPoint TestBlock -> StreamTo TestBlock
forall a b. (a -> b) -> a -> b
$ Point TestBlock -> RealPoint TestBlock
forall blk. HasCallStack => Point blk -> RealPoint blk
cantBeGenesis (Model TestBlock -> Point TestBlock
forall blk. HasHeader blk => Model blk -> Point blk
M.tipPoint Model TestBlock
model)
  secParam :: SecurityParam
secParam = TopLevelConfig TestBlock -> SecurityParam
forall blk.
ConsensusProtocol (BlockProtocol blk) =>
TopLevelConfig blk -> SecurityParam
configSecurityParam TopLevelConfig TestBlock
singleNodeTestConfig

-- | Workaround when we know the DB can't be empty, but the types don't
cantBeGenesis :: HasCallStack => Point blk -> RealPoint blk
cantBeGenesis :: forall blk. HasCallStack => Point blk -> RealPoint blk
cantBeGenesis Point blk
GenesisPoint = TestName -> RealPoint blk
forall a. HasCallStack => TestName -> a
error TestName
"cantBeGenesis: what did I tell you!?"
cantBeGenesis (BlockPoint SlotNo
s HeaderHash blk
h) = SlotNo -> HeaderHash blk -> RealPoint blk
forall blk. SlotNo -> HeaderHash blk -> RealPoint blk
RealPoint SlotNo
s HeaderHash blk
h

{-------------------------------------------------------------------------------
  Orphan instances
-------------------------------------------------------------------------------}

instance ModelSupportsBlock TestBlock