{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Shelley.Rules.Chain (
  CHAIN,
  ChainState (..),
  TestChainPredicateFailure (..),
  ChainEvent (..),
  PredicateFailure,
  AdaPots (..),
  initialShelleyState,
  totalAda,
  totalAdaPots,
  chainStateNesL,
) where

import Cardano.Ledger.BHeaderView (BHeaderView)
import Cardano.Ledger.BaseTypes (
  BlocksMade (..),
  Nonce (..),
  ShelleyBase,
  StrictMaybe (..),
 )
import Cardano.Ledger.Binary (EncCBORGroup)
import Cardano.Ledger.Block (Block (..))
import Cardano.Ledger.CertState (VState (..))
import Cardano.Ledger.Chain (
  ChainPredicateFailure (..),
  chainChecks,
  pparamsToChainChecksPParams,
 )
import Cardano.Ledger.Coin (Coin (..))
import qualified Cardano.Ledger.Core as Core
import Cardano.Ledger.EpochBoundary (emptySnapShots)
import Cardano.Ledger.Keys (
  GenDelegPair (..),
  GenDelegs (..),
  KeyHash,
  KeyRole (..),
  coerceKeyRole,
 )
import Cardano.Ledger.PoolDistr (PoolDistr (..))
import Cardano.Ledger.Shelley (ShelleyEra)
import Cardano.Ledger.Shelley.AdaPots (
  AdaPots (..),
  totalAdaES,
  totalAdaPotsES,
 )
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.LedgerState (
  AccountState (..),
  CertState (..),
  DState (..),
  EpochState (..),
  LedgerState (..),
  NewEpochState (..),
  PState (..),
  StashedAVVMAddresses,
  curPParamsEpochStateL,
  dsGenDelegs,
  futurePParamsEpochStateL,
  nesEpochStateL,
  prevPParamsEpochStateL,
  smartUTxOState,
  updateNES,
 )
import Cardano.Ledger.Shelley.Rules (
  BbodyEnv (..),
  ShelleyBBODY,
  ShelleyBbodyPredFailure,
  ShelleyBbodyState (..),
  ShelleyTICK,
  ShelleyTickEvent,
  ShelleyTickPredFailure,
 )
import Cardano.Ledger.Slot (EpochNo)
import qualified Cardano.Ledger.UMap as UM
import Cardano.Ledger.UTxO (UTxO (..))
import Cardano.Protocol.TPraos.BHeader (
  BHeader,
  HashHeader,
  LastAppliedBlock (..),
  bhHash,
  bhbody,
  bheaderBlockNo,
  bheaderSlotNo,
  lastAppliedHash,
  makeHeaderView,
  prevHashToNonce,
 )
import Cardano.Protocol.TPraos.Rules.Prtcl (
  PRTCL,
  PrtclEnv (..),
  PrtclState (..),
  PrtlSeqFailure,
  prtlSeqChecks,
 )
import Cardano.Protocol.TPraos.Rules.Tickn
import Cardano.Slotting.Slot (SlotNo, WithOrigin (..))
import Control.DeepSeq (NFData)
import Control.State.Transition (
  Embed (..),
  STS (..),
  TRC (..),
  TransitionRule,
  failBecause,
  judgmentContext,
  trans,
 )
import Data.Default.Class (Default, def)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Void (Void)
import Data.Word (Word64)
import GHC.Generics (Generic)
import Lens.Micro (Lens', lens, (&), (.~), (^.))
import NoThunks.Class (NoThunks (..))
import Test.Cardano.Ledger.Shelley.TreeDiff ()
import Test.Cardano.Ledger.TreeDiff (ToExpr (toExpr), defaultExprViaShow)

type instance EraRule "TICKN" (ShelleyEra c) = TICKN

data CHAIN era

data ChainState era = ChainState
  { forall era. ChainState era -> NewEpochState era
chainNes :: NewEpochState era
  , forall era.
ChainState era -> Map (KeyHash 'BlockIssuer (EraCrypto era)) Word64
chainOCertIssue :: Map.Map (KeyHash 'BlockIssuer (EraCrypto era)) Word64
  , forall era. ChainState era -> Nonce
chainEpochNonce :: Nonce
  , forall era. ChainState era -> Nonce
chainEvolvingNonce :: Nonce
  , forall era. ChainState era -> Nonce
chainCandidateNonce :: Nonce
  , forall era. ChainState era -> Nonce
chainPrevEpochNonce :: Nonce
  , forall era.
ChainState era -> WithOrigin (LastAppliedBlock (EraCrypto era))
chainLastAppliedBlock :: WithOrigin (LastAppliedBlock (EraCrypto era))
  }
  deriving (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 Show (NewEpochState era) => Show (ChainState era)

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

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

chainStateNesL :: Lens' (ChainState era) (NewEpochState era)
chainStateNesL :: forall era. Lens' (ChainState era) (NewEpochState era)
chainStateNesL = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens forall era. ChainState era -> NewEpochState era
chainNes forall a b. (a -> b) -> a -> b
$ \ChainState era
x NewEpochState era
y -> ChainState era
x {chainNes :: NewEpochState era
chainNes = NewEpochState era
y}

data TestChainPredicateFailure era
  = RealChainPredicateFailure !ChainPredicateFailure
  | BbodyFailure !(PredicateFailure (EraRule "BBODY" era)) -- Subtransition Failures
  | TickFailure !(PredicateFailure (EraRule "TICK" era)) -- Subtransition Failures
  | TicknFailure !(PredicateFailure (EraRule "TICKN" era)) -- Subtransition Failures
  | PrtclFailure !(PredicateFailure (PRTCL (EraCrypto era))) -- Subtransition Failures
  | PrtclSeqFailure !(PrtlSeqFailure (EraCrypto era)) -- Subtransition Failures
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (TestChainPredicateFailure era) x
-> TestChainPredicateFailure era
forall era x.
TestChainPredicateFailure era
-> Rep (TestChainPredicateFailure era) x
$cto :: forall era x.
Rep (TestChainPredicateFailure era) x
-> TestChainPredicateFailure era
$cfrom :: forall era x.
TestChainPredicateFailure era
-> Rep (TestChainPredicateFailure era) x
Generic)

data ChainEvent era
  = BbodyEvent !(Event (EraRule "BBODY" era))
  | TickEvent !(Event (EraRule "TICK" era))
  | TicknEvent !(Event (EraRule "TICKN" era))
  | PrtclEvent !(Event (PRTCL (EraCrypto era)))

deriving stock instance
  ( Era era
  , Show (PredicateFailure (EraRule "BBODY" era))
  , Show (PredicateFailure (EraRule "TICK" era))
  , Show (PredicateFailure (EraRule "TICKN" era))
  ) =>
  Show (TestChainPredicateFailure era)

deriving stock instance
  ( Era era
  , Eq (PredicateFailure (EraRule "BBODY" era))
  , Eq (PredicateFailure (EraRule "TICK" era))
  , Eq (PredicateFailure (EraRule "TICKN" era))
  ) =>
  Eq (TestChainPredicateFailure era)

instance
  ( Era era
  , NoThunks (PredicateFailure (EraRule "BBODY" era))
  , NoThunks (PredicateFailure (EraRule "TICK" era))
  , NoThunks (PredicateFailure (EraRule "TICKN" era))
  ) =>
  NoThunks (TestChainPredicateFailure era)

-- | Creates a valid initial chain state
initialShelleyState ::
  forall era.
  ( EraTxOut era
  , EraGov era
  , Default (StashedAVVMAddresses era)
  ) =>
  WithOrigin (LastAppliedBlock (EraCrypto era)) ->
  EpochNo ->
  UTxO era ->
  Coin ->
  Map (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era)) ->
  PParams era ->
  Nonce ->
  ChainState era
initialShelleyState :: forall era.
(EraTxOut era, EraGov era, Default (StashedAVVMAddresses era)) =>
WithOrigin (LastAppliedBlock (EraCrypto era))
-> EpochNo
-> UTxO era
-> Coin
-> Map
     (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
-> PParams era
-> Nonce
-> ChainState era
initialShelleyState WithOrigin (LastAppliedBlock (EraCrypto era))
lab EpochNo
e UTxO era
utxo Coin
reserves Map
  (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
genDelegs PParams era
pp Nonce
initNonce =
  forall era.
NewEpochState era
-> Map (KeyHash 'BlockIssuer (EraCrypto era)) Word64
-> Nonce
-> Nonce
-> Nonce
-> Nonce
-> WithOrigin (LastAppliedBlock (EraCrypto era))
-> ChainState era
ChainState
    ( forall era.
EpochNo
-> BlocksMade (EraCrypto era)
-> BlocksMade (EraCrypto era)
-> EpochState era
-> StrictMaybe (PulsingRewUpdate (EraCrypto era))
-> PoolDistr (EraCrypto era)
-> StashedAVVMAddresses era
-> NewEpochState era
NewEpochState
        EpochNo
e
        (forall c. Map (KeyHash 'StakePool c) Natural -> BlocksMade c
BlocksMade forall k a. Map k a
Map.empty)
        (forall c. Map (KeyHash 'StakePool c) Natural -> BlocksMade c
BlocksMade forall k a. Map k a
Map.empty)
        ( forall era.
AccountState
-> LedgerState era
-> SnapShots (EraCrypto era)
-> NonMyopic (EraCrypto era)
-> EpochState era
EpochState
            (Coin -> Coin -> AccountState
AccountState (Integer -> Coin
Coin Integer
0) Coin
reserves)
            ( forall era. UTxOState era -> CertState era -> LedgerState era
LedgerState
                ( forall era.
EraTxOut era =>
PParams era
-> UTxO era
-> Coin
-> Coin
-> GovState era
-> Coin
-> UTxOState era
smartUTxOState
                    PParams era
pp
                    UTxO era
utxo
                    (Integer -> Coin
Coin Integer
0)
                    (Integer -> Coin
Coin Integer
0)
                    forall era. EraGov era => GovState era
emptyGovState
                    forall a. Monoid a => a
mempty
                )
                (forall era. VState era -> PState era -> DState era -> CertState era
CertState forall a. Default a => a
def forall a. Default a => a
def DState era
dState)
            )
            forall c. SnapShots c
emptySnapShots
            forall a. Default a => a
def
            forall a b. a -> (a -> b) -> b
& forall era. EraGov era => Lens' (EpochState era) (PParams era)
curPParamsEpochStateL forall s t a b. ASetter s t a b -> b -> s -> t
.~ PParams era
pp
            forall a b. a -> (a -> b) -> b
& forall era. EraGov era => Lens' (EpochState era) (PParams era)
prevPParamsEpochStateL forall s t a b. ASetter s t a b -> b -> s -> t
.~ PParams era
pp
            forall a b. a -> (a -> b) -> b
& forall era.
EraGov era =>
Lens' (EpochState era) (FuturePParams era)
futurePParamsEpochStateL forall s t a b. ASetter s t a b -> b -> s -> t
.~ forall era. Maybe (PParams era) -> FuturePParams era
PotentialPParamsUpdate forall a. Maybe a
Nothing
        )
        forall a. StrictMaybe a
SNothing
        (forall c.
Map (KeyHash 'StakePool c) (IndividualPoolStake c)
-> CompactForm Coin -> PoolDistr c
PoolDistr forall k a. Map k a
Map.empty forall a. Monoid a => a
mempty)
        forall a. Default a => a
def
    )
    Map (KeyHash 'BlockIssuer (EraCrypto era)) Word64
cs
    Nonce
initNonce
    Nonce
initNonce
    Nonce
initNonce
    Nonce
NeutralNonce
    WithOrigin (LastAppliedBlock (EraCrypto era))
lab
  where
    cs :: Map (KeyHash 'BlockIssuer (EraCrypto era)) Word64
cs =
      forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
        ( forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
            (\(GenDelegPair KeyHash 'GenesisDelegate (EraCrypto era)
hk Hash (EraCrypto era) (VerKeyVRF (EraCrypto era))
_) -> (forall (a :: KeyRole -> * -> *) (r :: KeyRole) c (r' :: KeyRole).
HasKeyRole a =>
a r c -> a r' c
coerceKeyRole KeyHash 'GenesisDelegate (EraCrypto era)
hk, Word64
0))
            (forall k a. Map k a -> [a]
Map.elems Map
  (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
genDelegs)
        )

    dState :: DState era
    dState :: DState era
dState =
      DState
        { dsUnified :: UMap (EraCrypto era)
dsUnified = forall c. UMap c
UM.empty
        , dsFutureGenDelegs :: Map (FutureGenDeleg (EraCrypto era)) (GenDelegPair (EraCrypto era))
dsFutureGenDelegs = forall k a. Map k a
Map.empty
        , dsGenDelegs :: GenDelegs (EraCrypto era)
dsGenDelegs = forall c. Map (KeyHash 'Genesis c) (GenDelegPair c) -> GenDelegs c
GenDelegs Map
  (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
genDelegs
        , dsIRewards :: InstantaneousRewards (EraCrypto era)
dsIRewards = forall a. Default a => a
def
        }

instance
  ( EraGov era
  , Embed (EraRule "BBODY" era) (CHAIN era)
  , Environment (EraRule "BBODY" era) ~ BbodyEnv era
  , State (EraRule "BBODY" era) ~ ShelleyBbodyState era
  , Signal (EraRule "BBODY" era) ~ Block (BHeaderView (EraCrypto era)) era
  , Embed (EraRule "TICKN" era) (CHAIN era)
  , Environment (EraRule "TICKN" era) ~ TicknEnv
  , State (EraRule "TICKN" era) ~ TicknState
  , Signal (EraRule "TICKN" era) ~ Bool
  , Embed (EraRule "TICK" era) (CHAIN era)
  , Environment (EraRule "TICK" era) ~ ()
  , State (EraRule "TICK" era) ~ NewEpochState era
  , Signal (EraRule "TICK" era) ~ SlotNo
  , Embed (PRTCL (EraCrypto era)) (CHAIN era)
  , EncCBORGroup (TxSeq era)
  , ProtVerAtMost era 6
  , State (Core.EraRule "LEDGERS" era) ~ LedgerState era
  ) =>
  STS (CHAIN era)
  where
  type
    State (CHAIN era) =
      ChainState era

  type
    Signal (CHAIN era) =
      Block (BHeader (EraCrypto era)) era

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

  type PredicateFailure (CHAIN era) = TestChainPredicateFailure era
  type Event (CHAIN era) = ChainEvent era

  initialRules :: [InitialRule (CHAIN era)]
initialRules = []
  transitionRules :: [TransitionRule (CHAIN era)]
transitionRules = [forall era.
(Embed (EraRule "BBODY" era) (CHAIN era),
 Environment (EraRule "BBODY" era) ~ BbodyEnv era,
 State (EraRule "BBODY" era) ~ ShelleyBbodyState era,
 Signal (EraRule "BBODY" era)
 ~ Block (BHeaderView (EraCrypto era)) era,
 Embed (EraRule "TICKN" era) (CHAIN era),
 Environment (EraRule "TICKN" era) ~ TicknEnv,
 State (EraRule "TICKN" era) ~ TicknState,
 Signal (EraRule "TICKN" era) ~ Bool,
 Embed (EraRule "TICK" era) (CHAIN era),
 Environment (EraRule "TICK" era) ~ (),
 State (EraRule "TICK" era) ~ NewEpochState era,
 Signal (EraRule "TICK" era) ~ SlotNo,
 Embed (PRTCL (EraCrypto era)) (CHAIN era),
 EncCBORGroup (TxSeq era), ProtVerAtMost era 6,
 State (EraRule "LEDGERS" era) ~ LedgerState era, EraGov era) =>
TransitionRule (CHAIN era)
chainTransition]

chainTransition ::
  forall era.
  ( Embed (EraRule "BBODY" era) (CHAIN era)
  , Environment (EraRule "BBODY" era) ~ BbodyEnv era
  , State (EraRule "BBODY" era) ~ ShelleyBbodyState era
  , Signal (EraRule "BBODY" era) ~ Block (BHeaderView (EraCrypto era)) era
  , Embed (EraRule "TICKN" era) (CHAIN era)
  , Environment (EraRule "TICKN" era) ~ TicknEnv
  , State (EraRule "TICKN" era) ~ TicknState
  , Signal (EraRule "TICKN" era) ~ Bool
  , Embed (EraRule "TICK" era) (CHAIN era)
  , Environment (EraRule "TICK" era) ~ ()
  , State (EraRule "TICK" era) ~ NewEpochState era
  , Signal (EraRule "TICK" era) ~ SlotNo
  , Embed (PRTCL (EraCrypto era)) (CHAIN era)
  , EncCBORGroup (TxSeq era)
  , ProtVerAtMost era 6
  , State (Core.EraRule "LEDGERS" era) ~ LedgerState era
  , EraGov era
  ) =>
  TransitionRule (CHAIN era)
chainTransition :: forall era.
(Embed (EraRule "BBODY" era) (CHAIN era),
 Environment (EraRule "BBODY" era) ~ BbodyEnv era,
 State (EraRule "BBODY" era) ~ ShelleyBbodyState era,
 Signal (EraRule "BBODY" era)
 ~ Block (BHeaderView (EraCrypto era)) era,
 Embed (EraRule "TICKN" era) (CHAIN era),
 Environment (EraRule "TICKN" era) ~ TicknEnv,
 State (EraRule "TICKN" era) ~ TicknState,
 Signal (EraRule "TICKN" era) ~ Bool,
 Embed (EraRule "TICK" era) (CHAIN era),
 Environment (EraRule "TICK" era) ~ (),
 State (EraRule "TICK" era) ~ NewEpochState era,
 Signal (EraRule "TICK" era) ~ SlotNo,
 Embed (PRTCL (EraCrypto era)) (CHAIN era),
 EncCBORGroup (TxSeq era), ProtVerAtMost era 6,
 State (EraRule "LEDGERS" era) ~ LedgerState era, EraGov era) =>
TransitionRule (CHAIN era)
chainTransition =
  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
            ( Environment (CHAIN era)
_
              , ChainState
                  NewEpochState era
nes
                  Map (KeyHash 'BlockIssuer (EraCrypto era)) Word64
cs
                  Nonce
eta0
                  Nonce
etaV
                  Nonce
etaC
                  Nonce
etaH
                  WithOrigin (LastAppliedBlock (EraCrypto era))
lab
              , Block BHeader (EraCrypto era)
bh TxSeq era
txs
              )
          ) -> do
        case forall c (m :: * -> *).
(MonadError (PrtlSeqFailure c) m, Crypto c) =>
WithOrigin (LastAppliedBlock c) -> BHeader c -> m ()
prtlSeqChecks WithOrigin (LastAppliedBlock (EraCrypto era))
lab BHeader (EraCrypto era)
bh of
          Right () -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          Left PrtlSeqFailure (EraCrypto era)
e -> forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause forall a b. (a -> b) -> a -> b
$ forall era.
PrtlSeqFailure (EraCrypto era) -> TestChainPredicateFailure era
PrtclSeqFailure PrtlSeqFailure (EraCrypto era)
e

        let pp :: PParams era
pp = NewEpochState era
nes forall s a. s -> Getting a s a -> a
^. forall era. Lens' (NewEpochState era) (EpochState era)
nesEpochStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraGov era => Lens' (EpochState era) (PParams era)
curPParamsEpochStateL
            chainChecksData :: ChainChecksPParams
chainChecksData = forall era. EraPParams era => PParams era -> ChainChecksPParams
pparamsToChainChecksPParams PParams era
pp
            bhView :: BHeaderView (EraCrypto era)
bhView = forall c. Crypto c => BHeader c -> BHeaderView c
makeHeaderView BHeader (EraCrypto era)
bh

        -- We allow one protocol version higher than the current era's maximum, because
        -- that is the way we can get out of the current era into the next one. We test
        -- this functionality with application of PParamsUpdate that initiate an upgrade
        -- to the next era. This, of course, works properly only with HFC (Hard Fork
        -- Combinator), which is implemented in consensus, but for the purpose of the
        -- CHAIN test this is OK.
        case forall (m :: * -> *) c.
MonadError ChainPredicateFailure m =>
Version -> ChainChecksPParams -> BHeaderView c -> m ()
chainChecks (forall a. Enum a => a -> a
succ (forall era. Era era => Version
eraProtVerHigh @era)) ChainChecksPParams
chainChecksData BHeaderView (EraCrypto era)
bhView of
          Right () -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          Left ChainPredicateFailure
e -> forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause (forall era. ChainPredicateFailure -> TestChainPredicateFailure era
RealChainPredicateFailure ChainPredicateFailure
e)

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

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

        let NewEpochState EpochNo
e1 BlocksMade (EraCrypto era)
_ BlocksMade (EraCrypto era)
_ EpochState era
_ StrictMaybe (PulsingRewUpdate (EraCrypto era))
_ PoolDistr (EraCrypto era)
_ StashedAVVMAddresses era
_ = NewEpochState era
nes
            NewEpochState EpochNo
e2 BlocksMade (EraCrypto era)
_ BlocksMade (EraCrypto era)
bcur EpochState era
es StrictMaybe (PulsingRewUpdate (EraCrypto era))
_ PoolDistr (EraCrypto era)
_pd StashedAVVMAddresses era
_ = NewEpochState era
nes'
        let EpochState AccountState
account LedgerState era
ls SnapShots (EraCrypto era)
_ NonMyopic (EraCrypto era)
_ = EpochState era
es
            pp' :: PParams era
pp' = EpochState era
es forall s a. s -> Getting a s a -> a
^. forall era. EraGov era => Lens' (EpochState era) (PParams era)
curPParamsEpochStateL
        let LedgerState UTxOState era
_ (CertState VState {} PState {} DState {dsGenDelegs :: forall era. DState era -> GenDelegs (EraCrypto era)
dsGenDelegs = GenDelegs (EraCrypto era)
genDelegs}) = LedgerState era
ls
        let ph :: PrevHash (EraCrypto era)
ph = forall c. WithOrigin (LastAppliedBlock c) -> PrevHash c
lastAppliedHash WithOrigin (LastAppliedBlock (EraCrypto era))
lab
            etaPH :: Nonce
etaPH = forall c. PrevHash c -> Nonce
prevHashToNonce PrevHash (EraCrypto era)
ph

        TicknState Nonce
eta0' Nonce
etaH' <-
          forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "TICKN" era) forall a b. (a -> b) -> a -> b
$
            forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC
              ( Nonce -> Nonce -> Nonce -> TicknEnv
TicknEnv (PParams era
pp' forall s a. s -> Getting a s a -> a
^. forall era.
(EraPParams era, ProtVerAtMost era 6) =>
Lens' (PParams era) Nonce
ppExtraEntropyL) Nonce
etaC Nonce
etaPH
              , Nonce -> Nonce -> TicknState
TicknState Nonce
eta0 Nonce
etaH
              , EpochNo
e1 forall a. Eq a => a -> a -> Bool
/= EpochNo
e2
              )

        PrtclState Map (KeyHash 'BlockIssuer (EraCrypto era)) Word64
cs' Nonce
etaV' Nonce
etaC' <-
          forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(PRTCL (EraCrypto era)) forall a b. (a -> b) -> a -> b
$
            forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC
              ( forall c.
UnitInterval -> PoolDistr c -> GenDelegs c -> Nonce -> PrtclEnv c
PrtclEnv (PParams era
pp' forall s a. s -> Getting a s a -> a
^. forall era.
(EraPParams era, ProtVerAtMost era 6) =>
Lens' (PParams era) UnitInterval
ppDL) PoolDistr (EraCrypto era)
_pd GenDelegs (EraCrypto era)
genDelegs Nonce
eta0'
              , forall c.
Map (KeyHash 'BlockIssuer c) Word64
-> Nonce -> Nonce -> PrtclState c
PrtclState Map (KeyHash 'BlockIssuer (EraCrypto era)) Word64
cs Nonce
etaV Nonce
etaC
              , BHeader (EraCrypto era)
bh
              )

        let thouShaltNot :: a
thouShaltNot = forall a. HasCallStack => String -> a
error String
"A block with a header view should never be hashed"
        BbodyState State (EraRule "LEDGERS" era)
ls' BlocksMade (EraCrypto era)
bcur' <-
          forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "BBODY" era) forall a b. (a -> b) -> a -> b
$
            forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (forall era. PParams era -> AccountState -> BbodyEnv era
BbodyEnv PParams era
pp' AccountState
account, forall era.
State (EraRule "LEDGERS" era)
-> BlocksMade (EraCrypto era) -> ShelleyBbodyState era
BbodyState LedgerState era
ls BlocksMade (EraCrypto era)
bcur, forall h era. h -> TxSeq era -> ByteString -> Block h era
Block' BHeaderView (EraCrypto era)
bhView TxSeq era
txs forall {a}. a
thouShaltNot)

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

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

instance
  ( Era era
  , Era era
  , STS (ShelleyBBODY era)
  , PredicateFailure (EraRule "BBODY" era) ~ ShelleyBbodyPredFailure era
  , Event (EraRule "BBODY" era) ~ Event (ShelleyBBODY era)
  ) =>
  Embed (ShelleyBBODY era) (CHAIN era)
  where
  wrapFailed :: PredicateFailure (ShelleyBBODY era) -> PredicateFailure (CHAIN era)
wrapFailed = forall era.
PredicateFailure (EraRule "BBODY" era)
-> TestChainPredicateFailure era
BbodyFailure
  wrapEvent :: Event (ShelleyBBODY era) -> Event (CHAIN era)
wrapEvent = forall era. Event (EraRule "BBODY" era) -> ChainEvent era
BbodyEvent

instance
  ( Era era
  , Era era
  , PredicateFailure (EraRule "TICKN" era) ~ TicknPredicateFailure
  , Event (EraRule "TICKN" era) ~ Void
  ) =>
  Embed TICKN (CHAIN era)
  where
  wrapFailed :: PredicateFailure TICKN -> PredicateFailure (CHAIN era)
wrapFailed = forall era.
PredicateFailure (EraRule "TICKN" era)
-> TestChainPredicateFailure era
TicknFailure
  wrapEvent :: Event TICKN -> Event (CHAIN era)
wrapEvent = forall era. Event (EraRule "TICKN" era) -> ChainEvent era
TicknEvent

instance
  ( Era era
  , Era era
  , STS (ShelleyTICK era)
  , PredicateFailure (EraRule "TICK" era) ~ ShelleyTickPredFailure era
  , Event (EraRule "TICK" era) ~ ShelleyTickEvent era
  ) =>
  Embed (ShelleyTICK era) (CHAIN era)
  where
  wrapFailed :: PredicateFailure (ShelleyTICK era) -> PredicateFailure (CHAIN era)
wrapFailed = forall era.
PredicateFailure (EraRule "TICK" era)
-> TestChainPredicateFailure era
TickFailure
  wrapEvent :: Event (ShelleyTICK era) -> Event (CHAIN era)
wrapEvent = forall era. Event (EraRule "TICK" era) -> ChainEvent era
TickEvent

instance
  ( Era era
  , c ~ EraCrypto era
  , Era era
  , STS (PRTCL c)
  ) =>
  Embed (PRTCL c) (CHAIN era)
  where
  wrapFailed :: PredicateFailure (PRTCL c) -> PredicateFailure (CHAIN era)
wrapFailed = forall era.
PredicateFailure (PRTCL (EraCrypto era))
-> TestChainPredicateFailure era
PrtclFailure
  wrapEvent :: Event (PRTCL c) -> Event (CHAIN era)
wrapEvent = forall era. Event (PRTCL (EraCrypto era)) -> ChainEvent era
PrtclEvent

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

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

instance
  ( ToExpr (PParams era)
  , ToExpr (TxOut era)
  , ToExpr (StashedAVVMAddresses era)
  , ToExpr (GovState era)
  ) =>
  ToExpr (ChainState era)

instance ToExpr (HashHeader c) where
  toExpr :: HashHeader c -> Expr
toExpr = forall a. Show a => a -> Expr
defaultExprViaShow

instance ToExpr (LastAppliedBlock c)