cardano-ledger-test-9.9.9.9: Testing harness, tests and benchmarks for Shelley style cardano ledgers
Safe HaskellSafe-Inferred
LanguageHaskell2010

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

Documentation

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.

delegatesToMap (Credential 'DRepRole) (Set (Credential 'Staking)) → Set (Credential 'DRepRole) Source #

Compute the set of DRep Credentials that some (Credential 'Staking) delegates to

delegatorsMap (Credential 'DRepRole) (Set (Credential 'Staking)) → Set (Credential 'Staking) Source #

Compute the set of (Credential 'Staking) that delegate their vote to some DRep

dRepsOfMap (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)

credToDRepCredential 'DRepRoleDRep Source #

Turn a DRep Credential into a DRep

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.

canFollowTerm ProtVerTerm ProtVerPred Source #

The constraint for ProtVer always relates one ProtVer to another one that can follow it.

vStateSpec ∷ ∀ era. Era era ⇒ WitUniv era → Term EpochNoMap (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.

conwayAccountMapSpec ∷ ∀ era. Era era ⇒ WitUniv era → Map (Credential 'DRepRole) (Set (Credential 'Staking)) → Term (Map (KeyHash 'StakePool) PoolParams) → Map RewardAccount CoinSpecification (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

pStateSpecEra era ⇒ WitUniv era → Term EpochNoSpecification (PState era) Source #

utxoStateSpec ∷ ∀ era. (HasSpec (InstantStake era), era ~ ConwayEra) ⇒ PParams era → WitUniv era → Term (CertState era) → Specification (UTxOState 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 → CertContextTerm EpochNoSpecification (EpochState era) Source #

newEpochStateSpec ∷ ∀ era. (HasSpec (InstantStake era), era ~ ConwayEra) ⇒ PParams era → WitUniv era → CertContextSpecification (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)