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

module Cardano.Ledger.Shelley.Rules.Bbody (
  ShelleyBBODY,
  ShelleyBbodyState (..),
  BbodyEnv (..),
  ShelleyBbodyPredFailure (..),
  ShelleyBbodyEvent (..),
  PredicateFailure,
  State,
) where

import Cardano.Ledger.BHeaderView (BHeaderView (..), isOverlaySlot)
import Cardano.Ledger.BaseTypes (
  BlocksMade,
  Mismatch (..),
  Relation (..),
  ShelleyBase,
  epochInfoPure,
 )
import Cardano.Ledger.Block (Block (..))
import Cardano.Ledger.Core
import Cardano.Ledger.Keys (coerceKeyRole)
import Cardano.Ledger.Shelley.BlockChain (incrBlocks)
import Cardano.Ledger.Shelley.Era (ShelleyBBODY, ShelleyEra)
import Cardano.Ledger.Shelley.LedgerState (ChainAccountState)
import Cardano.Ledger.Shelley.Rules.Deleg (ShelleyDelegPredFailure)
import Cardano.Ledger.Shelley.Rules.Delegs (ShelleyDelegsPredFailure)
import Cardano.Ledger.Shelley.Rules.Delpl (ShelleyDelplPredFailure)
import Cardano.Ledger.Shelley.Rules.Ledger (ShelleyLedgerPredFailure)
import Cardano.Ledger.Shelley.Rules.Ledgers (ShelleyLedgersEnv (..), ShelleyLedgersPredFailure)
import Cardano.Ledger.Shelley.Rules.Pool (ShelleyPoolPredFailure)
import Cardano.Ledger.Shelley.Rules.Ppup (ShelleyPpupPredFailure)
import Cardano.Ledger.Shelley.Rules.Utxo (ShelleyUtxoPredFailure)
import Cardano.Ledger.Shelley.Rules.Utxow (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 GHC.Generics (Generic)
import Lens.Micro ((^.))
import NoThunks.Class (NoThunks (..))

data ShelleyBbodyState era
  = BbodyState !(State (EraRule "LEDGERS" era)) !BlocksMade

deriving stock instance Show (State (EraRule "LEDGERS" era)) => Show (ShelleyBbodyState era)

deriving stock instance Eq (State (EraRule "LEDGERS" era)) => Eq (ShelleyBbodyState era)

data BbodyEnv era = BbodyEnv
  { forall era. BbodyEnv era -> PParams era
bbodyPp :: PParams era
  , forall era. BbodyEnv era -> ChainAccountState
bbodyAccount :: ChainAccountState
  }

data ShelleyBbodyPredFailure era
  = -- | `mismatchSupplied` ~ Actual body size.
    --   `mismatchExpected` ~ Claimed body size in the header.
    WrongBlockBodySizeBBODY (Mismatch 'RelEQ Int)
  | -- | `mismatchSupplied` ~ Actual hash.
    --   `mismatchExpected` ~ Claimed hash in the header.
    InvalidBodyHashBBODY (Mismatch 'RelEQ (Hash HASH EraIndependentBlockBody))
  | LedgersFailure (PredicateFailure (EraRule "LEDGERS" era)) -- Subtransition Failures
  deriving ((forall x.
 ShelleyBbodyPredFailure era -> Rep (ShelleyBbodyPredFailure era) x)
-> (forall x.
    Rep (ShelleyBbodyPredFailure era) x -> ShelleyBbodyPredFailure era)
-> Generic (ShelleyBbodyPredFailure era)
forall x.
Rep (ShelleyBbodyPredFailure era) x -> ShelleyBbodyPredFailure era
forall x.
ShelleyBbodyPredFailure era -> Rep (ShelleyBbodyPredFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyBbodyPredFailure era) x -> ShelleyBbodyPredFailure era
forall era x.
ShelleyBbodyPredFailure era -> Rep (ShelleyBbodyPredFailure era) x
$cfrom :: forall era x.
ShelleyBbodyPredFailure era -> Rep (ShelleyBbodyPredFailure era) x
from :: forall x.
ShelleyBbodyPredFailure era -> Rep (ShelleyBbodyPredFailure era) x
$cto :: forall era x.
Rep (ShelleyBbodyPredFailure era) x -> ShelleyBbodyPredFailure era
to :: forall x.
Rep (ShelleyBbodyPredFailure era) x -> ShelleyBbodyPredFailure era
Generic)

type instance EraRuleFailure "BBODY" ShelleyEra = ShelleyBbodyPredFailure ShelleyEra

instance InjectRuleFailure "BBODY" ShelleyBbodyPredFailure ShelleyEra

instance InjectRuleFailure "BBODY" ShelleyLedgersPredFailure ShelleyEra where
  injectFailure :: ShelleyLedgersPredFailure ShelleyEra
-> EraRuleFailure "BBODY" ShelleyEra
injectFailure = PredicateFailure (EraRule "LEDGERS" ShelleyEra)
-> ShelleyBbodyPredFailure ShelleyEra
ShelleyLedgersPredFailure ShelleyEra
-> EraRuleFailure "BBODY" ShelleyEra
forall era.
PredicateFailure (EraRule "LEDGERS" era)
-> ShelleyBbodyPredFailure era
LedgersFailure

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

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

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

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

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

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

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

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

newtype ShelleyBbodyEvent era
  = LedgersEvent (Event (EraRule "LEDGERS" era))

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

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

instance
  ( Era era
  , NoThunks (PredicateFailure (EraRule "LEDGERS" era))
  ) =>
  NoThunks (ShelleyBbodyPredFailure era)

instance
  ( EraSegWits era
  , Embed (EraRule "LEDGERS" era) (ShelleyBBODY era)
  , Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era
  , Signal (EraRule "LEDGERS" era) ~ Seq (Tx era)
  ) =>
  STS (ShelleyBBODY era)
  where
  type
    State (ShelleyBBODY era) =
      ShelleyBbodyState era

  type
    Signal (ShelleyBBODY era) =
      Block BHeaderView era

  type Environment (ShelleyBBODY era) = BbodyEnv era

  type BaseM (ShelleyBBODY era) = ShelleyBase

  type PredicateFailure (ShelleyBBODY era) = ShelleyBbodyPredFailure era

  type Event (ShelleyBBODY era) = ShelleyBbodyEvent era

  initialRules :: [InitialRule (ShelleyBBODY era)]
initialRules = []
  transitionRules :: [TransitionRule (ShelleyBBODY era)]
transitionRules = [TransitionRule (ShelleyBBODY era)
forall era.
(STS (ShelleyBBODY era), EraSegWits era,
 Embed (EraRule "LEDGERS" era) (ShelleyBBODY era),
 Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era,
 Signal (EraRule "LEDGERS" era) ~ Seq (Tx era)) =>
TransitionRule (ShelleyBBODY era)
bbodyTransition]

bbodyTransition ::
  forall era.
  ( STS (ShelleyBBODY era)
  , EraSegWits era
  , Embed (EraRule "LEDGERS" era) (ShelleyBBODY era)
  , Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era
  , Signal (EraRule "LEDGERS" era) ~ Seq (Tx era)
  ) =>
  TransitionRule (ShelleyBBODY era)
bbodyTransition :: forall era.
(STS (ShelleyBBODY era), EraSegWits era,
 Embed (EraRule "LEDGERS" era) (ShelleyBBODY era),
 Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era,
 Signal (EraRule "LEDGERS" era) ~ Seq (Tx era)) =>
TransitionRule (ShelleyBBODY era)
bbodyTransition =
  Rule
  (ShelleyBBODY era)
  'Transition
  (RuleContext 'Transition (ShelleyBBODY era))
F (Clause (ShelleyBBODY era) 'Transition) (TRC (ShelleyBBODY era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
    F (Clause (ShelleyBBODY era) 'Transition) (TRC (ShelleyBBODY era))
-> (TRC (ShelleyBBODY era)
    -> F (Clause (ShelleyBBODY era) 'Transition)
         (ShelleyBbodyState era))
-> F (Clause (ShelleyBBODY era) 'Transition)
     (ShelleyBbodyState era)
forall a b.
F (Clause (ShelleyBBODY era) 'Transition) a
-> (a -> F (Clause (ShelleyBBODY era) 'Transition) b)
-> F (Clause (ShelleyBBODY 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
bhview TxSeq era
txsSeq
               )
           ) -> do
        let txs :: StrictSeq (Tx era)
txs = TxSeq era -> StrictSeq (Tx era)
forall era. EraSegWits era => TxSeq era -> StrictSeq (Tx era)
fromTxSeq TxSeq 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 = TxSeq era -> Hash HASH EraIndependentBlockBody
forall era.
EraSegWits era =>
TxSeq era -> Hash HASH EraIndependentBlockBody
hashTxSeq 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
bhview)
            Bool
-> PredicateFailure (ShelleyBBODY era)
-> Rule (ShelleyBBODY era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Mismatch 'RelEQ Int -> ShelleyBbodyPredFailure era
forall era. Mismatch 'RelEQ Int -> ShelleyBbodyPredFailure era
WrongBlockBodySizeBBODY
              ( 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
bhview
                  }
              )

        Hash HASH EraIndependentBlockBody
actualBodyHash
          Hash HASH EraIndependentBlockBody
-> Hash HASH EraIndependentBlockBody -> Bool
forall a. Eq a => a -> a -> Bool
== BHeaderView -> Hash HASH EraIndependentBlockBody
bhviewBHash BHeaderView
bhview
            Bool
-> PredicateFailure (ShelleyBBODY era)
-> Rule (ShelleyBBODY era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Mismatch 'RelEQ (Hash HASH EraIndependentBlockBody)
-> ShelleyBbodyPredFailure era
forall era.
Mismatch 'RelEQ (Hash HASH EraIndependentBlockBody)
-> ShelleyBbodyPredFailure era
InvalidBodyHashBBODY
              ( Mismatch
                  { mismatchSupplied :: Hash HASH EraIndependentBlockBody
mismatchSupplied = Hash HASH EraIndependentBlockBody
actualBodyHash
                  , mismatchExpected :: Hash HASH EraIndependentBlockBody
mismatchExpected = BHeaderView -> Hash HASH EraIndependentBlockBody
bhviewBHash BHeaderView
bhview
                  }
              )
        -- 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.
        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
bhview
            slot :: SlotNo
slot = BHeaderView -> SlotNo
bhviewSlot BHeaderView
bhview
        (SlotNo
firstSlotNo, EpochNo
curEpochNo) <- BaseM (ShelleyBBODY era) (SlotNo, EpochNo)
-> Rule (ShelleyBBODY era) 'Transition (SlotNo, EpochNo)
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (ShelleyBBODY era) (SlotNo, EpochNo)
 -> Rule (ShelleyBBODY era) 'Transition (SlotNo, EpochNo))
-> BaseM (ShelleyBBODY era) (SlotNo, EpochNo)
-> Rule (ShelleyBBODY 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)

        State (EraRule "LEDGERS" 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)
 -> F (Clause (ShelleyBBODY era) 'Transition)
      (State (EraRule "LEDGERS" era)))
-> RuleContext 'Transition (EraRule "LEDGERS" era)
-> F (Clause (ShelleyBBODY 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
bhview) EpochNo
curEpochNo PParams era
pp ChainAccountState
account, State (EraRule "LEDGERS" era)
ls, StrictSeq (Tx era) -> Seq (Tx era)
forall a. StrictSeq a -> Seq a
StrictSeq.fromStrict StrictSeq (Tx era)
txs)

        let isOverlay :: Bool
isOverlay = 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
        ShelleyBbodyState era
-> F (Clause (ShelleyBBODY era) 'Transition)
     (ShelleyBbodyState era)
forall a. a -> F (Clause (ShelleyBBODY era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ShelleyBbodyState era
 -> F (Clause (ShelleyBBODY era) 'Transition)
      (ShelleyBbodyState era))
-> ShelleyBbodyState era
-> F (Clause (ShelleyBBODY era) 'Transition)
     (ShelleyBbodyState era)
forall a b. (a -> b) -> a -> b
$ State (EraRule "LEDGERS" era)
-> BlocksMade -> ShelleyBbodyState era
forall era.
State (EraRule "LEDGERS" era)
-> BlocksMade -> ShelleyBbodyState era
BbodyState State (EraRule "LEDGERS" era)
ls' (Bool -> KeyHash 'StakePool -> BlocksMade -> BlocksMade
incrBlocks Bool
isOverlay KeyHash 'StakePool
hkAsStakePool BlocksMade
b)

instance
  forall era ledgers.
  ( Era era
  , BaseM ledgers ~ ShelleyBase
  , ledgers ~ EraRule "LEDGERS" era
  , STS ledgers
  , Era era
  ) =>
  Embed ledgers (ShelleyBBODY era)
  where
  wrapFailed :: PredicateFailure ledgers -> PredicateFailure (ShelleyBBODY era)
wrapFailed = PredicateFailure ledgers -> PredicateFailure (ShelleyBBODY era)
PredicateFailure (EraRule "LEDGERS" era)
-> ShelleyBbodyPredFailure era
forall era.
PredicateFailure (EraRule "LEDGERS" era)
-> ShelleyBbodyPredFailure era
LedgersFailure
  wrapEvent :: Event ledgers -> Event (ShelleyBBODY era)
wrapEvent = Event ledgers -> Event (ShelleyBBODY era)
Event (EraRule "LEDGERS" era) -> ShelleyBbodyEvent era
forall era. Event (EraRule "LEDGERS" era) -> ShelleyBbodyEvent era
LedgersEvent