{-# 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. 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
$cto :: forall x. Rep OverlayEnv x -> OverlayEnv
$cfrom :: forall x. OverlayEnv -> Rep OverlayEnv x
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 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
$cto :: forall c x.
Rep (OverlayPredicateFailure c) x -> OverlayPredicateFailure c
$cfrom :: forall c x.
OverlayPredicateFailure c -> Rep (OverlayPredicateFailure c) x
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 = [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
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless
    ( 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)
        (coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall c. BHBody c -> CertifiedVRF (VRF c) Nonce
bheaderEta BHBody c
bhb)
    )
    (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall c.
Nonce
-> SlotNo
-> Nonce
-> CertifiedVRF (VRF c) Nonce
-> OverlayPredicateFailure c
VRFKeyBadNonce Nonce
seedEta SlotNo
slot Nonce
eta0 (coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall c. BHBody c -> CertifiedVRF (VRF c) Nonce
bheaderEta BHBody c
bhb))
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless
    ( 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)
        (coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall c. BHBody c -> CertifiedVRF (VRF c) Natural
bheaderL BHBody c
bhb)
    )
    (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall c.
Nonce
-> SlotNo
-> Nonce
-> CertifiedVRF (VRF c) Nonce
-> OverlayPredicateFailure c
VRFKeyBadLeaderValue Nonce
seedL SlotNo
slot Nonce
eta0 (coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall c. BHBody c -> CertifiedVRF (VRF c) Natural
bheaderL BHBody c
bhb))
  where
    vrfK :: VerKeyVRF (VRF c)
vrfK = forall c. BHBody c -> VerKeyVRF (VRF c)
bheaderVrfVk BHBody c
bhb
    slot :: SlotNo
slot = 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' = 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 -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall c. KeyHash 'StakePool -> OverlayPredicateFailure c
VRFKeyUnknown KeyHash 'StakePool
hk
    Just (IndividualPoolStake Rational
sigma CompactForm Coin
_ VRFVerKeyHash 'StakePoolVRF
stakePoolVRFVerKeyHash) -> do
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless
        (forall (r :: KeyRoleVRF). VRFVerKeyHash r -> Hash HASH KeyRoleVRF
unVRFVerKeyHash VRFVerKeyHash 'StakePoolVRF
stakePoolVRFVerKeyHash forall a. Eq a => a -> a -> Bool
== forall (r :: KeyRoleVRF). VRFVerKeyHash r -> Hash HASH KeyRoleVRF
unVRFVerKeyHash VRFVerKeyHash 'BlockIssuerVRF
blockIssuerVRFVerKeyHash)
        (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall c.
KeyHash 'StakePool
-> VRFVerKeyHash 'StakePoolVRF
-> VRFVerKeyHash 'BlockIssuerVRF
-> OverlayPredicateFailure c
VRFKeyWrongVRFKey KeyHash 'StakePool
hk VRFVerKeyHash 'StakePoolVRF
stakePoolVRFVerKeyHash VRFVerKeyHash 'BlockIssuerVRF
blockIssuerVRFVerKeyHash)
      forall c.
(Crypto c, Signable (VRF c) Seed) =>
Nonce -> BHBody c -> Either (PredicateFailure (OVERLAY c)) ()
vrfChecks Nonce
eta0 BHBody c
bhb
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless
        (forall v.
VRFAlgorithm v =>
OutputVRF v -> Rational -> ActiveSlotCoeff -> Bool
checkLeaderValue (forall v a. CertifiedVRF v a -> OutputVRF v
VRF.certifiedOutput forall a b. (a -> b) -> a -> b
$ forall c. BHBody c -> CertifiedVRF (VRF c) Natural
bheaderL BHBody c
bhb) Rational
sigma ActiveSlotCoeff
f)
        (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall c.
OutputVRF (VRF c)
-> Rational -> ActiveSlotCoeff -> OverlayPredicateFailure c
VRFLeaderValueTooBig (forall v a. CertifiedVRF v a -> OutputVRF v
VRF.certifiedOutput forall a b. (a -> b) -> a -> b
$ forall c. BHBody c -> CertifiedVRF (VRF c) Natural
bheaderL BHBody c
bhb) Rational
sigma ActiveSlotCoeff
f)
  where
    hk :: KeyHash 'StakePool
hk = forall (a :: KeyRole -> *) (r :: KeyRole) (r' :: KeyRole).
HasKeyRole a =>
a r -> a r'
coerceKeyRole forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c. BHBody c -> KeyHash 'BlockIssuer
issuerIDfromBHBody 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 (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
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless
    (forall (r :: KeyRoleVRF). VRFVerKeyHash r -> Hash HASH KeyRoleVRF
unVRFVerKeyHash VRFVerKeyHash 'GenDelegVRF
genDelegVRFVerKeyHash forall a. Eq a => a -> a -> Bool
== forall (r :: KeyRoleVRF). VRFVerKeyHash r -> Hash HASH KeyRoleVRF
unVRFVerKeyHash VRFVerKeyHash 'BlockIssuerVRF
blockIssuerVRFVerKeyHash)
    (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall c.
KeyHash 'BlockIssuer
-> VRFVerKeyHash 'GenDelegVRF
-> VRFVerKeyHash 'BlockIssuerVRF
-> OverlayPredicateFailure c
WrongGenesisVRFKeyOVERLAY KeyHash 'BlockIssuer
hk VRFVerKeyHash 'GenDelegVRF
genDelegVRFVerKeyHash VRFVerKeyHash 'BlockIssuerVRF
blockIssuerVRFVerKeyHash)
  forall c.
(Crypto c, Signable (VRF c) Seed) =>
Nonce -> BHBody c -> Either (PredicateFailure (OVERLAY c)) ()
vrfChecks Nonce
eta0 BHBody c
bhb
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  where
    hk :: KeyHash 'BlockIssuer
hk = 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 (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 =
  forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
    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 = forall c. BHBody c -> VKey 'BlockIssuer
bheaderVk BHBody c
bhb
            vkh :: KeyHash 'BlockIssuer
vkh = forall (kd :: KeyRole). VKey kd -> KeyHash kd
hashKey VKey 'BlockIssuer
vk
            slot :: SlotNo
slot = forall c. BHBody c -> SlotNo
bheaderSlotNo BHBody c
bhb
            gkeys :: Set (KeyHash 'Genesis)
gkeys = forall k a. Map k a -> Set k
Map.keysSet Map (KeyHash 'Genesis) GenDelegPair
genDelegs

        ActiveSlotCoeff
asc <- forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> ActiveSlotCoeff
activeSlotCoeff
        SlotNo
firstSlotNo <- forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS forall a b. (a -> b) -> a -> b
$ do
          EpochInfo Identity
ei <- forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> EpochInfo Identity
epochInfoPure
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ HasCallStack => EpochInfo Identity -> EpochNo -> SlotNo
epochInfoFirst EpochInfo Identity
ei forall a b. (a -> b) -> a -> b
$ HasCallStack => 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 ->
            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 forall e sts (ctx :: RuleType).
Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
?!: forall a. a -> a
id
          Just OBftSlot
NonActiveSlot ->
            forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause forall a b. (a -> b) -> a -> b
$ forall c. SlotNo -> OverlayPredicateFailure c
NotActiveSlotOVERLAY (forall c. BHBody c -> SlotNo
bheaderSlotNo BHBody c
bhb)
          Just (ActiveSlot KeyHash 'Genesis
gkey) ->
            case 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 ->
                forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause forall a b. (a -> b) -> a -> b
$ forall c. KeyHash 'Genesis -> OverlayPredicateFailure c
UnknownGenesisKeyOVERLAY KeyHash 'Genesis
gkey
              Just (GenDelegPair KeyHash 'GenesisDelegate
genDelegsKey VRFVerKeyHash 'GenDelegVRF
genesisVrfKH) -> do
                KeyHash 'BlockIssuer
vkh forall a. Eq a => a -> a -> Bool
== forall (a :: KeyRole -> *) (r :: KeyRole) (r' :: KeyRole).
HasKeyRole a =>
a r -> a r'
coerceKeyRole KeyHash 'GenesisDelegate
genDelegsKey forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall c.
KeyHash 'BlockIssuer
-> KeyHash 'GenesisDelegate -> OverlayPredicateFailure c
WrongGenesisColdKeyOVERLAY KeyHash 'BlockIssuer
vkh KeyHash 'GenesisDelegate
genDelegsKey
                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 forall e sts (ctx :: RuleType).
Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
?!: forall a. a -> a
id

        let oce :: OCertEnv
oce =
              OCertEnv
                { ocertEnvStPools :: Set (KeyHash 'StakePool)
ocertEnvStPools = forall s t. Embed s t => Exp t -> s
eval (forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom forall a b. (a -> b) -> a -> b
$ PoolDistr -> Map (KeyHash 'StakePool) IndividualPoolStake
unPoolDistr PoolDistr
pd)
                , ocertEnvGenDelegs :: Set (KeyHash 'GenesisDelegate)
ocertEnvGenDelegs = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map GenDelegPair -> KeyHash 'GenesisDelegate
genDelegKeyHash forall a b. (a -> b) -> a -> b
$ 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) forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (OCertEnv
oce, State (OVERLAY c)
cs, 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 = forall c. PredicateFailure (OCERT c) -> OverlayPredicateFailure c
OcertFailure

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

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

instance DecCBOR OBftSlot where
  decCBOR :: forall s. Decoder s OBftSlot
decCBOR = do
    forall s. Decoder s TokenType
peekTokenType forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      TokenType
TypeNull -> do
        forall s. Decoder s ()
decodeNull
        forall (f :: * -> *) a. Applicative f => a -> f a
pure OBftSlot
NonActiveSlot
      TokenType
_ -> KeyHash 'Genesis -> OBftSlot
ActiveSlot forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall a. Integral a => a -> a -> a
`div` Int
ascInv) forall a. Integral a => a -> a -> a
`mod` forall a b. (Integral a, Num b) => a -> b
fromIntegral (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 = forall r. BoundedRational r => r -> Rational
unboundRational UnitInterval
dval
    position :: Int
position = forall a b. (RealFrac a, Integral b) => a -> b
ceiling (forall a b. (Integral a, Num b) => a -> b
fromIntegral (SlotNo
slot SlotNo -> SlotNo -> Duration
-* SlotNo
firstSlotNo) forall a. Num a => a -> a -> a
* Rational
d)
    isActive :: Bool
isActive = Int
position forall a. Integral a => a -> a -> a
`mod` Int
ascInv 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 forall a. Ord a => a -> a -> Bool
< forall (t :: * -> *) a. Foldable t => t a -> Int
length Set (KeyHash 'Genesis)
gs then KeyHash 'Genesis -> OBftSlot
ActiveSlot (forall a. Int -> Set a -> a
Set.elemAt Int
i Set (KeyHash 'Genesis)
gs) else OBftSlot
NonActiveSlot
    ascInv :: Int
ascInv = forall a b. (RealFrac a, Integral b) => a -> b
floor (Rational
1 forall a. Fractional a => a -> a -> a
/ 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 forall a. a -> Maybe a
Just 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 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 forall a. Num a => a -> a -> a
+ Word64
spe forall a. Num a => a -> a -> a
- Word64
1