{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Cardano.Ledger.Shelley.Rules.Delegs (
  ShelleyDELEGS,
  DelegsEnv (..),
  ShelleyDelegsPredFailure (..),
  ShelleyDelegsEvent (..),
  PredicateFailure,
  validateStakePoolDelegateeRegistered,
) where

import Cardano.Ledger.BaseTypes (
  CertIx (..),
  EpochNo,
  ShelleyBase,
  TxIx (..),
  invalidKey,
 )
import Cardano.Ledger.Binary (
  DecCBOR (..),
  EncCBOR (..),
  decodeRecordSum,
  encodeListLen,
 )
import Cardano.Ledger.Core
import Cardano.Ledger.Credential (Ptr (..), SlotNo32 (..))
import Cardano.Ledger.Rules.ValidationMode (Test)
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.Era (ShelleyDELEGS, ShelleyEra)
import Cardano.Ledger.Shelley.Rules.Deleg (ShelleyDelegPredFailure)
import Cardano.Ledger.Shelley.Rules.Delpl (
  DelplEnv (..),
  ShelleyDELPL,
  ShelleyDelplEvent,
  ShelleyDelplPredFailure,
 )
import Cardano.Ledger.Shelley.Rules.Pool (ShelleyPoolPredFailure)
import Cardano.Ledger.Shelley.State
import Cardano.Ledger.Slot (SlotNo (..))
import Control.DeepSeq
import Control.State.Transition (
  Embed (..),
  STS (..),
  TRC (..),
  TransitionRule,
  judgmentContext,
  trans,
  validateTrans,
 )
import qualified Data.Map.Strict as Map
import Data.Sequence (Seq (..))
import Data.Typeable (Typeable)
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.Generics (Generic)
import Lens.Micro
import NoThunks.Class (NoThunks (..))
import Validation (failureUnless)

data DelegsEnv era = DelegsEnv
  { forall era. DelegsEnv era -> SlotNo
delegsSlotNo :: SlotNo
  , forall era. DelegsEnv era -> EpochNo
delegsEpochNo :: EpochNo
  -- ^ Lazy on purpose, because not all certificates need to know the current EpochNo
  , forall era. DelegsEnv era -> TxIx
delegsIx :: TxIx
  , forall era. DelegsEnv era -> PParams era
delegspp :: PParams era
  , forall era. DelegsEnv era -> Tx TopTx era
delegsTx :: Tx TopTx era
  , forall era. DelegsEnv era -> ChainAccountState
delegsAccount :: ChainAccountState
  }

deriving stock instance
  ( Show (Tx TopTx era)
  , Show (PParams era)
  ) =>
  Show (DelegsEnv era)

data ShelleyDelegsPredFailure era
  = -- | Target pool which is not registered
    DelegateeNotRegisteredDELEG
      (KeyHash StakePool)
  | -- | Subtransition Failures
    DelplFailure (PredicateFailure (EraRule "DELPL" era))
  deriving ((forall x.
 ShelleyDelegsPredFailure era
 -> Rep (ShelleyDelegsPredFailure era) x)
-> (forall x.
    Rep (ShelleyDelegsPredFailure era) x
    -> ShelleyDelegsPredFailure era)
-> Generic (ShelleyDelegsPredFailure era)
forall x.
Rep (ShelleyDelegsPredFailure era) x
-> ShelleyDelegsPredFailure era
forall x.
ShelleyDelegsPredFailure era
-> Rep (ShelleyDelegsPredFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyDelegsPredFailure era) x
-> ShelleyDelegsPredFailure era
forall era x.
ShelleyDelegsPredFailure era
-> Rep (ShelleyDelegsPredFailure era) x
$cfrom :: forall era x.
ShelleyDelegsPredFailure era
-> Rep (ShelleyDelegsPredFailure era) x
from :: forall x.
ShelleyDelegsPredFailure era
-> Rep (ShelleyDelegsPredFailure era) x
$cto :: forall era x.
Rep (ShelleyDelegsPredFailure era) x
-> ShelleyDelegsPredFailure era
to :: forall x.
Rep (ShelleyDelegsPredFailure era) x
-> ShelleyDelegsPredFailure era
Generic)

type instance EraRuleFailure "DELEGS" ShelleyEra = ShelleyDelegsPredFailure ShelleyEra

instance InjectRuleFailure "DELEGS" ShelleyDelegsPredFailure ShelleyEra

instance InjectRuleFailure "DELEGS" ShelleyDelplPredFailure ShelleyEra where
  injectFailure :: ShelleyDelplPredFailure ShelleyEra
-> EraRuleFailure "DELEGS" ShelleyEra
injectFailure = PredicateFailure (EraRule "DELPL" ShelleyEra)
-> ShelleyDelegsPredFailure ShelleyEra
ShelleyDelplPredFailure ShelleyEra
-> EraRuleFailure "DELEGS" ShelleyEra
forall era.
PredicateFailure (EraRule "DELPL" era)
-> ShelleyDelegsPredFailure era
DelplFailure

instance InjectRuleFailure "DELEGS" ShelleyPoolPredFailure ShelleyEra where
  injectFailure :: ShelleyPoolPredFailure ShelleyEra
-> EraRuleFailure "DELEGS" ShelleyEra
injectFailure = PredicateFailure (EraRule "DELPL" ShelleyEra)
-> ShelleyDelegsPredFailure ShelleyEra
ShelleyDelplPredFailure ShelleyEra
-> ShelleyDelegsPredFailure ShelleyEra
forall era.
PredicateFailure (EraRule "DELPL" era)
-> ShelleyDelegsPredFailure era
DelplFailure (ShelleyDelplPredFailure ShelleyEra
 -> ShelleyDelegsPredFailure ShelleyEra)
-> (ShelleyPoolPredFailure ShelleyEra
    -> ShelleyDelplPredFailure ShelleyEra)
-> ShelleyPoolPredFailure ShelleyEra
-> ShelleyDelegsPredFailure ShelleyEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShelleyPoolPredFailure ShelleyEra
-> EraRuleFailure "DELPL" ShelleyEra
ShelleyPoolPredFailure ShelleyEra
-> ShelleyDelplPredFailure ShelleyEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "DELEGS" ShelleyDelegPredFailure ShelleyEra where
  injectFailure :: ShelleyDelegPredFailure ShelleyEra
-> EraRuleFailure "DELEGS" ShelleyEra
injectFailure = PredicateFailure (EraRule "DELPL" ShelleyEra)
-> ShelleyDelegsPredFailure ShelleyEra
ShelleyDelplPredFailure ShelleyEra
-> ShelleyDelegsPredFailure ShelleyEra
forall era.
PredicateFailure (EraRule "DELPL" era)
-> ShelleyDelegsPredFailure era
DelplFailure (ShelleyDelplPredFailure ShelleyEra
 -> ShelleyDelegsPredFailure ShelleyEra)
-> (ShelleyDelegPredFailure ShelleyEra
    -> ShelleyDelplPredFailure ShelleyEra)
-> ShelleyDelegPredFailure ShelleyEra
-> ShelleyDelegsPredFailure ShelleyEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShelleyDelegPredFailure ShelleyEra
-> EraRuleFailure "DELPL" ShelleyEra
ShelleyDelegPredFailure ShelleyEra
-> ShelleyDelplPredFailure ShelleyEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

newtype ShelleyDelegsEvent era = DelplEvent (Event (EraRule "DELPL" era))
  deriving ((forall x.
 ShelleyDelegsEvent era -> Rep (ShelleyDelegsEvent era) x)
-> (forall x.
    Rep (ShelleyDelegsEvent era) x -> ShelleyDelegsEvent era)
-> Generic (ShelleyDelegsEvent era)
forall x. Rep (ShelleyDelegsEvent era) x -> ShelleyDelegsEvent era
forall x. ShelleyDelegsEvent era -> Rep (ShelleyDelegsEvent era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyDelegsEvent era) x -> ShelleyDelegsEvent era
forall era x.
ShelleyDelegsEvent era -> Rep (ShelleyDelegsEvent era) x
$cfrom :: forall era x.
ShelleyDelegsEvent era -> Rep (ShelleyDelegsEvent era) x
from :: forall x. ShelleyDelegsEvent era -> Rep (ShelleyDelegsEvent era) x
$cto :: forall era x.
Rep (ShelleyDelegsEvent era) x -> ShelleyDelegsEvent era
to :: forall x. Rep (ShelleyDelegsEvent era) x -> ShelleyDelegsEvent era
Generic)

deriving instance Eq (Event (EraRule "DELPL" era)) => Eq (ShelleyDelegsEvent era)

instance NFData (Event (EraRule "DELPL" era)) => NFData (ShelleyDelegsEvent era)

deriving stock instance
  Show (PredicateFailure (EraRule "DELPL" era)) =>
  Show (ShelleyDelegsPredFailure era)

deriving stock instance
  Eq (PredicateFailure (EraRule "DELPL" era)) =>
  Eq (ShelleyDelegsPredFailure era)

instance
  NFData (PredicateFailure (EraRule "DELPL" era)) =>
  NFData (ShelleyDelegsPredFailure era)

instance
  ( EraTx era
  , EraCertState era
  , ShelleyEraTxBody era
  , Embed (EraRule "DELPL" era) (ShelleyDELEGS era)
  , Environment (EraRule "DELPL" era) ~ DelplEnv era
  , State (EraRule "DELPL" era) ~ CertState era
  , Signal (EraRule "DELPL" era) ~ TxCert era
  , EraRule "DELEGS" era ~ ShelleyDELEGS era
  ) =>
  STS (ShelleyDELEGS era)
  where
  type State (ShelleyDELEGS era) = CertState era
  type Signal (ShelleyDELEGS era) = Seq (TxCert era)
  type Environment (ShelleyDELEGS era) = DelegsEnv era
  type BaseM (ShelleyDELEGS era) = ShelleyBase
  type
    PredicateFailure (ShelleyDELEGS era) =
      ShelleyDelegsPredFailure era
  type Event (ShelleyDELEGS era) = ShelleyDelegsEvent era

  transitionRules :: [TransitionRule (ShelleyDELEGS era)]
transitionRules = [TransitionRule (ShelleyDELEGS era)
forall era.
(EraTx era, EraCertState era, ShelleyEraTxBody era,
 Embed (EraRule "DELPL" era) (ShelleyDELEGS era),
 Environment (EraRule "DELPL" era) ~ DelplEnv era,
 State (EraRule "DELPL" era) ~ CertState era,
 Signal (EraRule "DELPL" era) ~ TxCert era,
 EraRule "DELEGS" era ~ ShelleyDELEGS era) =>
TransitionRule (ShelleyDELEGS era)
delegsTransition]

instance
  NoThunks (PredicateFailure (EraRule "DELPL" era)) =>
  NoThunks (ShelleyDelegsPredFailure era)

instance
  ( Era era
  , EncCBOR (PredicateFailure (EraRule "DELPL" era))
  ) =>
  EncCBOR (ShelleyDelegsPredFailure era)
  where
  encCBOR :: ShelleyDelegsPredFailure era -> Encoding
encCBOR = \case
    DelegateeNotRegisteredDELEG 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
    (DelplFailure PredicateFailure (EraRule "DELPL" era)
a) ->
      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
1 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> PredicateFailure (EraRule "DELPL" era) -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR PredicateFailure (EraRule "DELPL" era)
a

instance
  ( Era era
  , DecCBOR (PredicateFailure (EraRule "DELPL" era))
  , Typeable (Script era)
  ) =>
  DecCBOR (ShelleyDelegsPredFailure era)
  where
  decCBOR :: forall s. Decoder s (ShelleyDelegsPredFailure era)
decCBOR =
    Text
-> (Word -> Decoder s (Int, ShelleyDelegsPredFailure era))
-> Decoder s (ShelleyDelegsPredFailure era)
forall s a. Text -> (Word -> Decoder s (Int, a)) -> Decoder s a
decodeRecordSum Text
"PredicateFailure" ((Word -> Decoder s (Int, ShelleyDelegsPredFailure era))
 -> Decoder s (ShelleyDelegsPredFailure era))
-> (Word -> Decoder s (Int, ShelleyDelegsPredFailure era))
-> Decoder s (ShelleyDelegsPredFailure 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, DelegateeNotRegisteredDELEG kh)
        Word
1 -> do
          a <- Decoder s (PredicateFailure (EraRule "DELPL" era))
forall s. Decoder s (PredicateFailure (EraRule "DELPL" era))
forall a s. DecCBOR a => Decoder s a
decCBOR
          pure (2, DelplFailure a)
        Word
k -> Word -> Decoder s (Int, ShelleyDelegsPredFailure era)
forall a (m :: * -> *). (Typeable a, MonadFail m) => Word -> m a
invalidKey Word
k

delegsTransition ::
  forall era.
  ( EraTx era
  , EraCertState era
  , ShelleyEraTxBody era
  , Embed (EraRule "DELPL" era) (ShelleyDELEGS era)
  , Environment (EraRule "DELPL" era) ~ DelplEnv era
  , State (EraRule "DELPL" era) ~ CertState era
  , Signal (EraRule "DELPL" era) ~ TxCert era
  , EraRule "DELEGS" era ~ ShelleyDELEGS era
  ) =>
  TransitionRule (ShelleyDELEGS era)
delegsTransition :: forall era.
(EraTx era, EraCertState era, ShelleyEraTxBody era,
 Embed (EraRule "DELPL" era) (ShelleyDELEGS era),
 Environment (EraRule "DELPL" era) ~ DelplEnv era,
 State (EraRule "DELPL" era) ~ CertState era,
 Signal (EraRule "DELPL" era) ~ TxCert era,
 EraRule "DELEGS" era ~ ShelleyDELEGS era) =>
TransitionRule (ShelleyDELEGS era)
delegsTransition = do
  TRC
    ( env@(DelegsEnv slot@(SlotNo slot64) epochNo txIx pp _tx chainAccountState)
      , certState
      , certificates
      ) <-
    Rule
  (ShelleyDELEGS era)
  'Transition
  (RuleContext 'Transition (ShelleyDELEGS era))
F (Clause (ShelleyDELEGS era) 'Transition)
  (TRC (ShelleyDELEGS era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  case certificates of
    Seq (TxCert era)
Signal (ShelleyDELEGS era)
Empty -> CertState era
-> F (Clause (ShelleyDELEGS era) 'Transition) (CertState era)
forall a. a -> F (Clause (ShelleyDELEGS era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CertState era
State (ShelleyDELEGS era)
certState
    Seq (TxCert era)
gamma :|> TxCert era
txCert -> do
      certState' <-
        forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(ShelleyDELEGS era) (RuleContext 'Transition (ShelleyDELEGS era)
 -> F (Clause (ShelleyDELEGS era) 'Transition)
      (State (ShelleyDELEGS era)))
-> RuleContext 'Transition (ShelleyDELEGS era)
-> F (Clause (ShelleyDELEGS era) 'Transition)
     (State (ShelleyDELEGS era))
forall a b. (a -> b) -> a -> b
$ (Environment (ShelleyDELEGS era), State (ShelleyDELEGS era),
 Signal (ShelleyDELEGS era))
-> TRC (ShelleyDELEGS era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment (ShelleyDELEGS era)
env, State (ShelleyDELEGS era)
certState, Seq (TxCert era)
Signal (ShelleyDELEGS era)
gamma)
      validateTrans DelegateeNotRegisteredDELEG $
        case txCert of
          DelegStakeTxCert Credential Staking
_ KeyHash StakePool
targetPool ->
            PState era
-> KeyHash StakePool
-> Validation (NonEmpty (KeyHash StakePool)) ()
forall era.
PState era
-> KeyHash StakePool
-> Validation (NonEmpty (KeyHash StakePool)) ()
validateStakePoolDelegateeRegistered (CertState era
certState' CertState era
-> Getting (PState era) (CertState era) (PState era) -> PState era
forall s a. s -> Getting a s a -> a
^. Getting (PState era) (CertState era) (PState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL) KeyHash StakePool
targetPool
          TxCert era
_ -> () -> Validation (NonEmpty (KeyHash StakePool)) ()
forall a. a -> Validation (NonEmpty (KeyHash StakePool)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      -- It is impossible to have 65535 number of certificates in a transaction.
      let certIx = Word16 -> CertIx
CertIx (forall a b. (Integral a, Num b) => a -> b
fromIntegral @Int @Word16 (Int -> Word16) -> Int -> Word16
forall a b. (a -> b) -> a -> b
$ Seq (TxCert era) -> Int
forall a. Seq a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq (TxCert era)
gamma)
          ptr = SlotNo32 -> TxIx -> CertIx -> Ptr
Ptr (Word32 -> SlotNo32
SlotNo32 (forall a b. (Integral a, Num b) => a -> b
fromIntegral @Word64 @Word32 Word64
slot64)) TxIx
txIx CertIx
certIx
      trans @(EraRule "DELPL" era) $
        TRC (DelplEnv slot epochNo ptr pp chainAccountState, certState', txCert)

validateStakePoolDelegateeRegistered ::
  PState era ->
  KeyHash StakePool ->
  Test (KeyHash StakePool)
validateStakePoolDelegateeRegistered :: forall era.
PState era
-> KeyHash StakePool
-> Validation (NonEmpty (KeyHash StakePool)) ()
validateStakePoolDelegateeRegistered PState era
pState KeyHash StakePool
targetPool =
  let stPools :: Map (KeyHash StakePool) StakePoolState
stPools = PState era -> Map (KeyHash StakePool) StakePoolState
forall era. PState era -> Map (KeyHash StakePool) StakePoolState
psStakePools PState era
pState
   in Bool
-> KeyHash StakePool
-> Validation (NonEmpty (KeyHash StakePool)) ()
forall e. Bool -> e -> Validation (NonEmpty e) ()
failureUnless (KeyHash StakePool -> Map (KeyHash StakePool) StakePoolState -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member KeyHash StakePool
targetPool Map (KeyHash StakePool) StakePoolState
stPools) KeyHash StakePool
targetPool

instance
  ( Era era
  , STS (ShelleyDELPL era)
  , PredicateFailure (EraRule "DELPL" era) ~ ShelleyDelplPredFailure era
  , Event (EraRule "DELPL" era) ~ ShelleyDelplEvent era
  ) =>
  Embed (ShelleyDELPL era) (ShelleyDELEGS era)
  where
  wrapFailed :: PredicateFailure (ShelleyDELPL era)
-> PredicateFailure (ShelleyDELEGS era)
wrapFailed = PredicateFailure (EraRule "DELPL" era)
-> ShelleyDelegsPredFailure era
PredicateFailure (ShelleyDELPL era)
-> PredicateFailure (ShelleyDELEGS era)
forall era.
PredicateFailure (EraRule "DELPL" era)
-> ShelleyDelegsPredFailure era
DelplFailure
  wrapEvent :: Event (ShelleyDELPL era) -> Event (ShelleyDELEGS era)
wrapEvent = Event (EraRule "DELPL" era) -> ShelleyDelegsEvent era
Event (ShelleyDELPL era) -> Event (ShelleyDELEGS era)
forall era. Event (EraRule "DELPL" era) -> ShelleyDelegsEvent era
DelplEvent