{-# 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.Chain (
  ChainPredicateFailure (..),
  chainChecks,
  pparamsToChainChecksPParams,
 )
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Core
import Cardano.Ledger.Keys (GenDelegPair (..), GenDelegs (..), coerceKeyRole)
import Cardano.Ledger.Shelley (ShelleyEra)
import Cardano.Ledger.Shelley.AdaPots (
  AdaPots (..),
  totalAdaES,
  totalAdaPotsES,
 )
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.LedgerState (
  EpochState (..),
  LedgerState (..),
  NewEpochState (..),
  StashedAVVMAddresses,
  curPParamsEpochStateL,
  futurePParamsEpochStateL,
  nesEpochStateL,
  prevPParamsEpochStateL,
  smartUTxOState,
  updateNES,
 )
import Cardano.Ledger.Shelley.Rules (
  BbodyEnv (..),
  ShelleyBBODY,
  ShelleyBbodyPredFailure,
  ShelleyBbodyState (..),
  ShelleyTICK,
  ShelleyTickEvent,
  ShelleyTickPredFailure,
 )
import Cardano.Ledger.Shelley.State
import Cardano.Ledger.Slot (EpochNo)
import qualified Cardano.Ledger.UMap as UM
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 (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.ConcreteCryptoTypes (MockCrypto)
import Test.Cardano.Ledger.Shelley.TreeDiff ()
import Test.Cardano.Ledger.TreeDiff (ToExpr (toExpr), defaultExprViaShow)

type instance EraRule "TICKN" ShelleyEra = TICKN

data CHAIN era

data ChainState era = ChainState
  { forall era. ChainState era -> NewEpochState era
chainNes :: NewEpochState era
  , forall era. ChainState era -> Map (KeyHash 'BlockIssuer) Word64
chainOCertIssue :: Map.Map (KeyHash 'BlockIssuer) 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
chainLastAppliedBlock :: WithOrigin LastAppliedBlock
  }
  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
$cfrom :: forall era x. ChainState era -> Rep (ChainState era) x
from :: forall x. ChainState era -> Rep (ChainState era) x
$cto :: forall era x. Rep (ChainState era) x -> ChainState era
to :: forall x. Rep (ChainState era) x -> ChainState era
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 (f :: * -> *).
Functor f =>
(NewEpochState era -> f (NewEpochState era))
-> ChainState era -> f (ChainState era)
chainStateNesL = (ChainState era -> NewEpochState era)
-> (ChainState era -> NewEpochState era -> ChainState era)
-> forall {f :: * -> *}.
   Functor f =>
   (NewEpochState era -> f (NewEpochState era))
   -> ChainState era -> f (ChainState era)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens ChainState era -> NewEpochState era
forall era. ChainState era -> NewEpochState era
chainNes ((ChainState era -> NewEpochState era -> ChainState era)
 -> forall {f :: * -> *}.
    Functor f =>
    (NewEpochState era -> f (NewEpochState era))
    -> ChainState era -> f (ChainState era))
-> (ChainState era -> NewEpochState era -> ChainState era)
-> forall {f :: * -> *}.
   Functor f =>
   (NewEpochState era -> f (NewEpochState era))
   -> ChainState era -> f (ChainState era)
forall a b. (a -> b) -> a -> b
$ \ChainState era
x NewEpochState era
y -> ChainState era
x {chainNes = 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 MockCrypto)) -- Subtransition Failures
  | PrtclSeqFailure PrtlSeqFailure -- Subtransition Failures
  deriving ((forall x.
 TestChainPredicateFailure era
 -> Rep (TestChainPredicateFailure era) x)
-> (forall x.
    Rep (TestChainPredicateFailure era) x
    -> TestChainPredicateFailure era)
-> Generic (TestChainPredicateFailure era)
forall x.
Rep (TestChainPredicateFailure era) x
-> TestChainPredicateFailure era
forall x.
TestChainPredicateFailure era
-> Rep (TestChainPredicateFailure era) x
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
$cfrom :: forall era x.
TestChainPredicateFailure era
-> Rep (TestChainPredicateFailure era) x
from :: forall x.
TestChainPredicateFailure era
-> Rep (TestChainPredicateFailure era) x
$cto :: forall era x.
Rep (TestChainPredicateFailure era) x
-> TestChainPredicateFailure era
to :: forall x.
Rep (TestChainPredicateFailure era) x
-> TestChainPredicateFailure era
Generic)

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

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.
  ( EraGov era
  , EraStake era
  , EraCertState era
  , Default (StashedAVVMAddresses era)
  ) =>
  WithOrigin LastAppliedBlock ->
  EpochNo ->
  UTxO era ->
  Coin ->
  Map (KeyHash 'Genesis) GenDelegPair ->
  PParams era ->
  Nonce ->
  ChainState era
initialShelleyState :: forall era.
(EraGov era, EraStake era, EraCertState era,
 Default (StashedAVVMAddresses era)) =>
WithOrigin LastAppliedBlock
-> EpochNo
-> UTxO era
-> Coin
-> Map (KeyHash 'Genesis) GenDelegPair
-> PParams era
-> Nonce
-> ChainState era
initialShelleyState WithOrigin LastAppliedBlock
lab EpochNo
e UTxO era
utxo Coin
reserves Map (KeyHash 'Genesis) GenDelegPair
genDelegs PParams era
pp Nonce
initNonce =
  NewEpochState era
-> Map (KeyHash 'BlockIssuer) Word64
-> Nonce
-> Nonce
-> Nonce
-> Nonce
-> WithOrigin LastAppliedBlock
-> ChainState era
forall era.
NewEpochState era
-> Map (KeyHash 'BlockIssuer) Word64
-> Nonce
-> Nonce
-> Nonce
-> Nonce
-> WithOrigin LastAppliedBlock
-> ChainState era
ChainState
    ( EpochNo
-> BlocksMade
-> BlocksMade
-> EpochState era
-> StrictMaybe PulsingRewUpdate
-> PoolDistr
-> StashedAVVMAddresses era
-> NewEpochState era
forall era.
EpochNo
-> BlocksMade
-> BlocksMade
-> EpochState era
-> StrictMaybe PulsingRewUpdate
-> PoolDistr
-> StashedAVVMAddresses era
-> NewEpochState era
NewEpochState
        EpochNo
e
        (Map (KeyHash 'StakePool) Natural -> BlocksMade
BlocksMade Map (KeyHash 'StakePool) Natural
forall k a. Map k a
Map.empty)
        (Map (KeyHash 'StakePool) Natural -> BlocksMade
BlocksMade Map (KeyHash 'StakePool) Natural
forall k a. Map k a
Map.empty)
        ( ChainAccountState
-> LedgerState era -> SnapShots -> NonMyopic -> EpochState era
forall era.
ChainAccountState
-> LedgerState era -> SnapShots -> NonMyopic -> EpochState era
EpochState
            ChainAccountState
              { casTreasury :: Coin
casTreasury = Integer -> Coin
Coin Integer
0
              , casReserves :: Coin
casReserves = Coin
reserves
              }
            ( UTxOState era -> CertState era -> LedgerState era
forall era. UTxOState era -> CertState era -> LedgerState era
LedgerState
                ( PParams era
-> UTxO era
-> Coin
-> Coin
-> GovState era
-> Coin
-> UTxOState era
forall era.
EraStake 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)
                    GovState era
forall era. EraGov era => GovState era
emptyGovState
                    Coin
forall a. Monoid a => a
mempty
                )
                (CertState era
forall a. Default a => a
def CertState era -> (CertState era -> CertState era) -> CertState era
forall a b. a -> (a -> b) -> b
& (DState era -> Identity (DState era))
-> CertState era -> Identity (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era -> Identity (DState era))
 -> CertState era -> Identity (CertState era))
-> DState era -> CertState era -> CertState era
forall s t a b. ASetter s t a b -> b -> s -> t
.~ DState era
dState)
            )
            SnapShots
emptySnapShots
            NonMyopic
forall a. Default a => a
def
            EpochState era
-> (EpochState era -> EpochState era) -> EpochState era
forall a b. a -> (a -> b) -> b
& (PParams era -> Identity (PParams era))
-> EpochState era -> Identity (EpochState era)
forall era. EraGov era => Lens' (EpochState era) (PParams era)
Lens' (EpochState era) (PParams era)
curPParamsEpochStateL ((PParams era -> Identity (PParams era))
 -> EpochState era -> Identity (EpochState era))
-> PParams era -> EpochState era -> EpochState era
forall s t a b. ASetter s t a b -> b -> s -> t
.~ PParams era
pp
            EpochState era
-> (EpochState era -> EpochState era) -> EpochState era
forall a b. a -> (a -> b) -> b
& (PParams era -> Identity (PParams era))
-> EpochState era -> Identity (EpochState era)
forall era. EraGov era => Lens' (EpochState era) (PParams era)
Lens' (EpochState era) (PParams era)
prevPParamsEpochStateL ((PParams era -> Identity (PParams era))
 -> EpochState era -> Identity (EpochState era))
-> PParams era -> EpochState era -> EpochState era
forall s t a b. ASetter s t a b -> b -> s -> t
.~ PParams era
pp
            EpochState era
-> (EpochState era -> EpochState era) -> EpochState era
forall a b. a -> (a -> b) -> b
& (FuturePParams era -> Identity (FuturePParams era))
-> EpochState era -> Identity (EpochState era)
forall era.
EraGov era =>
Lens' (EpochState era) (FuturePParams era)
Lens' (EpochState era) (FuturePParams era)
futurePParamsEpochStateL ((FuturePParams era -> Identity (FuturePParams era))
 -> EpochState era -> Identity (EpochState era))
-> FuturePParams era -> EpochState era -> EpochState era
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Maybe (PParams era) -> FuturePParams era
forall era. Maybe (PParams era) -> FuturePParams era
PotentialPParamsUpdate Maybe (PParams era)
forall a. Maybe a
Nothing
        )
        StrictMaybe PulsingRewUpdate
forall a. StrictMaybe a
SNothing
        (Map (KeyHash 'StakePool) IndividualPoolStake
-> CompactForm Coin -> PoolDistr
PoolDistr Map (KeyHash 'StakePool) IndividualPoolStake
forall k a. Map k a
Map.empty CompactForm Coin
forall a. Monoid a => a
mempty)
        StashedAVVMAddresses era
forall a. Default a => a
def
    )
    Map (KeyHash 'BlockIssuer) Word64
cs
    Nonce
initNonce
    Nonce
initNonce
    Nonce
initNonce
    Nonce
NeutralNonce
    WithOrigin LastAppliedBlock
lab
  where
    cs :: Map (KeyHash 'BlockIssuer) Word64
cs =
      [(KeyHash 'BlockIssuer, Word64)]
-> Map (KeyHash 'BlockIssuer) Word64
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
        ( (GenDelegPair -> (KeyHash 'BlockIssuer, Word64))
-> [GenDelegPair] -> [(KeyHash 'BlockIssuer, Word64)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
            (\(GenDelegPair KeyHash 'GenesisDelegate
hk VRFVerKeyHash 'GenDelegVRF
_) -> (KeyHash 'GenesisDelegate -> KeyHash 'BlockIssuer
forall (r :: KeyRole) (r' :: KeyRole). KeyHash r -> KeyHash r'
forall (a :: KeyRole -> *) (r :: KeyRole) (r' :: KeyRole).
HasKeyRole a =>
a r -> a r'
coerceKeyRole KeyHash 'GenesisDelegate
hk, Word64
0))
            (Map (KeyHash 'Genesis) GenDelegPair -> [GenDelegPair]
forall k a. Map k a -> [a]
Map.elems Map (KeyHash 'Genesis) GenDelegPair
genDelegs)
        )

    dState :: DState era
    dState :: DState era
dState =
      DState
        { dsUnified :: UMap
dsUnified = UMap
UM.empty
        , dsFutureGenDelegs :: Map FutureGenDeleg GenDelegPair
dsFutureGenDelegs = Map FutureGenDeleg GenDelegPair
forall k a. Map k a
Map.empty
        , dsGenDelegs :: GenDelegs
dsGenDelegs = Map (KeyHash 'Genesis) GenDelegPair -> GenDelegs
GenDelegs Map (KeyHash 'Genesis) GenDelegPair
genDelegs
        , dsIRewards :: InstantaneousRewards
dsIRewards = InstantaneousRewards
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 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 MockCrypto) (CHAIN era)
  , EncCBORGroup (TxSeq era)
  , ProtVerAtMost era 6
  , State (EraRule "LEDGERS" era) ~ LedgerState era
  , EraCertState era
  ) =>
  STS (CHAIN era)
  where
  type State (CHAIN era) = ChainState era

  type Signal (CHAIN era) = Block (BHeader MockCrypto) 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 = [TransitionRule (CHAIN era)
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 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 MockCrypto) (CHAIN era), ProtVerAtMost era 6,
 State (EraRule "LEDGERS" era) ~ LedgerState era, EraGov era,
 EraCertState 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 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 MockCrypto) (CHAIN era)
  , ProtVerAtMost era 6
  , State (EraRule "LEDGERS" era) ~ LedgerState era
  , EraGov era
  , EraCertState 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 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 MockCrypto) (CHAIN era), ProtVerAtMost era 6,
 State (EraRule "LEDGERS" era) ~ LedgerState era, EraGov era,
 EraCertState era) =>
TransitionRule (CHAIN era)
chainTransition =
  Rule (CHAIN era) 'Transition (RuleContext 'Transition (CHAIN era))
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 a b.
F (Clause (CHAIN era) 'Transition) a
-> (a -> F (Clause (CHAIN era) 'Transition) b)
-> F (Clause (CHAIN era) 'Transition) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \( TRC
             ( Environment (CHAIN era)
_
               , ChainState
                   NewEpochState era
nes
                   Map (KeyHash 'BlockIssuer) Word64
cs
                   Nonce
eta0
                   Nonce
etaV
                   Nonce
etaC
                   Nonce
etaH
                   WithOrigin LastAppliedBlock
lab
               , Block BHeader MockCrypto
bh TxSeq era
txs
               )
           ) -> do
        case WithOrigin LastAppliedBlock
-> BHeader MockCrypto -> Either PrtlSeqFailure ()
forall (m :: * -> *) c.
(MonadError PrtlSeqFailure m, Crypto c) =>
WithOrigin LastAppliedBlock -> BHeader c -> m ()
prtlSeqChecks WithOrigin LastAppliedBlock
lab BHeader MockCrypto
bh of
          Right () -> () -> F (Clause (CHAIN era) 'Transition) ()
forall a. a -> F (Clause (CHAIN era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          Left PrtlSeqFailure
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 -> TestChainPredicateFailure era
forall era. PrtlSeqFailure -> TestChainPredicateFailure era
PrtclSeqFailure PrtlSeqFailure
e

        let pp :: PParams era
pp = NewEpochState era
nes NewEpochState era
-> Getting (PParams era) (NewEpochState era) (PParams era)
-> PParams era
forall s a. s -> Getting a s a -> a
^. (EpochState era -> Const (PParams era) (EpochState era))
-> NewEpochState era -> Const (PParams era) (NewEpochState era)
forall era (f :: * -> *).
Functor f =>
(EpochState era -> f (EpochState era))
-> NewEpochState era -> f (NewEpochState era)
nesEpochStateL ((EpochState era -> Const (PParams era) (EpochState era))
 -> NewEpochState era -> Const (PParams era) (NewEpochState era))
-> ((PParams era -> Const (PParams era) (PParams era))
    -> EpochState era -> Const (PParams era) (EpochState era))
-> Getting (PParams era) (NewEpochState era) (PParams era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PParams era -> Const (PParams era) (PParams era))
-> EpochState era -> Const (PParams era) (EpochState era)
forall era. EraGov era => Lens' (EpochState era) (PParams era)
Lens' (EpochState era) (PParams era)
curPParamsEpochStateL
            chainChecksData :: ChainChecksPParams
chainChecksData = PParams era -> ChainChecksPParams
forall era. EraPParams era => PParams era -> ChainChecksPParams
pparamsToChainChecksPParams PParams era
pp
            bhView :: BHeaderView
bhView = BHeader MockCrypto -> BHeaderView
forall c. Crypto c => BHeader c -> BHeaderView
makeHeaderView BHeader MockCrypto
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 Version
-> ChainChecksPParams
-> BHeaderView
-> Either ChainPredicateFailure ()
forall (m :: * -> *).
MonadError ChainPredicateFailure m =>
Version -> ChainChecksPParams -> BHeaderView -> m ()
chainChecks (Version -> Version
forall a. Enum a => a -> a
succ (forall era. Era era => Version
eraProtVerHigh @era)) ChainChecksPParams
chainChecksData BHeaderView
bhView of
          Right () -> () -> F (Clause (CHAIN era) 'Transition) ()
forall a. a -> F (Clause (CHAIN era) 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          Left ChainPredicateFailure
e -> PredicateFailure (CHAIN era)
-> F (Clause (CHAIN era) 'Transition) ()
forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecause (ChainPredicateFailure -> TestChainPredicateFailure era
forall era. ChainPredicateFailure -> TestChainPredicateFailure era
RealChainPredicateFailure ChainPredicateFailure
e)

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

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

        let NewEpochState EpochNo
e1 BlocksMade
_ BlocksMade
_ EpochState era
_ StrictMaybe PulsingRewUpdate
_ PoolDistr
_ StashedAVVMAddresses era
_ = NewEpochState era
nes
            NewEpochState EpochNo
e2 BlocksMade
_ BlocksMade
bcur EpochState era
es StrictMaybe PulsingRewUpdate
_ PoolDistr
_pd StashedAVVMAddresses era
_ = NewEpochState era
nes'
        let EpochState ChainAccountState
account LedgerState era
ls SnapShots
_ NonMyopic
_ = EpochState era
es
            pp' :: PParams era
pp' = EpochState era
es EpochState era
-> ((PParams era -> Const (PParams era) (PParams era))
    -> EpochState era -> Const (PParams era) (EpochState era))
-> PParams era
forall s a. s -> Getting a s a -> a
^. (PParams era -> Const (PParams era) (PParams era))
-> EpochState era -> Const (PParams era) (EpochState era)
forall era. EraGov era => Lens' (EpochState era) (PParams era)
Lens' (EpochState era) (PParams era)
curPParamsEpochStateL
        let LedgerState UTxOState era
_ CertState era
certState = LedgerState era
ls
            genDelegs :: GenDelegs
genDelegs = CertState era
certState CertState era
-> Getting GenDelegs (CertState era) GenDelegs -> GenDelegs
forall s a. s -> Getting a s a -> a
^. (DState era -> Const GenDelegs (DState era))
-> CertState era -> Const GenDelegs (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era -> Const GenDelegs (DState era))
 -> CertState era -> Const GenDelegs (CertState era))
-> ((GenDelegs -> Const GenDelegs GenDelegs)
    -> DState era -> Const GenDelegs (DState era))
-> Getting GenDelegs (CertState era) GenDelegs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GenDelegs -> Const GenDelegs GenDelegs)
-> DState era -> Const GenDelegs (DState era)
forall era (f :: * -> *).
Functor f =>
(GenDelegs -> f GenDelegs) -> DState era -> f (DState era)
dsGenDelegsL
            ph :: PrevHash
ph = WithOrigin LastAppliedBlock -> PrevHash
lastAppliedHash WithOrigin LastAppliedBlock
lab
            etaPH :: Nonce
etaPH = PrevHash -> Nonce
prevHashToNonce PrevHash
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) (RuleContext 'Transition (EraRule "TICKN" era)
 -> Rule (CHAIN era) 'Transition (State (EraRule "TICKN" era)))
-> RuleContext 'Transition (EraRule "TICKN" era)
-> Rule (CHAIN era) 'Transition (State (EraRule "TICKN" era))
forall a b. (a -> b) -> a -> b
$
            (Environment (EraRule "TICKN" era), State (EraRule "TICKN" era),
 Signal (EraRule "TICKN" era))
-> TRC (EraRule "TICKN" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC
              ( Nonce -> Nonce -> Nonce -> TicknEnv
TicknEnv (PParams era
pp' PParams era -> Getting Nonce (PParams era) Nonce -> Nonce
forall s a. s -> Getting a s a -> a
^. Getting Nonce (PParams era) Nonce
forall era.
(EraPParams era, ProtVerAtMost era 6) =>
Lens' (PParams era) Nonce
Lens' (PParams era) Nonce
ppExtraEntropyL) 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) Word64
cs' Nonce
etaV' Nonce
etaC' <-
          forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(PRTCL MockCrypto) (RuleContext 'Transition (PRTCL MockCrypto)
 -> Rule (CHAIN era) 'Transition (State (PRTCL MockCrypto)))
-> RuleContext 'Transition (PRTCL MockCrypto)
-> Rule (CHAIN era) 'Transition (State (PRTCL MockCrypto))
forall a b. (a -> b) -> a -> b
$
            (Environment (PRTCL MockCrypto), State (PRTCL MockCrypto),
 Signal (PRTCL MockCrypto))
-> TRC (PRTCL MockCrypto)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC
              ( UnitInterval -> PoolDistr -> GenDelegs -> Nonce -> PrtclEnv
PrtclEnv (PParams era
pp' PParams era
-> Getting UnitInterval (PParams era) UnitInterval -> UnitInterval
forall s a. s -> Getting a s a -> a
^. Getting UnitInterval (PParams era) UnitInterval
forall era.
(EraPParams era, ProtVerAtMost era 6) =>
Lens' (PParams era) UnitInterval
Lens' (PParams era) UnitInterval
ppDL) PoolDistr
_pd GenDelegs
genDelegs Nonce
eta0'
              , Map (KeyHash 'BlockIssuer) Word64 -> Nonce -> Nonce -> PrtclState
PrtclState Map (KeyHash 'BlockIssuer) Word64
cs Nonce
etaV Nonce
etaC
              , BHeader MockCrypto
Signal (PRTCL MockCrypto)
bh
              )

        BbodyState State (EraRule "LEDGERS" era)
ls' BlocksMade
bcur' <-
          forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @(EraRule "BBODY" era) (RuleContext 'Transition (EraRule "BBODY" era)
 -> Rule (CHAIN era) 'Transition (State (EraRule "BBODY" era)))
-> RuleContext 'Transition (EraRule "BBODY" era)
-> Rule (CHAIN era) 'Transition (State (EraRule "BBODY" era))
forall a b. (a -> b) -> a -> b
$
            (Environment (EraRule "BBODY" era), State (EraRule "BBODY" era),
 Signal (EraRule "BBODY" era))
-> TRC (EraRule "BBODY" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (PParams era -> ChainAccountState -> BbodyEnv era
forall era. PParams era -> ChainAccountState -> BbodyEnv era
BbodyEnv PParams era
pp' ChainAccountState
account, State (EraRule "LEDGERS" era)
-> BlocksMade -> ShelleyBbodyState era
forall era.
State (EraRule "LEDGERS" era)
-> BlocksMade -> ShelleyBbodyState era
BbodyState State (EraRule "LEDGERS" era)
LedgerState era
ls BlocksMade
bcur, BHeaderView -> TxSeq era -> Block BHeaderView era
forall h era. h -> TxSeq era -> Block h era
Block BHeaderView
bhView TxSeq era
txs)

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

        ChainState era
-> F (Clause (CHAIN era) 'Transition) (ChainState era)
forall a. a -> F (Clause (CHAIN era) 'Transition) a
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) Word64
-> Nonce
-> Nonce
-> Nonce
-> Nonce
-> WithOrigin LastAppliedBlock
-> ChainState era
forall era.
NewEpochState era
-> Map (KeyHash 'BlockIssuer) Word64
-> Nonce
-> Nonce
-> Nonce
-> Nonce
-> WithOrigin LastAppliedBlock
-> ChainState era
ChainState NewEpochState era
nes'' Map (KeyHash 'BlockIssuer) Word64
cs' Nonce
eta0' Nonce
etaV' Nonce
etaC' Nonce
etaH' WithOrigin LastAppliedBlock
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 = PredicateFailure (EraRule "BBODY" era)
-> TestChainPredicateFailure era
PredicateFailure (ShelleyBBODY era) -> PredicateFailure (CHAIN era)
forall era.
PredicateFailure (EraRule "BBODY" era)
-> TestChainPredicateFailure era
BbodyFailure
  wrapEvent :: Event (ShelleyBBODY era) -> Event (CHAIN era)
wrapEvent = Event (EraRule "BBODY" era) -> ChainEvent era
Event (ShelleyBBODY era) -> Event (CHAIN era)
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 = PredicateFailure (EraRule "TICKN" era)
-> TestChainPredicateFailure era
PredicateFailure TICKN -> PredicateFailure (CHAIN era)
forall era.
PredicateFailure (EraRule "TICKN" era)
-> TestChainPredicateFailure era
TicknFailure
  wrapEvent :: Event TICKN -> Event (CHAIN era)
wrapEvent = Event (EraRule "TICKN" era) -> ChainEvent era
Event TICKN -> Event (CHAIN era)
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 = PredicateFailure (EraRule "TICK" era)
-> TestChainPredicateFailure era
PredicateFailure (ShelleyTICK era) -> PredicateFailure (CHAIN era)
forall era.
PredicateFailure (EraRule "TICK" era)
-> TestChainPredicateFailure era
TickFailure
  wrapEvent :: Event (ShelleyTICK era) -> Event (CHAIN era)
wrapEvent = Event (EraRule "TICK" era) -> ChainEvent era
Event (ShelleyTICK era) -> Event (CHAIN era)
forall era. Event (EraRule "TICK" era) -> ChainEvent era
TickEvent

instance Era era => Embed (PRTCL MockCrypto) (CHAIN era) where
  wrapFailed :: PredicateFailure (PRTCL MockCrypto) -> PredicateFailure (CHAIN era)
wrapFailed = PredicateFailure (PRTCL MockCrypto) -> PredicateFailure (CHAIN era)
PredicateFailure (PRTCL MockCrypto)
-> TestChainPredicateFailure era
forall era.
PredicateFailure (PRTCL MockCrypto)
-> TestChainPredicateFailure era
PrtclFailure
  wrapEvent :: Event (PRTCL MockCrypto) -> Event (CHAIN era)
wrapEvent = Event (PRTCL MockCrypto) -> Event (CHAIN era)
Event (PRTCL MockCrypto) -> ChainEvent era
forall era. Event (PRTCL MockCrypto) -> ChainEvent era
PrtclEvent

-- | Calculate the total ada pots in the chain state
totalAdaPots ::
  ( EraTxOut era
  , EraGov era
  , EraCertState era
  ) =>
  ChainState era ->
  AdaPots
totalAdaPots :: forall era.
(EraTxOut era, EraGov era, EraCertState era) =>
ChainState era -> AdaPots
totalAdaPots = EpochState era -> AdaPots
forall era.
(EraTxOut era, EraGov era, EraCertState 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 chain state
totalAda :: (EraTxOut era, EraGov era, EraCertState era) => ChainState era -> Coin
totalAda :: forall era.
(EraTxOut era, EraGov era, EraCertState era) =>
ChainState era -> Coin
totalAda = EpochState era -> Coin
forall era.
(EraTxOut era, EraGov era, EraCertState 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

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

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

instance ToExpr LastAppliedBlock