{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Generic.Trace where

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

import Cardano.Ledger.Address (Addr (..))
import Cardano.Ledger.Alonzo.Rules (AlonzoUtxowPredFailure (..))
import Cardano.Ledger.Babbage.Rules (BabbageUtxowPredFailure (..))
import Cardano.Ledger.BaseTypes (BlocksMade (..), Globals)
import Cardano.Ledger.Coin (CompactForm (CompactCoin))
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.LedgerState (
  EpochState (..),
  LedgerState (..),
  NewEpochState (..),
  StashedAVVMAddresses,
  UTxOState (..),
  curPParamsEpochStateL,
  esLStateL,
  lsCertStateL,
  prevPParamsEpochStateL,
 )
import Cardano.Ledger.Shelley.Rules (
  ShelleyLedgerPredFailure (..),
  ShelleyLedgersPredFailure (..),
  ShelleyUtxowPredFailure (ScriptWitnessNotValidatingUTXOW),
 )
import Cardano.Ledger.Shelley.State
import Cardano.Slotting.Slot (EpochNo (..), SlotNo (..))
import Control.Monad (forM)
import Control.Monad.Trans.Class (MonadTrans (lift))
import Control.Monad.Trans.RWS.Strict (get, gets)
import Control.Monad.Trans.Reader (ReaderT (..))
import qualified Control.State.Transition as STS
import Control.State.Transition.Extended (IRC (), STS (..), TRC (..))
import Data.Default (Default (def))
import Data.Foldable (Foldable (..))
import qualified Data.Foldable as Fold
import Data.Functor.Identity (Identity (runIdentity))
import Data.List.NonEmpty (NonEmpty)
import qualified Data.Map.Strict as Map
import Data.Maybe.Strict (StrictMaybe (..))
import Data.Sequence.Strict (StrictSeq (..))
import qualified Data.Sequence.Strict as SS
import qualified Data.Set as Set
import Data.TreeDiff
import Data.Vector (Vector, (!))
import qualified Data.Vector as Vector
import qualified Debug.Trace as Debug
import GHC.Word (Word64)
import Lens.Micro ((&), (.~), (^.))
import Test.Cardano.Ledger.Alonzo.Era
import Test.Cardano.Ledger.Common
import Test.Cardano.Ledger.Examples.STSTestUtils (EraModel (..))
import Test.Cardano.Ledger.Generic.Functions (
  adaPots,
  totalAda,
 )
import Test.Cardano.Ledger.Generic.GenState (
  EraGenericGen,
  GenEnv (..),
  GenRS,
  GenSize (..),
  GenState (..),
  defaultGenSize,
  getBlocksizeMax,
  getReserves,
  getSlot,
  getSlotDelta,
  getTreasury,
  initStableFields,
  initialLedgerState,
  modifyModel,
  runGenRS,
 )
import Test.Cardano.Ledger.Generic.Instances ()
import Test.Cardano.Ledger.Generic.MockChain
import Test.Cardano.Ledger.Generic.ModelState (MUtxo, stashedAVVMAddressesZero)
import Test.Cardano.Ledger.Generic.Proof hiding (lift)
import Test.Cardano.Ledger.Generic.TxGen (genAlonzoTx)
import Test.Cardano.Ledger.Shelley.Rules.IncrementalStake (stakeDistr)
import Test.Cardano.Ledger.Shelley.Utils (applySTSTest, runShelleyBase, testGlobals)
import Test.Control.State.Transition.Trace (Trace (..), lastState, splitTrace)
import Test.Control.State.Transition.Trace.Generator.QuickCheck (HasTrace (..), traceFromInitState)

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

-- | Generate a Tx and an internal Model of the state after the tx
--   has been applied. That model can be used to generate the next Tx
genRsTxAndModel ::
  forall era.
  EraGenericGen era =>
  Int -> SlotNo -> GenRS era (Tx TopTx era)
genRsTxAndModel :: forall era.
EraGenericGen era =>
Int -> SlotNo -> GenRS era (Tx TopTx era)
genRsTxAndModel Int
n SlotNo
slot = do
  (_, tx) <- SlotNo -> GenRS era (UTxO era, Tx TopTx era)
forall era.
EraGenericGen era =>
SlotNo -> GenRS era (UTxO era, Tx TopTx era)
genAlonzoTx SlotNo
slot
  modifyModel (\ModelNewEpochState era
model -> Int
-> SlotNo
-> ModelNewEpochState era
-> Tx TopTx era
-> ModelNewEpochState era
forall era.
EraModel era =>
Int -> SlotNo -> Model era -> Tx TopTx era -> Model era
applyTx Int
n SlotNo
slot ModelNewEpochState era
model Tx TopTx era
tx)
  pure tx

-- | Generate a Vector of (StrictSeq (Tx era))  representing a (Vector Block)
genRsTxSeq ::
  forall era.
  EraGenericGen era =>
  Int ->
  Int ->
  [(StrictSeq (Tx TopTx era), SlotNo)] ->
  SlotNo ->
  GenRS era (Vector (StrictSeq (Tx TopTx era), SlotNo))
genRsTxSeq :: forall era.
EraGenericGen era =>
Int
-> Int
-> [(StrictSeq (Tx TopTx era), SlotNo)]
-> SlotNo
-> GenRS era (Vector (StrictSeq (Tx TopTx era), SlotNo))
genRsTxSeq Int
this Int
lastN [(StrictSeq (Tx TopTx era), SlotNo)]
ans SlotNo
_slot | Int
this Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
lastN = do
  Vector (StrictSeq (Tx TopTx era), SlotNo)
-> RWST
     (GenEnv era)
     ()
     (GenState era)
     Gen
     (Vector (StrictSeq (Tx TopTx era), SlotNo))
forall a. a -> RWST (GenEnv era) () (GenState era) Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(StrictSeq (Tx TopTx era), SlotNo)]
-> Vector (StrictSeq (Tx TopTx era), SlotNo)
forall a. [a] -> Vector a
Vector.fromList ([(StrictSeq (Tx TopTx era), SlotNo)]
-> [(StrictSeq (Tx TopTx era), SlotNo)]
forall a. [a] -> [a]
reverse [(StrictSeq (Tx TopTx era), SlotNo)]
ans))
genRsTxSeq Int
this Int
lastN [(StrictSeq (Tx TopTx era), SlotNo)]
ans SlotNo
slot = do
  maxBlockSize <- GenState era -> Integer
forall era. GenState era -> Integer
getBlocksizeMax (GenState era -> Integer)
-> RWST (GenEnv era) () (GenState era) Gen (GenState era)
-> RWST (GenEnv era) () (GenState era) Gen Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RWST (GenEnv era) () (GenState era) Gen (GenState era)
forall w (m :: * -> *) r s. (Monoid w, Monad m) => RWST r w s m s
get
  n <- lift $ choose (2 :: Int, fromIntegral maxBlockSize)
  txs <- forM [0 .. n - 1] (\Int
i -> Int
-> SlotNo -> RWST (GenEnv era) () (GenState era) Gen (Tx TopTx era)
forall era.
EraGenericGen era =>
Int -> SlotNo -> GenRS era (Tx TopTx era)
genRsTxAndModel (Int
this Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i) SlotNo
slot)
  newSlotRange <- gets getSlotDelta
  nextSlotNo <- lift $ SlotNo . (+ unSlotNo slot) <$> choose newSlotRange
  genRsTxSeq (this + n) lastN ((SS.fromList txs, slot) : ans) nextSlotNo

-- | Generate a Vector of Blocks, and an initial LedgerState
genTxSeq ::
  forall era.
  EraGenericGen era =>
  GenSize -> -- Size of things the generated code should adhere to
  Int -> -- The number of Tx in the sequence
  GenRS era () -> -- An arbitrary 'initialization action', to run before we generate the sequence
  -- use (pure ()) if you don't want or need initialization
  Gen (Vector (StrictSeq (Tx TopTx era), SlotNo), GenState era)
genTxSeq :: forall era.
EraGenericGen era =>
GenSize
-> Int
-> GenRS era ()
-> Gen (Vector (StrictSeq (Tx TopTx era), SlotNo), GenState era)
genTxSeq GenSize
gensize Int
numTx GenRS era ()
initialize = do
  GenSize
-> GenRS era (Vector (StrictSeq (Tx TopTx era), SlotNo))
-> Gen (Vector (StrictSeq (Tx TopTx era), SlotNo), GenState era)
forall era a.
EraGenericGen era =>
GenSize -> GenRS era a -> Gen (a, GenState era)
runGenRS GenSize
gensize (GenRS era ()
initialize GenRS era ()
-> GenRS era (Vector (StrictSeq (Tx TopTx era), SlotNo))
-> GenRS era (Vector (StrictSeq (Tx TopTx era), SlotNo))
forall a b.
RWST (GenEnv era) () (GenState era) Gen a
-> RWST (GenEnv era) () (GenState era) Gen b
-> RWST (GenEnv era) () (GenState era) Gen b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Int
-> Int
-> [(StrictSeq (Tx TopTx era), SlotNo)]
-> SlotNo
-> GenRS era (Vector (StrictSeq (Tx TopTx era), SlotNo))
forall era.
EraGenericGen era =>
Int
-> Int
-> [(StrictSeq (Tx TopTx era), SlotNo)]
-> SlotNo
-> GenRS era (Vector (StrictSeq (Tx TopTx era), SlotNo))
genRsTxSeq Int
0 Int
numTx [] (Word64 -> SlotNo
SlotNo Word64
1))

runTest :: IO ()
runTest :: IO ()
runTest = do
  (v, _) <- Gen
  (Vector (StrictSeq (Tx TopTx BabbageEra), SlotNo),
   GenState BabbageEra)
-> IO
     (Vector (StrictSeq (Tx TopTx BabbageEra), SlotNo),
      GenState BabbageEra)
forall a. Gen a -> IO a
generate (Gen
   (Vector (StrictSeq (Tx TopTx BabbageEra), SlotNo),
    GenState BabbageEra)
 -> IO
      (Vector (StrictSeq (Tx TopTx BabbageEra), SlotNo),
       GenState BabbageEra))
-> Gen
     (Vector (StrictSeq (Tx TopTx BabbageEra), SlotNo),
      GenState BabbageEra)
-> IO
     (Vector (StrictSeq (Tx TopTx BabbageEra), SlotNo),
      GenState BabbageEra)
forall a b. (a -> b) -> a -> b
$ forall era.
EraGenericGen era =>
GenSize
-> Int
-> GenRS era ()
-> Gen (Vector (StrictSeq (Tx TopTx era), SlotNo), GenState era)
genTxSeq @BabbageEra GenSize
defaultGenSize Int
20 (() -> GenRS BabbageEra ()
forall a.
a -> RWST (GenEnv BabbageEra) () (GenState BabbageEra) Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
  print (Vector.length v)

-- ==================================================================
-- Constructing the "real", initial NewEpochState, from the GenState

initialMockChainState ::
  forall era.
  (Reflect era, ShelleyEraAccounts era) =>
  GenState era ->
  MockChainState era
initialMockChainState :: forall era.
(Reflect era, ShelleyEraAccounts era) =>
GenState era -> MockChainState era
initialMockChainState GenState era
gstate =
  NewEpochState era
-> NewEpochState era -> SlotNo -> Int -> MockChainState era
forall era.
NewEpochState era
-> NewEpochState era -> SlotNo -> Int -> MockChainState era
MockChainState NewEpochState era
newepochstate NewEpochState era
newepochstate (GenState era -> SlotNo
forall era. GenState era -> SlotNo
getSlot GenState era
gstate) Int
0
  where
    ledgerstate :: LedgerState era
ledgerstate = GenState era -> LedgerState era
forall era. Reflect era => GenState era -> LedgerState era
initialLedgerState GenState era
gstate
    newepochstate :: NewEpochState era
newepochstate =
      NewEpochState
        { nesEL :: EpochNo
nesEL = Word64 -> EpochNo
EpochNo Word64
0
        , nesBprev :: BlocksMade
nesBprev = Map (KeyHash StakePool) Natural -> BlocksMade
BlocksMade Map (KeyHash StakePool) Natural
forall k a. Map k a
Map.empty
        , nesBcur :: BlocksMade
nesBcur = Map (KeyHash StakePool) Natural -> BlocksMade
BlocksMade Map (KeyHash StakePool) Natural
forall k a. Map k a
Map.empty
        , nesEs :: EpochState era
nesEs = GenState era -> LedgerState era -> EpochState era
forall era.
(Reflect era, ShelleyEraAccounts era) =>
GenState era -> LedgerState era -> EpochState era
makeEpochState GenState era
gstate LedgerState era
ledgerstate
        , nesRu :: StrictMaybe PulsingRewUpdate
nesRu = StrictMaybe PulsingRewUpdate
forall a. StrictMaybe a
SNothing
        , nesPd :: PoolDistr
nesPd = Map (KeyHash StakePool) IndividualPoolStake
-> CompactForm Coin -> PoolDistr
PoolDistr (GenState era -> Map (KeyHash StakePool) IndividualPoolStake
forall era.
GenState era -> Map (KeyHash StakePool) IndividualPoolStake
gsInitialPoolDistr GenState era
gstate) (Word64 -> CompactForm Coin
CompactCoin Word64
1)
        , stashedAVVMAddresses :: StashedAVVMAddresses era
stashedAVVMAddresses = Proof era -> StashedAVVMAddresses era
forall era. Proof era -> StashedAVVMAddresses era
stashedAVVMAddressesZero (forall era. Reflect era => Proof era
reify @era)
        }

makeEpochState ::
  (Reflect era, ShelleyEraAccounts era) => GenState era -> LedgerState era -> EpochState era
makeEpochState :: forall era.
(Reflect era, ShelleyEraAccounts era) =>
GenState era -> LedgerState era -> EpochState era
makeEpochState GenState era
gstate LedgerState era
ledgerstate =
  EpochState
    { esChainAccountState :: ChainAccountState
esChainAccountState =
        ChainAccountState
          { casTreasury :: Coin
casTreasury = GenState era -> Coin
forall era. GenState era -> Coin
getTreasury GenState era
gstate
          , casReserves :: Coin
casReserves = GenState era -> Coin
forall era. GenState era -> Coin
getReserves GenState era
gstate
          }
    , esSnapshots :: SnapShots
esSnapshots = LedgerState era -> SnapShots
forall era.
(EraTxOut era, EraCertState era, ShelleyEraAccounts era) =>
LedgerState era -> SnapShots
snaps LedgerState era
ledgerstate
    , esLState :: LedgerState era
esLState = LedgerState era
ledgerstate
    , esNonMyopic :: NonMyopic
esNonMyopic = 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)
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
.~ GenEnv era -> PParams era
forall era. GenEnv era -> PParams era
gePParams (GenState era -> GenEnv era
forall era. GenState era -> GenEnv era
gsGenEnv GenState era
gstate)
    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
.~ GenEnv era -> PParams era
forall era. GenEnv era -> PParams era
gePParams (GenState era -> GenEnv era
forall era. GenState era -> GenEnv era
gsGenEnv GenState era
gstate)

snaps :: (EraTxOut era, EraCertState era, ShelleyEraAccounts era) => LedgerState era -> SnapShots
snaps :: forall era.
(EraTxOut era, EraCertState era, ShelleyEraAccounts era) =>
LedgerState era -> SnapShots
snaps (LedgerState UTxOState {utxosUtxo :: forall era. UTxOState era -> UTxO era
utxosUtxo = UTxO era
u, utxosFees :: forall era. UTxOState era -> Coin
utxosFees = Coin
f} CertState era
certState) =
  SnapShot -> PoolDistr -> SnapShot -> SnapShot -> Coin -> SnapShots
SnapShots SnapShot
snap (SnapShot -> PoolDistr
calculatePoolDistr SnapShot
snap) SnapShot
snap SnapShot
snap Coin
f
  where
    pstate :: PState era
pstate = CertState era
certState CertState era
-> Getting (PState era) (CertState era) (PState era) -> PState era
forall s a. s -> Getting a s a -> a
^. Getting (PState era) (CertState era) (PState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL
    dstate :: DState era
dstate = CertState era
certState CertState era
-> Getting (DState era) (CertState era) (DState era) -> DState era
forall s a. s -> Getting a s a -> a
^. Getting (DState era) (CertState era) (DState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL
    snap :: SnapShot
snap = UTxO era -> DState era -> PState era -> SnapShot
forall era.
(EraTxOut era, ShelleyEraAccounts era) =>
UTxO era -> DState era -> PState era -> SnapShot
stakeDistr UTxO era
u DState era
dstate PState era
pstate

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

raiseMockError ::
  forall era.
  Reflect era =>
  Word64 ->
  SlotNo ->
  EpochState era ->
  NonEmpty (MockChainFailure era) ->
  [Tx TopTx era] ->
  GenState era ->
  String
raiseMockError :: forall era.
Reflect era =>
Word64
-> SlotNo
-> EpochState era
-> NonEmpty (MockChainFailure era)
-> [Tx TopTx era]
-> GenState era
-> String
raiseMockError Word64
slot (SlotNo Word64
next) EpochState era
epochstate NonEmpty (MockChainFailure era)
_pdfs [Tx TopTx era]
_txs GenState era
_ =
  let _ssPoolParams :: Map (KeyHash StakePool) StakePoolState
_ssPoolParams = EpochState era
epochstate EpochState era
-> Getting
     (Map (KeyHash StakePool) StakePoolState)
     (EpochState era)
     (Map (KeyHash StakePool) StakePoolState)
-> Map (KeyHash StakePool) StakePoolState
forall s a. s -> Getting a s a -> a
^. (LedgerState era
 -> Const
      (Map (KeyHash StakePool) StakePoolState) (LedgerState era))
-> EpochState era
-> Const (Map (KeyHash StakePool) StakePoolState) (EpochState era)
forall era (f :: * -> *).
Functor f =>
(LedgerState era -> f (LedgerState era))
-> EpochState era -> f (EpochState era)
esLStateL ((LedgerState era
  -> Const
       (Map (KeyHash StakePool) StakePoolState) (LedgerState era))
 -> EpochState era
 -> Const (Map (KeyHash StakePool) StakePoolState) (EpochState era))
-> ((Map (KeyHash StakePool) StakePoolState
     -> Const
          (Map (KeyHash StakePool) StakePoolState)
          (Map (KeyHash StakePool) StakePoolState))
    -> LedgerState era
    -> Const
         (Map (KeyHash StakePool) StakePoolState) (LedgerState era))
-> Getting
     (Map (KeyHash StakePool) StakePoolState)
     (EpochState era)
     (Map (KeyHash StakePool) StakePoolState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CertState era
 -> Const (Map (KeyHash StakePool) StakePoolState) (CertState era))
-> LedgerState era
-> Const (Map (KeyHash StakePool) StakePoolState) (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL ((CertState era
  -> Const (Map (KeyHash StakePool) StakePoolState) (CertState era))
 -> LedgerState era
 -> Const
      (Map (KeyHash StakePool) StakePoolState) (LedgerState era))
-> ((Map (KeyHash StakePool) StakePoolState
     -> Const
          (Map (KeyHash StakePool) StakePoolState)
          (Map (KeyHash StakePool) StakePoolState))
    -> CertState era
    -> Const (Map (KeyHash StakePool) StakePoolState) (CertState era))
-> (Map (KeyHash StakePool) StakePoolState
    -> Const
         (Map (KeyHash StakePool) StakePoolState)
         (Map (KeyHash StakePool) StakePoolState))
-> LedgerState era
-> Const (Map (KeyHash StakePool) StakePoolState) (LedgerState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PState era
 -> Const (Map (KeyHash StakePool) StakePoolState) (PState era))
-> CertState era
-> Const (Map (KeyHash StakePool) StakePoolState) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL ((PState era
  -> Const (Map (KeyHash StakePool) StakePoolState) (PState era))
 -> CertState era
 -> Const (Map (KeyHash StakePool) StakePoolState) (CertState era))
-> ((Map (KeyHash StakePool) StakePoolState
     -> Const
          (Map (KeyHash StakePool) StakePoolState)
          (Map (KeyHash StakePool) StakePoolState))
    -> PState era
    -> Const (Map (KeyHash StakePool) StakePoolState) (PState era))
-> (Map (KeyHash StakePool) StakePoolState
    -> Const
         (Map (KeyHash StakePool) StakePoolState)
         (Map (KeyHash StakePool) StakePoolState))
-> CertState era
-> Const (Map (KeyHash StakePool) StakePoolState) (CertState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (KeyHash StakePool) StakePoolState
 -> Const
      (Map (KeyHash StakePool) StakePoolState)
      (Map (KeyHash StakePool) StakePoolState))
-> PState era
-> Const (Map (KeyHash StakePool) StakePoolState) (PState era)
forall era (f :: * -> *).
Functor f =>
(Map (KeyHash StakePool) StakePoolState
 -> f (Map (KeyHash StakePool) StakePoolState))
-> PState era -> f (PState era)
psStakePoolsL
   in [Expr] -> String
forall a. Show a => a -> String
show
        [ AdaPots -> Expr
forall a. ToExpr a => a -> Expr
toExpr (AdaPots -> Expr) -> AdaPots -> Expr
forall a b. (a -> b) -> a -> b
$ Proof era -> EpochState era -> AdaPots
forall era. Proof era -> EpochState era -> AdaPots
adaPots Proof era
forall era. Reflect era => Proof era
reify EpochState era
epochstate
        , Word64 -> Expr
forall a. ToExpr a => a -> Expr
toExpr Word64
slot
        , Word64 -> Expr
forall a. ToExpr a => a -> Expr
toExpr Word64
next
        , -- ppString "===================================",
          -- ppString "Real Pool Params\n" <> ppMap pcKeyHash pcPoolParams poolParams,
          PParams era -> Expr
forall a. ToExpr a => a -> Expr
toExpr (EpochState era
epochstate EpochState era
-> Getting (PParams era) (EpochState era) (PParams era)
-> PParams era
forall s a. s -> Getting a s a -> a
^. Getting (PParams era) (EpochState era) (PParams era)
forall era. EraGov era => Lens' (EpochState era) (PParams era)
Lens' (EpochState era) (PParams era)
curPParamsEpochStateL)
        ]

badScripts :: Proof era -> [MockChainFailure era] -> Set.Set ScriptHash
badScripts :: forall era. Proof era -> [MockChainFailure era] -> Set ScriptHash
badScripts Proof era
proof [MockChainFailure era]
xs = (Set ScriptHash -> MockChainFailure era -> Set ScriptHash)
-> Set ScriptHash -> [MockChainFailure era] -> Set ScriptHash
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Fold.foldl' (\Set ScriptHash
s MockChainFailure era
mcf -> Set ScriptHash -> Set ScriptHash -> Set ScriptHash
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set ScriptHash
s (Proof era -> MockChainFailure era -> Set ScriptHash
forall era. Proof era -> MockChainFailure era -> Set ScriptHash
getw Proof era
proof MockChainFailure era
mcf)) Set ScriptHash
forall a. Set a
Set.empty [MockChainFailure era]
xs
  where
    getw :: Proof era -> MockChainFailure era -> Set.Set ScriptHash
    getw :: forall era. Proof era -> MockChainFailure era -> Set ScriptHash
getw
      Proof era
Babbage
      ( MockChainFromLedgersFailure
          ( LedgerFailure
              ( UtxowFailure
                  ( AlonzoInBabbageUtxowPredFailure
                      ( ShelleyInAlonzoUtxowPredFailure
                          (ScriptWitnessNotValidatingUTXOW Set ScriptHash
set)
                        )
                    )
                )
            )
        ) = Set ScriptHash
set
    getw
      Proof era
Alonzo
      ( MockChainFromLedgersFailure
          ( LedgerFailure
              ( UtxowFailure
                  ( ShelleyInAlonzoUtxowPredFailure
                      (ScriptWitnessNotValidatingUTXOW Set ScriptHash
set)
                    )
                )
            )
        ) = Set ScriptHash
set
    getw
      Proof era
Mary
      ( MockChainFromLedgersFailure
          ( LedgerFailure
              ( UtxowFailure
                  (ScriptWitnessNotValidatingUTXOW Set ScriptHash
set)
                )
            )
        ) = Set ScriptHash
set
    getw
      Proof era
Allegra
      ( MockChainFromLedgersFailure
          ( LedgerFailure
              ( UtxowFailure
                  (ScriptWitnessNotValidatingUTXOW Set ScriptHash
set)
                )
            )
        ) = Set ScriptHash
set
    getw Proof era
_ MockChainFailure era
_ = Set ScriptHash
forall a. Set a
Set.empty

shortTxOut :: EraTxOut era => TxOut era -> Expr
shortTxOut :: forall era. EraTxOut era => TxOut era -> Expr
shortTxOut TxOut era
out = case TxOut era
out TxOut era -> Getting Addr (TxOut era) Addr -> Addr
forall s a. s -> Getting a s a -> a
^. Getting Addr (TxOut era) Addr
forall era. EraTxOut era => Lens' (TxOut era) Addr
Lens' (TxOut era) Addr
addrTxOutL of
  Addr Network
_ PaymentCredential
pay StakeReference
_ -> (PaymentCredential, Coin) -> Expr
forall a. ToExpr a => a -> Expr
toExpr (PaymentCredential
pay, TxOut era
out TxOut era -> Getting Coin (TxOut era) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (TxOut era) Coin
forall era. (HasCallStack, EraTxOut era) => Lens' (TxOut era) Coin
Lens' (TxOut era) Coin
coinTxOutL)
  Addr
_ -> String -> Expr
forall a. HasCallStack => String -> a
error String
"Bootstrap Address in shortTxOut"

smartTxBody :: EraTest era => MUtxo era -> TxBody TopTx era -> Expr
smartTxBody :: forall era. EraTest era => MUtxo era -> TxBody TopTx era -> Expr
smartTxBody Map TxIn (TxOut era)
u TxBody TopTx era
txbody = (Map TxIn (TxOut era), TxBody TopTx era) -> Expr
forall a. ToExpr a => a -> Expr
toExpr (Map TxIn (TxOut era)
u, TxBody TopTx era
txbody)

-- =====================================================================
-- HasTrace instance of MOCKCHAIN depends on STS(MOCKCHAIN era) instance
-- We show the type family instances here for reference.
{-
instance STS (MOCKCHAIN era)
  where
  type State (MOCKCHAIN era) = MockChainState era
  type Signal (MOCKCHAIN era) = (MockBlock era)
  type Environment (MOCKCHAIN era) = ()
-}
-- ==============================================================

data Gen1 era = Gen1 (Vector (StrictSeq (Tx TopTx era), SlotNo)) (GenState era)

instance
  ( STS (MOCKCHAIN era)
  , Reflect era
  , EraTest era
  , ToExpr (PredicateFailure (EraRule "LEDGER" era))
  ) =>
  HasTrace (MOCKCHAIN era) (Gen1 era)
  where
  type BaseEnv (MOCKCHAIN era) = Globals

  interpretSTS :: forall a.
HasCallStack =>
BaseEnv (MOCKCHAIN era) -> BaseM (MOCKCHAIN era) a -> a
interpretSTS BaseEnv (MOCKCHAIN era)
globals BaseM (MOCKCHAIN 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 (MOCKCHAIN era) a
act Globals
BaseEnv (MOCKCHAIN era)
globals

  envGen :: HasCallStack => Gen1 era -> Gen (Environment (MOCKCHAIN era))
envGen Gen1 era
_gstate = () -> Gen ()
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

  sigGen :: HasCallStack =>
Gen1 era
-> Environment (MOCKCHAIN era)
-> State (MOCKCHAIN era)
-> Gen (Signal (MOCKCHAIN era))
sigGen (Gen1 Vector (StrictSeq (Tx TopTx era), SlotNo)
txss GenState era
gs) () mcs :: State (MOCKCHAIN era)
mcs@(MockChainState NewEpochState era
newepoch NewEpochState era
_ (SlotNo Word64
lastSlot) Int
count) = do
    let NewEpochState EpochNo
epochnum BlocksMade
_ BlocksMade
_ EpochState era
epochstate StrictMaybe PulsingRewUpdate
_ PoolDistr
pooldistr StashedAVVMAddresses era
_ = NewEpochState era
newepoch
    issuerkey <- EpochNo -> Word64 -> Int -> PoolDistr -> Gen (KeyHash StakePool)
chooseIssuer EpochNo
epochnum Word64
lastSlot Int
count PoolDistr
pooldistr
    let (txs, nextSlotNo) = txss ! count
    -- Assmble it into a MockBlock
    let mockblock = KeyHash StakePool
-> SlotNo -> StrictSeq (Tx TopTx era) -> MockBlock era
forall era.
KeyHash StakePool
-> SlotNo -> StrictSeq (Tx TopTx era) -> MockBlock era
MockBlock KeyHash StakePool
issuerkey SlotNo
nextSlotNo StrictSeq (Tx TopTx era)
txs
    -- Run the STS Rules for MOCKCHAIN with generated signal

    case runShelleyBase (applySTSTest (TRC @(MOCKCHAIN era) ((), mcs, mockblock))) of
      Left NonEmpty (MockChainFailure era)
pdfs ->
        let txsl :: [Tx TopTx era]
txsl = StrictSeq (Tx TopTx era) -> [Tx TopTx era]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList StrictSeq (Tx TopTx era)
txs
         in String -> Gen (MockBlock era) -> Gen (MockBlock era)
forall a. String -> a -> a
Debug.trace
              (Word64
-> SlotNo
-> EpochState era
-> NonEmpty (MockChainFailure era)
-> [Tx TopTx era]
-> GenState era
-> String
forall era.
Reflect era =>
Word64
-> SlotNo
-> EpochState era
-> NonEmpty (MockChainFailure era)
-> [Tx TopTx era]
-> GenState era
-> String
raiseMockError Word64
lastSlot SlotNo
nextSlotNo EpochState era
epochstate NonEmpty (MockChainFailure era)
pdfs [Tx TopTx era]
txsl GenState era
gs)
              ( String -> Gen (MockBlock era)
forall a. HasCallStack => String -> a
error (String -> Gen (MockBlock era))
-> ([String] -> String) -> [String] -> Gen (MockBlock era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
unlines ([String] -> Gen (MockBlock era))
-> [String] -> Gen (MockBlock era)
forall a b. (a -> b) -> a -> b
$
                  [String
"EpochState:"]
                    [String] -> [String] -> [String]
forall a. Semigroup a => a -> a -> a
<> [EpochState era -> String
forall a. ToExpr a => a -> String
showExpr EpochState era
epochstate]
                    [String] -> [String] -> [String]
forall a. Semigroup a => a -> a -> a
<> [String
"Tx:"]
                    [String] -> [String] -> [String]
forall a. Semigroup a => a -> a -> a
<> StrictSeq String -> [String]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Tx TopTx era -> String
forall a. ToExpr a => a -> String
showExpr (Tx TopTx era -> String)
-> StrictSeq (Tx TopTx era) -> StrictSeq String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictSeq (Tx TopTx era)
txs)
                    [String] -> [String] -> [String]
forall a. Semigroup a => a -> a -> a
<> [String
"sigGen in (HasTrace (MOCKCHAIN era) (Gen1 era)) FAILS"]
                    [String] -> [String] -> [String]
forall a. Semigroup a => a -> a -> a
<> (MockChainFailure era -> String)
-> [MockChainFailure era] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map MockChainFailure era -> String
forall a. ToExpr a => a -> String
showExpr (NonEmpty (MockChainFailure era) -> [MockChainFailure era]
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList NonEmpty (MockChainFailure era)
pdfs)
              )
      Right State (MOCKCHAIN era)
mcs2 -> State (MOCKCHAIN era) -> Gen (MockBlock era) -> Gen (MockBlock era)
forall a b. a -> b -> b
seq State (MOCKCHAIN era)
mcs2 (MockBlock era -> Gen (MockBlock era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure MockBlock era
mockblock)

  shrinkSignal :: HasCallStack => Signal (MOCKCHAIN era) -> [Signal (MOCKCHAIN era)]
shrinkSignal Signal (MOCKCHAIN era)
_ = []

-- TODO, perhaps we might add shrinking like this. Just a thought. Failure is usually caused by just one Tx
-- in the Block. If the first or last Tx, is independent of the failing Tx, we can probably throw them away.
--  shrinkSignal (MockBlock _ _ xs) | SS.null xs = []
--  shrinkSignal (MockBlock i s xs) = [MockBlock i s (SS.drop 1 xs), MockBlock i s (SS.take (SS.length xs - 1) xs)]

mapProportion :: EpochNo -> Word64 -> Int -> Map.Map k Int -> Gen k
mapProportion :: forall k. EpochNo -> Word64 -> Int -> Map k Int -> Gen k
mapProportion EpochNo
epochnum Word64
lastSlot Int
count Map k Int
m =
  case [(Int, Gen k)]
pairs of
    [] ->
      -- TODO, we need to figure out why this occurs. It always occurs near SlotNo 300, So I am assuming that
      -- sometimes as we move into the 3rd epoch, however stakeDistr is computed becomes empty. This is probably
      -- because there is no action in Test.Cardano.Ledger.Constrained.Trace.Actions for the epoch boundary.
      -- This temporary fix is good enough for now. But the annoying trace message reminds us to fix this.
      String -> Gen k -> Gen k
forall a. String -> a -> a
Debug.trace
        ( String
"There are no stakepools to choose an issuer from"
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", epoch="
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ EpochNo -> String
forall a. Show a => a -> String
show EpochNo
epochnum
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", last slot="
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall a. Show a => a -> String
show Word64
lastSlot
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", index of Tx="
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
count
        )
        Gen k
forall a. a
discard
    ((Int, Gen k)
w : [(Int, Gen k)]
_) ->
      if ((Int, Gen k) -> Bool) -> [(Int, Gen k)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(Int
n, Gen k
_k) -> Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0) [(Int, Gen k)]
pairs
        then (Int, Gen k) -> Gen k
forall a b. (a, b) -> b
snd (Int, Gen k)
w -- All stakepools have zero Stake, choose issuer arbitrarily. possible, but rare.
        else [(Int, Gen k)] -> Gen k
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency [(Int, Gen k)]
pairs
  where
    pairs :: [(Int, Gen k)]
pairs = [(Int
n, k -> Gen k
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure k
k) | (k
k, Int
n) <- Map k Int -> [(k, Int)]
forall k a. Map k a -> [(k, a)]
Map.toList Map k Int
m]

chooseIssuer :: EpochNo -> Word64 -> Int -> PoolDistr -> Gen (KeyHash StakePool)
chooseIssuer :: EpochNo -> Word64 -> Int -> PoolDistr -> Gen (KeyHash StakePool)
chooseIssuer EpochNo
epochnum Word64
lastSlot Int
count (PoolDistr Map (KeyHash StakePool) IndividualPoolStake
m CompactForm Coin
_) = EpochNo
-> Word64
-> Int
-> Map (KeyHash StakePool) Int
-> Gen (KeyHash StakePool)
forall k. EpochNo -> Word64 -> Int -> Map k Int -> Gen k
mapProportion EpochNo
epochnum Word64
lastSlot Int
count (IndividualPoolStake -> Int
forall {b}. Integral b => IndividualPoolStake -> b
getInt (IndividualPoolStake -> Int)
-> Map (KeyHash StakePool) IndividualPoolStake
-> Map (KeyHash StakePool) Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map (KeyHash StakePool) IndividualPoolStake
m)
  where
    getInt :: IndividualPoolStake -> b
getInt IndividualPoolStake
x = Rational -> b
forall b. Integral b => Rational -> b
forall a b. (RealFrac a, Integral b) => a -> b
floor (IndividualPoolStake -> Rational
individualPoolStake IndividualPoolStake
x Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Rational
1000)

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

-- Generating Traces, and making properties out of a Trace
-- =========================================================================

genTrace ::
  forall era.
  ( HasTrace (MOCKCHAIN era) (Gen1 era)
  , EraGenericGen era
  , ShelleyEraAccounts era
  ) =>
  Int ->
  GenSize ->
  GenRS era () -> -- An arbitrary 'initialization action', to run before we generate the sequence
  -- use (pure ()) if you don't want or need initialization
  Gen (Trace (MOCKCHAIN era))
genTrace :: forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era,
 ShelleyEraAccounts era) =>
Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
genTrace Int
numTxInTrace GenSize
gsize GenRS era ()
initialize = do
  (vs, genstate) <- GenSize
-> Int
-> GenRS era ()
-> Gen (Vector (StrictSeq (Tx TopTx era), SlotNo), GenState era)
forall era.
EraGenericGen era =>
GenSize
-> Int
-> GenRS era ()
-> Gen (Vector (StrictSeq (Tx TopTx era), SlotNo), GenState era)
genTxSeq GenSize
gsize Int
numTxInTrace GenRS era ()
initialize
  let initState = GenState era -> MockChainState era
forall era.
(Reflect era, ShelleyEraAccounts era) =>
GenState era -> MockChainState era
initialMockChainState GenState era
genstate
  traceFromInitState @(MOCKCHAIN era)
    testGlobals
    (fromIntegral (length vs))
    (Gen1 vs genstate)
    (Just (\IRC (MOCKCHAIN era)
_ -> Either (NonEmpty (MockChainFailure era)) (MockChainState era)
-> Gen
     (Either (NonEmpty (MockChainFailure era)) (MockChainState era))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (NonEmpty (MockChainFailure era)) (MockChainState era)
 -> Gen
      (Either (NonEmpty (MockChainFailure era)) (MockChainState era)))
-> Either (NonEmpty (MockChainFailure era)) (MockChainState era)
-> Gen
     (Either (NonEmpty (MockChainFailure era)) (MockChainState era))
forall a b. (a -> b) -> a -> b
$ MockChainState era
-> Either (NonEmpty (MockChainFailure era)) (MockChainState era)
forall a b. b -> Either a b
Right MockChainState era
initState))

traceProp ::
  forall era prop.
  ( HasTrace (MOCKCHAIN era) (Gen1 era)
  , EraGenericGen era
  , ShelleyEraAccounts era
  ) =>
  Int ->
  GenSize ->
  (MockChainState era -> MockChainState era -> prop) ->
  Gen prop
traceProp :: forall era prop.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era,
 ShelleyEraAccounts era) =>
Int
-> GenSize
-> (MockChainState era -> MockChainState era -> prop)
-> Gen prop
traceProp Int
numTxInTrace GenSize
gsize MockChainState era -> MockChainState era -> prop
f = do
  trace1 <- Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era,
 ShelleyEraAccounts era) =>
Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
genTrace Int
numTxInTrace GenSize
gsize GenRS era ()
forall era. Reflect era => GenRS era ()
initStableFields
  pure (f (_traceInitState trace1) (lastState trace1))

forEachEpochTrace ::
  forall era prop.
  ( Testable prop
  , HasTrace (MOCKCHAIN era) (Gen1 era)
  , EraGenericGen era
  , ShelleyEraAccounts era
  ) =>
  Int ->
  GenSize ->
  (Trace (MOCKCHAIN era) -> prop) ->
  Gen Property
forEachEpochTrace :: forall era prop.
(Testable prop, HasTrace (MOCKCHAIN era) (Gen1 era),
 EraGenericGen era, ShelleyEraAccounts era) =>
Int -> GenSize -> (Trace (MOCKCHAIN era) -> prop) -> Gen Property
forEachEpochTrace Int
tracelen GenSize
genSize Trace (MOCKCHAIN era) -> prop
f = do
  let newEpoch :: MockChainState era -> MockChainState era -> Bool
newEpoch MockChainState era
tr1 MockChainState era
tr2 = NewEpochState era -> EpochNo
forall era. NewEpochState era -> EpochNo
nesEL (MockChainState era -> NewEpochState era
forall era. MockChainState era -> NewEpochState era
mcsNes MockChainState era
tr1) EpochNo -> EpochNo -> Bool
forall a. Eq a => a -> a -> Bool
/= NewEpochState era -> EpochNo
forall era. NewEpochState era -> EpochNo
nesEL (MockChainState era -> NewEpochState era
forall era. MockChainState era -> NewEpochState era
mcsNes MockChainState era
tr2)
  trc <- do
    (vs, genstate) <- GenSize
-> Int
-> GenRS era ()
-> Gen (Vector (StrictSeq (Tx TopTx era), SlotNo), GenState era)
forall era.
EraGenericGen era =>
GenSize
-> Int
-> GenRS era ()
-> Gen (Vector (StrictSeq (Tx TopTx era), SlotNo), GenState era)
genTxSeq GenSize
genSize Int
tracelen GenRS era ()
forall era. Reflect era => GenRS era ()
initStableFields
    let initState = GenState era -> MockChainState era
forall era.
(Reflect era, ShelleyEraAccounts era) =>
GenState era -> MockChainState era
initialMockChainState GenState era
genstate
    traceFromInitState @(MOCKCHAIN era)
      testGlobals
      (fromIntegral (length vs))
      (Gen1 vs genstate)
      (Just (\IRC (MOCKCHAIN era)
_ -> Either (NonEmpty (MockChainFailure era)) (MockChainState era)
-> Gen
     (Either (NonEmpty (MockChainFailure era)) (MockChainState era))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (NonEmpty (MockChainFailure era)) (MockChainState era)
 -> Gen
      (Either (NonEmpty (MockChainFailure era)) (MockChainState era)))
-> Either (NonEmpty (MockChainFailure era)) (MockChainState era)
-> Gen
     (Either (NonEmpty (MockChainFailure era)) (MockChainState era))
forall a b. (a -> b) -> a -> b
$ MockChainState era
-> Either (NonEmpty (MockChainFailure era)) (MockChainState era)
forall a b. b -> Either a b
Right MockChainState era
initState))
  let propf (Trace (MOCKCHAIN era)
subtrace, Int
index) = String -> prop -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"Subtrace of EpochNo " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
index String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" fails.") (Trace (MOCKCHAIN era) -> prop
f Trace (MOCKCHAIN era)
subtrace)
  -- The very last sub-trace may not be a full epoch, so we throw it away.
  case reverse (splitTrace newEpoch trc) of
    [] -> Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True)
    Trace (MOCKCHAIN era)
_ : [Trace (MOCKCHAIN era)]
revSplits -> Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ((Trace (MOCKCHAIN era), Int) -> Property
propf ((Trace (MOCKCHAIN era), Int) -> Property)
-> [(Trace (MOCKCHAIN era), Int)] -> [Property]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Trace (MOCKCHAIN era)] -> [Int] -> [(Trace (MOCKCHAIN era), Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([Trace (MOCKCHAIN era)] -> [Trace (MOCKCHAIN era)]
forall a. [a] -> [a]
reverse [Trace (MOCKCHAIN era)]
revSplits) [Int
0 :: Int ..]))

-- | Check a property on the 'sts' traces.
--
-- Takes an optional generator for initial state of the STS.
forAllTraceFromInitState ::
  forall sts traceGenEnv prop.
  ( HasTrace sts traceGenEnv
  , Testable prop
  , Show (Environment sts)
  ) =>
  BaseEnv sts ->
  -- | Maximum trace length.
  Word64 ->
  traceGenEnv ->
  -- | Optional generator of STS initial state
  Maybe (IRC sts -> Gen (Either (NonEmpty (STS.PredicateFailure sts)) (State sts))) ->
  (Trace sts -> prop) ->
  Property
forAllTraceFromInitState :: forall sts traceGenEnv prop.
(HasTrace sts traceGenEnv, Testable prop,
 Show (Environment sts)) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
     (IRC sts
      -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> (Trace sts -> prop)
-> Property
forAllTraceFromInitState BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Maybe
  (IRC sts
   -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
genSt0 =
  Gen (Trace sts)
-> (Trace sts -> [Trace sts]) -> (Trace sts -> prop) -> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
forAllShrinkBlind
    (forall sts traceGenEnv.
(HasTrace sts traceGenEnv, Show (Environment sts), HasCallStack) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
     (IRC sts
      -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> Gen (Trace sts)
traceFromInitState @sts @traceGenEnv BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Maybe
  (IRC sts
   -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
genSt0)
    ([Trace sts] -> Trace sts -> [Trace sts]
forall a b. a -> b -> a
const [])

-- =========================================================================
-- Test for just making a trace

-- | We are making 'smoke' tests, testing for smoke rather than fire.
--   Under the assumption that shorter tests have advantages
--   like not getting turned off because the tests take too long. A glaring failure is
--   likely to be caught in 'n' tests, rather than the standard '100'
testPropMax :: Testable prop => Int -> String -> prop -> Spec
testPropMax :: forall prop. Testable prop => Int -> String -> prop -> Spec
testPropMax Int
n String
name prop
x = String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
name (Int -> prop -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
n prop
x)

chainTest ::
  forall era.
  ( HasTrace (MOCKCHAIN era) (Gen1 era)
  , Eq (StashedAVVMAddresses era)
  , EraGenericGen era
  , ShelleyEraAccounts era
  ) =>
  Int ->
  GenSize ->
  Spec
chainTest :: forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era),
 Eq (StashedAVVMAddresses era), EraGenericGen era,
 ShelleyEraAccounts era) =>
Int -> GenSize -> Spec
chainTest Int
n GenSize
gsize = Int -> String -> Gen Property -> Spec
forall prop. Testable prop => Int -> String -> prop -> Spec
testPropMax Int
30 (forall era. Era era => String
eraName @era) Gen Property
action
  where
    action :: Gen Property
action = do
      (vs, genstate) <- forall era.
EraGenericGen era =>
GenSize
-> Int
-> GenRS era ()
-> Gen (Vector (StrictSeq (Tx TopTx era), SlotNo), GenState era)
genTxSeq @era GenSize
gsize Int
n GenRS era ()
forall era. Reflect era => GenRS era ()
initStableFields
      let initState = GenState era -> MockChainState era
forall era.
(Reflect era, ShelleyEraAccounts era) =>
GenState era -> MockChainState era
initialMockChainState GenState era
genstate
      trace1 <-
        traceFromInitState @(MOCKCHAIN era)
          testGlobals
          (fromIntegral (length vs))
          (Gen1 vs genstate)
          (Just (\IRC (MOCKCHAIN era)
_ -> Either (NonEmpty (MockChainFailure era)) (MockChainState era)
-> Gen
     (Either (NonEmpty (MockChainFailure era)) (MockChainState era))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (NonEmpty (MockChainFailure era)) (MockChainState era)
 -> Gen
      (Either (NonEmpty (MockChainFailure era)) (MockChainState era)))
-> Either (NonEmpty (MockChainFailure era)) (MockChainState era)
-> Gen
     (Either (NonEmpty (MockChainFailure era)) (MockChainState era))
forall a b. (a -> b) -> a -> b
$ MockChainState era
-> Either (NonEmpty (MockChainFailure era)) (MockChainState era)
forall a b. b -> Either a b
Right MockChainState era
initState))
      -- Here is where we can add some properties for traces:
      pure (_traceInitState trace1 === initState)

testTraces :: Int -> Spec
testTraces :: Int -> Spec
testTraces Int
n =
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"MockChainTrace" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era),
 Eq (StashedAVVMAddresses era), EraGenericGen era,
 ShelleyEraAccounts era) =>
Int -> GenSize -> Spec
chainTest @BabbageEra Int
n GenSize
defaultGenSize
    forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era),
 Eq (StashedAVVMAddresses era), EraGenericGen era,
 ShelleyEraAccounts era) =>
Int -> GenSize -> Spec
chainTest @AlonzoEra Int
n GenSize
defaultGenSize
    forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era),
 Eq (StashedAVVMAddresses era), EraGenericGen era,
 ShelleyEraAccounts era) =>
Int -> GenSize -> Spec
chainTest @MaryEra Int
n GenSize
defaultGenSize
    forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era),
 Eq (StashedAVVMAddresses era), EraGenericGen era,
 ShelleyEraAccounts era) =>
Int -> GenSize -> Spec
chainTest @AllegraEra Int
n GenSize
defaultGenSize
    forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era,
 ShelleyEraAccounts era) =>
Int -> GenSize -> Spec
multiEpochTest @BabbageEra Int
225 GenSize
defaultGenSize
    forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era,
 ShelleyEraAccounts era) =>
Int -> GenSize -> Spec
multiEpochTest @ShelleyEra Int
225 GenSize
defaultGenSize

-- | Show that Ada is preserved across multiple Epochs
multiEpochTest ::
  forall era.
  ( HasTrace (MOCKCHAIN era) (Gen1 era)
  , EraGenericGen era
  , ShelleyEraAccounts era
  ) =>
  Int ->
  GenSize ->
  Spec
multiEpochTest :: forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era,
 ShelleyEraAccounts era) =>
Int -> GenSize -> Spec
multiEpochTest Int
numTx GenSize
gsize =
  let gensize :: GenSize
gensize = GenSize
gsize {blocksizeMax = 4, slotDelta = (6, 12)}
      getEpoch :: MockChainState era -> EpochNo
getEpoch MockChainState era
mockchainstate = NewEpochState era -> EpochNo
forall era. NewEpochState era -> EpochNo
nesEL (MockChainState era -> NewEpochState era
forall era. MockChainState era -> NewEpochState era
mcsNes MockChainState era
mockchainstate)
      propf :: t -> MockChainState era -> Property
propf t
firstSt MockChainState era
lastSt =
        EpochNo -> Property -> Property
forall a prop. (Show a, Testable prop) => a -> prop -> Property
collect (MockChainState era -> EpochNo
forall {era}. MockChainState era -> EpochNo
getEpoch MockChainState era
lastSt) (t -> Coin
forall t. TotalAda t => t -> Coin
totalAda t
firstSt Coin -> Coin -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== MockChainState era -> Coin
forall t. TotalAda t => t -> Coin
totalAda MockChainState era
lastSt)
   in Int -> String -> Gen Property -> Spec
forall prop. Testable prop => Int -> String -> prop -> Spec
testPropMax
        Int
30
        (String
"Multi epoch. Ada is preserved. " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (forall era. Era era => String
eraName @era) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
". Trace length = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
numTx)
        (forall era prop.
(HasTrace (MOCKCHAIN era) (Gen1 era), EraGenericGen era,
 ShelleyEraAccounts era) =>
Int
-> GenSize
-> (MockChainState era -> MockChainState era -> prop)
-> Gen prop
traceProp @era Int
numTx GenSize
gensize MockChainState era -> MockChainState era -> Property
forall {era} {t}.
(ProtVerIsInBounds
   "at most"
   era
   11
   (OrdCond (CmpNat (ProtVerLow era) 11) 'True 'True 'False),
 Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 TotalAda t, Reflect era) =>
t -> MockChainState era -> Property
propf)