{-# 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 #-}
#if __GLASGOW_HASKELL__ < 900
{-# OPTIONS_GHC -O0 #-}
#endif
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.PoolParams (PoolParams (..))
import Cardano.Ledger.Shelley.LedgerState
import Constrained.API
import Data.Map (Map)
import Test.Cardano.Ledger.Constrained.Conway.Instances
import Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs (
EraSpecLedger (..),
accountStateSpec,
aggregateDRep,
conwayGovStateSpec,
dstateSpec,
epochNoSpec,
epochStateSpec,
getMarkSnapShot,
govEnvSpec,
ledgerStateSpec,
pstateSpec,
shelleyGovStateSpec,
snapShotSpec,
snapShotsSpec,
utxoSpecWit,
utxoStateSpec,
vstateSpec,
)
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) 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 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) (forall era.
Era era =>
WitUniv era -> Term EpochNo -> Specification (PState era)
pstateSpec WitUniv era
univ (forall a. HasSpec a => a -> Term a
lit EpochNo
epoch))
dsX :: forall era. EraSpecLedger era => Gen (DState era)
dsX :: forall era. EraSpecLedger era => Gen (DState era)
dsX = do
WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv Int
25
ChainAccountState
acct <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @ChainAccountState Specification ChainAccountState
accountStateSpec
Map (KeyHash 'StakePool) PoolParams
pools <-
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(Map (KeyHash 'StakePool) PoolParams)
(forall t. (HasSpec t, Sized t) => SizeSpec -> Specification t
hasSize (Integer -> Integer -> SizeSpec
rangeSize Integer
8 Integer
8))
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(DState era) (forall era.
EraSpecLedger era =>
WitUniv era
-> Term ChainAccountState
-> Term (Map (KeyHash 'StakePool) PoolParams)
-> Specification (DState era)
dstateSpec @era WitUniv era
univ (forall a. HasSpec a => a -> Term a
lit ChainAccountState
acct) (forall a. HasSpec a => a -> Term a
lit Map (KeyHash 'StakePool) PoolParams
pools))
vsX :: forall era. GenScript era => Gen (VState era)
vsX :: forall era. GenScript era => Gen (VState era)
vsX = do
WitUniv era
univ <- 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))
delegatees <-
Map (Credential 'Staking) DRep
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
aggregateDRep
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec
@(Map (Credential 'Staking) DRep)
forall a. Specification a
TrueSpec
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(VState era) (forall era.
Era era =>
WitUniv era
-> Term EpochNo
-> Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
-> Specification (VState era)
vstateSpec WitUniv era
univ (forall a. HasSpec a => a -> Term a
lit EpochNo
epoch) (forall a. HasSpec a => a -> Term a
lit Map (Credential 'DRepRole) (Set (Credential 'Staking))
delegatees))
csX :: forall era. EraSpecLedger era => Gen (CertState era)
csX :: forall era. EraSpecLedger era => Gen (CertState era)
csX = do
WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv Int
25
ChainAccountState
acct <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @ChainAccountState Specification ChainAccountState
accountStateSpec
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 @(CertState era)
(forall era.
EraSpecLedger era =>
WitUniv era
-> Term ChainAccountState
-> Term EpochNo
-> Specification (CertState era)
certStateSpec WitUniv era
univ (forall a. HasSpec a => a -> Term a
lit ChainAccountState
acct) (forall a. HasSpec a => a -> Term a
lit EpochNo
epoch))
utxoX :: forall era. EraSpecLedger era => Gen (UTxO era)
utxoX :: forall era. EraSpecLedger era => 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))
(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 (forall a. HasSpec a => a -> Term a
lit Map (Credential 'Staking) (KeyHash 'StakePool)
cs))
utxostateX ::
forall era.
( EraSpecLedger era
, HasSpec (InstantStake era)
) =>
PParams era ->
Gen (UTxOState era)
utxostateX :: forall era.
(EraSpecLedger era, 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
CertState era
certstate <- forall era. EraSpecLedger era => Gen (CertState era)
csX @era
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(UTxOState era) (forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era
-> WitUniv era
-> Term (CertState era)
-> Specification (UTxOState era)
utxoStateSpec PParams era
pp WitUniv era
univ (forall a. HasSpec a => a -> Term a
lit CertState era
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) (EraSpecLedger ConwayEra =>
PParams ConwayEra
-> GovEnv ConwayEra -> Specification (ConwayGovState ConwayEra)
conwayGovStateSpec PParams ConwayEra
pp GovEnv ConwayEra
env)
lsX ::
forall era.
( EraSpecLedger era
, HasSpec (InstantStake era)
) =>
PParams era ->
Gen (LedgerState era)
lsX :: forall era.
(EraSpecLedger era, 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
50
ChainAccountState
acct <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @ChainAccountState Specification ChainAccountState
accountStateSpec
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) (forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era
-> WitUniv era
-> Term ChainAccountState
-> Term EpochNo
-> Specification (LedgerState era)
ledgerStateSpec PParams era
pp WitUniv era
univ (forall a. HasSpec a => a -> Term a
lit ChainAccountState
acct) (forall a. HasSpec a => a -> Term a
lit EpochNo
epoch))
esX ::
forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era ->
Gen (EpochState era)
esX :: forall era.
(EraSpecLedger era, 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
50
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) (forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era
-> WitUniv era -> Term EpochNo -> Specification (EpochState era)
epochStateSpec PParams era
pp WitUniv era
univ (forall a. HasSpec a => a -> Term a
lit EpochNo
epoch))
nesX ::
forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era ->
Gen (NewEpochState era)
nesX :: forall era.
(EraSpecLedger era, 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
50
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(NewEpochState era) (forall era.
EraSpecLedger era =>
PParams era -> WitUniv era -> Specification (NewEpochState era)
newEpochStateSpec PParams era
pp WitUniv era
univ)
snapX :: Gen SnapShot
snapX :: Gen SnapShot
snapX = forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @SnapShot Specification SnapShot
snapShotSpec
snapsX ::
forall era.
( EraSpecLedger era
, HasSpec (InstantStake era)
) =>
PParams era ->
Gen SnapShots
snapsX :: forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
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
50
ChainAccountState
acct <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @ChainAccountState Specification ChainAccountState
accountStateSpec
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) (forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era
-> WitUniv era
-> Term ChainAccountState
-> Term EpochNo
-> Specification (LedgerState era)
ledgerStateSpec PParams era
pp WitUniv era
univ (forall a. HasSpec a => a -> Term a
lit ChainAccountState
acct) (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 (forall a. HasSpec a => a -> Term a
lit (forall era.
(EraCertState era, EraStake era) =>
LedgerState era -> SnapShot
getMarkSnapShot LedgerState era
ls)))
instanRewX :: forall era. EraSpecTxOut era => Gen InstantaneousRewards
instanRewX :: forall era. 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 (forall a. HasSpec a => a -> Term a
lit ChainAccountState
acct))
class
( EraSpecPParams era
, HasSpec (InstantStake era)
, HasSpec t
) =>
WellFormed t era
where
wffWithPP :: PParams era -> Gen t
wffWithPP PParams era
_ = forall t era. WellFormed t era => Gen t
wff @t @era
wff :: Gen t
wff = do
PParams era
pp <- forall era. EraSpecPParams era => Gen (PParams era)
ppX @era
forall t era. WellFormed t era => PParams era -> Gen t
wffWithPP PParams era
pp
instance (EraSpecPParams era, HasSpec (InstantStake era)) => WellFormed (PParams era) era where
wff :: Gen (PParams era)
wff = forall era. EraSpecPParams era => Gen (PParams era)
ppX @era
wffWithPP :: PParams era -> Gen (PParams era)
wffWithPP = forall (f :: * -> *) a. Applicative f => a -> f a
pure
instance (EraSpecPParams era, HasSpec (InstantStake era)) => WellFormed ChainAccountState era where
wff :: Gen ChainAccountState
wff = Gen ChainAccountState
acctX
wffWithPP :: PParams era -> Gen ChainAccountState
wffWithPP PParams era
_ = Gen ChainAccountState
acctX
instance
(GenScript era, HasSpec (InstantStake era), EraSpecPParams era) =>
WellFormed (PState era) era
where
wff :: Gen (PState era)
wff = forall era. GenScript era => Gen (PState era)
psX
wffWithPP :: PParams era -> Gen (PState era)
wffWithPP PParams era
_ = forall era. GenScript era => Gen (PState era)
psX
instance
(EraSpecPParams era, HasSpec (InstantStake era), EraSpecLedger era) =>
WellFormed (DState era) era
where
wff :: Gen (DState era)
wff = forall era. EraSpecLedger era => Gen (DState era)
dsX
wffWithPP :: PParams era -> Gen (DState era)
wffWithPP PParams era
_ = forall era. EraSpecLedger era => Gen (DState era)
dsX
instance
(GenScript era, HasSpec (InstantStake era), EraSpecPParams era) =>
WellFormed (VState era) era
where
wff :: Gen (VState era)
wff = forall era. GenScript era => Gen (VState era)
vsX
wffWithPP :: PParams era -> Gen (VState era)
wffWithPP PParams era
_ = forall era. GenScript era => Gen (VState era)
vsX
instance
( EraSpecPParams era
, EraSpecLedger era
, HasSpec (InstantStake era)
, CertState era ~ ShelleyCertState era
) =>
WellFormed (ShelleyCertState era) era
where
wff :: Gen (ShelleyCertState era)
wff = forall era. EraSpecLedger era => Gen (CertState era)
csX
instance
( EraSpecPParams era
, EraSpecLedger era
, HasSpec (InstantStake era)
, IsNormalType (CertState era)
) =>
WellFormed (UTxO era) era
where
wff :: Gen (UTxO era)
wff = forall era. EraSpecLedger era => Gen (UTxO era)
utxoX
instance
( EraSpecPParams era
, EraSpecLedger era
, IsNormalType (CertState era)
, HasSpec (InstantStake era)
) =>
WellFormed (UTxOState era) era
where
wffWithPP :: PParams era -> Gen (UTxOState era)
wffWithPP = forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era -> Gen (UTxOState era)
utxostateX
instance WellFormed (GovEnv ConwayEra) ConwayEra where
wffWithPP :: PParams ConwayEra -> Gen (GovEnv ConwayEra)
wffWithPP = PParams ConwayEra -> Gen (GovEnv ConwayEra)
govenvX
instance WellFormed (ConwayGovState ConwayEra) ConwayEra where
wffWithPP :: PParams ConwayEra -> Gen (ConwayGovState ConwayEra)
wffWithPP = PParams ConwayEra -> Gen (ConwayGovState ConwayEra)
conwaygovX
instance
( EraSpecPParams era
, EraSpecLedger era
, HasSpec (InstantStake era)
, IsNormalType (CertState era)
) =>
WellFormed (ShelleyGovState era) era
where
wffWithPP :: PParams era -> Gen (ShelleyGovState era)
wffWithPP PParams era
pp = forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(ShelleyGovState era) (forall era.
EraSpecLedger era =>
PParams era -> Specification (ShelleyGovState era)
shelleyGovStateSpec PParams era
pp)
instance
( EraSpecPParams era
, HasSpec (InstantStake era)
, EraSpecLedger era
, IsNormalType (CertState era)
) =>
WellFormed (LedgerState era) era
where
wffWithPP :: PParams era -> Gen (LedgerState era)
wffWithPP = forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era -> Gen (LedgerState era)
lsX
instance
( EraSpecPParams era
, EraSpecLedger era
, HasSpec (InstantStake era)
, IsNormalType (CertState era)
) =>
WellFormed (EpochState era) era
where
wffWithPP :: PParams era -> Gen (EpochState era)
wffWithPP = forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era -> Gen (EpochState era)
esX
instance
(EraSpecPParams era, HasSpec (InstantStake era), EraSpecLedger era) =>
WellFormed (NewEpochState era) era
where
wffWithPP :: PParams era -> Gen (NewEpochState era)
wffWithPP = forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era -> Gen (NewEpochState era)
nesX
instance (EraSpecPParams era, HasSpec (InstantStake era)) => WellFormed SnapShot era where
wff :: Gen SnapShot
wff = Gen SnapShot
snapX
instance
( EraSpecPParams era
, EraSpecLedger era
, HasSpec (InstantStake era)
, IsNormalType (CertState era)
) =>
WellFormed SnapShots era
where
wffWithPP :: PParams era -> Gen SnapShots
wffWithPP = forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era -> Gen SnapShots
snapsX @era
instance
(EraSpecPParams era, HasSpec (InstantStake era), EraSpecTxOut era) =>
WellFormed InstantaneousRewards era
where
wff :: Gen InstantaneousRewards
wff = forall era. EraSpecTxOut era => Gen InstantaneousRewards
instanRewX @era