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

module Shelley.Spec.Ledger.STS.Bbody
  ( BBODY,
    BbodyState (..),
    BbodyEnv (..),
    BbodyPredicateFailure (..),
    PredicateFailure,
    State,
  )
where

import Cardano.Ledger.Era (Era (Crypto))
import Cardano.Ledger.Shelley (ShelleyBased)
import Control.Monad.Trans.Reader (asks)
import Control.State.Transition
  ( Embed (..),
    STS (..),
    TRC (..),
    TransitionRule,
    judgmentContext,
    liftSTS,
    trans,
    (?!),
  )
import qualified Data.Sequence.Strict as StrictSeq
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))
import Shelley.Spec.Ledger.BaseTypes (ShelleyBase, epochInfo)
import Shelley.Spec.Ledger.BlockChain
  ( BHBody (..),
    BHeader (..),
    Block (..),
    HashBBody,
    TxSeq (..),
    bBodySize,
    bbHash,
    hBbsize,
    incrBlocks,
    issuerIDfromBHBody,
  )
import Shelley.Spec.Ledger.EpochBoundary (BlocksMade)
import Shelley.Spec.Ledger.Keys (DSignable, Hash, coerceKeyRole)
import Shelley.Spec.Ledger.LedgerState
  ( AccountState,
    LedgerState,
  )
import Shelley.Spec.Ledger.OverlaySchedule (isOverlaySlot)
import Shelley.Spec.Ledger.PParams (PParams, PParams' (..))
import Shelley.Spec.Ledger.STS.Ledgers (LEDGERS, LedgersEnv (..))
import Shelley.Spec.Ledger.Slot (epochInfoEpoch, epochInfoFirst)
import Shelley.Spec.Ledger.TxBody (EraIndependentTxBody)

data BBODY era

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

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

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

data BbodyPredicateFailure era
  = WrongBlockBodySizeBBODY
      !Int -- Actual Body Size
      !Int -- Claimed Body Size in Header
  | InvalidBodyHashBBODY
      !(HashBBody (Crypto era)) -- Actual Hash
      !(HashBBody (Crypto era)) -- Claimed Hash
  | LedgersFailure (PredicateFailure (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)

deriving stock instance
  ( ShelleyBased era,
    Show (PredicateFailure (LEDGERS era))
  ) =>
  Show (BbodyPredicateFailure era)

deriving stock instance
  ( ShelleyBased era,
    Eq (PredicateFailure (LEDGERS era))
  ) =>
  Eq (BbodyPredicateFailure era)

instance
  ( ShelleyBased era,
    NoThunks (PredicateFailure (LEDGERS era))
  ) =>
  NoThunks (BbodyPredicateFailure era)

instance
  ( Era era,
    ShelleyBased era,
    DSignable (Crypto era) (Hash (Crypto era) EraIndependentTxBody),
    Embed (LEDGERS era) (BBODY era)
  ) =>
  STS (BBODY era)
  where
  type
    State (BBODY era) =
      BbodyState era

  type
    Signal (BBODY era) =
      Block era

  type Environment (BBODY era) = BbodyEnv era

  type BaseM (BBODY era) = ShelleyBase

  type PredicateFailure (BBODY era) = BbodyPredicateFailure era

  initialRules :: [InitialRule (BBODY era)]
initialRules = []
  transitionRules :: [TransitionRule (BBODY era)]
transitionRules = [TransitionRule (BBODY era)
forall era.
(ShelleyBased era, Embed (LEDGERS era) (BBODY era),
 STS (BBODY era)) =>
TransitionRule (BBODY era)
bbodyTransition]

bbodyTransition ::
  forall era.
  ( ShelleyBased era,
    Embed (LEDGERS era) (BBODY era),
    STS (BBODY era)
  ) =>
  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,
               Block (BHeader bhb _) txsSeq
               )
           ) -> do
        let TxSeq StrictSeq (Tx era)
txs = TxSeq era
txsSeq
            actualBodySize :: Int
actualBodySize = TxSeq era -> Int
forall era. Era era => TxSeq era -> Int
bBodySize TxSeq era
txsSeq
            actualBodyHash :: HashBBody (Crypto era)
actualBodyHash = TxSeq era -> HashBBody (Crypto era)
forall era. Era era => TxSeq era -> HashBBody (Crypto era)
bbHash 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 (BHBody (Crypto era) -> Natural
forall era. BHBody era -> Natural
hBbsize BHBody (Crypto era)
bhb)
          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
$ BHBody (Crypto era) -> Natural
forall era. BHBody era -> Natural
hBbsize BHBody (Crypto era)
bhb)

        HashBBody (Crypto era)
actualBodyHash HashBBody (Crypto era) -> HashBBody (Crypto era) -> Bool
forall a. Eq a => a -> a -> Bool
== BHBody (Crypto era) -> HashBBody (Crypto era)
forall crypto. BHBody crypto -> HashBBody crypto
bhash BHBody (Crypto era)
bhb Bool
-> PredicateFailure (BBODY era) -> Rule (BBODY era) 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! HashBBody (Crypto era)
-> HashBBody (Crypto era) -> BbodyPredicateFailure era
forall era.
HashBBody (Crypto era)
-> HashBBody (Crypto era) -> BbodyPredicateFailure era
InvalidBodyHashBBODY HashBBody (Crypto era)
actualBodyHash (BHBody (Crypto era) -> HashBBody (Crypto era)
forall crypto. BHBody crypto -> HashBBody crypto
bhash BHBody (Crypto era)
bhb)

        LedgerState era
ls' <-
          forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (LEDGERS era) super =>
RuleContext rtype (LEDGERS era)
-> Rule super rtype (State (LEDGERS era))
trans @(LEDGERS era) (RuleContext 'Transition (LEDGERS era)
 -> Rule (BBODY era) 'Transition (State (LEDGERS era)))
-> RuleContext 'Transition (LEDGERS era)
-> Rule (BBODY era) 'Transition (State (LEDGERS era))
forall a b. (a -> b) -> a -> b
$
            (Environment (LEDGERS era), State (LEDGERS era),
 Signal (LEDGERS era))
-> TRC (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 (BHBody (Crypto era) -> SlotNo
forall crypto. BHBody crypto -> SlotNo
bheaderSlotNo BHBody (Crypto era)
bhb) PParams era
pp AccountState
account, State (LEDGERS era)
LedgerState era
ls, StrictSeq (Tx era) -> Seq (Tx era)
forall a. StrictSeq a -> Seq a
StrictSeq.getSeq 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))
-> (BHBody (Crypto era) -> KeyHash 'BlockIssuer (Crypto era))
-> BHBody (Crypto era)
-> KeyHash 'StakePool (Crypto era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BHBody (Crypto era) -> KeyHash 'BlockIssuer (Crypto era)
forall crypto.
Crypto crypto =>
BHBody crypto -> KeyHash 'BlockIssuer crypto
issuerIDfromBHBody (BHBody (Crypto era) -> KeyHash 'StakePool (Crypto era))
-> BHBody (Crypto era) -> KeyHash 'StakePool (Crypto era)
forall a b. (a -> b) -> a -> b
$ BHBody (Crypto era)
bhb
            slot :: SlotNo
slot = BHBody (Crypto era) -> SlotNo
forall crypto. BHBody crypto -> SlotNo
bheaderSlotNo BHBody (Crypto era)
bhb
        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
epochInfo
          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 era -> BbodyState era
forall era. LedgerState era -> BlocksMade era -> BbodyState era
BbodyState
            LedgerState era
ls'
            ( Bool
-> KeyHash 'StakePool (Crypto era)
-> BlocksMade era
-> BlocksMade era
forall era.
Bool
-> KeyHash 'StakePool (Crypto era)
-> BlocksMade era
-> BlocksMade era
incrBlocks
                (SlotNo -> UnitInterval -> SlotNo -> Bool
isOverlaySlot SlotNo
firstSlotNo (PParams era -> HKD Identity UnitInterval
forall (f :: * -> *) era. PParams' f era -> HKD f UnitInterval
_d PParams era
pp) SlotNo
slot)
                KeyHash 'StakePool (Crypto era)
hkAsStakePool
                BlocksMade era
b
            )

instance
  ( Era era,
    STS (LEDGERS era),
    DSignable (Crypto era) (Hash (Crypto era) EraIndependentTxBody),
    ShelleyBased era
  ) =>
  Embed (LEDGERS era) (BBODY era)
  where
  wrapFailed :: PredicateFailure (LEDGERS era) -> PredicateFailure (BBODY era)
wrapFailed = PredicateFailure (LEDGERS era) -> PredicateFailure (BBODY era)
forall era.
PredicateFailure (LEDGERS era) -> BbodyPredicateFailure era
LedgersFailure