{-# 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 GenesisRole) -- 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 GenesisRole) 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 GenesisRole)
gkeys = Map (KeyHash GenesisRole) GenDelegPair -> Set (KeyHash GenesisRole)
forall k a. Map k a -> Set k
Map.keysSet Map (KeyHash GenesisRole) GenDelegPair
genDelegs

        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
        firstSlotNo <- liftSTS $ do
          ei <- asks epochInfoPure
          pure $ epochInfoFirst ei $ epochInfoEpoch ei slot

        case lookupInOverlaySchedule firstSlotNo gkeys dval asc 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 GenesisRole
gkey) ->
            case KeyHash GenesisRole
-> Map (KeyHash GenesisRole) GenDelegPair -> Maybe GenDelegPair
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KeyHash GenesisRole
gkey Map (KeyHash GenesisRole) 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 GenesisRole -> OverlayPredicateFailure c
forall c. KeyHash GenesisRole -> OverlayPredicateFailure c
UnknownGenesisKeyOVERLAY KeyHash GenesisRole
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
                { 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 GenesisRole) 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 GenesisRole) GenDelegPair
genDelegs
                }

        trans @(OCERT c) $ TRC (oce, cs, 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 GenesisRole)
  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 GenesisRole
k) = KeyHash GenesisRole -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR KeyHash GenesisRole
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 GenesisRole -> OBftSlot
ActiveSlot (KeyHash GenesisRole -> OBftSlot)
-> Decoder s (KeyHash GenesisRole) -> Decoder s OBftSlot
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Decoder s (KeyHash GenesisRole)
forall s. Decoder s (KeyHash GenesisRole)
forall a s. DecCBOR a => Decoder s a
decCBOR

instance NoThunks OBftSlot

instance NFData OBftSlot

classifyOverlaySlot ::
  SlotNo -> -- first slot of the epoch
  Set (KeyHash GenesisRole) -> -- genesis Nodes
  UnitInterval -> -- decentralization parameter
  ActiveSlotCoeff -> -- active slot coefficent
  SlotNo -> -- overlay slot to classify
  OBftSlot
classifyOverlaySlot :: SlotNo
-> Set (KeyHash GenesisRole)
-> UnitInterval
-> ActiveSlotCoeff
-> SlotNo
-> OBftSlot
classifyOverlaySlot SlotNo
firstSlotNo Set (KeyHash GenesisRole)
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 GenesisRole) -> Int
forall a. Set a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Set (KeyHash GenesisRole)
gkeys)
       in Set (KeyHash GenesisRole)
gkeys Set (KeyHash GenesisRole) -> 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 GenesisRole) -> Int -> OBftSlot
getAtIndex Set (KeyHash GenesisRole)
gs Int
i = if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Set (KeyHash GenesisRole) -> Int
forall a. Set a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Set (KeyHash GenesisRole)
gs then KeyHash GenesisRole -> OBftSlot
ActiveSlot (Int -> Set (KeyHash GenesisRole) -> KeyHash GenesisRole
forall a. Int -> Set a -> a
Set.elemAt Int
i Set (KeyHash GenesisRole)
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 GenesisRole) -> -- genesis Nodes
  UnitInterval -> -- decentralization parameter
  ActiveSlotCoeff -> -- active slot coefficent
  SlotNo -> -- slot to lookup
  Maybe OBftSlot
lookupInOverlaySchedule :: SlotNo
-> Set (KeyHash GenesisRole)
-> UnitInterval
-> ActiveSlotCoeff
-> SlotNo
-> Maybe OBftSlot
lookupInOverlaySchedule SlotNo
firstSlotNo Set (KeyHash GenesisRole)
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 GenesisRole)
-> UnitInterval
-> ActiveSlotCoeff
-> SlotNo
-> OBftSlot
classifyOverlaySlot SlotNo
firstSlotNo Set (KeyHash GenesisRole)
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