-- | Property tests for header validations
module Test.Consensus.HeaderValidation (tests) where

import           Control.Monad.Except (runExcept)
import           Data.List.NonEmpty (NonEmpty (..))
import qualified Data.Map.Strict as Map
import           Data.Word (Word64)
import           Ouroboros.Consensus.Block.Abstract
import           Ouroboros.Consensus.Config
import           Ouroboros.Consensus.HeaderValidation
import qualified Test.QuickCheck as QC
import           Test.Tasty (TestTree, testGroup)
import           Test.Tasty.QuickCheck (testProperty)
import           Test.Util.TestBlock

tests :: TestTree
tests :: TestTree
tests = TestName -> [TestTree] -> TestTree
testGroup TestName
"HeaderValidation"
  [ TestName -> [TestTree] -> TestTree
testGroup TestName
"validateIfCheckpoint"
    [ TestName
-> ([NonNegative Int] -> NonNegative Int -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"non-checkpoints are ignored" [NonNegative Int] -> NonNegative Int -> Property
prop_validateIfCheckpoint_nonCheckpoint
    , TestName
-> ([NonNegative Int] -> NonNegative Int -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"checkpoint matches should be accepted" [NonNegative Int] -> NonNegative Int -> Property
prop_validateIfCheckpoint_checkpoint_matches
    , TestName
-> ([NonNegative Int] -> NonNegative Int -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"checkpoint mismatches should be rejected" [NonNegative Int] -> NonNegative Int -> Property
prop_validateIfCheckpoint_checkpoint_mismatches
    ]
  ]

-- | Make a test block from the length of the hash and the Word64
-- to create it.
mkTestBlock :: QC.NonNegative Int -> Word64 -> TestBlock
mkTestBlock :: NonNegative Int -> Word64 -> TestBlock
mkTestBlock (QC.NonNegative Int
n) Word64
h =
    TestHash -> SlotNo -> () -> TestBlock
forall ptype. TestHash -> SlotNo -> ptype -> TestBlockWith ptype
successorBlockWithPayload
      (NonEmpty Word64 -> TestHash
TestHash (NonEmpty Word64 -> TestHash) -> NonEmpty Word64 -> TestHash
forall a b. (a -> b) -> a -> b
$ Word64
h Word64 -> [Word64] -> NonEmpty Word64
forall a. a -> [a] -> NonEmpty a
:| Int -> Word64 -> [Word64]
forall a. Int -> a -> [a]
replicate Int
n Word64
h)
      (Int -> SlotNo
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n SlotNo -> SlotNo -> SlotNo
forall a. Num a => a -> a -> a
+ SlotNo
1)
      ()

-- | Like 'validateHeader', but takes a list of blocks to use as
-- checkpoints.
validateHeaderBlocks ::
     [TestBlock]
  -> TestBlock
  -> Either (HeaderError TestBlock) (HeaderState TestBlock)
validateHeaderBlocks :: [TestBlock]
-> TestBlock
-> Either (HeaderError TestBlock) (HeaderState TestBlock)
validateHeaderBlocks [TestBlock]
xs TestBlock
x =
    let
      checkpoints :: CheckpointsMap TestBlock
checkpoints = Map BlockNo (HeaderHash TestBlock) -> CheckpointsMap TestBlock
forall blk. Map BlockNo (HeaderHash blk) -> CheckpointsMap blk
CheckpointsMap (Map BlockNo (HeaderHash TestBlock) -> CheckpointsMap TestBlock)
-> Map BlockNo (HeaderHash TestBlock) -> CheckpointsMap TestBlock
forall a b. (a -> b) -> a -> b
$ [(BlockNo, HeaderHash TestBlock)]
-> Map BlockNo (HeaderHash TestBlock)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (TestBlock -> BlockNo
forall b. HasHeader b => b -> BlockNo
blockNo TestBlock
b, TestBlock -> HeaderHash TestBlock
forall b. HasHeader b => b -> HeaderHash b
blockHash TestBlock
b) | TestBlock
b <- [TestBlock]
xs]
      cfg :: TopLevelConfig TestBlock
cfg = TopLevelConfig TestBlock
singleNodeTestConfig {topLevelConfigCheckpoints = checkpoints}
      h :: Header TestBlock
h = TestBlock -> Header TestBlock
forall blk. GetHeader blk => blk -> Header blk
getHeader TestBlock
x
      -- Chose the header state carefully so it doesn't cause validation to fail
      annTip :: WithOrigin (AnnTip TestBlock)
annTip =
        case Header TestBlock -> ChainHash TestBlock
forall blk. GetPrevHash blk => Header blk -> ChainHash blk
headerPrevHash Header TestBlock
h of
          ChainHash TestBlock
GenesisHash -> WithOrigin (AnnTip TestBlock)
forall t. WithOrigin t
Origin
          BlockHash HeaderHash TestBlock
hsh -> AnnTip TestBlock -> WithOrigin (AnnTip TestBlock)
forall t. t -> WithOrigin t
NotOrigin (AnnTip TestBlock -> WithOrigin (AnnTip TestBlock))
-> AnnTip TestBlock -> WithOrigin (AnnTip TestBlock)
forall a b. (a -> b) -> a -> b
$ SlotNo -> BlockNo -> TipInfo TestBlock -> AnnTip TestBlock
forall blk. SlotNo -> BlockNo -> TipInfo blk -> AnnTip blk
AnnTip (TestBlock -> SlotNo
forall b. HasHeader b => b -> SlotNo
blockSlot TestBlock
x SlotNo -> SlotNo -> SlotNo
forall a. Num a => a -> a -> a
- SlotNo
1) (TestBlock -> BlockNo
forall b. HasHeader b => b -> BlockNo
blockNo TestBlock
x BlockNo -> BlockNo -> BlockNo
forall a. Num a => a -> a -> a
- BlockNo
1) HeaderHash TestBlock
TipInfo TestBlock
hsh
      headerState :: Ticked (HeaderState TestBlock)
headerState =
        ConsensusConfig (BlockProtocol TestBlock)
-> LedgerView (BlockProtocol TestBlock)
-> SlotNo
-> HeaderState TestBlock
-> Ticked (HeaderState TestBlock)
forall blk.
ConsensusProtocol (BlockProtocol blk) =>
ConsensusConfig (BlockProtocol blk)
-> LedgerView (BlockProtocol blk)
-> SlotNo
-> HeaderState blk
-> Ticked (HeaderState blk)
tickHeaderState
          (TopLevelConfig TestBlock
-> ConsensusConfig (BlockProtocol TestBlock)
forall blk.
TopLevelConfig blk -> ConsensusConfig (BlockProtocol blk)
topLevelConfigProtocol TopLevelConfig TestBlock
cfg)
          ()
          SlotNo
0
          (WithOrigin (AnnTip TestBlock)
-> ChainDepState (BlockProtocol TestBlock) -> HeaderState TestBlock
forall blk.
WithOrigin (AnnTip blk)
-> ChainDepState (BlockProtocol blk) -> HeaderState blk
HeaderState WithOrigin (AnnTip TestBlock)
annTip ())
     in
      Except (HeaderError TestBlock) (HeaderState TestBlock)
-> Either (HeaderError TestBlock) (HeaderState TestBlock)
forall e a. Except e a -> Either e a
runExcept (Except (HeaderError TestBlock) (HeaderState TestBlock)
 -> Either (HeaderError TestBlock) (HeaderState TestBlock))
-> Except (HeaderError TestBlock) (HeaderState TestBlock)
-> Either (HeaderError TestBlock) (HeaderState TestBlock)
forall a b. (a -> b) -> a -> b
$
        TopLevelConfig TestBlock
-> LedgerView (BlockProtocol TestBlock)
-> Header TestBlock
-> Ticked (HeaderState TestBlock)
-> Except (HeaderError TestBlock) (HeaderState TestBlock)
forall blk.
(BlockSupportsProtocol blk, ValidateEnvelope blk) =>
TopLevelConfig blk
-> LedgerView (BlockProtocol blk)
-> Header blk
-> Ticked (HeaderState blk)
-> Except (HeaderError blk) (HeaderState blk)
validateHeader TopLevelConfig TestBlock
cfg () Header TestBlock
h Ticked (HeaderState TestBlock)
headerState

prop_validateIfCheckpoint_nonCheckpoint
  :: [QC.NonNegative Int] -> QC.NonNegative Int -> QC.Property
prop_validateIfCheckpoint_nonCheckpoint :: [NonNegative Int] -> NonNegative Int -> Property
prop_validateIfCheckpoint_nonCheckpoint [NonNegative Int]
xs NonNegative Int
x0 =
    let
      blks :: [TestBlock]
blks = (NonNegative Int -> TestBlock) -> [NonNegative Int] -> [TestBlock]
forall a b. (a -> b) -> [a] -> [b]
map (NonNegative Int -> Word64 -> TestBlock
`mkTestBlock` Word64
0) ([NonNegative Int] -> [TestBlock])
-> [NonNegative Int] -> [TestBlock]
forall a b. (a -> b) -> a -> b
$ (NonNegative Int -> Bool) -> [NonNegative Int] -> [NonNegative Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (NonNegative Int -> NonNegative Int -> Bool
forall a. Eq a => a -> a -> Bool
/= NonNegative Int
x0) [NonNegative Int]
xs
     in
      case [TestBlock]
-> TestBlock
-> Either (HeaderError TestBlock) (HeaderState TestBlock)
validateHeaderBlocks [TestBlock]
blks (NonNegative Int -> Word64 -> TestBlock
mkTestBlock NonNegative Int
x0 Word64
0) of
        Left HeaderError TestBlock
e ->
          TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample TestName
"checkpoint validation should not fail on other blocks than checkpoints" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (HeaderError TestBlock -> TestName
forall a. Show a => a -> TestName
show HeaderError TestBlock
e) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          Bool -> Property
forall prop. Testable prop => prop -> Property
QC.property Bool
False
        Right HeaderState TestBlock
_ -> Bool -> Property
forall prop. Testable prop => prop -> Property
QC.property Bool
True

prop_validateIfCheckpoint_checkpoint_matches
  :: [QC.NonNegative Int] -> QC.NonNegative Int -> QC.Property
prop_validateIfCheckpoint_checkpoint_matches :: [NonNegative Int] -> NonNegative Int -> Property
prop_validateIfCheckpoint_checkpoint_matches [NonNegative Int]
xs NonNegative Int
x =
    let
      blks :: [TestBlock]
blks = (NonNegative Int -> TestBlock) -> [NonNegative Int] -> [TestBlock]
forall a b. (a -> b) -> [a] -> [b]
map (NonNegative Int -> Word64 -> TestBlock
`mkTestBlock` Word64
0) (NonNegative Int
xNonNegative Int -> [NonNegative Int] -> [NonNegative Int]
forall a. a -> [a] -> [a]
:[NonNegative Int]
xs)
     in
      case [TestBlock]
-> TestBlock
-> Either (HeaderError TestBlock) (HeaderState TestBlock)
validateHeaderBlocks [TestBlock]
blks (NonNegative Int -> Word64 -> TestBlock
mkTestBlock NonNegative Int
x Word64
0) of
        Left HeaderError TestBlock
e  ->
          TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample TestName
"checkpoint matches should be accepted" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (HeaderError TestBlock -> TestName
forall a. Show a => a -> TestName
show HeaderError TestBlock
e) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          Bool -> Property
forall prop. Testable prop => prop -> Property
QC.property Bool
False
        Right HeaderState TestBlock
_ -> Bool -> Property
forall prop. Testable prop => prop -> Property
QC.property Bool
True

prop_validateIfCheckpoint_checkpoint_mismatches
  :: [QC.NonNegative Int] -> QC.NonNegative Int -> QC.Property
prop_validateIfCheckpoint_checkpoint_mismatches :: [NonNegative Int] -> NonNegative Int -> Property
prop_validateIfCheckpoint_checkpoint_mismatches [NonNegative Int]
xs NonNegative Int
x =
    let
      blks :: [TestBlock]
blks = (NonNegative Int -> TestBlock) -> [NonNegative Int] -> [TestBlock]
forall a b. (a -> b) -> [a] -> [b]
map (NonNegative Int -> Word64 -> TestBlock
`mkTestBlock` Word64
0) (NonNegative Int
xNonNegative Int -> [NonNegative Int] -> [NonNegative Int]
forall a. a -> [a] -> [a]
:[NonNegative Int]
xs)
     in
      case [TestBlock]
-> TestBlock
-> Either (HeaderError TestBlock) (HeaderState TestBlock)
validateHeaderBlocks [TestBlock]
blks (NonNegative Int -> Word64 -> TestBlock
mkTestBlock NonNegative Int
x Word64
1) of
        Left (HeaderEnvelopeError CheckpointMismatch{})  -> Bool -> Property
forall prop. Testable prop => prop -> Property
QC.property Bool
True
        Left HeaderError TestBlock
e  ->
          TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample TestName
"checkpoint mismatches should be rejected with CheckpointMismatched" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (HeaderError TestBlock -> TestName
forall a. Show a => a -> TestName
show HeaderError TestBlock
e) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          Bool -> Property
forall prop. Testable prop => prop -> Property
QC.property Bool
False
        Right HeaderState TestBlock
_ ->
          TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample TestName
"checkpoint mismatches should be rejected" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          Bool -> Property
forall prop. Testable prop => prop -> Property
QC.property Bool
False