{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedLists #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
-- For the Field5 instance
{-# OPTIONS_GHC -Wno-orphans #-}

module Byron.Spec.Chain.STS.Rule.Chain where

import Byron.Spec.Chain.STS.Block
import Byron.Spec.Chain.STS.Rule.BBody
import Byron.Spec.Chain.STS.Rule.Epoch (EPOCH, sEpoch)
import Byron.Spec.Chain.STS.Rule.Pbft
import qualified Byron.Spec.Chain.STS.Rule.SigCnt as SigCntGen
import Byron.Spec.Ledger.Core
import qualified Byron.Spec.Ledger.Core.Generators as CoreGen
import Byron.Spec.Ledger.Delegation
import qualified Byron.Spec.Ledger.GlobalParams as GP
import Byron.Spec.Ledger.STS.UTXO (UTxOEnv (UTxOEnv, pps, utxo0), UTxOState)
import Byron.Spec.Ledger.STS.UTXOWS (UTXOWS)
import Byron.Spec.Ledger.UTxO (UTxO, mapUTxOValues)
import Byron.Spec.Ledger.Update hiding (delegationMap)
import qualified Byron.Spec.Ledger.Update as Update
import Control.State.Transition
import Data.Bimap (Bimap)
import Data.Bits (shift)
import Data.Data (Data)
import qualified Data.Map as Map
import Data.Sequence (Seq)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Word (Word8)
import GHC.Stack (HasCallStack)
import Hedgehog (Gen, MonadTest)
import qualified Hedgehog.Gen as Gen
import Hedgehog.Internal.Property (CoverPercentage)
import qualified Hedgehog.Range as Range
import Lens.Micro (Lens', (^.))
import Lens.Micro.Internal (Field1 (..), Field5 (..))
import Numeric.Natural (Natural)
import Test.Control.State.Transition.Generator

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

data ChainPredicateFailure
  = EpochFailure (PredicateFailure EPOCH)
  | HeaderSizeTooBig BlockHeader Natural (Threshold Natural)
  | BBodyFailure (PredicateFailure BBODY)
  | PBFTFailure (PredicateFailure PBFT)
  | MaximumBlockSize Natural Natural
  | LedgerDelegationFailure (PredicateFailure DELEG)
  | LedgerUTxOFailure (PredicateFailure UTXOWS)
  deriving (ChainPredicateFailure -> ChainPredicateFailure -> Bool
(ChainPredicateFailure -> ChainPredicateFailure -> Bool)
-> (ChainPredicateFailure -> ChainPredicateFailure -> Bool)
-> Eq ChainPredicateFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ChainPredicateFailure -> ChainPredicateFailure -> Bool
== :: ChainPredicateFailure -> ChainPredicateFailure -> Bool
$c/= :: ChainPredicateFailure -> ChainPredicateFailure -> Bool
/= :: ChainPredicateFailure -> ChainPredicateFailure -> Bool
Eq, Int -> ChainPredicateFailure -> ShowS
[ChainPredicateFailure] -> ShowS
ChainPredicateFailure -> String
(Int -> ChainPredicateFailure -> ShowS)
-> (ChainPredicateFailure -> String)
-> ([ChainPredicateFailure] -> ShowS)
-> Show ChainPredicateFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ChainPredicateFailure -> ShowS
showsPrec :: Int -> ChainPredicateFailure -> ShowS
$cshow :: ChainPredicateFailure -> String
show :: ChainPredicateFailure -> String
$cshowList :: [ChainPredicateFailure] -> ShowS
showList :: [ChainPredicateFailure] -> ShowS
Show, Typeable ChainPredicateFailure
Typeable ChainPredicateFailure =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g)
 -> ChainPredicateFailure
 -> c ChainPredicateFailure)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ChainPredicateFailure)
-> (ChainPredicateFailure -> Constr)
-> (ChainPredicateFailure -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ChainPredicateFailure))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c ChainPredicateFailure))
-> ((forall b. Data b => b -> b)
    -> ChainPredicateFailure -> ChainPredicateFailure)
-> (forall r r'.
    (r -> r' -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> ChainPredicateFailure
    -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> ChainPredicateFailure
    -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> ChainPredicateFailure -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> ChainPredicateFailure -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> ChainPredicateFailure -> m ChainPredicateFailure)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> ChainPredicateFailure -> m ChainPredicateFailure)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> ChainPredicateFailure -> m ChainPredicateFailure)
-> Data ChainPredicateFailure
ChainPredicateFailure -> Constr
ChainPredicateFailure -> DataType
(forall b. Data b => b -> b)
-> ChainPredicateFailure -> ChainPredicateFailure
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) -> ChainPredicateFailure -> u
forall u.
(forall d. Data d => d -> u) -> ChainPredicateFailure -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ChainPredicateFailure -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ChainPredicateFailure -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> ChainPredicateFailure -> m ChainPredicateFailure
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ChainPredicateFailure -> m ChainPredicateFailure
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ChainPredicateFailure
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> ChainPredicateFailure
-> c ChainPredicateFailure
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ChainPredicateFailure)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ChainPredicateFailure)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> ChainPredicateFailure
-> c ChainPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> ChainPredicateFailure
-> c ChainPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ChainPredicateFailure
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ChainPredicateFailure
$ctoConstr :: ChainPredicateFailure -> Constr
toConstr :: ChainPredicateFailure -> Constr
$cdataTypeOf :: ChainPredicateFailure -> DataType
dataTypeOf :: ChainPredicateFailure -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ChainPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ChainPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ChainPredicateFailure)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ChainPredicateFailure)
$cgmapT :: (forall b. Data b => b -> b)
-> ChainPredicateFailure -> ChainPredicateFailure
gmapT :: (forall b. Data b => b -> b)
-> ChainPredicateFailure -> ChainPredicateFailure
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ChainPredicateFailure -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ChainPredicateFailure -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ChainPredicateFailure -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ChainPredicateFailure -> r
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> ChainPredicateFailure -> [u]
gmapQ :: forall u.
(forall d. Data d => d -> u) -> ChainPredicateFailure -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> ChainPredicateFailure -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> ChainPredicateFailure -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> ChainPredicateFailure -> m ChainPredicateFailure
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> ChainPredicateFailure -> m ChainPredicateFailure
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ChainPredicateFailure -> m ChainPredicateFailure
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ChainPredicateFailure -> m ChainPredicateFailure
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ChainPredicateFailure -> m ChainPredicateFailure
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ChainPredicateFailure -> m ChainPredicateFailure
Data)

instance STS CHAIN where
  type
    Environment CHAIN =
      ( Slot -- Current slot
      , UTxO
      , -- Components needed to be able to bootstrap the traces generator. They are
        -- not part of the formal spec. These might be removed once we have decided
        -- on how do we want to model initial states.
        Set VKeyGenesis -- Allowed delegators. Needed by the initial delegation rules. The number of
        -- genesis keys is the size of this set.
      , PParams -- Needed to bootstrap this part of the chain state,
      -- which is used in the delegation rules
      , BlockCount -- Chain stability parameter
      )

  type
    State CHAIN =
      ( Slot
      , Seq VKeyGenesis
      , Hash
      , UTxOState
      , DIState
      , UPIState
      )

  type Signal CHAIN = Block

  type PredicateFailure CHAIN = ChainPredicateFailure

  initialRules :: [InitialRule CHAIN]
initialRules =
    [ do
        IRC (Slot
_sNow, UTxO
utxo0', Set VKeyGenesis
ads, PParams
pps', BlockCount
k) <- Rule CHAIN 'Initial (RuleContext 'Initial CHAIN)
F (Clause CHAIN 'Initial) (IRC CHAIN)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        let s0 :: Slot
s0 = Word64 -> Slot
Slot Word64
0
            -- Since we only test the delegation state we initialize the
            -- remaining fields of the update interface state to (m)empty. Once
            -- the formal spec includes initial rules for update we can use
            -- them here.
            upiState0 :: UPIState
upiState0 =
              ( (Natural -> Natural -> Natural -> ProtVer
ProtVer Natural
0 Natural
0 Natural
0, PParams
pps')
              , []
              , Map ApName (ApVer, Slot, Metadata)
forall k a. Map k a
Map.empty
              , Map UpId (ProtVer, PParams)
forall k a. Map k a
Map.empty
              , Map UpId (ApName, ApVer, Metadata)
forall k a. Map k a
Map.empty
              , Map UpId Slot
forall k a. Map k a
Map.empty
              , Set (UpId, VKeyGenesis)
forall a. Set a
Set.empty
              , Set (ProtVer, VKeyGenesis)
forall a. Set a
Set.empty
              , Map UpId Slot
forall k a. Map k a
Map.empty
              )
        UTxOState
utxoSt0 <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @UTXOWS (RuleContext 'Initial UTXOWS -> Rule CHAIN 'Initial (State UTXOWS))
-> RuleContext 'Initial UTXOWS
-> Rule CHAIN 'Initial (State UTXOWS)
forall a b. (a -> b) -> a -> b
$ Environment UTXOWS -> IRC UTXOWS
forall sts. Environment sts -> IRC sts
IRC UTxOEnv {utxo0 :: UTxO
utxo0 = UTxO
utxo0', pps :: PParams
pps = PParams
pps'}
        let dsEnv :: DSEnv
dsEnv =
              DSEnv
                { _dSEnvAllowedDelegators :: Set VKeyGenesis
_dSEnvAllowedDelegators = Set VKeyGenesis
ads
                , _dSEnvEpoch :: Epoch
_dSEnvEpoch = HasCallStack => Slot -> BlockCount -> Epoch
Slot -> BlockCount -> Epoch
sEpoch Slot
s0 BlockCount
k
                , _dSEnvSlot :: Slot
_dSEnvSlot = Slot
s0
                , _dSEnvK :: BlockCount
_dSEnvK = BlockCount
k
                }
        DIState
ds <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @DELEG (RuleContext 'Initial DELEG -> Rule CHAIN 'Initial (State DELEG))
-> RuleContext 'Initial DELEG -> Rule CHAIN 'Initial (State DELEG)
forall a b. (a -> b) -> a -> b
$ Environment DELEG -> IRC DELEG
forall sts. Environment sts -> IRC sts
IRC DSEnv
Environment DELEG
dsEnv
        (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Rule
     CHAIN
     'Initial
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall a. a -> F (Clause CHAIN 'Initial) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
 -> Rule
      CHAIN
      'Initial
      (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState))
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Rule
     CHAIN
     'Initial
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall a b. (a -> b) -> a -> b
$!
          ( Slot
s0
          , []
          , Hash
genesisHash
          , UTxOState
utxoSt0
          , DIState
ds
          , UPIState
upiState0
          )
    ]

  transitionRules :: [TransitionRule CHAIN]
transitionRules =
    [ do
        TRC (Environment CHAIN
_, State CHAIN
_, Signal CHAIN
b) <- Rule CHAIN 'Transition (RuleContext 'Transition CHAIN)
F (Clause CHAIN 'Transition) (TRC CHAIN)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        case Block -> Bool
bIsEBB Signal CHAIN
Block
b of
          Bool
True -> Rule
  CHAIN
  'Transition
  (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
TransitionRule CHAIN
isEBBRule
          Bool
False -> Rule
  CHAIN
  'Transition
  (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
TransitionRule CHAIN
notEBBRule
    ]
    where
      isEBBRule :: TransitionRule CHAIN
      isEBBRule :: TransitionRule CHAIN
isEBBRule = do
        TRC ((Slot
_sNow, UTxO
_, Set VKeyGenesis
_, PParams
_, BlockCount
_), (Slot
sLast, Seq VKeyGenesis
sgs, Hash
_, UTxOState
utxo, DIState
ds, UPIState
us), Signal CHAIN
b) <- Rule CHAIN 'Transition (RuleContext 'Transition CHAIN)
F (Clause CHAIN 'Transition) (TRC CHAIN)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        Block -> Natural
bSize Signal CHAIN
Block
b Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= (Natural
2 Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
`shift` Int
21) Bool -> PredicateFailure CHAIN -> Rule CHAIN 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Natural -> Natural -> ChainPredicateFailure
MaximumBlockSize (Block -> Natural
bSize Signal CHAIN
Block
b) (Natural
2 Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
`shift` Int
21)
        let h' :: Hash
h' = BlockHeader -> Hash
bhHash (Signal CHAIN
Block
b Block -> Getting BlockHeader Block BlockHeader -> BlockHeader
forall s a. s -> Getting a s a -> a
^. Getting BlockHeader Block BlockHeader
Lens' Block BlockHeader
bHeader)
        (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Rule
     CHAIN
     'Transition
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall a. a -> F (Clause CHAIN 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
 -> Rule
      CHAIN
      'Transition
      (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState))
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Rule
     CHAIN
     'Transition
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall a b. (a -> b) -> a -> b
$! (Slot
sLast, Seq VKeyGenesis
sgs, Hash
h', UTxOState
utxo, DIState
ds, UPIState
us)

      notEBBRule :: TransitionRule CHAIN
      notEBBRule :: TransitionRule CHAIN
notEBBRule = do
        TRC ((Slot
sNow, UTxO
utxoGenesis, Set VKeyGenesis
ads, PParams
_pps, BlockCount
k), (Slot
sLast, Seq VKeyGenesis
sgs, Hash
h, UTxOState
utxoSt, DIState
ds, UPIState
us), Signal CHAIN
b) <- Rule CHAIN 'Transition (RuleContext 'Transition CHAIN)
F (Clause CHAIN 'Transition) (TRC CHAIN)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        let dm :: Bimap VKeyGenesis VKey
dm = DIState -> Bimap VKeyGenesis VKey
_dIStateDelegationMap DIState
ds :: Bimap VKeyGenesis VKey
        UPIState
us' <-
          forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @EPOCH (RuleContext 'Transition EPOCH
 -> Rule CHAIN 'Transition (State EPOCH))
-> RuleContext 'Transition EPOCH
-> Rule CHAIN 'Transition (State EPOCH)
forall a b. (a -> b) -> a -> b
$ (Environment EPOCH, State EPOCH, Signal EPOCH) -> TRC EPOCH
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC ((HasCallStack => Slot -> BlockCount -> Epoch
Slot -> BlockCount -> Epoch
sEpoch Slot
sLast BlockCount
k, BlockCount
k), UPIState
State EPOCH
us, Block -> Slot
bSlot Signal CHAIN
Block
b)
        UPIState -> BlockHeader -> Rule CHAIN 'Transition ()
headerIsValid UPIState
us' (Signal CHAIN
Block
b Block -> Getting BlockHeader Block BlockHeader -> BlockHeader
forall s a. s -> Getting a s a -> a
^. Getting BlockHeader Block BlockHeader
Lens' Block BlockHeader
bHeader)
        let ppsUs' :: PParams
ppsUs' = (ProtVer, PParams) -> PParams
forall a b. (a, b) -> b
snd (UPIState
us' UPIState
-> Getting (ProtVer, PParams) UPIState (ProtVer, PParams)
-> (ProtVer, PParams)
forall s a. s -> Getting a s a -> a
^. Getting (ProtVer, PParams) UPIState (ProtVer, PParams)
forall s t a b. Field1 s t a b => Lens s t a b
Lens UPIState UPIState (ProtVer, PParams) (ProtVer, PParams)
_1)
        (UTxOState
utxoSt', DIState
ds', UPIState
us'') <-
          forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @BBODY (RuleContext 'Transition BBODY
 -> Rule CHAIN 'Transition (State BBODY))
-> RuleContext 'Transition BBODY
-> Rule CHAIN 'Transition (State BBODY)
forall a b. (a -> b) -> a -> b
$
            (Environment BBODY, State BBODY, Signal BBODY) -> TRC BBODY
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC
              (
                ( PParams
ppsUs'
                , HasCallStack => Slot -> BlockCount -> Epoch
Slot -> BlockCount -> Epoch
sEpoch (Block -> Slot
bSlot Signal CHAIN
Block
b) BlockCount
k
                , UTxO
utxoGenesis
                , Int -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Set VKeyGenesis -> Int
forall a. Set a -> Int
Set.size Set VKeyGenesis
ads)
                , BlockCount
k
                )
              , (UTxOState
utxoSt, DIState
ds, UPIState
us')
              , Signal BBODY
Signal CHAIN
b
              )
        (Hash
h', Seq VKeyGenesis
sgs') <-
          forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @PBFT (RuleContext 'Transition PBFT
 -> Rule CHAIN 'Transition (State PBFT))
-> RuleContext 'Transition PBFT
-> Rule CHAIN 'Transition (State PBFT)
forall a b. (a -> b) -> a -> b
$ (Environment PBFT, State PBFT, Signal PBFT) -> TRC PBFT
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC ((PParams
ppsUs', Bimap VKeyGenesis VKey
dm, Slot
sLast, Slot
sNow, BlockCount
k), (Hash
h, Seq VKeyGenesis
sgs), Signal CHAIN
Block
b Block -> Getting BlockHeader Block BlockHeader -> BlockHeader
forall s a. s -> Getting a s a -> a
^. Getting BlockHeader Block BlockHeader
Lens' Block BlockHeader
bHeader)
        (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Rule
     CHAIN
     'Transition
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall a. a -> F (Clause CHAIN 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
 -> Rule
      CHAIN
      'Transition
      (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState))
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> Rule
     CHAIN
     'Transition
     (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
forall a b. (a -> b) -> a -> b
$! (Block -> Slot
bSlot Signal CHAIN
Block
b, Seq VKeyGenesis
sgs', Hash
h', UTxOState
utxoSt', DIState
ds', UPIState
us'')

instance Embed EPOCH CHAIN where
  wrapFailed :: PredicateFailure EPOCH -> PredicateFailure CHAIN
wrapFailed = PredicateFailure EPOCH -> PredicateFailure CHAIN
PredicateFailure EPOCH -> ChainPredicateFailure
EpochFailure

instance Embed BBODY CHAIN where
  wrapFailed :: PredicateFailure BBODY -> PredicateFailure CHAIN
wrapFailed = PredicateFailure BBODY -> PredicateFailure CHAIN
PredicateFailure BBODY -> ChainPredicateFailure
BBodyFailure

instance Embed PBFT CHAIN where
  wrapFailed :: PredicateFailure PBFT -> PredicateFailure CHAIN
wrapFailed = PredicateFailure PBFT -> PredicateFailure CHAIN
PredicateFailure PBFT -> ChainPredicateFailure
PBFTFailure

instance Embed DELEG CHAIN where
  wrapFailed :: PredicateFailure DELEG -> PredicateFailure CHAIN
wrapFailed = PredicateFailure DELEG -> PredicateFailure CHAIN
PredicateFailure DELEG -> ChainPredicateFailure
LedgerDelegationFailure

instance Embed UTXOWS CHAIN where
  wrapFailed :: PredicateFailure UTXOWS -> PredicateFailure CHAIN
wrapFailed = PredicateFailure UTXOWS -> PredicateFailure CHAIN
PredicateFailure UTXOWS -> ChainPredicateFailure
LedgerUTxOFailure

isHeaderSizeTooBigFailure :: PredicateFailure CHAIN -> Bool
isHeaderSizeTooBigFailure :: PredicateFailure CHAIN -> Bool
isHeaderSizeTooBigFailure (HeaderSizeTooBig BlockHeader
_ Natural
_ Threshold Natural
_) = Bool
True
isHeaderSizeTooBigFailure PredicateFailure CHAIN
_ = Bool
False

headerIsValid :: UPIState -> BlockHeader -> Rule CHAIN 'Transition ()
headerIsValid :: UPIState -> BlockHeader -> Rule CHAIN 'Transition ()
headerIsValid UPIState
us BlockHeader
bh = do
  let sMax :: Natural
sMax = (ProtVer, PParams) -> PParams
forall a b. (a, b) -> b
snd (UPIState
us UPIState
-> Getting (ProtVer, PParams) UPIState (ProtVer, PParams)
-> (ProtVer, PParams)
forall s a. s -> Getting a s a -> a
^. Getting (ProtVer, PParams) UPIState (ProtVer, PParams)
forall s t a b. Field1 s t a b => Lens s t a b
Lens UPIState UPIState (ProtVer, PParams) (ProtVer, PParams)
_1) PParams -> Getting Natural PParams Natural -> Natural
forall s a. s -> Getting a s a -> a
^. Getting Natural PParams Natural
Lens' PParams Natural
maxHdrSz
  BlockHeader -> Natural
bHeaderSize BlockHeader
bh
    Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= Natural
sMax
      Bool -> PredicateFailure CHAIN -> Rule CHAIN 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! BlockHeader
-> Natural -> Threshold Natural -> ChainPredicateFailure
HeaderSizeTooBig BlockHeader
bh (BlockHeader -> Natural
bHeaderSize BlockHeader
bh) (Natural -> Threshold Natural
forall a. a -> Threshold a
Threshold Natural
sMax)

-- | Lens for the delegation interface state contained in the chain state.
disL :: Lens' (State CHAIN) DIState
disL :: Lens' (State CHAIN) DIState
disL = (DIState -> f DIState)
-> (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
-> f (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
(DIState -> f DIState) -> State CHAIN -> f (State CHAIN)
forall s t a b. Field5 s t a b => Lens s t a b
Lens
  (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
  (Slot, Seq VKeyGenesis, Hash, UTxOState, DIState, UPIState)
  DIState
  DIState
_5

instance HasTrace CHAIN where
  envGen :: Word64 -> Gen (Environment CHAIN)
envGen Word64
chainLength = do
    Word8
ngk <- Range Word8 -> GenT Identity Word8
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Word8 -> Word8 -> Range Word8
forall a. Integral a => a -> a -> Range a
Range.linear Word8
1 Word8
14)
    BlockCount
k <- Word64 -> Word64 -> Gen BlockCount
CoreGen.k Word64
chainLength (Word64
chainLength Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
`div` Word64
10)
    Double
sigCntT <- BlockCount -> Word8 -> Gen Double
SigCntGen.sigCntT BlockCount
k Word8
ngk
    (,,,,)
      (Slot
 -> UTxO
 -> Set VKeyGenesis
 -> PParams
 -> BlockCount
 -> (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount))
-> GenT Identity Slot
-> GenT
     Identity
     (UTxO
      -> Set VKeyGenesis
      -> PParams
      -> BlockCount
      -> (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenT Identity Slot
gCurrentSlot
      GenT
  Identity
  (UTxO
   -> Set VKeyGenesis
   -> PParams
   -> BlockCount
   -> (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount))
-> GenT Identity UTxO
-> GenT
     Identity
     (Set VKeyGenesis
      -> PParams
      -> BlockCount
      -> (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount))
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
<*> (UTxO -> UTxO
adjustUTxO (UTxO -> UTxO) -> (UTxOEnv -> UTxO) -> UTxOEnv -> UTxO
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UTxOEnv -> UTxO
utxo0 (UTxOEnv -> UTxO) -> GenT Identity UTxOEnv -> GenT Identity UTxO
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s. HasTrace s => Word64 -> Gen (Environment s)
envGen @UTXOWS Word64
chainLength)
      GenT
  Identity
  (Set VKeyGenesis
   -> PParams
   -> BlockCount
   -> (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount))
-> GenT Identity (Set VKeyGenesis)
-> GenT
     Identity
     (PParams
      -> BlockCount
      -> (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount))
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
<*> Set VKeyGenesis -> GenT Identity (Set VKeyGenesis)
forall a. a -> GenT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Word8 -> Set VKeyGenesis
mkVkGenesisSet Word8
ngk)
      -- TODO: for now we're returning a constant set of parameters, where only '_bkSgnCntT' varies.
      GenT
  Identity
  (PParams
   -> BlockCount
   -> (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount))
-> GenT Identity PParams
-> GenT
     Identity
     (BlockCount -> (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount))
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
<*> PParams -> GenT Identity PParams
forall a. a -> GenT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure PParams
initialPParams {_bkSgnCntT = Update.BkSgnCntT sigCntT}
      GenT
  Identity
  (BlockCount -> (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount))
-> Gen BlockCount
-> GenT Identity (Slot, UTxO, Set VKeyGenesis, PParams, BlockCount)
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
<*> BlockCount -> Gen BlockCount
forall a. a -> GenT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure BlockCount
k
    where
      -- If we want to generate large traces, we need to set up the value of the
      -- current slot to a sufficiently large value.
      gCurrentSlot :: GenT Identity Slot
gCurrentSlot = Word64 -> Slot
Slot (Word64 -> Slot) -> GenT Identity Word64 -> GenT Identity Slot
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. a -> a -> Range a
Range.constant Word64
32768 Word64
2147483648)

      -- The UTXOW generators assume the @b@ fee parameter to be @0 <= b <= 10@,
      -- and pick UTxO values that are correspondingly small. In order to allow
      -- for a difference in real transaction size between the spec and impl,
      -- however, the `initialParams` pick a value of @10 * GP.c@ for @b@
      -- instead. This @c@ correction factor allows real transactions to be
      -- @c@ times larger than the spec ones and still guarantee that the real
      -- transaction will have sufficient fees when the abstract tx does.
      -- If we don't apply this same correction factor to the generated UTxO,
      -- however, we will be unable to generate any /abstract/ transactions,
      -- because the UTxO values will not be large enough to cover tx fees.
      adjustUTxO :: UTxO -> UTxO
      adjustUTxO :: UTxO -> UTxO
adjustUTxO = (Lovelace -> Lovelace) -> UTxO -> UTxO
mapUTxOValues ((Lovelace -> Lovelace) -> UTxO -> UTxO)
-> (Lovelace -> Lovelace) -> UTxO -> UTxO
forall a b. (a -> b) -> a -> b
$ \(Lovelace Integer
v) ->
        Integer -> Lovelace
Lovelace (Integer -> Lovelace) -> Integer -> Lovelace
forall a b. (a -> b) -> a -> b
$ Integer
v Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
GP.c

  sigGen :: SignalGenerator CHAIN
sigGen = ShouldGenDelegation
-> ShouldGenUTxO -> ShouldGenUpdate -> SignalGenerator CHAIN
sigGenChain ShouldGenDelegation
GenDelegation ShouldGenUTxO
GenUTxO ShouldGenUpdate
GenUpdate

data ShouldGenDelegation = GenDelegation | NoGenDelegation

data ShouldGenUTxO = GenUTxO | NoGenUTxO

data ShouldGenUpdate = GenUpdate | NoGenUpdate

sigGenChain ::
  ShouldGenDelegation ->
  ShouldGenUTxO ->
  ShouldGenUpdate ->
  Environment CHAIN ->
  State CHAIN ->
  Gen (Signal CHAIN)
sigGenChain :: ShouldGenDelegation
-> ShouldGenUTxO -> ShouldGenUpdate -> SignalGenerator CHAIN
sigGenChain
  ShouldGenDelegation
shouldGenDelegation
  ShouldGenUTxO
shouldGenUTxO
  ShouldGenUpdate
shouldGenUpdate
  (Slot
_sNow, UTxO
utxo0, Set VKeyGenesis
ads, PParams
_pps, BlockCount
k)
  (Slot Word64
s, Seq VKeyGenesis
sgs, Hash
h, UTxOState
utxo, DIState
ds, UPIState
us) =
    do
      -- We'd expect the slot increment to be close to 1, even for large Gen's
      -- size numbers.
      Slot
nextSlot <- Word64 -> Slot
Slot (Word64 -> Slot) -> (Word64 -> Word64) -> Word64 -> Slot
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Word64
s Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+) (Word64 -> Slot) -> GenT Identity Word64 -> GenT Identity Slot
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.exponential Word64
1 Word64
10)

      -- We need to generate delegation, update proposals, votes, and transactions
      -- after a potential update in the protocol parameters (which is triggered
      -- only at epoch boundaries). Otherwise the generators will use a state that
      -- won't hold when the rules that correspond to these generators are
      -- applied. For instance, the fees might change, which will render the
      -- transaction as invalid.
      --
      let (State EPOCH
us', [PredicateFailure EPOCH]
_) =
            forall s (rtype :: RuleType).
(STS s, RuleTypeRep rtype, Identity ~ BaseM s) =>
RuleContext rtype s -> (State s, [PredicateFailure s])
applySTSIndifferently @EPOCH (RuleContext 'Transition EPOCH
 -> (State EPOCH, [PredicateFailure EPOCH]))
-> RuleContext 'Transition EPOCH
-> (State EPOCH, [PredicateFailure EPOCH])
forall a b. (a -> b) -> a -> b
$
              (Environment EPOCH, State EPOCH, Signal EPOCH) -> TRC EPOCH
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC
                ( (HasCallStack => Slot -> BlockCount -> Epoch
Slot -> BlockCount -> Epoch
sEpoch (Word64 -> Slot
Slot Word64
s) BlockCount
k, BlockCount
k)
                , UPIState
State EPOCH
us
                , Slot
Signal EPOCH
nextSlot
                )

          pps' :: PParams
pps' = UPIState -> PParams
protocolParameters UPIState
State EPOCH
us'

          upienv :: (Slot, Bimap VKeyGenesis VKey, BlockCount, Word8)
upienv =
            ( Word64 -> Slot
Slot Word64
s
            , DIState -> Bimap VKeyGenesis VKey
_dIStateDelegationMap DIState
ds
            , BlockCount
k
            , Int -> Word8
forall {a} {a}. (Show a, Integral a, Num a) => a -> a
toNumberOfGenesisKeys (Int -> Word8) -> Int -> Word8
forall a b. (a -> b) -> a -> b
$ Set VKeyGenesis -> Int
forall a. Set a -> Int
Set.size Set VKeyGenesis
ads
            )

          -- TODO: we might need to make the number of genesis keys a newtype, and
          -- provide this function in the same module where this newtype is
          -- defined.
          toNumberOfGenesisKeys :: a -> a
toNumberOfGenesisKeys a
n
            | Word8 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word8
forall a. Bounded a => a
maxBound :: Word8) a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
n =
                String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"sigGenChain: too many genesis keys: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n
            | Bool
otherwise = a -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
n

      ProtVer
aBlockVersion <-
        (Slot, Bimap VKeyGenesis VKey, BlockCount, Word8)
-> UPIState -> Gen ProtVer
Update.protocolVersionEndorsementGen (Slot, Bimap VKeyGenesis VKey, BlockCount, Word8)
upienv UPIState
State EPOCH
us'

      -- Here we do not want to shrink the issuer, since @Gen.element@ shrinks
      -- towards the first element of the list, which in this case won't provide
      -- us with better shrinks.
      VKey
vkI <- Environment SIGCNT -> State SIGCNT -> Gen VKey
SigCntGen.issuer (PParams
pps', DIState
ds 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 a.
HasDelegationMap a (Bimap VKeyGenesis VKey) =>
Lens' a (Bimap VKeyGenesis VKey)
Lens' DIState (Bimap VKeyGenesis VKey)
dmsL, BlockCount
k) Seq VKeyGenesis
State SIGCNT
sgs

      [DCert]
delegationPayload <-
        case ShouldGenDelegation
shouldGenDelegation of
          ShouldGenDelegation
GenDelegation ->
            -- In practice there won't be a delegation payload in every block, so we
            -- make this payload sparse.
            --
            -- NOTE: We arbitrarily chose to generate delegation payload in 30% of
            -- the cases. We could make this configurable.
            [(Int, GenT Identity [DCert])] -> GenT Identity [DCert]
forall (m :: * -> *) a. MonadGen m => [(Int, m a)] -> m a
Gen.frequency
              [ (Int
7, [DCert] -> GenT Identity [DCert]
forall a. a -> GenT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [])
              ,
                ( Int
3
                , let dsEnv :: DSEnv
dsEnv =
                        DSEnv
                          { _dSEnvAllowedDelegators :: Set VKeyGenesis
_dSEnvAllowedDelegators = Set VKeyGenesis
ads
                          , _dSEnvEpoch :: Epoch
_dSEnvEpoch = HasCallStack => Slot -> BlockCount -> Epoch
Slot -> BlockCount -> Epoch
sEpoch Slot
nextSlot BlockCount
k
                          , _dSEnvSlot :: Slot
_dSEnvSlot = Slot
nextSlot
                          , _dSEnvK :: BlockCount
_dSEnvK = BlockCount
k
                          }
                   in DSEnv -> DIState -> GenT Identity [DCert]
dcertsGen DSEnv
dsEnv DIState
ds
                )
              ]
          ShouldGenDelegation
NoGenDelegation -> [DCert] -> GenT Identity [DCert]
forall a. a -> GenT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

      [Tx]
utxoPayload <-
        case ShouldGenUTxO
shouldGenUTxO of
          ShouldGenUTxO
GenUTxO ->
            let utxoEnv :: UTxOEnv
utxoEnv = UTxO -> PParams -> UTxOEnv
UTxOEnv UTxO
utxo0 PParams
pps'
             in forall s. HasTrace s => SignalGenerator s
sigGen @UTXOWS UTxOEnv
Environment UTXOWS
utxoEnv UTxOState
State UTXOWS
utxo
          ShouldGenUTxO
NoGenUTxO -> [Tx] -> GenT Identity [Tx]
forall a. a -> GenT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

      (Maybe UProp
anOptionalUpdateProposal, [Vote]
aListOfVotes) <-
        case ShouldGenUpdate
shouldGenUpdate of
          ShouldGenUpdate
GenUpdate ->
            (Slot, Bimap VKeyGenesis VKey, BlockCount, Word8)
-> UPIState -> GenT Identity (Maybe UProp, [Vote])
Update.updateProposalAndVotesGen (Slot, Bimap VKeyGenesis VKey, BlockCount, Word8)
upienv UPIState
State EPOCH
us'
          ShouldGenUpdate
NoGenUpdate ->
            (Maybe UProp, [Vote]) -> GenT Identity (Maybe UProp, [Vote])
forall a. a -> GenT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe UProp
forall a. Maybe a
Nothing, [])

      Block -> GenT Identity Block
forall a. a -> GenT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Block -> GenT Identity Block) -> Block -> GenT Identity Block
forall a b. (a -> b) -> a -> b
$!
        Hash
-> Slot
-> VKey
-> ProtVer
-> [DCert]
-> Maybe UProp
-> [Vote]
-> [Tx]
-> Block
mkBlock
          Hash
h
          Slot
nextSlot
          VKey
vkI
          ProtVer
aBlockVersion
          [DCert]
delegationPayload
          Maybe UProp
anOptionalUpdateProposal
          [Vote]
aListOfVotes
          [Tx]
utxoPayload

coverInvalidBlockProofs ::
  forall m a.
  ( MonadTest m
  , HasCallStack
  , Data a
  ) =>
  -- | Minimum percentage that each failure must occur.
  CoverPercentage ->
  -- | Structure containing the failures
  a ->
  m ()
coverInvalidBlockProofs :: forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Data a) =>
CoverPercentage -> a -> m ()
coverInvalidBlockProofs CoverPercentage
coverPercentage =
  forall (m :: * -> *) s a.
(MonadTest m, HasCallStack, Data (PredicateFailure s), Data a) =>
CoverPercentage -> [PredicateFailure s] -> a -> m ()
coverFailures @_ @BBODY
    CoverPercentage
coverPercentage
    [ Item [BbodyPredicateFailure]
BbodyPredicateFailure
InvalidDelegationHash
    , Item [BbodyPredicateFailure]
BbodyPredicateFailure
InvalidUpdateProposalHash
    , Item [BbodyPredicateFailure]
BbodyPredicateFailure
InvalidUtxoHash
    ]

--------------------------------------------------------------------------------
-- FieldX instances for a 6-tuple
--------------------------------------------------------------------------------

instance Field1 (a, b, c, d, e, f) (a', b, c, d, e, f) a a' where
  _1 :: Lens (a, b, c, d, e, f) (a', b, c, d, e, f) a a'
_1 a -> f a'
k ~(a
a, b
b, c
c, d
d, e
e, f
f) = (\a'
a' -> (a'
a', b
b, c
c, d
d, e
e, f
f)) (a' -> (a', b, c, d, e, f)) -> f a' -> f (a', b, c, d, e, f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a'
k a
a
  {-# INLINE _1 #-}

instance Field5 (a, b, c, d, e, f) (a, b, c, d, e', f) e e' where
  _5 :: Lens (a, b, c, d, e, f) (a, b, c, d, e', f) e e'
_5 e -> f e'
k ~(a
a, b
b, c
c, d
d, e
e, f
f) = (\e'
e' -> (a
a, b
b, c
c, d
d, e'
e', f
f)) (e' -> (a, b, c, d, e', f)) -> f e' -> f (a, b, c, d, e', f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> e -> f e'
k e
e
  {-# INLINE _5 #-}