{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module Test.Cardano.Ledger.Shelley.Rules.TestChain (
  delegTraceFromBlock,
  forAllChainTrace,
  ledgerTraceFromBlock,
  ledgerTraceFromBlockWithRestrictedUTxO,
  chainSstWithTick,
  poolTraceFromBlock,
  TestingLedger,
  splitTrace,
  forEachEpochTrace,
  traceLen,
  longTraceLen,
  shortChainTrace,
) where

import Cardano.Ledger.BaseTypes (Globals)
import Cardano.Ledger.Block (
  Block (..),
  bheader,
  neededTxInsForBlock,
 )
import Cardano.Ledger.Core
import Cardano.Ledger.Credential (Ptr (..))
import Cardano.Ledger.Shelley.API (ApplyBlock, CertState (..), ShelleyDELEG)
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.LedgerState (
  EpochState (..),
  LedgerState (..),
  NewEpochState (..),
  UTxOState (..),
  curPParamsEpochStateL,
 )
import Cardano.Ledger.Shelley.Rules (
  DelegEnv (..),
  LedgerEnv (..),
  PoolEnv (..),
  ShelleyPOOL,
 )
import Cardano.Ledger.UTxO (UTxO (..))
import Cardano.Protocol.TPraos.API (GetLedgerView)
import Cardano.Protocol.TPraos.BHeader (
  BHeader (..),
  bhbody,
  bheaderSlotNo,
 )
import Control.Monad.Trans.Reader (ReaderT)
import Control.State.Transition
import Data.Foldable (toList)
import Data.Functor.Identity (Identity)
import qualified Data.Map.Strict as Map
import Data.Maybe (mapMaybe)
import Data.Proxy
import qualified Data.Set as Set
import Data.Word (Word64)
import Lens.Micro ((^.))
import Lens.Micro.Extras (view)
import Test.Cardano.Ledger.Shelley.Constants (Constants)
import Test.Cardano.Ledger.Shelley.Generator.Block (tickChainState)
import Test.Cardano.Ledger.Shelley.Generator.Core (GenEnv)
import Test.Cardano.Ledger.Shelley.Generator.EraGen (EraGen (..))
import qualified Test.Cardano.Ledger.Shelley.Generator.Presets as Preset (genEnv)
import Test.Cardano.Ledger.Shelley.Generator.ShelleyEraGen ()
import Test.Cardano.Ledger.Shelley.Generator.Trace.Chain (mkGenesisChainState)
import Test.Cardano.Ledger.Shelley.Rules.Chain (CHAIN, ChainState (..))
import Test.Cardano.Ledger.Shelley.Utils (
  ChainProperty,
  runShelleyBase,
  testGlobals,
 )
import Test.Control.State.Transition.Trace (
  SourceSignalTarget (..),
  Trace (..),
  sourceSignalTargets,
  splitTrace,
 )
import qualified Test.Control.State.Transition.Trace as Trace
import Test.Control.State.Transition.Trace.Generator.QuickCheck (forAllTraceFromInitState)
import qualified Test.Control.State.Transition.Trace.Generator.QuickCheck as QC
import Test.QuickCheck (
  Property,
  Testable (..),
  conjoin,
  withMaxSuccess,
 )

------------------------------
-- Constants for Properties --
------------------------------

numberOfTests :: Word64
numberOfTests :: Word64
numberOfTests = Word64
300

traceLen :: Word64
traceLen :: Word64
traceLen = Word64
100

longTraceLen :: Word64
longTraceLen :: Word64
longTraceLen = Word64
150

type TestingLedger era ledger =
  ( BaseM ledger ~ ReaderT Globals Identity
  , Environment ledger ~ LedgerEnv era
  , State ledger ~ LedgerState era
  , Signal ledger ~ Tx era
  , Embed (EraRule "DELEGS" era) ledger
  , Embed (EraRule "UTXOW" era) ledger
  , STS ledger
  )

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

-- | Properties on really short chains, with only 100 successes
shortChainTrace ::
  forall era.
  ( EraGen era
  , QC.HasTrace (CHAIN era) (GenEnv era)
  , EraGov era
  ) =>
  Constants ->
  (SourceSignalTarget (CHAIN era) -> Property) ->
  Property
shortChainTrace :: forall era.
(EraGen era, HasTrace (CHAIN era) (GenEnv era), EraGov era) =>
Constants
-> (SourceSignalTarget (CHAIN era) -> Property) -> Property
shortChainTrace Constants
constants SourceSignalTarget (CHAIN era) -> Property
f = forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
100 forall a b. (a -> b) -> a -> b
$ forall era prop.
(Testable prop, EraGen era, HasTrace (CHAIN era) (GenEnv era),
 EraGov era) =>
Word64 -> Constants -> (Trace (CHAIN era) -> prop) -> Property
forAllChainTrace @era Word64
10 Constants
constants forall a b. (a -> b) -> a -> b
$ \Trace (CHAIN era)
tr -> forall prop. Testable prop => [prop] -> Property
conjoin (forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget (CHAIN era) -> Property
f (forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (CHAIN era)
tr))

----------------------------------------------------------------------
-- Projections of CHAIN Trace
----------------------------------------------------------------------

-- | Reconstruct a LEDGER trace from the transactions in a Block and ChainState
ledgerTraceFromBlock ::
  forall era ledger.
  ( ChainProperty era
  , EraSegWits era
  , TestingLedger era ledger
  ) =>
  ChainState era ->
  Block (BHeader (EraCrypto era)) era ->
  (ChainState era, Trace ledger)
ledgerTraceFromBlock :: forall era ledger.
(ChainProperty era, EraSegWits era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader (EraCrypto era)) era
-> (ChainState era, Trace ledger)
ledgerTraceFromBlock ChainState era
chainSt Block (BHeader (EraCrypto era)) era
block =
  ( ChainState era
tickedChainSt
  , forall a. ShelleyBase a -> a
runShelleyBase forall a b. (a -> b) -> a -> b
$
      forall s (m :: * -> *).
(STS s, m ~ BaseM s) =>
Environment s -> State s -> [Signal s] -> m (Trace s)
Trace.closure @ledger LedgerEnv era
ledgerEnv LedgerState era
ledgerSt0 [Tx era]
txs
  )
  where
    (ChainState era
tickedChainSt, LedgerEnv era
ledgerEnv, LedgerState era
ledgerSt0, [Tx era]
txs) = forall era.
(EraSegWits era, GetLedgerView era, ApplyBlock era) =>
ChainState era
-> Block (BHeader (EraCrypto era)) era
-> (ChainState era, LedgerEnv era, LedgerState era, [Tx era])
ledgerTraceBase ChainState era
chainSt Block (BHeader (EraCrypto era)) era
block

-- | This function is nearly the same as ledgerTraceFromBlock, but
-- it restricts the UTxO state to only those needed by the block.
-- It also returns the unused UTxO for comparison later.
ledgerTraceFromBlockWithRestrictedUTxO ::
  forall era ledger.
  ( ChainProperty era
  , EraSegWits era
  , TestingLedger era ledger
  ) =>
  ChainState era ->
  Block (BHeader (EraCrypto era)) era ->
  (UTxO era, Trace ledger)
ledgerTraceFromBlockWithRestrictedUTxO :: forall era ledger.
(ChainProperty era, EraSegWits era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader (EraCrypto era)) era -> (UTxO era, Trace ledger)
ledgerTraceFromBlockWithRestrictedUTxO ChainState era
chainSt Block (BHeader (EraCrypto era)) era
block =
  ( forall era. Map (TxIn (EraCrypto era)) (TxOut era) -> UTxO era
UTxO Map (TxIn (EraCrypto era)) (TxOut era)
irrelevantUTxO
  , forall a. ShelleyBase a -> a
runShelleyBase forall a b. (a -> b) -> a -> b
$
      forall s (m :: * -> *).
(STS s, m ~ BaseM s) =>
Environment s -> State s -> [Signal s] -> m (Trace s)
Trace.closure @ledger LedgerEnv era
ledgerEnv LedgerState era
ledgerSt0' [Tx era]
txs
  )
  where
    (ChainState era
_tickedChainSt, LedgerEnv era
ledgerEnv, LedgerState era
ledgerSt0, [Tx era]
txs) = forall era.
(EraSegWits era, GetLedgerView era, ApplyBlock era) =>
ChainState era
-> Block (BHeader (EraCrypto era)) era
-> (ChainState era, LedgerEnv era, LedgerState era, [Tx era])
ledgerTraceBase ChainState era
chainSt Block (BHeader (EraCrypto era)) era
block
    txIns :: Set (TxIn (EraCrypto era))
txIns = forall h era.
EraSegWits era =>
Block h era -> Set (TxIn (EraCrypto era))
neededTxInsForBlock Block (BHeader (EraCrypto era)) era
block
    LedgerState UTxOState era
utxoSt CertState era
delegationSt = LedgerState era
ledgerSt0
    utxo :: Map (TxIn (EraCrypto era)) (TxOut era)
utxo = forall era. UTxO era -> Map (TxIn (EraCrypto era)) (TxOut era)
unUTxO forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. UTxOState era -> UTxO era
utxosUtxo forall a b. (a -> b) -> a -> b
$ UTxOState era
utxoSt
    (Map (TxIn (EraCrypto era)) (TxOut era)
relevantUTxO, Map (TxIn (EraCrypto era)) (TxOut era)
irrelevantUTxO) = forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey (forall a b. a -> b -> a
const forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (TxIn (EraCrypto era))
txIns)) Map (TxIn (EraCrypto era)) (TxOut era)
utxo
    ledgerSt0' :: LedgerState era
ledgerSt0' = forall era. UTxOState era -> CertState era -> LedgerState era
LedgerState (UTxOState era
utxoSt {utxosUtxo :: UTxO era
utxosUtxo = forall era. Map (TxIn (EraCrypto era)) (TxOut era) -> UTxO era
UTxO Map (TxIn (EraCrypto era)) (TxOut era)
relevantUTxO}) CertState era
delegationSt

-- | Reconstruct a POOL trace from the transactions in a Block and ChainState
poolTraceFromBlock ::
  forall era.
  ( ChainProperty era
  , ShelleyEraTxBody era
  , EraSegWits era
  ) =>
  ChainState era ->
  Block (BHeader (EraCrypto era)) era ->
  (ChainState era, Trace (ShelleyPOOL era))
poolTraceFromBlock :: forall era.
(ChainProperty era, ShelleyEraTxBody era, EraSegWits era) =>
ChainState era
-> Block (BHeader (EraCrypto era)) era
-> (ChainState era, Trace (ShelleyPOOL era))
poolTraceFromBlock ChainState era
chainSt Block (BHeader (EraCrypto era)) era
block =
  ( ChainState era
tickedChainSt
  , forall a. ShelleyBase a -> a
runShelleyBase forall a b. (a -> b) -> a -> b
$
      forall s (m :: * -> *).
(STS s, m ~ BaseM s) =>
Environment s -> State s -> [Signal s] -> m (Trace s)
Trace.closure @(ShelleyPOOL era) PoolEnv era
poolEnv PState era
poolSt0 [PoolCert (EraCrypto era)]
poolCerts
  )
  where
    (ChainState era
tickedChainSt, LedgerEnv era
ledgerEnv, LedgerState era
ledgerSt0, [Tx era]
txs) = forall era.
(EraSegWits era, GetLedgerView era, ApplyBlock era) =>
ChainState era
-> Block (BHeader (EraCrypto era)) era
-> (ChainState era, LedgerEnv era, LedgerState era, [Tx era])
ledgerTraceBase ChainState era
chainSt Block (BHeader (EraCrypto era)) era
block
    certs :: [Tx era] -> [TxCert era]
certs = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a s. Getting a s a -> s -> a
view forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictSeq (TxCert era))
certsTxBodyL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a s. Getting a s a -> s -> a
view forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL)
    poolCerts :: [PoolCert (EraCrypto era)]
poolCerts = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall era.
EraTxCert era =>
TxCert era -> Maybe (PoolCert (EraCrypto era))
getPoolCertTxCert ([Tx era] -> [TxCert era]
certs [Tx era]
txs)
    poolEnv :: PoolEnv era
poolEnv =
      let (LedgerEnv SlotNo
s TxIx
_ PParams era
pp AccountState
_ Bool
_) = LedgerEnv era
ledgerEnv
       in forall era. SlotNo -> PParams era -> PoolEnv era
PoolEnv SlotNo
s PParams era
pp
    poolSt0 :: PState era
poolSt0 =
      forall era. CertState era -> PState era
certPState (forall era. LedgerState era -> CertState era
lsCertState LedgerState era
ledgerSt0)

-- | Reconstruct a DELEG trace from all the transaction certificates in a Block
delegTraceFromBlock ::
  forall era.
  ( ChainProperty era
  , ShelleyEraTxBody era
  , EraSegWits era
  ) =>
  ChainState era ->
  Block (BHeader (EraCrypto era)) era ->
  (DelegEnv era, Trace (ShelleyDELEG era))
delegTraceFromBlock :: forall era.
(ChainProperty era, ShelleyEraTxBody era, EraSegWits era) =>
ChainState era
-> Block (BHeader (EraCrypto era)) era
-> (DelegEnv era, Trace (ShelleyDELEG era))
delegTraceFromBlock ChainState era
chainSt Block (BHeader (EraCrypto era)) era
block =
  ( DelegEnv era
delegEnv
  , forall a. ShelleyBase a -> a
runShelleyBase forall a b. (a -> b) -> a -> b
$
      forall s (m :: * -> *).
(STS s, m ~ BaseM s) =>
Environment s -> State s -> [Signal s] -> m (Trace s)
Trace.closure @(ShelleyDELEG era) DelegEnv era
delegEnv DState era
delegSt0 [TxCert era]
blockCerts
  )
  where
    (ChainState era
_tickedChainSt, LedgerEnv era
ledgerEnv, LedgerState era
ledgerSt0, [Tx era]
txs) = forall era.
(EraSegWits era, GetLedgerView era, ApplyBlock era) =>
ChainState era
-> Block (BHeader (EraCrypto era)) era
-> (ChainState era, LedgerEnv era, LedgerState era, [Tx era])
ledgerTraceBase ChainState era
chainSt Block (BHeader (EraCrypto era)) era
block
    certs :: [Tx era] -> [TxCert era]
certs = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a s. Getting a s a -> s -> a
view forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictSeq (TxCert era))
certsTxBodyL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a s. Getting a s a -> s -> a
view forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL)
    blockCerts :: [TxCert era]
blockCerts = forall a. (a -> Bool) -> [a] -> [a]
filter forall {era}.
(ProtVerIsInBounds
   "at most"
   era
   8
   (OrdCond (CmpNat (ProtVerLow era) 8) 'True 'True 'False),
 ShelleyEraTxCert era) =>
TxCert era -> Bool
delegCert ([Tx era] -> [TxCert era]
certs [Tx era]
txs)
    delegEnv :: DelegEnv era
delegEnv =
      let (LedgerEnv SlotNo
s TxIx
txIx PParams era
pp AccountState
reserves Bool
_) = LedgerEnv era
ledgerEnv
          dummyCertIx :: CertIx
dummyCertIx = forall a. Bounded a => a
minBound
          ptr :: Ptr
ptr = SlotNo -> TxIx -> CertIx -> Ptr
Ptr SlotNo
s TxIx
txIx CertIx
dummyCertIx
       in forall era.
SlotNo -> Ptr -> AccountState -> PParams era -> DelegEnv era
DelegEnv SlotNo
s Ptr
ptr AccountState
reserves PParams era
pp
    delegSt0 :: DState era
delegSt0 =
      forall era. CertState era -> DState era
certDState (forall era. LedgerState era -> CertState era
lsCertState LedgerState era
ledgerSt0)
    delegCert :: TxCert era -> Bool
delegCert (RegTxCert StakeCredential (EraCrypto era)
_) = Bool
True
    delegCert (UnRegTxCert StakeCredential (EraCrypto era)
_) = Bool
True
    delegCert (DelegStakeTxCert StakeCredential (EraCrypto era)
_ KeyHash 'StakePool (EraCrypto era)
_) = Bool
True
    delegCert (MirTxCert MIRCert (EraCrypto era)
_) = Bool
True
    delegCert TxCert era
_ = Bool
False

-- | Reconstruct a POOL trace from the transactions in a Block and ChainState
--
-- NOTE: we need to tick the slot before processing transactions
-- (in the same way that the CHAIN rule TICKs the slot before processing
-- transactions with the LEDGERS rule)
ledgerTraceBase ::
  forall era.
  ( EraSegWits era
  , GetLedgerView era
  , ApplyBlock era
  ) =>
  ChainState era ->
  Block (BHeader (EraCrypto era)) era ->
  (ChainState era, LedgerEnv era, LedgerState era, [Tx era])
ledgerTraceBase :: forall era.
(EraSegWits era, GetLedgerView era, ApplyBlock era) =>
ChainState era
-> Block (BHeader (EraCrypto era)) era
-> (ChainState era, LedgerEnv era, LedgerState era, [Tx era])
ledgerTraceBase ChainState era
chainSt Block (BHeader (EraCrypto era)) era
block =
  ( ChainState era
tickedChainSt
  , forall era.
SlotNo
-> TxIx -> PParams era -> AccountState -> Bool -> LedgerEnv era
LedgerEnv SlotNo
slot forall a. Bounded a => a
minBound PParams era
pp_ (forall era. EpochState era -> AccountState
esAccountState EpochState era
nes) Bool
False
  , forall era. EpochState era -> LedgerState era
esLState EpochState era
nes
  , [Tx era]
txs
  )
  where
    (UnserialisedBlock (BHeader BHBody (EraCrypto era)
bhb SignedKES (EraCrypto era) (BHBody (EraCrypto era))
_) TxSeq era
txSeq) = Block (BHeader (EraCrypto era)) era
block
    slot :: SlotNo
slot = forall c. BHBody c -> SlotNo
bheaderSlotNo BHBody (EraCrypto era)
bhb
    tickedChainSt :: ChainState era
tickedChainSt = forall era.
(GetLedgerView era, ApplyBlock era) =>
SlotNo -> ChainState era -> ChainState era
tickChainState SlotNo
slot ChainState era
chainSt
    nes :: EpochState era
nes = (forall era. NewEpochState era -> EpochState era
nesEs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. ChainState era -> NewEpochState era
chainNes) ChainState era
tickedChainSt
    pp_ :: PParams era
pp_ = EpochState era
nes forall s a. s -> Getting a s a -> a
^. forall era. EraGov era => Lens' (EpochState era) (PParams era)
curPParamsEpochStateL
    -- Oldest to Newest first
    txs :: [Tx era]
txs = (forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraSegWits era => TxSeq era -> StrictSeq (Tx era)
fromTxSeq) TxSeq era
txSeq -- HERE WE USE SOME SegWit function

-- | Transform the [(source, signal, target)] of a CHAIN Trace
-- by manually applying the Chain TICK Rule to each source and producing
-- [(source, signal, target')].
--
-- This allows for testing properties on Chain traces while excluding the effects
-- of Transactions and Certificates. For example we can check that pools that are
-- due for retirement at an epoch transition, are indeed retired.
--
-- Had we not excluded the effects of Transactions/Certificates, we might have
-- a pool that was correctly retired, but is again registered by a certificate
-- in the block following the transition.
chainSstWithTick ::
  forall era.
  ChainProperty era =>
  Trace (CHAIN era) ->
  [SourceSignalTarget (CHAIN era)]
chainSstWithTick :: forall era.
ChainProperty era =>
Trace (CHAIN era) -> [SourceSignalTarget (CHAIN era)]
chainSstWithTick Trace (CHAIN era)
ledgerTr =
  forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget (CHAIN era) -> SourceSignalTarget (CHAIN era)
applyTick (forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (CHAIN era)
ledgerTr)
  where
    applyTick :: SourceSignalTarget (CHAIN era) -> SourceSignalTarget (CHAIN era)
applyTick sst :: SourceSignalTarget (CHAIN era)
sst@SourceSignalTarget {source :: forall a. SourceSignalTarget a -> State a
source = State (CHAIN era)
chainSt, signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal (CHAIN era)
block} =
      let bh :: BHeader (EraCrypto era)
bh = forall h era. Block h era -> h
bheader Signal (CHAIN era)
block
          slot :: SlotNo
slot = (forall c. BHBody c -> SlotNo
bheaderSlotNo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c. Crypto c => BHeader c -> BHBody c
bhbody) BHeader (EraCrypto era)
bh
       in SourceSignalTarget (CHAIN era)
sst {target :: State (CHAIN era)
target = forall era.
(GetLedgerView era, ApplyBlock era) =>
SlotNo -> ChainState era -> ChainState era
tickChainState @era SlotNo
slot State (CHAIN era)
chainSt}

---------------------------
-- Utils --
---------------------------

forAllChainTrace ::
  forall era prop.
  ( Testable prop
  , EraGen era
  , QC.HasTrace (CHAIN era) (GenEnv era)
  , EraGov era
  ) =>
  Word64 -> -- trace length
  Constants ->
  (Trace (CHAIN era) -> prop) ->
  Property
forAllChainTrace :: forall era prop.
(Testable prop, EraGen era, HasTrace (CHAIN era) (GenEnv era),
 EraGov era) =>
Word64 -> Constants -> (Trace (CHAIN era) -> prop) -> Property
forAllChainTrace Word64
n Constants
constants Trace (CHAIN era) -> prop
prop =
  forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess (forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
numberOfTests) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$
    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
      Globals
testGlobals
      Word64
n
      (forall era. EraGen era => Proxy era -> Constants -> GenEnv era
Preset.genEnv Proxy era
p Constants
constants)
      (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall era a.
(EraGen era, EraGov era) =>
GenEnv era -> IRC (CHAIN era) -> Gen (Either a (ChainState era))
mkGenesisChainState (forall era. EraGen era => Proxy era -> Constants -> GenEnv era
Preset.genEnv Proxy era
p Constants
constants))
      Trace (CHAIN era) -> prop
prop
  where
    p :: Proxy era
    p :: Proxy era
p = forall {k} (t :: k). Proxy t
Proxy

-- | Test a property on the first 'subtracecount' sub-Traces that end on an EpochBoundary
forEachEpochTrace ::
  forall era prop.
  ( EraGen era
  , Testable prop
  , QC.HasTrace (CHAIN era) (GenEnv era)
  , EraGov era
  ) =>
  Int ->
  Word64 ->
  Constants ->
  (Trace (CHAIN era) -> prop) ->
  Property
forEachEpochTrace :: forall era prop.
(EraGen era, Testable prop, HasTrace (CHAIN era) (GenEnv era),
 EraGov era) =>
Int
-> Word64 -> Constants -> (Trace (CHAIN era) -> prop) -> Property
forEachEpochTrace Int
subtracecount Word64
tracelen Constants
constants Trace (CHAIN era) -> prop
f = forall era prop.
(Testable prop, EraGen era, HasTrace (CHAIN era) (GenEnv era),
 EraGov era) =>
Word64 -> Constants -> (Trace (CHAIN era) -> prop) -> Property
forAllChainTrace Word64
tracelen Constants
constants Trace (CHAIN era) -> Property
action
  where
    -- split at contiguous elements with different Epoch numbers
    p :: ChainState era -> ChainState era -> Bool
p ChainState era
new ChainState era
old = (forall era. NewEpochState era -> EpochNo
nesEL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. ChainState era -> NewEpochState era
chainNes) ChainState era
new forall a. Eq a => a -> a -> Bool
/= (forall era. NewEpochState era -> EpochNo
nesEL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. ChainState era -> NewEpochState era
chainNes) ChainState era
old
    -- At a minimum throw away the last trace which is probably an incomplete epoch
    action :: Trace (CHAIN era) -> Property
action Trace (CHAIN era)
tr = forall prop. Testable prop => [prop] -> Property
conjoin forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Trace (CHAIN era) -> prop
f (forall a. Int -> [a] -> [a]
take (forall a. Ord a => a -> a -> a
min Int
subtracecount (Int
m forall a. Num a => a -> a -> a
- Int
1)) (forall a. [a] -> [a]
reverse [Trace (CHAIN era)]
traces))
      where
        traces :: [Trace (CHAIN era)]
traces = forall s. (State s -> State s -> Bool) -> Trace s -> [Trace s]
splitTrace forall {era} {era}. ChainState era -> ChainState era -> Bool
p Trace (CHAIN era)
tr
        m :: Int
m = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Trace (CHAIN era)]
traces

-- ================================
-- an example how one might debug one test, which can be replayed
-- import Test.Tasty (defaultMain)
-- main :: IO ()
-- main = defaultMain (minimal @(ShelleyEra TestCrypto))
-- Then in ghci, one can just type
-- :main --quickcheck-replay=443873
-- =================================