{-# 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.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.Crypto
import Cardano.Ledger.Keys (
  DSignable,
  GenDelegPair (..),
  GenDelegs (..),
  KESignable,
  KeyHash (..),
  KeyRole (..),
  KeyRoleVRF (..),
  VRFVerKeyHash (..),
  coerceKeyRole,
  hashKey,
  hashVerKeyVRF,
 )
import Cardano.Ledger.PoolDistr (
  IndividualPoolStake (..),
  PoolDistr (..),
 )
import Cardano.Ledger.Slot (epochInfoEpoch, epochInfoFirst, (-*))
import Cardano.Protocol.TPraos.BHeader (
  BHBody (..),
  BHeader (BHeader),
  checkLeaderValue,
  issuerIDfromBHBody,
  mkSeed,
  seedEta,
  seedL,
 )
import Cardano.Protocol.TPraos.OCert (OCertSignable)
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 c
  = OverlayEnv
      UnitInterval -- the decentralization paramater @d@ from the protocal parameters
      (PoolDistr c)
      (GenDelegs c)
      Nonce
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c x. Rep (OverlayEnv c) x -> OverlayEnv c
forall c x. OverlayEnv c -> Rep (OverlayEnv c) x
$cto :: forall c x. Rep (OverlayEnv c) x -> OverlayEnv c
$cfrom :: forall c x. OverlayEnv c -> Rep (OverlayEnv c) x
Generic)

instance NoThunks (OverlayEnv c)

data OverlayPredicateFailure c
  = VRFKeyUnknown
      !(KeyHash 'StakePool c) -- unknown VRF keyhash (not registered)
  | VRFKeyWrongVRFKey
      !(KeyHash 'StakePool c) -- KeyHash of block issuer
      !(VRFVerKeyHash 'StakePoolVRF c) -- VRF KeyHash registered with stake pool
      !(VRFVerKeyHash 'BlockIssuerVRF c) -- 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 c) -- KeyHash of block issuer
      !(KeyHash 'GenesisDelegate c) -- KeyHash genesis delegate keyhash assigned to this slot
  | WrongGenesisVRFKeyOVERLAY
      !(KeyHash 'BlockIssuer c) -- KeyHash of block issuer
      !(VRFVerKeyHash 'GenDelegVRF c) -- VRF KeyHash registered with genesis delegation
      !(VRFVerKeyHash 'BlockIssuerVRF c) -- VRF KeyHash from Header
  | UnknownGenesisKeyOVERLAY
      !(KeyHash 'Genesis c) -- 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
  , DSignable c (OCertSignable c)
  , KESignable c (BHBody c)
  , VRF.Signable (VRF c) Seed
  ) =>
  STS (OVERLAY c)
  where
  type
    State (OVERLAY c) =
      Map (KeyHash 'BlockIssuer c) Word64

  type
    Signal (OVERLAY c) =
      BHeader c

  type Environment (OVERLAY c) = OverlayEnv c
  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, DSignable c (OCertSignable c), KESignable 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 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 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 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 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 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 c Natural
bheaderL BHBody c
bhb))
  where
    vrfK :: VerKeyVRF c
vrfK = forall c. BHBody c -> VerKeyVRF 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 c ->
  ActiveSlotCoeff ->
  BHBody c ->
  Either (PredicateFailure (OVERLAY c)) ()
praosVrfChecks :: forall c.
(Crypto c, Signable (VRF c) Seed) =>
Nonce
-> PoolDistr c
-> ActiveSlotCoeff
-> BHBody c
-> Either (PredicateFailure (OVERLAY c)) ()
praosVrfChecks Nonce
eta0 (PoolDistr Map (KeyHash 'StakePool c) (IndividualPoolStake c)
pd CompactForm Coin
_tot) ActiveSlotCoeff
f BHBody c
bhb = do
  let sigma' :: Maybe (IndividualPoolStake c)
sigma' = forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KeyHash 'StakePool c
hk Map (KeyHash 'StakePool c) (IndividualPoolStake c)
pd
  case Maybe (IndividualPoolStake c)
sigma' of
    Maybe (IndividualPoolStake c)
Nothing -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall c. KeyHash 'StakePool c -> OverlayPredicateFailure c
VRFKeyUnknown KeyHash 'StakePool c
hk
    Just (IndividualPoolStake Rational
sigma CompactForm Coin
_ VRFVerKeyHash 'StakePoolVRF c
stakePoolVRFVerKeyHash) -> do
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless
        (forall (r :: KeyRoleVRF) c.
VRFVerKeyHash r c -> Hash (HASH c) KeyRoleVRF
unVRFVerKeyHash VRFVerKeyHash 'StakePoolVRF c
stakePoolVRFVerKeyHash forall a. Eq a => a -> a -> Bool
== forall (r :: KeyRoleVRF) c.
VRFVerKeyHash r c -> Hash (HASH c) KeyRoleVRF
unVRFVerKeyHash VRFVerKeyHash 'BlockIssuerVRF c
blockIssuerVRFVerKeyHash)
        (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall c.
KeyHash 'StakePool c
-> VRFVerKeyHash 'StakePoolVRF c
-> VRFVerKeyHash 'BlockIssuerVRF c
-> OverlayPredicateFailure c
VRFKeyWrongVRFKey KeyHash 'StakePool c
hk VRFVerKeyHash 'StakePoolVRF c
stakePoolVRFVerKeyHash VRFVerKeyHash 'BlockIssuerVRF c
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 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 c Natural
bheaderL BHBody c
bhb) Rational
sigma ActiveSlotCoeff
f)
  where
    hk :: KeyHash 'StakePool c
hk = forall (a :: KeyRole -> * -> *) (r :: KeyRole) c (r' :: KeyRole).
HasKeyRole a =>
a r c -> a r' c
coerceKeyRole forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c. Crypto c => BHBody c -> KeyHash 'BlockIssuer c
issuerIDfromBHBody forall a b. (a -> b) -> a -> b
$ BHBody c
bhb
    blockIssuerVRFVerKeyHash :: VRFVerKeyHash 'BlockIssuerVRF c
blockIssuerVRFVerKeyHash = forall c (r :: KeyRoleVRF).
Crypto c =>
VerKeyVRF c -> VRFVerKeyHash r c
hashVerKeyVRF (forall c. BHBody c -> VerKeyVRF c
bheaderVrfVk BHBody c
bhb)

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

overlayTransition ::
  forall c.
  ( Crypto c
  , DSignable c (OCertSignable c)
  , KESignable c (BHBody c)
  , VRF.Signable (VRF c) Seed
  ) =>
  TransitionRule (OVERLAY c)
overlayTransition :: forall c.
(Crypto c, DSignable c (OCertSignable c), KESignable 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 c
pd (GenDelegs Map (KeyHash 'Genesis c) (GenDelegPair c)
genDelegs) Nonce
eta0
              , State (OVERLAY c)
cs
              , bh :: Signal (OVERLAY c)
bh@(BHeader BHBody c
bhb SignedKES c (BHBody c)
_)
              )
          ) -> do
        let vk :: VKey 'BlockIssuer c
vk = forall c. BHBody c -> VKey 'BlockIssuer c
bheaderVk BHBody c
bhb
            vkh :: KeyHash 'BlockIssuer c
vkh = forall c (kd :: KeyRole). Crypto c => VKey kd c -> KeyHash kd c
hashKey VKey 'BlockIssuer c
vk
            slot :: SlotNo
slot = forall c. BHBody c -> SlotNo
bheaderSlotNo BHBody c
bhb
            gkeys :: Set (KeyHash 'Genesis c)
gkeys = forall k a. Map k a -> Set k
Map.keysSet Map (KeyHash 'Genesis c) (GenDelegPair c)
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
          EpochNo
e <- HasCallStack => EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
epochInfoEpoch EpochInfo Identity
ei SlotNo
slot
          HasCallStack => EpochInfo Identity -> EpochNo -> ShelleyBase SlotNo
epochInfoFirst EpochInfo Identity
ei EpochNo
e

        case (forall c.
SlotNo
-> Set (KeyHash 'Genesis c)
-> UnitInterval
-> ActiveSlotCoeff
-> SlotNo
-> Maybe (OBftSlot c)
lookupInOverlaySchedule SlotNo
firstSlotNo Set (KeyHash 'Genesis c)
gkeys UnitInterval
dval ActiveSlotCoeff
asc SlotNo
slot :: Maybe (OBftSlot c)) of
          Maybe (OBftSlot c)
Nothing ->
            forall c.
(Crypto c, Signable (VRF c) Seed) =>
Nonce
-> PoolDistr c
-> ActiveSlotCoeff
-> BHBody c
-> Either (PredicateFailure (OVERLAY c)) ()
praosVrfChecks Nonce
eta0 PoolDistr c
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 c
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 c
gkey) ->
            case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KeyHash 'Genesis c
gkey Map (KeyHash 'Genesis c) (GenDelegPair c)
genDelegs of
              Maybe (GenDelegPair c)
Nothing ->
                forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause forall a b. (a -> b) -> a -> b
$ forall c. KeyHash 'Genesis c -> OverlayPredicateFailure c
UnknownGenesisKeyOVERLAY KeyHash 'Genesis c
gkey
              Just (GenDelegPair KeyHash 'GenesisDelegate c
genDelegsKey VRFVerKeyHash 'GenDelegVRF c
genesisVrfKH) -> do
                KeyHash 'BlockIssuer c
vkh forall a. Eq a => a -> a -> Bool
== forall (a :: KeyRole -> * -> *) (r :: KeyRole) c (r' :: KeyRole).
HasKeyRole a =>
a r c -> a r' c
coerceKeyRole KeyHash 'GenesisDelegate c
genDelegsKey forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall c.
KeyHash 'BlockIssuer c
-> KeyHash 'GenesisDelegate c -> OverlayPredicateFailure c
WrongGenesisColdKeyOVERLAY KeyHash 'BlockIssuer c
vkh KeyHash 'GenesisDelegate c
genDelegsKey
                forall c.
(Crypto c, Signable (VRF c) Seed) =>
VRFVerKeyHash 'GenDelegVRF c
-> Nonce -> BHBody c -> Either (PredicateFailure (OVERLAY c)) ()
pbftVrfChecks VRFVerKeyHash 'GenDelegVRF c
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 c
oce =
              OCertEnv
                { ocertEnvStPools :: Set (KeyHash 'StakePool c)
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
$ forall c.
PoolDistr c -> Map (KeyHash 'StakePool c) (IndividualPoolStake c)
unPoolDistr PoolDistr c
pd)
                , ocertEnvGenDelegs :: Set (KeyHash 'GenesisDelegate c)
ocertEnvGenDelegs = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map forall c. GenDelegPair c -> KeyHash 'GenesisDelegate c
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 c) (GenDelegPair c)
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 c
oce, State (OVERLAY c)
cs, Signal (OVERLAY c)
bh)

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

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

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

instance
  Crypto c =>
  DecCBOR (OBftSlot c)
  where
  decCBOR :: forall s. Decoder s (OBftSlot c)
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 forall c. OBftSlot c
NonActiveSlot
      TokenType
_ -> forall c. KeyHash 'Genesis c -> OBftSlot c
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 c)

instance NFData (OBftSlot c)

classifyOverlaySlot ::
  SlotNo -> -- first slot of the epoch
  Set (KeyHash 'Genesis c) -> -- genesis Nodes
  UnitInterval -> -- decentralization parameter
  ActiveSlotCoeff -> -- active slot coefficent
  SlotNo -> -- overlay slot to classify
  OBftSlot c
classifyOverlaySlot :: forall c.
SlotNo
-> Set (KeyHash 'Genesis c)
-> UnitInterval
-> ActiveSlotCoeff
-> SlotNo
-> OBftSlot c
classifyOverlaySlot SlotNo
firstSlotNo Set (KeyHash 'Genesis c)
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 c)
gkeys)
       in Set (KeyHash 'Genesis c)
gkeys forall {c}. Set (KeyHash 'Genesis c) -> Int -> OBftSlot c
`getAtIndex` Int
genesisIdx
    else forall c. OBftSlot c
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 c) -> Int -> OBftSlot c
getAtIndex Set (KeyHash 'Genesis c)
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 c)
gs then forall c. KeyHash 'Genesis c -> OBftSlot c
ActiveSlot (forall a. Int -> Set a -> a
Set.elemAt Int
i Set (KeyHash 'Genesis c)
gs) else forall c. OBftSlot c
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 c) -> -- genesis Nodes
  UnitInterval -> -- decentralization parameter
  ActiveSlotCoeff -> -- active slot coefficent
  SlotNo -> -- slot to lookup
  Maybe (OBftSlot c)
lookupInOverlaySchedule :: forall c.
SlotNo
-> Set (KeyHash 'Genesis c)
-> UnitInterval
-> ActiveSlotCoeff
-> SlotNo
-> Maybe (OBftSlot c)
lookupInOverlaySchedule SlotNo
firstSlotNo Set (KeyHash 'Genesis c)
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
$ forall c.
SlotNo
-> Set (KeyHash 'Genesis c)
-> UnitInterval
-> ActiveSlotCoeff
-> SlotNo
-> OBftSlot c
classifyOverlaySlot SlotNo
firstSlotNo Set (KeyHash 'Genesis c)
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