{-# 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.SetAlgebra (dom, eval, (∈))
import Control.State.Transition (
  Embed (..),
  STS (..),
  TRC (..),
  TransitionRule,
  judgmentContext,
  trans,
  validateTrans,
 )
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 StakeCredential
_ 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 (Exp Bool -> Bool
forall s t. Embed s t => Exp t -> s
eval (KeyHash StakePool
targetPool KeyHash StakePool -> Exp (Sett (KeyHash StakePool) ()) -> Exp Bool
forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∈ Map (KeyHash StakePool) StakePoolState
-> Exp (Sett (KeyHash StakePool) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom 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