{-# 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 (
  DELPL,
  DelplEnv (..),
  ShelleyDelplPredFailure (..),
  ShelleyDelplEvent,
) 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 (DELPL, ShelleyEra)
import Cardano.Ledger.Shelley.Rules.Deleg (
  DELEG,
  DelegEnv (..),
  ShelleyDelegEvent,
  ShelleyDelegPredFailure,
 )
import Cardano.Ledger.Shelley.Rules.Pool (POOL, PoolEnv (..), ShelleyPoolPredFailure)
import qualified Cardano.Ledger.Shelley.Rules.Pool as Pool
import Cardano.Ledger.Shelley.State
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 Lens.Micro ((&), (.~), (^.))

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

data ShelleyDelplPredFailure era
  = PoolFailure (PredicateFailure (EraRule "POOL" era)) -- Subtransition Failures
  | DelegFailure (PredicateFailure (EraRule "DELEG" era)) -- Subtransition Failures
  deriving ((forall x.
 ShelleyDelplPredFailure era -> Rep (ShelleyDelplPredFailure era) x)
-> (forall x.
    Rep (ShelleyDelplPredFailure era) x -> ShelleyDelplPredFailure era)
-> Generic (ShelleyDelplPredFailure era)
forall x.
Rep (ShelleyDelplPredFailure era) x -> ShelleyDelplPredFailure era
forall x.
ShelleyDelplPredFailure era -> Rep (ShelleyDelplPredFailure era) x
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
$cfrom :: forall era x.
ShelleyDelplPredFailure era -> Rep (ShelleyDelplPredFailure era) x
from :: forall x.
ShelleyDelplPredFailure era -> Rep (ShelleyDelplPredFailure era) x
$cto :: forall era x.
Rep (ShelleyDelplPredFailure era) x -> ShelleyDelplPredFailure era
to :: forall x.
Rep (ShelleyDelplPredFailure era) x -> ShelleyDelplPredFailure era
Generic)

type instance EraRuleFailure "DELPL" ShelleyEra = ShelleyDelplPredFailure ShelleyEra

instance InjectRuleFailure "DELPL" ShelleyDelplPredFailure ShelleyEra

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

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

data ShelleyDelplEvent era
  = PoolEvent (Event (EraRule "POOL" era))
  | DelegEvent (Event (EraRule "DELEG" era))
  deriving ((forall x. ShelleyDelplEvent era -> Rep (ShelleyDelplEvent era) x)
-> (forall x.
    Rep (ShelleyDelplEvent era) x -> ShelleyDelplEvent era)
-> Generic (ShelleyDelplEvent era)
forall x. Rep (ShelleyDelplEvent era) x -> ShelleyDelplEvent era
forall x. ShelleyDelplEvent era -> Rep (ShelleyDelplEvent era) x
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
$cfrom :: forall era x.
ShelleyDelplEvent era -> Rep (ShelleyDelplEvent era) x
from :: forall x. ShelleyDelplEvent era -> Rep (ShelleyDelplEvent era) x
$cto :: forall era x.
Rep (ShelleyDelplEvent era) x -> ShelleyDelplEvent era
to :: forall x. Rep (ShelleyDelplEvent era) x -> ShelleyDelplEvent era
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
  ( NFData (PredicateFailure (EraRule "DELEG" era))
  , NFData (PredicateFailure (EraRule "POOL" era))
  ) =>
  NFData (ShelleyDelplPredFailure era)

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

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

instance
  ( Era era
  , EncCBOR (PredicateFailure (EraRule "POOL" era))
  , EncCBOR (PredicateFailure (EraRule "DELEG" era))
  ) =>
  EncCBOR (ShelleyDelplPredFailure era)
  where
  encCBOR :: ShelleyDelplPredFailure era -> Encoding
encCBOR = \case
    (PoolFailure PredicateFailure (EraRule "POOL" 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
0 :: Word8)
        Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> PredicateFailure (EraRule "POOL" era) -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR PredicateFailure (EraRule "POOL" era)
a
    (DelegFailure PredicateFailure (EraRule "DELEG" 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 "DELEG" era) -> Encoding
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 =
    Text
-> (Word -> Decoder s (Int, ShelleyDelplPredFailure era))
-> Decoder s (ShelleyDelplPredFailure era)
forall s a. Text -> (Word -> Decoder s (Int, a)) -> Decoder s a
decodeRecordSum
      Text
"PredicateFailure (DELPL era)"
      ( \case
          Word
0 -> do
            a <- Decoder s (PredicateFailure (EraRule "POOL" era))
forall s. Decoder s (PredicateFailure (EraRule "POOL" era))
forall a s. DecCBOR a => Decoder s a
decCBOR
            pure (2, PoolFailure a)
          Word
1 -> do
            a <- Decoder s (PredicateFailure (EraRule "DELEG" era))
forall s. Decoder s (PredicateFailure (EraRule "DELEG" era))
forall a s. DecCBOR a => Decoder s a
decCBOR
            pure (2, DelegFailure a)
          Word
k -> Word -> Decoder s (Int, ShelleyDelplPredFailure era)
forall a (m :: * -> *). (Typeable a, MonadFail m) => Word -> m a
invalidKey Word
k
      )

delplTransition ::
  forall era.
  ( Embed (EraRule "DELEG" era) (DELPL era)
  , Environment (EraRule "DELEG" era) ~ DelegEnv era
  , State (EraRule "DELEG" era) ~ CertState era
  , State (EraRule "POOL" era) ~ PState era
  , Signal (EraRule "DELEG" era) ~ TxCert era
  , Embed (EraRule "POOL" era) (DELPL era)
  , Environment (EraRule "POOL" era) ~ PoolEnv era
  , Signal (EraRule "POOL" era) ~ PoolCert
  , TxCert era ~ ShelleyTxCert era
  , EraCertState era
  ) =>
  TransitionRule (DELPL era)
delplTransition :: forall era.
(Embed (EraRule "DELEG" era) (DELPL era),
 Environment (EraRule "DELEG" era) ~ DelegEnv era,
 State (EraRule "DELEG" era) ~ CertState era,
 State (EraRule "POOL" era) ~ PState era,
 Signal (EraRule "DELEG" era) ~ TxCert era,
 Embed (EraRule "POOL" era) (DELPL era),
 Environment (EraRule "POOL" era) ~ PoolEnv era,
 Signal (EraRule "POOL" era) ~ PoolCert,
 TxCert era ~ ShelleyTxCert era, EraCertState era) =>
TransitionRule (DELPL era)
delplTransition = do
  TRC (DelplEnv slot eNo ptr pp chainAccountState, d, c) <- Rule (DELPL era) 'Transition (RuleContext 'Transition (DELPL era))
F (Clause (DELPL era) 'Transition) (TRC (DELPL era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  case c of
    ShelleyTxCertPool PoolCert
poolCert -> do
      ps <-
        forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "POOL" era) (RuleContext 'Transition (EraRule "POOL" era)
 -> Rule (DELPL era) 'Transition (State (EraRule "POOL" era)))
-> RuleContext 'Transition (EraRule "POOL" era)
-> Rule (DELPL era) 'Transition (State (EraRule "POOL" era))
forall a b. (a -> b) -> a -> b
$ (Environment (EraRule "POOL" era), State (EraRule "POOL" era),
 Signal (EraRule "POOL" era))
-> TRC (EraRule "POOL" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (EpochNo -> PParams era -> PoolEnv era
forall era. EpochNo -> PParams era -> PoolEnv era
PoolEnv EpochNo
eNo PParams era
pp, CertState era
State (DELPL era)
d 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, PoolCert
Signal (EraRule "POOL" era)
poolCert)
      pure $ d & certPStateL .~ ps
    ShelleyTxCertGenesisDeleg GenesisDelegCert {} -> do
      forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "DELEG" era) (RuleContext 'Transition (EraRule "DELEG" era)
 -> Rule (DELPL era) 'Transition (State (EraRule "DELEG" era)))
-> RuleContext 'Transition (EraRule "DELEG" era)
-> Rule (DELPL era) 'Transition (State (EraRule "DELEG" era))
forall a b. (a -> b) -> a -> b
$
        (Environment (EraRule "DELEG" era), State (EraRule "DELEG" era),
 Signal (EraRule "DELEG" era))
-> TRC (EraRule "DELEG" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (SlotNo
-> EpochNo
-> Ptr
-> ChainAccountState
-> PParams era
-> DelegEnv era
forall era.
SlotNo
-> EpochNo
-> Ptr
-> ChainAccountState
-> PParams era
-> DelegEnv era
DelegEnv SlotNo
slot EpochNo
eNo Ptr
ptr ChainAccountState
chainAccountState PParams era
pp, State (EraRule "DELEG" era)
State (DELPL era)
d, Signal (EraRule "DELEG" era)
Signal (DELPL era)
c)
    ShelleyTxCertDelegCert ShelleyDelegCert
_ -> do
      forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "DELEG" era) (RuleContext 'Transition (EraRule "DELEG" era)
 -> Rule (DELPL era) 'Transition (State (EraRule "DELEG" era)))
-> RuleContext 'Transition (EraRule "DELEG" era)
-> Rule (DELPL era) 'Transition (State (EraRule "DELEG" era))
forall a b. (a -> b) -> a -> b
$
        (Environment (EraRule "DELEG" era), State (EraRule "DELEG" era),
 Signal (EraRule "DELEG" era))
-> TRC (EraRule "DELEG" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (SlotNo
-> EpochNo
-> Ptr
-> ChainAccountState
-> PParams era
-> DelegEnv era
forall era.
SlotNo
-> EpochNo
-> Ptr
-> ChainAccountState
-> PParams era
-> DelegEnv era
DelegEnv SlotNo
slot EpochNo
eNo Ptr
ptr ChainAccountState
chainAccountState PParams era
pp, State (EraRule "DELEG" era)
State (DELPL era)
d, Signal (EraRule "DELEG" era)
Signal (DELPL era)
c)
    ShelleyTxCertMir MIRCert
_ -> do
      forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "DELEG" era) (RuleContext 'Transition (EraRule "DELEG" era)
 -> Rule (DELPL era) 'Transition (State (EraRule "DELEG" era)))
-> RuleContext 'Transition (EraRule "DELEG" era)
-> Rule (DELPL era) 'Transition (State (EraRule "DELEG" era))
forall a b. (a -> b) -> a -> b
$
        (Environment (EraRule "DELEG" era), State (EraRule "DELEG" era),
 Signal (EraRule "DELEG" era))
-> TRC (EraRule "DELEG" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (SlotNo
-> EpochNo
-> Ptr
-> ChainAccountState
-> PParams era
-> DelegEnv era
forall era.
SlotNo
-> EpochNo
-> Ptr
-> ChainAccountState
-> PParams era
-> DelegEnv era
DelegEnv SlotNo
slot EpochNo
eNo Ptr
ptr ChainAccountState
chainAccountState PParams era
pp, State (EraRule "DELEG" era)
State (DELPL era)
d, Signal (EraRule "DELEG" era)
Signal (DELPL era)
c)

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

instance
  ( ShelleyEraAccounts era
  , ShelleyEraTxCert era
  , EraCertState era
  , EraPParams era
  , AtMostEra "Babbage" era
  , PredicateFailure (EraRule "DELEG" era) ~ ShelleyDelegPredFailure era
  , Event (EraRule "DELEG" era) ~ ShelleyDelegEvent era
  ) =>
  Embed (DELEG era) (DELPL era)
  where
  wrapFailed :: PredicateFailure (DELEG era) -> PredicateFailure (DELPL era)
wrapFailed = PredicateFailure (EraRule "DELEG" era)
-> ShelleyDelplPredFailure era
PredicateFailure (DELEG era) -> PredicateFailure (DELPL era)
forall era.
PredicateFailure (EraRule "DELEG" era)
-> ShelleyDelplPredFailure era
DelegFailure
  wrapEvent :: Event (DELEG era) -> Event (DELPL era)
wrapEvent = Event (EraRule "DELEG" era) -> ShelleyDelplEvent era
Event (DELEG era) -> Event (DELPL era)
forall era. Event (EraRule "DELEG" era) -> ShelleyDelplEvent era
DelegEvent