{-# 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,
  ledgerMempoolL,
  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 (
  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, epochFromSlot)
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 -> 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 Maybe EpochNo
_ 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
_ Maybe EpochNo
_ TxIx
_ PParams era
_ AccountState
_ Bool
_) =
    let LedgerEnv {Bool
Maybe EpochNo
PParams era
TxIx
SlotNo
AccountState
ledgerMempool :: Bool
ledgerAccount :: AccountState
ledgerPp :: PParams era
ledgerIx :: TxIx
ledgerEpochNo :: Maybe EpochNo
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
ledgerEpochNo :: forall era. LedgerEnv era -> Maybe EpochNo
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
-> Maybe EpochNo
-> 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 Maybe EpochNo
ledgerEpochNo
            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)) -- Subtransition Failures
  | DelegsFailure (PredicateFailure (EraRule "DELEGS" era)) -- Subtransition Failures
  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)

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

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

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

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

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

ledgerMempoolL :: Lens' (LedgerEnv era) Bool
ledgerMempoolL :: forall era. Lens' (LedgerEnv era) Bool
ledgerMempoolL = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens forall era. LedgerEnv era -> Bool
ledgerMempool forall a b. (a -> b) -> a -> b
$ \LedgerEnv era
x Bool
y -> LedgerEnv era
x {ledgerMempool :: Bool
ledgerMempool = Bool
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 = forall era.
PredicateFailure (EraRule "UTXOW" era)
-> ShelleyLedgerPredFailure era
UtxowFailure

instance InjectRuleFailure "LEDGER" ShelleyUtxoPredFailure ShelleyEra where
  injectFailure :: ShelleyUtxoPredFailure ShelleyEra
-> EraRuleFailure "LEDGER" ShelleyEra
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 where
  injectFailure :: ShelleyPpupPredFailure ShelleyEra
-> EraRuleFailure "LEDGER" ShelleyEra
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 where
  injectFailure :: ShelleyDelegsPredFailure ShelleyEra
-> EraRuleFailure "LEDGER" ShelleyEra
injectFailure = forall era.
PredicateFailure (EraRule "DELEGS" era)
-> ShelleyLedgerPredFailure era
DelegsFailure

instance InjectRuleFailure "LEDGER" ShelleyDelplPredFailure ShelleyEra where
  injectFailure :: ShelleyDelplPredFailure ShelleyEra
-> EraRuleFailure "LEDGER" ShelleyEra
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 where
  injectFailure :: ShelleyPoolPredFailure ShelleyEra
-> EraRuleFailure "LEDGER" ShelleyEra
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 where
  injectFailure :: ShelleyDelegPredFailure ShelleyEra
-> EraRuleFailure "LEDGER" ShelleyEra
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 = ShelleyLedgerEvent ShelleyEra

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

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
  ( 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, 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 = 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
  , 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 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
  EpochNo
curEpochNo <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS forall a b. (a -> b) -> a -> b
$ SlotNo -> Reader Globals EpochNo
epochFromSlot SlotNo
slot) 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) forall a b. (a -> b) -> a -> b
$
      forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC
        ( forall era.
SlotNo
-> EpochNo
-> TxIx
-> PParams era
-> Tx era
-> AccountState
-> DelegsEnv era
DelegsEnv SlotNo
slot EpochNo
curEpochNo 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 Maybe EpochNo
_ 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)