{-# 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,
  testIncompleteAndMissingWithdrawals,
) where

import Cardano.Ledger.Address (RewardAccount)
import Cardano.Ledger.BaseTypes (Mismatch, Relation (..), ShelleyBase, TxIx, invalidKey, networkId)
import Cardano.Ledger.Binary (
  DecCBOR (..),
  EncCBOR (..),
  decodeRecordSum,
  encodeListLen,
 )
import Cardano.Ledger.Binary.Coders (Encode (..), encode, (!>))
import Cardano.Ledger.Coin (Coin)
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 (
  Accounts,
  EraAccounts,
  EraCertState (..),
  accountsL,
  drainAccounts,
  withdrawalsThatDoNotDrainAccounts,
 )
import Control.DeepSeq (NFData (..))
import Control.Monad.Trans.Reader (asks)
import Control.State.Transition (
  Assertion (PostCondition),
  AssertionViolation (..),
  Embed (..),
  Rule,
  STS (..),
  TRC (..),
  TransitionRule,
  failOnJust,
  judgmentContext,
  liftSTS,
  trans,
 )
import Data.Map.Strict (Map)
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
  | ShelleyWithdrawalsMissingAccounts Withdrawals
  | ShelleyIncompleteWithdrawals (Map RewardAccount (Mismatch RelEQ Coin))
  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)
-> Lens (LedgerEnv era) (LedgerEnv era) SlotNo SlotNo
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)
 -> Lens (LedgerEnv era) (LedgerEnv era) SlotNo SlotNo)
-> (LedgerEnv era -> SlotNo -> LedgerEnv era)
-> Lens (LedgerEnv era) (LedgerEnv era) SlotNo SlotNo
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)
-> Lens
     (LedgerEnv era) (LedgerEnv era) (Maybe EpochNo) (Maybe EpochNo)
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)
 -> Lens
      (LedgerEnv era) (LedgerEnv era) (Maybe EpochNo) (Maybe EpochNo))
-> (LedgerEnv era -> Maybe EpochNo -> LedgerEnv era)
-> Lens
     (LedgerEnv era) (LedgerEnv era) (Maybe EpochNo) (Maybe EpochNo)
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)
-> Lens (LedgerEnv era) (LedgerEnv era) TxIx TxIx
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)
 -> Lens (LedgerEnv era) (LedgerEnv era) TxIx TxIx)
-> (LedgerEnv era -> TxIx -> LedgerEnv era)
-> Lens (LedgerEnv era) (LedgerEnv era) TxIx TxIx
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)
-> Lens (LedgerEnv era) (LedgerEnv era) (PParams era) (PParams 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)
 -> Lens
      (LedgerEnv era) (LedgerEnv era) (PParams era) (PParams era))
-> (LedgerEnv era -> PParams era -> LedgerEnv era)
-> Lens (LedgerEnv era) (LedgerEnv era) (PParams era) (PParams 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)
-> Lens
     (LedgerEnv era) (LedgerEnv era) ChainAccountState ChainAccountState
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)
 -> Lens
      (LedgerEnv era)
      (LedgerEnv era)
      ChainAccountState
      ChainAccountState)
-> (LedgerEnv era -> ChainAccountState -> LedgerEnv era)
-> Lens
     (LedgerEnv era) (LedgerEnv era) ChainAccountState ChainAccountState
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
    ShelleyWithdrawalsMissingAccounts Withdrawals
w -> 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
2 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Withdrawals -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Withdrawals
w
    ShelleyIncompleteWithdrawals Map RewardAccount (Mismatch RelEQ Coin)
w -> 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
3 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Map RewardAccount (Mismatch RelEQ Coin) -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Map RewardAccount (Mismatch RelEQ Coin)
w

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
          a <- Decoder s (PredicateFailure (EraRule "UTXOW" era))
forall s. Decoder s (PredicateFailure (EraRule "UTXOW" era))
forall a s. DecCBOR a => Decoder s a
decCBOR
          pure (2, UtxowFailure a)
        Word
1 -> do
          a <- Decoder s (PredicateFailure (EraRule "DELEGS" era))
forall s. Decoder s (PredicateFailure (EraRule "DELEGS" era))
forall a s. DecCBOR a => Decoder s a
decCBOR
          pure (2, DelegsFailure a)
        Word
2 -> do
          w <- Decoder s Withdrawals
forall s. Decoder s Withdrawals
forall a s. DecCBOR a => Decoder s a
decCBOR
          pure (2, ShelleyWithdrawalsMissingAccounts w)
        Word
3 -> do
          w <- Decoder s (Map RewardAccount (Mismatch RelEQ Coin))
forall s. Decoder s (Map RewardAccount (Mismatch RelEQ Coin))
forall a s. DecCBOR a => Decoder s a
decCBOR
          pure (2, ShelleyIncompleteWithdrawals w)
        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 TopTx era
  , Environment (EraRule "DELEGS" era) ~ DelegsEnv era
  , State (EraRule "DELEGS" era) ~ CertState era
  , Signal (EraRule "DELEGS" era) ~ Seq (TxCert era)
  , AtMostEra "Babbage" era
  , EraRule "LEDGER" era ~ ShelleyLEDGER era
  , EraRuleFailure "LEDGER" era ~ ShelleyLedgerPredFailure era
  , InjectRuleFailure "LEDGER" ShelleyLedgerPredFailure era
  ) =>
  STS (ShelleyLEDGER era)
  where
  type State (ShelleyLEDGER era) = LedgerState era
  type Signal (ShelleyLEDGER era) = Tx TopTx 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, EraCertState 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 TopTx era,
 EraRule "LEDGER" era ~ ShelleyLEDGER era,
 InjectRuleFailure "LEDGER" ShelleyLedgerPredFailure 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 TopTx 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
  , EraCertState 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 TopTx era
  , EraRule "LEDGER" era ~ ShelleyLEDGER era
  , InjectRuleFailure "LEDGER" ShelleyLedgerPredFailure era
  ) =>
  TransitionRule (ShelleyLEDGER era)
ledgerTransition :: forall era.
(EraTx era, EraCertState 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 TopTx era,
 EraRule "LEDGER" era ~ ShelleyLEDGER era,
 InjectRuleFailure "LEDGER" ShelleyLedgerPredFailure era) =>
TransitionRule (ShelleyLEDGER era)
ledgerTransition = do
  TRC (LedgerEnv slot mbCurEpochNo txIx pp account, LedgerState utxoSt certState, 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
  curEpochNo <- maybe (liftSTS $ epochFromSlot slot) pure mbCurEpochNo
  let withdrawals = Tx TopTx era
Signal (ShelleyLEDGER era)
tx Tx TopTx era
-> Getting Withdrawals (Tx TopTx era) Withdrawals -> Withdrawals
forall s a. s -> Getting a s a -> a
^. (TxBody TopTx era -> Const Withdrawals (TxBody TopTx era))
-> Tx TopTx era -> Const Withdrawals (Tx TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l era)
bodyTxL ((TxBody TopTx era -> Const Withdrawals (TxBody TopTx era))
 -> Tx TopTx era -> Const Withdrawals (Tx TopTx era))
-> ((Withdrawals -> Const Withdrawals Withdrawals)
    -> TxBody TopTx era -> Const Withdrawals (TxBody TopTx era))
-> Getting Withdrawals (Tx TopTx era) Withdrawals
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Withdrawals -> Const Withdrawals Withdrawals)
-> TxBody TopTx era -> Const Withdrawals (TxBody TopTx era)
forall era (l :: TxLevel).
EraTxBody era =>
Lens' (TxBody l era) Withdrawals
forall (l :: TxLevel). Lens' (TxBody l era) Withdrawals
withdrawalsTxBodyL
  testIncompleteAndMissingWithdrawals (certState ^. certDStateL . accountsL) withdrawals
  certState' <-
    trans @(EraRule "DELEGS" era) $
      TRC
        ( DelegsEnv slot curEpochNo txIx pp tx account
        , certState & certDStateL . accountsL %~ drainAccounts withdrawals
        , StrictSeq.fromStrict $ tx ^. bodyTxL . certsTxBodyL
        )

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

testIncompleteAndMissingWithdrawals ::
  ( EraAccounts era
  , STS sts
  , BaseM sts ~ ShelleyBase
  , InjectRuleFailure "LEDGER" ShelleyLedgerPredFailure era
  , sts ~ EraRule "LEDGER" era
  ) =>
  Accounts era ->
  Withdrawals ->
  Rule sts ctx ()
testIncompleteAndMissingWithdrawals :: forall era sts (ctx :: RuleType).
(EraAccounts era, STS sts, BaseM sts ~ ShelleyBase,
 InjectRuleFailure "LEDGER" ShelleyLedgerPredFailure era,
 sts ~ EraRule "LEDGER" era) =>
Accounts era -> Withdrawals -> Rule sts ctx ()
testIncompleteAndMissingWithdrawals Accounts era
accounts Withdrawals
withdrawals = do
  network <- BaseM sts Network -> Rule sts ctx Network
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM sts Network -> Rule sts ctx Network)
-> BaseM sts Network -> Rule sts ctx Network
forall a b. (a -> b) -> a -> b
$ (Globals -> Network) -> ReaderT Globals Identity Network
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> Network
networkId
  let (missingWithdrawals, incompleteWithdrawals) =
        case withdrawalsThatDoNotDrainAccounts withdrawals network accounts of
          Maybe (Withdrawals, Map RewardAccount (Mismatch RelEQ Coin))
Nothing -> (Maybe Withdrawals
forall a. Maybe a
Nothing, Maybe (Map RewardAccount (Mismatch RelEQ Coin))
forall a. Maybe a
Nothing)
          Just (Withdrawals
missing, Map RewardAccount (Mismatch RelEQ Coin)
incomplete) ->
            ( if Map RewardAccount Coin -> Bool
forall a. Map RewardAccount a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Withdrawals -> Map RewardAccount Coin
unWithdrawals Withdrawals
missing) then Maybe Withdrawals
forall a. Maybe a
Nothing else Withdrawals -> Maybe Withdrawals
forall a. a -> Maybe a
Just Withdrawals
missing
            , if Map RewardAccount (Mismatch RelEQ Coin) -> Bool
forall a. Map RewardAccount a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Map RewardAccount (Mismatch RelEQ Coin)
incomplete then Maybe (Map RewardAccount (Mismatch RelEQ Coin))
forall a. Maybe a
Nothing else Map RewardAccount (Mismatch RelEQ Coin)
-> Maybe (Map RewardAccount (Mismatch RelEQ Coin))
forall a. a -> Maybe a
Just Map RewardAccount (Mismatch RelEQ Coin)
incomplete
            )
  failOnJust missingWithdrawals $ injectFailure . ShelleyWithdrawalsMissingAccounts
  failOnJust incompleteWithdrawals $ injectFailure . ShelleyIncompleteWithdrawals

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 TopTx 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 TopTx 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 TopTx era
txb = Tx TopTx era
Signal t
tx Tx TopTx era
-> Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
-> TxBody TopTx era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l era)
bodyTxL
            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 TopTx era -> String
forall era (t :: TxLevel). EraTxBody era => TxBody t era -> String
showTxCerts TxBody TopTx 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, HasCallStack) =>
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 TopTx era
-> PParams era -> CertState era -> UTxO era -> Consumed
forall era (l :: TxLevel).
(EraTxBody era, EraCertState era) =>
TxBody l era
-> PParams era -> CertState era -> UTxO era -> Consumed
consumedTxBody TxBody TopTx 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 TopTx era -> PParams era -> CertState era -> Produced
forall era.
(EraTxBody era, EraCertState era) =>
TxBody TopTx era -> PParams era -> CertState era -> Produced
producedTxBody TxBody TopTx era
txb PParams era
pp CertState era
certstate)