{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# 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.ConcreteCryptoTypes (MockCrypto)
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,
epochFromSlotNo,
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,
)
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
)
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))
ledgerTraceFromBlock ::
forall era ledger.
( ChainProperty era
, EraSegWits era
, TestingLedger era ledger
) =>
ChainState era ->
Block (BHeader MockCrypto) era ->
(ChainState era, Trace ledger)
ledgerTraceFromBlock :: forall era ledger.
(ChainProperty era, EraSegWits era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader MockCrypto) era -> (ChainState era, Trace ledger)
ledgerTraceFromBlock ChainState era
chainSt Block (BHeader MockCrypto) 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 MockCrypto) era
-> (ChainState era, LedgerEnv era, LedgerState era, [Tx era])
ledgerTraceBase ChainState era
chainSt Block (BHeader MockCrypto) era
block
ledgerTraceFromBlockWithRestrictedUTxO ::
forall era ledger.
( ChainProperty era
, EraSegWits era
, TestingLedger era ledger
) =>
ChainState era ->
Block (BHeader MockCrypto) era ->
(UTxO era, Trace ledger)
ledgerTraceFromBlockWithRestrictedUTxO :: forall era ledger.
(ChainProperty era, EraSegWits era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader MockCrypto) era -> (UTxO era, Trace ledger)
ledgerTraceFromBlockWithRestrictedUTxO ChainState era
chainSt Block (BHeader MockCrypto) era
block =
( forall era. Map TxIn (TxOut era) -> UTxO era
UTxO Map TxIn (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 MockCrypto) era
-> (ChainState era, LedgerEnv era, LedgerState era, [Tx era])
ledgerTraceBase ChainState era
chainSt Block (BHeader MockCrypto) era
block
txIns :: Set TxIn
txIns = forall h era. EraSegWits era => Block h era -> Set TxIn
neededTxInsForBlock Block (BHeader MockCrypto) era
block
LedgerState UTxOState era
utxoSt CertState era
delegationSt = LedgerState era
ledgerSt0
utxo :: Map TxIn (TxOut era)
utxo = forall era. UTxO era -> Map TxIn (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 (TxOut era)
relevantUTxO, Map TxIn (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
txIns)) Map TxIn (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 (TxOut era) -> UTxO era
UTxO Map TxIn (TxOut era)
relevantUTxO}) CertState era
delegationSt
poolTraceFromBlock ::
forall era.
( ChainProperty era
, ShelleyEraTxBody era
, EraSegWits era
) =>
ChainState era ->
Block (BHeader MockCrypto) era ->
(ChainState era, Trace (ShelleyPOOL era))
poolTraceFromBlock :: forall era.
(ChainProperty era, ShelleyEraTxBody era, EraSegWits era) =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, Trace (ShelleyPOOL era))
poolTraceFromBlock ChainState era
chainSt Block (BHeader MockCrypto) 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]
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 MockCrypto) era
-> (ChainState era, LedgerEnv era, LedgerState era, [Tx era])
ledgerTraceBase ChainState era
chainSt Block (BHeader MockCrypto) 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]
poolCerts = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall era. EraTxCert era => TxCert era -> Maybe PoolCert
getPoolCertTxCert ([Tx era] -> [TxCert era]
certs [Tx era]
txs)
poolEnv :: PoolEnv era
poolEnv =
let (LedgerEnv SlotNo
sl Maybe EpochNo
_ TxIx
_ PParams era
pp AccountState
_ Bool
_) = LedgerEnv era
ledgerEnv
in forall era. EpochNo -> PParams era -> PoolEnv era
PoolEnv (SlotNo -> EpochNo
epochFromSlotNo SlotNo
sl) PParams era
pp
poolSt0 :: PState era
poolSt0 =
forall era. CertState era -> PState era
certPState (forall era. LedgerState era -> CertState era
lsCertState LedgerState era
ledgerSt0)
delegTraceFromBlock ::
forall era.
( ChainProperty era
, ShelleyEraTxBody era
, EraSegWits era
) =>
ChainState era ->
Block (BHeader MockCrypto) era ->
(DelegEnv era, Trace (ShelleyDELEG era))
delegTraceFromBlock :: forall era.
(ChainProperty era, ShelleyEraTxBody era, EraSegWits era) =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (DelegEnv era, Trace (ShelleyDELEG era))
delegTraceFromBlock ChainState era
chainSt Block (BHeader MockCrypto) 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 MockCrypto) era
-> (ChainState era, LedgerEnv era, LedgerState era, [Tx era])
ledgerTraceBase ChainState era
chainSt Block (BHeader MockCrypto) 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 Maybe EpochNo
_ 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
-> EpochNo -> Ptr -> AccountState -> PParams era -> DelegEnv era
DelegEnv SlotNo
s (SlotNo -> EpochNo
epochFromSlotNo 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
_) = Bool
True
delegCert (UnRegTxCert StakeCredential
_) = Bool
True
delegCert (DelegStakeTxCert StakeCredential
_ KeyHash 'StakePool
_) = Bool
True
delegCert (MirTxCert MIRCert
_) = Bool
True
delegCert TxCert era
_ = Bool
False
ledgerTraceBase ::
forall era.
( EraSegWits era
, GetLedgerView era
, ApplyBlock era
) =>
ChainState era ->
Block (BHeader MockCrypto) era ->
(ChainState era, LedgerEnv era, LedgerState era, [Tx era])
ledgerTraceBase :: forall era.
(EraSegWits era, GetLedgerView era, ApplyBlock era) =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, LedgerEnv era, LedgerState era, [Tx era])
ledgerTraceBase ChainState era
chainSt Block (BHeader MockCrypto) era
block =
( ChainState era
tickedChainSt
, forall era.
SlotNo
-> Maybe EpochNo
-> TxIx
-> PParams era
-> AccountState
-> Bool
-> LedgerEnv era
LedgerEnv SlotNo
slot forall a. Maybe a
Nothing 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 MockCrypto
bhb SignedKES (KES MockCrypto) (BHBody MockCrypto)
_) TxSeq era
txSeq) = Block (BHeader MockCrypto) era
block
slot :: SlotNo
slot = forall c. BHBody c -> SlotNo
bheaderSlotNo BHBody MockCrypto
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
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
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 MockCrypto
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 MockCrypto
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}
forAllChainTrace ::
forall era prop.
( Testable prop
, EraGen era
, QC.HasTrace (CHAIN era) (GenEnv era)
, EraGov era
) =>
Word64 ->
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
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
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
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