{-# 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 (AccountState)
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 -> AccountState
bbodyAccount :: AccountState
  }

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 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
$cto :: forall era x.
Rep (ShelleyBbodyPredFailure era) x -> ShelleyBbodyPredFailure era
$cfrom :: forall era x.
ShelleyBbodyPredFailure era -> Rep (ShelleyBbodyPredFailure era) x
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 = forall era.
PredicateFailure (EraRule "LEDGERS" era)
-> ShelleyBbodyPredFailure era
LedgersFailure

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

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

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

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

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

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

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

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

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 = [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 =
  forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \( TRC
            ( BbodyEnv PParams era
pp AccountState
account
              , BbodyState State (EraRule "LEDGERS" era)
ls BlocksMade
b
              , UnserialisedBlock BHeaderView
bhview TxSeq era
txsSeq
              )
          ) -> do
        let txs :: StrictSeq (Tx era)
txs = forall era. EraSegWits era => TxSeq era -> StrictSeq (Tx era)
fromTxSeq TxSeq era
txsSeq
            actualBodySize :: Int
actualBodySize = forall era. EraSegWits era => ProtVer -> TxSeq era -> Int
bBodySize (PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) ProtVer
ppProtocolVersionL) TxSeq era
txsSeq
            actualBodyHash :: Hash HASH EraIndependentBlockBody
actualBodyHash = forall era.
EraSegWits era =>
TxSeq era -> Hash HASH EraIndependentBlockBody
hashTxSeq TxSeq era
txsSeq

        Int
actualBodySize
          forall a. Eq a => a -> a -> Bool
== forall a b. (Integral a, Num b) => a -> b
fromIntegral (BHeaderView -> Word32
bhviewBSize BHeaderView
bhview)
            forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era. Mismatch 'RelEQ Int -> ShelleyBbodyPredFailure era
WrongBlockBodySizeBBODY
              ( Mismatch
                  { mismatchSupplied :: Int
mismatchSupplied = Int
actualBodySize
                  , mismatchExpected :: Int
mismatchExpected = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ BHeaderView -> Word32
bhviewBSize BHeaderView
bhview
                  }
              )

        Hash HASH EraIndependentBlockBody
actualBodyHash
          forall a. Eq a => a -> a -> Bool
== BHeaderView -> Hash HASH EraIndependentBlockBody
bhviewBHash BHeaderView
bhview
            forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! 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 = forall (a :: KeyRole -> *) (r :: KeyRole) (r' :: KeyRole).
HasKeyRole a =>
a r -> a r'
coerceKeyRole 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) <- forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS forall a b. (a -> b) -> a -> b
$ do
          EpochInfo Identity
ei <- forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> EpochInfo Identity
epochInfoPure
          let curEpochNo :: EpochNo
curEpochNo = HasCallStack => EpochInfo Identity -> SlotNo -> EpochNo
epochInfoEpoch EpochInfo Identity
ei SlotNo
slot
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (HasCallStack => 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) forall a b. (a -> b) -> a -> b
$
            forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (forall era.
SlotNo
-> EpochNo -> PParams era -> AccountState -> ShelleyLedgersEnv era
LedgersEnv (BHeaderView -> SlotNo
bhviewSlot BHeaderView
bhview) EpochNo
curEpochNo PParams era
pp AccountState
account, State (EraRule "LEDGERS" era)
ls, 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 forall s a. s -> Getting a s a -> a
^. forall era.
EraPParams era =>
SimpleGetter (PParams era) UnitInterval
ppDG) SlotNo
slot
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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 = forall era.
PredicateFailure (EraRule "LEDGERS" era)
-> ShelleyBbodyPredFailure era
LedgersFailure
  wrapEvent :: Event ledgers -> Event (ShelleyBBODY era)
wrapEvent = forall era. Event (EraRule "LEDGERS" era) -> ShelleyBbodyEvent era
LedgersEvent