{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
-- HasTrace instances for AlonzoLEDGE
{-# OPTIONS_GHC -fno-warn-orphans #-}

-- | Export HasTrace instance for AlonzoLEDGE Alonzo Era.
module Test.Cardano.Ledger.Alonzo.Trace () where

import Cardano.Ledger.Alonzo.Core
import Cardano.Ledger.Alonzo.Rules (LEDGER, LEDGERS)
import Cardano.Ledger.BaseTypes (Globals, epochInfo, systemStart)
import Cardano.Ledger.Shelley.API.Mempool (ApplyTx (..))
import Cardano.Ledger.Shelley.LedgerState (UTxOState, lsUTxOState, utxosUtxo)
import qualified Cardano.Ledger.Shelley.Rules as Shelley
import Cardano.Ledger.Shelley.State
import Cardano.Protocol.Crypto (Crypto)
import Cardano.Slotting.Slot (EpochNo (..), SlotNo (..))
import Control.Monad.Trans.Reader (runReaderT)
import Control.State.Transition
import Data.Functor.Identity (runIdentity)
import Data.Sequence (Seq)
import Test.Cardano.Ledger.Alonzo.AlonzoEraGen ()
import Test.Cardano.Ledger.Shelley.Generator.Core (GenEnv (..))
import Test.Cardano.Ledger.Shelley.Generator.EraGen (EraGen (..), MinLEDGER_STS)
import Test.Cardano.Ledger.Shelley.Generator.ShelleyEraGen ()
import Test.Cardano.Ledger.Shelley.Generator.Trace.Ledger (
  genAccountState,
  ledgersSigGen,
 )
import Test.Cardano.Ledger.Shelley.Generator.Trace.TxCert (CERTS)
import Test.Cardano.Ledger.Shelley.Generator.Utxo (genTx)
import Test.Cardano.Ledger.Shelley.Utils (testGlobals)
import qualified Test.Control.State.Transition.Trace.Generator.QuickCheck as TQC

-- The LEDGER STS combines utxo and delegation rules and allows for generating transactions
-- with meaningful delegation certificates.
instance
  ( ApplyTx era
  , EraGen era
  , EraGov era
  , EraUTxO era
  , AlonzoEraTx era
  , ShelleyEraAccounts era
  , MinLEDGER_STS era
  , Embed (EraRule "DELPL" era) (CERTS era)
  , Environment (EraRule "DELPL" era) ~ Shelley.DelplEnv era
  , State (EraRule "DELPL" era) ~ CertState era
  , Signal (EraRule "DELPL" era) ~ TxCert era
  , PredicateFailure (EraRule "DELPL" era) ~ Shelley.ShelleyDelplPredFailure era
  , Embed (EraRule "DELEGS" era) (LEDGER era)
  , Embed (EraRule "UTXOW" era) (LEDGER era)
  , Environment (EraRule "UTXOW" era) ~ Shelley.UtxoEnv era
  , State (EraRule "UTXOW" era) ~ UTxOState era
  , Signal (EraRule "UTXOW" era) ~ StAnnTx TopTx era
  , Environment (EraRule "DELEGS" era) ~ Shelley.DelegsEnv era
  , State (EraRule "DELEGS" era) ~ CertState era
  , Signal (EraRule "DELEGS" era) ~ Seq (TxCert era)
  , AtMostEra "Babbage" era
  , EraCertState era
  , Crypto c
  , EraRuleFailure "LEDGER" era ~ Shelley.ShelleyLedgerPredFailure era
  , EraRule "LEDGER" era ~ LEDGER era
  ) =>
  TQC.HasTrace (LEDGER era) (GenEnv c era)
  where
  envGen :: HasCallStack => GenEnv c era -> Gen (Environment (LEDGER era))
envGen GenEnv {Constants
geConstants :: Constants
geConstants :: forall c era. GenEnv c era -> Constants
geConstants} =
    SlotNo
-> Maybe EpochNo
-> TxIx
-> PParams era
-> ChainAccountState
-> LedgerEnv era
forall era.
SlotNo
-> Maybe EpochNo
-> TxIx
-> PParams era
-> ChainAccountState
-> LedgerEnv era
Shelley.LedgerEnv (Word64 -> SlotNo
SlotNo Word64
0) Maybe EpochNo
forall a. Maybe a
Nothing TxIx
forall a. Bounded a => a
minBound
      (PParams era -> ChainAccountState -> LedgerEnv era)
-> Gen (PParams era) -> Gen (ChainAccountState -> LedgerEnv era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era. EraGen era => Constants -> Gen (PParams era)
genEraPParams @era Constants
geConstants
      Gen (ChainAccountState -> LedgerEnv era)
-> Gen ChainAccountState -> Gen (LedgerEnv era)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Constants -> Gen ChainAccountState
genAccountState Constants
geConstants

  sigGen :: HasCallStack =>
GenEnv c era
-> Environment (LEDGER era)
-> State (LEDGER era)
-> Gen (Signal (LEDGER era))
sigGen GenEnv c era
ge ledgerEnv :: Environment (LEDGER era)
ledgerEnv@(Shelley.LedgerEnv SlotNo
_ Maybe EpochNo
_ TxIx
_ PParams era
pParams ChainAccountState
_) State (LEDGER era)
ls = do
    tx <- GenEnv c era
-> LedgerEnv era -> LedgerState era -> Gen (Tx TopTx era)
forall era c.
(EraGen era, EraUTxO era, ShelleyEraAccounts era,
 Embed (EraRule "DELPL" era) (CERTS era),
 Environment (EraRule "DELPL" era) ~ DelplEnv era,
 State (EraRule "DELPL" era) ~ CertState era,
 Signal (EraRule "DELPL" era) ~ TxCert era, Crypto c) =>
GenEnv c era
-> LedgerEnv era -> LedgerState era -> Gen (Tx TopTx era)
genTx GenEnv c era
ge LedgerEnv era
Environment (LEDGER era)
ledgerEnv State (LEDGER era)
LedgerState era
ls
    pure $
      mkStAnnTx
        (epochInfo testGlobals)
        (systemStart testGlobals)
        pParams
        (utxosUtxo (lsUTxOState ls))
        tx

  shrinkSignal :: HasCallStack => Signal (LEDGER era) -> [Signal (LEDGER era)]
shrinkSignal Signal (LEDGER era)
_ = [] -- TODO add some kind of Shrinker?

  type BaseEnv (LEDGER era) = Globals
  interpretSTS :: forall a.
HasCallStack =>
BaseEnv (LEDGER era) -> BaseM (LEDGER era) a -> a
interpretSTS BaseEnv (LEDGER era)
globals BaseM (LEDGER era) a
act = Identity a -> a
forall a. Identity a -> a
runIdentity (Identity a -> a) -> Identity a -> a
forall a b. (a -> b) -> a -> b
$ ReaderT Globals Identity a -> Globals -> Identity a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT Globals Identity a
BaseM (LEDGER era) a
act Globals
BaseEnv (LEDGER era)
globals

instance
  ( Crypto c
  , ApplyTx era
  , EraGen era
  , EraGov era
  , EraUTxO era
  , EraStake era
  , EraCertState era
  , ShelleyEraAccounts era
  , MinLEDGER_STS era
  , Embed (EraRule "DELPL" era) (CERTS era)
  , Environment (EraRule "DELPL" era) ~ Shelley.DelplEnv era
  , State (EraRule "DELPL" era) ~ CertState era
  , Signal (EraRule "DELPL" era) ~ TxCert era
  , PredicateFailure (EraRule "DELPL" era) ~ Shelley.ShelleyDelplPredFailure era
  , Embed (EraRule "DELEG" era) (Shelley.DELPL era)
  , Embed (EraRule "LEDGER" era) (LEDGERS era)
  , AtMostEra "Babbage" era
  ) =>
  TQC.HasTrace (LEDGERS era) (GenEnv c era)
  where
  envGen :: HasCallStack => GenEnv c era -> Gen (Environment (LEDGERS era))
envGen GenEnv {Constants
geConstants :: forall c era. GenEnv c era -> Constants
geConstants :: Constants
geConstants} =
    SlotNo
-> EpochNo
-> PParams era
-> ChainAccountState
-> ShelleyLedgersEnv era
forall era.
SlotNo
-> EpochNo
-> PParams era
-> ChainAccountState
-> ShelleyLedgersEnv era
Shelley.LedgersEnv (Word64 -> SlotNo
SlotNo Word64
0) (Word64 -> EpochNo
EpochNo Word64
0)
      (PParams era -> ChainAccountState -> ShelleyLedgersEnv era)
-> Gen (PParams era)
-> Gen (ChainAccountState -> ShelleyLedgersEnv era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era. EraGen era => Constants -> Gen (PParams era)
genEraPParams @era Constants
geConstants
      Gen (ChainAccountState -> ShelleyLedgersEnv era)
-> Gen ChainAccountState -> Gen (ShelleyLedgersEnv era)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Constants -> Gen ChainAccountState
genAccountState Constants
geConstants

  sigGen :: HasCallStack =>
GenEnv c era
-> Environment (LEDGERS era)
-> State (LEDGERS era)
-> Gen (Signal (LEDGERS era))
sigGen = GenEnv c era
-> ShelleyLedgersEnv era
-> LedgerState era
-> Gen (Seq (Tx TopTx era))
GenEnv c era
-> Environment (LEDGERS era)
-> State (LEDGERS era)
-> Gen (Signal (LEDGERS era))
forall c era.
(Crypto c, ApplyTx era, EraGen era, EraUTxO era,
 ShelleyEraAccounts era, MinLEDGER_STS era,
 Embed (EraRule "DELPL" era) (CERTS era),
 Environment (EraRule "DELPL" era) ~ DelplEnv era,
 State (EraRule "DELPL" era) ~ CertState era,
 Signal (EraRule "DELPL" era) ~ TxCert era) =>
GenEnv c era
-> ShelleyLedgersEnv era
-> LedgerState era
-> Gen (Seq (Tx TopTx era))
ledgersSigGen
  shrinkSignal :: HasCallStack => Signal (LEDGERS era) -> [Signal (LEDGERS era)]
shrinkSignal = [Seq (Tx TopTx era)] -> Seq (Tx TopTx era) -> [Seq (Tx TopTx era)]
forall a b. a -> b -> a
const []

  type BaseEnv (LEDGERS era) = Globals
  interpretSTS :: forall a.
HasCallStack =>
BaseEnv (LEDGERS era) -> BaseM (LEDGERS era) a -> a
interpretSTS BaseEnv (LEDGERS era)
globals BaseM (LEDGERS era) a
act = Identity a -> a
forall a. Identity a -> a
runIdentity (Identity a -> a) -> Identity a -> a
forall a b. (a -> b) -> a -> b
$ ReaderT Globals Identity a -> Globals -> Identity a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT Globals Identity a
BaseM (LEDGERS era) a
act Globals
BaseEnv (LEDGERS era)
globals