| 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 (StashedAVVMAddresses era), EraSpecPParams era, EraSpecDeleg era, HasSpec (TxOut era), IsNormalType (TxOut era), EraTxOut era, GenScript era) ⇒ EraSpecTxOut era where
- irewardSpec ∷ WitUniv era → Term ChainAccountState → Specification InstantaneousRewards
- hasPtrs ∷ proxy era → Term Bool
- txOutValue_ ∷ Term (TxOut era) → Term (Value era)
- txOutCoin_ ∷ Term (TxOut era) → Term Coin
- txOutAddr_ ∷ Term (TxOut era) → Term Addr
- txOutSpec ∷ ∀ era. EraSpecTxOut era ⇒ WitUniv era → Term (Map (Credential 'Staking) (KeyHash 'StakePool)) → Term (TxOut era) → Pred
- class (HasSpec (TxCert era), EraCertState era) ⇒ EraSpecCert era where
- txCertSpec ∷ WitUniv era → CertEnv era → CertState era → Specification (TxCert era)
- txCertKey ∷ TxCert era → CertKey
- certStateSpec ∷ WitUniv era → Set (Credential 'DRepRole) → Map RewardAccount Coin → Specification (CertState era)
- class (Era era, EraPParams era) ⇒ EraSpecDeleg era where
- hasGenDelegs ∷ proxy era → Bool
- delegatedStakeReference ∷ Term (Map (Credential 'Staking) (KeyHash 'StakePool)) → Specification StakeReference
- data CertKey
- = StakeKey !(Credential 'Staking)
- | PoolKey !(KeyHash 'StakePool)
- | DRepKey !(Credential 'DRepRole)
- | ColdKey !(Credential 'ColdCommitteeRole)
- | GenesisKey !(KeyHash 'Genesis)
- | MirKey !MIRPot
Documentation
class (HasSpec (StashedAVVMAddresses era), EraSpecPParams era, EraSpecDeleg era, HasSpec (TxOut era), IsNormalType (TxOut era), EraTxOut era, GenScript era) ⇒ EraSpecTxOut era 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 ∷ WitUniv era → Term ChainAccountState → Specification InstantaneousRewards Source #
hasPtrs ∷ proxy era → Term Bool Source #
txOutValue_ ∷ Term (TxOut era) → Term (Value era) Source #
Extract a Value from a TxOut
txOutCoin_ ∷ Term (TxOut era) → Term Coin Source #
Extract a Coin from a TxOut
txOutAddr_ ∷ Term (TxOut era) → Term Addr Source #
Extract an Addr from a TxOut
Instances
txOutSpec ∷ ∀ era. EraSpecTxOut era ⇒ WitUniv era → Term (Map (Credential 'Staking) (KeyHash 'StakePool)) → Term (TxOut era) → Pred Source #
An Era polymorhic Specification for type family TxOut
class (HasSpec (TxCert era), EraCertState era) ⇒ EraSpecCert era where Source #
Methods
txCertSpec ∷ WitUniv era → CertEnv era → CertState era → Specification (TxCert era) Source #
txCertKey ∷ TxCert era → CertKey Source #
certStateSpec ∷ WitUniv era → Set (Credential 'DRepRole) → Map RewardAccount Coin → Specification (CertState era) Source #
Instances
class (Era era, EraPParams era) ⇒ EraSpecDeleg era where Source #
Methods
hasGenDelegs ∷ proxy era → Bool Source #
Instances
| EraSpecDeleg AllegraEra Source # | |
Defined in Test.Cardano.Ledger.Constrained.Conway.Deleg Methods hasGenDelegs ∷ proxy AllegraEra → Bool Source # | |
| EraSpecDeleg AlonzoEra Source # | |
Defined in Test.Cardano.Ledger.Constrained.Conway.Deleg Methods hasGenDelegs ∷ proxy AlonzoEra → Bool Source # | |
| EraSpecDeleg BabbageEra Source # | |
Defined in Test.Cardano.Ledger.Constrained.Conway.Deleg Methods hasGenDelegs ∷ proxy BabbageEra → Bool Source # | |
| EraSpecDeleg ConwayEra Source # | |
Defined in Test.Cardano.Ledger.Constrained.Conway.Deleg Methods hasGenDelegs ∷ proxy ConwayEra → Bool Source # | |
| EraSpecDeleg MaryEra Source # | |
Defined in Test.Cardano.Ledger.Constrained.Conway.Deleg Methods hasGenDelegs ∷ proxy MaryEra → Bool Source # | |
| EraSpecDeleg ShelleyEra Source # | |
Defined in Test.Cardano.Ledger.Constrained.Conway.Deleg Methods hasGenDelegs ∷ proxy ShelleyEra → Bool Source # | |
delegatedStakeReference ∷ Term (Map (Credential 'Staking) (KeyHash 'StakePool)) → Specification StakeReference 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) | |
| PoolKey !(KeyHash 'StakePool) | |
| DRepKey !(Credential 'DRepRole) | |
| ColdKey !(Credential 'ColdCommitteeRole) | |
| GenesisKey !(KeyHash 'Genesis) | |
| MirKey !MIRPot |