| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs
Description
Specs necessary to generate constrained (well formed) values of types that appear in the Cardano Ledger Types. These Specifications are Era parametric, and one can use them to generate well formed values in any era (Shelley,Allegra,Mary,Alonzo,Babbage,Conway) by type applying them to a particular era type. These specifications are a usefull guide to building ones own specifications with one's own idea of whats well formed.
Synopsis
- class (EraSpecTxOut era, EraStake era, HasSpec (GovState era), HasSpec (CertState era), IsNormalType (CertState era), EraCertState era) ⇒ EraSpecLedger era where
- govStateSpec ∷ PParams era → Specification (GovState era)
- newEpochStateSpec ∷ PParams era → WitUniv era → Specification (NewEpochState era)
- certStateSpec ∷ WitUniv era → Term ChainAccountState → Term EpochNo → Specification (CertState era)
- testGovEnv ∷ PParams ConwayEra → GovEnv ConwayEra
- domEqualRng ∷ (Ord ptr, Ord cred, HasSpec cred, HasSpec ptr, HasSpec ume, IsNormalType cred, IsNormalType ptr, IsNormalType ume) ⇒ Term (Map ptr cred) → Term (Map cred ume) → Pred
- canFollow ∷ Term ProtVer → Term ProtVer → Pred
- protVersCanfollow ∷ Specification (ProtVer, ProtVer)
- goodDrep ∷ ∀ era. WitUniv era → Specification (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
- vstateSpec ∷ ∀ era. Era era ⇒ WitUniv era → Term EpochNo → Term (Map (Credential 'DRepRole) (Set (Credential 'Staking))) → Specification (VState era)
- getDelegatees ∷ DState era → Map (Credential 'DRepRole) (Set (Credential 'Staking))
- aggregateDRep ∷ Map (Credential 'Staking) DRep → Map (Credential 'DRepRole) (Set (Credential 'Staking))
- dstateSpec ∷ ∀ era. EraSpecLedger era ⇒ WitUniv era → Term ChainAccountState → Term (Map (KeyHash 'StakePool) PoolParams) → Specification (DState era)
- epochNoSpec ∷ Specification EpochNo
- pstateSpec ∷ Era era ⇒ WitUniv era → Term EpochNo → Specification (PState era)
- accountStateSpec ∷ Specification ChainAccountState
- shelleyCertStateSpec ∷ ∀ era. EraSpecLedger era ⇒ WitUniv era → Term ChainAccountState → Term EpochNo → Specification (ShelleyCertState era)
- conwayCertStateSpec ∷ EraSpecLedger ConwayEra ⇒ WitUniv ConwayEra → Term ChainAccountState → Term EpochNo → Specification (ConwayCertState ConwayEra)
- utxoSpecWit ∷ ∀ era. EraSpecTxOut era ⇒ WitUniv era → Term (Map (Credential 'Staking) (KeyHash 'StakePool)) → Specification (UTxO era)
- utxoStateSpec ∷ ∀ era. (EraSpecLedger era, HasSpec (InstantStake era)) ⇒ PParams era → WitUniv era → Term (CertState era) → Specification (UTxOState era)
- getDelegs ∷ ∀ era. EraCertState era ⇒ CertState era → Map (Credential 'Staking) (KeyHash 'StakePool)
- shelleyGovStateSpec ∷ ∀ era. EraSpecLedger era ⇒ PParams era → Specification (ShelleyGovState era)
- govEnvSpec ∷ PParams ConwayEra → Specification (GovEnv ConwayEra)
- conwayGovStateSpec ∷ EraSpecLedger ConwayEra ⇒ PParams ConwayEra → GovEnv ConwayEra → Specification (ConwayGovState ConwayEra)
- ledgerStateSpec ∷ ∀ era. (EraSpecLedger era, HasSpec (InstantStake era)) ⇒ PParams era → WitUniv era → Term ChainAccountState → Term EpochNo → Specification (LedgerState era)
- snapShotSpec ∷ Specification SnapShot
- snapShotsSpec ∷ Term SnapShot → Specification SnapShots
- getMarkSnapShot ∷ ∀ era. (EraCertState era, EraStake era) ⇒ LedgerState era → SnapShot
- epochStateSpec ∷ ∀ era. (EraSpecLedger era, HasSpec (InstantStake era)) ⇒ PParams era → WitUniv era → Term EpochNo → Specification (EpochState era)
- getPoolDistr ∷ ∀ era. EpochState era → PoolDistr
- newEpochStateSpecUTxO ∷ ∀ era. (EraSpecLedger era, HasSpec (InstantStake era), StashedAVVMAddresses era ~ UTxO era) ⇒ PParams era → WitUniv era → Specification (NewEpochState era)
- newEpochStateSpecUnit ∷ ∀ era. (EraSpecLedger era, HasSpec (InstantStake era), StashedAVVMAddresses era ~ ()) ⇒ PParams era → WitUniv era → Specification (NewEpochState era)
Documentation
class (EraSpecTxOut era, EraStake era, HasSpec (GovState era), HasSpec (CertState era), IsNormalType (CertState era), EraCertState era) ⇒ EraSpecLedger era where Source #
The class (EraSpecLedger era) supports Era parametric Specs over types that appear in the Cardano Ledger
It uses methods (see Test.Cardano.Ledger.Constrained.Conway.ParametricSpec)
that navigate the differences in types parameterized by era that are
embeded as type Families in types that appear in the Cardano Ledger Types.
It is these components that change from one Era to another.
and the EraSpecLedger class has methods that asbtract over those changes.
Methods
govStateSpec ∷ PParams era → Specification (GovState era) Source #
newEpochStateSpec ∷ PParams era → WitUniv era → Specification (NewEpochState era) Source #
certStateSpec ∷ WitUniv era → Term ChainAccountState → Term EpochNo → Specification (CertState era) Source #
Instances
domEqualRng ∷ (Ord ptr, Ord cred, HasSpec cred, HasSpec ptr, HasSpec ume, IsNormalType cred, IsNormalType ptr, IsNormalType ume) ⇒ Term (Map ptr cred) → Term (Map cred ume) → Pred Source #
Want (Rng v3) == (Dom v0), except the Rng is List and the Dom is a Set.
canFollow ∷ Term ProtVer → Term ProtVer → Pred Source #
The constraint for ProtVer always relates one ProtVer to another one that can follow it.
goodDrep ∷ ∀ era. WitUniv era → Specification (Map (Credential 'DRepRole) (Set (Credential 'Staking))) Source #
vstateSpec ∷ ∀ era. Era era ⇒ WitUniv era → Term EpochNo → Term (Map (Credential 'DRepRole) (Set (Credential 'Staking))) → Specification (VState era) Source #
BE SURE the parameter
delegated :: Term (Map (Credential 'DRepRole c) (Set (Credential 'Staking c))
has been witnessed with the same WitUniv as the parameter univ, or this will fail
For a standalone test of vstateSpec one may use goodDrep above, and pass
eraUniv as the actual parameter for the formal parameter univ
Note, that in certStateSpec, the call to vstateSpec is passed a witnessed delegated
that comes from the dstateSpec.
getDelegatees ∷ DState era → Map (Credential 'DRepRole) (Set (Credential 'Staking)) Source #
aggregateDRep ∷ Map (Credential 'Staking) DRep → Map (Credential 'DRepRole) (Set (Credential 'Staking)) Source #
Compute the map of DReps, to those that delegate to them, from the delegation map (Map (Credential 'Staking) Drep) which is stored in the DState This ensures that every staking Credential, delegates to exactly one DRep.
dstateSpec ∷ ∀ era. EraSpecLedger era ⇒ WitUniv era → Term ChainAccountState → Term (Map (KeyHash 'StakePool) PoolParams) → Specification (DState era) Source #
pstateSpec ∷ Era era ⇒ WitUniv era → Term EpochNo → Specification (PState era) Source #
shelleyCertStateSpec ∷ ∀ era. EraSpecLedger era ⇒ WitUniv era → Term ChainAccountState → Term EpochNo → Specification (ShelleyCertState era) Source #
The CertState spec Note, that in order to be self consistent, parts of the pState is passed as an argument the spec for DState spec (every stake delegation is to a registered pool) and parts of the DState are passed as an argument to the spec for VState (every voting delegation is to a registered DRep)
conwayCertStateSpec ∷ EraSpecLedger ConwayEra ⇒ WitUniv ConwayEra → Term ChainAccountState → Term EpochNo → Specification (ConwayCertState ConwayEra) Source #
utxoSpecWit ∷ ∀ era. EraSpecTxOut era ⇒ WitUniv era → Term (Map (Credential 'Staking) (KeyHash 'StakePool)) → Specification (UTxO era) Source #
utxoStateSpec ∷ ∀ era. (EraSpecLedger era, HasSpec (InstantStake era)) ⇒ PParams era → WitUniv era → Term (CertState era) → Specification (UTxOState era) Source #
getDelegs ∷ ∀ era. EraCertState era ⇒ CertState era → Map (Credential 'Staking) (KeyHash 'StakePool) Source #
shelleyGovStateSpec ∷ ∀ era. EraSpecLedger era ⇒ PParams era → Specification (ShelleyGovState era) Source #
conwayGovStateSpec ∷ EraSpecLedger ConwayEra ⇒ PParams ConwayEra → GovEnv ConwayEra → Specification (ConwayGovState ConwayEra) Source #
ledgerStateSpec ∷ ∀ era. (EraSpecLedger era, HasSpec (InstantStake era)) ⇒ PParams era → WitUniv era → Term ChainAccountState → Term EpochNo → Specification (LedgerState era) Source #
getMarkSnapShot ∷ ∀ era. (EraCertState era, EraStake era) ⇒ LedgerState era → SnapShot Source #
The Mark SnapShot (at the epochboundary) is a pure function of the LedgerState
epochStateSpec ∷ ∀ era. (EraSpecLedger era, HasSpec (InstantStake era)) ⇒ PParams era → WitUniv era → Term EpochNo → Specification (EpochState era) Source #
getPoolDistr ∷ ∀ era. EpochState era → PoolDistr Source #
newEpochStateSpecUTxO ∷ ∀ era. (EraSpecLedger era, HasSpec (InstantStake era), StashedAVVMAddresses era ~ UTxO era) ⇒ PParams era → WitUniv era → Specification (NewEpochState era) Source #
Used for Eras where StashedAVVMAddresses era ~ UTxO era (Shelley)
The newEpochStateSpec method (of (EraSpecLedger) class) in the Shelley instance
newEpochStateSpecUnit ∷ ∀ era. (EraSpecLedger era, HasSpec (InstantStake era), StashedAVVMAddresses era ~ ()) ⇒ PParams era → WitUniv era → Specification (NewEpochState era) Source #
Used for Eras where StashedAVVMAddresses era ~ () (Allegra,Mary,Alonzo,Babbage,Conway)
The newEpochStateSpec method (of (EraSpecLedger era) class) in the instances for (Allegra,Mary,Alonzo,Babbage,Conway)