{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Byron.Spec.Chain.STS.Rule.SigCnt where
import Byron.Spec.Ledger.Core hiding ((|>))
import Byron.Spec.Ledger.Update hiding (NotADelegate)
import Control.Arrow ((|||))
import Control.State.Transition
import Data.Bimap (Bimap)
import qualified Data.Bimap as Bimap
import Data.Data (Data)
import Data.Sequence (Seq, (|>))
import qualified Data.Sequence as S
import Data.Word (Word8)
import Hedgehog (Gen)
import qualified Hedgehog.Gen as Gen
import qualified Hedgehog.Range as Range
import Lens.Micro ((^.))
data SIGCNT deriving (Typeable SIGCNT
Typeable SIGCNT =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SIGCNT -> c SIGCNT)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SIGCNT)
-> (SIGCNT -> Constr)
-> (SIGCNT -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SIGCNT))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SIGCNT))
-> ((forall b. Data b => b -> b) -> SIGCNT -> SIGCNT)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SIGCNT -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SIGCNT -> r)
-> (forall u. (forall d. Data d => d -> u) -> SIGCNT -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> SIGCNT -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SIGCNT -> m SIGCNT)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SIGCNT -> m SIGCNT)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SIGCNT -> m SIGCNT)
-> Data SIGCNT
SIGCNT -> Constr
SIGCNT -> DataType
(forall b. Data b => b -> b) -> SIGCNT -> SIGCNT
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) -> SIGCNT -> u
forall u. (forall d. Data d => d -> u) -> SIGCNT -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SIGCNT -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SIGCNT -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SIGCNT -> m SIGCNT
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SIGCNT -> m SIGCNT
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SIGCNT
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SIGCNT -> c SIGCNT
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SIGCNT)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SIGCNT)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SIGCNT -> c SIGCNT
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SIGCNT -> c SIGCNT
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SIGCNT
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SIGCNT
$ctoConstr :: SIGCNT -> Constr
toConstr :: SIGCNT -> Constr
$cdataTypeOf :: SIGCNT -> DataType
dataTypeOf :: SIGCNT -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SIGCNT)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SIGCNT)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SIGCNT)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SIGCNT)
$cgmapT :: (forall b. Data b => b -> b) -> SIGCNT -> SIGCNT
gmapT :: (forall b. Data b => b -> b) -> SIGCNT -> SIGCNT
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SIGCNT -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SIGCNT -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SIGCNT -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SIGCNT -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SIGCNT -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> SIGCNT -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SIGCNT -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SIGCNT -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SIGCNT -> m SIGCNT
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SIGCNT -> m SIGCNT
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SIGCNT -> m SIGCNT
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SIGCNT -> m SIGCNT
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SIGCNT -> m SIGCNT
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SIGCNT -> m SIGCNT
Data)
data SigcntPredicateFailure
=
TooManyIssuedBlocks VKeyGenesis
|
NotADelegate
deriving (SigcntPredicateFailure -> SigcntPredicateFailure -> Bool
(SigcntPredicateFailure -> SigcntPredicateFailure -> Bool)
-> (SigcntPredicateFailure -> SigcntPredicateFailure -> Bool)
-> Eq SigcntPredicateFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SigcntPredicateFailure -> SigcntPredicateFailure -> Bool
== :: SigcntPredicateFailure -> SigcntPredicateFailure -> Bool
$c/= :: SigcntPredicateFailure -> SigcntPredicateFailure -> Bool
/= :: SigcntPredicateFailure -> SigcntPredicateFailure -> Bool
Eq, Int -> SigcntPredicateFailure -> ShowS
[SigcntPredicateFailure] -> ShowS
SigcntPredicateFailure -> String
(Int -> SigcntPredicateFailure -> ShowS)
-> (SigcntPredicateFailure -> String)
-> ([SigcntPredicateFailure] -> ShowS)
-> Show SigcntPredicateFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SigcntPredicateFailure -> ShowS
showsPrec :: Int -> SigcntPredicateFailure -> ShowS
$cshow :: SigcntPredicateFailure -> String
show :: SigcntPredicateFailure -> String
$cshowList :: [SigcntPredicateFailure] -> ShowS
showList :: [SigcntPredicateFailure] -> ShowS
Show, Typeable SigcntPredicateFailure
Typeable SigcntPredicateFailure =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> SigcntPredicateFailure
-> c SigcntPredicateFailure)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SigcntPredicateFailure)
-> (SigcntPredicateFailure -> Constr)
-> (SigcntPredicateFailure -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SigcntPredicateFailure))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SigcntPredicateFailure))
-> ((forall b. Data b => b -> b)
-> SigcntPredicateFailure -> SigcntPredicateFailure)
-> (forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> SigcntPredicateFailure
-> r)
-> (forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> SigcntPredicateFailure
-> r)
-> (forall u.
(forall d. Data d => d -> u) -> SigcntPredicateFailure -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> SigcntPredicateFailure -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SigcntPredicateFailure -> m SigcntPredicateFailure)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SigcntPredicateFailure -> m SigcntPredicateFailure)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SigcntPredicateFailure -> m SigcntPredicateFailure)
-> Data SigcntPredicateFailure
SigcntPredicateFailure -> Constr
SigcntPredicateFailure -> DataType
(forall b. Data b => b -> b)
-> SigcntPredicateFailure -> SigcntPredicateFailure
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) -> SigcntPredicateFailure -> u
forall u.
(forall d. Data d => d -> u) -> SigcntPredicateFailure -> [u]
forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> SigcntPredicateFailure
-> r
forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> SigcntPredicateFailure
-> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SigcntPredicateFailure -> m SigcntPredicateFailure
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SigcntPredicateFailure -> m SigcntPredicateFailure
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SigcntPredicateFailure
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> SigcntPredicateFailure
-> c SigcntPredicateFailure
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SigcntPredicateFailure)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SigcntPredicateFailure)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> SigcntPredicateFailure
-> c SigcntPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> SigcntPredicateFailure
-> c SigcntPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SigcntPredicateFailure
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SigcntPredicateFailure
$ctoConstr :: SigcntPredicateFailure -> Constr
toConstr :: SigcntPredicateFailure -> Constr
$cdataTypeOf :: SigcntPredicateFailure -> DataType
dataTypeOf :: SigcntPredicateFailure -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SigcntPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SigcntPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SigcntPredicateFailure)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SigcntPredicateFailure)
$cgmapT :: (forall b. Data b => b -> b)
-> SigcntPredicateFailure -> SigcntPredicateFailure
gmapT :: (forall b. Data b => b -> b)
-> SigcntPredicateFailure -> SigcntPredicateFailure
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> SigcntPredicateFailure
-> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> SigcntPredicateFailure
-> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> SigcntPredicateFailure
-> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> SigcntPredicateFailure
-> r
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> SigcntPredicateFailure -> [u]
gmapQ :: forall u.
(forall d. Data d => d -> u) -> SigcntPredicateFailure -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> SigcntPredicateFailure -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> SigcntPredicateFailure -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SigcntPredicateFailure -> m SigcntPredicateFailure
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SigcntPredicateFailure -> m SigcntPredicateFailure
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SigcntPredicateFailure -> m SigcntPredicateFailure
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SigcntPredicateFailure -> m SigcntPredicateFailure
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SigcntPredicateFailure -> m SigcntPredicateFailure
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SigcntPredicateFailure -> m SigcntPredicateFailure
Data)
instance STS SIGCNT where
type
Environment SIGCNT =
( PParams
, Bimap VKeyGenesis VKey
, BlockCount
)
type State SIGCNT = Seq VKeyGenesis
type Signal SIGCNT = VKey
type PredicateFailure SIGCNT = SigcntPredicateFailure
initialRules :: [InitialRule SIGCNT]
initialRules = []
transitionRules :: [TransitionRule SIGCNT]
transitionRules =
[ do
TRC ((PParams
pps, Bimap VKeyGenesis VKey
dms, BlockCount
k), State SIGCNT
sgs, Signal SIGCNT
vk) <- Rule SIGCNT 'Transition (RuleContext 'Transition SIGCNT)
F (Clause SIGCNT 'Transition) (TRC SIGCNT)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
let t' :: BkSgnCntT
t' = PParams
pps PParams -> Getting BkSgnCntT PParams BkSgnCntT -> BkSgnCntT
forall s a. s -> Getting a s a -> a
^. Getting BkSgnCntT PParams BkSgnCntT
Lens' PParams BkSgnCntT
bkSgnCntT
case VKey -> Bimap VKeyGenesis VKey -> Maybe VKeyGenesis
forall a b (m :: * -> *).
(Ord a, Ord b, MonadThrow m) =>
b -> Bimap a b -> m a
Bimap.lookupR VKey
Signal SIGCNT
vk Bimap VKeyGenesis VKey
dms of
Just VKeyGenesis
vkG -> do
let sgs' :: Seq VKeyGenesis
sgs' = Int -> Seq VKeyGenesis -> Seq VKeyGenesis
forall a. Int -> Seq a -> Seq a
S.drop (Seq VKeyGenesis -> Int
forall a. Seq a -> Int
S.length Seq VKeyGenesis
State SIGCNT
sgs Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word64 -> Int) -> (BlockCount -> Word64) -> BlockCount -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BlockCount -> Word64
unBlockCount (BlockCount -> Int) -> BlockCount -> Int
forall a b. (a -> b) -> a -> b
$ BlockCount
k)) (Seq VKeyGenesis
State SIGCNT
sgs Seq VKeyGenesis -> VKeyGenesis -> Seq VKeyGenesis
forall a. Seq a -> a -> Seq a
|> VKeyGenesis
vkG)
nrSignedBks :: BkSgnCntT
nrSignedBks = Int -> BkSgnCntT
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Seq VKeyGenesis -> Int
forall a. Seq a -> Int
S.length ((VKeyGenesis -> Bool) -> Seq VKeyGenesis -> Seq VKeyGenesis
forall a. (a -> Bool) -> Seq a -> Seq a
S.filter (VKeyGenesis -> VKeyGenesis -> Bool
forall a. Eq a => a -> a -> Bool
== VKeyGenesis
vkG) Seq VKeyGenesis
sgs'))
BkSgnCntT
nrSignedBks BkSgnCntT -> BkSgnCntT -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64 -> BkSgnCntT
forall a b. (Integral a, Num b) => a -> b
fromIntegral (BlockCount -> Word64
unBlockCount BlockCount
k) BkSgnCntT -> BkSgnCntT -> BkSgnCntT
forall a. Num a => a -> a -> a
* BkSgnCntT
t' Bool -> PredicateFailure SIGCNT -> Rule SIGCNT 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! VKeyGenesis -> SigcntPredicateFailure
TooManyIssuedBlocks VKeyGenesis
vkG
Seq VKeyGenesis -> F (Clause SIGCNT 'Transition) (Seq VKeyGenesis)
forall a. a -> F (Clause SIGCNT 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Seq VKeyGenesis
-> F (Clause SIGCNT 'Transition) (Seq VKeyGenesis))
-> Seq VKeyGenesis
-> F (Clause SIGCNT 'Transition) (Seq VKeyGenesis)
forall a b. (a -> b) -> a -> b
$! Seq VKeyGenesis
sgs'
Maybe VKeyGenesis
Nothing -> do
PredicateFailure SIGCNT -> Rule SIGCNT 'Transition ()
forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause PredicateFailure SIGCNT
SigcntPredicateFailure
NotADelegate
Seq VKeyGenesis -> F (Clause SIGCNT 'Transition) (Seq VKeyGenesis)
forall a. a -> F (Clause SIGCNT 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Seq VKeyGenesis
-> F (Clause SIGCNT 'Transition) (Seq VKeyGenesis))
-> Seq VKeyGenesis
-> F (Clause SIGCNT 'Transition) (Seq VKeyGenesis)
forall a b. (a -> b) -> a -> b
$! Seq VKeyGenesis
State SIGCNT
sgs
]
issuer ::
Environment SIGCNT ->
State SIGCNT ->
Gen VKey
issuer :: Environment SIGCNT -> State SIGCNT -> Gen VKey
issuer (PParams
pps, Bimap VKeyGenesis VKey
dms, BlockCount
k) State SIGCNT
sgs =
if [VKey] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VKey]
validIssuers
then
String -> Gen VKey
forall a. HasCallStack => String -> a
error (String -> Gen VKey) -> String -> Gen VKey
forall a b. (a -> b) -> a -> b
$
String
"No valid issuers!"
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"k = "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ BlockCount -> String
forall a. Show a => a -> String
show BlockCount
k
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"keys = "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ [VKey] -> String
forall a. Show a => a -> String
show (Bimap VKeyGenesis VKey -> [VKey]
forall a b. Bimap a b -> [b]
Bimap.elems Bimap VKeyGenesis VKey
dms)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"sgs = "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Seq VKeyGenesis -> String
forall a. Show a => a -> String
show Seq VKeyGenesis
State SIGCNT
sgs
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"length sgs = "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Seq VKeyGenesis -> Int
forall a. Seq a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq VKeyGenesis
State SIGCNT
sgs)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_bkSgnCntT = "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ BkSgnCntT -> String
forall a. Show a => a -> String
show (PParams -> BkSgnCntT
_bkSgnCntT PParams
pps)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"dms = "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bimap VKeyGenesis VKey -> String
forall a. Show a => a -> String
show Bimap VKeyGenesis VKey
dms
else [VKey] -> Gen VKey
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, MonadGen m) =>
f a -> m a
Gen.element [VKey]
validIssuers
where
validIssuers :: [VKey]
validIssuers =
(VKey -> Bool) -> [VKey] -> [VKey]
forall a. (a -> Bool) -> [a] -> [a]
filter VKey -> Bool
canIssueABlock [VKey]
anyIssuer
anyIssuer :: [VKey]
anyIssuer = Bimap VKeyGenesis VKey -> [VKey]
forall a b. Bimap a b -> [b]
Bimap.elems Bimap VKeyGenesis VKey
dms
canIssueABlock :: VKey -> Bool
canIssueABlock :: VKey -> Bool
canIssueABlock VKey
vk =
(Bool -> NonEmpty SigcntPredicateFailure -> Bool
forall a b. a -> b -> a
const Bool
False (NonEmpty (PredicateFailure SIGCNT) -> Bool)
-> (State SIGCNT -> Bool)
-> Either (NonEmpty (PredicateFailure SIGCNT)) (State SIGCNT)
-> Bool
forall b d c. (b -> d) -> (c -> d) -> Either b c -> d
forall (a :: * -> * -> *) b d c.
ArrowChoice a =>
a b d -> a c d -> a (Either b c) d
||| Bool -> Seq VKeyGenesis -> Bool
forall a b. a -> b -> a
const Bool
True) (Either (NonEmpty (PredicateFailure SIGCNT)) (State SIGCNT)
-> Bool)
-> Either (NonEmpty (PredicateFailure SIGCNT)) (State SIGCNT)
-> Bool
forall a b. (a -> b) -> a -> b
$ forall s (rtype :: RuleType).
(STS s, RuleTypeRep rtype, BaseM s ~ Identity) =>
RuleContext rtype s
-> Either (NonEmpty (PredicateFailure s)) (State s)
applySTS @SIGCNT ((Environment SIGCNT, State SIGCNT, Signal SIGCNT) -> TRC SIGCNT
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC ((PParams
pps, Bimap VKeyGenesis VKey
dms, BlockCount
k), State SIGCNT
sgs, VKey
Signal SIGCNT
vk))
sigCntT :: BlockCount -> Word8 -> Gen Double
sigCntT :: BlockCount -> Word8 -> Gen Double
sigCntT (BlockCount Word64
k) Word8
ngk =
Range Double -> Gen Double
forall (m :: * -> *). MonadGen m => Range Double -> m Double
Gen.double (Double -> Double -> Range Double
forall a. a -> a -> Range a
Range.constant Double
lower Double
upper)
where
lower :: Double
lower = Double
1 Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ (Word8 -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word8
ngk Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
0.7) Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
1 Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Word64 -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
k
upper :: Double
upper = Double
1 Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ (Word8 -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word8
ngk Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
0.5) Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
1 Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Word64 -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
k