{-# 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 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)

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 = 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
  ( Typeable era
  , EncCBOR (ShelleyBbodyPredFailure 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 Any) -> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode ((Mismatch 'RelLTEQ ExUnits -> AlonzoBbodyPredFailure Any)
-> Word
-> Encode
     'Open (Mismatch 'RelLTEQ ExUnits -> AlonzoBbodyPredFailure Any)
forall t. t -> Word -> Encode 'Open t
Sum Mismatch 'RelLTEQ ExUnits -> AlonzoBbodyPredFailure Any
forall era. Mismatch 'RelLTEQ ExUnits -> AlonzoBbodyPredFailure era
TooManyExUnits Word
1 Encode
  'Open (Mismatch 'RelLTEQ ExUnits -> AlonzoBbodyPredFailure Any)
-> Encode ('Closed 'Dense) (Mismatch 'RelLTEQ ExUnits)
-> Encode 'Open (AlonzoBbodyPredFailure Any)
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
  ( 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 = 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}.
(Typeable era, DecCBOR (ShelleyBbodyPredFailure 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 Any) (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 Any) (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 Any) (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 Any) (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 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 =
  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 TxSeq era
txsSeq
               )
           ) -> do
        let txs :: StrictSeq (Tx era)
txs = AlonzoTxSeq era -> StrictSeq (Tx era)
forall era. AlonzoTxSeq era -> StrictSeq (Tx era)
txSeqTxns TxSeq era
AlonzoTxSeq era
txsSeq
            actualBodySize :: Int
actualBodySize = ProtVer -> TxSeq era -> Int
forall era. EraSegWits era => ProtVer -> TxSeq 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) TxSeq era
txsSeq
            actualBodyHash :: Hash HASH EraIndependentBlockBody
actualBodyHash = forall era.
EraSegWits era =>
TxSeq era -> Hash HASH EraIndependentBlockBody
hashTxSeq @era TxSeq 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
        (SlotNo
firstSlotNo, EpochNo
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
          EpochInfo Identity
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 :: EpochNo
curEpochNo = HasCallStack => EpochInfo Identity -> SlotNo -> EpochNo
EpochInfo Identity -> SlotNo -> EpochNo
epochInfoEpoch EpochInfo Identity
ei SlotNo
slot
          (SlotNo, EpochNo) -> ReaderT Globals Identity (SlotNo, EpochNo)
forall a. a -> ReaderT Globals Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HasCallStack => EpochInfo Identity -> EpochNo -> SlotNo
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) (RuleContext 'Transition (EraRule "LEDGERS" era)
 -> Rule
      (EraRule "BBODY" era) 'Transition (State (EraRule "LEDGERS" era)))
-> RuleContext 'Transition (EraRule "LEDGERS" era)
-> Rule
     (EraRule "BBODY" era) 'Transition (State (EraRule "LEDGERS" era))
forall a b. (a -> b) -> a -> b
$
            (Environment (EraRule "LEDGERS" era),
 State (EraRule "LEDGERS" era), Signal (EraRule "LEDGERS" era))
-> TRC (EraRule "LEDGERS" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (SlotNo
-> EpochNo
-> PParams era
-> ChainAccountState
-> ShelleyLedgersEnv era
forall era.
SlotNo
-> EpochNo
-> PParams era
-> ChainAccountState
-> ShelleyLedgersEnv era
LedgersEnv (BHeaderView -> SlotNo
bhviewSlot BHeaderView
bh) EpochNo
curEpochNo PParams era
pp ChainAccountState
account, State (EraRule "LEDGERS" era)
ls, StrictSeq (AlonzoTx era) -> Seq (AlonzoTx era)
forall a. StrictSeq a -> Seq a
StrictSeq.fromStrict StrictSeq (Tx era)
StrictSeq (AlonzoTx era)
txs)

        {- ∑(tx ∈ txs)(totExunits tx) ≤ maxBlockExUnits pp  -}
        let txTotal, ppMax :: ExUnits
            txTotal :: ExUnits
txTotal = (Tx era -> ExUnits) -> StrictSeq (Tx 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 era -> ExUnits
forall era. (EraTx era, AlonzoEraTxWits era) => Tx era -> ExUnits
totExUnits StrictSeq (Tx era)
txs
            ppMax :: ExUnits
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
        (Natural -> Natural -> Bool) -> ExUnits -> ExUnits -> Bool
pointWiseExUnits Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
(<=) ExUnits
txTotal ExUnits
ppMax
          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 (Mismatch 'RelLTEQ ExUnits -> AlonzoBbodyPredFailure era
forall era. Mismatch 'RelLTEQ ExUnits -> AlonzoBbodyPredFailure era
TooManyExUnits Mismatch {mismatchSupplied :: ExUnits
mismatchSupplied = ExUnits
txTotal, mismatchExpected :: ExUnits
mismatchExpected = ExUnits
ppMax})

        ShelleyBbodyState era
-> F (Clause (EraRule "BBODY" era) 'Transition)
     (ShelleyBbodyState era)
forall a. a -> F (Clause (EraRule "BBODY" era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ShelleyBbodyState era
 -> F (Clause (EraRule "BBODY" era) 'Transition)
      (ShelleyBbodyState era))
-> ShelleyBbodyState era
-> F (Clause (EraRule "BBODY" era) 'Transition)
     (ShelleyBbodyState era)
forall a b. (a -> b) -> a -> b
$
          forall era.
State (EraRule "LEDGERS" era)
-> BlocksMade -> ShelleyBbodyState era
BbodyState @era
            State (EraRule "LEDGERS" era)
LedgerState era
ls'
            ( Bool -> KeyHash 'StakePool -> BlocksMade -> BlocksMade
incrBlocks
                (SlotNo -> UnitInterval -> SlotNo -> Bool
isOverlaySlot SlotNo
firstSlotNo (PParams era
pp PParams era
-> Getting UnitInterval (PParams era) UnitInterval -> UnitInterval
forall s a. s -> Getting a s a -> a
^. Getting UnitInterval (PParams era) UnitInterval
forall era.
EraPParams era =>
SimpleGetter (PParams era) UnitInterval
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 = 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