{-# 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
!Int
| InvalidBodyHashBBODY
!(HashBBody (Crypto era))
!(HashBBody (Crypto era))
| LedgersFailure (PredicateFailure (LEDGERS era))
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)
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