{-# 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 (..),
  ledgerSlotNoL,
  ledgerEpochNoL,
  ledgerIxL,
  ledgerPpL,
  ledgerAccountL,
  ShelleyLedgerPredFailure (..),
  ShelleyLedgerEvent (..),
  Event,
  PredicateFailure,
  epochFromSlot,
  renderDepositEqualsObligationViolation,
  shelleyLedgerAssertions,
) where

import Cardano.Ledger.BaseTypes (ShelleyBase, TxIx, invalidKey)
import Cardano.Ledger.Binary (
  DecCBOR (..),
  EncCBOR (..),
  decodeRecordSum,
  encodeListLen,
 )
import Cardano.Ledger.Binary.Coders (Encode (..), encode, (!>))
import Cardano.Ledger.Shelley.AdaPots (consumedTxBody, producedTxBody)
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.Era (ShelleyEra, ShelleyLEDGER)
import Cardano.Ledger.Shelley.LedgerState (
  ChainAccountState,
  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, epochFromSlot)
import Cardano.Ledger.State (EraCertState (..))
import Control.DeepSeq (NFData (..))
import Control.State.Transition (
  Assertion (PostCondition),
  AssertionViolation (..),
  Embed (..),
  STS (..),
  TRC (..),
  TransitionRule,
  judgmentContext,
  liftSTS,
  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 -> Maybe EpochNo
ledgerEpochNo :: Maybe EpochNo
  , forall era. LedgerEnv era -> TxIx
ledgerIx :: TxIx
  , forall era. LedgerEnv era -> PParams era
ledgerPp :: PParams era
  , forall era. LedgerEnv era -> ChainAccountState
ledgerAccount :: ChainAccountState
  }
  deriving ((forall x. LedgerEnv era -> Rep (LedgerEnv era) x)
-> (forall x. Rep (LedgerEnv era) x -> LedgerEnv era)
-> Generic (LedgerEnv era)
forall x. Rep (LedgerEnv era) x -> LedgerEnv era
forall x. LedgerEnv era -> Rep (LedgerEnv era) x
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
$cfrom :: forall era x. LedgerEnv era -> Rep (LedgerEnv era) x
from :: forall x. LedgerEnv era -> Rep (LedgerEnv era) x
$cto :: forall era x. Rep (LedgerEnv era) x -> LedgerEnv era
to :: forall x. Rep (LedgerEnv era) x -> LedgerEnv era
Generic)

deriving instance Show (PParams era) => Show (LedgerEnv era)

deriving instance Eq (PParams era) => Eq (LedgerEnv era)

instance NFData (PParams era) => NFData (LedgerEnv era)

instance EraPParams era => EncCBOR (LedgerEnv era) where
  encCBOR :: LedgerEnv era -> Encoding
encCBOR env :: LedgerEnv era
env@(LedgerEnv SlotNo
_ Maybe EpochNo
_ TxIx
_ PParams era
_ ChainAccountState
_) =
    let LedgerEnv {Maybe EpochNo
SlotNo
TxIx
PParams era
ChainAccountState
ledgerSlotNo :: forall era. LedgerEnv era -> SlotNo
ledgerEpochNo :: forall era. LedgerEnv era -> Maybe EpochNo
ledgerIx :: forall era. LedgerEnv era -> TxIx
ledgerPp :: forall era. LedgerEnv era -> PParams era
ledgerAccount :: forall era. LedgerEnv era -> ChainAccountState
ledgerSlotNo :: SlotNo
ledgerEpochNo :: Maybe EpochNo
ledgerIx :: TxIx
ledgerPp :: PParams era
ledgerAccount :: ChainAccountState
..} = LedgerEnv era
env
     in Encode ('Closed 'Dense) (LedgerEnv era) -> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode (Encode ('Closed 'Dense) (LedgerEnv era) -> Encoding)
-> Encode ('Closed 'Dense) (LedgerEnv era) -> Encoding
forall a b. (a -> b) -> a -> b
$
          (SlotNo
 -> Maybe EpochNo
 -> TxIx
 -> PParams era
 -> ChainAccountState
 -> LedgerEnv era)
-> Encode
     ('Closed 'Dense)
     (SlotNo
      -> Maybe EpochNo
      -> TxIx
      -> PParams era
      -> ChainAccountState
      -> LedgerEnv era)
forall t. t -> Encode ('Closed 'Dense) t
Rec SlotNo
-> Maybe EpochNo
-> TxIx
-> PParams era
-> ChainAccountState
-> LedgerEnv era
forall era.
SlotNo
-> Maybe EpochNo
-> TxIx
-> PParams era
-> ChainAccountState
-> LedgerEnv era
LedgerEnv
            Encode
  ('Closed 'Dense)
  (SlotNo
   -> Maybe EpochNo
   -> TxIx
   -> PParams era
   -> ChainAccountState
   -> LedgerEnv era)
-> Encode ('Closed 'Dense) SlotNo
-> Encode
     ('Closed 'Dense)
     (Maybe EpochNo
      -> TxIx -> PParams era -> ChainAccountState -> LedgerEnv era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> SlotNo -> Encode ('Closed 'Dense) SlotNo
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To SlotNo
ledgerSlotNo
            Encode
  ('Closed 'Dense)
  (Maybe EpochNo
   -> TxIx -> PParams era -> ChainAccountState -> LedgerEnv era)
-> Encode ('Closed 'Dense) (Maybe EpochNo)
-> Encode
     ('Closed 'Dense)
     (TxIx -> PParams era -> ChainAccountState -> LedgerEnv era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Maybe EpochNo -> Encode ('Closed 'Dense) (Maybe EpochNo)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Maybe EpochNo
ledgerEpochNo
            Encode
  ('Closed 'Dense)
  (TxIx -> PParams era -> ChainAccountState -> LedgerEnv era)
-> Encode ('Closed 'Dense) TxIx
-> Encode
     ('Closed 'Dense)
     (PParams era -> ChainAccountState -> LedgerEnv era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> TxIx -> Encode ('Closed 'Dense) TxIx
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To TxIx
ledgerIx
            Encode
  ('Closed 'Dense)
  (PParams era -> ChainAccountState -> LedgerEnv era)
-> Encode ('Closed 'Dense) (PParams era)
-> Encode ('Closed 'Dense) (ChainAccountState -> LedgerEnv era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> PParams era -> Encode ('Closed 'Dense) (PParams era)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To PParams era
ledgerPp
            Encode ('Closed 'Dense) (ChainAccountState -> LedgerEnv era)
-> Encode ('Closed 'Dense) ChainAccountState
-> Encode ('Closed 'Dense) (LedgerEnv era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> ChainAccountState -> Encode ('Closed 'Dense) ChainAccountState
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To ChainAccountState
ledgerAccount

data ShelleyLedgerPredFailure era
  = UtxowFailure (PredicateFailure (EraRule "UTXOW" era)) -- Subtransition Failures
  | DelegsFailure (PredicateFailure (EraRule "DELEGS" era)) -- Subtransition Failures
  deriving ((forall x.
 ShelleyLedgerPredFailure era
 -> Rep (ShelleyLedgerPredFailure era) x)
-> (forall x.
    Rep (ShelleyLedgerPredFailure era) x
    -> ShelleyLedgerPredFailure era)
-> Generic (ShelleyLedgerPredFailure era)
forall x.
Rep (ShelleyLedgerPredFailure era) x
-> ShelleyLedgerPredFailure era
forall x.
ShelleyLedgerPredFailure era
-> Rep (ShelleyLedgerPredFailure era) x
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
$cfrom :: forall era x.
ShelleyLedgerPredFailure era
-> Rep (ShelleyLedgerPredFailure era) x
from :: forall x.
ShelleyLedgerPredFailure era
-> Rep (ShelleyLedgerPredFailure era) x
$cto :: forall era x.
Rep (ShelleyLedgerPredFailure era) x
-> ShelleyLedgerPredFailure era
to :: forall x.
Rep (ShelleyLedgerPredFailure era) x
-> ShelleyLedgerPredFailure era
Generic)

ledgerSlotNoL :: Lens' (LedgerEnv era) SlotNo
ledgerSlotNoL :: forall era (f :: * -> *).
Functor f =>
(SlotNo -> f SlotNo) -> LedgerEnv era -> f (LedgerEnv era)
ledgerSlotNoL = (LedgerEnv era -> SlotNo)
-> (LedgerEnv era -> SlotNo -> LedgerEnv era)
-> forall {f :: * -> *}.
   Functor f =>
   (SlotNo -> f SlotNo) -> LedgerEnv era -> f (LedgerEnv era)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens LedgerEnv era -> SlotNo
forall era. LedgerEnv era -> SlotNo
ledgerSlotNo ((LedgerEnv era -> SlotNo -> LedgerEnv era)
 -> forall {f :: * -> *}.
    Functor f =>
    (SlotNo -> f SlotNo) -> LedgerEnv era -> f (LedgerEnv era))
-> (LedgerEnv era -> SlotNo -> LedgerEnv era)
-> forall {f :: * -> *}.
   Functor f =>
   (SlotNo -> f SlotNo) -> LedgerEnv era -> f (LedgerEnv era)
forall a b. (a -> b) -> a -> b
$ \LedgerEnv era
x SlotNo
y -> LedgerEnv era
x {ledgerSlotNo = y}

ledgerEpochNoL :: Lens' (LedgerEnv era) (Maybe EpochNo)
ledgerEpochNoL :: forall era (f :: * -> *).
Functor f =>
(Maybe EpochNo -> f (Maybe EpochNo))
-> LedgerEnv era -> f (LedgerEnv era)
ledgerEpochNoL = (LedgerEnv era -> Maybe EpochNo)
-> (LedgerEnv era -> Maybe EpochNo -> LedgerEnv era)
-> forall {f :: * -> *}.
   Functor f =>
   (Maybe EpochNo -> f (Maybe EpochNo))
   -> LedgerEnv era -> f (LedgerEnv era)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens LedgerEnv era -> Maybe EpochNo
forall era. LedgerEnv era -> Maybe EpochNo
ledgerEpochNo ((LedgerEnv era -> Maybe EpochNo -> LedgerEnv era)
 -> forall {f :: * -> *}.
    Functor f =>
    (Maybe EpochNo -> f (Maybe EpochNo))
    -> LedgerEnv era -> f (LedgerEnv era))
-> (LedgerEnv era -> Maybe EpochNo -> LedgerEnv era)
-> forall {f :: * -> *}.
   Functor f =>
   (Maybe EpochNo -> f (Maybe EpochNo))
   -> LedgerEnv era -> f (LedgerEnv era)
forall a b. (a -> b) -> a -> b
$ \LedgerEnv era
x Maybe EpochNo
y -> LedgerEnv era
x {ledgerEpochNo = y}

ledgerIxL :: Lens' (LedgerEnv era) TxIx
ledgerIxL :: forall era (f :: * -> *).
Functor f =>
(TxIx -> f TxIx) -> LedgerEnv era -> f (LedgerEnv era)
ledgerIxL = (LedgerEnv era -> TxIx)
-> (LedgerEnv era -> TxIx -> LedgerEnv era)
-> forall {f :: * -> *}.
   Functor f =>
   (TxIx -> f TxIx) -> LedgerEnv era -> f (LedgerEnv era)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens LedgerEnv era -> TxIx
forall era. LedgerEnv era -> TxIx
ledgerIx ((LedgerEnv era -> TxIx -> LedgerEnv era)
 -> forall {f :: * -> *}.
    Functor f =>
    (TxIx -> f TxIx) -> LedgerEnv era -> f (LedgerEnv era))
-> (LedgerEnv era -> TxIx -> LedgerEnv era)
-> forall {f :: * -> *}.
   Functor f =>
   (TxIx -> f TxIx) -> LedgerEnv era -> f (LedgerEnv era)
forall a b. (a -> b) -> a -> b
$ \LedgerEnv era
x TxIx
y -> LedgerEnv era
x {ledgerIx = y}

ledgerPpL :: Lens' (LedgerEnv era) (PParams era)
ledgerPpL :: forall era (f :: * -> *).
Functor f =>
(PParams era -> f (PParams era))
-> LedgerEnv era -> f (LedgerEnv era)
ledgerPpL = (LedgerEnv era -> PParams era)
-> (LedgerEnv era -> PParams era -> LedgerEnv era)
-> forall {f :: * -> *}.
   Functor f =>
   (PParams era -> f (PParams era))
   -> LedgerEnv era -> f (LedgerEnv era)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens LedgerEnv era -> PParams era
forall era. LedgerEnv era -> PParams era
ledgerPp ((LedgerEnv era -> PParams era -> LedgerEnv era)
 -> forall {f :: * -> *}.
    Functor f =>
    (PParams era -> f (PParams era))
    -> LedgerEnv era -> f (LedgerEnv era))
-> (LedgerEnv era -> PParams era -> LedgerEnv era)
-> forall {f :: * -> *}.
   Functor f =>
   (PParams era -> f (PParams era))
   -> LedgerEnv era -> f (LedgerEnv era)
forall a b. (a -> b) -> a -> b
$ \LedgerEnv era
x PParams era
y -> LedgerEnv era
x {ledgerPp = y}

ledgerAccountL :: Lens' (LedgerEnv era) ChainAccountState
ledgerAccountL :: forall era (f :: * -> *).
Functor f =>
(ChainAccountState -> f ChainAccountState)
-> LedgerEnv era -> f (LedgerEnv era)
ledgerAccountL = (LedgerEnv era -> ChainAccountState)
-> (LedgerEnv era -> ChainAccountState -> LedgerEnv era)
-> forall {f :: * -> *}.
   Functor f =>
   (ChainAccountState -> f ChainAccountState)
   -> LedgerEnv era -> f (LedgerEnv era)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens LedgerEnv era -> ChainAccountState
forall era. LedgerEnv era -> ChainAccountState
ledgerAccount ((LedgerEnv era -> ChainAccountState -> LedgerEnv era)
 -> forall {f :: * -> *}.
    Functor f =>
    (ChainAccountState -> f ChainAccountState)
    -> LedgerEnv era -> f (LedgerEnv era))
-> (LedgerEnv era -> ChainAccountState -> LedgerEnv era)
-> forall {f :: * -> *}.
   Functor f =>
   (ChainAccountState -> f ChainAccountState)
   -> LedgerEnv era -> f (LedgerEnv era)
forall a b. (a -> b) -> a -> b
$ \LedgerEnv era
x ChainAccountState
y -> LedgerEnv era
x {ledgerAccount = y}

type instance EraRuleFailure "LEDGER" ShelleyEra = ShelleyLedgerPredFailure ShelleyEra

instance InjectRuleFailure "LEDGER" ShelleyLedgerPredFailure ShelleyEra

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

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

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

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

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

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

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

type instance EraRuleEvent "LEDGER" ShelleyEra = ShelleyLedgerEvent ShelleyEra

data ShelleyLedgerEvent era
  = UtxowEvent (Event (EraRule "UTXOW" era))
  | DelegsEvent (Event (EraRule "DELEGS" era))
  deriving ((forall x.
 ShelleyLedgerEvent era -> Rep (ShelleyLedgerEvent era) x)
-> (forall x.
    Rep (ShelleyLedgerEvent era) x -> ShelleyLedgerEvent era)
-> Generic (ShelleyLedgerEvent era)
forall x. Rep (ShelleyLedgerEvent era) x -> ShelleyLedgerEvent era
forall x. ShelleyLedgerEvent era -> Rep (ShelleyLedgerEvent era) x
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
$cfrom :: forall era x.
ShelleyLedgerEvent era -> Rep (ShelleyLedgerEvent era) x
from :: forall x. ShelleyLedgerEvent era -> Rep (ShelleyLedgerEvent era) x
$cto :: forall era x.
Rep (ShelleyLedgerEvent era) x -> ShelleyLedgerEvent era
to :: forall x. Rep (ShelleyLedgerEvent era) x -> ShelleyLedgerEvent era
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 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 "UTXOW" era) -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR PredicateFailure (EraRule "UTXOW" era)
a
    (DelegsFailure PredicateFailure (EraRule "DELEGS" 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 "DELEGS" era) -> Encoding
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 =
    Text
-> (Word -> Decoder s (Int, ShelleyLedgerPredFailure era))
-> Decoder s (ShelleyLedgerPredFailure era)
forall s a. Text -> (Word -> Decoder s (Int, a)) -> Decoder s a
decodeRecordSum Text
"PredicateFailure (LEDGER era)" ((Word -> Decoder s (Int, ShelleyLedgerPredFailure era))
 -> Decoder s (ShelleyLedgerPredFailure era))
-> (Word -> Decoder s (Int, ShelleyLedgerPredFailure era))
-> Decoder s (ShelleyLedgerPredFailure era)
forall a b. (a -> b) -> a -> b
$
      \case
        Word
0 -> do
          PredicateFailure (EraRule "UTXOW" era)
a <- Decoder s (PredicateFailure (EraRule "UTXOW" era))
forall s. Decoder s (PredicateFailure (EraRule "UTXOW" era))
forall a s. DecCBOR a => Decoder s a
decCBOR
          (Int, ShelleyLedgerPredFailure era)
-> Decoder s (Int, ShelleyLedgerPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, PredicateFailure (EraRule "UTXOW" era)
-> ShelleyLedgerPredFailure era
forall era.
PredicateFailure (EraRule "UTXOW" era)
-> ShelleyLedgerPredFailure era
UtxowFailure PredicateFailure (EraRule "UTXOW" era)
a)
        Word
1 -> do
          PredicateFailure (EraRule "DELEGS" era)
a <- Decoder s (PredicateFailure (EraRule "DELEGS" era))
forall s. Decoder s (PredicateFailure (EraRule "DELEGS" era))
forall a s. DecCBOR a => Decoder s a
decCBOR
          (Int, ShelleyLedgerPredFailure era)
-> Decoder s (Int, ShelleyLedgerPredFailure era)
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
2, PredicateFailure (EraRule "DELEGS" era)
-> ShelleyLedgerPredFailure era
forall era.
PredicateFailure (EraRule "DELEGS" era)
-> ShelleyLedgerPredFailure era
DelegsFailure PredicateFailure (EraRule "DELEGS" era)
a)
        Word
k -> Word -> Decoder s (Int, ShelleyLedgerPredFailure era)
forall a (m :: * -> *). (Typeable a, MonadFail m) => Word -> m a
invalidKey Word
k

shelleyLedgerAssertions ::
  ( EraGov era
  , EraCertState era
  , State (rule era) ~ LedgerState era
  ) =>
  [Assertion (rule era)]
shelleyLedgerAssertions :: forall era (rule :: * -> *).
(EraGov era, EraCertState era,
 State (rule era) ~ LedgerState era) =>
[Assertion (rule era)]
shelleyLedgerAssertions =
  [ String
-> (TRC (rule era) -> State (rule era) -> Bool)
-> Assertion (rule era)
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) -> CertState era -> UTxOState era -> Bool
forall era.
(EraGov era, EraCertState era) =>
CertState era -> UTxOState era -> Bool
potEqualsObligation CertState era
dpstate UTxOState era
utxoSt
      )
  ]

instance
  ( EraTx era
  , EraGov era
  , EraCertState 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 = [TransitionRule (ShelleyLEDGER era)
forall era.
(EraTx era, STS (ShelleyLEDGER 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 = AssertionViolation (ShelleyLEDGER 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
renderDepositEqualsObligationViolation

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

ledgerTransition ::
  forall era.
  ( EraTx era
  , STS (ShelleyLEDGER 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, STS (ShelleyLEDGER 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 Maybe EpochNo
mbCurEpochNo TxIx
txIx PParams era
pp ChainAccountState
account, LedgerState UTxOState era
utxoSt CertState era
certState, Signal (ShelleyLEDGER era)
tx) <-
    Rule
  (ShelleyLEDGER era)
  'Transition
  (RuleContext 'Transition (ShelleyLEDGER era))
F (Clause (ShelleyLEDGER era) 'Transition)
  (TRC (ShelleyLEDGER era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
  EpochNo
curEpochNo <- F (Clause (ShelleyLEDGER era) 'Transition) EpochNo
-> (EpochNo -> F (Clause (ShelleyLEDGER era) 'Transition) EpochNo)
-> Maybe EpochNo
-> F (Clause (ShelleyLEDGER era) 'Transition) EpochNo
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (BaseM (ShelleyLEDGER era) EpochNo
-> F (Clause (ShelleyLEDGER era) 'Transition) EpochNo
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (ShelleyLEDGER era) EpochNo
 -> F (Clause (ShelleyLEDGER era) 'Transition) EpochNo)
-> BaseM (ShelleyLEDGER era) EpochNo
-> F (Clause (ShelleyLEDGER era) 'Transition) EpochNo
forall a b. (a -> b) -> a -> b
$ SlotNo -> Reader Globals EpochNo
epochFromSlot SlotNo
slot) EpochNo -> F (Clause (ShelleyLEDGER era) 'Transition) EpochNo
forall a. a -> F (Clause (ShelleyLEDGER era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe EpochNo
mbCurEpochNo
  CertState era
certState' <-
    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
      (ShelleyLEDGER era) 'Transition (State (EraRule "DELEGS" era)))
-> RuleContext 'Transition (EraRule "DELEGS" era)
-> Rule
     (ShelleyLEDGER 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 (ShelleyLEDGER 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
$ Tx era
Signal (ShelleyLEDGER era)
tx Tx era
-> Getting
     (StrictSeq (TxCert era)) (Tx era) (StrictSeq (TxCert era))
-> StrictSeq (TxCert era)
forall s a. s -> Getting a s a -> a
^. (TxBody era -> Const (StrictSeq (TxCert era)) (TxBody era))
-> Tx era -> Const (StrictSeq (TxCert era)) (Tx era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL ((TxBody era -> Const (StrictSeq (TxCert era)) (TxBody era))
 -> Tx era -> Const (StrictSeq (TxCert era)) (Tx era))
-> ((StrictSeq (TxCert era)
     -> Const (StrictSeq (TxCert era)) (StrictSeq (TxCert era)))
    -> TxBody era -> Const (StrictSeq (TxCert era)) (TxBody era))
-> Getting
     (StrictSeq (TxCert era)) (Tx era) (StrictSeq (TxCert era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StrictSeq (TxCert era)
 -> Const (StrictSeq (TxCert era)) (StrictSeq (TxCert era)))
-> TxBody era -> Const (StrictSeq (TxCert era)) (TxBody era)
forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictSeq (TxCert 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) (RuleContext 'Transition (EraRule "UTXOW" era)
 -> Rule
      (ShelleyLEDGER era) 'Transition (State (EraRule "UTXOW" era)))
-> RuleContext 'Transition (EraRule "UTXOW" era)
-> Rule
     (ShelleyLEDGER 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
        ( SlotNo -> PParams era -> CertState era -> UtxoEnv era
forall era. SlotNo -> PParams era -> CertState era -> UtxoEnv era
UtxoEnv SlotNo
slot PParams era
pp CertState era
certState
        , State (EraRule "UTXOW" era)
UTxOState era
utxoSt
        , Signal (EraRule "UTXOW" era)
Signal (ShelleyLEDGER era)
tx
        )
  LedgerState era
-> F (Clause (ShelleyLEDGER era) 'Transition) (LedgerState era)
forall a. a -> F (Clause (ShelleyLEDGER era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UTxOState era -> CertState era -> LedgerState era
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 = PredicateFailure (EraRule "DELEGS" era)
-> ShelleyLedgerPredFailure era
PredicateFailure (ShelleyDELEGS era)
-> PredicateFailure (ShelleyLEDGER era)
forall era.
PredicateFailure (EraRule "DELEGS" era)
-> ShelleyLedgerPredFailure era
DelegsFailure
  wrapEvent :: Event (ShelleyDELEGS era) -> Event (ShelleyLEDGER era)
wrapEvent = Event (EraRule "DELEGS" era) -> ShelleyLedgerEvent era
Event (ShelleyDELEGS era) -> Event (ShelleyLEDGER era)
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 = PredicateFailure (EraRule "UTXOW" era)
-> ShelleyLedgerPredFailure era
PredicateFailure (ShelleyUTXOW era)
-> PredicateFailure (ShelleyLEDGER era)
forall era.
PredicateFailure (EraRule "UTXOW" era)
-> ShelleyLedgerPredFailure era
UtxowFailure
  wrapEvent :: Event (ShelleyUTXOW era) -> Event (ShelleyLEDGER era)
wrapEvent = Event (EraRule "UTXOW" era) -> ShelleyLedgerEvent era
Event (ShelleyUTXOW era) -> Event (ShelleyLEDGER era)
forall era. Event (EraRule "UTXOW" era) -> ShelleyLedgerEvent era
UtxowEvent

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

renderDepositEqualsObligationViolation ::
  ( EraTx era
  , EraGov era
  , EraCertState era
  , Environment t ~ LedgerEnv era
  , Signal t ~ Tx era
  , State t ~ LedgerState era
  ) =>
  AssertionViolation t ->
  String
renderDepositEqualsObligationViolation :: forall era t.
(EraTx era, EraGov era, EraCertState era,
 Environment t ~ LedgerEnv era, Signal t ~ Tx era,
 State t ~ LedgerState era) =>
AssertionViolation t -> String
renderDepositEqualsObligationViolation
  AssertionViolation {String
avSTS :: String
avSTS :: forall sts. AssertionViolation sts -> String
avSTS, String
avMsg :: String
avMsg :: forall sts. AssertionViolation sts -> String
avMsg, avCtx :: forall sts. AssertionViolation sts -> TRC sts
avCtx = TRC (LedgerEnv SlotNo
slot Maybe EpochNo
_ TxIx
_ PParams era
pp ChainAccountState
_, State t
_, Signal t
tx), Maybe (State t)
avState :: Maybe (State t)
avState :: forall sts. AssertionViolation sts -> Maybe (State sts)
avState} =
    case Maybe (State t)
avState of
      Maybe (State t)
Nothing -> String
"\nAssertionViolation " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
avSTS String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
avMsg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" (avState is Nothing)."
      Just State t
lstate ->
        let certstate :: CertState era
certstate = LedgerState era -> CertState era
forall era. LedgerState era -> CertState era
lsCertState State t
LedgerState era
lstate
            utxoSt :: UTxOState era
utxoSt = LedgerState era -> UTxOState era
forall era. LedgerState era -> UTxOState era
lsUTxOState State t
LedgerState era
lstate
            utxo :: UTxO era
utxo = UTxOState era -> UTxO era
forall era. UTxOState era -> UTxO era
utxosUtxo UTxOState era
utxoSt
            txb :: TxBody era
txb = Tx era
Signal t
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
            pot :: Coin
pot = UTxOState era
utxoSt UTxOState era -> Getting Coin (UTxOState era) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (UTxOState era) Coin
forall era (f :: * -> *).
Functor f =>
(Coin -> f Coin) -> UTxOState era -> f (UTxOState era)
utxosDepositedL
         in String
"\n\nAssertionViolation ("
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
avSTS
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")\n\n  "
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
avMsg
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\n\nCERTS\n"
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> TxBody era -> String
forall era. EraTxBody era => TxBody era -> String
showTxCerts TxBody era
txb
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\n(slot,keyDeposit,poolDeposit) "
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> (SlotNo, Coin, Coin) -> String
forall a. Show a => a -> String
show (SlotNo
slot, PParams era
pp PParams era -> Getting Coin (PParams era) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (PParams era) Coin
forall era. EraPParams era => Lens' (PParams era) Coin
Lens' (PParams era) Coin
ppKeyDepositL, PParams era
pp PParams era -> Getting Coin (PParams era) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (PParams era) Coin
forall era. EraPParams era => Lens' (PParams era) Coin
Lens' (PParams era) Coin
ppPoolDepositL)
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\nThe Pot (utxosDeposited) = "
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Coin -> String
forall a. Show a => a -> String
show Coin
pot
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\n"
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Obligations -> String
forall a. Show a => a -> String
show (CertState era -> GovState era -> Obligations
forall era.
(EraGov era, EraCertState era) =>
CertState era -> GovState era -> Obligations
allObligations CertState era
certstate (UTxOState era -> GovState era
forall era. UTxOState era -> GovState era
utxosGovState UTxOState era
utxoSt))
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\nConsumed = "
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Consumed -> String
forall a. Show a => a -> String
show (TxBody era -> PParams era -> CertState era -> UTxO era -> Consumed
forall era.
(EraTxBody era, EraCertState era) =>
TxBody era -> PParams era -> CertState era -> UTxO era -> Consumed
consumedTxBody TxBody era
txb PParams era
pp CertState era
certstate UTxO era
utxo)
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\nProduced = "
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Produced -> String
forall a. Show a => a -> String
show (TxBody era -> PParams era -> CertState era -> Produced
forall era.
(EraTxBody era, EraCertState era) =>
TxBody era -> PParams era -> CertState era -> Produced
producedTxBody TxBody era
txb PParams era
pp CertState era
certstate)