| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Test.Cardano.Ledger.Constrained.Conway.GovCert
Description
Specs necessary to generate, environment, state, and signal for the GOVCERT rule
Synopsis
- vStateSpec ∷ ∀ fn era. (IsConwayUniv fn, Era era) ⇒ WitUniv era → Set (Credential 'DRepRole) → Specification fn (VState era)
- govCertSpec ∷ (IsConwayUniv fn, EraCertState era) ⇒ WitUniv era → ConwayGovCertEnv ConwayEra → CertState ConwayEra → Specification fn ConwayGovCert
- notYetResigned ∷ (HasSpec fn x, Ord x, IsConwayUniv fn) ⇒ Map x CommitteeAuthorization → Term fn x → Pred fn
- govCertEnvSpec ∷ ∀ fn. IsConwayUniv fn ⇒ WitUniv ConwayEra → Specification fn (ConwayGovCertEnv ConwayEra)
Documentation
vStateSpec ∷ ∀ fn era. (IsConwayUniv fn, Era era) ⇒ WitUniv era → Set (Credential 'DRepRole) → Specification fn (VState era) Source #
There are no hard constraints on VState, other than witnessing, and delegatee conformance which must align with the conwayCertExecContextSpec
govCertSpec ∷ (IsConwayUniv fn, EraCertState era) ⇒ WitUniv era → ConwayGovCertEnv ConwayEra → CertState ConwayEra → Specification fn ConwayGovCert Source #
notYetResigned ∷ (HasSpec fn x, Ord x, IsConwayUniv fn) ⇒ Map x CommitteeAuthorization → Term fn x → Pred fn Source #
Operations for authenticating a HotKey, or resigning a ColdKey are illegal if that key has already resigned.
govCertEnvSpec ∷ ∀ fn. IsConwayUniv fn ⇒ WitUniv ConwayEra → Specification fn (ConwayGovCertEnv ConwayEra) Source #