{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Cardano.Ledger.Alonzo.Rules.Ledger (
  AlonzoLEDGER,
  ledgerTransition,
) where

import Cardano.Ledger.Allegra.Rules (AllegraUtxoPredFailure)
import Cardano.Ledger.Alonzo.Era (AlonzoEra, AlonzoLEDGER)
import Cardano.Ledger.Alonzo.Rules.Delegs ()
import Cardano.Ledger.Alonzo.Rules.Utxo (AlonzoUtxoPredFailure)
import Cardano.Ledger.Alonzo.Rules.Utxos (AlonzoUtxosPredFailure)
import Cardano.Ledger.Alonzo.Rules.Utxow (AlonzoUTXOW, AlonzoUtxowEvent, AlonzoUtxowPredFailure)
import Cardano.Ledger.Alonzo.Tx (AlonzoEraTx (..), IsValid (..))
import Cardano.Ledger.BaseTypes (ShelleyBase)
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.LedgerState (
  CertState,
  LedgerState (..),
  UTxOState (..),
 )
import Cardano.Ledger.Shelley.Rules (
  DelegsEnv (..),
  ShelleyDELEGS,
  ShelleyDelegPredFailure,
  ShelleyDelegsEvent,
  ShelleyDelegsPredFailure,
  ShelleyDelplPredFailure (..),
  ShelleyLEDGERS,
  ShelleyPoolPredFailure,
  ShelleyPpupPredFailure,
  ShelleyUtxoPredFailure,
  ShelleyUtxowPredFailure,
  UtxoEnv (..),
  shelleyLedgerAssertions,
  testIncompleteAndMissingWithdrawals,
 )
import Cardano.Ledger.Shelley.Rules as Shelley (
  LedgerEnv (..),
  ShelleyLedgerEvent (..),
  ShelleyLedgerPredFailure (..),
  ShelleyLedgersEvent (..),
  ShelleyLedgersPredFailure (..),
  renderDepositEqualsObligationViolation,
 )
import Cardano.Ledger.Slot (epochFromSlot)
import Cardano.Ledger.State (EraCertState, accountsL, certDStateL, drainAccounts)
import Control.State.Transition (
  Embed (..),
  STS (..),
  TRC (..),
  TransitionRule,
  judgmentContext,
  liftSTS,
  trans,
 )
import Data.Kind (Type)
import Data.Sequence (Seq)
import qualified Data.Sequence.Strict as StrictSeq
import Lens.Micro

type instance EraRuleFailure "LEDGER" AlonzoEra = ShelleyLedgerPredFailure AlonzoEra

instance InjectRuleFailure "LEDGER" ShelleyLedgerPredFailure AlonzoEra

instance InjectRuleFailure "LEDGER" AlonzoUtxowPredFailure AlonzoEra where
  injectFailure :: AlonzoUtxowPredFailure AlonzoEra
-> EraRuleFailure "LEDGER" AlonzoEra
injectFailure = PredicateFailure (EraRule "UTXOW" AlonzoEra)
-> ShelleyLedgerPredFailure AlonzoEra
AlonzoUtxowPredFailure AlonzoEra
-> EraRuleFailure "LEDGER" AlonzoEra
forall era.
PredicateFailure (EraRule "UTXOW" era)
-> ShelleyLedgerPredFailure era
UtxowFailure

instance InjectRuleFailure "LEDGER" ShelleyUtxowPredFailure AlonzoEra where
  injectFailure :: ShelleyUtxowPredFailure AlonzoEra
-> EraRuleFailure "LEDGER" AlonzoEra
injectFailure = PredicateFailure (EraRule "UTXOW" AlonzoEra)
-> ShelleyLedgerPredFailure AlonzoEra
AlonzoUtxowPredFailure AlonzoEra
-> ShelleyLedgerPredFailure AlonzoEra
forall era.
PredicateFailure (EraRule "UTXOW" era)
-> ShelleyLedgerPredFailure era
UtxowFailure (AlonzoUtxowPredFailure AlonzoEra
 -> ShelleyLedgerPredFailure AlonzoEra)
-> (ShelleyUtxowPredFailure AlonzoEra
    -> AlonzoUtxowPredFailure AlonzoEra)
-> ShelleyUtxowPredFailure AlonzoEra
-> ShelleyLedgerPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShelleyUtxowPredFailure AlonzoEra
-> EraRuleFailure "UTXOW" AlonzoEra
ShelleyUtxowPredFailure AlonzoEra
-> AlonzoUtxowPredFailure AlonzoEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "LEDGER" AlonzoUtxoPredFailure AlonzoEra where
  injectFailure :: AlonzoUtxoPredFailure AlonzoEra
-> EraRuleFailure "LEDGER" AlonzoEra
injectFailure = PredicateFailure (EraRule "UTXOW" AlonzoEra)
-> ShelleyLedgerPredFailure AlonzoEra
AlonzoUtxowPredFailure AlonzoEra
-> ShelleyLedgerPredFailure AlonzoEra
forall era.
PredicateFailure (EraRule "UTXOW" era)
-> ShelleyLedgerPredFailure era
UtxowFailure (AlonzoUtxowPredFailure AlonzoEra
 -> ShelleyLedgerPredFailure AlonzoEra)
-> (AlonzoUtxoPredFailure AlonzoEra
    -> AlonzoUtxowPredFailure AlonzoEra)
-> AlonzoUtxoPredFailure AlonzoEra
-> ShelleyLedgerPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlonzoUtxoPredFailure AlonzoEra -> EraRuleFailure "UTXOW" AlonzoEra
AlonzoUtxoPredFailure AlonzoEra -> AlonzoUtxowPredFailure AlonzoEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "LEDGER" AlonzoUtxosPredFailure AlonzoEra where
  injectFailure :: AlonzoUtxosPredFailure AlonzoEra
-> EraRuleFailure "LEDGER" AlonzoEra
injectFailure = PredicateFailure (EraRule "UTXOW" AlonzoEra)
-> ShelleyLedgerPredFailure AlonzoEra
AlonzoUtxowPredFailure AlonzoEra
-> ShelleyLedgerPredFailure AlonzoEra
forall era.
PredicateFailure (EraRule "UTXOW" era)
-> ShelleyLedgerPredFailure era
UtxowFailure (AlonzoUtxowPredFailure AlonzoEra
 -> ShelleyLedgerPredFailure AlonzoEra)
-> (AlonzoUtxosPredFailure AlonzoEra
    -> AlonzoUtxowPredFailure AlonzoEra)
-> AlonzoUtxosPredFailure AlonzoEra
-> ShelleyLedgerPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlonzoUtxosPredFailure AlonzoEra
-> EraRuleFailure "UTXOW" AlonzoEra
AlonzoUtxosPredFailure AlonzoEra
-> AlonzoUtxowPredFailure AlonzoEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "LEDGER" ShelleyPpupPredFailure AlonzoEra where
  injectFailure :: ShelleyPpupPredFailure AlonzoEra
-> EraRuleFailure "LEDGER" AlonzoEra
injectFailure = PredicateFailure (EraRule "UTXOW" AlonzoEra)
-> ShelleyLedgerPredFailure AlonzoEra
AlonzoUtxowPredFailure AlonzoEra
-> ShelleyLedgerPredFailure AlonzoEra
forall era.
PredicateFailure (EraRule "UTXOW" era)
-> ShelleyLedgerPredFailure era
UtxowFailure (AlonzoUtxowPredFailure AlonzoEra
 -> ShelleyLedgerPredFailure AlonzoEra)
-> (ShelleyPpupPredFailure AlonzoEra
    -> AlonzoUtxowPredFailure AlonzoEra)
-> ShelleyPpupPredFailure AlonzoEra
-> ShelleyLedgerPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShelleyPpupPredFailure AlonzoEra
-> EraRuleFailure "UTXOW" AlonzoEra
ShelleyPpupPredFailure AlonzoEra
-> AlonzoUtxowPredFailure AlonzoEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "LEDGER" ShelleyUtxoPredFailure AlonzoEra where
  injectFailure :: ShelleyUtxoPredFailure AlonzoEra
-> EraRuleFailure "LEDGER" AlonzoEra
injectFailure = PredicateFailure (EraRule "UTXOW" AlonzoEra)
-> ShelleyLedgerPredFailure AlonzoEra
AlonzoUtxowPredFailure AlonzoEra
-> ShelleyLedgerPredFailure AlonzoEra
forall era.
PredicateFailure (EraRule "UTXOW" era)
-> ShelleyLedgerPredFailure era
UtxowFailure (AlonzoUtxowPredFailure AlonzoEra
 -> ShelleyLedgerPredFailure AlonzoEra)
-> (ShelleyUtxoPredFailure AlonzoEra
    -> AlonzoUtxowPredFailure AlonzoEra)
-> ShelleyUtxoPredFailure AlonzoEra
-> ShelleyLedgerPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShelleyUtxoPredFailure AlonzoEra
-> EraRuleFailure "UTXOW" AlonzoEra
ShelleyUtxoPredFailure AlonzoEra
-> AlonzoUtxowPredFailure AlonzoEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "LEDGER" AllegraUtxoPredFailure AlonzoEra where
  injectFailure :: AllegraUtxoPredFailure AlonzoEra
-> EraRuleFailure "LEDGER" AlonzoEra
injectFailure = PredicateFailure (EraRule "UTXOW" AlonzoEra)
-> ShelleyLedgerPredFailure AlonzoEra
AlonzoUtxowPredFailure AlonzoEra
-> ShelleyLedgerPredFailure AlonzoEra
forall era.
PredicateFailure (EraRule "UTXOW" era)
-> ShelleyLedgerPredFailure era
UtxowFailure (AlonzoUtxowPredFailure AlonzoEra
 -> ShelleyLedgerPredFailure AlonzoEra)
-> (AllegraUtxoPredFailure AlonzoEra
    -> AlonzoUtxowPredFailure AlonzoEra)
-> AllegraUtxoPredFailure AlonzoEra
-> ShelleyLedgerPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AllegraUtxoPredFailure AlonzoEra
-> EraRuleFailure "UTXOW" AlonzoEra
AllegraUtxoPredFailure AlonzoEra
-> AlonzoUtxowPredFailure AlonzoEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "LEDGER" ShelleyDelegsPredFailure AlonzoEra where
  injectFailure :: ShelleyDelegsPredFailure AlonzoEra
-> EraRuleFailure "LEDGER" AlonzoEra
injectFailure = PredicateFailure (EraRule "DELEGS" AlonzoEra)
-> ShelleyLedgerPredFailure AlonzoEra
ShelleyDelegsPredFailure AlonzoEra
-> EraRuleFailure "LEDGER" AlonzoEra
forall era.
PredicateFailure (EraRule "DELEGS" era)
-> ShelleyLedgerPredFailure era
DelegsFailure

instance InjectRuleFailure "LEDGER" ShelleyDelplPredFailure AlonzoEra where
  injectFailure :: ShelleyDelplPredFailure AlonzoEra
-> EraRuleFailure "LEDGER" AlonzoEra
injectFailure = PredicateFailure (EraRule "DELEGS" AlonzoEra)
-> ShelleyLedgerPredFailure AlonzoEra
ShelleyDelegsPredFailure AlonzoEra
-> ShelleyLedgerPredFailure AlonzoEra
forall era.
PredicateFailure (EraRule "DELEGS" era)
-> ShelleyLedgerPredFailure era
DelegsFailure (ShelleyDelegsPredFailure AlonzoEra
 -> ShelleyLedgerPredFailure AlonzoEra)
-> (ShelleyDelplPredFailure AlonzoEra
    -> ShelleyDelegsPredFailure AlonzoEra)
-> ShelleyDelplPredFailure AlonzoEra
-> ShelleyLedgerPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShelleyDelplPredFailure AlonzoEra
-> EraRuleFailure "DELEGS" AlonzoEra
ShelleyDelplPredFailure AlonzoEra
-> ShelleyDelegsPredFailure AlonzoEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "LEDGER" ShelleyPoolPredFailure AlonzoEra where
  injectFailure :: ShelleyPoolPredFailure AlonzoEra
-> EraRuleFailure "LEDGER" AlonzoEra
injectFailure = PredicateFailure (EraRule "DELEGS" AlonzoEra)
-> ShelleyLedgerPredFailure AlonzoEra
ShelleyDelegsPredFailure AlonzoEra
-> ShelleyLedgerPredFailure AlonzoEra
forall era.
PredicateFailure (EraRule "DELEGS" era)
-> ShelleyLedgerPredFailure era
DelegsFailure (ShelleyDelegsPredFailure AlonzoEra
 -> ShelleyLedgerPredFailure AlonzoEra)
-> (ShelleyPoolPredFailure AlonzoEra
    -> ShelleyDelegsPredFailure AlonzoEra)
-> ShelleyPoolPredFailure AlonzoEra
-> ShelleyLedgerPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShelleyPoolPredFailure AlonzoEra
-> EraRuleFailure "DELEGS" AlonzoEra
ShelleyPoolPredFailure AlonzoEra
-> ShelleyDelegsPredFailure AlonzoEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "LEDGER" ShelleyDelegPredFailure AlonzoEra where
  injectFailure :: ShelleyDelegPredFailure AlonzoEra
-> EraRuleFailure "LEDGER" AlonzoEra
injectFailure = PredicateFailure (EraRule "DELEGS" AlonzoEra)
-> ShelleyLedgerPredFailure AlonzoEra
ShelleyDelegsPredFailure AlonzoEra
-> ShelleyLedgerPredFailure AlonzoEra
forall era.
PredicateFailure (EraRule "DELEGS" era)
-> ShelleyLedgerPredFailure era
DelegsFailure (ShelleyDelegsPredFailure AlonzoEra
 -> ShelleyLedgerPredFailure AlonzoEra)
-> (ShelleyDelegPredFailure AlonzoEra
    -> ShelleyDelegsPredFailure AlonzoEra)
-> ShelleyDelegPredFailure AlonzoEra
-> ShelleyLedgerPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShelleyDelegPredFailure AlonzoEra
-> EraRuleFailure "DELEGS" AlonzoEra
ShelleyDelegPredFailure AlonzoEra
-> ShelleyDelegsPredFailure AlonzoEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

-- =======================================

-- | An abstract Alonzo Era, Ledger transition. Fix 'someLedger' at a concrete type to
--   make it concrete.
ledgerTransition ::
  forall (someLEDGER :: Type -> Type) era.
  ( STS (someLEDGER era)
  , BaseM (someLEDGER era) ~ ShelleyBase
  , Signal (someLEDGER era) ~ Tx TopTx era
  , State (someLEDGER era) ~ LedgerState era
  , Environment (someLEDGER era) ~ LedgerEnv era
  , Embed (EraRule "UTXOW" era) (someLEDGER era)
  , Embed (EraRule "DELEGS" era) (someLEDGER era)
  , Environment (EraRule "DELEGS" era) ~ DelegsEnv era
  , State (EraRule "DELEGS" era) ~ CertState era
  , Signal (EraRule "DELEGS" era) ~ Seq (TxCert era)
  , Environment (EraRule "UTXOW" era) ~ UtxoEnv era
  , State (EraRule "UTXOW" era) ~ UTxOState era
  , Signal (EraRule "UTXOW" era) ~ Tx TopTx era
  , AlonzoEraTx era
  , EraCertState era
  , EraRule "LEDGER" era ~ someLEDGER era
  , InjectRuleFailure "LEDGER" ShelleyLedgerPredFailure era
  ) =>
  TransitionRule (someLEDGER era)
ledgerTransition :: forall (someLEDGER :: * -> *) era.
(STS (someLEDGER era), BaseM (someLEDGER era) ~ ShelleyBase,
 Signal (someLEDGER era) ~ Tx TopTx era,
 State (someLEDGER era) ~ LedgerState era,
 Environment (someLEDGER era) ~ LedgerEnv era,
 Embed (EraRule "UTXOW" era) (someLEDGER era),
 Embed (EraRule "DELEGS" era) (someLEDGER era),
 Environment (EraRule "DELEGS" era) ~ DelegsEnv era,
 State (EraRule "DELEGS" era) ~ CertState era,
 Signal (EraRule "DELEGS" era) ~ Seq (TxCert era),
 Environment (EraRule "UTXOW" era) ~ UtxoEnv era,
 State (EraRule "UTXOW" era) ~ UTxOState era,
 Signal (EraRule "UTXOW" era) ~ Tx TopTx era, AlonzoEraTx era,
 EraCertState era, EraRule "LEDGER" era ~ someLEDGER era,
 InjectRuleFailure "LEDGER" ShelleyLedgerPredFailure era) =>
TransitionRule (someLEDGER era)
ledgerTransition = do
  TRC (LedgerEnv slot mbCurEpochNo txIx pp account, LedgerState utxoSt certState, tx) <-
    Rule
  (someLEDGER era)
  'Transition
  (RuleContext 'Transition (someLEDGER era))
F (Clause (someLEDGER era) 'Transition) (TRC (someLEDGER era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  let txBody = Tx TopTx era
Signal (someLEDGER era)
tx Tx TopTx era
-> Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
-> TxBody TopTx era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l era)
bodyTxL

  curEpochNo <- maybe (liftSTS $ epochFromSlot slot) pure mbCurEpochNo

  certState' <-
    if tx ^. isValidTxL == IsValid True
      then do
        let withdrawals = Tx TopTx era
Signal (someLEDGER era)
tx Tx TopTx era
-> Getting Withdrawals (Tx TopTx era) Withdrawals -> Withdrawals
forall s a. s -> Getting a s a -> a
^. (TxBody TopTx era -> Const Withdrawals (TxBody TopTx era))
-> Tx TopTx era -> Const Withdrawals (Tx TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l era)
bodyTxL ((TxBody TopTx era -> Const Withdrawals (TxBody TopTx era))
 -> Tx TopTx era -> Const Withdrawals (Tx TopTx era))
-> ((Withdrawals -> Const Withdrawals Withdrawals)
    -> TxBody TopTx era -> Const Withdrawals (TxBody TopTx era))
-> Getting Withdrawals (Tx TopTx era) Withdrawals
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Withdrawals -> Const Withdrawals Withdrawals)
-> TxBody TopTx era -> Const Withdrawals (TxBody TopTx era)
forall era (l :: TxLevel).
EraTxBody era =>
Lens' (TxBody l era) Withdrawals
forall (l :: TxLevel). Lens' (TxBody l era) Withdrawals
withdrawalsTxBodyL
        testIncompleteAndMissingWithdrawals (certState ^. certDStateL . accountsL) withdrawals
        trans @(EraRule "DELEGS" era) $
          TRC
            ( DelegsEnv slot curEpochNo txIx pp tx account
            , certState & certDStateL . accountsL %~ drainAccounts withdrawals
            , StrictSeq.fromStrict $ txBody ^. certsTxBodyL
            )
      else pure certState

  utxoSt' <-
    trans @(EraRule "UTXOW" era) $
      TRC
        ( UtxoEnv @era slot pp certState
        , utxoSt
        , tx
        )
  pure $ LedgerState utxoSt' certState'

instance
  ( AlonzoEraTx era
  , EraGov era
  , Embed (EraRule "DELEGS" era) (AlonzoLEDGER era)
  , Embed (EraRule "UTXOW" era) (AlonzoLEDGER era)
  , Environment (EraRule "UTXOW" era) ~ UtxoEnv era
  , State (EraRule "UTXOW" era) ~ UTxOState era
  , Signal (EraRule "UTXOW" era) ~ Tx TopTx era
  , Environment (EraRule "DELEGS" era) ~ DelegsEnv era
  , State (EraRule "DELEGS" era) ~ CertState era
  , Signal (EraRule "DELEGS" era) ~ Seq (TxCert era)
  , AtMostEra "Babbage" era
  , EraRule "LEDGER" era ~ AlonzoLEDGER era
  , EraRuleFailure "LEDGER" era ~ ShelleyLedgerPredFailure era
  , InjectRuleFailure "LEDGER" ShelleyLedgerPredFailure era
  , EraCertState era
  ) =>
  STS (AlonzoLEDGER era)
  where
  type State (AlonzoLEDGER era) = LedgerState era
  type Signal (AlonzoLEDGER era) = Tx TopTx era
  type Environment (AlonzoLEDGER era) = LedgerEnv era
  type BaseM (AlonzoLEDGER era) = ShelleyBase
  type PredicateFailure (AlonzoLEDGER era) = ShelleyLedgerPredFailure era
  type Event (AlonzoLEDGER era) = ShelleyLedgerEvent era

  initialRules :: [InitialRule (AlonzoLEDGER era)]
initialRules = []
  transitionRules :: [TransitionRule (AlonzoLEDGER era)]
transitionRules = [forall (someLEDGER :: * -> *) era.
(STS (someLEDGER era), BaseM (someLEDGER era) ~ ShelleyBase,
 Signal (someLEDGER era) ~ Tx TopTx era,
 State (someLEDGER era) ~ LedgerState era,
 Environment (someLEDGER era) ~ LedgerEnv era,
 Embed (EraRule "UTXOW" era) (someLEDGER era),
 Embed (EraRule "DELEGS" era) (someLEDGER era),
 Environment (EraRule "DELEGS" era) ~ DelegsEnv era,
 State (EraRule "DELEGS" era) ~ CertState era,
 Signal (EraRule "DELEGS" era) ~ Seq (TxCert era),
 Environment (EraRule "UTXOW" era) ~ UtxoEnv era,
 State (EraRule "UTXOW" era) ~ UTxOState era,
 Signal (EraRule "UTXOW" era) ~ Tx TopTx era, AlonzoEraTx era,
 EraCertState era, EraRule "LEDGER" era ~ someLEDGER era,
 InjectRuleFailure "LEDGER" ShelleyLedgerPredFailure era) =>
TransitionRule (someLEDGER era)
ledgerTransition @AlonzoLEDGER]

  renderAssertionViolation :: AssertionViolation (AlonzoLEDGER era) -> String
renderAssertionViolation = AssertionViolation (AlonzoLEDGER era) -> String
forall era t.
(EraTx era, EraGov era, EraCertState era,
 Environment t ~ LedgerEnv era, Signal t ~ Tx TopTx era,
 State t ~ LedgerState era) =>
AssertionViolation t -> String
Shelley.renderDepositEqualsObligationViolation

  assertions :: [Assertion (AlonzoLEDGER era)]
assertions = [Assertion (AlonzoLEDGER era)]
forall era (rule :: * -> *).
(EraGov era, EraCertState era,
 State (rule era) ~ LedgerState era) =>
[Assertion (rule era)]
shelleyLedgerAssertions

instance
  ( Era era
  , STS (ShelleyDELEGS era)
  , PredicateFailure (EraRule "DELEGS" era) ~ ShelleyDelegsPredFailure era
  , Event (EraRule "DELEGS" era) ~ ShelleyDelegsEvent era
  ) =>
  Embed (ShelleyDELEGS era) (AlonzoLEDGER era)
  where
  wrapFailed :: PredicateFailure (ShelleyDELEGS era)
-> PredicateFailure (AlonzoLEDGER era)
wrapFailed = PredicateFailure (EraRule "DELEGS" era)
-> ShelleyLedgerPredFailure era
PredicateFailure (ShelleyDELEGS era)
-> PredicateFailure (AlonzoLEDGER era)
forall era.
PredicateFailure (EraRule "DELEGS" era)
-> ShelleyLedgerPredFailure era
DelegsFailure
  wrapEvent :: Event (ShelleyDELEGS era) -> Event (AlonzoLEDGER era)
wrapEvent = Event (EraRule "DELEGS" era) -> ShelleyLedgerEvent era
Event (ShelleyDELEGS era) -> Event (AlonzoLEDGER era)
forall era. Event (EraRule "DELEGS" era) -> ShelleyLedgerEvent era
DelegsEvent

instance
  ( Era era
  , STS (AlonzoUTXOW era)
  , PredicateFailure (EraRule "UTXOW" era) ~ AlonzoUtxowPredFailure era
  , Event (EraRule "UTXOW" era) ~ AlonzoUtxowEvent era
  ) =>
  Embed (AlonzoUTXOW era) (AlonzoLEDGER era)
  where
  wrapFailed :: PredicateFailure (AlonzoUTXOW era)
-> PredicateFailure (AlonzoLEDGER era)
wrapFailed = PredicateFailure (EraRule "UTXOW" era)
-> ShelleyLedgerPredFailure era
PredicateFailure (AlonzoUTXOW era)
-> PredicateFailure (AlonzoLEDGER era)
forall era.
PredicateFailure (EraRule "UTXOW" era)
-> ShelleyLedgerPredFailure era
UtxowFailure
  wrapEvent :: Event (AlonzoUTXOW era) -> Event (AlonzoLEDGER era)
wrapEvent = Event (EraRule "UTXOW" era) -> ShelleyLedgerEvent era
Event (AlonzoUTXOW era) -> Event (AlonzoLEDGER era)
forall era. Event (EraRule "UTXOW" era) -> ShelleyLedgerEvent era
UtxowEvent

instance
  ( Era era
  , STS (AlonzoLEDGER era)
  , PredicateFailure (EraRule "LEDGER" era) ~ ShelleyLedgerPredFailure era
  , Event (EraRule "LEDGER" era) ~ ShelleyLedgerEvent era
  ) =>
  Embed (AlonzoLEDGER era) (ShelleyLEDGERS era)
  where
  wrapFailed :: PredicateFailure (AlonzoLEDGER era)
-> PredicateFailure (ShelleyLEDGERS era)
wrapFailed = PredicateFailure (EraRule "LEDGER" era)
-> ShelleyLedgersPredFailure era
PredicateFailure (AlonzoLEDGER era)
-> PredicateFailure (ShelleyLEDGERS era)
forall era.
PredicateFailure (EraRule "LEDGER" era)
-> ShelleyLedgersPredFailure era
Shelley.LedgerFailure
  wrapEvent :: Event (AlonzoLEDGER era) -> Event (ShelleyLEDGERS era)
wrapEvent = Event (EraRule "LEDGER" era) -> ShelleyLedgersEvent era
Event (AlonzoLEDGER era) -> Event (ShelleyLEDGERS era)
forall era. Event (EraRule "LEDGER" era) -> ShelleyLedgersEvent era
Shelley.LedgerEvent