| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Test.Cardano.Ledger.Constrained.Conway.ParametricSpec
Description
classes that support Era parametric Specifications.
I.e they work in all eras (Shelley,Allegra,Mary,Alonzo,Babbage,Conway)
In general, each class (except EraSpecTxOut, see below) navigates the differences of a single type family.
The class (EraSpecPParams era) (Defined in ‘Test.Cardano.Ledger.Constrained.Conway.SimplePParams’)
and reExported here, supports specifications over the type Family (PParams era).
The class EraSpecCert supports specifications over the type Family (TxCert era)
The class EraSpecLedger, with methods govStateSpec and newEpochStateSpec, support Parametric Ledger types.
The class EraSpecTxOut (with method correctTxOut and others) supports specifcations over the type Family TxOut.
Additional support for phased out Type Families like InstantaneousRewards,
GenDelegs, FutureGenDelegs, StashedAVVMAddresses, and Ptrs, are handled by methods in EraSpecTxOut
Synopsis
- module Test.Cardano.Ledger.Constrained.Conway.Instances.PParams
- class (HasSpec fn (StashedAVVMAddresses era), EraSpecPParams era, EraSpecDeleg era, HasSpec fn (TxOut era), IsNormalType (TxOut era), EraTxOut era, IsConwayUniv fn) ⇒ EraSpecTxOut era fn where
- irewardSpec ∷ Term fn AccountState → Specification fn (InstantaneousRewards (EraCrypto era))
- hasPtrs ∷ proxy era → Term fn Bool
- correctTxOut ∷ Term fn (Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))) → Term fn (TxOut era) → Pred fn
- txOutValue_ ∷ Term fn (TxOut era) → Term fn (Value era)
- txOutCoin_ ∷ Term fn (TxOut era) → Term fn Coin
- class (Era era, IsConwayUniv fn, HasSpec fn (TxCert era)) ⇒ EraSpecCert era fn where
- txCertSpec ∷ CertEnv era → CertState era → Specification fn (TxCert era)
- txCertKey ∷ TxCert era → CertKey (EraCrypto era)
- class (Era era, EraPParams era) ⇒ EraSpecDeleg era where
- hasGenDelegs ∷ proxy era → Bool
- delegatedStakeReference ∷ (IsConwayUniv fn, Crypto c) ⇒ Term fn (Map (Credential 'Staking c) (KeyHash 'StakePool c)) → Specification fn (StakeReference c)
- data CertKey c
- = StakeKey !(Credential 'Staking c)
- | PoolKey !(KeyHash 'StakePool c)
- | DRepKey !(Credential 'DRepRole c)
- | ColdKey !(Credential 'ColdCommitteeRole c)
- | GenesisKey !(KeyHash 'Genesis c)
- | MirKey !MIRPot
Documentation
class (HasSpec fn (StashedAVVMAddresses era), EraSpecPParams era, EraSpecDeleg era, HasSpec fn (TxOut era), IsNormalType (TxOut era), EraTxOut era, IsConwayUniv fn) ⇒ EraSpecTxOut era fn where Source #
The class EraSpecTxOut supports Era parametric Specifications that primarily navigate the differences in types parameterized type Family TxOut. Additional support for phased out Type Families like InstantaneousRewards, GenDelegs, FutureGenDelegs, StashedAVVMAddresses, and Ptrs, are also provided
Methods
irewardSpec ∷ Term fn AccountState → Specification fn (InstantaneousRewards (EraCrypto era)) Source #
hasPtrs ∷ proxy era → Term fn Bool Source #
correctTxOut ∷ Term fn (Map (Credential 'Staking (EraCrypto era)) (KeyHash 'StakePool (EraCrypto era))) → Term fn (TxOut era) → Pred fn Source #
txOutValue_ ∷ Term fn (TxOut era) → Term fn (Value era) Source #
Extract a Value from a TxOut
txOutCoin_ ∷ Term fn (TxOut era) → Term fn Coin Source #
Extract a Coin from a TxOut
Instances
class (Era era, IsConwayUniv fn, HasSpec fn (TxCert era)) ⇒ EraSpecCert era fn where Source #
Methods
txCertSpec ∷ CertEnv era → CertState era → Specification fn (TxCert era) Source #
Instances
| IsConwayUniv fn ⇒ EraSpecCert Allegra fn Source # | |
| IsConwayUniv fn ⇒ EraSpecCert Alonzo fn Source # | |
| IsConwayUniv fn ⇒ EraSpecCert Babbage fn Source # | |
| IsConwayUniv fn ⇒ EraSpecCert Conway fn Source # | |
| IsConwayUniv fn ⇒ EraSpecCert Mary fn Source # | |
| IsConwayUniv fn ⇒ EraSpecCert Shelley fn Source # | |
class (Era era, EraPParams era) ⇒ EraSpecDeleg era where Source #
Methods
hasGenDelegs ∷ proxy era → Bool Source #
Instances
| EraSpecDeleg Allegra Source # | |
Defined in Test.Cardano.Ledger.Constrained.Conway.Deleg Methods hasGenDelegs ∷ proxy Allegra → Bool Source # | |
| EraSpecDeleg Alonzo Source # | |
Defined in Test.Cardano.Ledger.Constrained.Conway.Deleg Methods hasGenDelegs ∷ proxy Alonzo → Bool Source # | |
| EraSpecDeleg Babbage Source # | |
Defined in Test.Cardano.Ledger.Constrained.Conway.Deleg Methods hasGenDelegs ∷ proxy Babbage → Bool Source # | |
| EraSpecDeleg Conway Source # | |
Defined in Test.Cardano.Ledger.Constrained.Conway.Deleg Methods hasGenDelegs ∷ proxy Conway → Bool Source # | |
| EraSpecDeleg Mary Source # | |
Defined in Test.Cardano.Ledger.Constrained.Conway.Deleg Methods hasGenDelegs ∷ proxy Mary → Bool Source # | |
| EraSpecDeleg Shelley Source # | |
Defined in Test.Cardano.Ledger.Constrained.Conway.Deleg Methods hasGenDelegs ∷ proxy Shelley → Bool Source # | |
delegatedStakeReference ∷ (IsConwayUniv fn, Crypto c) ⇒ Term fn (Map (Credential 'Staking c) (KeyHash 'StakePool c)) → Specification fn (StakeReference c) Source #
Generate random Stake references that have a high probability of being delegated.
Used to aggregate the key used in registering a Certificate. Different certificates use different kinds of Keys, that allows us to use one type to represent all kinds of keys (Similar to DepositPurpose)
Constructors
| StakeKey !(Credential 'Staking c) | |
| PoolKey !(KeyHash 'StakePool c) | |
| DRepKey !(Credential 'DRepRole c) | |
| ColdKey !(Credential 'ColdCommitteeRole c) | |
| GenesisKey !(KeyHash 'Genesis c) | |
| MirKey !MIRPot |
Instances
| Show (CertKey c) Source # | |
| Eq (CertKey c) Source # | |
| Ord (CertKey c) Source # | |
Defined in Test.Cardano.Ledger.Constrained.Conway.Cert | |