{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.WellFormed where
import Cardano.Ledger.Api
import Cardano.Ledger.BaseTypes hiding (inject)
import Cardano.Ledger.Conway.Rules (GovEnv (..))
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.Keys (KeyHash, KeyRole (..))
import Cardano.Ledger.Shelley.LedgerState
import Constrained.API
import Data.Map (Map)
import Test.Cardano.Ledger.Constrained.Conway.Deleg (witnessedKeyHashPoolParamMapSpec)
import Test.Cardano.Ledger.Constrained.Conway.Instances
import Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs (
accountStateSpec,
conwayCertStateSpec,
conwayDStateSpec,
conwayGovStateSpec,
epochNoSpec,
epochStateSpec,
genCertContext,
getMarkSnapShot,
govEnvSpec,
ledgerStateSpec,
newEpochStateSpec,
pStateSpec,
snapShotSpec,
snapShotsSpec,
utxoSpecWit,
utxoStateSpec,
vStateSpec,
whoDelegatesSpec,
)
import Test.Cardano.Ledger.Constrained.Conway.PParams (pparamsSpec)
import Test.Cardano.Ledger.Constrained.Conway.ParametricSpec (EraSpecTxOut (..))
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse (GenScript (..), genWitUniv)
import Test.QuickCheck (Gen)
ppX :: forall era. EraSpecPParams era => Gen (PParams era)
ppX :: forall era. EraSpecPParams era => Gen (PParams era)
ppX = forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(PParams era) Specification (PParams era)
forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec
acctX :: Gen ChainAccountState
acctX :: Gen ChainAccountState
acctX = forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @ChainAccountState Specification ChainAccountState
accountStateSpec
psX :: forall era. GenScript era => Gen (PState era)
psX :: forall era. GenScript era => Gen (PState era)
psX = do
WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
25
EpochNo
epoch <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @EpochNo Specification EpochNo
epochNoSpec
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(PState era) (WitUniv era -> Term EpochNo -> Specification (PState era)
forall era.
Era era =>
WitUniv era -> Term EpochNo -> Specification (PState era)
pStateSpec WitUniv era
univ (EpochNo -> Term EpochNo
forall a. HasSpec a => a -> Term a
lit EpochNo
epoch))
dsX :: forall era. era ~ ConwayEra => Gen (DState era)
dsX :: forall era. (era ~ ConwayEra) => Gen (DState era)
dsX = do
WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
100
CertContext
context <- forall era. Era era => WitUniv era -> Gen CertContext
genCertContext @era WitUniv era
univ
Map (KeyHash 'StakePool) PoolParams
khppMap <- 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)
witnessedKeyHashPoolParamMapSpec WitUniv era
univ)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(DState era) (WitUniv era
-> CertContext
-> Term (Map (KeyHash 'StakePool) PoolParams)
-> Specification (DState era)
forall era.
(era ~ ConwayEra) =>
WitUniv era
-> CertContext
-> Term (Map (KeyHash 'StakePool) PoolParams)
-> Specification (DState era)
conwayDStateSpec 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
khppMap))
conwayDStateGen ::
forall era. era ~ ConwayEra => Gen (DState era)
conwayDStateGen :: forall era. (era ~ ConwayEra) => Gen (DState era)
conwayDStateGen = forall era. (era ~ ConwayEra) => Gen (DState era)
dsX @ConwayEra
vsX :: forall era. (GenScript era, era ~ ConwayEra) => Gen (VState era)
vsX :: forall era. (GenScript era, era ~ ConwayEra) => Gen (VState era)
vsX = do
WitUniv era
univ <- Int -> Gen (WitUniv era)
forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv Int
25
EpochNo
epoch <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @EpochNo Specification EpochNo
epochNoSpec
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 (WitUniv era
-> Specification
(Map (Credential 'DRepRole) (Set (Credential 'Staking)))
forall era.
Era era =>
WitUniv era
-> Specification
(Map (Credential 'DRepRole) (Set (Credential 'Staking)))
whoDelegatesSpec WitUniv era
univ)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(VState era) (WitUniv era
-> Term EpochNo
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
-> Specification (VState era)
forall era.
Era era =>
WitUniv era
-> Term EpochNo
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
-> Specification (VState era)
vStateSpec WitUniv era
univ (EpochNo -> Term EpochNo
forall a. HasSpec a => a -> Term a
lit EpochNo
epoch) Map (Credential 'DRepRole) (Set (Credential 'Staking))
whodelegates)
csX :: forall era. era ~ ConwayEra => Gen (CertState era)
csX :: forall era. (era ~ ConwayEra) => Gen (CertState era)
csX = do
WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
300
CertContext
context <- forall era. Era era => WitUniv era -> Gen CertContext
genCertContext @era WitUniv era
univ
Specification (ConwayCertState ConwayEra)
-> Gen (ConwayCertState ConwayEra)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (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 (Word64 -> EpochNo
EpochNo Word64
10)))
utxoX :: forall era. era ~ ConwayEra => Gen (UTxO era)
utxoX :: forall era. (era ~ ConwayEra) => Gen (UTxO era)
utxoX = do
WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
50
Map (Credential 'Staking) (KeyHash 'StakePool)
cs <-
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec
@(Map (Credential 'Staking) (KeyHash 'StakePool))
(SizeSpec
-> Specification (Map (Credential 'Staking) (KeyHash 'StakePool))
forall t. (HasSpec t, Sized t) => SizeSpec -> Specification t
hasSize (Integer -> Integer -> SizeSpec
rangeSize Integer
30 Integer
30))
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(UTxO era) (forall era.
EraSpecTxOut era =>
WitUniv era
-> Term (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Specification (UTxO era)
utxoSpecWit @era WitUniv era
univ (Map (Credential 'Staking) (KeyHash 'StakePool)
-> Term (Map (Credential 'Staking) (KeyHash 'StakePool))
forall a. HasSpec a => a -> Term a
lit Map (Credential 'Staking) (KeyHash 'StakePool)
cs))
utxostateX ::
forall era.
(era ~ ConwayEra, HasSpec (InstantStake era)) =>
PParams era ->
Gen (UTxOState era)
utxostateX :: forall era.
(era ~ ConwayEra, HasSpec (InstantStake era)) =>
PParams era -> Gen (UTxOState era)
utxostateX PParams era
pp = do
WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
50
ConwayCertState ConwayEra
certstate <- forall era. (era ~ ConwayEra) => Gen (CertState era)
csX @era
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(UTxOState era) (PParams era
-> WitUniv era
-> Term (CertState era)
-> Specification (UTxOState era)
forall era.
(HasSpec (InstantStake era), era ~ ConwayEra) =>
PParams era
-> WitUniv era
-> Term (CertState era)
-> Specification (UTxOState era)
utxoStateSpec PParams era
pp WitUniv era
univ (ConwayCertState ConwayEra -> Term (ConwayCertState ConwayEra)
forall a. HasSpec a => a -> Term a
lit ConwayCertState ConwayEra
certstate))
govenvX :: PParams ConwayEra -> Gen (GovEnv ConwayEra)
govenvX :: PParams ConwayEra -> Gen (GovEnv ConwayEra)
govenvX PParams ConwayEra
pp = forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(GovEnv ConwayEra) (PParams ConwayEra -> Specification (GovEnv ConwayEra)
govEnvSpec PParams ConwayEra
pp)
conwaygovX :: PParams ConwayEra -> Gen (ConwayGovState ConwayEra)
conwaygovX :: PParams ConwayEra -> Gen (ConwayGovState ConwayEra)
conwaygovX PParams ConwayEra
pp = do
GovEnv ConwayEra
env <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(GovEnv ConwayEra) (PParams ConwayEra -> Specification (GovEnv ConwayEra)
govEnvSpec PParams ConwayEra
pp)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(ConwayGovState ConwayEra) (PParams ConwayEra
-> GovEnv ConwayEra -> Specification (ConwayGovState ConwayEra)
conwayGovStateSpec PParams ConwayEra
pp GovEnv ConwayEra
env)
lsX ::
forall era. (era ~ ConwayEra, HasSpec (InstantStake era)) => PParams era -> Gen (LedgerState era)
lsX :: forall era.
(era ~ ConwayEra, HasSpec (InstantStake era)) =>
PParams era -> Gen (LedgerState era)
lsX PParams era
pp = 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
epoch <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @EpochNo Specification EpochNo
epochNoSpec
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(LedgerState era) (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
epoch))
esX ::
forall era.
(era ~ ConwayEra, HasSpec (InstantStake era)) =>
PParams era ->
Gen (EpochState era)
esX :: forall era.
(era ~ ConwayEra, HasSpec (InstantStake era)) =>
PParams era -> Gen (EpochState era)
esX PParams era
pp = 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
epoch <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @EpochNo Specification EpochNo
epochNoSpec
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(EpochState era) (PParams era
-> WitUniv era
-> CertContext
-> Term EpochNo
-> Specification (EpochState era)
forall era.
(HasSpec (InstantStake era), era ~ ConwayEra) =>
PParams era
-> WitUniv era
-> CertContext
-> Term EpochNo
-> Specification (EpochState era)
epochStateSpec PParams era
pp WitUniv era
univ CertContext
context (EpochNo -> Term EpochNo
forall a. HasSpec a => a -> Term a
lit EpochNo
epoch))
nesX ::
forall era.
(era ~ ConwayEra, HasSpec (InstantStake era)) =>
PParams era ->
Gen (NewEpochState era)
nesX :: forall era.
(era ~ ConwayEra, HasSpec (InstantStake era)) =>
PParams era -> Gen (NewEpochState era)
nesX PParams era
pp = 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
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(NewEpochState era) (PParams era
-> WitUniv era -> CertContext -> Specification (NewEpochState era)
forall era.
(HasSpec (InstantStake era), era ~ ConwayEra) =>
PParams era
-> WitUniv era -> CertContext -> Specification (NewEpochState era)
newEpochStateSpec PParams era
pp WitUniv era
univ CertContext
context)
snapX :: Gen SnapShot
snapX :: Gen SnapShot
snapX = forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @SnapShot Specification SnapShot
snapShotSpec
snapsX ::
forall era.
( HasSpec (InstantStake era)
, era ~ ConwayEra
) =>
PParams era ->
Gen SnapShots
snapsX :: forall era.
(HasSpec (InstantStake era), era ~ ConwayEra) =>
PParams era -> Gen SnapShots
snapsX PParams era
pp = 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
epoch <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @EpochNo Specification EpochNo
epochNoSpec
LedgerState era
ls <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(LedgerState era) (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
epoch))
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @SnapShots (Term SnapShot -> Specification SnapShots
snapShotsSpec (SnapShot -> Term SnapShot
forall a. HasSpec a => a -> Term a
lit (LedgerState era -> SnapShot
forall era.
(EraCertState era, EraStake era) =>
LedgerState era -> SnapShot
getMarkSnapShot LedgerState era
ls)))
instanRewX :: forall era. (era ~ ConwayEra, EraSpecTxOut era) => Gen InstantaneousRewards
instanRewX :: forall era.
(era ~ ConwayEra, EraSpecTxOut era) =>
Gen InstantaneousRewards
instanRewX = do
WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
50
ChainAccountState
acct <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @ChainAccountState Specification ChainAccountState
accountStateSpec
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @InstantaneousRewards
(forall era.
EraSpecTxOut era =>
WitUniv era
-> Term ChainAccountState -> Specification InstantaneousRewards
irewardSpec @era WitUniv era
univ (ChainAccountState -> Term ChainAccountState
forall a. HasSpec a => a -> Term a
lit ChainAccountState
acct))