{-# 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
property forall a b. (a -> b) -> a -> b
$ do
  let (Word64
maxTraceLength, Word64
step) = (Word64
100, Word64
10)
  Trace CHAIN
tr <-
    forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$
      forall s.
HasTrace s =>
BaseEnv s -> TraceLength -> SignalGenerator s -> Gen (Trace s)
traceSigGen
        ()
        (Word64 -> TraceLength
Maximum Word64
maxTraceLength)
        (ShouldGenDelegation
-> ShouldGenUTxO
-> ShouldGenUpdate
-> Environment CHAIN
-> State CHAIN
-> Gen (Signal CHAIN)
sigGenChain ShouldGenDelegation
NoGenDelegation ShouldGenUTxO
NoGenUTxO ShouldGenUpdate
NoGenUpdate)
  forall s. Trace s -> Word64 -> Word64 -> PropertyT IO ()
classifyTraceLength Trace CHAIN
tr Word64
maxTraceLength Word64
step
  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 forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== forall a. (a -> a -> Ordering) -> [a] -> [a]
nubSortBy (forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing forall a. a -> Down a
Down) [Slot]
slots
  where
    blocks :: [Signal CHAIN]
blocks = forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
NewestFirst Trace CHAIN
tr
    slots :: [Slot]
slots = [Signal CHAIN]
blocks forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' Block BlockHeader
bHeader forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' BlockHeader Slot
bhSlot

blockIssuersAreDelegates :: Property
blockIssuersAreDelegates :: Property
blockIssuersAreDelegates =
  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
      let (Word64
maxTraceLength, Word64
step) = (Word64
100, Word64
10)
      Trace CHAIN
tr <-
        forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$
          forall s.
HasTrace s =>
BaseEnv s -> TraceLength -> SignalGenerator s -> Gen (Trace s)
traceSigGen
            ()
            (Word64 -> TraceLength
Maximum Word64
maxTraceLength)
            (ShouldGenDelegation
-> ShouldGenUTxO
-> ShouldGenUpdate
-> Environment CHAIN
-> State CHAIN
-> Gen (Signal CHAIN)
sigGenChain ShouldGenDelegation
GenDelegation ShouldGenUTxO
NoGenUTxO ShouldGenUpdate
GenUpdate)
      forall s. Trace s -> Word64 -> Word64 -> PropertyT IO ()
classifyTraceLength Trace CHAIN
tr Word64
maxTraceLength Word64
step
      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 =
      forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ forall (m :: * -> *).
MonadTest m =>
(State CHAIN, Signal CHAIN) -> m ()
checkIssuer forall a b. (a -> b) -> a -> b
$ 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
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
            Maybe VKeyGenesis
Nothing -> forall (m :: * -> *) a. (MonadTest m, HasCallStack) => m a
failure
          where
            issuer :: VKey
issuer = Signal CHAIN
bk forall s a. s -> Getting a s a -> a
^. Lens' Block BlockHeader
bHeader forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' BlockHeader VKey
bhIssuer
            dm :: Bimap VKeyGenesis VKey
dm = State CHAIN
st forall s a. s -> Getting a s a -> a
^. Lens' (State CHAIN) DIState
disL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s a. HasDelegationMap s a => Lens' s a
delegationMap

onlyValidSignalsAreGenerated :: Property
onlyValidSignalsAreGenerated :: Property
onlyValidSignalsAreGenerated =
  TestLimit -> Property -> Property
withTests TestLimit
200 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 forall a b. (a -> b) -> a -> b
$
  HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
    let maxTraceLength :: Word64
maxTraceLength = Word64
100
    Trace CHAIN
tr <-
      forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$
        forall s.
HasTrace s =>
BaseEnv s -> TraceLength -> SignalGenerator s -> Gen (Trace s)
traceSigGen
          ()
          (Word64 -> TraceLength
Maximum Word64
maxTraceLength)
          (ShouldGenDelegation
-> ShouldGenUTxO
-> ShouldGenUpdate
-> Environment CHAIN
-> State CHAIN
-> Gen (Signal CHAIN)
sigGenChain ShouldGenDelegation
GenDelegation ShouldGenUTxO
NoGenUTxO ShouldGenUpdate
GenUpdate)
    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 =
      forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (forall (m :: * -> *).
MonadTest m =>
BlockCount -> State CHAIN -> m ()
signersListIsBoundedByKInState BlockCount
k) forall a b. (a -> b) -> a -> b
$ 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) =
          forall (m :: * -> *). (MonadTest m, HasCallStack) => Bool -> m ()
assert forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq VKeyGenesis
sgs forall a. Ord a => a -> a -> Bool
<= forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
k'

relevantCasesAreCovered :: Property
relevantCasesAreCovered :: Property
relevantCasesAreCovered = 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
    Trace CHAIN
tr <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall s.
HasTrace s =>
BaseEnv s -> TraceLength -> SignalGenerator s -> Gen (Trace s)
traceSigGen () (Word64 -> TraceLength
Desired Word64
200) (ShouldGenDelegation
-> ShouldGenUTxO
-> ShouldGenUpdate
-> Environment CHAIN
-> State CHAIN
-> Gen (Signal 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...
    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
1
      LabelName
"there are more certificates than blocks"
      (forall s. Trace s -> Int
traceLength Trace CHAIN
tr forall a. Ord a => a -> a -> Bool
<= forall (t :: * -> *) a. Foldable t => t a -> Int
length [DCert]
certs)

    -- for at least 10% of traces...
    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) forall a. Ord a => a -> a -> Bool
<= Double
0.75)

    -- for at least 25% of traces...
    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 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...
    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 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...
    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 forall a. Ord a => a -> a -> Bool
<= Double
0.30)

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

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

    -- for at least 5% of traces...
    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 forall a. Ord a => a -> a -> Bool
<= Double
0.5)

    -- for at least 20% of traces...
    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 forall a. Ord a => a -> a -> Bool
<= [DCert] -> Int
maxChangedDelegations [DCert]
certs)

    -- for at least 2% of traces...
    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 forall a. Ord a => a -> a -> Bool
<= Double
0.25)

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

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

    -- for at least 50% of traces...
    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 forall a. Ord a => a -> a -> Bool
<= Trace CHAIN -> Int
epochBoundariesInTrace Trace CHAIN
tr)

    -- for at least 30% of traces...
    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 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
        forall a b. a -> (a -> b) -> b
& forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Slot -> Epoch
sEpoch_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a s. Getting a s a -> s -> a
view forall s t a b. Field1 s t a b => Lens s t a b
_1 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
. (BlockBody -> [DCert]
_bDCerts forall b c a. (b -> c) -> (a -> b) -> a -> c
. Block -> BlockBody
_bBody)))
        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
      where
        blockCount :: BlockCount
blockCount = forall s. Trace s -> Environment s
_traceEnv Trace CHAIN
tr forall s a. s -> Getting a s a -> a
^. forall s t a b. Field5 s t a b => Lens s t a b
_5
        sEpoch_ :: Slot -> Epoch
sEpoch_ = forall a b c. (a -> b -> c) -> b -> a -> c
flip HasCallStack => 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 =
      forall (t :: * -> *) a. Foldable t => t a -> Int
length forall a b. (a -> b) -> a -> b
$
        forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
== Word64
0) (Slot -> Word64
isAtBoundary forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Slot]
slots)
      where
        blocks :: [Signal CHAIN]
blocks = forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
NewestFirst Trace CHAIN
tr
        slots :: [Slot]
slots = [Signal CHAIN]
blocks forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' Block BlockHeader
bHeader forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' BlockHeader Slot
bhSlot
        k :: BlockCount
k = forall s. Trace s -> Environment s
_traceEnv Trace CHAIN
tr forall s a. s -> Getting a s a -> a
^. forall s t a b. Field5 s t a b => Lens s t a b
_5
        isAtBoundary :: Slot -> Word64
isAtBoundary = (forall a. Integral a => a -> a -> a
`rem` forall n. Integral n => BlockCount -> n
slotsPerEpoch BlockCount
k) 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Block -> BlockBody
_bBody forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. Trace CHAIN -> [[DCert]]
traceDCertsByBlock