{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

module Test.Byron.Spec.Chain.STS.Properties where

import Byron.Spec.Chain.STS.Block
import Byron.Spec.Chain.STS.Rule.Chain
import Byron.Spec.Chain.STS.Rule.Epoch (sEpoch)
import Byron.Spec.Ledger.Core (BlockCount (BlockCount), Epoch, Slot (unSlot))
import Byron.Spec.Ledger.Delegation
import Byron.Spec.Ledger.GlobalParams (slotsPerEpoch)
import Control.Arrow ((***))
import Control.State.Transition
import Data.Foldable (traverse_)
import Data.List.Ordered (nubSortBy)
import Data.Ord (Down (Down), comparing)
import Hedgehog (
  MonadTest,
  Property,
  assert,
  cover,
  failure,
  forAll,
  property,
  withTests,
  (===),
 )
import Lens.Micro ((&), (^.), (^..), _1, _5)
import Lens.Micro.Extras (view)
import Test.Control.State.Transition.Generator (
  TraceLength (Desired, Maximum),
  classifyTraceLength,
  traceSigGen,
 )
import qualified Test.Control.State.Transition.Generator as Transition.Generator
import Test.Control.State.Transition.Trace

slotsIncrease :: Property
slotsIncrease :: Property
slotsIncrease = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  let (Word64
maxTraceLength, Word64
step) = (Word64
100, Word64
10)
  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
$
      BaseEnv CHAIN
-> TraceLength -> SignalGenerator CHAIN -> Gen (Trace CHAIN)
forall s.
HasTrace s =>
BaseEnv s -> TraceLength -> SignalGenerator s -> Gen (Trace s)
traceSigGen
        ()
        (Word64 -> TraceLength
Maximum Word64
maxTraceLength)
        (ShouldGenDelegation
-> ShouldGenUTxO -> ShouldGenUpdate -> SignalGenerator CHAIN
sigGenChain ShouldGenDelegation
NoGenDelegation ShouldGenUTxO
NoGenUTxO ShouldGenUpdate
NoGenUpdate)
  Trace CHAIN -> Word64 -> Word64 -> PropertyT IO ()
forall s. Trace s -> Word64 -> Word64 -> PropertyT IO ()
classifyTraceLength Trace CHAIN
tr Word64
maxTraceLength Word64
step
  Trace CHAIN -> PropertyT IO ()
forall (m :: * -> *). MonadTest m => Trace CHAIN -> m ()
slotsIncreaseInTrace Trace CHAIN
tr

slotsIncreaseInTrace :: MonadTest m => Trace CHAIN -> m ()
slotsIncreaseInTrace :: forall (m :: * -> *). MonadTest m => Trace CHAIN -> m ()
slotsIncreaseInTrace Trace CHAIN
tr = [Slot]
slots [Slot] -> [Slot] -> m ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== (Slot -> Slot -> Ordering) -> [Slot] -> [Slot]
forall a. (a -> a -> Ordering) -> [a] -> [a]
nubSortBy ((Slot -> Down Slot) -> Slot -> Slot -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing Slot -> Down Slot
forall a. a -> Down a
Down) [Slot]
slots
  where
    blocks :: [Signal CHAIN]
blocks = TraceOrder -> Trace CHAIN -> [Signal CHAIN]
forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
NewestFirst Trace CHAIN
tr
    slots :: [Slot]
slots = [Block]
[Signal CHAIN]
blocks [Block] -> Getting (Endo [Slot]) [Block] Slot -> [Slot]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. (Block -> Const (Endo [Slot]) Block)
-> [Block] -> Const (Endo [Slot]) [Block]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((Block -> Const (Endo [Slot]) Block)
 -> [Block] -> Const (Endo [Slot]) [Block])
-> ((Slot -> Const (Endo [Slot]) Slot)
    -> Block -> Const (Endo [Slot]) Block)
-> Getting (Endo [Slot]) [Block] Slot
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BlockHeader -> Const (Endo [Slot]) BlockHeader)
-> Block -> Const (Endo [Slot]) Block
Lens' Block BlockHeader
bHeader ((BlockHeader -> Const (Endo [Slot]) BlockHeader)
 -> Block -> Const (Endo [Slot]) Block)
-> ((Slot -> Const (Endo [Slot]) Slot)
    -> BlockHeader -> Const (Endo [Slot]) BlockHeader)
-> (Slot -> Const (Endo [Slot]) Slot)
-> Block
-> Const (Endo [Slot]) Block
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Slot -> Const (Endo [Slot]) Slot)
-> BlockHeader -> Const (Endo [Slot]) BlockHeader
Lens' BlockHeader Slot
bhSlot

blockIssuersAreDelegates :: Property
blockIssuersAreDelegates :: Property
blockIssuersAreDelegates =
  TestLimit -> Property -> Property
withTests TestLimit
300 (Property -> Property) -> Property -> Property
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
maxTraceLength, Word64
step) = (Word64
100, Word64
10)
      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
$
          BaseEnv CHAIN
-> TraceLength -> SignalGenerator CHAIN -> Gen (Trace CHAIN)
forall s.
HasTrace s =>
BaseEnv s -> TraceLength -> SignalGenerator s -> Gen (Trace s)
traceSigGen
            ()
            (Word64 -> TraceLength
Maximum Word64
maxTraceLength)
            (ShouldGenDelegation
-> ShouldGenUTxO -> ShouldGenUpdate -> SignalGenerator CHAIN
sigGenChain ShouldGenDelegation
GenDelegation ShouldGenUTxO
NoGenUTxO ShouldGenUpdate
GenUpdate)
      Trace CHAIN -> Word64 -> Word64 -> PropertyT IO ()
forall s. Trace s -> Word64 -> Word64 -> PropertyT IO ()
classifyTraceLength Trace CHAIN
tr Word64
maxTraceLength Word64
step
      Trace CHAIN -> PropertyT IO ()
forall (m :: * -> *). MonadTest m => Trace CHAIN -> m ()
checkBlockIssuersAreDelegates Trace CHAIN
tr
  where
    checkBlockIssuersAreDelegates :: MonadTest m => Trace CHAIN -> m ()
    checkBlockIssuersAreDelegates :: forall (m :: * -> *). MonadTest m => Trace CHAIN -> m ()
checkBlockIssuersAreDelegates Trace CHAIN
tr =
      (((Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState),
  Block)
 -> m ())
-> [((Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState),
     Block)]
-> m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ ((Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState),
 Block)
-> m ()
(State CHAIN, Signal CHAIN) -> m ()
forall (m :: * -> *).
MonadTest m =>
(State CHAIN, Signal CHAIN) -> m ()
checkIssuer ([((Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState),
   Block)]
 -> m ())
-> [((Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState),
     Block)]
-> m ()
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
        checkIssuer :: MonadTest m => (State CHAIN, Signal CHAIN) -> m ()
        checkIssuer :: forall (m :: * -> *).
MonadTest m =>
(State CHAIN, Signal CHAIN) -> m ()
checkIssuer (State CHAIN
st, Signal CHAIN
bk) =
          case Bimap VKeyGenesis VKey -> VKey -> Maybe VKeyGenesis
delegatorOf Bimap VKeyGenesis VKey
dm VKey
issuer of
            Just VKeyGenesis
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
            Maybe VKeyGenesis
Nothing -> m ()
forall (m :: * -> *) a. (MonadTest m, HasCallStack) => m a
failure
          where
            issuer :: VKey
issuer = Block
Signal CHAIN
bk 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
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
. (VKey -> Const VKey VKey) -> BlockHeader -> Const VKey BlockHeader
Lens' BlockHeader VKey
bhIssuer
            dm :: Bimap VKeyGenesis VKey
dm = (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
State CHAIN
st (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Getting
     (Bimap VKeyGenesis VKey)
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
     (Bimap VKeyGenesis VKey)
-> Bimap VKeyGenesis VKey
forall s a. s -> Getting a s a -> a
^. (DIState -> Const (Bimap VKeyGenesis VKey) DIState)
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Const
     (Bimap VKeyGenesis VKey)
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
(DIState -> Const (Bimap VKeyGenesis VKey) DIState)
-> State CHAIN -> Const (Bimap VKeyGenesis VKey) (State CHAIN)
Lens' (State CHAIN) DIState
disL ((DIState -> Const (Bimap VKeyGenesis VKey) DIState)
 -> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
 -> Const
      (Bimap VKeyGenesis VKey)
      (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState))
-> ((Bimap VKeyGenesis VKey
     -> Const (Bimap VKeyGenesis VKey) (Bimap VKeyGenesis VKey))
    -> DIState -> Const (Bimap VKeyGenesis VKey) DIState)
-> Getting
     (Bimap VKeyGenesis VKey)
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
     (Bimap VKeyGenesis VKey)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bimap VKeyGenesis VKey
 -> Const (Bimap VKeyGenesis VKey) (Bimap VKeyGenesis VKey))
-> DIState -> Const (Bimap VKeyGenesis VKey) DIState
forall s a. HasDelegationMap s a => Lens' s a
Lens' DIState (Bimap VKeyGenesis VKey)
delegationMap

onlyValidSignalsAreGenerated :: Property
onlyValidSignalsAreGenerated :: Property
onlyValidSignalsAreGenerated =
  TestLimit -> Property -> Property
withTests TestLimit
200 (Property -> Property) -> Property -> Property
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 @CHAIN () Word64
100

signersListIsBoundedByK :: Property
signersListIsBoundedByK :: Property
signersListIsBoundedByK = TestLimit -> Property -> Property
withTests TestLimit
300 (Property -> Property) -> Property -> Property
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 maxTraceLength :: Word64
maxTraceLength = Word64
100
    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
$
        BaseEnv CHAIN
-> TraceLength -> SignalGenerator CHAIN -> Gen (Trace CHAIN)
forall s.
HasTrace s =>
BaseEnv s -> TraceLength -> SignalGenerator s -> Gen (Trace s)
traceSigGen
          ()
          (Word64 -> TraceLength
Maximum Word64
maxTraceLength)
          (ShouldGenDelegation
-> ShouldGenUTxO -> ShouldGenUpdate -> SignalGenerator CHAIN
sigGenChain ShouldGenDelegation
GenDelegation ShouldGenUTxO
NoGenUTxO ShouldGenUpdate
GenUpdate)
    Trace CHAIN -> PropertyT IO ()
forall (m :: * -> *). MonadTest m => Trace CHAIN -> m ()
signersListIsBoundedByKInTrace Trace CHAIN
tr
  where
    signersListIsBoundedByKInTrace :: MonadTest m => Trace CHAIN -> m ()
    signersListIsBoundedByKInTrace :: forall (m :: * -> *). MonadTest m => Trace CHAIN -> m ()
signersListIsBoundedByKInTrace Trace CHAIN
tr =
      ((Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
 -> m ())
-> [(Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)]
-> m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (BlockCount -> State CHAIN -> m ()
forall (m :: * -> *).
MonadTest m =>
BlockCount -> State CHAIN -> m ()
signersListIsBoundedByKInState BlockCount
k) ([(Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)]
 -> m ())
-> [(Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)]
-> m ()
forall a b. (a -> b) -> a -> b
$ TraceOrder -> Trace CHAIN -> [State CHAIN]
forall s. TraceOrder -> Trace s -> [State s]
traceStates TraceOrder
OldestFirst Trace CHAIN
tr
      where
        (Slot
_, UTxO
_, Set VKeyGenesis
_, PParams
_, BlockCount
k) = forall s. Trace s -> Environment s
_traceEnv @CHAIN Trace CHAIN
tr

        signersListIsBoundedByKInState :: MonadTest m => BlockCount -> State CHAIN -> m ()
        signersListIsBoundedByKInState :: forall (m :: * -> *).
MonadTest m =>
BlockCount -> State CHAIN -> m ()
signersListIsBoundedByKInState (BlockCount Word64
k') (Slot
_sLast, Seq VKeyGenesis
sgs, Hash
_h, UTxOState
_utxoSt, DIState
_ds, UPIState
_us) =
          Bool -> m ()
forall (m :: * -> *). (MonadTest m, HasCallStack) => Bool -> m ()
assert (Bool -> m ()) -> Bool -> m ()
forall a b. (a -> b) -> a -> b
$ Seq VKeyGenesis -> Int
forall a. Seq a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq VKeyGenesis
sgs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
k'

relevantCasesAreCovered :: Property
relevantCasesAreCovered :: Property
relevantCasesAreCovered = TestLimit -> Property -> Property
withTests TestLimit
200 (Property -> Property) -> Property -> Property
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
$ BaseEnv CHAIN
-> TraceLength -> SignalGenerator CHAIN -> Gen (Trace CHAIN)
forall s.
HasTrace s =>
BaseEnv s -> TraceLength -> SignalGenerator s -> Gen (Trace s)
traceSigGen () (Word64 -> TraceLength
Desired Word64
200) (ShouldGenDelegation
-> ShouldGenUTxO -> ShouldGenUpdate -> SignalGenerator CHAIN
sigGenChain ShouldGenDelegation
GenDelegation ShouldGenUTxO
NoGenUTxO ShouldGenUpdate
NoGenUpdate)
    let certs :: [DCert]
certs = Trace CHAIN -> [DCert]
traceDCerts Trace CHAIN
tr

    -- for at least 1% of traces...
    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
1
      LabelName
"there are more certificates than blocks"
      (Trace CHAIN -> Int
forall s. Trace s -> Int
traceLength Trace CHAIN
tr Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [DCert] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DCert]
certs)

    -- for at least 10% of traces...
    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
10
      LabelName
"at most 75% of blocks have no certificates"
      ([[DCert]] -> Double
emptyDelegationPayloadRatio (Trace CHAIN -> [[DCert]]
traceDCertsByBlock Trace CHAIN
tr) Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Double
0.75)

    -- for at least 25% of traces...
    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
25
      LabelName
"at least 25% of delegates will delegate to this epoch"
      (Double
0.25 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= [(Epoch, Epoch)] -> Double
thisEpochDelegationsRatio (Trace CHAIN -> [(Epoch, Epoch)]
epochDelegationEpoch Trace CHAIN
tr))

    -- for at least 60% of traces...
    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
60
      LabelName
"at least 50% of delegations will delegate to the next epoch"
      (Double
0.5 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= [(Epoch, Epoch)] -> Double
nextEpochDelegationsRatio (Trace CHAIN -> [(Epoch, Epoch)]
epochDelegationEpoch Trace CHAIN
tr))

    -- for at least 10% of traces...
    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
10
      LabelName
"at most 30% of certificates will self-delegate"
      ([DCert] -> Double
selfDelegationsRatio [DCert]
certs Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Double
0.30)

    -- for at least 60% of traces...
    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
60
      LabelName
"at least 25% delegates have multiple delegators"
      (Double
0.25 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= [DCert] -> Double
multipleDelegationsRatio [DCert]
certs)

    -- for at least 20% of traces...
    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
20
      LabelName
"some delegates have at least 5 corresponding delegators"
      (Int
5 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [DCert] -> Int
maxDelegationsTo [DCert]
certs)

    -- for at least 5% of traces...
    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
5
      LabelName
"at most 50% of delegators change their delegation"
      ([DCert] -> Double
changedDelegationsRatio [DCert]
certs Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Double
0.5)

    -- for at least 20% of traces...
    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
20
      LabelName
"some delegators have changed their delegation 5 or more times"
      (Int
5 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [DCert] -> Int
maxChangedDelegations [DCert]
certs)

    -- for at least 2% of traces...
    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
2
      LabelName
"at most 25% of delegations are repeats"
      ([DCert] -> Double
repeatedDelegationsRatio [DCert]
certs Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Double
0.25)

    -- for at least 30% of traces...
    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
30
      LabelName
"some delegations are repeated 10 or more times"
      (Int
10 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [DCert] -> Int
maxRepeatedDelegations [DCert]
certs)

    -- for at least 15% of traces...
    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
15
      LabelName
"some blocks have 5 or more certificates"
      (Int
5 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [[DCert]] -> Int
maxCertsPerBlock (Trace CHAIN -> [[DCert]]
traceDCertsByBlock Trace CHAIN
tr))

    -- for at least 50% of traces...
    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
50
      LabelName
"there is at least one change of epoch in the trace"
      (Int
2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Trace CHAIN -> Int
epochBoundariesInTrace Trace CHAIN
tr)

    -- for at least 30% of traces...
    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
30
      LabelName
"there are at least 5 epoch changes in the trace"
      (Int
5 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Trace CHAIN -> Int
epochBoundariesInTrace Trace CHAIN
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 CHAIN -> [(Epoch, Epoch)]
    epochDelegationEpoch :: Trace CHAIN -> [(Epoch, Epoch)]
epochDelegationEpoch Trace CHAIN
tr =
      forall s. TraceOrder -> Trace s -> [(State s, Signal s)]
preStatesAndSignals @CHAIN TraceOrder
OldestFirst Trace CHAIN
tr
        [((Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState),
  Block)]
-> ([((Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState),
      Block)]
    -> [(Epoch, [Epoch])])
-> [(Epoch, [Epoch])]
forall a b. a -> (a -> b) -> b
& (((Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState),
  Block)
 -> (Epoch, [Epoch]))
-> [((Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState),
     Block)]
-> [(Epoch, [Epoch])]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Slot -> Epoch
sEpoch_ (Slot -> Epoch)
-> ((Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
    -> Slot)
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Epoch
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting
  Slot
  (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
  Slot
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Slot
forall a s. Getting a s a -> s -> a
view Getting
  Slot
  (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
  Slot
forall s t a b. Field1 s t a b => Lens s t a b
Lens
  (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
  (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
  Slot
  Slot
_1 ((Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
 -> Epoch)
-> (Block -> [Epoch])
-> ((Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState),
    Block)
-> (Epoch, [Epoch])
forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** ((DCert -> Epoch) -> [DCert] -> [Epoch]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DCert -> Epoch
depoch ([DCert] -> [Epoch]) -> (Block -> [DCert]) -> Block -> [Epoch]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BlockBody -> [DCert]
_bDCerts (BlockBody -> [DCert]) -> (Block -> BlockBody) -> Block -> [DCert]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Block -> BlockBody
_bBody)))
        [(Epoch, [Epoch])]
-> ([(Epoch, [Epoch])] -> [[(Epoch, Epoch)]]) -> [[(Epoch, Epoch)]]
forall a b. a -> (a -> b) -> b
& ((Epoch, [Epoch]) -> [(Epoch, Epoch)])
-> [(Epoch, [Epoch])] -> [[(Epoch, Epoch)]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Epoch
e, [Epoch]
es) -> [Epoch] -> [Epoch] -> [(Epoch, Epoch)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Epoch -> [Epoch]
forall a. a -> [a]
repeat Epoch
e) [Epoch]
es)
        [[(Epoch, Epoch)]]
-> ([[(Epoch, Epoch)]] -> [(Epoch, Epoch)]) -> [(Epoch, Epoch)]
forall a b. a -> (a -> b) -> b
& [[(Epoch, Epoch)]] -> [(Epoch, Epoch)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      where
        blockCount :: BlockCount
blockCount = Trace CHAIN -> Environment CHAIN
forall s. Trace s -> Environment s
_traceEnv Trace CHAIN
tr (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount)
-> Getting
     BlockCount
     (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount)
     BlockCount
-> BlockCount
forall s a. s -> Getting a s a -> a
^. Getting
  BlockCount
  (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount)
  BlockCount
forall s t a b. Field5 s t a b => Lens s t a b
Lens
  (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount)
  (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount)
  BlockCount
  BlockCount
_5
        sEpoch_ :: Slot -> Epoch
sEpoch_ = (Slot -> BlockCount -> Epoch) -> BlockCount -> Slot -> Epoch
forall a b c. (a -> b -> c) -> b -> a -> c
flip HasCallStack => Slot -> BlockCount -> Epoch
Slot -> BlockCount -> Epoch
sEpoch BlockCount
blockCount

    -- Count the number of epoch boundaries in the trace
    epochBoundariesInTrace :: Trace CHAIN -> Int
    epochBoundariesInTrace :: Trace CHAIN -> Int
epochBoundariesInTrace Trace CHAIN
tr =
      [Word64] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Word64] -> Int) -> [Word64] -> Int
forall a b. (a -> b) -> a -> b
$
        (Word64 -> Bool) -> [Word64] -> [Word64]
forall a. (a -> Bool) -> [a] -> [a]
filter (Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
== Word64
0) (Slot -> Word64
isAtBoundary (Slot -> Word64) -> [Slot] -> [Word64]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Slot]
slots)
      where
        blocks :: [Signal CHAIN]
blocks = TraceOrder -> Trace CHAIN -> [Signal CHAIN]
forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
NewestFirst Trace CHAIN
tr
        slots :: [Slot]
slots = [Block]
[Signal CHAIN]
blocks [Block] -> Getting (Endo [Slot]) [Block] Slot -> [Slot]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. (Block -> Const (Endo [Slot]) Block)
-> [Block] -> Const (Endo [Slot]) [Block]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((Block -> Const (Endo [Slot]) Block)
 -> [Block] -> Const (Endo [Slot]) [Block])
-> ((Slot -> Const (Endo [Slot]) Slot)
    -> Block -> Const (Endo [Slot]) Block)
-> Getting (Endo [Slot]) [Block] Slot
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BlockHeader -> Const (Endo [Slot]) BlockHeader)
-> Block -> Const (Endo [Slot]) Block
Lens' Block BlockHeader
bHeader ((BlockHeader -> Const (Endo [Slot]) BlockHeader)
 -> Block -> Const (Endo [Slot]) Block)
-> ((Slot -> Const (Endo [Slot]) Slot)
    -> BlockHeader -> Const (Endo [Slot]) BlockHeader)
-> (Slot -> Const (Endo [Slot]) Slot)
-> Block
-> Const (Endo [Slot]) Block
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Slot -> Const (Endo [Slot]) Slot)
-> BlockHeader -> Const (Endo [Slot]) BlockHeader
Lens' BlockHeader Slot
bhSlot
        k :: BlockCount
k = Trace CHAIN -> Environment CHAIN
forall s. Trace s -> Environment s
_traceEnv Trace CHAIN
tr (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount)
-> Getting
     BlockCount
     (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount)
     BlockCount
-> BlockCount
forall s a. s -> Getting a s a -> a
^. Getting
  BlockCount
  (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount)
  BlockCount
forall s t a b. Field5 s t a b => Lens s t a b
Lens
  (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount)
  (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount)
  BlockCount
  BlockCount
_5
        isAtBoundary :: Slot -> Word64
isAtBoundary = (Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
`rem` BlockCount -> Word64
forall n. Integral n => BlockCount -> n
slotsPerEpoch BlockCount
k) (Word64 -> Word64) -> (Slot -> Word64) -> Slot -> Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Slot -> Word64
unSlot

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

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