{-# 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 (_sNow, utxo0', ads, pps', 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 = 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 =
              ( (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
              )
        utxoSt0 <- trans @UTXOWS $ IRC UTxOEnv {utxo0 = utxo0', pps = pps'}
        let 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
                }
        ds <- trans @DELEG $ IRC dsEnv
        pure $!
          ( s0
          , []
          , genesisHash
          , utxoSt0
          , ds
          , upiState0
          )
    ]

  transitionRules :: [TransitionRule CHAIN]
transitionRules =
    [ do
        TRC (_, _, 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 bIsEBB 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 ((_sNow, _, _, _, _), (sLast, sgs, _, utxo, ds, us), b) <- Rule CHAIN 'Transition (RuleContext 'Transition CHAIN)
F (Clause CHAIN 'Transition) (TRC CHAIN)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        bSize b <= (2 `shift` 21) ?! MaximumBlockSize (bSize b) (2 `shift` 21)
        let 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)
        pure $! (sLast, sgs, h', utxo, ds, us)

      notEBBRule :: TransitionRule CHAIN
      notEBBRule :: TransitionRule CHAIN
notEBBRule = do
        TRC ((sNow, utxoGenesis, ads, _pps, k), (sLast, sgs, h, utxoSt, ds, us), 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 = DIState -> Bimap VKeyGenesis VKey
_dIStateDelegationMap DIState
ds :: Bimap VKeyGenesis VKey
        us' <-
          trans @EPOCH $ TRC ((sEpoch sLast k, k), us, bSlot b)
        headerIsValid us' (b ^. bHeader)
        let 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)
        (utxoSt', ds', us'') <-
          trans @BBODY $
            TRC
              (
                ( ppsUs'
                , sEpoch (bSlot b) k
                , utxoGenesis
                , fromIntegral (Set.size ads)
                , k
                )
              , (utxoSt, ds, us')
              , b
              )
        (h', sgs') <-
          trans @PBFT $ TRC ((ppsUs', dm, sLast, sNow, k), (h, sgs), b ^. bHeader)
        pure $! (bSlot b, sgs', h', utxoSt', ds', 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
    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)
    k <- CoreGen.k chainLength (chainLength `div` 10)
    sigCntT <- SigCntGen.sigCntT k ngk
    (,,,,)
      <$> gCurrentSlot
      <*> (adjustUTxO . utxo0 <$> envGen @UTXOWS chainLength)
      <*> pure (mkVkGenesisSet ngk)
      -- TODO: for now we're returning a constant set of parameters, where only '_bkSgnCntT' varies.
      <*> pure initialPParams {_bkSgnCntT = Update.BkSgnCntT sigCntT}
      <*> pure 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.
      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 (us', _) =
            applySTSIndifferently @EPOCH $
              TRC
                ( (sEpoch (Slot s) k, k)
                , us
                , nextSlot
                )

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

          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
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

      aBlockVersion <-
        Update.protocolVersionEndorsementGen upienv 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.
      vkI <- SigCntGen.issuer (pps', ds ^. dmsL, k) sgs

      delegationPayload <-
        case 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.
(HasCallStack, 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 []

      utxoPayload <-
        case 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 []

      (anOptionalUpdateProposal, aListOfVotes) <-
        case 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, [])

      pure $!
        mkBlock
          h
          nextSlot
          vkI
          aBlockVersion
          delegationPayload
          anOptionalUpdateProposal
          aListOfVotes
          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 #-}