| 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 fn, HasSpec fn (GovState era)) ⇒ EraSpecLedger era fn where
- govStateSpec ∷ PParams era → Specification fn (GovState era)
- newEpochStateSpec ∷ PParams era → Specification fn (NewEpochState era)
- testGovEnv ∷ PParams Conway → GovEnv Conway
- domEqualRng ∷ (IsConwayUniv fn, Ord ptr, Ord cred, HasSpec fn cred, HasSpec fn ptr, HasSpec fn ume) ⇒ Term fn (Map ptr cred) → Term fn (Map cred ume) → Pred fn
- canFollow ∷ IsConwayUniv fn ⇒ Term fn ProtVer → Term fn ProtVer → Pred fn
- protVersCanfollow ∷ Specification ConwayFn (ProtVer, ProtVer)
- vstateSpec ∷ ∀ fn era. (IsConwayUniv fn, Era era) ⇒ Term fn EpochNo → Term fn (Map (Credential 'DRepRole (EraCrypto era)) (Set (Credential 'Staking (EraCrypto era)))) → Specification fn (VState era)
- getDelegatees ∷ DState era → Map (Credential 'DRepRole (EraCrypto era)) (Set (Credential 'Staking (EraCrypto era)))
- aggregateDRep ∷ Map (Credential 'Staking c) (DRep c) → Map (Credential 'DRepRole c) (Set (Credential 'Staking c))
- dstateSpec ∷ ∀ era fn. EraSpecLedger era fn ⇒ Term fn AccountState → Term fn (Map (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))) → Specification fn (DState era)
- epochNoSpec ∷ IsConwayUniv fn ⇒ Specification fn EpochNo
- pstateSpec ∷ (IsConwayUniv fn, Era era) ⇒ Term fn EpochNo → Specification fn (PState era)
- accountStateSpec ∷ IsConwayUniv fn ⇒ Specification fn AccountState
- certStateSpec ∷ ∀ era fn. EraSpecLedger era fn ⇒ Term fn (Set (Credential 'DRepRole (EraCrypto era))) → Term fn AccountState → Term fn EpochNo → Specification fn (CertState era)
- utxoSpec ∷ ∀ era fn. EraSpecLedger era fn ⇒ Term fn (Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))) → Specification fn (UTxO era)
- utxoStateSpec ∷ ∀ era fn. EraSpecLedger era fn ⇒ PParams era → Term fn (CertState era) → Specification fn (UTxOState era)
- getDelegs ∷ ∀ era. CertState era → Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))
- shelleyGovStateSpec ∷ ∀ era fn. EraSpecLedger era fn ⇒ PParams era → Specification fn (ShelleyGovState era)
- govEnvSpec ∷ IsConwayUniv fn ⇒ PParams Conway → Specification fn (GovEnv Conway)
- conwayGovStateSpec ∷ ∀ fn. EraSpecLedger Conway fn ⇒ PParams Conway → GovEnv Conway → Specification fn (ConwayGovState Conway)
- ledgerStateSpec ∷ ∀ era fn. EraSpecLedger era fn ⇒ PParams era → Term fn AccountState → Term fn EpochNo → Specification fn (LedgerState era)
- snapShotSpec ∷ (Crypto c, IsConwayUniv fn) ⇒ Specification fn (SnapShot c)
- snapShotsSpec ∷ (Crypto c, IsConwayUniv fn) ⇒ Term fn (SnapShot c) → Specification fn (SnapShots c)
- getMarkSnapShot ∷ ∀ era. LedgerState era → SnapShot (EraCrypto era)
- epochStateSpec ∷ ∀ era fn. EraSpecLedger era fn ⇒ PParams era → Term fn EpochNo → Specification fn (EpochState era)
- getPoolDistr ∷ ∀ era. EpochState era → PoolDistr (EraCrypto era)
- newEpochStateSpecUTxO ∷ ∀ era fn. (EraSpecLedger era fn, StashedAVVMAddresses era ~ UTxO era) ⇒ PParams era → Specification fn (NewEpochState era)
- newEpochStateSpecUnit ∷ ∀ era fn. (EraSpecLedger era fn, StashedAVVMAddresses era ~ ()) ⇒ PParams era → Specification fn (NewEpochState era)
- dRepToCred ∷ DRep c → Maybe (Credential 'DRepRole c)
- try10 ∷ IO ()
Documentation
class (EraSpecTxOut era fn, HasSpec fn (GovState era)) ⇒ EraSpecLedger era fn where Source #
The class (EraSpecLedger era) supports Era parametric Specs over types that appear in the Cardano Ledger.223
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 fn (GovState era) Source #
newEpochStateSpec ∷ PParams era → Specification fn (NewEpochState era) Source #
Instances
domEqualRng ∷ (IsConwayUniv fn, Ord ptr, Ord cred, HasSpec fn cred, HasSpec fn ptr, HasSpec fn ume) ⇒ Term fn (Map ptr cred) → Term fn (Map cred ume) → Pred fn Source #
Want (Rng v3) == (Dom v0), except the Rng is List and the Dom is a Set.
canFollow ∷ IsConwayUniv fn ⇒ Term fn ProtVer → Term fn ProtVer → Pred fn Source #
The constraint for ProtVer always relates one ProtVer to another one that can follow it.
vstateSpec ∷ ∀ fn era. (IsConwayUniv fn, Era era) ⇒ Term fn EpochNo → Term fn (Map (Credential 'DRepRole (EraCrypto era)) (Set (Credential 'Staking (EraCrypto era)))) → Specification fn (VState era) Source #
getDelegatees ∷ DState era → Map (Credential 'DRepRole (EraCrypto era)) (Set (Credential 'Staking (EraCrypto era))) Source #
aggregateDRep ∷ Map (Credential 'Staking c) (DRep c) → Map (Credential 'DRepRole c) (Set (Credential 'Staking c)) 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 fn. EraSpecLedger era fn ⇒ Term fn AccountState → Term fn (Map (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))) → Specification fn (DState era) Source #
epochNoSpec ∷ IsConwayUniv fn ⇒ Specification fn EpochNo Source #
pstateSpec ∷ (IsConwayUniv fn, Era era) ⇒ Term fn EpochNo → Specification fn (PState era) Source #
accountStateSpec ∷ IsConwayUniv fn ⇒ Specification fn AccountState Source #
certStateSpec ∷ ∀ era fn. EraSpecLedger era fn ⇒ Term fn (Set (Credential 'DRepRole (EraCrypto era))) → Term fn AccountState → Term fn EpochNo → Specification fn (CertState 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)
utxoSpec ∷ ∀ era fn. EraSpecLedger era fn ⇒ Term fn (Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))) → Specification fn (UTxO era) Source #
utxoStateSpec ∷ ∀ era fn. EraSpecLedger era fn ⇒ PParams era → Term fn (CertState era) → Specification fn (UTxOState era) Source #
getDelegs ∷ ∀ era. CertState era → Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era)) Source #
shelleyGovStateSpec ∷ ∀ era fn. EraSpecLedger era fn ⇒ PParams era → Specification fn (ShelleyGovState era) Source #
govEnvSpec ∷ IsConwayUniv fn ⇒ PParams Conway → Specification fn (GovEnv Conway) Source #
conwayGovStateSpec ∷ ∀ fn. EraSpecLedger Conway fn ⇒ PParams Conway → GovEnv Conway → Specification fn (ConwayGovState Conway) Source #
ledgerStateSpec ∷ ∀ era fn. EraSpecLedger era fn ⇒ PParams era → Term fn AccountState → Term fn EpochNo → Specification fn (LedgerState era) Source #
snapShotSpec ∷ (Crypto c, IsConwayUniv fn) ⇒ Specification fn (SnapShot c) Source #
snapShotsSpec ∷ (Crypto c, IsConwayUniv fn) ⇒ Term fn (SnapShot c) → Specification fn (SnapShots c) Source #
getMarkSnapShot ∷ ∀ era. LedgerState era → SnapShot (EraCrypto era) Source #
The Mark SnapShot (at the epochboundary) is a pure function of the LedgerState
epochStateSpec ∷ ∀ era fn. EraSpecLedger era fn ⇒ PParams era → Term fn EpochNo → Specification fn (EpochState era) Source #
getPoolDistr ∷ ∀ era. EpochState era → PoolDistr (EraCrypto era) Source #
newEpochStateSpecUTxO ∷ ∀ era fn. (EraSpecLedger era fn, StashedAVVMAddresses era ~ UTxO era) ⇒ PParams era → Specification fn (NewEpochState era) Source #
Used for Eras where StashedAVVMAddresses era ~ UTxO era (Shelley)
The newEpochStateSpec method (of (EraSpecLedger era fn) class) in the Shelley instance
newEpochStateSpecUnit ∷ ∀ era fn. (EraSpecLedger era fn, StashedAVVMAddresses era ~ ()) ⇒ PParams era → Specification fn (NewEpochState era) Source #
Used for Eras where StashedAVVMAddresses era ~ () (Allegra,Mary,Alonzo,Babbage,Conway)
The newEpochStateSpec method (of (EraSpecLedger era fn) class) in the instances for (Allegra,Mary,Alonzo,Babbage,Conway)
dRepToCred ∷ DRep c → Maybe (Credential 'DRepRole c) Source #