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
- type WhoDelegates = Map (Credential 'DRepRole) (Set (Credential 'Staking))
- whoDelegatesSpec ∷ ∀ era. Era era ⇒ WitUniv era → Specification (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
- wdrlSpec ∷ Era era ⇒ Map (Credential 'DRepRole) (Set (Credential 'Staking)) → WitUniv era → Specification (Map RewardAccount Coin)
- delegatesTo ∷ Map (Credential 'DRepRole) (Set (Credential 'Staking)) → Set (Credential 'DRepRole)
- delegators ∷ Map (Credential 'DRepRole) (Set (Credential 'Staking)) → Set (Credential 'Staking)
- dRepsOf ∷ Map (Credential 'DRepRole) (Set (Credential 'Staking)) → Set DRep
- credToDRep ∷ Credential 'DRepRole → DRep
- toDelta ∷ Coin → DeltaCoin
- type CertContext = (Map (Credential 'DRepRole) (Set (Credential 'Staking)), Map RewardAccount Coin)
- genCertContext ∷ ∀ era. Era era ⇒ WitUniv era → Gen CertContext
- testGovEnv ∷ PParams ConwayEra → GovEnv ConwayEra
- govEnvSpec ∷ PParams ConwayEra → Specification (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)
- epochNoSpec ∷ Specification EpochNo
- accountStateSpec ∷ Specification ChainAccountState
- goodDrep ∷ ∀ era. Era era ⇒ WitUniv era → Specification (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
- vStateSpec ∷ ∀ era. Era era ⇒ WitUniv era → Term EpochNo → Map (Credential 'DRepRole) (Set (Credential 'Staking)) → Specification (VState era)
- conwayDStateSpec ∷ ∀ era. era ~ ConwayEra ⇒ WitUniv era → (Map (Credential 'DRepRole) (Set (Credential 'Staking)), Map RewardAccount Coin) → Term (Map (KeyHash 'StakePool) PoolParams) → Specification (DState era)
- conwayAccountMapSpec ∷ ∀ era. Era era ⇒ WitUniv era → Map (Credential 'DRepRole) (Set (Credential 'Staking)) → Term (Map (KeyHash 'StakePool) PoolParams) → Map RewardAccount Coin → Specification (Map (Credential 'Staking) (ConwayAccountState era))
- pStateSpec ∷ Era era ⇒ WitUniv era → Term EpochNo → Specification (PState era)
- conwayCertStateSpec ∷ WitUniv ConwayEra → (Map (Credential 'DRepRole) (Set (Credential 'Staking)), Map RewardAccount Coin) → Term EpochNo → Specification (ConwayCertState ConwayEra)
- utxoSpecWit ∷ ∀ era. EraSpecTxOut era ⇒ WitUniv era → Term (Map (Credential 'Staking) (KeyHash 'StakePool)) → Specification (UTxO era)
- utxoStateSpec ∷ ∀ era. (HasSpec (InstantStake era), era ~ ConwayEra) ⇒ PParams era → WitUniv era → Term (CertState era) → Specification (UTxOState era)
- getDelegs ∷ ∀ era. EraCertState era ⇒ CertState era → Map (Credential 'Staking) (KeyHash 'StakePool)
- conwayGovStateSpec ∷ PParams ConwayEra → GovEnv ConwayEra → Specification (ConwayGovState ConwayEra)
- ledgerStateSpec ∷ ∀ era. (HasSpec (InstantStake era), era ~ ConwayEra) ⇒ PParams era → WitUniv era → CertContext → Term EpochNo → Specification (LedgerState era)
- snapShotSpec ∷ Specification SnapShot
- snapShotsSpec ∷ Term SnapShot → Specification SnapShots
- getMarkSnapShot ∷ ∀ era. (EraCertState era, EraStake era) ⇒ LedgerState era → SnapShot
- epochStateSpec ∷ ∀ era. (HasSpec (InstantStake era), era ~ ConwayEra) ⇒ PParams era → WitUniv era → CertContext → Term EpochNo → Specification (EpochState era)
- getPoolDistr ∷ ∀ era. EpochState era → PoolDistr
- newEpochStateSpec ∷ ∀ era. (HasSpec (InstantStake era), era ~ ConwayEra) ⇒ PParams era → WitUniv era → CertContext → Specification (NewEpochState era)
Documentation
type WhoDelegates = Map (Credential 'DRepRole) (Set (Credential 'Staking)) Source #
whoDelegatesSpec ∷ ∀ era. Era era ⇒ WitUniv era → Specification (Map (Credential 'DRepRole) (Set (Credential 'Staking))) Source #
In the Coway Era, the relationship between the Stake delegation and DRep delegation is
quite subtle. The best way to get this right during constrained generation, is to generate
one piece, we call WhoDelegates
and compute the other pieces from that.
type WhoDelegates = Map (Credential 'DRepRole) (Set (Credential 'Staking)
The functions delegatesTo
, dRepsOf
, credToDRep
, delegators
, help compute the other pieces.
One can observe that the VState and ConwayAccounts, both have Maps whose domain come from the
domain of WhoDelegates and these maps have strong invariants with each other.
We choose the type WhoDelegates because two key components of VState and ConwayAccounts have
related fields that must agree in many subtle ways. The most important way in that the the
domain of both the maps can be computed from WhoDelegates.
VState {vsDReps :: !(Map (Credential DRepRole) DRepState) ..}
ConwayAccounts :: {caStates :: Map(Credential Staking) (ConwayAccountState era)}
Map.keysSet vsDReps == delegatesTo onepiece
Map.keysSet caStates == delegators onepiece
Other more subtle agreement come from fields inside DRepState and ConwayAccountState
All of these are captured in the Specification for VState and DState (which contains the Account map)
One other thing we need to consider is: newtype Withdrawals = Withdrawals {unWithdrawals :: Map RewardAccount Coin}
WithDrawals come from Transactions, but they have subtle interactions with rewards map and the Drep delegation map
So we give special Specifcations that will generate both in ways that maintain the important relationships.
wdrlSpec ∷ Era era ⇒ Map (Credential 'DRepRole) (Set (Credential 'Staking)) → WitUniv era → Specification (Map RewardAccount Coin) Source #
delegatesTo ∷ Map (Credential 'DRepRole) (Set (Credential 'Staking)) → Set (Credential 'DRepRole) Source #
Compute the set of DRep Credentials that some (Credential 'Staking) delegates to
delegators ∷ Map (Credential 'DRepRole) (Set (Credential 'Staking)) → Set (Credential 'Staking) Source #
Compute the set of (Credential 'Staking) that delegate their vote to some DRep
dRepsOf ∷ Map (Credential 'DRepRole) (Set (Credential 'Staking)) → Set DRep Source #
Compute the set of DReps that some (Credential 'Staking) delegates to
Like delegatesTo
but returns the DRep rather than the (Credential 'DRepRole)
credToDRep ∷ Credential 'DRepRole → DRep Source #
Turn a DRep Credential into a DRep
type CertContext = (Map (Credential 'DRepRole) (Set (Credential 'Staking)), Map RewardAccount Coin) Source #
genCertContext ∷ ∀ era. Era era ⇒ WitUniv era → Gen CertContext Source #
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. Era era ⇒ WitUniv era → Specification (Map (Credential 'DRepRole) (Set (Credential 'Staking))) Source #
vStateSpec ∷ ∀ era. Era era ⇒ WitUniv era → Term EpochNo → Map (Credential 'DRepRole) (Set (Credential 'Staking)) → Specification (VState era) Source #
BE SURE the parameter whoDelegated has been witnessed with the same WitUniv as the parameter univ
.
conwayDStateSpec ∷ ∀ era. era ~ ConwayEra ⇒ WitUniv era → (Map (Credential 'DRepRole) (Set (Credential 'Staking)), Map RewardAccount Coin) → Term (Map (KeyHash 'StakePool) PoolParams) → Specification (DState era) Source #
conwayAccountMapSpec ∷ ∀ era. Era era ⇒ WitUniv era → Map (Credential 'DRepRole) (Set (Credential 'Staking)) → Term (Map (KeyHash 'StakePool) PoolParams) → Map RewardAccount Coin → Specification (Map (Credential 'Staking) (ConwayAccountState era)) Source #
Specify the internal Map of ConwayAccounts :: Map (Credential Staking) (ConwayAccountState era) Ensure that the Staking Credential is both staked to some Pool, and Delegated to some DRep | Given a set of Withdrawals:: newtype Withdrawals = Withdrawals {unWithdrawals :: Map RewardAccount Coin} where:: data RewardAccount = RewardAccount {raNetwork :: !Network, raCredential :: !(Credential Staking)} That ensures every AccountState has the propeties listed to the left data ConwayAccountState era = ConwayAccountState {casBalance :: (CompactForm Coin) -- Sometimes 0, Matches the withdrawl amount if part of a Withdrawal ,casDeposit :: (CompactFormCoin) -- witnessed ,casStakePoolDelegation :: (StrictMaybe (KeyHash StakePool)) -- The Pool Staked to exists ,casDRepDelegation :: (StrictMaybe DRep)} -- The DRep delegated to exists
pStateSpec ∷ Era era ⇒ WitUniv era → Term EpochNo → Specification (PState era) Source #
conwayCertStateSpec ∷ WitUniv ConwayEra → (Map (Credential 'DRepRole) (Set (Credential 'Staking)), Map RewardAccount Coin) → Term EpochNo → Specification (ConwayCertState ConwayEra) Source #
utxoSpecWit ∷ ∀ era. EraSpecTxOut era ⇒ WitUniv era → Term (Map (Credential 'Staking) (KeyHash 'StakePool)) → Specification (UTxO era) Source #
utxoStateSpec ∷ ∀ era. (HasSpec (InstantStake era), era ~ ConwayEra) ⇒ PParams era → WitUniv era → Term (CertState era) → Specification (UTxOState era) Source #
getDelegs ∷ ∀ era. EraCertState era ⇒ CertState era → Map (Credential 'Staking) (KeyHash 'StakePool) Source #
conwayGovStateSpec ∷ PParams ConwayEra → GovEnv ConwayEra → Specification (ConwayGovState ConwayEra) Source #
ledgerStateSpec ∷ ∀ era. (HasSpec (InstantStake era), era ~ ConwayEra) ⇒ PParams era → WitUniv era → CertContext → 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. (HasSpec (InstantStake era), era ~ ConwayEra) ⇒ PParams era → WitUniv era → CertContext → Term EpochNo → Specification (EpochState era) Source #
getPoolDistr ∷ ∀ era. EpochState era → PoolDistr Source #
newEpochStateSpec ∷ ∀ era. (HasSpec (InstantStake era), era ~ ConwayEra) ⇒ PParams era → WitUniv era → CertContext → 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)