Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Specs necessary to generate, environment, state, and signal for the DELEG rule
Synopsis
- someZeros ∷ ∀ fn. IsConwayUniv fn ⇒ Specification fn RDPair
- rewDepMapSpec ∷ (Era era, IsConwayUniv fn) ⇒ WitUniv era → Map RewardAccount Coin → Specification fn (Map (Credential 'Staking) RDPair)
- rewDepMapSpec2 ∷ ∀ fn era. (Era era, IsConwayUniv fn) ⇒ WitUniv era → Map RewardAccount Coin → Specification fn (Map (Credential 'Staking) RDPair)
- coinToWord64 ∷ Coin → Word64
- wdrlCredentials ∷ Map RewardAccount Coin → Set (Credential 'Staking)
- keyHashWdrl ∷ Map RewardAccount Coin → Set (Credential 'Staking)
- dStateSpec ∷ ∀ fn era. (IsConwayUniv fn, EraSpecDeleg era) ⇒ WitUniv era → Map RewardAccount Coin → Specification fn (DState era)
- conwayDelegCertSpec ∷ ∀ fn era. (EraPParams era, IsConwayUniv fn) ⇒ ConwayDelegEnv era → CertState era → Specification fn ConwayDelegCert
- delegEnvSpec ∷ (EraSpecPParams era, IsConwayUniv fn) ⇒ Specification fn (ConwayDelegEnv era)
- shelleyDelegCertSpec ∷ ∀ fn era. (EraPParams era, IsConwayUniv fn) ⇒ WitUniv era → ConwayDelegEnv era → DState era → Specification fn ShelleyDelegCert
- class (Era era, EraPParams era) ⇒ EraSpecDeleg era where
- hasGenDelegs ∷ proxy era → Bool
Documentation
someZeros ∷ ∀ fn. IsConwayUniv fn ⇒ Specification fn RDPair Source #
Specify that some of the rewards in the RDPair's are zero. without this in the DState, it is hard to generate the ConwayUnRegCert certificate, since it requires a rewards balance of 0. We also specify that both reward and deposit are greater than (Coin 0)
rewDepMapSpec ∷ (Era era, IsConwayUniv fn) ⇒ WitUniv era → Map RewardAccount Coin → Specification fn (Map (Credential 'Staking) RDPair) Source #
Specification for the RewardDepositMap of the Umap in the DState It must be witnessed, and conform to some properties relating to the withdrawals map, which is part of the context, so passed as an arg.
rewDepMapSpec2 ∷ ∀ fn era. (Era era, IsConwayUniv fn) ⇒ WitUniv era → Map RewardAccount Coin → Specification fn (Map (Credential 'Staking) RDPair) Source #
coinToWord64 ∷ Coin → Word64 Source #
keyHashWdrl ∷ Map RewardAccount Coin → Set (Credential 'Staking) Source #
dStateSpec ∷ ∀ fn era. (IsConwayUniv fn, EraSpecDeleg era) ⇒ WitUniv era → Map RewardAccount Coin → Specification fn (DState era) Source #
conwayDelegCertSpec ∷ ∀ fn era. (EraPParams era, IsConwayUniv fn) ⇒ ConwayDelegEnv era → CertState era → Specification fn ConwayDelegCert Source #
delegEnvSpec ∷ (EraSpecPParams era, IsConwayUniv fn) ⇒ Specification fn (ConwayDelegEnv era) Source #
shelleyDelegCertSpec ∷ ∀ fn era. (EraPParams era, IsConwayUniv fn) ⇒ WitUniv era → ConwayDelegEnv era → DState era → Specification fn ShelleyDelegCert Source #
class (Era era, EraPParams era) ⇒ EraSpecDeleg era where Source #
hasGenDelegs ∷ proxy era → Bool Source #
Instances
EraSpecDeleg AllegraEra Source # | |
Defined in Test.Cardano.Ledger.Constrained.Conway.Deleg hasGenDelegs ∷ proxy AllegraEra → Bool Source # | |
EraSpecDeleg AlonzoEra Source # | |
Defined in Test.Cardano.Ledger.Constrained.Conway.Deleg hasGenDelegs ∷ proxy AlonzoEra → Bool Source # | |
EraSpecDeleg BabbageEra Source # | |
Defined in Test.Cardano.Ledger.Constrained.Conway.Deleg hasGenDelegs ∷ proxy BabbageEra → Bool Source # | |
EraSpecDeleg ConwayEra Source # | |
Defined in Test.Cardano.Ledger.Constrained.Conway.Deleg hasGenDelegs ∷ proxy ConwayEra → Bool Source # | |
EraSpecDeleg MaryEra Source # | |
Defined in Test.Cardano.Ledger.Constrained.Conway.Deleg hasGenDelegs ∷ proxy MaryEra → Bool Source # | |
EraSpecDeleg ShelleyEra Source # | |
Defined in Test.Cardano.Ledger.Constrained.Conway.Deleg hasGenDelegs ∷ proxy ShelleyEra → Bool Source # |