{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Cardano.Ledger.Dijkstra.Rules.Pool (
  POOL,
  DijkstraPoolPredFailure (..),
  poolTransition,
) where

import Cardano.Crypto.DSIGN (verifyPossessionProofDSIGN)
import Cardano.Crypto.DSIGN.BLS12381.Internal (minSigPoPDST)
import Cardano.Crypto.Hash.Class (hashSize)
import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Binary (
  DecCBOR (..),
  EncCBOR (..),
  decodeRecordSum,
  encodeListLen,
 )
import Cardano.Ledger.Coin (Coin)
import Cardano.Ledger.Dijkstra.Core
import Cardano.Ledger.Dijkstra.Era (DijkstraEra, POOL)
import Cardano.Ledger.Rules.ValidationMode (checkFailOnJust, checkFailOnJustStatic)
import qualified Cardano.Ledger.Shelley.Rules as Shelley
import Cardano.Ledger.State
import Control.DeepSeq (NFData)
import Control.Monad (forM_, guard)
import Control.Monad.Trans.Reader (asks)
import Control.State.Transition (
  STS (..),
  TRC (..),
  TransitionRule,
  judgmentContext,
  liftSTS,
  tellEvent,
  (?!),
 )
import qualified Data.Map as Map
import Data.Primitive.ByteArray (sizeofByteArray)
import qualified Data.Set as Set
import Data.Word (Word8)
import GHC.Generics (Generic)
import Lens.Micro

data DijkstraPoolPredFailure era
  = StakePoolNotRegisteredOnKeyPOOL
      -- | KeyHash which cannot be retired since it is not registered
      (KeyHash StakePool)
  | StakePoolRetirementWrongEpochPOOL
      (Mismatch RelGT EpochNo)
      (Mismatch RelLTEQ EpochNo)
  | StakePoolCostTooLowPOOL
      (Mismatch RelGTEQ Coin)
  | WrongNetworkPOOL
      (Mismatch RelEQ Network)
      -- | Stake Pool ID
      (KeyHash StakePool)
  | PoolMedataHashTooBig
      -- | Stake Pool ID
      (KeyHash StakePool)
      -- | Size of the metadata hash
      Int
  | VRFKeyHashAlreadyRegistered
      -- | Stake Pool ID
      (KeyHash StakePool)
      -- | VRF key attempted to use, that has already been registered
      (VRFVerKeyHash StakePoolVRF)
  | BlsKeyInvalidProofOfPossession
      -- | Stake Pool ID
      (KeyHash StakePool)
      -- | BLS key set
      BlsKey
  | BlsKeyAlreadyRegistered
      -- | Stake Pool ID
      (KeyHash StakePool)
      -- | BLS key attempted to use, whose public key has already been registered
      BlsKey
  deriving (DijkstraPoolPredFailure era -> DijkstraPoolPredFailure era -> Bool
(DijkstraPoolPredFailure era
 -> DijkstraPoolPredFailure era -> Bool)
-> (DijkstraPoolPredFailure era
    -> DijkstraPoolPredFailure era -> Bool)
-> Eq (DijkstraPoolPredFailure era)
forall era.
DijkstraPoolPredFailure era -> DijkstraPoolPredFailure era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall era.
DijkstraPoolPredFailure era -> DijkstraPoolPredFailure era -> Bool
== :: DijkstraPoolPredFailure era -> DijkstraPoolPredFailure era -> Bool
$c/= :: forall era.
DijkstraPoolPredFailure era -> DijkstraPoolPredFailure era -> Bool
/= :: DijkstraPoolPredFailure era -> DijkstraPoolPredFailure era -> Bool
Eq, Eq (DijkstraPoolPredFailure era)
Eq (DijkstraPoolPredFailure era) =>
(DijkstraPoolPredFailure era
 -> DijkstraPoolPredFailure era -> Ordering)
-> (DijkstraPoolPredFailure era
    -> DijkstraPoolPredFailure era -> Bool)
-> (DijkstraPoolPredFailure era
    -> DijkstraPoolPredFailure era -> Bool)
-> (DijkstraPoolPredFailure era
    -> DijkstraPoolPredFailure era -> Bool)
-> (DijkstraPoolPredFailure era
    -> DijkstraPoolPredFailure era -> Bool)
-> (DijkstraPoolPredFailure era
    -> DijkstraPoolPredFailure era -> DijkstraPoolPredFailure era)
-> (DijkstraPoolPredFailure era
    -> DijkstraPoolPredFailure era -> DijkstraPoolPredFailure era)
-> Ord (DijkstraPoolPredFailure era)
DijkstraPoolPredFailure era -> DijkstraPoolPredFailure era -> Bool
DijkstraPoolPredFailure era
-> DijkstraPoolPredFailure era -> Ordering
DijkstraPoolPredFailure era
-> DijkstraPoolPredFailure era -> DijkstraPoolPredFailure era
forall era. Eq (DijkstraPoolPredFailure era)
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 era.
DijkstraPoolPredFailure era -> DijkstraPoolPredFailure era -> Bool
forall era.
DijkstraPoolPredFailure era
-> DijkstraPoolPredFailure era -> Ordering
forall era.
DijkstraPoolPredFailure era
-> DijkstraPoolPredFailure era -> DijkstraPoolPredFailure era
$ccompare :: forall era.
DijkstraPoolPredFailure era
-> DijkstraPoolPredFailure era -> Ordering
compare :: DijkstraPoolPredFailure era
-> DijkstraPoolPredFailure era -> Ordering
$c< :: forall era.
DijkstraPoolPredFailure era -> DijkstraPoolPredFailure era -> Bool
< :: DijkstraPoolPredFailure era -> DijkstraPoolPredFailure era -> Bool
$c<= :: forall era.
DijkstraPoolPredFailure era -> DijkstraPoolPredFailure era -> Bool
<= :: DijkstraPoolPredFailure era -> DijkstraPoolPredFailure era -> Bool
$c> :: forall era.
DijkstraPoolPredFailure era -> DijkstraPoolPredFailure era -> Bool
> :: DijkstraPoolPredFailure era -> DijkstraPoolPredFailure era -> Bool
$c>= :: forall era.
DijkstraPoolPredFailure era -> DijkstraPoolPredFailure era -> Bool
>= :: DijkstraPoolPredFailure era -> DijkstraPoolPredFailure era -> Bool
$cmax :: forall era.
DijkstraPoolPredFailure era
-> DijkstraPoolPredFailure era -> DijkstraPoolPredFailure era
max :: DijkstraPoolPredFailure era
-> DijkstraPoolPredFailure era -> DijkstraPoolPredFailure era
$cmin :: forall era.
DijkstraPoolPredFailure era
-> DijkstraPoolPredFailure era -> DijkstraPoolPredFailure era
min :: DijkstraPoolPredFailure era
-> DijkstraPoolPredFailure era -> DijkstraPoolPredFailure era
Ord, Int -> DijkstraPoolPredFailure era -> ShowS
[DijkstraPoolPredFailure era] -> ShowS
DijkstraPoolPredFailure era -> String
(Int -> DijkstraPoolPredFailure era -> ShowS)
-> (DijkstraPoolPredFailure era -> String)
-> ([DijkstraPoolPredFailure era] -> ShowS)
-> Show (DijkstraPoolPredFailure era)
forall era. Int -> DijkstraPoolPredFailure era -> ShowS
forall era. [DijkstraPoolPredFailure era] -> ShowS
forall era. DijkstraPoolPredFailure era -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall era. Int -> DijkstraPoolPredFailure era -> ShowS
showsPrec :: Int -> DijkstraPoolPredFailure era -> ShowS
$cshow :: forall era. DijkstraPoolPredFailure era -> String
show :: DijkstraPoolPredFailure era -> String
$cshowList :: forall era. [DijkstraPoolPredFailure era] -> ShowS
showList :: [DijkstraPoolPredFailure era] -> ShowS
Show, (forall x.
 DijkstraPoolPredFailure era -> Rep (DijkstraPoolPredFailure era) x)
-> (forall x.
    Rep (DijkstraPoolPredFailure era) x -> DijkstraPoolPredFailure era)
-> Generic (DijkstraPoolPredFailure era)
forall x.
Rep (DijkstraPoolPredFailure era) x -> DijkstraPoolPredFailure era
forall x.
DijkstraPoolPredFailure era -> Rep (DijkstraPoolPredFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (DijkstraPoolPredFailure era) x -> DijkstraPoolPredFailure era
forall era x.
DijkstraPoolPredFailure era -> Rep (DijkstraPoolPredFailure era) x
$cfrom :: forall era x.
DijkstraPoolPredFailure era -> Rep (DijkstraPoolPredFailure era) x
from :: forall x.
DijkstraPoolPredFailure era -> Rep (DijkstraPoolPredFailure era) x
$cto :: forall era x.
Rep (DijkstraPoolPredFailure era) x -> DijkstraPoolPredFailure era
to :: forall x.
Rep (DijkstraPoolPredFailure era) x -> DijkstraPoolPredFailure era
Generic, DijkstraPoolPredFailure era -> ()
(DijkstraPoolPredFailure era -> ())
-> NFData (DijkstraPoolPredFailure era)
forall era. DijkstraPoolPredFailure era -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall era. DijkstraPoolPredFailure era -> ()
rnf :: DijkstraPoolPredFailure era -> ()
NFData)

instance Era era => EncCBOR (DijkstraPoolPredFailure era) where
  encCBOR :: DijkstraPoolPredFailure era -> Encoding
encCBOR = \case
    StakePoolNotRegisteredOnKeyPOOL KeyHash StakePool
kh ->
      Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
0 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> KeyHash StakePool -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR KeyHash StakePool
kh
    StakePoolRetirementWrongEpochPOOL Mismatch RelGT EpochNo
gt Mismatch RelLTEQ EpochNo
lt ->
      Word -> Encoding
encodeListLen Word
3
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
1 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Mismatch RelGT EpochNo -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Mismatch RelGT EpochNo
gt
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Mismatch RelLTEQ EpochNo -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Mismatch RelLTEQ EpochNo
lt
    StakePoolCostTooLowPOOL Mismatch RelGTEQ Coin
m ->
      Word -> Encoding
encodeListLen Word
2 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
3 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Mismatch RelGTEQ Coin -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Mismatch RelGTEQ Coin
m
    WrongNetworkPOOL Mismatch RelEQ Network
m KeyHash StakePool
c ->
      Word -> Encoding
encodeListLen Word
3 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
4 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Mismatch RelEQ Network -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Mismatch RelEQ Network
m Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> KeyHash StakePool -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR KeyHash StakePool
c
    PoolMedataHashTooBig KeyHash StakePool
a Int
b ->
      Word -> Encoding
encodeListLen Word
3 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
5 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> KeyHash StakePool -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR KeyHash StakePool
a Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Int -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Int
b
    VRFKeyHashAlreadyRegistered KeyHash StakePool
a VRFVerKeyHash StakePoolVRF
b ->
      Word -> Encoding
encodeListLen Word
3 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
6 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> KeyHash StakePool -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR KeyHash StakePool
a Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> VRFVerKeyHash StakePoolVRF -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR VRFVerKeyHash StakePoolVRF
b
    BlsKeyInvalidProofOfPossession KeyHash StakePool
a BlsKey
b ->
      Word -> Encoding
encodeListLen Word
3 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
7 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> KeyHash StakePool -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR KeyHash StakePool
a Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> BlsKey -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR BlsKey
b
    BlsKeyAlreadyRegistered KeyHash StakePool
a BlsKey
b ->
      Word -> Encoding
encodeListLen Word
3 Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word8 -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
8 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> KeyHash StakePool -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR KeyHash StakePool
a Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> BlsKey -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR BlsKey
b

instance Era era => DecCBOR (DijkstraPoolPredFailure era) where
  decCBOR :: forall s. Decoder s (DijkstraPoolPredFailure era)
decCBOR = Text
-> (Word -> Decoder s (Int, DijkstraPoolPredFailure era))
-> Decoder s (DijkstraPoolPredFailure era)
forall s a. Text -> (Word -> Decoder s (Int, a)) -> Decoder s a
decodeRecordSum Text
"PredicateFailure (POOL era)" ((Word -> Decoder s (Int, DijkstraPoolPredFailure era))
 -> Decoder s (DijkstraPoolPredFailure era))
-> (Word -> Decoder s (Int, DijkstraPoolPredFailure era))
-> Decoder s (DijkstraPoolPredFailure era)
forall a b. (a -> b) -> a -> b
$
    \case
      Word
0 -> do
        kh <- Decoder s (KeyHash StakePool)
forall s. Decoder s (KeyHash StakePool)
forall a s. DecCBOR a => Decoder s a
decCBOR
        pure (2, StakePoolNotRegisteredOnKeyPOOL kh)
      Word
1 -> do
        gt <- Decoder s (Mismatch RelGT EpochNo)
forall s. Decoder s (Mismatch RelGT EpochNo)
forall a s. DecCBOR a => Decoder s a
decCBOR
        lt <- decCBOR
        pure (3, StakePoolRetirementWrongEpochPOOL gt lt)
      Word
3 -> do
        costMismatch <- Decoder s (Mismatch RelGTEQ Coin)
forall s. Decoder s (Mismatch RelGTEQ Coin)
forall a s. DecCBOR a => Decoder s a
decCBOR
        pure (2, StakePoolCostTooLowPOOL costMismatch)
      Word
4 -> do
        networkIdMismatch <- Decoder s (Mismatch RelEQ Network)
forall s. Decoder s (Mismatch RelEQ Network)
forall a s. DecCBOR a => Decoder s a
decCBOR
        poolId <- decCBOR
        pure (3, WrongNetworkPOOL networkIdMismatch poolId)
      Word
5 -> do
        poolID <- Decoder s (KeyHash StakePool)
forall s. Decoder s (KeyHash StakePool)
forall a s. DecCBOR a => Decoder s a
decCBOR
        s <- decCBOR
        pure (3, PoolMedataHashTooBig poolID s)
      Word
6 -> do
        poolID <- Decoder s (KeyHash StakePool)
forall s. Decoder s (KeyHash StakePool)
forall a s. DecCBOR a => Decoder s a
decCBOR
        vrfKeyHash <- decCBOR
        pure (3, VRFKeyHashAlreadyRegistered poolID vrfKeyHash)
      Word
7 -> do
        poolID <- Decoder s (KeyHash StakePool)
forall s. Decoder s (KeyHash StakePool)
forall a s. DecCBOR a => Decoder s a
decCBOR
        blsKey <- decCBOR
        pure (3, BlsKeyInvalidProofOfPossession poolID blsKey)
      Word
8 -> do
        poolID <- Decoder s (KeyHash StakePool)
forall s. Decoder s (KeyHash StakePool)
forall a s. DecCBOR a => Decoder s a
decCBOR
        blsKey <- decCBOR
        pure (3, BlsKeyAlreadyRegistered poolID blsKey)
      Word
k -> Word -> Decoder s (Int, DijkstraPoolPredFailure era)
forall a (m :: * -> *). (Typeable a, MonadFail m) => Word -> m a
invalidKey Word
k

type instance EraRuleFailure "POOL" DijkstraEra = DijkstraPoolPredFailure DijkstraEra

type instance EraRuleEvent "POOL" DijkstraEra = Shelley.PoolEvent DijkstraEra

instance InjectRuleFailure "POOL" DijkstraPoolPredFailure DijkstraEra

instance InjectRuleEvent "POOL" Shelley.PoolEvent DijkstraEra

instance InjectRuleFailure "POOL" Shelley.ShelleyPoolPredFailure DijkstraEra where
  injectFailure :: ShelleyPoolPredFailure DijkstraEra
-> EraRuleFailure "POOL" DijkstraEra
injectFailure = \case
    Shelley.StakePoolNotRegisteredOnKeyPOOL KeyHash StakePool
poolId -> KeyHash StakePool -> DijkstraPoolPredFailure DijkstraEra
forall era. KeyHash StakePool -> DijkstraPoolPredFailure era
StakePoolNotRegisteredOnKeyPOOL KeyHash StakePool
poolId
    Shelley.StakePoolRetirementWrongEpochPOOL Mismatch RelGT EpochNo
mismatchGTEpochNo Mismatch RelLTEQ EpochNo
mismatchLTEQEpochNo -> Mismatch RelGT EpochNo
-> Mismatch RelLTEQ EpochNo -> DijkstraPoolPredFailure DijkstraEra
forall era.
Mismatch RelGT EpochNo
-> Mismatch RelLTEQ EpochNo -> DijkstraPoolPredFailure era
StakePoolRetirementWrongEpochPOOL Mismatch RelGT EpochNo
mismatchGTEpochNo Mismatch RelLTEQ EpochNo
mismatchLTEQEpochNo
    Shelley.StakePoolCostTooLowPOOL Mismatch RelGTEQ Coin
mismatchCost -> Mismatch RelGTEQ Coin -> DijkstraPoolPredFailure DijkstraEra
forall era. Mismatch RelGTEQ Coin -> DijkstraPoolPredFailure era
StakePoolCostTooLowPOOL Mismatch RelGTEQ Coin
mismatchCost
    Shelley.WrongNetworkPOOL Mismatch RelEQ Network
mismatchNetwork KeyHash StakePool
poolId -> Mismatch RelEQ Network
-> KeyHash StakePool -> DijkstraPoolPredFailure DijkstraEra
forall era.
Mismatch RelEQ Network
-> KeyHash StakePool -> DijkstraPoolPredFailure era
WrongNetworkPOOL Mismatch RelEQ Network
mismatchNetwork KeyHash StakePool
poolId
    Shelley.PoolMedataHashTooBig KeyHash StakePool
poolId Int
metadataHashSize -> KeyHash StakePool -> Int -> DijkstraPoolPredFailure DijkstraEra
forall era. KeyHash StakePool -> Int -> DijkstraPoolPredFailure era
PoolMedataHashTooBig KeyHash StakePool
poolId Int
metadataHashSize
    Shelley.VRFKeyHashAlreadyRegistered KeyHash StakePool
poolId VRFVerKeyHash StakePoolVRF
poolVrfKeyHash -> KeyHash StakePool
-> VRFVerKeyHash StakePoolVRF
-> DijkstraPoolPredFailure DijkstraEra
forall era.
KeyHash StakePool
-> VRFVerKeyHash StakePoolVRF -> DijkstraPoolPredFailure era
VRFKeyHashAlreadyRegistered KeyHash StakePool
poolId VRFVerKeyHash StakePoolVRF
poolVrfKeyHash

instance
  ( EraPParams era
  , EraRule "POOL" era ~ POOL era
  , InjectRuleFailure "POOL" Shelley.ShelleyPoolPredFailure era
  , InjectRuleFailure "POOL" DijkstraPoolPredFailure era
  , InjectRuleEvent "POOL" Shelley.PoolEvent era
  ) =>
  STS (POOL era)
  where
  type State (POOL era) = PState era

  type Signal (POOL era) = PoolCert era

  type Environment (POOL era) = Shelley.PoolEnv era

  type BaseM (POOL era) = ShelleyBase
  type PredicateFailure (POOL era) = DijkstraPoolPredFailure era
  type Event (POOL era) = Shelley.PoolEvent era

  transitionRules :: [TransitionRule (POOL era)]
transitionRules = [TransitionRule (EraRule "POOL" era)
TransitionRule (POOL era)
forall (rule :: Symbol) era.
(EraPParams era, Signal (EraRule rule era) ~ PoolCert era,
 Environment (EraRule rule era) ~ PoolEnv era,
 State (EraRule rule era) ~ PState era, STS (EraRule rule era),
 BaseM (EraRule rule era) ~ ShelleyBase,
 InjectRuleFailure rule DijkstraPoolPredFailure era,
 InjectRuleEvent rule PoolEvent era) =>
TransitionRule (EraRule rule era)
poolTransition]

-- Invariant of `psVRFKeyHashes`: a VRF key hash maps to the number of
-- references held by registered stake pools, where a pool holds one reference
-- through its active parameters (`psStakePools`) and one more through its
-- future parameters (`psFutureStakePoolParams`) whenever the future VRF key
-- hash differs from the active one. A future VRF key hash that coincides with
-- the pool's active one is not counted separately.
--
-- Invariant of `psBlsKeyHashes`: it holds the hash of every BLS public key that
-- a registered stake pool uses through its active or its future parameters. No
-- two pools may use the same BLS public key, so it only needs to tell whether a
-- key is in use. Only the public key is hashed, so the proof of possession does
-- not matter for the uniqueness, and a BLS key that has aged out stays in the
-- state and still counts, as in `IsBLSUnique` of the Agda specification.
--
-- The Dijkstra POOLREAP rule keeps these invariants at the epoch boundary: a
-- pool whose future VRF or BLS key hash differs from its active one releases
-- the active one once the future parameters are adopted, and a retired pool
-- releases the key hashes it uses.
poolTransition ::
  forall rule era.
  ( EraPParams era
  , Signal (EraRule rule era) ~ PoolCert era
  , Environment (EraRule rule era) ~ Shelley.PoolEnv era
  , State (EraRule rule era) ~ PState era
  , STS (EraRule rule era)
  , BaseM (EraRule rule era) ~ ShelleyBase
  , InjectRuleFailure rule DijkstraPoolPredFailure era
  , InjectRuleEvent rule Shelley.PoolEvent era
  ) =>
  TransitionRule (EraRule rule era)
poolTransition :: forall (rule :: Symbol) era.
(EraPParams era, Signal (EraRule rule era) ~ PoolCert era,
 Environment (EraRule rule era) ~ PoolEnv era,
 State (EraRule rule era) ~ PState era, STS (EraRule rule era),
 BaseM (EraRule rule era) ~ ShelleyBase,
 InjectRuleFailure rule DijkstraPoolPredFailure era,
 InjectRuleEvent rule PoolEvent era) =>
TransitionRule (EraRule rule era)
poolTransition = do
  TRC
    ( Shelley.PoolEnv cEpoch pp
      , ps@PState {psStakePools, psFutureStakePoolParams, psVRFKeyHashes, psBlsKeyHashes}
      , poolCert
      ) <-
    Rule
  (EraRule rule era)
  'Transition
  (RuleContext 'Transition (EraRule rule era))
F (Clause (EraRule rule era) 'Transition) (TRC (EraRule rule era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  case poolCert of
    RegPool StakePoolParams era
stakePoolParams -> do
      let StakePoolParams {KeyHash StakePool
sppId :: KeyHash StakePool
sppId :: forall era. StakePoolParams era -> KeyHash StakePool
sppId, sppBlsKey :: forall era. StakePoolParams era -> StrictMaybe BlsKey
sppBlsKey = StrictMaybe BlsKey
newBlsKey, VRFVerKeyHash StakePoolVRF
sppVrf :: VRFVerKeyHash StakePoolVRF
sppVrf :: forall era. StakePoolParams era -> VRFVerKeyHash StakePoolVRF
sppVrf, AccountAddress
sppAccountAddress :: AccountAddress
sppAccountAddress :: forall era. StakePoolParams era -> AccountAddress
sppAccountAddress, StrictMaybe PoolMetadata
sppMetadata :: StrictMaybe PoolMetadata
sppMetadata :: forall era. StakePoolParams era -> StrictMaybe PoolMetadata
sppMetadata, Coin
sppCost :: Coin
sppCost :: forall era. StakePoolParams era -> Coin
sppCost} =
            StakePoolParams era
stakePoolParams
      actualNetID <- BaseM (EraRule rule era) Network
-> Rule (EraRule rule era) 'Transition Network
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (EraRule rule era) Network
 -> Rule (EraRule rule era) 'Transition Network)
-> BaseM (EraRule rule era) Network
-> Rule (EraRule rule era) 'Transition Network
forall a b. (a -> b) -> a -> b
$ (Globals -> Network) -> ReaderT Globals Identity Network
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> Network
networkId
      let suppliedNetID = AccountAddress -> Network
aaNetworkId AccountAddress
sppAccountAddress
      actualNetID
        == suppliedNetID
          ?! injectFailure
            ( WrongNetworkPOOL
                Mismatch
                  { mismatchSupplied = suppliedNetID
                  , mismatchExpected = actualNetID
                  }
                sppId
            )

      forM_ sppMetadata $ \PoolMetadata
pmd ->
        let s :: Int
s = ByteArray -> Int
sizeofByteArray (ByteArray -> Int) -> ByteArray -> Int
forall a b. (a -> b) -> a -> b
$ PoolMetadata -> ByteArray
pmHash PoolMetadata
pmd
         in Int
s
              Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Word -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([HASH] -> Word
forall h (proxy :: * -> *). HashAlgorithm h => proxy h -> Word
hashSize ([] @HASH))
                Bool
-> PredicateFailure (EraRule rule era)
-> Rule (EraRule rule era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! DijkstraPoolPredFailure era -> EraRuleFailure rule era
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure (KeyHash StakePool -> Int -> DijkstraPoolPredFailure era
forall era. KeyHash StakePool -> Int -> DijkstraPoolPredFailure era
PoolMedataHashTooBig KeyHash StakePool
sppId Int
s)

      let minPoolCost = PParams era
pp PParams era -> Getting Coin (PParams era) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (PParams era) Coin
forall era.
(EraPParams era, HasCallStack) =>
Lens' (PParams era) Coin
Lens' (PParams era) Coin
ppMinPoolCostL
      sppCost
        >= minPoolCost
          ?! injectFailure
            ( StakePoolCostTooLowPOOL
                Mismatch
                  { mismatchSupplied = sppCost
                  , mismatchExpected = minPoolCost
                  }
            )

      -- Returns the BlsKey wrapped in 'SJust' if it is invalid. A valid 'BlsKey' returns 'SNothing'.
      let invalidBlsKey = do
            SJust blsKey@BlsKey {blsPubKey, blsPossessionProof} <- StrictMaybe BlsKey -> Maybe (StrictMaybe BlsKey)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure StrictMaybe BlsKey
newBlsKey
            Left _ <-
              pure $
                verifyPossessionProofDSIGN
                  minSigPoPDST
                  blsPubKey
                  blsPossessionProof
            pure (sppId, blsKey)
      checkFailOnJustStatic invalidBlsKey $ uncurry BlsKeyInvalidProofOfPossession

      let newBlsKeyHash = BlsKey -> BlsVerKeyHash
hashBlsKey (BlsKey -> BlsVerKeyHash)
-> StrictMaybe BlsKey -> StrictMaybe BlsVerKeyHash
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe BlsKey
newBlsKey
          -- Returns the BLS key if another pool uses its public key, which is the case when
          -- its hash is in use, but is none of the given hashes of the pool's own BLS keys. A
          -- registration without a BLS key never clashes.
          blsKeyUsedByAnotherPool [StrictMaybe BlsVerKeyHash]
ownBlsKeyHashes = StrictMaybe BlsKey -> Maybe BlsKey
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe (StrictMaybe BlsKey -> Maybe BlsKey)
-> StrictMaybe BlsKey -> Maybe BlsKey
forall a b. (a -> b) -> a -> b
$ do
            blsKey <- StrictMaybe BlsKey
newBlsKey
            blsKeyHash <- newBlsKeyHash
            guard $
              Set.member blsKeyHash psBlsKeyHashes && newBlsKeyHash `notElem` ownBlsKeyHashes
            pure blsKey
          trackNewBlsKeyHash = (Set BlsVerKeyHash -> Set BlsVerKeyHash)
-> (BlsVerKeyHash -> Set BlsVerKeyHash -> Set BlsVerKeyHash)
-> StrictMaybe BlsVerKeyHash
-> Set BlsVerKeyHash
-> Set BlsVerKeyHash
forall a b. a -> (b -> a) -> StrictMaybe b -> a
strictMaybe Set BlsVerKeyHash -> Set BlsVerKeyHash
forall a. a -> a
id BlsVerKeyHash -> Set BlsVerKeyHash -> Set BlsVerKeyHash
forall a. Ord a => a -> Set a -> Set a
Set.insert StrictMaybe BlsVerKeyHash
newBlsKeyHash

      case Map.lookup sppId psStakePools of
        -- register new, Pool-Reg
        Maybe StakePoolState
Nothing -> do
          VRFVerKeyHash StakePoolVRF
-> Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.notMember VRFVerKeyHash StakePoolVRF
sppVrf Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
psVRFKeyHashes
            Bool
-> PredicateFailure (EraRule rule era)
-> Rule (EraRule rule era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! DijkstraPoolPredFailure era -> EraRuleFailure rule era
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure (KeyHash StakePool
-> VRFVerKeyHash StakePoolVRF -> DijkstraPoolPredFailure era
forall era.
KeyHash StakePool
-> VRFVerKeyHash StakePoolVRF -> DijkstraPoolPredFailure era
VRFKeyHashAlreadyRegistered KeyHash StakePool
sppId VRFVerKeyHash StakePoolVRF
sppVrf)
          Maybe BlsKey
-> (BlsKey -> DijkstraPoolPredFailure era)
-> Rule (EraRule rule era) 'Transition ()
forall (rule :: Symbol) (t :: * -> *) era sts a (ctx :: RuleType).
(InjectRuleFailure rule t era,
 PredicateFailure sts ~ EraRuleFailure rule era) =>
Maybe a -> (a -> t era) -> Rule sts ctx ()
checkFailOnJust ([StrictMaybe BlsVerKeyHash] -> Maybe BlsKey
blsKeyUsedByAnotherPool []) ((BlsKey -> DijkstraPoolPredFailure era)
 -> Rule (EraRule rule era) 'Transition ())
-> (BlsKey -> DijkstraPoolPredFailure era)
-> Rule (EraRule rule era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ KeyHash StakePool -> BlsKey -> DijkstraPoolPredFailure era
forall era.
KeyHash StakePool -> BlsKey -> DijkstraPoolPredFailure era
BlsKeyAlreadyRegistered KeyHash StakePool
sppId
          Event (EraRule rule era) -> Rule (EraRule rule era) 'Transition ()
forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent (Event (EraRule rule era)
 -> Rule (EraRule rule era) 'Transition ())
-> Event (EraRule rule era)
-> Rule (EraRule rule era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ PoolEvent era -> EraRuleEvent rule era
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleEvent rule t era =>
t era -> EraRuleEvent rule era
injectEvent (PoolEvent era -> EraRuleEvent rule era)
-> PoolEvent era -> EraRuleEvent rule era
forall a b. (a -> b) -> a -> b
$ KeyHash StakePool -> PoolEvent era
forall era. KeyHash StakePool -> PoolEvent era
Shelley.RegisterPool KeyHash StakePool
sppId
          PState era
-> F (Clause (EraRule rule era) 'Transition) (PState era)
forall a. a -> F (Clause (EraRule rule era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PState era
 -> F (Clause (EraRule rule era) 'Transition) (PState era))
-> PState era
-> F (Clause (EraRule rule era) 'Transition) (PState era)
forall a b. (a -> b) -> a -> b
$
            PState era
State (EraRule rule era)
ps
              PState era -> (PState era -> PState era) -> PState era
forall a b. a -> (a -> b) -> b
& (Map (KeyHash StakePool) StakePoolState
 -> Identity (Map (KeyHash StakePool) StakePoolState))
-> PState era -> Identity (PState era)
forall era (f :: * -> *).
Functor f =>
(Map (KeyHash StakePool) StakePoolState
 -> f (Map (KeyHash StakePool) StakePoolState))
-> PState era -> f (PState era)
psStakePoolsL
                ((Map (KeyHash StakePool) StakePoolState
  -> Identity (Map (KeyHash StakePool) StakePoolState))
 -> PState era -> Identity (PState era))
-> (Map (KeyHash StakePool) StakePoolState
    -> Map (KeyHash StakePool) StakePoolState)
-> PState era
-> PState era
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ KeyHash StakePool
-> StakePoolState
-> Map (KeyHash StakePool) StakePoolState
-> Map (KeyHash StakePool) StakePoolState
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert
                  KeyHash StakePool
sppId
                  (EpochNo
-> StrictMaybe BlsKeyState
-> CompactForm Coin
-> Set (Credential Staking)
-> StakePoolParams era
-> StakePoolState
forall era.
EpochNo
-> StrictMaybe BlsKeyState
-> CompactForm Coin
-> Set (Credential Staking)
-> StakePoolParams era
-> StakePoolState
mkStakePoolState EpochNo
cEpoch StrictMaybe BlsKeyState
forall a. StrictMaybe a
SNothing (PParams era
pp PParams era
-> Getting (CompactForm Coin) (PParams era) (CompactForm Coin)
-> CompactForm Coin
forall s a. s -> Getting a s a -> a
^. Getting (CompactForm Coin) (PParams era) (CompactForm Coin)
forall era.
EraPParams era =>
Lens' (PParams era) (CompactForm Coin)
Lens' (PParams era) (CompactForm Coin)
ppPoolDepositCompactL) Set (Credential Staking)
forall a. Monoid a => a
mempty StakePoolParams era
stakePoolParams)
              PState era -> (PState era -> PState era) -> PState era
forall a b. a -> (a -> b) -> b
& (Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
 -> Identity (Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)))
-> PState era -> Identity (PState era)
forall era (f :: * -> *).
Functor f =>
(Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
 -> f (Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)))
-> PState era -> f (PState era)
psVRFKeyHashesL ((Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
  -> Identity (Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)))
 -> PState era -> Identity (PState era))
-> (Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
    -> Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64))
-> PState era
-> PState era
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ VRFVerKeyHash StakePoolVRF
-> Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
-> Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
addVRFKeyHashOccurrence VRFVerKeyHash StakePoolVRF
sppVrf
              PState era -> (PState era -> PState era) -> PState era
forall a b. a -> (a -> b) -> b
& (Set BlsVerKeyHash -> Identity (Set BlsVerKeyHash))
-> PState era -> Identity (PState era)
forall era (f :: * -> *).
Functor f =>
(Set BlsVerKeyHash -> f (Set BlsVerKeyHash))
-> PState era -> f (PState era)
psBlsKeyHashesL ((Set BlsVerKeyHash -> Identity (Set BlsVerKeyHash))
 -> PState era -> Identity (PState era))
-> (Set BlsVerKeyHash -> Set BlsVerKeyHash)
-> PState era
-> PState era
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ Set BlsVerKeyHash -> Set BlsVerKeyHash
trackNewBlsKeyHash
        -- re-register Pool
        Just StakePoolState
stakePoolState -> do
          let activeVrf :: VRFVerKeyHash StakePoolVRF
activeVrf = StakePoolState
stakePoolState StakePoolState
-> Getting
     (VRFVerKeyHash StakePoolVRF)
     StakePoolState
     (VRFVerKeyHash StakePoolVRF)
-> VRFVerKeyHash StakePoolVRF
forall s a. s -> Getting a s a -> a
^. Getting
  (VRFVerKeyHash StakePoolVRF)
  StakePoolState
  (VRFVerKeyHash StakePoolVRF)
Lens' StakePoolState (VRFVerKeyHash StakePoolVRF)
spsVrfL
              mbFutureParams :: Maybe (StakePoolParams era)
mbFutureParams = KeyHash StakePool
-> Map (KeyHash StakePool) (StakePoolParams era)
-> Maybe (StakePoolParams era)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KeyHash StakePool
sppId Map (KeyHash StakePool) (StakePoolParams era)
psFutureStakePoolParams
              mbFutureVrf :: Maybe (VRFVerKeyHash StakePoolVRF)
mbFutureVrf = (StakePoolParams era
-> Getting
     (VRFVerKeyHash StakePoolVRF)
     (StakePoolParams era)
     (VRFVerKeyHash StakePoolVRF)
-> VRFVerKeyHash StakePoolVRF
forall s a. s -> Getting a s a -> a
^. Getting
  (VRFVerKeyHash StakePoolVRF)
  (StakePoolParams era)
  (VRFVerKeyHash StakePoolVRF)
forall era (f :: * -> *).
Functor f =>
(VRFVerKeyHash StakePoolVRF -> f (VRFVerKeyHash StakePoolVRF))
-> StakePoolParams era -> f (StakePoolParams era)
sppVrfL) (StakePoolParams era -> VRFVerKeyHash StakePoolVRF)
-> Maybe (StakePoolParams era)
-> Maybe (VRFVerKeyHash StakePoolVRF)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (StakePoolParams era)
mbFutureParams
              -- The only reference to this VRF key hash, if any, must be the
              -- pool's own, held through its active or its future parameters.
              expectedOccurrences :: Maybe (NonZero Word64)
expectedOccurrences
                | VRFVerKeyHash StakePoolVRF
sppVrf VRFVerKeyHash StakePoolVRF -> VRFVerKeyHash StakePoolVRF -> Bool
forall a. Eq a => a -> a -> Bool
== VRFVerKeyHash StakePoolVRF
activeVrf Bool -> Bool -> Bool
|| Maybe (VRFVerKeyHash StakePoolVRF)
mbFutureVrf Maybe (VRFVerKeyHash StakePoolVRF)
-> Maybe (VRFVerKeyHash StakePoolVRF) -> Bool
forall a. Eq a => a -> a -> Bool
== VRFVerKeyHash StakePoolVRF -> Maybe (VRFVerKeyHash StakePoolVRF)
forall a. a -> Maybe a
Just VRFVerKeyHash StakePoolVRF
sppVrf = NonZero Word64 -> Maybe (NonZero Word64)
forall a. a -> Maybe a
Just (forall (n :: Natural) a.
(KnownNat n, 1 <= n, WithinBounds n a, Num a) =>
NonZero a
knownNonZeroBounded @1)
                | Bool
otherwise = Maybe (NonZero Word64)
forall a. Maybe a
Nothing
          VRFVerKeyHash StakePoolVRF
-> Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
-> Maybe (NonZero Word64)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VRFVerKeyHash StakePoolVRF
sppVrf Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
psVRFKeyHashes
            Maybe (NonZero Word64) -> Maybe (NonZero Word64) -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe (NonZero Word64)
expectedOccurrences
              Bool
-> PredicateFailure (EraRule rule era)
-> Rule (EraRule rule era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! DijkstraPoolPredFailure era -> EraRuleFailure rule era
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure (KeyHash StakePool
-> VRFVerKeyHash StakePoolVRF -> DijkstraPoolPredFailure era
forall era.
KeyHash StakePool
-> VRFVerKeyHash StakePoolVRF -> DijkstraPoolPredFailure era
VRFKeyHashAlreadyRegistered KeyHash StakePool
sppId VRFVerKeyHash StakePoolVRF
sppVrf)
          let updateFutureVRFKeyHash :: Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
-> Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
updateFutureVRFKeyHash
                | Maybe (VRFVerKeyHash StakePoolVRF)
mbFutureVrf Maybe (VRFVerKeyHash StakePoolVRF)
-> Maybe (VRFVerKeyHash StakePoolVRF) -> Bool
forall a. Eq a => a -> a -> Bool
/= VRFVerKeyHash StakePoolVRF -> Maybe (VRFVerKeyHash StakePoolVRF)
forall a. a -> Maybe a
Just VRFVerKeyHash StakePoolVRF
sppVrf =
                    -- The reference held by the future parameters moves from
                    -- `mbFutureVrf` to `sppVrf`. References that coincide with
                    -- the active VRF key hash are not counted separately, per
                    -- the invariant on `psVRFKeyHashes`.
                    let removeOldOccurrence :: Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
-> Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
removeOldOccurrence = case Maybe (VRFVerKeyHash StakePoolVRF)
mbFutureVrf of
                          Just VRFVerKeyHash StakePoolVRF
oldFutureVrf
                            | VRFVerKeyHash StakePoolVRF
oldFutureVrf VRFVerKeyHash StakePoolVRF -> VRFVerKeyHash StakePoolVRF -> Bool
forall a. Eq a => a -> a -> Bool
/= VRFVerKeyHash StakePoolVRF
activeVrf -> VRFVerKeyHash StakePoolVRF
-> Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
-> Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
removeVRFKeyHashOccurrence VRFVerKeyHash StakePoolVRF
oldFutureVrf
                          Maybe (VRFVerKeyHash StakePoolVRF)
_ -> Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
-> Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
forall a. a -> a
id
                        addNewOccurrence :: Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
-> Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
addNewOccurrence
                          | VRFVerKeyHash StakePoolVRF
sppVrf VRFVerKeyHash StakePoolVRF -> VRFVerKeyHash StakePoolVRF -> Bool
forall a. Eq a => a -> a -> Bool
/= VRFVerKeyHash StakePoolVRF
activeVrf = VRFVerKeyHash StakePoolVRF
-> Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
-> Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
addVRFKeyHashOccurrence VRFVerKeyHash StakePoolVRF
sppVrf
                          | Bool
otherwise = Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
-> Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
forall a. a -> a
id
                     in Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
-> Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
addNewOccurrence (Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
 -> Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64))
-> (Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
    -> Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64))
-> Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
-> Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
-> Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
removeOldOccurrence
                | Bool
otherwise = Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
-> Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
forall a. a -> a
id
              activeBlsKeyHash :: StrictMaybe BlsVerKeyHash
activeBlsKeyHash = BlsKey -> BlsVerKeyHash
hashBlsKey (BlsKey -> BlsVerKeyHash)
-> (BlsKeyState -> BlsKey) -> BlsKeyState -> BlsVerKeyHash
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BlsKeyState -> BlsKey
bksKey (BlsKeyState -> BlsVerKeyHash)
-> StrictMaybe BlsKeyState -> StrictMaybe BlsVerKeyHash
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StakePoolState
stakePoolState StakePoolState
-> Getting
     (StrictMaybe BlsKeyState) StakePoolState (StrictMaybe BlsKeyState)
-> StrictMaybe BlsKeyState
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictMaybe BlsKeyState) StakePoolState (StrictMaybe BlsKeyState)
Lens' StakePoolState (StrictMaybe BlsKeyState)
spsBlsKeyL
              newFutureBlsKeyHash :: StrictMaybe BlsVerKeyHash
newFutureBlsKeyHash =
                BlsKey -> BlsVerKeyHash
hashBlsKey (BlsKey -> BlsVerKeyHash)
-> StrictMaybe BlsKey -> StrictMaybe BlsVerKeyHash
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (StakePoolParams era -> StrictMaybe BlsKey
forall era. StakePoolParams era -> StrictMaybe BlsKey
sppBlsKey (StakePoolParams era -> StrictMaybe BlsKey)
-> StrictMaybe (StakePoolParams era) -> StrictMaybe BlsKey
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Maybe (StakePoolParams era) -> StrictMaybe (StakePoolParams era)
forall a. Maybe a -> StrictMaybe a
maybeToStrictMaybe Maybe (StakePoolParams era)
mbFutureParams)
              -- The re-registration replaces the future parameters, which releases their BLS key,
              -- unless the active parameters use it as well. If the re-registration uses that
              -- same key, `trackNewBlsKeyHash` records it again.
              releaseFutureBlsKeyHash :: Set BlsVerKeyHash -> Set BlsVerKeyHash
releaseFutureBlsKeyHash = case StrictMaybe BlsVerKeyHash
newFutureBlsKeyHash of
                SJust BlsVerKeyHash
curFutureBlsKeyHash
                  | StrictMaybe BlsVerKeyHash
newFutureBlsKeyHash StrictMaybe BlsVerKeyHash -> StrictMaybe BlsVerKeyHash -> Bool
forall a. Eq a => a -> a -> Bool
/= StrictMaybe BlsVerKeyHash
activeBlsKeyHash -> BlsVerKeyHash -> Set BlsVerKeyHash -> Set BlsVerKeyHash
forall a. Ord a => a -> Set a -> Set a
Set.delete BlsVerKeyHash
curFutureBlsKeyHash
                StrictMaybe BlsVerKeyHash
_ -> Set BlsVerKeyHash -> Set BlsVerKeyHash
forall a. a -> a
id
          Maybe BlsKey
-> (BlsKey -> DijkstraPoolPredFailure era)
-> Rule (EraRule rule era) 'Transition ()
forall (rule :: Symbol) (t :: * -> *) era sts a (ctx :: RuleType).
(InjectRuleFailure rule t era,
 PredicateFailure sts ~ EraRuleFailure rule era) =>
Maybe a -> (a -> t era) -> Rule sts ctx ()
checkFailOnJust ([StrictMaybe BlsVerKeyHash] -> Maybe BlsKey
blsKeyUsedByAnotherPool [StrictMaybe BlsVerKeyHash
activeBlsKeyHash, StrictMaybe BlsVerKeyHash
newFutureBlsKeyHash]) ((BlsKey -> DijkstraPoolPredFailure era)
 -> Rule (EraRule rule era) 'Transition ())
-> (BlsKey -> DijkstraPoolPredFailure era)
-> Rule (EraRule rule era) 'Transition ()
forall a b. (a -> b) -> a -> b
$
            KeyHash StakePool -> BlsKey -> DijkstraPoolPredFailure era
forall era.
KeyHash StakePool -> BlsKey -> DijkstraPoolPredFailure era
BlsKeyAlreadyRegistered KeyHash StakePool
sppId
          Event (EraRule rule era) -> Rule (EraRule rule era) 'Transition ()
forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent (Event (EraRule rule era)
 -> Rule (EraRule rule era) 'Transition ())
-> Event (EraRule rule era)
-> Rule (EraRule rule era) 'Transition ()
forall a b. (a -> b) -> a -> b
$ PoolEvent era -> EraRuleEvent rule era
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleEvent rule t era =>
t era -> EraRuleEvent rule era
injectEvent (PoolEvent era -> EraRuleEvent rule era)
-> PoolEvent era -> EraRuleEvent rule era
forall a b. (a -> b) -> a -> b
$ KeyHash StakePool -> PoolEvent era
forall era. KeyHash StakePool -> PoolEvent era
Shelley.ReregisterPool KeyHash StakePool
sppId
          -- This `sppId` is already registered, so we want to reregister it.
          -- That means adding it to the futureStakePoolParams or overriding it  with the new 'poolParams'.
          -- We must also unretire it, if it has been scheduled for retirement.
          -- The deposit does not change.
          PState era
-> F (Clause (EraRule rule era) 'Transition) (PState era)
forall a. a -> F (Clause (EraRule rule era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PState era
 -> F (Clause (EraRule rule era) 'Transition) (PState era))
-> PState era
-> F (Clause (EraRule rule era) 'Transition) (PState era)
forall a b. (a -> b) -> a -> b
$
            PState era
State (EraRule rule era)
ps
              PState era -> (PState era -> PState era) -> PState era
forall a b. a -> (a -> b) -> b
& (Map (KeyHash StakePool) (StakePoolParams era)
 -> Identity (Map (KeyHash StakePool) (StakePoolParams era)))
-> PState era -> Identity (PState era)
forall era (f :: * -> *).
Functor f =>
(Map (KeyHash StakePool) (StakePoolParams era)
 -> f (Map (KeyHash StakePool) (StakePoolParams era)))
-> PState era -> f (PState era)
psFutureStakePoolParamsL
                ((Map (KeyHash StakePool) (StakePoolParams era)
  -> Identity (Map (KeyHash StakePool) (StakePoolParams era)))
 -> PState era -> Identity (PState era))
-> (Map (KeyHash StakePool) (StakePoolParams era)
    -> Map (KeyHash StakePool) (StakePoolParams era))
-> PState era
-> PState era
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ KeyHash StakePool
-> StakePoolParams era
-> Map (KeyHash StakePool) (StakePoolParams era)
-> Map (KeyHash StakePool) (StakePoolParams era)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert KeyHash StakePool
sppId StakePoolParams era
stakePoolParams
              PState era -> (PState era -> PState era) -> PState era
forall a b. a -> (a -> b) -> b
& (Map (KeyHash StakePool) EpochNo
 -> Identity (Map (KeyHash StakePool) EpochNo))
-> PState era -> Identity (PState era)
forall era (f :: * -> *).
Functor f =>
(Map (KeyHash StakePool) EpochNo
 -> f (Map (KeyHash StakePool) EpochNo))
-> PState era -> f (PState era)
psRetiringL ((Map (KeyHash StakePool) EpochNo
  -> Identity (Map (KeyHash StakePool) EpochNo))
 -> PState era -> Identity (PState era))
-> (Map (KeyHash StakePool) EpochNo
    -> Map (KeyHash StakePool) EpochNo)
-> PState era
-> PState era
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ KeyHash StakePool
-> Map (KeyHash StakePool) EpochNo
-> Map (KeyHash StakePool) EpochNo
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete KeyHash StakePool
sppId
              PState era -> (PState era -> PState era) -> PState era
forall a b. a -> (a -> b) -> b
& (Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
 -> Identity (Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)))
-> PState era -> Identity (PState era)
forall era (f :: * -> *).
Functor f =>
(Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
 -> f (Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)))
-> PState era -> f (PState era)
psVRFKeyHashesL ((Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
  -> Identity (Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)))
 -> PState era -> Identity (PState era))
-> (Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
    -> Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64))
-> PState era
-> PState era
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
-> Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
updateFutureVRFKeyHash
              PState era -> (PState era -> PState era) -> PState era
forall a b. a -> (a -> b) -> b
& (Set BlsVerKeyHash -> Identity (Set BlsVerKeyHash))
-> PState era -> Identity (PState era)
forall era (f :: * -> *).
Functor f =>
(Set BlsVerKeyHash -> f (Set BlsVerKeyHash))
-> PState era -> f (PState era)
psBlsKeyHashesL ((Set BlsVerKeyHash -> Identity (Set BlsVerKeyHash))
 -> PState era -> Identity (PState era))
-> (Set BlsVerKeyHash -> Set BlsVerKeyHash)
-> PState era
-> PState era
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ Set BlsVerKeyHash -> Set BlsVerKeyHash
trackNewBlsKeyHash (Set BlsVerKeyHash -> Set BlsVerKeyHash)
-> (Set BlsVerKeyHash -> Set BlsVerKeyHash)
-> Set BlsVerKeyHash
-> Set BlsVerKeyHash
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set BlsVerKeyHash -> Set BlsVerKeyHash
releaseFutureBlsKeyHash
    RetirePool KeyHash StakePool
sppId EpochNo
e -> do
      KeyHash StakePool -> Map (KeyHash StakePool) StakePoolState -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member KeyHash StakePool
sppId Map (KeyHash StakePool) StakePoolState
psStakePools Bool
-> PredicateFailure (EraRule rule era)
-> Rule (EraRule rule era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! DijkstraPoolPredFailure era -> EraRuleFailure rule era
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure (KeyHash StakePool -> DijkstraPoolPredFailure era
forall era. KeyHash StakePool -> DijkstraPoolPredFailure era
StakePoolNotRegisteredOnKeyPOOL KeyHash StakePool
sppId)
      let maxEpoch :: EpochInterval
maxEpoch = PParams era
pp PParams era
-> Getting EpochInterval (PParams era) EpochInterval
-> EpochInterval
forall s a. s -> Getting a s a -> a
^. Getting EpochInterval (PParams era) EpochInterval
forall era. EraPParams era => Lens' (PParams era) EpochInterval
Lens' (PParams era) EpochInterval
ppEMaxL
          limitEpoch :: EpochNo
limitEpoch = EpochNo -> EpochInterval -> EpochNo
addEpochInterval EpochNo
cEpoch EpochInterval
maxEpoch
      (EpochNo
cEpoch EpochNo -> EpochNo -> Bool
forall a. Ord a => a -> a -> Bool
< EpochNo
e Bool -> Bool -> Bool
&& EpochNo
e EpochNo -> EpochNo -> Bool
forall a. Ord a => a -> a -> Bool
<= EpochNo
limitEpoch)
        Bool
-> PredicateFailure (EraRule rule era)
-> Rule (EraRule rule era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! DijkstraPoolPredFailure era -> EraRuleFailure rule era
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure
          ( Mismatch RelGT EpochNo
-> Mismatch RelLTEQ EpochNo -> DijkstraPoolPredFailure era
forall era.
Mismatch RelGT EpochNo
-> Mismatch RelLTEQ EpochNo -> DijkstraPoolPredFailure era
StakePoolRetirementWrongEpochPOOL
              Mismatch -- RelGT - The supplied value should be greater than the current epoch
                { mismatchSupplied :: EpochNo
mismatchSupplied = EpochNo
e
                , mismatchExpected :: EpochNo
mismatchExpected = EpochNo
cEpoch
                }
              Mismatch -- RelLTEQ - The supplied value should be less then or equal to ppEMax after the current epoch
                { mismatchSupplied :: EpochNo
mismatchSupplied = EpochNo
e
                , mismatchExpected :: EpochNo
mismatchExpected = EpochNo
limitEpoch
                }
          )
      -- We just schedule it for retirement. When it is retired we refund the deposit (see POOLREAP)
      PState era
-> F (Clause (EraRule rule era) 'Transition) (PState era)
forall a. a -> F (Clause (EraRule rule era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PState era
 -> F (Clause (EraRule rule era) 'Transition) (PState era))
-> PState era
-> F (Clause (EraRule rule era) 'Transition) (PState era)
forall a b. (a -> b) -> a -> b
$ PState era
State (EraRule rule era)
ps PState era -> (PState era -> PState era) -> PState era
forall a b. a -> (a -> b) -> b
& (Map (KeyHash StakePool) EpochNo
 -> Identity (Map (KeyHash StakePool) EpochNo))
-> PState era -> Identity (PState era)
forall era (f :: * -> *).
Functor f =>
(Map (KeyHash StakePool) EpochNo
 -> f (Map (KeyHash StakePool) EpochNo))
-> PState era -> f (PState era)
psRetiringL ((Map (KeyHash StakePool) EpochNo
  -> Identity (Map (KeyHash StakePool) EpochNo))
 -> PState era -> Identity (PState era))
-> (Map (KeyHash StakePool) EpochNo
    -> Map (KeyHash StakePool) EpochNo)
-> PState era
-> PState era
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ KeyHash StakePool
-> EpochNo
-> Map (KeyHash StakePool) EpochNo
-> Map (KeyHash StakePool) EpochNo
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert KeyHash StakePool
sppId EpochNo
e