{-# 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 (..), ShelleyBase, epochInfoPure)
import Cardano.Ledger.Binary (DecCBOR (..), EncCBOR (..))
import Cardano.Ledger.Binary.Coders
import Cardano.Ledger.Block (Block (..))
import Cardano.Ledger.Core
import qualified Cardano.Ledger.Era as Era
import Cardano.Ledger.Keys (DSignable, Hash, 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
      -- | Computed Sum of ExUnits for all plutus scripts
      !ExUnits
      -- | Maximum allowed by protocal parameters
      !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 c) = AlonzoBbodyPredFailure (AlonzoEra c)

instance InjectRuleFailure "BBODY" AlonzoBbodyPredFailure (AlonzoEra c)

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

instance InjectRuleFailure "BBODY" ShelleyLedgersPredFailure (AlonzoEra c) where
  injectFailure :: ShelleyLedgersPredFailure (AlonzoEra c)
-> EraRuleFailure "BBODY" (AlonzoEra c)
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 c) where
  injectFailure :: ShelleyLedgerPredFailure (AlonzoEra c)
-> EraRuleFailure "BBODY" (AlonzoEra c)
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 c) where
  injectFailure :: AlonzoUtxowPredFailure (AlonzoEra c)
-> EraRuleFailure "BBODY" (AlonzoEra c)
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 c) where
  injectFailure :: ShelleyUtxowPredFailure (AlonzoEra c)
-> EraRuleFailure "BBODY" (AlonzoEra c)
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 c) where
  injectFailure :: AlonzoUtxoPredFailure (AlonzoEra c)
-> EraRuleFailure "BBODY" (AlonzoEra c)
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 c) where
  injectFailure :: AlonzoUtxosPredFailure (AlonzoEra c)
-> EraRuleFailure "BBODY" (AlonzoEra c)
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 c) where
  injectFailure :: ShelleyPpupPredFailure (AlonzoEra c)
-> EraRuleFailure "BBODY" (AlonzoEra c)
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 c) where
  injectFailure :: ShelleyUtxoPredFailure (AlonzoEra c)
-> EraRuleFailure "BBODY" (AlonzoEra c)
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 c) where
  injectFailure :: AllegraUtxoPredFailure (AlonzoEra c)
-> EraRuleFailure "BBODY" (AlonzoEra c)
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 c) where
  injectFailure :: ShelleyDelegsPredFailure (AlonzoEra c)
-> EraRuleFailure "BBODY" (AlonzoEra c)
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 c) where
  injectFailure :: ShelleyDelplPredFailure (AlonzoEra c)
-> EraRuleFailure "BBODY" (AlonzoEra c)
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 c) where
  injectFailure :: ShelleyPoolPredFailure (AlonzoEra c)
-> EraRuleFailure "BBODY" (AlonzoEra c)
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 c) where
  injectFailure :: ShelleyDelegPredFailure (AlonzoEra c)
-> EraRuleFailure "BBODY" (AlonzoEra c)
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 ExUnits
x ExUnits
y) = forall (w :: Wrapped) t. Encode w t -> Encoding
encode (forall t. t -> Word -> Encode 'Open t
Sum forall era. ExUnits -> 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 ExUnits
x 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 ExUnits
y)

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. ExUnits -> 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 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 (EraCrypto era)) 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
  , 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 (EraCrypto era)) 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 (EraCrypto era)
b
              , UnserialisedBlock BHeaderView (EraCrypto era)
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 (EraCrypto era)) EraIndependentBlockBody
actualBodyHash = forall era.
EraSegWits era =>
TxSeq era -> Hash (HASH (EraCrypto era)) 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 (forall c. BHeaderView c -> Word32
bhviewBSize BHeaderView (EraCrypto era)
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
$ forall c. BHeaderView c -> Word32
bhviewBSize BHeaderView (EraCrypto era)
bh
                        }
                  )
              )

        Hash (HASH (EraCrypto era)) EraIndependentBlockBody
actualBodyHash
          forall a. Eq a => a -> a -> Bool
== forall c. BHeaderView c -> Hash c EraIndependentBlockBody
bhviewBHash BHeaderView (EraCrypto era)
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 (EraCrypto era) EraIndependentBlockBody)
-> ShelleyBbodyPredFailure era
InvalidBodyHashBBODY @era forall a b. (a -> b) -> a -> b
$
                      Mismatch
                        { mismatchSupplied :: Hash (HASH (EraCrypto era)) EraIndependentBlockBody
mismatchSupplied = Hash (HASH (EraCrypto era)) EraIndependentBlockBody
actualBodyHash
                        , mismatchExpected :: Hash (HASH (EraCrypto era)) EraIndependentBlockBody
mismatchExpected = forall c. BHeaderView c -> Hash c EraIndependentBlockBody
bhviewBHash BHeaderView (EraCrypto era)
bh
                        }
                  )
              )

        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 -> PParams era -> AccountState -> ShelleyLedgersEnv era
LedgersEnv (forall c. BHeaderView c -> SlotNo
bhviewSlot BHeaderView (EraCrypto era)
bh) PParams era
pp AccountState
account, State (EraRule "LEDGERS" era)
ls, forall a. StrictSeq a -> Seq a
StrictSeq.fromStrict StrictSeq (Tx era)
txs)

        -- 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 (EraCrypto era)
hkAsStakePool = forall (a :: KeyRole -> * -> *) (r :: KeyRole) c (r' :: KeyRole).
HasKeyRole a =>
a r c -> a r' c
coerceKeyRole forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c. BHeaderView c -> KeyHash 'BlockIssuer c
bhviewID forall a b. (a -> b) -> a -> b
$ BHeaderView (EraCrypto era)
bh
            slot :: SlotNo
slot = forall c. BHeaderView c -> SlotNo
bhviewSlot BHeaderView (EraCrypto era)
bh
        SlotNo
firstSlotNo <- 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
          EpochNo
e <- HasCallStack => EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
epochInfoEpoch EpochInfo Identity
ei SlotNo
slot
          HasCallStack => EpochInfo Identity -> EpochNo -> ShelleyBase SlotNo
epochInfoFirst EpochInfo Identity
ei EpochNo
e

        {- ∑(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. ExUnits -> ExUnits -> AlonzoBbodyPredFailure era
TooManyExUnits ExUnits
txTotal 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 (EraCrypto era) -> ShelleyBbodyState era
BbodyState @era
            LedgerState era
ls'
            ( forall c.
Bool -> KeyHash 'StakePool c -> BlocksMade c -> BlocksMade c
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 (EraCrypto era)
hkAsStakePool
                BlocksMade (EraCrypto era)
b
            )

instance
  ( DSignable (EraCrypto era) (Hash (EraCrypto era) EraIndependentTxBody)
  , 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
  , 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 (EraCrypto era)) 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 (EraCrypto era)) 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
  , DSignable (EraCrypto era) (Hash (EraCrypto era) EraIndependentTxBody)
  , 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