{-# 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.Conway.State
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.Keys (KeyHash, KeyRole (..))
import Cardano.Ledger.PoolParams (PoolParams (..))
import Cardano.Ledger.Shelley.LedgerState (
EpochState (..),
LedgerState (..),
NewEpochState (..),
UTxOState (..),
)
import Constrained.API
import Data.Kind (Type)
import Data.Map (Map)
import Data.TreeDiff
import Data.Typeable
import Test.Cardano.Ledger.Constrained.Conway.Cert (
testConwayCert,
testShelleyCert,
)
import Test.Cardano.Ledger.Constrained.Conway.Instances.Basic (prettyE)
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.Conway.Era
import Test.Hspec hiding (context)
import Test.Hspec.QuickCheck (prop)
import Test.QuickCheck (
Gen,
Property,
counterexample,
property,
withMaxSuccess,
)
genConwayFn :: (HasCallStack, HasSpec a) => Specification a -> Gen a
genConwayFn :: forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genConwayFn = Specification a -> Gen a
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec
infixr 6 !$!
(!$!) ::
forall t a.
HasSpec a =>
(Term a -> t) -> Specification a -> Gen t
!$! :: forall t a. HasSpec a => (Term a -> t) -> Specification a -> Gen t
(!$!) Term a -> t
bf Specification a
specA = do a
a <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @a Specification a
specA; t -> Gen t
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term a -> t
bf (a -> Term a
forall a. HasSpec a => a -> Term a
lit a
a))
infixl 4 !*!
(!*!) ::
forall t a.
HasSpec a =>
Gen (Term a -> t) -> Specification a -> Gen t
!*! :: forall t a.
HasSpec a =>
Gen (Term a -> t) -> Specification a -> Gen t
(!*!) Gen (Term a -> t)
gentf Specification a
specA = do a
a <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @a Specification a
specA; Term a -> t
f <- Gen (Term a -> t)
gentf; t -> Gen t
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term a -> t
f (a -> Term a
forall a. HasSpec a => a -> Term a
lit a
a))
delegationsSpec ::
Specification
(Map (Credential 'Staking) (KeyHash 'StakePool))
delegationsSpec :: Specification (Map (Credential 'Staking) (KeyHash 'StakePool))
delegationsSpec = (SizeSpec
-> Specification (Map (Credential 'Staking) (KeyHash 'StakePool))
forall t. (HasSpec t, Sized t) => SizeSpec -> Specification t
hasSize (Integer -> Integer -> SizeSpec
rangeSize Integer
8 Integer
12))
poolRegSpec ::
forall era. Era era => WitUniv era -> Specification (Map (KeyHash 'StakePool) PoolParams)
poolRegSpec :: forall era.
Era era =>
WitUniv era -> Specification (Map (KeyHash 'StakePool) PoolParams)
poolRegSpec WitUniv era
univ = (Term (Map (KeyHash 'StakePool) PoolParams) -> [Pred])
-> Specification (Map (KeyHash 'StakePool) PoolParams)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map (KeyHash 'StakePool) PoolParams) -> [Pred])
-> Specification (Map (KeyHash 'StakePool) PoolParams))
-> (Term (Map (KeyHash 'StakePool) PoolParams) -> [Pred])
-> Specification (Map (KeyHash 'StakePool) PoolParams)
forall a b. (a -> b) -> a -> b
$ \Term (Map (KeyHash 'StakePool) PoolParams)
poolRegMap ->
[ WitUniv era -> Term (Set (KeyHash 'StakePool)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash 'StakePool) PoolParams)
-> Term (Set (KeyHash 'StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'StakePool) PoolParams)
poolRegMap)
, WitUniv era -> Term [PoolParams] -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash 'StakePool) PoolParams) -> Term [PoolParams]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (KeyHash 'StakePool) PoolParams)
poolRegMap)
, Term (Map (KeyHash 'StakePool) PoolParams)
-> Specification (Map (KeyHash 'StakePool) PoolParams) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Map (KeyHash 'StakePool) PoolParams)
poolRegMap (SizeSpec -> Specification (Map (KeyHash 'StakePool) PoolParams)
forall t. (HasSpec t, Sized t) => SizeSpec -> Specification t
hasSize (Integer -> Integer -> SizeSpec
rangeSize Integer
8 Integer
12))
]
soundSpec ::
forall t. (HasSpec t, ToExpr t) => Gen (Specification t) -> Gen Property
soundSpec :: forall t.
(HasSpec t, ToExpr t) =>
Gen (Specification t) -> Gen Property
soundSpec Gen (Specification t)
specGen = do
Specification t
spect <- Gen (Specification t)
specGen
t
x <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genConwayFn @t Specification t
spect
Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$
Property -> Property
forall prop. Testable prop => prop -> Property
property (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Doc -> String
forall a. Show a => a -> String
show (Doc
"Does not meet spec\n" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> t -> Doc
forall x. ToExpr x => x -> Doc
prettyE t
x)) (t -> Specification t -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
conformsToSpec t
x Specification t
spect)
soundSpecWith ::
forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith :: forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith Int
n Gen (Specification t)
specx = String -> Property -> SpecWith (Arg Property)
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it (TypeRep -> String
forall a. Show a => a -> String
show (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t))) (Property -> SpecWith (Arg Property))
-> Property -> SpecWith (Arg Property)
forall a b. (a -> b) -> a -> b
$ Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
n (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Gen Property -> Property
forall prop. Testable prop => prop -> Property
property (Gen Property -> Property) -> Gen Property -> Property
forall a b. (a -> b) -> a -> b
$ (forall t.
(HasSpec t, ToExpr t) =>
Gen (Specification t) -> Gen Property
soundSpec @t Gen (Specification t)
specx)
specSuite ::
forall (era :: Type).
( era ~ ConwayEra
, ShelleyEraTest era
) =>
Int -> Spec
specSuite :: forall era. (era ~ ConwayEra, ShelleyEraTest 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 t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(PState era) (Int
5 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n) (Gen (Specification (PState era)) -> SpecWith (Arg Property))
-> Gen (Specification (PState era)) -> SpecWith (Arg Property)
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
200
forall era.
Era era =>
WitUniv era -> Term EpochNo -> Specification (PState era)
pStateSpec @era WitUniv era
univ (Term EpochNo -> Specification (PState era))
-> Specification EpochNo -> Gen (Specification (PState era))
forall t a. HasSpec a => (Term a -> t) -> Specification a -> Gen t
!$! Specification EpochNo
epochNoSpec
forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(DState era) (Int
5 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n) (Gen (Specification (DState era)) -> SpecWith (Arg Property))
-> Gen (Specification (DState era)) -> SpecWith (Arg Property)
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
200
CertContext
context <- forall era. Era era => WitUniv era -> Gen CertContext
genCertContext @era WitUniv era
univ
Map (KeyHash 'StakePool) PoolParams
poolreg <- Specification (Map (KeyHash 'StakePool) PoolParams)
-> Gen (Map (KeyHash 'StakePool) PoolParams)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (WitUniv era -> Specification (Map (KeyHash 'StakePool) PoolParams)
forall era.
Era era =>
WitUniv era -> Specification (Map (KeyHash 'StakePool) PoolParams)
poolRegSpec WitUniv era
univ)
Specification (DState era) -> Gen (Specification (DState era))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era.
(era ~ ConwayEra) =>
WitUniv era
-> CertContext
-> Term (Map (KeyHash 'StakePool) PoolParams)
-> Specification (DState era)
conwayDStateSpec @era WitUniv era
univ CertContext
context (Map (KeyHash 'StakePool) PoolParams
-> Term (Map (KeyHash 'StakePool) PoolParams)
forall a. HasSpec a => a -> Term a
lit Map (KeyHash 'StakePool) PoolParams
poolreg))
forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(VState era) (Int
10 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n) (Gen (Specification (VState era)) -> SpecWith (Arg Property))
-> Gen (Specification (VState era)) -> SpecWith (Arg Property)
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
200
Map (Credential 'DRepRole) (Set (Credential 'Staking))
whodelegates <- Specification
(Map (Credential 'DRepRole) (Set (Credential 'Staking)))
-> Gen (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (forall era.
Era era =>
WitUniv era
-> Specification
(Map (Credential 'DRepRole) (Set (Credential 'Staking)))
goodDrep @era WitUniv era
univ)
EpochNo
epoch <- Specification EpochNo -> Gen EpochNo
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec Specification EpochNo
epochNoSpec
Specification (VState era) -> Gen (Specification (VState era))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era.
Era era =>
WitUniv era
-> Term EpochNo
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
-> Specification (VState era)
vStateSpec @era WitUniv era
univ (EpochNo -> Term EpochNo
forall a. HasSpec a => a -> Term a
lit EpochNo
epoch) Map (Credential 'DRepRole) (Set (Credential 'Staking))
whodelegates)
forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(CertState era) (Int
5 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n) (Gen (Specification (CertState era)) -> SpecWith (Arg Property))
-> Gen (Specification (CertState era)) -> SpecWith (Arg Property)
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
200
CertContext
context <- forall era. Era era => WitUniv era -> Gen CertContext
genCertContext @era WitUniv era
univ
EpochNo
epn <- Specification EpochNo -> Gen EpochNo
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec Specification EpochNo
epochNoSpec
Specification (ConwayCertState ConwayEra)
-> Gen (Specification (ConwayCertState ConwayEra))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WitUniv ConwayEra
-> CertContext
-> Term EpochNo
-> Specification (ConwayCertState ConwayEra)
conwayCertStateSpec WitUniv era
WitUniv ConwayEra
univ CertContext
context (EpochNo -> Term EpochNo
forall a. HasSpec a => a -> Term a
lit EpochNo
epn))
forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(UTxO era) (Int
5 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n) (forall era.
EraSpecTxOut era =>
WitUniv era
-> Term (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Specification (UTxO era)
utxoSpecWit @era (WitUniv era
-> Term (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Specification (UTxO era))
-> Gen (WitUniv era)
-> Gen
(Term (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Specification (UTxO era))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (WitUniv era)
universe Gen
(Term (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Specification (UTxO era))
-> Specification (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Gen (Specification (UTxO era))
forall t a.
HasSpec a =>
Gen (Term a -> t) -> Specification a -> Gen t
!*! Specification (Map (Credential 'Staking) (KeyHash 'StakePool))
delegationsSpec)
forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(UTxOState era) (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n) Gen (Specification (UTxOState era))
Gen (Specification (UTxOState ConwayEra))
utxoStateGen
forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(GovState era) (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n) (Gen (Specification (GovState era)) -> SpecWith (Arg Property))
-> Gen (Specification (GovState era)) -> SpecWith (Arg Property)
forall a b. (a -> b) -> a -> b
$ do
PParams ConwayEra
pp <- Specification (PParams ConwayEra) -> Gen (PParams ConwayEra)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec Specification (PParams ConwayEra)
forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec
Specification (ConwayGovState ConwayEra)
-> Gen (Specification (ConwayGovState ConwayEra))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PParams ConwayEra
-> GovEnv ConwayEra -> Specification (ConwayGovState ConwayEra)
conwayGovStateSpec PParams ConwayEra
pp (PParams ConwayEra -> GovEnv ConwayEra
testGovEnv PParams ConwayEra
pp))
forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(LedgerState era) (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n) (Gen (Specification (LedgerState era)) -> SpecWith (Arg Property))
-> Gen (Specification (LedgerState era)) -> SpecWith (Arg Property)
forall a b. (a -> b) -> a -> b
$ do
PParams era
pp <- Specification (PParams era) -> Gen (PParams era)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genConwayFn Specification (PParams era)
forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec
WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
200
CertContext
context <- forall era. Era era => WitUniv era -> Gen CertContext
genCertContext @era WitUniv era
univ
EpochNo
epn <- Specification EpochNo -> Gen EpochNo
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec Specification EpochNo
epochNoSpec
Specification (LedgerState era)
-> Gen (Specification (LedgerState era))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PParams era
-> WitUniv era
-> CertContext
-> Term EpochNo
-> Specification (LedgerState era)
forall era.
(HasSpec (InstantStake era), era ~ ConwayEra) =>
PParams era
-> WitUniv era
-> CertContext
-> Term EpochNo
-> Specification (LedgerState era)
ledgerStateSpec PParams era
pp WitUniv era
univ CertContext
context (EpochNo -> Term EpochNo
forall a. HasSpec a => a -> Term a
lit EpochNo
epn))
forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(EpochState era) (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n) (Gen (Specification (EpochState era)) -> SpecWith (Arg Property))
-> Gen (Specification (EpochState era)) -> SpecWith (Arg Property)
forall a b. (a -> b) -> a -> b
$ do
PParams era
pp <- Specification (PParams era) -> Gen (PParams era)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genConwayFn Specification (PParams era)
forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec
WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
200
CertContext
context <- forall era. Era era => WitUniv era -> Gen CertContext
genCertContext @era WitUniv era
univ
EpochNo
epn <- Specification EpochNo -> Gen EpochNo
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec Specification EpochNo
epochNoSpec
Specification (EpochState era)
-> Gen (Specification (EpochState era))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era.
(HasSpec (InstantStake era), era ~ ConwayEra) =>
PParams era
-> WitUniv era
-> CertContext
-> Term EpochNo
-> Specification (EpochState era)
epochStateSpec @era PParams era
pp WitUniv era
univ CertContext
context (EpochNo -> Term EpochNo
forall a. HasSpec a => a -> Term a
lit EpochNo
epn))
forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(NewEpochState era) (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n) (Gen (Specification (NewEpochState era))
-> SpecWith (Arg Property))
-> Gen (Specification (NewEpochState era))
-> SpecWith (Arg Property)
forall a b. (a -> b) -> a -> b
$ do
PParams era
pp <- Specification (PParams era) -> Gen (PParams era)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genConwayFn Specification (PParams era)
forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec
WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
200
CertContext
context <- forall era. Era era => WitUniv era -> Gen CertContext
genCertContext @era WitUniv era
univ
Specification (NewEpochState era)
-> Gen (Specification (NewEpochState era))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era.
(HasSpec (InstantStake era), era ~ ConwayEra) =>
PParams era
-> WitUniv era -> CertContext -> Specification (NewEpochState era)
newEpochStateSpec @era PParams era
pp WitUniv era
univ CertContext
context)
spec :: Spec
spec :: Spec
spec = do
String -> Gen Property -> Spec
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, EraCertState era) =>
Gen Property
testShelleyCert @BabbageEra)
String -> Gen Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"Classify ConwayCert" Gen Property
testConwayCert
String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Soundness of WellFormed types from the Cardano Ledger: " (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(ProtVer, ProtVer) Int
100 (Specification (ProtVer, ProtVer)
-> Gen (Specification (ProtVer, ProtVer))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Specification (ProtVer, ProtVer)
protVersCanfollow)
forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @SnapShots Int
10 (Gen (Specification SnapShots) -> SpecWith (Arg Property))
-> Gen (Specification SnapShots) -> SpecWith (Arg Property)
forall a b. (a -> b) -> a -> b
$ do
PParams ConwayEra
pp <- Specification (PParams ConwayEra) -> Gen (PParams ConwayEra)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genConwayFn Specification (PParams ConwayEra)
forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec
LedgerState ConwayEra
ls <- PParams ConwayEra -> Gen (LedgerState ConwayEra)
forall era.
(era ~ ConwayEra, HasSpec (InstantStake era)) =>
PParams era -> Gen (LedgerState era)
lsX PParams ConwayEra
pp
Specification SnapShots -> Gen (Specification SnapShots)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term SnapShot -> Specification SnapShots
snapShotsSpec (SnapShot -> Term SnapShot
forall a. HasSpec a => a -> Term a
lit (LedgerState ConwayEra -> SnapShot
forall era.
(EraCertState era, EraStake era) =>
LedgerState era -> SnapShot
getMarkSnapShot LedgerState ConwayEra
ls)))
forall era. (era ~ ConwayEra, ShelleyEraTest era) => Int -> Spec
specSuite @ConwayEra Int
10
utxoStateGen :: Gen (Specification (UTxOState ConwayEra))
utxoStateGen :: Gen (Specification (UTxOState ConwayEra))
utxoStateGen =
forall era.
(HasSpec (InstantStake era), era ~ ConwayEra) =>
PParams era
-> WitUniv era
-> Term (CertState era)
-> Specification (UTxOState era)
utxoStateSpec @ConwayEra
(PParams ConwayEra
-> WitUniv ConwayEra
-> TermD Deps (ConwayCertState ConwayEra)
-> Specification (UTxOState ConwayEra))
-> Gen (PParams ConwayEra)
-> Gen
(WitUniv ConwayEra
-> TermD Deps (ConwayCertState ConwayEra)
-> Specification (UTxOState ConwayEra))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genConwayFn @(PParams ConwayEra) Specification (PParams ConwayEra)
forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec
Gen
(WitUniv ConwayEra
-> TermD Deps (ConwayCertState ConwayEra)
-> Specification (UTxOState ConwayEra))
-> Gen (WitUniv ConwayEra)
-> Gen
(TermD Deps (ConwayCertState ConwayEra)
-> Specification (UTxOState ConwayEra))
forall a b. Gen (a -> b) -> Gen a -> Gen b
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 @ConwayEra Int
25
Gen
(TermD Deps (ConwayCertState ConwayEra)
-> Specification (UTxOState ConwayEra))
-> Gen (TermD Deps (ConwayCertState ConwayEra))
-> Gen (Specification (UTxOState ConwayEra))
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (ConwayCertState ConwayEra -> TermD Deps (ConwayCertState ConwayEra)
forall a. HasSpec a => a -> Term a
lit (ConwayCertState ConwayEra
-> TermD Deps (ConwayCertState ConwayEra))
-> Gen (ConwayCertState ConwayEra)
-> Gen (TermD Deps (ConwayCertState ConwayEra))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era. (era ~ ConwayEra) => Gen (CertState era)
csX @ConwayEra)