{-# 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.Era (AlonzoBBODY, AlonzoEra)
import Cardano.Ledger.Alonzo.PParams (AlonzoEraPParams, ppMaxBlockExUnitsL)
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 (AlonzoTx, totExUnits)
import Cardano.Ledger.Alonzo.TxSeq (AlonzoTxSeq, txSeqTxns)
import Cardano.Ledger.Alonzo.TxWits (AlonzoEraTxWits (..))
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.Core
import Cardano.Ledger.Keys (coerceKeyRole)
import Cardano.Ledger.Shelley.BlockChain (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.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 Data.Typeable
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 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
$cto :: forall era x.
Rep (AlonzoBbodyPredFailure era) x -> AlonzoBbodyPredFailure era
$cfrom :: forall era x.
AlonzoBbodyPredFailure era -> Rep (AlonzoBbodyPredFailure era) x
Generic)

newtype AlonzoBbodyEvent era
  = ShelleyInAlonzoEvent (ShelleyBbodyEvent 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 = forall era.
ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
ShelleyInAlonzoBbodyPredFailure

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

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

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

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

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

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

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

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

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

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

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

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

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

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
  ( Typeable era
  , EncCBOR (ShelleyBbodyPredFailure era)
  ) =>
  EncCBOR (AlonzoBbodyPredFailure era)
  where
  encCBOR :: AlonzoBbodyPredFailure era -> Encoding
encCBOR (ShelleyInAlonzoBbodyPredFailure ShelleyBbodyPredFailure era
x) = forall (w :: Wrapped) t. Encode w t -> Encoding
encode (forall t. t -> Word -> Encode 'Open t
Sum forall era.
ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
ShelleyInAlonzoBbodyPredFailure Word
0 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To ShelleyBbodyPredFailure era
x)
  encCBOR (TooManyExUnits Mismatch 'RelLTEQ ExUnits
m) = forall (w :: Wrapped) t. Encode w t -> Encoding
encode (forall t. t -> Word -> Encode 'Open t
Sum forall era. Mismatch 'RelLTEQ ExUnits -> AlonzoBbodyPredFailure era
TooManyExUnits Word
1 forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Mismatch 'RelLTEQ ExUnits
m)

instance
  ( Typeable era
  , DecCBOR (ShelleyBbodyPredFailure era) -- TODO why is there no DecCBOR for (ShelleyBbodyPredFailure era)
  ) =>
  DecCBOR (AlonzoBbodyPredFailure era)
  where
  decCBOR :: forall s. Decoder s (AlonzoBbodyPredFailure era)
decCBOR = forall (w :: Wrapped) t s. Decode w t -> Decoder s t
decode (forall t.
Text -> (Word -> Decode 'Open t) -> Decode ('Closed 'Dense) t
Summands Text
"AlonzoBbodyPredFail" forall {era}.
DecCBOR (ShelleyBbodyPredFailure era) =>
Word -> Decode 'Open (AlonzoBbodyPredFailure era)
dec)
    where
      dec :: Word -> Decode 'Open (AlonzoBbodyPredFailure era)
dec Word
0 = forall t. t -> Decode 'Open t
SumD forall era.
ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
ShelleyInAlonzoBbodyPredFailure forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
      dec Word
1 = forall t. t -> Decode 'Open t
SumD forall era. Mismatch 'RelLTEQ ExUnits -> AlonzoBbodyPredFailure era
TooManyExUnits forall (w1 :: Wrapped) a t (w :: Density).
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! forall t (w :: Wrapped). DecCBOR t => Decode w t
From
      dec Word
n = 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 era)
  , EraSegWits era
  , AlonzoEraTxWits era
  , TxSeq era ~ AlonzoTxSeq era
  , Tx era ~ AlonzoTx 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 era), EraSegWits era,
 AlonzoEraTxWits era, TxSeq era ~ AlonzoTxSeq era,
 Tx era ~ AlonzoTx era, AlonzoEraPParams era) =>
TransitionRule (EraRule "BBODY" era)
alonzoBbodyTransition =
  forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \( TRC
            ( BbodyEnv PParams era
pp AccountState
account
              , BbodyState State (EraRule "LEDGERS" era)
ls BlocksMade
b
              , UnserialisedBlock BHeaderView
bh TxSeq era
txsSeq
              )
          ) -> do
        let txs :: StrictSeq (Tx era)
txs = forall era. AlonzoTxSeq era -> StrictSeq (Tx era)
txSeqTxns TxSeq era
txsSeq
            actualBodySize :: Int
actualBodySize = forall era. EraSegWits era => ProtVer -> TxSeq era -> Int
bBodySize (PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) ProtVer
ppProtocolVersionL) TxSeq era
txsSeq
            actualBodyHash :: Hash HASH EraIndependentBlockBody
actualBodyHash = forall era.
EraSegWits era =>
TxSeq era -> Hash HASH EraIndependentBlockBody
hashTxSeq @era TxSeq era
txsSeq

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

        Hash HASH EraIndependentBlockBody
actualBodyHash
          forall a. Eq a => a -> a -> Bool
== BHeaderView -> Hash HASH EraIndependentBlockBody
bhviewBHash BHeaderView
bh
            forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure
              ( forall era.
ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
ShelleyInAlonzoBbodyPredFailure
                  ( forall era.
Mismatch 'RelEQ (Hash HASH EraIndependentBlockBody)
-> ShelleyBbodyPredFailure era
InvalidBodyHashBBODY @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 = forall (a :: KeyRole -> *) (r :: KeyRole) (r' :: KeyRole).
HasKeyRole a =>
a r -> a r'
coerceKeyRole forall a b. (a -> b) -> a -> b
$ BHeaderView -> KeyHash 'BlockIssuer
bhviewID BHeaderView
bh
            slot :: SlotNo
slot = BHeaderView -> SlotNo
bhviewSlot BHeaderView
bh
        (SlotNo
firstSlotNo, EpochNo
curEpochNo) <- forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS forall a b. (a -> b) -> a -> b
$ do
          EpochInfo Identity
ei <- forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> EpochInfo Identity
epochInfoPure
          let curEpochNo :: EpochNo
curEpochNo = HasCallStack => EpochInfo Identity -> SlotNo -> EpochNo
epochInfoEpoch EpochInfo Identity
ei SlotNo
slot
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (HasCallStack => EpochInfo Identity -> EpochNo -> SlotNo
epochInfoFirst EpochInfo Identity
ei EpochNo
curEpochNo, EpochNo
curEpochNo)

        LedgerState era
ls' <-
          forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "LEDGERS" era) forall a b. (a -> b) -> a -> b
$
            forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (forall era.
SlotNo
-> EpochNo -> PParams era -> AccountState -> ShelleyLedgersEnv era
LedgersEnv (BHeaderView -> SlotNo
bhviewSlot BHeaderView
bh) EpochNo
curEpochNo PParams era
pp AccountState
account, State (EraRule "LEDGERS" era)
ls, forall a. StrictSeq a -> Seq a
StrictSeq.fromStrict StrictSeq (Tx era)
txs)

        {- ∑(tx ∈ txs)(totExunits tx) ≤ maxBlockExUnits pp  -}
        let txTotal, ppMax :: ExUnits
            txTotal :: ExUnits
txTotal = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall era. (EraTx era, AlonzoEraTxWits era) => Tx era -> ExUnits
totExUnits StrictSeq (Tx era)
txs
            ppMax :: ExUnits
ppMax = PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. AlonzoEraPParams era => Lens' (PParams era) ExUnits
ppMaxBlockExUnitsL
        (Natural -> Natural -> Bool) -> ExUnits -> ExUnits -> Bool
pointWiseExUnits forall a. Ord a => a -> a -> Bool
(<=) ExUnits
txTotal ExUnits
ppMax
          forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure (forall era. Mismatch 'RelLTEQ ExUnits -> AlonzoBbodyPredFailure era
TooManyExUnits Mismatch {mismatchSupplied :: ExUnits
mismatchSupplied = ExUnits
txTotal, mismatchExpected :: ExUnits
mismatchExpected = ExUnits
ppMax})

        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
          forall era.
State (EraRule "LEDGERS" era)
-> BlocksMade -> ShelleyBbodyState era
BbodyState @era
            LedgerState era
ls'
            ( Bool -> KeyHash 'StakePool -> BlocksMade -> BlocksMade
incrBlocks
                (SlotNo -> UnitInterval -> SlotNo -> Bool
isOverlaySlot SlotNo
firstSlotNo (PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era.
EraPParams era =>
SimpleGetter (PParams era) UnitInterval
ppDG) SlotNo
slot)
                KeyHash 'StakePool
hkAsStakePool
                BlocksMade
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 (AlonzoTx era)
  , AlonzoEraTxWits era
  , Tx era ~ AlonzoTx era
  , TxSeq era ~ AlonzoTxSeq era
  , Tx era ~ AlonzoTx era
  , EraSegWits 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 era), EraSegWits era,
 AlonzoEraTxWits era, TxSeq era ~ AlonzoTxSeq era,
 Tx era ~ AlonzoTx 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 = forall era.
ShelleyBbodyPredFailure era -> AlonzoBbodyPredFailure era
ShelleyInAlonzoBbodyPredFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
PredicateFailure (EraRule "LEDGERS" era)
-> ShelleyBbodyPredFailure era
LedgersFailure
  wrapEvent :: Event ledgers -> Event (AlonzoBBODY era)
wrapEvent = forall era. ShelleyBbodyEvent era -> AlonzoBbodyEvent era
ShelleyInAlonzoEvent forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Event (EraRule "LEDGERS" era) -> ShelleyBbodyEvent era
LedgersEvent