{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
-- The HasTrace instance relies on test generators and so cannot
-- be included with the LEDGER STS
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Shelley.Generator.Trace.Ledger where

import Cardano.Ledger.BaseTypes (Globals, TxIx, epochInfo, mkTxIxPartial, systemStart)
import Cardano.Ledger.Shelley.API.Mempool (ApplyTx (..))
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.LedgerState (
  LedgerState (..),
  UTxOState,
  genesisState,
  lsUTxOState,
  utxosUtxo,
 )
import Cardano.Ledger.Shelley.Rules (
  DELPL,
  DelegsEnv,
  DelplEnv,
  LEDGER,
  LEDGERS,
  LedgerEnv (..),
  ShelleyDelplPredFailure,
  ShelleyLedgersEnv (..),
  UtxoEnv,
 )
import Cardano.Ledger.Shelley.State
import Cardano.Ledger.Slot (EpochNo (..), SlotNo (..))
import Cardano.Protocol.Crypto (Crypto)
import Control.Monad (foldM)
import Control.Monad.Trans.Reader (runReaderT)
import Control.State.Transition
import Data.Functor.Identity (runIdentity)
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import GHC.Stack
import Test.Cardano.Ledger.Shelley.Constants (Constants (..))
import Test.Cardano.Ledger.Shelley.Generator.Core (GenEnv (..), genCoin)
import Test.Cardano.Ledger.Shelley.Generator.EraGen (
  EraGen (..),
  MinLEDGER_STS,
  genUtxo0,
 )
import Test.Cardano.Ledger.Shelley.Generator.Presets (genesisDelegs0)
import Test.Cardano.Ledger.Shelley.Generator.Trace.TxCert (CERTS)
import Test.Cardano.Ledger.Shelley.Generator.Utxo (genTx)
import Test.Cardano.Ledger.Shelley.Utils (
  applySTSTest,
  runShelleyBase,
  testGlobals,
 )
import qualified Test.Control.State.Transition.Trace.Generator.QuickCheck as TQC
import Test.QuickCheck (Gen)

-- ======================================================

genAccountState :: Constants -> Gen ChainAccountState
genAccountState :: Constants -> Gen ChainAccountState
genAccountState Constants {Integer
minTreasury :: Integer
minTreasury :: Constants -> Integer
minTreasury, Integer
maxTreasury :: Integer
maxTreasury :: Constants -> Integer
maxTreasury, Integer
minReserves :: Integer
minReserves :: Constants -> Integer
minReserves, Integer
maxReserves :: Integer
maxReserves :: Constants -> Integer
maxReserves} =
  Coin -> Coin -> ChainAccountState
ChainAccountState
    (Coin -> Coin -> ChainAccountState)
-> Gen Coin -> Gen (Coin -> ChainAccountState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> Integer -> Gen Coin
genCoin Integer
minTreasury Integer
maxTreasury
    Gen (Coin -> ChainAccountState)
-> Gen Coin -> Gen ChainAccountState
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Integer -> Integer -> Gen Coin
genCoin Integer
minReserves Integer
maxReserves

-- 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
  , EraCertState 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
  , PredicateFailure (EraRule "DELPL" era) ~ ShelleyDelplPredFailure era
  , Embed (EraRule "DELEGS" era) (LEDGER era)
  , Embed (EraRule "UTXOW" era) (LEDGER era)
  , Environment (EraRule "UTXOW" era) ~ UtxoEnv era
  , State (EraRule "UTXOW" era) ~ UTxOState era
  , Signal (EraRule "UTXOW" era) ~ StAnnTx TopTx era
  , Environment (EraRule "DELEGS" era) ~ DelegsEnv era
  , State (EraRule "DELEGS" era) ~ CertState era
  , Signal (EraRule "DELEGS" era) ~ Seq (TxCert era)
  , AtMostEra "Babbage" era
  , EraRule "LEDGER" era ~ LEDGER era
  , Crypto c
  ) =>
  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
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@(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

ledgersSigGen ::
  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 :: 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
  ge :: GenEnv c era
ge@(GenEnv KeySpace c era
_ ScriptSpace era
_ Constants {Word64
maxTxsPerBlock :: Word64
maxTxsPerBlock :: Constants -> Word64
maxTxsPerBlock})
  (LedgersEnv SlotNo
slotNo EpochNo
epochNo PParams era
pParams ChainAccountState
reserves)
  LedgerState era
ls = do
    (_, txs') <-
      ((LedgerState era, [Tx TopTx era])
 -> TxIx -> Gen (LedgerState era, [Tx TopTx era]))
-> (LedgerState era, [Tx TopTx era])
-> [TxIx]
-> Gen (LedgerState era, [Tx TopTx era])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM
        HasCallStack =>
(LedgerState era, [Tx TopTx era])
-> TxIx -> Gen (LedgerState era, [Tx TopTx era])
(LedgerState era, [Tx TopTx era])
-> TxIx -> Gen (LedgerState era, [Tx TopTx era])
genAndApplyTx
        (LedgerState era
ls, [])
        [TxIx
forall a. Bounded a => a
minBound .. HasCallStack => Integer -> TxIx
Integer -> TxIx
mkTxIxPartial (Word64 -> Integer
forall a. Integral a => a -> Integer
toInteger Word64
maxTxsPerBlock Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)]

    pure $ Seq.fromList (reverse txs') -- reverse Newest first to Oldest first
    where
      genAndApplyTx ::
        HasCallStack =>
        (LedgerState era, [Tx TopTx era]) ->
        TxIx ->
        Gen (LedgerState era, [Tx TopTx era])
      genAndApplyTx :: HasCallStack =>
(LedgerState era, [Tx TopTx era])
-> TxIx -> Gen (LedgerState era, [Tx TopTx era])
genAndApplyTx (LedgerState era
ls', [Tx TopTx era]
txs) TxIx
txIx = do
        let ledgerEnv :: LedgerEnv era
ledgerEnv = SlotNo
-> Maybe EpochNo
-> TxIx
-> PParams era
-> ChainAccountState
-> LedgerEnv era
forall era.
SlotNo
-> Maybe EpochNo
-> TxIx
-> PParams era
-> ChainAccountState
-> LedgerEnv era
LedgerEnv SlotNo
slotNo (EpochNo -> Maybe EpochNo
forall a. a -> Maybe a
Just EpochNo
epochNo) TxIx
txIx PParams era
pParams ChainAccountState
reserves
        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
ledgerEnv LedgerState era
ls'

        let utxo = UTxOState era -> UTxO era
forall era. UTxOState era -> UTxO era
utxosUtxo (LedgerState era -> UTxOState era
forall era. LedgerState era -> UTxOState era
lsUTxOState LedgerState era
ls')
            stAnnTx =
              EpochInfo (Either Text)
-> SystemStart
-> PParams era
-> UTxO era
-> Tx TopTx era
-> StAnnTx TopTx era
forall era.
ApplyTx era =>
EpochInfo (Either Text)
-> SystemStart
-> PParams era
-> UTxO era
-> Tx TopTx era
-> StAnnTx TopTx era
mkStAnnTx
                (Globals -> EpochInfo (Either Text)
epochInfo Globals
testGlobals)
                (Globals -> SystemStart
systemStart Globals
testGlobals)
                PParams era
pParams
                UTxO era
utxo
                Tx TopTx era
tx
            res =
              ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
     (LedgerState era))
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
     (LedgerState era)
forall a. ShelleyBase a -> a
runShelleyBase (ShelleyBase
   (Either
      (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
      (LedgerState era))
 -> Either
      (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
      (LedgerState era))
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
        (LedgerState era))
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
     (LedgerState era)
forall a b. (a -> b) -> a -> b
$
                forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest @(EraRule "LEDGER" era)
                  ((Environment (EraRule "LEDGER" era), State (EraRule "LEDGER" era),
 Signal (EraRule "LEDGER" era))
-> TRC (EraRule "LEDGER" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (LedgerEnv era
Environment (EraRule "LEDGER" era)
ledgerEnv, State (EraRule "LEDGER" era)
LedgerState era
ls', StAnnTx TopTx era
Signal (EraRule "LEDGER" era)
stAnnTx))
        case res of
          Left NonEmpty (PredicateFailure (EraRule "LEDGER" era))
pf -> [Char] -> Gen (LedgerState era, [Tx TopTx era])
forall a. HasCallStack => [Char] -> a
error ([Char]
"LEDGER sigGen: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> NonEmpty (PredicateFailure (EraRule "LEDGER" era)) -> [Char]
forall a. Show a => a -> [Char]
show NonEmpty (PredicateFailure (EraRule "LEDGER" era))
pf)
          Right LedgerState era
ls'' -> (LedgerState era, [Tx TopTx era])
-> Gen (LedgerState era, [Tx TopTx era])
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LedgerState era
ls'', Tx TopTx era
tx Tx TopTx era -> [Tx TopTx era] -> [Tx TopTx era]
forall a. a -> [a] -> [a]
: [Tx TopTx era]
txs)

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) ~ DelplEnv era
  , State (EraRule "DELPL" era) ~ CertState era
  , Signal (EraRule "DELPL" era) ~ TxCert era
  , PredicateFailure (EraRule "DELPL" era) ~ ShelleyDelplPredFailure era
  , Embed (EraRule "DELEG" era) (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
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

  -- a LEDGERS signal is a sequence of LEDGER signals
  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

-- | Generate initial state for the LEDGER STS using the STS environment.
--
-- Note: this function must be usable in place of 'applySTS' and needs to align
-- with the signature 'RuleContext sts -> Gen (Either [[PredicateFailure sts]] (State sts))'.
-- To achieve this we (1) use 'IRC LEDGER' (the "initial rule context") instead of simply 'LedgerEnv'
-- and (2) always return Right (since this function does not raise predicate failures).
mkGenesisLedgerState ::
  forall a era ledger c.
  ( EraGen era
  , EraGov era
  , EraStake era
  ) =>
  GenEnv c era ->
  IRC ledger ->
  Gen (Either a (LedgerState era))
mkGenesisLedgerState :: forall a era ledger c.
(EraGen era, EraGov era, EraStake era) =>
GenEnv c era -> IRC ledger -> Gen (Either a (LedgerState era))
mkGenesisLedgerState ge :: GenEnv c era
ge@(GenEnv KeySpace c era
_ ScriptSpace era
_ Constants
c) IRC ledger
_ =
  LedgerState era -> Either a (LedgerState era)
forall a b. b -> Either a b
Right (LedgerState era -> Either a (LedgerState era))
-> (UTxO era -> LedgerState era)
-> UTxO era
-> Either a (LedgerState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (KeyHash GenesisRole) GenDelegPair
-> UTxO era -> LedgerState era
forall era.
(EraGov era, EraCertState era, EraStake era) =>
Map (KeyHash GenesisRole) GenDelegPair
-> UTxO era -> LedgerState era
genesisState (Constants -> Map (KeyHash GenesisRole) GenDelegPair
genesisDelegs0 Constants
c) (UTxO era -> Either a (LedgerState era))
-> Gen (UTxO era) -> Gen (Either a (LedgerState era))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenEnv c era -> Gen (UTxO era)
forall era c. EraGen era => GenEnv c era -> Gen (UTxO era)
genUtxo0 GenEnv c era
ge