{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Tests where

import Cardano.Ledger.Api
import Cardano.Ledger.BaseTypes hiding (inject)
import Cardano.Ledger.CertState
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.EpochBoundary (SnapShots (..))
import Cardano.Ledger.Keys (KeyHash, KeyRole (..))
import Cardano.Ledger.PoolParams (PoolParams (..))
import Cardano.Ledger.Shelley.LedgerState (
  EpochState (..),
  LedgerState (..),
  NewEpochState (..),
  UTxOState (..),
 )
import Cardano.Ledger.UTxO (UTxO (..))
import Constrained hiding (Value)
import Data.Kind (Type)
import Data.Map (Map)
import Data.Typeable
import Test.Cardano.Ledger.Constrained.Conway ()
import Test.Cardano.Ledger.Constrained.Conway.Cert (
  testConwayCert,
  testGenesisCert,
  testShelleyCert,
 )
import Test.Cardano.Ledger.Constrained.Conway.Instances
import Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs
import Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.WellFormed
import Test.Cardano.Ledger.Constrained.Conway.PParams (pparamsSpec)
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse
import Test.Cardano.Ledger.Generic.PrettyCore (PrettyA (prettyA))
import Test.Hspec
import Test.Hspec.QuickCheck (prop)
import Test.QuickCheck (
  Gen,
  Property,
  counterexample,
  property,
  withMaxSuccess,
 )

-- ====================================================================================
-- Some Specifications are constrained by types (say 'x') that do not appear in the type being
-- specified. We use the strategy of passing (Term fn x) as inputs to those specifcations.
-- For example, the AccountState must have sufficient capacity to support the InstantaneousRewards
-- So we pass a (Term fn AccountState) as input to 'instantaneousRewardsSpec' which then
-- constrains both the AccountState Term and the 'instantaneousRewardsSpec' so that they are consistent.
-- In order to create tests, we need specifications that are fully applied, so we write combinators
-- to lift (Term a -> Spec b) functions to (Specification a -> Gen(Specification b))
-- The idea is to combine several Specifications to get a Gen(composed specifations)
-- For example (dstateSpec @Shelley !$! accountStateSpec !*! poolMapSpec)
-- is a (Gen (Specification ConwayFn (DState Shelley)))
-- If a Specification takes an actual PParams (not a (Term fn PParams)), like
-- lederstateSpec, we can combine it like this using the Functor <$>, rather than our !$!
-- (ledgerStateSpec <$> genConwayFn pparamsSpec !*! accountStateSpec !*! epochNoSpec)
-- ====================================================================================

-- GenFromSpec fixed at ConwayFn
genConwayFn :: (HasCallStack, HasSpec ConwayFn a) => Specification ConwayFn a -> Gen a
genConwayFn :: forall a.
(HasCallStack, HasSpec ConwayFn a) =>
Specification ConwayFn a -> Gen a
genConwayFn = forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn

-- Analagous to <$> except the function to be applied takes a (Term fn a -> t) instead of (a -> t)
infixr 6 !$!
(!$!) ::
  forall fn t a.
  HasSpec fn a =>
  (Term fn a -> t) -> Specification fn a -> Gen t
!$! :: forall (fn :: Univ) t a.
HasSpec fn a =>
(Term fn a -> t) -> Specification fn a -> Gen t
(!$!) Term fn a -> t
bf Specification fn a
specA = do a
a <- forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @fn @a Specification fn a
specA; forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term fn a -> t
bf (forall a (fn :: Univ). Show a => a -> Term fn a
lit a
a))

-- Analagous to <*> except the function to be applied takes a Gen (Term fn a -> t) instead of F (a -> t)
infixl 4 !*!
(!*!) ::
  forall fn t a.
  HasSpec fn a =>
  Gen (Term fn a -> t) -> Specification fn a -> Gen t
!*! :: forall (fn :: Univ) t a.
HasSpec fn a =>
Gen (Term fn a -> t) -> Specification fn a -> Gen t
(!*!) Gen (Term fn a -> t)
gentf Specification fn a
specA = do a
a <- forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @fn @a Specification fn a
specA; Term fn a -> t
f <- Gen (Term fn a -> t)
gentf; forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term fn a -> t
f (forall a (fn :: Univ). Show a => a -> Term fn a
lit a
a))

poolMapSpec ::
  Specification ConwayFn (Map (KeyHash 'StakePool) PoolParams)
poolMapSpec :: Specification ConwayFn (Map (KeyHash 'StakePool) PoolParams)
poolMapSpec = forall (fn :: Univ) t.
(HasSpec fn t, Sized fn t) =>
SizeSpec fn -> Specification fn t
hasSize (forall (fn :: Univ). Integer -> Integer -> SizeSpec fn
rangeSize Integer
8 Integer
8)

delegationsSpec ::
  Specification
    ConwayFn
    (Map (Credential 'Staking) (KeyHash 'StakePool))
delegationsSpec :: Specification
  ConwayFn (Map (Credential 'Staking) (KeyHash 'StakePool))
delegationsSpec = (forall (fn :: Univ) t.
(HasSpec fn t, Sized fn t) =>
SizeSpec fn -> Specification fn t
hasSize (forall (fn :: Univ). Integer -> Integer -> SizeSpec fn
rangeSize Integer
8 Integer
12))

-- ====================================================================
-- HSpec tests
-- ===================================================================

soundSpec ::
  forall t. (HasSpec ConwayFn t, PrettyA t) => Gen (Specification ConwayFn t) -> Gen Property
soundSpec :: forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Gen (Specification ConwayFn t) -> Gen Property
soundSpec Gen (Specification ConwayFn t)
specGen = do
  Specification
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  t
spect <- Gen (Specification ConwayFn t)
specGen
  t
x <- forall a.
(HasCallStack, HasSpec ConwayFn a) =>
Specification ConwayFn a -> Gen a
genConwayFn @t Specification
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  t
spect
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
    forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$
      forall prop. Testable prop => String -> prop -> Property
counterexample (forall a. Show a => a -> String
show (PDoc
"Does not meet spec\n" forall a. Semigroup a => a -> a -> a
<> forall t. PrettyA t => t -> PDoc
prettyA t
x)) (forall (fn :: Univ) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
conformsToSpec t
x Specification
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  t
spect)

soundSpecWith ::
  forall t.
  (HasSpec ConwayFn t, PrettyA t) =>
  Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith :: forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith Int
n Gen (Specification ConwayFn t)
specx = forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it (forall a. Show a => a -> String
show (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t))) forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
n forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$ (forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Gen (Specification ConwayFn t) -> Gen Property
soundSpec @t Gen (Specification ConwayFn t)
specx)

-- | A bunch of soundness tests on different LederTypes, all in the same Era.
--   The idea is to run this suite on every era.
specSuite ::
  forall (era :: Type).
  ( EraSpecLedger era ConwayFn
  , PrettyA (GovState era)
  ) =>
  Int -> Spec
specSuite :: forall era.
(EraSpecLedger era ConwayFn, PrettyA (GovState era)) =>
Int -> Spec
specSuite Int
n = do
  let universe :: Gen (WitUniv era)
universe = forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
200

  forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith @(PState era) (Int
5 forall a. Num a => a -> a -> a
* Int
n) (forall (fn :: Univ) era.
(IsConwayUniv fn, Era era) =>
WitUniv era -> Term fn EpochNo -> Specification fn (PState era)
pstateSpec @ConwayFn @era forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (WitUniv era)
universe forall (fn :: Univ) t a.
HasSpec fn a =>
Gen (Term fn a -> t) -> Specification fn a -> Gen t
!*! forall (fn :: Univ). IsConwayUniv fn => Specification fn EpochNo
epochNoSpec)

  forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith @(DState era)
    (Int
5 forall a. Num a => a -> a -> a
* Int
n)
    forall a b. (a -> b) -> a -> b
$ do
      WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
50
      (forall era (fn :: Univ).
EraSpecLedger era fn =>
WitUniv era
-> Term fn AccountState
-> Term fn (Map (KeyHash 'StakePool) PoolParams)
-> Specification fn (DState era)
dstateSpec @era WitUniv era
univ forall (fn :: Univ) t a.
HasSpec fn a =>
(Term fn a -> t) -> Specification fn a -> Gen t
!$! forall (fn :: Univ).
IsConwayUniv fn =>
Specification fn AccountState
accountStateSpec forall (fn :: Univ) t a.
HasSpec fn a =>
Gen (Term fn a -> t) -> Specification fn a -> Gen t
!*! Specification ConwayFn (Map (KeyHash 'StakePool) PoolParams)
poolMapSpec)

  forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith @(VState era)
    (Int
10 forall a. Num a => a -> a -> a
* Int
n)
    forall a b. (a -> b) -> a -> b
$ do
      WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
25
      ( forall (fn :: Univ) era.
(IsConwayUniv fn, Era era) =>
WitUniv era
-> Term fn EpochNo
-> Term fn (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
-> Specification fn (VState era)
vstateSpec @_ @era WitUniv era
univ
          forall (fn :: Univ) t a.
HasSpec fn a =>
(Term fn a -> t) -> Specification fn a -> Gen t
!$! forall (fn :: Univ). IsConwayUniv fn => Specification fn EpochNo
epochNoSpec
          forall (fn :: Univ) t a.
HasSpec fn a =>
Gen (Term fn a -> t) -> Specification fn a -> Gen t
!*! (forall era.
WitUniv era
-> Specification
     ConwayFn (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
goodDrep @era WitUniv era
univ)
        )

  forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith @(CertState era)
    (Int
5 forall a. Num a => a -> a -> a
* Int
n)
    forall a b. (a -> b) -> a -> b
$ do
      WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
50
      (forall era (fn :: Univ).
EraSpecLedger era fn =>
WitUniv era
-> Term fn AccountState
-> Term fn EpochNo
-> Specification fn (CertState era)
certStateSpec @era @ConwayFn WitUniv era
univ {- (lit drepRoleCredSet) -} forall (fn :: Univ) t a.
HasSpec fn a =>
(Term fn a -> t) -> Specification fn a -> Gen t
!$! forall (fn :: Univ).
IsConwayUniv fn =>
Specification fn AccountState
accountStateSpec forall (fn :: Univ) t a.
HasSpec fn a =>
Gen (Term fn a -> t) -> Specification fn a -> Gen t
!*! forall (fn :: Univ). IsConwayUniv fn => Specification fn EpochNo
epochNoSpec)

  forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith @(UTxO era) (Int
5 forall a. Num a => a -> a -> a
* Int
n) (forall era (fn :: Univ).
EraSpecTxOut era fn =>
WitUniv era
-> Term fn (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Specification fn (UTxO era)
utxoSpecWit @era forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (WitUniv era)
universe forall (fn :: Univ) t a.
HasSpec fn a =>
Gen (Term fn a -> t) -> Specification fn a -> Gen t
!*! Specification
  ConwayFn (Map (Credential 'Staking) (KeyHash 'StakePool))
delegationsSpec)

  forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith @(UTxOState era) (Int
2 forall a. Num a => a -> a -> a
* Int
n) (forall era.
EraSpecLedger era ConwayFn =>
Gen (Specification ConwayFn (UTxOState era))
utxoStateGen @era)

  forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith @(GovState era)
    (Int
2 forall a. Num a => a -> a -> a
* Int
n)
    (do PParams era
x <- forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec (forall (fn :: Univ) era.
(EraSpecPParams era, BaseUniverse fn) =>
Specification fn (PParams era)
pparamsSpec @ConwayFn); forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall era (fn :: Univ).
EraSpecLedger era fn =>
PParams era -> Specification fn (GovState era)
govStateSpec @era PParams era
x)

  forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith @(LedgerState era)
    (Int
2 forall a. Num a => a -> a -> a
* Int
n)
    ( forall era (fn :: Univ).
EraSpecLedger era fn =>
PParams era
-> WitUniv era
-> Term fn AccountState
-> Term fn EpochNo
-> Specification fn (LedgerState era)
ledgerStateSpec
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
(HasCallStack, HasSpec ConwayFn a) =>
Specification ConwayFn a -> Gen a
genConwayFn forall (fn :: Univ) era.
(EraSpecPParams era, BaseUniverse fn) =>
Specification fn (PParams era)
pparamsSpec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
100 forall (fn :: Univ) t a.
HasSpec fn a =>
Gen (Term fn a -> t) -> Specification fn a -> Gen t
!*! forall (fn :: Univ).
IsConwayUniv fn =>
Specification fn AccountState
accountStateSpec forall (fn :: Univ) t a.
HasSpec fn a =>
Gen (Term fn a -> t) -> Specification fn a -> Gen t
!*! forall (fn :: Univ). IsConwayUniv fn => Specification fn EpochNo
epochNoSpec
    )
  forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith @(EpochState era)
    (Int
2 forall a. Num a => a -> a -> a
* Int
n)
    (forall era (fn :: Univ).
EraSpecLedger era fn =>
PParams era
-> WitUniv era
-> Term fn EpochNo
-> Specification fn (EpochState era)
epochStateSpec @era forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
(HasCallStack, HasSpec ConwayFn a) =>
Specification ConwayFn a -> Gen a
genConwayFn forall (fn :: Univ) era.
(EraSpecPParams era, BaseUniverse fn) =>
Specification fn (PParams era)
pparamsSpec forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
50 forall (fn :: Univ) t a.
HasSpec fn a =>
Gen (Term fn a -> t) -> Specification fn a -> Gen t
!*! forall (fn :: Univ). IsConwayUniv fn => Specification fn EpochNo
epochNoSpec)
  forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith @(NewEpochState era)
    (Int
2 forall a. Num a => a -> a -> a
* Int
n)
    (forall era (fn :: Univ).
EraSpecLedger era fn =>
PParams era -> WitUniv era -> Specification fn (NewEpochState era)
newEpochStateSpec @era forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
(HasCallStack, HasSpec ConwayFn a) =>
Specification ConwayFn a -> Gen a
genConwayFn forall (fn :: Univ) era.
(EraSpecPParams era, BaseUniverse fn) =>
Specification fn (PParams era)
pparamsSpec forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
50)

spec :: Spec
spec :: Spec
spec = do
  forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"Classify GenesisCert" (forall era.
(AtMostEra BabbageEra era, EraSpecDeleg era, EraSpecPParams era,
 GenScript era) =>
Gen Property
testGenesisCert @ShelleyEra)
  forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"Classify ShelleyCert" (forall era.
(Era era, AtMostEra BabbageEra era, EraSpecPParams era,
 EraSpecDeleg era, GenScript era) =>
Gen Property
testShelleyCert @BabbageEra)
  forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"Classify ConwayCert" Gen Property
testConwayCert
  forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Soundness of WellFormed types from the Cardano Ledger: " forall a b. (a -> b) -> a -> b
$ do
    forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith @(ProtVer, ProtVer) Int
100 (forall (f :: * -> *) a. Applicative f => a -> f a
pure Specification ConwayFn (ProtVer, ProtVer)
protVersCanfollow)
    forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith @InstantaneousRewards
      Int
20
      (forall era (fn :: Univ).
EraSpecTxOut era fn =>
WitUniv era
-> Term fn AccountState -> Specification fn InstantaneousRewards
irewardSpec @ShelleyEra (forall era. EraUniverse era => Int -> WitUniv era
eraWitUniv @ShelleyEra Int
50) forall (fn :: Univ) t a.
HasSpec fn a =>
(Term fn a -> t) -> Specification fn a -> Gen t
!$! forall (fn :: Univ).
IsConwayUniv fn =>
Specification fn AccountState
accountStateSpec)
    forall t.
(HasSpec ConwayFn t, PrettyA t) =>
Int -> Gen (Specification ConwayFn t) -> SpecWith (Arg Property)
soundSpecWith @SnapShots
      Int
10
      (forall (fn :: Univ).
IsConwayUniv fn =>
Term fn SnapShot -> Specification fn SnapShots
snapShotsSpec forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((forall a (fn :: Univ). Show a => a -> Term fn a
lit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. LedgerState era -> SnapShot
getMarkSnapShot) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall t era. WellFormed t era => Gen t
wff @(LedgerState ConwayEra) @ConwayEra)))
  forall era.
(EraSpecLedger era ConwayFn, PrettyA (GovState era)) =>
Int -> Spec
specSuite @ShelleyEra Int
10
  forall era.
(EraSpecLedger era ConwayFn, PrettyA (GovState era)) =>
Int -> Spec
specSuite @AllegraEra Int
10
  forall era.
(EraSpecLedger era ConwayFn, PrettyA (GovState era)) =>
Int -> Spec
specSuite @MaryEra Int
10
  forall era.
(EraSpecLedger era ConwayFn, PrettyA (GovState era)) =>
Int -> Spec
specSuite @AlonzoEra Int
10
  forall era.
(EraSpecLedger era ConwayFn, PrettyA (GovState era)) =>
Int -> Spec
specSuite @BabbageEra Int
10
  forall era.
(EraSpecLedger era ConwayFn, PrettyA (GovState era)) =>
Int -> Spec
specSuite @ConwayEra Int
10

utxoStateGen ::
  forall era. EraSpecLedger era ConwayFn => Gen (Specification ConwayFn (UTxOState era))
utxoStateGen :: forall era.
EraSpecLedger era ConwayFn =>
Gen (Specification ConwayFn (UTxOState era))
utxoStateGen =
  forall era (fn :: Univ).
EraSpecLedger era fn =>
PParams era
-> WitUniv era
-> Term fn (CertState era)
-> Specification fn (UTxOState era)
utxoStateSpec @era
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
(HasCallStack, HasSpec ConwayFn a) =>
Specification ConwayFn a -> Gen a
genConwayFn @(PParams era) forall (fn :: Univ) era.
(EraSpecPParams era, BaseUniverse fn) =>
Specification fn (PParams era)
pparamsSpec
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
25
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall a (fn :: Univ). Show a => a -> Term fn a
lit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t era. WellFormed t era => Gen t
wff @(CertState era) @era)