{-# 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)

-- | These `PredicateFailure`s are all throwable.
data SigcntPredicateFailure
  = -- | The given genesis key issued too many blocks.
    TooManyIssuedBlocks VKeyGenesis
  | -- | The key signing the block is not a delegate of a genesis key.
    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 -- Chain stability parameter
      )

  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 -- TODO: this is a quite inconvenient encoding for this transition system!
    ]

----------------------------------------------------------------------------------------------------
-- Generators
----------------------------------------------------------------------------------------------------

-- | Generate an issuer that can still issue blocks according to the @SIGCNT@ rule. The issuers are
-- taken from the range of the delegation map passed as parameter.
--
-- This generator will throw an error if no suitable issuer can be found, which means that the block
-- production halted.
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))

-- | Generate a signature count threshold given a chain stability parameter @k@ and number of
-- genesis keys @ngk@.
--
-- This threshold must allow that all the (honest) genesis keys can issue enough blocks to fill the
-- rolling window of @k@. If this is not possible, then the block production will halt since there
-- will not be valid issuers. So the threshold must make it possible to find an integer @n@ such
-- that:
--
-- > n <= k * t
--
-- and
--
-- > k < ngk * n
-- > = { algebra }
-- > k / ngk < n
--
-- We know there must be an integer in the interval
--
-- > (k/ngk, k/ngk + 1]
--
-- So to satisfy the requirements above, we can pick a @t@ such that:
--
-- > k/ngk + 1 <= k * t
-- > = { algebra }
-- > 1/ngk + 1/k <= t
--
-- To pick a value for @t@ we vary the proportion of honest keys.
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