{-# 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.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,
 )

-- ====================================================================================
-- Some Specifications are constrained by types (say 'x') that do not appear in the type being
-- specified. We use the strategy of passing (Term x) as inputs to those specifcations.
-- For example, the AccountState must have sufficient capacity to support the InstantaneousRewards
-- So we pass a (Term 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 (DState Shelley)))
-- If a Specification takes an actual PParams (not a (Term PParams)), like
-- lederstateSpec, we can combine it like this using the Functor <$>, rather than our !$!
-- (ledgerStateSpec <$> genConwayFn pparamsSpec !*! accountStateSpec !*! epochNoSpec)
-- ====================================================================================

-- GenFromSpec fixed at
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

-- Analagous to <$> except the function to be applied takes a (Term a -> t) instead of (a -> t)
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))

-- Analagous to <*> except the function to be applied takes a Gen (Term a -> t) instead of F (a -> t)
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) StakePoolState)
poolRegSpec :: forall era.
Era era =>
WitUniv era
-> Specification (Map (KeyHash 'StakePool) StakePoolState)
poolRegSpec WitUniv era
univ = (Term (Map (KeyHash 'StakePool) StakePoolState) -> [Pred])
-> Specification (Map (KeyHash 'StakePool) StakePoolState)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map (KeyHash 'StakePool) StakePoolState) -> [Pred])
 -> Specification (Map (KeyHash 'StakePool) StakePoolState))
-> (Term (Map (KeyHash 'StakePool) StakePoolState) -> [Pred])
-> Specification (Map (KeyHash 'StakePool) StakePoolState)
forall a b. (a -> b) -> a -> b
$ \Term (Map (KeyHash 'StakePool) StakePoolState)
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) StakePoolState)
-> 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) StakePoolState)
poolRegMap)
  , WitUniv era -> Term [StakePoolState] -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash 'StakePool) StakePoolState)
-> Term [StakePoolState]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (KeyHash 'StakePool) StakePoolState)
poolRegMap)
  , Term (Map (KeyHash 'StakePool) StakePoolState)
-> Specification (Map (KeyHash 'StakePool) StakePoolState) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Map (KeyHash 'StakePool) StakePoolState)
poolRegMap (SizeSpec -> Specification (Map (KeyHash 'StakePool) StakePoolState)
forall t. (HasSpec t, Sized t) => SizeSpec -> Specification t
hasSize (Integer -> Integer -> SizeSpec
rangeSize Integer
8 Integer
12))
  ]

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

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)

-- | 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).
  ( 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) StakePoolState
poolreg <- Specification (Map (KeyHash 'StakePool) StakePoolState)
-> Gen (Map (KeyHash 'StakePool) StakePoolState)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (WitUniv era
-> Specification (Map (KeyHash 'StakePool) StakePoolState)
forall era.
Era era =>
WitUniv era
-> Specification (Map (KeyHash 'StakePool) StakePoolState)
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) StakePoolState)
-> Specification (DState era)
conwayDStateSpec @era WitUniv era
univ CertContext
context (Map (KeyHash 'StakePool) StakePoolState
-> Term (Map (KeyHash 'StakePool) StakePoolState)
forall a. HasSpec a => a -> Term a
lit Map (KeyHash 'StakePool) StakePoolState
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)