{-# 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 (..), AlonzoTx (..), 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,
 )
import Cardano.Ledger.Shelley.Rules as Shelley (
  LedgerEnv (..),
  ShelleyLedgerEvent (..),
  ShelleyLedgerPredFailure (..),
  ShelleyLedgersEvent (..),
  ShelleyLedgersPredFailure (..),
  renderDepositEqualsObligationViolation,
 )
import Cardano.Ledger.Slot (epochFromSlot)
import Cardano.Ledger.State (EraCertState)
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 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 era
  , AlonzoEraTx era
  ) =>
  TransitionRule (someLEDGER era)
ledgerTransition :: forall (someLEDGER :: * -> *) era.
(STS (someLEDGER era), BaseM (someLEDGER era) ~ ShelleyBase,
 Signal (someLEDGER era) ~ Tx 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 era, AlonzoEraTx era) =>
TransitionRule (someLEDGER era)
ledgerTransition = do
  TRC (LedgerEnv SlotNo
slot Maybe EpochNo
mbCurEpochNo TxIx
txIx PParams era
pp ChainAccountState
account, LedgerState UTxOState era
utxoSt CertState era
certState, Signal (someLEDGER era)
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 :: TxBody era
txBody = Tx era
Signal (someLEDGER era)
tx Tx era -> Getting (TxBody era) (Tx era) (TxBody era) -> TxBody era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody era) (Tx era) (TxBody era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL

  EpochNo
curEpochNo <- F (Clause (someLEDGER era) 'Transition) EpochNo
-> (EpochNo -> F (Clause (someLEDGER era) 'Transition) EpochNo)
-> Maybe EpochNo
-> F (Clause (someLEDGER era) 'Transition) EpochNo
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (BaseM (someLEDGER era) EpochNo
-> F (Clause (someLEDGER era) 'Transition) EpochNo
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (someLEDGER era) EpochNo
 -> F (Clause (someLEDGER era) 'Transition) EpochNo)
-> BaseM (someLEDGER era) EpochNo
-> F (Clause (someLEDGER era) 'Transition) EpochNo
forall a b. (a -> b) -> a -> b
$ SlotNo -> Reader Globals EpochNo
epochFromSlot SlotNo
slot) EpochNo -> F (Clause (someLEDGER era) 'Transition) EpochNo
forall a. a -> F (Clause (someLEDGER era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe EpochNo
mbCurEpochNo

  CertState era
certState' <-
    if Tx era
Signal (someLEDGER era)
tx Tx era -> Getting IsValid (Tx era) IsValid -> IsValid
forall s a. s -> Getting a s a -> a
^. Getting IsValid (Tx era) IsValid
forall era. AlonzoEraTx era => Lens' (Tx era) IsValid
Lens' (Tx era) IsValid
isValidTxL IsValid -> IsValid -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> IsValid
IsValid Bool
True
      then
        forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "DELEGS" era) (RuleContext 'Transition (EraRule "DELEGS" era)
 -> Rule
      (someLEDGER era) 'Transition (State (EraRule "DELEGS" era)))
-> RuleContext 'Transition (EraRule "DELEGS" era)
-> Rule (someLEDGER era) 'Transition (State (EraRule "DELEGS" era))
forall a b. (a -> b) -> a -> b
$
          (Environment (EraRule "DELEGS" era), State (EraRule "DELEGS" era),
 Signal (EraRule "DELEGS" era))
-> TRC (EraRule "DELEGS" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC
            ( SlotNo
-> EpochNo
-> TxIx
-> PParams era
-> Tx era
-> ChainAccountState
-> DelegsEnv era
forall era.
SlotNo
-> EpochNo
-> TxIx
-> PParams era
-> Tx era
-> ChainAccountState
-> DelegsEnv era
DelegsEnv SlotNo
slot EpochNo
curEpochNo TxIx
txIx PParams era
pp Tx era
Signal (someLEDGER era)
tx ChainAccountState
account
            , CertState era
State (EraRule "DELEGS" era)
certState
            , StrictSeq (TxCert era) -> Seq (TxCert era)
forall a. StrictSeq a -> Seq a
StrictSeq.fromStrict (StrictSeq (TxCert era) -> Seq (TxCert era))
-> StrictSeq (TxCert era) -> Seq (TxCert era)
forall a b. (a -> b) -> a -> b
$ TxBody era
txBody TxBody era
-> Getting
     (StrictSeq (TxCert era)) (TxBody era) (StrictSeq (TxCert era))
-> StrictSeq (TxCert era)
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictSeq (TxCert era)) (TxBody era) (StrictSeq (TxCert era))
forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictSeq (TxCert era))
Lens' (TxBody era) (StrictSeq (TxCert era))
certsTxBodyL
            )
      else CertState era
-> F (Clause (someLEDGER era) 'Transition) (CertState era)
forall a. a -> F (Clause (someLEDGER era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CertState era
certState

  UTxOState era
utxoSt' <-
    forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "UTXOW" era) (RuleContext 'Transition (EraRule "UTXOW" era)
 -> Rule (someLEDGER era) 'Transition (State (EraRule "UTXOW" era)))
-> RuleContext 'Transition (EraRule "UTXOW" era)
-> Rule (someLEDGER era) 'Transition (State (EraRule "UTXOW" era))
forall a b. (a -> b) -> a -> b
$
      (Environment (EraRule "UTXOW" era), State (EraRule "UTXOW" era),
 Signal (EraRule "UTXOW" era))
-> TRC (EraRule "UTXOW" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC
        ( forall era. SlotNo -> PParams era -> CertState era -> UtxoEnv era
UtxoEnv @era SlotNo
slot PParams era
pp CertState era
certState
        , State (EraRule "UTXOW" era)
UTxOState era
utxoSt
        , Signal (someLEDGER era)
Signal (EraRule "UTXOW" era)
tx
        )
  LedgerState era
-> F (Clause (someLEDGER era) 'Transition) (LedgerState era)
forall a. a -> F (Clause (someLEDGER era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LedgerState era
 -> F (Clause (someLEDGER era) 'Transition) (LedgerState era))
-> LedgerState era
-> F (Clause (someLEDGER era) 'Transition) (LedgerState era)
forall a b. (a -> b) -> a -> b
$ UTxOState era -> CertState era -> LedgerState era
forall era. UTxOState era -> CertState era -> LedgerState era
LedgerState UTxOState era
utxoSt' CertState era
certState'

instance
  ( AlonzoEraTx era
  , EraGov era
  , Tx era ~ AlonzoTx 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) ~ AlonzoTx era
  , Environment (EraRule "DELEGS" era) ~ DelegsEnv era
  , State (EraRule "DELEGS" era) ~ CertState era
  , Signal (EraRule "DELEGS" era) ~ Seq (TxCert era)
  , ProtVerAtMost era 8
  , EraCertState era
  ) =>
  STS (AlonzoLEDGER era)
  where
  type State (AlonzoLEDGER era) = LedgerState era
  type Signal (AlonzoLEDGER era) = AlonzoTx 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 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 era, AlonzoEraTx 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 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