{-# 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.Delpl (
  ShelleyDELPL,
  DelplEnv (..),
  ShelleyDelplPredFailure (..),
  ShelleyDelplEvent,
  PredicateFailure,
)
where

import Cardano.Ledger.BaseTypes (EpochNo, ShelleyBase, invalidKey)
import Cardano.Ledger.Binary (
  DecCBOR (..),
  EncCBOR (..),
  decodeRecordSum,
  encodeListLen,
 )
import Cardano.Ledger.Credential (Ptr)
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.Era (ShelleyDELPL, ShelleyEra)
import Cardano.Ledger.Shelley.LedgerState (
  AccountState,
  CertState,
  DState,
  PState,
  certDState,
  certPState,
 )
import Cardano.Ledger.Shelley.Rules.Deleg (
  DelegEnv (..),
  ShelleyDELEG,
  ShelleyDelegEvent,
  ShelleyDelegPredFailure,
 )
import Cardano.Ledger.Shelley.Rules.Pool (PoolEnv (..), ShelleyPOOL, ShelleyPoolPredFailure)
import qualified Cardano.Ledger.Shelley.Rules.Pool as Pool
import Cardano.Ledger.Shelley.TxCert (GenesisDelegCert (..), ShelleyTxCert (..))
import Cardano.Ledger.Slot (SlotNo)
import Control.DeepSeq
import Control.State.Transition
import Data.Typeable (Typeable)
import Data.Word (Word8)
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))

data DelplEnv era = DelplEnv
  { forall era. DelplEnv era -> SlotNo
delplSlotNo :: SlotNo
  , forall era. DelplEnv era -> EpochNo
delpEpochNo :: EpochNo
  , forall era. DelplEnv era -> Ptr
delPlPtr :: Ptr
  , forall era. DelplEnv era -> PParams era
delPlPp :: PParams era
  , forall era. DelplEnv era -> AccountState
delPlAccount :: AccountState
  }

data ShelleyDelplPredFailure era
  = PoolFailure (PredicateFailure (EraRule "POOL" era)) -- Subtransition Failures
  | DelegFailure (PredicateFailure (EraRule "DELEG" era)) -- Subtransition Failures
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyDelplPredFailure era) x -> ShelleyDelplPredFailure era
forall era x.
ShelleyDelplPredFailure era -> Rep (ShelleyDelplPredFailure era) x
$cto :: forall era x.
Rep (ShelleyDelplPredFailure era) x -> ShelleyDelplPredFailure era
$cfrom :: forall era x.
ShelleyDelplPredFailure era -> Rep (ShelleyDelplPredFailure era) x
Generic)

type instance EraRuleFailure "DELPL" (ShelleyEra c) = ShelleyDelplPredFailure (ShelleyEra c)

instance InjectRuleFailure "DELPL" ShelleyDelplPredFailure (ShelleyEra c)

instance InjectRuleFailure "DELPL" ShelleyPoolPredFailure (ShelleyEra c) where
  injectFailure :: ShelleyPoolPredFailure (ShelleyEra c)
-> EraRuleFailure "DELPL" (ShelleyEra c)
injectFailure = forall era.
PredicateFailure (EraRule "POOL" era)
-> ShelleyDelplPredFailure era
PoolFailure

instance InjectRuleFailure "DELPL" ShelleyDelegPredFailure (ShelleyEra c) where
  injectFailure :: ShelleyDelegPredFailure (ShelleyEra c)
-> EraRuleFailure "DELPL" (ShelleyEra c)
injectFailure = forall era.
PredicateFailure (EraRule "DELEG" era)
-> ShelleyDelplPredFailure era
DelegFailure

data ShelleyDelplEvent era
  = PoolEvent (Event (EraRule "POOL" era))
  | DelegEvent (Event (EraRule "DELEG" era))
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyDelplEvent era) x -> ShelleyDelplEvent era
forall era x.
ShelleyDelplEvent era -> Rep (ShelleyDelplEvent era) x
$cto :: forall era x.
Rep (ShelleyDelplEvent era) x -> ShelleyDelplEvent era
$cfrom :: forall era x.
ShelleyDelplEvent era -> Rep (ShelleyDelplEvent era) x
Generic)

instance
  ( NFData (Event (EraRule "DELEG" era))
  , NFData (Event (EraRule "POOL" era))
  ) =>
  NFData (ShelleyDelplEvent era)

deriving instance
  ( Eq (Event (EraRule "DELEG" era))
  , Eq (Event (EraRule "POOL" era))
  ) =>
  Eq (ShelleyDelplEvent era)

deriving stock instance
  ( Eq (PredicateFailure (EraRule "DELEG" era))
  , Eq (PredicateFailure (EraRule "POOL" era))
  ) =>
  Eq (ShelleyDelplPredFailure era)

deriving stock instance
  ( Show (PredicateFailure (EraRule "DELEG" era))
  , Show (PredicateFailure (EraRule "POOL" era))
  ) =>
  Show (ShelleyDelplPredFailure era)

instance
  ( NoThunks (PredicateFailure (EraRule "DELEG" era))
  , NoThunks (PredicateFailure (EraRule "POOL" era))
  ) =>
  NoThunks (ShelleyDelplPredFailure era)

instance
  ( NFData (PredicateFailure (EraRule "DELEG" era))
  , NFData (PredicateFailure (EraRule "POOL" era))
  ) =>
  NFData (ShelleyDelplPredFailure era)

instance
  ( Era era
  , Embed (EraRule "DELEG" era) (ShelleyDELPL era)
  , Environment (EraRule "DELEG" era) ~ DelegEnv era
  , State (EraRule "DELEG" era) ~ DState era
  , Embed (EraRule "POOL" era) (ShelleyDELPL era)
  , Environment (EraRule "POOL" era) ~ PoolEnv era
  , State (EraRule "POOL" era) ~ PState era
  , Signal (EraRule "DELEG" era) ~ TxCert era
  , Embed (EraRule "POOL" era) (ShelleyDELPL era)
  , Environment (EraRule "POOL" era) ~ PoolEnv era
  , Signal (EraRule "POOL" era) ~ PoolCert (EraCrypto era)
  , TxCert era ~ ShelleyTxCert era
  ) =>
  STS (ShelleyDELPL era)
  where
  type State (ShelleyDELPL era) = CertState era
  type Signal (ShelleyDELPL era) = TxCert era
  type Environment (ShelleyDELPL era) = DelplEnv era
  type BaseM (ShelleyDELPL era) = ShelleyBase
  type PredicateFailure (ShelleyDELPL era) = ShelleyDelplPredFailure era
  type Event (ShelleyDELPL era) = ShelleyDelplEvent era

  transitionRules :: [TransitionRule (ShelleyDELPL era)]
transitionRules = [forall era.
(Embed (EraRule "DELEG" era) (ShelleyDELPL era),
 Environment (EraRule "DELEG" era) ~ DelegEnv era,
 State (EraRule "DELEG" era) ~ DState era,
 State (EraRule "POOL" era) ~ PState era,
 Signal (EraRule "DELEG" era) ~ TxCert era,
 Embed (EraRule "POOL" era) (ShelleyDELPL era),
 Environment (EraRule "POOL" era) ~ PoolEnv era,
 Signal (EraRule "POOL" era) ~ PoolCert (EraCrypto era),
 TxCert era ~ ShelleyTxCert era) =>
TransitionRule (ShelleyDELPL era)
delplTransition]

instance
  ( Era era
  , EncCBOR (PredicateFailure (EraRule "POOL" era))
  , EncCBOR (PredicateFailure (EraRule "DELEG" era))
  , Typeable (Script era)
  ) =>
  EncCBOR (ShelleyDelplPredFailure era)
  where
  encCBOR :: ShelleyDelplPredFailure era -> Encoding
encCBOR = \case
    (PoolFailure PredicateFailure (EraRule "POOL" era)
a) ->
      Word -> Encoding
encodeListLen Word
2
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
0 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR PredicateFailure (EraRule "POOL" era)
a
    (DelegFailure PredicateFailure (EraRule "DELEG" era)
a) ->
      Word -> Encoding
encodeListLen Word
2
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR (Word8
1 :: Word8)
        forall a. Semigroup a => a -> a -> a
<> forall a. EncCBOR a => a -> Encoding
encCBOR PredicateFailure (EraRule "DELEG" era)
a

instance
  ( Era era
  , DecCBOR (PredicateFailure (EraRule "POOL" era))
  , DecCBOR (PredicateFailure (EraRule "DELEG" era))
  , Typeable (Script era)
  ) =>
  DecCBOR (ShelleyDelplPredFailure era)
  where
  decCBOR :: forall s. Decoder s (ShelleyDelplPredFailure era)
decCBOR =
    forall s a. Text -> (Word -> Decoder s (Int, a)) -> Decoder s a
decodeRecordSum
      Text
"PredicateFailure (DELPL era)"
      ( \case
          Word
0 -> do
            PredicateFailure (EraRule "POOL" era)
a <- forall a s. DecCBOR a => Decoder s a
decCBOR
            forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era.
PredicateFailure (EraRule "POOL" era)
-> ShelleyDelplPredFailure era
PoolFailure PredicateFailure (EraRule "POOL" era)
a)
          Word
1 -> do
            PredicateFailure (EraRule "DELEG" era)
a <- forall a s. DecCBOR a => Decoder s a
decCBOR
            forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, forall era.
PredicateFailure (EraRule "DELEG" era)
-> ShelleyDelplPredFailure era
DelegFailure PredicateFailure (EraRule "DELEG" era)
a)
          Word
k -> forall (m :: * -> *) a. MonadFail m => Word -> m a
invalidKey Word
k
      )

delplTransition ::
  forall era.
  ( Embed (EraRule "DELEG" era) (ShelleyDELPL era)
  , Environment (EraRule "DELEG" era) ~ DelegEnv era
  , State (EraRule "DELEG" era) ~ DState era
  , State (EraRule "POOL" era) ~ PState era
  , Signal (EraRule "DELEG" era) ~ TxCert era
  , Embed (EraRule "POOL" era) (ShelleyDELPL era)
  , Environment (EraRule "POOL" era) ~ PoolEnv era
  , Signal (EraRule "POOL" era) ~ PoolCert (EraCrypto era)
  , TxCert era ~ ShelleyTxCert era
  ) =>
  TransitionRule (ShelleyDELPL era)
delplTransition :: forall era.
(Embed (EraRule "DELEG" era) (ShelleyDELPL era),
 Environment (EraRule "DELEG" era) ~ DelegEnv era,
 State (EraRule "DELEG" era) ~ DState era,
 State (EraRule "POOL" era) ~ PState era,
 Signal (EraRule "DELEG" era) ~ TxCert era,
 Embed (EraRule "POOL" era) (ShelleyDELPL era),
 Environment (EraRule "POOL" era) ~ PoolEnv era,
 Signal (EraRule "POOL" era) ~ PoolCert (EraCrypto era),
 TxCert era ~ ShelleyTxCert era) =>
TransitionRule (ShelleyDELPL era)
delplTransition = do
  TRC (DelplEnv SlotNo
slot EpochNo
eNo Ptr
ptr PParams era
pp AccountState
acnt, State (ShelleyDELPL era)
d, Signal (ShelleyDELPL era)
c) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  case Signal (ShelleyDELPL era)
c of
    ShelleyTxCertPool PoolCert (EraCrypto era)
poolCert -> do
      PState era
ps <-
        forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "POOL" era) forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (forall era. EpochNo -> PParams era -> PoolEnv era
PoolEnv EpochNo
eNo PParams era
pp, forall era. CertState era -> PState era
certPState State (ShelleyDELPL era)
d, PoolCert (EraCrypto era)
poolCert)
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ State (ShelleyDELPL era)
d {certPState :: PState era
certPState = PState era
ps}
    ShelleyTxCertGenesisDeleg GenesisDelegCert {} -> do
      DState era
ds <-
        forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "DELEG" era) forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (forall era.
SlotNo
-> EpochNo -> Ptr -> AccountState -> PParams era -> DelegEnv era
DelegEnv SlotNo
slot EpochNo
eNo Ptr
ptr AccountState
acnt PParams era
pp, forall era. CertState era -> DState era
certDState State (ShelleyDELPL era)
d, Signal (ShelleyDELPL era)
c)
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ State (ShelleyDELPL era)
d {certDState :: DState era
certDState = DState era
ds}
    ShelleyTxCertDelegCert ShelleyDelegCert (EraCrypto era)
_ -> do
      DState era
ds <-
        forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "DELEG" era) forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (forall era.
SlotNo
-> EpochNo -> Ptr -> AccountState -> PParams era -> DelegEnv era
DelegEnv SlotNo
slot EpochNo
eNo Ptr
ptr AccountState
acnt PParams era
pp, forall era. CertState era -> DState era
certDState State (ShelleyDELPL era)
d, Signal (ShelleyDELPL era)
c)
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ State (ShelleyDELPL era)
d {certDState :: DState era
certDState = DState era
ds}
    ShelleyTxCertMir MIRCert (EraCrypto era)
_ -> do
      DState era
ds <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "DELEG" era) forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (forall era.
SlotNo
-> EpochNo -> Ptr -> AccountState -> PParams era -> DelegEnv era
DelegEnv SlotNo
slot EpochNo
eNo Ptr
ptr AccountState
acnt PParams era
pp, forall era. CertState era -> DState era
certDState State (ShelleyDELPL era)
d, Signal (ShelleyDELPL era)
c)
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ State (ShelleyDELPL era)
d {certDState :: DState era
certDState = DState era
ds}

instance
  ( Era era
  , STS (ShelleyPOOL era)
  , PredicateFailure (EraRule "POOL" era) ~ ShelleyPoolPredFailure era
  , Event (EraRule "POOL" era) ~ Pool.PoolEvent era
  ) =>
  Embed (ShelleyPOOL era) (ShelleyDELPL era)
  where
  wrapFailed :: PredicateFailure (ShelleyPOOL era)
-> PredicateFailure (ShelleyDELPL era)
wrapFailed = forall era.
PredicateFailure (EraRule "POOL" era)
-> ShelleyDelplPredFailure era
PoolFailure
  wrapEvent :: Event (ShelleyPOOL era) -> Event (ShelleyDELPL era)
wrapEvent = forall era. Event (EraRule "POOL" era) -> ShelleyDelplEvent era
PoolEvent

instance
  ( ShelleyEraTxCert era
  , EraPParams era
  , ProtVerAtMost era 8
  , PredicateFailure (EraRule "DELEG" era) ~ ShelleyDelegPredFailure era
  , Event (EraRule "DELEG" era) ~ ShelleyDelegEvent era
  ) =>
  Embed (ShelleyDELEG era) (ShelleyDELPL era)
  where
  wrapFailed :: PredicateFailure (ShelleyDELEG era)
-> PredicateFailure (ShelleyDELPL era)
wrapFailed = forall era.
PredicateFailure (EraRule "DELEG" era)
-> ShelleyDelplPredFailure era
DelegFailure
  wrapEvent :: Event (ShelleyDELEG era) -> Event (ShelleyDELPL era)
wrapEvent = forall era. Event (EraRule "DELEG" era) -> ShelleyDelplEvent era
DelegEvent