{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

-- | Properties of the delegation traces induced by the transition systems
-- associated with this aspect of the ledger.
module Test.Byron.Spec.Ledger.Delegation.Properties (
  dcertsAreTriggered,
  rejectDupSchedDelegs,
  tracesAreClassified,
  dblockTracesAreClassified,
  relevantCasesAreCovered,
  onlyValidSignalsAreGenerated,
)
where

import Byron.Spec.Ledger.Core (
  Epoch (Epoch),
  Sig (Sig),
  Slot,
  SlotCount (SlotCount),
  VKey,
  VKeyGenesis,
  addSlot,
  mkVKeyGenesis,
  owner,
  unSlot,
  unSlotCount,
 )
import Byron.Spec.Ledger.Core.Generators (epochGen, slotGen, vkGen)
import qualified Byron.Spec.Ledger.Core.Generators as CoreGen
import Byron.Spec.Ledger.Delegation
import Byron.Spec.Ledger.GlobalParams (slotsPerEpoch)
import Control.Arrow (first, (***))
import Control.State.Transition (
  Embed,
  Environment,
  IRC (IRC),
  PredicateFailure,
  STS (..),
  Signal,
  State,
  TRC (TRC),
  applySTS,
  initialRules,
  judgmentContext,
  trans,
  transitionRules,
  wrapFailed,
  (?!),
 )
import Data.Bimap (Bimap)
import qualified Data.Bimap as Bimap
import Data.Data (Data, Typeable)
import Data.Foldable (toList)
import Data.List as F (foldl')
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import Hedgehog (
  Gen,
  MonadTest,
  Property,
  assert,
  cover,
  forAll,
  property,
  success,
  withTests,
  (===),
 )
import qualified Hedgehog.Gen as Gen
import qualified Hedgehog.Range as Range
import Lens.Micro (to, (&), (.~), (^.))
import Lens.Micro.Extras (view)
import Lens.Micro.TH (makeLenses)
import Test.Control.State.Transition.Generator (
  HasSizeInfo,
  HasTrace,
  classifySize,
  classifyTraceLength,
  envGen,
  isTrivial,
  nonTrivialTrace,
  sigGen,
  suchThatLastState,
  trace,
  traceLengthsAreClassified,
 )
import qualified Test.Control.State.Transition.Generator as Transition.Generator
import Test.Control.State.Transition.Trace (
  Trace,
  TraceOrder (OldestFirst),
  lastState,
  preStatesAndSignals,
  traceEnv,
  traceLength,
  traceSignals,
 )

--------------------------------------------------------------------------------
-- Delegation certification triggering tests
--------------------------------------------------------------------------------

-- | Initial state for the ADELEG and ADELEGS systems
initADelegsState :: DState
initADelegsState :: DState
initADelegsState =
  DState
    { _dStateDelegationMap :: Bimap VKeyGenesis VKey
_dStateDelegationMap = forall a b. Bimap a b
Bimap.empty
    , _dStateLastDelegation :: Map VKeyGenesis Slot
_dStateLastDelegation = forall k a. Map k a
Map.empty
    }

-- | Initial state for the ADELEG and ADELEGS systems
initSDelegsState :: DSState
initSDelegsState :: DSState
initSDelegsState =
  DSState
    { _dSStateScheduledDelegations :: [(Slot, (VKeyGenesis, VKey))]
_dSStateScheduledDelegations = []
    , _dSStateKeyEpochDelegations :: Set (Epoch, VKeyGenesis)
_dSStateKeyEpochDelegations = forall a. Set a
Set.empty
    }

-- | Initial state for the DELEG system
initialDIState :: DIState
initialDIState :: DIState
initialDIState =
  DIState
    { _dIStateDelegationMap :: Bimap VKeyGenesis VKey
_dIStateDelegationMap = DState -> Bimap VKeyGenesis VKey
_dStateDelegationMap DState
initADelegsState
    , _dIStateLastDelegation :: Map VKeyGenesis Slot
_dIStateLastDelegation = DState -> Map VKeyGenesis Slot
_dStateLastDelegation DState
initADelegsState
    , _dIStateScheduledDelegations :: [(Slot, (VKeyGenesis, VKey))]
_dIStateScheduledDelegations = DSState
initSDelegsState forall s a. s -> Getting a s a -> a
^. forall s a. HasScheduledDelegations s a => Lens' s a
scheduledDelegations
    , _dIStateKeyEpochDelegations :: Set (Epoch, VKeyGenesis)
_dIStateKeyEpochDelegations = DSState -> Set (Epoch, VKeyGenesis)
_dSStateKeyEpochDelegations DSState
initSDelegsState
    }

-- | Delegation blocks. Simple blockchain to test delegation.
data DBLOCK deriving (Typeable DBLOCK
DBLOCK -> DataType
DBLOCK -> Constr
(forall b. Data b => b -> b) -> DBLOCK -> DBLOCK
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> DBLOCK -> u
forall u. (forall d. Data d => d -> u) -> DBLOCK -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DBLOCK -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DBLOCK -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DBLOCK -> m DBLOCK
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DBLOCK -> m DBLOCK
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DBLOCK
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DBLOCK -> c DBLOCK
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DBLOCK)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DBLOCK)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DBLOCK -> m DBLOCK
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DBLOCK -> m DBLOCK
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DBLOCK -> m DBLOCK
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DBLOCK -> m DBLOCK
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DBLOCK -> m DBLOCK
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DBLOCK -> m DBLOCK
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DBLOCK -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DBLOCK -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> DBLOCK -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> DBLOCK -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DBLOCK -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DBLOCK -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DBLOCK -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DBLOCK -> r
gmapT :: (forall b. Data b => b -> b) -> DBLOCK -> DBLOCK
$cgmapT :: (forall b. Data b => b -> b) -> DBLOCK -> DBLOCK
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DBLOCK)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DBLOCK)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DBLOCK)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DBLOCK)
dataTypeOf :: DBLOCK -> DataType
$cdataTypeOf :: DBLOCK -> DataType
toConstr :: DBLOCK -> Constr
$ctoConstr :: DBLOCK -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DBLOCK
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DBLOCK
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DBLOCK -> c DBLOCK
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DBLOCK -> c DBLOCK
Data, Typeable)

-- | A delegation block.
data DBlock = DBlock
  { DBlock -> Slot
_blockSlot :: Slot
  , DBlock -> [DCert]
_blockCerts :: [DCert]
  }
  deriving (Int -> DBlock -> ShowS
[DBlock] -> ShowS
DBlock -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [DBlock] -> ShowS
$cshowList :: [DBlock] -> ShowS
show :: DBlock -> [Char]
$cshow :: DBlock -> [Char]
showsPrec :: Int -> DBlock -> ShowS
$cshowsPrec :: Int -> DBlock -> ShowS
Show, DBlock -> DBlock -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DBlock -> DBlock -> Bool
$c/= :: DBlock -> DBlock -> Bool
== :: DBlock -> DBlock -> Bool
$c== :: DBlock -> DBlock -> Bool
Eq)

makeLenses ''DBlock

data DBlockPredicateFailure
  = DPF (PredicateFailure DELEG)
  | NotIncreasingBlockSlot
  deriving (DBlockPredicateFailure -> DBlockPredicateFailure -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DBlockPredicateFailure -> DBlockPredicateFailure -> Bool
$c/= :: DBlockPredicateFailure -> DBlockPredicateFailure -> Bool
== :: DBlockPredicateFailure -> DBlockPredicateFailure -> Bool
$c== :: DBlockPredicateFailure -> DBlockPredicateFailure -> Bool
Eq, Int -> DBlockPredicateFailure -> ShowS
[DBlockPredicateFailure] -> ShowS
DBlockPredicateFailure -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [DBlockPredicateFailure] -> ShowS
$cshowList :: [DBlockPredicateFailure] -> ShowS
show :: DBlockPredicateFailure -> [Char]
$cshow :: DBlockPredicateFailure -> [Char]
showsPrec :: Int -> DBlockPredicateFailure -> ShowS
$cshowsPrec :: Int -> DBlockPredicateFailure -> ShowS
Show, Typeable DBlockPredicateFailure
DBlockPredicateFailure -> DataType
DBlockPredicateFailure -> Constr
(forall b. Data b => b -> b)
-> DBlockPredicateFailure -> DBlockPredicateFailure
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> DBlockPredicateFailure -> u
forall u.
(forall d. Data d => d -> u) -> DBlockPredicateFailure -> [u]
forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> DBlockPredicateFailure
-> r
forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> DBlockPredicateFailure
-> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> DBlockPredicateFailure -> m DBlockPredicateFailure
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DBlockPredicateFailure -> m DBlockPredicateFailure
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DBlockPredicateFailure
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> DBlockPredicateFailure
-> c DBlockPredicateFailure
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DBlockPredicateFailure)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DBlockPredicateFailure)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DBlockPredicateFailure -> m DBlockPredicateFailure
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DBlockPredicateFailure -> m DBlockPredicateFailure
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DBlockPredicateFailure -> m DBlockPredicateFailure
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DBlockPredicateFailure -> m DBlockPredicateFailure
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> DBlockPredicateFailure -> m DBlockPredicateFailure
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> DBlockPredicateFailure -> m DBlockPredicateFailure
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> DBlockPredicateFailure -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> DBlockPredicateFailure -> u
gmapQ :: forall u.
(forall d. Data d => d -> u) -> DBlockPredicateFailure -> [u]
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> DBlockPredicateFailure -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> DBlockPredicateFailure
-> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> DBlockPredicateFailure
-> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> DBlockPredicateFailure
-> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> DBlockPredicateFailure
-> r
gmapT :: (forall b. Data b => b -> b)
-> DBlockPredicateFailure -> DBlockPredicateFailure
$cgmapT :: (forall b. Data b => b -> b)
-> DBlockPredicateFailure -> DBlockPredicateFailure
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DBlockPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DBlockPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DBlockPredicateFailure)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DBlockPredicateFailure)
dataTypeOf :: DBlockPredicateFailure -> DataType
$cdataTypeOf :: DBlockPredicateFailure -> DataType
toConstr :: DBlockPredicateFailure -> Constr
$ctoConstr :: DBlockPredicateFailure -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DBlockPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DBlockPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> DBlockPredicateFailure
-> c DBlockPredicateFailure
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> DBlockPredicateFailure
-> c DBlockPredicateFailure
Data, Typeable)

-- | This corresponds to a state-transition rule where blocks with increasing
-- slot-numbers are produced.
instance STS DBLOCK where
  type Environment DBLOCK = DSEnv -- The initial environment is only used to bootstrap the initial state.
  type State DBLOCK = (DSEnv, DIState)
  type Signal DBLOCK = DBlock
  type PredicateFailure DBLOCK = DBlockPredicateFailure

  initialRules :: [InitialRule DBLOCK]
initialRules =
    [ do
        IRC Environment DBLOCK
env <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Environment DBLOCK
env, DIState
initialDIState)
    ]

  transitionRules :: [TransitionRule DBLOCK]
transitionRules =
    [ do
        TRC (Environment DBLOCK
_, (DIEnv
env, DIState
st), Signal DBLOCK
dblock) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        let nextSlot :: Slot
nextSlot = Signal DBLOCK
dblock forall s a. s -> Getting a s a -> a
^. Lens' DBlock Slot
blockSlot
        DIEnv
env forall s a. s -> Getting a s a -> a
^. forall s a. HasSlot s a => Lens' s a
slot forall a. Ord a => a -> a -> Bool
< Slot
nextSlot forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! DBlockPredicateFailure
NotIncreasingBlockSlot
        DIState
stNext <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @DELEG forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (DIEnv
env, DIState
st, Signal DBLOCK
dblock forall s a. s -> Getting a s a -> a
^. Lens' DBlock [DCert]
blockCerts)
        let nextEpoch :: Epoch
nextEpoch =
              if DIEnv -> BlockCount
_dSEnvK DIEnv
env forall a. Eq a => a -> a -> Bool
== BlockCount
0
                then Epoch
0
                else Word64 -> Epoch
Epoch forall a b. (a -> b) -> a -> b
$ Slot -> Word64
unSlot Slot
nextSlot forall a. Integral a => a -> a -> a
`div` forall n. Integral n => BlockCount -> n
slotsPerEpoch (DIEnv -> BlockCount
_dSEnvK DIEnv
env)
        forall (m :: * -> *) a. Monad m => a -> m a
return
          ( DIEnv
env
              forall a b. a -> (a -> b) -> b
& forall s a. HasSlot s a => Lens' s a
slot forall s t a b. ASetter s t a b -> b -> s -> t
.~ Slot
nextSlot
              forall a b. a -> (a -> b) -> b
& forall s a. HasEpoch s a => Lens' s a
epoch forall s t a b. ASetter s t a b -> b -> s -> t
.~ Epoch
nextEpoch
          , DIState
stNext
          )
    ]

instance Embed DELEG DBLOCK where
  wrapFailed :: PredicateFailure DELEG -> PredicateFailure DBLOCK
wrapFailed = PredicateFailure DELEG -> DBlockPredicateFailure
DPF

-- | Check that all the delegation certificates in the trace were correctly
-- applied.
dcertsAreTriggeredInTrace :: MonadTest m => Trace DBLOCK -> m ()
dcertsAreTriggeredInTrace :: forall (m :: * -> *). MonadTest m => Trace DBLOCK -> m ()
dcertsAreTriggeredInTrace Trace DBLOCK
tr =
  Bimap VKeyGenesis VKey
lastDms forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== Bimap VKeyGenesis VKey
trExpectedDms
  where
    lastDms :: Bimap VKeyGenesis VKey
lastDms = DIState
st forall s a. s -> Getting a s a -> a
^. forall s a. HasDelegationMap s a => Lens' s a
delegationMap

    trExpectedDms :: Bimap VKeyGenesis VKey
trExpectedDms =
      Int -> Int -> [(Int, DBlock)] -> Bimap VKeyGenesis VKey
expectedDms
        Int
lastSlot
        ((forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. SlotCount -> Word64
unSlotCount forall b c a. (b -> c) -> (a -> b) -> a -> c
. BlockCount -> SlotCount
liveAfter) (DIEnv -> BlockCount
_dSEnvK DIEnv
env))
        [(Int, DBlock)]
slotsAndDcerts

    (DIEnv
env, DIState
st) = forall s. Trace s -> State s
lastState Trace DBLOCK
tr

    lastSlot :: Int
    lastSlot :: Int
lastSlot = forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> a
last forall a b. (a -> b) -> a -> b
$ [(Int, DBlock)]
slotsAndDcerts

    slotsAndDcerts :: [(Int, DBlock)]
    slotsAndDcerts :: [(Int, DBlock)]
slotsAndDcerts =
      forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (forall a s. Getting a s a -> s -> a
view (forall s a. (s -> a) -> SimpleGetter s a
to forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s a. HasSlot s a => Lens' s a
slot forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s a. (s -> a) -> SimpleGetter s a
to Slot -> Word64
unSlot forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s a. (s -> a) -> SimpleGetter s a
to forall a b. (Integral a, Num b) => a -> b
fromIntegral))
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s. TraceOrder -> Trace s -> [(State s, Signal s)]
preStatesAndSignals TraceOrder
OldestFirst Trace DBLOCK
tr

-- | Compute the expected delegation map after applying the sequence of
-- delegation certificates contained in the given blocks.
--
-- Delegation certificates are applied in the order they appear in the within a
-- block, and blocks are considered in the order they appear on the list passed
-- as parameter.
expectedDms ::
  -- | Last slot that should have been considered for certificate activation.
  Int ->
  -- | Delegation certificate liveness parameter.
  Int ->
  -- | Delegation certificates to apply, and the slot at which these
  -- certificates where scheduled.
  [(Int, DBlock)] ->
  Bimap VKeyGenesis VKey
expectedDms :: Int -> Int -> [(Int, DBlock)] -> Bimap VKeyGenesis VKey
expectedDms Int
s Int
d [(Int, DBlock)]
sbs =
  forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
F.foldl' Bimap VKeyGenesis VKey
-> (VKeyGenesis, VKey) -> Bimap VKeyGenesis VKey
insertIfInjective forall a b. Bimap a b
Bimap.empty (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DCert -> (VKeyGenesis, VKey)
delegatorDelegate [DCert]
activeCerts)
  where
    insertIfInjective ::
      Bimap VKeyGenesis VKey ->
      (VKeyGenesis, VKey) ->
      Bimap VKeyGenesis VKey
    insertIfInjective :: Bimap VKeyGenesis VKey
-> (VKeyGenesis, VKey) -> Bimap VKeyGenesis VKey
insertIfInjective Bimap VKeyGenesis VKey
m (VKeyGenesis
k, VKey
v) =
      if forall a b. (Ord a, Ord b) => b -> Bimap a b -> Bool
Bimap.memberR VKey
v Bimap VKeyGenesis VKey
m
        then Bimap VKeyGenesis VKey
m
        else forall a b. (Ord a, Ord b) => a -> b -> Bimap a b -> Bimap a b
Bimap.insert VKeyGenesis
k VKey
v Bimap VKeyGenesis VKey
m
    activeCerts :: [DCert]
    activeCerts :: [DCert]
activeCerts = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DBlock -> [DCert]
_blockCerts [DBlock]
activeBlocks

    activeBlocks :: [DBlock]
    activeBlocks :: [DBlock]
activeBlocks =
      forall a b. (a, b) -> b
snd
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Ord a => a -> a -> Bool
<= Int
activationSlot) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Int, DBlock)]
sbs

    activationSlot :: Int
    activationSlot :: Int
activationSlot = Int
s forall a. Num a => a -> a -> a
- Int
d

instance HasTrace DBLOCK where
  envGen :: Word64 -> Gen (Environment DBLOCK)
envGen
    Word64
chainLength =
      Set VKeyGenesis -> Epoch -> Slot -> BlockCount -> DIEnv
DSEnv
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenT Identity (Set VKeyGenesis)
allowedDelegators'
        -- We do not expect the current epoch to have an influence on the tests, so
        -- we chose a small value here.
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Word64 -> Word64 -> Gen Epoch
epochGen Word64
0 Word64
10
        -- As with epochs, the current slot should not have influence in the tests.
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Word64 -> Word64 -> Gen Slot
slotGen Word64
0 Word64
10
        -- 2160 the value of @k@ used in production. However, delegation certificates are activated
        -- @2*k@ slots from the slot in which they are issued. This means that if we want to see
        -- delegation activations, we need to choose a small value for @k@ since we do not want to blow
        -- up the testing time by using large trace lengths.
        --
        -- Choosing a small @k@ value amounts to picking a large number of epochs. Given a trace length
        -- of @n@, if we have @10k@ slots per-epoch, we can have at most @n `div` 10@ epochs (by
        -- choosing @k == 1@).
        --
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Word64 -> Word64 -> Gen BlockCount
CoreGen.k Word64
chainLength (Word64
chainLength forall a. Integral a => a -> a -> a
`div` Word64
10)
      where
        -- We scale the number of delegators linearly up to twice the number of genesis keys we use in
        -- production. Factor 2 is chosen ad-hoc here.
        allowedDelegators' :: GenT Identity (Set VKeyGenesis)
allowedDelegators' = do
          Natural
n <- forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (forall a. Integral a => a -> a -> Range a
Range.linear Natural
0 Natural
13)
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! forall a. Eq a => [a] -> Set a
Set.fromAscList forall a b. (a -> b) -> a -> b
$ Natural -> VKeyGenesis
mkVKeyGenesis forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Natural
0 .. Natural
n]

  sigGen :: SignalGenerator DBLOCK
sigGen Environment DBLOCK
_ (DIEnv
env, DIState
st) =
    Slot -> [DCert] -> DBlock
DBlock forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DIEnv -> Gen Slot
nextSlotGen DIEnv
env forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall s. HasTrace s => SignalGenerator s
sigGen @DELEG DIEnv
env DIState
st

-- | Generate a next slot. We want the resulting trace to include a large number of epoch changes,
-- so we generate an epoch change with higher frequency.
nextSlotGen :: DSEnv -> Gen Slot
nextSlotGen :: DIEnv -> Gen Slot
nextSlotGen DIEnv
env =
  Word64 -> Slot
incSlot
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadGen m => [(Int, m a)] -> m a
Gen.frequency
      [ (Int
1, forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (forall a. a -> a -> Range a
Range.constant Word64
1 Word64
10))
      , (Int
2, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! forall n. Integral n => BlockCount -> n
slotsPerEpoch (DIEnv -> BlockCount
_dSEnvK DIEnv
env))
      ]
  where
    incSlot :: Word64 -> Slot
incSlot Word64
c = (DIEnv
env forall s a. s -> Getting a s a -> a
^. forall s a. HasSlot s a => Lens' s a
slot) Slot -> SlotCount -> Slot
`addSlot` Word64 -> SlotCount
SlotCount Word64
c

instance HasSizeInfo DBlock where
  isTrivial :: DBlock -> Bool
isTrivial = forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a s. Getting a s a -> s -> a
view Lens' DBlock [DCert]
blockCerts

dcertsAreTriggered :: Property
dcertsAreTriggered :: Property
dcertsAreTriggered =
  TestLimit -> Property -> Property
withTests TestLimit
300 forall a b. (a -> b) -> a -> b
$
    HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$
      -- The number of tests was determined ad-hoc, since the default failed to
      -- uncover the presence of errors.
      forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (forall s.
(HasTrace s, HasSizeInfo (Signal s)) =>
BaseEnv s -> Word64 -> Gen (Trace s)
nonTrivialTrace () Word64
100) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *). MonadTest m => Trace DBLOCK -> m ()
dcertsAreTriggeredInTrace

dblockTracesAreClassified :: Property
dblockTracesAreClassified :: Property
dblockTracesAreClassified = TestLimit -> Property -> Property
withTests TestLimit
200 forall a b. (a -> b) -> a -> b
$
  HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
    let (Word64
tl, Word64
step) = (Word64
100, Word64
10)
    Trace DBLOCK
tr <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (forall s. HasTrace s => BaseEnv s -> Word64 -> Gen (Trace s)
trace @DBLOCK () Word64
tl)
    forall s. Trace s -> Word64 -> Word64 -> PropertyT IO ()
classifyTraceLength Trace DBLOCK
tr Word64
tl Word64
step
    -- Classify the traces by the total number of delegation certificates on
    -- them.
    forall n a.
(Show n, Integral n) =>
[Char] -> a -> (a -> n) -> n -> n -> PropertyT IO ()
classifySize [Char]
"total dcerts" (Trace DBLOCK -> [DCert]
traceDCerts Trace DBLOCK
tr) (forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Int
length) Word64
tl Word64
step
    forall (m :: * -> *). MonadTest m => m ()
success

-- | Extract the delegation certificates in the blocks, in the order they would
-- have been applied.
traceDCertsByBlock :: Trace DBLOCK -> [[DCert]]
traceDCertsByBlock :: Trace DBLOCK -> [[DCert]]
traceDCertsByBlock Trace DBLOCK
tr = DBlock -> [DCert]
_blockCerts forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace DBLOCK
tr

-- | Flattended list of DCerts for the given Trace
traceDCerts :: Trace DBLOCK -> [DCert]
traceDCerts :: Trace DBLOCK -> [DCert]
traceDCerts = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. Trace DBLOCK -> [[DCert]]
traceDCertsByBlock

relevantCasesAreCovered :: Property
relevantCasesAreCovered :: Property
relevantCasesAreCovered = TestLimit -> Property -> Property
withTests TestLimit
400 forall a b. (a -> b) -> a -> b
$
  HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
    let tl :: Word64
tl = Word64
100
    Trace DBLOCK
tr <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (forall s. HasTrace s => BaseEnv s -> Word64 -> Gen (Trace s)
trace @DBLOCK () Word64
tl)

    -- 40% of the traces must contain as many delegation certificates as blocks.
    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
40
      LabelName
"there are at least as many delegation certificates as blocks"
      (forall s. Trace s -> Int
traceLength Trace DBLOCK
tr forall a. Ord a => a -> a -> Bool
<= forall (t :: * -> *) a. Foldable t => t a -> Int
length (Trace DBLOCK -> [DCert]
traceDCerts Trace DBLOCK
tr))

    -- 50% of the traces must contain at most 25% of blocks with empty delegation payload.
    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
50
      LabelName
"at most 25% of the blocks can contain empty delegation payload"
      (Double
0.25 forall a. Ord a => a -> a -> Bool
>= [[DCert]] -> Double
emptyDelegationPayloadRatio (Trace DBLOCK -> [[DCert]]
traceDCertsByBlock Trace DBLOCK
tr))

    -- 50% of the traces must contain at least 30% of delegations to this epoch.
    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
50
      LabelName
"at least 30% of all certificates delegate in this epoch"
      (Double
0.3 forall a. Ord a => a -> a -> Bool
<= [(Epoch, Epoch)] -> Double
thisEpochDelegationsRatio (Trace DBLOCK -> [(Epoch, Epoch)]
epochDelegationEpoch Trace DBLOCK
tr))

    -- 70% of the traces must contain at least 50% of delegations to the next
    -- epoch.
    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
70
      LabelName
"at least 50% of the certificates delegate in the next epoch"
      (Double
0.5 forall a. Ord a => a -> a -> Bool
<= [(Epoch, Epoch)] -> Double
nextEpochDelegationsRatio (Trace DBLOCK -> [(Epoch, Epoch)]
epochDelegationEpoch Trace DBLOCK
tr))

    -- 30% of the traces must contain at least 30% of self-delegations.
    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
30
      LabelName
"at least 30% of the certificates self delegate"
      (Double
0.3 forall a. Ord a => a -> a -> Bool
<= [DCert] -> Double
selfDelegationsRatio (Trace DBLOCK -> [DCert]
traceDCerts Trace DBLOCK
tr))

    -- 15% of the traces must contain at least 10% of delegations to the same
    -- delegate.
    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
50
      LabelName
"at least 25% of delegates have multiple delegators"
      (Double
0.05 forall a. Ord a => a -> a -> Bool
<= [DCert] -> Double
multipleDelegationsRatio (Trace DBLOCK -> [DCert]
traceDCerts Trace DBLOCK
tr))
  where
    -- Get the epoch in which the delegation certificates of the trace were
    -- applied, paired with the epoch of the delegation certificate.
    epochDelegationEpoch :: Trace DBLOCK -> [(Epoch, Epoch)]
    epochDelegationEpoch :: Trace DBLOCK -> [(Epoch, Epoch)]
epochDelegationEpoch Trace DBLOCK
tr =
      forall s. TraceOrder -> Trace s -> [(State s, Signal s)]
preStatesAndSignals @DBLOCK TraceOrder
OldestFirst Trace DBLOCK
tr
        forall a b. a -> (a -> b) -> b
& forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (DIEnv -> Epoch
_dSEnvEpoch forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DCert -> Epoch
depoch forall b c a. (b -> c) -> (a -> b) -> a -> c
. DBlock -> [DCert]
_blockCerts))
        forall a b. a -> (a -> b) -> b
& forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Epoch
e, [Epoch]
es) -> forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. a -> [a]
repeat Epoch
e) [Epoch]
es)
        forall a b. a -> (a -> b) -> b
& forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat

onlyValidSignalsAreGenerated :: Property
onlyValidSignalsAreGenerated :: Property
onlyValidSignalsAreGenerated =
  TestLimit -> Property -> Property
withTests TestLimit
300 forall a b. (a -> b) -> a -> b
$ forall s.
(HasTrace s, Show (Environment s), Show (State s), Show (Signal s),
 HasCallStack) =>
BaseEnv s -> Word64 -> Property
Transition.Generator.onlyValidSignalsAreGenerated @DBLOCK () Word64
100

--------------------------------------------------------------------------------
-- Properties related to the transition rules
--------------------------------------------------------------------------------

-- | Reject delegation certificates where a genesis key tries to delegate in
-- the same slot.
--
-- This property tries to generate a trace where the last state contains a
-- non-empty sequence of scheduled delegations. If such trace cannot be
-- generated, then the test will fail when the heap limit is reached, or
-- hedgehog gives up.
rejectDupSchedDelegs :: Property
rejectDupSchedDelegs :: Property
rejectDupSchedDelegs = TestLimit -> Property -> Property
withTests TestLimit
300 forall a b. (a -> b) -> a -> b
$
  HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
    (Trace DELEG
tr, DCert
dcert) <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ do
      Trace DELEG
tr <-
        forall s. HasTrace s => BaseEnv s -> Word64 -> Gen (Trace s)
trace @DELEG () Word64
100
          forall s. Gen (Trace s) -> (State s -> Bool) -> Gen (Trace s)
`suchThatLastState` (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a s. Getting a s a -> s -> a
view forall s a. HasScheduledDelegations s a => Lens' s a
scheduledDelegations)
      let vkS :: VKeyGenesis
vkS =
            case forall s. Trace s -> State s
lastState Trace DELEG
tr forall s a. s -> Getting a s a -> a
^. forall s a. HasScheduledDelegations s a => Lens' s a
scheduledDelegations of
              (Slot
_, (VKeyGenesis
res, VKey
_)) : [(Slot, (VKeyGenesis, VKey))]
_ -> VKeyGenesis
res
              [(Slot, (VKeyGenesis, VKey))]
_ ->
                forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$
                  [Char]
"This should not happen: "
                    forall a. [a] -> [a] -> [a]
++ [Char]
"tr is guaranteed to contain a non-empty sequence of scheduled delegations"
      VKey
vkD <- Gen VKey
vkGen
      Epoch
epo <- Word64 -> Epoch
Epoch 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. Integral a => a -> a -> Range a
Range.linear Word64
0 Word64
100)
      let dcert :: DCert
dcert = VKeyGenesis -> Sig (VKey, Epoch) -> VKey -> Epoch -> DCert
mkDCert VKeyGenesis
vkS (forall a. a -> Owner -> Sig a
Sig (VKey
vkD, Epoch
epo) (forall a. HasOwner a => a -> Owner
owner VKeyGenesis
vkS)) VKey
vkD Epoch
epo
      forall (m :: * -> *) a. Monad m => a -> m a
return (Trace DELEG
tr, DCert
dcert)
    let pfs :: [DelegPredicateFailure]
pfs = case forall s (rtype :: RuleType).
(STS s, RuleTypeRep rtype, BaseM s ~ Identity) =>
RuleContext rtype s
-> Either (NonEmpty (PredicateFailure s)) (State s)
applySTS @DELEG (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Trace DELEG
tr forall s a. s -> Getting a s a -> a
^. forall s. Lens' (Trace s) (Environment s)
traceEnv, forall s. Trace s -> State s
lastState Trace DELEG
tr, [DCert
dcert])) of
          Left NonEmpty (PredicateFailure DELEG)
res -> forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty (PredicateFailure DELEG)
res
          Right State DELEG
_ -> []
    forall (m :: * -> *). (MonadTest m, HasCallStack) => Bool -> m ()
assert forall a b. (a -> b) -> a -> b
$ PredicateFailure SDELEGS -> DelegPredicateFailure
SDelegSFailure (PredicateFailure SDELEG -> SdelegsPredicateFailure
SDelegFailure SdelegPredicateFailure
IsAlreadyScheduled) forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [DelegPredicateFailure]
pfs

-- | Classify the traces.
tracesAreClassified :: Property
tracesAreClassified :: Property
tracesAreClassified = forall s.
(HasTrace s, Show (Environment s), Show (State s),
 Show (Signal s)) =>
BaseEnv s -> Word64 -> Word64 -> Property
traceLengthsAreClassified @DELEG () Word64
1000 Word64
100