{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Cardano.Ledger.Shelley.Rules.Ledger (
ShelleyLEDGER,
LedgerEnv (..),
ShelleyLedgerPredFailure (..),
ShelleyLedgerEvent (..),
Event,
PredicateFailure,
epochFromSlot,
renderDepositEqualsObligationViolation,
shelleyLedgerAssertions,
)
where
import Cardano.Ledger.BaseTypes (Globals, ShelleyBase, TxIx, epochInfoPure, invalidKey)
import Cardano.Ledger.Binary (
DecCBOR (..),
EncCBOR (..),
decodeRecordSum,
encodeListLen,
)
import Cardano.Ledger.Binary.Coders (Encode (..), encode, (!>))
import Cardano.Ledger.Keys (DSignable, Hash)
import Cardano.Ledger.Shelley.AdaPots (consumedTxBody, producedTxBody)
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.Era (ShelleyEra, ShelleyLEDGER)
import Cardano.Ledger.Shelley.LedgerState (
AccountState,
CertState (..),
LedgerState (..),
UTxOState (..),
utxosDepositedL,
)
import Cardano.Ledger.Shelley.LedgerState.Types (allObligations, potEqualsObligation)
import Cardano.Ledger.Shelley.Rules.Deleg (ShelleyDelegPredFailure)
import Cardano.Ledger.Shelley.Rules.Delegs (
DelegsEnv (..),
ShelleyDELEGS,
ShelleyDelegsEvent,
ShelleyDelegsPredFailure,
)
import Cardano.Ledger.Shelley.Rules.Delpl (ShelleyDelplPredFailure)
import Cardano.Ledger.Shelley.Rules.Pool (ShelleyPoolPredFailure)
import Cardano.Ledger.Shelley.Rules.Ppup (ShelleyPpupPredFailure)
import Cardano.Ledger.Shelley.Rules.Reports (showTxCerts)
import Cardano.Ledger.Shelley.Rules.Utxo (ShelleyUtxoPredFailure (..), UtxoEnv (..))
import Cardano.Ledger.Shelley.Rules.Utxow (ShelleyUTXOW, ShelleyUtxowPredFailure)
import Cardano.Ledger.Slot (EpochNo, SlotNo, epochInfoEpoch)
import Control.DeepSeq (NFData (..))
import Control.Monad.Reader (Reader)
import Control.Monad.Trans.Reader (asks)
import Control.State.Transition (
Assertion (PostCondition),
AssertionViolation (..),
Embed (..),
STS (..),
TRC (..),
TransitionRule,
judgmentContext,
trans,
)
import Data.Sequence (Seq)
import qualified Data.Sequence.Strict as StrictSeq
import Data.Word (Word8)
import GHC.Generics (Generic)
import Lens.Micro
import NoThunks.Class (NoThunks (..))
data LedgerEnv era = LedgerEnv
{ forall era. LedgerEnv era -> SlotNo
ledgerSlotNo :: !SlotNo
, forall era. LedgerEnv era -> TxIx
ledgerIx :: !TxIx
, forall era. LedgerEnv era -> PParams era
ledgerPp :: !(PParams era)
, forall era. LedgerEnv era -> AccountState
ledgerAccount :: !AccountState
, forall era. LedgerEnv era -> Bool
ledgerMempool :: !Bool
}
deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x. Rep (LedgerEnv era) x -> LedgerEnv era
forall era x. LedgerEnv era -> Rep (LedgerEnv era) x
$cto :: forall era x. Rep (LedgerEnv era) x -> LedgerEnv era
$cfrom :: forall era x. LedgerEnv era -> Rep (LedgerEnv era) x
Generic)
deriving instance Show (PParams era) => Show (LedgerEnv era)
deriving instance Eq (PParams era) => Eq (LedgerEnv era)
instance NFData (PParams era) => NFData (LedgerEnv era) where
rnf :: LedgerEnv era -> ()
rnf (LedgerEnv SlotNo
_slotNo TxIx
_ix PParams era
pp AccountState
_account Bool
_mempool) = forall a. NFData a => a -> ()
rnf PParams era
pp
instance EraPParams era => EncCBOR (LedgerEnv era) where
encCBOR :: LedgerEnv era -> Encoding
encCBOR env :: LedgerEnv era
env@(LedgerEnv SlotNo
_ TxIx
_ PParams era
_ AccountState
_ Bool
_) =
let LedgerEnv {Bool
PParams era
TxIx
SlotNo
AccountState
ledgerMempool :: Bool
ledgerAccount :: AccountState
ledgerPp :: PParams era
ledgerIx :: TxIx
ledgerSlotNo :: SlotNo
ledgerMempool :: forall era. LedgerEnv era -> Bool
ledgerAccount :: forall era. LedgerEnv era -> AccountState
ledgerPp :: forall era. LedgerEnv era -> PParams era
ledgerIx :: forall era. LedgerEnv era -> TxIx
ledgerSlotNo :: forall era. LedgerEnv era -> SlotNo
..} = LedgerEnv era
env
in forall (w :: Wrapped) t. Encode w t -> Encoding
encode forall a b. (a -> b) -> a -> b
$
forall t. t -> Encode ('Closed 'Dense) t
Rec forall era.
SlotNo
-> TxIx -> PParams era -> AccountState -> Bool -> LedgerEnv era
LedgerEnv
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To SlotNo
ledgerSlotNo
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To TxIx
ledgerIx
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To PParams era
ledgerPp
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To AccountState
ledgerAccount
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Bool
ledgerMempool
data ShelleyLedgerPredFailure era
= UtxowFailure (PredicateFailure (EraRule "UTXOW" era))
| DelegsFailure (PredicateFailure (EraRule "DELEGS" era))
deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyLedgerPredFailure era) x
-> ShelleyLedgerPredFailure era
forall era x.
ShelleyLedgerPredFailure era
-> Rep (ShelleyLedgerPredFailure era) x
$cto :: forall era x.
Rep (ShelleyLedgerPredFailure era) x
-> ShelleyLedgerPredFailure era
$cfrom :: forall era x.
ShelleyLedgerPredFailure era
-> Rep (ShelleyLedgerPredFailure era) x
Generic)
type instance EraRuleFailure "LEDGER" (ShelleyEra c) = ShelleyLedgerPredFailure (ShelleyEra c)
instance InjectRuleFailure "LEDGER" ShelleyLedgerPredFailure (ShelleyEra c)
instance InjectRuleFailure "LEDGER" ShelleyUtxowPredFailure (ShelleyEra c) where
injectFailure :: ShelleyUtxowPredFailure (ShelleyEra c)
-> EraRuleFailure "LEDGER" (ShelleyEra c)
injectFailure = forall era.
PredicateFailure (EraRule "UTXOW" era)
-> ShelleyLedgerPredFailure era
UtxowFailure
instance InjectRuleFailure "LEDGER" ShelleyUtxoPredFailure (ShelleyEra c) where
injectFailure :: ShelleyUtxoPredFailure (ShelleyEra c)
-> EraRuleFailure "LEDGER" (ShelleyEra c)
injectFailure = forall era.
PredicateFailure (EraRule "UTXOW" era)
-> ShelleyLedgerPredFailure era
UtxowFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure
instance InjectRuleFailure "LEDGER" ShelleyPpupPredFailure (ShelleyEra c) where
injectFailure :: ShelleyPpupPredFailure (ShelleyEra c)
-> EraRuleFailure "LEDGER" (ShelleyEra c)
injectFailure = forall era.
PredicateFailure (EraRule "UTXOW" era)
-> ShelleyLedgerPredFailure era
UtxowFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure
instance InjectRuleFailure "LEDGER" ShelleyDelegsPredFailure (ShelleyEra c) where
injectFailure :: ShelleyDelegsPredFailure (ShelleyEra c)
-> EraRuleFailure "LEDGER" (ShelleyEra c)
injectFailure = forall era.
PredicateFailure (EraRule "DELEGS" era)
-> ShelleyLedgerPredFailure era
DelegsFailure
instance InjectRuleFailure "LEDGER" ShelleyDelplPredFailure (ShelleyEra c) where
injectFailure :: ShelleyDelplPredFailure (ShelleyEra c)
-> EraRuleFailure "LEDGER" (ShelleyEra c)
injectFailure = forall era.
PredicateFailure (EraRule "DELEGS" era)
-> ShelleyLedgerPredFailure era
DelegsFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure
instance InjectRuleFailure "LEDGER" ShelleyPoolPredFailure (ShelleyEra c) where
injectFailure :: ShelleyPoolPredFailure (ShelleyEra c)
-> EraRuleFailure "LEDGER" (ShelleyEra c)
injectFailure = forall era.
PredicateFailure (EraRule "DELEGS" era)
-> ShelleyLedgerPredFailure era
DelegsFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure
instance InjectRuleFailure "LEDGER" ShelleyDelegPredFailure (ShelleyEra c) where
injectFailure :: ShelleyDelegPredFailure (ShelleyEra c)
-> EraRuleFailure "LEDGER" (ShelleyEra c)
injectFailure = forall era.
PredicateFailure (EraRule "DELEGS" era)
-> ShelleyLedgerPredFailure era
DelegsFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure
type instance EraRuleEvent "LEDGER" (ShelleyEra c) = ShelleyLedgerEvent (ShelleyEra c)
data ShelleyLedgerEvent era
= UtxowEvent (Event (EraRule "UTXOW" era))
| DelegsEvent (Event (EraRule "DELEGS" era))
deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyLedgerEvent era) x -> ShelleyLedgerEvent era
forall era x.
ShelleyLedgerEvent era -> Rep (ShelleyLedgerEvent era) x
$cto :: forall era x.
Rep (ShelleyLedgerEvent era) x -> ShelleyLedgerEvent era
$cfrom :: forall era x.
ShelleyLedgerEvent era -> Rep (ShelleyLedgerEvent era) x
Generic)
deriving instance
( Eq (Event (EraRule "UTXOW" era))
, Eq (Event (EraRule "DELEGS" era))
) =>
Eq (ShelleyLedgerEvent era)
instance
( NFData (Event (EraRule "UTXOW" era))
, NFData (Event (EraRule "DELEGS" era))
) =>
NFData (ShelleyLedgerEvent era)
deriving stock instance
( Show (PredicateFailure (EraRule "DELEGS" era))
, Show (PredicateFailure (EraRule "UTXOW" era))
, Era era
) =>
Show (ShelleyLedgerPredFailure era)
deriving stock instance
( Eq (PredicateFailure (EraRule "DELEGS" era))
, Eq (PredicateFailure (EraRule "UTXOW" era))
, Era era
) =>
Eq (ShelleyLedgerPredFailure era)
instance
( NoThunks (PredicateFailure (EraRule "DELEGS" era))
, NoThunks (PredicateFailure (EraRule "UTXOW" era))
, Era era
) =>
NoThunks (ShelleyLedgerPredFailure era)
instance
( NFData (PredicateFailure (EraRule "DELEGS" era))
, NFData (PredicateFailure (EraRule "UTXOW" era))
, Era era
) =>
NFData (ShelleyLedgerPredFailure era)
instance
( EncCBOR (PredicateFailure (EraRule "DELEGS" era))
, EncCBOR (PredicateFailure (EraRule "UTXOW" era))
, Era era
) =>
EncCBOR (ShelleyLedgerPredFailure era)
where
encCBOR :: ShelleyLedgerPredFailure era -> Encoding
encCBOR = \case
(UtxowFailure PredicateFailure (EraRule "UTXOW" 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 "UTXOW" era)
a
(DelegsFailure PredicateFailure (EraRule "DELEGS" 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 "DELEGS" era)
a
instance
( DecCBOR (PredicateFailure (EraRule "DELEGS" era))
, DecCBOR (PredicateFailure (EraRule "UTXOW" era))
, Era era
) =>
DecCBOR (ShelleyLedgerPredFailure era)
where
decCBOR :: forall s. Decoder s (ShelleyLedgerPredFailure era)
decCBOR =
forall s a. Text -> (Word -> Decoder s (Int, a)) -> Decoder s a
decodeRecordSum Text
"PredicateFailure (LEDGER era)" forall a b. (a -> b) -> a -> b
$
\case
Word
0 -> do
PredicateFailure (EraRule "UTXOW" 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 "UTXOW" era)
-> ShelleyLedgerPredFailure era
UtxowFailure PredicateFailure (EraRule "UTXOW" era)
a)
Word
1 -> do
PredicateFailure (EraRule "DELEGS" 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 "DELEGS" era)
-> ShelleyLedgerPredFailure era
DelegsFailure PredicateFailure (EraRule "DELEGS" era)
a)
Word
k -> forall (m :: * -> *) a. MonadFail m => Word -> m a
invalidKey Word
k
epochFromSlot :: SlotNo -> Reader Globals EpochNo
epochFromSlot :: SlotNo -> Reader Globals EpochNo
epochFromSlot SlotNo
slot = do
EpochInfo Identity
ei <- forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> EpochInfo Identity
epochInfoPure
HasCallStack =>
EpochInfo Identity -> SlotNo -> Reader Globals EpochNo
epochInfoEpoch EpochInfo Identity
ei SlotNo
slot
shelleyLedgerAssertions ::
( EraGov era
, State (rule era) ~ LedgerState era
) =>
[Assertion (rule era)]
shelleyLedgerAssertions :: forall era (rule :: * -> *).
(EraGov era, State (rule era) ~ LedgerState era) =>
[Assertion (rule era)]
shelleyLedgerAssertions =
[ forall sts.
String -> (TRC sts -> State sts -> Bool) -> Assertion sts
PostCondition
String
"Deposit pot must equal obligation (LEDGER)"
( \(TRC (Environment (rule era)
_, State (rule era)
_, Signal (rule era)
_))
(LedgerState UTxOState era
utxoSt CertState era
dpstate) -> forall era. EraGov era => CertState era -> UTxOState era -> Bool
potEqualsObligation CertState era
dpstate UTxOState era
utxoSt
)
]
instance
( DSignable (EraCrypto era) (Hash (EraCrypto era) EraIndependentTxBody)
, EraTx era
, EraGov era
, Embed (EraRule "DELEGS" era) (ShelleyLEDGER era)
, Embed (EraRule "UTXOW" era) (ShelleyLEDGER era)
, Environment (EraRule "UTXOW" era) ~ UtxoEnv era
, State (EraRule "UTXOW" era) ~ UTxOState era
, Signal (EraRule "UTXOW" era) ~ Tx era
, Environment (EraRule "DELEGS" era) ~ DelegsEnv era
, State (EraRule "DELEGS" era) ~ CertState era
, Signal (EraRule "DELEGS" era) ~ Seq (TxCert era)
, ProtVerAtMost era 8
) =>
STS (ShelleyLEDGER era)
where
type State (ShelleyLEDGER era) = LedgerState era
type Signal (ShelleyLEDGER era) = Tx era
type Environment (ShelleyLEDGER era) = LedgerEnv era
type BaseM (ShelleyLEDGER era) = ShelleyBase
type PredicateFailure (ShelleyLEDGER era) = ShelleyLedgerPredFailure era
type Event (ShelleyLEDGER era) = ShelleyLedgerEvent era
initialRules :: [InitialRule (ShelleyLEDGER era)]
initialRules = []
transitionRules :: [TransitionRule (ShelleyLEDGER era)]
transitionRules = [forall era.
(EraTx era, Embed (EraRule "DELEGS" era) (ShelleyLEDGER era),
Environment (EraRule "DELEGS" era) ~ DelegsEnv era,
State (EraRule "DELEGS" era) ~ CertState era,
Signal (EraRule "DELEGS" era) ~ Seq (TxCert era),
Embed (EraRule "UTXOW" era) (ShelleyLEDGER era),
Environment (EraRule "UTXOW" era) ~ UtxoEnv era,
State (EraRule "UTXOW" era) ~ UTxOState era,
Signal (EraRule "UTXOW" era) ~ Tx era) =>
TransitionRule (ShelleyLEDGER era)
ledgerTransition]
renderAssertionViolation :: AssertionViolation (ShelleyLEDGER era) -> String
renderAssertionViolation = forall era t.
(EraTx era, EraGov era, Environment t ~ LedgerEnv era,
Signal t ~ Tx era, State t ~ LedgerState era) =>
AssertionViolation t -> String
renderDepositEqualsObligationViolation
assertions :: [Assertion (ShelleyLEDGER era)]
assertions = forall era (rule :: * -> *).
(EraGov era, State (rule era) ~ LedgerState era) =>
[Assertion (rule era)]
shelleyLedgerAssertions
ledgerTransition ::
forall era.
( EraTx era
, Embed (EraRule "DELEGS" era) (ShelleyLEDGER era)
, Environment (EraRule "DELEGS" era) ~ DelegsEnv era
, State (EraRule "DELEGS" era) ~ CertState era
, Signal (EraRule "DELEGS" era) ~ Seq (TxCert era)
, Embed (EraRule "UTXOW" era) (ShelleyLEDGER era)
, Environment (EraRule "UTXOW" era) ~ UtxoEnv era
, State (EraRule "UTXOW" era) ~ UTxOState era
, Signal (EraRule "UTXOW" era) ~ Tx era
) =>
TransitionRule (ShelleyLEDGER era)
ledgerTransition :: forall era.
(EraTx era, Embed (EraRule "DELEGS" era) (ShelleyLEDGER era),
Environment (EraRule "DELEGS" era) ~ DelegsEnv era,
State (EraRule "DELEGS" era) ~ CertState era,
Signal (EraRule "DELEGS" era) ~ Seq (TxCert era),
Embed (EraRule "UTXOW" era) (ShelleyLEDGER era),
Environment (EraRule "UTXOW" era) ~ UtxoEnv era,
State (EraRule "UTXOW" era) ~ UTxOState era,
Signal (EraRule "UTXOW" era) ~ Tx era) =>
TransitionRule (ShelleyLEDGER era)
ledgerTransition = do
TRC (LedgerEnv SlotNo
slot TxIx
txIx PParams era
pp AccountState
account Bool
_, LedgerState UTxOState era
utxoSt CertState era
certState, Signal (ShelleyLEDGER era)
tx) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
CertState era
certState' <-
forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "DELEGS" era) forall a b. (a -> b) -> a -> b
$
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC
( forall era.
SlotNo
-> TxIx -> PParams era -> Tx era -> AccountState -> DelegsEnv era
DelegsEnv SlotNo
slot TxIx
txIx PParams era
pp Signal (ShelleyLEDGER era)
tx AccountState
account
, CertState era
certState
, forall a. StrictSeq a -> Seq a
StrictSeq.fromStrict forall a b. (a -> b) -> a -> b
$ Signal (ShelleyLEDGER era)
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictSeq (TxCert era))
certsTxBodyL
)
UTxOState era
utxoSt' <-
forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "UTXOW" era) forall a b. (a -> b) -> a -> b
$
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC
( forall era. SlotNo -> PParams era -> CertState era -> UtxoEnv era
UtxoEnv SlotNo
slot PParams era
pp CertState era
certState
, UTxOState era
utxoSt
, Signal (ShelleyLEDGER era)
tx
)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era. UTxOState era -> CertState era -> LedgerState era
LedgerState UTxOState era
utxoSt' CertState era
certState')
instance
( Era era
, STS (ShelleyDELEGS era)
, PredicateFailure (EraRule "DELEGS" era) ~ ShelleyDelegsPredFailure era
, Event (EraRule "DELEGS" era) ~ ShelleyDelegsEvent era
) =>
Embed (ShelleyDELEGS era) (ShelleyLEDGER era)
where
wrapFailed :: PredicateFailure (ShelleyDELEGS era)
-> PredicateFailure (ShelleyLEDGER era)
wrapFailed = forall era.
PredicateFailure (EraRule "DELEGS" era)
-> ShelleyLedgerPredFailure era
DelegsFailure
wrapEvent :: Event (ShelleyDELEGS era) -> Event (ShelleyLEDGER era)
wrapEvent = forall era. Event (EraRule "DELEGS" era) -> ShelleyLedgerEvent era
DelegsEvent
instance
( STS (ShelleyUTXOW era)
, PredicateFailure (EraRule "UTXOW" era) ~ ShelleyUtxowPredFailure era
, Event (EraRule "UTXOW" era) ~ Event (ShelleyUTXOW era)
) =>
Embed (ShelleyUTXOW era) (ShelleyLEDGER era)
where
wrapFailed :: PredicateFailure (ShelleyUTXOW era)
-> PredicateFailure (ShelleyLEDGER era)
wrapFailed = forall era.
PredicateFailure (EraRule "UTXOW" era)
-> ShelleyLedgerPredFailure era
UtxowFailure
wrapEvent :: Event (ShelleyUTXOW era) -> Event (ShelleyLEDGER era)
wrapEvent = forall era. Event (EraRule "UTXOW" era) -> ShelleyLedgerEvent era
UtxowEvent
renderDepositEqualsObligationViolation ::
( EraTx era
, EraGov era
, Environment t ~ LedgerEnv era
, Signal t ~ Tx era
, State t ~ LedgerState era
) =>
AssertionViolation t ->
String
renderDepositEqualsObligationViolation :: forall era t.
(EraTx era, EraGov era, Environment t ~ LedgerEnv era,
Signal t ~ Tx era, State t ~ LedgerState era) =>
AssertionViolation t -> String
renderDepositEqualsObligationViolation
AssertionViolation {String
avSTS :: forall sts. AssertionViolation sts -> String
avSTS :: String
avSTS, String
avMsg :: forall sts. AssertionViolation sts -> String
avMsg :: String
avMsg, avCtx :: forall sts. AssertionViolation sts -> TRC sts
avCtx = TRC (LedgerEnv SlotNo
slot TxIx
_ PParams era
pp AccountState
_ Bool
_, State t
_, Signal t
tx), Maybe (State t)
avState :: forall sts. AssertionViolation sts -> Maybe (State sts)
avState :: Maybe (State t)
avState} =
case Maybe (State t)
avState of
Maybe (State t)
Nothing -> String
"\nAssertionViolation " forall a. [a] -> [a] -> [a]
++ String
avSTS forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ String
avMsg forall a. [a] -> [a] -> [a]
++ String
" (avState is Nothing)."
Just State t
lstate ->
let certstate :: CertState era
certstate = forall era. LedgerState era -> CertState era
lsCertState State t
lstate
utxoSt :: UTxOState era
utxoSt = forall era. LedgerState era -> UTxOState era
lsUTxOState State t
lstate
utxo :: UTxO era
utxo = forall era. UTxOState era -> UTxO era
utxosUtxo UTxOState era
utxoSt
txb :: TxBody era
txb = Signal t
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL
pot :: Coin
pot = UTxOState era
utxoSt forall s a. s -> Getting a s a -> a
^. forall era. Lens' (UTxOState era) Coin
utxosDepositedL
in String
"\n\nAssertionViolation ("
forall a. Semigroup a => a -> a -> a
<> String
avSTS
forall a. Semigroup a => a -> a -> a
<> String
")\n\n "
forall a. Semigroup a => a -> a -> a
<> String
avMsg
forall a. Semigroup a => a -> a -> a
<> String
"\n\nCERTS\n"
forall a. Semigroup a => a -> a -> a
<> forall era. EraTxBody era => TxBody era -> String
showTxCerts TxBody era
txb
forall a. Semigroup a => a -> a -> a
<> String
"\n(slot,keyDeposit,poolDeposit) "
forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show (SlotNo
slot, PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) Coin
ppKeyDepositL, PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) Coin
ppPoolDepositL)
forall a. Semigroup a => a -> a -> a
<> String
"\nThe Pot (utxosDeposited) = "
forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Coin
pot
forall a. Semigroup a => a -> a -> a
<> String
"\n"
forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show (forall era.
EraGov era =>
CertState era -> GovState era -> Obligations
allObligations CertState era
certstate (forall era. UTxOState era -> GovState era
utxosGovState UTxOState era
utxoSt))
forall a. Semigroup a => a -> a -> a
<> String
"\nConsumed = "
forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show (forall era.
EraTxBody era =>
TxBody era -> PParams era -> CertState era -> UTxO era -> Consumed
consumedTxBody TxBody era
txb PParams era
pp CertState era
certstate UTxO era
utxo)
forall a. Semigroup a => a -> a -> a
<> String
"\nProduced = "
forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show (forall era.
EraTxBody era =>
TxBody era -> PParams era -> CertState era -> Produced
producedTxBody TxBody era
txb PParams era
pp CertState era
certstate)