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

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

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) <- 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')
              , []
              , forall k a. Map k a
Map.empty
              , forall k a. Map k a
Map.empty
              , forall k a. Map k a
Map.empty
              , forall k a. Map k a
Map.empty
              , forall a. Set a
Set.empty
              , forall a. Set a
Set.empty
              , 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 forall a b. (a -> b) -> a -> b
$ 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
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 forall a b. (a -> b) -> a -> b
$ forall sts. Environment sts -> IRC sts
IRC DSEnv
dsEnv
        forall (f :: * -> *) a. Applicative f => a -> f a
pure 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) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        case Block -> Bool
bIsEBB Signal CHAIN
b of
          Bool
True -> TransitionRule CHAIN
isEBBRule
          Bool
False -> 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) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        Block -> Natural
bSize Signal CHAIN
b forall a. Ord a => a -> a -> Bool
<= (Natural
2 forall a. Bits a => a -> Int -> a
`shift` Int
21) forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Natural -> Natural -> ChainPredicateFailure
MaximumBlockSize (Block -> Natural
bSize Signal CHAIN
b) (Natural
2 forall a. Bits a => a -> Int -> a
`shift` Int
21)
        let h' :: Hash
h' = BlockHeader -> Hash
bhHash (Signal CHAIN
b forall s a. s -> Getting a s a -> a
^. Lens' Block BlockHeader
bHeader)
        forall (f :: * -> *) a. Applicative f => a -> f a
pure 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) <- 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 forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC ((HasCallStack => Slot -> BlockCount -> Epoch
sEpoch Slot
sLast BlockCount
k, BlockCount
k), UPIState
us, Block -> Slot
bSlot Signal CHAIN
b)
        UPIState -> BlockHeader -> Rule CHAIN 'Transition ()
headerIsValid UPIState
us' (Signal CHAIN
b forall s a. s -> Getting a s a -> a
^. Lens' Block BlockHeader
bHeader)
        let ppsUs' :: PParams
ppsUs' = forall a b. (a, b) -> b
snd (UPIState
us' forall s a. s -> Getting a s a -> a
^. forall s t a b. Field1 s t a b => Lens s t a b
_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 forall a b. (a -> b) -> a -> b
$
            forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC
              (
                ( PParams
ppsUs'
                , HasCallStack => Slot -> BlockCount -> Epoch
sEpoch (Block -> Slot
bSlot Signal CHAIN
b) BlockCount
k
                , UTxO
utxoGenesis
                , forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Set a -> Int
Set.size Set VKeyGenesis
ads)
                , BlockCount
k
                )
              , (UTxOState
utxoSt, DIState
ds, UPIState
us')
              , 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 forall a b. (a -> b) -> a -> b
$ 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
b forall s a. s -> Getting a s a -> a
^. Lens' Block BlockHeader
bHeader)
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! (Block -> Slot
bSlot Signal CHAIN
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 -> ChainPredicateFailure
EpochFailure

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

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

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

instance Embed UTXOWS CHAIN where
  wrapFailed :: PredicateFailure UTXOWS -> PredicateFailure CHAIN
wrapFailed = 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 = forall a b. (a, b) -> b
snd (UPIState
us forall s a. s -> Getting a s a -> a
^. forall s t a b. Field1 s t a b => Lens s t a b
_1) forall s a. s -> Getting a s a -> a
^. Lens' PParams Natural
maxHdrSz
  BlockHeader -> Natural
bHeaderSize BlockHeader
bh
    forall a. Ord a => a -> a -> Bool
<= Natural
sMax
      forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! BlockHeader
-> Natural -> Threshold Natural -> ChainPredicateFailure
HeaderSizeTooBig BlockHeader
bh (BlockHeader -> Natural
bHeaderSize BlockHeader
bh) (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 = forall s t a b. Field5 s t a b => Lens s t a b
_5

instance HasTrace CHAIN where
  envGen :: Word64 -> Gen (Environment CHAIN)
envGen Word64
chainLength = do
    Word8
ngk <- forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (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 forall a. Integral a => a -> a -> a
`div` Word64
10)
    Double
sigCntT <- BlockCount -> Word8 -> Gen Double
SigCntGen.sigCntT BlockCount
k Word8
ngk
    (,,,,)
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenT Identity Slot
gCurrentSlot
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (UTxO -> UTxO
adjustUTxO forall b c a. (b -> c) -> (a -> b) -> a -> c
. UTxOEnv -> UTxO
utxo0 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s. HasTrace s => Word64 -> Gen (Environment s)
envGen @UTXOWS Word64
chainLength)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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.
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure PParams
initialPParams {_bkSgnCntT :: BkSgnCntT
_bkSgnCntT = Double -> BkSgnCntT
Update.BkSgnCntT Double
sigCntT}
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (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 forall a b. (a -> b) -> a -> b
$ \(Lovelace Integer
v) ->
        Integer -> Lovelace
Lovelace forall a b. (a -> b) -> a -> b
$ Integer
v forall a. Num a => a -> a -> a
* 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Word64
s forall a. Num a => a -> a -> a
+) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (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 forall a b. (a -> b) -> a -> b
$
              forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC
                ( (HasCallStack => Slot -> BlockCount -> Epoch
sEpoch (Word64 -> Slot
Slot Word64
s) BlockCount
k, BlockCount
k)
                , UPIState
us
                , Slot
nextSlot
                )

          pps' :: PParams
pps' = UPIState -> PParams
protocolParameters 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
            , forall {a} {a}. (Show a, Integral a, Num a) => a -> a
toNumberOfGenesisKeys forall a b. (a -> b) -> a -> b
$ 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
            | forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
maxBound :: Word8) forall a. Ord a => a -> a -> Bool
< a
n =
                forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"sigGenChain: too many genesis keys: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
n
            | Bool
otherwise = 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 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 forall s a. s -> Getting a s a -> a
^. forall a.
HasDelegationMap a (Bimap VKeyGenesis VKey) =>
Lens' a (Bimap VKeyGenesis VKey)
dmsL, BlockCount
k) Seq VKeyGenesis
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.
            forall (m :: * -> *) a. MonadGen m => [(Int, m a)] -> m a
Gen.frequency
              [ (Int
7, 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
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 -> 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
utxoEnv UTxOState
utxo
          ShouldGenUTxO
NoGenUTxO -> 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 State EPOCH
us'
          ShouldGenUpdate
NoGenUpdate ->
            forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Maybe a
Nothing, [])

      forall (f :: * -> *) a. Applicative f => a -> f a
pure 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
    [ BbodyPredicateFailure
InvalidDelegationHash
    , BbodyPredicateFailure
InvalidUpdateProposalHash
    , 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)) 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)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> e -> f e'
k e
e
  {-# INLINE _5 #-}