{-# 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)
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 = Bimap VKeyGenesis VKey
forall a b. Bimap a b
Bimap.empty
    , _dStateLastDelegation :: Map VKeyGenesis Slot
_dStateLastDelegation = Map VKeyGenesis Slot
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 = Set (Epoch, VKeyGenesis)
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 DSState
-> Getting
     [(Slot, (VKeyGenesis, VKey))] DSState [(Slot, (VKeyGenesis, VKey))]
-> [(Slot, (VKeyGenesis, VKey))]
forall s a. s -> Getting a s a -> a
^. Getting
  [(Slot, (VKeyGenesis, VKey))] DSState [(Slot, (VKeyGenesis, VKey))]
forall s a. HasScheduledDelegations s a => Lens' s a
Lens' DSState [(Slot, (VKeyGenesis, VKey))]
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
Typeable DBLOCK =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> DBLOCK -> c DBLOCK)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c DBLOCK)
-> (DBLOCK -> Constr)
-> (DBLOCK -> DataType)
-> (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))
-> ((forall b. Data b => b -> b) -> DBLOCK -> DBLOCK)
-> (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 u. (forall d. Data d => d -> u) -> DBLOCK -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> DBLOCK -> u)
-> (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 (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DBLOCK -> m DBLOCK)
-> Data DBLOCK
DBLOCK -> Constr
DBLOCK -> DataType
(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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DBLOCK -> c DBLOCK
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DBLOCK -> c DBLOCK
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DBLOCK
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DBLOCK
$ctoConstr :: DBLOCK -> Constr
toConstr :: DBLOCK -> Constr
$cdataTypeOf :: DBLOCK -> DataType
dataTypeOf :: DBLOCK -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DBLOCK)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DBLOCK)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DBLOCK)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DBLOCK)
$cgmapT :: (forall b. Data b => b -> b) -> DBLOCK -> DBLOCK
gmapT :: (forall b. Data b => b -> b) -> DBLOCK -> DBLOCK
$cgmapQl :: 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
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DBLOCK -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DBLOCK -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> DBLOCK -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> DBLOCK -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DBLOCK -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DBLOCK -> u
$cgmapM :: forall (m :: * -> *).
Monad 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
$cgmapMp :: 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
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DBLOCK -> m DBLOCK
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DBLOCK -> m DBLOCK
Data)

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

makeLenses ''DBlock

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

-- | 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 <- Rule DBLOCK 'Initial (RuleContext 'Initial DBLOCK)
F (Clause DBLOCK 'Initial) (IRC DBLOCK)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        (DIEnv, DIState) -> F (Clause DBLOCK 'Initial) (DIEnv, DIState)
forall a. a -> F (Clause DBLOCK 'Initial) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DIEnv
Environment DBLOCK
env, DIState
initialDIState)
    ]

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

    trExpectedDms :: Bimap VKeyGenesis VKey
trExpectedDms =
      Int -> Int -> [(Int, DBlock)] -> Bimap VKeyGenesis VKey
expectedDms
        Int
lastSlot
        ((Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word64 -> Int) -> (BlockCount -> Word64) -> BlockCount -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SlotCount -> Word64
unSlotCount (SlotCount -> Word64)
-> (BlockCount -> SlotCount) -> BlockCount -> Word64
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) = Trace DBLOCK -> State DBLOCK
forall s. Trace s -> State s
lastState Trace DBLOCK
tr

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

    slotsAndDcerts :: [(Int, DBlock)]
    slotsAndDcerts :: [(Int, DBlock)]
slotsAndDcerts =
      ((DIEnv, DIState) -> Int)
-> ((DIEnv, DIState), DBlock) -> (Int, DBlock)
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (Getting Int (DIEnv, DIState) Int -> (DIEnv, DIState) -> Int
forall a s. Getting a s a -> s -> a
view (((DIEnv, DIState) -> DIEnv) -> SimpleGetter (DIEnv, DIState) DIEnv
forall s a. (s -> a) -> SimpleGetter s a
to (DIEnv, DIState) -> DIEnv
forall a b. (a, b) -> a
fst Getting Int (DIEnv, DIState) DIEnv
-> ((Int -> Const Int Int) -> DIEnv -> Const Int DIEnv)
-> Getting Int (DIEnv, DIState) Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Slot -> Const Int Slot) -> DIEnv -> Const Int DIEnv
forall s a. HasSlot s a => Lens' s a
Lens' DIEnv Slot
slot ((Slot -> Const Int Slot) -> DIEnv -> Const Int DIEnv)
-> ((Int -> Const Int Int) -> Slot -> Const Int Slot)
-> (Int -> Const Int Int)
-> DIEnv
-> Const Int DIEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Slot -> Word64) -> SimpleGetter Slot Word64
forall s a. (s -> a) -> SimpleGetter s a
to Slot -> Word64
unSlot Getting Int Slot Word64
-> ((Int -> Const Int Int) -> Word64 -> Const Int Word64)
-> (Int -> Const Int Int)
-> Slot
-> Const Int Slot
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Word64 -> Int) -> SimpleGetter Word64 Int
forall s a. (s -> a) -> SimpleGetter s a
to Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral))
        (((DIEnv, DIState), DBlock) -> (Int, DBlock))
-> [((DIEnv, DIState), DBlock)] -> [(Int, DBlock)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TraceOrder -> Trace DBLOCK -> [(State DBLOCK, Signal DBLOCK)]
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 =
  (Bimap VKeyGenesis VKey
 -> (VKeyGenesis, VKey) -> Bimap VKeyGenesis VKey)
-> Bimap VKeyGenesis VKey
-> [(VKeyGenesis, VKey)]
-> Bimap VKeyGenesis VKey
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
F.foldl' Bimap VKeyGenesis VKey
-> (VKeyGenesis, VKey) -> Bimap VKeyGenesis VKey
insertIfInjective Bimap VKeyGenesis VKey
forall a b. Bimap a b
Bimap.empty ((DCert -> (VKeyGenesis, VKey)) -> [DCert] -> [(VKeyGenesis, VKey)]
forall a b. (a -> b) -> [a] -> [b]
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 VKey -> Bimap VKeyGenesis VKey -> Bool
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 VKeyGenesis
-> VKey -> Bimap VKeyGenesis VKey -> Bimap VKeyGenesis VKey
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 = (DBlock -> [DCert]) -> [DBlock] -> [DCert]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DBlock -> [DCert]
_blockCerts [DBlock]
activeBlocks

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

    activationSlot :: Int
    activationSlot :: Int
activationSlot = Int
s Int -> Int -> Int
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
        (Set VKeyGenesis -> Epoch -> Slot -> BlockCount -> DIEnv)
-> GenT Identity (Set VKeyGenesis)
-> GenT Identity (Epoch -> Slot -> BlockCount -> DIEnv)
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.
        GenT Identity (Epoch -> Slot -> BlockCount -> DIEnv)
-> GenT Identity Epoch
-> GenT Identity (Slot -> BlockCount -> DIEnv)
forall a b.
GenT Identity (a -> b) -> GenT Identity a -> GenT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Word64 -> Word64 -> GenT Identity Epoch
epochGen Word64
0 Word64
10
        -- As with epochs, the current slot should not have influence in the tests.
        GenT Identity (Slot -> BlockCount -> DIEnv)
-> GenT Identity Slot -> GenT Identity (BlockCount -> DIEnv)
forall a b.
GenT Identity (a -> b) -> GenT Identity a -> GenT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Word64 -> Word64 -> GenT Identity 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@).
        --
        GenT Identity (BlockCount -> DIEnv)
-> GenT Identity BlockCount -> GenT Identity DIEnv
forall a b.
GenT Identity (a -> b) -> GenT Identity a -> GenT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Word64 -> Word64 -> GenT Identity BlockCount
CoreGen.k Word64
chainLength (Word64
chainLength Word64 -> Word64 -> Word64
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 <- Range Natural -> GenT Identity Natural
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Natural -> Natural -> Range Natural
forall a. Integral a => a -> a -> Range a
Range.linear Natural
0 Natural
13)
          Set VKeyGenesis -> GenT Identity (Set VKeyGenesis)
forall a. a -> GenT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set VKeyGenesis -> GenT Identity (Set VKeyGenesis))
-> Set VKeyGenesis -> GenT Identity (Set VKeyGenesis)
forall a b. (a -> b) -> a -> b
$! [VKeyGenesis] -> Set VKeyGenesis
forall a. Eq a => [a] -> Set a
Set.fromAscList ([VKeyGenesis] -> Set VKeyGenesis)
-> [VKeyGenesis] -> Set VKeyGenesis
forall a b. (a -> b) -> a -> b
$ Natural -> VKeyGenesis
mkVKeyGenesis (Natural -> VKeyGenesis) -> [Natural] -> [VKeyGenesis]
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 (Slot -> [DCert] -> DBlock)
-> GenT Identity Slot -> GenT Identity ([DCert] -> DBlock)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DIEnv -> GenT Identity Slot
nextSlotGen DIEnv
env GenT Identity ([DCert] -> DBlock)
-> GenT Identity [DCert] -> GenT Identity DBlock
forall a b.
GenT Identity (a -> b) -> GenT Identity a -> GenT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall s. HasTrace s => SignalGenerator s
sigGen @DELEG DIEnv
Environment DELEG
env DIState
State DELEG
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 -> GenT Identity Slot
nextSlotGen DIEnv
env =
  Word64 -> Slot
incSlot
    (Word64 -> Slot) -> GenT Identity Word64 -> GenT Identity Slot
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Int, GenT Identity Word64)] -> GenT Identity Word64
forall (m :: * -> *) a. MonadGen m => [(Int, m a)] -> m a
Gen.frequency
      [ (Int
1, Range Word64 -> GenT Identity Word64
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Word64 -> Word64 -> Range Word64
forall a. a -> a -> Range a
Range.constant Word64
1 Word64
10))
      , (Int
2, Word64 -> GenT Identity Word64
forall a. a -> GenT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Word64 -> GenT Identity Word64) -> Word64 -> GenT Identity Word64
forall a b. (a -> b) -> a -> b
$! BlockCount -> Word64
forall n. Integral n => BlockCount -> n
slotsPerEpoch (DIEnv -> BlockCount
_dSEnvK DIEnv
env))
      ]
  where
    incSlot :: Word64 -> Slot
incSlot Word64
c = (DIEnv
env DIEnv -> Getting Slot DIEnv Slot -> Slot
forall s a. s -> Getting a s a -> a
^. Getting Slot DIEnv Slot
forall s a. HasSlot s a => Lens' s a
Lens' DIEnv Slot
slot) Slot -> SlotCount -> Slot
`addSlot` Word64 -> SlotCount
SlotCount Word64
c

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

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

dblockTracesAreClassified :: Property
dblockTracesAreClassified :: Property
dblockTracesAreClassified = 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
    let (Word64
tl, Word64
step) = (Word64
100, Word64
10)
    Trace DBLOCK
tr <- Gen (Trace DBLOCK) -> PropertyT IO (Trace DBLOCK)
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)
    Trace DBLOCK -> Word64 -> Word64 -> PropertyT IO ()
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.
    [Char]
-> [DCert]
-> ([DCert] -> Word64)
-> Word64
-> Word64
-> PropertyT IO ()
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) (Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Word64) -> ([DCert] -> Int) -> [DCert] -> Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DCert] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length) Word64
tl Word64
step
    PropertyT IO ()
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 (DBlock -> [DCert]) -> [DBlock] -> [[DCert]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TraceOrder -> Trace DBLOCK -> [Signal DBLOCK]
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 = [[DCert]] -> [DCert]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[DCert]] -> [DCert])
-> (Trace DBLOCK -> [[DCert]]) -> Trace DBLOCK -> [DCert]
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 (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 tl :: Word64
tl = Word64
100
    Trace DBLOCK
tr <- Gen (Trace DBLOCK) -> PropertyT IO (Trace DBLOCK)
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.
    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
40
      LabelName
"there are at least as many delegation certificates as blocks"
      (Trace DBLOCK -> Int
forall s. Trace s -> Int
traceLength Trace DBLOCK
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 (Trace DBLOCK -> [DCert]
traceDCerts Trace DBLOCK
tr))

    -- 50% of the traces must contain at most 25% of blocks with empty delegation payload.
    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
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 Double -> Double -> Bool
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.
    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
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 Double -> Double -> Bool
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.
    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
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 Double -> Double -> Bool
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.
    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
30
      LabelName
"at least 30% of the certificates self delegate"
      (Double
0.3 Double -> Double -> Bool
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.
    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
50
      LabelName
"at least 25% of delegates have multiple delegators"
      (Double
0.05 Double -> Double -> Bool
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
        [((DIEnv, DIState), DBlock)]
-> ([((DIEnv, DIState), DBlock)] -> [(Epoch, [Epoch])])
-> [(Epoch, [Epoch])]
forall a b. a -> (a -> b) -> b
& (((DIEnv, DIState), DBlock) -> (Epoch, [Epoch]))
-> [((DIEnv, DIState), DBlock)] -> [(Epoch, [Epoch])]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (DIEnv -> Epoch
_dSEnvEpoch (DIEnv -> Epoch)
-> ((DIEnv, DIState) -> DIEnv) -> (DIEnv, DIState) -> Epoch
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DIEnv, DIState) -> DIEnv
forall a b. (a, b) -> a
fst ((DIEnv, DIState) -> Epoch)
-> (DBlock -> [Epoch])
-> ((DIEnv, DIState), DBlock)
-> (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]) -> (DBlock -> [DCert]) -> DBlock -> [Epoch]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DBlock -> [DCert]
_blockCerts))
        [(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

onlyValidSignalsAreGenerated :: Property
onlyValidSignalsAreGenerated :: Property
onlyValidSignalsAreGenerated =
  TestLimit -> Property -> Property
withTests TestLimit
300 (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 @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 (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 DELEG
tr, DCert
dcert) <- Gen (Trace DELEG, DCert) -> PropertyT IO (Trace DELEG, DCert)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen (Trace DELEG, DCert) -> PropertyT IO (Trace DELEG, DCert))
-> Gen (Trace DELEG, DCert) -> PropertyT IO (Trace DELEG, DCert)
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
          Gen (Trace DELEG) -> (State DELEG -> Bool) -> Gen (Trace DELEG)
forall s. Gen (Trace s) -> (State s -> Bool) -> Gen (Trace s)
`suchThatLastState` (Bool -> Bool
not (Bool -> Bool) -> (DIState -> Bool) -> DIState -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Slot, (VKeyGenesis, VKey))] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([(Slot, (VKeyGenesis, VKey))] -> Bool)
-> (DIState -> [(Slot, (VKeyGenesis, VKey))]) -> DIState -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting
  [(Slot, (VKeyGenesis, VKey))] DIState [(Slot, (VKeyGenesis, VKey))]
-> DIState -> [(Slot, (VKeyGenesis, VKey))]
forall a s. Getting a s a -> s -> a
view Getting
  [(Slot, (VKeyGenesis, VKey))] DIState [(Slot, (VKeyGenesis, VKey))]
forall s a. HasScheduledDelegations s a => Lens' s a
Lens' DIState [(Slot, (VKeyGenesis, VKey))]
scheduledDelegations)
      let vkS :: VKeyGenesis
vkS =
            case Trace DELEG -> State DELEG
forall s. Trace s -> State s
lastState Trace DELEG
tr DIState
-> Getting
     [(Slot, (VKeyGenesis, VKey))] DIState [(Slot, (VKeyGenesis, VKey))]
-> [(Slot, (VKeyGenesis, VKey))]
forall s a. s -> Getting a s a -> a
^. Getting
  [(Slot, (VKeyGenesis, VKey))] DIState [(Slot, (VKeyGenesis, VKey))]
forall s a. HasScheduledDelegations s a => Lens' s a
Lens' DIState [(Slot, (VKeyGenesis, VKey))]
scheduledDelegations of
              (Slot
_, (VKeyGenesis
res, VKey
_)) : [(Slot, (VKeyGenesis, VKey))]
_ -> VKeyGenesis
res
              [(Slot, (VKeyGenesis, VKey))]
_ ->
                [Char] -> VKeyGenesis
forall a. HasCallStack => [Char] -> a
error ([Char] -> VKeyGenesis) -> [Char] -> VKeyGenesis
forall a b. (a -> b) -> a -> b
$
                  [Char]
"This should not happen: "
                    [Char] -> ShowS
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 (Word64 -> Epoch) -> GenT Identity Word64 -> GenT Identity Epoch
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range Word64 -> GenT Identity Word64
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Word64 -> Word64 -> Range Word64
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 ((VKey, Epoch) -> Owner -> Sig (VKey, Epoch)
forall a. a -> Owner -> Sig a
Sig (VKey
vkD, Epoch
epo) (VKeyGenesis -> Owner
forall a. HasOwner a => a -> Owner
owner VKeyGenesis
vkS)) VKey
vkD Epoch
epo
      (Trace DELEG, DCert) -> Gen (Trace DELEG, DCert)
forall a. a -> GenT Identity a
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 ((Environment DELEG, State DELEG, Signal DELEG) -> TRC DELEG
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Trace DELEG
tr Trace DELEG -> Getting DIEnv (Trace DELEG) DIEnv -> DIEnv
forall s a. s -> Getting a s a -> a
^. Getting DIEnv (Trace DELEG) DIEnv
(Environment DELEG -> Const DIEnv (Environment DELEG))
-> Trace DELEG -> Const DIEnv (Trace DELEG)
forall s (f :: * -> *).
Functor f =>
(Environment s -> f (Environment s)) -> Trace s -> f (Trace s)
traceEnv, Trace DELEG -> State DELEG
forall s. Trace s -> State s
lastState Trace DELEG
tr, [DCert
dcert])) of
          Left NonEmpty (PredicateFailure DELEG)
res -> NonEmpty DelegPredicateFailure -> [DelegPredicateFailure]
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty (PredicateFailure DELEG)
NonEmpty DelegPredicateFailure
res
          Right State DELEG
_ -> []
    Bool -> PropertyT IO ()
forall (m :: * -> *). (MonadTest m, HasCallStack) => Bool -> m ()
assert (Bool -> PropertyT IO ()) -> Bool -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ PredicateFailure SDELEGS -> DelegPredicateFailure
SDelegSFailure (PredicateFailure SDELEG -> SdelegsPredicateFailure
SDelegFailure PredicateFailure SDELEG
SdelegPredicateFailure
IsAlreadyScheduled) DelegPredicateFailure -> [DelegPredicateFailure] -> Bool
forall a. Eq a => a -> [a] -> Bool
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