{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Cardano.Ledger.Alonzo.Rules.Bbody (
  AlonzoBBODY,
  AlonzoBbodyPredFailure (..),
  AlonzoBbodyEvent (..),
  alonzoBbodyTransition,
) where

import Cardano.Ledger.Allegra.Rules (AllegraUtxoPredFailure)
import Cardano.Ledger.Alonzo.Core
import Cardano.Ledger.Alonzo.Era (AlonzoBBODY, AlonzoEra)
import Cardano.Ledger.Alonzo.Rules.Ledgers ()
import Cardano.Ledger.Alonzo.Rules.Utxo (AlonzoUtxoPredFailure)
import Cardano.Ledger.Alonzo.Rules.Utxos (AlonzoUtxosPredFailure)
import Cardano.Ledger.Alonzo.Rules.Utxow (AlonzoUtxowPredFailure)
import Cardano.Ledger.Alonzo.Scripts (ExUnits (..), pointWiseExUnits)
import Cardano.Ledger.Alonzo.Tx (totExUnits)
import Cardano.Ledger.BHeaderView (BHeaderView (..), isOverlaySlot)
import Cardano.Ledger.BaseTypes (Mismatch (..), Relation (..), ShelleyBase, epochInfoPure)
import Cardano.Ledger.Binary (DecCBOR (..), EncCBOR (..))
import Cardano.Ledger.Binary.Coders
import Cardano.Ledger.Block (Block (..))
import Cardano.Ledger.Keys (coerceKeyRole)
import Cardano.Ledger.Shelley.BlockBody (incrBlocks)
import Cardano.Ledger.Shelley.LedgerState (LedgerState)
import Cardano.Ledger.Shelley.Rules (
  BbodyEnv (..),
  ShelleyBbodyEvent (..),
  ShelleyBbodyPredFailure (..),
  ShelleyBbodyState (..),
  ShelleyDelegPredFailure,
  ShelleyDelegsPredFailure,
  ShelleyDelplPredFailure,
  ShelleyLedgerPredFailure,
  ShelleyLedgersEnv (..),
  ShelleyLedgersPredFailure,
  ShelleyPoolPredFailure,
  ShelleyPpupPredFailure,
  ShelleyUtxoPredFailure,
  ShelleyUtxowPredFailure,
 )
import Cardano.Ledger.Slot (epochInfoEpoch, epochInfoFirst)
import Control.DeepSeq (NFData)
import Control.Monad.Trans.Reader (asks)
import Control.State.Transition (
  Embed (..),
  STS (..),
  TRC (..),
  TransitionRule,
  judgmentContext,
  liftSTS,
  trans,
  (?!),
 )
import Data.Sequence (Seq)
import qualified Data.Sequence.Strict as StrictSeq
import GHC.Generics (Generic)
import Lens.Micro ((^.))
import NoThunks.Class (NoThunks (..))

-- =======================================
-- A new PredicateFailure type

data AlonzoBbodyPredFailure era
  = ShelleyInAlonzoBbodyPredFailure (ShelleyBbodyPredFailure era)
  | TooManyExUnits (Mismatch RelLTEQ ExUnits)
  deriving ((forall x.
 AlonzoBbodyPredFailure era -> Rep (AlonzoBbodyPredFailure era) x)
-> (forall x.
    Rep (AlonzoBbodyPredFailure era) x -> AlonzoBbodyPredFailure era)
-> Generic (AlonzoBbodyPredFailure era)
forall x.
Rep (AlonzoBbodyPredFailure era) x -> AlonzoBbodyPredFailure era
forall x.
AlonzoBbodyPredFailure era -> Rep (AlonzoBbodyPredFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (AlonzoBbodyPredFailure era) x -> AlonzoBbodyPredFailure era
forall era x.
AlonzoBbodyPredFailure era -> Rep (AlonzoBbodyPredFailure era) x
$cfrom :: forall era x.
AlonzoBbodyPredFailure era -> Rep (AlonzoBbodyPredFailure era) x
from :: forall x.
AlonzoBbodyPredFailure era -> Rep (AlonzoBbodyPredFailure era) x
$cto :: forall era x.
Rep (AlonzoBbodyPredFailure era) x -> AlonzoBbodyPredFailure era
to :: forall x.
Rep (AlonzoBbodyPredFailure era) x -> AlonzoBbodyPredFailure era
Generic)

instance NFData (PredicateFailure (EraRule "LEDGERS" era)) => NFData (AlonzoBbodyPredFailure era)

newtype AlonzoBbodyEvent era
  = ShelleyInAlonzoEvent (ShelleyBbodyEvent era)
  deriving ((forall x. AlonzoBbodyEvent era -> Rep (AlonzoBbodyEvent era) x)
-> (forall x. Rep (AlonzoBbodyEvent era) x -> AlonzoBbodyEvent era)
-> Generic (AlonzoBbodyEvent era)
forall x. Rep (AlonzoBbodyEvent era) x -> AlonzoBbodyEvent era
forall x. AlonzoBbodyEvent era -> Rep (AlonzoBbodyEvent era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x. Rep (AlonzoBbodyEvent era) x -> AlonzoBbodyEvent era
forall era x. AlonzoBbodyEvent era -> Rep (AlonzoBbodyEvent era) x
$cfrom :: forall era x. AlonzoBbodyEvent era -> Rep (AlonzoBbodyEvent era) x
from :: forall x. AlonzoBbodyEvent era -> Rep (AlonzoBbodyEvent era) x
$cto :: forall era x. Rep (AlonzoBbodyEvent era) x -> AlonzoBbodyEvent era
to :: forall x. Rep (AlonzoBbodyEvent era) x -> AlonzoBbodyEvent era
Generic)

deriving instance
  Eq (Event (EraRule "LEDGERS" era)) =>
  Eq (AlonzoBbodyEvent era)

type instance EraRuleFailure "BBODY" AlonzoEra = AlonzoBbodyPredFailure AlonzoEra

instance InjectRuleFailure "BBODY" AlonzoBbodyPredFailure AlonzoEra

instance InjectRuleFailure "BBODY" ShelleyBbodyPredFailure AlonzoEra where
  injectFailure :: ShelleyBbodyPredFailure AlonzoEra
-> EraRuleFailure "BBODY" AlonzoEra
injectFailure = ShelleyBbodyPredFailure AlonzoEra
-> EraRuleFailure "BBODY" AlonzoEra
ShelleyBbodyPredFailure AlonzoEra
-> AlonzoBbodyPredFailure AlonzoEra
forall era.
ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
ShelleyInAlonzoBbodyPredFailure

instance InjectRuleFailure "BBODY" ShelleyLedgersPredFailure AlonzoEra where
  injectFailure :: ShelleyLedgersPredFailure AlonzoEra
-> EraRuleFailure "BBODY" AlonzoEra
injectFailure = ShelleyBbodyPredFailure AlonzoEra
-> AlonzoBbodyPredFailure AlonzoEra
forall era.
ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
ShelleyInAlonzoBbodyPredFailure (ShelleyBbodyPredFailure AlonzoEra
 -> AlonzoBbodyPredFailure AlonzoEra)
-> (ShelleyLedgersPredFailure AlonzoEra
    -> ShelleyBbodyPredFailure AlonzoEra)
-> ShelleyLedgersPredFailure AlonzoEra
-> AlonzoBbodyPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure (EraRule "LEDGERS" AlonzoEra)
-> ShelleyBbodyPredFailure AlonzoEra
ShelleyLedgersPredFailure AlonzoEra
-> ShelleyBbodyPredFailure AlonzoEra
forall era.
PredicateFailure (EraRule "LEDGERS" era)
-> ShelleyBbodyPredFailure era
LedgersFailure

instance InjectRuleFailure "BBODY" ShelleyLedgerPredFailure AlonzoEra where
  injectFailure :: ShelleyLedgerPredFailure AlonzoEra
-> EraRuleFailure "BBODY" AlonzoEra
injectFailure = ShelleyBbodyPredFailure AlonzoEra
-> AlonzoBbodyPredFailure AlonzoEra
forall era.
ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
ShelleyInAlonzoBbodyPredFailure (ShelleyBbodyPredFailure AlonzoEra
 -> AlonzoBbodyPredFailure AlonzoEra)
-> (ShelleyLedgerPredFailure AlonzoEra
    -> ShelleyBbodyPredFailure AlonzoEra)
-> ShelleyLedgerPredFailure AlonzoEra
-> AlonzoBbodyPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure (EraRule "LEDGERS" AlonzoEra)
-> ShelleyBbodyPredFailure AlonzoEra
ShelleyLedgersPredFailure AlonzoEra
-> ShelleyBbodyPredFailure AlonzoEra
forall era.
PredicateFailure (EraRule "LEDGERS" era)
-> ShelleyBbodyPredFailure era
LedgersFailure (ShelleyLedgersPredFailure AlonzoEra
 -> ShelleyBbodyPredFailure AlonzoEra)
-> (ShelleyLedgerPredFailure AlonzoEra
    -> ShelleyLedgersPredFailure AlonzoEra)
-> ShelleyLedgerPredFailure AlonzoEra
-> ShelleyBbodyPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShelleyLedgerPredFailure AlonzoEra
-> EraRuleFailure "LEDGERS" AlonzoEra
ShelleyLedgerPredFailure AlonzoEra
-> ShelleyLedgersPredFailure AlonzoEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "BBODY" AlonzoUtxowPredFailure AlonzoEra where
  injectFailure :: AlonzoUtxowPredFailure AlonzoEra
-> EraRuleFailure "BBODY" AlonzoEra
injectFailure = ShelleyBbodyPredFailure AlonzoEra
-> AlonzoBbodyPredFailure AlonzoEra
forall era.
ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
ShelleyInAlonzoBbodyPredFailure (ShelleyBbodyPredFailure AlonzoEra
 -> AlonzoBbodyPredFailure AlonzoEra)
-> (AlonzoUtxowPredFailure AlonzoEra
    -> ShelleyBbodyPredFailure AlonzoEra)
-> AlonzoUtxowPredFailure AlonzoEra
-> AlonzoBbodyPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure (EraRule "LEDGERS" AlonzoEra)
-> ShelleyBbodyPredFailure AlonzoEra
ShelleyLedgersPredFailure AlonzoEra
-> ShelleyBbodyPredFailure AlonzoEra
forall era.
PredicateFailure (EraRule "LEDGERS" era)
-> ShelleyBbodyPredFailure era
LedgersFailure (ShelleyLedgersPredFailure AlonzoEra
 -> ShelleyBbodyPredFailure AlonzoEra)
-> (AlonzoUtxowPredFailure AlonzoEra
    -> ShelleyLedgersPredFailure AlonzoEra)
-> AlonzoUtxowPredFailure AlonzoEra
-> ShelleyBbodyPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlonzoUtxowPredFailure AlonzoEra
-> EraRuleFailure "LEDGERS" AlonzoEra
AlonzoUtxowPredFailure AlonzoEra
-> ShelleyLedgersPredFailure AlonzoEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "BBODY" ShelleyUtxowPredFailure AlonzoEra where
  injectFailure :: ShelleyUtxowPredFailure AlonzoEra
-> EraRuleFailure "BBODY" AlonzoEra
injectFailure = ShelleyBbodyPredFailure AlonzoEra
-> AlonzoBbodyPredFailure AlonzoEra
forall era.
ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
ShelleyInAlonzoBbodyPredFailure (ShelleyBbodyPredFailure AlonzoEra
 -> AlonzoBbodyPredFailure AlonzoEra)
-> (ShelleyUtxowPredFailure AlonzoEra
    -> ShelleyBbodyPredFailure AlonzoEra)
-> ShelleyUtxowPredFailure AlonzoEra
-> AlonzoBbodyPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure (EraRule "LEDGERS" AlonzoEra)
-> ShelleyBbodyPredFailure AlonzoEra
ShelleyLedgersPredFailure AlonzoEra
-> ShelleyBbodyPredFailure AlonzoEra
forall era.
PredicateFailure (EraRule "LEDGERS" era)
-> ShelleyBbodyPredFailure era
LedgersFailure (ShelleyLedgersPredFailure AlonzoEra
 -> ShelleyBbodyPredFailure AlonzoEra)
-> (ShelleyUtxowPredFailure AlonzoEra
    -> ShelleyLedgersPredFailure AlonzoEra)
-> ShelleyUtxowPredFailure AlonzoEra
-> ShelleyBbodyPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShelleyUtxowPredFailure AlonzoEra
-> EraRuleFailure "LEDGERS" AlonzoEra
ShelleyUtxowPredFailure AlonzoEra
-> ShelleyLedgersPredFailure AlonzoEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "BBODY" AlonzoUtxoPredFailure AlonzoEra where
  injectFailure :: AlonzoUtxoPredFailure AlonzoEra -> EraRuleFailure "BBODY" AlonzoEra
injectFailure = ShelleyBbodyPredFailure AlonzoEra
-> AlonzoBbodyPredFailure AlonzoEra
forall era.
ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
ShelleyInAlonzoBbodyPredFailure (ShelleyBbodyPredFailure AlonzoEra
 -> AlonzoBbodyPredFailure AlonzoEra)
-> (AlonzoUtxoPredFailure AlonzoEra
    -> ShelleyBbodyPredFailure AlonzoEra)
-> AlonzoUtxoPredFailure AlonzoEra
-> AlonzoBbodyPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure (EraRule "LEDGERS" AlonzoEra)
-> ShelleyBbodyPredFailure AlonzoEra
ShelleyLedgersPredFailure AlonzoEra
-> ShelleyBbodyPredFailure AlonzoEra
forall era.
PredicateFailure (EraRule "LEDGERS" era)
-> ShelleyBbodyPredFailure era
LedgersFailure (ShelleyLedgersPredFailure AlonzoEra
 -> ShelleyBbodyPredFailure AlonzoEra)
-> (AlonzoUtxoPredFailure AlonzoEra
    -> ShelleyLedgersPredFailure AlonzoEra)
-> AlonzoUtxoPredFailure AlonzoEra
-> ShelleyBbodyPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlonzoUtxoPredFailure AlonzoEra
-> EraRuleFailure "LEDGERS" AlonzoEra
AlonzoUtxoPredFailure AlonzoEra
-> ShelleyLedgersPredFailure AlonzoEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "BBODY" AlonzoUtxosPredFailure AlonzoEra where
  injectFailure :: AlonzoUtxosPredFailure AlonzoEra
-> EraRuleFailure "BBODY" AlonzoEra
injectFailure = ShelleyBbodyPredFailure AlonzoEra
-> AlonzoBbodyPredFailure AlonzoEra
forall era.
ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
ShelleyInAlonzoBbodyPredFailure (ShelleyBbodyPredFailure AlonzoEra
 -> AlonzoBbodyPredFailure AlonzoEra)
-> (AlonzoUtxosPredFailure AlonzoEra
    -> ShelleyBbodyPredFailure AlonzoEra)
-> AlonzoUtxosPredFailure AlonzoEra
-> AlonzoBbodyPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure (EraRule "LEDGERS" AlonzoEra)
-> ShelleyBbodyPredFailure AlonzoEra
ShelleyLedgersPredFailure AlonzoEra
-> ShelleyBbodyPredFailure AlonzoEra
forall era.
PredicateFailure (EraRule "LEDGERS" era)
-> ShelleyBbodyPredFailure era
LedgersFailure (ShelleyLedgersPredFailure AlonzoEra
 -> ShelleyBbodyPredFailure AlonzoEra)
-> (AlonzoUtxosPredFailure AlonzoEra
    -> ShelleyLedgersPredFailure AlonzoEra)
-> AlonzoUtxosPredFailure AlonzoEra
-> ShelleyBbodyPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlonzoUtxosPredFailure AlonzoEra
-> EraRuleFailure "LEDGERS" AlonzoEra
AlonzoUtxosPredFailure AlonzoEra
-> ShelleyLedgersPredFailure AlonzoEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "BBODY" ShelleyPpupPredFailure AlonzoEra where
  injectFailure :: ShelleyPpupPredFailure AlonzoEra
-> EraRuleFailure "BBODY" AlonzoEra
injectFailure = ShelleyBbodyPredFailure AlonzoEra
-> AlonzoBbodyPredFailure AlonzoEra
forall era.
ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
ShelleyInAlonzoBbodyPredFailure (ShelleyBbodyPredFailure AlonzoEra
 -> AlonzoBbodyPredFailure AlonzoEra)
-> (ShelleyPpupPredFailure AlonzoEra
    -> ShelleyBbodyPredFailure AlonzoEra)
-> ShelleyPpupPredFailure AlonzoEra
-> AlonzoBbodyPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure (EraRule "LEDGERS" AlonzoEra)
-> ShelleyBbodyPredFailure AlonzoEra
ShelleyLedgersPredFailure AlonzoEra
-> ShelleyBbodyPredFailure AlonzoEra
forall era.
PredicateFailure (EraRule "LEDGERS" era)
-> ShelleyBbodyPredFailure era
LedgersFailure (ShelleyLedgersPredFailure AlonzoEra
 -> ShelleyBbodyPredFailure AlonzoEra)
-> (ShelleyPpupPredFailure AlonzoEra
    -> ShelleyLedgersPredFailure AlonzoEra)
-> ShelleyPpupPredFailure AlonzoEra
-> ShelleyBbodyPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShelleyPpupPredFailure AlonzoEra
-> EraRuleFailure "LEDGERS" AlonzoEra
ShelleyPpupPredFailure AlonzoEra
-> ShelleyLedgersPredFailure AlonzoEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "BBODY" ShelleyUtxoPredFailure AlonzoEra where
  injectFailure :: ShelleyUtxoPredFailure AlonzoEra
-> EraRuleFailure "BBODY" AlonzoEra
injectFailure = ShelleyBbodyPredFailure AlonzoEra
-> AlonzoBbodyPredFailure AlonzoEra
forall era.
ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
ShelleyInAlonzoBbodyPredFailure (ShelleyBbodyPredFailure AlonzoEra
 -> AlonzoBbodyPredFailure AlonzoEra)
-> (ShelleyUtxoPredFailure AlonzoEra
    -> ShelleyBbodyPredFailure AlonzoEra)
-> ShelleyUtxoPredFailure AlonzoEra
-> AlonzoBbodyPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure (EraRule "LEDGERS" AlonzoEra)
-> ShelleyBbodyPredFailure AlonzoEra
ShelleyLedgersPredFailure AlonzoEra
-> ShelleyBbodyPredFailure AlonzoEra
forall era.
PredicateFailure (EraRule "LEDGERS" era)
-> ShelleyBbodyPredFailure era
LedgersFailure (ShelleyLedgersPredFailure AlonzoEra
 -> ShelleyBbodyPredFailure AlonzoEra)
-> (ShelleyUtxoPredFailure AlonzoEra
    -> ShelleyLedgersPredFailure AlonzoEra)
-> ShelleyUtxoPredFailure AlonzoEra
-> ShelleyBbodyPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShelleyUtxoPredFailure AlonzoEra
-> EraRuleFailure "LEDGERS" AlonzoEra
ShelleyUtxoPredFailure AlonzoEra
-> ShelleyLedgersPredFailure AlonzoEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "BBODY" AllegraUtxoPredFailure AlonzoEra where
  injectFailure :: AllegraUtxoPredFailure AlonzoEra
-> EraRuleFailure "BBODY" AlonzoEra
injectFailure = ShelleyBbodyPredFailure AlonzoEra
-> AlonzoBbodyPredFailure AlonzoEra
forall era.
ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
ShelleyInAlonzoBbodyPredFailure (ShelleyBbodyPredFailure AlonzoEra
 -> AlonzoBbodyPredFailure AlonzoEra)
-> (AllegraUtxoPredFailure AlonzoEra
    -> ShelleyBbodyPredFailure AlonzoEra)
-> AllegraUtxoPredFailure AlonzoEra
-> AlonzoBbodyPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure (EraRule "LEDGERS" AlonzoEra)
-> ShelleyBbodyPredFailure AlonzoEra
ShelleyLedgersPredFailure AlonzoEra
-> ShelleyBbodyPredFailure AlonzoEra
forall era.
PredicateFailure (EraRule "LEDGERS" era)
-> ShelleyBbodyPredFailure era
LedgersFailure (ShelleyLedgersPredFailure AlonzoEra
 -> ShelleyBbodyPredFailure AlonzoEra)
-> (AllegraUtxoPredFailure AlonzoEra
    -> ShelleyLedgersPredFailure AlonzoEra)
-> AllegraUtxoPredFailure AlonzoEra
-> ShelleyBbodyPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AllegraUtxoPredFailure AlonzoEra
-> EraRuleFailure "LEDGERS" AlonzoEra
AllegraUtxoPredFailure AlonzoEra
-> ShelleyLedgersPredFailure AlonzoEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "BBODY" ShelleyDelegsPredFailure AlonzoEra where
  injectFailure :: ShelleyDelegsPredFailure AlonzoEra
-> EraRuleFailure "BBODY" AlonzoEra
injectFailure = ShelleyBbodyPredFailure AlonzoEra
-> AlonzoBbodyPredFailure AlonzoEra
forall era.
ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
ShelleyInAlonzoBbodyPredFailure (ShelleyBbodyPredFailure AlonzoEra
 -> AlonzoBbodyPredFailure AlonzoEra)
-> (ShelleyDelegsPredFailure AlonzoEra
    -> ShelleyBbodyPredFailure AlonzoEra)
-> ShelleyDelegsPredFailure AlonzoEra
-> AlonzoBbodyPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure (EraRule "LEDGERS" AlonzoEra)
-> ShelleyBbodyPredFailure AlonzoEra
ShelleyLedgersPredFailure AlonzoEra
-> ShelleyBbodyPredFailure AlonzoEra
forall era.
PredicateFailure (EraRule "LEDGERS" era)
-> ShelleyBbodyPredFailure era
LedgersFailure (ShelleyLedgersPredFailure AlonzoEra
 -> ShelleyBbodyPredFailure AlonzoEra)
-> (ShelleyDelegsPredFailure AlonzoEra
    -> ShelleyLedgersPredFailure AlonzoEra)
-> ShelleyDelegsPredFailure AlonzoEra
-> ShelleyBbodyPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShelleyDelegsPredFailure AlonzoEra
-> EraRuleFailure "LEDGERS" AlonzoEra
ShelleyDelegsPredFailure AlonzoEra
-> ShelleyLedgersPredFailure AlonzoEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "BBODY" ShelleyDelplPredFailure AlonzoEra where
  injectFailure :: ShelleyDelplPredFailure AlonzoEra
-> EraRuleFailure "BBODY" AlonzoEra
injectFailure = ShelleyBbodyPredFailure AlonzoEra
-> AlonzoBbodyPredFailure AlonzoEra
forall era.
ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
ShelleyInAlonzoBbodyPredFailure (ShelleyBbodyPredFailure AlonzoEra
 -> AlonzoBbodyPredFailure AlonzoEra)
-> (ShelleyDelplPredFailure AlonzoEra
    -> ShelleyBbodyPredFailure AlonzoEra)
-> ShelleyDelplPredFailure AlonzoEra
-> AlonzoBbodyPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure (EraRule "LEDGERS" AlonzoEra)
-> ShelleyBbodyPredFailure AlonzoEra
ShelleyLedgersPredFailure AlonzoEra
-> ShelleyBbodyPredFailure AlonzoEra
forall era.
PredicateFailure (EraRule "LEDGERS" era)
-> ShelleyBbodyPredFailure era
LedgersFailure (ShelleyLedgersPredFailure AlonzoEra
 -> ShelleyBbodyPredFailure AlonzoEra)
-> (ShelleyDelplPredFailure AlonzoEra
    -> ShelleyLedgersPredFailure AlonzoEra)
-> ShelleyDelplPredFailure AlonzoEra
-> ShelleyBbodyPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShelleyDelplPredFailure AlonzoEra
-> EraRuleFailure "LEDGERS" AlonzoEra
ShelleyDelplPredFailure AlonzoEra
-> ShelleyLedgersPredFailure AlonzoEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "BBODY" ShelleyPoolPredFailure AlonzoEra where
  injectFailure :: ShelleyPoolPredFailure AlonzoEra
-> EraRuleFailure "BBODY" AlonzoEra
injectFailure = ShelleyBbodyPredFailure AlonzoEra
-> AlonzoBbodyPredFailure AlonzoEra
forall era.
ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
ShelleyInAlonzoBbodyPredFailure (ShelleyBbodyPredFailure AlonzoEra
 -> AlonzoBbodyPredFailure AlonzoEra)
-> (ShelleyPoolPredFailure AlonzoEra
    -> ShelleyBbodyPredFailure AlonzoEra)
-> ShelleyPoolPredFailure AlonzoEra
-> AlonzoBbodyPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure (EraRule "LEDGERS" AlonzoEra)
-> ShelleyBbodyPredFailure AlonzoEra
ShelleyLedgersPredFailure AlonzoEra
-> ShelleyBbodyPredFailure AlonzoEra
forall era.
PredicateFailure (EraRule "LEDGERS" era)
-> ShelleyBbodyPredFailure era
LedgersFailure (ShelleyLedgersPredFailure AlonzoEra
 -> ShelleyBbodyPredFailure AlonzoEra)
-> (ShelleyPoolPredFailure AlonzoEra
    -> ShelleyLedgersPredFailure AlonzoEra)
-> ShelleyPoolPredFailure AlonzoEra
-> ShelleyBbodyPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShelleyPoolPredFailure AlonzoEra
-> EraRuleFailure "LEDGERS" AlonzoEra
ShelleyPoolPredFailure AlonzoEra
-> ShelleyLedgersPredFailure AlonzoEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

instance InjectRuleFailure "BBODY" ShelleyDelegPredFailure AlonzoEra where
  injectFailure :: ShelleyDelegPredFailure AlonzoEra
-> EraRuleFailure "BBODY" AlonzoEra
injectFailure = ShelleyBbodyPredFailure AlonzoEra
-> AlonzoBbodyPredFailure AlonzoEra
forall era.
ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
ShelleyInAlonzoBbodyPredFailure (ShelleyBbodyPredFailure AlonzoEra
 -> AlonzoBbodyPredFailure AlonzoEra)
-> (ShelleyDelegPredFailure AlonzoEra
    -> ShelleyBbodyPredFailure AlonzoEra)
-> ShelleyDelegPredFailure AlonzoEra
-> AlonzoBbodyPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure (EraRule "LEDGERS" AlonzoEra)
-> ShelleyBbodyPredFailure AlonzoEra
ShelleyLedgersPredFailure AlonzoEra
-> ShelleyBbodyPredFailure AlonzoEra
forall era.
PredicateFailure (EraRule "LEDGERS" era)
-> ShelleyBbodyPredFailure era
LedgersFailure (ShelleyLedgersPredFailure AlonzoEra
 -> ShelleyBbodyPredFailure AlonzoEra)
-> (ShelleyDelegPredFailure AlonzoEra
    -> ShelleyLedgersPredFailure AlonzoEra)
-> ShelleyDelegPredFailure AlonzoEra
-> ShelleyBbodyPredFailure AlonzoEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShelleyDelegPredFailure AlonzoEra
-> EraRuleFailure "LEDGERS" AlonzoEra
ShelleyDelegPredFailure AlonzoEra
-> ShelleyLedgersPredFailure AlonzoEra
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

deriving instance
  (Era era, Show (PredicateFailure (EraRule "LEDGERS" era))) =>
  Show (AlonzoBbodyPredFailure era)

deriving instance
  (Era era, Eq (PredicateFailure (EraRule "LEDGERS" era))) =>
  Eq (AlonzoBbodyPredFailure era)

deriving anyclass instance
  (Era era, NoThunks (PredicateFailure (EraRule "LEDGERS" era))) =>
  NoThunks (AlonzoBbodyPredFailure era)

instance
  (Era era, EncCBOR (PredicateFailure (EraRule "LEDGERS" era))) =>
  EncCBOR (AlonzoBbodyPredFailure era)
  where
  encCBOR :: AlonzoBbodyPredFailure era -> Encoding
encCBOR (ShelleyInAlonzoBbodyPredFailure ShelleyBbodyPredFailure era
x) = Encode Open (AlonzoBbodyPredFailure era) -> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode ((ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era)
-> Word
-> Encode
     Open (ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era)
forall t. t -> Word -> Encode Open t
Sum ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
forall era.
ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
ShelleyInAlonzoBbodyPredFailure Word
0 Encode
  Open (ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era)
-> Encode (Closed Dense) (ShelleyBbodyPredFailure era)
-> Encode Open (AlonzoBbodyPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> ShelleyBbodyPredFailure era
-> Encode (Closed Dense) (ShelleyBbodyPredFailure era)
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To ShelleyBbodyPredFailure era
x)
  encCBOR (TooManyExUnits Mismatch RelLTEQ ExUnits
m) = Encode Open (AlonzoBbodyPredFailure (ZonkAny 2)) -> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode ((Mismatch RelLTEQ ExUnits -> AlonzoBbodyPredFailure (ZonkAny 2))
-> Word
-> Encode
     Open
     (Mismatch RelLTEQ ExUnits -> AlonzoBbodyPredFailure (ZonkAny 2))
forall t. t -> Word -> Encode Open t
Sum Mismatch RelLTEQ ExUnits -> AlonzoBbodyPredFailure (ZonkAny 2)
forall era. Mismatch RelLTEQ ExUnits -> AlonzoBbodyPredFailure era
TooManyExUnits Word
1 Encode
  Open
  (Mismatch RelLTEQ ExUnits -> AlonzoBbodyPredFailure (ZonkAny 2))
-> Encode (Closed Dense) (Mismatch RelLTEQ ExUnits)
-> Encode Open (AlonzoBbodyPredFailure (ZonkAny 2))
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> Mismatch RelLTEQ ExUnits
-> Encode (Closed Dense) (Mismatch RelLTEQ ExUnits)
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To Mismatch RelLTEQ ExUnits
m)

instance
  (Era era, DecCBOR (PredicateFailure (EraRule "LEDGERS" era))) =>
  DecCBOR (AlonzoBbodyPredFailure era)
  where
  decCBOR :: forall s. Decoder s (AlonzoBbodyPredFailure era)
decCBOR = Decode (Closed Dense) (AlonzoBbodyPredFailure era)
-> Decoder s (AlonzoBbodyPredFailure era)
forall t (w :: Wrapped) s. Typeable t => Decode w t -> Decoder s t
decode (Text
-> (Word -> Decode Open (AlonzoBbodyPredFailure era))
-> Decode (Closed Dense) (AlonzoBbodyPredFailure era)
forall t.
Text -> (Word -> Decode Open t) -> Decode (Closed Dense) t
Summands Text
"AlonzoBbodyPredFail" Word -> Decode Open (AlonzoBbodyPredFailure era)
forall {era}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat MinVersion (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat MinVersion (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Era era, DecCBOR (PredicateFailure (EraRule "LEDGERS" era))) =>
Word -> Decode Open (AlonzoBbodyPredFailure era)
dec)
    where
      dec :: Word -> Decode Open (AlonzoBbodyPredFailure era)
dec Word
0 = (ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era)
-> Decode
     Open (ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era)
forall t. t -> Decode Open t
SumD ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
forall era.
ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
ShelleyInAlonzoBbodyPredFailure Decode
  Open (ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era)
-> Decode
     (Closed (ZonkAny MinVersion)) (ShelleyBbodyPredFailure era)
-> Decode Open (AlonzoBbodyPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode (Closed (ZonkAny MinVersion)) (ShelleyBbodyPredFailure era)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
      dec Word
1 = (Mismatch RelLTEQ ExUnits -> AlonzoBbodyPredFailure era)
-> Decode
     Open (Mismatch RelLTEQ ExUnits -> AlonzoBbodyPredFailure era)
forall t. t -> Decode Open t
SumD Mismatch RelLTEQ ExUnits -> AlonzoBbodyPredFailure era
forall era. Mismatch RelLTEQ ExUnits -> AlonzoBbodyPredFailure era
TooManyExUnits Decode
  Open (Mismatch RelLTEQ ExUnits -> AlonzoBbodyPredFailure era)
-> Decode (Closed (ZonkAny 1)) (Mismatch RelLTEQ ExUnits)
-> Decode Open (AlonzoBbodyPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode (Closed (ZonkAny 1)) (Mismatch RelLTEQ ExUnits)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
      dec Word
n = Word -> Decode Open (AlonzoBbodyPredFailure era)
forall (w :: Wrapped) t. Word -> Decode w t
Invalid Word
n

-- ========================================
-- The STS instance

alonzoBbodyTransition ::
  forall era.
  ( STS (EraRule "BBODY" era)
  , Signal (EraRule "BBODY" era) ~ Block BHeaderView era
  , InjectRuleFailure "BBODY" AlonzoBbodyPredFailure era
  , BaseM (EraRule "BBODY" era) ~ ShelleyBase
  , State (EraRule "BBODY" era) ~ ShelleyBbodyState era
  , Environment (EraRule "BBODY" era) ~ BbodyEnv era
  , Embed (EraRule "LEDGERS" era) (EraRule "BBODY" era)
  , Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era
  , State (EraRule "LEDGERS" era) ~ LedgerState era
  , Signal (EraRule "LEDGERS" era) ~ Seq (Tx TopTx era)
  , EraBlockBody era
  , AlonzoEraTxWits era
  , AlonzoEraPParams era
  ) =>
  TransitionRule (EraRule "BBODY" era)
alonzoBbodyTransition :: forall era.
(STS (EraRule "BBODY" era),
 Signal (EraRule "BBODY" era) ~ Block BHeaderView era,
 InjectRuleFailure "BBODY" AlonzoBbodyPredFailure era,
 BaseM (EraRule "BBODY" era) ~ ShelleyBase,
 State (EraRule "BBODY" era) ~ ShelleyBbodyState era,
 Environment (EraRule "BBODY" era) ~ BbodyEnv era,
 Embed (EraRule "LEDGERS" era) (EraRule "BBODY" era),
 Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era,
 State (EraRule "LEDGERS" era) ~ LedgerState era,
 Signal (EraRule "LEDGERS" era) ~ Seq (Tx TopTx era),
 EraBlockBody era, AlonzoEraTxWits era, AlonzoEraPParams era) =>
TransitionRule (EraRule "BBODY" era)
alonzoBbodyTransition =
  Rule
  (EraRule "BBODY" era)
  'Transition
  (RuleContext 'Transition (EraRule "BBODY" era))
F (Clause (EraRule "BBODY" era) 'Transition)
  (TRC (EraRule "BBODY" era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
    F (Clause (EraRule "BBODY" era) 'Transition)
  (TRC (EraRule "BBODY" era))
-> (TRC (EraRule "BBODY" era)
    -> F (Clause (EraRule "BBODY" era) 'Transition)
         (ShelleyBbodyState era))
-> F (Clause (EraRule "BBODY" era) 'Transition)
     (ShelleyBbodyState era)
forall a b.
F (Clause (EraRule "BBODY" era) 'Transition) a
-> (a -> F (Clause (EraRule "BBODY" era) 'Transition) b)
-> F (Clause (EraRule "BBODY" era) 'Transition) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \( TRC
             ( BbodyEnv PParams era
pp ChainAccountState
account
               , BbodyState State (EraRule "LEDGERS" era)
ls BlocksMade
b
               , Block BHeaderView
bh BlockBody era
txsSeq
               )
           ) -> do
        let txs :: StrictSeq (Tx TopTx era)
txs = BlockBody era
txsSeq BlockBody era
-> Getting
     (StrictSeq (Tx TopTx era))
     (BlockBody era)
     (StrictSeq (Tx TopTx era))
-> StrictSeq (Tx TopTx era)
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictSeq (Tx TopTx era))
  (BlockBody era)
  (StrictSeq (Tx TopTx era))
forall era.
EraBlockBody era =>
Lens' (BlockBody era) (StrictSeq (Tx TopTx era))
Lens' (BlockBody era) (StrictSeq (Tx TopTx era))
txSeqBlockBodyL
            actualBodySize :: Int
actualBodySize = ProtVer -> BlockBody era -> Int
forall era. EraBlockBody era => ProtVer -> BlockBody era -> Int
bBodySize (PParams era
pp PParams era -> Getting ProtVer (PParams era) ProtVer -> ProtVer
forall s a. s -> Getting a s a -> a
^. Getting ProtVer (PParams era) ProtVer
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams era) ProtVer
ppProtocolVersionL) BlockBody era
txsSeq
            actualBodyHash :: Hash HASH EraIndependentBlockBody
actualBodyHash = forall era.
EraBlockBody era =>
BlockBody era -> Hash HASH EraIndependentBlockBody
hashBlockBody @era BlockBody era
txsSeq

        Int
actualBodySize
          Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Word32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (BHeaderView -> Word32
bhviewBSize BHeaderView
bh)
            Bool
-> PredicateFailure (EraRule "BBODY" era)
-> Rule (EraRule "BBODY" era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! AlonzoBbodyPredFailure era -> EraRuleFailure "BBODY" era
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure
              ( ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
forall era.
ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
ShelleyInAlonzoBbodyPredFailure
                  ( Mismatch RelEQ Int -> ShelleyBbodyPredFailure era
forall era. Mismatch RelEQ Int -> ShelleyBbodyPredFailure era
WrongBlockBodySizeBBODY (Mismatch RelEQ Int -> ShelleyBbodyPredFailure era)
-> Mismatch RelEQ Int -> ShelleyBbodyPredFailure era
forall a b. (a -> b) -> a -> b
$
                      Mismatch
                        { mismatchSupplied :: Int
mismatchSupplied = Int
actualBodySize
                        , mismatchExpected :: Int
mismatchExpected = Word32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word32 -> Int) -> Word32 -> Int
forall a b. (a -> b) -> a -> b
$ BHeaderView -> Word32
bhviewBSize BHeaderView
bh
                        }
                  )
              )

        Hash HASH EraIndependentBlockBody
actualBodyHash
          Hash HASH EraIndependentBlockBody
-> Hash HASH EraIndependentBlockBody -> Bool
forall a. Eq a => a -> a -> Bool
== BHeaderView -> Hash HASH EraIndependentBlockBody
bhviewBHash BHeaderView
bh
            Bool
-> PredicateFailure (EraRule "BBODY" era)
-> Rule (EraRule "BBODY" era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! AlonzoBbodyPredFailure era -> EraRuleFailure "BBODY" era
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure
              ( ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
forall era.
ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
ShelleyInAlonzoBbodyPredFailure
                  ( forall era.
Mismatch RelEQ (Hash HASH EraIndependentBlockBody)
-> ShelleyBbodyPredFailure era
InvalidBodyHashBBODY @era (Mismatch RelEQ (Hash HASH EraIndependentBlockBody)
 -> ShelleyBbodyPredFailure era)
-> Mismatch RelEQ (Hash HASH EraIndependentBlockBody)
-> ShelleyBbodyPredFailure era
forall a b. (a -> b) -> a -> b
$
                      Mismatch
                        { mismatchSupplied :: Hash HASH EraIndependentBlockBody
mismatchSupplied = Hash HASH EraIndependentBlockBody
actualBodyHash
                        , mismatchExpected :: Hash HASH EraIndependentBlockBody
mismatchExpected = BHeaderView -> Hash HASH EraIndependentBlockBody
bhviewBHash BHeaderView
bh
                        }
                  )
              )

        -- Note that this may not actually be a stake pool - it could be a
        -- genesis key delegate. However, this would only entail an overhead of
        -- 7 counts, and it's easier than differentiating here.
        --
        -- TODO move this computation inside 'incrBlocks' where it belongs. Here
        -- we make an assumption that 'incrBlocks' must enforce, better for it
        -- to be done in 'incrBlocks' where we can see that the assumption is
        -- enforced.
        let hkAsStakePool :: KeyHash StakePool
hkAsStakePool = KeyHash BlockIssuer -> KeyHash StakePool
forall (r :: KeyRole) (r' :: KeyRole). KeyHash r -> KeyHash r'
forall (a :: KeyRole -> *) (r :: KeyRole) (r' :: KeyRole).
HasKeyRole a =>
a r -> a r'
coerceKeyRole (KeyHash BlockIssuer -> KeyHash StakePool)
-> KeyHash BlockIssuer -> KeyHash StakePool
forall a b. (a -> b) -> a -> b
$ BHeaderView -> KeyHash BlockIssuer
bhviewID BHeaderView
bh
            slot :: SlotNo
slot = BHeaderView -> SlotNo
bhviewSlot BHeaderView
bh
        (firstSlotNo, curEpochNo) <- BaseM (EraRule "BBODY" era) (SlotNo, EpochNo)
-> Rule (EraRule "BBODY" era) 'Transition (SlotNo, EpochNo)
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (EraRule "BBODY" era) (SlotNo, EpochNo)
 -> Rule (EraRule "BBODY" era) 'Transition (SlotNo, EpochNo))
-> BaseM (EraRule "BBODY" era) (SlotNo, EpochNo)
-> Rule (EraRule "BBODY" era) 'Transition (SlotNo, EpochNo)
forall a b. (a -> b) -> a -> b
$ do
          ei <- (Globals -> EpochInfo Identity)
-> ReaderT Globals Identity (EpochInfo Identity)
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> EpochInfo Identity
epochInfoPure
          let curEpochNo = HasCallStack => EpochInfo Identity -> SlotNo -> EpochNo
EpochInfo Identity -> SlotNo -> EpochNo
epochInfoEpoch EpochInfo Identity
ei SlotNo
slot
          pure (epochInfoFirst ei curEpochNo, curEpochNo)

        ls' <-
          trans @(EraRule "LEDGERS" era) $
            TRC (LedgersEnv (bhviewSlot bh) curEpochNo pp account, ls, StrictSeq.fromStrict txs)

        {- ∑(tx ∈ txs)(totExunits tx) ≤ maxBlockExUnits pp  -}
        let txTotal, ppMax :: ExUnits
            txTotal = (Tx TopTx era -> ExUnits) -> StrictSeq (Tx TopTx era) -> ExUnits
forall m a. Monoid m => (a -> m) -> StrictSeq a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Tx TopTx era -> ExUnits
forall era (l :: TxLevel).
(EraTx era, AlonzoEraTxWits era) =>
Tx l era -> ExUnits
totExUnits StrictSeq (Tx TopTx era)
txs
            ppMax = PParams era
pp PParams era -> Getting ExUnits (PParams era) ExUnits -> ExUnits
forall s a. s -> Getting a s a -> a
^. Getting ExUnits (PParams era) ExUnits
forall era. AlonzoEraPParams era => Lens' (PParams era) ExUnits
Lens' (PParams era) ExUnits
ppMaxBlockExUnitsL
        pointWiseExUnits (<=) txTotal ppMax
          ?! injectFailure (TooManyExUnits Mismatch {mismatchSupplied = txTotal, mismatchExpected = ppMax})

        pure $
          BbodyState @era
            ls'
            ( incrBlocks
                (isOverlaySlot firstSlotNo (pp ^. ppDG) slot)
                hkAsStakePool
                b
            )

instance
  ( EraRule "BBODY" era ~ AlonzoBBODY era
  , InjectRuleFailure "BBODY" AlonzoBbodyPredFailure era
  , Embed (EraRule "LEDGERS" era) (AlonzoBBODY era)
  , Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era
  , State (EraRule "LEDGERS" era) ~ LedgerState era
  , Signal (EraRule "LEDGERS" era) ~ Seq (Tx TopTx era)
  , AlonzoEraTxWits era
  , EraBlockBody era
  , AlonzoEraPParams era
  ) =>
  STS (AlonzoBBODY era)
  where
  type State (AlonzoBBODY era) = ShelleyBbodyState era

  type Signal (AlonzoBBODY era) = Block BHeaderView era

  type Environment (AlonzoBBODY era) = BbodyEnv era

  type BaseM (AlonzoBBODY era) = ShelleyBase

  type PredicateFailure (AlonzoBBODY era) = AlonzoBbodyPredFailure era
  type Event (AlonzoBBODY era) = AlonzoBbodyEvent era

  initialRules :: [InitialRule (AlonzoBBODY era)]
initialRules = []
  transitionRules :: [TransitionRule (AlonzoBBODY era)]
transitionRules = [forall era.
(STS (EraRule "BBODY" era),
 Signal (EraRule "BBODY" era) ~ Block BHeaderView era,
 InjectRuleFailure "BBODY" AlonzoBbodyPredFailure era,
 BaseM (EraRule "BBODY" era) ~ ShelleyBase,
 State (EraRule "BBODY" era) ~ ShelleyBbodyState era,
 Environment (EraRule "BBODY" era) ~ BbodyEnv era,
 Embed (EraRule "LEDGERS" era) (EraRule "BBODY" era),
 Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era,
 State (EraRule "LEDGERS" era) ~ LedgerState era,
 Signal (EraRule "LEDGERS" era) ~ Seq (Tx TopTx era),
 EraBlockBody era, AlonzoEraTxWits era, AlonzoEraPParams era) =>
TransitionRule (EraRule "BBODY" era)
alonzoBbodyTransition @era]

instance
  ( Era era
  , BaseM ledgers ~ ShelleyBase
  , ledgers ~ EraRule "LEDGERS" era
  , STS ledgers
  , Era era
  ) =>
  Embed ledgers (AlonzoBBODY era)
  where
  wrapFailed :: PredicateFailure ledgers -> PredicateFailure (AlonzoBBODY era)
wrapFailed = ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
forall era.
ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
ShelleyInAlonzoBbodyPredFailure (ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era)
-> (PredicateFailure ledgers -> ShelleyBbodyPredFailure era)
-> PredicateFailure ledgers
-> AlonzoBbodyPredFailure era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure ledgers -> ShelleyBbodyPredFailure era
PredicateFailure (EraRule "LEDGERS" era)
-> ShelleyBbodyPredFailure era
forall era.
PredicateFailure (EraRule "LEDGERS" era)
-> ShelleyBbodyPredFailure era
LedgersFailure
  wrapEvent :: Event ledgers -> Event (AlonzoBBODY era)
wrapEvent = ShelleyBbodyEvent era -> AlonzoBbodyEvent era
forall era. ShelleyBbodyEvent era -> AlonzoBbodyEvent era
ShelleyInAlonzoEvent (ShelleyBbodyEvent era -> AlonzoBbodyEvent era)
-> (Event ledgers -> ShelleyBbodyEvent era)
-> Event ledgers
-> AlonzoBbodyEvent era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Event ledgers -> ShelleyBbodyEvent era
Event (EraRule "LEDGERS" era) -> ShelleyBbodyEvent era
forall era. Event (EraRule "LEDGERS" era) -> ShelleyBbodyEvent era
LedgersEvent