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

module Cardano.Ledger.Shelley.Rules.Bbody
  ( BBODY,
    BbodyState (..),
    BbodyEnv (..),
    BbodyPredicateFailure (..),
    BbodyEvent (..),
    PredicateFailure,
    State,
  )
where

import Cardano.Ledger.BHeaderView (BHeaderView (..), isOverlaySlot)
import Cardano.Ledger.BaseTypes (BlocksMade, ShelleyBase, UnitInterval, epochInfoPure)
import Cardano.Ledger.Block (Block (..))
import qualified Cardano.Ledger.Core as Core
import Cardano.Ledger.Era (Era (Crypto), SupportsSegWit (fromTxSeq, hashTxSeq))
import qualified Cardano.Ledger.Era as Era
import Cardano.Ledger.Hashes (EraIndependentBlockBody, EraIndependentTxBody)
import Cardano.Ledger.Keys (DSignable, Hash, coerceKeyRole)
import Cardano.Ledger.Serialization (ToCBORGroup)
import Cardano.Ledger.Shelley.BlockChain (bBodySize, incrBlocks)
import Cardano.Ledger.Shelley.Constraints (UsesAuxiliary, UsesTxBody)
import Cardano.Ledger.Shelley.LedgerState
  ( AccountState,
    LedgerState,
  )
import Cardano.Ledger.Shelley.Rules.Ledgers (LedgersEnv (..))
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 GHC.Records
import NoThunks.Class (NoThunks (..))

data BBODY era

data BbodyState era
  = BbodyState (LedgerState era) (BlocksMade (Crypto era))

deriving stock instance Show (LedgerState era) => Show (BbodyState era)

deriving stock instance Eq (LedgerState era) => Eq (BbodyState era)

data BbodyEnv era = BbodyEnv
  { BbodyEnv era -> PParams era
bbodyPp :: Core.PParams era,
    BbodyEnv era -> AccountState
bbodyAccount :: AccountState
  }

data BbodyPredicateFailure era
  = WrongBlockBodySizeBBODY
      !Int -- Actual Body Size
      !Int -- Claimed Body Size in Header
  | InvalidBodyHashBBODY
      !(Hash (Crypto era) EraIndependentBlockBody) -- Actual Hash
      !(Hash (Crypto era) EraIndependentBlockBody) -- Claimed Hash
  | LedgersFailure (PredicateFailure (Core.EraRule "LEDGERS" era)) -- Subtransition Failures
  deriving ((forall x.
 BbodyPredicateFailure era -> Rep (BbodyPredicateFailure era) x)
-> (forall x.
    Rep (BbodyPredicateFailure era) x -> BbodyPredicateFailure era)
-> Generic (BbodyPredicateFailure era)
forall x.
Rep (BbodyPredicateFailure era) x -> BbodyPredicateFailure era
forall x.
BbodyPredicateFailure era -> Rep (BbodyPredicateFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (BbodyPredicateFailure era) x -> BbodyPredicateFailure era
forall era x.
BbodyPredicateFailure era -> Rep (BbodyPredicateFailure era) x
$cto :: forall era x.
Rep (BbodyPredicateFailure era) x -> BbodyPredicateFailure era
$cfrom :: forall era x.
BbodyPredicateFailure era -> Rep (BbodyPredicateFailure era) x
Generic)

newtype BbodyEvent era
  = LedgersEvent (Event (Core.EraRule "LEDGERS" era))

deriving stock instance
  ( Era era,
    Show (PredicateFailure (Core.EraRule "LEDGERS" era))
  ) =>
  Show (BbodyPredicateFailure era)

deriving stock instance
  ( Era era,
    Eq (PredicateFailure (Core.EraRule "LEDGERS" era))
  ) =>
  Eq (BbodyPredicateFailure era)

instance
  ( Era era,
    NoThunks (PredicateFailure (Core.EraRule "LEDGERS" era))
  ) =>
  NoThunks (BbodyPredicateFailure era)

instance
  ( UsesTxBody era,
    UsesAuxiliary era,
    ToCBORGroup (Era.TxSeq era),
    DSignable (Crypto era) (Hash (Crypto era) EraIndependentTxBody),
    Embed (Core.EraRule "LEDGERS" era) (BBODY era),
    Environment (Core.EraRule "LEDGERS" era) ~ LedgersEnv era,
    State (Core.EraRule "LEDGERS" era) ~ LedgerState era,
    Signal (Core.EraRule "LEDGERS" era) ~ Seq (Core.Tx era),
    HasField "_d" (Core.PParams era) UnitInterval
  ) =>
  STS (BBODY era)
  where
  type
    State (BBODY era) =
      BbodyState era

  type
    Signal (BBODY era) =
      Block (BHeaderView (Crypto era)) era

  type Environment (BBODY era) = BbodyEnv era

  type BaseM (BBODY era) = ShelleyBase

  type PredicateFailure (BBODY era) = BbodyPredicateFailure era

  type Event (BBODY era) = BbodyEvent era

  initialRules :: [InitialRule (BBODY era)]
initialRules = []
  transitionRules :: [TransitionRule (BBODY era)]
transitionRules = [TransitionRule (BBODY era)
forall era.
(STS (BBODY era), UsesTxBody era, ToCBORGroup (TxSeq era),
 Embed (EraRule "LEDGERS" era) (BBODY era),
 Environment (EraRule "LEDGERS" era) ~ LedgersEnv era,
 State (EraRule "LEDGERS" era) ~ LedgerState era,
 Signal (EraRule "LEDGERS" era) ~ Seq (Tx era),
 HasField "_d" (PParams era) UnitInterval) =>
TransitionRule (BBODY era)
bbodyTransition]

bbodyTransition ::
  forall era.
  ( STS (BBODY era),
    UsesTxBody era,
    ToCBORGroup (Era.TxSeq era),
    Embed (Core.EraRule "LEDGERS" era) (BBODY era),
    Environment (Core.EraRule "LEDGERS" era) ~ LedgersEnv era,
    State (Core.EraRule "LEDGERS" era) ~ LedgerState era,
    Signal (Core.EraRule "LEDGERS" era) ~ Seq (Core.Tx era),
    HasField "_d" (Core.PParams era) UnitInterval
  ) =>
  TransitionRule (BBODY era)
bbodyTransition :: TransitionRule (BBODY era)
bbodyTransition =
  F (Clause (BBODY era) 'Transition) (TRC (BBODY era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
    F (Clause (BBODY era) 'Transition) (TRC (BBODY era))
-> (TRC (BBODY era)
    -> F (Clause (BBODY era) 'Transition) (BbodyState era))
-> F (Clause (BBODY era) 'Transition) (BbodyState era)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \( TRC
             ( BbodyEnv pp account,
               BbodyState ls b,
               UnserialisedBlock bhview txsSeq
               )
           ) -> do
        let txs :: StrictSeq (Tx era)
txs = TxSeq era -> StrictSeq (Tx era)
forall era. SupportsSegWit era => TxSeq era -> StrictSeq (Tx era)
fromTxSeq @era TxSeq era
txsSeq
            actualBodySize :: Int
actualBodySize = TxSeq era -> Int
forall txSeq. ToCBORGroup txSeq => txSeq -> Int
bBodySize TxSeq era
txsSeq
            actualBodyHash :: Hash (HASH (Crypto era)) EraIndependentBlockBody
actualBodyHash = TxSeq era -> Hash (HASH (Crypto era)) EraIndependentBlockBody
forall era.
SupportsSegWit era =>
TxSeq era -> Hash (HASH (Crypto era)) EraIndependentBlockBody
hashTxSeq @era TxSeq era
txsSeq

        Int
actualBodySize Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (BHeaderView (Crypto era) -> Natural
forall crypto. BHeaderView crypto -> Natural
bhviewBSize BHeaderView (Crypto era)
bhview)
          Bool
-> PredicateFailure (BBODY era) -> Rule (BBODY era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Int -> Int -> BbodyPredicateFailure era
forall era. Int -> Int -> BbodyPredicateFailure era
WrongBlockBodySizeBBODY Int
actualBodySize (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ BHeaderView (Crypto era) -> Natural
forall crypto. BHeaderView crypto -> Natural
bhviewBSize BHeaderView (Crypto era)
bhview)

        Hash (HASH (Crypto era)) EraIndependentBlockBody
actualBodyHash Hash (HASH (Crypto era)) EraIndependentBlockBody
-> Hash (HASH (Crypto era)) EraIndependentBlockBody -> Bool
forall a. Eq a => a -> a -> Bool
== BHeaderView (Crypto era)
-> Hash (HASH (Crypto era)) EraIndependentBlockBody
forall crypto.
BHeaderView crypto -> Hash crypto EraIndependentBlockBody
bhviewBHash BHeaderView (Crypto era)
bhview Bool
-> PredicateFailure (BBODY era) -> Rule (BBODY era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! Hash (HASH (Crypto era)) EraIndependentBlockBody
-> Hash (HASH (Crypto era)) EraIndependentBlockBody
-> BbodyPredicateFailure era
forall era.
Hash (Crypto era) EraIndependentBlockBody
-> Hash (Crypto era) EraIndependentBlockBody
-> BbodyPredicateFailure era
InvalidBodyHashBBODY Hash (HASH (Crypto era)) EraIndependentBlockBody
actualBodyHash (BHeaderView (Crypto era)
-> Hash (HASH (Crypto era)) EraIndependentBlockBody
forall crypto.
BHeaderView crypto -> Hash crypto EraIndependentBlockBody
bhviewBHash BHeaderView (Crypto era)
bhview)

        LedgerState era
ls' <-
          forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (EraRule "LEDGERS" era) super =>
RuleContext rtype (EraRule "LEDGERS" era)
-> Rule super rtype (State (EraRule "LEDGERS" era))
trans @(Core.EraRule "LEDGERS" era) (RuleContext 'Transition (EraRule "LEDGERS" era)
 -> Rule (BBODY era) 'Transition (State (EraRule "LEDGERS" era)))
-> RuleContext 'Transition (EraRule "LEDGERS" era)
-> Rule (BBODY era) 'Transition (State (EraRule "LEDGERS" era))
forall a b. (a -> b) -> a -> b
$
            (Environment (EraRule "LEDGERS" era),
 State (EraRule "LEDGERS" era), Signal (EraRule "LEDGERS" era))
-> TRC (EraRule "LEDGERS" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (SlotNo -> PParams era -> AccountState -> LedgersEnv era
forall era. SlotNo -> PParams era -> AccountState -> LedgersEnv era
LedgersEnv (BHeaderView (Crypto era) -> SlotNo
forall crypto. BHeaderView crypto -> SlotNo
bhviewSlot BHeaderView (Crypto era)
bhview) PParams era
pp AccountState
account, State (EraRule "LEDGERS" era)
LedgerState era
ls, StrictSeq (Tx era) -> Seq (Tx era)
forall a. StrictSeq a -> Seq a
StrictSeq.fromStrict StrictSeq (Tx era)
txs)

        -- 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 (Crypto era)
hkAsStakePool = KeyHash 'BlockIssuer (Crypto era)
-> KeyHash 'StakePool (Crypto era)
forall (a :: KeyRole -> * -> *) (r :: KeyRole) crypto
       (r' :: KeyRole).
HasKeyRole a =>
a r crypto -> a r' crypto
coerceKeyRole (KeyHash 'BlockIssuer (Crypto era)
 -> KeyHash 'StakePool (Crypto era))
-> (BHeaderView (Crypto era) -> KeyHash 'BlockIssuer (Crypto era))
-> BHeaderView (Crypto era)
-> KeyHash 'StakePool (Crypto era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BHeaderView (Crypto era) -> KeyHash 'BlockIssuer (Crypto era)
forall crypto. BHeaderView crypto -> KeyHash 'BlockIssuer crypto
bhviewID (BHeaderView (Crypto era) -> KeyHash 'StakePool (Crypto era))
-> BHeaderView (Crypto era) -> KeyHash 'StakePool (Crypto era)
forall a b. (a -> b) -> a -> b
$ BHeaderView (Crypto era)
bhview
            slot :: SlotNo
slot = BHeaderView (Crypto era) -> SlotNo
forall crypto. BHeaderView crypto -> SlotNo
bhviewSlot BHeaderView (Crypto era)
bhview
        SlotNo
firstSlotNo <- BaseM (BBODY era) SlotNo -> Rule (BBODY era) 'Transition SlotNo
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (BBODY era) SlotNo -> Rule (BBODY era) 'Transition SlotNo)
-> BaseM (BBODY era) SlotNo -> Rule (BBODY era) 'Transition SlotNo
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
          EpochNo
e <- HasCallStack => EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
epochInfoEpoch EpochInfo Identity
ei SlotNo
slot
          HasCallStack => EpochInfo Identity -> EpochNo -> ShelleyBase SlotNo
EpochInfo Identity -> EpochNo -> ShelleyBase SlotNo
epochInfoFirst EpochInfo Identity
ei EpochNo
e
        BbodyState era
-> F (Clause (BBODY era) 'Transition) (BbodyState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BbodyState era
 -> F (Clause (BBODY era) 'Transition) (BbodyState era))
-> BbodyState era
-> F (Clause (BBODY era) 'Transition) (BbodyState era)
forall a b. (a -> b) -> a -> b
$
          LedgerState era -> BlocksMade (Crypto era) -> BbodyState era
forall era.
LedgerState era -> BlocksMade (Crypto era) -> BbodyState era
BbodyState
            LedgerState era
ls'
            ( Bool
-> KeyHash 'StakePool (Crypto era)
-> BlocksMade (Crypto era)
-> BlocksMade (Crypto era)
forall crypto.
Bool
-> KeyHash 'StakePool crypto
-> BlocksMade crypto
-> BlocksMade crypto
incrBlocks
                (SlotNo -> UnitInterval -> SlotNo -> Bool
isOverlaySlot SlotNo
firstSlotNo (PParams era -> UnitInterval
forall k (x :: k) r a. HasField x r a => r -> a
getField @"_d" PParams era
pp) SlotNo
slot)
                KeyHash 'StakePool (Crypto era)
hkAsStakePool
                BlocksMade (Crypto era)
b
            )

instance
  forall era ledgers.
  ( Era era,
    BaseM ledgers ~ ShelleyBase,
    ledgers ~ Core.EraRule "LEDGERS" era,
    STS ledgers,
    DSignable (Crypto era) (Hash (Crypto era) EraIndependentTxBody),
    Era era
  ) =>
  Embed ledgers (BBODY era)
  where
  wrapFailed :: PredicateFailure ledgers -> PredicateFailure (BBODY era)
wrapFailed = PredicateFailure ledgers -> PredicateFailure (BBODY era)
forall era.
PredicateFailure (EraRule "LEDGERS" era)
-> BbodyPredicateFailure era
LedgersFailure
  wrapEvent :: Event ledgers -> Event (BBODY era)
wrapEvent = Event ledgers -> Event (BBODY era)
forall era. Event (EraRule "LEDGERS" era) -> BbodyEvent era
LedgersEvent