{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# 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.Binary (DecCBOR (..), EncCBOR (..))
import Cardano.Ledger.Binary.Coders (
  Decode (From, FromGroup, Invalid, SumD, Summands),
  Encode (Sum, To, ToGroup),
  decode,
  encode,
  (!>),
  (<!),
 )
import Cardano.Ledger.Block (Block (..))
import Cardano.Ledger.Core
import Cardano.Ledger.Keys (coerceKeyRole)
import Cardano.Ledger.Shelley.BlockBody (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 ((forall x. ShelleyBbodyState era -> Rep (ShelleyBbodyState era) x)
-> (forall x.
    Rep (ShelleyBbodyState era) x -> ShelleyBbodyState era)
-> Generic (ShelleyBbodyState era)
forall x. Rep (ShelleyBbodyState era) x -> ShelleyBbodyState era
forall x. ShelleyBbodyState era -> Rep (ShelleyBbodyState era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyBbodyState era) x -> ShelleyBbodyState era
forall era x.
ShelleyBbodyState era -> Rep (ShelleyBbodyState era) x
$cfrom :: forall era x.
ShelleyBbodyState era -> Rep (ShelleyBbodyState era) x
from :: forall x. ShelleyBbodyState era -> Rep (ShelleyBbodyState era) x
$cto :: forall era x.
Rep (ShelleyBbodyState era) x -> ShelleyBbodyState era
to :: forall x. Rep (ShelleyBbodyState era) x -> ShelleyBbodyState era
Generic)

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

instance
  ( Era era
  , EncCBOR (PredicateFailure (EraRule "LEDGERS" era))
  ) =>
  EncCBOR (ShelleyBbodyPredFailure era)
  where
  encCBOR :: ShelleyBbodyPredFailure era -> Encoding
encCBOR =
    Encode Open (ShelleyBbodyPredFailure era) -> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode (Encode Open (ShelleyBbodyPredFailure era) -> Encoding)
-> (ShelleyBbodyPredFailure era
    -> Encode Open (ShelleyBbodyPredFailure era))
-> ShelleyBbodyPredFailure era
-> Encoding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      WrongBlockBodySizeBBODY Mismatch RelEQ Int
mm -> (Mismatch RelEQ Int -> ShelleyBbodyPredFailure era)
-> Word
-> Encode Open (Mismatch RelEQ Int -> ShelleyBbodyPredFailure era)
forall t. t -> Word -> Encode Open t
Sum Mismatch RelEQ Int -> ShelleyBbodyPredFailure era
forall era. Mismatch RelEQ Int -> ShelleyBbodyPredFailure era
WrongBlockBodySizeBBODY Word
0 Encode Open (Mismatch RelEQ Int -> ShelleyBbodyPredFailure era)
-> Encode (Closed Dense) (Mismatch RelEQ Int)
-> Encode Open (ShelleyBbodyPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> Mismatch RelEQ Int -> Encode (Closed Dense) (Mismatch RelEQ Int)
forall t. EncCBORGroup t => t -> Encode (Closed Dense) t
ToGroup Mismatch RelEQ Int
mm
      InvalidBodyHashBBODY Mismatch RelEQ (Hash HASH EraIndependentBlockBody)
mm -> (Mismatch RelEQ (Hash HASH EraIndependentBlockBody)
 -> ShelleyBbodyPredFailure era)
-> Word
-> Encode
     Open
     (Mismatch RelEQ (Hash HASH EraIndependentBlockBody)
      -> ShelleyBbodyPredFailure era)
forall t. t -> Word -> Encode Open t
Sum (forall era.
Mismatch RelEQ (Hash HASH EraIndependentBlockBody)
-> ShelleyBbodyPredFailure era
InvalidBodyHashBBODY @era) Word
1 Encode
  Open
  (Mismatch RelEQ (Hash HASH EraIndependentBlockBody)
   -> ShelleyBbodyPredFailure era)
-> Encode
     (Closed Dense) (Mismatch RelEQ (Hash HASH EraIndependentBlockBody))
-> Encode Open (ShelleyBbodyPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> Mismatch RelEQ (Hash HASH EraIndependentBlockBody)
-> Encode
     (Closed Dense) (Mismatch RelEQ (Hash HASH EraIndependentBlockBody))
forall t. EncCBORGroup t => t -> Encode (Closed Dense) t
ToGroup Mismatch RelEQ (Hash HASH EraIndependentBlockBody)
mm
      LedgersFailure PredicateFailure (EraRule "LEDGERS" era)
x -> (PredicateFailure (EraRule "LEDGERS" era)
 -> ShelleyBbodyPredFailure era)
-> Word
-> Encode
     Open
     (PredicateFailure (EraRule "LEDGERS" era)
      -> ShelleyBbodyPredFailure era)
forall t. t -> Word -> Encode Open t
Sum (forall era.
PredicateFailure (EraRule "LEDGERS" era)
-> ShelleyBbodyPredFailure era
LedgersFailure @era) Word
2 Encode
  Open
  (PredicateFailure (EraRule "LEDGERS" era)
   -> ShelleyBbodyPredFailure era)
-> Encode (Closed Dense) (PredicateFailure (EraRule "LEDGERS" era))
-> Encode Open (ShelleyBbodyPredFailure era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> PredicateFailure (EraRule "LEDGERS" era)
-> Encode (Closed Dense) (PredicateFailure (EraRule "LEDGERS" era))
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To PredicateFailure (EraRule "LEDGERS" era)
x

instance
  ( Era era
  , DecCBOR (PredicateFailure (EraRule "LEDGERS" era))
  ) =>
  DecCBOR (ShelleyBbodyPredFailure era)
  where
  decCBOR :: forall s. Decoder s (ShelleyBbodyPredFailure era)
decCBOR = Decode (Closed Dense) (ShelleyBbodyPredFailure era)
-> Decoder s (ShelleyBbodyPredFailure era)
forall t (w :: Wrapped) s. Typeable t => Decode w t -> Decoder s t
decode (Decode (Closed Dense) (ShelleyBbodyPredFailure era)
 -> Decoder s (ShelleyBbodyPredFailure era))
-> ((Word -> Decode Open (ShelleyBbodyPredFailure era))
    -> Decode (Closed Dense) (ShelleyBbodyPredFailure era))
-> (Word -> Decode Open (ShelleyBbodyPredFailure era))
-> Decoder s (ShelleyBbodyPredFailure era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text
-> (Word -> Decode Open (ShelleyBbodyPredFailure era))
-> Decode (Closed Dense) (ShelleyBbodyPredFailure era)
forall t.
Text -> (Word -> Decode Open t) -> Decode (Closed Dense) t
Summands Text
"ShelleyBbodyPredFailure" ((Word -> Decode Open (ShelleyBbodyPredFailure era))
 -> Decoder s (ShelleyBbodyPredFailure era))
-> (Word -> Decode Open (ShelleyBbodyPredFailure era))
-> Decoder s (ShelleyBbodyPredFailure era)
forall a b. (a -> b) -> a -> b
$ \case
    Word
0 -> (Mismatch RelEQ Int -> ShelleyBbodyPredFailure era)
-> Decode Open (Mismatch RelEQ Int -> ShelleyBbodyPredFailure era)
forall t. t -> Decode Open t
SumD Mismatch RelEQ Int -> ShelleyBbodyPredFailure era
forall era. Mismatch RelEQ Int -> ShelleyBbodyPredFailure era
WrongBlockBodySizeBBODY Decode Open (Mismatch RelEQ Int -> ShelleyBbodyPredFailure era)
-> Decode (Closed (ZonkAny 0)) (Mismatch RelEQ Int)
-> Decode Open (ShelleyBbodyPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode (Closed (ZonkAny 0)) (Mismatch RelEQ Int)
forall t (w :: Wrapped).
(EncCBORGroup t, DecCBORGroup t) =>
Decode w t
FromGroup
    Word
1 -> (Mismatch RelEQ (Hash HASH EraIndependentBlockBody)
 -> ShelleyBbodyPredFailure era)
-> Decode
     Open
     (Mismatch RelEQ (Hash HASH EraIndependentBlockBody)
      -> ShelleyBbodyPredFailure era)
forall t. t -> Decode Open t
SumD Mismatch RelEQ (Hash HASH EraIndependentBlockBody)
-> ShelleyBbodyPredFailure era
forall era.
Mismatch RelEQ (Hash HASH EraIndependentBlockBody)
-> ShelleyBbodyPredFailure era
InvalidBodyHashBBODY Decode
  Open
  (Mismatch RelEQ (Hash HASH EraIndependentBlockBody)
   -> ShelleyBbodyPredFailure era)
-> Decode
     (Closed (ZonkAny 1))
     (Mismatch RelEQ (Hash HASH EraIndependentBlockBody))
-> Decode Open (ShelleyBbodyPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode
  (Closed (ZonkAny 1))
  (Mismatch RelEQ (Hash HASH EraIndependentBlockBody))
forall t (w :: Wrapped).
(EncCBORGroup t, DecCBORGroup t) =>
Decode w t
FromGroup
    Word
2 -> (PredicateFailure (EraRule "LEDGERS" era)
 -> ShelleyBbodyPredFailure era)
-> Decode
     Open
     (PredicateFailure (EraRule "LEDGERS" era)
      -> ShelleyBbodyPredFailure era)
forall t. t -> Decode Open t
SumD PredicateFailure (EraRule "LEDGERS" era)
-> ShelleyBbodyPredFailure era
forall era.
PredicateFailure (EraRule "LEDGERS" era)
-> ShelleyBbodyPredFailure era
LedgersFailure Decode
  Open
  (PredicateFailure (EraRule "LEDGERS" era)
   -> ShelleyBbodyPredFailure era)
-> Decode
     (Closed (ZonkAny 2)) (PredicateFailure (EraRule "LEDGERS" era))
-> Decode Open (ShelleyBbodyPredFailure era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode (Closed w) a -> Decode w1 t
<! Decode
  (Closed (ZonkAny 2)) (PredicateFailure (EraRule "LEDGERS" era))
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
    Word
n -> Word -> Decode Open (ShelleyBbodyPredFailure era)
forall (w :: Wrapped) t. Word -> Decode w t
Invalid Word
n

newtype ShelleyBbodyEvent era
  = LedgersEvent (Event (EraRule "LEDGERS" era))
  deriving ((forall x. ShelleyBbodyEvent era -> Rep (ShelleyBbodyEvent era) x)
-> (forall x.
    Rep (ShelleyBbodyEvent era) x -> ShelleyBbodyEvent era)
-> Generic (ShelleyBbodyEvent era)
forall x. Rep (ShelleyBbodyEvent era) x -> ShelleyBbodyEvent era
forall x. ShelleyBbodyEvent era -> Rep (ShelleyBbodyEvent era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ShelleyBbodyEvent era) x -> ShelleyBbodyEvent era
forall era x.
ShelleyBbodyEvent era -> Rep (ShelleyBbodyEvent era) x
$cfrom :: forall era x.
ShelleyBbodyEvent era -> Rep (ShelleyBbodyEvent era) x
from :: forall x. ShelleyBbodyEvent era -> Rep (ShelleyBbodyEvent era) x
$cto :: forall era x.
Rep (ShelleyBbodyEvent era) x -> ShelleyBbodyEvent era
to :: forall x. Rep (ShelleyBbodyEvent era) x -> ShelleyBbodyEvent era
Generic)

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
  ( EraBlockBody era
  , Embed (EraRule "LEDGERS" era) (ShelleyBBODY era)
  , Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era
  , Signal (EraRule "LEDGERS" era) ~ Seq (Tx TopTx 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), EraBlockBody era,
 Embed (EraRule "LEDGERS" era) (ShelleyBBODY era),
 Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era,
 Signal (EraRule "LEDGERS" era) ~ Seq (Tx TopTx era)) =>
TransitionRule (ShelleyBBODY era)
bbodyTransition]

bbodyTransition ::
  forall era.
  ( STS (ShelleyBBODY era)
  , EraBlockBody era
  , Embed (EraRule "LEDGERS" era) (ShelleyBBODY era)
  , Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era
  , Signal (EraRule "LEDGERS" era) ~ Seq (Tx TopTx era)
  ) =>
  TransitionRule (ShelleyBBODY era)
bbodyTransition :: forall era.
(STS (ShelleyBBODY era), EraBlockBody era,
 Embed (EraRule "LEDGERS" era) (ShelleyBBODY era),
 Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era,
 Signal (EraRule "LEDGERS" era) ~ Seq (Tx TopTx 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 {blockHeader :: forall h era. Block h era -> h
blockHeader = BHeaderView
blockHeaderView, BlockBody era
blockBody :: BlockBody era
blockBody :: forall h era. Block h era -> BlockBody era
blockBody}
               )
           ) -> do
        let txs :: StrictSeq (Tx TopTx era)
txs = BlockBody era
blockBody BlockBody era
-> Getting
     (StrictSeq (Tx TopTx era))
     (BlockBody era)
     (StrictSeq (Tx TopTx era))
-> StrictSeq (Tx TopTx era)
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictSeq (Tx TopTx era))
  (BlockBody era)
  (StrictSeq (Tx TopTx era))
forall era.
EraBlockBody era =>
Lens' (BlockBody era) (StrictSeq (Tx TopTx era))
Lens' (BlockBody era) (StrictSeq (Tx TopTx era))
txSeqBlockBodyL
            actualBodySize :: Int
actualBodySize = ProtVer -> BlockBody era -> Int
forall era. EraBlockBody era => ProtVer -> BlockBody era -> Int
bBodySize (PParams era
pp PParams era -> Getting ProtVer (PParams era) ProtVer -> ProtVer
forall s a. s -> Getting a s a -> a
^. Getting ProtVer (PParams era) ProtVer
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams era) ProtVer
ppProtocolVersionL) BlockBody era
blockBody
            actualBodyHash :: Hash HASH EraIndependentBlockBody
actualBodyHash = BlockBody era -> Hash HASH EraIndependentBlockBody
forall era.
EraBlockBody era =>
BlockBody era -> Hash HASH EraIndependentBlockBody
hashBlockBody BlockBody era
blockBody

        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
blockHeaderView)
            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
blockHeaderView
                  }
              )

        Hash HASH EraIndependentBlockBody
actualBodyHash
          Hash HASH EraIndependentBlockBody
-> Hash HASH EraIndependentBlockBody -> Bool
forall a. Eq a => a -> a -> Bool
== BHeaderView -> Hash HASH EraIndependentBlockBody
bhviewBHash BHeaderView
blockHeaderView
            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
blockHeaderView
                  }
              )
        -- 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
blockHeaderView
            slot :: SlotNo
slot = BHeaderView -> SlotNo
bhviewSlot BHeaderView
blockHeaderView
        (firstSlotNo, 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
          ei <- (Globals -> EpochInfo Identity)
-> ReaderT Globals Identity (EpochInfo Identity)
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> EpochInfo Identity
epochInfoPure
          let curEpochNo = HasCallStack => EpochInfo Identity -> SlotNo -> EpochNo
EpochInfo Identity -> SlotNo -> EpochNo
epochInfoEpoch EpochInfo Identity
ei SlotNo
slot
          pure (epochInfoFirst ei curEpochNo, curEpochNo)

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

        let 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
        pure $ BbodyState ls' (incrBlocks isOverlay hkAsStakePool 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