{-# 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.Core (PParamsHKD)
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.Keys (KeyHash, KeyRole (..))
import Cardano.Ledger.PoolParams (PoolParams (..))
import Cardano.Ledger.Shelley.LedgerState (
  EpochState (..),
  LedgerState (..),
  NewEpochState (..),
  StashedAVVMAddresses,
  UTxOState (..),
 )
import Constrained.API
import Data.Functor.Identity (Identity)
import Data.Kind (Type)
import Data.Map (Map)
import Data.TreeDiff
import Data.Typeable
import Test.Cardano.Ledger.Constrained.Conway.Cert (
  testConwayCert,
  testGenesisCert,
  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.ParametricSpec (irewardSpec)
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse
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 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))

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

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))

-- ====================================================================
-- 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).
  ( EraSpecLedger era
  , ToExpr (GovState era)
  , ToExpr (TxOut era)
  , ToExpr (InstantStake era)
  , ToExpr (PParamsHKD Identity era)
  , ToExpr (StashedAVVMAddresses era)
  , HasSpec (InstantStake era)
  , CertState era ~ ShelleyCertState era
  ) =>
  Int -> Spec
specSuite :: forall era.
(EraSpecLedger era, ToExpr (GovState era), ToExpr (TxOut era),
 ToExpr (InstantStake era), ToExpr (PParamsHKD Identity era),
 ToExpr (StashedAVVMAddresses era), HasSpec (InstantStake era),
 CertState era ~ ShelleyCertState 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) (forall era.
Era era =>
WitUniv era -> Term EpochNo -> Specification (PState era)
pstateSpec @era (WitUniv era -> Term EpochNo -> Specification (PState era))
-> Gen (WitUniv era)
-> Gen (Term EpochNo -> Specification (PState era))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (WitUniv era)
universe Gen (Term EpochNo -> Specification (PState era))
-> Specification EpochNo -> Gen (Specification (PState era))
forall t a.
HasSpec a =>
Gen (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
50
      forall era.
EraSpecLedger era =>
WitUniv era
-> Term ChainAccountState
-> Term (Map (KeyHash 'StakePool) PoolParams)
-> Specification (DState era)
dstateSpec @era WitUniv era
univ (Term ChainAccountState
 -> Term (Map (KeyHash 'StakePool) PoolParams)
 -> Specification (DState era))
-> Specification ChainAccountState
-> Gen
     (Term (Map (KeyHash 'StakePool) PoolParams)
      -> Specification (DState era))
forall t a. HasSpec a => (Term a -> t) -> Specification a -> Gen t
!$! Specification ChainAccountState
accountStateSpec Gen
  (Term (Map (KeyHash 'StakePool) PoolParams)
   -> Specification (DState era))
-> Specification (Map (KeyHash 'StakePool) PoolParams)
-> Gen (Specification (DState era))
forall t a.
HasSpec a =>
Gen (Term a -> t) -> Specification a -> Gen t
!*! Specification (Map (KeyHash 'StakePool) PoolParams)
poolMapSpec

  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
25
      ( forall era.
Era era =>
WitUniv era
-> Term EpochNo
-> Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
-> Specification (VState era)
vstateSpec @era WitUniv era
univ
          (Term EpochNo
 -> Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
 -> Specification (VState era))
-> Specification EpochNo
-> Gen
     (Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
      -> Specification (VState era))
forall t a. HasSpec a => (Term a -> t) -> Specification a -> Gen t
!$! Specification EpochNo
epochNoSpec
          Gen
  (Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
   -> Specification (VState era))
-> Specification
     (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
-> Gen (Specification (VState era))
forall t a.
HasSpec a =>
Gen (Term a -> t) -> Specification a -> Gen t
!*! (forall era.
WitUniv era
-> Specification
     (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
goodDrep @era WitUniv era
univ)
        )

  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
50
      (forall era.
EraSpecLedger era =>
WitUniv era
-> Term ChainAccountState
-> Term EpochNo
-> Specification (CertState era)
certStateSpec @era WitUniv era
univ {- (lit drepRoleCredSet) -} (Term ChainAccountState
 -> Term EpochNo -> SpecificationD Deps (ShelleyCertState era))
-> Specification ChainAccountState
-> Gen (Term EpochNo -> SpecificationD Deps (ShelleyCertState era))
forall t a. HasSpec a => (Term a -> t) -> Specification a -> Gen t
!$! Specification ChainAccountState
accountStateSpec Gen (Term EpochNo -> SpecificationD Deps (ShelleyCertState era))
-> Specification EpochNo
-> Gen (SpecificationD Deps (ShelleyCertState era))
forall t a.
HasSpec a =>
Gen (Term a -> t) -> Specification a -> Gen t
!*! Specification EpochNo
epochNoSpec)

  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) (forall era.
(WellFormed (CertState era) era, EraSpecLedger era) =>
Gen (Specification (UTxOState era))
utxoStateGen @era)

  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)
    (forall era.
EraSpecLedger era =>
PParams era -> Specification (GovState era)
govStateSpec @era (PParams era -> Specification (GovState era))
-> Gen (PParams era) -> Gen (Specification (GovState era))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Specification (PParams era) -> Gen (PParams era)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec Specification (PParams era)
forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec)

  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)
    ( PParams era
-> WitUniv era
-> Term ChainAccountState
-> Term EpochNo
-> Specification (LedgerState era)
forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era
-> WitUniv era
-> Term ChainAccountState
-> Term EpochNo
-> Specification (LedgerState era)
ledgerStateSpec
        (PParams era
 -> WitUniv era
 -> Term ChainAccountState
 -> Term EpochNo
 -> Specification (LedgerState era))
-> Gen (PParams era)
-> Gen
     (WitUniv era
      -> Term ChainAccountState
      -> Term EpochNo
      -> Specification (LedgerState era))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
        Gen
  (WitUniv era
   -> Term ChainAccountState
   -> Term EpochNo
   -> Specification (LedgerState era))
-> Gen (WitUniv era)
-> Gen
     (Term ChainAccountState
      -> Term EpochNo -> Specification (LedgerState era))
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 @era Int
100 Gen
  (Term ChainAccountState
   -> Term EpochNo -> Specification (LedgerState era))
-> Specification ChainAccountState
-> Gen (Term EpochNo -> Specification (LedgerState era))
forall t a.
HasSpec a =>
Gen (Term a -> t) -> Specification a -> Gen t
!*! Specification ChainAccountState
accountStateSpec Gen (Term EpochNo -> Specification (LedgerState era))
-> Specification EpochNo -> Gen (Specification (LedgerState era))
forall t a.
HasSpec a =>
Gen (Term a -> t) -> Specification a -> Gen t
!*! Specification EpochNo
epochNoSpec
    )
  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)
    (forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era
-> WitUniv era -> Term EpochNo -> Specification (EpochState era)
epochStateSpec @era (PParams era
 -> WitUniv era -> Term EpochNo -> Specification (EpochState era))
-> Gen (PParams era)
-> Gen
     (WitUniv era -> Term EpochNo -> Specification (EpochState era))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 Gen (WitUniv era -> Term EpochNo -> Specification (EpochState era))
-> Gen (WitUniv era)
-> Gen (Term EpochNo -> Specification (EpochState era))
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 @era Int
50 Gen (Term EpochNo -> Specification (EpochState era))
-> Specification EpochNo -> Gen (Specification (EpochState era))
forall t a.
HasSpec a =>
Gen (Term a -> t) -> Specification a -> Gen t
!*! Specification EpochNo
epochNoSpec)
  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)
    (forall era.
EraSpecLedger era =>
PParams era -> WitUniv era -> Specification (NewEpochState era)
newEpochStateSpec @era (PParams era -> WitUniv era -> Specification (NewEpochState era))
-> Gen (PParams era)
-> Gen (WitUniv era -> Specification (NewEpochState era))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 Gen (WitUniv era -> Specification (NewEpochState era))
-> Gen (WitUniv era) -> Gen (Specification (NewEpochState era))
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 @era Int
50)

spec :: Spec
spec :: Spec
spec = do
  String -> Gen Property -> Spec
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)
  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 @InstantaneousRewards
      Int
20
      (forall era.
EraSpecTxOut era =>
WitUniv era
-> Term ChainAccountState -> Specification InstantaneousRewards
irewardSpec @ShelleyEra (forall era. EraUniverse era => Int -> WitUniv era
eraWitUniv @ShelleyEra Int
50) (Term ChainAccountState -> Specification InstantaneousRewards)
-> Specification ChainAccountState
-> Gen (Specification InstantaneousRewards)
forall t a. HasSpec a => (Term a -> t) -> Specification a -> Gen t
!$! Specification ChainAccountState
accountStateSpec)
    forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @SnapShots
      Int
10
      (Term SnapShot -> Specification SnapShots
snapShotsSpec (Term SnapShot -> Specification SnapShots)
-> Gen (Term SnapShot) -> Gen (Specification SnapShots)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SnapShot -> Term SnapShot
forall a. HasSpec a => a -> Term a
lit (SnapShot -> Term SnapShot)
-> (LedgerState ConwayEra -> SnapShot)
-> LedgerState ConwayEra
-> Term SnapShot
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LedgerState ConwayEra -> SnapShot
forall era.
(EraCertState era, EraStake era) =>
LedgerState era -> SnapShot
getMarkSnapShot (LedgerState ConwayEra -> Term SnapShot)
-> Gen (LedgerState ConwayEra) -> Gen (Term SnapShot)
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, ToExpr (GovState era), ToExpr (TxOut era),
 ToExpr (InstantStake era), ToExpr (PParamsHKD Identity era),
 ToExpr (StashedAVVMAddresses era), HasSpec (InstantStake era),
 CertState era ~ ShelleyCertState era) =>
Int -> Spec
specSuite @ShelleyEra Int
10
  forall era.
(EraSpecLedger era, ToExpr (GovState era), ToExpr (TxOut era),
 ToExpr (InstantStake era), ToExpr (PParamsHKD Identity era),
 ToExpr (StashedAVVMAddresses era), HasSpec (InstantStake era),
 CertState era ~ ShelleyCertState era) =>
Int -> Spec
specSuite @AllegraEra Int
10
  forall era.
(EraSpecLedger era, ToExpr (GovState era), ToExpr (TxOut era),
 ToExpr (InstantStake era), ToExpr (PParamsHKD Identity era),
 ToExpr (StashedAVVMAddresses era), HasSpec (InstantStake era),
 CertState era ~ ShelleyCertState era) =>
Int -> Spec
specSuite @MaryEra Int
10
  forall era.
(EraSpecLedger era, ToExpr (GovState era), ToExpr (TxOut era),
 ToExpr (InstantStake era), ToExpr (PParamsHKD Identity era),
 ToExpr (StashedAVVMAddresses era), HasSpec (InstantStake era),
 CertState era ~ ShelleyCertState era) =>
Int -> Spec
specSuite @AlonzoEra Int
10
  forall era.
(EraSpecLedger era, ToExpr (GovState era), ToExpr (TxOut era),
 ToExpr (InstantStake era), ToExpr (PParamsHKD Identity era),
 ToExpr (StashedAVVMAddresses era), HasSpec (InstantStake era),
 CertState era ~ ShelleyCertState era) =>
Int -> Spec
specSuite @BabbageEra Int
10
  forall era.
(EraSpecLedger era, ToExpr (GovState era), ToExpr (TxOut era),
 ToExpr (InstantStake era), ToExpr (PParamsHKD Identity era),
 ToExpr (StashedAVVMAddresses era), HasSpec (InstantStake era),
 CertState era ~ ShelleyCertState era) =>
Int -> Spec
specSuite @ShelleyEra Int
10

utxoStateGen ::
  forall era.
  ( WellFormed (CertState era) era
  , EraSpecLedger era
  ) =>
  Gen (Specification (UTxOState era))
utxoStateGen :: forall era.
(WellFormed (CertState era) era, EraSpecLedger era) =>
Gen (Specification (UTxOState era))
utxoStateGen =
  forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era
-> WitUniv era
-> Term (CertState era)
-> Specification (UTxOState era)
utxoStateSpec @era
    (PParams era
 -> WitUniv era
 -> Term (CertState era)
 -> Specification (UTxOState era))
-> Gen (PParams era)
-> Gen
     (WitUniv era
      -> Term (CertState era) -> Specification (UTxOState era))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genConwayFn @(PParams era) Specification (PParams era)
forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec
    Gen
  (WitUniv era
   -> Term (CertState era) -> Specification (UTxOState era))
-> Gen (WitUniv era)
-> Gen (Term (CertState era) -> Specification (UTxOState era))
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 @era Int
25
    Gen (Term (CertState era) -> Specification (UTxOState era))
-> Gen (Term (CertState era))
-> Gen (Specification (UTxOState era))
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (CertState era -> Term (CertState era)
forall a. HasSpec a => a -> Term a
lit (CertState era -> Term (CertState era))
-> Gen (CertState era) -> Gen (Term (CertState era))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t era. WellFormed t era => Gen t
wff @(CertState era) @era)