content: {-# LANGUAGE BangPatterns #-}
  {-# LANGUAGE CPP #-}
  {-# LANGUAGE DeriveGeneric #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE LambdaCase #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  
  -- |
  -- Module: Chainweb.BlockHeader.Validation
  -- Copyright: Copyright © 2018 - 2020 Kadena LLC.
  -- License: MIT
  -- Maintainer: Lars Kuhtz <lars@kadena.io>
  -- Stability: experimental
  --
  -- Block Header Validation
  --
  module Chainweb.BlockHeader.Validation
  (
  -- * Validated BockHeaders
    ValidatedHeader
  , _validatedHeader
  , ValidatedHeaders
  , _validatedHeaders
  
  -- * Input Data Types for Validation Functions
  -- $params
  , InvalidValidationParameters(..)
  , ChainStep
  , chainStep
  , _chainStepParent
  , _chainStepHeader
  , WebStep
  , webStep
  , _webStepAdjs
  , _webStepChain
  , _webStepParent
  , _webStepHeader
  
  -- * Validation Failures
  , ValidationFailure(..)
  , ValidationFailureType(..)
  , chainStepFailure
  , webStepFailure
  , definiteValidationFailures
  , isDefinite
  , ephemeralValidationFailures
  , isEphemeral
  
  -- * Top-level Validaton Functions
  , validateBlockHeaderM
  , validateBlockHeadersM
  
  -- * Partial validation functions
  --
  -- | For failing fast during cut validation
  , validateIntrinsicM
  , validateInductiveChainM
  
  -- * Validation of Input Parameters
  , validateBlockParentExists
  , validateAllParentsExist
  
  -- * Pure Top-level Validation functions
  , validateBlockHeader
  , isValidBlockHeader
  
  -- * Collections of Validation Properties
  , validateIntrinsic
  , validateInductive
  , validateInductiveChainStep
  , validateInductiveWebStep
  
  -- * Intrinsic BlockHeader Properties
  , prop_block_pow
  , prop_block_hash
  , prop_block_genesis_parent
  , prop_block_genesis_target
  , prop_block_target
  , prop_block_featureFlags
  
  -- * Inductive BlockHeader Properties
  , prop_block_epoch
  , prop_block_height
  , prop_block_weight
  , prop_block_chainwebVersion
  , prop_block_chainId
  , prop_block_creationTime
  , prop_block_adjacent_chainIds
  , prop_block_adjacent_parents_version
  ) where
  
  import Control.Lens
  import Control.Monad
  import Control.Monad.Catch
  import Control.Monad.Except
  import Control.Monad.Trans.Class
  
  import Data.Foldable
  import qualified Data.HashMap.Strict as HM
  import qualified Data.List as L
  import Data.Maybe (isJust)
  import qualified Data.Text as T
  
  import GHC.Generics
  
  -- internal modules
  
  import Chainweb.BlockCreationTime
  import Chainweb.BlockHash
  import Chainweb.BlockHeader
  import Chainweb.ChainId
  import Chainweb.ChainValue
  import Chainweb.Difficulty
  import Chainweb.Time
  import Chainweb.Utils
  import Chainweb.Version
  import Chainweb.Version.Guards
  
  -- -------------------------------------------------------------------------- --
  -- Validated BockHeader
  
  -- NOTE: the constructor of this type is intentionally NOT exported. Value of
  -- this type must be only created via functions from this module.
  --
  newtype ValidatedHeader = ValidatedHeader BlockHeader
      deriving (Show, Eq, Ord, Generic)
  
  instance HasChainId ValidatedHeader where
      _chainId = _chainId . _validatedHeader
      {-# INLINE _chainId #-}
  
  instance HasChainwebVersion ValidatedHeader where
      _chainwebVersion = _chainwebVersion . _validatedHeader
      {-# INLINE _chainwebVersion #-}
  
  instance HasChainGraph ValidatedHeader where
      _chainGraph = _chainGraph . _validatedHeader
      {-# INLINE _chainGraph #-}
  
  _validatedHeader :: ValidatedHeader -> BlockHeader
  _validatedHeader (ValidatedHeader h) = h
  {-# INLINE _validatedHeader #-}
  
  -- | Values of this type witness that a set of BlockHeaders has been validated for
  -- the properties defined in this module.
  --
  -- This includes all intrinsic and inductive block header properties. It does
  -- not include pact payload validation and cut validation.
  --
  -- The validation holds with respect to an implicit block header db, that is
  -- represented by a header lookup function in some functions in this module.
  --
  -- The validation of block headers is witnessed only for the group of headers and
  -- may not hold for the members of the set alone. If the headers are inserted
  -- in the block header db, they must be inserted all together.
  --
  -- NOTE: the constructor of this type is intentionally NOT exported. Value of
  -- this type must be only created via functions from this module.
  --
  newtype ValidatedHeaders = ValidatedHeaders (HM.HashMap BlockHash BlockHeader)
      deriving (Show, Eq, Ord, Generic)
  
  _validatedHeaders :: ValidatedHeaders -> HM.HashMap BlockHash BlockHeader
  _validatedHeaders (ValidatedHeaders hs) = hs
  {-# INLINE _validatedHeaders #-}
  
  -- -------------------------------------------------------------------------- --
  -- Input Data Types for Validation Functions
  
  -- $params
  -- Values of these types are witnesses for properties of parameters of the
  -- validation functions at runtime.
  --
  -- Usage of values of these types is sound only when they are constructed via
  -- the respective smart constructors.
  --
  
  data InvalidValidationParameters
      = InvalidChainStepParameters ParentHeader BlockHeader
      | InvalidWebStepParameters (HM.HashMap ChainId ParentHeader) ChainStep
      deriving (Show, Eq, Ord, Generic)
  
  instance Exception InvalidValidationParameters where
      displayException (InvalidChainStepParameters p b) =
          "Invalid block header validation parameters for ChainStep: " <> sshow p <> ", " <> sshow b
      displayException (InvalidWebStepParameters p s) =
          "Invalid block header validation parameters for WebStep: " <> sshow p <> ", " <> sshow s
  
  -- | Witnesses at runtime that
  --
  -- prop> \(ChainStep p h) -> view blockParent h == view blockHash p
  --
  -- NOTE: the constructor of this type is intentionally NOT exported.
  --
  data ChainStep = ChainStep ParentHeader BlockHeader
      deriving (Show, Eq, Ord, Generic)
  
  _chainStepParent :: ChainStep -> ParentHeader
  _chainStepParent (ChainStep p _) = p
  {-# INLINE _chainStepParent #-}
  
  _chainStepHeader :: ChainStep -> BlockHeader
  _chainStepHeader (ChainStep _ h) = h
  {-# INLINE _chainStepHeader #-}
  
  chainStep
      :: MonadThrow m
      => ParentHeader
          -- ^ Parent block header. The genesis header is considered its own parent.
      -> BlockHeader
          -- ^ Block header under scrutiny
      -> m ChainStep
  chainStep p b
      | view blockParent b == view blockHash (_parentHeader p)
          = return $ ChainStep p b
      | otherwise = throwM $ InvalidChainStepParameters p b
  
  -- | Witnesses at runtime that
  --
  -- prop> \(WebStep as (ChainStep _ h)) -> and $ HM.zipWith ((==) . view blockHash) as (view blockAdjacentHashes h)
  --
  -- It doesn't witness that @as@ is of the same size as @_blockAdjacentHashes
  -- h@ or that @_blockAdjacentHashes h@ covers all adjacent chains.
  --
  -- NOTE: the constructor of this type is intentionally NOT exported.
  --
  data WebStep = WebStep (HM.HashMap ChainId ParentHeader) ChainStep
      deriving (Show, Eq, Ord, Generic)
  
  webStep
      :: MonadThrow m
      => HM.HashMap ChainId ParentHeader
      -> ChainStep
      -> m WebStep
  webStep as hp@(ChainStep _ h) = WebStep
      <$> itraverse f hashes
      <*> pure hp
    where
      hashes :: HM.HashMap ChainId BlockHash
      hashes = view (blockAdjacentHashes . getBlockHashRecord) h
      f cid a = case HM.lookup cid as of
          Nothing -> throwM $ InvalidWebStepParameters as hp
          Just x
              | view blockHash (_parentHeader x) == a -> return x
              | otherwise -> throwM $ InvalidWebStepParameters as hp
  
  _webStepAdjs :: WebStep -> HM.HashMap ChainId ParentHeader
  _webStepAdjs (WebStep as _) = as
  {-# INLINE _webStepAdjs #-}
  
  _webStepChain :: WebStep -> ChainStep
  _webStepChain (WebStep _ p) = p
  {-# INLINE _webStepChain #-}
  
  _webStepHeader :: WebStep -> BlockHeader
  _webStepHeader (WebStep _ p) = _chainStepHeader p
  {-# INLINE _webStepHeader #-}
  
  _webStepParent :: WebStep -> ParentHeader
  _webStepParent (WebStep _ p) = _chainStepParent p
  {-# INLINE _webStepParent #-}
  
  -- -------------------------------------------------------------------------- --
  -- BlockHeader Validation Failures
  
  -- | A data type that describes a failure of validating a block header.
  --
  data ValidationFailure = ValidationFailure
      { _validateFailureParent :: !(Maybe ParentHeader)
      , _validateFailureAdjecents :: !(Maybe (HM.HashMap ChainId ParentHeader))
      , _validateFailureHeader :: !BlockHeader
      , _validationFailureFailures :: ![ValidationFailureType]
      }
  
  chainStepFailure :: ChainStep -> [ValidationFailureType] -> ValidationFailure
  chainStepFailure hp = ValidationFailure
      (Just $ _chainStepParent hp)
      Nothing
      (_chainStepHeader hp)
  
  webStepFailure :: WebStep -> [ValidationFailureType] -> ValidationFailure
  webStepFailure hp = ValidationFailure
      (Just $ _webStepParent hp)
      (Just $ _webStepAdjs hp)
      (_webStepHeader hp)
  
  instance Show ValidationFailure where
      show (ValidationFailure p as e ts)
          = T.unpack $ "Validation failure"
              <> ". Description: " <> T.unlines (map description ts)
              <> ". Header: " <> encodeToText (ObjectEncoded e)
              <> maybe "" (\p' -> ". Parent: " <> encodeToText (ObjectEncoded $ _parentHeader p')) p
              <> maybe "" (\as' -> ". Adjacents: " <> encodeToText (ObjectEncoded . _parentHeader <$> as')) as
        where
          description t = case t of
              MissingParent -> "Parent isn't in the database"
              MissingAdjacentParent -> "AdjacentParent isn't in the database"
              CreatedBeforeParent -> "Block claims to have been created before its parent"
              VersionMismatch -> "Block uses a version of chainweb different from its parent"
              AdjacentChainMismatch -> "Block uses the wrong set of adjacent chain ids"
              ChainMismatch -> "Block uses a chaind-id different from its parent"
              AdjacentParentChainMismatch -> "An adjacent parent hash references a block on the wrong chain"
              IncorrectHash -> "The hash of the block header does not match the one given"
              IncorrectPow -> "The POW hash does not match the POW target of the block"
              IncorrectEpoch -> "The epoch start time of the block is incorrect"
              IncorrectHeight -> "The given height is not one more than the parent height"
              IncorrectWeight -> "The given weight is not the sum of the difficulty target and the parent's weight"
              IncorrectTarget -> "The given target for the block is incorrect for its history"
              IncorrectGenesisParent -> "The block is a genesis block, but doesn't have its parent set to its own hash"
              IncorrectGenesisTarget -> "The block is a genesis block, but doesn't have the correct difficulty target"
              BlockInTheFuture -> "The creation time of the block is in the future"
              IncorrectPayloadHash -> "The payload hash does not match the payload hash that results from payload validation"
              MissingPayload -> "The payload of the block is missing"
              InvalidFeatureFlags -> "The block has an invalid feature flag value"
              InvalidBraiding -> "The block is not braided correctly into the chainweb"
              InvalidAdjacentVersion -> "An adjancent parent has a chainweb version that does not match the version of the validated header"
  
  -- | An enumeration of possible validation failures for a block header.
  --
  data ValidationFailureType
      = MissingParent
          -- ^ Parent isn't in the database.
      | MissingAdjacentParent
          -- ^ Adjacent Parent isn't in the database.
      | CreatedBeforeParent
          -- ^ Claims to be created at a time prior to its parent's creation.
      | VersionMismatch
          -- ^ Claims to use a version of chainweb different from that of its
          -- parent.
      | ChainMismatch
          -- ^ Claims to use a chain-id different from that of its parent.
      | AdjacentChainMismatch
          -- ^ The block uses the wrong set of adjacent chain ids.
      | AdjacentParentChainMismatch
          -- ^ An adajacent parent hash references a block on the wrong chain.
      | IncorrectHash
          -- ^ The hash of the header properties as computed by computeBlockHash
          -- does not match the hash given in the header.
      | IncorrectPow
          -- ^ The POW hash of the header does not match the POW target of the
          -- block.
      | IncorrectHeight
          -- ^ The given height is not one more than the parent height.
      | IncorrectWeight
          -- ^ The given weight is not the sum of the target difficulty and the
          -- parent's weight.
      | IncorrectTarget
          -- ^ The given target of the block is not correct. The target of the
          -- first block of an epoch is the adjusted target of the previous epoch.
          -- For all other blocks the target equals the target of the parent
          -- block.
      | IncorrectEpoch
          -- ^ The epoch start time value of the block is incorrect. The epoch
          -- start time of the first block of an epoch equals the block creation
          -- time of the parent block. For all other blocks the epoch start time
          -- equls the epoch start time of the parent block.
      | IncorrectGenesisParent
          -- ^ The block is a genesis block, but doesn't have its parent set to
          -- its own hash.
      | IncorrectGenesisTarget
          -- ^ The block is a genesis block, but doesn't have the correct
          -- POW target.
      | BlockInTheFuture
          -- ^ The creation time of the block is in the future.
      | IncorrectPayloadHash
          -- ^ The validation of the payload hash failed.
      | MissingPayload
          -- ^ The payload for the block is missing.
      | InvalidFeatureFlags
          -- ^ The block has an invalid feature flag setting.
      | InvalidBraiding
          -- ^ The block is not braided correctly into the chainweb.
      | InvalidAdjacentVersion
          -- ^ An adjacent parent has chainweb version that does not match the
          -- version of the validated header.
    deriving (Show, Eq, Ord)
  
  instance Exception ValidationFailure
  
  -- | The list of validation failures that are definite and independent of any
  -- external context. A block for which validation fails with one of these
  -- failures must be dicarded.
  --
  -- No node on the chainweb-web network should propgate blocks with these
  -- failures. If a block is received that causes a definite validation failures
  -- is receveived from a chainweb-node, that chainweb-node should be
  -- blacklisted/removed in the peer database.
  --
  definiteValidationFailures :: [ValidationFailureType]
  definiteValidationFailures =
      [ CreatedBeforeParent
      , VersionMismatch
      , ChainMismatch
      , IncorrectHash
      , IncorrectPow
      , IncorrectHeight
      , IncorrectWeight
      , IncorrectTarget
      , IncorrectEpoch
      , IncorrectGenesisParent
      , IncorrectGenesisTarget
      , IncorrectPayloadHash
      ]
  
  -- | Predicate that checks whether a validation failure is definite.
  --
  isDefinite :: [ValidationFailureType] -> Bool
  isDefinite failures
      = not . null $ L.intersect failures definiteValidationFailures
  
  -- | The list of ephemaral validation failures. These failure depend on a local
  -- context and validation may succeed in the future.
  --
  -- In case of 'BlockInTheFuture' validation /will/ eventually succeed.
  --
  ephemeralValidationFailures :: [ValidationFailureType]
  ephemeralValidationFailures =
      [ MissingParent
      , MissingAdjacentParent
      , MissingPayload
      , BlockInTheFuture
      ]
  
  -- | A predicate that checks whether a validation failure is ephemeral.
  --
  isEphemeral :: [ValidationFailureType] -> Bool
  isEphemeral failures
      = not . null $ L.intersect failures ephemeralValidationFailures
  
  -- -------------------------------------------------------------------------- --
  -- Top Level Validation Functions
  
  -- | Validate properties of the block header, throwing an exception detailing
  -- the failures if any.
  --
  -- This doesn't include checks for
  --
  -- * MissingPayload
  -- * MissingParent
  -- * IncorrectPayloadHash
  --
  validateBlockHeaderM
      :: MonadThrow m
      => Time Micros
          -- ^ The current clock time
      -> (ChainValue BlockHash -> m (Maybe BlockHeader))
          -- ^ Context of Validated BlockHeaders
      -> BlockHeader
      -> m ValidatedHeader
  validateBlockHeaderM t lookupHeader h =
      validateAllParentsExist lookupHeader h >>= \case
          Left e -> throwM $ ValidationFailure
              { _validateFailureParent = Nothing
              , _validateFailureAdjecents = Nothing
              , _validateFailureHeader = h
              , _validationFailureFailures = [e]
              }
          Right ws -> do
              let failures = validateBlockHeader t ws
              unless (null failures) $ throwM $ webStepFailure ws failures
              return $ ValidatedHeader h
  
  -- | Validate a set of blocks that may depend on each other.
  --
  -- This doesn't include checks for
  --
  -- * MissingPayload
  -- * IncorrectPayloadHash
  --
  validateBlockHeadersM
      :: MonadThrow m
      => Time Micros
          -- ^ The current clock time
      -> (ChainValue BlockHash -> m (Maybe BlockHeader))
          -- ^ Context of Validated BlockHeaders
      -> HM.HashMap BlockHash BlockHeader
      -> m ValidatedHeaders
  validateBlockHeadersM t lookupHeader as = do
      traverse_ (validateBlockHeaderM t lookupHeader') as
      return $ ValidatedHeaders as
    where
      lookupHeader' h = case HM.lookup (_chainValueValue h) as of
          Just p -> return (Just p)
          Nothing -> lookupHeader h
  
  -- -------------------------------------------------------------------------- --
  -- Partial Top-Level Validation Functions
  --
  -- These functions don't return ValidatedHeaders, so the result doesn't qualify
  -- the validated header to be inserted in the the chain database.
  
  -- | Only validate intrinsic properties of the block header, throwing an
  -- exception detailing the failures if any.
  --
  -- This doesn't return 'ValidatedHeaders' because no complete validation is
  -- performed
  --
  validateIntrinsicM
      :: MonadThrow m
      => Time Micros
          -- ^ The current clock time
      -> BlockHeader
          -- ^ The block header to be checked
      -> m ()
  validateIntrinsicM t e = unless (null failures)
      $ throwM (ValidationFailure Nothing Nothing e failures)
    where
      failures = validateIntrinsic t e
  
  -- | Only validate inductive properties of the block header, throwing an
  -- exception detailing the failures if any.
  --
  -- This doesn't return 'ValidatedHeaders' because no complete validation is
  -- performed
  --
  validateInductiveChainM
      :: MonadThrow m
      => (BlockHash -> m (Maybe BlockHeader))
          -- ^ Context of Validated BlockHeaders
      -> BlockHeader
      -> m ()
  validateInductiveChainM lookupHeader h =
      validateBlockParentExists lookupHeader h >>= \case
          Left e -> throwM $ ValidationFailure
              { _validateFailureParent = Nothing
              , _validateFailureAdjecents = Nothing
              , _validateFailureHeader = h
              , _validationFailureFailures = [e]
              }
          Right cs -> do
              let failures = validateInductiveChainStep cs
              unless (null failures) $ throwM $ chainStepFailure cs failures
  
  -- -------------------------------------------------------------------------- --
  -- Validation of Input Parameters
  
  -- | Validate that the parent exist with the given lookup function.
  --
  -- Returns the parent if it exists or an validation failure otherwise.
  --
  validateBlockParentExists
      :: Monad m
      => (BlockHash -> m (Maybe BlockHeader))
      -> BlockHeader
      -> m (Either ValidationFailureType ChainStep)
  validateBlockParentExists lookupParent h
      | isGenesisBlockHeader h = return $ Right $ ChainStep (ParentHeader h) h
      | otherwise = lookupParent (view blockParent h) >>= \case
          (Just !p) -> return $ Right $ ChainStep (ParentHeader p) h
          Nothing -> return $ Left MissingParent
  
  -- | Validate that the parent and all adjacent parents exist with the given
  -- lookup function.
  --
  -- Returns the parents if they exist or an validation failure otherwise.
  --
  validateAllParentsExist
      :: Monad m
      => (ChainValue BlockHash -> m (Maybe BlockHeader))
      -> BlockHeader
      -> m (Either ValidationFailureType WebStep)
  validateAllParentsExist lookupParent h = runExceptT $ WebStep
      <$> itraverse f (view (blockAdjacentHashes . getBlockHashRecord) h)
      <*> ExceptT (validateBlockParentExists lookupOnChain h)
    where
      lookupOnChain = lookupParent . ChainValue (_chainId h)
      v = _chainwebVersion h
      f c ph
          | genesisParentBlockHash v c == ph = return
              $ ParentHeader $ genesisBlockHeader v c
          | otherwise = lift (lookupParent $ ChainValue c ph) >>= \case
              (Just !p) -> return $ ParentHeader p
              Nothing -> throwError MissingAdjacentParent
  
  -- -------------------------------------------------------------------------- --
  -- Pure Top Level Validation Functions
  
  -- | Check whether a BlockHeader satisfies all validaiton properties.
  --
  -- This doesn't include checks for
  --
  -- * MissingPayload
  -- * MissingParent
  -- * IncorrectPayloadHash
  --
  isValidBlockHeader
      :: Time Micros
          -- ^ The current clock time
      -> WebStep
      -> Bool
  isValidBlockHeader t p = null $ validateBlockHeader t p
  
  -- | Validate properties of the block header, producing a list of the validation
  -- failures.
  --
  -- This doesn't include checks for
  --
  -- * MissingPayload
  -- * MissingParent
  -- * IncorrectPayloadHash
  --
  validateBlockHeader
      :: Time Micros
          -- ^ The current clock time
      -> WebStep
      -> [ValidationFailureType]
          -- ^ A list of ways in which the block header isn't valid
  validateBlockHeader t p
      = validateIntrinsic t (_webStepHeader p)
      <> validateInductive p
  
  -- -------------------------------------------------------------------------- --
  -- Collections of Validation Properties
  
  -- | Validates properties of a block which are checkable from the block header
  -- without observing the remainder of the database.
  --
  validateIntrinsic
      :: Time Micros
          -- ^ The current clock time
      -> BlockHeader
          -- ^ block header to be validated
      -> [ValidationFailureType]
          -- ^ A list of ways in which the block header isn't valid
  validateIntrinsic t b = concat
      [ [ IncorrectHash | not (prop_block_hash b) ]
      , [ IncorrectPow | not (prop_block_pow b) ]
      , [ IncorrectGenesisParent | not (prop_block_genesis_parent b)]
      , [ IncorrectGenesisTarget | not (prop_block_genesis_target b)]
      , [ BlockInTheFuture | not (prop_block_current t b)]
      , [ InvalidFeatureFlags | not (prop_block_featureFlags b)]
      , [ AdjacentChainMismatch | not (prop_block_adjacent_chainIds b) ]
      ]
  
  -- | Validate properties of a block with respect to a given parent.
  --
  validateInductive
      :: WebStep
      -> [ValidationFailureType]
          -- ^ A list of ways in which the block header isn't valid
  validateInductive ps
      = validateInductiveChainStep (_webStepChain ps)
      <> validateInductiveWebStep ps
  
  validateInductiveChainStep
      :: ChainStep
          -- ^ parent block header. The genesis header is considered its own parent.
      -> [ValidationFailureType]
          -- ^ A list of ways in which the block header isn't valid
  validateInductiveChainStep s = concat
      [ [ IncorrectHeight | not (prop_block_height s) ]
      , [ VersionMismatch | not (prop_block_chainwebVersion s) ]
      , [ IncorrectWeight | not (prop_block_weight s) ]
      , [ ChainMismatch | not (prop_block_chainId s) ]
      ]
  
  validateInductiveWebStep
      :: WebStep
          -- ^ parent block header. The genesis header is considered its own parent.
      -> [ValidationFailureType]
          -- ^ A list of ways in which the block header isn't valid
  validateInductiveWebStep s = concat
      [ [ IncorrectEpoch | not (prop_block_epoch s) ]
      , [ IncorrectTarget | not (prop_block_target s) ]
      , [ CreatedBeforeParent | not (prop_block_creationTime s) ]
      , [ AdjacentParentChainMismatch | not (prop_block_adjacent_parents s) ]
      , [ InvalidBraiding | not (prop_block_braiding s) ]
      , [ InvalidAdjacentVersion | not (prop_block_adjacent_parents_version s) ]
      ]
  
  -- -------------------------------------------------------------------------- --
  -- Intrinsic BlockHeader properties
  -- -------------------------------------------------------------------------- --
  
  prop_block_pow :: BlockHeader -> Bool
  prop_block_pow b
      | isGenesisBlockHeader b = True
      -- Genesis block headers are not mined. So there's not need for POW
      | b ^. chainwebVersion . versionCheats . disablePow = True
      | otherwise = checkTarget (view blockTarget b) (view blockPow b)
  
  prop_block_hash :: BlockHeader -> Bool
  prop_block_hash b = view blockHash b == computeBlockHash b
  
  prop_block_genesis_parent :: BlockHeader -> Bool
  prop_block_genesis_parent b
      = isGenesisBlockHeader b ==> hasGenesisParentHash b
      && hasGenesisParentHash b ==> isGenesisBlockHeader b
    where
      hasGenesisParentHash b' =
          view blockParent b' == genesisParentBlockHash (_chainwebVersion b') (_chainId b')
  
  prop_block_genesis_target :: BlockHeader -> Bool
  prop_block_genesis_target b = isGenesisBlockHeader b
      ==> view blockTarget b == _chainwebVersion b ^?! versionGenesis . genesisBlockTarget . atChain (_chainId b)
  
  prop_block_current :: Time Micros -> BlockHeader -> Bool
  prop_block_current t b = BlockCreationTime t >= view blockCreationTime b
  
  prop_block_featureFlags :: BlockHeader -> Bool
  prop_block_featureFlags b
      | skipFeatureFlagValidationGuard v cid h = True
      | otherwise = view blockFlags b == mkFeatureFlags
    where
      v = _chainwebVersion b
      h = view blockHeight b
      cid = _chainId b
  
  -- | Verify that the adjacent hashes of the block are for the correct set of
  -- chain ids.
  --
  prop_block_adjacent_chainIds :: BlockHeader -> Bool
  prop_block_adjacent_chainIds b
      = isJust $ checkAdjacentChainIds adjGraph b (Expected $ view blockAdjacentChainIds b)
    where
      adjGraph
          | isGenesisBlockHeader b = _chainGraph b
          | otherwise = chainGraphAt (_chainwebVersion b) (view blockHeight b - 1)
  
  -- -------------------------------------------------------------------------- --
  -- Inductive BlockHeader Properties
  -- -------------------------------------------------------------------------- --
  
  -- -------------------------------------------------------------------------- --
  -- Single chain inductive properties
  
  prop_block_height :: ChainStep -> Bool
  prop_block_height (ChainStep (ParentHeader p) b)
      | isGenesisBlockHeader b = view blockHeight b == view blockHeight p
      | otherwise = view blockHeight b == view blockHeight p + 1
  
  prop_block_chainwebVersion :: ChainStep -> Bool
  prop_block_chainwebVersion (ChainStep (ParentHeader p) b) =
      view blockChainwebVersion p == view blockChainwebVersion b
  
  prop_block_weight :: ChainStep -> Bool
  prop_block_weight (ChainStep (ParentHeader p) b)
      | isGenesisBlockHeader b = view blockWeight b == view blockWeight p
      | otherwise = view blockWeight b == expectedWeight
    where
      expectedWeight = int (targetToDifficulty (view blockTarget b)) + view blockWeight p
  
  prop_block_chainId :: ChainStep -> Bool
  prop_block_chainId (ChainStep (ParentHeader p) b)
      = view blockChainId p == view blockChainId b
  
  -- -------------------------------------------------------------------------- --
  -- Multi chain inductive properties
  
  prop_block_target :: WebStep -> Bool
  prop_block_target (WebStep as (ChainStep p b))
      = view blockTarget b == powTarget p as (view blockCreationTime b)
  
  prop_block_epoch :: WebStep -> Bool
  prop_block_epoch (WebStep as (ChainStep p b))
      | oldDaGuard (_chainwebVersion b) (_chainId b) (view blockHeight b)
          = view blockEpochStart b <= EpochStartTime (_bct $ view blockCreationTime b)
          && view blockEpochStart (_parentHeader p) <= view blockEpochStart b
          && view blockEpochStart b == epochStart p as (view blockCreationTime b)
      | otherwise
          = view blockEpochStart b <= EpochStartTime (_bct $ view blockCreationTime b)
          && view blockEpochStart b == epochStart p as (view blockCreationTime b)
  
  prop_block_creationTime :: WebStep -> Bool
  prop_block_creationTime (WebStep as (ChainStep (ParentHeader p) b))
      | isGenesisBlockHeader b
          = view blockCreationTime b == view blockCreationTime p
      | oldDaGuard (_chainwebVersion b) (_chainId b) (view blockHeight b)
          = view blockCreationTime b > view blockCreationTime p
      | otherwise
          = view blockCreationTime b > view blockCreationTime p
          && all (\x -> view blockCreationTime b > view blockCreationTime (_parentHeader x)) as
  
  -- | The chainId index of the adjacent parents of the header and the blocks
  -- in the webstep reference the same hashes and the chain Ids in of the
  -- referenced blocks match the chainIds in the index.
  --
  -- Note that this property is already witnessed by the constructor of WebStep,
  -- we include it here again as assertion (to double check during testing) and
  -- for documentation purposes.
  --
  prop_block_adjacent_parents :: WebStep -> Bool
  prop_block_adjacent_parents (WebStep as (ChainStep _ b))
      | isGenesisBlockHeader b
          = adjsHashes == imap (\cid _ -> genesisParentBlockHash v cid) as
              -- chainId indexes in web adjadent parent record references the
              -- genesis block parent hashes
      | otherwise
          = adjsHashes == (view blockHash . _parentHeader <$> as)
              -- chainId indexes in web adjadent parent record and web step are
              -- referencing the same hashes
          && iall (\cid h -> cid == _chainId h) as
              -- chainIds of adjancent parent header match the chainId under which
              -- it is indexed
    where
      adjsHashes = _getBlockHashRecord (view blockAdjacentHashes b)
      v = _chainwebVersion b
  
  prop_block_adjacent_parents_version :: WebStep -> Bool
  prop_block_adjacent_parents_version (WebStep as (ChainStep _ b))
      = all ((== v) . view blockChainwebVersion . _parentHeader) as
    where
      v = view blockChainwebVersion b
  
  -- | TODO: we don't current check this here. It is enforced in the cut merge
  -- algorithm , namely in 'monotonicCutExtension'. The property that is checked
  -- in the cut validation is stronger than the braiding property that we could
  -- check here (which is the property that is described in the chainweb paper).
  -- So, I check here would add some redundancy, but it's not clear of how much
  -- actual value that would be.
  --
  -- If we want to enforce it here, too, we would have to look back 2 steps in
  -- history.
  --
  prop_block_braiding :: WebStep -> Bool
  prop_block_braiding _ = True
  