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

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.

Instances

Instances details
IsConwayUniv fn ⇒ EraSpecLedger AllegraEra fn Source # 
Instance details

Defined in Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs

IsConwayUniv fn ⇒ EraSpecLedger AlonzoEra fn Source # 
Instance details

Defined in Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs

IsConwayUniv fn ⇒ EraSpecLedger BabbageEra fn Source # 
Instance details

Defined in Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs

IsConwayUniv fn ⇒ EraSpecLedger ConwayEra fn Source # 
Instance details

Defined in Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs

IsConwayUniv fn ⇒ EraSpecLedger MaryEra fn Source # 
Instance details

Defined in Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs

IsConwayUniv fn ⇒ EraSpecLedger ShelleyEra fn Source # 
Instance details

Defined in Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs

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.

canFollowIsConwayUniv fn ⇒ Term fn ProtVerTerm fn ProtVerPred fn Source #

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

vstateSpec ∷ ∀ fn era. (IsConwayUniv fn, Era era) ⇒ WitUniv era → Term fn EpochNoTerm 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.

aggregateDRepMap (Credential 'Staking) DRepMap (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 AccountStateTerm fn (Map (KeyHash 'StakePool) PoolParams) → Specification fn (DState era) Source #

pstateSpec ∷ (IsConwayUniv fn, Era era) ⇒ WitUniv era → Term fn EpochNoSpecification fn (PState era) Source #

certStateSpec ∷ ∀ era fn. EraSpecLedger era fn ⇒ WitUniv era → Term fn AccountStateTerm fn EpochNoSpecification 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 #

ledgerStateSpec ∷ ∀ era fn. EraSpecLedger era fn ⇒ PParams era → WitUniv era → Term fn AccountStateTerm fn EpochNoSpecification fn (LedgerState era) 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 EpochNoSpecification fn (EpochState era) 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)