{-# 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.Credential (Credential)
import Cardano.Ledger.Shelley.AdaPots (consumedTxBody, producedTxBody)
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.Era (ShelleyEra, ShelleyLEDGER)
import Cardano.Ledger.Shelley.LedgerState (
  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.Shelley.State
import Cardano.Ledger.Slot (EpochNo (..), SlotNo, epochFromSlot)
import Control.DeepSeq (NFData (..))
import Control.Monad (guard)
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 qualified Data.Map.Strict as Map
import Data.Sequence (Seq)
import qualified Data.Sequence.Strict as StrictSeq
import qualified Data.Set as Set
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
      )
  , String
-> (TRC (rule era) -> State (rule era) -> Bool)
-> Assertion (rule era)
forall sts.
String -> (TRC sts -> State sts -> Bool) -> Assertion sts
PostCondition
      String
"Reverse stake pool delegations must match"
      ( \(TRC (Environment (rule era)
_, State (rule era)
_, Signal (rule era)
_))
         (LedgerState UTxOState era
_ CertState era
certState) ->
            (Map (KeyHash StakePool) (Set (Credential Staking))
 -> Map (KeyHash StakePool) (Set (Credential Staking)) -> Bool)
-> (Map (KeyHash StakePool) (Set (Credential Staking)),
    Map (KeyHash StakePool) (Set (Credential Staking)))
-> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Map (KeyHash StakePool) (Set (Credential Staking))
-> Map (KeyHash StakePool) (Set (Credential Staking)) -> Bool
forall a. Eq a => a -> a -> Bool
(==) ((Map (KeyHash StakePool) (Set (Credential Staking)),
  Map (KeyHash StakePool) (Set (Credential Staking)))
 -> Bool)
-> (Map (KeyHash StakePool) (Set (Credential Staking)),
    Map (KeyHash StakePool) (Set (Credential Staking)))
-> Bool
forall a b. (a -> b) -> a -> b
$ CertState era
-> (Map (KeyHash StakePool) (Set (Credential Staking)),
    Map (KeyHash StakePool) (Set (Credential Staking)))
forall era.
EraCertState era =>
CertState era
-> (Map (KeyHash StakePool) (Set (Credential Staking)),
    Map (KeyHash StakePool) (Set (Credential Staking)))
calculateDelegatorsPerStakePool CertState era
certState
      )
  ]

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
        | String
avMsg String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"Deposit pot must equal obligation (LEDGER)" ->
            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, HasCallStack) =>
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)
        | String
avMsg String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"Reverse stake pool delegations must match" ->
            case CertState era
-> (Map (KeyHash StakePool) (Set (Credential Staking)),
    Map (KeyHash StakePool) (Set (Credential Staking)))
forall era.
EraCertState era =>
CertState era
-> (Map (KeyHash StakePool) (Set (Credential Staking)),
    Map (KeyHash StakePool) (Set (Credential Staking)))
calculateDelegatorsPerStakePool (LedgerState era -> CertState era
forall era. LedgerState era -> CertState era
lsCertState State t
LedgerState era
lstate) of
              (Map (KeyHash StakePool) (Set (Credential Staking))
reverseDelegatorsPerStakePool, Map (KeyHash StakePool) (Set (Credential Staking))
delegatorsPerStakePool) ->
                String
avMsg
                  String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\nReverse Delegations: \n  "
                  String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Map (KeyHash StakePool) (Set (Credential Staking)) -> String
forall a. Show a => a -> String
show Map (KeyHash StakePool) (Set (Credential Staking))
reverseDelegatorsPerStakePool
                  String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\nForward Delegations:\n  "
                  String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Map (KeyHash StakePool) (Set (Credential Staking)) -> String
forall a. Show a => a -> String
show Map (KeyHash StakePool) (Set (Credential Staking))
delegatorsPerStakePool
        | Bool
otherwise -> ShowS
forall a. HasCallStack => String -> a
error ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
"Unexpected assertion message: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
avMsg

calculateDelegatorsPerStakePool ::
  EraCertState era =>
  CertState era ->
  ( Map (KeyHash StakePool) (Set.Set (Credential Staking))
  , Map (KeyHash StakePool) (Set.Set (Credential Staking))
  )
calculateDelegatorsPerStakePool :: forall era.
EraCertState era =>
CertState era
-> (Map (KeyHash StakePool) (Set (Credential Staking)),
    Map (KeyHash StakePool) (Set (Credential Staking)))
calculateDelegatorsPerStakePool CertState era
certState =
  let accountsMap :: Map (Credential Staking) (AccountState era)
accountsMap = CertState era
certState CertState era
-> Getting
     (Map (Credential Staking) (AccountState era))
     (CertState era)
     (Map (Credential Staking) (AccountState era))
-> Map (Credential Staking) (AccountState era)
forall s a. s -> Getting a s a -> a
^. (DState era
 -> Const
      (Map (Credential Staking) (AccountState era)) (DState era))
-> CertState era
-> Const
     (Map (Credential Staking) (AccountState era)) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era
  -> Const
       (Map (Credential Staking) (AccountState era)) (DState era))
 -> CertState era
 -> Const
      (Map (Credential Staking) (AccountState era)) (CertState era))
-> ((Map (Credential Staking) (AccountState era)
     -> Const
          (Map (Credential Staking) (AccountState era))
          (Map (Credential Staking) (AccountState era)))
    -> DState era
    -> Const
         (Map (Credential Staking) (AccountState era)) (DState era))
-> Getting
     (Map (Credential Staking) (AccountState era))
     (CertState era)
     (Map (Credential Staking) (AccountState era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Accounts era
 -> Const
      (Map (Credential Staking) (AccountState era)) (Accounts era))
-> DState era
-> Const (Map (Credential Staking) (AccountState era)) (DState era)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL ((Accounts era
  -> Const
       (Map (Credential Staking) (AccountState era)) (Accounts era))
 -> DState era
 -> Const
      (Map (Credential Staking) (AccountState era)) (DState era))
-> ((Map (Credential Staking) (AccountState era)
     -> Const
          (Map (Credential Staking) (AccountState era))
          (Map (Credential Staking) (AccountState era)))
    -> Accounts era
    -> Const
         (Map (Credential Staking) (AccountState era)) (Accounts era))
-> (Map (Credential Staking) (AccountState era)
    -> Const
         (Map (Credential Staking) (AccountState era))
         (Map (Credential Staking) (AccountState era)))
-> DState era
-> Const (Map (Credential Staking) (AccountState era)) (DState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (Credential Staking) (AccountState era)
 -> Const
      (Map (Credential Staking) (AccountState era))
      (Map (Credential Staking) (AccountState era)))
-> Accounts era
-> Const
     (Map (Credential Staking) (AccountState era)) (Accounts era)
forall era.
EraAccounts era =>
Lens' (Accounts era) (Map (Credential Staking) (AccountState era))
Lens' (Accounts era) (Map (Credential Staking) (AccountState era))
accountsMapL
      delegatorsPerStakePool :: Map (KeyHash StakePool) (Set (Credential Staking))
delegatorsPerStakePool =
        (Map (KeyHash StakePool) (Set (Credential Staking))
 -> Credential Staking
 -> AccountState era
 -> Map (KeyHash StakePool) (Set (Credential Staking)))
-> Map (KeyHash StakePool) (Set (Credential Staking))
-> Map (Credential Staking) (AccountState era)
-> Map (KeyHash StakePool) (Set (Credential Staking))
forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey'
          ( \Map (KeyHash StakePool) (Set (Credential Staking))
acc Credential Staking
cred AccountState era
accountState ->
              case AccountState era
accountState AccountState era
-> Getting
     (Maybe (KeyHash StakePool))
     (AccountState era)
     (Maybe (KeyHash StakePool))
-> Maybe (KeyHash StakePool)
forall s a. s -> Getting a s a -> a
^. Getting
  (Maybe (KeyHash StakePool))
  (AccountState era)
  (Maybe (KeyHash StakePool))
forall era.
EraAccounts era =>
Lens' (AccountState era) (Maybe (KeyHash StakePool))
Lens' (AccountState era) (Maybe (KeyHash StakePool))
stakePoolDelegationAccountStateL of
                Maybe (KeyHash StakePool)
Nothing -> Map (KeyHash StakePool) (Set (Credential Staking))
acc
                Just KeyHash StakePool
poolId -> (Set (Credential Staking)
 -> Set (Credential Staking) -> Set (Credential Staking))
-> KeyHash StakePool
-> Set (Credential Staking)
-> Map (KeyHash StakePool) (Set (Credential Staking))
-> Map (KeyHash StakePool) (Set (Credential Staking))
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Set (Credential Staking)
-> Set (Credential Staking) -> Set (Credential Staking)
forall a. Semigroup a => a -> a -> a
(<>) KeyHash StakePool
poolId (Credential Staking -> Set (Credential Staking)
forall a. a -> Set a
Set.singleton Credential Staking
cred) Map (KeyHash StakePool) (Set (Credential Staking))
acc
          )
          Map (KeyHash StakePool) (Set (Credential Staking))
forall a. Monoid a => a
mempty
          Map (Credential Staking) (AccountState era)
accountsMap
      reverseDelegatorsPerStakePool :: Map (KeyHash StakePool) (Set (Credential Staking))
reverseDelegatorsPerStakePool =
        (StakePoolState -> Maybe (Set (Credential Staking)))
-> Map (KeyHash StakePool) StakePoolState
-> Map (KeyHash StakePool) (Set (Credential Staking))
forall a b k. (a -> Maybe b) -> Map k a -> Map k b
Map.mapMaybe
          (\StakePoolState
sps -> StakePoolState -> Set (Credential Staking)
spsDelegators StakePoolState
sps Set (Credential Staking)
-> Maybe () -> Maybe (Set (Credential Staking))
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (Set (Credential Staking) -> Bool
forall a. Set a -> Bool
Set.null (StakePoolState -> Set (Credential Staking)
spsDelegators StakePoolState
sps))))
          (CertState era
certState CertState era
-> Getting
     (Map (KeyHash StakePool) StakePoolState)
     (CertState era)
     (Map (KeyHash StakePool) StakePoolState)
-> Map (KeyHash StakePool) StakePoolState
forall s a. s -> Getting a s a -> a
^. (PState era
 -> Const (Map (KeyHash StakePool) StakePoolState) (PState era))
-> CertState era
-> Const (Map (KeyHash StakePool) StakePoolState) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL ((PState era
  -> Const (Map (KeyHash StakePool) StakePoolState) (PState era))
 -> CertState era
 -> Const (Map (KeyHash StakePool) StakePoolState) (CertState era))
-> ((Map (KeyHash StakePool) StakePoolState
     -> Const
          (Map (KeyHash StakePool) StakePoolState)
          (Map (KeyHash StakePool) StakePoolState))
    -> PState era
    -> Const (Map (KeyHash StakePool) StakePoolState) (PState era))
-> Getting
     (Map (KeyHash StakePool) StakePoolState)
     (CertState era)
     (Map (KeyHash StakePool) StakePoolState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (KeyHash StakePool) StakePoolState
 -> Const
      (Map (KeyHash StakePool) StakePoolState)
      (Map (KeyHash StakePool) StakePoolState))
-> PState era
-> Const (Map (KeyHash StakePool) StakePoolState) (PState era)
forall era (f :: * -> *).
Functor f =>
(Map (KeyHash StakePool) StakePoolState
 -> f (Map (KeyHash StakePool) StakePoolState))
-> PState era -> f (PState era)
psStakePoolsL)
   in (Map (KeyHash StakePool) (Set (Credential Staking))
reverseDelegatorsPerStakePool, Map (KeyHash StakePool) (Set (Credential Staking))
delegatorsPerStakePool)