cardano-ledger-conformance-9.9.9.9: Testing utilities for conformance testing
Safe HaskellSafe-Inferred
LanguageHaskell2010

Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

Synopsis

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

Instances

Instances details
Era era ⇒ Arbitrary (ConwayCertExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

Generic (ConwayCertExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

Associated Types

type Rep (ConwayCertExecContext era) ∷ TypeType #

Show (ConwayCertExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

Reflect era ⇒ DecCBOR (ConwayCertExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

Era era ⇒ EncCBOR (ConwayCertExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

Era era ⇒ HasSpec (ConwayCertExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

Typeable era ⇒ HasSimpleRep (ConwayCertExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

Associated Types

type SimpleRep (ConwayCertExecContext era) Source #

type TheSop (ConwayCertExecContext era) ∷ [Type] Source #

Era era ⇒ NFData (ConwayCertExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

Methods

rnfConwayCertExecContext era → () #

Eq (ConwayCertExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

Era era ⇒ ToExpr (ConwayCertExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

Inject (ConwayCertExecContext era) (VotingProcedures era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

Inject (ConwayCertExecContext era) (Map RewardAccount Coin) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

Inject (WitUniv ConwayEra, ConwayCertExecContext ConwayEra) (VotingProcedures ConwayEra) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.GovCert

Inject (WitUniv ConwayEra, ConwayCertExecContext ConwayEra) (Set (Credential 'DRepRole)) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Deleg

Inject (WitUniv ConwayEra, ConwayCertExecContext ConwayEra) (Map RewardAccount Coin) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.GovCert

type Rep (ConwayCertExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

type Rep (ConwayCertExecContext era) = D1 ('MetaData "ConwayCertExecContext" "Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base" "cardano-ledger-conformance-9.9.9.9-inplace" 'False) (C1 ('MetaCons "ConwayCertExecContext" 'PrefixI 'True) (S1 ('MetaSel ('Just "ccecWithdrawals") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Map RewardAccount Coin)) :*: (S1 ('MetaSel ('Just "ccecVotes") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (VotingProcedures era)) :*: S1 ('MetaSel ('Just "ccecDelegatees") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Map (Credential 'DRepRole) (Set (Credential 'Staking)))))))
type Prerequisites (ConwayCertExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

type TypeSpec (ConwayCertExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

type SimpleRep (ConwayCertExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

type TheSop (ConwayCertExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

conwayCertExecContextSpec ∷ ∀ era. Era era ⇒ WitUniv era → IntegerSpecification (ConwayCertExecContext era) Source #

A Specification version of genCertContext Makes sure all the subtle invariants of `type WhoDelegates` are met.

data ConwayRatifyExecContext era Source #

Instances

Instances details
(Era era, Arbitrary (PParamsHKD StrictMaybe era)) ⇒ Arbitrary (ConwayRatifyExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

Generic (ConwayRatifyExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

Associated Types

type Rep (ConwayRatifyExecContext era) ∷ TypeType #

EraPParams era ⇒ Show (ConwayRatifyExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

EraPParams era ⇒ DecCBOR (ConwayRatifyExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

EraPParams era ⇒ EncCBOR (ConwayRatifyExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

(EraPParams era, HasSpec (GovActionState era)) ⇒ HasSpec (ConwayRatifyExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

Methods

emptySpecTypeSpec (ConwayRatifyExecContext era) Source #

combineSpecTypeSpec (ConwayRatifyExecContext era) → TypeSpec (ConwayRatifyExecContext era) → Specification (ConwayRatifyExecContext era) Source #

genFromTypeSpec ∷ ∀ (m ∷ TypeType). (HasCallStack, MonadGenError m) ⇒ TypeSpec (ConwayRatifyExecContext era) → GenT m (ConwayRatifyExecContext era) Source #

conformsToConwayRatifyExecContext era → TypeSpec (ConwayRatifyExecContext era) → Bool Source #

shrinkWithTypeSpecTypeSpec (ConwayRatifyExecContext era) → ConwayRatifyExecContext era → [ConwayRatifyExecContext era] Source #

toPredsTerm (ConwayRatifyExecContext era) → TypeSpec (ConwayRatifyExecContext era) → Pred Source #

cardinalTypeSpecTypeSpec (ConwayRatifyExecContext era) → Specification Integer Source #

cardinalTrueSpecSpecification Integer Source #

typeSpecHasErrorTypeSpec (ConwayRatifyExecContext era) → Maybe (NonEmpty String) Source #

alternateShowTypeSpec (ConwayRatifyExecContext era) → BinaryShow Source #

monadConformsToConwayRatifyExecContext era → TypeSpec (ConwayRatifyExecContext era) → Writer [String] Bool Source #

typeSpecOptTypeSpec (ConwayRatifyExecContext era) → [ConwayRatifyExecContext era] → Specification (ConwayRatifyExecContext era) Source #

guardTypeSpec ∷ [String] → TypeSpec (ConwayRatifyExecContext era) → Specification (ConwayRatifyExecContext era) Source #

prerequisitesEvidence (Prerequisites (ConwayRatifyExecContext era)) Source #

Typeable era ⇒ HasSimpleRep (ConwayRatifyExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

EraPParams era ⇒ NFData (ConwayRatifyExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

Methods

rnfConwayRatifyExecContext era → () #

EraPParams era ⇒ Eq (ConwayRatifyExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

ToExpr (PParamsHKD StrictMaybe era) ⇒ ToExpr (ConwayRatifyExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

Inject (ConwayRatifyExecContext era) Coin Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

Inject (ConwayRatifyExecContext era) [GovActionState era] Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

type Rep (ConwayRatifyExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

type Rep (ConwayRatifyExecContext era) = D1 ('MetaData "ConwayRatifyExecContext" "Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base" "cardano-ledger-conformance-9.9.9.9-inplace" 'False) (C1 ('MetaCons "ConwayRatifyExecContext" 'PrefixI 'True) (S1 ('MetaSel ('Just "crecTreasury") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Coin) :*: S1 ('MetaSel ('Just "crecGovActionMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [GovActionState era])))
type Prerequisites (ConwayRatifyExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

type TypeSpec (ConwayRatifyExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

type SimpleRep (ConwayRatifyExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

type TheSop (ConwayRatifyExecContext era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base

whoDelegatesSpecEra 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.

Orphan instances

ExecSpecRule "ENACT" ConwayEra Source # 
Instance details

Associated Types

type ExecContext "ENACT" ConwayEra Source #

type ExecEnvironment "ENACT" ConwayEra Source #

type ExecState "ENACT" ConwayEra Source #

type ExecSignal "ENACT" ConwayEra Source #

Methods

environmentSpecExecContext "ENACT" ConwayEraSpecification (ExecEnvironment "ENACT" ConwayEra) Source #

stateSpecExecContext "ENACT" ConwayEraExecEnvironment "ENACT" ConwayEraSpecification (ExecState "ENACT" ConwayEra) Source #

signalSpecExecContext "ENACT" ConwayEraExecEnvironment "ENACT" ConwayEraExecState "ENACT" ConwayEraSpecification (ExecSignal "ENACT" ConwayEra) Source #

classOfExecSignal "ENACT" ConwayEraMaybe String Source #

genExecContextGen (ExecContext "ENACT" ConwayEra) Source #

runAgdaRuleSpecRep (ExecEnvironment "ENACT" ConwayEra) → SpecRep (ExecState "ENACT" ConwayEra) → SpecRep (ExecSignal "ENACT" ConwayEra) → Either OpaqueErrorString (SpecRep (ExecState "ENACT" ConwayEra)) Source #

translateInputsExecEnvironment "ENACT" ConwayEraExecState "ENACT" ConwayEraExecSignal "ENACT" ConwayEraExecContext "ENACT" ConwayEraImpTestM ConwayEra (SpecRep (ExecEnvironment "ENACT" ConwayEra), SpecRep (ExecState "ENACT" ConwayEra), SpecRep (ExecSignal "ENACT" ConwayEra)) Source #

testConformanceExecContext "ENACT" ConwayEraExecEnvironment "ENACT" ConwayEraExecState "ENACT" ConwayEraExecSignal "ENACT" ConwayEraProperty Source #

extraInfoGlobalsExecContext "ENACT" ConwayEraEnvironment (EraRule "ENACT" ConwayEra) → State (EraRule "ENACT" ConwayEra) → Signal (EraRule "ENACT" ConwayEra) → Either OpaqueErrorString (State (EraRule "ENACT" ConwayEra), [Event (EraRule "ENACT" ConwayEra)]) → Doc AnsiStyle Source #

ExecSpecRule "EPOCH" ConwayEra Source # 
Instance details

Associated Types

type ExecContext "EPOCH" ConwayEra Source #

type ExecEnvironment "EPOCH" ConwayEra Source #

type ExecState "EPOCH" ConwayEra Source #

type ExecSignal "EPOCH" ConwayEra Source #

Methods

environmentSpecExecContext "EPOCH" ConwayEraSpecification (ExecEnvironment "EPOCH" ConwayEra) Source #

stateSpecExecContext "EPOCH" ConwayEraExecEnvironment "EPOCH" ConwayEraSpecification (ExecState "EPOCH" ConwayEra) Source #

signalSpecExecContext "EPOCH" ConwayEraExecEnvironment "EPOCH" ConwayEraExecState "EPOCH" ConwayEraSpecification (ExecSignal "EPOCH" ConwayEra) Source #

classOfExecSignal "EPOCH" ConwayEraMaybe String Source #

genExecContextGen (ExecContext "EPOCH" ConwayEra) Source #

runAgdaRuleSpecRep (ExecEnvironment "EPOCH" ConwayEra) → SpecRep (ExecState "EPOCH" ConwayEra) → SpecRep (ExecSignal "EPOCH" ConwayEra) → Either OpaqueErrorString (SpecRep (ExecState "EPOCH" ConwayEra)) Source #

translateInputsExecEnvironment "EPOCH" ConwayEraExecState "EPOCH" ConwayEraExecSignal "EPOCH" ConwayEraExecContext "EPOCH" ConwayEraImpTestM ConwayEra (SpecRep (ExecEnvironment "EPOCH" ConwayEra), SpecRep (ExecState "EPOCH" ConwayEra), SpecRep (ExecSignal "EPOCH" ConwayEra)) Source #

testConformanceExecContext "EPOCH" ConwayEraExecEnvironment "EPOCH" ConwayEraExecState "EPOCH" ConwayEraExecSignal "EPOCH" ConwayEraProperty Source #

extraInfoGlobalsExecContext "EPOCH" ConwayEraEnvironment (EraRule "EPOCH" ConwayEra) → State (EraRule "EPOCH" ConwayEra) → Signal (EraRule "EPOCH" ConwayEra) → Either OpaqueErrorString (State (EraRule "EPOCH" ConwayEra), [Event (EraRule "EPOCH" ConwayEra)]) → Doc AnsiStyle Source #

ExecSpecRule "NEWEPOCH" ConwayEra Source # 
Instance details

Associated Types

type ExecContext "NEWEPOCH" ConwayEra Source #

type ExecEnvironment "NEWEPOCH" ConwayEra Source #

type ExecState "NEWEPOCH" ConwayEra Source #

type ExecSignal "NEWEPOCH" ConwayEra Source #

Methods

environmentSpecExecContext "NEWEPOCH" ConwayEraSpecification (ExecEnvironment "NEWEPOCH" ConwayEra) Source #

stateSpecExecContext "NEWEPOCH" ConwayEraExecEnvironment "NEWEPOCH" ConwayEraSpecification (ExecState "NEWEPOCH" ConwayEra) Source #

signalSpecExecContext "NEWEPOCH" ConwayEraExecEnvironment "NEWEPOCH" ConwayEraExecState "NEWEPOCH" ConwayEraSpecification (ExecSignal "NEWEPOCH" ConwayEra) Source #

classOfExecSignal "NEWEPOCH" ConwayEraMaybe String Source #

genExecContextGen (ExecContext "NEWEPOCH" ConwayEra) Source #

runAgdaRuleSpecRep (ExecEnvironment "NEWEPOCH" ConwayEra) → SpecRep (ExecState "NEWEPOCH" ConwayEra) → SpecRep (ExecSignal "NEWEPOCH" ConwayEra) → Either OpaqueErrorString (SpecRep (ExecState "NEWEPOCH" ConwayEra)) Source #

translateInputsExecEnvironment "NEWEPOCH" ConwayEraExecState "NEWEPOCH" ConwayEraExecSignal "NEWEPOCH" ConwayEraExecContext "NEWEPOCH" ConwayEraImpTestM ConwayEra (SpecRep (ExecEnvironment "NEWEPOCH" ConwayEra), SpecRep (ExecState "NEWEPOCH" ConwayEra), SpecRep (ExecSignal "NEWEPOCH" ConwayEra)) Source #

testConformanceExecContext "NEWEPOCH" ConwayEraExecEnvironment "NEWEPOCH" ConwayEraExecState "NEWEPOCH" ConwayEraExecSignal "NEWEPOCH" ConwayEraProperty Source #

extraInfoGlobalsExecContext "NEWEPOCH" ConwayEraEnvironment (EraRule "NEWEPOCH" ConwayEra) → State (EraRule "NEWEPOCH" ConwayEra) → Signal (EraRule "NEWEPOCH" ConwayEra) → Either OpaqueErrorString (State (EraRule "NEWEPOCH" ConwayEra), [Event (EraRule "NEWEPOCH" ConwayEra)]) → Doc AnsiStyle Source #

ExecSpecRule "RATIFY" ConwayEra Source # 
Instance details

Associated Types

type ExecContext "RATIFY" ConwayEra Source #

type ExecEnvironment "RATIFY" ConwayEra Source #

type ExecState "RATIFY" ConwayEra Source #

type ExecSignal "RATIFY" ConwayEra Source #

Methods

environmentSpecExecContext "RATIFY" ConwayEraSpecification (ExecEnvironment "RATIFY" ConwayEra) Source #

stateSpecExecContext "RATIFY" ConwayEraExecEnvironment "RATIFY" ConwayEraSpecification (ExecState "RATIFY" ConwayEra) Source #

signalSpecExecContext "RATIFY" ConwayEraExecEnvironment "RATIFY" ConwayEraExecState "RATIFY" ConwayEraSpecification (ExecSignal "RATIFY" ConwayEra) Source #

classOfExecSignal "RATIFY" ConwayEraMaybe String Source #

genExecContextGen (ExecContext "RATIFY" ConwayEra) Source #

runAgdaRuleSpecRep (ExecEnvironment "RATIFY" ConwayEra) → SpecRep (ExecState "RATIFY" ConwayEra) → SpecRep (ExecSignal "RATIFY" ConwayEra) → Either OpaqueErrorString (SpecRep (ExecState "RATIFY" ConwayEra)) Source #

translateInputsExecEnvironment "RATIFY" ConwayEraExecState "RATIFY" ConwayEraExecSignal "RATIFY" ConwayEraExecContext "RATIFY" ConwayEraImpTestM ConwayEra (SpecRep (ExecEnvironment "RATIFY" ConwayEra), SpecRep (ExecState "RATIFY" ConwayEra), SpecRep (ExecSignal "RATIFY" ConwayEra)) Source #

testConformanceExecContext "RATIFY" ConwayEraExecEnvironment "RATIFY" ConwayEraExecState "RATIFY" ConwayEraExecSignal "RATIFY" ConwayEraProperty Source #

extraInfoGlobalsExecContext "RATIFY" ConwayEraEnvironment (EraRule "RATIFY" ConwayEra) → State (EraRule "RATIFY" ConwayEra) → Signal (EraRule "RATIFY" ConwayEra) → Either OpaqueErrorString (State (EraRule "RATIFY" ConwayEra), [Event (EraRule "RATIFY" ConwayEra)]) → Doc AnsiStyle Source #

Inject (EpochExecEnv era) () Source # 
Instance details

Methods

injectEpochExecEnv era → () Source #