{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# 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,
  dsUnifiedL,
  esLStateL,
  lsCertStateL,
  prevPParamsEpochStateL,
  psDepositsL,
  psStakePoolParamsL,
 )
import Cardano.Ledger.Shelley.Rules (
  ShelleyLedgerPredFailure (..),
  ShelleyLedgersPredFailure (..),
  ShelleyUtxowPredFailure (ScriptWitnessNotValidatingUTXOW),
 )
import Cardano.Ledger.State (
  ChainAccountState (..),
  EraCertState (..),
  IndividualPoolStake (..),
  PoolDistr (..),
  SnapShots (..),
  calculatePoolDistr,
 )
import qualified Cardano.Ledger.UMap as UM
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 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.Generic.ApplyTx (applyTx)
import Test.Cardano.Ledger.Generic.Functions (
  adaPots,
  totalAda,
  txoutFields,
 )
import Test.Cardano.Ledger.Generic.GenState (
  GenEnv (..),
  GenRS,
  GenSize (..),
  GenState (..),
  getBlocksizeMax,
  getReserves,
  getSlot,
  getSlotDelta,
  getTreasury,
  initStableFields,
  initialLedgerState,
  modifyModel,
  runGenRS,
 )
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.TreeDiff ()
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)
import Test.QuickCheck
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.QuickCheck (testProperty)

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

-- | 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. Reflect era => Proof era -> Int -> SlotNo -> GenRS era (Tx era)
genRsTxAndModel :: forall era.
Reflect era =>
Proof era -> Int -> SlotNo -> GenRS era (Tx era)
genRsTxAndModel Proof era
proof Int
n SlotNo
slot = do
  (UTxO era
_, Tx era
tx) <- Proof era
-> SlotNo
-> RWST (GenEnv era) () (GenState era) Gen (UTxO era, Tx era)
forall era.
Reflect era =>
Proof era -> SlotNo -> GenRS era (UTxO era, Tx era)
genAlonzoTx Proof era
proof SlotNo
slot
  (ModelNewEpochState era -> ModelNewEpochState era) -> GenRS era ()
forall era.
(ModelNewEpochState era -> ModelNewEpochState era) -> GenRS era ()
modifyModel (\ModelNewEpochState era
model -> Proof era
-> Int
-> SlotNo
-> ModelNewEpochState era
-> Tx era
-> ModelNewEpochState era
forall era.
Reflect era =>
Proof era -> Int -> SlotNo -> Model era -> Tx era -> Model era
applyTx Proof era
proof Int
n SlotNo
slot ModelNewEpochState era
model Tx era
tx)
  Tx era -> GenRS era (Tx era)
forall a. a -> RWST (GenEnv era) () (GenState era) Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Tx era
tx

-- | Generate a Vector of (StrictSeq (Tx era))  representing a (Vector Block)
genRsTxSeq ::
  forall era.
  Reflect era =>
  Proof era ->
  Int ->
  Int ->
  [(StrictSeq (Tx era), SlotNo)] ->
  SlotNo ->
  GenRS era (Vector (StrictSeq (Tx era), SlotNo))
genRsTxSeq :: forall era.
Reflect era =>
Proof era
-> Int
-> Int
-> [(StrictSeq (Tx era), SlotNo)]
-> SlotNo
-> GenRS era (Vector (StrictSeq (Tx era), SlotNo))
genRsTxSeq Proof era
_ Int
this Int
lastN [(StrictSeq (Tx era), SlotNo)]
ans SlotNo
_slot | Int
this Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
lastN = do
  Vector (StrictSeq (Tx era), SlotNo)
-> GenRS era (Vector (StrictSeq (Tx era), SlotNo))
forall a. a -> RWST (GenEnv era) () (GenState era) Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(StrictSeq (Tx era), SlotNo)]
-> Vector (StrictSeq (Tx era), SlotNo)
forall a. [a] -> Vector a
Vector.fromList ([(StrictSeq (Tx era), SlotNo)] -> [(StrictSeq (Tx era), SlotNo)]
forall a. [a] -> [a]
reverse [(StrictSeq (Tx era), SlotNo)]
ans))
genRsTxSeq Proof era
proof Int
this Int
lastN [(StrictSeq (Tx era), SlotNo)]
ans SlotNo
slot = do
  Integer
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
  Int
n <- Gen Int -> RWST (GenEnv era) () (GenState era) Gen Int
forall (m :: * -> *) a.
Monad m =>
m a -> RWST (GenEnv era) () (GenState era) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Gen Int -> RWST (GenEnv era) () (GenState era) Gen Int)
-> Gen Int -> RWST (GenEnv era) () (GenState era) Gen Int
forall a b. (a -> b) -> a -> b
$ (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
2 :: Int, Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
maxBlockSize)
  [Tx era]
txs <- [Int]
-> (Int -> RWST (GenEnv era) () (GenState era) Gen (Tx era))
-> RWST (GenEnv era) () (GenState era) Gen [Tx era]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int
0 .. Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1] (\Int
i -> Proof era
-> Int
-> SlotNo
-> RWST (GenEnv era) () (GenState era) Gen (Tx era)
forall era.
Reflect era =>
Proof era -> Int -> SlotNo -> GenRS era (Tx era)
genRsTxAndModel Proof era
proof (Int
this Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i) SlotNo
slot)
  (Word64, Word64)
newSlotRange <- (GenState era -> (Word64, Word64))
-> RWST (GenEnv era) () (GenState era) Gen (Word64, Word64)
forall w (m :: * -> *) s a r.
(Monoid w, Monad m) =>
(s -> a) -> RWST r w s m a
gets GenState era -> (Word64, Word64)
forall era. GenState era -> (Word64, Word64)
getSlotDelta
  SlotNo
nextSlotNo <- Gen SlotNo -> RWST (GenEnv era) () (GenState era) Gen SlotNo
forall (m :: * -> *) a.
Monad m =>
m a -> RWST (GenEnv era) () (GenState era) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Gen SlotNo -> RWST (GenEnv era) () (GenState era) Gen SlotNo)
-> Gen SlotNo -> RWST (GenEnv era) () (GenState era) Gen SlotNo
forall a b. (a -> b) -> a -> b
$ Word64 -> SlotNo
SlotNo (Word64 -> SlotNo) -> (Word64 -> Word64) -> Word64 -> SlotNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ SlotNo -> Word64
unSlotNo SlotNo
slot) (Word64 -> SlotNo) -> Gen Word64 -> Gen SlotNo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Word64, Word64) -> Gen Word64
forall a. Random a => (a, a) -> Gen a
choose (Word64, Word64)
newSlotRange
  Proof era
-> Int
-> Int
-> [(StrictSeq (Tx era), SlotNo)]
-> SlotNo
-> GenRS era (Vector (StrictSeq (Tx era), SlotNo))
forall era.
Reflect era =>
Proof era
-> Int
-> Int
-> [(StrictSeq (Tx era), SlotNo)]
-> SlotNo
-> GenRS era (Vector (StrictSeq (Tx era), SlotNo))
genRsTxSeq Proof era
proof (Int
this Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) Int
lastN (([Tx era] -> StrictSeq (Tx era)
forall a. [a] -> StrictSeq a
SS.fromList [Tx era]
txs, SlotNo
slot) (StrictSeq (Tx era), SlotNo)
-> [(StrictSeq (Tx era), SlotNo)] -> [(StrictSeq (Tx era), SlotNo)]
forall a. a -> [a] -> [a]
: [(StrictSeq (Tx era), SlotNo)]
ans) SlotNo
nextSlotNo

-- | Generate a Vector of Blocks, and an initial LedgerState
genTxSeq ::
  forall era.
  Reflect era =>
  Proof era -> -- Proof of the Era we want to generate the sequence in
  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 era), SlotNo), GenState era)
genTxSeq :: forall era.
Reflect era =>
Proof era
-> GenSize
-> Int
-> GenRS era ()
-> Gen (Vector (StrictSeq (Tx era), SlotNo), GenState era)
genTxSeq Proof era
proof GenSize
gensize Int
numTx GenRS era ()
initialize = do
  Proof era
-> GenSize
-> GenRS era (Vector (StrictSeq (Tx era), SlotNo))
-> Gen (Vector (StrictSeq (Tx era), SlotNo), GenState era)
forall era a.
Reflect era =>
Proof era -> GenSize -> GenRS era a -> Gen (a, GenState era)
runGenRS Proof era
proof GenSize
gensize (GenRS era ()
initialize GenRS era ()
-> GenRS era (Vector (StrictSeq (Tx era), SlotNo))
-> GenRS era (Vector (StrictSeq (Tx 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
>> Proof era
-> Int
-> Int
-> [(StrictSeq (Tx era), SlotNo)]
-> SlotNo
-> GenRS era (Vector (StrictSeq (Tx era), SlotNo))
forall era.
Reflect era =>
Proof era
-> Int
-> Int
-> [(StrictSeq (Tx era), SlotNo)]
-> SlotNo
-> GenRS era (Vector (StrictSeq (Tx era), SlotNo))
genRsTxSeq Proof era
proof Int
0 Int
numTx [] (Word64 -> SlotNo
SlotNo (Word64 -> SlotNo) -> Word64 -> SlotNo
forall a b. (a -> b) -> a -> b
$ Word64
1))

runTest :: IO ()
runTest :: IO ()
runTest = do
  (Vector (StrictSeq (AlonzoTx BabbageEra), SlotNo)
v, GenState BabbageEra
_) <- Gen
  (Vector (StrictSeq (AlonzoTx BabbageEra), SlotNo),
   GenState BabbageEra)
-> IO
     (Vector (StrictSeq (AlonzoTx BabbageEra), SlotNo),
      GenState BabbageEra)
forall a. Gen a -> IO a
generate (Gen
   (Vector (StrictSeq (AlonzoTx BabbageEra), SlotNo),
    GenState BabbageEra)
 -> IO
      (Vector (StrictSeq (AlonzoTx BabbageEra), SlotNo),
       GenState BabbageEra))
-> Gen
     (Vector (StrictSeq (AlonzoTx BabbageEra), SlotNo),
      GenState BabbageEra)
-> IO
     (Vector (StrictSeq (AlonzoTx BabbageEra), SlotNo),
      GenState BabbageEra)
forall a b. (a -> b) -> a -> b
$ Proof BabbageEra
-> GenSize
-> Int
-> GenRS BabbageEra ()
-> Gen
     (Vector (StrictSeq (Tx BabbageEra), SlotNo), GenState BabbageEra)
forall era.
Reflect era =>
Proof era
-> GenSize
-> Int
-> GenRS era ()
-> Gen (Vector (StrictSeq (Tx era), SlotNo), GenState era)
genTxSeq Proof BabbageEra
Babbage GenSize
forall a. Default a => a
def Int
20 (() -> GenRS BabbageEra ()
forall a.
a -> RWST (GenEnv BabbageEra) () (GenState BabbageEra) Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
  Int -> IO ()
forall a. Show a => a -> IO ()
print (Vector (StrictSeq (AlonzoTx BabbageEra), SlotNo) -> Int
forall a. Vector a -> Int
Vector.length Vector (StrictSeq (AlonzoTx BabbageEra), SlotNo)
v)

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

initialMockChainState ::
  Reflect era =>
  Proof era ->
  GenState era ->
  MockChainState era
initialMockChainState :: forall era.
Reflect era =>
Proof era -> GenState era -> MockChainState era
initialMockChainState Proof era
proof 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 =>
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 Proof era
proof
        }

makeEpochState :: Reflect era => GenState era -> LedgerState era -> EpochState era
makeEpochState :: forall era.
Reflect 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) =>
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) => LedgerState era -> SnapShots
snaps :: forall era.
(EraTxOut era, EraCertState 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 =>
UTxO era -> DState era -> PState era -> SnapShot
stakeDistr UTxO era
u DState era
dstate PState era
pstate

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

raiseMockError ::
  forall era.
  ( Reflect era
  , EraTest era
  ) =>
  Word64 ->
  SlotNo ->
  EpochState era ->
  NonEmpty (MockChainFailure era) ->
  [Tx era] ->
  GenState era ->
  String
raiseMockError :: forall era.
(Reflect era, EraTest era) =>
Word64
-> SlotNo
-> EpochState era
-> NonEmpty (MockChainFailure era)
-> [Tx era]
-> GenState era
-> String
raiseMockError Word64
slot (SlotNo Word64
next) EpochState era
epochstate NonEmpty (MockChainFailure era)
_pdfs [Tx era]
_txs GenState era
_ =
  let _ssPoolParams :: Map (KeyHash 'StakePool) PoolParams
_ssPoolParams = EpochState era
epochstate EpochState era
-> Getting
     (Map (KeyHash 'StakePool) PoolParams)
     (EpochState era)
     (Map (KeyHash 'StakePool) PoolParams)
-> Map (KeyHash 'StakePool) PoolParams
forall s a. s -> Getting a s a -> a
^. (LedgerState era
 -> Const (Map (KeyHash 'StakePool) PoolParams) (LedgerState era))
-> EpochState era
-> Const (Map (KeyHash 'StakePool) PoolParams) (EpochState era)
forall era (f :: * -> *).
Functor f =>
(LedgerState era -> f (LedgerState era))
-> EpochState era -> f (EpochState era)
esLStateL ((LedgerState era
  -> Const (Map (KeyHash 'StakePool) PoolParams) (LedgerState era))
 -> EpochState era
 -> Const (Map (KeyHash 'StakePool) PoolParams) (EpochState era))
-> ((Map (KeyHash 'StakePool) PoolParams
     -> Const
          (Map (KeyHash 'StakePool) PoolParams)
          (Map (KeyHash 'StakePool) PoolParams))
    -> LedgerState era
    -> Const (Map (KeyHash 'StakePool) PoolParams) (LedgerState era))
-> Getting
     (Map (KeyHash 'StakePool) PoolParams)
     (EpochState era)
     (Map (KeyHash 'StakePool) PoolParams)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CertState era
 -> Const (Map (KeyHash 'StakePool) PoolParams) (CertState era))
-> LedgerState era
-> Const (Map (KeyHash 'StakePool) PoolParams) (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL ((CertState era
  -> Const (Map (KeyHash 'StakePool) PoolParams) (CertState era))
 -> LedgerState era
 -> Const (Map (KeyHash 'StakePool) PoolParams) (LedgerState era))
-> ((Map (KeyHash 'StakePool) PoolParams
     -> Const
          (Map (KeyHash 'StakePool) PoolParams)
          (Map (KeyHash 'StakePool) PoolParams))
    -> CertState era
    -> Const (Map (KeyHash 'StakePool) PoolParams) (CertState era))
-> (Map (KeyHash 'StakePool) PoolParams
    -> Const
         (Map (KeyHash 'StakePool) PoolParams)
         (Map (KeyHash 'StakePool) PoolParams))
-> LedgerState era
-> Const (Map (KeyHash 'StakePool) PoolParams) (LedgerState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PState era
 -> Const (Map (KeyHash 'StakePool) PoolParams) (PState era))
-> CertState era
-> Const (Map (KeyHash 'StakePool) PoolParams) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL ((PState era
  -> Const (Map (KeyHash 'StakePool) PoolParams) (PState era))
 -> CertState era
 -> Const (Map (KeyHash 'StakePool) PoolParams) (CertState era))
-> ((Map (KeyHash 'StakePool) PoolParams
     -> Const
          (Map (KeyHash 'StakePool) PoolParams)
          (Map (KeyHash 'StakePool) PoolParams))
    -> PState era
    -> Const (Map (KeyHash 'StakePool) PoolParams) (PState era))
-> (Map (KeyHash 'StakePool) PoolParams
    -> Const
         (Map (KeyHash 'StakePool) PoolParams)
         (Map (KeyHash 'StakePool) PoolParams))
-> CertState era
-> Const (Map (KeyHash 'StakePool) PoolParams) (CertState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (KeyHash 'StakePool) PoolParams
 -> Const
      (Map (KeyHash 'StakePool) PoolParams)
      (Map (KeyHash 'StakePool) PoolParams))
-> PState era
-> Const (Map (KeyHash 'StakePool) PoolParams) (PState era)
forall era (f :: * -> *).
Functor f =>
(Map (KeyHash 'StakePool) PoolParams
 -> f (Map (KeyHash 'StakePool) PoolParams))
-> PState era -> f (PState era)
psStakePoolParamsL
      _pooldeposits :: Map (KeyHash 'StakePool) Coin
_pooldeposits = EpochState era
epochstate EpochState era
-> Getting
     (Map (KeyHash 'StakePool) Coin)
     (EpochState era)
     (Map (KeyHash 'StakePool) Coin)
-> Map (KeyHash 'StakePool) Coin
forall s a. s -> Getting a s a -> a
^. (LedgerState era
 -> Const (Map (KeyHash 'StakePool) Coin) (LedgerState era))
-> EpochState era
-> Const (Map (KeyHash 'StakePool) Coin) (EpochState era)
forall era (f :: * -> *).
Functor f =>
(LedgerState era -> f (LedgerState era))
-> EpochState era -> f (EpochState era)
esLStateL ((LedgerState era
  -> Const (Map (KeyHash 'StakePool) Coin) (LedgerState era))
 -> EpochState era
 -> Const (Map (KeyHash 'StakePool) Coin) (EpochState era))
-> ((Map (KeyHash 'StakePool) Coin
     -> Const
          (Map (KeyHash 'StakePool) Coin) (Map (KeyHash 'StakePool) Coin))
    -> LedgerState era
    -> Const (Map (KeyHash 'StakePool) Coin) (LedgerState era))
-> Getting
     (Map (KeyHash 'StakePool) Coin)
     (EpochState era)
     (Map (KeyHash 'StakePool) Coin)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CertState era
 -> Const (Map (KeyHash 'StakePool) Coin) (CertState era))
-> LedgerState era
-> Const (Map (KeyHash 'StakePool) Coin) (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL ((CertState era
  -> Const (Map (KeyHash 'StakePool) Coin) (CertState era))
 -> LedgerState era
 -> Const (Map (KeyHash 'StakePool) Coin) (LedgerState era))
-> ((Map (KeyHash 'StakePool) Coin
     -> Const
          (Map (KeyHash 'StakePool) Coin) (Map (KeyHash 'StakePool) Coin))
    -> CertState era
    -> Const (Map (KeyHash 'StakePool) Coin) (CertState era))
-> (Map (KeyHash 'StakePool) Coin
    -> Const
         (Map (KeyHash 'StakePool) Coin) (Map (KeyHash 'StakePool) Coin))
-> LedgerState era
-> Const (Map (KeyHash 'StakePool) Coin) (LedgerState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PState era -> Const (Map (KeyHash 'StakePool) Coin) (PState era))
-> CertState era
-> Const (Map (KeyHash 'StakePool) Coin) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL ((PState era -> Const (Map (KeyHash 'StakePool) Coin) (PState era))
 -> CertState era
 -> Const (Map (KeyHash 'StakePool) Coin) (CertState era))
-> ((Map (KeyHash 'StakePool) Coin
     -> Const
          (Map (KeyHash 'StakePool) Coin) (Map (KeyHash 'StakePool) Coin))
    -> PState era
    -> Const (Map (KeyHash 'StakePool) Coin) (PState era))
-> (Map (KeyHash 'StakePool) Coin
    -> Const
         (Map (KeyHash 'StakePool) Coin) (Map (KeyHash 'StakePool) Coin))
-> CertState era
-> Const (Map (KeyHash 'StakePool) Coin) (CertState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (KeyHash 'StakePool) Coin
 -> Const
      (Map (KeyHash 'StakePool) Coin) (Map (KeyHash 'StakePool) Coin))
-> PState era -> Const (Map (KeyHash 'StakePool) Coin) (PState era)
forall era (f :: * -> *).
Functor f =>
(Map (KeyHash 'StakePool) Coin
 -> f (Map (KeyHash 'StakePool) Coin))
-> PState era -> f (PState era)
psDepositsL
      _keydeposits :: Map (Credential 'Staking) Coin
_keydeposits = UMap -> Map (Credential 'Staking) Coin
UM.depositMap (UMap -> Map (Credential 'Staking) Coin)
-> UMap -> Map (Credential 'Staking) Coin
forall a b. (a -> b) -> a -> b
$ EpochState era
epochstate EpochState era -> Getting UMap (EpochState era) UMap -> UMap
forall s a. s -> Getting a s a -> a
^. (LedgerState era -> Const UMap (LedgerState era))
-> EpochState era -> Const UMap (EpochState era)
forall era (f :: * -> *).
Functor f =>
(LedgerState era -> f (LedgerState era))
-> EpochState era -> f (EpochState era)
esLStateL ((LedgerState era -> Const UMap (LedgerState era))
 -> EpochState era -> Const UMap (EpochState era))
-> ((UMap -> Const UMap UMap)
    -> LedgerState era -> Const UMap (LedgerState era))
-> Getting UMap (EpochState era) UMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CertState era -> Const UMap (CertState era))
-> LedgerState era -> Const UMap (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL ((CertState era -> Const UMap (CertState era))
 -> LedgerState era -> Const UMap (LedgerState era))
-> ((UMap -> Const UMap UMap)
    -> CertState era -> Const UMap (CertState era))
-> (UMap -> Const UMap UMap)
-> LedgerState era
-> Const UMap (LedgerState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DState era -> Const UMap (DState era))
-> CertState era -> Const UMap (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era -> Const UMap (DState era))
 -> CertState era -> Const UMap (CertState era))
-> ((UMap -> Const UMap UMap)
    -> DState era -> Const UMap (DState era))
-> (UMap -> Const UMap UMap)
-> CertState era
-> Const UMap (CertState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UMap -> Const UMap UMap) -> DState era -> Const UMap (DState era)
forall era (f :: * -> *).
Functor f =>
(UMap -> f UMap) -> DState era -> f (DState era)
dsUnifiedL
   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 => Proof era -> TxOut era -> Expr
shortTxOut :: forall era. EraTxOut era => Proof era -> TxOut era -> Expr
shortTxOut Proof era
proof TxOut era
out = case Proof era -> TxOut era -> (Addr, Value era, [TxOutField era])
forall era.
Proof era -> TxOut era -> (Addr, Value era, [TxOutField era])
txoutFields Proof era
proof TxOut era
out of
  (Addr Network
_ PaymentCredential
pay StakeReference
_, Value era
_, [TxOutField era]
_) -> (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, Value era, [TxOutField era])
_ -> String -> Expr
forall a. HasCallStack => String -> a
error String
"Bootstrap Address in shortTxOut"

smartTxBody :: EraTest era => MUtxo era -> TxBody era -> Expr
smartTxBody :: forall era. EraTest era => MUtxo era -> TxBody era -> Expr
smartTxBody Map TxIn (TxOut era)
u TxBody era
txbody = (Map TxIn (TxOut era), TxBody era) -> Expr
forall a. ToExpr a => a -> Expr
toExpr (Map TxIn (TxOut era)
u, TxBody 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 era), SlotNo)) (GenState era)

instance
  ( STS (MOCKCHAIN era)
  , Reflect era
  , EraTest 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 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
    KeyHash 'StakePool
issuerkey <- EpochNo -> Word64 -> Int -> PoolDistr -> Gen (KeyHash 'StakePool)
chooseIssuer EpochNo
epochnum Word64
lastSlot Int
count PoolDistr
pooldistr
    let (StrictSeq (Tx era)
txs, SlotNo
nextSlotNo) = Vector (StrictSeq (Tx era), SlotNo)
txss Vector (StrictSeq (Tx era), SlotNo)
-> Int -> (StrictSeq (Tx era), SlotNo)
forall a. Vector a -> Int -> a
! Int
count
    -- Assmble it into a MockBlock
    let mockblock :: MockBlock era
mockblock = KeyHash 'StakePool -> SlotNo -> StrictSeq (Tx era) -> MockBlock era
forall era.
KeyHash 'StakePool -> SlotNo -> StrictSeq (Tx era) -> MockBlock era
MockBlock KeyHash 'StakePool
issuerkey SlotNo
nextSlotNo StrictSeq (Tx era)
txs
    -- Run the STS Rules for MOCKCHAIN with generated signal

    case ShelleyBase
  (Either (NonEmpty (MockChainFailure era)) (State (MOCKCHAIN era)))
-> Either (NonEmpty (MockChainFailure era)) (State (MOCKCHAIN era))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (MOCKCHAIN era)
-> ReaderT
     Globals
     Identity
     (Either
        (NonEmpty (PredicateFailure (MOCKCHAIN era)))
        (State (MOCKCHAIN era)))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC @(MOCKCHAIN era) ((), State (MOCKCHAIN era)
mcs, Signal (MOCKCHAIN era)
MockBlock era
mockblock))) of
      Left NonEmpty (MockChainFailure era)
pdfs ->
        let txsl :: [Tx era]
txsl = StrictSeq (Tx era) -> [Tx era]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList StrictSeq (Tx 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 era]
-> GenState era
-> String
forall era.
(Reflect era, EraTest era) =>
Word64
-> SlotNo
-> EpochState era
-> NonEmpty (MockChainFailure era)
-> [Tx era]
-> GenState era
-> String
raiseMockError Word64
lastSlot SlotNo
nextSlotNo EpochState era
epochstate NonEmpty (MockChainFailure era)
pdfs [Tx 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
"sigGen in (HasTrace (MOCKCHAIN era) (Gen1 era)) FAILS" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (MockChainFailure era -> String)
-> [MockChainFailure era] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map MockChainFailure era -> String
forall a. Show a => a -> String
show (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.
  ( Reflect era
  , HasTrace (MOCKCHAIN era) (Gen1 era)
  ) =>
  Proof 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.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
genTrace Proof era
proof Int
numTxInTrace GenSize
gsize GenRS era ()
initialize = do
  (Vector (StrictSeq (Tx era), SlotNo)
vs, GenState era
genstate) <- Proof era
-> GenSize
-> Int
-> GenRS era ()
-> Gen (Vector (StrictSeq (Tx era), SlotNo), GenState era)
forall era.
Reflect era =>
Proof era
-> GenSize
-> Int
-> GenRS era ()
-> Gen (Vector (StrictSeq (Tx era), SlotNo), GenState era)
genTxSeq Proof era
proof GenSize
gsize Int
numTxInTrace GenRS era ()
initialize
  let initState :: MockChainState era
initState = Proof era -> GenState era -> MockChainState era
forall era.
Reflect era =>
Proof era -> GenState era -> MockChainState era
initialMockChainState Proof era
proof GenState era
genstate
  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 @(MOCKCHAIN era)
    Globals
BaseEnv (MOCKCHAIN era)
testGlobals
    (Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Vector (StrictSeq (Tx era), SlotNo) -> Int
forall a. Vector a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Vector (StrictSeq (Tx era), SlotNo)
vs))
    (Vector (StrictSeq (Tx era), SlotNo) -> GenState era -> Gen1 era
forall era.
Vector (StrictSeq (Tx era), SlotNo) -> GenState era -> Gen1 era
Gen1 Vector (StrictSeq (Tx era), SlotNo)
vs GenState era
genstate)
    ((IRC (MOCKCHAIN era)
 -> Gen
      (Either (NonEmpty (MockChainFailure era)) (MockChainState era)))
-> Maybe
     (IRC (MOCKCHAIN era)
      -> Gen
           (Either (NonEmpty (MockChainFailure era)) (MockChainState era)))
forall a. a -> Maybe a
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.
  ( Reflect era
  , HasTrace (MOCKCHAIN era) (Gen1 era)
  ) =>
  Proof era ->
  Int ->
  GenSize ->
  (MockChainState era -> MockChainState era -> prop) ->
  Gen prop
traceProp :: forall era prop.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era
-> Int
-> GenSize
-> (MockChainState era -> MockChainState era -> prop)
-> Gen prop
traceProp Proof era
proof Int
numTxInTrace GenSize
gsize MockChainState era -> MockChainState era -> prop
f = do
  Trace (MOCKCHAIN era)
trace1 <- Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
genTrace Proof era
proof Int
numTxInTrace GenSize
gsize GenRS era ()
forall era. Reflect era => GenRS era ()
initStableFields
  prop -> Gen prop
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MockChainState era -> MockChainState era -> prop
f (Trace (MOCKCHAIN era) -> State (MOCKCHAIN era)
forall s. Trace s -> State s
_traceInitState Trace (MOCKCHAIN era)
trace1) (Trace (MOCKCHAIN era) -> State (MOCKCHAIN era)
forall s. Trace s -> State s
lastState Trace (MOCKCHAIN era)
trace1))

forEachEpochTrace ::
  forall era prop.
  ( Testable prop
  , Reflect era
  ) =>
  Proof era ->
  Int ->
  GenSize ->
  (Trace (MOCKCHAIN era) -> prop) ->
  Gen Property
forEachEpochTrace :: forall era prop.
(Testable prop, Reflect era) =>
Proof era
-> Int
-> GenSize
-> (Trace (MOCKCHAIN era) -> prop)
-> Gen Property
forEachEpochTrace Proof era
proof 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)
  Trace (MOCKCHAIN era)
trc <- case Proof era
proof of
    Proof era
Conway -> Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
genTrace Proof era
proof Int
tracelen GenSize
genSize GenRS era ()
forall era. Reflect era => GenRS era ()
initStableFields
    Proof era
Babbage -> Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
genTrace Proof era
proof Int
tracelen GenSize
genSize GenRS era ()
forall era. Reflect era => GenRS era ()
initStableFields
    Proof era
Alonzo -> Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
genTrace Proof era
proof Int
tracelen GenSize
genSize GenRS era ()
forall era. Reflect era => GenRS era ()
initStableFields
    Proof era
Allegra -> Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
genTrace Proof era
proof Int
tracelen GenSize
genSize GenRS era ()
forall era. Reflect era => GenRS era ()
initStableFields
    Proof era
Mary -> Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
genTrace Proof era
proof Int
tracelen GenSize
genSize GenRS era ()
forall era. Reflect era => GenRS era ()
initStableFields
    Proof era
Shelley -> Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
genTrace Proof era
proof Int
tracelen GenSize
genSize GenRS era ()
forall era. Reflect era => GenRS era ()
initStableFields
  let propf :: (Trace (MOCKCHAIN era), Int) -> Property
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 [Trace (MOCKCHAIN era)] -> [Trace (MOCKCHAIN era)]
forall a. [a] -> [a]
reverse ((State (MOCKCHAIN era) -> State (MOCKCHAIN era) -> Bool)
-> Trace (MOCKCHAIN era) -> [Trace (MOCKCHAIN era)]
forall s. (State s -> State s -> Bool) -> Trace s -> [Trace s]
splitTrace State (MOCKCHAIN era) -> State (MOCKCHAIN era) -> Bool
MockChainState era -> MockChainState era -> Bool
forall {era} {era}.
MockChainState era -> MockChainState era -> Bool
newEpoch Trace (MOCKCHAIN era)
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 -> TestTree
testPropMax :: forall prop. Testable prop => Int -> String -> prop -> TestTree
testPropMax Int
n String
name prop
x = String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty String
name (Int -> prop -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
n prop
x)

chainTest ::
  forall era.
  ( Reflect era
  , HasTrace (MOCKCHAIN era) (Gen1 era)
  , Eq (StashedAVVMAddresses era)
  ) =>
  Proof era ->
  Int ->
  GenSize ->
  TestTree
chainTest :: forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era),
 Eq (StashedAVVMAddresses era)) =>
Proof era -> Int -> GenSize -> TestTree
chainTest Proof era
proof Int
n GenSize
gsize = Int -> String -> Gen Property -> TestTree
forall prop. Testable prop => Int -> String -> prop -> TestTree
testPropMax Int
30 String
message Gen Property
action
  where
    message :: String
message = Proof era -> String
forall a. Show a => a -> String
show Proof era
proof String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" era."
    action :: Gen Property
action = do
      (Vector (StrictSeq (Tx era), SlotNo)
vs, GenState era
genstate) <- Proof era
-> GenSize
-> Int
-> GenRS era ()
-> Gen (Vector (StrictSeq (Tx era), SlotNo), GenState era)
forall era.
Reflect era =>
Proof era
-> GenSize
-> Int
-> GenRS era ()
-> Gen (Vector (StrictSeq (Tx era), SlotNo), GenState era)
genTxSeq Proof era
proof GenSize
gsize Int
n GenRS era ()
forall era. Reflect era => GenRS era ()
initStableFields
      let initState :: MockChainState era
initState = Proof era -> GenState era -> MockChainState era
forall era.
Reflect era =>
Proof era -> GenState era -> MockChainState era
initialMockChainState Proof era
proof GenState era
genstate
      Trace (MOCKCHAIN era)
trace1 <-
        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 @(MOCKCHAIN era)
          Globals
BaseEnv (MOCKCHAIN era)
testGlobals
          (Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Vector (StrictSeq (Tx era), SlotNo) -> Int
forall a. Vector a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Vector (StrictSeq (Tx era), SlotNo)
vs))
          (Vector (StrictSeq (Tx era), SlotNo) -> GenState era -> Gen1 era
forall era.
Vector (StrictSeq (Tx era), SlotNo) -> GenState era -> Gen1 era
Gen1 Vector (StrictSeq (Tx era), SlotNo)
vs GenState era
genstate)
          ((IRC (MOCKCHAIN era)
 -> Gen
      (Either (NonEmpty (MockChainFailure era)) (MockChainState era)))
-> Maybe
     (IRC (MOCKCHAIN era)
      -> Gen
           (Either (NonEmpty (MockChainFailure era)) (MockChainState era)))
forall a. a -> Maybe a
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:
      Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Trace (MOCKCHAIN era) -> State (MOCKCHAIN era)
forall s. Trace s -> State s
_traceInitState Trace (MOCKCHAIN era)
trace1 MockChainState era -> MockChainState era -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== MockChainState era
initState)

testTraces :: Int -> TestTree
testTraces :: Int -> TestTree
testTraces Int
n =
  String -> [TestTree] -> TestTree
testGroup
    String
"MockChainTrace"
    [ Proof BabbageEra -> Int -> GenSize -> TestTree
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era),
 Eq (StashedAVVMAddresses era)) =>
Proof era -> Int -> GenSize -> TestTree
chainTest Proof BabbageEra
Babbage Int
n GenSize
forall a. Default a => a
def
    , Proof AlonzoEra -> Int -> GenSize -> TestTree
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era),
 Eq (StashedAVVMAddresses era)) =>
Proof era -> Int -> GenSize -> TestTree
chainTest Proof AlonzoEra
Alonzo Int
n GenSize
forall a. Default a => a
def
    , Proof MaryEra -> Int -> GenSize -> TestTree
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era),
 Eq (StashedAVVMAddresses era)) =>
Proof era -> Int -> GenSize -> TestTree
chainTest Proof MaryEra
Mary Int
n GenSize
forall a. Default a => a
def
    , Proof AllegraEra -> Int -> GenSize -> TestTree
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era),
 Eq (StashedAVVMAddresses era)) =>
Proof era -> Int -> GenSize -> TestTree
chainTest Proof AllegraEra
Allegra Int
n GenSize
forall a. Default a => a
def
    , Proof BabbageEra -> Int -> GenSize -> TestTree
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> Int -> GenSize -> TestTree
multiEpochTest Proof BabbageEra
Babbage Int
225 GenSize
forall a. Default a => a
def
    , Proof ShelleyEra -> Int -> GenSize -> TestTree
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> Int -> GenSize -> TestTree
multiEpochTest Proof ShelleyEra
Shelley Int
225 GenSize
forall a. Default a => a
def
    ]

-- | Show that Ada is preserved across multiple Epochs
multiEpochTest ::
  ( Reflect era
  , HasTrace (MOCKCHAIN era) (Gen1 era)
  ) =>
  Proof era ->
  Int ->
  GenSize ->
  TestTree
multiEpochTest :: forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era -> Int -> GenSize -> TestTree
multiEpochTest Proof era
proof 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 -> TestTree
forall prop. Testable prop => Int -> String -> prop -> TestTree
testPropMax
        Int
30
        (String
"Multi epoch. Ada is preserved. " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Proof era -> String
forall a. Show a => a -> String
show Proof era
proof String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" era. Trace length = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
numTx)
        (Proof era
-> Int
-> GenSize
-> (MockChainState era -> MockChainState era -> Property)
-> Gen Property
forall era prop.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era
-> Int
-> GenSize
-> (MockChainState era -> MockChainState era -> prop)
-> Gen prop
traceProp Proof era
proof Int
numTx GenSize
gensize MockChainState era -> MockChainState era -> Property
forall {era} {t}.
(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)