| 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, Era era, HasSpec fn (GovState era)) ⇒ EraSpecLedger era fn where
- govStateSpec ∷ PParams era → Specification fn (GovState era)
- newEpochStateSpec ∷ PParams era → WitUniv era → Specification fn (NewEpochState era)
- testGovEnv ∷ PParams ConwayEra → GovEnv ConwayEra
- 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)
- goodDrep ∷ ∀ era. WitUniv era → Specification ConwayFn (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
- vstateSpec ∷ ∀ fn era. (IsConwayUniv fn, Era era) ⇒ WitUniv era → Term fn EpochNo → Term fn (Map (Credential 'DRepRole) (Set (Credential 'Staking))) → Specification fn (VState era)
- getDelegatees ∷ DState era → Map (Credential 'DRepRole) (Set (Credential 'Staking))
- aggregateDRep ∷ Map (Credential 'Staking) DRep → Map (Credential 'DRepRole) (Set (Credential 'Staking))
- dstateSpec ∷ ∀ era fn. EraSpecLedger era fn ⇒ WitUniv era → Term fn AccountState → Term fn (Map (KeyHash 'StakePool) PoolParams) → Specification fn (DState era)
- epochNoSpec ∷ IsConwayUniv fn ⇒ Specification fn EpochNo
- pstateSpec ∷ (IsConwayUniv fn, Era era) ⇒ WitUniv era → Term fn EpochNo → Specification fn (PState era)
- accountStateSpec ∷ IsConwayUniv fn ⇒ Specification fn AccountState
- certStateSpec ∷ ∀ era fn. EraSpecLedger era fn ⇒ WitUniv era → Term fn AccountState → Term fn EpochNo → Specification fn (CertState era)
- utxoSpecWit ∷ ∀ era fn. EraSpecTxOut era fn ⇒ WitUniv era → Term fn (Map (Credential 'Staking) (KeyHash 'StakePool)) → Specification fn (UTxO era)
- utxoStateSpec ∷ ∀ era fn. EraSpecLedger era fn ⇒ PParams era → WitUniv era → Term fn (CertState era) → Specification fn (UTxOState era)
- getDelegs ∷ ∀ era. CertState era → Map (Credential 'Staking) (KeyHash 'StakePool)
- shelleyGovStateSpec ∷ ∀ era fn. EraSpecLedger era fn ⇒ PParams era → Specification fn (ShelleyGovState era)
- govEnvSpec ∷ IsConwayUniv fn ⇒ PParams ConwayEra → Specification fn (GovEnv ConwayEra)
- conwayGovStateSpec ∷ ∀ fn. EraSpecLedger ConwayEra fn ⇒ PParams ConwayEra → GovEnv ConwayEra → Specification fn (ConwayGovState ConwayEra)
- ledgerStateSpec ∷ ∀ era fn. EraSpecLedger era fn ⇒ PParams era → WitUniv era → Term fn AccountState → Term fn EpochNo → Specification fn (LedgerState era)
- snapShotSpec ∷ IsConwayUniv fn ⇒ Specification fn SnapShot
- snapShotsSpec ∷ IsConwayUniv fn ⇒ Term fn SnapShot → Specification fn SnapShots
- getMarkSnapShot ∷ ∀ era. LedgerState era → SnapShot
- epochStateSpec ∷ ∀ era fn. EraSpecLedger era fn ⇒ PParams era → WitUniv era → Term fn EpochNo → Specification fn (EpochState era)
- getPoolDistr ∷ ∀ era. EpochState era → PoolDistr
- newEpochStateSpecUTxO ∷ ∀ era fn. (EraSpecLedger era fn, StashedAVVMAddresses era ~ UTxO era) ⇒ PParams era → WitUniv era → Specification fn (NewEpochState era)
- newEpochStateSpecUnit ∷ ∀ era fn. (EraSpecLedger era fn, StashedAVVMAddresses era ~ ()) ⇒ PParams era → WitUniv era → Specification fn (NewEpochState era)
Documentation
class (EraSpecTxOut era fn, Era era, 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 → WitUniv 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.
goodDrep ∷ ∀ era. WitUniv era → Specification ConwayFn (Map (Credential 'DRepRole) (Set (Credential 'Staking))) Source #
vstateSpec ∷ ∀ fn era. (IsConwayUniv fn, Era era) ⇒ WitUniv era → Term fn EpochNo → Term fn (Map (Credential 'DRepRole) (Set (Credential 'Staking))) → Specification fn (VState era) Source #
BE SURE the parameter
delegated :: Term fn (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 fn. EraSpecLedger era fn ⇒ WitUniv era → Term fn AccountState → Term fn (Map (KeyHash 'StakePool) PoolParams) → Specification fn (DState era) Source #
epochNoSpec ∷ IsConwayUniv fn ⇒ Specification fn EpochNo Source #
pstateSpec ∷ (IsConwayUniv fn, Era era) ⇒ WitUniv era → Term fn EpochNo → Specification fn (PState era) Source #
accountStateSpec ∷ IsConwayUniv fn ⇒ Specification fn AccountState Source #
certStateSpec ∷ ∀ era fn. EraSpecLedger era fn ⇒ WitUniv 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)
utxoSpecWit ∷ ∀ era fn. EraSpecTxOut era fn ⇒ WitUniv era → Term fn (Map (Credential 'Staking) (KeyHash 'StakePool)) → Specification fn (UTxO era) Source #
utxoStateSpec ∷ ∀ era fn. EraSpecLedger era fn ⇒ PParams era → WitUniv era → Term fn (CertState era) → Specification fn (UTxOState era) Source #
shelleyGovStateSpec ∷ ∀ era fn. EraSpecLedger era fn ⇒ PParams era → Specification fn (ShelleyGovState era) Source #
govEnvSpec ∷ IsConwayUniv fn ⇒ PParams ConwayEra → Specification fn (GovEnv ConwayEra) Source #
conwayGovStateSpec ∷ ∀ fn. EraSpecLedger ConwayEra fn ⇒ PParams ConwayEra → GovEnv ConwayEra → Specification fn (ConwayGovState ConwayEra) Source #
ledgerStateSpec ∷ ∀ era fn. EraSpecLedger era fn ⇒ PParams era → WitUniv era → Term fn AccountState → Term fn EpochNo → Specification fn (LedgerState era) Source #
snapShotSpec ∷ IsConwayUniv fn ⇒ Specification fn SnapShot Source #
snapShotsSpec ∷ IsConwayUniv fn ⇒ Term fn SnapShot → Specification fn SnapShots Source #
getMarkSnapShot ∷ ∀ era. LedgerState era → SnapShot Source #
The Mark SnapShot (at the epochboundary) is a pure function of the LedgerState
epochStateSpec ∷ ∀ era fn. EraSpecLedger era fn ⇒ PParams era → WitUniv era → Term fn EpochNo → Specification fn (EpochState era) Source #
getPoolDistr ∷ ∀ era. EpochState era → PoolDistr Source #
newEpochStateSpecUTxO ∷ ∀ era fn. (EraSpecLedger era fn, StashedAVVMAddresses era ~ UTxO era) ⇒ PParams era → WitUniv 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 → WitUniv 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)