{-# 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
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