{-# 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.BaseTypes (ShelleyBase, TxIx, invalidKey, networkId)
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 (
  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.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 Withdrawals
  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
    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 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
3 :: Word8) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Withdrawals -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Withdrawals
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
          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
2 -> do
          Withdrawals
w <- Decoder s Withdrawals
forall s. Decoder s Withdrawals
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, Withdrawals -> ShelleyLedgerPredFailure era
forall era. Withdrawals -> ShelleyLedgerPredFailure era
ShelleyWithdrawalsMissingAccounts Withdrawals
w)
        Word
3 -> do
          Withdrawals
w <- Decoder s Withdrawals
forall s. Decoder s Withdrawals
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, Withdrawals -> ShelleyLedgerPredFailure era
forall era. Withdrawals -> ShelleyLedgerPredFailure era
ShelleyIncompleteWithdrawals Withdrawals
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 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 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 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 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 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 era,
 EraRule "LEDGER" era ~ ShelleyLEDGER era,
 InjectRuleFailure "LEDGER" ShelleyLedgerPredFailure 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
  let withdrawals :: Withdrawals
withdrawals = Tx era
Signal (ShelleyLEDGER era)
tx Tx era -> Getting Withdrawals (Tx era) Withdrawals -> Withdrawals
forall s a. s -> Getting a s a -> a
^. (TxBody era -> Const Withdrawals (TxBody era))
-> Tx era -> Const Withdrawals (Tx era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL ((TxBody era -> Const Withdrawals (TxBody era))
 -> Tx era -> Const Withdrawals (Tx era))
-> ((Withdrawals -> Const Withdrawals Withdrawals)
    -> TxBody era -> Const Withdrawals (TxBody era))
-> Getting Withdrawals (Tx era) Withdrawals
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Withdrawals -> Const Withdrawals Withdrawals)
-> TxBody era -> Const Withdrawals (TxBody era)
forall era. EraTxBody era => Lens' (TxBody era) Withdrawals
Lens' (TxBody era) Withdrawals
withdrawalsTxBodyL
  Accounts era
-> Withdrawals -> Rule (ShelleyLEDGER era) 'Transition ()
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 (CertState era
certState CertState era
-> Getting (Accounts era) (CertState era) (Accounts era)
-> Accounts era
forall s a. s -> Getting a s a -> a
^. (DState era -> Const (Accounts era) (DState era))
-> CertState era -> Const (Accounts era) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era -> Const (Accounts era) (DState era))
 -> CertState era -> Const (Accounts era) (CertState era))
-> ((Accounts era -> Const (Accounts era) (Accounts era))
    -> DState era -> Const (Accounts era) (DState era))
-> Getting (Accounts era) (CertState era) (Accounts era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Accounts era -> Const (Accounts era) (Accounts era))
-> DState era -> Const (Accounts era) (DState era)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL) Withdrawals
withdrawals
  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
certState CertState era -> (CertState era -> CertState era) -> CertState era
forall a b. a -> (a -> b) -> b
& (DState era -> Identity (DState era))
-> CertState era -> Identity (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era -> Identity (DState era))
 -> CertState era -> Identity (CertState era))
-> ((Accounts era -> Identity (Accounts era))
    -> DState era -> Identity (DState era))
-> (Accounts era -> Identity (Accounts era))
-> CertState era
-> Identity (CertState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Accounts era -> Identity (Accounts era))
-> DState era -> Identity (DState era)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL ((Accounts era -> Identity (Accounts era))
 -> CertState era -> Identity (CertState era))
-> (Accounts era -> Accounts era) -> CertState era -> CertState era
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ Withdrawals -> Accounts era -> Accounts era
forall era.
EraAccounts era =>
Withdrawals -> Accounts era -> Accounts era
drainAccounts Withdrawals
withdrawals
        , 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')

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
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 (Maybe Withdrawals
missingWithdrawals, Maybe Withdrawals
incompleteWithdrawals) =
        case Withdrawals
-> Network -> Accounts era -> Maybe (Withdrawals, Withdrawals)
forall era.
EraAccounts era =>
Withdrawals
-> Network -> Accounts era -> Maybe (Withdrawals, Withdrawals)
withdrawalsThatDoNotDrainAccounts Withdrawals
withdrawals Network
network Accounts era
accounts of
          Maybe (Withdrawals, Withdrawals)
Nothing -> (Maybe Withdrawals
forall a. Maybe a
Nothing, Maybe Withdrawals
forall a. Maybe a
Nothing)
          Just (Withdrawals
missing, Withdrawals
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 Coin -> Bool
forall a. Map RewardAccount a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Withdrawals -> Map RewardAccount Coin
unWithdrawals Withdrawals
incomplete) then Maybe Withdrawals
forall a. Maybe a
Nothing else Withdrawals -> Maybe Withdrawals
forall a. a -> Maybe a
Just Withdrawals
incomplete
            )
  Maybe Withdrawals
-> (Withdrawals -> PredicateFailure sts) -> Rule sts ctx ()
forall a sts (ctx :: RuleType).
Maybe a -> (a -> PredicateFailure sts) -> Rule sts ctx ()
failOnJust Maybe Withdrawals
missingWithdrawals ((Withdrawals -> PredicateFailure sts) -> Rule sts ctx ())
-> (Withdrawals -> PredicateFailure sts) -> Rule sts ctx ()
forall a b. (a -> b) -> a -> b
$ ShelleyLedgerPredFailure era -> EraRuleFailure "LEDGER" era
ShelleyLedgerPredFailure era -> PredicateFailure sts
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure (ShelleyLedgerPredFailure era -> PredicateFailure sts)
-> (Withdrawals -> ShelleyLedgerPredFailure era)
-> Withdrawals
-> PredicateFailure sts
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Withdrawals -> ShelleyLedgerPredFailure era
forall era. Withdrawals -> ShelleyLedgerPredFailure era
ShelleyWithdrawalsMissingAccounts
  Maybe Withdrawals
-> (Withdrawals -> PredicateFailure sts) -> Rule sts ctx ()
forall a sts (ctx :: RuleType).
Maybe a -> (a -> PredicateFailure sts) -> Rule sts ctx ()
failOnJust Maybe Withdrawals
incompleteWithdrawals ((Withdrawals -> PredicateFailure sts) -> Rule sts ctx ())
-> (Withdrawals -> PredicateFailure sts) -> Rule sts ctx ()
forall a b. (a -> b) -> a -> b
$ ShelleyLedgerPredFailure era -> EraRuleFailure "LEDGER" era
ShelleyLedgerPredFailure era -> PredicateFailure sts
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure (ShelleyLedgerPredFailure era -> PredicateFailure sts)
-> (Withdrawals -> ShelleyLedgerPredFailure era)
-> Withdrawals
-> PredicateFailure sts
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Withdrawals -> ShelleyLedgerPredFailure era
forall era. Withdrawals -> ShelleyLedgerPredFailure era
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 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, 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 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)