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

module Shelley.Spec.Ledger.STS.Overlay
  ( OVERLAY,
    PredicateFailure,
    OverlayEnv (..),
    OverlayPredicateFailure (..),
  )
where

import qualified Cardano.Crypto.VRF as VRF
import Cardano.Ledger.Crypto
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 qualified Data.Set as Set
import Data.Word (Word64)
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))
import Shelley.Spec.Ledger.BaseTypes
  ( ActiveSlotCoeff,
    Nonce,
    Seed,
    ShelleyBase,
    UnitInterval,
    activeSlotCoeff,
    epochInfo,
  )
import Shelley.Spec.Ledger.BlockChain
  ( BHBody (..),
    BHeader (..),
    checkLeaderValue,
    issuerIDfromBHBody,
    mkSeed,
    seedEta,
    seedL,
  )
import Shelley.Spec.Ledger.Delegation.Certificates
  ( IndividualPoolStake (..),
    PoolDistr (..),
  )
import Shelley.Spec.Ledger.Keys
  ( DSignable,
    GenDelegPair (..),
    GenDelegs (..),
    Hash,
    KESignable,
    KeyHash,
    KeyRole (..),
    VerKeyVRF,
    coerceKeyRole,
    hashKey,
    hashVerKeyVRF,
  )
import Shelley.Spec.Ledger.OCert (OCertSignable)
import Shelley.Spec.Ledger.OverlaySchedule
  ( OBftSlot (..),
    lookupInOverlaySchedule,
  )
import Shelley.Spec.Ledger.STS.Ocert (OCERT, OCertEnv (..))
import Shelley.Spec.Ledger.Slot (SlotNo, epochInfoEpoch, epochInfoFirst)

data OVERLAY crypto

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

instance NoThunks (OverlayEnv crypto)

data OverlayPredicateFailure crypto
  = VRFKeyUnknown
      !(KeyHash 'StakePool crypto) -- unknown VRF keyhash (not registered)
  | VRFKeyWrongVRFKey
      !(KeyHash 'StakePool crypto) -- KeyHash of block issuer
      !(Hash crypto (VerKeyVRF crypto)) --VRF KeyHash registered with stake pool
      !(Hash crypto (VerKeyVRF crypto)) --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 crypto) 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 crypto) Nonce) -- VRF calculated leader value
  | VRFLeaderValueTooBig
      !(VRF.OutputVRF (VRF crypto)) -- 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 crypto) -- KeyHash of block issuer
      !(KeyHash 'GenesisDelegate crypto) -- KeyHash genesis delegate keyhash assigned to this slot
  | WrongGenesisVRFKeyOVERLAY
      !(KeyHash 'BlockIssuer crypto) -- KeyHash of block issuer
      !(Hash crypto (VerKeyVRF crypto)) --VRF KeyHash registered with genesis delegation
      !(Hash crypto (VerKeyVRF crypto)) --VRF KeyHash from Header
  | UnknownGenesisKeyOVERLAY
      !(KeyHash 'Genesis crypto) -- KeyHash which does not correspond to o genesis node
  | OcertFailure (PredicateFailure (OCERT crypto)) -- Subtransition Failures
  deriving ((forall x.
 OverlayPredicateFailure crypto
 -> Rep (OverlayPredicateFailure crypto) x)
-> (forall x.
    Rep (OverlayPredicateFailure crypto) x
    -> OverlayPredicateFailure crypto)
-> Generic (OverlayPredicateFailure crypto)
forall x.
Rep (OverlayPredicateFailure crypto) x
-> OverlayPredicateFailure crypto
forall x.
OverlayPredicateFailure crypto
-> Rep (OverlayPredicateFailure crypto) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall crypto x.
Rep (OverlayPredicateFailure crypto) x
-> OverlayPredicateFailure crypto
forall crypto x.
OverlayPredicateFailure crypto
-> Rep (OverlayPredicateFailure crypto) x
$cto :: forall crypto x.
Rep (OverlayPredicateFailure crypto) x
-> OverlayPredicateFailure crypto
$cfrom :: forall crypto x.
OverlayPredicateFailure crypto
-> Rep (OverlayPredicateFailure crypto) x
Generic)

instance
  ( Crypto crypto,
    DSignable crypto (OCertSignable crypto),
    KESignable crypto (BHBody crypto),
    VRF.Signable (VRF crypto) Seed
  ) =>
  STS (OVERLAY crypto)
  where
  type
    State (OVERLAY crypto) =
      Map (KeyHash 'BlockIssuer crypto) Word64

  type
    Signal (OVERLAY crypto) =
      BHeader crypto

  type Environment (OVERLAY crypto) = OverlayEnv crypto
  type BaseM (OVERLAY crypto) = ShelleyBase
  type PredicateFailure (OVERLAY crypto) = OverlayPredicateFailure crypto

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

  transitionRules :: [TransitionRule (OVERLAY crypto)]
transitionRules = [TransitionRule (OVERLAY crypto)
forall crypto.
(Crypto crypto, DSignable crypto (OCertSignable crypto),
 KESignable crypto (BHBody crypto), Signable (VRF crypto) Seed) =>
TransitionRule (OVERLAY crypto)
overlayTransition]

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

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

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

praosVrfChecks ::
  forall crypto.
  ( Crypto crypto,
    VRF.Signable (VRF crypto) Seed,
    VRF.ContextVRF (VRF crypto) ~ ()
  ) =>
  Nonce ->
  PoolDistr crypto ->
  ActiveSlotCoeff ->
  BHBody crypto ->
  Either (PredicateFailure (OVERLAY crypto)) ()
praosVrfChecks :: Nonce
-> PoolDistr crypto
-> ActiveSlotCoeff
-> BHBody crypto
-> Either (PredicateFailure (OVERLAY crypto)) ()
praosVrfChecks Nonce
eta0 (PoolDistr Map (KeyHash 'StakePool crypto) (IndividualPoolStake crypto)
pd) ActiveSlotCoeff
f BHBody crypto
bhb = do
  let sigma' :: Maybe (IndividualPoolStake crypto)
sigma' = KeyHash 'StakePool crypto
-> Map (KeyHash 'StakePool crypto) (IndividualPoolStake crypto)
-> Maybe (IndividualPoolStake crypto)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KeyHash 'StakePool crypto
hk Map (KeyHash 'StakePool crypto) (IndividualPoolStake crypto)
pd
  case Maybe (IndividualPoolStake crypto)
sigma' of
    Maybe (IndividualPoolStake crypto)
Nothing -> OverlayPredicateFailure crypto
-> Either (OverlayPredicateFailure crypto) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (OverlayPredicateFailure crypto
 -> Either (OverlayPredicateFailure crypto) ())
-> OverlayPredicateFailure crypto
-> Either (OverlayPredicateFailure crypto) ()
forall a b. (a -> b) -> a -> b
$ KeyHash 'StakePool crypto -> OverlayPredicateFailure crypto
forall crypto.
KeyHash 'StakePool crypto -> OverlayPredicateFailure crypto
VRFKeyUnknown KeyHash 'StakePool crypto
hk
    Just (IndividualPoolStake Rational
sigma Hash crypto (VerKeyVRF crypto)
vrfHK) -> do
      Bool
-> Either (OverlayPredicateFailure crypto) ()
-> Either (OverlayPredicateFailure crypto) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless
        (Hash crypto (VerKeyVRF crypto)
vrfHK Hash crypto (VerKeyVRF crypto)
-> Hash crypto (VerKeyVRF crypto) -> Bool
forall a. Eq a => a -> a -> Bool
== VerKeyVRF crypto -> Hash crypto (VerKeyVRF crypto)
forall v h.
(VRFAlgorithm v, HashAlgorithm h) =>
VerKeyVRF v -> Hash h (VerKeyVRF v)
hashVerKeyVRF VerKeyVRF crypto
vrfK)
        (OverlayPredicateFailure crypto
-> Either (OverlayPredicateFailure crypto) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (OverlayPredicateFailure crypto
 -> Either (OverlayPredicateFailure crypto) ())
-> OverlayPredicateFailure crypto
-> Either (OverlayPredicateFailure crypto) ()
forall a b. (a -> b) -> a -> b
$ KeyHash 'StakePool crypto
-> Hash crypto (VerKeyVRF crypto)
-> Hash crypto (VerKeyVRF crypto)
-> OverlayPredicateFailure crypto
forall crypto.
KeyHash 'StakePool crypto
-> Hash crypto (VerKeyVRF crypto)
-> Hash crypto (VerKeyVRF crypto)
-> OverlayPredicateFailure crypto
VRFKeyWrongVRFKey KeyHash 'StakePool crypto
hk Hash crypto (VerKeyVRF crypto)
vrfHK (VerKeyVRF crypto -> Hash crypto (VerKeyVRF crypto)
forall v h.
(VRFAlgorithm v, HashAlgorithm h) =>
VerKeyVRF v -> Hash h (VerKeyVRF v)
hashVerKeyVRF VerKeyVRF crypto
vrfK))
      Nonce
-> BHBody crypto -> Either (PredicateFailure (OVERLAY crypto)) ()
forall crypto.
(Crypto crypto, Signable (VRF crypto) Seed,
 ContextVRF (VRF crypto) ~ ()) =>
Nonce
-> BHBody crypto -> Either (PredicateFailure (OVERLAY crypto)) ()
vrfChecks Nonce
eta0 BHBody crypto
bhb
      Bool
-> Either (OverlayPredicateFailure crypto) ()
-> Either (OverlayPredicateFailure crypto) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless
        (OutputVRF (VRF crypto) -> Rational -> ActiveSlotCoeff -> Bool
forall v.
VRFAlgorithm v =>
OutputVRF v -> Rational -> ActiveSlotCoeff -> Bool
checkLeaderValue (CertifiedVRF (VRF crypto) Natural -> OutputVRF (VRF crypto)
forall v a. CertifiedVRF v a -> OutputVRF v
VRF.certifiedOutput (CertifiedVRF (VRF crypto) Natural -> OutputVRF (VRF crypto))
-> CertifiedVRF (VRF crypto) Natural -> OutputVRF (VRF crypto)
forall a b. (a -> b) -> a -> b
$ BHBody crypto -> CertifiedVRF (VRF crypto) Natural
forall crypto. BHBody crypto -> CertifiedVRF crypto Natural
bheaderL BHBody crypto
bhb) Rational
sigma ActiveSlotCoeff
f)
        (OverlayPredicateFailure crypto
-> Either (OverlayPredicateFailure crypto) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (OverlayPredicateFailure crypto
 -> Either (OverlayPredicateFailure crypto) ())
-> OverlayPredicateFailure crypto
-> Either (OverlayPredicateFailure crypto) ()
forall a b. (a -> b) -> a -> b
$ OutputVRF (VRF crypto)
-> Rational -> ActiveSlotCoeff -> OverlayPredicateFailure crypto
forall crypto.
OutputVRF (VRF crypto)
-> Rational -> ActiveSlotCoeff -> OverlayPredicateFailure crypto
VRFLeaderValueTooBig (CertifiedVRF (VRF crypto) Natural -> OutputVRF (VRF crypto)
forall v a. CertifiedVRF v a -> OutputVRF v
VRF.certifiedOutput (CertifiedVRF (VRF crypto) Natural -> OutputVRF (VRF crypto))
-> CertifiedVRF (VRF crypto) Natural -> OutputVRF (VRF crypto)
forall a b. (a -> b) -> a -> b
$ BHBody crypto -> CertifiedVRF (VRF crypto) Natural
forall crypto. BHBody crypto -> CertifiedVRF crypto Natural
bheaderL BHBody crypto
bhb) Rational
sigma ActiveSlotCoeff
f)
      () -> Either (OverlayPredicateFailure crypto) ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  where
    hk :: KeyHash 'StakePool crypto
hk = KeyHash 'BlockIssuer crypto -> KeyHash 'StakePool crypto
forall (a :: KeyRole -> * -> *) (r :: KeyRole) crypto
       (r' :: KeyRole).
HasKeyRole a =>
a r crypto -> a r' crypto
coerceKeyRole (KeyHash 'BlockIssuer crypto -> KeyHash 'StakePool crypto)
-> (BHBody crypto -> KeyHash 'BlockIssuer crypto)
-> BHBody crypto
-> KeyHash 'StakePool crypto
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BHBody crypto -> KeyHash 'BlockIssuer crypto
forall crypto.
Crypto crypto =>
BHBody crypto -> KeyHash 'BlockIssuer crypto
issuerIDfromBHBody (BHBody crypto -> KeyHash 'StakePool crypto)
-> BHBody crypto -> KeyHash 'StakePool crypto
forall a b. (a -> b) -> a -> b
$ BHBody crypto
bhb
    vrfK :: VerKeyVRF crypto
vrfK = BHBody crypto -> VerKeyVRF crypto
forall crypto. BHBody crypto -> VerKeyVRF crypto
bheaderVrfVk BHBody crypto
bhb

pbftVrfChecks ::
  forall crypto.
  ( Crypto crypto,
    VRF.Signable (VRF crypto) Seed,
    VRF.ContextVRF (VRF crypto) ~ ()
  ) =>
  Hash crypto (VerKeyVRF crypto) ->
  Nonce ->
  BHBody crypto ->
  Either (PredicateFailure (OVERLAY crypto)) ()
pbftVrfChecks :: Hash crypto (VerKeyVRF crypto)
-> Nonce
-> BHBody crypto
-> Either (PredicateFailure (OVERLAY crypto)) ()
pbftVrfChecks Hash crypto (VerKeyVRF crypto)
vrfHK Nonce
eta0 BHBody crypto
bhb = do
  Bool
-> Either (OverlayPredicateFailure crypto) ()
-> Either (OverlayPredicateFailure crypto) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless
    (Hash crypto (VerKeyVRF crypto)
vrfHK Hash crypto (VerKeyVRF crypto)
-> Hash crypto (VerKeyVRF crypto) -> Bool
forall a. Eq a => a -> a -> Bool
== VerKeyVRF crypto -> Hash crypto (VerKeyVRF crypto)
forall v h.
(VRFAlgorithm v, HashAlgorithm h) =>
VerKeyVRF v -> Hash h (VerKeyVRF v)
hashVerKeyVRF VerKeyVRF crypto
vrfK)
    (OverlayPredicateFailure crypto
-> Either (OverlayPredicateFailure crypto) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (OverlayPredicateFailure crypto
 -> Either (OverlayPredicateFailure crypto) ())
-> OverlayPredicateFailure crypto
-> Either (OverlayPredicateFailure crypto) ()
forall a b. (a -> b) -> a -> b
$ KeyHash 'BlockIssuer crypto
-> Hash crypto (VerKeyVRF crypto)
-> Hash crypto (VerKeyVRF crypto)
-> OverlayPredicateFailure crypto
forall crypto.
KeyHash 'BlockIssuer crypto
-> Hash crypto (VerKeyVRF crypto)
-> Hash crypto (VerKeyVRF crypto)
-> OverlayPredicateFailure crypto
WrongGenesisVRFKeyOVERLAY KeyHash 'BlockIssuer crypto
hk Hash crypto (VerKeyVRF crypto)
vrfHK (VerKeyVRF crypto -> Hash crypto (VerKeyVRF crypto)
forall v h.
(VRFAlgorithm v, HashAlgorithm h) =>
VerKeyVRF v -> Hash h (VerKeyVRF v)
hashVerKeyVRF VerKeyVRF crypto
vrfK))
  Nonce
-> BHBody crypto -> Either (PredicateFailure (OVERLAY crypto)) ()
forall crypto.
(Crypto crypto, Signable (VRF crypto) Seed,
 ContextVRF (VRF crypto) ~ ()) =>
Nonce
-> BHBody crypto -> Either (PredicateFailure (OVERLAY crypto)) ()
vrfChecks Nonce
eta0 BHBody crypto
bhb
  () -> Either (OverlayPredicateFailure crypto) ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  where
    hk :: KeyHash 'BlockIssuer crypto
hk = BHBody crypto -> KeyHash 'BlockIssuer crypto
forall crypto.
Crypto crypto =>
BHBody crypto -> KeyHash 'BlockIssuer crypto
issuerIDfromBHBody BHBody crypto
bhb
    vrfK :: VerKeyVRF crypto
vrfK = BHBody crypto -> VerKeyVRF crypto
forall crypto. BHBody crypto -> VerKeyVRF crypto
bheaderVrfVk BHBody crypto
bhb

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

        ActiveSlotCoeff
asc <- BaseM (OVERLAY crypto) ActiveSlotCoeff
-> Rule (OVERLAY crypto) 'Transition ActiveSlotCoeff
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (OVERLAY crypto) ActiveSlotCoeff
 -> Rule (OVERLAY crypto) 'Transition ActiveSlotCoeff)
-> BaseM (OVERLAY crypto) ActiveSlotCoeff
-> Rule (OVERLAY crypto) '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 crypto) SlotNo
-> Rule (OVERLAY crypto) 'Transition SlotNo
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (OVERLAY crypto) SlotNo
 -> Rule (OVERLAY crypto) 'Transition SlotNo)
-> BaseM (OVERLAY crypto) SlotNo
-> Rule (OVERLAY crypto) '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
epochInfo
          EpochNo
e <- HasCallStack => EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
epochInfoEpoch EpochInfo Identity
ei SlotNo
slot
          HasCallStack => EpochInfo Identity -> EpochNo -> ShelleyBase SlotNo
EpochInfo Identity -> EpochNo -> ShelleyBase SlotNo
epochInfoFirst EpochInfo Identity
ei EpochNo
e

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

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

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

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

instance
  ( Crypto crypto,
    DSignable crypto (OCertSignable crypto),
    KESignable crypto (BHBody crypto),
    VRF.Signable (VRF crypto) Seed
  ) =>
  Embed (OCERT crypto) (OVERLAY crypto)
  where
  wrapFailed :: PredicateFailure (OCERT crypto)
-> PredicateFailure (OVERLAY crypto)
wrapFailed = PredicateFailure (OCERT crypto)
-> PredicateFailure (OVERLAY crypto)
forall crypto.
PredicateFailure (OCERT crypto) -> OverlayPredicateFailure crypto
OcertFailure