{-# 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 (DSignable, Hash, 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 (EraCrypto era))

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 (EraCrypto era) 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 c) = ShelleyBbodyPredFailure (ShelleyEra c)

instance InjectRuleFailure "BBODY" ShelleyBbodyPredFailure (ShelleyEra c)

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

instance InjectRuleFailure "BBODY" ShelleyLedgerPredFailure (ShelleyEra c) where
  injectFailure :: ShelleyLedgerPredFailure (ShelleyEra c)
-> EraRuleFailure "BBODY" (ShelleyEra c)
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 c) where
  injectFailure :: ShelleyUtxowPredFailure (ShelleyEra c)
-> EraRuleFailure "BBODY" (ShelleyEra c)
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 c) where
  injectFailure :: ShelleyUtxoPredFailure (ShelleyEra c)
-> EraRuleFailure "BBODY" (ShelleyEra c)
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 c) where
  injectFailure :: ShelleyPpupPredFailure (ShelleyEra c)
-> EraRuleFailure "BBODY" (ShelleyEra c)
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 c) where
  injectFailure :: ShelleyDelegsPredFailure (ShelleyEra c)
-> EraRuleFailure "BBODY" (ShelleyEra c)
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 c) where
  injectFailure :: ShelleyDelplPredFailure (ShelleyEra c)
-> EraRuleFailure "BBODY" (ShelleyEra c)
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 c) where
  injectFailure :: ShelleyPoolPredFailure (ShelleyEra c)
-> EraRuleFailure "BBODY" (ShelleyEra c)
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 c) where
  injectFailure :: ShelleyDelegPredFailure (ShelleyEra c)
-> EraRuleFailure "BBODY" (ShelleyEra c)
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
  , DSignable (EraCrypto era) (Hash (EraCrypto era) EraIndependentTxBody)
  , 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 (EraCrypto era)) 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 (EraCrypto era)
b
              , UnserialisedBlock BHeaderView (EraCrypto era)
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 (EraCrypto era)) EraIndependentBlockBody
actualBodyHash = forall era.
EraSegWits era =>
TxSeq era -> Hash (HASH (EraCrypto era)) EraIndependentBlockBody
hashTxSeq TxSeq era
txsSeq

        Int
actualBodySize
          forall a. Eq a => a -> a -> Bool
== forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall c. BHeaderView c -> Word32
bhviewBSize BHeaderView (EraCrypto era)
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
$ forall c. BHeaderView c -> Word32
bhviewBSize BHeaderView (EraCrypto era)
bhview
                  }
              )

        Hash (HASH (EraCrypto era)) EraIndependentBlockBody
actualBodyHash
          forall a. Eq a => a -> a -> Bool
== forall c. BHeaderView c -> Hash c EraIndependentBlockBody
bhviewBHash BHeaderView (EraCrypto era)
bhview
            forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! forall era.
Mismatch 'RelEQ (Hash (EraCrypto era) EraIndependentBlockBody)
-> ShelleyBbodyPredFailure era
InvalidBodyHashBBODY
              ( Mismatch
                  { mismatchSupplied :: Hash (HASH (EraCrypto era)) EraIndependentBlockBody
mismatchSupplied = Hash (HASH (EraCrypto era)) EraIndependentBlockBody
actualBodyHash
                  , mismatchExpected :: Hash (HASH (EraCrypto era)) EraIndependentBlockBody
mismatchExpected = forall c. BHeaderView c -> Hash c EraIndependentBlockBody
bhviewBHash BHeaderView (EraCrypto era)
bhview
                  }
              )

        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 -> PParams era -> AccountState -> ShelleyLedgersEnv era
LedgersEnv (forall c. BHeaderView c -> SlotNo
bhviewSlot BHeaderView (EraCrypto era)
bhview) PParams era
pp AccountState
account, State (EraRule "LEDGERS" era)
ls, 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 (EraCrypto era)
hkAsStakePool = forall (a :: KeyRole -> * -> *) (r :: KeyRole) c (r' :: KeyRole).
HasKeyRole a =>
a r c -> a r' c
coerceKeyRole forall a b. (a -> b) -> a -> b
$ forall c. BHeaderView c -> KeyHash 'BlockIssuer c
bhviewID BHeaderView (EraCrypto era)
bhview
            slot :: SlotNo
slot = forall c. BHeaderView c -> SlotNo
bhviewSlot BHeaderView (EraCrypto era)
bhview
        SlotNo
firstSlotNo <- 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
          EpochNo
e <- HasCallStack => EpochInfo Identity -> SlotNo -> ShelleyBase EpochNo
epochInfoEpoch EpochInfo Identity
ei SlotNo
slot
          HasCallStack => EpochInfo Identity -> EpochNo -> ShelleyBase SlotNo
epochInfoFirst EpochInfo Identity
ei EpochNo
e
        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 (EraCrypto era) -> ShelleyBbodyState era
BbodyState State (EraRule "LEDGERS" era)
ls' (forall c.
Bool -> KeyHash 'StakePool c -> BlocksMade c -> BlocksMade c
incrBlocks Bool
isOverlay KeyHash 'StakePool (EraCrypto era)
hkAsStakePool BlocksMade (EraCrypto era)
b)

instance
  forall era ledgers.
  ( Era era
  , BaseM ledgers ~ ShelleyBase
  , ledgers ~ EraRule "LEDGERS" era
  , STS ledgers
  , DSignable (EraCrypto era) (Hash (EraCrypto era) EraIndependentTxBody)
  , 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