| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base
Contents
Synopsis
- data ConwayCertExecContext era = ConwayCertExecContext {
- ccecWithdrawals ∷ !(Map RewardAccount Coin)
- ccecVotes ∷ !(VotingProcedures era)
- ccecDelegatees ∷ !(Map (Credential 'DRepRole) (Set (Credential 'Staking)))
- conwayCertExecContextSpec ∷ ∀ era. Era era ⇒ WitUniv era → Integer → Specification (ConwayCertExecContext era)
- data ConwayRatifyExecContext era = ConwayRatifyExecContext {
- crecTreasury ∷ Coin
- crecGovActionMap ∷ [GovActionState era]
- nameEpoch ∷ EpochNo → String
- nameEnact ∷ EnactSignal era → String
- nameGovAction ∷ GovAction era → String
- crecTreasuryL ∷ Lens' (ConwayRatifyExecContext era) Coin
- crecGovActionMapL ∷ Lens' (ConwayRatifyExecContext era) [GovActionState era]
- enactStateSpec ∷ ConwayEnactExecContext ConwayEra → ConwayExecEnactEnv ConwayEra → Specification (EnactState ConwayEra)
- externalFunctions ∷ ExternalFunctions
- whoDelegatesSpec ∷ Era era ⇒ WitUniv era → Specification (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
Documentation
data ConwayCertExecContext era Source #
Constructors
| ConwayCertExecContext | The VState and the DState (which contains the AccountState) are subtly related. VState {vsDReps :: !(Map (Credential DRepRole) DRepState) ..} ConwayAccounts :: {caStates :: Map(Credential Staking) (ConwayAccountState era)} we maintain this subtle relationship by storing the ccecDelagatees field in this context. See Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs(whoDelegatesSpec) and its uses in that module. whoDelegatesSpec :: WitUniv era -> Specification (Map (Credential 'DRepRole) (Set (Credential 'Staking))) |
Fields
| |
Instances
conwayCertExecContextSpec ∷ ∀ era. Era era ⇒ WitUniv era → Integer → Specification (ConwayCertExecContext era) Source #
A Specification version of genCertContext
Makes sure all the subtle invariants of `type WhoDelegates` are met.
data ConwayRatifyExecContext era Source #
Constructors
| ConwayRatifyExecContext | |
Fields
| |
Instances
nameEnact ∷ EnactSignal era → String Source #
nameGovAction ∷ GovAction era → String Source #
crecTreasuryL ∷ Lens' (ConwayRatifyExecContext era) Coin Source #
crecGovActionMapL ∷ Lens' (ConwayRatifyExecContext era) [GovActionState era] Source #
enactStateSpec ∷ ConwayEnactExecContext ConwayEra → ConwayExecEnactEnv ConwayEra → Specification (EnactState ConwayEra) Source #
whoDelegatesSpec ∷ 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.