{-# 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, mkTxIxPartial)
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.LedgerState (
  AccountState (..),
  CertState,
  LedgerState (..),
  UTxOState,
  genesisState,
 )
import Cardano.Ledger.Shelley.Rules (
  DelegsEnv,
  DelplEnv,
  LedgerEnv (..),
  ShelleyDELPL,
  ShelleyDelplPredFailure,
  ShelleyLEDGER,
  ShelleyLEDGERS,
  ShelleyLedgersEnv (..),
  UtxoEnv,
 )
import Cardano.Ledger.Slot (SlotNo (..))
import Cardano.Ledger.UTxO (EraUTxO)
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.ConcreteCryptoTypes (Mock)
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,
 )
import qualified Test.Control.State.Transition.Trace.Generator.QuickCheck as TQC
import Test.QuickCheck (Gen)

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

genAccountState :: Constants -> Gen AccountState
genAccountState :: Constants -> Gen AccountState
genAccountState Constants {Integer
minTreasury :: Constants -> Integer
minTreasury :: Integer
minTreasury, Integer
maxTreasury :: Constants -> Integer
maxTreasury :: Integer
maxTreasury, Integer
minReserves :: Constants -> Integer
minReserves :: Integer
minReserves, Integer
maxReserves :: Constants -> Integer
maxReserves :: Integer
maxReserves} =
  Coin -> Coin -> AccountState
AccountState
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> Integer -> Gen Coin
genCoin Integer
minTreasury Integer
maxTreasury
    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
  ( EraGen era
  , EraGov era
  , EraUTxO era
  , Mock (EraCrypto 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) (ShelleyLEDGER era)
  , Embed (EraRule "UTXOW" era) (ShelleyLEDGER era)
  , Environment (EraRule "UTXOW" era) ~ UtxoEnv era
  , State (EraRule "UTXOW" era) ~ UTxOState era
  , Signal (EraRule "UTXOW" era) ~ Tx era
  , Environment (EraRule "DELEGS" era) ~ DelegsEnv era
  , State (EraRule "DELEGS" era) ~ CertState era
  , Signal (EraRule "DELEGS" era) ~ Seq (TxCert era)
  , ProtVerAtMost era 8
  ) =>
  TQC.HasTrace (ShelleyLEDGER era) (GenEnv era)
  where
  envGen :: HasCallStack => GenEnv era -> Gen (Environment (ShelleyLEDGER era))
envGen GenEnv {Constants
geConstants :: forall era. GenEnv era -> Constants
geConstants :: Constants
geConstants} =
    forall era.
SlotNo
-> TxIx -> PParams era -> AccountState -> Bool -> LedgerEnv era
LedgerEnv (Word64 -> SlotNo
SlotNo Word64
0) forall a. Bounded a => a
minBound
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era. EraGen era => Constants -> Gen (PParams era)
genEraPParams @era Constants
geConstants
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Constants -> Gen AccountState
genAccountState Constants
geConstants
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

  sigGen :: HasCallStack =>
GenEnv era
-> Environment (ShelleyLEDGER era)
-> State (ShelleyLEDGER era)
-> Gen (Signal (ShelleyLEDGER era))
sigGen GenEnv era
genenv Environment (ShelleyLEDGER era)
env State (ShelleyLEDGER era)
state = forall era.
(EraGen era, EraUTxO era, Mock (EraCrypto 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 era -> LedgerEnv era -> LedgerState era -> Gen (Tx era)
genTx GenEnv era
genenv Environment (ShelleyLEDGER era)
env State (ShelleyLEDGER era)
state

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

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

instance
  forall era.
  ( EraGen era
  , EraGov era
  , EraUTxO era
  , Mock (EraCrypto 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) (ShelleyDELPL era)
  , Embed (EraRule "LEDGER" era) (ShelleyLEDGERS era)
  , ProtVerAtMost era 8
  ) =>
  TQC.HasTrace (ShelleyLEDGERS era) (GenEnv era)
  where
  envGen :: HasCallStack =>
GenEnv era -> Gen (Environment (ShelleyLEDGERS era))
envGen GenEnv {Constants
geConstants :: Constants
geConstants :: forall era. GenEnv era -> Constants
geConstants} =
    forall era.
SlotNo -> PParams era -> AccountState -> ShelleyLedgersEnv era
LedgersEnv (Word64 -> SlotNo
SlotNo Word64
0)
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era. EraGen era => Constants -> Gen (PParams era)
genEraPParams @era Constants
geConstants
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Constants -> Gen AccountState
genAccountState Constants
geConstants

  -- a LEDGERS signal is a sequence of LEDGER signals
  sigGen :: HasCallStack =>
GenEnv era
-> Environment (ShelleyLEDGERS era)
-> State (ShelleyLEDGERS era)
-> Gen (Signal (ShelleyLEDGERS era))
sigGen
    ge :: GenEnv era
ge@(GenEnv KeySpace era
_ ScriptSpace era
_ Constants {Word64
maxTxsPerBlock :: Constants -> Word64
maxTxsPerBlock :: Word64
maxTxsPerBlock})
    (LedgersEnv SlotNo
slotNo PParams era
pParams AccountState
reserves)
    State (ShelleyLEDGERS era)
ls = do
      (LedgerState era
_, [Tx era]
txs') <-
        forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM
          HasCallStack =>
(LedgerState era, [Tx era])
-> TxIx -> Gen (LedgerState era, [Tx era])
genAndApplyTx
          (State (ShelleyLEDGERS era)
ls, [])
          [forall a. Bounded a => a
minBound .. HasCallStack => Integer -> TxIx
mkTxIxPartial (forall a. Integral a => a -> Integer
toInteger Word64
maxTxsPerBlock forall a. Num a => a -> a -> a
- Integer
1)]

      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Seq a
Seq.fromList (forall a. [a] -> [a]
reverse [Tx era]
txs') -- reverse Newest first to Oldest first
      where
        genAndApplyTx ::
          HasCallStack =>
          (LedgerState era, [Tx era]) ->
          TxIx ->
          Gen (LedgerState era, [Tx era])
        genAndApplyTx :: HasCallStack =>
(LedgerState era, [Tx era])
-> TxIx -> Gen (LedgerState era, [Tx era])
genAndApplyTx (LedgerState era
ls', [Tx era]
txs) TxIx
txIx = do
          let ledgerEnv :: LedgerEnv era
ledgerEnv = forall era.
SlotNo
-> TxIx -> PParams era -> AccountState -> Bool -> LedgerEnv era
LedgerEnv SlotNo
slotNo TxIx
txIx PParams era
pParams AccountState
reserves Bool
False
          Tx era
tx <- forall era.
(EraGen era, EraUTxO era, Mock (EraCrypto 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 era -> LedgerEnv era -> LedgerState era -> Gen (Tx era)
genTx GenEnv era
ge LedgerEnv era
ledgerEnv LedgerState era
ls'

          let res :: Either
  (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
  (LedgerState era)
res =
                forall a. ShelleyBase a -> a
runShelleyBase 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)
                    (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (LedgerEnv era
ledgerEnv, LedgerState era
ls', Tx era
tx))
          case Either
  (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
  (LedgerState era)
res of
            Left NonEmpty (PredicateFailure (EraRule "LEDGER" era))
pf -> forall a. HasCallStack => [Char] -> a
error ([Char]
"LEDGER sigGen: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> [Char]
show NonEmpty (PredicateFailure (EraRule "LEDGER" era))
pf)
            Right LedgerState era
ls'' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (LedgerState era
ls'', Tx era
tx forall a. a -> [a] -> [a]
: [Tx era]
txs)

  shrinkSignal :: HasCallStack =>
Signal (ShelleyLEDGERS era) -> [Signal (ShelleyLEDGERS era)]
shrinkSignal = forall a b. a -> b -> a
const []

  type BaseEnv (ShelleyLEDGERS era) = Globals
  interpretSTS :: forall a.
HasCallStack =>
BaseEnv (ShelleyLEDGERS era) -> BaseM (ShelleyLEDGERS era) a -> a
interpretSTS BaseEnv (ShelleyLEDGERS era)
globals BaseM (ShelleyLEDGERS era) a
act = forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT BaseM (ShelleyLEDGERS era) a
act BaseEnv (ShelleyLEDGERS 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.
  ( EraGen era
  , EraGov era
  ) =>
  GenEnv era ->
  IRC ledger ->
  Gen (Either a (LedgerState era))
mkGenesisLedgerState :: forall a era ledger.
(EraGen era, EraGov era) =>
GenEnv era -> IRC ledger -> Gen (Either a (LedgerState era))
mkGenesisLedgerState ge :: GenEnv era
ge@(GenEnv KeySpace era
_ ScriptSpace era
_ Constants
c) IRC ledger
_ =
  forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
EraGov era =>
Map
  (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
-> UTxO era -> LedgerState era
genesisState (forall c.
Crypto c =>
Constants -> Map (KeyHash 'Genesis c) (GenDelegPair c)
genesisDelegs0 Constants
c) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era. EraGen era => GenEnv era -> Gen (UTxO era)
genUtxo0 GenEnv era
ge