{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedLists #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

-- | Test module where we check that the block validation implementation
-- matches the formal specification. To this end, the strategy is:
--
-- 0. generate traces of abstract blocks, which conform to the formal semantics
--    of the blockchain layer
--
-- 1. elaborate these abstract blocks into concrete blocks
--
-- 2. feed the generated sequence of concrete blocks to the block validation
--    function, and check that it passes the validation.
module Test.Cardano.Chain.Block.Model (
  tests,
  elaborateAndUpdate,
  passConcreteValidation,
  elaborateBlock,
)
where

import Byron.Spec.Chain.STS.Block (BlockStats (..))
import qualified Byron.Spec.Chain.STS.Block as Abstract
import Byron.Spec.Chain.STS.Rule.BBody
import Byron.Spec.Chain.STS.Rule.Chain (
  CHAIN,
  isHeaderSizeTooBigFailure,
 )
import qualified Byron.Spec.Ledger.Core as AbstractCore
import Byron.Spec.Ledger.Delegation (
  _dIStateDelegationMap,
 )
import Byron.Spec.Ledger.Update (
  PParams,
  UPIEnv,
  UPIState,
  _maxBkSz,
  _maxHdrSz,
 )
import Cardano.Chain.Block (
  ABlock,
  BlockValidationMode (..),
  ChainValidationError (
    ChainValidationBlockTooLarge,
    ChainValidationHeaderTooLarge
  ),
  ChainValidationState (cvsUtxo),
  blockHeader,
  blockLength,
  cvsUpdateState,
  headerLength,
  initialChainValidationState,
  updateBlock,
 )
import Cardano.Chain.Common (unBlockCount)
import qualified Cardano.Chain.Genesis as Genesis
import Cardano.Chain.Update (
  ProtocolParameters,
  ppMaxBlockSize,
  ppMaxHeaderSize,
 )
import Cardano.Chain.Update.Validation.Interface (adoptedProtocolParameters)
import Cardano.Chain.ValidationMode (
  ValidationMode,
  fromBlockValidationMode,
 )
import Cardano.Prelude hiding (State, state, trace)
import Control.State.Transition (
  Environment,
  PredicateFailure,
  Signal,
  State,
  TRC (TRC),
  applySTS,
 )
import qualified Data.Set as Set
import Data.String (fromString)
import Hedgehog (
  Gen,
  MonadTest,
  PropertyT,
  TestLimit,
  assert,
  collect,
  cover,
  evalEither,
  failure,
  footnote,
  forAll,
  label,
  property,
  success,
 )
import qualified Hedgehog.Gen as Gen
import qualified Hedgehog.Range as Range
import Lens.Micro ((^.))
import Test.Cardano.Chain.Elaboration.Block (
  AbstractToConcreteIdMaps,
  abEnvToCfg,
  elaborateBS,
  rcDCert,
  transactionIds,
 )
import Test.Cardano.Chain.Elaboration.Keys (elaborateVKeyGenesisHash)
import Test.Cardano.Chain.UTxO.Model (elaborateInitialUTxO)
import Test.Cardano.Prelude
import Test.Control.State.Transition.Generator (
  SignalGenerator,
  classifyTraceLength,
  invalidTrace,
  ofLengthAtLeast,
  trace,
 )
import qualified Test.Control.State.Transition.Invalid.Trace as Invalid.Trace
import Test.Control.State.Transition.Trace (
  Trace,
  TraceOrder (NewestFirst, OldestFirst),
  extractValues,
  lastSignal,
  lastState,
  preStatesAndSignals,
  traceEnv,
  traceInit,
  traceSignals,
  _traceEnv,
 )
import Test.Options (TSGroup, TSProperty, withTestsTS)
import Prelude (String)

tests :: TSGroup
tests :: TSGroup
tests = $$discoverPropArg

-- | Every abstract chain that was generated according to the inference rules,
-- after being elaborated must be validated by the concrete block validator.
ts_prop_generatedChainsAreValidated :: TSProperty
ts_prop_generatedChainsAreValidated :: TSProperty
ts_prop_generatedChainsAreValidated =
  TestLimit -> Property -> TSProperty
withTestsTS TestLimit
300
    forall a b. (a -> b) -> a -> b
$ HasCallStack => PropertyT IO () -> Property
property
    forall a b. (a -> b) -> a -> b
$ do
      let (Word64
traceLength, Word64
step) = (Word64
200 :: Word64, Word64
10 :: Word64)
      Trace CHAIN
tr <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall s. HasTrace s => BaseEnv s -> Word64 -> Gen (Trace s)
trace @CHAIN () Word64
traceLength
      forall s. Trace s -> Word64 -> Word64 -> PropertyT IO ()
classifyTraceLength Trace CHAIN
tr Word64
traceLength Word64
step
      Maybe (BlockStats, BlockStats, BlockStats) -> PropertyT IO ()
classifyBlockStats
        forall a b. (a -> b) -> a -> b
$ [BlockStats] -> Maybe (BlockStats, BlockStats, BlockStats)
Abstract.chainBlockStats
        forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map Block -> BlockStats
Abstract.blockStats (forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace CHAIN
tr)
      forall (m :: * -> *). MonadTest m => Trace CHAIN -> m ()
printAdditionalInfoOnFailure Trace CHAIN
tr
      forall (m :: * -> *). MonadTest m => Trace CHAIN -> m ()
passConcreteValidation Trace CHAIN
tr
  where
    printAdditionalInfoOnFailure :: MonadTest m => Trace CHAIN -> m ()
    printAdditionalInfoOnFailure :: forall (m :: * -> *). MonadTest m => Trace CHAIN -> m ()
printAdditionalInfoOnFailure Trace CHAIN
tr =
      forall (m :: * -> *). MonadTest m => String -> m ()
footnote forall a b. (a -> b) -> a -> b
$ String
"Allowed delegators hashes: " forall a. [a] -> [a] -> [a]
++ forall a b. (Show a, ConvertText String b) => a -> b
show [KeyHash]
allowedDelegatorHashes
      where
        allowedDelegatorHashes :: [KeyHash]
allowedDelegatorHashes = VKeyGenesis -> KeyHash
elaborateVKeyGenesisHash forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Set a -> [a]
Set.toList Set VKeyGenesis
allowedDelegators
        (Slot
_, UTxO
_, Set VKeyGenesis
allowedDelegators, PParams
_, BlockCount
_) = forall s. Trace s -> Environment s
_traceEnv Trace CHAIN
tr

classifyBlockStats ::
  Maybe (BlockStats, BlockStats, BlockStats) ->
  PropertyT IO ()
classifyBlockStats :: Maybe (BlockStats, BlockStats, BlockStats) -> PropertyT IO ()
classifyBlockStats Maybe (BlockStats, BlockStats, BlockStats)
Nothing = forall (m :: * -> *) a. Monad m => a -> m a
return ()
classifyBlockStats (Just (BlockStats
sMin, BlockStats
sMax, BlockStats
sAvg)) = do
  String -> BlockStats -> (BlockStats -> Word) -> PropertyT IO ()
classify' String
"min # tx" BlockStats
sMin BlockStats -> Word
Abstract.blockStatsUtxo
  String -> BlockStats -> (BlockStats -> Word) -> PropertyT IO ()
classify' String
"max # tx" BlockStats
sMax BlockStats -> Word
Abstract.blockStatsUtxo
  String -> BlockStats -> (BlockStats -> Word) -> PropertyT IO ()
classify' String
"avg # tx" BlockStats
sAvg BlockStats -> Word
Abstract.blockStatsUtxo

  String -> BlockStats -> (BlockStats -> Word) -> PropertyT IO ()
classify' String
"min # dcert" BlockStats
sMin BlockStats -> Word
Abstract.blockStatsDCerts
  String -> BlockStats -> (BlockStats -> Word) -> PropertyT IO ()
classify' String
"max # dcert" BlockStats
sMax BlockStats -> Word
Abstract.blockStatsDCerts
  String -> BlockStats -> (BlockStats -> Word) -> PropertyT IO ()
classify' String
"avg # dcert" BlockStats
sAvg BlockStats -> Word
Abstract.blockStatsDCerts

  String -> BlockStats -> (BlockStats -> Word) -> PropertyT IO ()
classify' String
"min # votes" BlockStats
sMin BlockStats -> Word
Abstract.blockStatsUpdVotes
  String -> BlockStats -> (BlockStats -> Word) -> PropertyT IO ()
classify' String
"max # votes" BlockStats
sMax BlockStats -> Word
Abstract.blockStatsUpdVotes
  String -> BlockStats -> (BlockStats -> Word) -> PropertyT IO ()
classify' String
"avg # votes" BlockStats
sAvg BlockStats -> Word
Abstract.blockStatsUpdVotes

  String -> BlockStats -> (BlockStats -> Word) -> PropertyT IO ()
classify' String
"min # prop" BlockStats
sMin BlockStats -> Word
Abstract.blockStatsUpdProp
  String -> BlockStats -> (BlockStats -> Word) -> PropertyT IO ()
classify' String
"max # prop" BlockStats
sMax BlockStats -> Word
Abstract.blockStatsUpdProp
  String -> BlockStats -> (BlockStats -> Word) -> PropertyT IO ()
classify' String
"avg # prop" BlockStats
sAvg BlockStats -> Word
Abstract.blockStatsUpdProp
  where
    classify' :: String -> BlockStats -> (BlockStats -> Word) -> PropertyT IO ()
    classify' :: String -> BlockStats -> (BlockStats -> Word) -> PropertyT IO ()
classify' String
l BlockStats
stats BlockStats -> Word
f
      | BlockStats -> Word
f BlockStats
stats forall a. Eq a => a -> a -> Bool
== Word
0 = forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
LabelName -> m ()
label (forall a. IsString a => String -> a
fromString (String
l forall a. [a] -> [a] -> [a]
++ String
" == 0"))
      | BlockStats -> Word
f BlockStats
stats forall a. Eq a => a -> a -> Bool
== Word
1 = forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
LabelName -> m ()
label (forall a. IsString a => String -> a
fromString (String
l forall a. [a] -> [a] -> [a]
++ String
" == 1"))
      | Bool
otherwise = forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
LabelName -> m ()
label (forall a. IsString a => String -> a
fromString (String
l forall a. [a] -> [a] -> [a]
++ String
" >  1"))

passConcreteValidation :: MonadTest m => Trace CHAIN -> m ()
passConcreteValidation :: forall (m :: * -> *). MonadTest m => Trace CHAIN -> m ()
passConcreteValidation Trace CHAIN
tr = forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) x a.
(MonadTest m, Show x, HasCallStack) =>
Either x a -> m a
evalEither Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
result
  where
    ValidationOutput {Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
result :: ValidationOutput
-> Either
     ChainValidationError
     (ChainValidationState, AbstractToConcreteIdMaps)
result :: Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
result} = Trace CHAIN -> ValidationOutput
applyTrace Trace CHAIN
tr

-- | Elaborate an abstract signal into a concrete one, and apply the validators
-- to the elaborated signal and given concrete state. If the signal was
-- validated, return the next state. Otherwise return an error.
elaborateAndUpdate ::
  Genesis.Config ->
  (ChainValidationState, AbstractToConcreteIdMaps) ->
  (State CHAIN, Abstract.Block) ->
  Either
    ChainValidationError
    (ChainValidationState, AbstractToConcreteIdMaps)
elaborateAndUpdate :: Config
-> (ChainValidationState, AbstractToConcreteIdMaps)
-> (State CHAIN, Block)
-> Either
     ChainValidationError
     (ChainValidationState, AbstractToConcreteIdMaps)
elaborateAndUpdate Config
config (ChainValidationState
cvs, AbstractToConcreteIdMaps
abstractToConcreteIdMaps) (State CHAIN
ast, Block
ab) =
  (,AbstractToConcreteIdMaps
abstractToConcreteIdMaps') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (forall (m :: * -> *).
(MonadError ChainValidationError m,
 MonadReader ValidationMode m) =>
Config
-> ChainValidationState
-> ABlock ByteString
-> m ChainValidationState
updateBlock Config
config ChainValidationState
cvs ABlock ByteString
concreteBlock) ValidationMode
vMode
  where
    (ABlock ByteString
concreteBlock, AbstractToConcreteIdMaps
abstractToConcreteIdMaps') = AbstractToConcreteIdMaps
-> Config
-> DCert
-> ChainValidationState
-> Block
-> (ABlock ByteString, AbstractToConcreteIdMaps)
elaborateBS AbstractToConcreteIdMaps
abstractToConcreteIdMaps Config
config DCert
dCert ChainValidationState
cvs Block
ab

    dCert :: DCert
dCert = HasCallStack => VKey -> BlockCount -> State CHAIN -> DCert
rcDCert (Block
ab forall s a. s -> Getting a s a -> a
^. Lens' Block BlockHeader
Abstract.bHeader forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Lens' BlockHeader VKey
Abstract.bhIssuer) BlockCount
stableAfter State CHAIN
ast

    stableAfter :: BlockCount
stableAfter = Word64 -> BlockCount
AbstractCore.BlockCount forall a b. (a -> b) -> a -> b
$ BlockCount -> Word64
unBlockCount forall a b. (a -> b) -> a -> b
$ Config -> BlockCount
Genesis.configK Config
config

    vMode :: ValidationMode
    vMode :: ValidationMode
vMode = BlockValidationMode -> ValidationMode
fromBlockValidationMode BlockValidationMode
BlockValidation

elaborateBlock ::
  Genesis.Config ->
  ChainValidationState ->
  AbstractToConcreteIdMaps ->
  State CHAIN ->
  Abstract.Block ->
  ABlock ByteString
elaborateBlock :: Config
-> ChainValidationState
-> AbstractToConcreteIdMaps
-> State CHAIN
-> Block
-> ABlock ByteString
elaborateBlock
  Config
config
  ChainValidationState
chainValidationState
  AbstractToConcreteIdMaps
abstractToConcreteIdMaps
  State CHAIN
abstractState
  Block
abstractBlock = ABlock ByteString
concreteBlock
    where
      (ABlock ByteString
concreteBlock, AbstractToConcreteIdMaps
_) =
        AbstractToConcreteIdMaps
-> Config
-> DCert
-> ChainValidationState
-> Block
-> (ABlock ByteString, AbstractToConcreteIdMaps)
elaborateBS
          AbstractToConcreteIdMaps
abstractToConcreteIdMaps
          Config
config
          DCert
dCert
          ChainValidationState
chainValidationState
          Block
abstractBlock
        where
          dCert :: DCert
dCert =
            HasCallStack => VKey -> BlockCount -> State CHAIN -> DCert
rcDCert
              (Block
abstractBlock forall s a. s -> Getting a s a -> a
^. Lens' Block BlockHeader
Abstract.bHeader forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Lens' BlockHeader VKey
Abstract.bhIssuer)
              BlockCount
stableAfter
              State CHAIN
abstractState
            where
              stableAfter :: BlockCount
stableAfter =
                Word64 -> BlockCount
AbstractCore.BlockCount
                  forall a b. (a -> b) -> a -> b
$ BlockCount -> Word64
unBlockCount
                  forall a b. (a -> b) -> a -> b
$ Config -> BlockCount
Genesis.configK Config
config

classifyTransactions :: Trace CHAIN -> PropertyT IO ()
classifyTransactions :: Trace CHAIN -> PropertyT IO ()
classifyTransactions =
  forall (m :: * -> *) a.
(MonadTest m, Show a, HasCallStack) =>
a -> m ()
collect
    forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum
    forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. HasLength a => a -> Int
length forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. BlockBody -> [Tx]
Abstract._bUtxo forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Block -> BlockBody
Abstract._bBody)
    forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
NewestFirst

-- TODO: add coverage testing for delegation.
--
-- TODO: we could establish a mapping between concrete and abstract errors.
--
-- TODO: we want to check that the concrete errors are included in
-- the abstract ones. Currently the concrete implementation
-- short-circuits on the first failure, that's why we can only
-- check inclusion at the moment. To make sure we cover the errors
-- that can arise in the concrete implementation we need to make
-- sure that the invalid generators cover a good deal of abstract
-- errors permutations. So for instance, given abstract errors @X@,
-- @Y@, and @Z@, we would want to generate all combinations of them.

-- | Test that the invalid chains that are generated according to the given
-- failure profile are rejected. On failure agreement the given function is
-- called using the abstract and concrete predicate failures as arguments.
invalidChainTracesAreRejected ::
  TestLimit ->
  [(Int, SignalGenerator CHAIN)] ->
  (NonEmpty (PredicateFailure CHAIN) -> ChainValidationError -> PropertyT IO ()) ->
  TSProperty
invalidChainTracesAreRejected :: TestLimit
-> [(Int, SignalGenerator CHAIN)]
-> (NonEmpty (PredicateFailure CHAIN)
    -> ChainValidationError -> PropertyT IO ())
-> TSProperty
invalidChainTracesAreRejected TestLimit
numberOfTests [(Int, SignalGenerator CHAIN)]
failureProfile NonEmpty (PredicateFailure CHAIN)
-> ChainValidationError -> PropertyT IO ()
onFailureAgreement =
  TestLimit -> Property -> TSProperty
withTestsTS TestLimit
numberOfTests
    forall a b. (a -> b) -> a -> b
$ HasCallStack => PropertyT IO () -> Property
property
    forall a b. (a -> b) -> a -> b
$ do
      let traceLength :: Word64
traceLength = Word64
100 :: Word64
      Trace CHAIN
tr <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall s.
HasTrace s =>
BaseEnv s -> Word64 -> [(Int, SignalGenerator s)] -> Gen (Trace s)
invalidTrace @CHAIN () Word64
traceLength [(Int, SignalGenerator CHAIN)]
failureProfile
      let ValidationOutput {Config
elaboratedConfig :: ValidationOutput -> Config
elaboratedConfig :: Config
elaboratedConfig, Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
result :: Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
result :: ValidationOutput
-> Either
     ChainValidationError
     (ChainValidationState, AbstractToConcreteIdMaps)
result} =
            Trace CHAIN -> ValidationOutput
applyTrace (forall s. Trace s -> Trace s
Invalid.Trace.validPrefix Trace CHAIN
tr)
      case Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
result of
        Left ChainValidationError
error -> do
          forall (m :: * -> *). MonadTest m => String -> m ()
footnote forall a b. (a -> b) -> a -> b
$ String
"Expecting a valid prefix but got: " forall a. [a] -> [a] -> [a]
++ forall a b. (Show a, ConvertText String b) => a -> b
show ChainValidationError
error
          forall (m :: * -> *) a. (MonadTest m, HasCallStack) => m a
failure
        Right (ChainValidationState, AbstractToConcreteIdMaps)
concreteState ->
          let abstractState :: State CHAIN
abstractState = forall s. Trace s -> State s
lastState (forall s. Trace s -> Trace s
Invalid.Trace.validPrefix Trace CHAIN
tr)
              block :: Signal CHAIN
block = forall s. Trace s -> Signal s
Invalid.Trace.signal Trace CHAIN
tr
              result' :: Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
result' =
                Config
-> (ChainValidationState, AbstractToConcreteIdMaps)
-> (State CHAIN, Block)
-> Either
     ChainValidationError
     (ChainValidationState, AbstractToConcreteIdMaps)
elaborateAndUpdate
                  Config
elaboratedConfig
                  (ChainValidationState, AbstractToConcreteIdMaps)
concreteState
                  (State CHAIN
abstractState, Signal CHAIN
block)
           in case (forall s.
Trace s -> Either (NonEmpty (PredicateFailure s)) (State s)
Invalid.Trace.errorOrLastState Trace CHAIN
tr, Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
result') of
                (Right (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
_, Right (ChainValidationState, AbstractToConcreteIdMaps)
_) ->
                  -- Success: it is possible that the invalid signals generator
                  -- produces a valid signal, since the generator is probabilistic.
                  forall (m :: * -> *). MonadTest m => m ()
success
                (Left NonEmpty ChainPredicateFailure
abstractPfs, Left ChainValidationError
concretePfs) -> do
                  -- Success: both the model and the concrete implementation failed
                  -- to validate the signal.
                  --
                  NonEmpty (PredicateFailure CHAIN)
-> ChainValidationError -> PropertyT IO ()
onFailureAgreement NonEmpty ChainPredicateFailure
abstractPfs ChainValidationError
concretePfs
                (Either
  (NonEmpty ChainPredicateFailure)
  (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
abstractResult, Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
concreteResult) -> do
                  forall (m :: * -> *). MonadTest m => String -> m ()
footnote String
"Validation results mismatch."
                  forall (m :: * -> *). MonadTest m => String -> m ()
footnote forall a b. (a -> b) -> a -> b
$ String
"Signal: " forall a. [a] -> [a] -> [a]
++ forall a b. (Show a, ConvertText String b) => a -> b
show Signal CHAIN
block
                  forall (m :: * -> *). MonadTest m => String -> m ()
footnote forall a b. (a -> b) -> a -> b
$ String
"Abstract result: " forall a. [a] -> [a] -> [a]
++ forall a b. (Show a, ConvertText String b) => a -> b
show Either
  (NonEmpty ChainPredicateFailure)
  (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
abstractResult
                  forall (m :: * -> *). MonadTest m => String -> m ()
footnote forall a b. (a -> b) -> a -> b
$ String
"Concrete result: " forall a. [a] -> [a] -> [a]
++ forall a b. (Show a, ConvertText String b) => a -> b
show Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
concreteResult
                  forall (m :: * -> *) a. (MonadTest m, HasCallStack) => m a
failure

-- | Extract the update interface environment from a given block and chain
-- environment and state.
--
-- TODO: this should be in `cardano-ledger`.
mkUpiEnv ::
  Abstract.Block ->
  Environment CHAIN ->
  State CHAIN ->
  UPIEnv
mkUpiEnv :: Block -> Environment CHAIN -> State CHAIN -> UPIEnv
mkUpiEnv Block
block Environment CHAIN
env State CHAIN
st = (Slot
blockSlot, DIState -> Bimap VKeyGenesis VKey
_dIStateDelegationMap DIState
delegSt, BlockCount
k, Word8
ngk)
  where
    blockSlot :: Slot
blockSlot = BlockHeader -> Slot
Abstract._bhSlot (Block -> BlockHeader
Abstract._bHeader Block
block)
    (Slot
_, UTxO
_, Set VKeyGenesis
allowedDelegators, PParams
_, BlockCount
k) = Environment CHAIN
env
    (Slot
_slot, Seq VKeyGenesis
_sgs, Hash
_h, UTxOState
_utxoSt, DIState
delegSt, UPIState
_upiSt) = State CHAIN
st
    numberOfDelegators :: Int
numberOfDelegators = forall a. Set a -> Int
Set.size Set VKeyGenesis
allowedDelegators
    ngk :: Word8
ngk
      | forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
maxBound :: Word8) forall a. Ord a => a -> a -> Bool
< Int
numberOfDelegators =
          forall a. HasCallStack => Text -> a
panic
            forall a b. (a -> b) -> a -> b
$ Text
"ts_prop_invalidDelegationSignalsAreRejected: "
            forall a. Semigroup a => a -> a -> a
<> Text
"too many genesis keys: "
            forall a. Semigroup a => a -> a -> a
<> forall a b. (Show a, ConvertText String b) => a -> b
show Int
numberOfDelegators
      | Bool
otherwise = forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
numberOfDelegators

-- | Extract the update state from the given chain state.
--
-- TODO: put this in `cardano-ledger`.
mkUpiSt ::
  State CHAIN ->
  UPIState
mkUpiSt :: State CHAIN -> UPIState
mkUpiSt (Slot
_slot, Seq VKeyGenesis
_sgs, Hash
_h, UTxOState
_utxoSt, DIState
_delegSt, UPIState
upiSt) = UPIState
upiSt

-- | Output resulting from elaborating and validating an abstract trace with
-- the concrete validators.
data ValidationOutput = ValidationOutput
  { ValidationOutput -> Config
elaboratedConfig :: !Genesis.Config
  -- ^ Elaborated configuration. This configuration results from elaborating
  -- the trace initial environment.
  , ValidationOutput
-> Either
     ChainValidationError
     (ChainValidationState, AbstractToConcreteIdMaps)
result ::
      !( Either
          ChainValidationError
          (ChainValidationState, AbstractToConcreteIdMaps)
       )
  }

-- | Apply the concrete validators to the given abstract trace.
applyTrace ::
  Trace CHAIN ->
  ValidationOutput
applyTrace :: Trace CHAIN -> ValidationOutput
applyTrace Trace CHAIN
tr =
  ValidationOutput
    { elaboratedConfig :: Config
elaboratedConfig = Config
config
    , result :: Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
result =
        forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Config
-> (ChainValidationState, AbstractToConcreteIdMaps)
-> (State CHAIN, Block)
-> Either
     ChainValidationError
     (ChainValidationState, AbstractToConcreteIdMaps)
elaborateAndUpdate Config
config) (ChainValidationState
initialState, AbstractToConcreteIdMaps
initialAbstractToConcreteIdMaps)
          forall a b. (a -> b) -> a -> b
$ forall s. TraceOrder -> Trace s -> [(State s, Signal s)]
preStatesAndSignals TraceOrder
OldestFirst Trace CHAIN
tr
    }
  where
    initialState :: ChainValidationState
initialState = ChainValidationState
initialStateNoUTxO {$sel:cvsUtxo:ChainValidationState :: UTxO
cvsUtxo = UTxO
initialUTxO}

    initialAbstractToConcreteIdMaps :: AbstractToConcreteIdMaps
initialAbstractToConcreteIdMaps = forall a. Monoid a => a
mempty {transactionIds :: Map TxId TxId
transactionIds = Map TxId TxId
txIdMap}

    initialStateNoUTxO :: ChainValidationState
initialStateNoUTxO =
      forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a. HasCallStack => Text -> a
panic forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. (Show a, ConvertText String b) => a -> b
show) forall (cat :: * -> * -> *) a. Category cat => cat a a
identity forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadError Error m =>
Config -> m ChainValidationState
initialChainValidationState Config
config

    config :: Config
config = Environment CHAIN -> Config
abEnvToCfg (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount)
abstractEnv

    abstractEnv :: (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount)
abstractEnv@( Slot
_currentSlot
                  , UTxO
abstractInitialUTxO
                  , Set VKeyGenesis
_allowedDelegators
                  , PParams
_protocolParams
                  , BlockCount
_stableAfter
                  ) = Trace CHAIN
tr forall s a. s -> Getting a s a -> a
^. forall s. Lens' (Trace s) (Environment s)
traceEnv

    (UTxO
initialUTxO, Map TxId TxId
txIdMap) = UTxO -> (UTxO, Map TxId TxId)
elaborateInitialUTxO UTxO
abstractInitialUTxO

ts_prop_invalidHeaderSizesAreRejected :: TSProperty
ts_prop_invalidHeaderSizesAreRejected :: TSProperty
ts_prop_invalidHeaderSizesAreRejected =
  (PParams -> Natural -> PParams)
-> (Block -> Natural)
-> (ProtocolParameters -> Natural -> ProtocolParameters)
-> (ABlock ByteString -> Natural)
-> (NonEmpty (PredicateFailure CHAIN)
    -> ChainValidationError -> PropertyT IO ())
-> TSProperty
invalidSizesAreRejected
    (\PParams
pps Natural
newMax -> PParams
pps {_maxHdrSz :: Natural
_maxHdrSz = Natural
newMax})
    (BlockHeader -> Natural
Abstract.bHeaderSize forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Block -> BlockHeader
Abstract._bHeader)
    (\ProtocolParameters
protocolParameters Natural
newMax -> ProtocolParameters
protocolParameters {ppMaxHeaderSize :: Natural
ppMaxHeaderSize = Natural
newMax})
    (AHeader ByteString -> Natural
headerLength forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a. ABlock a -> AHeader a
blockHeader)
    NonEmpty (PredicateFailure CHAIN)
-> ChainValidationError -> PropertyT IO ()
checkMaxSizeFailure
  where
    checkMaxSizeFailure ::
      NonEmpty (PredicateFailure CHAIN) ->
      ChainValidationError ->
      PropertyT IO ()
    checkMaxSizeFailure :: NonEmpty (PredicateFailure CHAIN)
-> ChainValidationError -> PropertyT IO ()
checkMaxSizeFailure NonEmpty (PredicateFailure CHAIN)
abstractPfs ChainValidationHeaderTooLarge {} = do
      forall (m :: * -> *). (MonadTest m, HasCallStack) => Bool -> m ()
assert
        forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any PredicateFailure CHAIN -> Bool
isHeaderSizeTooBigFailure NonEmpty (PredicateFailure CHAIN)
abstractPfs
      forall (m :: * -> *). MonadTest m => String -> m ()
footnote
        forall a b. (a -> b) -> a -> b
$ String
"HeaderSizeTooBig not found in the abstract predicate failures: "
        forall a. [a] -> [a] -> [a]
++ forall a b. (Show a, ConvertText String b) => a -> b
show NonEmpty (PredicateFailure CHAIN)
abstractPfs
    checkMaxSizeFailure NonEmpty (PredicateFailure CHAIN)
_ ChainValidationError
concretePF = do
      forall (m :: * -> *). MonadTest m => String -> m ()
footnote forall a b. (a -> b) -> a -> b
$ String
"Expected 'ChainValidationHeaderTooLarge' error, got " forall a. [a] -> [a] -> [a]
++ forall a b. (Show a, ConvertText String b) => a -> b
show ChainValidationError
concretePF
      forall (m :: * -> *) a. (MonadTest m, HasCallStack) => m a
failure

-- | Check that blocks with components (e.g. headers, bodies) that have an
-- invalid size (according to the protocol parameters) are rejected.
invalidSizesAreRejected ::
  -- | Setter for the abstract protocol parameters. The 'Natural' parameter is
  -- used to pass a new (generated) maximum size.
  (PParams -> Natural -> PParams) ->
  -- | Function used to compute the size of the abstract-block's component.
  (Abstract.Block -> Natural) ->
  -- | Setter for the concrete protocol parameters.
  (ProtocolParameters -> Natural -> ProtocolParameters) ->
  -- | Function used to compute the size of the concrete-block's component.
  (ABlock ByteString -> Natural) ->
  -- | Function to check agreement of concrete and abstract failures.
  (NonEmpty (PredicateFailure CHAIN) -> ChainValidationError -> PropertyT IO ()) ->
  TSProperty
invalidSizesAreRejected :: (PParams -> Natural -> PParams)
-> (Block -> Natural)
-> (ProtocolParameters -> Natural -> ProtocolParameters)
-> (ABlock ByteString -> Natural)
-> (NonEmpty (PredicateFailure CHAIN)
    -> ChainValidationError -> PropertyT IO ())
-> TSProperty
invalidSizesAreRejected
  PParams -> Natural -> PParams
setAbstractParamTo
  Block -> Natural
abstractBlockComponentSize
  ProtocolParameters -> Natural -> ProtocolParameters
setConcreteParamTo
  ABlock ByteString -> Natural
concreteBlockComponentSize
  NonEmpty (PredicateFailure CHAIN)
-> ChainValidationError -> PropertyT IO ()
checkFailures =
    TestLimit -> Property -> TSProperty
withTestsTS TestLimit
300
      forall a b. (a -> b) -> a -> b
$ HasCallStack => PropertyT IO () -> Property
property
      forall a b. (a -> b) -> a -> b
$ do
        Trace CHAIN
tr <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall s. HasTrace s => BaseEnv s -> Word64 -> Gen (Trace s)
trace @CHAIN () Word64
100 forall s. Gen (Trace s) -> Int -> Gen (Trace s)
`ofLengthAtLeast` Int
1
        let ValidationOutput {Config
elaboratedConfig :: Config
elaboratedConfig :: ValidationOutput -> Config
elaboratedConfig, Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
result :: Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
result :: ValidationOutput
-> Either
     ChainValidationError
     (ChainValidationState, AbstractToConcreteIdMaps)
result} =
              Trace CHAIN -> ValidationOutput
applyTrace Trace CHAIN
initTr
            initTr :: Trace CHAIN
            initTr :: Trace CHAIN
initTr = forall s. HasCallStack => Trace s -> Trace s
traceInit Trace CHAIN
tr
        case Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
result of
          Left ChainValidationError
error -> do
            forall (m :: * -> *). MonadTest m => String -> m ()
footnote forall a b. (a -> b) -> a -> b
$ String
"Expecting a valid trace but got: " forall a. [a] -> [a] -> [a]
++ forall a b. (Show a, ConvertText String b) => a -> b
show ChainValidationError
error
            forall (m :: * -> *) a. (MonadTest m, HasCallStack) => m a
failure
          Right (ChainValidationState
concreteState, AbstractToConcreteIdMaps
concreteIdMaps) -> do
            let abstractState :: State CHAIN
                abstractState :: State CHAIN
abstractState = forall s. Trace s -> State s
lastState forall a b. (a -> b) -> a -> b
$ Trace CHAIN
initTr

                lastBlock :: Signal CHAIN
                lastBlock :: Signal CHAIN
lastBlock = forall s. HasCallStack => Trace s -> Signal s
lastSignal Trace CHAIN
tr

                abstractEnv :: Environment CHAIN
                abstractEnv :: Environment CHAIN
abstractEnv = forall s. Trace s -> Environment s
_traceEnv Trace CHAIN
tr

                concreteLastBlock :: ABlock ByteString
concreteLastBlock =
                  -- NOTE: since we're altering the maximum header/body size defined in
                  -- the parameters we it shouldn't matter whether we're using the
                  -- altered states.
                  Config
-> ChainValidationState
-> AbstractToConcreteIdMaps
-> State CHAIN
-> Block
-> ABlock ByteString
elaborateBlock
                    Config
elaboratedConfig
                    ChainValidationState
concreteState
                    AbstractToConcreteIdMaps
concreteIdMaps
                    State CHAIN
abstractState
                    Signal CHAIN
lastBlock

                lastBlockHeaderSize :: Natural
lastBlockHeaderSize = Block -> Natural
abstractBlockComponentSize Signal CHAIN
lastBlock

                concreteLastBlockSize :: Natural
concreteLastBlockSize = ABlock ByteString -> Natural
concreteBlockComponentSize ABlock ByteString
concreteLastBlock

            State CHAIN
alteredAbstractState :: State CHAIN <-
              forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ State CHAIN -> Natural -> Gen (State CHAIN)
genAbstractAlteredState State CHAIN
abstractState (Natural
lastBlockHeaderSize forall a. Num a => a -> a -> a
- Natural
1)

            ChainValidationState
alteredConcreteState <-
              forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ ChainValidationState -> Natural -> Gen ChainValidationState
genConcreteAlteredState ChainValidationState
concreteState (Natural
concreteLastBlockSize forall a. Num a => a -> a -> a
- Natural
1)
            --
            -- NOTE: Here we could simply choose not to use the concrete block size
            -- and use the abstract block size instead. The former will be larger
            -- than the latter. However the problem will be that we won't be
            -- testing the boundary condition block size - 1 == maximum block size

            let abstractResult :: Either (NonEmpty (PredicateFailure CHAIN)) (State CHAIN)
abstractResult =
                  forall s (rtype :: RuleType).
(STS s, RuleTypeRep rtype, BaseM s ~ Identity) =>
RuleContext rtype s
-> Either (NonEmpty (PredicateFailure s)) (State s)
applySTS @CHAIN (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment CHAIN
abstractEnv, State CHAIN
alteredAbstractState, Signal CHAIN
lastBlock))

                concreteResult :: Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
concreteResult =
                  Config
-> (ChainValidationState, AbstractToConcreteIdMaps)
-> (State CHAIN, Block)
-> Either
     ChainValidationError
     (ChainValidationState, AbstractToConcreteIdMaps)
elaborateAndUpdate
                    Config
elaboratedConfig
                    (ChainValidationState
alteredConcreteState, AbstractToConcreteIdMaps
concreteIdMaps)
                    (State CHAIN
alteredAbstractState, Signal CHAIN
lastBlock)

            case (Either (NonEmpty (PredicateFailure CHAIN)) (State CHAIN)
abstractResult, Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
concreteResult) of
              (Left NonEmpty ChainPredicateFailure
abstractPfs, Left ChainValidationError
concretePf) -> do
                NonEmpty (PredicateFailure CHAIN)
-> ChainValidationError -> PropertyT IO ()
checkFailures NonEmpty ChainPredicateFailure
abstractPfs ChainValidationError
concretePf
                forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover CoverPercentage
85 LabelName
"Size validation hit" Bool
True
                forall (m :: * -> *). MonadTest m => m ()
success
              (Right (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
_, Right (ChainValidationState, AbstractToConcreteIdMaps)
_) ->
                -- It might be that we are at an epoch boundary, so the altered
                -- update state will be overwritten by an epoch transition. In that
                -- case it is OK if both executable spec and implementation return
                -- 'Right'.
                forall (m :: * -> *). MonadTest m => m ()
success
              (Either
   (NonEmpty ChainPredicateFailure)
   (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState),
 Either
   ChainValidationError
   (ChainValidationState, AbstractToConcreteIdMaps))
_ -> do
                forall (m :: * -> *). MonadTest m => String -> m ()
footnote String
"Validation results mismatch."
                forall (m :: * -> *). MonadTest m => String -> m ()
footnote forall a b. (a -> b) -> a -> b
$ String
"Altered abstract state: " forall a. [a] -> [a] -> [a]
++ forall a b. (Show a, ConvertText String b) => a -> b
show State CHAIN
alteredAbstractState
                forall (m :: * -> *). MonadTest m => String -> m ()
footnote forall a b. (a -> b) -> a -> b
$ String
"Signal: " forall a. [a] -> [a] -> [a]
++ forall a b. (Show a, ConvertText String b) => a -> b
show Signal CHAIN
lastBlock
                forall (m :: * -> *). MonadTest m => String -> m ()
footnote forall a b. (a -> b) -> a -> b
$ String
"Abstract result: " forall a. [a] -> [a] -> [a]
++ forall a b. (Show a, ConvertText String b) => a -> b
show Either (NonEmpty (PredicateFailure CHAIN)) (State CHAIN)
abstractResult
                forall (m :: * -> *). MonadTest m => String -> m ()
footnote forall a b. (a -> b) -> a -> b
$ String
"Concrete result: " forall a. [a] -> [a] -> [a]
++ forall a b. (Show a, ConvertText String b) => a -> b
show Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
concreteResult
                forall (m :: * -> *) a. (MonadTest m, HasCallStack) => m a
failure
    where
      genAbstractAlteredState :: State CHAIN -> Natural -> Gen (State CHAIN)
      genAbstractAlteredState :: State CHAIN -> Natural -> Gen (State CHAIN)
genAbstractAlteredState (Slot
slot, Seq VKeyGenesis
sgs, Hash
h, UTxOState
utxo, DIState
ds, UPIState
us) Natural
maxSize =
        (Slot
slot,Seq VKeyGenesis
sgs,Hash
h,UTxOState
utxo,DIState
ds,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UPIState -> GenT Identity UPIState
genAlteredUpdateState UPIState
us
        where
          genAlteredUpdateState :: UPIState -> GenT Identity UPIState
genAlteredUpdateState ((ProtVer
pv, PParams
pps), [(Slot, (ProtVer, PParams))]
fads, Map ApName (ApVer, Slot, Metadata)
avs, Map UpId (ProtVer, PParams)
rpus, Map UpId (ApName, ApVer, Metadata)
raus, Map UpId Slot
cps, Set (UpId, VKeyGenesis)
vts, Set (ProtVer, VKeyGenesis)
bvs, Map UpId Slot
pws) = do
            Natural
newMaxSize <- forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (forall a. a -> a -> Range a
Range.constant Natural
0 Natural
maxSize)
            forall (f :: * -> *) a. Applicative f => a -> f a
pure
              forall a b. (a -> b) -> a -> b
$! ( (ProtVer
pv, PParams
pps PParams -> Natural -> PParams
`setAbstractParamTo` Natural
newMaxSize)
                 , [(Slot, (ProtVer, PParams))]
fads
                 , Map ApName (ApVer, Slot, Metadata)
avs
                 , Map UpId (ProtVer, PParams)
rpus
                 , Map UpId (ApName, ApVer, Metadata)
raus
                 , Map UpId Slot
cps
                 , Set (UpId, VKeyGenesis)
vts
                 , Set (ProtVer, VKeyGenesis)
bvs
                 , Map UpId Slot
pws
                 )

      genConcreteAlteredState ::
        ChainValidationState -> Natural -> Gen ChainValidationState
      genConcreteAlteredState :: ChainValidationState -> Natural -> Gen ChainValidationState
genConcreteAlteredState ChainValidationState
state Natural
maxSize =
        Natural -> ChainValidationState
setMaxHeaderSize forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (forall a. a -> a -> Range a
Range.constant Natural
0 Natural
maxSize)
        where
          setMaxHeaderSize :: Natural -> ChainValidationState
setMaxHeaderSize Natural
newSize = ChainValidationState
state {$sel:cvsUpdateState:ChainValidationState :: State
cvsUpdateState = State
newUpdateState}
            where
              newUpdateState :: State
newUpdateState =
                (ChainValidationState -> State
cvsUpdateState ChainValidationState
state) {adoptedProtocolParameters :: ProtocolParameters
adoptedProtocolParameters = ProtocolParameters
newParameters}
                where
                  newParameters :: ProtocolParameters
newParameters =
                    (State -> ProtocolParameters
adoptedProtocolParameters (ChainValidationState -> State
cvsUpdateState ChainValidationState
state))
                      ProtocolParameters -> Natural -> ProtocolParameters
`setConcreteParamTo` Natural
newSize

ts_prop_invalidBlockSizesAreRejected :: TSProperty
ts_prop_invalidBlockSizesAreRejected :: TSProperty
ts_prop_invalidBlockSizesAreRejected =
  (PParams -> Natural -> PParams)
-> (Block -> Natural)
-> (ProtocolParameters -> Natural -> ProtocolParameters)
-> (ABlock ByteString -> Natural)
-> (NonEmpty (PredicateFailure CHAIN)
    -> ChainValidationError -> PropertyT IO ())
-> TSProperty
invalidSizesAreRejected
    (\PParams
pps Natural
newMax -> PParams
pps {_maxBkSz :: Natural
_maxBkSz = Natural
newMax})
    Block -> Natural
Abstract.bSize
    (\ProtocolParameters
protocolParameters Natural
newMax -> ProtocolParameters
protocolParameters {ppMaxBlockSize :: Natural
ppMaxBlockSize = Natural
newMax})
    ABlock ByteString -> Natural
blockLength
    NonEmpty (PredicateFailure CHAIN)
-> ChainValidationError -> PropertyT IO ()
checkMaxSizeFailure
  where
    checkMaxSizeFailure ::
      NonEmpty (PredicateFailure CHAIN) ->
      ChainValidationError ->
      PropertyT IO ()
    checkMaxSizeFailure :: NonEmpty (PredicateFailure CHAIN)
-> ChainValidationError -> PropertyT IO ()
checkMaxSizeFailure NonEmpty (PredicateFailure CHAIN)
abstractPfs ChainValidationBlockTooLarge {} = do
      forall (m :: * -> *). (MonadTest m, HasCallStack) => Bool -> m ()
assert
        forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Eq a => a -> a -> Bool
== BbodyPredicateFailure
InvalidBlockSize)
        forall a b. (a -> b) -> a -> b
$ forall d a. (Data d, Typeable a) => d -> [a]
extractValues NonEmpty (PredicateFailure CHAIN)
abstractPfs
      forall (m :: * -> *). MonadTest m => String -> m ()
footnote
        forall a b. (a -> b) -> a -> b
$ String
"InvalidBlockSize not found in the abstract predicate failures: "
        forall a. [a] -> [a] -> [a]
++ forall a b. (Show a, ConvertText String b) => a -> b
show NonEmpty (PredicateFailure CHAIN)
abstractPfs
    checkMaxSizeFailure NonEmpty (PredicateFailure CHAIN)
_ ChainValidationError
concretePF = do
      forall (m :: * -> *). MonadTest m => String -> m ()
footnote forall a b. (a -> b) -> a -> b
$ String
"Expected 'ChainValidationBlockTooLarge' error, got " forall a. [a] -> [a] -> [a]
++ forall a b. (Show a, ConvertText String b) => a -> b
show ChainValidationError
concretePF
      forall (m :: * -> *) a. (MonadTest m, HasCallStack) => m a
failure