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

module Shelley.Spec.Ledger.STS.Chain
  ( CHAIN,
    ChainState (..),
    ChainPredicateFailure (..),
    PredicateFailure,
    initialShelleyState,
    totalAda,
    totalAdaES,
    totalAdaPots,
    ChainChecksData (..),
    pparamsToChainChecksData,
    chainChecks,
  )
where

import qualified Cardano.Crypto.VRF as VRF
import Cardano.Ledger.Crypto (VRF)
import Cardano.Ledger.Era (Crypto, Era)
import Cardano.Ledger.Shelley (ShelleyBased)
import qualified Cardano.Ledger.Val as Val
import Cardano.Slotting.Slot (WithOrigin (..))
import Control.DeepSeq (NFData)
import Control.Monad (unless)
import Control.Monad.Except (MonadError, throwError)
import Control.Monad.Trans.Reader (asks)
import Control.State.Transition
  ( Embed (..),
    STS (..),
    TRC (..),
    TransitionRule,
    failBecause,
    judgmentContext,
    liftSTS,
    trans,
  )
import Data.Foldable (fold)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Word (Word64)
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))
import Numeric.Natural (Natural)
import Shelley.Spec.Ledger.BaseTypes
  ( Globals (..),
    Nonce (..),
    Seed (..),
    ShelleyBase,
    StrictMaybe (..),
  )
import Shelley.Spec.Ledger.BlockChain
  ( BHBody,
    BHeader,
    Block (..),
    LastAppliedBlock (..),
    bHeaderSize,
    bhHash,
    bhbody,
    bheaderBlockNo,
    bheaderSlotNo,
    hBbsize,
    lastAppliedHash,
    prevHashToNonce,
  )
import Shelley.Spec.Ledger.Coin (Coin (..))
import Shelley.Spec.Ledger.Delegation.Certificates (PoolDistr (..))
import Shelley.Spec.Ledger.EpochBoundary (BlocksMade (..), emptySnapShots)
import Shelley.Spec.Ledger.Keys
  ( DSignable,
    GenDelegPair (..),
    GenDelegs (..),
    Hash,
    KESignable,
    KeyHash,
    KeyRole (..),
    coerceKeyRole,
  )
import Shelley.Spec.Ledger.LedgerState
  ( AccountState (..),
    DPState (..),
    DState (..),
    EpochState (..),
    LedgerState (..),
    NewEpochState (..),
    PState (..),
    UTxOState (..),
    emptyDState,
    emptyPPUPState,
    emptyPState,
    updateNES,
    _genDelegs,
  )
import Shelley.Spec.Ledger.OCert (OCertSignable)
import Shelley.Spec.Ledger.PParams
  ( PParams,
    PParams' (..),
    ProtVer (..),
  )
import Shelley.Spec.Ledger.Rewards (emptyNonMyopic)
import Shelley.Spec.Ledger.STS.Bbody (BBODY, BbodyEnv (..), BbodyState (..))
import Shelley.Spec.Ledger.STS.Prtcl
  ( PRTCL,
    PrtclEnv (..),
    PrtclState (..),
    PrtlSeqFailure,
    prtlSeqChecks,
  )
import Shelley.Spec.Ledger.STS.Tick (TICK)
import Shelley.Spec.Ledger.STS.Tickn
import Shelley.Spec.Ledger.Slot (EpochNo)
import Shelley.Spec.Ledger.TxBody (EraIndependentTxBody)
import Shelley.Spec.Ledger.UTxO (UTxO (..), balance)

data CHAIN era

data ChainState era = ChainState
  { ChainState era -> NewEpochState era
chainNes :: NewEpochState era,
    ChainState era -> Map (KeyHash 'BlockIssuer (Crypto era)) Word64
chainOCertIssue :: Map.Map (KeyHash 'BlockIssuer (Crypto era)) Word64,
    ChainState era -> Nonce
chainEpochNonce :: Nonce,
    ChainState era -> Nonce
chainEvolvingNonce :: Nonce,
    ChainState era -> Nonce
chainCandidateNonce :: Nonce,
    ChainState era -> Nonce
chainPrevEpochNonce :: Nonce,
    ChainState era -> WithOrigin (LastAppliedBlock (Crypto era))
chainLastAppliedBlock :: WithOrigin (LastAppliedBlock (Crypto era))
  }
  deriving ((forall x. ChainState era -> Rep (ChainState era) x)
-> (forall x. Rep (ChainState era) x -> ChainState era)
-> Generic (ChainState era)
forall x. Rep (ChainState era) x -> ChainState era
forall x. ChainState era -> Rep (ChainState era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x. Rep (ChainState era) x -> ChainState era
forall era x. ChainState era -> Rep (ChainState era) x
$cto :: forall era x. Rep (ChainState era) x -> ChainState era
$cfrom :: forall era x. ChainState era -> Rep (ChainState era) x
Generic)

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

deriving stock instance
  ShelleyBased era =>
  Eq (ChainState era)

instance (Era era) => NFData (ChainState era)

data ChainPredicateFailure era
  = HeaderSizeTooLargeCHAIN
      !Natural -- Header Size
      !Natural -- Max Header Size
  | BlockSizeTooLargeCHAIN
      !Natural -- Block Size
      !Natural -- Max Block Size
  | ObsoleteNodeCHAIN
      !Natural -- protocol version used
      !Natural -- max protocol version
  | BbodyFailure !(PredicateFailure (BBODY era)) -- Subtransition Failures
  | TickFailure !(PredicateFailure (TICK era)) -- Subtransition Failures
  | TicknFailure !(PredicateFailure TICKN) -- Subtransition Failures
  | PrtclFailure !(PredicateFailure (PRTCL (Crypto era))) -- Subtransition Failures
  | PrtclSeqFailure !(PrtlSeqFailure (Crypto era)) -- Subtransition Failures
  deriving ((forall x.
 ChainPredicateFailure era -> Rep (ChainPredicateFailure era) x)
-> (forall x.
    Rep (ChainPredicateFailure era) x -> ChainPredicateFailure era)
-> Generic (ChainPredicateFailure era)
forall x.
Rep (ChainPredicateFailure era) x -> ChainPredicateFailure era
forall x.
ChainPredicateFailure era -> Rep (ChainPredicateFailure era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ChainPredicateFailure era) x -> ChainPredicateFailure era
forall era x.
ChainPredicateFailure era -> Rep (ChainPredicateFailure era) x
$cto :: forall era x.
Rep (ChainPredicateFailure era) x -> ChainPredicateFailure era
$cfrom :: forall era x.
ChainPredicateFailure era -> Rep (ChainPredicateFailure era) x
Generic)

deriving stock instance
  ( ShelleyBased era,
    Show (PredicateFailure (BBODY era))
  ) =>
  Show (ChainPredicateFailure era)

deriving stock instance
  ( ShelleyBased era,
    Eq (PredicateFailure (BBODY era))
  ) =>
  Eq (ChainPredicateFailure era)

instance
  ( ShelleyBased era,
    NoThunks (PredicateFailure (BBODY era))
  ) =>
  NoThunks (ChainPredicateFailure era)

-- | Creates a valid initial chain state
initialShelleyState ::
  WithOrigin (LastAppliedBlock (Crypto era)) ->
  EpochNo ->
  UTxO era ->
  Coin ->
  Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era)) ->
  PParams era ->
  Nonce ->
  ChainState era
initialShelleyState :: WithOrigin (LastAppliedBlock (Crypto era))
-> EpochNo
-> UTxO era
-> Coin
-> Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
-> PParams era
-> Nonce
-> ChainState era
initialShelleyState WithOrigin (LastAppliedBlock (Crypto era))
lab EpochNo
e UTxO era
utxo Coin
reserves Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
genDelegs PParams era
pp Nonce
initNonce =
  NewEpochState era
-> Map (KeyHash 'BlockIssuer (Crypto era)) Word64
-> Nonce
-> Nonce
-> Nonce
-> Nonce
-> WithOrigin (LastAppliedBlock (Crypto era))
-> ChainState era
forall era.
NewEpochState era
-> Map (KeyHash 'BlockIssuer (Crypto era)) Word64
-> Nonce
-> Nonce
-> Nonce
-> Nonce
-> WithOrigin (LastAppliedBlock (Crypto era))
-> ChainState era
ChainState
    ( EpochNo
-> BlocksMade era
-> BlocksMade era
-> EpochState era
-> StrictMaybe (RewardUpdate era)
-> PoolDistr (Crypto era)
-> NewEpochState era
forall era.
EpochNo
-> BlocksMade era
-> BlocksMade era
-> EpochState era
-> StrictMaybe (RewardUpdate era)
-> PoolDistr (Crypto era)
-> NewEpochState era
NewEpochState
        EpochNo
e
        (Map (KeyHash 'StakePool (Crypto era)) Natural -> BlocksMade era
forall era.
Map (KeyHash 'StakePool (Crypto era)) Natural -> BlocksMade era
BlocksMade Map (KeyHash 'StakePool (Crypto era)) Natural
forall k a. Map k a
Map.empty)
        (Map (KeyHash 'StakePool (Crypto era)) Natural -> BlocksMade era
forall era.
Map (KeyHash 'StakePool (Crypto era)) Natural -> BlocksMade era
BlocksMade Map (KeyHash 'StakePool (Crypto era)) Natural
forall k a. Map k a
Map.empty)
        ( AccountState
-> SnapShots era
-> LedgerState era
-> PParams era
-> PParams era
-> NonMyopic era
-> EpochState era
forall era.
AccountState
-> SnapShots era
-> LedgerState era
-> PParams era
-> PParams era
-> NonMyopic era
-> EpochState era
EpochState
            (Coin -> Coin -> AccountState
AccountState (Integer -> Coin
Coin Integer
0) Coin
reserves)
            SnapShots era
forall era. SnapShots era
emptySnapShots
            ( UTxOState era -> DPState era -> LedgerState era
forall era. UTxOState era -> DPState era -> LedgerState era
LedgerState
                ( UTxO era -> Coin -> Coin -> PPUPState era -> UTxOState era
forall era.
UTxO era -> Coin -> Coin -> PPUPState era -> UTxOState era
UTxOState
                    UTxO era
utxo
                    (Integer -> Coin
Coin Integer
0)
                    (Integer -> Coin
Coin Integer
0)
                    PPUPState era
forall era. PPUPState era
emptyPPUPState
                )
                (DState era -> PState era -> DPState era
forall era. DState era -> PState era -> DPState era
DPState (DState era
forall era. DState era
emptyDState {_genDelegs :: GenDelegs (Crypto era)
_genDelegs = (Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
-> GenDelegs (Crypto era)
forall crypto.
Map (KeyHash 'Genesis crypto) (GenDelegPair crypto)
-> GenDelegs crypto
GenDelegs Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
genDelegs)}) PState era
forall era. PState era
emptyPState)
            )
            PParams era
pp
            PParams era
pp
            NonMyopic era
forall era. NonMyopic era
emptyNonMyopic
        )
        StrictMaybe (RewardUpdate era)
forall a. StrictMaybe a
SNothing
        (Map
  (KeyHash 'StakePool (Crypto era))
  (IndividualPoolStake (Crypto era))
-> PoolDistr (Crypto era)
forall crypto.
Map (KeyHash 'StakePool crypto) (IndividualPoolStake crypto)
-> PoolDistr crypto
PoolDistr Map
  (KeyHash 'StakePool (Crypto era))
  (IndividualPoolStake (Crypto era))
forall k a. Map k a
Map.empty)
    )
    Map (KeyHash 'BlockIssuer (Crypto era)) Word64
cs
    Nonce
initNonce
    Nonce
initNonce
    Nonce
initNonce
    Nonce
NeutralNonce
    WithOrigin (LastAppliedBlock (Crypto era))
lab
  where
    cs :: Map (KeyHash 'BlockIssuer (Crypto era)) Word64
cs = [(KeyHash 'BlockIssuer (Crypto era), Word64)]
-> Map (KeyHash 'BlockIssuer (Crypto era)) Word64
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ((GenDelegPair (Crypto era)
 -> (KeyHash 'BlockIssuer (Crypto era), Word64))
-> [GenDelegPair (Crypto era)]
-> [(KeyHash 'BlockIssuer (Crypto era), Word64)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(GenDelegPair KeyHash 'GenesisDelegate (Crypto era)
hk Hash (Crypto era) (VerKeyVRF (Crypto era))
_) -> (KeyHash 'GenesisDelegate (Crypto era)
-> KeyHash 'BlockIssuer (Crypto era)
forall (a :: KeyRole -> * -> *) (r :: KeyRole) crypto
       (r' :: KeyRole).
HasKeyRole a =>
a r crypto -> a r' crypto
coerceKeyRole KeyHash 'GenesisDelegate (Crypto era)
hk, Word64
0)) (Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
-> [GenDelegPair (Crypto era)]
forall k a. Map k a -> [a]
Map.elems Map (KeyHash 'Genesis (Crypto era)) (GenDelegPair (Crypto era))
genDelegs))

instance
  ( Era era,
    c ~ Crypto era,
    ShelleyBased era,
    Embed (BBODY era) (CHAIN era),
    Embed TICKN (CHAIN era),
    Embed (TICK era) (CHAIN era),
    Embed (PRTCL (Crypto era)) (CHAIN era),
    DSignable c (OCertSignable c),
    DSignable c (Hash c EraIndependentTxBody),
    KESignable c (BHBody c),
    VRF.Signable (VRF c) Seed
  ) =>
  STS (CHAIN era)
  where
  type
    State (CHAIN era) =
      ChainState era

  type
    Signal (CHAIN era) =
      Block era

  type Environment (CHAIN era) = ()
  type BaseM (CHAIN era) = ShelleyBase

  type PredicateFailure (CHAIN era) = ChainPredicateFailure era

  initialRules :: [InitialRule (CHAIN era)]
initialRules = []
  transitionRules :: [TransitionRule (CHAIN era)]
transitionRules = [TransitionRule (CHAIN era)
forall era.
(ShelleyBased era, STS (CHAIN era), Embed (BBODY era) (CHAIN era),
 Embed TICKN (CHAIN era), Embed (TICK era) (CHAIN era),
 Embed (PRTCL (Crypto era)) (CHAIN era)) =>
TransitionRule (CHAIN era)
chainTransition]

data ChainChecksData = ChainChecksData
  { ChainChecksData -> Natural
ccMaxBHSize :: Natural,
    ChainChecksData -> Natural
ccMaxBBSize :: Natural,
    ChainChecksData -> ProtVer
ccProtocolVersion :: ProtVer
  }
  deriving (Int -> ChainChecksData -> ShowS
[ChainChecksData] -> ShowS
ChainChecksData -> String
(Int -> ChainChecksData -> ShowS)
-> (ChainChecksData -> String)
-> ([ChainChecksData] -> ShowS)
-> Show ChainChecksData
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ChainChecksData] -> ShowS
$cshowList :: [ChainChecksData] -> ShowS
show :: ChainChecksData -> String
$cshow :: ChainChecksData -> String
showsPrec :: Int -> ChainChecksData -> ShowS
$cshowsPrec :: Int -> ChainChecksData -> ShowS
Show, ChainChecksData -> ChainChecksData -> Bool
(ChainChecksData -> ChainChecksData -> Bool)
-> (ChainChecksData -> ChainChecksData -> Bool)
-> Eq ChainChecksData
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ChainChecksData -> ChainChecksData -> Bool
$c/= :: ChainChecksData -> ChainChecksData -> Bool
== :: ChainChecksData -> ChainChecksData -> Bool
$c== :: ChainChecksData -> ChainChecksData -> Bool
Eq, (forall x. ChainChecksData -> Rep ChainChecksData x)
-> (forall x. Rep ChainChecksData x -> ChainChecksData)
-> Generic ChainChecksData
forall x. Rep ChainChecksData x -> ChainChecksData
forall x. ChainChecksData -> Rep ChainChecksData x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ChainChecksData x -> ChainChecksData
$cfrom :: forall x. ChainChecksData -> Rep ChainChecksData x
Generic, Context -> ChainChecksData -> IO (Maybe ThunkInfo)
Proxy ChainChecksData -> String
(Context -> ChainChecksData -> IO (Maybe ThunkInfo))
-> (Context -> ChainChecksData -> IO (Maybe ThunkInfo))
-> (Proxy ChainChecksData -> String)
-> NoThunks ChainChecksData
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
showTypeOf :: Proxy ChainChecksData -> String
$cshowTypeOf :: Proxy ChainChecksData -> String
wNoThunks :: Context -> ChainChecksData -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> ChainChecksData -> IO (Maybe ThunkInfo)
noThunks :: Context -> ChainChecksData -> IO (Maybe ThunkInfo)
$cnoThunks :: Context -> ChainChecksData -> IO (Maybe ThunkInfo)
NoThunks)

pparamsToChainChecksData :: PParams era -> ChainChecksData
pparamsToChainChecksData :: PParams era -> ChainChecksData
pparamsToChainChecksData PParams era
pp =
  ChainChecksData :: Natural -> Natural -> ProtVer -> ChainChecksData
ChainChecksData
    { ccMaxBHSize :: Natural
ccMaxBHSize = PParams era -> HKD Identity Natural
forall (f :: * -> *) era. PParams' f era -> HKD f Natural
_maxBHSize PParams era
pp,
      ccMaxBBSize :: Natural
ccMaxBBSize = PParams era -> HKD Identity Natural
forall (f :: * -> *) era. PParams' f era -> HKD f Natural
_maxBBSize PParams era
pp,
      ccProtocolVersion :: ProtVer
ccProtocolVersion = PParams era -> HKD Identity ProtVer
forall (f :: * -> *) era. PParams' f era -> HKD f ProtVer
_protocolVersion PParams era
pp
    }

chainChecks ::
  ( Era era,
    MonadError (PredicateFailure (CHAIN era)) m
  ) =>
  Natural ->
  ChainChecksData ->
  BHeader (Crypto era) ->
  m ()
chainChecks :: Natural -> ChainChecksData -> BHeader (Crypto era) -> m ()
chainChecks Natural
maxpv ChainChecksData
ccd BHeader (Crypto era)
bh = do
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Natural
m Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= Natural
maxpv) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ ChainPredicateFailure era -> m ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Natural -> Natural -> ChainPredicateFailure era
forall era. Natural -> Natural -> ChainPredicateFailure era
ObsoleteNodeCHAIN Natural
m Natural
maxpv)
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (BHeader (Crypto era) -> Int
forall crypto. Crypto crypto => BHeader crypto -> Int
bHeaderSize BHeader (Crypto era)
bh) Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= ChainChecksData -> Natural
ccMaxBHSize ChainChecksData
ccd) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
    ChainPredicateFailure era -> m ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (ChainPredicateFailure era -> m ())
-> ChainPredicateFailure era -> m ()
forall a b. (a -> b) -> a -> b
$
      Natural -> Natural -> ChainPredicateFailure era
forall era. Natural -> Natural -> ChainPredicateFailure era
HeaderSizeTooLargeCHAIN (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Natural) -> Int -> Natural
forall a b. (a -> b) -> a -> b
$ BHeader (Crypto era) -> Int
forall crypto. Crypto crypto => BHeader crypto -> Int
bHeaderSize BHeader (Crypto era)
bh) (ChainChecksData -> Natural
ccMaxBHSize ChainChecksData
ccd)
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (BHBody (Crypto era) -> Natural
forall era. BHBody era -> Natural
hBbsize (BHeader (Crypto era) -> BHBody (Crypto era)
forall crypto. Crypto crypto => BHeader crypto -> BHBody crypto
bhbody BHeader (Crypto era)
bh) Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= ChainChecksData -> Natural
ccMaxBBSize ChainChecksData
ccd) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
    ChainPredicateFailure era -> m ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (ChainPredicateFailure era -> m ())
-> ChainPredicateFailure era -> m ()
forall a b. (a -> b) -> a -> b
$
      Natural -> Natural -> ChainPredicateFailure era
forall era. Natural -> Natural -> ChainPredicateFailure era
BlockSizeTooLargeCHAIN (BHBody (Crypto era) -> Natural
forall era. BHBody era -> Natural
hBbsize (BHeader (Crypto era) -> BHBody (Crypto era)
forall crypto. Crypto crypto => BHeader crypto -> BHBody crypto
bhbody BHeader (Crypto era)
bh)) (ChainChecksData -> Natural
ccMaxBBSize ChainChecksData
ccd)
  where
    (ProtVer Natural
m Natural
_) = ChainChecksData -> ProtVer
ccProtocolVersion ChainChecksData
ccd

chainTransition ::
  forall era.
  ( ShelleyBased era,
    STS (CHAIN era),
    Embed (BBODY era) (CHAIN era),
    Embed TICKN (CHAIN era),
    Embed (TICK era) (CHAIN era),
    Embed (PRTCL (Crypto era)) (CHAIN era)
  ) =>
  TransitionRule (CHAIN era)
chainTransition :: TransitionRule (CHAIN era)
chainTransition =
  F (Clause (CHAIN era) 'Transition) (TRC (CHAIN era))
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
    F (Clause (CHAIN era) 'Transition) (TRC (CHAIN era))
-> (TRC (CHAIN era)
    -> F (Clause (CHAIN era) 'Transition) (ChainState era))
-> F (Clause (CHAIN era) 'Transition) (ChainState era)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \( TRC
             ( Environment (CHAIN era)
_,
               ChainState
                 nes
                 cs
                 eta0
                 etaV
                 etaC
                 etaH
                 lab,
               block :: Signal (CHAIN era)
block@(Block bh _)
               )
           ) -> do
        case WithOrigin (LastAppliedBlock (Crypto era))
-> BHeader (Crypto era) -> Either (PrtlSeqFailure (Crypto era)) ()
forall crypto (m :: * -> *).
(MonadError (PrtlSeqFailure crypto) m, Crypto crypto) =>
WithOrigin (LastAppliedBlock crypto) -> BHeader crypto -> m ()
prtlSeqChecks WithOrigin (LastAppliedBlock (Crypto era))
lab BHeader (Crypto era)
bh of
          Right () -> () -> F (Clause (CHAIN era) 'Transition) ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          Left PrtlSeqFailure (Crypto era)
e -> PredicateFailure (CHAIN era)
-> F (Clause (CHAIN era) 'Transition) ()
forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause (PredicateFailure (CHAIN era)
 -> F (Clause (CHAIN era) 'Transition) ())
-> PredicateFailure (CHAIN era)
-> F (Clause (CHAIN era) 'Transition) ()
forall a b. (a -> b) -> a -> b
$ PrtlSeqFailure (Crypto era) -> ChainPredicateFailure era
forall era.
PrtlSeqFailure (Crypto era) -> ChainPredicateFailure era
PrtclSeqFailure PrtlSeqFailure (Crypto era)
e

        let NewEpochState EpochNo
_ BlocksMade era
_ BlocksMade era
_ (EpochState AccountState
_ SnapShots era
_ LedgerState era
_ PParams era
_ PParams era
pp NonMyopic era
_) StrictMaybe (RewardUpdate era)
_ PoolDistr (Crypto era)
_ = NewEpochState era
nes
            chainChecksData :: ChainChecksData
chainChecksData = PParams era -> ChainChecksData
forall era. PParams era -> ChainChecksData
pparamsToChainChecksData PParams era
pp

        Natural
maxpv <- BaseM (CHAIN era) Natural -> Rule (CHAIN era) 'Transition Natural
forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS (BaseM (CHAIN era) Natural -> Rule (CHAIN era) 'Transition Natural)
-> BaseM (CHAIN era) Natural
-> Rule (CHAIN era) 'Transition Natural
forall a b. (a -> b) -> a -> b
$ (Globals -> Natural) -> ReaderT Globals Identity Natural
forall (m :: * -> *) r a. Monad m => (r -> a) -> ReaderT r m a
asks Globals -> Natural
maxMajorPV
        case Natural
-> ChainChecksData
-> BHeader (Crypto era)
-> Either (ChainPredicateFailure era) ()
forall era (m :: * -> *).
(Era era, MonadError (PredicateFailure (CHAIN era)) m) =>
Natural -> ChainChecksData -> BHeader (Crypto era) -> m ()
chainChecks Natural
maxpv ChainChecksData
chainChecksData BHeader (Crypto era)
bh of
          Right () -> () -> F (Clause (CHAIN era) 'Transition) ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          Left ChainPredicateFailure era
e -> PredicateFailure (CHAIN era)
-> F (Clause (CHAIN era) 'Transition) ()
forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause PredicateFailure (CHAIN era)
ChainPredicateFailure era
e

        let s :: SlotNo
s = BHBody (Crypto era) -> SlotNo
forall crypto. BHBody crypto -> SlotNo
bheaderSlotNo (BHBody (Crypto era) -> SlotNo) -> BHBody (Crypto era) -> SlotNo
forall a b. (a -> b) -> a -> b
$ BHeader (Crypto era) -> BHBody (Crypto era)
forall crypto. Crypto crypto => BHeader crypto -> BHBody crypto
bhbody BHeader (Crypto era)
bh

        NewEpochState era
nes' <-
          forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (TICK era) super =>
RuleContext rtype (TICK era) -> Rule super rtype (State (TICK era))
trans @(TICK era) (RuleContext 'Transition (TICK era)
 -> Rule (CHAIN era) 'Transition (State (TICK era)))
-> RuleContext 'Transition (TICK era)
-> Rule (CHAIN era) 'Transition (State (TICK era))
forall a b. (a -> b) -> a -> b
$ (Environment (TICK era), State (TICK era), Signal (TICK era))
-> TRC (TICK era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC ((), State (TICK era)
NewEpochState era
nes, SlotNo
Signal (TICK era)
s)

        let NewEpochState EpochNo
e1 BlocksMade era
_ BlocksMade era
_ EpochState era
_ StrictMaybe (RewardUpdate era)
_ PoolDistr (Crypto era)
_ = NewEpochState era
nes
            NewEpochState EpochNo
e2 BlocksMade era
_ BlocksMade era
bcur EpochState era
es StrictMaybe (RewardUpdate era)
_ PoolDistr (Crypto era)
_pd = NewEpochState era
nes'
        let EpochState AccountState
account SnapShots era
_ LedgerState era
ls PParams era
_ PParams era
pp' NonMyopic era
_ = EpochState era
es
        let LedgerState UTxOState era
_ (DPState (DState RewardAccounts era
_ Map (Credential 'Staking era) (KeyHash 'StakePool (Crypto era))
_ Bimap Ptr (Credential 'Staking era)
_ Map (FutureGenDeleg (Crypto era)) (GenDelegPair (Crypto era))
_ GenDelegs (Crypto era)
_genDelegs InstantaneousRewards era
_) (PState Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
_ Map (KeyHash 'StakePool (Crypto era)) (PoolParams era)
_ Map (KeyHash 'StakePool (Crypto era)) EpochNo
_)) = LedgerState era
ls

        let ph :: PrevHash (Crypto era)
ph = WithOrigin (LastAppliedBlock (Crypto era)) -> PrevHash (Crypto era)
forall crypto.
WithOrigin (LastAppliedBlock crypto) -> PrevHash crypto
lastAppliedHash WithOrigin (LastAppliedBlock (Crypto era))
lab
            etaPH :: Nonce
etaPH = PrevHash (Crypto era) -> Nonce
forall crypto. PrevHash crypto -> Nonce
prevHashToNonce PrevHash (Crypto era)
ph

        TicknState Nonce
eta0' Nonce
etaH' <-
          forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed TICKN super =>
RuleContext rtype TICKN -> Rule super rtype (State TICKN)
trans @TICKN (RuleContext 'Transition TICKN
 -> Rule (CHAIN era) 'Transition (State TICKN))
-> RuleContext 'Transition TICKN
-> Rule (CHAIN era) 'Transition (State TICKN)
forall a b. (a -> b) -> a -> b
$
            (Environment TICKN, State TICKN, Signal TICKN) -> TRC TICKN
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC
              ( Nonce -> Nonce -> Nonce -> TicknEnv
TicknEnv (PParams era -> HKD Identity Nonce
forall (f :: * -> *) era. PParams' f era -> HKD f Nonce
_extraEntropy PParams era
pp') Nonce
etaC Nonce
etaPH,
                Nonce -> Nonce -> TicknState
TicknState Nonce
eta0 Nonce
etaH,
                (EpochNo
e1 EpochNo -> EpochNo -> Bool
forall a. Eq a => a -> a -> Bool
/= EpochNo
e2)
              )

        PrtclState Map (KeyHash 'BlockIssuer (Crypto era)) Word64
cs' Nonce
etaV' Nonce
etaC' <-
          forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (PRTCL (Crypto era)) super =>
RuleContext rtype (PRTCL (Crypto era))
-> Rule super rtype (State (PRTCL (Crypto era)))
trans @(PRTCL (Crypto era)) (RuleContext 'Transition (PRTCL (Crypto era))
 -> Rule (CHAIN era) 'Transition (State (PRTCL (Crypto era))))
-> RuleContext 'Transition (PRTCL (Crypto era))
-> Rule (CHAIN era) 'Transition (State (PRTCL (Crypto era)))
forall a b. (a -> b) -> a -> b
$
            (Environment (PRTCL (Crypto era)), State (PRTCL (Crypto era)),
 Signal (PRTCL (Crypto era)))
-> TRC (PRTCL (Crypto era))
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC
              ( UnitInterval
-> PoolDistr (Crypto era)
-> GenDelegs (Crypto era)
-> Nonce
-> PrtclEnv (Crypto era)
forall crypto.
UnitInterval
-> PoolDistr crypto -> GenDelegs crypto -> Nonce -> PrtclEnv crypto
PrtclEnv (PParams era -> HKD Identity UnitInterval
forall (f :: * -> *) era. PParams' f era -> HKD f UnitInterval
_d PParams era
pp') PoolDistr (Crypto era)
_pd GenDelegs (Crypto era)
_genDelegs Nonce
eta0',
                Map (KeyHash 'BlockIssuer (Crypto era)) Word64
-> Nonce -> Nonce -> PrtclState (Crypto era)
forall crypto.
Map (KeyHash 'BlockIssuer crypto) Word64
-> Nonce -> Nonce -> PrtclState crypto
PrtclState Map (KeyHash 'BlockIssuer (Crypto era)) Word64
cs Nonce
etaV Nonce
etaC,
                Signal (PRTCL (Crypto era))
BHeader (Crypto era)
bh
              )

        BbodyState LedgerState era
ls' BlocksMade era
bcur' <-
          forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
forall super (rtype :: RuleType).
Embed (BBODY era) super =>
RuleContext rtype (BBODY era)
-> Rule super rtype (State (BBODY era))
trans @(BBODY era) (RuleContext 'Transition (BBODY era)
 -> Rule (CHAIN era) 'Transition (State (BBODY era)))
-> RuleContext 'Transition (BBODY era)
-> Rule (CHAIN era) 'Transition (State (BBODY era))
forall a b. (a -> b) -> a -> b
$
            (Environment (BBODY era), State (BBODY era), Signal (BBODY era))
-> TRC (BBODY era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (PParams era -> AccountState -> BbodyEnv era
forall era. PParams era -> AccountState -> BbodyEnv era
BbodyEnv PParams era
pp' AccountState
account, LedgerState era -> BlocksMade era -> BbodyState era
forall era. LedgerState era -> BlocksMade era -> BbodyState era
BbodyState LedgerState era
ls BlocksMade era
bcur, Signal (BBODY era)
Signal (CHAIN era)
block)

        let nes'' :: NewEpochState era
nes'' = NewEpochState era
-> BlocksMade era -> LedgerState era -> NewEpochState era
forall era.
NewEpochState era
-> BlocksMade era -> LedgerState era -> NewEpochState era
updateNES NewEpochState era
nes' BlocksMade era
bcur' LedgerState era
ls'
            bhb :: BHBody (Crypto era)
bhb = BHeader (Crypto era) -> BHBody (Crypto era)
forall crypto. Crypto crypto => BHeader crypto -> BHBody crypto
bhbody BHeader (Crypto era)
bh
            lab' :: WithOrigin (LastAppliedBlock (Crypto era))
lab' =
              LastAppliedBlock (Crypto era)
-> WithOrigin (LastAppliedBlock (Crypto era))
forall t. t -> WithOrigin t
At (LastAppliedBlock (Crypto era)
 -> WithOrigin (LastAppliedBlock (Crypto era)))
-> LastAppliedBlock (Crypto era)
-> WithOrigin (LastAppliedBlock (Crypto era))
forall a b. (a -> b) -> a -> b
$
                BlockNo
-> SlotNo
-> HashHeader (Crypto era)
-> LastAppliedBlock (Crypto era)
forall crypto.
BlockNo -> SlotNo -> HashHeader crypto -> LastAppliedBlock crypto
LastAppliedBlock
                  (BHBody (Crypto era) -> BlockNo
forall crypto. BHBody crypto -> BlockNo
bheaderBlockNo BHBody (Crypto era)
bhb)
                  (BHBody (Crypto era) -> SlotNo
forall crypto. BHBody crypto -> SlotNo
bheaderSlotNo BHBody (Crypto era)
bhb)
                  (BHeader (Crypto era) -> HashHeader (Crypto era)
forall crypto. Crypto crypto => BHeader crypto -> HashHeader crypto
bhHash BHeader (Crypto era)
bh)

        ChainState era
-> F (Clause (CHAIN era) 'Transition) (ChainState era)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ChainState era
 -> F (Clause (CHAIN era) 'Transition) (ChainState era))
-> ChainState era
-> F (Clause (CHAIN era) 'Transition) (ChainState era)
forall a b. (a -> b) -> a -> b
$ NewEpochState era
-> Map (KeyHash 'BlockIssuer (Crypto era)) Word64
-> Nonce
-> Nonce
-> Nonce
-> Nonce
-> WithOrigin (LastAppliedBlock (Crypto era))
-> ChainState era
forall era.
NewEpochState era
-> Map (KeyHash 'BlockIssuer (Crypto era)) Word64
-> Nonce
-> Nonce
-> Nonce
-> Nonce
-> WithOrigin (LastAppliedBlock (Crypto era))
-> ChainState era
ChainState NewEpochState era
nes'' Map (KeyHash 'BlockIssuer (Crypto era)) Word64
cs' Nonce
eta0' Nonce
etaV' Nonce
etaC' Nonce
etaH' WithOrigin (LastAppliedBlock (Crypto era))
lab'

instance
  ( Era era,
    ShelleyBased era,
    STS (BBODY era)
  ) =>
  Embed (BBODY era) (CHAIN era)
  where
  wrapFailed :: PredicateFailure (BBODY era) -> PredicateFailure (CHAIN era)
wrapFailed = PredicateFailure (BBODY era) -> PredicateFailure (CHAIN era)
forall era.
PredicateFailure (BBODY era) -> ChainPredicateFailure era
BbodyFailure

instance
  ( Era era,
    ShelleyBased era
  ) =>
  Embed TICKN (CHAIN era)
  where
  wrapFailed :: PredicateFailure TICKN -> PredicateFailure (CHAIN era)
wrapFailed = PredicateFailure TICKN -> PredicateFailure (CHAIN era)
forall era. PredicateFailure TICKN -> ChainPredicateFailure era
TicknFailure

instance
  ( Era era,
    ShelleyBased era,
    STS (TICK era)
  ) =>
  Embed (TICK era) (CHAIN era)
  where
  wrapFailed :: PredicateFailure (TICK era) -> PredicateFailure (CHAIN era)
wrapFailed = PredicateFailure (TICK era) -> PredicateFailure (CHAIN era)
forall era.
PredicateFailure (TICK era) -> ChainPredicateFailure era
TickFailure

instance
  ( Era era,
    c ~ Crypto era,
    ShelleyBased era,
    STS (PRTCL c)
  ) =>
  Embed (PRTCL c) (CHAIN era)
  where
  wrapFailed :: PredicateFailure (PRTCL c) -> PredicateFailure (CHAIN era)
wrapFailed = PredicateFailure (PRTCL c) -> PredicateFailure (CHAIN era)
forall era.
PredicateFailure (PRTCL (Crypto era)) -> ChainPredicateFailure era
PrtclFailure

data AdaPots = AdaPots
  { AdaPots -> Coin
treasuryAdaPot :: Coin,
    AdaPots -> Coin
reservesAdaPot :: Coin,
    AdaPots -> Coin
rewardsAdaPot :: Coin,
    AdaPots -> Coin
utxoAdaPot :: Coin,
    AdaPots -> Coin
depositsAdaPot :: Coin,
    AdaPots -> Coin
feesAdaPot :: Coin
  }
  deriving (Int -> AdaPots -> ShowS
[AdaPots] -> ShowS
AdaPots -> String
(Int -> AdaPots -> ShowS)
-> (AdaPots -> String) -> ([AdaPots] -> ShowS) -> Show AdaPots
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AdaPots] -> ShowS
$cshowList :: [AdaPots] -> ShowS
show :: AdaPots -> String
$cshow :: AdaPots -> String
showsPrec :: Int -> AdaPots -> ShowS
$cshowsPrec :: Int -> AdaPots -> ShowS
Show, AdaPots -> AdaPots -> Bool
(AdaPots -> AdaPots -> Bool)
-> (AdaPots -> AdaPots -> Bool) -> Eq AdaPots
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AdaPots -> AdaPots -> Bool
$c/= :: AdaPots -> AdaPots -> Bool
== :: AdaPots -> AdaPots -> Bool
$c== :: AdaPots -> AdaPots -> Bool
Eq)

-- | Calculate the total ada pots in the epoch state
totalAdaPotsES ::
  ShelleyBased era =>
  EpochState era ->
  AdaPots
totalAdaPotsES :: EpochState era -> AdaPots
totalAdaPotsES (EpochState (AccountState Coin
treasury_ Coin
reserves_) SnapShots era
_ LedgerState era
ls PParams era
_ PParams era
_ NonMyopic era
_) =
  AdaPots :: Coin -> Coin -> Coin -> Coin -> Coin -> Coin -> AdaPots
AdaPots
    { treasuryAdaPot :: Coin
treasuryAdaPot = Coin
treasury_,
      reservesAdaPot :: Coin
reservesAdaPot = Coin
reserves_,
      rewardsAdaPot :: Coin
rewardsAdaPot = Coin
rewards_,
      utxoAdaPot :: Coin
utxoAdaPot = Coin
circulation,
      depositsAdaPot :: Coin
depositsAdaPot = Coin
deposits,
      feesAdaPot :: Coin
feesAdaPot = Coin
fees_
    }
  where
    (UTxOState UTxO era
u Coin
deposits Coin
fees_ PPUPState era
_) = LedgerState era -> UTxOState era
forall era. LedgerState era -> UTxOState era
_utxoState LedgerState era
ls
    (DPState DState era
ds PState era
_) = LedgerState era -> DPState era
forall era. LedgerState era -> DPState era
_delegationState LedgerState era
ls
    rewards_ :: Coin
rewards_ = [Coin] -> Coin
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (Map (Credential 'Staking era) Coin -> [Coin]
forall k a. Map k a -> [a]
Map.elems (DState era -> Map (Credential 'Staking era) Coin
forall era. DState era -> RewardAccounts era
_rewards DState era
ds))
    circulation :: Coin
circulation = Value era -> Coin
forall t. Val t => t -> Coin
Val.coin (Value era -> Coin) -> Value era -> Coin
forall a b. (a -> b) -> a -> b
$ UTxO era -> Value era
forall era. ShelleyBased era => UTxO era -> Value era
balance UTxO era
u

-- | Calculate the total ada pots in the chain state
totalAdaPots ::
  ShelleyBased era =>
  ChainState era ->
  AdaPots
totalAdaPots :: ChainState era -> AdaPots
totalAdaPots = EpochState era -> AdaPots
forall era. ShelleyBased era => EpochState era -> AdaPots
totalAdaPotsES (EpochState era -> AdaPots)
-> (ChainState era -> EpochState era) -> ChainState era -> AdaPots
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewEpochState era -> EpochState era
forall era. NewEpochState era -> EpochState era
nesEs (NewEpochState era -> EpochState era)
-> (ChainState era -> NewEpochState era)
-> ChainState era
-> EpochState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChainState era -> NewEpochState era
forall era. ChainState era -> NewEpochState era
chainNes

-- | Calculate the total ada in the epoch state
totalAdaES :: ShelleyBased era => EpochState era -> Coin
totalAdaES :: EpochState era -> Coin
totalAdaES EpochState era
cs =
  Coin
treasuryAdaPot
    Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> Coin
reservesAdaPot
    Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> Coin
rewardsAdaPot
    Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> Coin
utxoAdaPot
    Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> Coin
depositsAdaPot
    Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> Coin
feesAdaPot
  where
    AdaPots
      { Coin
treasuryAdaPot :: Coin
treasuryAdaPot :: AdaPots -> Coin
treasuryAdaPot,
        Coin
reservesAdaPot :: Coin
reservesAdaPot :: AdaPots -> Coin
reservesAdaPot,
        Coin
rewardsAdaPot :: Coin
rewardsAdaPot :: AdaPots -> Coin
rewardsAdaPot,
        Coin
utxoAdaPot :: Coin
utxoAdaPot :: AdaPots -> Coin
utxoAdaPot,
        Coin
depositsAdaPot :: Coin
depositsAdaPot :: AdaPots -> Coin
depositsAdaPot,
        Coin
feesAdaPot :: Coin
feesAdaPot :: AdaPots -> Coin
feesAdaPot
      } = EpochState era -> AdaPots
forall era. ShelleyBased era => EpochState era -> AdaPots
totalAdaPotsES EpochState era
cs

-- | Calculate the total ada in the chain state
totalAda :: ShelleyBased era => ChainState era -> Coin
totalAda :: ChainState era -> Coin
totalAda = EpochState era -> Coin
forall era. ShelleyBased era => EpochState era -> Coin
totalAdaES (EpochState era -> Coin)
-> (ChainState era -> EpochState era) -> ChainState era -> Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewEpochState era -> EpochState era
forall era. NewEpochState era -> EpochState era
nesEs (NewEpochState era -> EpochState era)
-> (ChainState era -> NewEpochState era)
-> ChainState era
-> EpochState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChainState era -> NewEpochState era
forall era. ChainState era -> NewEpochState era
chainNes