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

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

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) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        let t' :: BkSgnCntT
t' = PParams
pps forall s a. s -> Getting a s a -> a
^. Lens' PParams BkSgnCntT
bkSgnCntT
        case forall a b (m :: * -> *).
(Ord a, Ord b, MonadThrow m) =>
b -> Bimap a b -> m a
Bimap.lookupR Signal SIGCNT
vk Bimap VKeyGenesis VKey
dms of
          Just VKeyGenesis
vkG -> do
            let sgs' :: Seq VKeyGenesis
sgs' = forall a. Int -> Seq a -> Seq a
S.drop (forall a. Seq a -> Int
S.length State SIGCNT
sgs forall a. Num a => a -> a -> a
+ Int
1 forall a. Num a => a -> a -> a
- (forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. BlockCount -> Word64
unBlockCount forall a b. (a -> b) -> a -> b
$ BlockCount
k)) (State SIGCNT
sgs forall a. Seq a -> a -> Seq a
|> VKeyGenesis
vkG)
                nrSignedBks :: BkSgnCntT
nrSignedBks = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Seq a -> Int
S.length (forall a. (a -> Bool) -> Seq a -> Seq a
S.filter (forall a. Eq a => a -> a -> Bool
== VKeyGenesis
vkG) Seq VKeyGenesis
sgs'))
            BkSgnCntT
nrSignedBks forall a. Ord a => a -> a -> Bool
<= forall a b. (Integral a, Num b) => a -> b
fromIntegral (BlockCount -> Word64
unBlockCount BlockCount
k) forall a. Num a => a -> a -> a
* BkSgnCntT
t' forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! VKeyGenesis -> SigcntPredicateFailure
TooManyIssuedBlocks VKeyGenesis
vkG
            forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Seq VKeyGenesis
sgs'
          Maybe VKeyGenesis
Nothing -> do
            forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause SigcntPredicateFailure
NotADelegate
            forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! 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 forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VKey]
validIssuers
    then
      forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$
        String
"No valid issuers!"
          forall a. [a] -> [a] -> [a]
++ String
"\n"
          forall a. [a] -> [a] -> [a]
++ String
"k = "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show BlockCount
k
          forall a. [a] -> [a] -> [a]
++ String
"\n"
          forall a. [a] -> [a] -> [a]
++ String
"keys = "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a b. Bimap a b -> [b]
Bimap.elems Bimap VKeyGenesis VKey
dms)
          forall a. [a] -> [a] -> [a]
++ String
"\n"
          forall a. [a] -> [a] -> [a]
++ String
"sgs = "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show State SIGCNT
sgs
          forall a. [a] -> [a] -> [a]
++ String
"\n"
          forall a. [a] -> [a] -> [a]
++ String
"length sgs = "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length State SIGCNT
sgs)
          forall a. [a] -> [a] -> [a]
++ String
"\n"
          forall a. [a] -> [a] -> [a]
++ String
"_bkSgnCntT = "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (PParams -> BkSgnCntT
_bkSgnCntT PParams
pps)
          forall a. [a] -> [a] -> [a]
++ String
"\n"
          forall a. [a] -> [a] -> [a]
++ String
"dms = "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Bimap VKeyGenesis VKey
dms
    else forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, MonadGen m) =>
f a -> m a
Gen.element [VKey]
validIssuers
  where
    validIssuers :: [VKey]
validIssuers =
      forall a. (a -> Bool) -> [a] -> [a]
filter VKey -> Bool
canIssueABlock [VKey]
anyIssuer
    anyIssuer :: [VKey]
anyIssuer = forall a b. Bimap a b -> [b]
Bimap.elems Bimap VKeyGenesis VKey
dms
    canIssueABlock :: VKey -> Bool
    canIssueABlock :: VKey -> Bool
canIssueABlock VKey
vk =
      (forall a b. a -> b -> a
const Bool
False forall (a :: * -> * -> *) b d c.
ArrowChoice a =>
a b d -> a c d -> a (Either b c) d
||| forall a b. a -> b -> a
const Bool
True) 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 (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC ((PParams
pps, Bimap VKeyGenesis VKey
dms, BlockCount
k), State SIGCNT
sgs, VKey
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 =
  forall (m :: * -> *). MonadGen m => Range Double -> m Double
Gen.double (forall a. a -> a -> Range a
Range.constant Double
lower Double
upper)
  where
    lower :: Double
lower = Double
1 forall a. Fractional a => a -> a -> a
/ (forall a b. (Integral a, Num b) => a -> b
fromIntegral Word8
ngk forall a. Num a => a -> a -> a
* Double
0.7) forall a. Num a => a -> a -> a
+ Double
1 forall a. Fractional a => a -> a -> a
/ forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
k
    upper :: Double
upper = Double
1 forall a. Fractional a => a -> a -> a
/ (forall a b. (Integral a, Num b) => a -> b
fromIntegral Word8
ngk forall a. Num a => a -> a -> a
* Double
0.5) forall a. Num a => a -> a -> a
+ Double
1 forall a. Fractional a => a -> a -> a
/ forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
k