{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Cardano.Protocol.TPraos.Rules.Overlay (
  OVERLAY,
  PredicateFailure,
  OverlayEnv (..),
  OverlayPredicateFailure (..),
  OBftSlot (..),
  classifyOverlaySlot,
  lookupInOverlaySchedule,
  overlaySlots,
) where

import qualified Cardano.Crypto.KES as KES
import qualified Cardano.Crypto.VRF as VRF
import Cardano.Ledger.BHeaderView (isOverlaySlot)
import Cardano.Ledger.BaseTypes (
  ActiveSlotCoeff,
  BoundedRational (..),
  Nonce,
  Seed,
  ShelleyBase,
  UnitInterval,
  activeSlotCoeff,
  activeSlotVal,
  epochInfoPure,
 )
import Cardano.Ledger.Binary (
  DecCBOR (..),
  EncCBOR (..),
  TokenType (TypeNull),
  decodeNull,
  encodeNull,
  peekTokenType,
 )
import Cardano.Ledger.Keys (
  GenDelegPair (..),
  GenDelegs (..),
  KeyHash (..),
  KeyRole (..),
  coerceKeyRole,
  hashKey,
 )
import Cardano.Ledger.Slot (epochInfoEpoch, epochInfoFirst, (-*))
import Cardano.Ledger.State (
  IndividualPoolStake (..),
  PoolDistr (..),
 )
import Cardano.Protocol.Crypto
import Cardano.Protocol.TPraos.BHeader (
  BHBody (..),
  BHeader (BHeader),
  checkLeaderValue,
  issuerIDfromBHBody,
  mkSeed,
  seedEta,
  seedL,
 )
import Cardano.Protocol.TPraos.Rules.OCert (OCERT, OCertEnv (..))
import Cardano.Slotting.Slot
import Control.DeepSeq (NFData)
import Control.Monad (unless)
import Control.Monad.Except (throwError)
import Control.Monad.Trans.Reader (asks)
import Control.SetAlgebra (dom, eval, range)
import Control.State.Transition
import Data.Coerce (coerce)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Word (Word64)
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))

data OVERLAY c

data OverlayEnv
  = OverlayEnv
      UnitInterval -- the decentralization paramater @d@ from the protocal parameters
      PoolDistr
      GenDelegs
      Nonce
  deriving ((forall x. OverlayEnv -> Rep OverlayEnv x)
-> (forall x. Rep OverlayEnv x -> OverlayEnv) -> Generic OverlayEnv
forall x. Rep OverlayEnv x -> OverlayEnv
forall x. OverlayEnv -> Rep OverlayEnv x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. OverlayEnv -> Rep OverlayEnv x
from :: forall x. OverlayEnv -> Rep OverlayEnv x
$cto :: forall x. Rep OverlayEnv x -> OverlayEnv
to :: forall x. Rep OverlayEnv x -> OverlayEnv
Generic)

instance NoThunks OverlayEnv

data OverlayPredicateFailure c
  = VRFKeyUnknown
      (KeyHash 'StakePool) -- unknown VRF keyhash (not registered)
  | VRFKeyWrongVRFKey
      (KeyHash 'StakePool) -- KeyHash of block issuer
      (VRFVerKeyHash 'StakePoolVRF) -- VRF KeyHash registered with stake pool
      (VRFVerKeyHash 'BlockIssuerVRF) -- VRF KeyHash from Header
  | VRFKeyBadNonce
      Nonce -- Nonce constant to distinguish VRF nonce values
      SlotNo -- Slot used for VRF calculation
      Nonce -- Epoch nonce used for VRF calculation
      (VRF.CertifiedVRF (VRF c) Nonce) -- VRF calculated nonce value
  | VRFKeyBadLeaderValue
      Nonce -- Leader constant to distinguish VRF leader values
      SlotNo -- Slot used for VRF calculation
      Nonce -- Epoch nonce used for VRF calculation
      (VRF.CertifiedVRF (VRF c) Nonce) -- VRF calculated leader value
  | VRFLeaderValueTooBig
      (VRF.OutputVRF (VRF c)) -- VRF Leader value
      Rational -- stake pool's relative stake
      ActiveSlotCoeff -- Praos active slot coefficient value
  | NotActiveSlotOVERLAY
      SlotNo -- Slot which is supposed to be silent
  | WrongGenesisColdKeyOVERLAY
      (KeyHash 'BlockIssuer) -- KeyHash of block issuer
      (KeyHash 'GenesisDelegate) -- KeyHash genesis delegate keyhash assigned to this slot
  | WrongGenesisVRFKeyOVERLAY
      (KeyHash 'BlockIssuer) -- KeyHash of block issuer
      (VRFVerKeyHash 'GenDelegVRF) -- VRF KeyHash registered with genesis delegation
      (VRFVerKeyHash 'BlockIssuerVRF) -- VRF KeyHash from Header
  | UnknownGenesisKeyOVERLAY
      (KeyHash 'Genesis) -- KeyHash which does not correspond to o genesis node
  | OcertFailure (PredicateFailure (OCERT c)) -- Subtransition Failures
  deriving ((forall x.
 OverlayPredicateFailure c -> Rep (OverlayPredicateFailure c) x)
-> (forall x.
    Rep (OverlayPredicateFailure c) x -> OverlayPredicateFailure c)
-> Generic (OverlayPredicateFailure c)
forall x.
Rep (OverlayPredicateFailure c) x -> OverlayPredicateFailure c
forall x.
OverlayPredicateFailure c -> Rep (OverlayPredicateFailure c) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c x.
Rep (OverlayPredicateFailure c) x -> OverlayPredicateFailure c
forall c x.
OverlayPredicateFailure c -> Rep (OverlayPredicateFailure c) x
$cfrom :: forall c x.
OverlayPredicateFailure c -> Rep (OverlayPredicateFailure c) x
from :: forall x.
OverlayPredicateFailure c -> Rep (OverlayPredicateFailure c) x
$cto :: forall c x.
Rep (OverlayPredicateFailure c) x -> OverlayPredicateFailure c
to :: forall x.
Rep (OverlayPredicateFailure c) x -> OverlayPredicateFailure c
Generic)

instance
  ( Crypto c
  , KES.Signable (KES c) (BHBody c)
  , VRF.Signable (VRF c) Seed
  ) =>
  STS (OVERLAY c)
  where
  type State (OVERLAY c) = Map (KeyHash 'BlockIssuer) Word64
  type Signal (OVERLAY c) = BHeader c
  type Environment (OVERLAY c) = OverlayEnv
  type BaseM (OVERLAY c) = ShelleyBase
  type PredicateFailure (OVERLAY c) = OverlayPredicateFailure c

  initialRules :: [InitialRule (OVERLAY c)]
initialRules = []

  transitionRules :: [TransitionRule (OVERLAY c)]
transitionRules = [TransitionRule (OVERLAY c)
forall c.
(Crypto c, Signable (KES c) (BHBody c), Signable (VRF c) Seed) =>
TransitionRule (OVERLAY c)
overlayTransition]

deriving instance
  VRF.VRFAlgorithm (VRF c) =>
  Show (OverlayPredicateFailure c)

deriving instance
  VRF.VRFAlgorithm (VRF c) =>
  Eq (OverlayPredicateFailure c)

vrfChecks ::
  forall c.
  ( Crypto c
  , VRF.Signable (VRF c) Seed
  ) =>
  Nonce ->
  BHBody c ->
  Either (PredicateFailure (OVERLAY c)) ()
vrfChecks :: forall c.
(Crypto c, Signable (VRF c) Seed) =>
Nonce -> BHBody c -> Either (PredicateFailure (OVERLAY c)) ()
vrfChecks Nonce
eta0 BHBody c
bhb = do
  Bool
-> Either (OverlayPredicateFailure c) ()
-> Either (OverlayPredicateFailure c) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless
    ( ContextVRF (VRF c)
-> VerKeyVRF (VRF c) -> Seed -> CertifiedVRF (VRF c) Seed -> Bool
forall v a.
(VRFAlgorithm v, Signable v a) =>
ContextVRF v -> VerKeyVRF v -> a -> CertifiedVRF v a -> Bool
VRF.verifyCertified
        ()
        VerKeyVRF (VRF c)
vrfK
        (Nonce -> SlotNo -> Nonce -> Seed
mkSeed Nonce
seedEta SlotNo
slot Nonce
eta0)
        (CertifiedVRF (VRF c) Nonce -> CertifiedVRF (VRF c) Seed
forall a b. Coercible a b => a -> b
coerce (CertifiedVRF (VRF c) Nonce -> CertifiedVRF (VRF c) Seed)
-> CertifiedVRF (VRF c) Nonce -> CertifiedVRF (VRF c) Seed
forall a b. (a -> b) -> a -> b
$ BHBody c -> CertifiedVRF (VRF c) Nonce
forall c. BHBody c -> CertifiedVRF (VRF c) Nonce
bheaderEta BHBody c
bhb)
    )
    (OverlayPredicateFailure c -> Either (OverlayPredicateFailure c) ()
forall a.
OverlayPredicateFailure c -> Either (OverlayPredicateFailure c) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (OverlayPredicateFailure c
 -> Either (OverlayPredicateFailure c) ())
-> OverlayPredicateFailure c
-> Either (OverlayPredicateFailure c) ()
forall a b. (a -> b) -> a -> b
$ Nonce
-> SlotNo
-> Nonce
-> CertifiedVRF (VRF c) Nonce
-> OverlayPredicateFailure c
forall c.
Nonce
-> SlotNo
-> Nonce
-> CertifiedVRF (VRF c) Nonce
-> OverlayPredicateFailure c
VRFKeyBadNonce Nonce
seedEta SlotNo
slot Nonce
eta0 (CertifiedVRF (VRF c) Nonce -> CertifiedVRF (VRF c) Nonce
forall a b. Coercible a b => a -> b
coerce (CertifiedVRF (VRF c) Nonce -> CertifiedVRF (VRF c) Nonce)
-> CertifiedVRF (VRF c) Nonce -> CertifiedVRF (VRF c) Nonce
forall a b. (a -> b) -> a -> b
$ BHBody c -> CertifiedVRF (VRF c) Nonce
forall c. BHBody c -> CertifiedVRF (VRF c) Nonce
bheaderEta BHBody c
bhb))
  Bool
-> Either (OverlayPredicateFailure c) ()
-> Either (OverlayPredicateFailure c) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless
    ( ContextVRF (VRF c)
-> VerKeyVRF (VRF c) -> Seed -> CertifiedVRF (VRF c) Seed -> Bool
forall v a.
(VRFAlgorithm v, Signable v a) =>
ContextVRF v -> VerKeyVRF v -> a -> CertifiedVRF v a -> Bool
VRF.verifyCertified
        ()
        VerKeyVRF (VRF c)
vrfK
        (Nonce -> SlotNo -> Nonce -> Seed
mkSeed Nonce
seedL SlotNo
slot Nonce
eta0)
        (CertifiedVRF (VRF c) Natural -> CertifiedVRF (VRF c) Seed
forall a b. Coercible a b => a -> b
coerce (CertifiedVRF (VRF c) Natural -> CertifiedVRF (VRF c) Seed)
-> CertifiedVRF (VRF c) Natural -> CertifiedVRF (VRF c) Seed
forall a b. (a -> b) -> a -> b
$ BHBody c -> CertifiedVRF (VRF c) Natural
forall c. BHBody c -> CertifiedVRF (VRF c) Natural
bheaderL BHBody c
bhb)
    )
    (OverlayPredicateFailure c -> Either (OverlayPredicateFailure c) ()
forall a.
OverlayPredicateFailure c -> Either (OverlayPredicateFailure c) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (OverlayPredicateFailure c
 -> Either (OverlayPredicateFailure c) ())
-> OverlayPredicateFailure c
-> Either (OverlayPredicateFailure c) ()
forall a b. (a -> b) -> a -> b
$ Nonce
-> SlotNo
-> Nonce
-> CertifiedVRF (VRF c) Nonce
-> OverlayPredicateFailure c
forall c.
Nonce
-> SlotNo
-> Nonce
-> CertifiedVRF (VRF c) Nonce
-> OverlayPredicateFailure c
VRFKeyBadLeaderValue Nonce
seedL SlotNo
slot Nonce
eta0 (CertifiedVRF (VRF c) Natural -> CertifiedVRF (VRF c) Nonce
forall a b. Coercible a b => a -> b
coerce (CertifiedVRF (VRF c) Natural -> CertifiedVRF (VRF c) Nonce)
-> CertifiedVRF (VRF c) Natural -> CertifiedVRF (VRF c) Nonce
forall a b. (a -> b) -> a -> b
$ BHBody c -> CertifiedVRF (VRF c) Natural
forall c. BHBody c -> CertifiedVRF (VRF c) Natural
bheaderL BHBody c
bhb))
  where
    vrfK :: VerKeyVRF (VRF c)
vrfK = BHBody c -> VerKeyVRF (VRF c)
forall c. BHBody c -> VerKeyVRF (VRF c)
bheaderVrfVk BHBody c
bhb
    slot :: SlotNo
slot = BHBody c -> SlotNo
forall c. BHBody c -> SlotNo
bheaderSlotNo BHBody c
bhb

praosVrfChecks ::
  forall c.
  ( Crypto c
  , VRF.Signable (VRF c) Seed
  ) =>
  Nonce ->
  PoolDistr ->
  ActiveSlotCoeff ->
  BHBody c ->
  Either (PredicateFailure (OVERLAY c)) ()
praosVrfChecks :: forall c.
(Crypto c, Signable (VRF c) Seed) =>
Nonce
-> PoolDistr
-> ActiveSlotCoeff
-> BHBody c
-> Either (PredicateFailure (OVERLAY c)) ()
praosVrfChecks Nonce
eta0 (PoolDistr Map (KeyHash 'StakePool) IndividualPoolStake
pd CompactForm Coin
_tot) ActiveSlotCoeff
f BHBody c
bhb = do
  let sigma' :: Maybe IndividualPoolStake
sigma' = KeyHash 'StakePool
-> Map (KeyHash 'StakePool) IndividualPoolStake
-> Maybe IndividualPoolStake
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KeyHash 'StakePool
hk Map (KeyHash 'StakePool) IndividualPoolStake
pd
  case Maybe IndividualPoolStake
sigma' of
    Maybe IndividualPoolStake
Nothing -> OverlayPredicateFailure c
-> Either (PredicateFailure (OVERLAY c)) ()
forall a.
OverlayPredicateFailure c
-> Either (PredicateFailure (OVERLAY c)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (OverlayPredicateFailure c
 -> Either (PredicateFailure (OVERLAY c)) ())
-> OverlayPredicateFailure c
-> Either (PredicateFailure (OVERLAY c)) ()
forall a b. (a -> b) -> a -> b
$ KeyHash 'StakePool -> OverlayPredicateFailure c
forall c. KeyHash 'StakePool -> OverlayPredicateFailure c
VRFKeyUnknown KeyHash 'StakePool
hk
    Just (IndividualPoolStake Rational
sigma CompactForm Coin
_ VRFVerKeyHash 'StakePoolVRF
stakePoolVRFVerKeyHash) -> do
      Bool
-> Either (OverlayPredicateFailure c) ()
-> Either (OverlayPredicateFailure c) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless
        (VRFVerKeyHash 'StakePoolVRF -> Hash HASH KeyRoleVRF
forall (r :: KeyRoleVRF). VRFVerKeyHash r -> Hash HASH KeyRoleVRF
unVRFVerKeyHash VRFVerKeyHash 'StakePoolVRF
stakePoolVRFVerKeyHash Hash HASH KeyRoleVRF -> Hash HASH KeyRoleVRF -> Bool
forall a. Eq a => a -> a -> Bool
== VRFVerKeyHash 'BlockIssuerVRF -> Hash HASH KeyRoleVRF
forall (r :: KeyRoleVRF). VRFVerKeyHash r -> Hash HASH KeyRoleVRF
unVRFVerKeyHash VRFVerKeyHash 'BlockIssuerVRF
blockIssuerVRFVerKeyHash)
        (OverlayPredicateFailure c -> Either (OverlayPredicateFailure c) ()
forall a.
OverlayPredicateFailure c -> Either (OverlayPredicateFailure c) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (OverlayPredicateFailure c
 -> Either (OverlayPredicateFailure c) ())
-> OverlayPredicateFailure c
-> Either (OverlayPredicateFailure c) ()
forall a b. (a -> b) -> a -> b
$ KeyHash 'StakePool
-> VRFVerKeyHash 'StakePoolVRF
-> VRFVerKeyHash 'BlockIssuerVRF
-> OverlayPredicateFailure c
forall c.
KeyHash 'StakePool
-> VRFVerKeyHash 'StakePoolVRF
-> VRFVerKeyHash 'BlockIssuerVRF
-> OverlayPredicateFailure c
VRFKeyWrongVRFKey KeyHash 'StakePool
hk VRFVerKeyHash 'StakePoolVRF
stakePoolVRFVerKeyHash VRFVerKeyHash 'BlockIssuerVRF
blockIssuerVRFVerKeyHash)
      Nonce -> BHBody c -> Either (PredicateFailure (OVERLAY c)) ()
forall c.
(Crypto c, Signable (VRF c) Seed) =>
Nonce -> BHBody c -> Either (PredicateFailure (OVERLAY c)) ()
vrfChecks Nonce
eta0 BHBody c
bhb
      Bool
-> Either (OverlayPredicateFailure c) ()
-> Either (OverlayPredicateFailure c) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless
        (OutputVRF (VRF c) -> Rational -> ActiveSlotCoeff -> Bool
forall v.
VRFAlgorithm v =>
OutputVRF v -> Rational -> ActiveSlotCoeff -> Bool
checkLeaderValue (CertifiedVRF (VRF c) Natural -> OutputVRF (VRF c)
forall v a. CertifiedVRF v a -> OutputVRF v
VRF.certifiedOutput (CertifiedVRF (VRF c) Natural -> OutputVRF (VRF c))
-> CertifiedVRF (VRF c) Natural -> OutputVRF (VRF c)
forall a b. (a -> b) -> a -> b
$ BHBody c -> CertifiedVRF (VRF c) Natural
forall c. BHBody c -> CertifiedVRF (VRF c) Natural
bheaderL BHBody c
bhb) Rational
sigma ActiveSlotCoeff
f)
        (OverlayPredicateFailure c -> Either (OverlayPredicateFailure c) ()
forall a.
OverlayPredicateFailure c -> Either (OverlayPredicateFailure c) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (OverlayPredicateFailure c
 -> Either (OverlayPredicateFailure c) ())
-> OverlayPredicateFailure c
-> Either (OverlayPredicateFailure c) ()
forall a b. (a -> b) -> a -> b
$ OutputVRF (VRF c)
-> Rational -> ActiveSlotCoeff -> OverlayPredicateFailure c
forall c.
OutputVRF (VRF c)
-> Rational -> ActiveSlotCoeff -> OverlayPredicateFailure c
VRFLeaderValueTooBig (CertifiedVRF (VRF c) Natural -> OutputVRF (VRF c)
forall v a. CertifiedVRF v a -> OutputVRF v
VRF.certifiedOutput (CertifiedVRF (VRF c) Natural -> OutputVRF (VRF c))
-> CertifiedVRF (VRF c) Natural -> OutputVRF (VRF c)
forall a b. (a -> b) -> a -> b
$ BHBody c -> CertifiedVRF (VRF c) Natural
forall c. BHBody c -> CertifiedVRF (VRF c) Natural
bheaderL BHBody c
bhb) Rational
sigma ActiveSlotCoeff
f)
  where
    hk :: KeyHash 'StakePool
hk = KeyHash 'BlockIssuer -> KeyHash 'StakePool
forall (r :: KeyRole) (r' :: KeyRole). KeyHash r -> KeyHash r'
forall (a :: KeyRole -> *) (r :: KeyRole) (r' :: KeyRole).
HasKeyRole a =>
a r -> a r'
coerceKeyRole (KeyHash 'BlockIssuer -> KeyHash 'StakePool)
-> (BHBody c -> KeyHash 'BlockIssuer)
-> BHBody c
-> KeyHash 'StakePool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BHBody c -> KeyHash 'BlockIssuer
forall c. BHBody c -> KeyHash 'BlockIssuer
issuerIDfromBHBody (BHBody c -> KeyHash 'StakePool) -> BHBody c -> KeyHash 'StakePool
forall a b. (a -> b) -> a -> b
$ BHBody c
bhb
    blockIssuerVRFVerKeyHash :: VRFVerKeyHash 'BlockIssuerVRF
blockIssuerVRFVerKeyHash = forall c (r :: KeyRoleVRF).
Crypto c =>
VerKeyVRF (VRF c) -> VRFVerKeyHash r
hashVerKeyVRF @c (BHBody c -> VerKeyVRF (VRF c)
forall c. BHBody c -> VerKeyVRF (VRF c)
bheaderVrfVk BHBody c
bhb)

pbftVrfChecks ::
  forall c.
  ( Crypto c
  , VRF.Signable (VRF c) Seed
  ) =>
  VRFVerKeyHash 'GenDelegVRF ->
  Nonce ->
  BHBody c ->
  Either (PredicateFailure (OVERLAY c)) ()
pbftVrfChecks :: forall c.
(Crypto c, Signable (VRF c) Seed) =>
VRFVerKeyHash 'GenDelegVRF
-> Nonce -> BHBody c -> Either (PredicateFailure (OVERLAY c)) ()
pbftVrfChecks VRFVerKeyHash 'GenDelegVRF
genDelegVRFVerKeyHash Nonce
eta0 BHBody c
bhb = do
  Bool
-> Either (OverlayPredicateFailure c) ()
-> Either (OverlayPredicateFailure c) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless
    (VRFVerKeyHash 'GenDelegVRF -> Hash HASH KeyRoleVRF
forall (r :: KeyRoleVRF). VRFVerKeyHash r -> Hash HASH KeyRoleVRF
unVRFVerKeyHash VRFVerKeyHash 'GenDelegVRF
genDelegVRFVerKeyHash Hash HASH KeyRoleVRF -> Hash HASH KeyRoleVRF -> Bool
forall a. Eq a => a -> a -> Bool
== VRFVerKeyHash 'BlockIssuerVRF -> Hash HASH KeyRoleVRF
forall (r :: KeyRoleVRF). VRFVerKeyHash r -> Hash HASH KeyRoleVRF
unVRFVerKeyHash VRFVerKeyHash 'BlockIssuerVRF
blockIssuerVRFVerKeyHash)
    (OverlayPredicateFailure c -> Either (OverlayPredicateFailure c) ()
forall a.
OverlayPredicateFailure c -> Either (OverlayPredicateFailure c) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (OverlayPredicateFailure c
 -> Either (OverlayPredicateFailure c) ())
-> OverlayPredicateFailure c
-> Either (OverlayPredicateFailure c) ()
forall a b. (a -> b) -> a -> b
$ KeyHash 'BlockIssuer
-> VRFVerKeyHash 'GenDelegVRF
-> VRFVerKeyHash 'BlockIssuerVRF
-> OverlayPredicateFailure c
forall c.
KeyHash 'BlockIssuer
-> VRFVerKeyHash 'GenDelegVRF
-> VRFVerKeyHash 'BlockIssuerVRF
-> OverlayPredicateFailure c
WrongGenesisVRFKeyOVERLAY KeyHash 'BlockIssuer
hk VRFVerKeyHash 'GenDelegVRF
genDelegVRFVerKeyHash VRFVerKeyHash 'BlockIssuerVRF
blockIssuerVRFVerKeyHash)
  Nonce -> BHBody c -> Either (PredicateFailure (OVERLAY c)) ()
forall c.
(Crypto c, Signable (VRF c) Seed) =>
Nonce -> BHBody c -> Either (PredicateFailure (OVERLAY c)) ()
vrfChecks Nonce
eta0 BHBody c
bhb
  () -> Either (OverlayPredicateFailure c) ()
forall a. a -> Either (OverlayPredicateFailure c) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  where
    hk :: KeyHash 'BlockIssuer
hk = BHBody c -> KeyHash 'BlockIssuer
forall c. BHBody c -> KeyHash 'BlockIssuer
issuerIDfromBHBody BHBody c
bhb
    blockIssuerVRFVerKeyHash :: VRFVerKeyHash 'BlockIssuerVRF
blockIssuerVRFVerKeyHash = forall c (r :: KeyRoleVRF).
Crypto c =>
VerKeyVRF (VRF c) -> VRFVerKeyHash r
hashVerKeyVRF @c (BHBody c -> VerKeyVRF (VRF c)
forall c. BHBody c -> VerKeyVRF (VRF c)
bheaderVrfVk BHBody c
bhb)

overlayTransition ::
  forall c.
  ( Crypto c
  , KES.Signable (KES c) (BHBody c)
  , VRF.Signable (VRF c) Seed
  ) =>
  TransitionRule (OVERLAY c)
overlayTransition :: forall c.
(Crypto c, Signable (KES c) (BHBody c), Signable (VRF c) Seed) =>
TransitionRule (OVERLAY c)
overlayTransition =
  Rule (OVERLAY c) 'Transition (RuleContext 'Transition (OVERLAY c))
F (Clause (OVERLAY c) 'Transition) (TRC (OVERLAY c))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
    F (Clause (OVERLAY c) 'Transition) (TRC (OVERLAY c))
-> (TRC (OVERLAY c)
    -> F (Clause (OVERLAY c) 'Transition)
         (Map (KeyHash 'BlockIssuer) Word64))
-> F (Clause (OVERLAY c) 'Transition)
     (Map (KeyHash 'BlockIssuer) Word64)
forall a b.
F (Clause (OVERLAY c) 'Transition) a
-> (a -> F (Clause (OVERLAY c) 'Transition) b)
-> F (Clause (OVERLAY c) 'Transition) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \( TRC
             ( OverlayEnv UnitInterval
dval PoolDistr
pd (GenDelegs Map (KeyHash 'Genesis) GenDelegPair
genDelegs) Nonce
eta0
               , State (OVERLAY c)
cs
               , bh :: Signal (OVERLAY c)
bh@(BHeader BHBody c
bhb SignedKES (KES c) (BHBody c)
_)
               )
           ) -> do
        let vk :: VKey 'BlockIssuer
vk = BHBody c -> VKey 'BlockIssuer
forall c. BHBody c -> VKey 'BlockIssuer
bheaderVk BHBody c
bhb
            vkh :: KeyHash 'BlockIssuer
vkh = VKey 'BlockIssuer -> KeyHash 'BlockIssuer
forall (kd :: KeyRole). VKey kd -> KeyHash kd
hashKey VKey 'BlockIssuer
vk
            slot :: SlotNo
slot = BHBody c -> SlotNo
forall c. BHBody c -> SlotNo
bheaderSlotNo BHBody c
bhb
            gkeys :: Set (KeyHash 'Genesis)
gkeys = Map (KeyHash 'Genesis) GenDelegPair -> Set (KeyHash 'Genesis)
forall k a. Map k a -> Set k
Map.keysSet Map (KeyHash 'Genesis) GenDelegPair
genDelegs

        ActiveSlotCoeff
asc <- BaseM (OVERLAY c) ActiveSlotCoeff
-> Rule (OVERLAY c) 'Transition ActiveSlotCoeff
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (OVERLAY c) ActiveSlotCoeff
 -> Rule (OVERLAY c) 'Transition ActiveSlotCoeff)
-> BaseM (OVERLAY c) ActiveSlotCoeff
-> Rule (OVERLAY c) 'Transition ActiveSlotCoeff
forall a b. (a -> b) -> a -> b
$ (Globals -> ActiveSlotCoeff)
-> ReaderT Globals Identity ActiveSlotCoeff
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> ActiveSlotCoeff
activeSlotCoeff
        SlotNo
firstSlotNo <- BaseM (OVERLAY c) SlotNo -> Rule (OVERLAY c) 'Transition SlotNo
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (OVERLAY c) SlotNo -> Rule (OVERLAY c) 'Transition SlotNo)
-> BaseM (OVERLAY c) SlotNo -> Rule (OVERLAY c) 'Transition SlotNo
forall a b. (a -> b) -> a -> b
$ do
          EpochInfo Identity
ei <- (Globals -> EpochInfo Identity)
-> ReaderT Globals Identity (EpochInfo Identity)
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> EpochInfo Identity
epochInfoPure
          SlotNo -> ReaderT Globals Identity SlotNo
forall a. a -> ReaderT Globals Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SlotNo -> ReaderT Globals Identity SlotNo)
-> SlotNo -> ReaderT Globals Identity SlotNo
forall a b. (a -> b) -> a -> b
$ HasCallStack => EpochInfo Identity -> EpochNo -> SlotNo
EpochInfo Identity -> EpochNo -> SlotNo
epochInfoFirst EpochInfo Identity
ei (EpochNo -> SlotNo) -> EpochNo -> SlotNo
forall a b. (a -> b) -> a -> b
$ HasCallStack => EpochInfo Identity -> SlotNo -> EpochNo
EpochInfo Identity -> SlotNo -> EpochNo
epochInfoEpoch EpochInfo Identity
ei SlotNo
slot

        case SlotNo
-> Set (KeyHash 'Genesis)
-> UnitInterval
-> ActiveSlotCoeff
-> SlotNo
-> Maybe OBftSlot
lookupInOverlaySchedule SlotNo
firstSlotNo Set (KeyHash 'Genesis)
gkeys UnitInterval
dval ActiveSlotCoeff
asc SlotNo
slot :: Maybe OBftSlot of
          Maybe OBftSlot
Nothing ->
            Nonce
-> PoolDistr
-> ActiveSlotCoeff
-> BHBody c
-> Either (PredicateFailure (OVERLAY c)) ()
forall c.
(Crypto c, Signable (VRF c) Seed) =>
Nonce
-> PoolDistr
-> ActiveSlotCoeff
-> BHBody c
-> Either (PredicateFailure (OVERLAY c)) ()
praosVrfChecks Nonce
eta0 PoolDistr
pd ActiveSlotCoeff
asc BHBody c
bhb Either (OverlayPredicateFailure c) ()
-> (OverlayPredicateFailure c -> PredicateFailure (OVERLAY c))
-> F (Clause (OVERLAY c) 'Transition) ()
forall e sts (ctx :: RuleType).
Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
?!: OverlayPredicateFailure c -> PredicateFailure (OVERLAY c)
OverlayPredicateFailure c -> OverlayPredicateFailure c
forall a. a -> a
id
          Just OBftSlot
NonActiveSlot ->
            PredicateFailure (OVERLAY c)
-> F (Clause (OVERLAY c) 'Transition) ()
forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause (PredicateFailure (OVERLAY c)
 -> F (Clause (OVERLAY c) 'Transition) ())
-> PredicateFailure (OVERLAY c)
-> F (Clause (OVERLAY c) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ SlotNo -> OverlayPredicateFailure c
forall c. SlotNo -> OverlayPredicateFailure c
NotActiveSlotOVERLAY (BHBody c -> SlotNo
forall c. BHBody c -> SlotNo
bheaderSlotNo BHBody c
bhb)
          Just (ActiveSlot KeyHash 'Genesis
gkey) ->
            case KeyHash 'Genesis
-> Map (KeyHash 'Genesis) GenDelegPair -> Maybe GenDelegPair
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KeyHash 'Genesis
gkey Map (KeyHash 'Genesis) GenDelegPair
genDelegs of
              Maybe GenDelegPair
Nothing ->
                PredicateFailure (OVERLAY c)
-> F (Clause (OVERLAY c) 'Transition) ()
forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause (PredicateFailure (OVERLAY c)
 -> F (Clause (OVERLAY c) 'Transition) ())
-> PredicateFailure (OVERLAY c)
-> F (Clause (OVERLAY c) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ KeyHash 'Genesis -> OverlayPredicateFailure c
forall c. KeyHash 'Genesis -> OverlayPredicateFailure c
UnknownGenesisKeyOVERLAY KeyHash 'Genesis
gkey
              Just (GenDelegPair KeyHash 'GenesisDelegate
genDelegsKey VRFVerKeyHash 'GenDelegVRF
genesisVrfKH) -> do
                KeyHash 'BlockIssuer
vkh KeyHash 'BlockIssuer -> KeyHash 'BlockIssuer -> Bool
forall a. Eq a => a -> a -> Bool
== KeyHash 'GenesisDelegate -> KeyHash 'BlockIssuer
forall (r :: KeyRole) (r' :: KeyRole). KeyHash r -> KeyHash r'
forall (a :: KeyRole -> *) (r :: KeyRole) (r' :: KeyRole).
HasKeyRole a =>
a r -> a r'
coerceKeyRole KeyHash 'GenesisDelegate
genDelegsKey Bool
-> PredicateFailure (OVERLAY c)
-> F (Clause (OVERLAY c) 'Transition) ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! KeyHash 'BlockIssuer
-> KeyHash 'GenesisDelegate -> OverlayPredicateFailure c
forall c.
KeyHash 'BlockIssuer
-> KeyHash 'GenesisDelegate -> OverlayPredicateFailure c
WrongGenesisColdKeyOVERLAY KeyHash 'BlockIssuer
vkh KeyHash 'GenesisDelegate
genDelegsKey
                VRFVerKeyHash 'GenDelegVRF
-> Nonce -> BHBody c -> Either (PredicateFailure (OVERLAY c)) ()
forall c.
(Crypto c, Signable (VRF c) Seed) =>
VRFVerKeyHash 'GenDelegVRF
-> Nonce -> BHBody c -> Either (PredicateFailure (OVERLAY c)) ()
pbftVrfChecks VRFVerKeyHash 'GenDelegVRF
genesisVrfKH Nonce
eta0 BHBody c
bhb Either (OverlayPredicateFailure c) ()
-> (OverlayPredicateFailure c -> PredicateFailure (OVERLAY c))
-> F (Clause (OVERLAY c) 'Transition) ()
forall e sts (ctx :: RuleType).
Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
?!: OverlayPredicateFailure c -> PredicateFailure (OVERLAY c)
OverlayPredicateFailure c -> OverlayPredicateFailure c
forall a. a -> a
id

        let oce :: OCertEnv
oce =
              OCertEnv
                { ocertEnvStPools :: Set (KeyHash 'StakePool)
ocertEnvStPools = Exp (Sett (KeyHash 'StakePool) ()) -> Set (KeyHash 'StakePool)
forall s t. Embed s t => Exp t -> s
eval (Map (KeyHash 'StakePool) IndividualPoolStake
-> Exp (Sett (KeyHash 'StakePool) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom (Map (KeyHash 'StakePool) IndividualPoolStake
 -> Exp (Sett (KeyHash 'StakePool) ()))
-> Map (KeyHash 'StakePool) IndividualPoolStake
-> Exp (Sett (KeyHash 'StakePool) ())
forall a b. (a -> b) -> a -> b
$ PoolDistr -> Map (KeyHash 'StakePool) IndividualPoolStake
unPoolDistr PoolDistr
pd)
                , ocertEnvGenDelegs :: Set (KeyHash 'GenesisDelegate)
ocertEnvGenDelegs = (GenDelegPair -> KeyHash 'GenesisDelegate)
-> Set GenDelegPair -> Set (KeyHash 'GenesisDelegate)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map GenDelegPair -> KeyHash 'GenesisDelegate
genDelegKeyHash (Set GenDelegPair -> Set (KeyHash 'GenesisDelegate))
-> Set GenDelegPair -> Set (KeyHash 'GenesisDelegate)
forall a b. (a -> b) -> a -> b
$ Map (KeyHash 'Genesis) GenDelegPair -> Set GenDelegPair
forall v k. Ord v => Map k v -> Set v
forall (f :: * -> * -> *) v k. (Basic f, Ord v) => f k v -> Set v
range Map (KeyHash 'Genesis) GenDelegPair
genDelegs
                }

        forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(OCERT c) (RuleContext 'Transition (OCERT c)
 -> Rule (OVERLAY c) 'Transition (State (OCERT c)))
-> RuleContext 'Transition (OCERT c)
-> Rule (OVERLAY c) 'Transition (State (OCERT c))
forall a b. (a -> b) -> a -> b
$ (Environment (OCERT c), State (OCERT c), Signal (OCERT c))
-> TRC (OCERT c)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment (OCERT c)
OCertEnv
oce, State (OCERT c)
State (OVERLAY c)
cs, Signal (OCERT c)
Signal (OVERLAY c)
bh)

instance
  VRF.VRFAlgorithm (VRF c) =>
  NoThunks (OverlayPredicateFailure c)

instance
  ( Crypto c
  , KES.Signable (KES c) (BHBody c)
  , VRF.Signable (VRF c) Seed
  ) =>
  Embed (OCERT c) (OVERLAY c)
  where
  wrapFailed :: PredicateFailure (OCERT c) -> PredicateFailure (OVERLAY c)
wrapFailed = PredicateFailure (OCERT c) -> PredicateFailure (OVERLAY c)
PredicateFailure (OCERT c) -> OverlayPredicateFailure c
forall c. PredicateFailure (OCERT c) -> OverlayPredicateFailure c
OcertFailure

data OBftSlot
  = NonActiveSlot
  | ActiveSlot !(KeyHash 'Genesis)
  deriving (Int -> OBftSlot -> ShowS
[OBftSlot] -> ShowS
OBftSlot -> String
(Int -> OBftSlot -> ShowS)
-> (OBftSlot -> String) -> ([OBftSlot] -> ShowS) -> Show OBftSlot
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> OBftSlot -> ShowS
showsPrec :: Int -> OBftSlot -> ShowS
$cshow :: OBftSlot -> String
show :: OBftSlot -> String
$cshowList :: [OBftSlot] -> ShowS
showList :: [OBftSlot] -> ShowS
Show, OBftSlot -> OBftSlot -> Bool
(OBftSlot -> OBftSlot -> Bool)
-> (OBftSlot -> OBftSlot -> Bool) -> Eq OBftSlot
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: OBftSlot -> OBftSlot -> Bool
== :: OBftSlot -> OBftSlot -> Bool
$c/= :: OBftSlot -> OBftSlot -> Bool
/= :: OBftSlot -> OBftSlot -> Bool
Eq, Eq OBftSlot
Eq OBftSlot =>
(OBftSlot -> OBftSlot -> Ordering)
-> (OBftSlot -> OBftSlot -> Bool)
-> (OBftSlot -> OBftSlot -> Bool)
-> (OBftSlot -> OBftSlot -> Bool)
-> (OBftSlot -> OBftSlot -> Bool)
-> (OBftSlot -> OBftSlot -> OBftSlot)
-> (OBftSlot -> OBftSlot -> OBftSlot)
-> Ord OBftSlot
OBftSlot -> OBftSlot -> Bool
OBftSlot -> OBftSlot -> Ordering
OBftSlot -> OBftSlot -> OBftSlot
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: OBftSlot -> OBftSlot -> Ordering
compare :: OBftSlot -> OBftSlot -> Ordering
$c< :: OBftSlot -> OBftSlot -> Bool
< :: OBftSlot -> OBftSlot -> Bool
$c<= :: OBftSlot -> OBftSlot -> Bool
<= :: OBftSlot -> OBftSlot -> Bool
$c> :: OBftSlot -> OBftSlot -> Bool
> :: OBftSlot -> OBftSlot -> Bool
$c>= :: OBftSlot -> OBftSlot -> Bool
>= :: OBftSlot -> OBftSlot -> Bool
$cmax :: OBftSlot -> OBftSlot -> OBftSlot
max :: OBftSlot -> OBftSlot -> OBftSlot
$cmin :: OBftSlot -> OBftSlot -> OBftSlot
min :: OBftSlot -> OBftSlot -> OBftSlot
Ord, (forall x. OBftSlot -> Rep OBftSlot x)
-> (forall x. Rep OBftSlot x -> OBftSlot) -> Generic OBftSlot
forall x. Rep OBftSlot x -> OBftSlot
forall x. OBftSlot -> Rep OBftSlot x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. OBftSlot -> Rep OBftSlot x
from :: forall x. OBftSlot -> Rep OBftSlot x
$cto :: forall x. Rep OBftSlot x -> OBftSlot
to :: forall x. Rep OBftSlot x -> OBftSlot
Generic)

instance EncCBOR OBftSlot where
  encCBOR :: OBftSlot -> Encoding
encCBOR OBftSlot
NonActiveSlot = Encoding
encodeNull
  encCBOR (ActiveSlot KeyHash 'Genesis
k) = KeyHash 'Genesis -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR KeyHash 'Genesis
k

instance DecCBOR OBftSlot where
  decCBOR :: forall s. Decoder s OBftSlot
decCBOR = do
    Decoder s TokenType
forall s. Decoder s TokenType
peekTokenType Decoder s TokenType
-> (TokenType -> Decoder s OBftSlot) -> Decoder s OBftSlot
forall a b. Decoder s a -> (a -> Decoder s b) -> Decoder s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      TokenType
TypeNull -> do
        Decoder s ()
forall s. Decoder s ()
decodeNull
        OBftSlot -> Decoder s OBftSlot
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure OBftSlot
NonActiveSlot
      TokenType
_ -> KeyHash 'Genesis -> OBftSlot
ActiveSlot (KeyHash 'Genesis -> OBftSlot)
-> Decoder s (KeyHash 'Genesis) -> Decoder s OBftSlot
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Decoder s (KeyHash 'Genesis)
forall s. Decoder s (KeyHash 'Genesis)
forall a s. DecCBOR a => Decoder s a
decCBOR

instance NoThunks OBftSlot

instance NFData OBftSlot

classifyOverlaySlot ::
  SlotNo -> -- first slot of the epoch
  Set (KeyHash 'Genesis) -> -- genesis Nodes
  UnitInterval -> -- decentralization parameter
  ActiveSlotCoeff -> -- active slot coefficent
  SlotNo -> -- overlay slot to classify
  OBftSlot
classifyOverlaySlot :: SlotNo
-> Set (KeyHash 'Genesis)
-> UnitInterval
-> ActiveSlotCoeff
-> SlotNo
-> OBftSlot
classifyOverlaySlot SlotNo
firstSlotNo Set (KeyHash 'Genesis)
gkeys UnitInterval
dval ActiveSlotCoeff
ascValue SlotNo
slot =
  if Bool
isActive
    then
      let genesisIdx :: Int
genesisIdx = (Int
position Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
ascInv) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Set (KeyHash 'Genesis) -> Int
forall a. Set a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Set (KeyHash 'Genesis)
gkeys)
       in Set (KeyHash 'Genesis)
gkeys Set (KeyHash 'Genesis) -> Int -> OBftSlot
`getAtIndex` Int
genesisIdx
    else OBftSlot
NonActiveSlot
  where
    d :: Rational
d = UnitInterval -> Rational
forall r. BoundedRational r => r -> Rational
unboundRational UnitInterval
dval
    position :: Int
position = Rational -> Int
forall b. Integral b => Rational -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling (Duration -> Rational
forall a b. (Integral a, Num b) => a -> b
fromIntegral (SlotNo
slot SlotNo -> SlotNo -> Duration
-* SlotNo
firstSlotNo) Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Rational
d)
    isActive :: Bool
isActive = Int
position Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
ascInv Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
    getAtIndex :: Set (KeyHash 'Genesis) -> Int -> OBftSlot
getAtIndex Set (KeyHash 'Genesis)
gs Int
i = if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Set (KeyHash 'Genesis) -> Int
forall a. Set a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Set (KeyHash 'Genesis)
gs then KeyHash 'Genesis -> OBftSlot
ActiveSlot (Int -> Set (KeyHash 'Genesis) -> KeyHash 'Genesis
forall a. Int -> Set a -> a
Set.elemAt Int
i Set (KeyHash 'Genesis)
gs) else OBftSlot
NonActiveSlot
    ascInv :: Int
ascInv = Rational -> Int
forall b. Integral b => Rational -> b
forall a b. (RealFrac a, Integral b) => a -> b
floor (Rational
1 Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ PositiveUnitInterval -> Rational
forall r. BoundedRational r => r -> Rational
unboundRational (ActiveSlotCoeff -> PositiveUnitInterval
activeSlotVal ActiveSlotCoeff
ascValue))

lookupInOverlaySchedule ::
  SlotNo -> -- first slot of the epoch
  Set (KeyHash 'Genesis) -> -- genesis Nodes
  UnitInterval -> -- decentralization parameter
  ActiveSlotCoeff -> -- active slot coefficent
  SlotNo -> -- slot to lookup
  Maybe OBftSlot
lookupInOverlaySchedule :: SlotNo
-> Set (KeyHash 'Genesis)
-> UnitInterval
-> ActiveSlotCoeff
-> SlotNo
-> Maybe OBftSlot
lookupInOverlaySchedule SlotNo
firstSlotNo Set (KeyHash 'Genesis)
gkeys UnitInterval
dval ActiveSlotCoeff
ascValue SlotNo
slot =
  if SlotNo -> UnitInterval -> SlotNo -> Bool
isOverlaySlot SlotNo
firstSlotNo UnitInterval
dval SlotNo
slot
    then OBftSlot -> Maybe OBftSlot
forall a. a -> Maybe a
Just (OBftSlot -> Maybe OBftSlot) -> OBftSlot -> Maybe OBftSlot
forall a b. (a -> b) -> a -> b
$ SlotNo
-> Set (KeyHash 'Genesis)
-> UnitInterval
-> ActiveSlotCoeff
-> SlotNo
-> OBftSlot
classifyOverlaySlot SlotNo
firstSlotNo Set (KeyHash 'Genesis)
gkeys UnitInterval
dval ActiveSlotCoeff
ascValue SlotNo
slot
    else Maybe OBftSlot
forall a. Maybe a
Nothing

-- | Return the list of overlaySlots for a given epoch.
-- Note that this linear in the size of the epoch, and should probably
-- only be used for testing.
-- If something more performant is needed, we could probably use
-- [start + floor(x/d) | x <- [0 .. (spe -1)], floor(x/d) < spe]
-- but we would need to make sure that this is equivalent.
overlaySlots ::
  SlotNo -> -- starting slot
  UnitInterval -> -- decentralization parameter
  EpochSize ->
  [SlotNo]
overlaySlots :: SlotNo -> UnitInterval -> EpochSize -> [SlotNo]
overlaySlots SlotNo
start UnitInterval
d (EpochSize Word64
spe) =
  [Word64 -> SlotNo
SlotNo Word64
x | Word64
x <- [SlotNo -> Word64
unSlotNo SlotNo
start .. Word64
end], SlotNo -> UnitInterval -> SlotNo -> Bool
isOverlaySlot SlotNo
start UnitInterval
d (Word64 -> SlotNo
SlotNo Word64
x)]
  where
    end :: Word64
end = SlotNo -> Word64
unSlotNo SlotNo
start Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
spe Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
1