{-# 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
    (Property -> TSProperty) -> Property -> TSProperty
forall a b. (a -> b) -> a -> b
$ HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property
    (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
      let (Word64
traceLength, Word64
step) = (Word64
200 :: Word64, Word64
10 :: Word64)
      Trace CHAIN
tr <- Gen (Trace CHAIN) -> PropertyT IO (Trace CHAIN)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen (Trace CHAIN) -> PropertyT IO (Trace CHAIN))
-> Gen (Trace CHAIN) -> PropertyT IO (Trace CHAIN)
forall a b. (a -> b) -> a -> b
$ forall s. HasTrace s => BaseEnv s -> Word64 -> Gen (Trace s)
trace @CHAIN () Word64
traceLength
      Trace CHAIN -> Word64 -> Word64 -> PropertyT IO ()
forall s. Trace s -> Word64 -> Word64 -> PropertyT IO ()
classifyTraceLength Trace CHAIN
tr Word64
traceLength Word64
step
      Maybe (BlockStats, BlockStats, BlockStats) -> PropertyT IO ()
classifyBlockStats
        (Maybe (BlockStats, BlockStats, BlockStats) -> PropertyT IO ())
-> Maybe (BlockStats, BlockStats, BlockStats) -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ [BlockStats] -> Maybe (BlockStats, BlockStats, BlockStats)
Abstract.chainBlockStats
        ([BlockStats] -> Maybe (BlockStats, BlockStats, BlockStats))
-> [BlockStats] -> Maybe (BlockStats, BlockStats, BlockStats)
forall a b. (a -> b) -> a -> b
$ (Block -> BlockStats) -> [Block] -> [BlockStats]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map Block -> BlockStats
Abstract.blockStats (TraceOrder -> Trace CHAIN -> [Signal CHAIN]
forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace CHAIN
tr)
      Trace CHAIN -> PropertyT IO ()
forall (m :: * -> *). MonadTest m => Trace CHAIN -> m ()
printAdditionalInfoOnFailure Trace CHAIN
tr
      Trace CHAIN -> PropertyT IO ()
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 =
      String -> m ()
forall (m :: * -> *). MonadTest m => String -> m ()
footnote (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"Allowed delegators hashes: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [KeyHash] -> String
forall a b. (Show a, ConvertText String b) => a -> b
show [KeyHash]
allowedDelegatorHashes
      where
        allowedDelegatorHashes :: [KeyHash]
allowedDelegatorHashes = VKeyGenesis -> KeyHash
elaborateVKeyGenesisHash (VKeyGenesis -> KeyHash) -> [VKeyGenesis] -> [KeyHash]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set VKeyGenesis -> [VKeyGenesis]
forall a. Set a -> [a]
Set.toList Set VKeyGenesis
allowedDelegators
        (Slot
_, UTxO
_, Set VKeyGenesis
allowedDelegators, PParams
_, BlockCount
_) = Trace CHAIN -> Environment CHAIN
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 = () -> PropertyT IO ()
forall a. a -> PropertyT IO a
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 Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
0 = LabelName -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
LabelName -> m ()
label (String -> LabelName
forall a. IsString a => String -> a
fromString (String
l String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" == 0"))
      | BlockStats -> Word
f BlockStats
stats Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
1 = LabelName -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
LabelName -> m ()
label (String -> LabelName
forall a. IsString a => String -> a
fromString (String
l String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" == 1"))
      | Bool
otherwise = LabelName -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
LabelName -> m ()
label (String -> LabelName
forall a. IsString a => String -> a
fromString (String
l String -> String -> String
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 = m (ChainValidationState, AbstractToConcreteIdMaps) -> m ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (m (ChainValidationState, AbstractToConcreteIdMaps) -> m ())
-> m (ChainValidationState, AbstractToConcreteIdMaps) -> m ()
forall a b. (a -> b) -> a -> b
$ Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
-> m (ChainValidationState, AbstractToConcreteIdMaps)
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 :: Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
result :: ValidationOutput
-> 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') (ChainValidationState
 -> (ChainValidationState, AbstractToConcreteIdMaps))
-> Either ChainValidationError ChainValidationState
-> Either
     ChainValidationError
     (ChainValidationState, AbstractToConcreteIdMaps)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT
  ValidationMode (Either ChainValidationError) ChainValidationState
-> ValidationMode
-> Either ChainValidationError ChainValidationState
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (Config
-> ChainValidationState
-> ABlock ByteString
-> ReaderT
     ValidationMode (Either ChainValidationError) ChainValidationState
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
VKey -> BlockCount -> State CHAIN -> DCert
rcDCert (Block
ab Block -> Getting VKey Block VKey -> VKey
forall s a. s -> Getting a s a -> a
^. (BlockHeader -> Const VKey BlockHeader)
-> Block -> Const VKey Block
Lens' Block BlockHeader
Abstract.bHeader ((BlockHeader -> Const VKey BlockHeader)
 -> Block -> Const VKey Block)
-> ((VKey -> Const VKey VKey)
    -> BlockHeader -> Const VKey BlockHeader)
-> Getting VKey Block VKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (VKey -> Const VKey VKey) -> BlockHeader -> Const VKey BlockHeader
Lens' BlockHeader VKey
Abstract.bhIssuer) BlockCount
stableAfter State CHAIN
ast

    stableAfter :: BlockCount
stableAfter = Word64 -> BlockCount
AbstractCore.BlockCount (Word64 -> BlockCount) -> Word64 -> BlockCount
forall a b. (a -> b) -> a -> b
$ BlockCount -> Word64
unBlockCount (BlockCount -> Word64) -> BlockCount -> Word64
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
VKey -> BlockCount -> State CHAIN -> DCert
rcDCert
              (Block
abstractBlock Block -> Getting VKey Block VKey -> VKey
forall s a. s -> Getting a s a -> a
^. (BlockHeader -> Const VKey BlockHeader)
-> Block -> Const VKey Block
Lens' Block BlockHeader
Abstract.bHeader ((BlockHeader -> Const VKey BlockHeader)
 -> Block -> Const VKey Block)
-> ((VKey -> Const VKey VKey)
    -> BlockHeader -> Const VKey BlockHeader)
-> Getting VKey Block VKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (VKey -> Const VKey VKey) -> BlockHeader -> Const VKey BlockHeader
Lens' BlockHeader VKey
Abstract.bhIssuer)
              BlockCount
stableAfter
              State CHAIN
abstractState
            where
              stableAfter :: BlockCount
stableAfter =
                Word64 -> BlockCount
AbstractCore.BlockCount
                  (Word64 -> BlockCount) -> Word64 -> BlockCount
forall a b. (a -> b) -> a -> b
$ BlockCount -> Word64
unBlockCount
                  (BlockCount -> Word64) -> BlockCount -> Word64
forall a b. (a -> b) -> a -> b
$ Config -> BlockCount
Genesis.configK Config
config

classifyTransactions :: Trace CHAIN -> PropertyT IO ()
classifyTransactions :: Trace CHAIN -> PropertyT IO ()
classifyTransactions =
  Int -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, Show a, HasCallStack) =>
a -> m ()
collect
    (Int -> PropertyT IO ())
-> (Trace CHAIN -> Int) -> Trace CHAIN -> PropertyT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum
    ([Int] -> Int) -> (Trace CHAIN -> [Int]) -> Trace CHAIN -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Block -> Int) -> [Block] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Tx] -> Int
forall a. HasLength a => a -> Int
length ([Tx] -> Int) -> (Block -> [Tx]) -> Block -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
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 (BlockBody -> [Tx]) -> (Block -> BlockBody) -> Block -> [Tx]
forall b c a. (b -> c) -> (a -> b) -> a -> c
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)
    ([Block] -> [Int])
-> (Trace CHAIN -> [Block]) -> Trace CHAIN -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. TraceOrder -> Trace CHAIN -> [Signal CHAIN]
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
    (Property -> TSProperty) -> Property -> TSProperty
forall a b. (a -> b) -> a -> b
$ HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property
    (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
      let traceLength :: Word64
traceLength = Word64
100 :: Word64
      Trace CHAIN
tr <- Gen (Trace CHAIN) -> PropertyT IO (Trace CHAIN)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen (Trace CHAIN) -> PropertyT IO (Trace CHAIN))
-> Gen (Trace CHAIN) -> PropertyT IO (Trace CHAIN)
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 :: Config
elaboratedConfig :: ValidationOutput -> Config
elaboratedConfig, Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
result :: ValidationOutput
-> Either
     ChainValidationError
     (ChainValidationState, AbstractToConcreteIdMaps)
result :: Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
result} =
            Trace CHAIN -> ValidationOutput
applyTrace (Trace CHAIN -> Trace CHAIN
forall s. Trace s -> Trace s
Invalid.Trace.validPrefix Trace CHAIN
tr)
      case Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
result of
        Left ChainValidationError
error -> do
          String -> PropertyT IO ()
forall (m :: * -> *). MonadTest m => String -> m ()
footnote (String -> PropertyT IO ()) -> String -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ String
"Expecting a valid prefix but got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ChainValidationError -> String
forall a b. (Show a, ConvertText String b) => a -> b
show ChainValidationError
error
          PropertyT IO ()
forall (m :: * -> *) a. (MonadTest m, HasCallStack) => m a
failure
        Right (ChainValidationState, AbstractToConcreteIdMaps)
concreteState ->
          let abstractState :: State CHAIN
abstractState = Trace CHAIN -> State CHAIN
forall s. Trace s -> State s
lastState (Trace CHAIN -> Trace CHAIN
forall s. Trace s -> Trace s
Invalid.Trace.validPrefix Trace CHAIN
tr)
              block :: Signal CHAIN
block = Trace CHAIN -> Signal CHAIN
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, Block
Signal CHAIN
block)
           in case (Trace CHAIN
-> Either (NonEmpty (PredicateFailure CHAIN)) (State CHAIN)
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.
                  PropertyT IO ()
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
NonEmpty (PredicateFailure CHAIN)
abstractPfs ChainValidationError
concretePfs
                (Either
  (NonEmpty ChainPredicateFailure)
  (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
abstractResult, Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
concreteResult) -> do
                  String -> PropertyT IO ()
forall (m :: * -> *). MonadTest m => String -> m ()
footnote String
"Validation results mismatch."
                  String -> PropertyT IO ()
forall (m :: * -> *). MonadTest m => String -> m ()
footnote (String -> PropertyT IO ()) -> String -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ String
"Signal: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Block -> String
forall a b. (Show a, ConvertText String b) => a -> b
show Block
Signal CHAIN
block
                  String -> PropertyT IO ()
forall (m :: * -> *). MonadTest m => String -> m ()
footnote (String -> PropertyT IO ()) -> String -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ String
"Abstract result: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Either
  (NonEmpty ChainPredicateFailure)
  (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> String
forall a b. (Show a, ConvertText String b) => a -> b
show Either
  (NonEmpty ChainPredicateFailure)
  (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
abstractResult
                  String -> PropertyT IO ()
forall (m :: * -> *). MonadTest m => String -> m ()
footnote (String -> PropertyT IO ()) -> String -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ String
"Concrete result: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
-> String
forall a b. (Show a, ConvertText String b) => a -> b
show Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
concreteResult
                  PropertyT IO ()
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 = Set VKeyGenesis -> Int
forall a. Set a -> Int
Set.size Set VKeyGenesis
allowedDelegators
    ngk :: Word8
ngk
      | Word8 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word8
forall a. Bounded a => a
maxBound :: Word8) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
numberOfDelegators =
          Text -> Word8
forall a. HasCallStack => Text -> a
panic
            (Text -> Word8) -> Text -> Word8
forall a b. (a -> b) -> a -> b
$ Text
"ts_prop_invalidDelegationSignalsAreRejected: "
            Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"too many genesis keys: "
            Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall a b. (Show a, ConvertText String b) => a -> b
show Int
numberOfDelegators
      | Bool
otherwise = Int -> Word8
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 =
        ((ChainValidationState, AbstractToConcreteIdMaps)
 -> ((Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState),
     Block)
 -> Either
      ChainValidationError
      (ChainValidationState, AbstractToConcreteIdMaps))
-> (ChainValidationState, AbstractToConcreteIdMaps)
-> [((Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState),
     Block)]
-> Either
     ChainValidationError
     (ChainValidationState, AbstractToConcreteIdMaps)
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)
          ([((Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState),
   Block)]
 -> Either
      ChainValidationError
      (ChainValidationState, AbstractToConcreteIdMaps))
-> [((Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState),
     Block)]
-> Either
     ChainValidationError
     (ChainValidationState, AbstractToConcreteIdMaps)
forall a b. (a -> b) -> a -> b
$ TraceOrder -> Trace CHAIN -> [(State CHAIN, Signal CHAIN)]
forall s. TraceOrder -> Trace s -> [(State s, Signal s)]
preStatesAndSignals TraceOrder
OldestFirst Trace CHAIN
tr
    }
  where
    initialState :: ChainValidationState
initialState = ChainValidationState
initialStateNoUTxO {cvsUtxo = initialUTxO}

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

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

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

    abstractEnv :: (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount)
abstractEnv@( Slot
_currentSlot
                  , UTxO
abstractInitialUTxO
                  , Set VKeyGenesis
_allowedDelegators
                  , PParams
_protocolParams
                  , BlockCount
_stableAfter
                  ) = Trace CHAIN
tr Trace CHAIN
-> Getting
     (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount)
     (Trace CHAIN)
     (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount)
-> (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount)
forall s a. s -> Getting a s a -> a
^. Getting
  (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount)
  (Trace CHAIN)
  (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount)
(Environment CHAIN
 -> Const
      (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount)
      (Environment CHAIN))
-> Trace CHAIN
-> Const
     (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount) (Trace CHAIN)
forall s (f :: * -> *).
Functor f =>
(Environment s -> f (Environment s)) -> Trace s -> f (Trace 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 = newMax})
    (BlockHeader -> Natural
Abstract.bHeaderSize (BlockHeader -> Natural)
-> (Block -> BlockHeader) -> Block -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
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 = newMax})
    (AHeader ByteString -> Natural
headerLength (AHeader ByteString -> Natural)
-> (ABlock ByteString -> AHeader ByteString)
-> ABlock ByteString
-> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ABlock ByteString -> AHeader ByteString
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
      Bool -> PropertyT IO ()
forall (m :: * -> *). (MonadTest m, HasCallStack) => Bool -> m ()
assert
        (Bool -> PropertyT IO ()) -> Bool -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ (ChainPredicateFailure -> Bool)
-> NonEmpty ChainPredicateFailure -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ChainPredicateFailure -> Bool
PredicateFailure CHAIN -> Bool
isHeaderSizeTooBigFailure NonEmpty ChainPredicateFailure
NonEmpty (PredicateFailure CHAIN)
abstractPfs
      String -> PropertyT IO ()
forall (m :: * -> *). MonadTest m => String -> m ()
footnote
        (String -> PropertyT IO ()) -> String -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ String
"HeaderSizeTooBig not found in the abstract predicate failures: "
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ NonEmpty ChainPredicateFailure -> String
forall a b. (Show a, ConvertText String b) => a -> b
show NonEmpty ChainPredicateFailure
NonEmpty (PredicateFailure CHAIN)
abstractPfs
    checkMaxSizeFailure NonEmpty (PredicateFailure CHAIN)
_ ChainValidationError
concretePF = do
      String -> PropertyT IO ()
forall (m :: * -> *). MonadTest m => String -> m ()
footnote (String -> PropertyT IO ()) -> String -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ String
"Expected 'ChainValidationHeaderTooLarge' error, got " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ChainValidationError -> String
forall a b. (Show a, ConvertText String b) => a -> b
show ChainValidationError
concretePF
      PropertyT IO ()
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
      (Property -> TSProperty) -> Property -> TSProperty
forall a b. (a -> b) -> a -> b
$ HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property
      (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
        Trace CHAIN
tr <- Gen (Trace CHAIN) -> PropertyT IO (Trace CHAIN)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen (Trace CHAIN) -> PropertyT IO (Trace CHAIN))
-> Gen (Trace CHAIN) -> PropertyT IO (Trace CHAIN)
forall a b. (a -> b) -> a -> b
$ forall s. HasTrace s => BaseEnv s -> Word64 -> Gen (Trace s)
trace @CHAIN () Word64
100 Gen (Trace CHAIN) -> Int -> Gen (Trace CHAIN)
forall s. Gen (Trace s) -> Int -> Gen (Trace s)
`ofLengthAtLeast` Int
1
        let ValidationOutput {Config
elaboratedConfig :: ValidationOutput -> Config
elaboratedConfig :: Config
elaboratedConfig, Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
result :: ValidationOutput
-> Either
     ChainValidationError
     (ChainValidationState, AbstractToConcreteIdMaps)
result :: Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
result} =
              Trace CHAIN -> ValidationOutput
applyTrace Trace CHAIN
initTr
            initTr :: Trace CHAIN
            initTr :: Trace CHAIN
initTr = Trace CHAIN -> Trace CHAIN
forall s. HasCallStack => Trace s -> Trace s
traceInit Trace CHAIN
tr
        case Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
result of
          Left ChainValidationError
error -> do
            String -> PropertyT IO ()
forall (m :: * -> *). MonadTest m => String -> m ()
footnote (String -> PropertyT IO ()) -> String -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ String
"Expecting a valid trace but got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ChainValidationError -> String
forall a b. (Show a, ConvertText String b) => a -> b
show ChainValidationError
error
            PropertyT IO ()
forall (m :: * -> *) a. (MonadTest m, HasCallStack) => m a
failure
          Right (ChainValidationState
concreteState, AbstractToConcreteIdMaps
concreteIdMaps) -> do
            let abstractState :: State CHAIN
                abstractState :: State CHAIN
abstractState = Trace CHAIN -> State CHAIN
forall s. Trace s -> State s
lastState (Trace CHAIN -> State CHAIN) -> Trace CHAIN -> State CHAIN
forall a b. (a -> b) -> a -> b
$ Trace CHAIN
initTr

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

                abstractEnv :: Environment CHAIN
                abstractEnv :: Environment CHAIN
abstractEnv = Trace CHAIN -> Environment CHAIN
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
                    Block
Signal CHAIN
lastBlock

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

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

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

            ChainValidationState
alteredConcreteState <-
              Gen ChainValidationState -> PropertyT IO ChainValidationState
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen ChainValidationState -> PropertyT IO ChainValidationState)
-> Gen ChainValidationState -> PropertyT IO ChainValidationState
forall a b. (a -> b) -> a -> b
$ ChainValidationState -> Natural -> Gen ChainValidationState
genConcreteAlteredState ChainValidationState
concreteState (Natural
concreteLastBlockSize Natural -> Natural -> Natural
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 ((Environment CHAIN, State CHAIN, Signal CHAIN) -> TRC 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, Block
Signal CHAIN
lastBlock)

            case (Either
  (NonEmpty ChainPredicateFailure)
  (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
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
NonEmpty (PredicateFailure CHAIN)
abstractPfs ChainValidationError
concretePf
                CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover CoverPercentage
85 LabelName
"Size validation hit" Bool
True
                PropertyT IO ()
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'.
                PropertyT IO ()
forall (m :: * -> *). MonadTest m => m ()
success
              (Either
   (NonEmpty ChainPredicateFailure)
   (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState),
 Either
   ChainValidationError
   (ChainValidationState, AbstractToConcreteIdMaps))
_ -> do
                String -> PropertyT IO ()
forall (m :: * -> *). MonadTest m => String -> m ()
footnote String
"Validation results mismatch."
                String -> PropertyT IO ()
forall (m :: * -> *). MonadTest m => String -> m ()
footnote (String -> PropertyT IO ()) -> String -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ String
"Altered abstract state: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> String
forall a b. (Show a, ConvertText String b) => a -> b
show (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
State CHAIN
alteredAbstractState
                String -> PropertyT IO ()
forall (m :: * -> *). MonadTest m => String -> m ()
footnote (String -> PropertyT IO ()) -> String -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ String
"Signal: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Block -> String
forall a b. (Show a, ConvertText String b) => a -> b
show Block
Signal CHAIN
lastBlock
                String -> PropertyT IO ()
forall (m :: * -> *). MonadTest m => String -> m ()
footnote (String -> PropertyT IO ()) -> String -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ String
"Abstract result: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Either
  (NonEmpty ChainPredicateFailure)
  (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> String
forall a b. (Show a, ConvertText String b) => a -> b
show Either
  (NonEmpty ChainPredicateFailure)
  (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
Either (NonEmpty (PredicateFailure CHAIN)) (State CHAIN)
abstractResult
                String -> PropertyT IO ()
forall (m :: * -> *). MonadTest m => String -> m ()
footnote (String -> PropertyT IO ()) -> String -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ String
"Concrete result: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
-> String
forall a b. (Show a, ConvertText String b) => a -> b
show Either
  ChainValidationError
  (ChainValidationState, AbstractToConcreteIdMaps)
concreteResult
                PropertyT IO ()
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,) (UPIState
 -> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState))
-> GenT Identity UPIState
-> GenT
     Identity
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
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 <- Range Natural -> GenT Identity Natural
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Natural -> Natural -> Range Natural
forall a. a -> a -> Range a
Range.constant Natural
0 Natural
maxSize)
            UPIState -> GenT Identity UPIState
forall a. a -> GenT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
              (UPIState -> GenT Identity UPIState)
-> UPIState -> GenT Identity UPIState
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 (Natural -> ChainValidationState)
-> GenT Identity Natural -> Gen ChainValidationState
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range Natural -> GenT Identity Natural
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Natural -> Natural -> Range Natural
forall a. a -> a -> Range a
Range.constant Natural
0 Natural
maxSize)
        where
          setMaxHeaderSize :: Natural -> ChainValidationState
setMaxHeaderSize Natural
newSize = ChainValidationState
state {cvsUpdateState = newUpdateState}
            where
              newUpdateState :: State
newUpdateState =
                (ChainValidationState -> State
cvsUpdateState ChainValidationState
state) {adoptedProtocolParameters = 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 = newMax})
    Block -> Natural
Abstract.bSize
    (\ProtocolParameters
protocolParameters Natural
newMax -> ProtocolParameters
protocolParameters {ppMaxBlockSize = 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
      Bool -> PropertyT IO ()
forall (m :: * -> *). (MonadTest m, HasCallStack) => Bool -> m ()
assert
        (Bool -> PropertyT IO ()) -> Bool -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ (BbodyPredicateFailure -> Bool) -> [BbodyPredicateFailure] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (BbodyPredicateFailure -> BbodyPredicateFailure -> Bool
forall a. Eq a => a -> a -> Bool
== BbodyPredicateFailure
InvalidBlockSize)
        ([BbodyPredicateFailure] -> Bool)
-> [BbodyPredicateFailure] -> Bool
forall a b. (a -> b) -> a -> b
$ NonEmpty ChainPredicateFailure -> [BbodyPredicateFailure]
forall d a. (Data d, Typeable a) => d -> [a]
extractValues NonEmpty ChainPredicateFailure
NonEmpty (PredicateFailure CHAIN)
abstractPfs
      String -> PropertyT IO ()
forall (m :: * -> *). MonadTest m => String -> m ()
footnote
        (String -> PropertyT IO ()) -> String -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ String
"InvalidBlockSize not found in the abstract predicate failures: "
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ NonEmpty ChainPredicateFailure -> String
forall a b. (Show a, ConvertText String b) => a -> b
show NonEmpty ChainPredicateFailure
NonEmpty (PredicateFailure CHAIN)
abstractPfs
    checkMaxSizeFailure NonEmpty (PredicateFailure CHAIN)
_ ChainValidationError
concretePF = do
      String -> PropertyT IO ()
forall (m :: * -> *). MonadTest m => String -> m ()
footnote (String -> PropertyT IO ()) -> String -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ String
"Expected 'ChainValidationBlockTooLarge' error, got " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ChainValidationError -> String
forall a b. (Show a, ConvertText String b) => a -> b
show ChainValidationError
concretePF
      PropertyT IO ()
forall (m :: * -> *) a. (MonadTest m, HasCallStack) => m a
failure