{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# 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 (..),
  BbodySignal (..),
  ShelleyBbodyPredFailure (..),
  ShelleyBbodyEvent (..),
  PredicateFailure,
  State,
  validateBlockBodySize,
  validateBlockBodyHash,
) where

import Cardano.Ledger.BaseTypes (
  BlocksMade,
  Mismatch (..),
  ProtVer,
  Relation (..),
  ShelleyBase,
 )
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 (BbodySignal (..), Block (..), EraBlockHeader (..))
import Cardano.Ledger.Core
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 (slotToEpochBoundary)
import Control.DeepSeq (NFData)
import Control.State.Transition (
  Embed (..),
  Rule,
  RuleType (..),
  STS (..),
  TRC (..),
  TransitionRule,
  judgmentContext,
  liftSTS,
  trans,
  (?!),
 )
import Data.Sequence (Seq)
import qualified Data.Sequence.Strict as StrictSeq
import GHC.Generics (Generic)
import Lens.Micro ((^.))

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)

instance NFData (PredicateFailure (EraRule "LEDGERS" era)) => NFData (ShelleyBbodyPredFailure era)

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 instance
  Eq (Event (EraRule "LEDGERS" era)) =>
  Eq (ShelleyBbodyEvent 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
  ( EraBlockBody era
  , EraRule "BBODY" era ~ ShelleyBBODY era
  , InjectRuleFailure "BBODY" ShelleyBbodyPredFailure 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) = BbodySignal 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), EraRule "BBODY" era ~ ShelleyBBODY era,
 EraBlockBody era, Embed (EraRule "LEDGERS" era) (ShelleyBBODY era),
 Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era,
 Signal (EraRule "LEDGERS" era) ~ Seq (Tx TopTx era),
 InjectRuleFailure "BBODY" ShelleyBbodyPredFailure era) =>
TransitionRule (ShelleyBBODY era)
bbodyTransition]

bbodyTransition ::
  forall era.
  ( STS (ShelleyBBODY era)
  , EraRule "BBODY" era ~ ShelleyBBODY era
  , EraBlockBody era
  , Embed (EraRule "LEDGERS" era) (ShelleyBBODY era)
  , Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era
  , Signal (EraRule "LEDGERS" era) ~ Seq (Tx TopTx era)
  , InjectRuleFailure "BBODY" ShelleyBbodyPredFailure era
  ) =>
  TransitionRule (ShelleyBBODY era)
bbodyTransition :: forall era.
(STS (ShelleyBBODY era), EraRule "BBODY" era ~ ShelleyBBODY era,
 EraBlockBody era, Embed (EraRule "LEDGERS" era) (ShelleyBBODY era),
 Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era,
 Signal (EraRule "LEDGERS" era) ~ Seq (Tx TopTx era),
 InjectRuleFailure "BBODY" ShelleyBbodyPredFailure era) =>
TransitionRule (ShelleyBBODY era)
bbodyTransition = do
  TRC (BbodyEnv pp account, BbodyState ls blocksMade, BbodySignal block@Block {blockBody}) <-
    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

  validateBlockBodySize block (pp ^. ppProtocolVersionL)

  validateBlockBodyHash block

  let bhSlot = Block h era
block Block h era -> Getting SlotNo (Block h era) SlotNo -> SlotNo
forall s a. s -> Getting a s a -> a
^. Getting SlotNo (Block h era) SlotNo
forall h era. EraBlockHeader h era => Lens' (Block h era) SlotNo
Lens' (Block h era) SlotNo
slotNoBlockHeaderL

  (firstSlot, curEpoch) <- liftSTS $ slotToEpochBoundary bhSlot

  ls' <-
    trans @(EraRule "LEDGERS" era) $
      TRC
        ( LedgersEnv bhSlot curEpoch pp account
        , ls
        , StrictSeq.fromStrict $ blockBody ^. txSeqBlockBodyL
        )

  pure $ BbodyState ls' $ incrBlocks block firstSlot (pp ^. ppDG) blocksMade

-- | Validate that actual block body size matches claimed size in block header.
validateBlockBodySize ::
  forall h era.
  ( EraBlockHeader h era
  , EraBlockBody era
  , InjectRuleFailure "BBODY" ShelleyBbodyPredFailure era
  ) =>
  Block h era ->
  ProtVer ->
  Rule (EraRule "BBODY" era) 'Transition ()
validateBlockBodySize :: forall h era.
(EraBlockHeader h era, EraBlockBody era,
 InjectRuleFailure "BBODY" ShelleyBbodyPredFailure era) =>
Block h era -> ProtVer -> Rule (EraRule "BBODY" era) 'Transition ()
validateBlockBodySize Block h era
block ProtVer
protVer =
  Int
actualSize
    Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
sizeInBlockHeader
      Bool
-> PredicateFailure (EraRule "BBODY" era)
-> F (Clause (EraRule "BBODY" era) 'Transition) ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! ShelleyBbodyPredFailure era -> EraRuleFailure "BBODY" era
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure
        ( 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
actualSize
              , mismatchExpected :: Int
mismatchExpected = Int
sizeInBlockHeader
              }
        )
  where
    actualSize :: Int
actualSize = ProtVer -> BlockBody era -> Int
forall era. EraBlockBody era => ProtVer -> BlockBody era -> Int
bBodySize ProtVer
protVer (BlockBody era -> Int) -> BlockBody era -> Int
forall a b. (a -> b) -> a -> b
$ Block h era -> BlockBody era
forall h era. Block h era -> BlockBody era
blockBody Block h era
block
    sizeInBlockHeader :: Int
sizeInBlockHeader = Word32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word32 -> Int) -> Word32 -> Int
forall a b. (a -> b) -> a -> b
$ Block h era
block Block h era -> Getting Word32 (Block h era) Word32 -> Word32
forall s a. s -> Getting a s a -> a
^. Getting Word32 (Block h era) Word32
forall h era. EraBlockHeader h era => Lens' (Block h era) Word32
Lens' (Block h era) Word32
blockBodySizeBlockHeaderL

-- | Validate that actual block body hash matches claimed hash in block header.
validateBlockBodyHash ::
  forall h era.
  ( EraBlockHeader h era
  , EraBlockBody era
  , InjectRuleFailure "BBODY" ShelleyBbodyPredFailure era
  ) =>
  Block h era ->
  Rule (EraRule "BBODY" era) 'Transition ()
validateBlockBodyHash :: forall h era.
(EraBlockHeader h era, EraBlockBody era,
 InjectRuleFailure "BBODY" ShelleyBbodyPredFailure era) =>
Block h era -> Rule (EraRule "BBODY" era) 'Transition ()
validateBlockBodyHash Block h era
block =
  Hash HASH EraIndependentBlockBody
actualHash
    Hash HASH EraIndependentBlockBody
-> Hash HASH EraIndependentBlockBody -> Bool
forall a. Eq a => a -> a -> Bool
== Hash HASH EraIndependentBlockBody
hashInBlockHeader
      Bool
-> PredicateFailure (EraRule "BBODY" era)
-> F (Clause (EraRule "BBODY" era) 'Transition) ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! ShelleyBbodyPredFailure era -> EraRuleFailure "BBODY" era
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure
        ( Mismatch RelEQ (Hash HASH EraIndependentBlockBody)
-> ShelleyBbodyPredFailure era
forall era.
Mismatch RelEQ (Hash HASH EraIndependentBlockBody)
-> ShelleyBbodyPredFailure era
InvalidBodyHashBBODY (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
actualHash
              , mismatchExpected :: Hash HASH EraIndependentBlockBody
mismatchExpected = Hash HASH EraIndependentBlockBody
hashInBlockHeader
              }
        )
  where
    actualHash :: Hash HASH EraIndependentBlockBody
actualHash = BlockBody era -> Hash HASH EraIndependentBlockBody
forall era.
EraBlockBody era =>
BlockBody era -> Hash HASH EraIndependentBlockBody
hashBlockBody (BlockBody era -> Hash HASH EraIndependentBlockBody)
-> BlockBody era -> Hash HASH EraIndependentBlockBody
forall a b. (a -> b) -> a -> b
$ Block h era -> BlockBody era
forall h era. Block h era -> BlockBody era
blockBody Block h era
block
    hashInBlockHeader :: Hash HASH EraIndependentBlockBody
hashInBlockHeader = Block h era
block Block h era
-> Getting
     (Hash HASH EraIndependentBlockBody)
     (Block h era)
     (Hash HASH EraIndependentBlockBody)
-> Hash HASH EraIndependentBlockBody
forall s a. s -> Getting a s a -> a
^. Getting
  (Hash HASH EraIndependentBlockBody)
  (Block h era)
  (Hash HASH EraIndependentBlockBody)
forall h era.
EraBlockHeader h era =>
Lens' (Block h era) (Hash HASH EraIndependentBlockBody)
Lens' (Block h era) (Hash HASH EraIndependentBlockBody)
blockBodyHashBlockHeaderL

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